Division by two, in homotopy type theory

DOI10.4230/LIPICS.FSCD.2022.11zbMATH Open1541.03024MaRDI QIDQ6544103FDOQ6544103

Authors: Samuel Mimram, Emile Oleon 

Publication date: 27 May 2024

Recommendations

• From multisets to sets in homotopy type theory
• The integers as a higher inductive type
• Homotopy canonicity for cubical type theory
• A Unified Formal Description of Arithmetic and Set Theoretical Data Types
• scientific article; zbMATH DE number 1420793

zbMATH Keywords

divisionaxiom of choiceset theoryhomotopy type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Axiom of choice and related propositions (03E25) Type theory (03B38)

This page was built for publication: Division by two, in homotopy type theory

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