aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_108.v
blob: 4f5ef997401baa7091957d7da46ff3dad7d0ea89 (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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
Require Import TestSuite.admit.
(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
(* NOTE: This bug is only triggered with -load-vernac-source / in interactive mode. *)
(* File reduced by coq-bug-finder from 139 lines to 124 lines. *)
Set Universe Polymorphism.
Reserved Notation "g 'o' f" (at level 40, left associativity).
Generalizable All Variables.
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.

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.

Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
: forall x, f x = g x
  := fun x => match h with idpath => idpath end.

Definition ap11 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y) : f x = g y.
  admit.
Defined.
Class IsEquiv {A B : Type} (f : A -> B) := {}.
Class Contr_internal (A : Type) := BuildContr {
                                       center : A ;
                                       contr : (forall y : A, center = y)
                                     }.

Arguments center A {_}.

Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.

Fixpoint nat_to_trunc_index (n : nat) : trunc_index
  := match n with
       | 0 => trunc_S (trunc_S minus_two)
       | S n' => trunc_S (nat_to_trunc_index n')
     end.

Coercion nat_to_trunc_index : nat >-> trunc_index.

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
  match n with
    | minus_two => Contr_internal A
    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
  end.
Class IsTrunc (n : trunc_index) (A : Type) : Type :=
  Trunc_is_trunc : IsTrunc_internal n A.

Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
: IsTrunc n (x = y)
  := H x y.

Notation Contr := (IsTrunc minus_two).

Notation IsHSet := (IsTrunc 0).

Class Funext :=
  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
Global Instance contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
: Contr (forall a, P a) | 100.
admit.
Defined.
Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a) | 100.
Proof.
  generalize dependent P.
  induction n as [ | n' IH]; [ | admit ]; simpl; intros P ?.
                                                        exact _.
Defined.
Set Implicit Arguments.

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';
    trunc_morphism : forall s d, IsHSet (morphism s d) }.

Existing Instance trunc_morphism.
Infix "o" := (@compose _ _ _ _) : morphism_scope.
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);
    composition_of : forall s d d'
                            (m1 : morphism C s d) (m2: morphism C d d'),
                       morphism_of _ _ (m2 o m1)
                       = (morphism_of _ _ m2) o (morphism_of _ _ m1);
    identity_of : forall x, morphism_of _ _ (@identity _ x)
                            = @identity _ (object_of x) }.

Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
  forall x : A, r (s x) = x.

Section path_functor.
  Context `{Funext}.
  Variable C : PreCategory.
  Variable D : PreCategory.
  Local Notation path_functor'_T F G
    := { HO : object_of F = object_of G
       | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d))
                   HO
                   (morphism_of F)
         = morphism_of G }
         (only parsing).
  Definition path_functor'_sig (F G : Functor C D) : path_functor'_T F G -> F = G.
  Proof.
    intros [H' H''].
    destruct F, G; simpl in *.
    induction H'. (* while destruct H' works *) destruct H''.
    apply ap11; [ apply ap | ];
    apply center; abstract exact _.
    Set Printing Universes.
    (* Fail Defined.*)
  (* The command has indeed failed with message:
=> Error: path_functor'_sig_subproof already exists. *)
  Defined.
(* Anomaly: Backtrack.backto 55: a state with no vcs_backup. Please report. *)
End path_functor.