Contribution: ConCaT

Constructive Category Theory

Authors

• Amokrane Saïbi

Description

Keywords

category theory

Available files

• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_BinProds.html
• ConCaT.CATEGORY_THEORY.LIMITS.FunForget_UA.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_Exponents.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.FREYD_THEOREM.FAFT_Part2_Proof2.html
• ConCaT.CATEGORY_THEORY.LIMITS.Discr.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.FSC_inc.html
• ConCaT.CATEGORY_THEORY.NT.Ntransformation.html
• ConCaT.CATEGORY_THEORY.LIMITS.CoUniversalArrow.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.CCC.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Comma_proj.html
• ConCaT.SETOID.Map.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Adjunction1.html
• ConCaT.SETOID.Map2.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.Terminal1.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.FREYD_THEOREM.FAFT_Part2_Proof1.html
• ConCaT.SETOID.Setoid_prop.html
• ConCaT.SETOID.SetoidPROD.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.HomFunctor.html
• ConCaT.SETOID.MapProperty.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.FREYD_THEOREM.FAFT_Part1.html
• ConCaT.SETOID.STRUCTURE.FreeMonoid.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.HomFunctor2.html
• ConCaT.SETOID.STRUCTURE.Group.html
• ConCaT.CATEGORY_THEORY.LIMITS.PULB.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.Cartesian1.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.Equalizers.html
• ConCaT.CATEGORY_THEORY.LIMITS.Limit.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Limit_Adj.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.FunOne.html
• ConCaT.RELATIONS.CONFLUENCE.TAIT.Tait.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.FREYD_THEOREM.FAFT_SSC2.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_Terminal.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Category_dup1.html
• ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.Map0_dup1.html
• ConCaT.CATEGORY_THEORY.LIMITS.PA.html
• ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.Functor_dup1.html
• ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.YonedaLemma.html
• ConCaT.RELATIONS.CONFLUENCE.Confluence.html
• ConCaT.CATEGORY_THEORY.CATEGORY.PermCat.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Dual_Functor.html
• ConCaT.SETOID.STRUCTURE.Monoid.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Setoid_dup1.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Adjunction.html
• ConCaT.CATEGORY_THEORY.LIMITS.CoLimit.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.CCC1.html
• ConCaT.CATEGORY_THEORY.LIMITS.Iso_Limit.html
• ConCaT.CATEGORY_THEORY.LIMITS.Products1.html
• ConCaT.CATEGORY_THEORY.CATEGORY.ONE.html
• ConCaT.CATEGORY_THEORY.CATEGORY.FullSubCat.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.HomFunctor_Continuous.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.PROD_proj.html
• ConCaT.CATEGORY_THEORY.NT.InterChangeLaw.html
• ConCaT.RELATIONS.Noetherian.html
• ConCaT.SETOID.BasicTypes.html
• ConCaT.SETOID.Setoid.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.IdCAT.html
• ConCaT.SETOID.STRUCTURE.Inverses_Group.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.Comma_Complete.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_Pullback.html
• ConCaT.RELATIONS.Relations.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.Binary_Products.html
• ConCaT.CATEGORY_THEORY.NT.CatFunct.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.FunctorProperty.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.CatProperty.html
• ConCaT.SETOID.Single.html
• ConCaT.CATEGORY_THEORY.NT.NatIso.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.Exponents.html
• ConCaT.CATEGORY_THEORY.LIMITS.Equalizers1.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Th_CoAdjoint.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.Pres_Limits.html
• ConCaT.CATEGORY_THEORY.CATEGORY.MON.html
• ConCaT.CATEGORY_THEORY.LIMITS.Comma_UA.html
• ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.YonedaEmbedding.html
• ConCaT.RELATIONS.CONFLUENCE.Coherence.html
• ConCaT.CATEGORY_THEORY.CATEGORY.PROD.html
• ConCaT.CATEGORY_THEORY.NT.Setoid_dup2.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_Equalizer.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SET_CCC.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.SET_Complete.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.Products.html
• ConCaT.RELATIONS.CONFLUENCE.NEWMAN.Newman.html
• ConCaT.CATEGORY_THEORY.CATEGORY.SET.html
• ConCaT.CATEGORY_THEORY.CATEGORY.Category.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.LeftAdj_Iso.html
• ConCaT.CATEGORY_THEORY.NT.HomFunctor_NT.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.Pullbacks.html
• ConCaT.CATEGORY_THEORY.CATEGORY.Dual.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.FunProd.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Comma.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.Th_Initial.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Adj_UA.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Th_Adjoint.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.CCC.Diagonal.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.CAT.html
• ConCaT.CATEGORY_THEORY.LIMITS.UniversalArrow.html
• ConCaT.CATEGORY_THEORY.LIMITS.Pullbacks1.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.FunFreeMon.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.Functor.html
• ConCaT.CATEGORY_THEORY.FUNCTOR.FunForget.html
• ConCaT.CATEGORY_THEORY.LIMITS.Const.html
• ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.SETProperty.html
• ConCaT.CATEGORY_THEORY.NT.Category_dup2.html
• ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html
• ConCaT.CATEGORY_THEORY.LIMIT_CONSTRUCTIONS.Th_Limits.html
• ConCaT.CATEGORY_THEORY.ADJUNCTION.Adj_FunFreeMon.html