michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hott): adjust expliciteness of arguments

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-02 13:49:47 -05:00 • committed by Leonardo de Moura
parent cda828bfe8
commit 6124b87870
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/algebra/category/basic.lean
View file

@ -10,16 +10,18 @@ structure category [class] (ob : Type) : Type :=
(hom : ob → ob → Type)
(comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
(ID : Π (a : ob), hom a a)
(assoc : Π ⦃a b c d : ob⦄ {h : hom c d} {g : hom b c} {f : hom a b},
(assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b),
comp h (comp g f) = comp (comp h g) f)
(id_left : Π ⦃a b : ob⦄ {f : hom a b}, comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ {f : hom a b}, comp f !ID = f)
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
namespace category
variables {ob : Type} [C : category ob]
variables {a b c d : ob}
include C
definition compose := comp
definition id [reducible] {a : ob} : hom a a := ID a
infixr `∘` := comp