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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.IdUPiPi {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Lambda
open import Definition.LogicalRelation.Substitution.Introductions.Application
open import Definition.LogicalRelation.Substitution.Introductions.Cast
open import Definition.LogicalRelation.Substitution.Introductions.Id
open import Definition.LogicalRelation.Substitution.Introductions.Transp
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Escape
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.ProofIrrelevance
open import Definition.LogicalRelation.Fundamental.Variable

open import Tools.Product
open import Tools.Nat
import Tools.PropositionalEquality as PE

lemma0 : ∀ σ A → (wk1 (wk1 (subst σ A))) PE.≡ subst (liftSubst (liftSubst σ)) (wk1 (wk1 A))
lemma0 σ A = PE.trans (PE.cong wk1 (PE.sym (Idsym-subst-lemma σ A))) (PE.sym (Idsym-subst-lemma (liftSubst σ) (wk1 A)))

lemma1 : ∀ {σ rA} A A' B →
                   wk1d (subst (liftSubst σ) B) [
                        cast ⁰ (wk1 (wk1 (subst σ A')))
                               (wk1 (wk1 (subst σ A)))
                               (Idsym (Univ rA ⁰) (wk1 (wk1 (subst σ A))) (wk1 (wk1 (subst σ A'))) (var 1))
                               (var 0)]↑
                   PE.≡
                     subst (liftSubst (liftSubst σ)) (U.wk (lift (step id)) B [
                     cast ⁰ (wk1 (wk1 A'))
                            (wk1 (wk1 A))
                            (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1))
                            (var 0)]↑)
lemma1 {σ} {rA} A A' B = PE.trans (PE.cong₂ (λ X Y → X [ Y ]↑) (PE.sym (Idsym-subst-lemma-wk1d σ B))
  (PE.cong₃ (λ X Y Z → cast ⁰ X Y Z (var 0)) (lemma0 σ A') (lemma0 σ A)
    (PE.trans (PE.cong₂ (λ X Y → Idsym (Univ rA ⁰) X Y (var 1)) (lemma0 σ A) (lemma0 σ A'))
    (PE.sym (subst-Idsym (liftSubst (liftSubst σ)) (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1))))))
  (PE.sym ((singleSubstLift↑ (liftSubst σ) (U.wk (lift (step id)) B) _)))

lemma2 : ∀ {σ} B → U.wk (lift (step id)) (subst (liftSubst σ) B)
                             PE.≡
                             subst (liftSubst (liftSubst σ)) (U.wk (lift (step id)) B)
lemma2 B = PE.sym (Idsym-subst-lemma-wk1d _ B)

Id-U-ΠΠ-resᵗᵛ : ∀ {A B A' B' rA Γ} ([Γ] : ⊩ᵛ Γ) →
        let l    = ∞
            lΠ = ⁰
            [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
            [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
            Id-U-ΠΠ-res A A' B B' =
                        (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                            (wk1d B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                            (wk1d B') ° ¹ ° ¹)

        in
           ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ rA , ι lΠ ] / [Γ])
           ([A'] : Γ ⊩ᵛ⟨ l ⟩ A' ^ [ rA , ι lΠ ] / [Γ])
           ([UB] : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A])
           ([UB'] : Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'])
           ([A]ₜ : Γ ⊩ᵛ⟨ l ⟩ A ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B]ₜ : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A] / (λ {Δ} {σ} → [UB] {Δ} {σ}))
           ([A']ₜ : Γ ⊩ᵛ⟨ l ⟩ A' ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B']ₜ :  Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B' ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'] / (λ {Δ} {σ} → [UB'] {Δ} {σ})) →
           let [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
               [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
               [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
               [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
               [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
               [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
               [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
               [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
               [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
               [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
               [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
               [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
               [SProp] = Uᵛ {rU = %} ∞< [ΓId]
           in
           ([var0]ₜ : (Γ ∙ Id (Univ rA ⁰) A A' ^ [ % , ι ¹ ] ∙ wk1 A' ^ [ rA , ι ⁰ ]) ⊩ᵛ⟨ ∞ ⟩ var 0 ∷ wk1 (wk1 A') ^ [ rA , ι ⁰ ] / [ΓIdA'] / [wwA']')
           ([var1]ₜ : (Γ ∙ Id (Univ rA ⁰) A A' ^ [ % , ι ¹ ] ∙ wk1 A' ^ [ rA , ι ⁰ ]) ⊩ᵛ⟨ ∞ ⟩ var 1 ∷  Id (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) ^ [ % , ι ¹ ] / [ΓIdA'] / [wwIdAA'])
         →  Γ ∙ Id (Univ rA ⁰) A A' ^ [ % , ι ¹ ] ⊩ᵛ⟨ ∞ ⟩ Id-U-ΠΠ-res  A A' B B' ∷ SProp ¹ ^ [ ! , ∞ ] / [ΓId] / (λ {Δ} {σ} → [SProp] {Δ} {σ})
Id-U-ΠΠ-resᵗᵛ {A} {B} {A'} {B'} {rA} {Γ}
        [Γ] [A] [A'] [UB] [UB'] [A]ₜ [B]ₜ [A']ₜ [B']ₜ [var0]ₜ [var1]ₜ =
  let l = ∞
      lΠ = ⁰
      [SProp] = Uᵛ {rU = %} ∞< [Γ]
      [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
      [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
      ⊢AΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A]ₜ ⊢Δ [σ]))
      ⊢A'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A']ₜ ⊢Δ [σ]))
      ⊢A = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A] {Δ} {σ} ⊢Δ [σ]))
      ⊢A' = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A'] {Δ} {σ} ⊢Δ [σ]))
      [ΓA]  = (_∙_ {Γ} {A} [Γ] [A])
      [ΓA'] = (_∙_ {Γ} {A'} [Γ]  [A'])
      ⊢BΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B]ₜ {Δ} {σ} ⊢Δ [σ]))
      [A]'  = univᵛ {A = A} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ
      [A']'  = univᵛ {A = A'} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A']ₜ
      [B]'  = univᵛ {A = B} [ΓA] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB] {Δ} {σ}) [B]ₜ
      [B]  = maybeEmbᵛ {A = B} [ΓA] [B]'
      [B']'  = univᵛ {A = B'} [ΓA'] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [B']ₜ
      [B']  = maybeEmbᵛ {A = B'} [ΓA'] [B']'
      ⊢B'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB'] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B']ₜ {Δ} {σ} ⊢Δ [σ]))
      [liftσ] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A] [σ]
      [liftσ'] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A'} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A'] [σ]
      [ΠAB] = Πᵗᵛ {A} {B} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A] (λ {Δ} {σ} → [UB] {Δ} {σ}) [A]ₜ [B]ₜ
      [ΠA'B'] = Πᵗᵛ {A'} {B'} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) [A']ₜ [B']ₜ
      [IdAA']ₜ = Idᵗᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ (Uᵗᵛ [Γ])
      [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
      Id-U-ΠΠ-res A A' B B' = ∃ (Id (Univ rA ⁰) A A') ▹
                      (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                        ((U.wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                        (U.wk (lift (step id)) B') ° ¹ ° ¹)
      [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
      [wSProp] = Uᵛ {rU = %} ∞< [ΓId]
      [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
      [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
      [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
      [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
      [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
      [wwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓIdA'] {Δ} {σ}
      [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
      [wwUA']ᵗ = Uᵗᵛ [ΓIdA']
      [ΓIdA] = _∙_ {A = wk1 A} [ΓId] [wA]'
      [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
      [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
      [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
      [wwA]' = wk1ᵛ {A = wk1 A} {F = wk1 A'}  [ΓId] [wA']' [wA]'
      [wwU0A] = maybeEmbᵛ {A = Univ ! _ } [ΓIdA] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA] {Δ} {σ})
      [wB'] = wk1dᵗᵛ {F = A'} {F' = Id (Univ rA ⁰) A A'} {G = B'} [Γ] [A'] [IdAA'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !) [B']ₜ
      [wB] = wk1dᵗᵛ {F = A} {F' = Id (Univ rA ⁰) A A'} {G = B} [Γ] [A] [IdAA'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [wwU0A] {Δ} {σ}) [B]ₜ
      [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
      [wwIdA'A] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A')} {u = wk1 (wk1 A)} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA'] [wwA]
   in Πᵗᵛ {wk1 A'} {Id (U ⁰) (U.wk (lift (step id)) B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A))
                                   (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                                              (U.wk (lift (step id)) B')} (<is≤ 0<1) (≡is≤ PE.refl) [ΓId] [wA']' (λ {Δ} {σ} → [wwU¹] {Δ} {σ} %) [wA']
                            (Idᵗᵛ {A = U ⁰} {t = (U.wk (lift (step id)) B [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A))
                                      (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)}
                                 {u = U.wk (lift (step id)) B'} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !)
                            (subst↑STerm {F = wk1 A'} {F' = wk1 A} {G = wk1d B}
                                         {t = cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0)}
                                         [ΓId] [wA']' [wA]' (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !) (λ {Δ} {σ} → [wwU0A] {Δ} {σ}) [wB]
                                         (castᵗᵛ {A = wk1 (wk1 A')} {B = wk1 (wk1 A)} {t = var 0} {e = (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1))}
                                                 [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA'] [wwA] [wwA']' [wwA]' [var0]ₜ
                                                 (Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A')} {u = wk1 (wk1 A)} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA'] [wwA])
                                                 (IdSymᵗᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} {e = var 1} [ΓIdA'] ((λ {Δ} {σ} → [wwU¹] {Δ} {σ} !))
                                                          (λ {Δ} {σ} → [wwUA']ᵗ {Δ} {σ}) (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA)
                                                          [wwA] [wwA'] [wwIdAA'] [wwIdA'A] [var1]ₜ))) [wB']
                                                          (λ {Δ} {σ} → Uᵗᵛ [ΓIdA'] {Δ} {σ}))

abstract
  Id-U-ΠΠᵗᵛ : ∀ {A B A' B' rA Γ} ([Γ] : ⊩ᵛ Γ) →
        let l    = ∞
            lΠ = ⁰
            [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
            [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
        in
           ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ rA , ι lΠ ] / [Γ])
           ([A'] : Γ ⊩ᵛ⟨ l ⟩ A' ^ [ rA , ι lΠ ] / [Γ])
           ([UB] : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A])
           ([UB'] : Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'])
           ([A]ₜ : Γ ⊩ᵛ⟨ l ⟩ A ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B]ₜ : Γ ∙ A ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A] / (λ {Δ} {σ} → [UB] {Δ} {σ}))
           ([A']ₜ : Γ ⊩ᵛ⟨ l ⟩ A' ∷ Univ rA lΠ ^ [ ! , next lΠ ] / [Γ] / [UA])
           ([B']ₜ :  Γ ∙ A' ^ [ rA , ι lΠ ] ⊩ᵛ⟨ l ⟩ B' ∷ Univ ! lΠ ^ [ ! , next lΠ ] / [Γ] ∙ [A'] / (λ {Δ} {σ} → [UB'] {Δ} {σ}))
         → [ Γ ⊩ᵛ⟨ l ⟩ (Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰))
                    ≡ ∃ (Id (Univ rA ⁰) A A') ▹
                      (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                        ((U.wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                        (U.wk (lift (step id)) B') ° ¹ ° ¹)
                  ∷ SProp ¹ ^ [ ! , next ¹ ] / [Γ] ]

  Id-U-ΠΠᵗᵛ {A} {B} {A'} {B'} {rA} {Γ} [Γ] [A] [A'] [UB] [UB'] [A]ₜ [B]ₜ [A']ₜ [B']ₜ =
    let l = ∞
        lΠ = ⁰
        [SProp] = Uᵛ {rU = %} ∞< [Γ]
        [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ emb< [Γ])
        [UΠ] = maybeEmbᵛ {A = Univ ! _} [Γ] (Uᵛ emb< [Γ])
        ⊢AΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A]ₜ ⊢Δ [σ]))
        ⊢A'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A']ₜ ⊢Δ [σ]))
        ⊢A = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A] {Δ} {σ} ⊢Δ [σ]))
        ⊢A' = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A'] {Δ} {σ} ⊢Δ [σ]))
        [ΓA]  = (_∙_ {Γ} {A} [Γ] [A])
        [ΓA'] = (_∙_ {Γ} {A'} [Γ]  [A'])
        ⊢BΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B]ₜ {Δ} {σ} ⊢Δ [σ]))
        [A]'  = univᵛ {A = A} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ
        [A']'  = univᵛ {A = A'} [Γ] (≡is≤ PE.refl) (λ {Δ} {σ} → [UA] {Δ} {σ}) [A']ₜ
        [B]'  = univᵛ {A = B} [ΓA] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB] {Δ} {σ}) [B]ₜ
        [B]  = maybeEmbᵛ {A = B} [ΓA] [B]'
        [B']'  = univᵛ {A = B'} [ΓA'] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [B']ₜ
        [B']  = maybeEmbᵛ {A = B'} [ΓA'] [B']'
        ⊢B'Δ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB'] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B']ₜ {Δ} {σ} ⊢Δ [σ]))
        [liftσ] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A] [σ]
        [liftσ'] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A'} {σ = σ} {Δ = Δ} [Γ] ⊢Δ [A'] [σ]
        [ΠAB] = Πᵗᵛ {A} {B} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A] (λ {Δ} {σ} → [UB] {Δ} {σ}) [A]ₜ [B]ₜ
        [ΠA'B'] = Πᵗᵛ {A'} {B'} (≡is≤ PE.refl) (≡is≤ PE.refl) [Γ] [A'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) [A']ₜ [B']ₜ
        [IdAA']ₜ = Idᵗᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ (Uᵗᵛ [Γ])
        [IdAA'] = Idᵛ {A = Univ rA ⁰} {t = A} {u = A'} [Γ] (λ {Δ} {σ} → [UA] {Δ} {σ}) [A]ₜ [A']ₜ
        Id-U-ΠΠ-res A A' B B' = ∃ (Id (Univ rA ⁰) A A') ▹
                         (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                         ((U.wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                         (U.wk (lift (step id)) B') ° ¹ ° ¹)
        [ΓId] = _∙_ {A = Id (Univ rA ⁰) A A'} [Γ] [IdAA']
        [wSProp] = Uᵛ {rU = %} ∞< [ΓId]
        [wA'] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A'} {lG = ⁰} [Γ] [IdAA'] [A']ₜ
        [wA']' = wk1ᵛ {A = A'} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A']
        [wA]' = wk1ᵛ {A = A} {F = Id (Univ rA ⁰) A A'} [Γ] [IdAA'] [A]
        [wA] = wk1ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = A} {lG = ⁰} [Γ] [IdAA'] [A]ₜ
        [ΓIdA'] = _∙_ {A = wk1 A'} [ΓId] [wA']'
        [wwU¹] = λ {Δ} {σ} r → Uᵛ {rU = r} ∞< [ΓIdA'] {Δ} {σ}
        [wwUA'] = λ {Δ} {σ} r → maybeEmbᵛ {A = Univ r _ } [ΓIdA'] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA'] {Δ} {σ}) {Δ} {σ}
        [ΓIdA] = _∙_ {A = wk1 A} [ΓId] [wA]'
        [wwA'] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A'} {lG = ⁰} [ΓId] [wA']' [wA']
        [wwA] = wk1ᵗᵛ {F = wk1 A'} {G = wk1 A} {lG = ⁰} [ΓId] [wA']' [wA]
        [wwA']' = wk1ᵛ {A = wk1 A'} {F = wk1 A'}  [ΓId] [wA']' [wA']'
        [wwA]' = wk1ᵛ {A = wk1 A} {F = wk1 A'}  [ΓId] [wA']' [wA]'
        [wwU0A] = maybeEmbᵛ {A = Univ ! _ } [ΓIdA] (λ {Δ} {σ} → Uᵛ emb< [ΓIdA] {Δ} {σ})
        [wB'] = wk1dᵗᵛ {F = A'} {F' = Id (Univ rA ⁰) A A'} {G = B'} [Γ] [A'] [IdAA'] (λ {Δ} {σ} → [UB'] {Δ} {σ}) (λ {Δ} {σ} → [wwUA'] {Δ} {σ} !) [B']ₜ
        [wB] = wk1dᵗᵛ {F = A} {F' = Id (Univ rA ⁰) A A'} {G = B} [Γ] [A] [IdAA'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [wwU0A] {Δ} {σ}) [B]ₜ
        [wwIdAA'] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A)} {u = wk1 (wk1 A')} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA] [wwA']
        [wwIdA'A] = Idᵛ {A = Univ rA ⁰} {t = wk1 (wk1 A')} {u = wk1 (wk1 A)} [ΓIdA'] (λ {Δ} {σ} → [wwUA'] {Δ} {σ} rA) [wwA'] [wwA]
        [var0]ₜ : (Γ ∙ Id (Univ rA ⁰) A A' ^ [ % , ι ¹ ] ∙ wk1 A' ^ [ rA , ι ⁰ ]) ⊩ᵛ⟨ ∞ ⟩ var 0 ∷ wk1 (wk1 A') ^ [ rA , ι ⁰ ] / [ΓIdA'] / [wwA']'
        [var0]ₜ = proj₂ (fundamentalVar here [ΓIdA'])
        [var1]ₜ : (Γ ∙ Id (Univ rA ⁰) A A' ^ [ % , ι ¹ ] ∙ wk1 A' ^ [ rA , ι ⁰ ]) ⊩ᵛ⟨ ∞ ⟩ var 1 ∷  Id (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) ^ [ % , ι ¹ ] / [ΓIdA'] / [wwIdAA']
        [var1]ₜ = let X = fundamentalVar (there here) [ΓIdA'] in S.irrelevanceTerm {A = Id (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A'))} {t = var 1}
                                                                                [ΓIdA'] [ΓIdA'] (proj₁ X) [wwIdAA'] (proj₂ X)
        [Id-U-ΠΠ-res] : Γ ⊩ᵛ⟨ ∞ ⟩ Id-U-ΠΠ-res  A A' B B' ∷ SProp ¹ ^ [ ! , ∞ ] / [Γ] / [SProp]
        [Id-U-ΠΠ-res] = ∃ᵗᵛ {F = Id (Univ rA ⁰) A A'} {G = (Π (wk1 A') ^ rA ° ⁰ ▹ Id (U ⁰)
                            ((U.wk (lift (step id)) B) [ cast ⁰ (wk1 (wk1 A')) (wk1 (wk1 A)) (Idsym (Univ rA ⁰) (wk1 (wk1 A)) (wk1 (wk1 A')) (var 1)) (var 0) ]↑)
                            (U.wk (lift (step id)) B') ° ¹ ° ¹)} [Γ] [IdAA'] (λ {Δ} {σ} → [wSProp] {Δ} {σ}) [IdAA']ₜ
                            (Id-U-ΠΠ-resᵗᵛ {A} {B} {A'} {B'} [Γ] [A] [A'] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [A]ₜ [B]ₜ [A']ₜ [B']ₜ [var0]ₜ [var1]ₜ)
        [Id-U-ΠΠ] : Γ ⊩ᵛ Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰) ⇒ Id-U-ΠΠ-res A A' B B' ∷ SProp ¹ ^ ∞  / [Γ]
        [Id-U-ΠΠ] = λ {Δ} {σ} ⊢Δ [σ] → let Aσ  = ⊢AΔ {Δ} {σ} ⊢Δ [σ]
                                           Bσ = ⊢BΔ {Δ ∙ subst σ A ^ _} {liftSubst σ} (⊢Δ ∙ ⊢A {Δ} {σ} ⊢Δ [σ]) ([liftσ] {Δ} {σ} ⊢Δ [σ])
                                           A'σ = ⊢A'Δ {Δ} {σ} ⊢Δ [σ]
                                           B'σ = ⊢B'Δ {Δ ∙ subst σ A' ^ _} {liftSubst σ} (⊢Δ ∙ ⊢A' {Δ} {σ} ⊢Δ [σ]) ([liftσ'] {Δ} {σ} ⊢Δ [σ])
                                           X : Δ ⊢ Id (U ⁰) (Π (subst σ A) ^ rA ° ⁰ ▹ (subst (liftSubst σ) B) ° ⁰ ° ⁰) (Π (subst σ A') ^ rA ° ⁰ ▹ (subst (liftSubst σ) B') ° ⁰ ° ⁰)
                                                   ⇒ Id-U-ΠΠ-res (subst σ A) (subst σ A') (subst (liftSubst σ) B) (subst (liftSubst σ) B')
                                                   ∷ SProp ¹ ^ ∞
                                           X = Id-U-ΠΠ {Δ} {subst σ A} {subst σ A'} {rA} {subst (liftSubst σ) B} {subst (liftSubst σ) B'} Aσ Bσ A'σ B'σ
                                       in  PE.subst (λ BB → Δ ⊢ Id (U ⁰) (Π (subst σ A) ^ rA ° ⁰ ▹ (subst (liftSubst σ) B) ° ⁰ ° ⁰) (Π (subst σ A') ^ rA ° ⁰ ▹ (subst (liftSubst σ) B') ° ⁰ ° ⁰)
                                                                   ⇒ BB  ∷ SProp ¹ ^ ∞ )
                                                    (PE.cong₃ (λ X Y Z → ∃ Id (Univ rA ⁰) (subst σ A) (subst σ A') ▹ Π X ^ rA ° ⁰ ▹ Id (U ⁰) Y Z ° ¹ ° ¹)
                                                              ((PE.sym (Idsym-subst-lemma σ A'))) (lemma1 A A' B) (lemma2 B'))  X
        [id] , [eq] = redSubstTermᵛ {SProp ¹} {Id (U ⁰) (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰) (Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰)} {Id-U-ΠΠ-res A A' B B'}
                                    [Γ] [Id-U-ΠΠ]
                                    (λ {Δ} {σ} → [SProp] {Δ} {σ}) [Id-U-ΠΠ-res]
    in modelsTermEq [SProp] [id] [Id-U-ΠΠ-res] [eq]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
module GUIgeneric.GUIModel where

open import GUIgeneric.Prelude renaming (inj₁ to secondButton; inj₂ to firstButton; WxColor to Color) hiding (IOInterfaceˢ)

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add) --; ComponentEls to Frame)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.writingOOsUsingIOVers4ReaderMethods
open import StateSizedIO.Base
open import GUIgeneric.GUIExample -- hiding (HandlerGUIObject)

open IOInterfaceˢ public

open import Data.Product

-- How many trivial io commands such as putStrLn are ignored in the model
skippedIOcmds : ℕ
skippedIOcmds = 2

data MethodStarted
        (f : Frame)
        (prop : properties f)
        (obj : HandlerObject ∞ f) : Set where
   notStarted : MethodStarted f prop obj
   started :    (m    : methodsG f)
                (pr : IO' GuiLev1Interface ∞ StateAndGuiObj)
                → MethodStarted f prop obj

data ModelGuiState : Set where
   state : (f       : Frame)
           (prop    : properties f)
           (obj     : HandlerObject ∞ f)
           (m       : MethodStarted f prop obj)
           → ModelGuiState

modelGuiCommand : (s : ModelGuiState) → Set
modelGuiCommand  (state g prop obj notStarted)
                 = methodsG g
modelGuiCommand  (state g prop obj (started m (do' c f)))
    = GuiLev1Response c
modelGuiCommand  (state g prop obj
                       (started m (return' a)))
                 = ⊤

-- modelGuiResponse : Set
-- modelGuiResponse = ⊤

handlerReturnTypeToStateAndGuiObj :
          (g       : Frame)
          (prop    : properties g)
          (obj     : HandlerObject ∞ g)
          (res :  Σ[ r ∈ returnType g ]
                  IOObjectˢ GuiLev1Interface handlerInterface ∞ (nextStateFrame g r))
           → StateAndGuiObj
handlerReturnTypeToStateAndGuiObj g prop obj (noChange , obj') = g , prop , obj'
handlerReturnTypeToStateAndGuiObj g prop obj (changedAttributes prop' , obj') = g , prop' , obj'
handlerReturnTypeToStateAndGuiObj g prop obj (changedGUI g' prop' , obj') = g' , prop' , obj'

modelGuiNextProgramStarted : (g : Frame)
                             (prop : properties g)
                             (obj  : HandlerObject ∞ g)
                             (m    : methodsG g)
                             → IO GuiLev1Interface ∞ StateAndGuiObj
modelGuiNextProgramStarted g prop obj m =
     fmap ∞  (handlerReturnTypeToStateAndGuiObj g prop obj ) (obj .method m)

modelGuiNextProgramStarted' : (g : Frame)
                             (prop : properties g)
                             (obj  : HandlerObject ∞ g)
                             (m    : methodsG g)
                             → IO' GuiLev1Interface ∞ StateAndGuiObj
modelGuiNextProgramStarted' s prop obj m = force (modelGuiNextProgramStarted s prop obj m)

modelGuiNextaux : (g : Frame)(prop : properties g)(obj : HandlerObject ∞ g)
                  (m : methodsG g)(pr : IO' GuiLev1Interface ∞ StateAndGuiObj)
                  (skippedCms : ℕ)
                  → ModelGuiState
modelGuiNextaux g prop obj m (do' (putStrLn s) f) (suc n) =
    modelGuiNextaux g prop obj m (force (f _)) n
modelGuiNextaux g prop obj m (do' c' f) n =
        state g prop obj (started m (do' c' f))
modelGuiNextaux g prop obj m (return' (gNew , propNew , objNew)) n =
        state gNew propNew objNew notStarted

modelGuiNext : (s : ModelGuiState)
               (c : modelGuiCommand s)
               → ModelGuiState
modelGuiNext (state g prop obj notStarted) m     =
       modelGuiNextaux g prop obj m  (modelGuiNextProgramStarted' g prop obj m) skippedIOcmds
modelGuiNext (state g prop obj (started m (do' c' f))) c =
       modelGuiNextaux g prop obj m (force (f c)) skippedIOcmds
modelGuiNext (state g prop obj (started m (return' (gNew , propNew , objNew)))) c =
       state gNew propNew objNew notStarted

modelGuiInterface : IOInterfaceˢ
IOStateˢ   modelGuiInterface         = ModelGuiState
Commandˢ   modelGuiInterface         = modelGuiCommand
Responseˢ  modelGuiInterface  s m    = ⊤
IOnextˢ    modelGuiInterface  s m r  = modelGuiNext s m

_-gui->_ : (s s' : ModelGuiState ) → Set
s -gui-> s' = IOˢindₚ modelGuiInterface ⊤  s s'

data _-gui->¹_ (s : ModelGuiState )
               : (s' : ModelGuiState)→ Set where
   step :  (c : modelGuiCommand s)
           → s -gui->¹ modelGuiNext s c

nextGui : (s : ModelGuiState)(c : modelGuiCommand s) → ModelGuiState
nextGui s c = modelGuiNext s c

modelToIOprog : (s : ModelGuiState) → Maybe (IO' GuiLev1Interface ∞ StateAndGuiObj)
modelToIOprog (state g prop obj notStarted) = nothing
modelToIOprog (state g prop obj (started s pr)) = just pr

nextGuiProg : (s : ModelGuiState)(c : modelGuiCommand s)
              → Maybe (IO' GuiLev1Interface ∞ StateAndGuiObj)
nextGuiProg s c = modelToIOprog (nextGui s c)

ext: agda

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
open import Coinduction using ( ∞ ; ♭ ; ♯_ )
open import Data.Bool using ( Bool ; true ; false )
open import Data.Nat using ( ℕ ; zero ; suc )
open import Data.Natural using ( Natural ; # ; % ; _+_ )
open import Data.Strict using ( Strict ; ! )
open import System.IO.Transducers.List using ( S⊆S&*T )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; out* ; _[&]_ ; _⟫_ )
open import System.IO.Transducers.Session using ( I ; Σ ; ⟨_⟩ ; _&_ ; ¿ ; * ; _&*_ )
open import System.IO.Transducers.Trace using ( [] ; _∷_ ; _≤_ )

module System.IO.Transducers.Stateful where

-- We apply the usual state transformer construction
-- for a premonoial category: morphisms
-- from T to U with state S are just regular morphisms
-- from T & S to U & S.

-- We are particularly interested in the case where T is I
-- and S is Bytes, since this collapses to Bytes ⇒ U & Bytes,
-- that is, the type for a parser over a byte stream.

-- The type Bytes ⇒ U & Bytes (or more generally * ⟨ B ⟩ ⇒ U & * ⟨ B ⟩)
-- is the type of an iteratee returning U.

-- Lookahead.

-- Lookahead buffers up all input until some output is produced.
-- If the output is (just x), then we discard the buffer, and
-- continue with the process. If the output is nothing, then we
-- return the buffer to the output stream and discard the process.

lookahead¿' : ∀ {T S S'} → (S' ≤ S) → (S' ⇒ ¿ T & S) → (S' ⇒ ¿ T & S)
lookahead¿' {T} as (inp F)       = inp (♯ λ a → lookahead¿' {T} (a ∷ as) (♭ F a))
lookahead¿' {T} as (out true P)  = out true P
lookahead¿' {T} as (out false P) = out false (out* as done)
lookahead¿' {T} as (done)        = inp (♯ λ a → lookahead¿' {T} (a ∷ as) (out a done))

lookahead¿ : ∀ {T S} → (S ⇒ ¿ T & S) → (S ⇒ ¿ T & S)
lookahead¿ {T} = lookahead¿' {T} []

lookahead*' : ∀ {T S S'} → (S' ≤ S) → (S' ⇒ * T & S) → (S' ⇒ * T & S)
lookahead*' {T} as (inp F)       = inp (♯ λ a → lookahead*' {T} (a ∷ as) (♭ F a))
lookahead*' {T} as (out true P)  = out true P
lookahead*' {T} as (out false P) = out false (out* as done)
lookahead*' {T} as (done)        = inp (♯ λ a → lookahead*' {T} (a ∷ as) (out a done))

lookahead* : ∀ {T S} → (S ⇒ * T & S) → (S ⇒ * T & S)
lookahead* {T} = lookahead*' {T} []

-- Iteration structure.

-- Deep breath.

-- This is the trickiest bit of building a stateful transducer
-- library. The idea is to turn a stateful transducer generating
-- an optional U into a stateful transducer generating many Us.
-- We transform the transducer P into one which runs P, then
-- if P returns nothing, then loop P returns nothing and terminates, and
-- if P returns (just x), then loop P finishes running P, then runs loop P again.

-- For example, given a function nat? : ℤ → (Maybe ℕ) which
-- such that nat? n = nothing if n < 0 and just n otherwise,
-- we can define:

-- loop (lookahead (inp (♯ λ n → out (nat? n) done))) :
-- * ⟨ ℤ ⟩ ⇒ * ⟨ ℕ ⟩ & * ⟨ ℤ ⟩

-- This transducer will return the longest non-negative prefix
-- of its input, for example on input just 2 ∷ just 5 ∷ just -3 ∷ ...
-- it will produce output just 2 ∷ just 5 ∷ nothing ∷ just -3 ∷ ...

mutual

  -- This is a remarkably obscure piece of code, given that all its doing is wiring...

  -- The n : ℕ parameter is the induction scheme that gets it all to pass the
  -- termination checker. When loop P is used properly, it is with a contracting
  -- P, that is one which produces stricly fewer S tokens than it consumes.
  -- Without the n parameter, loop P could produce infinite output if P isn't
  -- contracting. For example loop (out (just x) done) would just produce the stream
  -- (just x) ∷ (just x) ∷ ... without ever consuming any input. With the n parameter
  -- we keep track of how many tokens have been consumed. If we ever hit
  -- a loop where n==0, we just run P one last time, then terminate.
  -- For example, loop (out (just x) done) just produces the trace (just x) ∷ [].

  -- For efficiency, we also pass n around as a Natural, not just an ℕ. When we
  -- read input a, we add the weight of a onto n, strictly (in order to
  -- avoid potentially keeping a live), discard the previous ℕ and build a new ℕ.
  -- It would be nice to have an induction scheme for Natural.

  -- It would be a bit nicer to track statically which processes are contractions,
  -- and only allow loop P on contraction maps.

  -- Note that contractions come up in many contexts with treatments of recursion,
  -- for example in Plotkin uniformity, they're called strict maps. They're
  -- closely related to the notion of guarded recursion which is used in checking
  -- productivity of coinductive functions in Agda.

  -- TODO: Find a way to statically enforce contraction and non-expansion maps.
  -- Or alternatively, give in and allow coinductive output,
  -- and hence lose termination for transducers.

  -- TODO: Present this as a trace structure? Show that
  -- it has the expected properties on contracting morphisms.

  -- loop''' 0 P Q R is equivant to P ⟫ Q ⟫ (done ⟨&⟩ loop R)

  loop'''' : ∀ {T T' U S S'} → (Strict Natural) → (U ⇒ S) → (S ⇒ T' & S') → (S' ⇒ ¿ T & S') → (U ⇒ (T' &* T) & S')
  loop'''' {T} {T'} (! n) P Q R = loop''' {T} {T'} (% n) n P Q R

  loop''' : ∀ {T T' U S S'} → ℕ → Natural → (U ⇒ S) → (S ⇒ T' & S') → (S' ⇒ ¿ T & S') → (U ⇒ (T' &* T) & S')
  loop''' {T} {I}             m n P         Q         R = loop' {T} m n (P ⟫ Q) R R
  loop''' {T} {Σ V F} {Σ W G} m n (inp P)   (inp Q)   R = inp (♯ λ a → loop'''' {T} {Σ V F} (! (n + W a)) (♭ P a) (inp Q) R)
  loop''' {T} {Σ V F}         m n (out a P) (inp Q)   R = loop''' {T} {Σ V F} m n P (♭ Q a) R
  loop''' {T} {Σ V F} {Σ W G} m n done      (inp P)   R = inp (♯ λ a → loop'''' {T} {Σ V F} (! (n + W a)) done (♭ P a) R)
  loop''' {T} {Σ V F}         m n P         (out b Q) R = out b (loop''' {T} {♭ F b} m n P Q R)
  loop''' {T} {Σ V F} {Σ W G} m n (inp P)   done      R = inp (♯ λ a → loop'''' {T} {Σ V F} (! (n + W a)) (♭ P a) done R)
  loop''' {T} {Σ V F}         m n (out a P) done      R = out a (loop''' {T} {♭ F a} m n P done R)
  loop''' {T} {Σ V F}         m n done      done      R = inp (♯ λ a → out a (loop'''' {T} {♭ F a} (! (n + (V a))) done done R))

  -- loop' 0 P Q R is equivalent to P ⟫ Q ⟫ loop R ⟨¿⟩ done

  loop'' : ∀ {T U S S'} → (Strict Natural) → (U ⇒ S) → (S ⇒ ¿ T & S') → (S' ⇒ ¿ T & S') → (U ⇒ * T & S')
  loop'' {T} (! n) P Q R = loop' {T} (% n) n P Q R

  loop' : ∀ {T U S S'} → ℕ → Natural → (U ⇒ S) → (S ⇒ ¿ T & S') → (S' ⇒ ¿ T & S') → (U ⇒ * T & S')
  loop' {T} {Σ V F} m       n (inp P)   (inp Q)       R = inp (♯ λ a → loop'' {T} (! (n + V a)) (♭ P a) (inp Q) R)
  loop' {T}         m       n (out a P) (inp Q)       R = loop' {T} m n P (♭ Q a) R
  loop' {T} {Σ V F} m       n done      (inp Q)       R = inp (♯ λ a → loop'' {T} (! (n + V a)) done (♭ Q a) R)
  loop' {T}         zero    n P         (out true Q)  R = out true (P ⟫ Q ⟫ S⊆S&*T {T} [&] done)
  loop' {T}         (suc m) n P         (out true Q)  R = out true (loop''' {T} {T} m n P Q R)
  loop' {T}         m       n P         (out false Q) R = out false (P ⟫ Q)
  loop' {T} {Σ V F} m       n (inp P)   done          R = inp (♯ λ a → loop'' {T} (! (n + V a)) (♭ P a) done R)
  loop' {T}         m       n (out a P) done          R = loop' {T} m n P (out a done) R
  loop' {T}         m       n done      done          R = inp (♯ λ a → loop'' {T} (! (n + # 1)) done (out a done) R)

loop : ∀ {T S} → (S ⇒ ¿ T & S) → (S ⇒ * T & S)
loop {T} P = loop' {T} zero (# 0) done P P

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
open import Data.Product using (_×_; _,_)

open import IMP
open import OperationalSemantics
open import Hoare

soundness : ∀{P Q : assn} {c}
          → ⊢[ P ] c [ Q ]
          → ⊨[ P ] c [ Q ]
soundness Skip p Skip = p
soundness Loc p Loc = p
soundness (Comp r r₁) p (Comp z z₁) = soundness r₁ (soundness r p z) z₁
soundness (If r r₁) p (IfTrue x s) = soundness r (p , x) s
soundness (If r r₁) p (IfFalse x s) = soundness r₁ (p , x) s
soundness (While r) p (WhileFalse x₁) = p , x₁
soundness (While r) p (WhileTrue x₁ s s₁) = soundness (While r) (soundness r (p , x₁) s) s₁
soundness (Conseq x₁ r x₂) {s₁} {t} p s = x₂ t (soundness r (x₁ s₁ p) s)

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


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

open import Cubical.Data.Int.Base public

open import Cubical.Data.Int.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2016-06-26 issue #2066, reported by Mietek Bak
-- already fixed on stable-2.5

open import Data.Nat using (ℕ ; zero ; suc ; _≟_)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_ ; _≢_ ; refl)
open import Relation.Nullary using (yes ; no)

data Tm : Set where
  var : ℕ → Tm
  lam : ℕ → Tm → Tm
  app : Tm → Tm → Tm

data _∥_ (x : ℕ) : Tm → Set where
  var∥  : ∀ {y} → y ≢ x → x ∥ var y
  ≡lam∥ : ∀ {t} → x ∥ lam x t
  ≢lam∥ : ∀ {y t} → x ∥ t → x ∥ lam y t
  app∥  : ∀ {t u} → x ∥ t → x ∥ u → x ∥ app t u

_∥?_ : Decidable _∥_
x ∥? var y with y ≟ x
x ∥? var .x | yes refl = no (λ { (var∥ x≢x) → x≢x refl })
x ∥? var y  | no  y≢x  = yes (var∥ y≢x)
x ∥? lam y t with y ≟ x | x ∥? t
x ∥? lam .x t | yes refl | _       = yes ≡lam∥
x ∥? lam y  t | no  y≢x  | yes x∥t = yes (≢lam∥ x∥t)
x ∥? lam y  t | no  y≢x  | no  x∦t = no (λ { ≡lam∥ → {!!} ; (≢lam∥ p) → {!!} })
x ∥? app t u with x ∥? t | x ∥? u
x ∥? app t u | yes x∥t | yes x∥u = yes (app∥ x∥t x∥u)
x ∥? app t u | no  x∦t | _       = no (λ { (app∥ x∥t x∥u) → x∦t x∥t })
x ∥? app t u | _       | no  x∦u = no (λ { (app∥ x∥t x∥u) → x∦u x∥u })

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2012-03-08
module NoNoTerminationCheck where

{-# NO_TERMINATION_CHECK #-}
f : Set
f = f

-- the pragma should not extend to the following definition

g : Set
g = g

-- error: non-termination

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- {-# OPTIONS -v tc.meta:30 #-}
{-# OPTIONS --show-implicit --show-irrelevant #-}
module Issue629a where

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

uncurry : {A : Set} {B : A → Set} {C : ∃ B → Set} →
          ((x : A) (y : B x) → C (x , y)) →
          ((p : ∃ B) → C p)
uncurry f (x , y) = f x y

foo : {A : Set} {B : A → Set} → ∃ B → ∃ B
foo = uncurry λ x y → (x , y)


text:
module Fin where

import Nat
import Bool

open Nat hiding (_==_; _<_)
open Bool

data FZero : Set where

data FSuc (A : Set) : Set where
  fz : FSuc A
  fs : A -> FSuc A

mutual

  Fin' : Nat -> Set
  Fin' zero    = FZero
  Fin' (suc n) = FSuc (Fin n)

  data Fin (n : Nat) : Set where
    fin : Fin' n -> Fin n

fzero : {n : Nat} -> Fin (suc n)
fzero = fin fz

fsuc : {n : Nat} -> Fin n -> Fin (suc n)
fsuc n = fin (fs n)

_==_ : {n : Nat} -> Fin n -> Fin n -> Bool
_==_ {zero}  (fin ())     (fin ())
_==_ {suc n} (fin fz)     (fin fz)     = true
_==_ {suc n} (fin (fs i)) (fin (fs j)) = i == j
_==_ {suc n} (fin fz)     (fin (fs j)) = false
_==_ {suc n} (fin (fs i)) (fin fz)     = false

subst : {n : Nat}{i j : Fin n} -> (P : Fin n -> Set) -> IsTrue (i == j) -> P i -> P j
subst {zero}  {fin ()}     {fin ()}     P _  _
subst {suc n} {fin fz}     {fin fz}     P eq pi = pi
subst {suc n} {fin (fs i)} {fin (fs j)} P eq pi = subst (\z -> P (fsuc z)) eq pi
subst {suc n} {fin fz}     {fin (fs j)} P () _
subst {suc n} {fin (fs i)} {fin fz}     P () _

_<_ : {n : Nat} -> Fin n -> Fin n -> Bool
_<_ {zero}  (fin ())     (fin ())
_<_ {suc n} _            (fin fz)     = false
_<_ {suc n} (fin fz)     (fin (fs j)) = true
_<_ {suc n} (fin (fs i)) (fin (fs j)) = i < j

fromNat : (n : Nat) -> Fin (suc n)
fromNat  zero   = fzero
fromNat (suc n) = fsuc (fromNat n)

liftSuc : {n : Nat} -> Fin n -> Fin (suc n)
liftSuc {zero}  (fin ())
liftSuc {suc n} (fin fz)     = fin fz
liftSuc {suc n} (fin (fs i)) = fsuc (liftSuc i)

lift+ : {n : Nat}(m : Nat) -> Fin n -> Fin (m + n)
lift+  zero   i = i
lift+ (suc m) i = liftSuc (lift+ m i)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

Definition of the Klein bottle as a HIT

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.KleinBottle.Base where

open import Cubical.Core.Everything

data KleinBottle : Type where
  point : KleinBottle
  line1 : point ≡ point
  line2 : point ≡ point
  square : PathP (λ i → line1 (~ i) ≡ line1 i) line2 line2


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

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

-- LBFT monad used by implementation,
-- and functions to facilitate reasoning about it.

module LibraBFT.ImplShared.LBFT where

open import Dijkstra.RWS
open import Haskell.Modules.RWS public
open import Haskell.Modules.RWS.Lens public
open import Haskell.Modules.RWS.RustAnyHow
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import Util.Prelude

----------------
-- LBFT Monad --
----------------

-- Global 'LBFT'; works over the whole state.
LBFT : Set → Set₁
LBFT = RWS Unit Output RoundManager

act : Output → LBFT Unit
act x = tell (x ∷ [])

LBFT-run : ∀ {A} → LBFT A → RoundManager → (A × RoundManager × List Output)
LBFT-run m = RWS-run m unit

LBFT-result : ∀ {A} → LBFT A → RoundManager → A
LBFT-result m rm = proj₁ (LBFT-run m rm)

LBFT-post : ∀ {A} → LBFT A → RoundManager → RoundManager
LBFT-post m rm = proj₁ (proj₂ (LBFT-run m rm))

LBFT-outs : ∀ {A} → LBFT A → RoundManager → List Output
LBFT-outs m rm = proj₂ (proj₂ (LBFT-run m rm))

LBFT-Pre  = RoundManager → Set
LBFT-Post = RWS-Post Output RoundManager

LBFT-Post-True : ∀ {A} → LBFT-Post A → LBFT A → RoundManager → Set
LBFT-Post-True Post m pre =
  let (x , post , outs) = LBFT-run m pre in
  Post x post outs

LBFT-weakestPre : ∀ {A} (m : LBFT A)
                  → LBFT-Post A → LBFT-Pre
LBFT-weakestPre m Post pre = RWS-weakestPre m Post unit pre

LBFT-Contract : ∀ {A} (m : LBFT A) → Set₁
LBFT-Contract{A} m =
  (Post : RWS-Post Output RoundManager A)
  → (pre : RoundManager) → LBFT-weakestPre m Post pre
  → LBFT-Post-True Post m pre

LBFT-contract : ∀ {A} (m : LBFT A) → LBFT-Contract m
LBFT-contract m Post pre pf = RWS-contract m Post unit pre pf

LBFT-⇒
  : ∀ {A} {P Q : LBFT-Post A}
  → ∀ m pre → LBFT-weakestPre m P pre
  → RWS-Post-⇒ P Q
  → LBFT-weakestPre m Q pre
LBFT-⇒ m pre pf f = RWS-⇒ m unit pre pf f

LBFT-⇒-bind
  : ∀ {A B} (P : LBFT-Post A) (Q : LBFT-Post B) (f : A → LBFT B)
  → (RWS-Post-⇒ P (RWS-weakestPre-bindPost unit f Q))
  → ∀ m st → LBFT-weakestPre m P st → LBFT-weakestPre (m >>= f) Q st
LBFT-⇒-bind Post Q f pf m st con = RWS-⇒-bind {P = Post} {Q} {f} m unit st con pf

LBFT-⇒-ebind
  : ∀ {A B C} {P : LBFT-Post (Either C A)} {Q : LBFT-Post (Either C B)}
  → {f : A → LBFT (Either C B)}
  → ∀ m st → LBFT-weakestPre m P st
  → RWS-Post-⇒ P (RWS-weakestPre-ebindPost unit f Q)
  → LBFT-weakestPre (m ∙?∙ f) Q st
LBFT-⇒-ebind {P = Post} {Q} {f} m st con pf =
  RWS-⇒-ebind m unit st con pf


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

open import HoTT
open import homotopy.EilenbergMacLane
open import homotopy.EilenbergMacLane1
open import homotopy.SmashFmapConn
open import homotopy.IterSuspSmash
open import homotopy.EilenbergMacLaneFunctor
open import cohomology.CupProduct.OnEM.InLowDegrees
open import cohomology.CupProduct.OnEM.InLowDegrees2
open import cohomology.CupProduct.OnEM.InAllDegrees
open import cohomology.CupProduct.OnEM.CommutativityInLowDegrees using (⊙×-cp₀₀-comm)
open import cohomology.CupProduct.OnEM.CommutativityInLowDegrees2

module cohomology.CupProduct.OnEM.CommutativityInAllDegrees where

module _ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  open EMExplicit

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G

  private
    ⊙×-cp₀ₕ'-comm : ∀ (n : ℕ)
      → ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ◃⊙∘
        ⊙×-cp₀ₕ' G H n ◃⊙idf
        =⊙∘
        ⊙×-cpₕ₀' H G n ◃⊙∘
        ⊙×-swap ◃⊙idf
    ⊙×-cp₀ₕ'-comm n = =⊙∘-in $
      →-⊙→-uncurry (λ g → ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ⊙∘
                          ⊙EM-fmap H G⊗H.abgroup (G⊗H.ins-r-hom g) (S n))
        =⟨ (ap →-⊙→-uncurry $ λ= $ λ g →
           ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ⊙∘
           ⊙EM-fmap H G⊗H.abgroup (G⊗H.ins-r-hom g) (S n)
             =⟨ ! (⊙EM-fmap-∘ H G⊗H.abgroup H⊗G.abgroup G⊗H.swap (G⊗H.ins-r-hom g) (S n)) ⟩
           ⊙EM-fmap H H⊗G.abgroup (G⊗H.swap ∘ᴳ G⊗H.ins-r-hom g) (S n)
             =⟨ ap (λ φ → ⊙EM-fmap H H⊗G.abgroup φ (S n)) $
                group-hom= {φ = G⊗H.swap ∘ᴳ G⊗H.ins-r-hom g} {ψ = H⊗G.ins-l-hom g} $
                λ= $ G⊗H.swap-β g ⟩
           ⊙EM-fmap H H⊗G.abgroup (H⊗G.ins-l-hom g) (S n) =∎)
         ⟩
      →-⊙→-uncurry (λ g → ⊙EM-fmap H H⊗G.abgroup (H⊗G.ins-l-hom g) (S n)) =∎

  ⊙×-cp₀ₕ-comm : ∀ (n : ℕ)
    → ⊙transport (⊙EM H⊗G.abgroup) (+-comm O (S n)) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ◃⊙∘
      ⊙×-cp₀ₕ G H n ◃⊙idf
      =⊙∘
      ⊙×-cpₕ₀ H G n ◃⊙∘
      ⊙×-swap ◃⊙idf
  ⊙×-cp₀ₕ-comm n =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm O (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ◃⊙∘
    ⊙×-cp₀ₕ G H n ◃⊙idf
      =⊙∘⟨ 2 & 1 & ⊙expand (⊙×-cp₀ₕ-seq G H n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm O (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ◃⊙∘
    ⊙×-cp₀ₕ' G H n ◃⊙∘
    ⊙×-fmap (⊙<– (⊙emloop-equiv G.grp)) (⊙idf (⊙EM H (S n))) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙×-cp₀ₕ'-comm n ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm O (S n)) ◃⊙∘
    ⊙×-cpₕ₀' H G n ◃⊙∘
    ⊙×-swap ◃⊙∘
    ⊙×-fmap (⊙<– (⊙emloop-equiv G.grp)) (⊙idf (⊙EM H (S n))) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ap (⊙transport (⊙EM H⊗G.abgroup)) $
                    set-path ℕ-level (+-comm O (S n)) (! (+-unit-r (S n))) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-unit-r (S n))) ◃⊙∘
    ⊙×-cpₕ₀' H G n ◃⊙∘
    ⊙×-swap ◃⊙∘
    ⊙×-fmap (⊙<– (⊙emloop-equiv G.grp)) (⊙idf (⊙EM H (S n))) ◃⊙idf
      =⊙∘⟨ 2 & 2 &
           =⊙∘-in {gs = ⊙×-fmap (⊙idf (⊙EM H (S n))) (⊙<– (⊙emloop-equiv G.grp)) ◃⊙∘
                        ⊙×-swap ◃⊙idf} $ ! $ ⊙λ= $
           ⊙×-swap-natural (⊙<– (⊙emloop-equiv G.grp)) (⊙idf (⊙EM H (S n))) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-unit-r (S n))) ◃⊙∘
    ⊙×-cpₕ₀' H G n ◃⊙∘
    ⊙×-fmap (⊙idf (⊙EM H (S n))) (⊙<– (⊙emloop-equiv G.grp)) ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 0 & 3 & ⊙contract ⟩
    ⊙×-cpₕ₀ H G n ◃⊙∘
    ⊙×-swap ◃⊙idf ∎⊙∘

module _ {i} {j} (G : AbGroup i) (H : AbGroup j) where

  open EMExplicit

  private
    module G = AbGroup G
    module H = AbGroup H
    module G⊗H = TensorProduct G H
    module H⊗G = TensorProduct H G

  ⊙∧-cpₕₕ'-comm : ∀ (m n : ℕ)
    → ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
      ⊙∧-cpₕₕ' G H m n ◃⊙idf
      =⊙∘
      ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
      ⊙∧-cpₕₕ' H G n m ◃⊙∘
      ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
  ⊙∧-cpₕₕ'-comm m n =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
    ⊙∧-cpₕₕ' G H m n ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ! $ ⊙transport-⊙EM-uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative (S m + S n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S (m + S n))) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative) ◃⊙∘
    ⊙∧-cpₕₕ' G H m n ◃⊙idf
      =⊙∘⟨ 2 & 1 & ⊙expand (⊙∧-cpₕₕ'-seq G H m n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S (m + S n))) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative) ◃⊙∘
    ⊙cpₕₕ'' G⊗H.abgroup m n ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)
             (λ K → ⊙cpₕₕ'' K m n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙cpₕₕ'' H⊗G.abgroup m n ◃⊙∘
    ⊙transport (λ K → ⊙Susp^ (m + n) (⊙EM K 2)) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘₁⟨ 2 & 1 & p₁ ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙cpₕₕ'' H⊗G.abgroup m n ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙expand (⊙cpₕₕ''-seq H⊗G.abgroup m n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙cond-neg H⊗G.abgroup (S m + S n) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S m) n)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (+-comm (S m) (S n))
             (λ k → ⊙cond-neg H⊗G.abgroup k (odd n)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S m) n)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙transport-∙ (⊙EM H⊗G.abgroup) (! (+-βr (S m) n)) (+-comm (S m) (S n)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S m) n) ∙ +-comm (S m) (S n)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘₁⟨ 1 & 1 & ap (⊙transport (⊙EM H⊗G.abgroup)) $
            set-path ℕ-level (! (+-βr (S m) n) ∙ +-comm (S m) (S n))
                             (ap (λ k → S (S k)) (+-comm m n) ∙ ! (+-βr (S n) m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (ap (λ k → S (S k)) (+-comm m n) ∙ ! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 1 & 1 & ⊙transport-∙ (⊙EM H⊗G.abgroup)
             (ap (λ k → S (S k)) (+-comm m n))
             (! (+-βr (S n) m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (ap (λ k → S (S k)) (+-comm m n)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘₁⟨ 2 & 1 & ⊙transport-⊙coe (⊙EM H⊗G.abgroup) (ap (λ k → S (S k)) (+-comm m n)) ∙
                    ap ⊙coe (∘-ap (⊙EM H⊗G.abgroup) (λ k → S (S k)) (+-comm m n)) ∙
                    ! (⊙transport-⊙coe (λ k → ⊙EM H⊗G.abgroup (S (S k))) (+-comm m n)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙transport (λ k → ⊙EM H⊗G.abgroup (S (S k))) (+-comm m n) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap G⊗H.swap))) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ G H) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 4 & 2 & ⊙Susp^-fmap-seq-=⊙∘ (m + n) (⊙∧-cp₁₁-comm G H) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙transport (λ k → ⊙EM H⊗G.abgroup (S (S k))) (+-comm m n) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (m + n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 2 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘ (+-comm m n) (⊙EM2-Susp H⊗G.abgroup) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙transport (λ k → ⊙Susp^ k (⊙EM H⊗G.abgroup 2)) (+-comm m n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 3 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (+-comm m n)
             (λ k → ⊙Susp^-fmap k (⊙EM-neg H⊗G.abgroup 2)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙transport (λ k → ⊙Susp^ k (⊙EM H⊗G.abgroup 2)) (+-comm m n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 4 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (+-comm m n)
             (λ k → ⊙Susp^-fmap k (⊙∧-cp₁₁ H G)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙transport (λ k → ⊙Susp^ k (⊙EM₁ H.grp ⊙∧ ⊙EM₁ G.grp)) (+-comm m n) ◃⊙∘
    ⊙Susp^-fmap (m + n) (⊙∧-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp)) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ◃⊙idf
      =⊙∘⟨ 5 & 3 & ⊙Σ^∧Σ^-out-swap (⊙EM₁ G.grp) (⊙EM₁ H.grp) m n ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 4 & 2 & ⊙maybe-Susp^-flip-natural-=⊙∘ (⊙∧-cp₁₁ H G) (n + m) (and (odd n) (odd m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2) ◃⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘₁⟨ 3 & 1 & ! p₂ ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙transport (λ K → ⊙Susp^ (n + m) (⊙EM K 2)) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 2 & 2 & ⊙transport-natural-=⊙∘ (inv-path H⊗G.abgroup) (λ K → ⊙EM2-Susp K (n + m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S (S (n + m)))) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙transport-natural-=⊙∘
             (inv-path H⊗G.abgroup)
             (λ K → ⊙transport (⊙EM K) (! (+-βr (S n) m))) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S n + S m)) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙maybe-Susp^-flip (n + m) (and (odd n) (odd m)) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 3 & 2 & ⊙EM2-Susp-⊙maybe-Susp^-flip H⊗G.abgroup (n + m) (and (odd n) (odd m)) h₁ ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S n + S m)) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙Trunc-fmap (⊙maybe-Susp-flip (⊙Susp^ (n + m) (⊙EM₁ H⊗G.grp)) (and (odd n) (odd m))) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘₁⟨ 3 & 1 & ⊙maybe-Susp^-flip-⊙cond-neg
              H⊗G.abgroup (S n + m) (and (odd n) (odd m)) h₂ ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S n + S m)) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙cond-neg H⊗G.abgroup (S (S (n + m))) (and (odd n) (odd m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 2 & 2 & !⊙∘ $ ⊙transport-natural-=⊙∘
             (! (+-βr (S n) m))
             (λ k → ⊙cond-neg H⊗G.abgroup k (and (odd n) (odd m))) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙transport (λ K → ⊙EM K (S n + S m)) (inv-path H⊗G.abgroup) ◃⊙∘
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd n) (odd m)) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙cond-neg-∘ H⊗G.abgroup (S n + S m) true (and (odd n) (odd m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd n) ◃⊙∘
    ⊙cond-neg H⊗G.abgroup (S (n + S m)) (negate (and (odd n) (odd m))) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 0 & 2 & ⊙cond-neg-∘ H⊗G.abgroup (S n + S m) (odd n) (negate (and (odd n) (odd m))) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (xor (odd n) (negate (and (odd n) (odd m)))) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ap (⊙cond-neg H⊗G.abgroup (S n + S m)) (bp (odd n) (odd m)) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (xor (and (negate (odd m)) (negate (odd n))) (odd m)) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 0 & 1 & !⊙∘ $ ⊙cond-neg-∘ H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) (odd m) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙cond-neg H⊗G.abgroup (S n + S m) (odd m) ◃⊙∘
    ⊙transport (⊙EM H⊗G.abgroup) (! (+-βr (S n) m)) ◃⊙∘
    ⊙EM2-Susp H⊗G.abgroup (n + m) ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 3 & ⊙contract ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙cpₕₕ'' H⊗G.abgroup n m ◃⊙∘
    ⊙Susp^-fmap (n + m) (⊙∧-cp₁₁ H G) ◃⊙∘
    ⊙Σ^∧Σ^-out (⊙EM₁ H.grp) (⊙EM₁ G.grp) n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 3 & ⊙contract ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ' H G n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf ∎⊙∘
    where
      p₁ : ⊙transport (λ K → ⊙Susp^ (m + n) (⊙EM K 2)) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)
           == ⊙Susp^-fmap (m + n) (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 2)
      p₁ =
        ⊙transport (λ K → ⊙Susp^ (m + n) (⊙EM K 2)) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)
          =⟨ ⊙transport-⊙coe
               (λ K → ⊙Susp^ (m + n) (⊙EM K 2))
               (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative) ⟩
        ⊙coe (ap (λ K → ⊙Susp^ (m + n) (⊙EM K 2)) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative))
          =⟨ ap ⊙coe (ap-∘ (⊙Susp^ (m + n)) (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)) ⟩
        ⊙coe (ap (⊙Susp^ (m + n)) (ap (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)))
          =⟨ ! $ ⊙transport-⊙coe
               (⊙Susp^ (m + n))
               (ap (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)) ⟩
        ⊙transport (⊙Susp^ (m + n)) (ap (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative))
          =⟨ ⊙transport-⊙Susp^ (m + n) (ap (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)) ⟩
        ⊙Susp^-fmap (m + n) (⊙coe (ap (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative)))
          =⟨ ap (⊙Susp^-fmap (m + n)) $ ! $
             ⊙transport-⊙coe (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative) ⟩
        ⊙Susp^-fmap (m + n) (⊙transport (λ K → ⊙EM K 2) (uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative))
          =⟨ ap (⊙Susp^-fmap (m + n)) (⊙transport-⊙EM-uaᴬᴳ G⊗H.abgroup H⊗G.abgroup G⊗H.commutative 2) ⟩
        ⊙Susp^-fmap (m + n) (⊙Trunc-fmap (⊙Susp^-fmap 1 (⊙EM₁-fmap (–>ᴳ G⊗H.commutative)))) =∎
      p₂ : ⊙transport (λ K → ⊙Susp^ (n + m) (⊙EM K 2)) (inv-path H⊗G.abgroup)
           == ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2)
      p₂ =
        ⊙transport (λ K → ⊙Susp^ (n + m) (⊙EM K 2)) (inv-path H⊗G.abgroup)
          =⟨ ⊙transport-⊙coe (λ K → ⊙Susp^ (n + m) (⊙EM K 2)) (inv-path H⊗G.abgroup) ⟩
        ⊙coe (ap (λ K → ⊙Susp^ (n + m) (⊙EM K 2)) (inv-path H⊗G.abgroup))
          =⟨ ap ⊙coe (ap-∘ (⊙Susp^ (n + m)) (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup)) ⟩
        ⊙coe (ap (⊙Susp^ (n + m)) (ap (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup)))
          =⟨ ! $ ⊙transport-⊙coe (⊙Susp^ (n + m)) (ap (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup)) ⟩
        ⊙transport (⊙Susp^ (n + m)) (ap (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup))
          =⟨ ⊙transport-⊙Susp^ (n + m) (ap (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup)) ⟩
        ⊙Susp^-fmap (n + m) (⊙coe (ap (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup)))
          =⟨ ap (⊙Susp^-fmap (n + m)) $ ! $
             ⊙transport-⊙coe (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup) ⟩
        ⊙Susp^-fmap (n + m) (⊙transport (λ K → ⊙EM K 2) (inv-path H⊗G.abgroup))
          =⟨ ap (⊙Susp^-fmap (n + m)) $
             ⊙transport-⊙EM-uaᴬᴳ H⊗G.abgroup H⊗G.abgroup (inv-iso H⊗G.abgroup) 2 ⟩
        ⊙Susp^-fmap (n + m) (⊙EM-neg H⊗G.abgroup 2) =∎
      h₁ : n + m == 0 → and (odd n) (odd m) == false
      h₁ p = ap (λ k → and (odd k) (odd m)) (fst (+-0 n m p))
      h₂ : S (n + m) == 0 → and (odd n) (odd m) == inr unit
      h₂ p = ⊥-elim (ℕ-S≠O (n + m) p)
      bp : ∀ (b c : Bool) → xor b (negate (and b c)) == xor (and (negate c) (negate b)) c
      bp true  true  = idp
      bp true  false = idp
      bp false true  = idp
      bp false false = idp

  ⊙∧-cpₕₕ-comm : ∀ (m n : ℕ)
    → ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
      ⊙∧-cpₕₕ G H m n ◃⊙idf
      =⊙∘
      ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
      ⊙∧-cpₕₕ H G n m ◃⊙∘
      ⊙∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ◃⊙idf
  ⊙∧-cpₕₕ-comm m n =
    =⊙∘-in $
    –>-is-inj ⊙Ext.⊙restr-equiv _ _ $
    =⊙∘-out
      {fs = ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
            ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
            ⊙∧-cpₕₕ G H m n ◃⊙∘
            ⊙smash-truncate G H m n ◃⊙idf}
      {gs = ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
            ⊙∧-cpₕₕ H G n m ◃⊙∘
            ⊙∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ◃⊙∘
            ⊙smash-truncate G H m n ◃⊙idf} $
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
    ⊙∧-cpₕₕ G H m n ◃⊙∘
    ⊙smash-truncate G H m n ◃⊙idf
      =⊙∘₁⟨ 2 & 2 & SmashCPₕₕ.⊙ext-β G H m n (⊙∧-cpₕₕ' G H m n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
    ⊙∧-cpₕₕ' G H m n ◃⊙idf
      =⊙∘⟨ ⊙∧-cpₕₕ'-comm m n ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ' H G n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 1 & 1 & =⊙∘-in {gs = ⊙∧-cpₕₕ H G n m ◃⊙∘
                                ⊙smash-truncate H G n m ◃⊙idf} $
           ! $ SmashCPₕₕ.⊙ext-β H G n m (⊙∧-cpₕₕ' H G n m) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ H G n m ◃⊙∘
    ⊙smash-truncate H G n m ◃⊙∘
    ⊙∧-swap (⊙Susp^ m (⊙EM₁ G.grp)) (⊙Susp^ n (⊙EM₁ H.grp)) ◃⊙idf
      =⊙∘⟨ 2 & 2 & =⊙∘-in {gs = ⊙∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ◃⊙∘
                                ⊙smash-truncate G H m n ◃⊙idf} $
           ⊙∧-swap-naturality
             ([_] {n = ⟨ S m ⟩} {A = Susp^ m (EM₁ G.grp)} , idp)
             ([_] {n = ⟨ S n ⟩} {A = Susp^ n (EM₁ H.grp)} , idp) ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ H G n m ◃⊙∘
    ⊙∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ◃⊙∘
    ⊙smash-truncate G H m n ◃⊙idf ∎⊙∘
    where
    module ⊙Ext = ⊙ConnExtend
      {Z = ⊙EM H⊗G.abgroup (S n + S m)}
      {n = ⟨ S n + S m ⟩}
      (⊙smash-truncate G H m n)
      (transport (λ l → has-conn-fibers l (smash-truncate G H m n))
                 (ap ⟨_⟩ (+-comm (S m) (S n)))
                 (smash-truncate-conn G H m n))
      (EM-level H⊗G.abgroup (S n + S m))

  ⊙×-cpₕₕ-comm : ∀ (m n : ℕ)
    → ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
      ⊙×-cpₕₕ G H m n ◃⊙idf
      =⊙∘
      ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
      ⊙×-cpₕₕ H G n m ◃⊙∘
      ⊙×-swap ◃⊙idf
  ⊙×-cpₕₕ-comm m n =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + S n) ◃⊙∘
    ⊙×-cpₕₕ G H m n ◃⊙idf
      =⊙∘⟨ 2 & 1 & ⊙expand (⊙×-cpₕₕ-seq G H m n) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + S n)) ◃⊙∘
    ⊙∧-cpₕₕ G H m n ◃⊙∘
    ×-⊙to-∧ ◃⊙idf
      =⊙∘⟨ 0 & 3 & ⊙∧-cpₕₕ-comm m n ⟩
    ⊙cond-neg H⊗G.abgroup (S n + S m) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ H G n m ◃⊙∘
    ⊙∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ◃⊙∘
    ×-⊙to-∧ ◃⊙idf
      =⊙∘⟨ 2 & 2 & ×-⊙to-∧-swap (⊙EM G (S m)) (⊙EM H (S n)) ⟩
    ⊙cond-neg H⊗G.abgroup (S (n + S m)) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙∧-cpₕₕ H G n m ◃⊙∘
    ×-⊙to-∧ ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 1 & 2 & ⊙contract ⟩
    ⊙cond-neg H⊗G.abgroup (S (n + S m)) (and (odd (S m)) (odd (S n))) ◃⊙∘
    ⊙×-cpₕₕ H G n m ◃⊙∘
    ⊙×-swap ◃⊙idf ∎⊙∘

  ⊙×-cp-comm : ∀ (m n : ℕ)
    → ⊙transport (⊙EM H⊗G.abgroup) (+-comm m n) ◃⊙∘
      ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (m + n) ◃⊙∘
      ⊙×-cp G H m n ◃⊙idf
      =⊙∘
      ⊙cond-neg H⊗G.abgroup (n + m) (and (odd m) (odd n)) ◃⊙∘
      ⊙×-cp H G n m ◃⊙∘
      ⊙×-swap ◃⊙idf
  ⊙×-cp-comm 0 0 =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm 0 0) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 0 ◃⊙∘
    ⊙×-cp G H 0 0 ◃⊙idf
      =⊙∘⟨ 0 & 1 & =⊙∘-in {gs = ⊙idf-seq} $
           ap (⊙transport (⊙EM H⊗G.abgroup)) (set-path ℕ-level (+-comm 0 0) idp) ⟩
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap 0 ◃⊙∘
    ⊙×-cp G H 0 0 ◃⊙idf
      =⊙∘⟨ ⊙×-cp₀₀-comm G H ⟩
    ⊙×-cp H G 0 0 ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 0 & 0 & ⊙contract ⟩
    ⊙cond-neg H⊗G.abgroup 0 false ◃⊙∘
    ⊙×-cp H G 0 0 ◃⊙∘
    ⊙×-swap ◃⊙idf ∎⊙∘
  ⊙×-cp-comm 0 (S n) =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm O (S n)) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S n) ◃⊙∘
    ⊙×-cp₀ₕ G H n ◃⊙idf
      =⊙∘⟨ ⊙×-cp₀ₕ-comm G H n ⟩
    ⊙×-cpₕ₀ H G n ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 0 & 0 & ⊙contract ⟩
    ⊙cond-neg H⊗G.abgroup (S n + O) false ◃⊙∘
    ⊙×-cpₕ₀ H G n ◃⊙∘
    ⊙×-swap ◃⊙idf ∎⊙∘
  ⊙×-cp-comm (S m) 0 =
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) O) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S (m + O)) ◃⊙∘
    ⊙×-cpₕ₀ G H m ◃⊙idf
      =⊙∘⟨ 3 & 0 & =⊙∘-in {gs = ⊙×-swap ◃⊙∘ ⊙×-swap ◃⊙idf} idp ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) O) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + O) ◃⊙∘
    ⊙×-cpₕ₀ G H m ◃⊙∘
    ⊙×-swap ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 2 & 2 & !⊙∘ (⊙×-cp₀ₕ-comm H G m) ⟩
    ⊙transport (⊙EM H⊗G.abgroup) (+-comm (S m) O) ◃⊙∘
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m + O) ◃⊙∘
    ⊙transport (⊙EM G⊗H.abgroup) (+-comm O (S m)) ◃⊙∘
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 0 & 2 & !⊙∘ $
           ⊙transport-natural-=⊙∘
             (+-comm (S m) O)
             (⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap) ⟩
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m) ◃⊙∘
    ⊙transport (⊙EM G⊗H.abgroup) (+-comm (S m) O) ◃⊙∘
    ⊙transport (⊙EM G⊗H.abgroup) (+-comm O (S m)) ◃⊙∘
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 1 & 2 & !⊙∘ $ ⊙transport-∙
             (⊙EM G⊗H.abgroup) (+-comm 0 (S m)) (+-comm (S m) O) ⟩
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m) ◃⊙∘
    ⊙transport (⊙EM G⊗H.abgroup) (+-comm 0 (S m) ∙ +-comm (S m) O) ◃⊙∘
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 1 & 1 & =⊙∘-in {gs = ⊙idf-seq} $
           ap (⊙transport (⊙EM G⊗H.abgroup)) $
           set-path ℕ-level (+-comm 0 (S m) ∙ +-comm (S m) O) idp ⟩
    ⊙EM-fmap G⊗H.abgroup H⊗G.abgroup G⊗H.swap (S m) ◃⊙∘
    ⊙EM-fmap H⊗G.abgroup G⊗H.abgroup H⊗G.swap (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘₁⟨ 0 & 2 & ! $
            ⊙EM-fmap-∘ H⊗G.abgroup G⊗H.abgroup H⊗G.abgroup G⊗H.swap H⊗G.swap (S m) ⟩
    ⊙EM-fmap H⊗G.abgroup H⊗G.abgroup (G⊗H.swap ∘ᴳ H⊗G.swap) (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘₁⟨ 0 & 1 & ap (λ φ → ⊙EM-fmap H⊗G.abgroup H⊗G.abgroup φ (S m))
                       H⊗G.swap-swap-idhom ⟩
    ⊙EM-fmap H⊗G.abgroup H⊗G.abgroup (idhom H⊗G.grp) (S m) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘⟨ 0 & 1 & =⊙∘-in {gs = ⊙idf-seq} $ ⊙EM-fmap-idhom H⊗G.abgroup (S m) ⟩
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf
      =⊙∘₁⟨ 0 & 0 & ap (⊙cond-neg H⊗G.abgroup (S m)) (! (and-false-r (odd (S m)))) ⟩
    ⊙cond-neg H⊗G.abgroup (S m) (and (odd (S m)) (odd O)) ◃⊙∘
    ⊙×-cp₀ₕ H G m ◃⊙∘
    ⊙×-swap ◃⊙idf ∎⊙∘
  ⊙×-cp-comm (S m) (S n) = ⊙×-cpₕₕ-comm m n

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
-- Σ type (also used as existential) and
-- cartesian product (also used as conjunction).

{-# OPTIONS --safe #-}

import Tools.PropositionalEquality as PE

module Tools.Product where

infixr 4 _,_
infixr 2 _×_

-- Dependent pair type (aka dependent sum, Σ type).

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

open Σ public

-- Existential quantification.

∃ : {A : Set} → (A → Set) → Set
∃ = Σ _

∃₂ : {A : Set} {B : A → Set}
     (C : (x : A) → B x → Set) → Set
∃₂ C = ∃ λ a → ∃ λ b → C a b

-- Cartesian product.

_×_ : (A B : Set) → Set
A × B = Σ A (λ x → B)

×-eq : ∀ {A B : Set} {x x' : A} {y y' : B} → x PE.≡ x' × y PE.≡ y' → (x , y) PE.≡ ( x' , y' )
×-eq ( PE.refl , PE.refl ) = PE.refl


text:
{-# OPTIONS --without-K #-}
module 3to2 where

open import Type using (★; ★₁)
open import Function.NP using (id; const; _∘_; Π)
open import Data.Nat.NP
open import Data.Bool.NP renaming (Bool to 𝟚; true to 1b; false to 0b; toℕ to 𝟚▹ℕ)
open import Data.Product
open import Data.Maybe.NP
open import Relation.Binary.PropositionalEquality
open import Search.Type renaming (Search₀ to Explore₀; SearchInd to ExploreInd)
open import Search.Searchable
open import Search.Searchable.Product renaming (_×-search-ind_ to _×-explore-ind_)
open import Search.Searchable.Sum renaming (searchBit-ind to explore𝟚-ind)

record _→⁇_ (A B : ★) : ★ where
  constructor ⟨_∥_⟩
  field
    run    : A → B
    valid? : A → 𝟚

  to→? : A →? B
  to→? x = if valid? x then just (run x) else nothing

data 𝟛 : ★ where
  0t 1t 2t : 𝟛

explore𝟛 : Explore₀ 𝟛
explore𝟛 _∙_ f = f 0t ∙ (f 1t ∙ f 2t)

explore𝟛-ind : ∀ {ℓ} → ExploreInd ℓ explore𝟛
explore𝟛-ind _ _∙_ f = f 0t ∙ (f 1t ∙ f 2t)

module |𝟛| = Searchable₀ explore𝟛-ind
module |𝟛×𝟚| = Searchable₀ (explore𝟛-ind ×-explore-ind explore𝟚-ind)

𝟛▹𝟚 : 𝟛 → 𝟚
𝟛▹𝟚 0t = 0b
𝟛▹𝟚 1t = 1b
𝟛▹𝟚 2t = 0b

𝟛▹𝟚-valid? : 𝟛 → 𝟚
𝟛▹𝟚-valid? 0t = 1b
𝟛▹𝟚-valid? 1t = 1b
𝟛▹𝟚-valid? 2t = 0b

𝟛▹𝟚⁇ : 𝟛 →⁇ 𝟚
𝟛▹𝟚⁇ = ⟨ 𝟛▹𝟚 ∥ 𝟛▹𝟚-valid? ⟩

𝟛▹𝟚? : 𝟛 →? 𝟚
𝟛▹𝟚? 0t = just 0b
𝟛▹𝟚? 1t = just 1b
𝟛▹𝟚? 2t = nothing

-- here success? implies validity
success? : Maybe 𝟚 → 𝟚
success? (just x) = x
success? nothing  = 0b

valid? : Maybe 𝟚 → 𝟚
valid? (just _) = 1b
valid? nothing  = 0b

invalid? : Maybe 𝟚 → 𝟚
invalid? = not ∘ valid?

record Fraction : ★ where
  constructor _/_
  field
    numerator denominator : ℕ
open Fraction public

_≡Frac_ : (x y : Fraction) → ★
_≡Frac_ x y =
  numerator x * denominator y ≡ numerator y * denominator x

{- Pr[A|B] = Pr[A∧B] / Pr[B] = #(A∧B) / #B -}

module FromCount {R : ★} (#_ : (R → 𝟚) → ℕ) where

  module Using→? where

    module _ (f : R →? 𝟚) where

      Pr[success|valid] = # (success? ∘ f) / # (valid? ∘ f)

    module _ (f g : R →? 𝟚) where
      _≈_ = Pr[success|valid] f ≡Frac Pr[success|valid] g

  module Using→⁇ where

    module _ (f⁇ : R →⁇ 𝟚) where
      {- Pr[A|B] = Pr[A∧B] / Pr[B] = #(A∧B) / #B -}
      module f = _→⁇_ f⁇

      Pr[success|valid] = # f.run / # f.valid?

    module _ (f g : R →⁇ 𝟚) where
      _≈_ = Pr[success|valid] f ≡Frac Pr[success|valid] g

open FromCount |𝟛×𝟚|.count

module Test? where
    open Using→?

    ⅁₀ : 𝟛 × 𝟚 →? 𝟚
    ⅁₀ = 𝟛▹𝟚? ∘ proj₁

    ⅁₁ : 𝟛 × 𝟚 →? 𝟚
    ⅁₁ = just ∘ proj₂

    ⅁₀≈⅁₁ : ⅁₀ ≈ ⅁₁
    ⅁₀≈⅁₁ = refl

module Test⁇ where
    open Using→⁇

    ⅁₀ : 𝟛 × 𝟚 → 𝟚
    ⅁₀ = 𝟛▹𝟚 ∘ proj₁

    ⅁₀-valid? : 𝟛 × 𝟚 → 𝟚
    ⅁₀-valid? = 𝟛▹𝟚-valid? ∘ proj₁

    ⅁₁ : 𝟛 × 𝟚 → 𝟚
    ⅁₁ = proj₂

    ⅁₁-valid? : 𝟛 × 𝟚 → 𝟚
    ⅁₁-valid? _ = 1b

    ⅁₀≈⅁₁ : ⟨ ⅁₀ ∥ ⅁₀-valid? ⟩ ≈ ⟨ ⅁₁ ∥ ⅁₁-valid? ⟩
    ⅁₀≈⅁₁ = refl

-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
open import Relation.Binary.Core

module BBHeap.Insert.Properties {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Insert _≤_ tot≤ trans≤
open import BBHeap.Subtyping.Properties _≤_ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import Order.Total _≤_ tot≤

lemma-insert∼ : {b : Bound}{x : A}(b≤x : LeB b (val x))(h : BBHeap b) → (x ∷ flatten h) ∼ (flatten (insert b≤x h))
lemma-insert∼ b≤x leaf = refl∼
lemma-insert∼ {x = x} b≤x (left {x = y} {l = l} {r = r} b≤y l⋘r)
    with tot≤ x y
... | inj₁ x≤y
    with lemma-insert⋘ (lexy refl≤) l⋘r
... | inj₁ lᵢ⋘r
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) l)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) r
                     = ∼x /head /head (lemma++∼r (lemma-insert∼ (lexy refl≤) l))
... | inj₂ lᵢ⋗r
           rewrite  lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) l)
                      | lemma-subtyping≡ {val y} {val x} (lexy x≤y) r
                      = ∼x /head /head (lemma++∼r (lemma-insert∼ (lexy refl≤) l))
lemma-insert∼ {x = x} b≤x (left {x = y} {l = l} {r = r} b≤y l⋘r) | inj₂ y≤x
    with lemma-insert⋘ (lexy y≤x) l⋘r
... | inj₁ lᵢ⋘r = ∼x (/tail /head) /head (lemma++∼r (lemma-insert∼ (lexy y≤x) l))
... | inj₂ lᵢ⋗r = ∼x (/tail /head) /head (lemma++∼r (lemma-insert∼ (lexy y≤x) l))
lemma-insert∼ {x = x} b≤x (right {x = y} {l = l} {r = r} b≤y l⋙r)
    with tot≤ x y
... | inj₁ x≤y
    with lemma-insert⋙ (lexy refl≤) l⋙r
... | inj₁ l⋙rᵢ
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) r)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) l
                     = ∼x /head /head (trans∼ (∼x /head (lemma++/ {xs = flatten l}) refl∼) (lemma++∼l {xs = flatten l} (lemma-insert∼ (lexy refl≤) r)))
... | inj₂ l≃rᵢ
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) r)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) l
                     = ∼x /head /head (trans∼ (∼x /head (lemma++/ {xs = flatten l}) refl∼) (lemma++∼l {xs = flatten l} (lemma-insert∼ (lexy refl≤) r)))
lemma-insert∼ {x = x} b≤x (right {x = y} {l = l} {r = r} b≤y l⋙r) | inj₂ y≤x
    with lemma-insert⋙ (lexy y≤x) l⋙r
... | inj₁ l⋙rᵢ = ∼x (/tail /head) /head (trans∼ (∼x /head (lemma++/ {xs = flatten l}) refl∼) (lemma++∼l {xs = flatten l} (lemma-insert∼ (lexy y≤x) r)))
... | inj₂ l≃rᵢ = ∼x (/tail /head) /head (trans∼ (∼x /head (lemma++/ {xs = flatten l}) refl∼) (lemma++∼l {xs = flatten l} (lemma-insert∼ (lexy y≤x) r)))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --without-K #-}
module NTypes.Empty where

open import NTypes
open import Types

0-isSet : isSet ⊥
0-isSet x = 0-elim x

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module Lang.Instance where

import      Lvl
open import Type

private variable ℓ : Lvl.Level
private variable T X Y Z : Type{ℓ}

-- Infers/resolves/(searches for) an instance/proof of the specified type/statement
resolve : (T : Type{ℓ}) →  ⦃ _ : T ⦄ → T
resolve (_) ⦃ x ⦄ = x

-- Infers/resolves/(searches for) an instance/proof of an inferred type/statement
infer : ⦃ _ : T ⦄ → T
infer ⦃ x ⦄ = x

inst-fn : (X → Y) → (⦃ inst : X ⦄ → Y)
inst-fn P ⦃ x ⦄ = P(x)

inst-fn₂ : (X → Y → Z) → (⦃ inst₁ : X ⦄ → ⦃ inst₂ : Y ⦄ → Z)
inst-fn₂ P ⦃ x ⦄ ⦃ y ⦄ = P(x)(y)

inst-fnᵢ : ({_ : X} → Y → Z) → ({_ : X} → ⦃ _ : Y ⦄ → Z)
inst-fnᵢ P {x} ⦃ y ⦄ = P{x}(y)

impl-to-expl : ({ _ : X} → Y) → (X → Y)
impl-to-expl f(x) = f{x}

expl-to-impl : (X → Y) → ({ _ : X} → Y)
expl-to-impl f{x} = f(x)

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 --sized-types --guardedness --cubical #-}

-- Note: This module is not meant to be imported.
module All where

-- import All
import Automaton.Deterministic.Accessible
import Automaton.Deterministic.Finite
-- import Automaton.Deterministic.FormalLanguage
import Automaton.Deterministic.Oper
import Automaton.Deterministic
-- import Automaton.NonDeterministic
-- import Automaton.Pushdown
-- import Automaton.TuringMachine
import Data.Any
import Data.BinaryTree.Heap
import Data.BinaryTree.Properties
import Data.BinaryTree
import Data.Boolean.Equiv.Path
import Data.Boolean.Functions
import Data.Boolean.NaryOperators
import Data.Boolean.Numeral
import Data.Boolean.Operators
import Data.Boolean.Proofs
import Data.Boolean.Stmt.Proofs
import Data.Boolean.Stmt
import Data.Boolean
import Data.DependentWidthTree
import Data.DynamicTree
import Data.Either.Equiv.Id
import Data.Either.Equiv
import Data.Either.Multi
import Data.Either.Proofs
import Data.Either.Setoid
import Data.Either
import Data.FixedTree.Properties
import Data.FixedTree
import Data.IndexedList
import Data.Iterator
import Data.List.Categorical
import Data.List.Combinatorics.Proofs
import Data.List.Combinatorics
import Data.List.Decidable
import Data.List.Equiv.Id
import Data.List.Equiv
import Data.List.Functions.Multi
import Data.List.Functions.Positional
import Data.List.Functions
import Data.List.FunctionsProven
import Data.List.Iterable
import Data.List.Proofs.Length
import Data.List.Proofs
import Data.List.Relation.Membership.Proofs
import Data.List.Relation.Membership
import Data.List.Relation.Pairwise.Proofs
import Data.List.Relation.Pairwise
import Data.List.Relation.Permutation
import Data.List.Relation.Quantification.Proofs
import Data.List.Relation.Quantification
import Data.List.Relation.Sublist.Proofs
import Data.List.Relation.Sublist
import Data.List.Relation
import Data.List.Setoid
import Data.List.Size
import Data.List.SizeOrdering
import Data.List.Sorting.Functions
import Data.List.Sorting.HeapSort
import Data.List.Sorting.InsertionSort
import Data.List.Sorting.MergeSort
import Data.List.Sorting.Proofs
import Data.List.Sorting.QuickSort
import Data.List.Sorting.SelectionSort
import Data.List.Sorting
import Data.List
import Data.ListNonEmpty
import Data.ListSized.Functions
import Data.ListSized.Proofs
import Data.ListSized
import Data.Option.Categorical
import Data.Option.Equiv.Id
import Data.Option.Equiv.Path
import Data.Option.Equiv
import Data.Option.Functions
import Data.Option.Iterable
import Data.Option.Proofs
import Data.Option.Setoid
import Data.Option
import Data.Proofs
import Data.Tuple.Category
import Data.Tuple.Equiv.Id
import Data.Tuple.Equiv
import Data.Tuple.Equivalence
import Data.Tuple.Function
import Data.Tuple.List
import Data.Tuple.Proofs
import Data.Tuple.Raise
import Data.Tuple.RaiseTypeᵣ.Functions
import Data.Tuple.RaiseTypeᵣ
import Data.Tuple.Raiseᵣ.Functions
import Data.Tuple.Raiseᵣ.Iterable
import Data.Tuple.Raiseᵣ.Proofs
import Data.Tuple.Raiseᵣ
import Data.Tuple.Raiseₗ
import Data.Tuple
import Data
import FFI.IO
import FFI.MachineWord
import Float
-- import FormalLanguage.ContextFreeGrammar
-- import FormalLanguage.Equals
-- import FormalLanguage.Proofs
-- import FormalLanguage.RegularExpression
-- import FormalLanguage
import Formalization.ClassicalPredicateLogic.Semantics
import Formalization.ClassicalPredicateLogic.Syntax.Substitution
import Formalization.ClassicalPredicateLogic.Syntax
import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Consistency
import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Proofs
-- import Formalization.ClassicalPropositionalLogic.NaturalDeduction.Tree
import Formalization.ClassicalPropositionalLogic.NaturalDeduction
import Formalization.ClassicalPropositionalLogic.Place
import Formalization.ClassicalPropositionalLogic.Semantics.Proofs
import Formalization.ClassicalPropositionalLogic.Semantics
-- import Formalization.ClassicalPropositionalLogic.SequentCalculus
import Formalization.ClassicalPropositionalLogic.Syntax.Proofs
import Formalization.ClassicalPropositionalLogic.Syntax
import Formalization.ClassicalPropositionalLogic.TruthTable
-- import Formalization.ClassicalPropositionalLogic
-- import Formalization.FunctionalML
import Formalization.ImperativePL
import Formalization.LambdaCalculus.Semantics.CallByName
import Formalization.LambdaCalculus.Semantics.CallByValue
import Formalization.LambdaCalculus.Semantics.Reduction
import Formalization.LambdaCalculus.Semantics
import Formalization.LambdaCalculus.SyntaxTransformation
import Formalization.LambdaCalculus.Terms.Combinators
import Formalization.LambdaCalculus
import Formalization.Monoid
import Formalization.Polynomial
import Formalization.PredicateLogic.Classical.NaturalDeduction
-- import Formalization.PredicateLogic.Classical.Semantics.Homomorphism
import Formalization.PredicateLogic.Classical.Semantics.Satisfaction
import Formalization.PredicateLogic.Classical.Semantics
import Formalization.PredicateLogic.Classical.SequentCalculus
import Formalization.PredicateLogic.Constructive.NaturalDeduction
-- import Formalization.PredicateLogic.Constructive.SequentCalculus
-- import Formalization.PredicateLogic.Minimal.NaturalDeduction.NegativeTranslations
import Formalization.PredicateLogic.Minimal.NaturalDeduction.Tree
import Formalization.PredicateLogic.Minimal.NaturalDeduction
-- import Formalization.PredicateLogic.Minimal.SequentCalculus
import Formalization.PredicateLogic.Signature
import Formalization.PredicateLogic.Syntax.NegativeTranslations
import Formalization.PredicateLogic.Syntax.Substitution
import Formalization.PredicateLogic.Syntax.Tree
import Formalization.PredicateLogic.Syntax
import Formalization.PrimitiveRecursion
-- import Formalization.PureTypeSystem
import Formalization.RecursiveFunction
import Formalization.SKICombinatorCalculus
import Formalization.SimplyTypedLambdaCalculus
import Function.Axioms
import Function.DomainRaise
import Function.Domains.Functions
import Function.Domains.Id
import Function.Domains.Proofs
import Function.Domains
import Function.Equals.Multi
import Function.Equals.Proofs
import Function.Equals
import Function.Inverse
import Function.Inverseᵣ
import Function.Inverseₗ
import Function.Iteration.Order
import Function.Iteration.Proofs
import Function.Iteration
import Function.Multi.Functions
import Function.Multi
import Function.Multi₌.Functions
import Function.Multi₌
import Function.Names
import Function.PointwiseStructure
import Function.Proofs
import Function
import Functional.Combinations
import Functional.Dependent
import Functional
-- import Geometry.Axioms
-- import Geometry.HilbertAxioms
import Graph.Category
import Graph.Oper
import Graph.Properties.Proofs
import Graph.Properties
import Graph.Walk.Functions.Proofs
import Graph.Walk.Functions
import Graph.Walk.Proofs
import Graph.Walk.Properties
import Graph.Walk
import Graph
import Iterator
import Js
import Lang.Function
import Lang.Inspect
import Lang.Instance
import Lang.Irrelevance
import Lang.Reflection
import Lang.Size
import Lang.Vars.Structure.Operator
import Logic.Classical.DoubleNegated
import Logic.Classical
import Logic.DiagonalMethod
import Logic.IntroInstances
import Logic.Names
import Logic.Predicate.Equiv
import Logic.Predicate.Multi
import Logic.Predicate.Theorems
import Logic.Predicate
import Logic.Propositional.Equiv
import Logic.Propositional.Proofs.Structures
import Logic.Propositional.Theorems
import Logic.Propositional.Xor
import Logic.Propositional
import Logic.WeaklyClassical
import Logic
import Lvl.Decidable
import Lvl.Functions
import Lvl.MultiFunctions.Proofs
import Lvl.MultiFunctions
import Lvl.Proofs
import Lvl
import Main
import Numeral.CoordinateVector.Proofs
import Numeral.CoordinateVector
import Numeral.Finite.Bound
import Numeral.Finite.Category
import Numeral.Finite.Conversions
import Numeral.Finite.Equiv
import Numeral.Finite.Functions
import Numeral.Finite.LinearSearch
import Numeral.Finite.Oper.Comparisons.Proofs
import Numeral.Finite.Oper.Comparisons
import Numeral.Finite.Oper
import Numeral.Finite.Proofs
import Numeral.Finite.Relation.Order
import Numeral.Finite.Sequence
import Numeral.Finite
import Numeral.FixedPositional
import Numeral.Integer.Function
import Numeral.Integer.Oper
import Numeral.Integer.Proofs
import Numeral.Integer.Relation.Divisibility.Proofs
import Numeral.Integer.Relation.Divisibility
import Numeral.Integer.Relation.Order
-- import Numeral.Integer.Relation
import Numeral.Integer.Sign
import Numeral.Integer
-- import Numeral.Matrix.OverField
import Numeral.Matrix.Proofs
-- import Numeral.Matrix.Relations
import Numeral.Matrix
import Numeral.Natural.Combinatorics.Proofs
import Numeral.Natural.Combinatorics
import Numeral.Natural.Coprime.Proofs
import Numeral.Natural.Coprime
import Numeral.Natural.Decidable
import Numeral.Natural.Equiv.Path
import Numeral.Natural.Function.Coprimalize
import Numeral.Natural.Function.FlooredLogarithm
import Numeral.Natural.Function.GreatestCommonDivisor.Extended
import Numeral.Natural.Function.GreatestCommonDivisor.Proofs
import Numeral.Natural.Function.GreatestCommonDivisor
import Numeral.Natural.Function.Proofs
import Numeral.Natural.Function
import Numeral.Natural.Induction
import Numeral.Natural.Inductions
import Numeral.Natural.LinearSearch
-- import Numeral.Natural.LinearSearchDecidable
import Numeral.Natural.Oper.Comparisons.Proofs
import Numeral.Natural.Oper.Comparisons
import Numeral.Natural.Oper.DivMod.Proofs
import Numeral.Natural.Oper.Divisibility
import Numeral.Natural.Oper.FlooredDivision.Proofs.DivisibilityWithRemainder
import Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse
import Numeral.Natural.Oper.FlooredDivision.Proofs
import Numeral.Natural.Oper.FlooredDivision
import Numeral.Natural.Oper.Modulo.Proofs.Algorithm
import Numeral.Natural.Oper.Modulo.Proofs.DivisibilityWithRemainder
import Numeral.Natural.Oper.Modulo.Proofs.Elim
import Numeral.Natural.Oper.Modulo.Proofs
import Numeral.Natural.Oper.Modulo
-- import Numeral.Natural.Oper.Proofs.Elemantary
-- import Numeral.Natural.Oper.Proofs.Iteration
import Numeral.Natural.Oper.Proofs.Multiplication
import Numeral.Natural.Oper.Proofs.Order
import Numeral.Natural.Oper.Proofs.Rewrite
-- import Numeral.Natural.Oper.Proofs.Structure
import Numeral.Natural.Oper.Proofs
import Numeral.Natural.Oper.Summation.Proofs
import Numeral.Natural.Oper.Summation.Range.Proofs
import Numeral.Natural.Oper.Summation.Range
import Numeral.Natural.Oper.Summation
import Numeral.Natural.Oper
import Numeral.Natural.Prime.Proofs.Product
import Numeral.Natural.Prime.Proofs.Representation
import Numeral.Natural.Prime.Proofs
import Numeral.Natural.Prime
import Numeral.Natural.Proofs
import Numeral.Natural.Relation.Divisibility.Proofs.Modulo
import Numeral.Natural.Relation.Divisibility.Proofs.Product
import Numeral.Natural.Relation.Divisibility.Proofs
import Numeral.Natural.Relation.Divisibility
import Numeral.Natural.Relation.DivisibilityWithRemainder.Proofs
import Numeral.Natural.Relation.DivisibilityWithRemainder
import Numeral.Natural.Relation.ModuloCongruence
import Numeral.Natural.Relation.Order.Category
import Numeral.Natural.Relation.Order.Classical
import Numeral.Natural.Relation.Order.Decidable
import Numeral.Natural.Relation.Order.Existence.Proofs
import Numeral.Natural.Relation.Order.Existence
import Numeral.Natural.Relation.Order.Proofs
import Numeral.Natural.Relation.Order
import Numeral.Natural.Relation.Proofs
import Numeral.Natural.Relation.Properties
import Numeral.Natural.Relation
import Numeral.Natural.Sequence.Proofs
import Numeral.Natural.Sequence
import Numeral.Natural.TotalOper
import Numeral.Natural.UnclosedOper
import Numeral.Natural
import Numeral.Ordinal
import Numeral.PositiveInteger.Oper.Proofs
import Numeral.PositiveInteger.Oper
import Numeral.PositiveInteger
-- import Numeral.Rational.AlterAdd
-- import Numeral.Rational.SternBrocot
import Numeral.Sign.Oper.Proofs
import Numeral.Sign.Oper
import Numeral.Sign.Oper0
import Numeral.Sign.Proofs
import Numeral.Sign
import Operator.Equals
import ReductionSystem
import Relator.Category
import Relator.Congruence.Proofs
import Relator.Congruence
import Relator.Converse
import Relator.Equals.Category
import Relator.Equals.Proofs.Equiv
import Relator.Equals.Proofs.Equivalence
import Relator.Equals.Proofs
import Relator.Equals
import Relator.Ordering.Proofs
import Relator.Ordering
import Relator.ReflexiveTransitiveClosure
import Relator.Sets
import Sets.BoolSet
-- import Sets.ExtensionalPredicateSet.SetLike
import Sets.ExtensionalPredicateSet
import Sets.ImageSet.Oper
-- import Sets.ImageSet.SetLike
import Sets.ImageSet
import Sets.IterativeSet.Oper.Proofs
import Sets.IterativeSet.Oper
import Sets.IterativeSet.Relator.Proofs
import Sets.IterativeSet.Relator
import Sets.IterativeSet
import Sets.IterativeUSet
import Sets.PredicateSet.Listable
import Sets.PredicateSet
import Sized.Data.List
import Stream.Iterable
import Stream
import String
-- import Structure.Categorical.Multi
import Structure.Categorical.Names
import Structure.Categorical.Proofs
import Structure.Categorical.Properties
import Structure.Category.Action
import Structure.Category.Categories
import Structure.Category.Category
import Structure.Category.CoMonad
import Structure.Category.Dual
-- import Structure.Category.Equiv
import Structure.Category.Functor.Category
import Structure.Category.Functor.Contravariant
import Structure.Category.Functor.Equiv
import Structure.Category.Functor.Functors.Proofs
import Structure.Category.Functor.Functors
import Structure.Category.Functor.Proofs
import Structure.Category.Functor
import Structure.Category.Monad.Category
import Structure.Category.Monad.ExtensionSystem
import Structure.Category.Monad
import Structure.Category.Monoid
-- import Structure.Category.Monoidal
import Structure.Category.Morphism.IdTransport
import Structure.Category.Morphism.Transport
import Structure.Category.NaturalTransformation.Equiv
import Structure.Category.NaturalTransformation.NaturalTransformations
import Structure.Category.NaturalTransformation
import Structure.Category.Proofs
import Structure.Category
import Structure.Container.IndexedIterable
import Structure.Container.Iterable
-- import Structure.Container.SetLike.Proofs
-- import Structure.Container.SetLike
import Structure.Function.Domain.Proofs
import Structure.Function.Domain
import Structure.Function.Linear
-- import Structure.Function.Metric
import Structure.Function.Multi
import Structure.Function.Names
import Structure.Function.Ordering
import Structure.Function.Proofs
import Structure.Function
import Structure.Groupoid.Functor
import Structure.Groupoid.Groupoids
import Structure.Groupoid
import Structure.Logic.Constructive.BoundedPredicate
import Structure.Logic.Constructive.Predicate
import Structure.Logic.Constructive.Proofs
import Structure.Logic.Constructive.Propositional
import Structure.Logic
-- import Structure.Numeral.Integer.Proofs
import Structure.Numeral.Integer
import Structure.Numeral.Natural
import Structure.Operator.Algebra
import Structure.Operator.Field.VectorSpace
import Structure.Operator.Field
import Structure.Operator.Functions
import Structure.Operator.Group.Proofs
import Structure.Operator.Group
import Structure.Operator.IntegralDomain
-- import Structure.Operator.Iteration
import Structure.Operator.Lattice
import Structure.Operator.Monoid.Category
import Structure.Operator.Monoid.Homomorphism
import Structure.Operator.Monoid.Invertible.Proofs
import Structure.Operator.Monoid.Invertible
import Structure.Operator.Monoid.Monoids.Coset
import Structure.Operator.Monoid.Monoids.Function
import Structure.Operator.Monoid.Proofs
import Structure.Operator.Monoid.Submonoid
import Structure.Operator.Monoid
import Structure.Operator.Names
import Structure.Operator.Proofs.Util
import Structure.Operator.Proofs
import Structure.Operator.Properties
import Structure.Operator.Ring.Characteristic
import Structure.Operator.Ring.Homomorphism
import Structure.Operator.Ring.Proofs
import Structure.Operator.Ring.Rings
import Structure.Operator.Ring
import Structure.Operator.SetAlgebra
import Structure.Operator.Vector.Eigen
-- import Structure.Operator.Vector.Equiv
import Structure.Operator.Vector.FiniteDimensional.LinearMaps.ChangeOfBasis
-- import Structure.Operator.Vector.FiniteDimensional.Proofs
import Structure.Operator.Vector.FiniteDimensional
import Structure.Operator.Vector.InfiniteDimensional
-- import Structure.Operator.Vector.LinearCombination.Proofs
import Structure.Operator.Vector.LinearCombination
-- import Structure.Operator.Vector.LinearMap.Category
-- import Structure.Operator.Vector.LinearMap.Equiv
import Structure.Operator.Vector.LinearMap
import Structure.Operator.Vector.LinearMaps
import Structure.Operator.Vector.Proofs
-- import Structure.Operator.Vector.Subspace.Proofs
-- import Structure.Operator.Vector.Subspace
-- import Structure.Operator.Vector.Subspaces.DirectSum
-- import Structure.Operator.Vector.Subspaces.Image
-- import Structure.Operator.Vector.Subspaces.Kernel
-- import Structure.Operator.Vector.Subspaces.Span
import Structure.Operator.Vector
import Structure.Operator
import Structure.OrderedField.AbsoluteValue
import Structure.OrderedField
import Structure.Real.Abs
-- import Structure.Real.Continuity
-- import Structure.Real.Derivative
-- import Structure.Real.Limit
import Structure.Real
import Structure.Relator.Apartness.Proofs
import Structure.Relator.Apartness
import Structure.Relator.Equivalence.Proofs
import Structure.Relator.Equivalence
import Structure.Relator.Function.Multi
import Structure.Relator.Function.Proofs
import Structure.Relator.Function
import Structure.Relator.Names
import Structure.Relator.Ordering.Lattice
import Structure.Relator.Ordering.Proofs
import Structure.Relator.Ordering
import Structure.Relator.Proofs
import Structure.Relator.Properties.Proofs
import Structure.Relator.Properties
import Structure.Relator
import Structure.Semicategory
import Structure.Setoid.Category.HomFunctor
import Structure.Setoid.Category
import Structure.Setoid.Names
import Structure.Setoid.Proofs
import Structure.Setoid.Size.Proofs
import Structure.Setoid.Size
import Structure.Setoid.Uniqueness.Proofs
import Structure.Setoid.Uniqueness
import Structure.Setoid
import Structure.Sets.Names
import Structure.Sets.Operator
import Structure.Sets.Quantifiers.Proofs
import Structure.Sets.Quantifiers
import Structure.Sets.Relator
import Structure.Sets.Relators
import Structure.Sets.ZFC.Classical
import Structure.Sets.ZFC.Inductive
import Structure.Sets.ZFC.Oper
import Structure.Sets.ZFC
import Structure.Sets
import Structure.Signature
-- import Structure.Topology.Proofs
-- import Structure.Topology.Properties
import Structure.Topology
import Structure.Type.Identity.Proofs.Eliminator
-- import Structure.Type.Identity.Proofs.Multi
import Structure.Type.Identity.Proofs
import Structure.Type.Identity
import Structure.Type.Quotient
import Syntax.Do
import Syntax.Function
import Syntax.Idiom
import Syntax.Implication.Dependent
import Syntax.Implication
import Syntax.List
import Syntax.Number
import Syntax.Transitivity
import Syntax.Type
import TestProp
import Type.Category.ExtensionalFunctionsCategory.HomFunctor
import Type.Category.ExtensionalFunctionsCategory
-- import Type.Category.IntensionalFunctionsCategory.HomFunctor
import Type.Category.IntensionalFunctionsCategory.LvlUpFunctor
import Type.Category.IntensionalFunctionsCategory
import Type.Category
import Type.Cubical.Equiv
import Type.Cubical.HTrunc₁
import Type.Cubical.InductiveInterval
import Type.Cubical.InductivePath
import Type.Cubical.Logic
import Type.Cubical.Path.Category
import Type.Cubical.Path.Equality
import Type.Cubical.Path.Proofs
import Type.Cubical.Path
import Type.Cubical.Quotient
import Type.Cubical.SubtypeSet
import Type.Cubical.Univalence
import Type.Cubical
import Type.Dependent.Functions
import Type.Dependent
import Type.Equiv
import Type.Identity.Heterogenous
import Type.Identity.Proofs
import Type.Identity
import Type.Isomorphism
import Type.Proofs
import Type.Properties.Decidable.Proofs
import Type.Properties.Decidable
import Type.Properties.Empty.Proofs
import Type.Properties.Empty
-- import Type.Properties.Homotopy.Proofs
import Type.Properties.Homotopy
import Type.Properties.Inhabited
import Type.Properties.MereProposition
import Type.Properties.Singleton.Proofs
import Type.Properties.Singleton
import Type.Singleton.Proofs
import Type.Singleton
import Type.Size.Countable
import Type.Size.Finite
import Type.Size.Proofs
import Type.Size
import Type.WellOrdering
import Type


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- String Literals
------------------------------------------------------------------------

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

module Data.String.Literals where

open import Agda.Builtin.FromString
open import Data.Unit
open import Agda.Builtin.String

isString : IsString String
isString = record
  { Constraint = λ _ → ⊤
  ; fromString = λ s → s
  }


text:
module Logic.Predicate.Equiv where

import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable Obj : Type{ℓ}
private variable Pred : Obj → Stmt{ℓ}

module _ ⦃ _ : Equiv{ℓₑ}(Obj) ⦄ where
  _≡∃_ : ∃{Obj = Obj}(Pred) → ∃{Obj = Obj}(Pred) → Stmt
  [∃]-intro x ≡∃ [∃]-intro y = x ≡ y

  instance
    [≡∃]-reflexivity : Reflexivity(_≡∃_ {Pred = Pred})
    Reflexivity.proof [≡∃]-reflexivity = reflexivity(_≡_)

  instance
    [≡∃]-symmetry : Symmetry(_≡∃_ {Pred = Pred})
    Symmetry.proof [≡∃]-symmetry = symmetry(_≡_)

  instance
    [≡∃]-transitivity : Transitivity(_≡∃_ {Pred = Pred})
    Transitivity.proof [≡∃]-transitivity = transitivity(_≡_)

  instance
    [≡∃]-equivalence : Equivalence(_≡∃_ {Pred = Pred})
    [≡∃]-equivalence = intro

  instance
    [≡∃]-equiv : Equiv{ℓₑ}(∃{Obj = Obj} Pred)
    [≡∃]-equiv = intro(_≡∃_) ⦃ [≡∃]-equivalence ⦄