New to HoTTLean

Stream: new members

[Pesara Amarasekera]

Hey there, I'm learning HoTT and using Lean to work on HoTTLean. I'm trying to clarify some definitions in an Issue I'm working on. @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 I can see the definition of set univalence in hott0.lean:

hott0
  /-- The univalence axiom for sets. See HoTT book, Axiom 2.10.3. -/
  axiom setUv₀₀ {A B : Type} (A_set : isSet₀ A) (B_set : isSet₀ B) :
    isEquiv₁₀ (@Identity.toEquiv₀₀ A B)

But where is the definition for set-data?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hi @Pesara Amarasekera ! I am not following the question, apologies. What is 'set-data'? Which definition are you missing (is it in the HoTT book)?

I should also make a general disclaimer: HoTTLean is a very early prototype. You will run into missing functionality and performance issues all over the place. If you are just interested in learning HoTT, consider also looking into Ground Zero, or libraries in other provers such as the 1lab.

[Pesara Amarasekera]

Hi @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 , I meant as in issue #165
Prove that equivalent magmas consisting of set-data are equal using set-univalencein test/hott0.lean`.

I got the magma now, interms of a sigma type in here

So I'm trying to clarify what set-data is, I'm assuming I'm supposed to use isSet_0 but not sure...

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Sorry, I should have remembered my own ambiguous wording! I updated the description now: what is meant is a magma where the underlying type A has isSet A.

Pesara Amarasekera said:

interms of a sigma type in here

The link is broken.

[Pesara Amarasekera]

Thanks! let me fix the link here.
and to post the url
https://github.com/PradCoder/HoTTLean/commit/abbbaf75411f49c7b4176377d232ef266557c6c8

[Pesara Amarasekera]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

Sorry, I should have remembered my own ambiguous wording! I updated the description now: what is meant is a magma where the underlying type A has isSet A.

Pesara Amarasekera said:

interms of a sigma type in here

The link is broken.

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 just wondering where did you guys define path-induction, I tried searching the repo for the keyword, and I didn't get a match.

Also I started working on Hedberg's theorem, as an experiment... wondering if that would be useful.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Path induction is the elimination principle for identity types. In HoTT0 that's Identity.rec.

Hedberg's theorem would be useful, but I'm not sure it can be stated right now: there are no inductive types in HoTTLean at the moment, and no Booleans either (using which one could form binary sum types). You could add the Booleans using axioms, I suppose.

[Pesara Amarasekera]

(deleted)