From 73ab4d1836a9dd5cecf5fe4a4be62c3fced7d1e1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 16 Feb 2018 12:46:25 +0100
Subject: [PATCH] Proove identity laws for natural transformations

---
 src/Cat/Categories/Fun.agda | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 610c3ea..ada60d2 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -142,10 +142,21 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
           open IsCategory (isCategory 𝔻)
 
     module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
+      private
+        allNatural = naturalIsProp {F = A} {B}
+        f' = proj₁ f
+        module 𝔻Data = Category 𝔻
+        eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
+        eq-r C = begin
+          𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
+          𝔻 [ f' C ∘ 𝔻Data.𝟙 ]  ≡⟨ proj₁ (𝔻.ident {A} {B}) ⟩
+          f' C ∎
+        eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
+        eq-l C = proj₂ (𝔻.ident {A} {B})
       ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
-      ident-r = {!!}
+      ident-r = lemSig allNatural _ _ (funExt eq-r)
       ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f
-      ident-l = {!!}
+      ident-l = lemSig allNatural _ _ (funExt eq-l)
       :ident:
         : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f
         × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f