Constructing inductive-inductive types in cubical type theory

DOI10.1007/978-3-030-17127-8_17OpenAlexW2932790846MaRDI QIDQ2289082FDOQ2289082

Authors: Jasper Hugunin 

Publication date: 28 January 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-17127-8_17

Recommendations

• On higher inductive types in cubical type theory
• For Finitary Induction-Induction, Induction is Enough
• Inductive types in homotopy type theory
• Inductive-inductive definitions
• Non-wellfounded trees in homotopy type theory

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Cited In (9)

• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• Title not available (Why is no real title available?)
• A construction method for induced types and its application to \(G_2\)
• Internal Parametricity for Cubical Type Theory
• Implementing Euclid's straightedge and compass constructions in type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Inductive Type Schemas as Functors
• For Finitary Induction-Induction, Induction is Enough

This page was built for publication: Constructing inductive-inductive types in cubical type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2289082)