From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
Require Import Diagrams.Diagram.
Require Import Diagrams.DDiagram.
Require Import Diagrams.Span.
Require Import Diagrams.Cocone.
Require Import Colimits.Colimit.
Require Import Colimits.Colimit_Pushout.
Require Import Colimits.Colimit_Flattening.

(** * Pushout case *)

(** We deduce the flattening lemma for pushouts from the flattening lemma for general colimits. This pushout is defined as the colimit of a span and is not the pushout that appears elsewhere in the library. The flattening lemma for the pushout that appears elsewhere in the library is in Colimits/Pushout.v. *)

Section POCase.
  Context `{Univalence} {A B C} {f: A -> B} {g: A -> C}.

  Context (A0 : A -> Type) (B0 : B -> Type) (C0 : C -> Type)
          (f0 : forall x, A0 x <~> B0 (f x)) (g0 : forall x, A0 x <~> C0 (g x)).

  Definition POCase_P : PO f g -> Type.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO f g -> Type
  Proof.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO f g -> Type
    simple refine (PO_rec Type B0 C0 _).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
B0 o f == C0 o g
    cbn; intro x.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
B0 (f x) = C0 (g x) eapply path_universe_uncurried.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
B0 (f x) <~> C0 (g x)
    etransitivity.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
B0 (f x) <~> ?Goal
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
?Goal <~> C0 (g x)
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
B0 (f x) <~> ?Goal symmetry.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
?Goal <~> B0 (f x) apply f0.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
A0 x <~> C0 (g x) apply g0.
  Defined.

  Definition POCase_E : DDiagram (span f g).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
DDiagram (span f g)
  Proof.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
DDiagram (span f g)
    simple refine (Build_Diagram _ _ _); cbn.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{i : Unit + Bool &
match i with
| inl _ => A
| inr true => B
| inr false => C
end} -> Type
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall
(i : {i : Unit + Bool &
     match i with
     | inl _ => A
     | inr true => B
     | inr false => C
     end})
(j : {i0 : Unit + Bool &
     match i0 with
     | inl _ => A
     | inr true => B
     | inr false => C
     end}),
{g1
: match i.1 with
  | inl _ =>
      fun X : Unit + Bool =>
      match X with
      | inl _ => Empty
      | inr _ => Unit
      end
  | inr _ => fun X : Unit + Bool => match X with
                                    | inl _ | _ => Empty
                                    end
  end j.1
&
match
  i.1 as s
  return
    (forall j0 : Unit + Bool,
     match s with
     | inl _ =>
         fun X : Unit + Bool =>
         match X with
         | inl _ => Empty
         | inr _ => Unit
         end
     | inr _ => fun X : Unit + Bool => match X with
                                       | inl _ | _ => Empty
                                       end
     end j0 ->
     match s with
     | inl _ => A
     | inr true => B
     | inr false => C
     end -> match j0 with
            | inl _ => A
            | inr true => B
            | inr false => C
            end)
with
| inl _ =>
    fun j0 : Unit + Bool =>
    match
      j0 as s
      return
        (match s with
         | inl _ => Empty
         | inr _ => Unit
         end ->
         A -> match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
    with
    | inl _ => fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
    | inr b =>
        fun u0 : Unit =>
        match b as b0 return (Unit -> A -> if b0 then B else C) with
        | true => unit_name f
        | false => unit_name g
        end u0
    end
| inr b =>
    fun j0 : Unit + Bool =>
    match
      j0 as s
      return
        (match s with
         | inl _ | _ => Empty
         end ->
         (if b then B else C) ->
         match s with
         | inl _ => A
         | inr true => B
         | inr false => C
         end)
    with
    | inl _ =>
        fun (u0 : Empty) (_ : if b then B else C) =>
        Empty_rect (fun _ : Empty => A) u0
    | inr b0 =>
        fun (u : Empty) (_ : if b then B else C) =>
        Empty_rect (fun _ : Empty => if b0 then B else C) u
    end
end j.1 g1 i.2 = j.2} -> ?Goal i -> ?Goal j
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{i : Unit + Bool &
match i with
| inl _ => A
| inr true => B
| inr false => C
end} -> Type intros [[] x]; revert x.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
u: Unit
A -> Type
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
b: Bool
(if b then B else C) -> Type 
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
u: Unit
A -> Type exact A0.
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
b: Bool
(if b then B else C) -> Type destruct b; assumption.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall
(i : {i : Unit + Bool &
     match i with
     | inl _ => A
     | inr true => B
     | inr false => C
     end})
(j : {i0 : Unit + Bool &
     match i0 with
     | inl _ => A
     | inr true => B
     | inr false => C
     end}),
{g1
: match i.1 with
  | inl _ =>
      fun X : Unit + Bool =>
      match X with
      | inl _ => Empty
      | inr _ => Unit
      end
  | inr _ => fun X : Unit + Bool => match X with
                                    | inl _ | _ => Empty
                                    end
  end j.1
&
match
  i.1 as s
  return
    (forall j0 : Unit + Bool,
     match s with
     | inl _ =>
         fun X : Unit + Bool =>
         match X with
         | inl _ => Empty
         | inr _ => Unit
         end
     | inr _ => fun X : Unit + Bool => match X with
                                       | inl _ | _ => Empty
                                       end
     end j0 ->
     match s with
     | inl _ => A
     | inr true => B
     | inr false => C
     end -> match j0 with
            | inl _ => A
            | inr true => B
            | inr false => C
            end)
with
| inl _ =>
    fun j0 : Unit + Bool =>
    match
      j0 as s
      return
        (match s with
         | inl _ => Empty
         | inr _ => Unit
         end ->
         A -> match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
    with
    | inl _ => fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
    | inr b =>
        fun u0 : Unit =>
        match b as b0 return (Unit -> A -> if b0 then B else C) with
        | true => unit_name f
        | false => unit_name g
        end u0
    end
| inr b =>
    fun j0 : Unit + Bool =>
    match
      j0 as s
      return
        (match s with
         | inl _ | _ => Empty
         end ->
         (if b then B else C) ->
         match s with
         | inl _ => A
         | inr true => B
         | inr false => C
         end)
    with
    | inl _ =>
        fun (u0 : Empty) (_ : if b then B else C) =>
        Empty_rect (fun _ : Empty => A) u0
    | inr b0 =>
        fun (u : Empty) (_ : if b then B else C) =>
        Empty_rect (fun _ : Empty => if b0 then B else C) u
    end
end j.1 g1 i.2 = j.2} ->
(fun
   X : {i0 : Unit + Bool &
       match i0 with
       | inl _ => A
       | inr true => B
       | inr false => C
       end} =>
 (fun proj1 : Unit + Bool =>
  match
    proj1 as s
    return
      (match s with
       | inl _ => A
       | inr true => B
       | inr false => C
       end -> Type)
  with
  | inl u => unit_name (fun x : A => A0 x) u
  | inr b =>
      (fun (b0 : Bool) (x : if b0 then B else C) =>
       match b0 as b1 return ((if b1 then B else C) -> Type) with
       | true => B0
       | false => C0
       end x) b
  end) X.1 X.2) i ->
(fun
   X : {i0 : Unit + Bool &
       match i0 with
       | inl _ => A
       | inr true => B
       | inr false => C
       end} =>
 (fun proj1 : Unit + Bool =>
  match
    proj1 as s
    return
      (match s with
       | inl _ => A
       | inr true => B
       | inr false => C
       end -> Type)
  with
  | inl u => unit_name (fun x : A => A0 x) u
  | inr b =>
      (fun (b0 : Bool) (x : if b0 then B else C) =>
       match b0 as b1 return ((if b1 then B else C) -> Type) with
       | true => B0
       | false => C0
       end x) b
  end) X.1 X.2) j intros [[[]|[]] x] [[[]|[]] y]; cbn; intros [[] p].
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
y: B
p: f x = y
A0 x -> B0 y
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
y: C
p: g x = y
A0 x -> C0 y
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
y: B
p: f x = y
A0 x -> B0 y exact (fun y => p # (f0 x y)).
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: A
y: C
p: g x = y
A0 x -> C0 y exact (fun y => p # (g0 x y)).
  Defined.

  #[export] Instance POCase_HE : Equifibered POCase_E.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Equifibered POCase_E
  Proof.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Equifibered POCase_E
    apply Build_Equifibered.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall (i j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i j)
(x : span f g i), IsEquiv (POCase_E _f (g1; 1))
    intros [[]|[]] [[]|[]] [] x; compute.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: span f g (inl tt)
IsEquiv (fun y : A0 x => f0 x y)
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: span f g (inl tt)
IsEquiv (fun y : A0 x => g0 x y)
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: span f g (inl tt)
IsEquiv (fun y : A0 x => f0 x y) exact (equiv_isequiv (f0 x)).
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: span f g (inl tt)
IsEquiv (fun y : A0 x => g0 x y) exact (equiv_isequiv (g0 x)).
  Defined.

  Definition PO_flattening
    : PO (functor_sigma f f0) (functor_sigma g g0) <~> exists x, POCase_P x.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) <~>
{x : PO f g & POCase_P x}
  Proof.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) <~>
{x : PO f g & POCase_P x}
    transitivity (Colimit (diagram_sigma POCase_E)).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) <~>
Colimit (diagram_sigma POCase_E)
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Colimit (diagram_sigma POCase_E) <~> {x : PO f g & POCase_P x}
    {
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) <~>
Colimit (diagram_sigma POCase_E) apply equiv_path.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
PO (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) =
Colimit (diagram_sigma POCase_E)
      unfold PO; apply ap.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
span (functor_sigma f (fun x : A => f0 x))
  (functor_sigma g (fun x : A => g0 x)) =
diagram_sigma POCase_E
      srapply path_diagram; cbn.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall i : Unit + Bool,
match i with
| inl _ => {x : _ & A0 x}
| inr true => {x : _ & B0 x}
| inr false => {x : _ & C0 x}
end =
{x : match i with
     | inl _ => A
     | inr true => B
     | inr false => C
     end
&
match
  i as s
  return
    (match s with
     | inl _ => A
     | inr true => B
     | inr false => C
     end -> Type)
with
| inl _ => fun x0 : A => A0 x0
| inr b =>
    fun x0 : if b then B else C =>
    match b as b0 return ((if b0 then B else C) -> Type) with
    | true => B0
    | false => C0
    end x0
end x}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall (i j : Unit + Bool)
(g1 : match i with
      | inl _ =>
          fun X : Unit + Bool =>
          match X with
          | inl _ => Empty
          | inr _ => Unit
          end
      | inr _ => fun X : Unit + Bool => match X with
                                        | inl _ | _ => Empty
                                        end
      end j)
(x : match i with
     | inl _ => {x : _ & A0 x}
     | inr true => {x : _ & B0 x}
     | inr false => {x : _ & C0 x}
     end),
transport idmap (?Goal0 j)
  (match
     i as s
     return
       (forall j0 : Unit + Bool,
        match s with
        | inl _ =>
            fun X : Unit + Bool =>
            match X with
            | inl _ => Empty
            | inr _ => Unit
            end
        | inr _ =>
            fun X : Unit + Bool => match X with
                                   | inl _ | _ => Empty
                                   end
        end j0 ->
        match s with
        | inl _ => {x : _ & A0 x}
        | inr true => {x : _ & B0 x}
        | inr false => {x : _ & C0 x}
        end ->
        match j0 with
        | inl _ => {x : _ & A0 x}
        | inr true => {x : _ & B0 x}
        | inr false => {x : _ & C0 x}
        end)
   with
   | inl _ =>
       fun j0 : Unit + Bool =>
       match
         j0 as s
         return
           (match s with
            | inl _ => Empty
            | inr _ => Unit
            end ->
            {x : _ & A0 x} ->
            match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end)
       with
       | inl _ =>
           fun (u1 : Empty) (_ : {x : _ & A0 x}) =>
           Empty_rect (fun _ : Empty => {x : _ & A0 x}) u1
       | inr b =>
           fun u0 : Unit =>
           match
             b as b0
             return
               (Unit ->
                {x : _ & A0 x} ->
                if b0 then {x : _ & B0 x} else {x : _ & C0 x})
           with
           | true => unit_name (functor_sigma f (fun x0 : A => f0 x0))
           | false => unit_name (functor_sigma g (fun x0 : A => g0 x0))
           end u0
       end
   | inr b =>
       fun j0 : Unit + Bool =>
       match
         j0 as s
         return
           (match s with
            | inl _ | _ => Empty
            end ->
            (if b then {x : _ & B0 x} else {x : _ & C0 x}) ->
            match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end)
       with
       | inl _ =>
           fun (u0 : Empty)
             (_ : if b then {x : _ & B0 x} else {x : _ & C0 x}) =>
           Empty_rect (fun _ : Empty => {x : _ & A0 x}) u0
       | inr b0 =>
           fun (u : Empty) (_ : if b then {x : _ & B0 x} else {x : _ & C0 x}) =>
           Empty_rect
             (fun _ : Empty => if b0 then {x : _ & B0 x} else {x : _ & C0 x})
             u
       end
   end j g1 x) =
(match
   i as s
   return
     (forall j0 : Unit + Bool,
      match s with
      | inl _ =>
          fun X : Unit + Bool =>
          match X with
          | inl _ => Empty
          | inr _ => Unit
          end
      | inr _ => fun X : Unit + Bool => match X with
                                        | inl _ | _ => Empty
                                        end
      end j0 ->
      match s with
      | inl _ => A
      | inr true => B
      | inr false => C
      end -> match j0 with
             | inl _ => A
             | inr true => B
             | inr false => C
             end)
 with
 | inl _ =>
     fun j0 : Unit + Bool =>
     match
       j0 as s
       return
         (match s with
          | inl _ => Empty
          | inr _ => Unit
          end ->
          A -> match s with
               | inl _ => A
               | inr true => B
               | inr false => C
               end)
     with
     | inl _ =>
         fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
     | inr b =>
         fun u0 : Unit =>
         match b as b0 return (Unit -> A -> if b0 then B else C) with
         | true => unit_name f
         | false => unit_name g
         end u0
     end
 | inr b =>
     fun j0 : Unit + Bool =>
     match
       j0 as s
       return
         (match s with
          | inl _ | _ => Empty
          end ->
          (if b then B else C) ->
          match s with
          | inl _ => A
          | inr true => B
          | inr false => C
          end)
     with
     | inl _ =>
         fun (u0 : Empty) (_ : if b then B else C) =>
         Empty_rect (fun _ : Empty => A) u0
     | inr b0 =>
         fun (u : Empty) (_ : if b then B else C) =>
         Empty_rect (fun _ : Empty => if b0 then B else C) u
     end
 end j g1 (transport idmap (?Goal0 i) x).1;
match
  i as s
  return
    (forall
     (proj2 : match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
     (j0 : {i0 : Unit + Bool &
           match i0 with
           | inl _ => A
           | inr true => B
           | inr false => C
           end}),
     {g2
     : match s with
       | inl _ =>
           fun X : Unit + Bool =>
           match X with
           | inl _ => Empty
           | inr _ => Unit
           end
       | inr _ =>
           fun X : Unit + Bool => match X with
                                  | inl _ | _ => Empty
                                  end
       end j0.1
     &
     match
       s as s0
       return
         (forall j1 : Unit + Bool,
          match s0 with
          | inl _ =>
              fun X : Unit + Bool =>
              match X with
              | inl _ => Empty
              | inr _ => Unit
              end
          | inr _ =>
              fun X : Unit + Bool => match X with
                                     | inl _ | _ => Empty
                                     end
          end j1 ->
          match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end ->
          match j1 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end)
     with
     | inl _ =>
         fun j1 : Unit + Bool =>
         match
           j1 as s0
           return
             (match s0 with
              | inl _ => Empty
              | inr _ => Unit
              end ->
              A ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             match b as b0 return (Unit -> A -> if b0 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end u0
         end
     | inr b =>
         fun j1 : Unit + Bool =>
         match
           j1 as s0
           return
             (match s0 with
              | inl _ | _ => Empty
              end ->
              (if b then B else C) ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u0 : Empty) (_ : if b then B else C) =>
             Empty_rect (fun _ : Empty => A) u0
         | inr b0 =>
             fun (u : Empty) (_ : if b then B else C) =>
             Empty_rect (fun _ : Empty => if b0 then B else C) u
         end
     end j0.1 g2 proj2 = j0.2} ->
     match
       s as s0
       return
         (match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end -> Type)
     with
     | inl _ => fun x0 : A => A0 x0
     | inr b =>
         fun x0 : if b then B else C =>
         match b as b0 return ((if b0 then B else C) -> Type) with
         | true => B0
         | false => C0
         end x0
     end proj2 ->
     match
       j0.1 as s0
       return
         (match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end -> Type)
     with
     | inl _ => fun x0 : A => A0 x0
     | inr b =>
         fun x0 : if b then B else C =>
         match b as b0 return ((if b0 then B else C) -> Type) with
         | true => B0
         | false => C0
         end x0
     end j0.2)
with
| inl tt =>
    fun (x0 : A)
      (j0 : {i0 : Unit + Bool &
            match i0 with
            | inl _ => A
            | inr true => B
            | inr false => C
            end}) =>
    match
      j0.1 as s
      return
        (forall
         proj2 : match s with
                 | inl _ => A
                 | inr true => B
                 | inr false => C
                 end,
         {g2 : match s with
               | inl _ => Empty
               | inr _ => Unit
               end
         &
         match
           s as s0
           return
             (match s0 with
              | inl _ => Empty
              | inr _ => Unit
              end ->
              A ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             match b as b0 return (Unit -> A -> if b0 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end u0
         end g2 x0 = proj2} ->
         A0 x0 ->
         match
           s as s0
           return
             (match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end -> Type)
         with
         | inl _ => fun x1 : A => A0 x1
         | inr b =>
             fun x1 : if b then B else C =>
             match b as b0 return ((if b0 then B else C) -> Type) with
             | true => B0
             | false => C0
             end x1
         end proj2)
    with
    | inl tt =>
        fun (y : A)
          (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
        match
          X.1 as e
          return (Empty_rect (fun _ : Empty => A) e = y -> A0 x0 -> A0 y)
        with
        end X.2
    | inr b =>
        match
          b as b0
          return
            (forall proj2 : if b0 then B else C,
             {g2 : Unit &
             match b0 as b1 return (Unit -> A -> if b1 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end g2 x0 = proj2} ->
             A0 x0 ->
             match b0 as b1 return ((if b1 then B else C) -> Type) with
             | true => B0
             | false => C0
             end proj2)
        with
        | true =>
            fun (y : B) (X : {_ : Unit & f x0 = y}) =>
            match X.1 with
            | tt =>
                fun (p : f x0 = y) (y0 : A0 x0) => transport B0 p (f0 x0 y0)
            end X.2
        | false =>
            fun (y : C) (X : {_ : Unit & g x0 = y}) =>
            match X.1 with
            | tt =>
                fun (p : g x0 = y) (y0 : A0 x0) => transport C0 p (g0 x0 y0)
            end X.2
        end
    end j0.2
| inr b =>
    match
      b as b0
      return
        (forall (proj2 : if b0 then B else C)
         (j0 : {i0 : Unit + Bool &
               match i0 with
               | inl _ => A
               | inr true => B
               | inr false => C
               end}),
         {g2 : match j0.1 with
               | inl _ | _ => Empty
               end
         &
         match
           j0.1 as s
           return
             (match s with
              | inl _ | _ => Empty
              end ->
              (if b0 then B else C) ->
              match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u0 : Empty) (_ : if b0 then B else C) =>
             Empty_rect (fun _ : Empty => A) u0
         | inr b1 =>
             fun (u : Empty) (_ : if b0 then B else C) =>
             Empty_rect (fun _ : Empty => if b1 then B else C) u
         end g2 proj2 = j0.2} ->
         match b0 as b1 return ((if b1 then B else C) -> Type) with
         | true => B0
         | false => C0
         end proj2 ->
         match
           j0.1 as s
           return
             (match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end -> Type)
         with
         | inl _ => fun x0 : A => A0 x0
         | inr b1 =>
             fun x0 : if b1 then B else C =>
             match b1 as b2 return ((if b2 then B else C) -> Type) with
             | true => B0
             | false => C0
             end x0
         end j0.2)
    with
    | true =>
        fun (x0 : B)
          (j0 : {i0 : Unit + Bool &
                match i0 with
                | inl _ => A
                | inr true => B
                | inr false => C
                end}) =>
        match
          j0.1 as s
          return
            (forall
             proj2 : match s with
                     | inl _ => A
                     | inr true => B
                     | inr false => C
                     end,
             {g2 : match s with
                   | inl _ | _ => Empty
                   end
             &
             match
               s as s0
               return
                 (match s0 with
                  | inl _ | _ => Empty
                  end ->
                  B ->
                  match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end)
             with
             | inl _ =>
                 fun (u0 : Empty) (_ : B) =>
                 Empty_rect (fun _ : Empty => A) u0
             | inr b0 =>
                 fun (u : Empty) (_ : B) =>
                 Empty_rect (fun _ : Empty => if b0 then B else C) u
             end g2 x0 = proj2} ->
             B0 x0 ->
             match
               s as s0
               return
                 (match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b0 =>
                 fun x1 : if b0 then B else C =>
                 match b0 as b1 return ((if b1 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x1
             end proj2)
        with
        | inl tt =>
            fun (y : A)
              (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
            match
              X.1 as e
              return (Empty_rect (fun _ : Empty => A) e = y -> B0 x0 -> A0 y)
            with
            end X.2
        | inr b0 =>
            match
              b0 as b1
              return
                (forall proj2 : if b1 then B else C,
                 {g2 : Empty &
                 Empty_rect (fun _ : Empty => if b1 then B else C) g2 = proj2} ->
                 B0 x0 ->
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end proj2)
            with
            | true =>
                fun (y : B)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => B) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => B) e = y -> B0 x0 -> B0 y)
                with
                end X.2
            | false =>
                fun (y : C)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => C) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => C) e = y -> B0 x0 -> C0 y)
                with
                end X.2
            end
        end j0.2
    | false =>
        fun (x0 : C)
          (j0 : {i0 : Unit + Bool &
                match i0 with
                | inl _ => A
                | inr true => B
                | inr false => C
                end}) =>
        match
          j0.1 as s
          return
            (forall
             proj2 : match s with
                     | inl _ => A
                     | inr true => B
                     | inr false => C
                     end,
             {g2 : match s with
                   | inl _ | _ => Empty
                   end
             &
             match
               s as s0
               return
                 (match s0 with
                  | inl _ | _ => Empty
                  end ->
                  C ->
                  match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end)
             with
             | inl _ =>
                 fun (u0 : Empty) (_ : C) =>
                 Empty_rect (fun _ : Empty => A) u0
             | inr b0 =>
                 fun (u : Empty) (_ : C) =>
                 Empty_rect (fun _ : Empty => if b0 then B else C) u
             end g2 x0 = proj2} ->
             C0 x0 ->
             match
               s as s0
               return
                 (match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b0 =>
                 fun x1 : if b0 then B else C =>
                 match b0 as b1 return ((if b1 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x1
             end proj2)
        with
        | inl tt =>
            fun (y : A)
              (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
            match
              X.1 as e
              return (Empty_rect (fun _ : Empty => A) e = y -> C0 x0 -> A0 y)
            with
            end X.2
        | inr b0 =>
            match
              b0 as b1
              return
                (forall proj2 : if b1 then B else C,
                 {g2 : Empty &
                 Empty_rect (fun _ : Empty => if b1 then B else C) g2 = proj2} ->
                 C0 x0 ->
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end proj2)
            with
            | true =>
                fun (y : B)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => B) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => B) e = y -> C0 x0 -> B0 y)
                with
                end X.2
            | false =>
                fun (y : C)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => C) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => C) e = y -> C0 x0 -> C0 y)
                with
                end X.2
            end
        end j0.2
    end
end (transport idmap (?Goal0 i) x).1
  (j;
  match
    i as s
    return
      (forall j0 : Unit + Bool,
       match s with
       | inl _ =>
           fun X : Unit + Bool =>
           match X with
           | inl _ => Empty
           | inr _ => Unit
           end
       | inr _ =>
           fun X : Unit + Bool => match X with
                                  | inl _ | _ => Empty
                                  end
       end j0 ->
       match s with
       | inl _ => A
       | inr true => B
       | inr false => C
       end -> match j0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
  with
  | inl _ =>
      fun j0 : Unit + Bool =>
      match
        j0 as s
        return
          (match s with
           | inl _ => Empty
           | inr _ => Unit
           end ->
           A ->
           match s with
           | inl _ => A
           | inr true => B
           | inr false => C
           end)
      with
      | inl _ =>
          fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
      | inr b =>
          fun u0 : Unit =>
          match b as b0 return (Unit -> A -> if b0 then B else C) with
          | true => unit_name f
          | false => unit_name g
          end u0
      end
  | inr b =>
      fun j0 : Unit + Bool =>
      match
        j0 as s
        return
          (match s with
           | inl _ | _ => Empty
           end ->
           (if b then B else C) ->
           match s with
           | inl _ => A
           | inr true => B
           | inr false => C
           end)
      with
      | inl _ =>
          fun (u0 : Empty) (_ : if b then B else C) =>
          Empty_rect (fun _ : Empty => A) u0
      | inr b0 =>
          fun (u : Empty) (_ : if b then B else C) =>
          Empty_rect (fun _ : Empty => if b0 then B else C) u
      end
  end j g1 (transport idmap (?Goal0 i) x).1) (g1; 1)
  (transport idmap (?Goal0 i) x).2)
      -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall i : Unit + Bool,
match i with
| inl _ => {x : _ & A0 x}
| inr true => {x : _ & B0 x}
| inr false => {x : _ & C0 x}
end =
{x : match i with
     | inl _ => A
     | inr true => B
     | inr false => C
     end
&
match
  i as s
  return
    (match s with
     | inl _ => A
     | inr true => B
     | inr false => C
     end -> Type)
with
| inl _ => fun x0 : A => A0 x0
| inr b =>
    fun x0 : if b then B else C =>
    match b as b0 return ((if b0 then B else C) -> Type) with
    | true => B0
    | false => C0
    end x0
end x} intros [|[]]; cbn.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
u: Unit
{x : _ & A0 x} = {x : A & A0 x}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{x : _ & B0 x} = {x : B & B0 x}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{x : _ & C0 x} = {x : C & C0 x} all: reflexivity.
      -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall (i j : Unit + Bool)
(g1 : match i with
      | inl _ =>
          fun X : Unit + Bool =>
          match X with
          | inl _ => Empty
          | inr _ => Unit
          end
      | inr _ => fun X : Unit + Bool => match X with
                                        | inl _ | _ => Empty
                                        end
      end j)
(x : match i with
     | inl _ => {x : _ & A0 x}
     | inr true => {x : _ & B0 x}
     | inr false => {x : _ & C0 x}
     end),
transport idmap
  ((fun i0 : Unit + Bool =>
    match
      i0 as s
      return
        (match s with
         | inl _ => {x : _ & A0 x}
         | inr true => {x : _ & B0 x}
         | inr false => {x : _ & C0 x}
         end =
         {x0 : match s with
               | inl _ => A
               | inr true => B
               | inr false => C
               end
         &
         match
           s as s0
           return
             (match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end -> Type)
         with
         | inl _ => fun x1 : A => A0 x1
         | inr b =>
             fun x1 : if b then B else C =>
             match b as b0 return ((if b0 then B else C) -> Type) with
             | true => B0
             | false => C0
             end x1
         end x0})
    with
    | inl u => unit_name (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
    | inr b =>
        (fun b0 : Bool =>
         match
           b0 as b1
           return
             ((if b1 then {x : _ & B0 x} else {x : _ & C0 x}) =
              {x0 : if b1 then B else C &
              match b1 as b2 return ((if b2 then B else C) -> Type) with
              | true => B0
              | false => C0
              end x0})
         with
         | true => 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
         | false => 1 : {x : _ & C0 x} = {x0 : C & C0 x0}
         end) b
    end) j)
  (match
     i as s
     return
       (forall j0 : Unit + Bool,
        match s with
        | inl _ =>
            fun X : Unit + Bool =>
            match X with
            | inl _ => Empty
            | inr _ => Unit
            end
        | inr _ =>
            fun X : Unit + Bool => match X with
                                   | inl _ | _ => Empty
                                   end
        end j0 ->
        match s with
        | inl _ => {x : _ & A0 x}
        | inr true => {x : _ & B0 x}
        | inr false => {x : _ & C0 x}
        end ->
        match j0 with
        | inl _ => {x : _ & A0 x}
        | inr true => {x : _ & B0 x}
        | inr false => {x : _ & C0 x}
        end)
   with
   | inl _ =>
       fun j0 : Unit + Bool =>
       match
         j0 as s
         return
           (match s with
            | inl _ => Empty
            | inr _ => Unit
            end ->
            {x : _ & A0 x} ->
            match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end)
       with
       | inl _ =>
           fun (u1 : Empty) (_ : {x : _ & A0 x}) =>
           Empty_rect (fun _ : Empty => {x : _ & A0 x}) u1
       | inr b =>
           fun u0 : Unit =>
           match
             b as b0
             return
               (Unit ->
                {x : _ & A0 x} ->
                if b0 then {x : _ & B0 x} else {x : _ & C0 x})
           with
           | true => unit_name (functor_sigma f (fun x0 : A => f0 x0))
           | false => unit_name (functor_sigma g (fun x0 : A => g0 x0))
           end u0
       end
   | inr b =>
       fun j0 : Unit + Bool =>
       match
         j0 as s
         return
           (match s with
            | inl _ | _ => Empty
            end ->
            (if b then {x : _ & B0 x} else {x : _ & C0 x}) ->
            match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end)
       with
       | inl _ =>
           fun (u0 : Empty)
             (_ : if b then {x : _ & B0 x} else {x : _ & C0 x}) =>
           Empty_rect (fun _ : Empty => {x : _ & A0 x}) u0
       | inr b0 =>
           fun (u : Empty) (_ : if b then {x : _ & B0 x} else {x : _ & C0 x}) =>
           Empty_rect
             (fun _ : Empty => if b0 then {x : _ & B0 x} else {x : _ & C0 x})
             u
       end
   end j g1 x) =
(match
   i as s
   return
     (forall j0 : Unit + Bool,
      match s with
      | inl _ =>
          fun X : Unit + Bool =>
          match X with
          | inl _ => Empty
          | inr _ => Unit
          end
      | inr _ => fun X : Unit + Bool => match X with
                                        | inl _ | _ => Empty
                                        end
      end j0 ->
      match s with
      | inl _ => A
      | inr true => B
      | inr false => C
      end -> match j0 with
             | inl _ => A
             | inr true => B
             | inr false => C
             end)
 with
 | inl _ =>
     fun j0 : Unit + Bool =>
     match
       j0 as s
       return
         (match s with
          | inl _ => Empty
          | inr _ => Unit
          end ->
          A -> match s with
               | inl _ => A
               | inr true => B
               | inr false => C
               end)
     with
     | inl _ =>
         fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
     | inr b =>
         fun u0 : Unit =>
         match b as b0 return (Unit -> A -> if b0 then B else C) with
         | true => unit_name f
         | false => unit_name g
         end u0
     end
 | inr b =>
     fun j0 : Unit + Bool =>
     match
       j0 as s
       return
         (match s with
          | inl _ | _ => Empty
          end ->
          (if b then B else C) ->
          match s with
          | inl _ => A
          | inr true => B
          | inr false => C
          end)
     with
     | inl _ =>
         fun (u0 : Empty) (_ : if b then B else C) =>
         Empty_rect (fun _ : Empty => A) u0
     | inr b0 =>
         fun (u : Empty) (_ : if b then B else C) =>
         Empty_rect (fun _ : Empty => if b0 then B else C) u
     end
 end j g1
   (transport idmap
      ((fun i0 : Unit + Bool =>
        match
          i0 as s
          return
            (match s with
             | inl _ => {x : _ & A0 x}
             | inr true => {x : _ & B0 x}
             | inr false => {x : _ & C0 x}
             end =
             {x0
             : match s with
               | inl _ => A
               | inr true => B
               | inr false => C
               end
             &
             match
               s as s0
               return
                 (match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b =>
                 fun x1 : if b then B else C =>
                 match b as b0 return ((if b0 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x1
             end x0})
        with
        | inl u => unit_name (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
        | inr b =>
            (fun b0 : Bool =>
             match
               b0 as b1
               return
                 ((if b1 then {x : _ & B0 x} else {x : _ & C0 x}) =
                  {x0 : if b1 then B else C &
                  match b1 as b2 return ((if b2 then B else C) -> Type) with
                  | true => B0
                  | false => C0
                  end x0})
             with
             | true => 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
             | false => 1 : {x : _ & C0 x} = {x0 : C & C0 x0}
             end) b
        end) i)
      x).1;
match
  i as s
  return
    (forall
     (proj2 : match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
     (j0 : {i0 : Unit + Bool &
           match i0 with
           | inl _ => A
           | inr true => B
           | inr false => C
           end}),
     {g2
     : match s with
       | inl _ =>
           fun X : Unit + Bool =>
           match X with
           | inl _ => Empty
           | inr _ => Unit
           end
       | inr _ =>
           fun X : Unit + Bool => match X with
                                  | inl _ | _ => Empty
                                  end
       end j0.1
     &
     match
       s as s0
       return
         (forall j1 : Unit + Bool,
          match s0 with
          | inl _ =>
              fun X : Unit + Bool =>
              match X with
              | inl _ => Empty
              | inr _ => Unit
              end
          | inr _ =>
              fun X : Unit + Bool => match X with
                                     | inl _ | _ => Empty
                                     end
          end j1 ->
          match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end ->
          match j1 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end)
     with
     | inl _ =>
         fun j1 : Unit + Bool =>
         match
           j1 as s0
           return
             (match s0 with
              | inl _ => Empty
              | inr _ => Unit
              end ->
              A ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             match b as b0 return (Unit -> A -> if b0 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end u0
         end
     | inr b =>
         fun j1 : Unit + Bool =>
         match
           j1 as s0
           return
             (match s0 with
              | inl _ | _ => Empty
              end ->
              (if b then B else C) ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u0 : Empty) (_ : if b then B else C) =>
             Empty_rect (fun _ : Empty => A) u0
         | inr b0 =>
             fun (u : Empty) (_ : if b then B else C) =>
             Empty_rect (fun _ : Empty => if b0 then B else C) u
         end
     end j0.1 g2 proj2 = j0.2} ->
     match
       s as s0
       return
         (match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end -> Type)
     with
     | inl _ => fun x0 : A => A0 x0
     | inr b =>
         fun x0 : if b then B else C =>
         match b as b0 return ((if b0 then B else C) -> Type) with
         | true => B0
         | false => C0
         end x0
     end proj2 ->
     match
       j0.1 as s0
       return
         (match s0 with
          | inl _ => A
          | inr true => B
          | inr false => C
          end -> Type)
     with
     | inl _ => fun x0 : A => A0 x0
     | inr b =>
         fun x0 : if b then B else C =>
         match b as b0 return ((if b0 then B else C) -> Type) with
         | true => B0
         | false => C0
         end x0
     end j0.2)
with
| inl tt =>
    fun (x0 : A)
      (j0 : {i0 : Unit + Bool &
            match i0 with
            | inl _ => A
            | inr true => B
            | inr false => C
            end}) =>
    match
      j0.1 as s
      return
        (forall
         proj2 : match s with
                 | inl _ => A
                 | inr true => B
                 | inr false => C
                 end,
         {g2 : match s with
               | inl _ => Empty
               | inr _ => Unit
               end
         &
         match
           s as s0
           return
             (match s0 with
              | inl _ => Empty
              | inr _ => Unit
              end ->
              A ->
              match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             match b as b0 return (Unit -> A -> if b0 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end u0
         end g2 x0 = proj2} ->
         A0 x0 ->
         match
           s as s0
           return
             (match s0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end -> Type)
         with
         | inl _ => fun x1 : A => A0 x1
         | inr b =>
             fun x1 : if b then B else C =>
             match b as b0 return ((if b0 then B else C) -> Type) with
             | true => B0
             | false => C0
             end x1
         end proj2)
    with
    | inl tt =>
        fun (y : A)
          (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
        match
          X.1 as e
          return (Empty_rect (fun _ : Empty => A) e = y -> A0 x0 -> A0 y)
        with
        end X.2
    | inr b =>
        match
          b as b0
          return
            (forall proj2 : if b0 then B else C,
             {g2 : Unit &
             match b0 as b1 return (Unit -> A -> if b1 then B else C) with
             | true => unit_name f
             | false => unit_name g
             end g2 x0 = proj2} ->
             A0 x0 ->
             match b0 as b1 return ((if b1 then B else C) -> Type) with
             | true => B0
             | false => C0
             end proj2)
        with
        | true =>
            fun (y : B) (X : {_ : Unit & f x0 = y}) =>
            match X.1 with
            | tt =>
                fun (p : f x0 = y) (y0 : A0 x0) => transport B0 p (f0 x0 y0)
            end X.2
        | false =>
            fun (y : C) (X : {_ : Unit & g x0 = y}) =>
            match X.1 with
            | tt =>
                fun (p : g x0 = y) (y0 : A0 x0) => transport C0 p (g0 x0 y0)
            end X.2
        end
    end j0.2
| inr b =>
    match
      b as b0
      return
        (forall (proj2 : if b0 then B else C)
         (j0 : {i0 : Unit + Bool &
               match i0 with
               | inl _ => A
               | inr true => B
               | inr false => C
               end}),
         {g2 : match j0.1 with
               | inl _ | _ => Empty
               end
         &
         match
           j0.1 as s
           return
             (match s with
              | inl _ | _ => Empty
              end ->
              (if b0 then B else C) ->
              match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
         with
         | inl _ =>
             fun (u0 : Empty) (_ : if b0 then B else C) =>
             Empty_rect (fun _ : Empty => A) u0
         | inr b1 =>
             fun (u : Empty) (_ : if b0 then B else C) =>
             Empty_rect (fun _ : Empty => if b1 then B else C) u
         end g2 proj2 = j0.2} ->
         match b0 as b1 return ((if b1 then B else C) -> Type) with
         | true => B0
         | false => C0
         end proj2 ->
         match
           j0.1 as s
           return
             (match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end -> Type)
         with
         | inl _ => fun x0 : A => A0 x0
         | inr b1 =>
             fun x0 : if b1 then B else C =>
             match b1 as b2 return ((if b2 then B else C) -> Type) with
             | true => B0
             | false => C0
             end x0
         end j0.2)
    with
    | true =>
        fun (x0 : B)
          (j0 : {i0 : Unit + Bool &
                match i0 with
                | inl _ => A
                | inr true => B
                | inr false => C
                end}) =>
        match
          j0.1 as s
          return
            (forall
             proj2 : match s with
                     | inl _ => A
                     | inr true => B
                     | inr false => C
                     end,
             {g2 : match s with
                   | inl _ | _ => Empty
                   end
             &
             match
               s as s0
               return
                 (match s0 with
                  | inl _ | _ => Empty
                  end ->
                  B ->
                  match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end)
             with
             | inl _ =>
                 fun (u0 : Empty) (_ : B) =>
                 Empty_rect (fun _ : Empty => A) u0
             | inr b0 =>
                 fun (u : Empty) (_ : B) =>
                 Empty_rect (fun _ : Empty => if b0 then B else C) u
             end g2 x0 = proj2} ->
             B0 x0 ->
             match
               s as s0
               return
                 (match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b0 =>
                 fun x1 : if b0 then B else C =>
                 match b0 as b1 return ((if b1 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x1
             end proj2)
        with
        | inl tt =>
            fun (y : A)
              (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
            match
              X.1 as e
              return (Empty_rect (fun _ : Empty => A) e = y -> B0 x0 -> A0 y)
            with
            end X.2
        | inr b0 =>
            match
              b0 as b1
              return
                (forall proj2 : if b1 then B else C,
                 {g2 : Empty &
                 Empty_rect (fun _ : Empty => if b1 then B else C) g2 = proj2} ->
                 B0 x0 ->
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end proj2)
            with
            | true =>
                fun (y : B)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => B) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => B) e = y -> B0 x0 -> B0 y)
                with
                end X.2
            | false =>
                fun (y : C)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => C) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => C) e = y -> B0 x0 -> C0 y)
                with
                end X.2
            end
        end j0.2
    | false =>
        fun (x0 : C)
          (j0 : {i0 : Unit + Bool &
                match i0 with
                | inl _ => A
                | inr true => B
                | inr false => C
                end}) =>
        match
          j0.1 as s
          return
            (forall
             proj2 : match s with
                     | inl _ => A
                     | inr true => B
                     | inr false => C
                     end,
             {g2 : match s with
                   | inl _ | _ => Empty
                   end
             &
             match
               s as s0
               return
                 (match s0 with
                  | inl _ | _ => Empty
                  end ->
                  C ->
                  match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end)
             with
             | inl _ =>
                 fun (u0 : Empty) (_ : C) =>
                 Empty_rect (fun _ : Empty => A) u0
             | inr b0 =>
                 fun (u : Empty) (_ : C) =>
                 Empty_rect (fun _ : Empty => if b0 then B else C) u
             end g2 x0 = proj2} ->
             C0 x0 ->
             match
               s as s0
               return
                 (match s0 with
                  | inl _ => A
                  | inr true => B
                  | inr false => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b0 =>
                 fun x1 : if b0 then B else C =>
                 match b0 as b1 return ((if b1 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x1
             end proj2)
        with
        | inl tt =>
            fun (y : A)
              (X : {g2 : Empty & Empty_rect (fun _ : Empty => A) g2 = y}) =>
            match
              X.1 as e
              return (Empty_rect (fun _ : Empty => A) e = y -> C0 x0 -> A0 y)
            with
            end X.2
        | inr b0 =>
            match
              b0 as b1
              return
                (forall proj2 : if b1 then B else C,
                 {g2 : Empty &
                 Empty_rect (fun _ : Empty => if b1 then B else C) g2 = proj2} ->
                 C0 x0 ->
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end proj2)
            with
            | true =>
                fun (y : B)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => B) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => B) e = y -> C0 x0 -> B0 y)
                with
                end X.2
            | false =>
                fun (y : C)
                  (X : {g2 : Empty & Empty_rect (fun _ : Empty => C) g2 = y}) =>
                match
                  X.1 as e
                  return
                    (Empty_rect (fun _ : Empty => C) e = y -> C0 x0 -> C0 y)
                with
                end X.2
            end
        end j0.2
    end
end
  (transport idmap
     ((fun i0 : Unit + Bool =>
       match
         i0 as s
         return
           (match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end =
            {x0
            : match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end
            &
            match
              s as s0
              return
                (match s0 with
                 | inl _ => A
                 | inr true => B
                 | inr false => C
                 end -> Type)
            with
            | inl _ => fun x1 : A => A0 x1
            | inr b =>
                fun x1 : if b then B else C =>
                match b as b0 return ((if b0 then B else C) -> Type) with
                | true => B0
                | false => C0
                end x1
            end x0})
       with
       | inl u => unit_name (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
       | inr b =>
           (fun b0 : Bool =>
            match
              b0 as b1
              return
                ((if b1 then {x : _ & B0 x} else {x : _ & C0 x}) =
                 {x0 : if b1 then B else C &
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x0})
            with
            | true => 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
            | false => 1 : {x : _ & C0 x} = {x0 : C & C0 x0}
            end) b
       end) i)
     x).1
  (j;
  match
    i as s
    return
      (forall j0 : Unit + Bool,
       match s with
       | inl _ =>
           fun X : Unit + Bool =>
           match X with
           | inl _ => Empty
           | inr _ => Unit
           end
       | inr _ =>
           fun X : Unit + Bool => match X with
                                  | inl _ | _ => Empty
                                  end
       end j0 ->
       match s with
       | inl _ => A
       | inr true => B
       | inr false => C
       end -> match j0 with
              | inl _ => A
              | inr true => B
              | inr false => C
              end)
  with
  | inl _ =>
      fun j0 : Unit + Bool =>
      match
        j0 as s
        return
          (match s with
           | inl _ => Empty
           | inr _ => Unit
           end ->
           A ->
           match s with
           | inl _ => A
           | inr true => B
           | inr false => C
           end)
      with
      | inl _ =>
          fun (u1 : Empty) (_ : A) => Empty_rect (fun _ : Empty => A) u1
      | inr b =>
          fun u0 : Unit =>
          match b as b0 return (Unit -> A -> if b0 then B else C) with
          | true => unit_name f
          | false => unit_name g
          end u0
      end
  | inr b =>
      fun j0 : Unit + Bool =>
      match
        j0 as s
        return
          (match s with
           | inl _ | _ => Empty
           end ->
           (if b then B else C) ->
           match s with
           | inl _ => A
           | inr true => B
           | inr false => C
           end)
      with
      | inl _ =>
          fun (u0 : Empty) (_ : if b then B else C) =>
          Empty_rect (fun _ : Empty => A) u0
      | inr b0 =>
          fun (u : Empty) (_ : if b then B else C) =>
          Empty_rect (fun _ : Empty => if b0 then B else C) u
      end
  end j g1
    (transport idmap
       ((fun i0 : Unit + Bool =>
         match
           i0 as s
           return
             (match s with
              | inl _ => {x : _ & A0 x}
              | inr true => {x : _ & B0 x}
              | inr false => {x : _ & C0 x}
              end =
              {x0
              : match s with
                | inl _ => A
                | inr true => B
                | inr false => C
                end
              &
              match
                s as s0
                return
                  (match s0 with
                   | inl _ => A
                   | inr true => B
                   | inr false => C
                   end -> Type)
              with
              | inl _ => fun x1 : A => A0 x1
              | inr b =>
                  fun x1 : if b then B else C =>
                  match b as b0 return ((if b0 then B else C) -> Type) with
                  | true => B0
                  | false => C0
                  end x1
              end x0})
         with
         | inl u => unit_name (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
         | inr b =>
             (fun b0 : Bool =>
              match
                b0 as b1
                return
                  ((if b1 then {x : _ & B0 x} else {x : _ & C0 x}) =
                   {x0 : if b1 then B else C &
                   match b1 as b2 return ((if b2 then B else C) -> Type) with
                   | true => B0
                   | false => C0
                   end x0})
              with
              | true => 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
              | false => 1 : {x : _ & C0 x} = {x0 : C & C0 x0}
              end) b
         end) i)
       x).1)
  (g1; 1)
  (transport idmap
     ((fun i0 : Unit + Bool =>
       match
         i0 as s
         return
           (match s with
            | inl _ => {x : _ & A0 x}
            | inr true => {x : _ & B0 x}
            | inr false => {x : _ & C0 x}
            end =
            {x0
            : match s with
              | inl _ => A
              | inr true => B
              | inr false => C
              end
            &
            match
              s as s0
              return
                (match s0 with
                 | inl _ => A
                 | inr true => B
                 | inr false => C
                 end -> Type)
            with
            | inl _ => fun x1 : A => A0 x1
            | inr b =>
                fun x1 : if b then B else C =>
                match b as b0 return ((if b0 then B else C) -> Type) with
                | true => B0
                | false => C0
                end x1
            end x0})
       with
       | inl u => unit_name (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
       | inr b =>
           (fun b0 : Bool =>
            match
              b0 as b1
              return
                ((if b1 then {x : _ & B0 x} else {x : _ & C0 x}) =
                 {x0 : if b1 then B else C &
                 match b1 as b2 return ((if b2 then B else C) -> Type) with
                 | true => B0
                 | false => C0
                 end x0})
            with
            | true => 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
            | false => 1 : {x : _ & C0 x} = {x0 : C & C0 x0}
            end) b
       end) i)
     x).2) intros [[]|[]] [[]|[]] [] x; cbn in *.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: {x : _ & A0 x}
functor_sigma f (fun x0 : A => f0 x0) x =
(f x.1; transport B0 1 (f0 x.1 x.2))
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: {x : _ & A0 x}
functor_sigma g (fun x0 : A => g0 x0) x =
(g x.1; transport C0 1 (g0 x.1 x.2))
        all: reflexivity. }
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Colimit (diagram_sigma POCase_E) <~> {x : PO f g & POCase_P x}
    transitivity (exists x, E' (span f g) POCase_E POCase_HE x).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Colimit (diagram_sigma POCase_E) <~>
{x : Colimit (span f g) & E' (span f g) POCase_E POCase_HE x}
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{x : Colimit (span f g) & E' (span f g) POCase_E POCase_HE x} <~>
{x : PO f g & POCase_P x}
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
Colimit (diagram_sigma POCase_E) <~>
{x : Colimit (span f g) & E' (span f g) POCase_E POCase_HE x} apply flattening_lemma.
    -
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
{x : Colimit (span f g) & E' (span f g) POCase_E POCase_HE x} <~>
{x : PO f g & POCase_P x} apply equiv_functor_sigma_id.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
forall a : Colimit (span f g),
E' (span f g) POCase_E POCase_HE a <~> POCase_P a
      intro x.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
E' (span f g) POCase_E POCase_HE x <~> POCase_P x
      apply equiv_path.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
E' (span f g) POCase_E POCase_HE x = POCase_P x
      unfold E', POCase_P, PO_rec.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
Colimit_rec Type
  {|
    legs :=
      fun (i : Graph.graph0 span_graph) (x0 : span f g i) => POCase_E (i; x0);
    legs_comm :=
      fun (i j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i j)
        (x0 : span f g i) =>
      (path_universe (POCase_E _f (g1; 1)))^
  |} x =
Colimit_rec Type
  (Build_span_cocone B0 C0
     (fun x0 : A =>
      path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1%equiv)))
  x
      f_ap.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
{|
  legs :=
    fun (i : Graph.graph0 span_graph) (x0 : span f g i) => POCase_E (i; x0);
  legs_comm :=
    fun (i j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i j)
      (x0 : span f g i) =>
    (path_universe (POCase_E _f (g1; 1)))^
|} =
Build_span_cocone B0 C0
  (fun x0 : A =>
   path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1%equiv)) srapply path_cocone.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall i : Graph.graph0 span_graph,
{|
  legs :=
    fun (i0 : Graph.graph0 span_graph) (x0 : span f g i0) =>
    POCase_E (i0; x0);
  legs_comm :=
    fun (i0 j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i0 j)
      (x0 : span f g i0) =>
    (path_universe (POCase_E _f (g1; 1)))^
|} i ==
Build_span_cocone B0 C0
  (fun x0 : A =>
   path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
  i
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall (i j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i j)
(x0 : span f g i),
legs_comm
  {|
    legs :=
      fun (i0 : Graph.graph0 span_graph) (x1 : span f g i0) =>
      POCase_E (i0; x1);
    legs_comm :=
      fun (i0 j0 : Graph.graph0 span_graph)
        (g2 : Graph.graph1 span_graph i0 j0) (x1 : span f g i0) =>
      (path_universe (POCase_E _f (g2; 1)))^
  |} i j g1 x0 @
?path_legs i x0 =
?path_legs j (((span f g) _f g1) x0) @
legs_comm
  (Build_span_cocone B0 C0
     (fun x1 : A =>
      path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv)))
  i j g1 x0
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall i : Graph.graph0 span_graph,
{|
  legs :=
    fun (i0 : Graph.graph0 span_graph) (x0 : span f g i0) =>
    POCase_E (i0; x0);
  legs_comm :=
    fun (i0 j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i0 j)
      (x0 : span f g i0) =>
    (path_universe (POCase_E _f (g1; 1)))^
|} i ==
Build_span_cocone B0 C0
  (fun x0 : A =>
   path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
  i intros [[]|[]] y; cbn.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: span f g (inl tt)
A0 y = C0 (g y)
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: span f g (inr true)
B0 y = B0 y
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: span f g (inr false)
C0 y = C0 y
        1: apply path_universe_uncurried; apply g0.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: span f g (inr true)
B0 y = B0 y
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: span f g (inr false)
C0 y = C0 y
        all: reflexivity.
      +
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall (i j : Graph.graph0 span_graph) (g1 : Graph.graph1 span_graph i j)
(x0 : span f g i),
legs_comm
  {|
    legs :=
      fun (i0 : Graph.graph0 span_graph) (x1 : span f g i0) =>
      POCase_E (i0; x1);
    legs_comm :=
      fun (i0 j0 : Graph.graph0 span_graph)
        (g2 : Graph.graph1 span_graph i0 j0) (x1 : span f g i0) =>
      (path_universe (POCase_E _f (g2; 1)))^
  |} i j g1 x0 @
(fun i0 : Graph.graph0 span_graph =>
 match
   i0 as s
   return
     ({|
        legs :=
          fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
          POCase_E (i1; x1);
        legs_comm :=
          fun (i1 j0 : Graph.graph0 span_graph)
            (g2 : Graph.graph1 span_graph i1 j0) (x1 : span f g i1) =>
          (path_universe (POCase_E _f (g2; 1)))^
      |} s ==
      Build_span_cocone B0 C0
        (fun x1 : A =>
         path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
        s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inl u1) ==
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inl u1))
      with
      | tt =>
          (fun y : span f g (inl tt) =>
           path_universe_uncurried (g0 y)
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inl tt) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inl tt) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inl tt) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      match
        b0 as b1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr b1) ==
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr b1))
      with
      | true =>
          (fun y : span f g (inr true) =>
           1
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr true) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr true) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inr true) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inr true)
      | false =>
          (fun y : span f g (inr false) =>
           1
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr false) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr false) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inr false) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inr false)
      end) b
 end) i x0 =
(fun i0 : Graph.graph0 span_graph =>
 match
   i0 as s
   return
     ({|
        legs :=
          fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
          POCase_E (i1; x1);
        legs_comm :=
          fun (i1 j0 : Graph.graph0 span_graph)
            (g2 : Graph.graph1 span_graph i1 j0) (x1 : span f g i1) =>
          (path_universe (POCase_E _f (g2; 1)))^
      |} s ==
      Build_span_cocone B0 C0
        (fun x1 : A =>
         path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
        s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inl u1) ==
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inl u1))
      with
      | tt =>
          (fun y : span f g (inl tt) =>
           path_universe_uncurried (g0 y)
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inl tt) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inl tt) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inl tt) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      match
        b0 as b1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr b1) ==
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr b1))
      with
      | true =>
          (fun y : span f g (inr true) =>
           1
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr true) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr true) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inr true) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inr true)
      | false =>
          (fun y : span f g (inr false) =>
           1
           :
           {|
             legs :=
               fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
               POCase_E (i1; x1);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g2 : Graph.graph1 span_graph i1 j0) 
                 (x1 : span f g i1) =>
               (path_universe (POCase_E _f (g2; 1)))^
           |} (inr false) y =
           Build_span_cocone B0 C0
             (fun x1 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
             (inr false) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph) (x1 : span f g i1) =>
              POCase_E (i1; x1);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g2 : Graph.graph1 span_graph i1 j0) 
                (x1 : span f g i1) =>
              (path_universe (POCase_E _f (g2; 1)))^
          |} (inr false) ==
          Build_span_cocone B0 C0
            (fun x1 : A =>
             path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv))
            (inr false)
      end) b
 end) j (((span f g) _f g1) x0) @
legs_comm
  (Build_span_cocone B0 C0
     (fun x1 : A =>
      path_universe_uncurried (equiv_compose (g0 x1) (f0 x1)^-1%equiv)))
  i j g1 x0 intros [[]|[]] [[]|[]] []; cbn.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall x0 : A,
(path_universe (fun y : A0 x0 => transport B0 1 (f0 x0 y)))^ @
path_universe_uncurried (g0 x0) =
1 @ path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1)
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall x0 : A,
(path_universe (fun y : A0 x0 => transport C0 1 (g0 x0 y)))^ @
path_universe_uncurried (g0 x0) = 1
        *
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall x0 : A,
(path_universe (fun y : A0 x0 => transport B0 1 (f0 x0 y)))^ @
path_universe_uncurried (g0 x0) =
1 @ path_universe_uncurried (equiv_compose (g0 x0) (f0 x0)^-1) intro y.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
(path_universe (fun y0 : A0 y => transport B0 1 (f0 y y0)))^ @
path_universe_uncurried (g0 y) =
1 @ path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1) simpl.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
(path_universe (fun y0 : A0 y => f0 y y0))^ @ path_universe_uncurried (g0 y) =
1 @ path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1)
          rhs napply concat_1p.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
(path_universe (fun y0 : A0 y => f0 y y0))^ @ path_universe_uncurried (g0 y) =
path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1)
          unfold path_universe.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
(path_universe_uncurried
   {|
     equiv_fun := fun y0 : A0 y => f0 y y0;
     equiv_isequiv := equiv_isequiv (f0 y)
   |})^ @
path_universe_uncurried (g0 y) =
path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1)
          lhs napply (ap (fun x => x @ _) _^).
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
?Goal0 =
(path_universe_uncurried
   {|
     equiv_fun := fun y0 : A0 y => f0 y y0;
     equiv_isequiv := equiv_isequiv (f0 y)
   |})^
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
?Goal0 @ path_universe_uncurried (g0 y) =
path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1)
          1: napply path_universe_V_uncurried.
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
y: A
path_universe_uncurried
  {|
    equiv_fun := fun y0 : A0 y => f0 y y0;
    equiv_isequiv := equiv_isequiv (f0 y)
  |}^-1 @
path_universe_uncurried (g0 y) =
path_universe_uncurried (equiv_compose (g0 y) (f0 y)^-1)
          exact (path_universe_compose (f0 y)^-1 (g0 y))^. 
        *
H: Univalence
A, B, C: Type
f: A -> B
g: A -> C
A0: A -> Type
B0: B -> Type
C0: C -> Type
f0: forall x0 : A, A0 x0 <~> B0 (f x0)
g0: forall x0 : A, A0 x0 <~> C0 (g x0)
x: Colimit (span f g)
forall x0 : A,
(path_universe (fun y : A0 x0 => transport C0 1 (g0 x0 y)))^ @
path_universe_uncurried (g0 x0) = 1 intros; apply concat_Vp.
  Defined.

End POCase.