Finitary higher inductive types in the groupoid model

DOI10.1016/j.entcs.2018.03.019OpenAlexW2802510100WikidataQ113317560 ScholiaQ113317560MaRDI QIDQ2130587

Peter Dybjer, Hugo Moeneclaey

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.019

zbMATH Keywords

groupoidshomotopy type theoryidentity typesintuitionistic type theoryhigher inductive typessetoids

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

The construction of set-truncated higher inductive types ⋮ Bicategories in univalent foundations ⋮ Unnamed Item ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ A formal system of reduction paths for parallel reduction ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Inductive families
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Indexed induction-recursion
• Higher Inductive Types as Homotopy-Initial Algebras
• Positive Inductive-Recursive Definitions
• Inductive-Inductive Definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Internal type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Finitary higher inductive types in the groupoid model