From dcbc0fd019442326777cb0fc1afdedf4afe2f691 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@w199-8-v4.eduroam.dynamic.rbg.tum.de>
Date: Fri, 13 Oct 2023 17:06:47 +0200
Subject: [PATCH 1/3] towards more section-retraction stuff

---
 src/hott/03-equivalences.rzk.md | 33 ++++++++++++++++++++++++++-------
 1 file changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 56aaf0db..752249aa 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -539,25 +539,44 @@ A pair of maps `s : A' → B` and `r : B → A` is a section-retraction pair if
 composite `A' → A` is an equivalence.
 
 ```rzk
-#section is-section-retraction-pair
-
-#variables A' B A : U
-#variable s : A' → B
-#variable r : B → A
 
 
 #def is-section-retraction-pair
+  ( A' B A : U)
+  ( s : A' → B)
+  ( r : B → A)
   : U
   := is-equiv A' A (comp A' B A r s)
 ```
 
+We say that `s : A' → B` has a weak retraction if it can be completed to a
+section retraction pair.
+Note that like `has-section`, this is not a property but structure.
+
+```rzk
+#def has-weak-retraction
+  ( A' B : U)
+  ( s : A' → B)
+  : U
+  :=
+    Σ ( Σ (A : U) , r : B → A)
+    , ( is-section-retraction-pair A' B A s r)
+```
+
+
 In a section-retraction pair, if one of `s : A' → B` and `r : B → A` is an
 equivalence, then so is the other.
 
 This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`.
 
 ```rzk
-#variable is-sec-rec-pair : is-section-retraction-pair
+#section is-equiv-is-section-retraction-pair
+
+#variables A' B A : U
+#variable s : A' → B
+#variable r : B → A
+
+#variable is-sec-rec-pair : is-section-retraction-pair A' B A s r
 
 #def is-equiv-section-is-equiv-retraction-is-section-retraction-pair
   ( is-equiv-r : is-equiv B A r)
@@ -574,7 +593,7 @@ This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`.
     ( s) ( is-equiv-s)
     ( r) ( is-sec-rec-pair)
 
-#end is-section-retraction-pair
+#end is-equiv-is-section-retraction-pair
 ```
 
 ## Function extensionality

From 40593bdf8c9f73d2d3ed9df905008407380515e7 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@w199-8-v4.eduroam.dynamic.rbg.tum.de>
Date: Fri, 13 Oct 2023 20:23:55 +0200
Subject: [PATCH 2/3] internalize-externalize

---
 src/hott/03-equivalences.rzk.md | 172 ++++++++++++++++++++++++++------
 src/hott/06-contractible.rzk.md |  53 ++++------
 2 files changed, 166 insertions(+), 59 deletions(-)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index bac95b8f..6d98ce26 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -535,67 +535,183 @@ The retraction associated with an equivalence is an equivalence.
 
 ## Section-retraction pairs
 
-A pair of maps `s : A' → B` and `r : B → A` is a **section-retraction pair** if
-the composite `A' → A` is an equivalence.
+A pair of maps `s : A → B` and `r : B → A'` is a
+**section-retraction pair** if the composite `A → A'` is an equivalence.
 
 ```rzk
-
-
 #def is-section-retraction-pair
-  ( A' B A : U)
-  ( s : A' → B)
-  ( r : B → A)
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
   : U
-  := is-equiv A' A (comp A' B A r s)
+  := is-equiv A A' (comp A B A' r s)
 ```
 
-We say that `s : A' → B` has a weak retraction if it can be completed to a
-section retraction pair.
-Note that like `has-section`, this is not a property but structure.
+When we have such a section-retraction pair `(s, r)`,
+we say that `r` is an **external retraction** of `s`
+and `s` is an **external section** of `r`.
 
 ```rzk
-#def has-weak-retraction
-  ( A' B : U)
-  ( s : A' → B)
+#def has-external-retraction
+  ( A B : U)
+  ( s : A → B)
   : U
   :=
-    Σ ( Σ (A : U) , r : B → A)
-    , ( is-section-retraction-pair A' B A s r)
+    Σ ((A', r) : ( Σ (A' : U) , B → A'))
+    , ( is-section-retraction-pair A B A' s r)
+
+#def has-external-section
+  ( B A' : U)
+  ( r : B → A')
+  : U
+  :=
+    Σ ((A, s) : ( Σ (A : U) , A → B))
+    , ( is-section-retraction-pair A B A' s r)
 ```
 
+Note that exactly like `has-section` and `has-retraction`
+these are not _properties_ of `s` or `r`, but structure.
+
+Without univalence, we cannot yet show that the types
+`has-external-retraction` and `has-retraction`
+(and their section counterparts, respectively)
+are equivalent, so we content ourselves in showing that there is a
+logical biimplication between them.
+
+```rzk
+#def has-retraction-externalize
+  ( A B : U)
+  ( s : A → B)
+  ( (r , η) : has-retraction A B s)
+  : has-external-retraction A B s
+  :=
+    ( ( A , r)
+    , is-equiv-homotopy A A (\ a → r (s (a))) (identity A)
+      ( η) ( is-equiv-identity A))
+
+#def has-section-externalize
+  ( B A' : U)
+  ( r : B → A')
+  ( (s , ε) : has-section B A' r)
+  : has-external-section B A' r
+  :=
+    ( ( A' , s)
+    , is-equiv-homotopy A' A' (\ a' → r (s (a'))) (identity A')
+      ( ε) ( is-equiv-identity A'))
 
-In a section-retraction pair, if one of `s : A' → B` and `r : B → A` is an
+#def has-retraction-internalize
+  ( A B : U)
+  ( s : A → B)
+  ( ((A' , r) , ( (rec-rs , η-rs) , _))
+    : has-external-retraction A B s)
+  : has-retraction A B s
+  := ( comp B A' A rec-rs r , η-rs)
+
+#def has-section-internalize
+  ( B A' : U)
+  ( r : B → A')
+  ( ((A , s) , (_ , (sec-rs , ε-rs)))
+    : has-external-section B A' r)
+  : has-section B A' r
+  := ( comp A' A B s sec-rs , ε-rs)
+```
+
+A consequence of the above is that in a section-retraction pair `(s, r)`,
+the map `s` is a section and the map `r` is a retraction.
+Note that not every composable pair `(s, r)` of such maps is a
+section-retraction pair;
+they have to (up to composition with an equivalence)
+be section and retraction _of each other_.
+
+In a section-retraction pair, if one of `s : A → B` and `r : B → A'` is an
 equivalence, then so is the other.
 
-This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`.
+This is just a rephrasing of `is-equiv-left-factor`
+and `is-equiv-right-factor`.
 
 ```rzk
 #section is-equiv-is-section-retraction-pair
 
-#variables A' B A : U
-#variable s : A' → B
-#variable r : B → A
+#variables A B A' : U
+#variable s : A → B
+#variable r : B → A'
 
-#variable is-sec-rec-pair : is-section-retraction-pair A' B A s r
+#variable is-sec-rec-pair : is-section-retraction-pair A B A' s r
 
 #def is-equiv-section-is-equiv-retraction-is-section-retraction-pair
-  ( is-equiv-r : is-equiv B A r)
-  : is-equiv A' B s
+  ( is-equiv-r : is-equiv B A' r)
+  : is-equiv A B s
   :=
-    is-equiv-right-factor A' B A s r
+    is-equiv-right-factor A B A' s r
     ( is-equiv-r) ( is-sec-rec-pair)
 
 #def is-equiv-retraction-is-equiv-section-is-section-retraction-pair
-  ( is-equiv-s : is-equiv A' B s)
-  : is-equiv B A r
+  ( is-equiv-s : is-equiv A B s)
+  : is-equiv B A' r
   :=
-    is-equiv-left-factor A' B A
+    is-equiv-left-factor A B A'
     ( s) ( is-equiv-s)
     ( r) ( is-sec-rec-pair)
 
 #end is-equiv-is-section-retraction-pair
 ```
 
+## Retracts
+
+We say that a type `A` is a retract of a type `B` if we have a map
+`s : A → B` which has a retraction.
+
+```rzk title="The type of proofs that A is a retract of B"
+#def is-retract-of
+  ( A B : U)
+  : U
+  := Σ ( s : A → B) , has-retraction A B s
+
+#def section-is-retract-of
+  ( A B : U)
+  ( (s , (_ , _)) : is-retract-of A B)
+  : A → B
+  := s
+
+#def retraction-is-retract-of
+  ( A B : U)
+  ( (_ , (r , _)) : is-retract-of A B)
+  : B → A
+  := r
+
+#def homotopy-is-retract-of
+  ( A B : U)
+  ( (s , (r , η)) : is-retract-of A B)
+  : homotopy A A ( \ a → r ( s a)) ( identity A)
+  := η
+```
+
+Section-retraction pairs `A → B → A'` are a convenient way to exhibit
+both `A` and `A'` as retracts of `B`.
+
+```rzk
+#def is-retract-of-left-section-retraction-pair
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
+  ( is-sr-pair-sr : is-section-retraction-pair A B A' s r)
+  : is-retract-of A B
+  :=
+    ( ( s)
+    , ( has-retraction-internalize A B s ((A' , r) , is-sr-pair-sr)))
+
+#def is-retract-of-right-section-retraction-pair
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
+  ( is-sr-pair-sr : is-section-retraction-pair A B A' s r)
+  : is-retract-of A' B
+  :=
+    ( first ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr))
+    , ( r
+      , second ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr))))
+```
+
 ## Function extensionality
 
 By path induction, an identification between functions defines a homotopy.
diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 640c9eef..731bba54 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -175,39 +175,23 @@ A type is contractible if and only if its terminal map is an equivalence.
 
 A retract of contractible types is contractible.
 
-```rzk title="The type of proofs that A is a retract of B"
-#def is-retract-of
-  ( A B : U)
-  : U
-  := Σ ( s : A → B) , has-retraction A B s
 
-#section retraction-data
+```rzk title="If A is a retract of a contractible type it has a term"
+#section is-contr-is-retract-of-is-contr
 
 #variables A B : U
-#variable is-retract-of-A-B : is-retract-of A B
-
-#def section-is-retract-of
-  : A → B
-  := first is-retract-of-A-B
-
-#def retraction-is-retract-of
-  : B → A
-  := first (second is-retract-of-A-B)
+#variable is-retr-of-A-B : is-retract-of A B
 
-#def homotopy-is-retract-of
-  : homotopy A A (comp A B A retraction-is-retract-of section-is-retract-of) (identity A)
-  := second (second is-retract-of-A-B)
-```
-
-```rzk title="If A is a retract of a contractible type it has a term"
-#def is-inhabited-is-contr-is-retract-of uses (is-retract-of-A-B)
+#def is-inhabited-is-contr-is-retract-of uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   : A
-  := retraction-is-retract-of (center-contraction B is-contr-B)
+  :=
+    retraction-is-retract-of A B is-retr-of-A-B
+    ( center-contraction B is-contr-B)
 ```
 
 ```rzk title="If A is a retract of a contractible type it has a contracting homotopy"
-#def has-homotopy-is-contr-is-retract-of uses (is-retract-of-A-B)
+#def has-homotopy-is-contr-is-retract-of uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   ( a : A)
   : ( is-inhabited-is-contr-is-retract-of is-contr-B) = a
@@ -215,25 +199,32 @@ A retract of contractible types is contractible.
     concat
       ( A)
       ( is-inhabited-is-contr-is-retract-of is-contr-B)
-      ( (comp A B A retraction-is-retract-of section-is-retract-of) a)
+      ( comp A B A
+        ( retraction-is-retract-of A B is-retr-of-A-B)
+        ( section-is-retract-of A B is-retr-of-A-B)
+        ( a))
       ( a)
-      ( ap B A (center-contraction B is-contr-B) (section-is-retract-of a)
-        ( retraction-is-retract-of)
-        ( homotopy-contraction B is-contr-B (section-is-retract-of a)))
-      ( homotopy-is-retract-of a)
+      ( ap B A
+        ( center-contraction B is-contr-B)
+        ( section-is-retract-of A B is-retr-of-A-B a)
+        ( retraction-is-retract-of A B is-retr-of-A-B)
+        ( homotopy-contraction B is-contr-B
+          ( section-is-retract-of A B is-retr-of-A-B a)))
+      ( homotopy-is-retract-of A B is-retr-of-A-B a)
 ```
 
 ```rzk title="If A is a retract of a contractible type it is contractible"
-#def is-contr-is-retract-of-is-contr uses (is-retract-of-A-B)
+#def is-contr-is-retract-of-is-contr uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   : is-contr A
   :=
     ( is-inhabited-is-contr-is-retract-of is-contr-B ,
       has-homotopy-is-contr-is-retract-of is-contr-B)
+
+#end is-contr-is-retract-of-is-contr
 ```
 
 ```rzk
-#end retraction-data
 ```
 
 ## Functions between contractible types

From f642f440e4c385f8ceb422926ece30c1207f3802 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@w199-8-v4.eduroam.dynamic.rbg.tum.de>
Date: Fri, 13 Oct 2023 20:25:21 +0200
Subject: [PATCH 3/3] autoformat

---
 src/hott/03-equivalences.rzk.md | 44 +++++++++++++++------------------
 src/hott/06-contractible.rzk.md |  2 +-
 2 files changed, 21 insertions(+), 25 deletions(-)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 6d98ce26..cadb5c65 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -535,8 +535,8 @@ The retraction associated with an equivalence is an equivalence.
 
 ## Section-retraction pairs
 
-A pair of maps `s : A → B` and `r : B → A'` is a
-**section-retraction pair** if the composite `A → A'` is an equivalence.
+A pair of maps `s : A → B` and `r : B → A'` is a **section-retraction pair** if
+the composite `A → A'` is an equivalence.
 
 ```rzk
 #def is-section-retraction-pair
@@ -547,9 +547,8 @@ A pair of maps `s : A → B` and `r : B → A'` is a
   := is-equiv A A' (comp A B A' r s)
 ```
 
-When we have such a section-retraction pair `(s, r)`,
-we say that `r` is an **external retraction** of `s`
-and `s` is an **external section** of `r`.
+When we have such a section-retraction pair `(s, r)`, we say that `r` is an
+**external retraction** of `s` and `s` is an **external section** of `r`.
 
 ```rzk
 #def has-external-retraction
@@ -569,14 +568,13 @@ and `s` is an **external section** of `r`.
     , ( is-section-retraction-pair A B A' s r)
 ```
 
-Note that exactly like `has-section` and `has-retraction`
-these are not _properties_ of `s` or `r`, but structure.
+Note that exactly like `has-section` and `has-retraction` these are not
+_properties_ of `s` or `r`, but structure.
 
-Without univalence, we cannot yet show that the types
-`has-external-retraction` and `has-retraction`
-(and their section counterparts, respectively)
-are equivalent, so we content ourselves in showing that there is a
-logical biimplication between them.
+Without univalence, we cannot yet show that the types `has-external-retraction`
+and `has-retraction` (and their section counterparts, respectively) are
+equivalent, so we content ourselves in showing that there is a logical
+biimplication between them.
 
 ```rzk
 #def has-retraction-externalize
@@ -616,18 +614,16 @@ logical biimplication between them.
   := ( comp A' A B s sec-rs , ε-rs)
 ```
 
-A consequence of the above is that in a section-retraction pair `(s, r)`,
-the map `s` is a section and the map `r` is a retraction.
-Note that not every composable pair `(s, r)` of such maps is a
-section-retraction pair;
-they have to (up to composition with an equivalence)
-be section and retraction _of each other_.
+A consequence of the above is that in a section-retraction pair `(s, r)`, the
+map `s` is a section and the map `r` is a retraction. Note that not every
+composable pair `(s, r)` of such maps is a section-retraction pair; they have to
+(up to composition with an equivalence) be section and retraction _of each
+other_.
 
 In a section-retraction pair, if one of `s : A → B` and `r : B → A'` is an
 equivalence, then so is the other.
 
-This is just a rephrasing of `is-equiv-left-factor`
-and `is-equiv-right-factor`.
+This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`.
 
 ```rzk
 #section is-equiv-is-section-retraction-pair
@@ -658,8 +654,8 @@ and `is-equiv-right-factor`.
 
 ## Retracts
 
-We say that a type `A` is a retract of a type `B` if we have a map
-`s : A → B` which has a retraction.
+We say that a type `A` is a retract of a type `B` if we have a map `s : A → B`
+which has a retraction.
 
 ```rzk title="The type of proofs that A is a retract of B"
 #def is-retract-of
@@ -686,8 +682,8 @@ We say that a type `A` is a retract of a type `B` if we have a map
   := η
 ```
 
-Section-retraction pairs `A → B → A'` are a convenient way to exhibit
-both `A` and `A'` as retracts of `B`.
+Section-retraction pairs `A → B → A'` are a convenient way to exhibit both `A`
+and `A'` as retracts of `B`.
 
 ```rzk
 #def is-retract-of-left-section-retraction-pair
diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 731bba54..42f890a1 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -175,7 +175,6 @@ A type is contractible if and only if its terminal map is an equivalence.
 
 A retract of contractible types is contractible.
 
-
 ```rzk title="If A is a retract of a contractible type it has a term"
 #section is-contr-is-retract-of-is-contr
 
@@ -225,6 +224,7 @@ A retract of contractible types is contractible.
 ```
 
 ```rzk
+
 ```
 
 ## Functions between contractible types