Mercurial > hg > Members > kono > Proof > category

changeset 86:be4e3b073e0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
resosultion
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 27 Jul 2013 21:19:58 +0900
parents 31e1dbbf8800
children 4690953794c4
files cat-utility.agda nat.agda
diffstat 2 files changed, 19 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/cat-utility.agda	Sat Jul 27 17:51:39 2013 +0900
+++ b/cat-utility.agda	Sat Jul 27 21:19:58 2013 +0900
@@ -128,11 +128,19 @@
 --      nat-η     -- same as η but has different types
 
 record Resolution {c₁ c₂ ℓ  c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) ( B : Category c₁ c₂ ℓ ) 
-      { U_R : Functor B A } { F_R : Functor A B }
-      { η : NTrans A A identityFunctor  ( U_R ○ F_R ) }
-      { μ : NTrans A A (  ( U_R ○ F_R ) ○  ( U_R ○ F_R ) )  ( U_R ○ F_R ) }
-      ( M : Monad A  ( U_R ○ F_R ) η μ ) 
-      { ε_R : NTrans B B ( F_R ○ U_R ) identityFunctor } 
-      ( Adj : Adjunction A B U_R F_R η ε_R ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
-   field
-      μ=UεF : {x : Obj A } -> A [ TMap μ x ≈ FMap U_R ( TMap ε_R ( FObj F_R x ) ) ]
+      ( T : Functor A A ) 
+      { η : 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
+           field
+              T=UF  :  T ≃  (UR ○ FR) 
+              μ=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 ]
+
--- a/nat.agda	Sat Jul 27 17:51:39 2013 +0900
+++ b/nat.agda	Sat Jul 27 21:19:58 2013 +0900
@@ -542,8 +542,9 @@
 M_T : Monad  A ( U_T ○ F_T ) nat-η nat-μ 
 M_T = {!!}
 
-Resolution_T : Resolution A KleisliCategory M_T Adj_T 
+Resolution_T : Resolution A KleisliCategory T M U_T F_T Adj_T 
 Resolution_T = record {
+      T=UF  = {!!} ;
       μ=UεF  = {!!}
   }
 
@@ -555,7 +556,7 @@
       { μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } 
       ( MK :  Monad A (U_K ○ F_K) η_K μ_K )
       ( AdjK : Adjunction A B U_K F_K η_K ε_K )
-      ( ResK : Resolution A B MK AdjK )
+      ( ResK : Resolution A B T M AdjK )
   where
 
         kfmap : {!!}