lean2/hott/algebra/precategory/strict.hlean

54 lines
1.5 KiB
Text
Raw Normal View History

/-
Copyright (c) 2015 Jakob von Raumer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.precategory.functor
Authors: Floris van Doorn, Jakob von Raumer
-/
import .basic .functor
open category is_trunc eq function sigma sigma.ops
namespace category
structure strict_precategory[class] (ob : Type) extends precategory ob :=
(is_hset_ob : is_hset ob)
attribute strict_precategory.is_hset_ob [instance]
definition strict_precategory.mk' [reducible] (ob : Type) (C : precategory ob)
(H : is_hset ob) : strict_precategory ob :=
precategory.rec_on C strict_precategory.mk H
structure Strict_precategory : Type :=
(carrier : Type)
(struct : strict_precategory carrier)
attribute Strict_precategory.struct [instance] [coercion]
definition Strict_precategory.to_Precategory [coercion] [reducible]
(C : Strict_precategory) : Precategory :=
Precategory.mk (Strict_precategory.carrier C) C
open functor
definition precat_strict_precat : precategory Strict_precategory :=
precategory.mk (λ a b, functor a b)
(λ a b, @functor.is_hset_functor a b _)
(λ a b c g f, functor.compose g f)
(λ a, functor.id)
(λ a b c d h g f, !functor.assoc)
(λ a b f, !functor.id_left)
(λ a b f, !functor.id_right)
definition Precat_of_strict_precats := precategory.Mk precat_strict_precat
namespace ops
abbreviation SPreCat := Precat_of_strict_precats
--attribute precat_strict_precat [instance]
end ops
end category