宣言・定義ペアの完全な記述は
under D assuming Σ declare k-x-mor f :k Γ →k A in M define f := E
ここで：
- D はドクトリン。ドクトリンはメタ指標と文法からなる。ドクトリン配下の指標は、ドクトリンが定義した文法により記述する。
- シグマは背景指標。予備知識を表す。
- k は自然数で、次元を表す。
- x は（広義の）射のセル形状 simple, multi, comulti, poly のどれか
- f はラベルまたは記号〈symbol〉。構文範疇は識別子。
- Γ はコンテキスト／環境／型判断などと呼ばれる。シーケントの前提／仮定／仮説パート。
- A は射の余域。余域の型。「命題が型〈PaT〉」主義だと命題。
- M は圏、複圏、多圏などのアビタ
- E は諸々の条件で整形式なコンビネーション〈項 | 式〉
色々省略されて、
declare f : Γ → A define f := E
書き方のバリエーションとして、
declare Γ → f: A define f := E
定理の記述なら
theorem f: Γ → A proof E
ここで：
- f は定理の名前
- Γ は定理の仮定の記述
- A は定理の結論の記述
- E は証明項〈proof term〉
