(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modality.

Local Open Scope path_scope.


(** * The double negation 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
  snrapply 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 intros T x nx; exact (nx x).
  -
H: Funext
forall (A : Type)
(B : (fun X : Type => ~~ X) A -> Type),
(forall a : A,
 (fun X : Type => ~~ X)
   (B
      ((fun (T : Type) (x : T) =>
        (fun nx : ~ T => nx x)
        :
        (fun X : Type => ~~ X) T) A a))) ->
forall z : (fun X : Type => ~~ X) A,
(fun X : Type => ~~ X) (B z) intros A B f z nBz.
H: Funext
A: Type
B: (fun X : Type => ~~ X) A -> Type
f: forall a : A,
(fun X : Type => ~~ X)
  (B
     ((fun (T : Type) (x : T) =>
       (fun nx : ~ T => nx x)
       :
       (fun X : Type => ~~ X) T) A a))
z: (fun X : Type => ~~ X) A
nBz: ~ B z
Empty
    apply z; intros a.
H: Funext
A: Type
B: (fun X : Type => ~~ X) A -> Type
f: forall a : A,
(fun X : Type => ~~ X)
  (B
     ((fun (T : Type) (x : T) =>
       (fun nx : ~ T => nx x)
       :
       (fun X : Type => ~~ X) T) A a))
z: (fun X : Type => ~~ X) 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
          ((fun (T : Type) (x : T) =>
            (fun nx : ~ T => nx x)
            :
            (fun X : Type => ~~ X) T) A a))) (a : A),
(fun (A0 : Type)
   (B0 : (fun X : Type => ~~ X) A0 -> Type)
   (f0 : forall a0 : A0,
         (fun X : Type => ~~ X)
           (B0
              ((fun (T : Type) (x : T) =>
                (fun nx : ~ T => nx x)
                :
                (fun X : Type => ~~ X) T) A0 a0)))
   (z : (fun X : Type => ~~ X) A0) =>
 (fun nBz : ~ B0 z =>
  z
    ((fun a0 : A0 =>
      f0 a0
        (transport (fun x : ~~ A0 => ~ B0 x)
           (path_ishprop z (fun nx : ~ A0 => nx a0))
           nBz))
     :
     ~ A0))
 :
 (fun X : Type => ~~ X) (B0 z)) A B f
  ((fun (T : Type) (x : T) =>
    (fun nx : ~ T => nx x) : (fun X : Type => ~~ X) T)
     A a) = f a intros A B f a.
H: Funext
A: Type
B: (fun X : Type => ~~ X) A -> Type
f: forall a : A,
(fun X : Type => ~~ X)
  (B
     ((fun (T : Type) (x : T) =>
       (fun nx : ~ T => nx x)
       :
       (fun X : Type => ~~ X) T) A a))
a: A
(fun (A : Type) (B : (fun X : Type => ~~ X) A -> Type)
   (f : forall a : A,
        (fun X : Type => ~~ X)
          (B
             ((fun (T : Type) (x : T) =>
               (fun nx : ~ T => nx x)
               :
               (fun X : Type => ~~ X) T) A a)))
   (z : (fun X : Type => ~~ X) A) =>
 (fun nBz : ~ B z =>
  z
    ((fun a : A =>
      f a
        (transport (fun x : ~~ A => ~ B x)
           (path_ishprop z (fun nx : ~ A => nx a)) nBz))
     :
     ~ A))
 :
 (fun X : Type => ~~ X) (B z)) A B f
  ((fun (T : Type) (x : T) =>
    (fun nx : ~ T => nx x) : (fun X : Type => ~~ X) T)
     A a) = f a
    apply path_ishprop.
  -
H: Funext
forall (A : Type) (z z' : (fun X : Type => ~~ X) A),
IsEquiv
  ((fun (T : Type) (x : T) =>
    (fun nx : ~ T => nx x) : (fun X : Type => ~~ X) T)
     (z = z')) intros A z z'.
H: Funext
A: Type
z, z': (fun X : Type => ~~ X) A
IsEquiv
  ((fun (T : Type) (x : T) =>
    (fun nx : ~ T => nx x) : (fun X : Type => ~~ X) T)
     (z = z'))
    refine (isequiv_iff_hprop _ _).
H: Funext
A: Type
z, z': (fun X : Type => ~~ X) A
~~ (z = z') -> z = z'
    intros; apply path_ishprop.
Defined.