text:
{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.GroupStructure where

open import Cubical.ZCohomology.Base

open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws renaming (assoc to assoc∙)
open import Cubical.Data.Sigma
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2 ; setTruncIsSet to §)
open import Cubical.Data.Int hiding (-_) renaming (_+_ to _ℤ+_)
open import Cubical.Data.Nat renaming (+-assoc to +-assocℕ ; +-comm to +-commℕ)
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3 ; map2 to trMap2)
open import Cubical.Homotopy.Loopspace
open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid

open Iso renaming (inv to inv')

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'
    A' : Pointed ℓ

infixr 34 _+ₖ_
infixr 34 _+ₕ_
infixr 34 _+ₕ∙_

-- Addition in the Eilenberg-Maclane spaces is uniquely determined if we require it to have left- and right-unit laws,
-- such that these agree on 0. In particular, any h-structure (see http://ericfinster.github.io/files/emhott.pdf) is unique.
+ₖ-unique : (n : ℕ) → (comp1 comp2 : coHomK (suc n) → coHomK (suc n) → coHomK (suc n))
         → (rUnit1 : (x : _) → comp1 x (coHom-pt (suc n)) ≡ x)
         → (lUnit1 : (x : _) → comp1 (coHom-pt (suc n)) x ≡ x)
         → (rUnit2 : (x : _) → comp2 x (coHom-pt (suc n)) ≡ x)
         → (lUnit2 : (x : _) → comp2 (coHom-pt (suc n)) x ≡ x)
         → (unId1 : rUnit1 (coHom-pt (suc n)) ≡ lUnit1 (coHom-pt (suc n)))
         → (unId2 : rUnit2 (coHom-pt (suc n)) ≡ lUnit2 (coHom-pt (suc n)))
         → (x y : _) → comp1 x y ≡ comp2 x y
+ₖ-unique n comp1 comp2 rUnit1 lUnit1 rUnit2 lUnit2 unId1 unId2 =
  elim2 (λ _ _ → isOfHLevelPath (3 + n) (isOfHLevelTrunc (3 + n)) _ _)
        (wedgeConSn _ _
        (λ _ _ → help _ _)
        (λ x → lUnit1 ∣ x ∣ ∙ sym (lUnit2 ∣ x ∣))
        (λ x → rUnit1 ∣ x ∣ ∙ sym (rUnit2 ∣ x ∣))
        (cong₂ _∙_ unId1 (cong sym unId2)) .fst)
  where
  help : isOfHLevel (2 + (n + suc n)) (coHomK (suc n))
  help = subst (λ x → isOfHLevel x (coHomK (suc n))) (+-suc n (2 + n) ∙ +-suc (suc n) (suc n))
               (isOfHLevelPlus n (isOfHLevelTrunc (3 + n)))

wedgeConHLev : (n : ℕ) → isOfHLevel ((2 + n) + (2 + n)) (coHomK (2 + n))
wedgeConHLev n = subst (λ x → isOfHLevel x (coHomK (2 + n)))
                       (sym (+-suc (2 + n) (suc n) ∙ +-suc (3 + n) n))
                       (isOfHLevelPlus' {n = n} (4 + n) (isOfHLevelTrunc (4 + n)))
wedgeConHLev' : (n : ℕ) → isOfHLevel ((2 + n) + (2 + n)) (typ (Ω (coHomK-ptd (3 + n))))
wedgeConHLev' n = subst (λ x → isOfHLevel x (typ (Ω (coHomK-ptd (3 + n)))))
                        (sym (+-suc (2 + n) (suc n) ∙ +-suc (3 + n) n))
                        (isOfHLevelPlus' {n = n} (4 + n) (isOfHLevelTrunc (5 + n) _ _))

wedgeConHLevPath : (n : ℕ) → (x y : coHomK (suc n)) → isOfHLevel ((suc n) + (suc n)) (x ≡ y)
wedgeConHLevPath zero x y = isOfHLevelTrunc 3 _ _
wedgeConHLevPath (suc n) x y = isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev n) _ _

-- addition for n ≥ 2 together with the left- and right-unit laws (modulo truncations)
preAdd : (n : ℕ) → Σ[ f ∈ (S₊ (2 + n) → S₊ (2 + n) → coHomK (2 + n)) ]
                       ((x : S₊ (2 + n)) → f north x ≡ ∣ x ∣)
                     × ((x : S₊ (2 + n)) → f x north ≡ ∣ x ∣)
preAdd n =
  wedgeConSn _ _
             (λ _ _ → wedgeConHLev n)
             ∣_∣
             ∣_∣
             refl

-- addition for n = 1
wedgeMapS¹ : S¹ → S¹ → S¹
wedgeMapS¹ base y = y
wedgeMapS¹ (loop i) base = loop i
wedgeMapS¹ (loop i) (loop j) =
  hcomp (λ k → λ { (i = i0) → loop j
                  ; (i = i1) → loop (j ∧ k)
                  ; (j = i0) → loop i
                  ; (j = i1) → loop (i ∧ k)})
        (loop (i ∨ j))

---------- Algebra/Group stuff --------
0ₖ : (n : ℕ) → coHomK n
0ₖ = coHom-pt

_+ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_+ₖ_ {n = zero} x y = x ℤ+ y
_+ₖ_ {n = suc zero} = trMap2 wedgeMapS¹
_+ₖ_ {n = suc (suc n)} = trRec (isOfHLevelΠ (4 + n) λ _ → isOfHLevelTrunc (4 + n))
                            λ x → trRec (isOfHLevelTrunc (4 + n)) λ y → preAdd n .fst x y

private
  isEquiv+ : (n : ℕ) → (x : coHomK (suc n)) → isEquiv (_+ₖ_ {n = (suc n)} x)
  isEquiv+ zero =
    trElim (λ _ → isProp→isOfHLevelSuc 2 (isPropIsEquiv _))
           (toPropElim (λ _ → isPropIsEquiv _)
                       (subst isEquiv (sym help) (idIsEquiv _)))
    where
    help : _+ₖ_ {n = 1} (coHom-pt 1) ≡ idfun _
    help = funExt (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
                  λ _ → refl)
  isEquiv+ (suc n) =
    trElim (λ _ → isProp→isOfHLevelSuc (3 + n) (isPropIsEquiv _))
           (suspToPropElim (ptSn (suc n)) (λ _ → isPropIsEquiv _)
           (subst isEquiv (sym help) (idIsEquiv _)))
    where
    help : _+ₖ_ {n = (2 + n)} (coHom-pt (2 + n)) ≡ idfun _
    help = funExt (trElim (λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _) λ _ → refl)

  Kₙ≃Kₙ : (n : ℕ) (x : coHomK (suc n)) → coHomK (suc n) ≃ coHomK (suc n)
  Kₙ≃Kₙ n x = _ , isEquiv+ n x

-ₖ_ : {n : ℕ} →  coHomK n → coHomK n
-ₖ_ {n = zero} x = 0 - x
-ₖ_ {n = suc n} x = invEq (Kₙ≃Kₙ n x) (coHom-pt (suc n))

_-ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_-ₖ_ {n = n} x y = _+ₖ_ {n = n} x (-ₖ_ {n = n} y)

+ₖ-syntax : (n : ℕ) → coHomK n → coHomK n → coHomK n
+ₖ-syntax n = _+ₖ_ {n = n}

-ₖ-syntax : (n : ℕ) → coHomK n → coHomK n
-ₖ-syntax n = -ₖ_ {n = n}

-'ₖ-syntax : (n : ℕ) → coHomK n → coHomK n → coHomK n
-'ₖ-syntax n = _-ₖ_ {n = n}

syntax +ₖ-syntax n x y = x +[ n ]ₖ y
syntax -ₖ-syntax n x = -[ n ]ₖ x
syntax -'ₖ-syntax n x y = x -[ n ]ₖ y

------- Groupoid Laws for Kₙ ---------
commₖ : (n : ℕ) → (x y : coHomK n) → x +[ n ]ₖ y ≡ y +[ n ]ₖ x
commₖ zero = +-comm
commₖ (suc zero) =
  elim2 (λ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
        (wedgeConSn _ _
          (λ _ _ → isOfHLevelTrunc 3 _ _)
          (λ {base → refl ; (loop i) → refl})
          (λ {base → refl ; (loop i) → refl})
          refl .fst)
commₖ (suc (suc n)) =
  elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
        (wedgeConSn _ _
                    (λ x y → isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev n) _ _)
                    (λ x → preAdd n .snd .fst x ∙ sym (preAdd n .snd .snd x))
                    (λ x → preAdd n .snd .snd x ∙ sym (preAdd n .snd .fst x))
                    refl .fst)

commₖ-base : (n : ℕ) → commₖ n (coHom-pt n) (coHom-pt n) ≡ refl
commₖ-base zero = refl
commₖ-base (suc zero) = refl
commₖ-base (suc (suc n)) = sym (rUnit _)

rCancelₖ : (n : ℕ) → (x : coHomK n) → x -[ n ]ₖ x ≡ coHom-pt n
rCancelₖ zero x = +-comm x (pos 0 - x) ∙ minusPlus x 0
rCancelₖ (suc n) x = retEq (Kₙ≃Kₙ n x) (coHom-pt _)

lCancelₖ : (n : ℕ) → (x : coHomK n) → (-[ n ]ₖ x) +[ n ]ₖ x ≡ coHom-pt n
lCancelₖ zero x = minusPlus x 0
lCancelₖ (suc n) x = commₖ (suc n) _ _ ∙ rCancelₖ (suc n) x

rUnitₖ : (n : ℕ) → (x : coHomK n) → x +[ n ]ₖ coHom-pt n ≡ x
rUnitₖ zero x = refl
rUnitₖ (suc zero) =
  trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
         λ {base → refl
         ; (loop i) → refl}
rUnitₖ (suc (suc n)) =
  trElim (λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
          λ x → preAdd n .snd .snd x

lUnitₖ : (n : ℕ) → (x : coHomK n) → coHom-pt n +[ n ]ₖ x ≡ x
lUnitₖ zero x = sym (pos0+ x)
lUnitₖ (suc zero) =
  trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
         λ {base → refl
         ; (loop i) → refl}
lUnitₖ (suc (suc n)) =
  trElim (λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
          λ x → refl

assocₖ : (n : ℕ) → (x y z : coHomK n) → x +[ n ]ₖ (y +[ n ]ₖ z) ≡ (x +[ n ]ₖ y) +[ n ]ₖ z
assocₖ zero = +-assoc
assocₖ (suc zero) =
  trElim3 (λ _ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
          λ x → wedgeConSn _ _
                (λ _ _ → isOfHLevelTrunc 3 _ _)
                (λ y i → rUnitₖ 1 ∣ x ∣ (~ i) +ₖ ∣ y ∣)
                (λ z → cong (∣ x ∣ +ₖ_) (rUnitₖ 1 ∣ z ∣) ∙ sym (rUnitₖ 1 (∣ x ∣ +ₖ ∣ z ∣)))
                (helper x) .fst
  where
  helper : (x : S¹) → cong (∣ x ∣ +ₖ_) (rUnitₖ 1 ∣ base ∣) ∙ sym (rUnitₖ 1 (∣ x ∣ +ₖ ∣ base ∣))
                    ≡ (cong (_+ₖ ∣ base ∣) (sym (rUnitₖ 1 ∣ x ∣)))
  helper = toPropElim (λ _ → isOfHLevelTrunc 3 _ _ _ _)
                      (sym (lUnit refl))
assocₖ (suc (suc n)) =
  trElim3 (λ _ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
          (wedgeConSn-×3 _
            (λ x z i → preAdd n .snd .snd x (~ i) +ₖ ∣ z ∣)
            (λ x y → cong (∣ x ∣ +ₖ_) (rUnitₖ (2 + n) ∣ y ∣) ∙ sym (rUnitₖ (2 + n) (∣ x ∣ +ₖ ∣ y ∣)))
            (lUnit (sym (rUnitₖ (2 + n) (∣ north ∣ +ₖ ∣ north ∣)))))
  where
  wedgeConSn-×3 : (n : ℕ)
          → (f : (x z : S₊ (2 + n))→ ∣ x ∣ +ₖ ((0ₖ _) +ₖ ∣ z ∣) ≡ (∣ x ∣ +ₖ (0ₖ _)) +ₖ ∣ z ∣)
          → (g : (x y : S₊ (2 + n)) → ∣ x ∣ +ₖ (∣ y ∣ +ₖ 0ₖ _) ≡ (∣ x ∣ +ₖ ∣ y ∣) +ₖ 0ₖ _)
          → (f (ptSn _) (ptSn _) ≡ g (ptSn _) (ptSn _))
          → (x y z : S₊ (2 + n)) → ∣ x ∣ +ₖ (∣ y ∣ +ₖ ∣ z ∣) ≡ (∣ x ∣ +ₖ ∣ y ∣) +ₖ ∣ z ∣
  wedgeConSn-×3 n f g d x =
    wedgeConSn _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev n) _ _)
               (f x)
               (g x)
               (sphereElim _ {A = λ x → g x (ptSn (suc (suc n))) ≡ f x (ptSn (suc (suc n))) }
                             (λ _ → isOfHLevelTrunc (4 + n) _ _ _ _)
                             (sym d) x) .fst
{-
This was the original proof for the case n ≥ 2:
For some reason it doesn't check in reasonable time anymore:
assocₖ (suc (suc n)) =
  trElim3 (λ _ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
          λ x → wedgeConSn _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev n) _ _)
                           (λ z i → preAdd n .snd .snd x (~ i) +ₖ ∣ z ∣)
                           (λ y → cong (∣ x ∣ +ₖ_) (rUnitₖ (2 + n) ∣ y ∣) ∙ sym (rUnitₖ (2 + n) (∣ x ∣ +ₖ ∣ y ∣)))
                           (helper x) .fst
  where
  helper : (x : S₊ (2 + n)) → cong (∣ x ∣ +ₖ_) (rUnitₖ (2 + n) ∣ north ∣) ∙ sym (rUnitₖ (2 + n) (∣ x ∣ +ₖ ∣ north ∣))
                          ≡ cong (_+ₖ ∣ north ∣) (sym (preAdd n .snd .snd x))
  helper = sphereElim (suc n) (λ _ → isOfHLevelTrunc (4 + n) _ _ _ _)
                              (sym (lUnit (sym (rUnitₖ (2 + n) (∣ north ∣ +ₖ ∣ north ∣)))))
-}

lUnitₖ≡rUnitₖ : (n : ℕ) → lUnitₖ n (coHom-pt n) ≡ rUnitₖ n (coHom-pt n)
lUnitₖ≡rUnitₖ zero = isSetInt _ _ _ _
lUnitₖ≡rUnitₖ (suc zero) = refl
lUnitₖ≡rUnitₖ (suc (suc n)) = refl

------ Commutativity of  ΩKₙ
-- We show that p ∙ q ≡ (λ i → (p i) +ₖ (q i)) for any p q : ΩKₙ₊₁. This allows us to prove that p ∙ q ≡ q ∙ p
-- without having to use the equivalence Kₙ ≃ ΩKₙ₊₁
∙≡+₁ : (p q : typ (Ω (coHomK-ptd 1))) → p ∙ q ≡ cong₂ _+ₖ_ p q
∙≡+₁ p q = (λ i → (λ j → rUnitₖ 1 (p j) (~ i)) ∙ λ j → lUnitₖ 1 (q j) (~ i)) ∙  sym (cong₂Funct _+ₖ_ p q)

∙≡+₂ : (n : ℕ) (p q : typ (Ω (coHomK-ptd (suc (suc n))))) → p ∙ q ≡ cong₂ _+ₖ_ p q
∙≡+₂ n p q = (λ i → (λ j → rUnitₖ (2 + n) (p j) (~ i)) ∙ λ j → lUnitₖ (2 + n) (q j) (~ i)) ∙ sym (cong₂Funct _+ₖ_ p q)

cong+ₖ-comm : (n : ℕ) (p q : typ (Ω (coHomK-ptd (suc n)))) → cong₂ _+ₖ_ p q ≡ cong₂ _+ₖ_ q p
cong+ₖ-comm zero p q =
     rUnit (cong₂ _+ₖ_ p q)
  ∙∙ (λ i → (λ j → commₖ 1 ∣ base ∣ ∣ base ∣ (i ∧ j))
     ∙∙ (λ j → commₖ 1 (p j) (q j) i)
     ∙∙ λ j → commₖ 1 ∣ base ∣ ∣ base ∣ (i ∧ ~ j))
  ∙∙ ((λ i → commₖ-base 1 i ∙∙ cong₂ _+ₖ_ q p ∙∙ sym (commₖ-base 1 i))
    ∙ sym (rUnit (cong₂ _+ₖ_ q p)))
cong+ₖ-comm (suc n) p q =
     rUnit (cong₂ _+ₖ_ p q)
  ∙∙ (λ i → (λ j → commₖ (2 + n) ∣ north ∣ ∣ north ∣ (i ∧ j))
     ∙∙ (λ j → commₖ (2 + n) (p j) (q j) i )
     ∙∙ λ j → commₖ (2 + n) ∣ north ∣ ∣ north ∣ (i ∧ ~ j))
  ∙∙ ((λ i → commₖ-base (2 + n) i ∙∙ cong₂ _+ₖ_ q p ∙∙ sym (commₖ-base (2 + n) i))
    ∙ sym (rUnit (cong₂ _+ₖ_ q p)))

isCommΩK : (n : ℕ) → isComm∙ (coHomK-ptd n)
isCommΩK zero p q = isSetInt _ _ (p ∙ q) (q ∙ p)
isCommΩK (suc zero) p q = ∙≡+₁ p q ∙∙ cong+ₖ-comm 0 p q ∙∙ sym (∙≡+₁ q p)
isCommΩK (suc (suc n)) p q = ∙≡+₂ n p q ∙∙ cong+ₖ-comm (suc n) p q ∙∙ sym (∙≡+₂ n q p)

----- some other useful lemmas about algebra in Kₙ
-0ₖ : {n : ℕ} → -[ n ]ₖ (0ₖ n) ≡ (0ₖ n)
-0ₖ {n = zero} = refl
-0ₖ {n = suc zero} = refl
-0ₖ {n = suc (suc n)} = refl

-distrₖ : (n : ℕ) (x y : coHomK n) → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y)
-distrₖ zero x y = GroupLemmas.invDistr intGroup x y ∙ +-comm (0 - y) (0 - x)
-distrₖ (suc zero) =
  elim2 (λ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
        (wedgeConSn _ _ (λ _ _ → isOfHLevelTrunc 3 _ _)
          (λ x → sym (lUnitₖ 1 (-[ 1 ]ₖ ∣ x ∣)))
          (λ x → cong (λ x → -[ 1 ]ₖ x) (rUnitₖ 1 ∣ x ∣) ∙ sym (rUnitₖ 1 (-[ 1 ]ₖ ∣ x ∣)))
          (sym (rUnit refl)) .fst)
-distrₖ (suc (suc n)) =
  elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
        (wedgeConSn _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev n) _ _)
                        (λ x → sym (lUnitₖ (2 + n) (-[ (2 + n) ]ₖ ∣ x ∣)))
                        (λ x → cong (λ x → -[ (2 + n) ]ₖ x) (rUnitₖ (2 + n) ∣ x ∣ ) ∙ sym (rUnitₖ (2 + n) (-[ (2 + n) ]ₖ ∣ x ∣)))
                        (sym (rUnit refl)) .fst)

-cancelRₖ : (n : ℕ) (x y : coHomK n) → (y +[ n ]ₖ x) -[ n ]ₖ x ≡ y
-cancelRₖ zero x y = sym (+-assoc y x (0 - x))
                  ∙∙ cong (y ℤ+_) (+-comm x (0 - x))
                  ∙∙ cong (y ℤ+_) (minusPlus x (pos 0))
-cancelRₖ (suc zero) =
  elim2 (λ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
        (wedgeConSn _ _ (λ _ _ → wedgeConHLevPath 0 _ _)
                        (λ x → cong (_+ₖ ∣ base ∣) (rUnitₖ 1 ∣ x ∣) ∙ rUnitₖ 1 ∣ x ∣)
                        (λ x → rCancelₖ 1 ∣ x ∣)
                        (transportRefl refl ∙ rUnit refl) .fst)
-cancelRₖ (suc (suc n)) =
  elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
        (wedgeConSn _ _ (λ _ _ → wedgeConHLevPath (suc n) _ _)
                        (λ x → cong (_+ₖ ∣ north ∣) (rUnitₖ (2 + n) ∣ x ∣) ∙ rUnitₖ (2 + n) ∣ x ∣)
                        (λ x → rCancelₖ (2 + n) ∣ x ∣)
                        (transportRefl refl ∙ rUnit refl) .fst)

-cancelLₖ : (n : ℕ) (x y : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ x ≡ y
-cancelLₖ n x y = cong (λ z → z -[ n ]ₖ x) (commₖ n x y) ∙ -cancelRₖ n x y

-+cancelₖ : (n : ℕ) (x y : coHomK n) → (x -[ n ]ₖ y) +[ n ]ₖ y ≡ x
-+cancelₖ zero x y = sym (+-assoc x (0 - y) y) ∙ cong (x ℤ+_) (minusPlus y (pos 0))
-+cancelₖ (suc zero) =
  elim2 (λ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
        (wedgeConSn _ _ (λ _ _ → wedgeConHLevPath 0 _ _)
          (λ x → cong (_+ₖ ∣ x ∣) (lUnitₖ 1 (-ₖ ∣ x ∣)) ∙ lCancelₖ 1 ∣ x ∣)
          (λ x → cong (_+ₖ ∣ base ∣) (rUnitₖ 1 ∣ x ∣) ∙ rUnitₖ 1 ∣ x ∣)
          ((λ i → refl ∙ (transportRefl refl (~ i))) ∙ lUnit _) .fst)
-+cancelₖ (suc (suc n)) =
  elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
        (wedgeConSn _ _ (λ _ _ → wedgeConHLevPath (suc n) _ _)
          (λ x → cong (_+ₖ ∣ x ∣) (lUnitₖ (2 + n) (-ₖ ∣ x ∣)) ∙ lCancelₖ (2 + n) ∣ x ∣)
          (λ x → cong (_+ₖ ∣ north ∣) (rUnitₖ (2 + n) ∣ x ∣) ∙ rUnitₖ (2 + n) ∣ x ∣)
          (cong (refl ∙_) (rUnit refl ∙ (λ i → rUnit refl i ∙ transportRefl refl (~ i)))) .fst)

---- Group structure of cohomology groups
_+ₕ_ : {n : ℕ} → coHom n A → coHom n A → coHom n A
_+ₕ_ {n = n} = sRec2 § λ a b → ∣ (λ x → a x +[ n ]ₖ b x) ∣₂

-ₕ_  : {n : ℕ} → coHom n A → coHom n A
-ₕ_  {n = n} = sRec § λ a → ∣ (λ x → -[ n ]ₖ a x) ∣₂

_-ₕ_  : {n : ℕ} → coHom n A → coHom n A → coHom n A
_-ₕ_  {n = n} = sRec2 § λ a b → ∣ (λ x → a x -[ n ]ₖ b x) ∣₂

+ₕ-syntax : (n : ℕ) → coHom n A → coHom n A → coHom n A
+ₕ-syntax n = _+ₕ_ {n = n}

-ₕ-syntax : (n : ℕ) → coHom n A → coHom n A
-ₕ-syntax n = -ₕ_ {n = n}

-ₕ'-syntax : (n : ℕ) → coHom n A → coHom n A → coHom n A
-ₕ'-syntax n = _-ₕ_ {n = n}

syntax +ₕ-syntax n x y = x +[ n ]ₕ y
syntax -ₕ-syntax n x = -[ n ]ₕ x
syntax -ₕ'-syntax n x y = x -[ n ]ₕ y

0ₕ : (n : ℕ) → coHom n A
0ₕ n = ∣ (λ _ → (0ₖ n)) ∣₂

rUnitₕ : (n : ℕ) (x : coHom n A) → x +[ n ]ₕ (0ₕ n) ≡ x
rUnitₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                λ a i → ∣ funExt (λ x → rUnitₖ n (a x)) i ∣₂

lUnitₕ : (n : ℕ) (x : coHom n A) → (0ₕ n) +[ n ]ₕ x ≡ x
lUnitₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                  λ a i → ∣ funExt (λ x → lUnitₖ n (a x)) i ∣₂

rCancelₕ : (n : ℕ) (x : coHom n A) → x +[ n ]ₕ (-[ n ]ₕ x) ≡ 0ₕ n
rCancelₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → rCancelₖ n (a x)) i ∣₂

lCancelₕ : (n : ℕ) (x : coHom n A) → (-[ n ]ₕ x) +[ n ]ₕ x  ≡ 0ₕ n
lCancelₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → lCancelₖ n (a x)) i ∣₂

assocₕ : (n : ℕ) (x y z : coHom n A) →  (x +[ n ]ₕ (y +[ n ]ₕ z)) ≡ ((x +[ n ]ₕ y) +[ n ]ₕ z)
assocₕ n = elim3 (λ _ _ _ → isOfHLevelPath 1 (§ _ _))
               λ a b c i → ∣ funExt (λ x → assocₖ n (a x) (b x) (c x)) i ∣₂

commₕ : (n : ℕ) (x y : coHom n A) → (x +[ n ]ₕ y) ≡ (y +[ n ]ₕ x)
commₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ funExt (λ x → commₖ n (a x) (b x)) i ∣₂

-cancelLₕ : (n : ℕ) (x y : coHom n A) → (x +[ n ]ₕ y) -[ n ]ₕ x ≡ y
-cancelLₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -cancelLₖ n (a x) (b x) i) ∣₂

-cancelRₕ : (n : ℕ) (x y : coHom n A) → (y +[ n ]ₕ x) -[ n ]ₕ x ≡ y
-cancelRₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -cancelRₖ n (a x) (b x) i) ∣₂

-+cancelₕ : (n : ℕ) (x y : coHom n A) → (x -[ n ]ₕ y) +[ n ]ₕ y ≡ x
-+cancelₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -+cancelₖ n (a x) (b x) i) ∣₂

-- Group structure of reduced cohomology groups (in progress - might need K to compute properly first)
_+ₕ∙_ : {A : Pointed ℓ} {n : ℕ} → coHomRed n A → coHomRed n A → coHomRed n A
_+ₕ∙_ {n = zero} = sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ zero ]ₖ b x)
                                            , (λ i → (pa i +[ zero ]ₖ pb i)) ∣₂ }
_+ₕ∙_ {n = (suc zero)} = sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ 1 ]ₖ b x)
                                                 , (λ i → pa i +[ 1 ]ₖ pb i) ∣₂ }
_+ₕ∙_ {n = (suc (suc n))} =
  sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ (2 + n) ]ₖ b x)
                                  , (λ i → pa i +[ (2 + n) ]ₖ pb i) ∣₂ }

-ₕ∙_ : {A : Pointed ℓ} {n : ℕ} → coHomRed n A → coHomRed n A
-ₕ∙_ {n = zero} = sRec § λ {(f , p) → ∣ (λ x → -[ 0 ]ₖ (f x))
                                      , cong (λ x → -[ 0 ]ₖ x) p ∣₂}
-ₕ∙_ {n = suc zero} = sRec § λ {(f , p) → ∣ (λ x → -ₖ (f x))
                                           , cong -ₖ_ p ∣₂}
-ₕ∙_ {n = suc (suc n)} = sRec § λ {(f , p) → ∣ (λ x → -ₖ (f x))
                                             , cong -ₖ_ p ∣₂}

0ₕ∙ : {A : Pointed ℓ} (n : ℕ) → coHomRed n A
0ₕ∙ n = ∣ (λ _ → 0ₖ n) , refl ∣₂

+ₕ∙-syntax : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A → coHomRed n A
+ₕ∙-syntax n = _+ₕ∙_ {n = n}

-ₕ∙-syntax : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A
-ₕ∙-syntax n = -ₕ∙_ {n = n}

-'ₕ∙-syntax : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A → coHomRed n A
-'ₕ∙-syntax n x y = _+ₕ∙_ {n = n} x (-ₕ∙_ {n = n} y)

syntax +ₕ∙-syntax n x y = x +[ n ]ₕ∙ y
syntax -ₕ∙-syntax n x = -[ n ]ₕ∙ x
syntax -'ₕ∙-syntax n x y = x -[ n ]ₕ∙ y

commₕ∙ : {A : Pointed ℓ} (n : ℕ) (x y : coHomRed n A) → x +[ n ]ₕ∙ y ≡ y +[ n ]ₕ∙ x
commₕ∙ zero =
  sElim2 (λ _ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) (g , q)
           → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) λ i x → commₖ 0 (f x) (g x) i)}
commₕ∙ (suc zero) =
  sElim2 (λ _ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) (g , q)
           → cong ∣_∣₂ (ΣPathP ((λ i x → commₖ 1 (f x) (g x) i)
                             , λ i j → commₖ 1 (p j) (q j) i))}
commₕ∙ {A = A} (suc (suc n)) =
  sElim2 (λ _ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) (g , q)
           → cong ∣_∣₂ (ΣPathP ((λ i x → commₖ (2 + n) (f x) (g x) i)
                              , λ i j → hcomp (λ k → λ {(i = i0) → p j +ₖ q j
                                                        ; (i = i1) → q j +ₖ p j
                                                        ; (j = i0) → commₖ (2 + n) (f (pt A)) (g (pt A)) i
                                                        ; (j = i1) → rUnit (refl {x = 0ₖ (2 + n)}) (~ k) i})
                                               (commₖ (2 + n) (p j) (q j) i)))}

rUnitₕ∙ : {A : Pointed ℓ} (n : ℕ) (x : coHomRed n A) → x +[ n ]ₕ∙ 0ₕ∙ n ≡ x
rUnitₕ∙ zero =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) λ i x → rUnitₖ zero (f x) i)}
rUnitₕ∙ (suc zero) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) → cong ∣_∣₂ (ΣPathP ((λ i x → rUnitₖ 1 (f x) i) , λ i j → rUnitₖ 1 (p j) i))}
rUnitₕ∙ (suc (suc n)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) → cong ∣_∣₂ (ΣPathP ((λ i x → rUnitₖ (2 + n) (f x) i) , λ i j → rUnitₖ (2 + n) (p j) i))}

lUnitₕ∙ : {A : Pointed ℓ} (n : ℕ) (x : coHomRed n A) → 0ₕ∙ n +[ n ]ₕ∙ x ≡ x
lUnitₕ∙ zero =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) λ i x → lUnitₖ zero (f x) i)}
lUnitₕ∙ (suc zero) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) → cong ∣_∣₂ (ΣPathP ((λ i x → lUnitₖ 1 (f x) i) , λ i j → lUnitₖ 1 (p j) i))}
lUnitₕ∙ (suc (suc n)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) → cong ∣_∣₂ (ΣPathP ((λ i x → lUnitₖ (2 + n) (f x) i) , λ i j → lUnitₖ (2 + n) (p j) i))}

rCancelₕ∙ : {A : Pointed ℓ} (n : ℕ) (x : coHomRed n A) → x +[ n ]ₕ∙ (-[ n ]ₕ∙ x) ≡ 0ₕ∙ n
rCancelₕ∙ zero =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) λ i x → rCancelₖ zero (f x) i)}
rCancelₕ∙ {A = A} (suc zero) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p)
           → cong ∣_∣₂ (ΣPathP ((λ i x → rCancelₖ 1 (f x) i)
                               , λ i j → hcomp (λ k → λ { (i = i0) → p j +ₖ (-ₖ p j)
                                                         ; (i = i1) → 0ₖ 1
                                                         ; (j = i0) → rCancelₖ 1 (f (pt A)) i
                                                         ; (j = i1) → transportRefl (refl {x = 0ₖ 1}) k i})
                                                           (rCancelₖ 1 (p j) i)))}
rCancelₕ∙ {A = A} (suc (suc n)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p)
           → cong ∣_∣₂ (ΣPathP ((λ i x → rCancelₖ (2 + n) (f x) i)
                               , λ i j → hcomp (λ k → λ { (i = i0) → p j +ₖ (-ₖ p j)
                                                         ; (i = i1) → 0ₖ (2 + n)
                                                         ; (j = i0) → rCancelₖ (2 + n) (f (pt A)) i
                                                         ; (j = i1) → transportRefl (refl {x = 0ₖ (2 + n)}) k i})
                                                (rCancelₖ (2 + n) (p j) i)))}

lCancel-refl : lCancelₖ 1 (0ₖ _) ≡ refl
lCancel-refl = (λ i → refl ∙ transportRefl refl i) ∙ sym (rUnit refl)

lCancelₕ∙ : {A : Pointed ℓ} (n : ℕ) (x : coHomRed n A) → (-[ n ]ₕ∙ x) +[ n ]ₕ∙ x ≡ 0ₕ∙ n
lCancelₕ∙ zero =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p) → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) λ i x → lCancelₖ zero (f x) i)}
lCancelₕ∙ {A = A} (suc zero) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p)
           → cong ∣_∣₂ (ΣPathP ((λ i x → lCancelₖ 1 (f x) i)
                               , λ i j → hcomp (λ k → λ { (i = i0) → (-ₖ p j) +ₖ (p j)
                                                         ; (i = i1) → 0ₖ 1
                                                         ; (j = i0) → lCancelₖ 1 (f (pt A)) i
                                                         ; (j = i1) → ((λ i → refl {x = 0ₖ 1}
                                                                      ∙ transportRefl refl i) ∙ sym (rUnit refl)) k i})
                                                (lCancelₖ 1 (p j) i)))}
lCancelₕ∙ {A = A} (suc (suc n)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ {(f , p)
           → cong ∣_∣₂ (ΣPathP ((λ i x → lCancelₖ (2 + n) (f x) i)
                               , λ i j → hcomp (λ k → λ { (i = i0) → (-ₖ p j) +ₖ (p j)
                                                         ; (i = i1) → 0ₖ (2 + n)
                                                         ; (j = i0) → lCancelₖ (2 + n) (f (pt A)) i
                                                         ; (j = i1) → ((λ i → (rUnit refl (~ i))
                                                                              ∙ (transportRefl (refl {x = 0ₖ (2 + n)}) i))
                                                                       ∙ sym (rUnit refl)) k i})
                                                (lCancelₖ (2 + n) (p j) i)))}

assocₕ∙ : {A : Pointed ℓ} (n : ℕ) (x y z : coHomRed n A)
       → (x +[ n ]ₕ∙ (y +[ n ]ₕ∙ z)) ≡ ((x +[ n ]ₕ∙ y) +[ n ]ₕ∙ z)
assocₕ∙ zero =
  elim3 (λ _ _ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) (g , q) (h , r)
          → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _)
                              (λ i x → assocₖ zero (f x) (g x) (h x) i))}
assocₕ∙ (suc zero) =
  elim3 (λ _ _ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) (g , q) (h , r)
          → cong ∣_∣₂ (ΣPathP ((λ i x → assocₖ 1 (f x) (g x) (h x) i)
                             , λ i j → assocₖ 1 (p j) (q j) (r j) i))}
assocₕ∙ (suc (suc n)) =
  elim3 (λ _ _ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) (g , q) (h , r)
          → cong ∣_∣₂ (ΣPathP ((λ i x → assocₖ (2 + n) (f x) (g x) (h x) i)
                             , λ i j → assocₖ (2 + n) (p j) (q j) (r j) i))}

open IsSemigroup
open IsMonoid
open GroupStr
open GroupHom

coHomGr : (n : ℕ) (A : Type ℓ) → Group {ℓ}
coHomGr n A = coHom n A , coHomGrnA
  where
  coHomGrnA : GroupStr (coHom n A)
  0g coHomGrnA = 0ₕ n
  GroupStr._+_ coHomGrnA = λ x y → x +[ n ]ₕ y
  - coHomGrnA = λ x → -[ n ]ₕ x
  isGroup coHomGrnA = helper
    where
    abstract
      helper : IsGroup {G = coHom n A} (0ₕ n) (λ x y → x +[ n ]ₕ y) (λ x → -[ n ]ₕ x)
      helper = makeIsGroup § (assocₕ n) (rUnitₕ n) (lUnitₕ n) (rCancelₕ n) (lCancelₕ n)

×coHomGr : (n : ℕ) (A : Type ℓ) (B : Type ℓ') → Group
×coHomGr n A B = dirProd (coHomGr n A) (coHomGr n B)

coHomGroup : (n : ℕ) (A : Type ℓ) → AbGroup {ℓ}
fst (coHomGroup n A) = coHom n A
AbGroupStr.0g (snd (coHomGroup n A)) = 0ₕ n
AbGroupStr._+_ (snd (coHomGroup n A)) = _+ₕ_ {n = n}
AbGroupStr.- snd (coHomGroup n A) = -ₕ_ {n = n}
IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd (coHomGroup n A))) = isGroup (snd (coHomGr n A))
IsAbGroup.comm (AbGroupStr.isAbGroup (snd (coHomGroup n A))) = commₕ n

-- Reduced cohomology group (direct def)

coHomRedGroupDir : (n : ℕ) (A : Pointed ℓ) → AbGroup {ℓ}
fst (coHomRedGroupDir n A) = coHomRed n A
AbGroupStr.0g (snd (coHomRedGroupDir n A)) = 0ₕ∙ n
AbGroupStr._+_ (snd (coHomRedGroupDir n A)) = _+ₕ∙_ {n = n}
AbGroupStr.- snd (coHomRedGroupDir n A) = -ₕ∙_ {n = n}
IsAbGroup.isGroup (AbGroupStr.isAbGroup (snd (coHomRedGroupDir n A))) = helper
  where
  abstract
    helper : IsGroup {G = coHomRed n A} (0ₕ∙ n) (_+ₕ∙_ {n = n}) (-ₕ∙_ {n = n})
    helper = makeIsGroup § (assocₕ∙ n) (rUnitₕ∙ n) (lUnitₕ∙ n) (rCancelₕ∙ n) (lCancelₕ∙ n)
IsAbGroup.comm (AbGroupStr.isAbGroup (snd (coHomRedGroupDir n A))) = commₕ∙ n

coHomRedGrDir : (n : ℕ) (A : Pointed ℓ) → Group {ℓ}
coHomRedGrDir n A = AbGroup→Group (coHomRedGroupDir n A)

-- Induced map
coHomFun : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : ℕ) (f : A → B) → coHom n B → coHom n A
coHomFun n f = sRec § λ β → ∣ β ∘ f ∣₂

coHomMorph : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : ℕ) (f : A → B) → GroupHom (coHomGr n B) (coHomGr n A)
fun (coHomMorph n f) = coHomFun n f
isHom (coHomMorph zero f) = sElim2 (λ _ _ → isOfHLevelPath 2 § _ _) λ _ _ → refl
isHom (coHomMorph (suc zero) f) = sElim2 (λ _ _ → isOfHLevelPath 2 § _ _) λ _ _ → refl
isHom (coHomMorph (suc (suc n)) f) = sElim2 (λ _ _ → isOfHLevelPath 2 § _ _) λ _ _ → refl

-- Alternative definition of cohomology using ΩKₙ instead. Useful for breaking proofs of group isos
-- up into smaller parts
coHomGrΩ : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → Group {ℓ}
coHomGrΩ n A = ∥ (A → typ (Ω (coHomK-ptd (suc n)))) ∥₂ , coHomGrnA
  where
  coHomGrnA : GroupStr ∥ (A → typ (Ω (coHomK-ptd (suc n)))) ∥₂
  0g coHomGrnA = ∣ (λ _ → refl) ∣₂
  GroupStr._+_ coHomGrnA = sRec2 § λ p q → ∣ (λ x → p x ∙ q x) ∣₂
  - coHomGrnA = map λ f x → sym (f x)
  isGroup coHomGrnA = helper
    where
    abstract
      helper :
        IsGroup {G = ∥ (A → typ (Ω (coHomK-ptd (suc n)))) ∥₂}
          (∣ (λ _ → refl) ∣₂) (sRec2 § λ p q → ∣ (λ x → p x ∙ q x) ∣₂) (map λ f x → sym (f x))
      helper = makeIsGroup § (elim3 (λ _ _ _ → isOfHLevelPath 2 § _ _)
                                    (λ p q r → cong ∣_∣₂ (funExt λ x → assoc∙ (p x) (q x) (r x))))
                             (sElim (λ _ → isOfHLevelPath 2 § _ _) λ p → cong ∣_∣₂ (funExt λ x → sym (rUnit (p x))))
                             (sElim (λ _ → isOfHLevelPath 2 § _ _) λ p → cong ∣_∣₂ (funExt λ x → sym (lUnit (p x))))
                             (sElim (λ _ → isOfHLevelPath 2 § _ _) λ p → cong ∣_∣₂ (funExt λ x → rCancel (p x)))
                             (sElim (λ _ → isOfHLevelPath 2 § _ _) λ p → cong ∣_∣₂ (funExt λ x → lCancel (p x)))

--- the loopspace of Kₙ is commutative regardless of base
addIso : (n : ℕ) (x : coHomK n) → Iso (coHomK n) (coHomK n)
fun (addIso n x) y = y +[ n ]ₖ x
inv' (addIso n x) y = y -[ n ]ₖ x
rightInv (addIso n x) y = -+cancelₖ n y x
leftInv (addIso n x) y = -cancelRₖ n x y

isCommΩK-based : (n : ℕ) (x : coHomK n) → isComm∙ (coHomK n , x)
isCommΩK-based zero x p q = isSetInt _ _ (p ∙ q) (q ∙ p)
isCommΩK-based (suc zero) x =
  subst isComm∙ (λ i → coHomK 1 , lUnitₖ 1 x i)
                (ptdIso→comm {A = (_ , 0ₖ 1)} (addIso 1 x)
                              (isCommΩK 1))
isCommΩK-based (suc (suc n)) x =
  subst isComm∙ (λ i → coHomK (suc (suc n)) , lUnitₖ (suc (suc n)) x i)
                (ptdIso→comm {A = (_ , 0ₖ (suc (suc n)))} (addIso (suc (suc n)) x)
                              (isCommΩK (suc (suc n))))

-- hidden versions of cohom stuff using the "lock" hack. The locked versions can be used when proving things.
-- Swapping "key" for "tt*" will then give computing functions.
Unit' : Type₀
Unit' = lockUnit {ℓ-zero}

lock : ∀ {ℓ} {A : Type ℓ} → Unit' → A → A
lock unlock = λ x → x

module lockedCohom (key : Unit') where
  +K : (n : ℕ) → coHomK n → coHomK n → coHomK n
  +K n = lock key (_+ₖ_ {n = n})

  -K : (n : ℕ) → coHomK n → coHomK n
  -K n = lock key (-ₖ_ {n = n})

  -Kbin : (n : ℕ) → coHomK n → coHomK n → coHomK n
  -Kbin n x y = +K n x (-K n y)

  rUnitK : (n : ℕ) (x : coHomK n) → +K n x (0ₖ n) ≡ x
  rUnitK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x (0ₖ n) ≡ x
    pm unlock = rUnitₖ n x

  lUnitK : (n : ℕ) (x : coHomK n) → +K n (0ₖ n) x ≡ x
  lUnitK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (0ₖ n) x ≡ x
    pm unlock = lUnitₖ n x

  rCancelK : (n : ℕ) (x : coHomK n) → +K n x (-K n x) ≡ 0ₖ n
  rCancelK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x (lock t (-ₖ_ {n = n}) x) ≡ 0ₖ n
    pm unlock = rCancelₖ n x

  lCancelK : (n : ℕ) (x : coHomK n) → +K n (-K n x) x ≡ 0ₖ n
  lCancelK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (-ₖ_ {n = n}) x) x ≡ 0ₖ n
    pm unlock = lCancelₖ n x

  -cancelRK : (n : ℕ) (x y : coHomK n) → -Kbin n (+K n y x) x ≡ y
  -cancelRK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) y x) (lock t (-ₖ_ {n = n}) x) ≡ y
    pm unlock = -cancelRₖ n x y

  -cancelLK : (n : ℕ) (x y : coHomK n) → -Kbin n (+K n x y) x ≡ y
  -cancelLK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) x y) (lock t (-ₖ_ {n = n}) x) ≡ y
    pm unlock = -cancelLₖ n x y

  -+cancelK : (n : ℕ) (x y : coHomK n) → +K n (-Kbin n x y) y ≡ x
  -+cancelK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (_+ₖ_ {n = n})  x (lock t (-ₖ_ {n = n}) y)) y ≡ x
    pm unlock = -+cancelₖ n x y

  assocK : (n : ℕ) (x y z : coHomK n) → +K n x (+K n y z) ≡ +K n (+K n x y) z
  assocK n x y z = pm key
    where
    pm : (t : Unit') →  lock t (_+ₖ_ {n = n}) x (lock t (_+ₖ_ {n = n}) y z)
                       ≡ lock t (_+ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) x y) z
    pm unlock = assocₖ n x y z

  commK : (n : ℕ) (x y : coHomK n) → +K n x y ≡ +K n y x
  commK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x y ≡ lock t (_+ₖ_ {n = n}) y x
    pm unlock = commₖ n x y

  -- cohom

  +H : (n : ℕ) (x y : coHom n A) → coHom n A
  +H n = sRec2 § λ a b → ∣ (λ x → +K n (a x) (b x)) ∣₂

  -H : (n : ℕ) (x : coHom n A) → coHom n A
  -H n = sRec § λ a → ∣ (λ x → -K n (a x)) ∣₂

  -Hbin : (n : ℕ) → coHom n A → coHom n A → coHom n A
  -Hbin n = sRec2 § λ a b → ∣ (λ x → -Kbin n (a x) (b x)) ∣₂

  rUnitH : (n : ℕ) (x : coHom n A) → +H n x (0ₕ n) ≡ x
  rUnitH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                  λ a i → ∣ funExt (λ x → rUnitK n (a x)) i ∣₂

  lUnitH : (n : ℕ) (x : coHom n A) → +H n (0ₕ n) x ≡ x
  lUnitH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                    λ a i → ∣ funExt (λ x → lUnitK n (a x)) i ∣₂

  rCancelH : (n : ℕ) (x : coHom n A) → +H n x (-H n x) ≡ 0ₕ n
  rCancelH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                   λ a i → ∣ funExt (λ x → rCancelK n (a x)) i ∣₂

  lCancelH : (n : ℕ) (x : coHom n A) → +H n (-H n x) x  ≡ 0ₕ n
  lCancelH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                   λ a i → ∣ funExt (λ x → lCancelK n (a x)) i ∣₂

  assocH : (n : ℕ) (x y z : coHom n A) → (+H n x (+H n y z)) ≡ (+H n (+H n x y) z)
  assocH n = elim3 (λ _ _ _ → isOfHLevelPath 1 (§ _ _))
                 λ a b c i → ∣ funExt (λ x → assocK n (a x) (b x) (c x)) i ∣₂

  commH : (n : ℕ) (x y : coHom n A) → (+H n x y) ≡ (+H n y x)
  commH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                          λ a b i → ∣ funExt (λ x → commK n (a x) (b x)) i ∣₂

  -cancelRH : (n : ℕ) (x y : coHom n A) → -Hbin n (+H n y x) x ≡ y
  -cancelRH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -cancelRK n (a x) (b x) i) ∣₂

  -cancelLH : (n : ℕ) (x y : coHom n A) → -Hbin n (+H n x y) x ≡ y
  -cancelLH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -cancelLK n (a x) (b x) i) ∣₂

  -+cancelH : (n : ℕ) (x y : coHom n A) → +H n (-Hbin n x y) y ≡ x
  -+cancelH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -+cancelK n (a x) (b x) i) ∣₂

lUnitK≡rUnitK : (key : Unit') (n : ℕ) → lockedCohom.lUnitK key n (0ₖ n) ≡ lockedCohom.rUnitK key n (0ₖ n)
lUnitK≡rUnitK unlock = lUnitₖ≡rUnitₖ

open GroupIso renaming (map to grMap)
open GroupStr renaming (_+_ to _+gr_)
open GroupHom

inducedCoHom : ∀ {ℓ ℓ'} {A : Type ℓ} {G : Group {ℓ'}} {n : ℕ}
  → GroupIso (coHomGr n A) G
  → Group
inducedCoHom {A = A} {G = G} {n = n} e =
  InducedGroup (coHomGr n A)
               (coHom n A , λ x y → inv e (_+gr_ (snd G) (fun (grMap e) x)
                                                          (fun (grMap e) y)))
               (idEquiv _)
               λ x y → sym (leftInv e _)
                      ∙ cong (inv e) (isHom (grMap e) x y)

induced+ : ∀ {ℓ ℓ'} {A : Type ℓ} {G : Group {ℓ'}} {n : ℕ}
  → (e : GroupIso (coHomGr n A) G)
  → fst (inducedCoHom e) → fst (inducedCoHom e) → fst (inducedCoHom e)
induced+ e = _+gr_ (snd (inducedCoHom e))

inducedCoHomIso : ∀ {ℓ ℓ'} {A : Type ℓ} {G : Group {ℓ'}} {n : ℕ}
               → (e : GroupIso (coHomGr n A) G)
               → GroupIso (coHomGr n A) (inducedCoHom e)
fun (grMap (inducedCoHomIso e)) = idfun _
isHom (grMap (inducedCoHomIso e)) x y = sym (leftInv e _)
                                      ∙ cong (inv e) (isHom (grMap e) x y)
inv (inducedCoHomIso e) = idfun _
rightInv (inducedCoHomIso e) _ = refl
leftInv (inducedCoHomIso e) _ = refl

inducedCoHomPath : ∀ {ℓ ℓ'} {A : Type ℓ} {G : Group {ℓ'}} {n : ℕ}
               → (e : GroupIso (coHomGr n A) G)
               → coHomGr n A ≡ inducedCoHom e
inducedCoHomPath e = InducedGroupPath _ _ _ _

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Least common multiple
------------------------------------------------------------------------

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

module Data.Nat.LCM where

open import Algebra
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Nat.GCD
open import Data.Nat.Divisibility as Div
open import Data.Nat.Coprimality as Coprime
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)
open import Relation.Binary

open +-*-Solver

private
  module P  = Poset Div.poset

------------------------------------------------------------------------
-- Least common multiple (lcm).

module LCM where

  -- Specification of the least common multiple (lcm) of two natural
  -- numbers.

  record LCM (i j lcm : ℕ) : Set where
    field
      -- The lcm is a common multiple.
      commonMultiple : i ∣ lcm × j ∣ lcm

      -- The lcm divides all common multiples, i.e. the lcm is the least
      -- common multiple according to the partial order _∣_.
      least : ∀ {m} → i ∣ m × j ∣ m → lcm ∣ m

  open LCM public

  -- The lcm is unique.

  unique : ∀ {d₁ d₂ m n} → LCM m n d₁ → LCM m n d₂ → d₁ ≡ d₂
  unique d₁ d₂ = P.antisym (LCM.least d₁ (LCM.commonMultiple d₂))
                           (LCM.least d₂ (LCM.commonMultiple d₁))

open LCM public using (LCM) hiding (module LCM)

------------------------------------------------------------------------
-- Calculating the lcm

private
  lem₁ = solve 3 (λ a b c → a :* b :* c  :=  b :* (a :* c)) refl
  lem₂ = solve 3 (λ a b c → a :* b :* c  :=  a :* (b :* c)) refl

  -- If these lemmas are inlined, then type checking takes a lot
  -- longer... (In the development version of Agda from 2009-05-21.)

  mult₁ : ∀ q₁ q₂ d → q₁ * d ∣ q₁ * q₂ * d
  mult₁ q₁ q₂ d = divides q₂ (lem₁ q₁ q₂ d)

  mult₂ : ∀ q₁ q₂ d → q₂ * d ∣ q₁ * q₂ * d
  mult₂ q₁ q₂ d = divides q₁ (lem₂ q₁ q₂ d)

-- The lcm can be calculated from the gcd.

lcm : (i j : ℕ) → ∃ λ d → LCM i j d
lcm i j with gcd′ i j
lcm .(q₁ * d) .(q₂ * d) | (d , gcd-* q₁ q₂ q₁-q₂-coprime) =
  ( q₁ * q₂ * d
  , record { commonMultiple = (mult₁ q₁ q₂ d , mult₂ q₁ q₂ d)
           ; least          = least d
           }
  )
  where
  least : ∀ d {m} → q₁ * d ∣ m × q₂ * d ∣ m → q₁ * q₂ * d ∣ m
  least zero (divides q₃ refl , _) = begin
    q₁ * q₂ * 0    ∣⟨ (q₁ * q₂ * 0) ∣0 ⟩
    0              ≡⟨ solve 2 (λ a b → con 0  :=  a :* (b :* con 0))
                              refl q₃ q₁ ⟩
    q₃ * (q₁ * 0)  ∎
    where open ∣-Reasoning
  least (suc d) {m} (divides q₃ eq₃ , divides q₄ eq₄) =
    q₁q₂d′∣m q₃ eq₃ q₂∣q₃
    where
    open PropEq.≡-Reasoning
    d′ = suc d

    q₂∣q₃ : q₂ ∣ q₃
    q₂∣q₃ = coprime-divisor (Coprime.sym q₁-q₂-coprime)
              (divides q₄ $ *-cancelʳ-≡ _ _ (begin
                 q₁ * q₃ * d′    ≡⟨ lem₁ q₁ q₃ d′ ⟩
                 q₃ * (q₁ * d′)  ≡⟨ PropEq.sym eq₃ ⟩
                 m               ≡⟨ eq₄ ⟩
                 q₄ * (q₂ * d′)  ≡⟨ PropEq.sym (lem₂ q₄ q₂ d′) ⟩
                 q₄ *  q₂ * d′   ∎))

    q₁q₂d′∣m : ∀ q₃ → m ≡ q₃ * (q₁ * d′) → q₂ ∣ q₃ → q₁ * q₂ * d′ ∣ m
    q₁q₂d′∣m .(q₅ * q₂) eq₃′ (divides q₅ refl) =
      divides q₅ (begin
        m                    ≡⟨ eq₃′ ⟩
        q₅ * q₂ * (q₁ * d′)  ≡⟨ solve 4 (λ q₁ q₂ q₅ d′ → q₅ :* q₂ :* (q₁ :* d′)
                                                     :=  q₅ :* (q₁ :* q₂ :* d′))
                                        refl q₁ q₂ q₅ d′ ⟩
        q₅ * (q₁ * q₂ * d′)  ∎)

------------------------------------------------------------------------
-- Properties

-- The product of the gcd and the lcm is the product of the two
-- numbers.

gcd*lcm : ∀ {i j d m} → GCD i j d → LCM i j m → i * j ≡ d * m
gcd*lcm  {i}        {j}       {d}  {m}               g l with LCM.unique l (proj₂ (lcm i j))
gcd*lcm  {i}        {j}       {d} .{proj₁ (lcm i j)} g l | refl with gcd′ i j
gcd*lcm .{q₁ * d′} .{q₂ * d′} {d}                    g l | refl | (d′ , gcd-* q₁ q₂ q₁-q₂-coprime)
                                                           with GCD.unique g
                                                                  (gcd′-gcd (gcd-* q₁ q₂ q₁-q₂-coprime))
gcd*lcm .{q₁ * d}  .{q₂ * d}  {d}                    g l | refl | (.d , gcd-* q₁ q₂ q₁-q₂-coprime) | refl =
  solve 3 (λ q₁ q₂ d → q₁ :* d :* (q₂ :* d)
                   :=  d :* (q₁ :* q₂ :* d))
          refl q₁ q₂ d

ext: agda


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

module Agda.Builtin.Bool where

data Bool : Set where
  false true : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE  true  #-}

{-# COMPILED_DATA_UHC Bool __BOOL__ __FALSE__ __TRUE__ #-}

{-# COMPILED_JS Bool  function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
{-# COMPILED_JS false false #-}
{-# COMPILED_JS true  true  #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The identity monad
------------------------------------------------------------------------

module Category.Monad.Identity where

open import Category.Monad

Identity : ∀ {f} → Set f → Set f
Identity A = A

IdentityMonad : ∀ {f} → RawMonad (Identity {f})
IdentityMonad = record
  { return = λ x → x
  ; _>>=_  = λ x f → f x
  }


text:
module 842Inference where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.String using (String; _≟_)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)
import plfa.lambda.DeBruijn as DB

-- Syntax.

infix   4  _∋_⦂_
infix   4  _⊢_↑_
infix   4  _⊢_↓_
infixl  5  _,_⦂_

infixr  7  _⇒_

infix   5  ƛ_⇒_
infix   5  μ_⇒_
infix   6  _↑
infix   6  _↓_
infixl  7  _·_
infix   8  `suc_
infix   9  `_

Id : Set
Id = String

data Type : Set where
  `ℕ    : Type
  _⇒_   : Type → Type → Type

data Context : Set where
  ∅     : Context
  _,_⦂_ : Context → Id → Type → Context

data Term⁺ : Set
data Term⁻ : Set

data Term⁺ where
  `_                        : Id → Term⁺
  _·_                       : Term⁺ → Term⁻ → Term⁺
  _↓_                       : Term⁻ → Type → Term⁺

data Term⁻ where
  ƛ_⇒_                     : Id → Term⁻ → Term⁻
  `zero                    : Term⁻
  `suc_                    : Term⁻ → Term⁻
  `case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
  μ_⇒_                     : Id → Term⁻ → Term⁻
  _↑                       : Term⁺ → Term⁻

-- Examples of terms.

two : Term⁻
two = `suc (`suc `zero)

plus : Term⁺
plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
          `case (` "m") [zero⇒ ` "n" ↑
                        |suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
            ↓ (`ℕ ⇒ `ℕ ⇒ `ℕ)

2+2 : Term⁺
2+2 = plus · two · two
Ch : Type
Ch = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ

twoᶜ : Term⁻
twoᶜ = (ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · (` "z" ↑) ↑) ↑)

plusᶜ : Term⁺
plusᶜ = (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
           ` "m" · (` "s" ↑) · (` "n" · (` "s" ↑) · (` "z" ↑) ↑) ↑)
             ↓ (Ch ⇒ Ch ⇒ Ch)

sucᶜ : Term⁻
sucᶜ = ƛ "x" ⇒ `suc (` "x" ↑)

2+2ᶜ : Term⁺
2+2ᶜ = plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero

-- Lookup judgments.

data _∋_⦂_ : Context → Id → Type → Set where

  Z : ∀ {Γ x A}
      --------------------
    → Γ , x ⦂ A ∋ x ⦂ A

  S : ∀ {Γ x y A B}
    → x ≢ y
    → Γ ∋ x ⦂ A
      -----------------
    → Γ , y ⦂ B ∋ x ⦂ A

-- Synthesis and inheritance.

data _⊢_↑_ : Context → Term⁺ → Type → Set
data _⊢_↓_ : Context → Term⁻ → Type → Set

data _⊢_↑_ where

  ⊢` : ∀ {Γ A x}
    → Γ ∋ x ⦂ A
      -----------
    → Γ ⊢ ` x ↑ A

  _·_ : ∀ {Γ L M A B}
    → Γ ⊢ L ↑ A ⇒ B
    → Γ ⊢ M ↓ A
      -------------
    → Γ ⊢ L · M ↑ B

  ⊢↓ : ∀ {Γ M A}
    → Γ ⊢ M ↓ A
      ---------------
    → Γ ⊢ (M ↓ A) ↑ A

data _⊢_↓_ where

  ⊢ƛ : ∀ {Γ x N A B}
    → Γ , x ⦂ A ⊢ N ↓ B
      -------------------
    → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B

  ⊢zero : ∀ {Γ}
      --------------
    → Γ ⊢ `zero ↓ `ℕ

  ⊢suc : ∀ {Γ M}
    → Γ ⊢ M ↓ `ℕ
      ---------------
    → Γ ⊢ `suc M ↓ `ℕ

  ⊢case : ∀ {Γ L M x N A}
    → Γ ⊢ L ↑ `ℕ
    → Γ ⊢ M ↓ A
    → Γ , x ⦂ `ℕ ⊢ N ↓ A
      -------------------------------------
    → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A

  ⊢μ : ∀ {Γ x N A}
    → Γ , x ⦂ A ⊢ N ↓ A
      -----------------
    → Γ ⊢ μ x ⇒ N ↓ A

  ⊢↑ : ∀ {Γ M A B}
    → Γ ⊢ M ↑ A
    → A ≡ B
      -------------
    → Γ ⊢ (M ↑) ↓ B

-- PLFA exercise: write the term for multiplication (from Lambda)

-- PLFA exercise: extend the rules to support products (from More)

-- PLFA exercise (stretch): extend the rules to support the other
-- constructs from More

-- Equality of types.

_≟Tp_ : (A B : Type) → Dec (A ≡ B)
`ℕ      ≟Tp `ℕ              =  yes refl
`ℕ      ≟Tp (A ⇒ B)         =  no λ()
(A ⇒ B) ≟Tp `ℕ              =  no λ()
(A ⇒ B) ≟Tp (A′ ⇒ B′)
  with A ≟Tp A′ | B ≟Tp B′
...  | no A≢    | _         =  no λ{refl → A≢ refl}
...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
...  | yes refl | yes refl  =  yes refl

-- Helpers: domain and range of equal function types are equal,
-- `ℕ is not a function type.

dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
dom≡ refl = refl

rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
rng≡ refl = refl

ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
ℕ≢⇒ ()

-- Lookup judgments are unique.

uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
uniq-∋ Z Z                 =  refl
uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′

-- A synthesized type is unique.

uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl

-- Failed lookups still fail if a different binding is added.

ext∋ : ∀ {Γ B x y}
  → x ≢ y
  → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
    -----------------------------
  → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩

-- Decision procedure for lookup judgments.

lookup : ∀ (Γ : Context) (x : Id)
    -----------------------
  → Dec (∃[ A ](Γ ∋ x ⦂ A))
lookup ∅ x                        =  no  (λ ())
lookup (Γ , y ⦂ B) x with x ≟ y
... | yes refl                    =  yes ⟨ B , Z ⟩
... | no x≢y with lookup Γ x
...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩

-- Helpers for promoting a failure to type.

¬arg : ∀ {Γ A B L M}
  → Γ ⊢ L ↑ A ⇒ B
  → ¬ Γ ⊢ M ↓ A
    -------------------------
  → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′

¬switch : ∀ {Γ M A B}
  → Γ ⊢ M ↑ A
  → A ≢ B
    ---------------
  → ¬ Γ ⊢ (M ↑) ↓ B
¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B

-- Mutually-recursive synthesize and inherit functions.

synthesize : ∀ (Γ : Context) (M : Term⁺)
    -----------------------
  → Dec (∃[ A ](Γ ⊢ M ↑ A))

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
    ---------------
  → Dec (Γ ⊢ M ↓ A)

synthesize Γ (` x) with lookup Γ x
... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
synthesize Γ (L · M) with synthesize Γ L
... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩

inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢ƛ ⊢N)
inherit Γ `zero `ℕ          =  yes ⊢zero
inherit Γ `zero (A ⇒ B)     =  no  (λ())
inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
... | yes ⊢M                =  yes (⊢suc ⊢M)
inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })
... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
... | yes ⊢N                =  yes (⊢μ ⊢N)
inherit Γ (M ↑) B with synthesize Γ M
... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)

-- Copied from Lambda.

_≠_ : ∀ (x y : Id) → x ≢ y
x ≠ y  with x ≟ y
...       | no  x≢y  =  x≢y
...       | yes _    =  ⊥-elim impossible
  where postulate impossible : ⊥

-- Computed by evaluating 'synthesize ∅ 2+2' and editing.

⊢2+2 : ∅ ⊢ 2+2 ↑ `ℕ
⊢2+2 =
  (⊢↓
   (⊢μ
    (⊢ƛ
     (⊢ƛ
      (⊢case (⊢` (S (λ()) Z)) (⊢↑ (⊢` Z) refl)
       (⊢suc
        (⊢↑
         (⊢`
          (S (λ())
           (S (λ())
            (S (λ()) Z)))
          · ⊢↑ (⊢` Z) refl
          · ⊢↑ (⊢` (S (λ()) Z)) refl)
         refl))))))
   · ⊢suc (⊢suc ⊢zero)
   · ⊢suc (⊢suc ⊢zero))

-- Check that synthesis is correct (more below).

_ : synthesize ∅ 2+2 ≡ yes ⟨ `ℕ , ⊢2+2 ⟩
_ = refl

-- Example: 2+2 for Church numerals.

⊢2+2ᶜ : ∅ ⊢ 2+2ᶜ ↑ `ℕ
⊢2+2ᶜ =
  ⊢↓
  (⊢ƛ
   (⊢ƛ
    (⊢ƛ
     (⊢ƛ
      (⊢↑
       (⊢`
        (S (λ())
         (S (λ())
          (S (λ()) Z)))
        · ⊢↑ (⊢` (S (λ()) Z)) refl
        ·
        ⊢↑
        (⊢`
         (S (λ())
          (S (λ()) Z))
         · ⊢↑ (⊢` (S (λ()) Z)) refl
         · ⊢↑ (⊢` Z) refl)
        refl)
       refl)))))
  ·
  ⊢ƛ
  (⊢ƛ
   (⊢↑
    (⊢` (S (λ()) Z) ·
     ⊢↑ (⊢` (S (λ()) Z) · ⊢↑ (⊢` Z) refl)
     refl)
    refl))
  ·
  ⊢ƛ
  (⊢ƛ
   (⊢↑
    (⊢` (S (λ()) Z) ·
     ⊢↑ (⊢` (S (λ()) Z) · ⊢↑ (⊢` Z) refl)
     refl)
    refl))
  · ⊢ƛ (⊢suc (⊢↑ (⊢` Z) refl))
  · ⊢zero

_ : synthesize ∅ 2+2ᶜ ≡ yes ⟨ `ℕ , ⊢2+2ᶜ ⟩
_ = refl

-- Testing error cases.

_ : synthesize ∅ ((ƛ "x" ⇒ ` "y" ↑) ↓ (`ℕ ⇒ `ℕ)) ≡ no _
_ = refl

-- Bad argument type.

_ : synthesize ∅ (plus · sucᶜ) ≡ no _
_ = refl

-- Bad function types.

_ : synthesize ∅ (plus · sucᶜ · two) ≡ no _
_ = refl

_ : synthesize ∅ ((two ↓ `ℕ) · two) ≡ no _
_ = refl

_ : synthesize ∅ (twoᶜ ↓ `ℕ) ≡ no _
_ = refl

-- A natural can't have a function type.

_ : synthesize ∅ (`zero ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl

_ : synthesize ∅ (two ↓ `ℕ ⇒ `ℕ) ≡ no _
_ = refl

-- Can't hide a bad type.

_ : synthesize ∅ (`suc twoᶜ ↓ `ℕ) ≡ no _
_ = refl

-- Can't case on a function type.

_ : synthesize ∅
      ((`case (twoᶜ ↓ Ch) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl

-- Can't hide a bad type inside case.

_ : synthesize ∅
      ((`case (twoᶜ ↓ `ℕ) [zero⇒ `zero |suc "x" ⇒ ` "x" ↑ ] ↓ `ℕ) ) ≡ no _
_ = refl

-- Mismatch of inherited and synthesized types.

_ : synthesize ∅ (((ƛ "x" ⇒ ` "x" ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ))) ≡ no _
_ = refl

-- Erasure: Taking the evidence provided by synthesis on a decorated term
-- and producing the corresponding inherently-typed term.

-- Erasing a type.

∥_∥Tp : Type → DB.Type
∥ `ℕ ∥Tp             =  DB.`ℕ
∥ A ⇒ B ∥Tp          =  ∥ A ∥Tp DB.⇒ ∥ B ∥Tp

-- Erasing a context.

∥_∥Cx : Context → DB.Context
∥ ∅ ∥Cx              =  DB.∅
∥ Γ , x ⦂ A ∥Cx      =  ∥ Γ ∥Cx DB., ∥ A ∥Tp

-- Erasing a lookup judgment.

∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
∥ Z ∥∋               =  DB.Z
∥ S x≢ ⊢x ∥∋         =  DB.S ∥ ⊢x ∥∋

-- Mutually-recursive functions to erase typing judgments.

∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp

∥ ⊢` ⊢x ∥⁺           =  DB.` ∥ ⊢x ∥∋
∥ ⊢L · ⊢M ∥⁺         =  ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ ⊢↓ ⊢M ∥⁺           =  ∥ ⊢M ∥⁻

∥ ⊢ƛ ⊢N ∥⁻           =  DB.ƛ ∥ ⊢N ∥⁻
∥ ⊢zero ∥⁻           =  DB.`zero
∥ ⊢suc ⊢M ∥⁻         =  DB.`suc ∥ ⊢M ∥⁻
∥ ⊢case ⊢L ⊢M ⊢N ∥⁻  =  DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
∥ ⊢μ ⊢M ∥⁻           =  DB.μ ∥ ⊢M ∥⁻
∥ ⊢↑ ⊢M refl ∥⁻      =  ∥ ⊢M ∥⁺

-- Tests that erasure works.

_ : ∥ ⊢2+2 ∥⁺ ≡ DB.2+2
_ = refl

_ : ∥ ⊢2+2ᶜ ∥⁺ ≡ DB.2+2ᶜ
_ = refl

-- PLFA exercise: demonstrate that synthesis on your decorated multiplication
-- followed by erasure gives your inherently-typed multiplication.

-- PLFA exercise: extend the above to include products.

-- PLFA exercise (stretch): extend the above to include
-- the rest of the features added in More.

-- Additions by PR:

-- From Lambda, with type annotation added

data Term : Set where
  `_                      :  Id → Term
  ƛ_⇒_                    :  Id → Term → Term
  _·_                     :  Term → Term → Term
  `zero                   :  Term
  `suc_                   :  Term → Term
  `case_[zero⇒_|suc_⇒_]    :  Term → Term → Id → Term → Term
  μ_⇒_                    :  Id → Term → Term
  _⦂_                     :  Term → Type → Term

-- Mutually-recursive decorators.

decorate⁻ : Term → Term⁻
decorate⁺ : Term → Term⁺

decorate⁻ (` x) = ` x ↑
decorate⁻ (ƛ x ⇒ M) = ƛ x ⇒ decorate⁻ M
decorate⁻ (M · M₁) = (decorate⁺ M) · (decorate⁻ M₁) ↑
decorate⁻ `zero = `zero
decorate⁻ (`suc M) = `suc (decorate⁻ M)
decorate⁻ `case M [zero⇒ M₁ |suc x ⇒ M₂ ]
 = `case (decorate⁺ M) [zero⇒ (decorate⁻ M₁) |suc x ⇒ (decorate⁻ M₂) ]
decorate⁻ (μ x ⇒ M) = μ x ⇒ decorate⁻ M
decorate⁻ (M ⦂ x) = decorate⁻ M

decorate⁺ (` x) = ` x
decorate⁺ (ƛ x ⇒ M) = ⊥-elim impossible
 where postulate impossible : ⊥
decorate⁺ (M · M₁) = (decorate⁺ M) · (decorate⁻ M₁)
decorate⁺ `zero = ⊥-elim impossible
 where postulate impossible : ⊥
decorate⁺ (`suc M) = ⊥-elim impossible
 where postulate impossible : ⊥
decorate⁺ `case M [zero⇒ M₁ |suc x ⇒ M₂ ] = ⊥-elim impossible
 where postulate impossible : ⊥
decorate⁺ (μ x ⇒ M) = ⊥-elim impossible
 where postulate impossible : ⊥
decorate⁺ (M ⦂ x) = decorate⁻ M ↓ x

ltwo : Term
ltwo = `suc `suc `zero

lplus : Term
lplus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
          `case ` "m"
            [zero⇒ ` "n"
            |suc "m" ⇒ `suc (` "p" · ` "m" · ` "n") ])
         ⦂ (`ℕ ⇒ `ℕ ⇒ `ℕ)

l2+2 : Term
l2+2 = lplus · ltwo · ltwo

ltwoᶜ : Term
ltwoᶜ =  ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")

lplusᶜ : Term
lplusᶜ =  (ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒
         ` "m" · ` "s" · (` "n" · ` "s" · ` "z"))
         ⦂ (Ch ⇒ Ch ⇒ Ch)

lsucᶜ : Term
lsucᶜ = ƛ "x" ⇒ `suc (` "x")

l2+2ᶜ : Term
l2+2ᶜ = lplusᶜ · ltwoᶜ · ltwoᶜ · lsucᶜ · `zero

_ : decorate⁻ ltwo ≡ two
_ = refl

_ : decorate⁺ lplus ≡ plus
_ = refl

_ : decorate⁺ l2+2 ≡ 2+2
_ = refl

_ : decorate⁻ ltwoᶜ ≡ twoᶜ
_ = refl

_ : decorate⁺ lplusᶜ ≡ plusᶜ
_ = refl

_ : decorate⁻ lsucᶜ ≡ sucᶜ
_ = refl

_ : decorate⁺ l2+2ᶜ ≡ 2+2ᶜ
_ = refl

{-
  Unicode used in this chapter:

  ↓  U+2193:  DOWNWARDS ARROW (\d)
  ↑  U+2191:  UPWARDS ARROW (\u)
  ∥  U+2225:  PARALLEL TO (\||)

-}


text:
{-# OPTIONS --safe --without-K #-}
module Data.Fin.PigeonHole where

open import Data.Fin as Fin
open import Data.Fin.Properties
open import Data.Product hiding (swap)
open import Relation.Nullary
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; _≢_)
open import Function.Equality as Fun
open import Function.Injection renaming (_∘_ to _⟨∘⟩_)
open import Function.LeftInverse hiding (id ; _∘_ )
open import Function.Surjection  hiding (id ; _∘_ )
open import Function.Related
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥-elim; ⊥)

inj→≤ : ∀ {n m} → (Fin n ↣ Fin m) → n ℕ.≤ m
inj→≤ {n}{m} f = ℕ.≮⇒≥ (contra f)
  where
    inject≤I : ∀ {m n} → m ℕ.≤ n → (Fin m ↣ Fin n)
    inject≤I m≤n  = record {
                           to = PropEq.→-to-⟶ (λ i → inject≤ i m≤n )
                          ; injective = injective m≤n
                          }
            where
              injective : ∀ {n m} → (m≤n  : m ℕ.≤ n) → ∀ {i j} → inject≤ i m≤n ≡ inject≤ j m≤n → i ≡ j
              injective (ℕ.s≤s m≤n) {zero} {zero} PropEq.refl = PropEq.refl
              injective (ℕ.s≤s m≤n) {zero} {suc j} ()
              injective (ℕ.s≤s m≤n) {suc i} {zero} ()
              injective (ℕ.s≤s m≤n) {suc i} {suc j} feq = PropEq.cong suc (injective m≤n (suc-injective feq))

    contra₁ : ∀ {m} → (Fin (ℕ.suc m) ↣ Fin m) → ⊥
    contra₁ {m = ℕ.zero} f with Injection.to f ⟨$⟩ # 0
    contra₁ {ℕ.zero} f | ()
    contra₁ {m = ℕ.suc m} f = contra₁ h
      where
        k : Fin (ℕ.suc m)
        k = Injection.to f ⟨$⟩ # 0

        sucI : Fin (ℕ.suc m) ↣ Fin (ℕ.suc (ℕ.suc m))
        sucI = record {
               to = PropEq.→-to-⟶ suc
             ; injective = suc-injective
          }

        g : Fin (ℕ.suc m) ↣ Fin (ℕ.suc m)
        g = f ⟨∘⟩ sucI

        k≢g : ∀ (i : Fin (ℕ.suc m)) → k ≢ Injection.to g ⟨$⟩ i
        k≢g i = contraposition (Injection.injective f) λ ()
          where
            open import Relation.Nullary.Negation

        h : Fin (ℕ.suc m) ↣ Fin m
        h = record {
            to = PropEq.→-to-⟶ to
          ; injective = to-injective
          }
          where
            to : Fin (ℕ.suc m) → Fin m
            to i = punchOut (k≢g i)

            to-injective :  ∀ {i j} → to i ≡ to j → i ≡ j
            to-injective {i}{j} eq = Injection.injective g
              (punchOut-injective (k≢g i) (k≢g j) eq)

    contra : ∀ {n m} → (Fin n ↣ Fin m) → n ℕ.≯ m
    contra {ℕ.zero} {m} f ()
    contra {ℕ.suc n} {ℕ.zero} f n>m with Injection.to f ⟨$⟩ # 0
    contra {ℕ.suc n} {ℕ.zero} f n>m | ()
    contra {ℕ.suc n} {ℕ.suc m} f n>m = contra₁ (f ⟨∘⟩ inject≤I n>m)

FinRelated : ∀ {n m k} → Fin n ∼[ k ] Fin m → Set
FinRelated {n} {m} {implication} f = ⊤
FinRelated {n} {m} {reverse-implication} f = ⊤
FinRelated {n} {m} {equivalence} f = ⊤
FinRelated {n} {m} {injection} f = n ℕ.≤ m
FinRelated {n} {m} {reverse-injection} f = n ℕ.≥ m
FinRelated {n} {m} {left-inverse} f = n ℕ.≤ m
FinRelated {n} {m} {surjection} f = n ℕ.≥ m
FinRelated {n} {m} {bijection} f = n ≡ m

⇒Fin∼Fin : ∀ {n m k} (f : Fin n ∼[ k ] Fin m) → FinRelated f
⇒Fin∼Fin {n} {m} {implication} f = tt
⇒Fin∼Fin {n} {m} {reverse-implication} f = tt
⇒Fin∼Fin {n} {m} {equivalence} f = tt
⇒Fin∼Fin {n} {m} {injection} f = inj→≤ f
⇒Fin∼Fin {n} {m} {reverse-injection} f = inj→≤ (app-↢ f)
⇒Fin∼Fin {n} {m} {left-inverse} f = inj→≤ (LeftInverse.injection f)
⇒Fin∼Fin {n} {m} {surjection} f = inj→≤ (Surjection.injection f)
⇒Fin∼Fin {n} {m} {bijection} f = ℕ.≤-antisym (inj→≤ (↔⇒ f))
                                             (inj→≤ (app-↢ (↔⇒ f)))

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


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

module h-Universe where

open import Basic_Types

record 𝓤 : Set₁ where
  field
    El : ∀ (X : Set) → Set


text:
{-# OPTIONS --no-positivity-check #-}

module Functor where

import Sets

open Sets

infixr 40 _+_ _+₂_
infixr 60 _×_ _×₂_
infix  80 _[_]

data U : Set1 where
  K   : Set -> U
  Id  : U
  _+_ : U -> U -> U
  _×_ : U -> U -> U

data U₂ : Set1 where
  K₂   : (A : Set) -> U₂
  ↖    : U -> U₂
  ↗    : U -> U₂
  _+₂_ : U₂ -> U₂ -> U₂
  _×₂_ : U₂ -> U₂ -> U₂

-- Functor composition
_[_] : U -> U -> U
K A	[ H ] = K A
Id	[ H ] = H
(F + G) [ H ] = F [ H ] + G [ H ]
(F × G) [ H ] = F [ H ] × G [ H ]

module Semantics where

  -- The semantic of a functor
  ⟦_⟧ : U -> Set -> Set
  ⟦ K A	  ⟧ X = A
  ⟦ Id	  ⟧ X = X
  ⟦ F + G ⟧ X = ⟦ F ⟧ X [+] ⟦ G ⟧ X
  ⟦ F × G ⟧ X = ⟦ F ⟧ X [×] ⟦ G ⟧ X

  ⟦_⟧₂ : (F : U₂) -> Set -> Set -> Set
  ⟦ K₂ A   ⟧₂ C J = A
  ⟦ ↖ F	   ⟧₂ C J = ⟦ F ⟧ C
  ⟦ ↗ F	   ⟧₂ C J = ⟦ F ⟧ J
  ⟦ F +₂ G ⟧₂ C J = ⟦ F ⟧₂ C J [+] ⟦ G ⟧₂ C J
  ⟦ F ×₂ G ⟧₂ C J = ⟦ F ⟧₂ C J [×] ⟦ G ⟧₂ C J

module Recursive where

  -- Fixed points (we need to turn off positivity checking since we can't see
  -- that ⟦ F ⟧ is covariant).

  open Semantics

  data μ (F : U) : Set where
    inn : ⟦ F ⟧ (μ F) -> μ F

  out : {F : U} -> μ F -> ⟦ F ⟧ (μ F)
  out (inn f) = f

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module PiLevelm2 where

open import PiU using (U)

------------------------------------------------------------------------------
-- We define a trivial relation on finite types that identifies all
-- types; this effectively makes U a contractible (-2)-type, i.e., a
-- singleton

data _⟷_ : U → U → Set where
  collapse : {t₁ t₂ : U} → t₁ ⟷ t₂

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{- Type class for adjoint functors -}
module CategoryTheory.Adjunction where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import CategoryTheory.Comonad

-- Adjunction between two functors
record _⊣_ {n} {ℂ 𝔻 : Category n} (F : Functor ℂ 𝔻) (G : Functor 𝔻 ℂ) : Set (lsuc n) where
    private module ℂ = Category ℂ
    private module 𝔻 = Category 𝔻
    private module F = Functor F
    private module G = Functor G
    field
        -- || Definitions
        -- Unit
        η : I ⟹ G ◯ F
        -- Counit
        ε : F ◯ G ⟹ I

    private module η = _⟹_ η
    private module ε = _⟹_ ε

    -- | Isomorphism of homsets
    ϕ : ∀{A : ℂ.obj} {B : 𝔻.obj} -> (F.omap A 𝔻.~> B) -> (A ℂ.~> G.omap B)
    ϕ {A} f = G.fmap f ℂ.∘ η.at A

    ϕ⁻ : ∀{B : 𝔻.obj} {A : ℂ.obj} -> (A ℂ.~> G.omap B) -> (F.omap A 𝔻.~> B)
    ϕ⁻ {B} f = ε.at B 𝔻.∘ F.fmap f

    field
        -- || Laws
        -- First triangle identity: εF ∘ Fη = ιd
        tri1 : ∀ {A : ℂ.obj} -> ε.at (F.omap A) 𝔻.∘ F.fmap (η.at A) 𝔻.≈ 𝔻.id
        -- Second triangle inequality: Gε ∘ ηG = ιd
        tri2 : ∀ {B : 𝔻.obj} -> G.fmap (ε.at B) ℂ.∘ η.at (G.omap B) ℂ.≈ ℂ.id

-- || An adjunction induces a monad and a comonad
AdjMonad : ∀ {n} {ℂ 𝔻 : Category n} {F : Functor ℂ 𝔻} {G : Functor 𝔻 ℂ}
    -> F ⊣ G -> Monad ℂ
AdjMonad {n} {ℂ} {𝔻} {F} {G} adj = record
    { T = G ◯ F
    ; η = F⊣G.η
    ; μ = record
        { at = λ A → G.fmap (at F⊣G.ε (F.omap A))
        ; nat-cond = G.fmap-∘ [sym] ≈> G.fmap-cong (nat-cond F⊣G.ε) ≈> G.fmap-∘
        }
    ; η-unit1 = F⊣G.tri2
    ; η-unit2 = G.fmap-∘ [sym] ≈> G.fmap-cong (F⊣G.tri1) ≈> G.fmap-id
    ; μ-assoc = G.fmap-∘ [sym] ≈> G.fmap-cong (nat-cond F⊣G.ε) ≈> G.fmap-∘
    }
    where
    private module F⊣G = _⊣_ adj
    open Category ℂ
    private module 𝔻 = Category 𝔻
    private module F = Functor F
    private module G = Functor G
    open _⟹_

AdjComonad : ∀ {n} {ℂ 𝔻 : Category n} {F : Functor ℂ 𝔻} {G : Functor 𝔻 ℂ}
    -> F ⊣ G -> Comonad 𝔻
AdjComonad {n} {ℂ} {𝔻} {F} {G} adj = record
    { W = F ◯ G
    ; ε = F⊣G.ε
    ; δ = record
        { at = λ A → F.fmap (at F⊣G.η (G.omap A))
        ; nat-cond = F.fmap-∘ [sym] ≈> F.fmap-cong (nat-cond F⊣G.η) ≈> F.fmap-∘
        }
    ; ε-unit1 = F⊣G.tri1
    ; ε-unit2 = F.fmap-∘ [sym] ≈> F.fmap-cong (F⊣G.tri2) ≈> F.fmap-id
    ; δ-assoc = F.fmap-∘ [sym] ≈> F.fmap-cong ((nat-cond F⊣G.η) ℂ.[sym]) ≈> F.fmap-∘
    }
    where
    private module F⊣G = _⊣_ adj
    open Category 𝔻
    private module ℂ = Category ℂ
    private module F = Functor F
    private module G = Functor G
    open _⟹_

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
open import guarded-recursion.prelude
open import guarded-recursion.model

-- Agda^{ω}^{op}
module guarded-recursion.model.Agda where

  open Presheaf
            Type
            -→-
            id
            _∘′_
            idp
            idp
            idp
            𝟙
            _
            idp
         public
  open WithProducts
            _×_
            fst
            snd
            <_,_>
            idp
            idp
            idp
         public
  open Str1 ℕ
         public
  open WithMore
            𝟘
            𝟘-elim
            𝟘-elim-uniq!
            _⊎_
            inl
            inr
            [_,_]
            idp
            idp
            [,]-uniq!
         public

  <_>ᵖ : ∀ {A : Type} → A → 𝟙ᵖ →ᵖ [ A ]ᵖ
  < x >ᵖ = (λ _ _ → x) , (λ _ → idp)

  42s : 𝟙ᵖ →ᵖ Strᵖ
  42s = repeatᵖ < 42 >ᵖ

  test : ℕ × ℕ × ℕ × ℕ × 𝟙
  test = fst 42s 3 _

  test-test : test ≡ (42 , 42 , 42 , 42 , _)
  test-test = idp
  -- -}
  -- -}
  -- -}
  -- -}
  -- -}

max_stars_repo_name: np/guarded-recursion

max_issues_repo_name: np/guarded-recursion

max_forks_repo_name: np/guarded-recursion


text:
{-

Definition of what it means to be a notion of relational structure

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.RelationalStructure where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.HITs.SetQuotients
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.ZigZag.Base

open isEquivRel
open isQuasiEquivRel

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

-- A notion of structured relation for a structure S assigns a relation on S X and S Y to every relation on X
-- and Y. We require the output to be proposition-valued when the input is proposition-valued.
StrRel : (S : Type ℓ → Type ℓ') (ℓ'' : Level) → Type (ℓ-max (ℓ-suc (ℓ-max ℓ ℓ'')) ℓ')
StrRel {ℓ = ℓ} S ℓ'' = ∀ {A B} (R : Rel A B ℓ) → Rel (S A) (S B) ℓ''

-- Given a type A and relation R, a quotient structure is a structure on the set quotient A/R such that
-- the graph of [_] : A → A/R is a structured relation
InducedQuotientStr : (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'')
  (A : TypeWithStr ℓ S) (R : Rel (typ A) (typ A) ℓ)
  → Type (ℓ-max ℓ' ℓ'')
InducedQuotientStr S ρ A R =
  Σ[ s ∈ S (typ A / R) ] ρ (graphRel [_]) (A .snd) s

-- A structured equivalence relation R on a structured type A should induce a structure on A/R
InducesQuotientStr : (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'') → Type _
InducesQuotientStr {ℓ = ℓ} S ρ =
  (A : TypeWithStr ℓ S) (R : EquivPropRel (typ A) ℓ)
  → ρ (R .fst .fst) (A .snd) (A .snd)
  → ∃![ s ∈ S (typ A / R .fst .fst) ] ρ (graphRel [_]) (A .snd) s

-- The identity should be a structured relation
isReflexiveStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isReflexiveStrRel {ℓ = ℓ} {S = S} ρ =
  {X : Type ℓ} → (s : S X) → ρ (idPropRel X .fst) s s

-- The inverse of a structured relation should be structured
isSymmetricStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isSymmetricStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y : Type ℓ} (R : PropRel X Y ℓ)
  {sx : S X} {sy : S Y}
  → ρ (R .fst) sx sy
  → ρ (invPropRel R .fst) sy sx

-- The composite of structured relations should be structured
isTransitiveStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isTransitiveStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y Z : Type ℓ}
  (R : PropRel X Y ℓ) (R' : PropRel Y Z ℓ)
  {sx : S X} {sy : S Y} {sz : S Z}
  → ρ (R .fst) sx sy
  → ρ (R' .fst) sy sz
  → ρ (compPropRel R R' .fst) sx sz

-- The type of structures on a set should be a set
preservesSetsStr : (S : Type ℓ → Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ')
preservesSetsStr S = ∀ {X} → isSet X → isSet (S X)

-- The type of structures on a prop-valued relation should be a prop
preservesPropsStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
preservesPropsStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y : Type ℓ} {R : Rel X Y ℓ}
  → (∀ x y → isProp (R x y))
  → (sx : S X) (sy : S Y)
  → isProp (ρ R sx sy)

record SuitableStrRel (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'') : Type (ℓ-max (ℓ-max (ℓ-suc ℓ) ℓ') ℓ'')
  where
  field
    quo : InducesQuotientStr S ρ
    symmetric : isSymmetricStrRel ρ
    transitive : isTransitiveStrRel ρ
    set : preservesSetsStr S
    prop : preservesPropsStrRel ρ

open SuitableStrRel public

quotientPropRel : ∀ {ℓ} {A : Type ℓ} (R : Rel A A ℓ) → PropRel A (A / R) ℓ
quotientPropRel R .fst a t = [ a ] ≡ t
quotientPropRel R .snd _ _ = squash/ _ _

-- We can also ask for a notion of structured relations to agree with some notion of structured equivalences.

StrRelMatchesEquiv : {S : Type ℓ → Type ℓ'}
  → StrRel S ℓ'' → StrEquiv S ℓ''' → Type _
StrRelMatchesEquiv {S = S} ρ ι =
  (A B : TypeWithStr _ S) (e : typ A ≃ typ B) →
  ρ (graphRel (e .fst)) (A .snd) (B .snd) ≃ ι A B e

-- Additional conditions for a "positive" notion of structured relation

isDetransitiveStrRel : {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'') → Type _
isDetransitiveStrRel {ℓ = ℓ} {S = S} ρ =
  {X Y Z : Type ℓ}
  (R : PropRel X Y ℓ) (R' : PropRel Y Z ℓ)
  {sx : S X} {sz : S Z}
  → ρ (compPropRel R R' .fst) sx sz
  → ∃[ sy ∈ S Y ] ρ (R .fst) sx sy × ρ (R' .fst) sy sz

record StrRelAction {S : Type ℓ → Type ℓ'} (ρ : StrRel S ℓ'')
  : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓ' ℓ''))
  where
  field
    actStr : ∀ {X Y} → (X → Y) → S X → S Y
    actStrId : ∀ {X} (s : S X) → actStr (idfun X) s ≡ s
    actRel : ∀ {X₀ Y₀ X₁ Y₁} {f : X₀ → X₁} {g : Y₀ → Y₁}
      {R₀ : X₀ → Y₀ → Type ℓ} {R₁ : X₁ → Y₁ → Type ℓ}
      → (∀ x y → R₀ x y → R₁ (f x) (g y))
      → ∀ sx sy → ρ R₀ sx sy → ρ R₁ (actStr f sx) (actStr g sy)

open StrRelAction public

strRelQuotientComparison : {S : Type ℓ → Type ℓ'} {ρ : StrRel S ℓ''}
  (θ : SuitableStrRel S ρ) (α : StrRelAction ρ)
  {X : Type ℓ} (R : EquivPropRel X ℓ)
  → (S X / ρ (R .fst .fst)) → S (X / R .fst .fst)
strRelQuotientComparison θ α R [ s ] = α .actStr [_] s
strRelQuotientComparison {ρ = ρ} θ α R (eq/ s t r i) =
  (sym leftEq ∙ rightEq) i
  where
  ρs : ρ (R .fst .fst) s s
  ρs =
    subst (λ R' → ρ R' s s)
      (funExt₂ λ x x' →
        hPropExt squash (R .fst .snd x x')
          (Trunc.rec (R .fst .snd x x')
            (λ {(_ , r , r') → R .snd .transitive _ _ _ r (R .snd .symmetric _ _ r')}))
          (λ r → ∣ x' , r , R .snd .reflexive x' ∣))
      (θ .transitive (R .fst) (invPropRel (R .fst)) r (θ .symmetric (R .fst) r))

  leftEq : θ .quo (_ , s) R ρs .fst .fst ≡ α .actStr [_] s
  leftEq =
    cong fst
      (θ .quo (_ , s) R ρs .snd
        ( α .actStr [_] s
        , subst
          (λ s' → ρ (graphRel [_]) s' (α .actStr [_] s))
          (α .actStrId s)
          (α .actRel eq/ s s ρs)
        ))

  rightEq : θ .quo (_ , s) R ρs .fst .fst ≡ α .actStr [_] t
  rightEq =
    cong fst
      (θ .quo (_ , s) R ρs .snd
        ( α .actStr [_] t
        , subst
          (λ s' → ρ (graphRel [_]) s' (α .actStr [_] t))
          (α .actStrId s)
          (α .actRel eq/ s t r)
        ))
strRelQuotientComparison θ α R (squash/ _ _ p q i j) =
  θ .set squash/ _ _
    (cong (strRelQuotientComparison θ α R) p)
    (cong (strRelQuotientComparison θ α R) q)
    i j

record PositiveStrRel {S : Type ℓ → Type ℓ'} {ρ : StrRel S ℓ''} (θ : SuitableStrRel S ρ)
  : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓ' ℓ''))
  where
  field
    act : StrRelAction ρ
    reflexive : isReflexiveStrRel ρ
    detransitive : isDetransitiveStrRel ρ
    quo : {X : Type ℓ} (R : EquivPropRel X ℓ) → isEquiv (strRelQuotientComparison θ act R)

open PositiveStrRel public

posRelReflexive : {S : Type ℓ → Type ℓ'} {ρ : StrRel S ℓ''} {θ : SuitableStrRel S ρ}
  → PositiveStrRel θ
  → {X : Type ℓ} (R : EquivPropRel X ℓ)
  → (s : S X) → ρ (R .fst .fst) s s
posRelReflexive {ρ = ρ} σ R s =
  subst
    (uncurry (ρ (R .fst .fst)))
    (ΣPathP (σ .act .actStrId s , σ .act .actStrId s))
    (σ .act .actRel
      (λ x y →
        Trunc.rec (R .fst .snd _ _)
          (λ p → subst (R .fst .fst x) p (R .snd .reflexive x)))
      s s
      (σ .reflexive s))

-- Given a suitable notion of structured relation, if we have a structured quasi equivalence relation R
-- between structured types A and B, we get induced structures on the quotients A/(R ∙ R⁻¹) and B/(R⁻¹ ∙ R),
-- and the induced equivalence e : A/(R ∙ R⁻¹) ≃ B/(R⁻¹ ∙ R) is structured with respect to those quotient
-- structures.

record QERDescends (S : Type ℓ → Type ℓ') (ρ : StrRel S ℓ'')
  (A B : TypeWithStr ℓ S) (R : QuasiEquivRel (typ A) (typ B) ℓ) : Type (ℓ-max ℓ' ℓ'')
  where
  private
    module E = QER→Equiv R

  field
    quoᴸ : InducedQuotientStr S ρ A E.Rᴸ
    quoᴿ : InducedQuotientStr S ρ B E.Rᴿ
    rel : ρ (graphRel (E.Thm .fst)) (quoᴸ .fst) (quoᴿ .fst)

open QERDescends

structuredQER→structuredEquiv : {S : Type ℓ → Type ℓ'} {ρ : StrRel S ℓ''}
  (θ : SuitableStrRel S ρ)
  (A B : TypeWithStr ℓ S) (R : QuasiEquivRel (typ A) (typ B) ℓ)
  → ρ (R .fst .fst) (A .snd) (B .snd)
  → QERDescends S ρ A B R
structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴸ =
  θ .quo (X , s) (QER→EquivRel R)
    (θ .transitive (R .fst) (invPropRel (R .fst)) r (θ .symmetric (R .fst) r))
    .fst

structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴿ =
  θ .quo (Y , t) (QER→EquivRel (invQER R))
    (θ .transitive (invPropRel (R .fst)) (R .fst) (θ .symmetric (R .fst) r) r)
    .fst

structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .rel =
  subst (λ R' → ρ R' (quol .fst) (quor .fst)) correction
    (θ .transitive (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)
      (θ .transitive (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)
        (θ .symmetric (quotientPropRel E.Rᴸ) (quol .snd))
        r)
      (quor .snd))
  where
  module E = QER→Equiv R
  quol = structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴸ
  quor = structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴿ
  [R] = compPropRel (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)

  correction : [R] .fst ≡ graphRel (E.Thm .fst)
  correction =
    funExt₂ λ qx qy →
      (hPropExt squash (squash/ _ _)
        (Trunc.rec (squash/ _ _)
          (λ {(y , qr , py) →
            Trunc.rec
              (squash/ _ _)
              (λ {(x , px , r) →
                (cong (E.Thm .fst) (sym px)
                ∙ E.relToFwd≡ r)
                ∙ py})
              qr}))
        (elimProp {B = λ qx → E.Thm .fst qx ≡ qy → [R] .fst qx qy}
          (λ _ → isPropΠ λ _ → squash)
          (λ x →
            elimProp {B = λ qy → E.Thm .fst [ x ] ≡ qy → [R] .fst [ x ] qy}
              (λ _ → isPropΠ λ _ → squash)
              (λ y p → ∣ _ , ∣ _ , refl , E.fwd≡ToRel p ∣ , refl ∣)
              qy)
          qx))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}
module _ where

open import Common.Prelude
open import Common.Equality

foo : 0 ≡ 0
foo = refl

error : (x : 1 ≡ 1) → x ≡ refl
error x with foo
error x | y = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module BBHeap.Heap {A : Set}(_≤_ : A → A → Set)  where

open import BBHeap _≤_
open import BHeap _≤_ renaming (forget to forget')
open import BHeap.Heap _≤_
open import BTree.Heap _≤_
open import Bound.Lower A
open import Relation.Binary.PropositionalEquality

lemma-forget-forget' : {b : Bound}(h : BBHeap b) → forget h ≡ forget' (relax h)
lemma-forget-forget' leaf = refl
lemma-forget-forget' (left {l = l} {r = r} _ _) rewrite lemma-forget-forget' l | lemma-forget-forget' r = refl
lemma-forget-forget' (right {l = l} {r = r} _ _) rewrite lemma-forget-forget' l | lemma-forget-forget' r = refl

lemma-bbheap-heap : {b : Bound}(h : BBHeap b) → Heap (forget h)
lemma-bbheap-heap h rewrite lemma-forget-forget' h = lemma-bheap-heap (relax h)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue473 where

record _×_ A B : Set where
  constructor _,_
  field
    fst : A
    snd : B

open _×_

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Zero : Nat → Set where
  zero : Zero zero

data Zero₂ : Nat → Nat → Set where
  zero : Zero₂ zero zero

f₁ : (p : Nat × Nat) → Zero₂ (fst p) (snd p) → Set
f₁ (.zero , .zero) zero = Nat    -- works
-- f₁ .(zero , zero) zero = Nat  -- fails

f₂ : (p : Nat × Nat) → Zero (fst p) → Set
f₂ (.zero , y) zero = Nat  -- works
-- foo .?? zero             -- fails (nothing to write in place of ??)

f₃ : {p : Nat × Nat} → Zero (fst p) → Set
f₃ zero = Nat

f₄ : {p : Nat × (Nat × Nat)} → Zero (fst (snd p)) → Set
f₄ zero = Nat

f₅ : {p : Nat × Nat} → Zero₂ (fst p) (snd p) → Set
f₅ zero = Nat

data I : Set where
  i : I

record Box (A B : Set) : Set where
  constructor [_]
  field contents : A

data D : Set → Set₁ where
  d₁ : (R : Set) → D R
  d₂ : (i : I) (R : I → Set) → D (R i) → D (Box I (R i))

data S : (R : Set) → R → D R → Set₁ where
  s : (j : I) (R : I → Set) (p : D (R j)) →
      S (Box I (R j)) [ j ] (d₂ j R p)

postulate
  P : I → Set

WorksNow : {e : Box I (P i)} → S (Box I (P i)) e (d₂ i P (d₁ (P i))) → Set₁
WorksNow (s .i .P .(d₁ (P i))) = Set

-- No constructor
record Pair A B : Set where
  field
    first  : A
    second : B

open Pair

postulate
  T : {A B : Set} → A → B → Set
  mkT : ∀ {A B} (x : A)(y : B) → T x y

-- p is expanded even though it has no named constructor
bar : ∀ {A B} {p : Pair A B} → T (first p) (second p)
bar = mkT _ _


text:
------------------------------------------------------------------------
-- The All predicate, defined recursively
------------------------------------------------------------------------

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

open import Equality

module List.All.Recursive
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bag-equivalence eq hiding (module Dec)
open import Bijection eq as Bijection using (_↔_)
open import Equality.Decision-procedures eq
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import List eq as L using (_++_)
import List.All eq as A
open import Monad eq hiding (map)
import Nat eq as Nat
open import Surjection eq using (_↠_)
open import Tactic.By.Parametrised eq
open import Vec eq as Vec using (Vec)

private
  variable
    a ℓ p q : Level
    A B     : Type a
    f       : A → B
    P       : A → Type p
    Q       : A → Type q
    x y     : A
    xs ys   : List A
    n       : ℕ

-- All P xs means that P holds for every element of xs.

All : (A → Type p) → List A → Type p
All P []       = ↑ _ ⊤
All P (x ∷ xs) = P x × All P xs

-- The type xs ⊆ ys means that every element of xs is also an element
-- of ys.

infix 4 _⊆_

_⊆_ : {A : Type a} → List A → List A → Type a
xs ⊆ ys = All (_∈ ys) xs

-- If All P xs holds and x is an element of xs, then P x holds.

index : All P xs → x ∈ xs → P x
index {P = P} {xs = _ ∷ _} (p , _)  (inj₁ eq) = subst P (sym eq) p
index         {xs = _ ∷ _} (_ , ps) (inj₂ q)  = index ps q

-- If P holds for every element of xs, then All P xs holds.

tabulate : (∀ {x} → x ∈ xs → P x) → All P xs
tabulate {xs = []}    _ = _
tabulate {xs = _ ∷ _} f = f (inj₁ (refl _)) , tabulate (f ∘ inj₂)

-- Some synonyms.

cons : P x → All P xs → All P (x ∷ xs)
cons = _,_

head : All P (x ∷ xs) → P x
head = proj₁

tail : All P (x ∷ xs) → All P xs
tail = proj₂

-- All can be expressed using List and ∃.

∃-All↔List-∃ : (∃ λ xs → All P xs) ↔ List (∃ P)
∃-All↔List-∃ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : (∃ λ xs → All P xs) → List (∃ P)
  to ([]     , _)      = []
  to (x ∷ xs , p , ps) = (x , p) ∷ to (xs , ps)

  from : List (∃ P) → (∃ λ xs → All P xs)
  from []              = [] , _
  from ((x , p) ∷ xps) = Σ-map (x ∷_) (p ,_) (from xps)

  to∘from : ∀ xps → to (from xps) ≡ xps
  to∘from []         = refl _
  to∘from (xp ∷ xps) = cong (xp ∷_) (to∘from xps)

  from∘to : ∀ xsps → from (to xsps) ≡ xsps
  from∘to ([]     , _)      = refl _
  from∘to (x ∷ xs , p , ps) =
    cong (Σ-map (x ∷_) (p ,_)) (from∘to (xs , ps))

-- Some rearrangement lemmas.

All-[] : (P : A → Type p) → All P [] ↔ ⊤
All-[] P =
  All P []  ↔⟨⟩
  ↑ _ ⊤     ↝⟨ Bijection.↑↔ ⟩□
  ⊤         □

All-∷ : All P (x ∷ xs) ↔ P x × All P xs
All-∷ = F.id

All-++ : All P (xs ++ ys) ↔ All P xs × All P ys
All-++ {P = P} {xs = []} {ys = ys} =
  All P ys             ↝⟨ inverse $ drop-⊤-left-× (λ _ → All-[] P) ⟩□
  All P [] × All P ys  □
All-++ {P = P} {xs = x ∷ xs} {ys = ys} =
  P x × All P (xs ++ ys)       ↝⟨ F.id ×-cong All-++ ⟩
  P x × All P xs × All P ys    ↝⟨ ×-assoc ⟩□
  (P x × All P xs) × All P ys  □

All-map : All P (L.map f xs) ↔ All (P ∘ f) xs
All-map                 {xs = []}     = F.id
All-map {P = P} {f = f} {xs = x ∷ xs} =
  P (f x) × All P (L.map f xs)  ↝⟨ (∃-cong λ _ → All-map) ⟩□
  P (f x) × All (P ∘ f) xs      □

All-concat : All P (L.concat xs) ↔ All (All P) xs
All-concat         {xs = []}       = F.id
All-concat {P = P} {xs = xs ∷ xss} =
  All P (xs ++ L.concat xss)       ↝⟨ All-++ ⟩
  All P xs × All P (L.concat xss)  ↝⟨ (∃-cong λ _ → All-concat) ⟩□
  All P xs × All (All P) xss       □

All->>= :
  {A : Type ℓ} {f : A → List B} {xs : List A} →
  All P (xs >>= f) ↔ All (All P ∘ f) xs
All->>= {P = P} {f = f} {xs = xs} =
  All P (L.concat (L.map f xs))  ↝⟨ All-concat ⟩
  All (All P) (L.map f xs)       ↝⟨ All-map ⟩□
  All (All P ∘ f) xs             □

All-const : All (const A) xs ↔ Vec A (L.length xs)
All-const         {xs = []}     = F.id
All-const {A = A} {xs = x ∷ xs} =
  A × All (const A) xs     ↝⟨ (∃-cong λ _ → All-const) ⟩□
  A × Vec A (L.length xs)  □

All-const-replicate : All (const A) (L.replicate n tt) ↔ Vec A n
All-const-replicate         {n = zero}  = F.id
All-const-replicate {A = A} {n = suc n} =
  A × All (const A) (L.replicate n tt)  ↝⟨ (∃-cong λ _ → All-const-replicate) ⟩□
  A × Vec A n                           □

All-Σ :
  {A : Type a} {P : A → Type p} {Q : ∃ P → Type q} {xs : List A} →
  All (λ x → Σ (P x) (curry Q x)) xs ↔
  ∃ λ (ps : All P xs) → All Q (_↔_.to ∃-All↔List-∃ (xs , ps))
All-Σ {P = P} {Q = Q} {xs = []} =
  All (λ x → Σ (P x) (curry Q x)) []                             ↔⟨⟩
  ↑ _ ⊤                                                          ↝⟨ Bijection.↑↔ ⟩
  ⊤                                                              ↝⟨ inverse Bijection.↑↔ ⟩
  ↑ _ ⊤                                                          ↝⟨ inverse (drop-⊤-right λ _ → Bijection.↑↔) ⟩
  ↑ _ ⊤ × ↑ _ ⊤                                                  ↔⟨⟩
  (∃ λ (ps : All P []) → All Q (_↔_.to ∃-All↔List-∃ ([] , ps)))  □
All-Σ {P = P} {Q = Q} {xs = x ∷ xs} =
  All (λ x → Σ (P x) (curry Q x)) (x ∷ xs)                            ↔⟨⟩

  Σ (P x) (curry Q x) × All (λ x → Σ (P x) (curry Q x)) xs            ↝⟨ ∃-cong (λ _ → All-Σ) ⟩

  Σ (P x) (curry Q x) ×
  (∃ λ (ps : All P xs) → All Q (_↔_.to ∃-All↔List-∃ (_ , ps)))        ↝⟨ inverse Σ-assoc ⟩

  (∃ λ p → Q (x , p) ×
   ∃ λ (ps : All P xs) → All Q (_↔_.to ∃-All↔List-∃ (_ , ps)))        ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩

  (∃ λ p → ∃ λ (ps : All P xs) →
   Q (x , p) × All Q (_↔_.to ∃-All↔List-∃ (_ , ps)))                  ↝⟨ Σ-assoc ⟩

  (∃ λ (p , ps) → Q (x , p) × All Q (_↔_.to ∃-All↔List-∃ (xs , ps)))  ↔⟨⟩

  (∃ λ (ps : All P (x ∷ xs)) →
     All Q (_↔_.to ∃-All↔List-∃ (x ∷ xs , ps)))                       □

Vec-Σ :
  {A : Type a} {P : A → Type p} →
  Vec (Σ A P) n ↔
  ∃ λ (xs : Vec A n) → All P (Vec.to-list xs)
Vec-Σ {n = zero} {A = A} {P = P} =
  Vec (Σ A P) zero                                  ↔⟨⟩
  ↑ _ ⊤                                             ↝⟨ Bijection.↑↔ ⟩
  ⊤                                                 ↝⟨ inverse Bijection.↑↔ ⟩
  ↑ _ ⊤                                             ↝⟨ inverse (drop-⊤-right λ _ → Bijection.↑↔) ⟩
  ↑ _ ⊤ × ↑ _ ⊤                                     ↔⟨⟩
  (∃ λ (xs : Vec A zero) → All P (Vec.to-list xs))  □
Vec-Σ {n = suc n} {A = A} {P = P} =
  Vec (Σ A P) (suc n)                                                ↔⟨⟩

  Σ A P × Vec (Σ A P) n                                              ↝⟨ ∃-cong (λ _ → Vec-Σ) ⟩

  (Σ A P × ∃ λ (xs : Vec A n) → All P (Vec.to-list xs))              ↝⟨ inverse Σ-assoc ⟩

  (∃ λ (x : A) → P x × ∃ λ (xs : Vec A n) → All P (Vec.to-list xs))  ↝⟨ ∃-cong (λ _ → ∃-comm) ⟩

  (∃ λ (x : A) → ∃ λ (xs : Vec A n) → P x × All P (Vec.to-list xs))  ↝⟨ Σ-assoc ⟩

  (∃ λ ((x , xs) : A × Vec A n) → P x × All P (Vec.to-list xs))      ↔⟨⟩

  (∃ λ ((x , xs) : Vec A (suc n)) → P x × All P (Vec.to-list xs))    □

private

  -- The following alternative proof, which makes use of All-Σ, might
  -- compute less well if the J rule does not compute.

  Vec-Σ′ :
    {A : Type a} {P : A → Type p} →
    Vec (Σ A P) n ↔
    ∃ λ (xs : Vec A n) → All P (Vec.to-list xs)
  Vec-Σ′ {n = n} {A = A} {P = P} =
    Vec (Σ A P) n                                           ↝⟨ inverse All-const-replicate ⟩

    All (const (Σ A P)) (L.replicate n tt)                  ↝⟨ All-Σ ⟩

    (∃ λ (xs : All (const A) (L.replicate n tt)) →
       All (P ∘ proj₂) (_↔_.to ∃-All↔List-∃ (_ , xs)))      ↝⟨ (∃-cong λ _ → inverse All-map) ⟩

    (∃ λ (xs : All (const A) (L.replicate n tt)) →
       All P (L.map proj₂ (_↔_.to ∃-All↔List-∃ (_ , xs))))  ↝⟨ inverse (Σ-cong (inverse All-const-replicate) λ _ →
                                                               ≡⇒↝ _ (cong (All P) lemma)) ⟩□
    (∃ λ (xs : Vec A n) → All P (Vec.to-list xs))           □
    where
    lemma :
      ∀ {n} {xs : Vec A n} →
      Vec.to-list xs ≡
      L.map proj₂
        (_↔_.to ∃-All↔List-∃ (_ , _↔_.from All-const-replicate xs))
    lemma {n = zero}  = refl _
    lemma {n = suc n} = cong (_ ∷_) lemma

-- Concatenation.

append : All P xs → All P ys → All P (xs ++ ys)
append = curry (_↔_.from All-++)

private

  -- A lemma used below.

  subst-sym-refl : {p : P x} → subst P (sym (refl x)) p ≡ p
  subst-sym-refl {P = P} {x = x} {p = p} =
    subst P ⟨ sym (refl x) ⟩ p  ≡⟨ ⟨by⟩ sym-refl ⟩
    ⟨ subst P (refl x) p ⟩      ≡⟨ ⟨by⟩ subst-refl ⟩∎
    p                           ∎

-- The functions index and tabulate are inverses (roughly).

tabulate∘index :
  ∀ {xs} (ps : All P xs) →
  tabulate (index ps) ≡ ps
tabulate∘index         {xs = []}    _        = refl _
tabulate∘index {P = P} {xs = _ ∷ _} (p , ps) = cong₂ _,_
  (subst P (sym (refl _)) p  ≡⟨ subst-sym-refl ⟩∎
   p                         ∎)
  (tabulate (index ps)  ≡⟨ tabulate∘index ps ⟩∎
   ps                   ∎)

index∘tabulate :
  ∀ {xs} (f : ∀ {x} → x ∈ xs → P x) (×∈xs : x ∈ xs) →
  index (tabulate f) ×∈xs ≡ f ×∈xs
index∘tabulate         {xs = _ ∷ _} f (inj₂ p)  = index∘tabulate _ p
index∘tabulate {P = P} {xs = _ ∷ _} f (inj₁ eq) = elim₁
  (λ eq → subst P (sym eq) (f (inj₁ (refl _))) ≡ f (inj₁ eq))
  subst-sym-refl
  eq

-- The tabulate function preserves pointwise equality.

tabulate-cong :
  ∀ {xs} {f g : ∀ {x} → x ∈ xs → P x} →
  (∀ {x} (x∈xs : x ∈ xs) → f x∈xs ≡ g x∈xs) →
  tabulate f ≡ tabulate g
tabulate-cong {xs = []}    _   = refl _
tabulate-cong {xs = _ ∷ _} f≡g =
  cong₂ _,_ (f≡g _) (tabulate-cong (f≡g ∘ inj₂))

-- An extensionality principle for All.

extensionality :
  ∀ {xs} {ps qs : All P xs} →
  (∀ {x} (x∈xs : x ∈ xs) → index ps x∈xs ≡ index qs x∈xs) →
  ps ≡ qs
extensionality {ps = ps} {qs} ps≡qs =
  ps                   ≡⟨ sym $ tabulate∘index _ ⟩
  tabulate (index ps)  ≡⟨ tabulate-cong ps≡qs ⟩
  tabulate (index qs)  ≡⟨ tabulate∘index _ ⟩∎
  qs                   ∎

-- All and A.All are pointwise logically equivalent.

All⇔All : All P xs ⇔ A.All P xs
All⇔All = record { to = λ p _ → index p; from = λ f → tabulate (f _) }

-- There is a split surjection from A.All P xs to All P xs.

All↠All : A.All P xs ↠ All P xs
All↠All = record
  { logical-equivalence = inverse All⇔All
  ; right-inverse-of    = tabulate∘index
  }

-- All and A.All are pointwise equivalent (assuming extensionality).

All↔All :
  ∀ {k} {A : Type a} {P : A → Type p} {xs : List A} →
  Extensionality? k a (a ⊔ p) →
  All P xs ↝[ k ] A.All P xs
All↔All {a = a} =
  generalise-ext?
    All⇔All
    (λ ext →
         (λ _ →
            apply-ext ext λ _ →
            apply-ext (lower-extensionality a a ext) $
            index∘tabulate _)
       , tabulate∘index)

-- All preserves decidability of equality.

module Dec (dec : ∀ {x} → Decidable-equality (P x)) where

  infix 4 _≟_

  _≟_ : Decidable-equality (All P xs)
  _≟_ {xs = []}    = ↑.Dec._≟_ ⊤._≟_
  _≟_ {xs = _ ∷ _} = ×.Dec._≟_ dec _≟_

-- If xs and ys have type List A, where A is a set, then equality is
-- decidable for xs ⊆ ys.

module Dec-⊆ (A-set : Is-set A) where

  infix 4 _≟_

  _≟_ : {xs ys : List A} → Decidable-equality (xs ⊆ ys)
  _≟_ = Dec._≟_ (Dec-∈._≟_ A-set)

-- All preserves h-levels.

H-level-All :
  ∀ n →
  (∀ x → H-level n (P x)) →
  (∀ xs → H-level n (All P xs))
H-level-All n h []       = mono (Nat.zero≤ n) $
                           ↑-closure 0 ⊤-contractible
H-level-All n h (x ∷ xs) =
  ×-closure n (h _) (H-level-All n h xs)

-- The _⊆_ relation matches _∼[ implication ]_.

⊆↔∼[implication] :
  ∀ {k} {A : Type a} {xs ys : List A} →
  Extensionality? k a a →
  xs ⊆ ys ↝[ k ] xs ∼[ implication ] ys
⊆↔∼[implication] {xs = xs} {ys} ext =
  xs ⊆ ys                 ↝⟨ All↔All ext ⟩
  xs A.⊆ ys               ↔⟨ A.⊆↔∼[implication] ⟩
  xs ∼[ implication ] ys  □

-- A variant of _⊆_, based on A._⊆_.

infix 4 _⊆′_

_⊆′_ : {A : Type a} → List A → List A → Type a
xs ⊆′ ys = ∀ {z} → z ∈ xs → z ∈ ys

-- Some congruence lemmas.

All-cong₁ :
  ∀ {k} →
  (∀ x → P x ↝[ k ] Q x) →
  All P xs ↝[ k ] All Q xs
All-cong₁ {xs = []} P↝Q =
  ↑ _ ⊤  ↔⟨ Bijection.↑↔ ⟩
  ⊤      ↔⟨ inverse Bijection.↑↔ ⟩□
  ↑ _ ⊤  □
All-cong₁ {P = P} {Q = Q} {xs = x ∷ xs} P↝Q =
  P x × All P xs  ↝⟨ P↝Q _ ×-cong All-cong₁ P↝Q ⟩□
  Q x × All Q xs  □

map₁ : (∀ {x} → P x → Q x) → All P xs → All Q xs
map₁ f = All-cong₁ (λ _ → f)

map₂ : ys ⊆ xs → All P xs → All P ys
map₂ {ys = []}    _           ps = _
map₂ {ys = _ ∷ _} (y∈xs , qs) ps = index ps y∈xs , map₂ qs ps

map₂′ : ys ⊆′ xs → All P xs → All P ys
map₂′ = map₂ ∘ tabulate

map : (∀ {x} → P x → Q x) → ys ⊆ xs → All P xs → All Q ys
map P→Q ys∼xs = map₁ P→Q ∘ map₂ ys∼xs

All-cong-→ :
  (∀ x → P x → Q x) →
  ys ∼[ implication ] xs →
  All P xs → All Q ys
All-cong-→ {P = P} {Q = Q} {ys = ys} {xs = xs} P→Q ys∼xs =
  All P xs    ↝⟨ _↠_.from All↠All ⟩
  A.All P xs  ↝⟨ A.All-cong-→ P→Q ys∼xs ⟩
  A.All Q ys  ↝⟨ _↠_.to All↠All ⟩□
  All Q ys    □

All-cong :
  ∀ {k} {A : Type a} {P : A → Type p} {Q : A → Type q} {xs ys} →
  Extensionality? ⌊ k ⌋-sym a (a ⊔ p ⊔ q) →
  (∀ x → P x ↝[ ⌊ k ⌋-sym ] Q x) →
  xs ∼[ ⌊ k ⌋-sym ] ys →
  All P xs ↝[ ⌊ k ⌋-sym ] All Q ys
All-cong {a = a} {p = p} {q = q} {k} {P = P} {Q} {xs} {ys}
         ext P↝Q xs∼ys =
  All P xs    ↝⟨ All↔All (lower-extensionality? ⌊ k ⌋-sym a q ext) ⟩
  A.All P xs  ↝⟨ A.All-cong ext P↝Q xs∼ys ⟩
  A.All Q ys  ↝⟨ inverse-ext? All↔All (lower-extensionality? ⌊ k ⌋-sym a p ext) ⟩□
  All Q ys    □

-- A fusion lemma for index.

index∘index :
  ∀ {xs ys} {ps : All P ys} {x∈xs : x ∈ xs} (xs⊆ys : xs ⊆ ys) →
  index ps (index xs⊆ys x∈xs) ≡ index (map₂ xs⊆ys ps) x∈xs
index∘index {xs = _ ∷ _} {x∈xs = inj₂ _}  (_ , ⊆ys) =
  index∘index ⊆ys

index∘index {P = P} {xs = _ ∷ _} {ys} {ps} {inj₁ eq} (∈ys , _) = elim₁
  (λ eq → index ps (subst (_∈ ys) (sym eq) ∈ys) ≡
          subst P (sym eq) (index ps ∈ys))
  (index ps ⟨ subst (_∈ ys) (sym (refl _)) ∈ys ⟩  ≡⟨ ⟨by⟩ subst-sym-refl ⟩
   index ps ∈ys                                   ≡⟨ sym subst-sym-refl ⟩∎
   subst P (sym (refl _)) (index ps ∈ys)          ∎)
  eq

-- Some rearrangement lemmas for index.

index-map₁ :
  ∀ {P : A → Type p}
    xs {f : ∀ {x} → P x → Q x} {ps : All P xs} {q : x ∈ xs} →
  index (map₁ f ps) q ≡ f (index ps q)
index-map₁ (_ ∷ xs) {q = inj₂ q}  = index-map₁ xs

index-map₁ {Q = Q} {P = P} (_ ∷ _) {f} {p , _} {q = inj₁ eq} = elim₁
  (λ eq → subst Q (sym eq) (f p) ≡
          f (subst P (sym eq) p))
  (subst Q (sym (refl _)) (f p)  ≡⟨ subst-sym-refl ⟩
   f ⟨ p ⟩                       ≡⟨ ⟨by⟩ subst-sym-refl ⟩∎
   f (subst P (sym (refl _)) p)  ∎)
  eq

index-append-Any-++-inj₁ :
  ∀ {xs ys} {ps : All P xs} {qs : All P ys} (x∈xs : x ∈ xs) →
  index (append ps qs) (_↔_.from (Any-++ _ _ _) (inj₁ x∈xs)) ≡
  index ps x∈xs
index-append-Any-++-inj₁ {xs = _ ∷ _} (inj₁ _) = refl _
index-append-Any-++-inj₁ {xs = _ ∷ _} (inj₂ p) =
  index-append-Any-++-inj₁ p

index-append-Any-++-inj₂ :
  ∀ xs {ys} {ps : All P xs} {qs : All P ys} {y∈ys : y ∈ ys} →
  index (append ps qs) (_↔_.from (Any-++ _ xs _) (inj₂ y∈ys)) ≡
  index qs y∈ys
index-append-Any-++-inj₂ []       = refl _
index-append-Any-++-inj₂ (_ ∷ xs) = index-append-Any-++-inj₂ xs

index-All-const :
  ∀ (xs : List A) {bs : All (const B) xs} {i} →
  Vec.index (_↔_.to All-const bs) i ≡
  index bs (proj₂ (_↔_.from (Fin-length xs) i))
index-All-const (_ ∷ xs)    {i = fsuc i} = index-All-const xs
index-All-const (_ ∷ _) {b , _} {fzero}  =
  b                                 ≡⟨ sym subst-sym-refl ⟩∎
  subst (const _) (sym (refl _)) b  ∎

-- A rearrangement lemma for Vec-Σ.

proj₁-Vec-Σ :
  {A : Type a} {P : A → Type p} {xs : Vec (Σ A P) n} →
  proj₁ (_↔_.to Vec-Σ xs) ≡ Vec.map proj₁ xs
proj₁-Vec-Σ {n = zero}  = refl _
proj₁-Vec-Σ {n = suc n} = cong (_ ,_) proj₁-Vec-Σ

-- A fusion lemma for map₂.

map₂∘map₂′ :
  ∀ {xs ys zs} {xs⊆ys : xs ⊆ ys} {ys⊆zs : ys ⊆′ zs} {ps : All P zs} →
  map₂ xs⊆ys (map₂′ ys⊆zs ps) ≡ map₂ (map₁ ys⊆zs xs⊆ys) ps
map₂∘map₂′ {xs = []}                             = refl _
map₂∘map₂′ {xs = _ ∷ _} {xs⊆ys = q , _} {f} {ps} =
  cong₂ _,_ lemma map₂∘map₂′
  where
  lemma =
    index (map₂ (tabulate f) ps) q     ≡⟨ sym $ index∘index (tabulate f) ⟩
    index ps ⟨ index (tabulate f) q ⟩  ≡⟨ ⟨by⟩ (index∘tabulate f q) ⟩∎
    index ps (f q)                     ∎

-- Some rearrangement lemmas for map₂′.

map₂′-inj₂-∘ :
  ∀ {xs ys} {f : ys ⊆′ xs} {p : P x} {ps : All P xs} →
  map₂′ (inj₂ ∘ f) (p , ps) ≡ map₂′ f ps
map₂′-inj₂-∘ {ys = []}    = refl _
map₂′-inj₂-∘ {ys = _ ∷ _} = cong (_ ,_) map₂′-inj₂-∘

mutual

  map₂′-id :
    ∀ {xs} {ps : All P xs} →
    map₂′ id ps ≡ ps
  map₂′-id {xs = []}    = refl _
  map₂′-id {xs = _ ∷ _} = cong₂ _,_ subst-sym-refl map₂′-inj₂

  map₂′-inj₂ :
    ∀ {xs} {p : P x} {ps : All P xs} →
    map₂′ inj₂ (p , ps) ≡ ps
  map₂′-inj₂ {p = p} {ps} =
    map₂′ inj₂ (p , ps)  ≡⟨ map₂′-inj₂-∘ ⟩
    map₂′ id ps          ≡⟨ map₂′-id ⟩∎
    ps                   ∎

map₂′-⊎-map-id :
  ∀ {xs ys} {f : ys ⊆′ xs} {p : P x} {ps : All P xs} →
  map₂′ (⊎-map id f) (p , ps) ≡ (p , map₂′ f ps)
map₂′-⊎-map-id {f = f} {p} {ps} = cong₂ _,_ subst-sym-refl
  (map₂′ (inj₂ ∘ f) (p , ps)  ≡⟨ map₂′-inj₂-∘ ⟩∎
   map₂′ f ps                 ∎)

map₂′-⊎-map-id-inj₂ :
  ∀ {xs} {p : P x} {q : P y} {ps : All P xs} →
  map₂′ (⊎-map id inj₂) (p , q , ps) ≡ (p , ps)
map₂′-⊎-map-id-inj₂ {p = p} {q} {ps} =
  map₂′ (⊎-map id inj₂) (p , q , ps)  ≡⟨ map₂′-⊎-map-id ⟩
  (p , map₂′ inj₂ (q , ps))           ≡⟨ cong (_ ,_) map₂′-inj₂ ⟩
  (p , ps)                            ∎

map₂′-++-cong :
  ∀ xs₁ {xs₂ ys₁ ys₂} {ps : All P xs₂} {qs : All P ys₂}
  (f : xs₁ ⊆′ xs₂) {g : ys₁ ⊆′ ys₂} →
  map₂′ (++-cong (λ _ → f) (λ _ → g) _) (append ps qs) ≡
  append (map₂′ f ps) (map₂′ g qs)
map₂′-++-cong [] {ys₁ = []} _ = refl _

map₂′-++-cong [] {xs₂} {_ ∷ _} {ps = ps} {qs} f {g} = cong₂ _,_

  (index (append ps qs) (++-cong (λ _ → f) (λ _ → g) _ (inj₁ (refl _)))  ≡⟨⟩

   index (append ps qs)
     (_↔_.from (Any-++ _ xs₂ _) (inj₂ (g (inj₁ (refl _)))))              ≡⟨ index-append-Any-++-inj₂ xs₂ ⟩∎

   index qs (g (inj₁ (refl _)))                                          ∎)

  (map₂′ (++-cong (λ _ → f) (λ _ → g ∘ inj₂) _) (append ps qs)  ≡⟨ map₂′-++-cong _ f ⟩∎
   append (map₂′ f ps) (map₂′ (g ∘ inj₂) qs)                    ∎)

map₂′-++-cong (_ ∷ _) {ps = ps} {qs} f {g} = cong₂ _,_

  (index (append ps qs) (++-cong (λ _ → f) (λ _ → g) _ (inj₁ (refl _)))  ≡⟨⟩

   index (append ps qs)
         (_↔_.from (Any-++ _ _ _) (inj₁ (f (inj₁ (refl _)))))            ≡⟨ index-append-Any-++-inj₁ (f (inj₁ (refl _))) ⟩∎

   index ps (f (inj₁ (refl _)))                                          ∎)

  (map₂′ (++-cong (λ _ → f) (λ _ → g) _ ∘ inj₂) (append ps qs)  ≡⟨ cong (λ f → map₂ f _) (tabulate-cong (++-cong-inj₂ f g)) ⟩
   map₂′ (++-cong (λ _ → f ∘ inj₂) (λ _ → g) _) (append ps qs)  ≡⟨ map₂′-++-cong _ (f ∘ inj₂) ⟩
   append (map₂′ (f ∘ inj₂) ps) (map₂′ g qs)                    ≡⟨⟩
   append (proj₂ (map₂′ f ps)) (map₂′ g qs)                     ∎)

  where

  ++-cong-inj₂ :
    ∀ {xs₁ xs₂ ys₁ ys₂}
    (f : x ∷ xs₁ ⊆′ xs₂) (g : ys₁ ⊆′ ys₂) {z} (p : z ∈ xs₁ ++ ys₁) →
    ++-cong (λ _ → f) (λ _ → g) _ (inj₂ p) ≡
    ++-cong (λ _ → f ∘ inj₂) (λ _ → g) _ p
  ++-cong-inj₂ f g p =
    ++-cong (λ _ → f) (λ _ → g) _ (inj₂ p)                                  ≡⟨⟩

    _↔_.from (Any-++ _ _ _)
      ⟨ ⊎-map f g (_↔_.to ⊎-assoc (inj₂ (_↔_.to (Any-++ _ _ _) p))) ⟩       ≡⟨ ⟨by⟩ (lemma (_↔_.to (Any-++ _ _ _) p)) ⟩

    _↔_.from (Any-++ _ _ _) (⊎-map (f ∘ inj₂) g (_↔_.to (Any-++ _ _ _) p))  ≡⟨⟩

    ++-cong (λ _ → f ∘ inj₂) (λ _ → g) _ p                                  ∎
    where
    lemma : ∀ x → ⊎-map f g (_↔_.to ⊎-assoc (inj₂ x)) ≡
                  ⊎-map (f ∘ inj₂) g x
    lemma = [ (λ _ → refl _) , (λ _ → refl _) ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality