Conversion between Scott encoding and Church endocing for naturals in CoC

Church

\/(N: *) ->
\/(z: N) ->
\/(s: N -> N) ->
N

ChurchOne

./ChurchSucc ./ChurchZero

ChurchSucc

\(n: ./Church ) ->
\(N: *) ->
\(z: N) ->
\(s: N -> N) ->
s (n N z s)

ChurchThree

./ChurchSucc ./ChurchTwo

ChurchToScott

\(n: ./Church ) ->
n ./Scott ./ScottZero ./ScottSucc

ChurchTwo

./ChurchSucc ./ChurchOne

ChurchZero

\(N: *) ->
\(z: N) ->
\(s: N -> N) ->
z

Main

./ScottToChurch
    (./ScottSucc
        (./ChurchToScott
            (./ChurchSucc
                (./ScottToChurch ./ScottThree ))))

Mu

\(F: * -> *) ->
\/(A: *) ->
(F A -> A) ->
A

Scott

./ScottF (./Mu ./ScottF )

ScottCase

\(n: ./Scott ) ->
\(R: *) ->
\(a: R) ->
\(f: ./Scott -> R) ->
n R a (\(x: ./Mu ./ScottF ) -> f (./ScottOut x))

ScottF

\(X: *) -> \/(R: *) -> R -> (X -> R) -> R

ScottFmap

\(X: *) ->
\(Y: *) ->
\(f: X -> Y) ->
\(x: ./ScottF X) ->
\(R: *) ->
\(r: R) ->
\(ym: Y -> R) ->
x R r (\(xv: X) -> ym (f xv))

ScottFold

\(X: *) ->
\(k: ./ScottF X -> X) ->
\(t: ./Mu ./ScottF ) ->
t X k

ScottIn

\(s: ./Scott ) ->
\(X: *) ->
\(k: ./ScottF X -> X) ->
k ((./ScottFmap (./Mu ./ScottF ) X) (./ScottFold X k) s)

ScottOne

./ScottSucc ./ScottZero

ScottOut

\(t: ./Mu ./ScottF ) ->
./ScottFold (./Scott ) (./ScottFmap (./Scott ) (./Mu ./ScottF ) ./ScottIn ) t

ScottPred

\(n: ./Scott ) ->
./ScottCase n ./Scott ./ScottZero (\(pred: ./Scott ) -> pred)

ScottSucc

\(n: ./Scott ) ->
\(X: *) ->
\(x: X) ->
\(y: ./Mu ./ScottF -> X) ->
y (./ScottIn n)

ScottThree

./ScottSucc ./ScottTwo

ScottToChurch

\(n: ./Scott ) ->
./ScottFold
./Church
(\(k: ./ScottF ./Church ) -> k ./Church ./ChurchZero ./ChurchSucc )
(./ScottIn n)

ScottTwo

./ScottSucc ./ScottOne

ScottZero

\(X: *) ->
\(x: X) ->
\(y: ./Mu ./ScottF -> X) ->
x