def: empty quasigroups

Author: TOTBWF

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

@@ -0,0 +1,80 @@
+---
+description: |
+  The initial quasigroup.
+---
+<!--
+```agda
+open import Algebra.Quasigroup
+
+open import Cat.Displayed.Total
+open import Cat.Diagram.Initial
+open import Cat.Prelude hiding (_/_)
+```
+-->
+
+```agda
+module Algebra.Quasigroup.Instances.Initial where
+```
+
+# The initial quasigroup {defines="initial-quasigroup empty-quasigroup"}
+
+The empty type trivially forms a [[quasigroup]].
+
+<!--
+```agda
+private variable
+  ℓ : Level
+
+open Total-hom
+```
+-->
+
+```agda
+Empty-quasigroup : ∀ {ℓ} → Quasigroup ℓ
+Empty-quasigroup = to-quasigroup ⊥-quasigroup where
+  open make-quasigroup
+
+  ⊥-quasigroup : make-quasigroup (Lift _ ⊥)
+  ⊥-quasigroup .quasigroup-is-set = hlevel 2
+  ⊥-quasigroup ._⋆_ ()
+  ⊥-quasigroup ._⧵_ ()
+  ⊥-quasigroup ._/_ ()
+  ⊥-quasigroup ./-invl ()
+  ⊥-quasigroup ./-invr ()
+  ⊥-quasigroup .⧵-invr ()
+  ⊥-quasigroup .⧵-invl ()
+```
+
+Moreover, the empty quasigroup is an [[initial object]] in the category
+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 .hom ()
+Empty-quasigroup-is-initial A .centre .preserves .is-quasigroup-hom.pres-⋆ ()
+Empty-quasigroup-is-initial A .paths f = ext λ ()
+
+Initial-quasigroup : Initial (Quasigroups ℓ)
+Initial-quasigroup .Initial.bot = Empty-quasigroup
+Initial-quasigroup .Initial.has⊥ = Empty-quasigroup-is-initial
+```
+
+In fact, the empty quasigroup is a [[strict initial object]].
+
+```agda
+Initial-quasigroup-is-strict
+  : is-strict-initial (Quasigroups ℓ) Initial-quasigroup
+Initial-quasigroup-is-strict =
+  make-is-strict-initial (Quasigroups _) Initial-quasigroup $ λ A f → ext λ a →
+  absurd (Lift.lower (f # a))
+```
+
+<!--
+```agda
+Strict-initial-quasigroup : Strict-initial (Quasigroups ℓ)
+Strict-initial-quasigroup .Strict-initial.initial =
+  Initial-quasigroup
+Strict-initial-quasigroup .Strict-initial.has-is-strict =
+  Initial-quasigroup-is-strict
+```
+-->

src/Cat/Diagram/Initial.lagda.md

@@ -93,7 +93,7 @@ a proposition:
       (x1 .has⊥ ob) (x2 .has⊥ ob) i
 ```
 
-## Strictness
+## Strictness {defines="strict-initial-object"}
 
 An initial object is said to be *[strict]* if every morphism into it is an *iso*morphism.
 This is a categorical generalization of the fact that if one can write a function $X \to \bot$ then $X$ must itself be empty.
@@ -121,6 +121,19 @@ Strictness is a property of, not structure on, an initial object.
   is-strict-initial-is-prop i = hlevel 1
 ```
 
+As maps out of initial objects are unique, it suffices to show that
+every map $\text{!`} \circ f = id$ for every $f : X \to \bot$ to establish that $\bot$ is a
+strict initial object.
+
+```agda
+  make-is-strict-initial
+    : (i : Initial)
+    → (∀ x → (f : Hom x (i .bot)) → (¡ i) ∘ f ≡ id)
+    → is-strict-initial i
+  make-is-strict-initial i p x f =
+    make-invertible (¡ i) (¡-unique₂ i (f ∘ ¡ i) id) (p x f)
+```
+
 <!--
 ```agda
 module _ {o h} {C : Precategory o h} where