Clean up APIs for terminal and initial objects

src/1Lab/Equiv.lagda.md

@@ -833,6 +833,17 @@ is-contr→≃⊤ : is-contr A → A ≃ ⊤
 is-contr→≃⊤ c = is-contr→≃ c ⊤-is-contr
 ```
 
+<!--
+```agda
+is-contr≃equiv-⊤ : is-contr A ≃ (A ≃ ⊤)
+is-contr≃equiv-⊤ .fst = is-contr→≃⊤
+is-contr≃equiv-⊤ .snd = is-iso→is-equiv λ where
+  .is-iso.from e → contr (Equiv.from e tt) λ x → Equiv.η e x
+  .is-iso.rinv e → Σ-pathp refl (is-equiv-is-prop _ _ _)
+  .is-iso.linv x → is-contr-is-prop _ _
+```
+-->
+
 ### Strictness of the empty type
 
 We say that an [[initial object]] is *strict* if every map into it is an

src/1Lab/Type/Pi.lagda.md

@@ -67,6 +67,29 @@ codomain of a dependent function by an equivalence across universe levels:
   equiv-path (k x) (f {x}) (g {x} , λ k → p k {x}) i .snd j
 ```
 
+<!--
+```agda
+Π-ap-cod₂
+  : ∀ {ℓa ℓb ℓp ℓq}
+  → {A : Type ℓa} {B : A → Type ℓb}
+  → {P : (a : A) → B a → Type ℓp}
+  → {Q : (a : A) → B a → Type ℓq}
+  → (∀ (a : A) → (b : B a) → P a b ≃ Q a b)
+  → (∀ (a : A) (b : B a) → P a b) ≃ (∀ (a : A) (b : B a) → Q a b)
+Π-ap-cod₂ e = Π-ap-cod λ x → Π-ap-cod (e x)
+
+Π-ap-cod₃
+  : ∀ {ℓa ℓb ℓc ℓp ℓq}
+  → {A : Type ℓa} {B : A → Type ℓb} {C : (a : A) → B a → Type ℓc}
+  → {P : (a : A) (b : B a) → C a b → Type ℓp}
+  → {Q : (a : A) (b : B a) → C a b → Type ℓq}
+  → (∀ (a : A) (b : B a) (c : C a b) → P a b c ≃ Q a b c)
+  → (∀ (a : A) (b : B a) (c : C a b) → P a b c) ≃ (∀ (a : A) (b : B a) (c : C a b) → Q a b c)
+Π-ap-cod₃ e = Π-ap-cod λ x → Π-ap-cod₂ (e x)
+```
+-->
+
+
 For non-dependent functions, we can easily perturb both domain and
 codomain:
 
@@ -282,5 +305,15 @@ flip f b a = f a b
 Π²-impl≃ .fst f = f _ _
 Π²-impl≃ .snd .is-eqv f .centre = strict-fibres (λ f _ _ → f) (λ {a} {b} → f {a} {b}) .fst
 Π²-impl≃ .snd .is-eqv f .paths  = strict-fibres (λ f _ _ → f) (λ {a} {b} → f {a} {b}) .snd
+
+const-fibre-prop≃
+  : ∀ {ℓa ℓb} {A : Type ℓa} {B : Type ℓb}
+  → is-prop A
+  → (a a' : A)
+  → fibre (λ (b : B) → a) a' ≃ B
+const-fibre-prop≃ {B = B} A-prop a a' =
+  fibre (λ b → a) a' ≃⟨⟩
+  B × a ≡ a'         ≃⟨ Σ-contr-snd (λ b → Path-is-hlevel' zero A-prop a a') ⟩
+  B                  ≃∎
 ```
 -->

src/1Lab/Type/Sigma.lagda.md

@@ -154,6 +154,27 @@ they are included for completeness. </summary>
 ```
 </details>
 
+<!--
+```agda
+Σ-ap-snd₂
+  : ∀ {ℓa ℓb ℓp ℓq}
+  → {A : Type ℓa} {B : A → Type ℓb}
+  → {P : (a : A) → B a → Type ℓp}
+  → {Q : (a : A) → B a → Type ℓq}
+  → (∀ (a : A) → (b : B a) → P a b ≃ Q a b)
+  → (Σ[ a ∈ A ] Σ[ b ∈ B a ] P a b) ≃ (Σ[ a ∈ A ] Σ[ b ∈ B a ] Q a b)
+Σ-ap-snd₂ e = Σ-ap-snd (λ a → Σ-ap-snd (e a))
+
+Σ-ap-snd₃
+  : ∀ {ℓa ℓb ℓc ℓp ℓq}
+  → {A : Type ℓa} {B : A → Type ℓb} {C : (a : A) → B a → Type ℓc}
+  → {P : (a : A) (b : B a) → C a b → Type ℓp}
+  → {Q : (a : A) (b : B a) → C a b → Type ℓq}
+  → (∀ (a : A) (b : B a) (c : C a b) → P a b c ≃ Q a b c)
+  → (Σ[ a ∈ A ] Σ[ b ∈ B a ] Σ[ c ∈ C a b ] P a b c) ≃ (Σ[ a ∈ A ] Σ[ b ∈ B a ] Σ[ c ∈ C a b ] Q a b c)
+Σ-ap-snd₃ e = Σ-ap-snd (λ a → Σ-ap-snd₂ (e a))
+```
+-->
 
 ## Paths in subtypes
 
@@ -345,3 +366,25 @@ module _ {ℓ ℓ' ℓ''} {X : Type ℓ} {Y : X → Type ℓ'} {Z : (x : X) →
   curry≃ .snd .is-eqv f .paths  = strict-fibres uncurry f .snd
 ```
 -->
+
+<!--
+```agda
+Σ-pulll
+  : ∀ {ℓa ℓb ℓc ℓx}
+  → {A : Type ℓa} {B : A → Type ℓb} {C : ∀ a → B a → Type ℓc}
+  → {X : Type ℓx}
+  → (e : (Σ[ a ∈ A ] B a) ≃ X)
+  → (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b)
+  ≃ (Σ[ x ∈ X ] C (Equiv.from e x .fst) (Equiv.from e x .snd))
+Σ-pulll e = Σ-assoc ∙e Σ-ap-fst (e e⁻¹) e⁻¹
+
+Σ-pulll3
+  : ∀ {ℓa ℓb ℓc ℓd ℓx}
+  → {A : Type ℓa} {B : A → Type ℓb} {C : ∀ a → B a → Type ℓc} {D : ∀ a b → C a b → Type ℓd}
+  → {X : Type ℓx}
+  → (e : (Σ[ a ∈ A ] Σ[ b ∈ B a ] C a b) ≃ X)
+  → (Σ[ a ∈ A ] Σ[ b ∈ B a ] Σ[ c ∈ C a b ] D a b c)
+  ≃ (Σ[ x ∈ X ] D (Equiv.from e x .fst) (Equiv.from e x .snd .fst) (Equiv.from e x .snd .snd))
+Σ-pulll3 e = Σ-ap-snd (λ _ → Σ-assoc) ∙e Σ-pulll e
+```
+-->

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

@@ -61,19 +61,17 @@ Zero-group = to-group zg where
   zg .make-group.idl x = refl
 
 Zero-group-is-initial : is-initial (Groups ℓ) Zero-group
-Zero-group-is-initial (_ , G) .centre = ∫hom (λ x → G.unit) gh where
+Zero-group-is-initial .is-initial.¡ {_ , G} = ∫hom (λ x → G.unit) gh where
   module G = Group-on G
   gh : is-group-hom _ _ (λ x → G.unit)
   gh .pres-⋆ x y =
     G.unit            ≡˘⟨ G.idl ⟩
     G.unit G.⋆ G.unit ∎
-Zero-group-is-initial (_ , G) .paths x =
-  ext λ _ → sym (is-group-hom.pres-id (x .snd))
+Zero-group-is-initial .is-initial.¡-unique f = ext λ _ → is-group-hom.pres-id (f .snd)
 
 Zero-group-is-terminal : is-terminal (Groups ℓ) Zero-group
-Zero-group-is-terminal _ .centre =
-  ∫hom (λ _ → lift tt) record { pres-⋆ = λ _ _ _ → lift tt }
-Zero-group-is-terminal _ .paths x = ext λ _ → refl
+Zero-group-is-terminal .is-terminal.! = ∫hom (λ _ → lift tt) (record { pres-⋆ = λ _ _ → refl })
+Zero-group-is-terminal .is-terminal.!-unique h = ext λ _ → refl
 
 Zero-group-is-zero : is-zero (Groups ℓ) Zero-group
 Zero-group-is-zero = record
@@ -255,7 +253,7 @@ Groups-finitely-complete = with-equalisers (Groups ℓ) top prod Groups-equalise
   where
     top : Terminal (Groups ℓ)
     top .Terminal.top = Zero-group
-    top .Terminal.has⊤ = Zero-group-is-terminal
+    top .Terminal.has-is-term = Zero-group-is-terminal
 
     prod : ∀ A B → Product (Groups ℓ) A B
     prod A B .Product.apex = Direct-product A B

src/Algebra/Quasigroup/Instances/Initial.lagda.md

@@ -51,13 +51,13 @@ of quasigroups, as there is a unique function out of the empty type.
 
 ```agda
 Empty-quasigroup-is-initial : is-initial (Quasigroups ℓ) Empty-quasigroup
-Empty-quasigroup-is-initial A .centre .fst ()
-Empty-quasigroup-is-initial A .centre .snd .is-quasigroup-hom.pres-⋆ ()
-Empty-quasigroup-is-initial A .paths f = ext λ ()
+Empty-quasigroup-is-initial .is-initial.¡ .fst ()
+Empty-quasigroup-is-initial .is-initial.¡ .snd .is-quasigroup-hom.pres-⋆ ()
+Empty-quasigroup-is-initial .is-initial.¡-unique f = ext λ ()
 
 Initial-quasigroup : Initial (Quasigroups ℓ)
 Initial-quasigroup .Initial.bot = Empty-quasigroup
-Initial-quasigroup .Initial.has⊥ = Empty-quasigroup-is-initial
+Initial-quasigroup .Initial.has-is-init = Empty-quasigroup-is-initial
 ```
 
 In fact, the empty quasigroup is a [[strict initial object]].