# Quotients of families indexed by a finite type #

This file provides Quotient.finChoice, a mechanism to go from a finite family of quotients to a quotient of finite families.

## Main definitions #

• Quotient.finChoice
def Quotient.finChoiceAux {ι : Type u_1} [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) :
((i : ι) → i lQuotient (S i))Quotient inferInstance

An auxiliary function for Quotient.finChoice. Given a collection of setoids indexed by a type ι, a (finite) list l of indices, and a function that for each i ∈ l gives a term of the corresponding quotient type, then there is a corresponding term in the quotient of the product of the setoids indexed by l.

Equations
• One or more equations did not get rendered due to their size.
• = fun (i : ι) (h : i []) => nomatch
Instances For
theorem Quotient.finChoiceAux_eq {ι : Type u_1} [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) (f : (i : ι) → i lα i) :
(Quotient.finChoiceAux l fun (i : ι) (h : i l) => f i h) = f
def Quotient.finChoice {ι : Type u_1} [] [] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (f : (i : ι) → Quotient (S i)) :
Quotient inferInstance

Given a collection of setoids indexed by a fintype ι and a function that for each i : ι gives a term of the corresponding quotient type, then there is corresponding term in the quotient of the product of the setoids.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Quotient.finChoice_eq {ι : Type u_1} [] [] {α : ιType u_2} [(i : ι) → Setoid (α i)] (f : (i : ι) → α i) :
(Quotient.finChoice fun (i : ι) => f i) = f
def Trunc.finChoice {ι : Type u_1} [] [] {α : ιType u_2} (f : (i : ι) → Trunc (α i)) :
Trunc ((i : ι) → α i)

Given a function that for each i : ι gives a term of the corresponding truncation type, then there is corresponding term in the truncation of the product.

Equations
Instances For
theorem Trunc.finChoice_eq {ι : Type u_1} [] [] {α : ιType u_2} (f : (i : ι) → α i) :
(Trunc.finChoice fun (i : ι) => Trunc.mk (f i)) =