Coq で圏論 2016 年 12 月 ver.

cat_on_coq_201612.v

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Set Reversible Pattern Implicit.

Generalizable All Variables.

Set Primitive Projections.
Set Universe Polymorphism.

(* cmorphisms... *)
Require Export Coq.Program.Basics Coq.Program.Tactics Coq.Setoids.Setoid Coq.Classes.Morphisms.

Obligation Tactic := (try split); program_simpl; try now auto.

(** * 0. Setoid and Map **)
Structure Setoid: Type :=
  {
    setoid_carrier:> Type;
    setoid_equal: setoid_carrier -> setoid_carrier -> Prop;

    setoid_prf:> Equivalence setoid_equal
  }.
Existing Instance setoid_prf.

Notation "[ 'Setoid' 'by' P 'on' A ]" := (@Build_Setoid A P _).
Notation "[ 'Setoid' 'by' P ]" := [Setoid by P on _].

Notation "(== 'in' A )" := (setoid_equal A).
Notation "x == y 'in' A" := (setoid_equal A x y) (at level 70, y at next level, no associativity).
Notation "(==)" := (== in _).
Notation "x == y" := (x == y in _) (at level 70, no associativity).

Program Definition eq_setoid (X: Type) :=
  [Setoid by @eq X].

Program Definition function (X Y: Type): Setoid :=
  [Setoid by `(forall x, f x = g x) on X -> Y].
Next Obligation.
  intros f g h Heqfg Heqgh x.
  now rewrite Heqfg.
Qed.

Class IsMap {X Y: Setoid}(f: X -> Y) :=
  {
    map_proper:> Proper ((==) ==> (==)) f
  }.

Structure Map (X Y: Setoid): Type :=
  {
    map_fun:> X -> Y;

    map_prf:> IsMap map_fun
  }.
Existing Instance map_prf.

Notation "[ 'Map' 'by' f ]" := (@Build_Map _ _ f _).
Notation "[ x 'in' X :-> m ]" := [Map by fun (x: X) => m].
Notation "[ x :-> m ]" := ([ x in _ :-> m]).

Program Definition Map_compose (X Y Z: Setoid)(f: Map X Y)(g: Map Y Z): Map X Z :=
  [ x :-> g (f x)].
Next Obligation.
  intros x y Heq; simpl.
  now rewrite Heq.
Qed.

Program Definition Map_id (X: Setoid): Map X X :=
  [ x :-> x ].

Program Definition Map_setoid (X Y: Setoid): Setoid :=
  [Setoid by `(forall x, f x == g x) on Map X Y].
Next Obligation.
  intros f g h Heqfg Heqgh x.
  now rewrite Heqfg.
Qed.
Canonical Structure Map_setoid.

(** * 1. Category, Functor, Natural Transformation **)
(** ** 1.1 Category **)
(** *** 1.1.1 Definition **)
Class IsCategory
      (obj: Type)
      (hom: obj -> obj -> Setoid)
      (comp: forall {X Y Z: obj}, hom X Y -> hom Y Z -> hom X Z)
      (id: forall (X: obj), hom X X) :=
  {
    cat_comp_proper:>
      forall (X Y Z: obj),
        Proper ((==) ==> (==) ==> (==)) (@comp X Y Z);
    
    cat_comp_assoc:
      forall X Y Z W (f: hom X Y)(g: hom Y Z)(h: hom Z W),
        comp f (comp g h) == comp (comp f g) h;
    
    cat_comp_id_dom:
      forall X Y (f: hom X Y),
        comp (id X) f == f;
    
    cat_comp_id_cod:
      forall X Y (f: hom X Y),
        comp f (id Y) == f
  }.
Hint Resolve cat_comp_assoc cat_comp_id_dom cat_comp_id_cod.

Structure Category :=
  {
    cat_obj:> Type;
    cat_hom:> cat_obj -> cat_obj -> Setoid;
    cat_comp:
      forall (X Y Z: cat_obj),
        cat_hom X Y -> cat_hom Y Z -> cat_hom X Z;
    cat_id: forall X: cat_obj, cat_hom X X;

    cat_prf:> IsCategory cat_comp cat_id
  }.
Existing Instance cat_prf.

Notation "[ 'Category' 'by' hom 'with' comp , id ]" :=
  (@Build_Category _ hom comp id _).
Notation "[ 'Category' 'by' hom 'with' 'comp' := comp 'with' 'id' := id ]" :=
  [Category by hom with comp , id].

Notation "g \o{ C } f" := (@cat_comp C _ _ _ f g) (at level 60, right associativity).
Notation "g \o f" := (g \o{_} f) (at level 60, right associativity) .
Notation "Id_{ C } X" := (@cat_id C X) (at level 20, no associativity).
Notation "'Id' X" := (Id_{_} X) (at level 30, right associativity).

Definition domain {C: Category}{X Y: C}(f: C X Y) := X.
Definition codomain {C: Category}{X Y: C}(f: C X Y) := Y.

(** isomorphic **)
Definition isomorphic (C: Category)(X Y: C) :=
  exists (f: C X Y)(g: C Y X),
    (g \o f == Id X) /\ (f \o g == Id Y).

Program Definition isomorphic_setoid (C: Category) :=
  [Setoid by isomorphic C on C].
Next Obligation.
  - intros X.
    exists (Id X), (Id X); split.
    + now rewrite cat_comp_id_dom.
    + now rewrite cat_comp_id_cod.
  - intros X Y [f [g [Heqfg Heqgf]]].
    now exists g, f.
  - intros X Y Z [f [f' [Heqf Heqf']]] [g [g' [Heqg Heqg']]].
    exists (g \o f), (f' \o g'); split.
    + rewrite cat_comp_assoc, <- (cat_comp_assoc f), Heqg.
      now rewrite cat_comp_id_cod, Heqf.
    + rewrite cat_comp_assoc, <- (cat_comp_assoc g'), Heqf'.
      now rewrite cat_comp_id_cod, Heqg'.
Qed.
Notation "X === Y 'in' C" := (X == Y in (isomorphic_setoid C)) (at level 70, no associativity, Y at next level).
Notation "X === Y" := (X === Y in _) (at level 70, no associativity).

(** *** 1.1.2 Examples **)
(** Category of Type **)
Program Definition Types :=
  [Category by function
   with (fun X Y Z f g x => g (f x)),
        (fun X x => x)].
Next Obligation.
  intros f f' Heqf g g' Heqg x; simpl.
  now rewrite Heqf, Heqg.
Qed.

(** Category of Setoid **)
Program Definition Setoids :=
  [Category by Map_setoid with Map_compose, Map_id].
Next Obligation.
  intros f f' Heqf g g' Heqg x; simpl.
  now rewrite (Heqf x), (Heqg (f' x)).
Qed.
Canonical Structure Setoids.

(** Discrete category **)
Program Definition Prop_setoid (P: Prop) :=
  [Setoid by (fun _ _ => True) on P].

Program Definition DiscreteCategory (X: Setoid): Category :=
  [Category by `(Prop_setoid (x == y)) with _,_].
Next Obligation.
  revert H H0.
  now apply transitivity.
Qed.

(** Dual category **)
Program Definition DualCategory (C: Category): Category :=
  [Category by (fun X Y => C Y X)
   with (fun X Y Z (f: C Y X)(g: C Z Y) => f \o g),
        (fun X => Id X)].
Next Obligation.
  - now intros f f' Heqf g g' Heqg; rewrite Heqf, Heqg.
  - now rewrite cat_comp_assoc.
  - now rewrite cat_comp_id_cod.
  - now rewrite cat_comp_id_dom.
Qed.
Notation "C ^op" := (DualCategory C) (at level 0, format "C ^op").

(** ** 1.2 Functor **)
(** *** 1.2.1 Definition **)
Class IsFunctor (C D: Category)
      (fobj: C -> D)
      (fmap: forall {X Y: C}, C X Y -> D (fobj X) (fobj Y)) :=
  {
    fmap_subst:>
              forall X Y: C, Proper ((==) ==> (==)) (@fmap X Y);
    fmap_comp:
      forall (X Y Z: C)(f: C X Y)(g: C Y Z),
        fmap (g \o{C} f) == fmap g \o{D} fmap f;
    fmap_id:
      forall X: C, fmap (Id X) == Id (fobj X)
  }.

Structure Functor (C D: Category): Type :=
  {
    fun_obj:> C -> D;
    fmap: forall {X Y: C}, C X Y -> D (fun_obj X) (fun_obj Y);

    fun_prf:> IsFunctor (@fmap)
  }.
Existing Instance fun_prf.

Notation "C --> D" := (Functor C D).
Arguments fmap_comp {C D fobj fmap F}{X Y Z}(f g): rename, clear implicits.
Arguments fmap_id {C D fobj fmap F}(X): rename, clear implicits.

Notation "[ 'Functor' 'by' fmap 'with' fobj ; C 'to' D ]" := (@Build_Functor C D fobj fmap _).
Notation "[ 'Functor' 'by' fmap 'with' fobj ]" := [Functor by fmap with fobj ; _ to _].
Notation "[ 'Functor' 'by' fmap ]" := [Functor by fmap with _].
Notation "[ 'Functor' 'by' f :-> Ff 'with' X :-> FX ; C 'to' D ]" := [Functor by (fun _ _ f => Ff) with (fun X => FX) ; C to D].
Notation "[ 'Functor' 'by' f :-> Ff 'with' X :-> FX ]" := [Functor by f :-> Ff with X :-> FX ; _ to _].
Notation "[ 'Functor' 'by' f :-> Ff ; C 'to' D ]" :=
  [Functor by f :-> Ff with _ :-> _ ; _ to _].
Notation "[ 'Functor' 'by' f :-> Ff ]" := [Functor by f :-> Ff with _ :-> _ ; _ to _].

Program Definition Functor_compose (C D E: Category)(F: C --> D)(G: D --> E): C --> E :=
  [Functor by f :-> fmap G (fmap F f)].
Next Obligation.
  - intros f f' Heqf; simpl.
    now rewrite Heqf.
  - now rewrite !(fmap_comp _).
  - now rewrite !(fmap_id _).
Qed.  

Program Definition Functor_id (C: Category): C --> C :=
  [Functor by f :-> f].

(** *** 1.2.2 Category of Category **)
(** homogenous equality on Hom **)
Inductive hom_eq (C : Category)(X Y: C)(f: C X Y):
  forall (Z W: C), C Z W -> Prop :=
  hom_eq_def:
    forall (g: C X Y), f == g -> hom_eq f g.
Notation "f =H g 'in' C" := (@hom_eq C _ _ f _ _ g) (at level 70, g at next level).
Infix "=H" := hom_eq (at level 70, only parsing).

Lemma hom_eq_refl:
  forall (C: Category)(df cf: C)(bf: C df cf),
    bf =H bf.
Proof.
  intros C df cf bf; apply hom_eq_def; reflexivity.
Qed.

Lemma hom_eq_sym:
  forall (C: Category)
         (df cf: C)(bf: C df cf)
         (dg cg: C)(bg: C dg cg),
    bf =H bg -> bg =H bf.
Proof.
  intros C df cf bf dg cg bg [g Heq].
  apply hom_eq_def; apply symmetry; assumption.
Qed.

Lemma hom_eq_trans:
  forall (C : Category)
         (df cf: C)(bf: C df cf)
         (dg cg: C)(bg: C dg cg)
         (dh ch: C)(bh: C dh ch),
    bf =H bg -> bg =H bh -> bf =H bh.
Proof.
  intros C df cf bf dg cg bg dh ch bh [g Heqg] [h Heqh].
  apply hom_eq_def.
  transitivity g; assumption.
Qed.

Program Definition Functor_setoid (C D: Category): Setoid :=
  [Setoid by `(forall (X Y: C)(f: C X Y), fmap F f =H fmap G f) on C --> D].
Next Obligation.
  - intros F G Heq X Y f.
    now apply hom_eq_sym, Heq.
  - intros F G H HeqFG HeqGH X Y f.
    eapply hom_eq_trans.
    + now apply HeqFG.
    + now apply HeqGH.
Qed.
Canonical Structure Functor_setoid.

Program Definition Cat: Category :=
  [Category by Functor_setoid with Functor_compose, Functor_id].
Next Obligation.
  rename X into C, Y into D, Z into E.
  intros F F' HeqF G G' HeqG X Y f; simpl in *.
  destruct (HeqF _ _ f).
  destruct (HeqG _ _ g).
  apply hom_eq_def.
  now rewrite H, H0.
Qed.
Canonical Structure Cat.

(** *** 1.2.3 Examples **)
(* constant functor *)
Program Definition constant_functor (C D: Category)(d: D): C --> D :=
  [Functor by f :-> Id d with c :-> d].
Next Obligation.
  now rewrite cat_comp_id_dom.
Qed.
Notation "[ * 'in' D |-> c 'in' C ]" := (constant_functor D C c).

(** Hom(X,-): C -> Setoids **)
Program Definition covariant_hom_functor (C: Category)(X: C)
  : C --> Setoids :=
  [Functor by (fun (Y Z: C)(g: C Y Z) => [ f in C X Y :-> g \o f])
   with (fun Y => C X Y)].
Next Obligation.
  now intros f f' Heq; rewrite Heq.
Qed.
Next Obligation.
  - rename X0 into Y, Y into Z.
    intros g g' Heqg f; simpl.
    now rewrite Heqg.
  - now rewrite cat_comp_assoc.
  - now rewrite cat_comp_id_cod.
Qed.
Notation "'Hom' ( X , -)" := (covariant_hom_functor _ X).

(** Hom(-,Y): C^op -> Setoids **)
Program Definition contravariant_hom_functor (C: Category)(Y: C)
  : C^op --> Setoids :=
  [Functor by (fun (X W: C)(f: C W X) =>
                 [g in C X Y :-> g \o f] )
   with (fun X => C X Y)].
Next Obligation.
  now intros g g' Heq; rewrite Heq.
Qed.
Next Obligation.
  - rename Y0 into W.
    intros f f' Heqf g; simpl.
    now rewrite Heqf.
  - now rewrite cat_comp_assoc.
  - now rewrite cat_comp_id_dom.
Qed.
Notation "'Hom' (- , Y )" := (contravariant_hom_functor _ Y).

(** ** 1.3 Natural Transformation **)
(** *** 1.3.1 Definition **)
Class IsNatrans
      (C D: Category)
      (F G: C --> D)
      (natrans: forall (X: C), D (F X) (G X)) :=
  {
    natrans_naturality:
      forall (X Y: C)(f: C X Y),
        natrans Y \o fmap F f == fmap G f \o natrans X
  }.

Structure Natrans {C D: Category}(F G: C --> D): Type :=
  {
    natrans:> forall X: C, D (F X) (G X);
    natrans_prf:> IsNatrans natrans
  }.
Existing Instance natrans_prf.

Notation "F ==> G" := (Natrans F G).
Notation "[ X 'in' T :=> f 'from' F 'to' G ]" := (@Build_Natrans _ _ F G (fun X: T => f) _).
Notation "[ X :=> f 'from' F 'to' G ]" := [X in _ :=> f from F to G].
Notation "[ X 'in' T :=> f ]" := [X in T :=> f from _ to _].
Notation "[ X :=> f ]" := ([ X in _ :=> f]).

Program Definition Natrans_compose (C D: Category)(F G H: C --> D)(S: F ==> G)(T: G ==> H): F ==> H :=
  [X :=> T X \o S X].
Next Obligation.
  now rewrite cat_comp_assoc, (natrans_naturality (IsNatrans := S)), <- cat_comp_assoc, (natrans_naturality (IsNatrans:=T)), cat_comp_assoc.
Qed.

Program Definition Natrans_id (C D: Category)(F: C --> D): Natrans F F :=
  [X :=> Id (F X)].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition Natrans_dom_compose (B C D: Category)(E: B --> C)(F G: C --> D)(S: F ==> G): (F \o E) ==> (G \o E) :=
  [X :=> S (E X)].
Next Obligation.
  now rewrite natrans_naturality.
Qed.
Notation "S o> E" := (Natrans_dom_compose E S) (at level 50, left associativity).

Program Definition Natrans_cod_compose (C D E: Category)(F G: C --> D)(H: D --> E)(S: F ==> G): (H \o F) ==> (H \o G) :=
  [X :=> fmap H (S X)].
Next Obligation.
  now rewrite <- !(fmap_comp _), natrans_naturality.
Qed.
Notation "H <o S" := (Natrans_cod_compose H S) (at level 50, left associativity).

Program Definition Natrans_hcompose
        (C D E: Category)
        (F G: C --> D)(H K: D --> E)
        (S: F ==> G)(T: H ==> K)
  : (H \o F) ==> (K \o G) :=
  [ X :=> fmap K (S X) \o T (F X) ].
Next Obligation.
  rewrite cat_comp_assoc, natrans_naturality, <- !cat_comp_assoc.
  rewrite <- !(fmap_comp ).
  now rewrite <- (natrans_naturality (IsNatrans:=S)).
Qed.
Notation "T <o> S" := (Natrans_hcompose S T) (at level 60, right associativity).


Program Definition Natrans_setoid (C D: Category)(F G: C --> D): Setoid :=
  [Setoid by (fun (S T: F ==> G) => forall X, S X == T X)].
Next Obligation.
  intros S T U HeqST HeqTU X.
  now rewrite (HeqST X), (HeqTU X).
Qed.
Canonical Structure Natrans_setoid.


Program Definition Fun (C D: Category): Category :=
  [Category by (@Natrans_setoid C D)
   with (@Natrans_compose C D), (@Natrans_id C D)].
Next Obligation.
  - rename X into F, Y into G, Z into H.
  intros S S' HeqS T T' HeqT X; simpl.
  now rewrite HeqS, HeqT.

  - now rewrite cat_comp_assoc.
    
  - now rewrite cat_comp_id_dom.

    -now rewrite cat_comp_id_cod.
Qed.
Canonical Structure Fun.
Notation "D ^ C" := (Fun C D).


(** ** 1.4 Yoneda Lemma **)
Program Definition yoneda_map (C: Category)(X: C)(F: C --> Setoids)
  : Map (Natrans_setoid Hom(X,-) F) (F X) :=
  [ S in Natrans Hom(X,-) F :-> S X (Id X) ].


Program Definition inv_yoneda_map (C: Category)(X: C)(F: C --> Setoids)
  : Map (F X) (Natrans_setoid Hom(X,-) F) :=
  [ x in F X :-> [ Y in C :=> [ f in C X Y :-> fmap F f x ]]].
Next Obligation.
  intros f f' Heq.
  now apply (fmap_subst (IsFunctor:=F) Heq x).
Qed.
Next Obligation.
  now rewrite (fmap_comp (F:=F) _ _ x).
Qed.
Next Obligation.
  now intros x y Heq Y f; simpl; rewrite Heq.
Qed.

(* Yoneda Lemma *)
Definition injective (X Y: Setoid)(f: Map X Y) :=
  forall x y, f x == f y -> x == y.
Definition surjective (X Y: Setoid)(f: Map X Y) :=
  forall (y: Y), exists x: X, f x == y.
Definition bijective (X Y: Setoid)(f: Map X Y) :=
  injective f /\ surjective f.
Definition equiv (X Y: Setoid) :=
  exists f: Map X Y, bijective f.

Theorem yoneda_lemma:
  forall (C: Category)(X: C)(F: C --> Setoids),
    equiv ((Setoids^C) Hom(X,-) F) (F X).
Proof.
  intros; exists (yoneda_map X F).
  unfold bijective, injective, surjective; split; simpl.
  - intros S T Heq Y f.
    generalize (natrans_naturality (IsNatrans:=S) f (Id X)); simpl.
    rewrite cat_comp_id_dom; intros H; rewrite H; clear H.
    generalize (natrans_naturality (IsNatrans:=T) f (Id X)); simpl.
    rewrite cat_comp_id_dom; intros H; rewrite H; clear H.
    now rewrite Heq.
  - intros x.
    exists (inv_yoneda_map X F x); simpl.
    now rewrite (fmap_id (F:=F) X x).
Qed.

(** * 2. Universal Property **)
(** ** 2.1 Initial and Terminal **)
(** *** 2.1.1 Definitions **)
Class IsInitial (C: Category)
      (obj: C)
      (univ: forall X: C, C obj X) :=
  {
    initial_uniqueness:
      forall (X: C)(f: C obj X),
        f == univ X
  }.

Structure Initial (C: Category) :=
  {
    initial_obj:> C;
    initial_univ: forall X: C, C initial_obj X;

    initial_prf:> IsInitial initial_univ
  }.
Existing Instance initial_prf.

Notation "[ 'Initial' i 'by' univ ]" := (@Build_Initial _ i univ _).
Notation "[ 'Initial' 'by' univ ]" := [Initial _ by univ].

Class IsTerminal (C: Category)
      (obj: C)
      (univ: forall X: C, C X obj) :=
  {
    terminal_uniqueness:
      forall (X: C)(f: C X obj),
        f == univ X
  }.

Structure Terminal (C: Category) :=
  {
    terminal_obj:> C;
    terminal_univ: forall X: C, C X terminal_obj;

    terminal_prf:> IsTerminal terminal_univ
  }.
Existing Instance terminal_prf.

Notation "[ 'Terminal' t 'by' univ ]" := (@Build_Terminal _ t univ _).
Notation "[ 'Terminal' 'by' univ ]" := [Terminal _ by univ].

(** *** 2.1.2 Isomorphic **)
Lemma initial_isomorphic:
  forall (C: Category)(i i': Initial C),
    i === i' in C.
Proof.
  intros C i i'; simpl; unfold isomorphic.
  exists (initial_univ i i'), (initial_univ i' i); split.
  - rewrite (initial_uniqueness (Id i)).
    now apply initial_uniqueness.
  - rewrite (initial_uniqueness (Id i')).
    now apply initial_uniqueness.
Qed.

Lemma terminal_isomorphic:
  forall (C: Category)(t t': Terminal C),
    t === t' in C.
Proof.
  intros C t t'; simpl; unfold isomorphic.
  exists (terminal_univ t' t), (terminal_univ t t'); split.
  - rewrite (terminal_uniqueness (Id t)).
    now apply terminal_uniqueness.
  - rewrite (terminal_uniqueness (Id t')).
    now apply terminal_uniqueness.
Qed.

(** *** 2.1.3 Duality **)
Program Definition terminal_from_initial (C: Category)(i: Initial C): Terminal C^op :=
  [Terminal by (initial_univ i)].
Next Obligation.
  now apply initial_uniqueness.
Qed.

Program Definition initial_from_terminal (C: Category)(t: Terminal C): Initial C^op :=
  [Initial by (terminal_univ t)].
Next Obligation.
  now apply terminal_uniqueness.
Qed.

(** *** 2.1.3 Examples **)
(** Initial of Types, Setoids, Cat **)
Inductive empty := .

Program Definition initial_of_Types: Initial Types :=
  [Initial empty by (fun (X: Type)(e: empty) => match e with end)].

Program Definition empty_setoid: Setoid :=
  [Setoid by (fun e e' => match e, e' with end) on empty].

Program Definition initial_of_Setoids: Initial Setoids :=
  [Initial empty_setoid
    by (fun (X: Setoid) => [e in empty :-> match e with end])].

Program Definition Zero: Category :=
  [Category by (fun (e e': empty) => match e, e' with end)
   with (fun X Y Z f g => match X with end),
        (fun X => match X with end)].

Program Definition FromZero (C: Category): Zero --> C :=
  [Functor by (fun X Y f => match X with end)
   with (fun (X: empty) => match X with end)].

Program Definition initial_of_Cat: Initial Cat :=
  [Initial Zero by @FromZero].

(** Terminal of Types, Setoids, Cat **)
Inductive unit := tt.

Program Definition terminal_of_Types: Terminal Types :=
  [Terminal unit by (fun (X: Type)(_: X) => tt)].
Next Obligation.
  now destruct (f x).
Qed.

Program Definition unit_setoid: Setoid :=
  [Setoid by (fun x y => True) on unit].

Program Definition terminal_of_Setoids: Terminal Setoids :=
  [Terminal unit_setoid by (fun (X: Setoid) => [_ in X :-> tt])].

Program Definition One: Category :=
  [Category by (fun _ _ => unit_setoid)
   with (fun X Y Z f g => match X, Y, Z with tt, tt, tt => tt end),
        (fun X => match X with tt => tt end)].
Canonical Structure One.

Program Definition ToOne (C: Category): C --> One :=
  [Functor by f :-> Id tt with X :-> tt].

Program Definition terminal_of_Cat: Terminal Cat :=
  [Terminal One by @ToOne].
Next Obligation.
  rename X into C, f into F, X0 into X, f0 into f.
  destruct (fmap F f), (F X), (F Y).
  now apply hom_eq_refl.
Qed.


(** ** 2.2 Product **)
(** *** 2.2.1 Definitions **)
Class IsProduct (C: Category)(X Y: C)
      (P: C)(pi1: C P X)(pi2: C P Y)
      (univ: forall (Z: C), C Z X -> C Z Y -> C Z P) :=
  {
    product_universality_1:
      forall (Z: C)(p1: C Z X)(p2: C Z Y),
        (p1 == pi1 \o univ Z p1 p2);

    product_universality_2:
      forall (Z: C)(p1: C Z X)(p2: C Z Y),
        (p2 == pi2 \o univ Z p1 p2);
    
    product_uniqueness:
      forall (Z: C)(p1: C Z X)(p2: C Z Y)(u: C Z P),
        (p1 == pi1 \o u) ->
        (p2 == pi2 \o u) ->
        u == univ Z p1 p2
  }.

Structure Product (C: Category)(X Y: C) :=
  {
    product_obj:> C;
    product_proj1: C product_obj X;
    product_proj2: C product_obj Y;

    product_univ: forall (Z: C), C Z X -> C Z Y -> C Z product_obj;

    product_prf:> IsProduct product_proj1 product_proj2 (@product_univ)
  }.
Existing Instance product_prf.

Notation "[ 'Product' P 'by' univ 'with' pi1 , pi2 ]" :=
  (@Build_Product _ _ _ P pi1 pi2 univ _).
Notation "[ 'Product' 'by' univ 'with' pi1 , pi2 ]" :=
  [Product _ by univ with pi1, pi2].

Notation "[ f , g 'to' P ]" := (product_univ P f g).
Notation "pi1_{ P }" := (product_proj1 P) (at level 0, no associativity, format "pi1_{ P }").
Notation "pi2_{ P }" := (product_proj2 P) (at level 0, no associativity, format "pi2_{ P }").

Program Instance product_univ_proper (C: Category)(X Y: C)
        (prod: Product C X Y)
        (Z: C)
  : Proper ((== in C Z X) ==> (== in C Z Y) ==> (==))
           (@product_univ _ _ _ prod Z).
Next Obligation.
  intros f f' Heqf g g' Heqg.
  apply (product_uniqueness (IsProduct:=prod)(p1:=f')(p2:=g')(u:=[f , g to prod])).
  - rewrite <- Heqf.
    now apply (product_universality_1 (IsProduct:=prod) f g).
  - rewrite <- Heqg.
    now apply (product_universality_2 (IsProduct:=prod) f g).
Qed.  

Definition product_map (C: Category)(prod: forall (X Y: C), Product C X Y)
           (X X' Y Y': C)(f: C X Y)(g: C X' Y')
  : C (prod X X') (prod Y Y') :=
  [f \o pi1_{prod X X'} , g \o pi2_{prod X X'} to (prod Y Y')].
Notation "[ f \* g 'with' prod ]" := (product_map prod f g).

Program Instance product_map_proper
        (C: Category)(prod: forall (X Y: C), Product C X Y)
        (X X' Y Y': C)
  : Proper ((==) ==> (==) ==> (==)) (@product_map _ prod X X' Y Y').
Next Obligation.
  intros f f' Heqf g g' Heqg.
  unfold product_map.
  now rewrite Heqf, Heqg.
Qed.

Lemma product_map_compose:
  forall (C: Category)(prod: forall (X Y: C), Product C X Y)
         (X X' Y Y' Z Z': C)
         (f: C X Y)(g: C Y Z)
         (f': C X' Y')(g': C Y' Z'),
    [(g \o f) \* (g' \o f') with prod] ==
    [g \* g' with prod] \o [ f \* f' with prod].
Proof.
  intros.
  unfold product_map.
  symmetry.
  apply (product_uniqueness (IsProduct:=prod Z Z')).
  - rewrite <- cat_comp_assoc.
    rewrite <- (product_universality_1 (IsProduct:=prod Z Z') _ _).
    rewrite !cat_comp_assoc.
    now rewrite <- (product_universality_1 (IsProduct:=prod Y Y') _ _).
  - rewrite <- cat_comp_assoc.
    rewrite <- (product_universality_2 (IsProduct:=prod Z Z') _ _).
    rewrite !cat_comp_assoc.
    now rewrite <- (product_universality_2 (IsProduct:=prod Y Y') _ _).
Qed.

Lemma product_map_id:
  forall (C: Category)(prod: forall (X Y: C), Product C X Y)
         (X X': C),
    [Id X \* Id X' with prod] == Id (prod X X').
Proof.
  intros.
  unfold product_map.
  rewrite !cat_comp_id_cod.
  symmetry.
  now apply (product_uniqueness (IsProduct:=prod X X'));
    rewrite !cat_comp_id_dom.
Qed.

(** *** 2.2.2 Isomorphic **)
Lemma product_isomorphic:
  forall (C: Category)(X Y: C)(P Q: Product C X Y),
    P === Q in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists [pi1_{P}, pi2_{P} to Q], [pi1_{Q}, pi2_{Q} to P]; split.
  - rewrite (product_uniqueness (p1:=pi1_{P})(p2:=pi2_{P})(u:=Id P));
      try now rewrite cat_comp_id_dom.
    apply product_uniqueness.
    + rewrite <- cat_comp_assoc.
      rewrite <- (product_universality_1 (IsProduct:=P)).
      now rewrite <- (product_universality_1 (IsProduct:=Q)).
    + rewrite <- cat_comp_assoc.
      rewrite <- (product_universality_2 (IsProduct:=P)).
      now rewrite <- (product_universality_2 (IsProduct:=Q)).
  - rewrite (product_uniqueness (p1:=pi1_{Q})(p2:=pi2_{Q})(u:=Id Q));
      try now rewrite cat_comp_id_dom.
    apply product_uniqueness.
    + rewrite <- cat_comp_assoc.
      rewrite <- (product_universality_1 (IsProduct:=Q)).
      now rewrite <- (product_universality_1 (IsProduct:=P)).
    + rewrite <- cat_comp_assoc.
      rewrite <- (product_universality_2 (IsProduct:=Q)).
      now rewrite <- (product_universality_2 (IsProduct:=P)).
Qed.


(** *** 2.2.3 Examples **)
Record product (A B: Type): Type :=
 pair_of { fst: A; snd: B }.
Notation "( x , y )" := (pair_of x y) (format "( x ,  y )").

Notation "p .1" := (fst p) (at level 5, left associativity, format "p .1").
Notation "p .2" := (snd p) (at level 5, left associativity, format "p .2").

Program Definition product_of_types (X Y: Type)
  : Product Types X Y :=
  [Product (product X Y) by (fun P f g x => (f x, g x))
   with @fst X Y, @snd X Y].
Next Obligation.
  generalize (H x), (H0 x).
  now destruct (u x); simpl; intros; subst.
Qed.

Program Definition product_setoid (X Y: Setoid): Setoid :=
  [Setoid by `((p.1 == q.1) /\ (p.2 == q.2)) on product X Y].
Next Obligation.
  repeat split; program_simpl; try now auto.
  - now rewrite H.
  - now rewrite H2.
Qed.

Program Instance fst_proper (X Y: Setoid)
  : Proper ((== in product_setoid X Y) ==> (== in X)) (@fst X Y).

Program Instance snd_proper (X Y: Setoid)
  : Proper ((== in product_setoid X Y) ==> (== in Y)) (@snd X Y).

Program Instance pair_of_proper (X Y: Setoid)
  : Proper ((== in X) ==> (== in Y) ==> (== in product_setoid X Y)) (@pair_of X Y).

Program Definition product_of_Setoids (X Y: Setoid)
  : Product Setoids X Y :=
  [Product (product_setoid X Y)
    by (fun P f g => [x :-> (f x, g x)])
   with [Map by @fst X Y],
        [Map by @snd X Y]].
Next Obligation.
  now intros p q Heq; simpl; rewrite Heq.
Qed.

Program Definition product_category (C D: Category): Category :=
  [Category by (fun X Y => product_setoid (C X.1 Y.1) (D X.2 Y.2))
   with (fun X Y Z f g => (g.1 \o f.1, g.2 \o f.2)),
        (fun X => (Id X.1, Id X.2))].
Next Obligation.
  - repeat split; program_simpl; try now auto.
    + now rewrite H, H0.
    + now rewrite H1, H2.
  - now rewrite !cat_comp_assoc.
  - now rewrite !cat_comp_id_dom.
  - now rewrite !cat_comp_id_cod.
Qed.

Program Definition functor_for_product_of_Cat (C D: Category)
        (B: Category)(F: B --> C)(G: B --> D)
  : B --> (product_category C D) :=
  [Functor by f :-> (fmap F f, fmap G f)
   with b :-> (F b, G b)].
Next Obligation.
  - now intros f g Heq; simpl; rewrite Heq.
  - now rewrite !fmap_comp.
  - now rewrite !fmap_id.
Qed.

Program Definition product_of_Cat (C D: Category)
  : Product Cat C D :=
  [Product (product_category C D)
    by (@functor_for_product_of_Cat C D)
   with [Functor by fg :-> fg.1 with XY :-> XY.1],
        [Functor by fg :-> fg.2 with XY :-> XY.2]].
Next Obligation.
  generalize (H _ _ f), (H0 _ _ f); clear H H0; intros H1 H2.
  destruct (fmap u f); simpl in *.
  destruct (u X), (u Y); simpl in *.
  destruct H1, H2.
  now apply hom_eq_def; rewrite H, H0.
Qed.

(** ** 2.3 Coproduct **)
(** *** 2.3.1 Definitions **)
Class IsCoproduct (C: Category)(X Y: C)
      (CP: C)(in1: C X CP)(in2: C Y CP)
      (univ: forall (Z: C), C X Z -> C Y Z -> C CP Z) :=
  {
    coproduct_universality_1:
      forall (Z: C)(i1: C X Z)(i2: C Y Z),
        (i1 == univ Z i1 i2 \o in1);
    
    coproduct_universality_2:
      forall (Z: C)(i1: C X Z)(i2: C Y Z),
        (i2 == univ Z i1 i2 \o in2);
    
    coproduct_uniqueness:
      forall (Z: C)(i1: C X Z)(i2: C Y Z)(u: C CP Z),
        (i1 == u \o in1) ->
        (i2 == u \o in2) ->
        u == univ Z i1 i2
  }.

Structure Coproduct (C: Category)(X Y: C) :=
  {
    coproduct_obj:> C;
    coproduct_inj1: C X coproduct_obj;
    coproduct_inj2: C Y coproduct_obj;

    coproduct_univ: forall (Z: C), C X Z -> C Y Z -> C coproduct_obj Z;

    coproduct_prf:> IsCoproduct coproduct_inj1 coproduct_inj2 (@coproduct_univ)
  }.
Existing Instance coproduct_prf.

Notation "[ 'Coproduct' P 'by' univ 'with' in1 , in2 ]" :=
  (@Build_Coproduct _ _ _ P in1 in2 univ _).
Notation "[ 'Coproduct' 'by' univ 'with' in1 , in2 ]" :=
  [Coproduct _ by univ with in1, in2].

Notation "[ f , g 'from' P ]" := (coproduct_univ P f g).
Notation "in1_{ P }" := (coproduct_inj1 P) (at level 0, no associativity, format "in1_{ P }").
Notation "in2_{ P }" := (coproduct_inj2 P) (at level 0, no associativity, format "in2_{ P }").

Program Instance coproduct_univ_proper (C: Category)(X Y: C)
        (cp: Coproduct C X Y)
        (Z: C)
  : Proper ((== in C X Z) ==> (== in C Y Z) ==> (==))
           (@coproduct_univ _ _ _ cp Z).
Next Obligation.
  intros f f' Heqf g g' Heqg.
  apply coproduct_uniqueness.
  - rewrite <- Heqf.
    now apply coproduct_universality_1.
  - rewrite <- Heqg.
    now apply coproduct_universality_2.
Qed.  

Definition coproduct_map (C: Category)
           (coprod: forall (X Y: C), Coproduct C X Y)
           (X X' Y Y': C)(f: C X Y)(g: C X' Y')
  : C (coprod X X') (coprod Y Y') :=
  [in1_{coprod Y Y'} \o f, in2_{coprod Y Y'} \o g from (coprod X X')].
Notation "[ f \+ g 'with' coprod ]" := (coproduct_map coprod f g).

Program Instance coproduct_map_proper
        (C: Category)(coprod: forall (X Y: C), Coproduct C X Y)
        (X X' Y Y': C)
  : Proper ((==) ==> (==) ==> (==)) (@coproduct_map _ coprod X X' Y Y').
Next Obligation.
  intros f f' Heqf g g' Heqg.
  unfold coproduct_map.
  now rewrite Heqf, Heqg.
Qed.

Lemma coproduct_map_compose:
  forall (C: Category)(coprod: forall (X Y: C), Coproduct C X Y)
         (X X' Y Y' Z Z': C)
         (f: C X Y)(g: C Y Z)
         (f': C X' Y')(g': C Y' Z'),
    [(g \o f) \+ (g' \o f') with coprod] ==
    [g \+ g' with coprod] \o [ f \+ f' with coprod].
Proof.
  intros.
  unfold coproduct_map.
  symmetry.
  apply coproduct_uniqueness.
  - rewrite cat_comp_assoc.
    rewrite <- (coproduct_universality_1 _ _).
    rewrite <- !cat_comp_assoc.
    now rewrite <- (coproduct_universality_1 _ _).
  - rewrite cat_comp_assoc.
    rewrite <- (coproduct_universality_2 _ _).
    rewrite <- !cat_comp_assoc.
    now rewrite <- (coproduct_universality_2 _ _).
Qed.

Lemma coproduct_map_id:
  forall (C: Category)(coprod: forall (X Y: C), Coproduct C X Y)
         (X X': C),
    [Id X \+ Id X' with coprod] == Id (coprod X X').
Proof.
  intros.
  unfold coproduct_map.
  rewrite !cat_comp_id_dom.
  symmetry.
  now apply (coproduct_uniqueness); rewrite !cat_comp_id_cod.
Qed.

(** *** 2.3.2 Isomorphic **)
Lemma coproduct_isomorphic:
  forall (C: Category)(X Y: C)(P Q: Coproduct C X Y),
    P === Q in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists [in1_{Q}, in2_{Q} from P], [in1_{P}, in2_{P} from Q]; split.
  - rewrite (coproduct_uniqueness (i1:=in1_{P})(i2:=in2_{P})(u:=Id P));
      try now rewrite cat_comp_id_cod.
    apply coproduct_uniqueness.
    + rewrite cat_comp_assoc.
      rewrite <- (coproduct_universality_1 (IsCoproduct:=P)).
      now rewrite <- (coproduct_universality_1 (IsCoproduct:=Q)).
    + rewrite cat_comp_assoc.
      rewrite <- (coproduct_universality_2 (IsCoproduct:=P)).
      now rewrite <- (coproduct_universality_2 (IsCoproduct:=Q)).
  - rewrite (coproduct_uniqueness (i1:=in1_{Q})(i2:=in2_{Q})(u:=Id Q));
      try now rewrite cat_comp_id_cod.
    apply coproduct_uniqueness.
    + rewrite cat_comp_assoc.
      rewrite <- (coproduct_universality_1 (IsCoproduct:=Q)).
      now rewrite <- (coproduct_universality_1 (IsCoproduct:=P)).
    + rewrite cat_comp_assoc.
      rewrite <- (coproduct_universality_2 (IsCoproduct:=Q)).
      now rewrite <- (coproduct_universality_2 (IsCoproduct:=P)).
Qed.

(** *** 2.3.3 Examples **)
Inductive coproduct (A B: Type): Type :=
| inj1: A -> coproduct A B
| inj2: B -> coproduct A B.

Program Definition coproduct_of_Types (X Y: Type)
  : Coproduct Types X Y :=
  [Coproduct (coproduct X Y)
    by (fun P f g xy => match xy with
                        | inj1 _ x => f x
                        | inj2 _ y => g y
                        end)
   with @inj1 X Y, @inj2 X Y].
Next Obligation.
  destruct x as [x | y].
  - now rewrite H.
  - now rewrite H0.
Qed.

Program Definition coproduct_setoid (X Y: Setoid) :=
  [Setoid by (fun a b => match a, b with
                         | inj1 _ x, inj1 _ x' => x == x' in X
                         | inj2 _ y, inj2 _ y' => y == y' in Y
                         | _, _ => False
                         end)].
Next Obligation.
  - now intros [x | y].
  - now intros [x | y] [x' | y'].
  - intros [x | y] [x' | y'] [x'' | y'']; try contradiction;
      now apply transitivity.
Qed.

Program Instance inj1_proper (X Y: Setoid)
  : Proper ((== in X) ==> (== in coproduct_setoid X Y)) (@inj1 X Y).

Program Instance inj2_proper (X Y: Setoid)
  : Proper ((== in Y) ==> (== in coproduct_setoid X Y)) (@inj2 X Y).

Program Definition coproduct_of_Setoids (X Y: Setoid)
  : Coproduct Setoids X Y :=
  [Coproduct (coproduct_setoid X Y)
    by (fun P f g => [xy :-> match xy with
                             | inj1 _ x => f x
                             | inj2 _ y => g y
                             end])
   with [Map by @inj1 X Y],
        [Map by @inj2 X Y]].
Next Obligation.
  intros [x | y] [x' | y']; try contradiction; now apply map_proper.
Qed.
Next Obligation.
  destruct x as [x | y]; symmetry.
  - now apply H.
  - now apply H0.
Qed.

Definition coproduct_hom (C D: Category)(X Y: coproduct C D): Setoid :=
  match X, Y with
  | inj1 _ X, inj1 _ Y => C X Y
  | inj2 _ X, inj2 _ Y => D X Y
  | _, _ => empty_setoid
  end.

Program Definition coproduct_category (C D: Category): Category :=
  [Category by (@coproduct_hom C D)
   with (fun X Y Z f g => _),
        (fun X => match X with
                  | inj1 _ X => Id X
                  | inj2 _ X => Id X
                  end)].
Next Obligation.
  destruct X as [X | X], Y as [Y | Y], Z as [Z | Z]; simpl in *;
    try contradiction.
  - exact (g \o f).
  - exact (g \o f).
Defined.
Next Obligation.
  - now destruct X as [X | X], Y as [Y | Y], Z as [Z | Z]; 
      intros f f' Heqf g g' Heqg; simpl in *;
        try contradiction; rewrite Heqf, Heqg.
  - destruct X as [X | X], Y as [Y | Y], Z as [Z | Z], W as [W | W];
      simpl in *; try contradiction;
        now rewrite !cat_comp_assoc.
  - destruct X as [X | X], Y as [Y | Y];
      simpl in *; try contradiction;
        now rewrite cat_comp_id_dom.
  - destruct X as [X | X], Y as [Y | Y];
      simpl in *; try contradiction;
        now rewrite cat_comp_id_cod.
Qed.

Definition fobj_for_coproduct_of_Cat (C D: Category)
           (E: Category)(F: C --> E)(G:D --> E)
  : coproduct_category C D -> E :=
  fun X => match X with
           | inj1 _ X => F X
           | inj2 _ X => G X
           end.

Program Definition functor_for_coproduct_of_Cat (C D: Category)
        (E: Category)(F: C --> E)(G:D --> E)
  : (coproduct_category C D) --> E :=
  let fobj := fobj_for_coproduct_of_Cat F G in
  [Functor by (fun X Y =>
                 match X as X', Y as Y' return
                       (coproduct_category C D) X' Y' ->
                       E (fobj X')
                         (fobj Y') with
                 | inj1 _ X, inj1 _ Y => fun f => fmap F f
                 | inj2 _ X, inj2 _ Y => fun f => fmap G f
                 | _, _ => fun f => match f with end
                 end)].
Next Obligation.
  - now destruct X as [X | X], Y as [Y | Y];
      intros f f' Heq; simpl in *;
        try contradiction; rewrite Heq.
  - now destruct X as [X | X], Y as [Y | Y], Z as [Z | Z]; simpl in *;
      try contradiction; rewrite fmap_comp.
  - now destruct X; simpl; rewrite fmap_id.
Qed.

Program Definition coproduct_of_Cat (C D: Category)
  : Coproduct Cat C D :=
  [Coproduct (coproduct_category C D)
    by @functor_for_coproduct_of_Cat C D
   with [Functor by f :-> f with X :-> inj1 D X],
        [Functor by f :-> f with X :-> inj2 C X]].
Next Obligation.
  - destruct X as [X | X], Y as [Y | Y]; simpl in *;
      try contradiction; apply hom_eq_sym.
    + now apply H.
    + now apply H0.
Qed.

(** ** 2.4 Equalizer **)
(** *** 2.4.1 Definition **)
Class IsEqualizer (C: Category)(X Y: C)(f g: C X Y)
      (Eq: C)
      (eq: C Eq X)
      (univ: forall {Z: C}{k: C Z X},
          f \o k == g \o k -> C Z Eq) :=
  {
    equalize: f \o eq == g \o eq;

    equalizer_universality: forall Z (k: C Z X)(Heq: f \o k == g \o k),
        eq \o (univ Heq) == k;

    equalizer_uniqueness: forall Z (k: C Z X)(Heq: f \o k == g \o k)(u: C Z Eq),
          eq \o u == k -> u == univ Heq
  }.

Structure Equalizer (C: Category)(X Y: C)(f g: C X Y) :=
  {
    equalizer_obj: C;
    equalizer_map:> C equalizer_obj X;
    equalizer_univ: forall (Z: C)(k: C Z X), f \o k == g \o k -> C Z equalizer_obj;

    equalizer_prf:> IsEqualizer equalizer_map equalizer_univ
  }.
Existing Instance equalizer_prf.

Notation "[ 'Equalizer' 'of' f , g 'by' univ 'with' map 'from' Eq 'in' C ]" :=
  (@Build_Equalizer C _ _ f g Eq map univ _).
Notation "[ 'Equalizer' 'of' f , g 'by' univ 'with' map ]" :=
  [Equalizer of f,g by univ with map from _ in _].
Notation "[ 'Equalizer' 'by' univ 'with' map ]" :=
  [Equalizer of _,_ by univ with map].
Notation "[ 'Equalizer' 'by' univ ]" := [Equalizer by univ with _].

Lemma equalizer_univ_subst
      (C: Category)(X Y: C)(f g: C X Y)
      (eq: Equalizer f g)
      (Z: C)(k k': C Z X)
      (Heq: f \o k == g \o k)
      (Heq': f \o k' == g \o k'):
  k == k' -> 
  equalizer_univ eq Heq == equalizer_univ eq Heq'.
Proof.
  intros Heqk.
  apply equalizer_uniqueness; symmetry; rewrite <- Heqk.
  now rewrite equalizer_universality.
Qed.

(** *** 2.4.2 Isomorphic **)
Lemma equalizer_isomorphic:
  forall (C: Category)(X Y: C)(f g: C X Y)
         (eq eq': Equalizer f g),
    equalizer_obj eq === equalizer_obj eq' in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists (equalizer_univ eq' (equalize (IsEqualizer:=eq))),
  (equalizer_univ eq (equalize (IsEqualizer:=eq'))); split.
  - rewrite (equalizer_uniqueness (equalize (IsEqualizer:=eq)) (u:=Id (equalizer_obj eq))); [| now rewrite cat_comp_id_dom].
    apply equalizer_uniqueness.
    now rewrite <- cat_comp_assoc, !equalizer_universality.
  - rewrite (equalizer_uniqueness (equalize (IsEqualizer:=eq')) (u:=Id (equalizer_obj eq'))); [| now rewrite cat_comp_id_dom].
    apply equalizer_uniqueness.
    now rewrite <- cat_comp_assoc, !equalizer_universality.
Qed.

(** *** 2.4.3 Example **)
(** Equalizer of Setoids **)
Class IsPredicate (X: Setoid)(P: X -> Prop) :=
  {
    predicate_proper:> Proper ((== in X) ==> iff) P
  }.

Structure Predicate (X: Setoid) :=
  {
    predicate:> X -> Prop;
    predicate_prf:> IsPredicate X predicate
  }.
Existing Instance predicate_prf.

Notation "[ 'Predicate' 'by' P 'on' X ]" := (@Build_Predicate X P _).
Notation "[ 'Predicate' 'by' P ]" := [Predicate by P on _].

Inductive SubSetoid_type (X: Setoid)(P: Predicate X) :=
| subsetoid_def (x: X)(Hp: P x).
Notation "[ x 'satisfies' P 'on' X ]" := (@subsetoid_def X P x _).
Notation "[ x 'satisfies' P ]" := [x satisfies P on _].

Definition elem {X: Setoid}{P: Predicate X}(x: SubSetoid_type P): X :=
  match x with
  | @subsetoid_def _ _ x _ => x
  end.

Program Definition SubSetoid (X: Setoid)(P: Predicate X) :=
  [Setoid by `(elem x == elem y) on SubSetoid_type P].
Next Obligation.
  - now intros [x Hx] [y Hy] [z Hz]; transitivity y.
Qed.
Notation "{{ x 'in' X | P }}" := (SubSetoid [Predicate by fun x => P on X]).

Program Definition elem_map (X: Setoid)(P: Predicate X)
  : Map (SubSetoid P) X :=
  [Map by @elem _ P].

Program Definition equalize_predicate (X Y: Setoid)(f g: Map X Y) :=
  [Predicate by `(f x == g x) on X].
Next Obligation.
  now intros x y Heq; rewrite Heq.
Qed.

Program Definition equalizer_of_Setoids (X Y: Setoid)(f g: Map X Y)
  : Equalizer (C:=Setoids) f g:=
  [Equalizer of f, g
    by (fun Z k H => [z :-> subsetoid_def (H z)])
   with elem_map _ from {{x in X | f x == g x }}
     in Setoids].
Next Obligation.
  now intros x y Heq; rewrite Heq.
Qed.
Next Obligation.
  intros x y Heq.
  unfold elem.
  now rewrite Heq.
Qed.
Next Obligation.
  destruct x; unfold elem.
  now apply Hp.
Qed.


(** ** 2.5 Coequalizer **)
(** *** 2.5.1 Definition **)
Class IsCoequalizer (C: Category)(X Y: C)(f g: C X Y)
      (Coeq: C)
      (coeq: C Y Coeq)
      (univ: forall {Z: C}{h: C Y Z},
          h \o f == h \o g -> C Coeq Z) :=
  {
    coequalize: coeq \o f == coeq \o g;

    coequalizer_universality: forall Z (h: C Y Z)(Heq: h \o f == h \o g),
        (univ Heq) \o coeq == h;

    coequalizer_uniqueness: forall Z (h: C Y Z)(Heq: h \o f == h \o g)(u: C Coeq Z),
          u \o coeq == h -> u == univ Heq
  }.

Structure Coequalizer (C: Category)(X Y: C)(f g: C X Y) :=
  {
    coequalizer_obj: C;
    coequalizer_map:> C Y coequalizer_obj;
    coequalizer_univ: forall (Z: C)(h:C Y Z), h \o f == h \o g -> C coequalizer_obj Z;

    coequalizer_prf:> IsCoequalizer coequalizer_map coequalizer_univ
  }.
Existing Instance coequalizer_prf.

Notation "[ 'Coequalizer' 'of' f , g 'by' univ 'with' map 'to' Coeq 'in' C ]" :=
  (@Build_Coequalizer C _ _ f g Coeq map univ _).
Notation "[ 'Coequalizer' 'of' f , g 'by' univ 'with' map ]" :=
  [Coequalizer of f,g by univ with map to _ in _].
Notation "[ 'Coequalizer' 'by' univ 'with' map ]" :=
  [Coequalizer of _,_ by univ with map].
Notation "[ 'Coequalizer' 'by' univ ]" := [Coequalizer by univ with _].

Lemma coequalizer_univ_subst
      (C: Category)(X Y: C)(f g: C X Y)
      (coeq: Coequalizer f g)
      (Z: C)(h h': C Y Z)
      (Heq: h \o f == h \o g)
      (Heq': h' \o f == h' \o g):
  h == h' -> 
  coequalizer_univ coeq Heq == coequalizer_univ coeq Heq'.
Proof.
  intros Heqh.
  apply coequalizer_uniqueness; symmetry; rewrite <- Heqh.
  now rewrite coequalizer_universality.
Qed.

(** *** 2.5.2 Isomorphic **)
Lemma coequalizer_isomorphic:
  forall (C: Category)(X Y: C)(f g: C X Y)
         (eq eq': Coequalizer f g),
    coequalizer_obj eq === coequalizer_obj eq' in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists (coequalizer_univ eq (coequalize (IsCoequalizer:=eq'))),  (coequalizer_univ eq' (coequalize (IsCoequalizer:=eq))); split.
  - rewrite (coequalizer_uniqueness (coequalize (IsCoequalizer:=eq)) (u:=Id (coequalizer_obj eq))); [| now rewrite cat_comp_id_cod].
    apply coequalizer_uniqueness.
    now rewrite cat_comp_assoc, !coequalizer_universality.
  - rewrite (coequalizer_uniqueness (coequalize (IsCoequalizer:=eq')) (u:=Id (coequalizer_obj eq'))); [| now rewrite cat_comp_id_cod].
    apply coequalizer_uniqueness.
    now rewrite cat_comp_assoc, !coequalizer_universality.
Qed.

(** *** 2.5.3 Example **)
(** Coequalizer of Setoids **)
Class IsRelation (X: Setoid)(R: X -> X -> Prop) :=
  {
    relation_proper:> Proper ((== in X) ==> (== in X) ==> iff) R
  }.

Structure Relation (X: Setoid) :=
  {
    relation_rel:> X -> X -> Prop;
    relation_prf:> IsRelation X relation_rel
  }.
Existing Instance relation_prf.
Notation "[ 'Rel' 'by' rel 'on' X ]" := (@Build_Relation X rel _).

Inductive EquivClosure (A: Setoid)(R: Relation A): A -> A -> Prop :=
| eqcl_base: forall a b, R a b -> EquivClosure R a b
| eqcl_refl: forall a b: A, a == b -> EquivClosure R a b
| eqcl_sym: forall a b: A, EquivClosure R a b -> EquivClosure R b a
| eqcl_trans: forall a b c, EquivClosure R a b -> EquivClosure R b c -> EquivClosure R a c.

Program Instance EquivClosure_Equivalence (A: Setoid)(R: Relation A)
  : Equivalence (EquivClosure R).
Next Obligation.
  now intros x; apply eqcl_refl.
Qed.
Next Obligation.
  now intros x y; apply eqcl_sym.
Qed.
Next Obligation.
  now intros x y z; apply eqcl_trans.
Qed.

Program Definition EqCl (X: Setoid)(R: Relation X) :=
  [Rel by EquivClosure R on X].
Next Obligation.
  split; intros.
  - revert y y0 H H0.
    induction H1; intros.
    + apply eqcl_base.
      now rewrite <- H0, <- H1.
    + rewrite H0, H1 in H.
      now apply eqcl_refl.
    + now apply eqcl_sym, IHEquivClosure.
    + apply eqcl_trans with b.
      * now apply IHEquivClosure1.
      * now apply IHEquivClosure2.
  - rename x into y, y into x, x0 into y0, y0 into x0.
    revert y y0 H H0.
    induction H1; intros.
    + apply eqcl_base.
      now rewrite H0, H1.
    + rewrite <- H0, <- H1 in H.
      now apply eqcl_refl.
    + now apply eqcl_sym, IHEquivClosure.
    + apply eqcl_trans with b.
      * now apply IHEquivClosure1.
      * now apply IHEquivClosure2.
Qed.
    
Program Definition QuotientSetoid (X: Setoid)(R: Relation X)
        (Heq: Equivalence R) :=
  [Setoid by R on X].

Inductive coequalize_pair (X Y: Setoid)(f g: Map X Y): Y -> Y -> Prop :=
| coequalize_pair_def: forall (x: X)(y y': Y),
    f x == y -> g x == y' ->
    coequalize_pair f g y y'.

Program Definition coequalize_pair_relation (X Y: Setoid)(f g: Map X Y) :=
  [Rel by coequalize_pair f g on Y].
Next Obligation.
  split; intros.
  - destruct H1.
    apply coequalize_pair_def with x.
    + now rewrite H in H1.
    + now rewrite H0 in H2.
  - destruct H1.
    apply coequalize_pair_def with x1.
    + now rewrite H.
    + now rewrite H0.
Qed.

Program Definition coequalizer_of_Setoids (X Y: Setoid)(f g: Map X Y) :=
  [Coequalizer of f, g
    by (fun z h H => [ y :-> h y])
   with [y :-> y]
   to QuotientSetoid (EqCl (coequalize_pair_relation f g)) (EquivClosure_Equivalence Y (coequalize_pair_relation f g))
     in Setoids].
Next Obligation.
  intros y y' Heq.
  now apply eqcl_refl.
Qed.
Next Obligation.
  intros y y' Hr.
  induction Hr.
  - destruct H0.
    rewrite <- H0, <- H1.
    now rewrite (H x).
  - now rewrite H0.
  - now symmetry.
  - now transitivity (h b).
Qed.    
Next Obligation.
  now apply eqcl_base, coequalize_pair_def with x.
Qed.

(** ** 2.6 Exponential **)
(** *** 2.6.1 Definition **)
Class IsExponential
      (C: Category)
      (prod: forall (X Y: C), Product C X Y)
      (Y Z: C)
      (exp: C)(ev: C (prod exp Y) Z)
      (univ: forall (X: C)(g: C (prod X Y) Z), C X exp) :=
  {
    exp_universality:
      forall (X: C)(g: C (prod X Y) Z),
        g == ev \o [univ X g \* Id Y with prod];
    exp_uniqueness:
      forall (X: C)(g: C (prod X Y) Z)(u: C X exp),
        g == ev \o [u \* Id Y with prod] ->
        u == univ X g
  }.

Structure Exponential
          (C: Category)(prod: forall (X Y: C), Product C X Y)
          (Y Z: C) :=
  {
    exp_obj:> C;
    exp_eval: C (prod exp_obj Y) Z;
    exp_univ: forall (X: C), C (prod X Y) Z -> C X exp_obj;

    exp_prf:> IsExponential exp_eval exp_univ
  }.
Existing Instance exp_prf.

Notation "[ 'Exp' exp 'by' univ 'with' eval ]" :=
  (@Build_Exponential _ _ _ _ exp eval univ _).
Notation "[ 'Exp' 'by' univ 'with' eval ]" :=
  [Exp _ by univ with eval].
Notation "[ 'curry' f 'to' exp ]" := (exp_univ exp f) (f at next level).

Program Instance exponential_univ_proper
        (C: Category)
        (prod: forall (X Y: C), Product C X Y)
        (Y Z: C)
        (exp: Exponential prod Y Z)
        (X: C)
  : Proper ((==) ==> (==)) (@exp_univ _ prod _ _ exp X).
Next Obligation.
  intros f g Heq.
  apply (exp_uniqueness (IsExponential:=exp)).
  rewrite <- Heq.
  now apply (exp_universality (IsExponential:=exp)).
Qed.

(** *** 2.6.2 Isomorphic **)
Lemma exponential_isomorphic:
  forall (C: Category)
         (prod: forall (X Y: C), Product C X Y)
         (Y Z: C)(exp exp': Exponential prod Y Z),
    exp === exp' in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists [curry (exp_eval exp) to exp'], [curry (exp_eval exp') to exp]; split.
  - rewrite (exp_uniqueness (g:=exp_eval exp)(u:=Id exp)).
    + apply exp_uniqueness.
      rewrite <- (cat_comp_id_dom (Id Y)), product_map_compose.
      now rewrite <- cat_comp_assoc, <- !exp_universality.
    + now rewrite product_map_id, cat_comp_id_dom.
  - rewrite (exp_uniqueness (g:=exp_eval exp')(u:=Id exp')).
    + apply exp_uniqueness.
      rewrite <- (cat_comp_id_dom (Id Y)), product_map_compose.
      now rewrite <- cat_comp_assoc, <- !exp_universality.
    + now rewrite product_map_id, cat_comp_id_dom.
Qed.

(** *** 2.6.3 Examples **)
Program Definition exponential_of_Setoids (Y Z: Setoids)
  : Exponential (C:=Setoids) product_of_Setoids Y Z :=
  [Exp (Setoids Y Z)
    by (fun (X: Setoid) f => [x :-> [y :-> f (x, y)]])
   with [gy :-> gy.1 gy.2]].
Next Obligation.
  intros [g y] [g' y'] [Heqg Heqy]; simpl in *.
  now rewrite Heqy, Heqg.
Qed.
Next Obligation.
  now intros y y' Heq; rewrite Heq.
Qed.
Next Obligation.
  now intros x x' Heq y; simpl; rewrite Heq.
Qed.
Next Obligation.
  rename g into f, u into g, x0 into y.
  now rewrite (H (x, y)).
Qed.

(** * 3. Limit and Colimit **)
(** ** 3.1 Limit **)
(** *** 3.1.1 Definition **)
Class IsCone
      (J C: Category)
      (D: J --> C)
      (apex: C)
      (gen: forall i, C apex (D i)) :=
  {
    cone_commute:
      forall i j (u: J i j),
        fmap D u \o gen i == gen j
  }.

Structure Cone (J C: Category)(D: J --> C): Type :=
  {
    cone_apex:> C;
    cone_gen:> forall i, C cone_apex (D i);
    cone_prf:> IsCone cone_gen
  }.
Existing Instance cone_prf.

Notation "[ 'Cone' 'of' D 'by' gen 'from' apex ]" := (@Build_Cone _ _ D apex gen _).
Notation "[ 'Cone' 'by' gen 'from' apex ]" := [Cone of _ by gen from apex].
Notation "[ 'Cone' 'by' gen ]" := [Cone by gen from _].
Notation "[ 'Cone' 'by' i :-> f 'from' apex ]" := [Cone by (fun i => f) from apex].
Notation "[ 'Cone' 'by' i :-> f ]" := [Cone by i :-> f from _].

Class IsLimit (J C: Category)(D: J --> C)
      (obj: Cone D)
      (univ: forall c: Cone D, C c obj) :=
  {
    limit_universality:
      forall (c: Cone D)(i: J),
        obj i \o univ c == c i;
    
    limit_uniqueness:
      forall (c: Cone D)(u: C c obj),
        (forall i: J, obj i \o u == c i) ->
        u == univ c
  }.

Structure Limit (J C: Category)(D: J --> C) :=
  {
    limit_obj:> Cone D;
    limit_univ: forall c: Cone D, C c limit_obj;

    limit_prf:> IsLimit limit_univ
  }.
Existing Instance limit_prf.

Notation "[ 'Limit' obj 'by' univ 'of' D ]" := (@Build_Limit _ _ D obj univ _).
Notation "[ 'Limit' 'by' univ 'of' D ]" := [Limit _ by univ of D].
Notation "[ 'Limit' obj 'by' univ ]" := [Limit obj by univ of _].
Notation "[ 'Limit' 'by' univ ]" := [Limit by univ of _].

(** *** 3.1.2 Isomorphic **)
Lemma limit_isomorphic:
  forall (J C: Category)(D: J --> C)
         (lim lim': Limit D),
    lim === lim' in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists (limit_univ lim' lim), (limit_univ lim lim'); split.
  - rewrite (limit_uniqueness (u:=Id lim)).
    + apply limit_uniqueness; intros i.
      now rewrite <- cat_comp_assoc, !limit_universality.
    + now intros i; rewrite cat_comp_id_dom.
  - rewrite (limit_uniqueness (u:=Id lim')).
    + apply limit_uniqueness; intros i.
      now rewrite <- cat_comp_assoc, !limit_universality.
    + now intros i; rewrite cat_comp_id_dom.
Qed.

(** *** 3.1.3 Terminality of Limit **)
Class IsConeMap
      (J C: Category)
      (D: J --> C)
      (c d: Cone D)
      (map: C c d) :=
  {
    cone_map_commute:
      forall i: J,
        d i \o map == c i
  }.

Structure ConeMap
          (J C: Category)
          (D: J --> C)
          (c d: Cone D) :=
  {
    cone_map_map:> C c d;
    cone_map_prf:> IsConeMap cone_map_map
  }.
Existing Instance cone_map_prf.
Notation "[ 'ConeMap' 'by' f ]" := (@Build_ConeMap _ _ _ _ _ f _).

Program Definition ConeMap_compose (J C: Category)(D: J --> C)(c d e: Cone D)(f: ConeMap c d)(g: ConeMap d e)
  : ConeMap c e :=
  [ConeMap by g \o f].
Next Obligation.
  now rewrite <- cat_comp_assoc, !cone_map_commute.
Qed.

Program Definition ConeMap_id (J C: Category)(D: J --> C)(c: Cone D): ConeMap c c :=
  [ConeMap by Id c].
Next Obligation.
  now rewrite cat_comp_id_dom.
Qed.

Program Definition ConeMap_setoid (J C: Category)(D: J --> C)(c d: Cone D): Setoid :=
  [Setoid by `(f == g) on ConeMap c d].
Next Obligation.
  now intros f g h Heqfg Heqgh; rewrite Heqfg, Heqgh.
Qed.

Program Definition Cones (J C: Category)(D: J --> C): Category :=
  [Category by @ConeMap_setoid J C D
   with @ConeMap_compose J C D,
        @ConeMap_id J C D].
Next Obligation.
  - rename X into c, Y into d, Z into e.
    intros f f' Heqf g g' Heqg; simpl in *.
    now rewrite Heqf, Heqg.
  - now rewrite cat_comp_assoc.
  - now rewrite cat_comp_id_dom.
  - now rewrite cat_comp_id_cod.
Qed.

Program Definition limit_by_terminal_of_cones
        (J C: Category)(D: J --> C)(t: Terminal (Cones D)): Limit D :=
  [Limit by terminal_univ t].
Next Obligation.
  - now apply (cone_map_commute (IsConeMap:=terminal_univ t c)).
  - now apply (terminal_uniqueness (IsTerminal:=t) (X:=c) (Build_ConeMap (Build_IsConeMap H))).
Qed.


(** ** 3.2 Colimit **)
(** *** 3.2.1 Definition **)
Class IsCocone
      (J C: Category)(D: J --> C)
      (apex: C)
      (gen: forall i: J, C (D i) apex) :=
  {
    cocone_commute:
      forall (i j: J)(u: J i j),
        gen j \o fmap D u == gen i
  }.

Structure Cocone (J C: Category)(D: J --> C): Type :=
  {
    cocone_apex:> C;
    cocone_gen:> forall i: J, C (D i) cocone_apex;

    cocone_prf:> IsCocone cocone_gen
  }.
Existing Instance cocone_prf.

Notation "[ 'Cocone' 'of' D 'by' gen 'to' apex ]" := (@Build_Cocone _ _ D apex gen _).
Notation "[ 'Cocone' 'by' gen 'to' apex ]" := [Cocone of _ by gen to apex].
Notation "[ 'Cocone' 'by' gen ]" := [Cocone by gen to _].
Notation "[ 'Cocone' 'by' i :-> f 'to' apex ]" := [Cocone by (fun i => f) to apex].
Notation "[ 'Cocone' 'by' i :-> f ]" := [Cocone by i :-> f to _].


Class IsColimit (J C: Category)(D: J --> C)
      (obj: Cocone D)
      (univ: forall c: Cocone D, C obj c) :=
  {
    colimit_universality:
      forall (c: Cocone D)(i: J),
        univ c \o obj i == c i;
    
    colimit_uniqueness:
      forall (c: Cocone D)(u: C obj c),
        (forall i: J, u \o obj i == c i) ->
        u == univ c
  }.

Structure Colimit (J C: Category)(D: J --> C) :=
  {
    colimit_obj:> Cocone D;
    colimit_univ: forall c: Cocone D, C colimit_obj c;

    colimit_prf:> IsColimit colimit_univ
  }.
Existing Instance colimit_prf.

Notation "[ 'Colimit' obj 'by' univ 'of' D ]" := (@Build_Colimit _ _ D obj univ _).
Notation "[ 'Colimit' 'by' univ 'of' D ]" := [Colimit _ by univ of D].
Notation "[ 'Colimit' obj 'by' univ ]" := [Colimit obj by univ of _].
Notation "[ 'Colimit' 'by' univ ]" := [Colimit by univ of _].

(** *** 3.1.2 Isomorphic **)
Lemma colimit_isomorphic:
  forall (J C: Category)(D: J --> C)
         (colim colim': Colimit D),
    colim === colim' in C.
Proof.
  intros; simpl; unfold isomorphic.
  exists (colimit_univ colim colim'), (colimit_univ colim' colim); split.
  - rewrite (colimit_uniqueness (u:=Id colim)).
    + apply colimit_uniqueness; intros i.
      now rewrite cat_comp_assoc, !colimit_universality.
    + now intros i; rewrite cat_comp_id_cod.
  - rewrite (colimit_uniqueness (u:=Id colim')).
    + apply colimit_uniqueness; intros i.
      now rewrite cat_comp_assoc, !colimit_universality.
    + now intros i; rewrite cat_comp_id_cod.
Qed.

(** *** 3.2.3 Initiality of Colimit **)
Class IsCoconeMap
      (J C: Category)(D: J --> C)
      (c d: Cocone D)
      (map: C c d) :=
  {
    cocone_map_commute:
      forall i: J,
        map \o c i == d i
  }.

Structure CoconeMap (J C: Category)(D: J --> C)(c d: Cocone D) :=
  {
    cocone_map_map:> C c d;
    cocone_map_prf:> IsCoconeMap cocone_map_map
  }.
Existing Instance cocone_map_prf.

Notation "[ 'CoconeMap' 'by' f ]" :=
  (@Build_CoconeMap _ _ _ _ _ f _).

Program Definition CoconeMap_compose (J C: Category)(D: J --> C)(c d e: Cocone D)(f: CoconeMap c d)(g: CoconeMap d e)
  : CoconeMap c e :=
  [CoconeMap by g \o f].
Next Obligation.
  now rewrite cat_comp_assoc, !cocone_map_commute.
Qed.

Program Definition CoconeMap_id (J C: Category)(D: J --> C)(c: Cocone D): CoconeMap c c :=
  [CoconeMap by Id c].
Next Obligation.
  now rewrite cat_comp_id_cod.
Qed.

Program Definition CoconeMap_setoid (J C: Category)(D: J --> C)(c d: Cocone D): Setoid :=
  [Setoid by `(f == g) on CoconeMap c d].
Next Obligation.
  now intros f g h Heqfg Heqgh; rewrite Heqfg, Heqgh.
Qed.

Program Definition Cocones (J C: Category)(D: J --> C): Category :=
  [Category by @CoconeMap_setoid J C D
   with (@CoconeMap_compose J C D),
        (@CoconeMap_id J C D)].
Next Obligation.
  rename X into c, Y into d, Z into e.
  intros f f' Heqf g g' Heqg; simpl in *.
  now rewrite Heqf, Heqg.

  now rewrite cat_comp_assoc.

  now rewrite cat_comp_id_dom.

  now rewrite cat_comp_id_cod.
Qed.

Program Definition colimit_by_initial_of_cocones (J C: Category)(D: J --> C)(i: Initial (Cocones D)): Colimit D :=
  [Colimit (initial_obj i) by initial_univ i].
Next Obligation.
  - now apply cocone_map_commute.
  - apply Build_IsCoconeMap in H.
    now apply (initial_uniqueness (IsInitial:=i)(X:=c)[CoconeMap by u]).
Qed.

(** * 4. Adjunction **)
(** ** 4.1 Definition **)
(* 随伴 *)
Class IsAdjunction
      (C D: Category)(F: C --> D)(G: D --> C)
      (lr: forall {c: C}{d: D}, Map (D (F c) d) (C c (G d)))
      (rl: forall {c: C}{d: D}, Map (C c (G d)) (D (F c) d)) :=
  {
    adj_iso_lr_rl:
      forall (c: C)(d: D)(f: D (F c) d),
        rl (lr f) == f;

    adj_iso_rl_lr:
      forall (c: C)(d: D)(g: C c (G d)),
        lr (rl g) == g;

    adj_lr_naturality:
      forall (c c': C)(d d': D)(f : C c' c)(g: D d d')(h: D (F c) d),
        lr (g \o h \o fmap F f) == fmap G g \o lr h \o f;

    adj_rl_naturality:
      forall (c c': C)(d d': D)(f : C c' c)(g: D d d')(h: C c (G d)),
        rl (fmap G g \o h \o f) == g \o rl h \o fmap F f
  }.

Structure Adjunction (C D: Category)(F: C --> D)(G: D --> C) :=
  {
    adj_lr: forall {c: C}{d: D}, Map (D (F c) d) (C c (G d));
    adj_rl: forall {c: C}{d: D}, Map (C c (G d)) (D (F c) d);

    prf:> IsAdjunction (@adj_lr) (@adj_rl)
  }.
Existing Instance prf.

Notation "F -| G ; C <--> D" := (Adjunction (C:=C) (D:=D) F G) (at level 40, no associativity).
Notation "F -| G" := (F -| G ; _ <--> _) (at level 40, no associativity).
Notation "[ 'Adj' 'of' F , G 'by' lr , rl ]" :=
  (@Build_Adjunction _ _ F G lr rl _).
Notation "[ 'Adj' 'by' lr , rl ]" := [Adj of _, _ by lr, rl].
Notation "[ F -| G 'by' lr , rl ]" := [Adj of F,G by lr,rl].

(** unit of adjunction **)
Program Definition adj_unit
        (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G)
  : (Id C) ==> (G \o F) :=
  [ c :=> adj_lr adj (Id (F c))].
Next Obligation.
  rewrite <- cat_comp_id_cod.
  rewrite <- (fmap_id (F Y)).
  rewrite <- adj_lr_naturality.
  rewrite !cat_comp_id_cod.
  symmetry.
  rewrite <- cat_comp_id_dom, cat_comp_assoc.
  rewrite <- adj_lr_naturality.
  now rewrite cat_comp_id_cod, fmap_id, cat_comp_id_dom.
Qed.

(** counit of adjunction *)
Program Definition adj_counit
        (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G):
  (F \o G) ==> (Id D)  :=
  [d :=> adj_rl adj (Id (G d))].
Next Obligation.
  intros; simpl.
  rewrite <- cat_comp_id_cod.
  rewrite <- adj_rl_naturality.
  rewrite fmap_id, cat_comp_id_cod.
  symmetry.
  rewrite <- cat_comp_id_dom, <- fmap_id, cat_comp_assoc.
  rewrite <- adj_rl_naturality.
  now rewrite !cat_comp_id_dom, cat_comp_id_cod.
Qed.

(* Adjunction by unit and counit *)
Program Definition Natrans_id_dom (C D: Category)(F: C --> D): (F \o Id C) ==> F :=
  [X :=> fmap F (Id X)].
Next Obligation.
  now rewrite !fmap_id, cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation "[ * \o '1' ==> * ]" := (Natrans_id_dom _).

Program Definition Natrans_id_dom_inv (C D: Category)(F: C --> D): F ==> (F \o Id C) :=
  [X :=> fmap F (Id X)].
Next Obligation.
  now rewrite !fmap_id, cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation "[ * ==> * \o '1' ]" := (Natrans_id_dom_inv _).

Program Definition Natrans_id_cod (C D: Category)(F: C --> D): (Id D \o F) ==> F :=
  [X :=> Id (F X)].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation "[ '1' \o * ==> * ]" := (Natrans_id_cod _).

Program Definition Natrans_id_cod_inv (C D: Category)(F: C --> D): F ==> (Id D \o F) :=
  [X :=> Id (F X)].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation "[ * ==> '1' \o * ]" := (Natrans_id_cod_inv _).

Program Definition Natrans_assoc (B C D E: Category)(F: B --> C)(G: C --> D)(H: D --> E): (H \o (G \o F)) ==> ((H \o G) \o F) :=
  [ X in B :=> Id (H (G (F X)))].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation Nassoc := (Natrans_assoc _ _ _).
  
Program Definition Natrans_assoc_inv (B C D E: Category)(F: B --> C)(G: C --> D)(H: D --> E): ((H \o G) \o F) ==> (H \o (G \o F)) :=
  [ X in B :=> Id (H (G (F X)))].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation Nassoc_inv := (Natrans_assoc_inv _ _ _).


Definition adj_triangle 
           (C D: Category)
           (F: C --> D)(G: D --> C)
           (au: (Id C) ==> (G \o F))
           (ac: (F \o G) ==> (Id D)) :=
  ([1 \o * ==> *]
     \o (ac o> F)
     \o Nassoc
     \o (F <o au)
     \o [* ==> * \o 1]
   == Id F
    in Natrans_setoid _ _)      (* acF \o Fau == Id_F *)
  /\
  ([* \o 1 ==> *]
     \o (G <o ac)
     \o Nassoc_inv
     \o (au o> G)
     \o [* ==> 1 \o *]
   == Id G
    in Natrans_setoid _ _).     (* Gac \o auG == Id_G *)

Lemma adj_satisfies_triangle:
  forall (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G),
    adj_triangle (adj_unit adj) (adj_counit adj).
Proof.
  intros; split; simpl; [intro c | intro d];
    rewrite fmap_id, ?cat_comp_id_dom, ?cat_comp_id_cod.
  - rewrite <- cat_comp_id_cod, <- adj_rl_naturality.
    rewrite fmap_id, !cat_comp_id_cod.
    now rewrite adj_iso_lr_rl.
  - rewrite <- cat_comp_id_dom, cat_comp_assoc, <- adj_lr_naturality.
    rewrite fmap_id, !cat_comp_id_dom.
    now rewrite adj_iso_rl_lr.
Qed.

Program Definition Adjunction_by_unit_and_counit
        (C D: Category)
        (F: C --> D)(G: D --> C)
        (au: (Id C) ==> (G \o F))
        (ac: (F \o G) ==> (Id D))
        (Hadj: adj_triangle au ac)
  : F -| G :=
  [Adj by (fun c d => [g in D (F c) d :-> fmap G g \o au c]),
          (fun c d => [f in C c (G d) :-> ac d \o fmap F f])].
Next Obligation.
  now intros g g' Heq; rewrite Heq.
Qed.
Next Obligation.
  now intros f f' Heq; rewrite Heq.
Qed.
Next Obligation.
  - rewrite fmap_comp, <- cat_comp_assoc.
    rewrite (natrans_naturality (IsNatrans:=ac) f); simpl.
    rewrite cat_comp_assoc.
    destruct Hadj as [HF HG].
    generalize (HF c); simpl.
    rewrite fmap_id, !cat_comp_id_cod, !cat_comp_id_dom.
    now intros H; rewrite H, cat_comp_id_dom.
  - rewrite fmap_comp, cat_comp_assoc.
    rewrite <- (natrans_naturality (IsNatrans:=au) g); simpl.
    rewrite <- cat_comp_assoc.
    destruct Hadj as [HF HG].
    generalize (HG d); simpl.
    rewrite fmap_id, !cat_comp_id_cod, !cat_comp_id_dom.
    now intros H; rewrite H, cat_comp_id_cod.
  - rewrite !fmap_comp, !cat_comp_assoc.
    now rewrite (natrans_naturality (IsNatrans:=au) f).
  - rewrite !fmap_comp, <- !cat_comp_assoc.
    now rewrite (natrans_naturality (IsNatrans:=ac) g).
Qed.

(** ** 4.2 Examples **)
(** *** 4.2.1 -*Y -| (-)^Y **)
Program Definition Product_2_functor (C: Category)
        (prod: forall X Y: C, Product C X Y)
        (Y: C)
  : C --> C :=
  [Functor by (fun (W X: C)(f: C W X) => [f \* Id _ with prod ])
   with `(prod X Y) ].
Next Obligation.
  - rename X into W, Y0 into X.
    intros f f' Heq.
    now rewrite Heq.
  - rename X into V, Y0 into W, Z into X.
    now rewrite <- product_map_compose, cat_comp_id_dom.
  - now apply product_map_id.
Qed.

Program Definition Exponential_functor
        (C: Category)(prod: forall (X Y: C), Product C X Y)
        (exp: forall (Y Z: C), Exponential prod Y Z)
        (X: C)
  : C --> C :=
  [Functor by (fun (Y Z: C)(g: C Y Z) => [curry (g \o exp_eval (exp X Y)) to (exp X Z)]) with `(exp X Y)].
Next Obligation.
  - rename X0 into Y, Y into Z.
    now intros g g' Heq; rewrite Heq.
  - rename X0 into Y, Y into Z, Z into W.
    symmetry.
    apply exp_uniqueness.
    rewrite <- (cat_comp_id_dom (Id X)).
    rewrite product_map_compose.
    rewrite <- cat_comp_assoc.
    rewrite <- (exp_universality (IsExponential:=exp X W)).
    rewrite !cat_comp_assoc.
    now rewrite <- (exp_universality (IsExponential:=exp X Z)).
  - rename X0 into Y.
    symmetry.
    apply exp_uniqueness.
    now rewrite product_map_id, cat_comp_id_cod, cat_comp_id_dom.
Qed.

Program Definition prod_exp_adjunction
        (C: Category)
        (prod: forall (X Y: C), Product C X Y)
        (exp: forall (Y Z: C), Exponential prod Y Z)
        (Y: C)
  : Product_2_functor prod Y -| Exponential_functor exp Y :=
  [Adj by (fun X Z => [f in C (prod X Y) Z :-> [curry f to exp Y Z]]),
          (fun X Z => [f in C X (exp Y Z) :-> exp_eval (exp Y Z) \o [f \* Id Y with prod]])].
Next Obligation.
  now intros f f' Heq; rewrite Heq.
Qed.
Next Obligation.
  now intros f f' Heq; rewrite Heq.
Qed.
Next Obligation.
  - rename c into X, d into Z.
    now rewrite <- (exp_universality (IsExponential:=exp Y Z)).
  - rename c into X, d into Z.
    symmetry.
    now apply exp_uniqueness.
  - rename c' into W, c into X, d into Z, d' into Z'.
    symmetry.
    apply exp_uniqueness.
    rewrite <- (cat_comp_id_dom (Id Y)) at 2.
    rewrite product_map_compose.
    rewrite <- (cat_comp_assoc _ _ (exp_eval _)), <- exp_universality.
    rewrite !cat_comp_assoc.
    rewrite <- (cat_comp_id_dom (Id Y)) at 2.
    rewrite product_map_compose.
    now rewrite <- (cat_comp_assoc _ _ (exp_eval _)), <- exp_universality.
  - rename c' into W, c into X, d into Z, d' into Z'.
    rewrite !cat_comp_assoc.
    rewrite <- product_map_compose, cat_comp_id_dom.
    rewrite <- (cat_comp_id_dom (Id Y)) at 1.
    rewrite product_map_compose.
    now rewrite <- cat_comp_assoc, <- exp_universality, cat_comp_assoc.
Qed.

(** *** 4.2.2 Colimit -| Diagonal -| Limit **)
Program Definition Diagonal_functor (J C: Category)
  : C --> (C^J) :=
  [Functor by f :-> [X in J :=> f]
   with X :-> [ * in J |-> X in C ]].
Next Obligation.
  now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition Colimit_functor (J C: Category)(colim: forall (D: J --> C), Colimit D)
  : (C^J) --> C :=
  [Functor by (fun D D' S => colimit_univ (colim D) [Cocone by i :-> (colim D') i \o S i] )
   with `(colim D)].
Next Obligation.
  rewrite cat_comp_assoc, natrans_naturality.
  rewrite <- cat_comp_assoc.
  now rewrite (cocone_commute (IsCocone:=colim D')).
Qed.
Next Obligation.
  - rename X into D, Y into D'.
    intros S T Heq; simpl.
    apply (colimit_uniqueness (IsColimit:=colim D)(c:=[ Cocone by i :-> (colim D') i \o T i])(u:=colimit_univ (colim D) [ Cocone by i :-> (colim D') i \o S i])); simpl.
    intros j; simpl.
    rewrite <- (Heq j).
    now rewrite (colimit_universality (IsColimit:=colim D)[Cocone by i :-> colim D' i \o S i]).

  - rename X into D, Y into D', Z into D''.
    rename f into S, g into T.
    symmetry.
    apply (colimit_uniqueness (IsColimit:=colim D)(c:=[ Cocone by i :-> (colim D'') i \o T i \o S i])).
    simpl; intros i.
    rewrite cat_comp_assoc.
    rewrite (colimit_universality (IsColimit:=colim D)[ Cocone by i :-> (colim D') i \o S i]); simpl.
    rewrite <- cat_comp_assoc.
    rewrite (colimit_universality (IsColimit:=colim D')[ Cocone by i :-> (colim D'') i \o T i]); simpl.
    now rewrite cat_comp_assoc.
  - symmetry.
    rename X into D.
    apply (colimit_uniqueness (IsColimit:=colim D)(c:=[ Cocone by i :-> (colim D) i \o Id (D i)])); simpl.
    intros i.
    now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition colimit_diag_adjunction
        (J C: Category)
        (colim: forall (D: J --> C), Colimit D)
  : Colimit_functor colim -| Diagonal_functor J C :=
  [Adj by (fun D c => [f :-> [i in J :=> f \o colim D i]]),
          (fun D c => [g :-> colimit_univ (colim D) [Cocone by g to c]])].
Next Obligation.
  rename X into i, Y into j, f0 into u.
  rewrite cat_comp_assoc, (cocone_commute (IsCocone:=colim D)).
  now rewrite cat_comp_id_cod.
Qed.
Next Obligation.
  intros f g Heq i; simpl.
  now rewrite Heq.
Qed.
Next Obligation.
  rewrite (natrans_naturality (IsNatrans:=g)); simpl.
  now rewrite cat_comp_id_cod.
Qed.
Next Obligation.
  intros S T Heq; simpl.
  apply (colimit_uniqueness (IsColimit:=colim D)(c:=[Cocone by T to c])(u:=colimit_univ (colim D) [Cocone by S to c])); simpl.
  intros i.
  rewrite <- (Heq i).
  now rewrite (colimit_universality (IsColimit:=colim D) [Cocone by S to c]).
Qed.
Next Obligation.
  - symmetry.
    now apply (colimit_uniqueness (IsColimit:=colim c)(c:=[Cocone by i :-> f \o (colim c) i])); simpl.
  - now rewrite (colimit_universality (IsColimit:=colim c) [Cocone by g to d]).
  - rewrite !cat_comp_assoc.
    now rewrite (colimit_universality (IsColimit:=colim c')[Cocone by i :-> (colim c) i \o f i]).
  - rename c into D, c' into D', d into c, d' into c', f into S, g into f, h into T.
    symmetry.
    apply (colimit_uniqueness (IsColimit:=colim D')(c:=[ Cocone by X :-> f \o T X \o S X])); simpl.
    intros i.
    rewrite cat_comp_assoc.
    apply cat_comp_proper; try now idtac.
    rewrite cat_comp_assoc.
    rewrite (colimit_universality (IsColimit:=colim D')[ Cocone by i :-> (colim D) i \o S i]); simpl.
    rewrite <- cat_comp_assoc.
    now rewrite (colimit_universality (IsColimit:=colim D) [ Cocone by T to c]); simpl.
Qed.


Program Definition Limit_functor (J C: Category)(lim: forall (D: J --> C), Limit D)
  : (C^J) --> C :=
  [Functor by (fun D D' S => limit_univ (lim D') [Cone by i :-> S i \o (lim D) i] )
   with `(lim D)].
Next Obligation.
  rewrite <- cat_comp_assoc, <- natrans_naturality.
  rewrite cat_comp_assoc.
  now rewrite (cone_commute (IsCone:=lim D)).
Qed.
Next Obligation.
  - rename X into D, Y into D'.
    intros S T Heq; simpl.
    apply (limit_uniqueness (IsLimit:=lim D')(c:=[ Cone by i :-> T i \o (lim D) i])(u:=limit_univ (lim D') [ Cone by i :-> S i \o (lim D) i])); simpl.
    intros j; simpl.
    rewrite <- (Heq j).
    now rewrite (limit_universality (IsLimit:=lim D')[Cone by i :-> S i \o lim D i]).
  - rename X into D, Y into D', Z into D''.
    rename f into S, g into T.
    symmetry.
    apply (limit_uniqueness (IsLimit:=lim D'')(c:=[ Cone by i :-> (T i \o S i) \o (lim D i)])).
    simpl; intros i.
    rewrite <- cat_comp_assoc.
    rewrite (limit_universality (IsLimit:=lim D'')[ Cone by i :-> T i \o (lim D') i]); simpl.
    rewrite cat_comp_assoc.
    rewrite (limit_universality (IsLimit:=lim D')[ Cone by i :-> S i \o (lim D) i]); simpl.
    now rewrite cat_comp_assoc.
  - symmetry.
    rename X into D.
    apply (limit_uniqueness (IsLimit:=lim D)(c:=[ Cone by i :-> Id (D i) \o (lim D) i])); simpl.
    intros i.
    now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition diag_limit_adjunction
        (J C: Category)
        (lim: forall (D: J --> C), Limit D)
  : Diagonal_functor J C -| Limit_functor lim :=
  [Adj by (fun c D => [g :-> limit_univ (lim D) [Cone by g from c]]),
          (fun c D => [f :-> [i in J :=> lim D i \o f]])].
Next Obligation.
  rewrite <- (natrans_naturality (IsNatrans:=g)); simpl.
  now rewrite cat_comp_id_dom.
Qed.
Next Obligation.
  intros S T Heq; simpl.
  apply (limit_uniqueness (IsLimit:=lim D)(c:=[Cone by T from c])(u:=limit_univ (lim D) [Cone by S from c])); simpl.
  intros i.
  rewrite <- (Heq i).
  now rewrite (limit_universality (IsLimit:=lim D) [Cone by S from c]).
Qed.
Next Obligation.
  rename X into i, Y into j, f0 into u.
  rewrite <- cat_comp_assoc, (cone_commute (IsCone:=lim D)).
  now rewrite cat_comp_id_dom.
Qed.
Next Obligation.
  intros f g Heq i; simpl.
  now rewrite Heq.
Qed.
Next Obligation.
  - now rewrite (limit_universality (IsLimit:=lim d)[Cone by f from c]).
  - symmetry.
    now apply (limit_uniqueness (IsLimit:=lim d)(c:=[Cone by i :-> (lim d) i \o g])); simpl.
  - rename d into D, d' into D', g into S, h into T.
    symmetry.
    apply (limit_uniqueness (IsLimit:=lim D')(c:=[ Cone by X :-> S X \o T X \o f])); simpl.
    intros i.
    rewrite <- !cat_comp_assoc.
    apply cat_comp_proper; try now idtac.
    rewrite (limit_universality (IsLimit:=lim D')[ Cone by i :-> S i \o (lim D) i]); simpl.
    rewrite cat_comp_assoc.
    now rewrite (limit_universality (IsLimit:=lim D) [ Cone by T from c]); simpl.
  - rewrite <- !cat_comp_assoc.
    now rewrite (limit_universality (IsLimit:=lim d')[Cone by i :-> g i \o (lim d) i]).
Qed.

(** ** 4.3 naturality of adjunction **)
Program Definition prod_functor (C D C' D': Category)(F: C --> D)(F': C' --> D'): (product_category C C') --> (product_category D D') :=
  [ F \* F' with product_of_Cat].
Notation "[ F 'xF' G ]" := (prod_functor F G).

Program Definition hom_functor (C: Category): (product_category C^op C) --> Setoids :=
  [Functor by fh :-> [ g :-> fh.2 \o{C} g \o{C} fh.1]
   with XY :-> C XY.1 XY.2].
Next Obligation.
  now intros g g' Heq; rewrite Heq.
Qed.
Next Obligation.
  intros f f' [Heqf1 Heqf2] g; simpl.
  - now rewrite Heqf1, Heqf2.
  - now rewrite !cat_comp_assoc.
  - now rewrite cat_comp_id_dom, cat_comp_id_cod.
Qed.
Notation "'HomF' C" := (hom_functor C) (at level 40, no associativity).

Program Definition op_functor (C D: Category)(F: C --> D)
  : C^op --> D^op :=
  [Functor by f :-> fmap F f ].
Next Obligation.
  - now apply fmap_subst.
  - now apply fmap_comp.
  - now apply fmap_id.
Qed.
Notation "F ^opF" := (op_functor F) (at level 0, format "F ^opF").

(** 
#$Hom_D(-,-)\circ F\times Id_D$#
 **)
Definition adj_lrF (C D: Category)(F: C --> D): (product_category C^op D) --> Setoids :=
  hom_functor D \o [F^opF xF (Id D)].

(** 
#$Hom_C(-,-)\circ Id_{C^op}\times G$#
 **)
Definition adj_rlF (C D: Category)(G: D --> C): (product_category C^op D) --> Setoids :=
  hom_functor C \o [(Id C^op) xF G].


Program Definition adj_lr_Natrans
        (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G)
  : (adj_lrF F) ==> (adj_rlF G):=
  [ cd :=> let (c,d) := cd in adj_lr adj (c:=c)(d:=d)].
Next Obligation.
  now rewrite adj_lr_naturality.
Qed.

Program Definition adj_rl_Natrans
        (C D: Category)(F: C --> D)(G: D --> C)(adj: F -| G)
  : (adj_rlF G) ==> (adj_lrF F):=
  [ cd :=> let (c,d) := cd in adj_rl adj (c:=c)(d:=d)].
Next Obligation.
  now rewrite adj_rl_naturality.
Qed.


(** * 5. Kan extension **)
(** ** 5.1 Left Kan extension **)
(** *** 5.1.1 Definition **)
Class IsLan
      (C D E: Category)
      (F: C --> E)(K: C --> D)
      (lanF: D --> E)
      (lanN: F ==> (lanF \o K))
      (lanU: forall {S: D --> E},
          F ==> (S \o K) -> lanF ==> S) :=
  {
    lan_universality:
      forall (S: D --> E)(e: F ==> (S \o K)),
        (lanU e o> K) \o{Fun _ _} lanN == e;
    lan_uniqueness:
      forall (S: D --> E)(e: F ==> (S \o K))(u: lanF ==> S),
        (u o> K) \o{Fun _ _} lanN == e -> u == lanU e
  }.

Structure Lan (C D E: Category)(F: C --> E)(K: C --> D): Type :=
  {
    lanF: D --> E;
    lanN: F ==> (lanF \o K);
    lanU: forall {S: D --> E},
        F ==> (S \o K) -> lanF ==> S;

    lan_prf:> IsLan lanN (@lanU)
  }.
Notation "[ 'Lan' 'of' F 'along' K 'by' lanU 'with' lanF , lanN ]" :=
  (@Build_Lan _ _ _ F K lanF lanN lanU _).
Notation "[ 'Lan' 'by' lanU 'with' lanF , lanN ]" :=
  [Lan of _ along _ by lanU with lanF, lanN].

(** *** 5.1.2 Lan and Colimit **)
Program Definition colimit_from_lan
        (C D: Category)
        (F: C --> D)
        (lan: Lan F (ToOne C))
  : Colimit F :=
  [Colimit [Cocone by (lanN lan) to (lanF lan tt)]
    by `(lanU lan (S:=constant_functor One D (c: Cocone F)) [i :=> c i] tt) ].
Next Obligation.
  rewrite (natrans_naturality (IsNatrans:=lanN lan)); simpl.
  now rewrite (fmap_id (F:=lanF lan) tt), cat_comp_id_cod.
Qed.
Next Obligation.
  now rewrite cocone_commute, cat_comp_id_cod.
Qed.
Next Obligation.
  generalize (lan_universality (IsLan:=lan)(S:=[* in One |-> c in D])); simpl.
  intros H; apply H.

  generalize (lan_uniqueness (IsLan:=lan)(S:=[* in One |-> c in D])); simpl.
  intros Huniq; eapply (Huniq _ [x :=> match x with
                                       | tt => u
                                       end
                                   from (lanF lan) to [* in One |-> c in D]]); simpl.
  now apply H.
  Grab Existential Variables.
  split.
  intros [] [] []; simpl.
  now rewrite (fmap_id (F:=lanF lan)), cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition lan_from_colimit
        (C D: Category)
        (F: C --> D)
        (colim: Colimit F)
  : Lan F (ToOne C) :=
  [Lan by (fun S (e: F ==> (S \o ToOne C)) =>
           [ x :=> match x with
                   | tt => colimit_univ colim [Cocone by e to S tt]
                   end])
   with [Functor by f :-> Id colim], [ c in C :=> colim c]].
Next Obligation.
  now rewrite cat_comp_id_dom.
Qed.
Next Obligation.
  now rewrite cocone_commute, cat_comp_id_cod.
Qed.
Next Obligation.
  rewrite (natrans_naturality (IsNatrans:=e)); simpl.
  now rewrite (fmap_id (F:=S) tt), cat_comp_id_cod.
Qed.
Next Obligation.
  destruct X, Y, f.
  now rewrite cat_comp_id_dom, (fmap_id (F:=S) tt), cat_comp_id_cod.
Qed.
Next Obligation.
  generalize (colimit_universality (IsColimit:=colim)); simpl.
  intros H; apply (H [Cocone by e to S tt] X).
  destruct X.
  generalize (colimit_uniqueness (IsColimit:=colim)); intros Huniq.
  now apply (Huniq [Cocone by e to S tt]), H.
Qed.

(** equivalence **)
Program Definition Cocone_setoid {J C: Category}(D: J --> C): Setoid :=
  [Setoid by `(forall i, c i =H d i) on Cocone D].
Next Obligation.
  - intros c d Heq i.
    now apply hom_eq_sym, Heq.
  - intros c d e Heqcd Heqde i.
    now eapply hom_eq_trans; [apply Heqcd | apply Heqde].
Qed.

Program Definition Colimit_setoid {J C: Category}(D: J --> C): Setoid :=
  [Setoid by `(forall c, colimit_univ colim c =H colimit_univ colim' c) on Colimit D].
Next Obligation.
  - intros c d Heq i.
    now apply hom_eq_sym, Heq.
  - intros c d e Heqcd Heqde i.
    now eapply hom_eq_trans; [apply Heqcd | apply Heqde].
Qed.

Program Definition Lan_setoid (C D E: Category)(F: C --> E)(K: C --> D) :=
  [Setoid by (fun (lan lan': Lan F K) => forall x, lanN lan x =H lanN lan' x ) on Lan F K].
Next Obligation.
  - intros lan lan' Heq c; apply hom_eq_sym, Heq.
  - intros lan lan' lan'' Heq Heq' c.
    now eapply hom_eq_trans; [apply Heq | apply Heq'].
Qed.

Lemma lan_from_colimit_from_lan:
  forall (C D: Category)
         (F: C --> D)
         (lan: Lan F (ToOne C)),
    lan == lan_from_colimit (colimit_from_lan lan)
    in Lan_setoid F (ToOne C).
Proof.
  now simpl.
Qed.

Lemma colimit_from_lan_from_colimit:
  forall (C D: Category)
         (F: C --> D)
         (colim: Colimit F),
    colim === colimit_from_lan (lan_from_colimit colim).
Proof.
  intros; apply colimit_isomorphic.
Qed.


(** ** 5.2 Right Kan extension **)
(** *** 5.2.1 Definition **)
Class IsRan
      (C D E: Category)
      (F: C --> E)(K: C --> D)
      (ranF: D --> E)
      (ranN: (ranF \o K) ==> F)
      (ranU: forall {S: D --> E},
          (S \o K) ==> F -> S ==> ranF) :=
  {
    ran_universality:
      forall (S: D --> E)(e: (S \o K) ==> F),
        ranN \o{Fun _ _} (ranU e o> K) == e;
    ran_uniqueness:
      forall (S: D --> E)(e: (S \o K) ==> F)(u: S ==> ranF),
        ranN \o{Fun _ _} (u o> K) == e -> u == ranU e
  }.

Structure Ran (C D E: Category)(F: C --> E)(K: C --> D): Type :=
  {
    ranF: D --> E;
    ranN: (ranF \o K) ==> F;
    ranU: forall {S: D --> E},
        (S \o K) ==> F -> S ==> ranF;

    ran_prf:> IsRan ranN (@ranU)
  }.
Notation "[ 'Ran' 'of' F 'along' K 'by' ranU 'with' ranF , ranN ]" :=
  (@Build_Ran _ _ _ F K ranF ranN ranU _).
Notation "[ 'Ran' 'of' F 'along' K 'by' ranU ]" :=
  [Ran of F along K by ranU with _, _].
Notation "[ 'Ran' 'by' ranU 'with' ranF , ranN ]" :=
  [Ran of _ along _ by ranU with ranF, ranN].
Notation "[ 'Ran' 'by' ranU ]" := [Ran by ranU with _,_].


(** *** 5.2.2 Ran and Limit **)
Program Definition limit_from_ran
        (C D: Category)
        (F: C --> D)
        (ran: Ran F (ToOne C))
  : Limit F :=
  [Limit [Cone by (ranN ran) from (ranF ran tt)]
    by `(ranU ran (S:=[* in One |-> (c: Cone F) in D]) [i :=> c i] tt) ].
Next Obligation.
  rewrite <- (natrans_naturality (IsNatrans:=ranN ran)); simpl.
  now rewrite (fmap_id (F:=ranF ran) tt), cat_comp_id_dom.
Qed.
Next Obligation.
  now rewrite cone_commute, cat_comp_id_dom.
Qed.
Next Obligation.
  generalize (ran_universality (IsRan:=ran)(S:=[* in One |-> c in D ])); simpl.
  intros H; apply H.

  generalize (ran_uniqueness (IsRan:=ran)(S:=[* in One |-> c in D ])); simpl.
  intros Huniq; eapply (Huniq _ [x :=> match x with
                                       | tt => u
                                       end
                                   from [* in One |-> c in D] to (ranF ran)]); simpl.
  now apply H.
  Grab Existential Variables.
  split.
  intros [] [] []; simpl.
  now rewrite (fmap_id (F:=ranF ran)), cat_comp_id_dom, cat_comp_id_cod.
Qed.

Program Definition ran_from_limit
        (C D: Category)
        (F: C --> D)
        (lim: Limit F)
  : Ran F (ToOne C) :=
  [Ran by (fun S (e: (S \o ToOne C) ==> F) =>
           [ x :=> match x with
                   | tt => limit_univ lim [Cone by e from S tt]
                   end])
   with [Functor by f :-> Id lim], [ c in C :=> lim c]].
Next Obligation.
  now rewrite cat_comp_id_dom.
Qed.
Next Obligation.
  now rewrite cone_commute, cat_comp_id_dom.
Qed.
Next Obligation.
  rewrite <- (natrans_naturality (IsNatrans:=e)); simpl.
  now rewrite (fmap_id (F:=S) tt), cat_comp_id_dom.
Qed.
Next Obligation.
  destruct X, Y, f.
  now rewrite cat_comp_id_cod, (fmap_id (F:=S) tt), cat_comp_id_dom.
Qed.
Next Obligation.
  - generalize (limit_universality (IsLimit:=lim)); simpl.
    now intros H; apply (H [Cone by e from S tt] X).
  - destruct X.
    generalize (limit_uniqueness (IsLimit:=lim)); intros Huniq.
    now apply (Huniq [Cone by e from S tt]), H.
Qed.

(** ** 5.3 Adjunction and Kan extension **)
(** *** 5.3.1 Concepts **)
Class PreserveLan
      {C D E E': Category}{F: C --> E}{K: C --> D}
      (lan: Lan F K)
      (L: E --> E')
      (new: forall (S: D --> E'),
          (L \o F) ==> (S \o K) ->
          (L \o lanF lan) ==> S) :=
  preserve_lan:
    IsLan (lanF:=L \o lanF lan) (Nassoc \o (L <o lanN lan)) (@new).

(** left adjoint preserve lan **)
Program Instance left_adjoint_preserve_lan
        (C D E E': Category)
        (F: C --> E)(K: C --> D)(lan: Lan F K)
        (L: E --> E')(R: E' --> E)(adj: L -| R)
  : PreserveLan
      (fun S e =>
         [ 1 \o * ==> * ]
           \o (adj_counit adj o> S)
           \o Nassoc
           \o (L <o (lanU lan
                           (Nassoc
                              \o (R <o e)
                              \o Nassoc_inv
                              \o (adj_unit adj o> F)
                              \o [ * ==> 1 \o * ])))).
Next Obligation.
  - simpl; intros.
    rewrite !cat_comp_id_cod, !cat_comp_assoc, <- fmap_comp; simpl.
    generalize (lan_universality
                  (IsLan:=lan)
                  (Nassoc \o (R <o e) \o Nassoc_inv \o (adj_unit adj o> F) \o [ * ==> 1 \o * ]) X); simpl.
    intro H; rewrite H; simpl.
    rewrite cat_comp_id_cod, cat_comp_id_dom.
    rewrite <- cat_comp_id_cod.
    rewrite <- adj_rl_naturality.
    rewrite fmap_id, !cat_comp_id_cod.
    rewrite <- (cat_comp_id_dom (fmap R _ \o _)), cat_comp_assoc.
    rewrite adj_rl_naturality.
    now rewrite adj_iso_lr_rl, fmap_id, !cat_comp_id_dom.
  - simpl; intros.
    symmetry.
    rewrite !cat_comp_id_cod, <- cat_comp_id_cod.
    rewrite <- adj_rl_naturality.
    rewrite fmap_id, !cat_comp_id_cod.
    generalize (lan_uniqueness
                  (IsLan:=lan)
                  (e:=Nassoc \o (R <o e) \o Nassoc_inv \o (adj_unit adj o> F) \o Natrans_id_cod_inv F)
                  (u:=(R <o u) \o Nassoc_inv \o{Fun _ _} (adj_unit adj o> lanF lan) \o{Fun _ _} [* ==> 1 \o * ]));
      simpl; intros Heq.
    rewrite <- Heq.
    + rewrite cat_comp_id_cod.
      rewrite adj_rl_naturality.
      now rewrite fmap_id, cat_comp_id_dom, adj_iso_lr_rl, cat_comp_id_dom.
    + intros c.
      rewrite !cat_comp_id_cod.
      rewrite <- adj_lr_naturality.
      rewrite cat_comp_id_cod.
      rewrite (fmap_id (F:=L)), cat_comp_id_dom.
      rewrite <- adj_lr_naturality.
      rewrite (fmap_id (F:=L)), !cat_comp_id_dom.
      rewrite <- H.
      rewrite cat_comp_id_cod.
      rewrite <- (cat_comp_id_cod (u (K c) \o _)).
      rewrite (adj_lr_naturality (IsAdjunction:=adj) _ _ (u (K c))).
      now rewrite fmap_id, cat_comp_id_cod.
Qed.

(** lan from adjunction **)
Program Definition lan_from_adjunction
        (C D: Category)
        (F: C --> D)(G: D --> C)(adj: F -| G)
  : Lan (Id C) F :=
  [Lan by (fun S e => ([ * \o 1 ==> *]
                         \o (S <o adj_counit adj)
                         \o Nassoc_inv
                         \o (e o> G)
                         \o [* ==> 1 \o *]))
   with G, adj_unit adj].
Next Obligation.
  rewrite <- !cat_comp_assoc.
  rewrite <- fmap_comp, cat_comp_id_cod, !cat_comp_id_dom.
  rewrite cat_comp_assoc.
  generalize (natrans_naturality (IsNatrans:=e) (adj_lr adj (Id F X))); simpl; intros H; rewrite H; clear H.
  rewrite <- cat_comp_assoc, <- fmap_comp.
  rewrite <- (cat_comp_id_cod (adj_rl adj _ \o _)).
  rewrite <- adj_rl_naturality.
  rewrite !fmap_id, !cat_comp_id_cod.
  now rewrite adj_iso_lr_rl, fmap_id, cat_comp_id_cod.

  rewrite fmap_id, !cat_comp_id_cod, cat_comp_id_dom.
  rewrite <- H.
  rewrite <- cat_comp_assoc.
  rewrite <- (natrans_naturality (IsNatrans:=u) ((adj_rl adj) (Id G X))).
  rewrite cat_comp_assoc.
  rewrite <- (cat_comp_id_dom (fmap G _ \o _)), cat_comp_assoc.
  rewrite <- adj_lr_naturality, fmap_id, !cat_comp_id_dom.
  now rewrite adj_iso_rl_lr, cat_comp_id_dom.
Qed.

(** ran from adjunction **)
Program Definition ran_from_adjunction
        (C D: Category)
        (F: C --> D)(G: D --> C)(adj: F -| G)
  : Ran (Id D) G :=
  [Ran by (fun S e =>
             [1 \o * ==> *]
               \o (e o> F)
               \o Nassoc
               \o (S <o adj_unit adj)
               \o  [* ==> * \o 1])
   with F, adj_counit adj].
Next Obligation.
  rewrite <- fmap_comp, !cat_comp_id_cod, !cat_comp_id_dom.
  rewrite <- cat_comp_assoc.
  generalize (natrans_naturality (IsNatrans:=e) (adj_rl adj (Id (G X)))); simpl; intros H; rewrite <- H; clear H.
  rewrite cat_comp_assoc, <- fmap_comp.
  rewrite <- (cat_comp_id_dom (_ \o adj_lr adj _)).
  rewrite cat_comp_assoc, <- adj_lr_naturality.
  rewrite !fmap_id, !cat_comp_id_dom.
  now rewrite adj_iso_rl_lr, fmap_id, cat_comp_id_dom.

  rewrite fmap_id, !cat_comp_id_cod, cat_comp_id_dom.
  rewrite <- H.
  rewrite cat_comp_assoc.
  rewrite (natrans_naturality (IsNatrans:=u) (adj_lr adj (Id (F X)))).
  rewrite <- cat_comp_assoc.
  rewrite <- (cat_comp_id_cod (_ \o fmap F _)), <- !cat_comp_assoc.
  rewrite (cat_comp_assoc (fmap F _)).
  rewrite <- adj_rl_naturality, fmap_id, !cat_comp_id_cod.
  now rewrite adj_iso_lr_rl, cat_comp_id_cod.
Qed.

(** adjunction from lan **)
Program Definition counit_from_lan
        (C D: Category)
        (F: C --> D)(G: D --> C)
        (au: (Id C) ==> (G \o F))
        (luniv: forall (S: D --> C),
            (Id C) ==> (S \o F) -> G ==> S)
        (Hlan: IsLan (lanF:=G) au luniv)
        (puniv: forall (S: D --> D),
            (F \o Id C) ==> (S \o F) ->
            (F \o G) ==> S)
        (Hp: PreserveLan (lan:=Build_Lan Hlan)(L:=F) puniv)
  : (F \o G) ==> (Id D) :=
  puniv (Id D) ([* ==> 1 \o *] \o Id F \o [* \o 1 ==> *]).

Lemma counit_from_lan_makes_triangle:
  forall (C D: Category)
         (F: C --> D)(G: D --> C)
         (au: (Id C) ==> (G \o F))
         (luniv: forall (S: D --> C),
             (Id C) ==> (S \o F) -> G ==> S)
         (Hlan: IsLan (lanF:=G) au luniv)
         (puniv: forall (S: D --> D),
             (F \o Id C) ==> (S \o F) ->
             (F \o G) ==> S)
         (Hp: PreserveLan (lan:=Build_Lan Hlan)(L:=F) puniv),
    adj_triangle au (puniv (Id D) ([* ==> 1 \o *] \o Id F \o [* \o 1 ==> *])).
Proof.
  intros; split.
  - simpl; intros c.
    rewrite !cat_comp_id_cod, fmap_id, cat_comp_id_dom.
    generalize (lan_universality (IsLan:=Hp) ([ * ==> 1 \o * ] \o Natrans_id F \o [ * \o 1 ==> * ]) c); simpl.
    rewrite cat_comp_id_cod.
    intros H; rewrite H.
    now rewrite !cat_comp_id_cod, fmap_id.
  -
    generalize (lan_uniqueness (IsLan:=Hlan)(e:=au)(u:=Id G)).
    intros H'; rewrite H'; clear H'.
    + apply lan_uniqueness.
      simpl; intros c.
      rewrite fmap_id, !cat_comp_id_cod, cat_comp_id_dom.
      rewrite cat_comp_assoc.
      rewrite (natrans_naturality (IsNatrans:=au) (au c)); simpl.
      rewrite <- cat_comp_assoc, <- fmap_comp.

      generalize (lan_universality (IsLan:=Hp) ([ * ==> 1 \o * ] \o Natrans_id F \o [ * \o 1 ==> * ]) c); simpl.
      rewrite !cat_comp_id_cod.
      intros H; rewrite H.
      now rewrite !fmap_id, !cat_comp_id_cod.
    + now simpl; intros c; rewrite cat_comp_id_cod.
Qed.

Definition adjunction_from_lan
        (C D: Category)
        (F: C --> D)(G: D --> C)
        (au: (Id C) ==> (G \o F))
        (luniv: forall (S: D --> C),
            (Id C) ==> (S \o F) -> G ==> S)
        (Hlan: IsLan (lanF:=G) au luniv)
        (puniv: forall (S: D --> D),
            (F \o Id C) ==> (S \o F) ->
            (F \o G) ==> S)
        (Hp: PreserveLan (lan:=Build_Lan Hlan)(L:=F) puniv)
  : F -| G :=
  Adjunction_by_unit_and_counit
    (counit_from_lan_makes_triangle Hp).

(** *** 5.3.2 Lan -| Inverse -| Ran **)
Program Definition Inverse_functor
        (C D: Category)(K: C --> D)
        (E: Category)
  : (E^D) --> (E^C) :=
  [Functor by S :-> [c :=> S (K c)] with F :-> F \o K].
Next Obligation.
  now rewrite <- natrans_naturality.
Qed.
Next Obligation.
  rename X into F, Y into G.
  intros S T Heq c; simpl.
  now rewrite Heq.
Qed.

Program Definition Lan_functor
        (C D: Category)(K: C --> D)
        (E: Category)
        (lan: forall (F: C --> E), Lan F K)
  : (E^C) --> (E^D) :=
  [Functor by (fun F G S => lanU (lan F) (lanN (lan G) \o S))
   with `(lanF (lan F))].
Next Obligation.
  - rename X into F, Y into G.
    intros S T Heq d.
    apply (lan_uniqueness (IsLan:=lan F)(e:=lanN (lan G) \o T)).
    rewrite (lan_universality (IsLan:=lan F)(lanN (lan G) \o S)).
    now simpl; intros c; rewrite Heq.
  - rename X into F, Y into G, Z into H, f into S, g into T, X0 into d.
    symmetry.
    apply (lan_uniqueness (IsLan:=lan F)(e:=(lanN (lan H) \o T \o S))(u:=(lanU (lan G) (lanN (lan H) \o T))\o (lanU (lan F) (lanN (lan G) \o S)))); simpl; intros c.
    rewrite cat_comp_assoc.
    rewrite (lan_universality (IsLan:=lan F)(lanN (lan G) \o S) c).
    simpl.
    rewrite <- cat_comp_assoc.
    rewrite (lan_universality (IsLan:=lan G)(lanN (lan H) \o T) c).
    simpl.
    now rewrite cat_comp_assoc.
  - rename X into F, X0 into d.
    symmetry.
    apply (lan_uniqueness (IsLan:=lan F)(e:=(lanN (lan F) \o Natrans_id F))(u:=Natrans_id _)); simpl; intros c.
    now rewrite cat_comp_id_cod, cat_comp_id_dom.
Qed.

Program Definition Ran_functor
        (C D: Category)(K: C --> D)
        (E: Category)
        (ran: forall (F: C --> E), Ran F K)
  : (E^C) --> (E^D) :=
  [Functor by (fun F G S => ranU (ran G) (S \o ranN (ran F)))
   with `(ranF (ran F))].
Next Obligation.
  - rename X into F, Y into G.
    intros S T Heq d.
    apply (ran_uniqueness (IsRan:=ran G)(e:=T \o ranN (ran F))).
    rewrite (ran_universality (IsRan:=ran G)(S \o ranN (ran F))).
    now simpl; intros c; rewrite Heq.
  - rename X into F, Y into G, Z into H, f into S, g into T, X0 into d.
    symmetry.
    apply (ran_uniqueness (IsRan:=ran H)(e:=((T \o S) \o ranN (ran F)))(u:=(ranU (ran H) (T \o ranN (ran G))) \o (ranU (ran G) (S \o ranN (ran F))))); simpl; intros c.
    rewrite <- cat_comp_assoc.
    rewrite (ran_universality (IsRan:=ran H)(T \o ranN (ran G)) c).
    simpl.
    rewrite cat_comp_assoc.
    rewrite (ran_universality (IsRan:=ran G)(S \o ranN (ran F)) c).
    simpl.
    now rewrite cat_comp_assoc.
  - rename X into F, X0 into d.
    symmetry.
    apply (ran_uniqueness (IsRan:=ran F)(e:=(Natrans_id F \o ranN (ran F)))(u:=Natrans_id _)); simpl; intros c.
    now rewrite cat_comp_id_cod, cat_comp_id_dom.
Qed.

(** Lan -| Inverse **)
Program Definition lan_inverse_adjunction
        (C D: Category)(K: C --> D)
        (E: Category)
        (lan: forall (F: C --> E), Lan F K)
  : Lan_functor lan -| Inverse_functor K E :=
  [Adj by (fun (F: C --> E)(G: D --> E) =>
             [S in lanF (lan F) ==> G :->
                        (S o> K) \o lanN (lan F)]),
          (fun (F: C --> E)(G: D --> E) =>
             [S in F ==> (G \o K) :-> lanU (lan F) S]) ].
Next Obligation.
  intros S T Heq c; simpl.
  now rewrite Heq.
Qed.
Next Obligation.
  intros S T Heq d; simpl.
  apply (lan_uniqueness (IsLan:=lan F)(e:= T)); simpl; intros c.
  now rewrite (lan_universality (IsLan:=lan F) S c), Heq.
Qed.
Next Obligation.
  - rename c into F, d into G, f into S, X into d.
    symmetry.
    now apply (lan_uniqueness (IsLan:=lan F)(e:=S o> K \o lanN (lan F))).
  - rename c into F, d into G, g into T, X into c.
    now rewrite (lan_universality (IsLan:=lan F) T c).
  - rename c into F, c' into F', d into G, d' into G', f into S, g into T, h into U, X into c.
    rewrite !cat_comp_assoc.
    now rewrite (lan_universality (IsLan:=lan F') (lanN (lan F) \o S) c); simpl.
  - rename c into F, c' into F', d into G, d' into G', f into S, g into T, h into U, X into d.
    symmetry.
    generalize (lan_uniqueness (IsLan:=lan F')); simpl; intros Huniq.
    eapply (Huniq _ ([c :=> T (K c) from (G \o K) to (G' \o K)] \o U \o S)
                  (T \o (lanU (lan F) U) \o (lanU (lan F') (lanN (lan F) \o S)))); simpl; intros c.
    rewrite !cat_comp_assoc.
    rewrite (lan_universality (IsLan:=lan F')(lanN (lan F) \o S) c); simpl.
    rewrite <- (cat_comp_assoc (S c)).
    now rewrite (lan_universality (IsLan:=lan F) U c).
Qed.

(** Inverse -| Ran **)
Program Definition ran_inverse_adjunction
        (C D: Category)(K: C --> D)
        (E: Category)
        (ran: forall (F: C --> E), Ran F K)
  : Inverse_functor K E -| Ran_functor ran :=
  [Adj by (fun (G: D --> E)(F: C --> E) =>
             [S in (G \o K) ==> F :-> ranU (ran F) S]),
          (fun (G: D --> E)(F: C --> E) =>
             [S in G ==> ranF (ran F) :-> ranN (ran F) \o (S o> K)])].
Next Obligation.
  intros S T Heq d; simpl.
  apply (ran_uniqueness (IsRan:=ran F)(e:= T)); simpl; intros c.
  now rewrite (ran_universality (IsRan:=ran F) S c), Heq.
Qed.
Next Obligation.
  intros S T Heq c; simpl.
  now rewrite Heq.
Qed.
Next Obligation.
  - rename c into G, d into F, f into S, X into c.
    now rewrite (ran_universality (IsRan:=ran F) S c).
  - rename c into G, d into F, g into S, X into d.
    symmetry.
    now apply (ran_uniqueness (IsRan:=ran F)(e:=ranN (ran F) \o (S o> K))).
  - rename d into F, d' into F', c into G, c' into G', f into T, g into S, h into U, X into d.
    symmetry.
    generalize (ran_uniqueness (IsRan:=ran F')); simpl; intros Huniq.
    eapply (Huniq _ (S \o U \o [c :=> T (K c) from (_ \o _) to (_ \o _)])
                  ((ranU (ran F') (S \o ranN (ran F))) \o (ranU (ran F) U) \o T)); simpl; intros c.
    rewrite <- !cat_comp_assoc.
    rewrite (ran_universality (IsRan:=ran F')(S \o ranN (ran F)) c); simpl.
    rewrite (cat_comp_assoc _ _ (S c)).
    now rewrite (ran_universality (IsRan:=ran F) U c).
  - rename d into F, d' into F', c into G, c' into G', f into T, g into S, h into U, X into d.
    rewrite <- !cat_comp_assoc.
    now rewrite (ran_universality (IsRan:=ran F') (S \o ranN (ran F)) d); simpl.
Qed.