scholarly journals Indexed type theories

2020 ◽  
pp. 1-61
Author(s):  
Valery Isaev
Keyword(s):  
Homotopy Type ◽  
Orthogonal Factorization ◽  
Inductive Types ◽  
Indexed Categories

Abstract In this paper, we define indexed type theories which are related to indexed (∞-)categories in the same way as (homotopy) type theories are related to (∞-)categories. We define several standard constructions for such theories including finite (co)limits, arbitrary (co)products, exponents, object classifiers, and orthogonal factorization systems. We also prove that these constructions are equivalent to their type theoretic counterparts such as Σ-types, unit types, identity types, finite higher inductive types, Π-types, univalent universes, and higher modalities.

scholarly journals Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018 ◽  
Author(s):  
Michael Shulman
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Synthetic Approach ◽  
Homotopy Type Theory ◽  
Inductive Types ◽  
Basic Ideas ◽  
Univalent Foundations ◽  
Modern Mathematics

Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.

scholarly journals Modal descent

2020 ◽  
pp. 1-29
Author(s):  
Felix Cherubini ◽  
Egbert Rijke
Keyword(s):  
Homotopy Type ◽  
Type Theory ◽  
Orthogonal Factorization ◽  
Simple Description ◽  
Factorization System ◽  
Homotopy Type Theory ◽  
Orthogonal Factorization System ◽  
The Right ◽  
Special Case

Abstract Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated with any modality, of which the left class is the class of ○-equivalences and the right class is the class of ○-étale maps. This factorization system is called the modal reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the modal reflective factorization system of a modality. In the special case of the n-truncation, the modal reflective factorization system has a simple description: we show that the n-étale maps are the maps that are right orthogonal to the map $${\rm{1}} \to {\rm{ }}{{\rm{S}}^{n + 1}}$$ . We use the ○-étale maps to prove a modal descent theorem: a map with modal fibers into ○X is the same thing as a ○-étale map into a type X. We conclude with an application to real-cohesive homotopy type theory and remark how ○-étale maps relate to the formally etale maps from algebraic geometry.

scholarly journals FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY

2018 ◽  
Vol 83 (3) ◽  
pp. 1132-1146 ◽  
Author(s):  
HÅKON ROBBESTAD GYLTERUD
Keyword(s):  
Set Theory ◽  
Homotopy Type ◽  
Type Theory ◽  
Homotopy Type Theory ◽  
Constructive Set Theory ◽  
Inductive Types ◽  
Univalent Foundations

AbstractWe give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel’s 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of “Homotopy Type Theory” by the Univalent Foundations Program.

scholarly journals Homotopical patch theory

2016 ◽  
Vol 26 ◽  
Author(s):  
CARLO ANGIULI ◽  
EDWARD MOREHOUSE ◽  
DANIEL R. LICATA ◽  
ROBERT HARPER
Keyword(s):  
Control Systems ◽  
Homotopy Type ◽  
Category Theory ◽  
Type Theory ◽  
Homotopy Theory ◽  
New Class ◽  
Homotopy Type Theory ◽  
Inductive Type ◽  
Higher Category Theory ◽  
Inductive Types

AbstractHomotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type is proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.

The smooth case

2017 ◽  
Author(s):  
Ehud Hrushovski ◽  
François Loeser
Keyword(s):  
Homotopy Type ◽  
Unit Vector ◽  
Smooth Case ◽  
Open Set ◽  
Birational Invariant

This chapter examines the simplifications occurring in the proof of the main theorem in the smooth case. It begins by stating the theorem about the existence of an F-definable homotopy h : I × unit vector X → unit vector X and the properties for h. It then presents the proof, which depends on two lemmas. The first recaps the proof of Theorem 11.1.1, but on a Zariski dense open set V₀ only. The second uses smoothness to enable a stronger form of inflation, serving to move into V₀. The chapter also considers the birational character of the definable homotopy type in Remark 12.2.4 concerning a birational invariant.

Fast Multi-View Clustering via Nonnegative and Orthogonal Factorization

2020 ◽  
pp. 1-1
Author(s):  
Ben Yang ◽  
Xuetao Zhang ◽  
Feiping Nie ◽  
Fei Wang ◽  
Weizhong Yu ◽  
...  
Keyword(s):  
Orthogonal Factorization

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

2021 ◽  
Vol 31 ◽  
Author(s):  
ANDREA VEZZOSI ◽  
ANDERS MÖRTBERG ◽  
ANDREAS ABEL
Keyword(s):  
Programming Language ◽  
Type Theory ◽  
Type Checking ◽  
Dependent Type Theory ◽  
Wide Range ◽  
General Schema ◽  
Direct Definition ◽  
Inductive Types ◽  
Definition Of ◽  
Cubical Type Theory

Abstract Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types (HITs). This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

Sign in / Sign up

Export Citation Format

Share Document