The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory

Tom de Jong, Nicolai Kraus, Axel Ljungström

Simplicial type theory extends homotopy type theory and equips types with a notion of directed morphisms. A Segal type is defined to be a type in which these directed morphisms can…