diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index b8d3ef7f0..039f436c8 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -833,6 +833,17 @@ is-contr→≃⊤ : is-contr A → A ≃ ⊤
is-contr→≃⊤ c = is-contr→≃ c ⊤-is-contr
```
+
+
### Strictness of the empty type
We say that an [[initial object]] is *strict* if every map into it is an
diff --git a/src/1Lab/Type/Pi.lagda.md b/src/1Lab/Type/Pi.lagda.md
index 3c19163c7..102d8a12b 100644
--- a/src/1Lab/Type/Pi.lagda.md
+++ b/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
```
+
+
+
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 ≃∎
```
-->
diff --git a/src/1Lab/Type/Sigma.lagda.md b/src/1Lab/Type/Sigma.lagda.md
index ed51d69ea..a2da01773 100644
--- a/src/1Lab/Type/Sigma.lagda.md
+++ b/src/1Lab/Type/Sigma.lagda.md
@@ -154,6 +154,27 @@ they are included for completeness.
```
+
## 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
```
-->
+
+
diff --git a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md
index 313ea90cf..4fb116815 100644
--- a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md
+++ b/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
diff --git a/src/Algebra/Quasigroup/Instances/Initial.lagda.md b/src/Algebra/Quasigroup/Instances/Initial.lagda.md
index 18511071b..4c6593fb2 100644
--- a/src/Algebra/Quasigroup/Instances/Initial.lagda.md
+++ 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]].
diff --git a/src/Algebra/Ring/Cat/Initial.lagda.md b/src/Algebra/Ring/Cat/Initial.lagda.md
index 553c89882..4979c7ef9 100644
--- a/src/Algebra/Ring/Cat/Initial.lagda.md
+++ b/src/Algebra/Ring/Cat/Initial.lagda.md
@@ -69,8 +69,9 @@ prove...], so here it is:
```agda
Int-is-initial : is-initial (Rings ℓ) Liftℤ
-Int-is-initial R = contr z→r λ x → ext (lemma x) where
- module R = Kit R
+Int-is-initial = hom-contr→is-initial λ R → contr (z→r R) λ h → ext (lemma R h) where
+ module _ (R : Ring ℓ) where
+ module R = Kit R
```
Note that we treat 1 with care: we could have this map 1 to `1r + 0r`,
@@ -79,10 +80,10 @@ embedding. This will result in a bit more work right now, but is work
worth doing.
```agda
- e : Nat → ⌞ R ⌟
- e zero = R.0r
- e (suc zero) = R.1r
- e (suc (suc x)) = R.1r R.+ e (suc x)
+ e : Nat → ⌞ R ⌟
+ e zero = R.0r
+ e (suc zero) = R.1r
+ e (suc (suc x)) = R.1r R.+ e (suc x)
```
Zero gets sent to zero, and "adding one" gets sent to adding one. Is
@@ -92,32 +93,32 @@ naturals to sums in $R$, and products of naturals to products in $R$.
We'll need this later.
```agda
- e-suc : ∀ n → e (suc n) ≡ R.1r R.+ e n
- e-add : ∀ m n → e (m Nat.+ n) ≡ e m R.+ e n
- e-mul : ∀ m n → e (m Nat.* n) ≡ e m R.* e n
+ e-suc : ∀ n → e (suc n) ≡ R.1r R.+ e n
+ e-add : ∀ m n → e (m Nat.+ n) ≡ e m R.+ e n
+ e-mul : ∀ m n → e (m Nat.* n) ≡ e m R.* e n
```
@@ -129,13 +130,13 @@ integers, i.e. we need $e(m) - e(n) = e(1 + m) - e(1 + n)$. This is
annoying to show, but not _too_ annoying:
```agda
- e-tr : ∀ m n → e m R.- e n ≡ e (suc m) R.- e (suc n)
- e-tr m n = sym $
- (e (suc m) R.- e (suc n)) ≡⟨ ap₂ R._-_ (e-suc m) (e-suc n) ⟩
- (R.1r R.+ e m) R.- (R.1r R.+ e n) ≡⟨ ap₂ R._+_ refl (R.a.inv-comm ∙ R.+-commutes) ∙ R.+-associative ⟩
- R.1r R.+ e m R.+ (R.- R.1r) R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.pullr R.+-commutes ∙ R.pulll refl) refl ⟩
- R.1r R.+ (R.- R.1r) R.+ e m R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.eliml R.+-invr) refl ⟩
- e m R.- e n ∎
+ e-tr : ∀ m n → e m R.- e n ≡ e (suc m) R.- e (suc n)
+ e-tr m n = sym $
+ (e (suc m) R.- e (suc n)) ≡⟨ ap₂ R._-_ (e-suc m) (e-suc n) ⟩
+ (R.1r R.+ e m) R.- (R.1r R.+ e n) ≡⟨ ap₂ R._+_ refl (R.a.inv-comm ∙ R.+-commutes) ∙ R.+-associative ⟩
+ R.1r R.+ e m R.+ (R.- R.1r) R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.pullr R.+-commutes ∙ R.pulll refl) refl ⟩
+ R.1r R.+ (R.- R.1r) R.+ e m R.+ (R.- e n) ≡⟨ ap₂ R._+_ (R.eliml R.+-invr) refl ⟩
+ e m R.- e n ∎
```
We can now build the embedding $\ZZ \mono R$. It remains to show that
@@ -144,58 +145,58 @@ algebra, so I won't comment on it too much: it can be worked out on
paper, following the ring laws.
```agda
- ℤ↪R : Int → ⌞ R ⌟
- ℤ↪R (pos x) = e x
- ℤ↪R (negsuc x) = R.- (e (suc x))
-
- open is-ring-hom
-
- z-nat-diff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
- z-nat-diff x zero = R.intror R.inv-unit
- z-nat-diff zero (suc y) = R.introl refl
- z-nat-diff (suc x) (suc y) = z-nat-diff x y ∙ e-tr x y
-
- z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
- z-add (pos x) (pos y) = e-add x y
- z-add (pos x) (negsuc y) = z-nat-diff x (suc y)
- z-add (negsuc x) (pos y) = z-nat-diff y (suc x) ∙ R.+-commutes
- z-add (negsuc x) (negsuc y) =
- R.- (e 1 R.+ e (suc x Nat.+ y)) ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
- R.- (e (suc x) R.+ (e 1 R.+ e y)) ≡⟨ R.a.inv-comm ⟩
- (R.- (e 1 R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩
- (R.- e (suc x)) R.+ (R.- (e 1 R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add 1 y))) ⟩
- (R.- e (suc x)) R.+ (R.- e (1 Nat.+ y)) ∎
-
- z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
- z-mul (pos x) (pos y) =
- ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩
- e (x Nat.* y) ≡⟨ e-mul x y ⟩
- (e x R.* e y) ∎
- z-mul (posz) (negsuc y) = sym R.*-zerol
- z-mul (possuc x) (negsuc y) =
- R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
- R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩
- e (suc x) R.* (R.- e (suc y)) ∎
- z-mul (negsuc x) (posz) =
- ℤ↪R (assign neg (x Nat.* 0)) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩
- ℤ↪R 0 ≡⟨ sym R.*-zeror ⟩
- ℤ↪R (negsuc x) R.* R.0r ∎
- z-mul (negsuc x) (possuc y) =
- R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
- R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩
- (R.- e (suc x)) R.* e (suc y) ∎
- z-mul (negsuc x) (negsuc y) =
- e (suc x Nat.* suc y) ≡⟨ e-mul (suc x) (suc y) ⟩
- e (suc x) R.* e (suc y) ≡˘⟨ R.inv-inv ⟩
- R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩
- R.- (e (suc x) R.* ℤ↪R (negsuc y)) ≡˘⟨ R.*-negatel ⟩
- ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y) ∎
-
- z→r : Rings.Hom Liftℤ R
- z→r .fst (lift x) = ℤ↪R x
- z→r .snd .pres-id = refl
- z→r .snd .pres-+ (lift x) (lift y) = z-add x y
- z→r .snd .pres-* (lift x) (lift y) = z-mul x y
+ ℤ↪R : Int → ⌞ R ⌟
+ ℤ↪R (pos x) = e x
+ ℤ↪R (negsuc x) = R.- (e (suc x))
+
+ open is-ring-hom
+
+ z-nat-diff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
+ z-nat-diff x zero = R.intror R.inv-unit
+ z-nat-diff zero (suc y) = R.introl refl
+ z-nat-diff (suc x) (suc y) = z-nat-diff x y ∙ e-tr x y
+
+ z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
+ z-add (pos x) (pos y) = e-add x y
+ z-add (pos x) (negsuc y) = z-nat-diff x (suc y)
+ z-add (negsuc x) (pos y) = z-nat-diff y (suc x) ∙ R.+-commutes
+ z-add (negsuc x) (negsuc y) =
+ R.- (e 1 R.+ e (suc x Nat.+ y)) ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
+ R.- (e (suc x) R.+ (e 1 R.+ e y)) ≡⟨ R.a.inv-comm ⟩
+ (R.- (e 1 R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩
+ (R.- e (suc x)) R.+ (R.- (e 1 R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add 1 y))) ⟩
+ (R.- e (suc x)) R.+ (R.- e (1 Nat.+ y)) ∎
+
+ z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
+ z-mul (pos x) (pos y) =
+ ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩
+ e (x Nat.* y) ≡⟨ e-mul x y ⟩
+ (e x R.* e y) ∎
+ z-mul (posz) (negsuc y) = sym R.*-zerol
+ z-mul (possuc x) (negsuc y) =
+ R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
+ R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩
+ e (suc x) R.* (R.- e (suc y)) ∎
+ z-mul (negsuc x) (posz) =
+ ℤ↪R (assign neg (x Nat.* 0)) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩
+ ℤ↪R 0 ≡⟨ sym R.*-zeror ⟩
+ ℤ↪R (negsuc x) R.* R.0r ∎
+ z-mul (negsuc x) (possuc y) =
+ R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
+ R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩
+ (R.- e (suc x)) R.* e (suc y) ∎
+ z-mul (negsuc x) (negsuc y) =
+ e (suc x Nat.* suc y) ≡⟨ e-mul (suc x) (suc y) ⟩
+ e (suc x) R.* e (suc y) ≡˘⟨ R.inv-inv ⟩
+ R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩
+ R.- (e (suc x) R.* ℤ↪R (negsuc y)) ≡˘⟨ R.*-negatel ⟩
+ ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y) ∎
+
+ z→r : Rings.Hom Liftℤ R
+ z→r .fst (lift x) = ℤ↪R x
+ z→r .snd .pres-id = refl
+ z→r .snd .pres-+ (lift x) (lift y) = z-add x y
+ z→r .snd .pres-* (lift x) (lift y) = z-mul x y
```
The last thing we must show is that this is the _unique_ ring
@@ -215,14 +216,14 @@ and that last expression is pretty exactly what our canonical map
evaluates to on $n$. So we're done!
```agda
- module _ (f : Rings.Hom Liftℤ R) where
- private module f = is-ring-hom (f .snd)
+ module _ (f : Rings.Hom Liftℤ R) where
+ private module f = is-ring-hom (f .snd)
- f-pos : ∀ x → e x ≡ f · lift (pos x)
- f-pos zero = sym f.pres-0
- f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
+ f-pos : ∀ x → e x ≡ f · lift (pos x)
+ f-pos zero = sym f.pres-0
+ f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
- lemma : ∀ i → z→r · lift i ≡ f · lift i
- lemma (pos x) = f-pos x
- lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
+ lemma : ∀ i → z→r · lift i ≡ f · lift i
+ lemma (pos x) = f-pos x
+ lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
```
diff --git a/src/Algebra/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md
index 97967c986..9d9cf7757 100644
--- a/src/Algebra/Ring/Module/Action.lagda.md
+++ b/src/Algebra/Ring/Module/Action.lagda.md
@@ -8,6 +8,7 @@ open import Algebra.Group
open import Algebra.Ring
open import Cat.Displayed.Univalence.Thin
+open import Cat.Diagram.Initial
open import Cat.Abelian.Base
open import Cat.Abelian.Endo
open import Cat.Prelude hiding (_+_)
@@ -125,5 +126,7 @@ former!
```agda
ℤ-module-unique : ∀ {ℓ} (G : Abelian-group ℓ) → is-contr (Ring-action Liftℤ (G .snd))
-ℤ-module-unique G = Equiv→is-hlevel 0 (Action≃Hom Liftℤ G) (Int-is-initial _)
+ℤ-module-unique G =
+ Equiv→is-hlevel 0 (Action≃Hom Liftℤ G)
+ $ is-initial→hom-contr Int-is-initial _
```
diff --git a/src/Algebra/Ring/Module/Category.lagda.md b/src/Algebra/Ring/Module/Category.lagda.md
index aa179cce7..b8b769a9d 100644
--- a/src/Algebra/Ring/Module/Category.lagda.md
+++ b/src/Algebra/Ring/Module/Category.lagda.md
@@ -209,9 +209,9 @@ R-Mod-is-additive .has-terminal = term where
term : Terminal (R-Mod R _)
term .Terminal.top = ∅ᴹ
- term .Terminal.has⊤ x .centre .fst _ = lift tt
- term .Terminal.has⊤ x .centre .snd .linear r s t = refl
- term .Terminal.has⊤ x .paths r = ext λ _ → refl
+ term .Terminal.has-is-term .is-terminal.! .fst _ = lift tt
+ term .Terminal.has-is-term .is-terminal.! .snd .linear r s t = refl
+ term .Terminal.has-is-term .is-terminal.!-unique r = ext λ _ → refl
```
For the direct products, on the other hand, we have to do a bit more
diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda
index a94d1d5e7..63f744ffc 100644
--- a/src/Algebra/Ring/Solver.agda
+++ b/src/Algebra/Ring/Solver.agda
@@ -19,6 +19,7 @@ open import Algebra.Group.Ab
open import Algebra.Group
open import Algebra.Ring
+open import Cat.Diagram.Initial
open import Cat.Displayed.Total
open import Cat.Prelude hiding (_+_ ; _*_ ; _-_)
@@ -38,13 +39,14 @@ open ∫Hom
module Algebra.Ring.Solver where
module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
+ open is-initial
private
R' : Ring _
R' = record { fst = el _ (CRing-on.has-is-set cring) ; snd = CRing-on.has-ring-on cring }
module R = Kit R'
- ℤ↪R-rh = Int-is-initial R' .centre
+ ℤ↪R-rh = Int-is-initial .¡ {R'}
module ℤ↪R = is-ring-hom (ℤ↪R-rh .snd)
open CRing-on cring using (*-commutes)
@@ -56,7 +58,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
: {h' : Int → R}
→ is-ring-hom (Liftℤ {ℓ} .snd) (R' .snd) (h' ⊙ lower)
→ ∀ x → embed-coe x ≡ h' x
- embed-lemma p x = Int-is-initial R' .paths (∫hom _ p) ·ₚ lift x
+ embed-lemma p x = sym $ Int-is-initial .¡-unique (∫hom _ p) ·ₚ lift x
data Poly : Nat → Type ℓ
data Normal : Nat → Type ℓ
diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md
index cc05edd09..e0652cc6f 100644
--- a/src/Cat/Abelian/Base.lagda.md
+++ b/src/Cat/Abelian/Base.lagda.md
@@ -10,6 +10,7 @@ open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Biproduct
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Terminal
+open import Cat.Diagram.Initial
open import Cat.Diagram.Product
open import Cat.Displayed.Total
open import Cat.Instances.Slice
@@ -151,16 +152,21 @@ module _ {o ℓ} {C : Precategory o ℓ} (A : Ab-category C) where
private module A = Ab-category A
id-zero→zero : ∀ {X} → A.id {X} ≡ A.0m → is-zero C X
- id-zero→zero idm .is-zero.has-is-initial B = contr A.0m λ h → sym $
- h ≡⟨ A.intror refl ⟩
- h A.∘ A.id ≡⟨ A.refl⟩∘⟨ idm ⟩
- h A.∘ A.0m ≡⟨ A.∘-zero-r ⟩
- A.0m ∎
- id-zero→zero idm .is-zero.has-is-terminal x = contr A.0m λ h → sym $
- h ≡⟨ A.introl refl ⟩
- A.id A.∘ h ≡⟨ idm A.⟩∘⟨refl ⟩
- A.0m A.∘ h ≡⟨ A.∘-zero-l ⟩
- A.0m ∎
+ {-# INLINE id-zero→zero #-}
+ id-zero→zero idm = to-is-zero $ record
+ { ! = A.0m
+ ; ¡ = A.0m
+ ; !-unique = λ h →
+ h ≡⟨ A.introl refl ⟩
+ A.id A.∘ h ≡⟨ idm A.⟩∘⟨refl ⟩
+ A.0m A.∘ h ≡⟨ A.∘-zero-l ⟩
+ A.0m ∎
+ ; ¡-unique = λ h →
+ h ≡⟨ A.intror refl ⟩
+ h A.∘ A.id ≡⟨ A.refl⟩∘⟨ idm ⟩
+ h A.∘ A.0m ≡⟨ A.∘-zero-r ⟩
+ A.0m ∎
+ }
```
Perhaps the simplest example of an $\Ab$-category is.. any ring! In the
@@ -199,11 +205,11 @@ record is-additive {o ℓ} (C : Precategory o ℓ) : Type (o ⊔ lsuc ℓ) where
∅ : Zero C
∅ .Zero.∅ = has-terminal .Terminal.top
∅ .Zero.has-is-zero = id-zero→zero has-ab $
- is-contr→is-prop (has-terminal .Terminal.has⊤ _) _ _
+ Terminal.!-unique₂ has-terminal id 0m
module ∅ = Zero ∅
0m-unique : ∀ {A B} → ∅.zero→ {A} {B} ≡ 0m
- 0m-unique = ap₂ _∘_ (∅.has⊥ _ .paths _) refl ∙ ∘-zero-l
+ 0m-unique = ap₂ _∘_ (∅.¡-unique _) refl ∙ ∘-zero-l
```
Coincidence of finite products and finite coproducts leads to an object
@@ -411,7 +417,7 @@ monomorphism].
path : f ∘ kernel f .Kernel.kernel ≡ f ∘ 0m
path = Ker.equal f
∙∙ ∅.zero-∘r _
- ∙∙ ap₂ _∘_ (∅.has⊥ _ .paths 0m) refl
+ ∙∙ ap₂ _∘_ (sym $ ∅.¡-unique 0m) refl
∙∙ ∘-zero-l ∙∙ sym ∘-zero-r
```
-->
@@ -432,8 +438,7 @@ the canonical subobject inclusion $\ker(f) \to B$.
path : ∅.zero→ ∘ proj' ≡ Coker.coeq f ∘ proj'
path = Coker.unique₂ (Ker.kernel f)
{e' = 0m} (∘-zero-r ∙ sym ∘-zero-l)
- (pushl (∅.zero-∘r _) ∙ pulll ( ap₂ _∘_ refl (∅.has⊤ _ .paths 0m)
- ∙ ∘-zero-r)
+ (pushl (∅.zero-∘r _) ∙ pulll (∘-zero-r)
∙ ∘-zero-l)
(pullr (Coker.factors (Ker.kernel f)) ∙ sym (Coker.coequal _)
∙ ∘-zero-r)
diff --git a/src/Cat/Abelian/Functor.lagda.md b/src/Cat/Abelian/Functor.lagda.md
index e60d17823..06d474fe5 100644
--- a/src/Cat/Abelian/Functor.lagda.md
+++ b/src/Cat/Abelian/Functor.lagda.md
@@ -86,7 +86,7 @@ Ab-functor-pres-∅
Ab-functor-pres-∅ {A = A} {B = B} F ∅A =
id-zero→zero B $
B.id ≡˘⟨ F.F-id ⟩
- F.₁ A.id ≡⟨ ap F.₁ (is-contr→is-prop (Zero.has⊤ ∅A (Zero.∅ ∅A)) _ _) ⟩
+ F.₁ A.id ≡⟨ ap F.₁ (Zero.!-unique₂ ∅A A.id A.0m) ⟩
F.₁ A.0m ≡⟨ F.F-0m ⟩
B.0m ∎
where
diff --git a/src/Cat/Abelian/Images.lagda.md b/src/Cat/Abelian/Images.lagda.md
index 30544a7a5..778a0ba66 100644
--- a/src/Cat/Abelian/Images.lagda.md
+++ b/src/Cat/Abelian/Images.lagda.md
@@ -111,12 +111,13 @@ commutes.
```agda
im : Image C f
im .Initial.bot = the-img
- im .Initial.has⊥ other = contr factor unique where
- factor : ↓Hom (!Const (cut f)) Forget-full-subcat the-img other
- factor .top = tt
- factor .bot ./-Hom.map =
- Coker.universal (Ker.kernel f) {e' = other .map .map} path
- ∘ coker-ker≃ker-coker f .is-invertible.inv
+ im .Initial.has-is-init = hom-contr→is-initial (λ other → contr (factor other) (unique other)) where
+ module _ (other : ↓Obj (!Const (cut f)) Forget-full-subcat) where
+ factor : ↓Hom (!Const (cut f)) Forget-full-subcat the-img other
+ factor .top = tt
+ factor .bot ./-Hom.map =
+ Coker.universal (Ker.kernel f) {e' = other .map .map} path
+ ∘ coker-ker≃ker-coker f .is-invertible.inv
```
Observe that by the universal property of $\coker (\ker f)$^[hence of
@@ -125,14 +126,14 @@ we have a map $q : A \to X$ such that $0 = q\ker f$, then we can obtain
a (unique) map $\coker (\ker f) \to X$ s.t. the triangle above commutes!
```agda
- where abstract
- path : other .map .map ∘ 0m ≡ other .map .map ∘ kernel f .Kernel.kernel
- path = other .cod .snd _ _ $ sym $
- pulll (other .map .com)
- ∙∙ Ker.equal f
- ∙∙ ∅.zero-∘r _
- ∙∙ 0m-unique
- ∙∙ sym (ap₂ _∘_ refl ∘-zero-r ∙ ∘-zero-r)
+ where abstract
+ path : other .map .map ∘ 0m ≡ other .map .map ∘ kernel f .Kernel.kernel
+ path = other .cod .snd _ _ $ sym $
+ pulll (other .map .com)
+ ∙∙ Ker.equal f
+ ∙∙ ∅.zero-∘r _
+ ∙∙ 0m-unique
+ ∙∙ sym (ap₂ _∘_ refl ∘-zero-r ∙ ∘-zero-r)
```
To satisfy that equation, observe that since $i'$ is monic, it suffices
@@ -145,22 +146,22 @@ is the image of $f$.
Here's the tedious isomorphism algebra.
```agda
- factor .bot ./-Hom.com = invertible→epic (coker-ker≃ker-coker f) _ _ $
- Coker.unique₂ (Ker.kernel f)
- (sym (Ker.equal f ∙ ∅.zero-∘r _ ∙ 0m-unique ∙ sym ∘-zero-r))
- (ap₂ _∘_ ( sym (assoc _ _ _)
- ∙ ap₂ _∘_ refl (cancelr
- (coker-ker≃ker-coker f .is-invertible.invr))) refl
- ∙ pullr (Coker.factors _) ∙ other .map .com)
- (sym (decompose f .snd ∙ assoc _ _ _))
- factor .com = /-Hom-path $ sym $ other .cod .snd _ _ $
- pulll (factor .bot .com)
- ∙ the-img .map .com
- ∙∙ sym (other .map .com)
- ∙∙ ap (other .cod .fst .map ∘_) (intror refl)
-
- unique : ∀ x → factor ≡ x
- unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .cod .snd _ _ $
- sym (x .bot .com ∙ sym (factor .bot .com))
+ factor .bot ./-Hom.com = invertible→epic (coker-ker≃ker-coker f) _ _ $
+ Coker.unique₂ (Ker.kernel f)
+ (sym (Ker.equal f ∙ ∅.zero-∘r _ ∙ 0m-unique ∙ sym ∘-zero-r))
+ (ap₂ _∘_ ( sym (assoc _ _ _)
+ ∙ ap₂ _∘_ refl (cancelr
+ (coker-ker≃ker-coker f .is-invertible.invr))) refl
+ ∙ pullr (Coker.factors _) ∙ other .map .com)
+ (sym (decompose f .snd ∙ assoc _ _ _))
+ factor .com = /-Hom-path $ sym $ other .cod .snd _ _ $
+ pulll (factor .bot .com)
+ ∙ the-img .map .com
+ ∙∙ sym (other .map .com)
+ ∙∙ ap (other .cod .fst .map ∘_) (intror refl)
+
+ unique : ∀ x → factor ≡ x
+ unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .cod .snd _ _ $
+ sym (x .bot .com ∙ sym (factor .bot .com))
```
diff --git a/src/Cat/Abelian/Instances/Ab.lagda.md b/src/Cat/Abelian/Instances/Ab.lagda.md
index 108336f53..29209b96e 100644
--- a/src/Cat/Abelian/Instances/Ab.lagda.md
+++ b/src/Cat/Abelian/Instances/Ab.lagda.md
@@ -49,9 +49,9 @@ direct sums.
Ab-is-additive : is-additive (Ab ℓ)
Ab-is-additive .has-ab = Ab-ab-category
Ab-is-additive .has-terminal .top = from-commutative-group (Zero-group {ℓ}) (λ x y → refl)
-Ab-is-additive .has-terminal .has⊤ x =
- contr (∫hom (λ _ → lift tt) (record { pres-⋆ = λ x y i → lift tt }))
- λ x → ext λ _ → refl
+Ab-is-additive .has-terminal .has-is-term .is-terminal.! .fst _ = lift tt
+Ab-is-additive .has-terminal .has-is-term .is-terminal.! .snd = record { pres-⋆ = λ _ _ → refl }
+Ab-is-additive .has-terminal .has-is-term .is-terminal.!-unique h = ext λ _ → refl
Ab-is-additive .has-prods A B .apex = A ⊕ B
Ab-is-additive .has-prods A B .π₁ = _
diff --git a/src/Cat/Cartesian.lagda.md b/src/Cat/Cartesian.lagda.md
index 4435bffe8..0eee626e6 100644
--- a/src/Cat/Cartesian.lagda.md
+++ b/src/Cat/Cartesian.lagda.md
@@ -75,12 +75,16 @@ comparison map is an isomorphism.
record Cartesian-functor : Type (o ⊔ o' ⊔ ℓ ⊔ ℓ') where
field
pres-products : ∀ a b → D.is-invertible (product-comparison a b)
- pres-terminal : is-terminal D (F.₀ C.top)
+ pres-terminal : D.is-invertible (D.! {F.₀ C.top})
image-is-product
: ∀ {a b} → is-product D {A = F.₀ a} {B = F.₀ b} (F.₁ C.π₁) (F.₁ C.π₂)
image-is-product = is-product-iso-apex (pres-products _ _)
D.π₁∘⟨⟩ D.π₂∘⟨⟩ D.has-is-product
+
+ image-is-terminal
+ : is-terminal D (F.₀ C.top)
+ image-is-terminal = !-invertible→is-terminal D.has-is-term pres-terminal
```
@@ -13,7 +13,7 @@ module Cat.Diagram.Initial where
@@ -23,30 +23,89 @@ An object $\bot$ of a category $\mathcal{C}$ is said to be **initial**
if there exists a _unique_ map to any other object:
```agda
- is-initial : Ob → Type _
- is-initial ob = ∀ x → is-contr (Hom ob x)
+ record is-initial (bot : Ob) : Type (o ⊔ h) where
+ no-eta-equality
+ field
+ ¡ : ∀ {x} → Hom bot x
+ ¡-unique : ∀ {x} (h : Hom bot x) → h ≡ ¡
+
+ ¡-unique₂ : ∀ {x} (f g : Hom bot x) → f ≡ g
+ ¡-unique₂ f g = ¡-unique f ∙ sym (¡-unique g)
record Initial : Type (o ⊔ h) where
+ no-eta-equality
field
bot : Ob
- has⊥ : is-initial bot
-```
+ has-is-init : is-initial bot
-We refer to the centre of contraction as `¡`{.Agda}. Since it inhabits a
-contractible type, it is unique.
+ open is-initial has-is-init public
+```
+
## Intuition
@@ -68,13 +127,38 @@ like a notion of **Syntax** for our category. The idea here is that we
have a _unique_ means of interpreting our syntax into any other object,
which is exhibited by the universal map `¡`{.Agda}
+## Universal property
+
+An object $b : \cC$ is initial if and only if the type of morphisms
+$\cC(b, x)$ is [[contractible]] for every $x : \cC$.
+
+```agda
+ hom-contr→is-initial
+ : ∀ {b}
+ → (∀ x → is-contr (Hom b x))
+ → is-initial C b
+ {-# INLINE hom-contr→is-initial #-}
+ hom-contr→is-initial hom-contr = record
+ { ¡ = λ {x} → hom-contr x .centre
+ ; ¡-unique = λ {x} h → sym (hom-contr x .paths h)
+ }
+
+ is-initial→hom-contr
+ : ∀ {b}
+ → is-initial C b
+ → ∀ x → is-contr (Hom b x)
+ is-initial→hom-contr b-init x = contr b.¡ λ h → sym (b.¡-unique h)
+ where module b = is-initial b-init
+```
+
+
## Uniqueness
One important fact about initial objects is that they are **unique** up
to isomorphism:
```agda
- ⊥-unique : (i i' : Initial) → bot i ≅ bot i'
+ ⊥-unique : (i i' : Initial C) → bot i ≅ bot i'
⊥-unique i i' = make-iso (¡ i) (¡ i') (¡-unique₂ i' _ _) (¡-unique₂ i _ _)
```
@@ -82,31 +166,6 @@ Additionally, if $C$ is a category, then the space of initial objects is
a proposition:
```agda
- ⊥-is-prop : is-category C → is-prop Initial
- ⊥-is-prop ccat x1 x2 i .bot =
- Univalent.iso→path ccat (⊥-unique x1 x2) i
-
- ⊥-is-prop ccat x1 x2 i .has⊥ ob =
- is-prop→pathp
- (λ i → is-contr-is-prop
- {A = Hom (Univalent.iso→path ccat (⊥-unique x1 x2) i) _})
- (x1 .has⊥ ob) (x2 .has⊥ ob) i
+ ⊥-is-prop : is-category C → is-prop (Initial C)
+ ⊥-is-prop ccat x1 x2 = ext (Univalent.iso→path ccat (⊥-unique x1 x2))
```
-
-
diff --git a/src/Cat/Diagram/Initial/Weak.lagda.md b/src/Cat/Diagram/Initial/Weak.lagda.md
index b2fe55024..44f5f11b0 100644
--- a/src/Cat/Diagram/Initial/Weak.lagda.md
+++ b/src/Cat/Diagram/Initial/Weak.lagda.md
@@ -76,7 +76,8 @@ the joint equaliser $i : L \to X$ of all arrows $X \to X$ is an initial object.
→ is-joint-equaliser C {I = Hom X X} (λ x → x) l
→ has-equalisers C
→ is-initial C L
- is-weak-initial→equaliser X {L} {i} is-wi lim eqs y = contr cen (p' _) where
+ {-# INLINE is-weak-initial→equaliser #-}
+ is-weak-initial→equaliser X {L} {i} is-wi lim eqs = L-initial where
open is-joint-equaliser lim
```
@@ -86,7 +87,7 @@ arrows $f, g : L \to Y$, consider their equaliser $j : E \to L$. First,
we have some arrow $k : X \to E$.
```agda
- p' : is-prop (Hom L y)
+ p' : ∀ {y} → is-prop (Hom L y)
p' f g = ∥-∥-out! do
let
module fg = Equaliser (eqs f g)
@@ -124,8 +125,12 @@ since $j$ equalises $f$ and $g$ by construction, we have $f = g$!
pure (s f g fg.equal)
- cen : Hom L y
- cen = ∥-∥-out p' ((_∘ i) <$> is-wi y)
+ cen : ∀ {y} → Hom L y
+ cen {y} = ∥-∥-out p' ((_∘ i) <$> is-wi y)
+
+ L-initial : is-initial C L
+ {-# INLINE L-initial #-}
+ L-initial = hom-contr→is-initial λ y → is-prop∙→is-contr p' cen
```
Putting this together, we can show that, if a [[complete category]] has
@@ -138,7 +143,7 @@ a small weakly initial family, then it has an initial object.
→ is-weak-initial-fam F
→ Initial C
is-complete-weak-initial→initial {κ = κ} {I} F compl wif =
- record { has⊥ = equal-is-initial } where
+ record { has-is-init = equal-is-initial } where
```
diff --git a/src/Cat/Diagram/Limit/Cone.lagda.md b/src/Cat/Diagram/Limit/Cone.lagda.md
index 33347067e..2579356a0 100644
--- a/src/Cat/Diagram/Limit/Cone.lagda.md
+++ b/src/Cat/Diagram/Limit/Cone.lagda.md
@@ -190,6 +190,7 @@ differently.
→ is-terminal Cones K
→ is-limit F (Cone.apex K) (Cone→cone K)
is-terminal-cone→is-limit {K = K} term = isl where
+ open is-terminal term
open Cone-hom
open is-ran
open Cone
@@ -202,10 +203,10 @@ differently.
α' .commutes f = sym (α .is-natural _ _ f) ∙ C.elimr (M .Functor.F-id)
nt : M => !Const (K .apex)
- nt .η x = term α' .centre .map
+ nt .η x = ! {α'} .map
nt .is-natural tt tt tt = C.elimr (M .Functor.F-id) ∙ C.introl refl
- isl .σ-comm = ext λ x → term _ .centre .com _
- isl .σ-uniq {σ' = σ'} x = ext λ _ → ap map $ term _ .paths λ where
+ isl .σ-comm = ext λ x → ! .com x
+ isl .σ-uniq {σ' = σ'} x = ext λ _ → ap map $ sym $ !-unique λ where
.map → σ' .η _
.com _ → sym (x ηₚ _)
```
@@ -218,16 +219,18 @@ unpacking data.
: ∀ {x} {eps : Const x => F}
→ (L : is-limit F x eps)
→ is-terminal Cones (record { commutes = is-limit.commutes L })
- is-limit→is-terminal-cone {x = x} L K = term where
+ {-# INLINE is-limit→is-terminal-cone #-}
+ is-limit→is-terminal-cone {x = x} L = term where
module L = is-limit L
- module K = Cone K
open Cone-hom
+ open Cone
- term : is-contr (Cone-hom K _)
- term .centre .map = L.universal K.ψ K.commutes
- term .centre .com _ = L.factors K.ψ K.commutes
- term .paths f =
- Cone-hom-path (sym (L.unique K.ψ K.commutes (f .map) (f .com)))
+ term : is-terminal Cones (record { commutes = is-limit.commutes L })
+ {-# INLINE term #-}
+ term = record
+ { ! = λ {K} → cone-hom (L.universal (K .ψ) (K .commutes)) (λ _ → L.factors _ _)
+ ; !-unique = λ {K} h → Cone-hom-path (L.unique (K .ψ) (K .commutes) (h .map) (h .com))
+ }
```
diff --git a/src/Cat/Diagram/Limit/Finite.lagda.md b/src/Cat/Diagram/Limit/Finite.lagda.md
index 37dd1de2e..6fc06fc9d 100644
--- a/src/Cat/Diagram/Limit/Finite.lagda.md
+++ b/src/Cat/Diagram/Limit/Finite.lagda.md
@@ -3,6 +3,7 @@
open import Cat.Diagram.Pullback.Properties
open import Cat.Instances.Shape.Parallel
open import Cat.Diagram.Limit.Equaliser
+open import Cat.Instances.Shape.Initial
open import Cat.Diagram.Limit.Pullback
open import Cat.Diagram.Limit.Terminal
open import Cat.Diagram.Product.Finite
@@ -106,10 +107,10 @@ products).
: is-finitely-complete → Finitely-complete
is-finitely-complete→Finitely-complete flim = Flim where
Flim : Finitely-complete
- Flim .terminal = Limit→Terminal C (flim finite-cat _)
+ Flim .terminal = Limit→Terminal C ¡F (flim finite-cat _)
Flim .products a b = Limit→Product C (flim Disc-finite _)
Flim .equalisers f g = Limit→Equaliser C (flim ·⇉·-finite _)
- Flim .pullbacks f g = Limit→Pullback C {lzero} {lzero} (flim ·→·←·-finite _)
+ Flim .pullbacks f g = Limit→Pullback C (cospan→cospan-diagram lzero lzero f g) (flim ·→·←·-finite _)
```
## With equalisers
@@ -275,7 +276,7 @@ object $*$.
prod : is-product C p1 p2
prod .is-product.⟨_,_⟩ p1' p2' =
- Pb.universal {p₁' = p1'} {p₂' = p2'} (is-contr→is-prop (term _) _ _)
+ Pb.universal (is-terminal.!-unique₂ term (f ∘ p1') (g ∘ p2'))
prod .is-product.π₁∘⟨⟩ = Pb.p₁∘universal
prod .is-product.π₂∘⟨⟩ = Pb.p₂∘universal
prod .is-product.unique p q = Pb.unique p q
@@ -287,8 +288,8 @@ object $*$.
with-pullbacks top pb = fc where
module top = Terminal top
mkprod : ∀ A B → Product C A B
- mkprod A B = record { has-is-product = terminal-pullback→product top.has⊤ pb' }
- where pb' = pb (top.has⊤ A .centre) (top.has⊤ B .centre) .Pullback.has-is-pb
+ mkprod A B = record { has-is-product = terminal-pullback→product top.has-is-term pb' }
+ where pb' = pb (top.!) (top.!) .Pullback.has-is-pb
mkeq : ∀ {A B} (f g : Hom A B) → Equaliser C f g
mkeq {A = A} {B} f g = eq where
@@ -427,9 +428,10 @@ Putting it all together into a record we get our proof of finite completeness:
: ∀ {P X Y T} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X T} {g : Hom Y T}
→ is-terminal C T → is-product C p1 p2 → is-pullback C p1 f p2 g
product→terminal-pullback t r = pb where
+ open is-terminal t
open is-pullback
pb : is-pullback C _ _ _ _
- pb .square = is-contr→is-prop (t _) _ _
+ pb .square = !-unique₂ _ _
pb .universal _ = r .is-product.⟨_,_⟩ _ _
pb .p₁∘universal = r .is-product.π₁∘⟨⟩
pb .p₂∘universal = r .is-product.π₂∘⟨⟩
@@ -440,29 +442,10 @@ Putting it all together into a record we get our proof of finite completeness:
is-complete→finitely {a} {b} compl = with-pullbacks term' pb
where
pb : ∀ {x y z} (f : Hom x z) (g : Hom y z) → Pullback C f g
- pb f g = Limit→Pullback C (compl (cospan→cospan-diagram _ _ f g))
-
- idx : Precategory a b
- idx = Lift-cat a b (Disc ⊥ λ x → absurd x)
-
- F : Functor idx C
- F .Functor.F₀ ()
- F .Functor.F₁ {()}
- F .Functor.F-id {()}
- F .Functor.F-∘ {()}
-
- limF : Limit F
- limF = compl F
- open Terminal
- open Cone-hom
- open Cone
+ pb f g = Limit→Pullback C _ (compl (cospan→cospan-diagram _ _ f g))
term' : Terminal C
- term' = record { top = Limit.apex limF ; has⊤ = limiting } where
- limiting : ∀ x → is-contr _
- limiting x =
- contr (Limit.universal limF (λ { () }) (λ { {()} })) λ h →
- sym (Limit.unique limF _ _ h λ { () })
+ term' = Limit→Terminal C ¡F (is-complete-lower a b lzero lzero compl ¡F)
```
-->
@@ -507,8 +490,9 @@ products.
→ is-product C p1 p2
→ is-product D (F.₁ p1) (F.₁ p2)
pres-product term pr = terminal-pullback→product D (pres-⊤ term)
- (pres-pullback {f = term _ .centre} {g = term _ .centre}
+ (pres-pullback {f = !} {g = !}
(product→terminal-pullback C term pr))
+ where open is-terminal term
```
Since $f : A \to B$ being a monomorphism is equivalent to certain squares
diff --git a/src/Cat/Diagram/Limit/Initial.lagda.md b/src/Cat/Diagram/Limit/Initial.lagda.md
index 0dbd3780f..f7d8cf27a 100644
--- a/src/Cat/Diagram/Limit/Initial.lagda.md
+++ b/src/Cat/Diagram/Limit/Initial.lagda.md
@@ -43,9 +43,8 @@ module _ {o ℓ} {C : Precategory o ℓ} (L : Limit (Id {C = C})) where
Id-limit→Initial : Initial C
Id-limit→Initial .bot = L.apex
- Id-limit→Initial .has⊥ x = λ where
- .centre → L.ψ x
- .paths h → sym (intror rem₁ ∙ L.commutes h)
+ Id-limit→Initial .has-is-init .is-initial.¡ {x} = L.ψ x
+ Id-limit→Initial .has-is-init .is-initial.¡-unique h = intror rem₁ ∙ L.commutes h
```
```agda
-module Cat.Diagram.Limit.Pullback {o h} (Cat : Precategory o h) where
+module Cat.Diagram.Limit.Pullback {oc ℓc} (C : Precategory oc ℓc) where
```
We establish the correspondence between `Pullback`{.Agda} and the
@@ -18,11 +18,10 @@ We establish the correspondence between `Pullback`{.Agda} and the
diff --git a/src/Cat/Diagram/Product/Finite.lagda.md b/src/Cat/Diagram/Product/Finite.lagda.md
index a486b9c58..36de9527c 100644
--- a/src/Cat/Diagram/Product/Finite.lagda.md
+++ b/src/Cat/Diagram/Product/Finite.lagda.md
@@ -83,7 +83,7 @@ Cartesian→standard-finite-products F = prod where
: ∀ {Y} {n} (F : Fin n → Ob) (f : (i : Fin n) → Hom Y (F i))
→ {h : Hom Y (F-apex F)} → ((i : Fin n) → F-pi F i ∘ h ≡ f i)
→ h ≡ F-mult F f
- F-unique {n = zero} F f {h} p = sym $ !-unique terminal _
+ F-unique {n = zero} F f {h} p = !-unique terminal _
F-unique {n = suc zero} F f {h} p = sym (idl h) ∙ p fzero
F-unique {n = suc (suc n)} F f {h} p =
products _ _ .unique (p fzero)
diff --git a/src/Cat/Diagram/Subterminal.lagda.md b/src/Cat/Diagram/Subterminal.lagda.md
index 48a888f4a..e0bbee99a 100644
--- a/src/Cat/Diagram/Subterminal.lagda.md
+++ b/src/Cat/Diagram/Subterminal.lagda.md
@@ -38,7 +38,7 @@ In particular, every terminal object is subterminal.
```agda
terminal→subterminal : ∀ {T} → is-terminal C T → is-subterminal T
- terminal→subterminal term X = is-contr→is-prop (term X)
+ terminal→subterminal term X = is-terminal.!-unique₂ term
```
Subterminal objects can be thought of as the interpretations of *truth
diff --git a/src/Cat/Diagram/Terminal.lagda.md b/src/Cat/Diagram/Terminal.lagda.md
index 5ab24f830..1e6ee2ec9 100644
--- a/src/Cat/Diagram/Terminal.lagda.md
+++ b/src/Cat/Diagram/Terminal.lagda.md
@@ -26,30 +26,154 @@ An object $\top$ of a category $\mathcal{C}$ is said to be **terminal**
if it admits a _unique_ map from any other object:
```agda
- is-terminal : Ob → Type _
- is-terminal ob = ∀ x → is-contr (Hom x ob)
+ record is-terminal (t : Ob) : Type (o ⊔ h) where
+ no-eta-equality
+ field
+ ! : ∀ {x} → Hom x t
+ !-unique : ∀ {x} (h : Hom x t) → h ≡ !
+
+ !-unique₂ : ∀ {x} (f g : Hom x t) → f ≡ g
+ !-unique₂ f g = !-unique f ∙ sym (!-unique g)
record Terminal : Type (o ⊔ h) where
+ no-eta-equality
field
top : Ob
- has⊤ : is-terminal top
-```
+ has-is-term : is-terminal top
-We refer to the centre of contraction as `!`{.Agda}. Since it inhabits a
-contractible type, it is unique.
+ open is-terminal has-is-term public
+```
+
+## Universal property
+
+
+
+If the type of morphisms into an object $t : \cC$ is [[contractible]],
+then $t$ must be a terminal object.
+
+```agda
+ hom-contr→is-terminal
+ : ∀ {t}
+ → (∀ x → is-contr (Hom x t))
+ → is-terminal C t
+ {-# INLINE hom-contr→is-terminal #-}
+ hom-contr→is-terminal hom-contr = record
+ { ! = λ {x} → hom-contr x .centre
+ ; !-unique = λ {x} h → sym (hom-contr x .paths h)
+ }
+```
+
+We can further strengthen this implication to an if-and-only-if.
+
+```agda
+ is-terminal→hom-contr
+ : ∀ {t}
+ → is-terminal C t
+ → (∀ x → is-contr (Hom x t))
+
+ is-terminal-univ
+ : ∀ {t}
+ → is-terminal C t ≃ (∀ x → is-contr (Hom x t))
+```
+
+
+This holds essentially by definition, so we elide the details.
+
+
+```agda
+ is-terminal→hom-contr term x = contr t.! λ h → sym (t.!-unique h) where
+ module t = is-terminal term
+
+ is-terminal-univ {t = t} = prop-ext! is-terminal→hom-contr hom-contr→is-terminal
+```
+
+
+
+We can also state this universal property in terms of [[equivalences]]:
+an object $t$ is terminal if and only if the constant map $\cC(x, t) \to \top$
+is an equivalence for every $x : \cC$.
+
+```agda
+ is-terminal≃comparison-equiv
+ : ∀ {t}
+ → is-terminal C t ≃ (∀ x → is-equiv λ (h : Hom x t) → tt)
+ is-terminal≃comparison-equiv {t = t} =
+ is-terminal C t ≃⟨ is-terminal-univ ⟩
+ (∀ x → is-contr (Hom x t)) ≃˘⟨ Π-ap-cod (λ x → Π-contr-eqv ⊤-is-contr ∙e is-hlevel-ap 0 (const-fibre-prop≃ (hlevel 1) tt tt)) ⟩
+ (∀ x → ⊤ → is-contr (Hom x t × tt ≡ tt)) ≃˘⟨ Π-ap-cod (λ x → is-equiv≃fibre-is-contr) ⟩
+ (∀ x → is-equiv (λ h → tt)) ≃∎
+```
## Uniqueness
@@ -62,32 +186,43 @@ inhabit a contractible space, namely the space of maps into $t_2$, so
they are equal.
```agda
- !-invertible : (t1 t2 : Terminal) → is-invertible (! t1 {top t2})
- !-invertible t1 t2 = make-invertible (! t2) (!-unique₂ t1 _ _) (!-unique₂ t2 _ _)
-
- ⊤-unique : (t1 t2 : Terminal) → top t1 ≅ top t2
- ⊤-unique t1 t2 = invertible→iso (! t2) (!-invertible t2 t1)
+ module _ {t} (t-term : is-terminal C t) where
+ private
+ module t = is-terminal t-term
+
+ !-invertible→is-terminal
+ : ∀ {x} → is-invertible (t.! {x})
+ → is-terminal C x
+ {-# INLINE !-invertible→is-terminal #-}
+ !-invertible→is-terminal !-inv = record
+ { ! = λ {x} → !.inv ∘ t.!
+ ; !-unique = λ h → post-invl.from !-inv (t.!-unique (t.! ∘ h))
+ }
+ where module ! = is-invertible (!-inv)
+
+ !-invertible : (t1 t2 : Terminal C) → is-invertible (t1 .! {top t2})
+ !-invertible t1 t2 = make-invertible (t2 .!) (!-unique₂ t1 _ _) (!-unique₂ t2 _ _)
+
+ ⊤-unique : (t1 t2 : Terminal C) → top t1 ≅ top t2
+ ⊤-unique t1 t2 = invertible→iso (t2 .!) (!-invertible t2 t1)
```
Hence, if $C$ is additionally a category, it has a propositional space of
terminal objects:
```agda
- ⊤-is-prop : is-category C → is-prop Terminal
- ⊤-is-prop ccat x1 x2 i .top =
- ccat .to-path (⊤-unique x1 x2) i
-
- ⊤-is-prop ccat x1 x2 i .has⊤ ob =
- is-prop→pathp
- (λ i → is-contr-is-prop {A = Hom _
- (ccat .to-path (⊤-unique x1 x2) i)})
- (x1 .has⊤ ob) (x2 .has⊤ ob) i
-
- is-terminal-iso : ∀ {A B} → A ≅ B → is-terminal A → is-terminal B
- is-terminal-iso isom term x = contr (isom .to ∘ term x .centre) λ h →
- isom .to ∘ term x .centre ≡⟨ ap (isom .to ∘_) (term x .paths _) ⟩
- isom .to ∘ isom .from ∘ h ≡⟨ cancell (isom .invl) ⟩
- h ∎
+ ⊤-is-prop : is-category C → is-prop (Terminal C)
+ ⊤-is-prop ccat x1 x2 = ext (ccat .to-path (⊤-unique x1 x2))
+
+ is-terminal-iso : ∀ {A B} → A ≅ B → is-terminal C A → is-terminal C B
+ is-terminal-iso {B = B} isom A-term = B-term where
+ module isom = _≅_ isom
+ module A = is-terminal A-term
+ open is-terminal
+
+ B-term : is-terminal C B
+ B-term .! = isom.to ∘ A.!
+ B-term .!-unique h = pre-invl.to (iso→invertible isom) (A.!-unique (isom.from ∘ h))
```
## In terms of right adjoints
@@ -96,36 +231,23 @@ We prove that the inclusion functor of an object $x$ of $\cC$ is right adjoint
to the unique functor $\cC \to \top$ if and only if $x$ is terminal.
```agda
- module _ (x : Ob) (term : is-terminal x) where
- is-terminal→inclusion-is-right-adjoint : !F ⊣ !Const {C = C} x
- is-terminal→inclusion-is-right-adjoint =
- hom-iso→adjoints (e _ .fst) (e _ .snd)
- λ _ _ _ → term _ .paths _
- where
- e : ∀ y → ⊤ ≃ Hom y x
- e y = is-contr→≃ (hlevel 0) (term y)
-
- module _ (x : Ob) (adj : !F ⊣ !Const {C = C} x) where
- inclusion-is-right-adjoint→is-terminal : is-terminal x
- inclusion-is-right-adjoint→is-terminal y = Equiv→is-hlevel 0
+ is-terminal→inclusion-is-right-adjoint
+ : ∀ (x : Ob) → is-terminal C x
+ → !F ⊣ !Const {C = C} x
+ is-terminal→inclusion-is-right-adjoint x term =
+ hom-iso→adjoints (e _ .fst) (e _ .snd)
+ λ _ _ _ → is-terminal.!-unique₂ term _ _
+ where
+ e : ∀ y → ⊤ ≃ Hom y x
+ e y = is-contr→≃ (hlevel 0) (is-terminal→hom-contr term y)
+
+ inclusion-is-right-adjoint→is-terminal
+ : ∀ (x : Ob) (adj : !F ⊣ !Const {C = C} x)
+ → is-terminal C x
+ {-# INLINE inclusion-is-right-adjoint→is-terminal #-}
+ inclusion-is-right-adjoint→is-terminal x adj =
+ hom-contr→is-terminal λ y →
+ Equiv→is-hlevel 0
(Σ-contr-snd (λ _ → hlevel 0) e⁻¹)
(R-adjunct-is-equiv adj .is-eqv _)
```
-
-
diff --git a/src/Cat/Diagram/Zero.lagda.md b/src/Cat/Diagram/Zero.lagda.md
index 0149f671d..0d27624cd 100644
--- a/src/Cat/Diagram/Zero.lagda.md
+++ b/src/Cat/Diagram/Zero.lagda.md
@@ -27,11 +27,13 @@ coincide. When this occurs, we call the object a **zero object**.
```agda
record is-zero (ob : Ob) : Type (o ⊔ h) where
+ no-eta-equality
field
has-is-initial : is-initial C ob
has-is-terminal : is-terminal C ob
record Zero : Type (o ⊔ h) where
+ no-eta-equality
field
∅ : Ob
has-is-zero : is-zero ∅
@@ -39,10 +41,10 @@ coincide. When this occurs, we call the object a **zero object**.
open is-zero has-is-zero public
terminal : Terminal C
- terminal = record { top = ∅ ; has⊤ = has-is-terminal }
+ terminal = record { top = ∅ ; has-is-term = has-is-terminal }
initial : Initial C
- initial = record { bot = ∅ ; has⊥ = has-is-initial }
+ initial = record { bot = ∅ ; has-is-init = has-is-initial }
open Terminal terminal public hiding (top)
open Initial initial public hiding (bot)
@@ -59,10 +61,10 @@ $0 = ¡ \circ ! : x \to y$ is called the **zero morphism**.
zero→ = ¡ ∘ !
zero-∘l : ∀ {x y z} → (f : Hom y z) → f ∘ zero→ {x} {y} ≡ zero→
- zero-∘l f = pulll (sym (¡-unique (f ∘ ¡)))
+ zero-∘l f = pulll (¡-unique (f ∘ ¡))
zero-∘r : ∀ {x y z} → (f : Hom x y) → zero→ {y} {z} ∘ f ≡ zero→
- zero-∘r f = pullr (sym (!-unique (! ∘ f)))
+ zero-∘r f = pullr (!-unique (! ∘ f))
zero-comm : ∀ {x y z} → (f : Hom y z) → (g : Hom x y) → f ∘ zero→ ≡ zero→ ∘ g
zero-comm f g = zero-∘l f ∙ sym (zero-∘r g)
@@ -101,6 +103,9 @@ earlier acts as the designated basepoint for each of the hom sets.
diff --git a/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md b/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md
index aea6be208..7b413086a 100644
--- a/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md
+++ b/src/Cat/Displayed/Diagram/Total/Terminal.lagda.md
@@ -34,33 +34,33 @@ displayed over $!$.
```agda
record is-terminal-over {top} (term : is-terminal B top) (top' : E ʻ top) : Type (o ⊔ o' ⊔ ℓ') where
- open Terminal {C = B} record{ has⊤ = term } hiding (top)
+ open is-terminal term
field
!' : ∀ {y} {y' : E ʻ y} → E.Hom[ ! ] y' top'
- !-unique' : ∀ {y} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → !' ≡ h
+ !-unique' : ∀ {y} {y' : E ʻ y} (h : E.Hom[ ! ] y' top') → h ≡ !'
opaque
!ₚ : ∀ {y} {m : B.Hom y top} {y' : E ʻ y} → E.Hom[ m ] y' top'
- !ₚ {m = m} = E.hom[ !-unique m ] !'
+ !ₚ {m = m} = E.hom[ sym $ !-unique m ] !'
abstract
- !ₚ-unique : ∀ {y} {m : B.Hom y top} {y' : E ʻ y} (h : E.Hom[ m ] y' top') → !ₚ ≡ h
+ !ₚ-unique : ∀ {y} {m : B.Hom y top} {y' : E ʻ y} (h : E.Hom[ m ] y' top') → h ≡ !ₚ
!ₚ-unique {m = m} {y'} = J
- (λ m p → (h : E.Hom[ m ] y' top') → E.hom[ p ] !' ≡ h)
- (λ h → E.from-pathp[] (!-unique' h))
- (!-unique m)
+ (λ m p → (h : E.Hom[ m ] y' top') → h ≡ E.hom[ p ] !')
+ (λ h → E.from-pathp[]⁻ (!-unique' h))
+ (sym $ !-unique m)
abstract
!'-unique₂
: ∀ {y} {m m' : B.Hom y top} {y' : E ʻ y} {h : E.Hom[ m ] y' top'} {h' : E.Hom[ m' ] y' top'}
→ {p : m ≡ m'}
→ h E.≡[ p ] h'
- !'-unique₂ {h = h} {h' = h'} = to-pathp (sym (!ₚ-unique _) ∙ !ₚ-unique _)
+ !'-unique₂ {h = h} {h' = h'} = to-pathp ((!ₚ-unique _) ∙ sym (!ₚ-unique _))
record TerminalP (t : Terminal B) : Type (o ⊔ o' ⊔ ℓ') where
open Terminal t
field
top' : E ʻ top
- has⊤' : is-terminal-over has⊤ top'
+ has⊤' : is-terminal-over has-is-term top'
open is-terminal-over has⊤' public
```
diff --git a/src/Cat/Displayed/Doctrine/Frame.lagda.md b/src/Cat/Displayed/Doctrine/Frame.lagda.md
index 566ae76c4..6f9789ba0 100644
--- a/src/Cat/Displayed/Doctrine/Frame.lagda.md
+++ b/src/Cat/Displayed/Doctrine/Frame.lagda.md
@@ -97,7 +97,8 @@ function which is constantly the top element.
```agda
term : ∀ S → Terminal (Fibre disp S)
term S .top _ = F.top
- term S .has⊤ f = is-prop∙→is-contr (hlevel 1) (λ i → F.!)
+ term S .has-is-term .is-terminal.! _ = F.!
+ term S .has-is-term .is-terminal.!-unique _ = prop!
```
## As a fibration
diff --git a/src/Cat/Displayed/Instances/Gluing.lagda.md b/src/Cat/Displayed/Instances/Gluing.lagda.md
index e97218580..366534a5a 100644
--- a/src/Cat/Displayed/Instances/Gluing.lagda.md
+++ b/src/Cat/Displayed/Instances/Gluing.lagda.md
@@ -123,10 +123,10 @@ $\cC$, while the morphisms are induced by $F$'s comparison maps.
```agda
Gl-terminal : TerminalP Gl D.terminal
-Gl-terminal .top' = cut {dom = C.top} (pres-terminal _ .centre)
+Gl-terminal .top' = cut {dom = C.top} (is-terminal.! image-is-terminal)
Gl-terminal .has⊤' .!' = record
{ map = C.!
- ; com = is-contr→is-prop (pres-terminal _) _ _
+ ; com = is-terminal.!-unique₂ image-is-terminal _ _
}
Gl-terminal .has⊤' .!-unique' h = Slice-pathp (C.!-unique _)
```
diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md
index d2598b91b..fb8c91f2b 100644
--- a/src/Cat/Displayed/Instances/Subobjects.lagda.md
+++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md
@@ -478,7 +478,8 @@ opaque
Sub-terminal : ∀ {y} → Terminal (Sub y)
Sub-terminal .Terminal.top = ⊤ₘ
-Sub-terminal .Terminal.has⊤ m = contr !ₘ λ _ → prop!
+Sub-terminal .Terminal.has-is-term .is-terminal.! = !ₘ
+Sub-terminal .Terminal.has-is-term .is-terminal.!-unique _ = prop!
```
Since products in slice categories are given by pullbacks, and pullbacks
diff --git a/src/Cat/Functor/Adjoint.lagda.md b/src/Cat/Functor/Adjoint.lagda.md
index 959481852..746d97326 100644
--- a/src/Cat/Functor/Adjoint.lagda.md
+++ b/src/Cat/Functor/Adjoint.lagda.md
@@ -520,11 +520,13 @@ equivalence, but it would not be very useful, either.
```agda
free-object→universal-map
: ∀ {X} → Free-object U X → Initial (X ↙ U)
- free-object→universal-map fo = λ where
- .I.bot → ↓obj (fo .unit)
- .I.has⊥ x .centre → ↓hom (D.idr _ ∙ sym (fo .commute))
- .I.has⊥ x .paths p → ↓Hom-path _ _ refl $ sym $
- fo .unique _ (sym (p .com) ∙ D.idr _)
+ {-# INLINE free-object→universal-map #-}
+ free-object→universal-map fo = to-initial $ record
+ { bot = ↓obj X.unit
+ ; ¡ = ↓hom (D.idr _ ∙ sym X.commute)
+ ; ¡-unique = λ f → ↓Hom-path _ _ refl $ X.unique _ (sym (f .com) ∙ D.idr _)
+ }
+ where module X = Free-object fo
```
### Free objects and adjoints
@@ -699,9 +701,8 @@ $A$ is an initial object in $\cC$.
free-on-initial→initial
: (F[⊥] : Free-object U init)
→ is-initial C (F[⊥] .free)
- free-on-initial→initial F[⊥] x .centre = F[⊥] .fold ¡
- free-on-initial→initial F[⊥] x .paths f =
- sym $ F[⊥] .unique f (sym (¡-unique _))
+ free-on-initial→initial F[⊥] .is-initial.¡ = F[⊥] .fold ¡
+ free-on-initial→initial F[⊥] .is-initial.¡-unique f = F[⊥] .unique f (¡-unique _)
```
Conversely, if $\cC$ has an initial object $\bot_{\cC}$, then $\bot_{\cC}$
@@ -874,10 +875,10 @@ module _ {o h o' h'} {C : Precategory o h} {D : Precategory o' h'} where
universal-map→free-object : ∀ {R X} → Universal-morphism R X → Free-object R X
universal-map→free-object x .free = _
universal-map→free-object x .unit = x .bot .map
- universal-map→free-object x .fold f = x .has⊥ (↓obj f) .centre .bot
- universal-map→free-object x .commute = sym (x .has⊥ _ .centre .com) ∙ C.idr _
+ universal-map→free-object x .fold f = x .¡ {↓obj f} .bot
+ universal-map→free-object x .commute = sym (x .¡ .com) ∙ C.idr _
universal-map→free-object x .unique g p = ap bot
- (sym (x .has⊥ _ .paths (↓hom (sym (p ∙ sym (C.idr _))))))
+ (x .¡-unique (↓hom (sym (p ∙ sym (C.idr _)))))
universal-maps→functor : ∀ {R} → (∀ X → Universal-morphism R X) → Functor C D
universal-maps→functor u = free-objects→functor
diff --git a/src/Cat/Functor/Adjoint/Continuous.lagda.md b/src/Cat/Functor/Adjoint/Continuous.lagda.md
index 2b94851e3..fae7f2580 100644
--- a/src/Cat/Functor/Adjoint/Continuous.lagda.md
+++ b/src/Cat/Functor/Adjoint/Continuous.lagda.md
@@ -145,12 +145,11 @@ if we do it by hand.
right-adjoint→terminal
: ∀ {x} → is-terminal D x → is-terminal C (R.₀ x)
- right-adjoint→terminal term x = contr fin uniq where
- fin = L-adjunct L⊣R (term (L.₀ x) .centre)
- uniq : ∀ x → fin ≡ x
- uniq x = ap fst $ is-contr→is-prop (R-adjunct-is-equiv L⊣R .is-eqv _)
- (_ , equiv→counit (R-adjunct-is-equiv L⊣R) _)
- (x , is-contr→is-prop (term _) _ _)
+ {-# INLINE right-adjoint→terminal #-}
+ right-adjoint→terminal term = record
+ { ! = L-adjunct L⊣R !
+ ; !-unique = λ h → sym $ Equiv.adjunctr (_ , L-adjunct-is-equiv L⊣R) (sym (!-unique _))
+ } where open is-terminal term
right-adjoint→lex : is-lex R
right-adjoint→lex .is-lex.pres-⊤ =
diff --git a/src/Cat/Functor/Adjoint/Hom.lagda.md b/src/Cat/Functor/Adjoint/Hom.lagda.md
index 8deee3cdd..b577a814a 100644
--- a/src/Cat/Functor/Adjoint/Hom.lagda.md
+++ b/src/Cat/Functor/Adjoint/Hom.lagda.md
@@ -134,6 +134,27 @@ of adjunction units and co-units.
D.id ∎
```
+
+
@@ -102,6 +103,7 @@ Sliced-lex {C = C} {D = D} {F = F} {X = X} flex = lex where
module D = Cat.Reasoning D
module Dx = Cat.Reasoning (Slice D (F .F₀ X))
module C = Cat.Reasoning C
+ module F = Cat.Functor.Reasoning F
open is-lex
lex : is-lex (Sliced F X)
lex .pres-pullback = pullback-above→pullback-below
@@ -119,11 +121,11 @@ $F(T)$, being isomorphic to the terminal object, is itself terminal!
```agda
lex .pres-⊤ {T = T} term =
- is-terminal-iso (Slice D (F .F₀ X))
+ is-terminal-iso
(subst (Dx._≅ cut (F .F₁ (T .map))) (ap cut (F .F-id))
- (F-map-iso (Sliced F X)
- (⊤-unique (Slice C X) Slice-terminal-object (record { has⊤ = term }))))
- Slice-terminal-object'
+ (F-map-iso (Sliced F X)
+ (⊤-unique Slice-terminal-object (record { top = T ; has-is-term = term }))))
+ Slice-is-terminal-object
```
# Sliced adjoints
diff --git a/src/Cat/Instances/Assemblies/Limits.lagda.md b/src/Cat/Instances/Assemblies/Limits.lagda.md
index f10d5fecb..3649e170a 100644
--- a/src/Cat/Instances/Assemblies/Limits.lagda.md
+++ b/src/Cat/Instances/Assemblies/Limits.lagda.md
@@ -163,8 +163,8 @@ tracked by the constant function with value $\sf{x}$.
```agda
Assemblies-terminal : Terminal (Assemblies 𝔸 ℓ)
Assemblies-terminal .top = ⊤Asm
-Assemblies-terminal .has⊤ X .centre = !Asm
-Assemblies-terminal .has⊤ X .paths x = ext λ _ → refl
+Assemblies-terminal .has-is-term .is-terminal.! = !Asm
+Assemblies-terminal .has-is-term .is-terminal.!-unique _ = ext λ _ → refl
```
-->
diff --git a/src/Cat/Instances/Coalgebras/Cartesian.lagda.md b/src/Cat/Instances/Coalgebras/Cartesian.lagda.md
index 811e0fd26..eee6fb225 100644
--- a/src/Cat/Instances/Coalgebras/Cartesian.lagda.md
+++ b/src/Cat/Instances/Coalgebras/Cartesian.lagda.md
@@ -405,9 +405,10 @@ the former is contractible if the latter is.
```agda
Terminal-coalgebra : Terminal (Coalgebras W)
Terminal-coalgebra .top = _
-Terminal-coalgebra .has⊤ (A , α) = Equiv→is-hlevel 0
- (Equiv.inverse (_ , L-adjunct-is-equiv (Forget⊣Cofree W)))
- (terminal .has⊤ A)
+Terminal-coalgebra .has-is-term =
+ hom-contr→is-terminal λ (A , α) →
+ Equiv→is-hlevel 0 (Equiv.inverse (_ , L-adjunct-is-equiv (Forget⊣Cofree W)))
+ (is-terminal→hom-contr (terminal .has-is-term) A)
```
Since we have a terminal object and pullbacks, we have arbitrary finite
diff --git a/src/Cat/Instances/Graphs/Limits.lagda.md b/src/Cat/Instances/Graphs/Limits.lagda.md
index 3b2b2d93a..8d188ee5c 100644
--- a/src/Cat/Instances/Graphs/Limits.lagda.md
+++ b/src/Cat/Instances/Graphs/Limits.lagda.md
@@ -113,9 +113,9 @@ Graphs-products a b .has-is-product .unique p q = ext record where
Graphs-terminal : ∀ {o ℓ} → Terminal (Graphs o ℓ)
Graphs-terminal .Terminal.top = ⊤ᴳ
-Graphs-terminal .Terminal.has⊤ x .centre .node = _
-Graphs-terminal .Terminal.has⊤ x .centre .edge = _
-Graphs-terminal .Terminal.has⊤ x .paths h = trivialᴳ!
+Graphs-terminal .Terminal.has-is-term .is-terminal.! .node _ = lift tt
+Graphs-terminal .Terminal.has-is-term .is-terminal.! .edge _ = lift tt
+Graphs-terminal .Terminal.has-is-term .is-terminal.!-unique h = trivialᴳ!
Graphs-pullbacks : ∀ {o ℓ} → has-pullbacks (Graphs o ℓ)
Graphs-pullbacks f g .apex = f ⊓ᴳ g
diff --git a/src/Cat/Instances/Presheaf/Colimits.lagda.md b/src/Cat/Instances/Presheaf/Colimits.lagda.md
index deb8020c7..10ebd808a 100644
--- a/src/Cat/Instances/Presheaf/Colimits.lagda.md
+++ b/src/Cat/Instances/Presheaf/Colimits.lagda.md
@@ -55,12 +55,19 @@ private
⊥PSh .F-id = ext λ ()
⊥PSh .F-∘ _ _ = ext λ ()
+empty→is-initial-PSh
+ : ∀ (F : ⌞ PSh κ C ⌟)
+ → (∀ x → ¬ (F ʻ x))
+ → is-initial (PSh κ C) F
+{-# INLINE empty→is-initial-PSh #-}
+empty→is-initial-PSh F ¬Fx = record
+ { ¡ = NT (λ x Fx → absurd (¬Fx x Fx)) λ x y f → ext (λ Fx → absurd (¬Fx x Fx))
+ ; ¡-unique = λ h → ext (λ x Fx → absurd (¬Fx x Fx))
+ }
+
PSh-initial : Initial (PSh κ C)
-PSh-initial = record { has⊥ = uniq } where
- uniq : is-initial (PSh κ C) ⊥PSh
- uniq x .centre .η _ ()
- uniq x .centre .is-natural _ _ _ = ext λ ()
- uniq x .paths f = ext λ _ ()
+PSh-initial .Initial.bot = ⊥PSh
+PSh-initial .Initial.has-is-init = empty→is-initial-PSh ⊥PSh λ _ ()
_⊎PSh_ : (A B : PSh.Ob) → PSh.Ob
(A ⊎PSh B) .F₀ i = el! (∣ A .F₀ i ∣ ⊎ ∣ B .F₀ i ∣)
diff --git a/src/Cat/Instances/Presheaf/Limits.lagda.md b/src/Cat/Instances/Presheaf/Limits.lagda.md
index c8332d439..324854c2b 100644
--- a/src/Cat/Instances/Presheaf/Limits.lagda.md
+++ b/src/Cat/Instances/Presheaf/Limits.lagda.md
@@ -61,9 +61,11 @@ contr→is-terminal-PSh
: ∀ (T : ⌞ PSh κ C ⌟)
→ ⦃ ∀ {c n} → H-Level ⌞ T .F₀ c ⌟ n ⦄
→ is-terminal (PSh κ C) T
-contr→is-terminal-PSh T _ .centre .η _ _ = hlevel!
-contr→is-terminal-PSh T _ .centre .is-natural _ _ _ = prop!
-contr→is-terminal-PSh T _ .paths _ = ext λ _ _ → prop!
+{-# INLINE contr→is-terminal-PSh #-}
+contr→is-terminal-PSh T = record
+ { ! = NT (λ _ _ → hlevel!) λ _ _ _ → prop!
+ ; !-unique = λ _ → ext λ _ _ → prop!
+ }
prop→is-subterminal-PSh
: ∀ (T : ⌞ PSh κ C ⌟)
@@ -72,7 +74,7 @@ prop→is-subterminal-PSh
prop→is-subterminal-PSh T _ _ _ = ext λ _ _ → prop!
PSh-terminal : Terminal (PSh κ C)
-PSh-terminal = record { has⊤ = contr→is-terminal-PSh ⊤PSh }
+PSh-terminal = record { has-is-term = contr→is-terminal-PSh ⊤PSh }
```
The product presheaf is as described in the introduction, now with all
diff --git a/src/Cat/Instances/Sets/Cocomplete.lagda.md b/src/Cat/Instances/Sets/Cocomplete.lagda.md
index 44d442c8c..e6183349c 100644
--- a/src/Cat/Instances/Sets/Cocomplete.lagda.md
+++ b/src/Cat/Instances/Sets/Cocomplete.lagda.md
@@ -171,8 +171,8 @@ category of sets of _any_ level $\ell$ admits them.
```agda
Sets-initial : Initial (Sets ℓ)
Sets-initial .bot = el! (Lift _ ⊥)
- Sets-initial .has⊥ _ .centre ()
- Sets-initial .has⊥ _ .paths _ = ext λ ()
+ Sets-initial .has-is-init .is-initial.¡ = λ ()
+ Sets-initial .has-is-init .is-initial.¡-unique _ = ext λ ()
```
Coproducts are given by disjoint sums:
@@ -287,11 +287,8 @@ disjoint images: We must project out a path $i = j$ from a path $\|
truncation --- to prove $\bot$ using the assumption that $i ≠ j$.
```agda
- coprod .different-images-are-disjoint i j i≠j os = contr map uniq where
- map : Σ[ x ∈ F i ] Σ[ y ∈ F j ] (coprod.ι i x ≡ coprod.ι j y) → ∣ os ∣
- map (i , j , p) = absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
-
- uniq : ∀ x → map ≡ x
- uniq _ = funext λ where
- (_ , _ , p) → absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
+ coprod .different-images-are-disjoint i j i≠j .is-initial.¡ (_ , _ , p) =
+ absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
+ coprod .different-images-are-disjoint i j i≠j .is-initial.¡-unique _ = ext λ _ _ p →
+ absurd (i≠j (ap (∥-∥₀-elim (λ _ → I .is-tr) fst) p))
```
diff --git a/src/Cat/Instances/Sets/Complete.lagda.md b/src/Cat/Instances/Sets/Complete.lagda.md
index e53cc2e5b..0b8ebb2b0 100644
--- a/src/Cat/Instances/Sets/Complete.lagda.md
+++ b/src/Cat/Instances/Sets/Complete.lagda.md
@@ -103,7 +103,8 @@ category of sets of _any_ level $\ell$ admits them.
```agda
Sets-terminal : Terminal (Sets ℓ)
Sets-terminal .top = el! (Lift _ ⊤)
- Sets-terminal .has⊤ _ = hlevel 0
+ Sets-terminal .has-is-term .is-terminal.! _ = lift tt
+ Sets-terminal .has-is-term .is-terminal.!-unique _ = prop!
```
Products are given by product sets:
diff --git a/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md b/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md
index effe11f63..6d5f7eeae 100644
--- a/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md
+++ b/src/Cat/Instances/Sets/Counterexamples/SelfDual.lagda.md
@@ -49,7 +49,7 @@ open Sets.Inverses
```agda
Sets^op-initial : Initial (Sets ℓ ^op)
Sets^op-initial .bot = el! (Lift _ ⊤)
-Sets^op-initial .has⊥ x = hlevel 0
+Sets^op-initial .has-is-init = hom-contr→is-initial (λ _ → hlevel 0)
```
diff --git a/src/Cat/Instances/Shape/Interval.lagda.md b/src/Cat/Instances/Shape/Interval.lagda.md
index 9da79c16f..7e99ff5f3 100644
--- a/src/Cat/Instances/Shape/Interval.lagda.md
+++ b/src/Cat/Instances/Shape/Interval.lagda.md
@@ -80,12 +80,7 @@ function.
```agda
0≤1-top : Terminal 0≤1
0≤1-top .top = true
-
-0≤1-top .has⊤ false .centre = _
-0≤1-top .has⊤ false .paths _ = refl
-
-0≤1-top .has⊤ true .centre = _
-0≤1-top .has⊤ true .paths _ = refl
+0≤1-top .has-is-term = hom-contr→is-terminal λ _ → hlevel 0
0≤1-products : ∀ A B → Product 0≤1 A B
0≤1-products A B .apex = and A B
diff --git a/src/Cat/Instances/Sheaf/Limits/Finite.lagda.md b/src/Cat/Instances/Sheaf/Limits/Finite.lagda.md
index ca5159dc7..6b1dd5fcd 100644
--- a/src/Cat/Instances/Sheaf/Limits/Finite.lagda.md
+++ b/src/Cat/Instances/Sheaf/Limits/Finite.lagda.md
@@ -74,10 +74,12 @@ Sh[]-pullbacks {A = A} {B} {X} f g = pb where
pb : Pullback (Sheaves J _) _ _
pb .apex .fst = pb' .apex
- pb .apex .snd = is-sheaf-limit {o' = lzero} {ℓ' = lzero} (Limit.has-limit (Pullback→Limit (PSh ℓ C) pb')) λ where
- cs-a → A .snd
- cs-b → B .snd
- cs-c → X .snd
+ pb .apex .snd =
+ is-sheaf-limit {o' = lzero} {ℓ' = lzero}
+ (Limit.has-limit (Pullback→Limit (PSh ℓ C) (cospan→cospan-diagram lzero lzero f g) pb')) λ where
+ cs-a → A .snd
+ cs-b → B .snd
+ cs-c → X .snd
pb .p₁ = pb' .p₁
pb .p₂ = pb' .p₂
pb .has-is-pb = record { Pullback pb' }
@@ -89,11 +91,11 @@ The terminal object in sheaves is even easier to define:
```agda
Sh[]-terminal : Terminal (Sheaves J ℓ)
Sh[]-terminal .top .fst = PSh-terminal _ C .top
-Sh[]-terminal .has⊤ (S , _) = PSh-terminal _ C .has⊤ S
-
Sh[]-terminal .top .snd .whole _ _ = lift tt
Sh[]-terminal .top .snd .glues _ _ _ _ = refl
Sh[]-terminal .top .snd .separate _ _ = refl
+Sh[]-terminal .has-is-term = hom-contr→is-terminal λ S →
+ is-terminal→hom-contr (PSh-terminal ℓ C .has-is-term) (S .fst)
```
diff --git a/src/Homotopy/Space/Circle/Properties.lagda.md b/src/Homotopy/Space/Circle/Properties.lagda.md
index 2633c339e..6be76f68f 100644
--- a/src/Homotopy/Space/Circle/Properties.lagda.md
+++ b/src/Homotopy/Space/Circle/Properties.lagda.md
@@ -9,6 +9,8 @@ open import Algebra.Group.Cat.Base
open import Algebra.Group.Homotopy
open import Algebra.Group
+open import Cat.Diagram.Terminal
+
open import Data.Set.Truncation
open import Data.Int.Universal
open import Data.Bool
@@ -272,6 +274,6 @@ get that all of its higher homotopy groups are trivial.
πₙ₊₂S¹≡0 : ∀ n → πₙ₊₁ (suc n) S¹∙ ≡ Zero-group {lzero}
πₙ₊₂S¹≡0 n = ∫-Path
- (Zero-group-is-terminal _ .centre)
+ (Zero-group-is-terminal .is-terminal.!)
(is-contr→≃ (is-contr→∥-∥₀-is-contr (Ωⁿ⁺²S¹-is-contr n)) (hlevel 0) .snd)
```
diff --git a/src/Order/Diagram/Bottom.lagda.md b/src/Order/Diagram/Bottom.lagda.md
index 51ac10062..7032e742c 100644
--- a/src/Order/Diagram/Bottom.lagda.md
+++ b/src/Order/Diagram/Bottom.lagda.md
@@ -96,9 +96,12 @@ hom-sets with hom-props!
```agda
is-bottom→initial : ∀ {x} → is-bottom x → is-initial (poset→category P) x
-is-bottom→initial is-bot x .centre = is-bot x
-is-bottom→initial is-bot x .paths _ = ≤-thin _ _
+{-# INLINE is-bottom→initial #-}
+is-bottom→initial x-bot = record
+ { ¡ = λ {x} → x-bot x
+ ; ¡-unique = λ {x} h → ≤-thin h (x-bot x)
+ }
initial→is-bottom : ∀ {x} → is-initial (poset→category P) x → is-bottom x
-initial→is-bottom initial x = initial x .centre
+initial→is-bottom initial x = is-initial.¡ initial {x}
```
diff --git a/src/Order/Diagram/Top.lagda.md b/src/Order/Diagram/Top.lagda.md
index b7d14b769..83b710a58 100644
--- a/src/Order/Diagram/Top.lagda.md
+++ b/src/Order/Diagram/Top.lagda.md
@@ -95,9 +95,14 @@ hom-sets with hom-props!
```agda
is-top→terminal : ∀ {x} → is-top x → is-terminal (poset→category P) x
-is-top→terminal is-top x .centre = is-top x
-is-top→terminal is-top x .paths _ = ≤-thin _ _
+{-# INLINE is-top→terminal #-}
+is-top→terminal is-top = record
+ { ! = λ {x} → is-top x
+ ; !-unique = λ {x} h → ≤-thin h (is-top x)
+ }
terminal→is-top : ∀ {x} → is-terminal (poset→category P) x → is-top x
-terminal→is-top terminal x = terminal x .centre
+{-# INLINE terminal→is-top #-}
+terminal→is-top terminal x = is-terminal.! terminal
+-- terminal x .centre
```
diff --git a/src/Order/Instances/Coproduct.lagda.md b/src/Order/Instances/Coproduct.lagda.md
index a30ccd82f..c49643095 100644
--- a/src/Order/Instances/Coproduct.lagda.md
+++ b/src/Order/Instances/Coproduct.lagda.md
@@ -143,7 +143,7 @@ object]] in $\Pos$.
```agda
Posets-initial : ∀ {o ℓ} → Initial (Posets o ℓ)
Posets-initial .bot = 𝟘ᵖ
-Posets-initial .has⊥ P .centre .hom ()
-Posets-initial .has⊥ P .centre .pres-≤ ()
-Posets-initial .has⊥ P .paths f = ext λ ()
+Posets-initial .has-is-init .is-initial.¡ .hom ()
+Posets-initial .has-is-init .is-initial.¡ .pres-≤ ()
+Posets-initial .has-is-init .is-initial.¡-unique _ = ext λ ()
```
diff --git a/src/Order/Instances/Product.lagda.md b/src/Order/Instances/Product.lagda.md
index 164b03bba..c36e390f8 100644
--- a/src/Order/Instances/Product.lagda.md
+++ b/src/Order/Instances/Product.lagda.md
@@ -98,7 +98,7 @@ the set with one element is the [[terminal object]] in $\Pos$.
```agda
Posets-terminal : ∀ {o ℓ} → Terminal (Posets o ℓ)
Posets-terminal .top = 𝟙ᵖ
-Posets-terminal .has⊤ P .centre .hom _ = lift tt
-Posets-terminal .has⊤ P .centre .pres-≤ _ = lift tt
-Posets-terminal .has⊤ P .paths f = ext λ _ → refl
+Posets-terminal .has-is-term .is-terminal.! .hom x = lift tt
+Posets-terminal .has-is-term .is-terminal.! .pres-≤ _ = lift tt
+Posets-terminal .has-is-term .is-terminal.!-unique h = ext λ _ → refl
```
diff --git a/src/Topoi/Base.lagda.md b/src/Topoi/Base.lagda.md
index f3d4202a1..5aa97c745 100644
--- a/src/Topoi/Base.lagda.md
+++ b/src/Topoi/Base.lagda.md
@@ -22,6 +22,7 @@ open import Cat.Instances.Elements
open import Cat.Functor.Bifunctor
open import Cat.Instances.Functor
open import Cat.Diagram.Pullback
+open import Cat.Diagram.Terminal
open import Cat.Functor.Pullback
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
@@ -322,11 +323,12 @@ limits directly for efficiency concerns.
[adjoint equivalence]: Cat.Functor.Equivalence.html
```agda
- sets .L-lex .pres-⊤ {T} psh-terminal set = contr (cent .η _) uniq where
- func = incl .F₀ set
- cent = psh-terminal func .centre
- uniq : ∀ f → cent .η _ ≡ f
- uniq f = psh-terminal func .paths f' ηₚ _ where
+ sets .L-lex .pres-⊤ {T} psh-terminal = term' where
+ open is-terminal
+
+ term' : is-terminal (Sets κ) _
+ term' .! {X} = psh-terminal .! {incl .F₀ X} .η _
+ term' .!-unique f = psh-terminal .!-unique f' ηₚ _ where
f' : _ => _
f' .η _ = f
f' .is-natural _ _ _ = funext λ x → happly (sym (T .F-id)) _
@@ -677,7 +679,7 @@ The composition of two left-exact functors is again left-exact, so
there's no impediment to composition there, either.
```agda
- mk .Inv-lex .pres-⊤ term ob = g.Inv-lex .pres-⊤ (f.Inv-lex .pres-⊤ term) _
+ mk .Inv-lex .pres-⊤ term = g.Inv-lex .pres-⊤ (f.Inv-lex .pres-⊤ term)
mk .Inv-lex .pres-pullback pb = g.Inv-lex .pres-pullback (f.Inv-lex .pres-pullback pb)
```
diff --git a/src/Topoi/Reasoning.lagda.md b/src/Topoi/Reasoning.lagda.md
index bd2bcd45d..aa4d93d27 100644
--- a/src/Topoi/Reasoning.lagda.md
+++ b/src/Topoi/Reasoning.lagda.md
@@ -87,7 +87,7 @@ do it by hand for the [[terminal object]], binary [[products]], and binary
open Terminal
terminal-sheaf : Terminal 𝒯
terminal-sheaf .top = L.₀ (PSh-terminal _ site .top)
- terminal-sheaf .has⊤ = L-lex.pres-⊤ (PSh-terminal _ site .has⊤)
+ terminal-sheaf .has-is-term = L-lex.pres-⊤ (PSh-terminal _ site .has-is-term)
product-sheaf : ∀ A B → Product 𝒯 A B
product-sheaf A B = product' where
@@ -103,7 +103,7 @@ do it by hand for the [[terminal object]], binary [[products]], and binary
let
prod =
L-lex.pres-product
- (PSh-terminal _ site .has⊤)
+ (PSh-terminal _ site .has-is-term)
(product-presheaf .has-is-product)
in is-product-iso (Lι-iso _) (Lι-iso _) prod