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
- Implemented by homotopy levels.
- Implemented by homotopy equalities.
- Implemented by homotopy equivalences.
- 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))
.hom_eq(2, a, b) => (a == b) ⋀ ((a ~~ b) == (b ~~ b))
.- Higher quality univalence.
((a == b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.hom_eq(n, a, a)
.hom_eq(n, a, b) => hom_eq(n, b, a)
.hom_eq(n, a, b) ⋀ hom_eq(n, b, c) => hom_eq(n, a, c)
.((a => b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
.(a ~~ b) => hom_eq(2, a, b)
.(a == b) ⋀ ((a ~~ a) == (b ~~ b)) => hom_eq(2, a, b)
.((a == b) == (a ~~ b)) ~~ ((a == b) ~~ (a ~~ b))
.((a == b) ~~ (a ~~ b)) => ((a == b) => (a ~~ b))
.
Type Definitions
- Univalence from equality.
- A homotopy path between paths
A
andB
. - Homotopy equality of level
N
. - Homotopy equality of level 2.
- Homotopy equality of level 3.
- Quality univalence: Equality is qual to quality.