Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import Diagrams.Diagram.
Require Import Diagrams.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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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}),
{g0
: 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 =>
        (if b as b0
          return (Unit -> A -> if b0 then B else C)
         then unit_name f
         else unit_name g) 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 g0 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}),
{g0
: 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 =>
        (if b as b0
          return (Unit -> A -> if b0 then B else C)
         then unit_name f
         else unit_name g) 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 g0 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) =>
       (if b0 as b1
         return ((if b1 then B else C) -> Type)
        then B0
        else C0) 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) =>
       (if b0 as b1
         return ((if b1 then B else C) -> Type)
        then B0
        else C0) 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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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)
(g0 : Graph.graph1 span_graph i j) (x : span f g i),
IsEquiv (POCase_E _f (g0; 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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 =>
    (if b as b0 return ((if b0 then B else C) -> Type)
     then B0
     else C0) 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 =>
           (if b as b0
             return
               (Unit ->
                {x : _ & A0 x} ->
                if b0
                then {x : _ & B0 x}
                else {x : _ & C0 x})
            then
             unit_name
               (functor_sigma f (fun x0 : A => f0 x0))
            else
             unit_name
               (functor_sigma g (fun x0 : A => g0 x0)))
             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 =>
         (if b as b0
           return (Unit -> A -> if b0 then B else C)
          then unit_name f
          else unit_name g) 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}),
     {g0
     : 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 : ... =>
              match ... with
              | ... Empty
              | ... Unit
              end
          | inr _ =>
              fun X : ... =>
              match ... with
              | ... 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 ... with
              | ... => A
              | ... => B
              | ... => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) =>
             Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             (if b as b0 return (Unit -> ...)
              then unit_name f
              else unit_name g) 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 ... with
              | ... => A
              | ... => B
              | ... => 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 g0 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 =>
         (if b as b0
           return ((if b0 then B else C) -> Type)
          then B0
          else C0) 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 =>
         (if b as b0
           return ((if b0 then B else C) -> Type)
          then B0
          else C0) 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,
         {g0
         : match s with
           | inl _ => Empty
           | inr _ => Unit
           end &
         match
           s as s0
           return
             (match ... with
              | ... => Empty
              | ... => Unit
              end ->
              A ->
              match ... with
              | ... A
              | ... B
              | ... C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) =>
             Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             (if b as b0 return (...)
              then unit_name f
              else unit_name g) u0
         end g0 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 =>
             (if b as b0 return (... -> Type)
              then B0
              else C0) x1
         end proj2)
    with
    | inl tt =>
        fun (y : A)
          (X : {g : Empty &
               Empty_rect (fun _ : Empty => A) g = y})
        =>
        match
          X.1 as e
          return
            (Empty_rect (fun _ : Empty => A) e = y ->
             A0 x0 -> A0 y)
        with
        end X.2
    | inr b =>
        if b as b0
         return
           (forall proj2 : if b0 then B else C,
            {g0 : Unit &
            (if b0 as b1
              return (Unit -> A -> ... ... ...)
             then unit_name f
             else unit_name g) g0 x0 = proj2} ->
            A0 x0 ->
            (if b0 as b1
              return ((if b1 then B else C) -> Type)
             then B0
             else C0) proj2)
        then
         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
        else
         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 j0.2
| inr b =>
    if 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}),
        {g : 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 g proj2 = j0.2} ->
        (if b0 as b1
          return ((if b1 then B else C) -> Type)
         then B0
         else C0) 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 =>
            (if b1 as b2
              return ((if b2 then B else C) -> Type)
             then B0
             else C0) x0
        end j0.2)
    then
     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,
          {g : match s with
               | inl _ | _ => Empty
               end &
          match
            s as s0 return (...
                            ...
                            end -> B -> ...)
          with
          | inl _ =>
              fun (u0 : Empty) (_ : B) =>
              Empty_rect (fun ... => A) u0
          | inr b0 =>
              fun (u : Empty) (_ : B) =>
              Empty_rect (fun ... => ... ... ...) u
          end g x0 = proj2} ->
          B0 x0 ->
          match
            s as s0
            return
              (match ... with
               | ... A
               | ... B
               | ... C
               end -> Type)
          with
          | inl _ => fun x1 : A => A0 x1
          | inr b0 =>
              fun x1 : if b0 then B else C =>
              (if b0 as b1 return ... then B0 else C0)
                x1
          end proj2)
     with
     | inl tt =>
         fun (y : A)
           (X : {g : Empty &
                Empty_rect (fun _ : Empty => A) g = y})
         =>
         match
           X.1 as e
           return
             (Empty_rect (fun _ : Empty => A) e = y ->
              B0 x0 -> A0 y)
         with
         end X.2
     | inr b0 =>
         if b0 as b1
          return
            (forall proj2 : if b1 then B else C,
             {g : Empty &
             Empty_rect
               (fun _ : Empty => if b1 then B else C)
               g = proj2} ->
             B0 x0 ->
             (if b1 as b2 return ((...) -> Type)
              then B0
              else C0) proj2)
         then
          fun (y : B)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => B) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => B) e = y ->
               B0 x0 -> B0 y)
          with
          end X.2
         else
          fun (y : C)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => C) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => C) e = y ->
               B0 x0 -> C0 y)
          with
          end X.2
     end j0.2
    else
     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,
          {g : match s with
               | inl _ | _ => Empty
               end &
          match
            s as s0 return (...
                            ...
                            end -> C -> ...)
          with
          | inl _ =>
              fun (u0 : Empty) (_ : C) =>
              Empty_rect (fun ... => A) u0
          | inr b0 =>
              fun (u : Empty) (_ : C) =>
              Empty_rect (fun ... => ... ... ...) u
          end g x0 = proj2} ->
          C0 x0 ->
          match
            s as s0
            return
              (match ... with
               | ... A
               | ... B
               | ... C
               end -> Type)
          with
          | inl _ => fun x1 : A => A0 x1
          | inr b0 =>
              fun x1 : if b0 then B else C =>
              (if b0 as b1 return ... then B0 else C0)
                x1
          end proj2)
     with
     | inl tt =>
         fun (y : A)
           (X : {g : Empty &
                Empty_rect (fun _ : Empty => A) g = y})
         =>
         match
           X.1 as e
           return
             (Empty_rect (fun _ : Empty => A) e = y ->
              C0 x0 -> A0 y)
         with
         end X.2
     | inr b0 =>
         if b0 as b1
          return
            (forall proj2 : if b1 then B else C,
             {g : Empty &
             Empty_rect
               (fun _ : Empty => if b1 then B else C)
               g = proj2} ->
             C0 x0 ->
             (if b1 as b2 return ((...) -> Type)
              then B0
              else C0) proj2)
         then
          fun (y : B)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => B) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => B) e = y ->
               C0 x0 -> B0 y)
          with
          end X.2
         else
          fun (y : C)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => C) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => C) e = y ->
               C0 x0 -> C0 y)
          with
          end X.2
     end j0.2
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 =>
          (if b as b0
            return (Unit -> A -> if b0 then B else C)
           then unit_name f
           else unit_name g) 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 =>
    (if b as b0 return ((if b0 then B else C) -> Type)
     then B0
     else C0) 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 =>
             (if b as b0
               return ((... ... ...) -> Type)
              then B0
              else C0) x1
         end x0})
    with
    | inl u =>
        unit_name
          (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
    | inr b =>
        (fun b0 : Bool =>
         if b0 as b1
          return
            ((if b1
              then {x : _ & B0 x}
              else {x : _ & C0 x}) =
             {x0 : if b1 then B else C &
             (if b1 as b2
               return ((... ... ...) -> Type)
              then B0
              else C0) x0})
         then 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
         else 1 : {x : _ & C0 x} = {x0 : C & C0 x0}) 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 =>
           (if b as b0
             return
               (Unit ->
                {x : _ & A0 x} ->
                if b0
                then {x : _ & B0 x}
                else {x : _ & C0 x})
            then
             unit_name
               (functor_sigma f (fun x0 : A => f0 x0))
            else
             unit_name
               (functor_sigma g (fun x0 : A => g0 x0)))
             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 =>
         (if b as b0
           return (Unit -> A -> if b0 then B else C)
          then unit_name f
          else unit_name g) 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 ... with
                  | ... => A
                  | ... => B
                  | ... => C
                  end -> Type)
             with
             | inl _ => fun x1 : A => A0 x1
             | inr b =>
                 fun x1 : if b then B else C =>
                 (if b as b0 return (...)
                  then B0
                  else C0) x1
             end x0})
        with
        | inl u =>
            unit_name
              (1 : {x : _ & A0 x} = {x0 : A & A0 x0})
              u
        | inr b =>
            (fun b0 : Bool =>
             if b0 as b1
              return
                ((if b1
                  then {x : _ & B0 x}
                  else {x : _ & C0 x}) =
                 {x0 : if b1 then B else C &
                 (if b1 as b2 return (...)
                  then B0
                  else C0) x0})
             then
              1 : {x : _ & B0 x} = {x0 : B & B0 x0}
             else
              1 : {x : _ & C0 x} = {x0 : C & C0 x0}) 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}),
     {g0
     : 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 : ... =>
              match ... with
              | ... Empty
              | ... Unit
              end
          | inr _ =>
              fun X : ... =>
              match ... with
              | ... 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 ... with
              | ... => A
              | ... => B
              | ... => C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) =>
             Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             (if b as b0 return (Unit -> ...)
              then unit_name f
              else unit_name g) 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 ... with
              | ... => A
              | ... => B
              | ... => 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 g0 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 =>
         (if b as b0
           return ((if b0 then B else C) -> Type)
          then B0
          else C0) 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 =>
         (if b as b0
           return ((if b0 then B else C) -> Type)
          then B0
          else C0) 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,
         {g0
         : match s with
           | inl _ => Empty
           | inr _ => Unit
           end &
         match
           s as s0
           return
             (match ... with
              | ... => Empty
              | ... => Unit
              end ->
              A ->
              match ... with
              | ... A
              | ... B
              | ... C
              end)
         with
         | inl _ =>
             fun (u1 : Empty) (_ : A) =>
             Empty_rect (fun _ : Empty => A) u1
         | inr b =>
             fun u0 : Unit =>
             (if b as b0 return (...)
              then unit_name f
              else unit_name g) u0
         end g0 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 =>
             (if b as b0 return (... -> Type)
              then B0
              else C0) x1
         end proj2)
    with
    | inl tt =>
        fun (y : A)
          (X : {g : Empty &
               Empty_rect (fun _ : Empty => A) g = y})
        =>
        match
          X.1 as e
          return
            (Empty_rect (fun _ : Empty => A) e = y ->
             A0 x0 -> A0 y)
        with
        end X.2
    | inr b =>
        if b as b0
         return
           (forall proj2 : if b0 then B else C,
            {g0 : Unit &
            (if b0 as b1
              return (Unit -> A -> ... ... ...)
             then unit_name f
             else unit_name g) g0 x0 = proj2} ->
            A0 x0 ->
            (if b0 as b1
              return ((if b1 then B else C) -> Type)
             then B0
             else C0) proj2)
        then
         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
        else
         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 j0.2
| inr b =>
    if 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}),
        {g : 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 g proj2 = j0.2} ->
        (if b0 as b1
          return ((if b1 then B else C) -> Type)
         then B0
         else C0) 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 =>
            (if b1 as b2
              return ((if b2 then B else C) -> Type)
             then B0
             else C0) x0
        end j0.2)
    then
     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,
          {g : match s with
               | inl _ | _ => Empty
               end &
          match
            s as s0 return (...
                            ...
                            end -> B -> ...)
          with
          | inl _ =>
              fun (u0 : Empty) (_ : B) =>
              Empty_rect (fun ... => A) u0
          | inr b0 =>
              fun (u : Empty) (_ : B) =>
              Empty_rect (fun ... => ... ... ...) u
          end g x0 = proj2} ->
          B0 x0 ->
          match
            s as s0
            return
              (match ... with
               | ... A
               | ... B
               | ... C
               end -> Type)
          with
          | inl _ => fun x1 : A => A0 x1
          | inr b0 =>
              fun x1 : if b0 then B else C =>
              (if b0 as b1 return ... then B0 else C0)
                x1
          end proj2)
     with
     | inl tt =>
         fun (y : A)
           (X : {g : Empty &
                Empty_rect (fun _ : Empty => A) g = y})
         =>
         match
           X.1 as e
           return
             (Empty_rect (fun _ : Empty => A) e = y ->
              B0 x0 -> A0 y)
         with
         end X.2
     | inr b0 =>
         if b0 as b1
          return
            (forall proj2 : if b1 then B else C,
             {g : Empty &
             Empty_rect
               (fun _ : Empty => if b1 then B else C)
               g = proj2} ->
             B0 x0 ->
             (if b1 as b2 return ((...) -> Type)
              then B0
              else C0) proj2)
         then
          fun (y : B)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => B) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => B) e = y ->
               B0 x0 -> B0 y)
          with
          end X.2
         else
          fun (y : C)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => C) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => C) e = y ->
               B0 x0 -> C0 y)
          with
          end X.2
     end j0.2
    else
     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,
          {g : match s with
               | inl _ | _ => Empty
               end &
          match
            s as s0 return (...
                            ...
                            end -> C -> ...)
          with
          | inl _ =>
              fun (u0 : Empty) (_ : C) =>
              Empty_rect (fun ... => A) u0
          | inr b0 =>
              fun (u : Empty) (_ : C) =>
              Empty_rect (fun ... => ... ... ...) u
          end g x0 = proj2} ->
          C0 x0 ->
          match
            s as s0
            return
              (match ... with
               | ... A
               | ... B
               | ... C
               end -> Type)
          with
          | inl _ => fun x1 : A => A0 x1
          | inr b0 =>
              fun x1 : if b0 then B else C =>
              (if b0 as b1 return ... then B0 else C0)
                x1
          end proj2)
     with
     | inl tt =>
         fun (y : A)
           (X : {g : Empty &
                Empty_rect (fun _ : Empty => A) g = y})
         =>
         match
           X.1 as e
           return
             (Empty_rect (fun _ : Empty => A) e = y ->
              C0 x0 -> A0 y)
         with
         end X.2
     | inr b0 =>
         if b0 as b1
          return
            (forall proj2 : if b1 then B else C,
             {g : Empty &
             Empty_rect
               (fun _ : Empty => if b1 then B else C)
               g = proj2} ->
             C0 x0 ->
             (if b1 as b2 return ((...) -> Type)
              then B0
              else C0) proj2)
         then
          fun (y : B)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => B) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => B) e = y ->
               C0 x0 -> B0 y)
          with
          end X.2
         else
          fun (y : C)
            (X : {g : Empty &
                 Empty_rect (fun _ : Empty => C) g = y})
          =>
          match
            X.1 as e
            return
              (Empty_rect (fun ... => C) e = y ->
               C0 x0 -> C0 y)
          with
          end X.2
     end j0.2
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 ... with
                 | ... => A
                 | ... => B
                 | ... => C
                 end -> Type)
            with
            | inl _ => fun x1 : A => A0 x1
            | inr b =>
                fun x1 : if b then B else C =>
                (if b as b0 return (...)
                 then B0
                 else C0) x1
            end x0})
       with
       | inl u =>
           unit_name
             (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
       | inr b =>
           (fun b0 : Bool =>
            if b0 as b1
             return
               ((if b1
                 then {x : _ & B0 x}
                 else {x : _ & C0 x}) =
                {x0 : if b1 then B else C &
                (if b1 as b2 return (...)
                 then B0
                 else C0) x0})
            then 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
            else 1 : {x : _ & C0 x} = {x0 : C & C0 x0})
             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 =>
          (if b as b0
            return (Unit -> A -> if b0 then B else C)
           then unit_name f
           else unit_name g) 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 (...
                        ...
                        ...
                        ...
                        end -> Type)
              with
              | inl _ => fun x1 : A => A0 x1
              | inr b =>
                  fun x1 : if b then B else C =>
                  (if b as b0 ... then B0 else C0) x1
              end x0})
         with
         | inl u =>
             unit_name
               (1 : {x : _ & A0 x} = {x0 : A & A0 x0})
               u
         | inr b =>
             (fun b0 : Bool =>
              if b0 as b1
               return
                 ((if b1
                   then {x : _ & B0 x}
                   else {x : _ & C0 x}) =
                  {x0 : if b1 then B else C &
                  (if b1 as b2 ... then B0 else C0) x0})
              then
               1 : {x : _ & B0 x} = {x0 : B & B0 x0}
              else
               1 : {x : _ & C0 x} = {x0 : C & C0 x0})
               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 ... with
                 | ... => A
                 | ... => B
                 | ... => C
                 end -> Type)
            with
            | inl _ => fun x1 : A => A0 x1
            | inr b =>
                fun x1 : if b then B else C =>
                (if b as b0 return (...)
                 then B0
                 else C0) x1
            end x0})
       with
       | inl u =>
           unit_name
             (1 : {x : _ & A0 x} = {x0 : A & A0 x0}) u
       | inr b =>
           (fun b0 : Bool =>
            if b0 as b1
             return
               ((if b1
                 then {x : _ & B0 x}
                 else {x : _ & C0 x}) =
                {x0 : if b1 then B else C &
                (if b1 as b2 return (...)
                 then B0
                 else C0) x0})
            then 1 : {x : _ & B0 x} = {x0 : B & B0 x0}
            else 1 : {x : _ & C0 x} = {x0 : C & C0 x0})
             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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: {x : _ & A0 x}
functor_sigma f (fun x : A => f0 x) 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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: {x : _ & A0 x}
functor_sigma g (fun x : A => g0 x) 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 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 <~> 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 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 = 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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
Colimit_rec Type
  {|
    legs :=
      fun (i : Graph.graph0 span_graph)
        (x : span f g i) => POCase_E (i; x);
    legs_comm :=
      fun (i j : Graph.graph0 span_graph)
        (g0 : Graph.graph1 span_graph i j)
        (x : span f g i) =>
      (path_universe (POCase_E _f (g0; 1)))^
  |} x =
Colimit_rec Type
  (Build_span_cocone B0 C0
     (fun x : A =>
      path_universe_uncurried
        (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
{|
  legs :=
    fun (i : Graph.graph0 span_graph) (x : span f g i)
    => POCase_E (i; x);
  legs_comm :=
    fun (i j : Graph.graph0 span_graph)
      (g0 : Graph.graph1 span_graph i j)
      (x : span f g i) =>
    (path_universe (POCase_E _f (g0; 1)))^
|} =
Build_span_cocone B0 C0
  (fun x : A =>
   path_universe_uncurried
     (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
forall i : Graph.graph0 span_graph,
{|
  legs :=
    fun (i0 : Graph.graph0 span_graph)
      (x : span f g i0) => POCase_E (i0; x);
  legs_comm :=
    fun (i0 j : Graph.graph0 span_graph)
      (g0 : Graph.graph1 span_graph i0 j)
      (x : span f g i0) =>
    (path_universe (POCase_E _f (g0; 1)))^
|} i ==
Build_span_cocone B0 C0
  (fun x : A =>
   path_universe_uncurried
     (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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)
        (x : span f g i0) => POCase_E (i0; x);
    legs_comm :=
      fun (i0 j0 : Graph.graph0 span_graph)
        (g0 : Graph.graph1 span_graph i0 j0)
        (x : span f g i0) =>
      (path_universe (POCase_E _f (g0; 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 x : A =>
      path_universe_uncurried
        (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
forall i : Graph.graph0 span_graph,
{|
  legs :=
    fun (i0 : Graph.graph0 span_graph)
      (x : span f g i0) => POCase_E (i0; x);
  legs_comm :=
    fun (i0 j : Graph.graph0 span_graph)
      (g0 : Graph.graph1 span_graph i0 j)
      (x : span f g i0) =>
    (path_universe (POCase_E _f (g0; 1)))^
|} i ==
Build_span_cocone B0 C0
  (fun x : A =>
   path_universe_uncurried
     (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
forall (i j : Graph.graph0 span_graph)
(g1 : Graph.graph1 span_graph i j) (x : span f g i),
legs_comm
  {|
    legs :=
      fun (i0 : Graph.graph0 span_graph)
        (x0 : span f g i0) => POCase_E (i0; x0);
    legs_comm :=
      fun (i0 j0 : Graph.graph0 span_graph)
        (g0 : Graph.graph1 span_graph i0 j0)
        (x0 : span f g i0) =>
      (path_universe (POCase_E _f (g0; 1)))^
  |} i j g1 x @
(fun i0 : Graph.graph0 span_graph =>
 match
   i0 as s
   return
     ({|
        legs :=
          fun (i1 : Graph.graph0 span_graph)
            (x0 : span f g i1) => POCase_E (i1; x0);
        legs_comm :=
          fun (i1 j0 : Graph.graph0 span_graph)
            (g0 : Graph.graph1 span_graph i1 j0)
            (x0 : span f g i1) =>
          (path_universe (POCase_E _f (g0; 1)))^
      |} s ==
      Build_span_cocone B0 C0
        (fun x0 : A =>
         path_universe_uncurried
           (equiv_compose (g0 x0) (f0 x0)^-1%equiv)) s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph)
                 (x0 : span f g i1) =>
               POCase_E (i1; x0);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g0 : Graph.graph1 span_graph i1 j0)
                 (x0 : span f g i1) =>
               (path_universe (POCase_E _f (g0; 1)))^
           |} (inl u1) ==
           Build_span_cocone B0 C0
             (fun x0 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x0)
                   (f0 x0)^-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)
                 (x0 : span f g i1) =>
               POCase_E (i1; x0);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g0 : Graph.graph1 span_graph i1 j0)
                 (x0 : span f g i1) =>
               (path_universe (POCase_E _f ...))^
           |} (inl tt) y =
           Build_span_cocone B0 C0
             (fun x0 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x0)
                   (f0 x0)^-1%equiv)) (inl tt) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph)
                (x0 : span f g i1) =>
              POCase_E (i1; x0);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g0 : Graph.graph1 span_graph i1 j0)
                (x0 : span f g i1) =>
              (path_universe (POCase_E _f (g0; 1)))^
          |} (inl tt) ==
          Build_span_cocone B0 C0
            (fun x0 : A =>
             path_universe_uncurried
               (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
            (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1
       return
         ({|
            legs :=
              fun (i1 : Graph.graph0 span_graph)
                (x0 : span f g i1) =>
              POCase_E (i1; x0);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g0 : Graph.graph1 span_graph i1 j0)
                (x0 : span f g i1) =>
              (path_universe (POCase_E _f (g0; 1)))^
          |} (inr b1) ==
          Build_span_cocone B0 C0
            (fun x0 : A =>
             path_universe_uncurried
               (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
            (inr b1))
      then
       (fun y : span f g (inr true) =>
        1
        :
        {|
          legs :=
            fun (i1 : Graph.graph0 span_graph)
              (x0 : span f g i1) => POCase_E (i1; x0);
          legs_comm :=
            fun (i1 j0 : Graph.graph0 span_graph)
              (g0 : Graph.graph1 span_graph i1 j0)
              (x0 : span f g i1) =>
            (path_universe (POCase_E _f ...))^
        |} (inr true) y =
        Build_span_cocone B0 C0
          (fun x0 : A =>
           path_universe_uncurried
             (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
          (inr true) y)
       :
       {|
         legs :=
           fun (i1 : Graph.graph0 span_graph)
             (x0 : span f g i1) => POCase_E (i1; x0);
         legs_comm :=
           fun (i1 j0 : Graph.graph0 span_graph)
             (g0 : Graph.graph1 span_graph i1 j0)
             (x0 : span f g i1) =>
           (path_universe (POCase_E _f (g0; 1)))^
       |} (inr true) ==
       Build_span_cocone B0 C0
         (fun x0 : A =>
          path_universe_uncurried
            (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
         (inr true)
      else
       (fun y : span f g (inr false) =>
        1
        :
        {|
          legs :=
            fun (i1 : Graph.graph0 span_graph)
              (x0 : span f g i1) => POCase_E (i1; x0);
          legs_comm :=
            fun (i1 j0 : Graph.graph0 span_graph)
              (g0 : Graph.graph1 span_graph i1 j0)
              (x0 : span f g i1) =>
            (path_universe (POCase_E _f ...))^
        |} (inr false) y =
        Build_span_cocone B0 C0
          (fun x0 : A =>
           path_universe_uncurried
             (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
          (inr false) y)
       :
       {|
         legs :=
           fun (i1 : Graph.graph0 span_graph)
             (x0 : span f g i1) => POCase_E (i1; x0);
         legs_comm :=
           fun (i1 j0 : Graph.graph0 span_graph)
             (g0 : Graph.graph1 span_graph i1 j0)
             (x0 : span f g i1) =>
           (path_universe (POCase_E _f (g0; 1)))^
       |} (inr false) ==
       Build_span_cocone B0 C0
         (fun x0 : A =>
          path_universe_uncurried
            (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
         (inr false)) b
 end) i x =
(fun i0 : Graph.graph0 span_graph =>
 match
   i0 as s
   return
     ({|
        legs :=
          fun (i1 : Graph.graph0 span_graph)
            (x0 : span f g i1) => POCase_E (i1; x0);
        legs_comm :=
          fun (i1 j0 : Graph.graph0 span_graph)
            (g0 : Graph.graph1 span_graph i1 j0)
            (x0 : span f g i1) =>
          (path_universe (POCase_E _f (g0; 1)))^
      |} s ==
      Build_span_cocone B0 C0
        (fun x0 : A =>
         path_universe_uncurried
           (equiv_compose (g0 x0) (f0 x0)^-1%equiv)) s)
 with
 | inl u =>
     (fun u0 : Unit =>
      match
        u0 as u1
        return
          ({|
             legs :=
               fun (i1 : Graph.graph0 span_graph)
                 (x0 : span f g i1) =>
               POCase_E (i1; x0);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g0 : Graph.graph1 span_graph i1 j0)
                 (x0 : span f g i1) =>
               (path_universe (POCase_E _f (g0; 1)))^
           |} (inl u1) ==
           Build_span_cocone B0 C0
             (fun x0 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x0)
                   (f0 x0)^-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)
                 (x0 : span f g i1) =>
               POCase_E (i1; x0);
             legs_comm :=
               fun (i1 j0 : Graph.graph0 span_graph)
                 (g0 : Graph.graph1 span_graph i1 j0)
                 (x0 : span f g i1) =>
               (path_universe (POCase_E _f ...))^
           |} (inl tt) y =
           Build_span_cocone B0 C0
             (fun x0 : A =>
              path_universe_uncurried
                (equiv_compose (g0 x0)
                   (f0 x0)^-1%equiv)) (inl tt) y)
          :
          {|
            legs :=
              fun (i1 : Graph.graph0 span_graph)
                (x0 : span f g i1) =>
              POCase_E (i1; x0);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g0 : Graph.graph1 span_graph i1 j0)
                (x0 : span f g i1) =>
              (path_universe (POCase_E _f (g0; 1)))^
          |} (inl tt) ==
          Build_span_cocone B0 C0
            (fun x0 : A =>
             path_universe_uncurried
               (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
            (inl tt)
      end) u
 | inr b =>
     (fun b0 : Bool =>
      if b0 as b1
       return
         ({|
            legs :=
              fun (i1 : Graph.graph0 span_graph)
                (x0 : span f g i1) =>
              POCase_E (i1; x0);
            legs_comm :=
              fun (i1 j0 : Graph.graph0 span_graph)
                (g0 : Graph.graph1 span_graph i1 j0)
                (x0 : span f g i1) =>
              (path_universe (POCase_E _f (g0; 1)))^
          |} (inr b1) ==
          Build_span_cocone B0 C0
            (fun x0 : A =>
             path_universe_uncurried
               (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
            (inr b1))
      then
       (fun y : span f g (inr true) =>
        1
        :
        {|
          legs :=
            fun (i1 : Graph.graph0 span_graph)
              (x0 : span f g i1) => POCase_E (i1; x0);
          legs_comm :=
            fun (i1 j0 : Graph.graph0 span_graph)
              (g0 : Graph.graph1 span_graph i1 j0)
              (x0 : span f g i1) =>
            (path_universe (POCase_E _f ...))^
        |} (inr true) y =
        Build_span_cocone B0 C0
          (fun x0 : A =>
           path_universe_uncurried
             (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
          (inr true) y)
       :
       {|
         legs :=
           fun (i1 : Graph.graph0 span_graph)
             (x0 : span f g i1) => POCase_E (i1; x0);
         legs_comm :=
           fun (i1 j0 : Graph.graph0 span_graph)
             (g0 : Graph.graph1 span_graph i1 j0)
             (x0 : span f g i1) =>
           (path_universe (POCase_E _f (g0; 1)))^
       |} (inr true) ==
       Build_span_cocone B0 C0
         (fun x0 : A =>
          path_universe_uncurried
            (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
         (inr true)
      else
       (fun y : span f g (inr false) =>
        1
        :
        {|
          legs :=
            fun (i1 : Graph.graph0 span_graph)
              (x0 : span f g i1) => POCase_E (i1; x0);
          legs_comm :=
            fun (i1 j0 : Graph.graph0 span_graph)
              (g0 : Graph.graph1 span_graph i1 j0)
              (x0 : span f g i1) =>
            (path_universe (POCase_E _f ...))^
        |} (inr false) y =
        Build_span_cocone B0 C0
          (fun x0 : A =>
           path_universe_uncurried
             (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
          (inr false) y)
       :
       {|
         legs :=
           fun (i1 : Graph.graph0 span_graph)
             (x0 : span f g i1) => POCase_E (i1; x0);
         legs_comm :=
           fun (i1 j0 : Graph.graph0 span_graph)
             (g0 : Graph.graph1 span_graph i1 j0)
             (x0 : span f g i1) =>
           (path_universe (POCase_E _f (g0; 1)))^
       |} (inr false) ==
       Build_span_cocone B0 C0
         (fun x0 : A =>
          path_universe_uncurried
            (equiv_compose (g0 x0) (f0 x0)^-1%equiv))
         (inr false)) b
 end) j (((span f g) _f g1) x) @
legs_comm
  (Build_span_cocone B0 C0
     (fun x0 : A =>
      path_universe_uncurried
        (equiv_compose (g0 x0) (f0 x0)^-1%equiv))) i j
  g1 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)
x: Colimit (span f g)
forall x : A,
(path_universe
   (fun y : A0 x => transport B0 1 (f0 x y)))^ @
path_universe_uncurried (g0 x) =
1 @
path_universe_uncurried
  (equiv_compose (g0 x) (f0 x)^-1)
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)
forall x : A,
(path_universe
   (fun y : A0 x => transport C0 1 (g0 x y)))^ @
path_universe_uncurried (g0 x) = 1
        *
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)
forall x : A,
(path_universe
   (fun y : A0 x => transport B0 1 (f0 x y)))^ @
path_universe_uncurried (g0 x) =
1 @
path_universe_uncurried
  (equiv_compose (g0 x) (f0 x)^-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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
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 x : A, A0 x <~> B0 (f x)
g0: forall x : A, A0 x <~> C0 (g x)
x: Colimit (span f g)
forall x : A,
(path_universe
   (fun y : A0 x => transport C0 1 (g0 x y)))^ @
path_universe_uncurried (g0 x) = 1 intros; apply concat_Vp.
  Defined.

End POCase.