:PROPERTIES: :ID: c375ece5-74f6-48e7-98d2-08e450af915c :mtime: 20230920160113 20230918150936 20230808112409 :ctime: 20230808105011 :END: #+title: Path Induction #+filetags: :public:project:hott:type-theory:study: * Definition The induction principle for the identity type is called path induction, . It can be seen as stating that the family of identity types is freely generated by the elements of the form reflx : x = x. Path induction: Given a family #+BEGIN_SRC agda C : (x y : A ) → x ≡ y → Type #+END_SRC and a function #+BEGIN_SRC agda c : (x : A ) → (C x x refl) #+END_SRC There exists a function #+BEGIN_SRC agda f : (x y : A ) → (p : x ≡ y) → C x y p #+END_SRC such that #+BEGIN_SRC agda f x x refl ≡ c x #+END_SRC * Non-Dependent Induction The non-dependent form is easier to understand. It says that if #+BEGIN_SRC agda C : A → A → Type #+END_SRC such that #+BEGIN_SRC agda (x : A) → C x x #+END_SRC then we can construct a function #+BEGIN_SRC agda f : (x y : A ) → x ≡ y → C x y #+END_SRC * The Idea The idea behind induction for Nats is that every Nat is either 0 or suc n. The idea behind induction for equality is that every equality is refl.