Advice on Generalizing Definitions

Stream: new members

[Jesse Endo Jenks]

Hi everyone. I'm not quite sure how to phrase this question, but I'm hoping for some advice on how to structure definitions.

Here's my current example. I have a basic definition for categories:

class Category (obj : Type u) where
  Hom : obj → obj → Sort v
  Id : ∀ (A : obj), Hom A A
  comp : (Hom B C) → (Hom A B) → (Hom A C)

  assoc : ∀ {A B C D : obj} (f : Hom A B) (g : Hom B C) (h : Hom C D), comp h (comp g f) = comp (comp h g) f
  unit_right : ∀ {A B : obj} (f : Hom A B), comp f (Id A) = f
  unit_left : ∀ {A B : obj} (f : Hom A B), comp (Id B) f = f

I also have a basic definition for posets:

variable (A : Type u)

class Poset where
  rel : A → A → Prop

  reflexivity : ∀ (a : A), rel a a
  transitivity : ∀ {a b c : A}, rel a b → rel b c → rel a c
  antisymmetry : ∀ {a b : A}, rel a b → rel b c → a = b

It's relatively easy to show that an instance of Poset is an instance of Category

instance [Poset A] : LE A where
  le := Poset.rel

instance [Poset A] : Category A where
  Hom a b := a ≤ b
  Id := Poset.reflexivity
  comp a_le_b b_le_c := Poset.transitivity b_le_c a_le_b
  assoc := by simp
  unit_right := by simp
  unit_left := by simp

But how can I define instance : Category Poset (?)? Or for that matter, instance : Category Category (?)?

I'm guessing I have to take universe levels into account, like "Category of Posets whose objects are from universe level u", but I'm stuck on how to express such a definition.

I have definitions for what I _would_ put as Hom and Id (I think), but maybe this is also where my approach is misleading me.

def isMonotone {A B} [LE A] [LE B] (f : A → B) : Prop :=
  ∀ (a a' : A), a ≤ a' → (f a) ≤ (f a')

structure PosetHom [Poset A] [Poset B] where
  toFun : A → B
  isMonotone : isMonotone toFun

def PosetId [Poset A] : PosetHom A A where
  toFun := id
  isMonotone := by
    simp [isMonotone]
    intro _ _ h
    exact h

Any advice would be appreciated. Thanks!

[Kevin Buzzard]

You can see how mathlib does it using docs#CategoryTheory.Bundled

[Jesse Endo Jenks]

Ok, I think I got it! So far I have something like this

def Pos := Bundled Poset.{u}

instance : Category.{u+1,u+1} Pos where
  Hom P Q := @PosetHom P.α Q.α P.str Q.str
  Id P := @PosetId P.α P.str
  -- ... etc, bit ugly but can be cleanup up later

Similarly

def Cat := Bundled Category.{u, v}

and once I get to defining functors, I can define something like

instance : Category Cat where
  Hom X Y := X ⥤ Y
  -- etc

[Kevin Buzzard]

The point about Bundled is that it makes the category instances for you (using mathlib's categories).

Making category theory again with all the bells and whistles like Bundled will be a lot of work, mathlib has a category theory library where this stuff is made already.

[Jesse Endo Jenks]

Understood, this is more so I can learn lean, not to reinvent mathlib. Thanks for the pointers!