(\X =>
  [ Var: Nat
  , Zero: <>
  , Suc: X
  , Rec: <Target: X, Zero: X, Suc: X>
  , Abs: X
  , App: <Fun: X, Arg: X>
  ])
->
(\X =>
  [ Var: Nat
  , Lit: Nat
  , Suc: X
  , Abs: X
  , App: <Fun: X, Arg: X>
  , Unit: <>
  , Pair: <Fst: X, Snd: X>
  , Fst: X
  , Snd: X
  , Absurd: <Target: X>
  , Inl: X
  , Inr: X
  , Case: <Target: X, Left: X, Right: X>
  , Expand: X
  , Contract: X
  , Fold: <Target: X, Body: X>
  , Let: <Bound: X, Body: X>
  , Annot:
    < Term: X
    , Type: (\Y =>
      [ Var: Nat
      , N: <>
      , Arrow: <Dom: Y, Cod: Y>
      , Unit: <>
      , Pair: <Fst: Y, Snd: Y>
      , Bottom: <>
      , Sum: <Left: Y, Right: Y>
      , Fix: Y
      ])
    >
  ])