Library HoTT.Modalities.Nullification

Nullification

Require Import HoTT.Basics HoTT.Types.
Require Import Extensions.
Require Import Modality Accessible.
Require Export Modalities.Localization.

Nullification is a special case of localization

Local Open Scope path_scope.

Nullification is the special case of localization where the codomains of the generating maps are all Unit. In this case, we get a modality and not just a reflective subuniverse.

The hypotheses of this lemma may look slightly odd (why are we bothering to talk about type families dependent over Unit?), but they seem to be the most convenient to make the induction go through.

Definition extendable_over_unit (n : nat)
  (A : Type@{a}) (C : Unit → Type@{i}) (D : ∀ u , C u → Type@{j})
  (ext : ExtendableAlong@{a a i k } n (const_tt A) C)
  (ext' : ∀ (c : ∀ u , C u ),
            ExtendableAlong@{a a j k } n (const_tt A) (fun u ⇒ (D u (c u))))
  : ExtendableAlong_Over@{a a i j k } n (const_tt A) C D ext.
Proof.
  generalize dependent C; simple_induction n n IH;
    intros C D ext ext'; [exact tt | split].
  - intros g g'.
    ∃ ((fst (ext' (fst ext g).1)
                 (fun a ⇒ ((fst ext g).2 a )^ # (g' a ))).1);
      intros a; simpl.
    apply moveR_transport_p.
    exact ((fst (ext' (fst ext g).1)
                (fun a ⇒ ((fst ext g).2 a )^ # (g' a ))).2 a).
  - intros h k h' k'.
    apply IH; intros g.
    exact (snd (ext' k) (fun u ⇒ g u # h' u) k').
Defined.

Definition ooextendable_over_unit@{i j k l m}
  (A : Type@{i}) (C : Unit → Type@{j}) (D : ∀ u , C u → Type@{k})
  (ext : ooExtendableAlong@{l l j m } (const_tt A) C)
  (ext' : ∀ (c : ∀ u , C u ),
            ooExtendableAlong (const_tt A) (fun u ⇒ (D u (c u))))
  : ooExtendableAlong_Over (const_tt A) C D ext
  := fun n ⇒ extendable_over_unit n A C D (ext n) (fun c ⇒ ext' c n).

#[local] Hint Extern 4 ⇒ progress (cbv beta iota) : typeclass_instances.

Definition Nul@{a i} (S : NullGenerators@{a }) : Modality@{i }.
Proof.

We use the localization reflective subuniverses for most of the necessary data.

  simple refine (Build_Modality' (Loc (null_to_local_generators S)) _ _).
  - exact _.
  - intros A.

We take care with universes.

    snrefine (reflectsD_from_OO_ind@{i } _ _ _).
    + intros B B_inO g.
      refine (Localize_ind@{a i i i } (null_to_local_generators S) A B g _); intros i.
      apply ooextendable_over_unit; intros c.
      refine (ooextendable_postcompose@{a a i i i i i i i i }
                (fun (_:Unit) ⇒ B (c tt)) _ _
                (fun u ⇒ transport B (ap@{Set _} c (path_unit tt u))) _).
      refine (ooextendable_islocal _ i).
    + reflexivity.
    + apply inO_paths@{i i }.
Defined.

And here is the "real" definition of the notation IsNull.

Notation IsNull f := (In (Nul f)).

Nullification and Accessibility

Nullification modalities are accessible, essentially by definition.

Global Instance accmodality_nul (S : NullGenerators) : IsAccModality (Nul S).
Proof.
  unshelve econstructor.
  - exact S.
  - intros; reflexivity.
Defined.

And accessible modalities can be lifted to other universes.

Definition lift_accmodality@{a i j} (O : Subuniverse@{i }) `{IsAccModality@{a i } O}
  : Modality@{j }
  := Nul@{a j } (acc_ngen O).

Global Instance O_eq_lift_accmodality (O : Subuniverse@{i }) `{IsAccModality@{a i } O}
  : O <=> lift_accmodality O.
Proof.
  split; intros A; apply inO_iff_isnull.
Defined.