[Agda] Blog post: The Agda's New Sorts

[Martin Escardo]

Thorsten,

I do the following (in a base module):


\begin{code}

open import Agda.Primitive using (_⊔_) renaming (lzero to U₀ ; lsuc to 
_′ ; Level to Universe) public

_̇ : (U : Universe) → _
U ̇ = Set U -- This should be the only use of the Agda keyword 'Set'.

U₁ = U₀ ′
U₂ = U₁ ′

infix  0 _̇

\end{code}

Notice the almost invisible dot superscript. It is invisible on purpose 
(and it almost completely disappears from view when it is followed by 
")" or "}").

For example, we write the following instead of

     Π : ∀ {i j} {X : Set i} (Y : X → Set j) → Set (i ⊔ j)
     Π Y = ∀ x → Y x

\begin{code}

Π : ∀ {U V} {X : U ̇} (Y : X → V ̇) → U ⊔ V ̇
Π Y = ∀ x → Y x


_∘_ : ∀ {U V W} {X : U ̇} {Y : V ̇} {Z : Y → W ̇}
     → Π Z → (f : X → Y) → Π (λ x → Z (f x))
g ∘ f = λ x → g(f x)

\end{code}

The first definition says that X is the universe U and Y is an X-indexed 
family of types in the universe V, and then Π Y lives in the first 
universe after U and V. Then I consistently use U,V,W for universes. (I 
tried the curly versions, but the fonts are not available in all 
installations I use, and I don't know how to get them.)

(Also I avoid "Set" because in univalent mathematics not all elements of 
"Set j" are sets, and curly "U" is (aptly) used in the HoTT book for 
universes.)

Martin



On 15/05/18 19:09, Thorsten Altenkirch wrote:
> Hi jesper,
> 
> I appreciate your efforts to make universes more flexible and maybe 
> capture other notions of universe than the ones given by size. However, 
> I have another issue with the current mechanism (which I actually 
> proposed many years ago). I don't like that all definitions are 
> cluttered with these pesky level annotations. When teaching an 
> introductory course I don't really want to talk about levels but on the 
> other hand I would like to use the definitions from the standard library 
> and not my own simplified versions. However, whenever I show a library 
> definition I have to instruct them to ignore all those levels for the 
> time being.
> 
> Is there a way out of this dilemma? Coq only does fully automatic 
> indexing but there are many situation where this is not what you want. 
> Is there a way to infer levels and automatically add level annotations 
> but be still able to do the explicitly if you want (or need) to?
> 
> Cheers,
> Thorsten
> 
> From: Agda <agda-bounces at lists.chalmers.se 
> <mailto:agda-bounces at lists.chalmers.se>> on behalf of Jesper Cockx 
> <Jesper at sikanda.be <mailto:Jesper at sikanda.be>>
> Date: Friday, 4 May 2018 at 09:45
> To: agda list <agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>>
> Subject: [Agda] Blog post: The Agda's New Sorts
> 
> Hi all,
> 
> Yesterday I posted a blog post on the recent work I did on Agda's 
> handling of sorts. You can read it here: 
> https://jesper.sikanda.be/posts/agdas-new-sorts.html
> 
> Any comments are very welcome here on this list!
> 
> Cheers,
> Jesper
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe