From cfb7925cb5e973b21c1577b2d1d15928f0f846c5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Tue, 6 Mar 2018 09:45:04 +0100
Subject: [PATCH] Renaming

---
 src/Cat/Category/Monad.agda | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 674fd95..e853fc1 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -264,8 +264,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       module R² = Functor R²
       pureT : Transformation R⁰ R
       pureT A = pure
-      pureTNatural : Natural R⁰ R pureT
-      pureTNatural {A} {B} f = begin
+      pureN : Natural R⁰ R pureT
+      pureN {A} {B} f = begin
         pureT B             ∘ R⁰.func→ f ≡⟨⟩
         pure            ∘ f          ≡⟨ sym (isNatural _) ⟩
         bind (pure ∘ f) ∘ pure       ≡⟨⟩
@@ -273,8 +273,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         R.func→ f       ∘ pureT A        ∎
       joinT : Transformation R² R
       joinT C = join
-      joinTNatural : Natural R² R joinT
-      joinTNatural f = begin
+      joinN : Natural R² R joinT
+      joinN f = begin
         join       ∘ R².func→ f  ≡⟨⟩
         bind 𝟙     ∘ R².func→ f  ≡⟨⟩
         R².func→ f >>> bind 𝟙    ≡⟨⟩
@@ -304,11 +304,11 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
     pureNT : NaturalTransformation R⁰ R
     proj₁ pureNT = pureT
-    proj₂ pureNT = pureTNatural
+    proj₂ pureNT = pureN
 
     joinNT : NaturalTransformation R² R
     proj₁ joinNT = joinT
-    proj₂ joinNT = joinTNatural
+    proj₂ joinNT = joinN
 
     isNaturalForeign : IsNaturalForeign
     isNaturalForeign = begin