Mercurial > hg > Members > kono > Proof > category
comparison src/cokleisli.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 07 Oct 2023 19:43:31 +0900 |
| parents | e01a1d29492b |
| children |
comparison
equal
deleted
inserted
replaced
| 1109:71049ed05151 | 1110:45de2b31bf02 |
|---|---|
| 1 {-# OPTIONS --cubical-compatible --safe #-} | |
| 2 | |
| 1 open import Category | 3 open import Category |
| 2 open import Level | 4 open import Level |
| 3 open import HomReasoning | 5 open import HomReasoning |
| 4 open import cat-utility | 6 open import Definitions |
| 5 | 7 |
| 6 | 8 |
| 7 module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where | 9 module coKleisli { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where |
| 8 | 10 |
| 9 open coMonad | 11 open coMonad |