Интуиция для различия между eta для функции сверху и пустыми функциями в Agda

Question

В Агде, кажется, невозможно показать ∀ {A : Set} (f : ⊥ → A) → f ≡ λ ().

Однако, казалось бы, похожий термин ∀ {A : Set} (f : ⊤ → A) → f ≡ λ _ → f tt может быть подтвержден refl. Позже он может быть использован для доказательства формы экстенсиональности для ⊤:

ext⊤ : ∀ {A : Set} (f g : ⊤ → A) (H : ∀ x → f x ≡ g x) → f ≡ g

Согласно этот вопрос и ответ , объяснение может быть при рассмотрении разные модели теории типов. Можно ли иметь какую-то интуицию о том, почему одно принято, а другое нет? Разве f ≡ λ () не должно быть какой-то формой закона об Эте?

Answer 1

Обращаю ваше внимание, что первое утверждение пытается доказать уникальность ⊥ → A. Обычно это верно вплоть до изоморфизма.

Полное соответствие было бы между ∀ {A : Set} (f : ⊤ → A) → f ≡ λ _ → f tt и ∀ {A : Set} (f : ⊥ → A) → f ≡ λ _ → f () - выражение для ⊤ создает значение tt, поэтому вы должны построить значение для ⊥.

У Agda нет средств для создания значения ⊥, поэтому () не является допустимым конструктором, это только заполнитель для того, что вы хотите.

Хотя на самом деле это не сопоставление с образцом, вероятно, не вредно видеть использование () в качестве сопоставления с образцом для пустого типа - оно допускается только в позициях сопоставления с образцом.

Это сделано для того, чтобы показать, что сходство является поверхностным, поэтому следует изменить свою интуицию в отношении выражений.

Разве f ≡ λ () не должно быть какой-либо формой закона эта?

Не ясно, что вы получите от этого. Многие вещи могут быть доказаны только с точностью до изоморфизма. Так, например, доказательство уникальности ⊥ → A может соответствовать доказательству уникальности A → ⊤ (а не эта-равенство f и λ _ → f tt). И то и другое выполнимо.

Answer 2

Тип ⊤ имеет правило eta, которое гласит, что любые термины с этим типом по определению равны. Следовательно, f ≡ (λ x → f x) ≡ (λ x → f tt).

⊥ не имеет правила eta в Агде. Если f : ⊥ → A, то мы знаем только, что f ≡ λ x → f x. λ () по существу является синтактическим c сахаром для ⊥-elim, а f не определенно равен ⊥-elim.