Last active
November 7, 2024 12:08
-
-
Save Jademaster/5879b524f758b5f069636173de420890 to your computer and use it in GitHub Desktop.
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 characters
| import Data.Vect | |
| -- every kind has objects | |
| Signature : Type | |
| Signature = Nat -> Nat -> Type | |
| data Add : Nat -> Nat -> Nat -> Type where | |
| Zero : Add Z x x | |
| SucLeft : Add x y r -> Add (S x) y (S r) | |
| SucRight : Add x y r -> Add x (S y) (S r) | |
| data Lawvere : Signature -> Nat -> Nat -> Type where | |
| Id : (n : Nat) -> Lawvere f n n | |
| Pure : f m n -> Lawvere f m n | |
| Pair : {m, n, m', n' : Nat} -> Add m m' r -> Add n n' r' -> Lawvere f m n -> Lawvere f m' n' -> Lawvere f r r' | |
| ProjL : Add m n r -> Lawvere f r m | |
| ProjR : Add m n r -> Lawvere f r n | |
| Comp : {m, n, k : Nat} -> Lawvere f m n -> Lawvere f n k -> Lawvere f m k | |
| record Cat where | |
| constructor MkCat | |
| obj : Type | |
| hom : obj -> obj -> Type | |
| comp : {x,y,z : obj} -> hom x y -> hom y z -> hom x z | |
| id : (x : obj) -> hom x x | |
| LawvereCat : Signature -> Cat | |
| LawvereCat f = MkCat Nat (Lawvere f) ?o ?p | |
| One : Cat | |
| One = MkCat Unit (\x,y => Unit) ?h ?j | |
| Prod : Cat -> Cat -> Cat | |
| Prod a b = MkCat | |
| (a.obj, b.obj) | |
| (\x, y => (a.hom (fst x) (fst y),b.hom (snd x) (snd y))) | |
| ?n | |
| ?b | |
| record Functor (s, t : Cat) where | |
| constructor MkFunctor | |
| mapObj : s.obj -> t.obj | |
| mapHom : {x, y : s.obj} -> s.hom x y -> t.hom (mapObj x) (mapObj y) | |
| ProdFunc : Functor s t -> Functor s' t' -> Functor (Prod s s') (Prod t t') | |
| CompFunc : Functor s t -> Functor t r -> Functor s r | |
| IdFunc : Functor s s | |
| record NatTrans (a, b : Functor s t) where | |
| constructor MkNatTrans | |
| Component : (x : s.obj) -> t.hom (a.mapObj x) (b.mapObj x) | |
| record MonCat where | |
| constructor MkMonCat | |
| cat : Cat | |
| tensor : Functor (Prod cat cat) cat | |
| unit : Functor One cat | |
| LawvereMonCat : Signature -> MonCat | |
| LawvereMonCat f = MkMonCat (LawvereCat f) ?v ?w | |
| record MonFunctor (c : MonCat) (d : MonCat) where | |
| constructor MkMonFunctor | |
| functor : Functor c.cat d.cat | |
| strength : NatTrans (CompFunc c.tensor functor) (CompFunc (ProdFunc functor functor) d.tensor) | |
| idstrength : NatTrans (CompFunc c.unit functor) d.unit | |
| 0 SigMorphism : Signature -> Signature -> Type | |
| SigMorphism f g = {0 m, n : Nat} -> f m n -> g m n | |
| LawvereMap : SigMorphism f g -> MonFunctor (LawvereMonCat f) (LawvereMonCat g) | |
| LawvereMap a = MkMonFunctor | |
| (MkFunctor | |
| id | |
| ed) | |
| ?strengths | |
| ?idstrengths | |
| where | |
| ed : Lawvere f x y -> Lawvere g x y | |
| ed (Pure f) = Pure (a f) | |
| ed (Id n) = Id n | |
| ed (Pair r r' f g) = Pair r r' (ed f) (ed g) | |
| ed (Comp f g) = Comp (ed f) (ed g) | |
| ed (ProjL p)= ProjL p | |
| ed (ProjR p) = ProjR p | |
| MonCats : Cat | |
| MonCats = MkCat MonCat MonFunctor ?e ?qw | |
| 0 SigCat : Cat | |
| SigCat = MkCat Signature SigMorphism ?cds ?cfd | |
| FreeLawvere : Functor SigCat MonCats | |
| FreeLawvere = MkFunctor LawvereMonCat ?asddf | |
| -- example 1 | |
| data SigRig : Signature where | |
| Plus : SigRig n 1 | |
| Mul : SigRig n 1 | |
| Zer : SigRig 0 1 | |
| Onee : SigRig 0 1 | |
| data DivSig : Signature where | |
| Plusd : DivSig n 1 | |
| Muld : DivSig n 1 | |
| Zerd : DivSig 0 1 | |
| Oneed : DivSig 0 1 | |
| Inv: DivSig 1 1 | |
| Inc : SigMorphism SigRig DivSig | |
| Inc Plus = Plusd | |
| Inc Mul = Muld | |
| Inc Zer = Zerd | |
| Inc Onee = Oneed | |
| Term : Lawvere SigRig 0 1 | |
| Term = Comp (Pair {m=0,n=1,m'=0,n'=1} Zero (SucLeft Zero) (Pure Onee) (Pure Onee)) (Pure Plus) | |
| TranslatedTerm : Lawvere DivSig 0 1 | |
| TranslatedTerm = (LawvereMap Inc).functor.mapHom Term | |
| -- example 2 | |
| data BinaryMonoid: Signature where | |
| Unit : BinaryMonoid 0 1 | |
| BinaryProd : BinaryMonoid 2 1 | |
| data NonBinaryMonoid: Signature where | |
| NBUnit : NonBinaryMonoid 0 1 | |
| NonBinaryProd : {n : Nat} -> NonBinaryMonoid n 1 | |
| Forget : SigMorphism BinaryMonoid NonBinaryMonoid | |
| Forget Unit = NBUnit | |
| Forget BinaryProd = NonBinaryProd {n=2} | |
| --- models | |
| Sets : Cat | |
| Sets = MkCat Type (\x, y => x -> y) ?compos ?idents | |
| CartSets : MonCat | |
| CartSets = MkMonCat Sets (MkFunctor (\x => ((fst x), (snd x))) ?hgfdssa) ?asdf | |
| record PreModel (f : Signature) where | |
| constructor MkPreModel | |
| set : Type | |
| operation : f m n -> (Fin n -> Fin m -> set) | |
| Model : (f : Signature) -> PreModel f -> MonFunctor (LawvereMonCat f) CartSets | |
| Model f premod = MkMonFunctor | |
| ?w3qert | |
| ?sadfa | |
| ?ytueert | |
| {-- | |
| Free : SigMorphism NonBinaryMonoid BinaryMonoid | |
| Free NBUnit = Unit | |
| -- we proceed by induction | |
| Free (NonBinaryProd {n=1}) = Id 1 | |
| Free (NonBinaryProd {n=2}) = BinaryProd | |
| Free (NonBinaryProd {n}) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment