日々の流転

λ. True≠False の証明

ペアノの公理における 0≠s(x) のように、一般に異なるコンストラクタによって得られる値は異なるべきはず。 なので、最も単純な True≠False の場合について証明しようとしてみたのだが、簡単に証明できるかと思いきや large elimination が必要になってしまった。うーん……

data Taut = tt
data Absurd =

Not :: Set -> Set
Not X = X -> Absurd

idata Id (|X::Set) :: X -> X -> Set where
    refId (!x::X) :: Id x x

substId (X::Set) (!P::X->Set) (x,y::X) :: Id x y -> P x -> P y
substId id p = case id of (refId z)-> p

disjointness :: Not (Id True False)
disjointness id =
    let T :: Bool -> Set
        T b = case b of
                (False)-> Absurd
                (True )-> Taut
    in substId T id tt

λ. 「カッセ」

「カッセ」というのは何かと思っていたら、「かっ飛ばせ」の略だそうだ。 知らなかった。

λ. 『寄生獣 (2)』 by 岩明 均

を読んだ。

λ. 帰りの電車で今日も寝過ごした

.