3.5 subsets

src/HottBook/Chapter3.lagda.md

@@ -329,9 +329,40 @@ module definition3∙4∙3 where
 
 ## 3.5 Subsets and propositional resizing
 
+### Lemma 3.5.1
+
+```
+lemma3∙5∙1 : {A : Set} {P : A → Set}
+  → ((x : A) → isProp (P x))
+  → (u v : Σ A P)
+  → (Σ.fst u ≡ Σ.fst v)
+  → u ≡ v
+lemma3∙5∙1 {P = P} f u v p = 
+  let
+    eqv = theorem2∙7∙2 u v
+    func = Σ.fst (lemma2∙4∙12.sym-equiv eqv)
+    prf = p , f (Σ.fst v) (transport P p (Σ.snd u)) (Σ.snd v)
+  in func prf
 ```
 
 ```
+SubProp : (l : Level) → Set (lsuc l)
+SubProp l = Σ (Set l) isProp
+```
+
+```
+equation3∙5∙4 : {l : Level} → SubProp l → SubProp (lsuc l)
+equation3∙5∙4 {l} (A , Aprop) = Lift A , λ x y → ap lift (Aprop (Lift.lower x) (Lift.lower y))
+```
+
+### Axiom 3.5.5
+
+Not able to be proved, but is consistent
+
+```
+postulate
+  propResizingEquiv : {l : Level} → isequiv (equation3∙5∙4 {l})
+```
 
 ## 3.6 The logic of mere propositions