270 lines
9.9 KiB
Text
270 lines
9.9 KiB
Text
/-
|
|
Copyright (c) 2015 Floris van Doorn. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Module: cubical.pathover
|
|
Author: Floris van Doorn
|
|
|
|
Theorems about pathovers
|
|
-/
|
|
|
|
import types.sigma arity
|
|
|
|
open eq equiv is_equiv equiv.ops
|
|
|
|
namespace cubical
|
|
|
|
variables {A A' : Type} {B : A → Type} {C : Πa, B a → Type}
|
|
{a a₂ a₃ a₄ : A} {p : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄}
|
|
{b : B a} {b₂ : B a₂} {b₃ : B a₃} {b₄ : B a₄}
|
|
{c : C a b} {c₂ : C a₂ b₂}
|
|
{u v w : Σa, B a}
|
|
|
|
inductive pathover (B : A → Type) (b : B a) : Π{a₂ : A} (p : a = a₂) (b₂ : B a₂), Type :=
|
|
idpatho : pathover B b (refl a) b
|
|
|
|
notation b `=[`:50 p:0 `]`:0 b₂:50 := pathover _ b p b₂
|
|
|
|
definition idpo [reducible] {b : B a} : b =[refl a] b :=
|
|
pathover.idpatho b
|
|
|
|
/- equivalences with equality using transport -/
|
|
definition pathover_of_transport_eq (r : p ▸ b = b₂) : b =[p] b₂ :=
|
|
by cases p; cases r; exact idpo
|
|
|
|
definition pathover_of_eq_transport (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
|
|
by cases p; cases r; exact idpo
|
|
|
|
definition transport_eq_of_pathover (r : b =[p] b₂) : p ▸ b = b₂ :=
|
|
by cases r; exact idp
|
|
|
|
definition eq_transport_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ :=
|
|
by cases r; exact idp
|
|
|
|
definition pathover_equiv_transport_eq (p : a = a₂) (b : B a) (b₂ : B a₂)
|
|
: (b =[p] b₂) ≃ (p ▸ b = b₂) :=
|
|
begin
|
|
fapply equiv.MK,
|
|
{ exact transport_eq_of_pathover},
|
|
{ exact pathover_of_transport_eq},
|
|
{ intro r, cases p, cases r, apply idp},
|
|
{ intro r, cases r, apply idp},
|
|
end
|
|
|
|
definition pathover_equiv_eq_transport (p : a = a₂) (b : B a) (b₂ : B a₂)
|
|
: (b =[p] b₂) ≃ (b = p⁻¹ ▸ b₂) :=
|
|
begin
|
|
fapply equiv.MK,
|
|
{ exact eq_transport_of_pathover},
|
|
{ exact pathover_of_eq_transport},
|
|
{ intro r, cases p, cases r, apply idp},
|
|
{ intro r, cases r, apply idp},
|
|
end
|
|
|
|
definition pathover_transport (p : a = a₂) (b : B a) : b =[p] p ▸ b :=
|
|
pathover_of_transport_eq idp
|
|
|
|
definition transport_pathover (p : a = a₂) (b : B a) : p⁻¹ ▸ b =[p] b :=
|
|
pathover_of_eq_transport idp
|
|
|
|
definition concato (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
|
|
pathover.rec_on r₂ (pathover.rec_on r idpo)
|
|
|
|
definition inverseo (r : b =[p] b₂) : b₂ =[p⁻¹] b :=
|
|
pathover.rec_on r idpo
|
|
|
|
definition apdo (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
|
|
eq.rec_on p idpo
|
|
|
|
infix `⬝o`:75 := concato
|
|
postfix `⁻¹ᵒ`:(max+10) := inverseo
|
|
|
|
/- Some of the theorems analogous to theorems for = in init.path -/
|
|
|
|
definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo =[con_idp p] r :=
|
|
pathover.rec_on r idpo
|
|
|
|
definition idpo_cono (r : b =[p] b₂) : idpo ⬝o r =[idp_con p] r :=
|
|
pathover.rec_on r idpo
|
|
|
|
definition cono.assoc' (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) :
|
|
r ⬝o (r₂ ⬝o r₃) =[!con.assoc'] (r ⬝o r₂) ⬝o r₃ :=
|
|
pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo))
|
|
|
|
definition cono.assoc (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) :
|
|
(r ⬝o r₂) ⬝o r₃ =[!con.assoc] r ⬝o (r₂ ⬝o r₃) :=
|
|
pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo))
|
|
|
|
-- the left inverse law.
|
|
definition cono.right_inv (r : b =[p] b₂) : r ⬝o r⁻¹ᵒ =[!con.right_inv] idpo :=
|
|
pathover.rec_on r idpo
|
|
|
|
-- the right inverse law.
|
|
definition cono.left_inv (r : b =[p] b₂) : r⁻¹ᵒ ⬝o r =[!con.left_inv] idpo :=
|
|
pathover.rec_on r idpo
|
|
|
|
/- Some of the theorems analogous to theorems for transport in init.path -/
|
|
--set_option pp.notation false
|
|
definition pathover_constant (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' :=
|
|
begin
|
|
fapply equiv.MK,
|
|
{ intro r, cases r, exact idp},
|
|
{ intro r, cases p, cases r, exact idpo},
|
|
{ intro r, cases p, cases r, exact idp},
|
|
{ intro r, cases r, exact idp},
|
|
end
|
|
|
|
definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' :=
|
|
pathover_equiv_transport_eq idp b b'
|
|
|
|
definition eq_of_pathover_idp {b' : B a} (q : b =[idpath a] b') : b = b' :=
|
|
transport_eq_of_pathover q
|
|
|
|
definition pathover_idp_of_eq {b' : B a} (q : b = b') : b =[idpath a] b' :=
|
|
pathover_of_transport_eq q
|
|
|
|
definition idp_rec_on {P : Π⦃b₂ : B a⦄, b =[idpath a] b₂ → Type}
|
|
{b₂ : B a} (r : b =[idpath a] b₂) (H : P idpo) : P r :=
|
|
have H2 : P (pathover_idp_of_eq (eq_of_pathover_idp r)),
|
|
from eq.rec_on (eq_of_pathover_idp r) H,
|
|
left_inv !pathover_idp r ▸ H2
|
|
|
|
--pathover with fibration B' ∘ f
|
|
definition pathover_compose (B' : A' → Type) (f : A → A') (p : a = a₂)
|
|
(b : B' (f a)) (b₂ : B' (f a₂)) : b =[p] b₂ ≃ b =[ap f p] b₂ :=
|
|
begin
|
|
fapply equiv.MK,
|
|
{ intro r, cases r, exact idpo},
|
|
{ intro r, cases p, apply (idp_rec_on r), apply idpo},
|
|
{ intro r, cases p, esimp [function.compose,function.id], apply (idp_rec_on r), apply idp},
|
|
{ intro r, cases r, exact idp},
|
|
end
|
|
|
|
definition apdo_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃)
|
|
: apdo f (p ⬝ q) = apdo f p ⬝o apdo f q :=
|
|
by cases p; cases q; exact idp
|
|
|
|
open sigma sigma.ops
|
|
namespace sigma
|
|
/- pathovers used for sigma types -/
|
|
definition dpair_eq_dpair (p : a = a₂) (q : b =[p] b₂) : ⟨a, b⟩ = ⟨a₂, b₂⟩ :=
|
|
by cases q; apply idp
|
|
|
|
definition sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2) : u = v :=
|
|
by cases u; cases v; apply (dpair_eq_dpair p q)
|
|
|
|
/- Projections of paths from a total space -/
|
|
|
|
definition pathover_pr2 (p : u = v) : u.2 =[p..1] v.2 :=
|
|
by cases p; apply idpo
|
|
|
|
postfix `..2o`:(max+1) := pathover_pr2
|
|
--superfluous notation, but useful if you want an 'o' on both projections
|
|
postfix [parsing-only] `..1o`:(max+1) := eq_pr1
|
|
|
|
private definition dpair_sigma_eq (p : u.1 = v.1) (q : u.2 =[p] v.2)
|
|
: ⟨(sigma_eq p q)..1, (sigma_eq p q)..2o⟩ = ⟨p, q⟩ :=
|
|
by cases u; cases v; cases q; apply idp
|
|
|
|
definition sigma_eq_pr1 (p : u.1 = v.1) (q : u.2 =[p] v.2) : (sigma_eq p q)..1 = p :=
|
|
(dpair_sigma_eq p q)..1
|
|
|
|
definition sigma_eq_pr2 (p : u.1 = v.1) (q : u.2 =[p] v.2)
|
|
: (sigma_eq p q)..2o =[sigma_eq_pr1 p q] q :=
|
|
(dpair_sigma_eq p q)..2o
|
|
|
|
definition sigma_eq_eta (p : u = v) : sigma_eq (p..1) (p..2o) = p :=
|
|
by cases p; cases u; apply idp
|
|
|
|
/- the uncurried version of sigma_eq. We will prove that this is an equivalence -/
|
|
|
|
definition sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2), u = v
|
|
| sigma_eq_uncurried ⟨pq₁, pq₂⟩ := sigma_eq pq₁ pq₂
|
|
|
|
definition dpair_sigma_eq_uncurried : Π (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2),
|
|
⟨(sigma_eq_uncurried pq)..1, (sigma_eq_uncurried pq)..2o⟩ = pq
|
|
| dpair_sigma_eq_uncurried ⟨pq₁, pq₂⟩ := dpair_sigma_eq pq₁ pq₂
|
|
|
|
definition sigma_eq_pr1_uncurried (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2)
|
|
: (sigma_eq_uncurried pq)..1 = pq.1 :=
|
|
(dpair_sigma_eq_uncurried pq)..1
|
|
|
|
definition sigma_eq_pr2_uncurried (pq : Σ(p : u.1 = v.1), u.2 =[p] v.2)
|
|
: (sigma_eq_uncurried pq)..2o =[sigma_eq_pr1_uncurried pq] pq.2 :=
|
|
(dpair_sigma_eq_uncurried pq)..2o
|
|
|
|
definition sigma_eq_eta_uncurried (p : u = v) : sigma_eq_uncurried (sigma.mk p..1 p..2o) = p :=
|
|
sigma_eq_eta p
|
|
|
|
definition is_equiv_sigma_eq [instance] (u v : Σa, B a)
|
|
: is_equiv (@sigma_eq_uncurried A B u v) :=
|
|
adjointify sigma_eq_uncurried
|
|
(λp, ⟨p..1, p..2o⟩)
|
|
sigma_eq_eta_uncurried
|
|
dpair_sigma_eq_uncurried
|
|
|
|
definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1), u.2 =[p] v.2) ≃ (u = v) :=
|
|
equiv.mk sigma_eq_uncurried !is_equiv_sigma_eq
|
|
|
|
end sigma
|
|
|
|
definition apd011o (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
|
|
: f a b = f a₂ b₂ :=
|
|
by cases Hb; exact idp
|
|
|
|
definition apd0111o (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
|
|
(Hc : c =[apd011o C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
|
|
by cases Hb; apply (idp_rec_on Hc); apply idp
|
|
|
|
namespace pi
|
|
--the most 'natural' version here needs a notion of "path over a pathover"
|
|
definition pi_pathover {f : Πb, C a b} {g : Πb₂, C a₂ b₂}
|
|
(r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apd011o C p q] g b₂) : f =[p] g :=
|
|
begin
|
|
cases p, apply pathover_idp_of_eq,
|
|
apply eq_of_homotopy, intro b,
|
|
apply eq_of_pathover_idp, apply r
|
|
end
|
|
|
|
definition pi_pathover' {C : (Σa, B a) → Type} {f : Πb, C ⟨a, b⟩} {g : Πb₂, C ⟨a₂, b₂⟩}
|
|
(r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[sigma.dpair_eq_dpair p q] g b₂)
|
|
: f =[p] g :=
|
|
begin
|
|
cases p, apply pathover_idp_of_eq,
|
|
apply eq_of_homotopy, intro b,
|
|
apply (@eq_of_pathover_idp _ C), exact (r b b (pathover.idpatho b)),
|
|
end
|
|
|
|
definition ap11o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
|
|
{b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apd011o C p q] g b₂ :=
|
|
by cases r; apply (idp_rec_on q); exact idpo
|
|
|
|
definition ap10o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
|
|
{b : B a} : f b =[apd011o C p !pathover_transport] g (p ▸ b) :=
|
|
by cases r; exact idpo
|
|
|
|
-- definition equiv_pi_pathover' (f : Πb, C a b) (g : Πb₂, C a₂ b₂) :
|
|
-- (f =[p] g) ≃ (Π(b : B a), f b =[apd011o C p !pathover_transport] g (p ▸ b)) :=
|
|
-- begin
|
|
-- fapply equiv.MK,
|
|
-- { exact ap10o},
|
|
-- { exact pi_pathover'},
|
|
-- { cases p, exact sorry},
|
|
-- { intro r, cases r, },
|
|
-- end
|
|
|
|
|
|
-- definition equiv_pi_pathover (f : Πb, C a b) (g : Πb₂, C a₂ b₂) :
|
|
-- (f =[p] g) ≃ (Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apd011o C p q] g b₂) :=
|
|
-- begin
|
|
-- fapply equiv.MK,
|
|
-- { exact ap11o},
|
|
-- { exact pi_pathover},
|
|
-- { cases p, exact sorry},
|
|
-- { intro r, cases r, },
|
|
-- end
|
|
|
|
end pi
|
|
|
|
|
|
end cubical
|