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
32
33
34
35
|
Set Asymmetric Patterns.
Generalizable All Variables.
Set Implicit Arguments.
Set Universe Polymorphism.
Record SpecializedCategory (obj : Type) :=
{
Object :> _ := obj;
Morphism : obj -> obj -> Type;
Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
}.
Arguments Compose {obj} [C s d d'] _ _ : rename.
Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
match m in @ReifiedMorphism objC C s d return Morphism C s d with
| ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
(@ReifiedMorphismDenote _ _ _ _ m2)
end.
Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
refine match m with
| ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
end; clear m.
(* This fails with an error rather than an anomaly, but morally
it should work, if destruct were able to do the good generalization
in advance, before doing the "intros []". *)
Fail destruct (@ReifiedMorphismSimplifyWithProof T s1 d0 d0' m1) as [ [] ? ].
Abort.
|
