Skip to content

Instantly share code, notes, and snippets.

# cheery/demo.agda

Last active February 28, 2024 10:43
Show Gist options
• Save cheery/701902227be3ab5cf583ebfbd0479636 to your computer and use it in GitHub Desktop.
chu spaces
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 {-# 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
to join this conversation on GitHub. Already have an account? Sign in to comment