|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
#######
#
# E-scripts on programs for math, and on some electronic papers and books.
#
# Note 1: use the eev command (defined in eev.el) and the
# ee alias (in my .zshrc) to execute parts of this file.
# Executing this file as a whole makes no sense.
# An introduction to eev can be found here:
#
# (find-eev-quick-intro)
# http://angg.twu.net/eev-intros/find-eev-quick-intro.html
#
# Note 2: be VERY careful and make sure you understand what
# you're doing.
#
# Note 3: If you use a shell other than zsh things like |&
# and the for loops may not work.
#
# Note 4: I always run as root.
#
# Note 5: some parts are too old and don't work anymore. Some
# never worked.
#
# Note 6: the definitions for the find-xxxfile commands are on my
# .emacs.
#
# Note 7: if you see a strange command check my .zshrc -- it may
# be defined there as a function or an alias.
#
# Note 8: the sections without dates are always older than the
# sections with dates.
#
# This file is at <http://angg.twu.net/e/math.e>
# or at <http://angg.twu.net/e/math.e.html>.
# See also <http://angg.twu.net/emacs.html>,
# <http://angg.twu.net/.emacs[.html]>,
# <http://angg.twu.net/.zshrc[.html]>,
# <http://angg.twu.net/escripts.html>,
# and <http://angg.twu.net/>.
#
#######
# «.barr_wells» (to "barr_wells")
# «.ND_in_categories» (to "ND_in_categories")
# «.SDG» (to "SDG")
# «.nat_ops_in_gdif» (to "nat_ops_in_gdif")
# «.octave» (to "octave")
# «.octave_eeg2_demo» (to "octave_eeg2_demo")
# «.geomview» (to "geomview")
# «.qhull» (to "qhull")
# «.roots_poly» (to "roots_poly")
# «.octave-ode-solvers» (to "octave-ode-solvers")
# «.catlist» (to "catlist")
# «.xxx.lanl.gov» (to "xxx.lanl.gov")
# «.blas» (to "blas")
# «.SGA1» (to "SGA1")
# «.wdtp» (to "wdtp")
# «.winplot» (to "winplot")
# «.catsters» (to "catsters")
# «.catsters-code» (to "catsters-code")
# «.youtube-dl» (to "youtube-dl")
# «.gsl» (to "gsl")
# «.cat-dist» (to "cat-dist")
# «.encyclopedia-of-psyss» (to "encyclopedia-of-psyss")
# «.provas-MD-naufel» (to "provas-MD-naufel")
# «.naturality» (to "naturality")
# «.notacao-de-fisicos» (to "notacao-de-fisicos")
# «.bortolossi» (to "bortolossi")
# «.material-para-GA» (to "material-para-GA")
# «.material-para-GA-git» (to "material-para-GA-git")
# «.joshua-meyers» (to "joshua-meyers")
# «.presheaves-calc» (to "presheaves-calc")
# «.2020.1-videos-C2-C3» (to "2020.1-videos-C2-C3")
# «.hassediagram» (to "hassediagram")
# «.silvanus-thompson» (to "silvanus-thompson")
# «.desmos» (to "desmos")
# «.mathlingua» (to "mathlingua")
# «.dslsofmath» (to "dslsofmath")
# «.on-the-missing» (to "on-the-missing")
# «.mapcabral-c1v» (to "mapcabral-c1v")
# «.mapcabral-ar» (to "mapcabral-ar")
# «.goldfeld-al» (to "goldfeld-al")
# «.reamat-al» (to "reamat-al")
# «.reamat-c1v» (to "reamat-c1v")
# «.reamat-c0» (to "reamat-c0")
#####
#
# Barr & Wells' book ("Toposes, Triples and Theories")
# 2000nov24
#
#####
# «barr_wells» (to ".barr_wells")
# (find-angg ".emacs.papers" "barr")
# http://www.cwru.edu/artsci/math/wells/pub/ttt.html
# http://www.cwru.edu/artsci/math/wells/pub/dvi/tttdvi.zip
#*
cd $S/http/www.cwru.edu/artsci/math/wells/pub/dvi/
unzip -l tttdvi.zip
unzip tttdvi.zip
#*
# (find-fline "$S/http/www.cwru.edu/artsci/math/wells/pub/dvi/")
# (find-dvipage "$S/http/www.cwru.edu/artsci/math/wells/pub/dvi/tt.dvi" 1)
# (code-dvi "ttt" "$S/http/www.cwru.edu/artsci/math/wells/pub/dvi/tt.dvi")
# (find-tttpage (+ 14 98))
#*
xdvi $S/http/www.cwru.edu/artsci/math/wells/pub/dvi/tt.dvi &
#*
#####
#
# Papers (most are related to semantics)
# 2001feb05
#
#####
# «ND_in_categories» (to ".ND_in_categories")
# Barry Jay '96(?): Covariant Types (19p.)
gv $S/http/www-staff.it.uts.edu.au/~cbj/Publications/covariant_types.ps.gz &
#
# Jay/Moggi/Bellè '98(?): Functors, Types and Shapes (4p.)
gv $S/http/www-staff.it.uts.edu.au/~cbj/Publications/functors_and_shapes.ps.gz&
#
# Barry Jay '98(?): The FISh Language Definition (30p.)
gv $S/http/www-staff.it.uts.edu.au/~cbj/Publications/latest_fish.ps.gz &
#
# Jansson '00: Functional Polytypic Programming (190p.)
gv $S/http/www.cs.chalmers.se/~patrikj/poly/polythesis/polythesis.ps.gz &
#
# Bellè/Jay/Moggi '96: Functorial ML (28p.)
gv $S/http/www.disi.unige.it/person/MoggiE/ftp/plilp96.ps.gz &
#
# Fegaras '96: Fusion for Free!
gv $S/ftp/cse.ogi.edu/pub/tech-reports/1996/96-001.ps.gz
# Wadler '90(?): The Girard-Reynolds Isomorphism (14p.)
gv $S/http/www.cs.bell-labs.com/who/wadler/papers/gr/gr.ps.gz &
#
# Mairson '91(?): Outline of a Proof Theory of Polymorphism (15p.)
gv $S/http/www.cs.brandeis.edu/~mairson/Papers/para.ps.gz &
# Selinger '99: Control Categories and Duality: on the Categorical
# Semantics of the Lambda-Mu Calculus (53p.)
gv $S/ftp/ftp.math.lsa.umich.edu/pub/selinger/control.ps.gz &
# Uustalu/Vene '00(?): Least and Greatest Fixed Points in
# Intuitionistic Natural Deduction (28p.)
gv $S/http/www.cs.ioc.ee/~tarmo/papers/ttp-tokyo97.ps.gz &
# Wadler: Deforestation: Transforming Programs to Eliminate Trees (19p.)
gv $S/http/cm.bell-labs.com/who/wadler/papers/deforest/deforest.ps.gz &
# Sheard '93: Type Parametric Programming (13p.)
xdvi $S/http/www.cse.ogi.edu/~sheard/papers/typeparam.dvi &
# Sheard/Benaissa/Pasalic: DSL Implementation Using Staging and Monads (14p.)
gv $S/http/www.cse.ogi.edu/~sheard/papers/dsl99.ps &
# Moggi/Bellè/Jay '99: Monads, Shapely Functors, and Traversals (23p.)
gv $S/http/www.disi.unige.it/person/MoggiE/ftp/ctcs99.ps.gz &
# Moggi: Functor Categories and Two-Level Languages (15p.)
gv $S/http/www.disi.unige.it/person/MoggiE/ftp/fossacs98.ps.gz &
# Jay/Bellè/Moggi: Functorial ML (49p.)
gv $S/http/www.disi.unige.it/person/MoggiE/ftp/jfp98.ps.gz &
# Mitchell/Moggi: Kripke-Style for Typed Lambda Calculus (32p.)
gv $S/http/www.disi.unige.it/person/MoggiE/ftp/kripke.ps.gz &
# Blute/Scott '95: Linear Läuchli Semantics (44p.)
zxdvi $S/http/hypatia.dcs.qmw.ac.uk/data/S/ScottPJ/lauchli.dvi.gz &
#
# Cubric/Dybjer/Scott: Normalization and the Yoneda Embedding (39p.)
zxdvi $S/http/hypatia.dcs.qmw.ac.uk/data/S/ScottPJ/Yoneda_nf.dvi.Z &
#
# Girard/Scedrov/Scott '92: Normal Forms and Cut-Free Proofs as
# Natural Transformations (25p.)
zxdvi $S/http/hypatia.dcs.qmw.ac.uk/data/S/ScottPJ/nf_gss.dvi.gz &
# Jay: Coherence in Category Theory and the Church-Rosser Property (4p.)
gv $S/http/www-staff.it.uts.edu.au/~cbj/Publications/coherence+CR.ps.gz &
# Palsberg/Jay/Noble: Experiments with Generic Visitors (4p.)
gv $S/http/www-staff.it.uts.edu.au/~cbj/Publications/generic_visitors.ps.gz &
# B. Howard: Inductive, Coinductive and Pointed Types (7p.)
gv http://www.cis.ksu.edu/~bhoward/ftp/icfp.ps.Z &
# Wadler: Proofs are Programs: 19th Century Logic and 21st Century Computing
# (explains a little bit of Frege's notation; 14p.)
xpdf $S/http/www.cs.bell-labs.com/who/wadler/papers/frege/frege.pdf &
# Musty/Shenoy: Intuitionistic Type Theory -- Predicate Logic
# (student paper mentioning Martin-Löf's type theory)
gv $S/http/www.cis.ksu.edu/~stefan/Teaching/CIS705/Reports/MusShe-1.pdf &
# Telford: Static Analysis of Martin-Löf's Intuitionistic Type Theory (246p.)
gv $S/http/www.cs.ukc.ac.uk/pubs/1995/500/content.ps.gz &
# Hedberg: A coherence theorem for Martin-Löf's type theory
gv $S/http/www.cs.chalmers.se/~hedberg/coh.ps &
# Oops, I don't have this file...
zxdvi $S/ftp/ftp.diku.dk/pub/diku/users/tofte/tips.dvi.Z &
# Richman: The Fundamental Teorem of Algebra: A Constructive
# Development Without Choice (18p.)
xdvi $S/http/nyjm.albany.edu/PacJ/p/2000/196-1-10.hdvi &
gv $S/ftp/ftp.imf.au.dk/pub/kock/princ4.ps &
gv $S/http/www.cs.cmu.edu/~bp/KreitzPientka00.ps &
gv $S/http/www.cs.cmu.edu/~fp/papers/tlca99.ps.gz &
gv $S/http/www.cse.ogi.edu/~jlewis/implicit.ps.gz &
http://www.dina.kvl.dk/~sestoft/mosml.html
http://www.disi.unige.it/person/MoggiE/publications.html
http://www.dm.uba.ar/prof2.html
http://www.dms.umontreal.ca/Professeurs/reyes/
http://www.emis.de/journals/short_index.html
http://www.emis.de/monographs/KSM/index.html
http://www.emis.de/monographs/KSM/kmsbookh.dvi.gz
http://www.ftp.cl.cam.ac.uk/ftp/hvg/qed-project-archive/Manifesto
http://www.math.lsa.umich.edu/~ablass/
http://www.math.ucla.edu/~asl/bussproofs.sty
http://www.math.uiuc.edu/K-theory/0201/sheafcoho.dvi.gz
http://www.math.uu.nl/people/moerdijk/index.html
http://www.math.uu.se/~palmgren/index-eng.html
http://www.math.uu.se/~palmgren/publicat.html
http://www.maths.mq.edu.au/~street/LackLemma.html
http://www.maths.mq.edu.au/~street/Publications.html
http://www.maths.mq.edu.au/~street/
http://www.maths.sussex.ac.uk/Staff/GCW/
http://www.tac.mta.ca/tac/cahiers/index.html
http://www.tac.mta.ca/tac/volumes/1998/n9/n9.dvi
http://www.tac.mta.ca/tac/volumes/6/n9/n9.dvi
http://www.wraith.u-net.com/JTrivStud/index.html
http://www.wraith.u-net.com/JTrivStud/riley.dvi
http://www.wraith.u-net.com/Mum/Works.html
http://www.wraith.u-net.com/
http://www.wraith.u-net.com/whs.txt
http://www.cs.ukc.ac.uk/people/staff/cr3/toolbox/haskell/
http://www.mozart-oz.org/
http://www.informatik.uni-kiel.de/~pakcs/
http://www.acm.org/pubs/citations/proceedings/fp/351240/p280-jones/
http://www.dcs.ed.ac.uk/home/cvr/
#####
#
# Walter Moreira: SDG
#
#####
# «SDG» (to ".SDG")
# (find-shttpw3 "www.cmat.edu.uy/~walterm/")
gv $S/http/www.cmat.edu.uy/~walterm/works/sdg.ps.gz
# Paula Severi+Erik Poll: Pure Type Systems with Definitions
# (find-shttpw3 "www.cmat.edu.uy/~severi/publications.html")
# (find-shttpw3 "www.cmat.edu.uy/~severi/cs.html")
gv $S/ftp/ftp.win.tue.nl/pub/techreports/severi/defs.ps.Z
#####
#
# Kolar, Slovak, Michor: "Natural operations in differential geometry"
# 2001jan13
#
#####
# «nat_ops_in_gdif» (to ".nat_ops_in_gdif")
# (find-shttpw3 "www.emis.de/monographs/KSM/index.html")
#*
zxdvi $S/http/www.emis.de/monographs/KSM/kmsbookh.dvi.gz &
#*
cd /tmp/
zcat $S/http/www.emis.de/monographs/KSM/kmsbookh.dvi.gz > kmsbookh.dvi
dvifonts kmsbookh.dvi | sort | tee ~/o
# Some fonts are missing: lams1, lams2, lams3, lams4
# (They are used in diagrams, at least).
#*
#####
#
# Programação linear
#
#####
apti libwn6 libwn-dev octave-sp
apti pcx
# (find-vldifile "libwn6.list")
# (find-fline "/usr/doc/libwn6/")
# (find-vldifile "libwn-dev.list")
# (find-fline "/usr/doc/libwn-dev/")
# (eeman "wnsplx")
# (find-vldifile "octave-sp.list")
# (find-fline "/usr/doc/octave-sp/")
cd /usr/doc/octave-sp/
for i in doc.ps semidef_prog.ps; do gzip -cd < $i.gz > /tmp/$i; done
cd /tmp/
gv doc.ps
gv semidef_prog.ps
#####
#
# Octave
# 2000sep15
#
#####
# «octave» (to ".octave")
# (find-es "octave")
# (find-status "octave")
# (find-vldifile "octave.list")
# (find-fline "/usr/doc/octave/")
# (code-c-d "oct" "/usr/share/octave/2.0.16/m/" "octave")
# (find-octfile "")
# (find-octnode "Top")
# (find-node "(octave)Top")
# (find-node "(Octave-FAQ)Top")
# (find-node "(liboctave)Top")
#*
zcatinfo /usr/share/info/octave > /tmp/oct.info
agrep -i lapack /tmp/oct.info
# (find-fline "/tmp/oct.info" '* 3 "standard LAPACK")
#*
# (find-node "(octave)Index Expressions")
# (find-node "(octave)Simple Examples")
# (find-node "(octave)Script Files")
octave <<'---'
a = [1,2;3,4]
a*a
---
#*
cat > /tmp/simple.m <<'---'
1;
function xdot = f (x, t)
r = 0.25;
k = 1.4;
a = 1.5;
b = 0.16;
c = 0.9;
d = 0.8;
xdot(1) = r*x(1)*(1 - x(1)/k) - a*x(1)*x(2)/(1 + b*x(1));
xdot(2) = c*a*x(1)*x(2)/(1 + b*x(1)) - d*x(2);
endfunction
x0 = [1; 2];
t = linspace (0, 50, 200)';
x = lsode ("f", x0, t);
# use_plplot
plot (t, x)
keyboard
---
octave /tmp/simple.m
#*
# (find-node "(octave)Basic Matrix Functions")
# (find-node "(octave)Matrix Factorizations")
cat > $EEG <<'---'
a = [1, 2, 3;
0, 5, 4;
7, 8, 9]
lu(a)
[l, u, p] = lu(a)
---
eeg octave
#*
# «octave_eeg2_demo» (to ".octave_eeg2_demo")
# (find-node "(octave)Customizing the Prompt")
# (find-node "(octave)Startup Files")
# (find-fline "~/.octaverc")
#PS1 = "%%> "
#PS2 = "%> "
cat > $EEG <<'---'
function xdot = f (x, t)
r = 0.25;
k = 1.4;
a = 1.5;
b = 0.16;
c = 0.9;
d = 0.8;
xdot(1) = r*x(1)*(1 - x(1)/k) - a*x(1)*x(2)/(1 + b*x(1));
xdot(2) = c*a*x(1)*x(2)/(1 + b*x(1)) - d*x(2);
endfunction
x0 = [1; 2];
t = linspace (0, 50, 200)';
x = lsode ("f", x0, t);
# use_plplot
# plot (t, x)
quit
---
eeg -c '
set prompt {%> }
set fast 1
exec rm -f /tmp/o; exp_internal -f /tmp/o 0
' octave
#*
#####
#
# geomview (slink)
# 99nov08
#
#####
# «geomview» (to ".geomview")
apti geomview
# (find-vldifile "geomview.list")
# (find-node "(geomview)Top")
# (find-fline "/usr/doc/geomview/")
# (find-fline "/usr/doc/geomview/oogltour" "Polylist file format")
# (find-fline "/usr/doc/geomview/examples/")
# (find-fline "/usr/doc/geomview/examples/example4.tcl")
lynx /usr/doc/geomview/html/geomview_toc.html
edrxnetscape /usr/doc/geomview/html/geomview_toc.html &
lynx /usr/doc/geomview/html/geomview_8.html#SEC58
# (find-fline "/usr/doc/geomview/geomview.tex" "C, perl, tcl/tk")
# (find-node "(geomview)Example4")
# (find-fline "/usr/lib/geomview/modules/")
# (find-fline "/usr/lib/geomview/modules/tcl/")
#####
#
# qhull
# 99nov08
#
#####
# «qhull» (to ".qhull")
rm -Rv /usr/src/qhull/
cd /usr/src/
tar -xvzf $S/ftp/ftp.geom.umn.edu/pub/software/qhull.tar.Z
cd /usr/src/qhull/
make |& tee om
# (find-fline "/usr/src/qhull/")
# (find-fline "/usr/src/qhull/README.txt" "if you have Geomview")
# (find-fline "/usr/src/qhull/qhull.txt")
# (find-fline "/usr/src/qhull/q_eg")
# - try 'rbox 100 | qhull G >a' and load 'a' into Geomview
# - run 'q_eg' for Geomview examples of Qhull output (see qh-eg.htm)
rm -Rv /tmp/qhull/
mkdir /tmp/qhull/
cd /usr/src/qhull/
rbox 100 | tee /tmp/qhull/a3d.rbox | qhull G > /tmp/qhull/a3d
rbox D4 12 | tee /tmp/qhull/a4d.rbox | qhull G > /tmp/qhull/a4d
cd /usr/src/qhull/
q_eg |& tee /tmp/qhull/oqeg
mv -v eg.* /tmp/qhull
# (find-fline "/tmp/qhull/")
cd /tmp/qhull/
geomview
geomview /tmp/qhull/a3d
geomview /tmp/qhull/a4d
# Problema do Leonardo Lustosa (politopo estranho):
# (find-fline "/tmp/qhull/")
# (find-fline "/tmp/qhull/a3d.rbox")
cd /usr/src/qhull/
expect -c '
proc ang {frac} {expr 2*3.14159265*$frac}
set n 200
set oscs 3
puts "3 rbox $n"
puts "$n"
for {set i 0} {$i<$n} {incr i} {
puts "[expr cos([ang $i/$n])] [expr sin([ang $i/$n])] [expr sin([ang $i/$n*$oscs])]"
}
' | tee /tmp/qhull/garagem.rbox \
| qhull G > /tmp/qhull/garagem
geomview /tmp/qhull/garagem
#####
#
# cdd+
# 99nov08
#
#####
apti gmp2 gmp2-dev
apti libg++2.8.2 libg++2.8.2-dev
apti g++
rm -Rv /usr/src/cdd+-076a1/
cd /usr/src/
tar -xvzf $S/ftp/ftp.ifor.math.ethz.ch/pub/fukuda/cdd/cdd+-076a1.tar.gz
cd /usr/src/cdd+-076a1/
# (code-c-d "cdd+" "/usr/src/cdd+-076a1/")
# (find-cdd+file "README.cdd+")
# (find-cdd+file "makefile")
# The default is to use -O3, but I just want to compile fast and run the demos
make CC=g++ \
GMPUSED=TRUE GMPLIB=/usr/lib RATLIB=gmp2 GMPINCLUDEDIR=/usr/include/gmp2 \
OPTFLAGS= all \
|& tee om
latex cddman.tex
latex cddman.tex
latex cddman.tex
rm -Rv /tmp/cdd/
mkdir /tmp/cdd/
cd /usr/src/cdd+-076a1/
cp -v ext/ccc4.ext /tmp/cdd
cp -v ine/ucube.ine /tmp/cdd/
cddr+_gmp /tmp/cdd/ucube.ine |& tee /tmp/cdd/ocu
cddr+_gmp /tmp/cdd/ccc4.ext |& tee /tmp/cdd/occ
# (find-fline "/tmp/cdd/")
# (find-cdd+file "")
# (find-cdd+file "cddman.tex" "qhull")
# (find-cdd+file "ext/")
# (find-cdd+file "ine/")
# (find-cdd+file "om")
# Old notes:
# (find-fline "$S/ftp/ftp.ifor.math.ethz.ch/pub/fukuda/cdd/cddlib-085.tar.gz")
Pgrep m/gmp/ > ~/o
# (find-fline "~/o")
cd ~/SLINK/
echo *g++*
echo *gmp*
getlinks < $S/http/www.ifor.math.ethz.ch/ifor/staff/fukuda/cdd_home/cdd.html
#####
#
# Roots of a complex polynomial
#
#####
# «roots_poly» (to ".roots_poly")
# (code-c-d "oct" "/usr/src/octave-2.0.13.95/" "octave")
# (find-octnode "Polynomial Manipulations" "roots (V)")
# (find-octnode "Functions and Scripts")
#*
cat > $EEG <<'---'
r = roots([1, 4, 6, 4, 1]);
r = roots([1, 4, 6, 4, 1])
---
eeg octave
#*
# (find-status "octave")
# (find-vldifile "octave.list")
# (find-fline "/usr/doc/octave/")
# (find-vldifile "octave.list")
# (find-fline "/usr/doc/octave/")
pdsc /big/slinks2/dists/slink/main/source/math/octave_2.0.13.95-1.dsc
# (find-octfile "scripts/polynomial/roots.m")
# (find-octfile "doc/faq/")
#####
#
# octave-ode-solvers (ctellez)
#
#####
# «octave-ode-solvers» (to ".octave-ode-solvers")
# (find-fline "~/OCTAVE/")
# (code-c-d "octos" "/usr/src/octave_ode_solvers_v1.0/")
rm -Rv /usr/src/octave_ode_solvers_v1.0/
cd /usr/src/
tar -xvzf $S/http/www.mat.puc-rio.br/~edrx/tmp/octave_ode_solvers_v1.0.tar.gz
cd /usr/src/octave_ode_solvers_v1.0/
octave pendulum.m
# (find-octosfile "")
#####
#
# saml
# 2000sep09
#
#####
# (find-status "saml")
# (find-vldifile "saml.list")
# (find-fline "/usr/doc/saml/")
Pgrepp m/saml/ |& l
#####
#
# The "categories" mailing list
# 2000nov26
#
#####
# «catlist» (to ".catlist")
# (find-fline "/tmp/")
# (find-fline "/tmp/categories/tac.mta.ca/pub/categories/")
# (find-sftpfile "tac.mta.ca/pub/categories/")
#####
#
# xxx.lanl.gov: Yanofsky's "The Syntax of Coherence"
# 2000nov26
#
#####
# «xxx.lanl.gov» (to ".xxx.lanl.gov")
http://xxx.lanl.gov/dvi/math/9910006
# "The syntax of coherence":
# (w3-fetch "http://xxx.lanl.gov/dvi/math/9910006")
# (find-shttpfile "xxx.lanl.gov/dvi/math/9910006/")
# (find-shttpw3 "arxiv.org/abs/math/9910006/")
# (find-shttpfile "arxiv.org/abs/math/9910006/9910006.tex")
#*
cp -v $S/http/arxiv.org/abs/math/9910006/9910006.tex ~/tmp/
cd ~/tmp/
patch -p0 <<'%%%' 9910006.tex
1c1,2
< \documentstyle[10pt]{article}
---
> %\documentstyle[10pt]{article}
> \documentstyle{article}
%%%
latex 9910006.tex
latex 9910006.tex
#*
# (find-fline "~/tmp/9910006.tex")
# (find-fline "~/tmp/9910006.tex" "\\xymatrix")
#####
#
# blas
# 2001feb14
#
#####
# «blas» (to ".blas")
# (find-fline "/usr/doc/blas-dev/")
# (find-fline "/usr/doc/blas1/")
# (find-fline "/usr/doc/lapack-dev/")
# (find-fline "/usr/doc/lapack/")
# (find-status "blas-dev")
# (find-status "blas1")
# (find-status "lapack-dev")
# (find-status "lapack")
# (find-vldifile "blas-dev.list")
# (find-vldifile "blas1.list")
# (find-vldifile "lapack-dev.list")
# (find-vldifile "lapack.list")
# (find-fline "/usr/doc/f2c/")
# (find-fline "/usr/doc/f77reorder/")
# (find-fline "/usr/doc/fort77/")
# (find-status "f2c")
# (find-status "f77reorder")
# (find-status "fort77")
# (find-vldifile "f2c.list")
# (find-vldifile "f77reorder.list")
# (find-vldifile "fort77.list")
#*
pdsc $SDEBIAN/dists/potato/main/source/libs/blas_1.0-3.2.dsc
cd /usr/src/blas-1.0/
#debian/rules binary |& tee odrb
#debian/rules binary F77=f77reorder |& tee odrb
#debian/rules binary F77=f77-f77reorder |& tee odrb
debian/rules binary F77=fort77 |& tee odrb
# Everything ok but this:
# dh_gencontrol -a
# dpkg-gencontrol: error: current build architecture i386 does not
# appear in package's list (alpha)
#*
# (code-c-d "blas" "/usr/src/blas-1.0/")
# (find-blasfile "debian/")
# (find-blasfile "debian/rules" "until g77")
#####
#
# Grothendieck's SGA1
# 2003jan17
#
#####
# «SGA1» (to ".SGA1")
# (find-es "tex" "enlarge-pool_size")
lynx http://arxiv.org/format/math.AG/0206203
# (find-fline "$S/http/arxiv.org/ftp/math/papers/0206/0206203.tar.gz")
#*
rm -Rv /tmp/sga1/
mkdir /tmp/sga1/
cd /tmp/sga1/
tar -xvzf $S/http/arxiv.org/ftp/math/papers/0206/0206203.tar.gz
cp -iv sga1.tex sga1.tex.orig
# (find-fline "/tmp/sga1/sga1.tex" "`2000'")
# (find-fline "/tmp/sga1/sga1.tex" "corrected version.")
# (find-angg ".zshrc" "mydiff")
patch -p0 sga1.tex <<'%%%'
74c74,75
< \setboolean{orig}{true}
---
> %\setboolean{orig}{true}
> \setboolean{orig}{false}
99,100c100,101
< \usepackage{amsmath2000}
< %\usepackage{amsmath}
---
> %\usepackage{amsmath2000}
> \usepackage{amsmath}
109,110c110,111
< \usepackage{amscd2000}
< %\usepackage{amscd}
---
> %\usepackage{amscd2000}
> \usepackage{amscd}
%%%
# (find-fline "/tmp/sga1/")
# (find-fline "/tmp/sga1/sga1.tex" "latex sga1.tex")
#*
cd /tmp/sga1/
latex sga1.tex
latex sga1.tex
latex sga1.tex
cp -iv junk/*.ist .
makeindex -s term.ist -o sga1.term sga1.tindex
makeindex -s not.ist -o sga1.not sga1.nindex
latex sga1.tex
latex sga1.tex
#*
# (find-angg ".emacs" "papers" "sga1")
cp /tmp/sga1/sga1.dvi ~/tmp/sga1-corrected.dvi
#*
#####
#
# Wagner Dias Tableau Prover
# 2009apr23
#
#####
# «wdtp» (to ".wdtp")
# (find-angg ".emacs.papers" "dagostino")
# http://www.dainf.ct.utfpr.edu.br/wiki/index.php/WDTP_-_Wagner_Dias_Tableau_Prover
# http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/DissertacaoMestradoWagnerDias.pdf
# http://www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/project-tableau-linux.zip
#*
rm -Rv ~/usrc/project-tableau-linux/
unzip -d ~/usrc/ \
$S/http/www.dainf.ct.utfpr.edu.br/~adolfo/etc/Software/WDTP/project-tableau-linux.zip
cd ~/usrc/project-tableau-linux/
rm -fv *.gch
rm -fv *.o prove php h gamma statman
# make clean |& tee omc
make |& tee om
#*
# (code-c-d "wdtp" "~/usrc/project-tableau-linux/")
# (find-wdtpfile "")
# (find-wdtpfile "")
# (find-wdtpfile "cases/")
# (find-wdtpfile "gamma.cpp")
# (find-wdtpfile "gamma.cpp" "gamma: generates the gamma_n family of theorems.")
# (find-wdtpfile "gamma.cpp" "Usage: gamma -from n0 -to n [-n] [-l num]")
# (find-wdtpfile "h.cpp")
# (find-wdtpfile "h.cpp" "h: generates the h_n family of theorems.")
# (find-wdtpfile "h.cpp" "Usage: h -from n0 -to n [-n]")
# (find-wdtpfile "php.cpp")
# (find-wdtpfile "php.cpp" "php: generates the php_n family (Pigeon Hole")
# (find-wdtpfile "php.cpp" "Usage: php -from n0 -to n [-n]")
# (find-wdtpfile "statman.cpp")
# (find-wdtpfile "statman.cpp" "statman: generates the S_n family of theorems.")
# (find-wdtpfile "statman.cpp" "Usage: statman -from n0 -to n [-n]")
# (find-wdtpfile "prove.cpp")
# (find-wdtpfile "prove.cpp" "Usage: prove [-m analytic[+BU]*|ke[+V|P]|kes3[+PB]] [-v] -f file")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/usrc/project-tableau-linux/
./prove -m analytic -f cases/gamma1.prove -v
./prove -m analytic -f cases/gamma1.prove -v
cd ~/usrc/project-tableau-linux/
cd cases/
laf gamma*
../gamma -from 1 -to 5
laf gamma*
#####
#
# winplot
# 2009aug11
#
#####
# «winplot» (to ".winplot")
# http://math.exeter.edu/rparris/winplot.html
# http://math.exeter.edu/rparris/peanut/wp32z.exe
# http://math.exeter.edu/rparris/faq.html
# http://spot.pcc.edu/~ssimonds/winplot/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/.wine/drive_c/peanut/
laf
wine winplot.exe
#####
#
# gnuplot movies about the n-body problem
#
#####
#*
rm -Rv /tmp/movie/
cd /tmp/
tar -xvf $S/http/www.maia.ub.es/dsg/movie.tar
cd /tmp/movie/
startmovie
#*
#####
#
# Catsters videos
# 2009nov29
#
#####
# «catsters» (to ".catsters")
# http://www.youtube.com/user/TheCatsters
# http://www.simonwillerton.staff.shef.ac.uk/TheCatsters/
# http://www.simonwillerton.staff.shef.ac.uk/TheCatsters/index.html
# https://byorgey.wordpress.com/catsters-guide-2/ 2020mar28
(fooi-re "<ul>" "" "<li>" "" "<a href=\"" "" "\" target=\"_blank\">" " "
"</a>" "" "</li>" "" "</ul>" "")
Basics
Limits and Colimits
Terminal and Initial Objects
http://www.youtube.com/watch?v=yeQcmxM2e5I 1
http://www.youtube.com/watch?v=9vhWpOVPlIE 2
http://www.youtube.com/watch?v=yaPwKu5fHqI 3
Products and Coproducts
http://www.youtube.com/watch?v=upCSDIO9pjc 1
http://www.youtube.com/watch?v=BqRkULEhG40 2
http://www.youtube.com/watch?v=TCQWHOUBwDE 3
http://www.youtube.com/watch?v=n6nBgszToBE 4
Pullback and Pushouts
http://www.youtube.com/watch?v=XGysPJvCXOc 1
http://www.youtube.com/watch?v=LkkallToFQ0 2
General Limits and Colimits
http://www.youtube.com/watch?v=g47V6qxKQNU 1
http://www.youtube.com/watch?v=SpCyaNi257w 2
http://www.youtube.com/watch?v=U3nzEUEnLKQ 3
http://www.youtube.com/watch?v=7B4cawdLAPg 4
http://www.youtube.com/watch?v=Ud_k4HFIogQ 5
http://www.youtube.com/watch?v=9UOdrRF_pNc 6
Natural Transformations
http://www.youtube.com/watch?v=FZSUwqWjHCU 1
http://www.youtube.com/watch?v=XnrqHd39Cl0 2
http://www.youtube.com/watch?v=EG5xUYXHFeU 3
http://www.youtube.com/watch?v=fsfzEz6qAGQ 4
Representable Functors and Yoneda
http://www.youtube.com/watch?v=4QgjKUzyrhM 1
http://www.youtube.com/watch?v=eaJmUUogb6g 2
http://www.youtube.com/watch?v=TLMxHB19khE 3
Adjunctions
Introduction
http://www.youtube.com/watch?v=loOJxIOmShE 1
http://www.youtube.com/watch?v=JEJim3t-N9A 2
http://www.youtube.com/watch?v=nP5XQ6OBHHY 4
(Adjunctions 2 includes a nice description of what it means
for an isomorphism to be ``natural in A'')
Adjunctions and Monads
http://www.youtube.com/watch?v=2i_PpYsl8b8 3
http://www.youtube.com/watch?v=xqLgGB7Hv7g 5
http://www.youtube.com/watch?v=Ht1mQ97Zq2k 6
http://www.youtube.com/watch?v=D8g9xnVr0Lg 7
Adjunctions from Morphisms
http://www.youtube.com/watch?v=SzzHjpRmrLU 1
http://www.youtube.com/watch?v=jAQfNGEOass 2
http://www.youtube.com/watch?v=tWhB7E-HS8Y 3
http://www.youtube.com/watch?v=Cf7hCiTspJc 4
http://www.youtube.com/watch?v=MSOGEtW39qM 5
String Diagrams
Introduction
http://www.youtube.com/watch?v=USYRDDZ9yEc 1
http://www.youtube.com/watch?v=JeGhNhgOTuk 2
http://www.youtube.com/watch?v=pmvVE8AGAEA 3
http://www.youtube.com/watch?v=YNC5faXshAk 4
http://www.youtube.com/watch?v=kiXjcqxVogE 5
Visualization: Open-closed cobordisms
http://www.youtube.com/watch?v=Jb1ZHLXBMy4 1
http://www.youtube.com/watch?v=zQMhXy1-YNM 2
http://www.youtube.com/watch?v=_raQJYpEnU8 3
Specific Constructions
Slice and Comma Categories
http://www.youtube.com/watch?v=f4jpvwwnq_s 1
http://www.youtube.com/watch?v=W6sG5uraex0 2
Coequalisers
http://www.youtube.com/watch?v=vYktRTtulek 1
http://www.youtube.com/watch?v=DMSPS6us__Y 2
Monads
Introduction
http://www.youtube.com/watch?v=9fohXBj2UEI 1
http://www.youtube.com/watch?v=Si6_oG7ZdK4 2
http://www.youtube.com/watch?v=eBQnysX7oLI 3
http://www.youtube.com/watch?v=uYY5c1kkoIo 4
http://www.youtube.com/watch?v=Cm-O_ZWEIGY 5
Distributive Laws
http://www.youtube.com/watch?v=mw4IhOLhDwY 1
http://www.youtube.com/watch?v=TLgjH9Y8HOc 2
http://www.youtube.com/watch?v=g-SCYArh5RY 3
http://www.youtube.com/watch?v=FZeoHPRoBVk 4
Group Objects and Hopf Algebras
http://www.youtube.com/watch?v=p3kkm5dYH-w 1
http://www.youtube.com/watch?v=kJ2X_U7X5WA 2
http://www.youtube.com/watch?v=wAeHrtKMTHM 3
http://www.youtube.com/watch?v=zZn9ZETVkF8 4
http://www.youtube.com/watch?v=gmxZ_KCRZho 5
http://www.youtube.com/watch?v=Gv1sRLOwVWA 6
Monoid Objects
http://www.youtube.com/watch?v=PH-OhkrXXvA 1
http://www.youtube.com/watch?v=7Sf3Y4sesZE 2
Generalizations
Two-categories
http://www.youtube.com/watch?v=k-RehY4tLdI 1
http://www.youtube.com/watch?v=DRGh-HESyag 2
Double Categories
http://www.youtube.com/watch?v=kiCZiSA2W3Q 1
Multicategories
http://www.youtube.com/watch?v=D_pPNgGZYDs 1
http://www.youtube.com/watch?v=WytjdlserwU 2
Metric Spaces and Enriched Categories
http://www.youtube.com/watch?v=be7rx29eMr4 1
http://www.youtube.com/watch?v=0p3iS3Nf-fs 2
Bicategories
Spans
http://www.youtube.com/watch?v=SQfUXOCMUhI 1
http://www.youtube.com/watch?v=Jn5dZuebeXU 2
Eckmann-Hilton
http://www.youtube.com/watch?v=Rjdo-RWQVIY 1
http://www.youtube.com/watch?v=wnRqo7UHa-k 2
# Old:
# «youtube-dl» (to ".youtube-dl")
# (find-angg ".emacs" "find-mplayer")
# http://ubuntuforums.org/archive/index.php/t-1173378.html
# http://bitbucket.org/rg3/youtube-dl/wiki/Home
# http://bitbucket.org/rg3/youtube-dl/raw/2009.09.13/youtube-dl
# (find-youtubedl-links "/sda5/videos/" "Representables_and_Yoneda_1" "4QgjKUzyrhM" ".flv" "catsters-yoneda1")
# (code-mplayer "catsters-yoneda1" "/sda5/videos/Representables_and_Yoneda_1-4QgjKUzyrhM.flv")
# (find-catsters-yoneda1)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd /tmp/
# wget http://bitbucket.org/rg3/youtube-dl/raw/2009.09.13/youtube-dl
wget http://bitbucket.org/rg3/youtube-dl/raw/2010.08.04/youtube-dl
chmod 755 youtube-dl
mv -v youtube-dl ~/bin/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/CATSTERS/")
mkdir ~/CATSTERS/
cd ~/CATSTERS/
function ydl () { cd ~/CATSTERS/; echo "ydl '$1' \"$2\""; youtube-dl -b -t -c $1 }
function ydl () { cd ~/CATSTERS/; echo "ydl '$1' \"$2\""; youtube-dl -b -o "%(title)s.%(ext)s" -c $1 }
ydl 'http://www.youtube.com/watch?v=TLMxHB19khE' "Representables and Yoneda 3" "repyo3"
ydl 'http://www.youtube.com/watch?v=eaJmUUogb6g' "Representables and Yoneda 2" "repyo2"
ydl 'http://www.youtube.com/watch?v=4QgjKUzyrhM' "Representables and Yoneda 1" "repyo1"
ydl 'http://www.youtube.com/watch?v=W6sG5uraex0' "Slice and comma categories 2" "sliceandcomma2"
ydl 'http://www.youtube.com/watch?v=f4jpvwwnq_s' "Slice and comma categories 1" "sliceandcomma2"
ydl 'http://www.youtube.com/watch?v=DMSPS6us__Y' "Coequalisers 2" "coeqs1"
ydl 'http://www.youtube.com/watch?v=vYktRTtulek' "Coequalisers 1" "coeqs2"
ydl 'http://www.youtube.com/watch?v=MSOGEtW39qM' "Adjunctions from morphisms 5"
ydl 'http://www.youtube.com/watch?v=Cf7hCiTspJc' "Adjunctions from morphisms 4"
ydl 'http://www.youtube.com/watch?v=tWhB7E-HS8Y' "Adjunctions from morphisms 3"
ydl 'http://www.youtube.com/watch?v=jAQfNGEOass' "Adjunctions from morphisms 2"
ydl 'http://www.youtube.com/watch?v=SzzHjpRmrLU' "Adjunctions from morphisms 1"
ydl 'http://www.youtube.com/watch?v=9UOdrRF_pNc' "General limits and colimits 6"
ydl 'http://www.youtube.com/watch?v=Ud_k4HFIogQ' "General limits and colimits 5"
ydl 'http://www.youtube.com/watch?v=7B4cawdLAPg' "General limits and colimits 4"
ydl 'http://www.youtube.com/watch?v=U3nzEUEnLKQ' "General limits and colimits 3"
ydl 'http://www.youtube.com/watch?v=SpCyaNi257w' "General limits and colimits 2"
ydl 'http://www.youtube.com/watch?v=g47V6qxKQNU' "General limits and colimits 1"
ydl 'http://www.youtube.com/watch?v=LkkallToFQ0' "Pullbacks and pushouts 2"
ydl 'http://www.youtube.com/watch?v=XGysPJvCXOc' "Pullbacks and pushouts 1"
ydl 'http://www.youtube.com/watch?v=n6nBgszToBE' "Products and coproducts 4"
ydl 'http://www.youtube.com/watch?v=TCQWHOUBwDE' "Products and coproducts 3"
ydl 'http://www.youtube.com/watch?v=BqRkULEhG40' "Products and coproducts 2"
ydl 'http://www.youtube.com/watch?v=upCSDIO9pjc' "Products and coproducts 1"
ydl 'http://www.youtube.com/watch?v=yaPwKu5fHqI' "Terminal and initial objects 3"
ydl 'http://www.youtube.com/watch?v=9vhWpOVPlIE' "Terminal and initial objects 2"
ydl 'http://www.youtube.com/watch?v=yeQcmxM2e5I' "Terminal and initial objects 1"
ydl 'http://www.youtube.com/watch?v=RNwqc3eu6Y8' "How it is done"
ydl 'http://www.youtube.com/watch?v=0p3iS3Nf-fs' "Metric spaces and enriched categories 2"
ydl 'http://www.youtube.com/watch?v=7Sf3Y4sesZE' "Monoid objects 2"
ydl 'http://www.youtube.com/watch?v=PH-OhkrXXvA' "Monoid objects 1"
ydl 'http://www.youtube.com/watch?v=wnRqo7UHa-k' "Eckmann-Hilton 2 (beware typo at 4:13)"
ydl 'http://www.youtube.com/watch?v=be7rx29eMr4' "Metric spaces and enriched categories 1"
ydl 'http://www.youtube.com/watch?v=kteH2ZBW9Lg' "Klein bottle"
ydl 'http://www.youtube.com/watch?v=Rjdo-RWQVIY' "Eckmann-Hilton 1"
ydl 'http://www.youtube.com/watch?v=kiCZiSA2W3Q' "Double categories"
ydl 'http://www.youtube.com/watch?v=Gv1sRLOwVWA' "Group objects and Hopf algebras 6"
ydl 'http://www.youtube.com/watch?v=DRGh-HESyag' "2-categories 2"
ydl 'http://www.youtube.com/watch?v=gmxZ_KCRZho' "Group objects and Hopf algebras 5"
ydl 'http://www.youtube.com/watch?v=zZn9ZETVkF8' "Group objects and Hopf algebras 4 (Catsters 38)"
ydl 'http://www.youtube.com/watch?v=wAeHrtKMTHM' "Group objects and Hopf algebras 3 (Catsters 37)"
ydl 'http://www.youtube.com/watch?v=k-RehY4tLdI' "2-categories 1 (Catsters 36)"
ydl 'http://www.youtube.com/watch?v=guVjFOfi2o0' "Outtakes (Catsters 35)"
ydl 'http://www.youtube.com/watch?v=WytjdlserwU' "Multicategories 2 (Catsters 34)"
ydl 'http://www.youtube.com/watch?v=D_pPNgGZYDs' "Multicategories 1 (Catsters 33)"
ydl 'http://www.youtube.com/watch?v=Jn5dZuebeXU' "Spans 2 [32]"
ydl 'http://www.youtube.com/watch?v=SQfUXOCMUhI' "Spans 1 [31]"
ydl 'http://www.youtube.com/watch?v=FZeoHPRoBVk' "Distributive laws 4 [30]"
ydl 'http://www.youtube.com/watch?v=g-SCYArh5RY' "Distributive laws 3 and/or Monads 6 [29]"
ydl 'http://www.youtube.com/watch?v=TLgjH9Y8HOc' "Distributive laws 2"
ydl 'http://www.youtube.com/watch?v=mw4IhOLhDwY' "Distributive laws 1"
ydl 'http://www.youtube.com/watch?v=kJ2X_U7X5WA' "Group objects and Hopf algebras 2"
ydl 'http://www.youtube.com/watch?v=p3kkm5dYH-w' "Group objects and Hopf algebras 1"
ydl 'http://www.youtube.com/watch?v=_raQJYpEnU8' "Open-closed cobordisms 3"
ydl 'http://www.youtube.com/watch?v=zQMhXy1-YNM' "Open-closed cobordisms 2"
ydl 'http://www.youtube.com/watch?v=fsfzEz6qAGQ' "Natural transformations 3A"
ydl 'http://www.youtube.com/watch?v=EG5xUYXHFeU' "Natural transformations 3"
ydl 'http://www.youtube.com/watch?v=XnrqHd39Cl0' "Natural transformations 2"
ydl 'http://www.youtube.com/watch?v=FZSUwqWjHCU' "Natural transformations 1"
ydl 'http://www.youtube.com/watch?v=kiXjcqxVogE' "String diagrams 5"
ydl 'http://www.youtube.com/watch?v=YNC5faXshAk' "String diagrams 4"
ydl 'http://www.youtube.com/watch?v=pmvVE8AGAEA' "String diagrams 3"
ydl 'http://www.youtube.com/watch?v=JeGhNhgOTuk' "String diagrams 2"
ydl 'http://www.youtube.com/watch?v=USYRDDZ9yEc' "String diagrams 1"
ydl 'http://www.youtube.com/watch?v=Jb1ZHLXBMy4' "Open-closed cobordism 1"
ydl 'http://www.youtube.com/watch?v=D8g9xnVr0Lg' "Adjunctions 7"
ydl 'http://www.youtube.com/watch?v=Ht1mQ97Zq2k' "Adjunctions 6"
ydl 'http://www.youtube.com/watch?v=xqLgGB7Hv7g' "Adjunctions 5"
ydl 'http://www.youtube.com/watch?v=nP5XQ6OBHHY' "Adjunctions 4"
ydl 'http://www.youtube.com/watch?v=2i_PpYsl8b8' "Adjunctions 3"
ydl 'http://www.youtube.com/watch?v=JEJim3t-N9A' "Adjunctions 2"
ydl 'http://www.youtube.com/watch?v=loOJxIOmShE' "Adjunctions 1"
ydl 'http://www.youtube.com/watch?v=Cm-O_ZWEIGY' "Monads 4"
ydl 'http://www.youtube.com/watch?v=uYY5c1kkoIo' "Monads 3A"
ydl 'http://www.youtube.com/watch?v=eBQnysX7oLI' "Monads 3"
ydl 'http://www.youtube.com/watch?v=Si6_oG7ZdK4' "Monads 2"
ydl 'http://www.youtube.com/watch?v=9fohXBj2UEI' "Monads 1"
# «catsters-code» (to ".catsters-code")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/CATSTERS/
for i in *; do
echo "(code-mplayer \"catsters-\" \"~/CATSTERS/$i\")"
done |& tee /tmp/o
#####
#
# GSL
# 2011nov14
#
#####
# «gsl» (to ".gsl")
# (find-es "lua5" "gsl-shell")
# (find-status "gsl-doc-info")
# (find-vldifile "gsl-doc-info.list")
# (find-udfile "gsl-doc-info/")
# (find-status "gsl-doc-pdf")
# (find-vldifile "gsl-doc-pdf.list")
# (find-udfile "gsl-doc-pdf/")
# (find-status "gsl-ref-html")
# (find-vldifile "gsl-ref-html.list")
# (find-udfile "gsl-ref-html/")
# (find-status "libgsl0-dev")
# (find-vldifile "libgsl0-dev.list")
# (find-udfile "libgsl0-dev/")
# (find-node "(gsl-ref)")
# (find-node "(gsl-ref)Function Index")
# (find-node "(gsl-ref)Variable Index")
# (find-node "(gsl-ref)Type Index")
# (find-node "(gsl-ref)Concept Index")
apti gsl-doc-info gsl-doc-pdf gsl-ref-html libgsl0-dev
apti libagg-dev
#####
#
# cat-dist
# 2014jan20
#
#####
# «cat-dist» (to ".cat-dist")
# http://www.mta.ca/~cat-dist/
# http://news.gmane.org/gmane.science.mathematics.categories
# http://article.gmane.org/gmane.science.mathematics.categories/7984
# ^ Formalizations of category theory in proof assistants
Hi,
I have asked mathoverflow for formalizations of category theory in
proof assistants at
http://mathoverflow.net/questions/152497/formalizations-of-category-theory-in-proof-assistants,
and was told that my list (copied below) was approximately complete.
I would like to know if anyone on this list knows of formalizations
that I missed; feel free to respond either by email or on the
mathoverflow thread.
Thanks,
Jason
The mathoverflow question:
The ones I know about are:
* https://bitbucket.org/JasonGross/catdb, which became
https://github.com/JasonGross/HoTT-categories, which became
https://github.com/HoTT/HoTT/tree/master/theories/categories
* https://github.com/benediktahrens/Foundations/tree/typesystems
* https://github.com/pcapriotti/agda-categories/
* https://github.com/jmchapman/restriction-categories
* https://github.com/konn/category-agda
* http://coq.inria.fr/pylons/pylons/contribs/view/MathClasses/v8.4
* http://www.cs.berkeley.edu/~megacz/coq-categories/
* http://coq.inria.fr/pylons/pylons/contribs/view/Coalgebras/v8.4
* http://coq.inria.fr/pylons/pylons/contribs/view/Algebra/v8.4
* https://github.com/copumpkin/categories
* https://github.com/crypto-agda/crypto-agda/tree/master/FunUniverse
* http://coq.inria.fr/pylons/pylons/contribs/view/ConCaT/v8.4
* http://coq.inria.fr/pylons/pylons/contribs/view/CatsInZFC/v8.4
* http://mattam.org/repos/coq/cat/
* https://github.com/benediktahrens/rezk_completion
* https://github.com/rs-/Triangles
* https://github.com/benediktahrens/coinductives
I also know about the following papers about formalizing category
theory in proof assistants:
* "Veried Computing in Homological Algebra: A Journey Exploring the
Power and Limits of Dependent Type Theory" by Arnaud Spiwack
(http://assert-false.net/arnaud/papers/thesis.spiwack.pdf)
* "Galois: a theory development project" by Peter Aczel
(http://www.cs.man.ac.uk/~petera/galois.ps.gz)
* "A mechanically assisted constructive proof in category theory" by
James Altucher and Prakash Panangaden
(http://link.springer.com/chapter/10.1007/3-540-52885-7_110)
* "Category Theory in Coq" by Carvalho
(http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9846)
* "Category Theory as an Extension of Martin-Lof Type Theory" by
http://rd.host.cs.st-andrews.ac.uk/publications/CTMLTT.pdf
* "Automating Proofs in Category Theory" by Dexter Kozen, Christoph
Kreitz, and Eva Richter
(http://www.cs.uni-potsdam.de/ti/kreitz/PDF/06ijcar-categories.pdf)
* "Towards a readable formalisation of category theory" by Greg
O'Keefe (http://users.cecs.anu.edu.au/~okeefe/work/fcat4cats04.pdf)
I'm primarily interested in public-domain code implementing category
theory in a proof assistant, though I'm also interested in papers
about formalizations of category theory in proof assistants.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
#####
#
# Encyclopedia of Proof Systems (Bruno Wotzenlogel Paleo)
# 2016apr06
#
#####
# «encyclopedia-of-psyss» (to ".encyclopedia-of-psyss")
# (find-angg ".emacs.papers" "encyclopedia-of-psyss")
# https://github.com/ProofSystem/Encyclopedia
# https://github.com/ProofSystem/Encyclopedia/blob/master/README.md
# http://proofsystem.github.io/Encyclopedia/
# http://paleo.woltzenlogel.org/
# https://github.com/ProofSystem/Encyclopedia/raw/master/main.pdf
# (find-git-links "https://github.com/ProofSystem/Encyclopedia" "eopsys")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/Encyclopedia/
cd ~/usrc/
# git clone --depth 1 https://github.com/ProofSystem/Encyclopedia
git clone https://github.com/ProofSystem/Encyclopedia
cd ~/usrc/Encyclopedia/
cd ~/usrc/Encyclopedia/Source/
make |& tee om
dmissing qtree.sty
dmissing biblatex2.sty
dmissing tikzlibraryquotes
# http://tex.stackexchange.com/questions/236084/why-cant-i-load-the-tikz-cd-package
git pull --depth 1
# (code-c-d "eopsys" "~/usrc/Encyclopedia/")
# (find-eopsysfile "")
# (find-eopsysfile "Source/mainmatter/")
# (find-gitk "~/usrc/Encyclopedia/")
#####
#
# Provas de MD do Fernando Naufel
# 2018nov13
#
#####
# «provas-MD-naufel» (to ".provas-MD-naufel")
# https://serenitas50.wordpress.com/2018/03/12/md-informacoes-de-inicio-de-periodo-2018-1/
# https://drive.google.com/file/d/0B82xg7N6Wd-HZjEzWUlveXNZWDA/view
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
mkdir -p $S/https/serenitas50.wordpress.com/
cd $S/https/serenitas50.wordpress.com/
cp -v /tmp/Provas-MD-2012-2016.zip $S/https/serenitas50.wordpress.com/
# (find-fline "~/usrc/Provas-MD-2012-2016/")
rm -Rv ~/usrc/Provas-MD-2012-2016/
cd ~/usrc/
# mkdir ~/usrc/Provas-MD-2012-2016/
unzip -d ~/usrc/ $S/https/serenitas50.wordpress.com/Provas-MD-2012-2016.zip
cd ~/usrc/Provas-MD-2012-2016/
find * | grep pdf
mv -iv $(find * | grep pdf) .
(code-c-d "provasfnaufel" "~/usrc/Provas-MD-2012-2016/")
;; (find-provasfnaufelfile "")
;; (find-provasfnaufelfile "" "md-122-p1-manha-gab.pdf")
# (find-sh "unzip")
# (find-sh "unzip -hh")
#####
#
# naturality
# 2019nov09
#
#####
# «naturality» (to ".naturality")
# (find-angg ".emacs.papers" "wadler-free")
# (find-books "__logic/__logic.el" "reynolds")
# (find-books "__cats/__cats.el" "landry")
# (find-landrypage (+ 15 90) "6. Canonical Maps")
# (find-books "__cats/__cats.el" "kromer")
# (find-kromerpage (+ 34 58) "2.2.5 Passage to the limit and \"naturality\"")
# (find-kromertext (+ 34 58) "2.2.5 Passage to the limit and \"naturality\"")
# (find-kromerpage (+ 34 70) "2.3.4.1 \"Natural transformation\"")
# (find-kromertext (+ 34 70) "2.3.4.1 \"Natural transformation\"")
If you want lenghtier disscussions on the various kinds and degrees of
naturality and canonicality in categorical entities I recommend 1) the
chapter of Jean Pierre Marquis in "Categories for the Working
Philosopher" (it's called "Canonical Maps"), and 2) Ralf Krömer's
"Tool and Object - A History and Philosophy of Category Theory",
mainly its sections 2.2.5 and 2.3.4.1.
Also, take a look a Wadler's "Theorems for Free!" -
http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html#free -
it formalizes (in lambda-calculus) the idea that maps defined in a
natural way have certain invariance properties.
#####
#
# notacao-de-fisicos
# 2019nov07
#
#####
# «notacao-de-fisicos» (to ".notacao-de-fisicos")
# (find-TH "notacao-de-fisicos")
# https://tex.stackexchange.com/users/189105/eduardo-ochs#_=_
# (find-books "__logic/__logic.el" "wiedijk")
# (find-books "__comp/__comp.el" "sussman-wisdom")
# (find-books "__phil/__phil.el" "ganesalingam")
# (find-books "__phil/__phil.el" "ganesalingam" "2.4.4 Variables")
# (find-books "__cats/__cats.el" "bauer-dawn")
# (find-books "__analysis/__analysis.el" "john")
# (find-books "__analysis/__analysis.el" "ellermeijer-heck")
# (find-books "__analysis/__analysis.el" "redish-gupta")
# http://www.weizmann.ac.il/ScienceTeaching/Arcavi/publications-0
#####
#
# bortolossi
# 2019nov07
#
#####
# «bortolossi» (to ".bortolossi")
# (find-books "__analysis/__analysis.el" "bortolossi")
# (find-fline "~/2019.2-C3/Bortolossi/")
# (find-fline "~/2019.2-C3/Bortolossi/Cap_4/")
# (find-fline "~/2019.2-C3/Bortolossi/Cap_5/")
# (find-fline "/sda5/home/edrx/2019.2-C3/Bortolossi/Cap_4/")
# (find-fline "/sda5/home/edrx/2019.2-C3/Bortolossi/")
# (find-twusfile "2019.2-C3/Bortolossi/")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/2019.2-C3/Bortolossi/Cap_4/
djvuize djvus
# djvuize THIS=bortolossi-cap-4 djvu
djvm -create bortolossi-cap-4.djvu 20*.djvu
djvuize THIS=bortolossi-cap-4 pdf
cp -v bortolossi-cap-4.pdf ..
cd ~/2019.2-C3/Bortolossi/Cap_5/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-5 djvu
djvm -create bortolossi-cap-5.djvu 20*.djvu
djvuize THIS=bortolossi-cap-5 pdf
cp -v bortolossi-cap-5.pdf ..
cd ~/2019.2-C3/Bortolossi/Cap_7/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-7 djvu
djvm -create bortolossi-cap-7.djvu 20*.djvu
djvuize THIS=bortolossi-cap-7 pdf
cp -v bortolossi-cap-7.pdf ..
# (find-pdf-page "~/2019.2-C3/Bortolossi/Cap_4/bortolossi-cap-4.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/bortolossi-cap-4.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/Cap_5/bortolossi-cap-5.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/bortolossi-cap-5.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/Cap_7/bortolossi-cap-7.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/bortolossi-cap-7.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/Cap_10/bortolossi-cap-10.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/bortolossi-cap-10.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/Cap_11/bortolossi-cap-11.pdf")
# (find-pdf-page "~/2019.2-C3/Bortolossi/bortolossi-cap-11.pdf")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
cd ~/2019.2-C3/Bortolossi/Cap_10/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-10 djvu
djvm -create bortolossi-cap-10.djvu 20*.djvu
djvuize THIS=bortolossi-cap-10 pdf
cp -v bortolossi-cap-10.pdf ..
cd ~/2019.2-C3/Bortolossi/Cap_11/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-11 djvu
djvm -create bortolossi-cap-11.djvu 20*.djvu
djvuize THIS=bortolossi-cap-11 pdf
cp -v bortolossi-cap-11.pdf ..
cd ~/2019.2-C3/Bortolossi/Cap_12/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-12 djvu
djvm -create bortolossi-cap-12.djvu 20*.djvu
djvuize THIS=bortolossi-cap-12 pdf
cp -v bortolossi-cap-12.pdf ..
# (find-fline "~/2020.1-C3/Bortolossi/Cap_6/")
cd ~/2020.1-C3/Bortolossi/Cap_6/
djvuize pngs
djvuize djvus
# djvuize THIS=bortolossi-cap-6 djvu
djvm -create bortolossi-cap-6.djvu 20*.djvu
djvuize THIS=bortolossi-cap-6 pdf
cp -v bortolossi-cap-6.pdf ..
cd ~/2020.1-C3/Bortolossi/Cap_6/
rm -v *.png
rm -v *.djvu
rm -v *.pdf
#####
#
# material-para-GA
# 2020feb20
#
#####
# «material-para-GA» (to ".material-para-GA")
# (mpgp 2 "introducao")
# (mpg "introducao")
# Bibliografia:
# (taa)
# (taap)
* (eepitch-Twu)
* (eepitch-kill)
* (eepitch-Twu)
cd ~/slow_html/LATEX/
ls *GA*.pdf | awk '{print "http://angg.twu.net/LATEX/" $1}'
(find-twusfile "LATEX/" "2018-1-GA-conicas")
(find-twusfile "LATEX/" "2018-1-GA-R3")
# (find-LATEXfile "" "2018-1-GA-R3.tex")
http://angg.twu.net/LATEX/2018-1-GA-R3.tex
http://angg.twu.net/LATEX/2018-1-GA-R3.pdf
# http://angg.twu.net/LATEX/2018-1-GA-conicas.tex
# http://angg.twu.net/LATEX/2018-1-GA-conicas.pdf
# (find-fline "$S/http/angg.twu.net/LATEX/")
# (find-pdf-page "$S/http/angg.twu.net/LATEX/2018-1-GA-conicas.pdf")
# (find-pdf-text "$S/http/angg.twu.net/LATEX/2018-1-GA-conicas.pdf")
#####
#
# material-para-GA-git
# 2020mar03
#
#####
# «material-para-GA-git» (to ".material-para-GA-git")
# (find-LATEX "material-para-GA.tex" "git")
# (find-LATEX "material-para-GA.md")
# (find-angg "eev-current/README.md")
# (find-TH "material-para-GA")
# http://angg.twu.net/material-para-GA.html
# https://github.com/edrx/material-para-GA
# Creating the repository:
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-latex-upload-links "material-para-GA")
cd ~/LATEX/
flsfiles-zip material-para-GA.fls material-para-GA.zip
rm -rfv /tmp/material-para-GA.zip
rm -rfv /tmp/edrx-latex/
cd /tmp/
cp -v ~/LATEX/material-para-GA.zip .
mkdir /tmp/edrx-latex/
unzip -d /tmp/edrx-latex/ /tmp/material-para-GA.zip
cd /tmp/edrx-latex/
cp -v ~/LATEX/material-para-GA.pdf .
cp -v ~/LATEX/material-para-GA.md README.md
git init
git add README.md
git add *
git ls-files
git commit -m "first commit"
git remote add origin https://github.com/edrx/material-para-GA.git
git push -u origin master
find * -type f | sort
lualatex material-para-GA.tex
lualatex material-para-GA.tex
Scp-np material-para-GA.zip $TWUP/LATEX/material-para-GA.zip
Scp-np material-para-GA.zip $TWUS/LATEX/material-para-GA.zip
# http://angg.twu.net/LATEX/material-para-GA.zip
# 2023jun04:
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/edrx-latex/")
rm -Rv /tmp/edrx-latex/
mkdir /tmp/edrx-latex/
cd /tmp/edrx-latex/
git clone https://github.com/edrx/material-para-GA.git .
'rm' -Rfv /tmp/edrx-latex/*
# (find-fline "~/LATEX/material-para-GA.md")
cd /tmp/edrx-latex/
cp -v ~/LATEX/material-para-GA.md README.md
cp -v ~/LATEX/material-para-GA.pdf .
unzip -d /tmp/edrx-latex/ ~/LATEX/material-para-GA.zip
# (magit-status "/tmp/edrx-latex/")
#####
#
# Joshua Meyers - linear algebra notes
# 2020jun03
#
#####
# «joshua-meyers» (to ".joshua-meyers")
# https://mail.google.com/mail/ca/u/0/#search/from%3Ajoshua/QgrcJHrnsbjljsZDZFNLHJNcwFqvRMMpZhg
# https://github.com/meygerjos/linear_algebra_notes
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/linear_algebra_notes/
cd ~/usrc/
git clone https://github.com/meygerjos/linear_algebra_notes
cd ~/usrc/linear_algebra_notes/
pdflatex notes.tex
# (find-pdf-page "~/usrc/linear_algebra_notes/notes.pdf")
# (find-pdf-text "~/usrc/linear_algebra_notes/notes.pdf")
# (find-gitk "~/usrc/linear_algebra_notes/")
# (code-c-d "linearalgebranotes" "~/usrc/linear_algebra_notes/")
# (find-linearalgebranotesfile "")
#####
#
# presheaves-calc (by Jens Hemelaer)
# 2020oct08
#
#####
# «presheaves-calc» (to ".presheaves-calc")
# (find-books "__cats/__cats.el" "hemelaer")
# https://jhemelae.github.io/images/Presheaves-Calc.ipynb
# https://jhemelae.github.io/images/Presheaves-Calc.pdf
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/prec/")
rm -Rv /tmp/prec/
mkdir /tmp/prec/
cd /tmp/prec/
cp -iv $S/https/jhemelae.github.io/images/Presheaves-Calc.ipynb .
jupyter notebook
#####
#
# Videos de C2 e C3 (2020.1)
# 2020sep24
#
#####
# «2020.1-videos-C2-C3» (to ".2020.1-videos-C2-C3")
# (find-fline "~/2020.1-C2/")
# (find-fline "~/2020.1-C3/")
# (find-twusfile "2020.1-C2/")
# (find-twusfile "2020.1-C3/")
* (eepitch-Twu)
* (eepitch-kill)
* (eepitch-Twu)
cd ~/slow_html/2020.1-C2/
for i in $(ls *.mp4); do
echo http://angg.twu.net/2020.1-C2/$i
done
cd ~/slow_html/2020.1-C3/
for i in $(ls *.mp4); do
echo http://angg.twu.net/2020.1-C3/$i
done
#####
#
# hassediagram
# 2021mar11
#
#####
# «hassediagram» (to ".hassediagram")
# https://thelanguagegamer.github.io/HasseDiagram/
#####
#
# Calculus Made Easy by Silvanus P. Thompson (Project Gutenberg edition)
# 2021aug03
#
#####
# «silvanus-thompson» (to ".silvanus-thompson")
# (find-books "__analysis/__analysis.el" "thompson")
# https://www.gutenberg.org/ebooks/33283
# https://www.gutenberg.org/files/33283/33283-t.zip
# https://proceedings.sbmac.org.br/sbmac/article/view/3149/3185
# https://www.flickr.com/photos/bibliotecacomunitariawolgran/albums/72157630314168508/
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "~/usrc/silvanus/")
rm -Rv ~/usrc/silvanus/
mkdir ~/usrc/silvanus/
cd ~/usrc/silvanus/
unzip $S/https/www.gutenberg.org/files/33283/33283-t.zip
pdflatex 33283-t.tex
pdflatex 33283-t.tex
pdflatex 33283-t.tex
# (code-pdf-page "silvanusg" "~/usrc/silvanus/33283-t.pdf")
# (code-pdf-text "silvanusg" "~/usrc/silvanus/33283-t.pdf")
# (find-silvanusgpage)
# (find-silvanusgtext)
# (find-silvanusgpage 9 "CONTENTS")
# (find-silvanusgtext 9 "CONTENTS")
# (code-c-d "silvanusg" "~/usrc/silvanus/")
# (find-silvanusgfile "")
# (find-silvanusgfile "33283-t.tex")
;; https://www.gutenberg.org/files/33283/33283-pdf.pdf
#####
#
# desmos
# 2021nov23
#
#####
# «desmos» (to ".desmos")
https://www.desmos.com/
https://www.desmos.com/calculator/9hdca5njbw Freya Holmér's trajectory toy
#####
#
# mathlingua
# 2021dec03
#
#####
# «mathlingua» (to ".mathlingua")
https://news.ycombinator.com/item?id=29419039 Show HN: MathLingua – A Structured Language of Mathematics (mathlingua.org) ***
https://www.mathlingua.org/#/content/10_Introduction.math
#####
#
# dslsofmath
# 2022jan20
#
#####
# «dslsofmath» (to ".dslsofmath")
# (find-books "__comp/__comp.el" "dsls-of-math")
# https://github.com/DSLsofMath/DSLsofMath
# https://github.com/DSLsofMath/DSLsofMath/blob/master/L/snapshots/DSLsofMathBook_snapshot_2022-01-06.pdf
# https://github.com/DSLsofMath/DSLsofMath/raw/master/L/snapshots/DSLsofMathBook_snapshot_2022-01-06.pdf
# (code-pdf-page "dslsofmath" "$S/https/github.com/DSLsofMath/DSLsofMath/raw/master/L/snapshots/DSLsofMathBook_snapshot_2022-01-06.pdf")
# (code-pdf-text "dslsofmath" "$S/https/github.com/DSLsofMath/DSLsofMath/raw/master/L/snapshots/DSLsofMathBook_snapshot_2022-01-06.pdf" 6)
# (find-dslsofmathpage)
# (find-dslsofmathtext)
# (find-dslsofmathpage (+ 6 84) "hard to rename variables")
# (find-dslsofmathtext (+ 6 84) "hard to rename variables")
#####
#
# on-the-missing
# 2022may23
#
#####
# «on-the-missing» (to ".on-the-missing")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/On_the_missing_2022may23_1/")
rm -Rv /tmp/On_the_missing_2022may23_1/
mkdir /tmp/On_the_missing_2022may23_1/
cd /tmp/On_the_missing_2022may23_1/
unzip /tmp/On_the_missing_2022may23_1.zip
A=(
2022on-the-missing-b.tex
apa.bst
catsem-ab-bt.bib
catsem-ab.bib
edrx21.sty
edrx21chars-d.tex
edrx21chars.tex
edrx21defs.tex
edrxaccents.tex
edrxheadfoot.tex
svmult.cls
)
for i in $A; do cmp $i ~/LATEX/$i; done
f () { tkdiff $1 ~/LATEX/$1 }
f 2022on-the-missing-b.tex
f apa.bst
f catsem-ab-bt.bib
f catsem-ab.bib
pdflatex 2022on-the-missing-b.tex
pdflatex 2022on-the-missing-b.tex
bibtex 2022on-the-missing-b
pdflatex 2022on-the-missing-b.tex
pdflatex 2022on-the-missing-b.tex
(code-pdf-page "mism" "/tmp/On_the_missing_2022may23_1/2022on-the-missing-b.pdf")
(code-pdf-text "mism" "/tmp/On_the_missing_2022may23_1/2022on-the-missing-b.pdf")
(code-c-d "mism" "/tmp/On_the_missing_2022may23_1/")
;; (find-mismpage)
;; (find-mismtext)
;; (find-mismfile "")
# (find-mismfile "2022on-the-missing-b.tex")
% (find-LATEX "catsem-ab.bib" "bib-OchsMis1")
Hi Gianluca and Rocco,
the changes are FANTASTIC - and I realized that I don't have much
practice with the passive voice in English, so if I had to make the
changes myself it would have taken me much longer, and the result
wouldn't be 1/10 as good... many, many, many thanks! And the changes
in the sections that needed major rewrites are great too!!! =)
I made some minor changes to the version on Overleaf. The list below
includes both the changes that I made and the changes that I am not
sure how to write.
1) I added an entry "OchsMis1" to the .bib files - it points to the
paper "On the the missing diagrams in Category Theory (first-person
version)", that is on Arxiv.
2) The entry "Freyd76" in the .bib files had this line,
note = {\url{http://angg.twu.net/Freyd76.html}},
with a pointer to scan of that paper. I deleted it - and in section 4
I replaced "See the scan in..." by "See the paper...".
3) I commented out the mentions to Kan extensions and geometric
morphisms in the abstract - Kan extensions and GMs were explained in
the deleted sections.
4) On page 3, what do you thing of ending the section 1 with something
like this? "For reasons of space we had to omit several examples of
how to extend this diagrammatic language by adding new conventions to
it. These examples can be found at \cite[Section 8]{OchsMis1}."
5) On page 4, what do you think of rewriting the beginning of the
convention (CYo) like this idea, but written in a better way (i.e.,
please help!!!)?
"In some constructions related to the Yoneda Lemma the part of the
construction that looks like a part of an adjunction is drawn as
that part of an adjunction [would be drawn]. For example, ``The
functor $U:\Ring→\Set$ is representable'' (see \cite[Section
8]{OchsMis1}) is drawn as:
(diagram)
Its upper part looks like a part of an adjunction, but the rest
does not."
6) On page 19, section 6, I rewrote the first sentence to get rid of
the pointers to deleted sections. The old version is still in the
.tex, but commented out.
7) On page 23, section 6.6, I commented out the pointer to the
deleted section "\cite{ness}".
That's it for the moment...
Cheers, E.
``The functor $U:\Ring→\Set$ is
representable'' can be drawn as:
inherits its shape of that part --- see \cite[Section 8]{OchsMis1} ---
\cite{OchsMis1}
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-fline "/tmp/on_the_missing_may25/")
rm -Rv /tmp/on_the_missing_may25/
mkdir /tmp/on_the_missing_may25/
cd /tmp/on_the_missing_may25/
unzip /tmp/on_the_missing_may25.zip
pdflatex 2022on-the-missing-b.tex
pdflatex 2022on-the-missing-b.tex
bibtex 2022on-the-missing-b
pdflatex 2022on-the-missing-b.tex
pdflatex 2022on-the-missing-b.tex
cp -v 2022on-the-missing-b.pdf /tmp/
Tests for random number generators:
http://www.stat.fsu.edu/pub/diehard/
http://www.phy.duke.edu/~rgb/General/dieharder.php
http://burtleburtle.net/bob/rand/testsfor.html
http://www.iro.umontreal.ca/~simardr/testu01/tu01.html
https://github.com/Carneade/Monads-and-their-applications
https://github.com/Carneade/Monads-and-their-applications/blob/master/monads.pdf
http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf
http://cs.ioc.ee/ewscs/2011/jacobs/jacobs-slides.pdf
https://theintercept.com/2019/11/28/nos-bastidores-pf-descarta-envolvimento-de-ong-em-incendios-na-amazonia-2/?fbclid=IwAR0bWFesSVeQtsRvPjMiSaHTCbaw1cDQURi94jxn_-hawO7qsnDYPb-LTOA
https://news.ycombinator.com/item?id=29292294 An Introduction to Lagrange Multipliers (slimy.com)
http://www.slimy.com/~steuard/teaching/tutorials/Lagrange.html
#####
#
# mapcabral-c1v
# 2022dec16
#
#####
# «mapcabral-c1v» (to ".mapcabral-c1v")
# https://gitlab.com/mapcabral/livro-calculo-uma-variavel
# (find-git-links "https://gitlab.com/mapcabral/livro-calculo-uma-variavel" "mapcabralc1v")
# (code-pdf-page "mapcabralc1v" "~/usrc/livro-calculo-uma-variavel/curso-calculoI-editora-IM.pdf")
# (code-pdf-text "mapcabralc1v" "~/usrc/livro-calculo-uma-variavel/curso-calculoI-editora-IM.pdf")
# (find-mapcabralc1vpage)
# (find-mapcabralc1vtext)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
rm -Rfv ~/usrc/livro-calculo-uma-variavel/
cd ~/usrc/
git clone https://gitlab.com/mapcabral/livro-calculo-uma-variavel
cd ~/usrc/livro-calculo-uma-variavel/
make all
# (find-fline "~/usrc/")
# (find-fline "~/usrc/livro-calculo-uma-variavel/")
# (find-gitk "~/usrc/livro-calculo-uma-variavel/")
# (code-c-d "mapcabralc1v" "~/usrc/livro-calculo-uma-variavel/")
# (find-mapcabralc1vfile "")
https://gitlab.com/mapcabral/livro-calculo-uma-variavel
#####
#
# mapcabral-ar
# 2022dec16
#
#####
# «mapcabral-ar» (to ".mapcabral-ar")
# https://gitlab.com/mapcabral/livro-analise-real
# (find-git-links "https://gitlab.com/mapcabral/livro-analise-real" "mapcabralar")
# (code-pdf-page "mapcabralar" "~/usrc/livro-analise-real/curso-analise-real-com-capa.pdf")
# (code-pdf-text "mapcabralar" "~/usrc/livro-analise-real/curso-analise-real-com-capa.pdf")
# (find-mapcabralarpage)
# (find-mapcabralartext)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/livro-analise-real/
cd ~/usrc/
git clone https://gitlab.com/mapcabral/livro-analise-real
cd ~/usrc/livro-analise-real/
# (find-fline "~/usrc/")
# (find-fline "~/usrc/livro-analise-real/")
# (find-gitk "~/usrc/livro-analise-real/")
# (code-c-d "mapcabralar" "~/usrc/livro-analise-real/")
# (find-mapcabralarfile "")
make all
#####
#
# goldfeld-al
# 2022dec16
#
#####
# «goldfeld-al» (to ".goldfeld-al")
# https://gitlab.com/paulo.goldfeld/algebralinear
# (find-git-links "https://gitlab.com/paulo.goldfeld/algebralinear" "goldfeldal")
# (code-pdf-page "goldfeldal" "~/usrc/algebralinear/Livro/texto/CursoAlgLin-livro.pdf")
# (code-pdf-text "goldfeldal" "~/usrc/algebralinear/Livro/texto/CursoAlgLin-livro.pdf")
# (find-goldfeldalpage)
# (find-goldfeldaltext)
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/algebralinear/
cd ~/usrc/
git clone https://gitlab.com/paulo.goldfeld/algebralinear
cd ~/usrc/algebralinear/
# (find-fline "~/usrc/")
# (find-fline "~/usrc/algebralinear/")
# (find-gitk "~/usrc/algebralinear/")
# (code-c-d "goldfeldal" "~/usrc/algebralinear/")
# (find-goldfeldalfile "")
# (find-goldfeldalfile "Livro/texto/Makefile")
cd ~/usrc/algebralinear/Livro/texto/
make
# Álgebra Linear II, Curso Completo, UFRJ
# Álgebra Linear Cabral & Goldfeld
# https://www.youtube.com/playlist?list=PLMR4r7Hff-07HoFyyJmP4i5sgsHl8fsce
#####
#
# reamat-al
# 2022dec16
#
#####
# «reamat-al» (to ".reamat-al")
# https://www.ufrgs.br/reamat/AlgebraLinear
# https://github.com/reamat/AlgebraLinear
# https://www.ufrgs.br/reamat/AlgebraLinear/livro/main.html
# https://www.ufrgs.br/reamat/AlgebraLinear/livro/livro.pdf
;; <reamatal>
;; https://www.ufrgs.br/reamat/AlgebraLinear/livro/livro.pdf
;; (find-fline "$S/https/www.ufrgs.br/reamat/AlgebraLinear/livro/")
(code-pdf-page "reamatal" "$S/https/www.ufrgs.br/reamat/AlgebraLinear/livro/livro.pdf")
(code-pdf-text "reamatal" "$S/https/www.ufrgs.br/reamat/AlgebraLinear/livro/livro.pdf")
;; (find-reamatalpage)
;; (find-reamataltext)
# https://github.com/reamat/AlgebraLinear
# (find-git-links "https://github.com/reamat/AlgebraLinear" "reamatal")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/AlgebraLinear/
cd ~/usrc/
git clone https://github.com/reamat/AlgebraLinear
cd ~/usrc/AlgebraLinear/
make pdf
# (find-fline "~/usrc/")
# (find-fline "~/usrc/AlgebraLinear/")
# (find-gitk "~/usrc/AlgebraLinear/")
# (code-c-d "reamatal" "~/usrc/AlgebraLinear/")
# (find-reamatalfile "")
# (find-reamatalfile "Makefile")
# (code-pdf-page "reamatal" "~/usrc/AlgebraLinear/livro.pdf")
# (code-pdf-text "reamatal" "~/usrc/AlgebraLinear/livro.pdf")
# (find-reamatalpage)
# (find-reamataltext)
#####
#
# reamat-c1v
# 2022dec16
#
#####
# «reamat-c1v» (to ".reamat-c1v")
# https://www.ufrgs.br/reamat/Calculo/livro-cfuv/main.html
# https://www.ufrgs.br/reamat/Calculo/livro-cfuv/livro.pdf
#####
#
# reamat-c0
# 2022dec16
#
#####
# «reamat-c0» (to ".reamat-c0")
# https://github.com/reamat/PreCalculo
# https://www.ufrgs.br/reamat/PreCalculo/index.html
# https://www.ufrgs.br/reamat/PreCalculo/livro/livro.pdf
# (find-git-links "https://github.com/reamat/PreCalculo" "reamatc0")
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# rm -Rfv ~/usrc/PreCalculo/
cd ~/usrc/
git clone https://github.com/reamat/PreCalculo
cd ~/usrc/PreCalculo/
make pdf
# (find-fline "~/usrc/")
# (find-fline "~/usrc/PreCalculo/")
# (find-gitk "~/usrc/PreCalculo/")
# (code-c-d "reamatc0" "~/usrc/PreCalculo/")
# (code-pdf-page "reamatc0" "~/usrc/PreCalculo/main.pdf")
# (code-pdf-text "reamatc0" "~/usrc/PreCalculo/main.pdf")
# (find-reamatc0file "")
# (find-reamatc0page)
# (find-reamatc0text)
# (find-reamatc0page (+ 15 111) "estudo de sinal")
# (find-reamatc0text (+ 15 111) "estudo de sinal")
https://blog.revolutionanalytics.com/2014/01/the-fourier-transform-explained-in-one-sentence.html
https://science.slashdot.org/story/23/12/23/0516244/30-years-of-donald-knuths-christmas-lectures-go-online---including-2023s
https://news.ycombinator.com/item?id=38775882 30 years of Donald Knuth's 'Christmas Lectures' are online – including 2023's (slashdot.org)
# Local Variables:
# coding: utf-8-unix
# End: