Zulip Chat Archive

Stream: mathlib4

Topic: Constructing morphisms in a cartesian closed category

Albus Dompeldorius (Mar 04 2025 at 13:29):

TL;DR: Is there a method of constructing morphisms in a cartesian closed category that is just as simple as constructing functions between types?

Hi,

I'm working on defining Mealy machines (a type of automata) in a general way. Mealy machines can be defined in any monoidal category, and I'm particularly interested in defining them in the category Preord of preorders.

For instance, in the category of types, we have this definition of a Mealy machine:

structure Mealy (α β : Type) where
  state : Type
  trans : α → state → state
  out : α → state → β

Given a mealy machine Mealy α β, we get an induced mealy machine which takes a non-empty list of inputs (modeled as α × List α) and gives an output in β:

def Mealy.iterate (m : Mealy α β) : Mealy (α × List α) β where
  state := m.state
  trans as s := m.trans as.1 $ foldr m.trans s as.2
  out as s := m.out as.1 $ foldr m.trans s as.2

In the category of preorders, the above translates to the following:

structure PreordMealy (α β : Preord) where
  state : Preord
  trans : α × state →o state
  out : α × state →o β

As we can see, we have replaced the types and functions with preorders and monotone functions. Note that we are using the uncurried form of trans and out. I also tried doing the curried version, but then I had to do a lot of currying/uncurrying with curry.symm.toFun and curry.toFun everywhere.

Now, let's define iteration of a PreordMealy:

open List
open OrderHom

def foldrHom' [Preorder α] [Preorder β] (f : α × β →o β) : β × List α →o β where
  toFun := (foldr f.toFun.curry).uncurry
  monotone' := sorry

def foldrHom [Preorder α] [Preorder β] (f : α × β →o β) : List α × β →o β := (foldrHom' f).comp (OrderHomClass.toOrderHom OrderIso.prodComm)

--(I couln't find the following definition in mathlib)
def prodAssoc [Preorder α] [Preorder β] [Preorder γ] : (α × β) × γ ≃o (α × β × γ) where
  toEquiv := Equiv.prodAssoc α β γ
  map_rel_iff' := by aesop

def Mealy.iterate (m : Mealy α β) : Mealy (Preord.of $ (α × List α)) β where
  state := m.state
  trans := m.trans.comp ((prodMap id (foldrHom m.trans)).comp (OrderHomClass.toOrderHom prodAssoc))
  out := m.out.comp ((prodMap id (foldrHom m.trans)).comp (OrderHomClass.toOrderHom prodAssoc))

As you can see, this is a lot more verbose than the version for types. The curried version is even worse (I will spare you the details).

My question is: Is there a simpler way to define the monotone functions above, preferably in the curried version (trans : α →o state →o state and out : α →o state →o β)?

In theory, it should be just as simple as in the case of types, given the fact that Preord is a cartesian closed category, so it should allow lambda notation.

Aaron Liu (Mar 04 2025 at 13:38):

Albus Dompeldorius said:

My question is: Is there a simpler way to define the monotone functions above, preferably in the curried version (trans : α →o state →o state and out : α →o state →o β)?

In theory, it should be just as simple as in the case of types, given the fact that Preord is a cartesian closed category, so it should allow lambda notation.

Probably, there is, just no one has implemented such a thing yet.

David Wärn (Mar 04 2025 at 17:29):

I wrote a prototype tactic framework for this a while ago, in Lean 3 and based on Flypitch. Not sure what's happened since

Albus Dompeldorius (Mar 04 2025 at 21:52):

After some googling, I think I want something like this: https://acatalepsie.fr/posts/overloading-lambda

Aaron Liu (Mar 08 2025 at 03:48):

Here's a prototype I wrote

It's a bit long

Aaron Liu (Mar 08 2025 at 03:51):

(don't ask what the ₑ stands for, I don't know either)

Albus Dompeldorius (Mar 09 2025 at 17:06):

Really cool!

I also made a prototype based on the blog post I linked. It does not support currying yet, but it supports both categories and cartesian categories.

Here it is

Albus Dompeldorius (Mar 09 2025 at 17:08):

Our approaches are a bit different. While your approch seems to be using macros for everything, my approach tries to reuse as much of the standard syntax as possible.

Albus Dompeldorius (Mar 09 2025 at 17:09):

I also have a feeling that we get better error messages in my approach.

Albus Dompeldorius (Mar 09 2025 at 17:12):

Currently I'm trying to get rid of the macros, and the need to use pair in my prototype, fully relying on coercion. For instance, one should be able to just write code like this:

def reverse3 : a ⊗ b ⊗ c ⟶ c ⊗ b ⊗ a := fun (x,y,z) =>
  let (y',x') := swap (x,y)
  (z,y',x')

Albus Dompeldorius (Mar 11 2025 at 12:17):

I'm trying to use coercion to apply morphisms as f x, but I'm struggling to get the coercions to fire. Here is the code:

import Mathlib.CategoryTheory.ChosenFiniteProducts

open CategoryTheory MonoidalCategory

variable [Category C] [ChosenFiniteProducts C]
variable {r a b c : C}

def Port (r a : C) := r ⟶ a

def encode {a b : C} (f : a ⟶ b) : Port r a → Port r b := (· ≫ f)
instance : CoeFun (a ⟶ b) (fun _ => ∀ {r}, Port r a → Port r b) := ⟨fun f => encode f⟩

def pair : Port r a × Port r b -> Port r (a ⊗ b) := ChosenFiniteProducts.lift.uncurry

@[default_instance]
instance : CoeOut (Port r a) (Port r a)
  := ⟨id⟩

@[default_instance]
instance
  [CoeOut A (Port r a)]
  [CoeOut B (Port r b)]
  : CoeOut (A × B) (Port r (a ⊗ b))
  := ⟨pair ∘ Prod.map CoeOut.coe CoeOut.coe⟩

variable {f : a ⊗ b ⟶ c}
variable {x : Port r a × Port r b}

-- I want to use coersions to be able to write `f x` and get a value of type `Port r c`.

-- This works:
#check f (CoeOut.coe x) -- (fun {r} => encode f) (CoeOut.coe x) : Port r c
#check f (x : Port r (a ⊗ b)) -- (fun {r} => encode f) ((pair ∘ Prod.map id id) x) : Port r c
#check (f x : Port r c) -- (fun {r} => encode f) ((pair ∘ Prod.map id id) x) : Port r c

-- This coercion gives an error:
#check f x
-- application type mismatch
--   (fun {r} => encode f) x
-- argument
--   x
-- has type
--   Port r a × Port r b : Type ?u.50444
-- but is expected to have type
--   Port ?m.56807 (a ⊗ b) : Type ?u.50444

Albus Dompeldorius (Mar 11 2025 at 12:18):

Could this be an instance of the problem described here? #lean4 > RFC discussion: coercions don't fire with metavariables

Floris van Doorn (Mar 11 2025 at 13:02):

Albus Dompeldorius said:

Could this be an instance of the problem described here? #lean4 > RFC discussion: coercions don't fire with metavariables

Maybe... It's definitely a more complicated example, since it involves 2 coercions, one of which is not a CoeFun.

Albus Dompeldorius (Mar 11 2025 at 13:07):

It gives the same error if I manually convert f like this:

#check (encode f) x.

Now there is only one coercion involved. This shows that it is the CoeOut instances that fail to trigger.

Albus Dompeldorius (Mar 11 2025 at 13:27):

It seems I managed to fix it by modifying the encoding function:

def encode {a b : C} (f : a ⟶ b) [CoeOut A (Port r a)]: A → Port r b := fun x => (x : Port r a) ≫ f
instance : CoeFun (a ⟶ b) (fun _ => ∀ {r A} [CoeOut A (Port r a)], A → Port r b) := ⟨fun f => encode f⟩

Floris van Doorn (Mar 11 2025 at 13:43):

Yes, then it is an example of the same issue (and CoeFun by itself seems to work fine).

Last updated: May 02 2025 at 03:31 UTC