From 218c9dfc8197da504d0ec3a279d8dfce6551b3c4 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 6 Aug 2014 18:21:54 -0700 Subject: [PATCH] feat(library/hott): begin porting Coq HoTT --- library/hott/logic.lean | 438 +++++++++------ library/hott/path_groupoids.lean | 922 +++++++++++++++++++++++++++++++ 2 files changed, 1191 insertions(+), 169 deletions(-) create mode 100644 library/hott/path_groupoids.lean diff --git a/library/hott/logic.lean b/library/hott/logic.lean index 18ff2a146..d1ac3a44c 100644 --- a/library/hott/logic.lean +++ b/library/hott/logic.lean @@ -1,243 +1,343 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura +-- Author: Leonardo de Moura, Jeremy Avigad +-- Ported from Coq HoTT + +notation `assume` binders `,` r:(scoped f, f) := r +notation `take` binders `,` r:(scoped f, f) := r abbreviation id {A : Type} (a : A) := a abbreviation compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x) infixl `∘`:60 := compose -inductive path {A : Type} (a : A) : A → Type := -| refl : path a a -infix `=`:50 := path +-- -- Equivalences +-- -- ------------ -definition transport {A : Type} {a b : A} {P : A → Type} (H1 : a = b) (H2 : P a) : P b -:= path_rec H2 H1 +-- abbreviation Sect {A B : Type} (s : A → B) (r : B → A) := Πx : A, r (s x) ≈ x -namespace logic - notation p `*(`:75 u `)` := transport p u -end logic -using logic +-- -- TODO: need better means of declaring structures +-- -- TODO: note that Coq allows projections to be declared to be coercions on the fly +-- -- TODO: also think about namespaces: what should be in / out? +-- -- TODO: can we omit ': Type'? -definition symm {A : Type} {a b : A} (p : a = b) : b = a -:= p*(refl a) +-- -- Structure IsEquiv -definition trans {A : Type} {a b c : A} (p1 : a = b) (p2 : b = c) : a = c -:= p2*(p1) +-- inductive IsEquiv {A B : Type} (f : A → B) : Type := +-- | IsEquiv_mk : Π +-- (equiv_inv : B → A) +-- (eisretr : Sect equiv_inv f) +-- (eissect : Sect f equiv_inv) +-- (eisadj : Πx, eisretr (f x) ≈ ap f (eissect x)), +-- IsEquiv f -calc_subst transport -calc_refl refl -calc_trans trans +-- definition equiv_inv {A B : Type} {f : A → B} (H : IsEquiv f) : B → A := +-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, equiv_inv) H -namespace logic - postfix `⁻¹`:100 := symm - infixr `⬝`:75 := trans -end logic -using logic +-- -- TODO: note: does not type check without giving the type +-- definition eisretr {A B : Type} {f : A → B} (H : IsEquiv f) : Sect (equiv_inv H) f := +-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisretr) H -theorem trans_refl_right {A : Type} {x y : A} (p : x = y) : p = p ⬝ (refl y) -:= refl p +-- definition eissect {A B : Type} {f : A → B} (H : IsEquiv f) : Sect f (equiv_inv H) := +-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eissect) H -theorem trans_refl_left {A : Type} {x y : A} (p : x = y) : p = (refl x) ⬝ p -:= path_rec (trans_refl_right (refl x)) p +-- definition eisadj {A B : Type} {f : A → B} (H : IsEquiv f) : +-- Πx, eisretr H (f x) ≈ ap f (eissect H x) := +-- IsEquiv_rec (λequiv_inv eisretr eissect eisadj, eisadj) H -theorem refl_symm {A : Type} (x : A) : (refl x)⁻¹ = (refl x) -:= refl (refl x) +-- -- Structure Equiv -theorem refl_trans {A : Type} (x : A) : (refl x) ⬝ (refl x) = (refl x) -:= refl (refl x) +-- inductive Equiv (A B : Type) : Type := +-- | Equiv_mk : Π +-- (equiv_fun : A → B) +-- (equiv_isequiv : IsEquiv equiv_fun), +-- Equiv A B -theorem trans_symm {A : Type} {x y : A} (p : x = y) : p ⬝ p⁻¹ = refl x -:= have q : (refl x) ⬝ (refl x)⁻¹ = refl x, from - ((refl_symm x)⁻¹)*(refl_trans x), - path_rec q p +-- definition equiv_fun {A B : Type} (e : Equiv A B) : A → B := +-- Equiv_rec (λequiv_fun equiv_isequiv, equiv_fun) e -theorem symm_trans {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = refl y -:= have q : (refl x)⁻¹ ⬝ (refl x) = refl x, from - ((refl_symm x)⁻¹)*(refl_trans x), - path_rec q p +-- -- TODO: use a type class instead? +-- coercion equiv_fun : Equiv -theorem symm_symm {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p -:= have q : ((refl x)⁻¹)⁻¹ = refl x, from - refl (refl x), - path_rec q p +-- definition equiv_isequiv [coercion] {A B : Type} (e : Equiv A B) : IsEquiv (equiv_fun e) := +-- Equiv_rec (λequiv_fun equiv_isequiv, equiv_isequiv) e -theorem trans_assoc {A : Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r -:= have e1 : (p ⬝ q) ⬝ (refl z) = p ⬝ q, from - (trans_refl_right (p ⬝ q))⁻¹, - have e2 : q ⬝ (refl z) = q, from - (trans_refl_right q)⁻¹, - have e3 : p ⬝ (q ⬝ (refl z)) = p ⬝ q, from - e2*(refl (p ⬝ (q ⬝ (refl z)))), - path_rec (e3 ⬝ e1⁻¹) r +-- -- coercion equiv_isequiv -definition ap {A : Type} {B : Type} (f : A → B) {a b : A} (p : a = b) : f a = f b -:= p*(refl (f a)) +-- -- TODO: better symbol +-- infix `<~>`:25 := Equiv +-- notation e `⁻¹`:75 := equiv_inv e -theorem ap_refl {A : Type} {B : Type} (f : A → B) (a : A) : ap f (refl a) = refl (f a) -:= refl (refl (f a)) -section - parameters {A : Type} {B : Type} {C : Type} - parameters (f : A → B) (g : B → C) - parameters (x y z : A) (p : x = y) (q : y = z) +-- -- Truncation levels +-- -- ----------------- - theorem ap_trans_dist : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) - := have e1 : ap f (p ⬝ refl y) = (ap f p) ⬝ (ap f (refl y)), from refl _, - path_rec e1 q +-- inductive Contr (A : Type) : Type := +-- | Contr_mk : Π +-- (center : A) +-- (contr : Πy : A, center ≈ y), +-- Contr A - theorem ap_inv_dist : ap f (p⁻¹) = (ap f p)⁻¹ - := have e1 : ap f ((refl x)⁻¹) = (ap f (refl x))⁻¹, from refl _, - path_rec e1 p +-- definition center {A : Type} (C : Contr A) : A := Contr_rec (λcenter contr, center) C - theorem ap_compose : ap g (ap f p) = ap (g∘f) p - := have e1 : ap g (ap f (refl x)) = ap (g∘f) (refl x), from refl _, - path_rec e1 p +-- definition contr {A : Type} (C : Contr A) : Πy : A, center C ≈ y := +-- Contr_rec (λcenter contr, contr) C - theorem ap_id : ap id p = p - := have e1 : ap id (refl x) = (refl x), from refl (refl x), - path_rec e1 p -end +-- inductive trunc_index : Type := +-- | minus_two : trunc_index +-- | trunc_S : trunc_index → trunc_index -section - parameters {A : Type} {B : A → Type} (f : Π x, B x) - definition D [private] (x y : A) (p : x = y) := p*(f x) = f y - definition d [private] (x : A) : D x x (refl x) - := refl (f x) +-- -- TODO: add coercions to / from nat - theorem apd {a b : A} (p : a = b) : p*(f a) = f b - := path_rec (d a) p -end +-- -- TODO: note in the Coq version, there is an internal version +-- definition IsTrunc (n : trunc_index) : Type → Type := +-- trunc_index_rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n +-- -- TODO: in the Coq version, this is notation +-- abbreviation minus_one := trunc_S minus_two +-- abbreviation IsHProp := IsTrunc minus_one +-- abbreviation IsHSet := IsTrunc (trunc_S minus_one) -abbreviation homotopy {A : Type} {P : A → Type} (f g : Π x, P x) -:= Π x, f x = g x +-- prefix `!`:75 := center -namespace logic - infix `∼`:50 := homotopy -end logic -using logic -notation `assume` binders `,` r:(scoped f, f) := r -notation `take` binders `,` r:(scoped f, f) := r +-- -- Funext +-- -- ------ -section - parameters {A : Type} {B : Type} +-- -- TODO: move this to an "axioms" folder +-- -- TODO: take a look at the Coq tricks +-- axiom funext {A : Type} {P : A → Type} (f g : Π x : A, P x) : IsEquiv (@apD10 A P f g) - theorem hom_refl (f : A → B) : f ∼ f - := take x, refl (f x) +-- definition path_forall {A : Type} {P : A → Type} (f g : Π x : A, P x) : f ∼ g → f ≈ g := +-- (funext f g)⁻¹ - theorem hom_symm {f g : A → B} : f ∼ g → g ∼ f - := assume h, take x, (h x)⁻¹ +-- definition path_forall2 {A B : Type} {P : A → B → Type} (f g : Π x y, P x y) : +-- (Πx y, f x y ≈ g x y) → f ≈ g := +-- λE, path_forall f g (λx, path_forall (f x) (g x) (E x)) - theorem hom_trans {f g h : A → B} : f ∼ g → g ∼ h → f ∼ h - := assume h1 h2, take x, (h1 x) ⬝ (h2 x) - theorem hom_fun {f g : A → B} {x y : A} (H : f ∼ g) (p : x = y) : (H x) ⬝ (ap g p) = (ap f p) ⬝ (H y) - := have e1 : (H x) ⬝ (refl (g x)) = (refl (f x)) ⬝ (H x), from - calc (H x) ⬝ (refl (g x)) = H x : (trans_refl_right (H x))⁻¹ - ... = (refl (f x)) ⬝ (H x) : trans_refl_left (H x), - have e2 : (H x) ⬝ (ap g (refl x)) = (ap f (refl x)) ⬝ (H x), from - calc (H x) ⬝ (ap g (refl x)) = (H x) ⬝ (refl (g x)) : {ap_refl g x} - ... = (refl (f x)) ⬝ (H x) : e1 - ... = (ap f (refl x)) ⬝ (H x) : {symm (ap_refl f x)}, - path_rec e2 p +-- -- Empty type +-- -- ---------- +-- inductive empty : Type -end +-- theorem empty_elim (A : Type) (H : empty) : A := +-- empty_rec (λ e, A) H -definition loop_space (A : Type) (a : A) := a = a -notation `Ω` `(` A `,` a `)` := loop_space A a -definition loop2d_space (A : Type) (a : A) := (refl a) = (refl a) -notation `Ω²` `(` A `,` a `)` := loop2d_space A a -inductive empty : Type -theorem empty_elim (c : Type) (H : empty) : c -:= empty_rec (λ e, c) H +-- inductive true : Prop := +-- | trivial : true -definition not (A : Type) := A → empty -prefix `¬`:40 := not +-- abbreviation not (a : Prop) := a → false +-- prefix `¬`:40 := not -theorem not_intro {a : Type} (H : a → empty) : ¬ a -:= H -theorem not_elim {a : Type} (H1 : ¬ a) (H2 : a) : empty -:= H1 H2 -theorem absurd {a : Type} (H1 : a) (H2 : ¬ a) : empty -:= H2 H1 +-- theorem trans_refl_right {A : Type} {x y : A} (p : x = y) : p = p ⬝ (refl y) +-- := refl p -theorem mt {a b : Type} (H1 : a → b) (H2 : ¬ b) : ¬ a -:= assume Ha : a, absurd (H1 Ha) H2 +-- theorem trans_refl_left {A : Type} {x y : A} (p : x = y) : p = (refl x) ⬝ p +-- := path_rec (trans_refl_right (refl x)) p -theorem contrapos {a b : Type} (H : a → b) : ¬ b → ¬ a -:= assume Hnb : ¬ b, mt H Hnb +-- theorem refl_symm {A : Type} (x : A) : (refl x)⁻¹ = (refl x) +-- := refl (refl x) -theorem absurd_elim {a : Type} (b : Type) (H1 : a) (H2 : ¬ a) : b -:= empty_elim b (absurd H1 H2) +-- theorem refl_trans {A : Type} (x : A) : (refl x) ⬝ (refl x) = (refl x) +-- := refl (refl x) -inductive unit : Type := -| star : unit +-- theorem trans_symm {A : Type} {x y : A} (p : x = y) : p ⬝ p⁻¹ = refl x +-- := have q : (refl x) ⬝ (refl x)⁻¹ = refl x, from +-- ((refl_symm x)⁻¹)*(refl_trans x), +-- path_rec q p -notation `⋆`:max := star +-- theorem symm_trans {A : Type} {x y : A} (p : x = y) : p⁻¹ ⬝ p = refl y +-- := have q : (refl x)⁻¹ ⬝ (refl x) = refl x, from +-- ((refl_symm x)⁻¹)*(refl_trans x), +-- path_rec q p -theorem absurd_not_unit (H : ¬ unit) : empty -:= absurd star H +-- theorem symm_symm {A : Type} {x y : A} (p : x = y) : (p⁻¹)⁻¹ = p +-- := have q : ((refl x)⁻¹)⁻¹ = refl x, from +-- refl (refl x), +-- path_rec q p -theorem not_empty_trivial : ¬ empty -:= assume H : empty, H +-- theorem trans_assoc {A : Type} {x y z w : A} (p : x = y) (q : y = z) (r : z = w) : p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r +-- := have e1 : (p ⬝ q) ⬝ (refl z) = p ⬝ q, from +-- (trans_refl_right (p ⬝ q))⁻¹, +-- have e2 : q ⬝ (refl z) = q, from +-- (trans_refl_right q)⁻¹, +-- have e3 : p ⬝ (q ⬝ (refl z)) = p ⬝ q, from +-- e2*(refl (p ⬝ (q ⬝ (refl z)))), +-- path_rec (e3 ⬝ e1⁻¹) r -theorem upun (x : unit) : x = ⋆ -:= unit_rec (refl ⋆) x +-- definition ap {A : Type} {B : Type} (f : A → B) {a b : A} (p : a = b) : f a = f b +-- := p*(refl (f a)) -inductive product (A : Type) (B : Type) : Type := -| pair : A → B → product A B +-- theorem ap_refl {A : Type} {B : Type} (f : A → B) (a : A) : ap f (refl a) = refl (f a) +-- := refl (refl (f a)) -infixr `×`:30 := product -infixr `∧`:30 := product +-- section +-- parameters {A : Type} {B : Type} {C : Type} +-- parameters (f : A → B) (g : B → C) +-- parameters (x y z : A) (p : x = y) (q : y = z) -notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t +-- theorem ap_trans_dist : ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) +-- := have e1 : ap f (p ⬝ refl y) = (ap f p) ⬝ (ap f (refl y)), from refl _, +-- path_rec e1 q -definition pr1 {A : Type} {B : Type} (p : A × B) : A -:= product_rec (λ a b, a) p +-- theorem ap_inv_dist : ap f (p⁻¹) = (ap f p)⁻¹ +-- := have e1 : ap f ((refl x)⁻¹) = (ap f (refl x))⁻¹, from refl _, +-- path_rec e1 p -definition pr2 {A : Type} {B : Type} (p : A × B) : B -:= product_rec (λ a b, b) p +-- theorem ap_compose : ap g (ap f p) = ap (g∘f) p +-- := have e1 : ap g (ap f (refl x)) = ap (g∘f) (refl x), from refl _, +-- path_rec e1 p -theorem uppt {A : Type} {B : Type} (p : A × B) : (pr1 p, pr2 p) = p -:= product_rec (λ x y, refl (x, y)) p +-- theorem ap_id : ap id p = p +-- := have e1 : ap id (refl x) = (refl x), from refl (refl x), +-- path_rec e1 p +-- end -inductive sum (A : Type) (B : Type) : Type := -| inl : A → sum A B -| inr : B → sum A B +-- section +-- parameters {A : Type} {B : A → Type} (f : Π x, B x) +-- definition D [private] (x y : A) (p : x = y) := p*(f x) = f y +-- definition d [private] (x : A) : D x x (refl x) +-- := refl (f x) -namespace logic - infixr `+`:25 := sum -end logic -using logic -infixr `∨`:25 := sum +-- theorem apd {a b : A} (p : a = b) : p*(f a) = f b +-- := path_rec (d a) p +-- end -theorem sum_elim {a : Type} {b : Type} {c : Type} (H1 : a + b) (H2 : a → c) (H3 : b → c) : c -:= sum_rec H2 H3 H1 -theorem resolve_right {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ a) : b -:= sum_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb) +-- abbreviation homotopy {A : Type} {P : A → Type} (f g : Π x, P x) +-- := Π x, f x = g x -theorem resolve_left {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ b) : a -:= sum_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2) +-- namespace logic +-- infix `∼`:50 := homotopy +-- end +-- using logic -theorem sum_flip {a : Type} {b : Type} (H : a + b) : b + a -:= sum_elim H (assume Ha, inr b Ha) (assume Hb, inl a Hb) +-- notation `assume` binders `,` r:(scoped f, f) := r +-- notation `take` binders `,` r:(scoped f, f) := r -inductive Sigma {A : Type} (B : A → Type) : Type := -| sigma_intro : Π a, B a → Sigma B +-- section +-- parameters {A : Type} {B : Type} -notation `Σ` binders `,` r:(scoped P, Sigma P) := r +-- theorem hom_refl (f : A → B) : f ∼ f +-- := take x, refl (f x) -definition dpr1 {A : Type} {B : A → Type} (p : Σ x, B x) : A -:= Sigma_rec (λ a b, a) p +-- theorem hom_symm {f g : A → B} : f ∼ g → g ∼ f +-- := assume h, take x, (h x)⁻¹ -definition dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) -:= Sigma_rec (λ a b, b) p +-- theorem hom_trans {f g h : A → B} : f ∼ g → g ∼ h → f ∼ h +-- := assume h1 h2, take x, (h1 x) ⬝ (h2 x) + +-- theorem hom_fun {f g : A → B} {x y : A} (H : f ∼ g) (p : x = y) : (H x) ⬝ (ap g p) = (ap f p) ⬝ (H y) +-- := have e1 : (H x) ⬝ (refl (g x)) = (refl (f x)) ⬝ (H x), from +-- calc (H x) ⬝ (refl (g x)) = H x : (trans_refl_right (H x))⁻¹ +-- ... = (refl (f x)) ⬝ (H x) : trans_refl_left (H x), +-- have e2 : (H x) ⬝ (ap g (refl x)) = (ap f (refl x)) ⬝ (H x), from +-- calc (H x) ⬝ (ap g (refl x)) = (H x) ⬝ (refl (g x)) : {ap_refl g x} +-- ... = (refl (f x)) ⬝ (H x) : e1 +-- ... = (ap f (refl x)) ⬝ (H x) : {symm (ap_refl f x)}, +-- path_rec e2 p + + +-- end + +-- definition loop_space (A : Type) (a : A) := a = a +-- notation `Ω` `(` A `,` a `)` := loop_space A a + +-- definition loop2d_space (A : Type) (a : A) := (refl a) = (refl a) +-- notation `Ω²` `(` A `,` a `)` := loop2d_space A a + +-- inductive empty : Type + +-- theorem empty_elim (c : Type) (H : empty) : c +-- := empty_rec (λ e, c) H + +-- definition not (A : Type) := A → empty +-- prefix `¬`:40 := not + +-- theorem not_intro {a : Type} (H : a → empty) : ¬ a +-- := H + +-- theorem not_elim {a : Type} (H1 : ¬ a) (H2 : a) : empty +-- := H1 H2 + +-- theorem absurd {a : Type} (H1 : a) (H2 : ¬ a) : empty +-- := H2 H1 + +-- theorem mt {a b : Type} (H1 : a → b) (H2 : ¬ b) : ¬ a +-- := assume Ha : a, absurd (H1 Ha) H2 + +-- theorem contrapos {a b : Type} (H : a → b) : ¬ b → ¬ a +-- := assume Hnb : ¬ b, mt H Hnb + +-- theorem absurd_elim {a : Type} (b : Type) (H1 : a) (H2 : ¬ a) : b +-- := empty_elim b (absurd H1 H2) + +-- inductive unit : Type := +-- | star : unit + +-- notation `⋆`:max := star + +-- theorem absurd_not_unit (H : ¬ unit) : empty +-- := absurd star H + +-- theorem not_empty_trivial : ¬ empty +-- := assume H : empty, H + +-- theorem upun (x : unit) : x = ⋆ +-- := unit_rec (refl ⋆) x + +-- inductive product (A : Type) (B : Type) : Type := +-- | pair : A → B → product A B + +-- infixr `×`:30 := product +-- infixr `∧`:30 := product + +-- notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t + +-- definition pr1 {A : Type} {B : Type} (p : A × B) : A +-- := product_rec (λ a b, a) p + +-- definition pr2 {A : Type} {B : Type} (p : A × B) : B +-- := product_rec (λ a b, b) p + +-- theorem uppt {A : Type} {B : Type} (p : A × B) : (pr1 p, pr2 p) = p +-- := product_rec (λ x y, refl (x, y)) p + +-- inductive sum (A : Type) (B : Type) : Type := +-- | inl : A → sum A B +-- | inr : B → sum A B + +-- namespace logic +-- infixr `+`:25 := sum +-- end +-- using logic +-- infixr `∨`:25 := sum + +-- theorem sum_elim {a : Type} {b : Type} {c : Type} (H1 : a + b) (H2 : a → c) (H3 : b → c) : c +-- := sum_rec H2 H3 H1 + +-- theorem resolve_right {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ a) : b +-- := sum_elim H1 (assume Ha, absurd_elim b Ha H2) (assume Hb, Hb) + +-- theorem resolve_left {a : Type} {b : Type} (H1 : a + b) (H2 : ¬ b) : a +-- := sum_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2) + +-- theorem sum_flip {a : Type} {b : Type} (H : a + b) : b + a +-- := sum_elim H (assume Ha, inr b Ha) (assume Hb, inl a Hb) + +-- inductive Sigma {A : Type} (B : A → Type) : Type := +-- | sigma_intro : Π a, B a → Sigma B + +-- notation `Σ` binders `,` r:(scoped P, Sigma P) := r + +-- definition dpr1 {A : Type} {B : A → Type} (p : Σ x, B x) : A +-- := Sigma_rec (λ a b, a) p + +-- definition dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) +-- := Sigma_rec (λ a b, b) p diff --git a/library/hott/path_groupoids.lean b/library/hott/path_groupoids.lean new file mode 100644 index 000000000..9436a9da6 --- /dev/null +++ b/library/hott/path_groupoids.lean @@ -0,0 +1,922 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Jeremy Avigad +-- Ported from Coq HoTT + +import .logic .tactic + +using tactic + +-- Path +-- ---- + +inductive path {A : Type} (a : A) : A → Type := +| idpath : path a a + +infix `≈`:50 := path +notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right? +notation `idp`:max := idpath _ -- TODO: can we / should we use `1`? + +namespace path + abbreviation induction_on {A : Type} {a b : A} (p : a ≈ b) + {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p := + path_rec H p +end path + + +-- TODO: should all this be in namespace path? +using path + +-- Concatenation and inverse +-- ------------------------- + +definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z := +path_rec (λu, u) q p + +-- TODO: should this be an abbreviation? +definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x := +path_rec (idpath x) p + +infixl `@`:75 := concat +postfix `^`:100 := inverse + +-- In Coq, these are not needed, because concat and inv are kept transparent +definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp + +definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp + + +-- The 1-dimensional groupoid structure +-- ------------------------------------ + +-- The identity path is a right unit. +definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p @ idp ≈ p := +induction_on p idp + +-- The identity path is a right unit. +definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp @ p ≈ p := +induction_on p idp + +-- Concatenation is associative. +definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : + p @ (q @ r) ≈ (p @ q) @ r := +induction_on r (induction_on q idp) + +definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : + (p @ q) @ r ≈ p @ (q @ r) := +induction_on r (induction_on q idp) + +-- The left inverse law. +definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p @ p^ ≈ idp := +induction_on p idp + +-- The right inverse law. +definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ @ p ≈ idp := +induction_on p idp + + +-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat +-- redundant, following from earlier theorems. + +definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ @ (p @ q) ≈ q := +induction_on q (induction_on p idp) + +definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p @ (p^ @ q) ≈ q := +induction_on q (induction_on p idp) + +definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p @ q) @ q^ ≈ p := +induction_on q (induction_on p idp) + +definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p @ q^) @ q ≈ p := +induction_on q (take p, induction_on p idp) p + +-- Inverse distributes over concatenation +definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p @ q)^ ≈ q^ @ p^ := +induction_on q (induction_on p idp) + +definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ @ q)^ ≈ q^ @ p := +induction_on q (induction_on p idp) + +-- universe metavariables +definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p @ q^)^ ≈ q @ p^ := +induction_on p (λq, induction_on q idp) q + +definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ @ q^)^ ≈ q @ p := +induction_on p (induction_on q idp) + +-- Inverse is an involution. +definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p^^ ≈ p := +induction_on p idp + + +-- Theorems for moving things around in equations +-- ---------------------------------------------- + +definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + p ≈ (r^ @ q) → (r @ p) ≈ q := +have gen : Πp q, p ≈ (r^ @ q) → (r @ p) ≈ q, from + induction_on r + (take p q, + assume h : p ≈ idp^ @ q, + show idp @ p ≈ q, from concat_1p _ @ h @ concat_1p _), +gen p q + +definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + r ≈ q @ p^ → r @ p ≈ q := +induction_on p (take q r h, (concat_p1 _ @ h @ concat_p1 _)) q r + +definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : + p ≈ r @ q → r^ @ p ≈ q := +induction_on r (take p q h, concat_1p _ @ h @ concat_1p _) p q + +definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : + r ≈ q @ p → r @ p^ ≈ q := +induction_on p (take q r h, concat_p1 _ @ h @ concat_p1 _) q r + +definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + r^ @ q ≈ p → q ≈ r @ p := +induction_on r (take p q h, (concat_1p _)^ @ h @ (concat_1p _)^) p q + +definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + q @ p^ ≈ r → q ≈ r @ p := +induction_on p (take q r h, (concat_p1 _)^ @ h @ (concat_p1 _)^) q r + +definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : + r @ q ≈ p → q ≈ r^ @ p := +induction_on r (take p q h, (concat_1p _)^ @ h @ (concat_1p _)^) p q + +definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : + q @ p ≈ r → q ≈ r @ p^ := +induction_on p (take q r h, (concat_p1 _)^ @ h @ (concat_p1 _)^) q r + +definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) : + p @ q^ ≈ idp → p ≈ q := +induction_on q (take p h, (concat_p1 _)^ @ h) p + +definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) : + q^ @ p ≈ idp → p ≈ q := +induction_on q (take p h, (concat_1p _)^ @ h) p + +definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + p @ q ≈ idp → p ≈ q^ := +induction_on q (take p h, (concat_p1 _)^ @ h) p + +definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + q @ p ≈ idp → p ≈ q^ := +induction_on q (take p h, (concat_1p _)^ @ h) p + +definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) : + idp ≈ p^ @ q → p ≈ q := +induction_on p (take q h, h @ (concat_1p _)) q + +definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) : + idp ≈ q @ p^ → p ≈ q := +induction_on p (take q h, h @ (concat_p1 _)) q + +definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + idp ≈ q @ p → p^ ≈ q := +induction_on p (take q h, h @ (concat_p1 _)) q + +definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + idp ≈ p @ q → p^ ≈ q := +induction_on p (take q h, h @ (concat_1p _)) q + + +-- Transport +-- --------- + +-- keep transparent, so transport _ idp p is definitionally equal to p +abbreviation transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := +path.induction_on p u + +definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : transport _ idp u ≈ u := +idp + +-- This idiom makes the operation right associative. +notation p `#`:65 x:64 := transport _ p x + +definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y := +path.induction_on p idp + +-- TODO: is this better than an alias? Note use of curly brackets +abbreviation ap01 := ap + +abbreviation pointwise_paths {A : Type} {P : A → Type} (f g : Πx, P x) : Type := +Πx : A, f x ≈ g x + +infix `∼`:50 := pointwise_paths + +definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g := +λx, path.induction_on H idp + +definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H + +definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y := +induction_on H (induction_on p idp) + +definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y) : p # (f x) ≈ f y := +induction_on p idp + + +-- More theorems for moving things around in equations +-- --------------------------------------------------- + +definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : + u ≈ p^ # v → p # u ≈ v := +induction_on p (take u v, id) u v + +definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : + u ≈ p # v → p^ # u ≈ v := +induction_on p (take u v, id) u v + +definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : + p # u ≈ v → u ≈ p^ # v := +induction_on p (take u v, id) u v + +definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : + p^ # u ≈ v → u ≈ p # v := +induction_on p (take u v, id) u v + + +-- Functoriality of functions +-- -------------------------- + +-- Here we prove that functions behave like functors between groupoids, and that [ap] itself is +-- functorial. + +-- Functions take identity paths to identity paths +definition ap_1 {A B : Type} (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp + +definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp + +-- Functions commute with concatenation. +definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) : + ap f (p @ q) ≈ (ap f p) @ (ap f q) := +induction_on q (induction_on p idp) + +definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) : + r @ (ap f (p @ q)) ≈ (r @ ap f p) @ (ap f q) := +induction_on p (take r q, induction_on q (concat_p_pp r idp idp)) r q + +definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) : + (ap f (p @ q)) @ r ≈ (ap f p) @ (ap f q @ r) := +induction_on p (take q, induction_on q (take r, concat_pp_p _ _ _)) q r +-- induction_on p (take q : x ≈ z, induction_on q (take r : f x ≈ f w, concat_pp_p idp idp r)) q r + +-- TODO: can we do this proof using tactics? +-- proof +-- apply (induction_on p _ q r), +-- apply (take q, induction_on q _), +-- apply (concat_pp_p idp idp r) +-- qed + +-- proof +-- apply (induction_on p _ q r), +-- take q, proof +-- apply (induction_on q), +-- take r, +-- apply concat_pp_p +-- qed +-- qed + +-- Coq proof: +-- Proof. +-- destruct p, q. simpl. exact (concat_pp_p idp idp r). +-- Defined. + +-- Functions commute with path inverses. +definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)^ ≈ ap f (p^) := +induction_on p idp + +definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p^) ≈ (ap f p)^ := +induction_on p idp + +-- [ap] itself is functorial in the first argument. + +-- TODO: rename id to idmap? +definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p := +induction_on p idp + +definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : + ap (g ∘ f) p ≈ ap g (ap f p) := +induction_on p idp + +-- Sometimes we don't have the actual function [compose]. +definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : + ap (λa, g (f a)) p ≈ ap g (ap f p) := +induction_on p idp + +-- The action of constant maps. +definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) : + ap (λu, z) p ≈ idp := +induction_on p idp + +-- Naturality of [ap]. +definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) : + (ap f q) @ (p y) ≈ (p x) @ (ap g q) := +induction_on q (concat_1p _ @ (concat_p1 _)^) + +-- Naturality of [ap] at identity. +definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) : + (ap f q) @ (p y) ≈ (p x) @ q := +induction_on q (concat_1p _ @ (concat_p1 _)^) + +definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) : + (p x) @ (ap f q) ≈ q @ (p y) := +induction_on q (concat_p1 _ @ (concat_1p _)^) + +-- TODO: move these +calc_subst transport +calc_trans concat +calc_refl idpath + +-- Naturality with other paths hanging around. + +definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) + {x y : A} (q : x ≈ y) + {w z : B} (r : w ≈ f x) (s : g y ≈ z) : + (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (ap g q @ s) := +induction_on q (induction_on s + (calc + (r @ (ap f q)) @ ((p y) @ (idpath (g y))) ≈ (r @ (ap f q)) @ (p y) : {concat_p1 _} + ... ≈ r @ ((ap f q) @ (p y)) : concat_pp_p _ _ _ + ... ≈ r @ ((p x) @ (ap g q)) : {concat_Ap p q} + ... ≈ (r @ (p x)) @ ((ap g q)) : concat_p_pp _ _ _ + ... ≈ (r @ (p x)) @ ((ap g q) @ (idpath (g y))) : {concat_p1 _})) + +-- TODO: the Coq proof of the previous theorem is much shorter: +-- Proof. +-- destruct q, s; simpl. +-- repeat rewrite concat_p1. +-- reflexivity. +-- Defined. + +(-- TODO: These are similar + +definition concat_pA_p {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) + {x y : A} (q : x ≈ y) + {w : B} (r : w ≈ f x) + : + (r @ ap f q) @ p y ≈ (r @ p x) @ ap g q. +Proof. + destruct q; simpl. + repeat rewrite concat_p1. + reflexivity. +Defined. + +definition concat_A_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) + {x y : A} (q : x ≈ y) + {z : B} (s : g y ≈ z) + : + (ap f q) @ (p y @ s) ≈ (p x) @ (ap g q @ s). +Proof. + destruct q, s; simpl. + repeat rewrite concat_p1, concat_1p. + reflexivity. +Defined. + +definition concat_pA1_pp {A : Type} {f : A → A} (p : forall x, f x ≈ x) + {x y : A} (q : x ≈ y) + {w z : A} (r : w ≈ f x) (s : y ≈ z) + : + (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (q @ s). +Proof. + destruct q, s; simpl. + repeat rewrite concat_p1. + reflexivity. +Defined. + +definition concat_pp_A1p {A : Type} {g : A → A} (p : forall x, x ≈ g x) + {x y : A} (q : x ≈ y) + {w z : A} (r : w ≈ x) (s : g y ≈ z) + : + (r @ p x) @ (ap g q @ s) ≈ (r @ q) @ (p y @ s). +Proof. + destruct q, s; simpl. + repeat rewrite concat_p1. + reflexivity. +Defined. + +definition concat_pA1_p {A : Type} {f : A → A} (p : forall x, f x ≈ x) + {x y : A} (q : x ≈ y) + {w : A} (r : w ≈ f x) + : + (r @ ap f q) @ p y ≈ (r @ p x) @ q. +Proof. + destruct q; simpl. + repeat rewrite concat_p1. + reflexivity. +Defined. + +definition concat_A1_pp {A : Type} {f : A → A} (p : forall x, f x ≈ x) + {x y : A} (q : x ≈ y) + {z : A} (s : y ≈ z) + : + (ap f q) @ (p y @ s) ≈ (p x) @ (q @ s). +Proof. + destruct q, s; simpl. + repeat rewrite concat_p1, concat_1p. + reflexivity. +Defined. + +definition concat_pp_A1 {A : Type} {g : A → A} (p : forall x, x ≈ g x) + {x y : A} (q : x ≈ y) + {w : A} (r : w ≈ x) + : + (r @ p x) @ ap g q ≈ (r @ q) @ p y. +Proof. + destruct q; simpl. + repeat rewrite concat_p1. + reflexivity. +Defined. + +definition concat_p_A1p {A : Type} {g : A → A} (p : forall x, x ≈ g x) + {x y : A} (q : x ≈ y) + {z : A} (s : g y ≈ z) + : + p x @ (ap g q @ s) ≈ q @ (p y @ s). +Proof. + destruct q, s; simpl. + repeat rewrite concat_p1, concat_1p. + reflexivity. +Defined. +--) + + +-- Action of [apD10] and [ap10] on paths +-- ------------------------------------- + +-- Application of paths between functions preserves the groupoid structure + +definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f) x ≈ idp := idp + +definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : + apD10 (h @ h') x ≈ apD10 h x @ apD10 h' x := +induction_on h (take h', induction_on h' idp) h' + +definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) : + apD10 (h^) x ≈ (apD10 h x)^ := +induction_on h idp + +definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp + +definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : + ap10 (h @ h') x ≈ ap10 h x @ ap10 h' x := apD10_pp h h' x + +definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h^) x ≈ (ap10 h x)^ := apD10_V h x + +-- [ap10] also behaves nicely on paths produced by [ap] +definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) : + ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:= +induction_on p idp + + +-- Transport and the groupoid structure of paths +-- --------------------------------------------- + +-- TODO: move from above? +-- definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) +-- : idp # u ≈ u := idp + +definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) : + p @ q # u ≈ q # p # u := +induction_on q (induction_on p idp) + +definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : + p # p^ # z ≈ z := +(transport_pp P (p^) p z)^ @ ap (λr, transport P r z) (concat_Vp p) + +definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : + p^ # p # z ≈ z := +(transport_pp P p (p^) z)^ @ ap (λr, transport P r z) (concat_pV p) + + +----------------------------------------------- +-- TODO: Examples of difficult induction problems +----------------------------------------------- + +theorem double_induction + {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) + {C : Π(x y z : A), Π(p : x ≈ y), Π(q : y ≈ z), Type} + (H : C x x x (idpath x) (idpath x)) : + C x y z p q := +induction_on p (take z q, induction_on q H) z q + +theorem double_induction2 + {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) + {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type} + (H : C z z z (idpath z) (idpath z)) : + C x y z p q := +induction_on p (take y q, induction_on q H) y q + +theorem double_induction2' + {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) + {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type} + (H : C z z z (idpath z) (idpath z)) : C x y z p q := +induction_on p (take y q, induction_on q H) y q + +theorem triple_induction + {A : Type} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) + {C : Π(x y z w : A), Π(p : x ≈ y), Π(q : y ≈ z), Π(r: z ≈ w), Type} + (H : C x x x x (idpath x) (idpath x) (idpath x)) : + C x y z w p q r := +induction_on p (take z q, induction_on q (take w r, induction_on r H)) z q w r + +-- try this again +definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p @ q^) @ q ≈ p := +double_induction2 p q idp + +-- old proof: +-- induction_on q (take p, induction_on p idp) p + +-- This is an attempt to do it as a tactic proof +-- proof +-- apply (induction_on q _ p), +-- take p, +-- apply (induction_on p idp) +-- qed + +-- set_option unifier.max_steps 1000000 + +-- TODO: update: this no longer works, but it used to (it took a couple of seconds) + +-- theorem test {A : Type} (P : A → Type) (x : A) (u_1 : P x) : +-- path +-- (concat +-- (concat (ap (λ (e : path x x), transport P e u_1) (concat_p_pp (idpath x) (idpath x) (idpath x))) +-- (transport_pp P (concat (idpath x) (idpath x)) (idpath x) u_1)) +-- (ap (transport P (idpath x)) (transport_pp P (idpath x) (idpath x) u_1))) +-- (concat (transport_pp P (idpath x) (concat (idpath x) (idpath x)) u_1) +-- (transport_pp P (idpath x) (idpath x) (transport P (idpath x) u_1))) := +-- idp + +-- definition transport_p_pp {A : Type} (P : A → Type) +-- {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : +-- ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ +-- ap (transport P r) (transport_pp P p q u) +-- ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u)) +-- :> ((p @ (q @ r)) # u ≈ r # q # p # u) := +-- triple_induction p q r _ u +-- triple_induction p q r (take u, test P x u) u + +-- this doesn't work, even with max_steps = 100000 +--double_induction p q (take r, induction_on r (take u, test P x u))) r u + +-- even this doesn't work! +-- definition transport_p_pp' {A : Type} (P : A → Type) +-- {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : +-- ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ +-- ap (transport P r) (transport_pp P p q u) +-- ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u)) +-- :> ((p @ (q @ r)) # u ≈ r # q # p # u) := +-- have aux: +-- Πu_1 : P x, path +-- (concat +-- (concat (ap (λ (e : path x x), transport' e u_1) (concat_p_pp (idpath x) (idpath x) (idpath x))) +-- (transport_pp P (concat (idpath x) (idpath x)) (idpath x) u_1)) +-- (ap (transport P (idpath x)) (transport_pp P (idpath x) (idpath x) u_1))) +-- (concat (transport_pp P (idpath x) (concat (idpath x) (idpath x)) u_1) +-- (transport_pp P (idpath x) (idpath x) (transport' (idpath x) u_1))), from take u_1, idp, +-- triple_induction p q r (take u, aux u) u + +-- This works with max_steps = 10000 +-- definition transport_p_pp {A : Type} (P : A → Type) +-- {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : +-- ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ +-- ap (transport P r) (transport_pp P p q u) +-- ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u)) +-- :> ((p @ (q @ r)) # u ≈ r # q # p # u) := +-- induction_on p (take q, induction_on q (take r, induction_on r (take u, test P x u))) q r u + +-- This shows the goal, with max_steps = 100000 +-- definition transport_p_pp {A : Type} (P : A → Type) +-- {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : +-- ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ +-- ap (transport P r) (transport_pp P p q u) +-- ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u)) +-- :> ((p @ (q @ r)) # u ≈ r # q # p # u) := +-- induction_on p (take q, induction_on q (take r, induction_on r (take u, _)))) q r u + + + +-- Back to the regular development + +-- In the future, we may expect to need some higher coherence for transport: +-- for instance, that transport acting on the associator is trivial. + +-- set_option unifier.max_steps 1000000 + +-- TODO: we cannot get this yet +-- in Coq, the type annotation is only for clarity -- it is not needed +definition transport_p_pp {A : Type} (P : A → Type) + {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : + ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ + ap (transport P r) (transport_pp P p q u) + ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u)) + :> ((p @ (q @ r)) # u ≈ r # q # p # u) := +sorry + +(-- Coq proof: +Proof. + destruct p, q, r. simpl. exact 1. +Defined. +--) + +-- Here is another coherence lemma for transport. +definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : + transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) +:= induction_on p idp + +-- Dependent transport in a doubly dependent type. +definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type) + {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) : + C x2 (p # y) := +induction_on p z + +-- Transporting along higher-dimensional paths +definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : + p # z ≈ q # z := ap (λp', p' # z) r + +-- An alternative definition. +definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) + (z : Q x) : + transport2 Q r z ≈ ap10 (ap (transport Q) r) z := +induction_on r idp + +definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y} + (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : + transport2 P (r1 @ r2) z ≈ transport2 P r1 z @ transport2 P r2 z := +induction_on r1 (induction_on r2 idp) + +definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : + transport2 Q (r^) z ≈ ((transport2 Q r z)^) := +induction_on r idp + +definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) + (s : z ≈ w) : + ap (transport P p) s @ transport2 P r w ≈ transport2 P r z @ ap (transport P q) s := +induction_on r (concat_p1 _ @ (concat_1p _)^) + +-- TODO (from Coq library): What should this be called? +definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) : + f y (p # z) ≈ (p # (f x z)) := +induction_on p idp + + +-- Transporting in particular fibrations +-- ------------------------------------- + +(-- From the Coq HoTT library: + +One frequently needs lemmas showing that transport in a certain dependent type is equal to some +more explicitly defined operation, defined according to the structure of that dependent type. +For most dependent types, we prove these lemmas in the appropriate file in the types/ +subdirectory. Here we consider only the most basic cases. + +--) + +-- Transporting in a constant fibration. +definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) : + transport (λx, B) p y ≈ y := +induction_on p idp + +definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) : + transport_const p y ≈ transport2 (λu, B) r y @ transport_const q y := +induction_on r (concat_1p _)^ + +-- Transporting in a pulled back fibration. +definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) : + transport (λx, P (f x)) p z ≈ transport P (ap f p) z := +induction_on p idp + +definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') : + transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p := +induction_on p idp + +definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) : + apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) := +induction_on p idp + +definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : + apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) := +induction_on p idp + +-- A special case of [transport_compose] which seems to come up a lot. +definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) : + transport P p u ≈ transport (λz, z) (ap P p) u := +induction_on p idp + + +-- The behavior of [ap] and [apD] +-- ------------------------------ + +-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. +definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) : + apD f p ≈ transport_const p (f x) @ ap f p := +induction_on p idp + + +-- The 2-dimensional groupoid structure +-- ------------------------------------ + +-- Horizontal composition of 2-dimensional paths. +definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : + p @ q ≈ p' @ q' := +induction_on h (induction_on h' idp) + +infixl `@@`:75 := concat2 + +-- 2-dimensional path inversion +definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p^ ≈ q^ := +induction_on h idp + + +-- Whiskering +-- ---------- + +definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p @ q ≈ p @ r := +idp @@ h + +definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p @ r ≈ q @ r := +h @@ idp + +-- Unwhiskering, a.k.a. cancelling + +definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p @ q ≈ p @ r) → (q ≈ r) := +induction_on p (take r, induction_on r (take q a, (concat_1p q)^ @ a)) r q + +definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p @ r ≈ q @ r) → (p ≈ q) := +induction_on r (take p, induction_on p (take q a, a @ concat_p1 q)) p q + +-- Whiskering and identity paths. + +definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + (concat_p1 p)^ @ whiskerR h idp @ concat_p1 q ≈ h := +induction_on h (induction_on p idp) + +definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + whiskerR idp q ≈ idp :> (p @ q ≈ p @ q) := +induction_on q idp + +definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + whiskerL p idp ≈ idp :> (p @ q ≈ p @ q) := +induction_on q idp + +definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + (concat_1p p) ^ @ whiskerL idp h @ concat_1p q ≈ h := +induction_on h (induction_on p idp) + +definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + h @@ idp ≈ whiskerR h idp :> (p @ idp ≈ q @ idp) := +induction_on h idp + +definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + idp @@ h ≈ whiskerL idp h :> (idp @ p ≈ idp @ q) := +induction_on h idp + +-- TODO: note, 4 inductions +-- The interchange law for concatenation. +definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z} + (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') : + (a @@ c) @ (b @@ d) ≈ (a @ b) @@ (c @ d) := +induction_on d (induction_on c (induction_on b (induction_on a idp))) + +definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : + (whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') := +induction_on b (induction_on a (concat_1p _)^) + +-- Structure corresponding to the coherence equations of a bicategory. + +-- The "pentagonator": the 3-cell witnessing the associativity pentagon. +definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) : + whiskerL p (concat_p_pp q r s) + @ concat_p_pp p (q @ r) s + @ whiskerR (concat_p_pp p q r) s + ≈ concat_p_pp p q (r @ s) @ concat_p_pp (p @ q) r s := +sorry +-- induction_on p (induction_on q (induction_on r (induction_on s idp))) + +(-- The Coq proof: + +-- The "pentagonator": the 3-cell witnessing the associativity pentagon. +definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) + : whiskerL p (concat_p_pp q r s) + @ concat_p_pp p (q@r) s + @ whiskerR (concat_p_pp p q r) s + ≈ concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s. +Proof. + case p, q, r, s. reflexivity. +Defined. + +--) + +-- The 3-cell witnessing the left unit triangle. +definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + concat_p_pp p idp q @ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) := +induction_on p (take q, induction_on q idp) q + +definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p @ q ≈ q @ p := + (whiskerR_p1 p @@ whiskerL_1p q)^ + @ (concat_p1 _ @@ concat_p1 _) + @ (concat_1p _ @@ concat_1p _) + @ (concat_whisker _ _ _ _ p q) + @ (concat_1p _ @@ concat_1p _)^ + @ (concat_p1 _ @@ concat_p1 _)^ + @ (whiskerL_1p q @@ whiskerR_p1 p) + + +-- The action of functions on 2-dimensional paths +definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q := +induction_on r idp + +definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') : + ap02 f (r @ r') ≈ ap02 f r @ ap02 f r' := +induction_on r (induction_on r' idp) + +definition ap02_p2p {A B} (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') + (s : q ≈ q') : + ap02 f (r @@ s) ≈ ap_pp f p q + @ (ap02 f r @@ ap02 f s) + @ (ap_pp f p' q')^ := +sorry +-- induction_on r (induction_on s (induction_on p (induction_on q idp))) + +definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) : + apD f p ≈ transport2 B r (f x) @ apD f q := +induction_on r (concat_1p _)^ + +-- And now for a lemma whose statement is much longer than its proof. +definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A} + {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) : + apD02 f (r1 @ r2) ≈ apD02 f r1 + @ whiskerL (transport2 B r1 (f x)) (apD02 f r2) + @ concat_p_pp _ _ _ + @ (whiskerR ((transport2_p2p B r1 r2 (f x))^) (apD f p3)) := +sorry +-- induction_on r1 (take r2, induction_on r2 (take p1, induction_on p1 idp)) r2 p1 + +(-- + +The Coq proof: +definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A} + {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) + : apD02 f (r1 @ r2) + ≈ apD02 f r1 + @ whiskerL (transport2 B r1 (f x)) (apD02 f r2) + @ concat_p_pp _ _ _ + @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)). +Proof. + destruct r1, r2. destruct p1. reflexivity. +Defined. + +--) + +(-- +-- ** Tactics, hints, and aliases + +-- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required. +Notation concatR := (λp q, concat q p). + +Hint Resolve + concat_1p concat_p1 concat_p_pp + inv_pp inv_V + : path_hints. + +(* First try at a paths db +We want the RHS of the equation to become strictly simpler +Hint Rewrite +@concat_p1 +@concat_1p +@concat_p_pp (* there is a choice here !*) +@concat_pV +@concat_Vp +@concat_V_pp +@concat_p_Vp +@concat_pp_V +@concat_pV_p +(*@inv_pp*) (* I am not sure about this one +@inv_V +@moveR_Mp +@moveR_pM +@moveL_Mp +@moveL_pM +@moveL_1M +@moveL_M1 +@moveR_M1 +@moveR_1M +@ap_1 +(* @ap_pp +@ap_p_pp ?*) +@inverse_ap +@ap_idmap +(* @ap_compose +@ap_compose'*) +@ap_const +(* Unsure about naturality of [ap], was absent in the old implementation*) +@apD10_1 +:paths. + +Ltac hott_simpl := + autorewrite with paths in * |- * ; auto with path_hints. + +--) \ No newline at end of file