Quotients of families indexed by a finite type #
This file proves some basic facts and defines lifting and recursion principle for quotients indexed by a finite type.
Main definitions #
Quotient.finChoice
: Given a functionf : Π i, Quotient (S i)
on a fintypeι
, returns the class of functionsΠ i, α i
sending eachi
to an element of the classf i
.Quotient.finChoiceEquiv
: A finite family of quotients is equivalent to a quotient of finite families.Quotient.finLiftOn
: Given a fintypeι
. A function onΠ i, α i
which respects setoidS i
for eachi
can be lifted to a function onΠ i, Quotient (S i)
.Quotient.finRecOn
: Recursion principle for quotients indexed by a finite type. It is the dependent version ofQuotient.finLiftOn
.
Given a collection of setoids indexed by a type ι
, a 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
Instances For
Choice-free induction principle for quotients indexed by a List
.
Choice-free induction principle for quotients indexed by a finite type.
See Quotient.induction_on_pi
for the general version assuming Classical.choice
.
Choice-free induction principle for quotients indexed by a finite type.
See Quotient.induction_on_pi
for the general version assuming Classical.choice
.
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.
See Quotient.choice
for the noncomputable general version.
Equations
Instances For
Lift a function on ∀ i, α i
to a function on ∀ i, Quotient (S i)
.
Equations
Instances For
Quotient.finChoice
as an equivalence.
Equations
Instances For
Recursion principle for quotients indexed by a finite type.
Equations
Instances For
Recursion principle for quotients indexed by a finite type.
Equations
Instances For
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
Lift a function on ∀ i, α i
to a function on ∀ i, Trunc (α i)
.
Equations
Instances For
Trunc.finChoice
as an equivalence.
Equations
Instances For
Recursion principle for Trunc
s indexed by a finite type.