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 Diagrams.DDiagram.
Require Import Colimits.Colimit.

Local Open Scope path_scope.

(** * Flattening lemma *)

(** This file provides a proof of the flattening lemma for colimits. This lemma describes the type [sig E'] when [E' : colimit D -> Type] is a type family defined by recursion on a colimit. The flattening lemma in the case of coequalizers is presented in section 6.12 of the HoTT book and is in Colimits/Coeq.v. *)
(** TODO: See whether there's a straightforward way to deduce the flattening lemma for general colimits from the version for coequalizers. *)

Section Flattening.
  (** ** Equifibered diagrams *)

  Context `{Univalence} {G : Graph} (D : Diagram G)
    (E : DDiagram D) `(Equifibered _ _ E).

  Let E_f {i j : G} (g : G i j) (x : D i) : E (i; x) -> E (j; (D _f g) x)
      := @arr _ E (i; x) (j; D _f g x) (g; 1).

  (** Now, given an equifibered diagram and using univalence, one can define a type family [E' : colimit D -> Type] by recursion on the colimit. *)

  Definition E' : Colimit D -> Type.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Colimit D -> Type
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Colimit D -> Type
    apply Colimit_rec.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Cocone D Type simple refine (Build_Cocone _ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall i : G, D i -> Type
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall (i j : G) (g : G i j),
?legs j o D _f g == ?legs i
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall i : G, D i -> Type exact (fun i x => E (i; x)).
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall (i j : G) (g : G i j),
(fun (i0 : G) (x : D i0) => E (i0; x)) j o D _f g ==
(fun (i0 : G) (x : D i0) => E (i0; x)) i intros i j g x; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
E (j; (D _f g) x) = E (i; x)
      symmetry.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
E (i; x) = E (j; (D _f g) x)
      exact (path_universe (E_f _ _)).
  Defined.

  (** ** Helper lemmas *)

  Definition transport_E' {i j : G} (g : G i j)  (x : D i) (y : E (i; x))
    : transport E' (colimp i j g x) (E_f g x y) = y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport E' (colimp i j g x) (E_f g x y) = y
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport E' (colimp i j g x) (E_f g x y) = y
    refine (transport_idmap_ap _ _ _ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport idmap (ap E' (colimp i j g x)) (E_f g x y) =
y
    srefine (transport2 idmap _ _ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
E' (colim j ((D _f g) x)) = E' (colim i x)
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
ap E' (colimp i j g x) = ?q
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport idmap ?q (E_f g x y) = y
    2: apply Colimit_rec_beta_colimp; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport idmap
  (legs_comm
     {|
       legs := fun (i : G) (x : D i) => E (i; x);
       legs_comm :=
         fun (i j : G) (g : G i j) =>
         (fun x : D i =>
          (path_universe (E_f g x))^
          :
          E (j; (D _f g) x) = E (i; x))
         :
         (fun (i0 : G) (x : D i0) => E (i0; x)) j
         o D _f g ==
         (fun (i0 : G) (x : D i0) => E (i0; x)) i
     |} i j g x) (E_f g x y) = y
    apply (moveR_transport_V idmap).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
E_f g x y =
transport idmap (path_universe (E_f g x)) y
    symmetry; apply transport_path_universe.
  Defined.

  Definition transport_E'_V {i j : G} (g : G i j)  (x : D i) (y : E (i; x))
    : transport E' (colimp i j g x)^ y = E_f g x y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport E' (colimp i j g x)^ y = E_f g x y
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport E' (colimp i j g x)^ y = E_f g x y
    apply moveR_transport_V.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
y = transport E' (colimp i j g x) (E_f g x y)
    symmetry.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport E' (colimp i j g x) (E_f g x y) = y
    apply transport_E'.
  Defined.

  Definition transport_E'_V_E' {i j : G} (g : G i j)  (x : D i) (y : E (i; x))
    : transport_E' g x y
      = ap (transport E' (colimp i j g x)) (transport_E'_V g x y)^
        @ transport_pV E' (colimp i j g x) y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport_E' g x y =
ap (transport E' (colimp i j g x))
  (transport_E'_V g x y)^ @
transport_pV E' (colimp i j g x) y
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport_E' g x y =
ap (transport E' (colimp i j g x))
  (transport_E'_V g x y)^ @
transport_pV E' (colimp i j g x) y
    rewrite moveR_transport_V_V, inv_V.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E (i; x)
transport_E' g x y =
ap (transport E' (colimp i j g x))
  (moveL_transport_V E' (colimp i j g x) (E_f g x y) y
     (transport_E' g x y)) @
transport_pV E' (colimp i j g x) y
    symmetry; apply ap_transport_transport_pV.
  Defined.

  (** ** Main result *)

  (** We define the cocone over the sigma diagram to [sig E']. *)

  Definition cocone_E' : Cocone (diagram_sigma E) (sig E').
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Cocone (diagram_sigma E) {x : _ & E' x}
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Cocone (diagram_sigma E) {x : _ & E' x}
    srapply Build_Cocone; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall i : G, {x : D i & E (i; x)} -> {x : _ & E' x}
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 ?Goal j ((D _f g) x.1; (E _f (g; 1)) x.2)) == ?Goal i
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall i : G, {x : D i & E (i; x)} -> {x : _ & E' x} intros i w.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i: G
w: {x : D i & E (i; x)}
{x : _ & E' x}
      exists (colim i w.1); cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i: G
w: {x : D i & E (i; x)}
E' (colim i w.1)
      exact w.2.
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 (fun (i0 : G) (w : {x0 : D i0 & E (i0; x0)}) =>
  (colim i0 w.1; w.2 : E' (colim i0 w.1))) j
   ((D _f g) x.1; (E _f (g; 1)) x.2)) ==
(fun (i0 : G) (w : {x : D i0 & E (i0; x)}) =>
 (colim i0 w.1; w.2 : E' (colim i0 w.1))) i intros i j g x; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: {x : D i & E (i; x)}
(colim j ((D _f g) x.1); (E _f (g; 1)) x.2) =
(colim i x.1; x.2)
      srapply path_sigma'.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: {x : D i & E (i; x)}
colim j ((D _f g) x.1) = colim i x.1
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: {x : D i & E (i; x)}
transport E' ?p ((E _f (g; 1)) x.2) = x.2
      +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: {x : D i & E (i; x)}
colim j ((D _f g) x.1) = colim i x.1 apply colimp.
      +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: {x : D i & E (i; x)}
transport E' (colimp i j g x.1) ((E _f (g; 1)) x.2) =
x.2 apply transport_E'.
  Defined.

  (** And we directly prove that it is universal.  We break the proof into parts to slightly speed it up. *)

  Local Opaque path_sigma ap11.

  Local Definition cocone_extends Z: Cocone (diagram_sigma E) Z -> ((sig E') -> Z).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
Cocone (diagram_sigma E) Z -> {x : _ & E' x} -> Z
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
Cocone (diagram_sigma E) Z -> {x : _ & E' x} -> Z
    intros [q qq]; cbn in *.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
{x : _ & E' x} -> Z
    intros [x y]; revert x y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
forall x : Colimit D, E' x -> Z
    srapply Colimit_ind; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
forall (i : G) (x : D i), E' (colim i x) -> Z
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
forall (i j : G) (g : G i j) (x : D i),
transport (fun w : Colimit D => E' w -> Z)
  (colimp i j g x) (?Goal j ((D _f g) x)) = ?Goal i x
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
forall (i : G) (x : D i), E' (colim i x) -> Z intros i x y; exact (q i (x; y)).
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
forall (i j : G) (g : G i j) (x : D i),
transport (fun w : Colimit D => E' w -> Z)
  (colimp i j g x)
  ((fun (i0 : G) (x0 : D i0) (y : E' (colim i0 x0)) =>
    q i0 (x0; y)) j ((D _f g) x)) =
(fun (i0 : G) (x0 : D i0) (y : E' (colim i0 x0)) =>
 q i0 (x0; y)) i x intros i j g x; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
transport (fun w : Colimit D => E' w -> Z)
  (colimp i j g x)
  (fun y : E' (colim j ((D _f g) x)) =>
   q j ((D _f g) x; y)) =
(fun y : E' (colim i x) => q i (x; y))
      funext y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport (fun w : Colimit D => E' w -> Z)
  (colimp i j g x)
  (fun y : E' (colim j ((D _f g) x)) =>
   q j ((D _f g) x; y)) y = q i (x; y)
      refine (transport_arrow_toconst _ _ _ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
y: E' (colim i x)
q j ((D _f g) x; transport E' (colimp i j g x)^ y) =
q i (x; y)
      refine (_ @ qq i j g (x; y)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
y: E' (colim i x)
q j ((D _f g) x; transport E' (colimp i j g x)^ y) =
q j ((D _f g) (x; y).1; (E _f (g; 1)) (x; y).2)
      cbn; f_ap.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
y: E' (colim i x)
((D _f g) x; transport E' (colimp i j g x)^ y) =
((D _f g) x; (E _f (g; 1)) y)
      refine (path_sigma' _ 1 _); cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, {x : D i & E (i; x)} -> Z
qq: forall (i j : G) (g : G i j),
(fun x : {x : D i & E (i; x)} =>
 q j ((D _f g) x.1; (E _f (g; 1)) x.2)) == q i
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport E' (colimp i j g x)^ y = (E _f (g; 1)) y
      apply transport_E'_V.
  Defined.

  Local Definition cocone_isretr Z
    : cocone_postcompose cocone_E' o cocone_extends Z == idmap.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_postcompose cocone_E' o cocone_extends Z ==
idmap
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_postcompose cocone_E' o cocone_extends Z ==
idmap
    intros [q qq].
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
cocone_postcompose cocone_E'
  (cocone_extends Z {| legs := q; legs_comm := qq |}) =
{| legs := q; legs_comm := qq |}
    srapply path_cocone.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
forall i : G,
cocone_postcompose cocone_E'
  (cocone_extends Z {| legs := q; legs_comm := qq |})
  i == {| legs := q; legs_comm := qq |} i
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
forall (i j : G) (g : G i j) (x : diagram_sigma E i),
legs_comm
  (cocone_postcompose cocone_E'
     (cocone_extends Z
        {| legs := q; legs_comm := qq |})) i j g x @
?path_legs i x =
?path_legs j (((diagram_sigma E) _f g) x) @
legs_comm {| legs := q; legs_comm := qq |} i j g x
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
forall i : G,
cocone_postcompose cocone_E'
  (cocone_extends Z {| legs := q; legs_comm := qq |})
  i == {| legs := q; legs_comm := qq |} i intros i x; reflexivity.
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
forall (i j : G) (g : G i j) (x : diagram_sigma E i),
legs_comm
  (cocone_postcompose cocone_E'
     (cocone_extends Z
        {| legs := q; legs_comm := qq |})) i j g x @
(fun i0 : G =>
 (fun x0 : diagram_sigma E i0 => 1)
 :
 cocone_postcompose cocone_E'
   (cocone_extends Z {| legs := q; legs_comm := qq |})
   i0 == {| legs := q; legs_comm := qq |} i0) i x =
(fun i0 : G =>
 (fun x0 : diagram_sigma E i0 => 1)
 :
 cocone_postcompose cocone_E'
   (cocone_extends Z {| legs := q; legs_comm := qq |})
   i0 == {| legs := q; legs_comm := qq |} i0) j
  (((diagram_sigma E) _f g) x) @
legs_comm {| legs := q; legs_comm := qq |} i j g x intros i j g [x y].
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
legs_comm
  (cocone_postcompose cocone_E'
     (cocone_extends Z
        {| legs := q; legs_comm := qq |})) i j g
  (x; y) @ 1 =
1 @
legs_comm {| legs := q; legs_comm := qq |} i j g
  (x; y)
      rewrite concat_1p, concat_p1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
legs_comm
  (cocone_postcompose cocone_E'
     (cocone_extends Z
        {| legs := q; legs_comm := qq |})) i j g
  (x; y) =
legs_comm {| legs := q; legs_comm := qq |} i j g
  (x; y)
      cbn; rewrite ap_path_sigma.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    Colimit_ind (fun w : Colimit D => E' w -> Z)
      (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
       q i (x; y0))
      (fun (i j : G) (g : G i j) (x : D i) =>
       path_forall
         (transport (fun w : Colimit D => E' w -> Z)
            (colimp i j g x)
            (fun y0 : E' (colim j ((D _f g) x)) =>
             q j ((D _f g) x; y0)))
         (fun y0 : E' (colim i x) => q i (x; y0))
         (fun y0 : E' (colim i x) =>
          transport_arrow_toconst (colimp i j g x)
            (fun y1 : E' (colim j ((D _f g) x)) =>
             q j ((D _f g) x; y1)) y0 @
          (ap11 1
             (path_sigma' (fun x0 : D j => E (j; x0))
                1 (transport_E'_V g x y0)) @
           qq i j g (x; y0)))) (colim j ((D _f g) x))
      y)
   (moveL_transport_V E' (colimp i j g x)
      ((E _f (g; 1)) y) y (transport_E' g x y)) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E' (colim j ((D _f g) x)) =>
     Colimit_ind (fun w : Colimit D => E' w -> Z)
       (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
        q i (x; y0))
       (fun (i j : G) (g : G i j) (x : D i) =>
        path_forall
          (transport (fun w : Colimit D => E' w -> Z)
             (colimp i j g x)
             (fun y0 : E' (colim j ((D _f g) x)) =>
              q j ((D _f g) x; y0)))
          (fun y0 : E' (colim i x) => q i (x; y0))
          (fun y0 : E' (colim i x) =>
           transport_arrow_toconst (colimp i j g x)
             (fun y1 : E' (colim j ((D _f g) x)) =>
              q j ((D _f g) x; y1)) y0 @
           (ap11 1
              (path_sigma' (fun x0 : D j => E (j; x0))
                 1 (transport_E'_V g x y0)) @
            qq i j g (x; y0)))) (colim j ((D _f g) x))
       y) y)^) @
ap10
  (apD
     (fun (x : Colimit D) (y : E' x) =>
      Colimit_ind (fun w : Colimit D => E' w -> Z)
        (fun (i : G) (x0 : D i) (y0 : E' (colim i x0))
         => q i (x0; y0))
        (fun (i j : G) (g : G i j) (x0 : D i) =>
         path_forall
           (transport (fun w : Colimit D => E' w -> Z)
              (colimp i j g x0)
              (fun y0 : E' (colim j ((D _f g) x0)) =>
               q j ((D _f g) x0; y0)))
           (fun y0 : E' (colim i x0) => q i (x0; y0))
           (fun y0 : E' (colim i x0) =>
            transport_arrow_toconst (colimp i j g x0)
              (fun y1 : E' (colim j ((D _f g) x0)) =>
               q j ((D _f g) x0; y1)) y0 @
            (ap11 1
               (path_sigma'
                  (fun x1 : D j => E (j; x1)) 1
                  (transport_E'_V g x0 y0)) @
             qq i j g (x0; y0)))) x y)
     (colimp i j g x)) y = qq i j g (x; y)
      simpl.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
(ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
   (moveL_transport_V E' (colimp i j g x)
      ((E _f (g; 1)) y) y (transport_E' g x y)) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
    y)^) @
ap10
  (apD
     (fun (x : Colimit D) (y : E' x) =>
      Colimit_ind (fun w : Colimit D => E' w -> Z)
        (fun (i : G) (x0 : D i) (y0 : E (i; x0)) =>
         q i (x0; y0))
        (fun (i j : G) (g : G i j) (x0 : D i) =>
         path_forall
           (transport (fun w : Colimit D => E' w -> Z)
              (colimp i j g x0)
              (fun y0 : E (j; (D _f g) x0) =>
               q j ((D _f g) x0; y0)))
           (fun y0 : E (i; x0) => q i (x0; y0))
           (fun y0 : E (i; x0) =>
            transport_arrow_toconst (colimp i j g x0)
              (fun y1 : E (j; (D _f g) x0) =>
               q j ((D _f g) x0; y1)) y0 @
            (ap11 1
               (path_sigma'
                  (fun x1 : D j => E (j; x1)) 1
                  (transport_E'_V g x0 y0)) @
             qq i j g (x0; y0)))) x y)
     (colimp i j g x)) y = qq i j g (x; y)
      rewrite Colimit_ind_beta_colimp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
(ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
   (moveL_transport_V E' (colimp i j g x)
      ((E _f (g; 1)) y) y (transport_E' g x y)) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
    y)^) @
ap10
  (path_forall
     (transport (fun w : Colimit D => E' w -> Z)
        (colimp i j g x)
        (fun y : E (j; (D _f g) x) =>
         q j ((D _f g) x; y)))
     (fun y : E (i; x) => q i (x; y))
     (fun y : E (i; x) =>
      transport_arrow_toconst (colimp i j g x)
        (fun y0 : E (j; (D _f g) x) =>
         q j ((D _f g) x; y0)) y @
      (ap11 1
         (path_sigma' (fun x : D j => E (j; x)) 1
            (transport_E'_V g x y)) @ qq i j g (x; y))))
  y = qq i j g (x; y)
      rewrite ap10_path_forall.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
(ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
   (moveL_transport_V E' (colimp i j g x)
      ((E _f (g; 1)) y) y (transport_E' g x y)) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
    y)^) @
(transport_arrow_toconst (colimp i j g x)
   (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
   y @
 (ap11 1
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x y)) @ qq i j g (x; y))) =
qq i j g (x; y)
      rewrite concat_pp_p, concat_V_pp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  (moveL_transport_V E' (colimp i j g x)
     ((E _f (g; 1)) y) y (transport_E' g x y)) @
(ap11 1
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x y)) @ qq i j g (x; y)) =
qq i j g (x; y)
      refine (_ @ concat_1p _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  (moveL_transport_V E' (colimp i j g x)
     ((E _f (g; 1)) y) y (transport_E' g x y)) @
(ap11 1
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x y)) @ qq i j g (x; y)) =
1 @ qq i j g (x; y)
      refine (concat_p_pp _ _ _ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
(ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
   (moveL_transport_V E' (colimp i j g x)
      ((E _f (g; 1)) y) y (transport_E' g x y)) @
 ap11 1
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x y))) @ qq i j g (x; y) =
1 @ qq i j g (x; y)
      refine (_ @@ 1).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  (moveL_transport_V E' (colimp i j g x)
     ((E _f (g; 1)) y) y (transport_E' g x y)) @
ap11 1
  (path_sigma' (fun x : D j => E (j; x)) 1
     (transport_E'_V g x y)) = 1
      match goal with |- ap _ ?X @ _ = _ => set (p := X) end.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  p @
ap11 1
  (path_sigma' (fun x : D j => E (j; x)) 1
     (transport_E'_V g x y)) = 1
      assert (r : transport_E'_V g x y = p^).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
transport_E'_V g x y = p^
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
r: transport_E'_V g x y = p^
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  p @
ap11 1
  (path_sigma' (fun x : D j => E (j; x)) 1
     (transport_E'_V g x y)) = 1
      {
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
transport_E'_V g x y = p^ subst p.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
transport_E'_V g x y =
(moveL_transport_V E' (colimp i j g x)
   ((E _f (g; 1)) y) y (transport_E' g x y))^
        exact (moveL_transport_V_V E' _ _ _ _)^. }
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
r: transport_E'_V g x y = p^
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  p @
ap11 1
  (path_sigma' (fun x : D j => E (j; x)) 1
     (transport_E'_V g x y)) = 1
      rewrite r; clear r.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
p:= moveL_transport_V E' (colimp i j g x)
  ((E _f (g; 1)) y) y (transport_E' g x y): (E _f (g; 1)) y = transport E' (colimp i j g x)^ y
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  p @
ap11 1 (path_sigma' (fun x : D j => E (j; x)) 1 p^) =
1
      destruct p.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
q: forall i : G, diagram_sigma E i -> Z
qq: forall (i j : G) (g : G i j),
(fun x : diagram_sigma E i =>
 q j (((diagram_sigma E) _f g) x)) == q i
i, j: G
g: G i j
x: D i
y: E (i; x)
ap (fun y : E (j; (D _f g) x) => q j ((D _f g) x; y))
  1 @
ap11 1 (path_sigma' (fun x : D j => E (j; x)) 1 1^) =
1
      reflexivity.
  Defined. (* 0.1s *)

  Local Definition cocone_issect Z
    : cocone_extends Z o cocone_postcompose cocone_E' == idmap.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_extends Z o cocone_postcompose cocone_E' ==
idmap
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_extends Z o cocone_postcompose cocone_E' ==
idmap
    intro f.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
cocone_extends Z (cocone_postcompose cocone_E' f) = f
    funext [x y].
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
x: Colimit D
y: E' x
cocone_extends Z (cocone_postcompose cocone_E' f)
  (x; y) = f (x; y)
    revert x y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
forall (x : Colimit D) (y : E' x),
cocone_extends Z (cocone_postcompose cocone_E' f)
  (x; y) = f (x; y)
    srapply Colimit_ind.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
forall (i : G) (x : D i),
(fun w : Colimit D =>
 forall y : E' w,
 cocone_extends Z (cocone_postcompose cocone_E' f)
   (w; y) = f (w; y)) (colim i x)
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
forall (i j : G) (g : G i j) (x : D i),
transport
  (fun w : Colimit D =>
   forall y : E' w,
   cocone_extends Z (cocone_postcompose cocone_E' f)
     (w; y) = f (w; y)) (colimp i j g x)
  (?q j ((D _f g) x)) = ?q i x
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
forall (i : G) (x : D i),
(fun w : Colimit D =>
 forall y : E' w,
 cocone_extends Z (cocone_postcompose cocone_E' f)
   (w; y) = f (w; y)) (colim i x) cbn; reflexivity.
    +
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
forall (i j : G) (g : G i j) (x : D i),
transport
  (fun w : Colimit D =>
   forall y : E' w,
   cocone_extends Z (cocone_postcompose cocone_E' f)
     (w; y) = f (w; y)) (colimp i j g x)
  (((fun (i0 : G) (x0 : D i0) (y : E' (colim i0 x0))
     => 1)
    :
    forall (i0 : G) (x0 : D i0),
    (fun w : Colimit D =>
     forall y : E' w,
     cocone_extends Z (cocone_postcompose cocone_E' f)
       (w; y) = f (w; y)) (colim i0 x0)) j
     ((D _f g) x)) =
((fun (i0 : G) (x0 : D i0) (y : E' (colim i0 x0)) => 1)
 :
 forall (i0 : G) (x0 : D i0),
 (fun w : Colimit D =>
  forall y : E' w,
  cocone_extends Z (cocone_postcompose cocone_E' f)
    (w; y) = f (w; y)) (colim i0 x0)) i x intros i j g x; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
transport
  (fun w : Colimit D =>
   forall y : E' w,
   cocone_extends Z (cocone_postcompose cocone_E' f)
     (w; y) = f (w; y)) (colimp i j g x)
  (fun y : E' (colim j ((D _f g) x)) => 1) =
(fun y : E' (colim i x) => 1)
      funext y.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport
  (fun w : Colimit D =>
   forall y : E' w,
   cocone_extends Z (cocone_postcompose cocone_E' f)
     (w; y) = f (w; y)) (colimp i j g x)
  (fun y : E' (colim j ((D _f g) x)) => 1) y = 1
      set (L := cocone_extends Z (cocone_postcompose cocone_E' f)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
transport
  (fun w : Colimit D =>
   forall y : E' w, L (w; y) = f (w; y))
  (colimp i j g x)
  (fun y : E' (colim j ((D _f g) x)) => 1) y = 1
      refine (transport_forall _ _ _ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
transport
  (fun y : E' (colim i x) =>
   L (colim i x; y) = f (colim i x; y))
  (transport_pV E' (colimp i j g x) y)
  (transportD E'
     (fun (x : Colimit D) (y : E' x) =>
      L (x; y) = f (x; y)) (colimp i j g x)
     (transport E' (colimp i j g x)^ y) 1) = 1
      transport_paths (transport_paths_FlFr (f:=fun y0 => L (_; y0))).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
ap (fun y0 : E' (colim i x) => L (colim i x; y0))
  (transport_pV E' (colimp i j g x) y) @ 1 =
transportD E'
  (fun (x : Colimit D) (y : E' x) =>
   L (x; y) = f (x; y)) (colimp i j g x)
  (transport E' (colimp i j g x)^ y) 1 @
ap (fun x0 : E' (colim i x) => f (colim i x; x0))
  (transport_pV E' (colimp i j g x) y)
      lhs napply concat_p1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
ap (fun y0 : E' (colim i x) => L (colim i x; y0))
  (transport_pV E' (colimp i j g x) y) =
transportD E'
  (fun (x : Colimit D) (y : E' x) =>
   L (x; y) = f (x; y)) (colimp i j g x)
  (transport E' (colimp i j g x)^ y) 1 @
ap (fun x0 : E' (colim i x) => f (colim i x; x0))
  (transport_pV E' (colimp i j g x) y)
      lhs_V napply concat_1p.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
1 @
ap (fun y0 : E' (colim i x) => L (colim i x; y0))
  (transport_pV E' (colimp i j g x) y) =
transportD E'
  (fun (x : Colimit D) (y : E' x) =>
   L (x; y) = f (x; y)) (colimp i j g x)
  (transport E' (colimp i j g x)^ y) 1 @
ap (fun x0 : E' (colim i x) => f (colim i x; x0))
  (transport_pV E' (colimp i j g x) y)
      refine (_^ @@ 1).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
transportD E'
  (fun (x : Colimit D) (y : E' x) =>
   L (x; y) = f (x; y)) (colimp i j g x)
  (transport E' (colimp i j g x)^ y) 1 = 1
      lhs rapply (transportD_is_transport E' (fun w => L w = f w)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
transport (fun w : {x : _ & E' x} => L w = f w)
  (path_sigma' E' (colimp i j g x) 1) 1 = 1
      transport_paths FlFr; apply equiv_p1_1q.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
ap L (path_sigma' E' (colimp i j g x) 1) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite ap_path_sigma.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    Colimit_ind (fun w : Colimit D => E' w -> Z)
      (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
       cocone_postcompose cocone_E' f i (x; y0))
      (fun (i j : G) (g : G i j) (x : D i) =>
       path_forall
         (transport (fun w : Colimit D => E' w -> Z)
            (colimp i j g x)
            (fun y0 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y0)))
         (fun y0 : E' (colim i x) =>
          cocone_postcompose cocone_E' f i (x; y0))
         (fun y0 : E' (colim i x) =>
          transport_arrow_toconst (colimp i j g x)
            (fun y1 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y1)) y0 @
          (ap11 1
             (path_sigma' (fun x0 : D j => E (j; x0))
                1 (transport_E'_V g x y0)) @
           legs_comm (cocone_postcompose cocone_E' f)
             i j g (x; y0)))) (colim j ((D _f g) x)) y)
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E' (colim j ((D _f g) x)) =>
     Colimit_ind (fun w : Colimit D => E' w -> Z)
       (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
        cocone_postcompose cocone_E' f i (x; y0))
       (fun (i j : G) (g : G i j) (x : D i) =>
        path_forall
          (transport (fun w : Colimit D => E' w -> Z)
             (colimp i j g x)
             (fun y0 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y0)))
          (fun y0 : E' (colim i x) =>
           cocone_postcompose cocone_E' f i (x; y0))
          (fun y0 : E' (colim i x) =>
           transport_arrow_toconst (colimp i j g x)
             (fun y1 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y1)) y0 @
           (ap11 1
              (path_sigma' (fun x0 : D j => E (j; x0))
                 1 (transport_E'_V g x y0)) @
            legs_comm (cocone_postcompose cocone_E' f)
              i j g (x; y0)))) (colim j ((D _f g) x))
       y)
    (transport E' (colimp i j g x)
       (transport E' (colimp i j g x)^ y)))^) @
ap10
  (apD
     (fun (x : Colimit D) (y : E' x) =>
      Colimit_ind (fun w : Colimit D => E' w -> Z)
        (fun (i : G) (x0 : D i) (y0 : E' (colim i x0))
         => cocone_postcompose cocone_E' f i (x0; y0))
        (fun (i j : G) (g : G i j) (x0 : D i) =>
         path_forall
           (transport (fun w : Colimit D => E' w -> Z)
              (colimp i j g x0)
              (fun y0 : E' (colim j ((D _f g) x0)) =>
               cocone_postcompose cocone_E' f j
                 ((D _f g) x0; y0)))
           (fun y0 : E' (colim i x0) =>
            cocone_postcompose cocone_E' f i (x0; y0))
           (fun y0 : E' (colim i x0) =>
            transport_arrow_toconst (colimp i j g x0)
              (fun y1 : E' (colim j ((D _f g) x0)) =>
               cocone_postcompose cocone_E' f j
                 ((D _f g) x0; y1)) y0 @
            (ap11 1
               (path_sigma'
                  (fun x1 : D j => E (j; x1)) 1
                  (transport_E'_V g x0 y0)) @
             legs_comm
               (cocone_postcompose cocone_E' f) i j g
               (x0; y0)))) x y) (colimp i j g x))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite Colimit_ind_beta_colimp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    Colimit_ind (fun w : Colimit D => E' w -> Z)
      (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
       cocone_postcompose cocone_E' f i (x; y0))
      (fun (i j : G) (g : G i j) (x : D i) =>
       path_forall
         (transport (fun w : Colimit D => E' w -> Z)
            (colimp i j g x)
            (fun y0 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y0)))
         (fun y0 : E' (colim i x) =>
          cocone_postcompose cocone_E' f i (x; y0))
         (fun y0 : E' (colim i x) =>
          transport_arrow_toconst (colimp i j g x)
            (fun y1 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y1)) y0 @
          (ap11 1
             (path_sigma' (fun x0 : D j => E (j; x0))
                1 (transport_E'_V g x y0)) @
           legs_comm (cocone_postcompose cocone_E' f)
             i j g (x; y0)))) (colim j ((D _f g) x)) y)
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E' (colim j ((D _f g) x)) =>
     Colimit_ind (fun w : Colimit D => E' w -> Z)
       (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
        cocone_postcompose cocone_E' f i (x; y0))
       (fun (i j : G) (g : G i j) (x : D i) =>
        path_forall
          (transport (fun w : Colimit D => E' w -> Z)
             (colimp i j g x)
             (fun y0 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y0)))
          (fun y0 : E' (colim i x) =>
           cocone_postcompose cocone_E' f i (x; y0))
          (fun y0 : E' (colim i x) =>
           transport_arrow_toconst (colimp i j g x)
             (fun y1 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y1)) y0 @
           (ap11 1
              (path_sigma' (fun x0 : D j => E (j; x0))
                 1 (transport_E'_V g x y0)) @
            legs_comm (cocone_postcompose cocone_E' f)
              i j g (x; y0)))) (colim j ((D _f g) x))
       y)
    (transport E' (colimp i j g x)
       (transport E' (colimp i j g x)^ y)))^) @
ap10
  (path_forall
     (transport (fun w : Colimit D => E' w -> Z)
        (colimp i j g x)
        (fun y : E' (colim j ((D _f g) x)) =>
         cocone_postcompose cocone_E' f j
           ((D _f g) x; y)))
     (fun y : E' (colim i x) =>
      cocone_postcompose cocone_E' f i (x; y))
     (fun y : E' (colim i x) =>
      transport_arrow_toconst (colimp i j g x)
        (fun y0 : E' (colim j ((D _f g) x)) =>
         cocone_postcompose cocone_E' f j
           ((D _f g) x; y0)) y @
      (ap11 1
         (path_sigma' (fun x : D j => E (j; x)) 1
            (transport_E'_V g x y)) @
       legs_comm (cocone_postcompose cocone_E' f) i j
         g (x; y))))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite ap10_path_forall.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    Colimit_ind (fun w : Colimit D => E' w -> Z)
      (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
       cocone_postcompose cocone_E' f i (x; y0))
      (fun (i j : G) (g : G i j) (x : D i) =>
       path_forall
         (transport (fun w : Colimit D => E' w -> Z)
            (colimp i j g x)
            (fun y0 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y0)))
         (fun y0 : E' (colim i x) =>
          cocone_postcompose cocone_E' f i (x; y0))
         (fun y0 : E' (colim i x) =>
          transport_arrow_toconst (colimp i j g x)
            (fun y1 : E' (colim j ((D _f g) x)) =>
             cocone_postcompose cocone_E' f j
               ((D _f g) x; y1)) y0 @
          (ap11 1
             (path_sigma' (fun x0 : D j => E (j; x0))
                1 (transport_E'_V g x y0)) @
           legs_comm (cocone_postcompose cocone_E' f)
             i j g (x; y0)))) (colim j ((D _f g) x)) y)
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E' (colim j ((D _f g) x)) =>
     Colimit_ind (fun w : Colimit D => E' w -> Z)
       (fun (i : G) (x : D i) (y0 : E' (colim i x)) =>
        cocone_postcompose cocone_E' f i (x; y0))
       (fun (i j : G) (g : G i j) (x : D i) =>
        path_forall
          (transport (fun w : Colimit D => E' w -> Z)
             (colimp i j g x)
             (fun y0 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y0)))
          (fun y0 : E' (colim i x) =>
           cocone_postcompose cocone_E' f i (x; y0))
          (fun y0 : E' (colim i x) =>
           transport_arrow_toconst (colimp i j g x)
             (fun y1 : E' (colim j ((D _f g) x)) =>
              cocone_postcompose cocone_E' f j
                ((D _f g) x; y1)) y0 @
           (ap11 1
              (path_sigma' (fun x0 : D j => E (j; x0))
                 1 (transport_E'_V g x y0)) @
            legs_comm (cocone_postcompose cocone_E' f)
              i j g (x; y0)))) (colim j ((D _f g) x))
       y)
    (transport E' (colimp i j g x)
       (transport E' (colimp i j g x)^ y)))^) @
(transport_arrow_toconst (colimp i j g x)
   (fun y : E' (colim j ((D _f g) x)) =>
    cocone_postcompose cocone_E' f j ((D _f g) x; y))
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)) @
 (ap11 1
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y)))) @
  legs_comm (cocone_postcompose cocone_E' f) i j g
    (x;
    transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      simpl.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
L:= cocone_extends Z (cocone_postcompose cocone_E' f): {x : _ & E' x} -> Z
(ap
   (fun y : E (j; (D _f g) x) =>
    f (colim j ((D _f g) x); y))
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E (j; (D _f g) x) =>
     f (colim j ((D _f g) x); y))
    (transport E' (colimp i j g x)
       (transport E' (colimp i j g x)^ y)))^) @
(transport_arrow_toconst (colimp i j g x)
   (fun y : E (j; (D _f g) x) =>
    f (colim j ((D _f g) x); y))
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)) @
 (ap11 1
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y)))) @
  ap f
    (path_sigma' E' (colimp i j g x)
       (transport_E' g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y)))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      clear L.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(ap
   (fun y : E (j; (D _f g) x) =>
    f (colim j ((D _f g) x); y))
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 (transport_arrow_toconst (colimp i j g x)
    (fun y : E (j; (D _f g) x) =>
     f (colim j ((D _f g) x); y))
    (transport E' (colimp i j g x)
       (transport E' (colimp i j g x)^ y)))^) @
(transport_arrow_toconst (colimp i j g x)
   (fun y : E (j; (D _f g) x) =>
    f (colim j ((D _f g) x); y))
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)) @
 (ap11 1
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y)))) @
  ap f
    (path_sigma' E' (colimp i j g x)
       (transport_E' g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y)))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite concat_pp_p, concat_V_pp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun y : E (j; (D _f g) x) =>
   f (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
(ap11 1
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y)))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite ap11_is_ap10_ap01.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun y : E (j; (D _f g) x) =>
   f (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
((ap10 1
    ((D _f g) x;
    transport E' (colimp i j g x)^
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))) @
  ap
    (fun x : {x : D j & E (j; x)} =>
     f (colim j x.1; x.2))
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y))))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun y : E (j; (D _f g) x) =>
   f (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
((1 @
  ap
    (fun x : {x : D j & E (j; x)} =>
     f (colim j x.1; x.2))
    (path_sigma' (fun x : D j => E (j; x)) 1
       (transport_E'_V g x
          (transport E' (colimp i j g x)
             (transport E' (colimp i j g x)^ y))))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite concat_1p.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun y : E (j; (D _f g) x) =>
   f (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
(ap
   (fun x : {x : D j & E (j; x)} =>
    f (colim j x.1; x.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y)))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite (ap_compose (fun y => (colim j ((D _f g) x); y)) f).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap f
  (ap
     (fun y : E' (colim j ((D _f g) x)) =>
      (colim j ((D _f g) x); y))
     (moveL_transport_V E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)
        (transport E' (colimp i j g x)
           (transport E' (colimp i j g x)^ y)) 1)) @
(ap
   (fun x : {x : D j & E (j; x)} =>
    f (colim j x.1; x.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y)))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite (ap_compose (fun x0 : exists x0 : D j, E (j; x0)
        => (colim j (pr1 x0); pr2 x0)) f).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap f
  (ap
     (fun y : E' (colim j ((D _f g) x)) =>
      (colim j ((D _f g) x); y))
     (moveL_transport_V E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)
        (transport E' (colimp i j g x)
           (transport E' (colimp i j g x)^ y)) 1)) @
(ap f
   (ap
      (fun x0 : {x0 : D j & E (j; x0)} =>
       (colim j x0.1; x0.2))
      (path_sigma' (fun x : D j => E (j; x)) 1
         (transport_E'_V g x
            (transport E' (colimp i j g x)
               (transport E' (colimp i j g x)^ y))))) @
 ap f
   (path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      rewrite <- ! (ap_pp f).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap f
  (ap
     (fun y : E' (colim j ((D _f g) x)) =>
      (colim j ((D _f g) x); y))
     (moveL_transport_V E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)
        (transport E' (colimp i j g x)
           (transport E' (colimp i j g x)^ y)) 1) @
   (ap
      (fun x0 : {x0 : D j & E (j; x0)} =>
       (colim j x0.1; x0.2))
      (path_sigma' (fun x : D j => E (j; x)) 1
         (transport_E'_V g x
            (transport E' (colimp i j g x)
               (transport E' (colimp i j g x)^ y)))) @
    path_sigma' E' (colimp i j g x)
      (transport_E' g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) =
ap f (path_sigma' E' (colimp i j g x) 1)
      apply (ap (ap f)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun y : E' (colim j ((D _f g) x)) =>
   (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
(ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y)))) @
 path_sigma' E' (colimp i j g x)
   (transport_E' g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))) =
path_sigma' E' (colimp i j g x) 1
      symmetry.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
ap
  (fun y : E' (colim j ((D _f g) x)) =>
   (colim j ((D _f g) x); y))
  (moveL_transport_V E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)) 1) @
(ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y)))) @
 path_sigma' E' (colimp i j g x)
   (transport_E' g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))))
      refine (_ @ concat_pp_p _ _ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    (colim j ((D _f g) x); y))
   (moveL_transport_V E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)) 1) @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      match goal with |- _ = (ap ?ff ?pp1 @ ?pp2) @ ?pp3
        => set (p1 := pp1) end.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1: transport E' (colimp i j g x)^ y =
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    (colim j ((D _f g) x); y)) p1 @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      assert (p1eq : p1 = ap (transport E' (colimp i j g x)^)
        (transport_pV E' (colimp i j g x) y)^).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1: transport E' (colimp i j g x)^ y =
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1: transport E' (colimp i j g x)^ y =
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1eq: p1 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    (colim j ((D _f g) x); y)) p1 @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      {
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1: transport E' (colimp i j g x)^ y =
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^ subst p1; clear.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
        etransitivity.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1 = ?Goal0
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
?Goal0 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
        1: srapply moveL_transport_V_1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(transport_Vp E' (colimp i j g x)
   (transport E' (colimp i j g x)^ y))^ =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
        etransitivity.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(transport_Vp E' (colimp i j g x)
   (transport E' (colimp i j g x)^ y))^ = ?Goal0
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
?Goal0 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
        1: napply inverse2; snapply transport_VpV.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(ap (transport E' (colimp i j g x)^)
   (transport_pV E' (colimp i j g x) y))^ =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
        symmetry; apply ap_V. }
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= moveL_transport_V E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) 1: transport E' (colimp i j g x)^ y =
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1eq: p1 =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)^
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    (colim j ((D _f g) x); y)) p1 @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      rewrite p1eq; clear p1eq p1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun y : E' (colim j ((D _f g) x)) =>
    (colim j ((D _f g) x); y))
   (ap (transport E' (colimp i j g x)^)
      (transport_pV E' (colimp i j g x) y)^) @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      rewrite <- ap_compose; cbn.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun x0 : E' (colim i x) =>
    (colim j ((D _f g) x);
    transport E' (colimp i j g x)^ x0))
   (transport_pV E' (colimp i j g x) y)^ @
 ap
   (fun x0 : {x0 : D j & E (j; x0)} =>
    (colim j x0.1; x0.2))
   (path_sigma' (fun x : D j => E (j; x)) 1
      (transport_E'_V g x
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      rewrite (ap_path_sigma (fun x => E (j; x))
        (fun x y => (colim j x; y))).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun x0 : E' (colim i x) =>
    (colim j ((D _f g) x);
    transport E' (colimp i j g x)^ x0))
   (transport_pV E' (colimp i j g x) y)^ @
 ((ap
     (fun y : E (j; (D _f g) x) =>
      (colim j ((D _f g) x); y))
     (moveL_transport_V (fun x : D j => E (j; x)) 1
        (transport E' (colimp i j g x)^
           (transport E' (colimp i j g x)
              (transport E' (colimp i j g x)^ y)))
        ((E _f (g; 1))
           (transport E' (colimp i j g x)
              (transport E' (colimp i j g x)^ y)))
        (transport_E'_V g x
           (transport E' (colimp i j g x)
              (transport E' (colimp i j g x)^ y)))) @
   (transport_arrow_toconst 1
      (fun y : E (j; (D _f g) x) =>
       (colim j ((D _f g) x); y))
      ((E _f (g; 1))
         (transport E' (colimp i j g x)
            (transport E' (colimp i j g x)^ y))))^) @
  ap10
    (apD
       (fun (x : D j) (y : E (j; x)) => (colim j x; y))
       1)
    ((E _f (g; 1))
       (transport E' (colimp i j g x)
          (transport E' (colimp i j g x)^ y))))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      cbn; rewrite !concat_p1, concat_pp_p, ap_V.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' (colimp i j g x) 1 =
(ap
   (fun x0 : E' (colim i x) =>
    (colim j ((D _f g) x);
    transport E' (colimp i j g x)^ x0))
   (transport_pV E' (colimp i j g x) y))^ @
(ap
   (fun y : E (j; (D _f g) x) =>
    (colim j ((D _f g) x); y))
   (transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))) @
 path_sigma' E' (colimp i j g x)
   (transport_E' g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))))
      apply moveL_Vp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) @
path_sigma' E' (colimp i j g x) 1 =
ap
  (fun y : E (j; (D _f g) x) =>
   (colim j ((D _f g) x); y))
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      match goal with |- ?pp1 @ _ = ?pp2 @ _
        => set (p1 := pp1);
          change pp2 with (path_sigma' E' 1
                            (transport_E'_V g x
                               (transport E' (colimp i j g x) (transport E' (colimp i j g x)^ y)))) end.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y): (fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
(fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0)) y
p1 @ path_sigma' E' (colimp i j g x) 1 =
path_sigma' E' 1
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      assert (p1eq : p1 = path_sigma' E' 1 (transport_Vp _ _ _)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y): (fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
(fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0)) y
p1 =
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y): (fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
(fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0)) y
p1eq: p1 =
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1 @ path_sigma' E' (colimp i j g x) 1 =
path_sigma' E' 1
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      {
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y): (fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
(fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0)) y
p1 =
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) subst p1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        rewrite <- ap_exist.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
ap (exist E' (colim j ((D _f g) x)))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        rewrite (ap_compose (transport E' (colimp i j g x)^)
          (fun v => (colim j ((D _f g) x); v))).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun v : E' (colim j ((D _f g) x)) =>
   (colim j ((D _f g) x); v))
  (ap (transport E' (colimp i j g x)^)
     (transport_pV E' (colimp i j g x) y)) =
ap (exist E' (colim j ((D _f g) x)))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        f_ap; set (p := colimp i j g x).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p:= colimp i j g x: colim j ((D _f g) x) = colim i x
ap (transport E' p^) (transport_pV E' p y) =
transport_Vp E' p (transport E' p^ y)
        clear; symmetry.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p:= colimp i j g x: colim j ((D _f g) x) = colim i x
transport_Vp E' p (transport E' p^ y) =
ap (transport E' p^) (transport_pV E' p y)
        apply transport_VpV. }
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
p1:= ap
  (fun x0 : E' (colim i x) =>
   (colim j ((D _f g) x);
   transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y): (fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
(fun x0 : E' (colim i x) =>
 (colim j ((D _f g) x);
 transport E' (colimp i j g x)^ x0)) y
p1eq: p1 =
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
p1 @ path_sigma' E' (colimp i j g x) 1 =
path_sigma' E' 1
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      rewrite p1eq; clear p1eq p1.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
path_sigma' E' 1
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) @
path_sigma' E' (colimp i j g x) 1 =
path_sigma' E' 1
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
path_sigma' E' (colimp i j g x)
  (transport_E' g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y)))
      rewrite <- !path_sigma_pp_pp'; f_ap.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(transport_pp E' 1 (colimp i j g x)
   (transport E' (colimp i j g x)^
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))) @
 ap (transport E' (colimp i j g x))
   (transport_Vp E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y))) @ 1 =
(transport_pp E' 1 (colimp i j g x)
   (transport E' (colimp i j g x)^
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))) @
 ap (transport E' (colimp i j g x))
   (transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))) @
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
      rewrite concat_p1, concat_pp_p.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport_pp E' 1 (colimp i j g x)
  (transport E' (colimp i j g x)^
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
ap (transport E' (colimp i j g x))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
transport_pp E' 1 (colimp i j g x)
  (transport E' (colimp i j g x)^
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
(ap (transport E' (colimp i j g x))
   (transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))) @
 transport_E' g x
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)))
      refine (1 @@ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
ap (transport E' (colimp i j g x))
  (transport_E'_V g x
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) @
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
      apply moveL_Mp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(ap (transport E' (colimp i j g x))
   (transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y))))^ @
ap (transport E' (colimp i j g x))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
      rewrite <- ap_V, <- ap_pp.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))^ @
   transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
      srefine (_ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport E' (colimp i j g x)
  ((E _f (g; 1))
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) =
transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y)
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))^ @
   transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) = ?y
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
?y =
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
      -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport E' (colimp i j g x)
  ((E _f (g; 1))
     (transport E' (colimp i j g x)
        (transport E' (colimp i j g x)^ y))) =
transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y) refine (ap (transport E' (colimp i j g x)) _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(E _f (g; 1))
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
transport E' (colimp i j g x)^ y
        refine ((transport_E'_V _ _ _)^ @ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport E' (colimp i j g x)^
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
transport E' (colimp i j g x)^ y
        exact (ap _ (transport_pV _ _ _)).
      -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))^ @
   transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) =
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))^ @
   ap (transport E' (colimp i j g x)^)
     (transport_pV E' (colimp i j g x) y)) f_ap.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
(transport_E'_V g x
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)))^ @
transport_Vp E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y) =
(transport_E'_V g x
   (transport E' (colimp i j g x)
      (transport E' (colimp i j g x)^ y)))^ @
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)
        refine (1 @@ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport_Vp E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y) =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)
        apply transport_VpV.
      -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x
      (transport E' (colimp i j g x)
         (transport E' (colimp i j g x)^ y)))^ @
   ap (transport E' (colimp i j g x)^)
     (transport_pV E' (colimp i j g x) y)) =
transport_E' g x
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y)) set (e := transport E' (colimp i j g x)
          (transport E' (colimp i j g x)^ y)).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
e:= transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y): E' (colim i x)
ap (transport E' (colimp i j g x))
  ((transport_E'_V g x e)^ @
   ap (transport E' (colimp i j g x)^)
     (transport_pV E' (colimp i j g x) y)) =
transport_E' g x e
        rewrite ap_pp, <- ap_compose.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
e:= transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y): E' (colim i x)
ap (transport E' (colimp i j g x))
  (transport_E'_V g x e)^ @
ap
  (fun x0 : E' (colim i x) =>
   transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
transport_E' g x e
        refine (_ @ (transport_E'_V_E' _ _ _)^).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
e:= transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y): E' (colim i x)
ap (transport E' (colimp i j g x))
  (transport_E'_V g x e)^ @
ap
  (fun x0 : E' (colim i x) =>
   transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
ap (transport E' (colimp i j g x))
  (transport_E'_V g x e)^ @
transport_pV E' (colimp i j g x) e
        refine (1 @@ _).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
e:= transport E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y): E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
transport_pV E' (colimp i j g x) e
        subst e.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
transport_pV E' (colimp i j g x)
  (transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        refine (_ @ (transport_pVp _ _ _)^).
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap
  (fun x0 : E' (colim i x) =>
   transport E' (colimp i j g x)
     (transport E' (colimp i j g x)^ x0))
  (transport_pV E' (colimp i j g x) y) =
ap (transport E' (colimp i j g x))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        rewrite ap_compose.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
ap (transport E' (colimp i j g x))
  (ap (transport E' (colimp i j g x)^)
     (transport_pV E' (colimp i j g x) y)) =
ap (transport E' (colimp i j g x))
  (transport_Vp E' (colimp i j g x)
     (transport E' (colimp i j g x)^ y))
        f_ap; symmetry.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
f: {x : _ & E' x} -> Z
i, j: G
g: G i j
x: D i
y: E' (colim i x)
transport_Vp E' (colimp i j g x)
  (transport E' (colimp i j g x)^ y) =
ap (transport E' (colimp i j g x)^)
  (transport_pV E' (colimp i j g x) y)
        apply transport_VpV.
  Defined. (* TODO: a little slow, 0.40s *)

  #[export] Instance unicocone_cocone_E' : UniversalCocone cocone_E'.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
UniversalCocone cocone_E'
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
UniversalCocone cocone_E'
    srapply Build_UniversalCocone.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
forall Y : Type,
IsEquiv (cocone_postcompose cocone_E')
    intro Z; srapply isequiv_adjointify.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
Cocone (diagram_sigma E) Z -> {x : _ & E' x} -> Z
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_postcompose cocone_E' o ?g == idmap
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
?g o cocone_postcompose cocone_E' == idmap
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
Cocone (diagram_sigma E) Z -> {x : _ & E' x} -> Z exact (cocone_extends Z).
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_postcompose cocone_E' o cocone_extends Z ==
idmap exact (cocone_isretr Z).
    -
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Z: Type
cocone_extends Z o cocone_postcompose cocone_E' ==
idmap exact (cocone_issect Z).
  Defined.

  (** The flattening lemma follows by colimit uniqueness. *)

  Definition flattening_lemma : Colimit (diagram_sigma E) <~> sig E'.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Colimit (diagram_sigma E) <~> {x : _ & E' x}
  Proof.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Colimit (diagram_sigma E) <~> {x : _ & E' x}
    srapply colimit_unicity.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Graph
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
Diagram ?G
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
IsColimit ?D (Colimit (diagram_sigma E))
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
IsColimit ?D {x : _ & E' x}
    3: apply iscolimit_colimit.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
IsColimit (diagram_sigma E) {x : _ & E' x}
    rapply Build_IsColimit.
H: Univalence
G: Graph
D: Diagram G
E: DDiagram D
H0: Equifibered E
E_f:= fun (i j : G) (g : G i j) (x : D i) =>
E _f (g; 1): forall (i j : G) (g : G i j) (x : D i), E (i; x) -> E (j; (D _f g) x)
UniversalCocone ?Goal
    exact unicocone_cocone_E'.
  Defined.

End Flattening.
(* TODO: ending the section is a bit slow (0.2s).  But simply removing the Section (and changing "Let" to "Local Definition") causes the whole file to be much slower.  It should be possible to remove the section without making the whole file slower. *)