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
|
Set Universe Polymorphism.
Module A.
Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
Notation "x = y" := (paths _ x y).
Inductive IsTrunc : nat -> Type -> Type :=
| BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
| trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
Existing Class IsTrunc.
#[export] Instance is_trunc_unit : IsTrunc 0 unit.
Proof. apply BuildContr with (center:=tt). now intros []. Defined.
Check (_ : IsTrunc 0 unit).
End A.
Module B.
Fixpoint IsTrunc (n : nat) (A : Type) : Type :=
match n with
| O => True
| S _ => False
end.
Existing Class IsTrunc.
#[export] Instance is_trunc_unit : IsTrunc 0 unit.
Proof. exact I. Defined.
Check (_ : IsTrunc 0 unit).
Fail Definition foo := (_ : IsTrunc 1 unit).
End B.
|
