Division by two, in homotopy type theory

DOI10.4230/LIPICS.FSCD.2022.11MaRDI QIDQ6544103zbMATH OpenFDO

Authors Samuel Mimram, Emile Oleon

Publication date 27 May 2024

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)

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

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)