1 files changed, 77 insertions, 0 deletions
diff --git a/Functor/Properties.agda b/Functor/Properties.agda
new file mode 100644
index 0000000..1bd3ba6
--- /dev/null
+++ b/Functor/Properties.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Functor.Properties where
+
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+
+open import Categories.Category using (Category; _[_,_])
+open import Level using (Level)
+open import Categories.Morphism.Notation using (_[_≅_])
+open import Categories.Morphism using (_≅_)
+open import Categories.Functor using (Functor)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
+open import Data.Product using (Σ-syntax; _,_)
+
+module _
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    {𝒟 : Category o′ ℓ′ e′}
+  where
+
+  module 𝒞 = Category 𝒞
+  module 𝒟 = Category 𝒟
+
+  define-by-pw-iso
+      : (F : Functor 𝒞 𝒟)
+        (G₀ : 𝒞.Obj → 𝒟.Obj)
+      → (let module F = Functor F)
+      → ((X : 𝒞.Obj) → 𝒟 [ F.₀ X ≅ G₀ X ])
+      → Σ[ G ∈ Functor 𝒞 𝒟 ] F ≃ G
+  define-by-pw-iso F G₀ α = G , F≃G
+    where
+      open Functor
+      module F = Functor F
+      open 𝒟
+      open _≅_
+      open HomReasoning
+      open ⇒-Reasoning 𝒟
+
+      G-homo
+          : {X Y Z : 𝒞.Obj}
+          → (f : 𝒞 [ X , Y ])
+          → (g : 𝒞 [ Y , Z ])
+          → from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X)
+          ≈ (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X)
+      G-homo {X} {Y} {Z} f g = begin
+          from (α Z) ∘ F.₁ (g 𝒞.∘ f) ∘ to (α X)                           ≈⟨ extendʳ (pushʳ F.homomorphism) ⟩
+          (from (α Z) ∘ F.₁ g) ∘ F.₁ f ∘ to (α X)                         ≈⟨ extendˡ (pushˡ (insertʳ (isoˡ (α Y)))) ⟩
+          (from (α Z) ∘ F.₁ g ∘ to (α Y)) ∘ from (α Y) ∘ F.₁ f ∘ to (α X) ∎
+
+      G-resp-≈
+        : {X Y : 𝒞.Obj}
+        → {f g : 𝒞 [ X , Y ]}
+        → f 𝒞.≈ g
+        → from (α Y) ∘ F.₁ f ∘ to (α X)
+        ≈ from (α Y) ∘ F.₁ g ∘ to (α X)
+      G-resp-≈ f≈g = refl⟩∘⟨ F.F-resp-≈ f≈g ⟩∘⟨refl
+
+      G-identity : {X : 𝒞.Obj} → from (α X) ∘ F.₁ 𝒞.id ∘ to (α X) ≈ id
+      G-identity {X} = refl⟩∘⟨ (F.identity ⟩∘⟨refl ○ identityˡ) ○ isoʳ (α X)
+
+      G : Functor 𝒞 𝒟
+      G .F₀ = G₀
+      G .F₁ {X} {Y} f = from (α Y) ∘ F.₁ f ∘ to (α X)
+      G .identity {X} = G-identity
+      G .homomorphism {f = f} {g} = G-homo f g
+      G .F-resp-≈ = G-resp-≈
+
+      commute : {X Y : 𝒞.Obj} (f : 𝒞 [ X , Y ]) → from (α Y) ∘ F.F₁ f ≈ (from (α Y) ∘ F.₁ f ∘ to (α X)) ∘ from (α X)
+      commute {X} {Y} f = pushʳ (insertʳ (isoˡ (α X)))
+
+      F≃G : F ≃ G
+      F≃G = niHelper record
+          { η = λ X → from (α X)
+          ; η⁻¹ = λ X → to (α X)
+          ; commute = commute
+          ; iso = λ X → iso (α X)
+          }