# Why does Agda use Set instead of Type?

In the 'Hello world' example in Agda — Agda 2.6.5 documentation, it straightforwardly uses Set as follows:

‘Hello world’ in Agda — Agda 2.6.5 documentation

data Greeting : Set where
hello : Greeting

greet : Greeting
greet = hello


I understand Type to be similar to, but distinct from, Set. So, why does Agda use Set? From what I understand, Type Theory emerged to resolve Russell's paradox (the paradox of sets), so it's puzzling to use Set. This is just my perception, but I believe that Proof Assistants Languages prove by Type.

around 15 minutes and 22 seconds into the following video:

Agda Lecture 1: Introduction to Agda, dependent types and functions -- HoTTEST Summer School 2022

They forcefully (?) equate Type = Set. However, it was also mentioned that Set might not typically be used. (I am not good at English. Maybe there was an explanation in the video, but I could not discover it)

• I don't know enough of the history to answe on thst, but I always got the impression it's a historical thing to try to make it look more like conventional math, and the Type/Set distinction in HoTT came later Commented Jul 14 at 6:46
• Are you asking about the name (which is ultimately an arbitrary string of symbols that can be changed easily) or the rules associated with Type and Set (which determines how these type theories work)?
– Trebor
Commented Jul 14 at 17:23
• @Trebor I do not have a detailed understanding of either Type or Set (that's why I started learning about them). I only know that there are multiple types of Set, such as ZF and ZFC (though I do not understand them). I heard that Type and Set are separate (as mentioned in Russell's Paradox), but Set also appear in Agda, which confuses me about how to think about them. I asked the question to organize my understanding. Commented Jul 15 at 0:00

• Use --no-import-sorts (at the command line, in your agda-lib file, or in an OPTIONS pragma) and open import Agda.Primitive renaming (Set to Type ; Setω to Typeω). If you use cubical or 1lab then the prelude does this for you. Commented Jul 14 at 10:27