Stream: Coq users

Topic: HoTT


view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 11:04):

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

view this post on Zulip Bas Spitters (Jun 02 2020 at 11:26):

You may have better luck at the HoTT zulip

view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 11:28):

Hey, could you link me to it?

view this post on Zulip Bas Spitters (Jun 02 2020 at 11:32):

https://hott.zulipchat.com/

view this post on Zulip vlj (Jun 03 2020 at 18:14):

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.

view this post on Zulip Hugo Herbelin (Jun 03 2020 at 18:51):

@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.

view this post on Zulip vlj (Jun 03 2020 at 19:33):

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

view this post on Zulip Kenji Maillard (Jun 03 2020 at 19:39):

@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.

view this post on Zulip vlj (Jun 03 2020 at 21:33):

ok

view this post on Zulip vlj (Jun 03 2020 at 21:36):

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.

view this post on Zulip Kenji Maillard (Jun 03 2020 at 22:01):

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).

view this post on Zulip Assia Mahboubi (Jun 04 2020 at 13:46):

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.

view this post on Zulip Karl Palmskog (Jun 04 2020 at 14:51):

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)

view this post on Zulip vlj (Jun 04 2020 at 18:12):

Thanks for the info !

view this post on Zulip vlj (Jun 04 2020 at 18:13):

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

view this post on Zulip vlj (Jun 04 2020 at 19:18):

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)

view this post on Zulip vlj (Jun 04 2020 at 19:21):

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

view this post on Zulip vlj (Jun 04 2020 at 19:21):

but with opam it should be nicely handled ?

view this post on Zulip vlj (Jun 04 2020 at 19:21):

it happens on 2 different machines

view this post on Zulip Gaëtan Gilbert (Jun 04 2020 at 19:26):

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

view this post on Zulip Gaëtan Gilbert (Jun 04 2020 at 19:26):

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

view this post on Zulip Kenji Maillard (Jun 04 2020 at 19:27):

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

view this post on Zulip vlj (Jun 04 2020 at 19:28):

ho I though it was vanilla coq

view this post on Zulip vlj (Jun 04 2020 at 19:29):

indeed there is a hoqtop in the bin/ of opam

view this post on Zulip vlj (Jun 04 2020 at 19:29):

thanks !

view this post on Zulip Bas Spitters (Jun 04 2020 at 20:22):

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

view this post on Zulip Ramkumar Ramachandra (Jun 05 2020 at 06:12):

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

view this post on Zulip Assia Mahboubi (Jun 05 2020 at 14:41):

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.

view this post on Zulip Assia Mahboubi (Jun 05 2020 at 14:46):

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

view this post on Zulip vlj (Jun 07 2020 at 20:45):

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

view this post on Zulip Bas Spitters (Jun 08 2020 at 08:12):

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 ?)

view this post on Zulip Gaëtan Gilbert (Jun 08 2020 at 08:20):

I don't know about hott's install_coq stuff

view this post on Zulip Gaëtan Gilbert (Jun 08 2020 at 08:22):

maybe it just doesn't build coqide

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:30):

@vlj How are you running hoqide?

view this post on Zulip Ali Caglayan (Jun 08 2020 at 16:31):

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

view this post on Zulip vlj (Jun 08 2020 at 17:34):

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

view this post on Zulip vlj (Jun 08 2020 at 17:34):

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

view this post on Zulip vlj (Jun 08 2020 at 17:36):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:37):

Ah so configure is finding your opam install

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:37):

Can you try ./configure COQBIN="pwd/coq-HoTT/bin"

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:37):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:37):

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

view this post on Zulip vlj (Jun 08 2020 at 17:39):

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

view this post on Zulip vlj (Jun 08 2020 at 17:39):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:40):

Do a make clean to be sure

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:41):

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

view this post on Zulip vlj (Jun 08 2020 at 17:41):

ok

view this post on Zulip vlj (Jun 08 2020 at 17:41):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:42):

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

view this post on Zulip vlj (Jun 08 2020 at 17:42):

nvm

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:42):

Did you run etc/install_coq.sh?

view this post on Zulip vlj (Jun 08 2020 at 17:42):

yes but I think I erased it with make distclean

view this post on Zulip vlj (Jun 08 2020 at 17:43):

(I'm rebuilding it )

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:44):

It will take a bit of time unfortunately

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:44):

Afterwards, make sure you run

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:45):

You can do make -j n for the last bit if you wish

view this post on Zulip vlj (Jun 08 2020 at 17:53):

install_coq.sh will compile coqide ?

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:59):

It should do

view this post on Zulip Ali Caglayan (Jun 08 2020 at 17:59):

But it will be a local version that is not installed

view this post on Zulip Ali Caglayan (Jun 08 2020 at 18:00):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 18:00):

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

view this post on Zulip vlj (Jun 08 2020 at 18:26):

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

view this post on Zulip Ali Caglayan (Jun 08 2020 at 18:34):

@vlj Is that all working then?

view this post on Zulip vlj (Jun 08 2020 at 18:35):

hocq is still building

view this post on Zulip vlj (Jun 08 2020 at 18:36):

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

view this post on Zulip vlj (Jun 08 2020 at 18:57):

it works ! I have the ide

view this post on Zulip vlj (Jun 08 2020 at 18:57):

launch with hoqide

view this post on Zulip vlj (Jun 08 2020 at 20:33):

thanks a lot for the help!

view this post on Zulip Ramkumar Ramachandra (Jun 09 2020 at 15:48):

Some strangeness here, with respect to precedence of ~ and +. Does anyone (cc: @Hugo Herbelin ) know why the precedence of + is higher than that of ~?

view this post on Zulip Ramkumar Ramachandra (Jun 09 2020 at 15:52):

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).

view this post on Zulip Paolo Giarrusso (Jun 12 2020 at 10:50):

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

view this post on Zulip Paolo Giarrusso (Jun 12 2020 at 10:51):

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

view this post on Zulip Ramkumar Ramachandra (Jun 12 2020 at 10:53):

Cool, thanks :)

view this post on Zulip Bas Spitters (Jun 12 2020 at 13:51):

This of course is a modality in HoTT...

view this post on Zulip vlj (Jun 12 2020 at 22:34):

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.

view this post on Zulip vlj (Jun 12 2020 at 22:35):

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

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 12:47):

@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).

view this post on Zulip vlj (Jun 13 2020 at 14:02):

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

view this post on Zulip vlj (Jun 13 2020 at 14:03):

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

view this post on Zulip vlj (Jun 13 2020 at 14:06):

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

view this post on Zulip vlj (Jun 13 2020 at 14:07):

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

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 14:48):

if you install those Coqs in different opam switches, and use appropriate eval $(opam env) to switch across the two, that should become impossible

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 14:49):

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

view this post on Zulip Kenji Maillard (Jun 13 2020 at 17:10):

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

view this post on Zulip vlj (Jun 13 2020 at 20:17):

hmm yes seems non trivial indeed

view this post on Zulip vlj (Jun 14 2020 at 20:08):

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: Feb 06 2023 at 13:03 UTC