xxxxxxxxxx
142
 
1
#lang rzk-1
2
​
3
-- A is contractible there exists x : A such that for any y : A we have x = y.
4
#def iscontr (A : U) : U
5
  := ∑ (a : A), (x : A) -> a =_{A} x
6
​
7
-- A is a proposition if for any x, y : A we have x = y
8
#def isaprop (A : U) : U
9
  := (x : A) -> (y : A) -> x =_{A} y
10
​
11
-- A is a set if for any x, y : A the type x =_{A} y is a proposition
12
#def isaset (A : U) : U
13
  := (x : A) -> (y : A) -> isaprop (x =_{A} y)
14
​
15
-- Non-dependent product of A and B
16
#def prod (A : U) (B : U) : U
17
  := ∑ (x : A), B
18
​
19
-- A function f : A -> B is an equivalence
20
-- if there exists g : B -> A
21
-- such that for all x : A we have g (f x) = x
22
-- and for all y : B we have f (g y) = y
23
#def isweq (A : U) (B : U) (f : A -> B) : U
24
  := ∑ (g : B -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)
25
​
26
-- Equivalence of types A and B
27
#def weq (A : U) (B : U) : U
28
  := ∑ (f : A -> B), isweq A B f
29
​
30
-- Transport along a path
31
#def transport
32
    (A : U)
33
    (C : A -> U)
34
    (x y : A)
35
    (p : x =_{A} y)
36
    : C x -> C y
37
  := \cx -> idJ(A, x, (\z q -> C z), cx, y, p)
38
​
39
-- [RS17, Axiom 4.6] Relative function extensionality.
40
#def relfunext : U
41
  := (I : CUBE)
42
  -> (psi : I -> TOPE)
43
  -> (phi : psi -> TOPE)
44
  -> (A : psi -> U)
45
  -> ((t : psi) -> iscontr (A t))
46
  -> (a : (t : phi) -> A t)
47
  -> (t : psi) -> A t [ phi t |-> a t]
48
​
49
-- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
50
#def relfunext2 : U
51
  := (I : CUBE)
52
  -> (psi : I -> TOPE)
53
  -> (phi : psi -> TOPE)
54
  -> (A : psi -> U)
55
  -> (a : (t : phi) -> A t)
56
  -> (f : (t : psi) -> A t [ phi t |-> a t ])
57
  -> (g : (t : psi) -> A t [ phi t |-> a t ])
58
  -> weq (f = g)
59
         ((t : psi) -> (f t =_{A t} g t) [ phi t |-> refl ])
60
​
61
-- Restrict extension type to a subshape.
62
#def restrict
63
    (I : CUBE)
64
    (psi : I -> TOPE)
65
    (phi : I -> TOPE)
66
    (A : {t : I | psi t \/ phi t} -> U)
67
    (a : {t : I | psi t} -> A t)
68
  : {t : I | psi t /\ phi t} -> A t
69
  := \t -> a t
70
​
71
-- Reformulate extension type as an extension of a restriction.
72
#def ext-of-restrict
73
    (I : CUBE)
74
    (psi : I -> TOPE)
75
    (phi : I -> TOPE)
76
    (A : {t : I | psi t \/ phi t} -> U)
77
    (a : {t : I | psi t} -> A t)
78
  : (t : psi) -> A t [ psi t /\ phi t |-> restrict I psi phi A a t ]
79
  := a
80
​
81
-- Transform extension of an identity into an identity of restrictions.
82
#def restricts-path
83
    (r : relfunext2)
84
    (I : CUBE)
85
    (psi : I -> TOPE)
86
    (phi : I -> TOPE)
87
    (A : {t : I | psi t \/ phi t} -> U)
88
    (a_psi : (t : psi) -> A t)
89
    (a_phi : (t : phi) -> A t)
90
    (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
91
  : restrict I psi phi A a_psi = restrict I phi psi A a_phi
92
  := (first (second (r I
93
      (\t -> psi t /\ phi t)
94
      (\t -> BOT)
95
      (\t -> A t)
96
      (\t -> recBOT)
97
      (\t -> a_psi t)
98
      (\t -> a_phi t)))) e
99
​
100
-- A weaker version of recOR, demanding only a path between a and b:
101
-- recOR(psi, phi, a, b) demands that for psi /\ phi we have a == b (definitionally)
102
-- (recId psi phi a b e) demands that e is the proof that a = b (intensionally) for psi /\ phi
103
#def recId
104
    (r : relfunext2)
105
    (I : CUBE)
106
    (psi : I -> TOPE)
107
    (phi : I -> TOPE)
108
    (A : {t : I | psi t \/ phi t} -> U)
109
    (a_psi : (t : psi) -> A t)
110
    (a_phi : (t : phi) -> A t)
111
    (e : {t : I | psi t /\ phi t} -> a_psi t = a_phi t)
112
  : {t : I | psi t \/ phi t} -> A t
113
  := \t -> recOR(
114
        psi t |-> transport
115
          ({t : I | psi t /\ phi t} -> A t)
116
          (\ra -> (t : psi) -> A t [ psi t /\ phi t |-> ra t])
117
          (restrict I psi phi A a_psi)
118
          (restrict I phi psi A a_phi)
119
          (restricts-path r I psi phi A a_psi a_phi e)
120
          (ext-of-restrict I psi phi A a_psi)
121
          t,
122
        phi t |-> ext-of-restrict I phi psi A a_phi t
123
      )
124
​
125
-- If two extension types are equal along two subshapes,
126
-- then they are also equal along their union.
127
#def id-along-border
128
    (r : relfunext2)
129
    (I : CUBE)
130
    (psi : I -> TOPE)
131
    (phi : I -> TOPE)
132
    (A : {t : I | psi t \/ phi t} -> U)
133
    (a b : {t : I | psi t \/ phi t} -> A t)
134
    (e_psi : (t : psi) -> a t = b t)
135
    (e_phi : (t : phi) -> a t = b t)
136
    (border-is-a-set : {t : I | psi t /\ phi t} -> isaset (A t))
137
  : {t : I | psi t \/ phi t} -> a t = b t
138
  := recId r I psi phi
139
        (\t -> a t = b t)
140
        e_psi e_phi
141
        (\t -> border-is-a-set t (a t) (b t) (e_psi t) (e_phi t))
142
​