Zulip Chat Archive
Stream: general
Topic: errors in product of categories
Kind Bubble (Jan 19 2023 at 21:40):
Can anyone help me fix these errors in Lean 4? I'm trying to construct the product of categories.
import Init.Data.ToString.Basic
universe u
universe v
structure Cat where
Obj : Type u
Hom : ∀(_:Obj),∀(_:Obj), Type v
Idn : ∀(X:Obj),Hom X X
Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
Id2 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X X Y) (Idn X) f = f
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
def Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g
def Hom {C : Cat} (X : C.Obj) (Y : C.Obj) := C.Hom X Y
notation X "➔" Y => Hom X Y
def Idn {C : Cat} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X
structure Fun (C : Cat) (D : Cat) where
Obj : ∀(_ : C.Obj),D.Obj
Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
Idn : ∀(X : C.Obj),Mor X X (C.Idn X) = D.Idn (Obj X)
Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),D.Cmp (Obj X) (Obj Y) (Obj Z) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g))
def CatIdn (C : Cat) : Fun C C :=
{Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>Eq.refl (C.Cmp X Y Z f g)}
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):=
{Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>((Eq.trans) (G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))}
def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F
def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F
def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) := Eq.refl (CatCmp B C E F (CatCmp C D E G H))
def Cats : Cat := {Obj := Cat,Hom := Fun,Idn := CatIdn,Cmp := CatCmp,Id1 := CatId1,Id2 := CatId2,Ass := CatAss}
def CatPrd (C : Cat) (D : Cat) : Cat := {Obj := C.Obj × D.Obj, Hom := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>((Hom X.1 Y.1) × (Hom X.2 Y.2)), Idn := fun(P : C.Obj × D.Obj)=>(C.Idn P.1, D.Idn P.2), Cmp := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(Z : C.Obj × D.Obj)=>fun(f : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>fun(g : (Hom Y.1 Z.1) × (Hom Y.2 Z.2))=>(C.Cmp X.1 Y.1 Z.1 f.1 g.1, D.Cmp X.2 Y.2 Z.2 f.2 g.2), Id1 := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(f : (C.Hom X.1 Y.1) × (D.Hom X.2 Y.2))=>Eq.rec (C.Id1 X.1 Y.1 f.1) (D.Id1 X.2 Y.2 f.2), Id2 := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(f : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>Eq.rec (C.Id2 X.1 Y.1 f.1) (D.Id2 X.2 Y.2 f.2), Ass := fun(W : C.Obj × D.Obj)=>fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(Z : C.Obj × D.Obj)=>fun(f : (Hom W.1 X.1) × (Hom W.2 X.2))=>fun(g : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>fun(h : (Hom Y.1 Z.1) × (Hom Y.2 Z.2))=>Eq.rec (C.Ass W.1 X.1 Y.1 Z.1 f.1 g.1 h.1) (D.Ass W.2 X.2 Y.2 Z.2 f.2 g.2 h.2)}
The last definition is what's giving me trouble where I define Id1 and Id2.
I get this:
Main.lean:39:520: error: failed to elaborate eliminator, invalid motive
fun x x =>
(fun X Y Z f g => (Cat.Cmp C X.fst Y.fst Z.fst f.fst g.fst, Cat.Cmp D X.snd Y.snd Z.snd f.snd g.snd)) X Y Y f
((fun P => (Cat.Idn C P.fst, Cat.Idn D P.snd)) Y) =
f
Main.lean:39:663: error: failed to elaborate eliminator, invalid motive
fun x x =>
(fun X Y Z f g => (Cat.Cmp C X.fst Y.fst Z.fst f.fst g.fst, Cat.Cmp D X.snd Y.snd Z.snd f.snd g.snd)) X X Y
((fun P => (Cat.Idn C P.fst, Cat.Idn D P.snd)) X) f =
f
...
Kind Bubble (Jan 20 2023 at 22:11):
Kind Bubble said:
Can anyone help me fix these errors in Lean 4? I'm trying to construct the product of categories.
import Init.Data.ToString.Basic universe u universe v structure Cat where Obj : Type u Hom : ∀(_:Obj),∀(_:Obj), Type v Idn : ∀(X:Obj),Hom X X Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f Id2 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X X Y) (Idn X) f = f 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 def Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g notation g "∘" f => Cmp f g def Hom {C : Cat} (X : C.Obj) (Y : C.Obj) := C.Hom X Y notation X "➔" Y => Hom X Y def Idn {C : Cat} (X : C.Obj) := C.Idn X notation "𝟙" X => Idn X structure Fun (C : Cat) (D : Cat) where Obj : ∀(_ : C.Obj),D.Obj Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y) Idn : ∀(X : C.Obj),Mor X X (C.Idn X) = D.Idn (Obj X) Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),D.Cmp (Obj X) (Obj Y) (Obj Z) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g)) def CatIdn (C : Cat) : Fun C C := {Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>Eq.refl (C.Cmp X Y Z f g)} def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):= {Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>((Eq.trans) (G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))} def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) := Eq.refl (CatCmp B C E F (CatCmp C D E G H)) def Cats : Cat := {Obj := Cat,Hom := Fun,Idn := CatIdn,Cmp := CatCmp,Id1 := CatId1,Id2 := CatId2,Ass := CatAss} def CatPrd (C : Cat) (D : Cat) : Cat := {Obj := C.Obj × D.Obj, Hom := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>((Hom X.1 Y.1) × (Hom X.2 Y.2)), Idn := fun(P : C.Obj × D.Obj)=>(C.Idn P.1, D.Idn P.2), Cmp := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(Z : C.Obj × D.Obj)=>fun(f : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>fun(g : (Hom Y.1 Z.1) × (Hom Y.2 Z.2))=>(C.Cmp X.1 Y.1 Z.1 f.1 g.1, D.Cmp X.2 Y.2 Z.2 f.2 g.2), Id1 := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(f : (C.Hom X.1 Y.1) × (D.Hom X.2 Y.2))=>Eq.rec (C.Id1 X.1 Y.1 f.1) (D.Id1 X.2 Y.2 f.2), Id2 := fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(f : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>Eq.rec (C.Id2 X.1 Y.1 f.1) (D.Id2 X.2 Y.2 f.2), Ass := fun(W : C.Obj × D.Obj)=>fun(X : C.Obj × D.Obj)=>fun(Y : C.Obj × D.Obj)=>fun(Z : C.Obj × D.Obj)=>fun(f : (Hom W.1 X.1) × (Hom W.2 X.2))=>fun(g : (Hom X.1 Y.1) × (Hom X.2 Y.2))=>fun(h : (Hom Y.1 Z.1) × (Hom Y.2 Z.2))=>Eq.rec (C.Ass W.1 X.1 Y.1 Z.1 f.1 g.1 h.1) (D.Ass W.2 X.2 Y.2 Z.2 f.2 g.2 h.2)}The last definition is what's giving me trouble where I define Id1 and Id2.
I get this:
Main.lean:39:520: error: failed to elaborate eliminator, invalid motive fun x x => (fun X Y Z f g => (Cat.Cmp C X.fst Y.fst Z.fst f.fst g.fst, Cat.Cmp D X.snd Y.snd Z.snd f.snd g.snd)) X Y Y f ((fun P => (Cat.Idn C P.fst, Cat.Idn D P.snd)) Y) = f Main.lean:39:663: error: failed to elaborate eliminator, invalid motive fun x x => (fun X Y Z f g => (Cat.Cmp C X.fst Y.fst Z.fst f.fst g.fst, Cat.Cmp D X.snd Y.snd Z.snd f.snd g.snd)) X X Y ((fun P => (Cat.Idn C P.fst, Cat.Idn D P.snd)) X) f = f ...
I've been playing around with the product of categories construction (see previous message). I still can't get it to work, but I did maybe get closer. It seems there's a universe problem again?
I tried to construct the product of categories like this:
def CatPrdObj (C : Cat) (D : Cat) := C.Obj × D.Obj
def CatPrdHom (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) := (Hom X.1 Y.1) × (Hom X.2 Y.2)
def CatPrdIdn (C : Cat) (D : Cat) (P : CatPrdObj C D) := (C.Idn P.1, D.Idn P.2)
def CatPrdCmp (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (Z : CatPrdObj C D) (f : CatPrdHom C D X Y) (g : CatPrdHom C D Y Z) := (C.Cmp X.1 Y.1 Z.1 f.1 g.1, D.Cmp X.2 Y.2 Z.2 f.2 g.2)
def CatPrdId1A (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (CatPrdCmp C D X Y Y f (CatPrdIdn C D Y) = (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))) := Eq.refl (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))
def CatPrdId1B (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2)) = (f.1, f.2) := (C.Id1 X.1 Y.1 f.1) ▸ (D.Id1 X.2 Y.2 f.2)
def CatPrd (C : Cat) (D : Cat) : Cat2 := {Obj := CatPrdObj C D, Hom := CatPrdHom C D, Idn := CatPrdIdn C D, Cmp := CatPrdCmp C D, Id1 := CatPrdId1A C D}
which is loaded with errors for now... but the error seems to be that CatPrdId1B can't solve a universe constraint.
Eric Wieser (Jan 20 2023 at 22:16):
Note that the CatProdId* declarations should be theorems not defs
Kind Bubble (Jan 20 2023 at 22:52):
Eric Wieser said:
Note that the
CatProdId*declarations should betheorems notdefs
Yeah.
I'm totally lost with this congr stuff though.
Also, is it better to keep the Lean 4 stuff on the lean4 stream?
Last updated: Dec 20 2023 at 11:08 UTC