From 42076a890a7fa6b79cca566ce8b4368e72d69e85 Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Sat, 12 Oct 2024 12:07:22 +0100 Subject: [PATCH] vType: strip ongoing work adding degeneracies --- "theories/\316\275Type/\316\275Type.v" | 233 ------------------------- 1 file changed, 233 deletions(-) diff --git "a/theories/\316\275Type/\316\275Type.v" "b/theories/\316\275Type/\316\275Type.v" index 25bbb7d..fd5dca1 100644 --- "a/theories/\316\275Type/\316\275Type.v" +++ "b/theories/\316\275Type/\316\275Type.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.