blob: ed4895115e0d6e31ea04fa33a969878bc6e0fb91 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
(* Checking use of eta on Flexible/Rigid and SemiFlexible/Rigid unif problems *)
Set Implicit Arguments.
Generalizable All Variables.
Record Category {obj : Type} :=
{
Morphism : obj -> obj -> Type;
Identity : forall x, Morphism x x;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d';
LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
}.
Section DiscreteAdjoints.
Let C := {|
Morphism := (fun X Y : Type => X -> Y);
Identity := (fun X : Type => (fun x : X => x));
Compose := (fun _ _ _ f g => (fun x => f (g x)));
LeftIdentity := (fun X Y p => @eq_refl _ p : (fun x : X => p x) = p)
|}.
Variable ObjectFunctor : C = C.
Goal True.
Proof.
subst C.
revert ObjectFunctor.
intro ObjectFunctor.
simpl in ObjectFunctor.
revert ObjectFunctor. (* Used to failed in 8.4 up to 16 April 2013 *)
|
