13 citations · 28 across the 14 of their papers we have counts for
18 papers
Directed type theory, with a twist
Fernando Rafael Chu Rivera, Paige Randall North
In recent years, Homotopy Type Theory (HoTT) has had great success both as a foundation of mathematics and as internal language to reason about -groupoids (a.k.a. spaces).…
Functoriality of Enriched Data Types
Lukas Mulder, Paige Randall North, Maximilien Péroux
In previous work, categories of algebras of endofunctors were shown to be enriched in categories of coalgebras of the same endofunctor, and the extra structure of that enrichment w…
From Semantics to Syntax: A Type Theory for Comprehension Categories
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens +1
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial…
Categorical Diffusion of Weighted Lattices
Robert Ghrist, Miguel Lopez, Paige Randall North +1
We introduce a categorical formalization of diffusion processes for network-structured data, motivated by applications in data science and information dynamics. At the heart of our…
Comparing semantic frameworks for dependently-sorted algebraic theories
Benedikt Ahrens, Peter LeFanu Lumsdaine, Paige Randall North
Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using ca…
Measuring data types
Lukas Mulder, Paige Randall North, Maximilien Péroux
In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which -algebras are enriched in -coalgebras for a field -- with the theory of W-types…
Insights From Univalent Foundations: A Case Study Using Double Categories
Nima Rasekh, Niels van der Weide, Benedikt Ahrens +1
Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced area…
Univalent Double Categories
Niels van der Weide, Nima Rasekh, Benedikt Ahrens +1
Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only inc…
Coinductive control of inductive data types
Paige Randall North, Maximilien Péroux
We combine the theory of inductive data types with the theory of universal measurings. By doing so, we find that many categories of algebras of endofunctors are actually enriched i…
Univalent foundations and the equivalence principle
Benedikt Ahrens, Paige Randall North
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the ki…
Bicategorical type theory: semantics and syntax
Benedikt Ahrens, Paige Randall North, Niels van der Weide
We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is…
Algebraic Presentations of Type Dependency
Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North +1
C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised algebraic theories. B-systems were defined by Voevodsky in his quest to formul…
The Univalence Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based,…
A Higher Structure Identity Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant und…
A Hurewicz Model Structure for Directed Topology
Sanjeevi Krishnan, Paige Randall North
This paper constructs an h-model structure for diagrams of streams, locally preordered spaces. Along the way, the paper extends some classical characterizations of Hurewicz fibrati…
Type-theoretic weak factorization systems
Paige Randall North
This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, a…
Identity types and weak factorization systems in Cauchy complete categories
Paige Randall North
It has been known that categorical interpretations of dependent type theory with Sigma- and Id-types induce weak factorization systems. When one has a weak factorization system (L,…
Towards a directed homotopy type theory
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories, directed homotopy theory, and its applications to concurrency. We s…