open import Algebra.Quasigroup

open import Cat.Diagram.Initial
open import Cat.Displayed.Total
open import Cat.Prelude hiding (_/_)
module Algebra.Quasigroup.Instances.Initial where

The initial quasigroupπŸ”—

The empty type trivially forms a quasigroup.

private variable
  β„“ : Level

open Total-hom
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.

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.

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))
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