From 3810bda5c9689cbedea3976567f2f762fee7f5a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Tue, 4 May 2021 00:35:58 -0300 Subject: [PATCH] oops, shuffled some definitions Too Hard --- intro.tt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/intro.tt b/intro.tt index 7d2c035..238dc89 100644 --- a/intro.tt +++ b/intro.tt @@ -1631,11 +1631,11 @@ EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d w path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e) path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e) +pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B +pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A}) + uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B) uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where - pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B - pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A}) - pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A}) pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A})