text:
{- This file contains a direct proof that the Brunerie number (the
number n s.t. π₄(S³)≅ℤ/nℤ) is 2, not relying on any of the more
advanced constructions in chapters 4-6 in Brunerie's thesis (but still
using chapters 1-3 for the construction). The Brunerie number is defined via

S³ ≃ S¹ * S¹ -ᵂ→ S² ∨ S² -ᶠᵒˡᵈ→ S²

where * denotes the join, ∨ denotes the wedge sum, W is the Whitehead
map (see joinTo⋁ in Cubical.Homotopy.Whitehead) and the final map is
just the folding map. η := ∣ fold ∘ W ∣₀ defines an element of π₃(S²).
The (absolute value) of the Brunerie number is given by the absolute
value of ϕ(η) for any iso π₃(S²)≅ℤ. The reason it's hard to prove
ϕ(η) = ± 2 directly is mainly because the equivalence S³ ≃ S¹ * S¹
complicates things. In this file, we try to work around this problem.

The proof goes as follows.

1. Define π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ and define explicitly an
addition on this type. Prove that the equivalence π₃(A) ≃ π₃*(A) is
structure preserving, thereby giving a group structure on π₃*(A) and a
group iso π₃*(A) ≅ π₃(A)

2. Under this iso, η gets mapped to η₁ (by construction) defined by
S¹ * S¹ -ᵂ→ S² ∨ S² -ᶠᵒˡᵈ→ S²
which is much easier to work with.

3. Define a sequence of equivalences
π₃*(S²) ≅ π₃*(S¹ * S¹) ≅ π₃*(S³) ≅ π₃(S³) ≅ ℤ
and trace η₁ in each step, proving that it ends up at -2. It turns out
that that the iso S³ ≃ S¹ * S¹, which has been relatively explicitly
defined in Cubical.HITs.Sphere.Properties, kills off a good deal of
``annoying'' terms on the way, making the proof rather straightforward.

4. Conclude that π₄(S³) ≅ ℤ/2ℤ.

-}
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Homotopy.Group.Pi4S3.QuickProof where

open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.Pi3S2
open import Cubical.Homotopy.Group.PinSn
open import Cubical.Homotopy.Hopf
open import Cubical.Homotopy.Whitehead using (joinTo⋁)
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.HopfInvariant.HopfMap using (hopfMap≡HopfMap')
-- Only imports a simple equality of two constructions of the Hopf map.
open import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber
  using (fold∘W ; coFib-fold∘W∙ ; π₄S³≅π₃coFib-fold∘W∙ ; S³→S²→Pushout→Unit)
-- Only imports definitions/proofs from chapter 1-3 in Brunerie's thesis

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

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Int
  renaming (ℤ to Z ; _·_ to _·Z_ ; _+_ to _+Z_)

open import Cubical.HITs.S1 renaming (_·_ to _*_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.Join hiding (joinS¹S¹→S³)
open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.SetTruncation
  renaming (rec2 to sRec2 ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.Truncation renaming (rec to trRec)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Instances.IntMod

open S¹Hopf
open Iso
open GroupStr

private
  variable
    ℓ : Level
    A B : Pointed ℓ

-- Some abbreviations and simple lemmas
private
  σ₁ = σ (S₊∙ 1)
  σ₂ = σ (S₊∙ 2)

  σ-filler : ∀ {ℓ} {A : Type ℓ} (x y : A) (i j : I) → Susp A
  σ-filler x y i j = compPath-filler (merid x) (sym (merid y)) i j

  to3ConnectedId : {f g : A →∙ B}
    → (isConnected 3 (typ B)) → fst f ≡ fst g → ∣ f ∣₂ ≡ ∣ g ∣₂
  to3ConnectedId {f = f} {g = g} con p =
    trRec (squash₂ _ _)
      (λ q → cong ∣_∣₂ (ΣPathP (p , q)))
      (fst (isConnectedPathP 1 (isConnectedPath 2 con _ _) (snd f) (snd g)))

  connS³ : isConnected 3 (S₊ 3)
  connS³ =
    isConnectedSubtr 3 1 (sphereConnected 3)

  con-joinS¹S¹ : isConnected 3 (join S¹ S¹)
  con-joinS¹S¹ =
    (isConnectedRetractFromIso 3
        (IsoSphereJoin 1 1)
        (isConnectedSubtr 3 1 (sphereConnected 3)))

-- Key goal: prove that the following element of π₃(S²) gets mapped to -2
η : π' 3 (S₊∙ 2)
η = fst (π'∘∙Hom 2 (fold∘W , refl)) ∣ id∙ (S₊∙ 3) ∣₂

{- Step 1. Define an addition on π₃*(A) := ∥ S¹ * S¹ →∙ A ∥₀ -}
-- On the underlying function spaces.
_+join_ : (f g : (join S¹ S¹ , inl base) →∙ A)
       → (join S¹ S¹ , inl base) →∙ A
fst (f +join g) (inl x) = fst f (inl x)
fst (f +join g) (inr x) = fst g (inr x)
fst (f +join g) (push a b i) =
  (cong (fst f) (push a b ∙ sym (push base b))
  ∙∙ snd f ∙ sym (snd g)
  ∙∙ cong (fst g) (push base base ∙∙ sym (push a base) ∙∙ push a b)) i
snd (f +join g) = snd f

-- Homotopy group version
_π₃*+_ : (f g : ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂)
      → ∥ (join S¹ S¹ , inl base) →∙ S₊∙ 2 ∥₂
_π₃*+_ = sRec2 squash₂ λ x y → ∣ x +join y ∣₂

-- transferring between π₃ and π₃*
-- (homotopy groups defined in terms of S¹ * S¹)
joinify :  S₊∙ 3 →∙ A → (join S¹ S¹ , inl base) →∙ A
fst (joinify f) x = fst f (joinS¹S¹→S³ x)
snd (joinify f) = snd f

disjoin : (join S¹ S¹ , inl base) →∙ A → S₊∙ 3 →∙ A
fst (disjoin f) = λ x → fst f (Iso.inv (IsoSphereJoin 1 1) x)
snd (disjoin f) = snd f

-- joinify is structure preserving
+join≡∙Π : (f g : S₊∙ 3 →∙ A)
         → joinify (∙Π f g)
         ≡ (joinify f +join joinify g)
+join≡∙Π f' g' =
  ΣPathP ((funExt (λ { (inl x) → sym fp
                     ; (inr x) → sym gp ∙ cong g (merid north)
                     ; (push a b i) j → main a b j i}))
        , λ i j → fp (j ∨ ~ i))
  where
  f = fst f'
  g = fst g'

  fp = snd f'
  gp = snd g'

  path-lem : ∀ {ℓ} {A : Type ℓ} {x y z w u : A}
       (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) (s : w ≡ u)
    → (refl ∙∙ p ∙∙ q) ∙ (r ∙∙ s ∙∙ refl)
     ≡ (p ∙∙ (q ∙ r) ∙∙ s)
  path-lem p q r s =
       cong ((p ∙ q) ∙_) (sym (compPath≡compPath' r s))
    ∙∙ sym (∙assoc p q (r ∙ s))
    ∙∙ cong (p ∙_) (∙assoc q r s)
     ∙ sym (doubleCompPath≡compPath p (q ∙ r) s)

  main-helper : (a b : S¹)
    → Square ((refl ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp)
             ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ refl))
             ((cong f (merid (S¹×S¹→S² a b))
             ∙ sym (cong f (merid north)))
               ∙∙ (fp ∙ sym gp)
               ∙∙ cong g (merid (S¹×S¹→S² a b)))
           (λ _ → f north)
           (cong g (merid north))
  main-helper a b =
    path-lem (cong f (σ₂ (S¹×S¹→S² a b)))  fp (sym gp)
             (cong g (σ₂ (S¹×S¹→S² a b)))
          ◁ lem
    where
    lem : PathP (λ i → f north ≡ cong g (merid north) i)
              ((λ i → f (σ₂ (S¹×S¹→S² a b) i))
                    ∙∙ fp ∙ (sym gp) ∙∙
               (cong g (σ₂ (S¹×S¹→S² a b))))
              ((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north)))
               ∙∙ fp ∙ sym gp
               ∙∙ cong g (merid (S¹×S¹→S² a b)))
    lem i j =
      hcomp (λ k → λ { (i = i0) →
                          (cong-∙ f (merid (S¹×S¹→S² a b))
                                    (sym (merid north)) (~ k)
                       ∙∙ fp ∙ sym gp
                       ∙∙ (λ i → g (σ-filler (S¹×S¹→S² a b) north k i))) j
                       ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b))
                                       ∙ sym (cong f (merid north)))
                                     ∙∙ (fp ∙ sym gp)
                                     ∙∙ cong g (merid (S¹×S¹→S² a b))) j
                       ; (j = i0) → f north
                       ; (j = i1) → g (merid north (~ k ∨ i))})
            (((cong f (merid (S¹×S¹→S² a b)) ∙ sym (cong f (merid north)))
            ∙∙ (fp ∙ sym gp)
            ∙∙ cong g (merid (S¹×S¹→S² a b))) j)

  main-helper₂ : (a b : S¹)
    → cong (fst (joinify g')) (push base base ∙∙ sym (push a base) ∙∙ push a b)
    ≡ cong g (merid (S¹×S¹→S² a b))
  main-helper₂ a b = cong-∙∙ (fst (joinify g'))
       (push base base) (sym (push a base)) (push a b)
       ∙ cong (cong g (merid north) ∙∙_∙∙ cong g (merid (S¹×S¹→S² a b)))
              (cong (cong g) (cong sym (cong merid (S¹×S¹→S²rUnit a))))
       ∙  ((λ i → (cong g (λ j → merid north (j ∧ ~ i)))
       ∙∙ (cong g (λ j → merid north (~ j ∧ ~ i)))
       ∙∙ cong g (merid (S¹×S¹→S² a b)))
       ∙ sym (lUnit (cong g (merid (S¹×S¹→S² a b)))))

  main : (a b : S¹)
    → PathP (λ i → fp (~ i) ≡ (sym gp ∙ cong g (merid north)) i)
            ((sym fp ∙∙ cong f (σ₂ (S¹×S¹→S² a b)) ∙∙ fp)
           ∙ (sym gp ∙∙ cong g (σ₂ (S¹×S¹→S² a b)) ∙∙ gp))
            ((cong (fst (joinify f')) (push a b ∙ sym (push base b))
          ∙∙ fp ∙ sym gp
          ∙∙ cong (fst (joinify g'))
              (push base base ∙∙ sym (push a base) ∙∙ push a b)))
  main a b =
    ((λ i j → hcomp (λ k → λ {(i = i0) → (((λ j → fp (~ j ∧ k))
                                          ∙∙ cong f (σ₂ (S¹×S¹→S² a b))
                                          ∙∙ fp)
                                          ∙ (sym gp
                                          ∙∙ cong g (σ₂ (S¹×S¹→S² a b))
                                          ∙∙ λ j → gp (j ∧ k))) j
                              ; (i = i1) → ((cong f (merid (S¹×S¹→S² a b))
                                           ∙ sym (cong f (merid north)))
                                          ∙∙ fp ∙ sym gp
                                          ∙∙ cong g (merid (S¹×S¹→S² a b))) j
                              ; (j = i0) → fp (~ i ∧ k)
                              ; (j = i1) → compPath-filler'
                                           (sym gp) (cong g (merid north)) k i})
                     (main-helper a b i j)))
    ▷ λ i →
      cong-∙ (fst (joinify f')) (push a b) (sym (push base b)) (~ i)
      ∙∙ fp ∙ sym gp
      ∙∙ main-helper₂ a b (~ i)

-- Group structure on π₃*
-- todo: remove connectivity assumption
module _ (A : Pointed ℓ) (con : (isConnected 3 (typ A))) where
  π₃*Iso : Iso (typ (π'Gr 2 A)) ∥ (join S¹ S¹ , inl base) →∙ A ∥₂
  fun π₃*Iso = sMap joinify
  inv π₃*Iso = sMap disjoin
  rightInv π₃*Iso =
    sElim (λ _ → isSetPathImplicit)
      λ f → to3ConnectedId
        con (funExt λ x → cong (fst f) (Iso.leftInv (IsoSphereJoin 1 1) x))
  leftInv π₃*Iso =
    sElim (λ _ → isSetPathImplicit)
      λ f → to3ConnectedId
        con (funExt (λ x → cong (fst f) (Iso.rightInv (IsoSphereJoin 1 1) x)))

  π₃* : Group ℓ
  π₃* = InducedGroup (π'Gr 2 A) (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂))
        (isoToEquiv π₃*Iso)
          (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g)))

  π₃≅π₃* : GroupEquiv (π'Gr 2 A) π₃*
  π₃≅π₃* =
    InducedGroupEquiv (π'Gr 2 A) (sRec2 squash₂ (λ x y → ∣ x +join y ∣₂))
        (isoToEquiv π₃*Iso)
          (sElim2 (λ _ _ → isSetPathImplicit) (λ f g → cong ∣_∣₂ (+join≡∙Π f g)))

-- Induced homomorphisms (A →∙ B) → (π₃*(A) → π₃*(B))
-- todo: remove connectivity assumptions
module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B)))
         (f : A →∙ B) where
  postCompπ₃* : GroupHom (π₃* A conA) (π₃* B conB)
  fst postCompπ₃* = sMap (f ∘∙_)
  snd postCompπ₃* =
    makeIsGroupHom
      (sElim2 (λ _ _ → isSetPathImplicit)
        λ h g → to3ConnectedId conB
          (funExt λ { (inl x) → refl
                    ; (inr x) → refl
                    ; (push a b i) j →
           (cong-∙∙ (fst f)
                    (cong (fst h) ((push a b ∙ (sym (push base b)))))
                    (snd h ∙ (sym (snd g)))
                    (cong (fst g) ((push base base
                               ∙∙ (sym (push a base))
                               ∙∙ push a b)))
          ∙ cong (cong (fst f)
                   (cong (fst h) (push a b ∙ (sym (push base b))))
                    ∙∙_∙∙
                   cong (fst f ∘ fst g)
                     ((push base base ∙∙ (sym (push a base)) ∙∙ push a b)))
                 (cong-∙ (fst f) (snd h) (sym (snd g))
                 ∙ λ j → compPath-filler (cong (fst f) (snd h)) (snd f) j
                        ∙ sym (compPath-filler
                               (cong (fst f) (snd g)) (snd f) j))) j i}))

-- Induced iso (A ≃∙ B) → π₃*(A) ≅ π₃*(B)
-- todo: remove connectivity assumptions
module _ (conA : (isConnected 3 (typ A))) (conB : (isConnected 3 (typ B)))
         (f : A ≃∙ B) where
  postCompπ₃*Equiv : GroupEquiv (π₃* A conA) (π₃* B conB)
  fst postCompπ₃*Equiv = isoToEquiv h
    where
    h : Iso (π₃* A conA .fst) (π₃* B conB .fst)
    fun h = fst (postCompπ₃* conA conB (≃∙map f))
    inv h = fst (postCompπ₃* conB conA (≃∙map (invEquiv∙ f)))
    rightInv h =
      sElim (λ _ → isSetPathImplicit)
        λ g → to3ConnectedId conB (funExt λ x → secEq (fst f) (fst g x))
    leftInv h =
      sElim (λ _ → isSetPathImplicit)
        λ g → to3ConnectedId conA (funExt λ x → retEq (fst f) (fst g x))
  snd postCompπ₃*Equiv = snd (postCompπ₃* conA conB (≃∙map f))

-- The relevant groups (in order of the iso π₃(S²) ≅ ℤ)
π₃S² = π'Gr 2 (S₊∙ 2)

π₃*S² = π₃* (S₊∙ 2) (sphereConnected 2)

π₃*joinS¹S¹ = π₃* (join S¹ S¹ , inl base) con-joinS¹S¹

π₃*S³ = π₃* (S₊∙ 3) connS³

π₃S³ = π'Gr 2 (S₊∙ 3)

{- Goal now:  Show that
   (η : π₃(S²))
↦ (η₁ : π₃*(S²))
↦ (η₂ : π₃*(S¹ * S¹))
↦ (η₃ : π₃*(S³))
↦ (η₄ : π₃(S³))
↦ (-2 : ℤ)

for some terms η₁ ... η₄ by a sequence of isomorphisms
π₃(S²) ≅ π₃*(S²) ≅ π₃*(S¹ * S¹) ≅ π₃*(S³) ≅ π₃(S³) ≅ ℤ

Hence, there is an is an iso π₃(S²) ≅ ℤ taking η to
-2, from which we can conclude π₄(S³) ≅ ℤ/2ℤ.
-}

-- Underlying functions of (some of) the ηs
η₁-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 2
fst η₁-raw (inl x) = north
fst η₁-raw (inr x) = north
fst η₁-raw (push a b i) = (σ₁ b ∙ σ₁ a) i
snd η₁-raw = refl

η₂-raw : (join S¹ S¹ , inl base) →∙ (join S¹ S¹ , inl base)
fst η₂-raw (inl x) = inr (invLooper x)
fst η₂-raw (inr x) = inr x
fst η₂-raw (push a b i) =
    (sym (push (b * invLooper a) (invLooper a))
  ∙ push (b * invLooper a) b) i
snd η₂-raw = sym (push base base)

η₃-raw : (join S¹ S¹ , inl base) →∙ S₊∙ 3
fst η₃-raw (inl x) = north
fst η₃-raw (inr x) = north
fst η₃-raw (push a b i) =
  (sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b))) i
snd η₃-raw = refl

-- Homotopy group versions
η₁ : fst π₃*S²
η₁ = ∣ η₁-raw ∣₂

η₂ : fst (π₃*joinS¹S¹)
η₂ = ∣ η₂-raw ∣₂

η₃ : π₃*S³ .fst
η₃ = ∣ η₃-raw ∣₂

η₄ : fst π₃S³
η₄ = ·π' 2 (-π' 2 ∣ idfun∙ (S₊∙ 3) ∣₂) (-π' 2 ∣ idfun∙ (S₊∙ 3) ∣₂)

-- π₃S²≅π₃*S²
π₃S²→π₃*S² : GroupEquiv π₃S² π₃*S²
π₃S²→π₃*S² = π₃≅π₃* (S₊∙ 2) (sphereConnected 2)

-- Time for π₃*(S¹ * S¹) ≅ π₃*S².
-- We have this iso already, but slightly differently stated,
-- so the following proof becomes a bit technical.
-- We define it in terms a slight variation of the Hopf map

Hopfσ : join S¹ S¹ → S₊ 2
Hopfσ (inl x) = north
Hopfσ (inr x) = north
Hopfσ (push a b i) = σ₁ (invLooper a * b) i

π₃*joinS¹S¹→π₃*S² : GroupHom π₃*joinS¹S¹ π₃*S²
π₃*joinS¹S¹→π₃*S² =
  postCompπ₃* con-joinS¹S¹ (sphereConnected 2)
    (Hopfσ , refl)

π₃*joinS¹S¹≅π₃*S² : GroupEquiv π₃*joinS¹S¹ π₃*S²
fst (fst π₃*joinS¹S¹≅π₃*S²) = fst π₃*joinS¹S¹→π₃*S²
snd (fst π₃*joinS¹S¹≅π₃*S²) =
  subst isEquiv idLem isEquivπ₃*joinS¹S¹→π₃*S²'
  where
  π₃*joinS¹S¹→π₃*S²' : GroupHom π₃*joinS¹S¹ π₃*S²
  π₃*joinS¹S¹→π₃*S²' =
    postCompπ₃* con-joinS¹S¹ (sphereConnected 2)
      (fst ∘ JoinS¹S¹→TotalHopf , refl)

  isEquivπ₃*joinS¹S¹→π₃*S²' : isEquiv (fst π₃*joinS¹S¹→π₃*S²')
  isEquivπ₃*joinS¹S¹→π₃*S²' =
    transport (λ i → isEquiv (fst (help (~ i))))
      (snd (fst GrEq))
    where
    GrEq = compGroupEquiv (πS³≅πTotalHopf 2) π'₃S²≅π'₃TotalHopf

    help : PathP
        (λ i → GroupHom
                (GroupPath π₃*joinS¹S¹ π₃S³ .fst
                  (compGroupEquiv
                   (invGroupEquiv (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹))
                   (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl))) i)
                (GroupPath π₃*S² π₃S² .fst
                  (invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) i))
         π₃*joinS¹S¹→π₃*S²'
         (fst (fst GrEq) , snd GrEq)
    help =
      toPathP (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
        (funExt
          λ f → (λ i
           → transportRefl
              ((invGroupEquiv (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst .fst
                (fst π₃*joinS¹S¹→π₃*S²' (
                  ((fst (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹)))
                  (invEq (fst (π'Iso 2 (isoToEquiv (IsoSphereJoin 1 1) , refl)))
                     (transportRefl f i)))))) i)
              ∙ main f))

      where
      main : (f : _) → invEquiv (fst (π₃≅π₃* (S₊∙ 2) (sphereConnected 2))) .fst
        (fst π₃*joinS¹S¹→π₃*S²'
         (invEq
          (invEquiv (fst (π₃≅π₃* (join S¹ S¹ , inl base) con-joinS¹S¹)))
          (invEq (fst (π'Iso 2 (isoToEquiv Iso-joinS¹S¹-S³ , (λ _ → north))))
           f)))
        ≡ fst GrEq .fst f
      main = sElim (λ _ → isSetPathImplicit)
        λ f → to3ConnectedId (sphereConnected 2)
          (funExt λ x
            → (λ i → fst (JoinS¹S¹→TotalHopf (Iso.inv (IsoSphereJoin 1 1)
                              (fst f (Iso.rightInv (IsoSphereJoin 1 1) x i)))))
                    ∙ sym (funExt⁻ (sym (cong fst hopfMap≡HopfMap'))
                                (fst f x)))

  idLem : fst π₃*joinS¹S¹→π₃*S²' ≡ fst π₃*joinS¹S¹→π₃*S²
  idLem =
    funExt (sElim (λ _ → isSetPathImplicit)
           λ f → to3ConnectedId (sphereConnected 2)
      (funExt λ x → lem (fst f x)))
    where
    lem : (x : _) → fst (JoinS¹S¹→TotalHopf x) ≡ Hopfσ x
    lem (inl x) = refl
    lem (inr x) = sym (merid base)
    lem (push a b i) j =
      compPath-filler (merid (invLooper a * b)) (sym (merid base)) j i
snd π₃*joinS¹S¹≅π₃*S² = snd π₃*joinS¹S¹→π₃*S²

-- π₃*(S³) ≅ π₃*(S¹ * S¹)
π₃*S³≅π₃*joinS¹S¹ : GroupEquiv π₃*S³ π₃*joinS¹S¹
π₃*S³≅π₃*joinS¹S¹ =
  postCompπ₃*Equiv
    connS³ con-joinS¹S¹
      (isoToEquiv (invIso (IsoSphereJoin 1 1)) , refl)

-- π₃(S³)≅π₃*(S³)
π₃S³≅π₃*S³ : GroupEquiv π₃S³ π₃*S³
π₃S³≅π₃*S³ = π₃≅π₃* (S₊∙ 3) connS³

η↦η₁ :  fst (fst π₃S²→π₃*S²) η ≡ η₁
η↦η₁ = to3ConnectedId (sphereConnected 2)
         (funExt λ x → (funExt⁻ lem₁ x) ∙ sym (lem₂ x))
  where
  lem₁ : fold∘W ∘ joinS¹S¹→S³ ≡ fold⋁ ∘ (joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1})
  lem₁ = funExt λ x
    → cong (fold⋁ ∘ (joinTo⋁ {A = S₊∙ 1} {B = S₊∙ 1}))
      (leftInv (IsoSphereJoin 1 1) x)

  lem₂ : (x : join S¹ S¹) → fst η₁-raw x ≡ (fold⋁ ∘ joinTo⋁) x
  lem₂ (inl x) = refl
  lem₂ (inr x) = refl
  lem₂ (push a b i) j = help j i
    where
    help : (σ₁ b ∙ σ₁ a) ≡ cong (fold⋁ ∘ joinTo⋁) (push a b)
    help = sym (cong-∙∙ fold⋁ (λ j → inr (σ₁ b j))
                        (sym (push tt)) (λ j → inl (σ₁ a j))
             ∙ λ i → (λ j → σ₁ b (j ∧ ~ i))
                   ∙∙ (λ j → σ₁ b (j ∨ ~ i))
                   ∙∙ σ₁ a)

-- We show that η₂ ↦ η₁ (this is easier than η₁ ↦ η₂)
η₂↦η₁ : fst (fst π₃*joinS¹S¹≅π₃*S²) η₂ ≡ η₁
η₂↦η₁ =
  to3ConnectedId (sphereConnected 2)
    (funExt λ { (inl x) → refl
              ; (inr x) → refl
              ; (push a b i) j → main a b j i})
  where
  lem : (a b : S¹)
    → (sym (σ₁ (invLooper (b * invLooper a) * invLooper a)) ≡ σ₁ b)
     × (σ₁ (invLooper (b * invLooper a) * b) ≡ σ₁ a)
  fst (lem a b) =
       cong sym (cong σ₁ (sym (invLooperDistr (b * invLooper a) a))
               ∙ σ-invSphere 0 (b * invLooper a * a))
     ∙ cong σ₁ (sym (assocS¹ b (invLooper a) a)
     ∙ cong (b *_) (commS¹ _ _ ∙ sym (rCancelS¹ a))
     ∙ rUnitS¹ b)
  snd (lem a b) =
    cong σ₁ (cong (_* b) (invLooperDistr b (invLooper a)
           ∙ cong (invLooper b *_) (invSphere² 1 a)
           ∙ commS¹ (invLooper b) a)
           ∙ sym (assocS¹ a (invLooper b) b)
           ∙ cong (a *_) (commS¹ _ _ ∙ sym (rCancelS¹ b))
           ∙ rUnitS¹ a)

  main : (a b : S¹)
    → cong Hopfσ ((sym (push (b * invLooper a) (invLooper a))
                        ∙ push (b * invLooper a) b))
     ≡ σ₁ b ∙ σ₁ a
  main a b =
      cong-∙ Hopfσ (sym (push (b * invLooper a) (invLooper a)))
                          (push (b * invLooper a) b)
    ∙ cong₂ _∙_ (fst (lem a b)) (snd (lem a b))

-- We show that η₂ ↦ η₃
η₂↦η₃ : invEq (fst π₃*S³≅π₃*joinS¹S¹) η₂ ≡ η₃
η₂↦η₃ =
  to3ConnectedId connS³
   (funExt λ x → sym (joinS¹S¹→S³σ≡ (fst η₂-raw x))
                ∙ lem x)
  where
  joinS¹S¹→S³σ : join S¹ S¹ → S₊ 3
  joinS¹S¹→S³σ (inl x) = north
  joinS¹S¹→S³σ (inr x) = north
  joinS¹S¹→S³σ (push a b i) = σ₂ (S¹×S¹→S² a b) i

  joinS¹S¹→S³σ≡ : (x : _) → joinS¹S¹→S³σ x ≡ joinS¹S¹→S³ x
  joinS¹S¹→S³σ≡ (inl x) = refl
  joinS¹S¹→S³σ≡ (inr x) = merid north
  joinS¹S¹→S³σ≡ (push a b i) j =
    compPath-filler (merid (S¹×S¹→S² a b)) (sym (merid north)) (~ j) i

  lem : (x : _) → joinS¹S¹→S³σ (fst η₂-raw x) ≡ fst η₃-raw x
  lem (inl x) = refl
  lem (inr x) = refl
  lem (push a b i) j = main j i
    where
    left-lem : σ₂ (S¹×S¹→S² (b * invLooper a) (invLooper a))
             ≡ σ₂ (S¹×S¹→S² a b)
    left-lem = cong σ₂ (S¹×S¹→S²-Distr b (invLooper a)
             ∙ sym (S¹×S¹→S²-antiComm a b))

    right-lem : σ₂ (S¹×S¹→S² (b * invLooper a) b) ≡ sym (σ₂ (S¹×S¹→S² a b))
    right-lem =
         cong σ₂ ((cong (λ x → S¹×S¹→S² x b) (commS¹ b (invLooper a))
                 ∙ S¹×S¹→S²-Distr (invLooper a) b)
                 ∙∙ S¹×S¹→S²-antiComm (invLooper a) b
                 ∙∙ invSusp∘S¹×S¹→S² b (invLooper a))
      ∙∙ σ-invSphere 1 (S¹×S¹→S² b (invLooper a))
      ∙∙ cong (sym ∘ σ₂) (sym (S¹×S¹→S²-antiComm a b))

    main : cong (joinS¹S¹→S³σ ∘ fst η₂-raw) (push a b)
        ≡ sym (σ₂ (S¹×S¹→S² a b)) ∙ sym (σ₂ (S¹×S¹→S² a b))
    main = cong-∙ joinS¹S¹→S³σ
            (sym (push (b * invLooper a) (invLooper a)))
            (push (b * invLooper a) b)
         ∙ cong₂ _∙_ (cong sym left-lem) right-lem

-- We show that η₄ ↦ η₃ (this is easier than η₃ ↦ η₄)
η₄↦η₃ : fst (fst π₃S³≅π₃*S³) η₄ ≡ η₃
η₄↦η₃ = IsGroupHom.pres· (snd π₃S³≅π₃*S³)
            (-π' 2 ∣ idfun∙ (S₊∙ 3) ∣₂) (-π' 2 ∣ idfun∙ (S₊∙ 3) ∣₂)
       ∙ cong₂ _+π₃*_ gen↦η₃/2 gen↦η₃/2
       ∙ η₃/2+η₃/2≡η₃
  where
  _+π₃*_ : fst π₃*S³ → fst π₃*S³ → fst π₃*S³
  _+π₃*_ = GroupStr._·_ (snd π₃*S³)

  η₃-raw/2 : (join S¹ S¹ , inl base) →∙ S₊∙ 3
  fst η₃-raw/2 (inl x) = north
  fst η₃-raw/2 (inr x) = north
  fst η₃-raw/2 (push a b i) = σ₂ (S¹×S¹→S² a b) (~ i)
  snd η₃-raw/2 = refl

  η₃/2 : π₃*S³ .fst
  η₃/2 = ∣ η₃-raw/2 ∣₂

  gen↦η₃/2 : fst (fst π₃S³≅π₃*S³) (-π' 2 ∣ idfun∙ (S₊∙ 3) ∣₂) ≡ η₃/2
  gen↦η₃/2 =
    to3ConnectedId connS³
      (funExt λ { (inl x) → refl
                ; (inr x) → refl
                ; (push a b i) → refl})

  η₃/2+η₃/2≡η₃ : η₃/2 +π₃* η₃/2 ≡ η₃
  η₃/2+η₃/2≡η₃ =
    to3ConnectedId connS³
      (funExt λ { (inl x) → refl
                ; (inr x) → refl
                ; (push a b i) → λ j → lem a b j i})
    where
    lem : (a b : S¹) → cong (fst (η₃-raw/2 +join η₃-raw/2)) (push a b)
                      ≡ cong (fst η₃-raw) (push a b)
    lem a b = (λ i → cong-∙ (fst η₃-raw/2) (push a b) (sym (push base b)) i
                   ∙∙ rUnit refl (~ i)
                   ∙∙ cong-∙∙ (fst η₃-raw/2)
                        (push base base) (sym (push a base)) (push a b) i)
           ∙∙ (λ i → (sym (σ₂ (S¹×S¹→S² a b)) ∙ rCancel (merid north) i)
                   ∙∙ refl
                   ∙∙ (sym (rCancel (merid north) i)
                   ∙∙ (cong σ₂ (S¹×S¹→S²rUnit a) ∙ rCancel (merid north)) i
                   ∙∙ sym (σ₂ (S¹×S¹→S² a b))))
           ∙∙ ((λ i → rUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i)
                    ∙∙ refl
                    ∙∙ lUnit (sym (σ₂ (S¹×S¹→S² a b))) (~ i))
             ∙ λ i → (λ j → σ₂ (S¹×S¹→S² a b) (i ∨ ~ j))
                   ∙∙ (λ j → σ₂ (S¹×S¹→S² a b) (i ∧ ~ j))
                   ∙∙ sym (σ₂ (S¹×S¹→S² a b)))

-- Agda is very keen on expanding things, so we make an abstract
-- summary of the main lemmas above
abstract
  π₃S²≅π₃*S²-abs : GroupEquiv π₃S² π₃*S²
  π₃S²≅π₃*S²-abs = π₃S²→π₃*S²

  π₃*S²≅π₃*joinS¹S¹-abs : GroupEquiv π₃*S² π₃*joinS¹S¹
  π₃*S²≅π₃*joinS¹S¹-abs = invGroupEquiv π₃*joinS¹S¹≅π₃*S²

  π₃*joinS¹S¹≅π₃*S³-abs : GroupEquiv π₃*joinS¹S¹ π₃*S³
  π₃*joinS¹S¹≅π₃*S³-abs = invGroupEquiv π₃*S³≅π₃*joinS¹S¹

  π₃*S³≅π₃*S³-abs : GroupEquiv π₃*S³ π₃S³
  π₃*S³≅π₃*S³-abs = invGroupEquiv π₃S³≅π₃*S³

  -- stated in terms of (n : ℕ) to prevent normalisation
  π₃'S³≅ℤ-abs : (n : ℕ) → GroupEquiv (π'Gr n (S₊∙ (suc n))) ℤ
  π₃'S³≅ℤ-abs n = GroupIso→GroupEquiv (πₙ'Sⁿ≅ℤ n)

  η↦η₁-abs : fst (fst π₃S²≅π₃*S²-abs) η ≡ η₁
  η↦η₁-abs = η↦η₁

  η₁↦η₂-abs : fst (fst π₃*S²≅π₃*joinS¹S¹-abs) η₁ ≡ η₂
  η₁↦η₂-abs = cong (fst (fst π₃*S²≅π₃*joinS¹S¹-abs)) (sym η₂↦η₁)
              ∙ secEq (fst π₃*S²≅π₃*joinS¹S¹-abs) η₂

  η₂↦η₃-abs : fst (fst π₃*joinS¹S¹≅π₃*S³-abs) η₂ ≡ η₃
  η₂↦η₃-abs = η₂↦η₃

  η₃↦η₄-abs : fst (fst π₃*S³≅π₃*S³-abs) η₃ ≡ η₄
  η₃↦η₄-abs = cong (invEq (fst π₃S³≅π₃*S³)) (sym η₄↦η₃)
                  ∙ retEq (fst π₃S³≅π₃*S³) η₄

  gen↦1 : (n : ℕ) → fst (fst (π₃'S³≅ℤ-abs n)) ∣ idfun∙ (S₊∙ (suc n)) ∣₂ ≡ 1
  gen↦1 = πₙ'Sⁿ≅ℤ-idfun∙

-- We finally prove that η₄ ↦ -2
abstract
  η₄↦-2 : fst (fst (π₃'S³≅ℤ-abs 2)) η₄ ≡ -2
  η₄↦-2 = speedUp (∣ idfun∙ (S₊∙ 3) ∣₂) (gen↦1 2)
    where
    speedUp : (x : _)
      → fst (fst (π₃'S³≅ℤ-abs (suc (suc zero)))) x ≡ (pos (suc zero))
      → (fst (fst (π₃'S³≅ℤ-abs 2))) (·π' 2 (-π' 2 x) (-π' 2 x)) ≡ -2
    speedUp x p =
        IsGroupHom.pres· (π₃'S³≅ℤ-abs 2 .snd)
              (-π' 2 x) (-π' 2 x)
      ∙ cong (λ x → x +Z x)
        (IsGroupHom.presinv (π₃'S³≅ℤ-abs 2 .snd) x ∙ cong (inv (ℤ .snd)) p)

-- Puting it all together, we get our group iso π₃(S²) ≅ ℤ
π₃'S²≅ℤ : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤ
π₃'S²≅ℤ =
  compGroupEquiv
    π₃S²≅π₃*S²-abs
    (compGroupEquiv
      π₃*S²≅π₃*joinS¹S¹-abs
      (compGroupEquiv
        π₃*joinS¹S¹≅π₃*S³-abs
        (compGroupEquiv π₃*S³≅π₃*S³-abs
          (π₃'S³≅ℤ-abs 2))))

-- ... which takes η to -2
η↦-2 : fst (fst π₃'S²≅ℤ) η ≡ - 2
η↦-2 =
    cong (fst (fst (π₃'S³≅ℤ-abs 2)))
      (cong (fst π₃*S³≅π₃*S³-abs .fst)
        (cong (fst π₃*joinS¹S¹≅π₃*S³-abs .fst)
          (cong (fst (fst π₃*S²≅π₃*joinS¹S¹-abs))
            η↦η₁-abs
          ∙ η₁↦η₂-abs)
        ∙ η₂↦η₃-abs)
     ∙ η₃↦η₄-abs)
  ∙ η₄↦-2

-- We combine this with the rest of the main conclusions of chapters
-- 1-3 in Brunerie's thesis
BrunerieIso : GroupEquiv (π'Gr 3 (S₊∙ 3)) (ℤ/ 2)
BrunerieIso =
  compGroupEquiv
    (compGroupEquiv π₄S³≅π₃coFib-fold∘W∙
    (invGroupEquiv
      (GroupEquiv-abstractℤ/abs-gen
        (π'Gr 2 (S₊∙ 3)) (π'Gr 2 (S₊∙ 2)) (π'Gr 2 coFib-fold∘W∙)
          (invGroupEquiv (π₃'S³≅ℤ-abs 2))
          (invGroupEquiv π₃'S²≅ℤ)
          (π'∘∙Hom 2 (fold∘W , refl))
          _
          S³→S²→Pushout→Unit 2
            (cong abs (cong (invEq (invEquiv (fst π₃'S²≅ℤ))
                     ∘ sMap (_∘∙_ (fold∘W , refl)))
                      (sym (cong (invEq (fst (π₃'S³≅ℤ-abs 2))) (gen↦1 2))
                    ∙ retEq (fst (π₃'S³≅ℤ-abs 2)) ∣ idfun∙ (S₊∙ 3) ∣₂))
           ∙ cong abs η↦-2))))
           (abstractℤ/≅ℤ 2)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Kripke-style semantics with contexts as concrete worlds, and glueing for α and ▻.
-- Hilbert-style syntax.

module BasicIPC.Semantics.KripkeConcreteGluedHilbert where

open import BasicIPC.Syntax.Common public
open import Common.Semantics public

open ConcreteWorlds (Ty) public

-- Partial intuitionistic Kripke models with explicit syntax.

record Model : Set₁ where
  infix 3 _⊩ᵅ_ _[⊢]_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : World → Atom → Set
    mono⊩ᵅ : ∀ {P w w′} → w ≤ w′ → w ⊩ᵅ P → w′ ⊩ᵅ P

    -- Hilbert-style syntax representation; monotonic.
    _[⊢]_   : Cx Ty → Ty → Set
    mono[⊢] : ∀ {A Γ Γ′}  → Γ ⊆ Γ′ → Γ [⊢] A → Γ′ [⊢] A
    [var]    : ∀ {A Γ}     → A ∈ Γ → Γ [⊢] A
    [app]    : ∀ {A B Γ}   → Γ [⊢] A ▻ B → Γ [⊢] A → Γ [⊢] B
    [ci]     : ∀ {A Γ}     → Γ [⊢] A ▻ A
    [ck]     : ∀ {A B Γ}   → Γ [⊢] A ▻ B ▻ A
    [cs]     : ∀ {A B C Γ} → Γ [⊢] (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
    [cpair]  : ∀ {A B Γ}   → Γ [⊢] A ▻ B ▻ A ∧ B
    [cfst]   : ∀ {A B Γ}   → Γ [⊢] A ∧ B ▻ A
    [csnd]   : ∀ {A B Γ}   → Γ [⊢] A ∧ B ▻ B
    [unit]   : ∀ {Γ}       → Γ [⊢] ⊤

    -- NOTE: [lam] is necessary to give meaning to Gentzen-style syntax.
    [lam] : ∀ {A B Γ} → Γ , A [⊢] B → Γ [⊢] A ▻ B

  infix 3 _[⊢]⋆_
  _[⊢]⋆_ : Cx Ty → Cx Ty → Set
  Γ [⊢]⋆ ∅     = 𝟙
  Γ [⊢]⋆ Ξ , A = Γ [⊢]⋆ Ξ × Γ [⊢] A

open Model {{…}} public

-- Forcing in a particular world of a particular model.

module _ {{_ : Model}} where
  infix 3 _⊩_
  _⊩_ : World → Ty → Set
  w ⊩ α P   = Glue (unwrap w [⊢] α P) (w ⊩ᵅ P)
  w ⊩ A ▻ B = Glue (unwrap w [⊢] (A ▻ B)) (∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B)
  w ⊩ A ∧ B = w ⊩ A × w ⊩ B
  w ⊩ ⊤    = 𝟙

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Cx Ty → Set
  w ⊩⋆ ∅     = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

-- Monotonicity with respect to context inclusion.

module _ {{_ : Model}} where
  mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
  mono⊩ {α P}   ξ s = mono[⊢] (unwrap≤ ξ) (syn s) ⅋ mono⊩ᵅ ξ (sem s)
  mono⊩ {A ▻ B} ξ s = mono[⊢] (unwrap≤ ξ) (syn s) ⅋ λ ξ′ → sem s (trans≤ ξ ξ′)
  mono⊩ {A ∧ B} ξ s = mono⊩ {A} ξ (π₁ s) , mono⊩ {B} ξ (π₂ s)
  mono⊩ {⊤}    ξ s = ∙

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     ξ ∙        = ∙
  mono⊩⋆ {Ξ , A} ξ (ts , t) = mono⊩⋆ {Ξ} ξ ts , mono⊩ {A} ξ t

-- Extraction of syntax representation in a particular model.

module _ {{_ : Model}} where
  reifyʳ : ∀ {A w} → w ⊩ A → unwrap w [⊢] A
  reifyʳ {α P}   s = syn s
  reifyʳ {A ▻ B} s = syn s
  reifyʳ {A ∧ B} s = [app] ([app] [cpair] (reifyʳ {A} (π₁ s))) (reifyʳ {B} (π₂ s))
  reifyʳ {⊤}    s = [unit]

  reifyʳ⋆ : ∀ {Ξ w} → w ⊩⋆ Ξ → unwrap w [⊢]⋆ Ξ
  reifyʳ⋆ {∅}     ∙        = ∙
  reifyʳ⋆ {Ξ , A} (ts , t) = reifyʳ⋆ ts , reifyʳ t

-- Useful theorems in functional form.

module _ {{_ : Model}} where
  [multicut] : ∀ {Ξ A Γ} → Γ [⊢]⋆ Ξ → Ξ [⊢] A → Γ [⊢] A
  [multicut] {∅}     ∙        u = mono[⊢] bot⊆ u
  [multicut] {Ξ , B} (ts , t) u = [app] ([multicut] ts ([lam] u)) t

  [pair] : ∀ {A B Γ} → Γ [⊢] A → Γ [⊢] B → Γ [⊢] A ∧ B
  [pair] t u = [app] ([app] [cpair] t) u

  [fst] : ∀ {A B Γ} → Γ [⊢] A ∧ B → Γ [⊢] A
  [fst] t = [app] [cfst] t

  [snd] : ∀ {A B Γ} → Γ [⊢] A ∧ B → Γ [⊢] B
  [snd] t = [app] [csnd] t

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B w} → w ⊩ A ▻ B → w ⊩ A → w ⊩ B
  s ⟪$⟫ a = sem s refl≤ a

  ⟪K⟫ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A
  ⟪K⟫ {A} a = [app] [ck] (reifyʳ a) ⅋ λ ξ →
                K (mono⊩ {A} ξ a)

  ⟪S⟫ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ A ▻ B → w ⊩ A → w ⊩ C
  ⟪S⟫ s₁ s₂ a = (s₁ ⟪$⟫ a) ⟪$⟫ (s₂ ⟪$⟫ a)

  ⟪S⟫′ : ∀ {A B C w} → w ⊩ A ▻ B ▻ C → w ⊩ (A ▻ B) ▻ A ▻ C
  ⟪S⟫′ {A} {B} {C} s₁ = [app] [cs] (syn s₁) ⅋ λ ξ s₂ →
                          [app] ([app] [cs] (mono[⊢] (unwrap≤ ξ) (syn s₁))) (syn s₂) ⅋ λ ξ′ →
                            ⟪S⟫ (mono⊩ {A ▻ B ▻ C} (trans≤ ξ ξ′) s₁) (mono⊩ {A ▻ B} ξ′ s₂)

  _⟪,⟫′_ : ∀ {A B w} → w ⊩ A → w ⊩ B ▻ A ∧ B
  _⟪,⟫′_ {A} a = [app] [cpair] (reifyʳ a) ⅋ λ ξ →
                   _,_ (mono⊩ {A} ξ a)

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

  _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
  (s₁ ⟦$⟧ s₂) γ = s₁ γ ⟪$⟫ s₂ γ

  ⟦K⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B ▻ A
  ⟦K⟧ {A} {B} a γ = ⟪K⟫ {A} {B} (a γ)

  ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
  ⟦S⟧ s₁ s₂ a γ = ⟪S⟫ (s₁ γ) (s₂ γ) (a γ)

  _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
  (a ⟦,⟧ b) γ = a γ , b γ

  ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
  ⟦π₁⟧ s γ = π₁ (s γ)

  ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
  ⟦π₂⟧ s γ = π₂ (s γ)

ext: agda

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import HoTT
open import cohomology.Theory

{- Ordinary cohomology groups of the n-torus Tⁿ = (S¹)ⁿ.
 - We have Cᵏ(Tⁿ) == C⁰(S⁰)^(n choose' k) where _choose'_ defined as below.
 - This argument could give Cᵏ((Sᵐ)ⁿ) with a little more work. -}

module cohomology.Torus {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cohomology.Sphere OT
open import cohomology.SphereProduct cohomology-theory

{- Almost n choose k, but with n choose' O = 0 for any n. -}
_choose'_ : ℕ → ℤ → ℕ
n choose' negsucc _ = 0
n choose' pos O = 0
n choose' pos (S O) = n
O choose' pos (S (S k)) = 0
S n choose' pos (S (S k)) = (n choose' (pos (S (S k)))) + (n choose' (pos (S k)))

_-⊙Torus : ℕ → Ptd₀
O -⊙Torus = ⊙Unit
(S n) -⊙Torus = ⊙S¹ ⊙× (n -⊙Torus)

C-nTorus : (k : ℤ) (n : ℕ)
  → C k (⊙Lift (n -⊙Torus)) ≃ᴳ C 0 (⊙Lift ⊙S⁰) ^ᴳ (n choose' k)

C-nTorus (negsucc k) O = lift-iso ∘eᴳ trivial-iso-0ᴳ (C-Unit (negsucc k))

C-nTorus (negsucc k) (S n) =
  C (negsucc k) (⊙Lift (S n -⊙Torus))
    ≃ᴳ⟨ C-emap (negsucc k) (⊙lift-equiv ⊙∘e ⊙×-emap (⊙ide _) ⊙lower-equiv) ⟩
  C (negsucc k) (⊙S¹ ⊙× ⊙Lift (n -⊙Torus))
    ≃ᴳ⟨ C-Sphere× (negsucc k) 1 (⊙Lift (n -⊙Torus)) ⟩
  C (negsucc k) (⊙Lift ⊙S¹) ×ᴳ (C (negsucc k) (⊙Lift (n -⊙Torus)) ×ᴳ C (negsucc k) (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-emap (trivial-iso-0ᴳ (C-Sphere-≠-is-trivial (negsucc k) 1 (ℤ-negsucc≠pos _ _))) (idiso _) ⟩
  0ᴳ ×ᴳ (C (negsucc k) (⊙Lift (n -⊙Torus)) ×ᴳ C (negsucc k) (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-unit-l _ ⟩
  C (negsucc k) (⊙Lift (n -⊙Torus)) ×ᴳ C (negsucc k) (⊙Susp (⊙Lift (n -⊙Torus)))
    ≃ᴳ⟨ ×ᴳ-emap
          (lower-iso ∘eᴳ C-nTorus (negsucc k) n)
          (C-nTorus (negsucc (S k)) n ∘eᴳ C-Susp (negsucc (S k)) (⊙Lift (n -⊙Torus))) ⟩
  0ᴳ ×ᴳ Lift-group 0ᴳ
    ≃ᴳ⟨ ×ᴳ-unit-l (Lift-group 0ᴳ) ⟩
  Lift-group 0ᴳ
    ≃ᴳ∎

C-nTorus (pos O) O = lift-iso ∘eᴳ trivial-iso-0ᴳ (C-Unit 0)

C-nTorus (pos O) (S n) =
  C 0 (⊙Lift (S n -⊙Torus))
    ≃ᴳ⟨ C-emap 0 (⊙lift-equiv ⊙∘e ⊙×-emap (⊙ide _) ⊙lower-equiv) ⟩
  C 0 (⊙S¹ ⊙× ⊙Lift (n -⊙Torus))
    ≃ᴳ⟨ C-Sphere× 0 1 (⊙Lift (n -⊙Torus)) ⟩
  C 0 (⊙Lift ⊙S¹) ×ᴳ (C 0 (⊙Lift (n -⊙Torus)) ×ᴳ C 0 (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-emap (trivial-iso-0ᴳ (C-Sphere-≠-is-trivial 0 1 (pos-≠ (ℕ-O≠S _)))) (idiso _) ⟩
  0ᴳ ×ᴳ (C 0 (⊙Lift (n -⊙Torus)) ×ᴳ C 0 (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-unit-l _ ⟩
  C 0 (⊙Lift (n -⊙Torus)) ×ᴳ C 0 (⊙Susp (⊙Lift (n -⊙Torus)))
    ≃ᴳ⟨ ×ᴳ-emap
          (lower-iso ∘eᴳ C-nTorus 0 n)
          (C-nTorus -1 n ∘eᴳ C-Susp -1 (⊙Lift (n -⊙Torus))) ⟩
  0ᴳ ×ᴳ Lift-group 0ᴳ
    ≃ᴳ⟨ ×ᴳ-unit-l _ ⟩
  Lift-group 0ᴳ
    ≃ᴳ∎

C-nTorus (pos (S O)) O = lift-iso ∘eᴳ trivial-iso-0ᴳ (C-Unit 1)

C-nTorus (pos (S O)) (S n) =
  C 1 (⊙Lift (S n -⊙Torus))
    ≃ᴳ⟨ C-emap 1 (⊙lift-equiv ⊙∘e ⊙×-emap (⊙ide _) ⊙lower-equiv) ⟩
  C 1 (⊙S¹ ⊙× ⊙Lift (n -⊙Torus))
    ≃ᴳ⟨ C-Sphere× 1 1 (⊙Lift (n -⊙Torus)) ⟩
  C 1 (⊙Lift ⊙S¹) ×ᴳ (C 1 (⊙Lift (n -⊙Torus)) ×ᴳ C 1 (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-emap (C-Sphere-diag 1)
          ( ×ᴳ-unit-r _
        ∘eᴳ ×ᴳ-emap
              (C-nTorus 1 n)
              (lower-iso
                ∘eᴳ C-nTorus 0 n
                ∘eᴳ C-Susp 0 (⊙Lift (n -⊙Torus)))) ⟩
  C 0 (⊙Lift ⊙S⁰) ×ᴳ (C 0 (⊙Lift ⊙S⁰) ^ᴳ n)
    ≃ᴳ∎

C-nTorus (pos (S (S k))) O = lift-iso ∘eᴳ trivial-iso-0ᴳ (C-Unit (pos (S (S k))))

C-nTorus (pos (S (S k))) (S n) =
  C (pos (S (S k))) (⊙Lift (S n -⊙Torus))
    ≃ᴳ⟨ C-emap (pos (S (S k))) (⊙lift-equiv ⊙∘e ⊙×-emap (⊙ide _) ⊙lower-equiv) ⟩
  C (pos (S (S k))) (⊙S¹ ⊙× ⊙Lift (n -⊙Torus))
    ≃ᴳ⟨ C-Sphere× (pos (S (S k))) 1 (⊙Lift (n -⊙Torus)) ⟩
  C (pos (S (S k))) (⊙Lift ⊙S¹) ×ᴳ (C (pos (S (S k))) (⊙Lift (n -⊙Torus)) ×ᴳ C (pos (S (S k))) (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-emap (trivial-iso-0ᴳ (C-Sphere-≠-is-trivial (pos (S (S k))) 1 (pos-≠ (ℕ-S-≠ (ℕ-S≠O k))))) (idiso _) ⟩
  0ᴳ ×ᴳ (C (pos (S (S k))) (⊙Lift (n -⊙Torus)) ×ᴳ C (pos (S (S k))) (⊙Susp (⊙Lift (n -⊙Torus))))
    ≃ᴳ⟨ ×ᴳ-unit-l _ ⟩
  C (pos (S (S k))) (⊙Lift (n -⊙Torus)) ×ᴳ C (pos (S (S k))) (⊙Susp (⊙Lift (n -⊙Torus)))
    ≃ᴳ⟨ ×ᴳ-emap
        (C-nTorus (pos (S (S k))) n)
        (C-nTorus (pos (S k)) n ∘eᴳ C-Susp (pos (S k)) (⊙Lift (n -⊙Torus))) ⟩
  (C 0 (⊙Lift ⊙S⁰) ^ᴳ (n choose' pos (S (S k)))) ×ᴳ (C 0 (⊙Lift ⊙S⁰) ^ᴳ (n choose' pos (S k)))
    ≃ᴳ⟨ ^ᴳ-+ (C 0 (⊙Lift ⊙S⁰)) (n choose' pos (S (S k))) (n choose' pos (S k)) ⁻¹ᴳ ⟩
  C 0 (⊙Lift ⊙S⁰) ^ᴳ (S n choose' pos (S (S k)))
    ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.Lattice (l : Lattice) where

open Lattice l
open import Algebra.Structures
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Data.Function
open import Data.Product

∧-idempotent : Idempotent _∧_
∧-idempotent x = begin
  x ∧ x            ≈⟨ refl ⟨ ∧-pres-≈ ⟩ sym (proj₁ absorptive _ _) ⟩
  x ∧ (x ∨ x ∧ x)  ≈⟨ proj₂ absorptive _ _ ⟩
  x                ∎

∨-idempotent : Idempotent _∨_
∨-idempotent x = begin
  x ∨ x      ≈⟨ refl ⟨ ∨-pres-≈ ⟩ sym (∧-idempotent _) ⟩
  x ∨ x ∧ x  ≈⟨ proj₁ absorptive _ _ ⟩
  x          ∎

-- The dual construction is also a lattice.

∧-∨-isLattice : IsLattice _≈_ _∧_ _∨_
∧-∨-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ∧-comm
  ; ∨-assoc       = ∧-assoc
  ; ∨-pres-≈      = ∧-pres-≈
  ; ∧-comm        = ∨-comm
  ; ∧-assoc       = ∨-assoc
  ; ∧-pres-≈      = ∨-pres-≈
  ; absorptive    = swap absorptive
  }

∧-∨-lattice : Lattice
∧-∨-lattice = record
  { _∧_       = _∨_
  ; _∨_       = _∧_
  ; isLattice = ∧-∨-isLattice
  }

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- Code related to the paper "Bag Equivalence via a Proof-Relevant
-- Membership Relation"
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- Note that the code does not follow the paper exactly. For instance,
-- many definitions are universe-polymorphic, and in some cases where
-- the paper contains both a specialised and a more general definition
-- the code only contains the more general one. The code has also been
-- changed after the paper was published.

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

module README.Bag-equivalence where

------------------------------------------------------------------------
-- 2: Brief Introduction to Agda

-- The prelude, containing List, ℕ, Fin, ⊥, ⊤, _⊎_ (written as _+_ in
-- the paper), ∃, and _×_.

import Prelude

-- Some list functions: length and index (called lookup in the paper).

import List

-- Logical equivalences: _⇔_.

import Logical-equivalence

-- Bijections: _↔_.

import Bijection

-- Equality: _≡_.

import Equality.Propositional

-- The K rule, and a proof showing that it implies proof-irrelevance.

import Equality

-- Bijectional reasoning combinators (more general than those in the
-- paper): inverse (written as sym in the paper), _□, and _↔⟨_⟩_.

import Function-universe

------------------------------------------------------------------------
-- 3: Bag Equivalence for Lists

-- Any, _∈_, and the two definitions of bag equivalence.

import Bag-equivalence

------------------------------------------------------------------------
-- 4: Bijectional Reasoning

-- Definitions of map, concat and _>>=_ (the latter as part of a monad
-- instance).

import List

-- Algebraic properties of type constructors (like ⊥ ⊎ A ↔ A).

import Function-universe
import Fin

-- All the main lemmas from this section, including
-- >>=-left-distributive.

import Bag-equivalence

------------------------------------------------------------------------
-- 5: The Definitions Are Equivalent

-- The equivalence proof.

import Bag-equivalence

-- There are infinitely many proofs of ℕ ≡ ℕ in homotopy type theory.

import Univalence-axiom

------------------------------------------------------------------------
-- 6: Bag Equivalence for Arbitrary Containers

-- Containers, including Any, _∈_, the two definitions of bag
-- equivalence, and a proof showing that the two definitions are
-- logically equivalent.
--
-- There is also a proof which shows that the definitions are
-- isomorphic (assuming extensionality), if "bijection" is replaced by
-- the logically equivalent concept of "(weak) equivalence" in the
-- definitions of bag equivalence.

import Container
import Equivalence

-- The List, Stream and Tree containers. It is shown that the general
-- definition of bag equivalence for containers, instantiated with the
-- List container, is equivalent (in a certain sense) to the list-only
-- definition given above.

import Container.List
import Container.Stream
import Container.Tree

------------------------------------------------------------------------
-- 7: More Bijectional Reasoning

-- Three implementations of tree sort are provided.

-- 1) An implementation of tree sort, formally proved to return a
--    permutation of the input.

import Tree-sort.Partial
import Tree-sort.Examples

-- 2) An implementation of tree sort, formally proved to return a
--    /sorted/ permutation of the input.

import Tree-sort.Full
import Tree-sort.Examples

-- 3) An implementation of tree sort which uses containers to
--    represent trees and lists.
--
--    In the module Tree-sort.Full indexed types are used to enforce
--    sortedness, but this development uses non-indexed containers, so
--    sortedness is not enforced.
--
--    The implementation using containers has the advantage of uniform
--    definitions of Any/membership/bag equivalence, but the other
--    implementations use more direct definitions and are perhaps a
--    bit "leaner".

import Container.Tree
import Container.Tree-sort
import Container.Tree-sort.Example

------------------------------------------------------------------------
-- 8: Set Equivalence, Subsets and Subbags

-- Injections: _↣_.

import Injection

-- The general definition of set and bag equivalence and the subset
-- and subbag preorders, as well as preservation lemmas such as
-- >>=-cong.

import Bag-equivalence

------------------------------------------------------------------------
-- 9: Related Work

-- One of the definitions of bag equivalence from Coq's standard
-- library has been replicated, and shown to be sound with respect to
-- the other ones.

import Bag-equivalence

------------------------------------------------------------------------
-- 10: Conclusions

-- Two proofs showing that cons is left cancellative, using different
-- definitions of bag equivalence.

import Bag-equivalence

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Cham.Label where

open import Cham.Name

data Label : Set where
  _⁺ : Name → Label
  _⁻ : Name → Label


text:
module prelude where
open import Function using (id; _∘_) public
open import Data.Sum renaming (inj₁ to Σ₁; inj₂ to Σ₂) using (_⊎_) public
open import Data.Product renaming (proj₁ to π₁; proj₂ to π₂) using (Σ; _×_; _,_; ∃; Σ-syntax) public
open import Agda.Builtin.Unit using (⊤; tt) public
open import Data.Empty using (⊥) public
open import Data.Nat as Nat renaming (suc to ℕs; zero to ℕz; _+_ to _ℕ+_) using (ℕ) public
open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_; _≢_; refl; sym; trans; subst) renaming (cong to _⟨$⟩_) public
open Eq.≡-Reasoning using (_≡⟨⟩_; step-≡; _∎) public

postulate
  extensionality : {A : Set} {B : A → Set} {f g : (x : A) → B x}
                 → (∀ x → f x ≡ g x) → f ≡ g
extensionality2 : {A : Set} {B : A → Set} {C : (x : A) → B x → Set} {f g : (x : A) (y : B x) → C x y }
                 → (∀ x y → f x y ≡ g x y) → f ≡ g
extensionality2 λλf≡g = extensionality λ x → extensionality λ y → λλf≡g x y

trans-refl : {A : Set} {x y : A} (p : x ≡ y) → trans p refl ≡ p
trans-refl p rewrite p = refl

subst⋯ : {A : Set} {x y z : A} (P : A → Set) (p : x ≡ y) (q : y ≡ z) (Px : P x)
      → subst P (trans p q) Px ≡ subst P q (subst P p Px)
subst⋯ _ p _ _ rewrite p = refl

_×⁼_ : {A X : Set} {a b : A} {x y : X} → a ≡ b → x ≡ y → (a , x) ≡ (b , y)
_×⁼_ refl refl = refl

_⨄_ : {A B : Set} → (A → Set) → (B → Set) → A ⊎ B → Set
(F ⨄ G) (Σ₁ x) = F x
(F ⨄ G) (Σ₂ y) = G y
_⨃_ _⨉_ : {A B : Set} → (A → Set) → (B → Set) → A × B → Set
F ⨃ G = λ (a , b) → F a ⊎ G b
F ⨉ G = λ (a , b) → F a × G b

_$₁_ : ∀ {A B X : Set} (f : A → B) → A × X → B × X
f $₁ (a , x) = f a , x

_⁻¹ : {A B : Set} → (A → B) → B → Set
_⁻¹ {A} {B} f b = Σ[ a ∈ A ] (f a ≡ b)

uncurry : {a b c : Set} → (a → b → c) → (a × b) → c
uncurry f (a , b) = f a b

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
module Data.Vec.Membership.Propositional.Distinct.Properties where
open import Data.Fin as Fin
open import Relation.Binary.PropositionalEquality as P
open import Data.Vec as Vec using (Vec; [] ; _∷_ ; _++_)
open import Data.Vec.Any
open import Data.Vec.Membership.Propositional.Distinct
open import Data.Vec.Membership.Propositional.Disjoint renaming (Disjoint to _⋈_)
open import Data.Vec.Membership.Propositional.Properties
open import Data.Vec.Membership.Propositional
open import Data.Product
open import Data.Empty using (⊥-elim)
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)

distinct-++ˡ : ∀ {a}{A : Set a}{m n} (xs : Vec A m){ys : Vec A n} → Distinct (xs ++ ys) → Distinct xs
distinct-++ˡ [] dis = distinct-[]
distinct-++ˡ (x ∷ xs) (.x distinct-∷ dis by x∉xsys) = x distinct-∷ distinct-++ˡ xs dis by λ x∈xs → x∉xsys (∈-++⁺ˡ x∈xs)

distinct-++ʳ : ∀ {a}{A : Set a}{m n} (xs : Vec A m) {ys : Vec A n} → Distinct (xs ++ ys) → Distinct ys
distinct-++ʳ [] dys = dys
distinct-++ʳ (x ∷ xs) (.x distinct-∷ dxsys by _) = distinct-++ʳ xs dxsys

distinct-++→disjoint : ∀ {a}{A : Set a}{m n} (xs : Vec A m) {ys : Vec A n} → Distinct (xs ++ ys) → xs ⋈ ys
distinct-++→disjoint [] dxsys {z} () z∈ys
distinct-++→disjoint (x ∷ xs) (.x distinct-∷ dxsys by x∉xsys) {.x} (here refl) x∈ys = x∉xsys (∈-++⁺ʳ xs x∈ys)
distinct-++→disjoint (x ∷ xs) (.x distinct-∷ dxsys by x₁) {z} (there z∈xs) z∈ys = distinct-++→disjoint xs dxsys z∈xs z∈ys

⋈→distinct-++ : ∀ {a}{A : Set a}{m n}{xs : Vec A m}{ys : Vec A n} → Distinct xs → Distinct ys → xs ⋈ ys → Distinct (xs ++ ys)
⋈→distinct-++ {xs = []}  _ dys _ = dys
⋈→distinct-++ {xs = x ∷ xs} (.x distinct-∷ dxs by x∉xs) dys xxs⋈ys = x distinct-∷ ⋈→distinct-++ dxs dys (xxs⋈ys ∘ there)
  by λ x∈xs++ys → xxs⋈ys (here P.refl) (x∈xs++ys→x∉xs→x∈ys xs x∈xs++ys x∉xs)
  where
    x∈xs++ys→x∉xs→x∈ys : ∀ {a} {A : Set a} {m n} (xs : Vec A m){ys : Vec A n} →
                       ∀ {x} → x ∈ xs ++ ys → x ∉ xs → x ∈ ys
    x∈xs++ys→x∉xs→x∈ys [] x∈ys _ = x∈ys
    x∈xs++ys→x∉xs→x∈ys (x ∷ xs) (here refl) x∉xs = ⊥-elim (x∉xs (here refl))
    x∈xs++ys→x∉xs→x∈ys (x ∷ xs) (there x∈xsys) x∉xs = x∈xs++ys→x∉xs→x∈ys xs x∈xsys (x∉xs ∘ there)

distinct-++⇔⋈ : ∀ {a}{A : Set a}{m n} {xs : Vec A m}{ys : Vec A n} →
  Distinct (xs ++ ys) ⇔ (Distinct xs × Distinct ys × xs ⋈ ys)
distinct-++⇔⋈ = equivalence to from
  where
    open import Data.Nat.Properties

    to : ∀ {a}{A : Set a} {m n} {xs : Vec A m}{ys : Vec A n} →
         Distinct (xs ++ ys) → (Distinct xs × Distinct ys × xs ⋈ ys)
    to {xs = xs} dxsys = distinct-++ˡ xs dxsys , distinct-++ʳ xs dxsys , distinct-++→disjoint xs dxsys
    from : ∀ {a}{A : Set a} {m n} {xs : Vec A m}{ ys : Vec A n} →
         (Distinct xs × Distinct ys × xs ⋈ ys) → Distinct (xs ++ ys)
    from (dxs , dys , xs⋈ys) = ⋈→distinct-++ dxs dys xs⋈ys

private
  lookup-∈ : ∀ {a n}{A : Set a} i (xs : Vec A n) → Vec.lookup i xs ∈ xs
  lookup-∈ () []
  lookup-∈ zero (x ∷ xs) = here P.refl
  lookup-∈ (suc i) (x ∷ xs) = there (lookup-∈ i xs)

lookup-injective : ∀ {a n}{A : Set a} {xs : Vec A n}{i j} →
  Distinct xs → Vec.lookup i xs ≡ Vec.lookup j xs → i ≡ j
lookup-injective {i = ()} {j} distinct-[] _
lookup-injective {i = zero} {zero} (x distinct-∷ dxs by x∉xs) eq = P.refl
lookup-injective {i = suc i} {suc j} (x distinct-∷ dxs by x∉xs) eq = P.cong Fin.suc (lookup-injective dxs eq)
lookup-injective {xs = _ ∷ xs} {i = zero} {suc j} (x distinct-∷ dxs by x∉xs) eq rewrite eq =
  ⊥-elim (x∉xs (lookup-∈ j xs))
lookup-injective {xs = _ ∷ xs} {i = suc i} {zero} (x distinct-∷ dxs by x∉xs) eq  rewrite P.sym eq = ⊥-elim (x∉xs (lookup-∈ i xs))

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
module Utils where

open import Data.Fin using (Fin)
import      Data.Fin as F
open import Data.Nat

data Fromℕ (n : ℕ) : ℕ → Set where
  yes : (m : Fin n) → Fromℕ n (F.toℕ m)
  no  : (m : ℕ)     → Fromℕ n (n + m)

fromℕ : ∀ n m → Fromℕ n m
fromℕ zero m = no m
fromℕ (suc n) zero = yes F.zero
fromℕ (suc n) (suc m) with fromℕ n m
fromℕ (suc n) (suc .(F.toℕ m)) | yes m = yes (F.suc m)
fromℕ (suc n) (suc .(n + m))   | no  m = no m

max_stars_repo_name: bens/hwlc

max_issues_repo_name: bens/hwlc

max_forks_repo_name: bens/hwlc


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Fundamental {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions
import Definition.LogicalRelation.Substitution.Irrelevance as S

open import Agda.Primitive
open import Tools.Product
open import Tools.Unit
open import Tools.Nat
import Tools.PropositionalEquality as PE

mutual
  -- Fundamental theorem for contexts.
  valid : ∀ {Γ} → ⊢ Γ → ⊩ᵛ Γ
  valid ε = ε′
  valid (⊢Γ ∙ A) = let [Γ] , [A] = fundamental A in [Γ] ∙′ [A]

  -- Fundamental theorem for types.
  fundamental : ∀ {Γ A} (⊢A : Γ ⊢ A) → Σω₄ (⊩ᵛ Γ) (λ [Γ] → Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ])
  fundamental (ℕⱼ x) = valid x , ℕᵛ (valid x)
  fundamental (Uⱼ x) = valid x , Uᵛ (valid x)
  fundamental (Πⱼ_▹_ {F} {G} ⊢F ⊢G) with fundamental ⊢F | fundamental ⊢G
  fundamental (Πⱼ_▹_ {F} {G} ⊢F ⊢G) | [Γ] , [F] | [Γ∙F] , [G] =
    [Γ] , Πᵛ {F} {G} [Γ] [F] (S.irrelevance {A = G} [Γ∙F] ([Γ] ∙′ [F]) [G])
  fundamental (univ {A} ⊢A) with fundamentalTerm ⊢A
  fundamental (univ {A} ⊢A) | [Γ] , [U] , [A] =
    [Γ] , univᵛ {A} [Γ] [U] [A]

  -- Fundamental theorem for type equality.
  fundamentalEq : ∀{Γ A B} → Γ ⊢ A ≡ B
    → ∃ω₄  λ ([Γ] : ⊩ᵛ Γ)
    → ∃ω₃² λ ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]) ([B] : Γ ⊩ᵛ⟨ ¹ ⟩ B / [Γ])
    → Γ ⊩ᵛ⟨ ¹ ⟩ A ≡ B / [Γ] / [A]
  fundamentalEq (univ {A} {B} x) with fundamentalTermEq x
  fundamentalEq (univ {A} {B} x) | [Γ] , modelsTermEq [U] [t] [u] [t≡u] =
    let [A] = univᵛ {A} [Γ] [U] [t]
        [B] = univᵛ {B} [Γ] [U] [u]
    in  [Γ] , [A] , [B]
    ,   (λ ⊢Δ [σ] → univEqEq (proj₁ ([U] ⊢Δ [σ]))
                             (proj₁ ([A] ⊢Δ [σ]))
                             ([t≡u] ⊢Δ [σ]))
  fundamentalEq (refl D) =
    let [Γ] , [B] = fundamental D
    in  [Γ] , [B] , [B] , (λ ⊢Δ [σ] → reflEq (proj₁ ([B] ⊢Δ [σ])))
  fundamentalEq (sym A≡B) with fundamentalEq A≡B
  fundamentalEq (sym A≡B) | [Γ] , [B] , [A] , [B≡A] =
    [Γ] , [A] , [B]
        , (λ ⊢Δ [σ] → symEq (proj₁ ([B] ⊢Δ [σ]))
                            (proj₁ ([A] ⊢Δ [σ]))
                            ([B≡A] ⊢Δ [σ]))
  fundamentalEq (trans {A} {B₁} {B} A≡B₁ B₁≡B)
    with fundamentalEq A≡B₁ | fundamentalEq B₁≡B
  fundamentalEq (trans {A} {B₁} {B} A≡B B≡C) | [Γ] , [A] , [B₁] , [A≡B₁]
    | [Γ]₁ , [B₁]₁ , [B] , [B₁≡B] =
      [Γ] , [A] , S.irrelevance {A = B} [Γ]₁ [Γ] [B]
          , (λ ⊢Δ [σ] →
               let [σ]′ = S.irrelevanceSubst [Γ] [Γ]₁ ⊢Δ ⊢Δ [σ]
               in  transEq (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([B₁] ⊢Δ [σ]))
                           (proj₁ ([B] ⊢Δ [σ]′)) ([A≡B₁] ⊢Δ [σ])
                           (irrelevanceEq (proj₁ ([B₁]₁ ⊢Δ [σ]′))
                                          (proj₁ ([B₁] ⊢Δ [σ]))
                                          ([B₁≡B] ⊢Δ [σ]′)))
  fundamentalEq (Π-cong {F} {H} {G} {E} ⊢F A≡B A≡B₁)
    with fundamentalEq A≡B | fundamentalEq A≡B₁
  fundamentalEq (Π-cong {F} {H} {G} {E} ⊢F A≡B A≡B₁) | [Γ] , [F] , [H] , [F≡H]
    | [Γ]₁ , [G] , [E] , [G≡E] =
      let [G]′ = S.irrelevance {A = G} [Γ]₁ ([Γ] ∙′ [F]) [G]
          [E]′ = S.irrelevanceLift {A = E} {F = F} {H = H} [Γ] [F] [H] [F≡H]
                                   (S.irrelevance {A = E} [Γ]₁ ([Γ] ∙′ [F]) [E])
          [G≡E]′ = S.irrelevanceEq {A = G} {B = E} [Γ]₁
                                   ([Γ] ∙′ [F]) [G] [G]′ [G≡E]
      in  [Γ]
      ,   Πᵛ {F} {G} [Γ] [F] [G]′
      ,   Πᵛ {H} {E} [Γ] [H] [E]′
      ,   Π-congᵛ {F} {G} {H} {E} [Γ] [F] [G]′ [H] [E]′ [F≡H] [G≡E]′

  -- Fundamental theorem for variables.
  fundamentalVar : ∀ {Γ A x}
                 → x ∷ A ∈ Γ
                 → ([Γ] : ⊩ᵛ Γ)
                 → ∃ω₃ λ ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ])
                 → Γ ⊩ᵛ⟨ ¹ ⟩ var x ∷ A / [Γ] / [A]
  fundamentalVar here (VPack _ _ (V∙ {A = A} {l = l} [Γ] [A])) =
    (λ ⊢Δ [σ] →
       let [σA]  = proj₁ ([A] ⊢Δ (proj₁ [σ]))
           [σA′] = maybeEmb (irrelevance′ (PE.sym (subst-wk A)) [σA])
       in  [σA′]
       ,   (λ [σ′] [σ≡σ′] →
              irrelevanceEq″ (PE.sym (subst-wk A)) (PE.sym (subst-wk A))
                              [σA] [σA′] (proj₂ ([A] ⊢Δ (proj₁ [σ]))
                                                (proj₁ [σ′]) (proj₁ [σ≡σ′]))))
    , (λ ⊢Δ [σ] →
         let [σA]  = proj₁ ([A] ⊢Δ (proj₁ [σ]))
             [σA′] = maybeEmb (irrelevance′ (PE.sym (subst-wk A)) [σA])
         in  irrelevanceTerm′ (PE.sym (subst-wk A)) [σA] [σA′] (proj₂ [σ])
    , (λ [σ′] [σ≡σ′] → irrelevanceEqTerm′ (PE.sym (subst-wk A))
                                          [σA] [σA′] (proj₂ [σ≡σ′])))
  fundamentalVar (there {A = A} h) ([Γ] ∙′ [B]) =
    (λ ⊢Δ [σ] →
       let [h]   = proj₁ (fundamentalVar h [Γ]) ⊢Δ (proj₁ [σ])
           [σA]  = proj₁ [h]
           [σA′] = irrelevance′ (PE.sym (subst-wk A)) [σA]
       in  [σA′]
       ,   (λ [σ′] [σ≡σ′] →
              irrelevanceEq″ (PE.sym (subst-wk A)) (PE.sym (subst-wk A))
                              [σA] [σA′]
                              (proj₂ [h] (proj₁ [σ′]) (proj₁ [σ≡σ′]))))
    , (λ ⊢Δ [σ] →
         let [h]   = (proj₁ (fundamentalVar h [Γ])) ⊢Δ (proj₁ [σ])
             [σA]  = proj₁ [h]
             [σA′] = irrelevance′ (PE.sym (subst-wk A)) [σA]
             [h′] = (proj₂ (fundamentalVar h [Γ])) ⊢Δ (proj₁ [σ])
         in  irrelevanceTerm′ (PE.sym (subst-wk A)) [σA] [σA′] (proj₁ [h′])
         ,   (λ [σ′] [σ≡σ′] →
                irrelevanceEqTerm′ (PE.sym (subst-wk A)) [σA] [σA′]
                                   (proj₂ [h′] (proj₁ [σ′]) (proj₁ [σ≡σ′]))))

  -- Fundamental theorem for terms.
  fundamentalTerm : ∀{Γ A t} → Γ ⊢ t ∷ A
    → ∃ω₄ λ ([Γ] : ⊩ᵛ Γ)
    → ∃ω₃ λ ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ])
    → Γ ⊩ᵛ⟨ ¹ ⟩ t ∷ A / [Γ] / [A]
  fundamentalTerm (ℕⱼ x) = valid x , Uᵛ (valid x) , ℕᵗᵛ (valid x)
  fundamentalTerm (Πⱼ_▹_ {F} {G} ⊢F ⊢G)
    with fundamentalTerm ⊢F | fundamentalTerm ⊢G
  ... | [Γ] , [U] , [F]ₜ | [Γ]₁ , [U]₁ , [G]ₜ =
    let [F]   = univᵛ {F} [Γ] [U] [F]ₜ
        [U]′  = S.irrelevance {A = U} [Γ]₁ ([Γ] ∙′ [F]) [U]₁
        [F]ₜ′ = S.irrelevanceTerm {A = U} {t = F} [Γ] [Γ] [U] (Uᵛ [Γ]) [F]ₜ
        [G]ₜ′ = S.irrelevanceTerm {A = U} {t = G} [Γ]₁ ([Γ] ∙′ [F]) [U]₁
                                  (λ {Δ} {σ} → [U]′ {Δ} {σ}) [G]ₜ
    in  [Γ] , [U]
    ,   S.irrelevanceTerm {A = U} {t = Π F ▹ G} [Γ] [Γ] (Uᵛ [Γ]) [U]
                          (Πᵗᵛ {F} {G} [Γ] [F] (λ {Δ} {σ} → [U]′ {Δ} {σ})
                               [F]ₜ′ [G]ₜ′)
  fundamentalTerm (var ⊢Γ x∷A) = valid ⊢Γ , fundamentalVar x∷A (valid ⊢Γ)
  fundamentalTerm (lamⱼ {F} {G} {t} ⊢F ⊢t)
    with fundamental ⊢F | fundamentalTerm ⊢t
  ... | [Γ] , [F] | [Γ]₁ , [G] , [t] =
    let [G]′ = S.irrelevance {A = G} [Γ]₁ ([Γ] ∙′ [F]) [G]
        [t]′ = S.irrelevanceTerm {A = G} {t = t} [Γ]₁ ([Γ] ∙′ [F]) [G] [G]′ [t]
    in  [Γ] , Πᵛ {F} {G} [Γ] [F] [G]′
    ,   lamᵛ {F} {G} {t} [Γ] [F] [G]′ [t]′
  fundamentalTerm (_∘ⱼ_ {g} {a} {F} {G} Dt Du)
    with fundamentalTerm Dt | fundamentalTerm Du
  ... | [Γ] , [ΠFG] , [t] | [Γ]₁ , [F] , [u] =
    let [ΠFG]′ = S.irrelevance {A = Π F ▹ G} [Γ] [Γ]₁ [ΠFG]
        [t]′ = S.irrelevanceTerm {A = Π F ▹ G} {t = g} [Γ] [Γ]₁ [ΠFG] [ΠFG]′ [t]
        [G[t]] = substSΠ {F} {G} {a} [Γ]₁ [F] [ΠFG]′ [u]
        [t∘u] = appᵛ {F} {G} {g} {a} [Γ]₁ [F] [ΠFG]′ [t]′ [u]
    in  [Γ]₁ , [G[t]] , [t∘u]
  fundamentalTerm (zeroⱼ x) = valid x , ℕᵛ (valid x) , zeroᵛ {l = ¹} (valid x)
  fundamentalTerm (sucⱼ {n} t) with fundamentalTerm t
  fundamentalTerm (sucⱼ {n} t) | [Γ] , [ℕ] , [n] =
    [Γ] , [ℕ] , sucᵛ {n = n} [Γ] [ℕ] [n]
  fundamentalTerm (natrecⱼ {G} {s} {z} {n} ⊢G ⊢z ⊢s ⊢n)
    with fundamental ⊢G | fundamentalTerm ⊢z | fundamentalTerm ⊢s
       | fundamentalTerm ⊢n
  ... | [Γ] , [G] | [Γ]₁ , [G₀] , [z] | [Γ]₂ , [G₊] , [s] | [Γ]₃ , [ℕ] , [n] =
    let sType = Π ℕ ▹ (G ▹▹ G [ suc (var 0) ]↑)
        [Γ]′ = [Γ]₃
        [G]′ = S.irrelevance {A = G} [Γ] ([Γ]′ ∙′ [ℕ]) [G]
        [G₀]′ = S.irrelevance {A = G [ zero ]} [Γ]₁ [Γ]′ [G₀]
        [G₊]′ = S.irrelevance {A = sType} [Γ]₂ [Γ]′ [G₊]
        [Gₙ]′ = substS {F = ℕ} {G = G} {t = n} [Γ]′ [ℕ] [G]′ [n]
        [z]′ = S.irrelevanceTerm {A = G [ zero ]} {t = z} [Γ]₁ [Γ]′
                                 [G₀] [G₀]′ [z]
        [s]′ = S.irrelevanceTerm {A = sType} {t = s} [Γ]₂ [Γ]′ [G₊] [G₊]′ [s]
    in  [Γ]′ , [Gₙ]′
    ,   natrecᵛ {G} {z} {s} {n} [Γ]′ [ℕ] [G]′ [G₀]′ [G₊]′ [Gₙ]′ [z]′ [s]′ [n]
  fundamentalTerm (conv {t} {A} {B} ⊢t A′≡A)
    with fundamentalTerm ⊢t | fundamentalEq A′≡A
  fundamentalTerm (conv {t} {A} {B} ⊢t A′≡A) | [Γ] , [A′] , [t]
    | [Γ]₁ , [A′]₁ , [A] , [A′≡A] =
      let [Γ]′ = [Γ]₁
          [t]′ = S.irrelevanceTerm {A = A} {t = t} [Γ] [Γ]′ [A′] [A′]₁ [t]
      in  [Γ]′ , [A]
      ,   convᵛ {t} {A} {B} [Γ]′ [A′]₁ [A] [A′≡A] [t]′

  -- Fundamental theorem for term equality.
  fundamentalTermEq : ∀{Γ A t t′} → Γ ⊢ t ≡ t′ ∷ A
                    → ∃ω₄ λ ([Γ] : ⊩ᵛ Γ)
                    → [ Γ ⊩ᵛ⟨ ¹ ⟩ t ≡ t′ ∷ A / [Γ] ]
  fundamentalTermEq (refl D) with fundamentalTerm D
  ... | [Γ] , [A] , [t] =
    [Γ] , modelsTermEq [A] [t] [t]
                       (λ ⊢Δ [σ] → reflEqTerm (proj₁ ([A] ⊢Δ [σ]))
                                              (proj₁ ([t] ⊢Δ [σ])))
  fundamentalTermEq (sym D) with fundamentalTermEq D
  fundamentalTermEq (sym D) | [Γ] , modelsTermEq [A] [t′] [t] [t′≡t] =
    [Γ] , modelsTermEq [A] [t] [t′]
                       (λ ⊢Δ [σ] → symEqTerm (proj₁ ([A] ⊢Δ [σ]))
                                             ([t′≡t] ⊢Δ [σ]))
  fundamentalTermEq (trans {t} {u} {r} {A} t≡u u≡t′)
    with fundamentalTermEq t≡u | fundamentalTermEq u≡t′
  fundamentalTermEq (trans {t} {u} {r} {A} t≡u u≡t′)
    | [Γ] , modelsTermEq [A] [t] [u] [t≡u]
    | [Γ]₁ , modelsTermEq [A]₁ [t]₁ [u]₁ [t≡u]₁ =
      let [r]′ = S.irrelevanceTerm {A = A} {t = r} [Γ]₁ [Γ] [A]₁ [A] [u]₁
      in  [Γ] , modelsTermEq [A] [t] [r]′
                  (λ ⊢Δ [σ] →
                     let [σ]′ = S.irrelevanceSubst [Γ] [Γ]₁ ⊢Δ ⊢Δ [σ]
                         [t≡u]₁′ = irrelevanceEqTerm (proj₁ ([A]₁ ⊢Δ [σ]′))
                                                     (proj₁ ([A] ⊢Δ [σ]))
                                                     ([t≡u]₁ ⊢Δ [σ]′)
                     in  transEqTerm (proj₁ ([A] ⊢Δ [σ]))
                                     ([t≡u] ⊢Δ [σ]) [t≡u]₁′)
  fundamentalTermEq (conv {A} {B} {t} {u} t≡u A′≡A)
    with fundamentalTermEq t≡u | fundamentalEq A′≡A
  fundamentalTermEq (conv {A} {B} {t} {u} t≡u A′≡A)
    | [Γ] , modelsTermEq [A′] [t] [u] [t≡u] | [Γ]₁ , [A′]₁ , [A] , [A′≡A] =
      let [t]′ = S.irrelevanceTerm {A = A} {t = t} [Γ] [Γ]₁ [A′] [A′]₁ [t]
          [u]′ = S.irrelevanceTerm {A = A} {t = u} [Γ] [Γ]₁ [A′] [A′]₁ [u]
          [t]″ = convᵛ {t} {A} {B} [Γ]₁ [A′]₁ [A] [A′≡A] [t]′
          [u]″ = convᵛ {u} {A} {B} [Γ]₁ [A′]₁ [A] [A′≡A] [u]′
      in  [Γ]₁
      ,   modelsTermEq [A] [t]″ [u]″
            (λ ⊢Δ [σ] →
               let [σ]′ = S.irrelevanceSubst [Γ]₁ [Γ] ⊢Δ ⊢Δ [σ]
                   [t≡u]′ = irrelevanceEqTerm (proj₁ ([A′] ⊢Δ [σ]′))
                                              (proj₁ ([A′]₁ ⊢Δ [σ]))
                                              ([t≡u] ⊢Δ [σ]′)
               in  convEqTerm₁ (proj₁ ([A′]₁ ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ]))
                               ([A′≡A] ⊢Δ [σ]) [t≡u]′)
  fundamentalTermEq (Π-cong {E} {F} {G} {H} ⊢F F≡H G≡E)
    with fundamental ⊢F | fundamentalTermEq F≡H | fundamentalTermEq G≡E
  ... | [Γ] , [F] | [Γ]₁ , modelsTermEq [U] [F]ₜ [H]ₜ [F≡H]ₜ
      | [Γ]₂ , modelsTermEq [U]₁ [G]ₜ [E]ₜ [G≡E]ₜ =
    let [U]′  = Uᵛ [Γ]
        [F]ₜ′ = S.irrelevanceTerm {A = U} {t = F} [Γ]₁ [Γ] [U] [U]′ [F]ₜ
        [H]ₜ′ = S.irrelevanceTerm {A = U} {t = H} [Γ]₁ [Γ] [U] [U]′ [H]ₜ
        [F]′  = S.irrelevance {A = F} [Γ] [Γ]₁ [F]
        [H]   = univᵛ {A = H} [Γ] [U]′ [H]ₜ′
        [F≡H] = S.irrelevanceEq {A = F} {B = H} [Γ]₁ [Γ] [F]′ [F]
                  (univEqᵛ {F} {H} [Γ]₁ [U] [F]′ [F≡H]ₜ)
        [U]₁′ = Uᵛ (VPack _ _ (V∙ {A = F} [Γ] [F]))
        [U]₂′ = Uᵛ (VPack _ _ (V∙ {A = H} [Γ] [H]))
        [G]ₜ′ = S.irrelevanceTerm {A = U} {t = G} [Γ]₂ ([Γ] ∙′ [F])
                                  [U]₁ (λ {Δ} {σ} → [U]₁′ {Δ} {σ}) [G]ₜ
        [E]ₜ′ = S.irrelevanceTermLift {A = U} {F = F} {H = H} {t = E}
                                      [Γ] [F] [H] [F≡H]
                                      (λ {Δ} {σ} → [U]₁′ {Δ} {σ})
                  (S.irrelevanceTerm {A = U} {t = E} [Γ]₂ ([Γ] ∙′ [F])
                                     [U]₁ (λ {Δ} {σ} → [U]₁′ {Δ} {σ}) [E]ₜ)
        [F≡H]ₜ′ = S.irrelevanceEqTerm {A = U} {t = F} {u = H}
                                      [Γ]₁ [Γ] [U] (Uᵛ [Γ]) [F≡H]ₜ
        [G≡E]ₜ′ = S.irrelevanceEqTerm {A = U} {t = G} {u = E} [Γ]₂
                                      (VPack _ _ (V∙ {A = F} [Γ] [F])) [U]₁
                                      (λ {Δ} {σ} → [U]₁′ {Δ} {σ}) [G≡E]ₜ
    in  [Γ]
    ,   modelsTermEq
          [U]′
          (Πᵗᵛ {F} {G} [Γ] [F] (λ {Δ} {σ} → [U]₁′ {Δ} {σ}) [F]ₜ′ [G]ₜ′)
          (Πᵗᵛ {H} {E} [Γ] [H] (λ {Δ} {σ} → [U]₂′ {Δ} {σ}) [H]ₜ′ [E]ₜ′)
          (Π-congᵗᵛ {F} {G} {H} {E} [Γ] [F] [H]
                    (λ {Δ} {σ} → [U]₁′ {Δ} {σ}) (λ {Δ} {σ} → [U]₂′ {Δ} {σ})
                    [F]ₜ′ [G]ₜ′ [H]ₜ′ [E]ₜ′ [F≡H]ₜ′ [G≡E]ₜ′)
  fundamentalTermEq (app-cong {a} {b} {f} {g} {F} {G} f≡g a≡b)
    with fundamentalTermEq f≡g | fundamentalTermEq a≡b
  ... | [Γ] , modelsTermEq [ΠFG] [f] [g] [f≡g]
      | [Γ]₁ , modelsTermEq [F] [a] [b] [a≡b] =
    let [ΠFG]′ = S.irrelevance {A = Π F ▹ G} [Γ] [Γ]₁ [ΠFG]
        [f]′ = S.irrelevanceTerm {A = Π F ▹ G} {t = f} [Γ] [Γ]₁ [ΠFG] [ΠFG]′ [f]
        [g]′ = S.irrelevanceTerm {A = Π F ▹ G} {t = g} [Γ] [Γ]₁ [ΠFG] [ΠFG]′ [g]
        [f≡g]′ = S.irrelevanceEqTerm {A = Π F ▹ G} {t = f} {u = g}
                                     [Γ] [Γ]₁ [ΠFG] [ΠFG]′ [f≡g]
        [G[a]] = substSΠ {F} {G} {a} [Γ]₁ [F] [ΠFG]′ [a]
        [G[b]] = substSΠ {F} {G} {b} [Γ]₁ [F] [ΠFG]′ [b]
        [G[a]≡G[b]] = substSΠEq {F} {G} {F} {G} {a} {b} [Γ]₁ [F] [F] [ΠFG]′
                                [ΠFG]′ (reflᵛ {Π F ▹ G} [Γ]₁ [ΠFG]′) [a] [b] [a≡b]
    in  [Γ]₁ , modelsTermEq [G[a]]
                            (appᵛ {F} {G} {f} {a} [Γ]₁ [F] [ΠFG]′ [f]′ [a])
                            (conv₂ᵛ {g ∘ b} {G [ a ]} {G [ b ]} [Γ]₁
                                    [G[a]] [G[b]] [G[a]≡G[b]]
                                    (appᵛ {F} {G} {g} {b}
                                          [Γ]₁ [F] [ΠFG]′ [g]′ [b]))
                            (app-congᵛ {F} {G} {f} {g} {a} {b}
                                       [Γ]₁ [F] [ΠFG]′ [f≡g]′ [a] [b] [a≡b])
  fundamentalTermEq (β-red {a} {b} {F} {G} ⊢F ⊢b ⊢a)
    with fundamental ⊢F | fundamentalTerm ⊢b | fundamentalTerm ⊢a
  ... | [Γ] , [F] | [Γ]₁ , [G] , [b] | [Γ]₂ , [F]₁ , [a] =
    let [G]′ = S.irrelevance {A = G} [Γ]₁ ([Γ]₂ ∙′ [F]₁) [G]
        [b]′ = S.irrelevanceTerm {A = G} {t = b} [Γ]₁ ([Γ]₂ ∙′ [F]₁) [G] [G]′ [b]
        [G[a]] = substS {F} {G} {a} [Γ]₂ [F]₁ [G]′ [a]
        [b[a]] = substSTerm {F} {G} {a} {b} [Γ]₂ [F]₁ [G]′ [b]′ [a]
        [lam] , [eq] =
          redSubstTermᵛ {G [ a ]} {(lam b) ∘ a} {b [ a ]} [Γ]₂
            (λ {Δ} {σ} ⊢Δ [σ] →
               let [liftσ] = liftSubstS {F = F} [Γ]₂ ⊢Δ [F]₁ [σ]
                   ⊢σF = escape (proj₁ ([F]₁ ⊢Δ [σ]))
                   ⊢σb = escapeTerm (proj₁ ([G]′ (⊢Δ ∙ ⊢σF) [liftσ]))
                                       (proj₁ ([b]′ (⊢Δ ∙ ⊢σF) [liftσ]))
                   ⊢σa = escapeTerm (proj₁ ([F]₁ ⊢Δ [σ]))
                                       (proj₁ ([a] ⊢Δ [σ]))
               in  PE.subst₂ (λ x y → _ ⊢ (lam (subst (liftSubst σ) b))
                                          ∘ (subst σ a) ⇒ x ∷ y)
                             (PE.sym (singleSubstLift b a))
                             (PE.sym (singleSubstLift G a))
                             (β-red ⊢σF ⊢σb ⊢σa))
                         [G[a]] [b[a]]
    in  [Γ]₂ , modelsTermEq [G[a]] [lam] [b[a]] [eq]
  fundamentalTermEq (η-eq {f} {g} {F} {G} ⊢F ⊢t ⊢t′ t≡t′) with
    fundamental ⊢F | fundamentalTerm ⊢t |
    fundamentalTerm ⊢t′ | fundamentalTermEq t≡t′
  ... | [Γ] , [F] | [Γ]₁ , [ΠFG] , [t] | [Γ]₂ , [ΠFG]₁ , [t′]
      | [Γ]₃ , modelsTermEq [G] [t0] [t′0] [t0≡t′0] =
    let [F]′ = S.irrelevance {A = F} [Γ] [Γ]₁ [F]
        [G]′ = S.irrelevance {A = G} [Γ]₃ ([Γ]₁ ∙′ [F]′) [G]
        [t′]′ = S.irrelevanceTerm {A = Π F ▹ G} {t = g}
                                  [Γ]₂ [Γ]₁ [ΠFG]₁ [ΠFG] [t′]
        [ΠFG]″ = Πᵛ {F} {G} [Γ]₁ [F]′ [G]′
        [t]″ = S.irrelevanceTerm {A = Π F ▹ G} {t = f}
                                  [Γ]₁ [Γ]₁ [ΠFG] [ΠFG]″ [t]
        [t′]″ = S.irrelevanceTerm {A = Π F ▹ G} {t = g}
                                   [Γ]₂ [Γ]₁ [ΠFG]₁ [ΠFG]″ [t′]
        [t0≡t′0]′ = S.irrelevanceEqTerm {A = G} {t = wk1 f ∘ var 0}
                                        {u = wk1 g ∘ var 0}
                                        [Γ]₃ ([Γ]₁ ∙′ [F]′) [G] [G]′ [t0≡t′0]
        [t≡t′] = η-eqᵛ {f} {g} {F} {G} [Γ]₁ [F]′ [G]′ [t]″ [t′]″ [t0≡t′0]′
        [t≡t′]′ = S.irrelevanceEqTerm {A = Π F ▹ G} {t = f} {u = g}
                                      [Γ]₁ [Γ]₁ [ΠFG]″ [ΠFG] [t≡t′]
    in  [Γ]₁ , modelsTermEq [ΠFG] [t] [t′]′ [t≡t′]′
  fundamentalTermEq (suc-cong x) with fundamentalTermEq x
  fundamentalTermEq (suc-cong {t} {u} x)
    | [Γ] , modelsTermEq [A] [t] [u] [t≡u] =
      let [suct] = sucᵛ {n = t} [Γ] [A] [t]
          [sucu] = sucᵛ {n = u} [Γ] [A] [u]
      in  [Γ] , modelsTermEq [A] [suct] [sucu]
                             (λ ⊢Δ [σ] →
                                sucEqTerm (proj₁ ([A] ⊢Δ [σ])) ([t≡u] ⊢Δ [σ]))
  fundamentalTermEq (natrec-cong {z} {z′} {s} {s′} {n} {n′} {F} {F′}
                                 F≡F′ z≡z′ s≡s′ n≡n′)
    with fundamentalEq F≡F′ |
         fundamentalTermEq z≡z′      |
         fundamentalTermEq s≡s′      |
         fundamentalTermEq n≡n′
  fundamentalTermEq (natrec-cong {z} {z′} {s} {s′} {n} {n′} {F} {F′}
                                 F≡F′ z≡z′ s≡s′ n≡n′) |
    [Γ]  , [F] , [F′] , [F≡F′] |
    [Γ]₁ , modelsTermEq [F₀] [z] [z′] [z≡z′] |
    [Γ]₂ , modelsTermEq [F₊] [s] [s′] [s≡s′] |
    [Γ]₃ , modelsTermEq [ℕ] [n] [n′] [n≡n′] =
      let sType = Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
          s′Type = Π ℕ ▹ (F′ ▹▹ F′ [ suc (var 0) ]↑)
          [0] = S.irrelevanceTerm {l = ¹} {A = ℕ} {t = zero}
                                  [Γ]₃ [Γ]₃ (ℕᵛ [Γ]₃) [ℕ] (zeroᵛ {l = ¹} [Γ]₃)
          [F]′ = S.irrelevance {A = F} [Γ] ([Γ]₃ ∙′ [ℕ]) [F]
          [F₀]′ = S.irrelevance {A = F [ zero ]} [Γ]₁ [Γ]₃ [F₀]
          [F₊]′ = S.irrelevance {A = sType} [Γ]₂ [Γ]₃ [F₊]
          [Fₙ]′ = substS {ℕ} {F} {n} [Γ]₃ [ℕ] [F]′ [n]
          [F′]′ = S.irrelevance {A = F′} [Γ] ([Γ]₃ ∙′ [ℕ]) [F′]
          [F₀]″ = substS {ℕ} {F} {zero} [Γ]₃ [ℕ] [F]′ [0]
          [F′₀]′ = substS {ℕ} {F′} {zero} [Γ]₃ [ℕ] [F′]′ [0]
          [F′₊]′ = sucCase {F′} [Γ]₃ [ℕ] [F′]′
          [F′ₙ′]′ = substS {ℕ} {F′} {n′} [Γ]₃ [ℕ] [F′]′ [n′]
          [ℕ≡ℕ] = reflᵛ {ℕ} [Γ]₃ [ℕ]
          [0≡0] = reflᵗᵛ {ℕ} {zero} [Γ]₃ [ℕ] [0]
          [F≡F′]′ = S.irrelevanceEq {A = F} {B = F′}
                                    [Γ] ([Γ]₃ ∙′ [ℕ]) [F] [F]′ [F≡F′]
          [F₀≡F′₀] = substSEq {ℕ} {ℕ} {F} {F′} {zero} {zero}
                              [Γ]₃ [ℕ] [ℕ] [ℕ≡ℕ]
                              [F]′ [F′]′ [F≡F′]′ [0] [0] [0≡0]
          [F₀≡F′₀]′ = S.irrelevanceEq {A = F [ zero ]} {B = F′ [ zero ]}
                                      [Γ]₃ [Γ]₃ [F₀]″ [F₀]′ [F₀≡F′₀]
          [F₊≡F′₊] = sucCaseCong {F} {F′} [Γ]₃ [ℕ] [F]′ [F′]′ [F≡F′]′
          [F₊≡F′₊]′ = S.irrelevanceEq {A = sType} {B = s′Type}
                                      [Γ]₃ [Γ]₃ (sucCase {F} [Γ]₃ [ℕ] [F]′)
                                      [F₊]′ [F₊≡F′₊]
          [Fₙ≡F′ₙ′]′ = substSEq {ℕ} {ℕ} {F} {F′} {n} {n′}
                                [Γ]₃ [ℕ] [ℕ] [ℕ≡ℕ] [F]′ [F′]′ [F≡F′]′
                                [n] [n′] [n≡n′]
          [z]′ = S.irrelevanceTerm {A = F [ zero ]} {t = z}
                                   [Γ]₁ [Γ]₃ [F₀] [F₀]′ [z]
          [z′]′ = convᵛ {z′} {F [ zero ]} {F′ [ zero ]}
                        [Γ]₃ [F₀]′ [F′₀]′ [F₀≡F′₀]′
                        (S.irrelevanceTerm {A = F [ zero ]} {t = z′}
                                           [Γ]₁ [Γ]₃ [F₀] [F₀]′ [z′])
          [z≡z′]′ = S.irrelevanceEqTerm {A = F [ zero ]} {t = z} {u = z′}
                                        [Γ]₁ [Γ]₃ [F₀] [F₀]′ [z≡z′]
          [s]′ = S.irrelevanceTerm {A = sType} {t = s} [Γ]₂ [Γ]₃ [F₊] [F₊]′ [s]
          [s′]′ = convᵛ {s′} {sType} {s′Type} [Γ]₃ [F₊]′ [F′₊]′ [F₊≡F′₊]′
                        (S.irrelevanceTerm {A = sType} {t = s′}
                                           [Γ]₂ [Γ]₃ [F₊] [F₊]′ [s′])
          [s≡s′]′ = S.irrelevanceEqTerm {A = sType} {t = s} {u = s′}
                                        [Γ]₂ [Γ]₃ [F₊] [F₊]′ [s≡s′]
      in  [Γ]₃
      ,   modelsTermEq [Fₙ]′
                       (natrecᵛ {F} {z} {s} {n}
                                [Γ]₃ [ℕ] [F]′ [F₀]′ [F₊]′ [Fₙ]′ [z]′ [s]′ [n])
                       (conv₂ᵛ {natrec F′ z′ s′ n′} {F [ n ]} {F′ [ n′ ]}
                               [Γ]₃ [Fₙ]′ [F′ₙ′]′ [Fₙ≡F′ₙ′]′
                               (natrecᵛ {F′} {z′} {s′} {n′}
                                        [Γ]₃ [ℕ] [F′]′ [F′₀]′ [F′₊]′ [F′ₙ′]′
                                        [z′]′ [s′]′ [n′]))
                       (natrec-congᵛ {F} {F′} {z} {z′} {s} {s′} {n} {n′}
                                     [Γ]₃ [ℕ] [F]′ [F′]′ [F≡F′]′
                                     [F₀]′ [F′₀]′ [F₀≡F′₀]′
                                     [F₊]′ [F′₊]′ [F₊≡F′₊]′ [Fₙ]′
                                     [z]′ [z′]′ [z≡z′]′
                                     [s]′ [s′]′ [s≡s′]′ [n] [n′] [n≡n′])
  fundamentalTermEq (natrec-zero {z} {s} {F} ⊢F ⊢z ⊢s)
    with fundamental ⊢F | fundamentalTerm ⊢z | fundamentalTerm ⊢s
  fundamentalTermEq (natrec-zero {z} {s} {F} ⊢F ⊢z ⊢s) | [Γ] , [F]
    | [Γ]₁ , [F₀] , [z] | [Γ]₂ , [F₊] , [s] =
    let sType = Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
        [Γ]′ = [Γ]₁
        [ℕ]′ = ℕᵛ {l = ¹} [Γ]′
        [F₊]′ = S.irrelevance {A = sType} [Γ]₂ [Γ]′ [F₊]
        [s]′ = S.irrelevanceTerm {A = sType} {t = s} [Γ]₂ [Γ]′ [F₊] [F₊]′ [s]
        [F]′ = S.irrelevance {A = F} [Γ] ([Γ]′ ∙′ [ℕ]′) [F]
        d , r =
          redSubstTermᵛ {F [ zero ]} {natrec F z s zero} {z} [Γ]′
            (λ {Δ} {σ} ⊢Δ [σ] →
               let ⊢ℕ = escape (proj₁ ([ℕ]′ ⊢Δ [σ]))
                   ⊢F = escape (proj₁ ([F]′ (⊢Δ ∙ ⊢ℕ)
                                               (liftSubstS {F = ℕ}
                                                           [Γ]′ ⊢Δ [ℕ]′ [σ])))
                   ⊢z = PE.subst (λ x → Δ ⊢ subst σ z ∷ x)
                                 (singleSubstLift F zero)
                                 (escapeTerm (proj₁ ([F₀] ⊢Δ [σ]))
                                                (proj₁ ([z] ⊢Δ [σ])))
                   ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x)
                                 (natrecSucCase σ F)
                                 (escapeTerm (proj₁ ([F₊]′ ⊢Δ [σ]))
                                                (proj₁ ([s]′ ⊢Δ [σ])))
               in PE.subst (λ x → Δ ⊢ subst σ (natrec F z s zero)
                                    ⇒ subst σ z ∷ x)
                           (PE.sym (singleSubstLift F zero))
                           (natrec-zero ⊢F ⊢z ⊢s))
                        [F₀] [z]
    in  [Γ]′ , modelsTermEq [F₀] d [z] r
  fundamentalTermEq (natrec-suc {n} {z} {s} {F} ⊢n ⊢F ⊢z ⊢s)
    with fundamentalTerm ⊢n | fundamental ⊢F
       | fundamentalTerm ⊢z | fundamentalTerm ⊢s
  ... | [Γ] , [ℕ] , [n] | [Γ]₁ , [F] | [Γ]₂ , [F₀] , [z] | [Γ]₃ , [F₊] , [s] =
    let [ℕ]′ = S.irrelevance {A = ℕ} [Γ] [Γ]₃ [ℕ]
        [n]′ = S.irrelevanceTerm {A = ℕ} {t = n} [Γ] [Γ]₃ [ℕ] [ℕ]′ [n]
        [sucn] = sucᵛ {n = n} [Γ]₃ [ℕ]′ [n]′
        [F₀]′ = S.irrelevance {A = F [ zero ]} [Γ]₂ [Γ]₃ [F₀]
        [z]′ = S.irrelevanceTerm {A = F [ zero ]} {t = z}
                                 [Γ]₂ [Γ]₃ [F₀] [F₀]′ [z]
        [F]′ = S.irrelevance {A = F} [Γ]₁ ([Γ]₃ ∙′ [ℕ]′) [F]
        [F[sucn]] = substS {ℕ} {F} {suc n} [Γ]₃ [ℕ]′ [F]′ [sucn]
        [Fₙ]′ = substS {ℕ} {F} {n} [Γ]₃ [ℕ]′ [F]′ [n]′
        [natrecₙ] = natrecᵛ {F} {z} {s} {n}
                            [Γ]₃ [ℕ]′ [F]′ [F₀]′ [F₊] [Fₙ]′ [z]′ [s] [n]′
        t = (s ∘ n) ∘ (natrec F z s n)
        q = subst (liftSubst (sgSubst n))
                  (wk1 (F [ suc (var 0) ]↑))
        y = S.irrelevanceTerm′
              {A = q [ natrec F z s n ]} {A′ = F [ suc n ]} {t = t}
              (natrecIrrelevantSubst′ F z s n) [Γ]₃ [Γ]₃
              (substSΠ {F [ n ]} {q} {natrec F z s n} [Γ]₃
                (substS {ℕ} {F} {n} [Γ]₃ [ℕ]′ [F]′ [n]′)
                (substSΠ {ℕ} {F ▹▹ F [ suc (var 0) ]↑} {n}
                         [Γ]₃ [ℕ]′ [F₊] [n]′)
                [natrecₙ])
              [F[sucn]]
              (appᵛ {F [ n ]} {q} {s ∘ n} {natrec F z s n} [Γ]₃ [Fₙ]′
                (substSΠ {ℕ} {F ▹▹ F [ suc (var 0) ]↑} {n}
                         [Γ]₃ [ℕ]′ [F₊] [n]′)
                (appᵛ {ℕ} {F ▹▹ F [ suc (var 0) ]↑} {s} {n}
                      [Γ]₃ [ℕ]′ [F₊] [s] [n]′)
                [natrecₙ])
        d , r =
          redSubstTermᵛ {F [ suc n ]} {natrec F z s (suc n)} {t } {¹} {_} [Γ]₃
            (λ {Δ} {σ} ⊢Δ [σ] →
               let ⊢n = escapeTerm (proj₁ ([ℕ]′ ⊢Δ [σ]))
                                      (proj₁ ([n]′ ⊢Δ [σ]))
                   ⊢ℕ = escape (proj₁ ([ℕ]′ ⊢Δ [σ]))
                   ⊢F = escape (proj₁ ([F]′ (⊢Δ ∙ ⊢ℕ)
                                               (liftSubstS {F = ℕ}
                                                           [Γ]₃ ⊢Δ [ℕ]′ [σ])))
                   ⊢z = PE.subst (λ x → Δ ⊢ subst σ z ∷ x)
                                 (singleSubstLift F zero)
                                 (escapeTerm (proj₁ ([F₀]′ ⊢Δ [σ]))
                                                (proj₁ ([z]′ ⊢Δ [σ])))
                   ⊢s = PE.subst (λ x → Δ ⊢ subst σ s ∷ x)
                                 (natrecSucCase σ F)
                                 (escapeTerm (proj₁ ([F₊] ⊢Δ [σ]))
                                                (proj₁ ([s] ⊢Δ [σ])))
                   r = _⊢_⇒_∷_.natrec-suc {n = subst σ n}
                                          {z = subst σ z} {s = subst σ s}
                                          {F = subst (liftSubst σ) F}
                                          ⊢n ⊢F ⊢z ⊢s
               in PE.subst (λ x → Δ ⊢ subst σ (natrec F z s (suc n))
                                    ⇒ (subst σ t) ∷ x)
                           (PE.trans (PE.trans (substCompEq F)
                             (substVar-to-subst (λ { 0 → PE.refl
                                         ; (1+ x) → PE.trans (subst-wk (σ x))
                                                              (subst-id (σ x))
                                         })
                                      F))
                             (PE.sym (substCompEq F)))
                           r)
                        [F[sucn]] y
    in  [Γ]₃ , modelsTermEq [F[sucn]] d y r

-- Fundamental theorem for substitutions.
fundamentalSubst : ∀ {Γ Δ σ} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
      → Δ ⊢ˢ σ ∷ Γ
      → ∃ω₄ λ [Γ] → Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ
fundamentalSubst ε ⊢Δ [σ] = ε′ , tt
fundamentalSubst (⊢Γ ∙ ⊢A) ⊢Δ ([tailσ] , [headσ]) =
  let [Γ] , [A] = fundamental ⊢A
      [Δ] , [A]′ , [t] = fundamentalTerm [headσ]
      [Γ]′ , [σ] = fundamentalSubst ⊢Γ ⊢Δ [tailσ]
      [tailσ]′ = S.irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [σ]
      [idA]  = proj₁ ([A]′ (soundContext [Δ]) (idSubstS [Δ]))
      [idA]′ = proj₁ ([A] ⊢Δ [tailσ]′)
      [idt]  = proj₁ ([t] (soundContext [Δ]) (idSubstS [Δ]))
  in  [Γ] ∙′ [A] , ([tailσ]′
  ,   irrelevanceTerm″ (subst-id _) (subst-id _) [idA] [idA]′ [idt])

-- Fundamental theorem for substitution equality.
fundamentalSubstEq : ∀ {Γ Δ σ σ′} (⊢Γ : ⊢ Γ) (⊢Δ : ⊢ Δ)
      → Δ ⊢ˢ σ ≡ σ′ ∷ Γ
      → ∃ω₄ λ [Γ]
      → ∃ω₃²  λ [σ] ([σ′] : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
      → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]
fundamentalSubstEq ε ⊢Δ σ = ε′ , tt , tt , tt
fundamentalSubstEq (⊢Γ ∙ ⊢A) ⊢Δ (tailσ≡σ′ , headσ≡σ′) =
  let [Γ] , [A] = fundamental ⊢A
      [Γ]′ , [tailσ] , [tailσ′] , [tailσ≡σ′] = fundamentalSubstEq ⊢Γ ⊢Δ tailσ≡σ′
      [Δ] , modelsTermEq [A]′ [t] [t′] [t≡t′] = fundamentalTermEq headσ≡σ′
      [tailσ]′ = S.irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [tailσ]
      [tailσ′]′ = S.irrelevanceSubst [Γ]′ [Γ] ⊢Δ ⊢Δ [tailσ′]
      [tailσ≡σ′]′ = S.irrelevanceSubstEq [Γ]′ [Γ] ⊢Δ ⊢Δ [tailσ] [tailσ]′ [tailσ≡σ′]
      [idA]  = proj₁ ([A]′ (soundContext [Δ]) (idSubstS [Δ]))
      [idA]′ = proj₁ ([A] ⊢Δ [tailσ]′)
      [idA]″ = proj₁ ([A] ⊢Δ [tailσ′]′)
      [idt]  = proj₁ ([t] (soundContext [Δ]) (idSubstS [Δ]))
      [idt′] = proj₁ ([t′] (soundContext [Δ]) (idSubstS [Δ]))
      [idt≡t′]  = [t≡t′] (soundContext [Δ]) (idSubstS [Δ])
  in  [Γ] ∙′ [A]
  ,   ([tailσ]′ , irrelevanceTerm″ (subst-id _) (subst-id _) [idA] [idA]′ [idt])
  ,   ([tailσ′]′ , convTerm₁ [idA]′ [idA]″
                             (proj₂ ([A] ⊢Δ [tailσ]′) [tailσ′]′ [tailσ≡σ′]′)
                             (irrelevanceTerm″ (subst-id _) (subst-id _)
                                                [idA] [idA]′ [idt′]))
  ,   ([tailσ≡σ′]′ , irrelevanceEqTerm″ (subst-id _) (subst-id _) (subst-id _)
                                         [idA] [idA]′ [idt≡t′])

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
------------------------------------------------------------------------
-- Some auxiliary operations and lemmas
------------------------------------------------------------------------

module BreadthFirst.Lemmas where

open import Codata.Musical.Notation
open import Codata.Musical.Colist as Colist
  using (Colist; []; _∷_; concat; _++_)
open import Function
open import Data.List using ([]; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; _∷_; _⁺++⁺_)
import Data.Vec as Vec
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_) renaming (refl to ≡-refl)

open import BreadthFirst.Universe
open import BreadthFirst.Programs
open import Tree using (leaf; node; map)
open import Stream using (Stream; _≺_) renaming (_++_ to _++∞_)

------------------------------------------------------------------------
-- Some operations

zipWith : {A B : Set} (f : A → B → B) → Colist A → Stream B → Stream B
zipWith f []       ys       = ys
zipWith f (x ∷ xs) (y ≺ ys) = f x y ≺ ♯ zipWith f (♭ xs) (♭ ys)

infixr 5 _⁺++_ _⁺++∞_

_⁺++∞_ : {A : Set} → List⁺ A → Stream A → Stream A
xs ⁺++∞ ys = Colist.fromList (Vec.toList $ List⁺.toVec xs) ++∞ ys

_⁺++_ : {A : Set} → List⁺ A → Colist A → Colist A
xs ⁺++ ys = Colist.fromList (Vec.toList $ List⁺.toVec xs) ++ ys

------------------------------------------------------------------------
-- Eq is an equivalence relation

refl : ∀ {a} x → Eq a x x
refl {a = tree a}   leaf         = leaf
refl {a = tree a}   (node l x r) = node (♯ refl (♭ l)) (refl x) (♯ refl (♭ r))
refl {a = stream a} (x ≺ xs)     = refl x ≺ ♯ refl (♭ xs)
refl {a = colist a} []           = []
refl {a = colist a} (x ∷ xs)     = refl x ∷ ♯ refl (♭ xs)
refl {a = a ⊗ b}    (x , y)      = (refl x , refl y)
refl {a = ⌈ A ⌉}    x            = ⌈ PropEq.refl ⌉

sym : ∀ {a x y} → Eq a x y → Eq a y x
sym {a = tree a}   leaf                  = leaf
sym {a = tree a}   (node l≈l′ x≈x′ r≈r′) = node (♯ sym (♭ l≈l′)) (sym x≈x′) (♯ sym (♭ r≈r′))
sym {a = stream a} (x≈x′ ≺ xs≈xs′)       = sym x≈x′ ≺ ♯ sym (♭ xs≈xs′)
sym {a = colist a} []                    = []
sym {a = colist a} (x≈x′ ∷ xs≈xs′)       = sym x≈x′ ∷ ♯ sym (♭ xs≈xs′)
sym {a = a ⊗ b}    (x≈x′ , y≈y′)         = (sym x≈x′ , sym y≈y′)
sym {a = ⌈ A ⌉}    ⌈ x≡x′ ⌉              = ⌈ PropEq.sym x≡x′ ⌉

trans : ∀ {a x y z} → Eq a x y → Eq a y z → Eq a x z
trans {a = tree a}   leaf leaf                = leaf
trans {a = tree a}   (node l≈l′ x≈x′ r≈r′)
                     (node l′≈l″ x′≈x″ r′≈r″) = node (♯ trans (♭ l≈l′) (♭ l′≈l″))
                                                     (trans x≈x′ x′≈x″)
                                                     (♯ trans (♭ r≈r′) (♭ r′≈r″))
trans {a = stream a} (x≈x′  ≺ xs≈xs′)
                     (x′≈x″ ≺ xs′≈xs″)        = trans x≈x′ x′≈x″ ≺ ♯ trans (♭ xs≈xs′) (♭ xs′≈xs″)
trans {a = colist a} [] []                    = []
trans {a = colist a} (x≈x′  ∷ xs≈xs′)
                     (x′≈x″ ∷ xs′≈xs″)        = trans x≈x′ x′≈x″ ∷ ♯ trans (♭ xs≈xs′) (♭ xs′≈xs″)
trans {a = a ⊗ b}    (x≈x′  , y≈y′)
                     (x′≈x″ , y′≈y″)          = (trans x≈x′ x′≈x″ , trans y≈y′ y′≈y″)
trans {a = ⌈ A ⌉}    ⌈ x≡x′  ⌉ ⌈ x′≡x″ ⌉      = ⌈ PropEq.trans x≡x′ x′≡x″ ⌉

------------------------------------------------------------------------
-- Productivity checker workaround for Eq

infixr 5 _≺_ _∷_
infixr 4 _,_
infix  3 _∎
infixr 2 _≈⟨_⟩_ _≊⟨_⟩_

data EqP : ∀ a → El a → El a → Set₁ where
  leaf : ∀ {a} → EqP (tree a) leaf leaf
  node : ∀ {a x x′ l l′ r r′}
         (l≈l′ : ∞ (EqP (tree a) (♭ l) (♭ l′)))
         (x≈x′ :    Eq        a     x     x′  )
         (r≈r′ : ∞ (EqP (tree a) (♭ r) (♭ r′))) →
         EqP (tree a) (node l x r) (node l′ x′ r′)
  _≺_  : ∀ {a x x′ xs xs′}
         (x≈x′   :    Eq          a     x      x′   )
         (xs≈xs′ : ∞ (EqP (stream a) (♭ xs) (♭ xs′))) →
         EqP (stream a) (x ≺ xs) (x′ ≺ xs′)
  []   : ∀ {a} → EqP (colist a) [] []
  _∷_  : ∀ {a x x′ xs xs′}
         (x≈x′   :    Eq          a     x      x′   )
         (xs≈xs′ : ∞ (EqP (colist a) (♭ xs) (♭ xs′))) →
         EqP (colist a) (x ∷ xs) (x′ ∷ xs′)
  _,_  : ∀ {a b x x′ y y′}
         (x≈x′ : Eq a x x′) (y≈y′ : Eq b y y′) →
         EqP (a ⊗ b) (x , y) (x′ , y′)
  ⌈_⌉  : ∀ {A x x′} (x≡x′ : x ≡ x′) → EqP ⌈ A ⌉ x x′

  _≊⟨_⟩_ : ∀ {a} x {y z}
           (x≈y : EqP a x y) (y≈z : EqP a y z) → EqP a x z

  zipWith-cong :
    ∀ {a b} {f : El a → El b → El b}
    (cong : ∀ {x x′ y y′} →
            Eq a x x′ → Eq b y y′ → Eq b (f x y) (f x′ y′))
    {xs xs′ ys ys′}
    (xs≈xs′ : EqP (colist a) xs xs′)
    (ys≈ys′ : EqP (stream b) ys ys′) →
    EqP (stream b) (zipWith f xs ys) (zipWith f xs′ ys′)

data EqW : ∀ a → El a → El a → Set₁ where
  leaf : ∀ {a} → EqW (tree a) leaf leaf
  node : ∀ {a x x′ l l′ r r′}
         (l≈l′ : EqP (tree a) (♭ l) (♭ l′))
         (x≈x′ : Eq        a     x     x′ )
         (r≈r′ : EqP (tree a) (♭ r) (♭ r′)) →
         EqW (tree a) (node l x r) (node l′ x′ r′)
  _≺_  : ∀ {a x x′ xs xs′}
         (x≈x′   : Eq          a     x      x′  )
         (xs≈xs′ : EqP (stream a) (♭ xs) (♭ xs′)) →
         EqW (stream a) (x ≺ xs) (x′ ≺ xs′)
  []   : ∀ {a} → EqW (colist a) [] []
  _∷_  : ∀ {a x x′ xs xs′}
         (x≈x′   : Eq          a     x      x′  )
         (xs≈xs′ : EqP (colist a) (♭ xs) (♭ xs′)) →
         EqW (colist a) (x ∷ xs) (x′ ∷ xs′)
  _,_  : ∀ {a b x x′ y y′}
         (x≈x′ : Eq a x x′) (y≈y′ : Eq b y y′) →
         EqW (a ⊗ b) (x , y) (x′ , y′)
  ⌈_⌉  : ∀ {A x x′} (x≡x′ : x ≡ x′) → EqW ⌈ A ⌉ x x′

⟦_⟧≈⁻¹ : ∀ {a} {x y : El a} → Eq a x y → EqP a x y
⟦ leaf                ⟧≈⁻¹ = leaf
⟦ node l≈l′ x≈x′ r≈r′ ⟧≈⁻¹ = node (♯ ⟦ ♭ l≈l′ ⟧≈⁻¹) x≈x′ (♯ ⟦ ♭ r≈r′ ⟧≈⁻¹)
⟦ x≈x′ ≺ xs≈xs′       ⟧≈⁻¹ = x≈x′ ≺ ♯ ⟦ ♭ xs≈xs′ ⟧≈⁻¹
⟦ []                  ⟧≈⁻¹ = []
⟦ x≈x′ ∷ xs≈xs′       ⟧≈⁻¹ = x≈x′ ∷ ♯ ⟦ ♭ xs≈xs′ ⟧≈⁻¹
⟦ (x≈x′ , y≈y′)       ⟧≈⁻¹ = (x≈x′ , y≈y′)
⟦ ⌈ x≡x′ ⌉            ⟧≈⁻¹ = ⌈ x≡x′ ⌉

whnf≈ : ∀ {a xs ys} → EqP a xs ys → EqW a xs ys
whnf≈ leaf                  = leaf
whnf≈ (node l≈l′ x≈x′ r≈r′) = node (♭ l≈l′) x≈x′ (♭ r≈r′)
whnf≈ (x≈x′ ≺ xs≈xs′)       = x≈x′ ≺ ♭ xs≈xs′
whnf≈ []                    = []
whnf≈ (x≈x′ ∷ xs≈xs′)       = x≈x′ ∷ ♭ xs≈xs′
whnf≈ (x≈x′ , y≈y′)         = (x≈x′ , y≈y′)
whnf≈ ⌈ x≡x′ ⌉              = ⌈ x≡x′ ⌉

whnf≈ ( _ ≊⟨ x≈y ⟩ y≈z) with whnf≈ x≈y | whnf≈ y≈z
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | leaf           | leaf            = leaf
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | node l≈l′  x≈x′  r≈r′
                        | node l′≈l″ x′≈x″ r′≈r″ = node (_ ≊⟨ l≈l′ ⟩ l′≈l″) (trans x≈x′ x′≈x″) (_ ≊⟨ r≈r′ ⟩ r′≈r″)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | []             | []              = []
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | x≈y′ ∷ xs≈ys′  | y≈z′ ∷ ys≈zs′   = trans x≈y′ y≈z′ ∷ (_ ≊⟨ xs≈ys′ ⟩ ys≈zs′)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | x≈y′ ≺ xs≈ys′  | y≈z′ ≺ ys≈zs′   = trans x≈y′ y≈z′ ≺ (_ ≊⟨ xs≈ys′ ⟩ ys≈zs′)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | (x≈x′  , y≈y′) | (x′≈x″ , y′≈y″) = (trans x≈x′ x′≈x″ , trans y≈y′ y′≈y″)
whnf≈ ( _ ≊⟨ x≈y ⟩ y≈z) | ⌈ x≡x′  ⌉      | ⌈ x′≡x″ ⌉       = ⌈ PropEq.trans x≡x′ x′≡x″ ⌉

whnf≈ (zipWith-cong cong xs≈xs′ ys≈ys′) with whnf≈ xs≈xs′ | whnf≈ ys≈ys′
... | []            | ys≈ys″        = ys≈ys″
... | x≈x′ ∷ xs≈xs″ | y≈y′ ≺ ys≈ys″ =
  cong x≈x′ y≈y′ ≺ zipWith-cong cong xs≈xs″ ys≈ys″

mutual

  value≈ : ∀ {a xs ys} → EqW a xs ys → Eq a xs ys
  value≈ leaf                  = leaf
  value≈ (node l≈l′ x≈x′ r≈r′) = node (♯ ⟦ l≈l′ ⟧≈) x≈x′ (♯ ⟦ r≈r′ ⟧≈)
  value≈ (x≈x′ ≺ xs≈xs′)       = x≈x′ ≺ ♯ ⟦ xs≈xs′ ⟧≈
  value≈ []                    = []
  value≈ (x≈x′ ∷ xs≈xs′)       = x≈x′ ∷ ♯ ⟦ xs≈xs′ ⟧≈
  value≈ (x≈x′ , y≈y′)         = (x≈x′ , y≈y′)
  value≈ ⌈ x≡x′ ⌉              = ⌈ x≡x′ ⌉

  ⟦_⟧≈ : ∀ {a xs ys} → EqP a xs ys → Eq a xs ys
  ⟦ xs≈ys ⟧≈ = value≈ (whnf≈ xs≈ys)

_≈⟨_⟩_ : ∀ {a} x {y z}
         (x≈y : Eq a x y) (y≈z : EqP a y z) → EqP a x z
x ≈⟨ x≈y ⟩ y≈z = x ≊⟨ ⟦ x≈y ⟧≈⁻¹ ⟩ y≈z

_∎ : ∀ {a} x → EqP a x x
x ∎ = ⟦ refl x ⟧≈⁻¹

------------------------------------------------------------------------
-- Productivity checker workaround for PrefixOf

infixr 2 _≋⟨_⟩_ _⊑⟨_⟩_

data PrefixOfP (a : U) :
       Colist (El a) → Stream (El a) → Set₁ where
  []       : ∀ {ys} → PrefixOfP a [] ys
  ⁺++-mono : ∀ xs {ys ys′} (ys⊑ys′ : ∞ (PrefixOfP a ys ys′)) →
             PrefixOfP a (xs ⁺++ ys) (xs ⁺++∞ ys′)
  _≋⟨_⟩_   : ∀ xs {ys zs} (xs≈ys : Eq (colist a) xs ys)
             (ys⊑zs : PrefixOfP a ys zs) → PrefixOfP a xs zs
  _⊑⟨_⟩_   : ∀ xs {ys zs} (xs⊑ys : PrefixOfP a xs ys)
             (ys≈zs : EqP (stream a) ys zs) → PrefixOfP a xs zs

data PrefixOfW (a : U) :
       Colist (El a) → Stream (El a) → Set₁ where
  []  : ∀ {ys} → PrefixOfW a [] ys
  _∷_ : ∀ {x y xs ys}
        (x≈y : Eq a x y) (p : PrefixOfP a (♭ xs) (♭ ys)) →
        PrefixOfW a (x ∷ xs) (y ≺ ys)

whnf⊑ : ∀ {a xs ys} →
        PrefixOfP a xs ys → PrefixOfW a xs ys
whnf⊑ [] = []

whnf⊑ (⁺++-mono (x ∷ [])        ys⊑ys′) = refl x ∷ ♭ ys⊑ys′
whnf⊑ (⁺++-mono (x ∷ (x′ ∷ xs)) ys⊑ys′) =
  refl x ∷ ⁺++-mono (x′ ∷ xs) ys⊑ys′

whnf⊑ (._ ≋⟨ []          ⟩ _    ) = []
whnf⊑ (._ ≋⟨ x≈y ∷ xs≈ys ⟩ ys⊑zs) with whnf⊑ ys⊑zs
... | y≈z ∷ ys⊑zs′ = trans x≈y y≈z ∷ (_ ≋⟨ ♭ xs≈ys ⟩ ys⊑zs′)

whnf⊑ (._ ⊑⟨ xs⊑ys ⟩ ys≈zs) with whnf⊑ xs⊑ys | whnf≈ ys≈zs
... | []           | _            = []
... | x≈y ∷ xs⊑ys′ | y≈z ≺ ys≈zs′ = trans x≈y y≈z ∷ (_ ⊑⟨ xs⊑ys′ ⟩ ys≈zs′)

mutual

  value⊑ : ∀ {a xs ys} → PrefixOfW a xs ys → PrefixOf a xs ys
  value⊑ []            = []
  value⊑ (x≈y ∷ xs⊑ys) = x≈y ∷ ♯ ⟦ xs⊑ys ⟧⊑

  ⟦_⟧⊑ : ∀ {a xs ys} → PrefixOfP a xs ys → PrefixOf a xs ys
  ⟦ xs⊑ys ⟧⊑ = value⊑ (whnf⊑ xs⊑ys)

------------------------------------------------------------------------
-- More lemmas

⁺++∞-cong : ∀ {a xs xs′ ys ys′} →
            Eq ⌈ List⁺ (El a) ⌉ xs xs′ →
            Eq (stream a) ys ys′ →
            Eq (stream a) (xs ⁺++∞ ys) (xs′ ⁺++∞ ys′)
⁺++∞-cong {xs = x ∷ []}        ⌈ ≡-refl ⌉ ys≈ys′ = refl x ≺ ♯ ys≈ys′
⁺++∞-cong {xs = x ∷ (x′ ∷ xs)} ⌈ ≡-refl ⌉ ys≈ys′ =
  refl x ≺ ♯ ⁺++∞-cong {xs = x′ ∷ xs} ⌈ ≡-refl ⌉ ys≈ys′

++-assoc : ∀ {a} xs ys zs →
           Eq (stream a) (xs ⁺++∞ (ys ⁺++∞ zs)) ((xs ⁺++⁺ ys) ⁺++∞ zs)
++-assoc (x ∷ [])        ys zs = refl x ≺ ♯ refl (ys ⁺++∞ zs)
++-assoc (x ∷ (x′ ∷ xs)) ys zs = refl x ≺ ♯ ++-assoc (x′ ∷ xs) ys zs

zip-++-assoc : ∀ {a} xss yss (zss : Stream (Stream (El a))) →
               Eq (stream (stream a))
                  (zipWith _⁺++∞_ ⟦ xss ⟧ (zipWith _⁺++∞_ ⟦ yss ⟧ zss))
                  (zipWith _⁺++∞_ ⟦ longZipWith _⁺++⁺_ xss yss ⟧ zss)
zip-++-assoc xss yss (zs ≺ zss) with whnf xss | whnf yss
... | []            | []            = refl _
... | []            | ys     ∷ yss′ = refl _
... | xs     ∷ xss′ | []            = refl _
... | ⌈ xs ⌉ ∷ xss′ | ⌈ ys ⌉ ∷ yss′ =
  ++-assoc xs ys zs ≺ ♯ zip-++-assoc (♭ xss′) (♭ yss′) (♭ zss)

concat-lemma : ∀ {a} xs xss →
               Eq (colist a) (concat (xs ∷ xss))
                             (xs ⁺++ concat (♭ xss))
concat-lemma (x ∷ [])        xss = refl x ∷ ♯ refl (concat (♭ xss))
concat-lemma (x ∷ (x′ ∷ xs)) xss = refl x ∷ ♯ concat-lemma (x′ ∷ xs) xss

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --cubical --no-import-sorts --safe  #-}
module Cubical.HITs.GroupoidQuotients where

open import Cubical.HITs.GroupoidQuotients.Base public
open import Cubical.HITs.GroupoidQuotients.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{-# OPTIONS --copatterns #-}

-- 2013-05-30 Andreas, Oury's counterexample to subject reduction in Coq
-- 2014-11-04 Andreas: simplified (removed force)

module MatchingOnCoinductiveRecord where

open import Common.Equality

record U : Set where
  coinductive
  constructor inn
  field
    out : U
open U

u : U
out u = u

eq : (x : U) → x ≡ inn (out x)
eq (inn y) = refl
-- should fail, as internally this is just
-- eq x = refl
-- and we do not have η for coinductive records

equ : u ≡ inn u
equ = eq u
-- normalizes to refl, which does not have type u ≡ inn u

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Sum.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Empty
open import Cubical.Data.Nat

open import Cubical.Data.Sum.Base

-- Path space of sum type
module SumPath {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where

  Cover : A ⊎ B → A ⊎ B → Type (ℓ-max ℓ ℓ')
  Cover (inl a) (inl a') = Lift {j = ℓ-max ℓ ℓ'} (a ≡ a')
  Cover (inl _) (inr _) = Lift ⊥
  Cover (inr _) (inl _) = Lift ⊥
  Cover (inr b) (inr b') = Lift {j = ℓ-max ℓ ℓ'} (b ≡ b')

  reflCode : (c : A ⊎ B) → Cover c c
  reflCode (inl a) = lift refl
  reflCode (inr b) = lift refl

  encode : ∀ c c' → c ≡ c' → Cover c c'
  encode c _ = J (λ c' _ → Cover c c') (reflCode c)

  encodeRefl : ∀ c → encode c c refl ≡ reflCode c
  encodeRefl c = JRefl (λ c' _ → Cover c c') (reflCode c)

  decode : ∀ c c' → Cover c c' → c ≡ c'
  decode (inl a) (inl a') (lift p) = cong inl p
  decode (inl a) (inr b') ()
  decode (inr b) (inl a') ()
  decode (inr b) (inr b') (lift q) = cong inr q

  decodeRefl : ∀ c → decode c c (reflCode c) ≡ refl
  decodeRefl (inl a) = refl
  decodeRefl (inr b) = refl

  decodeEncode : ∀ c c' → (p : c ≡ c') → decode c c' (encode c c' p) ≡ p
  decodeEncode c _ =
    J (λ c' p → decode c c' (encode c c' p) ≡ p)
      (cong (decode c c) (encodeRefl c) ∙ decodeRefl c)

  isOfHLevelCover : (n : ℕ)
    → isOfHLevel (suc (suc n)) A
    → isOfHLevel (suc (suc n)) B
    → ∀ c c' → isOfHLevel (suc n) (Cover c c')
  isOfHLevelCover n p q (inl a) (inl a') = isOfHLevelLift (suc n) (p a a')
  isOfHLevelCover n p q (inl a) (inr b') =
    isOfHLevelLift (suc n)
    (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
      (hLevelLift n isProp⊥))
  isOfHLevelCover n p q (inr b) (inl a') =
    isOfHLevelLift (suc n)
      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
        (hLevelLift n isProp⊥))
  isOfHLevelCover n p q (inr b) (inr b') = isOfHLevelLift (suc n) (q b b')

isOfHLevelSum : ∀ {ℓ ℓ'} (n : ℕ) {A : Type ℓ} {B : Type ℓ'}
  → isOfHLevel (suc (suc n)) A
  → isOfHLevel (suc (suc n)) B
  → isOfHLevel (suc (suc n)) (A ⊎ B)
isOfHLevelSum n lA lB c c' =
  retractIsOfHLevel (suc n)
    (SumPath.encode c c')
    (SumPath.decode c c')
    (SumPath.decodeEncode c c')
    (SumPath.isOfHLevelCover n lA lB c c')

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module Sets.PredicateSet.Finite{ℓₗ}{ℓₒ} where

import      Lvl
open import Functional
open import Logic.Propositional{ℓₗ Lvl.⊔ ℓₒ}
open import Logic.Predicate{ℓₗ}{ℓₒ}
open import Numeral.Finite
open import Numeral.Natural
import      Relator.Equals
open import Sets.PredicateSet
open import Structure.Function.Domain
open import Type{ℓₒ}

{-
record Irrelevant∃ {X : Type} (Pred : X → Stmt) : Stmt where
  field
    witness   : X
    ⦃ .proof ⦄ : Pred(witness)

record Finite {T} (S : PredSet{ℓₗ}{ℓₒ}(T)) : Stmt where
  field
    count     : ℕ
    bijection : 𝕟(count) → Irrelevant∃(x ↦ (x ∈ S))
    proof     : Bijective(bijection) -- TODO: Bijective must allow different levels
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monad.Strong where

open import Categories.Category
open import Categories.Monoidal

open import Categories.Functor
  renaming (id to idF; _∘_ to _∘F_; _≡_ to _≡F_)
open import Categories.Functor.Constant
open import Categories.NaturalTransformation
  renaming (id to idN; _≡_ to _≡N_)
open import Categories.NaturalIsomorphism
  using (module NaturalIsomorphism)
open import Categories.Monad

open import Categories.Product

open import Data.Fin using (Fin)
open import Function using (flip)
open import Data.Nat using ()
open import Data.Product using (_,_)
open import Data.Vec
  using (Vec; _∷_; []; [_]; lookup)

open import Level

record Strength
  {o ℓ e}(C : Category o ℓ e)
  (monoidal : Monoidal C)
  (M : Monad C)
  : Set (o ⊔ ℓ ⊔ e) where
  open Category C

  open Monoidal monoidal
    using (⊗)
    renaming (id to idObj)
  open NaturalIsomorphism (Monoidal.identityˡ monoidal) using () renaming (F⇒G to υˡ)
  open NaturalIsomorphism (Monoidal.identityʳ monoidal) using () renaming (F⇒G to υʳ)
  open NaturalIsomorphism (Monoidal.assoc     monoidal) using ()
    renaming (F⇒G to αʳ; F⇐G to αˡ)

  module υˡ = NaturalTransformation υˡ
  open Functor ⊗
    using ()
    renaming (F₀ to ⊗₀; F₁ to ⊗₁)

  unitorˡ : ∀ A → ⊗₀ (idObj , A) ⇒ A
  unitorˡ A = υˡ.η (flip lookup [ A ])

  associatorʳ : ∀ A B C → ⊗₀ (⊗₀ (A , B) , C) ⇒ ⊗₀ (A , ⊗₀ (B , C))
  associatorʳ A B C = NaturalTransformation.η αʳ (flip lookup (A ∷ B ∷ C ∷ []))

  associatorˡ : ∀ A B C → ⊗₀ (A , ⊗₀ (B , C)) ⇒ ⊗₀ (⊗₀ (A , B) , C)
  associatorˡ A B C = NaturalTransformation.η αˡ (flip lookup (A ∷ B ∷ C ∷ []))

  module M = Monad M
  open M using (F)
  open Functor F
    using (F₀; F₁)
  open NaturalTransformation M.η
    using (η)
  open NaturalTransformation M.μ
    using ()
    renaming (η to μ)

  field
    σ : NaturalTransformation (⊗ ∘F (idF {C = C} ⁂ F)) (F ∘F ⊗)

  module σ = NaturalTransformation σ

  field
    .identity₁ : ∀ {A}
      → F₁ (unitorˡ A) ∘ σ.η (idObj , A)
      ≡ unitorˡ (F₀ A)

    .identity₂ : ∀ {A B}
      → σ.η (A , B) ∘ ⊗₁ (id , η B)
      ≡ η (⊗₀ (A , B))

    α-assoc : ∀ {A B C}
      → F₁ (associatorʳ A B C) ∘ σ.η (⊗₀ (A , B) , C)
      ≡ σ.η (A , ⊗₀ (B , C)) ∘ ⊗₁ (id , σ.η (B , C)) ∘ associatorʳ A B (F₀ C)

    μ-assoc : ∀ {A B}
      → μ (⊗₀ (A , B)) ∘ F₁ (σ.η (A , B)) ∘ σ.η (A , F₀ B)
      ≡ σ.η (A , B) ∘ ⊗₁ (id , μ B)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories