Library HoTT.Foundations.MLTT.Logic

This file is part of https://github.com/mjub/hott.

Require Export Foundations.MLTT.Init.

Martin-LΓΆf Type Theory, Part II: The Logic

The empty type

The Empty type, also known as False.

Inductive Empty : π‘ˆβ‚€ := .

Notation "βˆ…" := Empty.

Elimination principles for the empty type.

Definition ind_empty (C : βˆ… β†’ π‘ˆ) x : C x :=
  match x with
  end.

Definition rec_empty {C : π‘ˆ} (x : βˆ…) : C :=
  match x with
  end.

The unit type

The Unit type, also known as True.

Inductive Unit : π‘ˆβ‚€ := it.

Notation "𝟏" := Unit.
Notation "βˆ—" := it.

Elimination principles for the unit type.

Definition ind_unit (C : 𝟏 β†’ π‘ˆ) (cβ‚€ : C βˆ—) x :=
  match x with
  | βˆ— β‡’ cβ‚€
  end.

Definition rec_unit {C : π‘ˆ} (cβ‚€ : C) x :=
  match x with
  | βˆ— β‡’ cβ‚€
  end.

Product types

This is the nondependent version of βˆ‘-types, i.e. ordinary cartesian product A Γ— B.

Notation "A Γ— B" := (βˆ‘ (_ : A), B)
  (at level 40, right associativity).

Elimination principles for product types.

Section Prod.
  Context {A B : π‘ˆ}.

  Definition ind_prod (C : A Γ— B β†’ π‘ˆ) (f : ∏ (x : A) (y : B), C (x, y)) p :=
    match p with
    | (x, y) β‡’ f x y
    end.

  Definition rec_prod {C : π‘ˆ} (f : A β†’ B β†’ C) (p : A Γ— B) :=
    match p with
    | (x, y) β‡’ f x y
    end.

End Prod.

Coproduct types

The disjoint union A + B of two types A, B.

Inductive Coprod (A B : π‘ˆ) : π‘ˆ := inl : A β†’ _ | inr : B β†’ _.

Arguments inl {_ _}.
Arguments inr {_ _}.

Notation "A + B" := (Coprod A B)
  (at level 50, right associativity).

Elimination principles for coproduct types.

Section Coprod.
  Context {A B : π‘ˆ}.

  Definition ind_coprod (C : A + B β†’ π‘ˆ) (f : ∏ x, C (inl x)) (g : ∏ y, C (inr y)) p :=
    match p with
    | inl x β‡’ f x
    | inr y β‡’ g y
    end.

  Definition rec_coprod {C : π‘ˆ} (f : A β†’ C) (g : B β†’ C) p :=
    match p with
    | inl x β‡’ f x
    | inr y β‡’ g y
    end.

End Coprod.

The type of booleans

The type of Booleans, which could alternatively be defined as 𝟏 + 𝟏 (see above).

Inductive Bool : π‘ˆβ‚€ := true | false.

Elimination principles for the type of booleans.

Definition ind_bool (C : Bool β†’ π‘ˆ) (cβ‚€ : C true) (c₁ : C false) b :=
  match b with
  | true β‡’ cβ‚€
  | false β‡’ c₁
  end.

Definition rec_bool {C : π‘ˆ} (cβ‚€ c₁ : C) b :=
  match b with
  | true β‡’ cβ‚€
  | false β‡’ c₁
  end.