Proof assistant test: structure identity principle for magmas

[Vtec234]

Prove that equivalent magmas consisting of set-data (meaning magmas $(A,A×A→A)$ s.t. the underlying type $A$ is a set) are equal using set-univalence in test/hott0.lean.

[PradCoder]

Can I claim this issue? I'm new here.

[Vtec234]

Feel free @PradCoder! Note that the proof assistant is a very minimal prototype. E.g. you can't define magmas as a structure: you must instead use a def and Sigma types directly. If you run into issues, please report them here.

[PradCoder]

Hey, @Vtec234, I'm still working on this part (while learning HoTT from HoTTest Summer School Repo, So I got some thing to build, I tried to declare the magma type as found in the univalent foundations book

Page 33 of Univalent Foundations

Would I only need to modify the hott0.lean, as I'm writing a test for Synthlean no? I put them in my fork under branch magma type here.

I'm new to lean and picking it up as I go too, so help is appreciated. And let me know if you want any clarifications.

[Vtec234]

Would I only need to modify the hott0.lean, as I'm writing a test for Synthlean no?

That sounds right. At some point we will move HoTT0 code out of test/ and into its own folder, but for now it's right. Btw, the type hott0 def magma (A : Type) : Type := A → A → A you defined is the type of "magmas on A". The type of all magmas would be the corresponding Sigma type.

[PradCoder]

Is the definition of the Sigma type Σ given in HoTTLean or is it given somewhere else, I'm getting that it belongs in the file NotationExtra.lean in ~/.elan/toolchains/..., I should be able to use the internal Sigma type definition without any conflicts no?

So I tried using hott0 def magma : Type := Σ (A : Type), A → A → A to define the Sigma Type for all magmas, which gives the following error

Application type mismatch: The argument
  fun A ↦ A → A → A
has type
  Type → Type
but is expected to have type
  ?m.1 → Type
in the application
  (A : Type) × (A → A → A)Lean 4

I'm not entirely sure how to understand that

[Vtec234]

The problem is that that's a Type 1: hott0 def magma : Type 1 := Σ (A : Type), A → A → A. Btw, for questions that have more to do with learning Lean than implementation of HoTTLean specifically, I would encourage you to register on the Lean Zulip (if you haven't already) and ask questions on the #new members stream. Feel free to tag me (Wojciech Nawrocki) if it's related to HoTTLean.

[PradCoder]

Hey, so I almost have this working... Just trying to figure out how to resolve my sorry s I find that I can't also use theorem in hott0 as well, so everything is in def. Progress here.

Not being able to use let (I couldn't get def to work with it) felt like I was obfuscating stuff, but that was the only way I could type check

[PradCoder]

@Vtec234 so it seems I have pretty much everything. But the type checker keeps timing out. Progress here. I can keep refining stuff here (remove certain axioms that might be redundant)... but just wondering how feasible that might be.

[Vtec234]

Nice!

• It looks like you are still working off my typo'd definition of isProp 😬 Please make sure to apply the fix in 3456a23.
• Yes, timeouts are a known issue. The only partial salve until we fix that is to move parts of the definition that has grown bigger out into a new definition, and hopefully the two smaller definitions don't time out.

[PradCoder]

So @Vtec234 I ran it overnight, I think 5hrs or so (I went from fifty-thousand heartbeats to five-hundred-million) and it type checked... I'm going to clean it up, and ask for code review, unless it should be that I should optimize to keep it at the regular rate

set_option maxHeartbeats 500000000

-- Seems to be a problem, maybe try specifying which path to take
hott0 def magma_carrier_eq
    (M N : magma)
    (M_set : isSet₀ M.carrier)
    (N_set : isSet₀ N.carrier)
    (e : magma_equiv M N)
    : Identity M.carrier N.carrier := -- sorry
  (setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩

-- Strategy Show any two operations on M, or N are the same under univalence
-- Try a simpler intermediate definition
hott0 def transported_op
    (M N : magma)
    (M_set : isSet₀ M.carrier)
    (N_set : isSet₀ N.carrier)
    (e : magma_equiv M N)
    : N.carrier → N.carrier → N.carrier :=
  @Identity.rec Type M.carrier (fun X _ => X → X → X)
    M.op N.carrier ((setUv₀₀ M_set N_set).1 ⟨e.1, e.2.1⟩)

-- TODO : Pointwise Equality SUUUCKS
-- Implement transported-op the way that was done in Agda
-- Consider Equiv-elim

-- Univalence axiom doesn't specify, but asserts existence of a path.
set_option diagnostics true

hott0 def subexpr
    (M N : magma)
    (M_set : isSet₀ M.carrier)
    (N_set : isSet₀ N.carrier)
    (e : magma_equiv M N)
    (x y : N.carrier)
    :=
    ((e.2.2 (e.2.1.1 x) (e.2.1.1 y)).trans₀
      (ap₂ N.op
        (equiv_retraction M_set N_set e.1 e.2.1 x)
        (equiv_retraction M_set N_set e.1 e.2.1 y)))


hott0 def magma_op_eq_pointwise
    (M N : magma)
    (M_set : isSet₀ M.carrier)
    (N_set : isSet₀ N.carrier)
    (e : magma_equiv M N)
    (x y : N.carrier)
    : Identity (transported_op M N M_set N_set e x y) (N.op x y) :=
  --  sorry -- this keeps timing out
  (transport_op M_set N_set e.1 e.2.1 M.op x y).trans₀
    (subexpr M N M_set N_set e x y)




-- Charactarize Path Spaces using Identity Types
-- Unfiolding is crazy

[awodey]

5 hours!