Library UniMath.MoreFoundations.Univalence

Additional results about univalence

Require Import UniMath.Foundations.UnivalenceAxiom.

Funextsec and toforallpaths are mutually inverses

Lemma funextsec_toforallpaths {T : UU} {P : T -> UU} {f g : ∏ t : T , P t} :
∏ (h : f = g ), funextsec _ _ _ (toforallpaths _ _ _ h) = h.
Show proof.

intro h; exact (!homotinvweqweq0 (weqtoforallpaths _ _ _) h).

Funextsec and toforallpaths are mutually inverses

Lemma toforallpaths_funextsec {T : UU} {P : T -> UU} {f g : ∏ t : T , P t} :
∏ (h : ∏ t : T , f t = g t ), toforallpaths _ _ _ (funextsec _ _ _ h) = h.
Show proof.

intro h; exact (homotweqinvweq (weqtoforallpaths _ _ _) h).