This repository has been archived by the owner. It is now read-only.
Permalink
Browse files

Cleaning up the UnivalentFoundations library, and adding .gitignore f…

…iles all over the place
  • Loading branch information...
andrejbauer committed Mar 6, 2011
1 parent 1bc2ff6 commit cb1dd1a0c55da906e93083460668aacd0a3f8fa1
View
@@ -0,0 +1,11 @@
+# Ignore Emacs backup files
+*~
+# Ignore the .DS_Store file generated on a Mac
+.DS_Store
+# Ignore files generated by the Coq compiler
+*.vo
+*.glob
+# Ignore files generated by LaTeX
+*.aux
+*.log
+*.out
@@ -0,0 +1,2 @@
+# Ignore the auxiliary LaTeX file generated by coqdoc
+univalence_body.tex
@@ -0,0 +1 @@
+.depend
@@ -13,6 +13,8 @@ Definition function_extensionality_statement := forall A B (f g : A -> B), (fora
Section UnivalenceImpliesFunctionExtensionality.
+ (** * Univalence and Eta rule Imply Function Extensionality *)
+
Hypothesis univalence : univalence_statement.
Hypothesis eta_axiom : forall {A B} (h : A -> B), eta h ~~> h.
@@ -87,7 +89,6 @@ Section UnivalenceImpliesFunctionExtensionality.
apply opposite; apply concat_associativity.
path_via (idpath (f y) @ p y).
path_via (! map f q @ map f q).
- apply opposite; apply opposite_map.
Defined.
(** The eta axiom essentially states that [eta] is a weak equivalence. *)
@@ -172,4 +173,4 @@ Section UnivalenceImpliesFunctionExtensionality.
apply idpath.
Defined.
-End UnivalenceImpliesFunctionExtensionality.
+End UnivalenceImpliesFunctionExtensionality.
@@ -176,7 +176,7 @@ Ltac path_induction :=
not equal to [p] but only conntected to it with a path. We call paths between paths
_homotopies_. The following lemmas should be self-explanatory. *)
-Lemma idpath_left_unit A (x y : A) (p : x ~~> y) : (idpath x @ p) ~~> p.
+Lemma idpath_left_unit A (x y : A) (p : x ~~> y) : idpath x @ p ~~> p.
Proof.
path_induction.
Defined.
@@ -209,10 +209,6 @@ Defined.
(** We place the lemmas just proved into the [Hint Resolve] database so that
[auto] will know about them. *)
-Hint Resolve
- idpath_left_unit idpath_right_unit
- opposite_right_inverse opposite_left_inverse.
-
Lemma concat_associativity A (w x y z : A) (p : w ~~> x) (q : x ~~> y) (r : y ~~> z) :
(p @ q) @ r ~~> p @ (q @ r).
Proof.
@@ -229,14 +225,14 @@ Defined.
(** A path [p : x ~~> y] in a space [A] is mapped by [f : A -> B] to a map [map f p : f x
~~> f y] in [B]. Note that we cannot transfer [p] by just composing it with [f] because
- [p] is _not_ a function. Instead, we use the induction principle. *)
+ [p] is _not_ a function. *)
-Lemma map {A B} {x y : A} (f : A -> B) (p : x ~~> y) : f x ~~> f y.
+Lemma map {A B} {x y : A} (f : A -> B) : x ~~> y -> f x ~~> f y.
Proof.
path_induction.
Defined.
-(** The next two lemmas state that [map f p] is "functorial" in the path [p]. *)
+(** The next two lemmas state that [map_path f p] is "functorial" in the path [p]. *)
Lemma idpath_map A B (x : A) (f : A -> B) : map f (idpath x) ~~> idpath (f x).
Proof.
@@ -264,7 +260,7 @@ Defined.
(** Other facts about map. *)
-Lemma opposite_map A B (f : A -> B) (x y : A) (p : x ~~> y) : ! (map f p) ~~> map f (! p).
+Lemma opposite_map A B (f : A -> B) (x y : A) (p : x ~~> y) : map f (! p) ~~> ! map f p.
Proof.
path_induction.
Defined.
@@ -275,7 +271,6 @@ Proof.
path_induction.
Defined.
-
(** So far [path_induction] has worked beautifully, but we are soon going to prove more
complicated theorems which require smarter tactics, so we define some.
@@ -288,10 +283,14 @@ Defined.
A specific [Hint Resolve] database [db] can be used with [auto with db]. *)
Hint Resolve
- concat_map
+ @idpath @opposite
+ idpath_left_unit idpath_right_unit
+ opposite_right_inverse opposite_left_inverse
+ homotopy_concat @map
+ idpath_map concat_map idmap_map composition_map
opposite_map map_cancel
opposite_concat opposite_opposite
- homotopy_concat : path_hints.
+ : path_hints.
(** By the way, we can add more hints to the database later. *)
@@ -314,6 +313,24 @@ Ltac path_tricks :=
Ltac path_via x := apply @concat with (y := x); path_tricks.
+Ltac path_simpl :=
+ repeat progress first [
+ apply idpath_left_unit
+ | apply idpath_right_unit
+ | apply opposite_right_inverse
+ | apply opposite_left_inverse
+ | apply opposite_concat
+ | apply opposite_opposite
+ | apply map
+ | apply idpath_map
+ | apply concat_map
+ | apply idmap_map
+ | apply composition_map
+ | apply opposite_map
+ | apply map_cancel
+ | idtac
+ ].
+
(** Here are several more facts about [map] which have slightly more involved proofs. We use
the just defined tactics. The proofs a little too manual, obviously we need even better
tactics which will allow us to argue about paths as if they were equalities. *)
@@ -324,7 +341,6 @@ Proof.
induction q.
path_via (p x).
apply idpath_left_unit.
- apply opposite; apply idpath_right_unit.
Defined.
Hint Resolve map_naturality : path_hints.
@@ -336,7 +352,6 @@ Proof.
path_via (p x).
path_via (idpath (f x) @ p x).
path_via (p x @ idpath (g x)).
- apply opposite; auto.
Defined.
Lemma concat_cancel_right A (x y z : A) (p q : x ~~> y) (r : y ~~> z) : p @ r ~~> q @ r -> p ~~> q.
@@ -353,7 +368,6 @@ Proof.
induction p.
induction r.
path_via (idpath x @ q).
- apply opposite; auto.
Defined.
Lemma concat_move_over_left A (x y z : A) (p : x ~~> z) (q : x ~~> y) (r : y ~~> z) :
@@ -385,7 +399,6 @@ Lemma map_action A (f : A -> A) (p : forall x, f x ~~> x) (y z : A) (q : f z ~~>
Proof.
path_via (p (f z) @ q).
apply endomap_homotopy_commute.
- apply opposite; apply map_naturality.
Defined.
(** * Homotopy between maps
@@ -500,7 +513,6 @@ Proof.
path_via q.
path_via (!(idpath (f x)) @ q).
path_via (idpath (f x) @ q).
- apply opposite; auto.
Defined.
(** A weak equivalence is a map whose homotopy fibers are contractible. *)
@@ -1,14 +1,11 @@
-# Edit the following parameters if the Makefile does not succeed The
-# directory which contains the Coq executables (leave it empty if coqc
-# is in the PATH)
+# Edit the following parameter(s) if "make" fails to find the executables
+
+# The directory which contains the Coq executables (leave it empty if
+# coqc is in the PATH), for example on my Mac I would set
+# COQBIN=/Applications/CoqIdE_8.3.app/Contents/Resources/bin/
COQBIN=
# Edit below at your own risk
-
-COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
-
-COQLIBS:=-I .
-
COQC:=$(COQBIN)coqc
COQDEP:=$(COQBIN)coqdep
COQDOC:=$(COQBIN)coqdoc
@@ -26,25 +23,42 @@ GLOBFILES:=$(VFILES:.v=.glob)
.PHONY: all .depend html latex pdf
-all: .depend $(VOFILES)
+all: .depend $(VOFILES) doc
clean:
- /bin/rm -f *.vo *.glob *.~ doc/html/* doc/latex/*
+ /bin/rm -f *~ *.vo *.glob *.~ doc/html/* doc/latex/*
doc: html pdf
html: $(GLOBFILES)
$(COQDOC) --html --toc --utf8 --charset utf8 --interpolate --no-lib-name -d doc/html $(VFILES)
/bin/cp -f homotopy.css doc/html/coqdoc.css
+ echo +++++;\
+ echo +++++ HMTL documentation doc/html was generated successfully;\
+ echo +++++
-latex:
- echo Would generate LaTeX
+latex: $(GLOBFILES)
+ $(COQDOC) --latex --toc --utf8 --charset utf8 --interpolate -o doc/latex/UnivalentFoundations.tex $(VFILES)
+ if [ ! -f doc/latex/coqdoc.sty ] ; then echo coqdoc.sty not found, using my own; cp coqdoc.sty doc/latex; fi
pdf: latex
- echo Would generate PDF
+ if [ -x "`which latexmk`" ]; \
+ then \
+ echo Good, you have latexmk; \
+ cd doc/latex; \
+ latexmk -pdf UnivalentFoundations.tex; \
+ else \
+ echo Using pdflatex to generated PDF; \
+ cd doc/latex; \
+ pdflatex UnivalentFoundations.tex; \
+ pdflatex UnivalentFoundations.tex; \
+ fi
+ echo +++++;\
+ echo +++++ PDF document doc/latex/UnivalentFoundations.pdf was generated successfully;\
+ echo +++++
.depend:
- $(COQDEP) $(COQLIBS) $(VFILES) > .depend
+ $(COQDEP) -I . $(VFILES) > .depend
%.vo %.glob: %.v .depend
$(COQC) $<
@@ -0,0 +1,13 @@
+This folder contains a Coq implementation of Univalent Foundations.
+
+It is based on Vladimir Voevodsky's initial implementation. So far we have
+only reimplemented a small proportion of Vladimir's files.
+
+Type "make" to compile the Coq files and generate documentation. You will have
+to have installed:
+
+1. Coq 8.3 (it might work with 8.2 and if there is enough interest, we can make sure
+ that the files are compatible with 8.2).
+
+2. For generation of the PDF files you need pdflatex. The latexmk utility is desirable
+ but not required.
Oops, something went wrong.

0 comments on commit cb1dd1a

Please sign in to comment.