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 automation.
Thanks, Haitao
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
