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

Make private

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-06 10:06:45 +01:00
parent 4de27aa06c
commit 0cebe1e866
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Cat/Category/Monad.agda
View file

@ -377,8 +377,9 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
IsMonad.isDistributive (propIsMonad raw x y i)
= propIsDistributive raw (isDistributive x) (isDistributive y) i
module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
private
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
eqIsMonad = lemPropF propIsMonad eq
Monad≡ : m ≡ n
Monad.raw (Monad≡ i) = eq i