Functors in lambda calculus

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)