It's been about two weeks since I started using HOL. I have been able to
develop a new axiomatization of category theory sufficient enough to prove
Yoneda lemma partially. I want to thank Michael Norrish and Thomas Tuerk
for their generosity in helping me with the learning process. I have gained
some fluency with the tactics but I hope to learn more about automation in
the future. For example arrow chasing in category theory may be amenable to

hol-info mailing list

Reply via email to