can't synthesize argument

Stream: lean4

[Dean Young]

I have Cat and Trn structures already made as part of a project on categories. Here's a function I was trying to define:

def Comp (C : Cat ) ( D : Cat ) (g : Trn C D) (f : Trn C D) (p : g.Dom = f.Cod) := g

It's an attempt at vertical composition and the p is a witness to the compatibility.

I get this error:

Main.lean:255:77: error: don't know how to synthesize implicit argument
  @Trn.Cod C D f (?m.3459 C D g f)
context:
C D : Cat
g f : Trn C D
⊢ Cat

I'm not sure what the ?m.3459 really is. But it seems like equality of structures is giving me some trouble. I guess I assumed that equality type would be meaningful for structures, so maybe it's that.

Does anyone know how to fix this error?

[Reid Barton]

#mwe ?

[Dean Young]

Reid Barton said:

#mwe ?

Here you go:

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)

structure Fun (Dom : Cat) (Cod : Cat) where
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)))))

structure Trn (C : Cat) (D : Cat) where
Dom : Fun C CodCod
Cod : Fun C CodCod
Val : C.Obj -> D.Mor
DomVal : forall (X : C.Obj), D.Dom (Val X) = Dom.Obj X
CodVal : forall (X : C.Obj), D.Cod (Val X) = Cod.Obj X
Comm : forall (f : C.Mor), D.Comp (Cod.Mor f) (Val (C.Dom f)) (Eq.trans (Cod.DomObj f) (Eq.symm (CodVal (C.Dom f))))  = D.Comp (Val (C.Cod f)) (Dom.Mor f) (Eq.trans (DomVal (C.Cod f)) (Eq.symm (Dom.CodObj f)))

def Comp (C : Cat ) ( D : Cat ) (g : Trn C D) (f : Trn C D) (p : g.Dom = f.Cod) := g

[Sebastian Ullrich]

I'm assuming CodCod was not supposed to be a free variable (i.e. quantified at Dom and Cod, separately)

[Dean Young]

Sebastian Ullrich said:

I'm assuming CodCod was not supposed to be a free variable (i.e. quantified at Dom and Cod, separately)

yeah-let me edit that