module Realisability.PCA where
data Term (A : Type β) (n : Nat) : Type (level-of A) where
var : Fin n β Term A n
const : β―βΊ A β Term A n
app : Term A n β Term A n β Term A n
module eval (_%_ : β― A β β― A β β― A) where
eval : Term A n β Vec (β―βΊ A) n β β― A
eval (var x) Ο = lookup Ο x .fst
eval (const x) Ο = x .fst
eval (app f x) Ο = eval f Ο % eval x Ο
inst : Term A (suc n) β Term A n β Term A n
inst (var x) a with fin-view x
... | zero = a
... | suc i = var i
inst (const a) _ = const a
inst (app f x) a = app (inst f a) (inst x a)
abstract
eval-inst
: (t : Term A (suc n)) (x : β―βΊ A) (Ο : Vec (β―βΊ A) n)
β eval (inst t (const x)) Ο β‘ eval t (x β· Ο)
eval-inst (var i) y Ο with fin-view i
... | zero = refl
... | suc j = refl
eval-inst (const a) y Ο = refl
eval-inst (app f x) y Ο = apβ _%_ (eval-inst f y Ο) (eval-inst x y Ο)
record is-pca (_%_ : β― A β β― A β β― A) : Type (level-of A) where
open eval _%_ public
field
abs : Term A (suc n) β Term A n
absβ : (t : Term A (suc n)) (Ο : Vec (β―βΊ A) n) β β eval (abs t) Ο β
abs-Ξ² : (t : Term A (suc n)) (Ο : Vec (β―βΊ A) n) (a : β―βΊ A)
β eval (abs t) Ο % a .fst β‘ eval (inst t (const a)) Ο
absβ : (k : Nat) β Term A (k + n) β Term A n
absβ zero e = e
absβ (suc k) e = absβ k (abs e)
_%β_ : β {n} β β― A β Vec (β―βΊ A) n β β― A
a %β [] = a
a %β (b β· bs) = (a %β bs) % b .fst
abstract
abs-Ξ²β
: {k n : Nat} {e : Term A (k + n)}
β (Ο : Vec (β―βΊ A) n) (as : Vec (β―βΊ A) k)
β (eval (absβ k e) Ο %β as) β‘ eval e (as ++ Ο)
abs-Ξ²β Ο [] = refl
abs-Ξ²β {e = e} Ο (x β· as) = ap (_% x .fst) (abs-Ξ²β Ο as) β abs-Ξ² _ (as ++ Ο) x β eval-inst e x (as ++ Ο)
record PCA-on (A : Type β) : Type β where
infixl 25 _%_
field
has-is-set : is-set A
_%_ : β― A β β― A β β― A
has-is-pca : is-pca _%_
open is-pca has-is-pca public
PCA : (β : Level) β Type (lsuc β)
PCA β = Ξ£[ X β Set β ] PCA-on β£ X β£
module PCA {β} (A : PCA β) where
open PCA-on (A .snd) public