Title: Fibered Yoneda Lemma in Lean 4 Abstract: In this talk, I would like to give you a sense of what it’s like to do category theory in a computer. I use an interactive theorem prover called Lean4, a complex piece of software based on dependent type theory. In the first part, I will give a quick […]
Title: Calculus of fractions for quasicategories Abstract: A central object of interest in abstract homotopy theory is the localization of marked categories. One case of interest is when the marked category admits a "calculus of fractions". This condition was introduced by P. Gabriel and M. Zisman to construct better-behaved models for the localization. For instance, […]