Skip to main content
added 15 characters in body
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Different types of categories lead to different types of internal logics. Here is a very short list:

 Regular Logic            Regular Category
 Coherent Logic           Coherent Category 
 Geometric Logic          Infinitary Coherent Category/Geometric Category
 First-Order Logic        Heyting Category
 Dependent Type Theory    Locally Cartesian Closed Category
 Higher-Order Logic       Elementary Topos

Some of the names are somewhat standard by now, but be warned that Johnsone (Sketches of an Elephant), Freyd & Scedrov (Categories, Allegories), the nLab, and many others all use slightly different terminology. I think Johnstone's presentation in the Elephant is very nice, though you can certainly find friendlier and more localized accounts elsewhere.

Different types of categories lead to different types of internal logics. Here is a very short list:

 Regular Logic            Regular Category
 Coherent Logic           Coherent Category 
 Geometric Logic          Infinitary Coherent Category/Geometric Category
 First-Order Logic        Heyting Category
 Dependent Type Theory    Locally Cartesian Closed Category
 Higher-Order Logic       Elementary Topos

Some of the names are somewhat standard by now, but be warned that Johnsone (Sketches of an Elephant), Freyd & Scedrov (Categories, Allegories), the nLab, and many others all use slightly different terminology. I think Johnstone's presentation in the Elephant is very nice, though you can certainly find more localized accounts elsewhere.

Different types of categories lead to different types of internal logics. Here is a very short list:

 Regular Logic            Regular Category
 Coherent Logic           Coherent Category 
 Geometric Logic          Infinitary Coherent Category/Geometric Category
 First-Order Logic        Heyting Category
 Dependent Type Theory    Locally Cartesian Closed Category
 Higher-Order Logic       Elementary Topos

Some of the names are somewhat standard by now, but be warned that Johnsone (Sketches of an Elephant), Freyd & Scedrov (Categories, Allegories), the nLab, and many others all use slightly different terminology. I think Johnstone's presentation in the Elephant is very nice, though you can certainly find friendlier and more localized accounts elsewhere.

Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Different types of categories lead to different types of internal logics. Here is a very short list:

 Regular Logic            Regular Category
 Coherent Logic           Coherent Category 
 Geometric Logic          Infinitary Coherent Category/Geometric Category
 First-Order Logic        Heyting Category
 Dependent Type Theory    Locally Cartesian Closed Category
 Higher-Order Logic       Elementary Topos

Some of the names are somewhat standard by now, but be warned that Johnsone (Sketches of an Elephant), Freyd & Scedrov (Categories, Allegories), the nLab, and many others all use slightly different terminology. I think Johnstone's presentation in the Elephant is very nice, though you can certainly find more localized accounts elsewhere.