Merge branch 'newM'

Cubical/Data/Bool/Properties.agda

@@ -14,14 +14,14 @@ open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Pointed
 
-open import Cubical.Data.Sum
+open import Cubical.Data.Sum hiding (elim)
 open import Cubical.Data.Bool.Base
-open import Cubical.Data.Empty
-open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Empty hiding (elim)
+open import Cubical.Data.Empty as Empty hiding (elim)
 open import Cubical.Data.Sigma
 open import Cubical.Data.Unit using (Unit; isPropUnit)
 
-open import Cubical.HITs.PropositionalTruncation hiding (rec)
+open import Cubical.HITs.PropositionalTruncation hiding (elim; rec)
 
 open import Cubical.Relation.Nullary
 
@@ -30,6 +30,13 @@ private
     ℓ : Level
     A : Type ℓ
 
+elim : ∀ {ℓ} {A : Bool → Type ℓ}
+  → A true
+  → A false
+  → (b : Bool) → A b
+elim t f false = f
+elim t f true  = t
+
 notnot : ∀ x → not (not x) ≡ x
 notnot true  = refl
 notnot false = refl

Cubical/Foundations/Equiv/Dependent.agda

@@ -16,6 +16,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.HalfAdjoint
+open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Transport
 
@@ -54,6 +55,11 @@ isEquivOver :
   → Type _
 isEquivOver {A = A} F = (a : A) → isEquiv (F a)
 
+isPropIsEquivOver :
+  {f : A → B}
+  (F : mapOver f P Q)
+  → isProp (isEquivOver {Q = Q} F)
+isPropIsEquivOver F = isPropΠ (λ a → isPropIsEquiv (F a))
 
 -- Relative version of section and retract
 
@@ -122,6 +128,11 @@ IsoOver→isIsoOver isom .inv = isom .inv
 IsoOver→isIsoOver isom .rightInv = isom .rightInv
 IsoOver→isIsoOver isom .leftInv  = isom .leftInv
 
+invIsoOver : {isom : Iso A B} → IsoOver isom P Q → IsoOver (invIso isom) Q P
+invIsoOver {isom = isom} isom' .fun = isom' .inv
+invIsoOver {isom = isom} isom' .inv = isom' .fun
+invIsoOver {isom = isom} isom' .rightInv = isom' .leftInv
+invIsoOver {isom = isom} isom' .leftInv = isom' .rightInv
 
 compIsoOver :
   {ℓA ℓB ℓC ℓP ℓQ ℓR : Level}

Cubical/Foundations/Equiv/PathSplit.agda

@@ -93,8 +93,8 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
   PathSplitEquiv is a proposition and the type
   of path split equivs is equivalent to the type of equivalences
 -}
-isPropIsPathSplitEquiv : ∀ {ℓ} {A B : Type ℓ} (f : A → B) → isProp (isPathSplitEquiv f)
-isPropIsPathSplitEquiv {_} {A} {B} f
+isPropIsPathSplitEquiv : ∀ {ℓ} {ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → isProp (isPathSplitEquiv f)
+isPropIsPathSplitEquiv {A = A} {B = B} f
   record { sec = sec-φ ; secCong = secCong-φ }
   record { sec = sec-ψ ; secCong = secCong-ψ } i
   =

Cubical/HITs/RPn/Base.agda

@@ -22,7 +22,7 @@ open import Cubical.Foundations.SIP
 open import Cubical.Structures.Pointed
 open import Cubical.Structures.TypeEqvTo
 
-open import Cubical.Data.Bool
+open import Cubical.Data.Bool hiding (elim)
 open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.NatMinusOne
 open import Cubical.Data.Sigma

Cubical/HITs/Sn/Properties.agda

@@ -21,7 +21,7 @@ open import Cubical.HITs.Susp renaming (toSusp to σ)
 open import Cubical.HITs.Truncation
 open import Cubical.Homotopy.Connected
 open import Cubical.HITs.Join renaming (joinS¹S¹→S³ to joinS¹S¹→S3)
-open import Cubical.Data.Bool
+open import Cubical.Data.Bool hiding (elim)
 
 private
   variable

Cubical/HITs/Truncation/Properties.agda

@@ -20,7 +20,7 @@ open Modality
 
 open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.Sigma
-open import Cubical.Data.Bool
+open import Cubical.Data.Bool hiding (elim)
 open import Cubical.Data.Unit
 open import Cubical.HITs.Sn.Base
 open import Cubical.HITs.S1 hiding (rec ; elim)

Cubical/Homotopy/Connected.agda

@@ -14,6 +14,7 @@ open import Cubical.Foundations.Path
 open import Cubical.Foundations.Univalence
 
 open import Cubical.Functions.Fibration
+open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Data.Unit
 open import Cubical.Data.Bool
@@ -24,6 +25,7 @@ open import Cubical.HITs.Nullification
 open import Cubical.HITs.Susp
 open import Cubical.HITs.SmashProduct
 open import Cubical.HITs.Pushout
+open import Cubical.HITs.Join
 open import Cubical.HITs.Sn.Base
 open import Cubical.HITs.S1
 open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec)
@@ -691,6 +693,89 @@ isConnectedPushout→ f₁ f₂ g₁ g₂ h₀ h₁ h₂ e₁ e₂ n con₀ con
                       ; (j = i1) → transport refl (F (push a i))})
               (btm i j)
 
+
+module _ {ℓ' ℓ'' : Level}
+  (m n : HLevel) {A : Type ℓ} {A' : Type ℓ'} {v : A → A'} {B : Type ℓ''}
+  (hA : isConnectedFun m v) (hB : isConnected n B) where
+
+  private module _ {ℓ''' : Level} (P : join A' B → TypeOfHLevel ℓ''' (m + n)) where
+    module _ (k : (x : join A B) → P (join→ v (idfun B) x) .fst) where
+      -- We encode k as a section f of the family
+      --   A
+      -- v ↓  X
+      --   A' → Type
+      -- over A, and use the connectivity assumption on v
+      -- to extend it to a section f' over A'.
+
+      X : A' → Type _
+      X a' =
+        Σ[ x ∈ P (inl a') .fst ]
+          ∀ (b : B) → PathP (λ i → P (push a' b i) .fst) x (k (inr b))
+
+      f : (a : A) → X (v a)
+      fst (f a) = k (inl a)
+      snd (f a) = λ b i → k (push a b i)
+
+      -- Equivalent type to X, whose h-level we can estimate.
+      X' : A' → Type _
+      X' a' =
+        Σ[ x' ∈ (Unit → P (inl a') .fst) ]
+          (λ (b : B) → x' tt) ≡
+          (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b)))
+
+      X≃X' : (a' : A') → X a' ≃ X' a'
+      X≃X' a' =
+        (Σ[ x ∈ P (inl a') .fst ]
+          ∀ (b : B) → PathP (λ i → P (push a' b i) .fst) x (k (inr b)))
+        ≃⟨ invEquiv (Σ-cong-equiv-fst (UnitToType≃ _)) ⟩
+        (Σ[ x' ∈ (Unit → P (inl a') .fst) ]
+          ∀ (b : B) → PathP (λ i → P (push a' b i) .fst) (x' tt) (k (inr b)))
+        ≃⟨ Σ-cong-equiv-snd (λ x' → equivΠCod (λ b → pathToEquiv (PathP≡Path⁻ _ _ _))) ⟩
+        (Σ[ x' ∈ (Unit → P (inl a') .fst) ]
+          ∀ (b : B) → x' tt ≡ subst⁻ (λ y → P y .fst) (push a' b) (k (inr b)))
+        ≃⟨ Σ-cong-equiv-snd (λ x' → funExtEquiv) ⟩
+        (Σ[ x' ∈ (Unit → P (inl a') .fst) ]
+          (λ (b : B) → x' tt) ≡
+          (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b))))
+        ■
+
+      X'level : (a' : A') → isOfHLevel m (X' a')
+      X'level a' =
+        isOfHLevelPrecomposeConnected m n
+          (λ (_ : Unit) → P (inl a')) (λ (b : B) → tt)
+          (λ _ → isConnectedRetractFromIso _ fiberUnitIso hB) _
+
+      Xl : (a' : A') → TypeOfHLevel _ m
+      fst (Xl a') = X a'
+      snd (Xl a') = isOfHLevelRespectEquiv _ (invEquiv (X≃X' a')) (X'level a')
+
+      H : Iso ((a' : A') → X a') ((a : A) → X (v a))
+      H = elim.isIsoPrecompose v _ Xl hA
+
+      f' : (a' : A') → X a'
+      f' = Iso.inv H f
+
+      hf' : (a : A) → f' (v a) ≡ f a
+      hf' = funExt⁻ (Iso.rightInv H f)
+
+      k' : (x : join A' B) → P x .fst
+      k' (inl a') = f' a' .fst
+      k' (inr b) = k (inr b)
+      k' (push a' b i) = f' a' .snd b i
+
+      hk' : (x : join A B) → k' (join→ v (idfun B) x) ≡ k x
+      hk' (inl a) j = hf' a j .fst
+      hk' (inr b) j = k (inr b)
+      hk' (push a b i) j = hf' a j .snd b i
+
+    joinConnectedAux :
+      hasSection (λ (k : (x : join A' B) → P x .fst) → k ∘ join→ v (idfun B))
+    fst joinConnectedAux k = k' k
+    snd joinConnectedAux k = funExt (hk' k)
+
+  joinConnected : isConnectedFun (m + n) (join→ v (idfun B))
+  joinConnected = elim.isConnectedPrecompose _ _ joinConnectedAux
+
 {- Given two fibration B , C : A → Type and a family of maps on fibres
    f : (a : A) → B a → C a, we have that f a is n-connected for all (a : A)
    iff the induced map on totalspaces Σ A B → Σ A C is n-connected -}

Cubical/Homotopy/HopfInvariant/Homomorphism.agda

@@ -693,7 +693,7 @@ jᵣ-βₗ n f g =
   cong (coHomFun _ (jᵣ n f g)) (βₗ≡ n f g)
   ∙∙ natTranspLem ∣ βₗ'-fun n f g ∣₂ (λ m → coHomFun m (jᵣ n f g))
             (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
-  ∙∙ cong (subst (λ m → coHom m (HopfInvariantPush n (fst f)))
+  ∙∙ cong (subst (λ m → coHom m (HopfInvariantPush n (fst g)))
       (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
       cool
   where
@@ -795,7 +795,7 @@ isHom-HopfInvariant n f g =
 
   eq₃ : Hopfα n g ⌣ Hopfα n g
       ≡ (Y n f g ℤ[ coHomGr _ _ ]·
-                   subst (λ m → coHom m (HopfInvariantPush n (fst f)))
+                   subst (λ m → coHom m (HopfInvariantPush n (fst g)))
                    (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
                    (Hopfβ n g))
   eq₃ = cong (λ x → x ⌣ x) (sym (jᵣ-α n f g))

Cubical/Papers/AffineSchemes.agda

@@ -5,11 +5,11 @@ Please do not move this file. Changes should only be made if necessary.
 This file contains pointers to the code examples and main results from
 the paper:
 
-A Univalent Formalization of Affine Schemes
+A Univalent Formalization of Constructive Affine Schemes
 
-Anders Mörtberg, Max Zeuner
+Max Zeuner, Anders Mörtberg
 
-Preprint: !!! arXiv link !!!
+Preprint: https://arxiv.org/abs/2212.02902
 
 
 -}