From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3485.v | 133 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 test-suite/bugs/closed/3485.v (limited to 'test-suite/bugs/closed/3485.v') diff --git a/test-suite/bugs/closed/3485.v b/test-suite/bugs/closed/3485.v new file mode 100644 index 00000000..ede6b3cb --- /dev/null +++ b/test-suite/bugs/closed/3485.v @@ -0,0 +1,133 @@ +Set Universe Polymorphism. +Set Primitive Projections. +Reserved Infix "o" (at level 40, left associativity). +Definition relation (A : Type) := A -> A -> Type. +Class Transitive {A} (R : relation A) := transitivity : forall x y z, R x y -> R y z -> R x z. +Tactic Notation "etransitivity" open_constr(y) := + let R := match goal with |- ?R ?x ?z => constr:(R) end in + let x := match goal with |- ?R ?x ?z => constr:(x) end in + let z := match goal with |- ?R ?x ?z => constr:(z) end in + refine (@transitivity _ R _ x y z _ _). +Tactic Notation "etransitivity" := etransitivity _. +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation "x .1" := (projT1 x) (at level 3) : fibration_scope. +Notation "x .2" := (projT2 x) (at level 3) : fibration_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end. +Instance transitive_paths {A} : Transitive (@paths A) | 0 := @concat A. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Class Contr_internal (A : Type) := { center : A ; contr : (forall y : A, center = y) }. +Generalizable Variables X A B C f g n. +Definition projT1_path `{P : A -> Type} {u v : sigT P} (p : u = v) : u.1 = v.1 := ap (@projT1 _ _) p. +Notation "p ..1" := (projT1_path p) (at level 3) : fibration_scope. +Ltac simpl_do_clear tac term := + let H := fresh in + assert (H := term); + simpl in H |- *; + tac H; + clear H. +Set Implicit Arguments. +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; + + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f }. +Arguments identity {C%category} / x%object : rename. +Arguments compose {C%category} / {s d d'}%object (m1 m2)%morphism : rename. +Infix "o" := compose : morphism_scope. +Notation "1" := (identity _) : morphism_scope. +Delimit Scope functor_scope with functor. +Local Open Scope morphism_scope. +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); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) }. +Bind Scope functor_scope with Functor. +Arguments morphism_of [C%category] [D%category] F%functor / [s%object d%object] m%morphism : rename. +Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. +Section composition. + Variable C : PreCategory. + Variable D : PreCategory. + Variable E : PreCategory. + Variable G : Functor D E. + Variable F : Functor C D. + + Local Notation c_object_of c := (G (F c)) (only parsing). + Local Notation c_morphism_of m := (morphism_of G (morphism_of F m)) (only parsing). + + Definition compose_identity_of x + : c_morphism_of (identity x) = identity (c_object_of x) + := transport (@paths _ _) + (identity_of G _) + (ap (@morphism_of _ _ G _ _) (identity_of F x)). + + Definition composeF : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => morphism_of G (morphism_of F m)) + compose_identity_of. +End composition. +Infix "o" := composeF : functor_scope. + +Definition identityF C : Functor C C + := Build_Functor C C + (fun x => x) + (fun _ _ x => x) + (fun _ => idpath). +Notation "1" := (identityF _) : functor_scope. + +Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }. + +Section unit. + Variable C : PreCategory. + Variable D : PreCategory. + Variable F : Functor C D. + Variable G : Functor D C. + + Definition AdjunctionUnit := + { T : NaturalTransformation 1 (G o F) + & forall (c : C) (d : D) (f : morphism C c (G d)), + Contr_internal { g : morphism D (F c) d & G _1 g o T c = f } + }. +End unit. +Variable C : PreCategory. +Variable D : PreCategory. +Variable F : Functor C D. +Variable G : Functor D C. + +Definition zig__of__adjunction_unit + (A : AdjunctionUnit F G) + (Y : C) + (eta := A.1) + (eps := fun X => (@center _ (A.2 (G X) X 1)).1) +: G _1 (eps (F Y) o F _1 (eta Y)) o eta Y = eta Y + -> eps (F Y) o F _1 (eta Y) = 1. +Proof. + intros. + etransitivity; [ symmetry | ]; + simpl_do_clear + ltac:(fun H => apply H) + (fun y H => (@contr _ (A.2 _ _ (A.1 Y)) (y; H))..1); + try assumption. + simpl. + rewrite ?@identity_of, ?@left_identity, ?@right_identity; + reflexivity. +Qed. -- cgit v1.2.3