Library HoTT.Modalities.Closed

Require Import HoTT.Basics HoTT.Types.
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).
  Proof.
    split.
    - intros uac.
      simple refine (isequiv_adjointify _ _ _ _).
      × simple refine (Pushout_rec A _ _ _).
        + intros u; pose (uac u); exact (center A).
        + intros a; assumption.
        + intros [u a]. simpl.
          pose (uac u). apply contr.
      × intros z. pattern z.
        simple refine (Pushout_ind _ _ _ _ z).
        + intros u.
          pose (contr_inhabited_hprop U u).
          apply path_contr.
        + intros a; reflexivity.
        + intros [u a]; pose (contr_inhabited_hprop U u).
          apply path_contr.
      × intros a. reflexivity.
    - intros ? u.
      refine (contr_equiv (Join U A) (fun a:A ⇒ push (inr a))^-1).
      pose (contr_inhabited_hprop U u).
      exact _.
  Defined.

End ClosedModalTypes.

Exercise 7.13(ii): Closed modalities

Definition Cl (U : HProp) : Modality.
Proof.
  snapply Build_Modality.
  - intros X; exact (U → Contr X).
  - exact _.
  - intros T B T_inO f feq.
    cbn; intros u; pose (T_inO u).
    exact (contr_equiv _ f).
  - intros ; exact (Join U X).
  - intros T u.
    pose (contr_inhabited_hprop _ u).
    exact _.
  - intros T x.
    exact (push (inr x)).
  - intros A B B_inO f z.
    srefine (Pushout_ind B _ _ _ z).
    + intros u; apply center, B_inO, u.
    + intros a; apply f.
    + intros [u a].
      pose (B_inO (push (inr a)) u).
      apply path_contr.
  - intros; reflexivity.
  - intros A A_inO z z' u.
    pose (A_inO u).
    apply contr_paths_contr.
Defined.

The closed modality is accessible.

Instance accmodality_closed (U : HProp)
  : IsAccModality (Cl U).
Proof.
  unshelve econstructor.
  - econstructor.
    exact (fun _:U ⇒ Empty).
  - intros X; split.
    + intros X_inO u.
      pose (X_inO u).
      apply ooextendable_contr; exact _.
    + intros ext u.
      apply (Build_Contr _ ((fst (ext u 1%nat) Empty_rec ).1 tt)); intros x.
      unfold const in ext.
      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)
  := _.

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

Thus, it also has the following alternative version.

Definition Cl' (U : HProp) : Modality
:= Nul (Build_NullGenerators U (fun _ ⇒ Empty)).