Syntax for multicategories /coloured operads

Stream: general

[Adrian Marti]

Hello all, like some other people, I do believe that using the internal logic of categories for describing objects, arrows and subobjects in a variety of contexts is a very good candidate for formalization.

The reason for this is that statements proven this level of generality, gives us statements about models in all categories. For example, anything we prove in the theory of groups will be true in for group objects in other categories (Lie groups, etc.). As a first step, I'm seeing that there is the potential for developing an efficient notation for arrows in cartesian/symmetric monoidal/monoidal categories, making their use more convenient.

At the moment, I have the following problem. I am starting with formalizing terms. I've come to the conclusion that the right setting to interpret them are multicategories. These are like categories, but instead of an arrow having a source and a target, an arrow is allowed to have multiple sources. For objects $S_1,\cdots,S_n,T$, we denote these arrows by $Mul(S_1,\cdots,S_n;T)$. The classical example are vector spaces equipped with multilinear maps. In this case, these multicategorical arrows arise from the tensor product (or from a different viewpoint, the tensor product monoidal structure arises from this multicategory).

Multicategorical arrows get composed by taking an arrow $f \in Mul(S_1,\cdots,S_n;T)$ and arrows $g_i \in Mul(R_1,\cdots,R_{m_i}, S_i)$ and putting them together to an arrow $Mul(R_1,\cdots, R_{m_k},T)$. There is also an identity and we have corresponding identity and associativity rules. This models precisely the way that we combine terms in sorted logic. Multicategories also naturally provide a context for interpreting terms, at least terms where each free variable gets used exactly once and we're not able to permute the inputs. If we want to be able to permute the inputs, we need to use symmetric multicategories and if we want to use variables more than once, cartesian multicategories.

In the end, I want to be able to have a notation like term x y z w => f (x, g (y, z), w) for multicategorical arrows f and g be compiled into a multicategorical arrow with four inputs (in particular this then will also work for monoidal categories). I'm thinking of using this as a shallow embedding (i.e. no big Expr types, just notation) to keep this layer "lean" and giving us ways to delaborte arrows in this way and giving us better tactic mode behaviour.

However, with this idea I've quickly run into an important problem. A fully dependent version of multicategorical arrows is horrible, as you can see below. Stating the identity axiom requires transport with Eq.mp, and to me it looks like a pretty complicated type of transport (along two variables that depend on each other).

Header

import Mathlib

-- A base type of objects
variable (X: Type*)

structure Multiquiver where
  /-- `Mul ![x₁,..,xₙ] y` denotes the function symbols with input sorts x₁,..xₙ and the output sort y. -/
  Mul: {n: ℕ} → (Fin n → X) → X → Type*

-- Some auxilliary theorems/definitions for defining multicategories.
private theorem flattenPf {n : ℕ} {m : Fin (n + 1) → ℕ} (i : Fin (∑ i, m i))
  (p : ¬i < ∑ i: Fin n, m i.castSucc) : i - ∑ i: Fin n, m i.castSucc < m (Fin.last n) := by
  have h_lt : i.val < ∑ i, m i := i.2
  rw [not_lt] at p
  rwa [tsub_lt_iff_left p, <- Fin.sum_univ_castSucc]

def flatten {X: Type*} {n: ℕ} {m: Fin n → ℕ} (R: (i: Fin n) → Fin (m i) → X): Fin (∑ i, m i) → X :=
  fun i ↦ match n with
  | 0 => Fin.elim0 i
  | n + 1 => if p?: i < ∑i: Fin n, m i.castSucc then
      flatten (fun j ↦ R (Fin.castSucc j)) ⟨i,p?⟩
    else
      R (Fin.last n) ⟨i - ∑ i: Fin n, m i.castSucc, flattenPf i p?⟩

-- Two lemmas for transport at identity composition

lemma flatten_fin_1_idx {n: ℕ}: (∑ (_: Fin n), Nat.succ 0) = n := by
  sorry

lemma flatten_fin_1 {n: ℕ} {S: Fin n → X}: flatten (fun (i: Fin n) ↦ ![S i]) = S ∘ (congrArg Fin flatten_fin_1_idx).mp := by
  sorry

structure Multicategory extends Multiquiver X where
  id: (R: X) → Mul ![R] R
  comp: {n: ℕ} → {m: Fin n → ℕ} → {R: X} → {S: Fin n → X} → {T: (i: Fin n) → Fin (m i) → X}
    → (Π i, Mul (T i) (S i)) → Mul S R → Mul (flatten T) R
  id_comp_1: {n: ℕ} → {R: X} → {S: Fin n → X} → (f: Mul S R)
    → f ≍ comp (R:=R) (S:=S) (T:= fun i ↦ ![S i]) (fun i ↦ id (S i)) f
-- This is a heterogeneous equality because the types of the two functions are different.
-- Fixing this requires transporting the terms into the same type by a combination of the two lemmas above,
-- which is excessively ocmplicated.
-- id_comp_2, and comp_assoc for identity composition on the right and composition associativity are missing here

So what I'm wondering now is:

• How can I change the definition to make this type-theoretically more pleasant? I've thought about indexing by Fintypes instead of Fin n and another idea where we modify composition so that we only compose one input at the time, but none of the two ideas seem to help. Perhaps approaching this through categories of operators helps, i.e. allowing multiple outputs too, in the same way higher operads are done.
• Are there any thoughts on the feasibility of developing a term notation as above (or something something similar)? How would you go about it? I am really inexperienced with metaprogramming and macros.

[Aaron Liu]

Adrian Marti said:

• Are there any thoughts on the feasibility of developing a term notation as above (or something something similar)? How would you go about it? I am really inexperienced with metaprogramming and macros.

I remember doing this for cartesian closed categories although now that I'm a bit more experienced with metaprogramming I could probably come up with a better implementation now.

Aaron Liu said:

Here's a prototype I wrote

It's a bit long

import Mathlib.CategoryTheory.Closed.Cartesian

section
open CategoryTheory ChosenFiniteProducts MonoidalCategory

variable {C : Type*} [Category C] [ChosenFiniteProducts C] [CartesianClosed C] {X Y Z : C}

def CategoryTheory.CartesianClosed.uncurryHom : (Y ⟹ X ⟹ Z) ⟶ (X ⊗ Y ⟹ Z) :=
  CartesianClosed.curry ((α_ _ _ _).hom ≫ CartesianClosed.uncurry (CartesianClosed.uncurry (𝟙 _)))

def CategoryTheory.CartesianClosed.applyMapHom : X ⟹ Y ⟹ Z ⟶ (X ⟹ Y) ⟹ X ⟹ Z :=
  CartesianClosed.curry
    (CartesianClosed.curry
      (lift
        (lift (fst ..) (snd .. ≫ fst ..))
        (lift (fst ..) (snd .. ≫ snd ..)) ≫
      (CartesianClosed.uncurry (𝟙 _) ⊗ CartesianClosed.uncurry (𝟙 _)) ≫
        CartesianClosed.uncurry (𝟙 _)))

def CategoryTheory.CartesianClosed.constLeft (m : X ⟶ Z) : X ⟶ Y ⟹ Z :=
  CartesianClosed.curry (snd Y X ≫ m)

def CategoryTheory.CartesianClosed.constRight (m : Y ⟶ Z) : X ⟶ Y ⟹ Z :=
  CartesianClosed.curry (fst Y X ≫ m)

def CategoryTheory.CartesianClosed.funOfHom {W : C} (f : (W ⟹ X) ⟶ (Y ⟹ Z)) (x : W ⟶ X) : Y ⟶ Z :=
  lift (𝟙 Y) (constRight x) ≫ CartesianClosed.uncurry f

end

declare_syntax_cat efun

namespace efun

open Lean Macro Elab CategoryTheory CartesianClosed

syntax:max (name := eof) "~" term:max : efun
syntax:max (name := eid) ident : efun
syntax (name := eparen) "(" efun ")" : efun
syntax:max (name := eabst) "funₑ" explicitBinders "=>" efun : efun
syntax:lead (name := eapp) efun:max efun:arg+ : efun
syntax:max (name := eto) "~" efun:max : term

@[macro eto]
partial def flattenSearch : Macro := fun stx => match stx with
  | `(term| ~$t) => do
    let (u, t) ← search t
    unless u do throwUnsupported
    `(term| ~$t)
  | _ => throwUnsupported
where
  search (stx : TSyntax `efun) : MacroM (Bool × TSyntax `efun) := match stx with
    | `(efun| $f $[$xs]* $y $z) => do
      let stx ← `(efun| ($f $[$xs]* $y) $z)
      let (_, stx) ← search stx
      return (true, stx)
    | `(efun| $f $x) => do
      let (u, f) ← search f
      let (v, x) ← search x
      let res ← `(efun| $f $x)
      return (u || v, res)
    | `(efun| funₑ%$tk $binders => $x) => do
      let (u, x) ← search x
      let res ← `(efun| funₑ%$tk $binders => $x)
      return (u, res)
    | `(efun| ($t)) => do
      let (_, t) ← search t
      return (true, t)
    | _ => pure (false, stx)

@[macro eto]
partial def expandBindersSearch : Macro := fun stx => match stx with
  | `(term| ~$t) => do
    let (u, t) ← search t
    unless u do throwUnsupported
    `(term| ~$t)
  | _ => throwUnsupported
where
  search (stx : TSyntax `efun) : MacroM (Bool × TSyntax `efun) := do
    let (u, stx) ← expandBinders stx
    match stx with
    | `(efun| $f $x) => do
      let (v, f) ← search f
      let (w, x) ← search x
      let res ← `(efun| $f $x)
      return (u || v || w, res)
    | `(efun| funₑ $binders => $x) => do
      let (v, x) ← search x
      let res ← `(efun| funₑ $binders => $x)
      return (u || v, res)
    | _ => pure (u, stx)
  expandBinders (stx : TSyntax `efun) : MacroM (Bool × TSyntax `efun) := match stx with
  | `(efun| funₑ%$tk $[$xs:binderIdent]* => $b) =>
    Prod.mk true <$> `(efun| funₑ%$tk ($[$xs:binderIdent]* : _) => $b)
  | `(efun| funₑ%$tk $[$xs:binderIdent]* : $t => $b) =>
    Prod.mk true <$> `(efun| funₑ%$tk ($[$xs:binderIdent]* : $t) => $b)
  | `(efun| funₑ%$tk $[$xs]* $y $z => $b) =>
    Prod.mk true <$> `(efun| funₑ%$tk $[$xs]* $y => funₑ%$tk $z:bracketedExplicitBinders => $b)
  | `(efun| funₑ%$tk ($[$xs]* $y $z : $t) => $b) =>
    Prod.mk true <$> `(efun| funₑ%$tk ($[$xs]* $y : $t) => funₑ%$tk ($z : $t) => $b)
  | _ => pure (false, stx)

@[macro eto]
partial def elabAbstSearch : Macro := fun stx => match stx with
  | `(term| ~$t) => do
    let (u, t) ← search t
    unless u do throwUnsupported
    `(term| ~$t)
  | _ => throwUnsupported
where
  search (stx : TSyntax `efun) : MacroM (Bool × TSyntax `efun) := do
    let (u, stx) ← elabAbst stx
    match stx with
    | `(efun| $f $x) => do
      let (v, f) ← search f
      let (w, x) ← search x
      let res ← `(efun| $f $x)
      return (u || v || w, res)
    | `(efun| funₑ $binders => $x) => do
      let (v, x) ← search x
      let res ← `(efun| funₑ $binders => $x)
      return (u || v, res)
    | _ => pure (u, stx)
  elabAbst (stx : TSyntax `efun) : MacroM (Bool × TSyntax `efun) := match stx with
  | `(efun| funₑ%$tk ($x : $t) => $f $y) =>
    Prod.mk true <$>
      `(efun| ~$(mkCIdentFrom tk ``applyMapHom) (funₑ ($x : $t) => $f) (funₑ ($x : $t) => $y))
  | `(efun| funₑ%$tk ($_x : $t) => ~$b) =>
    Prod.mk true <$> `(efun| ~(@$(mkCIdentFrom tk ``constRight) _ _ _ _ $t _ _ $b))
  | _ => pure (false, stx)

macro_rules
  | `(term| ~$t) => match t with
    | `(efun| ~$t) =>
      `(term| $t)
    | `(efun| $f $x) => `(term| $(mkCIdentFrom t ``funOfHom) ~$f ~$x)
    | `(efun| $i:ident) => `(term| $i)
    | `(efun| ($t)) => `(term| ~$t)
    | _ => throwUnsupported

@[macro eto]
partial def efunTelescope : Macro := fun stx => match stx with
  | `(term| ~$t) => push t #[]
  | _ => throwUnsupported
where
  push (stx : TSyntax `efun) (acc : Array (Option (TSyntax `ident) × TSyntax `term × Syntax)) :
      MacroM (TSyntax `term) :=
    match stx with
    | `(efun| funₑ%$tk ($x:ident : $t:term) => $b) => push b (acc.push (some x, t, tk))
    | `(efun| funₑ%$tk (_ : $t:term) => $b) => push b (acc.push (none, t, tk))
    | `(efun| $i:ident) => do
      let mut res : Option (TSyntax `term) := none
      let mut escStack : Array (TSyntax `term × Syntax) := #[]
      for j in acc.reverse do
        match j.fst with
        | some n =>
          if h : res.isSome then
            let b := res.get h
            res := some (← `(term| @$(mkCIdentFrom j.snd.snd ``constRight) _ _ _ _ $j.snd.fst _ _ $b))
          else if i.getId == n.getId then
            let mut st : TSyntax `term ← `(term| $(mkCIdentFrom i ``CategoryStruct.id) $j.snd.fst)
            for m in escStack do
              st ← `(term| @$(mkCIdentFrom m.snd ``constLeft) _ _ _ _ $j.snd.fst $m.fst _ $st)
            res := some st
          else
            escStack := escStack.push j.snd
        | none =>
          escStack := escStack.push j.snd
      match res with
      | some t => return t
      | none =>
        let mut fold : TSyntax `efun ← `(efun| ~$i)
        for j in acc.reverse do
          match j.fst with
          | some n =>
            fold ← `(efun| funₑ%$j.snd.snd ($n:ident : $j.snd.fst) => $fold)
          | none =>
            fold ← `(efun| funₑ%$j.snd.snd (_ : $j.snd.fst) => $fold)
        `(term| ~$fold)
    | _ => throwUnsupported

end efun

open CategoryTheory

variable {C : Type*} [Category C] [ChosenFiniteProducts C] [CartesianClosed C] {X Y Z : C}

#check ~funₑ (g : Y ⟹ Z) (f : X ⟹ Y) (x : X) => g (f x)

[Adrian Marti]

I will have a look soon, I think that notation for arrows in CC categories is also something really useful (it also subsumes the cartesian category case).

[Adrian Marti]

Sorry for not taking the time earlier, but this is pretty cool :slight_smile: FYI, CategoryTheory.CartesianClosed.applyMapHom does not build on newer mathlib versions.

[Adrian Marti]

I was also wondering why the type of the example ~funₑ (g : Y ⟹ Z) (f : X ⟹ Y) (x : X) => g (f x) at the bottom is Y ⟹ Z ⟶ (X ⟹ Y) ⟹ X ⟹ Z.

[Adrian Marti]

Wait it actually makes sense, it's just the curried version of ((Y ⟹ Z) ⊗ (X ⟹ Y) ⊗ X) ⟶ Z

[Adrian Marti]

And maybe the generated term in the example can be simplified a bit so that it can be worked with better in proofs.