Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homotopy Type Theory (HoTT) where equality is interpreted as the identity type. The first model satisfies Scott's Anti-Foundation Axiom (SAFA) and dualises the construction of iterative sets. The second model satisfies Aczel's Anti-Foundation Axiom (AFA), and is constructed by adaption of Aczel-Mendler's terminal coalgebra theorem to type theory, which requires propositional resizing. In an bid to extend coalgebraic theory and anti-foundation axioms to higher type levels, we formulate generalisations of AFA and SAFA, and construct a hierarchy of models which satisfies the SAFA generalisations. These generalisations build on the framework of Univalent Material Set Theory, previously developed by two of the authors. Since the model constructions are based on M-types, the paper also includes a characterisation of the identity type of M-types as indexed M-types. Our results are formalised in the proof-assistant Agda.

We show how dinaturality plays a central role in the interpretation of directed type theory where types are given by (1-)categories and directed equality by hom-functors. We introduce a first-order directed type theory where types are semantically interpreted as categories, terms as functors, predicates as dipresheaves, and proof-relevant entailments as dinatural transformation. This type theory is equipped with an elimination principle for directed equality, motivated by dinaturality, which closely resembles the J -rule used in Martin-Löf type theory. This directed J -rule comes with a simple syntactic restriction which recovers all theorems about symmetric equality, except for symmetry. Dinaturality is used to prove properties about transitivity (composition), congruence (functoriality), and transport (coYoneda) in exactly the same way as in Martin-Löf type theory, and allows us to obtain an internal “naturality for free”. We then argue that the quantifiers of directed type theory should be ends and coends, which dinaturality allows us to capture formally. Our type theory provides a formal treatment to (co)end calculus and Yoneda reductions, which we use to give distinctly logical proofs to the (co)Yoneda lemma, the adjointness property of Kan extensions via (co)ends, exponential objects of presheaves, and the Fubini rule for quantifier exchange. Our main theorems are formalized in Agda.

Abstract This paper presents a formalization of the nonassociative Lambek calculus in the Agda proof assistant. The sequent calculus for this logic has sequents with binary trees as antecedents, in which formulae are stored as leaves. The shape of the antecedents creates subtleties when proving logical properties, since in many cases one needs to analyze equalities involving sequentially-composed trees. We formally characterize these equalities and show how to employ the resulting technical lemma to prove cut admissibility and the Maehara interpolation properly, which implies Craig interpolation. We show that both the cut rule and the interpolation procedure are well-defined wrt. a certain notion of equivalence of derivations. We additionally prove a proof-relevant version of Maehara interpolation, exhibiting the interpolation procedure as a right inverse of the admissible cut rule.

Abstract The symmetric skew monoidal categories of Bourke and Lack are a weakening of Mac Lane’s symmetric monoidal categories where (i) the three structural laws of left and right unitality and associativity are not required to be invertible, they are merely natural transformations with a specific orientation; (ii) the structural law of symmetry is a natural isomorphism involving three objects rather than two. In a similar fashion, symmetric skew closed categories are a weakening of de Schipper’s symmetric closed categories with non-invertible structural laws of left and right unitality. In this paper, we study the structural proof theory of symmetric skew monoidal and symmetric skew closed categories, progressing the project initiated by Uustalu et al. on deductive systems for categories with skew structure. We discuss three equivalent presentations of the free symmetric skew monoidal (resp. closed) category on a set of generating objects: a Hilbert-style categorical calculus; a cut-free sequent calculus; a focused subsystem of derivations, corresponding to a sound and complete goal-directed proof search strategy for the cut-free sequent calculus. Focusing defines an effective normalization procedure for maps in the free symmetric skew monoidal (resp. closed) category, as such solving the coherence problem for symmetric skew monoidal (resp. closed) categories.

Abstract We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

Dependent type theories with guarded recursion have shown themselves suitable for the development of denotational semantics of programming languages. In particular Ticked Cubical Type Theory (TCTT) has been used to show that for guarded labelled transition systems (GLTS) interpretation into the denotational semantics maps bisimilar processes to equal values. In fact the two notions are proved equivalent, allowing one to reason about equality in place of bisimilarity.

The Eilenberg-Kelly theorem states that a category C with an object I and two functors ⊗:C×C→C and ⊸:Cop×C→C related by an adjunction −⊗B⊣B⊸− natural in B is monoidal iff it is closed and moreover the adjunction holds internally. We dissect the proof of this theorem and observe that the necessity for a side condition on closedness arises because the standard definition of closed category is left-skew in regards to associativity. We analyze Street's observation that left-skew monoidality is equivalent to left-skew closedness and establish that monoidality is equivalent to closedness unconditionally under an adjusted definition of closedness that requires normal associativity. We also work out a definition of right-skew closedness equivalent to right-skew monoidality. We give examples of each type of structure; in particular, we look at the Kleisli category of a left-strong monad on a left-skew closed category and the Kleisli category of a lax closed monad on a right-skew closed category. We also view skew and normal monoidal and closed categories as special cases of skew and normal promonoidal categories and take a brief look at left-skew prounital-closed categories.

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos). Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity. Guarded recursion in the sense of Nakano has recently been suggested as a possible approach to dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.

Abstract Rational sequences are possibly infinite sequences with a finite number of distinct suffixes. In this paper, we present different implementations of rational sequences in Martin–Löf type theory. First, we literally translate the above definition of rational sequence into the language of type theory, i.e., we construct predicates on possibly infinite sequences expressing the finiteness of the set of suffixes. In type theory, there exist several inequivalent notions of finiteness. We consider two of them, listability and Noetherianness, and show that in the implementation of rational sequences the two notions are interchangeable. Then we introduce the type of lists with backpointers, which is an inductive implementation of rational sequences. Lists with backpointers can be unwound into rational sequences, and rational sequences can be truncated into lists with backpointers. As an example, we see how to convert the fractional representation of a rational number into its decimal representation and vice versa.