module Cat.Diagram.Initial.Weak where

Weakly initial objects and familiesπŸ”—

A weakly initial object is like an initial object, but dropping the requirement of uniqueness. Explicitly, an object is weakly initial in if, for every there merely exists an arrow

  is-weak-initial : ⌞ C ⌟ β†’ Type _
  is-weak-initial X = βˆ€ Y β†’ βˆ₯ Hom X Y βˆ₯

We can weaken this even further, by allowing a family of objects rather than the single object a family is weakly initial if, for every there exists a and a map Note that we don’t (can’t!) impose any compatibility conditions between the choices of indices.

  is-weak-initial-fam : βˆ€ {β„“'} {I : Type β„“'} (F : I β†’ ⌞ C ⌟) β†’ Type _
  is-weak-initial-fam {I = I} F = (Y : ⌞ C ⌟) β†’ βˆƒ[ i ∈ I ] (Hom (F i) Y)

The connection between these notions is the following: the indexed product of a weakly initial family is a weakly initial object.

  is-wif→is-weak-initial
    : βˆ€ {β„“'} {I : Type β„“'} (F : I β†’ ⌞ C ⌟) {Ξ F} {Ο€f : βˆ€ i β†’ Hom Ξ F (F i)}
    β†’ is-weak-initial-fam F
    β†’ is-indexed-product C F Ο€f
    β†’ (y : ⌞ C ⌟) β†’ βˆ₯ Hom Ξ F y βˆ₯
  is-wif→is-weak-initial F {πf = πf} wif ip y = do
    (ix , h) ← wif y
    pure (h ∘ Ο€f ix)

We can also connect these notions to the non-weak initial objects. Suppose has all equalisers, including joint equalisers for small families. If is a weakly initial object, then the domain of the joint equaliser of all arrows is an initial object.

  is-weak-initial→equaliser
    : βˆ€ (X : ⌞ C ⌟) {L} {l : Hom L X}
    β†’ (βˆ€ y β†’ βˆ₯ Hom X y βˆ₯)
    β†’ 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
    open is-joint-equaliser lim

Since, for any the space of maps is inhabited, it will suffice to show that it is a proposition. To this end, given two arrows consider their equaliser First, we have some arrow

    p' : is-prop (Hom L y)
    p' f g = βˆ₯-βˆ₯-out! do
      let
        module fg = Equaliser (eqs f g)
        open fg renaming (equ to j) using ()

      k ← is-wi fg.apex

Then, we can calculate: as maps we have

      let
        p =
          i               β‰‘βŸ¨ introl refl βŸ©β‰‘
          id ∘ i          β‰‘βŸ¨ equal {j = i ∘ j ∘ k} βŸ©β‰‘
          (i ∘ j ∘ k) ∘ i β‰‘βŸ¨ pullr (pullr refl) βŸ©β‰‘
          i ∘ j ∘ k ∘ i   ∎

Then, since a joint equaliser is a monomorphism, we can cancel from both sides to get

        r : j ∘ k ∘ i ≑ id
        r = is-joint-equaliserβ†’is-monic (j ∘ k ∘ i) id (sym p βˆ™ intror refl)

Finally, if we have with then we can calculate so is an epimorphism. So, since equalises and by construction, we have

        s : is-epic j
        s g h Ξ± = intror r βˆ™ extendl Ξ± βˆ™ elimr r

      pure (s f g fg.equal)

    cen : Hom L y
    cen = βˆ₯-βˆ₯-out p' ((_∘ i) <$> is-wi y)

Putting this together, we can show that, if a complete category has a small weakly initial family indexed by a set, then it has an initial object.

  is-complete-weak-initial→initial
    : βˆ€ {I : Type β„“} (F : I β†’ ⌞ C ⌟) ⦃ _ : βˆ€ {n} β†’ H-Level I (2 + n) ⦄
    β†’ is-complete β„“ β„“ C
    β†’ is-weak-initial-fam F
    β†’ Initial C
  is-complete-weak-initialβ†’initial F compl wif = record { hasβŠ₯ = equal-is-initial } where
The proof is by pasting together the results above.
    open Indexed-product

    prod : Indexed-product C F
    prod = Limit→IP C (hlevel 3) F (compl _)

    prod-is-wi : is-weak-initial (prod .Ξ F)
    prod-is-wi = is-wif→is-weak-initial F wif (prod .has-is-ip)

    equal : Joint-equaliser C {I = Hom (prod .Ξ F) (prod .Ξ F)} Ξ» h β†’ h
    equal = Limit→Joint-equaliser C _ id (is-complete-lower ℓ ℓ lzero ℓ compl _)
    open Joint-equaliser equal using (has-is-je)

    equal-is-initial = is-weak-initial→equaliser _ prod-is-wi has-is-je λ f g →
      Limit→Equaliser C (is-complete-lower ℓ ℓ lzero lzero compl _)