Last active
October 28, 2023 05:14
-
-
Save mstewartgallus/2d6a281f2c6e34cc982fc5ce502cd1f3 to your computer and use it in GitHub Desktop.
Revisions
-
mstewartgallus revised this gist
Oct 28, 2023 . 1 changed file with 112 additions and 76 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -1,7 +1,24 @@ Set Primitive Projections. Require Import Coq.Unicode.Utf8. Reserved Infix "∈" (at level 90, right associativity). Variant fiber {A B} (f: A → B): B → Type := | fiber_intro x: fiber f (f x). Arguments fiber_intro {A B f}. Notation "x ∈ X" := (fiber X x). Definition witness {A B} {X: A → B} {x} (p: x ∈ X): A := match p with | fiber_intro w => w end. Definition p2 {A B} {X: A → B} {x} (p: x ∈ X): X (witness p) = x := match p with | fiber_intro _ => eq_refl end. Module Span. Record t (A B: Type) := { @@ -25,9 +42,9 @@ Module Span. Definition compose {A B C} (P: t B C) (Q: t A B): t A C := {| s := { x & π1 P x ∈ π2 Q } ; π2 xy := π2 P (projT1 xy) ; π1 xy := π1 Q (witness (projT2 xy)) ; |}. End Span. @@ -40,120 +57,139 @@ Module Data. End Poly. Module μ. Inductive t (P: Poly.t) := | sup (g: Poly.s P) (f: Poly.π P g → t P). Definition tag {P} (x: t P): Poly.s P := match x with | sup _ t _ => t end. Definition field {P} (x: t P): Poly.π P (tag x) → t P := match x with | sup _ _ f => f end. End μ. End Data. Module Category. Class t (Obj: Type) := { Mor: Obj → Obj → Type ; id A: Mor A A ; compose {A B C} (f: Mor B C) (g: Mor A B): Mor A C ; compose_id_l {A B} (f: Mor A B): compose (id _) f = f ; compose_id_r {A B} (f: Mor A B): compose f (id _) = f ; compose_assoc {A B C D} (f: Mor C D) (g: Mor B C) (h: Mor A B): compose f (compose g h) = compose (compose f g) h ; }. Module Import CategoryNotations. Infix "∘" := compose (at level 30). End CategoryNotations. Module Poly. Record t := { data: Data.Poly.t ; Category :> Category.t (Data.Poly.s data) ; map {A B: Data.Poly.s data}: Mor A B → Span.t (Data.Poly.π data A) (Data.Poly.π data B) ; map_id {A} x: Span.π1 (map (id A)) x = Span.π2 (map (id A)) x ; map_compose {A B C} (f: Mor B C) (g: Mor A B): Span.s (Span.compose (map f) (map g)) ; map_compose_π1 {A B C} (f: Mor B C) (g: Mor A B) x: Span.π1 (map (f ∘ g)) x = Span.π1 _ (map_compose f g) ; map_compose_π2 {A B C} (f: Mor B C) (g: Mor A B) x: Span.π2 (map (f ∘ g)) x = Span.π2 _ (map_compose f g) ; }. Arguments map {_ A B}. Arguments map_id {_ _}. Arguments map_compose {_ _ _ _}. Arguments map_compose_π1 {_ _ _ _}. Arguments map_compose_π2 {_ _ _ _}. End Poly. Module μ. Inductive t {P: Poly.t} (A B: Data.μ.t (Poly.data P)) := | sup (g: @Mor _ (Poly.Category P) (Data.μ.tag A) (Data.μ.tag B)) (f: ∀ x, t (Data.μ.field A (Span.π1 (Poly.map g) x)) (Data.μ.field B (Span.π2 (Poly.map g) x))). Arguments sup {P A B}. Definition tag {P} {A B: Data.μ.t (Poly.data P)} (x: t A B): Mor _ _ := match x with | sup g _ => g end. Definition field {P} {A B: Data.μ.t (Poly.data P)} (x: t A B): ∀ y, t (Data.μ.field A (Span.π1 (Poly.map (tag x)) y)) (Data.μ.field B (Span.π2 (Poly.map (tag x)) y)) := match x with | sup _ f => f end. Arguments field {P A B}. Notation "s ▹ x , P" := (sup s (fun x => P)) (at level 100). Fixpoint id {P} (A: Data.μ.t (Poly.data P)) {struct A}: t A A := Category.id _ ▹ x, match Poly.map_id x with | eq_refl => id _ end. Definition compose_π1 {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) (x : Span.s (Poly.map (tag f ∘ tag g))): t (Data.μ.field B (Span.π1 (Poly.map (tag f)) (projT1 (Poly.map_compose (tag f) (tag g))))) (Data.μ.field C (Span.π2 (Poly.map (tag f ∘ tag g)) x)). Proof. rewrite (Poly.map_compose_π2 (tag f) (tag g) x). exact (field f (projT1 (Poly.map_compose (tag f) (tag g)))). Defined. Definition compose_π2 {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) (x : Span.s (Poly.map (tag f ∘ tag g))): t (Data.μ.field A (Span.π1 (Poly.map (tag f ∘ tag g)) x)) (Data.μ.field B (Span.π2 (Poly.map (tag g)) (witness (projT2 (Poly.map_compose (tag f) (tag g)))))). Proof. rewrite (Poly.map_compose_π1 (tag f) (tag g) x). exact (field g (witness (projT2 (Poly.map_compose (tag f) (tag g))))). Defined. Definition compose_π2' {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) (x : Span.s (Poly.map (tag f ∘ tag g))): t (Data.μ.field A (Span.π1 (Poly.map (tag f ∘ tag g)) x)) (Data.μ.field B (Span.π1 (Poly.map (tag f)) (projT1 (Poly.map_compose (tag f) (tag g))))). Proof. assert (g' := compose_π2 f g x). cbn in *. destruct (Poly.map_compose (tag f) (tag g)). cbn in *. destruct f0. exact g'. Defined. Fixpoint compose {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) {struct B}: t A C := tag f ∘ tag g ▹ x, compose (compose_π1 f g x) (compose_π2' f g x). Fixpoint compose_id_l {P A B} {f: @μ.t P A B} {struct B}: μ.compose (μ.id _) f = f. Proof. destruct B, f. cbn in *. Admitted. Lemma compose_id_r {P A B} {f: @μ.t P A B}: μ.compose f (μ.id _) = f. Admitted. Lemma compose_assoc {P A B C D} {f: @μ.t P C D} (g: @μ.t P B C) (h: @μ.t P A B): μ.compose f (μ.compose g h) = μ.compose (μ.compose f g) h. Admitted. End μ. #[export] Instance μ (P: Poly.t): Category.t (Data.μ.t (Poly.data P)) := { Mor := @μ.t P ; id := @μ.id P ; compose := @μ.compose P ; compose_assoc := @μ.compose_assoc P ; -
Oct 26, 2023 . 1 changed file with 32 additions and 22 deletions.There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -73,44 +73,44 @@ Module Category. Span.ext (map (compose f g)) x y → Span.ext (Span.compose (map f) (map g)) x y ; }. Arguments map {_ A B}. Arguments map_id {_ _ _ _}. Arguments map_compose {_ _ _ _} _ _ {x y}. End Poly. Module μ. Inductive t {P: Poly.t} (A B: Data.μ.t (Poly.data P)) := { tag: @Mor _ (Poly.Category P) (Data.μ.tag A) (Data.μ.tag B) ; field {x y}: Span.ext (Poly.map tag) x y → t (Data.μ.field A x) (Data.μ.field B y) ; }. Arguments tag {P A B}. Arguments field {P A B} _ {x y}. Fixpoint id {P} (A: Data.μ.t (Poly.data P)) {struct A}: t A A. Proof. exists (Category.id _). intros x y p. destruct (Poly.map_id p) as [x]. exact (id _ _). Defined. Fixpoint compose {P} {A B C: Data.μ.t (Poly.data P)} (f: t B C) (g: t A B) {struct B}: t A C. Proof. exists (Category.compose (tag f) (tag g)). intros x y p. destruct (Poly.map_compose _ _ p) as [xy]. cbn in *. refine (compose _ _ _ _ (field f (Span.ext_intro _ (fst (proj1_sig xy)))) _). rewrite (proj2_sig xy). exact (field g (Span.ext_intro _ (snd (proj1_sig xy)))). Defined. Module Equiv. Inductive t {P: Poly.t} {A B: Data.μ.t (Poly.data P)} (f g: t A B): Prop := { tag: tag f == tag g ; field {u v} (x: Span.ext (Poly.map (μ.tag f)) u v) (y: Span.ext (Poly.map (μ.tag g)) u v): t (field f x) (field g y) ; }. #[export] @@ -137,17 +137,27 @@ Module Category. End Equiv. #[export] Instance Setoid (P: Poly.t) {A B}: SetoidClass.Setoid (@μ.t P A B) := { }. Lemma compose_id_l {P A B} {f: @μ.t P A B}: μ.compose (μ.id _) f == f. Admitted. Lemma compose_id_r {P A B} {f: @μ.t P A B}: μ.compose f (μ.id _) == f. Admitted. Lemma compose_assoc {P A B C D} {f: @μ.t P C D} (g: @μ.t P B C) (h: @μ.t P A B): μ.compose f (μ.compose g h) == μ.compose (μ.compose f g) h. Admitted. End μ. #[export] Instance μ (P: Poly.t): Category.t (Data.μ.t (Poly.data P)) := { Mor := @μ.t P ; Setoid := @μ.Setoid P ; id := @μ.id P ; compose := @μ.compose P ; compose_assoc := @μ.compose_assoc P ; compose_id_l := @μ.compose_id_l P ; compose_id_r := @μ.compose_id_r P ; }. End Category. -
Oct 26, 2023 .There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode charactersOriginal file line number Diff line number Diff line change @@ -0,0 +1,153 @@ Set Primitive Projections. Require Import Coq.Unicode.Utf8. Require Import Coq.Classes.SetoidClass. Module Span. Record t (A B: Type) := { s: Type ; π1: s → A ; π2: s → B ; }. Arguments s {A B}. Arguments π1 {A B}. Arguments π2 {A B}. Variant ext {A B} (P: t A B): A → B → Type := | ext_intro x: ext P (π1 P x) (π2 P x). Definition id A: t A A := {| s := A ; π1 x := x ; π2 x := x ; |}. Definition compose {A B C} (P: t B C) (Q: t A B): t A C := {| s := { xy | π1 P (fst xy) = π2 Q (snd xy) } ; π1 xy := π1 Q (snd (proj1_sig xy)) ; π2 xy := π2 P (fst (proj1_sig xy)) ; |}. End Span. Module Data. Module Poly. Record t := { s: Type ; π: s → Type ; }. End Poly. Module μ. Inductive t (P: Poly.t) := { tag: Poly.s P ; field {x}: Poly.π P x → t P ; }. Arguments tag {P}. Arguments field {P} t {x}. End μ. End Data. Module Category. Class t (Obj: Type) := { Mor: Obj → Obj → Type ; Setoid A B :> Setoid (Mor A B) ; id A: Mor A A ; compose {A B C} (f: Mor B C) (g: Mor A B): Mor A C ; compose_id_l {A B} (f: Mor A B): compose (id _) f == f ; compose_id_r {A B} (f: Mor A B): compose f (id _) == f ; compose_assoc {A B C D} (f: Mor C D) (g: Mor B C) (h: Mor A B): compose f (compose g h) == compose (compose f g) h ; }. Module Poly. Record t := { data: Data.Poly.t ; Category :> Category.t (Data.Poly.s data) ; map {A B: Data.Poly.s data}: Mor A B → Span.t (Data.Poly.π data A) (Data.Poly.π data B) ; map_id {A x y}: Span.ext (map (id A)) x y → Span.ext (Span.id _) x y ; map_compose {A B C} (f: Mor B C) (g: Mor A B) {x y}: Span.ext (map (compose f g)) x y → Span.ext (Span.compose (map f) (map g)) x y ; }. End Poly. Module μ. Inductive t (P: Poly.t) (A B: Data.μ.t (Poly.data P)) := { tag: @Mor _ (Poly.Category P) (Data.μ.tag A) (Data.μ.tag B) ; field {x y}: Span.ext (Poly.map P tag) x y → t P (Data.μ.field A x) (Data.μ.field B y) ; }. Arguments tag {P A B}. Arguments field {P A B} _ {x y}. Definition id {P} A: t P A A. Proof. exists (Category.id _). intros x y p. destruct (Poly.map_id P p) as [x]. cbn in *. Admitted. Fixpoint compose {P A B C} (f: t P B C) (g: t P A B): t P A C. Proof. exists (Category.compose (tag f) (tag g)). intros x y p. destruct (Poly.map_compose P _ _ p) as [xy]. cbn in *. eapply compose. - cbn in *. assert (f' := field f (Span.ext_intro _ (fst (proj1_sig xy)))). rewrite (proj2_sig xy) in f'. exact f'. - cbn in *. exact (field g (Span.ext_intro _ (snd (proj1_sig xy)))). Defined. Module Equiv. Inductive t (P: Poly.t) {A B} (f g: t P A B): Prop := { tag: tag f == tag g ; field {u v} (x y: Span.ext _ u v): t P (field f x) (field g y) ; }. #[export] Instance Reflexive (P: Poly.t) {A B}: Reflexive (@t P A B). Proof. generalize dependent B. generalize dependent A. refine (fix loop A B e := _). eexists. 1: reflexivity. intros u v x y. Admitted. #[export] Instance Transitive (P: Poly.t) {A B}: Transitive (@t P A B). Admitted. #[export] Instance Symmetric (P: Poly.t) {A B}: Symmetric (@t P A B). Admitted. #[export] Instance Equivalence (P: Poly.t) {A B}: Equivalence (@t P A B) := { }. End Equiv. #[export] Instance Setoid (P: Poly.t) {A B}: SetoidClass.Setoid (μ.t P A B) := { }. End μ. #[export] #[refine] Instance μ (P: Poly.t): Category.t (Data.μ.t (Poly.data P)) := { Mor := μ.t P ; Setoid := @μ.Setoid P ; id := @μ.id P ; compose := @μ.compose P ; }. Admitted. End Category.