nLab coherent functor




A functor F:CDF : C \to D between coherent categories is called coherent if it is a regular functor and in addition preserves finite unions.


categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus


Page 34 of

Last revised on November 16, 2022 at 06:01:56. See the history of this page for a list of all contributions to it.