[Agda] another level problem

[Jason -Zhong Sheng- Hu]

I find it's very strange that you can write equalities between universe levels, as it sounds to me Level should live in some metalevel. Why I in cubical agda lives in Set omega but Level only lives in Set?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Siek, Jeremy <jsiek at indiana.edu>
Sent: May 20, 2021 10:32 AM
To: Agda List <agda at lists.chalmers.se>
Subject: Re: [Agda] another level problem

Chuckle... and just minutes later I find a solution:

⊔-cong : ∀{a b c d : Level} → (a ≡ b) → (c ≡ d) → a ⊔ c ≡ b ⊔ d
⊔-cong refl refl = refl

EQ : ∀ {ℓᵛ₁ ℓᵛ₂ ℓᶜ₁ ℓᶜ₂ : Level} → (ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁) → (ℓᵛ₂ ⊔ ℓᶜ₂ ≡ ℓᶜ₂) → (ℓᵛ₁ ⊔ ℓᵛ₂ ⊔ ℓᶜ₁ ⊔ ℓᶜ₂ ≡ ℓᶜ₁ ⊔ ℓᶜ₂)
EQ eq1 eq2 = ⊔-cong eq1 eq2

Cheers,
Jeremy

________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Siek, Jeremy <jsiek at indiana.edu>
Sent: Thursday, May 20, 2021 10:16 AM
To: Agda List <agda at lists.chalmers.se>
Subject: [Agda] another level problem

I'd like to prove:

EQ : ∀ {ℓᵛ₁ ℓᵛ₂ ℓᶜ₁ ℓᶜ₂ : Level} → (ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁) → (ℓᵛ₂ ⊔ ℓᶜ₂ ≡ ℓᶜ₂) → (ℓᵛ₁ ⊔ ℓᵛ₂ ⊔ ℓᶜ₁ ⊔ ℓᶜ₂ ≡ ℓᶜ₁ ⊔ ℓᶜ₂)
EQ eq1 eq2 = ?

From earlier threads it sounds like reasoning about equality of levels is mostly automated
in Agda.

So my question is  how to use assumptions such as ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁?

Cheers,
Jeremy


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210520/df29c0c3/attachment.html>