takanuva · March 11, 2020 16:42
diff --git a/Church b/Church
 \/(N: *) ->
 \/(z: N) ->
 \/(s: N -> N) ->
 N
diff --git a/ChurchOne b/ChurchOne
 ./ChurchSucc ./ChurchZero
diff --git a/ChurchSucc b/ChurchSucc
 \(n: ./Church ) ->
 \(N: *) ->
 \(z: N) ->
 \(s: N -> N) ->
 s (n N z s)
diff --git a/ChurchThree b/ChurchThree
 ./ChurchSucc ./ChurchTwo
diff --git a/ChurchToScott b/ChurchToScott
 \(n: ./Church ) ->
 n ./Scott ./ScottZero ./ScottSucc
diff --git a/ChurchTwo b/ChurchTwo
 ./ChurchSucc ./ChurchOne
diff --git a/ChurchZero b/ChurchZero
 \(N: *) ->
 \(z: N) ->
 \(s: N -> N) ->
 z
diff --git a/Main b/Main
 ./ScottToChurch
    (./ScottSucc
        (./ChurchToScott
            (./ChurchSucc
                (./ScottToChurch ./ScottThree ))))
diff --git a/Mu b/Mu
 \(F: * -> *) ->
 \/(A: *) ->
 (F A -> A) ->
 A
diff --git a/Scott b/Scott
 ./ScottF (./Mu ./ScottF )
diff --git a/ScottCase b/ScottCase
 \(n: ./Scott ) ->
 \(R: *) ->
 \(a: R) ->
 \(f: ./Scott -> R) ->
 n R a (\(x: ./Mu ./ScottF ) -> f (./ScottOut x))
diff --git a/ScottF b/ScottF
 \(X: *) -> \/(R: *) -> R -> (X -> R) -> R
diff --git a/ScottFmap b/ScottFmap
 \(X: *) ->
 \(Y: *) ->
 \(f: X -> Y) ->
 \(x: ./ScottF X) ->
 \(R: *) ->
 \(r: R) ->
 \(ym: Y -> R) ->
 x R r (\(xv: X) -> ym (f xv))
diff --git a/ScottFold b/ScottFold
 \(X: *) ->
 \(k: ./ScottF X -> X) ->
 \(t: ./Mu ./ScottF ) ->
 t X k
diff --git a/ScottIn b/ScottIn
 \(s: ./Scott ) ->
 \(X: *) ->
 \(k: ./ScottF X -> X) ->
 k ((./ScottFmap (./Mu ./ScottF ) X) (./ScottFold X k) s)
diff --git a/ScottOne b/ScottOne
 ./ScottSucc ./ScottZero
diff --git a/ScottOut b/ScottOut
 \(t: ./Mu ./ScottF ) ->
 ./ScottFold (./Scott ) (./ScottFmap (./Scott ) (./Mu ./ScottF ) ./ScottIn ) t
diff --git a/ScottPred b/ScottPred
 \(n: ./Scott ) ->
 ./ScottCase n ./Scott ./ScottZero (\(pred: ./Scott ) -> pred)
diff --git a/ScottSucc b/ScottSucc
 \(n: ./Scott ) ->
 \(X: *) ->
 \(x: X) ->
 \(y: ./Mu ./ScottF -> X) ->
 y (./ScottIn n)
diff --git a/ScottThree b/ScottThree
 ./ScottSucc ./ScottTwo
diff --git a/ScottToChurch b/ScottToChurch
 \(n: ./Scott ) ->
 ./ScottFold
 ./Church
 (\(k: ./ScottF ./Church ) -> k ./Church ./ChurchZero ./ChurchSucc )
 (./ScottIn n)
diff --git a/ScottTwo b/ScottTwo
 ./ScottSucc ./ScottOne
diff --git a/ScottZero b/ScottZero
 \(X: *) ->
 \(x: X) ->
 \(y: ./Mu ./ScottF -> X) ->
 x
	\(n: ./Church ) ->
	\(N: *) ->
	\(z: N) ->
	\(s: N -> N) ->
	s (n N z s)
	./ScottToChurch
	(./ScottSucc
	(./ChurchToScott
	(./ChurchSucc
	(./ScottToChurch ./ScottThree ))))
	\(n: ./Scott ) ->
	\(R: *) ->
	\(a: R) ->
	\(f: ./Scott -> R) ->
	n R a (\(x: ./Mu ./ScottF ) -> f (./ScottOut x))
	\(X: *) ->
	\(Y: *) ->
	\(f: X -> Y) ->
	\(x: ./ScottF X) ->
	\(R: *) ->
	\(r: R) ->
	\(ym: Y -> R) ->
	x R r (\(xv: X) -> ym (f xv))
	\(X: *) ->
	\(k: ./ScottF X -> X) ->
	\(t: ./Mu ./ScottF ) ->
	t X k
	\(s: ./Scott ) ->
	\(X: *) ->
	\(k: ./ScottF X -> X) ->
	k ((./ScottFmap (./Mu ./ScottF ) X) (./ScottFold X k) s)
	\(t: ./Mu ./ScottF ) ->
	./ScottFold (./Scott ) (./ScottFmap (./Scott ) (./Mu ./ScottF ) ./ScottIn ) t
	\(n: ./Scott ) ->
	./ScottCase n ./Scott ./ScottZero (\(pred: ./Scott ) -> pred)
	\(n: ./Scott ) ->
	\(X: *) ->
	\(x: X) ->
	\(y: ./Mu ./ScottF -> X) ->
	y (./ScottIn n)
	\(n: ./Scott ) ->
	./ScottFold
	./Church
	(\(k: ./ScottF ./Church ) -> k ./Church ./ChurchZero ./ChurchSucc )
	(./ScottIn n)