Merge pull request #141 from rzk-lang/representable-isos

Representable isos
rzk-lang · Dec 15, 2023 · 33b8fc5 · 33b8fc5
2 parents 296a11b + 06abed0
commit 33b8fc5
Show file tree

Hide file tree

Showing 2 changed files with 382 additions and 2 deletions.
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
@@ -13,9 +13,9 @@ This is a literate `rzk` file:
 - `hott/01-paths.rzk.md` - We require basic path algebra.
 - `hott/04-equivalences.rzk.md` - We require the notion of equivalence between
   types.
-- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
+- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
   their subshapes.
-- `04-extension-types.rzk.md` — We use extension extensionality.
+- `03-extension-types.rzk.md` — We use extension extensionality.
 - `05-segal-types.rzk.md` - We use the notion of hom types.
 
 Some of the definitions in this file rely on function extensionality and

diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md
@@ -941,3 +941,383 @@ In particular, every contractible type is Rezk
   : is-rezk Unit
   := is-rezk-is-contr Unit (is-contr-Unit)
 ```
+
+## Representable isomorphisms.
+
+We prove [RS17, Proposition 10.11]. We first need to access the fiberwise
+equivalence with no extra data, and then define some helpers.
+
+```rzk
+#section representable-isomorphisms
+
+#variable A : U
+#variable is-segal-A : is-segal A
+#variables a a' : A
+#variable ψ : (x : A) → (Equiv (hom A a x) (hom A a' x))
+
+#def map-representable-equiv
+  : ( x : A) → (hom A a x) → (hom A a' x)
+  := \ x → first (ψ x)
+
+#def inverse-representable-equiv
+  : ( x : A) → (has-inverse (hom A a x) (hom A a' x) (first (ψ x)))
+  :=
+  \ x →
+  has-inverse-is-equiv
+    ( hom A a x)
+    ( hom A a' x)
+    ( first (ψ x))
+    ( second (ψ x))
+
+#def inv-map-representable-equiv uses (A a a' ψ)
+  : ( x : A) → (hom A a' x) → (hom A a x)
+  := \ x → first (inverse-representable-equiv x)
+
+#def arr-map-representable-equiv
+  : hom A a' a
+  := evid A a (hom A a') (map-representable-equiv)
+
+#def arr-inv-map-representable-equiv
+  : hom A a a'
+  := evid A a' (hom A a) (inv-map-representable-equiv)
+```
+
+We now show that `#!rzk arrow-map-representable-equiv` has section
+`#!rzk arrow-inv-map-representable-equiv`.
+
+```rzk
+#def htpy-inv-map-fib-equiv-map-fib-equiv-id uses (A a a' ψ)
+  : ( x : A)
+  → ( homotopy
+      ( hom A a x)
+      ( hom A a x)
+      ( comp
+        ( hom A a x)
+        ( hom A a' x)
+        ( hom A a x)
+        ( inv-map-representable-equiv x)
+        ( map-representable-equiv x))
+      ( identity (hom A a x)))
+  := \ x → first (second (inverse-representable-equiv x))
+```
+
+We compute the required paths for the section of
+`#!rzk arrow-map-representable-equiv`.
+
+```rzk
+#def rev-comp-id-comp-arr-inv-map-arr-map-id-a uses (A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a a' a
+      arr-inv-map-representable-equiv
+      arr-map-representable-equiv
+  =_{ hom A a a}
+    comp-is-segal A is-segal-A a a a
+      ( comp-is-segal A is-segal-A a a' a
+          arr-inv-map-representable-equiv
+          arr-map-representable-equiv)
+      ( id-hom A a)
+  :=
+  rev
+    ( hom A a a)
+    ( comp-is-segal A is-segal-A a a a
+      ( comp-is-segal A is-segal-A a a' a
+          arr-inv-map-representable-equiv
+          arr-map-representable-equiv)
+      ( id-hom A a))
+    ( comp-is-segal A is-segal-A a a' a
+        arr-inv-map-representable-equiv
+        arr-map-representable-equiv)
+    ( comp-id-is-segal A is-segal-A a a
+      ( comp-is-segal A is-segal-A a a' a
+          arr-inv-map-representable-equiv
+          arr-map-representable-equiv))
+
+#def assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a
+  uses (A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a a a
+      ( comp-is-segal A is-segal-A a a' a
+         arr-inv-map-representable-equiv
+         arr-map-representable-equiv)
+      ( id-hom A a)
+  =_{ hom A a a}
+    comp-is-segal A is-segal-A a a' a
+      ( arr-inv-map-representable-equiv)
+      ( comp-is-segal A is-segal-A a' a a
+        ( arr-map-representable-equiv)
+        ( id-hom A a))
+  :=
+  associative-is-segal extext A is-segal-A a a' a a
+  ( arr-inv-map-representable-equiv)
+  ( arr-map-representable-equiv)
+  ( id-hom A a)
+
+#def rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv
+  uses (A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a a' a
+      ( arr-inv-map-representable-equiv)
+      ( comp-is-segal A is-segal-A a' a a
+        ( arr-map-representable-equiv)
+        ( id-hom A a))
+  =_{ hom A a a}
+    inv-map-representable-equiv a
+    ( comp-is-segal A is-segal-A a' a a
+      ( arr-map-representable-equiv)
+      ( id-hom A a))
+  :=
+  rev
+  ( hom A a a)
+  ( inv-map-representable-equiv a
+    ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
+  ( comp-is-segal A is-segal-A a a' a
+    ( arr-inv-map-representable-equiv)
+    ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
+  ( eq-compute-precomposition-evid funext A is-segal-A a' a
+    ( inv-map-representable-equiv)
+    ( a)
+    ( comp-is-segal A is-segal-A a' a a
+      ( arr-map-representable-equiv)
+      ( id-hom A a)))
+
+#def rev-ap-inv-map-representable-equiv uses (A is-segal-A a a' ψ)
+  : inv-map-representable-equiv a
+    ( comp-is-segal A is-segal-A a' a a
+      ( arr-map-representable-equiv)
+      ( id-hom A a))
+  =_{ hom A a a}
+    inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))
+  :=
+  ap
+  ( hom A a' a)
+  ( hom A a a)
+  ( comp-is-segal A is-segal-A a' a a
+        ( arr-map-representable-equiv)
+        ( id-hom A a))
+  ( map-representable-equiv a (id-hom A a))
+  ( inv-map-representable-equiv a)
+  ( rev (hom A a' a)
+    ( map-representable-equiv a (id-hom A a))
+    ( comp-is-segal A is-segal-A a' a a
+        ( arr-map-representable-equiv)
+        ( id-hom A a))
+    ( eq-compute-precomposition-evid funext A is-segal-A a a'
+        ( map-representable-equiv)
+        ( a)
+        ( id-hom A a)))
+
+#def compute-htpy-inv-map-fib-equiv-map-fib-equiv-id
+  : inv-map-representable-equiv a (map-representable-equiv a (id-hom A a))
+  =_{ hom A a a}
+    id-hom A a
+  := htpy-inv-map-fib-equiv-map-fib-equiv-id a (id-hom A a)
+```
+
+Concatenate all the paths above.
+
+```rzk
+#def eq-comp-arrow-inv-map-arrow-map-equiv-id-a
+  uses (extext funext A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a a' a
+      arr-inv-map-representable-equiv
+      arr-map-representable-equiv
+  =_{ hom A a a}
+    id-hom A a
+  :=
+  quintuple-concat
+  ( hom A a a)
+  ( comp-is-segal A is-segal-A a a' a
+      arr-inv-map-representable-equiv
+      arr-map-representable-equiv)
+  ( comp-is-segal A is-segal-A a a a
+    ( comp-is-segal A is-segal-A a a' a
+        arr-inv-map-representable-equiv
+        arr-map-representable-equiv)
+    ( id-hom A a))
+  ( comp-is-segal A is-segal-A a a' a
+    ( arr-inv-map-representable-equiv)
+    ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
+  ( inv-map-representable-equiv a
+    ( comp-is-segal A is-segal-A a' a a arr-map-representable-equiv (id-hom A a)))
+  ( inv-map-representable-equiv a (map-representable-equiv a (id-hom A a)))
+  ( id-hom A a)
+  ( rev-comp-id-comp-arr-inv-map-arr-map-id-a)
+  ( assoc-is-segal-comp-comp-arr-inv-equiv-arr-map-idhom-a)
+  ( rev-eq-compute-precomposition-evid-arr-inv-map-representable-equiv)
+  ( rev-ap-inv-map-representable-equiv)
+  ( compute-htpy-inv-map-fib-equiv-map-fib-equiv-id)
+```
+
+Now we give the section of `#!rzk arrow-map-representable-equiv`.
+
+```rzk
+#def section-arrow-map-representable-equiv uses (extext funext A is-segal-A a a' ψ)
+  : Section-arrow A is-segal-A a' a arr-map-representable-equiv
+  :=
+  ( arr-inv-map-representable-equiv , eq-comp-arrow-inv-map-arrow-map-equiv-id-a)
+```
+
+We see that `#!rzk arrow-map-representable-equiv` has retraction
+`#!rzk arrow-inv-map-representable-equiv`.
+
+```rzk
+#def htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ)
+  : ( x : A)
+  → ( homotopy
+      ( hom A a' x)
+      ( hom A a' x)
+      ( comp
+        ( hom A a' x)
+        ( hom A a x)
+        ( hom A a' x)
+        ( map-representable-equiv x)
+        ( inv-map-representable-equiv x))
+      ( identity (hom A a' x)))
+  := \ x → second (second (inverse-representable-equiv x))
+```
+
+We compute the required paths for the retraction of
+`#!rzk arrow-map-iso-representable`.
+
+```rzk
+#def rev-eq-compute-precomposition-evid-map-representable-equiv
+  uses (A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a' a a'
+      arr-map-representable-equiv
+      arr-inv-map-representable-equiv
+  =_{ hom A a' a'}
+    map-representable-equiv a' arr-inv-map-representable-equiv
+  :=
+  rev
+  ( hom A a' a')
+  ( map-representable-equiv a' arr-inv-map-representable-equiv)
+  ( comp-is-segal A is-segal-A a' a a'
+      arr-map-representable-equiv
+      arr-inv-map-representable-equiv)
+  ( eq-compute-precomposition-evid funext A is-segal-A a a'
+      map-representable-equiv
+      a'
+      arr-inv-map-representable-equiv)
+
+#def rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map
+  uses (A is-segal-A a a' ψ)
+  : map-representable-equiv a' arr-inv-map-representable-equiv
+  =_{ hom A a' a'}
+    map-representable-equiv a'
+    ( comp-is-segal A is-segal-A a a' a'
+      ( arr-inv-map-representable-equiv)
+      ( id-hom A a'))
+  :=
+  ap
+  ( hom A a a')
+  ( hom A a' a')
+  ( arr-inv-map-representable-equiv)
+  ( comp-is-segal A is-segal-A a a' a'
+    ( arr-inv-map-representable-equiv)
+    ( id-hom A a'))
+  ( map-representable-equiv a')
+  ( rev
+    ( hom A a a')
+    ( comp-is-segal A is-segal-A a a' a'
+      ( arr-inv-map-representable-equiv)
+      ( id-hom A a'))
+    ( arr-inv-map-representable-equiv)
+    ( comp-id-is-segal A is-segal-A a a' arr-inv-map-representable-equiv))
+
+#def rev-ap-map-representable-equiv uses (A is-segal-A a a' ψ)
+  : map-representable-equiv a'
+    ( comp-is-segal A is-segal-A a a' a'
+      ( arr-inv-map-representable-equiv)
+      ( id-hom A a'))
+  =_{ hom A a' a'}
+    map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))
+  :=
+  ap
+  ( hom A a a')
+  ( hom A a' a')
+  ( comp-is-segal A is-segal-A a a' a'
+    ( arr-inv-map-representable-equiv)
+    ( id-hom A a'))
+  ( inv-map-representable-equiv a' (id-hom A a'))
+  ( map-representable-equiv a')
+  ( rev
+    ( hom A a a')
+    ( inv-map-representable-equiv a' (id-hom A a'))
+    ( comp-is-segal A is-segal-A a a' a'
+      ( arr-inv-map-representable-equiv)
+      ( id-hom A a'))
+    ( eq-compute-precomposition-evid funext A is-segal-A a' a
+      ( inv-map-representable-equiv)
+      ( a')
+      ( id-hom A a')))
+
+#def compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv uses (A a a' ψ)
+  : map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a'))
+  =_{ hom A a' a'}
+    id-hom A a'
+  := htpy-comp-map-fib-equiv-inv-map-fib-equiv a' (id-hom A a')
+```
+
+Concatenate all the paths above.
+
+```rzk
+#def eq-comp-arr-map-representable-arr-inv-map-representable-id-a'
+  uses (funext A is-segal-A a a' ψ)
+  : comp-is-segal A is-segal-A a' a a'
+      arr-map-representable-equiv
+      arr-inv-map-representable-equiv
+  =_{ hom A a' a'}
+    id-hom A a'
+  :=
+  quadruple-concat
+  ( hom A a' a')
+  ( comp-is-segal A is-segal-A a' a a'
+      arr-map-representable-equiv
+      arr-inv-map-representable-equiv)
+  ( map-representable-equiv a' arr-inv-map-representable-equiv)
+  ( map-representable-equiv a'
+    ( comp-is-segal A is-segal-A a a' a'
+      ( arr-inv-map-representable-equiv)
+      ( id-hom A a')))
+  ( map-representable-equiv a' (inv-map-representable-equiv a' (id-hom A a')))
+  ( id-hom A a')
+  ( rev-eq-compute-precomposition-evid-map-representable-equiv)
+  ( rev-ap-map-representable-equiv-eq-arr-inv-map-id-a'-arr-inv-map)
+  ( rev-ap-map-representable-equiv)
+  ( compute-htpy-comp-map-fib-equiv-inv-map-fib-equiv)
+```
+
+Now we give the retraction of `#!rzk arrow-map-representable-equiv`.
+
+```rzk
+#def retraction-arrow-map-representable-equiv uses (funext A is-segal-A a a' ψ)
+  : Retraction-arrow A is-segal-A a' a arr-map-representable-equiv
+  :=
+  ( arr-inv-map-representable-equiv
+  , eq-comp-arr-map-representable-arr-inv-map-representable-id-a')
+```
+
+We show that arrows from representable equivalences are isomorphisms, i.e. that
+`#!rzk arr-map-representable-equiv` is an isomorphism.
+
+```rzk title="RS17, Proposition 10.11 (i)"
+#def representable-isomorphism uses (extext funext A is-segal-A a a' ψ)
+  : is-iso-arrow A is-segal-A a' a arr-map-representable-equiv
+  :=
+  ( retraction-arrow-map-representable-equiv
+  , section-arrow-map-representable-equiv)
+
+#end representable-isomorphisms
+```
+
+The second part of Proposition 10.11.
+
+```rzk title="RS17, Proposition 10.11 (ii)"
+#def eq-representable-isomorphism uses (extext funext)
+  ( A : U)
+  ( is-rezk-A : is-rezk A)
+  ( a a' : A)
+  ( ψ : (x : A) → (Equiv (hom A a x) (hom A a' x)))
+  : a' = a
+  :=
+  eq-iso-is-rezk A is-rezk-A a' a
+  ( arr-map-representable-equiv A a a' ψ
+  , representable-isomorphism A (first is-rezk-A) a a' ψ)
+```