Module prop::univalence

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

• HLev
  Implemented by homotopy levels.
• HomotopyEquality
  Implemented by homotopy equalities.
• HomotopyEquivalence
  Implemented by homotopy equivalences.
• HomotopyLevel0
  Homotopy Level.

Functions

• eq_lift
  Lift (a == b) == (a ~~ b) to (a == b) ~~ (a ~~ b).
• eq_univ_to_eqq
  ((a == b) => ((a == b) ~~ (a ~~ b))) => ((a == b) => (a ~~ b)).
• eqq_eq_q
  ((a == b) == (a ~~ b)) => ((a == b) ~~ (a ~~ b)).
• eqq_to_univ
  ((a == b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b)).
• from_hom_eq_2
  hom_eq(2, a, b) => (a == b) ⋀ ((a ~~ b) == (b ~~ b)).
• higher
  Higher quality univalence.
• hom_eq_q
  ((a == b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b)).
• hom_eq_refl
  hom_eq(n, a, a).
• hom_eq_symmetry
  hom_eq(n, a, b) => hom_eq(n, b, a).
• hom_eq_transitivity
  hom_eq(n, a, b) ⋀ hom_eq(n, b, c) => hom_eq(n, a, c).
• hom_to_univ
  ((a => b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b)).
• q_to_hom_eq_2
  (a ~~ b) => hom_eq(2, a, b).
• to_hom_eq_2
  (a == b) ⋀ ((a ~~ a) == (b ~~ b)) => hom_eq(2, a, b).
• univ_eq_q
  ((a == b) == (a ~~ b)) ~~ ((a == b) ~~ (a ~~ b)).
• univ_to_eqq
  ((a == b) ~~ (a ~~ b)) => ((a == b) => (a ~~ b)).

Type Definitions

• EqUniv
  Univalence from equality.
• Hom
  A homotopy path between paths A and B.
• HomEq
  Homotopy equality of level N.
• HomEq2
  Homotopy equality of level 2.
• HomEq3
  Homotopy equality of level 3.
• Univ
  Quality univalence: Equality is qual to quality.