Mercurial > hg > Members > kono > Proof > category
changeset 268:2ff44ee3cb32
co universal mapping
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 22 Sep 2013 18:05:09 +0900 |
| parents | b1b728559d89 |
| children | 6056a995964b |
| files | cat-utility.agda pullback.agda |
| diffstat | 2 files changed, 30 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sun Sep 22 17:26:47 2013 +0900 +++ b/cat-utility.agda Sun Sep 22 18:05:09 2013 +0900 @@ -35,6 +35,28 @@ _* : { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) → Hom B (F a ) b isUniversalMapping : IsUniversalMapping A B U F η _* + record coIsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( F : Functor A B ) + ( U : Obj B → Obj A ) + ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) + ( _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + field + couniversalMapping : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → + B [ B [ ε b o FMap F ( f *' ) ] ≈ f ] + couniquness : {b : Obj B} { a : Obj A } → { f : Hom B (FObj F a) b } → { g : Hom A a (U b) } → + B [ B [ ε b o FMap F g ] ≈ f ] → A [ f *' ≈ g ] + + record coUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') + ( F : Functor A B ) + ( U : Obj B → Obj A ) + ( ε : (b : Obj B) → Hom B ( FObj F (U b) ) b ) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where + infixr 11 _*' + field + _*' : { b : Obj B}{ a : Obj A} → ( Hom B (FObj F a) b ) → Hom A a (U b ) + iscoUniversalMapping : coIsUniversalMapping A B F U ε _*' + open NTrans open import Category.Cat record IsAdjunction {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
--- a/pullback.agda Sun Sep 22 17:26:47 2013 +0900 +++ b/pullback.agda Sun Sep 22 18:05:09 2013 +0900 @@ -204,8 +204,8 @@ -- -- Contancy Functor -KI : Functor A ( A ^ I ) -KI = record { +KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → Functor A ( A ^ I ) +KI { c₁'} {c₂'} {ℓ'} I = record { FObj = λ a → K I a ; FMap = λ f → record { -- NTrans I A (K I a) (K I b) TMap = λ a → f ; @@ -230,7 +230,10 @@ ∎ ---limit2adjoint : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) --- ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) --- ( lim : Limit I Γ a0 t0 ) → +open import Function +limit2adjoint : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) + ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) + ( lim : Limit I Γ a0 t0 ) → coUniversalMapping A ( A ^ I ) (KI I) ({!!}) ({!!}) +limit2adjoint = {!!} +