text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Base where

open import Cubical.Homotopy.Loopspace

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport

open import Cubical.Functions.Morphism

open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; rec2 to sRec2
          ; elim to sElim ; elim2 to sElim2 ; elim3 to sElim3
          ; map to sMap)
open import Cubical.HITs.Truncation
  renaming (rec to trRec ; elim to trElim ; elim2 to trElim2)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.S1

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Unit

open import Cubical.Algebra.Group
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid

open Iso
open IsGroup
open IsSemigroup
open IsMonoid
open GroupStr

{- Homotopy group -}
π : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Type ℓ
π n A = ∥ typ ((Ω^ n) A) ∥₂

{- Alternative formulation. This will be given a group structure in
  the Properties file -}
π' : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Type ℓ
π' n A = ∥ S₊∙ n →∙ A ∥₂

{- π as a group -}
1π : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π n A
1π zero {A = A} = ∣ pt A ∣₂
1π (suc n) = ∣ refl ∣₂

·π : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π (suc n) A → π (suc n) A → π (suc n) A
·π n = sRec2 squash₂ λ p q → ∣ p ∙ q ∣₂

-π : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π (suc n) A → π (suc n) A
-π n = sMap sym

π-rUnit : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π (suc n) A)
        → (·π n x (1π (suc n))) ≡ x
π-rUnit n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ rUnit p (~ i) ∣₂

π-lUnit : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π (suc n) A)
        → (·π n (1π (suc n)) x) ≡ x
π-lUnit n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ lUnit p (~ i) ∣₂

π-rCancel : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π (suc n) A)
        → (·π n x (-π n x)) ≡ 1π (suc n)
π-rCancel n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ rCancel p i ∣₂

π-lCancel : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π (suc n) A)
        → (·π n (-π n x) x) ≡ 1π (suc n)
π-lCancel n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ lCancel p i ∣₂

π-assoc : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x y z : π (suc n) A)
        → ·π n x (·π n y z) ≡ ·π n (·π n x y) z
π-assoc n = sElim3 (λ _ _ _ → isSetPathImplicit) λ p q r i → ∣ ∙assoc p q r i ∣₂

π-comm : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x y : π (suc (suc n)) A)
        → ·π (suc n) x y ≡ ·π (suc n) y x
π-comm n = sElim2 (λ _ _ → isSetPathImplicit) λ p q i → ∣ EH n p q i ∣₂

-- πₙ₊₁
πGr : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Group ℓ
fst (πGr n A) = π (suc n) A
1g (snd (πGr n A)) = 1π (suc n)
GroupStr._·_ (snd (πGr n A)) = ·π n
inv (snd (πGr n A)) = -π n
is-set (isSemigroup (isMonoid (isGroup (snd (πGr n A))))) = squash₂
assoc (isSemigroup (isMonoid (isGroup (snd (πGr n A))))) = π-assoc n
identity (isMonoid (isGroup (snd (πGr n A)))) x = (π-rUnit n x) , (π-lUnit n x)
inverse (isGroup (snd (πGr n A))) x = (π-rCancel n x) , (π-lCancel n x)

-- Group operations on π'.
-- We define the corresponding structure on the untruncated
-- (S₊∙ n →∙ A).

∙Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
  → (S₊∙ n →∙ A)
  → (S₊∙ n →∙ A)
  → (S₊∙ n →∙ A)
∙Π {A = A} {n = zero} p q = (λ _ → pt A) , refl
fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) base = pt A
fst (∙Π {A = A} {n = suc zero} (f , p) (g , q)) (loop j) =
  ((sym p ∙∙ cong f loop ∙∙ p) ∙ (sym q ∙∙ cong g loop ∙∙ q)) j
snd (∙Π {A = A} {n = suc zero} (f , p) (g , q)) = refl
fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) north = pt A
fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) south = pt A
fst (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) (merid a j) =
   ((sym p ∙∙ cong f (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ p)
  ∙ (sym q ∙∙ cong g (merid a ∙ sym (merid (ptSn (suc n)))) ∙∙ q)) j
snd (∙Π {A = A} {n = suc (suc n)} (f , p) (g , q)) = refl

-Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
  → (S₊∙ n →∙ A)
  → (S₊∙ n →∙ A)
-Π {n = zero} f = f
fst (-Π {A = A} {n = suc zero} f) base = fst f base
fst (-Π {A = A} {n = suc zero} f) (loop j) = fst f (loop (~ j))
snd (-Π {A = A} {n = suc zero} f) = snd f
fst (-Π {A = A} {n = suc (suc n)} f) north = fst f north
fst (-Π {A = A} {n = suc (suc n)} f) south = fst f north
fst (-Π {A = A} {n = suc (suc n)} f) (merid a j) =
 fst f ((merid a ∙ sym (merid (ptSn _))) (~ j))
snd (-Π {A = A} {n = suc (suc n)} f) = snd f

-- to prove that this gives a group structure on π', we first
-- prove that Ωⁿ A ≃ (Sⁿ →∙ A).
-- We use the following map
mutual
  Ω→SphereMap : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ}
   → typ ((Ω^ n) A) → (S₊∙ n →∙ A)
  fst (Ω→SphereMap zero a) false = a
  fst (Ω→SphereMap zero {A = A} a) true = pt A
  snd (Ω→SphereMap zero a) = refl
  fst (Ω→SphereMap (suc zero) {A = A} p) base = pt A
  fst (Ω→SphereMap (suc zero) p) (loop i) = p i
  snd (Ω→SphereMap (suc zero) p) = refl
  fst (Ω→SphereMap (suc (suc n)) {A = A} p) north = pt A
  fst (Ω→SphereMap (suc (suc n)) {A = A} p) south = pt A
  fst (Ω→SphereMap (suc (suc n)) p) (merid a i) =
    (sym (Ω→SphereMapId (suc n) a)
    ∙∙ (λ i → Ω→SphereMap (suc n) (p i) .fst a)
    ∙∙ Ω→SphereMapId (suc n) a) i
  snd (Ω→SphereMap (suc (suc n)) p) = refl

  Ω→SphereMapId : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (a : _)
    → Ω→SphereMap n {A = A} (pt ((Ω^ n) A)) .fst a ≡ pt A
  Ω→SphereMapId zero false = refl
  Ω→SphereMapId zero true = refl
  Ω→SphereMapId (suc zero) base = refl
  Ω→SphereMapId (suc zero) (loop i) = refl
  Ω→SphereMapId (suc (suc n)) north = refl
  Ω→SphereMapId (suc (suc n)) south = refl
  Ω→SphereMapId (suc (suc n)) {A = A} (merid a i) j =
    ∙∙lCancel (Ω→SphereMapId (suc n) {A = A} a) j i

Ω→SphereMapId2 : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ}
  → Ω→SphereMap n {A = A} (pt ((Ω^ n) A)) ≡ ((λ _ → pt A) , refl)
fst (Ω→SphereMapId2 n {A = A} i) a = funExt (Ω→SphereMapId n {A = A}) i a
snd (Ω→SphereMapId2 zero {A = A} i) = refl
snd (Ω→SphereMapId2 (suc zero) {A = A} i) = refl
snd (Ω→SphereMapId2 (suc (suc n)) {A = A} i) = refl

-- Pointed version
Ω→SphereMap∙ : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ}
  → ((Ω^ n) A) →∙ (S₊∙ n →∙ A ∙)
Ω→SphereMap∙ n .fst = Ω→SphereMap n
Ω→SphereMap∙ n .snd = Ω→SphereMapId2 n

-- We define the following maps which will be used to
-- show that Ω→SphereMap is an equivalence
Ω→SphereMapSplit₁ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
           → typ ((Ω^ (suc n)) A)
           → typ (Ω (S₊∙ n →∙ A ∙))
Ω→SphereMapSplit₁ n = Ω→ (Ω→SphereMap∙ n) .fst

ΩSphereMap : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → typ (Ω (S₊∙ n →∙ A ∙))
  → (S₊∙ (suc n) →∙ A)
fst (ΩSphereMap {A = A} zero p) base = p i0 .fst false
fst (ΩSphereMap {A = A} zero p) (loop i) = p i .fst false
snd (ΩSphereMap {A = A} zero p) = refl
ΩSphereMap {A = A} (suc n) = fun IsoΩFunSuspFun

-- Functoriality
-- The homogeneity assumption is not necessary but simplifying
isNaturalΩSphereMap : ∀ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ')
  (homogB : isHomogeneous B) (f : A →∙ B) (n : ℕ)
  → ∀ g → f ∘∙ ΩSphereMap n g ≡ ΩSphereMap n (Ω→ (post∘∙ (S₊∙ n) f) .fst g)
isNaturalΩSphereMap A B homogB f 0 g =
  →∙Homogeneous≡ homogB (funExt lem)
  where
  lem : ∀ x → f .fst (ΩSphereMap 0 g .fst x)
            ≡ ΩSphereMap 0 (Ω→ (post∘∙ (S₊∙ 0) f) .fst g) .fst x
  lem base = f .snd
  lem (loop i) j =
    hfill
      (λ j → λ
        { (i = i0) → post∘∙ _ f .snd j
        ; (i = i1) → post∘∙ _ f .snd j
        })
      (inS (f ∘∙ g i))
      j .fst false
isNaturalΩSphereMap A B homogB f (n@(suc _)) g =
  →∙Homogeneous≡ homogB (funExt lem)
  where
  lem : ∀ x → f .fst (ΩSphereMap n g .fst x)
            ≡ ΩSphereMap n (Ω→ (post∘∙ (S₊∙ n) f) .fst g) .fst x
  lem north = f .snd
  lem south = f .snd
  lem (merid a i) j =
    hfill
      (λ j → λ
        { (i = i0) → post∘∙ _ f .snd j
        ; (i = i1) → post∘∙ _ f .snd j
        })
      (inS (f ∘∙ g i))
      j .fst a

SphereMapΩ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → (S₊∙ (suc n) →∙ A)
  → typ (Ω (S₊∙ n →∙ A ∙))
SphereMapΩ {A = A} zero (f , p) =
  ΣPathP ((funExt λ { false → sym p ∙∙ cong f loop ∙∙ p
                    ; true → refl})
          , refl)
SphereMapΩ {A = A} (suc n) = inv IsoΩFunSuspFun

SphereMapΩIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → Iso (S₊∙ (suc n) →∙ A)
         (typ (Ω (S₊∙ n →∙ A ∙)))
fun (SphereMapΩIso n) = SphereMapΩ n
inv (SphereMapΩIso n) = ΩSphereMap n
fst (rightInv (SphereMapΩIso zero) f i j) false = rUnit (λ j → fst (f j) false) (~ i) j
fst (rightInv (SphereMapΩIso {A = A} zero) f i j) true = snd (f j) (~ i)
snd (rightInv (SphereMapΩIso {A = A} zero) f i j) k = snd (f j) (~ i ∨ k)
rightInv (SphereMapΩIso (suc n)) = leftInv IsoΩFunSuspFun
leftInv (SphereMapΩIso zero) f =
  ΣPathP ((funExt (λ { base → sym (snd f)
                    ; (loop i) j → doubleCompPath-filler
                                     (sym (snd f))
                                     (cong (fst f) loop)
                                     (snd f) (~ j) i}))
        , λ i j → snd f (~ i ∨ j))
leftInv (SphereMapΩIso (suc n)) = rightInv IsoΩFunSuspFun

{-
In order to show that Ω→SphereMap is an equivalence, we show that it factors

             Ω→SphereMapSplit₁               ΩSphereMap
Ωⁿ⁺¹(Sⁿ →∙ A) ----------------> Ω (Sⁿ →∙ A) -----------> (Sⁿ⁺¹ →∙ A)
-}

Ω→SphereMap-split : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p : typ ((Ω^ (suc n)) A))
    → Ω→SphereMap (suc n) p ≡ ΩSphereMap n (Ω→SphereMapSplit₁ n p)
Ω→SphereMap-split {A = A} zero p =
  ΣPathP ((funExt (λ { base → refl
                     ; (loop i) j → lem (~ j) i}))
         , refl)
  where
  lem : funExt⁻ (cong fst (Ω→SphereMapSplit₁ zero p)) false ≡ p
  lem = (λ i → funExt⁻ (cong-∙∙ fst (sym (Ω→SphereMapId2 zero))
                                     (cong (Ω→SphereMap zero) p)
                                     (Ω→SphereMapId2 zero) i) false)
    ∙ sym (rUnit _)
Ω→SphereMap-split {A = A} (suc n) p =
  ΣPathP ((funExt (λ { north → refl
                     ; south → refl
                     ; (merid a i) j → lem₂ a j i}))
          , refl)
  where
  lem : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (a : S₊ (suc n))
    → Ω→SphereMapId (suc n) {A = A} a
    ≡ (λ i → fst (Ω→SphereMapId2 (suc n) {A = A} i) a)
  lem zero base = refl
  lem zero (loop i) = refl
  lem (suc n) north = refl
  lem (suc n) south = refl
  lem (suc n) (merid a i) = refl

  lem₂ : (a : S₊ (suc n))
     → ((λ i₁ → Ω→SphereMapId (suc n) {A = A} a (~ i₁))
     ∙∙ (λ i₁ → Ω→SphereMap (suc n) (p i₁) .fst a)
     ∙∙ Ω→SphereMapId (suc n) a)
     ≡ (λ i → Ω→SphereMapSplit₁ (suc n) p i .fst a)
  lem₂ a = cong (λ x → sym x
                 ∙∙ funExt⁻ (cong fst (λ i → Ω→SphereMap (suc n) (p i))) a
                 ∙∙ x)
             (lem n a)
     ∙∙ sym (cong-∙∙ (λ x → x a)
              (cong fst (λ i → Ω→SphereMapId2 (suc n) (~ i)))
              (cong fst (λ i → Ω→SphereMap (suc n) (p i)))
              (cong fst (Ω→SphereMapId2 (suc n))))
     ∙∙ (λ i → funExt⁻ (cong-∙∙ fst (sym (Ω→SphereMapId2 (suc n)))
                          (cong (Ω→SphereMap (suc n)) p)
                          (Ω→SphereMapId2 (suc n)) (~ i)) a)

isEquiv-Ω→SphereMap₀ : ∀ {ℓ} {A : Pointed ℓ}
  → isEquiv (Ω→SphereMap 0 {A = A})
isEquiv-Ω→SphereMap₀ {A = A} =
  isoToIsEquiv
    (iso _ (λ f → fst f false)
         (λ f → ΣPathP ((funExt (λ { false → refl ; true → sym (snd f)}))
                       , λ i j → snd f (~ i ∨ j)))
         λ p → refl)

isEquiv-Ω→SphereMap : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ}
  → isEquiv (Ω→SphereMap n {A = A})
isEquiv-Ω→SphereMap zero {A = A} =
  (isoToIsEquiv
    (iso _ (λ f → fst f false)
           (λ f → ΣPathP ((funExt (λ { false → refl
                                      ; true → sym (snd f)}))
                          , λ i j → snd f (~ i ∨ j)))
            λ _ → refl))
isEquiv-Ω→SphereMap (suc zero) {A = A} =
  isoToIsEquiv (iso _ invFun sec λ p → sym (rUnit p))
  where
  invFun : S₊∙ 1 →∙ A → typ (Ω A)
  invFun (f , p) = sym p ∙∙ cong f loop ∙∙ p

  sec : section (Ω→SphereMap 1) invFun
  sec (f , p) =
    ΣPathP ((funExt (λ { base → sym p
                       ; (loop i) j → doubleCompPath-filler
                                        (sym p) (cong f loop) p (~ j) i}))
           , λ i j → p (~ i ∨ j))

isEquiv-Ω→SphereMap (suc (suc n)) =
  subst isEquiv (sym (funExt (Ω→SphereMap-split (suc n))))
    (snd (compEquiv
         ((Ω→SphereMapSplit₁ (suc n)) ,
              (isEquivΩ→ (Ω→SphereMap (suc n) , Ω→SphereMapId2 (suc n))
                           (isEquiv-Ω→SphereMap (suc n))))
         (invEquiv (isoToEquiv (SphereMapΩIso (suc n))))))

IsoΩSphereMap : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → Iso (typ ((Ω^ n) A)) (S₊∙ n →∙ A)
IsoΩSphereMap n = equivToIso (_ , isEquiv-Ω→SphereMap n)

IsoSphereMapΩ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
     → Iso (S₊∙ n →∙ A) (fst ((Ω^ n) A))
IsoSphereMapΩ {A = A} n =
  invIso (IsoΩSphereMap n)

SphereMap→Ω : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
      → S₊∙ n →∙ A → fst ((Ω^ n) A)
SphereMap→Ω n = fun (IsoSphereMapΩ n)

isHom-Ω→SphereMap : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (p q : _)
  → Ω→SphereMap (suc n) {A = A} (p ∙ q)
  ≡ ∙Π (Ω→SphereMap (suc n) {A = A} p)
       (Ω→SphereMap (suc n) {A = A} q)
isHom-Ω→SphereMap zero {A = A} p q =
  ΣPathP ((funExt (λ { base → refl
                    ; (loop i) j → (rUnit p j ∙ rUnit q j) i}))
        , refl)
isHom-Ω→SphereMap (suc n) {A = A} p q =
  ΣPathP ((funExt (λ { north → refl
                     ; south → refl
                     ; (merid a i) j → main a j i}))
        , refl)
  where
  doubleComp-lem : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) (q r : y ≡ y)
                 → (p ∙∙ q ∙∙ sym p) ∙ (p ∙∙ r ∙∙ sym p)
                  ≡ (p ∙∙ (q ∙ r) ∙∙ sym p)
  doubleComp-lem p q r i j =
    hcomp (λ k → λ { (i = i0) → (doubleCompPath-filler p q (sym p) k
                                ∙ doubleCompPath-filler p r (sym p) k) j
                    ; (i = i1) → doubleCompPath-filler p (q ∙ r) (sym p) k j
                    ; (j = i0) → p (~ k)
                    ; (j = i1) → p (~ k)})
          ((q ∙ r) j)

  lem : (p : typ ((Ω^ (suc (suc n))) A))
      → cong (fst (Ω→SphereMap (suc (suc n)) p)) (merid (ptSn _)) ≡ refl
  lem p =
    cong (sym (Ω→SphereMapId (suc n) (ptSn _)) ∙∙_∙∙ Ω→SphereMapId (suc n) (ptSn _))
              (rUnit _ ∙ (λ j → (λ i → Ω→SphereMap (suc n) {A = A} refl .snd (i ∧ j))
                       ∙∙ (λ i → Ω→SphereMap (suc n) {A = A} (p i) .snd j)
                       ∙∙ λ i → Ω→SphereMap (suc n) {A = A} refl .snd (~ i ∧ j))
                       ∙ ∙∙lCancel _)
              ∙ ∙∙lCancel _

  main : (a : S₊ (suc n))
    → sym (Ω→SphereMapId (suc n) a)
        ∙∙ funExt⁻ (cong fst (cong (Ω→SphereMap (suc n)) (p ∙ q))) a
        ∙∙ Ω→SphereMapId (suc n) a
     ≡ cong (fst (∙Π (Ω→SphereMap (suc (suc n)) p) (Ω→SphereMap (suc (suc n)) q))) (merid a)
  main a = (cong (sym (Ω→SphereMapId (suc n) a) ∙∙_∙∙ (Ω→SphereMapId (suc n) a))
              (cong-∙ (λ x → Ω→SphereMap (suc n) x .fst a) p q)
       ∙ sym (doubleComp-lem (sym (Ω→SphereMapId (suc n) a)) _ _))
     ∙∙ cong₂ _∙_ (sym (cong (cong (fst (Ω→SphereMap (suc (suc n)) p)) (merid a) ∙_)
                       (cong sym (lem p)) ∙ sym (rUnit _)))
                  (sym (cong (cong (fst (Ω→SphereMap (suc (suc n)) q)) (merid a) ∙_)
                       (cong sym (lem q)) ∙ sym (rUnit _)))
     ∙∙ λ i → (rUnit (cong-∙ (fst (Ω→SphereMap (suc (suc n)) p))
                              (merid a) (sym (merid (ptSn _))) (~ i)) i)
             ∙ (rUnit (cong-∙ (fst (Ω→SphereMap (suc (suc n)) q))
                              (merid a) (sym (merid (ptSn _)))(~ i)) i)

-- The iso is structure preserving
IsoSphereMapΩ-pres∙Π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (f g : S₊∙ (suc n) →∙ A)
             → SphereMap→Ω (suc n) (∙Π f g)
              ≡ SphereMap→Ω (suc n) f ∙ SphereMap→Ω (suc n) g
IsoSphereMapΩ-pres∙Π n =
  morphLemmas.isMorphInv _∙_ ∙Π (Ω→SphereMap (suc n))
    (isHom-Ω→SphereMap n)
    (SphereMap→Ω (suc n))
    (leftInv (IsoSphereMapΩ (suc n)))
    (rightInv (IsoSphereMapΩ (suc n)))

-- It is useful to define the ``Group Structure'' on (S₊∙ n →∙ A)
-- before doing it on π'. These will be the equivalents of the
-- usual groupoid laws on Ω A.
1Π : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ} → (S₊∙ n →∙ A)
fst (1Π {A = A}) _ = pt A
snd (1Π {A = A}) = refl

∙Π-rUnit : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f : S₊∙ (suc n) →∙ A)
        → ∙Π f 1Π ≡ f
fst (∙Π-rUnit {A = A} {n = zero} f i) base = snd f (~ i)
fst (∙Π-rUnit {A = A} {n = zero} f i) (loop j) = help i j
  where
  help : PathP (λ i → snd f (~ i) ≡ snd f (~ i))
               (((sym (snd f)) ∙∙ (cong (fst f) loop) ∙∙ snd f)
                 ∙ (refl ∙ refl))
               (cong (fst f) loop)
  help = (cong ((sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f) ∙_)
               (sym (rUnit refl)) ∙ sym (rUnit _))
        ◁ λ i j → doubleCompPath-filler (sym (snd f))
                     (cong (fst f) loop) (snd f) (~ i) j
snd (∙Π-rUnit {A = A} {n = zero} f i) j = snd f (~ i ∨ j)
fst (∙Π-rUnit {A = A} {n = suc n} f i) north = snd f (~ i)
fst (∙Π-rUnit {A = A} {n = suc n} f i) south =
  (sym (snd f) ∙ cong (fst f) (merid (ptSn (suc n)))) i
fst (∙Π-rUnit {A = A} {n = suc n} f i) (merid a j) = help i j
  where
  help : PathP (λ i → snd f (~ i)
             ≡ (sym (snd f) ∙ cong (fst f) (merid (ptSn (suc n)))) i)
               (((sym (snd f))
                 ∙∙ (cong (fst f) (merid a ∙ sym (merid (ptSn (suc n)))))
                 ∙∙ snd f)
                 ∙ (refl ∙ refl))
               (cong (fst f) (merid a))
  help = (cong (((sym (snd f))
                ∙∙ (cong (fst f) (merid a ∙ sym (merid (ptSn (suc n)))))
                ∙∙ snd f) ∙_)
              (sym (rUnit refl))
       ∙ sym (rUnit _))
       ◁ λ i j → hcomp (λ k →
         λ { (j = i0) → snd f (~ i ∧ k)
            ; (j = i1) → compPath-filler' (sym (snd f))
                           (cong (fst f) (merid (ptSn (suc n)))) k i
            ; (i = i0) → doubleCompPath-filler (sym (snd f))
                            (cong (fst f)
                            (merid a ∙ sym (merid (ptSn (suc n)))))
                            (snd f) k j
            ; (i = i1) → fst f (merid a j)})
            (fst f (compPath-filler (merid a)
                      (sym (merid (ptSn _))) (~ i) j))
snd (∙Π-rUnit {A = A} {n = suc n} f i) j = snd f (~ i ∨ j)

∙Π-lUnit : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f : S₊∙ (suc n) →∙ A)
        → ∙Π 1Π f ≡ f
fst (∙Π-lUnit {n = zero} f i) base = snd f (~ i)
fst (∙Π-lUnit {n = zero} f i) (loop j) = s i j
  where
  s : PathP (λ i → snd f (~ i) ≡ snd f (~ i))
            ((refl ∙ refl) ∙ (sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f))
            (cong (fst f) loop)
  s = (cong (_∙ (sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f))
            (sym (rUnit refl)) ∙ sym (lUnit _))
          ◁ λ i j → doubleCompPath-filler (sym (snd f))
                      (cong (fst f) loop) (snd f) (~ i) j
snd (∙Π-lUnit {n = zero} f i) j = snd f (~ i ∨ j)
fst (∙Π-lUnit {n = suc n} f i) north = snd f (~ i)
fst (∙Π-lUnit {n = suc n} f i) south =
  (sym (snd f) ∙ cong (fst f) (merid (ptSn _))) i
fst (∙Π-lUnit {n = suc n} f i) (merid a j) = help i j
  where
  help : PathP (λ i → snd f (~ i)
             ≡ (sym (snd f) ∙ cong (fst f) (merid (ptSn (suc n)))) i)
               ((refl ∙ refl) ∙ ((sym (snd f))
                      ∙∙ (cong (fst f) (merid a ∙ sym (merid (ptSn (suc n)))))
                      ∙∙ snd f))
               (cong (fst f) (merid a))
  help =
    (cong (_∙ ((sym (snd f))
            ∙∙ (cong (fst f) (merid a ∙ sym (merid (ptSn (suc n)))))
            ∙∙ snd f))
           (sym (rUnit refl))
    ∙ sym (lUnit _))
    ◁ λ i j → hcomp (λ k →
      λ { (j = i0) → snd f (~ i ∧ k)
        ; (j = i1) → compPath-filler' (sym (snd f))
                       (cong (fst f) (merid (ptSn (suc n)))) k i
        ; (i = i0) → doubleCompPath-filler (sym (snd f))
                        (cong (fst f) (merid a ∙ sym (merid (ptSn (suc n)))))
                        (snd f) k j
        ; (i = i1) → fst f (merid a j)})
        (fst f (compPath-filler (merid a) (sym (merid (ptSn _))) (~ i) j))
snd (∙Π-lUnit {n = suc n} f i) j = snd f (~ i ∨ j)

∙Π-rCancel : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f : S₊∙ (suc n) →∙ A)
        → ∙Π f (-Π f) ≡ 1Π
fst (∙Π-rCancel {A = A} {n = zero} f i) base = pt A
fst (∙Π-rCancel {A = A} {n = zero} f i) (loop j) =
  rCancel (sym (snd f) ∙∙ cong (fst f) loop ∙∙ snd f) i j
snd (∙Π-rCancel {A = A} {n = zero} f i) = refl
fst (∙Π-rCancel {A = A} {n = suc n} f i) north = pt A
fst (∙Π-rCancel {A = A} {n = suc n} f i) south = pt A
fst (∙Π-rCancel {A = A} {n = suc n} f i) (merid a i₁) = lem i i₁
  where
  pl = (sym (snd f)
     ∙∙ cong (fst f) (merid a ∙ sym (merid (ptSn _)))
     ∙∙ snd f)

  lem : pl
     ∙ ((sym (snd f)
      ∙∙ cong (fst (-Π f)) (merid a ∙ sym (merid (ptSn _)))
      ∙∙ snd f)) ≡ refl
  lem = cong (pl ∙_) (cong (sym (snd f) ∙∙_∙∙ (snd f))
        (cong-∙ (fst (-Π f)) (merid a) (sym (merid (ptSn _)))
        ∙∙ cong₂ _∙_ refl
                   (cong (cong (fst f)) (rCancel (merid (ptSn _))))
        ∙∙ sym (rUnit _)))
     ∙ rCancel pl
snd (∙Π-rCancel {A = A} {n = suc n} f i) = refl

∙Π-lCancel : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f : S₊∙ (suc n) →∙ A)
        → ∙Π (-Π f) f ≡ 1Π
fst (∙Π-lCancel {A = A} {n = zero} f i) base = pt A
fst (∙Π-lCancel {A = A} {n = zero} f i) (loop j) =
  rCancel (sym (snd f) ∙∙ cong (fst f) (sym loop) ∙∙ snd f) i j
fst (∙Π-lCancel {A = A} {n = suc n} f i) north = pt A
fst (∙Π-lCancel {A = A} {n = suc n} f i) south = pt A
fst (∙Π-lCancel {A = A} {n = suc n} f i) (merid a j) = lem i j
  where
  pl = (sym (snd f)
     ∙∙ cong (fst f) (merid a ∙ sym (merid (ptSn _)))
     ∙∙ snd f)

  lem : (sym (snd f)
     ∙∙ cong (fst (-Π f)) (merid a ∙ sym (merid (ptSn _)))
     ∙∙ snd f) ∙ pl
     ≡ refl
  lem = cong (_∙ pl) (cong (sym (snd f) ∙∙_∙∙ (snd f))
        (cong-∙ (fst (-Π f)) (merid a) (sym (merid (ptSn _)))
        ∙∙ cong₂ _∙_ refl (cong (cong (fst f)) (rCancel (merid (ptSn _))))
        ∙∙ sym (rUnit _)))
     ∙ lCancel pl
snd (∙Π-lCancel {A = A} {n = zero} f i) = refl
snd (∙Π-lCancel {A = A} {n = suc n} f i) = refl

∙Π-assoc : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f g h : S₊∙ (suc n) →∙ A)
        → ∙Π f (∙Π g h) ≡ ∙Π (∙Π f g) h
∙Π-assoc {n = n} f g h =
     sym (leftInv (IsoSphereMapΩ (suc n)) (∙Π f (∙Π g h)))
  ∙∙ cong (Ω→SphereMap (suc n)) (IsoSphereMapΩ-pres∙Π n f (∙Π g h)
                ∙∙ cong (SphereMap→Ω (suc n) f ∙_) (IsoSphereMapΩ-pres∙Π n g h)
                ∙∙ ∙assoc (SphereMap→Ω (suc n) f) (SphereMap→Ω (suc n) g) (SphereMap→Ω (suc n) h)
                ∙∙ cong (_∙ SphereMap→Ω (suc n) h) (sym (IsoSphereMapΩ-pres∙Π n f g))
                ∙∙ sym (IsoSphereMapΩ-pres∙Π n (∙Π f g) h))
  ∙∙ leftInv (IsoSphereMapΩ (suc n)) (∙Π (∙Π f g) h)

∙Π-comm : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ}
        → (f g : S₊∙ (suc (suc n)) →∙ A)
        → ∙Π f g ≡ ∙Π g f
∙Π-comm {A = A} {n = n} f g =
     sym (leftInv (IsoSphereMapΩ (suc (suc n))) (∙Π f g))
  ∙∙ cong (Ω→SphereMap (suc (suc n))) (IsoSphereMapΩ-pres∙Π (suc n) f g
  ∙∙ EH _ _ _
  ∙∙ sym (IsoSphereMapΩ-pres∙Π (suc n) g f))
  ∙∙ leftInv (IsoSphereMapΩ (suc (suc n))) (∙Π g f)

{- π'' as a group -}
1π' : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π' n A
1π' n {A = A} = ∣ 1Π ∣₂

·π' : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π' (suc n) A → π' (suc n) A → π' (suc n) A
·π' n = sRec2 squash₂ λ p q → ∣ ∙Π p q ∣₂

-π' : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} → π' (suc n) A → π' (suc n) A
-π' n = sMap -Π

π'-rUnit : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π' (suc n) A)
        → (·π' n x (1π' (suc n))) ≡ x
π'-rUnit n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ ∙Π-rUnit p i ∣₂

π'-lUnit : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π' (suc n) A)
        → (·π' n (1π' (suc n)) x) ≡ x
π'-lUnit n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ ∙Π-lUnit p i ∣₂

π'-rCancel : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π' (suc n) A)
        → (·π' n x (-π' n x)) ≡ 1π' (suc n)
π'-rCancel n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ ∙Π-rCancel p i ∣₂

π'-lCancel : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x : π' (suc n) A)
        → (·π' n (-π' n x) x) ≡ 1π' (suc n)
π'-lCancel n = sElim (λ _ → isSetPathImplicit) λ p i → ∣ ∙Π-lCancel p i ∣₂

π'-assoc : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x y z : π' (suc n) A)
        → ·π' n x (·π' n y z) ≡ ·π' n (·π' n x y) z
π'-assoc n = sElim3 (λ _ _ _ → isSetPathImplicit) λ p q r i → ∣ ∙Π-assoc p q r i ∣₂

π'-comm : ∀ {ℓ} (n : ℕ) {A : Pointed ℓ} (x y : π' (suc (suc n)) A)
        → ·π' (suc n) x y ≡ ·π' (suc n) y x
π'-comm n = sElim2 (λ _ _ → isSetPathImplicit) λ p q i → ∣ ∙Π-comm p q i ∣₂

-- We finally get the group definition
π'Gr : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Group ℓ
fst (π'Gr n A) = π' (suc n) A
1g (snd (π'Gr n A)) = 1π' (suc n)
GroupStr._·_ (snd (π'Gr n A)) = ·π' n
inv (snd (π'Gr n A)) = -π' n
is-set (isSemigroup (isMonoid (isGroup (snd (π'Gr n A))))) = squash₂
assoc (isSemigroup (isMonoid (isGroup (snd (π'Gr n A))))) = π'-assoc n
identity (isMonoid (isGroup (snd (π'Gr n A)))) x = (π'-rUnit n x) , (π'-lUnit n x)
inverse (isGroup (snd (π'Gr n A))) x = (π'-rCancel n x) , (π'-lCancel n x)

-- and finally, the Iso
π'Gr≅πGr : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → GroupIso (π'Gr n A) (πGr n A)
fst (π'Gr≅πGr n A) = setTruncIso (IsoSphereMapΩ (suc n))
snd (π'Gr≅πGr n A) =
  makeIsGroupHom (sElim2 (λ _ _ → isSetPathImplicit)
    λ p q i → ∣ IsoSphereMapΩ-pres∙Π n p q i ∣₂)

{- Proof of πₙ(ΩA) = πₙ₊₁(A) -}
Iso-πΩ-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
        → Iso (π n (Ω A)) (π (suc n) A)
Iso-πΩ-π {A = A} n = setTruncIso (invIso (flipΩIso n))

GrIso-πΩ-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
          → GroupIso (πGr n (Ω A)) (πGr (suc n) A)
fst (GrIso-πΩ-π n) = Iso-πΩ-π _
snd (GrIso-πΩ-π n) =
  makeIsGroupHom
    (sElim2 (λ _ _ → isSetPathImplicit)
     λ p q → cong ∣_∣₂ (flipΩIso⁻pres· n p q))

{- Proof that πₙ(A) ≅ πₙ(∥ A ∥ₙ) -}
isContrΩTrunc : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → isContr (typ ((Ω^ n) (hLevelTrunc∙ n A)))
isContrΩTrunc {A = A} zero = isContrUnit*
isContrΩTrunc {A = A} (suc n) =
  subst isContr main (isContrΩTrunc {A = Ω A} n)
  where
  lem₁ : (n : ℕ) → fun (PathIdTruncIso n) (λ _ → ∣ pt A ∣)
                ≡ snd (hLevelTrunc∙ n (Ω A))
  lem₁ zero = refl
  lem₁ (suc n) = transportRefl ∣ refl ∣

  lem₂ : hLevelTrunc∙ n (Ω A) ≡ (Ω (hLevelTrunc∙ (suc n) A))
  lem₂ = sym (ua∙ (isoToEquiv (PathIdTruncIso n))
          (lem₁ n))

  main : (typ ((Ω^ n) (hLevelTrunc∙ n (Ω A))))
       ≡ (typ ((Ω^ suc n) (hLevelTrunc∙ (suc n) A)))
  main = (λ i → typ ((Ω^ n) (lem₂ i)))
       ∙ sym (isoToPath (flipΩIso n))

mutual
  ΩTruncSwitchFun : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ) →
    (hLevelTrunc∙ (suc (suc m)) ((Ω^ n) A))
      →∙ ((Ω^ n) (hLevelTrunc∙ (suc n + suc m) A))
  ΩTruncSwitchFun {A = A} n m =
    ((λ x → transport
                (λ i → fst ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) i) A)))
                (Iso.fun (ΩTruncSwitch {A = A} n (suc (suc m))) x))
       , cong (transport
                 (λ i → fst ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) i) A))))
               (ΩTruncSwitch∙ n (suc (suc m)))
       ∙ λ j → transp
                (λ i → fst ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) (i ∨ j)) A)))
                j (snd ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) j) A))))

  ΩTruncSwitchLem :
    ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
    → Iso
      (typ (Ω (hLevelTrunc∙ (suc (suc m)) ((Ω^ n) A))))
      (typ ((Ω^ suc n) (hLevelTrunc∙ (suc n + suc m) A)))
  ΩTruncSwitchLem {A = A} n m =
    (equivToIso
     (Ω→ (ΩTruncSwitchFun n m) .fst
    , isEquivΩ→ _ (compEquiv (isoToEquiv (ΩTruncSwitch {A = A} n (suc (suc m))))
       (transportEquiv
         (λ i → typ ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) i) A)))) .snd)))

  ΩTruncSwitch : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
    → Iso (hLevelTrunc m (fst ((Ω^ n) A)))
           (typ ((Ω^ n) (hLevelTrunc∙ (n + m) A)))
  ΩTruncSwitch {A = A} n zero =
    equivToIso
    (invEquiv
      (isContr→≃Unit*
        (subst isContr
          (λ i → (typ ((Ω^ n) (hLevelTrunc∙ (+-comm zero n i) A))))
        (isContrΩTrunc n))))
  ΩTruncSwitch {A = A} zero (suc m) = idIso
  ΩTruncSwitch {A = A} (suc n) (suc m) =
    compIso (invIso (PathIdTruncIso _))
      (ΩTruncSwitchLem n m)

  ΩTruncSwitch∙ : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
    → Iso.fun (ΩTruncSwitch {A = A} n m) (snd (hLevelTrunc∙ m ((Ω^ n) A)))
     ≡ pt ((Ω^ n) (hLevelTrunc∙ (n + m) A))
  ΩTruncSwitch∙ {A = A} n zero =
    isContr→isProp
    ((subst isContr
       (λ i → (typ ((Ω^ n) (hLevelTrunc∙ (+-comm zero n i) A))))
       (isContrΩTrunc n))) _ _
  ΩTruncSwitch∙ {A = A} zero (suc m) = refl
  ΩTruncSwitch∙ {A = A} (suc n) (suc m) = ∙∙lCancel _

ΩTruncSwitch-hom : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ) (p q : _)
        → Iso.fun (ΩTruncSwitch {A = A} (suc n) (suc m)) ∣ p ∙ q ∣
         ≡ Iso.fun (ΩTruncSwitch {A = A} (suc n) (suc m)) ∣ p ∣
         ∙ Iso.fun (ΩTruncSwitch {A = A} (suc n) (suc m)) ∣ q ∣
ΩTruncSwitch-hom {A = A} n m p q =
    cong (Iso.fun (ΩTruncSwitchLem {A = A} n m))
         (cong-∙ ∣_∣ₕ p q)
  ∙ Ω→pres∙ (ΩTruncSwitchFun n m) (cong ∣_∣ₕ p) (cong ∣_∣ₕ q)

2TruncΩIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
    → Iso (hLevelTrunc 2 (fst ((Ω^ n) A)))
           (typ ((Ω^ n) (hLevelTrunc∙ (2 + n) A)))
2TruncΩIso zero = idIso
2TruncΩIso {A = A} (suc n) =
  compIso
   (ΩTruncSwitch (suc n) 2)
   (pathToIso λ i → typ ((Ω^ suc n) (hLevelTrunc∙ (+-comm (suc n) 2 i) A)))

hLevΩ+ : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ)
      → isOfHLevel (m + n) (typ A) → isOfHLevel n (typ ((Ω^ m) A))
hLevΩ+ n zero p = p
hLevΩ+ {A = A} zero (suc zero) p = refl , λ _ → isProp→isSet p _ _ _ _
hLevΩ+ {A = A} zero (suc (suc zero)) p =
  refl , λ y → isOfHLevelSuc 2 p _ _ _ _ refl y
hLevΩ+ {A = A} zero (suc (suc (suc m))) p =
  transport
   (λ i → isContr (typ (Ω (ua∙
            (isoToEquiv (flipΩIso {A = A} (suc m))) (flipΩrefl m) (~ i)))))
    (hLevΩ+ {A = Ω A} zero (suc (suc m))
     (subst (λ x → isOfHLevel x (typ (Ω A)))
            (+-comm zero (suc (suc m)))
            (lem (pt A) (pt A))))
  where
  lem : isOfHLevel (3 + m) (typ A)
  lem = subst (λ x → isOfHLevel x (typ A))
              (λ i → suc (+-comm (2 + m) zero i)) p
hLevΩ+ {A = A} (suc n) (suc m) p =
  subst (isOfHLevel (suc n))
    (sym (ua (isoToEquiv (flipΩIso {A = A} m))))
    (hLevΩ+ {A = Ω A} (suc n) m
      (isOfHLevelPath' (m + suc n) p _ _))

private
  isSetΩ : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
    → (isSet (typ (Ω ((Ω^ n) (hLevelTrunc∙ (suc (suc (suc n))) A)))))
  isSetΩ {A = A} zero = isOfHLevelTrunc 3 _ _
  isSetΩ {A = A} (suc n) =
    hLevΩ+ 2 (suc (suc n))
      (transport
       (λ i → isOfHLevel (+-comm 2 (2 + n) i) (hLevelTrunc (4 + n) (typ A)))
        (isOfHLevelTrunc (suc (suc (suc (suc n))))))

πTruncIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
             → Iso (π n A) (π n (hLevelTrunc∙ (2 + n) A))
πTruncIso {A = A} zero =
  compIso (invIso (setTruncIdempotentIso squash₂))
                  (setTruncIso setTruncTrunc2Iso)
πTruncIso {A = A} (suc n) =
  compIso setTruncTrunc2Iso
    (compIso
     (2TruncΩIso (suc n))
     (invIso (setTruncIdempotentIso (isSetΩ n))))

πTruncGroupIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
             → GroupIso (πGr n A) (πGr n (hLevelTrunc∙ (3 + n) A))
fst (πTruncGroupIso n) = πTruncIso (suc n)
snd (πTruncGroupIso {A = A} n) =
  makeIsGroupHom
    (sElim2 (λ _ _ → isSetPathImplicit)
      λ a b
      → cong (inv (setTruncIdempotentIso (isSetΩ n)))
         (cong
          (transport
           (λ i → typ ((Ω^ suc n) (hLevelTrunc∙ (+-comm (suc n) 2 i) A))))
           (ΩTruncSwitch-hom n 1 a b)
        ∙ transpΩTruncSwitch
            (λ w → ((Ω^ n) (hLevelTrunc∙ w A))) (+-comm (suc n) 2) _ _))
  where
  transpΩTruncSwitch : ∀ {ℓ} (A : ℕ → Pointed ℓ) {n m : ℕ}
    (r : n ≡ m) (p q : typ (Ω (A n)))
    → subst (λ n → typ (Ω (A n))) r (p ∙ q)
     ≡ subst (λ n → typ (Ω (A n))) r p
     ∙ subst (λ n → typ (Ω (A n))) r q
  transpΩTruncSwitch A {n = n} =
    J (λ m r → (p q : typ (Ω (A n)))
              → subst (λ n → typ (Ω (A n))) r (p ∙ q)
               ≡ subst (λ n → typ (Ω (A n))) r p
               ∙ subst (λ n → typ (Ω (A n))) r q)
      λ p q → transportRefl _ ∙ cong₂ _∙_
                (sym (transportRefl p)) (sym (transportRefl q))

max_stars_repo_name: rnarkk/cubical

max_issues_repo_name: rnarkk/cubical

max_forks_repo_name: rnarkk/cubical


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS --sized-types #-}         -- no longer necessary
-- {-# OPTIONS --termination-depth=2 #-} -- no longer necessary
-- {-# OPTIONS -v term:10 #-}

module SizedBTree where

open import Common.Size

module Old where

  data BTree (A : Set) : {size : Size} → Set where
    leaf : {i : Size} → A → BTree A {↑ i}
    node : {i : Size} → BTree A {i} → BTree A {i} → BTree A {↑ i}

  map : ∀ {A B i} → (A → B) → BTree A {i} → BTree B {i}
  map f (leaf a) = leaf (f a)
  map f (node l r) = node (map f l) (map f r)

  -- deep matching

  deep : ∀ {i A} → BTree A {i} → A
  deep (leaf a) = a
  deep (node (leaf _) r) = deep r
  deep (node (node l r) _) = deep (node l r)

  -- nesting

  -- Jesper 2015-12-18: The new unifier requires the size argument of the first
  -- deep2 to be given explicitly. This is because otherwise the unifier gets
  -- stuck on an equation [↑ i₁ =?= _i_46 {i} {A} l r t]. It's not clear whether
  -- it is safe to instantiate the meta to [↑ _] here.
  deep2 : ∀ {i A} → BTree A {i} → BTree A {i}
  deep2 (leaf a) = leaf a
  deep2 (node (leaf _) r) = r
  deep2 (node (node {i} l r) t) with deep2 {↑ i} (deep2 (node l r))
  ... | leaf a = leaf a
  ... | node l2 r2 = deep2 (node l2 r2)

  -- OUTDATED: -- increasing the termination count does the job!

module New where

  data BTree (A : Set) {i : Size} :  Set where
    leaf : A → BTree A
    node : {i' : Size< i} → BTree A {i'} → BTree A {i'} → BTree A

  map : ∀ {A B i} → (A → B) → BTree A {i} → BTree B {i}
  map f (leaf a)   = leaf (f a)
  map f (node l r) = node (map f l) (map f r)

  -- deep matching

  deep : ∀ {i A} → BTree A {i} → A
  deep (leaf a)            = a
  deep (node (leaf _)   r) = deep r
  deep (node (node l r) _) = deep (node l r)

  -- nesting

  deep2 : ∀ {i A} → BTree A {i} → BTree A {i}
  deep2 (leaf a)            = leaf a
  deep2 (node (leaf _)   r) = r
  deep2 (node (node l r) _) with deep2 (deep2 (node l r))
  ... | leaf a     = leaf a
  ... | node l2 r2 = deep2 (node l2 r2)

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --safe #-}
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Allstar
  {i} {I : Set i}
  {c} {C : Set c} {{rc : RawSep C}} {u} {{sc : IsUnitalSep rc u}}
  where

open import Level
open import Data.Product
open import Data.List hiding (concat)
open import Relation.Unary

{- Inductive separating forall over a list -}
module _ {ℓ} where
  data Allstar (P : I → Pred C ℓ) : List I → SPred (ℓ ⊔ c ⊔ i) where
    nil  :            ε[ Allstar P [] ]
    cons : ∀ {x xs} → ∀[ P x ✴ Allstar P xs ⇒ Allstar P (x ∷ xs) ]

  -- not typed well in non-pattern positions
  infixr 5 _:⟨_⟩:_
  pattern _:⟨_⟩:_ x p xs = cons (x ×⟨ p ⟩ xs)

  singleton : ∀ {P x} → ∀[ P x ⇒ Allstar P [ x ] ]
  singleton v = cons (v ×⟨ ⊎-idʳ ⟩ nil)

  open import Relation.Ternary.Separation.Construct.List I
  open import Data.List.Relation.Ternary.Interleaving.Propositional as I

  repartition : ∀ {P} {Σ₁ Σ₂ Σ} →
                Σ₁ ⊎ Σ₂ ≣ Σ → ∀[ Allstar P Σ ⇒ Allstar P Σ₁ ✴ Allstar P Σ₂ ]
  repartition [] nil   = nil ×⟨ ⊎-idˡ ⟩ nil
  repartition (consˡ σ) (cons (a ×⟨ σ′ ⟩ qx)) =
    let
      xs ×⟨ σ′′ ⟩ ys = repartition σ qx
      _ , τ₁ , τ₂    = ⊎-unassoc σ′ σ′′
    in (cons (a ×⟨ τ₁ ⟩ xs)) ×⟨ τ₂ ⟩ ys
  repartition (consʳ σ) (cons (a ×⟨ σ′ ⟩ qx)) =
    let
      xs ×⟨ σ′′ ⟩ ys = repartition σ qx
      _ , τ₁ , τ₂    = ⊎-unassoc σ′ (⊎-comm σ′′)
    in xs ×⟨ ⊎-comm τ₂ ⟩ (cons (a ×⟨ τ₁ ⟩ ys))

  concat : ∀ {P} {Γ₁ Γ₂} → ∀[ Allstar P Γ₁ ✴ Allstar P Γ₂ ⇒ Allstar P (Γ₁ ++ Γ₂) ]
  concat (nil ×⟨ s ⟩ env₂) rewrite ⊎-id⁻ˡ s = env₂
  concat (cons (v ×⟨ s ⟩ env₁) ×⟨ s' ⟩ env₂) =
    let _ , eq₁ , eq₂ = ⊎-assoc s s' in
    cons (v ×⟨ eq₁ ⟩ (concat (env₁ ×⟨ eq₂ ⟩ env₂)))


text:
------------------------------------------------------------------------------
-- Testing the translation of 11-ary predicates symbols
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module P11 where

postulate
  D : Set
  P : D → D → D → D → D → D → D → D → D → D → D → Set

postulate P-refl : ∀ {x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁} →
                   P x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁ →
                   P x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁
{-# ATP prove P-refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- The bug documented below was exposed by the fix to issue 274.

{-# OPTIONS --universe-polymorphism #-}

module Issue274 where

postulate
  Level : Set
  zero : Level
  suc  : Level → Level
  _⊔_ : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}

record Q a : Set (a ⊔ a) where

record R a : Set a where
  field q : Q a

  A : Set₁
  A = Set

postulate
  ℓ : Level
  r : R (ℓ ⊔ ℓ)

foo : R ℓ
foo = r

-- Issue274.agda:32,7-8
-- ℓ ⊔ ℓ !=< ℓ of type Level
-- when checking that the expression r has type R ℓ

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import cohomology.ChainComplex
open import cohomology.Theory
open import groups.KernelImage
open import cw.CW

module cw.cohomology.ReconstructedFirstCohomologyGroup {i : ULevel} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  import cw.cohomology.TipCoboundary OT as TC
  import cw.cohomology.HigherCoboundary OT as HC
  import cw.cohomology.TipAndAugment OT as TAA
  open import cw.cohomology.WedgeOfCells OT
  open import cw.cohomology.Descending OT
  open import cw.cohomology.ReconstructedCochainComplex OT
  import cw.cohomology.FirstCohomologyGroup OT as FCG
  import cw.cohomology.FirstCohomologyGroupOnDiag OT as FCGD
  import cw.cohomology.CohomologyGroupsTooHigh OT as CGTH

  private
    ≤-dec-has-all-paths : {m n : ℕ} → has-all-paths (Dec (m ≤ n))
    ≤-dec-has-all-paths = prop-has-all-paths (Dec-level ≤-is-prop)

  private
    abstract
      first-cohomology-group-descend : ∀ {n} (⊙skel : ⊙Skeleton {i} (3 + n))
        →  cohomology-group (cochain-complex ⊙skel) 1
        == cohomology-group (cochain-complex (⊙cw-init ⊙skel)) 1
      first-cohomology-group-descend {n = O} ⊙skel
        = ap2 (λ δ₁ δ₂ → Ker/Im δ₂ δ₁ (CXₙ/Xₙ₋₁-is-abelian (⊙cw-take (lteSR lteS) ⊙skel) 1))
            (coboundary-first-template-descend-from-far {n = 2} ⊙skel (ltSR ltS) ltS)
            (coboundary-higher-template-descend-from-one-above ⊙skel)
      first-cohomology-group-descend {n = S n} ⊙skel -- n = S n
        = ap2 (λ δ₁ δ₂ → Ker/Im δ₂ δ₁ (CXₙ/Xₙ₋₁-is-abelian (⊙cw-take (≤-+-l 1 (lteSR $ lteSR $ inr (O<S n))) ⊙skel) 1))
            (coboundary-first-template-descend-from-far  {n = 3 + n} ⊙skel (ltSR (ltSR (O<S n))) (<-+-l 1 (ltSR (O<S n))))
            (coboundary-higher-template-descend-from-far {n = 3 + n} ⊙skel (<-+-l 1 (ltSR (O<S n))) (<-+-l 2 (O<S n)))

      first-cohomology-group-β : ∀ (⊙skel : ⊙Skeleton {i} 2)
        →  cohomology-group (cochain-complex ⊙skel) 1
        == Ker/Im
            (HC.cw-co∂-last ⊙skel)
            (TC.cw-co∂-head (⊙cw-init ⊙skel))
            (CXₙ/Xₙ₋₁-is-abelian (⊙cw-init ⊙skel) 1)
      first-cohomology-group-β ⊙skel
        = ap2 (λ δ₁ δ₂ → Ker/Im δ₂ δ₁ (CXₙ/Xₙ₋₁-is-abelian (⊙cw-init ⊙skel) 1))
            ( coboundary-first-template-descend-from-two ⊙skel
            ∙ coboundary-first-template-β (⊙cw-init ⊙skel))
            (coboundary-higher-template-β ⊙skel)

      first-cohomology-group-β-one-below : ∀ (⊙skel : ⊙Skeleton {i} 1)
        →  cohomology-group (cochain-complex ⊙skel) 1
        == Ker/Im
            (cst-hom {H = Lift-group {j = i} Unit-group})
            (TC.cw-co∂-head ⊙skel)
            (CXₙ/Xₙ₋₁-is-abelian ⊙skel 1)
      first-cohomology-group-β-one-below ⊙skel
        = ap
            (λ δ₁ → Ker/Im
              (cst-hom {H = Lift-group {j = i} Unit-group})
              δ₁ (CXₙ/Xₙ₋₁-is-abelian ⊙skel 1))
            (coboundary-first-template-β ⊙skel)

  abstract
    first-cohomology-group : ∀ {n} (⊙skel : ⊙Skeleton {i} n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      → C 1 ⊙⟦ ⊙skel ⟧ ≃ᴳ cohomology-group (cochain-complex ⊙skel) 1
    first-cohomology-group {n = 0} ⊙skel ac =
      CGTH.C-cw-iso-ker/im 1 ltS (TAA.C2×CX₀ ⊙skel 0) ⊙skel ac
    first-cohomology-group {n = 1} ⊙skel ac =
          coe!ᴳ-iso (first-cohomology-group-β-one-below ⊙skel)
      ∘eᴳ FCGD.C-cw-iso-ker/im ⊙skel ac
    first-cohomology-group {n = 2} ⊙skel ac =
          coe!ᴳ-iso (first-cohomology-group-β ⊙skel)
      ∘eᴳ FCG.C-cw-iso-ker/im ⊙skel ac
    first-cohomology-group {n = S (S (S n))} ⊙skel ac =
          coe!ᴳ-iso (first-cohomology-group-descend ⊙skel)
      ∘eᴳ first-cohomology-group (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)
      ∘eᴳ C-cw-descend-at-lower ⊙skel (<-+-l 1 (O<S n)) ac

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --without-K #-}

open import Base
open import Homotopy.Pointed
open import Homotopy.Connected

module Homotopy.Cover.HomotopyGroupSetIsomorphism {i}
  (A⋆ : pType i) (A⋆-is-conn : is-connected⋆ ⟨0⟩ A⋆) where
  open pType A⋆ renaming (∣_∣ to A ; ⋆ to a)

  open import Algebra.Groups
  open import Homotopy.Truncation
  open import Homotopy.HomotopyGroups {i}
  open import Homotopy.PathTruncation
  open import Homotopy.Cover.Def A
  open import Homotopy.Cover.Ribbon A⋆

  private
    module G = group (fundamental-group A⋆)
  open import Algebra.GroupSets (fundamental-group A⋆)

  {-
      Isomorphism between pi1(A)-sets and coverings.
  -}

  gset⇒covering : gset → covering
  gset⇒covering gset[ _ , act , _ ] = cov[ ribbon act , ribbon-is-set ]

  covering⇒action : ∀ cov → action (covering.fiber cov a)
  covering⇒action cov = act[ tracing cov , (λ _ → refl) , compose-tracing cov ]

  covering⇒gset : covering → gset
  covering⇒gset cov = let open covering cov in
    gset[ fiber a , covering⇒action cov , fiber-is-set a ]

  -- The first direction: covering -> gset -> covering

  -- From 0-connectedness we can get a (-1)-truncated base path.
  -- The challenge is to get this path.
  abstract
    [base-path] : ∀ a₂ → [ a ≡ a₂ ]
    [base-path] = connected-has-all-τ-paths A⋆-is-conn a

  -- Part 1: Show that the generated cover (ribbon) is fiberwisely
  --         equivalent to the original fiber.
  private
    module _ (cov : covering) where

      -- Suppose that we get the path, we can compute the ribbon easily.
      fiber+path⇒ribbon : ∀ a₂ (y : covering.fiber cov a₂) (p : a ≡ a₂)
        → ribbon (covering⇒action cov) a₂
      fiber+path⇒ribbon a₂ y p = trace (tracing cov y (proj $ ! p)) (proj p)

      abstract
        -- Our construction is "constant" with respect to paths.
        fiber+path⇒ribbon-is-path-irrelevant : ∀ a₂
          (y : covering.fiber cov a₂) (p₁ p₂ : a ≡ a₂)
          → fiber+path⇒ribbon a₂ y p₁ ≡ fiber+path⇒ribbon a₂ y p₂
        fiber+path⇒ribbon-is-path-irrelevant .a y p refl =
          trace (tracing cov y (proj $ ! p)) (proj p)
            ≡⟨ paste y (proj $ ! p) (proj p) ⟩
          trace y (proj $ (! p ∘ p))
            ≡⟨ ap (λ x → trace y (proj x)) $ opposite-left-inverse p ⟩∎
          trace y refl₀
            ∎

      -- Call the magical factorization library.
      open import Homotopy.Extensions.ToPropToConstSet

      -- Now we can read the (-1)-truncated path.
      fiber+path₋₁⇒ribbon : ∀ a₂ (y : covering.fiber cov a₂)
        → [ a ≡ a₂ ] → ribbon (covering⇒action cov) a₂
      fiber+path₋₁⇒ribbon a₂ y = cst-extend
        ⦃ ribbon-is-set a₂ ⦄
        (fiber+path⇒ribbon a₂ y)
        (fiber+path⇒ribbon-is-path-irrelevant a₂ y)

  -- So the conversion from fiber to ribbon is done.
  fiber⇒ribbon : ∀ cov a₂ → covering.fiber cov a₂ → ribbon (covering⇒action cov) a₂
  fiber⇒ribbon cov a₂ y = fiber+path₋₁⇒ribbon cov a₂ y $ [base-path] a₂

  -- The other direction is easy.
  ribbon⇒fiber : ∀ cov a₂ → ribbon (covering⇒action cov) a₂ → covering.fiber cov a₂
  ribbon⇒fiber cov a₂ = let open covering cov in
    ribbon-rec-nondep a₂ (fiber a₂) ⦃ fiber-is-set a₂ ⦄ (tracing cov) (compose-tracing cov)

  private
    -- Some routine computations.
    abstract
      ribbon⇒fiber⇒ribbon : ∀ cov a₂ r → fiber⇒ribbon cov a₂ (ribbon⇒fiber cov a₂ r) ≡ r
      ribbon⇒fiber⇒ribbon cov a₂ = ribbon-rec a₂
        (λ r → fiber⇒ribbon cov a₂ (ribbon⇒fiber cov a₂ r) ≡ r)
        ⦃ λ _ → ≡-is-set $ ribbon-is-set a₂ ⦄
        (λ y p → []-extend
          -- All ugly things will go away when bp = proj bp′
          ⦃ λ bp → ribbon-is-set a₂
                    (fiber+path₋₁⇒ribbon cov a₂ (tracing cov y p) bp)
                    (trace y p) ⦄
          (lemma a₂ y p)
          ([base-path] a₂))
        (λ _ _ _ → prop-has-all-paths (ribbon-is-set a₂ _ _) _ _)
        where
          abstract
            lemma : ∀ a₂ (y : covering.fiber cov a) (p : a ≡₀ a₂) (bp : a ≡ a₂)
              → trace {act = covering⇒action cov}
                  (tracing cov (tracing cov y p) (proj $ ! bp)) (proj bp)
              ≡ trace y p
            lemma .a y p refl =
              trace (tracing cov y p) refl₀
                ≡⟨ paste y p refl₀ ⟩
              trace y (p ∘₀ refl₀)
                ≡⟨ ap (trace y) $ refl₀-right-unit p ⟩∎
              trace y p
                ∎

      fiber⇒ribbon⇒fiber : ∀ cov a₂ y → ribbon⇒fiber cov a₂ (fiber⇒ribbon cov a₂ y) ≡ y
      fiber⇒ribbon⇒fiber cov a₂ y = let open covering cov in []-extend
        -- All ugly things will go away when bp = proj bp′
        ⦃ λ bp → fiber-is-set a₂
                  (ribbon⇒fiber cov a₂
                    (fiber+path₋₁⇒ribbon cov a₂ y bp))
                  y ⦄
        (lemma a₂ y)
        ([base-path] a₂)
        where
          abstract
            lemma : ∀ a₂ (y : covering.fiber cov a₂) (bp : a ≡ a₂)
              → tracing cov (tracing cov y (proj $ ! bp)) (proj bp)
              ≡ y
            lemma .a y refl = refl

  covering⇒gset⇒covering : ∀ cov → gset⇒covering (covering⇒gset cov) ≡ cov
  covering⇒gset⇒covering cov = covering-eq $ funext λ a₂
    → eq-to-path $ ribbon⇒fiber cov a₂ , iso-is-eq
        (ribbon⇒fiber cov a₂)
        (fiber⇒ribbon cov a₂)
        (fiber⇒ribbon⇒fiber cov a₂)
        (ribbon⇒fiber⇒ribbon cov a₂)

  -- The second direction : gset -> covering -> gset

  -- Part 2.1: The fiber over the point a is the carrier.
  ribbon-a⇒Y : ∀ {Y} {act : action Y} ⦃ _ : is-set Y ⦄ → ribbon act a → Y
  ribbon-a⇒Y {Y} {act} ⦃ Y-is-set ⦄ = let open action act in
    ribbon-rec-nondep a Y ⦃ Y-is-set ⦄ _∙_ assoc

  ribbon-a≃Y : ∀ {Y} {act : action Y} ⦃ _ : is-set Y ⦄ → ribbon act a ≃ Y
  ribbon-a≃Y {Y} {act} ⦃ Y-is-set ⦄ = let open action act in
    ribbon-a⇒Y ⦃ Y-is-set ⦄ , iso-is-eq _
      (λ y → trace y refl₀)
      (λ y → right-unit y)
      (ribbon-rec a
        (λ r → trace (ribbon-a⇒Y ⦃ Y-is-set ⦄ r) refl₀ ≡ r)
        ⦃ λ _ → ≡-is-set $ ribbon-is-set a ⦄
        (λ y p →
          trace (y ∙ p) refl₀
            ≡⟨ paste y p refl₀ ⟩
          trace y (p G.∙ refl₀)
            ≡⟨ ap (trace y) $ G.right-unit p ⟩∎
          trace y p
            ∎)
        (λ _ _ _ → prop-has-all-paths (ribbon-is-set a _ _) _ _))

  private
    -- Some lemmas to simplify the proofs.
    trans-eq-∙ : ∀ {Y₁ Y₂ : Set i} (Y≃ : Y₁ ≃ Y₂) (_∙_ : Y₁ → G.carrier → Y₁) (y₂ : Y₂) (g : G.carrier)
      → transport (λ Y → Y → G.carrier → Y) (eq-to-path Y≃) _∙_ y₂ g ≡ (Y≃ ☆ (inverse Y≃ y₂ ∙ g))
    trans-eq-∙ = equiv-induction
      (λ {Y₁ Y₂ : Set i} (Y≃ : Y₁ ≃ Y₂)
        → ∀ (_∙_ : Y₁ → G.carrier → Y₁) (y₂ : Y₂) (g : G.carrier)
        → transport (λ Y → Y → G.carrier → Y) (eq-to-path Y≃) _∙_ y₂ g ≡ (Y≃ ☆ (inverse Y≃ y₂ ∙ g)))
      (λ Y _∙_ y₂ g → ap (λ x → transport (λ Y → Y → G.carrier → Y) x _∙_ y₂ g)
                         $ path-to-eq-right-inverse refl)

  gset⇒covering⇒gset : ∀ gs → covering⇒gset (gset⇒covering gs) ≡ gs
  gset⇒covering⇒gset gset[ Y , act , Y-is-set ] =
    let
      open action act
      _⊙_ = tracing cov[ ribbon act , ribbon-is-set {Y} {act} ]
      ≃Y = ribbon-a≃Y ⦃ Y-is-set ⦄
      ⇒Y = ribbon-a⇒Y ⦃ Y-is-set ⦄
    in gset-eq
        (eq-to-path ≃Y)
        (funext λ y → funext $ π₀-extend ⦃ λ _ → ≡-is-set Y-is-set ⦄ λ p →
          transport (λ Y → Y → G.carrier → Y) (eq-to-path ≃Y) _⊙_ y (proj p)
            ≡⟨ trans-eq-∙ ≃Y _⊙_ y (proj p) ⟩
          ⇒Y (transport (ribbon act) p (trace y refl₀))
            ≡⟨ ap ⇒Y $ trans-trace act p y refl₀ ⟩∎
          y ∙ proj p
            ∎)

  -- Finally...

  gset-covering-eq : gset ≃ covering
  gset-covering-eq = gset⇒covering , iso-is-eq _ covering⇒gset
                        covering⇒gset⇒covering
                        gset⇒covering⇒gset

  {-
      Universality of the covering generated by the fundamental group itself.
  -}

  -- FIXME What's the established terminology for this?
  canonical-gset : gset
  canonical-gset = record
    { carrier = G.carrier
    ; act     = record
      { _∙_        = _∘₀_
      ; right-unit = refl₀-right-unit
      ; assoc      = concat₀-assoc
      }
    ; set     = π₀-is-set (a ≡ a)
    }

  -- FIXME What's the established terminology for this?
  canonical-covering : covering
  canonical-covering = gset⇒covering canonical-gset

  private
    module Universality where
      open covering canonical-covering
      open gset canonical-gset

      center′ : Σ A fiber
      center′ = (a , trace {act = act} refl₀ refl₀)

      center : τ ⟨1⟩ (Σ A fiber)
      center = proj center′

      private
        -- An ugly lemma for this development only
        trans-fiber≡cst-proj-Σ-eq : ∀ {i} (P : Set i) (Q : P → Set i)
          (a : P) (c : Σ P Q) {b₁ b₂} (p : b₁ ≡ b₂) (q : a ≡ π₁ c)
          (r : transport Q q b₁ ≡ π₂ c)
          → transport (λ r → (a , r) ≡₀ c) p (proj $ Σ-eq q r)
          ≡ proj (Σ-eq q (ap (transport Q q) (! p) ∘ r))
        trans-fiber≡cst-proj-Σ-eq P Q a c refl q r = refl

      abstract
        path-trace-fiber : ∀ {a₂} y (p : a ≡ a₂)
          → transport fiber (! p ∘ ! y) (trace (proj y) (proj p))
          ≡ trace refl₀ refl₀
        path-trace-fiber y refl =
          transport fiber (! y) (trace (proj y) refl₀)
            ≡⟨ trans-trace act (! y) (proj y) refl₀ ⟩
          trace (proj y) (proj $ ! y)
            ≡⟨ paste refl₀ (proj y) (proj $ ! y) ⟩
          trace refl₀ (proj $ y ∘ ! y)
            ≡⟨ ap (trace refl₀ ◯ proj) $ opposite-right-inverse y ⟩∎
          trace refl₀ refl₀
            ∎

      path-trace : ∀ {a₂} y p → (a₂ , trace {act = act} y p) ≡₀ center′
      path-trace {a₂} =
        π₀-extend ⦃ λ y → Π-is-set λ p → π₀-is-set ((a₂ , trace y p) ≡ center′) ⦄
          (λ y → π₀-extend ⦃ λ p → π₀-is-set ((a₂ , trace (proj y) p) ≡ center′) ⦄
            (λ p → proj $ Σ-eq (! p ∘ ! y) (path-trace-fiber y p)))

      abstract
        path-paste′ : ∀ {a₂} y loop p
          → transport (λ r → (a₂ , r) ≡₀ center′) (paste (proj y) (proj loop) (proj p))
              (path-trace (proj $ y ∘ loop) (proj p))
          ≡ path-trace (proj y) (proj $ loop ∘ p)
        path-paste′ y loop refl =
          transport (λ r → (a , r) ≡₀ center′) (paste (proj y) (proj loop) refl₀)
            (proj $ Σ-eq (! (y ∘ loop)) (path-trace-fiber (y ∘ loop) refl))
              ≡⟨ trans-fiber≡cst-proj-Σ-eq A fiber a center′
                    (paste (proj y) (proj loop) refl₀)
                    (! (y ∘ loop)) (path-trace-fiber (y ∘ loop) refl) ⟩
          proj (Σ-eq (! (y ∘ loop)) _)
              ≡⟨ ap proj $
                  ap2 (λ p q → Σ-eq p q)
                    (! (y ∘ loop)
                      ≡⟨ opposite-concat y loop ⟩
                    ! loop ∘ ! y
                      ≡⟨ ap (λ x → ! x ∘ ! y) $ ! $ refl-right-unit loop ⟩∎
                    ! (loop ∘ refl) ∘ ! y
                      ∎)
                    (prop-has-all-paths (ribbon-is-set a _ _) _ _) ⟩∎
          proj (Σ-eq (! (loop ∘ refl) ∘ ! y) (path-trace-fiber y (loop ∘ refl)))
              ∎

      abstract
        path-paste : ∀ {a₂} y loop p
          → transport (λ r → (a₂ , r) ≡₀ center′) (paste y loop p)
              (path-trace (y ∘₀ loop) p)
          ≡ path-trace y (loop ∘₀ p)
        path-paste {a₂} =
          π₀-extend ⦃ λ y → Π-is-set λ loop → Π-is-set λ p → ≡-is-set $ π₀-is-set _ ⦄
            (λ y → π₀-extend ⦃ λ loop → Π-is-set λ p → ≡-is-set $ π₀-is-set _ ⦄
              (λ loop → π₀-extend ⦃ λ p → ≡-is-set $ π₀-is-set _ ⦄
                (λ p → path-paste′ y loop p)))

      path′ : (y : Σ A fiber) → proj {n = ⟨1⟩} y ≡ center
      path′ y = τ-path-equiv-path-τ-S {n = ⟨0⟩} ☆
        ribbon-rec {act = act} (π₁ y)
          (λ r → (π₁ y , r) ≡₀ center′)
          ⦃ λ r → π₀-is-set ((π₁ y , r) ≡ center′) ⦄
          path-trace
          path-paste
          (π₂ y)

      path : (y : τ ⟨1⟩ (Σ A fiber)) → y ≡ center
      path = τ-extend {n = ⟨1⟩} ⦃ λ _ → ≡-is-truncated ⟨1⟩ $ τ-is-truncated ⟨1⟩ _ ⦄ path′

  canonical-covering-is-universal : is-universal canonical-covering
  canonical-covering-is-universal = Universality.center , Universality.path

  -- The other direction:  If a covering is universal, then the fiber
  -- is equivalent to the fundamental group.
  module _ (cov : covering) (cov-is-universal : is-universal cov) where
    open covering cov
    open action (covering⇒action cov)

    -- We need a point!
    module GiveMeAPoint (center : fiber a) where

      -- Goal: fiber a <-> fundamental group

      fiber-a⇒fg : fiber a → a ≡₀ a
      fiber-a⇒fg y = ap₀ π₁ $ connected-has-all-τ-paths
        cov-is-universal (a , center) (a , y)

      fg⇒fiber-a : a ≡₀ a → fiber a
      fg⇒fiber-a = tracing cov center

      fg⇒fiber-a⇒fg : ∀ p → fiber-a⇒fg (fg⇒fiber-a p) ≡ p
      fg⇒fiber-a⇒fg = π₀-extend ⦃ λ _ → ≡-is-set $ π₀-is-set _ ⦄ λ p →
        ap₀ π₁ (connected-has-all-τ-paths
          cov-is-universal (a , center) (a , transport fiber p center))
            ≡⟨ ap (ap₀ π₁)
                  $ ! $ π₂ (connected-has-connected-paths cov-is-universal _ _)
                           (proj $ Σ-eq p refl) ⟩
        ap₀ π₁ (proj $ Σ-eq p refl)
            ≡⟨ ap proj $ base-path-Σ-eq p refl ⟩∎
        proj p
            ∎

      fiber-a⇒fg⇒fiber-a : ∀ y → fg⇒fiber-a (fiber-a⇒fg y) ≡ y
      fiber-a⇒fg⇒fiber-a y = π₀-extend
        ⦃ λ p → ≡-is-set {x = tracing cov center (ap₀ π₁ p)} {y = y}
                  $ fiber-is-set a ⦄
        (λ p →
          transport fiber (base-path p) center
            ≡⟨ trans-base-path p ⟩∎
          y
            ∎)
        (connected-has-all-τ-paths cov-is-universal (a , center) (a , y))

      fiber-a≃fg : fiber a ≃ (a ≡₀ a)
      fiber-a≃fg = fiber-a⇒fg , iso-is-eq _ fg⇒fiber-a
        fg⇒fiber-a⇒fg fiber-a⇒fg⇒fiber-a

    -- This is the best we can obtain, because there is no continuous
    -- choice of the center.
    [center] : [ fiber a ]
    [center] = τ-extend-nondep
      ⦃ prop-is-gpd []-is-prop ⦄
      (λ y → []-extend-nondep
        ⦃ []-is-prop ⦄
        (proj ◯ λ p → transport fiber p (π₂ y))
        (connected-has-all-τ-paths A⋆-is-conn (π₁ y) a))
      (π₁ cov-is-universal)

    -- [ isomorphism between the fiber and the fundamental group ]
    -- This is the best we can obtain, because there is no continuous
    -- choice of the center.
    [fiber-a≃fg] : [ fiber a ≃ (a ≡₀ a) ]
    [fiber-a≃fg] = []-extend-nondep ⦃ []-is-prop ⦄
      (proj ◯ GiveMeAPoint.fiber-a≃fg) [center]

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Susp.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Path
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.HITs.Join
open import Cubical.HITs.Susp.Base
open import Cubical.Homotopy.Loopspace

private
  variable
    ℓ : Level

open Iso

Susp-iso-joinBool : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (join A Bool)
fun Susp-iso-joinBool north = inr true
fun Susp-iso-joinBool south = inr false
fun Susp-iso-joinBool (merid a i) = (sym (push a true) ∙ push a false) i
inv Susp-iso-joinBool (inr true ) = north
inv Susp-iso-joinBool (inr false) = south
inv Susp-iso-joinBool (inl _) = north
inv Susp-iso-joinBool (push a true  i) = north
inv Susp-iso-joinBool (push a false i) = merid a i
rightInv Susp-iso-joinBool (inr true ) = refl
rightInv Susp-iso-joinBool (inr false) = refl
rightInv Susp-iso-joinBool (inl a) = sym (push a true)
rightInv Susp-iso-joinBool (push a true  i) j = push a true (i ∨ ~ j)
rightInv Susp-iso-joinBool (push a false i) j
  = hcomp (λ k → λ { (i = i0) → push a true (~ j)
                   ; (i = i1) → push a false k
                   ; (j = i1) → push a false (i ∧ k) })
          (push a true (~ i ∧ ~ j))
leftInv Susp-iso-joinBool north = refl
leftInv Susp-iso-joinBool south = refl
leftInv (Susp-iso-joinBool {A = A}) (merid a i) j
  = hcomp (λ k → λ { (i = i0) → transp (λ _ → Susp A) (k ∨ j) north
                   ; (i = i1) → transp (λ _ → Susp A) (k ∨ j) (merid a k)
                   ; (j = i1) → merid a (i ∧ k) })
          (transp (λ _ → Susp A) j north)

Susp≃joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≃ join A Bool
Susp≃joinBool = isoToEquiv Susp-iso-joinBool

Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
Susp≡joinBool = isoToPath Susp-iso-joinBool

congSuspIso : ∀ {ℓ} {A B : Type ℓ} → Iso A B → Iso (Susp A) (Susp B)
fun (congSuspIso is) = suspFun (fun is)
inv (congSuspIso is) = suspFun (inv is)
rightInv (congSuspIso is) north = refl
rightInv (congSuspIso is) south = refl
rightInv (congSuspIso is) (merid a i) j = merid (rightInv is a j) i
leftInv (congSuspIso is) north = refl
leftInv (congSuspIso is) south = refl
leftInv (congSuspIso is) (merid a i) j = merid (leftInv is a j) i

congSuspEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≃ B → Susp A ≃ Susp B
congSuspEquiv {ℓ} {A} {B} h = isoToEquiv (congSuspIso (equivToIso h))

suspToPropElim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Type ℓ'} (a : A)
                 → ((x : Susp A) → isProp (B x))
                 → B north
                 → (x : Susp A) → B x
suspToPropElim a isProp Bnorth north = Bnorth
suspToPropElim {B = B} a isProp Bnorth south = subst B (merid a) Bnorth
suspToPropElim {B = B} a isProp Bnorth (merid a₁ i) =
  isOfHLevel→isOfHLevelDep 1 isProp Bnorth (subst B (merid a) Bnorth) (merid a₁) i

suspToPropElim2 : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Susp A → Type ℓ'} (a : A)
                 → ((x y : Susp A) → isProp (B x y))
                 → B north north
                 → (x y : Susp A) → B x y
suspToPropElim2 _ _ Bnorth north north = Bnorth
suspToPropElim2 {B = B} a _ Bnorth north south = subst (B north) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth north (merid x i) =
  isProp→PathP (λ i → isprop north (merid x i))
               Bnorth (subst (B north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a _ Bnorth south north = subst (λ x → B x north) (merid a) Bnorth
suspToPropElim2 {B = B} a _ Bnorth south south = subst (λ x → B x x) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth south (merid x i) =
  isProp→PathP (λ i → isprop south (merid x i))
               (subst (λ x → B x north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) north =
  isProp→PathP (λ i → isprop (merid x i) north)
               Bnorth (subst (λ x → B x north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) south =
  isProp→PathP (λ i → isprop (merid x i) south)
               (subst (B north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) (merid y j) =
  isSet→SquareP (λ i j → isOfHLevelSuc 1 (isprop _ _))
     (isProp→PathP (λ i₁ → isprop north (merid y i₁)) Bnorth
                   (subst (B north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop south (merid y i₁))
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) north) Bnorth
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) south)
                   (subst (B north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth)) i j
{- Clever proof:
suspToPropElim2 a isProp Bnorth =
  suspToPropElim a (λ x → isOfHLevelΠ 1 λ y → isProp x y)
                   (suspToPropElim a (λ x → isProp north x) Bnorth)
-}

funSpaceSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
                   → Iso (Σ[ x ∈ B ] Σ[ y ∈ B ] (A → x ≡ y)) (Susp A → B)
Iso.fun funSpaceSuspIso (x , y , f) north = x
Iso.fun funSpaceSuspIso (x , y , f) south = y
Iso.fun funSpaceSuspIso (x , y , f) (merid a i) = f a i
Iso.inv funSpaceSuspIso f = (f north) , (f south , (λ x → cong f (merid x)))
Iso.rightInv funSpaceSuspIso f = funExt λ {north → refl
                                             ; south → refl
                                             ; (merid a i) → refl}
Iso.leftInv funSpaceSuspIso _ = refl

toSusp : (A : Pointed ℓ) → typ A → typ (Ω (Susp∙ (typ A)))
toSusp A x = merid x ∙ merid (pt A) ⁻¹

toSuspPointed : (A : Pointed ℓ) → A →∙ Ω (Susp∙ (typ A))
fst (toSuspPointed A) = toSusp A
snd (toSuspPointed A) = rCancel (merid (pt A))

module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} where
  fromSusp→toΩ : Susp∙ (typ A) →∙ B → (A →∙ Ω B)
  fst (fromSusp→toΩ f) x = sym (snd f) ∙∙ cong (fst f) (toSusp A x) ∙∙ snd f
  snd (fromSusp→toΩ f) =
    cong (sym (snd f) ∙∙_∙∙ (snd f))
          (cong (cong (fst f))
           (rCancel (merid (pt A))))
       ∙ ∙∙lCancel (snd f)

  toΩ→fromSusp : A →∙ Ω B → Susp∙ (typ A) →∙ B
  fst (toΩ→fromSusp f) north = pt B
  fst (toΩ→fromSusp f) south = pt B
  fst (toΩ→fromSusp f) (merid a i) = fst f a i
  snd (toΩ→fromSusp f) = refl

  ΩSuspAdjointIso : Iso (A →∙ Ω B) (Susp∙ (typ A) →∙ B)
  fun ΩSuspAdjointIso = toΩ→fromSusp
  inv ΩSuspAdjointIso = fromSusp→toΩ
  rightInv ΩSuspAdjointIso f =
    ΣPathP (funExt
      (λ { north → sym (snd f)
         ; south → sym (snd f) ∙ cong (fst f) (merid (pt A))
         ; (merid a i) j →
           hcomp (λ k → λ { (i = i0) → snd f (~ j ∧ k)
                           ; (i = i1) → compPath-filler'
                                          (sym (snd f))
                                          (cong (fst f) (merid (pt A))) k j
                           ; (j = i1) → fst f (merid a i)})
                 (fst f (compPath-filler (merid a) (sym (merid (pt A))) (~ j) i))})
         , λ i j → snd f (~ i ∨ j))
  leftInv ΩSuspAdjointIso f =
    →∙Homogeneous≡ (isHomogeneousPath _ _)
      (funExt λ x → sym (rUnit _)
             ∙ cong-∙ (fst (toΩ→fromSusp f)) (merid x) (sym (merid (pt A)))
             ∙ cong (fst f x ∙_) (cong sym (snd f))
             ∙ sym (rUnit _))

  IsoΩFunSuspFun : Iso (typ (Ω (A →∙ B ∙))) (Susp∙ (typ A) →∙ B)
  IsoΩFunSuspFun = compIso (ΩfunExtIso A B) ΩSuspAdjointIso

-- inversion
invSusp : ∀ {ℓ} {A : Type ℓ} → Susp A → Susp A
invSusp north = south
invSusp south = north
invSusp (merid a i) = merid a (~ i)

invSusp² : ∀ {ℓ} {A : Type ℓ} (x : Susp A) → invSusp (invSusp x) ≡ x
invSusp² north = refl
invSusp² south = refl
invSusp² (merid a i) = refl

invSuspIso : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (Susp A)
fun invSuspIso = invSusp
inv invSuspIso = invSusp
rightInv invSuspIso = invSusp²
leftInv invSuspIso = invSusp²

-- Explicit definition of the iso
-- join (Susp A) B ≃ Susp (join A B)
-- for pointed types A and B. This is useful for obtaining a ``nice'' iso
-- join Sⁿ Sᵐ ≃ Sⁿ⁺ᵐ⁺¹
module _ {A B : Pointed ℓ} where

  private -- some useful fillers
    rinv-filler : (b : typ B) → I → I → I → join (Susp (typ A)) (typ B)
    rinv-filler b i j k =
      hfill (λ k → λ {(i = i0) → push south b (~ k)
                     ; (i = i1) → push north b (~ k ∨ j)
                     ; (j = i0) → push (merid (pt A) (~ i)) b (~ k)
                     ; (j = i1) → push south b (~ k ∨ i)})
            (inS (inr b))
            k

    suspJoin→joinSuspFiller :
      I → I → I → (a : typ A) (b : typ B) → join (Susp (typ A)) (typ B)
    suspJoin→joinSuspFiller i j k a b =
      hfill (λ k → λ {(i = i0) → push north b (~ k)
                     ; (i = i1) → push south b (~ k)
                     ; (j = i0) → push (merid a i) b (~ k)
                     ; (j = i1) → push (merid (pt A) i) b (~ k)})
            (inS (inr b))
            k

    joinSuspFiller :
      I → I → I → (a : typ A) (b : typ B) → Susp (join (typ A) (typ B))
    joinSuspFiller i j k a b =
      hfill (λ k → λ {(i = i0) → merid (push a b (~ k)) j
                     ; (i = i1) → north
                     ; (j = i0) → north
                     ; (j = i1) → merid (push (pt A) b (~ k)) (~ i)})
            (inS (merid (inr b) (~ i ∧ j)))
            k

  suspJoin→joinSusp : Susp (join (typ A) (typ B)) → join (Susp (typ A)) (typ B)
  suspJoin→joinSusp north = inl north
  suspJoin→joinSusp south = inl south
  suspJoin→joinSusp (merid (inl x) i) = inl ((merid x) i)
  suspJoin→joinSusp  (merid (inr x) i) = inl (merid (pt A) i)
  suspJoin→joinSusp  (merid (push a b j) i) = suspJoin→joinSuspFiller i j i1 a b

  joinSusp→suspJoin : join (Susp (typ A)) (typ B) → Susp (join (typ A) (typ B))
  joinSusp→suspJoin (inl north) = north
  joinSusp→suspJoin (inl south) = south
  joinSusp→suspJoin (inl (merid a i)) = merid (inl a) i
  joinSusp→suspJoin (inr x) = north
  joinSusp→suspJoin (push north b i) = north
  joinSusp→suspJoin (push south b i) = merid (inl (pt A)) (~ i)
  joinSusp→suspJoin (push (merid a j) b i) = joinSuspFiller i j i1 a b

  suspJoin→joinSusp→suspJoin : (x : Susp (join (typ A) (typ B)))
    → joinSusp→suspJoin (suspJoin→joinSusp x) ≡ x
  suspJoin→joinSusp→suspJoin north = refl
  suspJoin→joinSusp→suspJoin south = refl
  suspJoin→joinSusp→suspJoin (merid (inl x) i) = refl
  suspJoin→joinSusp→suspJoin (merid (inr x) i) j = merid (push (pt A) x j) i
  suspJoin→joinSusp→suspJoin (merid (push a b j) i) k =
    hcomp (λ r → λ {(i = i0) → north
                   ; (i = i1) → merid (push (snd A) b (k ∧ (~ r ∨ j))) r
                   ; (j = i0) → joinSuspFiller (~ r) i (~ k ∨ r) a b
                   ; (j = i1) → joinSuspFiller (~ r) i (~ k) (pt A) b
                   ; (k = i0) → joinSusp→suspJoin (suspJoin→joinSuspFiller i j r a b)
                   ; (k = i1) → k=i1 i j r})
          north
     where
     k=i1 :
       Cube
         (λ j r → north)
         (λ j r → merid (push (snd A) b (~ r ∨ j)) r)
         (λ i r → joinSuspFiller (~ r) i r a b)
         (λ i r → merid (inr b) (r ∧ i))
         refl
         λ i j → merid (push a b j) i
     k=i1 i j r =
       hcomp (λ k → λ {(i = i0) → north
                      ; (i = i1) → merid (push (snd A) b (~ r ∨ ~ k ∨ j)) r
                      ; (j = i0) → joinSuspFiller (~ r) i (r ∧ k) a b
                      ; (j = i1) → merid (inr b) (r ∧ i)
                      ; (r = i0) → north
                      ; (r = i1) → merid (push a b (~ k ∨ j)) i})
             (merid (inr b) (i ∧ r))

  joinSusp→suspJoin→joinSusp : (x : join (Susp (typ A)) (typ B))
    → suspJoin→joinSusp (joinSusp→suspJoin x) ≡ x
  joinSusp→suspJoin→joinSusp (inl north) = refl
  joinSusp→suspJoin→joinSusp (inl south) = refl
  joinSusp→suspJoin→joinSusp (inl (merid a i)) = refl
  joinSusp→suspJoin→joinSusp (inr x) = push north x
  joinSusp→suspJoin→joinSusp (push north b i) j = push north b (j ∧ i)
  joinSusp→suspJoin→joinSusp (push south b i) j = rinv-filler b i j i1
  joinSusp→suspJoin→joinSusp (push (merid a j) b i) k =
    hcomp (λ r → λ { (j = i0) → push north b (k ∧ i)
                     ; (j = i1) → lem i k r
                     ; (i = i0) → suspJoin→joinSuspFiller j (~ r ∧ ~ k) i1 a b
                     ; (i = i1) → push north b k
                     ; (k = i0) → suspJoin→joinSusp (joinSuspFiller i j r a b)
                     ; (k = i1) → push (merid a j) b i})
          (hcomp (λ r → λ { (j = i0) → push north b (~ r ∨ (k ∧ i))
                     ; (j = i1) → rinv-filler b i k r
                     ; (i = i0) → suspJoin→joinSuspFiller j (~ k) r a b
                     ; (i = i1) → push north b (~ r ∨ k)
                     ; (k = i0) → push (merid (snd A) (~ i ∧ j)) b (~ r)
                     ; (k = i1) → push (merid a j) b (~ r ∨ i)})
                 (inr b))
    where
    lem : Cube (λ k r → inl south)
               (λ k r → push north b k)
               (λ i r → suspJoin→joinSuspFiller (~ i) r i1 (pt A) b)
               (λ i r → push south b i)
               (λ i k → rinv-filler b i k i1)
               λ i k → rinv-filler b i k i1
    lem i k r =
      hcomp (λ j → λ { (r = i0) → rinv-filler b i k j
                     ; (r = i1) → rinv-filler b i k j
                     ; (i = i0) → push south b (~ j)
                     ; (i = i1) → push north b (k ∨ ~ j)
                     ; (k = i0) → suspJoin→joinSuspFiller (~ i) r j (pt A) b
                     ; (k = i1) → push south b (i ∨ ~ j)})
                 (inr b)

  Iso-joinSusp-suspJoin :
    Iso (join (Susp (typ A)) (typ B)) (Susp (join (typ A) (typ B)))
  Iso.fun Iso-joinSusp-suspJoin = joinSusp→suspJoin
  Iso.inv Iso-joinSusp-suspJoin = suspJoin→joinSusp
  Iso.rightInv Iso-joinSusp-suspJoin = suspJoin→joinSusp→suspJoin
  Iso.leftInv Iso-joinSusp-suspJoin = joinSusp→suspJoin→joinSusp

-- interaction between invSusp and toSusp
toSusp-invSusp : (A : Pointed ℓ) (x : Susp (typ A))
  → toSusp (Susp∙ (typ A)) (invSusp x) ≡ sym (toSusp (Susp∙ (typ A)) x)
toSusp-invSusp A north =
  cong (toSusp (Susp∙ (typ A))) (sym (merid (snd A)))
                  ∙∙ rCancel (merid north)
                  ∙∙ cong sym (sym (rCancel (merid north)))
toSusp-invSusp A south =
     rCancel (merid north)
   ∙∙ cong sym (sym (rCancel (merid north)))
   ∙∙ cong sym (cong (toSusp (Susp∙ (typ A))) (merid (pt A)))
toSusp-invSusp A (merid a i) j =
  lem (toSusp (Susp∙ (typ A)) north) (toSusp (Susp∙ (typ A)) south)
         (sym (rCancel (merid north)))
         (cong (toSusp (Susp∙ (typ A))) ((merid (pt A))))
         (cong (toSusp (Susp∙ (typ A))) (merid a)) (~ j) i
  where
  lem : {A : Type ℓ} {x : A} (p q : x ≡ x) (l : refl ≡ p)
        (coh r : p ≡ q)
      → PathP (λ i → (cong sym (sym l) ∙∙ l ∙∙ coh) i
                     ≡ (cong sym (sym coh) ∙∙ cong sym (sym l) ∙∙ l) i)
               (cong sym r)
               (sym r)
  lem p q =
    J (λ p l → (coh r : p ≡ q)
            → PathP (λ i → (cong sym (sym l) ∙∙ l ∙∙ coh) i
                           ≡ (cong sym (sym coh) ∙∙ cong sym (sym l) ∙∙ l) i)
                     (cong sym r)
                     (sym r))
       (J (λ q coh → (r : refl ≡ q)
                   → PathP (λ i → (refl ∙ coh) i
                           ≡ (cong sym (sym coh) ∙∙ refl ∙∙ refl) i)
                     (cong sym r)
                     (sym r))
          λ r → flipSquare (sym (rUnit refl)
                ◁ (flipSquare (sym (sym≡cong-sym r))
                ▷ rUnit refl)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- With functions are now inlined before termination checking.
module Issue59 where

open import Common.Prelude
open import Common.Equality

module Order (A : Set) (_≤_ : A → A → Bool) where

  -- This now termination checks.
  merge : List A → List A → List A
  merge [] ys = ys
  merge xs [] = xs
  merge (x ∷ xs) (y ∷ ys) with x ≤ y
  merge (x ∷ xs) (y ∷ ys)      | false = y ∷ merge (x ∷ xs) ys
  merge (x ∷ []) (y ∷ ys)      | true  = x ∷ y ∷ ys
  merge (x ∷ x₁ ∷ xs) (y ∷ ys) | true  = x ∷ merge (x₁ ∷ xs) (y ∷ ys)

data Ordering : Nat → Nat → Set where
  eq : ∀ n → Ordering n n
  lt : ∀ n d → Ordering n (n + suc d)
  gt : ∀ n d → Ordering (n + suc d) n

-- Just make sure we didn't mess anything up when there are dot patterns.
-- Andreas, 2013-11-11: But there are no recursive calls in the clauses
-- with dot patterns!

compare : ∀ n m → Ordering n m
compare zero zero = eq zero
compare zero (suc m) = lt zero m
compare (suc n) zero = gt zero n
compare (suc n) (suc m) with compare n m
compare (suc n) (suc .(n + suc d)) | lt .n d = lt (suc n) d
compare (suc .(m + suc d)) (suc m) | gt .m d = gt (suc m) d
compare (suc n) (suc .n)           | eq .n = eq (suc n)

-- Rewrite

plus-zero : ∀ n → n + 0 ≡ n
plus-zero zero = refl
plus-zero (suc n) rewrite plus-zero n = refl

plus-suc : ∀ n m → n + suc m ≡ suc n + m
plus-suc zero m = refl
plus-suc (suc n) m rewrite plus-suc n m = refl

commute : ∀ m n → m + n ≡ n + m
commute m zero = plus-zero m
commute m (suc n) rewrite plus-suc m n | commute m n = refl


text:
{-# OPTIONS --without-K #-}

{-
  Favonia:  I was trying to generalize OneSkeleton but failed
  to achieve what I wanted.  Nicolai then told me this HIT
  which is suitable for the constancy lemma I was looking for.
  This construction should be attributed to Paolo Capriotti
  and Nicolai Kraus. [1]

  [1] Eliminating Higher Truncations via Constancy
      by Paolo Capriotti and Nicolai Kraus
      (in preparation/work in progress)
-}

open import HoTT

module experimental.TwoConstancyHIT where

module _ where
  private
    data #TwoConstancy-aux {i} (A : Type i) : Type i where
      #point : A → #TwoConstancy-aux A

    data #TwoConstancy {i} (A : Type i) : Type i where
      #two-constancy : #TwoConstancy-aux A → (Unit → Unit) → #TwoConstancy A

  TwoConstancy : ∀ {i} → Type i → Type i
  TwoConstancy = #TwoConstancy

  module _ {i} {A : Type i} where

    point : A → TwoConstancy A
    point a = #two-constancy (#point a) _

    postulate  -- HIT
      link₀ : ∀ a₁ a₂ → point a₁ == point a₂

      link₁ : ∀ a₁ a₂ a₃ → link₀ a₁ a₂ ∙' link₀ a₂ a₃ == link₀ a₁ a₃

      TwoConstancy-level : is-gpd (TwoConstancy A)

    module TwoConstancyElim
      {l} {P : TwoConstancy A → Type l}
      (p : ∀ x → is-gpd (P x))
      (point* : ∀ a → P (point a))
      (link₀* : ∀ a₁ a₂ → point* a₁ == point* a₂ [ P ↓ link₀ a₁ a₂ ])
      (link₁* : ∀ a₁ a₂ a₃
        →  link₀* a₁ a₂ ∙'ᵈ link₀* a₂ a₃
        == link₀* a₁ a₃
        [ (λ p → point* a₁ == point* a₃ [ P ↓ p ]) ↓ link₁ a₁ a₂ a₃ ]) where

      f : Π (TwoConstancy A) P
      f = f-aux phantom phantom phantom where

        f-aux : Phantom p → Phantom link₀* → Phantom link₁* → Π (TwoConstancy A) P
        f-aux phantom phantom phantom (#two-constancy (#point a) _) = point* a

      postulate  -- HIT
        link₀-β : ∀ a₁ a₂ → apd f (link₀ a₁ a₂) == link₀* a₁ a₂

      private
        lemma : ∀ a₁ a₂ a₃
              → apd f (link₀ a₁ a₂ ∙' link₀ a₂ a₃)
             == link₀* a₁ a₂ ∙'ᵈ link₀* a₂ a₃
        lemma a₁ a₂ a₃ =
          apd f (link₀ a₁ a₂ ∙' link₀ a₂ a₃)
            =⟨ apd-∙' f (link₀ a₁ a₂) (link₀ a₂ a₃) ⟩
          apd f (link₀ a₁ a₂) ∙'ᵈ apd f (link₀ a₂ a₃)
            =⟨ link₀-β a₁ a₂ |in-ctx (λ u → u ∙'ᵈ apd f (link₀ a₂ a₃)) ⟩
          link₀* a₁ a₂ ∙'ᵈ apd f (link₀ a₂ a₃)
            =⟨ link₀-β a₂ a₃ |in-ctx (λ u → link₀* a₁ a₂ ∙'ᵈ u) ⟩
          link₀* a₁ a₂ ∙'ᵈ link₀* a₂ a₃
            ∎

      postulate  -- HIT
        link₁-β : ∀ a₁ a₂ a₃
                → apd (apd f) (link₁ a₁ a₂ a₃)
               == lemma a₁ a₂ a₃ ◃ (link₁* a₁ a₂ a₃ ▹! link₀-β a₁ a₃)

open TwoConstancyElim public using () renaming (f to TwoConstancy-elim)

module TwoConstancyRec
  {i} {A : Type i}
  {l} {P : Type l}
  (p : is-gpd P)
  (point* : ∀ a → P)
  (link₀* : ∀ a₁ a₂ → point* a₁ == point* a₂)
  (link₁* : ∀ a₁ a₂ a₃
            → link₀* a₁ a₂ ∙' link₀* a₂ a₃
           == link₀* a₁ a₃) where

  private
    module M = TwoConstancyElim {A = A}
      {l = l} {P = λ _ → P}
      (λ _ → p)
      point*
      (λ a₁ a₂ → ↓-cst-in (link₀* a₁ a₂))
      (λ a₁ a₂ a₃
        → ↓-cst-in-∙' (link₀ a₁ a₂) (link₀ a₂ a₃) (link₀* a₁ a₂) (link₀* a₂ a₃)
       !◃ ↓-cst-in2 (link₁* a₁ a₂ a₃))

  f : TwoConstancy A → P
  f = M.f

  link₀-β : ∀ a₁ a₂ → ap f (link₀ a₁ a₂) == link₀* a₁ a₂
  link₀-β a₁ a₂ = apd=cst-in {f = f} $ M.link₀-β a₁ a₂

  private
    lemma : ∀ a₁ a₂ a₃
          → ap f (link₀ a₁ a₂ ∙' link₀ a₂ a₃)
         == link₀* a₁ a₂ ∙' link₀* a₂ a₃
    lemma a₁ a₂ a₃ =
      ap f (link₀ a₁ a₂ ∙' link₀ a₂ a₃)
        =⟨ ap-∙' f (link₀ a₁ a₂) (link₀ a₂ a₃) ⟩
      ap f (link₀ a₁ a₂) ∙' ap f (link₀ a₂ a₃)
        =⟨ link₀-β a₁ a₂ |in-ctx (λ u → u ∙' ap f (link₀ a₂ a₃)) ⟩
      link₀* a₁ a₂ ∙' ap f (link₀ a₂ a₃)
        =⟨ link₀-β a₂ a₃ |in-ctx (λ u → link₀* a₁ a₂ ∙' u) ⟩
      link₀* a₁ a₂ ∙' link₀* a₂ a₃
        ∎

  -- I am a lazy person.
  postulate  -- HIT
    link₁-β : ∀ a₁ a₂ a₃
            → ap (ap f) (link₁ a₁ a₂ a₃)
           == (lemma a₁ a₂ a₃ ∙ link₁* a₁ a₂ a₃) ∙ (! $ link₀-β a₁ a₃)

open TwoConstancyRec public using () renaming (f to TwoConstancy-rec)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda


text:
{-# OPTIONS --cubical --safe #-}

module Cubical.Data.Strict2Group.Explicit.Interface where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Group.Base
open import Cubical.Data.Sigma
open import Cubical.Data.Strict2Group.Explicit.Base
open import Cubical.Data.Strict2Group.Explicit.Notation

module S2GInterface {ℓ : Level} ((strict2groupexp C₀ C₁ s t i ∘ si ti s∘ t∘ isMorph∘ assoc∘ lUnit∘ rUnit∘) : Strict2GroupExp ℓ) where

  open S2GBaseNotation C₀ C₁ s t i ∘ public

  module Identities1 where
    -- to be consistent with the other notation
    tarId = ti
    srcId = si
    -- identity is preserved by id
    id1₀≡1₁ : id 1₀ ≡ 1₁
    id1₀≡1₁ = morphId {G = C₀} {H = C₁} i

  open Identities1 public

  module C₁×₀C₁ where

    -- the composable morphisms as record type
    record Co : Type ℓ where
      constructor co
      field
        g f : TC₁
        coh : CohCond g f

    -- syntax
    𝓁 𝓇 : Co → TC₁
    𝓁 = Co.g
    𝓇 = Co.f
    𝒸 : (gfc : Co) → CohCond (𝓁 gfc) (𝓇 gfc)
    𝒸 = Co.coh

    -- compose a co object using ∘
    ⊙ : Co → TC₁
    ⊙ gfc = ∘ (𝓁 gfc) (𝓇 gfc) (𝒸 gfc)

    -- basically ∘, but for the sake of interfacing, we don't want to use ∘
    ⊙' : (g f : TC₁) → CohCond g f → TC₁
    ⊙' g f c = ⊙ (co g f c)

    -- interface for those names aswell
    src⊙ : (gfc : Co) → src (⊙ gfc) ≡ src (𝓇 gfc)
    src⊙ (co g f c) = s∘ g f c

    tar⊙ : (gfc : Co) → tar (⊙ gfc) ≡ tar (𝓁 gfc)
    tar⊙ (co g f c) = t∘ g f c

    src⊙' : (g f : TC₁) → (c : CohCond g f) → src (⊙' g f c) ≡ src f
    src⊙' g f c = src⊙ (co g f c)

    tar⊙' : (g f : TC₁) → (c : CohCond g f) → tar (⊙' g f c) ≡ tar g
    tar⊙' g f c = tar⊙ (co g f c)

    -- multiplication in C₁×₀C₁
    _∙Co_ : (gfc gfc' : Co) → Co
    (co g f coh) ∙Co (co g' f' coh') =
      co (g ∙₁ g') (f ∙₁ f')
        (src∙₁ g g' ∙ cong (_∙₀ src g') coh ∙ cong (tar f ∙₀_) coh' ∙ sym (tar∙₁ f f'))

    -- unit element w.r.t. ∙c. Too bad there is no \_c
    1c : Co
    1c = co 1₁ 1₁ ((cong src (sym id1₀≡1₁)) ∙∙ si 1₀ ∙∙ sym (ti 1₀) ∙ cong tar id1₀≡1₁)

    -- the interchange law reformulated using ⊙
    isMorph⊙ : (gfc gfc' : Co) → ⊙ (gfc ∙Co gfc') ≡ ⊙ gfc ∙₁ ⊙ gfc'
    isMorph⊙ (co _ _ c) (co _ _ c') = isMorph∘ c c'

    -- associator notation
    assoc⊙' : (h g f : TC₁) → (c : CohCond g f) → (c' : CohCond h g) → ⊙' (⊙' h g c') f ((src⊙' h g c') ∙ c) ≡ ⊙' h (⊙' g f c) (c' ∙ (sym (tar⊙' g f c)))
    assoc⊙' h g f c c' = assoc∘ c c'

    -- the left and right unit laws reformulated using ⊙
    lUnit⊙ : (f : TC₁) → ⊙ (co (id (tar f)) f (srcId (tar f))) ≡ f
    lUnit⊙ = lUnit∘
    rUnit⊙ : (f : TC₁) → ⊙ (co f (id (src f)) (sym (tarId (src f)))) ≡ f
    rUnit⊙ = rUnit∘

    -- the path component of f in C₁
    ΣC₁p : (f : TC₁) → Type ℓ
    ΣC₁p f = Σ[ f' ∈ TC₁ ] (f ≡ f')

    private
      -- for given g, the type of f that g can be precomposed with
      _∘* : TC₁ → Type ℓ
      g ∘* = Σ[ f ∈ TC₁ ] (CohCond g f)
      -- for given f, the type of g that f can be postcomposed with
      *∘_ : TC₁ → Type ℓ
      *∘ f = Σ[ g ∈ TC₁ ] (CohCond g f)

      -- alternate notation for ∘
      -- this is used in ∘*≡ to λ-abstract in cong
      _∘*_ : (g : TC₁) (fc : g ∘*) → TC₁
      _∘*_ g (f , c) = ∘ g f c
      _*∘_ : (f : TC₁) (gc : *∘ f) → TC₁
      _*∘_ f (g , c) = ∘ g f c

      -- since we have proof irrelevance in C₀ we can show that f ≡ f' → g∘f ≡ g∘f'
      ∘*≡ : (g : TC₁) → (fc : g ∘*) → (f'p : ΣC₁p (fst fc)) → g ∘* fc ≡ g ∘* ((fst f'p) , snd fc ∙ cong tar (snd f'p))
      ∘*≡ g fc f'p = cong (g ∘*_) (ΣPathP (snd f'p , isProp→PathP (λ j → Group.setStruc C₀ (src g) (tar (snd f'p j))) (snd fc) (snd fc ∙ cong tar (snd f'p))))
      *∘≡ : (f : TC₁) → (gc : *∘ f) → (g'p : ΣC₁p (fst gc)) → f *∘ gc ≡ f *∘ (fst g'p , ((cong src (sym (snd g'p))) ∙ snd gc))
      *∘≡ f gc g'p = cong (_*∘_ f) (ΣPathP ((snd g'p) , (isProp→PathP (λ j → Group.setStruc C₀ (src (snd g'p j)) (tar f)) (snd gc) (cong src (sym (snd g'p)) ∙ snd gc))))

    -- ⊙ respecs paths on the right
    ⊙≡ : ((co g f c) : Co) → (f'p : ΣC₁p f) → ⊙ (co g f c) ≡ ⊙ (co g (fst f'p) (c ∙ (cong tar (snd f'p))))
    ⊙≡ (co g f c) (f' , f≡f') = ∘*≡ g (f , c) (f' , f≡f')

    -- ⊙ respects paths on the left
    ≡⊙ : ((co g f c) : Co) → ((g' , g≡g') : ΣC₁p g) → ⊙ (co g f c) ≡ ⊙ (co g' f (cong src (sym g≡g') ∙ c))
    ≡⊙ (co g f c) (g' , g≡g') = *∘≡ f (g , c) (g' , g≡g')

    -- ⊙ resepcts paths on the coherence condition
    ⊙≡c : ((co g f c) : Co) → (c' : CohCond g f) → ⊙ (co g f c) ≡ ⊙ (co g f c')
    ⊙≡c (co g f c) c' = cong (λ z → ⊙ (co g f z)) (Group.setStruc C₀ (src g) (tar f) c c')

    -- implicit version of ⊙≡c
    ⊙≡c~ : {g f : TC₁} (c c' : CohCond g f) → ⊙ (co g f c) ≡ ⊙ (co g f c')
    ⊙≡c~ {g} {f} c c' = cong (λ z → ⊙ (co g f z)) (Group.setStruc C₀ (src g) (tar f) c c')

    -- ⊙ respecting paths on the left also changes the coherence condition so this should be used instead
    ≡⊙c* : {g g' f : TC₁} (c : CohCond g f) (g≡g' : g ≡ g') (c' : CohCond g' f) → ⊙' g f c ≡ ⊙' g' f c'
    ≡⊙c* {g} {g'} {f} c g≡g' c' = (≡⊙ (co g f c) (g' , g≡g')) ∙ ⊙≡c~ ((cong src (sym g≡g')) ∙ c) c'

    -- ⊙ respecting paths on the right also changes the coherence condition so this should be used instead
    ⊙≡c* : {g f f' : TC₁} (c : CohCond g f) (f≡f' : f ≡ f') (c' : CohCond g f') → ⊙' g f c ≡ ⊙' g f' c'
    ⊙≡c* {g} {f} {f'} c f≡f' c' = (⊙≡ (co g f c) (f' , f≡f')) ∙ ⊙≡c~ (c ∙ cong tar f≡f') c'

    -- use the left and right unit law with an arbitrary coherence proof c
    lUnit⊙c : (f : TC₁) → (c : CohCond (id (tar f)) f) → ⊙ (co (id (tar f)) f c) ≡ f
    lUnit⊙c f c = (⊙≡c (co (id (tar f)) f c) (srcId (tar f))) ∙ (lUnit⊙ f)
    rUnit⊙c : (f : TC₁) → (c : CohCond f (id (src f))) → ⊙ (co f (id (src f)) c) ≡ f
    rUnit⊙c f c = (⊙≡c (co f (id (src f)) c) (sym (tarId (src f)))) ∙ (rUnit⊙ f)

  open C₁×₀C₁ public

  module Identities2 where
    -- source and target of unit element
    tar1₁≡1₀ : tar 1₁ ≡ 1₀
    tar1₁≡1₀ = morphId {G = C₁} {H = C₀} t
    src1₁≡1₀ = morphId {G = C₁} {H = C₀} s

    -- taking the source is the same as the target of the identity of the source
    src≡tarIdSrc : (f : TC₁) → CohCond f (id (src f))
    src≡tarIdSrc f = sym (ti (src f))

  open Identities2 public

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
open import FRP.LTL.ISet.Core using ( ISet ; ⌈_⌉ ; ⌊_⌋ )
open import FRP.LTL.RSet using ( RSet )
open import FRP.LTL.Time using ( Time ; _≤_ )

module FRP.LTL.ISet.Future where

data Future (A : RSet) (t : Time) : Set where
  _,_ : ∀ {u} .(t≤u : t ≤ u) → A u → Future A t

◇ : ISet → ISet
◇ A = ⌈ Future ⌊ A ⌋ ⌉

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
module WarningOnUsage2 where

open import WarningOnUsage

λx→x₂ = λx→x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.FunctionSeq
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlip
open import lib.types.PushoutFmap
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Truncation
open import lib.types.Lift
open import lib.cubical.Cube
open import lib.cubical.Square

-- Suspension is defined as a particular case of pushout

module lib.types.Suspension.Core where

module _ {i} (A : Type i) where

  susp-span : Span
  susp-span = span Unit Unit A (λ _ → tt) (λ _ → tt)

  Susp : Type i
  Susp = Pushout susp-span

  -- [north'] and [south'] explictly ask for [A]

  north' : Susp
  north' = left tt

  south' : Susp
  south' = right tt

module _ {i} {A : Type i} where

  north : Susp A
  north = north' A

  south : Susp A
  south = south' A

  merid : A → north == south
  merid x = glue x

  module SuspElim {j} {P : Susp A → Type j} (n : P north)
    (s : P south) (p : (x : A) → n == s [ P ↓ merid x ]) where

    private
      module P = PushoutElim (λ _ → n) (λ _ → s) p

    abstract
      f : Π (Susp A) P
      f = P.f

      north-β : f north ↦ n
      north-β = P.left-β unit
      {-# REWRITE north-β #-}

      south-β : f south ↦ s
      south-β = P.right-β unit
      {-# REWRITE south-β #-}

      merid-β : ∀ a → apd f (merid a) == p a
      merid-β = P.glue-β

  open SuspElim public using () renaming (f to Susp-elim)

  module SuspRec {j} {C : Type j} (n s : C) (p : A → n == s) where
    private
      module P = PushoutRec {d = susp-span A} (λ _ → n) (λ _ → s) p

    abstract
      f : Susp A → C
      f = P.f

      north-β : f north ↦ n
      north-β = P.left-β unit
      {-# REWRITE north-β #-}

      south-β : f south ↦ s
      south-β = P.right-β unit
      {-# REWRITE south-β #-}

      merid-β : ∀ a → ap f (merid a) == p a
      merid-β = P.glue-β

  open SuspRec public using () renaming (f to Susp-rec)

  module SuspRecType {j} (n s : Type j) (p : A → n ≃ s)
    = PushoutRecType {d = susp-span A} (λ _ → n) (λ _ → s) p

module SuspPathElim
  {i} {j} {A : Type i} {B : Type j}
  (f g : Susp A → B)
  (n : f north == g north)
  (s : f south == g south)
  (m : ∀ a → Square n (ap f (merid a)) (ap g (merid a)) s)
  where

  private
    module M =
      SuspElim
        {P = λ sa → f sa == g sa}
        n
        s
        (λ a → ↓-='-from-square (m a))

  open M public

  merid-square-β : ∀ a → natural-square M.f (merid a) == m a
  merid-square-β a = natural-square-β M.f (merid a) (M.merid-β a)

module SuspDoublePathElim
  {i} {j} {k} {A : Type i} {B : Type j} {C : Type k}
  (f g : Susp A → Susp B → C)
  (n-n : f north north == g north north)
  (n-s : f north south == g north south)
  (s-n : f south north == g south north)
  (s-s : f south south == g south south)
  (n-m : ∀ b → Square n-n (ap (f north) (merid b)) (ap (g north) (merid b)) n-s)
  (s-m : ∀ b → Square s-n (ap (f south) (merid b)) (ap (g south) (merid b)) s-s)
  (m-n : ∀ a → Square n-n (ap (λ sa → f sa north) (merid a)) (ap (λ sa → g sa north) (merid a)) s-n)
  (m-s : ∀ a → Square n-s (ap (λ sa → f sa south) (merid a)) (ap (λ sa → g sa south) (merid a)) s-s)
  (m-m : ∀ a b →
    Cube (m-n a)
         (m-s a)
         (n-m b)
         (natural-square (λ sb → ap (λ sa → f sa sb) (merid a)) (merid b))
         (natural-square (λ sb → ap (λ sa → g sa sb) (merid a)) (merid b))
         (s-m b))
  where

  private
    module N =
      SuspElim
        {P = λ sb → f north sb == g north sb}
        n-n
        n-s
        (λ b → ↓-='-from-square (n-m b))

    n-natural-square : ∀ (b : B) →
      natural-square N.f (merid b) == n-m b
    n-natural-square b = natural-square-β N.f (merid b) (N.merid-β b)

    module S =
      SuspElim
        {P = λ sb → f south sb == g south sb}
        s-n
        s-s
        (λ b → ↓-='-from-square (s-m b))

    s-natural-square : ∀ (b : B) →
      natural-square S.f (merid b) == s-m b
    s-natural-square b = natural-square-β S.f (merid b) (S.merid-β b)

    module M (sb : Susp B) =
      SuspElim {A = A}
        {P = λ sa → f sa sb == g sa sb}
        (N.f sb)
        (S.f sb)
        (λ a → Susp-elim
          {P = λ sb → N.f sb == S.f sb [ (λ sa → f sa sb == g sa sb) ↓ merid a ]}
          (↓-='-from-square (m-n a))
          (↓-='-from-square (m-s a))
          (λ b → ap↓ ↓-='-from-square $
            cube-to-↓-square $
            cube-shift-back (! (n-natural-square b)) $
            cube-shift-front (! (s-natural-square b)) $
            m-m a b)
          sb)

  abstract
    p : ∀ sa sb → f sa sb == g sa sb
    p sa sb = M.f sb sa

    north-north-β : p north north ↦ n-n
    north-north-β = N.north-β
    {-# REWRITE north-north-β #-}

    north-south-β : p north south ↦ n-s
    north-south-β = N.south-β
    {-# REWRITE north-south-β #-}

    south-north-β : p south north ↦ s-n
    south-north-β = S.north-β
    {-# REWRITE south-north-β #-}

    south-south-β : p south south ↦ s-s
    south-south-β = S.south-β
    {-# REWRITE south-south-β #-}

    north-merid-β : ∀ b → apd (p north) (merid b) == ↓-='-from-square (n-m b)
    north-merid-β = N.merid-β

    north-merid-square-β : ∀ b → natural-square (p north) (merid b) == n-m b
    north-merid-square-β b = natural-square-β (p north) (merid b) (north-merid-β b)

    south-merid-β : ∀ b → apd (p south) (merid b) == ↓-='-from-square (s-m b)
    south-merid-β = S.merid-β

    south-merid-square-β : ∀ b → natural-square (p south) (merid b) == s-m b
    south-merid-square-β b = natural-square-β (p south) (merid b) (south-merid-β b)

    merid-north-β : ∀ a → apd (λ sa → p sa north) (merid a) == ↓-='-from-square (m-n a)
    merid-north-β = M.merid-β north

    merid-north-square-β : ∀ a → natural-square (λ sa → p sa north) (merid a) == m-n a
    merid-north-square-β a =
      natural-square-β (λ sa → p sa north) (merid a) (merid-north-β a)

    merid-south-β : ∀ a → apd (λ sa → p sa south) (merid a) == ↓-='-from-square (m-s a)
    merid-south-β = M.merid-β south

    merid-south-square-β : ∀ a → natural-square (λ sa → p sa south) (merid a) == m-s a
    merid-south-square-β a =
      natural-square-β (λ sa → p sa south) (merid a) (merid-south-β a)

susp-⊙span : ∀ {i} → Ptd i → ⊙Span
susp-⊙span X =
  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})

⊙Susp : ∀ {i} → Type i → Ptd i
⊙Susp A = ⊙[ Susp A , north ]

σloop : ∀ {i} (X : Ptd i) → de⊙ X → north' (de⊙ X) == north' (de⊙ X)
σloop ⊙[ _ , x₀ ] x = merid x ∙ ! (merid x₀)

σloop-pt : ∀ {i} {X : Ptd i} → σloop X (pt X) == idp
σloop-pt {X = ⊙[ _ , x₀ ]} = !-inv-r (merid x₀)

⊙σloop : ∀ {i} (X : Ptd i) → X ⊙→ ⊙[ north' (de⊙ X) == north' (de⊙ X) , idp ]
⊙σloop X = σloop X , σloop-pt

module _ {i j} where

  module SuspFmap {A : Type i} {B : Type j} (f : A → B) =
    SuspRec north south (merid ∘ f)

  Susp-fmap : {A : Type i} {B : Type j} (f : A → B)
    → (Susp A → Susp B)
  Susp-fmap = SuspFmap.f

  ⊙Susp-fmap : {A : Type i} {B : Type j} (f : A → B)
    → ⊙Susp A ⊙→ ⊙Susp B
  ⊙Susp-fmap f = (Susp-fmap f , idp)

module _ {i} (A : Type i) where

  Susp-fmap-idf : ∀ a → Susp-fmap (idf A) a == a
  Susp-fmap-idf = Susp-elim idp idp $ λ a →
    ↓-='-in' (ap-idf (merid a) ∙ ! (SuspFmap.merid-β (idf A) a))

  ⊙Susp-fmap-idf : ⊙Susp-fmap (idf A) ◃⊙idf =⊙∘ ⊙idf-seq
  ⊙Susp-fmap-idf = =⊙∘-in (⊙λ=' Susp-fmap-idf idp)

transport-Susp : ∀ {i} {A B : Type i} (p : A == B)
  → transport Susp p ∼ Susp-fmap (coe p)
transport-Susp {i} {A} {.A} p@idp sa = ! (Susp-fmap-idf A sa)

⊙transport-⊙Susp : ∀ {i} {A B : Type i} (p : A == B)
  → ⊙transport ⊙Susp p == ⊙Susp-fmap (coe p)
⊙transport-⊙Susp {i} {A} {.A} p@idp = ! (=⊙∘-out (⊙Susp-fmap-idf A))

module _ {i} {A : Type i} where

  Susp-fmap-cst : ∀ {j} {B : Type j} (b : B)
    (a : Susp A) → Susp-fmap (cst b) a == north
  Susp-fmap-cst b = Susp-elim idp (! (merid b)) $ (λ a →
    ↓-app=cst-from-square $ SuspFmap.merid-β (cst b) a ∙v⊡ tr-square _)

  ⊙Susp-fmap-cst : ∀ {j} {Y : Ptd j}
    → ⊙Susp-fmap {A = A} (λ _ → pt Y) == ⊙cst
  ⊙Susp-fmap-cst = ⊙λ=' (Susp-fmap-cst _) idp

Susp-fmap-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  (σ : Susp A) → Susp-fmap (g ∘ f) σ == Susp-fmap g (Susp-fmap f σ)
Susp-fmap-∘ g f = Susp-elim
  idp
  idp
  (λ a → ↓-='-in' $
    ap-∘ (Susp-fmap g) (Susp-fmap f) (merid a)
    ∙ ap (ap (Susp-fmap g)) (SuspFmap.merid-β f a)
    ∙ SuspFmap.merid-β g (f a)
    ∙ ! (SuspFmap.merid-β (g ∘ f) a))

⊙Susp-fmap-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (f : A → B)
  → ⊙Susp-fmap (g ∘ f) == ⊙Susp-fmap g ⊙∘ ⊙Susp-fmap f
⊙Susp-fmap-∘ g f = ⊙λ=' (Susp-fmap-∘ g f) idp

⊙Susp-fmap-seq : ∀ {i} {A B : Type i} → (A –→ B) → ⊙Susp A ⊙–→ ⊙Susp B
⊙Susp-fmap-seq idf-seq = ⊙idf-seq
⊙Susp-fmap-seq (f ◃∘ fs) = ⊙Susp-fmap f ◃⊙∘ ⊙Susp-fmap-seq fs

abstract
  ⊙Susp-fmap-seq-∘ : ∀ {i} {A B : Type i} (fs : A –→ B)
    → ⊙Susp-fmap (compose fs) ◃⊙idf =⊙∘ ⊙Susp-fmap-seq fs
  ⊙Susp-fmap-seq-∘ idf-seq = ⊙Susp-fmap-idf _
  ⊙Susp-fmap-seq-∘ (f ◃∘ fs) = =⊙∘-in $
    ⊙Susp-fmap (f ∘ compose fs)
      =⟨ ⊙Susp-fmap-∘ f (compose fs) ⟩
    ⊙Susp-fmap f ⊙∘ ⊙Susp-fmap (compose fs)
      =⟨ ap (⊙Susp-fmap f ⊙∘_) (=⊙∘-out (⊙Susp-fmap-seq-∘ fs)) ⟩
    ⊙Susp-fmap f ⊙∘ ⊙compose (⊙Susp-fmap-seq fs) =∎

  ⊙Susp-fmap-seq-=⊙∘ : ∀ {i} {A B : Type i} {fs gs : A –→ B}
    → fs =∘ gs
    → ⊙Susp-fmap-seq fs =⊙∘ ⊙Susp-fmap-seq gs
  ⊙Susp-fmap-seq-=⊙∘ {fs = fs} {gs = gs} p =
    ⊙Susp-fmap-seq fs
      =⊙∘⟨ !⊙∘ (⊙Susp-fmap-seq-∘ fs) ⟩
    ⊙Susp-fmap (compose fs) ◃⊙idf
      =⊙∘₁⟨ ap ⊙Susp-fmap (=∘-out p) ⟩
    ⊙Susp-fmap (compose gs) ◃⊙idf
      =⊙∘⟨ ⊙Susp-fmap-seq-∘ gs ⟩
    ⊙Susp-fmap-seq gs ∎⊙∘

{- Extract the 'glue component' of a pushout -}
module _ {i j k} {s : Span {i} {j} {k}} where

  module ExtractGlue = PushoutRec {d = s} {D = Susp (Span.C s)}
    (λ _ → north) (λ _ → south) merid

  extract-glue = ExtractGlue.f

  module _ {x₀ : Span.A s} where

    ⊙extract-glue : ⊙[ Pushout s , left x₀ ] ⊙→ ⊙[ Susp (Span.C s) , north ]
    ⊙extract-glue = extract-glue , idp

module _ {i j} {A : Type i} {B : Type j} (eq : A ≃ B) where

  Susp-emap : Susp A ≃ Susp B
  Susp-emap =
    equiv
      (Susp-fmap (–> eq))
      (Susp-fmap (<– eq))
      (λ sb →
        Susp-fmap (–> eq) (Susp-fmap (<– eq) sb)
          =⟨ ! (Susp-fmap-∘ (–> eq) (<– eq) sb) ⟩
        Susp-fmap ((–> eq) ∘ (<– eq)) sb
          =⟨ ap (λ f → Susp-fmap f sb) (λ= (<–-inv-r eq)) ⟩
        Susp-fmap (idf B) sb
          =⟨ Susp-fmap-idf _ sb ⟩
        sb =∎)
      (λ sa →
        Susp-fmap (<– eq) (Susp-fmap (–> eq) sa)
          =⟨ ! (Susp-fmap-∘ (<– eq) (–> eq) sa) ⟩
        Susp-fmap ((<– eq) ∘ (–> eq)) sa
          =⟨ ap (λ f → Susp-fmap f sa) (λ= (<–-inv-l eq)) ⟩
        Susp-fmap (idf A) sa
          =⟨ Susp-fmap-idf _ sa ⟩
        sa =∎)

  private
    -- This is to make sure that we did not screw up [Susp-emap].
    test₀ : fst Susp-emap == Susp-fmap (fst eq)
    test₀ = idp

module _ {i j} {A : Type i} {B : Type j} where

  ⊙Susp-emap : A ≃ B → ⊙Susp A ⊙≃ ⊙Susp B
  ⊙Susp-emap eq = ≃-to-⊙≃ (Susp-emap eq) idp

{- Interaction with [Lift] -}
module _ {i j} (A : Type i) where

  Susp-Lift-econv : Susp (Lift {j = j} A) ≃ Lift {j = j} (Susp A)
  Susp-Lift-econv = lift-equiv ∘e Susp-emap lower-equiv

  Susp-Lift-conv : Susp (Lift {j = j} A) == Lift {j = j} (Susp A)
  Susp-Lift-conv = ua Susp-Lift-econv

module _ {i j} (A : Type i) where

  ⊙Susp-Lift-econv : ⊙Susp (Lift {j = j} A) ⊙≃ ⊙Lift {j = j} (⊙Susp A)
  ⊙Susp-Lift-econv = ⊙lift-equiv {j = j} ⊙∘e ⊙Susp-emap {A = Lift {j = j} A} {B = A} lower-equiv

  ⊙Susp-Lift-conv : ⊙Susp (Lift {j = j} A) == ⊙Lift {j = j} (⊙Susp A)
  ⊙Susp-Lift-conv = ⊙ua ⊙Susp-Lift-econv

{- Suspension of an n-connected space is n+1-connected -}
abstract
  Susp-conn : ∀ {i} {A : Type i} {n : ℕ₋₂}
    → is-connected n A → is-connected (S n) (Susp A)
  Susp-conn {A = A} {n = n} cA = has-level-in
    ([ north ] ,
     Trunc-elim
       (Susp-elim
         idp
         (Trunc-rec (λ a → ap [_] (merid a))
                    (contr-center cA))
         (λ x → Trunc-elim
            {P = λ y → idp ==
              Trunc-rec (λ a → ap [_] (merid a)) y
              [ (λ z → [ north ] == [ z ]) ↓ (merid x) ]}
            {{λ _ → ↓-preserves-level ⟨⟩}}
            (λ x' → ↓-cst=app-in (∙'-unit-l _ ∙ mers-eq n x x'))
            (contr-center cA))))
    where
    instance _ = cA

    mers-eq : ∀ {i} {A : Type i} (n : ℕ₋₂)
      {{_ : is-connected n A}} → (x x' : A)
      → ap ([_] {n = S n}) (merid x)
        == Trunc-rec {{has-level-apply (Trunc-level {n = S n}) _ _}} (λ a → ap [_] (merid a)) [ x' ]
    mers-eq ⟨-2⟩ x x' = contr-has-all-paths _ _
    mers-eq {A = A} (S n) x x' =
      conn-extend (pointed-conn-out A x)
        (λ y → ((ap [_] (merid x) == ap [_] (merid y)) ,
                has-level-apply (has-level-apply (Trunc-level {n = S (S n)}) _ _) _ _))
        (λ _ → idp) x'

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda