Extending homotopy type theory with strict equality

QR Code

Extending homotopy type theory with strict equality

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 and often impossible to handle towers of coherenc...

Full description

Bibliographic Details
Main Authors:	Altenkirch, Thorsten, Capriotti, Paolo, Nicolai, Kraus
Format:	Conference or Workshop Item
Published:	2016
Subjects:	homotopy type theory coherences strict equality homotopy type system
Online Access:	https://eprints.nottingham.ac.uk/34363/

Similar Items

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

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

Towards a cubical type theory without an interval
by: Altenkirch, Thorsten, et al.
Published: (2017)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Models of type theory with strict equality
by: Capriotti, Paolo
Published: (2017)

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

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)

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

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

Strict liability versus policy and regulation for environmental protection and agricultural waste management in Malaysia
by: Ishak, Mohd. Bakri, et al.
Published: (2010)

Liability of pharmacists in Malaysia / Intan Sharina Nasri, Azimah Nor Idris and Dg. Roslina Datu Mohamad.
by: Nasri, Intan Sharina, et al.
Published: (2006)

Entry to cyber cafe by children: duties and liabilities of the operators / Mohd Noor Redza Mohd Radzuan ...[et al.]
by: Mohd Radzuan, Mohd Noor Redza, et al.
Published: (2011)

Equality and Diversity in the NHS
by: Mellows, Sara
Published: (2006)

Iterative frequency domain equalization with generalized approximate message passing
by: Guo, Q., et al.
Published: (2013)

Reconstructive and cosmetic surgery: the need for consumer protection / Izreen Marleeza Mansoor and Norsyazreen Mohamed Salleh
by: Mansoor, Izreen Marleeza, et al.
Published: (2008)

Liability in medical negligence: looking into the position of non-medical staff / Nur Azura Othman, Mohd Azali Ibrahim and Tengku Chik Abu Bakar Tengku Ibrahim
by: Othman, Nur Azura, et al.
Published: (2006)

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

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

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

Type-2 fuzzy linear systems
by: Najariyan, Marzieh, et al.
Published: (2017)

Influence of vegetation and soil types on the wheatbelt termite, Drepanotermes tamminensis (Hill), in the Western Australian wheatbelt
by: Park, H., et al.
Published: (1994)

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

Innovative Social Policies for Gender Equality at Work
by: Fox, E, et al.
Published: (2006)

Baroque Historical Dances Lecture and Workshop by Mireia Frutos Fernandez : World Music History Lecture Series
by: Universiti Teknologi MARA, Faculty of Music
Published: (2018)

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

Analysis of g s-transferase, protien tyrosine phosphatase 1B, nuclear factor kappa-B1 and leptin receptor genetic polymorphisms as risk factors for Malaysian type 2 diabetes mellitus subjects
by: Etemad, Ali
Published: (2013)