From cf9f4e566b87d2875f757bb7d54ee4421988e315 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 10 May 2019 12:32:07 +0200 Subject: Make detyping robust w.r.t. indexed anonymous variables I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026. --- dev/top_printers.ml | 1 - pretyping/detyping.ml | 13 +- pretyping/detyping.mli | 3 - test-suite/bugs/closed/bug_10026.v | 3 + test-suite/bugs/closed/bug_3754.v | 287 +++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/bug_3754.v | 285 ------------------------------------ 6 files changed, 296 insertions(+), 296 deletions(-) create mode 100644 test-suite/bugs/closed/bug_10026.v create mode 100644 test-suite/bugs/closed/bug_3754.v delete mode 100644 test-suite/bugs/opened/bug_3754.v diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 816316487c..2cd8cc3a74 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,7 +27,6 @@ open Clenv let _ = Detyping.print_evar_arguments := true let _ = Detyping.print_universes := true let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false -let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found) (* std_ppcmds *) let pp x = Pp.pp_with !Topfmt.std_ft x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 062e3ca8b2..82726eccf0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -708,9 +708,6 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable.")) -let set_detype_anonymous f = detype_anonymous := f - let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in GType (UNamed l) @@ -732,11 +729,13 @@ and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar id - | Anonymous -> GVar (!detype_anonymous n) + | Name id -> GVar id + | Anonymous -> + let s = "_ANONYMOUS_REL_"^(string_of_int n) in + GVar (Id.of_string s) with Not_found -> - let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (Id.of_string s)) + let s = "_UNBOUND_REL_"^(string_of_int n) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 1a8e97efb8..00b0578a52 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -68,9 +68,6 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> clo val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -(* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit - val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v new file mode 100644 index 0000000000..0d3142d0f2 --- /dev/null +++ b/test-suite/bugs/closed/bug_10026.v @@ -0,0 +1,3 @@ +Require Import Coq.Lists.List. +Set Debug RAKAM. +Check fun _ => fold_right (fun A B => prod A B) unit _. diff --git a/test-suite/bugs/closed/bug_3754.v b/test-suite/bugs/closed/bug_3754.v new file mode 100644 index 0000000000..7031cbf132 --- /dev/null +++ b/test-suite/bugs/closed/bug_3754.v @@ -0,0 +1,287 @@ +Unset Strict Universe Declaration. +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) +(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 + coqtop version trunk (October 2014) *) + +Notation Type0 := Set. + +Notation idmap := (fun x => x). + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. + +Notation pr1 := projT1. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. + +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := + fun x => g (f x). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. +admit. +Defined. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p q) (at level 20) : path_scope. + +Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope. + +Notation "p @' q" := (concat p q) (at level 21, left associativity, + format "'[v' p '/' '@'' q ']'") : long_path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. +exact (match p with idpath => u end). +Defined. + +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. +exact (match p with idpath => idpath end). +Defined. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B} f {_} _. + +Record Equiv A B := BuildEquiv { + equiv_fun : A -> B ; + equiv_isequiv : IsEquiv equiv_fun +}. + +Coercion equiv_fun : Equiv >-> Funclass. + +Global Existing Instance equiv_isequiv. + +Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Local Open Scope path_scope. + +Definition concat_p1 {A : Type} {x y : A} (p : x = y) : + p @ 1 = p + := + match p with idpath => 1 end. + +Definition concat_1p {A : Type} {x y : A} (p : x = y) : + 1 @ p = p + := + match p with idpath => 1 end. + +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 := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +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) := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : + r^ @ q = p -> q = r @ p. +admit. +Defined. + +Ltac with_rassoc tac := + repeat rewrite concat_pp_p; + tac; + + repeat rewrite concat_p_pp. + +Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp). + +Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A} + (r : w = f x) (p : x = y) (q : y = z) : + r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q). +admit. +Defined. + +Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : + ap (g o f) p = ap g (ap f p) + := + match p with idpath => 1 end. + +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) + := + match q with + | idpath => concat_1p _ @ ((concat_p1 _) ^) + end. + +Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) + {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) + : D x2 (p # y) (p # z) + := + match p with idpath => w end. +Local Open Scope equiv_scope. + +Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2) + : (transport (fun x => B x -> C) p f) y = f (p^ # y). +admit. +Defined. + +Definition transport_arrow_fromconst {A B : Type} {C : A -> Type} + {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B) + : (transport (fun x => B -> C x) p f) y = p # (f y). +admit. +Defined. + +Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) + : ap (transport (fun x => B x -> C) p f) q + @ transport_arrow_toconst p f y2 + = transport_arrow_toconst p f y1 + @ ap (fun y => f (p^ # y)) q. +admit. +Defined. + +Class Univalence. +Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B). +admit. +Defined. +Definition transport_path_universe + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A) + : transport (fun X:Type => X) (path_universe f) z = f z. +admit. +Defined. +Definition transport_path_universe_V `{Funext} + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) + : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z. +admit. +Defined. + +Ltac simpl_do_clear tac term := + let H := fresh in + assert (H := term); + simpl in H |- *; + tac H; + clear H. + +Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term. + +Global Instance Univalence_implies_Funext `{Univalence} : Funext. +Admitted. + +Section Factorization. + + Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)} + {A B : Type@{i}} {f : A -> B}. + + Record Factorization := + { intermediate : Type ; + factor1 : A -> intermediate ; + factor2 : intermediate -> B ; + fact_factors : factor2 o factor1 == f ; + inclass1 : class1 _ _ factor1 ; + inclass2 : class2 _ _ factor2 + }. + + Record PathFactorization {fact fact' : Factorization} := + { path_intermediate : intermediate fact <~> intermediate fact' ; + path_factor1 : path_intermediate o factor1 fact == factor1 fact' ; + path_factor2 : factor2 fact == factor2 fact' o path_intermediate ; + path_fact_factors : forall a, path_factor2 (factor1 fact a) + @ ap (factor2 fact') (path_factor1 a) + @ fact_factors fact' a + = fact_factors fact a + }. + Context `{Univalence} {fact fact' : Factorization} + (pf : @PathFactorization fact fact'). + + Let II := path_intermediate pf. + Let ff1 := path_factor1 pf. + Let ff2 := path_factor2 pf. +Local Definition II' : intermediate fact = intermediate fact'. +admit. +Defined. + + Local Definition fff' (a : A) + : (transportD2 (fun X => A -> X) (fun X => X -> B) + (fun X g h => {_ : forall a : A, h (g a) = f a & + {_ : class1 A X g & class2 X B h}}) + II' (factor1 fact) (factor2 fact) + (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a = + ap (transport (fun X => X -> B) II' (factor2 fact)) + (transport_arrow_fromconst II' (factor1 fact) a + @ transport_path_universe II (factor1 fact a) + @ ff1 a) + @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a) + @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a)) + @ ff2 (II^-1 (factor1 fact' a)) + @ ap (factor2 fact') (eisretr II (factor1 fact' a)) + @ fact_factors fact' a. + Proof. + + Open Scope long_path_scope. + + rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)). + + simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^) + (factor2 fact)). + rewrite <- ap_p_pp; rewrite_moveL_Mp_p. + Set Debug Tactic Unification. + rewrite (concat_Ap ff2). + Abort. + +End Factorization. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v deleted file mode 100644 index 18820b1a4c..0000000000 --- a/test-suite/bugs/opened/bug_3754.v +++ /dev/null @@ -1,285 +0,0 @@ -Unset Strict Universe Declaration. -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) -(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 - coqtop version trunk (October 2014) *) - -Notation Type0 := Set. - -Notation idmap := (fun x => x). - -Notation "( x ; y )" := (existT _ x y) : fibration_scope. -Open Scope fibration_scope. - -Notation pr1 := projT1. - -Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. - -Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := - fun x => g (f x). - -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. - -Inductive paths {A : Type} (a : A) : A -> Type := - idpath : paths a a. - -Arguments idpath {A a} , [A] a. - -Notation "x = y :> A" := (@paths A x y) : type_scope. -Notation "x = y" := (x = y :>_) : type_scope. -Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. -admit. -Defined. - -Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := - match p, q with idpath, idpath => idpath end. - -Notation "1" := idpath : path_scope. - -Notation "p @ q" := (concat p q) (at level 20) : path_scope. - -Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope. - -Notation "p @' q" := (concat p q) (at level 21, left associativity, - format "'[v' p '/' '@'' q ']'") : long_path_scope. -Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. -exact (match p with idpath => u end). -Defined. - -Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. -exact (match p with idpath => idpath end). -Defined. - -Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) - := forall x:A, f x = g x. - -Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. - -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := - forall x : A, r (s x) = x. - -Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { - equiv_inv : B -> A ; - eisretr : Sect equiv_inv f; - eissect : Sect f equiv_inv; - eisadj : forall x : A, eisretr (f x) = ap f (eissect x) -}. - -Arguments eisretr {A B} f {_} _. - -Record Equiv A B := BuildEquiv { - equiv_fun : A -> B ; - equiv_isequiv : IsEquiv equiv_fun -}. - -Coercion equiv_fun : Equiv >-> Funclass. - -Global Existing Instance equiv_isequiv. - -Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. - -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. - -Class Contr_internal (A : Type) := BuildContr { - center : A ; - contr : (forall y : A, center = y) -}. - -Inductive trunc_index : Type := -| minus_two : trunc_index -| trunc_S : trunc_index -> trunc_index. - -Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. -Local Open Scope trunc_scope. -Notation "-2" := minus_two (at level 0) : trunc_scope. -Notation "-1" := (-2.+1) (at level 0) : trunc_scope. - -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | -2 => Contr_internal A - | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) - end. - -Class IsTrunc (n : trunc_index) (A : Type) : Type := - Trunc_is_trunc : IsTrunc_internal n A. -Notation IsHProp := (IsTrunc -1). - -Monomorphic Axiom dummy_funext_type : Type0. -Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. - -Local Open Scope path_scope. - -Definition concat_p1 {A : Type} {x y : A} (p : x = y) : - p @ 1 = p - := - match p with idpath => 1 end. - -Definition concat_1p {A : Type} {x y : A} (p : x = y) : - 1 @ p = p - := - match p with idpath => 1 end. - -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 := - match r with idpath => - match q with idpath => - match p with idpath => 1 - end end end. - -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) := - match r with idpath => - match q with idpath => - match p with idpath => 1 - end end end. - -Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : - r^ @ q = p -> q = r @ p. -admit. -Defined. - -Ltac with_rassoc tac := - repeat rewrite concat_pp_p; - tac; - - repeat rewrite concat_p_pp. - -Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp). - -Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A} - (r : w = f x) (p : x = y) (q : y = z) : - r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q). -admit. -Defined. - -Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : - ap (g o f) p = ap g (ap f p) - := - match p with idpath => 1 end. - -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) - := - match q with - | idpath => concat_1p _ @ ((concat_p1 _) ^) - end. - -Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) - {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) - : D x2 (p # y) (p # z) - := - match p with idpath => w end. -Local Open Scope equiv_scope. - -Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} - {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2) - : (transport (fun x => B x -> C) p f) y = f (p^ # y). -admit. -Defined. - -Definition transport_arrow_fromconst {A B : Type} {C : A -> Type} - {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B) - : (transport (fun x => B -> C x) p f) y = p # (f y). -admit. -Defined. - -Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} - {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) - : ap (transport (fun x => B x -> C) p f) q - @ transport_arrow_toconst p f y2 - = transport_arrow_toconst p f y1 - @ ap (fun y => f (p^ # y)) q. -admit. -Defined. - -Class Univalence. -Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B). -admit. -Defined. -Definition transport_path_universe - {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A) - : transport (fun X:Type => X) (path_universe f) z = f z. -admit. -Defined. -Definition transport_path_universe_V `{Funext} - {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) - : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z. -admit. -Defined. - -Ltac simpl_do_clear tac term := - let H := fresh in - assert (H := term); - simpl in H |- *; - tac H; - clear H. - -Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term. - -Global Instance Univalence_implies_Funext `{Univalence} : Funext. -Admitted. - -Section Factorization. - - Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}} - `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)} - `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)} - {A B : Type@{i}} {f : A -> B}. - - Record Factorization := - { intermediate : Type ; - factor1 : A -> intermediate ; - factor2 : intermediate -> B ; - fact_factors : factor2 o factor1 == f ; - inclass1 : class1 _ _ factor1 ; - inclass2 : class2 _ _ factor2 - }. - - Record PathFactorization {fact fact' : Factorization} := - { path_intermediate : intermediate fact <~> intermediate fact' ; - path_factor1 : path_intermediate o factor1 fact == factor1 fact' ; - path_factor2 : factor2 fact == factor2 fact' o path_intermediate ; - path_fact_factors : forall a, path_factor2 (factor1 fact a) - @ ap (factor2 fact') (path_factor1 a) - @ fact_factors fact' a - = fact_factors fact a - }. - Context `{Univalence} {fact fact' : Factorization} - (pf : @PathFactorization fact fact'). - - Let II := path_intermediate pf. - Let ff1 := path_factor1 pf. - Let ff2 := path_factor2 pf. -Local Definition II' : intermediate fact = intermediate fact'. -admit. -Defined. - - Local Definition fff' (a : A) - : (transportD2 (fun X => A -> X) (fun X => X -> B) - (fun X g h => {_ : forall a : A, h (g a) = f a & - {_ : class1 A X g & class2 X B h}}) - II' (factor1 fact) (factor2 fact) - (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a = - ap (transport (fun X => X -> B) II' (factor2 fact)) - (transport_arrow_fromconst II' (factor1 fact) a - @ transport_path_universe II (factor1 fact a) - @ ff1 a) - @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a) - @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a)) - @ ff2 (II^-1 (factor1 fact' a)) - @ ap (factor2 fact') (eisretr II (factor1 fact' a)) - @ fact_factors fact' a. - Proof. - - Open Scope long_path_scope. - - rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)). - - simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^) - (factor2 fact)). - rewrite <- ap_p_pp; rewrite_moveL_Mp_p. - Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). - Abort. -- cgit v1.2.3