# HG changeset patch # User Shinji KONO # Date 1376505240 -32400 # Node ID 945f26ed12d5a17882ce77c03fc3865f8a7cf789 # Parent 57df6cb8f253b870f19348a765912d64868352de assuing ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g ) diff -r 57df6cb8f253 -r 945f26ed12d5 HomReasoning.agda --- a/HomReasoning.agda Wed Aug 14 22:45:50 2013 +0900 +++ b/HomReasoning.agda Thu Aug 15 03:34:00 2013 +0900 @@ -116,7 +116,7 @@ → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] nat η = IsNTrans.commute ( isNTrans η ) - infixr 2 _∎ + infixr 2 _∎ infixr 2 _≈⟨_⟩_ _≈⟨⟩_ infix 1 begin_ @@ -136,12 +136,20 @@ 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 z : Hom A a b } → + y ≈ x → y IsRelatedTo z → x IsRelatedTo z + _≈↑⟨_⟩_ _ x≈y (relTo y≈z) = relTo (trans-hom (sym x≈y) y≈z) + + infixr 2 _≈↑⟨_⟩_ + _≈⟨⟩_ : { 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 + -- an example Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → diff -r 57df6cb8f253 -r 945f26ed12d5 monoid-monad.agda --- a/monoid-monad.agda Wed Aug 14 22:45:50 2013 +0900 +++ b/monoid-monad.agda Thu Aug 15 03:34:00 2013 +0900 @@ -1,8 +1,7 @@ open import Category -- https://github.com/konn/category-agda -open import Category.Monoid open import Algebra open import Level -module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ} where +module monoid-monad {c c₁ c₂ ℓ : Level} where open import Algebra.Structures open import HomReasoning @@ -13,7 +12,22 @@ open import Relation.Binary.Core open import Relation.Binary -open Monoid +-- open Monoid +open import Algebra.FunctionProperties using (Op₁; Op₂) + + +record ≡-Monoid c : Set (suc c) where + infixl 7 _∙_ + field + Carrier : Set c + _∙_ : Op₂ Carrier + ε : Carrier + isMonoid : IsMonoid _≡_ _∙_ ε + open IsMonoid isMonoid public + +postulate Mono : ≡-Monoid c +open ≡-Monoid + -- T : A → (M x A) @@ -28,7 +42,7 @@ } } where cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} → - Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ] + Sets [ f ≈ g ] → Sets [ map (λ (x : Carrier Mono) → x) f ≈ map (λ (x : Carrier Mono) → x) g ] cong1 _≡_.refl = _≡_.refl open Functor @@ -77,30 +91,35 @@ open NTrans --- Lemma-MM32 : ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( _≈_ Mono f g ) -> ( ( λ x → f x ) ≡ ( λ x → g x ) ) --- Lemma-MM32 eq = cong ( \f -> \x -> f x ) eq - ---cong-≈ : { a b : Carrier Mono } → (f : Carrier Mono -> Carrier Mono ) → --- _≈_ Mono a b → _≈_ Mono (f a) (f b) ---cong-≈ f eq = {!!} - Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) Lemma-MM33 = _≡_.refl -Lemma-M-34 : { x : Carrier Mono } -> _≈_ Mono ((_∙_ Mono (ε Mono) x)) x -Lemma-M-34 {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x +Lemma-MM34 : { x : Carrier Mono } -> ( (Mono ∙ ε Mono) x ≡ x ) +Lemma-MM34 {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x + +Lemma-MM35 : { x : Carrier Mono } -> ((Mono ∙ x) (ε Mono)) ≡ x +Lemma-MM35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid Mono )) ) x -Lemma-M-35 : { x : Carrier Mono } -> _≈_ Mono ((_∙_ Mono x (ε Mono))) x -Lemma-M-35 {x} = ( proj₂ ( IsMonoid.identity ( isMonoid Mono )) ) x +Lemma-MM36 : { x y z : Carrier Mono } -> ((Mono ∙ (Mono ∙ x) y) z) ≡ (_∙_ Mono x (_∙_ Mono y z ) ) +Lemma-MM36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono )) x y z + +-- We cannot prove this ... +-- Lemma-MM38 : ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> (( λ x -> f x) ≡ (λ x -> g x) ) +-- Lemma-MM38 {x} {f} {g} eq = {!!} -Lemma-M-36 : { x y z : Carrier Mono } -> _≈_ Mono (_∙_ Mono (_∙_ Mono x y ) z ) (_∙_ Mono x (_∙_ Mono y z ) ) -Lemma-M-36 {x} {y} {z} = ( IsMonoid.assoc ( isMonoid Mono )) x y z +postulate Lemma-MM39 : ∀{x : Carrier Mono } {f g : Carrier Mono -> Carrier Mono } -> (f x ≡ g x) -> ( f ≡ g ) + +postulate Lemma-MM40 : ∀{x y z : Carrier Mono } {f g : Carrier Mono -> Carrier Mono -> Carrier Mono -> Carrier Mono } -> + (f x y z ≡ g x y z ) -> ( f ≡ g ) -≡-to≈ : { f g : Carrier Mono } -> f ≡ g -> _≈_ Mono f g -≡-to≈ _≡_.refl = IsEquivalence.refl (IsMonoid.isEquivalence (isMonoid Mono ) ) +Lemma-MM9 : ( \(x : Carrier Mono) -> ( Mono ∙ ε Mono ) x ) ≡ ( \(x : Carrier Mono) -> x ) +Lemma-MM9 = Lemma-MM39 Lemma-MM34 -Lemma-M-37 : { a x y : Set } ( f g : Set -> Carrier Mono ) -> ( _≈_ Mono ( f a ) ( g a) ) -> ( f x , y ) ≡ ( g x , y ) -Lemma-M-37 f g eq = ? +Lemma-MM10 : ( \x -> ((Mono ∙ x) (ε Mono))) ≡ ( \x -> x ) +Lemma-MM10 = Lemma-MM39 Lemma-MM35 + +Lemma-MM11 : (\x y z -> ((Mono ∙ (Mono ∙ x) y) z)) ≡ (\x y z -> ( _∙_ Mono x (_∙_ Mono y z ) )) +Lemma-MM11 = Lemma-MM40 Lemma-MM36 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ MonoidMonad = record { @@ -117,7 +136,7 @@ TMap μ a o TMap η ( FObj T a ) ≈⟨⟩ ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x )) - ≈⟨ cong ( \f -> ( \x -> ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl ) ⟩ + ≈⟨ cong ( \f -> ( \x -> ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ ( λ x → (proj₁ x) , proj₂ x ) ≈⟨⟩ ( λ x → x ) @@ -130,7 +149,7 @@ TMap μ a o (FMap T (TMap η a )) ≈⟨⟩ ( λ x → (Mono ∙ proj₁ x) (ε Mono) , proj₂ x ) - ≈⟨ cong ( \f -> ( \x -> ( f (proj₁ x) ) , proj₂ x )) ( _≡_.refl ) ⟩ + ≈⟨ cong ( \f -> ( \x -> ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ ( λ x → (proj₁ x) , proj₂ x ) ≈⟨⟩ ( λ x → x ) @@ -143,8 +162,9 @@ TMap μ a o TMap μ ( FObj T a ) ≈⟨⟩ ( λ x → (Mono ∙ (Mono ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) - -- ≈⟨ (\x -> Lemma-M-36 ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) ⟩ - ≈⟨ {!!} ⟩ + ≈⟨ cong ( \f -> ( \x -> + (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) ) + )) Lemma-MM11 ⟩ ( λ x → (Mono ∙ proj₁ x) ((Mono ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) ≈⟨⟩ TMap μ a o FMap T (TMap μ a)