Ramkumar Ramachandra (Jun 02 2020 at 11:04): 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
Bas Spitters (Jun 02 2020 at 11:26):You may have better luck at the HoTT zulip
Ramkumar Ramachandra (Jun 02 2020 at 11:28):Hey, could you link me to it?
Bas Spitters (Jun 02 2020 at 11:32): 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.
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.
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
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.
vlj (Jun 03 2020 at 21:33):ok
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.
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).
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.
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)
vlj (Jun 04 2020 at 18:12):Thanks for the info !
vlj (Jun 04 2020 at 18:13):Btw is it expected that coq-hott does not install in user contrib when installed via opam ?
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)
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
vlj (Jun 04 2020 at 19:21):but with opam it should be nicely handled ?
vlj (Jun 04 2020 at 19:21):it happens on 2 different machines
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
Gaëtan Gilbert (Jun 04 2020 at 19:26):I don't know if opam installs the hoq* in your path
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
vlj (Jun 04 2020 at 19:28):ho I though it was vanilla coq
vlj (Jun 04 2020 at 19:29):indeed there is a hoqtop in the bin/ of opam
vlj (Jun 04 2020 at 19:29):thanks !
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.
Ramkumar Ramachandra (Jun 05 2020 at 06:12):@Kenji Maillard IIUC, a patched version of coq is unnecessary.
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.
Assia Mahboubi (Jun 05 2020 at 14:46):There are other examples in commutative algebra, for constructions related to field extensions.
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
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 ?)
Gaëtan Gilbert (Jun 08 2020 at 08:20):I don't know about hott's install_coq stuff
Gaëtan Gilbert (Jun 08 2020 at 08:22):maybe it just doesn't build coqide
Ali Caglayan (Jun 08 2020 at 16:30):@vlj How are you running hoqide?
Ali Caglayan (Jun 08 2020 at 16:31):And can you give me the output of ./configure?
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.
vlj (Jun 08 2020 at 17:34):@Ali Caglayan I'm trying to launch ./hoqide
vlj (Jun 08 2020 at 17:36):and here is the ouput of configure : https://gist.github.com/vlj/738767900150266de4169a2895c00c83
Ali Caglayan (Jun 08 2020 at 17:37):Ah so configure is finding your opam install
Ali Caglayan (Jun 08 2020 at 17:37):Can you try ./configure COQBIN="pwd/coq-HoTT/bin"
Ali Caglayan (Jun 08 2020 at 17:37):This should be the "custom" version of coq that the HoTT library uses
Ali Caglayan (Jun 08 2020 at 17:37): ./configure COQBIN="`pwd`/coq-HoTT/bin"
now the output is : https://gist.github.com/vlj/db1f93e50652e7244f72f37ba467646b
vlj (Jun 08 2020 at 17:39):can I do make directly or do I need to make clean before ?
Ali Caglayan (Jun 08 2020 at 17:40):Do a make clean to be sure
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
vlj (Jun 08 2020 at 17:41):ok
vlj (Jun 08 2020 at 17:41):btw the configure log tells that configure: Could not find coqide, will not make hoqide
Ali Caglayan (Jun 08 2020 at 17:42):Ah ok, so it looks like the local version of coq wasn't installed
vlj (Jun 08 2020 at 17:42):nvm
Ali Caglayan (Jun 08 2020 at 17:42):Did you run etc/install_coq.sh?
vlj (Jun 08 2020 at 17:42):yes but I think I erased it with make distclean
vlj (Jun 08 2020 at 17:43):(I'm rebuilding it )
Ali Caglayan (Jun 08 2020 at 17:44):It will take a bit of time unfortunately
Ali Caglayan (Jun 08 2020 at 17:44):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
vlj (Jun 08 2020 at 17:53):install_coq.sh will compile coqide ?
Ali Caglayan (Jun 08 2020 at 17:59):It should do
Ali Caglayan (Jun 08 2020 at 17:59):But it will be a local version that is not installed
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
Ali Caglayan (Jun 08 2020 at 18:00):After you finish running make you should be able to run hoqide
vlj (Jun 08 2020 at 18:26):yes ! this time it found a coqide in coq-HoTT
Ali Caglayan (Jun 08 2020 at 18:34):@vlj Is that all working then?
vlj (Jun 08 2020 at 18:35):hocq is still building
vlj (Jun 08 2020 at 18:36):but the configure told that it found a coqide in the right location
vlj (Jun 08 2020 at 18:57):it works ! I have the ide
vlj (Jun 08 2020 at 18:57):launch with hoqide
vlj (Jun 08 2020 at 20:33):thanks a lot for the help!
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 ~?
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).
Paolo Giarrusso (Jun 12 2020 at 10:50):@Ramkumar Ramachandra very roughly, under double negation you get classical logic
Paolo Giarrusso (Jun 12 2020 at 10:51):for a more accurate statement, see https://en.wikipedia.org/wiki/Double-negation_translation
Ramkumar Ramachandra (Jun 12 2020 at 10:53):Cool, thanks :)
Bas Spitters (Jun 12 2020 at 13:51):This of course is a modality in HoTT...
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.
Adding a Local Open Scope morphism_scope allows me to use "o" but I don't know how to get the "-->"
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).
vlj (Jun 13 2020 at 14:02):Yes usong github search the only usage of the notation is in comments
vlj (Jun 13 2020 at 14:03):I'm not sure why this notation is introduced, maybe a leftover from a code cleaning attemp
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
vlj (Jun 13 2020 at 14:07):(I have 2 coqs, a vanilla one and the one from coq hott)
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
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)
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
vlj (Jun 13 2020 at 20:17):hmm yes seems non trivial indeed
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: Oct 13 2024 at 01:02 UTC