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 ;
}.
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]
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) := {
}.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment