Tesla Zhang‮

Can you try Agda 2.5.4.2？

> The hott-core library works without modification as in 2.6.0. ``` ~/git-repos/FormalVerification/HoTT-Agda λ> agda --version Agda version 2.6.0-a40792b ~/git-repos/FormalVerification/HoTT-Agda λ> agda core/HoTT.agda Checking HoTT (core/HoTT.agda). Checking lib.Basics (core/lib/Basics.agda). Checking lib.Base...

> > > > @ice1000 Sorry, I forgot I already committed [63972b7](https://github.com/HoTT/HoTT-Agda/commit/63972b709fa8ab8df9a581181c43b6a261b9988d) to make `core/HoTT.agda` type check on my local branch. Also, the termination checker of `2.6.0-ac38171` seems to reject...

Is https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf (sec 3.2.4) a formalization of this work?

@Saizan is there any update on the cubicalagda2.pdf thing? Is it published now or is there an updated version?

> spring span Did you mean string span?

Can we have the `com.fifesoft:rsyntaxtextarea-antlr4:${version}` thing as a third-party library?

@imkiva We can just define the syntax better to make these code parse

@imkiva For example, we can make a "definition without body" a type error instead of a parse error

> > @imkiva For example, we can make a "definition without body" a type error instead of a parse error > > This sounds very unlike a type error It...