6
$\begingroup$

Are questions about categorical logic and the related category theory are on topic on this website? Categorical logic is strongly connected to type theory and the semantic of (many) proof assistants, and I believe that a lot of people who care about the theoretical aspects of proof assistants also know a lot about categorical logic.

I very much like the proof-assistant stackexchange and I have read a lot of very useful answers here. I would love if this would also be a site for the more mathematical aspects of type theory. How do you feel about it?

Here is an example of a question which I would have liked to ask here, but did not because I wasn't sure if it is on topic.

https://math.stackexchange.com/questions/4450310/2-categorical-universal-property-of-the-classifying-category-of-a-type-theory

$\endgroup$
2
  • 4
    $\begingroup$ If the question is strictly about categorical logic/category theory, then I would say no because such a question would already be within the scope of math.SE, mathoverflow, and cstheory.SE. However, if you can sufficiently connect the question to proof assistants or some type theory related to proof assistants I think it might be okay, or if it is about the semantics of a logic or type theory relevant to this site. $\endgroup$
    – Couchy Mod
    Commented May 16, 2022 at 4:29
  • 1
    $\begingroup$ Relevant discussion: proofassistants.meta.stackexchange.com/a/87/75 $\endgroup$
    – Couchy Mod
    Commented May 17, 2022 at 3:06

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .