(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about disjoint unions *)

Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Empty Types.Unit Types.Prod Types.Sigma.
(** The following are only required for the equivalence between [sum] and a sigma type *)
Require Import Types.Bool.

Local Open Scope trunc_scope.
Local Open Scope path_scope.

Generalizable Variables X A B f g n.

Scheme sum_ind := Induction for sum Sort Type.
Arguments sum_ind {A B} P f g s : rename.

Scheme sum_rec := Minimality for sum Sort Type.
Arguments sum_rec {A B} P f g s : rename.

(** ** CoUnpacking *)

(** Sums are coproducts, so there should be a dual to [unpack_prod].  I'm not sure what it is, though. *)

(** ** Eta conversion *)

Definition eta_sum `(z : A + B) : match z with
                                    | inl z' => inl z'
                                    | inr z' => inr z'
                                  end = z
  := match z with inl _ => 1 | inr _ => 1 end.

(** ** Paths *)

Definition path_sum {A B : Type} (z z' : A + B)
           (pq : match z, z' with
                   | inl z0, inl z'0 => z0 = z'0
                   | inr z0, inr z'0 => z0 = z'0
                   | _, _ => Empty
                 end)
: z = z'.
A, B: Type
z, z': A + B
pq: match z with
| inl z0 =>
    match z' with
    | inl z'0 => z0 = z'0
    | inr _ => Empty
    end
| inr z0 =>
    match z' with
    | inl _ => Empty
    | inr z'0 => z0 = z'0
    end
end
z = z'
  destruct z, z'.
A, B: Type
a, a0: A
pq: a = a0
inl a = inl a0
A, B: Type
a: A
b: B
pq: Empty
inl a = inr b
A, B: Type
b: B
a: A
pq: Empty
inr b = inl a
A, B: Type
b, b0: B
pq: b = b0
inr b = inr b0
  all:try apply ap, pq.
A, B: Type
a: A
b: B
pq: Empty
inl a = inr b
A, B: Type
b: B
a: A
pq: Empty
inr b = inl a
  all:elim pq.
Defined.

Definition path_sum_inv {A B : Type} {z z' : A + B}
           (pq : z = z')
: match z, z' with
    | inl z0, inl z'0 => z0 = z'0
    | inr z0, inr z'0 => z0 = z'0
    | _, _ => Empty
  end
  := match pq with
       | 1 => match z with
                | inl _ => 1
                | inr _ => 1
              end
     end.

Definition inl_ne_inr {A B : Type} (a : A) (b : B)
: inl a <> inr b
:= path_sum_inv.

Definition inr_ne_inl {A B : Type} (b : B) (a : A)
: inr b <> inl a
:= path_sum_inv.

(** This version produces only paths between closed terms, as opposed to paths between arbitrary inhabitants of sum types. *)
Definition path_sum_inl {A : Type} (B : Type) {x x' : A}
: inl x = inl x' -> x = x'
  := fun p => @path_sum_inv A B _ _ p.

Definition path_sum_inr (A : Type) {B : Type} {x x' : B}
: inr x = inr x' -> x = x'
  := fun p => @path_sum_inv A B _ _ p.

(** This lets us identify the path space of a sum type, up to equivalence. *)

Definition eisretr_path_sum {A B} {z z' : A + B}
: (path_sum z z') o (@path_sum_inv _ _ z z') == idmap
  := fun p => match p as p in (_ = z') return
                    path_sum z z' (path_sum_inv p) = p
              with
                | 1 => match z as z return
                             path_sum z z (path_sum_inv 1) = 1
                       with
                         | inl _ => 1
                         | inr _ => 1
                       end
              end.

Definition eissect_path_sum {A B} {z z' : A + B}
: (@path_sum_inv _ _ z z') o (path_sum z z') == idmap.
A, B: Type
z, z': A + B
path_sum_inv o path_sum z z' == idmap
Proof.
A, B: Type
z, z': A + B
path_sum_inv o path_sum z z' == idmap
  intro p.
A, B: Type
z, z': A + B
p: match z with
| inl z0 =>
    match z' with
    | inl z'0 => z0 = z'0
    | inr _ => Empty
    end
| inr z0 =>
    match z' with
    | inl _ => Empty
    | inr z'0 => z0 = z'0
    end
end
path_sum_inv (path_sum z z' p) = p
  destruct z, z', p; exact idpath.
Defined.

Global Instance isequiv_path_sum {A B : Type} {z z' : A + B}
: IsEquiv (path_sum z z') | 0.
A, B: Type
z, z': A + B
IsEquiv (path_sum z z')
Proof.
A, B: Type
z, z': A + B
IsEquiv (path_sum z z')
  refine (Build_IsEquiv _ _
                       (path_sum z z')
                       (@path_sum_inv _ _ z z')
                       (@eisretr_path_sum A B z z')
                       (@eissect_path_sum A B z z')
                       _).
A, B: Type
z, z': A + B
forall
x : match z with
    | inl z0 =>
        match z' with
        | inl z'0 => z0 = z'0
        | inr _ => Empty
        end
    | inr z0 =>
        match z' with
        | inl _ => Empty
        | inr z'0 => z0 = z'0
        end
    end,
eisretr_path_sum (path_sum z z' x) =
ap (path_sum z z') (eissect_path_sum x)
  destruct z, z';
    intros [];
    exact idpath.
Defined.

Definition equiv_path_sum {A B : Type} (z z' : A + B)
  := Build_Equiv _ _ _ (@isequiv_path_sum A B z z').

(** ** Fibers of [inl] and [inr] *)

(** It follows that the fibers of [inl] and [inr] are decidable hprops. *)

Global Instance ishprop_hfiber_inl {A B : Type} (z : A + B)
: IsHProp (hfiber inl z).
A, B: Type
z: A + B
IsHProp (hfiber inl z)
Proof.
A, B: Type
z: A + B
IsHProp (hfiber inl z)
  destruct z as [a|b]; unfold hfiber.
A, B: Type
a: A
IsHProp {x : A & inl x = inl a}
A, B: Type
b: B
IsHProp {x : A & inl x = inr b}
  -
A, B: Type
a: A
IsHProp {x : A & inl x = inl a} refine (istrunc_equiv_istrunc _
              (equiv_functor_sigma_id
                 (fun x => equiv_path_sum (inl x) (inl a)))).
  -
A, B: Type
b: B
IsHProp {x : A & inl x = inr b} refine (istrunc_isequiv_istrunc _
              (fun xp => inl_ne_inr (xp.1) b xp.2)^-1).
Defined.

Global Instance decidable_hfiber_inl {A B : Type} (z : A + B)
: Decidable (hfiber inl z).
A, B: Type
z: A + B
Decidable (hfiber inl z)
Proof.
A, B: Type
z: A + B
Decidable (hfiber inl z)
  destruct z as [a|b]; unfold hfiber.
A, B: Type
a: A
Decidable {x : A & inl x = inl a}
A, B: Type
b: B
Decidable {x : A & inl x = inr b}
  -
A, B: Type
a: A
Decidable {x : A & inl x = inl a} refine (decidable_equiv' _
              (equiv_functor_sigma_id
                 (fun x => equiv_path_sum (inl x) (inl a))) _).
  -
A, B: Type
b: B
Decidable {x : A & inl x = inr b} refine (decidable_equiv _
              (fun xp => inl_ne_inr (xp.1) b xp.2)^-1 _).
Defined.

Global Instance ishprop_hfiber_inr {A B : Type} (z : A + B)
: IsHProp (hfiber inr z).
A, B: Type
z: A + B
IsHProp (hfiber inr z)
Proof.
A, B: Type
z: A + B
IsHProp (hfiber inr z)
  destruct z as [a|b]; unfold hfiber.
A, B: Type
a: A
IsHProp {x : B & inr x = inl a}
A, B: Type
b: B
IsHProp {x : B & inr x = inr b}
  -
A, B: Type
a: A
IsHProp {x : B & inr x = inl a} refine (istrunc_isequiv_istrunc _
              (fun xp => inr_ne_inl (xp.1) a xp.2)^-1).
  -
A, B: Type
b: B
IsHProp {x : B & inr x = inr b} refine (istrunc_equiv_istrunc _
              (equiv_functor_sigma_id
                 (fun x => equiv_path_sum (inr x) (inr b)))).
Defined.

Global Instance decidable_hfiber_inr {A B : Type} (z : A + B)
: Decidable (hfiber inr z).
A, B: Type
z: A + B
Decidable (hfiber inr z)
Proof.
A, B: Type
z: A + B
Decidable (hfiber inr z)
  destruct z as [a|b]; unfold hfiber.
A, B: Type
a: A
Decidable {x : B & inr x = inl a}
A, B: Type
b: B
Decidable {x : B & inr x = inr b}
  -
A, B: Type
a: A
Decidable {x : B & inr x = inl a} refine (decidable_equiv _
              (fun xp => inr_ne_inl (xp.1) a xp.2)^-1 _).
  -
A, B: Type
b: B
Decidable {x : B & inr x = inr b} refine (decidable_equiv' _
              (equiv_functor_sigma_id
                 (fun x => equiv_path_sum (inr x) (inr b))) _).
Defined.

(** ** Decomposition *)

(** Conversely, a decidable predicate decomposes a type as a sum. *)

Section DecidableSum.
  Context `{Funext} {A : Type} (P : A -> Type)
          `{forall a, IsHProp (P a)} `{forall a, Decidable (P a)}.

  Definition equiv_decidable_sum
    : A <~> {x:A & P x} + {x:A & ~(P x)}.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
A <~> {x : A & P x} + {x : A & ~ P x}
  Proof.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
A <~> {x : A & P x} + {x : A & ~ P x}
    transparent assert (f : (A -> {x:A & P x} + {x:A & ~(P x)})).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
A -> {x : A & P x} + {x : A & ~ P x}
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= ?Goal: A -> {x : A & P x} + {x : A & ~ P x}
A <~> {x : A & P x} + {x : A & ~ P x}
    {
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
A -> {x : A & P x} + {x : A & ~ P x} intros x.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
x: A
{x : A & P x} + {x : A & ~ P x}
      destruct (dec (P x)) as [p|np].
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
x: A
p: P x
{x : A & P x} + {x : A & ~ P x}
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
x: A
np: ~ P x
{x : A & P x} + {x : A & ~ P x}
      -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
x: A
p: P x
{x : A & P x} + {x : A & ~ P x} exact (inl (x;p)).
      -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
x: A
np: ~ P x
{x : A & P x} + {x : A & ~ P x} exact (inr (x;np)). }
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
A <~> {x : A & P x} + {x : A & ~ P x}
    refine (Build_Equiv _ _ f _).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
IsEquiv f
    refine (isequiv_adjointify
              _ (fun z => match z with
                          | inl (x;p) => x
                          | inr (x;np) => x
                          end) _ _).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
(fun x : {x : A & P x} + {x : A & ~ P x} =>
 f match x with
   | inl y => y.1
   | inr y => y.1
   end) == idmap
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
(fun x : A =>
 match f x with
 | inl y => y.1
 | inr y => y.1
 end) == idmap
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
(fun x : {x : A & P x} + {x : A & ~ P x} =>
 f match x with
   | inl y => y.1
   | inr y => y.1
   end) == idmap intros [[x p]|[x np]]; unfold f;
        destruct (dec (P x)) as [p'|np'].
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
p, p': P x
inl (x; p') = inl (x; p)
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
p: P x
np': ~ P x
inr (x; np') = inl (x; p)
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
np: ~ P x
p': P x
inl (x; p') = inr (x; np)
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
np, np': ~ P x
inr (x; np') = inr (x; np)
      +
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
p, p': P x
inl (x; p') = inl (x; p) apply ap, ap, path_ishprop.
      +
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
p: P x
np': ~ P x
inr (x; np') = inl (x; p) elim (np' p).
      +
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
np: ~ P x
p': P x
inl (x; p') = inr (x; np) elim (np p').
      +
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
np, np': ~ P x
inr (x; np') = inr (x; np) apply ap, ap, path_ishprop.
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
(fun x : A =>
 match f x with
 | inl y => y.1
 | inr y => y.1
 end) == idmap intros x; unfold f.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
f:= fun x : A =>
let s := dec (P x) in
match s with
| inl p => (fun p0 : P x => inl (x; p0)) p
| inr n => (fun np : ~ P x => inr (x; np)) n
end: A -> {x : A & P x} + {x : A & ~ P x}
x: A
match
  match dec (P x) with
  | inl p => inl (x; p)
  | inr n => inr (x; n)
  end
with
| inl y => y.1
| inr y => y.1
end = x
      destruct (dec (P x)); cbn; reflexivity.
  Defined.

  Definition equiv_decidable_sum_l (a : A) (p : P a)
    : equiv_decidable_sum a = inl (a;p).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p: P a
equiv_decidable_sum a = inl (a; p)
  Proof.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p: P a
equiv_decidable_sum a = inl (a; p)
    unfold equiv_decidable_sum; cbn.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p: P a
match dec (P a) with
| inl p => inl (a; p)
| inr n => inr (a; n)
end = inl (a; p)
    destruct (dec (P a)) as [p'|np'].
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p, p': P a
inl (a; p') = inl (a; p)
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p: P a
np': ~ P a
inr (a; np') = inl (a; p)
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p, p': P a
inl (a; p') = inl (a; p) apply ap, path_sigma_hprop; reflexivity.
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
p: P a
np': ~ P a
inr (a; np') = inl (a; p) elim (np' p).
  Defined.

  Definition equiv_decidable_sum_r (a : A) (np : ~ (P a))
    : equiv_decidable_sum a = inr (a;np).
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np: ~ P a
equiv_decidable_sum a = inr (a; np)
  Proof.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np: ~ P a
equiv_decidable_sum a = inr (a; np)
    unfold equiv_decidable_sum; cbn.
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np: ~ P a
match dec (P a) with
| inl p => inl (a; p)
| inr n => inr (a; n)
end = inr (a; np)
    destruct (dec (P a)) as [p'|np'].
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np: ~ P a
p': P a
inl (a; p') = inr (a; np)
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np, np': ~ P a
inr (a; np') = inr (a; np)
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np: ~ P a
p': P a
inl (a; p') = inr (a; np) elim (np p').
    -
H: Funext
A: Type
P: A -> Type
H0: forall a : A, IsHProp (P a)
H1: forall a : A, Decidable (P a)
a: A
np, np': ~ P a
inr (a; np') = inr (a; np) apply ap, path_sigma_hprop; reflexivity.
  Defined.

End DecidableSum.

(** ** Transport *)

Definition transport_sum {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
           (z : P a + Q a)
: transport (fun a => P a + Q a) p z = match z with
                                         | inl z' => inl (p # z')
                                         | inr z' => inr (p # z')
                                       end
  := match p with idpath => match z with inl _ => 1 | inr _ => 1 end end.

(** ** Detecting the summands *)

Definition is_inl_and {A B} (P : A -> Type@{p}) : A + B -> Type@{p}
  := fun x => match x with inl a => P a | inr _ => Empty end.

Definition is_inr_and {A B} (P : B -> Type@{p}) : A + B -> Type@{p}
  := fun x => match x with inl _ => Empty | inr b => P b end.

Definition is_inl {A B} : A + B -> Type0
  := is_inl_and (fun _ => Unit).

Definition is_inr {A B} : A + B -> Type0
  := is_inr_and (fun _ => Unit).

Global Instance ishprop_is_inl {A B} (x : A + B)
: IsHProp (is_inl x).
A, B: Type
x: A + B
IsHProp (is_inl x)
Proof.
A, B: Type
x: A + B
IsHProp (is_inl x)
  destruct x; exact _.
Defined.

Global Instance ishprop_is_inr {A B} (x : A + B)
: IsHProp (is_inr x).
A, B: Type
x: A + B
IsHProp (is_inr x)
Proof.
A, B: Type
x: A + B
IsHProp (is_inr x)
  destruct x; exact _.
Defined.

Global Instance decidable_is_inl {A B} (x : A + B)
: Decidable (is_inl x).
A, B: Type
x: A + B
Decidable (is_inl x)
Proof.
A, B: Type
x: A + B
Decidable (is_inl x)
  destruct x; exact _.
Defined.

Global Instance decidable_is_inr {A B} (x : A + B)
: Decidable (is_inr x).
A, B: Type
x: A + B
Decidable (is_inr x)
Proof.
A, B: Type
x: A + B
Decidable (is_inr x)
  destruct x; exact _.
Defined.

Definition un_inl {A B} (z : A + B)
: is_inl z -> A.
A, B: Type
z: A + B
is_inl z -> A
Proof.
A, B: Type
z: A + B
is_inl z -> A
  destruct z as [a|b].
A, B: Type
a: A
is_inl (inl a) -> A
A, B: Type
b: B
is_inl (inr b) -> A
  -
A, B: Type
a: A
is_inl (inl a) -> A intros; exact a.
  -
A, B: Type
b: B
is_inl (inr b) -> A intros e; elim e.
Defined.

Definition un_inr {A B} (z : A + B)
: is_inr z -> B.
A, B: Type
z: A + B
is_inr z -> B
Proof.
A, B: Type
z: A + B
is_inr z -> B
  destruct z as [a|b].
A, B: Type
a: A
is_inr (inl a) -> B
A, B: Type
b: B
is_inr (inr b) -> B
  -
A, B: Type
a: A
is_inr (inl a) -> B intros e; elim e.
  -
A, B: Type
b: B
is_inr (inr b) -> B intros; exact b.
Defined.

Definition is_inl_not_inr {A B} (x : A + B)  (na : ~ A)
: is_inr x
  := match x with
     | inl a => na a
     | inr b => tt
     end.

Definition is_inr_not_inl {A B} (x : A + B)  (nb : ~ B)
: is_inl x
  := match x with
     | inl a => tt
     | inr b => nb b
     end.

Definition un_inl_inl {A B : Type} (a : A) (w : is_inl (inl a))
: un_inl (@inl A B a) w = a
  := 1.

Definition un_inr_inr {A B : Type} (b : B) (w : is_inr (inr b))
: un_inr (@inr A B b) w = b
  := 1.

Definition inl_un_inl {A B : Type} (z : A + B) (w : is_inl z)
: inl (un_inl z w) = z.
A, B: Type
z: A + B
w: is_inl z
inl (un_inl z w) = z
Proof.
A, B: Type
z: A + B
w: is_inl z
inl (un_inl z w) = z
  destruct z as [a|b]; simpl.
A, B: Type
a: A
w: is_inl (inl a)
inl a = inl a
A, B: Type
b: B
w: is_inl (inr b)
inl (Empty_rect (fun _ : Empty => A) w) = inr b
  -
A, B: Type
a: A
w: is_inl (inl a)
inl a = inl a reflexivity.
  -
A, B: Type
b: B
w: is_inl (inr b)
inl (Empty_rect (fun _ : Empty => A) w) = inr b elim w.
Defined.

Definition inr_un_inr {A B : Type} (z : A + B) (w : is_inr z)
: inr (un_inr z w) = z.
A, B: Type
z: A + B
w: is_inr z
inr (un_inr z w) = z
Proof.
A, B: Type
z: A + B
w: is_inr z
inr (un_inr z w) = z
  destruct z as [a|b]; simpl.
A, B: Type
a: A
w: is_inr (inl a)
inr (Empty_rect (fun _ : Empty => B) w) = inl a
A, B: Type
b: B
w: is_inr (inr b)
inr b = inr b
  -
A, B: Type
a: A
w: is_inr (inl a)
inr (Empty_rect (fun _ : Empty => B) w) = inl a elim w.
  -
A, B: Type
b: B
w: is_inr (inr b)
inr b = inr b reflexivity.
Defined.

Definition not_is_inl_and_inr {A B} (P : A -> Type) (Q : B -> Type)
           (x : A + B)
: is_inl_and P x -> is_inr_and Q x -> Empty.
A, B: Type
P: A -> Type
Q: B -> Type
x: A + B
is_inl_and P x -> is_inr_and Q x -> Empty
Proof.
A, B: Type
P: A -> Type
Q: B -> Type
x: A + B
is_inl_and P x -> is_inr_and Q x -> Empty
  destruct x as [a|b]; simpl.
A, B: Type
P: A -> Type
Q: B -> Type
a: A
P a -> Empty -> Empty
A, B: Type
P: A -> Type
Q: B -> Type
b: B
Empty -> Q b -> Empty
  -
A, B: Type
P: A -> Type
Q: B -> Type
a: A
P a -> Empty -> Empty exact (fun _ e => e).
  -
A, B: Type
P: A -> Type
Q: B -> Type
b: B
Empty -> Q b -> Empty exact (fun e _ => e).
Defined.

Definition not_is_inl_and_inr' {A B} (x : A + B)
: is_inl x -> is_inr x -> Empty
  := not_is_inl_and_inr (fun _ => Unit) (fun _ => Unit) x.

Definition is_inl_or_is_inr {A B} (x : A + B)
: (is_inl x) + (is_inr x)
  := match x return (is_inl x) + (is_inr x) with
       | inl _ => inl tt
       | inr _ => inr tt
     end.

Definition is_inl_ind {A B : Type} (P : A + B -> Type)
           (f : forall a:A, P (inl a))
: forall (x:A+B), is_inl x -> P x.
A, B: Type
P: A + B -> Type
f: forall a : A, P (inl a)
forall x : A + B, is_inl x -> P x
Proof.
A, B: Type
P: A + B -> Type
f: forall a : A, P (inl a)
forall x : A + B, is_inl x -> P x
  intros [a|b] H; [ exact (f a) | elim H ].
Defined.

Definition is_inr_ind {A B : Type} (P : A + B -> Type)
           (f : forall b:B, P (inr b))
: forall (x:A+B), is_inr x -> P x.
A, B: Type
P: A + B -> Type
f: forall b : B, P (inr b)
forall x : A + B, is_inr x -> P x
Proof.
A, B: Type
P: A + B -> Type
f: forall b : B, P (inr b)
forall x : A + B, is_inr x -> P x
  intros [a|b] H; [ elim H | exact (f b) ].
Defined.

(** ** Functorial action *)

Section FunctorSum.
  Context {A A' B B' : Type} (f : A -> A') (g : B -> B').

  Definition functor_sum : A + B -> A' + B'
    := fun z => match z with inl z' => inl (f z') | inr z' => inr (g z') end.

  (** The fibers of [functor_sum] are those of [f] and [g]. *)
  Definition hfiber_functor_sum_l (a' : A')
  : hfiber functor_sum (inl a') <~> hfiber f a'.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber functor_sum (inl a') <~> hfiber f a'
  Proof.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber functor_sum (inl a') <~> hfiber f a'
    simple refine (equiv_adjointify _ _ _ _).
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber functor_sum (inl a') -> hfiber f a'
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber f a' -> hfiber functor_sum (inl a')
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
?f o ?g == idmap
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
?g o ?f == idmap
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber functor_sum (inl a') -> hfiber f a' intros [[a|b] p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
hfiber f a'
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
b: B
p: functor_sum (inr b) = inl a'
hfiber f a'
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
hfiber f a' exists a.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
f a = a'
        exact (path_sum_inl _ p).
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
b: B
p: functor_sum (inr b) = inl a'
hfiber f a' elim (inr_ne_inl _ _ p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
hfiber f a' -> hfiber functor_sum (inl a') intros [a p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: f a = a'
hfiber functor_sum (inl a')
      exists (inl a).
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: f a = a'
functor_sum (inl a) = inl a'
      exact (ap inl p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
(fun X : hfiber functor_sum (inl a') =>
 (fun proj1 : A + B =>
  match
    proj1 as s
    return (functor_sum s = inl a' -> hfiber f a')
  with
  | inl a =>
      (fun (a0 : A)
         (p : functor_sum (inl a0) = inl a') =>
       (a0; path_sum_inl B' p)) a
  | inr b =>
      (fun (b0 : B)
         (p : functor_sum (inr b0) = inl a') =>
       Empty_rect (fun _ : Empty => hfiber f a')
         (inr_ne_inl (g b0) a' p)) b
  end) X.1 X.2)
o (fun X : hfiber f a' =>
   (fun (a : A) (p : f a = a') => (inl a; ap inl p))
     X.1 X.2) == idmap intros [a p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: f a = a'
(a; path_sum_inl B' (ap inl p)) = (a; p)
      apply ap.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: f a = a'
path_sum_inl B' (ap inl p) = p
      (** Why doesn't Coq find this? *)
      pose (@isequiv_path_sum A' B' (inl (f a)) (inl a')).
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: f a = a'
i:= isequiv_path_sum: IsEquiv (path_sum (inl (f a)) (inl a'))
path_sum_inl B' (ap inl p) = p
      exact (eissect (@path_sum A' B' (inl (f a)) (inl a')) p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
(fun X : hfiber f a' =>
 (fun (a : A) (p : f a = a') => (inl a; ap inl p)) X.1
   X.2)
o (fun X : hfiber functor_sum (inl a') =>
   (fun proj1 : A + B =>
    match
      proj1 as s
      return (functor_sum s = inl a' -> hfiber f a')
    with
    | inl a =>
        (fun (a0 : A)
           (p : functor_sum (inl a0) = inl a') =>
         (a0; path_sum_inl B' p)) a
    | inr b =>
        (fun (b0 : B)
           (p : functor_sum (inr b0) = inl a') =>
         Empty_rect (fun _ : Empty => hfiber f a')
           (inr_ne_inl (g b0) a' p)) b
    end) X.1 X.2) == idmap intros [[a|b] p]; simpl.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
(inl a; ap inl (path_sum_inl B' p)) = (inl a; p)
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
b: B
p: functor_sum (inr b) = inl a'
(inl
   (Empty_rect (fun _ : Empty => hfiber f a')
      (inr_ne_inl (g b) a' p)).1;
ap inl
  (Empty_rect (fun _ : Empty => hfiber f a')
     (inr_ne_inl (g b) a' p)).2) = (inr b; p)
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
(inl a; ap inl (path_sum_inl B' p)) = (inl a; p) apply ap.
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
ap inl (path_sum_inl B' p) = p
        pose (@isequiv_path_sum A' B' (inl (f a)) (inl a')).
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
a: A
p: functor_sum (inl a) = inl a'
i:= isequiv_path_sum: IsEquiv (path_sum (inl (f a)) (inl a'))
ap inl (path_sum_inl B' p) = p
        exact (eisretr (@path_sum A' B' (inl (f a)) (inl a')) p).
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
a': A'
b: B
p: functor_sum (inr b) = inl a'
(inl
   (Empty_rect (fun _ : Empty => hfiber f a')
      (inr_ne_inl (g b) a' p)).1;
ap inl
  (Empty_rect (fun _ : Empty => hfiber f a')
     (inr_ne_inl (g b) a' p)).2) = (inr b; p) elim (inr_ne_inl _ _ p).
  Defined.

  Definition hfiber_functor_sum_r (b' : B')
  : hfiber functor_sum (inr b') <~> hfiber g b'.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber functor_sum (inr b') <~> hfiber g b'
  Proof.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber functor_sum (inr b') <~> hfiber g b'
    simple refine (equiv_adjointify _ _ _ _).
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber functor_sum (inr b') -> hfiber g b'
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber g b' -> hfiber functor_sum (inr b')
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
?f o ?g == idmap
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
?g o ?f == idmap
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber functor_sum (inr b') -> hfiber g b' intros [[a|b] p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
a: A
p: functor_sum (inl a) = inr b'
hfiber g b'
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
hfiber g b'
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
a: A
p: functor_sum (inl a) = inr b'
hfiber g b' elim (inl_ne_inr _ _ p).
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
hfiber g b' exists b.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
g b = b'
        exact (path_sum_inr _ p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
hfiber g b' -> hfiber functor_sum (inr b') intros [b p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: g b = b'
hfiber functor_sum (inr b')
      exists (inr b).
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: g b = b'
functor_sum (inr b) = inr b'
      exact (ap inr p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
(fun X : hfiber functor_sum (inr b') =>
 (fun proj1 : A + B =>
  match
    proj1 as s
    return (functor_sum s = inr b' -> hfiber g b')
  with
  | inl a =>
      (fun (a0 : A)
         (p : functor_sum (inl a0) = inr b') =>
       Empty_rect (fun _ : Empty => hfiber g b')
         (inl_ne_inr (f a0) b' p)) a
  | inr b =>
      (fun (b0 : B)
         (p : functor_sum (inr b0) = inr b') =>
       (b0; path_sum_inr A' p)) b
  end) X.1 X.2)
o (fun X : hfiber g b' =>
   (fun (b : B) (p : g b = b') => (inr b; ap inr p))
     X.1 X.2) == idmap intros [b p].
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: g b = b'
(b; path_sum_inr A' (ap inr p)) = (b; p)
      apply ap.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: g b = b'
path_sum_inr A' (ap inr p) = p
      (** Why doesn't Coq find this? *)
      pose (@isequiv_path_sum A' B' (inr (g b)) (inr b')).
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: g b = b'
i:= isequiv_path_sum: IsEquiv (path_sum (inr (g b)) (inr b'))
path_sum_inr A' (ap inr p) = p
      exact (eissect (@path_sum A' B' (inr (g b)) (inr b')) p).
    -
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
(fun X : hfiber g b' =>
 (fun (b : B) (p : g b = b') => (inr b; ap inr p)) X.1
   X.2)
o (fun X : hfiber functor_sum (inr b') =>
   (fun proj1 : A + B =>
    match
      proj1 as s
      return (functor_sum s = inr b' -> hfiber g b')
    with
    | inl a =>
        (fun (a0 : A)
           (p : functor_sum (inl a0) = inr b') =>
         Empty_rect (fun _ : Empty => hfiber g b')
           (inl_ne_inr (f a0) b' p)) a
    | inr b =>
        (fun (b0 : B)
           (p : functor_sum (inr b0) = inr b') =>
         (b0; path_sum_inr A' p)) b
    end) X.1 X.2) == idmap intros [[a|b] p]; simpl.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
a: A
p: functor_sum (inl a) = inr b'
(inr
   (Empty_rect (fun _ : Empty => hfiber g b')
      (inl_ne_inr (f a) b' p)).1;
ap inr
  (Empty_rect (fun _ : Empty => hfiber g b')
     (inl_ne_inr (f a) b' p)).2) = (inl a; p)
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
(inr b; ap inr (path_sum_inr A' p)) = (inr b; p)
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
a: A
p: functor_sum (inl a) = inr b'
(inr
   (Empty_rect (fun _ : Empty => hfiber g b')
      (inl_ne_inr (f a) b' p)).1;
ap inr
  (Empty_rect (fun _ : Empty => hfiber g b')
     (inl_ne_inr (f a) b' p)).2) = (inl a; p) elim (inl_ne_inr _ _ p).
      +
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
(inr b; ap inr (path_sum_inr A' p)) = (inr b; p) apply ap.
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
ap inr (path_sum_inr A' p) = p
        pose (@isequiv_path_sum A' B' (inr (g b)) (inr b')).
A, A', B, B': Type
f: A -> A'
g: B -> B'
b': B'
b: B
p: functor_sum (inr b) = inr b'
i:= isequiv_path_sum: IsEquiv (path_sum (inr (g b)) (inr b'))
ap inr (path_sum_inr A' p) = p
        exact (eisretr (@path_sum A' B' (inr (g b)) (inr b')) p).
  Defined.

End FunctorSum.

Definition functor_sum_homotopic {A A' B B' : Type}
  {f f' : A -> A'} {g g' : B -> B'} (p : f == f') (q : g == g')
  : functor_sum f g == functor_sum f' g'.
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
functor_sum f g == functor_sum f' g'
Proof.
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
functor_sum f g == functor_sum f' g'
  intros [a|b].
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
a: A
functor_sum f g (inl a) = functor_sum f' g' (inl a)
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
b: B
functor_sum f g (inr b) = functor_sum f' g' (inr b)
  -
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
a: A
functor_sum f g (inl a) = functor_sum f' g' (inl a) exact (ap inl (p a)).
  -
A, A', B, B': Type
f, f': A -> A'
g, g': B -> B'
p: f == f'
q: g == g'
b: B
functor_sum f g (inr b) = functor_sum f' g' (inr b) exact (ap inr (q b)).
Defined.

(** ** "Unfunctorial action" *)

(** Not every function [A + B -> A' + B'] is of the form [functor_sum f g].  However, this is the case if it preserves the summands, i.e. if it maps [A] into [A'] and [B] into [B'].  More generally, if a function [A + B -> A' + B'] maps [A] into [A'] only, then we can extract from it a function [A -> A'].  Since these operations are a sort of inverse to [functor_sum], we call them [unfunctor_sum_*]. *)

Definition unfunctor_sum_l {A A' B B' : Type} (h : A + B -> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
: A -> A'
  := fun a => un_inl (h (inl a)) (Ha a).

Definition unfunctor_sum_r {A A' B B' : Type} (h : A + B -> A' + B')
           (Hb : forall b:B, is_inr (h (inr b)))
: B -> B'
  := fun b => un_inr (h (inr b)) (Hb b).

Definition unfunctor_sum_eta {A A' B B' : Type} (h : A + B -> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: functor_sum (unfunctor_sum_l h Ha) (unfunctor_sum_r h Hb) == h.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
functor_sum (unfunctor_sum_l h Ha)
  (unfunctor_sum_r h Hb) == h
Proof.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
functor_sum (unfunctor_sum_l h Ha)
  (unfunctor_sum_r h Hb) == h
  intros [a|b]; simpl.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
inl (unfunctor_sum_l h Ha a) = h (inl a)
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
inr (unfunctor_sum_r h Hb b) = h (inr b)
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
inl (unfunctor_sum_l h Ha a) = h (inl a) unfold unfunctor_sum_l; apply inl_un_inl.
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
inr (unfunctor_sum_r h Hb b) = h (inr b) unfold unfunctor_sum_r; apply inr_un_inr.
Defined.

Definition unfunctor_sum_l_beta {A A' B B' : Type} (h : A + B -> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
: inl o unfunctor_sum_l h Ha == h o inl.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
inl o unfunctor_sum_l h Ha == h o inl
Proof.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
inl o unfunctor_sum_l h Ha == h o inl
  intros a; unfold unfunctor_sum_l; apply inl_un_inl.
Defined.

Definition unfunctor_sum_r_beta {A A' B B' : Type} (h : A + B -> A' + B')
           (Hb : forall b:B, is_inr (h (inr b)))
: inr o unfunctor_sum_r h Hb == h o inr.
A, A', B, B': Type
h: A + B -> A' + B'
Hb: forall b : B, is_inr (h (inr b))
inr o unfunctor_sum_r h Hb == h o inr
Proof.
A, A', B, B': Type
h: A + B -> A' + B'
Hb: forall b : B, is_inr (h (inr b))
inr o unfunctor_sum_r h Hb == h o inr
  intros b; unfold unfunctor_sum_r; apply inr_un_inr.
Defined.

Definition unfunctor_sum_l_compose {A A' A'' B B' B'' : Type}
           (h : A + B -> A' + B') (k : A' + B' -> A'' + B'')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Ha' : forall a':A', is_inl (k (inl a')))
: unfunctor_sum_l k Ha' o unfunctor_sum_l h Ha
  == unfunctor_sum_l (k o h)
     (fun a => is_inl_ind (fun x' => is_inl (k x')) Ha' (h (inl a)) (Ha a)).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
unfunctor_sum_l k Ha' o unfunctor_sum_l h Ha ==
unfunctor_sum_l (k o h)
  (fun a : A =>
   is_inl_ind (fun x' : A' + B' => is_inl (k x')) Ha'
     (h (inl a)) (Ha a))
Proof.
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
unfunctor_sum_l k Ha' o unfunctor_sum_l h Ha ==
unfunctor_sum_l (k o h)
  (fun a : A =>
   is_inl_ind (fun x' : A' + B' => is_inl (k x')) Ha'
     (h (inl a)) (Ha a))
  intros a.
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
a: A
unfunctor_sum_l k Ha' (unfunctor_sum_l h Ha a) =
unfunctor_sum_l (fun x : A + B => k (h x))
  (fun a : A =>
   is_inl_ind (fun x' : A' + B' => is_inl (k x')) Ha'
     (h (inl a)) (Ha a)) a
  refine (path_sum_inl B'' _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
a: A
inl (unfunctor_sum_l k Ha' (unfunctor_sum_l h Ha a)) =
inl
  (unfunctor_sum_l (fun x : A + B => k (h x))
     (fun a : A =>
      is_inl_ind (fun x' : A' + B' => is_inl (k x'))
        Ha' (h (inl a)) (Ha a)) a)
  refine (unfunctor_sum_l_beta _ _ _ @ _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
a: A
k (inl (unfunctor_sum_l h Ha a)) =
inl
  (unfunctor_sum_l (fun x : A + B => k (h x))
     (fun a : A =>
      is_inl_ind (fun x' : A' + B' => is_inl (k x'))
        Ha' (h (inl a)) (Ha a)) a)
  refine (ap k (unfunctor_sum_l_beta _ _ _) @ _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Ha: forall a : A, is_inl (h (inl a))
Ha': forall a' : A', is_inl (k (inl a'))
a: A
k (h (inl a)) =
inl
  (unfunctor_sum_l (fun x : A + B => k (h x))
     (fun a : A =>
      is_inl_ind (fun x' : A' + B' => is_inl (k x'))
        Ha' (h (inl a)) (Ha a)) a)
  refine ((unfunctor_sum_l_beta _ _ _)^).
Defined.

Definition unfunctor_sum_r_compose {A A' A'' B B' B'' : Type}
           (h : A + B -> A' + B') (k : A' + B' -> A'' + B'')
           (Hb : forall b:B, is_inr (h (inr b)))
           (Hb' : forall b':B', is_inr (k (inr b')))
: unfunctor_sum_r k Hb' o unfunctor_sum_r h Hb
  == unfunctor_sum_r (k o h)
     (fun b => is_inr_ind (fun x' => is_inr (k x')) Hb' (h (inr b)) (Hb b)).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
unfunctor_sum_r k Hb' o unfunctor_sum_r h Hb ==
unfunctor_sum_r (k o h)
  (fun b : B =>
   is_inr_ind (fun x' : A' + B' => is_inr (k x')) Hb'
     (h (inr b)) (Hb b))
Proof.
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
unfunctor_sum_r k Hb' o unfunctor_sum_r h Hb ==
unfunctor_sum_r (k o h)
  (fun b : B =>
   is_inr_ind (fun x' : A' + B' => is_inr (k x')) Hb'
     (h (inr b)) (Hb b))
  intros b.
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
b: B
unfunctor_sum_r k Hb' (unfunctor_sum_r h Hb b) =
unfunctor_sum_r (fun x : A + B => k (h x))
  (fun b : B =>
   is_inr_ind (fun x' : A' + B' => is_inr (k x')) Hb'
     (h (inr b)) (Hb b)) b
  refine (path_sum_inr A'' _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
b: B
inr (unfunctor_sum_r k Hb' (unfunctor_sum_r h Hb b)) =
inr
  (unfunctor_sum_r (fun x : A + B => k (h x))
     (fun b : B =>
      is_inr_ind (fun x' : A' + B' => is_inr (k x'))
        Hb' (h (inr b)) (Hb b)) b)
  refine (unfunctor_sum_r_beta _ _ _ @ _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
b: B
k (inr (unfunctor_sum_r h Hb b)) =
inr
  (unfunctor_sum_r (fun x : A + B => k (h x))
     (fun b : B =>
      is_inr_ind (fun x' : A' + B' => is_inr (k x'))
        Hb' (h (inr b)) (Hb b)) b)
  refine (ap k (unfunctor_sum_r_beta _ _ _) @ _).
A, A', A'', B, B', B'': Type
h: A + B -> A' + B'
k: A' + B' -> A'' + B''
Hb: forall b : B, is_inr (h (inr b))
Hb': forall b' : B', is_inr (k (inr b'))
b: B
k (h (inr b)) =
inr
  (unfunctor_sum_r (fun x : A + B => k (h x))
     (fun b : B =>
      is_inr_ind (fun x' : A' + B' => is_inr (k x'))
        Hb' (h (inr b)) (Hb b)) b)
  refine ((unfunctor_sum_r_beta _ _ _)^).
Defined.

(** [unfunctor_sum] also preserves fibers, if both summands are preserved. *)
Definition hfiber_unfunctor_sum_l {A A' B B' : Type}
           (h : A + B -> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
           (a' : A')
: hfiber (unfunctor_sum_l h Ha) a' <~> hfiber h (inl a').
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber (unfunctor_sum_l h Ha) a' <~> hfiber h (inl a')
Proof.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber (unfunctor_sum_l h Ha) a' <~> hfiber h (inl a')
  simple refine (equiv_adjointify _ _ _ _).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber (unfunctor_sum_l h Ha) a' -> hfiber h (inl a')
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber h (inl a') -> hfiber (unfunctor_sum_l h Ha) a'
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
?f o ?g == idmap
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
?g o ?f == idmap
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber (unfunctor_sum_l h Ha) a' -> hfiber h (inl a') intros [a p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
hfiber h (inl a')
    exists (inl a).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
h (inl a) = inl a'
    refine (_ @ ap inl p).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
h (inl a) = inl (unfunctor_sum_l h Ha a)
    symmetry; apply inl_un_inl.
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
hfiber h (inl a') -> hfiber (unfunctor_sum_l h Ha) a' intros [[a|b] p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
hfiber (unfunctor_sum_l h Ha) a'
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h (inr b) = inl a'
hfiber (unfunctor_sum_l h Ha) a'
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
hfiber (unfunctor_sum_l h Ha) a' exists a.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
unfunctor_sum_l h Ha a = a'
      apply path_sum_inl with B'.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
inl (unfunctor_sum_l h Ha a) = inl a'
      refine (_ @ p).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
inl (unfunctor_sum_l h Ha a) = h (inl a)
      apply inl_un_inl.
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h (inr b) = inl a'
hfiber (unfunctor_sum_l h Ha) a' specialize (Hb b).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
b: B
Hb: is_inr (h (inr b))
a': A'
p: h (inr b) = inl a'
hfiber (unfunctor_sum_l h Ha) a'
      abstract (rewrite p in Hb; elim Hb).
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
(fun X : hfiber (unfunctor_sum_l h Ha) a' =>
 (fun (a : A) (p : unfunctor_sum_l h Ha a = a') =>
  (inl a; (inl_un_inl (h (inl a)) (Ha a))^ @ ap inl p))
   X.1 X.2)
o (fun X : hfiber h (inl a') =>
   (fun proj1 : A + B =>
    match
      proj1 as s
      return
        (h s = inl a' ->
         hfiber (unfunctor_sum_l h Ha) a')
    with
    | inl a =>
        (fun (a0 : A) (p : h (inl a0) = inl a') =>
         (a0;
         path_sum_inl B'
           (inl_un_inl (h (inl a0)) (Ha a0) @ p))) a
    | inr b =>
        (fun (b0 : B) (p : h (inr b0) = inl a') =>
         let Hb := Hb b0 in
         hfiber_unfunctor_sum_l_subproof A A' B B' h
           Ha b0 Hb a' p) b
    end) X.1 X.2) == idmap intros [[a|b] p]; simpl.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
(inl a;
(inl_un_inl (h (inl a)) (Ha a))^ @
ap inl
  (path_sum_inl B' (inl_un_inl (h (inl a)) (Ha a) @ p))) =
(inl a; p)
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h (inr b) = inl a'
(inl
   (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha b
      (Hb b) a' p).1;
(inl_un_inl
   (h
      (inl
         (hfiber_unfunctor_sum_l_subproof A A' B B' h
            Ha b (Hb b) a' p).1))
   (Ha
      (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha
         b (Hb b) a' p).1))^ @
ap inl
  (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha b
     (Hb b) a' p).2) = (inr b; p)
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
(inl a;
(inl_un_inl (h (inl a)) (Ha a))^ @
ap inl
  (path_sum_inl B' (inl_un_inl (h (inl a)) (Ha a) @ p))) =
(inl a; p) apply ap.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
(inl_un_inl (h (inl a)) (Ha a))^ @
ap inl
  (path_sum_inl B' (inl_un_inl (h (inl a)) (Ha a) @ p)) =
p
      apply moveR_Vp.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h (inl a) = inl a'
ap inl
  (path_sum_inl B' (inl_un_inl (h (inl a)) (Ha a) @ p)) =
inl_un_inl (h (inl a)) (Ha a) @ p
      exact (eisretr (@path_sum A' B' _ _)
                     (inl_un_inl (h (inl a)) (Ha a) @ p)).
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h (inr b) = inl a'
(inl
   (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha b
      (Hb b) a' p).1;
(inl_un_inl
   (h
      (inl
         (hfiber_unfunctor_sum_l_subproof A A' B B' h
            Ha b (Hb b) a' p).1))
   (Ha
      (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha
         b (Hb b) a' p).1))^ @
ap inl
  (hfiber_unfunctor_sum_l_subproof A A' B B' h Ha b
     (Hb b) a' p).2) = (inr b; p) apply Empty_rec.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h (inr b) = inl a'
Empty
      specialize (Hb b).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
b: B
Hb: is_inr (h (inr b))
a': A'
p: h (inr b) = inl a'
Empty
      abstract (rewrite p in Hb; elim Hb).
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
(fun X : hfiber h (inl a') =>
 (fun proj1 : A + B =>
  match
    proj1 as s
    return
      (h s = inl a' ->
       hfiber (unfunctor_sum_l h Ha) a')
  with
  | inl a =>
      (fun (a0 : A) (p : h (inl a0) = inl a') =>
       (a0;
       path_sum_inl B'
         (inl_un_inl (h (inl a0)) (Ha a0) @ p))) a
  | inr b =>
      (fun (b0 : B) (p : h (inr b0) = inl a') =>
       let Hb := Hb b0 in
       hfiber_unfunctor_sum_l_subproof A A' B B' h Ha
         b0 Hb a' p) b
  end) X.1 X.2)
o (fun X : hfiber (unfunctor_sum_l h Ha) a' =>
   (fun (a : A) (p : unfunctor_sum_l h Ha a = a') =>
    (inl a;
    (inl_un_inl (h (inl a)) (Ha a))^ @ ap inl p)) X.1
     X.2) == idmap intros [a p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
(a;
path_sum_inl B'
  (inl_un_inl (h (inl a)) (Ha a) @
   ((inl_un_inl (h (inl a)) (Ha a))^ @ ap inl p))) =
(a; p)
    apply ap.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
path_sum_inl B'
  (inl_un_inl (h (inl a)) (Ha a) @
   ((inl_un_inl (h (inl a)) (Ha a))^ @ ap inl p)) = p
    rewrite concat_p_Vp.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
path_sum_inl B' (ap inl p) = p
    pose (@isequiv_path_sum
            A' B' (inl (unfunctor_sum_l h Ha a)) (inl a')).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: unfunctor_sum_l h Ha a = a'
i:= isequiv_path_sum: IsEquiv
  (path_sum (inl (unfunctor_sum_l h Ha a))
     (inl a'))
path_sum_inl B' (ap inl p) = p
    exact (eissect (@path_sum A' B' (inl (unfunctor_sum_l h Ha a)) (inl a')) p).
Defined.

Definition hfiber_unfunctor_sum_r {A A' B B' : Type}
           (h : A + B -> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
           (b' : B')
: hfiber (unfunctor_sum_r h Hb) b' <~> hfiber h (inr b').
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber (unfunctor_sum_r h Hb) b' <~> hfiber h (inr b')
Proof.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber (unfunctor_sum_r h Hb) b' <~> hfiber h (inr b')
  simple refine (equiv_adjointify _ _ _ _).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber (unfunctor_sum_r h Hb) b' -> hfiber h (inr b')
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber h (inr b') -> hfiber (unfunctor_sum_r h Hb) b'
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
?f o ?g == idmap
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
?g o ?f == idmap
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber (unfunctor_sum_r h Hb) b' -> hfiber h (inr b') intros [b p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
hfiber h (inr b')
    exists (inr b).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
h (inr b) = inr b'
    refine (_ @ ap inr p).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
h (inr b) = inr (unfunctor_sum_r h Hb b)
    symmetry; apply inr_un_inr.
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
hfiber h (inr b') -> hfiber (unfunctor_sum_r h Hb) b' intros [[a|b] p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h (inl a) = inr b'
hfiber (unfunctor_sum_r h Hb) b'
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
hfiber (unfunctor_sum_r h Hb) b'
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h (inl a) = inr b'
hfiber (unfunctor_sum_r h Hb) b' specialize (Ha a).
A, A', B, B': Type
h: A + B -> A' + B'
a: A
Ha: is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
p: h (inl a) = inr b'
hfiber (unfunctor_sum_r h Hb) b'
      abstract (rewrite p in Ha; elim Ha).
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
hfiber (unfunctor_sum_r h Hb) b' exists b.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
unfunctor_sum_r h Hb b = b'
      apply path_sum_inr with A'.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
inr (unfunctor_sum_r h Hb b) = inr b'
      refine (_ @ p).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
inr (unfunctor_sum_r h Hb b) = h (inr b)
      apply inr_un_inr.
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
(fun X : hfiber (unfunctor_sum_r h Hb) b' =>
 (fun (b : B) (p : unfunctor_sum_r h Hb b = b') =>
  (inr b; (inr_un_inr (h (inr b)) (Hb b))^ @ ap inr p))
   X.1 X.2)
o (fun X : hfiber h (inr b') =>
   (fun proj1 : A + B =>
    match
      proj1 as s
      return
        (h s = inr b' ->
         hfiber (unfunctor_sum_r h Hb) b')
    with
    | inl a =>
        (fun (a0 : A) (p : h (inl a0) = inr b') =>
         let Ha := Ha a0 in
         hfiber_unfunctor_sum_r_subproof A A' B B' h
           a0 Ha Hb b' p) a
    | inr b =>
        (fun (b0 : B) (p : h (inr b0) = inr b') =>
         (b0;
         path_sum_inr A'
           (inr_un_inr (h (inr b0)) (Hb b0) @ p))) b
    end) X.1 X.2) == idmap intros [[a|b] p]; simpl.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h (inl a) = inr b'
(inr
   (hfiber_unfunctor_sum_r_subproof A A' B B' h a
      (Ha a) Hb b' p).1;
(inr_un_inr
   (h
      (inr
         (hfiber_unfunctor_sum_r_subproof A A' B B' h
            a (Ha a) Hb b' p).1))
   (Hb
      (hfiber_unfunctor_sum_r_subproof A A' B B' h a
         (Ha a) Hb b' p).1))^ @
ap inr
  (hfiber_unfunctor_sum_r_subproof A A' B B' h a
     (Ha a) Hb b' p).2) = (inl a; p)
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
(inr b;
(inr_un_inr (h (inr b)) (Hb b))^ @
ap inr
  (path_sum_inr A' (inr_un_inr (h (inr b)) (Hb b) @ p))) =
(inr b; p)
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h (inl a) = inr b'
(inr
   (hfiber_unfunctor_sum_r_subproof A A' B B' h a
      (Ha a) Hb b' p).1;
(inr_un_inr
   (h
      (inr
         (hfiber_unfunctor_sum_r_subproof A A' B B' h
            a (Ha a) Hb b' p).1))
   (Hb
      (hfiber_unfunctor_sum_r_subproof A A' B B' h a
         (Ha a) Hb b' p).1))^ @
ap inr
  (hfiber_unfunctor_sum_r_subproof A A' B B' h a
     (Ha a) Hb b' p).2) = (inl a; p) apply Empty_rec.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h (inl a) = inr b'
Empty
      specialize (Ha a).
A, A', B, B': Type
h: A + B -> A' + B'
a: A
Ha: is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
p: h (inl a) = inr b'
Empty
      abstract (rewrite p in Ha; elim Ha).
    +
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
(inr b;
(inr_un_inr (h (inr b)) (Hb b))^ @
ap inr
  (path_sum_inr A' (inr_un_inr (h (inr b)) (Hb b) @ p))) =
(inr b; p) apply ap.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
(inr_un_inr (h (inr b)) (Hb b))^ @
ap inr
  (path_sum_inr A' (inr_un_inr (h (inr b)) (Hb b) @ p)) =
p
      apply moveR_Vp.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h (inr b) = inr b'
ap inr
  (path_sum_inr A' (inr_un_inr (h (inr b)) (Hb b) @ p)) =
inr_un_inr (h (inr b)) (Hb b) @ p
      exact (eisretr (@path_sum A' B' _ _)
                     (inr_un_inr (h (inr b)) (Hb b) @ p)).
  -
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
(fun X : hfiber h (inr b') =>
 (fun proj1 : A + B =>
  match
    proj1 as s
    return
      (h s = inr b' ->
       hfiber (unfunctor_sum_r h Hb) b')
  with
  | inl a =>
      (fun (a0 : A) (p : h (inl a0) = inr b') =>
       let Ha := Ha a0 in
       hfiber_unfunctor_sum_r_subproof A A' B B' h a0
         Ha Hb b' p) a
  | inr b =>
      (fun (b0 : B) (p : h (inr b0) = inr b') =>
       (b0;
       path_sum_inr A'
         (inr_un_inr (h (inr b0)) (Hb b0) @ p))) b
  end) X.1 X.2)
o (fun X : hfiber (unfunctor_sum_r h Hb) b' =>
   (fun (b : B) (p : unfunctor_sum_r h Hb b = b') =>
    (inr b;
    (inr_un_inr (h (inr b)) (Hb b))^ @ ap inr p)) X.1
     X.2) == idmap intros [b p].
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
(b;
path_sum_inr A'
  (inr_un_inr (h (inr b)) (Hb b) @
   ((inr_un_inr (h (inr b)) (Hb b))^ @ ap inr p))) =
(b; p)
    apply ap.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
path_sum_inr A'
  (inr_un_inr (h (inr b)) (Hb b) @
   ((inr_un_inr (h (inr b)) (Hb b))^ @ ap inr p)) = p
    rewrite concat_p_Vp.
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
path_sum_inr A' (ap inr p) = p
    pose (@isequiv_path_sum
            A' B' (inr (unfunctor_sum_r h Hb b)) (inr b')).
A, A', B, B': Type
h: A + B -> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: unfunctor_sum_r h Hb b = b'
i:= isequiv_path_sum: IsEquiv
  (path_sum (inr (unfunctor_sum_r h Hb b))
     (inr b'))
path_sum_inr A' (ap inr p) = p
    exact (eissect (@path_sum A' B' (inr (unfunctor_sum_r h Hb b)) (inr b')) p).
Defined.

(** ** Functoriality on equivalences *)

Global Instance isequiv_functor_sum `{IsEquiv A A' f} `{IsEquiv B B' g}
: IsEquiv (functor_sum f g) | 1000.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
IsEquiv (functor_sum f g)
Proof.
A, A': Type
f: A -> A'
H: IsEquiv f
B, B': Type
g: B -> B'
H0: IsEquiv g
IsEquiv (functor_sum f g)
  apply (isequiv_adjointify
           (functor_sum f g)
           (functor_sum f^-1 g^-1));
  [ intros [?|?]; simpl; apply ap; apply eisretr
  | intros [?|?]; simpl; apply ap; apply eissect ].
Defined.

Definition equiv_functor_sum `{IsEquiv A A' f} `{IsEquiv B B' g}
: A + B <~> A' + B'
  := Build_Equiv _ _ (functor_sum f g) _.

Definition equiv_functor_sum' {A A' B B' : Type} (f : A <~> A') (g : B <~> B')
: A + B <~> A' + B'
  := equiv_functor_sum (f := f) (g := g).

Notation "f +E g" := (equiv_functor_sum' f g) : equiv_scope.

Definition equiv_functor_sum_l {A B B' : Type} (g : B <~> B')
: A + B <~> A + B'
  := 1 +E g.

Definition equiv_functor_sum_r {A A' B : Type} (f : A <~> A')
: A + B <~> A' + B
  := f +E 1.

(** ** Unfunctoriality on equivalences *)

Global Instance isequiv_unfunctor_sum_l {A A' B B' : Type}
           (h : A + B <~> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: IsEquiv (unfunctor_sum_l h Ha).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
IsEquiv (unfunctor_sum_l h Ha)
Proof.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
IsEquiv (unfunctor_sum_l h Ha)
  simple refine (isequiv_adjointify _ _ _ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
A' -> A
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_l h Ha o ?g == idmap
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
?g o unfunctor_sum_l h Ha == idmap
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
A' -> A refine (unfunctor_sum_l h^-1 _); intros a'.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
is_inl (h^-1 (inl a'))
    remember (h^-1 (inl a')) as x eqn:p.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
x: A + B
p: h^-1 (inl a') = x
is_inl x
    destruct x as [a|b].
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h^-1 (inl a') = inl a
is_inl (inl a)
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h^-1 (inl a') = inr b
is_inl (inr b)
    +
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
a: A
p: h^-1 (inl a') = inl a
is_inl (inl a) exact tt.
    +
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: h^-1 (inl a') = inr b
is_inl (inr b) apply moveL_equiv_M in p.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
b: B
p: inl a' = h (inr b)
is_inl (inr b)
      elim (p^ # (Hb b)).
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_l h Ha
o unfunctor_sum_l h^-1
    (fun a' : A' =>
     let x := h^-1 (inl a') in
     let p := 1 : h^-1 (inl a') = x in
     match
       x as s return (h^-1 (inl a') = s -> is_inl s)
     with
     | inl a =>
         (fun (a0 : A) (_ : h^-1 (inl a') = inl a0) =>
          tt) a
     | inr b =>
         (fun (b0 : B) (p0 : h^-1 (inl a') = inr b0)
          =>
          let p1 := moveL_equiv_M (inr b0) (inl a') p0
            in
          Overture.Empty_rec (is_inl (inr b0))
            (transport is_inr p1^ (Hb b0))) b
     end p) == idmap intros a'.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
unfunctor_sum_l h Ha
  (unfunctor_sum_l h^-1
     (fun a' : A' =>
      let x := h^-1 (inl a') in
      let p := 1 in
      match
        x as s return (h^-1 (inl a') = s -> is_inl s)
      with
      | inl a => fun _ : h^-1 (inl a') = inl a => tt
      | inr b =>
          fun p0 : h^-1 (inl a') = inr b =>
          let p1 := moveL_equiv_M (inr b) (inl a') p0
            in
          Overture.Empty_rec (is_inl (inr b))
            (transport is_inr p1^ (Hb b))
      end p) a') = a'
    refine (unfunctor_sum_l_compose _ _ _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
unfunctor_sum_l (fun x : A' + B' => h (h^-1 x))
  (fun a : A' =>
   is_inl_ind (fun x' : A + B => is_inl (h x')) Ha
     (h^-1 (inl a))
     (let x := h^-1 (inl a) in
      let p := 1 in
      match
        x as s return (h^-1 (inl a) = s -> is_inl s)
      with
      | inl a0 => fun _ : h^-1 (inl a) = inl a0 => tt
      | inr b =>
          fun p0 : h^-1 (inl a) = inr b =>
          let p1 := moveL_equiv_M (inr b) (inl a) p0
            in
          Overture.Empty_rec (is_inl (inr b))
            (transport is_inr p1^ (Hb b))
      end p)) a' = a'
    refine (path_sum_inl B' _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
inl
  (unfunctor_sum_l (fun x : A' + B' => h (h^-1 x))
     (fun a : A' =>
      is_inl_ind (fun x' : A + B => is_inl (h x')) Ha
        (h^-1 (inl a))
        (let x := h^-1 (inl a) in
         let p := 1 in
         match
           x as s
           return (h^-1 (inl a) = s -> is_inl s)
         with
         | inl a0 =>
             fun _ : h^-1 (inl a) = inl a0 => tt
         | inr b =>
             fun p0 : h^-1 (inl a) = inr b =>
             let p1 :=
               moveL_equiv_M (inr b) (inl a) p0 in
             Overture.Empty_rec (is_inl (inr b))
               (transport is_inr p1^ (Hb b))
         end p)) a') = inl a'
    refine (unfunctor_sum_l_beta _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a': A'
h (h^-1 (inl a')) = inl a'
    apply eisretr.
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_l h^-1
  (fun a' : A' =>
   let x := h^-1 (inl a') in
   let p := 1 : h^-1 (inl a') = x in
   match
     x as s return (h^-1 (inl a') = s -> is_inl s)
   with
   | inl a =>
       (fun (a0 : A) (_ : h^-1 (inl a') = inl a0) =>
        tt) a
   | inr b =>
       (fun (b0 : B) (p0 : h^-1 (inl a') = inr b0) =>
        let p1 := moveL_equiv_M (inr b0) (inl a') p0
          in
        Overture.Empty_rec (is_inl (inr b0))
          (transport is_inr p1^ (Hb b0))) b
   end p) o unfunctor_sum_l h Ha == idmap intros a.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
unfunctor_sum_l h^-1
  (fun a' : A' =>
   let x := h^-1 (inl a') in
   let p := 1 in
   match
     x as s return (h^-1 (inl a') = s -> is_inl s)
   with
   | inl a => fun _ : h^-1 (inl a') = inl a => tt
   | inr b =>
       fun p0 : h^-1 (inl a') = inr b =>
       let p1 := moveL_equiv_M (inr b) (inl a') p0 in
       Overture.Empty_rec (is_inl (inr b))
         (transport is_inr p1^ (Hb b))
   end p) (unfunctor_sum_l h Ha a) = a
    refine (unfunctor_sum_l_compose _ _ _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
unfunctor_sum_l (fun x : A + B => h^-1 (h x))
  (fun a : A =>
   is_inl_ind (fun x' : A' + B' => is_inl (h^-1 x'))
     (fun a' : A' =>
      let x := h^-1 (inl a') in
      let p := 1 in
      match
        x as s return (h^-1 (inl a') = s -> is_inl s)
      with
      | inl a0 => fun _ : h^-1 (inl a') = inl a0 => tt
      | inr b =>
          fun p0 : h^-1 (inl a') = inr b =>
          let p1 := moveL_equiv_M (inr b) (inl a') p0
            in
          Overture.Empty_rec (is_inl (inr b))
            (transport is_inr p1^ (Hb b))
      end p) (h (inl a)) (Ha a)) a = a
    refine (path_sum_inl B _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
inl
  (unfunctor_sum_l (fun x : A + B => h^-1 (h x))
     (fun a : A =>
      is_inl_ind
        (fun x' : A' + B' => is_inl (h^-1 x'))
        (fun a' : A' =>
         let x := h^-1 (inl a') in
         let p := 1 in
         match
           x as s
           return (h^-1 (inl a') = s -> is_inl s)
         with
         | inl a0 =>
             fun _ : h^-1 (inl a') = inl a0 => tt
         | inr b =>
             fun p0 : h^-1 (inl a') = inr b =>
             let p1 :=
               moveL_equiv_M (inr b) (inl a') p0 in
             Overture.Empty_rec (is_inl (inr b))
               (transport is_inr p1^ (Hb b))
         end p) (h (inl a)) (Ha a)) a) = inl a
    refine (unfunctor_sum_l_beta (h^-1 o h) _ a @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
a: A
h^-1 (h (inl a)) = inl a
    apply eissect.
Defined.

Definition equiv_unfunctor_sum_l {A A' B B' : Type}
           (h : A + B <~> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: A <~> A'
  := Build_Equiv _ _ (unfunctor_sum_l h Ha)
                (isequiv_unfunctor_sum_l h Ha Hb).

Global Instance isequiv_unfunctor_sum_r {A A' B B' : Type}
           (h : A + B <~> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: IsEquiv (unfunctor_sum_r h Hb).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
IsEquiv (unfunctor_sum_r h Hb)
Proof.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
IsEquiv (unfunctor_sum_r h Hb)
  simple refine (isequiv_adjointify _ _ _ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
B' -> B
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_r h Hb o ?g == idmap
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
?g o unfunctor_sum_r h Hb == idmap
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
B' -> B refine (unfunctor_sum_r h^-1 _); intros b'.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
is_inr (h^-1 (inr b'))
    remember (h^-1 (inr b')) as x eqn:p.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
x: A + B
p: h^-1 (inr b') = x
is_inr x
    destruct x as [a|b].
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h^-1 (inr b') = inl a
is_inr (inl a)
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h^-1 (inr b') = inr b
is_inr (inr b)
    +
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: h^-1 (inr b') = inl a
is_inr (inl a) apply moveL_equiv_M in p.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
a: A
p: inr b' = h (inl a)
is_inr (inl a)
      elim (p^ # (Ha a)).
    +
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
b: B
p: h^-1 (inr b') = inr b
is_inr (inr b) exact tt.
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_r h Hb
o unfunctor_sum_r h^-1
    (fun b' : B' =>
     let x := h^-1 (inr b') in
     let p := 1 : h^-1 (inr b') = x in
     match
       x as s return (h^-1 (inr b') = s -> is_inr s)
     with
     | inl a =>
         (fun (a0 : A) (p0 : h^-1 (inr b') = inl a0)
          =>
          let p1 := moveL_equiv_M (inl a0) (inr b') p0
            in
          Overture.Empty_rec (is_inr (inl a0))
            (transport is_inl p1^ (Ha a0))) a
     | inr b =>
         (fun (b0 : B) (_ : h^-1 (inr b') = inr b0) =>
          tt) b
     end p) == idmap intros b'.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
unfunctor_sum_r h Hb
  (unfunctor_sum_r h^-1
     (fun b' : B' =>
      let x := h^-1 (inr b') in
      let p := 1 in
      match
        x as s return (h^-1 (inr b') = s -> is_inr s)
      with
      | inl a =>
          fun p0 : h^-1 (inr b') = inl a =>
          let p1 := moveL_equiv_M (inl a) (inr b') p0
            in
          Overture.Empty_rec (is_inr (inl a))
            (transport is_inl p1^ (Ha a))
      | inr b => fun _ : h^-1 (inr b') = inr b => tt
      end p) b') = b'
    refine (unfunctor_sum_r_compose _ _ _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
unfunctor_sum_r (fun x : A' + B' => h (h^-1 x))
  (fun b : B' =>
   is_inr_ind (fun x' : A + B => is_inr (h x')) Hb
     (h^-1 (inr b))
     (let x := h^-1 (inr b) in
      let p := 1 in
      match
        x as s return (h^-1 (inr b) = s -> is_inr s)
      with
      | inl a =>
          fun p0 : h^-1 (inr b) = inl a =>
          let p1 := moveL_equiv_M (inl a) (inr b) p0
            in
          Overture.Empty_rec (is_inr (inl a))
            (transport is_inl p1^ (Ha a))
      | inr b0 => fun _ : h^-1 (inr b) = inr b0 => tt
      end p)) b' = b'
    refine (path_sum_inr A' _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
inr
  (unfunctor_sum_r (fun x : A' + B' => h (h^-1 x))
     (fun b : B' =>
      is_inr_ind (fun x' : A + B => is_inr (h x')) Hb
        (h^-1 (inr b))
        (let x := h^-1 (inr b) in
         let p := 1 in
         match
           x as s
           return (h^-1 (inr b) = s -> is_inr s)
         with
         | inl a =>
             fun p0 : h^-1 (inr b) = inl a =>
             let p1 :=
               moveL_equiv_M (inl a) (inr b) p0 in
             Overture.Empty_rec (is_inr (inl a))
               (transport is_inl p1^ (Ha a))
         | inr b0 =>
             fun _ : h^-1 (inr b) = inr b0 => tt
         end p)) b') = inr b'
    refine (unfunctor_sum_r_beta _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b': B'
h (h^-1 (inr b')) = inr b'
    apply eisretr.
  -
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
unfunctor_sum_r h^-1
  (fun b' : B' =>
   let x := h^-1 (inr b') in
   let p := 1 : h^-1 (inr b') = x in
   match
     x as s return (h^-1 (inr b') = s -> is_inr s)
   with
   | inl a =>
       (fun (a0 : A) (p0 : h^-1 (inr b') = inl a0) =>
        let p1 := moveL_equiv_M (inl a0) (inr b') p0
          in
        Overture.Empty_rec (is_inr (inl a0))
          (transport is_inl p1^ (Ha a0))) a
   | inr b =>
       (fun (b0 : B) (_ : h^-1 (inr b') = inr b0) =>
        tt) b
   end p) o unfunctor_sum_r h Hb == idmap intros b.
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
unfunctor_sum_r h^-1
  (fun b' : B' =>
   let x := h^-1 (inr b') in
   let p := 1 in
   match
     x as s return (h^-1 (inr b') = s -> is_inr s)
   with
   | inl a =>
       fun p0 : h^-1 (inr b') = inl a =>
       let p1 := moveL_equiv_M (inl a) (inr b') p0 in
       Overture.Empty_rec (is_inr (inl a))
         (transport is_inl p1^ (Ha a))
   | inr b => fun _ : h^-1 (inr b') = inr b => tt
   end p) (unfunctor_sum_r h Hb b) = b
    refine (unfunctor_sum_r_compose _ _ _ _ _ @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
unfunctor_sum_r (fun x : A + B => h^-1 (h x))
  (fun b : B =>
   is_inr_ind (fun x' : A' + B' => is_inr (h^-1 x'))
     (fun b' : B' =>
      let x := h^-1 (inr b') in
      let p := 1 in
      match
        x as s return (h^-1 (inr b') = s -> is_inr s)
      with
      | inl a =>
          fun p0 : h^-1 (inr b') = inl a =>
          let p1 := moveL_equiv_M (inl a) (inr b') p0
            in
          Overture.Empty_rec (is_inr (inl a))
            (transport is_inl p1^ (Ha a))
      | inr b0 => fun _ : h^-1 (inr b') = inr b0 => tt
      end p) (h (inr b)) (Hb b)) b = b
    refine (path_sum_inr A _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
inr
  (unfunctor_sum_r (fun x : A + B => h^-1 (h x))
     (fun b : B =>
      is_inr_ind
        (fun x' : A' + B' => is_inr (h^-1 x'))
        (fun b' : B' =>
         let x := h^-1 (inr b') in
         let p := 1 in
         match
           x as s
           return (h^-1 (inr b') = s -> is_inr s)
         with
         | inl a =>
             fun p0 : h^-1 (inr b') = inl a =>
             let p1 :=
               moveL_equiv_M (inl a) (inr b') p0 in
             Overture.Empty_rec (is_inr (inl a))
               (transport is_inl p1^ (Ha a))
         | inr b0 =>
             fun _ : h^-1 (inr b') = inr b0 => tt
         end p) (h (inr b)) (Hb b)) b) = inr b
    refine (unfunctor_sum_r_beta (h^-1 o h) _ b @ _).
A, A', B, B': Type
h: A + B <~> A' + B'
Ha: forall a : A, is_inl (h (inl a))
Hb: forall b : B, is_inr (h (inr b))
b: B
h^-1 (h (inr b)) = inr b
    apply eissect.
Defined.

Definition equiv_unfunctor_sum_r {A A' B B' : Type}
           (h : A + B <~> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: B <~> B'
  := Build_Equiv _ _ (unfunctor_sum_r h Hb)
                (isequiv_unfunctor_sum_r h Ha Hb).

Definition equiv_unfunctor_sum {A A' B B' : Type}
           (h : A + B <~> A' + B')
           (Ha : forall a:A, is_inl (h (inl a)))
           (Hb : forall b:B, is_inr (h (inr b)))
: (A <~> A') * (B <~> B')
  := (equiv_unfunctor_sum_l h Ha Hb , equiv_unfunctor_sum_r h Ha Hb).

(** ** Symmetry *)

(* This is a special property of [sum], of course, not an instance of a general family of facts about types. *)

Definition equiv_sum_symm (A B : Type) : A + B <~> B + A.
A, B: Type
A + B <~> B + A
Proof.
A, B: Type
A + B <~> B + A
  apply (equiv_adjointify
           (fun ab => match ab with inl a => inr a | inr b => inl b end)
           (fun ab => match ab with inl a => inr a | inr b => inl b end));
  intros [?|?]; exact idpath.
Defined.

(** ** Associativity *)

Definition equiv_sum_assoc (A B C : Type) : (A + B) + C <~> A + (B + C).
A, B, C: Type
A + B + C <~> A + (B + C)
Proof.
A, B, C: Type
A + B + C <~> A + (B + C)
  simple refine (equiv_adjointify _ _ _ _).
A, B, C: Type
A + B + C -> A + (B + C)
A, B, C: Type
A + (B + C) -> A + B + C
A, B, C: Type
?f o ?g == idmap
A, B, C: Type
?g o ?f == idmap
  -
A, B, C: Type
A + B + C -> A + (B + C) intros [[a|b]|c];
    [ exact (inl a) | exact (inr (inl b)) | exact (inr (inr c)) ].
  -
A, B, C: Type
A + (B + C) -> A + B + C intros [a|[b|c]];
    [ exact (inl (inl a)) | exact (inl (inr b)) | exact (inr c) ].
  -
A, B, C: Type
(fun X : A + B + C =>
 match X with
 | inl s =>
     (fun s0 : A + B =>
      match s0 with
      | inl a => (fun a0 : A => inl a0) a
      | inr b => (fun b0 : B => inr (inl b0)) b
      end) s
 | inr c => (fun c0 : C => inr (inr c0)) c
 end)
o (fun X : A + (B + C) =>
   match X with
   | inl a => (fun a0 : A => inl (inl a0)) a
   | inr s =>
       (fun s0 : B + C =>
        match s0 with
        | inl b => (fun b0 : B => inl (inr b0)) b
        | inr c => (fun c0 : C => inr c0) c
        end) s
   end) == idmap intros [a|[b|c]]; reflexivity.
  -
A, B, C: Type
(fun X : A + (B + C) =>
 match X with
 | inl a => (fun a0 : A => inl (inl a0)) a
 | inr s =>
     (fun s0 : B + C =>
      match s0 with
      | inl b => (fun b0 : B => inl (inr b0)) b
      | inr c => (fun c0 : C => inr c0) c
      end) s
 end)
o (fun X : A + B + C =>
   match X with
   | inl s =>
       (fun s0 : A + B =>
        match s0 with
        | inl a => (fun a0 : A => inl a0) a
        | inr b => (fun b0 : B => inr (inl b0)) b
        end) s
   | inr c => (fun c0 : C => inr (inr c0)) c
   end) == idmap intros [[a|b]|c]; reflexivity.
Defined.

(** ** Identity *)

Definition sum_empty_l (A : Type) : Empty + A <~> A.
A: Type
Empty + A <~> A
Proof.
A: Type
Empty + A <~> A
  refine (equiv_adjointify
       (fun z => match z:Empty+A with
                   | inl e => match e with end
                   | inr a => a
                 end)
       inr (fun a => 1) _).
A: Type
(fun x : Empty + A =>
 inr
   match x with
   | inl e => match e return A with
              end
   | inr a => a
   end) == idmap
  intros [e|z]; [ elim e | reflexivity ].
Defined.

Definition sum_empty_r (A : Type) : A + Empty <~> A.
A: Type
A + Empty <~> A
Proof.
A: Type
A + Empty <~> A
  refine (equiv_adjointify
       (fun z => match z : A + Empty with
                   | inr e => match e with end
                   | inl a => a
                 end)
       inl (fun a => 1) _).
A: Type
(fun x : A + Empty =>
 inl
   match x with
   | inl a => a
   | inr e => match e return A with
              end
   end) == idmap
  intros [z|e]; [ reflexivity | elim e ].
Defined.

(** ** Distributivity *)

Definition sum_distrib_l A B C
: A * (B + C) <~> (A * B) + (A * C).
A, B, C: Type
A * (B + C) <~> A * B + A * C
Proof.
A, B, C: Type
A * (B + C) <~> A * B + A * C
  refine (Build_Equiv (A * (B + C)) ((A * B) + (A * C))
            (fun abc => let (a,bc) := abc in
                        match bc with
                          | inl b => inl (a,b)
                          | inr c => inr (a,c)
                        end) _).
A, B, C: Type
IsEquiv
  (fun abc : A * (B + C) =>
   let a := fst abc in
   let bc := snd abc in
   match bc with
   | inl b => inl (a, b)
   | inr c => inr (a, c)
   end)
  simple refine (Build_IsEquiv (A * (B + C)) ((A * B) + (A * C)) _
            (fun ax => match ax with
                         | inl (a,b) => (a,inl b)
                         | inr (a,c) => (a,inr c)
                       end) _ _ _).
A, B, C: Type
(fun abc : A * (B + C) =>
 let a := fst abc in
 let bc := snd abc in
 match bc with
 | inl b => inl (a, b)
 | inr c => inr (a, c)
 end)
o (fun ax : A * B + A * C =>
   match ax with
   | inl p =>
       let p0 := p in
       let a := fst p0 in
       let b := snd p0 in (a, inl b)
   | inr p =>
       let p0 := p in
       let a := fst p0 in
       let c := snd p0 in (a, inr c)
   end) == idmap
A, B, C: Type
(fun ax : A * B + A * C =>
 match ax with
 | inl p =>
     let p0 := p in
     let a := fst p0 in let b := snd p0 in (a, inl b)
 | inr p =>
     let p0 := p in
     let a := fst p0 in let c := snd p0 in (a, inr c)
 end)
o (fun abc : A * (B + C) =>
   let a := fst abc in
   let bc := snd abc in
   match bc with
   | inl b => inl (a, b)
   | inr c => inr (a, c)
   end) == idmap
A, B, C: Type
forall x : A * (B + C),
?eisretr
  ((fun abc : A * (B + C) =>
    let a := fst abc in
    let bc := snd abc in
    match bc with
    | inl b => inl (a, b)
    | inr c => inr (a, c)
    end) x) =
ap
  (fun abc : A * (B + C) =>
   let a := fst abc in
   let bc := snd abc in
   match bc with
   | inl b => inl (a, b)
   | inr c => inr (a, c)
   end) (?eissect x)
  -
A, B, C: Type
(fun abc : A * (B + C) =>
 let a := fst abc in
 let bc := snd abc in
 match bc with
 | inl b => inl (a, b)
 | inr c => inr (a, c)
 end)
o (fun ax : A * B + A * C =>
   match ax with
   | inl p =>
       let p0 := p in
       let a := fst p0 in
       let b := snd p0 in (a, inl b)
   | inr p =>
       let p0 := p in
       let a := fst p0 in
       let c := snd p0 in (a, inr c)
   end) == idmap intros [[a b]|[a c]]; reflexivity.
  -
A, B, C: Type
(fun ax : A * B + A * C =>
 match ax with
 | inl p =>
     let p0 := p in
     let a := fst p0 in let b := snd p0 in (a, inl b)
 | inr p =>
     let p0 := p in
     let a := fst p0 in let c := snd p0 in (a, inr c)
 end)
o (fun abc : A * (B + C) =>
   let a := fst abc in
   let bc := snd abc in
   match bc with
   | inl b => inl (a, b)
   | inr c => inr (a, c)
   end) == idmap intros [a [b|c]]; reflexivity.
  -
A, B, C: Type
forall x : A * (B + C),
((fun x0 : A * B + A * C =>
  match
    x0 as s
    return
      ((let a :=
          fst
            match s with
            | inl p =>
                let p0 := p in
                let a := fst p0 in
                let b := snd p0 in (a, inl b)
            | inr p =>
                let p0 := p in
                let a := fst p0 in
                let c := snd p0 in (a, inr c)
            end in
        let bc :=
          snd
            match s with
            | inl p =>
                let p0 := p in
                let a0 := fst p0 in
                let b := snd p0 in (a0, inl b)
            | inr p =>
                let p0 := p in
                let a0 := fst p0 in
                let c := snd p0 in (a0, inr c)
            end in
        match bc with
        | inl b => inl (a, b)
        | inr c => inr (a, c)
        end) = s)
  with
  | inl p =>
      (fun p0 : A * B =>
       (fun (a : A) (b : B) => 1) (fst p0) (snd p0)) p
  | inr p =>
      (fun p0 : A * C =>
       (fun (a : A) (c : C) => 1) (fst p0) (snd p0)) p
  end)
 :
 (fun abc : A * (B + C) =>
  let a := fst abc in
  let bc := snd abc in
  match bc with
  | inl b => inl (a, b)
  | inr c => inr (a, c)
  end)
 o (fun ax : A * B + A * C =>
    match ax with
    | inl p =>
        let p0 := p in
        let a := fst p0 in
        let b := snd p0 in (a, inl b)
    | inr p =>
        let p0 := p in
        let a := fst p0 in
        let c := snd p0 in (a, inr c)
    end) == idmap)
  ((fun abc : A * (B + C) =>
    let a := fst abc in
    let bc := snd abc in
    match bc with
    | inl b => inl (a, b)
    | inr c => inr (a, c)
    end) x) =
ap
  (fun abc : A * (B + C) =>
   let a := fst abc in
   let bc := snd abc in
   match bc with
   | inl b => inl (a, b)
   | inr c => inr (a, c)
   end)
  (((fun x0 : A * (B + C) =>
     (fun (a : A) (snd : B + C) =>
      match
        snd as s
        return
          (match
             (let a0 := a in
              let bc := s in
              match ... with
              | ... ...
              | ... ...
              end)
           with
           | inl p =>
               let p0 := p in
               let a0 := fst p0 in
               let b := Overture.snd p0 in (a0, inl b)
           | inr p =>
               let p0 := p in
               let a0 := fst p0 in
               let c := Overture.snd p0 in (a0, inr c)
           end = (a, s))
      with
      | inl b => (fun b0 : B => 1) b
      | inr c => (fun c0 : C => 1) c
      end) (fst x0) (snd x0))
    :
    (fun ax : A * B + A * C =>
     match ax with
     | inl p =>
         let p0 := p in
         let a := fst p0 in
         let b := snd p0 in (a, inl b)
     | inr p =>
         let p0 := p in
         let a := fst p0 in
         let c := snd p0 in (a, inr c)
     end)
    o (fun abc : A * (B + C) =>
       let a := fst abc in
       let bc := snd abc in
       match bc with
       | inl b => inl (a, b)
       | inr c => inr (a, c)
       end) == idmap) x) intros [a [b|c]]; reflexivity.
Defined.

Definition sum_distrib_r A B C
: (B + C) * A <~> (B * A) + (C * A).
A, B, C: Type
(B + C) * A <~> B * A + C * A
Proof.
A, B, C: Type
(B + C) * A <~> B * A + C * A
  refine (Build_Equiv ((B + C) * A) ((B * A) + (C * A))
            (fun abc => let (bc,a) := abc in
                        match bc with
                          | inl b => inl (b,a)
                          | inr c => inr (c,a)
                        end) _).
A, B, C: Type
IsEquiv
  (fun abc : (B + C) * A =>
   let bc := fst abc in
   let a := snd abc in
   match bc with
   | inl b => inl (b, a)
   | inr c => inr (c, a)
   end)
  simple refine (Build_IsEquiv ((B + C) * A) ((B * A) + (C * A)) _
            (fun ax => match ax with
                         | inl (b,a) => (inl b,a)
                         | inr (c,a) => (inr c,a)
                       end) _ _ _).
A, B, C: Type
(fun abc : (B + C) * A =>
 let bc := fst abc in
 let a := snd abc in
 match bc with
 | inl b => inl (b, a)
 | inr c => inr (c, a)
 end)
o (fun ax : B * A + C * A =>
   match ax with
   | inl p =>
       let p0 := p in
       let b := fst p0 in
       let a := snd p0 in (inl b, a)
   | inr p =>
       let p0 := p in
       let c := fst p0 in
       let a := snd p0 in (inr c, a)
   end) == idmap
A, B, C: Type
(fun ax : B * A + C * A =>
 match ax with
 | inl p =>
     let p0 := p in
     let b := fst p0 in let a := snd p0 in (inl b, a)
 | inr p =>
     let p0 := p in
     let c := fst p0 in let a := snd p0 in (inr c, a)
 end)
o (fun abc : (B + C) * A =>
   let bc := fst abc in
   let a := snd abc in
   match bc with
   | inl b => inl (b, a)
   | inr c => inr (c, a)
   end) == idmap
A, B, C: Type
forall x : (B + C) * A,
?eisretr
  ((fun abc : (B + C) * A =>
    let bc := fst abc in
    let a := snd abc in
    match bc with
    | inl b => inl (b, a)
    | inr c => inr (c, a)
    end) x) =
ap
  (fun abc : (B + C) * A =>
   let bc := fst abc in
   let a := snd abc in
   match bc with
   | inl b => inl (b, a)
   | inr c => inr (c, a)
   end) (?eissect x)
  -
A, B, C: Type
(fun abc : (B + C) * A =>
 let bc := fst abc in
 let a := snd abc in
 match bc with
 | inl b => inl (b, a)
 | inr c => inr (c, a)
 end)
o (fun ax : B * A + C * A =>
   match ax with
   | inl p =>
       let p0 := p in
       let b := fst p0 in
       let a := snd p0 in (inl b, a)
   | inr p =>
       let p0 := p in
       let c := fst p0 in
       let a := snd p0 in (inr c, a)
   end) == idmap intros [[b a]|[c a]]; reflexivity.
  -
A, B, C: Type
(fun ax : B * A + C * A =>
 match ax with
 | inl p =>
     let p0 := p in
     let b := fst p0 in let a := snd p0 in (inl b, a)
 | inr p =>
     let p0 := p in
     let c := fst p0 in let a := snd p0 in (inr c, a)
 end)
o (fun abc : (B + C) * A =>
   let bc := fst abc in
   let a := snd abc in
   match bc with
   | inl b => inl (b, a)
   | inr c => inr (c, a)
   end) == idmap intros [[b|c] a]; reflexivity.
  -
A, B, C: Type
forall x : (B + C) * A,
((fun x0 : B * A + C * A =>
  match
    x0 as s
    return
      ((let bc :=
          fst
            match s with
            | inl p =>
                let p0 := p in
                let b := fst p0 in
                let a := snd p0 in (inl b, a)
            | inr p =>
                let p0 := p in
                let c := fst p0 in
                let a := snd p0 in (inr c, a)
            end in
        let a :=
          snd
            match s with
            | inl p =>
                let p0 := p in
                let b := fst p0 in
                let a := snd p0 in (inl b, a)
            | inr p =>
                let p0 := p in
                let c := fst p0 in
                let a := snd p0 in (inr c, a)
            end in
        match bc with
        | inl b => inl (b, a)
        | inr c => inr (c, a)
        end) = s)
  with
  | inl p =>
      (fun p0 : B * A =>
       (fun (b : B) (a : A) => 1) (fst p0) (snd p0)) p
  | inr p =>
      (fun p0 : C * A =>
       (fun (c : C) (a : A) => 1) (fst p0) (snd p0)) p
  end)
 :
 (fun abc : (B + C) * A =>
  let bc := fst abc in
  let a := snd abc in
  match bc with
  | inl b => inl (b, a)
  | inr c => inr (c, a)
  end)
 o (fun ax : B * A + C * A =>
    match ax with
    | inl p =>
        let p0 := p in
        let b := fst p0 in
        let a := snd p0 in (inl b, a)
    | inr p =>
        let p0 := p in
        let c := fst p0 in
        let a := snd p0 in (inr c, a)
    end) == idmap)
  ((fun abc : (B + C) * A =>
    let bc := fst abc in
    let a := snd abc in
    match bc with
    | inl b => inl (b, a)
    | inr c => inr (c, a)
    end) x) =
ap
  (fun abc : (B + C) * A =>
   let bc := fst abc in
   let a := snd abc in
   match bc with
   | inl b => inl (b, a)
   | inr c => inr (c, a)
   end)
  (((fun x0 : (B + C) * A =>
     (fun fst : B + C =>
      match
        fst as s
        return
          (forall snd : A,
           match
             (let bc := s in
              let a := snd in ...
                              ...
                              ...
                              end)
           with
           | inl p =>
               let p0 := p in
               let b := Overture.fst p0 in
               let a := Overture.snd p0 in (inl b, a)
           | inr p =>
               let p0 := p in
               let c := Overture.fst p0 in
               let a := Overture.snd p0 in (inr c, a)
           end = (s, snd))
      with
      | inl b => (fun (b0 : B) (a : A) => 1) b
      | inr c => (fun (c0 : C) (a : A) => 1) c
      end) (fst x0) (snd x0))
    :
    (fun ax : B * A + C * A =>
     match ax with
     | inl p =>
         let p0 := p in
         let b := fst p0 in
         let a := snd p0 in (inl b, a)
     | inr p =>
         let p0 := p in
         let c := fst p0 in
         let a := snd p0 in (inr c, a)
     end)
    o (fun abc : (B + C) * A =>
       let bc := fst abc in
       let a := snd abc in
       match bc with
       | inl b => inl (b, a)
       | inr c => inr (c, a)
       end) == idmap) x) intros [[b|c] a]; reflexivity.
Defined.

(** ** Extensivity *)

(** We can phrase extensivity in two ways, using either dependent types or functions. *)

(** The first is a statement about types dependent on a sum type. *)
Definition equiv_sigma_sum A B (C : A + B -> Type)
: { x : A+B & C x } <~>
  { a : A & C (inl a) } + { b : B & C (inr b) }.
A, B: Type
C: A + B -> Type
{x : A + B & C x} <~>
{a : A & C (inl a)} + {b : B & C (inr b)}
Proof.
A, B: Type
C: A + B -> Type
{x : A + B & C x} <~>
{a : A & C (inl a)} + {b : B & C (inr b)}
  refine (Build_Equiv { x : A+B & C x }
                     ({ a : A & C (inl a) } + { b : B & C (inr b) })
           (fun xc => let (x,c) := xc in
                      match x return
                            C x -> ({ a : A & C (inl a) } + { b : B & C (inr b) })
                      with
                        | inl a => fun c => inl (a;c)
                        | inr b => fun c => inr (b;c)
                      end c) _).
A, B: Type
C: A + B -> Type
IsEquiv
  (fun xc : {x : A + B & C x} =>
   let x := xc.1 in
   let c := xc.2 in
   match
     x as x0
     return
       (C x0 ->
        {a : A & C (inl a)} + {b : B & C (inr b)})
   with
   | inl a => fun c0 : C (inl a) => inl (a; c0)
   | inr b => fun c0 : C (inr b) => inr (b; c0)
   end c)
  simple refine (Build_IsEquiv { x : A+B & C x }
                       ({ a : A & C (inl a) } + { b : B & C (inr b) }) _
           (fun abc => match abc with
                         | inl (a;c) => (inl a ; c)
                         | inr (b;c) => (inr b ; c)
                       end) _ _ _).
A, B: Type
C: A + B -> Type
(fun xc : {x : A + B & C x} =>
 let x := xc.1 in
 let c := xc.2 in
 match
   x as x0
   return
     (C x0 ->
      {a : A & C (inl a)} + {b : B & C (inr b)})
 with
 | inl a => fun c0 : C (inl a) => inl (a; c0)
 | inr b => fun c0 : C (inr b) => inr (b; c0)
 end c)
o (fun abc : {a : A & C (inl a)} + {b : B & C (inr b)}
   =>
   match abc with
   | inl s =>
       let s0 := s in
       let a := s0.1 in let c := s0.2 in (inl a; c)
   | inr s =>
       let s0 := s in
       let b := s0.1 in let c := s0.2 in (inr b; c)
   end) == idmap
A, B: Type
C: A + B -> Type
(fun abc : {a : A & C (inl a)} + {b : B & C (inr b)}
 =>
 match abc with
 | inl s =>
     let s0 := s in
     let a := s0.1 in let c := s0.2 in (inl a; c)
 | inr s =>
     let s0 := s in
     let b := s0.1 in let c := s0.2 in (inr b; c)
 end)
o (fun xc : {x : A + B & C x} =>
   let x := xc.1 in
   let c := xc.2 in
   match
     x as x0
     return
       (C x0 ->
        {a : A & C (inl a)} + {b : B & C (inr b)})
   with
   | inl a => fun c0 : C (inl a) => inl (a; c0)
   | inr b => fun c0 : C (inr b) => inr (b; c0)
   end c) == idmap
A, B: Type
C: A + B -> Type
forall x : {x : A + B & C x},
?eisretr
  ((fun xc : {x0 : A + B & C x0} =>
    let x0 := xc.1 in
    let c := xc.2 in
    match
      x0 as x1
      return
        (C x1 ->
         {a : A & C (inl a)} + {b : B & C (inr b)})
    with
    | inl a => fun c0 : C (inl a) => inl (a; c0)
    | inr b => fun c0 : C (inr b) => inr (b; c0)
    end c) x) =
ap
  (fun xc : {x0 : A + B & C x0} =>
   let x0 := xc.1 in
   let c := xc.2 in
   match
     x0 as x1
     return
       (C x1 ->
        {a : A & C (inl a)} + {b : B & C (inr b)})
   with
   | inl a => fun c0 : C (inl a) => inl (a; c0)
   | inr b => fun c0 : C (inr b) => inr (b; c0)
   end c) (?eissect x)
  -
A, B: Type
C: A + B -> Type
(fun xc : {x : A + B & C x} =>
 let x := xc.1 in
 let c := xc.2 in
 match
   x as x0
   return
     (C x0 ->
      {a : A & C (inl a)} + {b : B & C (inr b)})
 with
 | inl a => fun c0 : C (inl a) => inl (a; c0)
 | inr b => fun c0 : C (inr b) => inr (b; c0)
 end c)
o (fun abc : {a : A & C (inl a)} + {b : B & C (inr b)}
   =>
   match abc with
   | inl s =>
       let s0 := s in
       let a := s0.1 in let c := s0.2 in (inl a; c)
   | inr s =>
       let s0 := s in
       let b := s0.1 in let c := s0.2 in (inr b; c)
   end) == idmap intros [[a c]|[b c]]; reflexivity.
  -
A, B: Type
C: A + B -> Type
(fun abc : {a : A & C (inl a)} + {b : B & C (inr b)}
 =>
 match abc with
 | inl s =>
     let s0 := s in
     let a := s0.1 in let c := s0.2 in (inl a; c)
 | inr s =>
     let s0 := s in
     let b := s0.1 in let c := s0.2 in (inr b; c)
 end)
o (fun xc : {x : A + B & C x} =>
   let x := xc.1 in
   let c := xc.2 in
   match
     x as x0
     return
       (C x0 ->
        {a : A & C (inl a)} + {b : B & C (inr b)})
   with
   | inl a => fun c0 : C (inl a) => inl (a; c0)
   | inr b => fun c0 : C (inr b) => inr (b; c0)
   end c) == idmap intros [[a|b] c]; reflexivity.
  -
A, B: Type
C: A + B -> Type
forall x : {x : A + B & C x},
((fun x0 : {a : A & C (inl a)} + {b : B & C (inr b)}
  =>
  match
    x0 as s
    return
      ((let x1 :=
          match s with
          | inl s0 =>
              let s1 := s0 in
              let a := s1.1 in
              let c := s1.2 in (inl a; c)
          | inr s0 =>
              let s1 := s0 in
              let b := s1.1 in
              let c := s1.2 in (inr b; c)
          end.1 in
        let c :=
          match s with
          | inl s0 =>
              let s1 := s0 in
              let a := s1.1 in
              let c := s1.2 in (inl a; c)
          | inr s0 =>
              let s1 := s0 in
              let b := s1.1 in
              let c := s1.2 in (inr b; c)
          end.2 in
        match
          x1 as x2
          return
            (C x2 ->
             {a : A & C (...)} + {b : B & C (...)})
        with
        | inl a => fun c0 : C (inl a) => inl (a; c0)
        | inr b => fun c0 : C (inr b) => inr (b; c0)
        end c) = s)
  with
  | inl s =>
      (fun s0 : {a : A & C (inl a)} =>
       (fun (a : A) (c : C (inl a)) => 1) s0.1 s0.2) s
  | inr s =>
      (fun s0 : {b : B & C (inr b)} =>
       (fun (b : B) (c : C (inr b)) => 1) s0.1 s0.2) s
  end)
 :
 (fun xc : {x0 : A + B & C x0} =>
  let x0 := xc.1 in
  let c := xc.2 in
  match
    x0 as x1
    return
      (C x1 ->
       {a : A & C (inl a)} + {b : B & C (inr b)})
  with
  | inl a => fun c0 : C (inl a) => inl (a; c0)
  | inr b => fun c0 : C (inr b) => inr (b; c0)
  end c)
 o (fun
      abc : {a : A & C (inl a)} + {b : B & C (inr b)}
    =>
    match abc with
    | inl s =>
        let s0 := s in
        let a := s0.1 in let c := s0.2 in (inl a; c)
    | inr s =>
        let s0 := s in
        let b := s0.1 in let c := s0.2 in (inr b; c)
    end) == idmap)
  ((fun xc : {x0 : A + B & C x0} =>
    let x0 := xc.1 in
    let c := xc.2 in
    match
      x0 as x1
      return
        (C x1 ->
         {a : A & C (inl a)} + {b : B & C (inr b)})
    with
    | inl a => fun c0 : C (inl a) => inl (a; c0)
    | inr b => fun c0 : C (inr b) => inr (b; c0)
    end c) x) =
ap
  (fun xc : {x0 : A + B & C x0} =>
   let x0 := xc.1 in
   let c := xc.2 in
   match
     x0 as x1
     return
       (C x1 ->
        {a : A & C (inl a)} + {b : B & C (inr b)})
   with
   | inl a => fun c0 : C (inl a) => inl (a; c0)
   | inr b => fun c0 : C (inr b) => inr (b; c0)
   end c)
  (((fun x0 : {x0 : A + B & C x0} =>
     (fun proj1 : A + B =>
      match
        proj1 as s
        return
          (forall proj2 : C s,
           match
             (let x1 := s in let c := proj2 in ... c)
           with
           | inl s0 =>
               let s1 := s0 in
               let a := s1.1 in
               let c := s1.2 in (inl a; c)
           | inr s0 =>
               let s1 := s0 in
               let b := s1.1 in
               let c := s1.2 in (inr b; c)
           end = (s; proj2))
      with
      | inl a =>
          (fun (a0 : A) (c : C (inl a0)) => 1) a
      | inr b =>
          (fun (b0 : B) (c : C (inr b0)) => 1) b
      end) x0.1 x0.2)
    :
    (fun
       abc : {a : A & C (inl a)} + {b : B & C (inr b)}
     =>
     match abc with
     | inl s =>
         let s0 := s in
         let a := s0.1 in let c := s0.2 in (inl a; c)
     | inr s =>
         let s0 := s in
         let b := s0.1 in let c := s0.2 in (inr b; c)
     end)
    o (fun xc : {x0 : A + B & C x0} =>
       let x0 := xc.1 in
       let c := xc.2 in
       match
         x0 as x1
         return
           (C x1 ->
            {a : A & C (inl a)} + {b : B & C (inr b)})
       with
       | inl a => fun c0 : C (inl a) => inl (a; c0)
       | inr b => fun c0 : C (inr b) => inr (b; c0)
       end c) == idmap) x) intros [[a|b] c]; reflexivity.
Defined.

(** The second is a statement about functions into a sum type. *)
Definition decompose_l {A B C} (f : C -> A + B) : Type
  := { c:C & is_inl (f c) }.

Definition decompose_r {A B C} (f : C -> A + B) : Type
  := { c:C & is_inr (f c) }.

Definition equiv_decompose {A B C} (f : C -> A + B)
: decompose_l f + decompose_r f <~> C.
A, B, C: Type
f: C -> A + B
decompose_l f + decompose_r f <~> C
Proof.
A, B, C: Type
f: C -> A + B
decompose_l f + decompose_r f <~> C
  simple refine (equiv_adjointify (sum_ind (fun _ => C) pr1 pr1) _ _ _).
A, B, C: Type
f: C -> A + B
C -> {c : C & is_inl (f c)} + {c : C & is_inr (f c)}
A, B, C: Type
f: C -> A + B
sum_ind
  (fun
     _ : {c : C & is_inl (f c)} +
         {c : C & is_inr (f c)} => C) pr1 pr1 o ?g ==
idmap
A, B, C: Type
f: C -> A + B
?g
o sum_ind
    (fun
       _ : {c : C & is_inl (f c)} +
           {c : C & is_inr (f c)} => C) pr1 pr1 ==
idmap
  -
A, B, C: Type
f: C -> A + B
C -> {c : C & is_inl (f c)} + {c : C & is_inr (f c)} intros c; destruct (is_inl_or_is_inr (f c));
    [ left | right ]; exists c; assumption.
  -
A, B, C: Type
f: C -> A + B
sum_ind
  (fun
     _ : {c : C & is_inl (f c)} +
         {c : C & is_inr (f c)} => C) pr1 pr1
o (fun c : C =>
   let s := is_inl_or_is_inr (f c) in
   match s with
   | inl i => (fun i0 : is_inl (f c) => inl (c; i0)) i
   | inr i => (fun i0 : is_inr (f c) => inr (c; i0)) i
   end) == idmap intros c; destruct (is_inl_or_is_inr (f c)); reflexivity.
  -
A, B, C: Type
f: C -> A + B
(fun c : C =>
 let s := is_inl_or_is_inr (f c) in
 match s with
 | inl i => (fun i0 : is_inl (f c) => inl (c; i0)) i
 | inr i => (fun i0 : is_inr (f c) => inr (c; i0)) i
 end)
o sum_ind
    (fun
       _ : {c : C & is_inl (f c)} +
           {c : C & is_inr (f c)} => C) pr1 pr1 ==
idmap intros [[c l]|[c r]]; simpl; destruct (is_inl_or_is_inr (f c)).
A, B, C: Type
f: C -> A + B
c: C
l, i: is_inl (f c)
inl (c; i) = inl (c; l)
A, B, C: Type
f: C -> A + B
c: C
l: is_inl (f c)
i: is_inr (f c)
inr (c; i) = inl (c; l)
A, B, C: Type
f: C -> A + B
c: C
r: is_inr (f c)
i: is_inl (f c)
inl (c; i) = inr (c; r)
A, B, C: Type
f: C -> A + B
c: C
r, i: is_inr (f c)
inr (c; i) = inr (c; r)
    +
A, B, C: Type
f: C -> A + B
c: C
l, i: is_inl (f c)
inl (c; i) = inl (c; l) apply ap, ap, path_ishprop.
    +
A, B, C: Type
f: C -> A + B
c: C
l: is_inl (f c)
i: is_inr (f c)
inr (c; i) = inl (c; l) elim (not_is_inl_and_inr' _ l i).
    +
A, B, C: Type
f: C -> A + B
c: C
r: is_inr (f c)
i: is_inl (f c)
inl (c; i) = inr (c; r) elim (not_is_inl_and_inr' _ i r).
    +
A, B, C: Type
f: C -> A + B
c: C
r, i: is_inr (f c)
inr (c; i) = inr (c; r) apply ap, ap, path_ishprop.
Defined.

Definition is_inl_decompose_l {A B C} (f : C -> A + B)
           (z : decompose_l f)
: is_inl (f (equiv_decompose f (inl z)))
  := z.2.

Definition is_inr_decompose_r {A B C} (f : C -> A + B)
           (z : decompose_r f)
: is_inr (f (equiv_decompose f (inr z)))
  := z.2.

(** ** Indecomposability *)

(** A type is indecomposable if whenever it maps into a finite sum, it lands entirely in one of the summands.  It suffices to assert this for binary and nullary sums; in the latter case it reduces to nonemptiness. *)
Class Indecomposable (X : Type) :=
  { indecompose : forall A B (f : X -> A + B),
                    (forall x, is_inl (f x)) + (forall x, is_inr (f x))
  ; indecompose0 : ~~X }.

(** For instance, contractible types are indecomposable. *)
Global Instance indecomposable_contr `{Contr X} : Indecomposable X.
X: Type
Contr0: Contr X
Indecomposable X
Proof.
X: Type
Contr0: Contr X
Indecomposable X
  constructor.
X: Type
Contr0: Contr X
forall (A B : Type) (f : X -> A + B),
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
X: Type
Contr0: Contr X
~~ X
  -
X: Type
Contr0: Contr X
forall (A B : Type) (f : X -> A + B),
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x)) intros A B f.
X: Type
Contr0: Contr X
A, B: Type
f: X -> A + B
(forall x : X, is_inl (f x)) +
(forall x : X, is_inr (f x))
    destruct (is_inl_or_is_inr (f (center X))); [ left | right ]; intros x.
X: Type
Contr0: Contr X
A, B: Type
f: X -> A + B
i: is_inl (f (center X))
x: X
is_inl (f x)
X: Type
Contr0: Contr X
A, B: Type
f: X -> A + B
i: is_inr (f (center X))
x: X
is_inr (f x)
    all:refine (transport _ (ap f (contr x)) _); assumption.
  -
X: Type
Contr0: Contr X
~~ X intros nx; exact (nx (center X)).
Defined.

(** In particular, if an indecomposable type is equivalent to a sum type, then one summand is empty and it is equivalent to the other. *)
Definition equiv_indecomposable_sum {X A B} `{Indecomposable X}
           (f : X <~> A + B)
: ((X <~> A) * (Empty <~> B)) + ((X <~> B) * (Empty <~> A)).
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
(X <~> A) * (Empty <~> B) + (X <~> B) * (Empty <~> A)
Proof.
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
(X <~> A) * (Empty <~> B) + (X <~> B) * (Empty <~> A)
  destruct (indecompose A B f) as [i|i]; [ left | right ].
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inl (f x)
(X <~> A) * (Empty <~> B)
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inr (f x)
(X <~> B) * (Empty <~> A)
  1:pose (g := (f oE sum_empty_r X)).
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inl (f x)
g:= f oE sum_empty_r X: X + Empty <~> A + B
(X <~> A) * (Empty <~> B)
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inr (f x)
(X <~> B) * (Empty <~> A)
  2:pose (g := (f oE sum_empty_l X)).
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inl (f x)
g:= f oE sum_empty_r X: X + Empty <~> A + B
(X <~> A) * (Empty <~> B)
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inr (f x)
g:= f oE sum_empty_l X: Empty + X <~> A + B
(X <~> B) * (Empty <~> A)
  2:apply (equiv_prod_symm _ _).
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inl (f x)
g:= f oE sum_empty_r X: X + Empty <~> A + B
(X <~> A) * (Empty <~> B)
X, A, B: Type
H: Indecomposable X
f: X <~> A + B
i: forall x : X, is_inr (f x)
g:= f oE sum_empty_l X: Empty + X <~> A + B
(Empty <~> A) * (X <~> B)
  all:refine (equiv_unfunctor_sum g _ _); try assumption; try intros [].
Defined.

(** Summing with an indecomposable type is injective on equivalence classes of types. *)
Definition equiv_unfunctor_sum_indecomposable_ll {A B B' : Type}
           `{Indecomposable A} (h : A + B <~> A + B')
: B <~> B'.
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
B <~> B'
Proof.
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
B <~> B'
  pose (f := equiv_decompose (h o inl)).
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
B <~> B'
  pose (g := equiv_decompose (h o inr)).
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
B <~> B'
  pose (k := (h oE (f +E g))).
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
k:= h oE (f +E g): decompose_l (h o inl) + decompose_r (h o inl) +
(decompose_l (h o inr) + decompose_r (h o inr)) <~>
A + B'
B <~> B'
  (** This looks messy, but it just amounts to swapping the middle two summands in [k]. *)
  pose (k' := k
                oE (equiv_sum_assoc _ _ _)
                oE ((equiv_sum_assoc _ _ _)^-1 +E 1)
                oE (1 +E (equiv_sum_symm _ _) +E 1)
                oE ((equiv_sum_assoc _ _ _) +E 1)
                oE (equiv_sum_assoc _ _ _)^-1).
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
k:= h oE (f +E g): decompose_l (h o inl) + decompose_r (h o inl) +
(decompose_l (h o inr) + decompose_r (h o inr)) <~>
A + B'
k':= k
oE equiv_sum_assoc
     (decompose_l (h o inl) +
      decompose_r (h o inl))
     (decompose_l (h o inr))
     (decompose_r (h o inr))
oE ((equiv_sum_assoc (decompose_l (h o inl))
       (decompose_r (h o inl))
       (decompose_l (h o inr)))^-1 +E 1)
oE (1 +E
    equiv_sum_symm (decompose_l (h o inr))
      (decompose_r (h o inl)) +E 1)
oE (equiv_sum_assoc (decompose_l (h o inl))
      (decompose_l (h o inr))
      (decompose_r (h o inl)) +E 1)
oE (equiv_sum_assoc
      (decompose_l (h o inl) +
       decompose_l (h o inr))
      (decompose_r (h o inl))
      (decompose_r (h o inr)))^-1: decompose_l (h o inl) + decompose_l (h o inr) +
(decompose_r (h o inl) + decompose_r (h o inr)) <~>
A + B'
B <~> B'
  destruct (equiv_unfunctor_sum k'
       (fun x : decompose_l (h o inl) + decompose_l (h o inr) =>
        match x as x0 return (is_inl (k' (inl x0))) with
        | inl x0 => x0.2
        | inr x0 => x0.2
        end)
       (fun x : decompose_r (h o inl) + decompose_r (h o inr) =>
        match x as x0 return (is_inr (k' (inr x0))) with
        | inl x0 => x0.2
        | inr x0 => x0.2
        end)) as [s t]; clear k k'.
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
B <~> B'
  refine (t oE (_ +E 1) oE g^-1).
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x))
  destruct (equiv_indecomposable_sum s^-1) as [[p q]|[p q]];
  destruct (equiv_indecomposable_sum f^-1) as [[u v]|[u v]].
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : A => h (inl x))
q: Empty <~> decompose_l (fun x : B => h (inr x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x))
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : A => h (inl x))
q: Empty <~> decompose_l (fun x : B => h (inr x))
u: A <~> decompose_r (fun x : A => h (inl x))
v: Empty <~> decompose_l (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x))
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x))
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_r (fun x : A => h (inl x))
v: Empty <~> decompose_l (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x))
  -
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : A => h (inl x))
q: Empty <~> decompose_l (fun x : B => h (inr x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x)) refine (v oE q^-1).
  -
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : A => h (inl x))
q: Empty <~> decompose_l (fun x : B => h (inr x))
u: A <~> decompose_r (fun x : A => h (inl x))
v: Empty <~> decompose_l (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x)) elim (indecompose0 (v^-1 o p)).
  -
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x)) refine (Empty_rec (indecompose0 _)); intros a.
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
a: A
Empty
    destruct (is_inl_or_is_inr (h (inl a))) as [l|r].
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
a: A
l: is_inl (h (inl a))
Empty
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
a: A
r: is_inr (h (inl a))
Empty
    *
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
a: A
l: is_inl (h (inl a))
Empty exact (q^-1 (a;l)).
    *
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_l (fun x : A => h (inl x))
v: Empty <~> decompose_r (fun x : A => h (inl x))
a: A
r: is_inr (h (inl a))
Empty exact (v^-1 (a;r)).
  -
A, B, B': Type
H: Indecomposable A
h: A + B <~> A + B'
f:= equiv_decompose (h o inl): decompose_l (h o inl) + decompose_r (h o inl) <~>
A
g:= equiv_decompose (h o inr): decompose_l (h o inr) + decompose_r (h o inr) <~>
B
s: decompose_l (fun x : A => h (inl x)) +
decompose_l (fun x : B => h (inr x)) <~> A
t: decompose_r (fun x : A => h (inl x)) +
decompose_r (fun x : B => h (inr x)) <~> B'
p: A <~> decompose_l (fun x : B => h (inr x))
q: Empty <~> decompose_l (fun x : A => h (inl x))
u: A <~> decompose_r (fun x : A => h (inl x))
v: Empty <~> decompose_l (fun x : A => h (inl x))
decompose_l (fun x : B => h (inr x)) <~>
decompose_r (fun x : A => h (inl x)) refine (u oE p^-1).
Defined.

Definition equiv_unfunctor_sum_contr_ll {A A' B B' : Type}
           `{Contr A} `{Contr A'}
           (h : A + B <~> A' + B')
: B <~> B'
  := equiv_unfunctor_sum_indecomposable_ll
       ((equiv_contr_contr +E 1) oE h).

(** ** Universal mapping properties *)

(** Ordinary universal mapping properties are expressed as equivalences of sets or spaces of functions.  In type theory, we can go beyond this and express an equivalence of types of *dependent* functions. *)

Definition sum_ind_uncurried {A B} (P : A + B -> Type)
           (fg : (forall a, P (inl a)) * (forall b, P (inr b)))
: forall s, P s
  := @sum_ind A B P (fst fg) (snd fg).

(* First the positive universal property.
   Doing this sort of thing without adjointifying will require very careful use of funext. *)
Global Instance isequiv_sum_ind `{Funext} `(P : A + B -> Type)
: IsEquiv (sum_ind_uncurried P) | 0.
H: Funext
A, B: Type
P: A + B -> Type
IsEquiv (sum_ind_uncurried P)
Proof.
H: Funext
A, B: Type
P: A + B -> Type
IsEquiv (sum_ind_uncurried P)
  apply (isequiv_adjointify
           (sum_ind_uncurried P)
           (fun f => (fun a => f (inl a), fun b => f (inr b))));
  repeat ((exact idpath)
            || intros []
            || intro
            || apply path_forall).
Defined.

Definition equiv_sum_ind `{Funext} `(P : A + B -> Type)
  := Build_Equiv _ _ _ (isequiv_sum_ind P).

(* The non-dependent version, which is a special case, is the sum-distributive equivalence. *)
Definition equiv_sum_distributive `{Funext} (A B C : Type)
: (A -> C) * (B -> C) <~> (A + B -> C)
  := equiv_sum_ind (fun _ => C).

(** ** Sums preserve most truncation *)

Global Instance istrunc_sum n' (n := n'.+2)
         `{IsTrunc n A, IsTrunc n B}
: IsTrunc n (A + B) | 100.
n': trunc_index
n:= n'.+2: trunc_index
A: Type
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
IsTrunc n (A + B)
Proof.
n': trunc_index
n:= n'.+2: trunc_index
A: Type
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
IsTrunc n (A + B)
  apply istrunc_S.
n': trunc_index
n:= n'.+2: trunc_index
A: Type
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
forall x y : A + B, IsTrunc n'.+1 (x = y)
  intros a b.
n': trunc_index
n:= n'.+2: trunc_index
A: Type
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
a, b: A + B
IsTrunc n'.+1 (a = b)
  eapply istrunc_equiv_istrunc;
    [ exact (equiv_path_sum _ _) | ].
n': trunc_index
n:= n'.+2: trunc_index
A: Type
IsTrunc0: IsTrunc n A
B: Type
IsTrunc1: IsTrunc n B
a, b: A + B
IsTrunc n'.+1
  match a with
  | inl z0 =>
      match b with
      | inl z'0 => z0 = z'0
      | inr _ => Empty
      end
  | inr z0 =>
      match b with
      | inl _ => Empty
      | inr z'0 => z0 = z'0
      end
  end
  destruct a, b; exact _.
Defined.

Global Instance ishset_sum `{HA : IsHSet A, HB : IsHSet B} : IsHSet (A + B) | 100
  := @istrunc_sum (-2) A HA B HB.

(** Sums don't preserve hprops in general, but they do for disjoint sums. *)

Global Instance ishprop_sum A B `{IsHProp A} `{IsHProp B}
: (A -> B -> Empty) -> IsHProp (A + B).
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
(A -> B -> Empty) -> IsHProp (A + B)
Proof.
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
(A -> B -> Empty) -> IsHProp (A + B)
  intros H.
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
IsHProp (A + B)
  apply hprop_allpath; intros [a1|b1] [a2|b2].
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
a1, a2: A
inl a1 = inl a2
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
a1: A
b2: B
inl a1 = inr b2
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
b1: B
a2: A
inr b1 = inl a2
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
b1, b2: B
inr b1 = inr b2
  -
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
a1, a2: A
inl a1 = inl a2 apply ap, path_ishprop.
  -
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
a1: A
b2: B
inl a1 = inr b2 case (H a1 b2).
  -
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
b1: B
a2: A
inr b1 = inl a2 case (H a2 b1).
  -
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
H: A -> B -> Empty
b1, b2: B
inr b1 = inr b2 apply ap, path_ishprop.
Defined.

(** ** Decidability *)

(** Sums preserve decidability *)
Global Instance decidable_sum {A B : Type}
       `{Decidable A} `{Decidable B}
: Decidable (A + B).
A, B: Type
H: Decidable A
H0: Decidable B
Decidable (A + B)
Proof.
A, B: Type
H: Decidable A
H0: Decidable B
Decidable (A + B)
  destruct (dec A) as [x1|y1].
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
Decidable (A + B)
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
Decidable (A + B)
  -
A, B: Type
H: Decidable A
H0: Decidable B
x1: A
Decidable (A + B) exact (inl (inl x1)).
  -
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
Decidable (A + B) destruct (dec B) as [x2|y2].
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
x2: B
Decidable (A + B)
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
Decidable (A + B)
    +
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
x2: B
Decidable (A + B) exact (inl (inr x2)).
    +
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
Decidable (A + B) apply inr; intros z.
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
z: A + B
Empty
      destruct z as [x1|x2].
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
x1: A
Empty
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
x2: B
Empty
      *
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
x1: A
Empty exact (y1 x1).
      *
A, B: Type
H: Decidable A
H0: Decidable B
y1: ~ A
y2: ~ B
x2: B
Empty exact (y2 x2).
Defined.

(** Sums preserve decidable paths *)
Global Instance decidablepaths_sum {A B}
       `{DecidablePaths A} `{DecidablePaths B}
: DecidablePaths (A + B).
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
DecidablePaths (A + B)
Proof.
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
DecidablePaths (A + B)
  intros [a1|b1] [a2|b2].
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
Decidable (inl a1 = inl a2)
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1: A
b2: B
Decidable (inl a1 = inr b2)
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1: B
a2: A
Decidable (inr b1 = inl a2)
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
Decidable (inr b1 = inr b2)
  -
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
Decidable (inl a1 = inl a2) destruct (dec_paths a1 a2) as [p|np].
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
p: a1 = a2
Decidable (inl a1 = inl a2)
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
np: a1 <> a2
Decidable (inl a1 = inl a2)
    +
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
p: a1 = a2
Decidable (inl a1 = inl a2) exact (inl (ap inl p)).
    +
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
np: a1 <> a2
Decidable (inl a1 = inl a2) apply inr; intros p.
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1, a2: A
np: a1 <> a2
p: inl a1 = inl a2
Empty
      exact (np ((path_sum _ _)^-1 p)).
  -
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
a1: A
b2: B
Decidable (inl a1 = inr b2) exact (inr (path_sum _ _)^-1).
  -
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1: B
a2: A
Decidable (inr b1 = inl a2) exact (inr (path_sum _ _)^-1).
  -
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
Decidable (inr b1 = inr b2) destruct (dec_paths b1 b2) as [p|np].
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
p: b1 = b2
Decidable (inr b1 = inr b2)
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
np: b1 <> b2
Decidable (inr b1 = inr b2)
    +
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
p: b1 = b2
Decidable (inr b1 = inr b2) exact (inl (ap inr p)).
    +
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
np: b1 <> b2
Decidable (inr b1 = inr b2) apply inr; intros p.
A, B: Type
H: DecidablePaths A
H0: DecidablePaths B
b1, b2: B
np: b1 <> b2
p: inr b1 = inr b2
Empty
      exact (np ((path_sum _ _)^-1 p)).
Defined.

(** Because of [ishprop_sum], decidability of an hprop is again an hprop. *)
Global Instance ishprop_decidable_hprop `{Funext} A `{IsHProp A}
: IsHProp (Decidable A).
H: Funext
A: Type
IsHProp0: IsHProp A
IsHProp (Decidable A)
Proof.
H: Funext
A: Type
IsHProp0: IsHProp A
IsHProp (Decidable A)
  unfold Decidable; refine (ishprop_sum _ _ _).
H: Funext
A: Type
IsHProp0: IsHProp A
A -> ~ A -> Empty
  intros a na; exact (na a).
Defined.

(** ** Binary coproducts are equivalent to dependent sigmas where the first component is a bool. *)

Definition sig_of_sum A B (x : A + B)
: { b : Bool & if b then A else B }
  := (_;
      match
        x as s
        return
        (if match s with
              | inl _ => true
              | inr _ => false
            end then A else B)
      with
        | inl a => a
        | inr b => b
      end).

Definition sum_of_sig A B (x : { b : Bool & if b then A else B })
: A + B
  := match x with
       | (true; a) => inl a
       | (false; b) => inr b
     end.

Global Instance isequiv_sig_of_sum A B : IsEquiv (@sig_of_sum A B) | 0.
A, B: Type
IsEquiv (sig_of_sum A B)
Proof.
A, B: Type
IsEquiv (sig_of_sum A B)
  apply (isequiv_adjointify (@sig_of_sum A B)
                            (@sum_of_sig A B)).
A, B: Type
(fun x : {b : Bool & if b then A else B} =>
 sig_of_sum A B (sum_of_sig A B x)) == idmap
A, B: Type
(fun x : A + B => sum_of_sig A B (sig_of_sum A B x)) ==
idmap
  -
A, B: Type
(fun x : {b : Bool & if b then A else B} =>
 sig_of_sum A B (sum_of_sig A B x)) == idmap intros [[] ?]; exact idpath.
  -
A, B: Type
(fun x : A + B => sum_of_sig A B (sig_of_sum A B x)) ==
idmap intros []; exact idpath.
Defined.

Global Instance isequiv_sum_of_sig A B : IsEquiv (sum_of_sig A B)
  := isequiv_inverse (@sig_of_sum A B).

(** An alternative way of proving the truncation property of [sum]. *)
Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B}
: (IsTrunc n (A + B)).
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n Bool
IsTrunc1: IsTrunc n A
IsTrunc2: IsTrunc n B
IsTrunc n (A + B)
Proof.
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n Bool
IsTrunc1: IsTrunc n A
IsTrunc2: IsTrunc n B
IsTrunc n (A + B)
  eapply istrunc_equiv_istrunc; [ esplit;
                         exact (@isequiv_sum_of_sig _ _)
                       | ].
n: trunc_index
A, B: Type
IsTrunc0: IsTrunc n Bool
IsTrunc1: IsTrunc n A
IsTrunc2: IsTrunc n B
IsTrunc n {b : Bool & if b then A else B}
  typeclasses eauto.
Defined.