Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Category where
- open import Level
- open import Relation.Binary using (Rel; IsEquivalence; module IsEquivalence; Reflexive; Symmetric; Transitive) renaming (_⇒_ to _⊆_)
- record Category {o m e} : Set ( suc ( o ⊔ m ⊔ e ) ) where
- infix 4 _⇛_ _≡_
- infixr 9 _∘_
- field
- Obj : Set o
- _⇛_ : Rel Obj m
- _≡_ : ∀ {A B} -> Rel (A ⇛ B ) e
- id : ∀ {x} -> x ⇛ x
- _∘_ : ∀ {a b c : Obj} -> (b ⇛ c) -> (a ⇛ b) -> (a ⇛ c )
- data TrivMorph {o} (obj : Set o) : obj -> obj -> Set (suc o) where
- idM : ∀ {x} -> TrivMorph obj x x
- data TrivEquiv {i l} (obj : Set i) (morph : Rel obj l) {dom cod : obj} : morph dom cod -> morph dom cod -> Set (i ⊔ suc l ) where
- idE : forall {x} -> TrivEquiv obj morph x x
- trivEqSimple : ∀ {i l} {obj : Set i} {dom cod : obj} {morph : Rel obj l } {f g h : morph cod dom } -> TrivEquiv obj morph f g
- -> TrivEquiv obj morph g h -> TrivEquiv obj morph f h
- trivEqSimple idE idE = idE
- trivMorphSimpleComp : forall {o} {obj : Set o} {a b c : obj} -> TrivMorph obj b c -> TrivMorph obj a b -> TrivMorph obj a c
- trivMorphSimpleComp idM idM = idM
- trivCat : forall {o } (obj : Set o) -> Category {o}
- trivCat obj = record {Obj = obj
- ; _⇛_ = TrivMorph obj
- ; _≡_ = TrivEquiv obj (TrivMorph obj)
- ; id = idM
- ; _∘_ = trivMorphSimpleComp }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement