Warning: this is an htmlized version!
The original is across this link,
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.
#
# 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")




#####
#
# 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

(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/")







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









#  Local Variables:
#  coding:               raw-text-unix
#  ee-delimiter-hash:    "\n#*\n"
#  ee-delimiter-percent: "\n%*\n"
#  ee-anchor-format:     "«%s»"
#  End: