Home

関手

module category-theory.functor where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.retraction
open import category-theory.category

record FunctorData {o₁ h₁ o₂ h₂}
  (𝒞 : CategoryData o₁ h₁) (𝒟 : CategoryData o₂ h₂)
  : Type (o₁ ⊔ h₁ ⊔ o₂ ⊔ h₂) where
  private module 𝒞 = CategoryData 𝒞
  open CategoryData 𝒟

  field
    F₀ : 𝒞.Ob → Ob
    F₁ : ∀ {A B} → (f : 𝒞.Hom A B)
      → Hom (F₀ A) (F₀ B)

  ₀ = F₀
  ₁ = F₁

module _ {o₁ h₁ o₂ h₂}
  (𝒞 : CategoryData o₁ h₁) (𝒟 : CategoryData o₂ h₂) where
  private module 𝒞 = CategoryData 𝒞
  open CategoryData 𝒟

  functorDataToΣ : FunctorData 𝒞 𝒟
    → Σ[ F₀ ∈ (𝒞.Ob → Ob) ] (∀ {A B} → (f : 𝒞.Hom A B) → Hom (F₀ A) (F₀ B))
  functorDataToΣ F = FunctorData.₀ F , FunctorData.₁ F

  ΣToFunctorData :
    Σ[ F₀ ∈ (𝒞.Ob → Ob) ] (∀ {A B} → (f : 𝒞.Hom A B) → Hom (F₀ A) (F₀ B))
    → FunctorData 𝒞 𝒟
  ΣToFunctorData (F₀ , F₁) = record { F₀ = F₀ ; F₁ = F₁ }

  hasRetractionFunctorDataToΣ : HasRetraction functorDataToΣ
  hasRetractionFunctorDataToΣ .fst = ΣToFunctorData
  hasRetractionFunctorDataToΣ .snd F = refl

record isFunctor {o₁ h₁ o₂ h₂} (𝒞 : Category o₁ h₁) (𝒟 : Category o₂ h₂)
  (F : FunctorData (Category.𝒞 𝒞) (Category.𝒞 𝒟)) : Type (o₁ ⊔ h₁ ⊔ h₂) where
  private module 𝒞 = Category 𝒞
  open Category 𝒟
  open FunctorData F

  field
    preserve-id : ∀ (A : 𝒞.Ob)
      → F₁ (𝒞.id A) ＝ id (F₀ A)
    preserve-∘ : ∀ {A B C} (f : 𝒞.Hom A B) (g : 𝒞.Hom B C)
      → F₁ (g 𝒞.∘ f) ＝ F₁ g ∘ F₁ f

record Functor {o₁ h₁ o₂ h₂} (𝒞 : Category o₁ h₁) (𝒟 : Category o₂ h₂)
  : Type (o₁ ⊔ h₁ ⊔ o₂ ⊔ h₂) where
  field
    F : FunctorData (Category.𝒞 𝒞) (Category.𝒞 𝒟)
    is-functor : isFunctor 𝒞 𝒟 F

  open FunctorData F public
  open isFunctor is-functor public