## Stream: new members

### Topic: fixing "broken" composition

#### Dean Young (Mar 06 2023 at 05:30):

Here, as you can see, I have the definition of a category:

-- A category C consists of:
structure category where

-- A type of objects:
Obj : Type u  -- which depends on an unknown universe u

-- For each object X and each object Y, a type C.Hom X Y
Hom : (_:Obj),(_:Obj), Type v

-- For each object X, a term C.Idn X : C.Hom X X
Idn : (X:Obj),Hom X X

-- For objects X, Y, and Z, and terms _ : Hom X Y and _ : Hom Y Z, a term
-- C.Cmp X Y Z f g
Cmp : (X:Obj),(Y:Obj),(Z:Obj),(_:Hom X Y),(_:Hom Y Z),Hom X Z

-- such that:

-- 1) for objects X, Y : C.Obj and a morphism f : C.Hom X Y, C.Cmp X Y Y f (C.Idn Y) = f,
Id₁ : (X:Obj),(Y:Obj),(f:Hom X Y),Cmp X Y Y f (Idn Y) = f

-- 2) for objects X, Y : C.Obj and a morphism f : C.Hom X Y, C.Cmp X X Y (C.Idn X) f = f,
Id₂ : (X:Obj),(Y:Obj),(f:Hom X Y),Cmp X X Y (Idn X) f = f

-- 3) for objects W, X, Y, Z : C.Obj and morphisms f : C.Hom W X, g : C.Hom X Y, h : C.Hom Y Z,
-- (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h
Ass : (W:Obj),(X:Obj),(Y:Obj),(Z:Obj),(f:Hom W X),(g:Hom X Y),(h:Hom Y Z),
(Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- Obj notation:
def Obj (C : category) := C.Obj

-- Hom notation which infers the category in which the hom Type resides:
def Hom {C : category} (X : Obj C) (Y : Obj C) := C.Hom X Y

-- Idn morphism notation which infers the category in which the Idn morphism resides:
def Idn {C : category} (X : Obj C) := C.Idn X

I am playing around with basic definitions and tactics involving this single structure for now. The first goal I have could be called "fixing broken composition". I want to define a composition like so:

def Cmp {C : category} (X : Obj C) (Y₁ : Obj C) (Y₂ : Obj C) (Z : Obj C) (p : Y₁ = Y₂) (f : Hom X Y₁) (g : Hom Y₂ Z) : Hom X Z := sorry

It seems like I need some kind of rule involving equality of types, which I am not familiar with. Where can I find the necessary information to define Cmp here?

#### Dean Young (Mar 06 2023 at 06:03):

I think it would be really helpful to see this spelled out some more. I don't want to take too much of your time though.

Where is Eq.rec defined?

Automatically

#### Reid Barton (Mar 06 2023 at 06:04):

It's annoying that it does not get documentation.

#### Reid Barton (Mar 06 2023 at 06:05):

The slightly longer answer is ... then what? If you're actually using this "fixed composition" (and it seems hard to avoid in some cases) then you're also going to have to reason about it

#### Mario Carneiro (Mar 06 2023 at 06:05):

We can give it documentation using add_decl_doc

#### Reid Barton (Mar 06 2023 at 06:05):

In the mathlib 3 category theory library we have something called docs#category_theory.eq_to_hom

#### Reid Barton (Mar 06 2023 at 06:06):

which is kind of a "fixed identity" between two equal objects, and seems to work fairly well

#### Reid Barton (Mar 06 2023 at 06:07):

And then to build your Cmp, we stick this thing in the middle

#### Dean Young (Mar 06 2023 at 06:13):

Aha, I see -- that's better. Maybe you could spell out these instead:

variable {X : Type}
variable {Y : Type}
variable {p : X = Y}
def f : X  Y := sorry
def g : Y  X := sorry
def id₁ (x : X) : g (f x) = x := sorry
def id₂ (y : Y) : f (g y) = y := sorry

#### Reid Barton (Mar 06 2023 at 06:17):

The theorems will be proved by something like by cases p; rfl

#### Reid Barton (Mar 06 2023 at 06:17):

f is exactly Eq.cast p, I think, though for your actual application you will need Eq.rec

#### Reid Barton (Mar 06 2023 at 06:18):

It's also okay to define f and g with tactics, with rw.

#### Dean Young (Mar 06 2023 at 06:40):

I wanted something like this as well:

variable {X : Type}
variable {Y : Type}
variable {p : X = Y}
def eq_to_hom {X Y : Obj C} (p : X = Y) : Hom X Y := by rewrite p; Idn Y end

#### Dean Young (Mar 06 2023 at 06:40):

I'm still pretty unfamiliar with tactics which is why this was a good exercise for me.

#### Reid Barton (Mar 06 2023 at 06:50):

by should not have a matching end

#### Dean Young (Mar 06 2023 at 06:51):

after fixing that I still get this:

unsolved goals
C: category
XY: Obj C
p: X = Y
Hom Y Y

How do I tell it to fill it with Idn Y?

#### Dean Young (Mar 06 2023 at 06:55):

variable {X : Type}
variable {Y : Type}
variable {p : X = Y}
def asdfj {_ Y : Obj C} (_ : Y = Y) : Hom Y Y := Idn Y
def eq_to_hom {X Y : Obj C} (p : X = Y) : Hom X Y := by
rw [p ];
asdfj

a bit Yoneda...

#### Dean Young (Mar 06 2023 at 06:57):

lovely connection with the Yoneda lemma.

#### Dean Young (Mar 06 2023 at 06:58):

I guess I just want to give it a formula at the end but I don't know the syntax for that.

exact whatever

#### Dean Young (Mar 06 2023 at 07:02):

I just haven't heard how to give an explicit formula in the tactic mode.