Towards a cubical type theory without an interval

QR Code

Towards a cubical type theory without an interval

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 of equality is encoded as a term in a context ext...

Full description

Bibliographic Details
Main Authors:	Altenkirch, Thorsten, Kaposi, Ambrus
Format:	Article
Published:	Dagstuhl Publishing 2017
Subjects:	homotopy type theory parametricity univalence
Online Access:	https://eprints.nottingham.ac.uk/44008/

Similar Items

Type theory in a type theory with quotient inductive types
by: Kaposi, Ambrus
Published: (2017)

Type theory in type theory using quotient inductive types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Extending homotopy type theory with strict equality
by: Altenkirch, Thorsten, et al.
Published: (2016)

Normalisation by evaluation for type theory, in type theory
by: Altenkirch, Thorsten, et al.
Published: (2017)

Quotient types in type theory
by: Li, Nuo
Published: (2015)

Normalisation by evaluation for dependent types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Constructions with non-recursive higher inductive types
by: Kraus, Nicolai
Published: (2016)

Partiality, revisited: the partiality monad as a quotient inductive-inductive type
by: Altenkirch, Thorsten, et al.
Published: (2017)

Truncation levels in homotopy type theory
by: Kraus, Nicolai
Published: (2015)

Notions of anonymous existence in Martin-Löf type theory
by: Kraus, Nicolai, et al.
Published: (2016)

Higher inductive types, inductive families, and inductive-inductive types
by: von Raumer, Jakob
Published: (2020)

Twisted Cubes and their Applications in Type Theory
by: Pinyo, Gun
Published: (2023)

Univalent higher categories via complete semi-segal types
by: Capriotti, Paolo, et al.
Published: (2018)

Types with extra structure: predicates, equations, composition
by: Hewer, Brandon
Published: (2024)

Homotopy Analysis And Legendre Multi-Wavelets Methods For Solving Integral Equations
by: Vahdati, Saeed
Published: (2009)

Higher linear algebraic quantum field theory
by: Bruinsma, Simen
Published: (2022)

Modified homotopy perturbation method for integro-differential and hypersingular integral equations
by: Zulkarnain, Fatimah Samihah
Published: (2018)

Spectral homotopy analysis method and composite Chebyshev finite difference method for solving integro-differential equations
by: Atabakan, Zohreh Pashazadeh
Published: (2015)

Homotopy colimits and global observables in Abelian gauge theory
by: Benini, Marco, et al.
Published: (2015)

On Nie-Tan operator and type-reduction of interval type-2 fuzzy sets
by: Li, Jiawei, et al.
Published: (2018)

Learning of interval and general type-2 fuzzy logic systems using simulated annealing: theory and practice
by: Almaraashia, M., et al.
Published: (2016)

Free higher groups in homotopy type theory
by: Kraus, Nicolai, et al.
Published: (2018)

Handling uncertainty: from type-1 to interval type-2 fuzzy sets and systems
by: Aladi, Jabran
Published: (2016)

Interval type–2 fuzzy decision making
by: Runkler, Thomas, et al.
Published: (2017)

Assessing the Performance of Value-at-Risk Models in Chinese Stock Market
by: Lin, Lin
Published: (2008)

Methods of Measuring and Simulating the Intracluster Light of Galaxy Clusters
by: de-Ville, Jordan
Published: (2024)

Agent-Based Logics in Dependent Type Theory
by: Baston, Colm
Published: (2025)

A novel framework for the implementation and evaluation of type-1 and interval type-2 ANFIS
by: Chen, Chao
Published: (2018)

Representations of first order function types as terminal coalgebras
by: Altenkirch, Thorsten
Published: (2001)

Error estimations of Homotopy perturbation method for linear integral and integro-differential equations of the third kind
by: Eshkuvatov, Zainidin K., et al.
Published: (2016)

Parametric modelling of architectural surfaces
by: Pitts, G., et al.
Published: (2009)

Interval type-2 A-intuitionistic fuzzy logic for regression problems
by: Eyoh, Imo, et al.
Published: (2017)

Linear homotopy solution of nonlinear systems of equations in geodesy
by: Palancz, B., et al.
Published: (2010)

From interval-valued data to general type-2 fuzzy sets
by: Wagner, Christian, et al.
Published: (2014)

Interval type-2 fuzzy modelling and stochastic search for real-world inventory management
by: Miller, Simon, et al.
Published: (2012)

Microstructural abnormalities in white and gray matter in obese adolescents with and without type 2 diabetes
by: Nouwen, Arie, et al.
Published: (2017)

Parametric factory simulation for the responsive enterprise
by: Farr, Richard, et al.
Published: (2007)

Parametric modelling and the tessellation of architectural surfaces
by: Pitts, G., et al.
Published: (2008)

Space of SO(3) orbits of elasticity tensors
by: Bona, Andrej, et al.
Published: (2008)

Rapid Manufacturing: Torus geometry and surface tessellation
by: Pitts, G., et al.
Published: (2007)