§ CubicalTT: sharpening thinking about indexed functions

-- | function from nat to nat defined by lambda abstraction
f1 : nat -> nat -> nat = \(b: nat) -> \(c : nat) ->  b

-- | function from nat, nat -> nat defined by case analaysis
f2 : nat -> nat -> nat =
  split
    zero -> split@(nat -> nat) with
                zero -> zero
                suc b' -> zero
    suc a' -> split@(nat -> nat) with
                zero -> a'
                suc b' -> b'

-- | parametrized family of nats, defined by definition.
g1 (b : nat) (c : nat) : nat = b

-- | Family of nat parameterized by `(x: nat), `(y: nat)
-- | cannot split on parameters, can only split on fn.
-- g2 (x : nat) (y : nat) : nat =
--   split
--     zero -> split@(nat -> nat) with
--                 zero -> zero
--                 suc b' -> zero
--     suc a' -> split@(nat -> nat) with
--                 zero -> a'
--                 suc b' -> b'