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

chore(hott) fix init

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-12 13:17:50 -05:00 committed by Leonardo de Moura
parent dae2aeb605
commit a02cc1aff9
21 changed files with 612 additions and 570 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
hott/algebra/binary.hlean
View file

@ -8,8 +8,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
General properties of binary operations.
-/
import hott.path
open path
open eq
namespace path_binary
section
@ -20,26 +19,26 @@ namespace path_binary
notation [local] a ⁻¹ := inv a
notation [local] 1 := one
definition commutative := ∀a b, a*b ≈ b*a
definition associative := ∀a b c, (a*b)*c ≈ a*(b*c)
definition left_identity := ∀a, 1 * a ≈ a
definition right_identity := ∀a, a * 1 ≈ a
definition left_inverse := ∀a, a⁻¹ * a ≈ 1
definition right_inverse := ∀a, a * a⁻¹ ≈ 1
definition left_cancelative := ∀a b c, a * b ≈ a * c → b ≈ c
definition right_cancelative := ∀a b c, a * b ≈ c * b → a ≈ c
definition commutative := ∀a b, a*b = b*a
definition associative := ∀a b c, (a*b)*c = a*(b*c)
definition left_identity := ∀a, 1 * a = a
definition right_identity := ∀a, a * 1 = a
definition left_inverse := ∀a, a⁻¹ * a = 1
definition right_inverse := ∀a, a * a⁻¹ = 1
definition left_cancelative := ∀a b c, a * b = a * c → b = c
definition right_cancelative := ∀a b c, a * b = c * b → a = c
definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) ≈ b
definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) ≈ b
definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b ≈ a
definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ ≈ a
definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b
definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b
definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b = a
definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a
variable (op₂ : A → A → A)
notation [local] a + b := op₂ a b
definition left_distributive := ∀a b c, a * (b + c) ≈ a * b + a * c
definition right_distributive := ∀a b c, (a + b) * c ≈ a * c + b * c
definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
end
context
@ -48,17 +47,17 @@ namespace path_binary
variable H_comm : commutative f
variable H_assoc : associative f
infixl `*` := f
theorem left_comm : ∀a b c, a*(b*c) ≈ b*(a*c) :=
theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) :=
take a b c, calc
a*(b*c) ≈ (a*b)*c : H_assoc
... ≈ (b*a)*c : H_comm
... ≈ b*(a*c) : H_assoc
a*(b*c) = (a*b)*c : H_assoc
... = (b*a)*c : H_comm
... = b*(a*c) : H_assoc
theorem right_comm : ∀a b c, (a*b)*c ≈ (a*c)*b :=
theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b :=
take a b c, calc
(a*b)*c ≈ a*(b*c) : H_assoc
... ≈ a*(c*b) : H_comm
... ≈ (a*c)*b : H_assoc
(a*b)*c = a*(b*c) : H_assoc
... = a*(c*b) : H_comm
... = (a*c)*b : H_assoc
end
context
@ -66,10 +65,10 @@ namespace path_binary
variable {f : A → A → A}
variable H_assoc : associative f
infixl `*` := f
theorem assoc4helper (a b c d) : (a*b)*(c*d) ≈ a*((b*c)*d) :=
theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
calc
(a*b)*(c*d) ≈ a*(b*(c*d)) : H_assoc
... ≈ a*((b*c)*d) : H_assoc
(a*b)*(c*d) = a*(b*(c*d)) : H_assoc
... = a*((b*c)*d) : H_assoc
end
end path_binary

4
hott/algebra/relation.hlean
View file

@ -94,14 +94,14 @@ namespace is_congruence
is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
theorem const {T2 : Type} (R2 : T2 → T2 → Type) (H : relation.reflexive R2)
⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
⦃T1 : Type⦄ (R1 : T1 → T1 → Type) (c : T2) :
is_congruence R1 R2 (λu : T1, c) :=
is_congruence.mk (λx y H1, H c)
end is_congruence
theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Type)
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
[C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Type) (c : T2) :
is_congruence R1 R2 (λu : T1, c) :=
is_congruence.const R2 (is_reflexive.refl R2) R1 c

4
hott/default.hlean
View file

@ -1,10 +1,8 @@
-- Copyright (c) 2014 Jeremy Avigad. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
-- Author: Jeremy Avigad, Jakob von Raumer
-- hott.default
-- ============
-- A library for homotopy type theory
import ..standard .path .equiv .trunc .fibrant

24
hott/equiv_precomp.hlean
View file

@ -2,8 +2,8 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.equiv hott.axioms.funext
open path function funext
import init.equiv init.axioms.funext
open eq function funext
namespace is_equiv
context
@ -34,12 +34,12 @@ namespace is_equiv
--the domain or the codomain.
protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type)
(Ceq : is_equiv (precomp f C)) (Deq : is_equiv (precomp f D)) (k : C → D) (h : A → C) :
k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) :=
k ∘ (inv (precomp f C)) h = (inv (precomp f D)) (k ∘ h) :=
let invD := inv (precomp f D) in
let invC := inv (precomp f C) in
have eq1 : invD (k ∘ h) ≈ k ∘ (invC h),
from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
... ≈ k ∘ (invC h) : !sect,
have eq1 : invD (k ∘ h) = k ∘ (invC h),
from calc invD (k ∘ h) = invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h
... = k ∘ (invC h) : !sect,
eq1⁻¹
definition from_isequiv_precomp {A B : Type} (f : A → B) (Aeq : is_equiv (precomp f A))
@ -47,14 +47,14 @@ namespace is_equiv
let invA := inv (precomp f A) in
let invB := inv (precomp f B) in
let sect' : f ∘ (invA id) ∼ id := (λx,
calc f (invA id x) ≈ (f ∘ invA id) x : idp
... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
... ≈ invB (precomp f B id) x : idp
... ≈ x : apD10 (sect (precomp f B) id))
calc f (invA id x) = (f ∘ invA id) x : idp
... = invB (f ∘ id) x : apD10 (!isequiv_precompose_eq)
... = invB (precomp f B id) x : idp
... = x : apD10 (sect (precomp f B) id))
in
let retr' : (invA id) ∘ f ∼ id := (λx,
calc invA id (f x) ≈ precomp f A (invA id) x : idp
... ≈ x : apD10 (retr (precomp f A) id)) in
calc invA id (f x) = precomp f A (invA id) x : idp
... = x : apD10 (retr (precomp f A) id)) in
adjointify f (invA id) sect' retr'
end

10
hott/axioms/funext.hlean → hott/init/axioms/funext.hlean
View file

@ -2,9 +2,9 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad, Jakob von Raumer
-- Ported from Coq HoTT
import hott.path hott.equiv
open path
prelude
import ..path ..equiv
open eq
-- Funext
-- ------
@ -23,12 +23,12 @@ namespace funext
protected definition ap [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) :=
rec_on F (λ(H : Π A P f g, _), !H)
definition path_pi {f g : Π x, P x} : f ∼ g → f ≈ g :=
definition path_pi {f g : Π x, P x} : f ∼ g → f = g :=
is_equiv.inv (@apD10 A P f g)
omit F
definition path_pi2 [F : funext] {A B : Type} {P : A → B → Type}
(f g : Πx y, P x y) : (Πx y, f x y ≈ g x y) → f ≈ g :=
(f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g :=
λ E, path_pi (λx, path_pi (E x))
end funext

57
hott/init/funext_from_ua.hlean → hott/init/axioms/funext_from_ua.hlean
View file

@ -2,10 +2,11 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.equiv hott.funext_varieties hott.axioms.ua hott.axioms.funext
import data.prod data.sigma data.unit
prelude
import ..equiv ..datatypes
import .funext_varieties .ua .funext
open path function prod sigma truncation equiv is_equiv unit ua_type
open eq function prod sigma truncation equiv is_equiv unit ua_type
context
universe variables l
@ -14,38 +15,38 @@ context
protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type}
{w : A → B} {H0 : is_equiv w} : is_equiv (@compose C A B w) :=
let w' := equiv.mk w H0 in
let eqinv : A ≈ B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
let eqinv : A = B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in
let eq' := equiv_path eqinv in
is_equiv.adjointify (@compose C A B w)
(@compose C B A (is_equiv.inv w))
(λ (x : C → B),
have eqretr : eq' ≈ w',
have eqretr : eq' = w',
from (@retr _ _ (@equiv_path A B) (@ua_type.inst UA A B) w'),
have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹,
from inv_eq eq' w' eqretr,
have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
from (λ p,
(@path.rec_on Type.{l+1} A
(@eq.rec_on Type.{l+1} A
(λ B' p', Π (x' : C → B'), (to_fun (equiv_path p'))
∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') ≈ x')
∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') = x')
B p (λ x', idp))
) eqinv x,
have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x,
have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
from eqretr ▹ eqfin,
have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) ≈ x,
have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) = x,
from invs_eq ▹ eqfin',
eqfin''
)
(λ (x : C → A),
have eqretr : eq' ≈ w',
have eqretr : eq' = w',
from (@retr _ _ (@equiv_path A B) ua_type.inst w'),
have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹,
have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹,
from inv_eq eq' w' eqretr,
have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) ≈ x,
from (λ p, path.rec_on p idp) eqinv,
have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) = x,
from (λ p, eq.rec_on p idp) eqinv,
have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) = x,
from eqretr ▹ eqfin,
have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x,
have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) = x,
from invs_eq ▹ eqfin',
eqfin''
)
@ -53,7 +54,7 @@ context
-- We are ready to prove functional extensionality,
-- starting with the naive non-dependent version.
protected definition diagonal [reducible] (B : Type) : Type
:= Σ xy : B × B, pr₁ xy ≈ pr₂ xy
:= Σ xy : B × B, pr₁ xy = pr₂ xy
protected definition isequiv_src_compose {A B : Type}
: @is_equiv (A → diagonal B)
@ -64,7 +65,7 @@ context
(λ x, dpair (x , x) idp) (λx, idp)
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
(λ b c p, path.rec_on p idp))))
(λ b c p, eq.rec_on p idp))))
protected definition isequiv_tgt_compose {A B : Type}
: @is_equiv (A → diagonal B)
@ -75,10 +76,10 @@ context
(λ x, dpair (x , x) idp) (λx, idp)
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
(λ b c p, path.rec_on p idp))))
(λ b c p, eq.rec_on p idp))))
theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}}
: Π {f g : A → B}, f ∼ g → f ≈ g :=
: Π {f g : A → B}, f ∼ g → f = g :=
(λ (f g : A → B) (p : f ∼ g),
let d := λ (x : A), dpair (f x , f x) idp in
let e := λ (x : A), dpair (f x , g x) (p x) in
@ -88,13 +89,13 @@ context
have equiv2 [visible] : Π x y, is_equiv (ap precomp1),
from is_equiv.ap_closed precomp1,
have H' : Π (x y : A → diagonal B),
pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y,
pr₁ ∘ dpr1 ∘ x = pr₁ ∘ dpr1 ∘ y → x = y,
from (λ x y, is_equiv.inv (ap precomp1)),
have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e,
have eq2 : pr₁ ∘ dpr1 ∘ d = pr₁ ∘ dpr1 ∘ e,
from idp,
have eq0 : d ≈ e,
have eq0 : d = e,
from H' d e eq2,
have eq1 : (pr₂ ∘ dpr1) ∘ d ≈ (pr₂ ∘ dpr1) ∘ e,
have eq1 : (pr₂ ∘ dpr1) ∘ d = (pr₂ ∘ dpr1) ∘ e,
from ap _ eq0,
eq1
)
@ -109,10 +110,10 @@ theorem weak_funext_from_ua [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_f
let U := (λ (x : A), unit) in
have pequiv : Π (x : A), P x ≃ U x,
from (λ x, @equiv_contr_unit(P x) (allcontr x)),
have psim : Π (x : A), P x ≈ U x,
have psim : Π (x : A), P x = U x,
from (λ x, @is_equiv.inv _ _
equiv_path ua_type.inst (pequiv x)),
have p : P ≈ U,
have p : P = U,
from @nondep_funext_from_ua _ A Type P U psim,
have tU' : is_contr (A → unit),
from is_contr.mk (λ x, ⋆)
@ -121,7 +122,7 @@ theorem weak_funext_from_ua [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_f
have tU : is_contr (Π x, U x),
from tU',
have tlast : is_contr (Πx, P x),
from path.transport _ (p⁻¹) tU,
from eq.transport _ (p⁻¹) tU,
tlast
)

36
hott/init/funext_varieties.hlean → hott/init/axioms/funext_varieties.hlean
View file

@ -2,9 +2,9 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jakob von Raumer
-- Ported from Coq HoTT
import hott.path hott.trunc hott.equiv hott.axioms.funext
import ..path ..trunc ..equiv .funext
open path truncation sigma function
open eq truncation sigma function
/- In hott.axioms.funext, we defined function extensionality to be the assertion
that the map apD10 is an equivalence. We now prove that this follows
@ -17,7 +17,7 @@ open path truncation sigma function
-- Naive funext is the simple assertion that pointwise equal functions are equal.
-- TODO think about universe levels
definition naive_funext :=
Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g
Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
-- Weak funext says that a product of contractible types is contractible.
definition weak_funext.{l k} :=
@ -39,7 +39,7 @@ definition weak_funext_from_naive_funext : naive_funext → weak_funext :=
is_contr.mk c (λ f,
have eq' : (λx, center (P x)) ∼ f,
from (λx, contr (f x)),
have eq : (λx, center (P x)) ≈ f,
have eq : (λx, center (P x)) = f,
from nf A P (λx, center (P x)) f eq',
eq
)
@ -60,19 +60,19 @@ context
is_contr.mk (dpair f idhtpy)
(λ dp, sigma.rec_on dp
(λ (g : Π x, B x) (h : f ∼ g),
let r := λ (k : Π x, Σ y, f x ≈ y),
let r := λ (k : Π x, Σ y, f x = y),
@dpair _ (λg, f ∼ g)
(λx, dpr1 (k x)) (λx, dpr2 (k x)) in
let s := λ g h x, @dpair _ (λy, f x ≈ y) (g x) (h x) in
have t1 : Πx, is_contr (Σ y, f x ≈ y),
let s := λ g h x, @dpair _ (λy, f x = y) (g x) (h x) in
have t1 : Πx, is_contr (Σ y, f x = y),
from (λx, !contr_basedpaths),
have t2 : is_contr (Πx, Σ y, f x ≈ y),
have t2 : is_contr (Πx, Σ y, f x = y),
from !wf,
have t3 : (λ x, @dpair _ (λ y, f x ≈ y) (f x) idp) ≈ s g h,
from @path_contr (Π x, Σ y, f x ≈ y) t2 _ _,
have t4 : r (λ x, dpair (f x) idp) ≈ r (s g h),
have t3 : (λ x, @dpair _ (λ y, f x = y) (f x) idp) = s g h,
from @path_contr (Π x, Σ y, f x = y) t2 _ _,
have t4 : r (λ x, dpair (f x) idp) = r (s g h),
from ap r t3,
have endt : dpair f idhtpy ≈ dpair g h,
have endt : dpair f idhtpy = dpair g h,
from t4,
endt
)
@ -84,7 +84,7 @@ context
@transport _ (λ gh, Q (dpr1 gh) (dpr2 gh)) (dpair f idhtpy) (dpair g h)
(@path_contr _ contr_basedhtpy _ _) d
definition htpy_ind_beta : htpy_ind f idhtpy ≈ d :=
definition htpy_ind_beta : htpy_ind f idhtpy = d :=
(@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp
end
@ -94,16 +94,16 @@ universe variables l k
theorem funext_from_weak_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+1} :=
funext.mk (λ A B f g,
let eq_to_f := (λ g' x, f ≈ g') in
let eq_to_f := (λ g' x, f = g') in
let sim2path := htpy_ind _ f eq_to_f idp in
have t1 : sim2path f (idhtpy f) ≈ idp,
have t1 : sim2path f (idhtpy f) = idp,
proof htpy_ind_beta _ f eq_to_f idp qed,
have t2 : apD10 (sim2path f (idhtpy f)) ≈ (idhtpy f),
have t2 : apD10 (sim2path f (idhtpy f)) = (idhtpy f),
proof ap apD10 t1 qed,
have sect : apD10 ∘ (sim2path g) ∼ id,
proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed,
proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) = x) t2) g qed,
have retr : (sim2path g) ∘ apD10 ∼ id,
from (λ h, path.rec_on h (htpy_ind_beta _ f _ idp)),
from (λ h, eq.rec_on h (htpy_ind_beta _ f _ idp)),
is_equiv.adjointify apD10 (sim2path g) sect retr)
definition funext_from_naive_funext : naive_funext -> funext :=

13
hott/init/ua.hlean → hott/init/axioms/ua.hlean
View file

@ -2,18 +2,19 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.path hott.equiv
open path equiv
prelude
import ..path ..equiv
open eq equiv
--Ensure that the types compared are in the same universe
section
universe variable l
variables {A B : Type.{l}}
definition isequiv_path (H : A ≈ B) :=
definition isequiv_path (H : A = B) :=
(@is_equiv.transport Type (λX, X) A B H)
definition equiv_path (H : A ≈ B) : A ≃ B :=
definition equiv_path (H : A = B) : A ≃ B :=
equiv.mk _ (isequiv_path H)
end
@ -32,7 +33,7 @@ namespace ua_type
rec_on F (λ H, H A B)
-- This is the version of univalence axiom we will probably use most often
definition ua : A ≃ B → A ≈ B :=
definition ua : A ≃ B → A = B :=
@is_equiv.inv _ _ (@equiv_path A B) inst
end
@ -45,7 +46,7 @@ namespace Equiv
protected definition subst [UA : ua_type] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
: P A → P B :=
path.transport P (ua_type.ua H)
eq.transport P (ua_type.ua H)
-- We can use this for calculation evironments
calc_subst subst

10
hott/init/datatypes.hlean
View file

@ -2,7 +2,7 @@
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Authors: Leonardo de Moura, Jakob von Raumer
Basic datatypes
-/
@ -17,7 +17,13 @@ notation `Type₃` := Type.{3}
inductive unit.{l} : Type.{l} :=
star : unit
inductive empty : Type
namespace unit
notation `⋆` := star
end unit
inductive empty.{l} : Type.{l}
inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
refl : eq a a

5
hott/init/default.hlean
View file

@ -6,5 +6,6 @@ Authors: Leonardo de Moura
-/
prelude
import init.datatypes init.reserved_notation init.tactic init.logic
import init.bool init.num init.priority init.relation init.wf init.prod
import init.sigma
import init.bool init.num init.priority init.relation init.wf
import init.types.sigma init.types.prod
import init.trunc init.path init.equiv

117
hott/init/equiv.hlean
View file

@ -2,8 +2,9 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad, Jakob von Raumer
-- Ported from Coq HoTT
import .path
open path function
prelude
import .path .function
open eq function
-- Equivalences
-- ------------
@ -14,7 +15,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) :=
(inv : B → A)
(retr : (f ∘ inv) ∼ id)
(sect : (inv ∘ f) ∼ id)
(adj : Πx, retr (f x) ≈ ap f (sect x))
(adj : Πx, retr (f x) = ap f (sect x))
-- A more bundled version of equivalence to calculate with
@ -47,8 +48,8 @@ namespace is_equiv
)
-- Any function equal to an equivalence is an equivlance as well.
definition path_closed [Hf : is_equiv f] (Heq : f ≈ f') : (is_equiv f') :=
path.rec_on Heq Hf
definition path_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') :=
eq.rec_on Heq Hf
-- Any function pointwise equal to an equivalence is an equivalence as well.
definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
@ -60,26 +61,26 @@ namespace is_equiv
let secta := sect f a in
let retrfa := retr f (f a) in
let retrf'a := retr f (f' a) in
have eq1 : _ ≈ _,
have eq1 : _ = _,
from calc ap f secta ⬝ ff'a
≈ retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _)
... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p
... ≈ ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f,
have eq2 : _ ≈ _,
= retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _)
... = ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p
... = ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f,
have eq2 : _ = _,
from calc retrf'a
≈ (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹)
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a
... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap
... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p
... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V
... ≈ (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap
... ≈ (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V
... ≈ Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p,
have eq3 : _ ≈ _,
= (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹)
... = ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a
... = ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap
... = (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p
... = (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V
... = (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap
... = (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V
... = Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p,
have eq3 : _ = _,
from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
≈ (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2
... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V
... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp,
= (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2
... = (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V
... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp,
eq3) in
is_equiv.mk (inv f) sect' retr' adj'
end is_equiv
@ -92,34 +93,34 @@ namespace is_equiv
definition adjointify_sect' : g ∘ f ∼ id :=
(λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)
definition adjointify_adj' : Π (x : A), ret (f x) ≈ ap f (adjointify_sect' x) :=
definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) :=
(λ (a : A),
let fgretrfa := ap f (ap g (ret (f a))) in
let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in
let fgfa := f (g (f a)) in
let retrfa := ret (f a) in
have eq1 : ap f (sec a) ≈ _,
have eq1 : ap f (sec a) = _,
from calc ap f (sec a)
≈ idp ⬝ ap f (sec a) : !concat_1p⁻¹
... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV
... ≈ ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
... ≈ ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
... ≈ (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,
have eq2 : ap f (sec a) ⬝ idp ≈ (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
= idp ⬝ ap f (sec a) : !concat_1p⁻¹
... = (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV
... = ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
... = ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
... = (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,
have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
from !concat_p1 ⬝ eq1,
have eq3 : idp ≈ _,
have eq3 : idp = _,
from calc idp
≈ (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2
... ≈ (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp
... ≈ (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹}
... ≈ ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp
... ≈ ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
... ≈ ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
... ≈ (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹}
... ≈ retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹}
... ≈ retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹
... ≈ retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹},
have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
= (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2
... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp
... = (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹}
... = ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp
... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹}
... = retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹}
... = retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹
... = retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹},
have eq4 : ret (f a) = ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
from moveR_M1 _ _ eq3,
eq4)
@ -153,16 +154,16 @@ namespace is_equiv
@homotopy_closed _ _ _ _ (compose (f ∘ g) (f⁻¹)) (λa, sect f (g a))
--Rewrite rules
definition moveR_M {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) :=
definition moveR_M {x : A} {y : B} (p : x = (inv f) y) : (f x = y) :=
(ap f p) ⬝ (@retr _ _ f _ y)
definition moveL_M {x : A} {y : B} (p : (inv f) y ≈ x) : (y ≈ f x) :=
definition moveL_M {x : A} {y : B} (p : (inv f) y = x) : (y = f x) :=
(moveR_M f (p⁻¹))⁻¹
definition moveR_V {x : B} {y : A} (p : x ≈ f y) : (inv f) x ≈ y :=
definition moveR_V {x : B} {y : A} (p : x = f y) : (inv f) x = y :=
ap (f⁻¹) p ⬝ sect f y
definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x :=
definition moveL_V {x : B} {y : A} (p : f y = x) : y = (inv f) x :=
(moveR_V f (p⁻¹))⁻¹
definition ap_closed [instance] (x y : A) : is_equiv (ap f) :=
@ -191,20 +192,20 @@ namespace is_equiv
definition equiv_rect (P : B -> Type) :
(Πx, P (f x)) → (Πy, P y) :=
(λg y, path.transport _ (retr f y) (g (f⁻¹ y)))
(λg y, eq.transport _ (retr f y) (g (f⁻¹ y)))
definition equiv_rect_comp (P : B → Type)
(df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) ≈ df x :=
(df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
calc equiv_rect f P df (f x)
≈ transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
... ≈ transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
... ≈ transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
... ≈ df x : apD df (sect f x)
= transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
... = transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
... = transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
... = df x : apD df (sect f x)
end
--Transporting is an equivalence
protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (is_equiv (transport P p)) :=
protected definition transport [instance] (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
is_equiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
end is_equiv
@ -227,7 +228,7 @@ namespace equiv
equiv.mk ((to_fun eqg) ∘ f)
(is_equiv.compose f (to_fun eqg))
theorem path_closed (f' : A → B) (Heq : to_fun eqf ≈ f') : A ≃ B :=
theorem path_closed (f' : A → B) (Heq : to_fun eqf = f') : A ≃ B :=
equiv.mk f' (is_equiv.path_closed f Heq)
theorem symm : B ≃ A :=
@ -239,7 +240,7 @@ namespace equiv
theorem cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : C ≃ A :=
equiv.mk g (is_equiv.cancel_L f _)
protected theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
protected theorem transport (P : A → Type) {x y : A} {p : x = y} : (P x) ≃ (P y) :=
equiv.mk (transport P p) (is_equiv.transport P p)
end
@ -251,9 +252,9 @@ namespace equiv
private definition Hg [instance] : is_equiv (to_fun eqg) := to_is_equiv eqg
--We need this theorem for the funext_from_ua proof
theorem inv_eq (p : eqf ≈ eqg)
: is_equiv.inv (to_fun eqf) ≈ is_equiv.inv (to_fun eqg) :=
path.rec_on p idp
theorem inv_eq (p : eqf = eqg)
: is_equiv.inv (to_fun eqf) = is_equiv.inv (to_fun eqg) :=
eq.rec_on p idp
end

494
hott/init/path.hlean
View file

@ -1,47 +1,44 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad
-- Author: Jeremy Avigad, Jakob von Raumer
-- Ported from Coq HoTT
--
-- TODO: things to test:
-- o To what extent can we use opaque definitions outside the file?
-- o Try doing these proofs with tactics.
-- o Try using the simplifier on some of these proofs.
prelude
import .function .datatypes .relation .tactic
import algebra.function
open function eq
open function
-- Path equality
-- ---- --------
-- Path
-- ----
inductive path.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
idpath : path a a
namespace path
namespace eq
variables {A B C : Type} {P : A → Type} {x y z t : A}
notation a ≈ b := path a b
notation x ≈ y `:>`:50 A:49 := @path A x y
definition idp {a : A} := idpath a
--notation a = b := eq a b
notation x = y `:>`:50 A:49 := @eq A x y
definition idp {a : A} := refl a
-- unbased path induction
definition rec' [reducible] {P : Π (a b : A), (a ≈ b) -> Type}
(H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p :=
path.rec (H a) p
definition rec' [reducible] {P : Π (a b : A), (a = b) -> Type}
(H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p :=
eq.rec (H a) p
definition rec_on' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b)
definition rec_on' [reducible] {P : Π (a b : A), (a = b) -> Type} {a b : A} (p : a = b)
(H : Π (a : A), P a a idp) : P a b p :=
path.rec (H a) p
eq.rec (H a) p
-- Concatenation and inverse
-- -------------------------
definition concat (p : x ≈ y) (q : y ≈ z) : x ≈ z :=
path.rec (λu, u) q p
definition concat (p : x = y) (q : y = z) : x = z :=
eq.rec (λu, u) q p
definition inverse (p : x ≈ y) : y ≈ x :=
path.rec (idpath x) p
definition inverse (p : x = y) : y = x :=
eq.rec (refl x) p
notation p₁ ⬝ p₂ := concat p₁ p₂
notation p ⁻¹ := inverse p
@ -50,159 +47,159 @@ namespace path
-- ------------------------------------
-- The identity path is a right unit.
definition concat_p1 (p : x ≈ y) : p ⬝ idp ≈ p :=
definition concat_p1 (p : x = y) : p ⬝ idp = p :=
rec_on p idp
-- The identity path is a right unit.
definition concat_1p (p : x ≈ y) : idp ⬝ p ≈ p :=
definition concat_1p (p : x = y) : idp ⬝ p = p :=
rec_on p idp
-- Concatenation is associative.
definition concat_p_pp (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r :=
definition concat_p_pp (p : x = y) (q : y = z) (r : z = t) :
p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r :=
rec_on r (rec_on q idp)
definition concat_pp_p (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
(p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) :=
definition concat_pp_p (p : x = y) (q : y = z) (r : z = t) :
(p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) :=
rec_on r (rec_on q idp)
-- The left inverse law.
definition concat_pV (p : x ≈ y) : p ⬝ p⁻¹ ≈ idp :=
definition concat_pV (p : x = y) : p ⬝ p⁻¹ = idp :=
rec_on p idp
-- The right inverse law.
definition concat_Vp (p : x ≈ y) : p⁻¹ ⬝ p ≈ idp :=
definition concat_Vp (p : x = y) : p⁻¹ ⬝ p = idp :=
rec_on p idp
-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
-- redundant, following from earlier theorems.
definition concat_V_pp (p : x ≈ y) (q : y ≈ z) : p⁻¹ ⬝ (p ⬝ q) ≈ q :=
definition concat_V_pp (p : x = y) (q : y = z) : p⁻¹ ⬝ (p ⬝ q) = q :=
rec_on q (rec_on p idp)
definition concat_p_Vp (p : x ≈ y) (q : x ≈ z) : p ⬝ (p⁻¹ ⬝ q) ≈ q :=
definition concat_p_Vp (p : x = y) (q : x = z) : p ⬝ (p⁻¹ ⬝ q) = q :=
rec_on q (rec_on p idp)
definition concat_pp_V (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q⁻¹ ≈ p :=
definition concat_pp_V (p : x = y) (q : y = z) : (p ⬝ q) ⬝ q⁻¹ = p :=
rec_on q (rec_on p idp)
definition concat_pV_p (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p :=
definition concat_pV_p (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p :=
rec_on q (take p, rec_on p idp) p
-- Inverse distributes over concatenation
definition inv_pp (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p⁻¹ :=
definition inv_pp (p : x = y) (q : y = z) : (p ⬝ q)⁻¹ = q⁻¹ ⬝ p⁻¹ :=
rec_on q (rec_on p idp)
definition inv_Vp (p : y ≈ x) (q : y ≈ z) : (p⁻¹ ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p :=
definition inv_Vp (p : y = x) (q : y = z) : (p⁻¹ ⬝ q)⁻¹ = q⁻¹ ⬝ p :=
rec_on q (rec_on p idp)
-- universe metavariables
definition inv_pV (p : x ≈ y) (q : z ≈ y) : (p ⬝ q⁻¹)⁻¹ ≈ q ⬝ p⁻¹ :=
definition inv_pV (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ :=
rec_on p (take q, rec_on q idp) q
definition inv_VV (p : y ≈ x) (q : z ≈ y) : (p⁻¹ ⬝ q⁻¹)⁻¹ ≈ q ⬝ p :=
definition inv_VV (p : y = x) (q : z = y) : (p⁻¹ ⬝ q⁻¹)⁻¹ = q ⬝ p :=
rec_on p (rec_on q idp)
-- Inverse is an involution.
definition inv_V (p : x ≈ y) : p⁻¹⁻¹ ≈ p :=
definition inv_V (p : x = y) : p⁻¹⁻¹ = p :=
rec_on p idp
-- Theorems for moving things around in equations
-- ----------------------------------------------
definition moveR_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
p ≈ (r⁻¹ ⬝ q) → (r ⬝ p) ≈ q :=
definition moveR_Mp (p : x = z) (q : y = z) (r : y = x) :
p = (r⁻¹ ⬝ q) → (r ⬝ p) = q :=
rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p
definition moveR_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
r ≈ q ⬝ p⁻¹ → r ⬝ p ≈ q :=
definition moveR_pM (p : x = z) (q : y = z) (r : y = x) :
r = q ⬝ p⁻¹ → r ⬝ p = q :=
rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q
definition moveR_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
p ≈ r ⬝ q → r⁻¹ ⬝ p ≈ q :=
definition moveR_Vp (p : x = z) (q : y = z) (r : x = y) :
p = r ⬝ q → r⁻¹ ⬝ p = q :=
rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q
definition moveR_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
r ≈ q ⬝ p → r ⬝ p⁻¹ ≈ q :=
definition moveR_pV (p : z = x) (q : y = z) (r : y = x) :
r = q ⬝ p → r ⬝ p⁻¹ = q :=
rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r
definition moveL_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
r⁻¹ ⬝ q ≈ p → q ≈ r ⬝ p :=
definition moveL_Mp (p : x = z) (q : y = z) (r : y = x) :
r⁻¹ ⬝ q = p → q = r ⬝ p :=
rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p
definition moveL_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
q ⬝ p⁻¹ ≈ r → q ≈ r ⬝ p :=
definition moveL_pM (p : x = z) (q : y = z) (r : y = x) :
q ⬝ p⁻¹ = r → q = r ⬝ p :=
rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q
definition moveL_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
r ⬝ q ≈ p → q ≈ r⁻¹ ⬝ p :=
definition moveL_Vp (p : x = z) (q : y = z) (r : x = y) :
r ⬝ q = p → q = r⁻¹ ⬝ p :=
rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q
definition moveL_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
q ⬝ p ≈ r → q ≈ r ⬝ p⁻¹ :=
definition moveL_pV (p : z = x) (q : y = z) (r : y = x) :
q ⬝ p = r → q = r ⬝ p⁻¹ :=
rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r
definition moveL_1M (p q : x ≈ y) :
p ⬝ q⁻¹ ≈ idp → p ≈ q :=
definition moveL_1M (p q : x = y) :
p ⬝ q⁻¹ = idp → p = q :=
rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p
definition moveL_M1 (p q : x ≈ y) :
q⁻¹ ⬝ p ≈ idp → p ≈ q :=
definition moveL_M1 (p q : x = y) :
q⁻¹ ⬝ p = idp → p = q :=
rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p
definition moveL_1V (p : x ≈ y) (q : y ≈ x) :
p ⬝ q ≈ idp → p ≈ q⁻¹ :=
definition moveL_1V (p : x = y) (q : y = x) :
p ⬝ q = idp → p = q⁻¹ :=
rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p
definition moveL_V1 (p : x ≈ y) (q : y ≈ x) :
q ⬝ p ≈ idp → p ≈ q⁻¹ :=
definition moveL_V1 (p : x = y) (q : y = x) :
q ⬝ p = idp → p = q⁻¹ :=
rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p
definition moveR_M1 (p q : x ≈ y) :
idp ≈ p⁻¹ ⬝ q → p ≈ q :=
definition moveR_M1 (p q : x = y) :
idp = p⁻¹ ⬝ q → p = q :=
rec_on p (take q h, h ⬝ (concat_1p _)) q
definition moveR_1M (p q : x ≈ y) :
idp ≈ q ⬝ p⁻¹ → p ≈ q :=
definition moveR_1M (p q : x = y) :
idp = q ⬝ p⁻¹ → p = q :=
rec_on p (take q h, h ⬝ (concat_p1 _)) q
definition moveR_1V (p : x ≈ y) (q : y ≈ x) :
idp ≈ q ⬝ p → p⁻¹ ≈ q :=
definition moveR_1V (p : x = y) (q : y = x) :
idp = q ⬝ p → p⁻¹ = q :=
rec_on p (take q h, h ⬝ (concat_p1 _)) q
definition moveR_V1 (p : x ≈ y) (q : y ≈ x) :
idp ≈ p ⬝ q → p⁻¹ ≈ q :=
definition moveR_V1 (p : x = y) (q : y = x) :
idp = p ⬝ q → p⁻¹ = q :=
rec_on p (take q h, h ⬝ (concat_1p _)) q
-- Transport
-- ---------
definition transport [reducible] (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y :=
path.rec_on p u
definition transport [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P x) : P y :=
eq.rec_on p u
-- 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.rec_on p idp
definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y :=
eq.rec_on p idp
definition ap01 := ap
definition homotopy [reducible] (f g : Πx, P x) : Type :=
Πx : A, f x ≈ g x
Πx : A, f x = g x
notation f ∼ g := homotopy f g
definition apD10 {f g : Πx, P x} (H : f ≈ g) : f ∼ g :=
λx, path.rec_on H idp
definition apD10 {f g : Πx, P x} (H : f = g) : f ∼ g :=
λx, eq.rec_on H idp
definition ap10 {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H
definition ap10 {f g : A → B} (H : f = g) : f ∼ g := apD10 H
definition ap11 {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y :=
definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
rec_on H (rec_on p idp)
definition apD (f : Πa:A, P a) {x y : A} (p : x ≈ y) : p ▹ (f x) ≈ f y :=
definition apD (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ (f x) = f y :=
rec_on p idp
@ -211,26 +208,26 @@ namespace path
calc_subst transport
calc_trans concat
calc_refl idpath
calc_refl refl
calc_symm inverse
-- More theorems for moving things around in equations
-- ---------------------------------------------------
definition moveR_transport_p (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
u ≈ p⁻¹ ▹ v → p ▹ u ≈ v :=
definition moveR_transport_p (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) :
u = p⁻¹ ▹ v → p ▹ u = v :=
rec_on p (take v, id) v
definition moveR_transport_V (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
u ≈ p ▹ v → p⁻¹ ▹ u ≈ v :=
definition moveR_transport_V (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) :
u = p ▹ v → p⁻¹ ▹ u = v :=
rec_on p (take u, id) u
definition moveL_transport_V (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
p ▹ u ≈ v → u ≈ p⁻¹ ▹ v :=
definition moveL_transport_V (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) :
p ▹ u = v → u = p⁻¹ ▹ v :=
rec_on p (take v, id) v
definition moveL_transport_p (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
p⁻¹ ▹ u ≈ v → u ≈ p ▹ v :=
definition moveL_transport_p (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) :
p⁻¹ ▹ u = v → u = p ▹ v :=
rec_on p (take u, id) u
-- Functoriality of functions
@ -240,115 +237,115 @@ namespace path
-- functorial.
-- Functions take identity paths to identity paths
definition ap_1 (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp
definition ap_1 (x : A) (f : A → B) : (ap f idp) = idp :> (f x = f x) := idp
definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp = idp :> (f x = f x) := idp
-- Functions commute with concatenation.
definition ap_pp (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) :=
definition ap_pp (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) :=
rec_on q (rec_on p idp)
definition ap_p_pp (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) :=
definition ap_p_pp (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) :=
rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p
definition ap_pp_p (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) :=
definition ap_pp_p (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) :=
rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r
-- Functions commute with path inverses.
definition inverse_ap (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)⁻¹ ≈ ap f (p⁻¹) :=
definition inverse_ap (f : A → B) {x y : A} (p : x = y) : (ap f p)⁻¹ = ap f (p⁻¹) :=
rec_on p idp
definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p⁻¹) ≈ (ap f p)⁻¹ :=
definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x = y) : ap f (p⁻¹) = (ap f p)⁻¹ :=
rec_on p idp
-- [ap] itself is functorial in the first argument.
definition ap_idmap (p : x ≈ y) : ap id p ≈ p :=
definition ap_idmap (p : x = y) : ap id p = p :=
rec_on p idp
definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
ap (g ∘ f) p ≈ ap g (ap f p) :=
definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x = y) :
ap (g ∘ f) p = ap g (ap f p) :=
rec_on p idp
-- Sometimes we don't have the actual function [compose].
definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) :
ap (λa, g (f a)) p ≈ ap g (ap f p) :=
definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x = y) :
ap (λa, g (f a)) p = ap g (ap f p) :=
rec_on p idp
-- The action of constant maps.
definition ap_const (p : x ≈ y) (z : B) :
ap (λu, z) p ≈ idp :=
definition ap_const (p : x = y) (z : B) :
ap (λu, z) p = idp :=
rec_on p idp
-- Naturality of [ap].
definition concat_Ap {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) :
(ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
definition concat_Ap {f g : A → B} (p : Π x, f x = g x) {x y : A} (q : x = y) :
(ap f q) ⬝ (p y) = (p x) ⬝ (ap g q) :=
rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹)
-- Naturality of [ap] at identity.
definition concat_A1p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) :
(ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
definition concat_A1p {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) :
(ap f q) ⬝ (p y) = (p x) ⬝ q :=
rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹)
definition concat_pA1 {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) :
(p x) ⬝ (ap f q) ≈ q ⬝ (p y) :=
definition concat_pA1 {f : A → A} (p : Πx, x = f x) {x y : A} (q : x = y) :
(p x) ⬝ (ap f q) = q ⬝ (p y) :=
rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹)
-- Naturality with other paths hanging around.
definition concat_pA_pp {f g : A → B} (p : Π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) :=
definition concat_pA_pp {f g : A → B} (p : Π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) :=
rec_on s (rec_on q idp)
definition concat_pA_p {f g : A → B} (p : Π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 :=
definition concat_pA_p {f g : A → B} (p : Π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 :=
rec_on q idp
-- TODO: try this using the simplifier, and compare proofs
definition concat_A_pp {f g : A → B} (p : Π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) :=
definition concat_A_pp {f g : A → B} (p : Π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) :=
rec_on s (rec_on q
(calc
(ap f idp) ⬝ (p x ⬝ idp) ≈ idp ⬝ p x : idp
... ≈ p x : concat_1p _
... ≈ (p x) ⬝ (ap g idp ⬝ idp) : idp))
(ap f idp) ⬝ (p x ⬝ idp) = idp ⬝ p x : idp
... = p x : concat_1p _
... = (p x) ⬝ (ap g idp ⬝ idp) : idp))
-- This also works:
-- rec_on s (rec_on q (concat_1p _ ▹ idp))
definition concat_pA1_pp {f : A → A} (p : Π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) :=
definition concat_pA1_pp {f : A → A} (p : Π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) :=
rec_on s (rec_on q idp)
definition concat_pp_A1p {g : A → A} (p : Π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) :=
definition concat_pp_A1p {g : A → A} (p : Π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) :=
rec_on s (rec_on q idp)
definition concat_pA1_p {f : A → A} (p : Π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 :=
definition concat_pA1_p {f : A → A} (p : Π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 :=
rec_on q idp
definition concat_A1_pp {f : A → A} (p : Π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) :=
definition concat_A1_pp {f : A → A} (p : Π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) :=
rec_on s (rec_on q (concat_1p _ ▹ idp))
definition concat_pp_A1 {g : A → A} (p : Π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 :=
definition concat_pp_A1 {g : A → A} (p : Π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 :=
rec_on q idp
definition concat_p_A1p {g : A → A} (p : Π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) :=
definition concat_p_A1p {g : A → A} (p : Π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) :=
begin
apply (rec_on s),
apply (rec_on q),
@ -360,27 +357,27 @@ namespace path
-- Application of paths between functions preserves the groupoid structure
definition apD10_1 (f : Πx, P x) (x : A) : apD10 (idpath f) x ≈ idp := idp
definition apD10_1 (f : Πx, P x) (x : A) : apD10 (refl f) x = idp := idp
definition apD10_pp {f f' f'' : Πx, P x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x :=
definition apD10_pp {f f' f'' : Πx, P x} (h : f = f') (h' : f' = f'') (x : A) :
apD10 (h ⬝ h') x = apD10 h x ⬝ apD10 h' x :=
rec_on h (take h', rec_on h' idp) h'
definition apD10_V {f g : Πx : A, P x} (h : f ≈ g) (x : A) :
apD10 (h⁻¹) x ≈ (apD10 h x)⁻¹ :=
definition apD10_V {f g : Πx : A, P x} (h : f = g) (x : A) :
apD10 (h⁻¹) x = (apD10 h x)⁻¹ :=
rec_on h idp
definition ap10_1 {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
definition ap10_1 {f : A → B} (x : A) : ap10 (refl f) x = idp := idp
definition ap10_pp {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_pp {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 {f g : A → B} (h : f ≈ g) (x : A) : ap10 (h⁻¹) x ≈ (ap10 h x)⁻¹ :=
definition ap10_V {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 (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:=
definition ap_ap10 (f g : A → B) (h : B → C) (p : f = g) (a : A) :
ap h (ap10 p a) = ap10 (ap (λ f', h ∘ f') p) a:=
rec_on p idp
@ -388,77 +385,77 @@ namespace path
-- ---------------------------------------------
definition transport_1 (P : A → Type) {x : A} (u : P x) :
idp ▹ u ≈ u := idp
idp ▹ u = u := idp
definition transport_pp (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
p ⬝ q ▹ u ≈ q ▹ p ▹ u :=
definition transport_pp (P : A → Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
p ⬝ q ▹ u = q ▹ p ▹ u :=
rec_on q (rec_on p idp)
definition transport_pV (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
p ▹ p⁻¹ ▹ z ≈ z :=
definition transport_pV (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 (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
p⁻¹ ▹ p ▹ z ≈ z :=
definition transport_Vp (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)
definition transport_p_pp (P : A → Type)
{x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) :
{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) :=
= (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u))
:> ((p ⬝ (q ⬝ r)) ▹ u = r ▹ q ▹ p ▹ u) :=
rec_on r (rec_on q (rec_on p idp))
-- Here is another coherence lemma for transport.
definition transport_pVp (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) :=
definition transport_pVp (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) :=
rec_on p idp
-- Dependent transport in a doubly dependent type.
-- should P, Q and y all be explicit here?
definition transportD (P : A → Type) (Q : Π a : A, P a → Type)
{a a' : A} (p : a ≈ a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=
{a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=
rec_on p z
-- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation
notation p `▹D`:65 x:64 := transportD _ _ p _ x
-- Transporting along higher-dimensional paths
definition transport2 (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) :
p ▹ z ≈ q ▹ z :=
definition transport2 (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
notation p `▹2`:65 x:64 := transport2 _ p _ x
-- An alternative definition.
definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q)
definition transport2_is_ap10 (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 :=
transport2 Q r z = ap10 (ap (transport Q) r) z :=
rec_on r idp
definition transport2_p2p (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 :=
definition transport2_p2p (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 :=
rec_on r1 (rec_on r2 idp)
definition transport2_V (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
transport2 Q (r⁻¹) z ≈ ((transport2 Q r z)⁻¹) :=
definition transport2_V (Q : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) :
transport2 Q (r⁻¹) z = ((transport2 Q r z)⁻¹) :=
rec_on r idp
definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type)
{x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) :=
{x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) :=
rec_on p w
notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x
definition concat_AT (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 :=
definition concat_AT (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 :=
rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹)
-- TODO (from Coq library): What should this be called?
definition ap_transport {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)) :=
definition ap_transport {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)) :=
rec_on p idp
@ -475,34 +472,34 @@ namespace path
-/
-- Transporting in a constant fibration.
definition transport_const (p : x ≈ y) (z : B) : transport (λx, B) p z ≈ z :=
definition transport_const (p : x = y) (z : B) : transport (λx, B) p z = z :=
rec_on p idp
definition transport2_const {p q : x ≈ y} (r : p ≈ q) (z : B) :
transport_const p z ≈ transport2 (λu, B) r z ⬝ transport_const q z :=
definition transport2_const {p q : x = y} (r : p = q) (z : B) :
transport_const p z = transport2 (λu, B) r z ⬝ transport_const q z :=
rec_on r (concat_1p _)⁻¹
-- Transporting in a pulled back fibration.
-- TODO: P can probably be implicit
definition transport_compose (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
transport (P ∘ f) p z ≈ transport P (ap f p) z :=
definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) :
transport (P ∘ f) p z = transport P (ap f p) z :=
rec_on p idp
definition transport_precompose (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 :=
definition transport_precompose (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 :=
rec_on p idp
definition apD10_ap_precompose (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) :=
definition apD10_ap_precompose (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) :=
rec_on p idp
definition apD10_ap_postcompose (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) :=
definition apD10_ap_postcompose (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) :=
rec_on p idp
-- A special case of [transport_compose] which seems to come up a lot.
definition transport_idmap_ap (P : A → Type) x y (p : x ≈ y) (u : P x) :
transport P p u ≈ transport (λz, z) (ap P p) u :=
definition transport_idmap_ap (P : A → Type) x y (p : x = y) (u : P x) :
transport P p u = transport (λz, z) (ap P p) u :=
rec_on p idp
@ -510,8 +507,8 @@ namespace path
-- ------------------------------
-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const].
definition apD_const (f : A → B) (p: x ≈ y) :
apD f p ≈ transport_const p (f x) ⬝ ap f p :=
definition apD_const (f : A → B) (p: x = y) :
apD f p = transport_const p (f x) ⬝ ap f p :=
rec_on p idp
@ -519,87 +516,87 @@ namespace path
-- ------------------------------------
-- Horizontal composition of 2-dimensional paths.
definition concat2 {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
p ⬝ q ≈ p' ⬝ q' :=
definition concat2 {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') :
p ⬝ q = p' ⬝ q' :=
rec_on h (rec_on h' idp)
infixl `◾`:75 := concat2
-- 2-dimensional path inversion
definition inverse2 {p q : x ≈ y} (h : p ≈ q) : p⁻¹ ≈ q⁻¹ :=
definition inverse2 {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ :=
rec_on h idp
-- Whiskering
-- ----------
definition whiskerL (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r :=
definition whiskerL (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r :=
idp ◾ h
definition whiskerR {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r :=
definition whiskerR {p q : x = y} (h : p = q) (r : y = z) : p ⬝ r = q ⬝ r :=
h ◾ idp
-- Unwhiskering, a.k.a. cancelling
definition cancelL {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
definition cancelL {x y z : A} (p : x = y) (q r : y = z) : (p ⬝ q = p ⬝ r) → (q = r) :=
rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q
definition cancelR {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
definition cancelR {x y z : A} (p q : x = y) (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) :=
rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q
-- Whiskering and identity paths.
definition whiskerR_p1 {p q : x ≈ y} (h : p ≈ q) :
(concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
definition whiskerR_p1 {p q : x = y} (h : p = q) :
(concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q = h :=
rec_on h (rec_on p idp)
definition whiskerR_1p (p : x ≈ y) (q : y ≈ z) :
whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
definition whiskerR_1p (p : x = y) (q : y = z) :
whiskerR idp q = idp :> (p ⬝ q = p ⬝ q) :=
rec_on q idp
definition whiskerL_p1 (p : x ≈ y) (q : y ≈ z) :
whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
definition whiskerL_p1 (p : x = y) (q : y = z) :
whiskerL p idp = idp :> (p ⬝ q = p ⬝ q) :=
rec_on q idp
definition whiskerL_1p {p q : x ≈ y} (h : p ≈ q) :
(concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
definition whiskerL_1p {p q : x = y} (h : p = q) :
(concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q = h :=
rec_on h (rec_on p idp)
definition concat2_p1 {p q : x ≈ y} (h : p ≈ q) :
h ◾ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) :=
definition concat2_p1 {p q : x = y} (h : p = q) :
h ◾ idp = whiskerR h idp :> (p ⬝ idp = q ⬝ idp) :=
rec_on h idp
definition concat2_1p {p q : x ≈ y} (h : p ≈ q) :
idp ◾ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) :=
definition concat2_1p {p q : x = y} (h : p = q) :
idp ◾ h = whiskerL idp h :> (idp ⬝ p = idp ⬝ q) :=
rec_on h idp
-- TODO: note, 4 inductions
-- The interchange law for concatenation.
definition concat_concat2 {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) :=
definition concat_concat2 {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) :=
rec_on d (rec_on c (rec_on b (rec_on a idp)))
definition concat_whisker {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') :=
definition concat_whisker {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') :=
rec_on b (rec_on a (concat_1p _)⁻¹)
-- Structure corresponding to the coherence equations of a bicategory.
-- The "pentagonator": the 3-cell witnessing the associativity pentagon.
definition pentagon {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
definition pentagon {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 :=
= concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s :=
rec_on s (rec_on r (rec_on q (rec_on p idp)))
-- The 3-cell witnessing the left unit triangle.
definition triangulator (p : x ≈ y) (q : y ≈ z) :
concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
definition triangulator (p : x = y) (q : y = z) :
concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q = whiskerL p (concat_1p q) :=
rec_on q (rec_on p idp)
definition eckmann_hilton {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
definition eckmann_hilton {x:A} (p q : idp = idp :> (x = x)) : p ⬝ q = q ⬝ p :=
(!whiskerR_p1 ◾ !whiskerL_1p)⁻¹
⬝ (!concat_p1 ◾ !concat_p1)
⬝ (!concat_1p ◾ !concat_1p)
@ -609,51 +606,52 @@ namespace path
⬝ (!whiskerL_1p ◾ !whiskerR_p1)
-- The action of functions on 2-dimensional paths
definition ap02 (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q :=
definition ap02 (f:A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q :=
rec_on r idp
definition ap02_pp (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' :=
definition ap02_pp (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' :=
rec_on r (rec_on r' idp)
definition ap02_p2p (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
definition ap02_p2p (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')⁻¹ :=
rec_on r (rec_on s (rec_on q (rec_on p idp)))
-- rec_on r (rec_on s (rec_on p (rec_on q idp)))
definition apD02 {p q : x ≈ y} (f : Π x, P x) (r : p ≈ q) :
apD f p ≈ transport2 P r (f x) ⬝ apD f q :=
definition apD02 {p q : x = y} (f : Π x, P x) (r : p = q) :
apD f p = transport2 P r (f x) ⬝ apD f q :=
rec_on r (concat_1p _)⁻¹
-- And now for a lemma whose statement is much longer than its proof.
definition apD02_pp (P : A → Type) (f : Π x:A, P x) {x y : A}
{p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) :
apD02 f (r1 ⬝ r2) ≈ apD02 f r1
{p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) :
apD02 f (r1 ⬝ r2) = apD02 f r1
⬝ whiskerL (transport2 P r1 (f x)) (apD02 f r2)
⬝ concat_p_pp _ _ _
⬝ (whiskerR ((transport2_p2p P r1 r2 (f x))⁻¹) (apD f p3)) :=
rec_on r2 (rec_on r1 (rec_on p1 idp))
end path
namespace path
end eq
namespace eq
variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D}
theorem congr_arg2 (f : A → B → C) (Ha : a ≈ a') (Hb : b ≈ b') : f a b ≈ f a' b' :=
theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
rec_on Ha (rec_on Hb idp)
theorem congr_arg3 (f : A → B → C → D) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c')
: f a b c ≈ f a' b' c' :=
theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c')
: f a b c = f a' b' c' :=
rec_on Ha (congr_arg2 (f a) Hb Hc)
theorem congr_arg4 (f : A → B → C → D → E) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c') (Hd : d ≈ d')
: f a b c d ≈ f a' b' c' d' :=
theorem congr_arg4 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d')
: f a b c d = f a' b' c' d' :=
rec_on Ha (congr_arg3 (f a) Hb Hc Hd)
end path
end eq
namespace path
namespace eq
variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
{E : Πa b c, D a b c → Type} {F : Type}
variables {a a' : A}
@ -661,8 +659,8 @@ variables {a a' : A}
{c : C a b} {c' : C a' b'}
{d : D a b c} {d' : D a' b' c'}
theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a ≈ a') (Hb : Ha ▹ b ≈ b')
: f a b ≈ f a' b' :=
theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : (Ha ▹ b) = b')
: f a b = f a' b' :=
rec_on Hb (rec_on Ha idp)
/- From the Coq version:
@ -717,4 +715,4 @@ rec_on Hb (rec_on Ha idp)
autorewrite with paths in * |- * ; auto with path_hints.
-/
end path
end eq

46
hott/trunc.hlean → hott/init/trunc.hlean
View file

@ -2,9 +2,9 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Jeremy Avigad, Floris van Doorn
-- Ported from Coq HoTT
import .path .logic data.nat.basic data.empty data.unit data.sigma .equiv
open path nat sigma unit
prelude
import .path .logic .datatypes .equiv .types.empty .types.sigma
open eq nat sigma unit
set_option pp.universes true
-- Truncation levels
@ -59,11 +59,11 @@ namespace truncation
-/
structure contr_internal (A : Type) :=
(center : A) (contr : Π(a : A), center ≈ a)
(center : A) (contr : Π(a : A), center = a)
definition is_trunc_internal (n : trunc_index) : Type → Type :=
trunc_index.rec_on n (λA, contr_internal A)
(λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
(λn trunc_n A, (Π(x y : A), trunc_n (x = y)))
structure is_trunc [class] (n : trunc_index) (A : Type) :=
(to_internal : is_trunc_internal n A)
@ -79,33 +79,33 @@ namespace truncation
variables {A B : Type}
-- TODO: rename to is_trunc_succ
definition is_trunc_succ (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x ≈ y)]
definition is_trunc_succ (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x = y)]
: is_trunc n.+1 A :=
is_trunc.mk (λ x y, !is_trunc.to_internal)
-- TODO: rename to is_trunc_path
definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) :=
is_trunc.mk (!is_trunc.to_internal x y)
/- contractibility -/
definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A :=
definition is_contr.mk (center : A) (contr : Π(a : A), center = a) : is_contr A :=
is_trunc.mk (contr_internal.mk center contr)
definition center (A : Type) [H : is_contr A] : A :=
@contr_internal.center A !is_trunc.to_internal
definition contr [H : is_contr A] (a : A) : !center ≈ a :=
definition contr [H : is_contr A] (a : A) : !center = a :=
@contr_internal.contr A !is_trunc.to_internal a
definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
definition path_contr [H : is_contr A] (x y : A) : x = y :=
contr x⁻¹ ⬝ (contr y)
definition path2_contr {A : Type} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
definition path2_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
have K : ∀ (r : x = y), path_contr x y = r, from (λ r, eq.rec_on r !concat_Vp),
K p⁻¹ ⬝ K q
definition contr_paths_contr [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
definition contr_paths_contr [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
is_contr.mk !path_contr (λ p, !path2_contr)
/- truncation is upward close -/
@ -132,7 +132,7 @@ namespace truncation
λm IHm n, trunc_index.rec_on n
(λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn))
(λn IHn A Hnm (Hn : is_trunc n.+1 A),
@is_trunc_succ A m (λx y, IHm n (x≈y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)),
@is_trunc_succ A m (λx y, IHm n (x = y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)),
trunc_index.rec_on m base step n A Hnm Hn
-- the following cannot be instances in their current form, because it is looping
@ -145,11 +145,11 @@ namespace truncation
definition trunc_hset (A : Type) (n : trunc_index) [H : is_hset A]
: is_trunc (n.+2) A :=
trunc_leq A 0 (n.+2) star
trunc_leq A nat.zero (n.+2) star
/- hprops -/
definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y :=
definition is_hprop.elim [H : is_hprop A] (x y : A) : x = y :=
@center _ !succ_is_trunc
definition contr_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A :=
@ -162,21 +162,21 @@ namespace truncation
have H2 [visible] : is_contr A, from H x,
!contr_paths_contr)
definition is_hprop.mk {A : Type} (H : ∀x y : A, x ≈ y) : is_hprop A :=
definition is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A :=
hprop_inhabited_contr (λ x, is_contr.mk x (H x))
/- hsets -/
definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A :=
@is_trunc_succ _ _ (λ x y, is_hprop.mk (H x y))
definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q :=
definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q :=
@is_hprop.elim _ !succ_is_trunc p q
/- instances -/
definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp))
definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a = x) :=
is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))
-- definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry
@ -197,7 +197,7 @@ namespace truncation
notation `hset` := 0-Type
definition hprop.mk := @trunctype.mk -1
definition hset.mk := @trunctype.mk 0
definition hset.mk := @trunctype.mk nat.zero
--what does the following line in Coq do?
--Canonical Structure default_TruncType := fun n T P => (@BuildTruncType n T P).
@ -224,7 +224,7 @@ namespace truncation
trunc_index.rec_on n
(λA (HA : is_contr A) B f (H : is_equiv f), !equiv_preserves_contr)
(λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ _ _ (λ x y : B,
IH (f⁻¹ x ≈ f⁻¹ y) !succ_is_trunc (x ≈ y) ((ap (f⁻¹))⁻¹) !inv_closed))
IH (f⁻¹ x = f⁻¹ y) !succ_is_trunc (x = y) ((ap (f⁻¹))⁻¹) !inv_closed))
A HA B f H
definition trunc_equiv' (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B :=

36
hott/init/types/empty.hlean Normal file
View file

@ -0,0 +1,36 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jeremy Avigad, Floris van Doorn, Jakob von Raumer
prelude
import ..datatypes ..logic
-- Empty type
-- ----------
namespace empty
protected theorem elim (A : Type) (H : empty) : A :=
rec (λe, A) H
end empty
protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
take (a b : empty), decidable.inl (!empty.elim a)
definition tneg.tneg (A : Type) := A → empty
prefix `~` := tneg.tneg
namespace tneg
variables {A B : Type}
protected definition intro (H : A → empty) : ~A := H
protected definition elim (H1 : ~A) (H2 : A) : empty := H1 H2
protected definition empty : ~empty := λH : empty, H
definition tabsurd (H1 : A) (H2 : ~A) : B := !empty.elim (H2 H1)
definition tneg_tneg_intro (H : A) : ~~A := λH2 : ~A, tneg.elim H2 H
definition tmt (H1 : A → B) (H2 : ~B) : ~A := λHA : A, tabsurd (H1 HA) H2
definition tneg_pi_left {B : A → Type} (H : ~Πa, B a) : ~~A :=
λHnA : ~A, tneg.elim H (λHA : A, tabsurd HA HnA)
definition tneg_function_right (H : ~(A → B)) : ~B :=
λHB : B, tneg.elim H (λHA : A, HB)
end tneg

5
hott/init/prod.hlean → hott/init/types/prod.hlean
View file

@ -6,7 +6,7 @@ Module: data.prod.decl
Author: Leonardo de Moura, Jeremy Avigad
-/
prelude
import init.wf
import ..wf
definition pair := @prod.mk
@ -18,6 +18,8 @@ namespace prod
infixr `*` := prod
end low_precedence_times
definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
notation `pr₁` := pr1
notation `pr₂` := pr2
@ -80,4 +82,5 @@ namespace prod
subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb)
end
end prod

2
hott/init/sigma.hlean → hott/init/types/sigma.hlean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-/
prelude
import init.num init.wf init.logic init.tactic
import ..num ..wf ..logic ..tactic
structure sigma {A : Type} (B : A → Type) :=
dpair :: (dpr1 : A) (dpr2 : B dpr1)

6
hott/logic.hlean
View file

@ -1,9 +1,9 @@
import data.empty .path
--javra: Maybe this should go somewhere else
open path
open eq
inductive tdecidable [class] (A : Type) : Type :=
inl : A → tdecidable A,
inr : ~A → tdecidable A
structure decidable_paths [class] (A : Type) :=
(elim : ∀(x y : A), tdecidable (x ≈ y))
(elim : ∀(x y : A), tdecidable (x = y))

7
hott/pointed.hlean
View file

@ -2,9 +2,8 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
import hott.path hott.trunc data.sigma data.prod
open path prod truncation
import init.trunc
open eq prod truncation
structure is_pointed [class] (A : Type) :=
(point : A)
@ -30,7 +29,7 @@ namespace is_pointed
: is_pointed (A × B) :=
is_pointed.mk (prod.mk (point A) (point B))
protected definition loop_space (a : A) : is_pointed (a ≈ a) :=
protected definition loop_space (a : A) : is_pointed (a = a) :=
is_pointed.mk idp
end is_pointed

53
hott/types/pi.hlean
View file

@ -6,9 +6,8 @@ Ported from Coq HoTT
Theorems about pi-types (dependent function spaces)
-/
import ..trunc ..axioms.funext .sigma
open path equiv is_equiv funext
import init.equiv init.axioms.funext types.sigma
open eq equiv is_equiv funext
namespace pi
universe variables l k
@ -27,45 +26,45 @@ namespace pi
definition apD10_path_pi [H : funext] (h : f ∼ g) : apD10 (path_pi h) ∼ h :=
apD10 (retr apD10 h)
definition path_pi_eta [H : funext] (p : f ≈ g) : path_pi (apD10 p) ≈ p :=
definition path_pi_eta [H : funext] (p : f = g) : path_pi (apD10 p) = p :=
sect apD10 p
definition path_pi_idp [H : funext] : path_pi (λx : A, idpath (f x)) ≈ idpath f :=
definition path_pi_idp [H : funext] : path_pi (λx : A, refl (f x)) = refl f :=
!path_pi_eta
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f ≈ g) ≃ (f ∼ g) :=
definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f = g) ≃ (f ∼ g) :=
equiv.mk _ !funext.ap
definition is_equiv_path_pi [instance] [H : funext] (f g : Πx, B x)
: is_equiv (@path_pi _ _ _ f g) :=
inv_closed apD10
definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f ≈ g) :=
definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f = g) :=
equiv.mk _ !is_equiv_path_pi
/- Transport -/
protected definition transport (p : a ≈ a') (f : Π(b : B a), C a b)
protected definition transport (p : a = a') (f : Π(b : B a), C a b)
: (transport (λa, Π(b : B a), C a b) p f)
∼ (λb, transport (C a') !transport_pV (transportD _ _ p _ (f (p⁻¹ ▹ b)))) :=
path.rec_on p (λx, idp)
eq.rec_on p (λx, idp)
/- A special case of [transport_pi] where the type [B] does not depend on [A],
and so it is just a fixed type [B]. -/
definition transport_constant {C : A → A' → Type} (p : a ≈ a') (f : Π(b : A'), C a b)
: (path.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, path.transport (λa, C a b) p (f b)) :=
path.rec_on p (λx, idp)
definition transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b)
: (eq.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, eq.transport (λa, C a b) p (f b)) :=
eq.rec_on p (λx, idp)
/- Maps on paths -/
/- The action of maps given by lambda. -/
definition ap_lambdaD [H : funext] {C : A' → Type} (p : a ≈ a') (f : Πa b, C b) :
ap (λa b, f a b) p ≈ path_pi (λb, ap (λa, f a b) p) :=
definition ap_lambdaD [H : funext] {C : A' → Type} (p : a = a') (f : Πa b, C b) :
ap (λa b, f a b) p = path_pi (λb, ap (λa, f a b) p) :=
begin
apply (path.rec_on p),
apply (eq.rec_on p),
apply inverse,
apply path_pi_idp
end
@ -73,20 +72,20 @@ namespace pi
/- Dependent paths -/
/- with more implicit arguments the conclusion of the following theorem is
(Π(b : B a), transportD B C p b (f b) ≈ g (path.transport B p b)) ≃
(path.transport (λa, Π(b : B a), C a b) p f ≈ g) -/
definition dpath_pi [H : funext] (p : a ≈ a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
: (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) ≃ (p ▹ f ≈ g) :=
path.rec_on p (λg, !homotopy_equiv_path) g
(Π(b : B a), transportD B C p b (f b) = g (eq.transport B p b)) ≃
(eq.transport (λa, Π(b : B a), C a b) p f = g) -/
definition dpath_pi [H : funext] (p : a = a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
: (Π(b : B a), p ▹D (f b) = g (p ▹ b)) ≃ (p ▹ f = g) :=
eq.rec_on p (λg, !homotopy_equiv_path) g
section open sigma.ops
/- more implicit arguments:
(Π(b : B a), path.transport C (sigma.path p idp) (f b) ≈ g (p ▹ b)) ≃
(Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) ≈ g (path.transport B p b)) -/
definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a ≈ a')
(Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃
(Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
(f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
(Π(b : B a), (sigma.path p idp) ▹ (f b) ≈ g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) :=
path.rec_on p (λg, !equiv.refl) g
(Π(b : B a), (sigma.path p idp) ▹ (f b) = g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) = g (p ▹ b)) :=
eq.rec_on p (λg, !equiv.refl) g
end
/- truncation -/
@ -108,12 +107,12 @@ namespace pi
apply equiv.symm, apply path_equiv_homotopy,
apply IH,
intro a,
show is_trunc n (f a ≈ g a), from
show is_trunc n (f a = g a), from
succ_is_trunc n (f a) (g a)
end
definition trunc_path_pi [instance] [H : funext.{l k}] (n : trunc_index) (f g : Πa, B a)
[H : ∀a, is_trunc n (f a ≈ g a)] : is_trunc n (f ≈ g) :=
[H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) :=
begin
apply trunc_equiv', apply equiv.symm,
apply path_equiv_homotopy,

12
hott/types/prod.hlean
View file

@ -7,8 +7,8 @@ Ported from Coq HoTT
Theorems about products
-/
import ..trunc data.prod
open path equiv is_equiv truncation prod
import init.trunc init.datatypes
open eq equiv is_equiv truncation prod
variables {A A' B B' C D : Type}
{a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}
@ -16,13 +16,13 @@ variables {A A' B B' C D : Type}
namespace prod
-- prod.eta is already used for the eta rule for strict equality
protected definition peta (u : A × B) : (pr₁ u , pr₂ u) ≈ u :=
protected definition peta (u : A × B) : (pr₁ u , pr₂ u) = u :=
destruct u (λu1 u2, idp)
definition pair_path (pa : a ≈ a') (pb : b ≈ b') : (a , b) ≈ (a' , b') :=
path.rec_on pa (path.rec_on pb idp)
definition pair_path (pa : a = a') (pb : b = b') : (a , b) = (a' , b') :=
eq.rec_on pa (eq.rec_on pb idp)
protected definition path : (pr₁ u ≈ pr₁ v) → (pr₂ u ≈ pr₂ v) → u ≈ v :=
protected definition path : (pr₁ u = pr₁ v) → (pr₂ u = pr₂ v) → u = v :=
begin
apply (prod.rec_on u), intros (a₁, b₁),
apply (prod.rec_on v), intros (a₂, b₂, H₁, H₂),

188
hott/types/sigma.hlean
View file

@ -7,8 +7,8 @@ Ported from Coq HoTT
Theorems about sigma-types (dependent sums)
-/
import ..trunc .prod ..axioms.funext
open path sigma sigma.ops equiv is_equiv
import init.trunc init.axioms.funext init.types.prod
open eq sigma sigma.ops equiv is_equiv
namespace sigma
infixr [local] ∘ := function.compose --remove
@ -17,95 +17,95 @@ namespace sigma
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
-- sigma.eta is already used for the eta rule for strict equality
protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ ≈ u :=
protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ = u :=
destruct u (λu1 u2, idp)
definition eta2 (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ ≈ u :=
definition eta2 (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ = u :=
destruct u (λu1 u2, destruct u2 (λu21 u22, idp))
definition eta3 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ ≈ u :=
definition eta3 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ = u :=
destruct u (λu1 u2, destruct u2 (λu21 u22, destruct u22 (λu221 u222, idp)))
definition dpair_eq_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
path.rec_on p (λb b' q, path.rec_on q idp) b b' q
definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' :=
eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
/- In Coq they often have to give u and v explicitly -/
protected definition path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
protected definition path (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : u = v :=
destruct u
(λu1 u2, destruct v (λ v1 v2, dpair_eq_dpair))
p q
/- Projections of paths from a total space -/
definition path_pr1 (p : u ≈ v) : u.1 ≈ v.1 :=
definition path_pr1 (p : u = v) : u.1 = v.1 :=
ap dpr1 p
postfix `..1`:(max+1) := path_pr1
definition path_pr2 (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 :=
path.rec_on p idp
definition path_pr2 (p : u = v) : p..1 ▹ u.2 = v.2 :=
eq.rec_on p idp
--Coq uses the following proof, which only computes if u,v are dpairs AND p is idp
--(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p
postfix `..2`:(max+1) := path_pr2
definition dpair_sigma_path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: dpair (sigma.path p q)..1 (sigma.path p q)..2 ≈ ⟨p, q⟩ :=
definition dpair_sigma_path (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
: dpair (sigma.path p q)..1 (sigma.path p q)..2 = ⟨p, q⟩ :=
begin
reverts (p, q),
apply (destruct u), intros (u1, u2),
apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert
apply (path.rec_on p), intros (v2, q),
apply (path.rec_on q), apply idp
apply (eq.rec_on p), intros (v2, q),
apply (eq.rec_on q), apply idp
end
definition sigma_path_pr1 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (sigma.path p q)..1 ≈ p :=
definition sigma_path_pr1 (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : (sigma.path p q)..1 = p :=
(!dpair_sigma_path)..1
definition sigma_path_pr2 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: sigma_path_pr1 p q ▹ (sigma.path p q)..2 ≈ q :=
definition sigma_path_pr2 (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
: sigma_path_pr1 p q ▹ (sigma.path p q)..2 = q :=
(!dpair_sigma_path)..2
definition sigma_path_eta (p : u ≈ v) : sigma.path (p..1) (p..2) ≈ p :=
definition sigma_path_eta (p : u = v) : sigma.path (p..1) (p..2) = p :=
begin
apply (path.rec_on p),
apply (eq.rec_on p),
apply (destruct u), intros (u1, u2),
apply idp
end
definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: transport (λx, B' x.1) (sigma.path p q) ≈ transport B' p :=
definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
: transport (λx, B' x.1) (sigma.path p q) = transport B' p :=
begin
reverts (p, q),
apply (destruct u), intros (u1, u2),
apply (destruct v), intros (v1, v2, p), generalize v2,
apply (path.rec_on p), intros (v2, q),
apply (path.rec_on q), apply idp
apply (eq.rec_on p), intros (v2, q),
apply (eq.rec_on q), apply idp
end
/- the uncurried version of sigma_path. We will prove that this is an equivalence -/
/- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
definition sigma_path_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
definition sigma_path_uncurried (pq : Σ(p : dpr1 u = dpr1 v), p ▹ (dpr2 u) = dpr2 v) : u = v :=
destruct pq sigma.path
definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 ≈ pq :=
definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
: dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 = pq :=
destruct pq dpair_sigma_path
definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: (sigma_path_uncurried pq)..1 ≈ pq.1 :=
definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
: (sigma_path_uncurried pq)..1 = pq.1 :=
(!dpair_sigma_path_uncurried)..1
definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 ≈ pq.2 :=
definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
: (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 = pq.2 :=
(!dpair_sigma_path_uncurried)..2
definition sigma_path_eta_uncurried (p : u ≈ v) : sigma_path_uncurried (dpair p..1 p..2) ≈ p :=
definition sigma_path_eta_uncurried (p : u = v) : sigma_path_uncurried (dpair p..1 p..2) = p :=
!sigma_path_eta
definition transport_sigma_path_dpr1_uncurried {B' : A → Type}
(pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) ≈ transport B' pq.1 :=
(pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2)
: transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) = transport B' pq.1 :=
destruct pq transport_dpr1_sigma_path
definition is_equiv_sigma_path [instance] (u v : Σa, B a)
@ -115,25 +115,25 @@ namespace sigma
sigma_path_eta_uncurried
dpair_sigma_path_uncurried
definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 = v.1), p ▹ u.2 = v.2) ≃ (u = v) :=
equiv.mk sigma_path_uncurried !is_equiv_sigma_path
definition dpair_eq_dpair_pp_pp (p1 : a ≈ a' ) (q1 : p1 ▹ b ≈ b' )
(p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
definition dpair_eq_dpair_pp_pp (p1 : a = a' ) (q1 : p1 ▹ b = b' )
(p2 : a' = a'') (q2 : p2 ▹ b' = b'') :
dpair_eq_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
≈ dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 :=
= dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 :=
begin
reverts (b', p2, b'', q1, q2),
apply (path.rec_on p1), intros (b', p2),
apply (path.rec_on p2), intros (b'', q1),
apply (path.rec_on q1), intro q2,
apply (path.rec_on q2), apply idp
apply (eq.rec_on p1), intros (b', p2),
apply (eq.rec_on p2), intros (b'', q1),
apply (eq.rec_on q1), intro q2,
apply (eq.rec_on q2), apply idp
end
definition sigma_path_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2)
(p2 : v.1 ≈ w.1) (q2 : p2 ▹ v.2 ≈ w.2) :
definition sigma_path_pp_pp (p1 : u.1 = v.1) (q1 : p1 ▹ u.2 = v.2)
(p2 : v.1 = w.1) (q2 : p2 ▹ v.2 = w.2) :
sigma.path (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
≈ sigma.path p1 q1 ⬝ sigma.path p2 q2 :=
= sigma.path p1 q1 ⬝ sigma.path p2 q2 :=
begin
reverts (p1, q1, p2, q2),
apply (destruct u), intros (u1, u2),
@ -142,49 +142,49 @@ namespace sigma
apply dpair_eq_dpair_pp_pp
end
definition dpair_eq_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
dpair_eq_dpair p q ≈ dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') :
dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
begin
reverts (b', q),
apply (path.rec_on p), intros (b', q),
apply (path.rec_on q), apply idp
apply (eq.rec_on p), intros (b', q),
apply (eq.rec_on q), apply idp
end
/- path_pr1 commutes with the groupoid structure. -/
definition path_pr1_idp (u : Σa, B a) : (idpath u)..1 ≈ idpath (u.1) := idp
definition path_pr1_pp (p : u ≈ v) (q : v ≈ w) : (p ⬝ q) ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp
definition path_pr1_V (p : u ≈ v) : p⁻¹ ..1 ≈ (p..1)⁻¹ := !ap_V
definition path_pr1_idp (u : Σa, B a) : (refl u)..1 = refl (u.1) := idp
definition path_pr1_pp (p : u = v) (q : v = w) : (p ⬝ q) ..1 = (p..1) ⬝ (q..1) := !ap_pp
definition path_pr1_V (p : u = v) : p⁻¹ ..1 = (p..1)⁻¹ := !ap_V
/- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/
definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ dpair_eq_dpair idp q :=
path.rec_on q idp
definition ap_dpair (q : b₁ = b₂) : ap (dpair a) q = dpair_eq_dpair idp q :=
eq.rec_on q idp
/- Dependent transport is the same as transport along a sigma_path. -/
/- Dependent transport is the same as transport along a sigma_eq. -/
definition transportD_eq_transport (p : a ≈ a') (c : C a b) :
p ▹D c ≈ transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
path.rec_on p idp
definition transportD_eq_transport (p : a = a') (c : C a b) :
p ▹D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
eq.rec_on p idp
definition sigma_path_eq_sigma_path {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'}
(r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : sigma.path p1 p2 ≈ sigma.path q1 q2 :=
path.rec_on r
proof (λq2 s, path.rec_on s idp) qed
definition sigma_path_eq_sigma_path {p1 q1 : a = a'} {p2 : p1 ▹ b = b'} {q2 : q1 ▹ b = b'}
(r : p1 = q1) (s : r ▹ p2 = q2) : sigma.path p1 p2 = sigma.path q1 q2 :=
eq.rec_on r
proof (λq2 s, eq.rec_on s idp) qed
q2
s
-- begin
-- reverts (q2, s),
-- apply (path.rec_on r), intros (q2, s),
-- apply (path.rec_on s), apply idp
-- apply (eq.rec_on r), intros (q2, s),
-- apply (eq.rec_on s), apply idp
-- end
/- A path between paths in a total space is commonly shown component wise. -/
definition path_sigma_path {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
definition path_sigma_path {p q : u = v} (r : p..1 = q..1) (s : r ▹ p..2 = q..2) : p = q :=
begin
reverts (q, r, s),
apply (path.rec_on p),
apply (eq.rec_on p),
apply (destruct u), intros (u1, u2, q, r, s),
apply concat, rotate 1,
apply sigma_path_eta,
@ -192,8 +192,8 @@ namespace sigma
end
/- In Coq they often have to give u and v explicitly when using the following definition -/
definition path_sigma_path_uncurried {p q : u ≈ v}
(rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
definition path_sigma_path_uncurried {p q : u = v}
(rs : Σ(r : p..1 = q..1), transport (λx, transport B x u.2 = v.2) r p..2 = q..2) : p = q :=
destruct rs path_sigma_path
/- Transport -/
@ -202,30 +202,30 @@ namespace sigma
In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory). A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/
definition transport_eq (p : a ≈ a') (bc : Σ(b : B a), C a b)
: p ▹ bc ≈ ⟨p ▹ bc.1, p ▹D bc.2⟩ :=
definition transport_eq (p : a = a') (bc : Σ(b : B a), C a b)
: p ▹ bc = ⟨p ▹ bc.1, p ▹D bc.2⟩ :=
begin
apply (path.rec_on p),
apply (eq.rec_on p),
apply (destruct bc), intros (b, c),
apply idp
end
/- The special case when the second variable doesn't depend on the first is simpler. -/
definition transport_eq_deg {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b)
: p ▹ bc ≈ ⟨bc.1, p ▹ bc.2⟩ :=
definition transport_eq_deg {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b)
: p ▹ bc = ⟨bc.1, p ▹ bc.2⟩ :=
begin
apply (path.rec_on p),
apply (eq.rec_on p),
apply (destruct bc), intros (b, c),
apply idp
end
/- Or if the second variable contains a first component that doesn't depend on the first. -/
definition transport_eq_4deg {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
(bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd ≈ ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ :=
definition transport_eq_4deg {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a')
(bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd = ⟨p ▹ bcd.1, p ▹ bcd.2.1, p ▹D2 bcd.2.2⟩ :=
begin
revert bcd,
apply (path.rec_on p), intro bcd,
apply (eq.rec_on p), intro bcd,
apply (destruct bcd), intros (b, cd),
apply (destruct cd), intros (c, d),
apply idp
@ -251,24 +251,24 @@ namespace sigma
apply (sigma.path (retr f a')),
-- "rewrite retr (g (f⁻¹ a'))"
apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))),
show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') ≈ b',
show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') = b',
from transport_pV B' (retr f a') b'
end
begin
intro u,
apply (destruct u), intros (a, b),
apply (sigma.path (sect f a)),
show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) ≈ b,
show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) = b,
from calc
transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b)))
≈ g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b)))
= g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b)))
: ap_transport (sect f a) (λ a, g a⁻¹)
... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b)))
... = g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b)))
: ap (g a⁻¹) !transport_compose
... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b)))
... = g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b)))
: ap (λ x, g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (x⁻¹) (g a b)))) (adj f a)
... ≈ g a⁻¹ (g a b) : transport_pV
... ≈ b : sect (g a) b
... = g a⁻¹ (g a b) : transport_pV
... = b : sect (g a) b
end
-- -- "rewrite ap_transport"
-- apply concat, apply inverse, apply (ap_transport (sect f a) (λ a, g a⁻¹)),
@ -293,20 +293,20 @@ namespace sigma
definition equiv_functor_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a :=
equiv_functor equiv.refl Hg
definition ap_functor_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b')
definition ap_functor_sigma_dpair (p : a = a') (q : p ▹ b = b')
: ap (sigma.functor f g) (sigma.path p q)
≈ sigma.path (ap f p)
= sigma.path (ap f p)
(transport_compose _ f p (g a b)⁻¹ ⬝ ap_transport p g b⁻¹ ⬝ ap (g a') q) :=
begin
reverts (b', q),
apply (path.rec_on p),
intros (b', q), apply (path.rec_on q),
apply (eq.rec_on p),
intros (b', q), apply (eq.rec_on q),
apply idp
end
definition ap_functor_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
definition ap_functor_sigma (p : u.1 = v.1) (q : p ▹ u.2 = v.2)
: ap (sigma.functor f g) (sigma.path p q)
≈ sigma.path (ap f p)
= sigma.path (ap f p)
(transport_compose B' f p (g u.1 u.2)⁻¹ ⬝ ap_transport p g u.2⁻¹ ⬝ ap (g v.1) q) :=
begin
reverts (p, q),
@ -429,14 +429,14 @@ namespace sigma
/- ** Subtypes (sigma types whose second components are hprops) -/
/- To prove equality in a subtype, we only need equality of the first component. -/
definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 ≈ v.1 → u ≈ v :=
definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 = v.1 → u = v :=
(sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc))))
definition is_equiv_path_hprop [instance] [H : Πa, is_hprop (B a)] (u v : Σa, B a)
: is_equiv (path_hprop u v) :=
!is_equiv.compose
definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 ≈ v.1) ≃ (u ≈ v)
definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 = v.1) ≃ (u = v)
:=
equiv.mk !path_hprop _
@ -458,7 +458,7 @@ namespace sigma
apply IH,
apply succ_is_trunc, assumption,
intro p,
show is_trunc n (p ▹ u .2 ≈ v .2), from
show is_trunc n (p ▹ u .2 = v .2), from
succ_is_trunc n (p ▹ u.2) (v.2),
end