module Cat.Diagram.Limit.Product {o h} (C : Precategory o h) where

Products are limitsπŸ”—

We establish the correspondence between binary products and limits over the functor out of which maps to and to We begin by defining the functor (reusing existing infrastructure):

2-object-category : Precategory _ _
2-object-category = Disc' (el Bool Bool-is-set)

2-object-diagram : Ob β†’ Ob β†’ Functor 2-object-category C
2-object-diagram a b = Disc-diagram Ξ» where
  true  β†’ a
  false β†’ b

With that out of the way, we can establish the claimed equivalence. We start by showing that any pair of morphisms defines a cone over the discrete diagram consisting of and This is essentially by definition of what it means to be a cone in this case, but they’re arranged in very different ways:

  : βˆ€ {q a b} β†’ Hom q a β†’ Hom q b
  β†’ Const q => (2-object-diagram a b)
Pair→Cone f g = Disc-natural λ where
  true  β†’ f
  false β†’ g

The two-way correspondence between products and terminal cones is then simple enough to establish by appropriately shuffling the data.

  : βˆ€ {x a b} {p1 : Hom x a} {p2 : Hom x b}
  β†’ is-product C p1 p2
  → is-limit {C = C} (2-object-diagram a b) x (Pair→Cone p1 p2)
is-product→is-limit {x = x} {a} {b} {p1} {p2} is-prod =
  to-is-limitp ml Ξ» where
    {true} β†’ refl
    {false} β†’ refl
    module is-prod = is-product is-prod
    open make-is-limit

    ml : make-is-limit (2-object-diagram a b) x
    ml .ψ true = p1
    ml .ψ false = p2
    ml .commutes {true}  {true}  f = idl p1
    ml .commutes {true}  {false} f = absurd (true≠false f)
    ml .commutes {false} {true}  f = absurd (true≠false $ sym f)
    ml .commutes {false} {false} f = idl p2
    ml .universal       eta _ = is-prod.⟨ eta true , eta false ⟩is-prod.
    ml .factors {true}  eta _ = is-prod.Ο€β‚βˆ˜factor
    ml .factors {false} eta _ = is-prod.Ο€β‚‚βˆ˜factor
    ml .unique eta p other q = is-prod.unique other (q true) (q false)

  : βˆ€ {a b} {K : Functor ⊀Cat C}
  β†’ {eta : K F∘ !F => 2-object-diagram a b}
  β†’ is-ran !F (2-object-diagram a b) K eta
  β†’ is-product C (eta .Ξ· true) (eta .Ξ· false)
is-limit→is-product {a} {b} {K} {eta} lim = prod where
  module lim = is-limit lim

    : βˆ€ {y} β†’ Hom y a β†’ Hom y b
    β†’ βˆ€ (j : Bool) β†’ Hom y (2-object-diagram a b .Fβ‚€ j)
  pair p1 p2 true = p1
  pair p1 p2 false = p2

    : βˆ€ {y} {p1 : Hom y a} {p2 : Hom y b}
    β†’ {i j : Bool}
    β†’ (p : i ≑ j)
    β†’ 2-object-diagram a b .F₁ p ∘ pair p1 p2 i ≑ pair p1 p2 j
  pair-commutes {p1 = p1} {p2 = p2} =
      J (Ξ» _ p β†’ 2-object-diagram a b .F₁ p ∘ pair p1 p2 _ ≑ pair p1 p2 _)
        (eliml (2-object-diagram a b .F-id))

  prod : is-product C (eta .Ξ· true) (eta .Ξ· false)
  prod .⟨_,_⟩ f g = lim.universal (pair f g) pair-commutes
  prod .Ο€β‚βˆ˜factor {_} {p1'} {p2'} = lim.factors (pair p1' p2') pair-commutes
  prod .Ο€β‚‚βˆ˜factor {_} {p1'} {p2'} = lim.factors (pair p1' p2') pair-commutes
  prod .unique other p q = lim.unique _ _ other Ξ» where
    true β†’ p
    false β†’ q

Productβ†’Limit : βˆ€ {a b} β†’ Product C a b β†’ Limit (2-object-diagram a b)
Product→Limit prod = to-limit (is-product→is-limit (has-is-product prod))

Limitβ†’Product : βˆ€ {a b} β†’ Limit (2-object-diagram a b) β†’ Product C a b
Limit→Product lim .apex = Limit.apex lim
Limitβ†’Product lim .π₁ = Limit.cone lim .Ξ· true
Limit→Product lim .π₂ = Limit.cone lim .η false
Limit→Product lim .has-is-product =
  is-limit→is-product (Limit.has-limit lim)

We note that any functor is canonically equal, not just naturally isomorphic, to the one we defined above.

  : βˆ€ (F : Functor 2-object-category C)
  β†’ F ≑ 2-object-diagram (F # true) (F # false)
canonical-functors F = Functor-path p q where
  p : βˆ€ x β†’ _
  p false = refl
  p true  = refl

  q : βˆ€ {x y} (f : x ≑ y) β†’ _
  q {false} {false} p =
    F .F₁ p           β‰‘βŸ¨ ap (F .F₁) (Bool-is-set _ _ _ _) βŸ©β‰‘
    F .F₁ refl        β‰‘βŸ¨ F .F-id βŸ©β‰‘
    id                ∎
  q {true} {true} p =
    F .F₁ p           β‰‘βŸ¨ ap (F .F₁) (Bool-is-set _ _ _ _) βŸ©β‰‘
    F .F₁ refl        β‰‘βŸ¨ F .F-id βŸ©β‰‘
    id                ∎
  q {false} {true} p = absurd (true≠false (sym p))
  q {true} {false} p = absurd (true≠false p)

Indexed products as limitsπŸ”—

In the particular case where is a groupoid, e.g.Β because it arises as the space of objects of a univalent category, an indexed product for is the same thing as a limit over considered as a functor We can not lift this restriction: If is not a groupoid, then its path spaces are not necessarily sets, and so the Disc construction does not apply to it.

module _ {β„“} {I : Type β„“} (i-is-grpd : is-groupoid I) (F : I β†’ Ob) where
  open _=>_

  Projβ†’Cone : βˆ€ {x} β†’ (βˆ€ i β†’ Hom x (F i))
            β†’ Const x => Disc-adjunct {C = C} {iss = i-is-grpd} F
  Proj→Cone π .η i = π i
  Proj→Cone π .is-natural i j p =
    J (Ξ» j p β†’  Ο€ j ∘ id ≑ subst (Hom (F i) βŠ™ F) p id ∘ Ο€ i)
      (idr _ βˆ™ introl (transport-refl id))

    : βˆ€ {x} {Ο€ : βˆ€ i β†’ Hom x (F i)}
    β†’ is-indexed-product C F Ο€
    → is-limit (Disc-adjunct F) x (Proj→Cone π)
  is-indexed-product→is-limit {x = x} {π} ip =
    to-is-limitp ml refl
      module ip = is-indexed-product ip
      open make-is-limit

      ml : make-is-limit (Disc-adjunct F) x
      ml .ψ j = Ο€ j
      ml .commutes {i} {j} p =
        J (Ξ» j p β†’ subst (Hom (F i) βŠ™ F) p id ∘ Ο€ i ≑ Ο€ j)
          (eliml (transport-refl _))
      ml .universal eta p = ip.tuple eta
      ml .factors eta p = ip.commute
      ml .unique eta p other q = ip.unique eta q

    : βˆ€ {K : Functor ⊀Cat C}
    β†’ {eta : K F∘ !F => Disc-adjunct {iss = i-is-grpd} F}
    β†’ is-ran !F (Disc-adjunct F) K eta
    β†’ is-indexed-product C F (eta .Ξ·)
  is-limit→is-indexed-product {K = K} {eta} lim = ip where
    module lim = is-limit lim
    open is-indexed-product hiding (eta)

    ip : is-indexed-product C F (eta .Ξ·)
    ip .tuple k =
      lim.universal k
        (J (Ξ» j p β†’ subst (Hom (F _) βŠ™ F) p id ∘ k _ ≑ k j)
           (eliml (transport-refl _)))
    ip .commute =
      lim.factors _ _
    ip .unique k comm =
      lim.unique _ _ _ comm

  IP→Limit : Indexed-product C F → Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F)
  IP→Limit ip =
    to-limit (is-indexed-product→is-limit has-is-ip)
    where open Indexed-product ip

  Limit→IP : Limit {C = C} (Disc-adjunct {iss = i-is-grpd} F) → Indexed-product C F
  Limit→IP lim .Indexed-product.ΠF = _
  Limit→IP lim .Indexed-product.π = _
  Limit→IP lim .Indexed-product.has-is-ip =
    is-limit→is-indexed-product (Limit.has-limit lim)