Timings for Notnot.v
(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
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.
intros X; exact (~ (~ X)).
intros T x nx; exact (nx x).
exact (f a (transport (fun x => ~ (B x))
(path_ishprop _ _)
nBz)).
refine (isequiv_iff_hprop _ _).
intros; apply path_ishprop.