Require Import HoTT.Basics HoTT.Types Universes.HProp.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modality.

Local Open Scope path_scope.

(** * The double negation modality *)

(** The operation sending [X] to [~~X] is a modality.  This is Exercise 7.12 in the book.  Note that it is (apparently) *not* accessible unless we assume propositional resizing. *)
Definition NotNot `{Funext} : Modality.
H: Funext
Modality
Proof.
H: Funext
Modality
  snapply easy_modality.
H: Funext
Type -> Type
H: Funext
forall T : Type, T -> ?O_reflector T
H: Funext
forall (A : Type) (B : ?O_reflector A -> Type),
(forall a : A, ?O_reflector (B (?to A a))) ->
forall z : ?O_reflector A, ?O_reflector (B z)
H: Funext
forall (A : Type) (B : ?O_reflector A -> Type)
(f : forall a : A, ?O_reflector (B (?to A a)))
(a : A), ?O_indO A B f (?to A a) = f a
H: Funext
forall (A : Type) (z z' : ?O_reflector A),
IsEquiv (?to (z = z'))
  -
H: Funext
Type -> Type intros X; exact (~~X).
  -
H: Funext
forall T : Type, T -> (fun X : Type => ~~ X) T exact @not_not_unit.
  -
H: Funext
forall (A : Type)
(B : (fun X : Type => ~~ X) A -> Type),
(forall a : A,
 (fun X : Type => ~~ X) (B (not_not_unit a))) ->
forall z : (fun X : Type => ~~ X) A,
(fun X : Type => ~~ X) (B z) cbn beta; intros A B f z nBz.
H: Funext
A: Type
B: ~~ A -> Type
f: forall a : A, ~~ B (not_not_unit a)
z: ~~ A
nBz: ~ B z
Empty
    apply z; intros a.
H: Funext
A: Type
B: ~~ A -> Type
f: forall a : A, ~~ B (not_not_unit a)
z: ~~ A
nBz: ~ B z
a: A
Empty
    exact (f a (transport (fun x => ~ (B x))
                          (path_ishprop _ _)
                          nBz)).
  -
H: Funext
forall (A : Type)
(B : (fun X : Type => ~~ X) A -> Type)
(f : forall a : A,
     (fun X : Type => ~~ X) (B (not_not_unit a)))
(a : A),
((fun (A0 : Type) (B0 : ~~ A0 -> Type)
    (f0 : forall a0 : A0, ~~ B0 (not_not_unit a0))
    (z : ~~ A0) =>
  (fun nBz : ~ B0 z =>
   z
     ((fun a0 : A0 =>
       f0 a0
         (transport (fun x : ~~ A0 => ~ B0 x)
            (path_ishprop z (not_not_unit a0)) nBz))
      :
      ~ A0))
  :
  ~~ B0 z)
 :
 forall (A0 : Type)
 (B0 : (fun X : Type => ~~ X) A0 -> Type),
 (forall a0 : A0,
  (fun X : Type => ~~ X) (B0 (not_not_unit a0))) ->
 forall z : (fun X : Type => ~~ X) A0,
 (fun X : Type => ~~ X) (B0 z)) A B f (not_not_unit a) =
f a cbn beta; intros A B f a.
H: Funext
A: Type
B: ~~ A -> Type
f: forall a : A, ~~ B (not_not_unit a)
a: A
(fun nBz : ~ B (not_not_unit a) =>
 not_not_unit a
   (fun a0 : A =>
    f a0
      (transport (fun x : ~~ A => ~ B x)
         (path_ishprop (not_not_unit a)
            (not_not_unit a0)) nBz))) = f a
    apply path_ishprop.
  -
H: Funext
forall (A : Type) (z z' : (fun X : Type => ~~ X) A),
IsEquiv not_not_unit cbn beta; intros A z z'.
H: Funext
A: Type
z, z': ~~ A
IsEquiv not_not_unit
    refine (isequiv_iff_hprop _ _).
H: Funext
A: Type
z, z': ~~ A
~~ (z = z') -> z = z'
    intros; apply path_ishprop.
Defined.

(** By definition, the local types for this modality are the types such that [not_not_unit : P -> ~~P] is an equivalence.  These are exactly the stable propositions, i.e. those propositions [P] such that [~~P -> P]. *)
Definition inO_notnot `{Funext} (P : Type)
  : In NotNot P <~> (Stable P * IsHProp P)
  := equiv_isequiv_not_not_unit_stable_hprop P.