wip

src/HottBook/Chapter8.lagda.md

@@ -86,10 +86,14 @@ module lemma8∙1∙2 where
   open definition8∙1∙1
   open axiom2∙10∙3
   open ≡-Reasoning
+  open S¹
+
+  lifted-loop : {l : Level} → lift base ≡ lift base
+  lifted-loop {l} = ap (lift {l = l}) loop
 
   i : {l : Level} → (x : Int {l}) → (transport code loop x) ≡ int-suc x
   i x = begin
-    (transport code loop x) ≡⟨ lemma2∙3∙10 {! id  !} code loop x ⟩
+    (transport code loop x) ≡⟨ lemma2∙3∙10 id code {! lifted-loop  !} x ⟩
     (transport id (ap code loop) x) ≡⟨ {!   !} ⟩
     -- (transport id (ua int-suc) x) ≡⟨ {!   !} ⟩
     int-suc x ∎

src/HottBook/CoreUtil.agda

@@ -4,6 +4,6 @@ module HottBook.CoreUtil where
 
 open import Agda.Primitive
 
-record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
+record Lift {a l} (A : Set a) : Set (a ⊔ l) where
   constructor lift
   field lower : A