Mercurial > hg > Members > kono > Proof > category
changeset 94:4fa718e4fd77
Comparison Functor constructed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jul 2013 12:41:40 +0900 |
| parents | 44b61ce90dd9 |
| children | 4be27d290ea2 |
| files | cat-utility.agda nat.agda |
| diffstat | 2 files changed, 65 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/cat-utility.agda Sun Jul 28 21:24:17 2013 +0900 +++ b/cat-utility.agda Mon Jul 29 12:41:40 2013 +0900 @@ -129,24 +129,19 @@ record MResolution {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁' c₂' ℓ' ) ( T : Functor A A ) - { η : NTrans A A identityFunctor T } - { μ : NTrans A A (T ○ T) T } - ( M : Monad A T η μ ) + -- { η : NTrans A A identityFunctor T } + -- { μ : NTrans A A (T ○ T) T } + -- { M : Monad A T η μ } ( UR : Functor B A ) ( FR : Functor A B ) { ηR : NTrans A A identityFunctor ( UR ○ FR ) } { εR : NTrans B B ( FR ○ UR ) identityFunctor } { μR : NTrans A A ( (UR ○ FR) ○ ( UR ○ FR )) ( UR ○ FR ) } ( Adj : Adjunction A B UR FR ηR εR ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where - -- MObj : (a : Obj A) -> Obj A - -- MObj a = FObj ( UR ○ FR ) a - -- MMap : {a b c d : Obj A} -> (f : Hom A a b) -> Hom A (FObj T a) (FObj T b) - -- MMap f = FMap ( UR ○ FR ) f field T=UF : T ≃ (UR ○ FR) - UF=T : (UR ○ FR) ≃ T μ=UεF : {x : Obj A } -> A [ TMap μR x ≈ FMap UR ( TMap εR ( FObj FR x ) ) ] - -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] + -- ηR=η : {x : Obj A } -> A [ TMap ηR x ≈ TMap η x ] -- We need T -> UR FR conversion -- μR=μ : {x : Obj A } -> A [ TMap μR x ≈ TMap μ x ]
--- a/nat.agda Sun Jul 28 21:24:17 2013 +0900 +++ b/nat.agda Mon Jul 29 12:41:40 2013 +0900 @@ -541,7 +541,7 @@ open MResolution -Resolution_T : MResolution A KleisliCategory T M U_T F_T Adj_T +Resolution_T : MResolution A KleisliCategory T U_T F_T Adj_T Resolution_T = record { T=UF = Lemma11; μ=UεF = Lemma12 @@ -555,40 +555,47 @@ { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } ( K : Monad A (U_K ○ F_K) η_K μ_K ) ( AdjK : Adjunction A B U_K F_K η_K ε_K ) - ( RK : MResolution A B T M U_K F_K AdjK ) + ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K} AdjK ) where open Category.Cat.[_]_~_ ≃-sym : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } {F G : Functor C D} → F ≃ G → G ≃ F - ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G {A} {B} f = helper (F≃G f) + ≃-sym {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f) where helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] g ~ f helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl {C = D} (IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory D)) Ff≈Gf) + -- to T=UF constraints happy + hoge : {c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } {c₁' c₂' ℓ' : Level} { D : Category c₁' c₂' ℓ' } + {F G : Functor C D} → F ≃ G → F ≃ G + hoge {_} {_} {_} {C} {_} {_} {_} {D} {F} {G} F≃G f = helper (F≃G f) + where + helper : ∀{a b c d} {f : Hom D a b} {g : Hom D c d} → [ D ] f ~ g → [ D ] f ~ g + helper (Category.Cat.refl Ff≈Gf) = Category.Cat.refl Ff≈Gf + RHom = \(a b : Obj A) -> KleisliHom {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } a b - TtoK : {a b : Obj A} -> (KHom a b) -> {g : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } -> - ([ A ] g ~ g) -> Hom A a (FObj ( U_K ○ F_K ) b) - TtoK f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ] + TtoK : {a b : Obj A} -> (KHom a b) -> {g h : Hom A (FObj T b) (FObj ( U_K ○ F_K) b) } -> + ([ A ] g ~ h) -> Hom A a (FObj ( U_K ○ F_K ) b) + TtoK f {g} (Category.Cat.refl _) = A [ g o (KMap f) ] RMap : {a b : Obj A} -> (f : KHom a b) -> Hom A a (FObj ( U_K ○ F_K ) b) - RMap {a} {b} f = TtoK f (( ≃-sym (UF=T RK))(id1 A b)) + RMap {_} {b} f = TtoK {_} {b} f {_} {_} ((hoge (T=UF RK) (id1 A b))) - KtoT : {a b : Obj A} -> (RHom a b) -> {g : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> - ([ A ] g ~ g) -> Hom A a (FObj T b) - KtoT f (Category.Cat.refl {g} eq) = A [ g o (KMap f) ] + KtoT : {a b : Obj A} -> (RHom a b) -> {g h : Hom A (FObj ( U_K ○ F_K ) b) (FObj T b) } -> + ([ A ] g ~ h) -> Hom A a (FObj T b) + KtoT f {g} {h} (Category.Cat.refl eq) = A [ g o (KMap f) ] RKMap : {a b : Obj A} -> (f : RHom a b) -> Hom A a (FObj T b) RKMap {_} {b} f = KtoT f (( ≃-sym (T=UF RK)) (id1 A b)) RMap-cong : {a b : Obj A} {f g : KHom a b} -> A [ KMap f ≈ KMap g ] -> A [ RMap f ≈ RMap g ] - RMap-cong {a} {b} {f} {g} eq = helper a b f g eq (( ≃-sym (UF=T RK))( id1 A b )) + RMap-cong {a} {b} {f} {g} eq = helper a b f g eq ((hoge (T=UF RK))( id1 A b )) where open ≈-Reasoning (A) helper : (a b : Obj A) (f g : KHom a b) -> A [ KMap f ≈ KMap g ] -> {conv : Hom A (FObj T b) (FObj ( U_K ○ F_K ) b) } -> ([ A ] conv ~ conv) -> A [ RMap f ≈ RMap g ] - helper a b f g eq (Category.Cat.refl {conv} eq2) = - (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq - (refl-hom {FObj T b} {FObj ( U_K ○ F_K ) b} {conv} ) + helper _ _ _ _ eq (Category.Cat.refl _) = + (Category.IsCategory.o-resp-≈ (Category.isCategory A)) eq refl-hom kfmap : {a b : Obj A} (f : KHom a b) -> Hom B (FObj F_K a) (FObj F_K b) kfmap {_} {b} f = B [ TMap ε_K (FObj F_K b) o FMap F_K (RMap f) ] @@ -633,8 +640,46 @@ ≈⟨⟩ TMap ε_K (FObj F_K c) o FMap F_K (RMap (g * f)) ≈⟨⟩ - TMap ε_K (FObj F_K c) o FMap F_K (RMap (A [ (TMap μ c) o A [ (FMap ( U_K ○ F_K ) (RMap g)) o (RMap f) ] ] )) - ≈⟨ {!!} ⟩ + TMap ε_K (FObj F_K c) o FMap F_K (A [ TMap μ_K c o A [ FMap ( U_K ○ F_K ) (RMap g) o RMap f ] ] ) + ≈⟨ cdr ( distr F_K ) ⟩ + TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o ( FMap F_K (A [ FMap ( U_K ○ F_K ) (RMap g) o RMap f ]))) + ≈⟨ cdr (cdr ( distr F_K )) ⟩ + TMap ε_K (FObj F_K c) o ( FMap F_K (TMap μ_K c) o (( FMap F_K (FMap ( U_K ○ F_K ) (RMap g))) o (FMap F_K (RMap f)))) + ≈⟨ cdr assoc ⟩ + TMap ε_K (FObj F_K c) o ((( FMap F_K (TMap μ_K c) o ( FMap F_K (FMap (U_K ○ F_K) (RMap g))))) o (FMap F_K (RMap f))) + ≈⟨ cdr (car (car ( fcong F_K ( μ=UεF RK )))) ⟩ + TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )) o + ( FMap F_K (FMap (U_K ○ F_K) (RMap g)))) o (FMap F_K (RMap f))) + ≈⟨ sym (cdr assoc) ⟩ + TMap ε_K (FObj F_K c) o (( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) ))) o + (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f)))) + ≈⟨ assoc ⟩ + (TMap ε_K (FObj F_K c) o ( FMap F_K ( FMap U_K ( TMap ε_K ( FObj F_K c ) )))) o + (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f))) + ≈⟨ car (sym (nat ε_K)) ⟩ + (TMap ε_K (FObj F_K c) o ( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)))) o + (( FMap F_K (FMap (U_K ○ F_K) (RMap g))) o (FMap F_K (RMap f))) + ≈⟨ sym assoc ⟩ + TMap ε_K (FObj F_K c) o (( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o + ((( FMap F_K (FMap (U_K ○ F_K) (RMap g)))) o (FMap F_K (RMap f)))) + ≈⟨ cdr assoc ⟩ + TMap ε_K (FObj F_K c) o ((( TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c))) o + (( FMap F_K (FMap (U_K ○ F_K) (RMap g))))) o (FMap F_K (RMap f))) + ≈⟨ cdr ( car ( + begin + TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o ((FMap F_K (FMap (U_K ○ F_K) (RMap g)))) + ≈⟨⟩ + TMap ε_K (FObj (F_K ○ U_K) (FObj F_K c)) o (FMap (F_K ○ U_K) (FMap F_K (RMap g))) + ≈⟨ sym (nat ε_K) ⟩ + ( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b)) + ∎ + )) ⟩ + TMap ε_K (FObj F_K c) o ((( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b))) o FMap F_K (RMap f)) + ≈⟨ cdr (sym assoc) ⟩ + TMap ε_K (FObj F_K c) o (( FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f))) + ≈⟨ assoc ⟩ + (TMap ε_K (FObj F_K c) o FMap F_K (RMap g)) o (TMap ε_K (FObj F_K b) o FMap F_K (RMap f)) + ≈⟨⟩ kfmap g o kfmap f ∎