Move properties about natural transformations to that module

2018-03-23 15:20:26 +01:00 · 2018-03-23 15:20:26 +01:00 · d3864dbae5
parent ef688202a2
commit d3864dbae5
8 changed files with 171 additions and 179 deletions
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@ -9,7 +9,7 @@ open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
 open import Cat.Category.Exponential hiding (_×_ ; product)
-open import Cat.Category.NaturalTransformation
+import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun

 -- The category of categories
@ -155,6 +155,9 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
 -- | The category of categories have expoentntials - and because it has products
 -- it is therefory also cartesian closed.
 module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
+  open Cat.Category.NaturalTransformation ℂ 𝔻
+    renaming (identity to identityNT)
+    using ()
  private
    module ℂ = Category ℂ
    module 𝔻 = Category 𝔻
@ -189,7 +192,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
  module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
    open Σ c renaming (proj₁ to F ; proj₂ to C)

-    ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙
+    ident : fmap {c} {c} (identityNT F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙
    ident = begin
      fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c})        ≡⟨⟩
      fmap {c} {c} (idN F , ℂ.𝟙)               ≡⟨⟩
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@ -5,62 +5,26 @@ open import Cat.Prelude

 open import Cat.Category
 open import Cat.Category.Functor
-open import Cat.Category.NaturalTransformation

 module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
-  module NT = NaturalTransformation ℂ 𝔻
-  open NT public
+  import Cat.Category.NaturalTransformation ℂ 𝔻
+    as NaturalTransformation
+  open NaturalTransformation public hiding (module Properties)
+  open NaturalTransformation.Properties
  private
    module ℂ = Category ℂ
    module 𝔻 = Category 𝔻
-  private
-    module _ {A B C D : Functor ℂ 𝔻} {θNT : NaturalTransformation A B}
-      {ηNT : NaturalTransformation B C} {ζNT : NaturalTransformation C D} where
-      open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat)
-      open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat)
-      open Σ ζNT renaming (proj₁ to ζ ; proj₂ to ζNat)
-      private
-        L : NaturalTransformation A D
-        L = (NT[_∘_] {A} {C} {D} ζNT (NT[_∘_] {A} {B} {C} ηNT θNT))
-        R : NaturalTransformation A D
-        R = (NT[_∘_] {A} {B} {D} (NT[_∘_] {B} {C} {D} ζNT ηNT) θNT)
-        _g⊕f_ = NT[_∘_] {A} {B} {C}
-        _h⊕g_ = NT[_∘_] {B} {C} {D}
-      isAssociative : L ≡ R
-      isAssociative = lemSig (naturalIsProp {F = A} {D})
-        L R (funExt (λ x → 𝔻.isAssociative))

-  private
-    module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
-      allNatural = naturalIsProp {F = A} {B}
-      f' = proj₁ f
-      eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C
-      eq-r C = begin
-        𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩
-        𝔻 [ f' C ∘ 𝔻.𝟙 ]  ≡⟨ 𝔻.rightIdentity ⟩
-        f' C ∎
-      eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C
-      eq-l C = 𝔻.leftIdentity
-      ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
-      ident-r = lemSig allNatural _ _ (funExt eq-r)
-      ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
-      ident-l = lemSig allNatural _ _ (funExt eq-l)
-      isIdentity
-        : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f
-        × (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f
-      isIdentity = ident-l , ident-r
-  -- Functor categories. Objects are functors, arrows are natural transformations.
-  RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  RawFun = record
-    { Object = Functor ℂ 𝔻
-    ; Arrow = NaturalTransformation
-    ; 𝟙 = λ {F} → NT.identity F
-    ; _∘_ = λ {F G H} → NT[_∘_] {F} {G} {H}
-    }
+    -- Functor categories. Objects are functors, arrows are natural transformations.
+    raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
+    RawCategory.Object raw = Functor ℂ 𝔻
+    RawCategory.Arrow  raw = NaturalTransformation
+    RawCategory.𝟙      raw {F} = identity F
+    RawCategory._∘_    raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
+
+    open RawCategory raw
+    open Univalence (λ {A} {B} {f} → isIdentity {F = A} {B} {f})

-  open RawCategory RawFun
-  open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f})
-  private
    module _ (F : Functor ℂ 𝔻) where
      center : Σ[ G ∈ Object ] (F ≅ G)
      center = F , id-to-iso F F refl
@ -126,7 +90,6 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
      univalent[Contr] : isContr (Σ[ G ∈ Object ] (F ≅ G))
      univalent[Contr] = center , isContractible

-  private
    module _ {A B : Functor ℂ 𝔻} where
      module A = Functor A
      module B = Functor B
@ -176,69 +139,67 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
        fromEq : NaturalTransformation A B
        fromEq = coe𝟙 , nat

-  module _ {A B : Functor ℂ 𝔻} where
-    obverse : A ≡ B → A ≅ B
-    obverse p = res
-      where
-      ob  : Arrow A B
-      ob = fromEq p
-      re : Arrow B A
-      re = fromEq (sym p)
-      vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
-      vr = {!!}
-      rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
-      rv = {!!}
-      isInverse : IsInverseOf {A} {B} ob re
-      isInverse = vr , rv
-      iso : Isomorphism {A} {B} ob
-      iso = re , isInverse
-      res : A ≅ B
-      res = ob , iso
+    module _ {A B : Functor ℂ 𝔻} where
+      obverse : A ≡ B → A ≅ B
+      obverse p = res
+        where
+        ob  : Arrow A B
+        ob = fromEq p
+        re : Arrow B A
+        re = fromEq (sym p)
+        vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
+        vr = {!!}
+        rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
+        rv = {!!}
+        isInverse : IsInverseOf {A} {B} ob re
+        isInverse = vr , rv
+        iso : Isomorphism {A} {B} ob
+        iso = re , isInverse
+        res : A ≅ B
+        res = ob , iso

-    reverse : A ≅ B → A ≡ B
-    reverse iso = {!!}
+      reverse : A ≅ B → A ≡ B
+      reverse iso = {!!}

-    ve-re : (y : A ≅ B) → obverse (reverse y) ≡ y
-    ve-re = {!!}
+      ve-re : (y : A ≅ B) → obverse (reverse y) ≡ y
+      ve-re = {!!}

-    re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
-    re-ve = {!!}
+      re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x
+      re-ve = {!!}

-    done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B)
-    done = {!gradLemma obverse reverse ve-re re-ve!}
+      done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {F = A} {B}}) A B)
+      done = {!gradLemma obverse reverse ve-re re-ve!}

-  univalent : Univalent
-  univalent = done
+    -- univalent : Univalent
+    -- univalent = done

-  instance
-    isCategory : IsCategory RawFun
-    isCategory = record
-      { isAssociative = λ {A B C D} → isAssociative {A} {B} {C} {D}
-      ; isIdentity = λ {A B} → isIdentity {A} {B}
-      ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSet {F} {G}
-      ; univalent = univalent
-      }
+    isCategory : IsCategory raw
+    IsCategory.isAssociative isCategory {A} {B} {C} {D} = isAssociative {A} {B} {C} {D}
+    IsCategory.isIdentity    isCategory {A} {B} = isIdentity {A} {B}
+    IsCategory.arrowsAreSets isCategory {F} {G} = naturalTransformationIsSet {F} {G}
+    IsCategory.univalent     isCategory = {!!}

  Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-  Category.raw Fun = RawFun
+  Category.raw        Fun = raw
+  Category.isCategory Fun = isCategory

-module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  private
-    open import Cat.Categories.Sets
-    open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+-- module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+--   private
+--     open import Cat.Categories.Sets
+--     open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')

-    -- Restrict the functors to Presheafs.
-    rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-    rawPresh = record
-      { Object = Presheaf ℂ
-      ; Arrow = NaturalTransformation
-      ; 𝟙 = λ {F} → identity F
-      ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
-      }
-    instance
-      isCategory : IsCategory rawPresh
-      isCategory = Fun.isCategory _ _
+--     -- Restrict the functors to Presheafs.
+--     rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+--     rawPresh = record
+--       { Object = Presheaf ℂ
+--       ; Arrow = NaturalTransformation
+--       ; 𝟙 = λ {F} → identity F
+--       ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
+--       }
+--     instance
+--       isCategory : IsCategory rawPresh
+--       isCategory = Fun.isCategory _ _

-  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
-  Category.raw        Presh = rawPresh
-  Category.isCategory Presh = isCategory
+--   Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+--   Category.raw        Presh = rawPresh
+--   Category.isCategory Presh = isCategory
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@ -23,7 +23,7 @@ module Cat.Category.Monad where
 open import Cat.Prelude
 open import Cat.Category
 open import Cat.Category.Functor as F
-open import Cat.Category.NaturalTransformation
+import Cat.Category.NaturalTransformation
 import Cat.Category.Monad.Monoidal
 import Cat.Category.Monad.Kleisli
 open import Cat.Categories.Fun
@ -33,6 +33,7 @@ module Kleisli = Cat.Category.Monad.Kleisli

 -- | The monoidal- and kleisli presentation of monads are equivalent.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Cat.Category.NaturalTransformation ℂ ℂ
  private
    module ℂ = Category ℂ
    open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
@ -171,8 +172,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
      Req : M.RawMonad.R (backRaw (forth m)) ≡ R
      Req = Functor≡ rawEq

-      open NaturalTransformation ℂ ℂ
-
      pureTEq : M.RawMonad.pureT (backRaw (forth m)) ≡ pureT
      pureTEq = funExt (λ X → refl)

--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@ -8,11 +8,11 @@ open import Cat.Prelude

 open import Cat.Category
 open import Cat.Category.Functor as F
-open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun

 -- "A monad in the Kleisli form" [voe]
 module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+open import Cat.Category.NaturalTransformation ℂ ℂ hiding (propIsNatural)
 private
  ℓ = ℓa ⊔ ℓb
  module ℂ = Category ℂ
@ -116,8 +116,6 @@ record IsMonad (raw : RawMonad) : Set ℓ where
  Functor.isFunctor R = isFunctorR

  private
-    open NaturalTransformation ℂ ℂ
-
    R⁰ : EndoFunctor ℂ
    R⁰ = Functors.identity
    R² : EndoFunctor ℂ
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/src/Cat/Category/Monad/Monoidal.agda
@ -8,7 +8,6 @@ open import Cat.Prelude

 open import Cat.Category
 open import Cat.Category.Functor as F
-open import Cat.Category.NaturalTransformation
 open import Cat.Categories.Fun

 module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
@ -18,7 +17,7 @@ private
  ℓ = ℓa ⊔ ℓb

 open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
-open NaturalTransformation ℂ ℂ
+open import Cat.Category.NaturalTransformation ℂ ℂ
 record RawMonad : Set ℓ where
  field
    R      : EndoFunctor ℂ
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@ -9,17 +9,17 @@ open import Function

 open import Cat.Category
 open import Cat.Category.Functor as F
-open import Cat.Category.NaturalTransformation
+import Cat.Category.NaturalTransformation
 open import Cat.Category.Monad
 open import Cat.Categories.Fun
 open import Cat.Equivalence

 module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
+  open Cat.Category.NaturalTransformation ℂ ℂ
  private
    ℓ = ℓa ⊔ ℓb
    module ℂ = Category ℂ
    open ℂ using (Object ; Arrow)
-    open NaturalTransformation ℂ ℂ
    module M = Monoidal ℂ
    module K = Kleisli  ℂ

--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@ -18,8 +18,6 @@
 --
 -- * A composition operator.
 {-# OPTIONS --allow-unsolved-metas --cubical #-}
-module Cat.Category.NaturalTransformation where
-
 open import Cat.Prelude

 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
@ -29,77 +27,79 @@ open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Wishlist

-module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
+module Cat.Category.NaturalTransformation
+  {ℓc ℓc' ℓd ℓd' : Level}
  (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where

-  open Category using (Object ; 𝟙)
+open Category using (Object ; 𝟙)
+private
+  module ℂ = Category ℂ
+  module 𝔻 = Category 𝔻
+
+module _ (F G : Functor ℂ 𝔻) where
  private
-    module ℂ = Category ℂ
-    module 𝔻 = Category 𝔻
+    module F = Functor F
+    module G = Functor G
+  -- What do you call a non-natural tranformation?
+  Transformation : Set (ℓc ⊔ ℓd')
+  Transformation = (C : Object ℂ) → 𝔻 [ F.omap C , G.omap C ]

-  module _ (F G : Functor ℂ 𝔻) where
-    private
-      module F = Functor F
-      module G = Functor G
-    -- What do you call a non-natural tranformation?
-    Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : Object ℂ) → 𝔻 [ F.omap C , G.omap C ]
+  Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
+  Natural θ
+    = {A B : Object ℂ}
+    → (f : ℂ [ A , B ])
+    → 𝔻 [ θ B ∘ F.fmap f ] ≡ 𝔻 [ G.fmap f ∘ θ A ]

-    Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
-    Natural θ
-      = {A B : Object ℂ}
-      → (f : ℂ [ A , B ])
-      → 𝔻 [ θ B ∘ F.fmap f ] ≡ 𝔻 [ G.fmap f ∘ θ A ]
+  NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
+  NaturalTransformation = Σ Transformation Natural

-    NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
-    NaturalTransformation = Σ Transformation Natural
+  -- Think I need propPi and that arrows are sets
+  propIsNatural : (θ : _) → isProp (Natural θ)
+  propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i

-    -- Think I need propPi and that arrows are sets
-    propIsNatural : (θ : _) → isProp (Natural θ)
-    propIsNatural θ x y i {A} {B} f = 𝔻.arrowsAreSets _ _ (x f) (y f) i
+  NaturalTransformation≡ : {α β : NaturalTransformation}
+    → (eq₁ : α .proj₁ ≡ β .proj₁)
+    → α ≡ β
+  NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq

-    NaturalTransformation≡ : {α β : NaturalTransformation}
-      → (eq₁ : α .proj₁ ≡ β .proj₁)
-      → α ≡ β
-    NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
+identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
+identityTrans F C = 𝟙 𝔻

-  identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
-  identityTrans F C = 𝟙 𝔻
+identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
+identityNatural F {A = A} {B = B} f = begin
+  𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
+  𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ 𝔻.leftIdentity ⟩
+  F→ f                            ≡⟨ sym 𝔻.rightIdentity ⟩
+  𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
+  𝔻 [ F→ f ∘ identityTrans F A ]  ∎
+  where
+    module F = Functor F
+    F→ = F.fmap

-  identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
-  identityNatural F {A = A} {B = B} f = begin
-    𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
-    𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ 𝔻.leftIdentity ⟩
-    F→ f                            ≡⟨ sym 𝔻.rightIdentity ⟩
-    𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
-    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
-    where
-      module F = Functor F
-      F→ = F.fmap
+identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
+identity F = identityTrans F , identityNatural F

-  identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
-  identity F = identityTrans F , identityNatural F
+module _ {F G H : Functor ℂ 𝔻} where
+  private
+    module F = Functor F
+    module G = Functor G
+    module H = Functor H
+  T[_∘_] : Transformation G H → Transformation F G → Transformation F H
+  T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]

-  module _ {F G H : Functor ℂ 𝔻} where
-    private
-      module F = Functor F
-      module G = Functor G
-      module H = Functor H
-    T[_∘_] : Transformation G H → Transformation F G → Transformation F H
-    T[ θ ∘ η ] C = 𝔻 [ θ C ∘ η C ]
-
-    NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
-    proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
-    proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
-      𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ]     ≡⟨⟩
-      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
-      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
-      𝔻 [ θ B ∘ 𝔻 [ G.fmap f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
-      𝔻 [ 𝔻 [ θ B ∘ G.fmap f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
-      𝔻 [ 𝔻 [ H.fmap f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
-      𝔻 [ H.fmap f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
-      𝔻 [ H.fmap f ∘ T[ θ ∘ η ] A ]     ∎
+  NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
+  proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
+  proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
+    𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ]     ≡⟨⟩
+    𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
+    𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
+    𝔻 [ θ B ∘ 𝔻 [ G.fmap f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
+    𝔻 [ 𝔻 [ θ B ∘ G.fmap f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
+    𝔻 [ 𝔻 [ H.fmap f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
+    𝔻 [ H.fmap f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
+    𝔻 [ H.fmap f ∘ T[ θ ∘ η ] A ]     ∎

+module Properties where
  module _ {F G : Functor ℂ 𝔻} where
    transformationIsSet : isSet (Transformation F G)
    transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C)   (λ l → q l C) i j
@ -118,3 +118,31 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}

    naturalTransformationIsSet : isSet (NaturalTransformation F G)
    naturalTransformationIsSet = sigPresSet transformationIsSet naturalIsSet
+
+  module _
+    {F G H I : Functor ℂ 𝔻}
+    {θ : NaturalTransformation F G}
+    {η : NaturalTransformation G H}
+    {ζ : NaturalTransformation H I} where
+    -- isAssociative : NT[ ζ ∘ NT[ η ∘ θ ] ] ≡ NT[ NT[ ζ ∘ η ] ∘ θ ]
+    isAssociative
+      : NT[_∘_] {F} {H} {I} ζ (NT[_∘_] {F} {G} {H} η θ)
+      ≡ NT[_∘_] {F} {G} {I} (NT[_∘_] {G} {H} {I} ζ η) θ
+    isAssociative
+      = lemSig (naturalIsProp {F = F} {I}) _ _
+        (funExt (λ _ → 𝔻.isAssociative))
+
+  module _ {F G : Functor ℂ 𝔻} {θNT : NaturalTransformation F G} where
+    private
+      propNat = naturalIsProp {F = F} {G}
+
+    rightIdentity : (NT[_∘_] {F} {F} {G} θNT (identity F)) ≡ θNT
+    rightIdentity = lemSig propNat _ _ (funExt (λ _ → 𝔻.rightIdentity))
+
+    leftIdentity : (NT[_∘_] {F} {G} {G} (identity G) θNT) ≡ θNT
+    leftIdentity = lemSig propNat _ _ (funExt (λ _ → 𝔻.leftIdentity))
+
+    isIdentity
+      : (NT[_∘_] {F} {G} {G} (identity G) θNT) ≡ θNT
+      × (NT[_∘_] {F} {F} {G} θNT (identity F)) ≡ θNT
+    isIdentity = leftIdentity , rightIdentity
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@ -6,8 +6,11 @@ open import Cat.Prelude

 open import Cat.Category
 open import Cat.Category.Functor
+open import Cat.Category.NaturalTransformation
+  renaming (module Properties to F)
+  using ()

-open import Cat.Categories.Fun
+open import Cat.Categories.Fun using (module Fun)
 open import Cat.Categories.Sets hiding (presheaf)

 -- There is no (small) category of categories. So we won't use _⇑_ from
@ -47,10 +50,11 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
    open RawFunctor rawYoneda hiding (fmap)

    isIdentity : IsIdentity
-    isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq
+    isIdentity {c} = lemSig prp _ _ eq
      where
      eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c)
      eq = funExt λ A → funExt λ B → ℂ.leftIdentity
+      prp = F.naturalIsProp _ _ {F = presheaf c} {presheaf c}

    isDistributive : IsDistributive
    isDistributive {A} {B} {C} {f = f} {g}