Re: #397 Modeling set theory

[WorldSEnder]

Defines a higher inductive type V, that the HoTT book calls "cumulative hierarchy" §10.5, modeling "ZF without powersets".

[WorldSEnder]

For future me: build fails cause TERMINATING is not compatible with --safe.

[mortberg]

Sorry for the slow reply, I've been really swamped lately. Some quick comments for now:

1. All problems with termination has been resolved now right?
2. Some lines are very long. Please make a pass over the files and shorten them to <100 characters.
3. There is some conflict with Cubical/Functions/Embedding.agda. Can you fix?

Please let me know when you've done 2-3 and I'll review everything properly.

[WorldSEnder]

1. Correct, all modules should now be marked as safe.
2. Did a pass over the 3 main files I added. A lot of other files show up when I do rg -l '.{101,}' (which searches for all files with lines longer than 100 characters), it might be worth at some point to include a test in the CI that this list comes out empty?
   Do you have any advice how to configure emacs to mark violations? When I try with whitespace-mode, it doesn't mark the lines unless I disable agda2-mode and switch to text-mode which is a bit annoying. It does mark trailing whitespace though, even in agda-mode.
3. Done, looking forward to the review.

[mortberg]

2. Did a pass over the 3 main files I added. A lot of other files show up when I do `rg -l '.{101,}'` (which searches for all files with lines longer than 100 characters), it might be worth at some point to include a test in the CI that this list comes out empty?
   Do you have any advice how to configure emacs to mark violations? When I try with whitespace-mode, it doesn't mark the lines unless I disable agda2-mode and switch to text-mode which is a bit annoying. It _does_ mark _trailing_ whitespace though, even in agda-mode.

Good idea with adding a test to the CI! Can you do it in a separate PR?

I don't know how to configure emacs to mark it. Maybe someone else knows?

[mortberg]

Very nice and interesting stuff!

How does the formalization compare to the Coq code?

Is there some test you can try which actually involves this HIT and univalence computing? Like constructing some concrete sets and taking their union or something.

[WorldSEnder]

Sorry for the long response time. Regarding computational behaviour, performance is currently poor. There is some insight to be gained though, consider:

MonicDataF : Type (ℓ-suc ℓ) → Type (ℓ-suc ℓ)
MonicDataF {ℓ} T = Embedding T ℓ

V-fixpoint : V ℓ ≃ MonicDataF (V ℓ)
V-fixpoint {ℓ} =
  V ℓ ≃⟨ invEquiv (Σ-contractSnd λ a → inhProp→isContr (V-repr a) (isPropMonicPresentation a)) ⟩
  (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃⟨ boringswap ⟩
  (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix)) ≃⟨ Σ-contractSnd (λ _ → isContrSingl _) ⟩
  MonicDataF (V ℓ) ■ where
  boringswap : (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃ (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix))
  boringswap = isoToEquiv (iso
    (λ (a , X , ix , emb , p) → (X , ix , emb) , a , sym p)
    (λ ((X , ix , emb) , a , p) → a , X , ix , emb , sym p)
    (λ _ → refl)
    λ _ → refl)

so V ℓ should be the least fix point of MonicDataF! The reason V can't be defined that way is that MonicDataF is not strictly positive (due to isEmbedding contained therein). Can we talk about this tomorrow on Zulip @ agdameetup?

[mortberg]

Sorry for the long response time. Regarding computational behaviour, performance is currently poor. There is some insight to be gained though, consider:

MonicDataF : Type (ℓ-suc ℓ) → Type (ℓ-suc ℓ)
MonicDataF {ℓ} T = Embedding T ℓ

V-fixpoint : V ℓ ≃ MonicDataF (V ℓ)
V-fixpoint {ℓ} =
  V ℓ ≃⟨ invEquiv (Σ-contractSnd λ a → inhProp→isContr (V-repr a) (isPropMonicPresentation a)) ⟩
  (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃⟨ boringswap ⟩
  (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix)) ≃⟨ Σ-contractSnd (λ _ → isContrSingl _) ⟩
  MonicDataF (V ℓ) ■ where
  boringswap : (Σ[ a ∈ V ℓ ] MonicPresentation a) ≃ (Σ[ (X , ix , _) ∈ MonicDataF (V ℓ) ] singl (sett X ix))
  boringswap = isoToEquiv (iso
    (λ (a , X , ix , emb , p) → (X , ix , emb) , a , sym p)
    (λ ((X , ix , emb) , a , p) → a , X , ix , emb , sym p)
    (λ _ → refl)
    λ _ → refl)

so V ℓ should be the least fix point of MonicDataF! The reason V can't be defined that way is that MonicDataF is not strictly positive (due to isEmbedding contained therein). Can we talk about this tomorrow on Zulip @ agdameetup?

Sure, feel free to post your question on Zulip whenever you want and we can take the discussion there

[WorldSEnder]

Since it might take a little longer to make this perform well, I could split off the parts of the PR that touch the rest of the library and could be required from other parts and open a separate PR for those only.

[mortberg]

Since it might take a little longer to make this perform well, I could split off the parts of the PR that touch the rest of the library and could be required from other parts and open a separate PR for those only.

Sounds reasonable to me. The more code we can merge into the library from this PR the less hassle you'll have with conflicts.

[mortberg]

What is the plan for this PR? Was it going to be split into smaller parts or was there some problem with it?

[WorldSEnder]

Most of the reusable working parts were in #460. I pushed it onto the long bench because when I wanted to address

Is there some test you can try which actually involves this HIT and univalence computing? Like constructing some concrete sets and taking their union or something.

Even trying small examples, such as

  open InfinitySet

  the1 : V ℓ-zero
  the1 = # 1
  -- asking agda to normalize `the1` already takes a long time on my machine, although
  test : ∥ Bool ∥
  test = do
    prf ← infinity-ax the1 .fst (#-in-ω 1)
    case prf of λ { (⊎.inl _) → ∣ false ∣ ; (⊎.inr _) → ∣ true ∣ }
    where
    open PropMonad
  -- `test` evaluates in a few miliseconds to | true |
  test : 1-ok? ≡ ∣ true ∣
  test = refl

I didn't have the time to properly investigate this or test other approaches. I would update to the newest version of cubical and push this example and small fixes as documentation, but for the most part, the code sits in my freezer :)

[mortberg]

Most of the reusable working parts were in #460. I pushed it onto the long bench because when I wanted to address

Is there some test you can try which actually involves this HIT and univalence computing? Like constructing some concrete sets and taking their union or something.

Even trying small examples, such as

  open InfinitySet

  the1 : V ℓ-zero
  the1 = # 1
  -- asking agda to normalize `the1` already takes a long time on my machine, although
  test : ∥ Bool ∥
  test = do
    prf ← infinity-ax the1 .fst (#-in-ω 1)
    case prf of λ { (⊎.inl _) → ∣ false ∣ ; (⊎.inr _) → ∣ true ∣ }
    where
    open PropMonad
  -- `test` evaluates in a few miliseconds to | true |
  test : 1-ok? ≡ ∣ true ∣
  test = refl

I didn't have the time to properly investigate this or test other approaches. I would update to the newest version of cubical and push this example and small fixes as documentation, but for the most part, the code sits in my freezer :)

Ok, that sounds good! Let me know when you're done and I'll take a look and then we can merge it.

The typechecking of the actual files are not too slow right? It's just normalization of examples that's slow?

[WorldSEnder]

The small example is now included and yes, typechecking works reasonably well, it's just normalization. @mortberg

[mortberg]

Finally merging this if the CI accepts it