fredefox
/
cat
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update cubical

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-07 16:24:43 +01:00
parent 50f51db4fc
commit 19103e1678
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/cubical

@ -1 +1 @@
Subproject commit 159c519936afcfb72afe5c1528637dd0f0a7303a
Subproject commit 2fa05f70edfc59f205be9af2227996bdd6084948

2
src/Cat/Category/Monad.agda
View File

@ -759,7 +759,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
Monoidal→Kleisli = proj₁ Monoidal≃Kleisli
Kleisli→Monoidal : K.Monad → M.Monad
Kleisli→Monoidal = reverse Monoidal≃Kleisli
Kleisli→Monoidal = inverse Monoidal≃Kleisli
forth : voe-2-3-1 → voe-2-3-2
forth = voe-2-3-2-fromMonad ∘f Monoidal→Kleisli ∘f voe-2-3-1.toMonad