tiny/examples.tiny at master · mvr/tiny · GitHub

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
the (A : U) (a : A) : A := a;

const : (A B : U) → A → B → A
  := λ A B x y. x;

comp (A : U) (B : U) (C : U)
    (f : B → C)
    (g : A → B)
    : (A → C)
  := λ x. f (g x);

extract
  (A : √ U)
  (x : √ relim i. A[i])
  : relim i. A
  := relim i. x;

duplicate (A : √ U)
  (r : √ relim i. A[i])
  : (√ √ relim i. A[i, i])
  := rintro rintro relim i. r[i, i];

iteratedkeys : T → √ (T → T)
  := λ i. rintro (λ j. i[i[i[i[j]]]]);

functorial (A : √ U) (B : √ U)
  (f : √ ((relim i. A[i]) → (relim i. B[i])))
  : (√ (relim i. A[i])) → (√ relim i. B[i])
  := λ r. rintro (relim i. f[i]) (relim i. r[i]);

preserve_sigma (A : √ U) (B : √ (relim i. A[i]) → U)
  (r : √ (x : relim i. A[i]) × (relim i. B[i]) x)
  : (x : √ relim i. A[i]) × √ (relim i. B[i]) (relim i. x[i])
  := < rintro fst relim i. r[i], rintro snd relim i. r[i] >;

preserve_sigma_inv (A : √ U) (B : √ (relim i. A[i]) → U)
  (p : (x : √ relim i. A[i]) × √ (relim i. B[i]) (relim i. x[i]))
  : (√ (x : relim i. A[i]) × (relim i. B[i]) x)
  := rintro < relim i. fst p[i] , relim i. snd p[i] >;

T