Embedding Multimode Type Theory (MTT) as a library enables the usage of additional reasoning principles in off-the-shelf proof assistants without risking soundness or compatibility. Moreover, by interpreting embedded MTT terms in an internally constructed model of MTT, we can extract programs and proofs to the meta language and obtain interoperability between the embedded language and the metalanguage. The existing Sikkel library for Agda achieves this for Multimode Simple Type Theory (MSTT) with an internal presheaf model of dependent MTT. In this work, we add, on top of the simply-typed layer, a logical framework in which users can write multimode proofs about multimode Sikkel programs, still in an off-the-shelf proof assistant. To this end, we carve out of MTT a new multimode logical framework µLF over MSTT and implement it on top of Sikkel, interpreting both in the existing internal model. In the process, we further extend and improve the original codebase for each of the three layers (syntax, semantics and extraction) of Sikkel. We demonstrate the use of µLF by proving some properties about functions manipulating guarded streams and by implementing an example involving parametricity predicates.

Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in order to carry out further reasoning internally, allowing greater abstraction and sometimes automated verification. While the constructions of presheaf models largely follow a common pattern, approaches towards internalization do not. Throughout the literature, various internal presheaf operators ($\surd$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$, $\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and little is known about their relative expressivenes. Moreover, some of these require that variables whose type is a shape (representable presheaf, e.g. an interval) be used affinely. We propose a novel type former, the transpension type, which is right adjoint to universal quantification over a shape. Its structure resembles a dependent version of the suspension type in HoTT. We give general typing rules and a presheaf semantics in terms of base category functors dubbed multipliers. Structural rules for shape variables and certain aspects of the transpension type depend on characteristics of the multiplier. We demonstrate how the transpension type and the strictness axiom can be combined to implement all and improve some of the aforementioned internalization operators (without formal claim in the case of locally fresh names).

Two approaches exist to incorporate parametricity into proof assistants based on dependent type theory. On the one hand, parametricity translations conveniently compute parametricity statements and their proofs solely based on individual well-typed polymorphic programs. But they do not offer internal parametricity: formal proofs that any polymorphic program of a certain type satisfies its parametricity statement. On the other hand, internally parametric type theories augment plain type theory with additional primitives out of which internal parametricity can be derived. But those type theories lack mature proof assistant implementations and deriving parametricity in them involves low-level intractable proofs. In this paper, we contribute Agda --bridges: the first practical internally parametric proof assistant. We provide the first mechanized proofs of crucial theorems for internal parametricity, like the relativity theorem. We identify a high-level sufficient condition for proving internal parametricity which we call the structure relatedness principle (SRP) by analogy with the structure identity principle (SIP) of HoTT/UF. We state and prove a general parametricity theorem for types that satisfy the SRP. Our parametricity theorem lets us obtain one-liner proofs of standard internal free theorems. We observe that the SRP is harder to prove than the SIP and provide in Agda --bridges a shallowly embedded type theory to compose types that satisfy the SRP. This type theory is an observational type theory of logical relations and our parametricity theorem ought to be one of its inference rules.

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin's mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion, thereby demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transformations between them. We show that different choices of mode theory allow us to use the same type theory to compute and reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion --- demonstrating that MTT constitutes a simple and usable syntax whose instantiations intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating MTT to a particular situation unearths a previously unknown type theory that improves upon prior systems. Finally, we investigate the metatheory of MTT. We prove the consistency of MTT and establish canonicity through an extension of recent type-theoretic gluing techniques. These results hold irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

Dependent type theory allows us to write programs and to prove properties about those programs in the same language. However, some properties do not require much proof, as they are evident from a program's implementation, e.g. if a polymorphic program is not ad hoc but relationally parametric, then we get parametricity theorems for free. If we want to safely shortcut proofs by relying on the evident good behaviour of a program, then we need a type-level guarantee that the program is indeed well-behaved. This can be achieved by annotating function types with a modality describing the behaviour of functions.

Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically in Reynolds's theory of relational parametricity, which allows the metatheoretical derivation of parametricity theorems about all values of a given type. Although predicative System F embeds into dependent type systems such as Martin-Löf Type Theory (MLTT), parametricity does not carry over as easily. The identity extension lemma, which is crucial if we want to prove theorems involving equality, has only been shown to hold for small types, excluding the universe. We attribute this to the fact that MLTT uses a single type former Π to generalize both the parametric quantifier ∀ and the type former → which is non-parametric in the sense that its elements may use their argument as a value. We equip MLTT with parametric quantifiers ∀ and ∃ alongside the existing Π and Σ, and provide relation type formers for proving parametricity theorems internally. We show internally the existence of initial algebras and final co-algebras of indexed functors both by Church encoding and, for a large class of functors, by using sized types. We prove soundness of our type system by enhancing existing iterated reflexive graph (cubical set) models of dependently typed parametricity by distinguishing between edges that express relatedness of objects (bridges) and edges that express equality (paths). The parametric functions are those that map bridges to paths. We implement an extension to the Agda proof assistant that type-checks proofs in our type system.