Type theory in a type theory with quotient inductive types

QR Code

Type theory in a type theory with quotient inductive types

Type theory (with dependent types) was introduced by Per Martin-Löf with the intention of providing a foundation for constructive mathematics. A part of constructive mathematics is type theory itself, hence we should be able to say what type theory is using the formal language of type theory. In add...

Full description

Bibliographic Details
Main Author:	Kaposi, Ambrus
Format:	Thesis (University of Nottingham only)
Language:	English
Published:	2017
Subjects:	type theory homotopy type theory parametricity normalisation by evaluation
Online Access:	https://eprints.nottingham.ac.uk/41385/

Similar Items

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

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

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

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

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)

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

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

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)

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

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

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

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

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

Quotient inductive-inductive types
by: Altenkirch, Thorsten, et al.
Published: (2017)

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)

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

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

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)

A Study on Relationship Between Decision-making Behaviour and Myers-Briggs Type Indicator
by: Chen, Jelico
Published: (2007)

Prediction of bandgaps in membrane-type metamaterial attached to a thin plate
by: Gao, Cong, et al.
Published: (2019)

The role of C-type lectin receptors in the recognition of Pseudiminas aeruginosa
by: Alshahrani, Mohammad
Published: (2018)

Study of bandgap property of a bilayer membrane-type metamaterial applied on a thin plate
by: GAO, Cong, et al.
Published: (2020)

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

Analysis of gastrointestinal microbiota in relation to obesity and type 2 diabetes among adults
by: Kaliyappan, Roseni
Published: (2015)

The role of b-type natriuretic peptide in heart failure management
by: Newton, Phillip, et al.
Published: (2009)

Exploring the management of type 2 diabetes in the Caribbean
by: Nixon, Amy L.
Published: (2021)

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

Early Loss of the Glucagon Response to Hypoglycemia in Adolescents with Type 1 Diabetes
by: Siafarikas, A., et al.
Published: (2012)

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)

Factors associated with glycaemic control among diabetes mellitus type 2 patients attending health clinics in Tampin district Negeri Sembilan, Malaysia
by: Wan Hamdzan, Wan Farzana Fasya
Published: (2016)

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

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

THE EFFECT OF DIFFERENT TYPES OF DIRECTORS ON CORPORATE PERFORMANCE: EVIDENCE FROM INDIAN LISTED COMPANIES.
by: Dake, Ghoshal Vishwas
Published: (2007)

Association of dietary patterns with socio-demographic, lifestyle, weight status and biochemical profiles among type 2 diabetes mellitus patients in a special Medical Center, Tehran Iran
by: Zad, Nasrin Darani
Published: (2012)

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

Floating s- and p-type Gaussian Orbitals
by: Brailsford, David F., et al.
Published: (1975)