Library HoTT.Spaces.Universe

(* -*- mode: coq; mode: visual-line -*-  *)
Require Import Basics Types.
Require Import HoTT.Truncations.
Require Import Spaces.BAut Spaces.BAut.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, Escardo, 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.
  Proof.
    refine (((equiv_decidable_sum (fun X:Type ⇒ merely (X=A)))^-1)
              oE _ oE
              (equiv_decidable_sum (fun 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))))).
    refine ((equiv_sum_assoc _ _ _)
              oE _ oE
              (equiv_sum_assoc _ _ _)^-1).
    apply equiv_functor_sum_r.
    assert (q : BAut B <~> {x : {x : Type & ¬ merely (x = A)} &
                                merely (x.1 = B)}).
    { refine (equiv_sigma_assoc _ _ oE _).
      apply equiv_functor_sigma_id; intros X.
      apply equiv_iff_hprop.
      - intros p.
        refine (fun q ⇒ _ ; p).
        strip_truncations.
        destruct q.
        exact (ne (equiv_path X B p)).
      - exact pr2. }
    refine (_ oE equiv_sum_symm _ _).
    apply equiv_functor_sum'.
    - exact (e^-1 oE q^-1).
    - exact (q oE e).
  Defined.

  Definition equiv_swap_types_swaps : merely (equiv_swap_types A = B).
  Proof.
    assert (ea := (e (point _)).2). cbn in ea.
    strip_truncations; apply tr.
    unfold equiv_swap_types.
    apply moveR_equiv_V.
    rewrite (equiv_decidable_sum_l
               (fun X ⇒ merely (X=A)) A (tr 1)).
    assert (ne' : ¬ merely (B=A))
      by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
    rewrite (equiv_decidable_sum_r
               (fun X ⇒ merely (X=A)) B ne').
    cbn.
    apply ap, path_sigma_hprop; cbn.
    exact ea.
  Defined.

  Definition equiv_swap_types_not_id
    : equiv_swap_types ≠ equiv_idmap.
  Proof.
    intros p.
    assert (q := equiv_swap_types_swaps).
    strip_truncations.
    apply ne.
    apply equiv_path.
    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.
Proof.
  refine (equiv_swap_types A B ne _).
  apply 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.
Proof.
  unfold equiv_swap_rigid, equiv_swap_types.
  apply moveR_equiv_V.
  rewrite (equiv_decidable_sum_l
             (fun X ⇒ merely (X=A)) A (tr 1)).
  assert (ne' : ¬ merely (B=A))
    by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
  rewrite (equiv_decidable_sum_r
             (fun X ⇒ merely (X=A)) B ne').
  cbn.
  apply ap, path_sigma_hprop; cbn.
  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.
Proof.
  refine (equiv_swap_types (X×A) (X×B) ne _).
  transitivity (BAut X).
  - symmetry; exact (baut_prod_rigid_equiv X A n).
  - 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.
Proof.
  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
  ∃ (f P); split.
  - intros p.
    assert (Contr P) by (apply contr_inhabited_hprop; assumption).
    assert (q : Unit = P)
      by (apply path_universe_uncurried, equiv_contr_contr).
    destruct q.
    rewrite eu.
    auto.
  - intros nfp.
    assert (q : f P = Empty)
      by (apply path_universe_uncurried, equiv_to_empty, nfp).
    rewrite <- eu in q.
    apply ((ap f)^-1) in q.
    rewrite q; exact tt.
Defined.

Lemma equiv_hprop_idprod `{Univalence}
      (A : Type) (P : Type) (a : merely A) `{IsHProp P}
  : P ↔ (P × A = A).
Proof.
  split.
  - intros p; apply path_universe with snd.
    apply isequiv_adjointify with (fun a ⇒ (p,a)).
    + intros x; reflexivity.
    + intros [p' x].
      apply path_prod; [ apply path_ishprop | reflexivity ].
  - intros q.
    strip_truncations.
    apply equiv_path in q.
    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.
Proof.
  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
  ∃ (f (P × A)); split.
  - intros p.
    assert (q := fst (equiv_hprop_idprod A P a) p).
    apply (ap f) in q.
    rewrite eu in q.
    rewrite q; auto.
  - intros q.
    apply equiv_to_empty in q.
    apply path_universe_uncurried in q.
    rewrite <- eu in q.
    apply ((ap f)^-1) in q.
    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.
Proof.
  pose (f := equiv_inverse g).
  intros nlem.
  apply ge.
  apply path_universe_uncurried, equiv_to_empty; intros gz.
  apply nlem.
  apply (lem_from_aut_type_inhabited_empty f (g Empty) (tr gz)).
  unfold f; apply eissect.
Defined.

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