Library HoTT.Foundations.MLTT.Init

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

Require Export Ltac.

Martin-LΓΆf Type Theory, Part I: The Essentials

Universes

Let us write the universes π‘ˆ instead of Type because, why not?

Notation π‘ˆβ‚€ := Set.
Notation π‘ˆ := Type.

Dependent function types

Dependent function types, or ∏-types.
The notation level and format was extracted from the Coq standard library.

Notation "∏ x .. y , B" := (βˆ€ x, .. (βˆ€ y, B) ..)
  (at level 200, x binder, y binder, right associativity,
  format "'[ ' '[ ' ∏ x .. y ']' , '/' B ']'").

Nondependent version, i.e. ordinary functions A β†’ B.

Notation "A β†’ B" := (∏ (_ : A), B)
  (at level 99, B at level 200, right associativity).

Ξ»-abstractions.

Notation "'Ξ»' x .. y , T" := (fun x β‡’ .. (fun y β‡’ T) ..)
  (at level 200, x binder, y binder, right associativity,
  format "'[ ' '[ ' 'Ξ»' x .. y ']' , '/' T ']'").

Dependent pair types

Dependent pair types, or βˆ‘-types.
I write pair instead of exist because I find it unequivocal. The notations were, again, extracted from the Coq standard library.
I may change the definition to Record in the future so that I can make use of Primitive Projections.

Inductive Sigma (A : π‘ˆ) (B : A β†’ π‘ˆ) : π‘ˆ :=
  pair : ∏ x, B x β†’ _.

Arguments pair {_ _}.

Notation "βˆ‘ x .. y , B" := (Sigma _ (Ξ» x, .. (Sigma _ (Ξ» y, B)) ..))
  (at level 200, x binder, y binder, right associativity,
  format "'[ ' '[ ' βˆ‘ x .. y ']' , '/' B ']'").

Notation "( x , .. , y , z )" := (pair x (.. (pair y z) ..))
  (at level 0, format "( '[' x , '/' .. , '/' y , '/' z ']' )").

Elimination principles for βˆ‘-types.

Section Sigma.
  Context {A : π‘ˆ} {B : A β†’ π‘ˆ}.

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

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

Projections.

  Definition pr₁ (p : βˆ‘ x, B x) :=
    match p with
    | (x, y) β‡’ x
    end.

  Definition prβ‚‚ (p : βˆ‘ x, B x) : B (pr₁ p) :=
    match p with
    | (x, y) β‡’ y
    end.

End Sigma.

Notation "p .1" := (pr₁ p)
  (at level 1, left associativity, format "p .1").
Notation "p .2" := (prβ‚‚ p)
  (at level 1, left associativity, format "p .2").

Identity types

I write Id instead of Path because I hold the controversial opinion that we should not think of types as spaces.

Inductive Id {A : π‘ˆ} (x : A) : A β†’ π‘ˆ :=
  refl : Id x x.

Arguments refl {_ _}.

Notation "x = y" := (Id x y)
  (at level 70, no associativity).

Elimination principles for identity types.

Section Id.
  Context {A : π‘ˆ} {x : A}.

  Definition ind_id (C : ∏ y, x = y β†’ π‘ˆ) (cβ‚€ : C x refl) {y : A} (p : x = y) :=
    match p with
    | refl β‡’ cβ‚€
    end.

  Definition rec_id {C : π‘ˆ} (cβ‚€ : C) {y : A} (p : x = y) :=
    match p with
    | refl β‡’ cβ‚€
    end.

End Id.