From 20ee756ff1159c19c2aa57ddfe241f3d746f4984 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 22 Sep 2016 16:33:24 -0400 Subject: [PATCH] add a small puzzle due to Andrew Polonsky --- experiments/andrew_puzzle.ctt | 66 +++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 experiments/andrew_puzzle.ctt diff --git a/experiments/andrew_puzzle.ctt b/experiments/andrew_puzzle.ctt new file mode 100644 index 0000000..11cdfba --- /dev/null +++ b/experiments/andrew_puzzle.ctt @@ -0,0 +1,66 @@ +-- Formalization of a puzzle posted by Andrew Polonsky in: +-- https://groups.google.com/forum/#!topic/homotopytypetheory/ebUESBRBxVc +module andrew_puzzle where + +Path (A : U) (a0 a1 : A) : U = PathP ( A) a0 a1 + +mapOnPath (A B : U) (f : A -> B) (a b : A) + (p : Path A a b) : Path B (f a) (f b) = f (p @ i) + +subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b = + transport (mapOnPath A U P a b p) e + + +data Bool = tt | ff +data Unit = uu + +-- f, g : Bool -> Bool -> Bool +-- f x y = if x then y else ff +-- g x y = if y then x else ff +f : Bool -> Bool -> Bool = split + tt -> \(y : Bool) -> y + ff -> \(_ : Bool) -> ff + +g (x : Bool) : Bool -> Bool = split + tt -> x + ff -> ff + +-- e : f = g +e : Path (Bool -> Bool -> Bool) f g = + let p : (x y : Bool) -> Path Bool (f x y) (g x y) = split + tt -> split@((y : Bool) -> Path Bool (f tt y) (g tt y)) with + tt -> <_> tt + ff -> <_> ff + ff -> split@((y : Bool) -> Path Bool (f ff y) (g ff y)) with + tt -> <_> ff + ff -> <_> ff + in \(x y : Bool) -> p x y @ i + + +-- Phi : Bool -> Type +-- Phi tt = Bool +-- Phi ff = Unit +Phi : Bool -> U = split + tt -> Bool + ff -> Unit + + +-- Psi : (Bool->Bool->Bool)->Type +-- Psi = \u. (u tt tt) x (u tt ff) x (u ff tt) x (u ff ff) +Prod (A B : U) : U = (_ : A) * B + +Psi : (Bool -> Bool -> Bool) -> U = + \(u : Bool -> Bool -> Bool) -> Prod (Phi (u tt tt)) + (Prod (Phi (u tt ff)) + (Prod (Phi (u ff tt)) (Phi (u ff ff)))) + +-- X : Psi f +-- X = (tt,*,*,*) +X : Psi f = (tt,uu,uu,uu) + +-- Y : Psi g +-- Y = subst Psi e X +Y : Psi g = subst (Bool -> Bool -> Bool) Psi f g e X + +-- X and Y are definitionally equal: +goal : Path (Psi f) X Y = <_> (tt,uu,uu,uu) -- 2.34.1