https://m-hiyama-memo.hatenablog.com/entry/2021/01/09/221819

$\require{color} \newcommand{\hyp}{\mbox{-}}% \newcommand{\To}{\Rightarrow}% \newcommand{\F}[1]{ \langle\![{#1}]\!\rangle }% \newcommand{\As}{\;::\;}%$
連言

and.left : ?M_1 ∧ ?M_2 → ?M_1 （A∧B ⇒ A）
and.right : ?M_1 ∧ ?M_2 → ?M_2 （A∧B ⇒ B)
and.intro : ?M_1 → ?M_2 → ?M_1 ∧ ?M_2 （A B ⇒ A∧B）

含意

空白〈right-eval〉 : ((?M_1 → ?M_2) → ?M1) → ?M_2 (（A → B) A ⇒ B）
assume 変数 : 型, 式 ≡ λ 変数 : 型, 式

assume h : A ∧ ¬ B,
and.intro (and.right h) (and.left h)

${}^\cap(copy;(\F{and.right} \otimes \F{and.left}) ; \F{and.intro})\\ \xymatrix { {} &{\# 1 \;\lambda\, h} \ar[d]^{A\land \lnot B} &{} \\ {} &*{\bullet} \ar[dl] \ar[dr] &{} \\ {\bar{\urcorner} } \ar[d]_-{\lnot B} &{} &{\bar{\ulcorner} } \ar[d]^-{A} \\ {}\ar[dr]_-{\lnot B} &{} &{}\ar[dl]^-{A} \\ {} &*{\blacktriangledown} \ar[d]^-{\lnot B \land A} &{} \\ {\#1} &*+[o][F]{\to} \ar[l] \ar[d]^-{A\land \lnot B \,\to\, \lnot B \land A} &{} \\ {} & & }$

選言

or.inl : ?M_1 → ?M_1 ∨ ?M_2 （A ⇒ A∨B）
or.inr : ?M_2 → ?M_1 ∨ ?M_2 （B ⇒ A∨B）
or.elim : ?M_1 ∨ ?M_2 → (?M_1 → ?M_3) → (?M_2 → ?M_3) → ?M_3 （A∨B A→C B→C ⇒ C）

section
  variable h : A ∨ B
  variables (ha : A → C) (hb : B → C)
  example : C :=
  or.elim h
    (assume h1 : A,
      show C, from ha h1)
    (assume h1 : B,
      show C, from hb h1)
end

否定（矛盾）

true, false : Prop
false.elim : false → ?M_1 （⊥ → A）
trivial : true
by_contradiction : (¬?M_1 → false) → ?M_1 （¬¬A → A）