From b86ee9dfa6029c9f46e90efd191c97c2c76fb9c7 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sun, 19 Apr 2015 16:03:52 -0400
Subject: [PATCH] feat(precategory): add composition of nat. trans. with
 functor

---
 hott/algebra/precategory/iso.hlean       |  2 +-
 hott/algebra/precategory/nat_trans.hlean | 22 +++++++++++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 9c59835e9..23866a458 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -150,7 +150,7 @@ namespace iso
   namespace iso
     attribute to_hom [coercion]
 
-    definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
+    protected definition MK (f : a ⟶ b) (g : b ⟶ a) (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
     @mk _ _ _ _ f (is_iso.mk H1 H2)
 
     definition to_inv (f : a ≅ b) : b ⟶ a :=
diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean
index 5f7bed90d..c1310ccde 100644
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@@ -15,7 +15,7 @@ structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
 namespace nat_trans
 
   infixl `⟹`:25 := nat_trans -- \==>
-  variables {C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E}
+  variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E}
 
   attribute natural_map [coercion]
 
@@ -108,6 +108,26 @@ namespace nat_trans
     : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
   nat_trans_eq_mk (λc, (naturality θ (η c))⁻¹)
 
+  definition fn_n_distrib (F' : D ⇒ E) (η : G ⟹ H) (θ : F ⟹ G)
+    : F' ∘fn (η ∘n θ) = (F' ∘fn η) ∘n (F' ∘fn θ) :=
+  nat_trans_eq_mk (λc, !respect_comp)
+
+  definition n_nf_distrib (η : G ⟹ H) (θ : F ⟹ G) (F' : B ⇒ C)
+    : (η ∘n θ) ∘nf F' = (η ∘nf F') ∘n (θ ∘nf F') :=
+  nat_trans_eq_mk (λc, idp)
+
+  definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = nat_trans.id :=
+  nat_trans_eq_mk (λc, !respect_id)
+
+  definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = nat_trans.id :=
+  nat_trans_eq_mk (λc, idp)
+
+  definition id_fn (η : G ⟹ H) (c : C) : (functor.id ∘fn η) c = η c :=
+  idp
+
+  definition nf_id (η : G ⟹ H) (c : C) : (η ∘nf functor.id) c = η c :=
+  idp
+
   definition nat_trans_of_eq [reducible] (p : F = G) : F ⟹ G :=
   nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
                (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))