Create Instance of a Category

Stream: new members

[Hank]

Hello all,

I am trying to create an instance of a category whose objects are True and False and whose morphisms are identity and "not". Here is what I tried, with some help from ChatGPT:

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Category.Cat

-- Define the morphisms (arrows) between objects
def BoolCatHom : Bool → Bool → Type
| false, false => Unit  -- Identity morphism
| true, true   => Unit  -- Identity morphism
| false, true  => Unit  -- A morphism representing 'not'
| true, false  => Empty -- No morphism from True to False

-- Now declare the category instance
instance : CategoryStruct Bool where
  Hom := BoolCatHom
  id := λ X, Unit.unit  -- Identity morphism is trivial (only one element in Unit)
  comp := λ X Y Z f g, Unit.unit  -- Composition is trivial since morphisms are unique

-- Now we extend the Category structure by showing that the axioms hold
instance : Category Bool where
  id_comp := by intros; cases X; cases f; rfl  -- The identity morphism is a left identity
  comp_id := by intros; cases X; cases f; rfl  -- The identity morphism is a right identity
  assoc := by intros; cases W; cases X; cases Y; cases Z; cases f; cases g; cases h; rfl  -- Associativity of composition

However, CategoryStruct Bool and Category Bool have error messages saying

function expected at
  CategoryStruct
term has type
  ?m.153

I do not know how to fix them. I suppose Category is a class that takes in a type as a parameter, and that should be enough? I would appreciate it if anyone can answer this.

[Kevin Buzzard]

Try set_option autoImplicit false at the top of your file. Does the error change?

[Hank]

@Kevin Buzzard Yes, CategoryStruct Bool and Category Bool no longer cause errors after adding that. Thank you!

[Kevin Buzzard]

Are you sure? No errors reported by VS Code at all?

[Hank]

Yes, there are other errors, but I will try to fix them myself before asking further questions. I guess some of those errors are about LEAN 3 syntax that is not compatible with LEAN 4. I noticed that ChatGPT only generates LEAN 3.

[Kevin Buzzard]

I thought that the problem with your code was that you did not have open CategoryTheory or whatever namespace the things you're trying to use, are in.

[Hank]

So far I have the following

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Category.Cat

set_option autoImplicit false

open CategoryTheory

def BoolCatHom : Bool → Bool → Type
-- Unit is a type with exactly one element, Unit.unit
| false, false => Unit
| true, true => Unit
| false, true => Unit
| true, false => Empty

instance : Category Bool where
  Hom := BoolCatHom
  id := fun X => match X with
    | false => Unit.unit
    | true => Unit.unit
  -- why can I not write fun X => Unit.unit?
  comp := by
    intro X Y Z f g
    cases X
    cases Z
    exact Unit.unit
    exact Unit.unit
    cases Z
    sorry
    exact Unit.unit

I currently implement comp by considering all cases of X, Y, and Z. But I have trouble continuing at the line before the sorry. The goals there are
image.png
I believe the first goal true --> false means BoolCatHom true false, which is of type Empty. So I guess this is an impossible case, but how do I close this goal?

Also, for id, I wonder why I cannot simply write fun X => Unit.unit.

Any help will be appreciated.
And yes, I need open CategoryTheory so that I can use Category in the subsequent code. Thanks to Kevin Buzzard for pointing that out.

[Kevin Buzzard]

Just do cases on Y?

[Kevin Buzzard]

By the way, reading your first post, the morphisms you're making here are not "the identity and not" as you can see from your definition. In fact I can't really make sense of this goal, "not" is a function from Bool to Bool, not a function from an element of Bool to an element of Bool

[Hank]

Ah, I have changed my definition of morphisms here to the imply relation.

The following now works

  comp := by
    intro X Y Z f g
    cases X
    cases Z
    exact Unit.unit
    exact Unit.unit
    cases Y
    nomatch f -- since f is of type BoolCatHom false true, so f : Empty
    cases Z
    nomatch g
    exact Unit.unit

Indeed, I need cases Y to turn f into a case like true --> false, which is of type Empty and needs to be eliminated beforehand.

If there is a better way of implementing this Bool category with "imply" as morphisms, please let me know. I am not sure if using Unit and Emptyin BoolCatHom to denote which morphisms are allowed or not is the right way.

[Kevin Buzzard]

It looks fine to meactually you're constructing data in tactic mode which is probably not good, for the data fields you should probably be using match rather than by. I guess the acid test is whether you can prove the axioms. If you can it's probably ok.