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

theory CategoryOfSets : base:?Logic =
    include ?Categories 
    include http://mathhub.info/MitM/Foundation/sets?ZFC 
    include http://mathhub.info/MitM/Foundation/sets?SetTypeConversions 

    composition_of_functions : {s,t,r} (elem s ⟶ elem t) ⟶ (elem t ⟶ elem r) ⟶ (elem s ⟶ elem r) 
        = [s,t,r] [f,g] [x] g (f x)  # 5 ∘c 4 
    cSet : category  = ['
        universe := set ,
        hom := ([s,t] (elem s) ⟶ (elem t)) ,
        comp := composition_of_functions ,
        identity := ([s] [x : elem s] x) ,
        axiom_assoc := ([a,b,c,d] trivial) ,
        axiom_id_r := ([x,u] trivial) ,
        axiom_id_l := ([x,u] trivial)
    '] 


theory Temp : base:?Logic =
    include http://mathhub.info/MitM/Foundation/sets?ZFC 
    include http://mathhub.info/MitM/Foundation/sets?SetTypeConversions 

    Image : {s,t}{f: elem s ⟶ elem t} elem (℘ s) ⟶ elem (℘ t)  # Im 4 3 
    Preimage : {s,t}{f: elem s ⟶ elem t} elem (℘ t) ⟶ elem (℘ s)  # PreIm 4 3 


theory PowersetFunctors : base:?Logic =
    include ?CategoryOfSets 
    include ?Functors 
    include ?Opposite 
    include ?Temp 

    covariantPowersetFunctor : functor cSet cSet  = ['
            objF := ([A] ℘ A),
            homF := ([A,B][f] [x] Im x f),
            axiom_id := ([x] trivial) ,
            axiom_comp := ([a,b,c,f,g] trivial)
        '] 
    contravariantPowersetFunctor : functor (cSet op) cSet  // = ['
            objF := ([A] ℘ A),
            homF := ([A,B][f] [x] PreIm x f),
            axiom_id := ([x] trivial) ,
            axiom_comp := ([a,b,c,f,g] trivial)
        ']  // Definiens takes forever ❙


theory Coalgebras : base:?Logic =
    include ?CategoryOfSets 
    include ?Functors 

    theory coalgebra_theory : base:?Logic =
        T : functor cSet cSet 
        C : set 
        gamma : elem C ⟶ elem (objectF cSet cSet T C)