hoq-0.3: examples/circle.hoq

import Paths

data Nat = zero | suc Nat

data Z = positive Nat | negative Nat with
    negative zero = positive zero

succ : Z -> Z
succ (positive x)       = positive (suc x)
succ (negative zero)    = positive (suc zero)
succ (negative (suc x)) = negative x

pred : Z -> Z
pred (positive zero)    = negative (suc zero)
pred (positive (suc x)) = positive x
pred (negative x)       = negative (suc x)

data Circle = base | loop I with
    loop left  = base
    loop right = base

wind : Z -> base = base
wind (positive zero)    = idp
wind (positive (suc x)) = wind (positive x) * path loop
wind (negative (suc x)) = wind (negative x) * inv (path loop)

pred-succ : (x : Z) -> pred (succ x) = x
pred-succ (positive x) = idp
pred-succ (negative (suc x)) = idp

succ-pred : (x : Z) -> succ (pred x) = x
succ-pred (positive zero) = idp
succ-pred (positive (suc x)) = idp
succ-pred (negative x) = idp

iter : I -> Set
iter i = iso Z Z succ pred pred-succ succ-pred i

code : Circle -> Set
code base     = Z
code (loop i) = iter i

encode : {x : Circle} -> base = x -> code x
encode _ p = coe (\i -> code (p @ i)) left (positive zero) right

assoc : (p q r : base = base) -> (p * q) * r = p * (q * r)
assoc p q = J (\x s -> (p * q) * s = p * (q * s)) idp

wind-succ-loop-neg : (x : Nat) -> wind (pred (negative x)) * path loop = wind (negative x)
wind-succ-loop-neg x =
    assoc (wind (negative x)) (inv (path loop)) (path loop) *
    map (\p -> wind (negative x) * p) (inv-comp (path loop))

wind-succ-loop : (x : Z) -> wind (pred x) * path loop = wind x
wind-succ-loop (positive zero) = wind-succ-loop-neg zero
wind-succ-loop (positive (suc x)) = idp
wind-succ-loop (negative x) = wind-succ-loop-neg x

decode : (x : Circle) -> code x -> base = x
decode base     = wind
decode (loop i) =
    coe (\j -> Path (\k -> iter k -> base = loop k) wind (\y -> wind-succ-loop y @ j)) left
    (path (\k y -> wind (coe iter k y left) * psqueeze (path loop) k))
    right @ i

encode-decode : {x : Circle} (p : base = x) -> decode x (encode p) = p
encode-decode _ = J (\x p -> decode x (encode p) = p) idp

coe-comp : (p q : base = base) (z : Z) ->
    coe (\i -> code (p * q @ i)) left z right =
    coe (\i -> code (q @ i)) left (coe (\i -> code (p @ i)) left z right) right
coe-comp p q z = J (\x s -> coe (\i -> code (p * s @ i)) left z right =
    coe (\i -> code (s @ i)) left (coe (\i -> code (p @ i)) left z right) right) idp q

coe-inv : (p : base = base) (z : Z) -> coe (\i -> code (inv p @ i)) left z right = coe (\i -> code (p @ i)) right z left
coe-inv = J (\x s -> (y : code x) ->
    coe (\i -> code (inv s @ i)) left y right = coe (\i -> code (s @ i)) right y left) (\_ -> idp)

decode-encode-base : (z : Z) -> encode (wind z) = z
decode-encode-base (positive zero) = idp
decode-encode-base (positive (suc x)) =
    coe-comp (wind (positive x)) (path loop) (positive zero) * map succ (decode-encode-base (positive x))
decode-encode-base (negative (suc x)) =
    
    encode (wind (negative (suc x)))
    
  ==< idp >==
    
    coe (\i -> code (wind (negative x) * inv (path loop) @ i)) left (positive zero) right
    
  ==< coe-comp (wind (negative x)) (inv (path loop)) (positive zero) >==
    
    coe (\i -> code (inv (path loop) @ i)) left (coe (\i -> code (wind (negative x) @ i)) left (positive zero) right) right
    
  ==< coe-inv (path loop) (coe (\i -> code (wind (negative x) @ i)) left (positive zero) right) >==
    
    coe (\i -> code (loop i)) right (coe (\i -> code (wind (negative x) @ i)) left (positive zero) right) left
    
  ==< idp >==
    
    pred (encode (wind (negative x)))
    
  ==< map pred (decode-encode-base (negative x)) >==
    
    pred (negative x)
    
  ==< idp >==
    
    negative (suc x)
    
  !qed

Prop-Contr : {A : Prop} (a a' : A) -> a = a'
Prop-Contr _ _ _ = contr

Circle-elim-Prop : (P : Circle -> Prop) (b : P base) -> (x : Circle) -> P x
Circle-elim-Prop P b base     = b
Circle-elim-Prop P b (loop i) = 
    coe  (\j -> Path (\k -> P (loop k)) b (Prop-Contr (transport P (path loop) b) b @ j)) left
    (path (\j -> coe (\k -> P (loop k)) left b j)) right @ i

decode-encode : (x : Circle) (z : code x) -> encode (decode x z) = z
decode-encode = Circle-elim-Prop (\x -> (z : code x) -> encode (decode x z) = z) decode-encode-base

Circle-loop-space-is-Z : (base = base) = Z
Circle-loop-space-is-Z = path (iso (base = base) Z encode (decode base) encode-decode (decode-encode base))