cubical-0.1.0: examples/testInh.cub

module testInh where

import set

-- test the inh and squash functions

zz : inh N
zz = inc N zero

eq1 : Id (inh N) zz zz
eq1 = refl (inh N) zz

eq2 : Id (inh N) zz zz
eq2 = squash N zz zz

inhUIP : (A : U) -> set (inh A)
inhUIP A = propUIP (inh A) (squash A)

test : Id (Id (inh N) zz zz) eq1 eq2
test = inhUIP N zz zz eq1 eq2

-- impredicative encoding

inhI : U -> U
inhI A = (X : U) -> prop X -> (A -> X) -> X

incI : (A : U) -> A -> inhI A
incI A a = \X h f -> f a

squashI : (A : U) -> prop (inhI A)
squashI A = propPi U (\X -> prop X -> (A -> X) -> X) rem
  where
  rem1 : (X : U) -> prop X -> prop ((A -> X) -> X)
  rem1 X h = propImply (A -> X) X (\_ -> h)

  rem : (X : U) -> prop (prop X -> (A -> X) -> X)
  rem X =  propImply (prop X) ((A -> X) -> X) (rem1 X)

inhrecI : (A : U) (B : U) (p : prop B) (f : A -> B) (h : inhI A) -> B
inhrecI A B p f h = h B p f

inhUIPI : (A : U) -> UIP (inhI A)
inhUIPI A = propUIP (inhI A) (squashI A)

zzI : inhI N
zzI = incI N zero

eq1I : Id (inhI N) zzI zzI
eq1I = refl (inhI N) zzI

eq2I : Id (inhI N) zzI zzI
eq2I = squashI N zzI zzI

testI : Id (Id (inhI N) zzI zzI) eq1I eq2I
testI = inhUIPI N zzI zzI eq1I eq2I