Introduction

• Pick a book or paper, and formalize its ideas within the ITP system to build and further my understanding.
• Formalize my own notions and ideas (e.g. Local Lexing [7]) for the same reasons.

Use Case: Category Theory

structure Category =
  type Object
  type Arrow
  let dom : Arrow → Object
  let cod : Arrow → Object
  def HomSet(A : Object, B : Object) =
    { f : Arrow | dom f = A ∧ cod f = B }
  let id : (x : Object) → HomSet(x, x)
  let then : (f : Arrow) → (g : Arrow | dom g = cod f) →
             { h : Arrow | dom h = dom f ∧ cod h = cod g }
  axiom identity : ∀ x : Arrow. (x then id (cod x)) = (id (dom x) then x) = x
  axiom associativity : ∀ e f g : Arrow. ((e then f) then g) = (e then (f then g))
end

{ f : Arrow | dom f = A ∧ cod f = B }

(g : { g : Arrow | dom g = cod f })

cod e = dom f ∧ cod f = dom g

Nil Type For Expressing Undefinedness

let Arrow : Type
axiom ¬(nil : Arrow)

Function Subtyping

C ≤ A ∧ B ≤ D

∀ x : A. f x = g x

A = C ∧ B ≤ D

Union, Intersection and Difference Types

A ≤ A ∪ B ∧ B ≤ A ∪ B

A ∩ B ≤ A ∧ A ∩ B ≤ B

¬ (∃x : Null. true)

∀ A B : Type. ∀ a : A. (a : B) = (a : A ∩ B)
∀ A B : Type. ∀ b : B. (b : A) = (b : A ∩ B)
∀ A B : Type. ∀ a : A. a : A ∪ B
∀ A B : Type. ∀ b : B. b : A ∪ B

Type Extensionality