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
