[Agda] another level problem

[Siek, Jeremy]

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/a5f6b459/attachment.html>