natrec-and-monotonicity

data Nat = Z | S Nat

-- plus is monotone
plus Z = \x. x
plus (S x) = \y. S (plus x y)

-- pred is monotone
pred Z = Z
pred (S x) = x

-- (sub x y) = y - x
-- sub is monotone in its second argument
-- but critically, not in its first!
-- woah, how did that happen? induction broke our monotonicity guarantee!

sub Z = \x. x
sub (S x) = \y. pred (sub x y)

sub = natrec (\x. x) (\f y. pred (f y))

-- so sub x = (pred . pred . ... . pred), with `x` many `pred`s
-- key point: id > pred > pred . pred > ... and so on.

-- **what's the type of natrec?**
-- what justifies inductive datastructures in a monotone setting?
-- does Poset have all initial algebras?
-- (what the hell are subobject classifiers?)

-- what is this monotone in?
-- if z <= s z, then it's monotone in n (and s?)
-- if s z <= z, then it's antitone in n
natrec : (z : a) (s : a -> a) -> (n : []Nat) -> a

-- conjecture: monotone in s and z, but not necessarily in n?
-- what does this mean?

type ChurchNat = forall a. (a -> a) -> a -> a

natrec : Nat -> ChurchNat

-- What is the "natural" order on ChurchNat?
-- I dunno, what's the order on a forall-type?
-- *aha*, finally an interesting question!
-- how do we give semantics to forall in Poset?
-- how do we give semantics to forall at all?