equality type and equality of types

Stream: lean4

[Dean Young]

I have a category structure like this:

structure Cat where
Obj   : Type 1
Mor   : Type 1
Dom : Mor -> Obj
Cod : Mor -> Obj
Id : Obj -> Mor

Comp : forall (G : Mor),
forall (F : Mor),
forall (_ : Dom G = Cod F),
Mor

DomId : forall (C : Obj),
Dom (Id C) = C

CodId : forall (C : Obj),
Cod (Id C) = C

DomComp : forall (G : Mor),
$\forall$ (F : Mor),
$\forall$ (p : Dom G = Cod F),
Dom (Comp G F p) = Dom F
CodComp : \forall (G : Mor),
forall (F : Mor),
forall (p : Dom G = Cod F),
Cod (Comp G F p) = Cod G
CompComp : forall (H : Mor),
forall (G : Mor),
forall (F : Mor),
forall (p : Dom H = Cod G),
forall (q : Dom G = Cod F),
Comp H (Comp G F q) (Eq.trans p (Eq.symm (CodComp G F q))) = Comp (Comp H G p) F (Eq.trans (DomComp H G p) q)

And a functor structure like this:

structure Fun where
Dom : Cat
Cod : Cat
Obj : Dom.Obj -> Cod.Obj
Mor : Dom.Mor -> Cod.Mor

Id  : forall (C : Dom.Obj),
Mor (Dom.Id C) = Cod.Id (Obj C)

DomObj : $\forall$ (f : Dom.Mor),
Cod.Dom (Mor f) = Obj (Dom.Dom f)

CodObj : $\forall$ (f : Dom.Mor),
Cod.Cod (Mor f) = Obj (Dom.Cod f)

MorComp : forall (G : Dom.Mor),
forall (F : Dom.Mor),
forall (p : Dom.Dom G = Dom.Cod F),
Mor (Dom.Comp G F p) = (Cod.Comp (Mor G) (Mor F) (Eq.trans (DomObj G) (Eq.trans (congrArg Obj p) (Eq.symm (CodObj F)))))

Now I'm trying to make a natural transformation structure:

structure Trn where
Dom : Fun
Cod : Fun
DoubleDom : Dom.Dom = Cod.Dom
DoubleCod : Dom.Cod = Cod.Cod
Val : Dom.Dom.Obj -> Dom.Cod.Mor
DomVal : forall (X : Dom.Dom.Obj), Dom.Cod.Dom (Val X) = Dom.Obj X
/-
CodVal : forall (X : Dom.Dom.Obj), Dom.Cod.Cod (Val X) = Cod.Obj X
-/
/-
Comm : $\forall$ (f : Dom.Dom.Mor), Comp (Dom.Mor f) (Val (Dom.Dom.Dom f)) (Eq.trans (Dom.DomObj f) (Eq.symm CodVal Dom.Dom.Dom f)) = Comp (Val (Dom.Dom.Cod f)) (Cod.Mor f) (Eq.trans (DomVal Dom.Dom.Cod f) (Eq.symm (CodObj Cod.CodObj)))
-/

However, I can't create the right witnesses for the codomain at the structure map and commutativity. For instance, if

variables {X Y : Type 1}
variable p : X = Y
variables {x y : X}

how do I obtain x = y in Y?

[Reid Barton]

(deleted)

[Reid Barton]

You need to use Eq.rec somehow (not sure of Lean 4 spelling).

[Reid Barton]

This "essentially algebraic theory" presentation of categories works okay for 1-categories, but Cat itself isn't really a 1-category so you are going to end up with some pain.

[Trebor Huang]

You can coerce using the equation, but another way is to expose the domain and codomain as parameters of the structure, instead of a field. That's how it is actually done.

[Notification Bot]

Dean Young has marked this topic as unresolved.

[Dean Young]

Trebor Huang said:

You can coerce using the equation, but another way is to expose the domain and codomain as parameters of the structure, instead of a field. That's how it is actually done.

Thanks!!!