diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 39a51c3..731cdb4 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -384,10 +384,22 @@ 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)
@@ -395,8 +407,7 @@ equivalences.
   := (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)
@@ -404,8 +415,7 @@ equivalences.
   := 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)))
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 4165ee0..dd82ae7 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -102,17 +102,17 @@ This is a literate `rzk` file:
   ( X : ψ -> ζ -> U)
   ( f : { (t , s) : I * J | (ϕ t /\ ζ s) \/ (ψ t /\ χ s)} -> X t s )
   : Equiv
-    ( {t : I | ψ t} -> ({ s : J | ζ s} -> X t s [ χ s |-> f (t , s) ])
+    ( {t : ψ} -> ({s : ζ} -> X t s [ χ s |-> f (t , s) ])
         [ ϕ t |-> \ s -> f (t , s) ])
-    ( {s : J | ζ s} -> ({ t : I | ψ t} -> X t s [ ϕ t |-> f (t , s) ])
+    ( {s : ζ} -> ({t : ψ} -> X t s [ ϕ t |-> f (t , s) ])
         [ χ s |-> \ t -> f (t , s) ])
   :=
     comp-equiv
-      ( {t : I | ψ t} -> ({ s : J | ζ s} -> X t s [ χ s |-> f (t , s) ])
+      ( {t : ψ} -> ({s : ζ} -> X t s [ χ s |-> f (t , s) ])
         [ ϕ t |-> \ s -> f (t , s) ])
       ( { (t , s) : I * J | ψ t /\ ζ s} -> X t s
         [(ϕ t /\ ζ s) \/ (ψ t /\ χ s) |-> f (t , s)])
-      ( {s : J | ζ s} -> ({ t : I | ψ t} -> X t s [ ϕ t |-> f (t , s) ])
+      ( {s : ζ} -> ({t : ψ} -> X t s [ ϕ t |-> f (t , s) ])
         [ χ s |-> \ t -> f (t , s) ])
       ( curry-uncurry I J ψ ϕ ζ χ X f)
       ( uncurry-opcurry I J ψ ϕ ζ χ X f)
@@ -130,7 +130,7 @@ This is a literate `rzk` file:
   ( a : (t : ϕ) -> X t)
   ( b : (t : ϕ) -> Y t (a t))
   : Equiv
-    ( {t : I | ψ t} -> (Σ (x : X t) , Y t x) [ ϕ t |-> (a t , b t) ])
+    ( {t : ψ} -> (Σ (x : X t) , Y t x) [ ϕ t |-> (a t , b t) ])
     ( Σ ( f : ((t : ψ) -> X t [ ϕ t |-> a t ])) ,
         ( (t : ψ) -> Y t (f t) [ ϕ t |-> b t ]))
     :=
@@ -157,8 +157,8 @@ This is a literate `rzk` file:
           ( (t : χ) -> X t [ χ t /\ ψ t |-> f t ]))
   :=
     ( \ h -> (\ t -> h t , \ t -> h t) ,
-      ( ( \ fg t -> (second fg) t , \ h -> refl) ,
-        ( \ fg t -> (second fg) t , \ h -> refl)))
+      ( ( \ (_f, g) t -> g t , \ h -> refl) ,
+        ( \ (_f, g) t -> g t , \ h -> refl)))
 ```
 
 ```rzk title="RS17, Theorem 4.4"
@@ -176,8 +176,8 @@ This is a literate `rzk` file:
         ( (t : χ) -> X t [ ψ t |-> f t ]))
   :=
     ( \ h -> (\ t -> h t , \ t -> h t) ,
-      ( ( \ fg t -> (second fg) t , \ h -> refl) ,
-        ( ( \ fg t -> (second fg) t , \ h -> refl))))
+      ( ( \ (_f, g) t -> g t , \ h -> refl) ,
+        ( ( \ (_f, g) t -> g t , \ h -> refl))))
 ```
 
 ```rzk title="RS17, Theorem 4.5"
@@ -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)
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 8c8169b..fde8707 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/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,16 +896,15 @@ 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)
@@ -916,15 +912,14 @@ The front face:
   (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)
@@ -932,14 +927,13 @@ The front face:
   (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)
diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
index 92ab6b8..92b9b75 100644
--- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
+++ b/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)
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index d466cbc..856f23a 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -17,6 +17,14 @@ 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 function extensionality and
+extension extensionality:
+
+```rzk
+#assume funext : FunExt
+#assume extext : ExtExt
+```
+
 ## The definition
 
 Discrete types are types in which the hom-types are canonically equivalent to
@@ -42,8 +50,7 @@ By function extensionality, the dependent function type associated to a family
 of discrete types is discrete.
 
 ```rzk
-#def equiv-discrete-family
-  ( funext : FunExt)
+#def equiv-discrete-family uses (funext)
   ( X : U)
   ( A : X -> U)
   ( is-discrete-A : (x : X) -> is-discrete (A x))
@@ -67,30 +74,28 @@ of discrete types is discrete.
         ( \ t x -> A x)
         ( \ t x -> recOR (t === 0_2 |-> f x , t === 1_2 |-> g x)))
 
-#def equiv-discrete-family-map
-  ( funext : FunExt)
+#def equiv-discrete-family-map uses (funext)
   ( X : U)
   ( A : X -> U)
   ( is-discrete-A : (x : X) -> is-discrete (A x))
   ( f g : (x : X) -> A x)
   ( h : f = g)
   : ( arr-eq ((x : X) -> A x) f g h) =
-    ( first (equiv-discrete-family funext X A is-discrete-A f g)) h
+    ( first (equiv-discrete-family X A is-discrete-A f g)) h
   :=
     idJ
     ( ( (x : X) -> A x) ,
       ( f) ,
       ( \ g' h' ->
         arr-eq ((x : X) -> A x) f g' h' =
-        (first (equiv-discrete-family funext X A is-discrete-A f g')) h') ,
+        (first (equiv-discrete-family X A is-discrete-A f g')) h') ,
       ( refl) ,
       ( g) ,
       ( h))
 ```
 
 ```rzk title="RS17, Proposition 7.2"
-#def is-discrete-dependent-function-discrete-family
-  ( funext : FunExt)
+#def is-discrete-dependent-function-discrete-family uses (funext)
   ( X : U)
   ( A : X -> U)
   ( is-discrete-A : (x : X) -> is-discrete (A x))
@@ -101,9 +106,9 @@ of discrete types is discrete.
       ( f = g)
       ( hom ((x : X) -> A x) f g)
       ( arr-eq ((x : X) -> A x) f g)
-      ( first (equiv-discrete-family funext X A is-discrete-A f g))
-      ( equiv-discrete-family-map funext X A is-discrete-A f g)
-      ( second (equiv-discrete-family funext X A is-discrete-A f g))
+      ( first (equiv-discrete-family X A is-discrete-A f g))
+      ( equiv-discrete-family-map X A is-discrete-A f g)
+      ( second (equiv-discrete-family X A is-discrete-A f g))
 ```
 
 By extension extensionality, an extension type into a family of discrete types
@@ -111,8 +116,7 @@ is discrete. Sinced fibered-Eq-extension-Equiv considers total extension types
 only, extending from BOT, that's all we prove here for now.
 
 ```rzk
-#def Eq-discrete-extension
-  ( extext : ExtExt)
+#def Eq-discrete-extension uses (extext)
   ( I : CUBE)
   ( ψ : I -> TOPE)
   ( A : ψ -> U)
@@ -143,8 +147,7 @@ only, extending from BOT, that's all we prove here for now.
         ( \ t s -> A t)
         ( \ (t , s) -> recOR (s === 0_2 |-> f t , s === 1_2 |-> g t)))
 
-#def Eq-discrete-extension-map
-  ( extext : ExtExt)
+#def Eq-discrete-extension-map uses (extext)
   ( I : CUBE)
   ( ψ : (t : I) -> TOPE)
   ( A : ψ -> U)
@@ -152,22 +155,21 @@ only, extending from BOT, that's all we prove here for now.
   ( f g : (t : ψ) -> A t)
   ( h : f = g)
   : arr-eq ((t : ψ) -> A t) f g h =
-    ( first (Eq-discrete-extension extext I ψ A is-discrete-A f g)) h
+    ( first (Eq-discrete-extension I ψ A is-discrete-A f g)) h
   :=
     idJ
     ( ( (t : ψ) -> A t) ,
       ( f) ,
       ( \ g' h' ->
         ( arr-eq ((t : ψ) -> A t) f g' h') =
-        ( first (Eq-discrete-extension extext I ψ A is-discrete-A f g') h')) ,
+        ( first (Eq-discrete-extension I ψ A is-discrete-A f g') h')) ,
       ( refl) ,
       ( g) ,
       ( h))
 ```
 
 ```rzk title="RS17, Proposition 7.2, for extension types"
-#def is-discrete-extension-family
-  ( extext : ExtExt)
+#def is-discrete-extension-family uses (extext)
   ( I : CUBE)
   ( ψ : (t : I) -> TOPE)
   ( A : ψ -> U)
@@ -179,20 +181,19 @@ only, extending from BOT, that's all we prove here for now.
       ( f = g)
       ( hom ((t : ψ) -> A t) f g)
       ( arr-eq ((t : ψ) -> A t) f g)
-      ( first (Eq-discrete-extension extext I ψ A is-discrete-A f g))
-      ( Eq-discrete-extension-map extext I ψ A is-discrete-A f g)
-      ( second (Eq-discrete-extension extext I ψ A is-discrete-A f g))
+      ( first (Eq-discrete-extension I ψ A is-discrete-A f g))
+      ( Eq-discrete-extension-map I ψ A is-discrete-A f g)
+      ( second (Eq-discrete-extension I ψ A is-discrete-A f g))
 ```
 
 For instance, the arrow type of a discrete type is discrete.
 
 ```rzk
-#def is-discrete-arr-is-discrete
-  ( extext : ExtExt)
+#def is-discrete-arr-is-discrete uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   : is-discrete (arr A)
-  := is-discrete-extension-family extext 2 Δ¹ (\ _ -> A) (\ _ -> is-discrete-A)
+  := is-discrete-extension-family 2 Δ¹ (\ _ -> A) (\ _ -> is-discrete-A)
 ```
 
 ## Discrete types are Segal types
@@ -202,28 +203,27 @@ Discrete types are automatically Segal types.
 ```rzk
 #section discrete-arr-equivalences
 
-#variable extext : ExtExt
 #variable A : U
 #variable is-discrete-A : is-discrete A
 #variables x y z w : A
 #variable f : hom A x y
 #variable g : hom A z w
 
-#def is-equiv-arr-eq-discrete uses (x y z w)
+#def is-equiv-arr-eq-discrete uses (extext x y z w)
   : is-equiv (f =_{Δ¹ -> A} g) (hom (arr A) f g) (arr-eq (arr A) f g)
-  := (is-discrete-arr-is-discrete extext A is-discrete-A) f g
+  := (is-discrete-arr-is-discrete A is-discrete-A) f g
 
-#def equiv-arr-eq-discrete uses (x y z w)
+#def equiv-arr-eq-discrete uses (extext x y z w)
   : Equiv (f =_{Δ¹ -> A} g) (hom (arr A) f g)
   := (arr-eq (arr A) f g ,
-          (is-discrete-arr-is-discrete extext A is-discrete-A) f g)
+          (is-discrete-arr-is-discrete A is-discrete-A) f g)
 
 #def equiv-square-hom-arr
   : Equiv
       ( hom (arr A) f g)
       ( Σ ( h : hom A x z) ,
           ( Σ ( k : hom A y w) ,
-              ( { ((t , s) : 2 * 2) | Δ¹×Δ¹ (t, s) } -> A
+              ( { (t , s) : Δ¹×Δ¹ } -> A
                 [ t === 0_2 /\ Δ¹ s |-> f s ,
                   t === 1_2 /\ Δ¹ s |-> g s ,
                   Δ¹ t /\ s === 0_2 |-> h t ,
@@ -290,7 +290,7 @@ Discrete types are automatically Segal types.
               ( product-transport A A (hom A) x z y w p q f = g)))
       ( Σ ( h : hom A x z) ,
           ( Σ ( k : hom A y w) ,
-              ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+              ( { (t , s) : Δ¹×Δ¹ } -> A
                 [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                   ((t === 1_2) /\ Δ¹ s) |-> g s ,
                   (Δ¹ t /\ (s === 0_2)) |-> h t ,
@@ -303,7 +303,7 @@ Discrete types are automatically Segal types.
               ( product-transport A A (hom A) x z y w p q f = g)))
       ( Σ ( h : hom A x z) ,
           ( Σ ( k : hom A y w) ,
-              ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+              ( { (t , s) : Δ¹×Δ¹ } -> A
                 [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                   ((t === 1_2) /\ Δ¹ s) |-> g s ,
                   (Δ¹ t /\ (s === 0_2)) |-> h t ,
@@ -321,7 +321,7 @@ Discrete types are automatically Segal types.
         ( hom (arr A) f g)
         ( Σ ( h : hom A x z) ,
             ( Σ ( k : hom A y w) ,
-                ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+                ( { (t , s) : Δ¹×Δ¹ } -> A
                   [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                     ((t === 1_2) /\ Δ¹ s) |-> g s ,
                     (Δ¹ t /\ (s === 0_2)) |-> h t ,
@@ -333,7 +333,6 @@ Discrete types are automatically Segal types.
 
 -- closing the section so I can use path induction
 #def fibered-map-square-sigma-over-product
-  ( extext : ExtExt)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z w : A)
@@ -342,7 +341,7 @@ Discrete types are automatically Segal types.
   ( q : y = w)
   : ( g : hom A z w) ->
     ( product-transport A A (hom A) x z y w p q f = g) ->
-    ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ( { (t , s) : Δ¹×Δ¹ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
         ((t === 1_2) /\ Δ¹ s) |-> g s ,
         (Δ¹ t /\ (s === 0_2)) |-> (arr-eq A x z p) t ,
@@ -354,7 +353,7 @@ Discrete types are automatically Segal types.
       ( \ z' p' ->
         ( g : hom A z' w) ->
         ( product-transport A A (hom A) x z' y w p' q f = g) ->
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
             ((t === 1_2) /\ Δ¹ s) |-> g s ,
             (Δ¹ t /\ (s === 0_2)) |-> (arr-eq A x z' p') t ,
@@ -365,7 +364,7 @@ Discrete types are automatically Segal types.
           ( \ w' q' ->
             ( g : hom A x w') ->
             ( product-transport A A (hom A) x x y w' refl q' f = g) ->
-            ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+            ( { (t , s) : Δ¹×Δ¹ } -> A
               [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                 ((t === 1_2) /\ Δ¹ s) |-> g s ,
                 (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -375,7 +374,7 @@ Discrete types are automatically Segal types.
             ( ( hom A x y) ,
               ( f) ,
               ( \ g' τ' ->
-                ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+                ( { (t , s) : Δ¹×Δ¹ } -> A
                   [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                     ((t === 1_2) /\ Δ¹ s) |-> g' s ,
                     (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -389,7 +388,6 @@ Discrete types are automatically Segal types.
       ( p))
 
 #def square-sigma-over-product
-  ( extext : ExtExt)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z w : A)
@@ -401,7 +399,7 @@ Discrete types are automatically Segal types.
             ( product-transport A A (hom A) x z y w p q f = g))))
   : Σ ( h : hom A x z) ,
       ( Σ ( k : hom A y w) ,
-          ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> h t ,
@@ -410,7 +408,6 @@ Discrete types are automatically Segal types.
     ( arr-eq A x z p ,
       ( arr-eq A y w q ,
         fibered-map-square-sigma-over-product
-          ( extext)
           ( A) (is-discrete-A)
           ( x) (y) (z) (w)
           ( f)
@@ -419,18 +416,16 @@ Discrete types are automatically Segal types.
           ( g)
           ( τ)))
 
-#def refl-refl-map-equiv-square-sigma-over-product
-  ( extext : ExtExt)
+#def refl-refl-map-equiv-square-sigma-over-product uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
   ( f g : hom A x y)
   ( τ : product-transport A A (hom A) x x y y refl refl f = g)
   : ( first
-      ( equiv-square-sigma-over-product extext A is-discrete-A x y x y f g)
+      ( equiv-square-sigma-over-product A is-discrete-A x y x y f g)
       (refl , (refl , τ))) =
     ( square-sigma-over-product
-      ( extext)
       ( A) (is-discrete-A)
       ( x) (y) (x) (y)
       ( f) (g)
@@ -441,10 +436,9 @@ Discrete types are automatically Segal types.
       ( f) ,
       ( \ g' τ' ->
         ( first
-          ( equiv-square-sigma-over-product extext A is-discrete-A x y x y f g')
+          ( equiv-square-sigma-over-product A is-discrete-A x y x y f g')
           ( refl , (refl , τ'))) =
         ( square-sigma-over-product
-          ( extext)
           ( A) (is-discrete-A)
           ( x) (y) (x) (y)
           ( f) (g')
@@ -453,8 +447,7 @@ Discrete types are automatically Segal types.
       ( g) ,
       ( τ))
 
-#def map-equiv-square-sigma-over-product
-  ( extext : ExtExt)
+#def map-equiv-square-sigma-over-product uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z w : A)
@@ -464,10 +457,10 @@ Discrete types are automatically Segal types.
   : ( g : hom A z w) ->
     ( τ : product-transport A A (hom A) x z y w p q f = g) ->
     ( first
-      ( equiv-square-sigma-over-product extext A is-discrete-A x y z w f g)
+      ( equiv-square-sigma-over-product A is-discrete-A x y z w f g)
       ( p , (q , τ))) =
     ( square-sigma-over-product
-        extext A is-discrete-A x y z w f g (p , (q , τ)))
+        A is-discrete-A x y z w f g (p , (q , τ)))
   :=
     idJ
     ( A ,
@@ -476,9 +469,9 @@ Discrete types are automatically Segal types.
       ( g : hom A z w') ->
       ( τ : product-transport A A (hom A) x z y w' p q' f = g) ->
       ( first (equiv-square-sigma-over-product
-                extext A is-discrete-A x y z w' f g))
+                A is-discrete-A x y z w' f g))
         ( p , (q' , τ)) =
-      ( square-sigma-over-product extext A is-discrete-A x y z w' f g)
+      ( square-sigma-over-product A is-discrete-A x y z w' f g)
         ( p , (q' , τ)) ,
       idJ
       ( ( A) ,
@@ -488,13 +481,12 @@ Discrete types are automatically Segal types.
           ( τ :
             product-transport A A (hom A) x z' y y p' refl f = g) ->
           ( first
-            ( equiv-square-sigma-over-product extext A is-discrete-A x y z' y f g)
+            ( equiv-square-sigma-over-product A is-discrete-A x y z' y f g)
             ( p' , (refl , τ))) =
-          ( square-sigma-over-product extext A is-discrete-A x y z' y f g
+          ( square-sigma-over-product A is-discrete-A x y z' y f g
             ( p' , (refl , τ)))) ,
         ( \ g τ ->
           refl-refl-map-equiv-square-sigma-over-product
-            ( extext)
             ( A) (is-discrete-A)
             ( x) (y)
             ( f) (g)
@@ -504,8 +496,7 @@ Discrete types are automatically Segal types.
       ( w) ,
       ( q))
 
-#def is-equiv-square-sigma-over-product
-  ( extext : ExtExt)
+#def is-equiv-square-sigma-over-product uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z w : A)
@@ -517,12 +508,12 @@ Discrete types are automatically Segal types.
             ( product-transport A A (hom A) x z y w p q f = g)))
     ( Σ ( h : hom A x z) ,
         ( Σ ( k : hom A y w) ,
-            ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+            ( { (t , s) : Δ¹×Δ¹ } -> A
               [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                 ((t === 1_2) /\ Δ¹ s) |-> g s ,
                 (Δ¹ t /\ (s === 0_2)) |-> h t ,
                 (Δ¹ t /\ (s === 1_2)) |-> k t ])))
-    ( square-sigma-over-product extext A is-discrete-A x y z w f g)
+    ( square-sigma-over-product A is-discrete-A x y z w f g)
   :=
     is-equiv-rev-homotopic-is-equiv
     ( Σ ( p : x = z) ,
@@ -530,22 +521,21 @@ Discrete types are automatically Segal types.
             ( product-transport A A (hom A) x z y w p q f = g)))
     ( Σ ( h : hom A x z) ,
         ( Σ ( k : hom A y w) ,
-            ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+            ( { (t , s) : Δ¹×Δ¹ } -> A
               [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
                 ((t === 1_2) /\ Δ¹ s) |-> g s ,
                 (Δ¹ t /\ (s === 0_2)) |-> h t ,
                 (Δ¹ t /\ (s === 1_2)) |-> k t ])))
     ( first
-      ( equiv-square-sigma-over-product extext A is-discrete-A x y z w f g))
-    ( square-sigma-over-product extext A is-discrete-A x y z w f g)
+      ( equiv-square-sigma-over-product A is-discrete-A x y z w f g))
+    ( square-sigma-over-product A is-discrete-A x y z w f g)
     ( \ (p , (q , τ)) ->
       map-equiv-square-sigma-over-product
-        extext A is-discrete-A x y z w f p q g τ)
+        A is-discrete-A x y z w f p q g τ)
     ( second
-      ( equiv-square-sigma-over-product extext A is-discrete-A x y z w f g))
+      ( equiv-square-sigma-over-product A is-discrete-A x y z w f g))
 
-#def is-equiv-fibered-map-square-sigma-over-product
-  ( extext : ExtExt)
+#def is-equiv-fibered-map-square-sigma-over-product uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z w : A)
@@ -555,12 +545,12 @@ Discrete types are automatically Segal types.
   ( q : y = w)
   : is-equiv
     ( product-transport A A (hom A) x z y w p q f = g)
-    ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ( { (t , s) : Δ¹×Δ¹ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
         ((t === 1_2) /\ Δ¹ s) |-> g s ,
         (Δ¹ t /\ (s === 0_2)) |-> (arr-eq A x z p) t ,
         (Δ¹ t /\ (s === 1_2)) |-> (arr-eq A y w q) t ])
-    ( fibered-map-square-sigma-over-product extext A is-discrete-A x y z w f p q g)
+    ( fibered-map-square-sigma-over-product A is-discrete-A x y z w f p q g)
   :=
     fibered-map-is-equiv-bases-are-equiv-total-map-is-equiv
       ( x = z)
@@ -569,7 +559,7 @@ Discrete types are automatically Segal types.
       ( hom A y w)
       ( \ p' q' -> (product-transport A A (hom A) x z y w p' q' f) = g)
       ( \ h' k' ->
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
             ((t === 1_2) /\ Δ¹ s) |-> g s ,
             (Δ¹ t /\ (s === 0_2)) |-> h' t ,
@@ -578,21 +568,19 @@ Discrete types are automatically Segal types.
       ( arr-eq A y w)
       ( \ p' q' ->
         fibered-map-square-sigma-over-product
-          ( extext)
           ( A) (is-discrete-A)
           ( x) (y) (z) (w)
           ( f)
           ( p')
           ( q')
           ( g))
-      ( is-equiv-square-sigma-over-product extext A is-discrete-A x y z w f g)
+      ( is-equiv-square-sigma-over-product A is-discrete-A x y z w f g)
       ( is-discrete-A x z)
       ( is-discrete-A y w)
       ( p)
       ( q)
 
-#def is-equiv-fibered-map-square-sigma-over-product-refl-refl
-  ( extext : ExtExt)
+#def is-equiv-fibered-map-square-sigma-over-product-refl-refl uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
@@ -600,23 +588,22 @@ Discrete types are automatically Segal types.
   ( g : hom A x y)
   : is-equiv
     (f = g)
-    ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ( { (t , s) : Δ¹×Δ¹ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
         ((t === 1_2) /\ Δ¹ s) |-> g s ,
         (Δ¹ t /\ (s === 0_2)) |-> x ,
         (Δ¹ t /\ (s === 1_2)) |-> y ])
     ( fibered-map-square-sigma-over-product
-      extext A is-discrete-A x y x y f refl refl g)
+      A is-discrete-A x y x y f refl refl g)
   :=
     is-equiv-fibered-map-square-sigma-over-product
-      extext A is-discrete-A x y x y f g refl refl
+      A is-discrete-A x y x y f g refl refl
 ```
 
 The previous calculations allow us to establish a family of equivalences:
 
 ```rzk
-#def is-equiv-sum-fibered-map-square-sigma-over-product-refl-refl
-  ( extext : ExtExt)
+#def is-equiv-sum-fibered-map-square-sigma-over-product-refl-refl uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
@@ -624,7 +611,7 @@ The previous calculations allow us to establish a family of equivalences:
   : is-equiv
     ( Σ (g : hom A x y) , f = g)
     ( Σ (g : hom A x y) ,
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
             ((t === 1_2) /\ Δ¹ s) |-> g s ,
             (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -633,34 +620,32 @@ The previous calculations allow us to establish a family of equivalences:
       ( hom A x y)
       ( \ g -> f = g)
       ( \ g ->
-        { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        { (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
           ((t === 1_2) /\ Δ¹ s) |-> g s ,
           (Δ¹ t /\ (s === 0_2)) |-> x ,
           (Δ¹ t /\ (s === 1_2)) |-> y ])
       ( fibered-map-square-sigma-over-product
-          extext A is-discrete-A x y x y f refl refl))
+          A is-discrete-A x y x y f refl refl))
   :=
     family-of-equiv-total-equiv
       ( hom A x y)
       ( \ g -> f = g)
       ( \ g ->
-        { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        { (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
           ((t === 1_2) /\ Δ¹ s) |-> g s ,
           (Δ¹ t /\ (s === 0_2)) |-> x ,
           (Δ¹ t /\ (s === 1_2)) |-> y ])
       ( fibered-map-square-sigma-over-product
-          extext A is-discrete-A x y x y f refl refl)
+          A is-discrete-A x y x y f refl refl)
       ( \ g ->
         is-equiv-fibered-map-square-sigma-over-product-refl-refl
-          ( extext)
           ( A) (is-discrete-A)
           ( x) (y)
           ( f) (g))
 
-#def equiv-sum-fibered-map-square-sigma-over-product-refl-refl
-  ( extext : ExtExt)
+#def equiv-sum-fibered-map-square-sigma-over-product-refl-refl uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
@@ -668,7 +653,7 @@ The previous calculations allow us to establish a family of equivalences:
   : Equiv
       ( Σ (g : hom A x y) , f = g)
       ( Σ (g : hom A x y) ,
-          ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -678,30 +663,29 @@ The previous calculations allow us to establish a family of equivalences:
         ( hom A x y)
         ( \ g -> f = g)
         ( \ g ->
-          { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> x ,
               (Δ¹ t /\ (s === 1_2)) |-> y ])
         ( fibered-map-square-sigma-over-product
-            extext A is-discrete-A x y x y f refl refl)) ,
+            A is-discrete-A x y x y f refl refl)) ,
     is-equiv-sum-fibered-map-square-sigma-over-product-refl-refl
-      extext A is-discrete-A x y f)
+      A is-discrete-A x y f)
 ```
 
 Now using the equivalence on total spaces and the contractibility of based path
 spaces, we conclude that the codomain extension type is contractible.
 
 ```rzk
-#def is-contr-horn-refl-refl-extension-type
-  ( extext : ExtExt)
+#def is-contr-horn-refl-refl-extension-type uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
   ( f : hom A x y)
   : is-contr
     ( Σ ( g : hom A x y) ,
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
             ((t === 1_2) /\ Δ¹ s) |-> g s ,
             (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -709,13 +693,13 @@ spaces, we conclude that the codomain extension type is contractible.
   := is-contr-is-equiv-from-contr
       ( Σ ( g : hom A x y) , f = g)
       ( Σ ( g : hom A x y) ,
-          ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> x ,
               (Δ¹ t /\ (s === 1_2)) |-> y ]))
       ( equiv-sum-fibered-map-square-sigma-over-product-refl-refl
-          extext A is-discrete-A x y f)
+          A is-discrete-A x y f)
       ( is-contr-based-paths (hom A x y) f)
 ```
 
@@ -728,7 +712,7 @@ The extension types that appear in the Segal condition are retracts of this type
   (x y : A)
   (f g : hom A x y)
   (α : hom2 A x y y f (id-arr A y) g)
-  : { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+  : { (t , s) : Δ¹×Δ¹ } -> A
     [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
       ((t === 1_2) /\ Δ¹ s) |-> g s ,
       (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -741,7 +725,7 @@ The extension types that appear in the Segal condition are retracts of this type
   ( f : hom A x y)
   ( (d , α) : Σ (d : hom A x y) , hom2 A x y y f (id-arr A y) d)
   : Σ ( g : hom A x y) ,
-      ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ( { (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
           ((t === 1_2) /\ Δ¹ s) |-> g s ,
           (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -754,7 +738,7 @@ The extension types that appear in the Segal condition are retracts of this type
   ( f : hom A x y)
   ( (g , σ) :
     Σ (g : hom A x y) ,
-      ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ( { (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
           ((t === 1_2) /\ Δ¹ s) |-> g s ,
           (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -769,7 +753,7 @@ The extension types that appear in the Segal condition are retracts of this type
   : is-retract-of
       ( Σ (d : hom A x y) , hom2 A x y y f (id-arr A y) d)
       ( Σ (g : hom A x y) ,
-          ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> x ,
@@ -784,8 +768,7 @@ We can now verify the Segal condition in the case of composable pairs in which
 the second arrow is an identity.
 
 ```rzk
-#def is-contr-hom2-with-id-is-discrete
-  ( extext : ExtExt)
+#def is-contr-hom2-with-id-is-discrete uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y : A)
@@ -795,13 +778,13 @@ the second arrow is an identity.
     is-retract-of-is-contr-is-contr
       ( Σ ( d : hom A x y) , (hom2 A x y y f (id-arr A y) d))
       ( Σ ( g : hom A x y) ,
-          ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+          ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> f s ,
               ((t === 1_2) /\ Δ¹ s) |-> g s ,
               (Δ¹ t /\ (s === 0_2)) |-> x ,
               (Δ¹ t /\ (s === 1_2)) |-> y ]))
       ( sigma-triangle-to-sigma-square-retract A x y f)
-      ( is-contr-horn-refl-refl-extension-type extext A is-discrete-A x y f)
+      ( is-contr-horn-refl-refl-extension-type A is-discrete-A x y f)
 ```
 
 But since `A` is discrete, its hom type family is equivalent to its identity
@@ -809,8 +792,7 @@ type family, and we can use "path induction" over arrows to reduce the general
 case to the one just proven:
 
 ```rzk
-#def is-contr-hom2-is-discrete
-  ( extext : ExtExt)
+#def is-contr-hom2-is-discrete uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   ( x y z : A)
@@ -826,7 +808,7 @@ case to the one just proven:
       ( is-discrete-A y)
       ( \ w d -> is-contr ( Σ (h : hom A x w) , hom2 A x y w f d h))
       ( is-contr-hom2-with-id-is-discrete
-          extext A is-discrete-A x y f)
+          A is-discrete-A x y f)
       ( z)
       ( g)
 ```
@@ -834,10 +816,9 @@ case to the one just proven:
 Finally, we conclude:
 
 ```rzk title="RS17, Proposition 7.3"
-#def is-segal-is-discrete
-  ( extext : ExtExt)
+#def is-segal-is-discrete uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   : is-segal A
-  := is-contr-hom2-is-discrete extext A is-discrete-A
+  := is-contr-hom2-is-discrete A is-discrete-A
 ```
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index b1e5fb3..d902cdd 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -32,9 +32,9 @@ live over a specified arrow in the base type.
   (u : C x)          -- A lift of the domain.
   (v : C y)          -- A lift of the codomain.
   : U
-    := {t : 2 | Δ¹ t } -> C (f t)
-      [t === 0_2 |-> u ,
-      t === 1_2 |-> v ]
+    := {t : Δ¹ } -> C (f t)
+      [ t === 0_2 |-> u ,
+        t === 1_2 |-> v ]
 ```
 
 It will be convenient to collect together dependent hom types with fixed domain
@@ -70,10 +70,10 @@ triangle.
   (gg : dhom A y z g C v w)    -- A lift of the second arrow.
   (hh : dhom A x z h C u w)    -- A lift of the diagonal arrow.
   : U
-    := { (t1 , t2) : 2 * 2 | Δ² (t1 , t2)} -> C (alpha (t1 , t2))
-      [t2 === 0_2 |-> ff t1 ,
-      t1 === 1_2 |-> gg t2 ,
-      t2 === t1 |-> hh t2 ]
+    := { (t1 , t2) : Δ² } -> C (alpha (t1 , t2))
+      [ t2 === 0_2 |-> ff t1 ,
+        t1 === 1_2 |-> gg t2 ,
+        t2 === t1  |-> hh t2 ]
 ```
 
 ## Covariant families
@@ -178,15 +178,17 @@ equivalences.
   (u : hom A a x)        -- A lift of the domain.
   (v : hom A a y)        -- A lift of the codomain.
   : Equiv (dhom-representable A a x y f u v)
-  ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
-                      ((t === 1_2) /\ Δ¹ s) |-> v s ,
-                      (Δ¹ t /\ (s === 0_2)) |-> a ,
-                      (Δ¹ t /\ (s === 1_2)) |-> f t ])
+  ({ (t , s) : Δ¹×Δ¹ } -> A
+    [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
+      ((t === 1_2) /\ Δ¹ s) |-> v s ,
+      (Δ¹ t /\ (s === 0_2)) |-> a ,
+      (Δ¹ t /\ (s === 1_2)) |-> f t ])
   := curry-uncurry 2 2 Δ¹ ∂Δ¹ Δ¹ ∂Δ¹ (\ t s -> A)
-    (\ (t , s) -> recOR (((t === 0_2) /\ Δ¹ s) |-> u s ,
-            ((t === 1_2) /\ Δ¹ s) |-> v s ,
-            (Δ¹ t /\ (s === 0_2)) |-> a ,
-            (Δ¹ t /\ (s === 1_2)) |-> f t ))
+    (\ (t , s) -> recOR
+      ( ((t === 0_2) /\ Δ¹ s) |-> u s ,
+        ((t === 1_2) /\ Δ¹ s) |-> v s ,
+        (Δ¹ t /\ (s === 0_2)) |-> a ,
+        (Δ¹ t /\ (s === 1_2)) |-> f t ))
 
 #def dhom-from-representable
   (A : U)            -- The ambient type.
@@ -203,15 +205,17 @@ equivalences.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv (dhom-from-representable A a x y f u)
-    (Σ (v : hom A a y) , ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
-                      ((t === 1_2) /\ Δ¹ s) |-> v s ,
-                      (Δ¹ t /\ (s === 0_2)) |-> a ,
-                      (Δ¹ t /\ (s === 1_2)) |-> f t ]))
+    (Σ (v : hom A a y) , ({ (t , s) : Δ¹×Δ¹ } -> A
+      [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
+        ((t === 1_2) /\ Δ¹ s) |-> v s ,
+        (Δ¹ t /\ (s === 0_2)) |-> a ,
+        (Δ¹ t /\ (s === 1_2)) |-> f t ]))
   := total-equiv-family-equiv (hom A a y) (\ v -> dhom-representable A a x y f u v)
-    (\ v -> ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
-                      ((t === 1_2) /\ Δ¹ s) |-> v s ,
-                      (Δ¹ t /\ (s === 0_2)) |-> a ,
-                      (Δ¹ t /\ (s === 1_2)) |-> f t ]))
+    (\ v -> ({ (t , s) : Δ¹×Δ¹ } -> A
+      [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
+        ((t === 1_2) /\ Δ¹ s) |-> v s ,
+        (Δ¹ t /\ (s === 0_2)) |-> a ,
+        (Δ¹ t /\ (s === 1_2)) |-> f t ]))
     (\ v -> uncurried-dhom-representable A a x y f u v)
 
 #def square-to-hom2-pushout
@@ -221,7 +225,7 @@ equivalences.
   (f : hom A x z)
   (g : hom A w y)
   (v : hom A y z)
-  : ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+  : ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> g t ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ])
@@ -236,7 +240,7 @@ equivalences.
   (g : hom A w y)
   (v : hom A y z)
   : (Σ (d : hom A w z) , product (hom2 A w x z u f d) (hom2 A w y z g v d))
-  -> ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+  -> ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> g t ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ])
@@ -249,7 +253,7 @@ equivalences.
   (f : hom A x z)
   (g : hom A w y)
   (v : hom A y z)
-  : Equiv ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+  : Equiv ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> g t ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ])
@@ -263,13 +267,13 @@ equivalences.
   (a x y : A)          -- The representing object and two points in the base.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
-  : Equiv (Σ (v : hom A a y) , ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+  : Equiv (Σ (v : hom A a y) , ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> a ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ]))
     (Σ (v : hom A a y) , (Σ (d : hom A a y) , product (hom2 A a x y u f d) (hom2 A a a y (id-arr A a) v d)))
   := total-equiv-family-equiv (hom A a y)
-    (\ v -> ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+    (\ v -> ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> a ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ]))
@@ -285,7 +289,7 @@ equivalences.
     (Σ (d : hom A a y) , (Σ (v : hom A a y) , product (hom2 A a x y u f d) (hom2 A a a y (id-arr A a) v d)))
   := triple-comp-equiv
     (dhom-from-representable A a x y f u)
-    (Σ (v : hom A a y) , ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+    (Σ (v : hom A a y) , ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> a ,
                       (Δ¹ t /\ (s === 1_2)) |-> f t ]))
@@ -435,7 +439,7 @@ types as follows.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv
-    ( { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    ( { (t , s) : ∂□ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ])
@@ -477,14 +481,14 @@ types as follows.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv
-    ( { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    ( { (t , s) : ∂□ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t])
     (hom A a y)
   :=
     comp-equiv
-    ( { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    ( { (t , s) : ∂□ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
           (Δ¹ t /\ (s === 0_2)) |-> a ,
           (Δ¹ t /\ (s === 1_2)) |-> f t ] )
@@ -501,24 +505,24 @@ types as follows.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv
-    (Σ (sq : { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    (Σ (sq : { (t , s) : ∂□ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
           (Δ¹ t /\ (s === 0_2)) |-> a ,
           (Δ¹ t /\ (s === 1_2)) |-> f t ]) ,
-        ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ({ (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             ((t === 1_2) /\ Δ¹ s) |-> (sq (1_2 , s)) ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ]))
     (Σ (v : hom A a y) ,
-      ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ({ (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             ((t === 1_2) /\ Δ¹ s) |-> v s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ]))
   :=
     total-equiv-pullback-is-equiv
-    (  { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    (  { (t , s) : ∂□ } -> A
       [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ] )
@@ -526,7 +530,7 @@ types as follows.
             (first (base-hom-expansion A a x y f u))
             (second (base-hom-expansion A a x y f u))
     ( \ v ->
-      ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ( { (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             ((t === 1_2) /\ Δ¹ s) |-> v s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
@@ -538,11 +542,11 @@ types as follows.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv (dhom-from-representable A a x y f u)
-      (Σ (sq : { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+      (Σ (sq : { (t , s) : ∂□ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               (Δ¹ t /\ (s === 0_2)) |-> a ,
               (Δ¹ t /\ (s === 1_2)) |-> f t ]) ,
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               ((t === 1_2) /\ Δ¹ s) |-> (sq (1_2 , s)) ,
               (Δ¹ t /\ (s === 0_2)) |-> a ,
@@ -550,16 +554,16 @@ types as follows.
   :=
     right-cancel-equiv
     ( dhom-from-representable A a x y f u)
-    ( Σ (sq : { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    ( Σ (sq : { (t , s) : ∂□ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               (Δ¹ t /\ (s === 0_2)) |-> a ,
               (Δ¹ t /\ (s === 1_2)) |-> f t ]) ,
-        ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ( { (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               ((t === 1_2) /\ Δ¹ s) |-> (sq (1_2 , s)) ,
               (Δ¹ t /\ (s === 0_2)) |-> a ,
               (Δ¹ t /\ (s === 1_2)) |-> f t ]))
-    ( Σ (v : hom A a y) , ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ( Σ (v : hom A a y) , ({ (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
           ((t === 1_2) /\ Δ¹ s) |-> v s ,
           (Δ¹ t /\ (s === 0_2)) |-> a ,
@@ -573,15 +577,15 @@ types as follows.
   (f : hom A x y)        -- An arrow in the base.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv
-    ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ({ (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
           (Δ¹ t /\ (s === 0_2)) |-> a ,
           (Δ¹ t /\ (s === 1_2)) |-> f t] )
-    (Σ (sq : { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    (Σ (sq : { (t , s) : ∂□ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ]) ,
-        ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ({ (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             ((t === 1_2) /\ Δ¹ s) |-> (sq (1_2 , s)) ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
@@ -603,22 +607,22 @@ types as follows.
   (u : hom A a x)        -- A lift of the domain.
   : Equiv
       (dhom-from-representable A a x y f u)
-      ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ({ (t , s) : Δ¹×Δ¹ } -> A
               [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
                 (Δ¹ t /\ (s === 0_2)) |-> a ,
                 (Δ¹ t /\ (s === 1_2)) |-> f t] )
   :=
     right-cancel-equiv
     ( dhom-from-representable A a x y f u)
-    ( { (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    ( { (t , s) : Δ¹×Δ¹ } -> A
         [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
           (Δ¹ t /\ (s === 0_2)) |-> a ,
           (Δ¹ t /\ (s === 1_2)) |-> f t] )
-    ( Σ (sq : { (t , s) : 2 * 2 | ∂□ (t , s)} -> A
+    ( Σ (sq : { (t , s) : ∂□ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             (Δ¹ t /\ (s === 0_2)) |-> a ,
             (Δ¹ t /\ (s === 1_2)) |-> f t ]) ,
-        ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ({ (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               ((t === 1_2) /\ Δ¹ s) |-> (sq (1_2 , s)) ,
               (Δ¹ t /\ (s === 0_2)) |-> a ,
@@ -852,7 +856,7 @@ a rather lengthy composition of equivalences.
   (u : hom A x a)        -- A lift of the domain.
   (v : hom A y a)        -- A lift of the codomain.
   : Equiv (dhom-contra-representable A a x y f u v)
-  ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
+  ({ (t , s) : Δ¹×Δ¹ } -> A [((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> f t ,
                       (Δ¹ t /\ (s === 1_2)) |-> a ])
@@ -878,7 +882,7 @@ a rather lengthy composition of equivalences.
   (v : hom A y a)    -- A lift of the codomain.
   : Equiv (dhom-to-representable A a x y f v)
     (Σ (u : hom A x a) ,
-        ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ({ (t , s) : Δ¹×Δ¹ } -> A
                     [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> f t ,
@@ -888,7 +892,7 @@ a rather lengthy composition of equivalences.
     ( hom A x a)
     ( \ u -> dhom-contra-representable A a x y f u v)
     ( \ u ->
-      ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ({ (t , s) : Δ¹×Δ¹ } -> A
           [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
             ((t === 1_2) /\ Δ¹ s) |-> v s ,
             (Δ¹ t /\ (s === 0_2)) |-> f t ,
@@ -901,7 +905,7 @@ a rather lengthy composition of equivalences.
   (f : hom A x y)    -- An arrow in the base.
   (v : hom A y a)    -- A lift of the codomain.
   : Equiv
-    (Σ (u : hom A x a) , ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+    (Σ (u : hom A x a) , ({ (t , s) : Δ¹×Δ¹ } -> A
                     [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> f t ,
@@ -912,7 +916,7 @@ a rather lengthy composition of equivalences.
   :=
     total-equiv-family-equiv (hom A x a)
     ( \ u ->
-      ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+      ({ (t , s) : Δ¹×Δ¹ } -> A
                     [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
                       ((t === 1_2) /\ Δ¹ s) |-> v s ,
                       (Δ¹ t /\ (s === 0_2)) |-> f t ,
@@ -936,7 +940,7 @@ a rather lengthy composition of equivalences.
     triple-comp-equiv
     ( dhom-to-representable A a x y f v)
     ( Σ (u : hom A x a) ,
-        ({ (t , s) : 2 * 2 | Δ¹×Δ¹ (t , s)} -> A
+        ({ (t , s) : Δ¹×Δ¹ } -> A
             [ ((t === 0_2) /\ Δ¹ s) |-> u s ,
               ((t === 1_2) /\ Δ¹ s) |-> v s ,
               (Δ¹ t /\ (s === 0_2)) |-> f t ,
diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 34f064e..e024948 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -19,6 +19,12 @@ This is a literate `rzk` file:
 - `5-segal-types.md` - We make heavy use of the notion of Segal types
 - `8-covariant.md` - We use covariant type families.
 
+Some of the definitions in this file rely on function extensionality:
+
+```rzk
+#assume funext : FunExt
+```
+
 ## Natural transformations involving a representable functor
 
 Fix a Segal type $A$ and a term $a : A$. The Yoneda lemma characterizes natural
@@ -138,8 +144,7 @@ in two steps.
         ( Segal-id-comp A is-segal-A a x f))
 
 -- By funext, these are equals as functions of f pointwise in x.
-#def yon-evid-once-pointwise
-  (funext : FunExt)
+#def yon-evid-once-pointwise uses (funext)
   (ϕ : (z : A) -> hom A a z -> C z)
   (x : A)
   : ((yon A is-segal-A a C is-covariant-C) ((evid A a C) ϕ )) x = ϕ x
@@ -152,8 +157,7 @@ in two steps.
       ( \ f -> yon-evid-twice-pointwise ϕ x f)
 
 -- By funext again, these are equal as functions of x and f.
-#def yon-evid
-  (funext : FunExt)
+#def yon-evid uses (funext)
   (ϕ : (z : A) -> hom A a z -> C z)
   : ((yon A is-segal-A a C is-covariant-C) ((evid A a C) ϕ )) = ϕ
   := eq-htpy funext
@@ -161,7 +165,7 @@ in two steps.
       ( \ x -> (hom A a x -> C x))
       ( \ x -> ((yon A is-segal-A a C is-covariant-C) ((evid A a C) ϕ )) x)
       ( \ x -> (ϕ x))
-      ( \ x -> yon-evid-once-pointwise funext ϕ x)
+      ( \ x -> yon-evid-once-pointwise ϕ x)
 
 #end yon-evid
 ```
@@ -171,8 +175,7 @@ in two steps.
 The Yoneda lemma says that evaluation at the identity defines an equivalence.
 
 ```rzk
-#def Yoneda-lemma
-  (funext : FunExt)
+#def Yoneda-lemma uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -181,7 +184,7 @@ The Yoneda lemma says that evaluation at the identity defines an equivalence.
   : is-equiv ((z : A) -> hom A a z -> C z) (C a) (evid A a C)
   :=
     ( ( ( yon A is-segal-A a C is-covariant-C),
-        ( yon-evid A is-segal-A a C is-covariant-C funext)),
+        ( yon-evid A is-segal-A a C is-covariant-C)),
       ( ( yon A is-segal-A a C is-covariant-C),
         ( evid-yon A is-segal-A a C is-covariant-C)))
 ```
@@ -298,8 +301,7 @@ in two steps.
         ( Segal-comp-id A is-segal-A x a f))
 
 -- By funext, these are equals as functions of f pointwise in x.
-#def contra-yon-evid-once-pointwise
-  (funext : FunExt)
+#def contra-yon-evid-once-pointwise uses (funext)
   (ϕ : (z : A) -> hom A z a -> C z)
   (x : A)
   : ((contra-yon A is-segal-A a C is-contravariant-C)
@@ -315,8 +317,7 @@ in two steps.
       ( \ f -> contra-yon-evid-twice-pointwise ϕ x f)
 
 -- By funext again, these are equal as functions of x and f.
-#def contra-yon-evid
-  (funext : FunExt)
+#def contra-yon-evid uses (funext)
   (ϕ : (z : A) -> hom A z a -> C z)
   : (contra-yon A is-segal-A a C is-contravariant-C)((contra-evid A a C) ϕ) = ϕ
   :=
@@ -327,7 +328,7 @@ in two steps.
         ( (contra-yon A is-segal-A a C is-contravariant-C)
               ((contra-evid A a C) ϕ )) x)
       ( \ x -> (ϕ x))
-      ( \ x -> contra-yon-evid-once-pointwise funext ϕ x)
+      ( \ x -> contra-yon-evid-once-pointwise ϕ x)
 
 #end contra-yon-evid
 ```
@@ -336,8 +337,7 @@ The contravariant Yoneda lemma says that evaluation at the identity defines an
 equivalence.
 
 ```rzk
-#def contra-Yoneda-lemma
-  (funext : FunExt)
+#def contra-Yoneda-lemma uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -346,7 +346,7 @@ equivalence.
   : is-equiv ((z : A) -> hom A z a -> C z) (C a) (contra-evid A a C)
   :=
     ( ( ( contra-yon A is-segal-A a C is-contravariant-C),
-        ( contra-yon-evid A is-segal-A a C is-contravariant-C funext)),
+        ( contra-yon-evid A is-segal-A a C is-contravariant-C)),
       ( ( contra-yon A is-segal-A a C is-contravariant-C),
         ( contra-evid-yon A is-segal-A a C is-contravariant-C)))
 ```
@@ -440,8 +440,7 @@ We now prove that induction from an initial element in the base of a covariant
 family defines an inverse equivalence to evaluation at the element.
 
 ```rzk title="RS17, Theorem 9.7"
-#def is-equiv-covariant-ev-initial
-  (funext : FunExt)
+#def is-equiv-covariant-ev-initial uses (funext)
   (A : U)
   (a : A)
   (is-initial-a : is-initial A a)
@@ -542,8 +541,7 @@ The dependent Yoneda lemma now follows by specializing these results.
   : ((p : coslice A a) -> C p) -> C (a, id-arr A a)
   := \ s -> s (a, id-arr A a)
 
-#def dependent-yoneda-lemma'
-  (funext : FunExt)
+#def dependent-yoneda-lemma' uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -555,7 +553,6 @@ The dependent Yoneda lemma now follows by specializing these results.
       ( dependent-ev-id A a C)
   :=
     is-equiv-covariant-ev-initial
-      ( funext)
       ( coslice A a)
       ( (a, id-arr A a))
       ( is-initial-id-arr-is-segal A is-segal-A a)
@@ -567,8 +564,7 @@ The actual dependent Yoneda is equivalent to the result just proven, just with
 an equivalent type in the domain of the evaluation map.
 
 ```rzk title="RS17, Theorem 9.5"
-#def dependent-yoneda-lemma
-  (funext : FunExt)
+#def dependent-yoneda-lemma uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -586,7 +582,7 @@ an equivalent type in the domain of the evaluation map.
       ( first (equiv-dependent-curry A (\ z -> hom A a z)(\ x f -> C (x, f))))
       ( second (equiv-dependent-curry A (\ z -> hom A a z)(\ x f -> C (x, f))))
       ( \ s -> s a (id-arr A a))
-      ( dependent-yoneda-lemma' funext A is-segal-A a C is-covariant-C)
+      ( dependent-yoneda-lemma' A is-segal-A a C is-covariant-C)
 ```
 
 ## Final objects
@@ -673,8 +669,7 @@ We now prove that induction from a final element in the base of a contravariant
 family defines an inverse equivalence to evaluation at the element.
 
 ```rzk title="RS17, Theorem 9.7, dual"
-#def is-equiv-contravariant-ev-final
-  (funext : FunExt)
+#def is-equiv-contravariant-ev-final uses (funext)
   (A : U)
   (a : A)
   (is-final-a : is-final A a)
@@ -776,8 +771,7 @@ specializing these results.
   : ((p : slice A a) -> C p) -> C (a, id-arr A a)
   := \ s -> s (a, id-arr A a)
 
-#def contra-dependent-yoneda-lemma'
-  (funext : FunExt)
+#def contra-dependent-yoneda-lemma' uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -789,7 +783,6 @@ specializing these results.
       ( contra-dependent-ev-id A a C)
   :=
     is-equiv-contravariant-ev-final
-      ( funext)
       ( slice A a)
       ( (a, id-arr A a))
       ( is-final-id-arr-is-segal A is-segal-A a)
@@ -801,8 +794,7 @@ The actual contravariant dependent Yoneda is equivalent to the result just
 proven, just with an equivalent type in the domain of the evaluation map.
 
 ```rzk title="RS17, Theorem 9.5, dual"
-#def contra-dependent-yoneda-lemma
-  (funext : FunExt)
+#def contra-dependent-yoneda-lemma uses (funext)
   (A : U)
   (is-segal-A : is-segal A)
   (a : A)
@@ -821,5 +813,5 @@ proven, just with an equivalent type in the domain of the evaluation map.
       ( second (equiv-dependent-curry A (\ z -> hom A z a)(\ x f -> C (x, f))))
       ( \ s -> s a (id-arr A a))
       ( contra-dependent-yoneda-lemma'
-          funext A is-segal-A a C is-contravariant-C)
+          A is-segal-A a C is-contravariant-C)
 ```
diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md
index 09ac15d..2a34dbe 100644
--- a/src/simplicial-hott/10-rezk-types.rzk.md
+++ b/src/simplicial-hott/10-rezk-types.rzk.md
@@ -6,6 +6,12 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
+Some of the definitions in this file rely on extension extensionality:
+
+```rzk
+#assume extext : ExtExt
+```
+
 ```rzk
 #section isomorphisms
 
@@ -74,8 +80,7 @@ This is a literate `rzk` file:
     : (arrow-has-inverse A is-segal-A x y f) -> (arrow-is-iso A is-segal-A x y f)
     := (\ (g , (p , q)) -> ((g , p) , (g , q)))
 
-#def arrow-iso-to-inverse
-    (extext : ExtExt) -- This proof uses extension extensionality.
+#def arrow-iso-to-inverse uses (extext)
     (A : U)
     (is-segal-A : is-segal A)
     (x y : A)
@@ -119,17 +124,15 @@ This is a literate `rzk` file:
     )
  )
 
-#def arrow-inverse-iff-iso
-    (extext : ExtExt) -- This proof uses extension extensionality.
+#def arrow-inverse-iff-iso uses (extext)
     (A : U)
     (is-segal-A : is-segal A)
     (x y : A)
     (f : hom A x y)
     : iff (arrow-has-inverse A is-segal-A x y f) (arrow-is-iso A is-segal-A x y f)
-    := (arrow-inverse-to-iso A is-segal-A x y f , arrow-iso-to-inverse extext A is-segal-A x y f)
+    := (arrow-inverse-to-iso A is-segal-A x y f , arrow-iso-to-inverse A is-segal-A x y f)
 
-#def if-iso-then-postcomp-has-retraction
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-postcomp-has-retraction uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -153,8 +156,7 @@ This is a literate `rzk` file:
        )
   )
 
-#def if-iso-then-postcomp-has-section
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-postcomp-has-section uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -178,8 +180,7 @@ This is a literate `rzk` file:
        )
   )
 
-#def if-iso-then-postcomp-is-equiv
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-postcomp-is-equiv uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -191,11 +192,10 @@ This is a literate `rzk` file:
   : (z : A) -> is-equiv (hom A z x) (hom A z y) (Segal-postcomp A is-segal-A x y f z)
   :=
     \ z ->
-    ( (if-iso-then-postcomp-has-retraction extext A is-segal-A x y f g gg z) ,
-      (if-iso-then-postcomp-has-section extext A is-segal-A x y f h hh z))
+    ( (if-iso-then-postcomp-has-retraction A is-segal-A x y f g gg z) ,
+      (if-iso-then-postcomp-has-section A is-segal-A x y f h hh z))
 
-#def if-iso-then-precomp-has-retraction
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-precomp-has-retraction uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -224,8 +224,7 @@ This is a literate `rzk` file:
        )
   )
 
-#def if-iso-then-precomp-has-section
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-precomp-has-section uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -253,8 +252,7 @@ This is a literate `rzk` file:
        )
   )
 
-#def if-iso-then-precomp-is-equiv
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def if-iso-then-precomp-is-equiv uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -266,11 +264,10 @@ This is a literate `rzk` file:
   : (z : A) -> is-equiv (hom A y z) (hom A x z) (Segal-precomp A is-segal-A x y f z)
   :=
     \ z ->
-    ( (if-iso-then-precomp-has-retraction extext A is-segal-A x y f h hh z) ,
-    (if-iso-then-precomp-has-section extext A is-segal-A x y f g gg z))
+    ( (if-iso-then-precomp-has-retraction A is-segal-A x y f h hh z) ,
+    (if-iso-then-precomp-has-section A is-segal-A x y f g gg z))
 
-#def iso-inhabited-implies-hasRetr-contr
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def iso-inhabited-implies-hasRetr-contr uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -281,11 +278,10 @@ This is a literate `rzk` file:
   (hh : arrow-has-section A is-segal-A x y f h)
   : is-contr (arrow-Retraction A is-segal-A x y f)
   := (is-contr-map-is-equiv (hom A y x) (hom A x x) (Segal-precomp A is-segal-A x y f x)
-                          (if-iso-then-precomp-is-equiv extext A is-segal-A x y f g gg h hh x))
+                          (if-iso-then-precomp-is-equiv A is-segal-A x y f g gg h hh x))
       (id-arr A x)
 
-#def iso-inhabited-implies-hasSec-contr
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def iso-inhabited-implies-hasSec-contr uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -296,11 +292,10 @@ This is a literate `rzk` file:
   (hh : arrow-has-section A is-segal-A x y f h)
   : is-contr (arrow-Section A is-segal-A x y f)
   := (is-contr-map-is-equiv (hom A y x) (hom A y y) (Segal-postcomp A is-segal-A x y f y)
-                          (if-iso-then-postcomp-is-equiv extext A is-segal-A x y f g gg h hh y))
+                          (if-iso-then-postcomp-is-equiv A is-segal-A x y f g gg h hh y))
       (id-arr A y)
 
-#def iso-inhabited-implies-iso-contr
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def iso-inhabited-implies-iso-contr uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
@@ -311,19 +306,18 @@ This is a literate `rzk` file:
   (hh : arrow-has-section A is-segal-A x y f h)
   : is-contr (arrow-is-iso A is-segal-A x y f)
   := (is-contr-product (arrow-Retraction A is-segal-A x y f) (arrow-Section A is-segal-A x y f)
-      (iso-inhabited-implies-hasRetr-contr extext A is-segal-A x y f g gg h hh)
-      (iso-inhabited-implies-hasSec-contr extext A is-segal-A x y f g gg h hh)
+      (iso-inhabited-implies-hasRetr-contr A is-segal-A x y f g gg h hh)
+      (iso-inhabited-implies-hasSec-contr A is-segal-A x y f g gg h hh)
     )
 
-#def iso-is-prop
-  (extext : ExtExt) -- This proof uses extension extensionality.
+#def iso-is-prop uses (extext)
   (A : U)
   (is-segal-A : is-segal A)
   (x y : A)
   (f : hom A x y)
    : (is-prop (arrow-is-iso A is-segal-A x y f))
   := (is-prop-is-contr-is-inhabited (arrow-is-iso A is-segal-A x y f)
-      (\ is-isof -> (iso-inhabited-implies-iso-contr extext A is-segal-A x y f (first (first is-isof)) (second (first is-isof))
+      (\ is-isof -> (iso-inhabited-implies-iso-contr A is-segal-A x y f (first (first is-isof)) (second (first is-isof))
         (first (second is-isof)) (second (second is-isof))))
     )