chu spaces

demo.agda

{-# 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