(* -*- 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 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
  snrapply 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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 a : A, U -> B (fun _ : U => a)
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 u : U => ap10 (f u) u) = 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 u : U => ap10 (f u) u) =
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 u : U => ap10 (f u) u) =
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 u : U => ap10 (f u) u) = 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
      refine (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). *)
Global 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)
  nrapply 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. *)

Global 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)
      apply 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 (f := (fun x => unit_name x))
                              (g := (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))
      refine (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)).