Home

関手の合成

module category-theory.composition-of-functors where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.proposition
open import foundations.groupoid-laws
open import foundations.function
open import foundations.functions-are-functors
open import foundations.function-extensionality
open import category-theory.category
open import category-theory.functor
open import category-theory.functor-identity

private variable o h : Level

idFunctorData : ∀ (𝒞 : CategoryData o h) → FunctorData 𝒞 𝒞
idFunctorData _ = record
  { F₀ = λ A → A
  ; F₁ = λ f → f
  }

idFunctor : ∀ (𝒞 : Category o h) → Functor 𝒞 𝒞
idFunctor 𝒞 = record
  { F = idFunctorData (Category.𝒞 𝒞)
  ; is-functor = record
    { preserve-id = λ A → refl
   ; preserve-∘ = λ f g → refl
   }
 }

private variable 𝒞′ 𝒟′ ℰ′ : CategoryData o h

-- Judgmentally associativeなので左結合にする。
infixl 30 _∘FData_

_∘FData_ : FunctorData 𝒟′ ℰ′ → FunctorData 𝒞′ 𝒟′ → FunctorData 𝒞′ ℰ′
G ∘FData F = record
  { F₀ = G.₀ ∘ F.₀
  ; F₁ = G.₁ ∘ F.₁
  }
  where
    module F = FunctorData F
    module G = FunctorData G

private variable
  𝒞 𝒟 ℰ ℱ : Category o h

isFunctor-∘FData : ∀ (F : Functor 𝒞 𝒟) (G : Functor 𝒟 ℰ)
  → isFunctor 𝒞 ℰ (Functor.F G ∘FData Functor.F F)
isFunctor-∘FData F G = record
  { preserve-id = λ A → ap G.₁ (F.preserve-id A) ∙ G.preserve-id _
  ; preserve-∘ = λ f g → (ap G.₁ (F.preserve-∘ f g)) ∙ G.preserve-∘ _ _
  }
  where
    module F = Functor F
    module G = Functor G

-- Judgmentally associativeではないのでinfixにする。
infix 30 _∘F_

_∘F_ : Functor 𝒟 ℰ → Functor 𝒞 𝒟 → Functor 𝒞 ℰ
G ∘F F = record
  { F = G.F ∘FData F.F
  ; is-functor = isFunctor-∘FData F G
  }
  where
    module F = Functor F
    module G = Functor G

lunit-∘F : FunExtAll → (F : Functor 𝒞 𝒟) → idFunctor 𝒟 ∘F F ＝ F
lunit-∘F e F = toFunctorId e _ _ _ F refl

runit-∘F : FunExtAll → (F : Functor 𝒞 𝒟) → F ∘F idFunctor 𝒞 ＝ F
runit-∘F e F = toFunctorId e _ _ _ F refl

assoc-∘F : FunExtAll
  → (F : Functor 𝒞 𝒟)
  → (G : Functor 𝒟 ℰ)
  → (H : Functor ℰ ℱ)
  → (H ∘F G) ∘F F ＝ H ∘F (G ∘F F)
assoc-∘F e F G H = toFunctorId e _ _ _ _ refl