tiny/adjunction.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
42
refl (A : U) (x : A) : Path x x
    := λ i. x;

eta (A : U) (x : A)
    : √ ((i : T) → A[i])
  := rintro λ i. x[i];

epsilon
  (B : T → √ U)
  (f : (t : T) → √ relim j. B[j] t[j])
  : relim j. B j
  := relim i. f(i);

transpose_left
  (A : U)
  (B : A → √ U)
  (f : (a : A) → √ relim i. B[i] a[i])
  : (√ ((h : (t : T) → A[t]) → relim i. B[i] (h i)))
  := rintro λ h. relim k. f[k] (h k);

transpose_right
  (A : U)
  (B : A → √ U)
  (g : √ (h : (t : T) → A[t]) → relim i. B[i] (h i))
  : ((a : A) → √ relim i. B[i] a[i])
  := λ a. rintro (relim i. g[i]) (λ j. a[j]);

inv_left
  (A : U)
  (B : A → √ U)
  (f : (a : A) → √ relim i. B[i] a[i])
  : Path f (transpose_right A B (transpose_left A B f))
  := refl ((a : A) → √ relim i. B[i] a[i]) f;

inv_right
  (A : U)
  (B : A → √ U)
  (g : √ (h : (t : T) → A[t]) → relim i. B[i] (h i))
  : Path g (transpose_left A B (transpose_right A B g))
  := refl (√ (h : (t : T) → A[t]) → relim i. B[i] (h i)) g;

inv_right