open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Limit.Base
open import Cat.Instances.Discrete
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Bool

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

open import Cat.Reasoning C

open is-product
open Product
open Functor
open _=>_


# 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:

PairβCone
: β {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.

is-productβis-limit
: β {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
where
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)

is-limitβis-product
: β {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

pair
: β {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

pair-commutes
: β {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.

canonical-functors
: β (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))
p

is-indexed-productβis-limit
: β {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
where
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 _))
p
ml .universal eta p = ip.tuple eta
ml .factors eta p = ip.commute
ml .unique eta p other q = ip.unique eta q

is-limitβis-indexed-product
: β {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)