From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cone.
Require Import Diagrams.ConstantDiagram.

Local Open Scope path_scope.
Generalizable All Variables.

(** This file contains the definition of limits, and functoriality results on limits. *)

(** * Limits *)

(** A Limit is the extremity of a cone. *)

Class IsLimit `(D : Diagram G) (Q : Type) := {
  islimit_cone :: Cone Q D;
  islimit_unicone : UniversalCone islimit_cone;
}.
Coercion islimit_cone : IsLimit >-> Cone.

Arguments Build_IsLimit {G D Q} C H : rename.
Arguments islimit_cone {G D Q} C : rename.
Arguments islimit_unicone {G D Q} H : rename.

(** [cone_precompose_inv] is defined for convenience: it is only the inverse of [cone_precompose]. It allows to recover the map [h] from a cone [C']. *)

Definition cone_precompose_inv `{D: Diagram G} {Q X}
  (H : IsLimit D Q) (C' : Cone X D) : X -> Q
  := @equiv_inv _ _ _ (islimit_unicone H X) C'.


(** * Existence of limits *)

Record Limit `(D : Diagram G) := {
  lim : forall i, D i;
  limp : forall i j (g : G i j), D _f g (lim i) = lim j;
}.

Arguments lim {_ _}.
Arguments limp {_ _}.

Definition cone_limit `(D : Diagram G) : Cone (Limit D) D.
G: Graph
D: Diagram G
Cone (Limit D) D
Proof.
G: Graph
D: Diagram G
Cone (Limit D) D
  srapply Build_Cone.
G: Graph
D: Diagram G
forall i : G, Limit D -> D i
G: Graph
D: Diagram G
forall (i j : G) (g : G i j), D _f g o ?legs i == ?legs j
  +
G: Graph
D: Diagram G
forall i : G, Limit D -> D i intros i x.
G: Graph
D: Diagram G
i: G
x: Limit D
D i
    exact (lim x i).
  +
G: Graph
D: Diagram G
forall (i j : G) (g : G i j),
D _f g o (fun (i0 : G) (x : Limit D) => lim x i0) i ==
(fun (i0 : G) (x : Limit D) => lim x i0) j intros i j g x.
G: Graph
D: Diagram G
i, j: G
g: G i j
x: Limit D
(D _f g) (lim x i) = lim x j
    apply limp.
Defined.

Instance unicone_limit `(D : Diagram G)
  : UniversalCone (cone_limit D).
G: Graph
D: Diagram G
UniversalCone (cone_limit D)
Proof.
G: Graph
D: Diagram G
UniversalCone (cone_limit D)
  srapply Build_UniversalCone; intro Y.
G: Graph
D: Diagram G
Y: Type
IsEquiv (cone_precompose (cone_limit D))
  srapply isequiv_adjointify.
G: Graph
D: Diagram G
Y: Type
Cone Y D -> Y -> Limit D
G: Graph
D: Diagram G
Y: Type
cone_precompose (cone_limit D) o ?g == idmap
G: Graph
D: Diagram G
Y: Type
?g o cone_precompose (cone_limit D) == idmap
  {
G: Graph
D: Diagram G
Y: Type
Cone Y D -> Y -> Limit D intros c y.
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
Limit D
    srapply Build_Limit.
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
forall i : G, D i
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
forall (i j : G) (g : G i j), (D _f g) (?lim i) = ?lim j
    {
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
forall i : G, D i intro i.
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
i: G
D i
      exact (legs c i y). }
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
forall (i j : G) (g : G i j),
(D _f g) ((fun i0 : G => c i0 y) i) = (fun i0 : G => c i0 y) j
    intros i j g.
G: Graph
D: Diagram G
Y: Type
c: Cone Y D
y: Y
i, j: G
g: G i j
(D _f g) ((fun i0 : G => c i0 y) i) = (fun i0 : G => c i0 y) j
    apply legs_comm. }
G: Graph
D: Diagram G
Y: Type
cone_precompose (cone_limit D)
o (fun (c : Cone Y D) (y : Y) =>
   {|
     lim := fun i : G => c i y;
     limp := fun (i j : G) (g : G i j) => legs_comm c i j g y
   |}) ==
idmap
G: Graph
D: Diagram G
Y: Type
(fun (c : Cone Y D) (y : Y) =>
 {|
   lim := fun i : G => c i y;
   limp := fun (i j : G) (g : G i j) => legs_comm c i j g y
 |})
o cone_precompose (cone_limit D) == idmap
  all: intro; reflexivity.
Defined.

Instance islimit_limit `(D : Diagram G) : IsLimit D (Limit D)
  := Build_IsLimit (cone_limit _) _.

(** * Functoriality of limits *)

Section FunctorialityLimit.

  Context `{Funext} {G : Graph}.

  (** Limits are preserved by composition with a (diagram) equivalence. *)

  Definition islimit_precompose_equiv {D : Diagram G} `(f : Q <~> Q')
    : IsLimit D Q' -> IsLimit D Q.
H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
IsLimit D Q' -> IsLimit D Q
  Proof.
H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
IsLimit D Q' -> IsLimit D Q
    intros HQ.
H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
HQ: IsLimit D Q'
IsLimit D Q
    srapply (Build_IsLimit (cone_precompose HQ f) _).
H: Funext
G: Graph
D: Diagram G
Q, Q': Type
f: Q <~> Q'
HQ: IsLimit D Q'
UniversalCone (cone_precompose HQ f)
    apply cone_precompose_equiv_universality, HQ.
  Defined.

  Definition islimit_postcompose_equiv {D1 D2 : Diagram G} (m : D1 ~d~ D2)
    {Q : Type} : IsLimit D1 Q -> IsLimit D2 Q.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
IsLimit D1 Q -> IsLimit D2 Q
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
IsLimit D1 Q -> IsLimit D2 Q
    intros HQ.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
HQ: IsLimit D1 Q
IsLimit D2 Q
    srapply (Build_IsLimit (cone_postcompose m HQ) _).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q: Type
HQ: IsLimit D1 Q
UniversalCone (cone_postcompose m HQ)
    apply cone_postcompose_equiv_universality, HQ.
  Defined.

  (** A diagram map [m] : [D1] => [D2] induces a map between any two limits of [D1] and [D2]. *)

  Definition functor_limit {D1 D2 : Diagram G} (m : DiagramMap D1 D2)
    {Q1 Q2} (HQ1 : IsLimit D1 Q1) (HQ2 : IsLimit D2 Q2)
    : Q1 -> Q2 := cone_precompose_inv HQ2 (cone_postcompose m HQ1).

  (** And this map commutes with diagram map. *)

  Definition functor_limit_commute {D1 D2 : Diagram G}
    (m : DiagramMap D1 D2) {Q1 Q2}
    (HQ1 : IsLimit D1 Q1) (HQ2 : IsLimit D2 Q2)
    : cone_postcompose m HQ1
      = cone_precompose HQ2 (functor_limit m HQ1 HQ2)
    := (eisretr (cone_precompose HQ2) _)^.

  (** ** Limits of equivalent diagrams *)

  (** Now we have than two equivalent diagrams have equivalent limits. *)

  Context {D1 D2 : Diagram G} (m : D1 ~d~ D2) {Q1 Q2}
    (HQ1 : IsLimit D1 Q1) (HQ2 : IsLimit D2 Q2).

  Definition functor_limit_eissect
    : functor_limit m HQ1 HQ2
      o functor_limit (diagram_equiv_inv m) HQ2 HQ1 == idmap.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
functor_limit m HQ1 HQ2 o functor_limit (diagram_equiv_inv m) HQ2 HQ1 ==
idmap
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
functor_limit m HQ1 HQ2 o functor_limit (diagram_equiv_inv m) HQ2 HQ1 ==
idmap
    apply ap10.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
(fun x : Q2 =>
 functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
idmap
    srapply (equiv_inj (cone_precompose HQ2) _).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
IsEquiv (cone_precompose HQ2)
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ2
  (fun x : Q2 =>
   functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
cone_precompose HQ2 idmap
    1: apply HQ2.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ2
  (fun x : Q2 =>
   functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
cone_precompose HQ2 idmap
    etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ2
  (fun x : Q2 =>
   functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
?Goal = cone_precompose HQ2 idmap
    2:symmetry; apply cone_precompose_identity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ2
  (fun x : Q2 =>
   functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
HQ2
    etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ2
  (fun x : Q2 =>
   functor_limit m HQ1 HQ2 (functor_limit (diagram_equiv_inv m) HQ2 HQ1 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
?Goal = HQ2
    1: apply cone_precompose_comp.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose (cone_precompose HQ2 (functor_limit m HQ1 HQ2))
  (functor_limit (diagram_equiv_inv m) HQ2 HQ1) =
HQ2
    rewrite eisretr, cone_postcompose_precompose, eisretr.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_postcompose m (cone_postcompose (diagram_equiv_inv m) HQ2) = HQ2
    rewrite cone_postcompose_comp, diagram_inv_is_section.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_postcompose (diagram_idmap D2) HQ2 = HQ2
    apply cone_postcompose_identity.
  Defined.

  Definition functor_limit_eisretr
    : functor_limit (diagram_equiv_inv m) HQ2 HQ1
      o functor_limit m HQ1 HQ2 == idmap.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
functor_limit (diagram_equiv_inv m) HQ2 HQ1 o functor_limit m HQ1 HQ2 ==
idmap
  Proof.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
functor_limit (diagram_equiv_inv m) HQ2 HQ1 o functor_limit m HQ1 HQ2 ==
idmap
    apply ap10.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
(fun x : Q1 =>
 functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
idmap
    srapply (equiv_inj (cone_precompose HQ1) _).
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
IsEquiv (cone_precompose HQ1)
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ1
  (fun x : Q1 =>
   functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
cone_precompose HQ1 idmap
    1: apply HQ1.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ1
  (fun x : Q1 =>
   functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
cone_precompose HQ1 idmap
    etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ1
  (fun x : Q1 =>
   functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
?Goal = cone_precompose HQ1 idmap
    2:symmetry; apply cone_precompose_identity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ1
  (fun x : Q1 =>
   functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
HQ1
    etransitivity.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose HQ1
  (fun x : Q1 =>
   functor_limit (diagram_equiv_inv m) HQ2 HQ1 (functor_limit m HQ1 HQ2 x)) =
?Goal
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
?Goal = HQ1
    1: apply cone_precompose_comp.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_precompose
  (cone_precompose HQ1 (functor_limit (diagram_equiv_inv m) HQ2 HQ1))
  (functor_limit m HQ1 HQ2) =
HQ1
    rewrite eisretr, cone_postcompose_precompose, eisretr.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_postcompose (diagram_equiv_inv m) (cone_postcompose m HQ1) = HQ1
    rewrite cone_postcompose_comp, diagram_inv_is_retraction.
H: Funext
G: Graph
D1, D2: Diagram G
m: D1 ~d~ D2
Q1, Q2: Type
HQ1: IsLimit D1 Q1
HQ2: IsLimit D2 Q2
cone_postcompose (diagram_idmap D1) HQ1 = HQ1
    apply cone_postcompose_identity.
  Defined.

  #[export] Instance isequiv_functor_limit
    : IsEquiv (functor_limit m HQ1 HQ2)
    := isequiv_adjointify _ _
      functor_limit_eissect functor_limit_eisretr.

  Definition equiv_functor_limit : Q1 <~> Q2
    := Build_Equiv _ _ _ isequiv_functor_limit.

End FunctorialityLimit.

(** * Unicity of limits *)

(** A particular case of the functoriality result is that all limits of a diagram are equivalent (and hence equal in presence of univalence). *)

Theorem limit_unicity `{Funext} {G : Graph} {D : Diagram G} {Q1 Q2 : Type}
  (HQ1 : IsLimit D Q1) (HQ2 : IsLimit D Q2)
  : Q1 <~> Q2.
H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsLimit D Q1
HQ2: IsLimit D Q2
Q1 <~> Q2
Proof.
H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsLimit D Q1
HQ2: IsLimit D Q2
Q1 <~> Q2
  srapply equiv_functor_limit.
H: Funext
G: Graph
D: Diagram G
Q1, Q2: Type
HQ1: IsLimit D Q1
HQ2: IsLimit D Q2
D ~d~ D
  srapply (Build_diagram_equiv (diagram_idmap D)).
Defined.

(** * Limits are right adjoint to constant diagram *)

Theorem limit_adjoint {G : Graph} {D : Diagram G} {C : Type}
  : (C -> Limit D) <~> DiagramMap (diagram_const C) D.
G: Graph
D: Diagram G
C: Type
(C -> Limit D) <~> DiagramMap (diagram_const C) D
Proof.
G: Graph
D: Diagram G
C: Type
(C -> Limit D) <~> DiagramMap (diagram_const C) D
  srapply equiv_adjointify.
G: Graph
D: Diagram G
C: Type
(C -> Limit D) -> DiagramMap (diagram_const C) D
G: Graph
D: Diagram G
C: Type
DiagramMap (diagram_const C) D -> C -> Limit D
G: Graph
D: Diagram G
C: Type
?f o ?g == idmap
G: Graph
D: Diagram G
C: Type
?g o ?f == idmap
  {
G: Graph
D: Diagram G
C: Type
(C -> Limit D) -> DiagramMap (diagram_const C) D intro f.
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
DiagramMap (diagram_const C) D
    srapply Build_DiagramMap.
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
forall i : G, diagram_const C i -> D i
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((diagram_const C) _f g) x)
    {
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
forall i : G, diagram_const C i -> D i intros i c.
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
i: G
c: diagram_const C i
D i
      apply lim, f, c. }
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) ((fun (i0 : G) (c : diagram_const C i0) => lim (f c) i0) i x) =
(fun (i0 : G) (c : diagram_const C i0) => lim (f c) i0) j
  (((diagram_const C) _f g) x)
    intros i j g x.
G: Graph
D: Diagram G
C: Type
f: C -> Limit D
i, j: G
g: G i j
x: diagram_const C i
(D _f g) ((fun (i0 : G) (c : diagram_const C i0) => lim (f c) i0) i x) =
(fun (i0 : G) (c : diagram_const C i0) => lim (f c) i0) j
  (((diagram_const C) _f g) x)
    apply limp. }
G: Graph
D: Diagram G
C: Type
DiagramMap (diagram_const C) D -> C -> Limit D
G: Graph
D: Diagram G
C: Type
(fun f : C -> Limit D =>
 {|
   DiagramMap_obj := fun (i : G) (c : diagram_const C i) => lim (f c) i;
   DiagramMap_comm :=
     fun (i j : G) (g : G i j) (x : diagram_const C i) =>
     limp (f (((diagram_const C) _f g) x)) i j g
 |})
o ?g == idmap
G: Graph
D: Diagram G
C: Type
?g
o (fun f : C -> Limit D =>
   {|
     DiagramMap_obj := fun (i : G) (c : diagram_const C i) => lim (f c) i;
     DiagramMap_comm :=
       fun (i j : G) (g : G i j) (x : diagram_const C i) =>
       limp (f (((diagram_const C) _f g) x)) i j g
   |}) ==
idmap
  {
G: Graph
D: Diagram G
C: Type
DiagramMap (diagram_const C) D -> C -> Limit D intros [f p] c.
G: Graph
D: Diagram G
C: Type
f: forall i : G, diagram_const C i -> D i
p: forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (f i x) = f j (((diagram_const C) _f g) x)
c: C
Limit D
    srapply Build_Limit.
G: Graph
D: Diagram G
C: Type
f: forall i : G, diagram_const C i -> D i
p: forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (f i x) = f j (((diagram_const C) _f g) x)
c: C
forall i : G, D i
G: Graph
D: Diagram G
C: Type
f: forall i : G, diagram_const C i -> D i
p: forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (f i x) = f j (((diagram_const C) _f g) x)
c: C
forall (i j : G) (g : G i j), (D _f g) (?lim i) = ?lim j
    {
G: Graph
D: Diagram G
C: Type
f: forall i : G, diagram_const C i -> D i
p: forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (f i x) = f j (((diagram_const C) _f g) x)
c: C
forall i : G, D i intro i.
G: Graph
D: Diagram G
C: Type
f: forall i0 : G, diagram_const C i0 -> D i0
p: forall (i0 j : G) (g : G i0 j) (x : diagram_const C i0),
(D _f g) (f i0 x) = f j (((diagram_const C) _f g) x)
c: C
i: G
D i
      apply f, c. }
G: Graph
D: Diagram G
C: Type
f: forall i : G, diagram_const C i -> D i
p: forall (i j : G) (g : G i j) (x : diagram_const C i),
(D _f g) (f i x) = f j (((diagram_const C) _f g) x)
c: C
forall (i j : G) (g : G i j),
(D _f g) ((fun i0 : G => f i0 c) i) = (fun i0 : G => f i0 c) j
    intros i j g.
G: Graph
D: Diagram G
C: Type
f: forall i0 : G, diagram_const C i0 -> D i0
p: forall (i0 j0 : G) (g0 : G i0 j0) (x : diagram_const C i0),
(D _f g0) (f i0 x) = f j0 (((diagram_const C) _f g0) x)
c: C
i, j: G
g: G i j
(D _f g) ((fun i0 : G => f i0 c) i) = (fun i0 : G => f i0 c) j
    apply p. }
G: Graph
D: Diagram G
C: Type
(fun f : C -> Limit D =>
 {|
   DiagramMap_obj := fun (i : G) (c : diagram_const C i) => lim (f c) i;
   DiagramMap_comm :=
     fun (i j : G) (g : G i j) (x : diagram_const C i) =>
     limp (f (((diagram_const C) _f g) x)) i j g
 |})
o (fun X : DiagramMap (diagram_const C) D =>
   (fun (f : forall i : G, diagram_const C i -> D i)
      (p : forall (i j : G) (g : G i j) (x : diagram_const C i),
           (D _f g) (f i x) = f j (((diagram_const C) _f g) x))
      (c : C) =>
    {|
      lim := fun i : G => f i c;
      limp := fun (i j : G) (g : G i j) => p i j g c
    |}) X (DiagramMap_comm X)) ==
idmap
G: Graph
D: Diagram G
C: Type
(fun X : DiagramMap (diagram_const C) D =>
 (fun (f : forall i : G, diagram_const C i -> D i)
    (p : forall (i j : G) (g : G i j) (x : diagram_const C i),
         (D _f g) (f i x) = f j (((diagram_const C) _f g) x))
    (c : C) =>
  {|
    lim := fun i : G => f i c; limp := fun (i j : G) (g : G i j) => p i j g c
  |}) X (DiagramMap_comm X))
o (fun f : C -> Limit D =>
   {|
     DiagramMap_obj := fun (i : G) (c : diagram_const C i) => lim (f c) i;
     DiagramMap_comm :=
       fun (i j : G) (g : G i j) (x : diagram_const C i) =>
       limp (f (((diagram_const C) _f g) x)) i j g
   |}) ==
idmap
  1,2: intro; reflexivity.
Defined.