Mercurial > hg > Members > kono > Proof > category
diff nat.agda @ 97:2feec58bb02d
seprate comparison functor
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 29 Jul 2013 15:54:58 +0900 |
| parents | 85425bd12835 |
| children | e763efd30868 |
line wrap: on
line diff
--- a/nat.agda Mon Jul 29 14:47:57 2013 +0900 +++ b/nat.agda Mon Jul 29 15:54:58 2013 +0900 @@ -580,139 +580,4 @@ μ=UεF = Lemma12 } - -module comparison-functor {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) - { U_K : Functor B A } { F_K : Functor A B } - { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } - { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } - { μ_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 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 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 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 a b f {_} {_} ((hoge (T=UF RK)) (id1 A b)) - - 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 {a} {b} f = KtoT a b 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 ((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 _ _ _ _ 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) ] - - open Adjunction - K_T : Functor KleisliCategory B - K_T = record { - FObj = FObj F_K - ; FMap = kfmap - ; isFunctor = record - { ≈-cong = ≈-cong - ; identity = identity - ; distr = distr1 - } - } where - identity : {a : Obj A} → B [ kfmap (K-id {a}) ≈ id1 B (FObj F_K a) ] - identity {a} = let open ≈-Reasoning (B) in - begin - kfmap (K-id {a}) - ≈⟨⟩ - TMap ε_K (FObj F_K a) o FMap F_K (RMap (K-id {a})) - ≈⟨⟩ - TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) - ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ - id1 B (FObj F_K a) - ∎ - ≈-cong : {a b : Obj A} -> {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] - ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in - begin - kfmap f - ≈⟨⟩ - TMap ε_K (FObj F_K b) o FMap F_K (RMap f) - ≈⟨ cdr ( fcong F_K (RMap-cong f≈g)) ⟩ - TMap ε_K (FObj F_K b) o FMap F_K (RMap g) - ≈⟨⟩ - kfmap g - ∎ - distr1 : {a b c : Obj A} {f : KHom a b} {g : KHom b c} → B [ kfmap (g * f) ≈ (B [ kfmap g o kfmap f ] )] - distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in - begin - kfmap (g * f) - ≈⟨⟩ - TMap ε_K (FObj F_K c) o FMap F_K (RMap (g * 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 - ∎ - +-- end