fixing "broken" composition

Stream: new members

[Dean Young]

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?

[Reid Barton]

The short answer is Eq.rec

[Dean Young]

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?

[Reid Barton]

Automatically

[Reid Barton]

It's annoying that it does not get documentation.

[Reid Barton]

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]

We can give it documentation using add_decl_doc

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Dean Young]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Dean Young]

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]

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

[Reid Barton]

by should not have a matching end

[Dean Young]

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]

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

[Dean Young]

a bit Yoneda...

[Dean Young]

lovely connection with the Yoneda lemma.

[Dean Young]

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

[Reid Barton]

exact whatever

[Dean Young]

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

[Dean Young]

Thanks for your help

[Dean Young]

oh haha I thought you were commenting on my asking for an exact answer. But it's just the name of the tactic.

[Dean Young]

oh this is great! I'm so happy to have learned the exact tactic.