namespace http://mathhub.info/MitM/core/categories ❚
import base http://mathhub.info/MitM/Foundation ❚

theory Functors : base:?Logic =
	include ?Categories ❙
	theory functor_theory : base:?Logic > 𝒞 : Cat, 𝒟 : Cat ❘ =
		objF : |𝒞| ⟶ |𝒟| ❙
		homF : {A,B} hom A B ⟶ hom (objF A) (objF B) ❘ # ihomF 3 ❙
		axiom_id : {A:|𝒞|} ⊦ ihomF (id A) ≐ id (objF A) ❙
		axiom_comp : {A:|𝒞|,B:|𝒞|,C:|𝒞|}{f : hom A B, g : hom B C} ⊦ ihomF (g ∘ f) ≐ (ihomF g) ∘ (ihomF f) ❙
	❚
	functor = [𝒞:Cat,𝒟:Cat] Mod ☞?Functors/functor_theory 𝒞 𝒟 ❙
	objectF : {𝒞,𝒟} functor 𝒞 𝒟 ⟶ |𝒞| ⟶ |𝒟| ❘ = [𝒞,𝒟][F] F.objF ❘ # objF 3 4 ❙
	morphismF : {𝒞,𝒟} {F :functor 𝒞 𝒟} {A:|𝒞|,B:|𝒞|} hom A B ⟶ hom ((F.objF) A) ((F.objF) B) ❘
	    = [𝒞,𝒟][F][A,B][f] (F.homF) A B f ❘ # homF 3 6 ❙
❚

theory NaturalTransformations : base:?Logic =
    include ?Functors ❙
    theory naturaltransformation_theory > 𝒞 : Cat, 𝒟 : Cat, F : functor 𝒞 𝒟, G : functor 𝒞 𝒟 ❘ =
        alpha : {C: |𝒞|} hom (objF F C) (objF G C) ❙
        axiom_alpha_commutes : {c : |𝒞|, cp : |𝒞|} ⊦ ∀[f:hom c cp]
          (homF G f) ∘ (alpha c) ≐ (alpha cp) ∘ (homF F f) ❘ ❙
    ❚
    naturaltransformation = [𝒞 : Cat, 𝒟 : Cat, F : functor 𝒞 𝒟, G : functor 𝒞 𝒟]
        Mod ☞?NaturalTransformations/naturaltransformation_theory 𝒞 𝒟 F G ❘ # natTrans 3 4 ❙
❚