From 750e9a218bea4b91a7c5a40fa1dba6bd06facc6b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 14 Oct 2024 21:10:08 -0500
Subject: [PATCH] closes #30

---
 src/CubicalHott/Theorem7-1-9.agda | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 src/CubicalHott/Theorem7-1-9.agda

diff --git a/src/CubicalHott/Theorem7-1-9.agda b/src/CubicalHott/Theorem7-1-9.agda
new file mode 100644
index 0000000..131d45a
--- /dev/null
+++ b/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
\ No newline at end of file