[Agda] another level problem

[András Kovács]

Making Level a first-class type, and putting it in the smallest universe,
is OK: https://arxiv.org/abs/2103.00223

Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com> ezt írta (időpont: 2021.
máj. 20., Cs, 18:46):

> 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/ <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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210520/929e3a36/attachment.html>