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⟧
.
Equations
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
.
Equations
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
and applies it.
Equations
Instances For
Descends a function f : α → β → γ
to quotients of α
and β
with values in a quotient of
γ
.
Equations
Instances For
A binary version of Quot.recOnSubsingleton
.
Equations
Instances For
Equations
Note that this provides DecidableRel (Quot.Lift₂ f ha hb)
when α = β
.
Equations
Equations
Equations
Places an element of a type into the quotient that equates terms according to an equivalence relation.
The setoid instance is provided explicitly. Quotient.mk'
uses instance synthesis instead.
Given v : α
, Quotient.mk s v : Quotient s
is like v
, except all observations of v
's value
must respect s.r
. Quotient.lift
allows values in a quotient to be mapped to other types, so long
as the mapping respects s.r
.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
Induction on two Quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Equations
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.
Equations
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.
Equations
Instances For
Equations
Note that this provides DecidableRel (Quotient.lift₂ f h)
when α = β
.
Equations
Equations
Quot.mk r
is a surjective function.
Quotient.mk
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.
Equations
Instances For
Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.
Equations
Instances For
Given a class of functions q : @Quotient (∀ i, α i) _
, returns the class of i
-th projection
Quotient (S i)
.
Equations
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.
Equations
Instances For
A version of Trunc.recOn
assuming the codomain is a Subsingleton
.
Equations
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.
Equations
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.
Equations
Instances For
A version of Quotient.liftOn₂
taking {s₁ : Setoid α} {s₂ : Setoid β}
as implicit arguments
instead of instance arguments.
Equations
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.
Equations
Instances For
A version of Quotient.recOnSubsingleton₂
taking {s₁ : Setoid α} {s₂ : Setoid α}
as implicit arguments instead of instance arguments.
Equations
Instances For
Recursion on two Quotient
arguments a
and b
, result type depends on ⟦a⟧
and ⟦b⟧
.
Equations
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.
Equations
Instances For
A version of Quotient.map₂
using curly braces and unification.