(** * Nullification *)

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.
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 : forall u, C u -> Type@{j})
  (ext : ExtendableAlong@{a a i k} n (const_tt A) C)
  (ext' : forall (c : forall 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.
n: nat
A: Type
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n (const_tt A)
  (fun u : Unit => D u (c u))
ExtendableAlong_Over n (const_tt A) C D ext
Proof.
n: nat
A: Type
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n (const_tt A)
  (fun u : Unit => D u (c u))
ExtendableAlong_Over n (const_tt A) C D ext
  generalize dependent C; simple_induction n n IH;
    intros C D ext ext'; [exact tt | split].
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
forall (g : forall a : A, C (const_tt A a))
(g' : forall a : A, D (const_tt A a) (g a)),
{rec : forall b : Unit, D b ((fst ext g).1 b) &
forall a : A,
transport (D (const_tt A a)) ((fst ext g).2 a)
  (rec (const_tt A a)) = g' a}
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
forall (h k : forall b : Unit, C b)
(h' : forall b : Unit, D b (h b))
(k' : forall b : Unit, D b (k b)),
ExtendableAlong_Over n (const_tt A)
  (fun b : Unit => h b = k b)
  (fun (b : Unit) (c : h b = k b) =>
   transport (D b) c (h' b) = k' b) 
  (snd ext h k)
  -
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
forall (g : forall a : A, C (const_tt A a))
(g' : forall a : A, D (const_tt A a) (g a)),
{rec : forall b : Unit, D b ((fst ext g).1 b) &
forall a : A,
transport (D (const_tt A a)) ((fst ext g).2 a)
  (rec (const_tt A a)) = g' a} intros g g'.
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
g: forall a : A, C (const_tt A a)
g': forall a : A, D (const_tt A a) (g a)
{rec : forall b : Unit, D b ((fst ext g).1 b) &
forall a : A,
transport (D (const_tt A a)) ((fst ext g).2 a)
  (rec (const_tt A a)) = g' a}
    exists ((fst (ext' (fst ext g).1)
                 (fun a => ((fst ext g).2 a)^ # (g' a))).1);
      intros a; simpl.
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
g: forall a : A, C (const_tt A a)
g': forall a : A, D (const_tt A a) (g a)
a: A
transport (D (const_tt A a)) ((fst ext g).2 a)
  ((fst (ext' (fst ext g).1)
      (fun a : A =>
       transport (D (const_tt A a)) ((fst ext g).2 a)^
         (g' a))).1 (const_tt A a)) = g' a
    apply moveR_transport_p.
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
g: forall a : A, C (const_tt A a)
g': forall a : A, D (const_tt A a) (g a)
a: A
(fst (ext' (fst ext g).1)
   (fun a : A =>
    transport (D (const_tt A a)) ((fst ext g).2 a)^
      (g' a))).1 (const_tt A a) =
transport (D (const_tt A a)) ((fst ext g).2 a)^ (g' a)
    exact ((fst (ext' (fst ext g).1)
                (fun a => ((fst ext g).2 a)^ # (g' a))).2 a).
  -
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
forall (h k : forall b : Unit, C b)
(h' : forall b : Unit, D b (h b))
(k' : forall b : Unit, D b (k b)),
ExtendableAlong_Over n (const_tt A)
  (fun b : Unit => h b = k b)
  (fun (b : Unit) (c : h b = k b) =>
   transport (D b) c (h' b) = k' b) (snd ext h k) intros h k h' k'.
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
h, k: forall b : Unit, C b
h': forall b : Unit, D b (h b)
k': forall b : Unit, D b (k b)
ExtendableAlong_Over n (const_tt A)
  (fun b : Unit => h b = k b)
  (fun (b : Unit) (c : h b = k b) =>
   transport (D b) c (h' b) = k' b) (snd ext h k)
    apply IH; intros g.
A: Type
n: nat
IH: forall (C : Unit -> Type)
(D : forall u : Unit, C u -> Type)
(ext : ExtendableAlong n (const_tt A) C),
(forall c : forall u : Unit, C u,
 ExtendableAlong n (const_tt A)
   (fun u : Unit => D u (c u))) ->
ExtendableAlong_Over n (const_tt A) C D ext
C: Unit -> Type
D: forall u : Unit, C u -> Type
ext: ExtendableAlong n.+1 (const_tt A) C
ext': forall c : forall u : Unit, C u,
ExtendableAlong n.+1 (const_tt A)
  (fun u : Unit => D u (c u))
h, k: forall b : Unit, C b
h': forall b : Unit, D b (h b)
k': forall b : Unit, D b (k b)
g: forall u : Unit, h u = k u
ExtendableAlong n (const_tt A)
  (fun u : Unit => transport (D u) (g u) (h' u) = k' u)
    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 : forall u, C u -> Type@{k})
  (ext : ooExtendableAlong@{l l j m} (const_tt A) C)
  (ext' : forall (c : forall 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}.
S: NullGenerators
Modality
Proof.
S: NullGenerators
Modality
  (** We use the localization reflective subuniverses for most of the necessary data. *)
  simple refine (Build_Modality' (Loc (null_to_local_generators S)) _ _).
S: NullGenerators
forall T : Type,
PreReflects (Loc (null_to_local_generators S)) T
S: NullGenerators
forall T : Type,
ReflectsD (Loc (null_to_local_generators S))
  (Loc (null_to_local_generators S)) T
  -
S: NullGenerators
forall T : Type,
PreReflects (Loc (null_to_local_generators S)) T exact _.
  -
S: NullGenerators
forall T : Type,
ReflectsD (Loc (null_to_local_generators S))
  (Loc (null_to_local_generators S)) T intros A.
S: NullGenerators
A: Type
ReflectsD (Loc (null_to_local_generators S))
  (Loc (null_to_local_generators S)) A
    (** We take care with universes. *)
    snrefine (reflectsD_from_OO_ind@{i} _ _ _).
S: NullGenerators
A: Type
forall
B : O_reflector (Loc (null_to_local_generators S)) A ->
    Type,
(forall
 oa : O_reflector (Loc (null_to_local_generators S)) A,
 In (Loc (null_to_local_generators S)) (B oa)) ->
(forall a : A,
 B (to (Loc (null_to_local_generators S)) A a)) ->
forall
oa : O_reflector (Loc (null_to_local_generators S)) A,
B oa
S: NullGenerators
A: Type
forall
(B : O_reflector (Loc (null_to_local_generators S)) A ->
     Type)
(B_inO : forall
         oa : O_reflector
                (Loc (null_to_local_generators S)) A,
         In (Loc (null_to_local_generators S)) (B oa))
(f : forall a : A,
     B (to (Loc (null_to_local_generators S)) A a))
(a : A),
?OO_ind' B B_inO f
  (to (Loc (null_to_local_generators S)) A a) = f a
S: NullGenerators
A: Type
forall B : Type,
In (Loc (null_to_local_generators S)) B ->
forall z z' : B,
In (Loc (null_to_local_generators S)) (z = z')
    +
S: NullGenerators
A: Type
forall
B : O_reflector (Loc (null_to_local_generators S)) A ->
    Type,
(forall
 oa : O_reflector (Loc (null_to_local_generators S)) A,
 In (Loc (null_to_local_generators S)) (B oa)) ->
(forall a : A,
 B (to (Loc (null_to_local_generators S)) A a)) ->
forall
oa : O_reflector (Loc (null_to_local_generators S)) A,
B oa intros B B_inO g.
S: NullGenerators
A: Type
B: O_reflector (Loc (null_to_local_generators S)) A ->
Type
B_inO: forall
oa : O_reflector
       (Loc (null_to_local_generators S)) A,
In (Loc (null_to_local_generators S)) (B oa)
g: forall a : A,
B (to (Loc (null_to_local_generators S)) A a)
forall
oa : O_reflector (Loc (null_to_local_generators S)) A,
B oa
      refine (Localize_ind@{a i i i} (null_to_local_generators S) A B g _); intros i.
S: NullGenerators
A: Type
B: O_reflector (Loc (null_to_local_generators S)) A ->
Type
B_inO: forall
oa : O_reflector
       (Loc (null_to_local_generators S)) A,
In (Loc (null_to_local_generators S)) (B oa)
g: forall a : A,
B (to (Loc (null_to_local_generators S)) A a)
i: lgen_indices (null_to_local_generators S)
ooExtendableAlong_Over (null_to_local_generators S i)
  (fun
     _ : lgen_codomain (null_to_local_generators S) i
   => Localize (null_to_local_generators S) A)
  (fun
     _ : lgen_codomain (null_to_local_generators S) i
   => B)
  (islocal_localize (null_to_local_generators S) A i)
      apply ooextendable_over_unit; intros c.
S: NullGenerators
A: Type
B: O_reflector (Loc (null_to_local_generators S)) A ->
Type
B_inO: forall
oa : O_reflector
       (Loc (null_to_local_generators S)) A,
In (Loc (null_to_local_generators S)) (B oa)
g: forall a : A,
B (to (Loc (null_to_local_generators S)) A a)
i: lgen_indices (null_to_local_generators S)
c: Unit -> Localize (null_to_local_generators S) A
ooExtendableAlong
  (const_tt
     (lgen_domain (null_to_local_generators S) i))
  (fun u : Unit => B (c u))
      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))) _).
S: NullGenerators
A: Type
B: O_reflector (Loc (null_to_local_generators S)) A ->
Type
B_inO: forall
oa : O_reflector
       (Loc (null_to_local_generators S)) A,
In (Loc (null_to_local_generators S)) (B oa)
g: forall a : A,
B (to (Loc (null_to_local_generators S)) A a)
i: lgen_indices (null_to_local_generators S)
c: Unit -> Localize (null_to_local_generators S) A
ooExtendableAlong
  (const_tt
     (lgen_domain (null_to_local_generators S) i))
  (unit_name (B (c tt)))
      exact (ooextendable_islocal _ i).
    +
S: NullGenerators
A: Type
forall
(B : O_reflector (Loc (null_to_local_generators S)) A ->
     Type)
(B_inO : forall
         oa : O_reflector
                (Loc (null_to_local_generators S)) A,
         In (Loc (null_to_local_generators S)) (B oa))
(f : forall a : A,
     B (to (Loc (null_to_local_generators S)) A a))
(a : A),
(fun
   (B0 : O_reflector
           (Loc (null_to_local_generators S)) A ->
         Type)
   (B_inO0 : forall
             oa : O_reflector
                    (Loc (null_to_local_generators S))
                    A,
             In (Loc (null_to_local_generators S))
               (B0 oa))
   (g : forall a0 : A,
        B0
          (to (Loc (null_to_local_generators S)) A a0))
 =>
 Localize_ind (null_to_local_generators S) A B0 g
   (fun i : lgen_indices (null_to_local_generators S)
    =>
    ooextendable_over_unit
      (lgen_domain (null_to_local_generators S) i)
      (fun
         _ : lgen_codomain
               (null_to_local_generators S) i =>
       Localize (null_to_local_generators S) A)
      (fun
         _ : lgen_codomain
               (null_to_local_generators S) i => B0)
      (islocal_localize (null_to_local_generators S) A
         i)
      (fun
         c : Unit ->
             Localize (null_to_local_generators S) A
       =>
       ooextendable_postcompose
         (unit_name (B0 (c tt)))
         (fun u : Unit => B0 (c u))
         (const_tt
            (lgen_domain (null_to_local_generators S)
               i))
         (fun u : Unit =>
          transport B0 (ap c (path_unit tt u)))
         (ooextendable_islocal
            (null_to_local_generators S) i)))) B B_inO
  f (to (Loc (null_to_local_generators S)) A a) = 
f a reflexivity.
    +
S: NullGenerators
A: Type
forall B : Type,
In (Loc (null_to_local_generators S)) B ->
forall z z' : B,
In (Loc (null_to_local_generators S)) (z = z') 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. *)
Instance accmodality_nul (S : NullGenerators) : IsAccModality (Nul S).
S: NullGenerators
IsAccModality (Nul S)
Proof.
S: NullGenerators
IsAccModality (Nul S)
  unshelve econstructor.
S: NullGenerators
NullGenerators
S: NullGenerators
forall X : Type,
In (Nul S) X <-> IsNull_Internal.IsNull ?acc_ngen X
  -
S: NullGenerators
NullGenerators exact S.
  -
S: NullGenerators
forall X : Type,
In (Nul S) X <-> IsNull_Internal.IsNull S X 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).

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