Skip to content

Instantly share code, notes, and snippets.

@cheery
Last active February 28, 2024 10:43
Show Gist options
  • Save cheery/701902227be3ab5cf583ebfbd0479636 to your computer and use it in GitHub Desktop.
Save cheery/701902227be3ab5cf583ebfbd0479636 to your computer and use it in GitHub Desktop.
chu spaces
{-# OPTIONS --guardedness #-}
module demo where
open import Data.Product
open import Data.Empty
open import Agda.Builtin.Equality
open import Agda.Primitive
sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : ∀ {a} {A : Set a} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq
data Either (A : Set) (B : Set) : Set where
inj₁ : A -> Either A B
inj₂ : B -> Either A B
data Unit : Set where
point : Unit
variable K : Set
data Chu : Set -> Set₁ where
chu : (a : Set) -> (x : Set) -> (a -> x -> K) -> Chu K
pos : Chu K -> Set
pos (chu a x t) = a
neg : Chu K -> Set
neg (chu a x t) = x
rel : (c : Chu K) -> pos c -> neg c -> K
rel (chu a x t) = t
op : Chu K -> Chu K
op (chu a x t) = chu x a (λ x -> λ y -> t y x)
data ChuMap : Chu K -> Chu K -> Set₁ where
chumap : {a b : Chu K}
-> (f : pos a -> pos b)
-> (g : neg b -> neg a)
-> ((x : pos a) -> (y : neg b) -> rel b (f x) y ≡ rel a x (g y))
-> ChuMap a b
opfn : {a b : Chu K} -> ChuMap a b -> ChuMap (op b) (op a)
opfn {a = chu x y t} {b = chu z w u} (chumap f g h) = chumap g f (λ r r' -> sym (h r' r))
unit : Chu K
unit {K} = chu Unit K (λ _ -> λ k -> k)
counit : Chu K
counit = op unit
addunit : Chu K
addunit = chu Unit ⊥ (λ _ -> λ x -> ⊥-elim x)
wthunit : Chu K
wthunit = op addunit
mul : Chu K -> Chu K -> Chu K
mul a b = chu ((pos a) × (pos b))
(Σ ((pos a -> neg b) × (pos b -> neg a))
λ fg -> ((x : pos a) -> (y : pos b) -> rel a x (proj₂ fg y) ≡ rel b y (proj₁ fg x)))
(λ ab -> λ fg -> rel a (proj₁ ab) (proj₂ (proj₁ fg) (proj₂ ab)))
mulFunctor : {a b c d : Chu K} -> ChuMap a b -> ChuMap c d -> ChuMap (mul a c) (mul b d)
mulFunctor (chumap f g fg) (chumap h k hk) = chumap (λ (pa , pc) -> f pa , h pc) (λ pbd -> ((λ pa -> k (proj₁ (proj₁ pbd) (f pa))) , λ pc -> g (proj₂ (proj₁ pbd) (h pc))) , λ x y -> trans (sym (fg x (proj₂ (proj₁ pbd) (h y)))) (trans (proj₂ pbd (f x) (h y)) (hk y (proj₁ (proj₁ pbd) (f x))))) λ { (x , y) (z , w) → fg x (proj₂ z (h y))}
par : Chu K -> Chu K -> Chu K
par a b = op (mul (op a) (op b))
parFunctor : {a b c d : Chu K} -> ChuMap a b -> ChuMap c d -> ChuMap (par a c) (par b d)
parFunctor f g = opfn (mulFunctor (opfn f) (opfn g))
add : Chu K -> Chu K -> Chu K
add a b = chu (Either (pos a) (pos b))
(neg a × neg b)
(λ { (inj₁ x) pq -> rel a x (proj₁ pq) ;
(inj₂ y) pq -> rel b y (proj₂ pq) })
addFunctor : {a b c d : Chu K} -> ChuMap a b -> ChuMap c d -> ChuMap (add a c) (add b d)
addFunctor (chumap f g fg) (chumap h k hk) = chumap (λ { (inj₁ pa) → inj₁ (f pa) ; (inj₂ pc) → inj₂ (h pc)}) (λ (pb , pd) -> g pb , k pd) λ { (inj₁ x) y → fg x (proj₁ y) ; (inj₂ x) y → hk x (proj₂ y)}
wth : Chu K -> Chu K -> Chu K
wth a b = op (add (op a) (op b))
wthFunctor : {a b c d : Chu K} -> ChuMap a b -> ChuMap c d -> ChuMap (wth a c) (wth b d)
wthFunctor f g = opfn (addFunctor (opfn f) (opfn g))
exp : Chu K -> Chu K
exp {K} a = chu (pos a) (pos a -> K) (λ pa pk -> pk pa)
ptIsPoint : ∀ {K} {pt} {f} →
rel {K} (exp unit) pt f ≡ rel {K} unit pt (f point)
ptIsPoint {K} {point} {f} = refl
init : {K} -> ChuMap {K} unit (exp unit)
init {K} = chumap (λ u -> u) (λ f -> f point) λ pt f -> ptIsPoint {K} {pt} {f}
lift : {a b : Chu K} -> ChuMap a b -> ChuMap (exp a) (exp b)
lift (chumap f g h) = chumap f (λ q pa -> q (f pa)) (λ _ _ -> refl)
dup : {a : Chu K} -> ChuMap (exp a) (mul (exp a) (exp a))
dup {K} {a} = chumap (λ x -> x , x) (λ ((f , g) , h) pa -> f pa pa) λ x ((f , g) , h) -> h x x
drop : {a : Chu K} -> ChuMap (exp a) unit
drop {K} {a} = chumap (λ x -> point) (λ k pa -> k) (λ x y -> refl)
inst : {a : Chu K} -> ChuMap (exp a) a
inst {K} {a} = chumap (λ a -> a) (λ x y -> rel a y x) (λ x y -> refl)
ax : {a : Chu K} -> ChuMap unit (par a (op a))
ax {K} {a = chu x y t} = chumap (λ _ -> ((λ i -> i) , λ i -> i) , λ i j -> refl) (λ (y , x) -> t x y) (λ i j -> refl)
sel₁ : {a b : Chu K} -> ChuMap a (add a b)
sel₁ {K} {a} {b} = chumap inj₁ proj₁ (λ i jk -> refl)
sel₂ : {a b : Chu K} -> ChuMap b (add a b)
sel₂ {K} {a} {b} = chumap inj₂ proj₂ (λ i jk -> refl)
vanish : {a : Chu K} -> ChuMap (add a a) a
vanish {K} {a} = chumap (λ { (inj₁ x) → x ; (inj₂ x) → x}) (λ y -> y , y) λ { (inj₁ x) y → refl ; (inj₂ x) y → refl}
zap : {K} -> ChuMap {K} unit addunit
zap = chumap (λ x -> x) ⊥-elim (λ x y -> refl)
zanything : {a : Chu K} -> ChuMap addunit (par addunit a)
zanything {K} {a = chu x y t} = chumap (λ _ -> (⊥-elim , λ _ -> point) , λ z _ -> ⊥-elim z) proj₁ (λ i kj -> refl)
sll : {a b c : Chu K} -> ChuMap (mul (par a c) b) (par (mul a b) c)
sll {K} {a = chu x y t} {b = chu z w u} {c = chu q r v} = chumap (λ (((yq , rx) , yyy) , pz) -> ((λ ((zw , zy) , qq) -> yq (zy pz)) , λ r' -> rx r' , pz) , λ ((xw , zy), pp) r' -> yyy (zy pz) r') (λ (((xw , zy), pp), r') -> ((λ ((yq , rx), pat) -> xw (rx r')) , λ z' -> zy z' , r') , λ ((yq , rx), zzz) z' -> pp (rx r') z') (λ x y -> refl)
hil : {a b c : Chu K} -> ChuMap (wth (par a c) (par b c)) (par (wth a b) c)
hil {K} {a} {b} {c} = chumap (λ (pac , pbc) -> ((λ { (inj₁ a') → proj₁ (proj₁ pac) a' ; (inj₂ b') → proj₁ (proj₁ pbc) b' }) , λ c' -> proj₂ (proj₁ pac) c' , proj₂ (proj₁ pbc) c') , λ { (inj₁ x) c' → proj₂ pac x c' ; (inj₂ x) c' → proj₂ pbc x c'}) (λ { (inj₁ a' , c') → inj₁ (a' , c') ; (inj₂ b' , c') → inj₂ (b' , c')}) λ { (fst , fst₂ , snd) (inj₁ x , snd₁) → refl ; (fst , fst₂ , snd) (inj₂ x , snd₁) → refl}
{--
srl : a⊗(b⅋c) → (a⊗b)⅋c
slr : (c⅋a)⊗b → c⅋(a⊗b)
srr : a⊗(c⅋b) → c⅋(a⊗b)
hir : (c⅋a) & (c⅋b) → c ⅋ (a&b)
dil : (a⊕b) ⊗ c → a⊗c ⊕ b⊗c
dir : c ⊗ (a⊕b) → c⊗a ⊕ c⊗b
ql : !a ⊗ ?b → ?(!a ⊗ b)
qr : ?a ⊗ !b → ?(a ⊗ !b)
el : !(?a ⅋ b) → ?a ⅋ !b
er : !(a ⅋ ?b) → !a ⅋ ?b
asl : (a ∘ b) ∘ c → a ∘ (b ∘ c)
asr : a ∘ (b ∘ c) → (a ∘ b) ∘ c
--}
comMul : {a b : Chu K} -> ChuMap (mul a b) (mul b a)
comMul = chumap (λ (x , y) -> y , x) (λ ((x , y) , z) -> (y , x), λ i j -> sym (z j i)) λ (pa , pb) ((x , y), z) -> z pb pa
comPar : {a b : Chu K} -> ChuMap (par a b) (par b a)
comPar {K} {a} {b} = opfn (comMul {K} {op b} {op a})
comAdd : {a b : Chu K} -> ChuMap (add a b) (add b a)
comAdd = chumap (λ { (inj₁ x) → inj₂ x ; (inj₂ x) → inj₁ x}) (λ (x , y) -> y , x) λ { (inj₁ x) y → refl ; (inj₂ x) y → refl}
comWth : {a b : Chu K} -> ChuMap (wth a b) (wth b a)
comWth {K} {a} {b} = opfn (comAdd {K} {op b} {op a})
frontmap : {a b : Chu K} -> ChuMap a b -> pos a -> pos b
frontmap (chumap f _ _) = f
backmap : {a b : Chu K} -> ChuMap a b -> neg b -> neg a
backmap (chumap _ g _) = g
relmap : {a b : Chu K} -> (f : ChuMap a b) -> (x : pos a) -> (y : neg b) -> rel b (frontmap f x) y ≡ rel a x (backmap f y)
relmap (chumap _ _ fg) = fg
exists : {X : Set} -> (P : X -> Chu K) -> Chu K
exists {K} {X} P = chu (Σ X λ x -> pos (P x)) ((x : X) -> neg (P x)) λ (x , Y) xN -> rel (P x) Y (xN x)
all : {X : Set} -> (P : X -> Chu K) -> Chu K
all {K} {X} P = chu ((x : X) -> pos (P x)) (Σ X λ x -> neg (P x)) λ xY (x , N) -> rel (P x) (xY x) N
intros : {X : Set} -> (P : X -> Chu K) -> (x : X) -> ChuMap (P x) (exists P)
intros P x = chumap (λ Px -> (x , Px)) (λ nPx -> nPx x) λ Px nPx -> refl
elims : {X : Set} -> (P : X -> Chu K) -> (y : Chu K) -> ((x : X) -> ChuMap (P x) y) -> ChuMap (exists P) y
elims P y f = chumap (λ (x , xP) -> frontmap (f x) xP) (λ nX x -> backmap (f x) nX) λ (x , pX) y -> relmap (f x) pX y
apply : {X : Set} -> (P : X -> Chu K) -> (x : X) -> ChuMap (all P) (P x)
apply P x = chumap (λ xP -> xP x) (λ nPx -> (x , nPx)) λ nPx Px -> refl
generate : {X : Set} -> (P : X -> Chu K) -> (y : Chu K) -> ((x : X) -> ChuMap y (P x)) -> ChuMap y (all P)
generate P x f = chumap (λ px x -> frontmap (f x) px) (λ (x , nP) -> backmap (f x) nP) λ px (x , nP) -> relmap (f x) px nP
idmap : {a : Chu K} -> ChuMap a a
idmap = chumap (λ i -> i) (λ i -> i) λ x y -> refl
compose : {a b c : Chu K} -> ChuMap a b -> ChuMap b c -> ChuMap a c
compose f g = chumap (λ x -> frontmap g (frontmap f x)) (λ y -> backmap f (backmap g y)) λ x y -> trans (relmap g (frontmap f x) y) (relmap f x (backmap g y))
record Functor (K : Set) : Set₁ where
field
F₀ : Chu K → Chu K
F₁ : ∀ {A B} -> (ChuMap A B) → ChuMap (F₀ A) (F₀ B)
-- Were too complicated to prove.
-- identityF : ∀ {A} -> F₁ {A} {A} idmap ≡ idmap
-- compositionF : ∀ {A B C} {f : ChuMap A B} {g : ChuMap B C} -> F₁ (compose f g) ≡ compose (F₁ f) (F₁ g)
record BiFunctor (K : Set) : Set₁ where
field
G₀ : Chu K → Chu K → Chu K
G₁ : ∀ {A B C D : Chu K} -> (ChuMap A B) → (ChuMap C D) → ChuMap (G₀ A C) (G₀ B D)
-- identityG : ∀ {A B} -> G₁ {A} {A} {B} {B} idmap idmap ≡ idmap
-- compositionG : ∀ {A B C A' B' C'} (f : ChuMap A B) (g : ChuMap B C) (f' : ChuMap A' B') (g' : ChuMap B' C') -> G₁ (compose f g) (compose f' g') ≡ compose (G₁ f f') (G₁ g g')
addF : BiFunctor K
addF = record { G₀ = add; G₁ = addFunctor }
mulF : BiFunctor K
mulF = record { G₀ = mul; G₁ = mulFunctor }
parF : BiFunctor K
parF = record { G₀ = par; G₁ = parFunctor }
wthF : BiFunctor K
wthF = record { G₀ = wth; G₁ = wthFunctor }
expF : Functor K
expF = record { F₀ = exp; F₁ = lift }
data ChuF (K : Set) : Set₁ where
Var : ChuF K
Add : ChuF K -> ChuF K -> ChuF K
Wth : ChuF K -> ChuF K -> ChuF K
Mul : ChuF K -> ChuF K -> ChuF K
Par : ChuF K -> ChuF K -> ChuF K
Exp : ChuF K -> ChuF K
Const : Chu K -> ChuF K
ChuFobj : ChuF K -> Chu K -> Chu K
ChuFobj Var x = x
ChuFobj (Add c d) x = add (ChuFobj c x) (ChuFobj d x)
ChuFobj (Wth c d) x = wth (ChuFobj c x) (ChuFobj d x)
ChuFobj (Mul c d) x = mul (ChuFobj c x) (ChuFobj d x)
ChuFobj (Par c d) x = par (ChuFobj c x) (ChuFobj d x)
ChuFobj (Exp c) x = exp (ChuFobj c x)
ChuFobj (Const x) y = x
ChuFfun : {A B : Chu K} → (chuf : ChuF K) → ChuMap A B → ChuMap (ChuFobj chuf A) (ChuFobj chuf B)
ChuFfun Var m = m
ChuFfun (Add c d) m = addFunctor (ChuFfun c m) (ChuFfun d m)
ChuFfun (Wth c d) m = wthFunctor (ChuFfun c m) (ChuFfun d m)
ChuFfun (Mul c d) m = mulFunctor (ChuFfun c m) (ChuFfun d m)
ChuFfun (Par c d) m = parFunctor (ChuFfun c m) (ChuFfun d m)
ChuFfun (Exp c) m = lift (ChuFfun c m)
ChuFfun (Const x) m = idmap
ChuFtoFunctor : ChuF K -> Functor K
ChuFtoFunctor chuf = record { F₀ = ChuFobj chuf ; F₁ = ChuFfun chuf }
mutual
{-# NO_POSITIVITY_CHECK #-}
data InitialFixPoint (F : Functor K) : Set where
fix₁ : pos (Functor.F₀ F (Fix {K} F)) → InitialFixPoint F
{-# NO_POSITIVITY_CHECK #-}
record FinalFixPoint (F : Functor K) : Set where
coinductive
constructor fix₂
field
unfix₂ : neg (Functor.F₀ F (Fix {K} F))
{-# TERMINATING #-}
Fix : Functor K -> Chu K
Fix F = chu (InitialFixPoint F) (FinalFixPoint F) λ { (fix₁ x) y → rel (Functor.F₀ F (Fix F)) x (FinalFixPoint.unfix₂ y)}
ins : (F : Functor K) -> ChuMap (Functor.F₀ F (Fix F)) (Fix F)
ins F = chumap fix₁ FinalFixPoint.unfix₂ λ x y -> refl
uns : (F : Functor K) -> ChuMap (Fix F) (Functor.F₀ F (Fix F))
uns F = chumap (λ { (fix₁ x) → x}) fix₂ λ { (fix₁ x) y → refl }
{-# TERMINATING #-}
cata : ∀ {c} (F : Functor K) -> ChuMap (Functor.F₀ F c) c -> ChuMap (Fix F) c
cata F alg = compose (uns F) (compose (Functor.F₁ F ((cata F alg))) alg)
opF : Functor K -> Functor K
opF record { F₀ = F₀ ; F₁ = F₁ } = record { F₀ = λ x → op (F₀ (op x)) ; F₁ = λ f → opfn (F₁ (opfn f)) }
CoFix : Functor K -> Chu K
CoFix F = op (Fix (opF F))
cofun : ∀{a b : Chu K} → ChuMap (op (op a)) b → ChuMap a b
cofun {K} {chu _ _ _} m = m
cofun₂ : ∀{a b : Chu K} → ChuMap a (op (op b)) → ChuMap a b
cofun₂ {K} {a} {chu _ _ _} m = m
coins : (F : Functor K) -> ChuMap (CoFix F) (((Functor.F₀ F (CoFix F))))
coins F = cofun₂ (opfn (ins (opF F)))
couns : (F : Functor K) -> ChuMap (((Functor.F₀ F (CoFix F)))) (CoFix F)
couns F = cofun (opfn (uns (opF F)))
ana : ∀ {c} (F : Functor K) -> ChuMap c (Functor.F₀ F c) -> ChuMap c (CoFix F)
ana {K} {chu a y t} F coalg = opfn (cata (opF F) (opfn coalg))
frontframe : {a b : Chu K} -> ChuMap a b -> ChuMap unit (par (op a) b)
frontframe {K} {a = chu x y t} {b = chu z w v} f = chumap (λ point -> (frontmap f , backmap f) , λ x y -> sym (relmap f x y)) (λ (x' , w') -> v (frontmap f x') w') λ point (x' , w') -> sym (relmap f x' w')
frontframemap : {a b : Chu K} -> ChuMap a b -> pos (par (op a) b)
frontframemap f = frontmap (frontframe f) point
sessionF : Functor K
sessionF = record { F₀ = wth unit; F₁ = wthFunctor idmap }
sessionCoalg : ChuMap unit (wth unit unit)
sessionCoalg = chumap (λ point → point , point) (λ { (inj₁ x) → x ; (inj₂ x) → x}) λ { x (inj₁ y) → refl ; x (inj₂ y) → refl}
session : ChuMap unit (CoFix sessionF)
session = ana sessionF sessionCoalg
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment