Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cocone.
Require Import Colimits.Colimit.

(** * Colimit of the dependent sum of a family of diagrams *)

(** Given a family of diagrams [D y], and a colimit [Q y] of each diagram, one can consider the diagram of the sigmas of the types of the [D y]s. Then, a colimit of such a diagram is the sigma of the [Q y]s. *)

Section ColimitSigma.

  Context `{Funext} {G : Graph} {Y : Type} (D : Y -> Diagram G).

  (** The diagram of the sigmas. *)

  Definition sigma_diagram : Diagram G.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Diagram G
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Diagram G
    srapply Build_Diagram.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
G -> Type
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
forall i j : G, G i j -> ?obj i -> ?obj j
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
G -> Type exact (fun i => {y: Y & D y i}).
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
forall i j : G,
G i j ->
(fun i0 : G => {y : Y & D y i0}) i ->
(fun i0 : G => {y : Y & D y i0}) j simpl; intros i j g x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
i, j: G
g: G i j
x: {y : Y & D y i}
{y : Y & D y j}
      exact (x.1; D x.1 _f g x.2).
  Defined.

  (** The embedding, for a particular [y], of [D(y)] in the sigma diagram. *)

  Definition sigma_diagram_map (y: Y) : DiagramMap (D y) sigma_diagram.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
DiagramMap (D y) sigma_diagram
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
DiagramMap (D y) sigma_diagram
    srapply Build_DiagramMap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall i : G, D y i -> sigma_diagram i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall (i j : G) (g : G i j) (x : D y i),
(sigma_diagram _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((D y) _f g) x)
    1: exact (fun i x => (y; x)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall (i j : G) (g : G i j) (x : D y i),
(sigma_diagram _f g)
  ((fun (i0 : G) (x0 : D y i0) => (y; x0)) i x) =
(fun (i0 : G) (x0 : D y i0) => (y; x0)) j
  (((D y) _f g) x)
    reflexivity.
  Defined.

  Context {Q : Y -> Type}.

  (** The sigma of a family of cocones. *)

  Definition sigma_cocone (C : forall y, Cocone (D y) (Q y))
    : Cocone sigma_diagram (sig Q).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
Cocone sigma_diagram {x : _ & Q x}
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
Cocone sigma_diagram {x : _ & Q x}
    srapply Build_Cocone; simpl; intros i x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i: G
x: {y : Y & D y i}
{x : _ & Q x}
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
forall g : G i x,
(fun x0 : {y : Y & D y i} =>
 (fun (i : G) (x : {y : Y & D y i}) => ?Goal) x
   (x0.1; ((D x0.1) _f g) x0.2)) ==
(fun (i : G) (x : {y : Y & D y i}) => ?Goal) i
    1: exact (x.1; legs (C x.1) i x.2).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
forall g : G i x,
(fun x0 : {y : Y & D y i} =>
 (fun (i : G) (x : {y : Y & D y i}) =>
  (x.1; C x.1 i x.2)) x (x0.1; ((D x0.1) _f g) x0.2)) ==
(fun (i : G) (x : {y : Y & D y i}) =>
 (x.1; C x.1 i x.2)) i
    simpl; intros g x'.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
(x'.1; C x'.1 x (((D x'.1) _f g) x'.2)) =
(x'.1; C x'.1 i x'.2)
    srapply path_sigma'.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
x'.1 = x'.1
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
transport Q ?p (C x'.1 x (((D x'.1) _f g) x'.2)) =
C x'.1 i x'.2
    1: reflexivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
transport Q 1 (C x'.1 x (((D x'.1) _f g) x'.2)) =
C x'.1 i x'.2
    apply legs_comm.
  Defined.

  (** The main result: [sig Q] is a colimit of the diagram of sigma types. *)

  Lemma iscolimit_sigma (HQ : forall y, IsColimit (D y) (Q y))
  : IsColimit sigma_diagram (sig Q).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
IsColimit sigma_diagram {x : _ & Q x}
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
IsColimit sigma_diagram {x : _ & Q x}
    pose (SigmaC := sigma_cocone (fun y => HQ y)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
IsColimit sigma_diagram {x : _ & Q x}
    srapply (Build_IsColimit SigmaC).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
UniversalCocone SigmaC
    srapply Build_UniversalCocone.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
forall Y0 : Type, IsEquiv (cocone_postcompose SigmaC)
    intros X; srapply isequiv_adjointify.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
Cocone sigma_diagram X -> {x : _ & Q x} -> X
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
cocone_postcompose SigmaC o ?g == idmap
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
?g o cocone_postcompose SigmaC == idmap
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
Cocone sigma_diagram X -> {x : _ & Q x} -> X intros CX x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
X
      srapply (cocone_postcompose_inv (HQ x.1) _ x.2).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
Cocone (D x.1) X
      srapply (cocone_precompose _ CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
DiagramMap (D x.1) sigma_diagram
      apply sigma_diagram_map.
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
cocone_postcompose SigmaC
o (fun (CX : Cocone sigma_diagram X)
     (x : {x : _ & Q x}) =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX)
     x.2) == idmap intro CX.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX)
     x.2) = CX
      pose (CXy := fun y => cocone_precompose (sigma_diagram_map y) CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX)
     x.2) = CX
      change (cocone_postcompose SigmaC
        (fun x => cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2) = CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2) = CX
      srapply path_cocone; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall i : G,
(fun x : {y : Y & D y i} =>
 cocone_postcompose_inv (HQ x.1) (CXy x.1)
   (HQ x.1 i x.2)) == CX i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall (i j : G) (g : G i j) 
(x : {y : Y & D y i}),
ap
  (fun x0 : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ x.1) i j g x.2)) @
?Goal i x =
?Goal j (x.1; ((D x.1) _f g) x.2) @
legs_comm CX i j g x
      +
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall i : G,
(fun x : {y : Y & D y i} =>
 cocone_postcompose_inv (HQ x.1) (CXy x.1)
   (HQ x.1 i x.2)) == CX i intros i x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i: G
x: {y : Y & D y i}
cocone_postcompose_inv (HQ x.1) (CXy x.1)
  (HQ x.1 i x.2) = CX i x
        change (legs (cocone_postcompose (HQ x.1)
                 (cocone_postcompose_inv (HQ x.1) (CXy x.1))) i x.2 = CX i x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i: G
x: {y : Y & D y i}
cocone_postcompose (HQ x.1)
  (cocone_postcompose_inv (HQ x.1) (CXy x.1)) i x.2 =
CX i x
        exact (ap10 (apD10 (ap legs (eisretr
          (cocone_postcompose (HQ x.1)) (CXy _))) i) x.2).
      +
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall (i j : G) (g : G i j) (x : {y : Y & D y i}),
ap
  (fun x0 : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ x.1) i j g x.2)) @
(fun i0 : G =>
 (fun x0 : {y : Y & D y i0} =>
  ap10
    (apD10
       (ap legs
          (eisretr (cocone_postcompose (HQ x0.1))
             (CXy x0.1))) i0) x0.2)
 :
 (fun x0 : {y : Y & D y i0} =>
  cocone_postcompose_inv (HQ x0.1) (CXy x0.1)
    (HQ x0.1 i0 x0.2)) == CX i0) i x =
(fun i0 : G =>
 (fun x0 : {y : Y & D y i0} =>
  ap10
    (apD10
       (ap legs
          (eisretr (cocone_postcompose (HQ x0.1))
             (CXy x0.1))) i0) x0.2)
 :
 (fun x0 : {y : Y & D y i0} =>
  cocone_postcompose_inv (HQ x0.1) (CXy x0.1)
    (HQ x0.1 i0 x0.2)) == CX i0) j
  (x.1; ((D x.1) _f g) x.2) @ legs_comm CX i j g x intros i j g [y x]; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10
  (apD10
     (ap legs
        (eisretr (cocone_postcompose (HQ y)) (CXy y)))
     i) x =
ap10
  (apD10
     (ap legs
        (eisretr (cocone_postcompose (HQ y)) (CXy y)))
     j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        set (py := (eisretr (cocone_postcompose (HQ y)) (CXy y))).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y)
 o (cocone_postcompose (HQ y))^-1) 
  (CXy y) = idmap (CXy y)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 (ap legs py) i) x =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        set (py1 := ap legs py).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y)
 o (cocone_postcompose (HQ y))^-1) 
  (CXy y) = idmap (CXy y)
py1:= ap legs py: cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        specialize (apD legs_comm py); intro py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y)
 o (cocone_postcompose (HQ y))^-1) 
  (CXy y) = idmap (CXy y)
py1:= ap legs py: cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: transport
  (fun C : Cocone (D y) X =>
   forall (i j : G) (g : G i j),
   C j o (D y) _f g == C i) py
  (legs_comm
     (cocone_postcompose 
        (HQ y)
        ((cocone_postcompose (HQ y))^-1 (CXy y)))) =
legs_comm (CXy y)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          simpl in *.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: transport
  (fun C : Cocone (D y) X =>
   forall (i j : G) (g : G i j),
   (fun x : D y i => C j (((D y) _f g) x)) ==
   C i) py
  (fun (i j : G) (g : G i j) (x : D y i) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y))
     (legs_comm (HQ y) i j g x)) =
(fun (i j : G) (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: (fun y0 : G =>
 transport
   (fun x : Cocone (D y) X =>
    forall (j : G) (g : G y0 j),
    (fun x0 : D y y0 => x j (((D y) _f g) x0)) ==
    x y0) py
   (fun (j : G) (g : G y0 j) (x : D y y0) =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y))
      (legs_comm (HQ y) y0 j g x))) =
(fun (i j : G) (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 i); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: transport
  (fun x : Cocone (D y) X =>
   forall (j : G) (g : G i j),
   (fun x0 : D y i => x j (((D y) _f g) x0)) ==
   x i) py
  (fun (j : G) (g : G i j) (x : D y i) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y))
     (legs_comm (HQ y) i j g x)) =
(fun (j : G) (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: (fun y0 : G =>
 transport
   (fun x : Cocone (D y) X =>
    forall g : G i y0,
    (fun x0 : D y i => x y0 (((D y) _f g) x0)) ==
    x i) py
   (fun (g : G i y0) (x : D y i) =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y))
      (legs_comm (HQ y) i y0 g x))) =
(fun (j : G) (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 j); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: transport
  (fun x : Cocone (D y) X =>
   forall g : G i j,
   (fun x0 : D y i => x j (((D y) _f g) x0)) ==
   x i) py
  (fun (g : G i j) (x : D y i) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y))
     (legs_comm (HQ y) i j g x)) =
(fun (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: (fun y0 : G i j =>
 transport
   (fun x : Cocone (D y) X =>
    (fun x0 : D y i => x j (((D y) _f y0) x0)) ==
    x i) py
   (fun x : D y i =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y))
      (legs_comm (HQ y) i j y0 x))) =
(fun (g : G i j) (x : D y i) =>
 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 g); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: transport
  (fun x : Cocone (D y) X =>
   (fun x0 : D y i => x j (((D y) _f g) x0)) ==
   x i) py
  (fun x : D y i =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y))
     (legs_comm (HQ y) i j g x)) =
(fun x : D y i => 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: (fun y0 : D y i =>
 transport
   (fun x : Cocone (D y) X =>
    x j (((D y) _f g) y0) = x i y0) py
   (ap ((cocone_postcompose (HQ y))^-1 (CXy y))
      (legs_comm (HQ y) i j g y0))) =
(fun x : D y i => 1 @ legs_comm CX i j g (y; x))
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 x); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: transport
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x) = x0 i x) py
  (ap ((cocone_postcompose (HQ y))^-1 (CXy y))
     (legs_comm (HQ y) i j g x)) =
1 @ legs_comm CX i j g (y; x)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite transport_paths_FlFr in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: ((ap
    (fun x0 : Cocone (D y) X =>
     x0 j (((D y) _f g) x)) py)^ @
 ap ((cocone_postcompose (HQ y))^-1 (CXy y))
   (legs_comm (HQ y) i j g x)) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
1 @ legs_comm CX i j g (y; x)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          rewrite concat_1p, concat_pp_p in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: (ap
   (fun x0 : Cocone (D y) X =>
    x0 j (((D y) _f g) x)) py)^ @
(ap ((cocone_postcompose (HQ y))^-1 (CXy y))
   (legs_comm (HQ y) i j g x) @
 ap (fun x0 : Cocone (D y) X => x0 i x) py) =
legs_comm CX i j g (y; x)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
          apply moveL_Mp in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        rewrite (ap_path_sigma_1p
          (fun x01 x02 => cocone_postcompose_inv (HQ x01) (CXy x01) x02)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py1:= ap legs py: (fun (i : G) (x : D y i) =>
 (cocone_postcompose (HQ y))^-1 
   (CXy y) (HQ y i x)) =
(fun (i : G) (x : D y i) => CX i (y; x))
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @ ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        (* Set Printing Coercions. (* to understand what happens *)   *)
        subst py1.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        etransitivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
?Goal =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        *
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal etransitivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal1
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
?Goal1 = ?Goal
          2:exact py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun z : Q y =>
   cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x =
ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py
          apply ap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x =
ap (fun x0 : Cocone (D y) X => x0 i x) py
          rewrite (ap_compose legs (fun x0 => x0 i x)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x =
ap (fun x0 : forall i : G, D y i -> X => x0 i x)
  (ap legs py)
          rewrite (ap_apply_lD2 _ i x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x =
apD10 (apD10 (ap legs py) i) x
          reflexivity.
        *
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x))
  py @ legs_comm CX i j g (y; x) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @
legs_comm CX i j g (y; x) apply ap10, ap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x))
  py = ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          rewrite (ap_compose legs (fun x0 => x0 j _)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun x0 : forall i : G, D y i -> X =>
   x0 j (((D y) _f g) x)) (ap legs py) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          rewrite (ap_apply_lD2 _ j _).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y =>
cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y)
  ((cocone_postcompose (HQ y))^-1 (CXy y)) =
CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y))
  (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap
  (fun x0 : Cocone (D y) X =>
   x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
apD10 (apD10 (ap legs py) j) (((D y) _f g) x) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          reflexivity.
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
(fun (CX : Cocone sigma_diagram X) (x : {x : _ & Q x})
 =>
 cocone_postcompose_inv (HQ x.1)
   (cocone_precompose (sigma_diagram_map x.1) CX) x.2)
o cocone_postcompose SigmaC == idmap intros f.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
(fun x : {x : _ & Q x} =>
 cocone_postcompose_inv (HQ x.1)
   (cocone_precompose (sigma_diagram_map x.1)
      (cocone_postcompose SigmaC f)) x.2) = f
      apply path_forall; intros [y x]; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_precompose (sigma_diagram_map y)
     (cocone_postcompose SigmaC f)) x = f (y; x)
      rewrite <- cocone_precompose_postcompose.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_postcompose
     (cocone_precompose (sigma_diagram_map y) SigmaC)
     f) x = f (y; x)
      srapply (apD10 (g := fun x => f (y; x)) _ x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_postcompose
     (cocone_precompose (sigma_diagram_map y) SigmaC)
     f) = (fun x : Q y => f (y; x))
      snrapply equiv_moveR_equiv_V.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose
  (cocone_precompose (sigma_diagram_map y) SigmaC) f =
cocone_postcompose (HQ y) (fun x : Q y => f (y; x))
      srapply path_cocone.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall i : G,
cocone_postcompose
  (cocone_precompose (sigma_diagram_map y) SigmaC) f i ==
cocone_postcompose (HQ y) (fun x : Q y => f (y; x)) i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall (i j : G) (g : G i j) 
(x0 : D y i),
legs_comm
  (cocone_postcompose
     (cocone_precompose (sigma_diagram_map y) SigmaC)
     f) i j g x0 @ ?path_legs i x0 =
?path_legs j (((D y) _f g) x0) @
legs_comm
  (cocone_postcompose (HQ y) (fun x : Q y => f (y; x)))
  i j g x0
      1: reflexivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall (i j : G) (g : G i j) (x : D y i),
legs_comm
  (cocone_postcompose
     (cocone_precompose (sigma_diagram_map y) SigmaC)
     f) i j g x @
(fun (i0 : G) (x0 : D y i0) => 1) i x =
(fun (i0 : G) (x0 : D y i0) => 1) j (((D y) _f g) x) @
legs_comm
  (cocone_postcompose (HQ y)
     (fun x0 : Q y => f (y; x0))) i j g x
      intros i j g x'; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
i, j: G
g: G i j
x': D y i
ap f (1 @ path_sigma' Q 1 (legs_comm (HQ y) i j g x')) @
1 =
1 @
ap (fun x : Q y => f (y; x))
  (legs_comm (HQ y) i j g x')
      hott_simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
i, j: G
g: G i j
x': D y i
ap f (path_sigma' Q 1 (legs_comm (HQ y) i j g x')) =
ap (fun x : Q y => f (y; x))
  (legs_comm (HQ y) i j g x')
      exact (ap_compose _ _ _)^.
  Defined.

End ColimitSigma.

(** ** Sigma diagrams and diagram maps / equivalences *)

Section SigmaDiagram.

  Context {G : Graph} {Y : Type} (D1 D2 : Y -> Diagram G).

  Definition sigma_diagram_functor (m : forall y, DiagramMap (D1 y) (D2 y))
  : DiagramMap (sigma_diagram D1) (sigma_diagram D2).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
DiagramMap (sigma_diagram D1) (sigma_diagram D2)
  Proof.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
DiagramMap (sigma_diagram D1) (sigma_diagram D2)
    srapply Build_DiagramMap.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall i : G, sigma_diagram D1 i -> sigma_diagram D2 i
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall (i j : G) (g : G i j) (x : sigma_diagram D1 i),
((sigma_diagram D2) _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((sigma_diagram D1) _f g) x)
    -
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall i : G, sigma_diagram D1 i -> sigma_diagram D2 i intros i.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i: G
sigma_diagram D1 i -> sigma_diagram D2 i
      srapply (functor_sigma idmap _).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i: G
forall a : Y,
(fun y : Y => D1 y i) a ->
(fun y : Y => D2 y i) (idmap a)
      intros y; apply m.
    -
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall (i j : G) (g : G i j) (x : sigma_diagram D1 i),
((sigma_diagram D2) _f g)
  ((fun i0 : G =>
    functor_sigma idmap
      (fun y : Y =>
       let X := fun y0 : Y => DiagramMap_obj (m y0) in
       X y i0)) i x) =
(fun i0 : G =>
 functor_sigma idmap
   (fun y : Y =>
    let X := fun y0 : Y => DiagramMap_obj (m y0) in
    X y i0)) j (((sigma_diagram D1) _f g) x) intros i j g x; simpl in *.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
(x.1; ((D2 x.1) _f g) (m x.1 i x.2)) =
functor_sigma idmap (fun y : Y => m y j)
  (x.1; ((D1 x.1) _f g) x.2)
    srapply path_sigma'.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
x.1 = (x.1; ((D1 x.1) _f g) x.2).1
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
transport (fun y : Y => D2 y j) ?p
  (((D2 x.1) _f g) (m x.1 i x.2)) =
m (x.1; ((D1 x.1) _f g) x.2).1 j
  (x.1; ((D1 x.1) _f g) x.2).2
    1: reflexivity.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
transport (fun y : Y => D2 y j) 1
  (((D2 x.1) _f g) (m x.1 i x.2)) =
m (x.1; ((D1 x.1) _f g) x.2).1 j
  (x.1; ((D1 x.1) _f g) x.2).2
    simpl.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
((D2 x.1) _f g) (m x.1 i x.2) =
m x.1 j (((D1 x.1) _f g) x.2)
    apply (DiagramMap_comm (m x.1)).
  Defined.

  Definition sigma_diag_functor_equiv (m : forall y, (D1 y) ~d~ (D2 y))
    : (sigma_diagram D1) ~d~ (sigma_diagram D2).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
sigma_diagram D1 ~d~ sigma_diagram D2
  Proof.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
sigma_diagram D1 ~d~ sigma_diagram D2
    srapply (Build_diagram_equiv (sigma_diagram_functor m)).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
forall i : G,
IsEquiv (sigma_diagram_functor (fun y : Y => m y) i)
    intros i.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
i: G
IsEquiv (sigma_diagram_functor (fun y : Y => m y) i)
    srapply isequiv_functor_sigma.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
i: G
forall a : Y,
IsEquiv
  ((fun y : Y =>
    let X :=
      fun y0 : Y =>
      DiagramMap_obj
        ((fun y1 : Y => diag_equiv_map (m y1)) y0) in
    X y i) a)
    intros y; apply m.
  Defined.

End SigmaDiagram.