Skip to content

Instantly share code, notes, and snippets.

@rwbarton

rwbarton/assoc_rw_test.lean Secret

Created Jul 30, 2018
Embed
What would you like to do?
universes u v
class category (Obj : Type u) : Type (max u (v+1)) :=
(Hom : Obj → Obj → Type v)
(identity : Π X : Obj, Hom X X)
(compose : Π {X Y Z : Obj}, Hom X Y → Hom Y Z → Hom X Z)
(left_identity : ∀ {X Y : Obj} (f : Hom X Y), compose (identity X) f = f)
(right_identity : ∀ {X Y : Obj} (f : Hom X Y), compose f (identity Y) = f)
(associativity : ∀ {W X Y Z : Obj} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z), compose (compose f g) h = compose f (compose g h))
infixr ` ≫ `:80 := category.compose -- type as \gg
infixr ` ⟶ `:10 := category.Hom -- type as \h
local notation f ` ∘ `:80 g:80 := g ≫ f
section
parameters {C : Type u} [cat : category.{u v} C]
include cat
parameters {a b : C} {i : a ⟶ b}
parameters {x : C} {f : a ⟶ x} (h : b ⟶ x) (e : h ∘ i = f)
parameters {y : C} (g : x ⟶ y)
include e
def gh : b ⟶ y := g ∘ h
example : gh ∘ i = g ∘ f := begin
dsimp [gh],
-- assoc_rw [e]
rw [←category.associativity, e]
end
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment