fix(tests/lean/slow/path_groupoids): to reflect changes in the libraries
This commit is contained in:
Leonardo de Moura
parent
0eb52e1f8b
commit
ea7694ca32
1 changed files with 69 additions and 69 deletions
|
|
@ -29,10 +29,10 @@ definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
|
|||
path.rec (idpath x) p
|
||||
|
||||
infixl `⬝` := concat
|
||||
postfix `^`:100 := inverse
|
||||
postfix `**`:100 := inverse
|
||||
|
||||
-- In Coq, these are not needed, because concat and inv are kept transparent
|
||||
definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
|
||||
definition inv_1 {A : Type} (x : A) : (idpath x)** ≈ idpath x := idp
|
||||
|
||||
definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp
|
||||
|
||||
|
|
@ -58,45 +58,45 @@ definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r :
|
|||
path.rec_on r (path.rec_on q idp)
|
||||
|
||||
-- The left inverse law.
|
||||
definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p^ ≈ idp :=
|
||||
definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p** ≈ idp :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- The right inverse law.
|
||||
definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ ⬝ p ≈ idp :=
|
||||
definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p** ⬝ p ≈ idp :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
|
||||
-- redundant, following from earlier theorems.
|
||||
|
||||
definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ ⬝ (p ⬝ q) ≈ q :=
|
||||
definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p** ⬝ (p ⬝ q) ≈ q :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p^ ⬝ q) ≈ q :=
|
||||
definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p** ⬝ q) ≈ q :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q^ ≈ p :=
|
||||
definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q** ≈ p :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p :=
|
||||
definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
|
||||
path.rec_on q (take p, path.rec_on p idp) p
|
||||
|
||||
-- Inverse distributes over concatenation
|
||||
definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)^ ≈ q^ ⬝ p^ :=
|
||||
definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)** ≈ q** ⬝ p** :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ ⬝ q)^ ≈ q^ ⬝ p :=
|
||||
definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p** ⬝ q)** ≈ q** ⬝ p :=
|
||||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
-- universe metavariables
|
||||
definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q^)^ ≈ q ⬝ p^ :=
|
||||
definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q**)** ≈ q ⬝ p** :=
|
||||
path.rec_on p (λq, path.rec_on q idp) q
|
||||
|
||||
definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ ⬝ q^)^ ≈ q ⬝ p :=
|
||||
definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p** ⬝ q**)** ≈ q ⬝ p :=
|
||||
path.rec_on p (path.rec_on q idp)
|
||||
|
||||
-- Inverse is an involution.
|
||||
definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p^^ ≈ p :=
|
||||
definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p**** ≈ p :=
|
||||
path.rec_on p idp
|
||||
|
||||
|
||||
|
|
@ -104,72 +104,72 @@ path.rec_on p idp
|
|||
-- ----------------------------------------------
|
||||
|
||||
definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q :=
|
||||
have gen : Πp q, p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q, from
|
||||
p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q :=
|
||||
have gen : Πp q, p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q, from
|
||||
path.rec_on r
|
||||
(take p q,
|
||||
assume h : p ≈ idp^ ⬝ q,
|
||||
assume h : p ≈ idp** ⬝ q,
|
||||
show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _),
|
||||
gen p q
|
||||
|
||||
definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p^ → r ⬝ p ≈ q :=
|
||||
r ≈ q ⬝ p** → r ⬝ p ≈ q :=
|
||||
path.rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r
|
||||
|
||||
definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
p ≈ r ⬝ q → r^ ⬝ p ≈ q :=
|
||||
p ≈ r ⬝ q → r** ⬝ p ≈ q :=
|
||||
path.rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q
|
||||
|
||||
definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q ⬝ p → r ⬝ p^ ≈ q :=
|
||||
r ≈ q ⬝ p → r ⬝ p** ≈ q :=
|
||||
path.rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r
|
||||
|
||||
definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r^ ⬝ q ≈ p → q ≈ r ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
|
||||
r** ⬝ q ≈ p → q ≈ r ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
|
||||
|
||||
definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p^ ≈ r → q ≈ r ⬝ p :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
|
||||
q ⬝ p** ≈ r → q ≈ r ⬝ p :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
|
||||
|
||||
definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
r ⬝ q ≈ p → q ≈ r^ ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
|
||||
r ⬝ q ≈ p → q ≈ r** ⬝ p :=
|
||||
path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
|
||||
|
||||
definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
q ⬝ p ≈ r → q ≈ r ⬝ p^ :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
|
||||
q ⬝ p ≈ r → q ≈ r ⬝ p** :=
|
||||
path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
|
||||
|
||||
definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
p ⬝ q^ ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_p1 _)^ ⬝ h) p
|
||||
p ⬝ q** ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_p1 _)** ⬝ h) p
|
||||
|
||||
definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
q^ ⬝ p ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_1p _)^ ⬝ h) p
|
||||
q** ⬝ p ≈ idp → p ≈ q :=
|
||||
path.rec_on q (take p h, (concat_1p _)** ⬝ h) p
|
||||
|
||||
definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
p ⬝ q ≈ idp → p ≈ q^ :=
|
||||
path.rec_on q (take p h, (concat_p1 _)^ ⬝ h) p
|
||||
p ⬝ q ≈ idp → p ≈ q** :=
|
||||
path.rec_on q (take p h, (concat_p1 _)** ⬝ h) p
|
||||
|
||||
definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
q ⬝ p ≈ idp → p ≈ q^ :=
|
||||
path.rec_on q (take p h, (concat_1p _)^ ⬝ h) p
|
||||
q ⬝ p ≈ idp → p ≈ q** :=
|
||||
path.rec_on q (take p h, (concat_1p _)** ⬝ h) p
|
||||
|
||||
definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ p^ ⬝ q → p ≈ q :=
|
||||
idp ≈ p** ⬝ q → p ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ q ⬝ p^ → p ≈ q :=
|
||||
idp ≈ q ⬝ p** → p ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ q ⬝ p → p^ ≈ q :=
|
||||
idp ≈ q ⬝ p → p** ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ p ⬝ q → p^ ≈ q :=
|
||||
idp ≈ p ⬝ q → p** ≈ q :=
|
||||
path.rec_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
|
||||
|
|
@ -218,19 +218,19 @@ path.rec_on p idp
|
|||
-- ---------------------------------------------------
|
||||
|
||||
definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
u ≈ p^ # v → p # u ≈ v :=
|
||||
u ≈ p** # v → p # u ≈ v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
u ≈ p # v → p^ # u ≈ v :=
|
||||
u ≈ p # v → p** # u ≈ v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
|
||||
p # u ≈ v → u ≈ p^ # v :=
|
||||
p # u ≈ v → u ≈ p** # v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
|
||||
p^ # u ≈ v → u ≈ p # v :=
|
||||
p** # u ≈ v → u ≈ p # v :=
|
||||
path.rec_on p (take u v, id) u v
|
||||
|
||||
|
||||
|
|
@ -259,10 +259,10 @@ definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y
|
|||
path.rec_on p (take q, path.rec_on q (take r, concat_pp_p _ _ _)) q r
|
||||
|
||||
-- Functions commute with path inverses.
|
||||
definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)^ ≈ ap f (p^) :=
|
||||
definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)** ≈ ap f (p**) :=
|
||||
path.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)** :=
|
||||
path.rec_on p idp
|
||||
|
||||
-- TODO: rename id to idmap?
|
||||
|
|
@ -286,21 +286,21 @@ path.rec_on p idp
|
|||
-- Naturality of [ap].
|
||||
definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^)
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
|
||||
|
||||
-- Naturality of [ap] at identity.
|
||||
definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^)
|
||||
path.rec_on q (concat_1p _ ⬝ (concat_p1 _)**)
|
||||
|
||||
definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) :
|
||||
(p x) ⬝ (ap f q) ≈ q ⬝ (p y) :=
|
||||
path.rec_on q (concat_p1 _ ⬝ (concat_1p _)^)
|
||||
path.rec_on q (concat_p1 _ ⬝ (concat_1p _)**)
|
||||
|
||||
--TODO: note that the Coq proof for the preceding is
|
||||
--
|
||||
-- match q as i in (_ ≈ y) return (p x ⬝ ap f i ≈ i ⬝ p y) with
|
||||
-- | idpath => concat_p1 _ ⬝ (concat_1p _)^
|
||||
-- | idpath => concat_p1 _ ⬝ (concat_1p _)**
|
||||
-- end.
|
||||
--
|
||||
-- It is nice that we don't have to give the predicate.
|
||||
|
|
@ -324,7 +324,7 @@ definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h
|
|||
path.rec_on h (take h', path.rec_on h' idp) h'
|
||||
|
||||
definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
|
||||
apD10 (h^) x ≈ (apD10 h x)^ :=
|
||||
apD10 (h**) x ≈ (apD10 h x)** :=
|
||||
path.rec_on h idp
|
||||
|
||||
definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
|
||||
|
|
@ -332,7 +332,7 @@ definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
|
|||
definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x
|
||||
|
||||
definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h^) x ≈ (ap10 h x)^ := apD10_V h x
|
||||
definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h**) x ≈ (ap10 h x)** := apD10_V h x
|
||||
|
||||
-- [ap10] also behaves nicely on paths produced by [ap]
|
||||
definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
|
||||
|
|
@ -352,12 +352,12 @@ definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q
|
|||
path.rec_on q (path.rec_on p idp)
|
||||
|
||||
definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
|
||||
p # p^ # z ≈ z :=
|
||||
(transport_pp P (p^) p z)^ ⬝ ap (λr, transport P r z) (concat_Vp p)
|
||||
p # p** # z ≈ z :=
|
||||
(transport_pp P (p**) p z)** ⬝ ap (λr, transport P r z) (concat_Vp p)
|
||||
|
||||
definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
|
||||
p^ # p # z ≈ z :=
|
||||
(transport_pp P p (p^) z)^ ⬝ ap (λr, transport P r z) (concat_pV p)
|
||||
p** # p # z ≈ z :=
|
||||
(transport_pp P p (p**) z)** ⬝ ap (λr, transport P r z) (concat_pV p)
|
||||
|
||||
|
||||
-----------------------------------------------
|
||||
|
|
@ -392,7 +392,7 @@ theorem triple_induction
|
|||
path.rec_on p (take z q, path.rec_on q (take w r, path.rec_on r H)) z q w r
|
||||
|
||||
-- try this again
|
||||
definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p :=
|
||||
definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
|
||||
double_induction2 p q idp
|
||||
|
||||
definition transport_p_pp {A : Type} (P : A → Type)
|
||||
|
|
@ -431,14 +431,14 @@ path.rec_on r1 (path.rec_on r2 idp)
|
|||
|
||||
-- TODO: another interesting case
|
||||
definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
|
||||
transport2 Q (r^) z ≈ ((transport2 Q r z)^) :=
|
||||
transport2 Q (r**) z ≈ ((transport2 Q r z)**) :=
|
||||
-- path.rec_on r idp -- doesn't work
|
||||
path.rec_on r (idpath (inverse (transport2 Q (idpath p) z)))
|
||||
|
||||
definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
|
||||
(s : z ≈ w) :
|
||||
ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s :=
|
||||
path.rec_on r (concat_p1 _ ⬝ (concat_1p _)^)
|
||||
path.rec_on r (concat_p1 _ ⬝ (concat_1p _)**)
|
||||
|
||||
-- TODO (from Coq library): What should this be called?
|
||||
definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
|
||||
|
|
@ -465,7 +465,7 @@ path.rec_on p idp
|
|||
|
||||
definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) :
|
||||
transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y :=
|
||||
path.rec_on r (concat_1p _)^
|
||||
path.rec_on r (concat_1p _)**
|
||||
|
||||
-- Transporting in a pulled back fibration.
|
||||
definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
|
||||
|
|
@ -511,7 +511,7 @@ path.rec_on h (path.rec_on h' idp)
|
|||
infixl `⬝⬝`:75 := concat2
|
||||
|
||||
-- 2-dimensional path inversion
|
||||
definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p^ ≈ q^ :=
|
||||
definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p** ≈ q** :=
|
||||
path.rec_on h idp
|
||||
|
||||
-- Whiskering
|
||||
|
|
@ -528,7 +528,7 @@ h ⬝⬝ idp
|
|||
-- -------------------------------
|
||||
|
||||
definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
|
||||
path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)^ ⬝ a)) r q
|
||||
path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)** ⬝ a)) r q
|
||||
|
||||
definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
|
||||
path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
|
||||
|
|
@ -536,7 +536,7 @@ path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
|
|||
-- Whiskering and identity paths.
|
||||
|
||||
definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_p1 p)^ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
|
||||
(concat_p1 p)** ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
|
||||
path.rec_on h (path.rec_on p idp)
|
||||
|
||||
definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
|
|
@ -548,7 +548,7 @@ definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
|||
path.rec_on q idp
|
||||
|
||||
definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_1p p) ^ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
|
||||
(concat_1p p) ** ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
|
||||
path.rec_on h (path.rec_on p idp)
|
||||
|
||||
definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
|
|
@ -568,7 +568,7 @@ path.rec_on d (path.rec_on c (path.rec_on b (path.rec_on a idp)))
|
|||
|
||||
definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
|
||||
(whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
|
||||
path.rec_on b (path.rec_on a (concat_1p _)^)
|
||||
path.rec_on b (path.rec_on a (concat_1p _)**)
|
||||
|
||||
-- Structure corresponding to the coherence equations of a bicategory.
|
||||
|
||||
|
|
@ -586,12 +586,12 @@ definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
|||
path.rec_on p (take q, path.rec_on q idp) q
|
||||
|
||||
definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
|
||||
(whiskerR_p1 p ⬝⬝ whiskerL_1p q)^
|
||||
(whiskerR_p1 p ⬝⬝ whiskerL_1p q)**
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)
|
||||
⬝ (concat_whisker _ _ _ _ p q)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)^
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)^
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)**
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)**
|
||||
⬝ (whiskerL_1p q ⬝⬝ whiskerR_p1 p)
|
||||
|
||||
|
||||
|
|
@ -607,10 +607,10 @@ definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈
|
|||
(s : q ≈ q') :
|
||||
ap02 f (r ⬝⬝ s) ≈ ap_pp f p q
|
||||
⬝ (ap02 f r ⬝⬝ ap02 f s)
|
||||
⬝ (ap_pp f p' q')^ :=
|
||||
⬝ (ap_pp f p' q')** :=
|
||||
path.rec_on r (path.rec_on s (path.rec_on q (path.rec_on p idp)))
|
||||
|
||||
definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) :
|
||||
apD f p ≈ transport2 B r (f x) ⬝ apD f q :=
|
||||
path.rec_on r (concat_1p _)^
|
||||
path.rec_on r (concat_1p _)**
|
||||
end path
|
||||
|
|
|
|||
Loading…
Reference in a new issue