chapter \The identity type\ text \ The identity type, the higher groupoid structure of types, and type families as fibrations. \ theory Identity imports MLTT begin axiomatization Id :: \o \ o \ o \ o\ and refl :: \o \ o\ and IdInd :: \o \ (o \ o \ o \ o) \ (o \ o) \ o \ o \ o \ o\ syntax "_Id" :: \o \ o \ o \ o\ ("(2_ =\<^bsub>_\<^esub>/ _)" [111, 0, 111] 110) translations "a =\<^bsub>A\<^esub> b" \ "CONST Id A a b" axiomatization where \ \Here \A: U i\ comes last because A is often implicit\ IdF: "\a: A; b: A; A: U i\ \ a =\<^bsub>A\<^esub> b: U i" and IdI: "a: A \ refl a: a =\<^bsub>A\<^esub> a" and IdE: "\ p: a =\<^bsub>A\<^esub> b; a: A; b: A; \x y p. \p: x =\<^bsub>A\<^esub> y; x: A; y: A\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) \ \ IdInd A (fn x y p. C x y p) (fn x. f x) a b p: C a b p" and Id_comp: "\ a: A; \x y p. \x: A; y: A; p: x =\<^bsub>A\<^esub> y\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) \ \ IdInd A (fn x y p. C x y p) (fn x. f x) a a (refl a) \ f a" lemmas [form] = IdF and [intr, intro] = IdI and [elim ?p ?a ?b] = IdE and [comp] = Id_comp and [refl] = IdI section \Path induction\ \ \With \p: x = y\ in the context the invokation \eq p\ is essentially \elim p x y\, with some extra bits before and after.\ method_setup eq = \Args.term >> (fn tm => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS 0 ( CONTEXT_SUBGOAL (fn (goal, i) => fn cst as (ctxt, st) => let val facts = Proof_Context.facts_of ctxt val prems = Logic.strip_assums_hyp goal val template = \<^const>\has_type\ $ tm $ (\<^const>\Id\ $ Var (("*?A", 0), \<^typ>\o\) $ Var (("*?x", 0), \<^typ>\o\) $ Var (("*?y", 0), \<^typ>\o\)) val types = map (Thm.prop_of o #1) (Facts.could_unify facts template) @ filter (fn prem => Term.could_unify (template, prem)) prems |> map Lib.type_of_typing in case types of (Const (\<^const_name>\Id\, _) $ _ $ x $ y) :: _ => elim_ctac [tm, x, y] i cst | _ => no_ctac cst end)))))\ section \Symmetry and transitivity\ Lemma (def) pathinv: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "y =\<^bsub>A\<^esub> x" by (eq p) intro Lemma pathinv_comp [comp]: assumes "A: U i" "x: A" shows "pathinv A x x (refl x) \ refl x" unfolding pathinv_def by compute Lemma (def) pathcomp: assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" shows "x =\<^bsub>A\<^esub> z" proof (eq p) fix x q assuming "x: A" and "q: x =\<^bsub>A\<^esub> z" show "x =\<^bsub>A\<^esub> z" by (eq q) refl qed Lemma pathcomp_comp [comp]: assumes "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \ refl a" unfolding pathcomp_def by compute method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] section \Notation\ definition Id_i (infix "=" 110) where [implicit]: "x = y \ x =\<^bsub>{}\<^esub> y" definition pathinv_i ("_\" [1000]) where [implicit]: "pathinv_i p \ pathinv {} {} {} p" definition pathcomp_i (infixl "\" 121) where [implicit]: "pathcomp_i p q \ pathcomp {} {} {} {} p q" translations "x = y" \ "x =\<^bsub>A\<^esub> y" "p\" \ "CONST pathinv A x y p" "p \ q" \ "CONST pathcomp A x y z p q" section \Calculational reasoning\ calc "x = y" rhs y lemmas [sym] = pathinv[rotated 3] and [trans] = pathcomp[rotated 4] section \Basic propositional equalities\ Lemma (def) refl_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(refl x) \ p = p" by (eq p) (compute, refl) Lemma (def) pathcomp_refl: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ (refl y) = p" by (eq p) (compute, refl) definition [implicit]: "lu p \ refl_pathcomp {} {} {} p" definition [implicit]: "ru p \ pathcomp_refl {} {} {} p" translations "CONST lu p" \ "CONST refl_pathcomp A x y p" "CONST ru p" \ "CONST pathcomp_refl A x y p" Lemma lu_refl [comp]: assumes "A: U i" "x: A" shows "lu (refl x) \ refl (refl x)" unfolding refl_pathcomp_def by compute Lemma ru_refl [comp]: assumes "A: U i" "x: A" shows "ru (refl x) \ refl (refl x)" unfolding pathcomp_refl_def by compute Lemma (def) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\ \ p = refl y" by (eq p) (compute, refl) Lemma (def) pathcomp_inv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \ p\ = refl x" by (eq p) (compute, refl) Lemma (def) pathinv_pathinv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\\ = p" by (eq p) (compute, refl) Lemma (def) pathcomp_assoc: assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x = y" "q: y = z" "r: z = w" shows "p \ (q \ r) = p \ q \ r" proof (eq p) fix x q assuming "x: A" "q: x = z" show "refl x \ (q \ r) = refl x \ q \ r" proof (eq q) fix x r assuming "x: A" "r: x = w" show "refl x \ (refl x \ r) = refl x \ refl x \ r" by (eq r) (compute, refl) qed qed section \Functoriality of functions\ Lemma (def) ap: assumes "A: U i" "B: U i" "x: A" "y: A" "f: A \ B" "p: x = y" shows "f x = f y" by (eq p) intro definition ap_i ("_[_]" [1000, 0]) where [implicit]: "ap_i f p \ ap {} {} {} {} f p" translations "f[p]" \ "CONST ap A B x y f p" Lemma ap_refl [comp]: assumes "A: U i" "B: U i" "f: A \ B" "x: A" shows "f[refl x] \ refl (f x)" unfolding ap_def by compute Lemma (def) ap_pathcomp: assumes "A: U i" "B: U i" "x: A" "y: A" "z: A" "f: A \ B" "p: x = y" "q: y = z" shows "f[p \ q] = f[p] \ f[q]" proof (eq p) fix x q assuming "x: A" "q: x = z" show "f[refl x \ q] = f[refl x] \ f[q]" by (eq q) (compute, refl) qed Lemma (def) ap_pathinv: assumes "A: U i" "B: U i" "x: A" "y: A" "f: A \ B" "p: x = y" shows "f[p\] = f[p]\" by (eq p) (compute, refl) Lemma (def) ap_funcomp: assumes "A: U i" "B: U i" "C: U i" "x: A" "y: A" "f: A \ B" "g: B \ C" "p: x = y" shows "(g \ f)[p] = g[f[p]]" apply (eq p) \<^item> by compute \<^item> by compute refl done Lemma (def) ap_id: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" by (eq p) (compute, refl) section \Transport\ Lemma (def) transport: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" shows "P x \ P y" by (eq p) intro definition transport_i ("transp") where [implicit]: "transp P p \ transport {} P {} {} p" translations "transp P p" \ "CONST transport A P x y p" Lemma transport_comp [comp]: assumes "a: A" "A: U i" "\x. x: A \ P x: U i" shows "transp P (refl a) \ id (P a)" unfolding transport_def by compute Lemma apply_transport: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: y =\<^bsub>A\<^esub> x" "u: P x" shows "transp P p\ u: P y" by typechk method rewr uses eq = (rule apply_transport[OF _ _ _ _ eq]) Lemma (def) pathcomp_cancel_left: assumes "A: U i" "x: A" "y: A" "z: A" "p: x = y" "q: y = z" "r: y = z" "\: p \ q = p \ r" shows "q = r" proof - have "q = (p\ \ p) \ q" by (rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl also have ".. = p\ \ (p \ r)" by (rewr eq: pathcomp_assoc[symmetric], rewr eq: \\:_\) refl also have ".. = r" by (rewr eq: pathcomp_assoc, rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl finally show "?" by this qed Lemma (def) pathcomp_cancel_right: assumes "A: U i" "x: A" "y: A" "z: A" "p: x = y" "q: x = y" "r: y = z" "\: p \ r = q \ r" shows "p = q" proof - have "p = p \ r \ r\" by (rewr eq: pathcomp_assoc[symmetric], rewr eq: pathcomp_inv, rewr eq: pathcomp_refl) refl also have ".. = q" by (rewr eq: \\:_\, rewr eq: pathcomp_assoc[symmetric], rewr eq: pathcomp_inv, rewr eq: pathcomp_refl) refl finally show "?" by this qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] method pathcomp_cancelr = rule pathcomp_cancel_right[rotated 7] Lemma (def) transport_left_inv: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" shows "(transp P p\) \ (transp P p) = id (P x)" by (eq p) (compute, refl) Lemma (def) transport_right_inv: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" shows "(transp P p) \ (transp P p\) = id (P y)" by (eq p) (compute, refl) Lemma (def) transport_pathcomp: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "z: A" "u: P x" "p: x = y" "q: y = z" shows "transp P q (transp P p u) = transp P (p \ q) u" proof (eq p) fix x q u assuming "x: A" "q: x = z" "u: P x" show "transp P q (transp P (refl x) u) = transp P ((refl x) \ q) u" by (eq q) (compute, refl) qed Lemma (def) transport_compose_typefam: assumes "A: U i" "B: U i" "\x. x: B \ P x: U i" "f: A \ B" "x: A" "y: A" "p: x = y" "u: P (f x)" shows "transp (fn x. P (f x)) p u = transp P f[p] u" by (eq p) (compute, refl) Lemma (def) transport_function_family: assumes "A: U i" "\x. x: A \ P x: U i" "\x. x: A \ Q x: U i" "f: \x: A. P x \ Q x" "x: A" "y: A" "u: P x" "p: x = y" shows "transp Q p ((f x) u) = (f y) (transp P p u)" by (eq p) (compute, refl) Lemma (def) transport_const: assumes "A: U i" "B: U i" "x: A" "y: A" "p: x = y" shows "\b: B. transp (fn _. B) p b = b" by intro (eq p, compute, refl) definition transport_const_i ("transp'_c") where [implicit]: "transp_c B p \ transport_const {} B {} {} p" translations "transp_c B p" \ "CONST transport_const A B x y p" Lemma transport_const_comp [comp]: assumes "x: A" "b: B" "A: U i" "B: U i" shows "transp_c B (refl x) b \ refl b" unfolding transport_const_def by compute Lemma (def) pathlift: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "p: x = y" "u: P x" shows " = " by (eq p) (compute, refl) definition pathlift_i ("lift") where [implicit]: "lift P p u \ pathlift {} P {} {} p u" translations "lift P p u" \ "CONST pathlift A P x y p u" Lemma pathlift_comp [comp]: assumes "u: P x" "x: A" "\x. x: A \ P x: U i" "A: U i" shows "lift P (refl x) u \ refl " unfolding pathlift_def by compute Lemma (def) pathlift_fst: assumes "A: U i" "\x. x: A \ P x: U i" "x: A" "y: A" "u: P x" "p: x = y" shows "fst[lift P p u] = p" by (eq p) (compute, refl) section \Dependent paths\ Lemma (def) apd: assumes "A: U i" "\x. x: A \ P x: U i" "f: \x: A. P x" "x: A" "y: A" "p: x = y" shows "transp P p (f x) = f y" by (eq p) (compute, refl) definition apd_i ("apd") where [implicit]: "apd f p \ Identity.apd {} {} f {} {} p" translations "apd f p" \ "CONST Identity.apd A P f x y p" Lemma dependent_map_comp [comp]: assumes "f: \x: A. P x" "x: A" "A: U i" "\x. x: A \ P x: U i" shows "apd f (refl x) \ refl (f x)" unfolding apd_def by compute Lemma (def) apd_ap: assumes "A: U i" "B: U i" "f: A \ B" "x: A" "y: A" "p: x = y" shows "apd f p = transp_c B p (f x) \ f[p]" by (eq p) (compute, refl) section \Whiskering\ Lemma (def) right_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: a = b" "q: a = b" "r: b = c" and "\: p = q" shows "p \ r = q \ r" apply (eq r) focus vars x s t proof - have "s \ refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \ refl x" by (rule pathcomp_refl[symmetric]) finally show "?" by this qed done Lemma (def) left_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: b = c" "q: b = c" "r: a = b" and "\: p = q" shows "r \ p = r \ q" apply (eq r) focus vars x s t proof - have "refl x \ s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \ t" by (rule refl_pathcomp[symmetric]) finally show "?" by this qed done definition right_whisker_i (infix "\\<^sub>r" 121) where [implicit]: "\ \\<^sub>r r \ right_whisker {} {} {} {} {} {} r \" definition left_whisker_i (infix "\\<^sub>l" 121) where [implicit]: "r \\<^sub>l \ \ left_whisker {} {} {} {} {} {} r \" translations "\ \\<^sub>r r" \ "CONST right_whisker A a b c p q r \" "r \\<^sub>l \" \ "CONST left_whisker A a b c p q r \" Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\: p = q" shows "\ \\<^sub>r (refl b) \ ru p \ \ \ (ru q)\" unfolding right_whisker_def by compute Lemma refl_whisker [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\: p = q" shows "(refl a) \\<^sub>l \ \ (lu p) \ \ \ (lu q)\" unfolding left_whisker_def by compute method left_whisker = (rule left_whisker) method right_whisker = (rule right_whisker) section \Horizontal path-composition\ locale horiz_pathcomposable = \ \Conditions under which horizontal path-composition is defined.\ fixes i A a b c p q r s assumes [type]: "A: U i" "a: A" "b: A" "c: A" "p: a =\<^bsub>A\<^esub> b" "q: a =\<^bsub>A\<^esub> b" "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c" begin Lemma (def) horiz_pathcomp: assumes "\: p = q" "\: r = s" shows "p \ r = q \ s" proof (rule pathcomp) show "p \ r = q \ r" by right_whisker fact show ".. = q \ s" by left_whisker fact qed typechk Lemma (def) horiz_pathcomp': assumes "\: p = q" "\: r = s" shows "p \ r = q \ s" proof (rule pathcomp) show "p \ r = p \ s" by left_whisker fact show ".. = q \ s" by right_whisker fact qed typechk notation horiz_pathcomp (infix "\" 121) notation horiz_pathcomp' (infix "\''" 121) Lemma (def) horiz_pathcomp_eq_horiz_pathcomp': assumes "\: p = q" "\: r = s" shows "\ \ \ = \ \' \" unfolding horiz_pathcomp_def horiz_pathcomp'_def proof (eq \, eq \) fix p q assuming "p: a = b" "q: b = c" show "refl p \\<^sub>r q \ (p \\<^sub>l refl q) = p \\<^sub>l refl q \ (refl p \\<^sub>r q)" proof (eq p) fix a r assuming "a: A" "r: a = c" show "refl (refl a) \\<^sub>r r \ (refl a \\<^sub>l refl r) = refl a \\<^sub>l refl r \ (refl (refl a) \\<^sub>r r)" by (eq r) (compute, refl) qed qed end section \Loop space\ definition \ where "\ A a \ a =\<^bsub>A\<^esub> a" definition \2 where "\2 A a \ refl a =\<^bsub>a =\<^bsub>A\<^esub> a\<^esub> refl a" Lemma \2_\_of_\: "\2 A a \ \ (\ A a) (refl a)" unfolding \2_def \_def . section \Eckmann-Hilton\ context fixes i A a assumes [type]: "A: U i" "a: A" begin interpretation \2: horiz_pathcomposable i A a a a "refl a" "refl a" "refl a" "refl a" by unfold_locales typechk+ notation \2.horiz_pathcomp (infix "\" 121) notation \2.horiz_pathcomp' (infix "\''" 121) Lemma assumes "\: \2 A a" and "\: \2 A a" shows horiz_pathcomp_type [type]: "\ \ \: \2 A a" and horiz_pathcomp'_type [type]: "\ \' \: \2 A a" using assms unfolding \2.horiz_pathcomp_def \2.horiz_pathcomp'_def \2_def by compute+ Lemma (def) pathcomp_eq_horiz_pathcomp: assumes "\: \2 A a" "\: \2 A a" shows "\ \ \ = \ \ \" unfolding \2.horiz_pathcomp_def using assms[unfolded \2_def, type] (*TODO: A `noting` keyword that puts the noted theorem into [type]*) proof (compute, rule pathinv) have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) finally show "? = \ \ \" by this qed Lemma (def) pathcomp_eq_horiz_pathcomp': assumes "\: \2 A a" "\: \2 A a" shows "\ \' \ = \ \ \" unfolding \2.horiz_pathcomp'_def using assms[unfolded \2_def, type] proof compute have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) finally have eq\: "? = \" by this have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) finally show "? = \ \ \" by this qed Lemma (def) eckmann_hilton: assumes "\: \2 A a" "\: \2 A a" shows "\ \ \ = \ \ \" using \2_def[comp] proof - have "\ \ \ = \ \ \" by (rule pathcomp_eq_horiz_pathcomp) also have [simplified comp]: ".. = \ \' \" \ \Danger! Inferred implicit has an equivalent form but needs to be manually simplified.\ by (rewr eq: \2.horiz_pathcomp_eq_horiz_pathcomp') refl also have ".. = \ \ \" by (rule pathcomp_eq_horiz_pathcomp') finally show "\ \ \ = \ \ \" by this qed end end