<div dir="ltr">Making Level a first-class type, and putting it in the smallest universe, is OK: <a href="https://arxiv.org/abs/2103.00223">https://arxiv.org/abs/2103.00223</a> </div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Jason -Zhong Sheng- Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> ezt írta (időpont: 2021. máj. 20., Cs, 18:46):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">




<div dir="ltr">
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0);background-color:rgb(255,255,255)">
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?<br>
</div>
<div>
<div style="font-family:Calibri,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div id="gmail-m_-305029333776271965Signature">
<div>
<div></div>
<div id="gmail-m_-305029333776271965divtagdefaultwrapper" dir="ltr" style="font-size:12pt;color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size:12pt;color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size:12pt;color:rgb(0,0,0);font-family:Calibri,Arial,Helvetica,sans-serif">
<font size="3"><b><a href="https://hustmphrrr.github.io/" target="_blank">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:"trebuchet ms",sans-serif"><b><a></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="gmail-m_-305029333776271965appendonsend"></div>
<hr style="display:inline-block;width:98%">
<div id="gmail-m_-305029333776271965divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Siek, Jeremy <<a href="mailto:jsiek@indiana.edu" target="_blank">jsiek@indiana.edu</a>><br>
<b>Sent:</b> May 20, 2021 10:32 AM<br>
<b>To:</b> Agda List <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject:</b> Re: [Agda] another level problem</font>
<div> </div>
</div>

<div dir="ltr">
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Chuckle... and just minutes later I find a solution:</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
⊔-cong : ∀{a b c d : Level} → (a ≡ b) → (c ≡ d) → a ⊔ c ≡ b ⊔ d
<div>⊔-cong refl refl = refl</div>
<div><br>
</div>
<div>EQ : ∀ {ℓᵛ₁ ℓᵛ₂ ℓᶜ₁ ℓᶜ₂ : Level} → (ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁) → (ℓᵛ₂ ⊔ ℓᶜ₂ ≡ ℓᶜ₂) → (ℓᵛ₁ ⊔ ℓᵛ₂ ⊔ ℓᶜ₁ ⊔ ℓᶜ₂ ≡ ℓᶜ₁ ⊔ ℓᶜ₂)</div>
EQ eq1 eq2 = ⊔-cong eq1 eq2</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Cheers,</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
Jeremy</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div id="gmail-m_-305029333776271965x_appendonsend"></div>
<hr style="display:inline-block;width:98%">
<div id="gmail-m_-305029333776271965x_divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Siek, Jeremy <<a href="mailto:jsiek@indiana.edu" target="_blank">jsiek@indiana.edu</a>><br>
<b>Sent:</b> Thursday, May 20, 2021 10:16 AM<br>
<b>To:</b> Agda List <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject:</b> [Agda] another level problem</font>
<div> </div>
</div>

<div dir="ltr">
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
I'd like to prove:<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
EQ : ∀ {ℓᵛ₁ ℓᵛ₂ ℓᶜ₁ ℓᶜ₂ : Level} → (ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁) → (ℓᵛ₂ ⊔ ℓᶜ₂ ≡ ℓᶜ₂) → (ℓᵛ₁ ⊔ ℓᵛ₂ ⊔ ℓᶜ₁ ⊔ ℓᶜ₂ ≡ ℓᶜ₁ ⊔ ℓᶜ₂)<br>
<span>EQ eq1 eq2 = ?</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span><br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span>From earlier threads it sounds like reasoning about equality of levels is mostly automated</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span>in Agda.</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span><br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span>So my question is  how to use assumptions such as ℓᵛ₁ ⊔ ℓᶜ₁ ≡ ℓᶜ₁?</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span><br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span>Cheers,</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<span>Jeremy<br>
</span></div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Arial,Helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)">
<br>
</div>
</div>
</div>
</div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>