rewrite failed

Stream: new members

[Dean Young]

Does anyone know why this gives me an error of

tactic 'rewrite' failed, motive is not type correct
C : category
X Y : Obj C
p : X = Y
⊢ Cmp C X Y X (Iso C X Y p) (Iso C Y X (_ : Y = X)) = Idn X

-- 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


-- Cmp morphism
def Cmp (C : category) (X : Obj C) (Y : Obj C) (Z : Obj C) (f : Hom X Y) (g : Hom Y Z) := C.Cmp X Y Z f g


-- An equality of objects should produce a homomorphism
def Iso (C : category) (X : Obj C) (Y : Obj C) (p : X = Y) : C.Hom X Y := by
rewrite [p];
exact (Idn Y)


def IsoInv (C : category) (X : Obj C) (Y : Obj C) (p : X = Y) : Cmp C X Y X (Iso C X Y p) (Iso C Y X (Eq.symm p)) = Idn X := by
rewrite [p];

[Adam Topaz]

Try subst p instead

[Dean Young]

That worked.

Could you say a bit about the difference between subst and rewrite?