Skip to content

Instantly share code, notes, and snippets.

@cheery

cheery/demo..agda

Created January 21, 2023 05:36
Show Gist options
  • Save cheery/9198e3ca26e0f919c167fa710c8f10b7 to your computer and use it in GitHub Desktop.
Save cheery/9198e3ca26e0f919c167fa710c8f10b7 to your computer and use it in GitHub Desktop.
Download ZIP
Functors in lambda calculus
Raw
demo..agda
{-# OPTIONS --type-in-type #-}
module demo where
open import Data.Product
open import Data.Unit
open import Agda.Builtin.Equality
data Unit₁ : Set₁ where
point : Unit₁
data Ty : Set where
unit : Ty
arrow : Ty -> Ty -> Ty
prod : Ty -> Ty -> Ty
cat : Ty
opcat : Ty
data Env : Set where
nil : Env
cons : Ty -> Env -> Env
data FTerm : Env -> Ty -> Set where
var : {t : Ty} -> {e : Env} -> FTerm (cons t e) t
weak : {t u : Ty} -> {e : Env} -> FTerm e t -> FTerm (cons u e) t
app : {a b : Ty} -> {e : Env} -> FTerm e (arrow a b) -> FTerm e a -> FTerm e b
abs : {a b : Ty} -> {e : Env} -> FTerm (cons a e) b -> FTerm e (arrow a b)
pair : {a b : Ty} -> {e : Env} -> FTerm e a -> FTerm e b -> FTerm e (prod a b)
fst : {a b : Ty} -> {e : Env} -> FTerm e (prod a b) -> FTerm e a
snd : {a b : Ty} -> {e : Env} -> FTerm e (prod a b) -> FTerm e b
const : {e : Env} -> (a : Set) -> FTerm e cat
constOp : {e : Env} -> (a : Set) -> FTerm e opcat
prodType : {e : Env} -> FTerm e cat -> FTerm e cat -> FTerm e cat
prodTypeOp : {e : Env} -> FTerm e opcat -> FTerm e opcat -> FTerm e opcat
arrowType : {e : Env} -> FTerm e opcat -> FTerm e cat -> FTerm e cat
arrowTypeOp : {e : Env} -> FTerm e cat -> FTerm e opcat -> FTerm e opcat
record Category : Set₁ where
field
Obj : Set
Map : Obj → Obj → Set
Comp : ∀ {A B C} → (Map B C) → (Map A B) → (Map A C)
Id : ∀ {A} → (Map A A)
open Category
record Functor (a : Category) (b : Category) : Set₁ where
field
ObjF : Obj a → Obj b
MapF : ∀ {A B} → Map a A B → Map b (ObjF A) (ObjF B)
open Functor
unitCategory : Category
Obj unitCategory = ⊤
Map unitCategory tt tt = ⊤
Comp unitCategory tt tt = tt
Id unitCategory = tt
functorCategory : Category → Category → Category
Obj (functorCategory x y) = Functor x y
Map (functorCategory x y) a b = (A : Obj x) → Map y (ObjF a A) (ObjF b A)
Comp (functorCategory x y) g f = λ a → Comp y (g a) (f a)
Id (functorCategory x y) = λ a → Id y
cartesianCategory : Category → Category → Category
Obj (cartesianCategory x y) = Obj x × Obj y
Map (cartesianCategory x y) (a , b) (c , d) = Map x a c × Map y b d
Comp (cartesianCategory x y) (g , g') (f , f') = Comp x g f , Comp y g' f'
Id (cartesianCategory x y) = Id x , Id y
setCategory : Category
Obj setCategory = Set
Map setCategory x y = x -> y
Comp setCategory g f = λ x → g (f x)
Id setCategory = λ x → x
opSetCategory : Category
Obj opSetCategory = Set
Map opSetCategory x y = y -> x
Comp opSetCategory g f = λ x → f (g x)
Id opSetCategory = λ x → x
category : Ty → Category
category unit = unitCategory
category (arrow t v) = functorCategory (category t) (category v)
category (prod t v) = cartesianCategory (category t) (category v)
category cat = setCategory
category opcat = opSetCategory
data ObjSpace : Env → Set₁ where
nilO : ObjSpace nil
consO : {t : Ty} → {e : Env} → Obj (category t) → ObjSpace e → ObjSpace (cons t e)
data MapSpace : Env → Set₁ where
nilM : MapSpace nil
consM : {t : Ty} → {e : Env} → (a b : Obj (category t)) (f : Map (category t) a b) → MapSpace e → MapSpace (cons t e)
left : ∀ {e} → MapSpace e → ObjSpace e
left nilM = nilO
left (consM a b f m) = consO a (left m)
right : ∀ {e} → MapSpace e → ObjSpace e
right nilM = nilO
right (consM a b f m) = consO b (right m)
vectorize : ∀ {e} → ObjSpace e → MapSpace e
vectorize nilO = nilM
vectorize (consO {t} x m) = consM x x (Id (category t)) (vectorize m)
cong : ∀ {A B : Set} (f : A → B) {x y : A}
→ x ≡ y
→ f x ≡ f y
cong f refl = refl
theorem1 : ∀ {e} → (m : ObjSpace e) → left (vectorize m) ≡ m
theorem1 nilO = refl
theorem1 (consO x m) = cong (consO x) (theorem1 m)
theorem2 : ∀ {e} → (m : ObjSpace e) → right (vectorize m) ≡ m
theorem2 nilO = refl
theorem2 (consO x m) = cong (consO x) (theorem2 m)
mutual
obj : {a : Ty} → {e : Env} → FTerm e a → ObjSpace e → Obj (category a)
obj var (consO x space) = x
obj (weak term) (consO x space) = obj term space
obj (app t v) space with obj t space
obj (app t v) space | functor = ObjF functor (obj v space)
ObjF (obj (abs t) space) x = obj t (consO x space)
MapF (obj {arrow a b} (abs t) space) = mapM a b t space
obj (pair t v) space = obj t space , obj v space
obj (fst t) space = proj₁ (obj t space)
obj (snd t) space = proj₂ (obj t space)
obj (prodType t v) space = obj t space × obj v space
obj (prodTypeOp t v) space = obj t space × obj v space
obj (arrowType t v) space = obj t space -> obj v space
obj (arrowTypeOp t v) space = obj t space -> obj v space
obj (const a) space = a
obj (constOp a) space = a
mapM : ∀ a b {e} (t : FTerm (cons a e) b) (space : ObjSpace e) {A B : Obj (category a)} →
Map (category a) A B →
Map (category b) (ObjF (obj (abs t) space) A)
(ObjF (obj (abs t) space) B)
mapM a b t space {A} {B} ab with mapF t (consM A B ab (vectorize space))
mapM a b t space {A} {B} ab | m rewrite theorem1 space rewrite theorem2 space = m
mapF : {a : Ty} → {e : Env} → (t : FTerm e a) → (m : MapSpace e) → Map (category a) (obj t (left m)) (obj t (right m))
mapF var (consM a b f space) = f
mapF (weak term) (consM a b f space) = mapF term space
mapF (app t v) space with mapF t space | mapF v space
mapF {z} (app t v) space | f | g = Comp (category z) (f (obj v (right space))) (MapF (obj t (left space)) g)
mapF {a = arrow a b} (abs t) space x = mapF t (consM x x (Id (category a)) space)
mapF (pair t v) space = mapF t space , mapF v space
mapF (fst t) space = proj₁ (mapF t space)
mapF (snd t) space = proj₂ (mapF t space)
mapF (prodType t v) space with mapF t space | mapF v space
mapF (prodType t v) space | m | w = λ (x , y) → m x , w y
mapF (prodTypeOp t v) space = λ (x , y) → mapF t space x , mapF v space y
mapF (arrowType t v) space = λ f x → (mapF v space) (f (mapF t space x))
mapF (arrowTypeOp t v) space = λ f x → (mapF v space) (f (mapF t space x))
mapF (const a) space = Id setCategory
mapF (constOp a) space = Id opSetCategory
testFunctor : ∀{e} → FTerm e (arrow cat cat)
testFunctor = abs (prodType var var)
testTest : (A B : Set) → (A → B) → A × A → B × B
testTest A B f = mapF (app testFunctor var) (consM A B f nilM)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment