summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3422.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3422.v')
-rw-r--r--test-suite/bugs/closed/3422.v208
1 files changed, 208 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3422.v b/test-suite/bugs/closed/3422.v
new file mode 100644
index 00000000..d984f623
--- /dev/null
+++ b/test-suite/bugs/closed/3422.v
@@ -0,0 +1,208 @@
+Generalizable All Variables.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Reserved Infix "o" (at level 40, left associativity).
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
+Existing Instance equiv_isequiv.
+Delimit Scope equiv_scope with equiv.
+Local Open Scope equiv_scope.
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+Axiom IsHSet : Type -> Type.
+Existing Class IsHSet.
+Definition trunc_equiv' `(f : A <~> B) `{IsHSet A} : IsHSet B := admit.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory :=
+ { object :> Type;
+ morphism : object -> object -> Type;
+
+ compose : forall s d d',
+ morphism d d'
+ -> morphism s d
+ -> morphism s d'
+ where "f 'o' g" := (compose f g);
+
+ trunc_morphism : forall s d, IsHSet (morphism s d) }.
+
+Bind Scope category_scope with PreCategory.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+
+Delimit Scope functor_scope with functor.
+
+Record Functor (C D : PreCategory) :=
+ {
+ object_of :> C -> D;
+ morphism_of : forall s d, morphism C s d
+ -> morphism D (object_of s) (object_of d)
+ }.
+
+Bind Scope functor_scope with Functor.
+Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
+Local Open Scope morphism_scope.
+
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
+
+Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
+
+Class Isomorphic {C : PreCategory} s d :=
+ {
+ morphism_isomorphic :> morphism C s d;
+ isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+ }.
+
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+
+Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}.
+
+Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1)
+: IsIsomorphism (m0 o m1).
+admit.
+Defined.
+
+Section composition.
+ Variable C : PreCategory.
+ Variable D : PreCategory.
+ Variable E : PreCategory.
+ Variable G : Functor D E.
+ Variable F : Functor C D.
+
+ Definition composeF : Functor C E
+ := Build_Functor
+ C E
+ (fun c => G (F c))
+ (fun _ _ m => morphism_of G (morphism_of F m)).
+End composition.
+Infix "o" := composeF : functor_scope.
+
+Delimit Scope natural_transformation_scope with natural_transformation.
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+
+Section compose.
+ Variable C : PreCategory.
+ Variable D : PreCategory.
+ Variables F F' F'' : Functor C D.
+
+ Variable T' : NaturalTransformation F' F''.
+ Variable T : NaturalTransformation F F'.
+
+ Local Notation CO c := (T' c o T c).
+
+ Definition composeT
+ : NaturalTransformation F F'' := Build_NaturalTransformation F F'' (fun c => CO c).
+
+End compose.
+
+Section whisker.
+ Variable C : PreCategory.
+ Variable D : PreCategory.
+ Variable E : PreCategory.
+
+ Section L.
+ Variable F : Functor D E.
+ Variables G G' : Functor C D.
+ Variable T : NaturalTransformation G G'.
+
+ Local Notation CO c := (morphism_of F (T c)).
+
+ Definition whisker_l
+ := Build_NaturalTransformation
+ (F o G) (F o G')
+ (fun c => CO c).
+
+ End L.
+
+ Section R.
+ Variables F F' : Functor D E.
+ Variable T : NaturalTransformation F F'.
+ Variable G : Functor C D.
+
+ Local Notation CO c := (T (G c)).
+
+ Definition whisker_r
+ := Build_NaturalTransformation
+ (F o G) (F' o G)
+ (fun c => CO c).
+ End R.
+End whisker.
+Infix "o" := composeT : natural_transformation_scope.
+Infix "oL" := whisker_l (at level 40, left associativity) : natural_transformation_scope.
+Infix "oR" := whisker_r (at level 40, left associativity) : natural_transformation_scope.
+
+Section path_natural_transformation.
+
+ Variable C : PreCategory.
+ Variable D : PreCategory.
+ Variables F G : Functor C D.
+
+ Lemma equiv_sig_natural_transformation
+ : { CO : forall x, morphism D (F x) (G x)
+ | forall s d (m : morphism C s d),
+ CO d o F _1 m = G _1 m o CO s }
+ <~> NaturalTransformation F G.
+ admit.
+ Defined.
+
+ Global Instance trunc_natural_transformation
+ : IsHSet (NaturalTransformation F G).
+ Proof.
+ eapply trunc_equiv'; [ exact equiv_sig_natural_transformation | ].
+ admit.
+ Qed.
+
+End path_natural_transformation.
+Definition functor_category (C D : PreCategory) : PreCategory
+ := @Build_PreCategory (Functor C D) (@NaturalTransformation C D) (@composeT C D) _.
+
+Notation "C -> D" := (functor_category C D) : category_scope.
+
+Definition NaturalIsomorphism (C D : PreCategory) F G := @Isomorphic (C -> D) F G.
+
+Coercion natural_transformation_of_natural_isomorphism C D F G (T : @NaturalIsomorphism C D F G) : NaturalTransformation F G
+ := T : morphism _ _ _.
+Local Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
+Global Instance isisomorphism_compose'
+ `(T' : @NaturalTransformation C D F' F'')
+ `(T : @NaturalTransformation C D F F')
+ `{@IsIsomorphism (C -> D) F' F'' T'}
+ `{@IsIsomorphism (C -> D) F F' T}
+: @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
+ := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+
+Section lemmas.
+ Local Open Scope natural_transformation_scope.
+
+ Variable C : PreCategory.
+ Variable F : C -> PreCategory.
+ Context
+ {w x y z}
+ {f : Functor (F w) (F z)} {f0 : Functor (F w) (F y)}
+ {f1 : Functor (F x) (F y)} {f2 : Functor (F y) (F z)}
+ {f3 : Functor (F w) (F x)} {f4 : Functor (F x) (F z)}
+ {f5 : Functor (F w) (F z)} {n : f5 <~=~> (f4 o f3)%functor}
+ {n0 : f4 <~=~> (f2 o f1)%functor} {n1 : f0 <~=~> (f1 o f3)%functor}
+ {n2 : f <~=~> (f2 o f0)%functor}.
+
+ Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper'
+ : @IsIsomorphism
+ (_ -> _) _ _
+ (n2 ^-1 o (f2 oL n1 ^-1 o (admit o (n0 oR f3 o n))))%natural_transformation.
+ Proof.
+ eapply isisomorphism_compose';
+ [ eapply isisomorphism_inverse
+ | eapply isisomorphism_compose';
+ [ admit
+ | eapply isisomorphism_compose';
+ [ admit |
+ eapply isisomorphism_compose'; [ admit | ]]]].
+ Set Printing All. Set Printing Universes.
+ apply @isisomorphism_isomorphic.
+ Qed.
+
+End lemmas.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 01:39:41 +0000