added Iso symbol and edits on trinitarianis/quest3

0Trinitarianism/Quest3.agda

@@ -5,5 +5,7 @@ open import 0Trinitarianism.Preambles.P3
 _+_ : ℕ → ℕ → ℕ
 n + m = {!!}
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
-SumOfEven x y = {!!}
+{-
+Write here you proof that the sum of
+even naturals is even.
+-}

0Trinitarianism/Quest3Solutions.agda

@@ -10,13 +10,13 @@ _+'_ : ℕ → ℕ → ℕ
 zero +' n = n
 suc m +' n = suc (m +' n)
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
+SumOfEven : (x y : Σ ℕ isEven) → isEven (x .fst + y .fst)
 SumOfEven x (zero , hy) = x .snd
 SumOfEven x (suc (suc y) , hy) = SumOfEven x (y , hy)
 
 {-
 
-Sum'OfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst +' y .fst)
+Sum'OfEven : (x y : Σ ℕ isEven) → isEven (x .fst +' y .fst)
 Sum'OfEven x (zero , hy) = x .snd
 Sum'OfEven x (suc (suc y) , hy) = Sum'OfEven x (y , hy)
 

1FundamentalGroup/Preambles/P2.agda

@@ -2,7 +2,7 @@ module 1FundamentalGroup.Preambles.P2 where
 
 open import Cubical.Data.Nat public
 open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public
-open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
 open import Cubical.Foundations.Prelude renaming (subst to endPt) public
 open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
 open import 1FundamentalGroup.Quest1Solutions public

1FundamentalGroup/Quest2Solutions.agda

@@ -12,7 +12,7 @@ predℤ (pos zero) = negsuc zero
 predℤ (pos (suc n)) = pos n
 predℤ (negsuc n) = negsuc (suc n)
 
-sucℤIso : Iso ℤ ℤ
+sucℤIso : ℤ ≅ ℤ
 sucℤIso = iso sucℤ predℤ s r where
 
   s : section sucℤ predℤ