vType: strip ongoing work adding degeneracies

theories/νType/νType.v

@@ -581,239 +581,6 @@ CoInductive νTypeFrom n (X: (νTypeAt n).(prefix)): Type@{m'} := cons {
 (** The final construction *)
 Definition νTypes := νTypeFrom 0 tt.
 
-(* Degeneracies *)
-
-Class DgnFrameBlockPrev {n'} (C: νType n'.+1) := {
-  dgnFrame' p {Hp: p.+2 <= n'.+1} {D}:
-    C.(FramePrev).(frame'') p D -> C.(FramePrev).(frame') p D;
-}.
-
-Arguments dgnFrame' {n' C} _ p {Hp D} d.
-
-Class DgnFrameBlock {n'} (C: νType n'.+1) p (Prev: DgnFrameBlockPrev C) := {
-  dgnFrame {Hp: p.+1 <= n'.+1} {D}:
-    C.(FramePrev).(frame') p D -> C.(Frame).(frame p) D;
-  idDgnRestrFrame {ε} {Hp: p.+1 <= n'.+1} {D}
-    {d: C.(FramePrev).(frame') p D}:
-    C.(Frame).(restrFrame) n' ε (dgnFrame d) = d;
-  cohDgnRestrFrame q {ε} {Hpq: p.+2 <= q.+2} {Hq: q.+2 <= n'.+1} {D}
-    {d: C.(FramePrev).(frame') p D}:
-    Prev.(dgnFrame') p (C.(FramePrev).(restrFrame') p q ε d) =
-      C.(Frame).(restrFrame) q ε (dgnFrame d);
-}.
-
-Arguments dgnFrame {n' C p Prev} _ {Hp D} d.
-Arguments idDgnRestrFrame {n' C p Prev} _ {ε Hp D d}.
-Arguments cohDgnRestrFrame {n' C p Prev} _ q {ε Hpq Hq D d}.
-
-Class DgnPaintingBlockPrev {n'} (C: νType n'.+1) (Prev: DgnFrameBlockPrev C) := {
-  dgnPainting' p {Hp: p.+2 <= n'.+1} {D} {d: C.(FramePrev).(frame'') p D}:
-    C.(PaintingPrev).(painting'') d ->
-    C.(PaintingPrev).(painting') (Prev.(dgnFrame') p d);
-}.
-
-Arguments dgnPainting' {n' C Prev} _ p {Hp D d} c.
-
-Class DgnPaintingBlock {n'} (C: νType n'.+1) {Q: DgnFrameBlockPrev C}
-  (Prev: DgnPaintingBlockPrev C Q)
-  (FrameBlock: forall {p}, DgnFrameBlock C p Q) := {
-  dgnPainting p {Hp: p.+1 <= n'.+1} {D E} {d: C.(FramePrev).(frame') p D}:
-    C.(PaintingPrev).(painting') d ->
-    C.(Painting).(painting) E (FrameBlock.(dgnFrame) d);
-  idDgnRestrPainting {p ε} {Hp: p.+1 <= n'.+1} {D E}
-    {d: C.(FramePrev).(frame') p D} {c: C.(PaintingPrev).(painting') d}:
-    rew [C.(PaintingPrev).(painting')] FrameBlock.(idDgnRestrFrame) in
-    C.(Painting).(restrPainting) p n' (ε := ε) (E := E) (dgnPainting p c) = c;
-  cohDgnRestrPainting {p} q {ε} {Hpq: p.+2 <= q.+2} {Hq: q.+2 <= n'.+1} {D E}
-    {d: C.(FramePrev).(frame') p D} {c: C.(PaintingPrev).(painting') d}:
-    rew <- [C.(PaintingPrev).(painting')] FrameBlock.(cohDgnRestrFrame) q in
-    C.(Painting).(restrPainting) p q (ε := ε) (E := E) (dgnPainting p c) =
-    Prev.(dgnPainting') p (C.(PaintingPrev).(restrPainting') _ q ε c);
-}.
-
-Arguments dgnPainting {n' C Q Prev FrameBlock} _ p {Hp D E d} c.
-Arguments idDgnRestrPainting {n' C Q Prev FrameBlock} _ {p ε Hp D E d c}.
-Arguments cohDgnRestrPainting {n' C Q Prev FrameBlock} _ {p} q {ε Hpq Hq D E d c}.
-
-Class DgnLift {n'} (C: νType n'.+1) (DgnFramePrev : DgnFrameBlockPrev C)
-  (DgnFrame : forall {p}, DgnFrameBlock C p DgnFramePrev) := {
-  dgnLift {p} {Hp: p.+1 <= n'.+1} {D E} {d: C.(FramePrev).(frame') n' D}
-    (c: C.(PaintingPrev).(painting') d):
-    let l ε :=
-      rew <- [C.(PaintingPrev).(painting')] DgnFrame.(idDgnRestrFrame) in c in
-     E (rew <- [id] C.(eqFrameSp) in (DgnFrame.(dgnFrame) d; l))
-}.
-
-Class Dgn {n'} (C: νType n'.+1) := {
-  DgnFramePrev: DgnFrameBlockPrev C;
-  DgnFrame {p}: DgnFrameBlock C p DgnFramePrev;
-  DgnPaintingPrev: DgnPaintingBlockPrev C DgnFramePrev;
-  DgnPainting: DgnPaintingBlock C DgnPaintingPrev (@DgnFrame);
-
-  DgnLayer {p} {Hp: p.+2 <= n'.+1} {D} {d: C.(FramePrev).(frame') p D}
-    (l: C.(Layer') d): C.(Layer) (DgnFrame.(dgnFrame) d) :=
-    fun ε => rew [C.(PaintingPrev).(painting')]
-    DgnFrame.(cohDgnRestrFrame) p in DgnPaintingPrev.(dgnPainting') p (l ε);
-  eqDgnFrameSp {p q} {Hpq: p.+2 <= q.+2} {Hq: q.+2 <= n'.+1} {D}
-    {d: C.(FramePrev).(frame') p D} (l: C.(Layer') d):
-    DgnFrame.(dgnFrame) (rew <- [id] C.(eqFrameSp') in (d; l)) =
-    rew <- [id] C.(eqFrameSp) in (DgnFrame.(dgnFrame) d; DgnLayer l);
-}.
-
-Arguments DgnFramePrev {n' C} _.
-Arguments DgnFrame {n' C} _ {p}.
-Arguments DgnPaintingPrev {n' C} _.
-Arguments DgnPainting {n' C} _.
-Arguments DgnLayer {n' C} _ {p Hp D d} l.
-
-#[local]
-Instance mkDgnFramePrev {n'} {C: νType n'.+1} {G: Dgn C}:
-  DgnFrameBlockPrev (mkνTypeSn C) := {|
-  dgnFrame' p Hp (D: (mkνTypeSn C).(prefix)) d := G.(DgnFrame).(dgnFrame) d;
-|}.
-
-Definition mkDgnLayer {n' p} {C: νType n'.+1} {G: Dgn C}
-  {Hp: p.+2 <= n'.+2} {Frame: DgnFrameBlock (mkνTypeSn C) p mkDgnFramePrev}
-  {D} {d: mkFramePrev.(frame') p D} (l: mkLayer' d):
-  mkLayer (Frame.(dgnFrame) d) :=
-  fun ω => rew [C.(Painting).(painting) D.2]
-    Frame.(cohDgnRestrFrame) p in G.(DgnPainting).(dgnPainting) p (l ω).
-
-Definition mkidDgnRestrLayer {n' p ε} {C: νType n'.+1} {G: Dgn C}
-  {Hp: p.+2 <= n'.+2}
-  {FrameBlock: DgnFrameBlock (mkνTypeSn C) p mkDgnFramePrev} {D}
-  {d: mkFramePrev.(frame') p D} {l: mkLayer' d}:
-  rew [mkLayer'] FrameBlock.(idDgnRestrFrame) (ε := ε) in
-    mkRestrLayer p n' (mkDgnLayer l) = l.
-Proof.
-  apply functional_extensionality_dep; intros 𝛉.
-  unfold mkRestrLayer, mkDgnLayer.
-  rewrite <-
-    (G.(DgnPainting).(idDgnRestrPainting) (ε := ε) (E := D.2) (c := l 𝛉)).
-  rewrite <- map_subst_app, <- map_subst.
-  rewrite rew_map with
-    (P := fun x => C.(PaintingPrev).(painting') x),
-  rew_map with
-    (P := fun x => C.(PaintingPrev).(painting') x)
-    (f := fun d => C.(Frame).(restrFrame) n' ε d).
-  repeat rewrite rew_compose.
-  apply rew_swap with
-    (P := fun x => C.(PaintingPrev).(painting') x).
-  rewrite rew_app. now trivial.
-  now apply (C.(FramePrev).(frame') p D.1).(UIP).
-Defined.
-
-Definition mkCohDgnRestrLayer {n' p} q {ε} {C: νType n'.+1} {G: Dgn C}
-  {Hp: p.+3 <= q.+3} {Hq: q.+3 <= n'.+2}
-  {FrameBlock: DgnFrameBlock (mkνTypeSn C) p mkDgnFramePrev} {D}
-  {d: mkFramePrev.(frame') p D} {l: mkLayer' (C := C) d}:
-    rew [mkLayer'] FrameBlock.(cohDgnRestrFrame) q.+1 in
-     G.(DgnLayer) (C.(RestrLayer) p q ε l) = mkRestrLayer p q (mkDgnLayer l).
-Proof.
-  apply functional_extensionality_dep; intros 𝛉.
-  unfold RestrLayer, mkRestrLayer, DgnLayer, mkDgnLayer.
-  rewrite <- map_subst_app, <- !map_subst.
-  rewrite rew_map with
-    (P := fun x => C.(PaintingPrev).(painting') x),
-  rew_map with
-    (P := fun x => C.(PaintingPrev).(painting') x)
-    (f := fun d => C.(Frame).(restrFrame) q ε d),
-  rew_map with
-    (P := fun x => C.(PaintingPrev).(painting') x)
-    (f := fun x => G.(DgnFramePrev).(dgnFrame') p x).
-  rewrite <- (G.(DgnPainting).(cohDgnRestrPainting) q (E := D.2)).
-  repeat rewrite rew_compose.
-  apply rew_swap with
-    (P := fun x => C.(PaintingPrev).(painting') x).
-  rewrite rew_app. now trivial.
-  now apply (C.(FramePrev).(frame') p D.1).(UIP).
-Defined.
-
-#[local]
-Instance mkDgnFrame0 {n'} {C: νType n'.+1} {G: Dgn C}:
-  DgnFrameBlock (mkνTypeSn C) O mkDgnFramePrev.
-  unshelve esplit.
-  * intros; now exact tt.
-  * intros; apply rew_swap with (P := id); now destruct (rew <- _ in _).
-  * intros; apply rew_swap with (P := id); now destruct (rew _ in _).
-Defined.
-
-#[local]
-Instance mkDgnFrameSp {n' p} {C: νType n'.+1} {G: Dgn C}
-  {Frame: DgnFrameBlock (mkνTypeSn C) p mkDgnFramePrev}:
-  DgnFrameBlock (mkνTypeSn C) p.+1 mkDgnFramePrev.
-  unshelve esplit.
-  * (* dgnFrame *)
-    intros Hp D d'.
-    destruct (rew [id] (mkνTypeSn C).(eqFrameSp') in d') as (d, l); clear d'.
-    now exact (Frame.(dgnFrame) d; mkDgnLayer l).
-  * (* idDgnRestrFrame *)
-    simpl; intros ε Hp D d'.
-    rewrite <- rew_opp_l with (P := id) (H := C.(eqFrameSp)).
-    destruct (rew [id] _ in d') as (d, l); clear d'.
-    f_equal.
-    now exact (= Frame.(idDgnRestrFrame); mkidDgnRestrLayer).
-  * (* cohDgnRestrFrame *)
-    intros q ε Hpq Hq D d'; simpl. invert_le Hpq. invert_le Hq.
-    rewrite <- rew_opp_l with (P := id) (H := C.(eqFrameSp)) (a := d').
-    rewrite rew_opp_r.
-    destruct (rew [id] _ in d') as (d, l); clear d'.
-    rewrite C.(eqRestrFrameSp), G.(eqDgnFrameSp).
-    f_equal.
-    now exact (= Frame.(cohDgnRestrFrame) q.+1; mkCohDgnRestrLayer q).
-Defined.
-
-#[local]
-Instance mkDgnFrame {n' p} {C: νType n'.+1} {G: Dgn C}:
-  DgnFrameBlock (mkνTypeSn C) p mkDgnFramePrev.
-  induction p.
-  * now exact mkDgnFrame0.
-  * now exact mkDgnFrameSp.
-Defined.
-
-#[local]
-Instance mkDgnPaintingPrev {n'} {C: νType n'.+1} {G: Dgn C}:
-  DgnPaintingBlockPrev (mkνTypeSn C) mkDgnFramePrev := {|
-  dgnPainting' p Hp (D: (mkνTypeSn C).(prefix)) d c := G.(DgnPainting).(dgnPainting) p c;
-|}.
-
-Definition mkDgnPaintingType {n' p} {C: νType n'.+1} {G: Dgn C}
-  (L: DgnLift (mkνTypeSn C) mkDgnFramePrev (fun p => mkDgnFrame))
-  {Hp: p.+1 <= n'.+2} {D E} {d: mkFramePrev.(frame') p D}
-  (c: mkPaintingPrev.(painting') d): mkPaintingType E (mkDgnFrame.(dgnFrame) d).
-Proof.
-  revert d c; apply le_induction' with (Hp := Hp); clear p Hp.
-  * intros d c. rewrite mkpainting_computes. unshelve esplit.
-    - now exact (fun ε : arity => rew <- [(mkPaintingPrev.(painting'))]
-      (mkDgnFrame).(idDgnRestrFrame) (ε := ε) in c).
-    - unfold mkPaintingType.
-      rewrite le_induction_base_computes. (* TODO: make a "painting"-level lemma *)
-      now exact (L.(dgnLift) (E := E) c).
-  * intros * mkDgnPaintingS * c.
-    destruct (rew [id] C.(eqPaintingSp) in c) as (l, c').
-    specialize (mkDgnPaintingS (rew <- [id] C.(eqFrameSp) in (d; l)) c').
-    simpl in mkDgnPaintingS; rewrite rew_rew' in mkDgnPaintingS.
-    rewrite mkpainting_computes.
-    unshelve esplit.
-    - now exact (mkDgnLayer l).
-    - now apply mkDgnPaintingS.
-Defined.
-
-Instance mkDgnPaintingBlock {n'} {C: νType n'.+1} {G: Dgn C}
-  (L: DgnLift (mkνTypeSn C) mkDgnFramePrev (fun p => mkDgnFrame)):
-  DgnPaintingBlock (mkνTypeSn C)  mkDgnPaintingPrev (fun p => mkDgnFrame).
-  unshelve esplit.
-  - intros. apply mkDgnPaintingType.
-    * now exact L.
-    * now exact X.
-  - intros. revert d c. pattern p, Hp; apply le_induction'; clear p Hp.
-    * intros d c. simpl (mkνTypeSn C).(Painting).(restrPainting).
-      unfold mkRestrPainting; rewrite le_induction'_base_computes.
-      unfold mkDgnPaintingType; rewrite le_induction'_base_computes.
-      now repeat rewrite rew_rew'.
-    * intros p Hp IHP d c. simpl.
-Admitted.
-
 End νType.
 
 Definition AugmentedSemiSimplicial := νTypes hunit.