Closed.v

(* -*- 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 Topological.
Require Import Colimits.Pushout Homotopy.Join.Core.

Local Open Scope nat_scope.
Local Open Scope path_scope.


(** * Closed modalities *)

(** We begin by characterizing the modal types. *)
Section ClosedModalTypes.
  Context (U : HProp).

  Definition equiv_inO_closed (A : Type)
  : (U -> Contr A) <-> IsEquiv (fun a:A => push (inr a) : Join U A).U: HProp
A: Type
(U -> Contr A) <->
IsEquiv (fun a : A => push (inr a) : Join U A)
  Proof.U: HProp
A: Type
(U -> Contr A) <->
IsEquiv (fun a : A => push (inr a) : Join U A)
    split.U: HProp
A: Type
(U -> Contr A) -> IsEquiv (fun a : A => push (inr a))
U: HProp
A: Type
IsEquiv (fun a : A => push (inr a)) -> U -> Contr A
    -U: HProp
A: Type
(U -> Contr A) -> IsEquiv (fun a : A => push (inr a)) intros uac.U: HProp
A: Type
uac: U -> Contr A
IsEquiv (fun a : A => push (inr a))
      simple refine (isequiv_adjointify _ _ _ _).U: HProp
A: Type
uac: U -> Contr A
Join U A -> A
U: HProp
A: Type
uac: U -> Contr A
(fun a : A => push (inr a)) o ?g == idmap
U: HProp
A: Type
uac: U -> Contr A
?g o (fun a : A => push (inr a)) == idmap
      *U: HProp
A: Type
uac: U -> Contr A
Join U A -> A simple refine (Pushout_rec A _ _ _).U: HProp
A: Type
uac: U -> Contr A
U -> A
U: HProp
A: Type
uac: U -> Contr A
A -> A
U: HProp
A: Type
uac: U -> Contr A
forall a : U * A, ?pushb (fst a) = ?pushc (snd a)
        +U: HProp
A: Type
uac: U -> Contr A
U -> A intros u; pose (uac u); exact (center A).
        +U: HProp
A: Type
uac: U -> Contr A
A -> A intros a; assumption.
        +U: HProp
A: Type
uac: U -> Contr A
forall a : U * A,
(fun u : U => let i := uac u in center A) (fst a) =
idmap (snd a) intros [u a].U: HProp
A: Type
uac: U -> Contr A
u: U
a: A
(let i := uac (fst (u, a)) in center A) = snd (u, a) simpl.U: HProp
A: Type
uac: U -> Contr A
u: U
a: A
center A = a
          pose (uac u).U: HProp
A: Type
uac: U -> Contr A
u: U
a: A
i:= uac u: Contr A
center A = a apply contr.
      *U: HProp
A: Type
uac: U -> Contr A
(fun a : A => push (inr a))
o Pushout_rec A
    (fun u : U => let i := uac u in center A) idmap
    (fun a0 : U * A =>
     (fun (u : U) (a : A) =>
      (let i := uac u in contr a)
      :
      (let i := uac (fst (u, a)) in center A) =
      snd (u, a)) (fst a0) (snd a0)) == idmap intros z.U: HProp
A: Type
uac: U -> Contr A
z: Join U A
push
  (inr
     (Pushout_rec A
        (fun u : U => let i := uac u in center A)
        idmap
        (fun a0 : U * A =>
         let i := uac (fst a0) in contr (snd a0)) z)) =
z pattern z.U: HProp
A: Type
uac: U -> Contr A
z: Join U A
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) z
        simple refine (Pushout_ind _ _ _ _ z).U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall b : U,
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushl b)
U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall c : A,
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushr c)
U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall a : U * A,
transport
  (fun j : Join U A =>
   push
     (inr
        (Pushout_rec A
           (fun u : U => let i := uac u in center A)
           idmap
           (fun a0 : U * A =>
            let i := uac (fst a0) in contr (snd a0)) j)) =
   j) (pglue a) (?pushb (fst a)) = ?pushc (snd a)
        +U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall b : U,
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushl b) intros u.U: HProp
A: Type
uac: U -> Contr A
z: Join U A
u: U
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushl u)
          pose (contr_inhabited_hprop U u).U: HProp
A: Type
uac: U -> Contr A
z: Join U A
u: U
i:= contr_inhabited_hprop U u: Contr U
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushl u)
          apply path_contr.
        +U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall c : A,
(fun j : Join U A =>
 push
   (inr
      (Pushout_rec A
         (fun u : U => let i := uac u in center A)
         idmap
         (fun a0 : U * A =>
          let i := uac (fst a0) in contr (snd a0)) j)) =
 j) (pushr c) intros a; reflexivity.
        +U: HProp
A: Type
uac: U -> Contr A
z: Join U A
forall a : U * A,
transport
  (fun j : Join U A =>
   push
     (inr
        (Pushout_rec A
           (fun u : U => let i := uac u in center A)
           idmap
           (fun a0 : U * A =>
            let i := uac (fst a0) in contr (snd a0)) j)) =
   j) (pglue a)
  ((fun u : U =>
    let i := contr_inhabited_hprop U u in
    path_contr
      (push
         (inr
            (Pushout_rec A
               (fun u0 : U =>
                let i0 := uac u0 in center A) idmap
               (fun a0 : U * A =>
                let i0 := uac (fst a0) in
                contr (snd a0)) (pushl u)))) (pushl u))
     (fst a)) = (fun a0 : A => 1) (snd a) intros [u a]; pose (contr_inhabited_hprop U u).U: HProp
A: Type
uac: U -> Contr A
z: Join U A
u: U
a: A
i:= contr_inhabited_hprop U u: Contr U
transport
  (fun j : Join U A =>
   push
     (inr
        (Pushout_rec A
           (fun u : U => let i := uac u in center A)
           idmap
           (fun a0 : U * A =>
            let i := uac (fst a0) in contr (snd a0)) j)) =
   j) (pglue (u, a))
  (let i := contr_inhabited_hprop U (fst (u, a)) in
   path_contr
     (push
        (inr
           (Pushout_rec A
              (fun u : U =>
               let i0 := uac u in center A) idmap
              (fun a0 : U * A =>
               let i0 := uac (fst a0) in
               contr (snd a0)) (pushl (fst (u, a))))))
     (pushl (fst (u, a)))) = 1
          apply path_contr.
      *U: HProp
A: Type
uac: U -> Contr A
Pushout_rec A
  (fun u : U => let i := uac u in center A) idmap
  (fun a0 : U * A =>
   (fun (u : U) (a : A) =>
    (let i := uac u in contr a)
    :
    (let i := uac (fst (u, a)) in center A) =
    snd (u, a)) (fst a0) (snd a0))
o (fun a : A => push (inr a)) == idmap intros a.U: HProp
A: Type
uac: U -> Contr A
a: A
Pushout_rec A
  (fun u : U => let i := uac u in center A) idmap
  (fun a0 : U * A =>
   let i := uac (fst a0) in contr (snd a0))
  (push (inr a)) = a reflexivity.
    -U: HProp
A: Type
IsEquiv (fun a : A => push (inr a)) -> U -> Contr A intros ? u.U: HProp
A: Type
X: IsEquiv (fun a : A => push (inr a))
u: U
Contr A
      refine (contr_equiv (Join U A) (fun a:A => push (inr a))^-1).U: HProp
A: Type
X: IsEquiv (fun a : A => push (inr a))
u: U
Contr (Join U A)
      pose (contr_inhabited_hprop U u).U: HProp
A: Type
X: IsEquiv (fun a : A => push (inr a))
u: U
i:= contr_inhabited_hprop U u: Contr U
Contr (Join U A)
      exact _.
  Defined.

End ClosedModalTypes.

(** Exercise 7.13(ii): Closed modalities *)
Definition Cl (U : HProp) : Modality.U: HProp
Modality
Proof.U: HProp
Modality
  snrapply Build_Modality.U: HProp
Type -> Type
U: HProp
Funext -> forall T : Type, IsHProp (?In' T)
U: HProp
forall T U0 : Type,
?In' T -> forall f : T -> U0, IsEquiv f -> ?In' U0
U: HProp
Type -> Type
U: HProp
forall T : Type, ?In' (?O_reflector' T)
U: HProp
forall T : Type, T -> ?O_reflector' T
U: HProp
forall (A : Type) (B : ?O_reflector' A -> Type),
(forall oa : ?O_reflector' A, ?In' (B oa)) ->
(forall a : A, B (?to' A a)) ->
forall z : ?O_reflector' A, B z
U: HProp
forall (A : Type) (B : ?O_reflector' A -> Type)
(B_inO : forall oa : ?O_reflector' A, ?In' (B oa))
(f : forall a : A, B (?to' A a)) (a : A),
?O_ind' A B B_inO f (?to' A a) = f a
U: HProp
forall A : Type,
?In' A -> forall z z' : A, ?In' (z = z')
  -U: HProp
Type -> Type intros X; exact (U -> Contr X).
  -U: HProp
Funext ->
forall T : Type,
IsHProp ((fun X : Type => U -> Contr X) T) exact _.
  -U: HProp
forall T U0 : Type,
(fun X : Type => U -> Contr X) T ->
forall f : T -> U0,
IsEquiv f -> (fun X : Type => U -> Contr X) U0 intros T B T_inO f feq.U: HProp
T, B: Type
T_inO: (fun X : Type => U -> Contr X) T
f: T -> B
feq: IsEquiv f
(fun X : Type => U -> Contr X) B
    cbn; intros u; pose (T_inO u).U: HProp
T, B: Type
T_inO: (fun X : Type => U -> Contr X) T
f: T -> B
feq: IsEquiv f
u: U
i:= T_inO u: Contr T
Contr B
    refine (contr_equiv _ f); exact _.
  -U: HProp
Type -> Type intros ; exact (Join U X).
  -U: HProp
forall T : Type,
(fun X : Type => U -> Contr X)
  ((fun H : Type => Join U H) T) intros T u.U: HProp
T: Type
u: U
Contr (Join U T)
    pose (contr_inhabited_hprop _ u).U: HProp
T: Type
u: U
i:= contr_inhabited_hprop U u: Contr U
Contr (Join U T)
    exact _.
  -U: HProp
forall T : Type, T -> (fun H : Type => Join U H) T intros T x.U: HProp
T: Type
x: T
(fun H : Type => Join U H) T
    exact (push (inr x)).
  -U: HProp
forall (A : Type)
(B : (fun H : Type => Join U H) A -> Type),
(forall oa : (fun H : Type => Join U H) A,
 (fun X : Type => U -> Contr X) (B oa)) ->
(forall a : A,
 B ((fun (T : Type) (x : T) => push (inr x)) A a)) ->
forall z : (fun H : Type => Join U H) A, B z intros A B B_inO f z.U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
B z
    srefine (Pushout_ind B _ _ _ z).U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall b : U, B (pushl b)
U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall c : A, B (pushr c)
U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall a : U * A,
transport B (pglue a) (?pushb (fst a)) =
?pushc (snd a)
    +U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall b : U, B (pushl b) intros u; apply center, B_inO, u.
    +U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall c : A, B (pushr c) intros a; apply f.
    +U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
forall a : U * A,
transport B (pglue a)
  ((fun u : U => center (B (pushl u))) (fst a)) =
(fun a0 : A => f a0) (snd a) intros [u a].U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
u: U
a: A
transport B (pglue (u, a))
  (center (B (pushl (fst (u, a))))) = 
f (snd (u, a))
      pose (B_inO (push (inr a)) u).U: HProp
A: Type
B: (fun H : Type => Join U H) A -> Type
B_inO: forall oa : (fun H : Type => Join U H) A,
(fun X : Type => U -> Contr X) (B oa)
f: forall a : A,
B ((fun (T : Type) (x : T) => push (inr x)) A a)
z: (fun H : Type => Join U H) A
u: U
a: A
i:= B_inO (push (inr a)) u: Contr (B (push (inr a)))
transport B (pglue (u, a))
  (center (B (pushl (fst (u, a))))) = 
f (snd (u, a))
      apply path_contr.
  -U: HProp
forall (A : Type)
(B : (fun H : Type => Join U H) A -> Type)
(B_inO : forall oa : (fun H : Type => Join U H) A,
         (fun X : Type => U -> Contr X) (B oa))
(f : forall a : A,
     B ((fun (T : Type) (x : T) => push (inr x)) A a))
(a : A),
(fun (A0 : Type)
   (B0 : (fun H : Type => Join U H) A0 -> Type)
   (B_inO0 : forall
             oa : (fun H : Type => Join U H) A0,
             (fun X : Type => U -> Contr X) (B0 oa))
   (f0 : forall a0 : A0,
         B0
           ((fun (T : Type) (x : T) => push (inr x))
              A0 a0))
   (z : (fun H : Type => Join U H) A0) =>
 Pushout_ind B0 (fun u : U => center (B0 (pushl u)))
   (fun a0 : A0 => f0 a0)
   (fun a0 : U * A0 =>
    (fun (u : U) (a1 : A0) =>
     let i := B_inO0 (push (inr a1)) u in
     path_contr
       (transport B0 (pglue (u, a1))
          (center (B0 (pushl (fst (u, a1))))))
       (f0 (snd (u, a1)))) 
      (fst a0) (snd a0)) z) A B B_inO f
  ((fun (T : Type) (x : T) => push (inr x)) A a) = 
f a intros; reflexivity.
  -U: HProp
forall A : Type,
(fun X : Type => U -> Contr X) A ->
forall z z' : A,
(fun X : Type => U -> Contr X) (z = z') intros A A_inO z z' u.U: HProp
A: Type
A_inO: (fun X : Type => U -> Contr X) A
z, z': A
u: U
Contr (z = z')
    pose (A_inO u).U: HProp
A: Type
A_inO: (fun X : Type => U -> Contr X) A
z, z': A
u: U
i:= A_inO u: Contr A
Contr (z = z')
    apply contr_paths_contr.
Defined.

(** The closed modality is accessible. *)
Global Instance accmodality_closed (U : HProp)
  : IsAccModality (Cl U).U: HProp
IsAccModality (Cl U)
Proof.U: HProp
IsAccModality (Cl U)
  unshelve econstructor.U: HProp
NullGenerators
U: HProp
forall X : Type,
In (Cl U) X <-> IsNull_Internal.IsNull ?acc_ngen X
  -U: HProp
NullGenerators econstructor.U: HProp
?ngen_indices -> Type
    exact (fun _:U => Empty).
  -U: HProp
forall X : Type,
In (Cl U) X <->
IsNull_Internal.IsNull
  {|
    ngen_indices := U; ngen_type := fun _ : U => Empty
  |} X intros X; split.U: HProp
X: Type
In (Cl U) X ->
IsNull_Internal.IsNull
  {|
    ngen_indices := U; ngen_type := fun _ : U => Empty
  |} X
U: HProp
X: Type
IsNull_Internal.IsNull
  {|
    ngen_indices := U; ngen_type := fun _ : U => Empty
  |} X -> In (Cl U) X
    +U: HProp
X: Type
In (Cl U) X ->
IsNull_Internal.IsNull
  {|
    ngen_indices := U; ngen_type := fun _ : U => Empty
  |} X intros X_inO u.U: HProp
X: Type
X_inO: In (Cl U) X
u: lgen_indices
  (null_to_local_generators
     {|
       ngen_indices := U;
       ngen_type := fun _ : U => Empty
     |})
ooExtendableAlong
  (null_to_local_generators
     {|
       ngen_indices := U;
       ngen_type := fun _ : U => Empty
     |} u)
  (fun
     _ : lgen_codomain
           (null_to_local_generators
              {|
                ngen_indices := U;
                ngen_type := fun _ : U => Empty
              |}) u => X)
      pose (X_inO u).U: HProp
X: Type
X_inO: In (Cl U) X
u: lgen_indices
  (null_to_local_generators
     {|
       ngen_indices := U;
       ngen_type := fun _ : U => Empty
     |})
i:= X_inO u: Contr X
ooExtendableAlong
  (null_to_local_generators
     {|
       ngen_indices := U;
       ngen_type := fun _ : U => Empty
     |} u)
  (fun
     _ : lgen_codomain
           (null_to_local_generators
              {|
                ngen_indices := U;
                ngen_type := fun _ : U => Empty
              |}) u => X)
      apply ooextendable_contr; exact _.
    +U: HProp
X: Type
IsNull_Internal.IsNull
  {|
    ngen_indices := U; ngen_type := fun _ : U => Empty
  |} X -> In (Cl U) X intros ext u.U: HProp
X: Type
ext: IsNull_Internal.IsNull
  {|
    ngen_indices := U;
    ngen_type := fun _ : U => Empty
  |} X
u: U
Contr X
      apply (Build_Contr _ ((fst (ext u 1%nat) Empty_rec).1 tt)); intros x.U: HProp
X: Type
ext: IsNull_Internal.IsNull
  {|
    ngen_indices := U;
    ngen_type := fun _ : U => Empty
  |} X
u: U
x: X
(fst (ext u 1) Empty_rec).1 tt = x
      unfold const in ext.U: HProp
X: Type
ext: IsNull_Internal.IsNull
  {|
    ngen_indices := U;
    ngen_type := fun _ : U => Empty
  |} X
u: U
x: X
(fst (ext u 1) Empty_rec).1 tt = x
      exact ((fst (snd (ext u 2) (fst (ext u 1%nat) Empty_rec).1
                       (fun _ => x)) (Empty_ind _)).1 tt).
Defined.

(** In fact, it is topological, and therefore (assuming univalence) lex.  As for topological modalities generally, we don't need to declare these as global instances, but we prove them here as local instances for exposition. *)
Local Instance topological_closed (U : HProp)
  : Topological (Cl U)
  := _.

Global Instance lex_closed `{Univalence} (U : HProp)
  : Lex (Cl U).H: Univalence
U: HProp
Lex (Cl U)
Proof.H: Univalence
U: HProp
Lex (Cl U)
  rapply lex_topological.
Defined.

(** Thus, it also has the following alternative version. *)
Definition Cl' (U : HProp) : Modality
  := Nul (Build_NullGenerators U (fun _ => Empty)).