Require Import HoTT.Basics HoTT.Types.Require Import HoTT.Basics HoTT.Types.
Require Import Extensions.
Require Import Modality Accessible Nullification Lex.

Local Open Scope path_scope.


(** * Open modalities *)

(** ** Definition *)

Definition Op `{Funext} (U : HProp) : Modality.
H: Funext
U: HProp
Modality
Proof.
H: Funext
U: HProp
Modality
  snapply easy_modality.
H: Funext
U: HProp
Type -> Type
H: Funext
U: HProp
forall T : Type, T -> ?O_reflector T
H: Funext
U: HProp
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
U: HProp
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
U: HProp
forall (A : Type) (z z' : ?O_reflector A), IsEquiv (?to (z = z'))
  -
H: Funext
U: HProp
Type -> Type intros X; exact (U -> X).
  -
H: Funext
U: HProp
forall T : Type, T -> (fun X : Type => U -> X) T intros T x; cbn.
H: Funext
U: HProp
T: Type
x: T
U -> T
    exact (fun _ => x).
  -
H: Funext
U: HProp
forall (A : Type) (B : (fun X : Type => U -> X) A -> Type),
(forall a : A,
 (fun X : Type => U -> X)
   (B
      ((fun (T : Type) (x : T) =>
        (fun _ : U => x) : (fun X : Type => U -> X) T) A a))) ->
forall z : (fun X : Type => U -> X) A, (fun X : Type => U -> X) (B z) cbn; intros A B f z u.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a : A, U -> B (fun _ : U => a)
z: U -> A
u: U
B z
    refine (transport B _ (f (z u) u)).
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a : A, U -> B (fun _ : U => a)
z: U -> A
u: U
(fun _ : U => z u) = z
    apply path_arrow; intros u'.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a : A, U -> B (fun _ : U => a)
z: U -> A
u, u': U
z u = z u'
    apply ap; apply path_ishprop.
  -
H: Funext
U: HProp
forall (A : Type) (B : (fun X : Type => U -> X) A -> Type)
(f : forall a : A,
     (fun X : Type => U -> X)
       (B
          ((fun (T : Type) (x : T) =>
            (fun _ : U => x) : (fun X : Type => U -> X) T) A a)))
(a : A),
((fun (A0 : Type) (B0 : (U -> A0) -> Type)
    (f0 : forall a0 : A0, U -> B0 (fun _ : U => a0)) 
    (z : U -> A0) (u : U) =>
  transport B0
    (path_arrow (fun _ : U => z u) z
       ((fun u' : U => ap z (path_ishprop u u')) : (fun _ : U => z u) == z))
    (f0 (z u) u))
 :
 forall (A0 : Type) (B0 : (fun X : Type => U -> X) A0 -> Type),
 (forall a0 : A0,
  (fun X : Type => U -> X)
    (B0
       ((fun (T : Type) (x : T) =>
         (fun _ : U => x) : (fun X : Type => U -> X) T) A0 a0))) ->
 forall z : (fun X : Type => U -> X) A0, (fun X : Type => U -> X) (B0 z)) A B
  f
  ((fun (T : Type) (x : T) => (fun _ : U => x) : (fun X : Type => U -> X) T)
     A a) =
f a cbn; intros A B f a.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
(fun u : U =>
 transport B
   (path_arrow (fun _ : U => a) (fun _ : U => a)
      (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')))
   (f a u)) =
f a
    apply path_arrow; intros u.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
transport B
  (path_arrow (fun _ : U => a) (fun _ : U => a)
     (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')))
  (f a u) =
f a u
    transitivity (transport B 1 (f a u));
      auto with path_hints.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
transport B
  (path_arrow (fun _ : U => a) (fun _ : U => a)
     (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')))
  (f a u) =
transport B 1 (f a u)
    apply (ap (fun p => transport B p (f a u))).
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
path_arrow (fun _ : U => a) (fun _ : U => a)
  (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')) =
1
    transitivity (path_arrow (fun _ => a) (fun _ => a) (@ap10 U _ _ _ 1));
      auto with path_hints.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
path_arrow (fun _ : U => a) (fun _ : U => a)
  (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')) =
path_arrow (fun _ : U => a) (fun _ : U => a) (ap10 1)
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
path_arrow (fun _ : U => a) (fun _ : U => a) (ap10 1) = 1
    *
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
path_arrow (fun _ : U => a) (fun _ : U => a)
  (fun u' : U => ap (fun _ : U => a) (path_ishprop u u')) =
path_arrow (fun _ : U => a) (fun _ : U => a) (ap10 1) apply ap.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
(fun u' : U => ap (fun _ : U => a) (path_ishprop u u')) = ap10 1
      apply path_forall; intros u'.
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u, u': U
ap (fun _ : U => a) (path_ishprop u u') = ap10 1 u'
      apply ap_const.
    *
H: Funext
U: HProp
A: Type
B: (U -> A) -> Type
f: forall a0 : A, U -> B (fun _ : U => a0)
a: A
u: U
path_arrow (fun _ : U => a) (fun _ : U => a) (ap10 1) = 1 apply eta_path_arrow.
  -
H: Funext
U: HProp
forall (A : Type) (z z' : (fun X : Type => U -> X) A),
IsEquiv
  ((fun (T : Type) (x : T) => (fun _ : U => x) : (fun X : Type => U -> X) T)
     (z = z')) intros A z z'.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
IsEquiv
  ((fun (T : Type) (x : T) => (fun _ : U => x) : (fun X : Type => U -> X) T)
     (z = z'))
    srefine (isequiv_adjointify _ _ _ _).
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
(U -> z = z') -> z = z'
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
(fun x : z = z' => (fun _ : U => x) : (fun X : Type => U -> X) (z = z')) o ?g ==
idmap
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
?g o (fun x : z = z' => (fun _ : U => x) : (fun X : Type => U -> X) (z = z')) ==
idmap
    *
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
(U -> z = z') -> z = z' intros f; apply path_arrow; intros u.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
z u = z' u
      exact (ap10 (f u) u).
    *
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
(fun x : z = z' => (fun _ : U => x) : (fun X : Type => U -> X) (z = z'))
o (fun f : U -> z = z' =>
   path_arrow z z' ((fun u : U => ap10 (f u) u) : z == z')) ==
idmap intros f; apply path_arrow; intros u.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
path_arrow z z' (fun u0 : U => ap10 (f u0) u0) = f u
      transitivity (path_arrow z z' (ap10 (f u))).
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
path_arrow z z' (fun u0 : U => ap10 (f u0) u0) = path_arrow z z' (ap10 (f u))
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
path_arrow z z' (ap10 (f u)) = f u
      +
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
path_arrow z z' (fun u0 : U => ap10 (f u0) u0) = path_arrow z z' (ap10 (f u)) unfold to; apply ap.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
(fun u0 : U => ap10 (f u0) u0) = ap10 (f u)
        apply path_forall; intros u'.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u, u': U
ap10 (f u') u' = ap10 (f u) u'
        apply (ap (fun u0 => ap10 (f u0) u')).
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u, u': U
u' = u
        apply path_ishprop.
      +
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
f: U -> z = z'
u: U
path_arrow z z' (ap10 (f u)) = f u apply eta_path_arrow.
    *
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
(fun f : U -> z = z' =>
 path_arrow z z' ((fun u : U => ap10 (f u) u) : z == z'))
o (fun x : z = z' => (fun _ : U => x) : (fun X : Type => U -> X) (z = z')) ==
idmap intros p.
H: Funext
U: HProp
A: Type
z, z': (fun X : Type => U -> X) A
p: z = z'
path_arrow z z' (fun u : U => ap10 p u) = p
      exact (eta_path_arrow _ _ _).
Defined.

(** ** The open modality is lex *)

(** Note that unlike most other cases, we can prove this without univalence (though we do of course need funext). *)
Instance lex_open `{Funext} (U : HProp)
  : Lex (Op U).
H: Funext
U: HProp
Lex (Op U)
Proof.
H: Funext
U: HProp
Lex (Op U)
  apply lex_from_isconnected_paths.
H: Funext
U: HProp
forall A : Type,
IsConnected (Op U) A -> forall x y : A, IsConnected (Op U) (x = y)
  intros A Ac x y.
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
IsConnected (Op U) (x = y)
  napply contr_forall.
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
U -> Contr (x = y)
  intro u.
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
u: U
Contr (x = y)
  pose (contr_inhabited_hprop U u).
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
u: U
i:= contr_inhabited_hprop U u: Contr U
Contr (x = y)
  rapply contr_paths_contr.
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
u: U
i:= contr_inhabited_hprop U u: Contr U
Contr A
  refine (contr_equiv (U -> A) (equiv_contr_forall _)).
H: Funext
U: HProp
A: Type
Ac: IsConnected (Op U) A
x, y: A
u: U
i:= contr_inhabited_hprop U u: Contr U
Contr (U -> A)
  exact Ac.
Defined.

(** ** The open modality is accessible. *)

Instance acc_open `{Funext} (U : HProp)
  : IsAccModality (Op U).
H: Funext
U: HProp
IsAccModality (Op U)
Proof.
H: Funext
U: HProp
IsAccModality (Op U)
  unshelve econstructor.
H: Funext
U: HProp
NullGenerators
H: Funext
U: HProp
forall X : Type, In (Op U) X <-> IsNull_Internal.IsNull ?acc_ngen X
  -
H: Funext
U: HProp
NullGenerators econstructor.
H: Funext
U: HProp
?ngen_indices -> Type
    exact (unit_name U).
  -
H: Funext
U: HProp
forall X : Type,
In (Op U) X <->
IsNull_Internal.IsNull {| ngen_indices := Unit; ngen_type := unit_name U |} X intros X; split.
H: Funext
U: HProp
X: Type
In (Op U) X ->
IsNull_Internal.IsNull {| ngen_indices := Unit; ngen_type := unit_name U |} X
H: Funext
U: HProp
X: Type
IsNull_Internal.IsNull {| ngen_indices := Unit; ngen_type := unit_name U |} X ->
In (Op U) X
    +
H: Funext
U: HProp
X: Type
In (Op U) X ->
IsNull_Internal.IsNull {| ngen_indices := Unit; ngen_type := unit_name U |} X intros X_inO u.
H: Funext
U: HProp
X: Type
X_inO: In (Op U) X
u: lgen_indices
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |})
ooExtendableAlong
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |} u)
  (fun
     _ : lgen_codomain
           (null_to_local_generators
              {| ngen_indices := Unit; ngen_type := unit_name U |})
           u =>
   X)
      apply (equiv_inverse (equiv_ooextendable_isequiv _ _)).
H: Funext
U: HProp
X: Type
X_inO: In (Op U) X
u: lgen_indices
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |})
IsEquiv
  (fun
     g : lgen_codomain
           (null_to_local_generators
              {| ngen_indices := Unit; ngen_type := unit_name U |})
           u ->
         X =>
   g
   oD null_to_local_generators
        {| ngen_indices := Unit; ngen_type := unit_name U |} u)
      refine (cancelR_isequiv (fun x (u:Unit) => x)).
H: Funext
U: HProp
X: Type
X_inO: In (Op U) X
u: lgen_indices
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |})
IsEquiv
  (fun x : X =>
   unit_name x
   oD null_to_local_generators
        {| ngen_indices := Unit; ngen_type := unit_name U |} u)
      exact X_inO.
    +
H: Funext
U: HProp
X: Type
IsNull_Internal.IsNull {| ngen_indices := Unit; ngen_type := unit_name U |} X ->
In (Op U) X intros ext; specialize (ext tt).
H: Funext
U: HProp
X: Type
ext: ooExtendableAlong
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |} tt)
  (fun
     _ : lgen_codomain
           (null_to_local_generators
              {| ngen_indices := Unit; ngen_type := unit_name U |})
           tt =>
   X)
In (Op U) X
      refine (isequiv_compose (fun x => unit_name x)
                              (fun h => h o const_tt U)).
H: Funext
U: HProp
X: Type
ext: ooExtendableAlong
  (null_to_local_generators
     {| ngen_indices := Unit; ngen_type := unit_name U |} tt)
  (fun
     _ : lgen_codomain
           (null_to_local_generators
              {| ngen_indices := Unit; ngen_type := unit_name U |})
           tt =>
   X)
IsEquiv (fun (h : Unit -> X) (x : U) => h (const_tt U x))
      exact (isequiv_ooextendable (fun _ => X) (const_tt U) ext).
Defined.

(** Thus, arguably a better definition of [Op] would be as a nullification modality, as it would not require [Funext] and would have a judgmental computation rule.  However, the above definition is also nice to know, as it doesn't use HITs.  We name the other version [Op']. *)
Definition Op' (U : HProp) : Modality
  := Nul (Build_NullGenerators Unit (fun _ => U)).