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

module sets.int.definition where

open import sum
open import equality
open import function
open import sets.nat.core
open import hott.level

private
  data Z : Set where
    mk-int : ℕ → ℕ → Z

ℤ : Set
ℤ = Z

_[-]_ : ℕ → ℕ → ℤ
_[-]_ = mk-int

postulate
  eq-ℤ : (n m d : ℕ) → n [-] m ≡ (d + n) [-] (d + m)
  hℤ : h 2 ℤ

IsAlg-ℤ : ∀ {i} → Set i → Set _
IsAlg-ℤ X = Σ (ℕ → ℕ → X) λ f
          → (∀ n m d → f n m ≡ f (d + n) (d + m))

aℤ : IsAlg-ℤ ℤ
aℤ = _[-]_ , eq-ℤ

map-Alg-ℤ : ∀ {i j}{X : Set i}{Y : Set j}
          → (X → Y) → IsAlg-ℤ X → IsAlg-ℤ Y
map-Alg-ℤ {X = X}{Y} h (f , u) = (g , v)
  where
    g : ℕ → ℕ → Y
    g n m = h (f n m)

    v : ∀ n m d → g n m ≡ g (d + n) (d + m)
    v n m d = ap h (u n m d)

map-Alg-ℤ-id : ∀ {i}{X : Set i}(aX : IsAlg-ℤ X)
             → map-Alg-ℤ (λ x → x) aX ≡ aX
map-Alg-ℤ-id aX = unapΣ (refl ,
  funext λ n → funext λ m → funext λ d → ap-id _)

map-Alg-ℤ-hom : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
     → (f : Y → Z)(g : X → Y)(aX : IsAlg-ℤ X)
     → map-Alg-ℤ (f ∘' g) aX
     ≡ map-Alg-ℤ f (map-Alg-ℤ g aX)
map-Alg-ℤ-hom f g aX = unapΣ (refl , funext λ n → funext λ m → funext λ d
  → sym (ap-hom g f _))

Hom-ℤ : ∀ {i j}{X : Set i}{Y : Set j}
      → IsAlg-ℤ X → IsAlg-ℤ Y → Set _
Hom-ℤ {X = X}{Y} aX aY = Σ (X → Y) λ h → map-Alg-ℤ h aX ≡ aY

id-ℤ : ∀ {i}{X : Set i}(aX : IsAlg-ℤ X) → Hom-ℤ aX aX
id-ℤ aX = (λ x → x) , map-Alg-ℤ-id aX

_⋆ℤ_ : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
     → {aX : IsAlg-ℤ X}{aY : IsAlg-ℤ Y}{aZ : IsAlg-ℤ Z}
     → Hom-ℤ aY aZ → Hom-ℤ aX aY → Hom-ℤ aX aZ
_⋆ℤ_ {aX = aX} (f , u) (g , v) = f ∘' g , map-Alg-ℤ-hom f g aX · ap (map-Alg-ℤ f) v · u

module _ {i}{X : Set i}(hX : h 2 X)(aX : IsAlg-ℤ X) where

  elim-ℤ : ℤ → X
  elim-ℤ (mk-int n n') = proj₁ aX n n'

  postulate elim-β-ℤ : ∀ n m d → ap elim-ℤ (eq-ℤ n m d) ≡ proj₂ aX n m d

  elim-Alg-β-ℤ : map-Alg-ℤ elim-ℤ aℤ ≡ aX
  elim-Alg-β-ℤ = unapΣ (refl , funext λ n → funext λ m → funext λ d → elim-β-ℤ n m d)

  elim-Alg-ℤ : Hom-ℤ aℤ aX
  elim-Alg-ℤ = elim-ℤ , elim-Alg-β-ℤ

  postulate univ-ℤ : (h : Hom-ℤ aℤ aX) → elim-Alg-ℤ ≡ h

  Hom-ℤ-contr : contr (Hom-ℤ aℤ aX)
  Hom-ℤ-contr = elim-Alg-ℤ , univ-ℤ

elim-prop-ℤ : ∀ {i}{X : ℤ → Set i} → (∀ n → h 1 (X n))
            → (f : ∀ n m → X (n [-] m))
            → ∀ n → X n
elim-prop-ℤ {X = X} hX f n = subst X (i-β₀ n) (proj₂ (s₀ n))
  where
    Y : Set _
    Y = Σ ℤ X

    hY : h 2 Y
    hY = Σ-level hℤ λ n → h↑ (hX n)

    aY : IsAlg-ℤ Y
    aY = (λ n m → (n [-] m , f n m))
       , (λ n m d → unapΣ (eq-ℤ n m d , h1⇒prop (hX ((d + n) [-] (d + m))) _ _))

    pY : Hom-ℤ aY aℤ
    pY = proj₁ , unapΣ (refl , h1⇒prop
      (Π-level λ n → Π-level λ m → Π-level λ p → hℤ _ _) _ _)

    s : Hom-ℤ aℤ aY
    s = elim-Alg-ℤ hY aY

    s₀ : ℤ → Y
    s₀ = proj₁ s

    i-β₀ : ∀ n → proj₁ (s₀ n) ≡ n
    i-β₀ n = ap (λ f → proj₁ f n)
      (contr⇒prop (Hom-ℤ-contr hℤ aℤ) (pY ⋆ℤ s) (id-ℤ aℤ))

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Files where

open import Prelude
open import System.File
open import System.FilePath
open import Prelude.Equality

fileIsEqual : ∀ {k} → Path k → Path k → IO Unit
fileIsEqual a b = _≟_ <$> readBinaryFile a <*> readBinaryFile b >>= λ x →
  if x then return unit else exitWith (Failure 1)
  where
    -- Move this to Prelude.Equality?
    _≟_ : ∀ {a} {A : Set a} → {{eq : Eq A}} → A → A → Bool
    x ≟ y = isYes (x == y)

main : IO ⊤
main =
  readTextFile fIn >>=
  writeTextFile fTxtOut >>
  readBinaryFile fIn >>=
  writeBinaryFile fBinOut >>
  fileIsEqual fIn fTxtOut >>
  fileIsEqual fIn fBinOut
  where
    fIn = relative "Files.agda"
    fTxtOut = relative "test_files_txt.out"
    fBinOut = relative "test_files_bin.out"

ext: agda

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

open import Cubical.ZCohomology.Base
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Data.Empty
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2 ; setTruncIsSet to §)
open import Cubical.HITs.Nullification
open import Cubical.Data.Int renaming (_+_ to _ℤ+_)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3)
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Freudenthal
open import Cubical.HITs.SmashProduct.Base
open import Cubical.Algebra.Group
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Foundations.Equiv.HalfAdjoint

open import Cubical.HITs.Pushout
open import Cubical.Data.Sum.Base
open import Cubical.Data.HomotopyGroup

open import Cubical.ZCohomology.KcompPrelims

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

{- Equivalence between cohomology of A and reduced cohomology of (A + 1) -}
coHomRed+1Equiv : (n : ℕ) →
                  (A : Type ℓ) →
                  (coHom n A) ≡ (coHomRed n ((A ⊎ Unit , inr (tt))))
coHomRed+1Equiv zero A i = ∥ helpLemma {C = (Int , pos 0)} i ∥₂
  module coHomRed+1 where
  helpLemma : {C : Pointed ℓ} → ( (A → (typ C)) ≡  ((((A ⊎ Unit) , inr (tt)) →∙ C)))
  helpLemma {C = C} = isoToPath (iso map1
                                     map2
                                     (λ b → linvPf b)
                                     (λ _  → refl))
    where
    map1 : (A → typ C) → ((((A ⊎ Unit) , inr (tt)) →∙ C))
    map1 f = map1' , refl
      module helpmap where
      map1' : A ⊎ Unit → fst C
      map1' (inl x) = f x
      map1' (inr x) = pt C

    map2 : ((((A ⊎ Unit) , inr (tt)) →∙ C)) → (A → typ C)
    map2 (g , pf) x = g (inl x)

    linvPf : (b :((((A ⊎ Unit) , inr (tt)) →∙ C))) →  map1 (map2 b) ≡ b
    linvPf (f , snd) i = (λ x → helper x i)  , λ j → snd ((~ i) ∨ j)
      where
      helper : (x : A ⊎ Unit) → ((helpmap.map1') (map2 (f , snd)) x) ≡ f x
      helper (inl x) = refl
      helper (inr tt) = sym snd

coHomRed+1Equiv (suc n) A i = ∥ coHomRed+1.helpLemma A i {C = ((coHomK (suc n)) , ∣ north ∣)} i ∥₂

-----------

Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
Kn→ΩKn+1 n = Iso.fun (Iso3-Kn-ΩKn+1 n)

ΩKn+1→Kn : {n : ℕ} → typ (Ω (coHomK-ptd (suc n))) → coHomK n
ΩKn+1→Kn {n = n} = Iso.inv (Iso3-Kn-ΩKn+1 n)

Kn≃ΩKn+1 : {n : ℕ} → coHomK n ≃ typ (Ω (coHomK-ptd (suc n)))
Kn≃ΩKn+1 {n = n} = isoToEquiv (Iso-Kn-ΩKn+1 n)

---------- Algebra/Group stuff --------

0ₖ : {n : ℕ} → coHomK n
0ₖ {n = zero} = pt (coHomK-ptd 0)
0ₖ {n = suc n} = pt (coHomK-ptd (suc n))

infixr 35 _+ₖ_

_+ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_+ₖ_ {n = n} x y  = ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)

-ₖ_ : {n : ℕ} → coHomK n → coHomK n
-ₖ_ {n = n} x = ΩKn+1→Kn (sym (Kn→ΩKn+1 n x))

Kn→ΩKn+10ₖ : (n : ℕ) → Kn→ΩKn+1 n 0ₖ ≡ refl
Kn→ΩKn+10ₖ zero = refl
Kn→ΩKn+10ₖ (suc n) = (λ i → cong ∣_∣ (rCancel (merid north) i)) -- could also use refl for n = 1, but for computational reasons I don't want to expand the definition if not necessary.

-0ₖ : {n : ℕ} → -ₖ 0ₖ {n = n} ≡ 0ₖ
-0ₖ {n = n} = (λ i → ΩKn+1→Kn (sym (Kn→ΩKn+10ₖ n i)))
            ∙∙ (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ n (~ i)))
            ∙∙ Iso.leftInv (Iso3-Kn-ΩKn+1 n) 0ₖ

+ₖ→∙ : (n : ℕ) (a b : coHomK n) → Kn→ΩKn+1 n (a +ₖ b) ≡ Kn→ΩKn+1 n a ∙ Kn→ΩKn+1 n b
+ₖ→∙ n a b = Iso.rightInv (Iso3-Kn-ΩKn+1 n) (Kn→ΩKn+1 n a ∙ Kn→ΩKn+1 n b)

lUnitₖ : {n : ℕ} (x : coHomK n) → 0ₖ +ₖ x ≡ x
lUnitₖ {n = zero} x = cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 zero x))) ∙
                      Iso.leftInv (Iso3-Kn-ΩKn+1 zero) x
lUnitₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) i ∙ Kn→ΩKn+1 (suc n) x)) ∙
                       (cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 (suc n) x)))) ∙
                       Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) x

rUnitₖ : {n : ℕ} (x : coHomK n) → x +ₖ 0ₖ ≡ x
rUnitₖ {n = zero} x = cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 zero x))) ∙
                      Iso.leftInv (Iso3-Kn-ΩKn+1 zero) x
rUnitₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) x ∙ Kn→ΩKn+10ₖ (suc n) i)) ∙
                       (cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 (suc n) x)))) ∙
                       Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) x
--

rCancelₖ  : {n : ℕ} (x : coHomK n) → x +ₖ (-ₖ x) ≡ 0ₖ
rCancelₖ {n = zero} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 zero x ∙ Iso.rightInv (Iso3-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i)) ∙
                        cong ΩKn+1→Kn (rCancel (Kn→ΩKn+1 zero x))
rCancelₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (1 + n) x ∙ Iso.rightInv (Iso3-Kn-ΩKn+1 (1 + n)) (sym (Kn→ΩKn+1 (1 + n) x)) i)) ∙
                               cong ΩKn+1→Kn (rCancel (Kn→ΩKn+1 (1 + n) x)) ∙
                               (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) (~ i))) ∙
                               Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) 0ₖ

lCancelₖ : {n : ℕ} (x : coHomK n) → (-ₖ x) +ₖ x  ≡ 0ₖ
lCancelₖ {n = zero} x = (λ i → ΩKn+1→Kn (Iso.rightInv (Iso3-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i ∙ Kn→ΩKn+1 zero x)) ∙
                        cong ΩKn+1→Kn (lCancel (Kn→ΩKn+1 zero x))
lCancelₖ {n = suc n} x = (λ i → ΩKn+1→Kn (Iso.rightInv (Iso3-Kn-ΩKn+1 (1 + n)) (sym (Kn→ΩKn+1 (1 + n) x)) i ∙ Kn→ΩKn+1 (1 + n) x)) ∙
                               cong ΩKn+1→Kn (lCancel (Kn→ΩKn+1 (1 + n) x)) ∙
                               (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) (~ i))) ∙
                               Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) 0ₖ

assocₖ : {n : ℕ} (x y z : coHomK n) → ((x +ₖ y) +ₖ z) ≡ (x +ₖ (y +ₖ z))
assocₖ {n = n} x y z = ((λ i → ΩKn+1→Kn (Kn→ΩKn+1 n (ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)) ∙ Kn→ΩKn+1 n z)) ∙∙
                          (λ i → ΩKn+1→Kn (Iso.rightInv (Iso3-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i ∙ Kn→ΩKn+1 n z)) ∙∙
                          (λ i → ΩKn+1→Kn (assoc (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) (Kn→ΩKn+1 n z) (~ i)))) ∙
                          (λ i → ΩKn+1→Kn ((Kn→ΩKn+1 n x) ∙ Iso.rightInv (Iso3-Kn-ΩKn+1 n) ((Kn→ΩKn+1 n y ∙ Kn→ΩKn+1 n z)) (~ i)))

commₖ : {n : ℕ} (x y : coHomK n) → (x +ₖ y) ≡ (y +ₖ x)
commₖ {n = n} x y i = ΩKn+1→Kn (EH-instance (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) i)
  where
  EH-instance : (p q : typ (Ω ((∥ S₊ (suc n) ∥ (2 + (suc n))) , ∣ north ∣))) → p ∙ q ≡ q ∙ p
  EH-instance = transport (λ i → (p q : K-Id n (~ i)) → p ∙ q ≡ q ∙ p)
                          λ p q → Eckmann-Hilton 0 p q
    where
    K-Id : (n : HLevel) → typ (Ω (hLevelTrunc (3 + n) (S₊ (1 + n)) , ∣ north ∣)) ≡ typ ((Ω^ 2) (hLevelTrunc (4 + n) (S₊ (2 + n)) , ∣  north ∣ ))
    K-Id n = (λ i → typ (Ω (isoToPath (Iso2-Kn-ΩKn+1 (suc n)) i , hcomp (λ k → λ { (i = i0) → ∣ north ∣
                                                                                ;  (i = i1) → transportRefl (λ j → ∣ rCancel (merid north) k j ∣) k})
                                                                         (transp (λ j → isoToPath (Iso2-Kn-ΩKn+1 (suc n)) (i ∧ j)) (~ i)  ∣ north ∣))))

rUnitₖ' : {n : ℕ} (x : coHomK n) → x +ₖ 0ₖ ≡ x
rUnitₖ' {n = n} x = commₖ x 0ₖ ∙ lUnitₖ x

-distrₖ : {n : ℕ} → (x y : coHomK n) → -ₖ (x +ₖ y) ≡ (-ₖ x) +ₖ (-ₖ y)
-distrₖ {n = n} x y = ((λ i → ΩKn+1→Kn (sym (Kn→ΩKn+1 n (ΩKn+1→Kn (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y))))) ∙∙
                      (λ i → ΩKn+1→Kn (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i))) ∙∙
                      (λ i → ΩKn+1→Kn (symDistr (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) i))) ∙∙
                      (λ i → ΩKn+1→Kn (Iso.rightInv (Iso3-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n y)) (~ i) ∙ (Iso.rightInv (Iso3-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n x)) (~ i)))) ∙∙
                      commₖ (-ₖ y) (-ₖ x)

---- Group structure of cohomology groups ---

_+ₕ_ : {n : ℕ} → coHom n A → coHom n A → coHom n A
_+ₕ_ = sElim2 (λ _ _ → §) λ a b → ∣ (λ x → a x +ₖ b x) ∣₂

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

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

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

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

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

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

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

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

-- Proof that rUnitₖ and lUnitₖ agree on 0ₖ. Needed for Mayer-Vietoris.
rUnitlUnit0 : {n : ℕ} → rUnitₖ {n = n} 0ₖ ≡ lUnitₖ 0ₖ
rUnitlUnit0 {n = zero} = refl
rUnitlUnit0 {n = suc n} =
  (assoc (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) 0ₖ ∙ Kn→ΩKn+10ₖ (suc n) i))
         (cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 (suc n) 0ₖ))))
         (Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) 0ₖ))
 ∙∙ (λ j → helper j
         ∙ Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) 0ₖ)
 ∙∙ sym (assoc (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) i ∙ Kn→ΩKn+1 (suc n) 0ₖ))
               (cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 (suc n) 0ₖ))))
               (Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) 0ₖ))

  where
  helper : (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) 0ₖ ∙ Kn→ΩKn+10ₖ (suc n) i))
          ∙ (cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 (suc n) 0ₖ))))
          ≡ (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) i ∙ Kn→ΩKn+1 (suc n) 0ₖ))
          ∙ (cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 (suc n) 0ₖ))))
  helper = ((λ j → lUnit (rUnit ((λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) 0ₖ ∙ Kn→ΩKn+10ₖ (suc n) i))) j) j
                   ∙ rUnit (cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+1 (suc n) 0ₖ)))) j)
         ∙∙ (λ j → ((λ z → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) ∣ north ∣ ∙ (λ i → ∣ rCancel (merid north) (z ∧ j) i ∣)))
                 ∙ (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) 0ₖ ∙ Kn→ΩKn+10ₖ (suc n) (i ∨ j)))
                 ∙ λ z → ΩKn+1→Kn (((λ i → ∣ rCancel (merid north) (z ∧ j) i ∣)) ∙ refl))
                 ∙ cong ΩKn+1→Kn (sym (rUnit (Kn→ΩKn+10ₖ (suc n) j)))
                 ∙ λ z → ΩKn+1→Kn (λ i → ∣ rCancel (merid north) ((~ z) ∧ j) i ∣))
         ∙∙ (λ j → (((λ z → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) ∣ north ∣ ∙ (λ i → ∣ rCancel (merid north) z i ∣))))
                  ∙ (λ i → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) 0ₖ ∙ refl))
                  ∙ λ z → ΩKn+1→Kn ((λ i → ∣ rCancel (merid north) z i ∣) ∙ λ i → ∣ rCancel (merid north) ((~ z) ∨ (~ j)) i ∣))
                 ∙ cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+10ₖ (suc n) (~ j))))
                 ∙ λ z → ΩKn+1→Kn (λ i → ∣ rCancel (merid north) (~ z ∧ (~ j)) i ∣)))
         ∙∙ (λ j → ((λ z → ΩKn+1→Kn (Kn→ΩKn+1 (suc n) ∣ north ∣  ∙ λ i → ∣ rCancel (merid north) (z ∧ (~ j)) i ∣))
                  ∙ (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) (i ∧ j) ∙ Kn→ΩKn+10ₖ (suc n) (~ j)))
                  ∙ λ z → ΩKn+1→Kn ((λ i → ∣ rCancel (merid north) (z ∨ j) i ∣) ∙ λ i → ∣ rCancel (merid north) (~ z ∧ ~ j) i ∣))
                 ∙ rUnit (cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 (suc n) 0ₖ)))) (~ j))
         ∙∙ (λ j → lUnit (rUnit (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) i ∙ Kn→ΩKn+1 (suc n) 0ₖ)) (~ j)) (~ j)
                 ∙ cong ΩKn+1→Kn (sym (lUnit (Kn→ΩKn+1 (suc n) 0ₖ))))

---- Group structure of reduced cohomology groups (in progress - might need K to compute properly first) ---

+ₕ∙ : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A → coHomRed n A
+ₕ∙ zero = sElim2 (λ _ _ → §) λ { (a , pa) (b , pb) → ∣ (λ x → a x +ₖ b x) , (λ i → (pa i +ₖ pb i)) ∣₂ }
+ₕ∙ (suc n) = sElim2 (λ _ _ → §) λ { (a , pa) (b , pb) → ∣ (λ x → a x +ₖ b x) , (λ i → pa i +ₖ pb i) ∙ lUnitₖ 0ₖ ∣₂ }

-ₕ∙  : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A
-ₕ∙ zero = sRec § λ {(a , pt) → ∣ (λ x → -ₖ a x ) , (λ i → -ₖ (pt i)) ∣₂}
-ₕ∙ (suc n) = sRec § λ {(a , pt) → ∣ (λ x → -ₖ a x ) , (λ i → -ₖ (pt i)) ∙
                                                              (λ i → ΩKn+1→Kn (sym (Kn→ΩKn+10ₖ (suc n) i))) ∙
                                                              (λ i → ΩKn+1→Kn (Kn→ΩKn+10ₖ (suc n) (~ i))) ∙
                                                              Iso.leftInv (Iso3-Kn-ΩKn+1 (suc n)) ∣ north ∣ ∣₂}

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

open IsSemigroup
open IsMonoid
open Group
coHomGr : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → Group
Carrier (coHomGr n A) = coHom n A
0g (coHomGr n A) = 0ₕ
Group._+_ (coHomGr n A) = _+ₕ_
Group.- coHomGr n A = -ₕ
is-set (isSemigroup (IsGroup.isMonoid (Group.isGroup (coHomGr n A)))) = §
IsSemigroup.assoc (isSemigroup (IsGroup.isMonoid (Group.isGroup (coHomGr n A)))) x y z = sym (assocₕ x y z)
identity (IsGroup.isMonoid (Group.isGroup (coHomGr n A))) x = (rUnitₕ x) , (lUnitₕ x)
IsGroup.inverse (Group.isGroup (coHomGr n A)) x = (rCancelₕ x) , (lCancelₕ x)

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

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

--- ΩKₙ is commutative
isCommΩK : (n : ℕ) → (p q : typ (Ω (coHomK n , coHom-pt n))) → p ∙ q ≡ q ∙ p
isCommΩK zero p q = isSetInt _ _ (p ∙ q) (q ∙ p)
isCommΩK (suc n) p q =
  cong₂ _∙_ (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) p))
             (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) q))
  ∙∙ (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) (Kn→ΩKn+1 n (ΩKn+1→Kn p) ∙ Kn→ΩKn+1 n (ΩKn+1→Kn q)))
  ∙∙ cong (Kn→ΩKn+1 n) (commₖ (ΩKn+1→Kn p) (ΩKn+1→Kn q))
  ∙∙ Iso.rightInv (Iso3-Kn-ΩKn+1 n) (Kn→ΩKn+1 n (ΩKn+1→Kn q) ∙ Kn→ΩKn+1 n (ΩKn+1→Kn p)))
  ∙∙ sym (cong₂ _∙_ (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) q))
                   (sym (Iso.rightInv (Iso3-Kn-ΩKn+1 n) p)))

--- the loopspace of Kₙ is commutative regardless of base
isCommΩK-based : (n : ℕ) (x : coHomK n) (p q : x ≡ x) → p ∙ q ≡ q ∙ p
isCommΩK-based zero x p q = isSetInt _ _ (p ∙ q) (q ∙ p)
isCommΩK-based (suc n) x p q =
      sym (transport⁻Transport (typId x) (p ∙ q))
  ∙∙ (cong (transport (λ i → typId x (~ i))) (transpTypId p q)
  ∙∙  (λ i → transport (λ i → typId x (~ i)) (isCommΩK (suc n) (transport (λ i → typId x i) p) (transport (λ i → typId x i) q) i))
  ∙∙  cong (transport (λ i → typId x (~ i))) (sym (transpTypId q p)))
  ∙∙  transport⁻Transport (typId x) (q ∙ p)
  where
  congIsoHelper : (x : coHomK (suc n)) → Iso (coHomK (suc n)) (coHomK (suc n))
  Iso.fun (congIsoHelper x) = _+ₖ x
  Iso.inv (congIsoHelper x) = _+ₖ (-ₖ x)
  Iso.rightInv (congIsoHelper x) a = assocₖ a (-ₖ x) x ∙∙ cong (a +ₖ_) (lCancelₖ x) ∙∙ rUnitₖ a
  Iso.leftInv (congIsoHelper x) a = assocₖ a x (-ₖ x) ∙∙ cong (a +ₖ_) (rCancelₖ x) ∙∙ rUnitₖ a

  typId : (x : coHomK (suc n)) → (x ≡ x) ≡ Path (coHomK (suc n)) 0ₖ 0ₖ
  typId x = isoToPath (congIso (invIso (congIsoHelper x))) ∙ λ i → rCancelₖ x i ≡ rCancelₖ x i

  transpTypId : (p q : (x ≡ x)) → transport (λ i → typId x i) (p ∙ q) ≡ transport (λ i → typId x i) p ∙ transport (λ i → typId x i) q
  transpTypId p q =
      ((substComposite (λ x → x) (isoToPath ((congIso (invIso (congIsoHelper x)))))
                                 (λ i → rCancelₖ x i ≡ rCancelₖ x i) (p ∙ q))
    ∙∙ (λ i → transport (λ i → rCancelₖ x i ≡ rCancelₖ x i) (transportRefl (congFunct (_+ₖ (-ₖ x)) p q i) i))
    ∙∙ overPathFunct (cong (_+ₖ (-ₖ x)) p) (cong (_+ₖ (-ₖ x)) q) (rCancelₖ x))
    ∙∙ cong₂ (λ y z → transport (λ i → rCancelₖ x i ≡ rCancelₖ x i) y ∙ transport (λ i → rCancelₖ x i ≡ rCancelₖ x i) z)
             (sym (transportRefl (cong (_+ₖ (-ₖ x)) p)))
             (sym (transportRefl (cong (_+ₖ (-ₖ x)) q)))
    ∙∙ cong₂ (_∙_) (sym (substComposite (λ x → x) (isoToPath ((congIso (invIso (congIsoHelper x))))) (λ i → rCancelₖ x i ≡ rCancelₖ x i) p))
                   (sym (substComposite (λ x → x) (isoToPath ((congIso (invIso (congIsoHelper x))))) (λ i → rCancelₖ x i ≡ rCancelₖ x i) q))

addLemma : (a b : Int) → a +ₖ b ≡ (a ℤ+ b)
addLemma a b = (cong ΩKn+1→Kn (sym (congFunct ∣_∣ (looper a) (looper b)))
              ∙∙ cong₂ (λ x y → ΩKn+1→Kn (cong ∣_∣ (x ∙ y))) (looper≡looper2 a) (looper≡looper2 b)
              ∙∙ (λ i → ΩKn+1→Kn (cong ∣_∣ (cong SuspBool→S1 (cong S¹→SuspBool (intLoop a)) ∙ cong SuspBool→S1 (cong S¹→SuspBool (intLoop b))))))
              ∙∙ (cong (λ x → ΩKn+1→Kn (cong ∣_∣ x)) (sym (congFunct SuspBool→S1 (cong S¹→SuspBool (intLoop a)) (cong S¹→SuspBool (intLoop b))))
              ∙∙ cong (λ x → ΩKn+1→Kn (cong ∣_∣ (cong SuspBool→S1 x))) (sym (congFunct S¹→SuspBool (intLoop a) (intLoop b)))
              ∙∙ cong (λ x → ΩKn+1→Kn (cong ∣_∣ (cong SuspBool→S1 (cong S¹→SuspBool x)))) (intLoop-hom a b))
              ∙∙ (cong (λ x → ΩKn+1→Kn (cong ∣_∣ x)) (sym (looper≡looper2 (a ℤ+ b)))
                ∙ Iso.leftInv (Iso3-Kn-ΩKn+1 zero) (a ℤ+ b))

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
{-# OPTIONS --warning=error #-}

-- Useless private

module Issue476a where

A : Set₁
private
  A = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Relation.Binary.Core

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

open import BBHeap _≤_
open import BBHeap.Equality _≤_
open import BBHeap.Equality.Properties _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Bound.Lower.Order.Properties _≤_ trans≤
open import Data.Sum renaming (_⊎_ to _∨_)
open import Order.Total _≤_ tot≤

mutual
  push⋘ : {b : Bound}{x y : A}{l r : BBHeap (val y)} → LeB b (val x) → LeB b (val y) → l ⋘ r → BBHeap b
  push⋘ b≤x _ lf⋘ = left b≤x lf⋘
  push⋘ {x = x} b≤x b≤y (ll⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =  left b≤x (ll⋘ (lexy x≤y₁) (lexy (trans≤ x≤y₁ y₁≤y₂)) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋘r' = ll⋘ (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        pl'⋘r' = lemma≈⋘ pl'≈l' l'⋘r'
                   in left (transLeB b≤y y≤y₁) pl'⋘r'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = left b≤x (ll⋘ (lexy (trans≤ x≤y₂ y₂≤y₁)) (lexy x≤y₂) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋘r' = ll⋘ (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        l'⋘pr' = lemma⋘≈ l'⋘r' r'≈pr'
                   in left (transLeB b≤y y≤y₂) l'⋘pr'
  push⋘ {x = x} b≤x b≤y (lr⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =  left b≤x (lr⋘ (lexy x≤y₁) (lexy (trans≤ x≤y₁ y₁≤y₂)) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'≈l' = lemma-push⋙ (lexy y₁≤x) (lexy refl≤) l₁⋙r₁ ;
                        l'⋘r' = lr⋘ (lexy refl≤) (lexy y₁≤y₂) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        pl'⋘r' = lemma≈⋘ pl'≈l' l'⋘r'
                   in left (transLeB b≤y y≤y₁) pl'⋘r'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = left b≤x (lr⋘ (lexy (trans≤ x≤y₂ y₂≤y₁)) (lexy x≤y₂) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋘r' = lr⋘ (lexy y₂≤y₁) (lexy refl≤) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        l'⋘pr'  = lemma⋘≈ l'⋘r' r'≈pr'
                   in left (transLeB b≤y y≤y₂) l'⋘pr'

  push⋙ : {b : Bound}{x y : A}{l r : BBHeap (val y)} → LeB b (val x) → LeB b (val y) → l ⋙ r → BBHeap b
  push⋙ {x = x} b≤x b≤y (⋙lf {x = z} y≤z)
      with tot≤ x z
  ... | inj₁ x≤z = right b≤x (⋙lf (lexy x≤z))
  ... | inj₂ z≤x = right (transLeB b≤y y≤z) (⋙lf (lexy z≤x))
  push⋙ {x = x} b≤x b≤y (⋙rl {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = right b≤x (⋙rl (lexy x≤y₁) (lexy (trans≤ x≤y₁ y₁≤y₂)) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋙r' = ⋙rl (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        pl'⋙r' = lemma≈⋙ pl'≈l' l'⋙r'
                   in right (transLeB b≤y y≤y₁) pl'⋙r'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = right b≤x (⋙rl (lexy (trans≤ x≤y₂ y₂≤y₁)) (lexy x≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋙r' = ⋙rl (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        l'⋙pr' = lemma⋙≈ l'⋙r' r'≈pr'
                   in right (transLeB b≤y y≤y₂) l'⋙pr'
  push⋙ {x = x} b≤x b≤y (⋙rr {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ = right b≤x (⋙rr (lexy x≤y₁) (lexy (trans≤ x≤y₁ y₁≤y₂)) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋙r' = ⋙rr (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        pl'⋙r' = lemma≈⋙ pl'≈l' l'⋙r'
                   in right (transLeB b≤y y≤y₁) pl'⋙r'
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ = right b≤x (⋙rr (lexy (trans≤ x≤y₂ y₂≤y₁)) (lexy x≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let pr'≈r' = lemma-push⋙ (lexy y₂≤x) (lexy refl≤) l₂⋙r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋙r' = ⋙rr (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        l'⋙pr' = lemma⋙≈ l'⋙r' r'≈pr'
                   in right (transLeB b≤y y≤y₂) l'⋙pr'

  lemma-push⋘ : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋘r : l ⋘ r) → push⋘ b≤x b≤y l⋘r ≈ left b≤y l⋘r
  lemma-push⋘ b≤x b≤y lf⋘ = ≈left b≤x b≤y lf⋘ lf⋘ ≈leaf ≈leaf
  lemma-push⋘ {x = x} b≤x b≤y (ll⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =
                   let l⋘r = ll⋘ y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        x≤y₂ = lexy (trans≤ x≤y₁ y₁≤y₂) ;
                        l'⋘r' = ll⋘ (lexy x≤y₁) x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        l'≈l = ≈left (lexy x≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈left x≤y₂ y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈left b≤x b≤y l'⋘r' l⋘r l'≈l r'≈r
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let l⋘r = ll⋘ y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋘r' = ll⋘ (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        pl'⋘r' = lemma≈⋘ pl'≈l' l'⋘r' ;
                        l'≈l = ≈left (lexy refl≤) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        pl'≈l = trans≈ pl'≈l' l'≈l ;
                        r'≈r = ≈left (lexy y₁≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈left (transLeB b≤y y≤y₁) b≤y pl'⋘r' l⋘r pl'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ =
                   let l⋘r = ll⋘ y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        x≤y₁ = lexy (trans≤ x≤y₂ y₂≤y₁) ;
                        l'⋘r' = ll⋘ x≤y₁ (lexy x≤y₂) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        r'≈r = ≈left (lexy x≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                        l'≈l = ≈left x≤y₁ y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈
                   in ≈left b≤x b≤y l'⋘r' l⋘r l'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let l⋘r = ll⋘ y≤y₁ y≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋘r' = ll⋘ (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ ;
                        l'⋘pr' = lemma⋘≈ l'⋘r' r'≈pr' ;
                        r'≈r = ≈left (lexy refl≤) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                        pr'≈r = trans≈ pr'≈r' r'≈r ;
                        l'≈l = ≈left (lexy y₂≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈
                   in ≈left (transLeB b≤y y≤y₂) b≤y l'⋘pr' l⋘r l'≈l pr'≈r
  lemma-push⋘ {x = x} b≤x b≤y (lr⋘ {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =
                   let l⋘r = lr⋘ y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        x≤y₂ = lexy (trans≤ x≤y₁ y₁≤y₂) ;
                        l'⋘r' = lr⋘ (lexy x≤y₁) x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        l'≈l = ≈right (lexy x≤y₁) y≤y₁ l₁⋙r₁ l₁⋙r₁ refl≈ refl≈ ;
                        r'≈r = ≈left x≤y₂ y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈left b≤x b≤y l'⋘r' l⋘r l'≈l r'≈r
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let l⋘r = lr⋘ y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        pl'≈l' = lemma-push⋙ (lexy y₁≤x) (lexy refl≤) l₁⋙r₁ ;
                        l'⋘r' = lr⋘ (lexy refl≤) (lexy y₁≤y₂) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        pl'⋘r' = lemma≈⋘ pl'≈l' l'⋘r' ;
                        l'≈l = ≈right (lexy refl≤) y≤y₁ l₁⋙r₁ l₁⋙r₁ refl≈ refl≈ ;
                        pl'≈l = trans≈ pl'≈l' l'≈l ;
                        r'≈r = ≈left (lexy y₁≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈left (transLeB b≤y y≤y₁) b≤y pl'⋘r' l⋘r pl'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ =
                   let l⋘r = lr⋘ y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        x≤y₁ = lexy (trans≤ x≤y₂ y₂≤y₁) ;
                        l'⋘r' = lr⋘ x≤y₁ (lexy x≤y₂) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        l'≈l = ≈right x≤y₁ y≤y₁ l₁⋙r₁ l₁⋙r₁ refl≈ refl≈ ;
                        r'≈r = ≈left (lexy x≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈left b≤x b≤y l'⋘r' l⋘r l'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let l⋘r = lr⋘ y≤y₁ y≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋘r' = lr⋘ (lexy y₂≤y₁) (lexy refl≤) l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ ;
                        l'⋘pr'  = lemma⋘≈ l'⋘r' r'≈pr' ;
                        l'≈l = ≈right (lexy y₂≤y₁) y≤y₁ l₁⋙r₁ l₁⋙r₁ refl≈ refl≈ ;
                        r'≈r = ≈left (lexy refl≤) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                        pr'≈r = trans≈ pr'≈r' r'≈r
                   in ≈left (transLeB b≤y y≤y₂) b≤y l'⋘pr' l⋘r l'≈l pr'≈r

  lemma-push⋙ : {b : Bound}{x y : A}{l r : BBHeap (val y)}(b≤x : LeB b (val x))(b≤y : LeB b (val y))(l⋙r : l ⋙ r) → push⋙ b≤x b≤y l⋙r ≈ right b≤y l⋙r
  lemma-push⋙ {x = x} b≤x b≤y (⋙lf {x = z} y≤z)
      with tot≤ x z
  ... | inj₁ x≤z = ≈right b≤x b≤y (⋙lf (lexy x≤z)) (⋙lf y≤z) (≈left (lexy x≤z) y≤z lf⋘ lf⋘ ≈leaf ≈leaf) ≈leaf
  ... | inj₂ z≤x = ≈right (transLeB b≤y y≤z) b≤y (⋙lf (lexy z≤x)) (⋙lf y≤z) (≈left (lexy z≤x) y≤z lf⋘ lf⋘ ≈leaf ≈leaf) ≈leaf
  lemma-push⋙ {x = x} b≤x b≤y (⋙rl {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =
                   let l⋙r = ⋙rl y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        x≤y₂ = lexy (trans≤ x≤y₁ y₁≤y₂) ;
                        l'⋙r' = ⋙rl (lexy x≤y₁) x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        l'≈l = ≈left (lexy x≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈left x≤y₂ y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈right b≤x b≤y l'⋙r' l⋙r l'≈l r'≈r
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let l⋙r = ⋙rl y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋙r' = ⋙rl (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        pl'⋙r' = lemma≈⋙ pl'≈l' l'⋙r' ;
                        l'≈l = ≈left (lexy refl≤) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        pl'≈l = trans≈ pl'≈l' l'≈l ;
                        r'≈r = ≈left (lexy y₁≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈right (transLeB b≤y y≤y₁) b≤y pl'⋙r' l⋙r pl'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ =
                   let l⋙r = ⋙rl y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        x≤y₁ = lexy (trans≤ x≤y₂ y₂≤y₁) ;
                        l'⋙r' = ⋙rl x≤y₁ (lexy x≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        l'≈l = ≈left x≤y₁ y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈left (lexy x≤y₂) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈
                   in ≈right b≤x b≤y l'⋙r' l⋙r l'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let l⋙r = ⋙rl y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        pr'≈r' = lemma-push⋘ (lexy y₂≤x) (lexy refl≤) l₂⋘r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋙r' = ⋙rl (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂ ;
                        l'⋙pr' = lemma⋙≈ l'⋙r' r'≈pr' ;
                        l'≈l = ≈left (lexy y₂≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈left (lexy refl≤) y≤y₂ l₂⋘r₂ l₂⋘r₂ refl≈ refl≈ ;
                        pr'≈r = trans≈ pr'≈r' r'≈r
                   in ≈right (transLeB b≤y y≤y₂) b≤y l'⋙pr' l⋙r l'≈l pr'≈r
  lemma-push⋙ {x = x} b≤x b≤y (⋙rr {x = y₁} {x' = y₂} y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | tot≤ x y₁ | tot≤ x y₂
  ... | inj₁ y₁≤y₂ | inj₁ x≤y₁ | _ =
                   let l⋙r = ⋙rr y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        x≤y₂ = lexy (trans≤ x≤y₁ y₁≤y₂) ;
                        l'⋙r' = ⋙rr (lexy x≤y₁) x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        l'≈l = ≈left (lexy x≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈right x≤y₂ y≤y₂ l₂⋙r₂ l₂⋙r₂ refl≈ refl≈
                   in ≈right b≤x b≤y l'⋙r' l⋙r l'≈l r'≈r
  ... | inj₁ y₁≤y₂ | inj₂ y₁≤x | _ =
                   let l⋙r = ⋙rr y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        pl'≈l' = lemma-push⋘ (lexy y₁≤x) (lexy refl≤) l₁⋘r₁ ;
                        l'⋙r' = ⋙rr (lexy refl≤) (lexy y₁≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        pl'⋙r' = lemma≈⋙ pl'≈l' l'⋙r' ;
                        l'≈l = ≈left (lexy refl≤) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        pl'≈l = trans≈ pl'≈l' l'≈l ;
                        r'≈r = ≈right (lexy y₁≤y₂) y≤y₂ l₂⋙r₂ l₂⋙r₂ refl≈ refl≈
                   in ≈right (transLeB b≤y y≤y₁) b≤y pl'⋙r' l⋙r pl'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₁ x≤y₂ =
                   let l⋙r = ⋙rr y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        x≤y₁ = lexy (trans≤ x≤y₂ y₂≤y₁) ;
                        l'⋙r' = ⋙rr x≤y₁ (lexy x≤y₂) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        l'≈l = ≈left x≤y₁ y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈right (lexy x≤y₂) y≤y₂ l₂⋙r₂ l₂⋙r₂ refl≈ refl≈
                   in ≈right b≤x b≤y l'⋙r' l⋙r l'≈l r'≈r
  ... | inj₂ y₂≤y₁ | _ | inj₂ y₂≤x =
                   let l⋙r = ⋙rr y≤y₁ y≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        pr'≈r' = lemma-push⋙ (lexy y₂≤x) (lexy refl≤) l₂⋙r₂ ;
                        r'≈pr' = sym≈ pr'≈r' ;
                        l'⋙r' = ⋙rr (lexy y₂≤y₁) (lexy refl≤) l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂ ;
                        l'⋙pr' = lemma⋙≈ l'⋙r' r'≈pr' ;
                        l'≈l = ≈left (lexy y₂≤y₁) y≤y₁ l₁⋘r₁ l₁⋘r₁ refl≈ refl≈ ;
                        r'≈r = ≈right (lexy refl≤) y≤y₂ l₂⋙r₂ l₂⋙r₂ refl≈ refl≈ ;
                        pr'≈r = trans≈ pr'≈r' r'≈r
                   in ≈right (transLeB b≤y y≤y₂) b≤y l'⋙pr' l⋙r l'≈l pr'≈r

push : {b : Bound}{x : A} → LeB b (val x) → BBHeap b → BBHeap b
push _ leaf = leaf
push b≤x (left b≤y l⋘r) = push⋘ b≤x b≤y l⋘r
push b≤x (right b≤y l⋙r) = push⋙ b≤x b≤y l⋙r

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import OscarPrelude
open import Sequent

infix 13 _¶_
record Problem : Set
 where
  constructor _¶_
  field
    inferences : List Sequent
    interest : Sequent

open Problem public

instance EqProblem : Eq Problem
EqProblem = {!!}

open import 𝓐ssertion

instance 𝓐ssertionProblem : 𝓐ssertion Problem
𝓐ssertionProblem = record {}

open import HasSatisfaction

instance HasSatisfactionProblem : HasSatisfaction Problem
HasSatisfaction._⊨_ HasSatisfactionProblem I (Φ⁺s ¶ Φ⁻) = I ⊨ Φ⁺s → I ⊨ Φ⁻

open import HasDecidableValidation

instance HasDecidableValidationProblem : HasDecidableValidation Problem
HasDecidableValidationProblem = {!!}

open import HasSubstantiveDischarge

instance HasSubstantiveDischargeProblemProblem : HasSubstantiveDischarge Problem Problem
HasSubstantiveDischarge._≽_ HasSubstantiveDischargeProblemProblem (+s ¶ +) (-s ¶ -) = {!!} -- + ≽ - × +s ≽ -s

open import HasDecidableSubstantiveDischarge

instance HasDecidableSubstantiveDischargeProblemProblem : HasDecidableSubstantiveDischarge Problem Problem
HasDecidableSubstantiveDischarge._≽?_ HasDecidableSubstantiveDischargeProblemProblem = {!!}


text:
-- Andreas, 2015-06-29 constructors should be covariant.
-- They are already treated as strictly positive in the positivity checker.

-- {-# OPTIONS -v tc.polarity:20 -v tc.proj.like:10 #-}
-- {-# OPTIONS -v tc.conv.elim:25 -v tc.conv.atom:30 -v tc.conv.term:30 --show-implicit #-}

open import Common.Size
open import Common.Product

-- U (i : contravariant)
record U (i : Size) : Set where
  coinductive
  field out : (j : Size< i) → U j

record Tup (P : Set × Set) : Set where
  constructor tup
  field
    fst : proj₁ P
    snd : proj₂ P

Dup : Set → Set
Dup X = Tup (X , X)

-- This is accepted, as constructors are taken as monotone.
data D : Set where
  c : Dup D → D

fine : ∀{i} → Dup (U ∞) → Dup (U i)
fine (tup x y) = tup x y

-- This should also be accepted.
-- (Additionally, it is the η-short form of fine.)
cast : ∀{i} → Dup (U ∞) → Dup (U i)
cast x = x


text:
{-# OPTIONS --copatterns #-}
module Copatterns where

open import Common.Equality

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

pair : {A B : Set} → A → B → A × B
fst (pair a b) = a
snd (pair a b) = b

swap : {A B : Set} → A × B → B × A
fst (swap p) = snd p
snd (swap p) = fst p

swap3 : {A B C : Set} → A × (B × C) → C × (B × A)
fst (swap3 t)       = snd (snd t)
fst (snd (swap3 t)) = fst (snd t)
snd (snd (swap3 t)) = fst t

-- should also work if we shuffle the clauses
swap4 : {A B C D : Set} → A × (B × (C × D)) → D × (C × (B × A))
fst (snd (swap4 t))       = fst (snd (snd t))
snd (snd (snd (swap4 t))) = fst t
fst (swap4 t)             = snd (snd (snd t))
fst (snd (snd (swap4 t))) = fst (snd t)

-- State monad example

record State (S A : Set) : Set where
  constructor state
  field
    runState : S → A × S
open State

record Monad (M : Set → Set) : Set1 where
  constructor monad
  field
    return : {A : Set}   → A → M A
    _>>=_  : {A B : Set} → M A → (A → M B) → M B
open Monad {{...}}

stateMonad : {S : Set} → Monad (State S)
runState (return {{stateMonad}} a  ) s  = a , s
runState (_>>=_  {{stateMonad}} m k) s₀ =
  let a , s₁ = runState m s₀
  in  runState (k a) s₁

leftId : {A B S : Set}(a : A)(k : A → State S B) → (return a >>= k) ≡ k a
leftId a k = refl

rightId : {A B S : Set}(m : State S A) → (m >>= return) ≡ m
rightId m = refl

assoc : {A B C S : Set}(m : State S A)(k : A → State S B)(l : B → State S C) →
   ((m >>= k) >>= l) ≡ (m >>= λ a → k a >>= l)
assoc m k l = refl

-- multiple clauses with abstractions

fswap3 : {A B C X : Set} → (X → A) × ((X → B) × C) → (X → C) × (X → (B × A))
fst (fswap3 t) x       = snd (snd t)
fst (snd (fswap3 t) y) = fst (snd t) y
snd (snd (fswap3 t) z) = fst t z

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --universe-polymorphism #-}

module TrustMe where

open import Common.Equality

postulate
  A   : Set
  x y : A

eq : x ≡ y
eq = primTrustMe

does-not-evaluate-to-refl : sym (sym eq) ≡ eq
does-not-evaluate-to-refl = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import OscarPrelude
open import VariableName
open import FunctionName
open import Arity
open import Term
open import Vector

data TermCode : Set
 where
  variable : VariableName → TermCode
  function : FunctionName → Arity → TermCode

termCode-function-inj₁ : ∀ {𝑓₁ 𝑓₂ arity₁ arity₂} → TermCode.function 𝑓₁ arity₁ ≡ function 𝑓₂ arity₂ → 𝑓₁ ≡ 𝑓₂
termCode-function-inj₁ refl = refl

termCode-function-inj₂ : ∀ {𝑓₁ 𝑓₂ arity₁ arity₂} → TermCode.function 𝑓₁ arity₁ ≡ function 𝑓₂ arity₂ → arity₁ ≡ arity₂
termCode-function-inj₂ refl = refl

instance
  EqTermCode : Eq TermCode
  Eq._==_ EqTermCode (variable 𝑥₁) (variable 𝑥₂) with 𝑥₁ ≟ 𝑥₂
  … | yes 𝑥₁≡𝑥₂ rewrite 𝑥₁≡𝑥₂ = yes refl
  … | no 𝑥₁≢𝑥₂ = no (λ { refl → 𝑥₁≢𝑥₂ refl})
  Eq._==_ EqTermCode (variable x) (function x₁ x₂) = no (λ ())
  Eq._==_ EqTermCode (function x x₁) (variable x₂) = no (λ ())
  Eq._==_ EqTermCode (function 𝑓₁ 𝑎₁) (function 𝑓₂ 𝑎₂) = decEq₂ termCode-function-inj₁ termCode-function-inj₂ (𝑓₁ ≟ 𝑓₂) (𝑎₁ ≟ 𝑎₂)

mutual
  encodeTerm : Term → List TermCode
  encodeTerm (variable 𝑥) = variable 𝑥 ∷ []
  encodeTerm (function 𝑓 (⟨_⟩ {arity} τs)) = function 𝑓 arity ∷ encodeTerms τs

  encodeTerms : {arity : Arity} → Vector Term arity → List TermCode
  encodeTerms ⟨ [] ⟩ = []
  encodeTerms ⟨ τ ∷ τs ⟩ = encodeTerm τ ++ encodeTerms ⟨ τs ⟩

mutual

  decodeTerm : Nat → StateT (List TermCode) Maybe Term
  decodeTerm zero = lift nothing
  decodeTerm (suc n) = do
    caseM get of λ
    { [] → lift nothing
    ; (variable 𝑥 ∷ _) →
      modify (drop 1) ~|
      return (variable 𝑥)
    ; (function 𝑓 arity ∷ _) →
      modify (drop 1) ~|
      decodeFunction n 𝑓 arity }

  decodeFunction : Nat → FunctionName → Arity → StateT (List TermCode) Maybe Term
  decodeFunction n 𝑓 arity = do
    τs ← decodeTerms n arity -|
    return (function 𝑓 ⟨ τs ⟩)

  decodeTerms : Nat → (arity : Arity) → StateT (List TermCode) Maybe (Vector Term arity)
  decodeTerms n ⟨ zero ⟩ = return ⟨ [] ⟩
  decodeTerms n ⟨ suc arity ⟩ = do
    τ ← decodeTerm n -|
    τs ← decodeTerms n ⟨ arity ⟩ -|
    return ⟨ τ ∷ vector τs ⟩

.decode-is-inverse-of-encode : ∀ τ → runStateT (decodeTerm ∘ length $ encodeTerm τ) (encodeTerm τ) ≡ (just $ τ , [])
decode-is-inverse-of-encode (variable 𝑥) = refl
decode-is-inverse-of-encode (function 𝑓 ⟨ ⟨ [] ⟩ ⟩) = {!!}
decode-is-inverse-of-encode (function 𝑓 ⟨ ⟨ variable 𝑥 ∷ τs ⟩ ⟩) = {!!}
decode-is-inverse-of-encode (function 𝑓 ⟨ ⟨ function 𝑓' τs' ∷ τs ⟩ ⟩) = {!!}

module ExampleEncodeDecode where
  example-Term : Term
  example-Term =
    (function ⟨ 2 ⟩
              ⟨ ⟨ ( variable ⟨ 0 ⟩ ∷
                  function ⟨ 3 ⟩ ⟨ ⟨ variable ⟨ 2 ⟩ ∷ [] ⟩ ⟩ ∷
                  variable ⟨ 5 ⟩ ∷ [] )
                ⟩ ⟩
    )

  -- function ⟨ 2 ⟩ ⟨ 3 ⟩ ∷ variable ⟨ 0 ⟩ ∷ function ⟨ 3 ⟩ ⟨ 1 ⟩ ∷ variable ⟨ 2 ⟩ ∷ variable ⟨ 5 ⟩ ∷ []
  example-TermCodes : List TermCode
  example-TermCodes = encodeTerm example-Term

  example-TermDecode : Maybe (Term × List TermCode)
  example-TermDecode = runStateT (decodeTerm (length example-TermCodes)) example-TermCodes

  example-verified : example-TermDecode ≡ (just $ example-Term , [])
  example-verified = refl

  example-bad : runStateT (decodeTerm 2) (function ⟨ 2 ⟩ ⟨ 2 ⟩ ∷ variable ⟨ 0 ⟩ ∷ []) ≡ nothing
  example-bad = refl


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

module Definition.Conversion.Stability where

open import Definition.Untyped
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Conversion
open import Definition.Conversion.Soundness
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Equality of contexts.
data ⊢_≡_ : (Γ Δ : Con Term) → Set where
  ε : ⊢ ε ≡ ε
  _∙_ : ∀ {Γ Δ A B} → ⊢ Γ ≡ Δ → Γ ⊢ A ≡ B → ⊢ Γ ∙ A ≡ Δ ∙ B

mutual
  -- Syntactic validity and conversion substitution of a context equality.
  contextConvSubst : ∀ {Γ Δ} → ⊢ Γ ≡ Δ → ⊢ Γ × ⊢ Δ × Δ ⊢ˢ idSubst ∷ Γ
  contextConvSubst ε = ε , ε , id
  contextConvSubst (_∙_ {Γ} {Δ} {A} {B} Γ≡Δ A≡B) =
    let ⊢Γ , ⊢Δ , [σ] = contextConvSubst Γ≡Δ
        ⊢A , ⊢B = syntacticEq A≡B
        Δ⊢B = stability Γ≡Δ ⊢B
    in  ⊢Γ ∙ ⊢A , ⊢Δ ∙ Δ⊢B
        , (wk1Subst′ ⊢Γ ⊢Δ Δ⊢B [σ]
        , conv (var (⊢Δ ∙ Δ⊢B) here)
               (PE.subst (λ x → _ ⊢ _ ≡ x)
                         (wk1-tailId A)
                         (wkEq (step id) (⊢Δ ∙ Δ⊢B) (stabilityEq Γ≡Δ (sym A≡B)))))

  -- Stability of types under equal contexts.
  stability : ∀ {A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A → Δ ⊢ A
  stability Γ≡Δ A =
    let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
        q = substitution A σ ⊢Δ
    in  PE.subst (λ x → _ ⊢ x) (subst-id _) q

  -- Stability of type equality.
  stabilityEq : ∀ {A B Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ≡ B → Δ ⊢ A ≡ B
  stabilityEq Γ≡Δ A≡B =
    let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
        q = substitutionEq A≡B (substRefl σ) ⊢Δ
    in  PE.subst₂ (λ x y → _ ⊢ x ≡ y) (subst-id _) (subst-id _) q

-- Reflexivity of context equality.
reflConEq : ∀ {Γ} → ⊢ Γ → ⊢ Γ ≡ Γ
reflConEq ε = ε
reflConEq (⊢Γ ∙ ⊢A) = reflConEq ⊢Γ ∙ refl ⊢A

-- Symmetry of context equality.
symConEq : ∀ {Γ Δ} → ⊢ Γ ≡ Δ → ⊢ Δ ≡ Γ
symConEq ε = ε
symConEq (Γ≡Δ ∙ A≡B) = symConEq Γ≡Δ ∙ stabilityEq Γ≡Δ (sym A≡B)

-- Stability of terms.
stabilityTerm : ∀ {t A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t ∷ A → Δ ⊢ t ∷ A
stabilityTerm Γ≡Δ t =
  let ⊢Γ , ⊢Δ , σ = contextConvSubst Γ≡Δ
      q = substitutionTerm t σ ⊢Δ
  in  PE.subst₂ (λ x y → _ ⊢ x ∷ y) (subst-id _) (subst-id _) q

-- Stability of term reduction.
stabilityRedTerm : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t ⇒ u ∷ A → Δ ⊢ t ⇒ u ∷ A
stabilityRedTerm Γ≡Δ (conv d x) =
  conv (stabilityRedTerm Γ≡Δ d) (stabilityEq Γ≡Δ x)
stabilityRedTerm Γ≡Δ (app-subst d x) =
  app-subst (stabilityRedTerm Γ≡Δ d) (stabilityTerm Γ≡Δ x)
stabilityRedTerm Γ≡Δ (fst-subst ⊢F ⊢G t⇒) =
  fst-subst (stability Γ≡Δ ⊢F)
            (stability (Γ≡Δ ∙ refl ⊢F) ⊢G)
            (stabilityRedTerm Γ≡Δ t⇒)
stabilityRedTerm Γ≡Δ (snd-subst ⊢F ⊢G t⇒) =
  snd-subst (stability Γ≡Δ ⊢F)
            (stability (Γ≡Δ ∙ refl ⊢F) ⊢G)
            (stabilityRedTerm Γ≡Δ t⇒)
stabilityRedTerm Γ≡Δ (Σ-β₁ ⊢F ⊢G ⊢t ⊢u) =
  Σ-β₁ (stability Γ≡Δ ⊢F)
       (stability (Γ≡Δ ∙ refl ⊢F) ⊢G)
       (stabilityTerm Γ≡Δ ⊢t)
       (stabilityTerm Γ≡Δ ⊢u)
stabilityRedTerm Γ≡Δ (Σ-β₂ ⊢F ⊢G ⊢t ⊢u) =
  Σ-β₂ (stability Γ≡Δ ⊢F)
       (stability (Γ≡Δ ∙ refl ⊢F) ⊢G)
       (stabilityTerm Γ≡Δ ⊢t)
       (stabilityTerm Γ≡Δ ⊢u)
stabilityRedTerm Γ≡Δ (β-red x x₁ x₂) =
  β-red (stability Γ≡Δ x) (stabilityTerm (Γ≡Δ ∙ refl x) x₁)
        (stabilityTerm Γ≡Δ x₂)
stabilityRedTerm Γ≡Δ (natrec-subst x x₁ x₂ d) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-subst (stability (Γ≡Δ ∙ refl (ℕⱼ ⊢Γ)) x) (stabilityTerm Γ≡Δ x₁)
                   (stabilityTerm Γ≡Δ x₂) (stabilityRedTerm Γ≡Δ d)
stabilityRedTerm Γ≡Δ (natrec-zero x x₁ x₂) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-zero (stability (Γ≡Δ ∙ refl (ℕⱼ ⊢Γ)) x) (stabilityTerm Γ≡Δ x₁)
                  (stabilityTerm Γ≡Δ x₂)
stabilityRedTerm Γ≡Δ (natrec-suc x x₁ x₂ x₃) =
  let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
  in  natrec-suc (stabilityTerm Γ≡Δ x) (stability (Γ≡Δ ∙ refl (ℕⱼ ⊢Γ)) x₁)
                 (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₃)
stabilityRedTerm Γ≡Δ (Emptyrec-subst x d) =
  Emptyrec-subst (stability Γ≡Δ x) (stabilityRedTerm Γ≡Δ d)

-- Stability of type reductions.
stabilityRed : ∀ {A B Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ⇒ B → Δ ⊢ A ⇒ B
stabilityRed Γ≡Δ (univ x) = univ (stabilityRedTerm Γ≡Δ x)

-- Stability of type reduction closures.
stabilityRed* : ∀ {A B Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A ⇒* B → Δ ⊢ A ⇒* B
stabilityRed* Γ≡Δ (id x) = id (stability Γ≡Δ x)
stabilityRed* Γ≡Δ (x ⇨ D) = stabilityRed Γ≡Δ x ⇨ stabilityRed* Γ≡Δ D

-- Stability of term reduction closures.
stabilityRed*Term : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t ⇒* u ∷ A → Δ ⊢ t ⇒* u ∷ A
stabilityRed*Term Γ≡Δ (id x) = id (stabilityTerm Γ≡Δ x)
stabilityRed*Term Γ≡Δ (x ⇨ d) = stabilityRedTerm Γ≡Δ x ⇨ stabilityRed*Term Γ≡Δ d

mutual
  -- Stability of algorithmic equality of neutrals.
  stability~↑ : ∀ {k l A Γ Δ}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↑ A
              → Δ ⊢ k ~ l ↑ A
  stability~↑ Γ≡Δ (var-refl x x≡y) =
    var-refl (stabilityTerm Γ≡Δ x) x≡y
  stability~↑ Γ≡Δ (app-cong k~l x) =
    app-cong (stability~↓ Γ≡Δ k~l) (stabilityConv↑Term Γ≡Δ x)
  stability~↑ Γ≡Δ (fst-cong p~r) =
    fst-cong (stability~↓ Γ≡Δ p~r)
  stability~↑ Γ≡Δ (snd-cong p~r) =
    snd-cong (stability~↓ Γ≡Δ p~r)
  stability~↑ Γ≡Δ (natrec-cong x₁ x₂ x₃ k~l) =
    let ⊢Γ , _ , _ = contextConvSubst Γ≡Δ
    in natrec-cong (stabilityConv↑ (Γ≡Δ ∙ (refl (ℕⱼ ⊢Γ))) x₁)
                   (stabilityConv↑Term Γ≡Δ x₂)
                   (stabilityConv↑Term Γ≡Δ x₃)
                   (stability~↓ Γ≡Δ k~l)
  stability~↑ Γ≡Δ (Emptyrec-cong x₁ k~l) =
    Emptyrec-cong (stabilityConv↑ Γ≡Δ x₁)
                (stability~↓ Γ≡Δ k~l)

  -- Stability of algorithmic equality of neutrals of types in WHNF.
  stability~↓ : ∀ {k l A Γ Δ}
              → ⊢ Γ ≡ Δ
              → Γ ⊢ k ~ l ↓ A
              → Δ ⊢ k ~ l ↓ A
  stability~↓ Γ≡Δ ([~] A D whnfA k~l) =
    [~] A (stabilityRed* Γ≡Δ D) whnfA (stability~↑ Γ≡Δ k~l)

  -- Stability of algorithmic equality of types.
  stabilityConv↑ : ∀ {A B Γ Δ}
                 → ⊢ Γ ≡ Δ
                 → Γ ⊢ A [conv↑] B
                 → Δ ⊢ A [conv↑] B
  stabilityConv↑ Γ≡Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] A′ B′ (stabilityRed* Γ≡Δ D) (stabilityRed* Γ≡Δ D′) whnfA′ whnfB′
        (stabilityConv↓ Γ≡Δ A′<>B′)

  -- Stability of algorithmic equality of types in WHNF.
  stabilityConv↓ : ∀ {A B Γ Δ}
                 → ⊢ Γ ≡ Δ
                 → Γ ⊢ A [conv↓] B
                 → Δ ⊢ A [conv↓] B
  stabilityConv↓ Γ≡Δ (U-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  U-refl ⊢Δ
  stabilityConv↓ Γ≡Δ (ℕ-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  ℕ-refl ⊢Δ
  stabilityConv↓ Γ≡Δ (Empty-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Empty-refl ⊢Δ
  stabilityConv↓ Γ≡Δ (Unit-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Unit-refl ⊢Δ
  stabilityConv↓ Γ≡Δ (ne x) =
    ne (stability~↓ Γ≡Δ x)
  stabilityConv↓ Γ≡Δ (Π-cong F A<>B A<>B₁) =
    Π-cong (stability Γ≡Δ F) (stabilityConv↑ Γ≡Δ A<>B)
           (stabilityConv↑ (Γ≡Δ ∙ refl F) A<>B₁)
  stabilityConv↓ Γ≡Δ (Σ-cong F A<>B A<>B₁) =
    Σ-cong (stability Γ≡Δ F) (stabilityConv↑ Γ≡Δ A<>B)
           (stabilityConv↑ (Γ≡Δ ∙ refl F) A<>B₁)

  -- Stability of algorithmic equality of terms.
  stabilityConv↑Term : ∀ {t u A Γ Δ}
                     → ⊢ Γ ≡ Δ
                     → Γ ⊢ t [conv↑] u ∷ A
                     → Δ ⊢ t [conv↑] u ∷ A
  stabilityConv↑Term Γ≡Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ B t′ u′ (stabilityRed* Γ≡Δ D) (stabilityRed*Term Γ≡Δ d)
                 (stabilityRed*Term Γ≡Δ d′) whnfB whnft′ whnfu′
                 (stabilityConv↓Term Γ≡Δ t<>u)

  -- Stability of algorithmic equality of terms in WHNF.
  stabilityConv↓Term : ∀ {t u A Γ Δ}
                     → ⊢ Γ ≡ Δ
                     → Γ ⊢ t [conv↓] u ∷ A
                     → Δ ⊢ t [conv↓] u ∷ A
  stabilityConv↓Term Γ≡Δ (ℕ-ins x) =
    ℕ-ins (stability~↓ Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (Empty-ins x) =
    Empty-ins (stability~↓ Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (Unit-ins x) =
    Unit-ins (stability~↓ Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (ne-ins t u neN x) =
    ne-ins (stabilityTerm Γ≡Δ t) (stabilityTerm Γ≡Δ u) neN (stability~↓ Γ≡Δ x)
  stabilityConv↓Term Γ≡Δ (univ x x₁ x₂) =
    univ (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁) (stabilityConv↓ Γ≡Δ x₂)
  stabilityConv↓Term Γ≡Δ (zero-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  stabilityConv↓Term Γ≡Δ (suc-cong t<>u) = suc-cong (stabilityConv↑Term Γ≡Δ t<>u)
  stabilityConv↓Term Γ≡Δ (η-eq x x₁ y y₁ t<>u) =
    let ⊢F , ⊢G = syntacticΠ (syntacticTerm x)
    in  η-eq (stabilityTerm Γ≡Δ x) (stabilityTerm Γ≡Δ x₁)
             y y₁ (stabilityConv↑Term (Γ≡Δ ∙ refl ⊢F) t<>u)
  stabilityConv↓Term Γ≡Δ (Σ-η ⊢p ⊢r pProd rProd fstConv sndConv) =
    Σ-η (stabilityTerm Γ≡Δ ⊢p) (stabilityTerm Γ≡Δ ⊢r)
        pProd rProd
        (stabilityConv↑Term Γ≡Δ fstConv) (stabilityConv↑Term Γ≡Δ sndConv)
  stabilityConv↓Term Γ≡Δ (η-unit [t] [u] tUnit uUnit) =
    let [t] = stabilityTerm Γ≡Δ [t]
        [u] = stabilityTerm Γ≡Δ [u]
    in  η-unit [t] [u] tUnit uUnit


text:
------------------------------------------------------------------------
-- Some lemmas used by the other modules in this directory
------------------------------------------------------------------------

module Hinze.Lemmas where

open import Stream.Programs
open import Stream.Equality

open import Codata.Musical.Notation hiding (∞)
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_; flip)

------------------------------------------------------------------------
-- Some lemmas from Section 2.3 of Hinze's paper

-- See also Stream.Equality.≊-η.

⋎-∞ : ∀ {A} (x : A) → x ∞ ⋎ x ∞ ≊ x ∞
⋎-∞ x = refl ≺ ♯ ⋎-∞ x

⋎-map : ∀ {A B} (⊟ : A → B) s t →
        ⊟ · s ⋎ ⊟ · t ≊ ⊟ · (s ⋎ t)
⋎-map ⊟ s t with whnf s
⋎-map ⊟ s t | x ≺ s′ = refl ≺ ♯ ⋎-map ⊟ t s′

abide-law : ∀ {A B C} (⊞ : A → B → C) s₁ s₂ t₁ t₂ →
            s₁ ⟨ ⊞ ⟩ s₂ ⋎ t₁ ⟨ ⊞ ⟩ t₂ ≊ (s₁ ⋎ t₁) ⟨ ⊞ ⟩ (s₂ ⋎ t₂)
abide-law ⊞ s₁ s₂ t₁ t₂ with whnf s₁ | whnf s₂
abide-law ⊞ s₁ s₂ t₁ t₂ | x₁ ≺ s₁′ | x₂ ≺ s₂′ =
  refl ≺ ♯ abide-law ⊞ t₁ t₂ s₁′ s₂′

------------------------------------------------------------------------
-- Other lemmas

tailP-cong : ∀ {A} (xs ys : Prog A) →
             xs ≊ ys → tailP xs ≊ tailP ys
tailP-cong xs ys xs≈ys with whnf xs | whnf ys | ≅⇒≃ xs≈ys
tailP-cong xs ys xs≈ys | x ≺ xs′ | y ≺ ys′ | x≡y ≺ xs≈ys′ = xs≈ys′

map-fusion : ∀ {A B C} (f : B → C) (g : A → B) xs →
             f · g · xs ≊ (f ∘ g) · xs
map-fusion f g xs with whnf xs
map-fusion f g xs | x ≺ xs′ = refl ≺ ♯ map-fusion f g xs′

zip-const-is-map : ∀ {A B C} (_∙_ : A → B → C) xs y →
                   xs ⟨ _∙_ ⟩ y ∞ ≊ (λ x → x ∙ y) · xs
zip-const-is-map _∙_ xs y with whnf xs
zip-const-is-map _∙_ xs y | x ≺ xs′ =
  refl ≺ ♯ zip-const-is-map _∙_ xs′ y

zip-flip : ∀ {A B C} (∙ : A → B → C) s t →
           s ⟨ ∙ ⟩ t ≊ t ⟨ flip ∙ ⟩ s
zip-flip ∙ s t with whnf s | whnf t
zip-flip ∙ s t | x ≺ s′ | y ≺ t′ = refl ≺ ♯ zip-flip ∙ s′ t′

zip-⋎-const : ∀ {A B C} (∙ : A → B → C) s t x →
              (s ⋎ t) ⟨ ∙ ⟩ x ∞ ≊ s ⟨ ∙ ⟩ x ∞ ⋎ t ⟨ ∙ ⟩ x ∞
zip-⋎-const _∙_ s t x =
  (s ⋎ t) ⟨ _∙_ ⟩ x ∞
                                         ≊⟨ zip-const-is-map _ (s ⋎ t) _ ⟩
  (λ y → y ∙ x) · (s ⋎ t)
                                         ≊⟨ ≅-sym (⋎-map (λ y → y ∙ x) s t) ⟩
  (λ y → y ∙ x) · s ⋎ (λ y → y ∙ x) · t
                                         ≊⟨ ≅-sym (⋎-cong (s ⟨ _∙_ ⟩ x ∞) ((λ y → y ∙ x) · s)
                                                          (zip-const-is-map _∙_ s x)
                                                      _ _ (zip-const-is-map _∙_ t x)) ⟩
  s ⟨ _∙_ ⟩ x ∞ ⋎ t ⟨ _∙_ ⟩ x ∞
                                         ∎

zip-const-⋎ : ∀ {A B C} (∙ : A → B → C) x s t →
              x ∞ ⟨ ∙ ⟩ (s ⋎ t) ≊ x ∞ ⟨ ∙ ⟩ s ⋎ x ∞ ⟨ ∙ ⟩ t
zip-const-⋎ ∙ x s t =
  x ∞ ⟨ ∙ ⟩ (s ⋎ t)
                                       ≊⟨ zip-flip ∙ (x ∞) (s ⋎ t) ⟩
  (s ⋎ t) ⟨ flip ∙ ⟩ x ∞
                                       ≊⟨ zip-⋎-const (flip ∙) s t x ⟩
  s ⟨ flip ∙ ⟩ x ∞ ⋎ t ⟨ flip ∙ ⟩ x ∞
                                       ≊⟨ ≅-sym (⋎-cong (x ∞ ⟨ ∙ ⟩ s) (s ⟨ flip ∙ ⟩ x ∞)
                                                        (zip-flip ∙ (x ∞) s)
                                                    _ _ (zip-flip ∙ (x ∞) t)) ⟩
  x ∞ ⟨ ∙ ⟩ s ⋎ x ∞ ⟨ ∙ ⟩ t
                                       ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module MultipleIdentifiersOneSignature where

data Bool : Set where
  false true : Bool

not : Bool → Bool
not true = false
not false = true

data Suit : Set where
  ♥ ♢ ♠ ♣ : Suit

record R : Set₁ where
  field
    A B C : Set

postulate
  A : Set
  B C    : Set

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

primitive
  primIsDigit primIsSpace : Char → Bool

.b : Bool
b = true

f g h : Bool
f = true
g = false
h = true

.i j .k : Bool
i = not b
j = true
k = not (not b)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of pretty printing of rose trees
------------------------------------------------------------------------

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

module README.Text.Tree where

open import Data.List.Base
open import Data.String.Base
open import Data.Tree.Rose
open import Function.Base
open import Agda.Builtin.Equality

------------------------------------------------------------------------
-- We import the module defining the pretty printer for rose trees

open import Text.Tree.Linear

------------------------------------------------------------------------
-- Example

_ : unlines (display
  $ node [ "one" ]
      (node [ "two" ] []
     ∷ node ("three" ∷ "and" ∷ "four" ∷ [])
         (node [ "five" ] []
        ∷ node [ "six" ] (node [ "seven" ] [] ∷ [])
        ∷ node [ "eight" ] []
        ∷ [])
     ∷ node [ "nine" ]
         (node [ "ten" ] []
        ∷ node [ "eleven" ] [] ∷ [])
        ∷ []))
  ≡ "one
\   \ ├ two
\   \ ├ three
\   \ │ and
\   \ │ four
\   \ │  ├ five
\   \ │  ├ six
\   \ │  │  └ seven
\   \ │  └ eight
\   \ └ nine
\   \    ├ ten
\   \    └ eleven"
_ = refl


text:
-- The ATP pragma with the role <definition> can be used with functions.

module ATPDefinition where

postulate
  D    : Set
  zero : D
  succ : D → D

one : D
one = succ zero
{-# ATP definition one #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

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

open import LibraBFT.Base.Types
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.BlockStorage.SyncManager
open import LibraBFT.Impl.Consensus.ConsensusTypes.Vote as Vote
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.Properties.Util
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import LibraBFT.Impl.Consensus.BlockStorage.BlockStore
open import LibraBFT.Impl.Properties.Util
open import Optics.All
open import Util.ByteString
open import Util.Hash
open import Util.PKCS
open import Util.Prelude
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

open Invariants
open RoundManagerTransProps
open OutputProps

module LibraBFT.Impl.Consensus.BlockStorage.Properties.SyncManager where

module insertQuorumCertMSpec
  (qc : QuorumCert) (retriever : BlockRetriever) where

  open insertQuorumCertM qc retriever
  open import LibraBFT.Impl.Consensus.BlockStorage.Properties.BlockStore

  module _ (pre : RoundManager) where

    record Contract (r : Either ErrLog Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        noEpochChange : NoEpochChange pre post
        noVoteOuts    : NoVotes outs
        -- Voting
        noVote        : VoteNotGenerated pre post true
        -- Signatures
        outQcs∈RM : QCProps.OutputQc∈RoundManager outs post
        qcPost  : QCProps.∈Post⇒∈PreOr (_≡ qc) pre post

  private -- NOTE: need to re-generalize over `pre` because the prestate might differ
    module step₁Spec (bs : BlockStore) (pool : SentMessages) (pre : RoundManager) where
      postulate -- TODO-2: Prove
        contract' : LBFT-weakestPre (step₁ bs) (Contract pre) pre

      contract : ∀ Q → RWS-Post-⇒ (Contract pre) Q → LBFT-weakestPre (step₁ bs) Q pre
      contract Q pf = LBFT-⇒ (step₁ bs) pre contract' pf

  module _ (pool : SentMessages) (pre : RoundManager) where
    contract' : LBFT-weakestPre (insertQuorumCertM qc retriever) (Contract pre) pre
    proj₁ (contract' bs@._ refl) _ nfIsLeft ._ refl = step₁Spec.contract' bs pool pre
    proj₂ (contract' bs@._ refl) NeedFetch nf≡ =
      obm-dangerous-magic' "TODO: waiting on contract for `fetchQuorumCertM`"
    proj₂ (contract' bs@._ refl) QCBlockExist nf≡ =
      insertSingleQuorumCertMSpec.contract qc pre Post₁ contract₁
      where
      Post₁ : LBFT-Post (Either ErrLog Unit)
      Post₁ =
        (RWS-weakestPre-∙^∙Post unit (withErrCtx $ "" ∷ [])
          (RWS-weakestPre-ebindPost unit (λ _ → use lBlockStore >>= (λ _ → logInfo fakeInfo) >> ok unit)
            (RWS-weakestPre-bindPost unit (λ _ → step₁ bs) (Contract pre))))

      module _ (r₁ : Either ErrLog Unit) (st₁ : RoundManager) (outs₁ : List Output) (con₁ : insertSingleQuorumCertMSpec.Contract qc pre r₁ st₁ outs₁) where
        module ISQC = insertSingleQuorumCertMSpec.Contract con₁

        contract₁' : ∀ outs' → NoMsgs outs' → RWS-Post-⇒ (Contract st₁) (RWS-Post++ (Contract pre) outs')
        contract₁' outs' noMsgs r₂ st₂ outs₂ con₂ =
          mkContract
            (transPreservesRoundManagerInv ISQC.rmInv Step₁.rmInv)
            (transNoEpochChange{i = pre}{st₁}{st₂} ISQC.noEpochChange Step₁.noEpochChange)
            (++-NoVotes outs' outs₂ (NoMsgs⇒NoVotes outs' noMsgs) Step₁.noVoteOuts)
            (transVoteNotGenerated ISQC.noVote Step₁.noVote)
            (QCProps.++-OutputQc∈RoundManager{st₂}{outs'}{outs₂} (QCProps.NoMsgs⇒OutputQc∈RoundManager outs' st₂ noMsgs) Step₁.outQcs∈RM)
            qcPost
          where
          module Step₁ = Contract con₂

          qcPost : QCProps.∈Post⇒∈PreOr (_≡ qc) pre st₂
          qcPost qc qc∈st₂
             with Step₁.qcPost qc qc∈st₂
          ...| Right qc≡ = Right qc≡
          ...| Left qc∈st₁
             with ISQC.qcPost qc qc∈st₁
          ...| Right qc≡ = Right qc≡
          ...| Left qc∈pre = Left qc∈pre

      contract₁ : RWS-Post-⇒ (insertSingleQuorumCertMSpec.Contract qc pre) Post₁
      contract₁ (Left _) st₁ outs₁ con₁ ._ refl ._ refl =
        step₁Spec.contract bs pool st₁ (RWS-Post++ (Contract pre) (outs₁ ++ []))
          (contract₁' _ _ _ con₁ (outs₁ ++ [])
            (++-NoMsgs outs₁ [] (insertSingleQuorumCertMSpec.Contract.noMsgOuts con₁) refl))
      contract₁ (Right y) st₁ outs₁ con₁ ._ refl ._ refl ._ refl ._ refl ._ refl =
        step₁Spec.contract bs pool st₁ (RWS-Post++ (Contract pre) ((outs₁ ++ []) ++ LogInfo fakeInfo ∷ []))
          (contract₁' _ _ _ con₁ ((outs₁ ++ []) ++ LogInfo fakeInfo ∷ [])
            (++-NoMsgs (outs₁ ++ []) (LogInfo fakeInfo ∷ [])
              (++-NoMsgs outs₁ [] (insertSingleQuorumCertMSpec.Contract.noMsgOuts con₁) refl)
              refl))

    proj₂ (contract' bs@._ refl) QCRoundBeforeRoot _ ._ refl = step₁Spec.contract' bs pool pre
    proj₂ (contract' bs@._ refl) QCAlreadyExist _ ._ refl = step₁Spec.contract' bs pool pre

module addCertsMSpec
  (syncInfo : SyncInfo) (retriever : BlockRetriever) where

  module _ (pre : RoundManager) where

    record Contract (r : Either ErrLog Unit) (post : RoundManager) (outs : List Output) : Set where
      constructor mkContract
      field
        -- General invariants / properties
        rmInv         : Preserves RoundManagerInv pre post
        dnmBtIdToBlk  : post ≡L pre at (lBlockTree ∙ btIdToBlock)
        noEpochChange : NoEpochChange pre post
        noVoteOuts    : OutputProps.NoVotes outs
        -- Voting
        noVote        : VoteNotGenerated pre post true
        -- Signatures
        noOutQc : QCProps.¬OutputQc outs
        qcPost  : QCProps.∈Post⇒∈PreOr (_QC∈SyncInfo syncInfo) pre post

    postulate -- TODO-2: prove
      contract' : LBFT-weakestPre (addCertsM syncInfo retriever) Contract pre

    contract : ∀ Q → RWS-Post-⇒ Contract Q → LBFT-weakestPre (addCertsM syncInfo retriever) Q pre
    contract Q pf = LBFT-⇒ (addCertsM syncInfo retriever) pre contract' pf


text:
module Hello where

data Bool : Set where
  true : Bool
  false : Bool

data Unit : Set where
  one : Unit

unit : Unit
unit = ?

test : Bool → Bool
test x = ?

unicodeTest₁ : Bool → Bool
unicodeTest₁ x = ?

slap : Bool → Bool
slap = λ { x → ? }

module _ where
  testIndent : Bool → Bool
  testIndent true = ?
  testIndent false = ?


text:
-- Andreas, 2012-01-13
module Issue555b where

data Empty : Set where
record Unit : Set where
  constructor tt

-- Do we want to allow this?
data Exp (A : Set) : Set1
data Exp where -- ? needs to report that too few parameters are given
  var : Exp Empty
  app : {A B : Set} → Exp (A → B) → Exp A → Exp B

-- Basically, A is first declared as a parameter, but later,
-- in the definition, it is turned into an index.

bla : {A : Set} → Exp A → Unit
bla var = tt
bla (app f a) = bla f

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Data.Binary.Bits where

open import Data.Bool
  as Bool
  using (not; _∨_; _∧_; _xor_; T)
  renaming (Bool to Bit; true to I; false to O)
  public

_xnor_ : Bit → Bit → Bit
O xnor y = not y
I xnor y = y

sumᵇ : Bit → Bit → Bit → Bit
sumᵇ O = _xor_
sumᵇ I = _xnor_

carryᵇ : Bit → Bit → Bit → Bit
carryᵇ O = _∧_
carryᵇ I = _∨_

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module Span where

open import Prelude
open import Star
open import Modal

data SpanView {A : Set}{R : Rel A}(p : {a b : A} -> R a b -> Bool) :
              EdgePred (Star R) where
  oneFalse : {a b c d : A}(xs : Star R a b)(pxs : All (\x -> IsTrue (p x)) xs)
             (x : R b c)(¬px : IsFalse (p x))(ys : Star R c d) ->
             SpanView p (xs ++ x • ys)
  allTrue  : {a b : A}{xs : Star R a b}(ts : All (\x -> IsTrue (p x)) xs) ->
             SpanView p xs

span : {A : Set}{R : Rel A}(p : {a b : A} -> R a b -> Bool){a b : A}
       (xs : Star R a b) -> SpanView p xs
span p ε = allTrue ε
span p (x • xs) with inspect (p x)
span p (x • xs) | itsFalse ¬px = oneFalse ε ε x ¬px xs
span p (x • xs) | itsTrue px with span p xs
span p (x • .(xs ++ y • ys)) | itsTrue px
     | oneFalse xs pxs y ¬py ys =
       oneFalse (x • xs) (check px • pxs) y ¬py ys
span p (x • xs) | itsTrue px | allTrue pxs =
       allTrue (check px • pxs)

_│_ : {A : Set}(R : Rel A)(P : EdgePred R) -> Rel A
(R │ P) a b = Σ (R a b) P

forget : {A : Set}{R : Rel A}{P : EdgePred R} -> Star (R │ P) =[ id ]=> Star R
forget = map id fst

data SpanView' {A : Set}{R : Rel A}(p : {a b : A} -> R a b -> Bool) :
               EdgePred (Star R) where
  oneFalse' : {a b c d : A}(xs : Star (R │ \{a b} x -> IsTrue (p x)) a b)
              (x : R b c)(¬px : IsFalse (p x))(ys : Star R c d) ->
              SpanView' p (forget xs ++ x • ys)
  allTrue'  : {a b : A}(xs : Star (R │ \{a b} x -> IsTrue (p x)) a b) ->
              SpanView' p (forget xs)

span' : {A : Set}{R : Rel A}(p : {a b : A} -> R a b -> Bool){a b : A}
        (xs : Star R a b) -> SpanView' p xs
span' p ε = allTrue' ε
span' p (x • xs) with inspect (p x)
span' p (x • xs) | itsFalse ¬px = oneFalse' ε x ¬px xs
span' p (x • xs) | itsTrue px with span' p xs
span' p (x • .(forget xs ++ y • ys)) | itsTrue px
        | oneFalse' xs y ¬py ys = oneFalse' ((x ,, px) • xs) y ¬py ys
span' p (x • .(forget xs)) | itsTrue px
        | allTrue' xs = allTrue' ((x ,, px) • xs)

-- Can't seem to define it as 'map Some.a (\x -> (_ ,, uncheck x))'
all│ : {A : Set}{R : Rel A}{P : EdgePred R}{a b : A}{xs : Star R a b} ->
       All P xs -> Star (R │ P) a b
all│ (check p • pxs) = (_ ,, p) • all│ pxs
all│ ε               = ε


text:
module Issue396 where

record ⊤ : Set where
  constructor tt

foo : (P : ⊤ → Set) →
      ((x : ⊤) → P x → P x) →
      (x y : ⊤) → P x → P y
foo P hyp x y = hyp x

-- Error was:
-- x != y of type ⊤
-- when checking that the expression hyp x has type P x → P y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Bifunctor.NaturalTransformation where

open import Level

open import Categories.Category
open import Categories.Bifunctor
open import Categories.Product

open import Categories.NaturalTransformation public

-- just for completeness ...
BiNaturalTransformation : ∀ {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o′′ ℓ′′ e′′} → Bifunctor C D E → Bifunctor C D E → Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ o′′ ⊔ ℓ′′ ⊔ e′′)
BiNaturalTransformation F G = NaturalTransformation F G

reduceN-× : ∀ {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} (H : Bifunctor D₁ D₂ C) {o″₁ ℓ″₁ e″₁} {E₁ : Category o″₁ ℓ″₁ e″₁} {F F′ : Functor E₁ D₁} (φ : NaturalTransformation F F′) {o″₂ ℓ″₂ e″₂} {E₂ : Category o″₂ ℓ″₂ e″₂} {G G′ : Functor E₂ D₂} (γ : NaturalTransformation G G′) → NaturalTransformation (reduce-× {D₁ = D₁} {D₂ = D₂} H F G) (reduce-× {D₁ = D₁} {D₂ = D₂} H F′ G′)
reduceN-× H φ γ = H ∘ˡ (φ ⁂ⁿ γ)

overlapN-× : ∀ {o ℓ e} {o′₁ ℓ′₁ e′₁} {o′₂ ℓ′₂ e′₂} {C : Category o ℓ e} {D₁ : Category o′₁ ℓ′₁ e′₁} {D₂ : Category o′₂ ℓ′₂ e′₂} (H : Bifunctor D₁ D₂ C) {o″ ℓ″ e″} {E : Category o″ ℓ″ e″} {F F′ : Functor E D₁} (φ : NaturalTransformation F F′) {G G′ : Functor E D₂} (γ : NaturalTransformation G G′) → NaturalTransformation (overlap-× {D₁ = D₁} {D₂ = D₂} H F G) (overlap-× {D₁ = D₁} {D₂ = D₂} H F′ G′)
overlapN-× H φ γ = H ∘ˡ (φ ※ⁿ γ)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module plfa-code.Connectives where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa-code.Isomorphism using (_≃_; _≲_; extensionality)
open plfa-code.Isomorphism.≃-Reasoning

data _×_ (A B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  → B
proj₂ ⟨ x , y ⟩ = y

record _×′_ (A B : Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , y ⟩ = refl

infixr 2 _×_

data Bool : Set where
  true  : Bool
  false : Bool

data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

×-count : Bool × Tri → ℕ
×-count ⟨ true  , aa ⟩  =  1
×-count ⟨ true  , bb ⟩  =  2
×-count ⟨ true  , cc ⟩  =  3
×-count ⟨ false , aa ⟩  =  4
×-count ⟨ false , bb ⟩  =  5
×-count ⟨ false , cc ⟩  =  6

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { to       =  λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; from     =  λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; from∘to  =  λ{ ⟨ x , y ⟩ → refl }
    ; to∘from  =  λ{ ⟨ y , x ⟩ → refl }
    }

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
  record
    { to      = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
    ; from    = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
    ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
    ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
    }

---------- practice ----------
open plfa-code.Isomorphism using (_⇔_)
open _⇔_

⇔-≃-→×→ : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
⇔-≃-→×→ =
  record
  { to      = λ x → ⟨ to x , from x ⟩
  ; from    = λ{ ⟨ A→B , B→A ⟩ → record { to = A→B ; from = B→A } }
  ; from∘to = λ x → refl
  ; to∘from = λ{ ⟨ A→B , B→A ⟩ → refl }
  }

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

data ⊤ : Set where

  tt :
    --
    ⊤

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl

⊤-count : ⊤ → ℕ
⊤-count tt = 1

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
⊤-identityˡ =
  record
    { to      = λ{ ⟨ tt , x ⟩ → x }
    ; from    = λ x → ⟨ tt , x ⟩
    ; from∘to = λ{ ⟨ tt , x ⟩ → refl }
    ; to∘from = λ x → refl
    }

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ {A} =
  ≃-begin
    (A × ⊤)
  ≃⟨ ×-comm ⟩
    (⊤ × A)
  ≃⟨ ⊤-identityˡ ⟩
    A
  ≃-∎

data _⊎_ (A B : Set) : Set where

  inj₁ :
      A
      -----
    → A ⊎ B

  inj₂ :
      B
      -----
    → A ⊎ B

case-⊎ : ∀ {A B C : Set}
  → (A → C)
  → (B → C)
  → A ⊎ B
    -----------
  → C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ y) = g y

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
  case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl

infix 1 _⊎_

⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true)  =  1
⊎-count (inj₁ false) =  2
⊎-count (inj₂ aa)    =  3
⊎-count (inj₂ bb)    =  4
⊎-count (inj₂ cc)    =  5

---------- practice ----------
⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm =
  record
  { to      = λ{(inj₁ a) → inj₂ a ; (inj₂ b) → inj₁ b }
  ; from    = λ{(inj₁ b) → inj₂ b ; (inj₂ a) → inj₁ a }
  ; from∘to = λ{(inj₁ a) → refl ; (inj₂ b) → refl }
  ; to∘from = λ{(inj₁ b) → refl ; (inj₂ a) → refl }
  }

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc =
  record
  { to      = to′
  ; from    = from′
  ; from∘to = from∘to′
  ; to∘from = to∘from′
  }
  where
    to′ : ∀ {A B C : Set} → (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
    to′ (inj₁ (inj₁ a)) = inj₁ a
    to′ (inj₁ (inj₂ b)) = inj₂ (inj₁ b)
    to′ (inj₂ c) = inj₂ (inj₂ c)
    from′ : ∀ {A B C : Set} → A ⊎ (B ⊎ C) → (A ⊎ B) ⊎ C
    from′ (inj₁ a) = inj₁ (inj₁ a)
    from′ (inj₂ (inj₁ b)) = inj₁ (inj₂ b)
    from′ (inj₂ (inj₂ c)) = inj₂ c
    from∘to′ : ∀ (x) → from′ (to′ x) ≡ x
    from∘to′ (inj₁ (inj₁ a)) = refl
    from∘to′ (inj₁ (inj₂ b)) = refl
    from∘to′ (inj₂ c) = refl
    to∘from′ : ∀ (x) → to′ (from′ x) ≡ x
    to∘from′ (inj₁ a) = refl
    to∘from′ (inj₂ (inj₁ b)) = refl
    to∘from′ (inj₂ (inj₂ c)) = refl

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

data ⊥ : Set where
  -- no clauses!

⊥-elim : ∀ {A : Set}
  → ⊥
    --
  → A
⊥-elim ()

uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h ()

⊥-count : ⊥ → ℕ
⊥-count ()

---------- practice ----------
⊥-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
⊥-identityˡ =
  record
  { to      = λ{ (inj₂ a) → a }
  ; from    = inj₂
  ; from∘to = λ{ (inj₂ a) → refl }
  ; to∘from = λ a → refl
  }

⊥-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
⊥-identityʳ {A} =
  ≃-begin
    (A ⊎ ⊥)
  ≃⟨ ⊎-comm ⟩
    (⊥ ⊎ A)
  ≃⟨ ⊥-identityˡ ⟩
    A
  ≃-∎

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

→-elim : ∀ {A B : Set}
  → (A → B)
  → A
    -------
  → B
→-elim L M = L M

η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ f = refl

→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
...          | aa     | aa      =   1
...          | aa     | bb      =   2
...          | aa     | cc      =   3
...          | bb     | aa      =   4
...          | bb     | bb      =   5
...          | bb     | cc      =   6
...          | cc     | aa      =   7
...          | cc     | bb      =   8
...          | cc     | cc      =   9

currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
  record
    { to      = λ f → λ{ ⟨ x , y ⟩ → f x y }
    ; from    = λ g x y → g ⟨ x , y ⟩
    ; from∘to = λ x → refl
    ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl } }
    }

→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
  record
    { to      = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
    ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
  record
    { to      = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
    ; from    = λ{ ⟨ g , h ⟩ → λ x → ⟨ g x , h x ⟩ }
    ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } }
    ; to∘from = λ{ ⟨ g , h ⟩ → refl }
    }

×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
  record
    { to      = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
                 ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
                 }
    ; from    = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
                 ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩
                 }
    ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl
                 ; ⟨ inj₂ y , z ⟩ → refl
                 }
    ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
                 ; (inj₂ ⟨ y , z ⟩) → refl
                 }
    }

⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× =
  record
    { to      = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
                 ; (inj₂ z)         → ⟨ inj₂ z , inj₂ z ⟩
                 }
    ; from    = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
                 ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
                 ; ⟨ inj₂ z , _      ⟩ → (inj₂ z)
                 }
    ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
                 ; (inj₂ z)         → refl
                 }
    }

---------- practice ----------
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-× ⟨ inj₁ a , c ⟩ = inj₁ a
⊎-weak-× ⟨ inj₂ b , c ⟩ = inj₂ ⟨ b , c ⟩
-- the corresponding distributive law is ×-distrib-⊎, ×-distrib-⊎ is more strong

⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎ (inj₁ ⟨ a , b ⟩) = ⟨ inj₁ a , inj₁ b ⟩
⊎×-implies-×⊎ (inj₂ ⟨ c , d ⟩) = ⟨ inj₂ c , inj₂ d ⟩
-- the converse doesn't hold. ⟨ inj₁ a , inj₂ d ⟩ could not build a
-- (A × B) ⊎ (C × D) value

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

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
-- This file tests that record constructors are used in error
-- messages, if possible.

-- Andreas, 2016-07-20 Repaired this long disfunctional test case.

module RecordConstructorsInErrorMessages where

record R : Set₁ where
  constructor con
  field
    {A}         : Set
    f           : A → A
    {B C} D {E} : Set
    g           : B → C → E

postulate
  A : Set
  r : R

data _≡_ {A : Set₁} (x : A) : A → Set where
  refl : x ≡ x

foo : r ≡ record
  { A = A
  ; f = λ x → x
  ; B = A
  ; C = A
  ; D = A
  ; g = λ x _ → x
  }
foo = refl

-- EXPECTED ERROR:
-- .R.A r != A of type Set
-- when checking that the expression refl has type
-- r ≡ con (λ x → x) A (λ x _ → x)