# Zulip Chat Archive

## Stream: general

### Topic: Arend — HoTT ITP

#### Johan Commelin (Aug 07 2019 at 06:14):

https://arend-lang.github.io/2019/07/17/Arend-1.0.0-released.html

#### Johan Commelin (Aug 07 2019 at 06:57):

From my first glimpse it seems they have no bundling issues: https://arend-lang.github.io/about/arend-features#anonymous-extensions

#### Johan Commelin (Aug 07 2019 at 06:58):

Of course I can't say anything about speed.

#### Johan Commelin (Aug 07 2019 at 06:59):

Universes are cumulative

#### Johan Commelin (Aug 07 2019 at 07:00):

It's HoTT, so it has transport

#### Johan Commelin (Aug 07 2019 at 07:01):

What!! And `\Prop`

is even impredicative.

#### Johan Commelin (Aug 07 2019 at 07:01):

Is this thing even consistent?

#### Andrew Ashworth (Aug 07 2019 at 07:05):

You can always pick 2 of: impredicative Prop, large elimination, and excluded middle

#### Johan Commelin (Aug 07 2019 at 07:06):

What does "large elimination" mean?

#### Andrew Ashworth (Aug 07 2019 at 07:09):

https://lean-forward.github.io/logical-verification/2018/41_notes.html

#### Andrew Ashworth (Aug 07 2019 at 07:10):

there's a section on large elimination in the notes

#### Johan Commelin (Aug 07 2019 at 07:11):

The list of editor features (Intellij) also looks quite nice: https://arend-lang.github.io/about/intellij-features

#### Johan Commelin (Aug 07 2019 at 07:11):

@Andrew Ashworth Thanks, I'll take a look

#### Johan Commelin (Aug 07 2019 at 07:17):

As an example of the bundling thing: they have

\class Group \extends CancelMonoid { | inverse : E -> E | inverse-left (x : E) : inverse x * x = ide | inverse-right (x : E) : x * inverse x = ide

This allows you to write `(X : \Type) (Group X)`

or `(X : Group)`

, and these two are defeq. At the same time, they can also write

\instance GroupCategory : Cat Group => subCat (\new Embedding { | f (G : Group) => \new Monoid G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc | isEmb G H => \new Retraction { | sec => Group.equals G H | f_sec => idpe } })

to prove that groups form a category.

There is no distinction between bundled and unbundled objects.

#### Johan Commelin (Aug 07 2019 at 07:22):

@Andrew Ashworth So you gave a pick-2-out-of-3. If I pick impredicative `Prop`

and LEM, then I have to sacrifice large elimination. But do I sacrifice it for `Prop`

, or in general?

#### Chris Hughes (Aug 07 2019 at 07:23):

I think in general would make your theory a bit useless.

#### Johan Commelin (Aug 07 2019 at 07:25):

It seems that Arend sacrifices LEM... which is a pity.

#### Chris Hughes (Aug 07 2019 at 07:27):

I don't understand how large elimination could be consistent.

#### Chris Hughes (Aug 07 2019 at 07:30):

This would give you a way to "choose" a bijection between types, which gives you em, at least in Lean.

#### Chris Hughes (Aug 07 2019 at 07:31):

So this HoTT must be weaker in some sense than Lean without choice

#### Jason Rute (Sep 06 2019 at 22:27):

I've looked into Arend (vs Lean) a bit and here is what I think I've found...

#### Jason Rute (Sep 06 2019 at 22:27):

I think, just like in Lean, `\Prop`

in Arend is impredicative and does *not* allow large elimination. Also, like Lean, the `\Type`

universe levels are predicative and support large elimination. I see nothing inconsistent about LEM (for `\Prop`

) in Arend, especially since LEM (for propositions) is consistent in other HoTT systems.

#### Jason Rute (Sep 06 2019 at 22:27):

Indeed, to me, the foundations for Arend seem very similar to those for Lean, but contain more “levels” of types. An analogy (possibly too simplistic) is that Lean is a logic for propositions (`Prop`

) and sets (`Type`

) while Arend is a logic for propositions (`\Prop`

), sets (`\Set`

), and other higher homotopy spaces/types (`\1-Type`

, `\2-Type`

, …). This allows univalence since the univalence axiom requires that a type universe (except `\Prop`

) not be a set.

#### Jason Rute (Sep 06 2019 at 22:28):

Now, in book HoTT, propositions and sets are defined. (A *proposition* is a type `P`

for which all pairs of elements are equal, and a *set* is a type `A`

for which every `a = a'`

is a proposition). In Arend, however, it seems `\Prop`

and `\Set`

are also built into the type hierarchy. So if `A : \Set`

and `a a' : A`

, then the type of `a = a'`

is Prop, judgmentally. In this way, Arend’s `\Prop`

is similar to Lean’s `Prop`

.

#### Jason Rute (Sep 06 2019 at 22:28):

In Lean, inductively defined propositions are formed through a special `Prop`

-valued induction. Similarly, in Arend they are formed by truncating an inductively defined type to `\Prop`

. So, logical disjunction `\/`

in `\Prop`

would have the same definition as disjoint union `+`

in `\Type`

, except that the former is explicitly truncated to `\Prop`

. This truncation prevents large elimination.

#### Jason Rute (Sep 06 2019 at 22:28):

When it comes to classical reasoning, that is where Lean and Arend/HoTT start to differ is subtle ways (that I don’t completely appreciate yet). HoTT is all about proof relevant reasoning, but proof relevant versions of classical reasoning are not compatible with the univalence axiom. From the Curry-Howard Isomorphism, the analogy of LEM in `Type`

would be `Π α : Type, α + (α -> empty)`

which contradicts univalence, and would be inconsistent in Arend. Instead, Arend/HoTT’s version of LEM replaces `\Type`

with `\Prop`

. In Lean, this is `prop_decidable`

, but using the univalence axiom it is equivalent to the usual propositional LEM `Π p : Prop, p ∨ ¬ p`

). In Lean, the “type-valued LEM” above is provable via Lean’s choice function, which takes a nonempty type and extracts a value. Arend/HoTT can’t have such a strong choice function. Instead, in the Arend/HoTT version of AC, all one can do is say is that if a *set* `A`

is non-empty (proposition) then there exists (proposition) a choice function. Since “exists” here is a proposition, one can’t directly use that choice function for constructions except inside proofs of propositions. (Also, in Arend/HoTT there doesn’t propositionally exist one universal choice function, but instead one for each set-indexed family of non-empty sets.)

#### Jason Rute (Sep 06 2019 at 22:28):

Just like in Lean, in Arend’s version of HoTT, it seems useful to have an impredicative universe `\Prop`

of propositions and predicative universes of other types. (Arend/HoTT also seems to make it easier to go between arbitrary types and `\Prop`

by either proving that a type is a proposition or by truncating it to one.) How one uses `\Prop`

seems to me to be a matter of taste, engineering, and philosophy. Should one lean into constructive, proof relevant mathematics trying to avoid `\Prop`

whenever possible? Or, like Lean, should one embrace classical mathematics and propositions, adding AC (in the HoTT sense) as an axiom (while still getting univalence!). (Or is there a “best of both worlds”, where one uses arbitrary types for constructive, proof-relevant reasoning, and AC for classical reasoning in `\Prop`

and `\Set`

, all within the same system?)

#### Johan Commelin (Sep 07 2019 at 04:46):

@Jason Rute Thanks for this thorough comparison! It only makes it seem more interesting to me!

#### Moses Schönfinkel (Sep 09 2019 at 07:07):

Huh, I had no idea Jetbrains people care about this, given their (apparent) focus on industrial applications.

#### Jason Rute (Sep 09 2019 at 11:11):

They have a research arm, https://research.jetbrains.org . This project is listed under applied math and physics. I guess one could justify this as supporting software verification, but I don’t know how it was sold.

Last updated: Aug 03 2023 at 10:10 UTC