Quotient types #
This module extends the core library's treatment of quotient types (init.data.quot
).
Tags #
quotient
Equations
- quot.inhabited r = {default := quot.mk r inhabited.default}
Recursion on two quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
If ra
is a subrelation of ra'
, then we have a natural map quot ra → quot ra'
.
Equations
- quot.map_right h = quot.map id h
Weaken the relation of a quotient. This is the same as quot.map id
.
Equations
- quot.factor r s h = quot.lift (quot.mk s) _
Alias of quot.lift_beta
.
Descends a function f : α → β → γ
to quotients of α
and β
.
Equations
- quot.lift₂ f hr hs q₁ q₂ = quot.lift (λ (a : α), quot.lift (f a) _) _ q₁ q₂
Descends a function f : α → β → γ
to quotients of α
and β
and applies it.
Equations
- p.lift_on₂ q f hr hs = quot.lift₂ f hr hs p q
Descends a function f : α → β → γ
to quotients of α
and β
wih values in a quotient of
γ
.
Equations
- quot.map₂ f hr hs q₁ q₂ = quot.lift₂ (λ (a : α) (b : β), quot.mk t (f a b)) _ _ q₁ q₂
A binary version of quot.rec_on_subsingleton
.
Equations
- q₁.rec_on_subsingleton₂ q₂ f = q₁.rec_on_subsingleton (λ (a : α), q₂.rec_on_subsingleton (λ (b : β), f a b))
Equations
- quot.lift.decidable_pred r f h = λ (q : quot (λ (a b : α), r a b)), q.rec_on_subsingleton hf
Note that this provides decidable_rel (quot.lift₂ f ha hb)
when α = β
.
Equations
- quot.lift₂.decidable_pred r s f ha hb q₁ = λ (q₂ : quot (λ (b₁ b₂ : β), s b₁ b₂)), q₁.rec_on_subsingleton₂ q₂ hf
Equations
- quot.lift_on.decidable r q f h = quot.lift.decidable_pred (λ (a b : α), r a b) f h q
Equations
- quot.lift_on₂.decidable r s q₁ q₂ f ha hb = quot.lift₂.decidable_pred (λ (a₁ a₂ : α), r a₁ a₂) (λ (b₁ b₂ : β), s b₁ b₂) f ha hb q₁ q₂
Equations
Induction on two quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Equations
- qa.hrec_on₂ qb f c = quot.hrec_on₂ qa qb f _ _
Map a function f : α → β
that sends equivalent elements to equivalent elements
to a function quotient sa → quotient sb
. Useful to define unary operations on quotients.
Equations
- quotient.map f h = quot.map f h
Map a function f : α → β → γ
that sends equivalent elements to equivalent elements
to a function f : quotient sa → quotient sb → quotient sc
.
Useful to define binary operations on quotients.
Equations
- quotient.map₂ f h = quotient.lift₂ (λ (x : α) (y : β), ⟦f x y⟧) _
Equations
- quotient.lift.decidable_pred f h = quot.lift.decidable_pred (λ (a b : α), a ≈ b) f h
Note that this provides decidable_rel (quotient.lift₂ f h)
when α = β
.
Equations
- quotient.lift₂.decidable_pred f h q₁ = λ (q₂ : quotient sb), q₁.rec_on_subsingleton₂ q₂ hf
Equations
- quotient.lift_on.decidable q f h = quotient.lift.decidable_pred f h q
Equations
- quotient.lift_on₂.decidable q₁ q₂ f h = quotient.lift₂.decidable_pred f h q₁ q₂
quot.mk r
is a surjective function.
quotient.mk
is a surjective function.
Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.
Equations
- q.out = classical.some _
Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.
Equations
Given a function f : Π i, quotient (S i)
, returns the class of functions Π i, α i
sending
each i
to an element of the class f i
.
Equations
- quotient.choice f = ⟦(λ (i : ι), (f i).out)⟧
Truncation #
trunc α
is the quotient of α
by the always-true relation. This
is related to the propositional truncation in HoTT, and is similar
in effect to nonempty α
, but unlike nonempty α
, trunc α
is data,
so the VM representation is the same as α
, and so this can be used to
maintain computability.
Instances for trunc
Equations
Any constant function lifts to a function out of the truncation
Equations
- trunc.lift f c = quot.lift f _
Lift a constant function on q : trunc α
.
Equations
- q.lift_on f c = trunc.lift f c q
A version of trunc.rec_on
assuming the codomain is a subsingleton
.
Equations
- q.rec_on_subsingleton f = trunc.rec f _ q
Versions of quotient definitions and lemmas ending in '
use unification instead
of typeclass inference for inferring the setoid
argument. This is useful when there are
several different quotient relations on a type, for example quotient groups, rings and modules.
A version of quotient.mk
taking {s : setoid α}
as an implicit argument instead of an
instance argument.
Equations
- quotient.mk' a = quot.mk setoid.r a
quotient.mk'
is a surjective function.
A version of quotient.lift_on
taking {s : setoid α}
as an implicit argument instead of an
instance argument.
A version of quotient.lift_on₂
taking {s₁ : setoid α} {s₂ : setoid β}
as implicit arguments
instead of instance arguments.
A version of quotient.ind
taking {s : setoid α}
as an implicit argument instead of an
instance argument.
A version of quotient.ind₂
taking {s₁ : setoid α} {s₂ : setoid β}
as implicit arguments
instead of instance arguments.
A version of quotient.induction_on
taking {s : setoid α}
as an implicit argument instead
of an instance argument.
A version of quotient.induction_on₂
taking {s₁ : setoid α} {s₂ : setoid β}
as implicit
arguments instead of instance arguments.
A version of quotient.induction_on₃
taking {s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ}
as implicit arguments instead of instance arguments.
A version of quotient.rec_on_subsingleton
taking {s₁ : setoid α}
as an implicit argument
instead of an instance argument.
Equations
- q.rec_on_subsingleton' f = q.rec_on_subsingleton f
A version of quotient.rec_on_subsingleton₂
taking {s₁ : setoid α} {s₂ : setoid α}
as implicit arguments instead of instance arguments.
Equations
- q₁.rec_on_subsingleton₂' q₂ f = q₁.rec_on_subsingleton₂ q₂ f
Recursion on a quotient
argument a
, result type depends on ⟦a⟧
.
Equations
- qa.hrec_on' f c = quot.hrec_on qa f c
Recursion on two quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Map a function f : α → β
that sends equivalent elements to equivalent elements
to a function quotient sa → quotient sb
. Useful to define unary operations on quotients.
Equations
- quotient.map' f h = quot.map f h
A version of quotient.map₂
using curly braces and unification.
Equations
- quotient.map₂' f h = quotient.map₂ f h
A version of quotient.out
taking {s₁ : setoid α}
as an implicit argument instead of an
instance argument.
Equations
- quotient.lift_on'.decidable q f h = quotient.lift.decidable_pred f h q
Equations
- quotient.lift_on₂'.decidable q₁ q₂ f h = quotient.lift₂.decidable_pred (λ (a₁ : α), f a₁) h q₁ q₂