|
912
|
1 open import Category
|
|
|
2 open import Level
|
|
|
3 module subcat {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') (B : Category c₁ c₂ ℓ) (F : Functor A B) where
|
|
|
4
|
|
|
5 open import cat-utility
|
|
|
6 open import Relation.Binary.PropositionalEquality
|
|
|
7 open Functor
|
|
|
8
|
|
|
9 FCat : Category c₁' c₂ ℓ
|
|
|
10 FCat = record {
|
|
|
11 Obj = Obj A
|
|
|
12 ; Hom = λ a b → Hom B (FObj F a) (FObj F b)
|
|
|
13 ; _o_ = Category._o_ B
|
|
|
14 ; _≈_ = Category._≈_ B
|
|
|
15 ; Id = λ {a} → id1 B (FObj F a)
|
|
|
16 ; isCategory = record {
|
|
|
17 isEquivalence = IsCategory.isEquivalence (Category.isCategory B) ;
|
|
|
18 identityL = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
|
|
|
19 identityR = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
|
|
|
20 o-resp-≈ = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
|
|
|
21 associative = λ{a b c d f g h } → IsCategory.associative (Category.isCategory B)
|
|
|
22 }
|
|
|
23 }
|
