У A | B = Either A B всегда есть "разложение" на проекции, то есть, наоборот, стрелки из компонент в "сумму". В данном случае это Left: A → Either A B и Right: B → Either A B. Натурально, для всех f: (Either A B)→C есть пара стрелок g: A→C и h: B→C таких, что f=[g, h], и наоборот, для каждой пары g: A→C и h: B→C есть стрелка f такая, что g=f . Left, и h=f . Right.
Это всего лишь многословное заявление того простого факта, что f: (Either A (A→⊥))→⊥ всегда можно разложить на некоторые g:A→⊥ и h:(A→⊥)→⊥, и наоборот, её всегда можно собрать из g и h, если таковые даны.
Тогда при N=flip id доказывающем в частности A→¬¬A, получаем M f = N g h = N (f . Left) (f . Right)
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2013-04-25 05:41 pm (UTC)вот теперь я таки готов так заявить :)
У A | B = Either A B всегда есть "разложение" на проекции, то есть, наоборот, стрелки из компонент в "сумму". В данном случае это Left: A → Either A B и Right: B → Either A B. Натурально, для всех f: (Either A B)→C есть пара стрелок g: A→C и h: B→C таких, что f=[g, h], и наоборот, для каждой пары g: A→C и h: B→C есть стрелка f такая, что g=f . Left, и h=f . Right.
Это всего лишь многословное заявление того простого факта, что f: (Either A (A→⊥))→⊥ всегда можно разложить на некоторые g:A→⊥ и h:(A→⊥)→⊥, и наоборот, её всегда можно собрать из g и h, если таковые даны.
Тогда при N=flip id доказывающем в частности A→¬¬A, получаем M f = N g h = N (f . Left) (f . Right)