7 problems

Let $\textsf{CCTT}$ be the type theory whose judgements and rules reflect the structure of comprehension categories, and let comprehension categories provide its categorical models…

Let $\textsf{CCTT}$ be the type theory defined from the judgements and rules corresponding to comprehension categories, including the coercion morphisms…

Physical duoidal category conjecture. Physical duoidal categories also form isomix linearly distributive categories.

Let a dependent type theory be extended by additional strict equalities, and factor the extension through the freely generated infinity-congruence on the base theory. Coherence con…

A model of second-order multiplicative linear logic is injective with respect to existential linkings when distinct existential linkings are mapped to distinct elements by the mode…

Let $\mathbb{O}\mathbf{pen}(\mathsf{Petri})$ be the double category of open Petri nets, and let $\mathbb{O}\mathbf{neWay}(\mathsf{Petri})$ be the full sub-double category whose hor…

Let $P$colon $LX\to LY$ and $Q\colon LY\to LZ$ be composable open Petri nets, and let $\blacksquare$ denote their reachability semantics. An open Petri net is one-way if no place i…