chore: make Discrete into a record so it displays better

src/1Lab/Classical.lagda.md

@@ -161,12 +161,12 @@ prove that $\Sigma P$ is also discrete. Since the path type $N \equiv S$ in $\Si
 is equivalent to $P$, this concludes the proof.
 
 ```agda
-  Discrete-ΣP : Discrete (Susp ∣ P ∣)
-  Discrete-ΣP = ∥-∥-rec (Dec-is-hlevel 1 (Susp-prop-is-set (hlevel 1) _ _))
-    (λ f → Discrete-inj (fst ∘ f) (right-inverse→injective 2→Σ (snd ∘ f))
-                        Discrete-Bool)
-    section
+  instance
+    Discrete-ΣP : Discrete (Susp ∣ P ∣)
+    Discrete-ΣP = case section of λ f → Discrete-inj (fst ∘ f)
+      (right-inverse→injective 2→Σ (snd ∘ f))
+      Discrete-Bool
 
   AC→LEM : Dec ∣ P ∣
-  AC→LEM = Susp-prop-path (hlevel 1) <≃> Discrete-ΣP
+  AC→LEM = Susp-prop-path (hlevel 1) <≃> auto
 ```

src/1Lab/Equiv.lagda.md

@@ -1056,7 +1056,8 @@ id≃ : ∀ {ℓ} {A : Type ℓ} → A ≃ A
 id≃ = id , id-equiv
 
 _∙e_ : A ≃ B → B ≃ C → A ≃ C
-_∙e_ (f , ef) (g , eg) = g ∘ f , ∘-is-equiv ef eg
+{-# INLINE _∙e_ #-}
+_∙e_ (f , ef) (g , eg) = record { fst = g ∘ f ; snd = ∘-is-equiv ef eg }
 
 _e⁻¹ : A ≃ B → B ≃ A
 ((f , ef) e⁻¹) = equiv→inverse ef , inverse-is-equiv ef

src/1Lab/Path/IdentitySystem.lagda.md

@@ -457,7 +457,8 @@ This is known as **Hedberg's theorem**.
 
 opaque
   Discrete→is-set : ∀ {ℓ} {A : Type ℓ} → Discrete A → is-set A
-  Discrete→is-set {A = A} dec = identity-system→hlevel 1
-    (¬¬-stable-identity-system (dec→dne ⦃ dec ⦄))
+  Discrete→is-set {A = A} dec =
+    let instance _ = dec in identity-system→hlevel 1
+    (¬¬-stable-identity-system dec→dne)
     λ x y f g → funext λ h → absurd (g h)
 ```

src/Algebra/Group/Ab.lagda.md

@@ -200,18 +200,15 @@ open Functor
 
 Ab↪Grp : ∀ {ℓ} → Functor (Ab ℓ) (Groups ℓ)
 Ab↪Grp .F₀ = Abelian→Group
-Ab↪Grp .F₁ f .hom = f .hom
-Ab↪Grp .F₁ f .preserves = f .preserves
+Ab↪Grp .F₁ f = record { ∫Hom f }
 Ab↪Grp .F-id = trivial!
 Ab↪Grp .F-∘ f g = trivial!
 
 Ab↪Grp-is-ff : ∀ {ℓ} → is-fully-faithful (Ab↪Grp {ℓ})
 Ab↪Grp-is-ff {x = A} {B} = is-iso→is-equiv $ iso
-  promote (λ _ → trivial!) (λ _ → trivial!)
-  where
-    promote : Groups.Hom (Abelian→Group A) (Abelian→Group B) → Ab.Hom A B
-    promote f .hom = f .hom
-    promote f .preserves = f .preserves
+  (λ f → record { ∫Hom f })
+  (λ _ → ext λ _ → refl)
+  (λ _ → ext λ _ → refl)
 
 Ab↪Sets : ∀ {ℓ} → Functor (Ab ℓ) (Sets ℓ)
 Ab↪Sets = Grp↪Sets F∘ Ab↪Grp

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

@@ -201,13 +201,13 @@ open Free-object
 ```agda
 make-free-abelian : ∀ {ℓ} (G : Group ℓ) → Free-object Ab↪Grp G
 make-free-abelian G .free = Abelianise G
-make-free-abelian G .unit .hom =  inc^ab G
-make-free-abelian G .unit .preserves .is-group-hom.pres-⋆ x y = refl
-make-free-abelian G .fold {H} f .hom =
+make-free-abelian G .unit .fst =  inc^ab G
+make-free-abelian G .unit .snd .is-group-hom.pres-⋆ x y = refl
+make-free-abelian G .fold {H} f .fst =
   Coeq-elim (λ _ → H.has-is-set) (apply f) (λ (a , b , c) → resp a b c) where
   module G = Group-on (G .snd)
   module H = Abelian-group-on (H .snd)
-  open is-group-hom (f .preserves)
+  open is-group-hom (f .snd)
   abstract
     resp : ∀ a b c → f · (a G.⋆ (b G.⋆ c)) ≡ f · (a G.⋆ (c G.⋆ b))
     resp a b c =
@@ -217,8 +217,8 @@ make-free-abelian G .fold {H} f .hom =
       f · a H.* (f · c H.* f · b) ≡˘⟨ ap (f · a H.*_) (pres-⋆ _ _) ⟩
       f · a H.* f · (c G.⋆ b)     ≡˘⟨ pres-⋆ _ _ ⟩
       f · (a G.⋆ (c G.⋆ b))       ∎
-make-free-abelian G .fold {H} f .preserves .is-group-hom.pres-⋆ =
-  elim! λ _ _ → f .preserves .is-group-hom.pres-⋆ _ _
+make-free-abelian G .fold {H} f .snd .is-group-hom.pres-⋆ =
+  elim! λ _ _ → f .snd .is-group-hom.pres-⋆ _ _
 make-free-abelian G .commute = trivial!
 make-free-abelian G .unique f p = ext (p ·ₚ_)
 ```

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

@@ -56,7 +56,7 @@ module _ {ℓ} (T : Type ℓ) (t-set : is-set T) where
   function→free-ab-hom G fn = morp where
     module G = Abelian-group-on (G .snd)
     go₀ : Free-group T → ⌞ G ⌟
-    go₀ = fold-free-group {G = G .fst , G.Abelian→Group-on} fn .hom
+    go₀ = fold-free-group {G = G .fst , G.Abelian→Group-on} fn .fst
 
     go : ⌞ Free-abelian T ⌟ → ⌞ G ⌟
     go (inc x)              = go₀ x
@@ -65,7 +65,7 @@ module _ {ℓ} (T : Type ℓ) (t-set : is-set T) where
       G.has-is-set (go x) (go y) (λ i → go (p i)) (λ i → go (q i)) i j
 
     morp : Ab.Hom (Free-abelian T) G
-    morp .hom = go
-    morp .preserves .pres-⋆ = elim! λ x y → refl
+    morp .fst = go
+    morp .snd .pres-⋆ = elim! λ x y → refl
 ```
 -->

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

@@ -19,7 +19,7 @@ module Algebra.Group.Ab.Hom where
 <!--
 ```agda
 open is-group-hom
-open Total-hom
+open ∫Hom
 ```
 -->
 
@@ -57,23 +57,23 @@ Abelian-group-on-hom A B = to-abelian-group-on make-ab-on-hom module Hom-ab wher
 -->
 
 ```agda
-  make-ab-on-hom .mul f g .hom x = f · x B.* g · x
-  make-ab-on-hom .mul f g .preserves .pres-⋆ x y =
-    f · (x A.* y) B.* g · (x A.* y)          ≡⟨ ap₂ B._*_ (f .preserves .pres-⋆ x y) (g .preserves .pres-⋆ x y) ⟩
+  make-ab-on-hom .mul f g .fst x = f · x B.* g · x
+  make-ab-on-hom .mul f g .snd .pres-⋆ x y =
+    f · (x A.* y) B.* g · (x A.* y)          ≡⟨ ap₂ B._*_ (f .snd .pres-⋆ x y) (g .snd .pres-⋆ x y) ⟩
     (f · x B.* f · y) B.* (g · x B.* g · y)  ≡⟨ B.pullr (B.pulll refl)  ⟩
     f · x B.* (f · y B.* g · x) B.* g · y    ≡⟨ (λ i → f · x B.* B.commutes {x = f · y} {y = g · x} i B.* (g · y)) ⟩
     f · x B.* (g · x B.* f · y) B.* g · y    ≡⟨ B.pushr (B.pushl refl) ⟩
     (f · x B.* g · x) B.* (f · y B.* g · y)  ∎
 
-  make-ab-on-hom .inv f .hom x = B._⁻¹ (f · x)
-  make-ab-on-hom .inv f .preserves .pres-⋆ x y =
-    f · (x A.* y) B.⁻¹            ≡⟨ ap B._⁻¹ (f .preserves .pres-⋆ x y) ⟩
+  make-ab-on-hom .inv f .fst x = B._⁻¹ (f · x)
+  make-ab-on-hom .inv f .snd .pres-⋆ x y =
+    f · (x A.* y) B.⁻¹            ≡⟨ ap B._⁻¹ (f .snd .pres-⋆ x y) ⟩
     (f · x B.* f · y) B.⁻¹        ≡⟨ B.inv-comm ⟩
     (f · y B.⁻¹) B.* (f · x B.⁻¹) ≡⟨ B.commutes ⟩
     (f · x B.⁻¹) B.* (f · y B.⁻¹) ∎
 
-  make-ab-on-hom .1g .hom x = B.1g
-  make-ab-on-hom .1g .preserves .pres-⋆ x y = B.introl refl
+  make-ab-on-hom .1g .fst x = B.1g
+  make-ab-on-hom .1g .snd .pres-⋆ x y = B.introl refl
 ```
 
 <!--
@@ -98,9 +98,9 @@ $\Ab\op \times \Ab \to \Ab$.
 ```agda
 Ab-hom-functor : ∀ {ℓ} → Functor (Ab ℓ ^op ×ᶜ Ab ℓ) (Ab ℓ)
 Ab-hom-functor .F₀ (A , B) = Ab[ A , B ]
-Ab-hom-functor .F₁ (f , g) .hom h = g Ab.∘ h Ab.∘ f
-Ab-hom-functor .F₁ (f , g) .preserves .pres-⋆ x y = ext λ z →
-  g .preserves .pres-⋆ _ _
+Ab-hom-functor .F₁ (f , g) .fst h = g Ab.∘ h Ab.∘ f
+Ab-hom-functor .F₁ (f , g) .snd .pres-⋆ x y = ext λ z →
+  g .snd .pres-⋆ _ _
 Ab-hom-functor .F-id    = trivial!
 Ab-hom-functor .F-∘ f g = trivial!
 ```

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

@@ -70,18 +70,18 @@ limits][rapl]).
 
 ```agda
   ⊕-proj₁ : Ab.Hom (G ⊕ H) G
-  ⊕-proj₁ .hom = fst
-  ⊕-proj₁ .preserves .pres-⋆ x y = refl
+  ⊕-proj₁ .fst = fst
+  ⊕-proj₁ .snd .pres-⋆ x y = refl
 
   ⊕-proj₂ : Ab.Hom (G ⊕ H) H
-  ⊕-proj₂ .hom = snd
-  ⊕-proj₂ .preserves .pres-⋆ x y = refl
+  ⊕-proj₂ .fst = snd
+  ⊕-proj₂ .snd .pres-⋆ x y = refl
 
   open is-product
   Direct-sum-is-product : is-product (Ab ℓ) {A = G} {H} {G ⊕ H} ⊕-proj₁ ⊕-proj₂
-  Direct-sum-is-product .⟨_,_⟩ f g .hom x = f · x , g · x
-  Direct-sum-is-product .⟨_,_⟩ f g .preserves .pres-⋆ x y =
-    Σ-pathp (f .preserves .pres-⋆ x y) (g .preserves .pres-⋆ x y)
+  Direct-sum-is-product .⟨_,_⟩ f g .fst x = f · x , g · x
+  Direct-sum-is-product .⟨_,_⟩ f g .snd .pres-⋆ x y =
+    Σ-pathp (f .snd .pres-⋆ x y) (g .snd .pres-⋆ x y)
 
   Direct-sum-is-product .π₁∘⟨⟩ = trivial!
   Direct-sum-is-product .π₂∘⟨⟩ = trivial!

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

@@ -112,17 +112,17 @@ homomorphisms $A \to [B,C]$.
 
 ```agda
   curry-bilinear : Bilinear A B C → Ab.Hom A Ab[ B , C ]
-  curry-bilinear f .hom a .hom       = f .Bilinear.map a
-  curry-bilinear f .hom a .preserves = Bilinear.fixl-is-group-hom f a
-  curry-bilinear f .preserves .is-group-hom.pres-⋆ x y = ext λ z →
+  curry-bilinear f .fst a .fst = f .Bilinear.map a
+  curry-bilinear f .fst a .snd = Bilinear.fixl-is-group-hom f a
+  curry-bilinear f .snd .is-group-hom.pres-⋆ x y = ext λ z →
     f .Bilinear.pres-*l _ _ _
 
   curry-bilinear-is-equiv : is-equiv curry-bilinear
   curry-bilinear-is-equiv = is-iso→is-equiv morp where
     morp : is-iso curry-bilinear
     morp .is-iso.from uc .Bilinear.map x y = uc · x · y
-    morp .is-iso.from uc .Bilinear.pres-*l x y z = ap (_· _) (uc .preserves .is-group-hom.pres-⋆ _ _)
-    morp .is-iso.from uc .Bilinear.pres-*r x y z = (uc · _) .preserves .is-group-hom.pres-⋆ _ _
+    morp .is-iso.from uc .Bilinear.pres-*l x y z = ap (_· _) (uc .snd .is-group-hom.pres-⋆ _ _)
+    morp .is-iso.from uc .Bilinear.pres-*r x y z = (uc · _) .snd .is-group-hom.pres-⋆ _ _
     morp .is-iso.rinv uc = trivial!
     morp .is-iso.linv uc = trivial!
 ```
@@ -272,8 +272,8 @@ module _ {ℓ} (A B C : Abelian-group ℓ) where
 
 ```agda
   from-bilinear-map : Bilinear A B C → Ab.Hom (A ⊗ B) C
-  from-bilinear-map bilin .hom = bilinear-map→function A B C bilin
-  from-bilinear-map bilin .preserves .is-group-hom.pres-⋆ x y = refl
+  from-bilinear-map bilin .fst = bilinear-map→function A B C bilin
+  from-bilinear-map bilin .snd .is-group-hom.pres-⋆ x y = refl
 ```
 
 It's also easy to construct a function in the opposite direction,
@@ -286,19 +286,19 @@ an equivalence requires appealing to an induction principle of
   to-bilinear-map : Ab.Hom (A ⊗ B) C → Bilinear A B C
   to-bilinear-map gh .Bilinear.map x y = gh · (x , y)
   to-bilinear-map gh .Bilinear.pres-*l x y z =
-    ap (apply gh) t-pres-*l ∙ gh .preserves .is-group-hom.pres-⋆ _ _
+    ap (apply gh) t-pres-*l ∙ gh .snd .is-group-hom.pres-⋆ _ _
   to-bilinear-map gh .Bilinear.pres-*r x y z =
-    ap (apply gh) t-pres-*r ∙ gh .preserves .is-group-hom.pres-⋆ _ _
+    ap (apply gh) t-pres-*r ∙ gh .snd .is-group-hom.pres-⋆ _ _
 
   from-bilinear-map-is-equiv : is-equiv from-bilinear-map
   from-bilinear-map-is-equiv = is-iso→is-equiv morp where
     morp : is-iso from-bilinear-map
     morp .is-iso.from = to-bilinear-map
     morp .is-iso.rinv hom = ext $ Tensor-elim-prop A B (λ x → C.has-is-set _ _)
       (λ x y → refl)
-      (λ x y → ap₂ C._*_ x y ∙ sym (hom .preserves .is-group-hom.pres-⋆ _ _))
-      (λ x → ap C._⁻¹ x ∙ sym (is-group-hom.pres-inv (hom .preserves)))
-      (sym (is-group-hom.pres-id (hom .preserves)))
+      (λ x y → ap₂ C._*_ x y ∙ sym (hom .snd .is-group-hom.pres-⋆ _ _))
+      (λ x → ap C._⁻¹ x ∙ sym (is-group-hom.pres-inv (hom .snd)))
+      (sym (is-group-hom.pres-id (hom .snd)))
     morp .is-iso.linv x = trivial!
 ```
 
@@ -318,7 +318,7 @@ module _ {ℓ} {A B C : Abelian-group ℓ} where instance
     : ∀ {ℓr} ⦃ ef : Extensional (⌞ A ⌟ → ⌞ B ⌟ → ⌞ C ⌟) ℓr ⦄ → Extensional (Ab.Hom (A ⊗ B) C) ℓr
   Extensional-tensor-hom ⦃ ef ⦄ =
     injection→extensional!
-      {f = λ f x y → f .hom (x , y)}
+      {f = λ f x y → f .fst (x , y)}
       (λ {x} p → Hom≃Bilinear.injective _ _ _ (ext (subst (ef .Pathᵉ _) p (ef .reflᵉ _))))
       auto
   {-# OVERLAPS Extensional-tensor-hom #-}
@@ -348,8 +348,8 @@ Ab-tensor-functor .F₀ (A , B) = A ⊗ B
 Ab-tensor-functor .F₁ (f , g) = from-bilinear-map _ _ _ bilin where
   bilin : Bilinear _ _ _
   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
+  bilin .Bilinear.pres-*l x y z = ap (_, g · z) (f .snd .is-group-hom.pres-⋆ _ _) ∙ t-pres-*l
+  bilin .Bilinear.pres-*r x y z = ap (f · x ,_) (g .snd .is-group-hom.pres-⋆ _ _) ∙ t-pres-*r
 Ab-tensor-functor .F-id    = trivial!
 Ab-tensor-functor .F-∘ f g = trivial!
 

src/Algebra/Group/Action.lagda.md

@@ -130,19 +130,19 @@ of $G$ on the object $F(\bull)$!
 
 ```agda
     Functor→action : (F : Functor BG C) → Action G (F .F₀ tt)
-    Functor→action F .hom it = C.make-iso
+    Functor→action F .fst it = C.make-iso
         (F .F₁ it) (F .F₁ (it ⁻¹))
         (F.annihilate inversel) (F.annihilate inverser)
       where
         open Group-on (G .snd)
         module F = Functor-kit F
-    Functor→action F .preserves .is-group-hom.pres-⋆ x y = ext (F .F-∘ _ _)
+    Functor→action F .snd .is-group-hom.pres-⋆ x y = ext (F .F-∘ _ _)
 
     Action→functor : {X : C.Ob} (A : Action G X) → Functor BG C
     Action→functor {X = X} A .F₀ _ = X
     Action→functor A .F₁ e = (A · e) .C.to
-    Action→functor A .F-id = ap C.to (is-group-hom.pres-id (A .preserves))
-    Action→functor A .F-∘ f g = ap C.to (is-group-hom.pres-⋆ (A .preserves) _ _)
+    Action→functor A .F-id = ap C.to (is-group-hom.pres-id (A .snd))
+    Action→functor A .F-∘ f g = ap C.to (is-group-hom.pres-⋆ (A .snd) _ _)
 ```
 
 After constructing these functions in either direction, it's easy enough
@@ -161,7 +161,7 @@ applying the right helpers for pushing paths inwards, we're left with
       .is-iso.from (x , act) → Action→functor act
       .is-iso.linv x → Functor-path (λ _ → refl) λ _ → refl
       .is-iso.rinv x → Σ-pathp refl $
-        total-hom-pathp _ _ _ (funext (λ i → C.≅-pathp _ _ refl))
+        ∫Hom-pathp _ _ _ (funext (λ i → C.≅-pathp _ _ refl))
           (is-prop→pathp (λ i → is-group-hom-is-prop) _ _)
 ```
 
@@ -196,8 +196,8 @@ module _ {ℓ} (G : Group ℓ) where
 
 ```agda
   principal-action : Action (Sets ℓ) G (G .fst)
-  principal-action .hom x = equiv→iso ((G._⋆ x) , G.⋆-equivr x)
-  principal-action .preserves .pres-⋆ x y = ext λ z → G.associative
+  principal-action .fst x = equiv→iso ((G._⋆ x) , G.⋆-equivr x)
+  principal-action .snd .pres-⋆ x y = ext λ z → G.associative
 ```
 
 $G$ also acts on itself *as a group* by **conjugation**. An automorphism
@@ -206,8 +206,8 @@ of $G$ that arises from conjugation with an element of $G$ is called an
 
 ```agda
   conjugation-action : Action (Groups ℓ) G G
-  conjugation-action .hom x = total-iso
+  conjugation-action .fst x = total-iso
     ((λ y → x G.⁻¹ G.⋆ y G.⋆ x) , ∘-is-equiv (G.⋆-equivr x) (G.⋆-equivl (x G.⁻¹)))
     (record { pres-⋆ = λ y z → group! G })
-  conjugation-action .preserves .pres-⋆ x y = ext λ z → group! G
+  conjugation-action .snd .pres-⋆ x y = ext λ z → group! G
 ```

src/Algebra/Group/Cat/Base.lagda.md

@@ -96,8 +96,8 @@ LiftGroup {ℓ} ℓ' G = G' where
   G' .snd .has-is-group .inverser = ap lift G.inverser
 
 G→LiftG : ∀ {ℓ} (G : Group ℓ) → Groups.Hom G (LiftGroup lzero G)
-G→LiftG G .hom = lift
-G→LiftG G .preserves .pres-⋆ _ _ = refl
+G→LiftG G .fst = lift
+G→LiftG G .snd .pres-⋆ _ _ = refl
 ```
 -->