Тип сквоша

Шаблон:Без виносок Тип сквоша (пропозиційне обрізання) — тип, який «стискає» або «обрізає» тип до пропозиційної секвенції у гомотопічній теорії типів. Позначається подвійною вертикальною рискою $||\cdot ||$.

Визначення

Для будь-якого терму $a$ типу $A$ існує пропозиційне обрізання $|a|:||A||$, де $|a|$ — образ $a:A$ у $||A||.$ Її можна розглядати як формальну операцію, яка робить рівними усі терми, які належать до даного типу («населяють» його). Інший випадок, де для будь-яких $x,y:||A||$ має місце $x=y,$ гарантує, що $||A||$ — пропозиція.

Принцип рекурсії для $||A||$ полягає у тому, що якщо $B$ — пропозиція та $f:A\to B,$ то існує індукована функція $g:||A||\to B$ така, що $g(|a|)\equiv f(a)$ для усіх $a:A.$ Іншими словами, будь-яка пропозиція слідує з $||A||.$ Таким чином, пропозиція $||A||$ не містить більше інформації, ніж факт належності (населеності) $A.$ Завдяки пропозиційному обрізанню можна розширити логіку простих пропозицій, щоб охопити диз'юнкцію й квантор існування. Зокрема, $||A+B||$ проста пропозиційна версія «$A$ або $B$» яка не «запам'ятовує» інформацію про те, який диз'юнкт є істинним. Принцип рекурсії для обрізання має на увазі, що можна провести аналіз на випадок $||A+B||$ при спробі доказати просту пропозицію. Іншими словами, якщо $P$ — пропозиція, то для визначення $||A+B||\to P$ достатньо побудувати функцію $A+B\to Q.$

Якщо $P$ проста пропозиція, то $P\sim ||P||.$ В силу ${\mathrm{I}\mathrm{d}}_P:P\to P$ для $||P||$ справедливе $||P||\to P.$ Припустимо, що сімейство типів $P:A\to 𝒰$ таке, що

• для будь-якого $x$ тип $P(x)$ є простою пропозицією та
• для будь-якого $x$ має місце $||P||.$

Тоді $\prod _{(x:A)}P(x).$

Можна визначити предикат $Q:B\to 𝒰$ такий, що $\sum _{x:B}Q(x)$ є простою пропозицією. Тоді з елемента $A$ отримується елемент $b:B$ такий, що $Q(b),$ тому з $||A||$ можна побудувати $||\sum _{(x:B)Q(x)}||$ і тому, що $||\sum _{(x:B)}Q(x)||\sim \sum _{(x:B)}Q(x),$ може бути отриманий елемент з $B.$

Таким чином, вибір єдиний.

Якщо ми хочемо визначити функцію $f:A\to B,$ та в залежності від елемента $a:A$ доказати просто існування декотрого $b:B,$ необхідно визначити елемент з $B$ шляхом допрацювання аргументу для унікального існування $b:B$ як у теорії типів. У теорії множин ця проблема вирішується застосуванням аксіоми вибору, яка допомагає вибрати необхідні елементи. Таким чином, якщо $A$ не є множиною (наприклад, універсумом $𝒰$), то не існує узгодженої форми вибору, яка дозволила б просто вибрати елемент з $B$ для кожного $a:A$ для використання у визначенні $f(a).$

Аксіома вибору

Запис у звичайній нотації

$(\mathrm{\forall }(x:X).\mathrm{\exists }(a:A(x)).P(x,a))\Rightarrow (\mathrm{\exists }(g:\prod _{(x:X)}A(x)).\mathrm{\forall }(x:X).P(x,g(x)))$

перепишеться

$(\prod _{x:X}||\sum _{a:A(x)}P(x,a)||)\to ||\sum _{(g:\prod _{(x:X)}a(x))}\prod _{(x:X)}P(x,g(x))||,$

де «існує $x:A$ таке, що $B(x)$» записується як $||\sum _{(x:A)}B(x)||.$ Це еквівалентно формулюванню, що для будь-якої множини $X$ та будь-якого $Y:X\to 𝒰$ такого, що кожне $Y(x)$ є множиною, має місце $(\prod _{x:X}||Y(x)||)\to ||\prod _{x:X}Y(x)||,$ де $Y(x):\equiv \sum _{(g:A(x))}P(x,a).$ Та навпаки, $A(x):\equiv Y(x)$ та $P(x,a):\equiv 1.$

Це відповідає відомій еквівалентній формі класичної аксіоми вибору, а саме:

Дано набір непорожніх множин, їхній декартів добуток є непорожньою множиною.

Програмування

Пропозиційне обрізання дозволяє перевести тип \Type у пропозицію \Prop. У мові Arend є спеціальні універсуми \Prop та \Set, які складаються з пропозицій та множин, відповідно. Якщо відомо, що тип А міститься у \Prop (або \Set), то доказ відповідної властивості isProp (або isSet) у Arend може бути отриманий за допомогою вбудованої до прелюдії аксіоми Path.inProp:

\func inProp {A : \Prop} : \Pi (a a' : A) -> a = a'

Посилання

• Homotopy Type Theory Шаблон:Webarchive
• nLab Шаблон:Webarchive