chore: get rid of Extensionality w/w

src/Algebra/Group/Ab/Tensor.lagda.md

@@ -94,12 +94,10 @@ module _ {A : Abelian-group ℓ} {B : Abelian-group ℓ'} {C : Abelian-group ℓ
       q i .pres-*r x y z = is-prop→pathp (λ i → C.has-is-set (p x (y B.* z) i) (p x y i C.* p x z i))
         (ba .pres-*r x y z) (bb .pres-*r x y z) i
 
-  Extensional-bilinear : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Bilinear A B C) ℓr
-  Extensional-bilinear ⦃ ef ⦄ = injection→extensional! (λ h → Bilinear-path (λ x y → h # x # y)) ef
-
   instance
-    extensionality-bilinear : Extensionality (Bilinear A B C)
-    extensionality-bilinear = record { lemma = quote Extensional-bilinear }
+    Extensional-bilinear
+      : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Bilinear A B C) ℓr
+    Extensional-bilinear ⦃ ef ⦄ = injection→extensional! (λ h → Bilinear-path (λ x y → h # x # y)) ef
 
 module _ {ℓ} (A B C : Abelian-group ℓ) where
 ```
@@ -314,6 +312,16 @@ an equivalence requires appealing to an induction principle of
 
   module Bilinear≃Hom = Equiv Bilinear≃Hom
   module Hom≃Bilinear = Equiv Hom≃Bilinear
+
+module _ {ℓ} {A B C : Abelian-group ℓ} where instance
+  Extensional-tensor-hom
+    : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Ab.Hom (A ⊗ B) C) ℓr
+  Extensional-tensor-hom ⦃ ef ⦄ =
+    injection→extensional! {B = ⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟}
+      {f = λ f x y → f .hom (x , y)}
+      (λ {x} p → Hom≃Bilinear.injective _ _ _ (ext (subst (ef .Pathᵉ _) p (ef .reflᵉ _))))
+      auto
+  {-# OVERLAPS Extensional-tensor-hom #-}
 ```
 -->
 
@@ -342,8 +350,8 @@ Ab-tensor-functor .F₁ (f , g) = from-bilinear-map _ _ _ bilin where
   bilin .Bilinear.map x y       = f # x , g # y
   bilin .Bilinear.pres-*l x y z = ap (_, g # z) (f .preserves .is-group-hom.pres-⋆ _ _) ∙ t-pres-*l
   bilin .Bilinear.pres-*r x y z = ap (f # x ,_) (g .preserves .is-group-hom.pres-⋆ _ _) ∙ t-pres-*r
-Ab-tensor-functor .F-id    = Hom≃Bilinear.injective _ _ _ trivial!
-Ab-tensor-functor .F-∘ f g = Hom≃Bilinear.injective _ _ _ trivial!
+Ab-tensor-functor .F-id    = trivial!
+Ab-tensor-functor .F-∘ f g = trivial!
 
 Tensor⊣Hom : (A : Abelian-group ℓ) → Bifunctor.Left Ab-tensor-functor A ⊣ Bifunctor.Right Ab-hom-functor A
 Tensor⊣Hom A = hom-iso→adjoints to to-eqv nat where

src/Algebra/Group/Subgroup.lagda.md

@@ -310,10 +310,8 @@ rest of the construction, most of it is applying induction
 will compute.
 
 ```agda
-    coeq : is-coequaliser _ _ A→im
-    coeq .coequal = Forget-is-faithful (funext path) where
-      path : (x : ⌞ Kerf.ker ⌟) → A→im # A.unit ≡ A→im # (x .fst)
-      path (x* , p) = Tpath (f.pres-id ∙ sym p)
+    coeq : is-coequaliser (Groups.Zero.zero→ ∅ᴳ) Kerf.kernel A→im
+    coeq .coequal = ext λ x p → f.pres-id ∙ sym p
 
     coeq .universal {F = F} {e' = e'} p = gh where
       module F = Group-on (F .snd)
@@ -328,17 +326,8 @@ will compute.
 
     coeq .factors = Forget-is-faithful refl
 
-    coeq .unique {F} {p = p} {colim = colim} prf = Forget-is-faithful (funext path)
-      where
-        module F = Group-on (F .snd)
-        path : ∀ (x : image (apply f)) → colim # x ≡ elim p (x .snd)
-        path (x , t) =
-          ∥-∥-elim
-            {P = λ q → colim # (x , q) ≡ elim p q}
-            (λ _ → F.has-is-set _ _)
-            (λ { (f , fp) → ap (apply colim) (Σ-prop-path! (sym fp))
-                          ∙ (happly (ap hom prf) f) })
-            t
+    coeq .unique {F} {p = p} {colim = colim} prf = ext λ x y p →
+      ap# colim (Σ-prop-path! (sym p)) ∙ happly (ap hom prf) y
 ```
 
 ## Representing kernels

src/Algebra/Ring/Module.lagda.md

@@ -412,6 +412,7 @@ open Mod
     ; Module-on→Abelian-group-on
     ; H-Level-is-linear-map
     ; H-Level-is-module
+    ; H-Level-Linear-map
     )
   public
 
@@ -428,18 +429,16 @@ module _ {ℓ} {R : Ring ℓ} where
       ; Module-on→Abelian-group-on
       ; H-Level-is-linear-map
       ; H-Level-is-module
+      ; H-Level-Linear-map
       )
     public
 
-  Extensional-linear-map
-    : ∀ {ℓr} {M : Module R ℓm} {N : Module R ℓn}
-    → ⦃ ext : Extensional (⌞ M ⌟ → ⌞ N ⌟) ℓr ⦄
-    → Extensional (Linear-map M N) ℓr
-  Extensional-linear-map ⦃ ext ⦄ = injection→extensional! (λ p → Linear-map-path (happly p)) ext
-
   instance
-    extensionality-linear-map : {M : Module R ℓm} {N : Module R ℓn} → Extensionality (Linear-map M N)
-    extensionality-linear-map = record { lemma = quote Extensional-linear-map }
+    Extensional-linear-map
+      : ∀ {ℓr} {M : Module R ℓm} {N : Module R ℓn}
+      → ⦃ ext : Extensional (⌞ M ⌟ → ⌞ N ⌟) ℓr ⦄
+      → Extensional (Linear-map M N) ℓr
+    Extensional-linear-map ⦃ ext ⦄ = injection→extensional! (λ p → Linear-map-path (happly p)) ext
 
 module R-Mod {ℓ ℓm} {R : Ring ℓ} = Cat.Reasoning (R-Mod R ℓm)
 
@@ -456,5 +455,14 @@ linear-map→hom
   → R-Mod.Hom M N
 linear-map→hom h .hom       = h .map
 linear-map→hom h .preserves = h .lin
+
+extensional-mod-hom
+  : ∀ {ℓ ℓrel} {R : Ring ℓ} {M : Module R ℓm} {N : Module R ℓm}
+  → ⦃ ext : Extensional (Linear-map M N) ℓrel ⦄
+  → Extensional (R-Mod R _ .Precategory.Hom M N) ℓrel
+extensional-mod-hom ⦃ ei ⦄ = injection→extensional! {f = hom→linear-map} (λ p → ext λ e → ap map p $ₚ e) ei
+
+instance Extensional-mod-hom = extensional-mod-hom
+{-# OVERLAPS Extensional-mod-hom #-}
 ```
 -->

src/Algebra/Ring/Module/Action.lagda.md

@@ -101,13 +101,15 @@ and ring morphisms $R \to [G,G]$ into the [endomorphism ring] of $G$.
 
   Action→Hom G act .hom r .hom = act .Ring-action._⋆_ r
   Action→Hom G act .hom r .preserves .is-group-hom.pres-⋆ x y = act .Ring-action.⋆-distribl r x y
-  Action→Hom G act .preserves .is-ring-hom.pres-id    = Homomorphism-path λ i → act .Ring-action.⋆-id _
-  Action→Hom G act .preserves .is-ring-hom.pres-+ x y = Homomorphism-path λ i → act .Ring-action.⋆-distribr _ _ _
-  Action→Hom G act .preserves .is-ring-hom.pres-* r s = Homomorphism-path λ x → sym (act .Ring-action.⋆-assoc _ _ _)
+  Action→Hom G act .preserves .is-ring-hom.pres-id    = ext λ x → act .Ring-action.⋆-id _
+  Action→Hom G act .preserves .is-ring-hom.pres-+ x y = ext λ x → act .Ring-action.⋆-distribr _ _ _
+  Action→Hom G act .preserves .is-ring-hom.pres-* r s = ext λ x → sym (act .Ring-action.⋆-assoc _ _ _)
 
   Action≃Hom
     : (G : Abelian-group ℓ)
     → Ring-action (G .snd) ≃ Rings.Hom R (Endo Ab-ab-category G)
-  Action≃Hom G = Iso→Equiv $ Action→Hom G , iso (Hom→Action G)
-    (λ x → trivial!) (λ x → refl)
+  Action≃Hom G =
+    Iso→Equiv $ Action→Hom G , iso (Hom→Action G) (λ x → trivial!)
+      (λ x → Iso.injective eqv (Σ-prop-path! refl))
+    where private unquoteDecl eqv = declare-record-iso eqv (quote Ring-action)
 ```

src/Algebra/Ring/Module/Free.lagda.md

@@ -249,34 +249,15 @@ equal-on-basis M {f} {g} p =
     module g = Linear-map g
     module M = Module-on (M .snd)
 
-Extensional-linear-map-free
-  : ∀ {ℓb ℓg ℓr} {T : Type ℓb} {M : Module R ℓg}
-  → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄
-  → Extensional (Linear-map (Free-Mod T) M) ℓr
-Extensional-linear-map-free {M = M} ⦃ ext ⦄ =
-  injection→extensional! {f = λ m x → m .map (inc x)} (λ p → equal-on-basis M (happly p)) ext
-
-Extensional-hom-free
-  : ∀ {ℓ' ℓr} {T : Type ℓ'} {M : Module R (ℓ ⊔ ℓ')}
-  → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄
-  → Extensional (R-Mod.Hom (Free-Mod T) M) ℓr
-Extensional-hom-free {M = M} ⦃ ef ⦄ =
-  injection→extensional! {f = λ m x → m # (inc x)}
-    (λ {f} {g} p →
-      let it = equal-on-basis M {hom→linear-map f} {hom→linear-map g} (happly p)
-       in ext (happly (ap map it)))
-    ef
-
 instance
-  extensionality-linear-map-free
-    : ∀ {ℓb ℓg} {T : Type ℓb} {M : Module R ℓg}
-    → Extensionality (Linear-map (Free-Mod T) M)
-  extensionality-linear-map-free = record { lemma = quote Extensional-linear-map-free }
-
-  extensionality-hom-free
-    : ∀ {ℓ'} {T : Type ℓ'} {M : Module R (ℓ ⊔ ℓ')}
-    → Extensionality (R-Mod.Hom {ℓm = ℓ ⊔ ℓ'} (Free-Mod T) M)
-  extensionality-hom-free = record { lemma = quote Extensional-hom-free }
+  Extensional-linear-map-free
+    : ∀ {ℓb ℓg ℓr} {T : Type ℓb} {M : Module R ℓg}
+    → ⦃ ext : Extensional (T → ⌞ M ⌟) ℓr ⦄
+    → Extensional (Linear-map (Free-Mod T) M) ℓr
+  Extensional-linear-map-free {M = M} ⦃ ext ⦄ =
+    injection→extensional! {f = λ m x → m .map (inc x)} (λ p → equal-on-basis M (happly p)) ext
+
+  {-# OVERLAPS Extensional-linear-map-free #-}
 ```
 -->
 

src/Cat/Base.lagda.md

@@ -580,49 +580,19 @@ instance
     → Funlike (F => G) ⌞ C ⌟ (λ x → D .Precategory.Hom (F # x) (G # x))
   Funlike-natural-transformation = record { _#_ = _=>_.η }
 
-{-
-Set-up for using natural transformations with the extensionality tactic;
-See the docs in 1Lab.Extensionality for a more detailed explanation of
-how it works.
-
-This function is the actual worker which computes the preferred
-identity system for natural transformations. Its type asks for
-
-   ∀ x → Extensional (D.Hom (F # x) (G # x))
-
-instead of the more generic ∀ x y → Extensional (D.Hom x y) so that
-any specific *instances* for D.Hom involving the object parts of F and G
-have a chance to fire. E.g. if G is the product functor on Sets then
-(x → y) will only match the funext instance but (x → G # y) will
-match funext *and* product extensionality.
--}
-Extensional-natural-transformation
-  : ∀ {o ℓ o' ℓ' ℓr} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
-  → {F G : Functor C D}
-  → {@(tactic extensionalᶠ {A = ⌞ C ⌟ → Type _}
-        (λ x → D .Hom (F # x) (G # x)))
-      sa : ∀ x → Extensional (D .Hom (F # x) (G # x)) ℓr}
-  → Extensional (F => G) (o ⊔ ℓr)
-Extensional-natural-transformation {sa = sa} .Pathᵉ f g = ∀ i → Pathᵉ (sa i) (f .η i) (g .η i)
-Extensional-natural-transformation {sa = sa} .reflᵉ x i = reflᵉ (sa i) (x .η i)
-Extensional-natural-transformation {sa = sa} .idsᵉ .to-path x = Nat-pathp _ _ λ i →
-  sa _ .idsᵉ .to-path (x i)
-Extensional-natural-transformation {D = D} {sa = sa} .idsᵉ .to-path-over h =
-  is-prop→pathp
-    (λ i → Π-is-hlevel 1
-      (λ _ → Equiv→is-hlevel 1 (identity-system-gives-path (sa _ .idsᵉ)) (D .Hom-set _ _ _ _)))
-    _ _
-
--- Actually define the loop-breaker instance which tells the
--- extensionality tactic what lemma to use for a type of natural
--- transformations.
-
-instance
-  extensionality-natural-transformation
-    : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
-        {F G : Functor C D}
-    → Extensionality (F => G)
-  extensionality-natural-transformation = record
-    { lemma = quote Extensional-natural-transformation }
+  Extensional-natural-transformation
+    : ∀ {o ℓ o' ℓ' ℓr} {C : Precategory o ℓ} {D : Precategory o' ℓ'}
+    → {F G : Functor C D}
+    → ⦃ sa : {x : ⌞ C ⌟} → Extensional (D .Hom (F # x) (G # x)) ℓr ⦄
+    → Extensional (F => G) (o ⊔ ℓr)
+  Extensional-natural-transformation ⦃ sa ⦄ .Pathᵉ f g = ∀ i → Pathᵉ sa (f .η i) (g .η i)
+  Extensional-natural-transformation ⦃ sa ⦄ .reflᵉ x i = reflᵉ sa (x .η i)
+  Extensional-natural-transformation ⦃ sa ⦄ .idsᵉ .to-path x = Nat-pathp _ _ λ i →
+    sa .idsᵉ .to-path (x i)
+  Extensional-natural-transformation {D = D} ⦃ sa ⦄ .idsᵉ .to-path-over h =
+    is-prop→pathp
+      (λ i → Π-is-hlevel 1
+        (λ _ → Equiv→is-hlevel 1 (identity-system-gives-path (sa .idsᵉ)) (D .Hom-set _ _ _ _)))
+      _ _
 ```
 -->

src/Cat/Diagram/Monad.lagda.md

@@ -204,7 +204,7 @@ open Algebra-hom public
 
 open _=>_ using (η)
 
-module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where
+module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where instance
   private module C = Cat.Reasoning C
 
   Extensional-Algebra-Hom
@@ -214,22 +214,18 @@ module _ {o ℓ} {C : Precategory o ℓ} {M : Monad C} where
   Extensional-Algebra-Hom ⦃ sa ⦄ = injection→extensional!
     (Algebra-hom-path C) sa
 
-  instance
-    extensionality-algebra-hom
-      : ∀ {a b} {A : Algebra-on C M a} {B : Algebra-on C M b}
-      → Extensionality (Algebra-hom C M (a , A) (b , B))
-    extensionality-algebra-hom = record { lemma = quote Extensional-Algebra-Hom }
+  Funlike-Algebra-hom
+    : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {X Y}
+    → ⦃ i : Funlike (C.Hom (X .fst) (Y .fst)) A B ⦄
+    → Funlike (Algebra-hom C M X Y) A B
+  Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x
 
-  instance
-    Funlike-Algebra-hom
-      : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {X Y}
-      → ⦃ i : Funlike (C.Hom (X .fst) (Y .fst)) A B ⦄
-      → Funlike (Algebra-hom C M X Y) A B
-    Funlike-Algebra-hom ⦃ i ⦄ .Funlike._#_ f x = f .morphism # x
+  H-Level-Algebra-hom : ∀ {A B n} → H-Level (Algebra-hom C M A B) (2 + n)
+  H-Level-Algebra-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv (hlevel 2)
+    where unquoteDecl eqv = declare-record-iso eqv (quote Algebra-hom)
 
 module _ {o ℓ} (C : Precategory o ℓ) where
   private module C = Cat.Reasoning C
-  private unquoteDecl eqv = declare-record-iso eqv (quote Algebra-hom)
 ```
 -->
 
@@ -281,8 +277,7 @@ the identity and associativity laws from its underlying category.
     Eilenberg-Moore .idr f = ext (C.idr _)
     Eilenberg-Moore .idl f = ext (C.idl _)
     Eilenberg-Moore .assoc f g h = ext (C.assoc _ _ _)
-    Eilenberg-Moore .Hom-set X Y = Iso→is-hlevel 2 eqv (hlevel 2)
-      where open C.HLevel-instance
+    Eilenberg-Moore .Hom-set X Y = hlevel 2
 ```
 
 </details>

src/Cat/Displayed/Univalence/Thin.lagda.md

@@ -128,32 +128,23 @@ module _ {ℓ o' ℓ'} {S : Type ℓ → Type o'} {spec : Thin-structure ℓ' S}
     module So = Precategory (Structured-objects spec)
     module Som = Cat.Morphism (Structured-objects spec)
 
-  Extensional-Hom
-    : ∀ {a b ℓr} ⦃ sa : Extensional (⌞ a ⌟ → ⌞ b ⌟) ℓr ⦄
-    → Extensional (So.Hom a b) ℓr
-  Extensional-Hom ⦃ sa ⦄ = injection→extensional!
-    (Structured-hom-path spec) sa
-
   instance
-    extensionality-hom : ∀ {a b} → Extensionality (So.Hom a b)
-    extensionality-hom = record { lemma = quote Extensional-Hom }
+    Extensional-Hom
+      : ∀ {a b ℓr} ⦃ sa : Extensional (⌞ a ⌟ → ⌞ b ⌟) ℓr ⦄
+      → Extensional (So.Hom a b) ℓr
+    Extensional-Hom ⦃ sa ⦄ = injection→extensional!
+      (Structured-hom-path spec) sa
 
     Funlike-Hom : ∀ {x y} → Funlike (So.Hom x y) ⌞ x ⌟ λ _ → ⌞ y ⌟
     Funlike-Hom = record
       { _#_ = Total-hom.hom
       }
 
-  Homomorphism-path
-    : ∀ {x y : So.Ob} {f g : So.Hom x y}
-    → (∀ x → f # x ≡ g # x)
-    → f ≡ g
-  Homomorphism-path h = Structured-hom-path spec (funext h)
-
   Homomorphism-monic
     : ∀ {x y : So.Ob} (f : So.Hom x y)
     → (∀ {x y} (p : f # x ≡ f # y) → x ≡ y)
     → Som.is-monic f
-  Homomorphism-monic f wit g h p = Homomorphism-path λ x → wit (ap hom p $ₚ x)
+  Homomorphism-monic f wit g h p = ext λ x → wit (ap hom p $ₚ x)
 
 record is-equational {ℓ o' ℓ'} {S : Type ℓ → Type o'} (spec : Thin-structure ℓ' S) : Type (lsuc ℓ ⊔ o' ⊔ ℓ') where
   field

src/Cat/Functor/Base.lagda.md

@@ -77,9 +77,9 @@ Cat[ C , D ] .Pc.Hom-set F G = Nat-is-set
 Cat[ C , D ] .Pc.id  = idnt
 Cat[ C , D ] .Pc._∘_ = _∘nt_
 
-Cat[ C , D ] .Pc.idr f       = ext λ x → Pc.idr D _
-Cat[ C , D ] .Pc.idl f       = ext λ x → Pc.idl D _
-Cat[ C , D ] .Pc.assoc f g h = ext λ x → Pc.assoc D _ _ _
+Cat[ C , D ] .Pc.idr f       = ext λ x → D .Pc.idr _
+Cat[ C , D ] .Pc.idl f       = ext λ x → D .Pc.idl _
+Cat[ C , D ] .Pc.assoc f g h = ext λ x → D .Pc.assoc _ _ _
 ```
 
 We'll also need the following foundational tool, characterising paths

src/Cat/Functor/Subcategory.lagda.md

@@ -91,15 +91,12 @@ module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {S : Subcat C o' ℓ'} where
   Subcat-hom-pathp {f = f} {g = g} p q r i .witness =
     is-prop→pathp (λ i → is-hom-prop (r i) (p i .snd) (q i .snd)) (f .witness) (g .witness) i
 
-  Extensional-subcat-hom
-    : ∀ {ℓr x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) ℓr ⦄
-    → Extensional (Subcat-hom S x y) ℓr
-  Extensional-subcat-hom ⦃ sa ⦄ = injection→extensional!
-    (Subcat-hom-pathp refl refl) sa
-
   instance
-    extensionality-subcat-hom : ∀ {x y} → Extensionality (Subcat-hom S x y)
-    extensionality-subcat-hom = record { lemma = quote Extensional-subcat-hom }
+    Extensional-subcat-hom
+      : ∀ {ℓr x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) ℓr ⦄
+      → Extensional (Subcat-hom S x y) ℓr
+    Extensional-subcat-hom ⦃ sa ⦄ = injection→extensional!
+      (Subcat-hom-pathp refl refl) sa
 
     Funlike-Subcat-hom
       : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y}