I’m struggling with the basic syntax and I’m going to need to see some examples. I get the impression that I need to declare a polymorphic type param.

Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
  (at level 10, x binder, y binder, t at level 200,
  format "'[  ' '[  ' 'λ'  x  ..  y ']' ,  '/' t ']'").

Definition Identity       := λ"x",     "x".
Notation   "I"            := Identity.
Check       I.

Syntax error: [open_binders] expected after 'λ' (in [term]).

I’m also trying to do something which I think would be more idiomatic in COQ, but with even less success:

Require Import Int.
Require Import ZArith.
Open Scope Int_scope.

Definition double (n : Z) : Z := n * 2.
Definition half   (n : Z) : Z := n / 2.

(* n = (a+b)(a+b) = (a*a) + (2*a*b) + (b*b) *)

Fixpoint square   (n : Z) : nat := match n with
| 0 => 0
| n => square(half(n)) + double(half(n) * (n - half(n))) + square(n - half(n))
end.

Lemma square_n_n :
  forall (n : Z),
    square(n) = n * n.
Proof.
  intro n.
  unfold square.
  reflexivity.
Qed.

Close Scope Int_scope.

Found a constructor of inductive type nat while a constructor of Z is expected