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

open import Algebra.Structures.Bundles.Field
open import Algebra.Linear.Structures.Bundles

module Algebra.Linear.Space.Product
  {k ℓ} (K : Field k ℓ)
  {a₁ ℓ₁} (V₁-space : VectorSpace K a₁ ℓ₁)
  {a₂ ℓ₂} (V₂-space : VectorSpace K a₂ ℓ₂)
  where

open import Relation.Binary
open import Level using (_⊔_)
open import Data.Nat using (ℕ; zero; suc) renaming (_+_ to _+ℕ_)
open import Algebra.Linear.Structures.VectorSpace
import Algebra.FunctionProperties as FP

open VectorSpaceField K

open VectorSpace V₁-space
  using ()
  renaming
  ( Carrier       to V₁
  ; _≈_           to _≈₁_
  ; isEquivalence to ≈₁-isEquiv
  ; refl          to ≈₁-refl
  ; sym           to ≈₁-sym
  ; trans         to ≈₁-trans
  ; _+_           to _+₁_
  ; _∙_           to _∙₁_
  ; -_            to -₁_
  ; 0#            to 0₁
  ; +-identityˡ    to +₁-identityˡ
  ; +-identityʳ    to +₁-identityʳ
  ; +-identity    to +₁-identity
  ; +-cong        to +₁-cong
  ; +-assoc       to +₁-assoc
  ; +-comm        to +₁-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₁-compat
  ; ∙-+-distrib   to ∙₁-+₁-distrib
  ; ∙-+ᵏ-distrib  to ∙₁-+ᵏ-distrib
  ; ∙-cong        to ∙₁-cong
  ; ∙-identity    to ∙₁-identity
  ; ∙-absorbˡ      to ∙₁-absorbˡ
  ; ∙-absorbʳ      to ∙₁-absorbʳ
  ; -‿cong        to -₁‿cong
  ; -‿inverseˡ    to -₁‿inverseˡ
  ; -‿inverseʳ    to -₁‿inverseʳ
  )

open VectorSpace V₂-space
  using ()
  renaming
  ( Carrier       to V₂
  ; _≈_           to _≈₂_
  ; isEquivalence to ≈₂-isEquiv
  ; refl          to ≈₂-refl
  ; sym           to ≈₂-sym
  ; trans         to ≈₂-trans
  ; _+_           to _+₂_
  ; _∙_           to _∙₂_
  ; -_            to -₂_
  ; 0#            to 0₂
  ; +-identityˡ    to +₂-identityˡ
  ; +-identityʳ    to +₂-identityʳ
  ; +-identity    to +₂-identity
  ; +-cong        to +₂-cong
  ; +-assoc       to +₂-assoc
  ; +-comm        to +₂-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₂-compat
  ; ∙-+-distrib   to ∙₂-+₂-distrib
  ; ∙-+ᵏ-distrib  to ∙₂-+ᵏ-distrib
  ; ∙-cong        to ∙₂-cong
  ; ∙-identity    to ∙₂-identity
  ; ∙-absorbˡ      to ∙₂-absorbˡ
  ; ∙-absorbʳ      to ∙₂-absorbʳ
  ; -‿cong        to -₂‿cong
  ; -‿inverseˡ    to -₂‿inverseˡ
  ; -‿inverseʳ    to -₂‿inverseʳ
  )

open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent

private
  V : Set (a₁ ⊔ a₂)
  V = V₁ × V₂

_≈_ : Rel V (ℓ₁ ⊔ ℓ₂)
_≈_ = Pointwise _≈₁_ _≈₂_

≈-isEquiv : IsEquivalence _≈_
≈-isEquiv = ×-isEquivalence ≈₁-isEquiv ≈₂-isEquiv

prod-setoid : Setoid (a₁ ⊔ a₂) (ℓ₁ ⊔ ℓ₂)
prod-setoid = record
  { Carrier       = V
  ; _≈_           = _≈_
  ; isEquivalence = ≈-isEquiv
  }

open IsEquivalence ≈-isEquiv renaming
  ( refl  to ≈-refl
  ; sym   to ≈-sym
  ; trans to ≈-trans
  )

open import Algebra.FunctionProperties _≈_
open import Algebra.Structures _≈_

0# : V
0# = (0₁ , 0₂)

-_ : Op₁ V
- (x₁ , x₂) = (-₁ x₁ , -₂ x₂)

infixr 25 _+_
_+_ : Op₂ V
(x₁ , x₂) + (y₁ , y₂) = (x₁ +₁ y₁ , x₂ +₂ y₂)

infixr 30 _∙_
_∙_ : K' -> V -> V
k ∙ (x₁ , x₂) = (k ∙₁ x₁ , k ∙₂ x₂)

+-cong : Congruent₂ _+_
+-cong (r₁ , r₂) (s₁ , s₂) = ( +₁-cong r₁ s₁ , +₂-cong r₂ s₂ )

+-assoc : Associative _+_
+-assoc (x₁ , x₂) (y₁ , y₂) (z₁ , z₂) = ( +₁-assoc x₁ y₁ z₁ , +₂-assoc x₂ y₂ z₂ )

+-identityˡ : LeftIdentity 0# _+_
+-identityˡ (x₁ , x₂) = ( +₁-identityˡ x₁ , +₂-identityˡ x₂ )

+-identityʳ : RightIdentity 0# _+_
+-identityʳ (x₁ , x₂) = ( +₁-identityʳ x₁ , +₂-identityʳ x₂ )

+-identity : Identity 0# _+_
+-identity = +-identityˡ , +-identityʳ

+-comm : Commutative _+_
+-comm (x₁ , x₂) (y₁ , y₂) = ( +₁-comm x₁ y₁ , +₂-comm x₂ y₂ )

*ᵏ-∙-compat : ∀ (a b : K') (u : V) -> ((a *ᵏ b) ∙ u) ≈ (a ∙ (b ∙ u))
*ᵏ-∙-compat a b (x₁ , x₂) = ( *ᵏ-∙₁-compat a b x₁ , *ᵏ-∙₂-compat a b x₂ )

∙-+-distrib : ∀ (a : K') (u v : V) -> (a ∙ (u + v)) ≈ ((a ∙ u) + (a ∙ v))
∙-+-distrib a (x₁ , x₂) (y₁ , y₂) = ( ∙₁-+₁-distrib a x₁ y₁ , ∙₂-+₂-distrib a x₂ y₂ )

∙-+ᵏ-distrib : ∀ (a b : K') (u : V) -> ((a +ᵏ b) ∙ u) ≈ ((a ∙ u) + (b ∙ u))
∙-+ᵏ-distrib a b  (x₁ , x₂) = ( ∙₁-+ᵏ-distrib a b x₁ , ∙₂-+ᵏ-distrib a b x₂ )

∙-cong : ∀ {a b : K'} {u v : V} -> a ≈ᵏ b -> u ≈ v -> (a ∙ u) ≈ (b ∙ v)
∙-cong rₓ (r₁ , r₂) = ( ∙₁-cong rₓ r₁ , ∙₂-cong rₓ r₂ )

∙-identity : ∀ (x : V) → (1ᵏ ∙ x) ≈ x
∙-identity (x₁ , x₂) = ( ∙₁-identity x₁ , ∙₂-identity x₂ )

∙-absorbˡ : ∀ (x : V) → (0ᵏ ∙ x) ≈ 0#
∙-absorbˡ (x₁ , x₂) = ( ∙₁-absorbˡ x₁ , ∙₂-absorbˡ x₂ )

-‿inverseˡ : LeftInverse 0# -_ _+_
-‿inverseˡ (x₁ , x₂) = ( -₁‿inverseˡ x₁ , -₂‿inverseˡ x₂ )

-‿inverseʳ : RightInverse 0# -_ _+_
-‿inverseʳ (x₁ , x₂) = ( -₁‿inverseʳ x₁ , -₂‿inverseʳ x₂ )

-‿inverse : Inverse 0# -_ _+_
-‿inverse = -‿inverseˡ , -‿inverseʳ

-‿cong : Congruent₁ -_
-‿cong  (x₁ , x₂) = ( -₁‿cong x₁ , -₂‿cong x₂ )

isMagma : IsMagma _+_
isMagma = record
  { isEquivalence = ≈-isEquiv
  ; ∙-cong        = +-cong
  }

isSemigroup : IsSemigroup _+_
isSemigroup = record
  { isMagma = isMagma
  ; assoc   = +-assoc
  }

isMonoid : IsMonoid _+_ 0#
isMonoid = record
  { isSemigroup = isSemigroup
  ; identity    = +-identity
  }

isGroup : IsGroup _+_ 0# -_
isGroup = record
  { isMonoid = isMonoid
  ; inverse  = -‿inverse
  ; ⁻¹-cong   = -‿cong
  }

isAbelianGroup : IsAbelianGroup _+_ 0# -_
isAbelianGroup = record
  { isGroup = isGroup
  ; comm    = +-comm
  }

isVectorSpace : IsVectorSpace K _≈_ _+_ _∙_ -_ 0#
isVectorSpace = record
  { isAbelianGroup = isAbelianGroup
  ; *ᵏ-∙-compat      = *ᵏ-∙-compat
  ; ∙-+-distrib      = ∙-+-distrib
  ; ∙-+ᵏ-distrib     = ∙-+ᵏ-distrib
  ; ∙-cong           = ∙-cong
  ; ∙-identity       = ∙-identity
  ; ∙-absorbˡ         = ∙-absorbˡ
  }

vectorSpace : VectorSpace K (a₁ ⊔ a₂)  (ℓ₁ ⊔ ℓ₂)
vectorSpace = record { isVectorSpace = isVectorSpace }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
import      LibraBFT.Concrete.Properties.PreferredRound as PR

open import LibraBFT.Concrete.Obligations

-- In this module, we (will) prove the implementation obligation for the PreferredRound rule.

module LibraBFT.Impl.Properties.PreferredRound where

  postulate  -- TODO-3 : prove.  Note that this is a substantial
             -- undertaking that should not be started before we have
             -- a proof for the similar-but-much-simpler VotesOnce
             -- property, and also not before we have an
             -- implementation (perhaps some incremental extension of
             -- our current fake/simple implementaion) that we can
             -- reasonably hope actually ensures the property!
    pr₁ : PR.ImplObligation₁

ext: agda

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Gysin where

open import Cubical.Foundations.Path
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed.Homogeneous

open import Cubical.Functions.Embedding

open import Cubical.Relation.Nullary

open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Fin

open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int

open import Cubical.HITs.Truncation as T
open import Cubical.HITs.SetTruncation as ST
open import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.Pushout.Flattening
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.S1 renaming (_·_ to _*_)
open import Cubical.HITs.Join

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Hopf
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.RingLaws
open import Cubical.ZCohomology.RingStructure.GradedCommutativity

open PlusBis

-- There seems to be some problems with the termination checker.
-- Spelling out integer induction with 3 base cases like this
-- solves the issue.
private
  Int-ind : ∀ {ℓ} (P : ℤ → Type ℓ)
          → P (pos zero) → P (pos 1)
          → P (negsuc zero)
          → ((x y : ℤ) → P x → P y → P (x + y)) → (x : ℤ) → P x
  Int-ind P z one min ind (pos zero) = z
  Int-ind P z one min ind (pos (suc zero)) = one
  Int-ind P z one min ind (pos (suc (suc n))) =
    ind (pos (suc n)) 1  (Int-ind P z one min ind (pos (suc n))) one
  Int-ind P z one min ind (negsuc zero) = min
  Int-ind P z one min ind (negsuc (suc n)) =
    ind (negsuc n) (negsuc zero) (Int-ind P z one min ind (negsuc n)) min

-- The untruncated version (coHomRed n (S₊ n)), i.e.
-- (S₊∙ n →∙ coHomK-ptd n) is in fact equal to
-- (coHomRed n (S₊ n)). Its useful to formulate
-- (S₊∙ n →∙ coHomK-ptd n) as a group in its own right
-- and prove it equivalent to (coHomRed n (S₊ n)).

-- We start with the addition
private
  _++_ : ∀ {ℓ} {A : Pointed ℓ} {n : ℕ} →
        (A →∙ coHomK-ptd n) → (A →∙ coHomK-ptd n) → (A →∙ coHomK-ptd n)
  fst (f ++ g) x = fst f x +ₖ fst g x
  snd (f ++ g) = cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ _ (0ₖ _)

-- If we truncate the addition, we get back our usual
-- addition on (coHomRed n (S₊ n))
addAgree : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (x y : A →∙ coHomK-ptd n)
         → Path (fst (coHomRedGrDir n A))
                 ∣ x ++ y ∣₂
                 (∣ x ∣₂ +ₕ∙ ∣ y ∣₂)
addAgree {A = A} zero f g =
  cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _) refl)
addAgree {A = A} (suc zero) f g =
  cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _) refl)
addAgree {A = A} (suc (suc n)) f g =
  cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _) refl)

-- We formulate (S₊∙ n →∙ coHomK-ptd n) as a group, πS.
module _ where
  open import Cubical.Algebra.Monoid
  open import Cubical.Algebra.Semigroup
  open GroupStr
  open IsGroup
  open IsMonoid
  open IsSemigroup
  πS : (n : ℕ) → Group ℓ-zero
  fst (πS n) = S₊∙ n →∙ coHomK-ptd n
  1g (snd (πS n)) = (λ _ → 0ₖ n) , refl
  GroupStr._·_ (snd (πS n)) f g = (λ x → fst f x +ₖ fst g x)
                                  , cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ n (0ₖ n)
  inv (snd (πS n)) f = (λ x → -ₖ fst f x) , cong -ₖ_ (snd f) ∙ -0ₖ {n = n}
  isGroup (snd (πS n)) = makeIsGroup
                         (helper n)
                         (λ x y z → →∙Homogeneous≡
                                     (isHomogeneousKn n)
                                     (funExt λ w → assocₖ n (fst x w) (fst y w) (fst z w)))
                         (λ { (f , p) → →∙Homogeneous≡ (isHomogeneousKn n) (funExt λ x → rUnitₖ n (f x)) })
                         (λ { (f , p) → →∙Homogeneous≡ (isHomogeneousKn n) (funExt λ x → lUnitₖ n (f x)) })
                         (λ { (f , p) → →∙Homogeneous≡ (isHomogeneousKn n) (funExt λ x → rCancelₖ n (f x)) })
                         (λ { (f , p) → →∙Homogeneous≡ (isHomogeneousKn n) (funExt λ x → lCancelₖ n (f x)) })
          where
          helper : (n : ℕ) → isSet (S₊∙ n →∙ coHomK-ptd n)
          helper zero = isOfHLevelΣ 2 (isSetΠ (λ _ → isSetℤ))  λ _ → isOfHLevelPath 2 isSetℤ _ _
          helper (suc n) = isOfHLevel↑∙' 0 n

  isSetπS : (n : ℕ) → isSet (S₊∙ n →∙ coHomK-ptd n)
  isSetπS = λ n → is-set (snd (πS n))

-- πS is equivalent to (coHomRed n (S₊∙ n))
K : (n : ℕ) → GroupIso (coHomRedGrDir n (S₊∙ n)) (πS n)
fst (K n) = setTruncIdempotentIso (isSetπS n)
snd (K zero) =
  makeIsGroupHom
    (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSetπS 0) _ _)
      λ f g → →∙Homogeneous≡ (isHomogeneousKn 0) refl)
snd (K (suc zero)) =
    makeIsGroupHom
    (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSetπS 1) _ _)
      λ f g → →∙Homogeneous≡ (isHomogeneousKn 1) refl)
snd (K (suc (suc n))) =
    makeIsGroupHom
    (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSetπS _) _ _)
      λ f g → →∙Homogeneous≡ (isHomogeneousKn _) refl)

-- πS has the following generator
genFunSpace : (n : ℕ) → S₊∙ n →∙ coHomK-ptd n
fst (genFunSpace zero) false = 1
fst (genFunSpace zero) true = 0
snd (genFunSpace zero) = refl
fst (genFunSpace (suc n)) = ∣_∣
snd (genFunSpace (suc zero)) = refl
snd (genFunSpace (suc (suc n))) = refl

πS≅ℤ : (n : ℕ) → GroupIso (πS n) ℤGroup
fst (πS≅ℤ zero) = IsoBool→∙
snd (πS≅ℤ zero) = makeIsGroupHom λ _ _ → refl
πS≅ℤ (suc n) =
  compGroupIso
    (invGroupIso (K (suc n)))
    (compGroupIso
      (GroupEquiv→GroupIso (coHomGr≅coHomRedGr n (S₊∙ (suc n))))
      (Hⁿ-Sⁿ≅ℤ n))

Iso-πS-ℤ : (n : ℕ) → Iso (S₊∙ (suc n) →∙ coHomK-ptd (suc n)) ℤ
Iso-πS-ℤ n = compIso (invIso (setTruncIdempotentIso (isOfHLevel↑∙' 0 n)))
               (compIso (equivToIso (fst (coHomGr≅coHomRedGr n (S₊∙ (suc n)))))
               (fst (Hⁿ-Sⁿ≅ℤ n)))

Iso-πS-ℤ' : (n : ℕ) → Iso (S₊∙ n →∙ coHomK-ptd n) ℤ
Iso-πS-ℤ' n = fst (πS≅ℤ n)

Iso-πS-ℤPres1 : (n : ℕ) → Iso.fun (fst (πS≅ℤ (suc n))) (∣_∣ , refl) ≡ pos 1
Iso-πS-ℤPres1 zero = refl
Iso-πS-ℤPres1 (suc n) =
  cong (Iso.fun (fst (Hⁿ-Sⁿ≅ℤ n))) (lem n) ∙ Iso-πS-ℤPres1 n
  where
  lem : (n : ℕ) → Iso.fun (fst (suspensionAx-Sn n n)) ∣ ∣_∣ ∣₂ ≡ ∣ ∣_∣ ∣₂
  lem zero =
    cong ∣_∣₂ (funExt λ x → transportRefl (∣ x ∣ +ₖ (0ₖ 1)) ∙ rUnitₖ 1 ∣ x ∣)
  lem (suc n) = cong ∣_∣₂
    (funExt λ x → (λ i → transportRefl ((ΩKn+1→Kn (suc (suc n))
       (transp (λ j → 0ₖ (suc (suc (suc n))) ≡ ∣ merid north (~ j ∧ ~ i) ∣) i
        (λ z → ∣ compPath-filler
                  (merid (transportRefl (transportRefl x i) i))
                  (sym (merid north)) i z
           ∣)))) i)
    ∙ Iso.leftInv (Iso-Kn-ΩKn+1 (suc (suc n))) ∣ x ∣)

-- The first step of the Gysin sequence is to formulate
-- an equivalence g : Kᵢ ≃ (Sⁿ →∙ Kᵢ₊ₙ)
module g-base where
  g : (n : ℕ) (i : ℕ) → coHomK i → (S₊∙ n →∙ coHomK-ptd (i +' n))
  fst (g n i x) y = x ⌣ₖ (genFunSpace n) .fst y
  snd (g n i x) = cong (x ⌣ₖ_) ((genFunSpace n) .snd) ∙ ⌣ₖ-0ₖ i n x

  -- We give another version of g which will be easier to work with now
  G : (n : ℕ) (i : ℕ) → coHomK i → (S₊∙ n →∙ coHomK-ptd (n +' i))
  fst (G n i x) y = (genFunSpace n) .fst y ⌣ₖ x
  snd (G n i x) = cong (_⌣ₖ x) ((genFunSpace n) .snd) ∙ 0ₖ-⌣ₖ n i x

  -ₖ'^-Iso : (n : ℕ) (i : ℕ)
    → (S₊∙ n →∙ coHomK-ptd (i +' n)) ≃ (S₊∙ n →∙ coHomK-ptd (i +' n))
  -ₖ'^-Iso n i = isoToEquiv (iso F F FF FF)
    where
    lem : (i n : ℕ) → (-ₖ'^ i · n) (snd (coHomK-ptd (i +' n))) ≡ 0ₖ _
    lem zero zero = refl
    lem zero (suc zero) = refl
    lem zero (suc (suc n)) = refl
    lem (suc zero) zero = refl
    lem (suc (suc i)) zero = refl
    lem (suc i) (suc n) = refl

    F : S₊∙ n →∙ coHomK-ptd (i +' n) → S₊∙ n →∙ coHomK-ptd (i +' n)
    fst (F f) x = (-ₖ'^ i · n) (fst f x)
    snd (F f) = cong (-ₖ'^ i · n) (snd f) ∙ lem i n

    FF : (x : _) → F (F x) ≡ x
    FF x =
      →∙Homogeneous≡ (isHomogeneousKn _)
        (funExt λ y → -ₖ'-gen² i n _ _ (fst x y))

  transpPres0ₖ : ∀ {k m : ℕ} (p : k ≡ m) → subst coHomK p (0ₖ k) ≡ 0ₖ m
  transpPres0ₖ {k = k} =
    J (λ m p → subst coHomK p (0ₖ k) ≡ 0ₖ m) (transportRefl _)

  -- There will be some index swapping going on. We state this explicitly, since we will
  -- need to trace the maps later
  indexSwap : (n : ℕ) (i : ℕ)
    → (S₊∙ n →∙ coHomK-ptd (n +' i))
     ≃ (S₊∙ n →∙ coHomK-ptd (i +' n))
  indexSwap n i =
    isoToEquiv (iso (λ f → (λ x → subst coHomK (+'-comm n i) (fst f x)) ,
      cong (subst coHomK (+'-comm n i)) (snd f) ∙ transpPres0ₖ (+'-comm n i))
      (λ f → (λ x → subst coHomK (sym (+'-comm n i)) (fst f x))
            , (cong (subst coHomK (sym (+'-comm n i))) (snd f)
                    ∙ transpPres0ₖ (sym (+'-comm n i))))
      (λ f → →∙Homogeneous≡ (isHomogeneousKn _)
                (funExt λ x → transportTransport⁻ _ (f .fst x)))
      λ f → →∙Homogeneous≡ (isHomogeneousKn _)
                (funExt λ x → transportTransport⁻ _ (f .fst x)))

  -- g is a composition of G and our two previous equivs.
  g≡ : (n : ℕ) (i : ℕ) → g n i ≡ λ x
    → fst (compEquiv (indexSwap n i) (-ₖ'^-Iso n i)) ((G n i) x)
  g≡ n i = funExt (λ f → →∙Homogeneous≡ (isHomogeneousKn _)
             (funExt λ y → gradedComm'-⌣ₖ _ _ f (genFunSpace n .fst y)))

  -- We need a third Iso.

  suspKn-Iso-fun : (n m : ℕ) →
    (S₊∙ (suc n) →∙ coHomK-ptd (suc m))
        → (S₊ n → coHomK m)
  suspKn-Iso-fun zero m (f , p) false = ΩKn+1→Kn _ (sym p ∙∙ cong f loop ∙∙ p)
  suspKn-Iso-fun zero m (f , p) true = 0ₖ _
  suspKn-Iso-fun (suc n) m (f , p) x =
    ΩKn+1→Kn _ (sym p ∙∙ cong f (merid x ∙ sym (merid (ptSn _))) ∙∙ p)

  suspKn-Iso-fun∙ : (n m : ℕ) → (f : _) → suspKn-Iso-fun n m f (ptSn _) ≡ 0ₖ m
  suspKn-Iso-fun∙ zero m = λ _ → refl
  suspKn-Iso-fun∙ (suc n) m (f , p) =
    cong (ΩKn+1→Kn m)
      (cong (sym p ∙∙_∙∙ p) (cong (cong f) (rCancel (merid (ptSn _)))))
     ∙∙ cong (ΩKn+1→Kn m) (∙∙lCancel p)
     ∙∙ ΩKn+1→Kn-refl m

  suspKn-Iso-inv : (n m : ℕ) → (S₊∙ n →∙ coHomK-ptd m)
    → (S₊∙ (suc n) →∙ coHomK-ptd (suc m))
  fst (suspKn-Iso-inv zero m (f , p)) base = 0ₖ _
  fst (suspKn-Iso-inv zero m (f , p)) (loop i) = Kn→ΩKn+1 m (f false) i
  snd (suspKn-Iso-inv zero m (f , p)) = refl
  fst (suspKn-Iso-inv (suc n) m (f , p)) north = 0ₖ _
  fst (suspKn-Iso-inv (suc n) m (f , p)) south = 0ₖ _
  fst (suspKn-Iso-inv (suc n) m (f , p)) (merid a i) = Kn→ΩKn+1 m (f a) i
  snd (suspKn-Iso-inv (suc n) m (f , p)) = refl

  suspKn-Iso : (n m : ℕ) →
    Iso (S₊∙ (suc n) →∙ coHomK-ptd (suc m))
        (S₊∙ n →∙ coHomK-ptd m)
  Iso.fun (suspKn-Iso n m) f = (suspKn-Iso-fun n m f)
                             , (suspKn-Iso-fun∙ n m f)
  Iso.inv (suspKn-Iso n m) = suspKn-Iso-inv n m
  Iso.rightInv (suspKn-Iso zero m) (f , p) =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ { false → cong (ΩKn+1→Kn m) (sym (rUnit _))
                         ∙ Iso.leftInv (Iso-Kn-ΩKn+1 _) (f false)
                ; true → sym p})
  Iso.rightInv (suspKn-Iso (suc n) m) (f , p) =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ x →
         (λ i → ΩKn+1→Kn m
           (sym (rUnit
             (cong-∙
               (suspKn-Iso-inv (suc n) m (f , p) .fst)
                 (merid x) (sym (merid (ptSn _))) i)) i))
      ∙∙ cong (ΩKn+1→Kn m)
          (cong (Kn→ΩKn+1 m (f x) ∙_)
            (cong sym (cong (Kn→ΩKn+1 m) p ∙ Kn→ΩKn+10ₖ m))
             ∙ sym (rUnit _))
      ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 _)  (f x))
  Iso.leftInv (suspKn-Iso zero m) (f , p) = →∙Homogeneous≡ (isHomogeneousKn _)
    (funExt λ { base → sym p
              ; (loop i) j → lem j i})
    where
    lem : PathP (λ i → p (~ i) ≡ p (~ i))
               (Kn→ΩKn+1 m (ΩKn+1→Kn m (sym p ∙∙ cong f loop ∙∙ p)))
               (cong f loop)
    lem = Iso.rightInv (Iso-Kn-ΩKn+1 _) _
      ◁ λ i → doubleCompPath-filler (sym p) (cong f loop) p (~ i)
  Iso.leftInv (suspKn-Iso (suc n) m) (f , p) =
    →∙Homogeneous≡ (isHomogeneousKn _)
     (funExt λ { north → sym p
               ; south → sym p ∙ cong f (merid (ptSn _))
               ; (merid a i) j → lem a j i})
    where
    lem : (a : S₊ (suc n))
      → PathP (λ i → p (~ i) ≡ (sym p ∙ cong f (merid (ptSn (suc n)))) i)
               (Kn→ΩKn+1 m
                 (ΩKn+1→Kn m
                   (sym p ∙∙ cong f (merid a ∙ sym (merid (ptSn _))) ∙∙ p)))
               (cong f (merid a))
    lem a = Iso.rightInv (Iso-Kn-ΩKn+1 _) _
        ◁ λ i j → hcomp (λ k →
             λ { (i = i1) → (f (merid a j))
               ; (j = i0) → p (k ∧ ~ i)
               ; (j = i1) → compPath-filler'
                              (sym p) (cong f (merid (ptSn _))) k i })
               (f (compPath-filler (merid a) (sym (merid (ptSn _))) (~ i) j))

  glIsoInvHom : (n m : ℕ) (x y : coHomK n) (z : S₊ (suc m))
    → Iso.inv (suspKn-Iso _ _) (G m n (x +ₖ y)) .fst z
    ≡ Iso.inv (suspKn-Iso _ _) (G m n x) .fst z
    +ₖ Iso.inv (suspKn-Iso _ _) (G m n y) .fst z
  glIsoInvHom zero zero x y base = refl
  glIsoInvHom (suc n) zero x y base = refl
  glIsoInvHom zero zero x y (loop i) j = lem j i
    where
    lem : (cong (Iso.inv (suspKn-Iso _ _) (G zero zero (x + y)) .fst) loop)
        ≡ cong₂ _+ₖ_ (cong (Iso.inv (suspKn-Iso _ _) (G zero zero x) .fst) loop)
                     (cong (Iso.inv (suspKn-Iso _ _) (G zero zero y) .fst) loop)
    lem = Kn→ΩKn+1-hom 0 x y
     ∙ ∙≡+₁ (cong (Iso.inv (suspKn-Iso _ _) (G zero zero x) .fst) loop)
            (cong (Iso.inv (suspKn-Iso _ _) (G zero zero y) .fst) loop)
  glIsoInvHom (suc n) zero x y (loop i) j = lem j i
    where
    lem : Kn→ΩKn+1 (suc n) ((pos (suc zero)) ·₀ (x +ₖ y))
      ≡ cong₂ _+ₖ_ (cong (Iso.inv (suspKn-Iso zero (zero +' suc n))
                         (G zero (suc n) x) .fst) loop)
                   (cong (Iso.inv (suspKn-Iso zero (zero +' suc n))
                         (G zero (suc n) y) .fst) loop)
    lem = cong (Kn→ΩKn+1 (suc n)) (lUnit⌣ₖ _ (x +ₖ y))
     ∙∙ Kn→ΩKn+1-hom (suc n) x y
     ∙∙ (λ i → ∙≡+₂ n (Kn→ΩKn+1 (suc n) (lUnit⌣ₖ _ x (~ i)))
                       (Kn→ΩKn+1 (suc n) (lUnit⌣ₖ _ y (~ i))) i)
  glIsoInvHom zero (suc m) x y north = refl
  glIsoInvHom zero (suc m) x y south = refl
  glIsoInvHom zero (suc m) x y (merid a i) j = lem j i
    where
    lem : Kn→ΩKn+1 (suc m) (_⌣ₖ_ {n = suc m} {m = zero} ∣ a ∣ (x + y))
      ≡ cong₂ _+ₖ_ (Kn→ΩKn+1 (suc m) (_⌣ₖ_ {n = suc m} {m = zero} ∣ a ∣ x))
                   (Kn→ΩKn+1 (suc m) (_⌣ₖ_ {n = suc m} {m = zero} ∣ a ∣ y))
    lem = cong (Kn→ΩKn+1 (suc m)) (leftDistr-⌣ₖ (suc m) 0 ∣ a ∣ x y)
     ∙∙ Kn→ΩKn+1-hom (suc m) _ _
     ∙∙ ∙≡+₂ _ _ _
  glIsoInvHom (suc n) (suc m) x y north = refl
  glIsoInvHom (suc n) (suc m) x y south = refl
  glIsoInvHom (suc n) (suc m) x y (merid a i) j = lem j i
    where
    lem : Kn→ΩKn+1 (suc (suc (m +ℕ n)))
                   (_⌣ₖ_ {n = suc m} {m = suc n} ∣ a ∣ (x +ₖ y))
      ≡ cong₂ _+ₖ_ (Kn→ΩKn+1 (suc (suc (m +ℕ n)))
                     (_⌣ₖ_ {n = suc m} {m = suc n} ∣ a ∣ x))
                   (Kn→ΩKn+1 (suc (suc (m +ℕ n)))
                     (_⌣ₖ_ {n = suc m} {m = suc n} ∣ a ∣ y))
    lem = cong (Kn→ΩKn+1 (suc (suc (m +ℕ n))))
             (leftDistr-⌣ₖ (suc m) (suc n) ∣ a ∣ x y)
     ∙∙ Kn→ΩKn+1-hom _ _ _
     ∙∙ ∙≡+₂ _ _ _

  private
    +'-suc : (n m : ℕ) → suc n +' m ≡ suc (n +' m)
    +'-suc zero zero = refl
    +'-suc (suc n) zero = refl
    +'-suc zero (suc m) = refl
    +'-suc (suc n) (suc m) = refl

  decomposeG : (i n : ℕ) (x : coHomK i)
    → G (suc n) i x
     ≡ subst (λ x → S₊∙ (suc n) →∙ coHomK-ptd x)
              (sym (+'-suc n i))
              (Iso.inv (suspKn-Iso n _) (G n i x))
  decomposeG zero zero x =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ z → (λ i → x ·₀ ∣ z ∣) ∙ h3 x z ∙ sym (transportRefl _))
      where
      h3 : (x : ℤ) (z : S¹)
        → _·₀_ {n = 1} x ∣ z ∣
          ≡ fst (Iso.inv (suspKn-Iso 0 zero) (G zero zero x)) z
      h3 =
        Int-ind _
          (λ { base → refl ; (loop i) j → Kn→ΩKn+10ₖ zero (~ j) i})
          (λ { base → refl ; (loop i) j → rUnit (cong ∣_∣ₕ (lUnit loop j)) j i})
          (λ { base → refl ; (loop i) j → rUnit (cong ∣_∣ₕ (sym loop)) j i})
          λ x y inx iny z
            → rightDistr-⌣ₖ 0 1 x y ∣ z ∣
            ∙∙ cong₂ _+ₖ_ (inx z) (iny z)
            ∙∙ sym (glIsoInvHom zero zero x y z)
  decomposeG (suc i) zero x =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ z → lem z
            ∙ sym (transportRefl
               ((Iso.inv (suspKn-Iso zero (suc i)) (G zero (suc i) x)) .fst z)))
    where
    lem : (z : S₊ 1)
      → _ ≡ Iso.inv (suspKn-Iso zero (suc i)) (G zero (suc i) x) .fst z
    lem base = refl
    lem (loop k) j = Kn→ΩKn+1 (suc i) (lUnit⌣ₖ _ x (~ j)) k
  decomposeG zero (suc n) x =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ z → main x z
        ∙ λ i → transportRefl
                  (Iso.inv (suspKn-Iso (suc n) (suc n))
                           (G (suc n) zero x)) (~ i) .fst z)
      where
      +merid : rUnitₖ (suc (suc n)) ∣ south ∣ ≡ cong ∣_∣ₕ (merid (ptSn _))
      +merid = sym (lUnit _)
             ∙ cong (cong ∣_∣ₕ)
             λ j i → transp (λ _ → S₊ (suc (suc n))) (i ∨ j)
                             (merid (ptSn (suc n)) i)

      lem : (a : S₊ (suc n))
        → PathP (λ i → ∣ merid a i ∣ₕ
                       ≡ Kn→ΩKn+1 (suc n) (∣ a ∣ +ₖ (0ₖ _)) i)
                 refl (sym (rUnitₖ (suc (suc n)) ∣ south ∣))
      lem a =
        flipSquare ((λ i j → ∣ compPath-filler (merid a)
                                 (sym (merid (ptSn _))) i j ∣ₕ)
              ▷ cong (Kn→ΩKn+1 (suc n)) (sym (rUnitₖ (suc n) ∣ a ∣ₕ)))
            ▷ sym (cong sym +merid)

      lem₂ : (a : S₊ (suc n)) → (λ i → -ₖ ∣ merid a i ∣)
                               ≡ Kn→ΩKn+1 (suc n) (-ₖ ∣ a ∣)
      lem₂ a =
        cong (cong ∣_∣ₕ) (sym (symDistr (merid a)
                       (sym (merid (ptSn (suc n))))))
            ∙ sym (Kn→ΩKn+1-ₖ (suc n) ∣ a ∣)

      main : (x : ℤ) (z : S₊ (suc (suc n)))
       → _⌣ₖ_ {n = suc (suc n)} {m = 0} ∣ z ∣ x
        ≡ Iso.inv (suspKn-Iso (suc n) (suc n)) (G (suc n) zero x) .fst z
      main = Int-ind _
            (λ { north → refl ; south → refl
              ; (merid a i) j → Kn→ΩKn+10ₖ (suc n) (~ j) i})
            (λ { north → refl ; south → refl
               ; (merid a i) j →
                 hcomp (λ k →
                    λ { (i = i0) → ∣ north ∣
                      ; (i = i1) → rUnitₖ (suc (suc n)) ∣ south ∣ (~ k)
                      ; (j = i0) → rUnitₖ (suc (suc n)) ∣ merid a i ∣ (~ k)
                      ; (j = i1) → lem a i k})
                      ∣ merid a i ∣ₕ})
            (λ { north → refl
               ; south → refl
               ; (merid a i) j → lem₂ a j i})
            λ x y indx indy z → leftDistr-⌣ₖ _ _ ∣ z ∣ x y
                               ∙ cong₂ _+ₖ_ (indx z) (indy z)
                               ∙ sym (glIsoInvHom _ _ _ _ _)
  decomposeG (suc i) (suc n) x =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ z → lem z
         ∙ λ j →
           transportRefl ((Iso.inv (suspKn-Iso (suc n) (suc (suc (n +ℕ i))))
                     (G (suc n) (suc i) x))) (~ j) .fst z)
    where
    lem : (z : S₊ (suc (suc n))) → _
    lem north = refl
    lem south = refl
    lem (merid a i) = refl

  isEquivGzero : (i : ℕ) → isEquiv (G zero i)
  isEquivGzero i =
    isoToIsEquiv
      (iso _ (λ f → fst f false)
        (λ {(f , p) → →∙Homogeneous≡ (isHomogeneousKn _)
              (funExt λ { false → rUnitₖ _ (f false) ; true → sym p})})
        (lUnit⌣ₖ _))

  isEquivG : (n i : ℕ) → isEquiv (G n i)
  isEquivG zero i =
    isoToIsEquiv
      (iso _ (λ f → fst f false)
        (λ {(f , p) → →∙Homogeneous≡ (isHomogeneousKn _)
              (funExt λ { false → rUnitₖ _ (f false) ; true → sym p})})
        (lUnit⌣ₖ _))
  isEquivG (suc n) i =
    subst isEquiv (sym (funExt (decomposeG i n)))
      (compEquiv (compEquiv (G n i , isEquivG n i)
        (isoToEquiv (invIso (suspKn-Iso n (n +' i)))))
        (pathToEquiv (λ j → S₊∙ (suc n) →∙ coHomK-ptd (+'-suc n i (~ j)))) .snd)

  isEquiv-g : (n i : ℕ) → isEquiv (g n i)
  isEquiv-g n i =
    subst isEquiv (sym (g≡ n i))
      (compEquiv (G n i , isEquivG n i)
        (compEquiv (indexSwap n i) (-ₖ'^-Iso n i)) .snd)

-- We now generealise the equivalence g to also apply to arbitrary fibrations (Q : B → Type)
-- satisfying (Q * ≃∙ Sⁿ)
module _ {ℓ} (B : Pointed ℓ) (Q : typ B → Pointed ℓ-zero)
         (conB : (x y : typ B) → ∥ x ≡ y ∥₁)
         (n : ℕ) (Q-is : Iso (typ (Q (pt B))) (S₊ n))
         (Q-is-ptd : Iso.fun Q-is (pt (Q (pt B))) ≡ snd (S₊∙ n))
         (c : (b : typ B) → (Q b →∙ coHomK-ptd n))
         (c-pt : c (pt B) .fst ≡ ((λ x → genFunSpace n .fst (Iso.fun Q-is x))))
         where

  g : (b : typ B) (i : ℕ) → coHomK i → (Q b →∙ coHomK-ptd (i +' n))
  fst (g b i x) y = x ⌣ₖ c b .fst y
  snd (g b i x) = cong (x ⌣ₖ_) (c b .snd) ∙ ⌣ₖ-0ₖ i n x

  g-hom : (b : typ B) (i : ℕ) → (x y : coHomK i)
        → g b i (x +ₖ y) ≡ ((g b i x) ++ (g b i y))
  g-hom b i x y =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ z → rightDistr-⌣ₖ i n x y (c b .fst z))

  gPathP' : (i : ℕ)
    → PathP (λ j → coHomK i →
                 (isoToPath Q-is j , ua-gluePath (isoToEquiv Q-is) (Q-is-ptd) j)
              →∙ coHomK-ptd (i +' n))
       (g (pt B) i) (g-base.g n i)
  gPathP' i =
    toPathP
      (funExt
      λ x → →∙Homogeneous≡ (isHomogeneousKn _)
          (funExt λ y
         → (λ i → transportRefl (transportRefl x i ⌣ₖ c (pt B) .fst
                                     (Iso.inv Q-is (transportRefl y i))) i)
                  ∙ cong (x ⌣ₖ_)
                         (funExt⁻ c-pt (Iso.inv Q-is y)
                            ∙ cong (genFunSpace n .fst) (Iso.rightInv Q-is y))))

  g-base : (i : ℕ) → isEquiv (g (pt B) i)
  g-base i = transport (λ j → isEquiv (gPathP' i (~ j))) (g-base.isEquiv-g n i)

  g-equiv : (b : typ B) (i : ℕ) → isEquiv (g b i)
  g-equiv b i =
    PT.rec (isPropIsEquiv _)
         (J (λ b _ → isEquiv (g b i))
           (g-base i))
         (conB (pt B) b)

module _ {ℓ} (B : Pointed ℓ) (Q : typ B → Pointed ℓ-zero)
         (conB : (x y : typ B) → ∥ x ≡ y ∥₂)
         (n : ℕ) (Q-is : Iso (typ (Q (pt B))) (S₊ n))
         (Q-is-ptd : Iso.fun Q-is (pt (Q (pt B))) ≡ snd (S₊∙ n)) where

  is-setQ→K : (b : typ B) → isSet (Q b →∙ coHomK-ptd n)
  is-setQ→K b =
    ST.rec (isProp→isOfHLevelSuc 1 isPropIsSet)
          (J (λ b _ → isSet (Q b →∙ coHomK-ptd n))
            (subst isSet (cong (_→∙ coHomK-ptd n)
              (ua∙ (isoToEquiv (invIso Q-is))
                   (cong (Iso.inv Q-is) (sym Q-is-ptd) ∙ Iso.leftInv Q-is _)))
              (isOfHLevelRetractFromIso 2 (fst (πS≅ℤ n)) isSetℤ)))
          (conB (pt B) b)

  isConnB : isConnected 3 (typ B)
  fst isConnB = ∣ pt B ∣
  snd isConnB =
    T.elim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
           λ a → ST.rec (isOfHLevelTrunc 3 _ _) (cong ∣_∣ₕ) (conB (pt B) a)

  isPropPath : isProp (∥ pt B ≡ pt B ∥₂)
  isPropPath =
    isOfHLevelRetractFromIso 1 setTruncTrunc2Iso
      (isContr→isProp (isConnectedPath _ isConnB (pt B) (pt B)))

  -- We construct a term in c* : (b : B) → (Q b →∙ Kₙ)
  -- Which is equal to the generator of (Sⁿ →∙ Kₙ) over the base point.
  c* : Σ[ c ∈ ((b : typ B) → (Q b →∙ coHomK-ptd n)) ]
         (c (pt B) .fst ≡ ((λ x → genFunSpace n .fst (Iso.fun Q-is x))))
  fst c* b =
    ST.rec (is-setQ→K b)
          (J (λ b _ → Q b →∙ coHomK-ptd n)
            ((λ x → genFunSpace n .fst (Iso.fun Q-is x))
           , cong (genFunSpace n .fst) Q-is-ptd ∙ genFunSpace n .snd))
         (conB (pt B) b)
  snd c* =
    funExt λ x → (λ i → ST.rec (is-setQ→K (pt B))
                  (J (λ b _ → Q b →∙ coHomK-ptd n)
                   ((λ x₁ → genFunSpace n .fst (Iso.fun Q-is x₁)) ,
                    (λ i → genFunSpace n .fst (Q-is-ptd i))
                          ∙ genFunSpace n .snd))
                  (isPropPath (conB (pt B) (pt B)) ∣ refl ∣₂ i) .fst x)
      ∙ (λ i → transportRefl (genFunSpace n .fst
                               (Iso.fun Q-is (transportRefl x i))) i)

  p-help : {b : fst B} (p : pt B ≡ b)
        → (subst (fst ∘ Q) (sym p) (snd (Q b))) ≡ (snd (Q (pt B)))
  p-help {b = b} =
    J (λ b p → subst (fst ∘ Q) (sym p) (snd (Q b)) ≡ snd (Q (pt B)))
      (transportRefl _)

  -- This form of c* will make things somewhat easier to work with later on.
  c≡ : (b : fst B) (p : ∥ pt B ≡ b ∥₂)
    → (c* .fst b)
      ≡ ST.rec (is-setQ→K b)
             (λ pp → (λ qb →
               genFunSpace n .fst (Iso.fun Q-is (subst (fst ∘ Q) (sym pp) qb)))
             , cong (genFunSpace n .fst ∘ Iso.fun Q-is) (p-help pp)
             ∙ ((λ i → genFunSpace n .fst (Q-is-ptd i)) ∙ genFunSpace n .snd)) p
  c≡ b =
    ST.elim (λ _ → isOfHLevelPath 2 (is-setQ→K b) _ _)
          (J (λ b a → c* .fst b ≡
      ST.rec (is-setQ→K b) (λ pp →
         (λ qb →
            genFunSpace n .fst (Iso.fun Q-is (subst (fst ∘ Q) (sym pp) qb)))
         ,
         cong (genFunSpace n .fst ∘ Iso.fun Q-is) (p-help pp) ∙
         (λ i → genFunSpace n .fst (Q-is-ptd i)) ∙ genFunSpace n .snd) ∣ a ∣₂)
      ((λ i → ST.rec (is-setQ→K (pt B))
      (J (λ b₁ _ → Q b₁ →∙ coHomK-ptd n)
       ((λ x → genFunSpace n .fst (Iso.fun Q-is x)) ,
        (λ i → genFunSpace n .fst (Q-is-ptd i)) ∙ genFunSpace n .snd))
          (isPropPath (conB (pt B) (pt B)) ∣ refl ∣₂ i))
          ∙ →∙Homogeneous≡ (isHomogeneousKn n)
            (transportRefl ((λ x → genFunSpace n .fst (Iso.fun Q-is x)))
            ∙ funExt λ x → cong (genFunSpace n .fst ∘ Iso.fun Q-is)
                     (sym (transportRefl x)))))

-- We are now almost ready to define the Thom isomorphism.
-- The following module contains the types and functions occuring in it.
module preThom {ℓ ℓ'} (B : Pointed ℓ) (P : typ B → Type ℓ') where
  E : Type _
  E = Σ (typ B) P

  Ẽ : Type _
  Ẽ = Pushout {A = E} (λ _ → tt) fst

  i : (n : ℕ) → (P-base : Iso (P (pt B)) (S₊ n)) → S₊ (suc n) → Ẽ
  i zero P-base base = inr (pt B)
  i zero P-base (loop j) = (sym (push (pt B , Iso.inv P-base false))
                               ∙ push ((pt B) , Iso.inv P-base true)) j
  i (suc n) P-base north = inl tt
  i (suc n) P-base south = inr (pt B)
  i (suc n) P-base (merid a i₁) = push (pt B , Iso.inv P-base a) i₁

  Q : typ B → Pointed ℓ'
  Q x = Susp (P x) , north

  F : Type _
  F = Σ (typ B) λ x → Q x .fst

  F̃ : Type _
  F̃ = Pushout {A = typ B} {C = F} (λ _ → tt) λ b → b , north

  invFE : Ẽ → F̃
  invFE (inl x) = inl tt
  invFE (inr x) = inr (x , south)
  invFE (push (x , a) i₁) = ((push x) ∙ λ i → inr (x , merid a i)) i₁

  funFE : F̃ → Ẽ
  funFE (inl x) = inl tt
  funFE (inr (x , north)) = inl tt
  funFE (inr (x , south)) = inr x
  funFE (inr (x , merid a i₁)) = push (x , a) i₁
  funFE (push a i₁) = inl tt

  IsoFE : Iso F̃ Ẽ
  Iso.fun IsoFE = funFE
  Iso.inv IsoFE = invFE
  Iso.rightInv IsoFE (inl x) = refl
  Iso.rightInv IsoFE (inr x) = refl
  Iso.rightInv IsoFE (push (x , a) i₁) k = lem k i₁
    where
    lem : cong funFE (((push x) ∙ λ i → inr (x , merid a i)))
        ≡ push (x , a)
    lem = congFunct funFE (push x) (λ i → inr (x , merid a i))
     ∙ sym (lUnit (push (x , a)))
  Iso.leftInv IsoFE (inl x) = refl
  Iso.leftInv IsoFE (inr (x , north)) = push x
  Iso.leftInv IsoFE (inr (x , south)) = refl
  Iso.leftInv IsoFE (inr (x , merid a i)) j =
    compPath-filler' (push x) (λ i₁ → inr (x , merid a i₁)) (~ j) i
  Iso.leftInv IsoFE (push a i₁) k =  push a (i₁ ∧ k)

  F̃→Q : ∀ {ℓ} {A : Pointed ℓ} → (F̃ , inl tt) →∙ A → (b : typ B) → Q b →∙ A
  fst (F̃→Q {A = A , a} (f , p) b) north = f (inr (b , north))
  fst (F̃→Q {A = A , a} (f , p) b) south = f (inr (b , south))
  fst (F̃→Q {A = A , a} (f , p) b) (merid a₁ i₁) = f (inr (b , merid a₁ i₁))
  snd (F̃→Q {A = A , a} (f , p) b) = sym (cong f (push b)) ∙ p

  Q→F̃ : ∀ {ℓ} {A : Pointed ℓ} → ((b : typ B) → Q b →∙ A) → (F̃ , inl tt) →∙ A
  fst (Q→F̃ {A = A , a} f) (inl x) = a
  fst (Q→F̃ {A = A , a} f) (inr (x , north)) = f x .fst north
  fst (Q→F̃ {A = A , a} f) (inr (x , south)) = f x .fst south
  fst (Q→F̃ {A = A , a} f) (inr (x , merid a₁ i₁)) = f x .fst (merid a₁ i₁)
  fst (Q→F̃ {A = A , a} f) (push a₁ i₁) = snd (f a₁) (~ i₁)
  snd (Q→F̃ {A = A , a} f) = refl

  Q→F̃-hom : (n : ℕ) → (f g : ((b : typ B) → Q b →∙ coHomK-ptd n))
             → Q→F̃ (λ b → f b ++ g b) ≡ (Q→F̃ f ++ Q→F̃ g)
  Q→F̃-hom n f g =
    →∙Homogeneous≡ (isHomogeneousKn _)
      (funExt λ { (inl x) → sym (rUnitₖ _ (0ₖ _))
                ; (inr (x , north)) → refl
                ; (inr (x , south)) → refl
                ; (inr (x , merid a i₁)) → refl
                ; (push a j) i →
                  compPath-filler (cong₂ _+ₖ_ (snd (f a)) (snd (g a)))
                                  (rUnitₖ n (0ₖ n)) (~ i) (~ j)})

  Q→F̃→Q : ∀ {ℓ} {A : Pointed ℓ}
    → (x : (b : typ B) → Q b →∙ A) (b : typ B) (q : Q b .fst)
    → F̃→Q (Q→F̃ x) b .fst q ≡ x b .fst q
  Q→F̃→Q f b north = refl
  Q→F̃→Q f b south = refl
  Q→F̃→Q f b (merid a i₁) = refl

  F̃→Q→F̃ : ∀ {ℓ} {A : Pointed ℓ} (f : F̃ → typ A) (p : _)
    → (x : F̃) → fst (Q→F̃ {A = A} (F̃→Q (f , p))) x ≡ f x
  F̃→Q→F̃ f p (inl x) = sym p
  F̃→Q→F̃ f p (inr (x , north)) = refl
  F̃→Q→F̃ f p (inr (x , south)) = refl
  F̃→Q→F̃ f p (inr (x , merid a i₁)) = refl
  F̃→Q→F̃ f p (push a i₁) j =
    compPath-filler (sym (cong f (push a))) p (~ j) (~ i₁)

  IsoF̃Q : ∀ {ℓ} {A : Pointed ℓ}
    → Iso ((F̃ , inl tt) →∙ A)
          ((b : typ B) → Q b →∙ A)
  Iso.fun (IsoF̃Q {A = A , a}) = F̃→Q
  Iso.inv (IsoF̃Q {A = A , a}) = Q→F̃
  Iso.rightInv (IsoF̃Q {A = A , a}) f =
    funExt λ b → ΣPathP (funExt (Q→F̃→Q f b)
               , sym (rUnit (snd (f b))))
  Iso.leftInv (IsoF̃Q {A = A , a}) (f , p) =
    ΣPathP ((funExt (F̃→Q→F̃ f p))
         , λ i j → p (~ i ∨ j))

  -- The main result
  ι : (k : ℕ) → Iso ((b : typ B) → Q b →∙ coHomK-ptd k)
                      ((Ẽ , inl tt) →∙ coHomK-ptd k)
  ι k = compIso (invIso IsoF̃Q) IsoFE-extend
    where

    IsoFE-extend : Iso ((F̃ , inl tt) →∙ coHomK-ptd k)
             ((Ẽ , inl tt) →∙ coHomK-ptd k)
    Iso.fun IsoFE-extend G = (λ x → G .fst (Iso.inv IsoFE x))
                , (snd G)
    Iso.inv IsoFE-extend G = (λ x → G .fst (Iso.fun IsoFE x))
                , (snd G)
    Iso.rightInv IsoFE-extend G =
      →∙Homogeneous≡ (isHomogeneousKn _)
        (funExt λ x → cong (G .fst) (Iso.rightInv IsoFE x))
    Iso.leftInv IsoFE-extend G =
      →∙Homogeneous≡ (isHomogeneousKn _)
        (funExt λ x → cong (G .fst) (Iso.leftInv IsoFE x))

  ι-hom : (k : ℕ) → (f g : ((b : typ B) → Q b →∙ coHomK-ptd k))
                   → Iso.fun (ι k) (λ b → f b ++ g b)
                   ≡ (Iso.fun (ι k) f ++ Iso.fun (ι k) g)
  ι-hom k f g =
    →∙Homogeneous≡ (isHomogeneousKn _)
        (funExt λ x → funExt⁻ (cong fst (Q→F̃-hom _ f g)) (invFE x))

-- Packing everything up gives us the Thom Isomorphism between
-- the nᵗʰ cohomology of B and the (n+i)ᵗʰ reduced cohomology of Ẽ,
-- as defined above
module Thom {ℓ} (B : Pointed ℓ) (P : typ B → Type ℓ-zero)
         (conB : (x y : typ B) → ∥ x ≡ y ∥₁)
         (n : ℕ) (Q-is : Iso (typ (preThom.Q B P (pt B))) (S₊ n))
         (Q-is-ptd : Iso.fun Q-is (pt (preThom.Q B P (pt B))) ≡ snd (S₊∙ n))
         (c : (b : typ B) → (preThom.Q B P b →∙ coHomK-ptd n))
         (c-pt : c (pt B) .fst ≡ ((λ x → genFunSpace n .fst (Iso.fun Q-is x))))
         where

  ϕ : (i : ℕ)
    → GroupEquiv (coHomGr i (typ B))
                  (coHomRedGrDir (i +' n) (preThom.Ẽ B P , inl tt))
  fst (ϕ i) =
    isoToEquiv
      (setTruncIso
        (compIso
          (codomainIsoDep
            λ b →
              equivToIso ((g B (preThom.Q B P) conB n Q-is Q-is-ptd c c-pt b i)
                 , g-equiv B (preThom.Q B P) conB n Q-is Q-is-ptd c c-pt b i))
            (preThom.ι B P (i +' n))))
  snd (ϕ i) =
    makeIsGroupHom
    (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
      λ F G →
        cong ∣_∣₂ (cong (Iso.fun (preThom.ι B P (i +' n)))
                       (funExt (λ a →
                         g-hom B (preThom.Q B P)
                               conB n Q-is Q-is-ptd c c-pt a i (F a) (G a)))
                     ∙ preThom.ι-hom B P (i +' n) _ _)
           ∙ addAgree (i +' n) _ _)

-- We finally get the Gysin sequence
module Gysin {ℓ} (B : Pointed ℓ) (P : typ B → Type ℓ-zero)
         (conB : (x y : typ B) → ∥ x ≡ y ∥₂)
         (n : ℕ) (Q-is : Iso (typ (preThom.Q B P (pt B))) (S₊ n))
         (Q-is-ptd : Iso.fun Q-is (pt (preThom.Q B P (pt B))) ≡ snd (S₊∙ n))
         where

  0-connB : (x y : typ B) → ∥ x ≡ y ∥₁
  0-connB x y = ST.rec (isProp→isSet squash₁) (∥_∥₁.∣_∣₁) (conB x y)

  c = (c* B (preThom.Q B P) conB n Q-is Q-is-ptd .fst)
  c-ptd = (c* B (preThom.Q B P) conB n Q-is Q-is-ptd .snd)
  cEq = c≡ B (preThom.Q B P) conB n Q-is Q-is-ptd

  module w = Thom B P 0-connB n Q-is Q-is-ptd c c-ptd

  ϕ = w.ϕ

  E' = preThom.E B P

  E'̃ = preThom.Ẽ B P

  -- The generator of coHom n (typ B)
  e : coHom n (typ B)
  e = ∣ (λ b → c b .fst south) ∣₂

  -- The maps of interest are ⌣, p, E-susp and j*. In reality, we are interested
  -- in the composition of ϕ and j* (which is just the cup product),
  -- but it's easier to first give an exact sequence involving p, E-susp and j*
  ⌣-hom : (i : ℕ) → GroupHom (coHomGr i (typ B)) (coHomGr (i +' n) (typ B))
  fst (⌣-hom i) x = x ⌣ e
  snd (⌣-hom i) =
    makeIsGroupHom λ f g → rightDistr-⌣ _ _ f g e

  p : E' → typ B
  p = fst

  p-hom : (i : ℕ) → GroupHom (coHomGr i (typ B)) (coHomGr i E')
  p-hom i = coHomMorph _ p

  E-susp : (i : ℕ) →
    GroupHom (coHomGr i E') (coHomRedGrDir (suc i) (E'̃ , inl tt))
  fst (E-susp i) =
    ST.map λ f → (λ { (inl x) → 0ₖ _
                   ; (inr x) → 0ₖ _
                   ; (push a j) → Kn→ΩKn+1 _ (f a) j}) , refl
  snd (E-susp zero) =
    makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
      λ f g →
        cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn 1)
          (funExt λ { (inl x) → refl
                    ; (inr x) → refl
                    ; (push a j) k →
                      (Kn→ΩKn+1-hom zero (f a) (g a)
                     ∙ ∙≡+₁ (Kn→ΩKn+1 _ (f a)) (Kn→ΩKn+1 _ (g a))) k j})))
  snd (E-susp (suc i)) =
    makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
      λ f g →
        cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _)
          (funExt λ { (inl x) → refl
                    ; (inr x) → refl
                    ; (push a j) k → (Kn→ΩKn+1-hom _ (f a) (g a)
                                   ∙ ∙≡+₂ _ (Kn→ΩKn+1 _ (f a))
                                            (Kn→ΩKn+1 _ (g a))) k j})))

  module cofibSeq where
    j* : (i : ℕ) →
      GroupHom (coHomRedGrDir i (E'̃ , (inl tt))) (coHomGr i (typ B))
    fst (j* i) = ST.map λ f → λ x → fst f (inr x)
    snd (j* zero) =
      makeIsGroupHom
        (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ _ _ → refl)
    snd (j* (suc zero)) =
      makeIsGroupHom
        (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ _ _ → refl)
    snd (j* (suc (suc i₁))) =
      makeIsGroupHom
        (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ _ _ → refl)

    Im-j⊂Ker-p : (i : ℕ) (x : _) → isInIm (j* i) x → isInKer (p-hom i) x
    Im-j⊂Ker-p i =
      ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
        λ f → PT.rec (squash₂ _ _)
          (uncurry (ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
            λ g P → subst (isInKer (p-hom i)) P
              (cong ∣_∣₂ (funExt λ x →
                cong (g .fst) (sym (push x)) ∙ g .snd))))

    Ker-p⊂Im-j : (i : ℕ) (x : _) → isInKer (p-hom i) x → isInIm (j* i) x
    Ker-p⊂Im-j i =
      ST.elim (λ _ → isSetΠ (λ _ → isProp→isSet squash₁))
        λ f ker → PT.rec squash₁
          (λ id → ∣ ∣ (λ { (inl x) → 0ₖ _
                         ; (inr x) → f x
                         ; (push a i₁) → funExt⁻ id a (~ i₁)}) , refl ∣₂
                         , refl ∣₁)
                   (Iso.fun PathIdTrunc₀Iso ker)

  Im-p⊂Ker-Susp : (i : ℕ) (x : _)
                → isInIm (p-hom i) x → isInKer (E-susp i) x
  Im-p⊂Ker-Susp i =
    ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
      λ f → PT.rec (squash₂ _ _)
        (uncurry (ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
          λ g y → subst (isInKer (E-susp i)) y
            (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _)
              (funExt λ { (inl x) → refl
                        ; (inr x) → sym (Kn→ΩKn+1 _ (g x))
                        ; (push a j) k → Kn→ΩKn+1 i (g (fst a)) (~ k ∧ j)})))))

  Ker-Susp⊂Im-p : (i : ℕ) (x : _)
                → isInKer (E-susp i) x → isInIm (p-hom i) x
  Ker-Susp⊂Im-p i =
    ST.elim (λ _ → isSetΠ (λ _ → isProp→isSet squash₁))
      λ f ker → PT.rec squash₁
        (λ id → ∣ ∣ (λ x → ΩKn+1→Kn i (sym (funExt⁻ (cong fst id) (inr x)))) ∣₂
                  , cong ∣_∣₂ (funExt (λ { (a , b) →
                         cong (ΩKn+1→Kn i)
                           (lUnit _
                          ∙ cong (_∙ sym (funExt⁻ (λ i₁ → fst (id i₁)) (inr a)))
                           (sym (flipSquare (cong snd id))
                       ∙∙ (PathP→compPathR
                            (cong (funExt⁻ (cong fst id)) (push (a , b))))
                       ∙∙ assoc _ _ _
                        ∙ sym (rUnit _))
                        ∙ (sym (assoc _ _ _)
                        ∙∙ cong (Kn→ΩKn+1 i (f (a , b)) ∙_) (rCancel _)
                        ∙∙ sym (rUnit _)))
                        ∙ Iso.leftInv (Iso-Kn-ΩKn+1 _) (f (a , b))})) ∣₁)
        (Iso.fun PathIdTrunc₀Iso ker)

  Im-Susp⊂Ker-j : (i : ℕ) (x : _)
               → isInIm (E-susp i) x → isInKer (cofibSeq.j* (suc i)) x
  Im-Susp⊂Ker-j i =
    ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
      λ g → PT.rec (squash₂ _ _)
        (uncurry (ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
          λ f id → PT.rec (squash₂ _ _)
            (λ P → subst (isInKer (cofibSeq.j* (suc i))) (cong ∣_∣₂ P)
              (cong ∣_∣₂ refl))
            (Iso.fun PathIdTrunc₀Iso id)))

  Ker-j⊂Im-Susp : (i : ℕ) (x : _)
                → isInKer (cofibSeq.j* (suc i)) x → isInIm (E-susp i) x
  Ker-j⊂Im-Susp i =
    ST.elim (λ _ → isSetΠ (λ _ → isProp→isSet squash₁))
      λ f ker
       → PT.rec squash₁
          (λ p → ∣ ∣ (λ x → ΩKn+1→Kn _ (sym (snd f)
                                     ∙∙ cong (fst f) (push x)
                                     ∙∙ funExt⁻ p (fst x))) ∣₂
                  , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousKn _)
                    (funExt (λ { (inl x) → sym (snd f)
                               ; (inr x) → sym (funExt⁻ p x)
                               ; (push a j) k → h3 f p a k j}))) ∣₁)
          (Iso.fun PathIdTrunc₀Iso ker)
          where
          h3 : (f : (E'̃ , inl tt) →∙ coHomK-ptd (suc i))
           → (p : (fst f ∘ inr) ≡ (λ _ → 0ₖ (suc i)))
           → (a : preThom.E B P)
           → PathP (λ i → snd f (~ i) ≡ p (~ i) (fst a))
                   (Kn→ΩKn+1 i (ΩKn+1→Kn i (sym (snd f)
                                          ∙∙ cong (fst f) (push a)
                                          ∙∙ funExt⁻ p (fst a))))
                   (cong (fst f) (push a))
          h3 f p a =
            Iso.rightInv (Iso-Kn-ΩKn+1 i) _
              ◁ λ i j →
                 doubleCompPath-filler (sym (snd f)) (cong (fst f) (push a))
                 (funExt⁻ p (fst a)) (~ i) j

  -- We compose ϕ and j*. The above exact sequence will induce another one for
  -- this composition. In fact, this group hom is definitionally equal to
  -- (λ x → x ⌣ e) modulo truncation elimination and snd fields.
  ϕ∘j : (i : ℕ) → GroupHom (coHomGr i (typ B)) (coHomGr (i +' n) (typ B))
  ϕ∘j i = compGroupHom (fst (fst (ϕ i)) , snd (ϕ i)) (cofibSeq.j* (i +' n))

  private
    +'-suc : (i n : ℕ) → (suc i +' n) ≡ suc (i +' n)
    +'-suc zero zero = refl
    +'-suc (suc i₁) zero = refl
    +'-suc zero (suc n) = refl
    +'-suc (suc i₁) (suc n) = refl

    Path→GroupPath : ∀ {ℓ ℓ'} {n m : ℕ} (G : ℕ → Group ℓ) (H : Group ℓ')
         (p : n ≡ m)
      → GroupEquiv (G n) H
      → GroupEquiv (G m) H
    Path→GroupPath {n = n} G H =
      J (λ m _ → GroupEquiv (G n) H → GroupEquiv (G m) H)
        λ p → p

    h-ret : ∀ {ℓ ℓ'} {n m : ℕ} (G : ℕ → Group ℓ) (H : Group ℓ')
      → (e : GroupEquiv (G n) H)
      → (p : n ≡ m)
      → (x : G m .fst)
      → invEq (fst e) (fst (fst (Path→GroupPath G H p e)) x)
       ≡ subst (λ x → G x .fst) (sym p) x
    h-ret G H e =
      J (λ m p → ((x : G m .fst)
               → invEq (fst e) (fst (fst (Path→GroupPath G H p e)) x)
                ≡ subst (λ x → G x .fst) (sym p) x))
        λ x → cong (invEq (fst e) )
              (λ i → transportRefl (transportRefl (fst (fst e)
                     (transportRefl (transportRefl x i) i)) i) i)
           ∙∙ retEq (fst e) x
           ∙∙ sym (transportRefl _)

  thomIso' : (i : ℕ) → GroupEquiv (coHomRedGrDir (suc (i +' n)) (E'̃ , inl tt))
                            (coHomGr (suc i) (typ B))
  thomIso' i = (Path→GroupPath
                (λ n → coHomRedGrDir n (E'̃ , inl tt)) _ (+'-suc i n)
                  (invGroupEquiv (ϕ (suc i))))

  ϕ' : (i : ℕ) → GroupHom (coHomRedGrDir (suc (i +' n)) (E'̃ , inl tt))
                            (coHomGr (suc i) (typ B))
  ϕ' i = fst (fst (thomIso' i)) , snd (thomIso' i)

  susp∘ϕ : (i : ℕ) → GroupHom (coHomGr (i +' n) E') (coHomGr (suc i) (typ B))
  susp∘ϕ i = compGroupHom (E-susp (i +' n)) (ϕ' i)

  Im-ϕ∘j⊂Ker-p : (i : ℕ) (x : _) → isInIm (ϕ∘j i) x → isInKer (p-hom _) x
  Im-ϕ∘j⊂Ker-p i x p =
    cofibSeq.Im-j⊂Ker-p _ x
      (PT.rec squash₁ (uncurry (λ f p → ∣ fst (fst (ϕ _)) f , p ∣₁)) p)

  Ker-p⊂Im-ϕ∘j : (i : ℕ) (x : _) → isInKer (p-hom _) x → isInIm (ϕ∘j i) x
  Ker-p⊂Im-ϕ∘j i x p =
    PT.rec squash₁
      (uncurry (λ f p →
          ∣ (invEq (fst (ϕ _)) f)
         , (cong (fst (cofibSeq.j* _)) (secEq (fst (ϕ _)) f) ∙ p) ∣₁))
        (cofibSeq.Ker-p⊂Im-j _ x p)

  Im-p⊂KerSusp∘ϕ : (i : ℕ) (x : _)
                 → isInIm (p-hom _) x → isInKer (susp∘ϕ i) x
  Im-p⊂KerSusp∘ϕ i x p =
    cong (fst (ϕ' _)) (Im-p⊂Ker-Susp _ x p) ∙ IsGroupHom.pres1 (snd (ϕ' _))

  KerSusp∘ϕ⊂Im-p : (i : ℕ) (x : _)
    → isInKer (susp∘ϕ i) x → isInIm (p-hom _) x
  KerSusp∘ϕ⊂Im-p i x p =
    Ker-Susp⊂Im-p _ x (sym (retEq (fst (thomIso' _)) _)
                    ∙ (cong (invEq (fst (thomIso' _))) p
                    ∙ IsGroupHom.pres1 (snd (invGroupEquiv (thomIso' _)))))

  Im-Susp∘ϕ⊂Ker-ϕ∘j : (i : ℕ) → (x : _)
                    → isInIm (susp∘ϕ i) x → isInKer (ϕ∘j (suc i)) x
  Im-Susp∘ϕ⊂Ker-ϕ∘j i x =
    PT.rec (squash₂ _ _)
      (uncurry λ f → J (λ x p → isInKer (ϕ∘j (suc i)) x)
        ((λ i → fst (cofibSeq.j* _) (fst (fst (ϕ _)) (fst (ϕ' _) (fst (E-susp _) f))))
             ∙∙ cong (fst (cofibSeq.j* _))
                     ((h-ret (λ n → coHomRedGrDir n (E'̃ , inl tt)) _
                             (invGroupEquiv (ϕ (suc i))) (+'-suc i n)) (fst (E-susp _) f))
             ∙∙ (natTranspLem _ (λ n → fst (cofibSeq.j* n)) (sym (+'-suc i n))
             ∙ cong (subst (λ z → coHomGr z (typ B) .fst) (sym (+'-suc i n)))
                    (Im-Susp⊂Ker-j _ (fst (E-susp (i +' n)) f) ∣ f , refl ∣₁)
              ∙ tLem i n)))
    where
    tLem : (i n : ℕ) → subst (λ z → coHomGr z (typ B) .fst) (sym (+'-suc i n))
                               (0ₕ _) ≡ 0ₕ _
    tLem zero zero = refl
    tLem zero (suc n) = refl
    tLem (suc i₁) zero = refl
    tLem (suc i₁) (suc n) = refl

  Ker-ϕ∘j⊂Im-Susp∘ϕ : (i : ℕ) (x : _)
    → isInKer (ϕ∘j (suc i)) x → isInIm (susp∘ϕ i) x
  Ker-ϕ∘j⊂Im-Susp∘ϕ i x p =
    PT.rec squash₁
      (uncurry (λ f p → ∣ f , cong (fst (fst (thomIso' i))) p
                        ∙ secEq (fst (thomIso' _)) x ∣₁))
      (Ker-j⊂Im-Susp _ (invEq (fst (thomIso' _)) x)
        ((cong (cofibSeq.j* (suc (i +' n)) .fst ) lem₁
        ∙ natTranspLem _ (λ n → cofibSeq.j* n .fst) (+'-suc i n))
        ∙∙ cong (transport (λ j → (coHomGr (+'-suc i n j) (typ B) .fst))) p
        ∙∙ lem₂ i n))
    where
    lem₁ : invEq (fst (thomIso' i)) x
         ≡ transport (λ j → coHomRed (+'-suc i n j)
                     (E'̃ , inl tt)) (fst (fst (ϕ _)) x)
    lem₁ = cong (transport (λ j → coHomRed (+'-suc i n j) (E'̃ , inl tt)))
                (transportRefl _ ∙ cong (fst (fst (ϕ _)))
                  λ i → transportRefl (transportRefl x i) i)

    lem₂ : (i n : ℕ)
         → transport (λ j → coHomGr (+'-suc i n j) (typ B) .fst)
                      (GroupStr.1g (coHomGr (suc i +' n) (typ B) .snd)) ≡ 0ₕ _
    lem₂ zero zero = refl
    lem₂ zero (suc n) = refl
    lem₂ (suc i₁) zero = refl
    lem₂ (suc i₁) (suc n) = refl

  -- Finally, we have that ϕ∘j is just the cup product, and we have arrived
  -- at an exact sequence involving it.
  ϕ∘j≡ : (i : ℕ) → ϕ∘j i ≡ ⌣-hom i
  ϕ∘j≡ i =
    Σ≡Prop (λ _ → isPropIsGroupHom _ _)
           (funExt (ST.elim (λ _ → isOfHLevelPath 2 squash₂ _ _)
           λ _ → refl))

  -- We can now restate the previous resluts for (λ x → x ⌣ e)
  Im-⌣e⊂Ker-p : (i : ℕ) (x : _)
              → isInIm (⌣-hom i) x → isInKer (p-hom _) x
  Im-⌣e⊂Ker-p i x p =
    Im-ϕ∘j⊂Ker-p i x (subst (λ p → isInIm p x) (sym (ϕ∘j≡ i)) p)

  Ker-p⊂Im-⌣e : (i : ℕ) (x : _)
              → isInKer (p-hom _) x → isInIm (⌣-hom i) x
  Ker-p⊂Im-⌣e i x p =
    subst (λ p → isInIm p x) (ϕ∘j≡ i) (Ker-p⊂Im-ϕ∘j i x p)

  Im-Susp∘ϕ⊂Ker-⌣e : (i : ℕ) (x : _)
                   → isInIm (susp∘ϕ i) x → isInKer (⌣-hom (suc i)) x
  Im-Susp∘ϕ⊂Ker-⌣e i x p =
    subst (λ p → isInKer p x) (ϕ∘j≡ (suc i)) (Im-Susp∘ϕ⊂Ker-ϕ∘j i x p)

  Ker-⌣e⊂Im-Susp∘ϕ : (i : ℕ) (x : _)
                   → isInKer (⌣-hom (suc i)) x → isInIm (susp∘ϕ i) x
  Ker-⌣e⊂Im-Susp∘ϕ i x p =
    Ker-ϕ∘j⊂Im-Susp∘ϕ i x (subst (λ p → isInKer p x) (sym (ϕ∘j≡ (suc i))) p)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
import      Lvl
open import Type

module Structure.Logic.Constructive.Propositional {ℓₗ} {Formula : Type{ℓₗ}} {ℓₘₗ} (Proof : Formula → Type{ℓₘₗ}) where

open import Logic.Predicate

private variable X Y Z : Formula

-- Rules of bottom (falsity).
record Bottom(⊥ : Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    elim : Proof(⊥) → Proof(X)
⊥ = \ ⦃([∃]-intro ▫) : ∃(Bottom)⦄ → ▫
module ⊥ {▫} ⦃ p ⦄ = Bottom {▫} p

-- Rules of top (truth).
record Top(⊤ : Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro : Proof(⊤)
⊤ = \ ⦃([∃]-intro ▫) : ∃(Top)⦄ → ▫
module ⊤ {▫} ⦃ p ⦄ = Top {▫} p

-- Rules of conjunction (and).
record Conjunction(_∧_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro : Proof(X) → Proof(Y) → Proof(X ∧ Y)
    elimₗ : Proof(X ∧ Y) → Proof(X)
    elimᵣ : Proof(X ∧ Y) → Proof(Y)
_∧_ = \ ⦃([∃]-intro ▫) : ∃(Conjunction)⦄ → ▫
module ∧ {▫} ⦃ p ⦄ = Conjunction {▫} p

-- Rules of implication.
record Implication(_⟶_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro : (Proof(X) → Proof(Y)) → Proof(X ⟶ Y)
    elim  : Proof(X ⟶ Y) → Proof(X) → Proof(Y)
_⟶_ = \ ⦃([∃]-intro ▫) : ∃(Implication)⦄ → ▫
module ⟶ {▫} ⦃ p ⦄ = Implication {▫} p

-- Rules of reversed implication.
record Consequence(_⟵_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro : (Proof(X) → Proof(Y)) → Proof(Y ⟵ X)
    elim  : Proof(Y ⟵ X) → Proof(X) → Proof(Y)
_⟵_ = \ ⦃([∃]-intro ▫) : ∃(Consequence)⦄ → ▫
module ⟵ {▫} ⦃ p ⦄ = Consequence {▫} p

-- Rules of equivalence.
record Equivalence(_⟷_ : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro  : let _ = X in (Proof(Y) → Proof(X)) → (Proof(X) → Proof(Y)) → Proof(X ⟷ Y)
    elimₗ  : Proof(X ⟷ Y) → Proof(Y) → Proof(X)
    elimᵣ  : Proof(X ⟷ Y) → Proof(X) → Proof(Y)
_⟷_ = \ ⦃([∃]-intro ▫) : ∃(Equivalence)⦄ → ▫
module ⟷ {▫} ⦃ p ⦄ = Equivalence {▫} p

-- Rules of disjunction (or).
record Disjunction(_∨_  : Formula → Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    introₗ : Proof(X) → Proof(X ∨ Y)
    introᵣ : Proof(Y) → Proof(X ∨ Y)
    elim   : (Proof(X) → Proof(Z)) → (Proof(Y) → Proof(Z)) → Proof(X ∨ Y) → Proof(Z)
_∨_ = \ ⦃([∃]-intro ▫) : ∃(Disjunction)⦄ → ▫
module ∨ {▫} ⦃ p ⦄ = Disjunction {▫} p

-- Rules of negation (not).
record Negation(¬_ : Formula → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    intro : (Proof(X) → Proof(Y)) → (Proof(X) → Proof(¬ Y)) → Proof(¬ X)
    elim  : Proof(X) → Proof(¬ X) → Proof(Y)
¬_ = \ ⦃([∃]-intro ▫) : ∃(Negation)⦄ → ▫
module ¬ {▫} ⦃ p ⦄ = Negation {▫} p

record Logic : Type{ℓₘₗ Lvl.⊔ ℓₗ} where
  field
    ⦃ bottom ⦄      : ∃(Bottom)
    ⦃ top ⦄         : ∃(Top)
    ⦃ conjunction ⦄ : ∃(Conjunction)
    ⦃ implication ⦄ : ∃(Implication)
    ⦃ consequence ⦄ : ∃(Consequence)
    ⦃ equivalence ⦄ : ∃(Equivalence)
    ⦃ disjunction ⦄ : ∃(Disjunction)
    ⦃ negation ⦄    : ∃(Negation)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------------
-- Properties for the equality on Conat
------------------------------------------------------------------------------

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

module FOTC.Data.Conat.Equality.PropertiesI where

open import FOTC.Base
open import FOTC.Data.Conat
open import FOTC.Data.Conat.Equality.Type

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- relation _≈_ is also a pre-fixed point of the functional ≈-F, i.e.
--
-- ≈-F _≈_ ≤ _≈_ (see FOTC.Data.Conat.Equality.Type).
≈-in :
  ∀ {m n} →
  m ≡ zero ∧ n ≡ zero
    ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ m' ≈ n') →
  m ≈ n
≈-in h = ≈-coind R h' h
  where
  R : D → D → Set
  R m n = m ≡ zero ∧ n ≡ zero
            ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ m' ≈ n')

  h' : ∀ {m n} → R m n →
       m ≡ zero ∧ n ≡ zero
         ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ R m' n')
  h' (inj₁ prf) = inj₁ prf
  h' (inj₂ (m' , n' , prf₁ , prf₂ , m'≈n')) =
    inj₂ (m' , n' , prf₁ , prf₂ , ≈-out m'≈n')

≈-refl : ∀ {n} → Conat n → n ≈ n
≈-refl {n} Cn = ≈-coind R h₁ h₂
  where
  R : D → D → Set
  R a b = Conat a ∧ Conat b ∧ a ≡ b

  h₁ : ∀ {a b} → R a b →
       a ≡ zero ∧ b ≡ zero
         ∨ (∃[ a' ] ∃[ b' ] a ≡ succ₁ a' ∧ b ≡ succ₁ b' ∧ R a' b')
  h₁ (Ca , Cb , h) with Conat-out Ca
  ... | inj₁ prf              = inj₁ (prf , trans (sym h) prf)
  ... | inj₂ (a' , prf , Ca') =
    inj₂ (a' , a' , prf , trans (sym h) prf , (Ca' , Ca' , refl))

  h₂ : R n n
  h₂ = Cn , Cn , refl

≡→≈ : ∀ {m n} → Conat m → Conat n → m ≡ n → m ≈ n
≡→≈ Cm _ refl = ≈-refl Cm

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc