michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/hott): begin porting Coq HoTT

Browse source
This commit is contained in:
Jeremy Avigad 2014-08-06 18:21:54 -07:00 committed by Leonardo de Moura
parent 0ea2d287e1
commit 218c9dfc81
2 changed files with 1191 additions and 169 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

438
library/hott/logic.lean
View file

@ -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

922
library/hott/path_groupoids.lean Normal file
View file

@ -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.
--)