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