From 3151fb3e46b8e04c0294f887af6ea43d09fc0867 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 16:35:47 +0100
Subject: [PATCH] Prove propositionality for naturality

---
 src/Cat/Category/NaturalTransformation.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index 12df9ea..525933a 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -58,7 +58,8 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
     NaturalTransformation = Σ Transformation Natural
 
     -- Think I need propPi and that arrows are sets
-    postulate propIsNatural : (θ : _) → isProp (Natural θ)
+    propIsNatural : (θ : _) → isProp (Natural θ)
+    propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
 
     NaturalTransformation≡ : {α β : NaturalTransformation}
       → (eq₁ : α .proj₁ ≡ β .proj₁)