Require Import HoTT.Basics HoTT.Types HFiber.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Colimits.Pushout.
Require Import Colimits.SpanPushout.
Require Import Homotopy.Suspension.
Require Import Limits.Pullback.
Require Import Homotopy.Join.Core.
Require Import Truncations.

(** * The Generalized Blakers-Massey Theorem *)

(** This file follows the paper "A Generalized Blakers-Massey Theorem" (https://arxiv.org/abs/1703.09050) by Mathieu Anel, Georg Biedermann, Eric Finster, André Joyal, hereafter referred to as ABFJ. We also follow "A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory" by Favonia, Eric Finster, Dan Licata, and Peter LeFanu Lumsdaine, hereafter referred to as HFLL. *)

(** ** Path algebra helper lemma *)

(** Here is a strange-looking path algebra helper lemma that is easier to prove by lifting to a general case and doing a path-induction blast.  It says something about what happens when we transport from the center of a based path-space to some other point, assuming we know a particular way to "compute" the action of the type family in question. *)

Definition transport_singleton `{Univalence}
           {A : Type} {x : A} (B : forall (y : A), (x = y) -> Type)
           {y : A} (p : x = y) (u : B x idpath)
           (f : forall (q:x=x), B x q <~> B y (q @ p))
           (ev : ap10 (apD B p) p =
   transport_arrow_toconst p (B x) p @
   path_universe_uncurried
     (@equiv_transport _ (B y) ((p @ p^) @ p) p (concat_pV_p p p)
      oE (f (p @ p^))
      oE @equiv_transport _ (B x)
           (transport (fun y => x = y) p^ p)
           (p @ p^) (transport_paths_r p^ p)))
  : transport (fun yp:{y:A & x=y} => B yp.1 yp.2)
              (path_contr (A := {y:A & x=y}) (x;idpath) (y;p)) u
    = transport (B y) (concat_1p _) (f idpath u).
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
y: A
p: x = y
u: B x 1
f: forall q : x = x, B x q <~> B y (q @ p)
ev: ap10 (apD B p) p =
transport_arrow_toconst p (B x) p @
path_universe_uncurried
  (equiv_transport (B y) (concat_pV_p p p)
   oE f (p @ p^)
   oE equiv_transport (B x)
        (transport_paths_r p^ p))
transport (fun yp : {y : A & x = y} => B yp.1 yp.2)
  (path_contr (x; 1) (y; p)) u =
transport (B y) (concat_1p p) (f 1 u)
Proof.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
y: A
p: x = y
u: B x 1
f: forall q : x = x, B x q <~> B y (q @ p)
ev: ap10 (apD B p) p =
transport_arrow_toconst p (B x) p @
path_universe_uncurried
  (equiv_transport (B y) (concat_pV_p p p)
   oE f (p @ p^)
   oE equiv_transport (B x)
        (transport_paths_r p^ p))
transport (fun yp : {y : A & x = y} => B yp.1 yp.2)
  (path_contr (x; 1) (y; p)) u =
transport (B y) (concat_1p p) (f 1 u)
  destruct p; cbn in *.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: 1 =
1 @
path_universe_uncurried
  (equiv_transport (B x) 1 oE f 1%path
   oE equiv_transport (B x) 1)
u = transport (B x) 1 (f 1 u)
  apply (fun e => e @ concat_1p _) in ev.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: 1 =
path_universe_uncurried
  (equiv_transport (B x) 1 oE f 1%path
   oE equiv_transport (B x) 1)
u = transport (B x) 1 (f 1 u)
  apply moveR_equiv_V in ev.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: ((equiv_path (B x 1) (B x 1))^-1 o idmap)^-1 1 =
equiv_transport (B x) 1 oE f 1%path
oE equiv_transport (B x) 1
u = transport (B x) 1 (f 1 u)
  apply (ap equiv_fun) in ev.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: ((equiv_path (B x 1) (B x 1))^-1 o idmap)^-1 1 =
equiv_transport (B x) 1 oE f 1%path
oE equiv_transport (B x) 1
u = transport (B x) 1 (f 1 u)
  apply ap10 in ev.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: ((equiv_path (B x 1) (B x 1))^-1 o idmap)^-1 1 ==
equiv_transport (B x) 1 oE f 1%path
oE equiv_transport (B x) 1
u = transport (B x) 1 (f 1 u)
  specialize (ev u).
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: ((equiv_path (B x 1) (B x 1))^-1 o idmap)^-1 1 u =
(equiv_transport (B x) 1 oE f 1%path
 oE equiv_transport (B x) 1) u
u = transport (B x) 1 (f 1 u)
  cbn in ev.
H: Univalence
A: Type
x: A
B: forall y : A, x = y -> Type
u: B x 1
f: forall q : x = x, B x q <~> B x (q @ 1)
ev: u = transport (B x) 1 (f 1 u)
u = transport (B x) 1 (f 1 u)
  exact ev.
Defined.

(** ** Setup *)

Section GBM.
    Context {X Y : Type} (Q : X -> Y -> Type).

    (** Here's the hypothesis of ABFJ's generalized Blakers-Massey.  It works for any reflective subuniverse, not only modalities! *)
    Context (O : ReflectiveSubuniverse).
    Context
      (isconnected_cogap :
         forall (x1 x3 : X) (y2 y4 : Y)
                (q12 : Q x1 y2) (q32 : Q x3 y2) (q34 : Q x3 y4),
           IsConnected O (Join ((x1;q12) = (x3;q32) :> {x:X & Q x y2})
                               ((y2;q32) = (y4;q34) :> {y:Y & Q x3 y}))).

    Let P := SPushout Q.
    Local Notation left := (spushl Q).
    Local Notation right := (spushr Q).
    Local Notation glue := (spglue Q).

    (** Here's a lemma that's a sort of "singleton contractibility" equivalence, but expressed in a particularly strange way.  As we'll see, this form of the lemma comes up naturally *twice* in the proof, and proving it once here to use in both places is crucial so that the two uses can be identified later on. *)

    Local Definition frobnicate {x0 x1 : X} (r : left x0 = left x1)
          (s : x0 = x1) (y : Y) (q1 : Q x1 y)
      : {q0 : Q x0 y &
              {w : transport (fun x => Q x y) s q0 = q1 &
                   glue q0 @ (glue q1)^ = r } }
          <~> ap left s = r.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
{q0 : Q x0 y &
{_ : transport (fun x : X => Q x y) s q0 = q1 &
glue q0 @ (glue q1)^ = r}} <~> ap left s = r
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
{q0 : Q x0 y &
{_ : transport (fun x : X => Q x y) s q0 = q1 &
glue q0 @ (glue q1)^ = r}} <~> ap left s = r
      refine (_ oE equiv_sigma_assoc' _ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
{ap
: {a : Q x0 y &
  transport (fun x : X => Q x y) s a = q1} &
glue ap.1 @ (glue q1)^ = r} <~> ap left s = r
      refine (_ oE equiv_functor_sigma'
                (Q := fun qt => glue qt.1 @ (glue q1)^ = r)
                (equiv_functor_sigma_id
                   (fun q0 : Q x0 y =>
                      equiv_moveL_transport_V
                        (fun x => Q x y) s q0 q1))
                (fun qt => equiv_idmap)).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
{qt
: {q0 : Q x0 y &
  q0 = transport (fun x : X => Q x y) s^ q1} &
glue qt.1 @ (glue q1)^ = r} <~> ap left s = r
      refine (_ oE equiv_contr_sigma _); cbn.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
glue (transport (fun x : X => Q x y) s^ q1) @
(glue q1)^ = r <~> ap left s = r
      rewrite (ap_transport s^ (fun x q => glue q) q1).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
transport (fun x : X => left x = right y) s^ (glue q1) @
(glue q1)^ = r <~> ap left s = r
      rewrite (transport_paths_FlFr s^ (glue q1)).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
(((ap left s^)^ @ glue q1) @
 ap (fun _ : X => right y) s^) @ (glue q1)^ = r <~>
ap left s = r
      rewrite ap_V, inv_V, ap_const, concat_p1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y: Y
q1: Q x1 y
(ap left s @ glue q1) @ (glue q1)^ = r <~>
ap left s = r
      exact (equiv_concat_l (concat_pp_V _ _)^ _).
      (** Although we proved this lemma with [rewrite], we make it transparent, not so that *we* can reason about it, but so that Coq can evaluate it. *)
    Defined.
    (* But except in one place, we don't want it to try (otherwise things get really slow). *)
    Opaque frobnicate.

    (** ** Codes *)

    (** *** Right-hand codes *)

    (** The right-hand codes family is easy. *)
    Definition coderight {x0 : X} {y : Y} (r : left x0 = right y) : Type
      := O (hfiber glue r).

    (** *** Left-hand codes *)

    (** We enhance the HFLL and ABFJ theorems by defining a version of code-left that doesn't depend on one map being surjective. *)

    Section CodeLeft.
      Context {x0 x1 : X} (r : left x0 = left x1).

      (** The left codes are themselves a pushout, of what is morally also a dependent span, but we formulate it as an ordinary pushout of projections between iterated Sigma-types, most of which we express as records for performance reasons.  The span is [codeleft1] <- [codeleft0] -> [codeleft2]. *)

      Definition codeleft1 : Type
        := { s : x0 = x1 &
          (* v : *) ap left s = r}.

      Record codeleft2
        := { codeleft2_y0  : Y ;
             codeleft2_q00 : Q x0 codeleft2_y0 ;
             codeleft2_q10 : Q x1 codeleft2_y0 ;
             codeleft2_u   : glue codeleft2_q00 @ (glue codeleft2_q10)^ = r }.

      Record codeleft0
        := { codeleft0_s   : x0 = x1 ;
             codeleft0_y0  : Y ;
             codeleft0_v   : ap left codeleft0_s = r ;
             codeleft0_q00 : Q x0 codeleft0_y0 ;
             codeleft0_q10 : Q x1 codeleft0_y0 ;
             codeleft0_w   : transport (fun x => Q x codeleft0_y0) codeleft0_s codeleft0_q00
                             = codeleft0_q10 ;
             codeleft0_u   : glue codeleft0_q00 @ (glue codeleft0_q10)^ = r ;
                   (** Note the first use of frobnicate here. *)
             codeleft0_d   : frobnicate r codeleft0_s codeleft0_y0 codeleft0_q10
                                        (codeleft0_q00 ; codeleft0_w ; codeleft0_u) = codeleft0_v }.

      Definition codeleft01 : codeleft0 -> codeleft1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
codeleft0 -> codeleft1
      Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
codeleft0 -> codeleft1
        intros [s y0 v q00 q10 w u d].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y0: Y
v: ap left s = r
q00: Q x0 y0
q10: Q x1 y0
w: transport (fun x : X => Q x y0) s q00 = q10
u: glue q00 @ (glue q10)^ = r
d: frobnicate r s y0 q10 (q00; w; u) = v
codeleft1
        exact (s;v).
      Defined.

      Definition codeleft02 : codeleft0 -> codeleft2.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
codeleft0 -> codeleft2
      Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
codeleft0 -> codeleft2
        intros [s y0 v q00 q10 w u d].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
s: x0 = x1
y0: Y
v: ap left s = r
q00: Q x0 y0
q10: Q x1 y0
w: transport (fun x : X => Q x y0) s q00 = q10
u: glue q00 @ (glue q10)^ = r
d: frobnicate r s y0 q10 (q00; w; u) = v
codeleft2
        exact (Build_codeleft2 y0 q00 q10 u).
      Defined.

      Definition codeleft : Type
        := O (Pushout codeleft01 codeleft02).

      (** *** Codes for glue *)

      Section CodeGlue.
        Context {y1 : Y} (q11 : Q x1 y1).

        (** We prove that codes respect glue as a chain of equivalences between types built from pushouts and double-pushouts.  The first step is to add the data of our hypothesized-to-be-connected type inside [codeleft2]. *)

        Definition codeleft2plus :=
          {yqqu : codeleft2 &
                  Join ((x0; codeleft2_q00 yqqu) = (x1; codeleft2_q10 yqqu)
                                           :> {x:X & Q x (codeleft2_y0 yqqu)})
                       ((codeleft2_y0 yqqu; codeleft2_q10 yqqu) = (y1; q11)
                                           :> {y:Y & Q x1 y})}.

        (** Since this connected type is itself a join, hence a pushout, the second step is to distribute this and re-express the whole thing as another pushout of iterated Sigma-types (again mostly expressed as records for performance reasons). *)

        Record Ocodeleft2b
        := { Ocodeleft2b_s   : x0 = x1 ;
             Ocodeleft2b_y0  : Y ;
             Ocodeleft2b_q00 : Q x0 Ocodeleft2b_y0 ;
             Ocodeleft2b_q10 : Q x1 Ocodeleft2b_y0 ;
             Ocodeleft2b_w   : transport (fun x => Q x Ocodeleft2b_y0) Ocodeleft2b_s Ocodeleft2b_q00
                               = Ocodeleft2b_q10 ;
             Ocodeleft2b_u   : glue Ocodeleft2b_q00 @ (glue Ocodeleft2b_q10)^ = r }.

        Definition Ocodeleft2c
          := { q01 : Q x0 y1 &
            (* u: *) glue q01 @ (glue q11)^ = r }.

        Record Ocodeleft2a
        := { Ocodeleft2a_s   : x0 = x1 ;
             Ocodeleft2a_q01 : Q x0 y1 ;
             Ocodeleft2a_w   : transport (fun x => Q x y1) Ocodeleft2a_s Ocodeleft2a_q01 = q11 ;
             Ocodeleft2a_u   : glue Ocodeleft2a_q01 @ (glue q11)^ = r }.

        Definition Ocodeleft2ab : Ocodeleft2a -> Ocodeleft2b.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a -> Ocodeleft2b
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a -> Ocodeleft2b
          intros [s q01 w u].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
s: x0 = x1
q01: Q x0 y1
w: transport (fun x : X => Q x y1) s q01 = q11
u: glue q01 @ (glue q11)^ = r
Ocodeleft2b
          exact (Build_Ocodeleft2b s y1 q01 q11 w u).
        Defined.

        Definition Ocodeleft2ac : Ocodeleft2a -> Ocodeleft2c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a -> Ocodeleft2c
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a -> Ocodeleft2c
          intros [s q01 w u].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
s: x0 = x1
q01: Q x0 y1
w: transport (fun x : X => Q x y1) s q01 = q11
u: glue q01 @ (glue q11)^ = r
Ocodeleft2c
          exact (q01;u).
        Defined.

        (** This proof is basically just rearranging Sigma-types/records and paths in Sigma-types and contracting based path spaces. *)
        Definition equiv_Ocodeleft2plus
          : Pushout Ocodeleft2ab Ocodeleft2ac <~> codeleft2plus.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Pushout Ocodeleft2ab Ocodeleft2ac <~> codeleft2plus
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Pushout Ocodeleft2ab Ocodeleft2ac <~> codeleft2plus
          refine ((equiv_sigma_pushout _ _ _ _ _)^-1 oE _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Pushout Ocodeleft2ab Ocodeleft2ac <~>
Pushout
  (functor_sigma idmap (fun x : codeleft2 => fst))
  (functor_sigma idmap (fun x : codeleft2 => snd))
          srefine (equiv_pushout _ _ _ _ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~>
{x : codeleft2 &
((x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)) *
((codeleft2_y0 x; codeleft2_q10 x) = (y1; q11))}
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2b <~>
{x : codeleft2 &
(x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)}
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2c <~>
{x : codeleft2 &
(codeleft2_y0 x; codeleft2_q10 x) = (y1; q11)}
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
?eB o Ocodeleft2ab ==
functor_sigma idmap (fun x : codeleft2 => fst) o ?eA
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
?eC o Ocodeleft2ac ==
functor_sigma idmap (fun x : codeleft2 => snd) o ?eA
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~>
{x : codeleft2 &
((x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)) *
((codeleft2_y0 x; codeleft2_q10 x) = (y1; q11))} srefine (equiv_functor_sigma_id _ oE _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft2 -> Type
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
forall a : codeleft2,
?P a <~>
(fun x : codeleft2 =>
 ((x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)) *
 ((codeleft2_y0 x; codeleft2_q10 x) = (y1; q11))) a
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~> {x : _ & ?P x}
            2:intro; refine (equiv_functor_prod' _ _); apply equiv_path_sigma.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~>
{a : codeleft2 &
{p : (x0; codeleft2_q00 a).1 = (x1; codeleft2_q10 a).1
&
transport (fun x : X => Q x (codeleft2_y0 a)) p
  (x0; codeleft2_q00 a).2 = (x1; codeleft2_q10 a).2} *
{p : (codeleft2_y0 a; codeleft2_q10 a).1 = (y1; q11).1
&
transport (fun y : Y => Q x1 y) p
  (codeleft2_y0 a; codeleft2_q10 a).2 = (y1; q11).2}}
            make_equiv_contr_basedpaths.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2b <~>
{x : codeleft2 &
(x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)} srefine (equiv_functor_sigma_id _ oE _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft2 -> Type
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
forall a : codeleft2,
?P a <~>
(fun x : codeleft2 =>
 (x0; codeleft2_q00 x) = (x1; codeleft2_q10 x)) a
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2b <~> {x : _ & ?P x}
            2:intro; apply equiv_path_sigma.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2b <~>
{a : codeleft2 &
{p : (x0; codeleft2_q00 a).1 = (x1; codeleft2_q10 a).1
&
transport (fun x : X => Q x (codeleft2_y0 a)) p
  (x0; codeleft2_q00 a).2 = (x1; codeleft2_q10 a).2}}
            make_equiv.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2c <~>
{x : codeleft2 &
(codeleft2_y0 x; codeleft2_q10 x) = (y1; q11)} srefine (equiv_functor_sigma_id _ oE _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft2 -> Type
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
forall a : codeleft2,
?P a <~>
(fun x : codeleft2 =>
 (codeleft2_y0 x; codeleft2_q10 x) = (y1; q11)) a
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2c <~> {x : _ & ?P x}
            2:intro; apply equiv_path_sigma.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2c <~>
{a : codeleft2 &
{p : (codeleft2_y0 a; codeleft2_q10 a).1 = (y1; q11).1
&
transport (fun y : Y => Q x1 y) p
  (codeleft2_y0 a; codeleft2_q10 a).2 = (y1; q11).2}}
            make_equiv_contr_basedpaths.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
equiv_functor_sigma_id
  (fun a : codeleft2 =>
   equiv_path_sigma
     (fun x : X => Q x (codeleft2_y0 a))
     (x0; codeleft2_q00 a) (x1; codeleft2_q10 a))
oE equiv_adjointify
     (fun H : Ocodeleft2b =>
      (fun (H0 : x0 = x1) (H1 : Y) (H2 : Q x0 H1)
         (H3 : Q x1 H1)
         (H4 : transport (fun x : X => Q x H1) H0 H2 =
               H3) (H5 : glue H2 @ (glue H3)^ = r) =>
       ({|
          codeleft2_y0 := H1 : Y;
          codeleft2_q00 := H2 : Q x0 (H1 : Y);
          codeleft2_q10 := H3 : Q x1 (H1 : Y);
          codeleft2_u :=
            H5
            :
            glue (H2 : Q x0 (H1 : Y)) @
            (glue (H3 : Q x1 (H1 : Y)))^ = r
        |}
        :
        codeleft2;
       (H0 : x0 = x1;
       H4
       :
       transport
         (fun x : X =>
          Q x
            (codeleft2_y0
               {|
                 codeleft2_y0 := H1;
                 codeleft2_q00 := H2;
                 codeleft2_q10 := H3;
                 codeleft2_u := H5
               |})) (H0 : x0 = x1)
         (codeleft2_q00
            {|
              codeleft2_y0 := H1;
              codeleft2_q00 := H2;
              codeleft2_q10 := H3;
              codeleft2_u := H5
            |}) =
       codeleft2_q10
         {|
           codeleft2_y0 := H1;
           codeleft2_q00 := H2;
           codeleft2_q10 := H3;
           codeleft2_u := H5
         |})
       :
       {p : x0 = x1 &
       transport
         (fun x : X =>
          Q x
            (codeleft2_y0
               ({|
                  codeleft2_y0 := H1 : Y;
                  codeleft2_q00 := H2 : Q x0 ...;
                  codeleft2_q10 := H3 : Q x1 ...;
                  codeleft2_u := H5 : ... = r
                |}
                :
                codeleft2))) p
         (codeleft2_q00
            ({|
               codeleft2_y0 := H1 : Y;
               codeleft2_q00 := H2 : Q x0 (H1 : Y);
               codeleft2_q10 := H3 : Q x1 (H1 : Y);
               codeleft2_u :=
                 H5 : glue (...) @ (glue ...)^ = r
             |}
             :
             codeleft2)) =
       codeleft2_q10
         ({|
            codeleft2_y0 := H1 : Y;
            codeleft2_q00 := H2 : Q x0 (H1 : Y);
            codeleft2_q10 := H3 : Q x1 (H1 : Y);
            codeleft2_u :=
              H5
              :
              glue (H2 : Q x0 ...) @
              (glue (H3 : ...))^ = r
          |}
          :
          codeleft2)})
       :
       {a : codeleft2 &
       {p
       : (x0; codeleft2_q00 a).1 =
         (x1; codeleft2_q10 a).1 &
       transport (fun x : X => Q x (codeleft2_y0 a)) p
         (x0; codeleft2_q00 a).2 =
       (x1; codeleft2_q10 a).2}}) (Ocodeleft2b_s H)
        (Ocodeleft2b_y0 H) (Ocodeleft2b_q00 H)
        (Ocodeleft2b_q10 H) (Ocodeleft2b_w H)
        (Ocodeleft2b_u H))
     (fun
        H : {a : codeleft2 &
            {p
            : (x0; codeleft2_q00 a).1 =
              (x1; codeleft2_q10 a).1 &
            transport
              (fun x : X => Q x (codeleft2_y0 a)) p
              (x0; codeleft2_q00 a).2 =
            (x1; codeleft2_q10 a).2}} =>
      (fun H0 : codeleft2 =>
       (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
          (H4 : glue H2 @ (glue H3)^ = r)
          (H5 : {p : x0 = x1 &
                transport
                  (fun x : X =>
                   Q x
                     (codeleft2_y0
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |})) p
                  (codeleft2_q00
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |}) =
                codeleft2_q10
                  {|
                    codeleft2_y0 := H1;
                    codeleft2_q00 := H2;
                    codeleft2_q10 := H3;
                    codeleft2_u := H4
                  |}}) =>
        (fun (H6 : x0 = x1)
           (H7 : transport (fun x : X => Q x H1) H6 H2 =
                 H3) =>
         {|
           Ocodeleft2b_s := H6 : x0 = x1;
           Ocodeleft2b_y0 := H1 : Y;
           Ocodeleft2b_q00 := H2 : Q x0 (H1 : Y);
           Ocodeleft2b_q10 := H3 : Q x1 (H1 : Y);
           Ocodeleft2b_w :=
             H7
             :
             transport (fun x : X => Q x (H1 : Y))
               (H6 : x0 = x1) (H2 : Q x0 (H1 : Y)) =
             (H3 : Q x1 (H1 : Y));
           Ocodeleft2b_u :=
             H4
             :
             glue (H2 : Q x0 (...)) @
             (glue (H3 : Q x1 ...))^ = r
         |}
         :
         Ocodeleft2b) H5.1 H5.2) (codeleft2_y0 H0)
         (codeleft2_q00 H0) (codeleft2_q10 H0)
         (codeleft2_u H0)) H.1 H.2)
     ((fun
         H : {a : codeleft2 &
             {p
             : (x0; codeleft2_q00 a).1 =
               (x1; codeleft2_q10 a).1 &
             transport
               (fun x : X => Q x (codeleft2_y0 a)) p
               (x0; codeleft2_q00 a).2 =
             (x1; codeleft2_q10 a).2}} =>
       (fun H0 : codeleft2 =>
        (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
           (H4 : glue H2 @ (glue H3)^ = r)
           (H5 : {p : x0 = x1 &
                 transport
                   (fun x : X =>
                    Q x
                      (codeleft2_y0
                         {|
                           codeleft2_y0 := H1;
                           codeleft2_q00 := H2;
                           codeleft2_q10 := H3;
                           codeleft2_u := H4
                         |})) p
                   (codeleft2_q00
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}) =
                 codeleft2_q10
                   {|
                     codeleft2_y0 := H1;
                     codeleft2_q00 := H2;
                     codeleft2_q10 := H3;
                     codeleft2_u := H4
                   |}}) =>
         (fun (H6 : x0 = x1)
            (H7 : transport (fun x : X => Q x H1) H6
                    H2 = H3) => 1%path) H5.1 H5.2)
          (codeleft2_y0 H0) (codeleft2_q00 H0)
          (codeleft2_q10 H0) (codeleft2_u H0)) H.1 H.2)
      :
      (fun H : Ocodeleft2b =>
       (fun (H0 : x0 = x1) (H1 : Y) (H2 : Q x0 H1)
          (H3 : Q x1 H1)
          (H4 : transport (fun x : X => Q x H1) H0 H2 =
                H3) (H5 : glue H2 @ (glue H3)^ = r) =>
        ({|
           codeleft2_y0 := H1 : Y;
           codeleft2_q00 := H2 : Q x0 (H1 : Y);
           codeleft2_q10 := H3 : Q x1 (H1 : Y);
           codeleft2_u :=
             H5
             :
             glue (H2 : Q x0 (...)) @
             (glue (H3 : Q x1 ...))^ = r
         |}
         :
         codeleft2;
        (H0 : x0 = x1;
        H4
        :
        transport
          (fun x : X =>
           Q x (codeleft2_y0 {| ...; ...; ...; ... |}))
          (H0 : x0 = x1)
          (codeleft2_q00
             {|
               codeleft2_y0 := H1;
               codeleft2_q00 := H2;
               codeleft2_q10 := H3;
               codeleft2_u := H5
             |}) =
        codeleft2_q10
          {|
            codeleft2_y0 := H1;
            codeleft2_q00 := H2;
            codeleft2_q10 := H3;
            codeleft2_u := H5
          |})
        :
        {p : x0 = x1 &
        transport
          (fun x : X =>
           Q x (codeleft2_y0 ({| ... |} : codeleft2)))
          p
          (codeleft2_q00
             ({|
                codeleft2_y0 := H1 : Y;
                codeleft2_q00 := H2 : ...;
                codeleft2_q10 := H3 : ...;
                codeleft2_u := H5 : ...
              |}
              :
              codeleft2)) =
        codeleft2_q10
          ({|
             codeleft2_y0 := H1 : Y;
             codeleft2_q00 := H2 : Q x0 (...);
             codeleft2_q10 := H3 : Q x1 (...);
             codeleft2_u := H5 : ... @ ...^ = r
           |}
           :
           codeleft2)})
        :
        {a : codeleft2 &
        {p
        : (x0; codeleft2_q00 a).1 =
          (x1; codeleft2_q10 a).1 &
        transport (fun x : X => Q x (codeleft2_y0 a))
          p (x0; codeleft2_q00 a).2 =
        (x1; codeleft2_q10 a).2}}) (Ocodeleft2b_s H)
         (Ocodeleft2b_y0 H) (Ocodeleft2b_q00 H)
         (Ocodeleft2b_q10 H) (Ocodeleft2b_w H)
         (Ocodeleft2b_u H))
      o (fun
           H : {a : codeleft2 &
               {p
               : (x0; codeleft2_q00 a).1 =
                 (x1; codeleft2_q10 a).1 &
               transport
                 (fun x : X => Q x (codeleft2_y0 a)) p
                 (x0; codeleft2_q00 a).2 =
               (x1; codeleft2_q10 a).2}} =>
         (fun H0 : codeleft2 =>
          (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
             (H4 : glue H2 @ (glue H3)^ = r)
             (H5 : {p : x0 = x1 &
                   transport
                     (fun x : X =>
                      Q x (codeleft2_y0 {| ... |})) p
                     (codeleft2_q00
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) =
                   codeleft2_q10
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |}}) =>
           (fun (H6 : x0 = x1)
              (H7 : transport (fun x : X => Q x H1) H6
                      H2 = H3) =>
            {|
              Ocodeleft2b_s := H6 : x0 = x1;
              Ocodeleft2b_y0 := H1 : Y;
              Ocodeleft2b_q00 := H2 : Q x0 (H1 : Y);
              Ocodeleft2b_q10 := H3 : Q x1 (H1 : Y);
              Ocodeleft2b_w :=
                H7
                :
                transport (...) (...) (...) =
                (H3 : ...);
              Ocodeleft2b_u :=
                H4 : glue ... @ (...)^ = r
            |}
            :
            Ocodeleft2b) H5.1 H5.2) (codeleft2_y0 H0)
            (codeleft2_q00 H0) (codeleft2_q10 H0)
            (codeleft2_u H0)) H.1 H.2) == idmap)
     ((fun H : Ocodeleft2b =>
       (fun (H0 : x0 = x1) (H1 : Y) (H2 : Q x0 H1)
          (H3 : Q x1 H1)
          (H4 : transport (fun x : X => Q x H1) H0 H2 =
                H3) (H5 : glue H2 @ (glue H3)^ = r) =>
        1%path) (Ocodeleft2b_s H) (Ocodeleft2b_y0 H)
         (Ocodeleft2b_q00 H) (Ocodeleft2b_q10 H)
         (Ocodeleft2b_w H) (Ocodeleft2b_u H))
      :
      (fun
         H : {a : codeleft2 &
             {p
             : (x0; codeleft2_q00 a).1 =
               (x1; codeleft2_q10 a).1 &
             transport
               (fun x : X => Q x (codeleft2_y0 a)) p
               (x0; codeleft2_q00 a).2 =
             (x1; codeleft2_q10 a).2}} =>
       (fun H0 : codeleft2 =>
        (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
           (H4 : glue H2 @ (glue H3)^ = r)
           (H5 : {p : x0 = x1 &
                 transport
                   (fun x : X =>
                    Q x (codeleft2_y0 {| ... |})) p
                   (codeleft2_q00
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}) =
                 codeleft2_q10
                   {|
                     codeleft2_y0 := H1;
                     codeleft2_q00 := H2;
                     codeleft2_q10 := H3;
                     codeleft2_u := H4
                   |}}) =>
         (fun (H6 : x0 = x1)
            (H7 : transport (fun x : X => Q x H1) H6
                    H2 = H3) =>
          {|
            Ocodeleft2b_s := H6 : x0 = x1;
            Ocodeleft2b_y0 := H1 : Y;
            Ocodeleft2b_q00 := H2 : Q x0 (H1 : Y);
            Ocodeleft2b_q10 := H3 : Q x1 (H1 : Y);
            Ocodeleft2b_w :=
              H7
              :
              transport (...) (...) (...) = (H3 : ...);
            Ocodeleft2b_u :=
              H4 : glue ... @ (...)^ = r
          |}
          :
          Ocodeleft2b) H5.1 H5.2) (codeleft2_y0 H0)
          (codeleft2_q00 H0) (codeleft2_q10 H0)
          (codeleft2_u H0)) H.1 H.2)
      o (fun H : Ocodeleft2b =>
         (fun (H0 : x0 = x1) (H1 : Y) (H2 : Q x0 H1)
            (H3 : Q x1 H1)
            (H4 : transport (fun x : X => Q x H1) H0
                    H2 = H3)
            (H5 : glue H2 @ (glue H3)^ = r) =>
          ({|
             codeleft2_y0 := H1 : Y;
             codeleft2_q00 := H2 : Q x0 (H1 : Y);
             codeleft2_q10 := H3 : Q x1 (H1 : Y);
             codeleft2_u :=
               H5
               :
               glue (H2 : Q x0 (...)) @
               (glue (H3 : Q x1 ...))^ = r
           |}
           :
           codeleft2;
          (H0 : x0 = x1;
          H4
          :
          transport
            (fun x : X =>
             Q x
               (codeleft2_y0 {| ...; ...; ...; ... |}))
            (H0 : x0 = x1)
            (codeleft2_q00
               {|
                 codeleft2_y0 := H1;
                 codeleft2_q00 := H2;
                 codeleft2_q10 := H3;
                 codeleft2_u := H5
               |}) =
          codeleft2_q10
            {|
              codeleft2_y0 := H1;
              codeleft2_q00 := H2;
              codeleft2_q10 := H3;
              codeleft2_u := H5
            |})
          :
          {p : x0 = x1 &
          transport
            (fun x : X =>
             Q x
               (codeleft2_y0 ({| ... |} : codeleft2)))
            p
            (codeleft2_q00
               ({|
                  codeleft2_y0 := H1 : Y;
                  codeleft2_q00 := H2 : ...;
                  codeleft2_q10 := H3 : ...;
                  codeleft2_u := H5 : ...
                |}
                :
                codeleft2)) =
          codeleft2_q10
            ({|
               codeleft2_y0 := H1 : Y;
               codeleft2_q00 := H2 : Q x0 (...);
               codeleft2_q10 := H3 : Q x1 (...);
               codeleft2_u := H5 : ... @ ...^ = r
             |}
             :
             codeleft2)})
          :
          {a : codeleft2 &
          {p
          : (x0; codeleft2_q00 a).1 =
            (x1; codeleft2_q10 a).1 &
          transport
            (fun x : X => Q x (codeleft2_y0 a)) p
            (x0; codeleft2_q00 a).2 =
          (x1; codeleft2_q10 a).2}}) (Ocodeleft2b_s H)
           (Ocodeleft2b_y0 H) (Ocodeleft2b_q00 H)
           (Ocodeleft2b_q10 H) (Ocodeleft2b_w H)
           (Ocodeleft2b_u H)) == idmap) o Ocodeleft2ab ==
functor_sigma idmap (fun x : codeleft2 => fst)
o (equiv_functor_sigma_id
     (fun a : codeleft2 =>
      equiv_path_sigma
        (fun x : X => Q x (codeleft2_y0 a))
        (x0; codeleft2_q00 a) (x1; codeleft2_q10 a) *E
      equiv_path_sigma (fun y : Y => Q x1 y)
        (codeleft2_y0 a; codeleft2_q10 a) (y1; q11))
   oE equiv_adjointify
        (fun H : Ocodeleft2a =>
         (fun (H0 : x0 = x1) (H1 : Q x0 y1)
            (H2 : transport (fun x : X => Q x y1) H0
                    H1 = q11)
            (H3 : glue H1 @ (glue q11)^ = r) =>
          ({|
             codeleft2_y0 := y1 : Y;
             codeleft2_q00 := H1 : Q x0 (y1 : Y);
             codeleft2_q10 := q11 : Q x1 (y1 : Y);
             codeleft2_u :=
               H3
               :
               glue (H1 : Q x0 (y1 : Y)) @
               (glue (q11 : Q x1 (y1 : Y)))^ = r
           |}
           :
           codeleft2;
          ((H0 : x0 = x1;
           H2
           :
           transport (fun x : X => Q x y1)
             (H0 : x0 = x1) H1 = q11)
           :
           {p : x0 = x1 &
           transport (fun x : X => Q x y1) p H1 = q11},
          (1%path : y1 = y1;
          1%path
          :
          transport (fun y : Y => Q x1 y)
            (1%path : y1 = y1) q11 = q11)
          :
          {p : y1 = y1 &
          transport (fun y : Y => Q x1 y) p q11 = q11})
          :
          {p : x0 = x1 &
          transport
            (fun x : X =>
             Q x
               (codeleft2_y0
                  ({|
                     codeleft2_y0 := ...;
                     codeleft2_q00 := ...;
                     codeleft2_q10 := ...;
                     codeleft2_u := ...
                   |}
                   :
                   codeleft2))) p
            (codeleft2_q00
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : Q x0 (...);
                  codeleft2_q10 := q11 : Q x1 (...);
                  codeleft2_u := H3 : ... @ ...^ = r
                |}
                :
                codeleft2)) =
          codeleft2_q10
            ({|
               codeleft2_y0 := y1 : Y;
               codeleft2_q00 := H1 : Q x0 (y1 : Y);
               codeleft2_q10 := q11 : Q x1 (y1 : Y);
               codeleft2_u :=
                 H3 : glue (...) @ (glue ...)^ = r
             |}
             :
             codeleft2)} *
          {p
          : codeleft2_y0
              ({|
                 codeleft2_y0 := y1 : Y;
                 codeleft2_q00 := H1 : Q x0 (y1 : Y);
                 codeleft2_q10 := q11 : Q x1 (y1 : Y);
                 codeleft2_u :=
                   H3 : glue (...) @ (glue ...)^ = r
               |}
               :
               codeleft2) = y1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_q10
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : Q x0 (...);
                  codeleft2_q10 := q11 : Q x1 (...);
                  codeleft2_u := H3 : ... @ ...^ = r
                |}
                :
                codeleft2)) = q11})
          :
          {a : codeleft2 &
          {p
          : (x0; codeleft2_q00 a).1 =
            (x1; codeleft2_q10 a).1 &
          transport
            (fun x : X => Q x (codeleft2_y0 a)) p
            (x0; codeleft2_q00 a).2 =
          (x1; codeleft2_q10 a).2} *
          {p
          : (codeleft2_y0 a; codeleft2_q10 a).1 =
            (y1; q11).1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_y0 a; codeleft2_q10 a).2 =
          (y1; q11).2}}) (Ocodeleft2a_s H)
           (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
           (Ocodeleft2a_u H))
        (fun
           H : {a : codeleft2 &
               {p
               : (x0; codeleft2_q00 a).1 =
                 (x1; codeleft2_q10 a).1 &
               transport
                 (fun x : X => Q x (codeleft2_y0 a)) p
                 (x0; codeleft2_q00 a).2 =
               (x1; codeleft2_q10 a).2} *
               {p
               : (codeleft2_y0 a; codeleft2_q10 a).1 =
                 (y1; q11).1 &
               transport (fun y : Y => Q x1 y) p
                 (codeleft2_y0 a; codeleft2_q10 a).2 =
               (y1; q11).2}} =>
         (fun H0 : codeleft2 =>
          (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
             (H4 : glue H2 @ (glue H3)^ = r)
             (H5 : {p : x0 = x1 &
                   transport
                     (fun x : X =>
                      Q x
                        (codeleft2_y0
                           {|
                             codeleft2_y0 := H1;
                             codeleft2_q00 := H2;
                             codeleft2_q10 := H3;
                             codeleft2_u := H4
                           |})) p
                     (codeleft2_q00
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) =
                   codeleft2_q10
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |}} *
                   {p
                   : codeleft2_y0
                       {|
                         codeleft2_y0 := H1;
                         codeleft2_q00 := H2;
                         codeleft2_q10 := H3;
                         codeleft2_u := H4
                       |} = y1 &
                   transport (fun y : Y => Q x1 y) p
                     (codeleft2_q10
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) = q11}) =>
           (fun
              H6 : {p : x0 = x1 &
                   transport (fun x : X => Q x H1) p
                     H2 = H3} =>
            (fun (H7 : x0 = x1)
               (H8 : transport (fun x : X => Q x H1)
                       H7 H2 = H3)
               (H9 : {p : H1 = y1 &
                     transport (fun ... => Q x1 y) p
                       H3 = q11}) =>
             (fun H10 : H1 = y1 =>
              paths_ind_r y1
                (fun (y : Y) (p : ...) =>
                 forall (H11 : ...) (H12 : ...),
                 ... -> ...)
                (fun (H11 : ...) (H12 : ...)
                   (H13 : ...) (H14 : ...) (H15 : ...)
                 =>
                 paths_ind_r q11 (...) (...) H12 H15
                   H13 H14) H1 H10 H2 H3 H4 H8) H9.1
               H9.2) H6.1 H6.2) (fst H5) (snd H5))
            (codeleft2_y0 H0) (codeleft2_q00 H0)
            (codeleft2_q10 H0) (codeleft2_u H0)) H.1
           H.2)
        ((fun
            H : {a : codeleft2 &
                {p
                : (x0; codeleft2_q00 a).1 =
                  (x1; codeleft2_q10 a).1 &
                transport
                  (fun x : X => Q x (codeleft2_y0 a))
                  p (x0; codeleft2_q00 a).2 =
                (x1; codeleft2_q10 a).2} *
                {p
                : (codeleft2_y0 a; codeleft2_q10 a).1 =
                  (y1; q11).1 &
                transport (fun y : Y => Q x1 y) p
                  (codeleft2_y0 a; codeleft2_q10 a).2 =
                (y1; q11).2}} =>
          (fun H0 : codeleft2 =>
           (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
              (H4 : glue H2 @ (glue H3)^ = r)
              (H5 : {p : x0 = x1 &
                    transport
                      (fun x : X =>
                       Q x (codeleft2_y0 {| ... |})) p
                      (codeleft2_q00
                         {|
                           codeleft2_y0 := H1;
                           codeleft2_q00 := H2;
                           codeleft2_q10 := H3;
                           codeleft2_u := H4
                         |}) =
                    codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}} *
                    {p
                    : codeleft2_y0
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |} = y1 &
                    transport (fun y : Y => Q x1 y) p
                      (codeleft2_q10
                         {|
                           codeleft2_y0 := H1;
                           codeleft2_q00 := H2;
                           codeleft2_q10 := H3;
                           codeleft2_u := H4
                         |}) = q11}) =>
            (fun
               H6 : {p : x0 = x1 &
                    transport (fun x : X => Q x H1) p
                      H2 = H3} =>
             (fun (H7 : x0 = x1)
                (H8 : transport (... => ...) H7 H2 =
                      H3)
                (H9 : {p : H1 = y1 &
                      transport (...) p H3 = q11}) =>
              (fun H10 : H1 = y1 =>
               paths_ind_r y1 (... => ...)
                 (... => ...) H1 H10 H2 H3 H4 H8) H9.1
                H9.2) H6.1 H6.2) (fst H5) (snd H5))
             (codeleft2_y0 H0) (codeleft2_q00 H0)
             (codeleft2_q10 H0) (codeleft2_u H0)) H.1
            H.2)
         :
         (fun H : Ocodeleft2a =>
          (fun (H0 : x0 = x1) (H1 : Q x0 y1)
             (H2 : transport (fun x : X => Q x y1) H0
                     H1 = q11)
             (H3 : glue H1 @ (glue q11)^ = r) =>
           ({|
              codeleft2_y0 := y1 : Y;
              codeleft2_q00 := H1 : Q x0 (y1 : Y);
              codeleft2_q10 := q11 : Q x1 (y1 : Y);
              codeleft2_u :=
                H3
                :
                glue (H1 : Q x0 ...) @
                (glue (q11 : ...))^ = r
            |}
            :
            codeleft2;
           ((H0 : x0 = x1;
            H2
            :
            transport (fun x : X => Q x y1)
              (H0 : x0 = x1) H1 = q11)
            :
            {p : x0 = x1 &
            transport (fun x : X => Q x y1) p H1 = q11},
           (1%path : y1 = y1;
           1%path
           :
           transport (fun y : Y => Q x1 y)
             (1%path : y1 = y1) q11 = q11)
           :
           {p : y1 = y1 &
           transport (fun y : Y => Q x1 y) p q11 = q11})
           :
           {p : x0 = x1 &
           transport
             (fun x : X => Q x (codeleft2_y0 (...))) p
             (codeleft2_q00
                ({| ...; ...; ...; ... |} : codeleft2)) =
           codeleft2_q10
             ({|
                codeleft2_y0 := y1 : Y;
                codeleft2_q00 := H1 : ...;
                codeleft2_q10 := q11 : ...;
                codeleft2_u := H3 : ...
              |}
              :
              codeleft2)} *
           {p
           : codeleft2_y0
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : ...;
                  codeleft2_q10 := q11 : ...;
                  codeleft2_u := H3 : ...
                |}
                :
                codeleft2) = y1 &
           transport (fun y : Y => Q x1 y) p
             (codeleft2_q10
                ({| ...; ...; ...; ... |} : codeleft2)) =
           q11})
           :
           {a : codeleft2 &
           {p
           : (x0; codeleft2_q00 a).1 =
             (x1; codeleft2_q10 a).1 &
           transport
             (fun x : X => Q x (codeleft2_y0 a)) p
             (x0; codeleft2_q00 a).2 =
           (x1; codeleft2_q10 a).2} *
           {p
           : (codeleft2_y0 a; codeleft2_q10 a).1 =
             (y1; q11).1 &
           transport (fun y : Y => Q x1 y) p
             (codeleft2_y0 a; codeleft2_q10 a).2 =
           (y1; q11).2}}) (Ocodeleft2a_s H)
            (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
            (Ocodeleft2a_u H))
         o (fun
              H : {a : codeleft2 &
                  {p
                  : (x0; codeleft2_q00 a).1 =
                    (x1; codeleft2_q10 a).1 &
                  transport
                    (fun x : X => Q x (codeleft2_y0 a))
                    p (x0; codeleft2_q00 a).2 =
                  (x1; codeleft2_q10 a).2} *
                  {p
                  : (codeleft2_y0 a; codeleft2_q10 a).1 =
                    (y1; q11).1 &
                  transport (fun y : Y => Q x1 y) p
                    (codeleft2_y0 a; codeleft2_q10 a).2 =
                  (y1; q11).2}} =>
            (fun H0 : codeleft2 =>
             (fun (H1 : Y) (H2 : Q x0 H1)
                (H3 : Q x1 H1)
                (H4 : glue H2 @ (glue H3)^ = r)
                (H5 : {p : x0 = x1 &
                      transport
                        (fun x : X => Q x (...)) p
                        (codeleft2_q00
                           {| ...; ...; ...; ... |}) =
                      codeleft2_q10
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}} *
                      {p
                      : codeleft2_y0
                          {|
                            codeleft2_y0 := H1;
                            codeleft2_q00 := H2;
                            codeleft2_q10 := H3;
                            codeleft2_u := H4
                          |} = y1 &
                      transport (fun y : Y => Q x1 y)
                        p
                        (codeleft2_q10
                           {| ...; ...; ...; ... |}) =
                      q11}) =>
              (fun
                 H6 : {p : x0 = x1 &
                      transport (... => ...) p H2 = H3}
               =>
               (fun (H7 : x0 = x1)
                  (H8 : transport ... H7 H2 = H3)
                  (H9 : {p : H1 = y1 & ... = q11}) =>
                (fun ... =>
                 paths_ind_r y1 ... ... H1 H10 H2 H3
                   H4 H8) H9.1 H9.2) H6.1 H6.2)
                (fst H5) (snd H5)) (codeleft2_y0 H0)
               (codeleft2_q00 H0) (codeleft2_q10 H0)
               (codeleft2_u H0)) H.1 H.2) == idmap)
        ((fun H : Ocodeleft2a =>
          (fun (H0 : x0 = x1) (H1 : Q x0 y1)
             (H2 : transport (fun x : X => Q x y1) H0
                     H1 = q11)
             (H3 : glue H1 @ (glue q11)^ = r) =>
           1%path) (Ocodeleft2a_s H)
            (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
            (Ocodeleft2a_u H))
         :
         (fun
            H : {a : codeleft2 &
                {p
                : (x0; codeleft2_q00 a).1 =
                  (x1; codeleft2_q10 a).1 &
                transport
                  (fun x : X => Q x (codeleft2_y0 a))
                  p (x0; codeleft2_q00 a).2 =
                (x1; codeleft2_q10 a).2} *
                {p
                : (codeleft2_y0 a; codeleft2_q10 a).1 =
                  (y1; q11).1 &
                transport (fun y : Y => Q x1 y) p
                  (codeleft2_y0 a; codeleft2_q10 a).2 =
                (y1; q11).2}} =>
          (fun H0 : codeleft2 =>
           (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
              (H4 : glue H2 @ (glue H3)^ = r)
              (H5 : {p : x0 = x1 &
                    transport (fun x : X => Q x (...))
                      p
                      (codeleft2_q00
                         {| ...; ...; ...; ... |}) =
                    codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}} *
                    {p
                    : codeleft2_y0
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |} = y1 &
                    transport (fun y : Y => Q x1 y) p
                      (codeleft2_q10
                         {| ...; ...; ...; ... |}) =
                    q11}) =>
            (fun
               H6 : {p : x0 = x1 &
                    transport (... => ...) p H2 = H3}
             =>
             (fun (H7 : x0 = x1)
                (H8 : transport ... H7 H2 = H3)
                (H9 : {p : H1 = y1 & ... = q11}) =>
              (fun ... =>
               paths_ind_r y1 ... ... H1 H10 H2 H3 H4
                 H8) H9.1 H9.2) H6.1 H6.2) (fst H5)
              (snd H5)) (codeleft2_y0 H0)
             (codeleft2_q00 H0) (codeleft2_q10 H0)
             (codeleft2_u H0)) H.1 H.2)
         o (fun H : Ocodeleft2a =>
            (fun (H0 : x0 = x1) (H1 : Q x0 y1)
               (H2 : transport (fun x : X => Q x y1)
                       H0 H1 = q11)
               (H3 : glue H1 @ (glue q11)^ = r) =>
             ({|
                codeleft2_y0 := y1 : Y;
                codeleft2_q00 := H1 : Q x0 (y1 : Y);
                codeleft2_q10 := q11 : Q x1 (y1 : Y);
                codeleft2_u :=
                  H3
                  :
                  glue (H1 : Q x0 ...) @
                  (glue (q11 : ...))^ = r
              |}
              :
              codeleft2;
             ((H0 : x0 = x1;
              H2
              :
              transport (fun x : X => Q x y1)
                (H0 : x0 = x1) H1 = q11)
              :
              {p : x0 = x1 &
              transport (fun x : X => Q x y1) p H1 =
              q11},
             (1%path : y1 = y1;
             1%path
             :
             transport (fun y : Y => Q x1 y)
               (1%path : y1 = y1) q11 = q11)
             :
             {p : y1 = y1 &
             transport (fun y : Y => Q x1 y) p q11 =
             q11})
             :
             {p : x0 = x1 &
             transport
               (fun x : X => Q x (codeleft2_y0 (...)))
               p
               (codeleft2_q00
                  ({| ...; ...; ...; ... |}
                   :
                   codeleft2)) =
             codeleft2_q10
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : ...;
                  codeleft2_q10 := q11 : ...;
                  codeleft2_u := H3 : ...
                |}
                :
                codeleft2)} *
             {p
             : codeleft2_y0
                 ({|
                    codeleft2_y0 := y1 : Y;
                    codeleft2_q00 := H1 : ...;
                    codeleft2_q10 := q11 : ...;
                    codeleft2_u := H3 : ...
                  |}
                  :
                  codeleft2) = y1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_q10
                  ({| ...; ...; ...; ... |}
                   :
                   codeleft2)) = q11})
             :
             {a : codeleft2 &
             {p
             : (x0; codeleft2_q00 a).1 =
               (x1; codeleft2_q10 a).1 &
             transport
               (fun x : X => Q x (codeleft2_y0 a)) p
               (x0; codeleft2_q00 a).2 =
             (x1; codeleft2_q10 a).2} *
             {p
             : (codeleft2_y0 a; codeleft2_q10 a).1 =
               (y1; q11).1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_y0 a; codeleft2_q10 a).2 =
             (y1; q11).2}}) (Ocodeleft2a_s H)
              (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
              (Ocodeleft2a_u H)) == idmap)) intros; reflexivity.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
equiv_functor_sigma_id
  (fun a : codeleft2 =>
   equiv_path_sigma (fun y : Y => Q x1 y)
     (codeleft2_y0 a; codeleft2_q10 a) (y1; q11))
oE equiv_adjointify
     (fun H : Ocodeleft2c =>
      (fun (H0 : Q x0 y1)
         (H1 : glue H0 @ (glue q11)^ = r) =>
       ({|
          codeleft2_y0 := y1 : Y;
          codeleft2_q00 := H0 : Q x0 (y1 : Y);
          codeleft2_q10 := q11 : Q x1 (y1 : Y);
          codeleft2_u :=
            H1
            :
            glue (H0 : Q x0 (y1 : Y)) @
            (glue (q11 : Q x1 (y1 : Y)))^ = r
        |}
        :
        codeleft2;
       (1%path : y1 = y1;
       1%path
       :
       transport (fun y : Y => Q x1 y)
         (1%path : y1 = y1) q11 = q11)
       :
       {p
       : codeleft2_y0
           ({|
              codeleft2_y0 := y1 : Y;
              codeleft2_q00 := H0 : Q x0 (y1 : Y);
              codeleft2_q10 := q11 : Q x1 (y1 : Y);
              codeleft2_u :=
                H1
                :
                glue (H0 : Q x0 ...) @
                (glue (q11 : ...))^ = r
            |}
            :
            codeleft2) = y1 &
       transport (fun y : Y => Q x1 y) p
         (codeleft2_q10
            ({|
               codeleft2_y0 := y1 : Y;
               codeleft2_q00 := H0 : Q x0 (y1 : Y);
               codeleft2_q10 := q11 : Q x1 (y1 : Y);
               codeleft2_u :=
                 H1 : glue (...) @ (glue ...)^ = r
             |}
             :
             codeleft2)) = q11})
       :
       {a : codeleft2 &
       {p
       : (codeleft2_y0 a; codeleft2_q10 a).1 =
         (y1; q11).1 &
       transport (fun y : Y => Q x1 y) p
         (codeleft2_y0 a; codeleft2_q10 a).2 =
       (y1; q11).2}}) H.1 H.2)
     (fun
        H : {a : codeleft2 &
            {p
            : (codeleft2_y0 a; codeleft2_q10 a).1 =
              (y1; q11).1 &
            transport (fun y : Y => Q x1 y) p
              (codeleft2_y0 a; codeleft2_q10 a).2 =
            (y1; q11).2}} =>
      (fun H0 : codeleft2 =>
       (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
          (H4 : glue H2 @ (glue H3)^ = r)
          (H5 : {p
                : codeleft2_y0
                    {|
                      codeleft2_y0 := H1;
                      codeleft2_q00 := H2;
                      codeleft2_q10 := H3;
                      codeleft2_u := H4
                    |} = y1 &
                transport (fun y : Y => Q x1 y) p
                  (codeleft2_q10
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |}) = q11}) =>
        (fun H6 : H1 = y1 =>
         paths_ind_r y1
           (fun (y : Y) (p : y = y1) =>
            forall (H7 : Q x0 y) (H8 : Q x1 y),
            glue H7 @ (glue H8)^ = r ->
            transport (fun y0 : Y => Q x1 y0) p H8 =
            q11 -> Ocodeleft2c)
           (fun (H7 : Q x0 y1) (H8 : Q x1 y1)
              (H9 : glue H7 @ (glue H8)^ = r)
              (H10 : transport (fun y : Y => Q x1 y) 1
                       H8 = q11) =>
            paths_ind_r q11
              (fun (y : Q x1 y1) (_ : y = q11) =>
               glue H7 @ (glue y)^ = r -> Ocodeleft2c)
              (fun H11 : glue H7 @ (glue q11)^ = r =>
               (H7 : Q x0 y1;
               H11 : glue ... @ (...)^ = r)
               :
               Ocodeleft2c) H8 H10 H9) H1 H6 H2 H3 H4)
          H5.1 H5.2) (codeleft2_y0 H0)
         (codeleft2_q00 H0) (codeleft2_q10 H0)
         (codeleft2_u H0)) H.1 H.2)
     ((fun
         H : {a : codeleft2 &
             {p
             : (codeleft2_y0 a; codeleft2_q10 a).1 =
               (y1; q11).1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_y0 a; codeleft2_q10 a).2 =
             (y1; q11).2}} =>
       (fun H0 : codeleft2 =>
        (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
           (H4 : glue H2 @ (glue H3)^ = r)
           (H5 : {p
                 : codeleft2_y0
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |} = y1 &
                 transport (fun y : Y => Q x1 y) p
                   (codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}) = q11}) =>
         (fun H6 : H1 = y1 =>
          paths_ind_r y1
            (fun (y : Y) (p : y = y1) =>
             forall (H7 : Q x0 y) (H8 : Q x1 y)
             (H9 : glue H7 @ (glue H8)^ = r)
             (proj2 : transport (fun ... => Q x1 y0) p
                        H8 = q11),
             ({|
                codeleft2_y0 := y1;
                codeleft2_q00 := (...).1;
                codeleft2_q10 := q11;
                codeleft2_u := (...).2
              |}; 1%path; 1%path) =
             ({|
                codeleft2_y0 := y;
                codeleft2_q00 := H7;
                codeleft2_q10 := H8;
                codeleft2_u := H9
              |}; p; proj2))
            (fun (H7 : Q x0 y1) (H8 : Q x1 y1)
               (H9 : glue H7 @ (glue H8)^ = r)
               (H10 : transport (fun ... => Q x1 y) 1
                        H8 = q11) =>
             paths_ind_r q11
               (fun (y : Q x1 y1) (p : y = q11) =>
                forall H11 : ... @ ...^ = r,
                ({| ... |}; 1%path; 1%path) =
                ({| ... |}; 1%path; p))
               (fun H11 : ... @ ...^ = r => 1%path) H8
               H10 H9) H1 H6 H2 H3 H4) H5.1 H5.2)
          (codeleft2_y0 H0) (codeleft2_q00 H0)
          (codeleft2_q10 H0) (codeleft2_u H0)) H.1 H.2)
      :
      (fun H : Ocodeleft2c =>
       (fun (H0 : Q x0 y1)
          (H1 : glue H0 @ (glue q11)^ = r) =>
        ({|
           codeleft2_y0 := y1 : Y;
           codeleft2_q00 := H0 : Q x0 (y1 : Y);
           codeleft2_q10 := q11 : Q x1 (y1 : Y);
           codeleft2_u :=
             H1
             :
             glue (H0 : Q x0 (...)) @
             (glue (q11 : Q x1 ...))^ = r
         |}
         :
         codeleft2;
        (1%path : y1 = y1;
        1%path
        :
        transport (fun y : Y => Q x1 y)
          (1%path : y1 = y1) q11 = q11)
        :
        {p
        : codeleft2_y0
            ({|
               codeleft2_y0 := y1 : Y;
               codeleft2_q00 := H0 : Q x0 (...);
               codeleft2_q10 := q11 : Q x1 (...);
               codeleft2_u := H1 : ... @ ...^ = r
             |}
             :
             codeleft2) = y1 &
        transport (fun y : Y => Q x1 y) p
          (codeleft2_q10
             ({|
                codeleft2_y0 := y1 : Y;
                codeleft2_q00 := H0 : ...;
                codeleft2_q10 := q11 : ...;
                codeleft2_u := H1 : ...
              |}
              :
              codeleft2)) = q11})
        :
        {a : codeleft2 &
        {p
        : (codeleft2_y0 a; codeleft2_q10 a).1 =
          (y1; q11).1 &
        transport (fun y : Y => Q x1 y) p
          (codeleft2_y0 a; codeleft2_q10 a).2 =
        (y1; q11).2}}) H.1 H.2)
      o (fun
           H : {a : codeleft2 &
               {p
               : (codeleft2_y0 a; codeleft2_q10 a).1 =
                 (y1; q11).1 &
               transport (fun y : Y => Q x1 y) p
                 (codeleft2_y0 a; codeleft2_q10 a).2 =
               (y1; q11).2}} =>
         (fun H0 : codeleft2 =>
          (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
             (H4 : glue H2 @ (glue H3)^ = r)
             (H5 : {p
                   : codeleft2_y0
                       {|
                         codeleft2_y0 := H1;
                         codeleft2_q00 := H2;
                         codeleft2_q10 := H3;
                         codeleft2_u := H4
                       |} = y1 &
                   transport (fun y : Y => Q x1 y) p
                     (codeleft2_q10
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) = q11}) =>
           (fun H6 : H1 = y1 =>
            paths_ind_r y1
              (fun (y : Y) (p : y = y1) =>
               forall (H7 : Q x0 y) (H8 : Q x1 y),
               glue H7 @ (...)^ = r ->
               transport ... p H8 = q11 -> Ocodeleft2c)
              (fun (H7 : Q x0 y1) (H8 : Q x1 y1)
                 (H9 : glue H7 @ (...)^ = r)
                 (H10 : transport (...) 1 H8 = q11) =>
               paths_ind_r q11
                 (fun (y : ...) (_ : ...) =>
                  ... = r -> Ocodeleft2c)
                 (fun H11 : ... =>
                  (...; ...) : Ocodeleft2c) H8 H10 H9)
              H1 H6 H2 H3 H4) H5.1 H5.2)
            (codeleft2_y0 H0) (codeleft2_q00 H0)
            (codeleft2_q10 H0) (codeleft2_u H0)) H.1
           H.2) == idmap)
     ((fun H : Ocodeleft2c =>
       (fun (H0 : Q x0 y1)
          (H1 : glue H0 @ (glue q11)^ = r) => 1%path)
         H.1 H.2)
      :
      (fun
         H : {a : codeleft2 &
             {p
             : (codeleft2_y0 a; codeleft2_q10 a).1 =
               (y1; q11).1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_y0 a; codeleft2_q10 a).2 =
             (y1; q11).2}} =>
       (fun H0 : codeleft2 =>
        (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
           (H4 : glue H2 @ (glue H3)^ = r)
           (H5 : {p
                 : codeleft2_y0
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |} = y1 &
                 transport (fun y : Y => Q x1 y) p
                   (codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}) = q11}) =>
         (fun H6 : H1 = y1 =>
          paths_ind_r y1
            (fun (y : Y) (p : y = y1) =>
             forall (H7 : Q x0 y) (H8 : Q x1 y),
             glue H7 @ (...)^ = r ->
             transport ... p H8 = q11 -> Ocodeleft2c)
            (fun (H7 : Q x0 y1) (H8 : Q x1 y1)
               (H9 : glue H7 @ (...)^ = r)
               (H10 : transport (...) 1 H8 = q11) =>
             paths_ind_r q11
               (fun (y : ...) (_ : ...) =>
                ... = r -> Ocodeleft2c)
               (fun H11 : ... =>
                (...; ...) : Ocodeleft2c) H8 H10 H9)
            H1 H6 H2 H3 H4) H5.1 H5.2)
          (codeleft2_y0 H0) (codeleft2_q00 H0)
          (codeleft2_q10 H0) (codeleft2_u H0)) H.1 H.2)
      o (fun H : Ocodeleft2c =>
         (fun (H0 : Q x0 y1)
            (H1 : glue H0 @ (glue q11)^ = r) =>
          ({|
             codeleft2_y0 := y1 : Y;
             codeleft2_q00 := H0 : Q x0 (y1 : Y);
             codeleft2_q10 := q11 : Q x1 (y1 : Y);
             codeleft2_u :=
               H1
               :
               glue (H0 : Q x0 (...)) @
               (glue (q11 : Q x1 ...))^ = r
           |}
           :
           codeleft2;
          (1%path : y1 = y1;
          1%path
          :
          transport (fun y : Y => Q x1 y)
            (1%path : y1 = y1) q11 = q11)
          :
          {p
          : codeleft2_y0
              ({|
                 codeleft2_y0 := y1 : Y;
                 codeleft2_q00 := H0 : Q x0 (...);
                 codeleft2_q10 := q11 : Q x1 (...);
                 codeleft2_u := H1 : ... @ ...^ = r
               |}
               :
               codeleft2) = y1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_q10
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H0 : ...;
                  codeleft2_q10 := q11 : ...;
                  codeleft2_u := H1 : ...
                |}
                :
                codeleft2)) = q11})
          :
          {a : codeleft2 &
          {p
          : (codeleft2_y0 a; codeleft2_q10 a).1 =
            (y1; q11).1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_y0 a; codeleft2_q10 a).2 =
          (y1; q11).2}}) H.1 H.2) == idmap)
o Ocodeleft2ac ==
functor_sigma idmap (fun x : codeleft2 => snd)
o (equiv_functor_sigma_id
     (fun a : codeleft2 =>
      equiv_path_sigma
        (fun x : X => Q x (codeleft2_y0 a))
        (x0; codeleft2_q00 a) (x1; codeleft2_q10 a) *E
      equiv_path_sigma (fun y : Y => Q x1 y)
        (codeleft2_y0 a; codeleft2_q10 a) (y1; q11))
   oE equiv_adjointify
        (fun H : Ocodeleft2a =>
         (fun (H0 : x0 = x1) (H1 : Q x0 y1)
            (H2 : transport (fun x : X => Q x y1) H0
                    H1 = q11)
            (H3 : glue H1 @ (glue q11)^ = r) =>
          ({|
             codeleft2_y0 := y1 : Y;
             codeleft2_q00 := H1 : Q x0 (y1 : Y);
             codeleft2_q10 := q11 : Q x1 (y1 : Y);
             codeleft2_u :=
               H3
               :
               glue (H1 : Q x0 (y1 : Y)) @
               (glue (q11 : Q x1 (y1 : Y)))^ = r
           |}
           :
           codeleft2;
          ((H0 : x0 = x1;
           H2
           :
           transport (fun x : X => Q x y1)
             (H0 : x0 = x1) H1 = q11)
           :
           {p : x0 = x1 &
           transport (fun x : X => Q x y1) p H1 = q11},
          (1%path : y1 = y1;
          1%path
          :
          transport (fun y : Y => Q x1 y)
            (1%path : y1 = y1) q11 = q11)
          :
          {p : y1 = y1 &
          transport (fun y : Y => Q x1 y) p q11 = q11})
          :
          {p : x0 = x1 &
          transport
            (fun x : X =>
             Q x
               (codeleft2_y0
                  ({|
                     codeleft2_y0 := ...;
                     codeleft2_q00 := ...;
                     codeleft2_q10 := ...;
                     codeleft2_u := ...
                   |}
                   :
                   codeleft2))) p
            (codeleft2_q00
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : Q x0 (...);
                  codeleft2_q10 := q11 : Q x1 (...);
                  codeleft2_u := H3 : ... @ ...^ = r
                |}
                :
                codeleft2)) =
          codeleft2_q10
            ({|
               codeleft2_y0 := y1 : Y;
               codeleft2_q00 := H1 : Q x0 (y1 : Y);
               codeleft2_q10 := q11 : Q x1 (y1 : Y);
               codeleft2_u :=
                 H3 : glue (...) @ (glue ...)^ = r
             |}
             :
             codeleft2)} *
          {p
          : codeleft2_y0
              ({|
                 codeleft2_y0 := y1 : Y;
                 codeleft2_q00 := H1 : Q x0 (y1 : Y);
                 codeleft2_q10 := q11 : Q x1 (y1 : Y);
                 codeleft2_u :=
                   H3 : glue (...) @ (glue ...)^ = r
               |}
               :
               codeleft2) = y1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_q10
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : Q x0 (...);
                  codeleft2_q10 := q11 : Q x1 (...);
                  codeleft2_u := H3 : ... @ ...^ = r
                |}
                :
                codeleft2)) = q11})
          :
          {a : codeleft2 &
          {p
          : (x0; codeleft2_q00 a).1 =
            (x1; codeleft2_q10 a).1 &
          transport
            (fun x : X => Q x (codeleft2_y0 a)) p
            (x0; codeleft2_q00 a).2 =
          (x1; codeleft2_q10 a).2} *
          {p
          : (codeleft2_y0 a; codeleft2_q10 a).1 =
            (y1; q11).1 &
          transport (fun y : Y => Q x1 y) p
            (codeleft2_y0 a; codeleft2_q10 a).2 =
          (y1; q11).2}}) (Ocodeleft2a_s H)
           (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
           (Ocodeleft2a_u H))
        (fun
           H : {a : codeleft2 &
               {p
               : (x0; codeleft2_q00 a).1 =
                 (x1; codeleft2_q10 a).1 &
               transport
                 (fun x : X => Q x (codeleft2_y0 a)) p
                 (x0; codeleft2_q00 a).2 =
               (x1; codeleft2_q10 a).2} *
               {p
               : (codeleft2_y0 a; codeleft2_q10 a).1 =
                 (y1; q11).1 &
               transport (fun y : Y => Q x1 y) p
                 (codeleft2_y0 a; codeleft2_q10 a).2 =
               (y1; q11).2}} =>
         (fun H0 : codeleft2 =>
          (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
             (H4 : glue H2 @ (glue H3)^ = r)
             (H5 : {p : x0 = x1 &
                   transport
                     (fun x : X =>
                      Q x
                        (codeleft2_y0
                           {|
                             codeleft2_y0 := H1;
                             codeleft2_q00 := H2;
                             codeleft2_q10 := H3;
                             codeleft2_u := H4
                           |})) p
                     (codeleft2_q00
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) =
                   codeleft2_q10
                     {|
                       codeleft2_y0 := H1;
                       codeleft2_q00 := H2;
                       codeleft2_q10 := H3;
                       codeleft2_u := H4
                     |}} *
                   {p
                   : codeleft2_y0
                       {|
                         codeleft2_y0 := H1;
                         codeleft2_q00 := H2;
                         codeleft2_q10 := H3;
                         codeleft2_u := H4
                       |} = y1 &
                   transport (fun y : Y => Q x1 y) p
                     (codeleft2_q10
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}) = q11}) =>
           (fun
              H6 : {p : x0 = x1 &
                   transport (fun x : X => Q x H1) p
                     H2 = H3} =>
            (fun (H7 : x0 = x1)
               (H8 : transport (fun x : X => Q x H1)
                       H7 H2 = H3)
               (H9 : {p : H1 = y1 &
                     transport (fun ... => Q x1 y) p
                       H3 = q11}) =>
             (fun H10 : H1 = y1 =>
              paths_ind_r y1
                (fun (y : Y) (p : ...) =>
                 forall (H11 : ...) (H12 : ...),
                 ... -> ...)
                (fun (H11 : ...) (H12 : ...)
                   (H13 : ...) (H14 : ...) (H15 : ...)
                 =>
                 paths_ind_r q11 (...) (...) H12 H15
                   H13 H14) H1 H10 H2 H3 H4 H8) H9.1
               H9.2) H6.1 H6.2) (fst H5) (snd H5))
            (codeleft2_y0 H0) (codeleft2_q00 H0)
            (codeleft2_q10 H0) (codeleft2_u H0)) H.1
           H.2)
        ((fun
            H : {a : codeleft2 &
                {p
                : (x0; codeleft2_q00 a).1 =
                  (x1; codeleft2_q10 a).1 &
                transport
                  (fun x : X => Q x (codeleft2_y0 a))
                  p (x0; codeleft2_q00 a).2 =
                (x1; codeleft2_q10 a).2} *
                {p
                : (codeleft2_y0 a; codeleft2_q10 a).1 =
                  (y1; q11).1 &
                transport (fun y : Y => Q x1 y) p
                  (codeleft2_y0 a; codeleft2_q10 a).2 =
                (y1; q11).2}} =>
          (fun H0 : codeleft2 =>
           (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
              (H4 : glue H2 @ (glue H3)^ = r)
              (H5 : {p : x0 = x1 &
                    transport
                      (fun x : X =>
                       Q x (codeleft2_y0 {| ... |})) p
                      (codeleft2_q00
                         {|
                           codeleft2_y0 := H1;
                           codeleft2_q00 := H2;
                           codeleft2_q10 := H3;
                           codeleft2_u := H4
                         |}) =
                    codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}} *
                    {p
                    : codeleft2_y0
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |} = y1 &
                    transport (fun y : Y => Q x1 y) p
                      (codeleft2_q10
                         {|
                           codeleft2_y0 := H1;
                           codeleft2_q00 := H2;
                           codeleft2_q10 := H3;
                           codeleft2_u := H4
                         |}) = q11}) =>
            (fun
               H6 : {p : x0 = x1 &
                    transport (fun x : X => Q x H1) p
                      H2 = H3} =>
             (fun (H7 : x0 = x1)
                (H8 : transport (... => ...) H7 H2 =
                      H3)
                (H9 : {p : H1 = y1 &
                      transport (...) p H3 = q11}) =>
              (fun H10 : H1 = y1 =>
               paths_ind_r y1 (... => ...)
                 (... => ...) H1 H10 H2 H3 H4 H8) H9.1
                H9.2) H6.1 H6.2) (fst H5) (snd H5))
             (codeleft2_y0 H0) (codeleft2_q00 H0)
             (codeleft2_q10 H0) (codeleft2_u H0)) H.1
            H.2)
         :
         (fun H : Ocodeleft2a =>
          (fun (H0 : x0 = x1) (H1 : Q x0 y1)
             (H2 : transport (fun x : X => Q x y1) H0
                     H1 = q11)
             (H3 : glue H1 @ (glue q11)^ = r) =>
           ({|
              codeleft2_y0 := y1 : Y;
              codeleft2_q00 := H1 : Q x0 (y1 : Y);
              codeleft2_q10 := q11 : Q x1 (y1 : Y);
              codeleft2_u :=
                H3
                :
                glue (H1 : Q x0 ...) @
                (glue (q11 : ...))^ = r
            |}
            :
            codeleft2;
           ((H0 : x0 = x1;
            H2
            :
            transport (fun x : X => Q x y1)
              (H0 : x0 = x1) H1 = q11)
            :
            {p : x0 = x1 &
            transport (fun x : X => Q x y1) p H1 = q11},
           (1%path : y1 = y1;
           1%path
           :
           transport (fun y : Y => Q x1 y)
             (1%path : y1 = y1) q11 = q11)
           :
           {p : y1 = y1 &
           transport (fun y : Y => Q x1 y) p q11 = q11})
           :
           {p : x0 = x1 &
           transport
             (fun x : X => Q x (codeleft2_y0 (...))) p
             (codeleft2_q00
                ({| ...; ...; ...; ... |} : codeleft2)) =
           codeleft2_q10
             ({|
                codeleft2_y0 := y1 : Y;
                codeleft2_q00 := H1 : ...;
                codeleft2_q10 := q11 : ...;
                codeleft2_u := H3 : ...
              |}
              :
              codeleft2)} *
           {p
           : codeleft2_y0
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : ...;
                  codeleft2_q10 := q11 : ...;
                  codeleft2_u := H3 : ...
                |}
                :
                codeleft2) = y1 &
           transport (fun y : Y => Q x1 y) p
             (codeleft2_q10
                ({| ...; ...; ...; ... |} : codeleft2)) =
           q11})
           :
           {a : codeleft2 &
           {p
           : (x0; codeleft2_q00 a).1 =
             (x1; codeleft2_q10 a).1 &
           transport
             (fun x : X => Q x (codeleft2_y0 a)) p
             (x0; codeleft2_q00 a).2 =
           (x1; codeleft2_q10 a).2} *
           {p
           : (codeleft2_y0 a; codeleft2_q10 a).1 =
             (y1; q11).1 &
           transport (fun y : Y => Q x1 y) p
             (codeleft2_y0 a; codeleft2_q10 a).2 =
           (y1; q11).2}}) (Ocodeleft2a_s H)
            (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
            (Ocodeleft2a_u H))
         o (fun
              H : {a : codeleft2 &
                  {p
                  : (x0; codeleft2_q00 a).1 =
                    (x1; codeleft2_q10 a).1 &
                  transport
                    (fun x : X => Q x (codeleft2_y0 a))
                    p (x0; codeleft2_q00 a).2 =
                  (x1; codeleft2_q10 a).2} *
                  {p
                  : (codeleft2_y0 a; codeleft2_q10 a).1 =
                    (y1; q11).1 &
                  transport (fun y : Y => Q x1 y) p
                    (codeleft2_y0 a; codeleft2_q10 a).2 =
                  (y1; q11).2}} =>
            (fun H0 : codeleft2 =>
             (fun (H1 : Y) (H2 : Q x0 H1)
                (H3 : Q x1 H1)
                (H4 : glue H2 @ (glue H3)^ = r)
                (H5 : {p : x0 = x1 &
                      transport
                        (fun x : X => Q x (...)) p
                        (codeleft2_q00
                           {| ...; ...; ...; ... |}) =
                      codeleft2_q10
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |}} *
                      {p
                      : codeleft2_y0
                          {|
                            codeleft2_y0 := H1;
                            codeleft2_q00 := H2;
                            codeleft2_q10 := H3;
                            codeleft2_u := H4
                          |} = y1 &
                      transport (fun y : Y => Q x1 y)
                        p
                        (codeleft2_q10
                           {| ...; ...; ...; ... |}) =
                      q11}) =>
              (fun
                 H6 : {p : x0 = x1 &
                      transport (... => ...) p H2 = H3}
               =>
               (fun (H7 : x0 = x1)
                  (H8 : transport ... H7 H2 = H3)
                  (H9 : {p : H1 = y1 & ... = q11}) =>
                (fun ... =>
                 paths_ind_r y1 ... ... H1 H10 H2 H3
                   H4 H8) H9.1 H9.2) H6.1 H6.2)
                (fst H5) (snd H5)) (codeleft2_y0 H0)
               (codeleft2_q00 H0) (codeleft2_q10 H0)
               (codeleft2_u H0)) H.1 H.2) == idmap)
        ((fun H : Ocodeleft2a =>
          (fun (H0 : x0 = x1) (H1 : Q x0 y1)
             (H2 : transport (fun x : X => Q x y1) H0
                     H1 = q11)
             (H3 : glue H1 @ (glue q11)^ = r) =>
           1%path) (Ocodeleft2a_s H)
            (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
            (Ocodeleft2a_u H))
         :
         (fun
            H : {a : codeleft2 &
                {p
                : (x0; codeleft2_q00 a).1 =
                  (x1; codeleft2_q10 a).1 &
                transport
                  (fun x : X => Q x (codeleft2_y0 a))
                  p (x0; codeleft2_q00 a).2 =
                (x1; codeleft2_q10 a).2} *
                {p
                : (codeleft2_y0 a; codeleft2_q10 a).1 =
                  (y1; q11).1 &
                transport (fun y : Y => Q x1 y) p
                  (codeleft2_y0 a; codeleft2_q10 a).2 =
                (y1; q11).2}} =>
          (fun H0 : codeleft2 =>
           (fun (H1 : Y) (H2 : Q x0 H1) (H3 : Q x1 H1)
              (H4 : glue H2 @ (glue H3)^ = r)
              (H5 : {p : x0 = x1 &
                    transport (fun x : X => Q x (...))
                      p
                      (codeleft2_q00
                         {| ...; ...; ...; ... |}) =
                    codeleft2_q10
                      {|
                        codeleft2_y0 := H1;
                        codeleft2_q00 := H2;
                        codeleft2_q10 := H3;
                        codeleft2_u := H4
                      |}} *
                    {p
                    : codeleft2_y0
                        {|
                          codeleft2_y0 := H1;
                          codeleft2_q00 := H2;
                          codeleft2_q10 := H3;
                          codeleft2_u := H4
                        |} = y1 &
                    transport (fun y : Y => Q x1 y) p
                      (codeleft2_q10
                         {| ...; ...; ...; ... |}) =
                    q11}) =>
            (fun
               H6 : {p : x0 = x1 &
                    transport (... => ...) p H2 = H3}
             =>
             (fun (H7 : x0 = x1)
                (H8 : transport ... H7 H2 = H3)
                (H9 : {p : H1 = y1 & ... = q11}) =>
              (fun ... =>
               paths_ind_r y1 ... ... H1 H10 H2 H3 H4
                 H8) H9.1 H9.2) H6.1 H6.2) (fst H5)
              (snd H5)) (codeleft2_y0 H0)
             (codeleft2_q00 H0) (codeleft2_q10 H0)
             (codeleft2_u H0)) H.1 H.2)
         o (fun H : Ocodeleft2a =>
            (fun (H0 : x0 = x1) (H1 : Q x0 y1)
               (H2 : transport (fun x : X => Q x y1)
                       H0 H1 = q11)
               (H3 : glue H1 @ (glue q11)^ = r) =>
             ({|
                codeleft2_y0 := y1 : Y;
                codeleft2_q00 := H1 : Q x0 (y1 : Y);
                codeleft2_q10 := q11 : Q x1 (y1 : Y);
                codeleft2_u :=
                  H3
                  :
                  glue (H1 : Q x0 ...) @
                  (glue (q11 : ...))^ = r
              |}
              :
              codeleft2;
             ((H0 : x0 = x1;
              H2
              :
              transport (fun x : X => Q x y1)
                (H0 : x0 = x1) H1 = q11)
              :
              {p : x0 = x1 &
              transport (fun x : X => Q x y1) p H1 =
              q11},
             (1%path : y1 = y1;
             1%path
             :
             transport (fun y : Y => Q x1 y)
               (1%path : y1 = y1) q11 = q11)
             :
             {p : y1 = y1 &
             transport (fun y : Y => Q x1 y) p q11 =
             q11})
             :
             {p : x0 = x1 &
             transport
               (fun x : X => Q x (codeleft2_y0 (...)))
               p
               (codeleft2_q00
                  ({| ...; ...; ...; ... |}
                   :
                   codeleft2)) =
             codeleft2_q10
               ({|
                  codeleft2_y0 := y1 : Y;
                  codeleft2_q00 := H1 : ...;
                  codeleft2_q10 := q11 : ...;
                  codeleft2_u := H3 : ...
                |}
                :
                codeleft2)} *
             {p
             : codeleft2_y0
                 ({|
                    codeleft2_y0 := y1 : Y;
                    codeleft2_q00 := H1 : ...;
                    codeleft2_q10 := q11 : ...;
                    codeleft2_u := H3 : ...
                  |}
                  :
                  codeleft2) = y1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_q10
                  ({| ...; ...; ...; ... |}
                   :
                   codeleft2)) = q11})
             :
             {a : codeleft2 &
             {p
             : (x0; codeleft2_q00 a).1 =
               (x1; codeleft2_q10 a).1 &
             transport
               (fun x : X => Q x (codeleft2_y0 a)) p
               (x0; codeleft2_q00 a).2 =
             (x1; codeleft2_q10 a).2} *
             {p
             : (codeleft2_y0 a; codeleft2_q10 a).1 =
               (y1; q11).1 &
             transport (fun y : Y => Q x1 y) p
               (codeleft2_y0 a; codeleft2_q10 a).2 =
             (y1; q11).2}}) (Ocodeleft2a_s H)
              (Ocodeleft2a_q01 H) (Ocodeleft2a_w H)
              (Ocodeleft2a_u H)) == idmap)) intros; reflexivity.
        Defined.

        (** Now we combine this equivalence with the insertion of our connected type. *)
        Definition equiv_Ocodeleft2
          : O (Pushout Ocodeleft2ab Ocodeleft2ac) <~> O codeleft2.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O (Pushout Ocodeleft2ab Ocodeleft2ac) <~> O codeleft2
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O (Pushout Ocodeleft2ab Ocodeleft2ac) <~> O codeleft2
          refine (_ oE equiv_O_functor O equiv_Ocodeleft2plus).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O codeleft2plus <~> O codeleft2
          refine (_ oE (equiv_O_sigma_O O _)^-1).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O
  {x : codeleft2 &
  O
    (Join
       ((x0; codeleft2_q00 x) = (x1; codeleft2_q10 x))
       ((codeleft2_y0 x; codeleft2_q10 x) = (y1; q11)))} <~>
O codeleft2
          apply equiv_O_functor.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
{x : codeleft2 &
O
  (Join
     ((x0; codeleft2_q00 x) = (x1; codeleft2_q10 x))
     ((codeleft2_y0 x; codeleft2_q10 x) = (y1; q11)))} <~>
codeleft2
          rapply equiv_sigma_contr.
        Defined.

        (** The next step is to reassociate the resulting double-pushout and "contract" both of them, one after the other, because they are pushouts along equivalences.  In order to do this, we need first of all to know that the resulting map from [codeleft0] to the above pushout factors through [Ocodeleft2b] via an equivalence.  Here's the equivalence: *)

        Definition Ocodeleft02b : codeleft0 <~> Ocodeleft2b.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0 <~> Ocodeleft2b
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0 <~> Ocodeleft2b
          make_equiv_contr_basedpaths.
        Defined.

        Definition Ocodeleft02 (c : codeleft0)
          : Pushout Ocodeleft2ab Ocodeleft2ac
          := pushl' Ocodeleft2ab Ocodeleft2ac (Ocodeleft02b c).

        Definition Ocodeleft02plus_02b (c : codeleft0)
          : (equiv_Ocodeleft2plus (Ocodeleft02 c)).1 = codeleft02 c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
c: codeleft0
(equiv_Ocodeleft2plus (Ocodeleft02 c)).1 =
codeleft02 c
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
c: codeleft0
(equiv_Ocodeleft2plus (Ocodeleft02 c)).1 =
codeleft02 c
          destruct c; reflexivity.
        Qed.

        (** And here we show that this equivalence is indeed a factor of the relevant map in the original pushout. *)

        Definition Ocodeleft02_02b (c : codeleft0)
          : equiv_Ocodeleft2 (to O _ (Ocodeleft02 c)) = to O _ (codeleft02 c).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
c: codeleft0
equiv_Ocodeleft2
  (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
     (Ocodeleft02 c)) = to O codeleft2 (codeleft02 c)
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
c: codeleft0
equiv_Ocodeleft2
  (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
     (Ocodeleft02 c)) = to O codeleft2 (codeleft02 c)
          destruct c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
equiv_Ocodeleft2
  (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
     (Ocodeleft02
        {|
          codeleft0_s := codeleft0_s0;
          codeleft0_y0 := codeleft0_y1;
          codeleft0_v := codeleft0_v0;
          codeleft0_q00 := codeleft0_q01;
          codeleft0_q10 := codeleft0_q11;
          codeleft0_w := codeleft0_w0;
          codeleft0_u := codeleft0_u0;
          codeleft0_d := codeleft0_d0
        |})) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          unfold equiv_Ocodeleft2.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
(equiv_O_functor O
   (equiv_sigma_contr
      (fun x : codeleft2 =>
       O
         (Join
            ((x0; codeleft2_q00 x) =
             (x1; codeleft2_q10 x))
            ((codeleft2_y0 x; codeleft2_q10 x) =
             (y1; q11)))))
 oE (equiv_O_sigma_O O
       (fun x : codeleft2 =>
        Join
          ((x0; codeleft2_q00 x) =
           (x1; codeleft2_q10 x))
          ((codeleft2_y0 x; codeleft2_q10 x) =
           (y1; q11))))^-1
 oE equiv_O_functor O equiv_Ocodeleft2plus)
  (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
     (Ocodeleft02
        {|
          codeleft0_s := codeleft0_s0;
          codeleft0_y0 := codeleft0_y1;
          codeleft0_v := codeleft0_v0;
          codeleft0_q00 := codeleft0_q01;
          codeleft0_q10 := codeleft0_q11;
          codeleft0_w := codeleft0_w0;
          codeleft0_u := codeleft0_u0;
          codeleft0_d := codeleft0_d0
        |})) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          Opaque equiv_Ocodeleft2plus.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
(equiv_O_functor O
   (equiv_sigma_contr
      (fun x : codeleft2 =>
       O
         (Join
            ((x0; codeleft2_q00 x) =
             (x1; codeleft2_q10 x))
            ((codeleft2_y0 x; codeleft2_q10 x) =
             (y1; q11)))))
 oE (equiv_O_sigma_O O
       (fun x : codeleft2 =>
        Join
          ((x0; codeleft2_q00 x) =
           (x1; codeleft2_q10 x))
          ((codeleft2_y0 x; codeleft2_q10 x) =
           (y1; q11))))^-1
 oE equiv_O_functor O equiv_Ocodeleft2plus)
  (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
     (Ocodeleft02
        {|
          codeleft0_s := codeleft0_s0;
          codeleft0_y0 := codeleft0_y1;
          codeleft0_v := codeleft0_v0;
          codeleft0_q00 := codeleft0_q01;
          codeleft0_q10 := codeleft0_q11;
          codeleft0_w := codeleft0_w0;
          codeleft0_u := codeleft0_u0;
          codeleft0_d := codeleft0_d0
        |})) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          cbn.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
O_functor O pr1
  (O_functor O
     (functor_sigma idmap
        (fun x : codeleft2 =>
         to O
           (Join
              ((x0; codeleft2_q00 x) =
               (x1; codeleft2_q10 x))
              ((codeleft2_y0 x; codeleft2_q10 x) =
               (y1; q11)))))
     (O_functor O equiv_Ocodeleft2plus
        (to O (Pushout Ocodeleft2ab Ocodeleft2ac)
           (Ocodeleft02
              {|
                codeleft0_s := codeleft0_s0;
                codeleft0_y0 := codeleft0_y1;
                codeleft0_v := codeleft0_v0;
                codeleft0_q00 := codeleft0_q01;
                codeleft0_q10 := codeleft0_q11;
                codeleft0_w := codeleft0_w0;
                codeleft0_u := codeleft0_u0;
                codeleft0_d := codeleft0_d0
              |})))) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          refine (ap _ (ap _ (to_O_natural _ _ _)) @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
O_functor O pr1
  (O_functor O
     (functor_sigma idmap
        (fun x : codeleft2 =>
         to O
           (Join
              ((x0; codeleft2_q00 x) =
               (x1; codeleft2_q10 x))
              ((codeleft2_y0 x; codeleft2_q10 x) =
               (y1; q11)))))
     (to O codeleft2plus
        (equiv_Ocodeleft2plus
           (Ocodeleft02
              {|
                codeleft0_s := codeleft0_s0;
                codeleft0_y0 := codeleft0_y1;
                codeleft0_v := codeleft0_v0;
                codeleft0_q00 := codeleft0_q01;
                codeleft0_q10 := codeleft0_q11;
                codeleft0_w := codeleft0_w0;
                codeleft0_u := codeleft0_u0;
                codeleft0_d := codeleft0_d0
              |})))) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          refine (ap _ (to_O_natural _ _ _) @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
O_functor O pr1
  (to O
     {x : codeleft2 &
     O
       (Join
          ((x0; codeleft2_q00 x) =
           (x1; codeleft2_q10 x))
          ((codeleft2_y0 x; codeleft2_q10 x) =
           (y1; q11)))}
     (functor_sigma idmap
        (fun x : codeleft2 =>
         to O
           (Join
              ((x0; codeleft2_q00 x) =
               (x1; codeleft2_q10 x))
              ((codeleft2_y0 x; codeleft2_q10 x) =
               (y1; q11))))
        (equiv_Ocodeleft2plus
           (Ocodeleft02
              {|
                codeleft0_s := codeleft0_s0;
                codeleft0_y0 := codeleft0_y1;
                codeleft0_v := codeleft0_v0;
                codeleft0_q00 := codeleft0_q01;
                codeleft0_q10 := codeleft0_q11;
                codeleft0_w := codeleft0_w0;
                codeleft0_u := codeleft0_u0;
                codeleft0_d := codeleft0_d0
              |})))) =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          refine (to_O_natural _ _ _ @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
to O codeleft2
  (functor_sigma idmap
     (fun x : codeleft2 =>
      to O
        (Join
           ((x0; codeleft2_q00 x) =
            (x1; codeleft2_q10 x))
           ((codeleft2_y0 x; codeleft2_q10 x) =
            (y1; q11))))
     (equiv_Ocodeleft2plus
        (Ocodeleft02
           {|
             codeleft0_s := codeleft0_s0;
             codeleft0_y0 := codeleft0_y1;
             codeleft0_v := codeleft0_v0;
             codeleft0_q00 := codeleft0_q01;
             codeleft0_q10 := codeleft0_q11;
             codeleft0_w := codeleft0_w0;
             codeleft0_u := codeleft0_u0;
             codeleft0_d := codeleft0_d0
           |}))).1 =
to O codeleft2
  (codeleft02
     {|
       codeleft0_s := codeleft0_s0;
       codeleft0_y0 := codeleft0_y1;
       codeleft0_v := codeleft0_v0;
       codeleft0_q00 := codeleft0_q01;
       codeleft0_q10 := codeleft0_q11;
       codeleft0_w := codeleft0_w0;
       codeleft0_u := codeleft0_u0;
       codeleft0_d := codeleft0_d0
     |})
          apply ap.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft0_s0: x0 = x1
codeleft0_y1: Y
codeleft0_v0: ap left codeleft0_s0 = r
codeleft0_q01: Q x0 codeleft0_y1
codeleft0_q11: Q x1 codeleft0_y1
codeleft0_w0: transport
  (fun x : X => Q x codeleft0_y1)
  codeleft0_s0 codeleft0_q01 =
codeleft0_q11
codeleft0_u0: glue codeleft0_q01 @
(glue codeleft0_q11)^ = r
codeleft0_d0: frobnicate r codeleft0_s0 codeleft0_y1
  codeleft0_q11
  (codeleft0_q01; codeleft0_w0;
  codeleft0_u0) = codeleft0_v0
(functor_sigma idmap
   (fun x : codeleft2 =>
    to O
      (Join
         ((x0; codeleft2_q00 x) =
          (x1; codeleft2_q10 x))
         ((codeleft2_y0 x; codeleft2_q10 x) =
          (y1; q11))))
   (equiv_Ocodeleft2plus
      (Ocodeleft02
         {|
           codeleft0_s := codeleft0_s0;
           codeleft0_y0 := codeleft0_y1;
           codeleft0_v := codeleft0_v0;
           codeleft0_q00 := codeleft0_q01;
           codeleft0_q10 := codeleft0_q11;
           codeleft0_w := codeleft0_w0;
           codeleft0_u := codeleft0_u0;
           codeleft0_d := codeleft0_d0
         |}))).1 =
codeleft02
  {|
    codeleft0_s := codeleft0_s0;
    codeleft0_y0 := codeleft0_y1;
    codeleft0_v := codeleft0_v0;
    codeleft0_q00 := codeleft0_q01;
    codeleft0_q10 := codeleft0_q11;
    codeleft0_w := codeleft0_w0;
    codeleft0_u := codeleft0_u0;
    codeleft0_d := codeleft0_d0
  |}
          rapply Ocodeleft02plus_02b.
        Qed.

        (** Thus, our pushout in which one vertex is itself a pushout can be written as a "double pushout"

[codeleft1] <- [codeleft0] -> [codeleft2b] <- [codeleft2a] -> [codeleft2c].

Since the map [codeleft0] -> [codeleft2b] is an equivalence, the pushout of the left-hand span is equivalent to [codeleft1], and thus the whole thing is equivalent to a pushout

[codeleft1] <- [codeleft2a] -> [codeleft2c]

Now we claim that the left-hand map of this span is also an equivalence.  Rather than showing this directly, it seems to be much easier to first construct *an* equivalence from [codeleft2a] to [codeleft1] and then show that it is equal (as a function) to the induced one.  Here's the equivalence: *)

        Definition Ocodeleft2a1 : Ocodeleft2a <~> codeleft1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~> codeleft1
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~> codeleft1
          etransitivity.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~> ?Goal
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
?Goal <~> codeleft1
          2:{
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
?Goal <~> codeleft1 rapply equiv_functor_sigma_id; intros s.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
s: x0 = x1
?Goal0 s <~> ap left s = r
              (** Here's frobnicate showing up again! *)
              apply frobnicate. }
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a <~>
{s : x0 = x1 &
{q0 : Q x0 ?y &
{_ : transport (fun x : X => Q x ?y) s q0 = ?q1 &
glue q0 @ (glue ?q1)^ = r}}}
          make_equiv.
        Defined.

        (** And now we check that the two are equal.  Because we used the same proof of [frobnicate] in two places, this equality becomes definitional after simply decomposing up a Sigma-type! *)
        Definition Ocodeleft2a1_through_2b0
          : Ocodeleft2a1 == codeleft01 o Ocodeleft02b^-1 o Ocodeleft2ab.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a1 ==
codeleft01 o Ocodeleft02b^-1 o Ocodeleft2ab
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
Ocodeleft2a1 ==
codeleft01 o Ocodeleft02b^-1 o Ocodeleft2ab
          intros; reflexivity.
        Defined.

        (** Now we're finally ready to prove the glue equivalence.  Since later on we'll have to compute its action on inputs from [codeleft1], we decompose it into seven steps, each of which with a corresponding computation lemma.  (These lemmas seem to be much easier to prove step-by-step than all at once if we proved the whole equivalence in a big shebang.) *)

        Definition codeglue1
          : codeleft <~> O (Pushout (O_functor O codeleft01)
                                    (O_functor O codeleft02))
        := equiv_O_pushout O _ _.

        Definition codeglue1_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue1 (to O _ (pushl (s;v))) =
            to O _ (pushl (to O _ (s; v)))
          := equiv_O_pushout_to_O_pushl _ _ _ _.

        Definition codeglue2
          : O (Pushout (O_functor O codeleft01) (O_functor O codeleft02))
        <~> O (Pushout (O_functor O codeleft01) (O_functor O Ocodeleft02)).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O
  (Pushout (O_functor O codeleft01)
     (O_functor O codeleft02)) <~>
O
  (Pushout (O_functor O codeleft01)
     (O_functor O Ocodeleft02))
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O
  (Pushout (O_functor O codeleft01)
     (O_functor O codeleft02)) <~>
O
  (Pushout (O_functor O codeleft01)
     (O_functor O Ocodeleft02))
          srefine (equiv_O_functor O
                    (equiv_inverse
                    (equiv_pushout (f := O_functor O codeleft01)
                                   (g := O_functor O Ocodeleft02)
                                   1%equiv 1%equiv equiv_Ocodeleft2 _ _))).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
1%equiv o O_functor O codeleft01 ==
O_functor O codeleft01 o 1%equiv
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
equiv_Ocodeleft2 o O_functor O Ocodeleft02 ==
O_functor O codeleft02 o 1%equiv
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
1%equiv o O_functor O codeleft01 ==
O_functor O codeleft01 o 1%equiv intros x; reflexivity.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
equiv_Ocodeleft2 o O_functor O Ocodeleft02 ==
O_functor O codeleft02 o 1%equiv apply O_indpaths; intros x.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
x: codeleft0
equiv_Ocodeleft2
  (O_functor O Ocodeleft02 (to O codeleft0 x)) =
O_functor O codeleft02 (1%equiv (to O codeleft0 x))
            abstract (rewrite !to_O_natural; apply Ocodeleft02_02b).
        Defined.

        Definition codeglue2_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue2 (to O _ (pushl (to O _ (s;v))))
            = to O _ (pushl (to O _ (s;v)))
          := to_O_equiv_natural _ _ _.

        Definition codeglue3
          : O (Pushout (O_functor O codeleft01) (O_functor O Ocodeleft02))
              <~> O (Pushout codeleft01 Ocodeleft02)
          := equiv_inverse (equiv_O_pushout O _ _).

        Definition codeglue3_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue3 (to O _ (pushl (to O _ (s;v))))
            = to O _ (pushl (s;v))
          := inverse_equiv_O_pushout_to_O_pushl _ _ _ _.

        Definition codeglue4
          : O (Pushout codeleft01 Ocodeleft02)
            <~> O (Pushout
                     (fun x : Ocodeleft2a =>
                        pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
                     Ocodeleft2ac)
          := equiv_O_functor O (equiv_inverse (equiv_pushout_assoc _ _ _ _)).

        Definition codeglue4_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue4 (to O _ (pushl (s;v)))
            = to O _ (pushl (pushl (s;v)))
          := to_O_equiv_natural _ _ _.

        Definition codeglue5
          : O (Pushout
                 (fun x : Ocodeleft2a =>
                    pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
                 Ocodeleft2ac)
        <~> O (Pushout Ocodeleft2a1 Ocodeleft2ac).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O
  (Pushout
     (fun x : Ocodeleft2a =>
      pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
     Ocodeleft2ac) <~>
O (Pushout Ocodeleft2a1 Ocodeleft2ac)
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O
  (Pushout
     (fun x : Ocodeleft2a =>
      pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
     Ocodeleft2ac) <~>
O (Pushout Ocodeleft2a1 Ocodeleft2ac)
          srefine (equiv_O_functor O
                     (equiv_inverse
                        (equiv_pushout (f := Ocodeleft2a1) (g := Ocodeleft2ac)
                                       1%equiv _ 1%equiv _ _))).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft1 <~> Pushout codeleft01 Ocodeleft02b
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
?eB o Ocodeleft2a1 ==
(fun x : Ocodeleft2a =>
 pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
o 1%equiv
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
1%equiv o Ocodeleft2ac == Ocodeleft2ac o 1%equiv
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
codeleft1 <~> Pushout codeleft01 Ocodeleft02b exact (Build_Equiv _ _ (pushl' codeleft01 Ocodeleft02b) _).
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
{|
  equiv_fun := pushl' codeleft01 Ocodeleft02b;
  equiv_isequiv :=
    isequiv_pushout_isequiv' codeleft01 Ocodeleft02b
|} o Ocodeleft2a1 ==
(fun x : Ocodeleft2a =>
 pushr' codeleft01 Ocodeleft02b (Ocodeleft2ab x))
o 1%equiv intros x.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
x: Ocodeleft2a
{|
  equiv_fun := pushl' codeleft01 Ocodeleft02b;
  equiv_isequiv :=
    isequiv_pushout_isequiv' codeleft01 Ocodeleft02b
|} (Ocodeleft2a1 x) =
pushr' codeleft01 Ocodeleft02b
  (Ocodeleft2ab (1%equiv x))
            refine (ap _ (Ocodeleft2a1_through_2b0 x) @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
x: Ocodeleft2a
{|
  equiv_fun := pushl' codeleft01 Ocodeleft02b;
  equiv_isequiv :=
    isequiv_pushout_isequiv' codeleft01 Ocodeleft02b
|} (codeleft01 (Ocodeleft02b^-1 (Ocodeleft2ab x))) =
pushr' codeleft01 Ocodeleft02b
  (Ocodeleft2ab (1%equiv x))
            refine (pglue' codeleft01 Ocodeleft02b _ @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
x: Ocodeleft2a
pushr
  (Ocodeleft02b (Ocodeleft02b^-1 (Ocodeleft2ab x))) =
pushr' codeleft01 Ocodeleft02b
  (Ocodeleft2ab (1%equiv x))
            apply ap, eisretr.
          -
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
1%equiv o Ocodeleft2ac == Ocodeleft2ac o 1%equiv intros x; reflexivity.
        Defined.

        Definition codeglue5_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue5 (to O _ (pushl (pushl (s;v))))
            = to O _ (pushl (s;v))
        := to_O_equiv_natural _ _ _.

        Definition codeglue6
          : O (Pushout Ocodeleft2a1 Ocodeleft2ac) <~> O Ocodeleft2c
          := equiv_O_functor
               O (equiv_inverse
                    (Build_Equiv _ _ (pushr' Ocodeleft2a1 Ocodeleft2ac) _)).

        Definition codeglue6_pushl (s : x0 = x1) (v : ap left s = r)
          : codeglue6 (to O _ (pushl (s;v)))
            = let z := (frobnicate r s y1 q11)^-1 v in
              to O Ocodeleft2c (Ocodeleft2ac (Build_Ocodeleft2a s z.1 z.2.1 z.2.2))
          := to_O_equiv_natural _ _ _.

        Definition codeglue7
          : O Ocodeleft2c <~> coderight (r @ glue q11).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O Ocodeleft2c <~> coderight (r @ glue q11)
        Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O Ocodeleft2c <~> coderight (r @ glue q11)
          unfold coderight, Ocodeleft2c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
O {q01 : Q x0 y1 & glue q01 @ (glue q11)^ = r} <~>
O (hfiber glue (r @ glue q11))
          apply equiv_O_functor.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
{q01 : Q x0 y1 & glue q01 @ (glue q11)^ = r} <~>
hfiber glue (r @ glue q11)
          apply equiv_functor_sigma_id; intros q01.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
x0, x1: X
r: left x0 = left x1
y1: Y
q11: Q x1 y1
q01: Q x0 y1
glue q01 @ (glue q11)^ = r <~> glue q01 = r @ glue q11
          apply equiv_moveL_pM.
        Defined.

        Definition codeglue7_to_O
                   (q01 : Q x0 y1) (u : glue q01 @ (glue q11)^ = r)
          : codeglue7 (to O _ (q01;u))
            = to O (hfiber glue (r @ glue q11))
                 (q01 ; moveL_pM (glue q11) (glue q01) r u)
          := to_O_equiv_natural _ _ _.

        Definition codeglue
          : codeleft <~> coderight (r @ glue q11)
          := codeglue7 oE
             codeglue6 oE
             codeglue5 oE
             codeglue4 oE
             codeglue3 oE
             codeglue2 oE
             codeglue1.

      End CodeGlue.

    End CodeLeft.

    (** *** Completion of codes *)

    Context `{Univalence}.
    Context (x0 : X).

    (** The equivalence [codeglue] requires a bit of massaging to put it into the form needed by the actual definition of [code] from pushout-induction and univalence. *)

    Definition ap_code_glue (x1 : X) (y1 : Y) (q11 : Q x1 y1)
      : transport (fun p : SPushout Q => left x0 = p -> Type)
                  (glue q11) codeleft
        = coderight.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
transport (fun p : SPushout Q => left x0 = p -> Type)
  (glue q11) codeleft = coderight
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
transport (fun p : SPushout Q => left x0 = p -> Type)
  (glue q11) codeleft = coderight
      apply path_arrow; intros z.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
transport (fun p : SPushout Q => left x0 = p -> Type)
  (glue q11) codeleft z = coderight z
      refine ((transport_arrow_toconst _ _ _) @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
codeleft (transport (paths (left x0)) (glue q11)^ z) =
coderight z
      apply path_universe_uncurried.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
codeleft (transport (paths (left x0)) (glue q11)^ z) <~>
coderight z
      refine (_ oE equiv_transport codeleft (transport_paths_r _ _)).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
codeleft (z @ (glue q11)^) <~> coderight z
      refine (_ oE codeglue _ q11).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
coderight ((z @ (glue q11)^) @ glue q11) <~>
coderight z
      refine (equiv_transport coderight _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
z: left x0 = right y1
(z @ (glue q11)^) @ glue q11 = z
      exact (concat_pV_p z (glue q11)).
    Defined.

    (** Here's the final definition of [code]. *)

    Definition code (p : P) (r : left x0 = p) : Type
        := spushout_ind Q (fun p => left x0 = p -> Type)
                        (@codeleft x0) (@coderight x0)
                        ap_code_glue p r.

    (** When we compute with [code], we'll need to extract from it the actual behavior of the function [codeglue].  Here's the mess of path algebra that we "naturally" get out when we try to do that; later we'll see how to deal with it. *)
    Definition code_beta_glue (x1 : X) (y1 : Y) (q11 : Q x1 y1)
               (r : left x0 = right y1)
      : ap10 (apD code (glue q11)) r
        = transport_arrow_toconst (glue q11) codeleft r
        @ path_universe_uncurried
           (@equiv_transport _ coderight ((r @ (glue q11)^) @ glue q11) r
                            (concat_pV_p r (glue q11))
            oE (codeglue (r @ (glue q11)^) q11)
            oE @equiv_transport _ codeleft
                 (transport (fun y : SPushout Q => left x0 = y) (glue q11)^ r)
                 (r @ (glue q11)^) (transport_paths_r (glue q11)^ r)).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
r: left x0 = right y1
ap10 (apD code (glue q11)) r =
transport_arrow_toconst (glue q11) codeleft r @
path_universe_uncurried
  (equiv_transport coderight
     (concat_pV_p r (glue q11))
   oE codeglue (r @ (glue q11)^) q11
   oE equiv_transport codeleft
        (transport_paths_r (glue q11)^ r))
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
r: left x0 = right y1
ap10 (apD code (glue q11)) r =
transport_arrow_toconst (glue q11) codeleft r @
path_universe_uncurried
  (equiv_transport coderight
     (concat_pV_p r (glue q11))
   oE codeglue (r @ (glue q11)^) q11
   oE equiv_transport codeleft
        (transport_paths_r (glue q11)^ r))
      refine (ap (fun h => ap10 h r)
             (spushout_ind_beta_spglue Q (fun p => left x0 = p -> Type)
                                  (@codeleft x0) (@coderight x0)
                                  ap_code_glue
                                  x1 y1 q11) @ _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0, x1: X
y1: Y
q11: Q x1 y1
r: left x0 = right y1
ap10 (ap_code_glue x1 y1 q11) r =
transport_arrow_toconst (glue q11) codeleft r @
path_universe_uncurried
  (equiv_transport coderight
     (concat_pV_p r (glue q11))
   oE codeglue (r @ (glue q11)^) q11
   oE equiv_transport codeleft
        (transport_paths_r (glue q11)^ r))
      exact (ap10_path_arrow _ _ _ _).
    Defined.

    (** ** Contractibility of codes *)

    (** To construct a center for every type of codes, we construct one in an easy case and transport it around. *)

    Definition center_code1 : code (left x0) 1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
code (left x0) 1
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
code (left x0) 1
      change (codeleft (idpath (left x0))).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
codeleft 1
      unfold codeleft.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
O (Pushout (codeleft01 1) (codeleft02 1))
      apply to, pushl.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
codeleft1 1
      unfold codeleft1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
{s : x0 = x0 & ap left s = 1}
      exact (idpath; idpath).
    Defined.

    Definition center_code (p : P) (r : left x0 = p) : code p r
      := transport (fun (pr : {p : P & left x0 = p}) => code pr.1 pr.2)
                   (path_contr (A := {p : P & left x0 = p})
                               (left x0; idpath) (p;r))
                   center_code1.

    (** As in HFLL, we first construct a contraction in the "partially general" case of an arbitrary path from left to right. *)

    Definition contraction_code_right (y1 : Y) (r : left x0 = right y1)
               (c : code (right y1) r)
      : center_code (right y1) r = c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
c: code (right y1) r
center_code (right y1) r = c
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
c: code (right y1) r
center_code (right y1) r = c
      change (coderight r) in c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
c: coderight r
center_code (right y1) r = c
      unfold coderight in c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
c: O (hfiber glue r)
center_code (right y1) r = c
      revert c; refine (O_indpaths _ _ _); intros [q01 t].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
q01: Q x0 y1
t: glue q01 = r
center_code (right y1) r =
to O (hfiber glue r) (q01; t)
      unfold center_code, center_code1.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
r: left x0 = right y1
q01: Q x0 y1
t: glue q01 = r
transport
  (fun pr : {p : P & left x0 = p} => code pr.1 pr.2)
  (path_contr (left x0; 1) (right y1; r))
  (to O (Pushout (codeleft01 1) (codeleft02 1))
     (pushl (1; 1))) = to O (hfiber glue r) (q01; t)
      (** Here's how we use the apparently-unmanageable [code_beta_glue].  First we destruct the path [t] to make things simpler. *)
      destruct t.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
transport
  (fun pr : {p : P & left x0 = p} => code pr.1 pr.2)
  (path_contr (left x0; 1) (right y1; glue q01))
  (to O (Pushout (codeleft01 1) (codeleft02 1))
     (pushl (1; 1))) =
to O (hfiber glue (glue q01)) (q01; 1)
      (** Then we notice that if we tried rewriting with [code_beta_glue] here, the unmanageable-looking result is actually fully general over the path [glue q01], so we can prove by path induction that it equals the nicer expression we'd like to see.  This is the purpose of the lemma [transport_singleton]. *)
      rewrite (transport_singleton
                 code (glue q01) _
                 (fun r => @codeglue x0 x0 r y1 q01)
                 (code_beta_glue x0 y1 q01 (glue q01))).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
transport (code (right y1)) (concat_1p (glue q01))
  (codeglue 1 q01
     (to O (Pushout (codeleft01 1) (codeleft02 1))
        (pushl (1; 1)))) =
to O (hfiber glue (glue q01)) (q01; 1)
      unfold codeglue.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
transport (code (right y1)) (concat_1p (glue q01))
  ((codeglue7 1 q01 oE codeglue6 1 q01
    oE codeglue5 1 q01 oE codeglue4 1 q01
    oE codeglue3 1 q01 oE codeglue2 1 q01
    oE codeglue1 1)
     (to O (Pushout (codeleft01 1) (codeleft02 1))
        (pushl (1; 1)))) =
to O (hfiber glue (glue q01)) (q01; 1)
      (** Now we evaluate [codeglue] step by step using our lemmas. *)
      do 6 change_apply_equiv_compose.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
transport (code (right y1)) (concat_1p (glue q01))
  (codeglue7 1 q01
     (codeglue6 1 q01
        (codeglue5 1 q01
           (codeglue4 1 q01
              (codeglue3 1 q01
                 (codeglue2 1 q01
                    (codeglue1 1
                       (to O
                          (Pushout (codeleft01 1)
                             (codeleft02 1))
                          (pushl (1; 1)))))))))) =
to O (hfiber glue (glue q01)) (q01; 1)
      rewrite codeglue1_pushl, codeglue2_pushl, codeglue3_pushl,
      codeglue4_pushl, codeglue5_pushl, codeglue6_pushl, codeglue7_to_O.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
transport (code (right y1)) (concat_1p (glue q01))
  (to O (hfiber glue (1 @ glue q01))
     ((Ocodeleft2ac 1 q01
         {|
           Ocodeleft2a_s := 1;
           Ocodeleft2a_q01 :=
             ((frobnicate 1 1 y1 q01)^-1 1).1;
           Ocodeleft2a_w :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).1;
           Ocodeleft2a_u :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).2
         |}).1;
     moveL_pM (glue q01)
       (glue
          (Ocodeleft2ac 1 q01
             {|
               Ocodeleft2a_s := 1;
               Ocodeleft2a_q01 :=
                 ((frobnicate 1 1 y1 q01)^-1 1).1;
               Ocodeleft2a_w :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).1;
               Ocodeleft2a_u :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).2
             |}).1) 1
       (Ocodeleft2ac 1 q01
          {|
            Ocodeleft2a_s := 1;
            Ocodeleft2a_q01 :=
              ((frobnicate 1 1 y1 q01)^-1 1).1;
            Ocodeleft2a_w :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).1;
            Ocodeleft2a_u :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).2
          |}).2)) =
to O (hfiber glue (glue q01)) (q01; 1)
      rewrite <- (ap_transport (concat_1p (glue q01))
                               (fun r => to O (hfiber glue r)) _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
to O (hfiber glue (glue q01))
  (transport (hfiber glue) (concat_1p (glue q01))
     ((Ocodeleft2ac 1 q01
         {|
           Ocodeleft2a_s := 1;
           Ocodeleft2a_q01 :=
             ((frobnicate 1 1 y1 q01)^-1 1).1;
           Ocodeleft2a_w :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).1;
           Ocodeleft2a_u :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).2
         |}).1;
     moveL_pM (glue q01)
       (glue
          (Ocodeleft2ac 1 q01
             {|
               Ocodeleft2a_s := 1;
               Ocodeleft2a_q01 :=
                 ((frobnicate 1 1 y1 q01)^-1 1).1;
               Ocodeleft2a_w :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).1;
               Ocodeleft2a_u :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).2
             |}).1) 1
       (Ocodeleft2ac 1 q01
          {|
            Ocodeleft2a_s := 1;
            Ocodeleft2a_q01 :=
              ((frobnicate 1 1 y1 q01)^-1 1).1;
            Ocodeleft2a_w :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).1;
            Ocodeleft2a_u :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).2
          |}).2)) =
to O (hfiber glue (glue q01)) (q01; 1)
      apply ap; unfold hfiber; rewrite transport_sigma'.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
(((Ocodeleft2ac 1 q01
     {|
       Ocodeleft2a_s := 1;
       Ocodeleft2a_q01 :=
         ((frobnicate 1 1 y1 q01)^-1 1).1;
       Ocodeleft2a_w :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).1;
       Ocodeleft2a_u :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).2
     |}).1;
 moveL_pM (glue q01)
   (glue
      (Ocodeleft2ac 1 q01
         {|
           Ocodeleft2a_s := 1;
           Ocodeleft2a_q01 :=
             ((frobnicate 1 1 y1 q01)^-1 1).1;
           Ocodeleft2a_w :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).1;
           Ocodeleft2a_u :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).2
         |}).1) 1
   (Ocodeleft2ac 1 q01
      {|
        Ocodeleft2a_s := 1;
        Ocodeleft2a_q01 :=
          ((frobnicate 1 1 y1 q01)^-1 1).1;
        Ocodeleft2a_w :=
          (((frobnicate 1 1 y1 q01)^-1 1).2).1;
        Ocodeleft2a_u :=
          (((frobnicate 1 1 y1 q01)^-1 1).2).2
      |}).2).1;
transport
  (fun x : left x0 = right y1 =>
   glue
     ((Ocodeleft2ac 1 q01
         {|
           Ocodeleft2a_s := 1;
           Ocodeleft2a_q01 :=
             ((frobnicate 1 1 y1 q01)^-1 1).1;
           Ocodeleft2a_w :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).1;
           Ocodeleft2a_u :=
             (((frobnicate 1 1 y1 q01)^-1 1).2).2
         |}).1;
     moveL_pM (glue q01)
       (glue
          (Ocodeleft2ac 1 q01
             {|
               Ocodeleft2a_s := 1;
               Ocodeleft2a_q01 :=
                 ((frobnicate 1 1 y1 q01)^-1 1).1;
               Ocodeleft2a_w :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).1;
               Ocodeleft2a_u :=
                 (((frobnicate 1 1 y1 q01)^-1 1).2).2
             |}).1) 1
       (Ocodeleft2ac 1 q01
          {|
            Ocodeleft2a_s := 1;
            Ocodeleft2a_q01 :=
              ((frobnicate 1 1 y1 q01)^-1 1).1;
            Ocodeleft2a_w :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).1;
            Ocodeleft2a_u :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).2
          |}).2).1 = x) (concat_1p (glue q01))
  ((Ocodeleft2ac 1 q01
      {|
        Ocodeleft2a_s := 1;
        Ocodeleft2a_q01 :=
          ((frobnicate 1 1 y1 q01)^-1 1).1;
        Ocodeleft2a_w :=
          (((frobnicate 1 1 y1 q01)^-1 1).2).1;
        Ocodeleft2a_u :=
          (((frobnicate 1 1 y1 q01)^-1 1).2).2
      |}).1;
  moveL_pM (glue q01)
    (glue
       (Ocodeleft2ac 1 q01
          {|
            Ocodeleft2a_s := 1;
            Ocodeleft2a_q01 :=
              ((frobnicate 1 1 y1 q01)^-1 1).1;
            Ocodeleft2a_w :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).1;
            Ocodeleft2a_u :=
              (((frobnicate 1 1 y1 q01)^-1 1).2).2
          |}).1) 1
    (Ocodeleft2ac 1 q01
       {|
         Ocodeleft2a_s := 1;
         Ocodeleft2a_q01 :=
           ((frobnicate 1 1 y1 q01)^-1 1).1;
         Ocodeleft2a_w :=
           (((frobnicate 1 1 y1 q01)^-1 1).2).1;
         Ocodeleft2a_u :=
           (((frobnicate 1 1 y1 q01)^-1 1).2).2
       |}).2).2) = (q01; 1)
      apply ap; rewrite transport_paths_r.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
((Ocodeleft2ac 1 q01
    {|
      Ocodeleft2a_s := 1;
      Ocodeleft2a_q01 :=
        ((frobnicate 1 1 y1 q01)^-1 1).1;
      Ocodeleft2a_w :=
        (((frobnicate 1 1 y1 q01)^-1 1).2).1;
      Ocodeleft2a_u :=
        (((frobnicate 1 1 y1 q01)^-1 1).2).2
    |}).1;
moveL_pM (glue q01)
  (glue
     (Ocodeleft2ac 1 q01
        {|
          Ocodeleft2a_s := 1;
          Ocodeleft2a_q01 :=
            ((frobnicate 1 1 y1 q01)^-1 1).1;
          Ocodeleft2a_w :=
            (((frobnicate 1 1 y1 q01)^-1 1).2).1;
          Ocodeleft2a_u :=
            (((frobnicate 1 1 y1 q01)^-1 1).2).2
        |}).1) 1
  (Ocodeleft2ac 1 q01
     {|
       Ocodeleft2a_s := 1;
       Ocodeleft2a_q01 :=
         ((frobnicate 1 1 y1 q01)^-1 1).1;
       Ocodeleft2a_w :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).1;
       Ocodeleft2a_u :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).2
     |}).2).2 @ concat_1p (glue q01) = 1
      (** Finally, we have another terrible-looking thing involving [frobnicate].  However, there are enough identity paths that [frobnicate] evaluates to something we can prove with path-induction. *)
      Transparent frobnicate.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
((Ocodeleft2ac 1 q01
    {|
      Ocodeleft2a_s := 1;
      Ocodeleft2a_q01 :=
        ((frobnicate 1 1 y1 q01)^-1 1).1;
      Ocodeleft2a_w :=
        (((frobnicate 1 1 y1 q01)^-1 1).2).1;
      Ocodeleft2a_u :=
        (((frobnicate 1 1 y1 q01)^-1 1).2).2
    |}).1;
moveL_pM (glue q01)
  (glue
     (Ocodeleft2ac 1 q01
        {|
          Ocodeleft2a_s := 1;
          Ocodeleft2a_q01 :=
            ((frobnicate 1 1 y1 q01)^-1 1).1;
          Ocodeleft2a_w :=
            (((frobnicate 1 1 y1 q01)^-1 1).2).1;
          Ocodeleft2a_u :=
            (((frobnicate 1 1 y1 q01)^-1 1).2).2
        |}).1) 1
  (Ocodeleft2ac 1 q01
     {|
       Ocodeleft2a_s := 1;
       Ocodeleft2a_q01 :=
         ((frobnicate 1 1 y1 q01)^-1 1).1;
       Ocodeleft2a_w :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).1;
       Ocodeleft2a_u :=
         (((frobnicate 1 1 y1 q01)^-1 1).2).2
     |}).2).2 @ concat_1p (glue q01) = 1
      simpl.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
moveL_pM (glue q01) (glue q01) 1
  ((internal_paths_rew_r
      (fun p : left x0 = right y1 =>
       p @ (glue q01)^ = 1 <~> 1 = 1)
      (internal_paths_rew_r
         (fun p : left x0 = right y1 =>
          p @ (glue q01)^ = 1 <~> 1 = 1)
         (equiv_concat_l (concat_pp_V 1 (glue q01))^ 1)
         (concat_p1 (1 @ glue q01)))
      ((concat_1p (glue q01))^ @
       (concat_p1 (1 @ glue q01))^))^-1 1) @
concat_1p (glue q01) = 1
      Opaque frobnicate.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y1: Y
q01: Q x0 y1
moveL_pM (glue q01) (glue q01) 1
  ((internal_paths_rew_r
      (fun p : left x0 = right y1 =>
       p @ (glue q01)^ = 1 <~> 1 = 1)
      (internal_paths_rew_r
         (fun p : left x0 = right y1 =>
          p @ (glue q01)^ = 1 <~> 1 = 1)
         (equiv_concat_l (concat_pp_V 1 (glue q01))^ 1)
         (concat_p1 (1 @ glue q01)))
      ((concat_1p (glue q01))^ @
       (concat_p1 (1 @ glue q01))^))^-1 1) @
concat_1p (glue q01) = 1
      destruct (glue q01); reflexivity.
    Qed.

    (** It should be possible to prove an analogous [contraction_code_left] directly, but for now we follow HFLL and ABFJ by introducing a surjectivity assumption. *)

    Definition contraction_code {y0 : Y} (q00 : Q x0 y0)
               (pr : { p : P & left x0 = p }) (c : code pr.1 pr.2)
      : center_code pr.1 pr.2 = c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y0: Y
q00: Q x0 y0
pr: {p : P & left x0 = p}
c: code pr.1 pr.2
center_code pr.1 pr.2 = c
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y0: Y
q00: Q x0 y0
pr: {p : P & left x0 = p}
c: code pr.1 pr.2
center_code pr.1 pr.2 = c
      revert c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y0: Y
q00: Q x0 y0
pr: {p : P & left x0 = p}
forall c : code pr.1 pr.2, center_code pr.1 pr.2 = c
      srefine (transport (fun pr' => forall c, center_code pr'.1 pr'.2 = c)
                         (path_contr (right y0 ; glue q00) pr) _).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y0: Y
q00: Q x0 y0
pr: {p : P & left x0 = p}
(fun pr' : {p : P & left x0 = p} =>
 forall c : code pr'.1 pr'.2,
 center_code pr'.1 pr'.2 = c) (right y0; glue q00)
      clear pr; cbn; intros c.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
y0: Y
q00: Q x0 y0
c: code (right y0) (glue q00)
center_code (right y0) (glue q00) = c
      apply contraction_code_right.
    Defined.

    Definition contr_code_inhab (inh : merely { y0 : Y & Q x0 y0 })
               (p : P) (r : left x0 = p)
      : Contr (code p r).
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
inh: merely {y0 : Y & Q x0 y0}
p: P
r: left x0 = p
Contr (code p r)
    Proof.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
inh: merely {y0 : Y & Q x0 y0}
p: P
r: left x0 = p
Contr (code p r)
      strip_truncations.
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
p: P
r: left x0 = p
inh: {y0 : Y & Q x0 y0}
Contr (code p r)
      destruct inh as [y0 q00].
X, Y: Type
Q: X -> Y -> Type
O: ReflectiveSubuniverse
isconnected_cogap: forall (x1 x3 : X) 
(y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected O
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
P:= SPushout Q: Type
H: Univalence
x0: X
p: P
r: left x0 = p
y0: Y
q00: Q x0 y0
Contr (code p r)
      exact (Build_Contr _ (center_code p r) (contraction_code q00 (p;r))).
    Defined.

    (** This version is sufficient for the classical Blakers-Massey theorem, as we'll see below, since its leg-wise connectivity hypothesis implies the above surjectivity assumption.  Anel-Biedermann-Finster-Joyal have a different method for eliminating the surjectivity assumption using a lemma about pushouts of monos also being pullbacks, though it seems to only work for coderight. *)

End GBM.

(** ** The classical Blakers-Massey Theorem *)

Instance blakers_massey `{Univalence} (m n : trunc_index)
  {X Y : Type} (Q : X -> Y -> Type)
  `{forall y, IsConnected m.+1 { x : X & Q x y } }
  `{forall x, IsConnected n.+1 { y : Y & Q x y } }
  (x : X) (y : Y)
  : IsConnMap (m +2+ n) (@spglue X Y Q x y).
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
IsConnMap (Tr (m +2+ n)) (spglue Q)
Proof.
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
IsConnMap (Tr (m +2+ n)) (spglue Q)
  intros r.
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
IsConnected (Tr (m +2+ n)) (hfiber (spglue Q) r)
  snrefine (contr_code_inhab Q (m +2+ n) _ x
                            (merely_isconnected n _) (spushr Q y) r).
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
forall (x1 x3 : X) (y2 y4 : Y) (q12 : Q x1 y2)
(q32 : Q x3 y2) (q34 : Q x3 y4),
IsConnected (Tr (m +2+ n))
  (Join ((x1; q12) = (x3; q32))
     ((y2; q32) = (y4; q34)))
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
IsConnected (Tr n.+1) {y0 : Y & Q x y0}
  1: intros; apply isconnected_join.
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
x1, x3: X
y2, y4: Y
q12: Q x1 y2
q32: Q x3 y2
q34: Q x3 y4
IsConnected (Tr m) ((x1; q12) = (x3; q32))
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
x1, x3: X
y2, y4: Y
q12: Q x1 y2
q32: Q x3 y2
q34: Q x3 y4
IsConnected (Tr n) ((y2; q32) = (y4; q34))
H: Univalence
m, n: trunc_index
X, Y: Type
Q: X -> Y -> Type
H0: forall y : Y,
IsConnected (Tr m.+1) {x : X & Q x y}
H1: forall x : X,
IsConnected (Tr n.+1) {y : Y & Q x y}
x: X
y: Y
r: spushl Q x = spushr Q y
IsConnected (Tr n.+1) {y0 : Y & Q x y0}
  all: exact _.
Defined.

(** A sigma functor is connected if its fibers are, so we have the following. *)
Definition blakers_massey_total_map `{Univalence} (m n : trunc_index)
  {X Y : Type} (Q : X -> Y -> Type)
  `{forall y, IsConnected m.+1 { x : X & Q x y } }
  `{forall x, IsConnected n.+1 { y : Y & Q x y } }
  : IsConnMap (Tr (m +2+ n)) (spushout_sjoin_map Q)
  := _.

Definition blakers_massey_po `{Univalence} (m n : trunc_index)
  {X Y Z : Type} (f : X -> Y) (g : X -> Z)
  `{H1 : !IsConnMap n.+1 f} `{H2 : !IsConnMap m.+1 g}
  : IsConnMap (m +2+ n) (pullback_corec (pglue (f:=f) (g:=g))).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
IsConnMap (Tr (m +2+ n)) (pullback_corec pglue)
Proof.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
IsConnMap (Tr (m +2+ n)) (pullback_corec pglue)
  (** We postcompose our map with an equivalence from the the pullback of the pushout of [f] and [g] to the pullback of an equivalent [SPushout] over a family [Q]. *)
  pose (Q := fun y z => {x : X & f x = y /\ g x = z}).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n)) (pullback_corec pglue)
  snapply cancelL_equiv_conn_map.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
Type
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
Pullback pushl pushr <~> ?C
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n)) (?g o pullback_corec pglue)
  1: exact (Pullback (spushl Q) (spushr Q)).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
Pullback pushl pushr <~>
Pullback (spushl Q) (spushr Q)
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n)) (?g o pullback_corec pglue)
  1: by snapply (equiv_pullback (equiv_pushout_spushout _ _)).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n))
  (equiv_pullback (equiv_pushout_spushout f g) 1 1
     (fun x0 : Y => 1) (fun x0 : Z => 1)
   o pullback_corec pglue)
  (** Next we precompose with the equivalence from the total space of [Q] to [X]. *)
  rapply (cancelR_conn_map _ (equiv_double_fibration_replacement f g)^-1%equiv).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n))
  (fun
     x : {y : Y &
         {z : Z & {x : X & (f x = y) * (g x = z)}}} =>
   equiv_pullback (equiv_pushout_spushout f g) 1 1
     (fun x0 : Y => 1) (fun x0 : Z => 1)
     (pullback_corec pglue
        ((equiv_double_fibration_replacement f g)^-1%equiv
           x)))
  (** Next we prove that this composition is homotopic to [spushout_sjoin_map Q]. *)
  snapply (conn_map_homotopic _ (spushout_sjoin_map Q)).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
spushout_sjoin_map Q ==
(fun
   x : {y : Y &
       {z : Z & {x : X & (f x = y) * (g x = z)}}} =>
 equiv_pullback (equiv_pushout_spushout f g) 1 1
   (fun x0 : Y => 1) (fun x0 : Z => 1)
   (pullback_corec pglue
      ((equiv_double_fibration_replacement f g)^-1%equiv
         x)))
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n)) (spushout_sjoin_map Q)
  {
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
spushout_sjoin_map Q ==
(fun
   x : {y : Y &
       {z : Z & {x : X & (f x = y) * (g x = z)}}} =>
 equiv_pullback (equiv_pushout_spushout f g) 1 1
   (fun x0 : Y => 1) (fun x0 : Z => 1)
   (pullback_corec pglue
      ((equiv_double_fibration_replacement f g)^-1%equiv
         x))) intros [y [z [x [[] []]]]].
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
spushout_sjoin_map Q (f x; g x; x; (1, 1)) =
equiv_pullback (equiv_pushout_spushout f g) 1 1
  (fun x0 : Y => 1) (fun x0 : Z => 1)
  (pullback_corec pglue
     ((equiv_double_fibration_replacement f g)^-1%equiv
        (f x; g x; x; (1, 1))))
    snapply (path_sigma' _ 1 (path_sigma' _ 1 _)); simpl; symmetry.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
match
  ap
    (functor_coeq
       (fun x : X => ((f x, g x); x; (1, 1)))
       (functor_sum idmap idmap) (fun x : X => 1)
       (fun x : X => 1)) (pglue x) @ 1 in (_ = a)
  return (spushl Q (f x) = a)
with
| 1 => 1
end = spglue Q (x; (1, 1))
    lhs napply concat_1p.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
ap
  (functor_coeq (fun x : X => ((f x, g x); x; (1, 1)))
     (functor_sum idmap idmap) (fun x : X => 1)
     (fun x : X => 1)) (pglue x) @ 1 =
spglue Q (x; (1, 1))
    lhs napply concat_p1.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
ap
  (functor_coeq (fun x : X => ((f x, g x); x; (1, 1)))
     (functor_sum idmap idmap) (fun x : X => 1)
     (fun x : X => 1)) (pglue x) =
spglue Q (x; (1, 1))
    lhs napply functor_coeq_beta_cglue.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
(ap coeq 1 @ cglue ((f x, g x); x; (1, 1))) @
ap coeq 1^ = spglue Q (x; (1, 1))
    lhs napply concat_p1.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
z: Z
x: X
ap coeq 1 @ cglue ((f x, g x); x; (1, 1)) =
spglue Q (x; (1, 1))
    napply concat_1p. }
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
IsConnMap (Tr (m +2+ n)) (spushout_sjoin_map Q)
  rapply blakers_massey_total_map.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
forall y : Z, IsConnected (Tr m.+1) {x : Y & Q x y}
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
forall x : Y, IsConnected (Tr n.+1) {y : Z & Q x y}
  (** What's left is to check that the partial total spaces of [Q] are connected, which we get since [f] and [g] are connected maps. We just have to strip off the irrelevant parts of [Q] to get the hfiber in each case. *)
  -
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
forall y : Z, IsConnected (Tr m.+1) {x : Y & Q x y} intros z.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
z: Z
IsConnected (Tr m.+1) {x : Y & Q x z}
    nrefine (isconnected_equiv' _ _ _ (H2 z)).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
z: Z
hfiber g z <~> {x : Y & Q x z}
    make_equiv_contr_basedpaths.
  -
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
forall x : Y, IsConnected (Tr n.+1) {y : Z & Q x y} intros y.
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
IsConnected (Tr n.+1) {y0 : Z & Q y y0}
    nrefine (isconnected_equiv' _ _ _ (H1 y)).
H: Univalence
m, n: trunc_index
X, Y, Z: Type
f: X -> Y
g: X -> Z
H1: IsConnMap (Tr n.+1) f
H2: IsConnMap (Tr m.+1) g
Q:= fun (y : Y) (z : Z) =>
{x : X & (f x = y) * (g x = z)}: Y -> Z -> Type
y: Y
hfiber f y <~> {y0 : Z & Q y y0}
    make_equiv_contr_basedpaths.
Defined.

(** ** The Freudenthal Suspension Theorem *)

(** The Freudenthal suspension theorem is a fairly trivial corollary of the Blakers-Massey theorem.  It says that [merid : X -> North = South] is highly connected. *)
Instance freudenthal `{Univalence} (n : trunc_index)
           (X : Type@{u}) `{IsConnected n.+1 X}
  : IsConnMap (n +2+ n) (@merid X).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) merid
Proof.
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n)) merid
  (* If we post-compose [merid : X -> North = South] with an equivalence [North = South <~> P], where [P] is the pullback of the inclusions [Unit -> Susp X] hitting [North] and [South], we get the canonical comparison map [X -> P] whose connectivity follows from the Blakers-Massey theorem. *)
  rapply (cancelL_equiv_conn_map _ _ (equiv_pullback_unit_unit_paths _ _)^-1%equiv).
H: Univalence
n: trunc_index
X: Type
H0: IsConnected (Tr n.+1) X
IsConnMap (Tr (n +2+ n))
  (fun x : X =>
   (equiv_pullback_unit_unit_paths pushl pushr)^-1%equiv
     (merid x))
  rapply blakers_massey_po.
Defined.