would it make sense to port this definition of Set quotients from the Coq lib?

https://github.com/HoTT/HoTT/blob/master/theories/hit/quotient.v

The one in old/ makes use of spheres which seems overkill?

https://github.com/HoTT/HoTT-Agda/blob/master/core/lib/Base.agda#L79

J and J' are duplicates

I'm seeing some weird behavior with the current HoTT-Agda library in Agda 2.5.1.1: frequently when I want to compose two complicated paths, Agda is unwilling to parse the path-composition operator infix. It says complains something like

Don't know how to parse
(blah1)
∙ (blah2)
Could mean any one of
((blah1)
 ∙)
(blah2)
_∙_
(blah1)
(blah2)
Operators used in the grammar:
  ∙ (infixr operator, level 80) [_∙_ (/home/shulman/hott/agda/core/lib/PathGroupoid.agda:18,3-6)]
(the treatment of operators was changed in Agda 2.5.1, so code that
used to parse may have to be changed)

Here (blah1) and (blah2) are simple function applications, not mixfix operations, and both enclosed in parentheses, so I don't see what the ambiguity could possibly be. I haven't managed to isolate a MWE, but I wonder whether anyone else is seeing this? Is there an easy solution?

Agda 2.3.4 will introduce changes incompatible with the previous version. I am currently using the developer-version Agda so I put all my recent commits in the branch agda-2.3.4. Any thought?

There are a lot of new files that currently don't get included into index.agda. As a result, the GitHub pages don't display them, and they don't get built when you built index.agda.

This should change, but I don't know which files are safe to include right now. (I'm having some trouble building Agda 2.4.0.1 on my machine, so I can't check for myself.)

I get a lot of confusing yellow highlighting when using HoTT-Agda, which I initially ascribed to inability on my part, but have now reduced to a simple example which has left me just as confused, yet not so assured of my guilt:

https://gist.github.com/aerskine/7962608

When I load this file with Agda 2.3.2.1 the S m == S n term is highlighted yellow, with missing metadata as indicated in the comments.

However, upon commenting out the import statements and replacing with the cut / pasted code from HoTT-Agda the problem vanishes.

Why doesn't lib/types/Nat export S-injective? It's a useful fact.

Let's start a new issue to continue the discussion in Issue #4. Should we rename or merge branches (now)? The issue is that the new development is in the branch 2.0 while the old one is master, which can be confusing, and the porting is not done either.

Agda 2.5.4 will introduce --caching which would hopefully speed up the interactive mode. The down side is that this is probably not backward-compatible.

to what I can see, this library seems in a frozen state. however, for education purposes, I think it will be beneficial if there is an artifact, in a form of docker image or even a VM. Thus, people in the future could just run that VM without having to work with a more and more out-of-date Agda configuration.

• theorems/groups/KernelImage.agda needs to be rewritten due to agda/agda#2979

For many years, there have not been any active developments in this repository. All significant contributors to this repository (me included) have moved on to similar-but-different theories (e.g., https://github.com/RedPRL/cooltt and https://github.com/agda/cubical) or even different careers. Even without adding new theorems, updating the current codebase to match the latest development of Agda would still take significant efforts, and more importantly, I do not expect that any new development would be based on this repository.

At this point, it seems I (the only active benevolent dictator) should archive this repository to reflect the reality. I can make some final changes to address a few concerns (e.g., where to find a working Agda 2.5.3), but all other issues will be effectively closed after the archival. I plan to execute the archiving in about one month (around 2021/09/01).

Thanks to all the people who have starred or have even been watching this repository over the years. My Ph.D. thesis was based on this repository and I had a strong emotional attachment. However, actively maintaining this repository is no longer an option for me.

Here are the people whose contributions are above some threshold: @guillaumebrunerie @ecavallo @timjb @ericfinster @jespercockx @sattlerc @ystael @mikeshulman I am tagging them in case I made a misjudgment or abused my ************.

The upcoming Agda 4.3 no longer has a default fixity/precedence for operators and syntax (which was infix 20 and infix -666, respectively, I believe). In order to make the current code compile we need to put in many fixity/precedence declarations. I would like to take this opportunity to propose the following general rules for precedence:

1. Separators _$_ and arrows: 0
2. Layout combinators (equational reasoning): 10-15
3. Equalities, equivalences: 30
4. Other relations, operators with line-level separators: 40
5. Constructors (for example _,_): 60
6. Binary operators (including type formers like _×_): 80
7. Prefix operators: 100
8. Postfix operators: 120

Any suggestions or comments?

Agda 2.5.x introduced various changes that break the current codebase.

https://github.com/agda/agda/blob/master/CHANGELOG

This issue is to remind us that cohomology.MayerVietorisExact has been broken since we adopted the commuting squares.

Hi,

I get the following type error while checking lib/types/Flattening.agda:

HoTT-Agda/lib/types/Flattening.agda:57,21-37
W !=< (a : A) → _P_105 A B f g C D (cc a) of type Set (lmax j i)
when checking that the expression FlattenCurried.f has type
(w : W) → P w → Wt

I am using Agda version 2.4.2.

Hello!
(disclamer: I'm new to both HoTT and Agda)

I use current (git) version of Agda (Agda version 2.6.0-dc58db0) and HoTT (commit 831dcfc), both pulled 1st July

When I try to compile the library itself it gives warning:

/home/wojciech/Kod/HoTT-Agda/core/lib/Base.agda:70,1-25
Builtin REFL does no longer exist. It is now bound by BUILTIN
EQUALITY
when checking the pragma BUILTIN REFL idp

It's following piece of code:

infix 30 _==_
data _==_ {i} {A : Type i} (a : A) : A → Type i where
  idp : a == a

Path = _==_

{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL idp #-}

Simply commenting out the BUILTIN REFL line fixes the problem.

Last changes to these lines are from 2013. Has anyone had similar issue and knows how to fix it?

See comment f62afb0#r31023192

I think providing a Bool defined as GADT and provide conversion to ⊤ ⊔ ⊤ will be better.

• Builtin REFL should be removed. #28.
• Update the document about the minimum Agda version.

Raised in PR #29.

Experience shows that, at least for homotopy groups, ⊙Ω^ (S n) X should be ⊙Ω^ n (⊙Ω X), not ⊙Ω (⊙Ω^ n X).

HITs have changed to use the REWRITE rules for computation and have become much simpler, so I think the README should reflect this.

Building with agda 2.6.0-d6640d6:

HoTT-Agda/core/lib/NType.agda:156,7-157,47
Instance declarations with explicit arguments are never considered
by instance search, so making =-preserves-level into an instance
has no effect.

↓-='-in takes a path (u ∙ ap g p) == (ap f p ∙' v) and turns it into a dependent path u == v [ (λ x → f x == g x) ↓ p ]. Is there a reason why the left side of the first path uses ∙ and the right side uses ∙'? The other similar lemmas in lib.types.Paths have ∙' on the left and ∙ on the right, which would make more sense to me, since then path induction on p reduces both equalities to u == v for a simpler proof.

(This came up because I want to prove something about a path α : (u ∙ ap g p) == (ap f p ∙' v) and would have a much easier time if I could do induction on α after inducting on p.)

Self-explanatory, I think. I can submit a PR but it'd be a very small change.