All Outputs (26)

The Münchhausen Method in Type Theory (2023)
Journal Article

In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the ter... Read More about The Münchhausen Method in Type Theory.

Combinatory logic and lambda calculus are equal, algebraically (2023)
Journal Article

It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both lan... Read More about Combinatory logic and lambda calculus are equal, algebraically.

Should Type Theory Replace Set Theory as the Foundation of Mathematics? (2023)
Journal Article

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (H... Read More about Should Type Theory Replace Set Theory as the Foundation of Mathematics?.

Constructing a universe for the setoid model (2021)
Conference Proceeding

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent pr... Read More about Constructing a universe for the setoid model.

Big Step Normalisation for Type Theory (2020)
Journal Article

Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to... Read More about Big Step Normalisation for Type Theory.

The Integers as a Higher Inductive Type (2020)
Conference Proceeding

We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to... Read More about The Integers as a Higher Inductive Type.

Naive Type Theory (2019)
Book Chapter

We introduce Type Theory, including Homotopy Type Theory, as an alternative to set theory as a foundation of Mathematics emphasising the intuitive and naive understanding of its concepts.

Setoid Type Theory—A Syntactic Translation (2019)
Conference Proceeding

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a s... Read More about Setoid Type Theory—A Syntactic Translation.

Constructing quotient inductive-inductive types (2019)
Conference Proceeding

Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting... Read More about Constructing quotient inductive-inductive types.

Pure Functional Epidemics: An Agent-Based Approach (2018)
Conference Proceeding

Agent-Based Simulation (ABS) is a methodology in which a system is simulated in a bottom-up approach by modelling the micro interactions of its constituting parts, called agents, out of which the global system behaviour emerges. So far mainly object-... Read More about Pure Functional Epidemics: An Agent-Based Approach.

Free Higher Groups in Homotopy Type Theory (2018)
Conference Proceeding

© 2018 ACM. Given a type A in homotopy type theory (HoTT), we can define the free∞-group onA as the loop space of the suspension ofA+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A),... Read More about Free Higher Groups in Homotopy Type Theory.

Quotient inductive-inductive types (2018)
Book Chapter

Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of H... Read More about Quotient inductive-inductive types.

Towards a cubical type theory without an interval (2018)
Journal Article

Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof... Read More about Towards a cubical type theory without an interval.

Normalisation by evaluation for type theory, in type theory (2017)
Journal Article

© Altenkirch and Kaposi. We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation henc... Read More about Normalisation by evaluation for type theory, in type theory.

Notions of anonymous existence in Martin-Löf type theory (2017)
Journal Article

As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have uniqu... Read More about Notions of anonymous existence in Martin-Löf type theory.

Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017)
Conference Proceeding

Capretta's delay monad can be used to model partial computations, but it has the ``wrong'' notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the ``right''notion of equality, weak bisimilarity. However,... Read More about Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type.

Extending Homotopy Type Theory with Strict Equality (2016)
Conference Proceeding

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult a... Read More about Extending Homotopy Type Theory with Strict Equality.

Normalisation by evaluation for dependent types (2016)
Conference Proceeding

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realiz... Read More about Normalisation by evaluation for dependent types.

Type theory in type theory using quotient inductive types (2016)
Conference Proceeding

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids r... Read More about Type theory in type theory using quotient inductive types.

Indexed containers (2015)
Journal Article

We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide... Read More about Indexed containers.