Zulip Chat Archive

Stream: general

Topic: Arend — HoTT ITP


view this post on Zulip Johan Commelin (Aug 07 2019 at 06:14):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2019 at 06:58):

Of course I can't say anything about speed.

view this post on Zulip Johan Commelin (Aug 07 2019 at 06:59):

Universes are cumulative

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:00):

It's HoTT, so it has transport

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:01):

What!! And \Prop is even impredicative.

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:01):

Is this thing even consistent?

view this post on Zulip Andrew Ashworth (Aug 07 2019 at 07:05):

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

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:06):

What does "large elimination" mean?

view this post on Zulip Andrew Ashworth (Aug 07 2019 at 07:09):

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

view this post on Zulip Andrew Ashworth (Aug 07 2019 at 07:10):

there's a section on large elimination in the notes

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:11):

@Andrew Ashworth Thanks, I'll take a look

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Aug 07 2019 at 07:23):

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

view this post on Zulip Johan Commelin (Aug 07 2019 at 07:25):

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

view this post on Zulip Chris Hughes (Aug 07 2019 at 07:27):

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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Aug 07 2019 at 07:31):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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?)

view this post on Zulip Johan Commelin (Sep 07 2019 at 04:46):

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

view this post on Zulip 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.

view this post on Zulip 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: May 14 2021 at 21:11 UTC