Mercurial > hg > Members > kono > Proof > category
changeset 1123:b6ab443f7a43
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Jul 2024 17:05:16 +0900 |
parents | 47694f2bcd7f |
children | f683d96fbc93 |
files | src/monad→monoidal.agda |
diffstat | 1 files changed, 25 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/monad→monoidal.agda Sun Jul 07 13:54:12 2024 +0900 +++ b/src/monad→monoidal.agda Sun Jul 07 17:05:16 2024 +0900 @@ -116,10 +116,33 @@ proj1 = proj₁ proj2 : {a : Obj Sets} → _*_ {l} {l} One a → a proj2 = proj₂ + import HomReasoning + -- open ≈-Reasoning (Sets {l}) as HR idrφ : {a : Obj Sets } { x : FObj T a } → FMap T (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x - idrφ {a} {x} = ? + idrφ {a} {x} = begin + FMap T (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡⟨ cong (λ f → FMap T (Iso.≅→ (mρ-iso isM)) (TMap μ _ f)) ( begin + FMap T (λ f → FMap T (λ g → f , g) unit) x ≡⟨ fcong x (λ g → nat η _ ) ⟩ + FMap T (λ z → TMap η (Σ a (λ v → One)) (z , OneObj)) x ≡⟨ fdistr x ⟩ + FMap T ( TMap η(a * One )) (FMap T ( λ f → ( f , OneObj )) x ) ∎ ) ⟩ + FMap T proj1 ( TMap μ (a * One ) (FMap T ( TMap η(a * One )) (FMap T ( λ f → ( f , OneObj )) x ))) + ≡⟨ cong (λ f → FMap T proj₁ f) (IsMonad.unity2 isMonad _ ) ⟩ + FMap T proj₁ (id1 Sets (FObj T (a * One)) (FMap T (λ f → f , OneObj) x)) ≡⟨ fcong _ (λ f → ≈-Reasoning.idL Sets x ) ⟩ + FMap T proj₁ (FMap T (λ f → f , OneObj) x) ≡⟨ sym (fdistr x) ⟩ + FMap T ( id1 Sets a) x ≡⟨ IsFunctor.identity (isFunctor T) x ⟩ + id1 Sets (FObj T a) x ≡⟨ refl ⟩ + x ∎ idlφ : {a : Obj Sets } { x : FObj T a } → FMap T (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x - idlφ {a} {x} = ? + idlφ {a} {x} = begin + FMap T (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡⟨ cong (λ f → FMap T (Iso.≅→ (mλ-iso isM)) (TMap μ _ f)) ( begin + FMap T (λ f → FMap T (λ g → f , g) x) unit ≡⟨ nat η _ ⟩ + TMap η (FObj T (Σ One (λ _ → a))) (FMap T (λ f → OneObj , f) x) ∎ ) ⟩ + FMap T proj₂ (TMap μ (One * a) (TMap η (FObj T (Σ One (λ _ → a))) (FMap T (λ f → OneObj , f) x))) + ≡⟨ cong (λ f → FMap T proj₂ f) (IsMonad.unity1 isMonad _ ) ⟩ + FMap T proj₂ (id1 Sets (FObj T (One * a)) (FMap T (λ f → OneObj , f) x)) ≡⟨ fcong _ (λ f → ≈-Reasoning.idR Sets x ) ⟩ + FMap T proj₂ (FMap T (λ f → OneObj , f) x) ≡⟨ sym (fdistr x) ⟩ + FMap T ( id1 Sets a) x ≡⟨ IsFunctor.identity (isFunctor T) x ⟩ + id1 Sets (FObj T a) x ≡⟨ refl ⟩ + x ∎ Monad→Applicative : {l : Level } (m : Monad (Sets {l} ) ) → Applicative ( Monad.T m ) Monad→Applicative {l} monad = record {