Daniel Carranza

Photo of me taken by Jacqueline Doan

I am a 4th year undergradute student in mathematics at Western University under the supervision of Chris Kapulkin.

I am interested in logic, category theory, and homotopy theory. My most recent project was a construction of the type of two-adjoint equivalences in Homotopy Type Theory, formalized in Lean 3.

My email: dcarran@uwo.ca and my CV.

Research Experience

Paper 2-adjoint equivalences in homotopy type theory.
with J. Chang, C. Kapulkin, and R. Sandford,
Logical Methods in Computer Science 17 (2021), no. 1, Paper No. 3, 9pp.
[arXiv] [LMCS] [github]
Talks Formal Verification of Mathematics.
Canadian Undergradute Mathematics Conference 2020 (August 20, 2020)
[youtube]
Formalizing 2-Adjoint Equivalences in Homotopy Type Theory.
Western Homotopy Theory Seminar (August 18, 2020)
[youtube]

Awards and Scholarships

Extracurricular Activities

February 2020 Higher Categories and Categorification.
Research visit. Mathematical Sciences Research Institute.
Winter 2020 Directed Reading Program.
Category Theory. Western University.
October 2019 Midwest Homotopy Type Theory Seminar
University of Michigan.

Miscellaneous