unification regression with Coq 8.20alpha #18593
Labels
needs: minimization
This issue needs a minimal working example.
part: unification
The unification mechanism.
Comments
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
|
actually I meant @coqbot minimize coq.dev |
|
Hey @SkySkimmer, the coq bug minimizer is running your script, I'll come back to you with the results once it's done. |
|
@SkySkimmer, Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/UniMath/UniMath/Bicategories/DisplayedBicats/Examples/Codomain.v (full log on GitHub Actions - verbose log) 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/UniMath/UniMath" "UniMath" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/home/coq/.opam/4.13.1+flambda/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.Bicategories.DisplayedBicats.Examples.Codomain") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1297 lines to 65 lines, then from 78 lines to 1367 lines, then from 1372 lines to 158 lines, then from 171 lines to 789 lines, then from 794 lines to 228 lines, then from 241 lines to 2028 lines, then from 2029 lines to 475 lines, then from 488 lines to 1014 lines, then from 1018 lines to 539 lines, then from 552 lines to 1029 lines, then from 1032 lines to 575 lines, then from 588 lines to 2311 lines, then from 2311 lines to 692 lines, then from 705 lines to 786 lines, then from 791 lines to 737 lines, then from 750 lines to 1116 lines, then from 1120 lines to 764 lines, then from 777 lines to 2285 lines, then from 2277 lines to 784 lines, then from 797 lines to 886 lines, then from 891 lines to 785 lines, then from 798 lines to 838 lines, then from 843 lines to 784 lines, then from 797 lines to 2190 lines, then from 2094 lines to 787 lines, then from 800 lines to 4844 lines, then from 4754 lines to 807 lines, then from 820 lines to 1020 lines, then from 1024 lines to 827 lines, then from 840 lines to 1050 lines, then from 1055 lines to 873 lines, then from 878 lines to 874 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.13.1
coqtop version buildkitsandbox:/home/coq/.opam/4.13.1+flambda/.opam-switch/build/coq-core.dev/_build/default,master (a6cc4b424842ee8b4dead86f291f4580fea2cc43)
Expected coqc runtime on this file: 0.677 sec *)
Require Coq.Init.Ltac.
Require Coq.Init.Notations.
Inductive False : Prop := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Export Coq.Init.Notations.
Export Coq.Init.Ltac.
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Notation "x → y" := (x -> y)
(at level 99, y at level 200, right associativity): type_scope.
Reserved Notation "A × B" (at level 75, right associativity).
Reserved Notation "C ⟦ a , b ⟧" (at level 49, right associativity).
Reserved Notation "f · g" (at level 40, left associativity).
Reserved Notation "a --> b" (at level 55).
Reserved Notation "q '^-1'" (at level 10).
Reserved Notation "x ,, y" (at level 60, right associativity).
Ltac simple_rapply p :=
simple refine p ||
simple refine (p _) ||
simple refine (p _ _) ||
simple refine (p _ _ _) ||
simple refine (p _ _ _ _) ||
simple refine (p _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Tactic Notation "use" uconstr(p) := simple_rapply p.
Definition UU := Type.
Identity Coercion fromUUtoType : UU >-> Sortclass.
Inductive paths {A:UU} (a:A) : A -> UU := paths_refl : paths a a.
Notation "a = b" := (paths a b) : type_scope.
Set Primitive Projections.
Record total2 { T: UU } ( P: T -> UU ) := tpair { pr1 : T; pr2 : P pr1 }.
Arguments tpair {_} _ _ _.
Arguments pr1 {_ _} _.
Arguments pr2 {_ _} _.
Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "x ,, y" := (tpair _ x y).
Definition dirprod (X Y : UU) := ∑ x:X, Y.
Notation "A × B" := (dirprod A B) : type_scope.
Definition make_dirprod {X Y : UU} (x:X) (y:Y) : X × Y.
Admitted.
Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
(e: t1 = t2) : f t1 = f t2.
Admitted.
Definition transportf {X : UU} (P : X -> UU) {x x' : X}
(e : x = x') : P x -> P x'.
Admitted.
Definition transportb {X : UU} (P : X -> UU) {x x' : X}
(e : x = x') : P x' -> P x.
admit.
Defined.
Definition isaset (X : UU) : UU.
Admitted.
Notation "'pr11' x" := (pr1 (pr1 x)) (at level 10, left associativity).
Lemma pr1_transportf {A : UU} {B : A -> UU} {P : ∏ a, B a -> UU}
{a a' : A} (e : a = a') (xs : ∑ b : B a, P _ b):
pr1 (transportf (λ x, ∑ b : B x, P _ b) e xs) =
transportf (λ x, B x) e (pr1 xs).
Admitted.
Definition precategory_ob_mor : UU.
exact (∑ ob : UU, ob -> ob -> UU).
Defined.
Definition ob (C : precategory_ob_mor) : UU.
exact (@pr1 _ _ C).
Defined.
Coercion ob : precategory_ob_mor >-> UU.
Definition precategory_morphisms { C : precategory_ob_mor } :
C -> C -> UU.
exact (pr2 C).
Defined.
Declare Scope cat.
Local Open Scope cat.
Notation "a --> b" := (precategory_morphisms a b) : cat.
Notation "C ⟦ a , b ⟧" := (precategory_morphisms (C:=C) a b) : cat.
Definition precategory_id_comp (C : precategory_ob_mor) : UU.
exact ((∏ c : C, c --> c)
×
(∏ a b c : C, a --> b -> b --> c -> a --> c)).
Defined.
Definition precategory_data : UU.
exact (∑ C : precategory_ob_mor, precategory_id_comp C).
Defined.
Definition precategory_ob_mor_from_precategory_data (C : precategory_data) :
precategory_ob_mor.
exact (pr1 C).
Defined.
Coercion precategory_ob_mor_from_precategory_data :
precategory_data >-> precategory_ob_mor.
Definition identity {C : precategory_data}
: ∏ c : C, c --> c.
exact (pr1 (pr2 C)).
Defined.
Definition compose {C : precategory_data} { a b c : C }
: a --> b -> b --> c -> a --> c.
exact (pr2 (pr2 C) a b c).
Defined.
Notation "f · g" := (compose f g) : cat.
Definition prebicat_2cell_struct (C : precategory_ob_mor)
: UU.
exact (∏ (a b: C), C⟦a, b⟧ → C⟦a, b⟧ → UU).
Defined.
Definition prebicat_1_id_comp_cells : UU.
exact (∑ (C : precategory_data), prebicat_2cell_struct C).
Defined.
Coercion precat_data_from_prebicat_1_id_comp_cells (C : prebicat_1_id_comp_cells)
: precategory_data.
exact (pr1 C).
Defined.
Definition prebicat_cells (C : prebicat_1_id_comp_cells) {a b : C} (f g : C⟦a, b⟧)
: UU.
exact (pr2 C a b f g).
Defined.
Local Notation "f '==>' g" := (prebicat_cells _ f g) (at level 60).
Local Notation "f '<==' g" := (prebicat_cells _ g f) (at level 60, only parsing).
Definition prebicat_2_id_comp_struct (C : prebicat_1_id_comp_cells) : UU.
exact ((∏ (a b : C) (f : C⟦a, b⟧), f ==> f)
×
(∏ (a b : C) (f : C⟦a, b⟧), identity _ · f ==> f)
×
(∏ (a b : C) (f : C⟦a, b⟧), f · identity _ ==> f)
×
(∏ (a b : C) (f : C⟦a, b⟧), identity _ · f <== f)
×
(∏ (a b : C) (f : C⟦a, b⟧), f · identity _ <== f)
×
(∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧),
(f · g) · h ==> f · (g · h))
×
(∏ (a b c d : C) (f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧),
f · (g · h) ==> (f · g) · h)
×
(∏ (a b : C) (f g h : C⟦a, b⟧), f ==> g -> g ==> h -> f ==> h)
×
(∏ (a b c : C) (f : C⟦a, b⟧) (g1 g2 : C⟦b, c⟧),
g1 ==> g2 → f · g1 ==> f · g2)
×
(∏ (a b c : C) (f1 f2 : C⟦a, b⟧) (g : C⟦b, c⟧),
f1 ==> f2 → f1 · g ==> f2 · g)).
Defined.
Definition prebicat_data : UU.
exact (∑ C, prebicat_2_id_comp_struct C).
Defined.
Coercion prebicat_cells_1_id_comp_from_prebicat_data (C : prebicat_data)
: prebicat_1_id_comp_cells.
exact (pr1 C).
Defined.
Definition id2 {C : prebicat_data} {a b : C} (f : C⟦a, b⟧) : f ==> f.
exact (pr1 (pr2 C) a b f).
Defined.
Definition lunitor {C : prebicat_data} {a b : C} (f : C⟦a, b⟧)
: identity _ · f ==> f.
exact (pr1 (pr2 (pr2 C)) a b f).
Defined.
Definition runitor {C : prebicat_data} {a b : C} (f : C⟦a, b⟧)
: f · identity _ ==> f.
exact (pr1 (pr2 (pr2 (pr2 C))) a b f).
Defined.
Definition linvunitor {C : prebicat_data} {a b : C} (f : C⟦a, b⟧)
: identity _ · f <== f.
exact (pr1 (pr2 (pr2 (pr2 (pr2 C)))) a b f).
Defined.
Definition rinvunitor {C : prebicat_data} {a b : C} (f : C⟦a, b⟧)
: f · identity _ <== f.
exact (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 C))))) a b f).
Defined.
Definition rassociator {C : prebicat_data} {a b c d : C}
(f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧)
: (f · g) · h ==> f · (g · h).
exact (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))) a b c d f g h).
Defined.
Definition lassociator {C : prebicat_data} {a b c d : C}
(f : C⟦a, b⟧) (g : C⟦b, c⟧) (h : C⟦c, d⟧)
: f · (g · h) ==> (f · g) · h.
exact (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))) a b c d f g h).
Defined.
Definition vcomp2 {C : prebicat_data} {a b : C} {f g h: C⟦a, b⟧}
: f ==> g → g ==> h → f ==> h.
exact (λ x y, pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C)))))))) _ _ _ _ _ x y).
Defined.
Definition lwhisker {C : prebicat_data} {a b c : C} (f : C⟦a, b⟧) {g1 g2 : C⟦b, c⟧}
: g1 ==> g2 → f · g1 ==> f · g2.
exact (λ x, pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))) _ _ _ _ _ _ x).
Defined.
Definition rwhisker {C : prebicat_data} {a b c : C} {f1 f2 : C⟦a, b⟧} (g : C⟦b, c⟧)
: f1 ==> f2 → f1 · g ==> f2 · g.
exact (λ x, pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 C))))))))) _ _ _ _ _ _ x).
Defined.
Local Notation "x • y" := (vcomp2 x y) (at level 60).
Local Notation "f ◃ x" := (lwhisker f x) (at level 60).
Local Notation "y ▹ g" := (rwhisker g y) (at level 60).
Definition prebicat_laws (C : prebicat_data)
: UU.
Admitted.
Definition prebicat : UU.
exact (∑ C : prebicat_data, prebicat_laws C).
Defined.
Coercion prebicat_data_from_bicat (C : prebicat) : prebicat_data.
exact (pr1 C).
Defined.
Definition isaset_cells (C : prebicat) : UU.
exact (∏ (a b : C) (f g : a --> b), isaset (f ==> g)).
Defined.
Definition bicat : UU.
exact (∑ C : prebicat, isaset_cells C).
Defined.
Coercion prebicat_of_bicat (C : bicat)
: prebicat.
exact (pr1 C).
Defined.
Definition is_invertible_2cell {C : prebicat_data}
{a b : C} {f g : a --> b} (η : f ==> g)
: UU.
Admitted.
Definition make_is_invertible_2cell {C : prebicat_data}
{a b : C} {f g : a --> b}
{η : f ==> g}
{φ : g ==> f}
(ηφ : η • φ = id2 f)
(φη : φ • η = id2 g)
: is_invertible_2cell η.
Admitted.
Definition inv_cell {C : prebicat_data} {a b : C} {f g : a --> b} {η : f ==> g}
: is_invertible_2cell η → g ==> f.
Admitted.
Notation "inv_η ^-1" := (inv_cell inv_η) : bicategory_scope.
Local Open Scope bicategory_scope.
Definition vcomp_rinv {C : prebicat_data} {a b : C} {f g : a --> b}
{η : f ==> g} (inv_η : is_invertible_2cell η)
: η • inv_η^-1 = id2 f.
Admitted.
Definition invertible_2cell {C : prebicat_data}
{a b : C} (f g : a --> b) : UU.
exact (∑ η : f ==> g, is_invertible_2cell η).
Defined.
Coercion cell_from_invertible_2cell {C : prebicat_data}
{a b : C} {f g : a --> b} (η : invertible_2cell f g)
: f ==> g.
Admitted.
Coercion property_from_invertible_2cell {C : prebicat_data}
{a b : C} {f g : a --> b}
(η : invertible_2cell f g)
: is_invertible_2cell η.
Admitted.
Definition id2_invertible_2cell {C : prebicat} {a b : C} (f : a --> b)
: invertible_2cell f f.
Admitted.
Definition disp_cat_ob_mor (C : precategory_ob_mor)
:= ∑ (obd : C -> UU), (∏ x y:C, obd x -> obd y -> (x --> y) -> UU).
Definition make_disp_cat_ob_mor
(C : precategory_ob_mor)
(obd : C -> UU)
(mord : ∏ x y:C, obd x -> obd y -> (x --> y) -> UU)
: disp_cat_ob_mor C.
exact (obd,, mord).
Defined.
Definition ob_disp {C: precategory_ob_mor} (D : disp_cat_ob_mor C) : C -> UU.
exact (pr1 D).
Defined.
Coercion ob_disp : disp_cat_ob_mor >-> Funclass.
Definition mor_disp {C: precategory_ob_mor} {D : disp_cat_ob_mor C}
{x y} xx yy (f : x --> y)
:= pr2 D x y xx yy f : UU.
Local Notation "xx -->[ f ] yy" := (mor_disp xx yy f) (at level 50, left associativity, yy at next level).
Definition disp_cat_id_comp (C : precategory_data)
(D : disp_cat_ob_mor C)
: UU.
exact ((forall (x:C) (xx : D x), xx -->[identity x] xx)
× (forall (x y z : C) (f : x --> y) (g : y --> z) (xx:D x) (yy:D y) (zz:D z),
(xx -->[f] yy) -> (yy -->[g] zz) -> (xx -->[f · g] zz))).
Defined.
Definition disp_cat_data C := total2 (disp_cat_id_comp C).
Definition disp_cat_ob_mor_from_disp_cat_data {C: precategory_data}
(D : disp_cat_data C)
: disp_cat_ob_mor C.
exact (pr1 D).
Defined.
Coercion disp_cat_ob_mor_from_disp_cat_data :
disp_cat_data >-> disp_cat_ob_mor.
Definition id_disp {C: precategory_data} {D : disp_cat_data C} {x:C} (xx : D x)
: xx -->[identity x] xx.
exact (pr1 (pr2 D) x xx).
Defined.
Definition comp_disp {C: precategory_data} {D : disp_cat_data C}
{x y z : C} {f : x --> y} {g : y --> z}
{xx : D x} {yy} {zz} (ff : xx -->[f] yy) (gg : yy -->[g] zz)
: xx -->[f · g] zz.
exact (pr2 (pr2 D) _ _ _ _ _ _ _ _ ff gg).
Defined.
Notation "ff ;; gg" := (comp_disp ff gg)
(at level 50, left associativity, format "ff ;; gg")
: mor_disp_scope.
Delimit Scope mor_disp_scope with mor_disp.
Local Open Scope mor_disp.
Section Total_Category_data.
Context {C : precategory_data} (D : disp_cat_data C).
Definition total_category_ob_mor : precategory_ob_mor.
Proof.
exists (∑ x:C, D x).
intros xx yy.
exact (∑ (f : pr1 xx --> pr1 yy), pr2 xx -->[f] pr2 yy).
Defined.
Definition total_category_id_comp : precategory_id_comp (total_category_ob_mor).
Proof.
apply tpair; simpl.
-
intros.
exists (identity _).
apply id_disp.
-
intros xx yy zz ff gg.
exists (pr1 ff · pr1 gg).
exact (pr2 ff ;; pr2 gg).
Defined.
End Total_Category_data.
Definition disp_2cell_struct {C : prebicat_1_id_comp_cells} (D : disp_cat_ob_mor C) : UU.
exact (∏ (c c' : C) (f g : C⟦c,c'⟧) (x : f ==> g)
(d : D c) (d' : D c') (f' : d -->[f] d') (g' : d -->[g] d'), UU).
Defined.
Definition disp_prebicat_1_id_comp_cells (C : prebicat_1_id_comp_cells) : UU.
exact (∑ D : disp_cat_data C, disp_2cell_struct D).
Defined.
Coercion disp_cat_data_from_disp_prebicat_1_id_comp_cells
{C : prebicat_1_id_comp_cells} (D : disp_prebicat_1_id_comp_cells C)
: disp_cat_data C.
exact (pr1 D).
Defined.
Definition disp_2cells {C : prebicat_1_id_comp_cells}
{D : disp_prebicat_1_id_comp_cells C}
{c c' : C} {f g : C⟦c,c'⟧} (x : f ==> g)
{d : D c} {d' : D c'} (f' : d -->[f] d') (g' : d -->[g] d')
: UU.
exact (pr2 D c c' f g x d d' f' g').
Defined.
Section disp_prebicat.
Context {C : bicat}.
Local Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).
Local Notation "f' <==[ x ] g'" := (disp_2cells x g' f') (at level 60, only parsing).
Definition disp_prebicat_ops (D : disp_prebicat_1_id_comp_cells C) : UU.
exact ((∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y),
f' ==>[id2 _] f')
× (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y),
id_disp x ;; f' ==>[lunitor _] f')
× (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y),
f' ;; id_disp y ==>[runitor _] f')
× (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y),
id_disp x ;; f' <==[linvunitor _] f')
× (∏ (a b : C) (f : C⟦a,b⟧) (x : D a) (y : D b) (f' : x -->[f] y),
f' ;; id_disp y <==[rinvunitor _] f')
× (∏ (a b c d : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧) (h : C⟦c,d⟧)
(w : D a) (x : D b) (y : D c) (z : D d)
(ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z),
(ff ;; gg) ;; hh ==>[rassociator _ _ _] ff ;; (gg ;; hh))
× (∏ (a b c d : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧) (h : C⟦c,d⟧)
(w : D a) (x : D b) (y : D c) (z : D d)
(ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z),
ff ;; (gg ;; hh) ==>[lassociator _ _ _] (ff ;; gg) ;; hh)
× (∏ (a b : C) (f g h : C⟦a,b⟧) (r : f ==> g) (s : g ==> h)
(x : D a) (y : D b) (ff : x -->[f] y) (gg : x -->[g] y) (hh : x -->[h] y),
ff ==>[r] gg → gg ==>[s] hh → ff ==>[r • s] hh)
× (∏ (a b c : C) (f : C⟦a,b⟧) (g1 g2 : C⟦b,c⟧)
(r : g1 ==> g2) (x : D a) (y : D b) (z : D c)
(ff : x -->[f] y) (gg1 : y -->[g1] z) (gg2 : y -->[g2] z),
gg1 ==>[r] gg2 → ff ;; gg1 ==>[f ◃ r] ff ;; gg2)
× (∏ (a b c : C) (f1 f2 : C⟦a,b⟧) (g : C⟦b,c⟧)
(r : f1 ==> f2) (x : D a) (y : D b) (z : D c)
(ff1 : x -->[f1] y) (ff2 : x -->[f2] y) (gg : y -->[g] z),
ff1 ==>[r] ff2 → ff1 ;; gg ==>[r ▹ g] ff2 ;; gg)).
Defined.
Definition disp_prebicat_data : UU.
exact (∑ D : disp_prebicat_1_id_comp_cells C, disp_prebicat_ops D).
Defined.
Coercion disp_prebicat_ob_mor_cells_1_id_comp_from_disp_prebicat_data
(D : disp_prebicat_data)
: disp_prebicat_1_id_comp_cells C.
exact (pr1 D).
Defined.
Section disp_prebicat_ops_projections.
Context {D : disp_prebicat_data}.
Definition disp_id2 {a b : C} {f : C⟦a,b⟧} {x : D a} {y : D b} (f' : x -->[f] y)
: f' ==>[id2 _] f'.
Admitted.
Definition disp_lunitor {a b : C} {f : C⟦a,b⟧} {x : D a} {y : D b} (f' : x -->[f] y)
: id_disp x ;; f' ==>[lunitor _] f'.
Admitted.
Definition disp_runitor {a b : C} {f : C⟦a,b⟧} {x : D a} {y : D b} (f' : x -->[f] y)
: f' ;; id_disp y ==>[runitor _] f'.
Admitted.
Definition disp_linvunitor
{a b : C} {f : C⟦a,b⟧} {x : D a} {y : D b} (f' : x -->[f] y)
: id_disp x ;; f' <==[linvunitor _] f'.
Admitted.
Definition disp_rinvunitor
{a b : C} {f : C⟦a,b⟧} {x : D a} {y : D b} (f' : x -->[f] y)
: f' ;; id_disp y <==[rinvunitor _] f'.
Admitted.
Definition disp_rassociator
{a b c d : C} {f : C⟦a,b⟧} {g : C⟦b,c⟧} {h : C⟦c,d⟧}
{w : D a} {x : D b} {y : D c} {z : D d}
(ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z)
: (ff ;; gg) ;; hh ==>[rassociator _ _ _] ff ;; (gg ;; hh).
Admitted.
Definition disp_lassociator
{a b c d : C} {f : C⟦a,b⟧} {g : C⟦b,c⟧} {h : C⟦c,d⟧}
{w : D a} {x : D b} {y : D c} {z : D d}
(ff : w -->[f] x) (gg : x -->[g] y) (hh : y -->[h] z)
: ff ;; (gg ;; hh) ==>[lassociator _ _ _] (ff ;; gg) ;; hh.
Admitted.
Definition disp_vcomp2
{a b : C} {f g h : C⟦a,b⟧}
{r : f ==> g} {s : g ==> h}
{x : D a} {y : D b}
{ff : x -->[f] y} {gg : x -->[g] y} {hh : x -->[h] y}
: ff ==>[r] gg → gg ==>[s] hh → ff ==>[r • s] hh.
Admitted.
Definition disp_lwhisker
{a b c : C} {f : C⟦a,b⟧} {g1 g2 : C⟦b,c⟧}
{r : g1 ==> g2}
{x : D a} {y : D b} {z : D c}
(ff : x -->[f] y) {gg1 : y -->[g1] z} {gg2 : y -->[g2] z}
: gg1 ==>[r] gg2 → ff ;; gg1 ==>[f ◃ r] ff ;; gg2.
Admitted.
Definition disp_rwhisker
{a b c : C} {f1 f2 : C⟦a,b⟧} {g : C⟦b,c⟧}
{r : f1 ==> f2}
{x : D a} {y : D b} {z : D c}
{ff1 : x -->[f1] y} {ff2 : x -->[f2] y} (gg : y -->[g] z)
: ff1 ==>[r] ff2 → ff1 ;; gg ==>[r ▹ g] ff2 ;; gg.
Admitted.
End disp_prebicat_ops_projections.
Local Notation "rr •• ss" := (disp_vcomp2 rr ss) (at level 60).
Local Notation "ff ◃◃ rr" := (disp_lwhisker ff rr) (at level 60).
Local Notation "rr ▹▹ gg" := (disp_rwhisker gg rr) (at level 60).
Section disp_prebicat_laws.
Context (D : disp_prebicat_data).
Definition disp_prebicat_laws : UU.
Admitted.
End disp_prebicat_laws.
Definition disp_prebicat : UU.
exact (∑ D : disp_prebicat_data, disp_prebicat_laws D).
Defined.
Coercion disp_prebicat_data_from_disp_prebicat (D : disp_prebicat)
: disp_prebicat_data.
exact (pr1 D).
Defined.
Section Display_Invertible_2cell.
Context {D : disp_prebicat}.
Section Def_inv_2cell.
Context {c c' : C} {f f' : C⟦c,c'⟧} {d : D c} {d' : D c'}.
Definition is_disp_invertible_2cell {α : f ==> f'} (inv_α : is_invertible_2cell α)
{ff : d -->[f] d'} {ff' : d -->[f'] d'} (x : ff ==>[α] ff')
: UU.
Admitted.
Definition disp_invertible_2cell (α : invertible_2cell f f')
(ff : d -->[f] d') (ff' : d -->[f'] d')
: UU.
exact (∑ (x : ff ==>[α] ff'), is_disp_invertible_2cell α x).
Defined.
Coercion disp_cell_from_invertible_2cell {α : invertible_2cell f f'}
{ff : d -->[f] d'} {ff' : d -->[f'] d'}
(e : disp_invertible_2cell α ff ff')
: ff ==>[α] ff'.
Admitted.
Definition disp_inv_cell {α : invertible_2cell f f'}
{ff : d -->[f] d'} {ff' : d -->[f'] d'}
(e : disp_invertible_2cell α ff ff')
: ff' ==>[α^-1] ff.
Admitted.
Definition disp_vcomp_rinv {α : invertible_2cell f f'}
{ff : d -->[f] d'} {ff' : d -->[f'] d'}
(e : disp_invertible_2cell α ff ff')
: e •• disp_inv_cell e =
transportb (λ α, _ ==>[α] _) (vcomp_rinv α) (disp_id2 ff).
Admitted.
End Def_inv_2cell.
End Display_Invertible_2cell.
Section total_prebicat.
Variable D : disp_prebicat.
Definition total_prebicat_1_data : precategory_data.
exact (total_category_ob_mor D ,, total_category_id_comp D).
Defined.
Definition total_prebicat_cell_struct : prebicat_2cell_struct (total_category_ob_mor D).
exact (λ a b f g, ∑ η : pr1 f ==> pr1 g, pr2 f ==>[η] pr2 g).
Defined.
Definition total_prebicat_1_id_comp_cells : prebicat_1_id_comp_cells.
exact ((total_prebicat_1_data,, total_prebicat_cell_struct)).
Defined.
Definition total_prebicat_2_id_comp_struct
: prebicat_2_id_comp_struct total_prebicat_1_id_comp_cells.
Proof.
repeat split; cbn; unfold total_prebicat_cell_struct.
-
intros.
exists (id2 _).
exact (disp_id2 _).
-
intros.
exists (lunitor _).
exact (disp_lunitor _).
-
intros.
exists (runitor _).
exact (disp_runitor _).
-
intros.
exists (linvunitor _).
exact (disp_linvunitor _).
-
intros.
exists (rinvunitor _).
exact (disp_rinvunitor _).
-
intros.
exists (rassociator _ _ _).
exact (disp_rassociator _ _ _).
-
intros.
exists (lassociator _ _ _).
exact (disp_lassociator _ _ _).
-
intros a b f g h r s.
exists (pr1 r • pr1 s).
exact (pr2 r •• pr2 s).
-
intros a b d f g1 g2 r.
exists (pr1 f ◃ pr1 r).
exact (pr2 f ◃◃ pr2 r).
-
intros a b c f1 f2 g r.
exists (pr1 r ▹ pr1 g).
exact (pr2 r ▹▹ pr2 g).
Defined.
Definition total_prebicat_data : prebicat_data.
exact (_ ,, total_prebicat_2_id_comp_struct).
Defined.
Lemma total_prebicat_laws : prebicat_laws total_prebicat_data.
Admitted.
Definition total_prebicat : prebicat.
exact (_ ,, total_prebicat_laws).
Defined.
End total_prebicat.
Definition has_disp_cellset (D : disp_prebicat) : UU.
exact (∏ (a b : C) (f g : C⟦a,b⟧) (x : f ==> g)
(aa : D a) (bb : D b)
(ff : aa -->[f] bb)
(gg : aa -->[g] bb),
isaset (ff ==>[x] gg)).
Defined.
Definition disp_bicat : UU.
exact (∑ D : disp_prebicat, has_disp_cellset D).
Defined.
Coercion disp_prebicat_of_disp_bicat (D : disp_bicat)
: disp_prebicat.
exact (pr1 D).
Defined.
Lemma isaset_cells_total_prebicat (D : disp_bicat)
: isaset_cells (total_prebicat D).
Admitted.
Definition total_bicat (D : disp_bicat) : bicat.
exact (total_prebicat D,, isaset_cells_total_prebicat D).
Defined.
End disp_prebicat.
Arguments disp_prebicat_data _ : clear implicits.
Arguments disp_prebicat _ : clear implicits.
Arguments disp_bicat _ : clear implicits.
Notation "f' ==>[ x ] g'" := (disp_2cells x f' g') (at level 60).
Section Trivial_Displayed.
Variable (B C : bicat).
Definition trivial_disp_cat_ob_mor : disp_cat_ob_mor B.
exact (make_disp_cat_ob_mor
B
(λ _ : B, C)
(λ (_ _ : B) (a b : C) _, C⟦a,b⟧)).
Defined.
Definition trivial_disp_cat_id_comp
: disp_cat_id_comp B trivial_disp_cat_ob_mor.
exact ((λ (_ : B) (a : C), identity a),,
(λ (_ _ _ : B) _ _ (a b c : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧), f · g)).
Defined.
Definition trivial_disp_cat_data : disp_cat_data B.
exact (trivial_disp_cat_ob_mor,, trivial_disp_cat_id_comp).
Defined.
Definition trivial_disp_prebicat_1_id_comp_cells : disp_prebicat_1_id_comp_cells B.
exact (tpair (λ C:disp_cat_data B, disp_2cell_struct C)
trivial_disp_cat_data
(λ _ _ _ _ _ a b f g, f ==> g)).
Defined.
Definition trivial_displayed_data : disp_prebicat_data B.
use (trivial_disp_prebicat_1_id_comp_cells,, _).
repeat apply make_dirprod; cbn.
-
intros _ _ _.
exact (λ a b f, id2 f).
-
intros _ _ _.
exact (λ a b f, lunitor f).
-
intros _ _ _.
exact (λ a b f, runitor f).
-
intros _ _ _.
exact (λ a b f, linvunitor f).
-
intros _ _ _.
exact (λ a b f, rinvunitor f).
-
intros _ _ _ _ _ _ _.
exact (λ a b c d f g h, rassociator f g h).
-
intros _ _ _ _ _ _ _.
exact (λ a b c d f g h, lassociator f g h).
-
intros _ _ _ _ _ _ _.
exact (λ a b f g h x y, vcomp2 x y).
-
intros _ _ _ _ _ _ _.
exact (λ a b c f g1 g2 x, lwhisker f x).
-
intros _ _ _ _ _ _ _.
exact (λ a b c f1 f2 g x, rwhisker g x).
Defined.
Lemma trivial_disp_prebicat_laws : disp_prebicat_laws trivial_displayed_data.
Admitted.
Definition trivial_displayed_prebicat : disp_prebicat B.
exact (trivial_displayed_data,, trivial_disp_prebicat_laws).
Defined.
Definition trivial_displayed_bicat : disp_bicat B.
Proof.
refine (trivial_displayed_prebicat ,, _).
repeat intro; apply C.
Defined.
End Trivial_Displayed.
Definition prod_bicat
(B C : bicat)
: bicat.
exact (total_bicat (trivial_displayed_bicat B C)).
Defined.
Section Sigma.
Variable (C : bicat)
(D : disp_bicat C)
(E : disp_bicat (total_bicat D)).
Definition sigma_disp_cat_ob_mor : disp_cat_ob_mor C.
Proof.
exists (λ c, ∑ (d : D c), (E (c,,d))).
intros x y xx yy f.
exact (∑ (fD : pr1 xx -->[f] pr1 yy), pr2 xx -->[f,,fD] pr2 yy).
Defined.
Definition sigma_disp_cat_id_comp
: disp_cat_id_comp _ sigma_disp_cat_ob_mor.
Proof.
apply tpair.
-
intros x xx.
exists (id_disp _).
exact (id_disp (pr2 xx)).
-
intros x y z f g xx yy zz ff gg.
exists (pr1 ff ;; pr1 gg).
exact (pr2 ff ;; pr2 gg).
Defined.
Definition sigma_disp_cat_data : disp_cat_data C.
exact ((_ ,, sigma_disp_cat_id_comp)).
Defined.
Definition sigma_prebicat_1_id_comp_cells : disp_prebicat_1_id_comp_cells C.
Proof.
exists sigma_disp_cat_data.
red.
intros c c' f g x d d' ff gg.
cbn in *.
use (∑ xx : pr1 ff ==>[x] pr1 gg , _).
set (PPP := @prebicat_cells (total_bicat D) (c,, pr1 d) (c',, pr1 d')
(f,, pr1 ff) (g,, pr1 gg)).
exact (pr2 ff ==>[(x,, xx) : PPP] pr2 gg).
Defined.
Definition sigma_bicat_data : disp_prebicat_data C.
Proof.
exists sigma_prebicat_1_id_comp_cells.
repeat split; cbn; first [intros * | intros].
-
exists (disp_id2 _).
exact (disp_id2 _).
-
exists (disp_lunitor (pr1 f')).
exact (disp_lunitor (pr2 f')).
-
exists (disp_runitor (pr1 f')).
exact (disp_runitor (pr2 f')).
-
exists (disp_linvunitor (pr1 f')).
exact (disp_linvunitor (pr2 f')).
-
exists (disp_rinvunitor (pr1 f')).
exact (disp_rinvunitor (pr2 f')).
-
exists (disp_rassociator (pr1 ff) (pr1 gg) (pr1 hh)).
exact (disp_rassociator (pr2 ff) (pr2 gg) (pr2 hh)).
-
exists (disp_lassociator (pr1 ff) (pr1 gg) (pr1 hh)).
exact (disp_lassociator (pr2 ff) (pr2 gg) (pr2 hh)).
-
intros xx yy.
exists (disp_vcomp2 (pr1 xx) (pr1 yy)).
exact (disp_vcomp2 (pr2 xx) (pr2 yy)).
-
intros xx.
exists (disp_lwhisker (pr1 ff) (pr1 xx)).
exact (disp_lwhisker (pr2 ff) (pr2 xx)).
-
intros xx.
exists (disp_rwhisker (pr1 gg) (pr1 xx)).
exact (disp_rwhisker (pr2 gg) (pr2 xx)).
Defined.
Lemma sigma_prebicat_laws : disp_prebicat_laws sigma_bicat_data.
Admitted.
Definition sigma_prebicat : disp_prebicat C.
exact (sigma_bicat_data,, sigma_prebicat_laws).
Defined.
Lemma has_disp_cellset_sigma_prebicat
: has_disp_cellset sigma_prebicat.
Admitted.
Definition sigma_bicat
: disp_bicat C.
exact (sigma_prebicat,, has_disp_cellset_sigma_prebicat).
Defined.
End Sigma.
Section CodomainArrow.
Variable (B : bicat).
Definition cod_disp_bicat_help
: disp_bicat (prod_bicat B B).
Admitted.
Definition cod_disp_bicat
: disp_bicat B.
exact (sigma_bicat _ _ cod_disp_bicat_help).
Defined.
End CodomainArrow.
Definition coherent_homot
{B : bicat}
{X Y : B}
{f g : X --> Y}
(α : f ==> g)
{dX : cod_disp_bicat B X}
{dY : cod_disp_bicat B Y}
{df : dX -->[ f ] dY}
{dg : dX -->[ g ] dY}
(h : pr1 df ==> pr1 dg)
: UU.
Admitted.
Context (B : bicat).
Definition cod_disp_invertible_invertible_2_cell
{c₁ c₂ : B}
{f : B ⟦ c₁, c₂ ⟧}
{φ₁ : cod_disp_bicat B c₁}
{φ₂ : cod_disp_bicat B c₂}
{ψ₁ ψ₂ : φ₁ -->[ f] φ₂}
: disp_invertible_2cell (id2_invertible_2cell f) ψ₁ ψ₂
→
∑ (α : invertible_2cell (pr1 ψ₁) (pr1 ψ₂)),
coherent_homot (id2_invertible_2cell f) (pr1 α).
Proof.
intro α.
simple refine ((_ ,, _) ,, _).
-
exact (pr11 α).
-
simpl.
use make_is_invertible_2cell.
+
exact (pr1 (disp_inv_cell α)).
+
abstract
(pose (maponpaths pr1 (disp_vcomp_rinv α)) as p ;
cbn in p ;
unfold transportb in p ;
rewrite pr1_transportf, transportf_const in p ;
exact p).🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 531KiB file on GitHub Actions Artifacts under
|
|
Looks like it minimized too much, I get the same error with 8.18 on that file |
SkySkimmer
changed the title
SkySkimmer
added
the
needs: minimization
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Description of the problem
UniMath checks compilation with, among others, the development version of Coq, currently Coq 8.20 alpha. With that version, compilation of two files in package
Bicategoriesfails, even though it works with Coq 8.18. (The packageBicategoriesis deactivated in the Coq CI, hence the failure does not show up in PRs to Coq.)The corresponding issue at UniMath, with information about the error, is at UniMath/UniMath#1832.
The failure is likely easy to fix on the UniMath side; but I am wondering if it would be useful for the Coq developers to understand why code that works in 8.18 does not work in 8.20alpha.
Coq Version
Coq 8.20 alpha.
The text was updated successfully, but these errors were encountered: