Zulip Chat Archive

\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: Dec 20 2023 at 11:08 UTC