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) ❙
❚
❚