From 0b12d51b259320bddb717ac3a7e0d67976883fa4 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 22 May 2015 04:35:38 -0400 Subject: [PATCH] feat(hott): use pathovers in all the recursors of hits move pathover file to the init folder --- .../category/constructions/comma.hlean | 7 +- hott/algebra/hott.hlean | 6 +- hott/core.hlean | 3 +- hott/cubical/pathover.hlean | 268 ------------------ hott/hit/circle.hlean | 85 +++--- hott/hit/coeq.hlean | 14 +- hott/hit/colimit.hlean | 30 +- hott/hit/cylinder.hlean | 14 +- hott/hit/pushout.hlean | 14 +- hott/hit/quotient.hlean | 21 +- hott/hit/suspension.hlean | 14 +- hott/hit/type_quotient.hlean | 6 +- hott/init/default.hlean | 2 +- hott/init/equiv.hlean | 24 +- hott/init/hit.hlean | 12 +- hott/init/init.md | 1 + hott/init/pathover.hlean | 183 ++++++++++++ hott/init/trunc.hlean | 18 +- hott/types/int/default.hlean | 2 +- 19 files changed, 336 insertions(+), 388 deletions(-) delete mode 100644 hott/cubical/pathover.hlean create mode 100644 hott/init/pathover.hlean diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index cbdbf6fa3..caf1df24b 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -1,14 +1,15 @@ /- Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn, Jakob von Raumer + +Authors: Floris van Doorn Comma category -/ -import ..functor cubical.pathover ..strict ..category +import ..functor ..strict ..category -open eq functor equiv sigma sigma.ops is_trunc cubical iso is_equiv +open eq functor equiv sigma sigma.ops is_trunc iso is_equiv namespace category diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 959bbd492..208daa68d 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -6,9 +6,9 @@ Author: Floris van Doorn Theorems about algebra specific to HoTT -/ -import .group arity types.pi types.hprop_trunc cubical.pathover +import .group arity types.pi types.hprop_trunc -open equiv eq equiv.ops is_trunc cubical +open equiv eq equiv.ops is_trunc namespace algebra open Group has_mul has_inv @@ -55,7 +55,7 @@ namespace algebra (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H := begin cases G with Gc G, cases H with Hc H, - apply (apd011o mk (ua f)), + apply (apo011 mk (ua f)), apply group_pathover, exact resp_mul end diff --git a/hott/core.hlean b/hott/core.hlean index e62b6517a..49a537e91 100644 --- a/hott/core.hlean +++ b/hott/core.hlean @@ -7,5 +7,6 @@ The core of the HoTT library -/ import types -import cubical.pathover cubical.square +import cubical.square import hit.circle +import algebra.hott diff --git a/hott/cubical/pathover.hlean b/hott/cubical/pathover.hlean deleted file mode 100644 index f3a07bce7..000000000 --- a/hott/cubical/pathover.hlean +++ /dev/null @@ -1,268 +0,0 @@ -/- -Copyright (c) 2015 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -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] [constructor] {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 [recursor] {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 diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index 3c798b1b5..e88d88a7c 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -20,10 +20,10 @@ namespace circle definition seg2 : base1 = base2 := merid !south definition base : circle := base1 - definition loop : base = base := seg1 ⬝ seg2⁻¹ + definition loop : base = base := seg2 ⬝ seg1⁻¹ definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) - (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) (x : circle) : P x := + (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) (x : circle) : P x := begin induction x with b, { exact Pb1}, @@ -35,21 +35,21 @@ namespace circle end definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2) - (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) : P x := + (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) : P x := circle.rec2 Pb1 Pb2 Ps1 Ps2 x theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) - (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) - : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := + (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) + : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := !rec_merid theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2) - (Ps1 : seg1 ▸ Pb1 = Pb2) (Ps2 : seg2 ▸ Pb1 = Pb2) - : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := + (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2) + : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := !rec_merid definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 Ps2 : Pb1 = Pb2) (x : circle) : P := - rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x + rec2 Pb1 Pb2 (pathover_of_eq Ps1) (pathover_of_eq Ps2) x definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : P := @@ -58,15 +58,15 @@ namespace circle theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 := begin - apply (@cancel_left _ _ _ _ (tr_constant seg1 (elim2 Pb1 Pb2 Ps1 Ps2 base1))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg1], + apply eq_of_fn_eq_fn_inv !(pathover_constant seg1), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg1], end theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := begin - apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base1))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2], + apply eq_of_fn_eq_fn_inv !(pathover_constant seg2), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg2], end definition elim2_type (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2) (x : circle) : Type := @@ -84,41 +84,38 @@ namespace circle : transport (elim2_type Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 := by rewrite [tr_eq_cast_ap_fn,↑elim2_type,elim2_seg2];apply cast_ua_fn - protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase) + protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) (x : circle) : P x := begin fapply (rec2_on x), { exact Pbase}, { exact (transport P seg1 Pbase)}, - { apply idp}, - { apply tr_eq_of_eq_inv_tr, exact (Ploop⁻¹ ⬝ !con_tr)}, + { apply pathover_tr}, + { apply pathover_tr_of_pathover, exact Ploop} end ---rewrite -tr_con, exact Ploop⁻¹ protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base) - (Ploop : loop ▸ Pbase = Pbase) : P x := + (Ploop : Pbase =[loop] Pbase) : P x := circle.rec Pbase Ploop x theorem rec_loop_helper {A : Type} (P : A → Type) - {x y : A} {p : x = y} {u : P x} {v : P y} (q : u = p⁻¹ ▸ v) : - eq_inv_tr_of_tr_eq (tr_eq_of_eq_inv_tr q) = q := - by cases p; exact idp + {x y z : A} {p : x = y} {p' : z = y} {u : P x} {v : P z} (q : u =[p ⬝ p'⁻¹] v) : + pathover_tr_of_pathover q ⬝o !pathover_tr⁻¹ᵒ = q := + by cases p'; cases q; exact idp definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p := eq.rec_on p idp - theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase) : - apd (circle.rec Pbase Ploop) loop = Ploop := + theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) : + apdo (circle.rec Pbase Ploop) loop = Ploop := begin - rewrite [↑loop,apd_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap], --con_idp should work here - apply concat, apply (ap (λx, x ⬝ _)), apply con_idp, esimp, - rewrite [rec_loop_helper,inv_con_inv_left], - apply con_inv_cancel_left + rewrite [↑loop,apdo_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apdo_inv,rec2_seg1], + apply rec_loop_helper end protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) (x : circle) : P := - circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x + circle.rec Pbase (pathover_of_eq Ploop) x protected definition elim_on [reducible] {P : Type} (x : circle) (Pbase : P) (Ploop : Pbase = Pbase) : P := @@ -127,8 +124,8 @@ namespace circle theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) : ap (circle.elim Pbase Ploop) loop = Ploop := begin - apply (@cancel_left _ _ _ _ (tr_constant loop (circle.elim Pbase Ploop base))), - rewrite [-apd_eq_tr_constant_con_ap,↑circle.elim,rec_loop], + apply eq_of_fn_eq_fn_inv !(pathover_constant loop), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,rec_loop], end protected definition elim_type (Pbase : Type) (Ploop : Pbase ≃ Pbase) @@ -149,7 +146,7 @@ namespace circle end circle attribute circle.base1 circle.base2 circle.base [constructor] -attribute circle.rec2 circle.elim2 [unfold-c 6] [recursor 6] +attribute circle.elim2 circle.rec2 [unfold-c 6] [recursor 6] attribute circle.elim2_type [unfold-c 5] attribute circle.rec2_on circle.elim2_on [unfold-c 2] attribute circle.elim2_type [unfold-c 1] @@ -164,17 +161,22 @@ namespace circle definition loop_neq_idp : loop ≠ idp := assume H : loop = idp, - have H2 : Π{A : Type₁} {a : A} (p : a = a), p = idp, + have H2 : Π{A : Type₁} {a : A} {p : a = a}, p = idp, from λA a p, calc p = ap (circle.elim a p) loop : elim_loop ... = ap (circle.elim a p) (refl base) : by rewrite H, - absurd !H2 eq_bnot_ne_idp + absurd H2 eq_bnot_ne_idp definition nonidp (x : circle) : x = x := - circle.rec_on x loop - (calc - loop ▸ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr - ... = loop : by rewrite [con.left_inv, idp_con]) + begin + induction x, + { exact loop}, + { exact sorry} + end + -- circle.rec_on x loop + -- (calc + -- loop ▸ loop = loop⁻¹ ⬝ loop ⬝ loop : transport_eq_lr + -- ... = loop : by rewrite [con.left_inv, idp_con]) definition nonidp_neq_idp : nonidp ≠ (λx, idp) := assume H : nonidp = λx, idp, @@ -200,9 +202,10 @@ namespace circle begin induction x, { exact power loop}, - { apply eq_of_homotopy, intro a, - refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _, - rewrite [transport_code_loop_inv,power_con,succ_pred]} + { apply sorry} +-- apply eq_of_homotopy, intro a, +-- refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _, +-- rewrite [transport_code_loop_inv,power_con,succ_pred]} end --remove this theorem after #484 @@ -219,11 +222,11 @@ namespace circle apply transport (λ(y : base = base), transport circle.code y _ = _), { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹}, rewrite [▸*,@con_tr _ circle.code,transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ]}}, - { apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [circle.code,base,base1], exact _} + --{ apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [circle.code,base,base1], exact _} + { apply sorry} --simplify after #587 end - definition circle_eq_equiv (x : circle) : (base = x) ≃ circle.code x := begin fapply equiv.MK, diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 08cba18dc..2db0dcc67 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -31,7 +31,7 @@ parameters {A B : Type.{u}} (f g : A → B) eq_of_rel coeq_rel (Rmk f g x) protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x)) - (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) (y : coeq) : P y := + (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) (y : coeq) : P y := begin induction y, { apply P_i}, @@ -39,17 +39,17 @@ parameters {A B : Type.{u}} (f g : A → B) end protected definition rec_on [reducible] {P : coeq → Type} (y : coeq) - (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) : P y := + (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) : P y := rec P_i Pcp y theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x)) - (Pcp : Π(x : A), cp x ▸ P_i (f x) = P_i (g x)) - (x : A) : apd (rec P_i Pcp) (cp x) = Pcp x := + (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x)) + (x : A) : apdo (rec P_i Pcp) (cp x) = Pcp x := !rec_eq_of_rel protected definition elim {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x)) (y : coeq) : P := - rec P_i (λx, !tr_constant ⬝ Pcp x) y + rec P_i (λx, pathover_of_eq (Pcp x)) y protected definition elim_on [reducible] {P : Type} (y : coeq) (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x)) : P := @@ -58,8 +58,8 @@ parameters {A B : Type.{u}} (f g : A → B) theorem elim_cp {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x)) (x : A) : ap (elim P_i Pcp) (cp x) = Pcp x := begin - apply (@cancel_left _ _ _ _ (tr_constant (cp x) (elim P_i Pcp (coeq_i (f x))))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cp], + apply eq_of_fn_eq_fn_inv !(pathover_constant (cp x)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cp], end protected definition elim_type (P_i : B → Type) diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index d4408db12..c1540c3fc 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -34,7 +34,7 @@ section protected definition rec {P : colimit → Type} (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) - (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x) + (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) (y : colimit) : P y := begin fapply (type_quotient.rec_on y), @@ -44,18 +44,18 @@ section protected definition rec_on [reducible] {P : colimit → Type} (y : colimit) (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) - (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x) : P y := + (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) : P y := rec Pincl Pglue y theorem rec_cglue {P : colimit → Type} (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) - (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▸ Pincl (f j x) = Pincl x) - {j : J} (x : A (dom j)) : apd (rec Pincl Pglue) (cglue j x) = Pglue j x := + (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) + {j : J} (x : A (dom j)) : apdo (rec Pincl Pglue) (cglue j x) = Pglue j x := !rec_eq_of_rel - protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P) + protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P) (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P := - rec Pincl (λj a, !tr_constant ⬝ Pglue j a) y + rec Pincl (λj a, pathover_of_eq (Pglue j a)) y protected definition elim_on [reducible] {P : Type} (y : colimit) (Pincl : Π⦃i : I⦄ (x : A i), P) @@ -67,8 +67,8 @@ section (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x := begin - apply (@cancel_left _ _ _ _ (tr_constant (cglue j x) (elim Pincl Pglue (ι (f j x))))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cglue], + apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cglue], end protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type) @@ -118,7 +118,7 @@ section protected definition rec {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) - (Pglue : Π(n : ℕ) (a : A n), glue a ▸ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa := + (Pglue : Π(n : ℕ) (a : A n), Pincl (f a) =[glue a] Pincl a) (aa : seq_colim) : P aa := begin fapply (type_quotient.rec_on aa), { intro a, cases a, apply Pincl}, @@ -127,18 +127,18 @@ section protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim) (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) - (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a) + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) : P aa := rec Pincl Pglue aa theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) - (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▸ Pincl (f a) = Pincl a) {n : ℕ} (a : A n) - : apd (rec Pincl Pglue) (glue a) = Pglue a := + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) {n : ℕ} (a : A n) + : apdo (rec Pincl Pglue) (glue a) = Pglue a := !rec_eq_of_rel protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P) (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P := - rec Pincl (λn a, !tr_constant ⬝ Pglue a) + rec Pincl (λn a, pathover_of_eq (Pglue a)) protected definition elim_on [reducible] {P : Type} (aa : seq_colim) (Pincl : Π⦃n : ℕ⦄ (a : A n), P) @@ -149,8 +149,8 @@ section (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : ℕ} (a : A n) : ap (elim Pincl Pglue) (glue a) = Pglue a := begin - apply (@cancel_left _ _ _ _ (tr_constant (glue a) (elim Pincl Pglue (sι (f a))))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue], + apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_glue], end protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type) diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index f0c7eaa2e..606894ade 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -35,7 +35,7 @@ parameters {A B : Type.{u}} (f : A → B) protected definition rec {P : cylinder → Type} (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a)) - (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) (x : cylinder) : P x := + (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a) (x : cylinder) : P x := begin induction x, { cases a, @@ -46,18 +46,18 @@ parameters {A B : Type.{u}} (f : A → B) protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder) (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a)) - (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) : P x := + (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a) : P x := rec Pbase Ptop Pseg x theorem rec_seg {P : cylinder → Type} (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a)) - (Pseg : Π(a : A), seg a ▸ Pbase (f a) = Ptop a) - (a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a := + (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a) + (a : A) : apdo (rec Pbase Ptop Pseg) (seg a) = Pseg a := !rec_eq_of_rel protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P) (Pseg : Π(a : A), Pbase (f a) = Ptop a) (x : cylinder) : P := - rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x + rec Pbase Ptop (λa, pathover_of_eq (Pseg a)) x protected definition elim_on [reducible] {P : Type} (x : cylinder) (Pbase : B → P) (Ptop : A → P) (Pseg : Π(a : A), Pbase (f a) = Ptop a) : P := @@ -67,8 +67,8 @@ parameters {A B : Type.{u}} (f : A → B) (Pseg : Π(a : A), Pbase (f a) = Ptop a) (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a := begin - apply (@cancel_left _ _ _ _ (tr_constant (seg a) (elim Pbase Ptop Pseg (base (f a))))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_seg], + apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_seg], end protected definition elim_type (Pbase : B → Type) (Ptop : A → Type) diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index e62bcb12b..e34213b16 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -33,7 +33,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) eq_of_rel pushout_rel (Rmk f g x) protected definition rec {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) - (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x)) + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x)) (y : pushout) : P y := begin induction y, @@ -45,17 +45,17 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) protected definition rec_on [reducible] {P : pushout → Type} (y : pushout) (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) - (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x)) : P y := + (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x)) : P y := rec Pinl Pinr Pglue y theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x)) - (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▸ Pinl (f x) = Pinr (g x)) - (x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x := + (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x)) + (x : TL) : apdo (rec Pinl Pinr Pglue) (glue x) = Pglue x := !rec_eq_of_rel protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P := - rec Pinl Pinr (λx, !tr_constant ⬝ Pglue x) y + rec Pinl Pinr (λx, pathover_of_eq (Pglue x)) y protected definition elim_on [reducible] {P : Type} (y : pushout) (Pinl : BL → P) (Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) : P := @@ -65,8 +65,8 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (x : TL) : ap (elim Pinl Pinr Pglue) (glue x) = Pglue x := begin - apply (@cancel_left _ _ _ _ (tr_constant (glue x) (elim Pinl Pinr Pglue (inl (f x))))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue], + apply eq_of_fn_eq_fn_inv !(pathover_constant (glue x)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue], end protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type) diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 511c19c25..9fea2c754 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -8,7 +8,7 @@ Declaration of set-quotients import .type_quotient .trunc -open eq is_trunc trunc type_quotient +open eq is_trunc trunc type_quotient equiv namespace quotient section @@ -26,30 +26,29 @@ parameters {A : Type} (R : A → A → hprop) begin unfold quotient, exact _ end protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)] - (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a') + (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') (x : quotient) : P x := begin apply (@trunc.rec_on _ _ P x), { intro x', apply Pt}, { intro y, fapply (type_quotient.rec_on y), { exact Pc}, - { intros, - apply concat, apply transport_compose; apply Pp}} + { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}} end protected definition rec_on [reducible] {P : quotient → Type} (x : quotient) [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a)) - (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a') : P x := + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') : P x := rec Pc Pp x theorem rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)] - (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▸ Pc a = Pc a') - {a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H := - !is_hset.elim + (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') + {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H := + !is_hset.elimo protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P := - rec Pc (λa a' H, !tr_constant ⬝ Pp H) x + rec Pc (λa a' H, pathover_of_eq (Pp H)) x protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_hset P] (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := @@ -59,8 +58,8 @@ parameters {A : Type} (R : A → A → hprop) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a') : ap (elim Pc Pp) (eq_of_rel H) = Pp H := begin - apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel H) (elim Pc Pp (class_of a)))), - rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_eq_of_rel], + apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], end /- diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean index d46a2036d..0fdd39096 100644 --- a/hott/hit/suspension.hlean +++ b/hott/hit/suspension.hlean @@ -25,7 +25,7 @@ namespace suspension glue _ _ a protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south) - (Pm : Π(a : A), merid a ▸ PN = PS) (x : suspension A) : P x := + (Pm : Π(a : A), PN =[merid a] PS) (x : suspension A) : P x := begin fapply (pushout.rec_on _ _ x), { intro u, cases u, exact PN}, @@ -34,17 +34,17 @@ namespace suspension end protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A) - (PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▸ PN = PS) : P y := + (PN : P !north) (PS : P !south) (Pm : Π(a : A), PN =[merid a] PS) : P y := suspension.rec PN PS Pm y theorem rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south) - (Pm : Π(a : A), merid a ▸ PN = PS) (a : A) - : apd (suspension.rec PN PS Pm) (merid a) = Pm a := + (Pm : Π(a : A), PN =[merid a] PS) (a : A) + : apdo (suspension.rec PN PS Pm) (merid a) = Pm a := !rec_glue protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (x : suspension A) : P := - suspension.rec PN PS (λa, !tr_constant ⬝ Pm a) x + suspension.rec PN PS (λa, pathover_of_eq (Pm a)) x protected definition elim_on [reducible] {P : Type} (x : suspension A) (PN : P) (PS : P) (Pm : A → PN = PS) : P := @@ -53,8 +53,8 @@ namespace suspension theorem elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (a : A) : ap (suspension.elim PN PS Pm) (merid a) = Pm a := begin - apply (@cancel_left _ _ _ _ (tr_constant (merid a) (suspension.elim PN PS Pm !north))), - rewrite [-apd_eq_tr_constant_con_ap,↑suspension.elim,rec_merid], + apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑suspension.elim,rec_merid], end protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS) diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean index ed3c0c4b5..776786dd6 100644 --- a/hott/hit/type_quotient.hlean +++ b/hott/hit/type_quotient.hlean @@ -16,7 +16,7 @@ namespace type_quotient protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : type_quotient R) : P := - type_quotient.rec Pc (λa a' H, !tr_constant ⬝ Pp H) x + type_quotient.rec Pc (λa a' H, pathover_of_eq (Pp H)) x protected definition elim_on [reducible] {P : Type} (x : type_quotient R) (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := @@ -26,8 +26,8 @@ namespace type_quotient (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a') : ap (type_quotient.elim Pc Pp) (eq_of_rel R H) = Pp H := begin - apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel R H) (type_quotient.elim Pc Pp (class_of R a)))), - rewrite [-apd_eq_tr_constant_con_ap,↑type_quotient.elim,rec_eq_of_rel], + apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑type_quotient.elim,rec_eq_of_rel], end protected definition elim_type (Pc : A → Type) diff --git a/hott/init/default.hlean b/hott/init/default.hlean index 71a46b51a..72fdc34d3 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -10,7 +10,7 @@ import init.bool init.num init.priority init.relation init.wf import init.types import init.trunc init.path init.equiv init.util import init.ua init.funext -import init.hedberg init.nat init.hit +import init.hedberg init.nat init.hit init.pathover namespace core export bool empty unit sum diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 0dfadab67..cf328c141 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -28,7 +28,6 @@ structure equiv (A B : Type) := (to_fun : A → B) (to_is_equiv : is_equiv to_fun) - namespace is_equiv /- Some instances and closure properties of equivalences -/ postfix `⁻¹` := inv @@ -157,9 +156,13 @@ namespace is_equiv have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, left_inv f (g a)) - definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) := - adjointify (ap f) - (λq, (inverse (left_inv f x)) ⬝ ap f⁻¹ q ⬝ left_inv f y) + definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y := + (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y + + definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f : x = y → f x = f y) := + adjointify + (ap f) + (eq_of_fn_eq_fn' f) (λq, !ap_con ⬝ whisker_right !ap_con _ ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) @@ -252,7 +255,7 @@ namespace equiv protected definition refl [refl] [constructor] : A ≃ A := equiv.mk id !is_equiv_id - protected definition symm [symm] (f : A ≃ B) : B ≃ A := + protected definition symm [symm] [unfold-c 3] (f : A ≃ B) : B ≃ A := equiv.mk f⁻¹ !is_equiv_inv protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C := @@ -270,6 +273,12 @@ namespace equiv definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) := equiv.mk (transport P p) !is_equiv_tr + definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y := + (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y + + definition eq_of_fn_eq_fn_inv (f : A ≃ B) {x y : B} (q : f⁻¹ x = f⁻¹ y) : x = y := + (right_inv f x)⁻¹ ⬝ ap f q ⬝ right_inv f y + --we need this theorem for the funext_of_ua proof theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ := eq.rec_on p idp @@ -280,7 +289,10 @@ namespace equiv namespace ops infixl `⬝e`:75 := equiv.trans postfix `⁻¹` := equiv.symm -- overloaded notation for inverse - postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded + postfix [parsing-only] `⁻¹ᵉ`:(max + 1) := equiv.symm + -- notation for inverse which is not overloaded abbreviation erfl [constructor] := @equiv.refl end ops end equiv + +export [unfold-hints] equiv [unfold-hints] is_equiv diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index b30721405..4573904a7 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -8,7 +8,7 @@ Declaration of the primitive hits in Lean prelude -import .trunc +import .trunc .pathover open is_trunc eq @@ -55,12 +55,12 @@ namespace type_quotient : class_of R a = class_of R a' protected constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type} - (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') + (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') (x : type_quotient R) : P x protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type} (x : type_quotient R) (Pc : Π(a : A), P (class_of R a)) - (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') : P x := + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') : P x := type_quotient.rec Pc Pp x end type_quotient @@ -75,13 +75,13 @@ end trunc namespace type_quotient definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type} - (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') + (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') (a : A) : type_quotient.rec Pc Pp (class_of R a) = Pc a := idp constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type} - (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a') - {a a' : A} (H : R a a') : apd (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H + (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') + {a a' : A} (H : R a a') : apdo (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H end type_quotient attribute type_quotient.class_of trunc.tr [constructor] diff --git a/hott/init/init.md b/hott/init/init.md index cae694a9f..bd2839981 100644 --- a/hott/init/init.md +++ b/hott/init/init.md @@ -24,6 +24,7 @@ Datatypes and logic: HoTT basics: * [path](path.hlean) +* [pathover](pathover.hlean) * [hedberg](hedberg.hlean) * [trunc](trunc.hlean) * [equiv](equiv.hlean) diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean new file mode 100644 index 000000000..c47a60bbc --- /dev/null +++ b/hott/init/pathover.hlean @@ -0,0 +1,183 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Floris van Doorn + +Basic theorems about pathovers +-/ + +prelude +import .path .equiv + +open equiv is_equiv equiv.ops + +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₂} + +namespace eq + inductive pathover.{l} (B : A → Type.{l}) (b : B a) : Π{a₂ : A}, a = a₂ → B a₂ → Type.{l} := + idpatho : pathover B b (refl a) b + + notation b `=[`:50 p:0 `]`:0 b₂:50 := pathover _ b p b₂ + + definition idpo [reducible] [constructor] : b =[refl a] b := + pathover.idpatho b + + /- equivalences with equality using transport -/ + definition pathover_of_tr_eq (r : p ▸ b = b₂) : b =[p] b₂ := + by cases p; cases r; exact idpo + + definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ := + by cases p; cases r; exact idpo + + definition tr_eq_of_pathover (r : b =[p] b₂) : p ▸ b = b₂ := + by cases r; exact idp + + definition eq_tr_of_pathover (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ := + by cases r; exact idp + + definition pathover_equiv_tr_eq (p : a = a₂) (b : B a) (b₂ : B a₂) + : (b =[p] b₂) ≃ (p ▸ b = b₂) := + begin + fapply equiv.MK, + { exact tr_eq_of_pathover}, + { exact pathover_of_tr_eq}, + { intro r, cases p, cases r, apply idp}, + { intro r, cases r, apply idp}, + end + + definition pathover_equiv_eq_tr (p : a = a₂) (b : B a) (b₂ : B a₂) + : (b =[p] b₂) ≃ (b = p⁻¹ ▸ b₂) := + begin + fapply equiv.MK, + { exact eq_tr_of_pathover}, + { exact pathover_of_eq_tr}, + { intro r, cases p, cases r, apply idp}, + { intro r, cases r, apply idp}, + end + + definition pathover_tr (p : a = a₂) (b : B a) : b =[p] p ▸ b := + pathover_of_tr_eq idp + + definition tr_pathover (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b := + pathover_of_eq_tr 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 `⬝` := concato + infix `⬝o`:75 := concato + -- postfix `⁻¹` := inverseo + 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 -/ + + definition eq_of_pathover {a' a₂' : A'} (q : a' =[p] a₂') : a' = a₂' := + by cases q;reflexivity + + definition pathover_of_eq {a' a₂' : A'} (q : a' = a₂') : a' =[p] a₂' := + by cases p;cases q;exact idpo + + definition pathover_constant [constructor] (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' := + begin + fapply equiv.MK, + { exact eq_of_pathover}, + { exact pathover_of_eq}, + { 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_tr_eq idp b b' + + definition eq_of_pathover_idp {b' : B a} (q : b =[idpath a] b') : b = b' := + tr_eq_of_pathover q + + definition pathover_idp_of_eq {b' : B a} (q : b = b') : b =[idpath a] b' := + pathover_of_tr_eq q + + definition idp_rec_on [recursor] {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 + + definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ := + by cases p; exact idp + + definition apdo_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) : + apdo f p = pathover_of_eq (ap f p) := + eq.rec_on p idp + + definition pathover_of_pathover_tr (q : b =[p ⬝ p₂] p₂ ▸ b₂) : b =[p] b₂ := + by cases p₂;exact q + + definition pathover_tr_of_pathover {p : a = a₃} (q : b =[p ⬝ p₂⁻¹] b₂) : b =[p] p₂ ▸ b₂ := + by cases p₂;exact q + + definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) + : f a b = f a₂ b₂ := + by cases Hb; exact idp + + definition apo0111 (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂) + (Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ := + by cases Hb; apply (idp_rec_on Hc); apply idp + + definition apo11 {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 =[apo011 C p q] g b₂ := + by cases r; apply (idp_rec_on q); exact idpo + + definition apo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g) + {b : B a} : f b =[apo011 C p !pathover_tr] g (p ▸ b) := + by cases r; exact idpo + + +end eq diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 2f5c1f078..4e1f52418 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -11,7 +11,7 @@ Ported from Coq HoTT. --TODO: can we replace some definitions with a hprop as codomain by theorems? prelude -import .logic .equiv .types +import .logic .equiv .types .pathover open eq nat sigma unit namespace is_trunc @@ -270,6 +270,22 @@ namespace is_trunc (λ (u : unit), unit.rec_on u idp) (λ (x : A), center_eq x) + /- interaction with pathovers -/ + variables {C : A → Type} + {a a₂ : A} (p : a = a₂) + (c : C a) (c₂ : C a₂) + + definition is_hprop.elimo [H : is_hprop (C a)] : c =[p] c₂ := + pathover_of_eq_tr !is_hprop.elim + + definition is_trunc_pathover [instance] + (n : trunc_index) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) := + is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr + + variables {p c c₂} + theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' := + !is_hprop.elim + -- TODO: port "Truncated morphisms" end is_trunc diff --git a/hott/types/int/default.hlean b/hott/types/int/default.hlean index f83a9b73f..10147301e 100644 --- a/hott/types/int/default.hlean +++ b/hott/types/int/default.hlean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import .basic +import .basic .hott