Browse Source

Rearrange definitions in example code

Amélia Liao 2 years ago
committed by Abigail Magalhães
parent
commit
d583216120
1 changed files with 3 additions and 3 deletions
  1. +3
    -3
      intro.tt

+ 3
- 3
intro.tt View File

@ -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 : 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) 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 : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B)
uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where 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 : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A})
pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A}) pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A})


Loading…
Cancel
Save