From e7eb186315d82277028e28d8870c6ba0bc772928 Mon Sep 17 00:00:00 2001 From: tslil clingman <> Date: Wed, 17 Jul 2019 10:57:08 -0400 Subject: Init --- README.md | 5 ++ y_and_j.v | 254 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 259 insertions(+) create mode 100644 README.md create mode 100644 y_and_j.v diff --git a/README.md b/README.md new file mode 100644 index 0000000..332889d --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# A proof of Yoneda <-> Dependent path induction formalised in UniMath + +Write-up: pending + +Formalisation: [y_and_j.v](y_and_j/tree/master/y_and_j.v) diff --git a/y_and_j.v b/y_and_j.v new file mode 100644 index 0000000..b8db325 --- /dev/null +++ b/y_and_j.v @@ -0,0 +1,254 @@ +Require Import UniMath.Foundations.UnivalenceAxiom. + +Definition j_type + := ∑ (j : ∏ (A : UU) (a : A) (D : ∏ (b : A), a = b -> UU), + D a (idpath a) -> ∏ (b : A) (p : a = b), D b p), + ∏ (A : UU) (a : A) (D : ∏ (b : A) (p : a = b), UU) + (d : D a (idpath a)), j A a D d a (idpath a) = d. + +Definition nat_trans {A : UU} (F G : A -> UU) := ∏ (a : A), F a -> G a. + +Definition vert_comp {A : UU} {H G F : A -> UU} + (α : nat_trans G F) (β : nat_trans H G) : nat_trans H F + := λ a, (α a) ∘ (β a). + +Notation "α # β" := (vert_comp α β). + +Definition yoneda_type := + ∑ (y : ∏ (A : UU) (F : A -> UU) (a : A), + F a -> (nat_trans (λ b, a = b) F)), + (∏ (A : UU) (G F : A -> UU) (α : nat_trans G F) (a b : A) (p : a = b) + (x : G a), (α # y A G a x) b p = y A F a (α a x) b p) +× ((∏ (A : UU) (a b : A) (p : a = b) + , (y A (λ b, a = b) a (idpath a) b) p = p) + × (∏ (A : UU) (F : A -> UU) (a : A) (x : F a), + y A F a x a (idpath a) = x)). + +Section j_to_yoneda. + + Context (j : j_type). + + Definition j_derive_transport {A : UU} (F : A -> UU): + ∑ (transp : ∏ (a : A) (b : A) (p : a = b), F a -> F b), + ∏ (a : A), transp a a (idpath a) = λ x, x. + Proof. + exists (λ a, (pr1 j) A a (λ b _, F a -> F b) (λ x, x)). + exact (λ a, pr2 j A a (λ b _, F a -> F b) (λ x, x)). + Defined. + + Definition j_derive_idtohomot {A B : UU} {f g : A -> B}: + f = g -> ∏ (a : A), f a = g a + := (pr1 j) (A -> B) f (λ g p, ∏ (a : A), f a = g a) + (λ a, idpath _) g. + + Definition j_derive_path_concat {A : UU} {a b c : A}: + a = b -> b = c -> a = c + := (pr1 j) A a (λ b _, b = c -> a = c) (λ x, x) b. + + Definition j_derive_ap {A B : UU} (f : A -> B) {a b : A}: + a = b -> f a = f b + := (pr1 j) A a (λ b _, f a = f b) (idpath _) b. + + Definition j_derive_inv {A : UU} {a b : A}: + a = b -> b = a + := (pr1 j) A a (λ b _, b = a) (idpath _) b. + + Definition j_yoneda_fun (A : UU) (F : A -> UU) (a : A) (x : F a): + nat_trans (λ b, a = b) F + := λ b p, (pr1 (j_derive_transport F)) a b p x. + + Definition j_yoneda_naturality + (A : UU) (G F : A -> UU) (α : nat_trans G F) + (a b : A) (p : a = b) (x : G a) : + (α # j_yoneda_fun A G a x) b p = j_yoneda_fun A F a (α a x) b p. + Proof. + apply (λ d, (pr1 j) + A a (λ b p, (α # j_yoneda_fun A G a x) b p = + j_yoneda_fun A F a (α a x) b p) d b). + refine (j_derive_path_concat _ _). + - use (j_derive_ap (α a)). + + exact x. + + exact (j_derive_idtohomot + ((pr2 j) A a (λ b _ , G a → G b) (λ x,x)) x). + - apply j_derive_inv. + exact (j_derive_idtohomot + ((pr2 j) A a (λ b _, F a -> F b) (λ x,x)) + (α a x)). + Defined. + + Definition j_yoneda_special (A : UU) (a b : A) (p : a = b): + j_yoneda_fun A (λ b, a = b) a (idpath a) b p = p. + Proof. + apply ((pr1 j) A a + (λ b p, + j_yoneda_fun A (λ b0 : A, a = b0) + a (idpath a) b p = p)). + cbn. + exact (j_derive_idtohomot ((pr2 j) A a (λ b _ , a = a → a = b) + (λ x,x)) (idpath _)). + Defined. + + Definition j_yoneda_from (A : UU) (F : A -> UU) (a : A) + (α : nat_trans (λ b, a = b) F): F a + := α a (idpath a). + + Definition j_yoneda_fromto (A : UU) (F : A -> UU) (a : A): + (λ x, j_yoneda_from A F a (j_yoneda_fun A F a x)) = λ x, x + := pr2 (j_derive_transport F) a. + + Definition j_derive_y : yoneda_type. + exists j_yoneda_fun. + apply dirprodpair. + - exact j_yoneda_naturality. + - apply dirprodpair. + + exact j_yoneda_special. + + exact (λ A F a x, j_derive_idtohomot (j_yoneda_fromto A F a) x). + Defined. + +End j_to_yoneda. + +Section yoneda_to_j. + + Context (y_inhab : yoneda_type). + + Definition y := pr1 y_inhab. + Definition y_naturality := pr1 (pr2 y_inhab). + Definition y_special := pr1 (pr2 (pr2 y_inhab)). + Definition y_inverse := pr2 (pr2 (pr2 y_inhab)). + + Definition y_derive_ap {A B : UU} (f : A -> B) {a b : A} + (p : a = b) : f a = f b + := y A (λ b, f a = f b) a (idpath _) b p. + + Definition y_derive_pathcomp {A : UU} {a b c : A} + (p : a = b) (q : b = c) : a = c + := y A (λ c, a = c) b p c q. + + Definition y_derive_transp {A : UU} {B : A -> UU} + {a a' : A} : a = a' -> B a -> B a' + := y A (λ a', B a -> B a') a (λ b, b) a'. + + Definition y_derive_reverse {A : UU} {a b : A}: a = b -> b = a + := y A (λ x, x = a) a (idpath _) b. + + Definition y_total_paths {A : UU} {a b : A} (p : a = b): A -> UU + := (λ x, ∑ (q : a = x), (b ,, p) = (x ,, q)). + + Definition y_underlying {A : UU} {a : A}: + nat_trans (y_total_paths (idpath a)) (λ b, a = b) := λ _, pr1. + + Definition y_lift {A : UU} {a : A}: + nat_trans (λ b, a = b) (y_total_paths (idpath a)) + := y A (y_total_paths (idpath a)) a (idpath _ ,, idpath _). + + Definition y_lift_fixes_paths {A : UU} {a b : A} (p : a = b): + (y_underlying # y_lift) b p = p. + Proof. + refine (y_derive_pathcomp _ _) ; try apply y_naturality. + apply y_special. + Defined. + + Definition y_j_fun_bad (A : UU) (a : A) (D : ∏ (b : A), a = b -> UU) + (d : D a (idpath a)) (b : A) (p : a = b) : D b p. + Proof. + apply (y_derive_transp (y_lift_fixes_paths p)). + apply (λ d', y (∑ b0 : A, a = b0) + (λ bp, D (pr1 bp) (pr2 bp)) + (a,,idpath _) d' (b ,, pr1 (y_lift b p))). + - exact d. + - exact (pr2 (y_lift b p)). + Defined. + + Definition y_pathcomp_computes_right + {A : UU} {a : A}: ∏ (b : A) (p : a = b), + y_derive_pathcomp p (idpath b) = p. + Proof. + apply (y_j_fun_bad A a _). + unfold y_derive_pathcomp. + apply y_inverse. + Defined. + + Definition y_pathcomp_reveres_computes + {A : UU} {a : A}: ∏ (b : A) (p : a = b), + y_derive_pathcomp (y_derive_reverse p) p = idpath b. + Proof. + apply (y_j_fun_bad A a _). + refine (y_derive_pathcomp _ _). + - apply y_pathcomp_computes_right. + - exact (y_inverse A (λ x, x=a) a (idpath a)). + Defined. + + Definition y_embed_paths1 {A : UU} {a b : A} (p : a=b): + (a ,, idpath _) = (b ,, p). + Proof. + apply (y_derive_pathcomp (pr2 (y_lift b p))). + exact (@y_derive_ap _ _ (λ q, (b,,q)) + (pr1 (y_lift b p)) p + (y_lift_fixes_paths p)). + Defined. + + Definition y_embed_paths2 {A : UU} {a b : A} (p : a=b): + (a ,, idpath _) = (b ,, p). + Proof. + refine (y_derive_pathcomp _ _). + - exact (y_derive_reverse (y_embed_paths1 (idpath a))). + - exact (y_embed_paths1 p). + Defined. + + Definition y_embed_paths2_computes {A : UU} {a : A}: + y_embed_paths2 (idpath a) = idpath _. + Proof. + unfold y_embed_paths2. + apply y_pathcomp_reveres_computes. + Defined. + + Definition y_j_fun (A : UU) (a : A) (D : ∏ (b : A), a = b -> UU) + (d : D a (idpath a)) (b : A) (p : a = b) : D b p. + Proof. + apply (λ d', y (∑ b0 : A, a = b0) + (λ bp, D (pr1 bp) (pr2 bp)) + (a,,idpath _) d' (b ,, p)). + - exact d. + - apply y_embed_paths2. + Defined. + + Definition y_derive_j : j_type. + Proof. + exists y_j_fun. + intros. + refine (y_derive_pathcomp _ _). + unfold y_j_fun. + - apply y_derive_ap. + exact y_embed_paths2_computes. + - exact (y_inverse (∑ b, a=b) + (λ bp, D (pr1 bp) (pr2 bp)) + (a ,, idpath _) d). + Defined. + +End yoneda_to_j. + +Print All Dependencies y_derive_j. +Print All Dependencies j_derive_y. + + +(** This proof makes use of function extensionality twice. + + Notice however that it is _not_ used to derive a term of type + [yoneda_type]. With [j_derive_y] alone we may construct + [y_derive_j], as done above, from which we may then construct + [yoneda_tofrom]. + + That is, in the presence of function extensionality, [yoneda_type] + implies a Yoneda equivalence. *) +Definition yoneda_tofrom (j : j_type) (A : UU) (F : A -> UU) (a : A) + (α : nat_trans (λ b, a = b) F) : + j_yoneda_fun A F a (j_yoneda_from A F a α) = α. +Proof. + apply isweqtoforallpaths ; intro b. + apply funextfun ; intro p. + apply ((pr1 j) A a (λ b p, + j_yoneda_fun A F a (j_yoneda_from A F a α) b p = α b p)). + unfold j_yoneda_fun. + rewrite (pr2 (j_derive_transport F) a). + apply idpath. +Defined. -- cgit v1.2.3