open import Cat.Diagram.Equaliser.Joint
open import Cat.Diagram.Limit.Equaliser
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Limit.Product
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Initial
open import Cat.Prelude

import Cat.Reasoning as Cat

module Cat.Diagram.Initial.Weak where

Weakly initial objects and familiesπŸ”—

module _ {o β„“} (C : Precategory o β„“) where
  open Cat C

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