тут ещё интересный момент. В интуиционизме выбрасывают law of excluded middle, но ещё и добавляют law of contradiction: ¬A → (A → B). А это не что иное, как объявление ⊥ инициальным объектом:

∀ A B . (A → ⊥) → (A → B)

Т.е. когда A = ⊥, мы говорим о существовании стрелки из ⊥ во все объекты. Тогда если стрелок из других A в ⊥ нет, выходит, что ⊥ → (A → B), т.е. истинно (ибо есть стрелки из ⊥ во все объекты).