Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HoTT.Truncations.
Require Import Universes.BAut Universes.Rigid.
Require Import ExcludedMiddle.

Local Open Scope trunc_scope.
Local Open Scope path_scope.

(** * The universe *)

(** ** Automorphisms of the universe *)

(** See "Parametricity, automorphisms of the universe, and excluded middle" by Booij, Escardó, Lumsdaine, Shulman. *)

(** If two inequivalent types have equivalent automorphism oo-groups, then assuming LEM we can swap them and leave the rest of the universe untouched. *)
Section SwapTypes.
  (** Amusingly, this does not actually require univalence!  But of course, to verify [BAut A <~> BAut B] in any particular example does require univalence. *)
  Context `{Funext} `{ExcludedMiddle}.
  Context (A B : Type) (ne : ~(A <~> B)) (e : BAut A <~> BAut B).

  Definition equiv_swap_types : Type <~> Type.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
Type <~> Type
  Proof.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
Type <~> Type
    refine (((equiv_decidable_sum (fun X:Type => merely (X=A)))^-1)
              oE _ oE
              (equiv_decidable_sum (fun X:Type => merely (X=A)))).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
{x : Type & merely (x = A)} +
{x : Type & ~ merely (x = A)} <~>
{x : Type & merely (x = A)} +
{x : Type & ~ merely (x = A)}
    refine ((equiv_functor_sum_l
               (equiv_decidable_sum (fun X => merely (X.1=B)))^-1)
              oE _ oE
              (equiv_functor_sum_l
                 (equiv_decidable_sum (fun X => merely (X.1=B))))).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
{x : Type & merely (x = A)} +
({x : {x : Type & ~ merely (x = A)} &
 merely (x.1 = B)} +
 {x : {x : Type & ~ merely (x = A)} &
 ~ merely (x.1 = B)}) <~>
{x : Type & merely (x = A)} +
({x : {x : Type & ~ merely (x = A)} &
 merely (x.1 = B)} +
 {x : {x : Type & ~ merely (x = A)} &
 ~ merely (x.1 = B)})
    refine ((equiv_sum_assoc _ _ _)
              oE _ oE
              (equiv_sum_assoc _ _ _)^-1).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} +
{x : {x : Type & ~ merely (x = A)} &
~ merely (x.1 = B)} <~>
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} +
{x : {x : Type & ~ merely (x = A)} &
~ merely (x.1 = B)}
    apply equiv_functor_sum_r.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} <~>
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
    assert (q : BAut B <~> {x : {x : Type & ~ merely (x = A)} &
                                merely (x.1 = B)}).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
BAut B <~>
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} <~>
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
    {
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
BAut B <~>
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} refine (equiv_sigma_assoc _ _ oE _).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
BAut B <~>
{a : Type &
{p : ~ merely (a = A) & merely ((a; p).1 = B)}}
      apply equiv_functor_sigma_id; intros X.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
merely (X = B) <~>
{p : ~ merely (X = A) & merely ((X; p).1 = B)}
      apply equiv_iff_hprop.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
merely (X = B) ->
{p : ~ merely (X = A) & merely ((X; p).1 = B)}
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
{p : ~ merely (X = A) & merely ((X; p).1 = B)} ->
merely (X = B)
      -
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
merely (X = B) ->
{p : ~ merely (X = A) & merely ((X; p).1 = B)} intros p.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
p: merely (X = B)
{p : ~ merely (X = A) & merely ((X; p).1 = B)}
        refine (fun q => _ ; p).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
p: merely (X = B)
q: merely (X = A)
Empty
        strip_truncations.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
q: X = A
p: X = B
Empty
        destruct q.
H: Funext
H0: ExcludedMiddle
B, X: Type
ne: ~ (X <~> B)
e: BAut X <~> BAut B
p: X = B
Empty
        exact (ne (equiv_path X B p)).
      -
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
X: Type
{p : ~ merely (X = A) & merely ((X; p).1 = B)} ->
merely (X = B) exact pr2. }
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} <~>
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
    refine (_ oE equiv_sum_symm _ _).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} +
{x : Type & merely (x = A)} <~>
{x : Type & merely (x = A)} +
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
    apply equiv_functor_sum'.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} <~>
{x : Type & merely (x = A)}
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : Type & merely (x = A)} <~>
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)}
    -
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} <~>
{x : Type & merely (x = A)} exact (e^-1 oE q^-1).
    -
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
q: BAut B <~>
{x : {x : Type & ~ merely (x = A)} &
merely (x.1 = B)}
{x : Type & merely (x = A)} <~>
{x : {x : Type & ~ merely (x = A)} & merely (x.1 = B)} exact (q oE e).
  Defined.

  Definition equiv_swap_types_swaps : merely (equiv_swap_types A = B).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
merely (equiv_swap_types A = B)
  Proof.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
merely (equiv_swap_types A = B)
    assert (ea := (e (point _)).2).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (fun Z : Type => trunctype_type (merely (Z = B)))
  (e (point (BAut A))).1
merely (equiv_swap_types A = B) cbn in ea.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: Trunc (-1) ((e (point (BAut A))).1 = B)
merely (equiv_swap_types A = B)
    strip_truncations; apply tr.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
equiv_swap_types A = B
    unfold equiv_swap_types.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
((equiv_decidable_sum (fun X : Type => merely (X = A)))^-1
 oE (equiv_functor_sum_l
       (equiv_decidable_sum
          (fun X : {x : Type & ~ merely (x = A)} =>
           merely (X.1 = B)))^-1
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)}
         oE equiv_functor_sum_r
              ((e^-1
                oE (equiv_sigma_assoc
                      (fun a : Type =>
                       ~ merely (a = A))
                      (fun
                         x : {x : Type & ~ merely ...}
                       => merely (x.1 = B))
                    oE equiv_functor_sigma_id
                         (fun X : Type =>
                          equiv_iff_hprop
                            (fun p : ... =>
                             (... => ...; p)) pr2))^-1 +E
                equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun x : {x : Type & ~ merely (...)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely ... =>
                         (fun ... =>
                          Trunc_ind ... ... q; p)) pr2)
                oE e)
               oE equiv_sum_symm
                    {x : Type & merely (x = A)}
                    {x : {x : Type & ~ merely (x = A)}
                    & merely (x.1 = B)})
         oE (equiv_sum_assoc
               {x : Type & merely (x = A)}
               {x : {x : Type & ~ merely (x = A)} &
               merely (x.1 = B)}
               {x : {x : Type & ~ merely (x = A)} &
               ~ merely (x.1 = B)})^-1)
     oE equiv_functor_sum_l
          (equiv_decidable_sum
             (fun X : {x : Type & ~ merely (x = A)} =>
              merely (X.1 = B))))
 oE equiv_decidable_sum
      (fun X : Type => merely (X = A))) A = B
    apply moveR_equiv_V.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((e^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE e)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B))))
  (equiv_decidable_sum
     (fun X : Type => merely (X = A)) A) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
    rewrite (equiv_decidable_sum_l
               (fun X => merely (X=A)) A (tr 1)).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((e^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE e)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
    assert (ne' : ~ merely (B=A))
      by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
ne': ~ merely (B = A)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((e^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE e)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
    rewrite (equiv_decidable_sum_r
               (fun X => merely (X=A)) B ne').
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
ne': ~ merely (B = A)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((e^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE e)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
inr (B; ne')
    cbn.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
ne': ~ merely (B = A)
inr
  ((e (A; tr 1)).1;
  fun q : Trunc (-1) ((e (A; tr 1)).1 = A) =>
  Trunc_ind
    (fun _ : Trunc (-1) ((e (A; tr 1)).1 = A) => Empty)
    (fun q0 : (e (A; tr 1)).1 = A =>
     Trunc_ind
       (fun _ : Trunc (-1) ((e (A; tr 1)).1 = B) =>
        Empty)
       (fun p : (e (A; tr 1)).1 = B =>
        match
          q0 in (_ = T)
          return
            (~ (T <~> B) -> BAut T <~> BAut B -> Empty)
        with
        | 1 =>
            fun (ne : ~ ((e (A; tr 1)).1 <~> B))
              (_ : BAut (e (A; tr 1)).1 <~> BAut B) =>
            ne (equiv_path (e (A; tr 1)).1 B p)
        end ne e) (e (A; tr 1)).2) q) = inr (B; ne')
    apply ap, path_sigma_hprop; cbn.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
ea: (e (point (BAut A))).1 = B
ne': ~ merely (B = A)
(e (A; tr 1)).1 = B
    exact ea.
  Defined.

  Definition equiv_swap_types_not_id
    : equiv_swap_types <> equiv_idmap.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
equiv_swap_types <> 1%equiv
  Proof.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
equiv_swap_types <> 1%equiv
    intros p.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
p: equiv_swap_types = 1%equiv
Empty
    assert (q := equiv_swap_types_swaps).
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
p: equiv_swap_types = 1%equiv
q: merely (equiv_swap_types A = B)
Empty
    strip_truncations.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
p: equiv_swap_types = 1%equiv
q: equiv_swap_types A = B
Empty
    apply ne.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
p: equiv_swap_types = 1%equiv
q: equiv_swap_types A = B
A <~> B
    apply equiv_path.
H: Funext
H0: ExcludedMiddle
A, B: Type
ne: ~ (A <~> B)
e: BAut A <~> BAut B
p: equiv_swap_types = 1%equiv
q: equiv_swap_types A = B
A = B
    rewrite p in q; exact q.
  Qed.

End SwapTypes.

(** In particular, we can swap any two distinct rigid types. *)

Definition equiv_swap_rigid `{Univalence} `{ExcludedMiddle}
           (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B))
  : Type <~> Type.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
Type <~> Type
Proof.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
Type <~> Type
  refine (equiv_swap_types A B ne _).
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
BAut A <~> BAut B
  exact equiv_contr_contr.
Defined.

(** Such as [Empty] and [Unit]. *)

Definition equiv_swap_empty_unit `{Univalence} `{ExcludedMiddle}
  : Type <~> Type
  := equiv_swap_rigid Empty Unit (fun e => e^-1 tt).

(** In this case we get an untruncated witness of the swapping. *)

Definition equiv_swap_rigid_swaps `{Univalence} `{ExcludedMiddle}
           (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B))
  : equiv_swap_rigid A B ne A = B.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
equiv_swap_rigid A B ne A = B
Proof.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
equiv_swap_rigid A B ne A = B
  unfold equiv_swap_rigid, equiv_swap_types.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
((equiv_decidable_sum (fun X : Type => merely (X = A)))^-1
 oE (equiv_functor_sum_l
       (equiv_decidable_sum
          (fun X : {x : Type & ~ merely (x = A)} =>
           merely (X.1 = B)))^-1
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)}
         oE equiv_functor_sum_r
              ((equiv_contr_contr^-1
                oE (equiv_sigma_assoc
                      (fun a : Type =>
                       ~ merely (a = A))
                      (fun
                         x : {x : Type & ~ merely ...}
                       => merely (x.1 = B))
                    oE equiv_functor_sigma_id
                         (fun X : Type =>
                          equiv_iff_hprop
                            (fun p : ... =>
                             (... => ...; p)) pr2))^-1 +E
                equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun x : {x : Type & ~ merely (...)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely ... =>
                         (fun ... =>
                          Trunc_ind ... ... q; p)) pr2)
                oE equiv_contr_contr)
               oE equiv_sum_symm
                    {x : Type & merely (x = A)}
                    {x : {x : Type & ~ merely (x = A)}
                    & merely (x.1 = B)})
         oE (equiv_sum_assoc
               {x : Type & merely (x = A)}
               {x : {x : Type & ~ merely (x = A)} &
               merely (x.1 = B)}
               {x : {x : Type & ~ merely (x = A)} &
               ~ merely (x.1 = B)})^-1)
     oE equiv_functor_sum_l
          (equiv_decidable_sum
             (fun X : {x : Type & ~ merely (x = A)} =>
              merely (X.1 = B))))
 oE equiv_decidable_sum
      (fun X : Type => merely (X = A))) A = B
  apply moveR_equiv_V.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((equiv_contr_contr^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE equiv_contr_contr)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B))))
  (equiv_decidable_sum
     (fun X : Type => merely (X = A)) A) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
  rewrite (equiv_decidable_sum_l
             (fun X => merely (X=A)) A (tr 1)).
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((equiv_contr_contr^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE equiv_contr_contr)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
  assert (ne' : ~ merely (B=A))
    by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
ne': ~ merely (B = A)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((equiv_contr_contr^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE equiv_contr_contr)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
equiv_decidable_sum (fun X : Type => merely (X = A)) B
  rewrite (equiv_decidable_sum_r
             (fun X => merely (X=A)) B ne').
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
ne': ~ merely (B = A)
(equiv_functor_sum_l
   (equiv_decidable_sum
      (fun X : {x : Type & ~ merely (x = A)} =>
       merely (X.1 = B)))^-1
 oE (equiv_sum_assoc {x : Type & merely (x = A)}
       {x : {x : Type & ~ merely (x = A)} &
       merely (x.1 = B)}
       {x : {x : Type & ~ merely (x = A)} &
       ~ merely (x.1 = B)}
     oE equiv_functor_sum_r
          ((equiv_contr_contr^-1
            oE (equiv_sigma_assoc
                  (fun a : Type => ~ merely (a = A))
                  (fun
                     x : {x : Type & ~ merely (x = A)}
                   => merely (x.1 = B))
                oE equiv_functor_sigma_id
                     (fun X : Type =>
                      equiv_iff_hprop
                        (fun p : merely (X = B) =>
                         (fun q : merely ... =>
                          Trunc_ind (... => Empty)
                            (... => ...) q; p)) pr2))^-1 +E
            equiv_sigma_assoc
              (fun a : Type => ~ merely (a = A))
              (fun x : {x : Type & ~ merely (x = A)}
               => merely (x.1 = B))
            oE equiv_functor_sigma_id
                 (fun X : Type =>
                  equiv_iff_hprop
                    (fun p : merely (X = B) =>
                     (fun q : merely (...) =>
                      Trunc_ind (fun ... => Empty)
                        (fun ... =>
                         Trunc_ind ... ... p) q; p))
                    pr2) oE equiv_contr_contr)
           oE equiv_sum_symm
                {x : Type & merely (x = A)}
                {x : {x : Type & ~ merely (x = A)} &
                merely (x.1 = B)})
     oE (equiv_sum_assoc {x : Type & merely (x = A)}
           {x : {x : Type & ~ merely (x = A)} &
           merely (x.1 = B)}
           {x : {x : Type & ~ merely (x = A)} &
           ~ merely (x.1 = B)})^-1)
 oE equiv_functor_sum_l
      (equiv_decidable_sum
         (fun X : {x : Type & ~ merely (x = A)} =>
          merely (X.1 = B)))) (inl (A; tr 1)) =
inr (B; ne')
  cbn.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
ne': ~ merely (B = A)
inr
  (B;
  fun q : Trunc (-1) (B = A) =>
  Trunc_ind (fun _ : Trunc (-1) (B = A) => Empty)
    (fun q0 : B = A =>
     match
       q0 in (_ = T)
       return
         (~ (T <~> B) -> BAut T <~> BAut B -> Empty)
     with
     | 1 =>
         fun (ne : ~ (B <~> B))
           (_ : BAut B <~> BAut B) =>
         ne (equiv_path B B 1)
     end ne equiv_contr_contr) q) = inr (B; ne')
  apply ap, path_sigma_hprop; cbn.
H: Univalence
H0: ExcludedMiddle
A, B: Type
H1: IsRigid A
H2: IsRigid B
ne: ~ (A <~> B)
ne': ~ merely (B = A)
B = B
  exact ((path_contr (center (BAut B)) (point (BAut B)))..1).
Defined.

(** We can also swap the products of two rigid types with another type [X], under a connectedness/truncatedness assumption. *)

Definition equiv_swap_prod_rigid  `{Univalence} `{ExcludedMiddle}
           (X A B : Type) (n : trunc_index) (ne : ~(X*A <~> X*B))
           `{IsRigid A} `{IsConnected n.+1 A}
           `{IsRigid B} `{IsConnected n.+1 B}
           `{IsTrunc n.+1 X}
  : Type <~> Type.
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
Type <~> Type
Proof.
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
Type <~> Type
  refine (equiv_swap_types (X*A) (X*B) ne _).
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
BAut (X * A) <~> BAut (X * B)
  transitivity (BAut X).
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
BAut (X * A) <~> BAut X
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
BAut X <~> BAut (X * B)
  -
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
BAut (X * A) <~> BAut X symmetry; exact (baut_prod_rigid_equiv X A n).
  -
H: Univalence
H0: ExcludedMiddle
X, A, B: Type
n: trunc_index
ne: ~ (X * A <~> X * B)
H1: IsRigid A
H2: IsConnected (Tr n.+1) A
H3: IsRigid B
H4: IsConnected (Tr n.+1) B
IsTrunc0: IsTrunc n.+1 X
BAut X <~> BAut (X * B) exact (baut_prod_rigid_equiv X B n).
Defined.

(** Conversely, from some nontrivial automorphisms of the universe we can deduce nonconstructive consequences. *)

Definition lem_from_aut_type_unit_empty `{Univalence}
           (f : Type <~> Type) (eu : f Unit = Empty)
  : ExcludedMiddle_type.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
ExcludedMiddle_type
Proof.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
ExcludedMiddle_type
  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
{Q : Type & P <-> ~ Q}
  exists (f P); split.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
P -> ~ f P
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
~ f P -> P
  -
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
P -> ~ f P intros p.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
p: P
~ f P
    assert (Contr P) by (apply contr_inhabited_hprop; assumption).
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type
X: IsHProp P
p: P
X0: Contr P
~ f P
    assert (q : Unit = P)
      by (apply path_universe_uncurried, equiv_contr_contr).
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
p: P
X0: Contr P
q: Unit = P
~ f P
    destruct q.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
X: IsHProp Unit
p: Unit
X0: Contr Unit
~ f Unit
    rewrite eu.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
X: IsHProp Unit
p: Unit
X0: Contr Unit
~ Empty
    auto.
  -
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
~ f P -> P intros nfp.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
nfp: ~ f P
P
    assert (q : f P = Empty)
      by (apply path_universe_uncurried, equiv_to_empty, nfp).
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
nfp: ~ f P
q: f P = Empty
P
    rewrite <- eu in q.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
nfp: ~ f P
q: f P = f Unit
P
    apply ((ap f)^-1) in q.
H: Univalence
f: Type <~> Type
eu: f Unit = Empty
P: Type0
X: IsHProp P
nfp: ~ f P
q: P = Unit
P
    rewrite q; exact tt.
Defined.

Lemma equiv_hprop_idprod `{Univalence}
      (A : Type) (P : Type) (a : merely A) `{IsHProp P}
  : P <-> (P * A = A).
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P <-> P * A = A
Proof.
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P <-> P * A = A
  split.
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P -> P * A = A
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P * A = A -> P
  -
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P -> P * A = A intros p; apply path_universe with snd.
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p: P
IsEquiv snd
    apply isequiv_adjointify with (fun a => (p,a)).
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p: P
(fun x : A => snd (p, x)) == idmap
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p: P
(fun x : P * A => (p, snd x)) == idmap
    +
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p: P
(fun x : A => snd (p, x)) == idmap intros x; reflexivity.
    +
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p: P
(fun x : P * A => (p, snd x)) == idmap intros [p' x].
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
p, p': P
x: A
(p, snd (p', x)) = (p', x)
      apply path_prod; [ apply path_ishprop | reflexivity ].
  -
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
P * A = A -> P intros q.
H: Univalence
A, P: Type
a: merely A
IsHProp0: IsHProp P
q: P * A = A
P
    strip_truncations.
H: Univalence
A, P: Type
IsHProp0: IsHProp P
q: P * A = A
a: A
P
    apply equiv_path in q.
H: Univalence
A, P: Type
IsHProp0: IsHProp P
q: P * A <~> A
a: A
P
    exact (fst (q^-1 a)).
Defined.

Definition lem_from_aut_type_inhabited_empty `{Univalence}
           (f : Type <~> Type)
           (A : Type) (a : merely A) (eu : f A = Empty)
  : ExcludedMiddle_type.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
ExcludedMiddle_type
Proof.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
ExcludedMiddle_type
  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
{Q : Type & P <-> ~ Q}
  exists (f (P * A)); split.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
P -> ~ f (P * A)
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
~ f (P * A) -> P
  -
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
P -> ~ f (P * A) intros p.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
p: P
~ f (P * A)
    assert (q := fst (equiv_hprop_idprod A P a) p).
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
p: P
q: P * A = A
~ f (P * A)
    apply (ap f) in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
p: P
q: f (P * A) = f A
~ f (P * A)
    rewrite eu in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
p: P
q: f (P * A) = Empty
~ f (P * A)
    rewrite q; auto.
  -
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
~ f (P * A) -> P intros q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
q: ~ f (P * A)
P
    apply equiv_to_empty in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
q: f (P * A) <~> Empty
P
    apply path_universe_uncurried in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
q: f (P * A) = Empty
P
    rewrite <- eu in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
q: f (P * A) = f A
P
    apply ((ap f)^-1) in q.
H: Univalence
f: Type <~> Type
A: Type
a: merely A
eu: f A = Empty
P: Type
X: IsHProp P
q: P * A = A
P
    exact (snd (equiv_hprop_idprod A P a) q).
Defined.

(** If you can derive a constructive taboo from an automorphism of the universe such that [g X <> X], then you get [X]-many beers; see <https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/blCo7x-B7aoJ>. *)

Definition zero_beers `{Univalence}
           (g : Type <~> Type) (ge : g Empty <> Empty)
  : ~~ExcludedMiddle_type.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
~~ ExcludedMiddle_type
Proof.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
~~ ExcludedMiddle_type
  pose (f := equiv_inverse g).
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
~~ ExcludedMiddle_type
  intros nlem.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
nlem: ~ ExcludedMiddle_type
Empty
  apply ge.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
nlem: ~ ExcludedMiddle_type
g Empty = Empty
  apply path_universe_uncurried, equiv_to_empty; intros gz.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
nlem: ~ ExcludedMiddle_type
gz: g Empty
Empty
  apply nlem.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
nlem: ~ ExcludedMiddle_type
gz: g Empty
ExcludedMiddle_type
  apply (lem_from_aut_type_inhabited_empty f (g Empty) (tr gz)).
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
f:= g^-1%equiv: Type <~> Type
nlem: ~ ExcludedMiddle_type
gz: g Empty
f (g Empty) = Empty
  unfold f; apply eissect.
Defined.

Definition lem_beers `{Univalence}
           (g : Type <~> Type) (ge : g ExcludedMiddle_type <> ExcludedMiddle_type)
  : ~~ExcludedMiddle_type.
H: Univalence
g: Type <~> Type
ge: g ExcludedMiddle_type <> ExcludedMiddle_type
~~ ExcludedMiddle_type
Proof.
H: Univalence
g: Type <~> Type
ge: g ExcludedMiddle_type <> ExcludedMiddle_type
~~ ExcludedMiddle_type
  intros nlem.
H: Univalence
g: Type <~> Type
ge: g ExcludedMiddle_type <> ExcludedMiddle_type
nlem: ~ ExcludedMiddle_type
Empty
  pose (nlem' := equiv_to_empty nlem).
H: Univalence
g: Type <~> Type
ge: g ExcludedMiddle_type <> ExcludedMiddle_type
nlem: ~ ExcludedMiddle_type
nlem':= equiv_to_empty nlem: ExcludedMiddle_type <~> Empty
Empty
  apply path_universe_uncurried in nlem'.
H: Univalence
g: Type <~> Type
ge: g ExcludedMiddle_type <> ExcludedMiddle_type
nlem: ~ ExcludedMiddle_type
nlem': ExcludedMiddle_type = Empty
Empty
  rewrite nlem' in ge.
H: Univalence
g: Type <~> Type
ge: g Empty <> Empty
nlem: ~ ExcludedMiddle_type
nlem': ExcludedMiddle_type = Empty
Empty
  apply (zero_beers g) in ge.
H: Univalence
g: Type <~> Type
ge: ~~ ExcludedMiddle_type
nlem: ~ ExcludedMiddle_type
nlem': ExcludedMiddle_type = Empty
Empty
  exact (ge nlem).
Defined.