Mercurial > hg > Members > kono > Proof > category
diff nat.agda @ 7:79d9c30e995a
Reasoning
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2013 13:14:54 +0900 |
| parents | b1fd8d8689a9 |
| children | d5e4db7bbe01 |
line wrap: on
line diff
--- a/nat.agda Sat Jul 06 16:28:26 2013 +0900 +++ b/nat.agda Sun Jul 07 13:14:54 2013 +0900 @@ -26,28 +26,28 @@ -- G(a) ----> G(b) -- G(f) -record IsNNAT {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) +record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) ( F G : Functor D C ) - (NAT : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field naturality : {a b : Obj D} {f : Hom D a b} - → C [ C [ ( FMap G f ) o ( NAT a ) ] ≈ C [ (NAT b ) o (FMap F f) ] ] + → C [ C [ ( FMap G f ) o ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] -- uniqness : {d : Obj D} --- → C [ NAT d ≈ NAT d ] +-- → C [ Trans d ≈ Trans d ] -record NNAT {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) +record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field - NAT : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) - isNNAT : IsNNAT domain codomain F G NAT + Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) + isNTrans : IsNTrans domain codomain F G Trans -open NNAT +open NTrans Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} - -> (μ : NNAT A A F G) -> {a b : Obj A} { f : Hom A a b } - -> A [ A [ FMap G f o NAT μ a ] ≈ A [ NAT μ b o FMap F f ] ] -Lemma2 = \n -> IsNNAT.naturality ( isNNAT n ) + -> (μ : NTrans A A F G) -> {a b : Obj A} { f : Hom A a b } + -> A [ A [ FMap G f o Trans μ a ] ≈ A [ Trans μ b o FMap F f ] ] +Lemma2 = \n -> IsNTrans.naturality ( isNTrans n ) open import Category.Cat @@ -59,19 +59,19 @@ record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( T : Functor A A ) - ( η : NNAT A A identityFunctor T ) - ( μ : NNAT A A (T ○ T) T) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where field - assoc : {a : Obj A} -> A [ A [ NAT μ a o NAT μ ( FObj T a ) ] ≈ A [ NAT μ a o FMap T (NAT μ a) ] ] - unity1 : {a : Obj A} -> A [ A [ NAT μ a o NAT η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - unity2 : {a : Obj A} -> A [ A [ NAT μ a o (FMap T (NAT η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + assoc : {a : Obj A} -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] + unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] -record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NNAT A A identityFunctor T) (μ : NNAT A A (T ○ T) T) +record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - eta : NNAT A A identityFunctor T + eta : NTrans A A identityFunctor T eta = η - mu : NNAT A A (T ○ T) T + mu : NTrans A A (T ○ T) T mu = μ field isMonad : IsMonad A T η μ @@ -79,11 +79,11 @@ open Monad Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a : Obj A } -> ( M : Monad A T η μ ) - -> A [ A [ NAT μ a o NAT μ ( FObj T a ) ] ≈ A [ NAT μ a o FMap T (NAT μ a) ] ] + -> A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] Lemma3 = \m -> IsMonad.assoc ( isMonad m ) @@ -93,20 +93,20 @@ Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a : Obj A } -> ( M : Monad A T η μ ) - -> A [ A [ NAT μ a o NAT η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] Lemma5 = \m -> IsMonad.unity1 ( isMonad m ) Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a : Obj A } -> ( M : Monad A T η μ ) - -> A [ A [ NAT μ a o (FMap T (NAT η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + -> A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] Lemma6 = \m -> IsMonad.unity2 ( isMonad m ) -- T = M x A @@ -118,45 +118,79 @@ record Kleisli { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) ( T : Functor A A ) - ( η : NNAT A A identityFunctor T ) - ( μ : NNAT A A (T ○ T) T ) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T ) ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where monad : Monad A T η μ monad = M join : { a b : Obj A } -> ( c : Obj A ) -> ( Hom A b ( FObj T c )) -> ( Hom A a ( FObj T b)) -> Hom A a ( FObj T c ) - join c g f = A [ NAT μ c o A [ FMap T g o f ] ] + join c g f = A [ Trans μ c o A [ FMap T g o f ] ] + +open import Relation.Binary renaming (Trans to Trans1 ) +open import Relation.Binary.Core renaming (Trans to Trans1 ) + +module ≈-Reasoning where + + -- The code in Relation.Binary.EqReasoning cannot handle + -- heterogeneous equalities, hence the code duplication here. + + trans : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } + { x y z : Hom A a b } → + A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ] + trans a b = {!!} -open import Relation.Binary -open import Relation.Binary.Core + infix 2 _∎ + infixr 2 _≈⟨_!_⟩_ + infix 1 begin_ + + data IsRelatedTo {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } ( x y : Hom A a b ) : + Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + relTo : (x≈y : A [ x ≈ y ] ) → IsRelatedTo A x y + + begin_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } { x y : Hom A a b} → + IsRelatedTo A x y → A [ x ≈ y ] + begin relTo x≈y = x≈y + + _≈⟨_!_⟩_ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } + { x y z : Hom A a b } → + A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z + _≈⟨_!_⟩_ = {!!} +-- _ ≈⟨_ x≈y ⟩ relTo y≈z = relTo (trans x≈y y≈z) + + _∎ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x + _∎ _ = relTo {!!} open Kleisli -Lemma7 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} +Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a b : Obj A } { f : Hom A a ( FObj T b) } { M : Monad A T η μ } ( K : Kleisli A T η μ M) - -> A [ join K b (NAT η b) f ≈ f ] -Lemma7 k = {!!} + -> A [ join K b (Trans η b) f ≈ f ] +Lemma7 c k = {!!} + + + Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a b : Obj A } { f : Hom A a ( FObj T b) } { M : Monad A T η μ } ( K : Kleisli A T η μ M) - -> A [ join K b f (NAT η a) ≈ f ] -Lemma8 k = ? + -> A [ join K b f (Trans η a) ≈ f ] +Lemma8 k = {!!} Lemma9 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { T : Functor A A } - { η : NNAT A A identityFunctor T } - { μ : NNAT A A (T ○ T) T } + { η : NTrans A A identityFunctor T } + { μ : NTrans A A (T ○ T) T } { a b c d : Obj A } { f : Hom A a ( FObj T b) } { g : Hom A b ( FObj T c) }