Module prop::univalence
source · [−]Expand description
Quality Univalence
Helper methods for reasoning about Quality Univalence. For more information about Quality, see the documentation of the “quality” module.
Equality ==
has the property that left or right side can be substituted.
Univalence is the idea that a different form of equivalence (partial or total),
can be converted back and forth with equality and this translation back and forth itself
is also an equivalence.
From (a == b) => (a ~~ b)
, one can prove (a == b) == (a ~~ b)
.
However, this is not strong enough to prove (a == b) ~~ (a ~~ b)
.
The latter is called “Quality Univalence”.
Quality vs Homotopy Univalence
Quality Univalence differs from Homotopy Univalence by these properties:
- Quality:
(a == b) => (a ~~ b)
(Equality implies Quality) - Homotopy:
(a => b) => (a ~= b)
(Implication implies Equivalence)
The Homotopy Univalence axiom is the following:
(a == b) ~= (a ~= b)
Under the homotopy univalence axiom with path semantical quality,
quality univalence is equal to homotopy univalence.
Since equality is homotopic equivalent to homotopy equivalence,
and equality is qual to quality, it means ~=
can be replaced by ~~
.
Traits
Shorthand for homotopy proposition.
Homotopy level.
Functions
Lift (a == b) == (a ~~ b)
to (a == b) ~~ (a ~~ b)
.
((a == b) => ((a == b) ~~ (a ~~ b))) => ((a == b) => (a ~~ b))
.
((a == b) == (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.
((a == b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.
(x : a) ⋀ (x : b) => (a ~~ b)
when a
and b
are homotopy level 0.
Proves that homotopy level 0 has quality between any members.
(x : a) ⋀ (x : b) ⋀ ((x ~~ x) == x) => (a ~~ b)
when a
and b
are homotopy level 1 or larger.
Proves that homotopy level 1 or higher has quality between self-quality of any members.
Get the type of the path between paths.
Higher quality univalence.
((a == b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.
((a => b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.
Lift type of path.
((a == b) == (a ~~ b)) ~~ ((a == b) ~~ (a ~~ b))
.
((a == b) ~~ (a ~~ b)) => ((a == b) => (a ~~ b))
.