Mercurial > hg > Members > kono > Proof > category
changeset 30:98b8431a419b
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 13 Jul 2013 18:12:57 +0900 |
| parents | 87cefecc5663 |
| children | 17b8bafebad7 |
| files | list-nat.agda nat.agda |
| diffstat | 2 files changed, 68 insertions(+), 52 deletions(-) [+] |
line wrap: on
line diff
--- a/list-nat.agda Sat Jul 13 11:46:58 2013 +0900 +++ b/list-nat.agda Sat Jul 13 18:12:57 2013 +0900 @@ -24,6 +24,16 @@ l3 = l1 ++ l2 +data Node {a} ( A : Set a ) : Set a where + leaf : A -> Node A + node : Node A -> Node A -> Node A + +flatten : ∀{n} { A : Set n } -> Node A -> List A +flatten ( leaf a ) = a :: [] +flatten ( node a b ) = flatten a ++ flatten b + +n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c )) + open import Relation.Binary.PropositionalEquality infixr 20 _==_ @@ -61,7 +71,7 @@ module ==-Reasoning {n} (A : Set n ) where infixr 2 _∎ - infixr 2 _==⟨_⟩_ + infixr 2 _==⟨_⟩_ _==⟨⟩_ infix 1 begin_ @@ -77,6 +87,10 @@ x == y → y IsRelatedTo z → x IsRelatedTo z _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z) + _==⟨⟩_ : (x : List A ) {y : List A} + → x IsRelatedTo y → x IsRelatedTo y + _ ==⟨⟩ x≈y = x≈y + _∎ : (x : List A ) → x IsRelatedTo x _∎ _ = relTo reflection @@ -109,8 +123,6 @@ - - --data Bool : Set where -- true : Bool -- false : Bool
--- a/nat.agda Sat Jul 13 11:46:58 2013 +0900 +++ b/nat.agda Sat Jul 13 18:12:57 2013 +0900 @@ -28,25 +28,25 @@ record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) ( F G : Functor D C ) - (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + (TMap : (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 ( Trans a ) ] ≈ C [ (Trans b ) o (FMap F f) ] ] + → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] -- uniqness : {d : Obj D} --- → C [ Trans d ≈ Trans d ] +-- → C [ TMap d ≈ TMap d ] 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 - Trans : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) - isNTrans : IsNTrans domain codomain F G Trans + TMap : (A : Obj domain) → Hom codomain (FObj F A) (FObj G A) + isNTrans : IsNTrans domain codomain F G TMap open NTrans Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} → (μ : 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 ] ] + → A [ A [ FMap G f o TMap μ a ] ≈ A [ TMap μ b o FMap F f ] ] Lemma2 = \n → IsNTrans.naturality ( isNTrans n ) open import Category.Cat @@ -63,9 +63,9 @@ ( μ : NTrans A A (T ○ T) T) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where field - 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) ] + assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] + unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] 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 @@ -83,7 +83,7 @@ { μ : NTrans A A (T ○ T) T } { a : Obj A } → ( M : Monad A T η μ ) - → A [ A [ Trans μ a o Trans μ ( FObj T a ) ] ≈ A [ Trans μ a o FMap T (Trans μ a) ] ] + → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] Lemma3 = \m → IsMonad.assoc ( isMonad m ) @@ -97,7 +97,7 @@ { μ : NTrans A A (T ○ T) T } { a : Obj A } → ( M : Monad A T η μ ) - → A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] Lemma5 = \m → IsMonad.unity1 ( isMonad m ) Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} @@ -106,7 +106,7 @@ { μ : NTrans A A (T ○ T) T } { a : Obj A } → ( M : Monad A T η μ ) - → A [ A [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] + → A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] Lemma6 = \m → IsMonad.unity2 ( isMonad m ) -- T = M x A @@ -126,12 +126,12 @@ -- g ○ f = μ(c) T(g) f 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 [ Trans μ c o A [ FMap T g o f ] ] + join c g f = A [ TMap μ c o A [ FMap T g o f ] ] module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where - open import Relation.Binary.Core renaming ( Trans to Trasn1 ) + open import Relation.Binary.Core _o_ : {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b x o y = A [ x o y ] @@ -181,11 +181,12 @@ nat : { c₁′ c₂′ ℓ′ : Level} (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b} {F G : Functor D A } → (η : NTrans D A F G ) - → FMap G f o Trans η a ≈ Trans η b o FMap F f + → FMap G f o TMap η a ≈ TMap η b o FMap F f nat _ η = IsNTrans.naturality ( isNTrans η ) + infixr 2 _∎ - infixr 2 _≈⟨_⟩_ + infixr 2 _≈⟨_⟩_ _≈⟨⟩_ infix 1 begin_ ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly @@ -194,7 +195,7 @@ data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - relTo : (x≈y : x ≈ y ) → x IsRelatedTo y + relTo : (x≈y : x ≈ y ) → x IsRelatedTo y begin_ : { a b : Obj A } { x y : Hom A a b } → x IsRelatedTo y → x ≈ y @@ -204,6 +205,9 @@ x ≈ y → y IsRelatedTo z → x IsRelatedTo z _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) + _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y + _ ≈⟨⟩ x∼y = x∼y + _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x _∎ _ = relTo refl-hom @@ -235,17 +239,17 @@ ( f : Hom A a ( FObj T b) ) ( m : Monad A T η μ ) ( k : Kleisli A T η μ m) - → A [ join k b (Trans η b) f ≈ f ] + → A [ join k b (TMap η b) f ≈ f ] Lemma7 c T η b f m k = let open ≈-Reasoning (c) μ = mu ( monad k ) in begin - join k b (Trans η b) f + join k b (TMap η b) f ≈⟨ refl-hom ⟩ - c [ Trans μ b o c [ FMap T ((Trans η b)) o f ] ] + c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ - c [ c [ Trans μ b o FMap T ((Trans η b)) ] o f ] + c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ c [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ @@ -261,16 +265,16 @@ ( f : Hom A a ( FObj T b) ) ( m : Monad A T η μ ) ( k : Kleisli A T η μ m) - → A [ join k b f (Trans η a) ≈ f ] + → A [ join k b f (TMap η a) ≈ f ] Lemma8 c T η a b f m k = begin - join k b f (Trans η a) + join k b f (TMap η a) ≈⟨ refl-hom ⟩ - c [ Trans μ b o c [ FMap T f o (Trans η a) ] ] + c [ TMap μ b o c [ FMap T f o (TMap η a) ] ] ≈⟨ cdr ( IsNTrans.naturality ( isNTrans η )) ⟩ - c [ Trans μ b o c [ (Trans η ( FObj T b)) o f ] ] + c [ TMap μ b o c [ (TMap η ( FObj T b)) o f ] ] ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ - c [ c [ Trans μ b o (Trans η ( FObj T b)) ] o f ] + c [ c [ TMap μ b o (TMap η ( FObj T b)) ] o f ] ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩ c [ id (FObj T b) o f ] ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ @@ -294,53 +298,53 @@ Lemma9 A T η μ a b c d f g h m k = begin join k d h (join k c g f) - ≈⟨ refl-hom ⟩ - join k d h ( ( Trans μ c o ( FMap T g o f ) ) ) + ≈⟨⟩ + join k d h ( ( TMap μ c o ( FMap T g o f ) ) ) ≈⟨ refl-hom ⟩ - ( Trans μ d o ( FMap T h o ( Trans μ c o ( FMap T g o f ) ) ) ) + ( TMap μ d o ( FMap T h o ( TMap μ c o ( FMap T g o f ) ) ) ) ≈⟨ cdr ( cdr ( assoc )) ⟩ - ( Trans μ d o ( FMap T h o ( ( Trans μ c o FMap T g ) o f ) ) ) + ( TMap μ d o ( FMap T h o ( ( TMap μ c o FMap T g ) o f ) ) ) ≈⟨ assoc ⟩ --- ( f o ( g o h ) ) = ( ( f o g ) o h ) - ( ( Trans μ d o FMap T h ) o ( (Trans μ c o FMap T g ) o f ) ) + ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) ≈⟨ assoc ⟩ - ( ( ( Trans μ d o FMap T h ) o (Trans μ c o FMap T g ) ) o f ) + ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) ≈⟨ car (sym assoc) ⟩ - ( ( Trans μ d o ( FMap T h o ( Trans μ c o FMap T g ) ) ) o f ) + ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) ≈⟨ car ( cdr (assoc) ) ⟩ - ( ( Trans μ d o ( ( FMap T h o Trans μ c ) o FMap T g ) ) o f ) + ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) ≈⟨ car assoc ⟩ - ( ( ( Trans μ d o ( FMap T h o Trans μ c ) ) o FMap T g ) o f ) + ( ( ( TMap μ d o ( FMap T h o TMap μ c ) ) o FMap T g ) o f ) ≈⟨ car (car ( cdr ( begin - ( FMap T h o Trans μ c ) + ( FMap T h o TMap μ c ) ≈⟨ nat A μ ⟩ - ( Trans μ (FObj T d) o FMap T (FMap T h) ) + ( TMap μ (FObj T d) o FMap T (FMap T h) ) ∎ ))) ⟩ - ( ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) + ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) ≈⟨ car (sym assoc) ⟩ - ( ( Trans μ d o ( ( Trans μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) + ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) ≈⟨ car ( cdr (sym assoc) ) ⟩ - ( ( Trans μ d o ( Trans μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) + ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ - ( ( Trans μ d o ( Trans μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) + ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) ≈⟨ car assoc ⟩ - ( ( ( Trans μ d o Trans μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) + ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) ≈⟨ car ( car ( begin - ( Trans μ d o Trans μ (FObj T d) ) + ( TMap μ d o TMap μ (FObj T d) ) ≈⟨ IsMonad.assoc ( isMonad m) ⟩ - ( Trans μ d o FMap T (Trans μ d) ) + ( TMap μ d o FMap T (TMap μ d) ) ∎ )) ⟩ - ( ( ( Trans μ d o FMap T ( Trans μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) + ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) ≈⟨ car (sym assoc) ⟩ - ( ( Trans μ d o ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) + ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) ≈⟨ sym assoc ⟩ - ( Trans μ d o ( ( FMap T ( Trans μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) + ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ - ( Trans μ d o ( FMap T ( ( ( Trans μ d ) o ( FMap T h o g ) ) ) o f ) ) + ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) ≈⟨ refl-hom ⟩ - join k d ( ( Trans μ d o ( FMap T h o g ) ) ) f + join k d ( ( TMap μ d o ( FMap T h o g ) ) ) f ≈⟨ refl-hom ⟩ join k d ( join k d h g) f ∎ where open ≈-Reasoning (A)