Skip to content

Instantly share code, notes, and snippets.

@mstewartgallus

mstewartgallus/fixed.v

Last active October 28, 2023 05:14
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mstewartgallus/2d6a281f2c6e34cc982fc5ce502cd1f3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mstewartgallus/2d6a281f2c6e34cc982fc5ce502cd1f3 to your computer and use it in GitHub Desktop.
Download ZIP
the fixed point of a lax double endofunctor on Span ought to be a category. I can't figure it out though as I get trapped in setoid hell and stuff.
Raw
fixed.v
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment