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

module Categories.Category.Construction.Properties.Presheaves where

open import Categories.Category.Construction.Properties.Presheaves.Cartesian
  using (module IsCartesian)
  public

open import Categories.Category.Construction.Properties.Presheaves.CartesianClosed
  using (module IsCCC)
  public

open import Categories.Category.Construction.Properties.Presheaves.Complete
  using (Presheaves-Complete; Presheaves-Cocomplete)
  public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- An example
------------------------------------------------------------------------

module Mixfix.Acyclic.Example where

open import Codata.Musical.Notation
open import Data.Vec using ([]; _∷_; [_])
open import Data.List as List
  using (List; []; _∷_) renaming ([_] to L[_])
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (here; there)
import Codata.Musical.Colist as Colist
open import Data.Product using (∃₂; -,_)
open import Data.Unit.Polymorphic using (⊤)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Nat using (zero; suc)
open import Data.Fin using (#_)
import Data.List.Relation.Binary.Pointwise as ListEq
import Data.String as String
open String using (String; _++_)
import Data.String.Properties as String
open import Relation.Binary
open DecSetoid (ListEq.decSetoid String.≡-decSetoid) using (_≟_)
open import Function using (_∘_; _$_)
open import Data.Bool using (Bool; if_then_else_)
import Data.Bool.Show as Bool
open import Relation.Nullary.Decidable using (⌊_⌋)
import Relation.Binary.PropositionalEquality as P
open import IO
import Level

open import Mixfix.Fixity hiding (_≟_)
open import Mixfix.Operator
open import Mixfix.Expr
open import Mixfix.Acyclic.PrecedenceGraph
import Mixfix.Acyclic.Grammar as Grammar
import Mixfix.Acyclic.Show as Show
import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified using (Parser)
import StructurallyRecursiveDescentParsing.DepthFirst as DepthFirst
import TotalParserCombinators.BreadthFirst as BreadthFirst

------------------------------------------------------------------------
-- Operators

atom : Operator closed 0
atom = record { nameParts = "•" ∷ [] }

plus : Operator (infx left) 0
plus = record { nameParts = "+" ∷ [] }

ifThen : Operator prefx 1
ifThen = record { nameParts = "i" ∷ "t" ∷ [] }

ifThenElse : Operator prefx 2
ifThenElse = record { nameParts = "i" ∷ "t" ∷ "e" ∷ [] }

comma : Operator (infx left) 0
comma = record { nameParts = "," ∷ [] }

wellTyped : Operator postfx 1
wellTyped = record { nameParts = "⊢" ∷ "∶" ∷ [] }

------------------------------------------------------------------------
-- Precedence graph

prec : List (∃₂ Operator) → List Precedence → Precedence
prec ops = precedence (λ fix → List.mapMaybe (hasFixity fix) ops)

mutual

  a  = prec ((-, -, atom) ∷ [])                        []
  pl = prec ((-, -, plus) ∷ [])                        (a ∷ [])
  ii = prec ((-, -, ifThen) ∷ (-, -, ifThenElse) ∷ []) (pl ∷ a ∷ [])
  c  = prec ((-, -, comma) ∷ [])                       (ii ∷ pl ∷ a ∷ [])
  wt = prec ((-, -, wellTyped) ∷ [])                   (c ∷ a ∷ [])

g : PrecedenceGraph
g = wt ∷ c ∷ ii ∷ pl ∷ a ∷ []

------------------------------------------------------------------------
-- Expressions

open PrecedenceCorrect acyclic g

• : ExprIn a non
• = ⟪ here P.refl ∙ [] ⟫

_+_ : Outer pl left → Expr (a ∷ []) → ExprIn pl left
e₁ + e₂ = e₁ ⟨ here P.refl ∙ [] ⟩ˡ e₂

i_t_ : Expr g → Outer ii right → ExprIn ii right
i e₁ t e₂ = ⟪ here P.refl ∙ e₁ ∷ [] ⟩ e₂

i_t_e_ : Expr g → Expr g → Outer ii right → ExprIn ii right
i e₁ t e₂ e e₃ = ⟪ there (here P.refl) ∙ e₁ ∷ e₂ ∷ [] ⟩ e₃

_,_ : Outer c left → Expr (ii ∷ pl ∷ a ∷ []) → ExprIn c left
e₁ , e₂ = e₁ ⟨ here P.refl ∙ [] ⟩ˡ e₂

_⊢_∶ : Outer wt left → Expr g → Expr g
e₁ ⊢ e₂ ∶ = here P.refl ∙ (e₁ ⟨ here P.refl ∙ [ e₂ ] ⟫)

------------------------------------------------------------------------
-- Some tests

open Show g

fromNameParts : List NamePart → String
fromNameParts = List.foldr _++_ ""

toNameParts : String → List NamePart
toNameParts = List.map (String.fromList ∘ L[_]) ∘ String.toList

data Backend : Set where
  depthFirst   : Backend
  breadthFirst : Backend

parse : ∀ {Tok e R} → Backend → Parser Tok e R → List Tok → List R
parse depthFirst   p = DepthFirst.parseComplete p
parse breadthFirst p = BreadthFirst.parse (Simplified.⟦_⟧ p)

parseExpr : Backend → String → List String
parseExpr backend = List.map (fromNameParts ∘ show) ∘
                    parse backend (Grammar.expression g) ∘
                    toNameParts

-- The breadth-first backend is considerably slower than the
-- depth-first one on these examples.
backend = depthFirst

runTest : String → List String → IO (⊤ {ℓ = Level.zero})
runTest s₁ s₂ = do
  putStrLn ("Testing: " ++ s₁)
  Colist.mapM′ putStrLn (Colist.fromList p₁)
  putStrLn (if ⌊ p₁ ≟ s₂ ⌋ then "Passed" else "Failed")
  where p₁ = parseExpr backend s₁

main = run do
  runTest "•+•⊢•∶"      []
  runTest "•,•⊢∶"       []
  runTest "•⊢•∶"        L[ "•⊢•∶" ]
  runTest "•,i•t•+•⊢•∶" L[ "•,i•t•+•⊢•∶" ]
  runTest "i•ti•t•e•"   ("i•ti•t•e•" ∷ "i•ti•t•e•" ∷ [])

ext: agda

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module List.Permutation.Base (A : Set) where

open import Data.List

data _/_⟶_ : List A → A → List A → Set where
  /head : {x : A}{xs : List A}
                   →  (x ∷ xs) / x ⟶ xs
  /tail : {x y : A}{xs ys : List A}
                   → xs / y ⟶ ys
                   → (x ∷ xs) / y ⟶ (x ∷ ys)

data _∼_ : List A → List A → Set where
  ∼[] : [] ∼ []
  ∼x : {x : A}{xs ys xs' ys' : List A}
                   → xs / x ⟶ xs'
                   → ys / x ⟶ ys'
                   → xs' ∼ ys'
                   → xs ∼ ys

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Groups.Subgroups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Ideals.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Ring R
open Setoid S
open Equivalence eq
open Group additiveGroup

open import Rings.Lemmas R
open import Rings.Divisible.Definition R

record Ideal {c : _} (pred : A → Set c) : Set (a ⊔ b ⊔ c) where
  field
    isSubgroup : Subgroup additiveGroup pred
    accumulatesTimes : {x : A} → {y : A} → pred x → pred (x * y)
  closedUnderPlus = Subgroup.closedUnderPlus isSubgroup
  closedUnderInverse = Subgroup.closedUnderInverse isSubgroup
  containsIdentity = Subgroup.containsIdentity isSubgroup
  isSubset = Subgroup.isSubset isSubgroup
  predicate = pred

generatedIdealPred : A → A → Set (a ⊔ b)
generatedIdealPred a b = a ∣ b

generatedIdeal : (a : A) → Ideal (generatedIdealPred a)
Subgroup.isSubset (Ideal.isSubgroup (generatedIdeal a)) {x} {y} x=y (c , prC) = c , transitive prC x=y
Subgroup.closedUnderPlus (Ideal.isSubgroup (generatedIdeal a)) {g} {h} (c , prC) (d , prD) = (c + d) , transitive *DistributesOver+ (+WellDefined prC prD)
Subgroup.containsIdentity (Ideal.isSubgroup (generatedIdeal a)) = 0G , timesZero
Subgroup.closedUnderInverse (Ideal.isSubgroup (generatedIdeal a)) {g} (c , prC) = inverse c , transitive ringMinusExtracts (inverseWellDefined additiveGroup prC)
Ideal.accumulatesTimes (generatedIdeal a) {x} {y} (c , prC) = (c * y) , transitive *Associative (*WellDefined prC reflexive)


text:
-- Note that the flag --guardedness-preserving-type-constructors is
-- not (should not be) enabled in this module.

module TypeConstructorsWhichPreserveGuardedness1 where

open import Common.Coinduction

record ⊤ : Set where

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

record ∃ {A : Set} (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

data Rec (A : ∞ Set) : Set where
  fold : ♭ A → Rec A

module ℕ₁ where

  -- Without the flag, the following is non-terminating,
  -- hence, not reduced.
  {-# NON_TERMINATING #-}
  ℕ : Set
  ℕ = ⊤ ⊎ Rec (♯ ℕ)

  zero : ℕ
  zero = inj₁ _  -- yields a type error since ℕ does not reduce

  suc : ℕ → ℕ
  suc n = inj₂ (fold n)

  ℕ-rec : (P : ℕ → Set) →
          P zero →
          (∀ n → P n → P (suc n)) →
          ∀ n → P n
  ℕ-rec P z s (inj₁ _)        = z
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)

module ℕ₂ where

  data ℕC : Set where
    ′zero : ℕC
    ′suc  : ℕC

  mutual

    ℕ : Set
    ℕ = ∃ λ (c : ℕC) → ℕ′ c

    ℕ′ : ℕC → Set
    ℕ′ ′zero = ⊤
    ℕ′ ′suc  = Rec (♯ ℕ)

  zero : ℕ
  zero = (′zero , _)

  suc : ℕ → ℕ
  suc n = (′suc , fold n)

  ℕ-rec : (P : ℕ → Set) →
          P zero →
          (∀ n → P n → P (suc n)) →
          ∀ n → P n
  ℕ-rec P z s (′zero , _)      = z
  ℕ-rec P z s (′suc  , fold n) = s n (ℕ-rec P z s n)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
-- The same name can not be exported more than once from a module.
module Issue154 where

module A where
  postulate X : Set

module B where
  postulate X : Set
  open A public

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.SuspensionMap

open import Cubical.ZCohomology.Base
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.GradedCommutativity
open import Cubical.ZCohomology.Gysin

open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
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.Data.Sigma
open import Cubical.Data.Int hiding (_+'_)
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _·_ to _·ℕ_)
open import Cubical.Data.Unit

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.GroupPath

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Truncation
open import Cubical.HITs.SetTruncation
  renaming (elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation

open PlusBis

-- The pushout describing the hopf invariant of the multiplication (∙Π) of
-- two maps (S³⁺²ⁿ →∙ S²⁺ⁿ)
C·Π : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n)) → Type _
C·Π n f g = Pushout (λ _ → tt) (∙Π f g .fst)

-- Another pushout, essentially the same, but starting with
-- S³⁺²ⁿ ∨ S³⁺²ⁿ. This will be used to break up the hopf invariant
-- of ∙Π f g.
C* : ∀ n → (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n)) → Type _
C* n f g = Pushout (λ _ → tt) (fst (∨→∙ f g))

-- The coequaliser of ∙Π and ∨→∙
θ : ∀ {ℓ} {A : Pointed ℓ} → Susp (fst A)
  → (Susp (fst A) , north) ⋁ (Susp (fst A) , north)
θ north = inl north
θ south = inr north
θ {A = A} (merid a i₁) =
     ((λ i → inl ((merid a ∙ sym (merid (pt A))) i))
  ∙∙ push tt
  ∙∙ λ i → inr ((merid a ∙ sym (merid (pt A))) i)) i₁

∙Π≡∨→∘θ : ∀ n → (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
     → (x : _) → ∙Π f g .fst x ≡ (f ∨→ g) (θ {A = S₊∙ _} x)
∙Π≡∨→∘θ n f g north = sym (snd f)
∙Π≡∨→∘θ n f g south = sym (snd g)
∙Π≡∨→∘θ n f g (merid a i₁) j = main j i₁
  where
  help : cong (f ∨→ g) (cong (θ {A = S₊∙ _}) (merid a))
       ≡ (refl ∙∙ cong (fst f) (merid a ∙ sym (merid north)) ∙∙ snd f)
       ∙ (sym (snd g) ∙∙ cong (fst g) (merid a ∙ sym (merid north)) ∙∙ refl)
  help = cong-∙∙ (f ∨→ g) ((λ i → inl ((merid a ∙ sym (merid north)) i)))
                           (push tt)
                           (λ i → inr ((merid a ∙ sym (merid north)) i))
      ∙∙ doubleCompPath≡compPath _ _ _
      ∙∙ cong (cong (f ∨→ g)
              (λ i₂ → inl ((merid a ∙ (λ i₃ → merid north (~ i₃))) i₂)) ∙_)
              (sym (assoc _ _ _))
      ∙∙ assoc _ _ _
      ∙∙ cong₂ _∙_ refl (compPath≡compPath' _ _)

  main : PathP (λ i → snd f (~ i)
                    ≡ snd g (~ i)) (λ i₁ → ∙Π f g .fst (merid a i₁))
               λ i₁ → (f ∨→ g) (θ {A = S₊∙ _} (merid a i₁))
  main = (λ i → ((λ j → snd f (~ i ∧ ~ j))
               ∙∙ cong (fst f) (merid a ∙ sym (merid north))
               ∙∙ snd f)
       ∙ (sym (snd g)
         ∙∙ cong (fst g) (merid a ∙ sym (merid north))
         ∙∙ λ j → snd g (~ i ∧ j)))
       ▷ sym help

private
  WedgeElim : ∀ {ℓ} (n : ℕ)
              {P : S₊∙ (3 +ℕ (n +ℕ n)) ⋁ S₊∙ (3 +ℕ (n +ℕ n)) → Type ℓ}
            → ((x : _) → isOfHLevel (3 +ℕ n) (P x))
            → P (inl north)
            → (x : _) → P x
  WedgeElim n {P = P} x s (inl x₁) =
    sphereElim _ {A = P ∘ inl}
      (λ _ → isOfHLevelPlus' {n = n} (3 +ℕ n) (x _)) s x₁
  WedgeElim n {P = P} x s (inr x₁) =
    sphereElim _ {A = P ∘ inr}
      (sphereElim _ (λ _ → isProp→isOfHLevelSuc ((suc (suc (n +ℕ n))))
        (isPropIsOfHLevel (suc (suc (suc (n +ℕ n))))))
          (subst (isOfHLevel ((3 +ℕ n) +ℕ n)) (cong P (push tt))
            (isOfHLevelPlus' {n = n} (3 +ℕ n) (x _))))
          (subst P (push tt) s) x₁
  WedgeElim n {P = P} x s (push a j) =
    transp (λ i → P (push tt (i ∧ j))) (~ j) s

H²C*≅ℤ : ∀ n → (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
     → GroupIso (coHomGr (2 +ℕ n) (C* n f g)) ℤGroup
H²C*≅ℤ n f g = compGroupIso is (Hⁿ-Sⁿ≅ℤ (suc n))
  where
  ∘inr : (coHom (2 +ℕ n) (C* n f g)) → coHom (2 +ℕ n) (S₊ (2 +ℕ n))
  ∘inr = sMap λ f → f ∘ inr

  invMapPrim : (S₊ (2 +ℕ n) → coHomK (2 +ℕ n))
             → C* n f g → coHomK (2 +ℕ n)
  invMapPrim h (inl x) = h (ptSn _)
  invMapPrim h (inr x) = h x
  invMapPrim h (push a i₁) =
    WedgeElim n {P = λ a → h north ≡ h (fst (∨→∙ f g) a)}
                (λ _ → isOfHLevelTrunc (4 +ℕ n) _ _)
                (cong h (sym (snd f))) a i₁

  invMap : coHom (2 +ℕ n) (S₊ (2 +ℕ n)) → (coHom (2 +ℕ n) (C* n f g))
  invMap = sMap invMapPrim

  ∘inrSect : (x : coHom (2 +ℕ n) (S₊ (2 +ℕ n))) → ∘inr (invMap x) ≡ x
  ∘inrSect = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
               λ a → refl

  ∘inrRetr : (x : (coHom (2 +ℕ n) (C* n f g))) → invMap (∘inr x) ≡ x
  ∘inrRetr =
    sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
      λ h → cong ∣_∣₂ (funExt λ { (inl x) → cong h ((λ i →  inr ((snd f) (~ i)))
                                                  ∙ sym (push (inl north)))
                                ; (inr x) → refl
                                ; (push a i) → lem₁ h a i})
    where
    lem₁ : (h : C* n f g → coHomK (2 +ℕ n)) (a : _)
         → PathP (λ i → invMapPrim (h ∘ inr) (push a i) ≡ h (push a i))
                  (cong h ((λ i →  inr ((snd f) (~ i)))
                         ∙ sym (push (inl north))))
                  refl
    lem₁ h =
      WedgeElim n (λ _ → isOfHLevelPathP (3 +ℕ n)
                           (isOfHLevelTrunc (4 +ℕ n) _ _) _ _)
         lem₂

      where
      lem₂ : PathP (λ i → invMapPrim (h ∘ inr) (push (inl north) i)
                         ≡ h (push (inl north) i))
                  (cong h ((λ i →  inr ((snd f) (~ i)))
                          ∙ sym (push (inl north))))
                  refl
      lem₂ i j = h (hcomp (λ k → λ { (i = i1) → inr (fst f north)
                                     ; (j = i0) → inr (snd f (~ i))
                                     ; (j = i1) → push (inl north) (i ∨ ~ k)})
                           (inr (snd f (~ i ∧ ~ j))))

  is : GroupIso (coHomGr (2 +ℕ n) (C* n f g)) (coHomGr (2 +ℕ n) (S₊ (2 +ℕ n)))
  Iso.fun (fst is) = ∘inr
  Iso.inv (fst is) = invMap
  Iso.rightInv (fst is) = ∘inrSect
  Iso.leftInv (fst is) = ∘inrRetr
  snd is = makeIsGroupHom
    (sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
           λ f g → refl)

H⁴-C·Π : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
        → GroupIso (coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C·Π n f g))
                    ℤGroup
H⁴-C·Π n f g = compGroupIso
  (transportCohomIso (cong (3 +ℕ_) (+-suc n n))) (Hopfβ-Iso n (∙Π f g))

H²-C·Π : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
      → GroupIso (coHomGr (2 +ℕ n) (C·Π n f g))
                  ℤGroup
H²-C·Π n f g = Hopfα-Iso n (∙Π f g)

H⁴-C* : ∀ n → (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
     → GroupIso (coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g))
                 (DirProd ℤGroup ℤGroup)
H⁴-C* n f g =
  compGroupIso (GroupEquiv→GroupIso (invGroupEquiv fstIso))
                  (compGroupIso (transportCohomIso (cong (2 +ℕ_) (+-suc n n)))
                    (compGroupIso (Hⁿ-⋁ (S₊∙ (suc (suc (suc (n +ℕ n)))))
                                        (S₊∙ (suc (suc (suc (n +ℕ n))))) _)
                      (GroupIsoDirProd (Hⁿ-Sⁿ≅ℤ _) (Hⁿ-Sⁿ≅ℤ _))))
  where
  module Ms = MV _ _ _ (λ _ → tt) (fst (∨→∙ f g))
  fstIso : GroupEquiv (coHomGr ((suc (suc (n +ℕ suc n))))
                               (S₊∙ (3 +ℕ (n +ℕ n)) ⋁ S₊∙ (3 +ℕ (n +ℕ n))))
                      (coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g))
  fst (fst fstIso) = Ms.d (suc (suc (n +ℕ suc n))) .fst
  snd (fst fstIso) =
    SES→isEquiv
      (sym (fst (GroupPath _ _)
        (isContr→≃Unit
          (isContrΣ (subst isContr (isoToPath (invIso (fst (Hⁿ-Unit≅0 _))))
                           isContrUnit)
             (λ _ → subst isContr (isoToPath (invIso
                           (fst (Hⁿ-Sᵐ≅0 _ _ λ p →
                                   ¬lemHopf 0 ((λ _ → north) , refl)
                                   n n (cong suc (sym (+-suc n n)) ∙ p)))))
                                   isContrUnit))
       , makeIsGroupHom λ _ _ → refl)))
      (GroupPath _ _ .fst
        (compGroupEquiv (invEquiv (isContr→≃Unit ((tt , tt) , (λ _ → refl)))
                                   , makeIsGroupHom λ _ _ → refl)
            (GroupEquivDirProd
             (GroupIso→GroupEquiv (invGroupIso (Hⁿ-Unit≅0 _)))
             (GroupIso→GroupEquiv
               (invGroupIso (Hⁿ-Sᵐ≅0 _ _ λ p →
                              ¬lemHopf 0 ((λ _ → north) , refl)
                              n (suc n) (cong (2 +ℕ_) (sym (+-suc n n))
                                                      ∙ p)))))))
      (Ms.Δ (suc (suc (n +ℕ suc n))))
      (Ms.d (suc (suc (n +ℕ suc n))))
      (Ms.i (suc (suc (suc (n +ℕ suc n)))))
      (Ms.Ker-d⊂Im-Δ _)
      (Ms.Ker-i⊂Im-d _)
  snd fstIso = Ms.d (suc (suc (n +ℕ suc n))) .snd

module _ (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n)) where

  C·Π' = C·Π n f g

  -- The generators of the cohomology groups of C* and C·Π

  βₗ : coHom ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g)
  βₗ = Iso.inv (fst (H⁴-C* n f g)) (1 , 0)

  βᵣ : coHom ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g)
  βᵣ = Iso.inv (fst (H⁴-C* n f g)) (0 , 1)

  β·Π : coHom ((2 +ℕ n) +' (2 +ℕ n)) C·Π'
  β·Π = Iso.inv (fst (H⁴-C·Π n f g)) 1

  α* : coHom (2 +ℕ n) (C* n f g)
  α* = Iso.inv (fst (H²C*≅ℤ n f g)) 1

  -- They can be difficult to work with in this form.
  -- We give them simpler forms and prove that these are equivalent
  βᵣ'-fun : C* n f g → coHomK ((4 +ℕ (n +ℕ n)))
  βᵣ'-fun (inl x) = 0ₖ _
  βᵣ'-fun (inr x) = 0ₖ _
  βᵣ'-fun (push (inl x) i₁) = 0ₖ _
  βᵣ'-fun (push (inr x) i₁) = Kn→ΩKn+1 _ ∣ x ∣ i₁
  βᵣ'-fun (push (push a i₂) i₁) = Kn→ΩKn+10ₖ _ (~ i₂) i₁

  βₗ'-fun : C* n f g → coHomK (4 +ℕ (n +ℕ n))
  βₗ'-fun (inl x) = 0ₖ _
  βₗ'-fun (inr x) = 0ₖ _
  βₗ'-fun (push (inl x) i₁) = Kn→ΩKn+1 _ ∣ x ∣ i₁
  βₗ'-fun (push (inr x) i₁) = 0ₖ _
  βₗ'-fun (push (push a i₂) i₁) = Kn→ΩKn+10ₖ _ i₂ i₁

  βₗ''-fun : coHom ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g)
  βₗ''-fun = subst (λ m → coHom m (C* n f g))
                   (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
                   ∣ βₗ'-fun ∣₂

  βᵣ''-fun : coHom ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g)
  βᵣ''-fun = subst (λ m → coHom m (C* n f g))
                   (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
                   ∣ βᵣ'-fun ∣₂

  private
    0ₖ≡∨→ : (a : _) → 0ₖ (suc (suc n)) ≡ ∣ (f ∨→ g) a ∣
    0ₖ≡∨→ = WedgeElim _ (λ _ → isOfHLevelTrunc (4 +ℕ n) _ _)
                   (cong ∣_∣ₕ (sym (snd f)))

  0ₖ≡∨→-inr : 0ₖ≡∨→ (inr north) ≡ cong ∣_∣ₕ (sym (snd g))
  0ₖ≡∨→-inr =
    (λ j → transport (λ i →  0ₖ (2 +ℕ n)
                          ≡ ∣ compPath-filler' (snd f) (sym (snd g)) (~ j) i ∣ₕ)
                      λ i → ∣ snd f (~ i ∨ j) ∣ₕ)
         ∙ λ j → transp (λ i → 0ₖ (2 +ℕ n) ≡ ∣ snd g (~ i ∧ ~ j) ∣ₕ) j
                         λ i → ∣ snd g (~ i ∨ ~ j) ∣ₕ

  α*'-fun : C* n f g → coHomK (2 +ℕ n)
  α*'-fun (inl x) = 0ₖ _
  α*'-fun (inr x) = ∣ x ∣
  α*'-fun (push a i₁) = 0ₖ≡∨→ a i₁

  α*' : coHom (2 +ℕ n) (C* n f g)
  α*' = ∣ α*'-fun ∣₂

  -- We also need the following three maps
  jₗ : HopfInvariantPush n (fst f) → C* n f g
  jₗ (inl x) = inl x
  jₗ (inr x) = inr x
  jₗ (push a i₁) = push (inl a) i₁

  jᵣ : HopfInvariantPush n (fst g) → C* n f g
  jᵣ (inl x) = inl x
  jᵣ (inr x) = inr x
  jᵣ (push a i₁) = push (inr a) i₁

  q : C·Π' → C* n f g
  q (inl x) = inl x
  q (inr x) = inr x
  q (push a i₁) = (push (θ a) ∙ λ i → inr (∙Π≡∨→∘θ n f g a (~ i))) i₁

α↦1 : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
        → Iso.fun (fst (H²C*≅ℤ n f g)) (α*' n f g) ≡ 1
α↦1 n f g =
     sym (cong (Iso.fun (fst (Hⁿ-Sⁿ≅ℤ (suc n)))) (Hⁿ-Sⁿ≅ℤ-nice-generator n))
   ∙ Iso.rightInv (fst (Hⁿ-Sⁿ≅ℤ (suc n))) (pos 1)

α≡ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
        → α* n f g ≡ α*' n f g
α≡ n f g = sym (Iso.leftInv (fst (H²C*≅ℤ n f g)) _)
             ∙∙ cong (Iso.inv (fst (H²C*≅ℤ n f g))) lem
             ∙∙ Iso.leftInv (fst (H²C*≅ℤ n f g)) _
  where
  lem : Iso.fun (fst (H²C*≅ℤ n f g)) (α* n f g)
       ≡ Iso.fun (fst (H²C*≅ℤ n f g)) (α*' n f g)
  lem = (Iso.rightInv (fst (H²C*≅ℤ n f g)) (pos 1)) ∙ sym (α↦1 n f g)

q-α : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (q n f g) (α* n f g) ≡ Hopfα n (∙Π f g)
q-α n f g = (λ i → coHomFun _ (q n f g) (α≡ n f g i))
          ∙ sym (Iso.leftInv is _)
          ∙∙ cong (Iso.inv is) lem
          ∙∙ Iso.leftInv is _
  where
  is = fst (Hopfα-Iso n (∙Π f g))

  lem : Iso.fun is (coHomFun _ (q n f g) (α*' n f g))
       ≡ Iso.fun is (Hopfα n (∙Π f g))
  lem = sym (cong (Iso.fun (fst (Hⁿ-Sⁿ≅ℤ (suc n)))) (Hⁿ-Sⁿ≅ℤ-nice-generator n))
      ∙∙ Iso.rightInv (fst (Hⁿ-Sⁿ≅ℤ (suc n))) (pos 1)
      ∙∙ sym (Hopfα-Iso-α n (∙Π f g))

βₗ≡ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → βₗ n f g ≡ βₗ''-fun n f g
βₗ≡ n f g = cong (∨-d ∘ subber₂)
                 (cong (Iso.inv (fst ((Hⁿ-⋁ (S₊∙ (suc (suc (suc (n +ℕ n)))))
                                            (S₊∙ (suc (suc (suc (n +ℕ n)))))
                                (((suc (suc (n +ℕ n))))))))) help
               ∙ lem)
          ∙ funExt⁻ ∨-d∘subber ∣ wedgeGen ∣₂
          ∙ cong subber₃ (sym βₗ'-fun≡)
  where
  ∨-d = MV.d _ _ _ (λ _ → tt) (fst (∨→∙ f g)) (suc (suc (n +ℕ suc n))) .fst
  ∨-d' = MV.d _ _ _ (λ _ → tt) (fst (∨→∙ f g)) (suc (suc (suc (n +ℕ n)))) .fst

  help : Iso.inv (fst (GroupIsoDirProd
                        (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n))))
                        (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n)))))) (1 , 0)
       ≡ (∣ ∣_∣ ∣₂ , 0ₕ _)
  help = ΣPathP ((Hⁿ-Sⁿ≅ℤ-nice-generator _)
       , IsGroupHom.pres1 (snd (invGroupIso (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n)))))))

  subber₃ = subst (λ m → coHom m (C* n f g))
                  (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))

  subber₂ = (subst (λ m → coHom m (S₊∙ (suc (suc (suc (n +ℕ n))))
                                  ⋁ S₊∙ (suc (suc (suc (n +ℕ n))))))
                   (sym (cong (2 +ℕ_) (+-suc n n))))

  ∨-d∘subber : ∨-d ∘ subber₂ ≡ subber₃ ∘ ∨-d'
  ∨-d∘subber =
    funExt (λ a →
      (λ j → transp (λ i → coHom ((suc ∘ suc ∘ suc) (+-suc n n (~ i ∧ j)))
                                  (C* n f g)) (~ j)
               (MV.d _ _ _ (λ _ → tt) (fst (∨→∙ f g))
                           (suc (suc (+-suc n n j))) .fst
                  (transp (λ i → coHom (2 +ℕ (+-suc n n (j ∨ ~ i)))
                                          (S₊∙ (suc (suc (suc (n +ℕ n))))
                                         ⋁ S₊∙ (suc (suc (suc (n +ℕ n)))))) j
                          a))))

  wedgeGen : (S₊∙ (suc (suc (suc (n +ℕ n)))) ⋁ S₊∙ (suc (suc (suc (n +ℕ n))))
           → coHomK (suc (suc (suc (n +ℕ n)))))
  wedgeGen (inl x) = ∣ x ∣
  wedgeGen (inr x) = 0ₖ _
  wedgeGen (push a i₁) = 0ₖ _

  βₗ'-fun≡ : ∣ βₗ'-fun n f g ∣₂ ≡ ∨-d' ∣ wedgeGen ∣₂
  βₗ'-fun≡ =
    cong ∣_∣₂ (funExt λ { (inl x) → refl
                       ; (inr x) → refl
                       ; (push (inl x) i₁) → refl
                       ; (push (inr x) i₁) j → Kn→ΩKn+10ₖ _ (~ j) i₁
                       ; (push (push a i₂) i₁) j → Kn→ΩKn+10ₖ _ (~ j ∧ i₂) i₁})

  lem : Iso.inv (fst (Hⁿ-⋁ (S₊∙ (suc (suc (suc (n +ℕ n)))))
                           (S₊∙ (suc (suc (suc (n +ℕ n)))))
                           (((suc (suc (n +ℕ n)))))))
                   (∣ ∣_∣ ∣₂ , 0ₕ _)
                   ≡ ∣ wedgeGen ∣₂
  lem = cong ∣_∣₂ (funExt λ { (inl x) → rUnitₖ (suc (suc (suc (n +ℕ n)))) ∣ x ∣
                           ; (inr x) → refl
                           ; (push a i₁) → refl})

βᵣ≡ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → βᵣ n f g ≡ βᵣ''-fun n f g
βᵣ≡ n f g =
    cong (∨-d ∘ subber₂)
      (cong (Iso.inv (fst (Hⁿ-⋁ (S₊∙ (suc (suc (suc (n +ℕ n)))))
                                 (S₊∙ (suc (suc (suc (n +ℕ n)))))
                                (suc (suc (n +ℕ n))))))
            help
          ∙ lem)
  ∙ funExt⁻ ∨-d∘subber ∣ wedgeGen ∣₂
  ∙ cong (subber₃) (sym βᵣ'-fun≡)
  where
  ∨-d = MV.d _ _ _ (λ _ → tt) (fst (∨→∙ f g)) (suc (suc (n +ℕ suc n))) .fst
  ∨-d' = MV.d _ _ _ (λ _ → tt) (fst (∨→∙ f g)) (suc (suc (suc (n +ℕ n)))) .fst

  help : Iso.inv (fst (GroupIsoDirProd
                       (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n))))
                       (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n)))))) (0 , 1)
       ≡ (0ₕ _ , ∣ ∣_∣ ∣₂)
  help =
    ΣPathP (IsGroupHom.pres1 (snd (invGroupIso (Hⁿ-Sⁿ≅ℤ (suc (suc (n +ℕ n))))))
         , (Hⁿ-Sⁿ≅ℤ-nice-generator _))

  subber₃ = subst (λ m → coHom m (C* n f g))
                  (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))

  subber₂ = (subst (λ m → coHom m (S₊∙ (suc (suc (suc (n +ℕ n))))
                                 ⋁ S₊∙ (suc (suc (suc (n +ℕ n))))))
                   (sym (cong (2 +ℕ_) (+-suc n n))))

  ∨-d∘subber : ∨-d ∘ subber₂ ≡ subber₃ ∘ ∨-d'
  ∨-d∘subber =
    funExt (λ a →
      (λ j → transp (λ i → coHom ((suc ∘ suc ∘ suc) (+-suc n n (~ i ∧ j)))
                     (C* n f g)) (~ j)
               (MV.d _ _ _ (λ _ → tt)
                 (fst (∨→∙ f g)) (suc (suc (+-suc n n j))) .fst
                  (transp (λ i → coHom (2 +ℕ (+-suc n n (j ∨ ~ i)))
                                        (S₊∙ (suc (suc (suc (n +ℕ n))))
                                       ⋁ S₊∙ (suc (suc (suc (n +ℕ n)))))) j
                          a))))

  wedgeGen : (S₊∙ (suc (suc (suc (n +ℕ n)))) ⋁ S₊∙ (suc (suc (suc (n +ℕ n))))
      → coHomK (suc (suc (suc (n +ℕ n)))))
  wedgeGen (inl x) = 0ₖ _
  wedgeGen (inr x) = ∣ x ∣
  wedgeGen (push a i₁) = 0ₖ _

  lem : Iso.inv (fst ((Hⁿ-⋁ (S₊∙ (suc (suc (suc (n +ℕ n)))))
                            (S₊∙ (suc (suc (suc (n +ℕ n)))))
                            (suc (suc (n +ℕ n))))))
                   (0ₕ _ , ∣ ∣_∣ ∣₂)
                   ≡ ∣ wedgeGen ∣₂
  lem = cong ∣_∣₂ (funExt λ { (inl x) → refl
                          ; (inr x) → lUnitₖ (suc (suc (suc (n +ℕ n)))) ∣ x ∣
                          ; (push a i₁) → refl})

  βᵣ'-fun≡ : ∣ βᵣ'-fun n f g ∣₂ ≡ ∨-d' ∣ wedgeGen ∣₂
  βᵣ'-fun≡ =
    cong ∣_∣₂ (funExt
      λ { (inl x) → refl
         ; (inr x) → refl
         ; (push (inl x) i₁) j → Kn→ΩKn+10ₖ _ (~ j) i₁
         ; (push (inr x) i₁) → refl
         ; (push (push a i₂) i₁) j → Kn→ΩKn+10ₖ _ (~ j ∧ ~ i₂) i₁})

q-βₗ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (q n f g) (βₗ n f g)
    ≡ β·Π n f g
q-βₗ n f g = cong (coHomFun _ (q n f g)) (βₗ≡ n f g)
           ∙ transportLem
           ∙ cong (subst (λ m → coHom m (C·Π' n f g))
                  (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
                        (sym (Iso.leftInv (fst (Hopfβ-Iso n (∙Π f g)))
                                               (Hopfβ n (∙Π f g)))
                        ∙ cong (Iso.inv ((fst (Hopfβ-Iso n (∙Π f g)))))
                               (Hopfβ↦1 n (∙Π f g)))
  where
  transportLem : coHomFun (suc (suc (suc (n +ℕ suc n)))) (q n f g)
      (βₗ''-fun n f g)
     ≡ subst (λ m → coHom m (C·Π' n f g))
             (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
             (Hopfβ n (∙Π f g))
  transportLem =
      natTranspLem ∣ βₗ'-fun n f g ∣₂ (λ m → coHomFun m (q n f g))
           (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
    ∙ cong (subst (λ m → coHom m (C·Π' n f g))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
        (cong ∣_∣₂ (funExt λ { (inl x) → refl
                            ; (inr x) → refl
                            ; (push a i₁) → push-lem a i₁}))
    where
    push-lem : (x : fst (S₊∙ (3 +ℕ (n +ℕ n)))) →
      PathP (λ i₁ → βₗ'-fun n f g ((push (θ x)
                   ∙ λ i → inr (∙Π≡∨→∘θ n f g x (~ i))) i₁)
                 ≡ MV.d-pre Unit (fst (S₊∙ (2 +ℕ n))) (fst (S₊∙ (3 +ℕ n +ℕ n)))
                     (λ _ → tt) (fst (∙Π f g)) (3 +ℕ n +ℕ n) ∣_∣ (push x i₁))
      (λ _ → βₗ'-fun n f g (q n f g (inl tt)))
      (λ _ → βₗ'-fun n f g (q n f g (inr (∙Π f g .fst x))))
    push-lem x =
      flipSquare (cong-∙ (βₗ'-fun n f g)
                         (push (θ x)) (λ i → inr (∙Π≡∨→∘θ n f g x (~ i)))
              ∙∙ sym (rUnit _)
              ∙∙ lem₁ x)

      where
      lem₁ : (x : _) → cong (βₗ'-fun n f g) (push (θ {A = S₊∙ _} x))
                      ≡ Kn→ΩKn+1 _ ∣ x ∣
      lem₁ north = refl
      lem₁ south =
          sym (Kn→ΩKn+10ₖ _)
        ∙ cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n))))) (cong ∣_∣ₕ (merid north))
      lem₁ (merid a j) k = merid-lem k j
        where
        p = pt (S₊∙ (suc (suc (n +ℕ n))))

        merid-lem :
          PathP (λ k → Kn→ΩKn+1 _ ∣ north ∣ₕ
                      ≡ (sym (Kn→ΩKn+10ₖ _)
                       ∙ cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))))
                              (cong ∣_∣ₕ (merid north))) k)
             (λ j → cong (βₗ'-fun n f g) (push (θ {A = S₊∙ _} (merid a j))))
             (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ) (merid a))
        merid-lem =
           (cong-∙∙ (cong (βₗ'-fun n f g) ∘ push)
                          (λ i₁ → inl ((merid a ∙ (sym (merid p))) i₁))
                    (push tt)
                         ((λ i₁ → inr ((merid a ∙ (sym (merid p))) i₁)))
         ∙ sym (compPath≡compPath' _ _)
         ∙ cong (_∙ Kn→ΩKn+10ₖ _)
                (cong-∙ ((Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ))
                        (merid a) (sym (merid north)))
         ∙ sym (assoc _ _ _)
         ∙ cong (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ) (merid a) ∙_)
                (sym (symDistr (sym ((Kn→ΩKn+10ₖ _)))
                       (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))))
                             (cong ∣_∣ₕ (merid north))))))
         ◁ λ i j → compPath-filler
           (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ) (merid a))
                 (sym (sym (Kn→ΩKn+10ₖ _)
                 ∙ cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))))
                        (cong ∣_∣ₕ (merid north))))
                 (~ i) j

q-βᵣ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (q n f g) (βᵣ n f g)
    ≡ β·Π n f g
q-βᵣ n f g = cong (coHomFun _ (q n f g)) (βᵣ≡ n f g)
           ∙ transportLem
           ∙ cong (subst (λ m → coHom m (C·Π' n f g))
                  (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
                        (sym (Iso.leftInv (fst (Hopfβ-Iso n (∙Π f g)))
                                               (Hopfβ n (∙Π f g)))
                        ∙ cong (Iso.inv ((fst (Hopfβ-Iso n (∙Π f g)))))
                               (Hopfβ↦1 n (∙Π f g)))
  where
  transportLem : coHomFun (suc (suc (suc (n +ℕ suc n)))) (q n f g)
      (βᵣ''-fun n f g)
     ≡ subst (λ m → coHom m (C·Π' n f g))
             (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
             (Hopfβ n (∙Π f g))
  transportLem =
      natTranspLem ∣ βᵣ'-fun n f g ∣₂ (λ m → coHomFun m (q n f g))
            (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
    ∙ cong (subst (λ m → coHom m (C·Π' n f g))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
        (cong ∣_∣₂ (funExt λ { (inl x) → refl
                            ; (inr x) → refl
                            ; (push a i₁) → push-lem a i₁}))
    where
    push-lem : (x : fst (S₊∙ (3 +ℕ (n +ℕ n)))) →
      PathP
      (λ i₁ →
         βᵣ'-fun n f g ((push (θ x) ∙ λ i → inr (∙Π≡∨→∘θ n f g x (~ i))) i₁) ≡
         MV.d-pre Unit (fst (S₊∙ (2 +ℕ n))) (fst (S₊∙ (3 +ℕ n +ℕ n)))
         (λ _ → tt) (fst (∙Π f g)) (3 +ℕ n +ℕ n) ∣_∣ (push x i₁))
      (λ _ → βᵣ'-fun n f g (q n f g (inl tt)))
      (λ _ → βᵣ'-fun n f g (q n f g (inr (∙Π f g .fst x))))
    push-lem x = flipSquare (cong-∙ (βᵣ'-fun n f g) (push (θ x))
                                    (λ i → inr (∙Π≡∨→∘θ n f g x (~ i)))
              ∙∙ sym (rUnit _)
              ∙∙ lem₁ x)
      where
      lem₁ : (x : _) → cong (βᵣ'-fun n f g) (push (θ {A = S₊∙ _} x))
                      ≡ Kn→ΩKn+1 _ ∣ x ∣
      lem₁ north = sym (Kn→ΩKn+10ₖ _)
      lem₁ south = cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))))
                        (cong ∣_∣ₕ (merid north))
      lem₁ (merid a j) k = merid-lem k j
        where
        p = pt (S₊∙ (suc (suc (n +ℕ n))))

        merid-lem :
          PathP (λ k → (Kn→ΩKn+10ₖ _) (~ k)
                      ≡ (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))))
                              (cong ∣_∣ₕ (merid north))) k)
                (λ j → cong (βᵣ'-fun n f g) (push (θ {A = S₊∙ _} (merid a j))))
                (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ) (merid a))
        merid-lem =
          (cong-∙∙ (cong (βᵣ'-fun n f g) ∘ push)
                        (λ i₁ → inl ((merid a
                                    ∙ (sym (merid p))) i₁))
                        (push tt)
                        (λ i₁ → inr ((merid a
                                    ∙ (sym (merid p))) i₁))
             ∙∙ (cong (sym (Kn→ΩKn+10ₖ _) ∙_)
                      (cong-∙ (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ)
                              (merid a) (sym (merid (ptSn _)))))
             ∙∙ sym (doubleCompPath≡compPath _ _ _))
             ◁ symP (doubleCompPath-filler
                      (sym (Kn→ΩKn+10ₖ _))
                      (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ)
                            (merid a))
                      (cong (Kn→ΩKn+1 (suc (suc (suc (n +ℕ n)))) ∘ ∣_∣ₕ)
                            (sym (merid north))))

jₗ-α : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jₗ n f g) (α* n f g)
    ≡ Hopfα n f
jₗ-α n f g =
    cong (coHomFun _ (jₗ n f g)) (α≡ n f g)
  ∙ cong ∣_∣₂ (funExt (HopfInvariantPushElim n (fst f)
                      (isOfHLevelPath ((suc (suc (suc (suc (n +ℕ n))))))
                        (isOfHLevelPlus' {n = n} (4 +ℕ n)
                          (isOfHLevelTrunc (4 +ℕ n))) _ _)
                      refl
                      (λ _ → refl)
                      λ j → refl))

jₗ-βₗ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jₗ n f g) (βₗ n f g)
    ≡ subst (λ m → coHom m (HopfInvariantPush n (fst f)))
            (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
            (Hopfβ n f)
jₗ-βₗ n f g =
     cong (coHomFun _ (jₗ n f g)) (βₗ≡ n f g)
  ∙∙ natTranspLem ∣ βₗ'-fun n f g ∣₂ (λ m → coHomFun m (jₗ n f g))
          (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
  ∙∙ cong (subst (λ m → coHom m (HopfInvariantPush n (fst f)))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
        (cong ∣_∣₂
          (funExt λ { (inl x) → refl
                    ; (inr x) → refl
                    ; (push a i₁) → refl}))

jₗ-βᵣ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jₗ n f g) (βᵣ n f g)
    ≡ 0ₕ _
jₗ-βᵣ n f g =
  cong (coHomFun _ (jₗ n f g)) (βᵣ≡ n f g)
  ∙∙ natTranspLem ∣ βᵣ'-fun n f g ∣₂ (λ m → coHomFun m (jₗ n f g))
          (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
  ∙∙ cong (subst (λ m → coHom m (HopfInvariantPush n (fst f)))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
      cool
  where
  cool : coHomFun (suc (suc (suc (suc (n +ℕ n))))) (jₗ n f g)
      ∣ βᵣ'-fun n f g ∣₂ ≡ 0ₕ _
  cool = cong ∣_∣₂ (funExt λ { (inl x) → refl
                            ; (inr x) → refl
                            ; (push a i₁) → refl})

jᵣ-α : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jᵣ n f g) (α* n f g)
    ≡ Hopfα n g
jᵣ-α n f g = cong (coHomFun _ (jᵣ n f g)) (α≡ n f g)
  ∙ cong ∣_∣₂ (funExt (HopfInvariantPushElim n (fst g)
                      (isOfHLevelPath ((suc (suc (suc (suc (n +ℕ n))))))
                        (isOfHLevelPlus' {n = n} (4 +ℕ n)
                          (isOfHLevelTrunc (4 +ℕ n))) _ _)
                      refl
                      (λ _ → refl)
                      (flipSquare (0ₖ≡∨→-inr n f g))))

jᵣ-βₗ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jᵣ n f g) (βₗ n f g) ≡ 0ₕ _
jᵣ-βₗ n f g =
  cong (coHomFun _ (jᵣ n f g)) (βₗ≡ n f g)
  ∙∙ natTranspLem ∣ βₗ'-fun n f g ∣₂ (λ m → coHomFun m (jᵣ n f g))
            (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
  ∙∙ cong (subst (λ m → coHom m (HopfInvariantPush n (fst f)))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
      cool
  where
  cool : coHomFun (suc (suc (suc (suc (n +ℕ n))))) (jᵣ n f g)
      ∣ βₗ'-fun n f g ∣₂ ≡ 0ₕ _
  cool = cong ∣_∣₂ (funExt λ { (inl x) → refl
                            ; (inr x) → refl
                            ; (push a i₁) → refl})

jᵣ-βᵣ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
    → coHomFun _ (jᵣ n f g) (βᵣ n f g)
    ≡ subst (λ m → coHom m (HopfInvariantPush n (fst g)))
            (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
            (Hopfβ n g)
jᵣ-βᵣ n f g =
  cong (coHomFun _ (jᵣ n f g)) (βᵣ≡ n f g)
  ∙∙ natTranspLem ∣ βᵣ'-fun n f g ∣₂ (λ m → coHomFun m (jᵣ n f g))
            (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
  ∙∙  cong (subst (λ m → coHom m (HopfInvariantPush n (fst g)))
      (cong (suc ∘ suc ∘ suc) (sym (+-suc n n))))
        (cong ∣_∣₂
          (funExt λ { (inl x) → refl
                    ; (inr x) → refl
                    ; (push a i₁) → refl}))

genH²ⁿC* : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
         → gen₂-by (coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g))
                    (βₗ n f g)
                    (βᵣ n f g)
genH²ⁿC* n f g =
  Iso-pres-gen₂ (DirProd ℤGroup ℤGroup)
    (coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g))
    (1 , 0)
    (0 , 1)
    gen₂ℤ×ℤ
    (invGroupIso (H⁴-C* n f g))

private
  H⁴C* : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n)) → Group _
  H⁴C* n f g = coHomGr ((2 +ℕ n) +' (2 +ℕ n)) (C* n f g)

  X : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
      → ℤ
  X n f g = (genH²ⁿC* n f g) (α* n f g ⌣ α* n f g) .fst .fst

  Y : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
      → ℤ
  Y n  f g = (genH²ⁿC* n f g) (α* n f g ⌣ α* n f g) .fst .snd

  α*≡⌣ : (n : ℕ) (f g : S₊∙ (3 +ℕ (n +ℕ n)) →∙ S₊∙ (2 +ℕ n))
      → α* n f g ⌣ α* n f g ≡ ((X n f g) ℤ[ H⁴C* n f g ]· βₗ n f g)
                            +ₕ ((Y n f g) ℤ[ H⁴C* n f g ]· βᵣ n f g)
  α*≡⌣ n f g = (genH²ⁿC* n f g) (α* n f g ⌣ α* n f g) .snd

coHomFun⌣ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B)
          → (n : ℕ) (x y : coHom n B)
          → coHomFun _ f (x ⌣ y) ≡ coHomFun _ f x ⌣ coHomFun _ f y
coHomFun⌣ f n = sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _) λ _ _ → refl

isHom-HopfInvariant :
          (n : ℕ) (f g : S₊∙ (suc (suc (suc (n +ℕ n)))) →∙ S₊∙ (suc (suc n)))
        → HopfInvariant n (∙Π f g) ≡ HopfInvariant n f + HopfInvariant n g
isHom-HopfInvariant n f g =
      mainL
   ∙ sym (cong₂ _+_ f-id g-id)
  where
  eq₁ : (Hopfα n (∙Π f g)) ⌣ (Hopfα n (∙Π f g))
      ≡ ((X n f g + Y n f g) ℤ[ coHomGr _ _ ]· (β·Π n f g))
  eq₁ = cong (λ x → x ⌣ x) (sym (q-α n f g)
                           ∙ cong (coHomFun (suc (suc n)) (q n f g)) (α≡ n f g))
      ∙ cong ((coHomFun _) (q _ f g)) (cong (λ x → x ⌣ x) (sym (α≡ n f g))
                           ∙ α*≡⌣ n f g)
      ∙ IsGroupHom.pres· (coHomMorph _ (q n f g) .snd) _ _
      ∙ cong₂ _+ₕ_ (homPresℤ· (coHomMorph _ (q n f g)) (βₗ n f g) (X n f g)
                           ∙ cong (λ z → (X n f g) ℤ[ coHomGr _ _ ]· z)
                                  (q-βₗ n f g))
                   (homPresℤ· (coHomMorph _ (q n f g)) (βᵣ n f g) (Y n f g)
                           ∙ cong (λ z → (Y n f g) ℤ[ coHomGr _ _ ]· z)
                                  (q-βᵣ n f g))
      ∙ sym (distrℤ· (coHomGr _ _) (β·Π n f g) (X n f g) (Y n f g))

  eq₂ : Hopfα n f ⌣ Hopfα n f
      ≡ (X n f g ℤ[ coHomGr _ _ ]·
                   subst (λ m → coHom m (HopfInvariantPush n (fst f)))
                   (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
                   (Hopfβ n f))
  eq₂ = cong (λ x → x ⌣ x) (sym (jₗ-α n f g))
     ∙∙ sym (coHomFun⌣ (jₗ n f g) _ _ _)
     ∙∙ cong (coHomFun _ (jₗ n f g)) (α*≡⌣ n f g)
     ∙∙ IsGroupHom.pres· (snd (coHomMorph _ (jₗ n f g))) _ _
     ∙∙ cong₂ _+ₕ_ (homPresℤ· (coHomMorph _ (jₗ n f g)) (βₗ n f g) (X n f g))
                   (homPresℤ· (coHomMorph _ (jₗ n f g)) (βᵣ n f g) (Y n f g)
                             ∙ cong (λ z → (Y n f g) ℤ[ coHomGr _ _ ]· z)
                                    (jₗ-βᵣ n f g))
     ∙∙ cong₂ _+ₕ_ refl (rUnitℤ· (coHomGr _ _) (Y n f g))
     ∙∙ (rUnitₕ _ _
      ∙ cong (X n f g ℤ[ coHomGr _ _ ]·_) (jₗ-βₗ n f g))

  eq₃ : Hopfα n g ⌣ Hopfα n g
      ≡ (Y n f g ℤ[ coHomGr _ _ ]·
                   subst (λ m → coHom m (HopfInvariantPush n (fst f)))
                   (cong (suc ∘ suc ∘ suc) (sym (+-suc n n)))
                   (Hopfβ n g))
  eq₃ = cong (λ x → x ⌣ x) (sym (jᵣ-α n f g))
     ∙∙ sym (coHomFun⌣ (jᵣ n f g) _ _ _)
     ∙∙ cong (coHomFun _ (jᵣ n f g)) (α*≡⌣ n f g)
     ∙∙ IsGroupHom.pres· (snd (coHomMorph _ (jᵣ n f g))) _ _
     ∙∙ cong₂ _+ₕ_ (homPresℤ· (coHomMorph _ (jᵣ n f g)) (βₗ n f g) (X n f g)
                             ∙ cong (λ z → (X n f g) ℤ[ coHomGr _ _ ]· z)
                                    (jᵣ-βₗ n f g))
                   (homPresℤ· (coHomMorph _ (jᵣ n f g)) (βᵣ n f g) (Y n f g))
     ∙∙ cong₂ _+ₕ_ (rUnitℤ· (coHomGr _ _) (X n f g)) refl
     ∙∙ ((lUnitₕ _ _) ∙ cong (Y n f g ℤ[ coHomGr _ _ ]·_) (jᵣ-βᵣ n f g))

  transpLem : ∀ {ℓ} {G : ℕ → Group ℓ} (n m : ℕ) (x : ℤ) (p : m ≡ n)
              (g : fst (G n))
             → subst (fst ∘ G) p (x ℤ[ G m ]· subst (fst ∘ G) (sym p) g)
              ≡ (x ℤ[ G n ]· g)
  transpLem {G = G} n m x =
    J (λ n p → (g : fst (G n))
             → subst (fst ∘ G) p (x ℤ[ G m ]· subst (fst ∘ G) (sym p) g)
              ≡ (x ℤ[ G n ]· g))
      λ g → transportRefl _ ∙ cong (x ℤ[ G m ]·_) (transportRefl _)

  mainL : HopfInvariant n (∙Π f g) ≡ X n f g + Y n f g
  mainL =
       cong (Iso.fun (fst (Hopfβ-Iso n (∙Π f g))))
            (cong (subst (λ x → coHom x (HopfInvariantPush n (fst (∙Π f g))))
                         λ i₁ → suc (suc (suc (+-suc n n i₁))))
                  eq₁)
    ∙∙ cong (Iso.fun (fst (Hopfβ-Iso n (∙Π f g))))
        (transpLem {G = λ x → coHomGr x
                                (HopfInvariantPush n (fst (∙Π f g)))} _ _
                   (X n f g + Y n f g)
                   (λ i₁ → suc (suc (suc (+-suc n n i₁))))
                   (Iso.inv (fst (Hopfβ-Iso n (∙Π f g))) 1))
    ∙∙ homPresℤ· (_ , snd (Hopfβ-Iso n (∙Π f g)))
                 (Iso.inv (fst (Hopfβ-Iso n (∙Π f g))) 1)
                 (X n f g + Y n f g)
    ∙∙ cong ((X n f g + Y n f g) ℤ[ ℤ , ℤGroup .snd ]·_)
            (Iso.rightInv ((fst (Hopfβ-Iso n (∙Π f g)))) 1)
    ∙∙ rUnitℤ·ℤ (X n f g + Y n f g)

  f-id :  HopfInvariant n f ≡ X n f g
  f-id =
      cong (Iso.fun (fst (Hopfβ-Iso n f)))
      (cong (subst (λ x → coHom x (HopfInvariantPush n (fst f)))
            (λ i₁ → suc (suc (suc (+-suc n n i₁))))) eq₂)
    ∙ cong (Iso.fun (fst (Hopfβ-Iso n f)))
           (transpLem {G = λ x → coHomGr x
                           (HopfInvariantPush n (fst f))} _ _
                      (X n f g)
                      ((cong (suc ∘ suc ∘ suc) (+-suc n n)))
                      (Hopfβ n f))
    ∙ homPresℤ· (_ , snd (Hopfβ-Iso n f)) (Hopfβ n f) (X n f g)
    ∙ cong (X n f g ℤ[ ℤ , ℤGroup .snd ]·_) (Hopfβ↦1 n f)
    ∙ rUnitℤ·ℤ (X n f g)

  g-id : HopfInvariant n g ≡ Y n f g
  g-id =
       cong (Iso.fun (fst (Hopfβ-Iso n g)))
            (cong (subst (λ x → coHom x (HopfInvariantPush n (fst g)))
                      (λ i₁ → suc (suc (suc (+-suc n n i₁)))))
                      eq₃)
    ∙∙ cong (Iso.fun (fst (Hopfβ-Iso n g)))
                   (transpLem {G = λ x → coHomGr x
                                           (HopfInvariantPush n (fst g))} _ _
                              (Y n f g)
                              ((cong (suc ∘ suc ∘ suc) (+-suc n n)))
                              (Hopfβ n g))
    ∙∙ homPresℤ· (_ , snd (Hopfβ-Iso n g)) (Hopfβ n g) (Y n f g)
    ∙∙ cong (Y n f g ℤ[ ℤ , ℤGroup .snd ]·_) (Hopfβ↦1 n g)
    ∙∙ rUnitℤ·ℤ (Y n f g)

GroupHom-HopfInvariant-π' : (n : ℕ)
  → GroupHom (π'Gr (suc (suc (n +ℕ n))) (S₊∙ (suc (suc n)))) ℤGroup
fst (GroupHom-HopfInvariant-π' n) = HopfInvariant-π' n
snd (GroupHom-HopfInvariant-π' n) =
  makeIsGroupHom (sElim2 (λ _ _ → isOfHLevelPath 2 isSetℤ _ _)
                 (isHom-HopfInvariant n))

GroupHom-HopfInvariant-π : (n : ℕ)
  → GroupHom (πGr (suc (suc (n +ℕ n))) (S₊∙ (suc (suc n)))) ℤGroup
fst (GroupHom-HopfInvariant-π n) = HopfInvariant-π n
snd (GroupHom-HopfInvariant-π n) =
  makeIsGroupHom (sElim2 (λ _ _ → isOfHLevelPath 2 isSetℤ _ _)
    λ p q → cong (HopfInvariant-π' n)
                  (IsGroupHom.pres·
                    (snd (invGroupIso (π'Gr≅πGr (suc (suc (n +ℕ n)))
                                                (S₊∙ (suc (suc n))))))
                                    ∣ p ∣₂ ∣ q ∣₂)
          ∙ IsGroupHom.pres· (GroupHom-HopfInvariant-π' n .snd)
                             ∣ Ω→SphereMap _ p ∣₂ ∣ Ω→SphereMap _ q ∣₂)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma

module lib.types.Pointed where

Ptd : ∀ i → Type (lsucc i)
Ptd i = Σ (Type i) (λ A → A)

Ptd₀ = Ptd lzero

⊙[_,_] : ∀ {i} (A : Type i) (a : A) → Ptd i
⊙[_,_] = _,_

_⊙→_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
(A , a₀) ⊙→ (B , b₀) = ⊙[ Σ (A → B) (λ f → f a₀ == b₀) , ((λ _ → b₀), idp) ]

infixr 0 _⊙→_

_⊙×_ : ∀ {i j} → Ptd i → Ptd j → Ptd (lmax i j)
(A , a₀) ⊙× (B , b₀) = (A × B , (a₀ , b₀))

⊙fst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙× Y ⊙→ X)
⊙fst = (fst , idp)

⊙snd : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙× Y ⊙→ Y)
⊙snd = (snd , idp)

⊙diag : ∀ {i} {X : Ptd i} → fst (X ⊙→ X ⊙× X)
⊙diag = ((λ x → (x , x)) , idp)

pair⊙→ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  → fst (X ⊙→ Y) → fst (Z ⊙→ W)
  → fst ((X ⊙× Z) ⊙→ (Y ⊙× W))
pair⊙→ (f , fpt) (g , gpt) =
  ((λ {(x , z) → (f x , g z)}) , pair×= fpt gpt)

infixr 4 _⊙∘_

⊙idf : ∀ {i} (X : Ptd i) → fst (X ⊙→ X)
⊙idf A = ((λ x → x) , idp)

⊙cst : ∀ {i j} {X : Ptd i} {Y : Ptd j} → fst (X ⊙→ Y)
⊙cst {Y = Y} = ((λ x → snd Y) , idp)

_⊙∘_ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y)) → fst (X ⊙→ Z)
(g , gpt) ⊙∘ (f , fpt) = (g ∘ f) , (ap g fpt ∙ gpt)

⊙∘-unit-l : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : fst (X ⊙→ Y))
  → ⊙idf Y ⊙∘ f == f
⊙∘-unit-l (f , idp) = idp

⊙∘-assoc : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (h : fst (Z ⊙→ W)) (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
  → ((h ⊙∘ g) ⊙∘ f) == (h ⊙∘ (g ⊙∘ f))
⊙∘-assoc (h , hpt) (g , gpt) (f , fpt) = pair= idp (lemma fpt gpt hpt)
  where
  lemma : ∀ {x₁ x₂} (fpt : x₁ == x₂) → ∀ gpt → ∀ hpt →
          ap (h ∘ g) fpt ∙ ap h gpt ∙ hpt == ap h (ap g fpt ∙ gpt) ∙ hpt
  lemma idp gpt hpt = idp

{- Obtaining equality of pointed types from an equivalence -}
⊙ua : ∀ {i} {A B : Type i} {a₀ : A} {b₀ : B}
  (e : A ≃ B) → –> e a₀ == b₀ → ⊙[ A , a₀ ] == ⊙[ B , b₀ ]
⊙ua e p = pair= (ua e) (↓-idf-ua-in e p)

{- ⊙→ preserves hlevel -}
⊙→-level : ∀ {i j} {X : Ptd i} {Y : Ptd j} {n : ℕ₋₂}
  → has-level n (fst Y) → has-level n (fst (X ⊙→ Y))
⊙→-level pY = Σ-level (Π-level (λ _ → pY)) (λ _ → =-preserves-level _ pY)

{- function extensionality for pointed functions -}
⊙λ= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : fst (X ⊙→ Y)}
  (p : ∀ x → fst f x == fst g x) (α : snd f == p (snd X) ∙ snd g)
  → f == g
⊙λ= {g = g} p α =
  pair= (λ= p) (↓-app=cst-in (α ∙ ap (λ w → w ∙ snd g) (! (app=-β p _))))

{- Obtaining pointed maps from an pointed equivalence -}
module _ {i j} {X : Ptd i} {Y : Ptd j} (e : fst X ≃ fst Y)
  (p : –> e (snd X) == snd Y) where

  ⊙–> : fst (X ⊙→ Y)
  ⊙–> = (–> e , p)

  ⊙<– : fst (Y ⊙→ X)
  ⊙<– = (<– e , ap (<– e) (! p) ∙ <–-inv-l e (snd X))

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
data D : Set where
  d : D

foo : D
foo = {!!}
-- C-c C-r gives me a weird-looking '0'

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


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

-- Some of the obvious properties of cartesian functors
module Categories.Functor.Cartesian.Properties where

open import Data.Product using (_,_; proj₁; proj₂)
open import Level

open import Categories.Category.Core using (Category)
open import Categories.Category.Cartesian
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Cartesian
open import Categories.Morphism.Reasoning
open import Categories.NaturalTransformation hiding (id)
import Categories.Object.Product as OP

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ : Level

idF-Cartesian : {A : Category o ℓ e} {CA : Cartesian A} → CartesianF CA CA idF
idF-Cartesian {A = A} {CA} = record
  { ε = id
  ; ⊗-homo = ntHelper record
    { η = λ _ → id
    ; commute = λ _ → id-comm-sym A }
  }
  where
  open Category A

∘-Cartesian : {A : Category o ℓ e} {B : Category o′ ℓ′ e′} {C : Category o″ ℓ″ e″}
  {CA : Cartesian A} {CB : Cartesian B} {CC : Cartesian C}
  {F : Functor B C} {G : Functor A B} (CF : CartesianF CB CC F) (CG : CartesianF CA CB G) → CartesianF CA CC (F ∘F G)
∘-Cartesian {B = B} {C} {CA} {CB} {CC} {F} {G} CF CG = record
  { ε = F.₁ CG.ε ∘ CF.ε
  ; ⊗-homo = ntHelper record
    { η = λ X → F.₁ (NTG.η X) ∘ NTF.η (Functor.F₀ (G ⁂ G) X)
    ; commute = λ { {A} {B} f →
      let GGA = F₀ (G ⁂ G) A in
      let GGB = F₀ (G ⁂ G) B in
      let GGf = F₁ (G ⁂ G) f in
      begin
      (F.₁ (NTG.η B) ∘ NTF.η GGB) ∘ F₁ (⊗ CC ∘F ((F ∘F G) ⁂ (F ∘F G))) f  ≈⟨ C.assoc ⟩
      F.₁ (NTG.η B) ∘ NTF.η GGB ∘ F₁ (⊗ CC ∘F ((F ∘F G) ⁂ (F ∘F G))) f    ≈⟨ (refl⟩∘⟨ NTF.commute GGf) ⟩
      F.₁ (NTG.η B) ∘ (F.₁ (F₁ (⊗ CB) GGf) ∘ NTF.η GGA)                   ≈⟨ C.sym-assoc ⟩
      (F.₁ (NTG.η B) ∘ F.₁ (F₁ (⊗ CB) GGf)) ∘ NTF.η GGA                   ≈˘⟨ (F.homomorphism ⟩∘⟨refl) ⟩
      (F.₁ (NTG.η B B.∘ F₁ (⊗ CB) GGf)) ∘ NTF.η GGA                       ≈⟨ (F.F-resp-≈ (NTG.commute f) ⟩∘⟨refl) ⟩
      F.F₁ (F₁ G (F₁ (⊗ CA) f) B.∘ NTG.η A) ∘ NTF.η GGA                   ≈⟨ (F.homomorphism ⟩∘⟨refl) ⟩
      (F₁ ((F ∘F G) ∘F ⊗ CA) f ∘ F.₁ (NTG.η A)) ∘ NTF.η GGA               ≈⟨ C.assoc ⟩
      F₁ ((F ∘F G) ∘F ⊗ CA) f ∘ F.₁ (NTG.η A) ∘ NTF.η GGA ∎}
    }
  }
  where
  module CF = CartesianF CF
  module CG = CartesianF CG
  module NTF = NaturalTransformation CF.⊗-homo
  module NTG = NaturalTransformation CG.⊗-homo
  module F = Functor F
  module B = Category B
  module C = Category C
  open C using (_≈_; _∘_)
  open C.HomReasoning
  open Cartesian CC using (products)
  open Functor
  open OP C using (Product)
  open Product
  open Cartesian using (⊗)


text:
-- Sometimes we can't infer a record type

module InferRecordTypes-2 where

record R : Set₁ where
  field
    x₁ : Set
    x₂ : Set

bad = record { x₃ = Set }

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical-compatible #-}
-- Issue raised by Martin Escardo 2012-12-13
-- on the Agda list "no longer type checks"
module WithoutKDisjointSum where

open import Common.Equality

data ⊥ : Set where

data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

distinct : {A B : Set} (a : A) (b : B) → inl a ≡ inr b → ⊥
distinct a b ()


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

open import PathInduction using (Type; _==_; idp; Square; !; _∙_; Coh; path-induction)

module ExPathInduction {i} where

{-<excoh>-}
coh :  {A : Type i} {a : A} →
       Coh  ({b : A} (p : a == b)
            {d : A} {s : d == b}
            {c : A} {r : b == c}
            {f : A} {u : f == c}
            {e : A} {t : e == c}
            {w : f == e} (ν : Square w idp t u)
            {v : d == e} (α : Square v s t r)
            {vw : d == f} (vw= : vw == v ∙ ! w)
            → Square (p ∙ ! s) p vw (r ∙ ! u))
coh = path-induction
{-</>-}

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text: module exec-tc.empty where


text:
open import Prelude hiding (subst; module Fin)

module Implicits.Substitutions.Lemmas.MetaType where

open import Implicits.Syntax.Type
open import Implicits.Syntax.Term hiding (var)
open import Implicits.Syntax.Context
open import Implicits.WellTyped
open import Implicits.Substitutions

open import Data.Vec hiding ([_])
open import Data.Fin as Fin using ()
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Data.Nat.Properties.Simple
open import Extensions.Substitution
open import Relation.Binary.HeterogeneousEquality as H using ()

private
  module HR = H.≅-Reasoning

module MetaTypeTypeLemmas where
  open MetaTypeTypeSubst hiding (_/✶_)
  open import Implicits.Syntax.MetaType
  open import Data.Star

  private module V = VarLemmas

  module _ {m : ℕ} where

    MT : ℕ → Set
    MT = MetaType m

    open MetaTypeApp hiding (_/_)

    module _ {T₁ T₂} {lift₁ : MetaLift T₁} {lift₂ : MetaLift T₂} where

        open Lifted {m} lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
        open Lifted {m} lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

        /✶-↑✶ : ∀ {n n'} (ρs₁ : Subs (T₁ m) n n') (ρs₂ : Subs (T₂ m) n n') →
                (∀ k x → (simpl (tvar x)) /✶₁ ρs₁ ↑✶₁ k ≡ (simpl (tvar x)) /✶₂ ρs₂ ↑✶₂ k) →
                ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k
        /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
                (a ⇒ b) /✶₁ ρs₁ ↑✶₁ k
            ≡⟨ ⇒-/✶-↑✶ lift₁ k ρs₁ ⟩
                ((a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k))
            ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
                (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k)
            ≡⟨ sym (⇒-/✶-↑✶ lift₂ k ρs₂) ⟩
                (a ⇒ b) /✶₂ ρs₂ ↑✶₂ k ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (∀' t) = begin
                (∀' t) /✶₁ ρs₁ ↑✶₁ k
            ≡⟨ ∀'-/✶-↑✶ lift₁ k ρs₁ ⟩
                ∀' (t /✶₁ ρs₁ ↑✶₁ (suc k))
            ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) t) ⟩
                ∀' (t /✶₂ ρs₂ ↑✶₂ (suc k))
            ≡⟨ sym $ ∀'-/✶-↑✶ lift₂ k ρs₂ ⟩
                (∀' t) /✶₂ ρs₂ ↑✶₂ k ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tvar c)) = hyp k c
        /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (mvar x)) = begin
                (simpl (mvar x)) /✶₁ ρs₁ ↑✶₁ k
            ≡⟨ mvar-/✶-↑✶ lift₁ k ρs₁ ⟩
                (simpl (mvar x))
            ≡⟨ sym $ mvar-/✶-↑✶ lift₂ k ρs₂ ⟩
                (simpl (mvar x)) /✶₂ ρs₂ ↑✶₂ k ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (a →' b)) = begin
                (simpl (a →' b)) /✶₁ ρs₁ ↑✶₁ k
            ≡⟨ →'-/✶-↑✶ lift₁ k ρs₁ ⟩
                simpl ((a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k))
            ≡⟨ cong₂ (λ a b → simpl (a →' b)) (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
                simpl ((a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k))
            ≡⟨ sym (→'-/✶-↑✶ lift₂ k ρs₂) ⟩
                (simpl (a →' b)) /✶₂ ρs₂ ↑✶₂ k ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tc c)) = begin
                (simpl (tc c)) /✶₁ ρs₁ ↑✶₁ k
            ≡⟨ tc-/✶-↑✶ lift₁ k ρs₁ ⟩
                (simpl (tc c))
            ≡⟨ sym $ tc-/✶-↑✶ lift₂ k ρs₂ ⟩
                (simpl (tc c)) /✶₂ ρs₂ ↑✶₂ k ∎

    lemmas₃ : Lemmas₃ (MetaType m)
    lemmas₃ = record
        { lemmas₂ = record
        { lemmas₁ = record
            { lemmas₀ = record
            { simple = simple
            }
            ; weaken-var = λ {_ x} → begin
                (simpl (tvar x)) /Var V.wk      ≡⟨ refl ⟩
                (simpl (tvar (lookup x V.wk)))  ≡⟨ cong (λ x → simpl (tvar x)) (V.lookup-wk x) ⟩
                (simpl (tvar (suc x)))          ∎
            }
        ; application = Subst.application subst
        ; var-/       = refl
        }
        ; /✶-↑✶ = /✶-↑✶
        }

    private module L₃ = Lemmas₃ lemmas₃

    lemmas₅ : Lemmas₅ (MetaType m)
    lemmas₅ = record
        { lemmas₄ = record
        { lemmas₃ = lemmas₃
        ; /-wk    = λ {_ t} → begin
            t / wk       ≡⟨ /✶-↑✶ (ε ▻ wk) (ε ▻ V.wk)
                                (λ k x → begin
                                (simpl (tvar x)) / wk ↑⋆ k
                                  ≡⟨ L₃.var-/-wk-↑⋆ k x ⟩
                                (simpl (tvar (Fin.lift k suc x)))
                                  ≡⟨ cong (λ x → (simpl (tvar x))) (sym (V.var-/-wk-↑⋆ k x)) ⟩
                                (simpl (tvar (lookup x (V._↑⋆_ V.wk k))))
                                  ≡⟨ refl ⟩
                                (simpl (tvar x)) /Var V._↑⋆_ V.wk k        ∎)
                                zero t ⟩
            t /Var V.wk  ≡⟨ refl ⟩
            weaken t     ∎
        }
        }

    open Lemmas₅ lemmas₅ public hiding (lemmas₃)

module MetaTypeMetaLemmas where
  open MetaTypeMetaSubst using (module Lifted; MetaLift)
  open import Implicits.Syntax.MetaType
  open import Data.Star as Star hiding (map)
  open import Data.Star.Properties

  private module V = VarLemmas

  module MetaTypeAppLemmas {T} (l : MetaLift T) where
    open Lifted l

    →'-/✶-↑✶ : ∀ k {ν n n' a b} (ρs : Subs (flip T ν) n n') →
            (simpl (a →' b)) /✶ ρs ↑✶ k ≡ simpl ((a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k))
    →'-/✶-↑✶ k ε        = refl
    →'-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

    ⇒-/✶-↑✶ : ∀ k {ν n n' a b} (ρs : Subs (flip T ν) n n') →
            (a ⇒ b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) ⇒ (b /✶ ρs ↑✶ k)
    ⇒-/✶-↑✶ k ε        = refl
    ⇒-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

    tc-/✶-↑✶ : ∀ k {ν c n n'} (ρs : Subs (flip T ν) n n') →
            (simpl (tc c)) /✶ ρs ↑✶ k ≡ simpl (tc c)
    tc-/✶-↑✶ k ε        = refl
    tc-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tc-/✶-↑✶ k ρs) refl

    tvar-/✶-↑✶ : ∀ k {ν n n' c} (ρs : Subs (flip T ν) n n') →
            (simpl (tvar c)) /✶ ρs ↑✶ k ≡ simpl (tvar c)
    tvar-/✶-↑✶ k ε        = refl
    tvar-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tvar-/✶-↑✶ k ρs) refl

    tpweaken-subs : ∀ {ν n n'} (ρs : Subs (flip T ν) n n') → Subs (flip T (suc ν)) n n'
    tpweaken-subs ρs = Star.map (λ x → x ↑tp) ρs

    comm-↑-↑tp : ∀ {ν n n'} (s : Sub (flip T ν) n n') → (s ↑) ↑tp ≡ (s ↑tp) ↑
    comm-↑-↑tp s = begin
      (s ↑) ↑tp
        ≡⟨ refl ⟩
      map tpweaken (var zero ∷ map weaken s)
        ≡⟨ refl ⟩
      (tpweaken (var zero)) ∷ (map tpweaken (map weaken s))
        ≡⟨ cong₂ (λ x xs → x ∷ xs) (tpweaken-var zero) (sym $ map-∘ tpweaken weaken s) ⟩
      (var zero) ∷ (map (tpweaken ∘ weaken) s)
        ≡⟨ cong (λ u → var zero ∷ u) (sym $ map-cong comm-weaken-tpweaken s) ⟩
      (var zero) ∷ (map (weaken ∘ tpweaken) s)
        ≡⟨ cong (λ u → (var zero) ∷ u) (map-∘ weaken tpweaken s) ⟩
      (s ↑tp) ↑ ∎

    comm-↑⋆-↑tp : ∀ k {ν n n'} (s : Sub (flip T ν) n n') → (s ↑⋆ k) ↑tp ≡ (s ↑tp) ↑⋆ k
    comm-↑⋆-↑tp zero s = refl
    comm-↑⋆-↑tp (suc k) s = begin
      ((s ↑⋆ k) ↑) ↑tp
        ≡⟨ comm-↑-↑tp (s ↑⋆ k) ⟩
      ((s ↑⋆ k) ↑tp) ↑
        ≡⟨ cong _↑ (comm-↑⋆-↑tp k s) ⟩
      (s ↑tp) ↑⋆ (suc k) ∎

    comm-tpweaken-↑✶ : ∀ k {ν n n'} (ρs : Subs (flip T ν) n n') →
                     (tpweaken-subs ρs) ↑✶ k ≡ tpweaken-subs (ρs ↑✶ k)
    comm-tpweaken-↑✶ k ρs = begin
       (tpweaken-subs ρs) ↑✶ k
         ≡⟨ refl ⟩
       Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) (Star.map _↑tp ρs)
         ≡⟨ gmap-∘ (_+_ k) (λ ρ₁ → ρ₁ ↑⋆ k) Prelude.id _↑tp ρs ⟩
       Star.gmap (_+_ k) (λ ρ → (ρ ↑tp) ↑⋆ k) ρs
       ≡⟨ gmap-cong (_+_ k) (λ ρ₁ → _↑tp ρ₁ ↑⋆ k) (λ ρ₁ → _↑tp (ρ₁ ↑⋆ k))
           (λ s → sym $ comm-↑⋆-↑tp k s) ρs ⟩
       Star.gmap (_+_ k) (λ ρ → (ρ ↑⋆ k) ↑tp) ρs
         ≡⟨ sym $ gmap-∘ Prelude.id _↑tp (_+_ k) (λ ρ₁ → ρ₁ ↑⋆ k) ρs ⟩
       Star.map _↑tp (Star.gmap (_+_ k) (λ ρ → ρ ↑⋆ k) ρs)
         ≡⟨ refl ⟩
       tpweaken-subs (ρs ↑✶ k) ∎

    ∀'-/✶-↑✶ : ∀ k {ν n n' a} (ρs : Subs (flip T ν) n n') →
               (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ (tpweaken-subs ρs) ↑✶ k)
    ∀'-/✶-↑✶ k {a = a} ε = refl
    ∀'-/✶-↑✶ k {a = a} (x ◅ ρs) = begin
        (∀' a) /✶ (x  ◅ ρs) ↑✶ k
          ≡⟨ cong (flip _/_ (x ↑⋆ k)) (∀'-/✶-↑✶ k ρs) ⟩
        (∀' (a /✶ (tpweaken-subs ρs) ↑✶ k)) / (x ↑⋆ k)
          ≡⟨ cong (λ u → ∀' (a /✶ u / _↑tp (x ↑⋆ k))) (comm-tpweaken-↑✶ k ρs) ⟩
        ∀' (a /✶ (tpweaken-subs ((x ◅ ρs) ↑✶ k)))
          ≡⟨ sym $ cong (λ u → ∀' (a /✶ u)) (comm-tpweaken-↑✶ k (x ◅ ρs)) ⟩
        ∀' (a /✶ (tpweaken-subs (x ◅ ρs)) ↑✶ k) ∎

    module _ where
      open MetaTypeTypeSubst using () renaming (weaken to mtt-weaken)
      private
        module MTT = MetaTypeTypeSubst

      {-}↑tp-mtt-weaken : ∀ {ν m n} x (s : Sub (flip T ν) m n) →
                                 (mtt-weaken x) / (s ↑tp) ≡ mtt-weaken (x / s)-}
      postulate ↑tp-mtt-weaken : ∀ {ν m n } k x (s : Sub (flip T ν) m n) →
                       (x MTT./Var VarSubst.wk VarSubst.↑⋆ k) /
                         (Prelude.subst (λ ν → Sub (flip T ν) m n) (sym $ +-suc k ν) (s ↑tp⋆ (suc k))) ≡
                       (x / (s ↑tp⋆ k)) MTT./Var VarSubst.wk VarSubst.↑⋆ k
      {-
      ↑tp-mtt-weaken k (a ⇒ b) s = cong₂ _⇒_ (↑tp-mtt-weaken k a s) (↑tp-mtt-weaken k b s)
      ↑tp-mtt-weaken {ν} {m} {n} k (∀' x) s = begin
        (∀' (x MTT./Var VarSubst.wk VarSubst.↑⋆ (suc k))) /
          (Prelude.subst (λ ν → Sub (flip T ν) m n) (sym $ +-suc k ν) (s ↑tp⋆ (suc k)))
          ≡⟨ refl ⟩
        ∀' ((x MTT./Var VarSubst.wk VarSubst.↑⋆ (suc k)) /
          (Prelude.subst (λ ν → Sub (flip T ν) m n) (cong suc (sym $ +-suc k ν)) (s ↑tp⋆ (suc (suc k)))))
          ≡⟨ cong ∀' (↑tp-mtt-weaken (suc k) {!!} {!!}) ⟩
        (∀' ((x / (s ↑tp⋆ (suc k))) MTT./Var VarSubst.wk VarSubst.↑⋆ (suc k)))
          ≡⟨ refl ⟩
        (∀' (x / (s ↑tp⋆ (suc k)))) MTT./Var VarSubst.wk VarSubst.↑⋆ k
          ≡⟨ refl ⟩
        (∀' x / s ↑tp⋆ k) MTT./Var VarSubst.wk VarSubst.↑⋆ k ∎

      ↑tp-mtt-weaken k (simpl (tvar x)) s = refl
      ↑tp-mtt-weaken k (simpl (mvar x)) s = {!!}
      ↑tp-mtt-weaken k (simpl (a →' b)) s = cong₂ (λ u v → simpl (u →' v)) (↑tp-mtt-weaken k a s)
                                            (↑tp-mtt-weaken k b s)
      ↑tp-mtt-weaken k (simpl (tc x)) s = refl
      -}

      tpweaken-subs-var : ∀ {ν n n'} x (ρs : Subs (flip T ν) n n') →
                          (simpl (mvar x)) /✶ (tpweaken-subs ρs)
                            ≡ mtt-weaken ((simpl (mvar x)) /✶ ρs)
      tpweaken-subs-var x ε = refl
      tpweaken-subs-var x (s ◅ ρs) = begin
        (simpl (mvar x)) /✶ (Star.map _↑tp (s ◅ ρs))
          ≡⟨ refl ⟩
        (simpl (mvar x)) /✶ (tpweaken-subs ρs) / (s ↑tp)
          ≡⟨ cong (flip _/_ (_↑tp s)) (tpweaken-subs-var x ρs) ⟩
        (mtt-weaken ((simpl (mvar x)) /✶ ρs)) / (s ↑tp)
          ≡⟨ ↑tp-mtt-weaken zero (simpl (mvar x) /✶ ρs) s ⟩
        mtt-weaken ((simpl (mvar x)) /✶ (s ◅ ρs)) ∎

  module _ {T₁ T₂} {lift₁ : MetaLift T₁} {lift₂ : MetaLift T₂} where
    open MetaTypeTypeSubst using () renaming (weaken to mtt-weaken)

    open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_; _↑tp to _↑tp₁)
    open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_; _↑tp to _↑tp₂)

    open MetaTypeAppLemmas

    weaken-hyp : ∀ {ν n n'} (ρs₁ : Subs (flip T₁ ν) n n') (ρs₂ : Subs (flip T₂ ν) n n') →
                        (∀ k x → (simpl (mvar x)) /✶₁ ρs₁ ↑✶₁ k ≡ (simpl (mvar x)) /✶₂ ρs₂ ↑✶₂ k) →
                        (∀ k x → (simpl (mvar x)) /✶₁ (tpweaken-subs lift₁ ρs₁) ↑✶₁ k ≡ (simpl (mvar x)) /✶₂ (tpweaken-subs lift₂ ρs₂) ↑✶₂ k)
    weaken-hyp ρs₁ ρs₂ hyp k x = begin
      simpl (mvar x) /✶₁ (tpweaken-subs lift₁ ρs₁) ↑✶₁ k
        ≡⟨ cong (λ u → simpl (mvar x) /✶₁ u) (comm-tpweaken-↑✶ lift₁ k ρs₁) ⟩
      simpl (mvar x) /✶₁ tpweaken-subs lift₁ (ρs₁ ↑✶₁ k)
        ≡⟨ tpweaken-subs-var lift₁ x (ρs₁ ↑✶₁ k) ⟩
      mtt-weaken (simpl (mvar x) /✶₁ (ρs₁ ↑✶₁ k))
        ≡⟨ cong mtt-weaken (hyp k x) ⟩
      mtt-weaken (simpl (mvar x) /✶₂ (ρs₂ ↑✶₂ k))
        ≡⟨ sym $ tpweaken-subs-var lift₂ x (ρs₂ ↑✶₂ k) ⟩
      simpl (mvar x) /✶₂ tpweaken-subs lift₂ (ρs₂ ↑✶₂ k)
        ≡⟨ cong (λ u → simpl (mvar x) /✶₂ u) (sym $ comm-tpweaken-↑✶ lift₂ k ρs₂) ⟩
      simpl (mvar x) /✶₂ (tpweaken-subs lift₂ ρs₂) ↑✶₂ k ∎

    /✶-↑✶ : ∀ {ν n n'} (ρs₁ : Subs (flip T₁ ν) n n') (ρs₂ : Subs (flip T₂ ν) n n') →
            (∀ k x → (simpl (mvar x)) /✶₁ ρs₁ ↑✶₁ k ≡ (simpl (mvar x)) /✶₂ ρs₂ ↑✶₂ k) →
            ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k
    /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
            (a ⇒ b) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ ⇒-/✶-↑✶ lift₁ k ρs₁ ⟩
            ((a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k))
        ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
            (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k)
        ≡⟨ sym (⇒-/✶-↑✶ lift₂ k ρs₂) ⟩
            (a ⇒ b) /✶₂ ρs₂ ↑✶₂ k ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (∀' t) = begin
            (∀' t) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ ∀'-/✶-↑✶ lift₁ k ρs₁ ⟩
            (∀' (t /✶₁ (tpweaken-subs lift₁ ρs₁) ↑✶₁ k))
        ≡⟨ cong ∀' (/✶-↑✶ (tpweaken-subs lift₁ ρs₁) (tpweaken-subs lift₂ ρs₂) (weaken-hyp ρs₁ ρs₂ hyp) k t ) ⟩
            (∀' (t /✶₂ (tpweaken-subs lift₂ ρs₂) ↑✶₂ k))
        ≡⟨ sym $ ∀'-/✶-↑✶ lift₂ k ρs₂ ⟩
            (∀' t) /✶₂ ρs₂ ↑✶₂ k ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (mvar c)) = hyp k c
    /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tvar x)) = begin
            (simpl (tvar x)) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ tvar-/✶-↑✶ lift₁ k ρs₁ ⟩
            (simpl (tvar x))
        ≡⟨ sym $ tvar-/✶-↑✶ lift₂ k ρs₂ ⟩
            (simpl (tvar x)) /✶₂ ρs₂ ↑✶₂ k ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (a →' b)) = begin
            (simpl (a →' b)) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ →'-/✶-↑✶ lift₁ k ρs₁ ⟩
            simpl ((a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k))
        ≡⟨ cong₂ (λ a b → simpl (a →' b)) (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
            simpl ((a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k))
        ≡⟨ sym (→'-/✶-↑✶ lift₂ k ρs₂) ⟩
            (simpl (a →' b)) /✶₂ ρs₂ ↑✶₂ k ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (simpl (tc c)) = begin
            (simpl (tc c)) /✶₁ ρs₁ ↑✶₁ k
        ≡⟨ tc-/✶-↑✶ lift₁ k ρs₁ ⟩
            (simpl (tc c))
        ≡⟨ sym $ tc-/✶-↑✶ lift₂ k ρs₂ ⟩
            (simpl (tc c)) /✶₂ ρs₂ ↑✶₂ k ∎

  module _ {ν : ℕ} where
    open MetaTypeMetaSubst

    MT : ℕ → Set
    MT = flip MetaType ν

    lemmas₃ : Lemmas₃ (flip MetaType ν)
    lemmas₃ = record
        { lemmas₂ = record
        { lemmas₁ = record
            { lemmas₀ = record
            { simple = simple
            }
            ; weaken-var = λ {_ x} → begin
                (simpl (mvar x)) /Var V.wk      ≡⟨ refl ⟩
                (simpl (mvar (lookup x V.wk)))  ≡⟨ cong (λ x → simpl (mvar x)) (V.lookup-wk x) ⟩
                (simpl (mvar (suc x)))          ∎
            }
        ; application = Subst.application subst
        ; var-/       = refl
        }
        ; /✶-↑✶ = /✶-↑✶
        }

    private module L₃ = Lemmas₃ lemmas₃

    lemmas₅ : Lemmas₅ (flip MetaType ν)
    lemmas₅ = record
        { lemmas₄ = record
        { lemmas₃ = lemmas₃
        ; /-wk    = λ {_ t} → begin
            t / wk       ≡⟨ /✶-↑✶ (ε ▻ wk) (ε ▻ V.wk)
                                (λ k x → begin
                                (simpl (mvar x)) / wk ↑⋆ k
                                  ≡⟨ L₃.var-/-wk-↑⋆ k x ⟩
                                (simpl (mvar (Fin.lift k suc x)))
                                  ≡⟨ cong (λ x → (simpl (mvar x))) (sym (V.var-/-wk-↑⋆ k x)) ⟩
                                (simpl (mvar (lookup x (V._↑⋆_ V.wk k))))
                                  ≡⟨ refl ⟩
                                (simpl (mvar x)) /Var V._↑⋆_ V.wk k        ∎)
                                zero t ⟩
            t /Var V.wk  ≡⟨ refl ⟩
            weaken t     ∎
        }
        }

    open Lemmas₅ lemmas₅ public hiding (lemmas₃)

  open MetaTypeMetaSubst using (open-meta-k; open-meta; _↑⋆tp_; _↑tp; _◁m; _◁m₁)

  us↑-⊙-sub-u≡u∷us : ∀ {ν m} (u : MetaType zero ν) (us : Sub (flip MetaType ν) m zero) →
                     us ↑ ⊙ sub u ≡ u ∷ us
  us↑-⊙-sub-u≡u∷us {ν} {m} u us = cong (λ v → u ∷ v) map-weaken-⊙-sub

  open-mvar : ∀ {ν m} (x : Fin m) → open-meta {ν = ν} (simpl (mvar x)) ≡ simpl (mvar (suc x))
  open-mvar x = weaken-var

  open-tvar-suc : ∀ {ν m} (x : Fin m) → open-meta {ν} (simpl (tvar (suc x))) ≡ simpl (tvar x)
  open-tvar-suc x = MetaTypeTypeLemmas.suc-/-sub {t = (simpl (tvar x))}

  open import Implicits.Substitutions.Type as TS using ()
  open import Implicits.Substitutions.Lemmas.Type as TSLemmas using ()

  private
    module MTT = MetaTypeTypeSubst


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Setoids.Setoids
open import Setoids.Functions.Definition
open import Sets.EquivalenceRelations

module Setoids.Functions.Extension where

ExtensionallyEqual : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {f g : A → B} (fWd : WellDefined S T f) (gWd : WellDefined S T g) → Set (a ⊔ d)
ExtensionallyEqual {A = A} {T = T} {f = f} {g = g} fWD gWD = (∀ {x : A} → Setoid._∼_ T (f x) (g x))

extensionallyEqualReflexive : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) (fWD1 fWD2 : WellDefined S T f) → ExtensionallyEqual {S = S} {T} fWD1 fWD2
extensionallyEqualReflexive S T f fWD1 _ = Equivalence.reflexive (Setoid.eq T)

extensionallyEqualSymmetric : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f g : A → B) (fWD : WellDefined S T f) (gWD : WellDefined S T g) → ExtensionallyEqual {S = S} {T = T} fWD gWD → ExtensionallyEqual {S = S} {T} gWD fWD
extensionallyEqualSymmetric S T f g fWD gWD pr = Equivalence.symmetric (Setoid.eq T) pr

extensionallyEqualTransitive : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f g h : A → B) (fWD : WellDefined S T f) (gWD : WellDefined S T g) (hWD : WellDefined S T h) → ExtensionallyEqual {S = S} {T} fWD gWD → ExtensionallyEqual {S = S} {T} gWD hWD → ExtensionallyEqual {S = S} {T} fWD hWD
extensionallyEqualTransitive S T f g h fWD gWD hWD pr1 pr2 = Equivalence.transitive (Setoid.eq T) pr1 pr2


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

open import Level using (Level)
open import Data.Nat using (ℕ) renaming (_+_ to _+ᴺ_)

open import Data.Vec using (Vec; _++_; take; drop; replicate; map; foldr)
open import Data.Vec.Properties

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Function using (id)

open import FLA.Algebra.Structures
open import FLA.Algebra.Properties.Field
open import FLA.Algebra.LinearMap
open import FLA.Algebra.LinearAlgebra
open import FLA.Algebra.LinearAlgebra.Properties
open import FLA.Data.Vec.Properties

module FLA.Algebra.LinearAlgebra.Matrix where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ

-------------------------------------------------------------------------------
--                          M constructor and values                         --
-------------------------------------------------------------------------------

data Mat_×_ {A : Set ℓ} ⦃ F : Field A ⦄ (m n : ℕ) : Set ℓ where
  ⟦_,_,_⟧ : (M : n ⊸ m )
          → (Mᵀ : m ⊸ n )
          → (p : (x : Vec A m) → (y : Vec A n)
               → ⟨ x , M ·ˡᵐ y ⟩ ≡ ⟨ y , Mᵀ ·ˡᵐ x ⟩ )
          → Mat m × n

module _ ⦃ F : Field A ⦄ where

  _ᵀ : Mat m × n → Mat n × m
  ⟦ f , a , p ⟧ ᵀ = ⟦ a , f , (λ x y → sym (p y x)) ⟧

  _·ᴹₗ_ : Mat m × n → Vec A n → Vec A m
  ⟦ f , _ , _ ⟧ ·ᴹₗ x = f ·ˡᵐ x

  _·ᴹᵣ_ : Vec A m → Mat m × n → Vec A n
  x ·ᴹᵣ ⟦ _ , a , _ ⟧ = a ·ˡᵐ x

  infixr 20 _·ᴹᵣ_
  infixr 21 _·ᴹₗ_
  infixl 25 _ᵀ

module _ ⦃ F : Field A ⦄ where
  open Field F
  open _⊸_

  _+ᴹ_ : Mat m × n → Mat m × n → Mat m × n
  ⟦ M₁ , M₁ᵀ , p₁ ⟧ +ᴹ ⟦ M₂ , M₂ᵀ , p₂ ⟧ =
    ⟦ M₁ +ˡᵐ M₂
    , M₁ᵀ +ˡᵐ M₂ᵀ
    , ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ p₁ p₂
    ⟧
    where
      ⟨⟩-proof : (M₁ M₂ : n ⊸ m) (M₁ᵀ M₂ᵀ : m ⊸ n)
               → (M₁-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₁ ·ˡᵐ y ⟩ ≡ ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ )
               → (M₂-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₂ ·ˡᵐ y ⟩ ≡ ⟨ y , M₂ᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A m) (y : Vec A n)
               → ⟨ x , (M₁ +ˡᵐ M₂) ·ˡᵐ y ⟩ ≡ ⟨ y , (M₁ᵀ +ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ M₁-proof M₂-proof x y =
        begin
            ⟨ x , (M₁ +ˡᵐ M₂) ·ˡᵐ y ⟩
          ≡⟨⟩
            ⟨ x , M₁ ·ˡᵐ y +ⱽ M₂ ·ˡᵐ y ⟩
          ≡⟨ ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ x (M₁ ·ˡᵐ y) (M₂ ·ˡᵐ y) ⟩
            ⟨ x , M₁ ·ˡᵐ y ⟩ + ⟨ x , M₂ ·ˡᵐ y ⟩
          ≡⟨ cong₂ _+_ (M₁-proof x y) (M₂-proof x y) ⟩
            ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + ⟨ y , M₂ᵀ ·ˡᵐ x ⟩
          ≡⟨ sym (⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ y (M₁ᵀ ·ˡᵐ x) (M₂ᵀ ·ˡᵐ x)) ⟩
            ⟨ y , (M₁ᵀ +ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
        ∎

  _-ᴹ_ : Mat m × n → Mat m × n → Mat m × n
  ⟦ M₁ , M₁ᵀ , p₁ ⟧ -ᴹ ⟦ M₂ , M₂ᵀ , p₂ ⟧ =
    ⟦ M₁ -ˡᵐ M₂
    , M₁ᵀ -ˡᵐ M₂ᵀ
    , ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ p₁ p₂
    ⟧
    where
      ⟨⟩-proof : (M₁ M₂ : n ⊸ m) (M₁ᵀ M₂ᵀ : m ⊸ n)
               → (M₁-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₁ ·ˡᵐ y ⟩ ≡ ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ )
               → (M₂-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₂ ·ˡᵐ y ⟩ ≡ ⟨ y , M₂ᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A m) (y : Vec A n)
               → ⟨ x , (M₁ -ˡᵐ M₂) ·ˡᵐ y ⟩ ≡ ⟨ y , (M₁ᵀ -ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ M₁-proof M₂-proof x y = begin
          ⟨ x , (M₁ -ˡᵐ M₂) ·ˡᵐ y ⟩
        ≡⟨⟩
          ⟨ x , M₁ ·ˡᵐ y -ⱽ M₂ ·ˡᵐ y ⟩
        ≡⟨ cong (λ a → ⟨ x , M₁ ·ˡᵐ y +ⱽ a ⟩) (-ⱽ≡-1ᶠ∘ⱽ (M₂ ·ˡᵐ y)) ⟩
          ⟨ x , M₁ ·ˡᵐ y +ⱽ (- 1ᶠ) ∘ⱽ M₂ ·ˡᵐ y ⟩
        ≡⟨ ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ x (M₁ ·ˡᵐ y) ((- 1ᶠ) ∘ⱽ M₂ ·ˡᵐ y) ⟩
          ⟨ x , M₁ ·ˡᵐ y ⟩ + ⟨ x , (- 1ᶠ) ∘ⱽ M₂ ·ˡᵐ y ⟩
        ≡⟨ cong (λ a → ⟨ x , M₁ ·ˡᵐ y ⟩ + ⟨ x , a ⟩ )
                (sym (f[c*v]≡c*f[v] M₂ (- 1ᶠ) y)) ⟩
          ⟨ x , M₁ ·ˡᵐ y ⟩ + ⟨ x , (M₂ ·ˡᵐ ((- 1ᶠ) ∘ⱽ y)) ⟩
        ≡⟨ cong₂ _+_ (M₁-proof x y) (M₂-proof x ((- 1ᶠ) ∘ⱽ y)) ⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + ⟨ (- 1ᶠ) ∘ⱽ y , M₂ᵀ ·ˡᵐ x ⟩
        ≡⟨⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + sum ( ((- 1ᶠ) ∘ⱽ y) *ⱽ M₂ᵀ ·ˡᵐ x )
        ≡⟨ cong (λ a → ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + sum a)
                (sym (∘ⱽ*ⱽ-assoc (- 1ᶠ) y (M₂ᵀ ·ˡᵐ x))) ⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + sum ((- 1ᶠ) ∘ⱽ (y *ⱽ M₂ᵀ ·ˡᵐ x))
        ≡⟨ cong (λ a → ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + sum a)
                (sym (*ⱽ∘ⱽ≡∘ⱽ*ⱽ (- 1ᶠ) y (M₂ᵀ ·ˡᵐ x))) ⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + sum (y *ⱽ ((- 1ᶠ) ∘ⱽ M₂ᵀ ·ˡᵐ x))
        ≡⟨⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ + ⟨ y , (- 1ᶠ) ∘ⱽ M₂ᵀ ·ˡᵐ x ⟩
        ≡˘⟨ ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ y (M₁ᵀ ·ˡᵐ x) ((- 1ᶠ) ∘ⱽ M₂ᵀ ·ˡᵐ x) ⟩
          ⟨ y , M₁ᵀ ·ˡᵐ x +ⱽ (- 1ᶠ) ∘ⱽ M₂ᵀ ·ˡᵐ x ⟩
        ≡˘⟨ cong (λ a → ⟨ y , M₁ᵀ ·ˡᵐ x +ⱽ a ⟩) (-ⱽ≡-1ᶠ∘ⱽ (M₂ᵀ ·ˡᵐ x)) ⟩
          ⟨ y , (M₁ᵀ -ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
        ∎

  _*ᴹ_ : Mat m × n → Mat n × p → Mat m × p
  ⟦ M₁ , M₁ᵀ , p₁ ⟧ *ᴹ ⟦ M₂ , M₂ᵀ , p₂ ⟧ =
    ⟦ M₁ *ˡᵐ M₂
    , M₂ᵀ *ˡᵐ M₁ᵀ
    , ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ p₁ p₂
    ⟧
    where
      ⟨⟩-proof : (M₁ : n ⊸ m) (M₂ : p ⊸ n) (M₁ᵀ : m ⊸ n) (M₂ᵀ : n ⊸ p)
               → (M₁-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₁ ·ˡᵐ y ⟩ ≡ ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ )
               → (M₂-⟨⟩-proof : (x : Vec A n) (y : Vec A p)
                               → ⟨ x , M₂ ·ˡᵐ y ⟩ ≡ ⟨ y , M₂ᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A m) (y : Vec A p)
               → ⟨ x , (M₁ *ˡᵐ M₂) ·ˡᵐ y ⟩ ≡ ⟨ y , (M₂ᵀ *ˡᵐ M₁ᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ M₁-proof M₂-proof x y =
        begin
          ⟨ x , (M₁ *ˡᵐ M₂) ·ˡᵐ y ⟩   ≡⟨⟩
          ⟨ x , M₁ ·ˡᵐ M₂ ·ˡᵐ y ⟩     ≡⟨ M₁-proof x (M₂ ·ˡᵐ y) ⟩
          ⟨ M₂ ·ˡᵐ y , M₁ᵀ ·ˡᵐ x ⟩    ≡⟨ ⟨⟩-comm (M₂ ·ˡᵐ y) (M₁ᵀ ·ˡᵐ x) ⟩
          ⟨ M₁ᵀ ·ˡᵐ x , M₂ ·ˡᵐ y ⟩    ≡⟨ M₂-proof (M₁ᵀ ·ˡᵐ x) y ⟩
          ⟨ y , (M₂ᵀ *ˡᵐ M₁ᵀ) ·ˡᵐ x ⟩ ∎

  _|ᴹ_ : Mat m × n → Mat m × p → Mat m × (n +ᴺ p)
  ⟦ M₁ , M₁ᵀ , p₁ ⟧ |ᴹ ⟦ M₂ , M₂ᵀ , p₂ ⟧ =
    ⟦ M₁ |ˡᵐ M₂
    , M₁ᵀ —ˡᵐ M₂ᵀ
    , ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ p₁ p₂
    ⟧
    where
      ⟨⟩-proof : {m n p : ℕ}
               → (M₁ : n ⊸ m) (M₂ : p ⊸ m) (M₁ᵀ : m ⊸ n) (M₂ᵀ : m ⊸ p)
               → (M₁-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₁ ·ˡᵐ y ⟩ ≡ ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ )
               → (M₂-⟨⟩-proof : (x : Vec A m) (y : Vec A p)
                               → ⟨ x , M₂ ·ˡᵐ y ⟩ ≡ ⟨ y , M₂ᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A m) (y : Vec A (n +ᴺ p)) →
                      ⟨ x , (M₁ |ˡᵐ M₂) ·ˡᵐ y ⟩ ≡ ⟨ y , (M₁ᵀ —ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof {m} {n} {p} M₁ M₂ M₁ᵀ M₂ᵀ M₁-proof M₂-proof x y =
        begin
            ⟨ x , (M₁ |ˡᵐ M₂) ·ˡᵐ y ⟩
          ≡⟨⟩
            ⟨ x , M₁ ·ˡᵐ take n y +ⱽ M₂ ·ˡᵐ drop n y ⟩
          ≡⟨ ⟨x,y+z⟩≡⟨x,y⟩+⟨x,z⟩ x (M₁ ·ˡᵐ take n y) (M₂ ·ˡᵐ drop n y) ⟩
            ⟨ x , M₁ ·ˡᵐ take n y ⟩ + ⟨ x ,  M₂ ·ˡᵐ drop n y ⟩
          ≡⟨ cong₂ _+_ (M₁-proof x (take n y)) (M₂-proof x (drop n y)) ⟩
            ⟨ take n y , M₁ᵀ ·ˡᵐ x ⟩ + ⟨ drop n y ,  M₂ᵀ ·ˡᵐ x ⟩
          ≡⟨ ⟨a,b⟩+⟨c,d⟩≡⟨a++c,b++d⟩ (take n y) (M₁ᵀ ·ˡᵐ x)
                                     (drop n y) (M₂ᵀ ·ˡᵐ x) ⟩
            ⟨ take n y ++ drop n y , M₁ᵀ ·ˡᵐ x ++ M₂ᵀ ·ˡᵐ x ⟩
          ≡⟨ cong (λ a → ⟨ a , M₁ᵀ ·ˡᵐ x ++ M₂ᵀ ·ˡᵐ x ⟩) (take-drop-id n y) ⟩
            ⟨ y , M₁ᵀ ·ˡᵐ x ++ M₂ᵀ ·ˡᵐ x ⟩
          ≡⟨⟩
            ⟨ y , (M₁ᵀ —ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
        ∎

  _—ᴹ_ : Mat m × p → Mat n × p → Mat (m +ᴺ n) × p
  M —ᴹ N = (M ᵀ |ᴹ N ᵀ) ᵀ

  -- Block diagonal matrix
  _/ᴹ_ : Mat m × n → Mat p × q → Mat (m +ᴺ p) × (n +ᴺ q)
  ⟦ M₁ , M₁ᵀ , p₁ ⟧ /ᴹ ⟦ M₂ , M₂ᵀ , p₂ ⟧ =
    ⟦ M₁ /ˡᵐ M₂
    , M₁ᵀ /ˡᵐ M₂ᵀ
    , ⟨⟩-proof M₁ M₂ M₁ᵀ M₂ᵀ p₁ p₂
    ⟧
    where
      ⟨⟩-proof : {m n p q : ℕ}
               → (M₁ : n ⊸ m) (M₂ : q ⊸ p) (M₁ᵀ : m ⊸ n) (M₂ᵀ : p ⊸ q)
               → (M₁-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M₁ ·ˡᵐ y ⟩ ≡ ⟨ y , M₁ᵀ ·ˡᵐ x ⟩ )
               → (M₂-⟨⟩-proof : (x : Vec A p) (y : Vec A q)
                               → ⟨ x , M₂ ·ˡᵐ y ⟩ ≡ ⟨ y , M₂ᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A (m +ᴺ p)) (y : Vec A (n +ᴺ q)) →
                        ⟨ x , (M₁ /ˡᵐ M₂) ·ˡᵐ y ⟩ ≡ ⟨ y , (M₁ᵀ /ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof {m} {n} {p} M₁ M₂ M₁ᵀ M₂ᵀ M₁-proof M₂-proof x y =
        begin
            ⟨ x , (M₁ /ˡᵐ M₂) ·ˡᵐ y ⟩
          ≡⟨⟩
            ⟨ x , M₁ ·ˡᵐ take n y ++ M₂ ·ˡᵐ drop n y ⟩
          ≡⟨ cong (λ x → ⟨ x , M₁ ·ˡᵐ take n y ++ M₂ ·ˡᵐ drop n y ⟩)
                  (sym (take-drop-id m x)) ⟩
            ⟨ take m x ++ drop m x , M₁ ·ˡᵐ (take n y) ++ M₂ ·ˡᵐ drop n y ⟩
          ≡⟨ ⟨a++b,c++d⟩≡⟨a,c⟩+⟨b,d⟩ (take m x) (drop m x)
                                     (M₁ ·ˡᵐ (take n y)) (M₂ ·ˡᵐ drop n y) ⟩
            ⟨ take m x , M₁ ·ˡᵐ (take n y) ⟩ + ⟨ drop m x , M₂ ·ˡᵐ drop n y ⟩
          ≡⟨ cong₂ _+_ (M₁-proof (take m x) (take n y))
                       (M₂-proof (drop m x) (drop n y)) ⟩
            ⟨ take n y , M₁ᵀ ·ˡᵐ take m x  ⟩ + ⟨ drop n y , M₂ᵀ ·ˡᵐ  drop m x ⟩
          ≡⟨ ⟨a,b⟩+⟨c,d⟩≡⟨a++c,b++d⟩ (take n y) (M₁ᵀ ·ˡᵐ take m x)
                                     (drop n y) (M₂ᵀ ·ˡᵐ  drop m x) ⟩
            ⟨ take n y ++ drop n y , M₁ᵀ ·ˡᵐ take m x ++ M₂ᵀ ·ˡᵐ  drop m x ⟩
          ≡⟨ cong (λ y → ⟨ y , M₁ᵀ ·ˡᵐ take m x ++ M₂ᵀ ·ˡᵐ  drop m x ⟩)
                  (take-drop-id n y) ⟩
            ⟨ y , M₁ᵀ ·ˡᵐ (take m x) ++ M₂ᵀ ·ˡᵐ (drop m x) ⟩
          ≡⟨⟩
            ⟨ y , (M₁ᵀ /ˡᵐ M₂ᵀ) ·ˡᵐ x ⟩
        ∎

  -- Multiply by a constant
  _∘ᴹ_ : A → Mat m × n → Mat m × n
  c ∘ᴹ ⟦ M , Mᵀ , p ⟧ = ⟦ c ∘ˡᵐ M , c ∘ˡᵐ Mᵀ , ⟨⟩-proof M Mᵀ c p ⟧
    where
      ⟨⟩-proof : {m n : ℕ} (M : n ⊸ m) (Mᵀ : m ⊸ n) (c : A)
               → (M-⟨⟩-proof : (x : Vec A m) (y : Vec A n)
                               → ⟨ x , M ·ˡᵐ y ⟩ ≡ ⟨ y , Mᵀ ·ˡᵐ x ⟩ )
               → (x : Vec A m) (y : Vec A n)
               → ⟨ x , (c ∘ˡᵐ M) ·ˡᵐ y ⟩ ≡ ⟨ y , (c ∘ˡᵐ Mᵀ) ·ˡᵐ x ⟩
      ⟨⟩-proof {m} {n} M Mᵀ c M-⟨⟩-proof x y =
        begin
            ⟨ x , (c ∘ˡᵐ M) ·ˡᵐ y ⟩
          ≡⟨⟩
            ⟨ x , c ∘ⱽ (M ·ˡᵐ y) ⟩
          ≡⟨ cong (λ z → ⟨ x , z ⟩) (sym (f[c*v]≡c*f[v] M c y)) ⟩
            ⟨ x , M ·ˡᵐ (c ∘ⱽ y) ⟩
          ≡⟨ M-⟨⟩-proof x ((c ∘ⱽ y)) ⟩
            ⟨ c ∘ⱽ y , Mᵀ ·ˡᵐ x ⟩
          ≡⟨ ⟨⟩-comm (c ∘ⱽ y) (Mᵀ ·ˡᵐ x) ⟩
            ⟨ Mᵀ ·ˡᵐ x , c ∘ⱽ y ⟩
          ≡⟨ cong sum (trans (*ⱽ∘ⱽ≡∘ⱽ*ⱽ c (Mᵀ ·ˡᵐ x) y)
                             (∘ⱽ*ⱽ-assoc c (Mᵀ ·ˡᵐ x) y)) ⟩
            ⟨ (c ∘ˡᵐ Mᵀ) ·ˡᵐ x , y ⟩
          ≡⟨ ⟨⟩-comm ((c ∘ˡᵐ Mᵀ) ·ˡᵐ x) y ⟩
            ⟨ y , (c ∘ˡᵐ Mᵀ) ·ˡᵐ x ⟩
        ∎

  infixl 2 _—ᴹ_
  infixl 3 _|ᴹ_
  infixl 4 _/ᴹ_
  infixl 6 _+ᴹ_
  infixl 6 _-ᴹ_
  infixl 7 _*ᴹ_
  infixl 10 _∘ᴹ_

-- Matrix Free Operators ------------------------------------------------------

module _ ⦃ F : Field A ⦄ where
  open Field F

  I : Mat n × n
  I = ⟦ idₗₘ , idₗₘ , id-transpose  ⟧
    where
      id-transpose : (x y : Vec A n)
                   → ⟨ x , id y ⟩ ≡ ⟨ y , id x ⟩
      id-transpose x y rewrite
          zipWith-comm (*-comm) x y
        = refl

  diag : Vec A n → Mat n × n
  diag d = ⟦ diagₗₘ d , diagₗₘ d , diag-transpose d ⟧
    where
      diag-transpose : (d : Vec A n) → (x y : Vec A n)
                     → ⟨ x , diagₗₘ d ·ˡᵐ y ⟩ ≡ ⟨ y , diagₗₘ d ·ˡᵐ x ⟩
      diag-transpose d x y =
        begin
          ⟨ x , diagₗₘ d ·ˡᵐ y ⟩ ≡⟨⟩
          sum (x *ⱽ (d *ⱽ y))    ≡⟨ cong (sum) (*ⱽ-comm x (d *ⱽ y)) ⟩
          sum ((d *ⱽ y) *ⱽ x)    ≡⟨ cong (λ dy → sum (dy *ⱽ x)) (*ⱽ-comm d y) ⟩
          sum ((y *ⱽ d) *ⱽ x)    ≡⟨ cong sum (*ⱽ-assoc y d x) ⟩
          sum (y *ⱽ (d *ⱽ x))    ≡⟨⟩
          ⟨ y , diagₗₘ d ·ˡᵐ x ⟩ ∎

  1ᴹ : Mat m × n
  1ᴹ = ⟦ 1ₗₘ , 1ₗₘ , 1ₗₘ-transpose  ⟧
    where
      zip-rep = zipWith-replicate₂

      1ₗₘ-transpose : (x : Vec A m) (y : Vec A n)
                    → ⟨ x , 1ₗₘ ·ˡᵐ y ⟩ ≡ ⟨ y , 1ₗₘ ·ˡᵐ x ⟩
      1ₗₘ-transpose x y = begin
          ⟨ x , 1ₗₘ ·ˡᵐ y ⟩            ≡⟨⟩
          sum (x *ⱽ replicate (sum y)) ≡⟨ cong sum (zip-rep _*_ x (sum y)) ⟩
          sum (map (_* sum y) x)       ≡⟨ cong sum (map-*c-≡c∘ⱽ (sum y) x) ⟩
          sum (sum y ∘ⱽ x)             ≡⟨ sum[c∘ⱽv]≡c*sum[v] (sum y) x ⟩
          sum y * sum x                ≡⟨ *-comm (sum y) (sum x) ⟩
          sum x * sum y                ≡˘⟨ sum[c∘ⱽv]≡c*sum[v] (sum x) y ⟩
          sum (sum x ∘ⱽ y)             ≡˘⟨ cong sum (map-*c-≡c∘ⱽ (sum x) y) ⟩
          sum (map (_* sum x) y)       ≡˘⟨ cong sum (zip-rep _*_ y (sum x)) ⟩
          sum (y *ⱽ replicate (sum x)) ≡⟨⟩
          ⟨ y , 1ₗₘ ·ˡᵐ x ⟩            ∎

  0ᴹ : Mat m × n
  0ᴹ = ⟦ 0ₗₘ , 0ₗₘ , 0ₗₘ-transpose ⟧
    where
      0ₗₘ-transpose : (x : Vec A m) (y : Vec A n)
                    → ⟨ x , 0ₗₘ ·ˡᵐ y ⟩ ≡ ⟨ y , 0ₗₘ ·ˡᵐ x ⟩
      0ₗₘ-transpose {m = m} {n = n} x y = begin
        ⟨ x , 0ₗₘ ·ˡᵐ y ⟩               ≡⟨⟩
        sum (x *ⱽ replicate 0ᶠ)         ≡⟨ cong sum (v*ⱽ0ᶠⱽ≡0ᶠⱽ x) ⟩
        sum (replicate {n = m} 0ᶠ)      ≡⟨ sum[0ᶠⱽ]≡0ᶠ {n = m} ⟩
        0ᶠ                              ≡˘⟨ sum[0ᶠⱽ]≡0ᶠ {n = n} ⟩
        sum (replicate {n = n} 0ᶠ)      ≡˘⟨ cong sum (v*ⱽ0ᶠⱽ≡0ᶠⱽ y) ⟩
        sum (y *ⱽ replicate {n = n} 0ᶠ) ≡⟨⟩
        ⟨ y , 0ₗₘ ·ˡᵐ x ⟩               ∎

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


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

-- Any category can be made into a trivial restriction category

module Categories.Category.Restriction.Construction.Trivial where

open import Level using (Level)

open import Categories.Category.Core using (Category)
open import Categories.Category.Restriction using (Restriction)
open import Categories.Morphism.Reasoning.Core using (id-comm-sym)

private
  variable
     o ℓ e : Level

Trivial : (C : Category o ℓ e) → Restriction C
Trivial C = record
  { _↓ = λ _ → id
  ; pidʳ = identityʳ
  ; ↓-comm = Equiv.refl
  ; ↓-denestʳ = Equiv.sym identity²
  ; ↓-skew-comm = id-comm-sym C
  ; ↓-cong = λ _ → Equiv.refl
  }
  where open Category C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- basic stuff: core definitions, etc
open import statics-core
open import statics-checks
open import judgemental-erase
open import moveerase
open import examples

-- first wave theorems
open import sensibility
open import aasubsume-min
open import determinism

-- second wave theorems (checksums)
open import reachability
open import constructability

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

module Multidimensional.Data.Dir.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty

open import Cubical.Relation.Nullary

open import Multidimensional.Data.Dir.Base

¬↓≡↑ : ¬ ↓ ≡ ↑
¬↓≡↑ eq = subst (caseDir Dir ⊥) eq ↓

¬↑≡↓ : ¬ ↑ ≡ ↓
¬↑≡↓ eq = subst (caseDir ⊥ Dir) eq ↓

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Coproduct where

-- Coproduct of categories.  Need to pull out some of the combinators.
-- Coproduct of Groupoid as well.

open import Level
open import Data.Sum
open import Data.Empty
open import Relation.Binary using (Rel)
open import Function using (_$_)

open import Categories.Category
open import Categories.Category.Groupoid using (IsGroupoid)
import Categories.Morphism as Morphism

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

private
  _⊞_ : {a b c d r s : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         (R : A → B → Set r) (S : C → D → Set s) →
         (A ⊎ C) → (B ⊎ D) → Set (r ⊔ s)
  _⊞_ {r = r} {s = s} R S =
           λ { (inj₁ x) (inj₁ x₁) → Lift (r ⊔ s) (R x x₁)
             ; (inj₁ x) (inj₂ y) → Lift (r ⊔ s) ⊥
             ; (inj₂ y₁) (inj₁ x) → Lift (r ⊔ s) ⊥
             ; (inj₂ y₁) (inj₂ y) → Lift (r ⊔ s) (S y₁ y)
             }

  _⊞Rel_ : {a b c d r s u v : Level} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : A → B → Set r} {S : C → D → Set s}  →
         ({a₁ : A} {b₁ : B} → Rel (R a₁ b₁) u) → ({c₁ : C} {d₁ : D} → Rel (S c₁ d₁) v) →
         ({x : A ⊎ C} {y : B ⊎ D} → Rel (_⊞_ R S x y) (u ⊔ v))
  _⊞Rel_ {u = u} {v = v} R₁ R₂ {inj₁ x} {inj₁ x₁} p q = Lift (u ⊔ v) (R₁ (lower p) (lower q))
  (R₁ ⊞Rel R₂) {inj₁ x} {inj₂ y} () ()
  (R₁ ⊞Rel R₂) {inj₂ y₁} {inj₁ x} () ()
  _⊞Rel_ {u = u} {v = v} R₁ R₂ {inj₂ y₁} {inj₂ y} p q = Lift (u ⊔ v) (R₂ (lower p) (lower q))

Coproduct : (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
Coproduct C D = record
  { Obj = C.Obj ⊎ D.Obj
  ; _⇒_ = C._⇒_ ⊞ D._⇒_
  ; _≈_ = C._≈_ ⊞Rel D._≈_
  ; id = λ { {inj₁ _} → lift C.id ; {inj₂ _} → lift D.id }
  ; _∘_ = λ { {inj₁ x} {inj₁ x₁} {inj₁ x₂} → λ { (lift p) (lift q) → lift (p C.∘ q) }
            ; {inj₁ x} {inj₁ x₁} {inj₂ y} → λ ()
            ; {inj₁ x} {inj₂ y} {inj₁ x₁} → λ ()
            ; {inj₁ x} {inj₂ y} {inj₂ y₁} → λ _ ()
            ; {inj₂ y} {inj₁ x} {inj₁ x₁} → λ _ ()
            ; {inj₂ y} {inj₁ x} {inj₂ y₁} → λ ()
            ; {inj₂ y} {inj₂ y₁} {inj₁ x} → λ ()
            ; {inj₂ y} {inj₂ y₁} {inj₂ y₂} → λ { (lift p) (lift q) → lift (p D.∘ q) }
            }
  ; assoc = λ { {inj₁ x} {inj₁ x₁} {inj₁ x₂} {inj₁ x₃} → lift C.assoc
              ; {inj₂ y} {inj₂ y₁} {inj₂ y₂} {inj₂ y₃} → lift D.assoc}
  ; sym-assoc = λ { {inj₁ x} {inj₁ x₁} {inj₁ x₂} {inj₁ x₃} → lift C.sym-assoc
                  ; {inj₂ y} {inj₂ y₁} {inj₂ y₂} {inj₂ y₃} → lift D.sym-assoc}
  ; identityˡ = λ { {inj₁ x} {inj₁ x₁} → lift C.identityˡ
                  ; {inj₂ y} {inj₂ y₁} → lift D.identityˡ }
  ; identityʳ = λ { {inj₁ x} {inj₁ x₁} → lift C.identityʳ
                  ; {inj₂ y} {inj₂ y₁} → lift D.identityʳ}
  ; identity² = λ { {inj₁ x} → lift C.identity²
                  ; {inj₂ y} → lift D.identity² }
  ; equiv = λ { {inj₁ x} {inj₁ x₁} → record
                { refl = lift C.Equiv.refl
                ; sym = λ { (lift p) → lift $ C.Equiv.sym p }
                ; trans = λ { (lift p) (lift q) → lift $ C.Equiv.trans p q } }
              ; {inj₁ x} {inj₂ y} → record { refl = λ { {()} } ; sym = λ { {()} } ; trans = λ { {()} } }
              ; {inj₂ y} {inj₁ x} → record { refl = λ { {()} } ; sym = λ { {()} } ; trans = λ { {()} } }
              ; {inj₂ y} {inj₂ y₁} → record
                { refl = lift D.Equiv.refl
                ; sym = λ { (lift p) → lift $ D.Equiv.sym p }
                ; trans = λ { (lift p) (lift q) → lift $ D.Equiv.trans p q } }
              }
  ; ∘-resp-≈ = λ { {inj₁ x} {inj₁ x₁} {inj₁ x₂} → λ { (lift f≈h) (lift g≈i) → lift $ C.∘-resp-≈ f≈h g≈i }
                 ; {inj₂ y} {inj₂ y₁} {inj₂ y₂} → λ { (lift f≈h) (lift g≈i) → lift $ D.∘-resp-≈ f≈h g≈i } }
  }
  where
  module C = Category C
  module D = Category D

IsGroupoid-⊎ : {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → IsGroupoid C → IsGroupoid D → IsGroupoid (Coproduct C D)
IsGroupoid-⊎ G₁ G₂ = record
  { _⁻¹ = λ { {inj₁ x} {inj₁ x₁} (lift f) → lift $ IsGroupoid._⁻¹ G₁ f
            ; {inj₂ y} {inj₂ y₁} (lift f) → lift $ IsGroupoid._⁻¹ G₂ f
            }
  ; iso = λ { {inj₁ x} {inj₁ x₁} {lift f} → record
              { isoˡ = lift $ Iso.isoˡ i₁
              ; isoʳ = lift $ Iso.isoʳ i₁
              }
            ; {inj₂ y} {inj₂ y₁} {lift f} → record
              { isoˡ = lift $ Iso.isoˡ i₂
              ; isoʳ = lift $ Iso.isoʳ i₂
              }
            }
  }
  where
  open Morphism
  i₁ = IsGroupoid.iso G₁
  i₂ = IsGroupoid.iso G₂


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

open import HoTT
open import homotopy.EilenbergMacLane
open import cohomology.Theory
open import cohomology.SpectrumModel
open import cohomology.WithCoefficients

module cohomology.EMModel where

module _ {i} (G : Group i) (G-abelian : is-abelian G) where

  open EMExplicit G G-abelian using (⊙EM; EM-level; EM-conn; spectrum)

  private
    E : (n : ℤ) → Ptd i
    E O = ⊙EM O
    E (pos m) = ⊙EM (S m)
    E (neg m) = ⊙Lift ⊙Unit

    E-spectrum : (n : ℤ) → ⊙Ω (E (succ n)) == E n
    E-spectrum O = spectrum O
    E-spectrum (pos n) = spectrum (S n)
    E-spectrum (neg O) =
      ⊙ua (equiv (λ _ → _) (λ _ → idp)
            (λ _ → idp) (prop-has-all-paths (EM-level _ _ _) _))
          idp
    E-spectrum (neg (S n)) =
      ⊙ua (equiv (λ _ → _) (λ _ → idp)
            (λ _ → idp) (prop-has-all-paths (Lift-level Unit-is-set _ _) _))
          idp

  EM-Cohomology : CohomologyTheory i
  EM-Cohomology = spectrum-cohomology E E-spectrum

  open CohomologyTheory EM-Cohomology

  EM-dimension : (n : ℤ) → n ≠ O → C n (⊙Sphere O) == 0ᴳ
  EM-dimension O neq = ⊥-rec (neq idp)
  EM-dimension (pos n) _ =
    contr-is-0ᴳ _ $ connected-at-level-is-contr
      (Trunc-level {n = ⟨0⟩})
      (Trunc-preserves-conn ⟨0⟩
        (transport (λ B → is-connected ⟨0⟩ B)
          (! (Bool⊙→-path _))
          (path-conn (connected-≤T (⟨⟩-monotone-≤ (≤-ap-S (O≤ n)))
                                   (EM-conn (S n))))))
  EM-dimension (neg O) _ =
    contr-is-0ᴳ _ $ Trunc-preserves-level ⟨0⟩ $ ⊙→-level $
      inhab-prop-is-contr idp (EM-level O _ _)
  EM-dimension (neg (S n)) _ =
    contr-is-0ᴳ _ $ Trunc-preserves-level ⟨0⟩ $ ⊙→-level $
      Lift-level Unit-is-prop _ _

  EM-Ordinary : OrdinaryTheory i
  EM-Ordinary = ordinary-theory EM-Cohomology EM-dimension