hott / coq-hott

A Coq library for Homotopy Type Theory

Homotopy Type Theory is an interpretation of Martin-Löf’s intensional type theory into abstract homotopy theory. Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. As the natural logic of homotopy, type theory is also related to higher category theory as it is used e.g. in the notion of a higher topos.

The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.

More information about this library can be found in:

• The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 arXiv CPP17

Other publications related to the library can be found here.

Installation

The HoTT library is part of the Coq Platform and can be installed using the installation instructions there.

More detailed installation instructions are provided in the file INSTALL.md.

Usage

The HoTT library can be used like any other Coq library. If you wish to use the HoTT library in your own project, make sure to put the following arguments in your _CoqProject file:

-arg -noinit
-arg -indices-matter

For more advanced use such as contribution see INSTALL.md.

We recommend the following text editors:

• Emacs together with Proof General.
• CoqIDE part of the Coq Proof Assistant.
• Visual Studio Code together with VSCoq.

Other methods of developing in coq will work as long as the correct arguments are passed.

Contributing

Contributions to the HoTT library are very welcome! For style guidelines and further information, see the file STYLE.md.

Licensing

The library is released under the permissive BSD 2-clause license, see the file LICENSE.txt for further information. In brief, this means you can do whatever you like with it, as long as you preserve the Copyright messages. And of course, no warranty!

Wiki

More information can be found in the Wiki.

coq-hott's Issues

complete types/Sigma

Complete types/Paths

Port FunextEquivalences (from old HoTT)

Reduce clashes with Coq

Where we have departed from Coq’s names (eg Unit, Empty, …), make our definitions notations for Coq’s own, for better compatibility.

A list of known clashes:

• unit (coq) vs Unit (HoTT)
• Empty_set (coq) vs Empty (HoTT)
• 'not A := A -> False(coq) vsnot A := A -> Empty` (HoTT)

Questionable clashes:

• identity and eq (coq) vs paths

Complete types/Forall

Why are the Oberwolfach tutorials copied over rather than included as a submodule?

I see my Oberwolfach tutorials are copied to the repository. It would be better to include them as a submodule. Then if I update my version of the notes, the change will be reflected here.

Port HLevel (from old HoTT)

Complete types/Unit

Complete types/Arrow

Port Funext (from old HoTT)

Complete types/Prod

Compilation error with Coq 8.4

The compilation of the project fails when using Coq 8.4 with the following error message:

File "./Equivalences.v", line 583, characters 8-11:
Error: Impossible to unify "?2025 == ?2026" with "A".

With Coq 8.3pl4 everything runs through smoothly. Given that 8.4 is not totally backwards compatible with 8.3 this is not completly unexpected behaviour but I think it would be nice to explicitly state which version(s) of Coq are known to work. As of now "README.markdown" says:

"You will need Coq version 8.3 or newer to compile the files."

which one could argue is not really the case.

Anomaly in hoqtop on inversion tactic

The following code run through hoqtop/hoqc gives an anomaly. (This is where my global Coq is the trunk of HoTT/coq; I'm working on compiling the stable branch now.) (I realize that this is something that shouldn't be done with "fake higher inductive types", but I figured I'd report it, in case it was an unintended anomaly...)

Require Import Overture.

Inductive interval := zero | one.
Axiom seg : zero = one.
Goal False.
  pose proof seg as P.
  inversion P.
(* Toplevel input, characters 0-11:
Anomaly: in Coqlib: cannot find Coq.Init.Logic.eq:
Coqlib: cannot find Coq.Init.Logic.eq. Please report.
*)

Medium-term: reorganise library

Various problems with current library organisation: especially, interdependencies, between files, etc. In particular, e.g. results about equivalences cannot go in Equiv.v, because they depend on files from the types directory, which depend on Equiv.v.

No-one is ready to do it now, BUT: before too long someone (ideally a couple of us, to maintain consensus?) should try something like the following:

• work in a new branch!
• find everything from Contr.v, Equiv.v, Trunc.v, etc that’s used by the Types directory; hopefully this will not be much more than the definitions;
• move these into a file Basics.v, on which the types files will then depend;
• allow Equiv.v etc. to depend on the types files.

Port FiberEquivalences (from old HoTT)

"make" does (almost) nothing, after modifications and even after "make clean"

make intermittently fails to detect when it should be (re)compiling files after modifications. Usually make clean successfully resets this, but sometimes even this doesn’t help: it re-runs coqdep, but not hoqc.

I’ve had this happen on multiple occasions, but have no idea how to reproduce it, I’m afraid. Have others had the same problem?

Sample terminal session output.

I’m running Mac OS 10.6.8; can provide further system details if anyone has ideas what might be relevant.

Stand-alone?

We have now defined our own concat and inverse in Paths.v, even though the equivalent identity_trans and identity_sym exist in the standard library. Would it make sense to just go all independent and define our own identity type? And call it paths? I think the ssreflect library won't be too happy about that.

Complete types/Sum

We’re not sure if we really need this.

Unit in Prop ??

Check Unit.
Unit : Prop
Inductive HoTT.types.Unit.Unit

I thought we had managed to ban Prop?

port 2Sphere1 and Pi1S2 from Dan Licata's Agda Library

First step in moving Agda proofs to Coq.

Port UsefulEquivalences (from old HoTT)

Port UnivalenceImpliesFunext (from old HoTT)

Complete types/Empty[Set]

Empty, or EmptySet?

To assign to Dan G.

Contractible.v

Reorganize Contractible.v so that it uses canonical structures.

In the absence of "contradict"

This is either a taste issue or a documentation issue; since the hlevel of a W-type is at most that of its constructor indexing type (when that's positive), can we restore some of the machinery for concluding pathwise-separation? e.g., Inductive bool := | true | false. and Inductive Empty :=. have "decidable equality" in the sense that the eq type is a finite table; but what's the way to get a map ( true = false -> Empty)?

Complete types/Record

Port Automation

The old library had lots of Ltac commands. Do we want to port them?

Equivalences.v:Ltac contract_hfiber y p :=
Equivalences.v:Ltac cancel_inverses_in s :=
Equivalences.v:Ltac cancel_inverses :=
Equivalences.v:Ltac expand_inverse_src w x :=
Equivalences.v:Ltac expand_inverse_trg w x :=
Equivalences.v:Ltac equiv_moveright :=
Equivalences.v:Ltac equiv_moveleft :=
Paths.v:Ltac path_induction :=
Paths.v:Ltac apply_happly :=
Paths.v:Ltac path_simplify :=
Paths.v:Ltac path_simplify' lem :=
Paths.v:Ltac path_via mid :=
Paths.v:Ltac path_using mid lem :=
Paths.v:Ltac path_via' mid :=
Paths.v:Ltac associate_right_in s :=
Paths.v:Ltac associate_right :=
Paths.v:Ltac associate_left_in s :=
Paths.v:Ltac associate_left :=
Paths.v:Ltac unwhisker :=
Paths.v:Ltac cancel_units_in s :=
Paths.v:Ltac cancel_units :=
Paths.v:Ltac partly_cancel_left_opposite_of_in p s :=
Paths.v:Ltac cancel_left_opposite_of p :=
Paths.v:Ltac partly_cancel_right_opposite_of_in p s :=
Paths.v:Ltac cancel_right_opposite_of p :=
Paths.v:Ltac cancel_opposite_of p :=
Paths.v:Ltac cancel_opposites_in s :=
Paths.v:Ltac cancel_opposites :=
Paths.v:Ltac do_opposite_opposite_in s :=
Paths.v:Ltac do_opposite_opposite :=
Paths.v:Ltac apply_opposite_map :=
Paths.v:Ltac do_opposite_map_in s :=
Paths.v:Ltac do_opposite_map :=
Paths.v:Ltac undo_opposite_map_in s :=
Paths.v:Ltac undo_opposite_map :=
Paths.v:Ltac do_opposite_concat_in s :=
Paths.v:Ltac do_opposite_concat :=
Paths.v:Ltac undo_opposite_concat_in s :=
Paths.v:Ltac undo_opposite_concat :=
Paths.v:Ltac apply_compose_map :=
Paths.v:Ltac do_compose_map_in s :=
Paths.v:Ltac do_compose_map :=
Paths.v:Ltac undo_compose_map_in s :=
Paths.v:Ltac undo_compose_map :=
Paths.v:Ltac do_concat_map_in s :=
Paths.v:Ltac do_concat_map :=
Paths.v:Ltac undo_concat_map_in s :=
Paths.v:Ltac undo_concat_map :=
Paths.v:Ltac moveright_onright :=
Paths.v:Ltac moveleft_onright :=
Paths.v:Ltac moveleft_onleft :=
Paths.v:Ltac moveright_onleft :=
Univalence.v:Ltac undo_concat_to_compose_in s :=
Univalence.v:Ltac undo_concat_to_compose :=
Univalence.v:Ltac undo_opposite_to_inverse_in s :=
Univalence.v:Ltac undo_opposite_to_inverse :=

Also, we may want to think about what should go into the path_hints database.

Fix HIT definitions.

Rewrite the defined HIT eliminators as described to Yves’ email today, so that Anthony’s inconsistency isn’t available for them.

Name clash: [isequiv_cancelR] and relatives

(This one is my fault!) Currently used both for the lemma in /theories/Equivalences.v allowing us to cancel equivalences:

Global Instance isequiv_cancelR : IsEquiv g
:= isequiv_homotopic (compose (compose g f) f^-1) g
     (fun b => ap g (eisretr f b)).

and for the lemma in /theories/types/Paths.v showing that cancelR (which cancels paths) is an equivalence:

Definition isequiv_cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
  : IsEquiv (cancelR p q r).

The latter seems to fit our current naming conventions better (the pattern [isequiv_somelemma]). Any objections if I rename the former to [cancelR_isequiv], or any suggestions for better names?

FunextAxiom gives Universe inconsistency

I am getting a Universe Inconsistency in my development.
Error: Universe inconsistency (cannot enforce HoTT.FunextAxiom.12 =
Top.3367 because Top.3367 <= Top.3368 < HoTT.FunextAxiom.12).

I would imaging we want to make FunextAxiom polymorphic with
Set Universe Polymorphism.

"only global references can be polymorphic hints"

I get an error building the latest hott/hott with the latest hott/coq. Any ideas?

/usr/local/hott/bin/coqtop -indices-matter -boot -nois -coqlib ./coq -R ./coq/theories Coq -compile coq/theories/Init/Peano
File "/usr/local/hott/src/hott/files/HoTT/coq/theories/Init/Peano.v", line 35, characters 0-30:
Error: (f_equal S)
is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints.
make[1]: *** [coq/theories/Init/Peano.vo] Error 1

Equivalences

Reorganize equivalences so that they use canonical structures. Also think about what to call the various files, it is a bit silly that we have a file called UsefulEquivalences.v.

The IT subdirectory is problematic

The IT subdirectory which contains the development of W-types by Steve Awodey and Kristina Sojakova is problematic. It contains a copy Vladimir Voevodsky's Coq files copied over. This is bad because it allows us no way of synchronizing with Vladimir. When Steve copied my Oberwolfach tutorials it didn't matter so much, but now we are reaching a point where we will be sorry for bad practices.

Further, IT/identity/identity.v redefines a lot of stuff that is already defined in paths.v, for example notations such as @, and it makes an incompatible notation p! (whereas in the rest of repository it is !p).

The IT subdirectory is properly a sub-project of Vladimir's files and that's where it should be. It does not even depend on anything else in HoTT.

I think we have reached a stage when we have to be far more conservative about accepting things into the main HoTT repository. The repository is watched by 30 people and forked by 14, and we should care about them.

I propose that IT be removed from HoTT. It can of course still live on Kristina's fork, nobody is forcing her to do anything.

We also need to set clear guidelines about what gets accepted. For example, I think we should never accept a pull request which has insufficient description of changes. The person who accepts a pull request should read every single change made to the repository, etc.

We could also consider reducing the number of people who are permitted to make pull requests. This seems to work well. For example, in my project on the eff programming language, Matija Pretnar is the only person who can accept pull requests, even though I am a co-author of the language. This way a certain level of coherence is achieved.

Let me know what you think.

Notation reversion n

I'm sure the new proofs and new theorems are all very helpful, and separating ExtensionalityAxiom from UnivalenceAxiom makes perfect sense; but for those of us who would like to use these files and not work on them, could the developers settle on a stable basic interface, particularly wrt notations? I suppose it ought to be possible to define new notations meaning the same as the old ones in a local file "Notations.v", but coq complains about trying to overide old ones without constraining the "Scope" (whatever that is...), and I can't feel sure that collisions won't occur --- after all, there are only a couple thousand pictures one can draw in three special characters, and most of them don't look like much. On top of which, it would be just an ugly kludge!

Transport.v

The old Fibrations.v contained a lot of facts about transport. These should be reorganized into Fibrations.v.

Notation 'idmap'

I'm not sure if this is the right place to note this, or if anyone cares, but in Overture.v, it's not necessary to quote idmap in Notation "'idmap'" := ...; I believe it suffices to do Notation idmap := .... Also, I'm curious if/why it's better to have Notation idmap := (fun x => x). rather than Definition idmap {T} : T -> T := (fun x => x). Arguments idmap {T} / x.

HoTT does not export EquivalenceVarieties

Was this deliberate, or just an unintended omission? If the latter, I will add it.

Add Miscellaneous file for homeless lemmas

Add a Misc.v file for lemmas/groups that don’t have good homes in existing files, and aren’t large enough to warrant files of their own.

Document clearly that this a suboptimal place to put things, and that lemmas in it should be re-housed whenever possible — but (agreed at meeting today) it seems better to have this than to hide such lemmas in files where they don’t belong.

Complete types/Universe

Bool in Type instead of Set?

theories/types/Bool.v defines Bool as being in "Type".

Shouldn't it be in "Set"? (Or does that not matter now?)

minor corrections to hits chapter

i corrected a number of typo's, one mistake (the base path of the example about natural numbers induction was specified as s rather than suc), and one wording change ("concision" rather than "conciseness"). if my experience is typical, there are probably a lot of spelling errors remaining. i can check them if it is wanted.

Port FiberSequences (from old HoTT)

Capitalisation conventions

Adhere better to our declared capitalisation etc. conventions: names of types should typically be capitalised, names of other objects should not be (including when they include names of types).

Also: DOCUMENT this (and other conventions) in the wiki!

Two theorems with same name

There are two theorems with the name "equiv_path_inverse" in the HoTT library: one in Universes.v and one in Paths.v. They of course have different types:

Definition equiv_path_inverse `{Funext} (A B : Type) (p : A = B) :
equiv_path B A (p^) = equiv_inverse (equiv_path A B p).

Definition equiv_path_inverse {A : Type} (x y : A)
: (x = y) <~> (y = x)

Complete types/Bool

Pullbacks?

What is the status of pullbacks?
./Experimental/Pullback.v
./old/UsefulEquivalences.v

Create types/Sum.v (or types/Coprod.v ?)

This seems to have been overlooked (or not needed upto now).

Rewrites working slowly

The rewrites in these two files work very slowly:

https://github.com/kristinas/hinitiality/blob/master/w/w_alg.v
https://github.com/kristinas/hinitiality/blob/master/two/two_alg.v

The proof terms themselves aren't that big so I don't see why it should be so slow.

Port HSet (from old HoTT)

Style Guide

(This and following issues are to-dos generated from the working group meeting, 2013-01-30.)

Put a list of conventions on the wiki. To include:

• Notational conventions
• Use of type classes (esp. for axioms)