[aa4262]: / thys / Category2 / document / root.tex  Maximize  Restore  History

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 % $Id: root.tex,v 1.2 2007-11-12 21:00:45 nipkow Exp$ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,isabellesym} \newcommand{\isasymemdash}{-} % further packages required for unusual symbols (see also isabellesym.sty) % use only when needed %\usepackage{amssymb} % for \, \, \, % \, \, \, % \, \, \, % \, \, % \, \, \ %\usepackage[greek,english]{babel} % greek for \, % english for \, % \ % default language = last %\usepackage[latin1]{inputenc} % for \, \, % \, \, % \, \, % \ %\usepackage[only,bigsqcap]{stmaryrd} % for \ %\usepackage{eufrak} % for \ ... \, \ ... \ % (only needed if amssymb not used) %\usepackage{textcomp} % for \, \ % this should be the last package used \usepackage{pdfsetup} % urls in roman style, theory text in math-similar italics \urlstyle{rm} \isabellestyle{it} \begin{document} \title{Category Theory} \author{Alexander Katovsky} \maketitle \begin{abstract} This article presents a development of Category Theory in Isabelle. A Category is defined using records and locales in Isabelle/HOL. Functors and Natural Transformations are also defined. The main result that has been formalized is that the Yoneda functor is a full and faithful embedding. We also formalize the completeness of many sorted monadic equational logic. Extensive use is made of the HOLZF theory in both cases. For an informal description see~\cite{apk}. \end{abstract} \tableofcontents % include generated text of all theories \input{session} \bibliographystyle{abbrv} \bibliography{root} \end{document}