module Kraus where

import swapDisc
import testInh

-- we encode the example of Nicolai Kraus
-- for this we need the impredicative encoding of propositional truncation

-- swap with zero

swZero : N -> N -> N
swZero = swapF N eqN zero


homogeneous : (x:N) -> Id ptU (N,x) (N,zero)
homogeneous x = homogDec N eqN f0N f1N x zero

-- test : (x:N) -> Id (Id ptU (N,x) (N,zero)) (homogeneous x) (homogeneous x)
-- test x = refl (Id ptU (N,x) (N,zero)) (homogeneous x)

-- the following type is a contractible, hence a proposition

sNzero : U
sNzero = singl ptU (N,zero)  -- Sigma (Sigma U (id U)) (\ v -> Id ptU u (N,zero))

propSNzero : prop sNzero
propSNzero = singlIsProp ptU (N,zero)

-- we have a map inhI N -> sNzero, with the notation of Nicolai Kraus

flifted : inhI N -> sNzero
flifted = inhrecI N sNzero propSNzero (\ x -> ((N,x),homogeneous x))

Tmyst : inhI N -> U
Tmyst x = (flifted x).1.1

opaque homogeneous

myst : (x: inhI N) -> Tmyst x
myst x = (flifted x).1.2

transparent homogeneous

mystN : (n: N) -> Tmyst (incI N n)
mystN n = myst (incI N n)

propMyst : (n:N) -> Id N (myst (incI N n)) n
propMyst n = refl N n

testMyst : N -> N
testMyst n = myst (incI N n)