fixed import issues

0Trinitarianism/Preambles/P5.agda

@@ -0,0 +1,37 @@
+module 0Trinitarianism.Preambles.P5 where
+
+open import Cubical.Foundations.Prelude renaming
+  (funExt to libFunExt ;
+   sym to libSym ;
+   _≡⟨_⟩_ to lib_≡⟨_⟩_ ;
+   _∎ to lib_∎ ;
+   _∙_ to lib_∙_ ;
+   fst to libFst ;
+   snd to libSnd
+  ) public
+open import Cubical.HITs.S1 using ( S¹ ; base ; loop ) public
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
+open import Cubical.Foundations.Path public
+open import 0Trinitarianism.Quest4Solutions public
+open import 1FundamentalGroup.Quest0Solutions public
+open import Cubical.Data.Bool public
+
+pathToFun≡transport : {u : Level} {A B : Type u} (p : A ≡ B) (x : A)
+  → pathToFun p x ≡ transport p x
+pathToFun≡transport {u} {A} = J (λ B p → (x : A) → pathToFun p x ≡ transport p x)
+  λ x →
+      pathToFun refl x
+    ≡⟨ pathToFunReflx x ⟩
+      x
+    ≡⟨ sym (transportRefl x) ⟩
+      transport refl x ∎
+
+PathPIsoPathD : {u : Level} {A B : Type u} (p : A ≡ B) (x : A) (y : B) →
+  (PathP (λ i → p i) x y) ≅ (pathToFun p x ≡ y)
+PathPIsoPathD {u} {A} {B} p x =
+  subst (λ b → (y : B) → (PathP (λ i → p i) x y) ≅ (b ≡ y))
+    (sym (pathToFun≡transport p x))
+    (PathPIsoPath _ x)
+
+
+

0Trinitarianism/Quest4Solutions.agda

@@ -7,30 +7,30 @@ private
     u : Level
 
 
-data Id {A : Type} : (x y : A) → Type where
+data Id {A : Type u} : (x y : A) → Type u where
 
   rfl : {x : A} → Id x x
 
-idSym : (A : Type) (x y : A) → Id x y → Id y x
+idSym : (A : Type u) (x y : A) → Id x y → Id y x
 idSym A x .x rfl = rfl
 
-Sym : {A : Type} {x y : A} → Id x y → Id y x
+Sym : {A : Type u} {x y : A} → Id x y → Id y x
 Sym rfl = rfl
 
-_*_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+_*_ : {A : Type u} {x y z : A} → Id x y → Id y z → Id x z
 rfl * q = q
 
-_*0_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+_*0_ : {A : Type u} {x y z : A} → Id x y → Id y z → Id x z
 p *0 rfl = p
 
-_*1_ : {A : Type} {x y z : A} → Id x y → Id y z → Id x z
+_*1_ : {A : Type u} {x y z : A} → Id x y → Id y z → Id x z
 rfl *1 rfl = rfl
 
 ------------Cong-------------------------
 
 private
   variable
-    A B : Type
+    A B : Type u
     w x y z : A
 
 ------------Groupoid Laws----------------
@@ -54,14 +54,14 @@ Assoc rfl q r = rfl
 
 -------------Mapping Out----------------
 
-outOfId : (M : (y : A) → Id x y → Type) → M x rfl
+outOfId : (M : (y : A) → Id x y → Type u) → M x rfl
   → {y : A} (p : Id x y) → M y p
 outOfId M h rfl = h
 
 ------------Path vs Id--------------------
 
 Path→Id : x ≡ y → Id x y
-Path→Id {A} {x} = J (λ y p → Id x y) rfl
+Path→Id {u} {A} {x} = J (λ y p → Id x y) rfl
 
 Id→Path : Id x y → x ≡ y
 Id→Path rfl = refl
@@ -83,21 +83,21 @@ Path→IdRefl : Path→Id (refl {x = x}) ≡ rfl
 Path→IdRefl {x = x} = JRefl (λ y p → Id x y) rfl
 
 Path≡Id : (x ≡ y) ≡ (Id x y)
-Path≡Id {A} {x} {y} = isoToPath (iso Path→Id Id→Path rightInv leftInv) where
+Path≡Id {u} {A} {x} {y} = isoToPath (iso Path→Id Id→Path rightInv leftInv) where
 
-  rightInv : section (Path→Id {A} {x} {y}) Id→Path
+  rightInv : section (Path→Id {u} {A} {x} {y}) Id→Path
   rightInv rfl = Path→IdRefl
 
-  leftInv : retract (Path→Id {A} {x} {y}) Id→Path
+  leftInv : retract (Path→Id {u} {A} {x} {y}) Id→Path
   leftInv = J (λ y p → Id→Path (Path→Id p) ≡ p) (cong (λ p → Id→Path p) Path→IdRefl)
 
 -----------Basics about Path Space-----------------
 
 sym : {x y : A} → x ≡ y → y ≡ x
-sym {A} {x} = J (λ y1 p → y1 ≡ x) refl
+sym {u} {A} {x} = J (λ y1 p → y1 ≡ x) refl
 
-symRefl : {x : A} → sym {A} {x} {x} (refl) ≡ refl
-symRefl {A} {x} = JRefl (λ y1 p → y1 ≡ x) refl
+symRefl : {x : A} → sym {u} {A} {x} {x} (refl) ≡ refl
+symRefl {u} {A} {x} = JRefl (λ y1 p → y1 ≡ x) refl
 
 Trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 Trans {x = x} {z = z} = J (λ y1 p → y1 ≡ z → x ≡ z) λ q → q
@@ -114,20 +114,20 @@ infixr 30 _∙_
 infix  3 _∎
 infixr 2 _≡⟨_⟩_
 
-TransRefl : {x y : A} → Trans {A} {x} {x} {y} refl ≡ λ q → q
+TransRefl : {x y : A} → Trans {u} {A} {x} {x} {y} refl ≡ λ q → q
 TransRefl {x = x} {y = y} = JRefl ((λ y1 p → y1 ≡ y → x ≡ y)) λ q → q
 
 refl∙refl : {x : A} → refl {_} {A} {x} ∙ refl ≡ refl
 refl∙refl = cong (λ f → f refl) TransRefl
 
 ∙refl : {x y : A} (p : x ≡ y) → Trans p refl ≡ p
-∙refl {A} {x} {y} = J (λ y p → Trans p refl ≡ p) refl∙refl
+∙refl {u} {A} {x} {y} = J (λ y p → Trans p refl ≡ p) refl∙refl
 
-refl∙ : {A : Type} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
+refl∙ : {A : Type u} {x y : A} (p : x ≡ y) → refl ∙ p ≡ p
 refl∙ = J (λ y p → refl ∙ p ≡ p) refl∙refl
 
 
-∙sym : {A : Type} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
+∙sym : {A : Type u} {x y : A} (p : x ≡ y) → p ∙ sym p ≡ refl
 ∙sym = J (λ y p → p ∙ sym p ≡ refl)
        (
          refl ∙ sym refl
@@ -138,7 +138,7 @@ refl∙ = J (λ y p → refl ∙ p ≡ p) refl∙refl
        )
 
 
-sym∙ : {A : Type} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
+sym∙ : {A : Type u} {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl
 sym∙ = J (λ y p → (sym p) ∙ p ≡ refl)
        (
          (sym refl) ∙ refl
@@ -148,9 +148,9 @@ sym∙ = J (λ y p → (sym p) ∙ p ≡ refl)
          refl ∎
        )
 
-assoc : {A : Type} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
+assoc : {A : Type u} {w x : A} (p : w ≡ x) {y z : A} (q : x ≡ y) (r : y ≡ z)
         → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
-assoc {A} = J
+assoc {u} {A} = J
         -- casing on p
         (λ x p → {y z : A} (q : x ≡ y) (r : y ≡ z) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r))
         -- reduce to showing when p = refl
@@ -166,50 +166,50 @@ id : A → A
 id x = x
 
 pathToFun : A ≡ B → A → B
-pathToFun {A} = J (λ B p → (A → B)) id
+pathToFun {u} {A} = J (λ B p → (A → B)) id
 
 pathToFunRefl : pathToFun (refl {x = A}) ≡ id
-pathToFunRefl {A} = JRefl (λ B p → (A → B)) id
+pathToFunRefl {u} {A} = JRefl (λ B p → (A → B)) id
 
-pathToFunReflx : pathToFun (refl {x = A}) x ≡ x
-pathToFunReflx {x = x} = cong (λ f → f x) pathToFunRefl
+pathToFunReflx : (x : A) → pathToFun (refl {x = A}) x ≡ x
+pathToFunReflx x = cong (λ f → f x) pathToFunRefl
 
-endPt : (B : A → Type) (p : x ≡ y) → B x → B y
+endPt : (B : A → Type u) (p : x ≡ y) → B x → B y
 endPt {x = x} B = J (λ y p → B x → B y) id
 
-endPtRefl : (B : A → Type) → endPt B (refl {x = x}) ≡ id
+endPtRefl : (B : A → Type u) → endPt B (refl {x = x}) ≡ id
 endPtRefl {x = x} B = JRefl ((λ y p → B x → B y)) id
 
-endPt' : (B : A → Type) (p : x ≡ y) → B x → B y
+endPt' : (B : A → Type u) (p : x ≡ y) → B x → B y
 endPt' B p = pathToFun (cong B p )
 
 --------------funExt---------------------
 
-funExt : (B : A → Type) (f g : (a : A) → B a) →
+funExt : {B : A → Type u} {f g : (a : A) → B a} →
   ((a : A) → f a ≡ g a) → f ≡ g
-funExt B f g h = λ i a → h a i
+funExt h = λ i a → h a i
 
-funExtPath : (B : A → Type) (f g : (a : A) → B a) → (f ≡ g) ≡ ((a : A) → f a ≡ g a)
-funExtPath {A} B f g = isoToPath (iso fun (funExt B f g) rightInv leftInv) where
+funExtPath : (B : A → Type u) (f g : (a : A) → B a) → (f ≡ g) ≡ ((a : A) → f a ≡ g a)
+funExtPath {u} {A} B f g = isoToPath (iso fun funExt rightInv leftInv) where
 
   fun : f ≡ g → (a : A) → f a ≡ g a
   fun h = λ a i → h i a
 
-  rightInv : section fun (funExt B f g)
+  rightInv : section fun funExt
   rightInv h = refl
 
-  leftInv : retract fun (funExt B f g)
+  leftInv : retract fun funExt
   leftInv h = refl
 
 --------------Path on Products-----------
 
-data _×_ (A B : Type) : Type where
+data _×_ (A B : Type u) : Type u where
 
   _,_ : A → B → A × B
 
-Id× : {A B : Type} (a0 a1 : A) (b0 b1 : B)
-  → (Id {A × B} ( a0 , b0 ) ( a1 , b1 )) ≡ (Id a0 a1 × Id b0 b1)
-Id× {A} {B} a0 a1 b0 b1 = isoToPath (iso fun inv rightInv leftInv) where
+Id× : (a0 a1 : A) (b0 b1 : B)
+  → (Id {u} {A × B} ( a0 , b0 ) ( a1 , b1 )) ≡ (Id a0 a1 × Id b0 b1)
+Id× {u} {A} {B} a0 a1 b0 b1 = isoToPath (iso fun inv rightInv leftInv) where
 
   fun : Id {A = A × B} ( a0 , b0 ) ( a1 , b1 ) → Id a0 a1 × Id b0 b1
   fun rfl = rfl , rfl
@@ -229,8 +229,8 @@ fst (a , b) = a
 snd : A × B → B
 snd (a , b) = b
 
-Path× : {A B : Type} (x y : A × B) → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y))
-Path× {A} {B} (a0 , b0) (a1 , b1) =
+Path× : {A B : Type u} (x y : A × B) → (x ≡ y) ≡ ((fst x ≡ fst y) × (snd x ≡ snd y))
+Path× {u} {A} {B} (a0 , b0) (a1 , b1) =
   isoToPath (iso fun (inv a0 a1 b0 b1) rightInv leftInv) where
 
   fun : {x y : A × B} → x ≡ y → (fst x ≡ fst y) × (snd x ≡ snd y)

0Trinitarianism/Quest5Solutions.agda

@@ -1,11 +1,6 @@
 module 0Trinitarianism.Quest5Solutions where
 
-open import Cubical.Foundations.Prelude renaming (subst to endPt ; transport to pathToFun)
-open import Cubical.HITs.S1 using ( S¹ ; base ; loop )
-open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
-open import Cubical.Foundations.Path renaming (PathPIsoPath to PathPIsoPathD)
-open import 1FundamentalGroup.Quest0Solutions
-open import Cubical.Data.Bool
+open import 0Trinitarianism.Preambles.P5
 
 PathD : {A0 A1 : Type} (A : A0 ≡ A1) (x : A0) (y : A1) → Type
 PathD A x y = pathToFun A x ≡ y
@@ -16,7 +11,7 @@ outOfS¹P : (B : S¹ → Type) (b : B base) → PathP (λ i → B (loop i)) b b
 outOfS¹P B b p base = b
 outOfS¹P B b p (loop i) = p i
 
-outOfS¹D : (B : S¹ → Type) (b : B base) → b ≡ b along (λ i → B (loop i)) → (x : S¹) → B x
+outOfS¹D : (B : S¹ → Type) (b : B base) → PathD (λ i → B (loop i)) b b → (x : S¹) → B x
 outOfS¹D B b p x = outOfS¹P B b (_≅_.inv (PathPIsoPathD (λ i → B (loop i)) b b) p) x
 
 example : (x : S¹) → doubleCover x → doubleCover x
@@ -42,3 +37,29 @@ example' = outOfS¹D (λ x → doubleCover x → doubleCover x) Flip (funExt lem
 outOfS¹DBase : (B : S¹ → Type) (b : B base)
   (p : b ≡ b along (λ i → B (loop i)))→ outOfS¹D B b p base ≡ b
 outOfS¹DBase B b p = refl
+
+pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
+  pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
+pathToFun→ {A0} {A1} {B0} {B1} {A} {B} f =
+  J (λ A1 A → pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1)))
+  (
+    J (λ B1 B → pathToFun (λ i → A0 → B i) f ≡ λ a → pathToFun B (f (pathToFun (sym refl) a)))
+    (
+        pathToFun refl f
+      ≡⟨ pathToFunReflx f ⟩
+        f
+      ≡⟨ funExt (λ a →
+           f a
+         ≡⟨ cong f (sym (pathToFunReflx a)) ⟩
+           f (pathToFun refl a)
+         ≡⟨ cong (λ p → f (pathToFun p a)) (sym symRefl) ⟩
+           f (pathToFun (sym refl) a)
+         ≡⟨ sym (pathToFunReflx (f (pathToFun (sym refl) a))) ⟩
+           pathToFun refl (f (pathToFun (sym refl) a)) ∎
+      )
+      ⟩
+        (λ a → pathToFun refl (f (pathToFun (sym refl) a))) ∎
+    )
+    B
+  )
+  A

1FundamentalGroup/Preambles/P3.agda

@@ -4,17 +4,30 @@ open import Cubical.Foundations.Prelude public
   renaming (transport to pathToFun ;
             transportRefl to pathToFunRefl ;
             subst to endPt) public
-open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
 open import Cubical.Foundations.GroupoidLaws
   renaming (lCancel to sym∙ ; rCancel to ∙sym ; lUnit to Refl∙ ; rUnit to ∙Refl) public
 open import Cubical.Foundations.Path public
 open import Cubical.Data.Int using (ℤ ; isSetℤ) public
 open import Cubical.Data.Nat public
 open import Cubical.HITs.S1 using ( S¹ ; base ; loop ) public
-open import 0Trinitarianism.Quest5Solutions public
 open import 1FundamentalGroup.Quest1Solutions public
 
 open ℤ public
 
+PathD : {A0 A1 : Type} (A : A0 ≡ A1) (x : A0) (y : A1) → Type
+PathD A x y = pathToFun A x ≡ y
+
 endPtRefl : {A : Type} {x : A} (B : A → Type) → endPt B (refl {x = x}) ≡ λ b → b
 endPtRefl {x = x} B = funExt (λ b → substRefl {B = B} b)
+
+outOfS¹P : (B : S¹ → Type) (b : B base) → PathP (λ i → B (loop i)) b b → (x : S¹) → B x
+outOfS¹P B b p base = b
+outOfS¹P B b p (loop i) = p i
+
+outOfS¹D : (B : S¹ → Type) (b : B base) → PathD (λ i → B (loop i)) b b → (x : S¹) → B x
+outOfS¹D B b p x = outOfS¹P B b (_≅_.inv (PathPIsoPath (λ i → B (loop i)) b b) p) x
+
+outOfS¹DBase : (B : S¹ → Type) (b : B base)
+  (p : PathD (λ i → B (loop i)) b b) → outOfS¹D B b p base ≡ b
+outOfS¹DBase B b p = refl

1FundamentalGroup/Quest3Solutions.agda

@@ -30,11 +30,6 @@ pathToFunPathFibration {A} {x} {y} q = J (λ z p → pathToFun (λ i → x ≡ p
     q ∙ refl ∎
   )
 
-pathToFun→ : {A0 A1 B0 B1 : Type} (A : A0 ≡ A1) (B : B0 ≡ B1) (f : A0 → B0) →
-  pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
-pathToFun→ A B f = refl
-
-
 rewind : (x : S¹) → helix x → base ≡ x
 rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
   (