I've written out some notes for HoTT Ch. 2. Posting here for comments and corrections: https://artagnon.com/notes/HoTT

You may have better luck at the HoTT zulip

Hey, could you link me to it?

I read somewhere (but I don't remember where) that hott could simplify some structure in Coq, like quotient. Is there some info on that ? I'm still figuring out the main concepts of HoTT, and I'm curious to see how it could help for quotient.

@vlj: you can define quotients as a Higher Inductive Type (one of the outcomes of the types-as-spaces correspondence). In virtual Coq's syntax, the quotient of `A`

by a relation `R`

would be:

```
Inductive quo A R :=
| quo_in : A -> quo A R
| quo_eq : forall a b : A, R a b -> quo_in A R a = quo_in A R b.
```

In passing, no need for `R`

to be an equivalence relation, its reflexive-symmetric-transitive closure will be automatically considered.

thanks. Hott ensure that quo_eq will be properly typed ? I mean quo_eq is an equality type over quo_in so I'm expecting coq to fail typing

@vlj it depends a bit what your goals are. As explaine by @Hugo Herbelin, HoTT often assumes the existence of a certain class of HITs (Higher inductive types) among which the coequalizer `quo`

(note however that this does not generate a type as simple as it might look at first sight: for instance quotienting an h-set (= verify UIP) A by an arbitrary relation R may not result an h-set `quo A R`

but there are ways to fix that). However you could just as well axiomatize quotients and "pure" HoTT won't give you much more in practice if you are only interested in working with quotients (it's another story if you go to cubical theories such as cubical agda that computes much more - you have more definitional equalities).

One point of interest for HoTT is that it allows to analyze equality in a rather sensible fashion and to find conditions where the above construction produces types with UIP for instance.

ok

I'm not sure I understand the issue with quotient in Coq in the first place to be honest, in some discussion the argument of quotient being difficult to express in coq comes often so I though this was an issue in the first place but I didn't try myself.

Axiomatizing quotients is as simple in Coq as in any other dependent type theory, here is a sketch:

given a type `A : Type`

and a relation `R : A -> A -> Type`

, postulate the existence of a type `quo A R`

with an operation `quo_in : A -> quo A R`

that sends an element of type `A`

to its equivalence class modulo `R`

, an equality `quo_eq a b w : quo_in a = quo_in b`

for any witness `w : R a b`

that `a`

and `b`

are in relation (so they define the same equivalence class) and an eliminator `quo_elim : forall (P : quo A R -> Type) (Hin : forall a : A, P (quo_in a)) (Heq : forall (a b : A) (w : R a b), rew [P] (quo_eq a b w) in Hin a = Hin b), forall (q : quo A R), P q`

and a computation rule for this eliminator stated as a propositional equality `quo_elim P Hin Heq (quo_in a) = Hin a`

.

Working with these axiomatic quotients is also as painful as in any other dtt, the main problem coming from the fact that the computation rule is only propositional and not definitional (so the "eliminator" do not reduce in conversion) but that's entirely possible.

In order to sidestep this problem, you can either 1) restrict the class of quotients that you want to consider (typically if you can pick out some canonical element for each equivalence class -- I think that's the approach taken by @Cyril Cohen here), or 2) change your dtt by adding more conversion rules (this path have been taken in lean 3 which leads to discutable consequences; I'm frequently playing around with quotients in Agda adding a rewrite rule by hand; at some level the cubical version of HoTT implemented in cubical-agda also provides corresponding computation rules).

Kenji Maillard said:

you can either 1) restrict the class of quotients that you want to consider (typically if you can pick out some canonical element for each equivalence class -- I think that's the approach taken by Cyril Cohen here), or 2) (...).

Indeed. Note that this work by C. Cohen is now part of mathcomp-ssreflect, and the source file has a hopefully informative documentation header. The main idea is to package the type `A`

, as in Kenji's message, with another type `T`

, the quotient type, and an explicit surjection `A -> T`

. Instances can constructed, either with explicit quotient types and surjections, or as corollaries of a non-effective choice axiom, or etc. Then the library is about useful infrastructure for notations, transfer of structures, etc.

are there any highlights in mathcomp of using quotients defined in this way for working-class math? (As in, just proving some useful non-research math results in a better way than without quotients)

Thanks for the info !

Btw is it expected that coq-hott does not install in user contrib when installed via opam ?

I tried to install coq-hott via opam, but I have an error message when I try to import it : `Compiled library HoTT.HoTT (in file /home/vlj/.opam/default/share/hott/theories/HoTT.vo) makes inconsistent assumptions over library Coq.Init.Notations`

via vscoq (I'm using WSL2 but usually it works well)

usually this hints at mismatching coq version between what was used to build the lib and the toplevel that tries to load the lib

but with opam it should be nicely handled ?

it happens on 2 different machines

You're supposed to use the hoq* (hoqtop, hoqide, hoqc) wrappers instead of coq directly

alternatively pass the right -coqlib and -R options to coq

I don't know if opam installs the hoq* in your path

The hott library requires a patched version of coq IIRC, some instructions are given in their readme

ho I though it was vanilla coq

indeed there is a hoqtop in the bin/ of opam

thanks !

@vlj You might also be interested in the HoTT zulip. More of the HoTT developers are hanging around there.

@Kenji Maillard IIUC, a patched version of coq is unnecessary.

Karl Palmskog said:

are there any highlights in mathcomp of using quotients defined in this way for working-class math? (As in, just proving some useful non-research math results in a better way than without quotients)

Hi @Karl Palmskog see, e.g., the construction of algebraic numbers (aka the fundamental theorem of algebra, algebraic part). This is done here.

There are other examples in commutative algebra, for constructions related to field extensions.

I tried to follow the instruction here : https://hott.github.io/HoTT-2019/coq-installation/ instead of installing via opam, but hoqide doesn't work `Fatal error: coqide with -indices-matter was not found during configuration.`

Is there something I'm missing ? On google I don't really find similar error

I'm in the middle of something. Here are the official install instructions. https://github.com/HoTT/HoTT/blob/master/INSTALL.md

@Ali Caglayan or @Gaëtan Gilbert may know more.

(generally, I prefer to know who am talking to. Who are you vlj ?)

I don't know about hott's install_coq stuff

maybe it just doesn't build coqide

@vlj How are you running hoqide?

And can you give me the output of `./configure`

?

@Bas Spitters I'm Vincent Lejeune, vlj on github, I'm rather on mathcomp/analysis at the moment. I'm a coq beginner.

@Ali Caglayan I'm trying to launch ./hoqide

and here is the ouput of configure : https://gist.github.com/vlj/738767900150266de4169a2895c00c83

Ah so configure is finding your opam install

Can you try ` ./configure COQBIN="`

pwd`/coq-HoTT/bin"`

This should be the "custom" version of coq that the HoTT library uses

```
./configure COQBIN="`pwd`/coq-HoTT/bin"
```

now the output is : https://gist.github.com/vlj/db1f93e50652e7244f72f37ba467646b

can I do make directly or do I need to make clean before ?

Do a `make clean`

to be sure

btw, you can paste your log here, zulip condenses long messages anyway. Just stick the log between a pair of 3 backticks

ok

btw the configure log tells that `configure: Could not find coqide, will not make hoqide`

Ah ok, so it looks like the local version of coq wasn't installed

nvm

Did you run ` etc/install_coq.sh`

?

yes but I think I erased it with make distclean

(I'm rebuilding it )

It will take a bit of time unfortunately

Afterwards, make sure you run

```
./autogen.sh
./configure COQBIN="`pwd`/coq-HoTT/bin"
make
```

You can do `make -j n`

for the last bit if you wish

install_coq.sh will compile coqide ?

It should do

But it will be a local version that is not installed

Then when you run ./configure with the correct argument it will configure the scripts hoqc and hoqide to point to the local versions

After you finish running make you should be able to run hoqide

yes ! this time it found a coqide in coq-HoTT

@vlj Is that all working then?

hocq is still building

but the configure told that it found a coqide in the right location

it works ! I have the ide

launch with hoqide

thanks a lot for the help!

Some strangeness here, with respect to precedence of `~`

and `+`

. Does anyone (cc: @Hugo Herbelin ) know why the precedence of `+`

is higher than that of `~`

?

Also, does anyone know why `auto`

works here? There is obviously no LEM in stdlib, and the goal is `P + (~ P)`

with hyp `~ P + (~P)`

.

@Ramkumar Ramachandra very roughly, under double negation you get classical logic

for a more accurate statement, see https://en.wikipedia.org/wiki/Double-negation_translation

Cool, thanks :)

This of course is a modality in HoTT...

I'm having some trouble with the category notation. In https://github.com/HoTT/HoTT/blob/master/theories/Categories/Category/Core.v there are a couple notations I'd like to use, like "-->" or "o" but coq complains that it doesn't find the notation. Does the "Local Notation" means that they can't be used outside of the CategoryCoreNotations module ? But then I don't understand why they are defined since they are not used afterwards in this file and thus in this module.

Repro code:

```
Require Import HoTT.Categories.Category.
Import HoTT.Categories.Category.CategoryCoreNotations.
Local Open Scope category_scope.
Section Ex_2_1_15_4.
Context (C:PreCategory) (A:object C) (u: A --> A).
Lemma part1:
forall B: object C, forall (g:morphism C A B), g o u = g -> u = identity A.
```

Adding a Local Open Scope morphism_scope allows me to use "o" but I don't know how to get the "-->"

@vlj “Local Notation” is indeed not exported; I’d copy-paste one of the notation definitions (not sure which, `-->`

has conflicting definitions), so I don’t get that code either. And I can’t easily find uses of `-->`

in code (at least from GitHub’s limited search).

Yes usong github search the only usage of the notation is in comments

I'm not sure why this notation is introduced, maybe a leftover from a code cleaning attemp

HoTT built coq doesn't ship with ssreflect ? I tried to import ssreflect but it said there was some conflict in the definitions, it's like it loads a lib built with another coq, I have opam with mathcomp installed so I guess it may use ssreflect from there for some reasons

(I have 2 coqs, a vanilla one and the one from coq hott)

if you install those Coqs in different `opam switches`

, and use appropriate `eval $(opam env)`

to switch across the two, that should become impossible

(and normal Coq itself only ships with “minimal” ssreflect (the tactics and 3 modules), most of the rest is in separate packages)

@vlj Looking at https://github.com/HoTT/HoTT/issues/1048 I don't think it's totally immediate to mix HoTT and ssreflect

hmm yes seems non trivial indeed

Is there a definition of a factorisation system in HoTT lib ? I was looking for a definition of "factor through" but I didn't find one

Last updated: Jun 14 2024 at 19:02 UTC