mere proposition

mere proposition(単命題？、単なる命題？)

ChatGPTによる訳は単命題

ホモトピー型理論を調べたときに出てきた

ホモトピー型理論ではh-propositionsとも呼ばれる？

(ホモトピー・レベル) h-level 1の型(types of h-level 1)

(ホモトピー論) homotopy (−1)-types

高次元圏での対応: (-1)-groupoid

定義

型$ A が単命題(mere proposition)とは任意の$ x,y: P について$ x = y である

型$ A が型宇宙$ \mathscr{U} の型であることを$ A : \mathscr{U} と表す

$ \mathrm{isProp}(A) :\equiv \prod_{x:A} \prod_{y:A} (x = y)

真偽値レベルの対応？

(論理) 命題

(圏論) 部分終対象(subterminal object)

HoTTでの対応？

(ホモトピーレベル) h-level 1

(ホモトピー論) contractible-if-inhabited

(高次圏論) (-1)-groupoid

(高次圏論) 真偽値(truth value)

(高次トポス) (0,1)-sheaf

(高次トポス) イデアル

(ホモトピー型理論) mere propositions

(ホモトピー型理論) h-proposition