reorganizing the repository

.gitignore

@@ -0,0 +1,18 @@
+/build/Makefile-coq.make.bak
+/TAGS*
+/html
+/enhanced-html
+/build/Makefile-configuration
+/.coq_makefile_input
+/.coq_makefile_output
+/build/CoqMakefile.make
+/latex/*.log
+/latex/*.aux
+/latex/*.pdf
+/latex/*.tex
+/latex/*.out
+/latex/*.bbl
+/latex/*.blg
+/latex/*.fdb_latexmk
+/latex/*.fls
+/latex/coqdoc.sty

Makefile

@@ -8,7 +8,7 @@ endif
 endif
 ############################################
 # The packages, listed in order by dependency:
-#PACKAGES += Auxiliary
+PACKAGES += Prelims
 #PACKAGES += ALV1
 #PACKAGES += Displayed_Cats
 #PACKAGES += ALV2
@@ -39,7 +39,7 @@ COQDOC := coqdoc
 COQDOCFLAGS := -interpolate --charset utf-8
 COQDOC_OPTIONS := -toc $(COQDOCFLAGS) $(COQDOCLIBS) -utf8
 
-PACKAGE_FILES := $(patsubst %, TypeTheory/%/.package/files, $(PACKAGES))
+PACKAGE_FILES := $(patsubst %, Modules/%/.package/files, $(PACKAGES))
 
 ifneq "$(INCLUDE)" "no"
 include build/CoqMakefile.make
@@ -95,15 +95,15 @@ COQDEFS := --language=none												\
 	-r "/^[[:space:]]*Notation.* \"'\([[:alnum:]]+\)'/\1/"								\
 	-r '/^[[:space:]]*Tactic Notation.* "\([[:alnum:]]+\)" /\1/'
 
-# $(foreach P,$(PACKAGES),$(eval TAGS-$P: $(filter TypeTheory/$P/%,$(VFILES)); etags -o $$@ $$^))
+# $(foreach P,$(PACKAGES),$(eval TAGS-$P: $(filter Modules/$P/%,$(VFILES)); etags -o $$@ $$^))
 $(VFILES:.v=.vo) : # $(COQBIN)coqc
 # TAGS : $(PACKAGE_FILES) $(VFILES); etags $(COQDEFS) $(VFILES)
 FILES_FILTER := grep -vE '^[[:space:]]*(\#.*)?$$'
-$(foreach P,$(PACKAGES),$(eval $P: $(shell <TypeTheory/$P/.package/files $(FILES_FILTER) |sed "s=^\(.*\)=TypeTheory/$P/\1o=" )))
+$(foreach P,$(PACKAGES),$(eval $P: $(shell <Modules/$P/.package/files $(FILES_FILTER) |sed "s=^\(.*\)=Modules/$P/\1o=" )))
 install:all
 coqwc:; coqwc $(VFILES)
 lc:; wc -l $(VFILES)
-lcp:; for i in $(PACKAGES) ; do echo ; echo ==== $$i ==== ; for f in $(VFILES) ; do echo "$$f" ; done | grep "TypeTheory/$$i" | xargs wc -l ; done
+lcp:; for i in $(PACKAGES) ; do echo ; echo ==== $$i ==== ; for f in $(VFILES) ; do echo "$$f" ; done | grep "Modules/$$i" | xargs wc -l ; done
 wc:; wc -w $(VFILES)
 admitted: 
 	grep --color=auto Admitted $(VFILES)
@@ -117,10 +117,10 @@ Make: $(PACKAGE_FILES) $(UMAKEFILES)
 	echo '# DO NOT EDIT THIS FILE!' ;\
 	echo '# It is made by automatically (by code in Makefile)' ;\
 	echo ;\
-	echo '-Q TypeTheory TypeTheory' ;\
+	echo '-Q Modules Modules' ;\
 	echo ;\
 	for i in $(PACKAGES) ;\
-	do <TypeTheory/$$i/.package/files $(FILES_FILTER) |sed "s=^=TypeTheory/$$i/="  ;\
+	do <Modules/$$i/.package/files $(FILES_FILTER) |sed "s=^=Modules/$$i/="  ;\
 	done ;\
 	echo ;\
 	echo '# Local ''Variables:' ;\
@@ -135,8 +135,8 @@ build/CoqMakefile.make: Make
 # "clean::" occurs also in build/CoqMakefile.make, hence both colons
 clean::
 	rm -f .coq_makefile_input .coq_makefile_output build/CoqMakefile.make
-	find TypeTheory \( -name .\*.aux -o -name \*.glob -o -name \*.v.d -o -name \*.vo \) -delete
-	find TypeTheory -type d -empty -delete
+	find Modules \( -name .\*.aux -o -name \*.glob -o -name \*.v.d -o -name \*.vo \) -delete
+	find Modules -type d -empty -delete
 clean::; rm -rf $(ENHANCEDDOCTARGET)
 latex-clean clean::; cd $(LATEXDIR) ; rm -f *.pdf *.tex *.log *.aux *.out *.blg *.bbl
 
@@ -181,7 +181,7 @@ doc: $(GLOBFILES) $(VFILES)
 	sed -i'.bk' -f $(ENHANCEDDOCSOURCE)/proofs-toggle.sed $(ENHANCEDDOCTARGET)/*html
 
 # Jason Gross' coq-tools bug isolator:
-# The isolated bug will appear in this file, in the TypeTheory directory:
+# The isolated bug will appear in this file, in the Modules directory:
 ISOLATED_BUG_FILE := isolated_bug.v
 # To use it, run something like this command in an interactive shell:
 #     make isolate-bug BUGGY_FILE=Foundations/Basics/PartB.v
@@ -209,7 +209,7 @@ $(LATEXDIR)/doc.pdf : $(LATEXDIR)/helper.tex $(LATEXDIR)/references.bib $(LATEXD
 	cd $(LATEXDIR) && latexmk -pdf doc
 
 $(LATEXDIR)/coqdoc.sty $(LATEXDIR)/helper.tex : $(VFILES:.v=.glob) $(VFILES)
-	$(COQDOC) -Q TypeTheory TypeTheory $(COQDOC_OPTIONS) $(COQDOCLATEXOPTIONS) $(VFILES) -o $@
+	$(COQDOC) -Q Modules Modules $(COQDOC_OPTIONS) $(COQDOCLATEXOPTIONS) $(VFILES) -o $@
 
 .PHONY: enforce-max-line-length
 enforce-max-line-length:

.dir-locals.el → Modules/.dir-locals.el

@@ -2,4 +2,4 @@
   . ((eval . 
 	   (progn
 	     (make-local-variable 'coq-prog-args)
-	     (setq coq-prog-args `("-emacs" "-indices-matter" "-type-in-type" "-R" ,(expand-file-name (locate-dominating-file buffer-file-name ".dir-locals.el")) "Largecat" )))))))
+	     (setq coq-prog-args `("-emacs" "-indices-matter" "-type-in-type" "-R" ,(expand-file-name (locate-dominating-file buffer-file-name ".dir-locals.el")) "Modules" )))))))

Modules/Prelims/.package/files

@@ -0,0 +1,4 @@
+ardef.v
+modules.v
+quotientfunctor.v
+uniproof.v

ardef.v → Modules/Prelims/ardef.v

@@ -10,7 +10,7 @@ Require Import UniMath.CategoryTheory.limits.terminal.
 Require Import UniMath.CategoryTheory.limits.bincoproducts.
 
 Require Import UniMath.CategoryTheory.Monads.
-Require Import Largecat.modules.
+Require Import Modules.Prelims.modules.
 (* Require Import UniMath.CategoryTheory.Modules. *)
 
 

uniproof.v → Modules/Prelims/uniproof.v

@@ -11,7 +11,7 @@ Require Import UniMath.CategoryTheory.limits.bincoproducts.
 Require Import UniMath.CategoryTheory.Epis.
 
 Require Import UniMath.CategoryTheory.Monads.
-Require Import Largecat.modules.
+Require Import Modules.Prelims.modules.
 (* Require Import UniMath.CategoryTheory.Modules. *)
 
 
@@ -32,8 +32,8 @@ Notation "α 'ø' Z" := (pre_whisker Z α)  (at level 25).
 Notation "Z ∘ α" := (post_whisker α Z) (at level 50, left associativity).
 
 
-Require Import Largecat.ardef.
-Require Import Largecat.quotientfunctor.
+Require Import Modules.Prelims.ardef.
+Require Import Modules.Prelims.quotientfunctor.
 
 (* Let f : A -> B be a function.
 It induces an equivalence relation on A.