feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248
This commit is contained in:
Leonardo de Moura
parent
dea3357d7c
commit
6b89080b1a
4 changed files with 127 additions and 115 deletions
|
|
@ -33,5 +33,3 @@ trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
|
|||
definition minus_one := trunc_index.trunc_S trunc_index.minus_two
|
||||
definition IsHProp := IsTrunc minus_one
|
||||
definition IsHSet := IsTrunc (trunc_index.trunc_S minus_one)
|
||||
|
||||
prefix `!`:75 := center
|
||||
|
|
|
|||
|
|
@ -67,10 +67,22 @@ using notation::mk_ext_lua_action;
|
|||
using notation::transition;
|
||||
using notation::action;
|
||||
|
||||
static char const * g_forbidden_tokens[] = {"!", "@", nullptr};
|
||||
|
||||
void check_not_forbidden(char const * tk) {
|
||||
auto it = g_forbidden_tokens;
|
||||
while (*it) {
|
||||
if (strcmp(*it, tk) == 0)
|
||||
throw exception(sstream() << "invalid token `" << tk << "`, it is reserved");
|
||||
++it;
|
||||
}
|
||||
}
|
||||
|
||||
static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve)
|
||||
-> pair<notation_entry, optional<token_entry>> {
|
||||
std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
|
||||
char const * tks = tk.c_str();
|
||||
check_not_forbidden(tks);
|
||||
environment const & env = p.env();
|
||||
optional<token_entry> new_token;
|
||||
optional<unsigned> prec;
|
||||
|
|
@ -192,6 +204,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
|
|||
auto tk = p.get_name_val();
|
||||
auto tks = tk.to_string();
|
||||
auto tkcs = tks.c_str();
|
||||
check_not_forbidden(tkcs);
|
||||
p.next();
|
||||
if (p.curr_is_token(get_colon_tk())) {
|
||||
p.next();
|
||||
|
|
@ -205,6 +218,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
|
|||
return tk;
|
||||
} else if (p.curr_is_keyword()) {
|
||||
auto tk = p.get_token_info().token();
|
||||
check_not_forbidden(tk.to_string().c_str());
|
||||
p.next();
|
||||
return tk;
|
||||
} else {
|
||||
|
|
|
|||
|
|
@ -4,9 +4,9 @@ open path tactic
|
|||
open path (induction_on)
|
||||
|
||||
definition concat_whisker2 {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') :=
|
||||
(whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
|
||||
begin
|
||||
apply induction_on b,
|
||||
apply induction_on a,
|
||||
apply (concat_1p _)^,
|
||||
apply (concat_1p _)⁻¹,
|
||||
end
|
||||
|
|
|
|||
|
|
@ -38,71 +38,71 @@ path.rec (λu, u) q p
|
|||
definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
|
||||
path.rec (idpath x) p
|
||||
|
||||
infixl `@`:75 := concat
|
||||
infixl `⬝`:75 := concat
|
||||
postfix `^`:100 := inverse
|
||||
|
||||
-- In Coq, these are not needed, because concat and inv are kept transparent
|
||||
definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
|
||||
|
||||
definition concat_11 {A : Type} (x : A) : idpath x @ idpath x ≈ idpath x := idp
|
||||
definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp
|
||||
|
||||
|
||||
-- The 1-dimensional groupoid structure
|
||||
-- ------------------------------------
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p @ idp ≈ p :=
|
||||
definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p ⬝ idp ≈ p :=
|
||||
induction_on p idp
|
||||
|
||||
-- The identity path is a right unit.
|
||||
definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp @ p ≈ p :=
|
||||
definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp ⬝ p ≈ p :=
|
||||
induction_on p idp
|
||||
|
||||
-- Concatenation is associative.
|
||||
definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
p @ (q @ r) ≈ (p @ q) @ r :=
|
||||
p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r :=
|
||||
induction_on r (induction_on q idp)
|
||||
|
||||
definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) :
|
||||
(p @ q) @ r ≈ p @ (q @ r) :=
|
||||
(p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) :=
|
||||
induction_on r (induction_on q idp)
|
||||
|
||||
-- The left inverse law.
|
||||
definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p @ p^ ≈ idp :=
|
||||
definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p^ ≈ idp :=
|
||||
induction_on p idp
|
||||
|
||||
-- The right inverse law.
|
||||
definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ @ p ≈ idp :=
|
||||
definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ ⬝ p ≈ idp :=
|
||||
induction_on p idp
|
||||
|
||||
|
||||
-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
|
||||
-- redundant, following from earlier theorems.
|
||||
|
||||
definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ @ (p @ q) ≈ q :=
|
||||
definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ ⬝ (p ⬝ q) ≈ q :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p @ (p^ @ q) ≈ q :=
|
||||
definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p^ ⬝ q) ≈ q :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p @ q) @ q^ ≈ p :=
|
||||
definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q^ ≈ p :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p @ q^) @ q ≈ p :=
|
||||
definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p :=
|
||||
induction_on q (take p, induction_on p idp) p
|
||||
|
||||
-- Inverse distributes over concatenation
|
||||
definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p @ q)^ ≈ q^ @ p^ :=
|
||||
definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)^ ≈ q^ ⬝ p^ :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ @ q)^ ≈ q^ @ p :=
|
||||
definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ ⬝ q)^ ≈ q^ ⬝ p :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
-- universe metavariables
|
||||
definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p @ q^)^ ≈ q @ p^ :=
|
||||
definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q^)^ ≈ q ⬝ p^ :=
|
||||
induction_on p (λq, induction_on q idp) q
|
||||
|
||||
definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ @ q^)^ ≈ q @ p :=
|
||||
definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ ⬝ q^)^ ≈ q ⬝ p :=
|
||||
induction_on p (induction_on q idp)
|
||||
|
||||
-- Inverse is an involution.
|
||||
|
|
@ -114,73 +114,73 @@ induction_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
|
||||
induction_on r
|
||||
(take p q,
|
||||
assume h : p ≈ idp^ @ q,
|
||||
show idp @ p ≈ q, from concat_1p _ @ h @ concat_1p _),
|
||||
assume h : p ≈ idp^ ⬝ q,
|
||||
show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _),
|
||||
gen p q
|
||||
|
||||
definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q @ p^ → r @ p ≈ q :=
|
||||
induction_on p (take q r h, (concat_p1 _ @ h @ concat_p1 _)) q r
|
||||
r ≈ q ⬝ p^ → r ⬝ p ≈ q :=
|
||||
induction_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r
|
||||
|
||||
definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
p ≈ r @ q → r^ @ p ≈ q :=
|
||||
induction_on r (take p q h, concat_1p _ @ h @ concat_1p _) p q
|
||||
p ≈ r ⬝ q → r^ ⬝ p ≈ q :=
|
||||
induction_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q
|
||||
|
||||
definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
r ≈ q @ p → r @ p^ ≈ q :=
|
||||
induction_on p (take q r h, concat_p1 _ @ h @ concat_p1 _) q r
|
||||
r ≈ q ⬝ p → r ⬝ p^ ≈ q :=
|
||||
induction_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r
|
||||
|
||||
definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
r^ @ q ≈ p → q ≈ r @ p :=
|
||||
induction_on r (take p q h, (concat_1p _)^ @ h @ (concat_1p _)^) p q
|
||||
r^ ⬝ q ≈ p → q ≈ r ⬝ p :=
|
||||
induction_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
|
||||
|
||||
definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
|
||||
q @ p^ ≈ r → q ≈ r @ p :=
|
||||
induction_on p (take q r h, (concat_p1 _)^ @ h @ (concat_p1 _)^) q r
|
||||
q ⬝ p^ ≈ r → q ≈ r ⬝ p :=
|
||||
induction_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
|
||||
|
||||
definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
|
||||
r @ q ≈ p → q ≈ r^ @ p :=
|
||||
induction_on r (take p q h, (concat_1p _)^ @ h @ (concat_1p _)^) p q
|
||||
r ⬝ q ≈ p → q ≈ r^ ⬝ p :=
|
||||
induction_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
|
||||
|
||||
definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
|
||||
q @ p ≈ r → q ≈ r @ p^ :=
|
||||
induction_on p (take q r h, (concat_p1 _)^ @ h @ (concat_p1 _)^) q r
|
||||
q ⬝ p ≈ r → q ≈ r ⬝ p^ :=
|
||||
induction_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
|
||||
|
||||
definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
p @ q^ ≈ idp → p ≈ q :=
|
||||
induction_on q (take p h, (concat_p1 _)^ @ h) p
|
||||
p ⬝ q^ ≈ idp → p ≈ q :=
|
||||
induction_on q (take p h, (concat_p1 _)^ ⬝ h) p
|
||||
|
||||
definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
q^ @ p ≈ idp → p ≈ q :=
|
||||
induction_on q (take p h, (concat_1p _)^ @ h) p
|
||||
q^ ⬝ p ≈ idp → p ≈ q :=
|
||||
induction_on q (take p h, (concat_1p _)^ ⬝ h) p
|
||||
|
||||
definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
p @ q ≈ idp → p ≈ q^ :=
|
||||
induction_on q (take p h, (concat_p1 _)^ @ h) p
|
||||
p ⬝ q ≈ idp → p ≈ q^ :=
|
||||
induction_on q (take p h, (concat_p1 _)^ ⬝ h) p
|
||||
|
||||
definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
q @ p ≈ idp → p ≈ q^ :=
|
||||
induction_on q (take p h, (concat_1p _)^ @ h) p
|
||||
q ⬝ p ≈ idp → p ≈ q^ :=
|
||||
induction_on q (take p h, (concat_1p _)^ ⬝ h) p
|
||||
|
||||
definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ p^ @ q → p ≈ q :=
|
||||
induction_on p (take q h, h @ (concat_1p _)) q
|
||||
idp ≈ p^ ⬝ q → p ≈ q :=
|
||||
induction_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) :
|
||||
idp ≈ q @ p^ → p ≈ q :=
|
||||
induction_on p (take q h, h @ (concat_p1 _)) q
|
||||
idp ≈ q ⬝ p^ → p ≈ q :=
|
||||
induction_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ q @ p → p^ ≈ q :=
|
||||
induction_on p (take q h, h @ (concat_p1 _)) q
|
||||
idp ≈ q ⬝ p → p^ ≈ q :=
|
||||
induction_on p (take q h, h ⬝ (concat_p1 _)) q
|
||||
|
||||
definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
|
||||
idp ≈ p @ q → p^ ≈ q :=
|
||||
induction_on p (take q h, h @ (concat_1p _)) q
|
||||
idp ≈ p ⬝ q → p^ ≈ q :=
|
||||
induction_on p (take q h, h ⬝ (concat_1p _)) q
|
||||
|
||||
|
||||
-- Transport
|
||||
|
|
@ -257,15 +257,15 @@ definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f
|
|||
|
||||
-- Functions commute with concatenation.
|
||||
definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
ap f (p @ q) ≈ (ap f p) @ (ap f q) :=
|
||||
ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) :
|
||||
r @ (ap f (p @ q)) ≈ (r @ ap f p) @ (ap f q) :=
|
||||
r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) :=
|
||||
induction_on p (take r q, induction_on q (concat_p_pp r idp idp)) r q
|
||||
|
||||
definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) :
|
||||
(ap f (p @ q)) @ r ≈ (ap f p) @ (ap f q @ r) :=
|
||||
(ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) :=
|
||||
induction_on p (take q, induction_on q (take r, concat_pp_p _ _ _)) q r
|
||||
|
||||
-- Functions commute with path inverses.
|
||||
|
|
@ -295,22 +295,22 @@ induction_on p idp
|
|||
|
||||
-- Naturality of [ap].
|
||||
definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) @ (p y) ≈ (p x) @ (ap g q) :=
|
||||
induction_on q (concat_1p _ @ (concat_p1 _)^)
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
|
||||
induction_on q (concat_1p _ ⬝ (concat_p1 _)^)
|
||||
|
||||
-- Naturality of [ap] at identity.
|
||||
definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) :
|
||||
(ap f q) @ (p y) ≈ (p x) @ q :=
|
||||
induction_on q (concat_1p _ @ (concat_p1 _)^)
|
||||
(ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
|
||||
induction_on q (concat_1p _ ⬝ (concat_p1 _)^)
|
||||
|
||||
definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) :
|
||||
(p x) @ (ap f q) ≈ q @ (p y) :=
|
||||
induction_on q (concat_p1 _ @ (concat_1p _)^)
|
||||
(p x) ⬝ (ap f q) ≈ q ⬝ (p y) :=
|
||||
induction_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 _)^
|
||||
-- match q as i in (_ ≈ y) return (p x ⬝ ap f i ≈ i ⬝ p y) with
|
||||
-- | idpath => concat_p1 _ ⬝ (concat_1p _)^
|
||||
-- end.
|
||||
--
|
||||
-- It is nice that we don't have to give the predicate.
|
||||
|
|
@ -319,7 +319,7 @@ induction_on q (concat_p1 _ @ (concat_1p _)^)
|
|||
definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
|
||||
{x y : A} (q : x ≈ y)
|
||||
{w z : B} (r : w ≈ f x) (s : g y ≈ z) :
|
||||
(r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (ap g q @ s) :=
|
||||
(r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) :=
|
||||
induction_on q (take s, induction_on s (take r, idp)) s r
|
||||
|
||||
-- Action of [apD10] and [ap10] on paths
|
||||
|
|
@ -330,7 +330,7 @@ induction_on q (take s, induction_on s (take r, idp)) s r
|
|||
definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
apD10 (h @ h') x ≈ apD10 h x @ apD10 h' x :=
|
||||
apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x :=
|
||||
induction_on h (take h', induction_on h' idp) h'
|
||||
|
||||
definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
|
||||
|
|
@ -340,7 +340,7 @@ induction_on h idp
|
|||
definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
|
||||
|
||||
definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
|
||||
ap10 (h @ h') x ≈ ap10 h x @ ap10 h' x := apD10_pp h h' x
|
||||
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
|
||||
|
||||
|
|
@ -358,16 +358,16 @@ induction_on p idp
|
|||
-- : idp # u ≈ u := idp
|
||||
|
||||
definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
|
||||
p @ q # u ≈ q # p # u :=
|
||||
p ⬝ q # u ≈ q # p # u :=
|
||||
induction_on q (induction_on p idp)
|
||||
|
||||
definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
|
||||
p # p^ # z ≈ z :=
|
||||
(transport_pp P (p^) p z)^ @ ap (λr, transport P r z) (concat_Vp p)
|
||||
(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)
|
||||
(transport_pp P p (p^) z)^ ⬝ ap (λr, transport P r z) (concat_pV p)
|
||||
|
||||
|
||||
-----------------------------------------------
|
||||
|
|
@ -402,15 +402,15 @@ theorem triple_induction
|
|||
induction_on p (take z q, induction_on q (take w r, induction_on r H)) z q w r
|
||||
|
||||
-- try this again
|
||||
definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p @ q^) @ q ≈ p :=
|
||||
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)
|
||||
{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 (λ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) :=
|
||||
triple_induction p q r (take u, idp) u
|
||||
|
||||
-- Here is another coherence lemma for transport.
|
||||
|
|
@ -436,7 +436,7 @@ induction_on r idp
|
|||
|
||||
definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y}
|
||||
(r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) :
|
||||
transport2 P (r1 @ r2) z ≈ transport2 P r1 z @ transport2 P r2 z :=
|
||||
transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z :=
|
||||
induction_on r1 (induction_on r2 idp)
|
||||
|
||||
-- TODO: another interesting case
|
||||
|
|
@ -447,8 +447,8 @@ induction_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 :=
|
||||
induction_on r (concat_p1 _ @ (concat_1p _)^)
|
||||
ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s :=
|
||||
induction_on r (concat_p1 _ ⬝ (concat_1p _)^)
|
||||
|
||||
-- TODO (from Coq library): What should this be called?
|
||||
definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
|
||||
|
|
@ -474,7 +474,7 @@ definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) :
|
|||
induction_on p idp
|
||||
|
||||
definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) :
|
||||
transport_const p y ≈ transport2 (λu, B) r y @ transport_const q y :=
|
||||
transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y :=
|
||||
induction_on r (concat_1p _)^
|
||||
|
||||
-- Transporting in a pulled back fibration.
|
||||
|
|
@ -506,7 +506,7 @@ induction_on p (idpath (transport (λ (z : Type), z) (ap P (idpath x)) u))
|
|||
|
||||
-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const].
|
||||
definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) :
|
||||
apD f p ≈ transport_const p (f x) @ ap f p :=
|
||||
apD f p ≈ transport_const p (f x) ⬝ ap f p :=
|
||||
induction_on p idp
|
||||
|
||||
|
||||
|
|
@ -515,10 +515,10 @@ induction_on p idp
|
|||
|
||||
-- Horizontal composition of 2-dimensional paths.
|
||||
definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') :
|
||||
p @ q ≈ p' @ q' :=
|
||||
p ⬝ q ≈ p' ⬝ q' :=
|
||||
induction_on h (induction_on h' idp)
|
||||
|
||||
infixl `@@`:75 := concat2
|
||||
infixl `⬝⬝`:75 := concat2
|
||||
|
||||
-- 2-dimensional path inversion
|
||||
definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p^ ≈ q^ :=
|
||||
|
|
@ -527,57 +527,57 @@ induction_on h idp
|
|||
-- Whiskering
|
||||
-- ----------
|
||||
|
||||
definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p @ q ≈ p @ r :=
|
||||
idp @@ h
|
||||
definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r :=
|
||||
idp ⬝⬝ h
|
||||
|
||||
definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p @ r ≈ q @ r :=
|
||||
h @@ idp
|
||||
definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r :=
|
||||
h ⬝⬝ idp
|
||||
|
||||
|
||||
-- Unwhiskering, a.k.a. cancelling
|
||||
-- -------------------------------
|
||||
|
||||
definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p @ q ≈ p @ r) → (q ≈ r) :=
|
||||
induction_on p (take r, induction_on r (take q a, (concat_1p q)^ @ a)) r q
|
||||
definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
|
||||
induction_on p (take r, induction_on r (take q a, (concat_1p q)^ ⬝ a)) r q
|
||||
|
||||
definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p @ r ≈ q @ r) → (p ≈ q) :=
|
||||
induction_on r (take p, induction_on p (take q a, a @ concat_p1 q)) p q
|
||||
definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
|
||||
induction_on r (take p, induction_on p (take q a, a ⬝ concat_p1 q)) p q
|
||||
|
||||
-- Whiskering and identity paths.
|
||||
|
||||
definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_p1 p)^ @ whiskerR h idp @ concat_p1 q ≈ h :=
|
||||
(concat_p1 p)^ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
|
||||
induction_on h (induction_on p idp)
|
||||
|
||||
definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerR idp q ≈ idp :> (p @ q ≈ p @ q) :=
|
||||
whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
induction_on q idp
|
||||
|
||||
definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
whiskerL p idp ≈ idp :> (p @ q ≈ p @ q) :=
|
||||
whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) :=
|
||||
induction_on q idp
|
||||
|
||||
definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
(concat_1p p) ^ @ whiskerL idp h @ concat_1p q ≈ h :=
|
||||
(concat_1p p) ^ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
|
||||
induction_on h (induction_on p idp)
|
||||
|
||||
definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
h @@ idp ≈ whiskerR h idp :> (p @ idp ≈ q @ idp) :=
|
||||
h ⬝⬝ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) :=
|
||||
induction_on h idp
|
||||
|
||||
definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
|
||||
idp @@ h ≈ whiskerL idp h :> (idp @ p ≈ idp @ q) :=
|
||||
idp ⬝⬝ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) :=
|
||||
induction_on h idp
|
||||
|
||||
-- TODO: note, 4 inductions
|
||||
-- The interchange law for concatenation.
|
||||
definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z}
|
||||
(a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') :
|
||||
(a @@ c) @ (b @@ d) ≈ (a @ b) @@ (c @ d) :=
|
||||
(a ⬝⬝ c) ⬝ (b ⬝⬝ d) ≈ (a ⬝ b) ⬝⬝ (c ⬝ d) :=
|
||||
induction_on d (induction_on c (induction_on b (induction_on a idp)))
|
||||
|
||||
definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
|
||||
(whiskerR a q) @ (whiskerL p' b) ≈ (whiskerL p b) @ (whiskerR a q') :=
|
||||
(whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
|
||||
induction_on b (induction_on a (concat_1p _)^)
|
||||
|
||||
-- Structure corresponding to the coherence equations of a bicategory.
|
||||
|
|
@ -585,24 +585,24 @@ induction_on b (induction_on a (concat_1p _)^)
|
|||
-- The "pentagonator": the 3-cell witnessing the associativity pentagon.
|
||||
definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) :
|
||||
whiskerL p (concat_p_pp q r s)
|
||||
@ concat_p_pp p (q @ r) s
|
||||
@ whiskerR (concat_p_pp p q r) s
|
||||
≈ concat_p_pp p q (r @ s) @ concat_p_pp (p @ q) r s :=
|
||||
⬝ 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 :=
|
||||
induction_on p (take q, induction_on q (take r, induction_on r (take s, induction_on s idp))) q r s
|
||||
|
||||
-- The 3-cell witnessing the left unit triangle.
|
||||
definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
|
||||
concat_p_pp p idp q @ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
|
||||
concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) :=
|
||||
induction_on p (take q, induction_on q idp) q
|
||||
|
||||
definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p @ q ≈ q @ p :=
|
||||
(whiskerR_p1 p @@ whiskerL_1p q)^
|
||||
@ (concat_p1 _ @@ concat_p1 _)
|
||||
@ (concat_1p _ @@ concat_1p _)
|
||||
@ (concat_whisker _ _ _ _ p q)
|
||||
@ (concat_1p _ @@ concat_1p _)^
|
||||
@ (concat_p1 _ @@ concat_p1 _)^
|
||||
@ (whiskerL_1p q @@ whiskerR_p1 p)
|
||||
definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
|
||||
(whiskerR_p1 p ⬝⬝ whiskerL_1p q)^
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)
|
||||
⬝ (concat_whisker _ _ _ _ p q)
|
||||
⬝ (concat_1p _ ⬝⬝ concat_1p _)^
|
||||
⬝ (concat_p1 _ ⬝⬝ concat_p1 _)^
|
||||
⬝ (whiskerL_1p q ⬝⬝ whiskerR_p1 p)
|
||||
|
||||
|
||||
-- The action of functions on 2-dimensional paths
|
||||
|
|
@ -610,16 +610,16 @@ definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q)
|
|||
induction_on r idp
|
||||
|
||||
definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') :
|
||||
ap02 f (r @ r') ≈ ap02 f r @ ap02 f r' :=
|
||||
ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' :=
|
||||
induction_on r (induction_on r' idp)
|
||||
|
||||
definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p')
|
||||
(s : q ≈ q') :
|
||||
ap02 f (r @@ s) ≈ ap_pp f p q
|
||||
@ (ap02 f r @@ ap02 f s)
|
||||
@ (ap_pp f p' q')^ :=
|
||||
ap02 f (r ⬝⬝ s) ≈ ap_pp f p q
|
||||
⬝ (ap02 f r ⬝⬝ ap02 f s)
|
||||
⬝ (ap_pp f p' q')^ :=
|
||||
induction_on r (induction_on s (induction_on q (induction_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 :=
|
||||
apD f p ≈ transport2 B r (f x) ⬝ apD f q :=
|
||||
induction_on r (concat_1p _)^
|
||||
|
|
|
|||
Loading…
Reference in a new issue