Quotient types #
This module extends the core library's treatment of quotient types (Init.Core
).
Tags #
quotient
Recursion on two Quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
.
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
and applies it.
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
with values in a quotient of
γ
.
Instances For
A binary version of Quot.recOnSubsingleton
.
Instances For
Note that this provides DecidableRel (Quot.Lift₂ f ha hb)
when α = β
.
The canonical quotient map into a Quotient
.
Instances For
Induction on two Quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Instances For
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.
Instances For
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.
Instances For
Note that this provides DecidableRel (Quotient.lift₂ f h)
when α = β
.
Quot.mk r
is a surjective function.
Quotient.mk'
is a surjective function.
Unwrap the VM representation of a quotient to obtain an element of the equivalence class. Computable but unsound.
Instances For
Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.
Instances For
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
A version of Trunc.recOn
assuming the codomain is a Subsingleton
.
Instances For
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.
Instances For
Quotient.mk''
is a surjective function.
A version of Quotient.liftOn
taking {s : Setoid α}
as an implicit argument instead of an
instance argument.
Instances For
A version of Quotient.liftOn₂
taking {s₁ : Setoid α} {s₂ : Setoid β}
as implicit arguments
instead of instance arguments.
Instances For
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.inductionOn
taking {s : Setoid α}
as an implicit argument instead
of an instance argument.
A version of Quotient.inductionOn₂
taking {s₁ : Setoid α} {s₂ : Setoid β}
as implicit
arguments instead of instance arguments.
A version of Quotient.inductionOn₃
taking {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ}
as implicit arguments instead of instance arguments.
A version of Quotient.recOnSubsingleton
taking {s₁ : Setoid α}
as an implicit argument
instead of an instance argument.
Instances For
A version of Quotient.recOnSubsingleton₂
taking {s₁ : Setoid α} {s₂ : Setoid α}
as implicit arguments instead of instance arguments.
Instances For
Recursion on two Quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Instances For
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.
Instances For
A version of Quotient.out
taking {s₁ : Setoid α}
as an implicit argument instead of an
instance argument.