В Agda тип a forall определяется таким образом, что следующие все имеют тип Set1 (где Set1 - тип Set и A имеет тип Set)
Set → A
A → Set
Set → Set
Однако следующее имеет тип Set:
A → A
Я понимаю, что если Set имел тип Set, были бы противоречия, но я не вижу, как, если бы какой-либо из трех терминов выше имел тип Set, у нас были бы противоречия. Могут ли они использоваться для доказательства False? Можно ли их использовать, чтобы показать, что Set : Set?
Ясно, что Set : Set вызовет противоречие, например парадокс Рассела.
Теперь рассмотрим () -> Set, где () - тип единицы . Это, очевидно, изоморфно Set. Поэтому, если () -> Set : Set, то также Set : Set. В самом деле, если для любого живого A мы имели A -> Set : Set, тогда мы могли бы обернуть Set в A -> Set с использованием постоянной функции:
wrap1 : {A : Set} -> Set -> (A -> Set)
wrap1 v = \_ -> v
и при необходимости получить значение
unwrap1 : {A : Set}(anyInhabitant : A) -> (A -> Set) -> Set
unwrap1 anyInhabitant f = f anyInhabitant
Итак, мы могли бы восстановить парадокс Рассела так же, как если бы у нас было Set : Set.
То же самое относится и к Set -> Set, мы можем заключить Set в Set -> Set:
data Void : Set where
unwrap2 : (Set -> Set) -> Set
unwrap2 f = f Void
wrap2 : Set -> (Set -> Set)
wrap2 v = \_ -> v
Здесь мы можем использовать любой тип Set вместо Void.
Я не уверен, как сделать что-то подобное с Set -> A, но интуитивно это кажется еще более проблематичным, чем другие, может быть, кто-то еще узнает.
Я думаю, что лучший способ понять это - рассмотреть, что это такое, как теоретико-множественные множества, в отличие от Agda Set. предположим, что у вас есть A = {a,b,c}. Примером функции f : A → A является множество пар, скажем, f = { (a,a) , (b,b) , (c,c) }, удовлетворяющее некоторым свойствам, которые не имеют значения для этого обсуждения. То есть элементы f - это те же вещи, что элементы A - это просто значения или пары значений, ничего слишком "большие".
Теперь рассмотрим функцию F : A → Set. Это тоже набор пар, но его пары выглядят иначе: F = { (a,A) , (b,Nat) , (c,Bool) } скажет. Первый элемент каждой пары является всего лишь элементом A, поэтому он довольно прост, но второй элемент каждой пары - это Set! То есть, второй элемент сам по себе является "большим". Поэтому A → Set невозможно установить, потому что если бы это было так, то мы могли бы иметь некоторый G : A → Set, который выглядит как G = { (a,G) , ... }. Как только мы сможем это сделать, мы можем получить парадокс Рассела. Поэтому мы говорим A → Set : Set1.
Здесь также рассматривается вопрос о том, должен ли Set → A быть в Set1 вместо Set, потому что функции из Set → A аналогичны функциям в A → Set, за исключением того, что A находятся справа, а Set находятся слева от пар.