closes #30

src/CubicalHott/Theorem7-1-9.agda

@@ -0,0 +1,31 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem7-1-9 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Equiv
+open import Cubical.Functions.FunExtEquiv
+open import Data.Nat
+
+theorem : {A : Type} {B : A → Type}
+  → (n : ℕ)
+  → ((a : A) → isOfHLevel n (B a))
+  → isOfHLevel n ((x : A) → B x)
+theorem {A = A} {B = B} zero prf = (λ x → fst (prf x)) , helper where
+  helper : (f' : (x : A) → B x) → (λ x → fst (prf x)) ≡ f'
+  helper f' i x =
+    let given = snd (prf x) in
+    given (f' x) i
+theorem (suc zero) prf f1 f2 i x =
+  let result = prf x (f1 x) (f2 x) in
+  result i
+theorem {A = A} {B = B} (2+ n) prf f1 f2 =
+  subst (isOfHLevel (suc n)) funExtPath (theorem (suc n) λ a → prf a (f1 a) (f2 a))
+  -- goal1 where
+  -- goal1 : isOfHLevel (suc n) (f1 ≡ f2)
+  -- goal2 : isOfHLevel (suc n) ((a : A) → f1 a ≡ f2 a)
+  -- goal1 = subst (λ x → isOfHLevel (suc n) x) funExtPath goal2
+
+  -- IH = theorem {A = A} {B = λ a → f1 a ≡ f2 a} (suc n) λ a → prf a (f1 a) (f2 a)
+  -- goal2 = IH