Univalent higher categories via complete semi-segal types

QR Code

Univalent higher categories via complete semi-segal types

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.)solves this by considering only truncated types, roughly corresponding to an ordin...

Full description

Bibliographic Details
Main Authors:	Capriotti, Paolo, Kraus, Nicolai
Format:	Article
Published:	Association for Computing Machinery 2018
Subjects:	Homotopy type theory higher categories complete Segal spaces
Online Access:	https://eprints.nottingham.ac.uk/49374/

Similar Items

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

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

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

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)

An analysis of factors contributing to apprenticeship and traineeship completion
by: Stromback, Carl, et al.
Published: (2010)

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

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

A retail category management model integrating shelf space and inventory levels
by: Ramaseshan, Balasubramanian, et al.
Published: (2009)

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

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)

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

The brand-personality of three categories of drinks in Australia
by: Liang, Johan, et al.
Published: (2010)

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

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

Drilling and completion challenges and remedies of CO2 injected wells with emphasis to mitigate well integrity issues
by: Hossain, Mofazzal, et al.
Published: (2011)

When the safety net of treatment has been removed: patients' unmet needs at the completion of treatment for haematological malignancies
by: Lobb, Elizabeth, et al.
Published: (2009)

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

Quantum field theories on categories fibered in groupoids
by: Benini, Marco, et al.
Published: (2017)

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

Nonassociative geometry in quasi-Hopf representation categories II: connections and curvature
by: Barnes, Gwendolyn E., et al.
Published: (2016)

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

Nonassociative geometry in quasi-Hopf representation categories I: bimodules and their internal homomorphisms
by: Barnes, Gwendolyn E., et al.
Published: (2015)

The complete solution to the Sylvester-polynomial-conjugate matrix equations
by: Wu, A., et al.
Published: (2011)

Assessing the impact of the introduction of an electronic hospital discharge system on the completeness and timeliness of discharge communication: a before and after study
by: Mehta, Rajnikant, et al.
Published: (2017)

Modularity and implementation of mathematical operational semantics
by: Jaskelioff, Mauro Javier, et al.
Published: (2008)

How does consumers' skepticism affect advertising claims?
by: Tien, Cheryl
Published: (2010)

Dato' Haji Sidek Haji Jamil / Nurul Nadrah Abdul Kader, Nur Shahidah Mohamad Ali and Siti Hajar Mat Arsat
by: Abdul Kader, Nurul Nadrah, et al.
Published: (2011)

Distributive laws in programming structures
by: Rypacek, Ondrej
Published: (2010)

New complexity results for the k-covers problem
by: Iliopoulos, Costas, et al.
Published: (2004)

New complexity results for the k-covers problem
by: Iliopoulos, Costas, et al.
Published: (2011)

A Novel Complete Reading Embedded System for the Vision Impaired
by: Nazemi, Azadeh, et al.
Published: (2012)

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

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

Monads need not be endofunctors
by: Altenkirch, Thorsten, et al.
Published: (2015)

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)

On the complexities of polymorphic stream equation systems, isomorphism of finitary inductive types, and higher homotopies in univalent universes
by: Sattler, Christian
Published: (2015)

Examine the Factors Influencing Brand-switching: the Effects of Advertising and Promotion
by: Luo, Xueling
Published: (2006)

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