diff --git a/Cubical/Categories/Constructions/BinProduct/More.agda b/Cubical/Categories/Constructions/BinProduct/More.agda
index 815085be..239d645c 100644
--- a/Cubical/Categories/Constructions/BinProduct/More.agda
+++ b/Cubical/Categories/Constructions/BinProduct/More.agda
@@ -12,91 +12,28 @@ open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Functors.Constant
 open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.NaturalTransformation.More
 open import Cubical.Categories.Instances.Functors.More
 
-open import Cubical.Tactics.CategorySolver.Reflection
+open import Cubical.Categories.Constructions.BinProduct
 
 private
   variable
-    ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+    ℓA ℓA' ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
 
 open Category
 open Functor
 
--- helpful decomposition of morphisms used in several proofs
--- about product category
-module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{E : Category ℓE ℓE'} where
-
-  BinMorphDecompL : ∀ {x1 x2} {y1 y2} ((f , g) : (C ×C D) [ (x1 , y1) ,
-                                                            (x2 , y2) ])
-                      → (F : Functor (C ×C D) E)
-                      → (F ⟪ f , g ⟫) ≡
-                           (F ⟪ f , D .id ⟫) ⋆⟨ E ⟩ (F ⟪ C .id , g ⟫)
-  BinMorphDecompL (f , g) F =
-    (F ⟪ f , g ⟫)
-      ≡⟨ (λ i → F ⟪ C .⋆IdR f (~ i), D .⋆IdL g (~ i)⟫) ⟩
-    (F ⟪ f ⋆⟨ C ⟩ C .id , D .id ⋆⟨ D ⟩ g ⟫)
-      ≡⟨ F .F-seq (f , D .id) (C .id , g) ⟩
-    (F ⟪ f , D .id ⟫) ⋆⟨ E ⟩ (F ⟪ C .id , g ⟫) ∎
-
-  BinMorphDecompR : ∀ {x1 x2} {y1 y2} ((f , g) : (C ×C D) [ (x1 , y1) ,
-                                                            (x2 , y2) ])
-                      → (F : Functor (C ×C D) E)
-                      → (F ⟪ f , g ⟫) ≡
-                        (F ⟪ C .id , g ⟫) ⋆⟨ E ⟩ (F ⟪ f , D .id ⟫)
-  BinMorphDecompR (f , g) F =
-    (F ⟪ f , g ⟫)
-      ≡⟨ (λ i → F ⟪ C .⋆IdL f (~ i), D .⋆IdR g (~ i)⟫) ⟩
-    (F ⟪ C .id ⋆⟨ C ⟩ f , g ⋆⟨ D ⟩ D .id ⟫)
-      ≡⟨ F .F-seq (C .id , g) (f , D .id) ⟩
-    (F ⟪ C .id , g ⟫) ⋆⟨ E ⟩ (F ⟪ f , D .id ⟫) ∎
-
-  open NatIso
-  open NatTrans
+module _ (C : Category ℓC ℓC')
+         (D : Category ℓD ℓD') where
+  open Functor
 
-  -- Natural isomorphism in each component yields naturality of bifunctor
-  binaryNatIso : ∀ (F G : Functor (C ×C D) E)
-    → ( βc : (∀ (c : C .ob) →
-           NatIso (((curryF D E {Γ = C}) ⟅ F ⟆) ⟅ c ⟆)
-                  (((curryF D E {Γ = C}) ⟅ G ⟆) ⟅ c ⟆)))
-    → ( βd : (∀ (d : D .ob) →
-           NatIso (((curryFl C E {Γ = D}) ⟅ F ⟆) ⟅ d ⟆)
-                  (((curryFl C E {Γ = D}) ⟅ G ⟆) ⟅ d ⟆)))
-    → ( ∀ ((c , d) : (C ×C D) .ob) →
-        ((βc c .trans .N-ob d) ≡ (βd d .trans .N-ob c)))
-    → NatIso F G
-  binaryNatIso F G βc βd β≡ .trans .N-ob (c , d) = (βc c) .trans .N-ob d
-  binaryNatIso F G βc βd β≡ .trans .N-hom {(c₁ , d₁)} {(c₂ , d₂)} (fc , fd) =
-    ((F ⟪ fc , fd ⟫) ⋆⟨ E ⟩ ((βc c₂) .trans .N-ob d₂))
-      ≡⟨ (λ i →
-        ((BinMorphDecompL (fc , fd) F) (i)) ⋆⟨ E ⟩ ((βc c₂) .trans .N-ob d₂)) ⟩
-    (((F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-      (F ⟪ C .id , fd ⟫)) ⋆⟨ E ⟩ ((βc c₂) .trans .N-ob d₂))
-      ≡⟨ solveCat! E ⟩
-    ((F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-      ((F ⟪ C .id , fd ⟫) ⋆⟨ E ⟩ ((βc c₂) .trans .N-ob d₂)))
-      ≡⟨ (λ i → (F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩ ((βc c₂) .trans .N-hom fd (i))) ⟩
-    ((F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-      (((βc c₂) .trans .N-ob d₁) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫)))
-      ≡⟨ (λ i → (F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-        (((β≡ (c₂ , d₁)) (i)) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫))) ⟩
-    ((F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-      (((βd d₁) .trans .N-ob c₂) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫)))
-      ≡⟨ solveCat! E ⟩
-    (((F ⟪ fc , D .id ⟫) ⋆⟨ E ⟩
-      ((βd d₁) .trans .N-ob c₂)) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫))
-      ≡⟨ (λ i → ((βd  d₁) .trans .N-hom fc (i)) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫)) ⟩
-    ((((βd d₁) .trans .N-ob c₁) ⋆⟨ E ⟩
-      (G ⟪ fc , D .id ⟫)) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫))
-      ≡⟨ solveCat! E ⟩
-    (((βd d₁) .trans .N-ob c₁) ⋆⟨ E ⟩
-      ((G ⟪ fc , D .id ⟫) ⋆⟨ E ⟩ (G ⟪ C .id , fd ⟫)))
-      ≡⟨ (λ i → ((βd d₁) .trans .N-ob c₁) ⋆⟨ E ⟩
-        ((BinMorphDecompL (fc , fd) G) (~ i))) ⟩
-    (((βd  d₁) .trans .N-ob c₁) ⋆⟨ E ⟩ (G ⟪ fc , fd ⟫))
-      ≡⟨ (λ i → (β≡ (c₁ , d₁) (~ i)) ⋆⟨ E ⟩ (G ⟪ fc , fd ⟫)) ⟩
-    (((βc c₁) .trans .N-ob d₁) ⋆⟨ E ⟩ (G ⟪ fc , fd ⟫)) ∎
-  binaryNatIso F G βc βd β≡ .nIso (c , d)  = (βc c) .nIso d
+  module _ (E : Category ℓE ℓE') where
+    ×C-assoc⁻ : Functor ((C ×C D) ×C E) (C ×C (D ×C E))
+    ×C-assoc⁻ .F-ob = λ z → z .fst .fst , z .fst .snd , z .snd
+    ×C-assoc⁻ .F-hom x = x .fst .fst , x .fst .snd , x .snd
+    ×C-assoc⁻ .F-id = refl
+    ×C-assoc⁻ .F-seq f g = refl
 
 module _ (C : Category ℓC ℓC')
          (D : Category ℓD ℓD') where
@@ -112,3 +49,34 @@ module _ (C : Category ℓC ℓC')
   SplitCatIso× f .snd .snd .isIso.inv = f .snd .isIso.inv .snd
   SplitCatIso× f .snd .snd .isIso.sec = cong snd (f .snd .isIso.sec)
   SplitCatIso× f .snd .snd .isIso.ret = cong snd (f .snd .isIso.ret)
+
+private
+  variable
+    A A' : Category ℓA ℓA'
+    B B' : Category ℓB ℓB'
+    C C' : Category ℓC ℓC'
+    D D' : Category ℓD ℓD'
+    F F' : Functor A B
+    G G' : Functor C D
+
+module _ {A : Category ℓA ℓA'}
+    {B : Category ℓB ℓB'}
+    {C : Category ℓC ℓC'}
+    {D : Category ℓD ℓD'}
+    {F F' : Functor A B}
+    {G G' : Functor C D}
+  where
+  open NatTrans
+  NatTrans× :
+    NatTrans F F' → NatTrans G G' →
+    NatTrans (F ×F G) (F' ×F G')
+  NatTrans× α β .N-ob x .fst = α ⟦ x .fst ⟧
+  NatTrans× α β .N-ob x .snd = β ⟦ x .snd ⟧
+  NatTrans× α β .N-hom (f , g) = ΣPathP ((α .N-hom f) , (β .N-hom g))
+
+  open NatIso
+  open isIso
+  NatIso× :
+    NatIso F F' → NatIso G G' → NatIso (F ×F G) (F' ×F G')
+  NatIso× α β .trans = NatTrans× (α .trans) (β .trans)
+  NatIso× α β .nIso (x , y) = CatIso× _ _ (NatIsoAt α x) (NatIsoAt β y) .snd
diff --git a/Cubical/Categories/Displayed/Instances/Arrow/Base.agda b/Cubical/Categories/Displayed/Instances/Arrow/Base.agda
index 8d8b0849..c88038ac 100644
--- a/Cubical/Categories/Displayed/Instances/Arrow/Base.agda
+++ b/Cubical/Categories/Displayed/Instances/Arrow/Base.agda
@@ -65,6 +65,11 @@ module _ {C : Category ℓC ℓC'}
   ArrowReflection Fᴰ = natTrans Fᴰ.F-obᴰ Fᴰ.F-homᴰ
     where module Fᴰ = Section Fᴰ
 
+  arrIntroS : F1 ⇒ F2 → Section (F1 ,F F2) (Arrow C)
+  arrIntroS α = mkPropHomsSection (hasPropHomsArrow C)
+    (NatTrans.N-ob α)
+    (NatTrans.N-hom α)
+
   IsoReflection : ∀ (Fᴰ : Section (F1 ,F F2) (Iso C)) → F1 ≅ᶜ F2
   IsoReflection Fᴰ = record
     { trans = natTrans
@@ -74,6 +79,11 @@ module _ {C : Category ℓC ℓC'}
     }
     where module Fᴰ = Section Fᴰ
 
+  isoIntroS : F1 ≅ᶜ F2 → Section (F1 ,F F2) (Iso C)
+  isoIntroS α = mkPropHomsSection (hasPropHomsIso C)
+    (λ x → NatTrans.N-ob (α .NatIso.trans) x , α .NatIso.nIso x)
+    (λ {x} {y} f → NatTrans.N-hom (α .NatIso.trans) f , tt)
+
 module _ {C : Category ℓC ℓC'}
          {D : Category ℓD ℓD'}
          {F : Functor D (C ×C C)}
diff --git a/Cubical/Categories/Monoidal/Combinators/Base.agda b/Cubical/Categories/Monoidal/Combinators/Base.agda
new file mode 100644
index 00000000..e330ad8b
--- /dev/null
+++ b/Cubical/Categories/Monoidal/Combinators/Base.agda
@@ -0,0 +1,79 @@
+{- Various large associator combinators etc -}
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Monoidal.Base
+module Cubical.Categories.Monoidal.Combinators.Base
+  {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') where
+
+
+import      Cubical.Data.Equality as Eq
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Constructions.BinProduct.More
+open import Cubical.Categories.NaturalTransformation.More hiding (α)
+open import Cubical.Categories.NaturalTransformation.Reind
+
+private
+  module M = MonoidalCategory M
+  variable
+    v w x y z x' x'' x''' x'''' x''''' : M.ob
+
+-- The 3 is the number of ⊗s involved, not objects. This would make α α2
+α2 = M.α
+
+α3⟨_,_,_,_⟩ : ∀ w x y z →
+  M.Hom[ w M.⊗ (x M.⊗ (y M.⊗ z)) , (w M.⊗ (x M.⊗ y)) M.⊗ z ]
+α3⟨ w , x , y , z ⟩ = M.α⟨ w , (x M.⊗ y) , z ⟩ M.∘ (M.id M.⊗ₕ M.α⟨ x , y , z ⟩)
+
+α3⁻¹⟨_,_,_,_⟩ : ∀ w x y z →
+  M.Hom[ (w M.⊗ (x M.⊗ y)) M.⊗ z , w M.⊗ (x M.⊗ (y M.⊗ z)) ]
+α3⁻¹⟨ w , x , y , z ⟩ =
+  (M.id M.⊗ₕ M.α⁻¹⟨ x , y , z ⟩) M.∘ M.α⁻¹⟨ w , x M.⊗ y , z ⟩
+
+α3 : NatIso {C = M.C ×C M.C ×C M.C ×C M.C}{D = M.C}
+  (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─))))
+  ((M.─⊗─ ∘F (M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C) ∘F
+    (𝟙⟨ M.C ⟩ ×F ((M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C)))
+α3 = seqNatIso ((M.─⊗─ ∘ʳⁱ NatIso× (idNatIso 𝟙⟨ M.C ⟩) M.α))
+  (reindNatIso _ _ _ _ (Eq.refl , Eq.refl)
+    ((M.α ∘ˡⁱ (𝟙⟨ M.C ⟩ ×F ((M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C)))))
+
+private
+  testα3 : ∀ {w x y z}
+    → α3⟨ w , x , y , z ⟩ ≡ α3 .NatIso.trans ⟦ w , x , y , z ⟧
+  testα3 = refl
+
+  testα⁻3 : ∀ {w x y z}
+    → α3⁻¹⟨ w , x , y , z ⟩ ≡ α3 .NatIso.nIso (w , x , y , z) .isIso.inv
+  testα⁻3 = refl
+
+α4⟨_,_,_,_,_⟩ : ∀ v w x y z →
+  M.Hom[ v M.⊗ (w M.⊗ (x M.⊗ (y M.⊗ z))) , (v M.⊗ (w M.⊗ (x M.⊗ y))) M.⊗ z ]
+α4⟨ v , w , x , y , z ⟩ =
+  M.α⟨ v , w M.⊗ (x M.⊗ y) , z ⟩
+  M.∘ (M.id M.⊗ₕ α3⟨ w , x , y , z ⟩)
+
+α4⁻¹⟨_,_,_,_,_⟩ : ∀ v w x y z →
+  M.Hom[ (v M.⊗ (w M.⊗ (x M.⊗ y))) M.⊗ z , v M.⊗ (w M.⊗ (x M.⊗ (y M.⊗ z))) ]
+α4⁻¹⟨ v , w , x , y , z ⟩ =
+  M.id M.⊗ₕ α3⁻¹⟨ w , x , y , z ⟩
+  M.∘ M.α⁻¹⟨ v , w M.⊗ (x M.⊗ y) , z ⟩
+
+α4 : NatIso {C = M.C ×C M.C ×C M.C ×C M.C ×C M.C}{D = M.C}
+  (M.─⊗─
+  ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F (M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─))))))
+  ((M.─⊗─ ∘F (M.─⊗─ ×F 𝟙⟨ M.C ⟩) ∘F ×C-assoc M.C M.C M.C) ∘F
+    (𝟙⟨ M.C ⟩ ×F
+     (((((M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)) ∘F ×C-assoc⁻ M.C M.C M.C) ×F
+        𝟙⟨ M.C ⟩)
+       ∘F ×C-assoc (M.C ×C M.C) M.C M.C)
+      ∘F ×C-assoc M.C M.C (M.C ×C M.C))))
+α4 = seqNatIso
+  (((M.─⊗─ ∘ʳⁱ NatIso× (idNatIso 𝟙⟨ M.C ⟩) α3)))
+  (reindNatIso _ _ _ _ (Eq.refl , Eq.refl)
+    (M.α ∘ˡⁱ
+    (𝟙⟨ M.C ⟩
+    ×F ((((M.─⊗─ ∘F (𝟙⟨ M.C ⟩ ×F M.─⊗─)) ∘F ×C-assoc⁻ M.C M.C M.C ) ×F 𝟙⟨ M.C ⟩)
+      ∘F ×C-assoc (M.C ×C M.C) M.C M.C
+      ∘F ×C-assoc M.C M.C (M.C ×C M.C)))))
diff --git a/Cubical/Categories/Monoidal/Combinators/Equations.agda b/Cubical/Categories/Monoidal/Combinators/Equations.agda
new file mode 100644
index 00000000..c2c3ba92
--- /dev/null
+++ b/Cubical/Categories/Monoidal/Combinators/Equations.agda
@@ -0,0 +1,102 @@
+{- Various large associator combinators etc -}
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Monoidal.Base
+module Cubical.Categories.Monoidal.Combinators.Equations
+  where
+
+open import Cubical.Foundations.HLevels
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.NaturalTransformation.More hiding (α)
+open import Cubical.Categories.Monoidal.Functor
+import Cubical.Categories.Monoidal.Combinators.Base as Combinators
+open import Cubical.Categories.Constructions.Free.Monoidal.Base
+open import Cubical.Categories.Constructions.Free.Monoidal.Coherence
+open import Cubical.Data.SumFin
+
+open Category
+open Functor
+private
+  α4⁻¹α-lhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') →
+    ∀ x x' x'' x''' x'''' x'''''
+    → (MonoidalCategory.C M) [ _ , _ ]
+  α4⁻¹α-lhs M x x' x'' x''' x'''' x''''' =
+    MComb.α4⁻¹⟨ x , x' , x'' , x''' , x'''' ⟩ M.⊗ₕ M.id {x'''''}
+    M.∘ M.α⟨ x M.⊗ (x' M.⊗ (x'' M.⊗ x''')) , x'''' , x''''' ⟩
+    where module M = MonoidalCategory M
+          module MComb = Combinators M
+  α4⁻¹α-rhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') →
+    ∀ x x' x'' x''' x'''' x'''''
+    → (MonoidalCategory.C M) [ _ , _ ]
+  α4⁻¹α-rhs M x x' x'' x''' x'''' x''''' =
+    MComb.α4⟨ x , x' , x'' , x''' M.⊗ x'''' , x''''' ⟩
+    M.∘ (M.id M.⊗ₕ (M.id M.⊗ₕ (M.id M.⊗ₕ M.α⟨ x''' , x'''' , x''''' ⟩)))
+    M.∘ MComb.α4⁻¹⟨ x , x' , x'' , x''' , x'''' M.⊗ x''''' ⟩
+    where module M = MonoidalCategory M
+          module MComb = Combinators M
+
+  ηα-lhs ηα-rhs : ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ') →
+    ∀ x x'
+    → (MonoidalCategory.C M) [ _ , _ ]
+  ηα-lhs M x x' = (M.η⟨ x ⟩ M.⊗ₕ M.id {x'}) M.∘ M.α⟨ M.unit , x , x' ⟩
+    where module M = MonoidalCategory M
+  ηα-rhs M x x' = M.η⟨ x M.⊗ x' ⟩
+    where module M = MonoidalCategory M
+
+private
+  F6 = FreeMonoidalCategory (Fin 6)
+  module F6 = MonoidalCategory F6
+
+  x x' x'' x''' x'''' x''''' : F6.ob
+  x = ↑ (fromℕ 0)
+  x' = ↑ (fromℕ 1)
+  x'' = ↑ (fromℕ 2)
+  x''' = ↑ (fromℕ 3)
+  x'''' = ↑ (fromℕ 4)
+  x''''' = ↑ (fromℕ 5)
+  α4⁻¹α-free :
+    α4⁻¹α-lhs F6 x x' x'' x''' x'''' x'''''
+    ≡ α4⁻¹α-rhs F6 x x' x'' x''' x'''' x'''''
+  α4⁻¹α-free = coherence (Fin 6 , isSetFin) _ _
+
+α4⁻¹α :
+  ∀ {ℓ ℓ' : Level} (M : MonoidalCategory ℓ ℓ')
+  → ∀ x x' x'' x''' x'''' x'''''
+  → α4⁻¹α-lhs M x x' x'' x''' x'''' x'''''
+  ≡ α4⁻¹α-rhs M x x' x'' x''' x'''' x'''''
+α4⁻¹α M x x' x'' x''' x'''' x''''' = cong (sem.F .F-hom) α4⁻¹α-free
+  where
+    module M = MonoidalCategory M
+    ı : Fin 6 → M.ob
+    ı (inl _) = x
+    ı (fsuc (inl x₁)) = x'
+    ı (fsuc (fsuc (inl x₁))) = x''
+    ı (fsuc (fsuc (fsuc (inl x₁)))) = x'''
+    ı (fsuc (fsuc (fsuc (fsuc (inl x₁))))) = x''''
+    ı (fsuc (fsuc (fsuc (fsuc (fsuc (inl x₁)))))) = x'''''
+    sem = rec (Fin 6) M ı
+    module sem = StrongMonoidalFunctor sem
+
+private
+  F2 = FreeMonoidalCategory (Fin 2)
+  module F2 = MonoidalCategory F2
+
+  y y' : F2.ob
+  y = ↑ (fromℕ 0)
+  y' = ↑ (fromℕ 1)
+  ηα-free : ηα-lhs F2 y y' ≡ ηα-rhs F2 y y'
+  ηα-free = coherence (Fin 2 , isSetFin) _ _
+
+ηα : ∀ {ℓ ℓ'} (M : MonoidalCategory ℓ ℓ')
+  → ∀ x x'
+  → ηα-lhs M x x' ≡ ηα-rhs M x x'
+ηα M x x' = cong (sem.F .F-hom) ηα-free
+  where
+    module M = MonoidalCategory M
+    ı : Fin 2 → M.ob
+    ı (inl x₁) = x
+    ı (fsuc x₁) = x'
+    sem = rec (Fin 2) M ı
+    module sem = StrongMonoidalFunctor sem
diff --git a/Cubical/Categories/NaturalTransformation/More.agda b/Cubical/Categories/NaturalTransformation/More.agda
index 0491b0e9..7fa44adb 100644
--- a/Cubical/Categories/NaturalTransformation/More.agda
+++ b/Cubical/Categories/NaturalTransformation/More.agda
@@ -6,8 +6,10 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism renaming (iso to iIso)
 open import Cubical.Data.Sigma
+import      Cubical.Data.Equality as Eq
 open import Cubical.Categories.Category renaming (isIso to isIsoC)
 open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Equality
 open import Cubical.Categories.Functor.Properties
 open import Cubical.Categories.Commutativity
 open import Cubical.Categories.Morphism
@@ -96,3 +98,10 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {F G : Functor C D}
          (α : F ≅ᶜ G) where
   NatIsoAt : ∀ x → CatIso D (F ⟅ x ⟆) (G ⟅ x ⟆)
   NatIsoAt x = (N-ob (α .trans) x) , (α .nIso x)
+
+
+_∘ʳⁱ_ : ∀ (K : Functor C D) → {G H : Functor B C} (β : NatIso G H)
+       → NatIso (K ∘F G) (K ∘F H)
+(K ∘ʳⁱ β) .trans = K ∘ʳ (β .trans)
+(K ∘ʳⁱ β) .nIso x = F-Iso {F = K} (β .trans ⟦ x ⟧ , β .nIso x) .snd
+
diff --git a/Cubical/Categories/NaturalTransformation/Reind.agda b/Cubical/Categories/NaturalTransformation/Reind.agda
new file mode 100644
index 00000000..b1b813d5
--- /dev/null
+++ b/Cubical/Categories/NaturalTransformation/Reind.agda
@@ -0,0 +1,61 @@
+
+{-# OPTIONS --safe #-}
+module Cubical.Categories.NaturalTransformation.Reind where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism renaming (iso to iIso)
+open import Cubical.Data.Sigma
+import      Cubical.Data.Equality as Eq
+open import Cubical.Categories.Category renaming (isIso to isIsoC)
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Functor.Equality
+open import Cubical.Categories.Functor.Properties
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.Morphism
+open import Cubical.Categories.Isomorphism
+open import Cubical.Categories.NaturalTransformation.Base
+open import Cubical.Categories.NaturalTransformation.Properties
+
+open import Cubical.Categories.Instances.Functors
+open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Instances.Arrow
+
+private
+  variable
+    ℓA ℓA' ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level
+    ℓ ℓ' ℓ'' : Level
+    B C D E : Category ℓ ℓ'
+
+open Category
+open NatTrans
+open NatIso
+open isIsoC
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
+  open Functor
+  reindNatTrans : (Fl Fr Gl Gr : Functor C D)
+    → FunctorEq (Fl ,F Gl) (Fr ,F Gr)
+    → Fl ⇒ Gl
+    → Fr ⇒ Gr
+  reindNatTrans Fl Fr Gl Gr F≡G α = ArrowReflection
+    (reindS' F≡G (arrIntroS α))
+
+  reindNatIso : (Fl Fr Gl Gr : Functor C D)
+    → FunctorEq (Fl ,F Gl) (Fr ,F Gr)
+    → Fl ≅ᶜ Gl
+    → Fr ≅ᶜ Gr
+  reindNatIso Fl Fr Gl Gr F≡G α = IsoReflection
+    (reindS' F≡G (isoIntroS α))
+
+  eqToNatTrans : {F G : Functor C D}
+    → FunctorEq (F ,F F) (F ,F G) → F ⇒ G
+  eqToNatTrans {F = F}{G = G} F≡G =
+    reindNatTrans F F F G F≡G
+    (idTrans F)
+
+  eqToNatIso : {F G : Functor C D}
+    → FunctorEq (F ,F F) (F ,F G) → F ≅ᶜ G
+  eqToNatIso {F = F}{G = G} F≡G =
+    reindNatIso F F F G F≡G
+    (idNatIso F)