2014-12-12 04:14:53 +00:00
|
|
|
-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
|
|
|
-- Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
-- Author: Floris van Doorn
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
open eq is_trunc
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
structure precategory [class] (ob : Type) : Type :=
|
|
|
|
(hom : ob → ob → Type)
|
|
|
|
(homH : Π {a b : ob}, is_hset (hom a b))
|
|
|
|
(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),
|
2014-12-12 19:19:06 +00:00
|
|
|
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)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
2015-01-26 19:31:12 +00:00
|
|
|
attribute precategory [multiple-instances]
|
2014-12-22 01:18:38 +00:00
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
namespace precategory
|
|
|
|
variables {ob : Type} [C : precategory ob]
|
|
|
|
variables {a b c d : ob}
|
|
|
|
include C
|
2015-01-26 19:31:12 +00:00
|
|
|
attribute homH [instance]
|
2014-12-12 04:14:53 +00:00
|
|
|
|
2015-02-01 05:29:34 +00:00
|
|
|
definition compose [reducible] := comp
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
definition id [reducible] {a : ob} : hom a a := ID a
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
infixr `∘` := comp
|
2014-12-12 04:14:53 +00:00
|
|
|
infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
|
|
|
|
|
|
|
|
variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
theorem id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left
|
2014-12-12 04:14:53 +00:00
|
|
|
|
2014-12-12 19:19:06 +00:00
|
|
|
theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
|
|
|
|
calc i = i ∘ id : id_right
|
|
|
|
... = id : H
|
2014-12-12 04:14:53 +00:00
|
|
|
|
2014-12-12 19:19:06 +00:00
|
|
|
theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id :=
|
|
|
|
calc i = id ∘ i : id_left
|
|
|
|
... = id : H
|
2015-02-21 00:30:32 +00:00
|
|
|
|
|
|
|
definition homset [reducible] (x y : ob) : hset :=
|
|
|
|
hset.mk (hom x y) _
|
|
|
|
|
2014-12-12 04:14:53 +00:00
|
|
|
end precategory
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
structure Precategory : Type :=
|
|
|
|
(objects : Type)
|
|
|
|
(category_instance : precategory objects)
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
namespace precategory
|
|
|
|
definition Mk {ob} (C) : Precategory := Precategory.mk ob C
|
|
|
|
definition MK (a b c d e f g h) : Precategory := Precategory.mk a (precategory.mk b c d e f g h)
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
definition objects [coercion] [reducible] := Precategory.objects
|
|
|
|
definition category_instance [instance] [coercion] [reducible] := Precategory.category_instance
|
|
|
|
notation g `∘⁅` C `⁆` f := @compose (objects C) (category_instance C) _ _ _ g f
|
|
|
|
-- TODO: make this left associative
|
|
|
|
-- TODO: change this notation?
|
2014-12-12 04:14:53 +00:00
|
|
|
|
|
|
|
end precategory
|
|
|
|
|
|
|
|
open precategory
|
|
|
|
|
2015-02-21 00:30:32 +00:00
|
|
|
protected definition Precategory.eta (C : Precategory) : Precategory.mk C C = C :=
|
|
|
|
Precategory.rec (λob c, idp) C
|