From e2fa2f06f5bc03cda7604135bb219fc2742437a6 Mon Sep 17 00:00:00 2001 From: Tim Daly Date: Fri, 30 Jan 2015 06:45:25 -0500 Subject: axiom.sty introduce 'laws' environment for adding laws to categories %% This is the 'laws' environment for stating the laws that a category %% must obey (in theory). For example %% %% \begin{laws}{Category} %% \begin{enumerate} %% \item Left identity: id . f = f %% \item Right identity: f . id = f %% \item Associativity: f . (g . h) = (f . g) . h %% \end{enumerate} %% \end{laws} --- books/axiom.sty | 18 ++++++++++++++++++ books/bookvol10.2.pamphlet | 10 ++++++++++ changelog | 3 +++ patch | 14 +++++++++++++- src/axiom-website/patches.html | 2 ++ 5 files changed, 46 insertions(+), 1 deletions(-) diff --git a/books/axiom.sty b/books/axiom.sty index 1db076d..f5316df 100644 --- a/books/axiom.sty +++ b/books/axiom.sty @@ -545,6 +545,24 @@ \newcommand{\ranb}{{\tt ]}} \newcommand{\vertline}{$|$} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%% Axiom Proof Support +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%% This defines the proof support for Axiom. + +%% This is the 'laws' environment for stating the laws that a category +%% must obey (in theory). For example +%% +%% \begin{laws}{Category} +%% \begin{enumerate} +%% \item Left identity: id . f = f +%% \item Right identity: f . id = f +%% \item Associativity: f . (g . h) = (f . g) . h +%% \end{enumerate} +%% \end{laws} + +\def\laws#1{\vspace{1mm}\hrule\par\small\noindent{\bf #1 Laws:\\}} +\def\endlaws{\par\vspace{1mm}\hrule\vspace{1mm}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% Axiom Literate Programming Chunk Support diff --git a/books/bookvol10.2.pamphlet b/books/bookvol10.2.pamphlet index f3b3c74..8eb08ab 100644 --- a/books/bookvol10.2.pamphlet +++ b/books/bookvol10.2.pamphlet @@ -58,6 +58,16 @@ A ``yellow'' color indicates a domain. \pagehead{Category}{CATEGORY} \pagepic{ps/v102category.ps}{CATEGORY}{1.00} +\begin{laws}{Category} +\begin{itemize} +\item Left identity: id . f = f +\item Right identity: f . id = f +\item Associativity: f . (g . h) = (f . g) . h +\end{itemize} +\end{laws} +% NOTE: look up Kleisli categories (Maybe == Union?) +% http://stackoverflow.com/questions/2813259/why-do-we-need-monads + This is the root of the category hierarchy and is not represented by code. {\bf See:} diff --git a/changelog b/changelog index 9f086a5..b6974b6 100644 --- a/changelog +++ b/changelog @@ -1,3 +1,6 @@ +20150130 tpd src/axiom-website/patches.html 20150130.01.tpd.patch +20150130 tpd axiom.sty introduce 'laws' environment +20150130 tpd bookvol10.2 add laws to Category 20150129 tpd src/axiom-website/patches.html 20150129.01.tpd.patch 20150129 tpd books/bookvol13 add Lamport 21st Century Proofs paper 20150126 tpd src/axiom-website/patches.html 20150126.03.tpd.patch diff --git a/patch b/patch index 09b6421..c8c4b9b 100644 --- a/patch +++ b/patch @@ -1,2 +1,14 @@ -books/bookvol13 add Lamport 21st Century Proofs paper +axiom.sty introduce 'laws' environment for adding laws to categories + +%% This is the 'laws' environment for stating the laws that a category +%% must obey (in theory). For example +%% +%% \begin{laws}{Category} +%% \begin{enumerate} +%% \item Left identity: id . f = f +%% \item Right identity: f . id = f +%% \item Associativity: f . (g . h) = (f . g) . h +%% \end{enumerate} +%% \end{laws} + diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html index 08a952f..9c0a92c 100644 --- a/src/axiom-website/patches.html +++ b/src/axiom-website/patches.html @@ -4982,6 +4982,8 @@ bookvol10.4 MLIFT bug 7298: coercion to SUP failure in factor
buglist: bug 7299: docker image does not contain GCC
20150129.01.tpd.patch books/bookvol13 add Lamport 21st Century Proofs paper
+20150130.01.tpd.patch +axiom.sty introduce 'laws' environment
-- 1.7.5.4