Library interfaces.Limits

Require Import interfaces.Category.
Require Import interfaces.Functor.
Require Import interfaces.MonoidalCategory.
Require Import interfaces.FunctorCategory.
Require Import FunctionalExtensionality.
Require Import ProofIrrelevance.

Products

Category with all products

Module Type ProductsDefinition (C : CategoryDefinition).

  Parameter prod : ∀ {I}, (I → C.t ) → C.t.
  Parameter pi : ∀ {I A}, ∀ i:I, C.m (prod A) (A i).
  Parameter tuple : ∀ {I X A}, (∀ i:I, C.m X (A i)) → C.m X (prod A).

  Axiom pi_tuple :
    ∀ {I X A} (f : ∀ i:I, C.m X (A i)),
      ∀ i, C.compose (pi i) (tuple f) = f i.

  Axiom tuple_pi :
    ∀ {I X A} (x : C.m X (@prod I A)),
      tuple (fun i ⇒ C.compose (pi i) x) = x.

End ProductsDefinition.

Module ProductsTheory (C : CategoryDefinition) (P : ProductsDefinition C).
  Import P.

  Lemma pi_tuple_rewrite {I X Y A} (f : ∀ i:I, C.m Y (A i)) (g : C.m X Y) :
    ∀ i, C.compose (pi i) (C.compose (tuple f) g) = C.compose (f i) g.

  Lemma tuple_uni {I X A} (f : ∀ i:I, C.m X (A i)) (x : C.m X (prod A)) :
    (∀ i, C.compose (pi i) x = f i ) → x = tuple f.
End ProductsTheory.

Module Type Products (C : CategoryDefinition) :=
  ProductsDefinition C <+
  ProductsTheory C.

Derived cartesian structure

If we have all products then in particular with have a cartesian structure. However in some cases the derived structure below is not the most natural or convenient definition. For example in SET we will want to use Rocq's built-in unit and prod types to define the cartesian structure rather than the equivalent but awkward ∀ i:Empty_set, _ and ∀ i:bool, if i then A else B. Hence we don't include the following in ProductsTheory but provide it separately to use as needed.

Module CartesianStructureFromProducts (C : Category) (P : Products C)
    <: CartesianStructure C.

  Definition unit :=
    P.prod (fun i : Empty_set ⇒ match i with end).

  Definition ter X : C.m X unit :=
    P.tuple (fun i : Empty_set ⇒ match i with end).

  Proposition ter_uni {X} (x y : C.m X unit) :
    x = y.

  Definition omap A B :=
    P.prod (fun i:bool ⇒ if i then A else B).

  Definition p1 {A B} : C.m (omap A B) A :=
    P.pi true.

  Definition p2 {A B} : C.m (omap A B) B :=
    P.pi false.

  Definition pair {X A B} (f : C.m X A) (g : C.m X B) : C.m X (omap A B) :=
    P.tuple
      (fun i:bool ⇒ if i return C.m X (if i then A else B) then f else g).

  Proposition p1_pair {X A B} (f : C.m X A) (g : C.m X B) :
    C.compose p1 (pair f g) = f.

  Proposition p2_pair {X A B} (f : C.m X A) (g : C.m X B) :
    C.compose p2 (pair f g) = g.

  Proposition pair_pi {X A B} (x : C.m X (omap A B)) :
    pair (C.compose p1 x) (C.compose p2 x) = x.

  Include CartesianStructureTheory C.
  Include BifunctorTheory C C C.
End CartesianStructureFromProducts.

Module CartesianFromProducts (C : Category) (P : Products C) <: Cartesian C.
  Module Prod := CartesianStructureFromProducts C P.
  Include CartesianTheory C.
End CartesianFromProducts.

Preservation

Note that this only works when both the source and target category have all products. It would be preferable to define product preservation when particular products may or may not exist in C and D; when all products do exist the definition would be equivalent to the following. However this would require basing the definition on a notion of an object and projection morphisms being a product, which would be best defined elsewhere.

Module Type PreservesProducts (C : CategoryDefinition) (D : Category)
  (PC : Products C) (PD : Products D) (F : Functor C D).

  Import (notations, coercions) D.

  Parameter omap_prod :
    ∀ {I} (A : I → C.t),
      D.iso (F.omap (PC.prod A)) (PD.prod (fun i ⇒ F.omap (A i))).

  Parameter fmap_pi :
    ∀ {I} (A : I → C.t) (i : I),
      F.fmap (PC.pi i) = PD.pi i @ omap_prod A.

End PreservesProducts.

Coproducts

Category with all coproducts

Module Type CoproductsDefinition (C : CategoryDefinition).

  Parameter coprod : ∀ {I}, (I → C.t ) → C.t.
  Parameter iota : ∀ {I A}, ∀ i:I, C.m (A i) (coprod A).
  Parameter cotuple : ∀ {I X A}, (∀ i:I, C.m (A i) X ) → C.m (coprod A) X.

  Axiom cotuple_iota :
    ∀ {I X A} (f : ∀ i:I, C.m (A i) X),
      ∀ i, C.compose (cotuple f) (iota i) = f i.

  Axiom iota_cotuple :
    ∀ {I X A} (x : C.m (@coprod I A) X),
      cotuple (fun i ⇒ C.compose x (iota i)) = x.

End CoproductsDefinition.

Module CoproductsTheory (C : CategoryDefinition) (P : CoproductsDefinition C).
  Import P.

  Lemma cotuple_iota_rewrite {I X Y A} (f: ∀ i:I, C.m (A i) Y) i (g: C.m X (A i)):
    C.compose (cotuple f) (C.compose (iota i) g) = C.compose (f i) g.

  Lemma cotuple_uni {I X A} (f : ∀ i:I, C.m (A i) X) (x : C.m (coprod A) X) :
    (∀ i, C.compose x (iota i) = f i ) → x = cotuple f.
End CoproductsTheory.

Module Type Coproducts (C : CategoryDefinition) :=
  CoproductsDefinition C <+
  CoproductsTheory C.

Limits in general

Limits of shape J in a category C

Module LimitsPreliminaries (J C : CategoryDefinition).

Module Diagram := FunctorCategory J C.

A cone over a diagram

  Record cone {F : Diagram.t} :=
    {
      vertex :> C.t;
      edge (j : J.t) : C.m vertex (Diagram.oapply F j);
      face {i j} (f : J.m i j) :
        C.compose (Diagram.fapply F f) (edge i) = edge j;
    }.

  Arguments cone : clear implicits.

  Record cone_mor {F} {x y : cone F} :=
    {
      vertex_mor :> C.m x y;
      edge_mor j : C.compose (edge y j) vertex_mor = edge x j;
    }.

  Arguments cone_mor {_} _ _.

  Lemma cone_mor_eq {F x y} (m1 m2 : @cone_mor F x y) :
    vertex_mor m1 = vertex_mor m2 → m1 = m2.

A limit is a terminal cone

  Class Limit {F} (l : cone F) :=
    {
      lim_mor (x : cone F) : cone_mor x l;
      lim_uni {x} (m : cone_mor x l) : m = lim_mor x;
    }.

End LimitsPreliminaries.

Module Type Limits (J C : CategoryDefinition).
  Include LimitsPreliminaries J C.

  Parameter lim : ∀ F, cone F.
  Axiom lim_spec : ∀ F, Limit (lim F).

End Limits.

Module Type Colimits (J : CategoryDefinition) (C : Category) :=
  Limits J C.Op.

Specific types of limits

Require Import MonoidalCategory.

The discrete category with two objects is used for the product and coproduct diagrams.

Module D2 <: Category.

  Variant m_def : bool → bool → Type :=
    | id_def A : m_def A A.

  Definition t : Type := bool.
  Definition m : t → t → Type := m_def.

  Definition id : ∀ A, m A A := id_def.

  Program Definition compose {A B C} (g : m B C) : m A B → m A C :=
    match g with
      | id_def A ⇒ fun f ⇒ f
    end.

  Lemma compose_id_left {A B} (f : m A B) :
    compose (id B) f = f.

  Lemma compose_id_right {A B} (f : m A B) :
    compose f (id A) = f.

  Lemma compose_assoc {A B C D} (f : m A B) (g : m B C) (h : m C D) :
    compose (compose h g) f = compose h (compose g f).

  Include CategoryTheory.
End D2.

Module CartesianStructureLimit (C : CartesianCategory).
  Include LimitsPreliminaries D2 C.
  Import (notations) C.

  Program Definition prod_d (A B : C.t) : Diagram.t :=
    {|
      Diagram.oapply j := if j then A else B;
      Diagram.fapply i j f :=
        match f with D2.id_def j ⇒ C.id (if j then A else B) end;
    |}.

  Program Canonical Structure prod_c A B : cone (prod_d A B) :=
    {|
      vertex := A && B;
      edge j :=
        if j return A && B ~~> Diagram.oapply (prod_d A B) j
        then C.Prod.p1
        else C.Prod.p2;
    |}.

End CartesianStructureLimit.