|
31
|
1 module universal-mapping where
|
|
|
2
|
|
|
3 open import Category -- https://github.com/konn/category-agda
|
|
|
4 open import Level
|
|
|
5 open import Category.HomReasoning
|
|
|
6
|
|
|
7 open Functor
|
|
|
8 record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
9 ( U : Functor B A )
|
|
|
10 ( F : Obj A -> Obj B )
|
|
|
11 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
|
|
|
12 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b )
|
|
|
13 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
14 field
|
|
|
15 universalMapping : {a' : Obj A} { b' : Obj B } -> ( f : Hom A a' (FObj U b') ) ->
|
|
|
16 A [ A [ FMap U ( f * ) o η a' ] ≈ f ]
|
|
|
17
|
|
|
18
|
|
|
19 record UniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
|
|
|
20 ( U : Functor B A )
|
|
|
21 ( F : Obj A -> Obj B )
|
|
|
22 ( η : (a : Obj A) -> Hom A a ( FObj U (F a) ) )
|
|
|
23 ( _* : { a : Obj A}{ b : Obj B} -> ( Hom A a (FObj U b) ) -> Hom B (F a ) b )
|
|
|
24 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
|
|
|
25 field
|
|
|
26 isUniversalMapping : IsUniversalMapping A B U F η _*
|
|
|
27
|
|
|
28
|
|
|
29
|
