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

theory Categories : base:?Logic =
    include ☞base:?InformalProofs ❙

	theory category_theory : base:?Logic =
		universe : 𝒰 10 ❘ # U ❙
		hom : U ⟶ U ⟶ 𝒰 10 ❘ # ihom 1 2 ❙
		comp : {a,b,c:U} ihom a b ⟶ ihom b c ⟶ ihom a c ❘ # 5 ∘m 4 ❙
	    identity: {a:U} ihom a a ❘ # iid %I1 ❙
		axiom_assoc : {a,b,c,d:U} ⊦ ∀[f:ihom a b] ∀[g:ihom b c] ∀[h:ihom c d] h ∘m (g ∘m f) ≐ (h ∘m g) ∘m f ❙
		axiom_id_r : {x:U,a:U} ⊦ ∀[f:ihom a x] f ∘m iid ≐ f ❙
		axiom_id_l : {x:U,a:U} ⊦ ∀[f:ihom x a] iid ∘m f ≐ f ❙

		prop_isomorphism = [A,B,f:ihom A B] ∃ [g] g ∘m f ≐ iid ∧ f ∘m g ≐ iid ❘ # prop_isomorphic 3 ❙
		prop_isomorphic = [A,B] ∃[f : ihom A B] prop_isomorphic f ❘ # 1 ≅ 2 ❙
	❚
	category = Mod ☞?Categories/category_theory ❘ # Cat ❙
	objects : Cat ⟶ 𝒰 10 ❘ = [𝒞] 𝒞.universe ❘ # | 1 | ❙
	morphisms : {𝒞: Cat} |𝒞| ⟶ |𝒞| ⟶ 𝒰 10 ❘ = [𝒞,a,b] (𝒞.hom) a b ❘ # hom 2 3 ❙
	hom_composition : {𝒞:Cat,a,b,c:|𝒞|} hom a b ⟶ hom b c ⟶ hom a c ❘ = [𝒞,a,b,c,f,g] (𝒞.comp) a b c f g ❘ # 6 ∘ 5 prec 1 ❙
	id: {𝒞:Cat,a:|𝒞|} hom a a ❘ = [𝒞,a] (𝒞.identity) a❘ # id 2 ❙
❚

theory Opposite : base:?Logic =
    include ?Categories ❙

    opposite : category ⟶ category ❘ = [𝒞] ['
        universe := (𝒞.universe) ,
        hom := ([a,b] hom b a) ,
        comp := ([a,b,c][f,g] f ∘ g),
        identity := ([a] id a),
        axiom_assoc := ([a,b,c,d] trivial),
        axiom_id_r := ([a,b] trivial),
        axiom_id_l := ([a,b] trivial)
    '] ❘ # 1 op ❙
❚

theory Product : base:?Logic =
    include ?Categories ❙
    include ☞base:?ProductTypes ❙

    product : Cat ⟶ Cat ⟶ Cat ❘ = [𝒞,𝒟] ['
        universe := ((𝒞.universe) × (𝒟.universe)) ,
        hom := ([a,b] (hom (πl a) (πl b)) × (hom (πr a) (πr b))) ,
        comp := ([a,b,c][f,g] ⟨(πl g) ∘ (πl f),(πr g) ∘ (πr f) ⟩ ),
        identity := ([a] ⟨ id (πl a), id (πr a) ⟩),
        axiom_assoc := ([a,b,c,d] trivial),
        axiom_id_r := ([a,b] trivial),
        axiom_id_l := ([a,b] trivial)
    '] ❘ # 1 ×C 2 ❙
❚

theory ArrowCategory : base:?Logic =
    include ?Categories ❙
    include ☞base:?ProductTypes ❙
    // include base:?Subtyping ❙

    arr : Cat ⟶ Cat ❘ // = [𝒞] ['
        universe := (Σ A : | 𝒞 |, B : | 𝒞 |. hom A B) ,
        dom : universe ⟶ type := [tr] πl tr ,
        cod : universe ⟶ type := [tr] πl ( πr tr) ,
        arrow : universe ⟶ type := [tr] πr (πr) ,
        hom := ([a,b] Σ p : ((hom (dom a) (dom b)) × (hom (cod a) (cod b))) . ⊦ (πr p) ∘ a ≐ b ∘ (πl p) ) ,
        comp := ([a,b,c][f,g] ⟨⟨(πl (πl g)) ∘ (πl (πl f)),(πr (πl g)) ∘ (πr (πl f)) ⟩,trivial ⟩ ),
        identity := ([a] ⟨⟨ id (dom a), id (cod a) ⟩, trivial⟩),
        axiom_assoc := ([a,b,c,d] trivial),
        axiom_id_r := ([a,b] trivial),
        axiom_id_l := ([a,b] trivial)
    '] ❘ # 1 ×C 2 ❙ // Definiens fails ❙
❚



theory SmallCategories : base:?Logic =

    theory small_category_theory : base:?Logic =
    	universe : type ❘ # U ❙
    	hom : U ⟶ U ⟶ type ❘ # ihom 1 2 ❙
    	comp : {a,b,c:U} ihom a b ⟶ ihom b c ⟶ ihom a c ❘ # 5 ∘m 4 ❙
    	identity: {a:U} ihom a a ❘ # iid %I1 ❙
    	axiom_assoc : {a,b,c,d:U} ⊦ ∀[f:ihom a b] ∀[g:ihom b c] ∀[h:ihom c d] h ∘m (g ∘m f) ≐ (h ∘m g) ∘m f ❙
    	axiom_id_r : {x:U,a:U} ⊦ ∀[f:ihom a x] f ∘m iid ≐ f ❙
    	axiom_id_l : {x:U,a:U} ⊦ ∀[f:ihom x a] iid ∘m f ≐ f ❙
    ❚
	small_category = Mod ☞?SmallCategories/small_category_theory ❘ # SCat ❙

	include ?Categories ❙
❚

// theory CategoryOfSmallCategories : base:?Logic =
    include ?Functors ❙
    include ?SmallCategories ❙
    include base:?InformalProofs ❙

    Instance functor_composition (𝒞 : Cat, 𝒟 : Cat, E : Cat, F : functor 𝒞 𝒟, G : functor 𝒟 E) (functor 𝒞 E) ❘ =
        objF = [c : |𝒞|] objF G (objF F c) ❙
        homF : {A,B} hom A B ⟶ hom (objF A) (objF B) ❘ = [A,B][f] homF G (homF F f) ❘ # ihomF 3 ❙
        axiom_id : {A:|𝒞|} ⊦ ihomF (id A) ≐ id (objF A) ❘ = [A] sketch "trivial" ❙
        axiom_comp: {A:|𝒞|,B:|𝒞|,C:|𝒞|}{f : hom A B, g : hom B C} ⊦ ihomF (g ∘ f) ≐ (ihomF g) ∘ (ihomF f) ❘ = [A,B,C][f,g] sketch "trivial" ❙
    ❚ //

    Instance small_categories () Cat ❘ =
        universe = SCat ❙
        hom = [𝒞:universe,𝒟:universe] functor 𝒞 𝒟 ❙
        comp = [A:universe,B:universe,C:universe][f : hom A B,g : hom B C] functor_composition A B C f g ❙
    ❚ //
❚