Use #assume and use for FunExt and ExtExt

src/hott/03-equivalences.rzk.md

@@ -384,28 +384,38 @@ equivalences.
     ( f : (x : X) -> A x) ->
     ( g : (x : X) -> A x) ->
     is-equiv (f = g) ((x : X) -> f x = g x) (htpy-eq X A f g)
+```
+
+In the formalisations below, some definitions will assume function
+extensionality:
 
+```rzk
+#assume funext : FunExt
+```
+
+Whenever a definition (implicitly) uses function extensionality, we write
+`uses (funext)`. In particular, the following definitions rely on function
+extensionality:
+
+```rzk
 -- The equivalence provided by function extensionality.
-#def FunExt-equiv
-  ( funext : FunExt)
+#def FunExt-equiv uses (funext)
   ( X : U)
   ( A : X -> U)
   ( f g : (x : X) -> A x)
   : Equiv (f = g) ((x : X) -> f x = g x)
   := (htpy-eq X A f g , funext X A f g)
 
 -- In particular, function extensionality implies that homotopies give rise to identifications. This defines eq-htpy to be the retraction to htpy-eq.
-#def eq-htpy
-  ( funext : FunExt)
+#def eq-htpy uses (funext)
   ( X : U)
   ( A : X -> U)
   ( f g : (x : X) -> A x)
   : ((x : X) -> f x = g x) -> (f = g)
   := first (first (funext X A f g))
 
 -- Using function extensionality, a fiberwise equivalence defines an equivalence of dependent function types
-#def equiv-function-equiv-fibered
-  ( funext : FunExt)
+#def equiv-function-equiv-fibered uses (funext)
   ( X : U)
   ( A B : X -> U)
   ( fibequiv : (x : X) -> Equiv (A x) (B x))
@@ -415,7 +425,7 @@ equivalences.
       ( ( ( \ b x -> (first (first (second (fibequiv x)))) (b x)) ,
           ( \ a ->
             eq-htpy
-              funext X A
+              X A
               ( \ x ->
                 (first (first (second (fibequiv x))))
                   ((first (fibequiv x)) (a x)))
@@ -424,7 +434,7 @@ equivalences.
         ( ( \ b x -> (first (second (second (fibequiv x)))) (b x)) ,
           ( \ b ->
             eq-htpy
-              funext X B
+              X B
               ( \ x ->
                 (first (fibequiv x))
                   ((first (second (second (fibequiv x)))) (b x)))

src/simplicial-hott/04-extension-types.rzk.md

@@ -239,9 +239,10 @@ footnote 8, we assert this as an "extension extensionality" axiom
       ( (t : ψ) -> (f t = g t) [ ϕ t |-> refl ])
       ( ext-htpy-eq I ψ ϕ A a f g)
 
+#assume extext : ExtExt
+
 -- The equivalence provided by extension extensionality.
-#def equiv-ExtExt
-  ( extext : ExtExt)
+#def equiv-ExtExt uses (extext)
   ( I : CUBE)
   ( ψ : I -> TOPE)
   ( ϕ : ψ -> TOPE)
@@ -257,8 +258,7 @@ identifications. This definition defines `eq-ext-htpy` to be the retraction to
 `ext-htpy-eq`.
 
 ```rzk
-#def eq-ext-htpy
-  ( extext : ExtExt)
+#def eq-ext-htpy uses (extext)
   ( I : CUBE)
   ( ψ : I -> TOPE)
   ( ϕ : ψ -> TOPE)
@@ -275,8 +275,7 @@ equivalences of extension types.
 ```rzk
 -- A fiberwise equivalence defines an equivalence of extension types, for
 -- simplicity extending from BOT
-#def equiv-extension-equiv-fibered
-  ( extext : ExtExt)
+#def equiv-extension-equiv-fibered uses (extext)
   ( I : CUBE)
   ( ψ : I -> TOPE)
   ( A B : ψ -> U)
@@ -287,7 +286,6 @@ equivalences of extension types.
       ( ( ( \ b t -> (first (first (second (fibequiv t)))) (b t)) ,
           ( \ a ->
             eq-ext-htpy
-              ( extext)
               ( I)
               ( ψ)
               ( \ t -> BOT)
@@ -300,7 +298,6 @@ equivalences of extension types.
         ( ( \ b t -> first (second (second (fibequiv t))) (b t)) ,
           ( \ b ->
             eq-ext-htpy
-              ( extext)
               ( I)
               ( ψ)
               ( \ t -> BOT)

src/simplicial-hott/05-segal-types.rzk.md

@@ -20,6 +20,14 @@ This is a literate `rzk` file:
 - `4-extension-types.md` — We use the fubini theorem and extension
   extensionality.
 
+Some of the definitions in this file rely on function extensionality and
+extension extensionality:
+
+```rzk
+#assume funext : FunExt
+#assume extext : ExtExt
+```
+
 ## Hom types
 
 Extension types are used ∂to define the type of arrows between fixed terms:
@@ -369,8 +377,7 @@ instance if $X$ is a type and $A : X → U$ is such that $A x$ is a Segal type f
 all $x$ then $(x : X) → A x$ is a Segal type.
 
 ```rzk title="RS17, Corollary 5.6(i)"
-#def Segal-function-types
-  (funext : FunExt)
+#def Segal-function-types uses (funext)
   (X : U)
   (A : (_ : X) -> U)
   (fiberwise-is-segal-A : (x : X) -> is-local-horn-inclusion (A x))
@@ -410,8 +417,7 @@ If $X$ is a shape and $A : X → U$ is such that $A x$ is a Segal type for all $
 then $(x : X) → A x$ is a Segal type.
 
 ```rzk title="RS17, Corollary 5.6(ii)"
-#def Segal-extension-types
-  (extext : ExtExt)
+#def Segal-extension-types uses (extext)
   (I : CUBE)
   (ψ : (s : I) -> TOPE)
   (A : (s : ψ) -> U )
@@ -474,29 +480,25 @@ For later use, an equivalent characterization of the arrow type.
 
 ```rzk title="RS17, Corollary 5.6(ii)"
 -- special case using `is-local-horn-inclusion`
-#def Segal'-arrow-types
-  (extext : ExtExt)
+#def Segal'-arrow-types uses (extext)
   (A : U)
   (is-segal-A : is-local-horn-inclusion A)
   : is-local-horn-inclusion (arr A)
   :=
     Segal-extension-types
-      ( extext)
       ( 2)
       ( Δ¹)
       ( \ t -> A)
       ( \ t -> is-segal-A)
 
 -- special case using `is-segal`
-#def Segal-arrow-types
-  (extext : ExtExt)
+#def Segal-arrow-types uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   : is-segal (arr A)
   :=
     is-segal-is-local-horn-inclusion (arr A)
       ( Segal-extension-types
-          ( extext)
           ( 2)
           ( Δ¹)
           ( \ t -> A)
@@ -728,8 +730,7 @@ The `Segal-comp-witness-square` as an arrow in the arrow type:
 </svg>
 
 ```rzk
-#def Segal-associativity-witness
-  (extext : ExtExt)
+#def Segal-associativity-witness uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -739,14 +740,14 @@ The `Segal-comp-witness-square` as an arrow in the arrow type:
   : hom2 (arr A) f g h
       (Segal-arr-in-arr A is-segal-A w x y f g)
       (Segal-arr-in-arr A is-segal-A x y z g h)
-      (Segal-comp (arr A) (Segal-arrow-types extext A is-segal-A)
+      (Segal-comp (arr A) (Segal-arrow-types A is-segal-A)
       f g h
       (Segal-arr-in-arr A is-segal-A w x y f g)
       (Segal-arr-in-arr A is-segal-A x y z g h))
   :=
     Segal-comp-witness
       ( arr A)
-      ( Segal-arrow-types extext A is-segal-A)
+      ( Segal-arrow-types A is-segal-A)
       f g h
       ( Segal-arr-in-arr A is-segal-A w x y f g)
       ( Segal-arr-in-arr A is-segal-A x y z g h)
@@ -775,8 +776,7 @@ The `Segal-associativity-witness` curries to define a diagram $Δ²×Δ¹ → A$
 $((t , s) , r) ↦ ((t , r) , s)$ from $Δ³$ to $Δ²×Δ¹$.
 
 ```rzk
-#def Segal-associativity-tetrahedron
-  (extext : ExtExt)
+#def Segal-associativity-tetrahedron uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -786,7 +786,7 @@ $((t , s) , r) ↦ ((t , r) , s)$ from $Δ³$ to $Δ²×Δ¹$.
   : Δ³ -> A
   :=
     \ ((t , s) , r) ->
-    (Segal-associativity-witness extext A is-segal-A w x y z f g h) (t , r) s
+    (Segal-associativity-witness A is-segal-A w x y z f g h) (t , r) s
 ```
 
 <svg style="float: right" viewBox="0 0 200 250" width="150" height="200">
@@ -811,8 +811,7 @@ The diagonal composite of three arrows extracted from the
 `Segal-associativity-tetrahedron`.
 
 ```rzk
-#def Segal-triple-composite
-  (extext : ExtExt)
+#def Segal-triple-composite uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -822,7 +821,7 @@ The diagonal composite of three arrows extracted from the
   : hom A w z
   :=
     \ t ->
-    ( Segal-associativity-tetrahedron extext A is-segal-A w x y z f g h)
+    ( Segal-associativity-tetrahedron A is-segal-A w x y z f g h)
       ( (t , t) , t)
 ```
 
@@ -847,8 +846,7 @@ The diagonal composite of three arrows extracted from the
 </svg>
 
 ```rzk
-#def Segal-left-associativity-witness
-  (extext : ExtExt)
+#def Segal-left-associativity-witness uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -858,10 +856,10 @@ The diagonal composite of three arrows extracted from the
   : hom2 A w y z
     (Segal-comp A is-segal-A w x y f g)
     h
-    (Segal-triple-composite extext A is-segal-A w x y z f g h)
+    (Segal-triple-composite A is-segal-A w x y z f g h)
   :=
     \ (t , s) ->
-    ( Segal-associativity-tetrahedron extext A is-segal-A w x y z f g h)
+    ( Segal-associativity-tetrahedron A is-segal-A w x y z f g h)
       ( (t , t) , s)
 ```
 
@@ -888,8 +886,7 @@ The front face:
 </svg>
 
 ```rzk
-#def Segal-right-associativity-witness
-  (extext : ExtExt)
+#def Segal-right-associativity-witness uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -899,47 +896,44 @@ The front face:
   : hom2 A w x z
     f
     (Segal-comp A is-segal-A x y z g h)
-    (Segal-triple-composite extext A is-segal-A w x y z f g h)
+    (Segal-triple-composite A is-segal-A w x y z f g h)
   :=
     \ (t , s) ->
-    ( Segal-associativity-tetrahedron extext A is-segal-A w x y z f g h)
+    ( Segal-associativity-tetrahedron A is-segal-A w x y z f g h)
       ((t , s) , s)
 ```
 
 ```rzk
-#def Segal-left-associativity
-  (extext : ExtExt)
+#def Segal-left-associativity uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
   (f : hom A w x)
   (g : hom A x y)
   (h : hom A y z)
   : (Segal-comp A is-segal-A w y z (Segal-comp A is-segal-A w x y f g) h) =
-    (Segal-triple-composite extext A is-segal-A w x y z f g h)
+    (Segal-triple-composite A is-segal-A w x y z f g h)
   :=
     Segal-comp-uniqueness
       A is-segal-A w y z (Segal-comp A is-segal-A w x y f g) h
-      ( Segal-triple-composite extext A is-segal-A w x y z f g h)
-      ( Segal-left-associativity-witness extext A is-segal-A w x y z f g h)
+      ( Segal-triple-composite A is-segal-A w x y z f g h)
+      ( Segal-left-associativity-witness A is-segal-A w x y z f g h)
 
-#def Segal-right-associativity
-  (extext : ExtExt)
+#def Segal-right-associativity uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
   (f : hom A w x)
   (g : hom A x y)
   (h : hom A y z)
   : (Segal-comp A is-segal-A w x z f (Segal-comp A is-segal-A x y z g h)) =
-      (Segal-triple-composite extext A is-segal-A w x y z f g h)
+      (Segal-triple-composite A is-segal-A w x y z f g h)
   := Segal-comp-uniqueness
         A is-segal-A w x z f (Segal-comp A is-segal-A x y z g h)
-      ( Segal-triple-composite extext A is-segal-A w x y z f g h)
-      ( Segal-right-associativity-witness extext A is-segal-A w x y z f g h)
+      ( Segal-triple-composite A is-segal-A w x y z f g h)
+      ( Segal-right-associativity-witness A is-segal-A w x y z f g h)
 
-#def Segal-associativity
-  (extext : ExtExt)
+#def Segal-associativity uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (w x y z : A)
@@ -952,10 +946,10 @@ The front face:
     zig-zag-concat
     ( hom A w z)
     ( Segal-comp A is-segal-A w y z (Segal-comp A is-segal-A w x y f g) h)
-    ( Segal-triple-composite extext A is-segal-A w x y z f g h)
+    ( Segal-triple-composite A is-segal-A w x y z f g h)
     ( Segal-comp A is-segal-A w x z f (Segal-comp A is-segal-A x y z g h))
-    ( Segal-left-associativity extext A is-segal-A w x y z f g h)
-    ( Segal-right-associativity extext A is-segal-A w x y z f g h)
+    ( Segal-left-associativity A is-segal-A w x y z f g h)
+    ( Segal-right-associativity A is-segal-A w x y z f g h)
 
 
 #def Segal-postcomp
@@ -1261,8 +1255,6 @@ composition:
 
 #section is-segal-Unit
 
-#variable extext : ExtExt
-
 #def iscontr-Unit : is-contr Unit := (unit , \ _ -> refl)
 
 #def is-contr-Δ²→Unit uses (extext)

src/simplicial-hott/06-2cat-of-segal-types.rzk.md

@@ -15,6 +15,12 @@ This is a literate `rzk` file:
 - `4-extension-types.md` — We use extension extensionality.
 - `5-segal-types.md` - We use the notion of hom types.
 
+Some of the definitions in this file rely on extension extensionality:
+
+```rzk
+#assume extext : ExtExt
+```
+
 ## Functors
 
 Functions between types induce an action on hom types , preserving sources and
@@ -47,8 +53,7 @@ Functions between types automatically preserve identity arrows.
 
 ```rzk title="RS17, Proposition 6.1.a"
 -- Preservation of identities follows from extension extensionality because these arrows are pointwise equal.
-#def functors-pres-id
-  (extext : ExtExt)
+#def functors-pres-id uses (extext)
   (A B : U)
   (F : A -> B)
   (x : A)