×

Found 300 Documents (Results 1–100)

Coherence for monoidal groupoids in HoTT. (English) Zbl 07756113

Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 8, 20 p. (2020).
MSC:  03B70 68N30
PDFBibTeX XMLCite
Full Text: DOI

From cubes to twisted cubes via graph morphisms in type theory. (English) Zbl 07756110

Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 5, 18 p. (2020).
MSC:  03B70 68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv

Unifying cubical models of univalent type theory. (English) Zbl 07650827

Fernández, Maribel (ed.) et al., 28th EACSL annual conference on computer science logic, CSL 2020, Barcelona, Spain, January 13–16, 2020. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 152, Article 14, 17 p. (2020).
MSC:  68-XX 03B70
PDFBibTeX XMLCite
Full Text: DOI

Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03036

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 929-943 (2020).
MSC:  03B38 18N10 55U35
PDFBibTeX XMLCite
Full Text: DOI

A constructive model of directed univalence in bicubical sets. (English) Zbl 1498.03038

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 915-928 (2020).
PDFBibTeX XMLCite
Full Text: DOI

Sequential colimits in homotopy type theory. (English) Zbl 1498.03035

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 845-858 (2020).
MSC:  03B38 55U35 18N45
PDFBibTeX XMLCite
Full Text: DOI

Partial univalence in \(n\)-truncated type theory. (English) Zbl 1498.03034

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 807-819 (2020).
MSC:  03B38 55U35 18N45
PDFBibTeX XMLCite
Full Text: DOI arXiv

Coherence via well-foundedness. Taming set-quotients in homotopy type theory. (English) Zbl 1498.03033

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 662-675 (2020).
MSC:  03B38 55U35 20E05
PDFBibTeX XMLCite
Full Text: DOI arXiv

The integers as a higher inductive type. (English) Zbl 1498.03028

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 67-73 (2020).
MSC:  03B38 55U35 18N45
PDFBibTeX XMLCite
Full Text: DOI arXiv

A higher structure identity principle. (English) Zbl 1498.03027

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 53-66 (2020).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Models of HoTT and the constructive view of theories. (English) Zbl 1528.03112

Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 191-219 (2019).
PDFBibTeX XMLCite
Full Text: DOI

Univalent foundations and the unimath library. (English) Zbl 1528.03104

Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 173-189 (2019).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Higher structures in homotopy type theory. (English) Zbl 1528.03105

Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 151-172 (2019).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Univalent foundations and the equivalence principle. (English) Zbl 1528.03101

Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 137-150 (2019).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing. (English) Zbl 1528.03114

Dybjer, Peter (ed.) et al., 24th international conference on types for proofs and programs, TYPES 2018, Braga, Portugal, June 18–21, 2018. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 130, Article 7, 20 p. (2019).
PDFBibTeX XMLCite
Full Text: DOI arXiv

Homotopy canonicity for cubical type theory. (English) Zbl 1528.03106

Geuvers, Herman (ed.), 4th international conference on formal structures for computation and deduction, FSCD 2019, Dortmund, Germany, June 24–30, 2019. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 131, Article 11, 23 p. (2019).
MSC:  03B38 03G30 55U35
PDFBibTeX XMLCite
Full Text: DOI

From mathesis universalis to provability, computability, and constructivity. (English) Zbl 1469.03113

Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 203-234 (2019).
PDFBibTeX XMLCite
Full Text: DOI

Mathesis universalis and homotopy type theory. (English) Zbl 1469.03035

Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 13-36 (2019).
MSC:  03B38 55U40
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

Database

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software