text:
------------------------------------------------------------------------------
-- Conat properties
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Data.Conat.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Conat
open import FOTC.Data.Nat

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Conat predicate is also a pre-fixed point of the functional NatF,
-- i.e.
--
-- NatF Conat ≤ Conat (see FOTC.Data.Conat.Type).

-- See Issue https://github.com/asr/apia/issues/81 .
Conat-inA : D → Set
Conat-inA n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
{-# ATP definition Conat-inA #-}

Conat-in : ∀ {n} →
           n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n') →
           Conat n
Conat-in h = Conat-coind Conat-inA h' h
  where
  postulate h' : ∀ {n} → Conat-inA n →
                 n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat-inA n')
  {-# ATP prove h' #-}

-- See Issue https://github.com/asr/apia/issues/81 .
0-ConatA : D → Set
0-ConatA n = n ≡ zero
{-# ATP definition 0-ConatA #-}

0-Conat : Conat zero
0-Conat = Conat-coind 0-ConatA h refl
  where
  postulate h : ∀ {n} → 0-ConatA n →
                n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ 0-ConatA n')
  {-# ATP prove h #-}

∞-Conat : Conat ∞
∞-Conat = Conat-coind A h refl
  where
  A : D → Set
  A n = n ≡ ∞
  {-# ATP definition A #-}

  postulate h : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')
  {-# ATP prove h #-}

N→Conat : ∀ {n} → N n → Conat n
N→Conat Nn = Conat-coind N h Nn
  where
  h : ∀ {m} → N m → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ N m')
  h nzero = prf
    where postulate prf : zero ≡ zero ∨ (∃[ m' ] zero ≡ succ₁ m' ∧ N m')
          {-# ATP prove prf #-}
  h (nsucc {m} Nm) = prf
    where postulate prf : succ₁ m ≡ zero ∨ (∃[ m' ] succ₁ m ≡ succ₁ m' ∧ N m')
          {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything

module Cubical.Algebra.Structures {a} (A : Type a) where

-- The file is divided into sections depending on the arities of the
-- components of the algebraic structure.

open import Cubical.Foundations.Prelude using (isSet; cong; _∙_)
open import Cubical.Foundations.HLevels using (hSet)

open import Cubical.Algebra.Base
open import Cubical.Algebra.Definitions
open import Cubical.Algebra.Properties
open import Cubical.Data.Sigma using (_,_; fst; snd)
open import Cubical.Data.Nat.Base renaming (zero to ℕ-zero; suc to ℕ-suc)
open import Cubical.Data.Int.Base
open import Cubical.Data.NatPlusOne.Base

open import Cubical.Relation.Nullary using (¬_)
open import Cubical.Relation.Binary.Reasoning.Equality

_NotEqualTo_ : A → Type a
_NotEqualTo_ z = Σ[ x ∈ A ] ¬ (x ≡ z)

------------------------------------------------------------------------
-- Algebra with 1 binary operation
------------------------------------------------------------------------

record IsMagma (_•_ : Op₂ A) : Type a where
  constructor ismagma
  field
    is-set : isSet A

  set : hSet a
  set = A , is-set

record IsSemigroup (_•_ : Op₂ A) : Type a where
  constructor issemigroup
  field
    isMagma : IsMagma _•_
    assoc   : Associative _•_

  open IsMagma isMagma public

  infixl 10 _^_
  _^_ : A → ℕ₊₁ → A
  x ^ one    = x
  x ^ (2+ n) = x • (x ^ 1+ n)

record IsBand (_•_ : Op₂ A) : Type a where
  constructor isband
  field
    isSemigroup : IsSemigroup _•_
    idem        : Idempotent _•_

  open IsSemigroup isSemigroup public

record IsCommutativeSemigroup (_•_ : Op₂ A) : Type a where
  constructor iscommsemigroup
  field
    isSemigroup : IsSemigroup _•_
    comm        : Commutative _•_

  open IsSemigroup isSemigroup public

record IsSemilattice (_•_ : Op₂ A) : Type a where
  constructor issemilattice
  field
    isBand : IsBand _•_
    comm   : Commutative _•_

  open IsBand isBand public

record IsSelectiveMagma (_•_ : Op₂ A) : Type a where
  constructor isselmagma
  field
    isMagma : IsMagma _•_
    sel     : Selective _•_

  open IsMagma isMagma public

------------------------------------------------------------------------
-- Algebra with 1 binary operation & 1 element
------------------------------------------------------------------------

record IsMonoid (_•_ : Op₂ A) (ε : A) : Type a where
  constructor ismonoid
  field
    isSemigroup : IsSemigroup _•_
    identity    : Identity ε _•_

  open IsSemigroup isSemigroup public hiding (_^_)

  identityˡ : LeftIdentity ε _•_
  identityˡ = fst identity

  identityʳ : RightIdentity ε _•_
  identityʳ = snd identity

  ε-uniqueʳ : ∀ {e} → RightIdentity e _•_ → ε ≡ e
  ε-uniqueʳ idʳ = id-unique′ identityˡ idʳ

  ε-uniqueˡ : ∀ {e} → LeftIdentity e _•_ → e ≡ ε
  ε-uniqueˡ idˡ = id-unique′ idˡ identityʳ

  infixl 10 _^_
  _^_ : A → ℕ → A
  _ ^ ℕ-zero    = ε
  x ^ (ℕ-suc n) = x • (x ^ n)

record IsCommutativeMonoid (_•_ : Op₂ A) (ε : A) : Type a where
  constructor iscommmonoid
  field
    isMonoid : IsMonoid _•_ ε
    comm     : Commutative _•_

  open IsMonoid isMonoid public

  isCommutativeSemigroup : IsCommutativeSemigroup _•_
  isCommutativeSemigroup = record
    { isSemigroup = isSemigroup
    ; comm        = comm
    }

record IsIdempotentCommutativeMonoid (_•_ : Op₂ A) (ε : A) : Type a where
  constructor isidemcommmonoid
  field
    isCommutativeMonoid : IsCommutativeMonoid _•_ ε
    idem                : Idempotent _•_

  open IsCommutativeMonoid isCommutativeMonoid public

-- Idempotent commutative monoids are also known as bounded lattices.
-- Note that the BoundedLattice necessarily uses the notation inherited
-- from monoids rather than lattices.

IsBoundedLattice = IsIdempotentCommutativeMonoid
pattern isboundedlattice = isidemcommmonoid

module IsBoundedLattice {_•_ : Op₂ A}
                        {ε : A}
                        (isIdemCommMonoid : IsIdempotentCommutativeMonoid _•_ ε) =
       IsIdempotentCommutativeMonoid isIdemCommMonoid

------------------------------------------------------------------------
-- Algebra with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------

record IsGroup (_•_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Type a where
  constructor isgroup
  field
    isMonoid  : IsMonoid _•_ ε
    inverse   : Inverse ε _⁻¹ _•_

  open IsMonoid isMonoid public hiding (_^_)

  infixl 10 _^_
  _^_ : A → ℤ → A
  x ^ pos ℕ-zero       = ε
  x ^ pos (ℕ-suc n)    = x • (x ^ pos n)
  x ^ negsuc ℕ-zero    = x ⁻¹
  x ^ negsuc (ℕ-suc n) = (x ⁻¹) • (x ^ negsuc n)

  -- Right division
  infixl 6 _/_
  _/_ : Op₂ A
  x / y = x • (y ⁻¹)

  -- Left division
  infixr 6 _/ˡ_
  _/ˡ_ : Op₂ A
  x /ˡ y = (x ⁻¹) • y

  inverseˡ : LeftInverse ε _⁻¹ _•_
  inverseˡ = fst inverse

  inverseʳ : RightInverse ε _⁻¹ _•_
  inverseʳ = snd inverse

  inv-uniqueʳ : ∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹)
  inv-uniqueʳ = assoc+id+invʳ⇒invʳ-unique assoc identity inverseʳ

  inv-uniqueˡ : ∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹)
  inv-uniqueˡ = assoc+id+invˡ⇒invˡ-unique assoc identity inverseˡ

  cancelˡ : LeftCancellative _•_
  cancelˡ = assoc+idˡ+invˡ⇒cancelˡ assoc identityˡ inverseˡ

  cancelʳ : RightCancellative _•_
  cancelʳ = assoc+idʳ+invʳ⇒cancelʳ assoc identityʳ inverseʳ

record IsAbelianGroup (_+_ : Op₂ A) (ε : A) (-_ : Op₁ A) : Type a where
  constructor isabgroup
  field
    isGroup : IsGroup _+_ ε -_
    comm    : Commutative _+_

  open IsGroup isGroup public hiding (_/ˡ_) renaming (_/_ to _-_; _^_ to _*_)

  isCommutativeMonoid : IsCommutativeMonoid _+_ ε
  isCommutativeMonoid = record
    { isMonoid = isMonoid
    ; comm     = comm
    }

  open IsCommutativeMonoid isCommutativeMonoid public
    using (isCommutativeSemigroup)

------------------------------------------------------------------------
-- Algebra with 2 binary operations
------------------------------------------------------------------------

-- Note that `IsLattice` is not defined in terms of `IsSemilattice`
-- because the idempotence laws of ⋀ and ⋁ can be derived from the
-- absorption laws, which makes the corresponding "idem" fields
-- redundant.  The derived idempotence laws are stated and proved in
-- `Algebra.Properties.Lattice` along with the fact that every lattice
-- consists of two semilattices.

record IsLattice (_⋀_ _⋁_ : Op₂ A) : Type a where
  constructor islattice
  field
    ⋀-comm        : Commutative _⋀_
    ⋀-assoc       : Associative _⋀_
    ⋁-comm        : Commutative _⋁_
    ⋁-assoc       : Associative _⋁_
    absorptive    : Absorptive _⋀_ _⋁_

  ⋀-absorbs-⋁ : _⋀_ Absorbs _⋁_
  ⋀-absorbs-⋁ = fst absorptive

  ⋁-absorbs-⋀ : _⋁_ Absorbs _⋀_
  ⋁-absorbs-⋀ = snd absorptive

record IsDistributiveLattice (_⋀_ _⋁_ : Op₂ A) : Type a where
  constructor isdistrlattice
  field
    isLattice    : IsLattice _⋀_ _⋁_
    ⋀-distribʳ-⋁ : _⋀_ DistributesOverʳ _⋁_

  open IsLattice isLattice public

------------------------------------------------------------------------
-- Algebra with 2 binary operations & 1 element
------------------------------------------------------------------------

record IsNearSemiring (_+_ _*_ : Op₂ A) (0# : A) : Type a where
  constructor isnearsemiring
  field
    +-isMonoid    : IsMonoid _+_ 0#
    *-isSemigroup : IsSemigroup _*_
    distribˡ      : _*_ DistributesOverˡ _+_
    zeroˡ         : LeftZero 0# _*_

  open IsMonoid +-isMonoid public
    renaming
    ( assoc       to +-assoc
    ; identity    to +-identity
    ; identityˡ   to +-identityˡ
    ; identityʳ   to +-identityʳ
    ; ε-uniqueˡ   to 0#-uniqueˡ
    ; ε-uniqueʳ   to 0#-uniqueʳ
    ; isMagma     to +-isMagma
    ; isSemigroup to +-isSemigroup
    ; _^_         to _**_
    )

  open IsSemigroup *-isSemigroup public
    using (_^_)
    renaming
    ( assoc    to *-assoc
    ; isMagma  to *-isMagma
    )

record IsSemiringWithoutOne (_+_ _*_ : Op₂ A) (0# : A) : Type a where
  constructor issemiringwo1
  field
    +-isCommutativeMonoid : IsCommutativeMonoid _+_ 0#
    *-isSemigroup         : IsSemigroup _*_
    distrib               : _*_ DistributesOver _+_
    zero                  : Zero 0# _*_

  open IsCommutativeMonoid +-isCommutativeMonoid public
    using ()
    renaming
    ( comm                   to +-comm
    ; isMonoid               to +-isMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    )

  zeroˡ : LeftZero 0# _*_
  zeroˡ = fst zero

  zeroʳ : RightZero 0# _*_
  zeroʳ = snd zero

  distribˡ : _*_ DistributesOverˡ _+_
  distribˡ = fst distrib

  distribʳ : _*_ DistributesOverʳ _+_
  distribʳ = snd distrib

  isNearSemiring : IsNearSemiring _+_ _*_ 0#
  isNearSemiring = record
    { +-isMonoid    = +-isMonoid
    ; *-isSemigroup = *-isSemigroup
    ; distribˡ      = distribˡ
    ; zeroˡ         = zeroˡ
    }

  open IsNearSemiring isNearSemiring public
    hiding (+-isMonoid; zeroˡ; *-isSemigroup; distribˡ)

record IsCommutativeSemiringWithoutOne (_+_ _*_ : Op₂ A) (0# : A) : Type a where
  constructor iscommsemiringwo1
  field
    isSemiringWithoutOne : IsSemiringWithoutOne _+_ _*_ 0#
    *-comm               : Commutative _*_

  open IsSemiringWithoutOne isSemiringWithoutOne public

------------------------------------------------------------------------
-- Algebra with 2 binary operations & 2 elements
------------------------------------------------------------------------

record IsSemiringWithoutAnnihilatingZero (_+_ _*_ : Op₂ A)
                                         (0# 1# : A) : Type a where
  constructor issemiringwoa0
  field
    -- Note that these Algebra do have an additive unit, but this
    -- unit does not necessarily annihilate multiplication.
    +-isCommutativeMonoid : IsCommutativeMonoid _+_ 0#
    *-isMonoid            : IsMonoid _*_ 1#
    distrib               : _*_ DistributesOver _+_

  distribˡ : _*_ DistributesOverˡ _+_
  distribˡ = fst distrib

  distribʳ : _*_ DistributesOverʳ _+_
  distribʳ = snd distrib

  open IsCommutativeMonoid +-isCommutativeMonoid public
    renaming
    ( assoc                  to +-assoc
    ; identity               to +-identity
    ; identityˡ              to +-identityˡ
    ; identityʳ              to +-identityʳ
    ; ε-uniqueˡ              to 0#-uniqueˡ
    ; ε-uniqueʳ              to 0#-uniqueʳ
    ; comm                   to +-comm
    ; isMagma                to +-isMagma
    ; isSemigroup            to +-isSemigroup
    ; isMonoid               to +-isMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    ; _^_                    to _**_
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; ε-uniqueˡ   to 1#-uniqueˡ
    ; ε-uniqueʳ   to 1#-uniqueʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

record IsSemiring (_+_ _*_ : Op₂ A) (0# 1# : A) : Type a where
  constructor issemiring
  field
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero _+_ _*_ 0# 1#
    zero : Zero 0# _*_

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  isSemiringWithoutOne : IsSemiringWithoutOne _+_ _*_ 0#
  isSemiringWithoutOne = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isSemigroup         = *-isSemigroup
    ; distrib               = distrib
    ; zero                  = zero
    }

  open IsSemiringWithoutOne isSemiringWithoutOne public
    using
    ( isNearSemiring
    ; zeroˡ
    ; zeroʳ
    )

record IsCommutativeSemiring (_+_ _*_ : Op₂ A) (0# 1# : A) : Type a where
  constructor iscommsemiring
  field
    isSemiring : IsSemiring _+_ _*_ 0# 1#
    *-comm     : Commutative _*_

  open IsSemiring isSemiring public

  isCommutativeSemiringWithoutOne :
    IsCommutativeSemiringWithoutOne _+_ _*_ 0#
  isCommutativeSemiringWithoutOne = record
    { isSemiringWithoutOne = isSemiringWithoutOne
    ; *-comm = *-comm
    }

  *-isCommutativeSemigroup : IsCommutativeSemigroup _*_
  *-isCommutativeSemigroup = record
    { isSemigroup = *-isSemigroup
    ; comm        = *-comm
    }

  *-isCommutativeMonoid : IsCommutativeMonoid _*_ 1#
  *-isCommutativeMonoid = record
    { isMonoid = *-isMonoid
    ; comm     = *-comm
    }

------------------------------------------------------------------------
-- Algebra with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

record IsRing (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Type a where
  constructor isring
  field
    +-isAbelianGroup : IsAbelianGroup _+_ 0# -_
    *-isMonoid       : IsMonoid _*_ 1#
    distrib          : _*_ DistributesOver _+_

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc                  to +-assoc
    ; identity               to +-identity
    ; identityˡ              to +-identityˡ
    ; identityʳ              to +-identityʳ
    ; ε-uniqueˡ              to 0#-uniqueˡ
    ; ε-uniqueʳ              to 0#-uniqueʳ
    ; inverse                to +-inverse
    ; inverseˡ               to +-inverseˡ
    ; inverseʳ               to +-inverseʳ
    ; inv-uniqueˡ            to neg-uniqueˡ
    ; inv-uniqueʳ            to neg-uniqueʳ
    ; cancelˡ                to +-cancelˡ
    ; cancelʳ                to +-cancelʳ
    ; comm                   to +-comm
    ; isMagma                to +-isMagma
    ; isSemigroup            to +-isSemigroup
    ; isMonoid               to +-isMonoid
    ; isCommutativeMonoid    to +-isCommutativeMonoid
    ; isCommutativeSemigroup to +-isCommutativeSemigroup
    ; isGroup                to +-isGroup
    ; _*_                    to _**_
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; ε-uniqueˡ   to 1#-uniqueˡ
    ; ε-uniqueʳ   to 1#-uniqueʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

  distribˡ : _*_ DistributesOverˡ _+_
  distribˡ = fst distrib

  distribʳ : _*_ DistributesOverʳ _+_
  distribʳ = snd distrib

  zeroˡ : LeftZero 0# _*_
  zeroˡ = assoc+distribʳ+idʳ+invʳ⇒zeˡ {_+_ = _+_} {_*_ = _*_} { -_} +-assoc distribʳ +-identityʳ +-inverseʳ

  zeroʳ : RightZero 0# _*_
  zeroʳ = assoc+distribˡ+idʳ+invʳ⇒zeʳ {_+_ = _+_} {_*_ = _*_} { -_} +-assoc distribˡ +-identityʳ +-inverseʳ

  zero : Zero 0# _*_
  zero = zeroˡ , zeroʳ

  isSemiringWithoutAnnihilatingZero
    : IsSemiringWithoutAnnihilatingZero _+_ _*_ 0# 1#
  isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isMonoid            = *-isMonoid
    ; distrib               = distrib
    }

  isSemiring : IsSemiring _+_ _*_ 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    ; zero = zero
    }

  open IsSemiring isSemiring public
    using (isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Type a where
  constructor iscommring
  field
    isRing : IsRing _+_ _*_ -_ 0# 1#
    *-comm : Commutative _*_

  open IsRing isRing public

  *-isCommutativeMonoid : IsCommutativeMonoid _*_ 1#
  *-isCommutativeMonoid =  record
    { isMonoid = *-isMonoid
    ; comm     = *-comm
    }

  isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0# 1#
  isCommutativeSemiring = record
    { isSemiring = isSemiring
    ; *-comm = *-comm
    }

  open IsCommutativeSemiring isCommutativeSemiring public
    using ( isCommutativeSemiringWithoutOne )

record IsIntegralDomain {ℓ} (Cancellable : A → Type ℓ) (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Type (ℓ-max a ℓ) where
  constructor isintegraldomain

  Cancellables : Type (ℓ-max a ℓ)
  Cancellables = Σ A Cancellable

  field
    isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
    *-cancelˡ         : ∀ (x : Cancellables) {y z} → (x .fst) * y ≡ (x .fst) * z → y ≡ z

  open IsCommutativeRing isCommutativeRing public

  *-cancelʳ : ∀ {x y} (z : Cancellables) → x * (z .fst) ≡ y * (z .fst) → x ≡ y
  *-cancelʳ {x} {y} zᵖ@(z , _) eq = *-cancelˡ zᵖ (
    z * x ≡⟨ *-comm z x ⟩
    x * z ≡⟨ eq ⟩
    y * z ≡⟨ *-comm y z ⟩
    z * y ∎)

record IsBooleanAlgebra (_⋀_ _⋁_ : Op₂ A) (¬_ : Op₁ A) (⊤ ⊥ : A) : Type a where
  constructor isbooleanalgebra
  field
    isDistributiveLattice : IsDistributiveLattice _⋀_ _⋁_
    ⋀-identityʳ           : RightIdentity ⊤ _⋀_
    ⋁-identityʳ           : RightIdentity ⊥ _⋁_
    ⋀-complementʳ         : RightInverse ⊥ ¬_ _⋀_
    ⋁-complementʳ         : RightInverse ⊤ ¬_ _⋁_

  open IsDistributiveLattice isDistributiveLattice public

  ⋀-identityˡ : LeftIdentity ⊤ _⋀_
  ⋀-identityˡ x = ⋀-comm _ _ ∙ ⋀-identityʳ x

  ⋀-identity : Identity ⊤ _⋀_
  ⋀-identity = ⋀-identityˡ , ⋀-identityʳ

  ⋁-identityˡ : LeftIdentity ⊥ _⋁_
  ⋁-identityˡ x = ⋁-comm _ _ ∙ ⋁-identityʳ x

  ⋁-identity : Identity ⊥ _⋁_
  ⋁-identity = ⋁-identityˡ , ⋁-identityʳ

  ⋀-complementˡ : LeftInverse ⊥ ¬_ _⋀_
  ⋀-complementˡ = comm+invʳ⇒invˡ ⋀-comm ⋀-complementʳ

  ⋀-complement : Inverse ⊥ ¬_ _⋀_
  ⋀-complement = ⋀-complementˡ , ⋀-complementʳ

  ⋁-complementˡ : LeftInverse ⊤ ¬_ _⋁_
  ⋁-complementˡ = comm+invʳ⇒invˡ ⋁-comm ⋁-complementʳ

  ⋁-complement : Inverse ⊤ ¬_ _⋁_
  ⋁-complement = ⋁-complementˡ , ⋁-complementʳ

------------------------------------------------------------------------
-- Algebra with 2 binary operations, 2 unary operations & 2 elements
------------------------------------------------------------------------

-- The standard definition of division rings excludes the zero ring, but such a restriction is rarely important
record IsDivisionRing {ℓ} (Invertible : A → Type ℓ) (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (_⁻¹ : Σ A Invertible → A) (0# 1# : A) : Type (ℓ-max a ℓ) where
  constructor isdivring

  Invertibles : Type (ℓ-max a ℓ)
  Invertibles = Σ A Invertible

  field
    isRing   : IsRing _+_ _*_ -_ 0# 1#
    *-inverseˡ : (x : Invertibles) → (x ⁻¹) * (x .fst) ≡ 1#
    *-inverseʳ : (x : Invertibles) → (x .fst) * (x ⁻¹) ≡ 1#

  open IsRing isRing public

  infixl 6 _/_
  _/_ : A → Invertibles → A
  x / y = x * (y ⁻¹)

  infixr 6 _/ˡ_
  _/ˡ_ : Invertibles → A → A
  x /ˡ y = (x ⁻¹) * y

  *-cancelˡ : ∀ (x : Invertibles) {y z} → (x .fst) * y ≡ (x .fst) * z → y ≡ z
  *-cancelˡ xᵖ@(x , _) {y} {z} eq =
    y                 ≡˘⟨ *-identityˡ y ⟩
    1# * y            ≡˘⟨ cong (_* y) (*-inverseˡ xᵖ) ⟩
    ((xᵖ ⁻¹) * x) * y ≡⟨ *-assoc (xᵖ ⁻¹) x y ⟩
    (xᵖ ⁻¹) * (x * y) ≡⟨ cong ((xᵖ ⁻¹) *_) eq ⟩
    (xᵖ ⁻¹) * (x * z) ≡˘⟨ *-assoc (xᵖ ⁻¹) x z ⟩
    ((xᵖ ⁻¹) * x) * z ≡⟨ cong (_* z) (*-inverseˡ xᵖ) ⟩
    1# * z            ≡⟨ *-identityˡ z ⟩
    z                 ∎

  *-cancelʳ : ∀ {x y} (z : Invertibles) → x * (z .fst) ≡ y * (z .fst) → x ≡ y
  *-cancelʳ {x} {y} zᵖ@(z , _) eq =
    x                 ≡˘⟨ *-identityʳ x ⟩
    x * 1#            ≡˘⟨ cong (x *_) (*-inverseʳ zᵖ) ⟩
    x * (z * (zᵖ ⁻¹)) ≡˘⟨ *-assoc x z (zᵖ ⁻¹) ⟩
    (x * z) * (zᵖ ⁻¹) ≡⟨ cong (_* (zᵖ ⁻¹)) eq ⟩
    (y * z) * (zᵖ ⁻¹) ≡⟨ *-assoc y z (zᵖ ⁻¹) ⟩
    y * (z * (zᵖ ⁻¹)) ≡⟨ cong (y *_) (*-inverseʳ zᵖ) ⟩
    y * 1#            ≡⟨ *-identityʳ y ⟩
    y                 ∎

record IsField {ℓ} (Invertible : A → Type ℓ) (_+_ _*_ : Op₂ A) (-_ : Op₁ A) (_⁻¹ : Σ A Invertible → A) (0# 1# : A) : Type (ℓ-max a ℓ) where
  constructor isfield
  field
    isDivisionRing : IsDivisionRing Invertible _+_ _*_ -_ _⁻¹ 0# 1#
    *-comm         : Commutative _*_

  open IsDivisionRing isDivisionRing public hiding (_/ˡ_)

  isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
  isCommutativeRing = record
    { isRing = isRing
    ; *-comm = *-comm
    }

  isIntegralDomain : IsIntegralDomain Invertible _+_ _*_ -_ 0# 1#
  isIntegralDomain = record
    { isCommutativeRing = isCommutativeRing
    ; *-cancelˡ         = *-cancelˡ
    }

  open IsIntegralDomain isIntegralDomain public
    using (*-isCommutativeMonoid; isCommutativeSemiring; isCommutativeSemiringWithoutOne)

ext: agda


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

open import BBHeap _≤_
open import BBHeap.Order _≤_ renaming (Acc to Accₕ ; acc to accₕ)
open import Data.Nat
open import Induction.Nat
open import Induction.WellFounded

ii-acc : ∀ {b} {h} → Acc _<′_ (# {b} h) → Accₕ h
ii-acc (acc rs) = accₕ (λ h' #h'<′#h → ii-acc (rs (# h') #h'<′#h))

≺-wf : ∀ {b} h → Accₕ {b} h
≺-wf = λ h → ii-acc (<-well-founded (# h))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
import Definition.Typed.Weakening as T
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Introductions.Empty
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Product
open import Tools.Unit
open import Tools.Empty
open import Tools.Nat

import Tools.PropositionalEquality as PE

-- Empty elimination closure reduction (requires reducible terms and equality).
Emptyrec-subst* : ∀ {Γ C n n′ l}
              → Γ ⊢ C
              → Γ ⊢ n ⇒* n′ ∷ Empty
              → ([Empty] : Γ ⊩⟨ l ⟩ Empty)
              → Γ ⊩⟨ l ⟩ n′ ∷ Empty / [Empty]
              → Γ ⊢ Emptyrec C n ⇒* Emptyrec C n′ ∷ C
Emptyrec-subst* C (id x) [Empty] [n′] = id (Emptyrecⱼ C x)
Emptyrec-subst* C (x ⇨ n⇒n′) [Empty] [n′] =
  let q , w = redSubst*Term n⇒n′ [Empty] [n′]
      a , s = redSubstTerm x [Empty] q
  in  Emptyrec-subst C x ⇨ conv* (Emptyrec-subst* C n⇒n′ [Empty] [n′]) (refl C)

-- Reducibility of empty elimination under a valid substitution.
EmptyrecTerm : ∀ {F n Γ Δ σ l}
             ([Γ]  : ⊩ᵛ Γ)
             ([F]  : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             (⊢Δ   : ⊢ Δ)
             ([σ]  : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
             ([σn] : Δ ⊩⟨ l ⟩ n ∷ Empty / Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)))
           → Δ ⊩⟨ l ⟩ Emptyrec (subst σ F) n
               ∷ subst σ F
               / proj₁ ([F] ⊢Δ [σ])
EmptyrecTerm {F} {n} {Γ} {Δ} {σ} {l} [Γ] [F] ⊢Δ [σ]
           (Emptyₜ m d n≡n (ne (neNfₜ neM ⊢m m≡m))) =
  let [Empty] = Emptyᵛ {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σm] = neuTerm [σEmpty] neM ⊢m m≡m
      [σF] = proj₁ ([F] ⊢Δ [σ])
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      EmptyrecM = neuTerm [σF] (Emptyrecₙ neM) (Emptyrecⱼ ⊢F ⊢m)
                        (~-Emptyrec ⊢F≡F m≡m)
      reduction = Emptyrec-subst* ⊢F (redₜ d) [σEmpty] [σm]
  in proj₁ (redSubst*Term reduction [σF] EmptyrecM)

-- Reducibility of empty elimination congruence under a valid substitution equality.
Emptyrec-congTerm : ∀ {F F′ n m Γ Δ σ σ′ l}
                  ([Γ]      : ⊩ᵛ Γ)
                  ([F]      : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
                  ([F′]     : Γ ⊩ᵛ⟨ l ⟩ F′ / [Γ])
                  ([F≡F′]   : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] / [F])
                  (⊢Δ       : ⊢ Δ)
                  ([σ]      : Δ ⊩ˢ σ  ∷ Γ / [Γ] / ⊢Δ)
                  ([σ′]     : Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ)
                  ([σ≡σ′]   : Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
                  ([σn]     : Δ ⊩⟨ l ⟩ n ∷ Empty / Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)))
                  ([σm]     : Δ ⊩⟨ l ⟩ m ∷ Empty / Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)))
                  ([σn≡σm]  : Δ ⊩⟨ l ⟩ n ≡ m ∷ Empty / Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)))
                → Δ ⊩⟨ l ⟩ Emptyrec (subst σ F) n
                    ≡ Emptyrec (subst σ′ F′) m
                    ∷ subst σ F
                    / proj₁ ([F] ⊢Δ [σ])
Emptyrec-congTerm {F} {F′} {n} {m} {Γ} {Δ} {σ} {σ′} {l}
                [Γ] [F] [F′] [F≡F′]
                ⊢Δ [σ] [σ′] [σ≡σ′]
                (Emptyₜ n′ d n≡n (ne (neNfₜ neN′ ⊢n′ n≡n₁)))
                (Emptyₜ m′ d′ m≡m (ne (neNfₜ neM′ ⊢m′ m≡m₁)))
                (Emptyₜ₌ n″ m″ d₁ d₁′ t≡u (ne (neNfₜ₌ x₂ x₃ prop₂))) =
  let n″≡n′ = whrDet*Term (redₜ d₁ , ne x₂) (redₜ d , ne neN′)
      m″≡m′ = whrDet*Term (redₜ d₁′ , ne x₃) (redₜ d′ , ne neM′)
      [Empty] = Emptyᵛ {l = l} [Γ]
      [σEmpty] = proj₁ ([Empty] ⊢Δ [σ])
      [σ′Empty] = proj₁ ([Empty] ⊢Δ [σ′])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [σ′F] = proj₁ ([F] ⊢Δ [σ′])
      [σ′F′] = proj₁ ([F′] ⊢Δ [σ′])
      [σn′] = neuTerm [σEmpty] neN′ ⊢n′ n≡n₁
      [σ′m′] = neuTerm [σ′Empty] neM′ ⊢m′ m≡m₁
      ⊢F = escape [σF]
      ⊢F≡F = escapeEq [σF] (reflEq [σF])
      ⊢F′ = escape [σ′F′]
      ⊢F′≡F′ = escapeEq [σ′F′] (reflEq [σ′F′])
      ⊢σF≡σ′F = escapeEq [σF] (proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′])
      ⊢σ′F≡σ′F′ = escapeEq [σ′F] ([F≡F′] ⊢Δ [σ′])
      ⊢F≡F′ = ≅-trans ⊢σF≡σ′F ⊢σ′F≡σ′F′
      [σF≡σ′F] = proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]
      [σ′F≡σ′F′] = [F≡F′] ⊢Δ [σ′]
      [σF≡σ′F′] = transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′]
      EmptyrecN = neuTerm [σF] (Emptyrecₙ neN′) (Emptyrecⱼ ⊢F ⊢n′)
                        (~-Emptyrec ⊢F≡F n≡n₁)
      EmptyrecM = neuTerm [σ′F′] (Emptyrecₙ neM′) (Emptyrecⱼ ⊢F′ ⊢m′)
                        (~-Emptyrec ⊢F′≡F′ m≡m₁)
      EmptyrecN≡M =
          (neuEqTerm [σF] (Emptyrecₙ neN′) (Emptyrecₙ neM′)
                     (Emptyrecⱼ ⊢F ⊢n′)
                     (conv (Emptyrecⱼ ⊢F′ ⊢m′)
                            (sym (≅-eq (escapeEq [σF]
                              (transEq [σF] [σ′F] [σ′F′] [σF≡σ′F] [σ′F≡σ′F′])))))
                     (~-Emptyrec ⊢F≡F′
                               (PE.subst₂ (λ x y → _ ⊢ x ~ y ∷ _)
                                          n″≡n′ m″≡m′ prop₂)))
      reduction₁ = Emptyrec-subst* ⊢F (redₜ d) [σEmpty] [σn′]
      reduction₂ = Emptyrec-subst* ⊢F′ (redₜ d′) [σ′Empty] [σ′m′]
      eq₁ = proj₂ (redSubst*Term reduction₁ [σF] EmptyrecN)
      eq₂ = proj₂ (redSubst*Term reduction₂ [σ′F′] EmptyrecM)
  in transEqTerm [σF] eq₁
                 (transEqTerm [σF] EmptyrecN≡M
                              (convEqTerm₂ [σF] [σ′F′] [σF≡σ′F′]
                                           (symEqTerm [σ′F′] eq₂)))

-- Validity of empty elimination.
Emptyrecᵛ : ∀ {F n Γ l} ([Γ] : ⊩ᵛ Γ)
          ([Empty]  : Γ ⊩ᵛ⟨ l ⟩ Empty / [Γ])
          ([F]  : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
        → ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ Empty / [Γ] / [Empty])
        → Γ ⊩ᵛ⟨ l ⟩ Emptyrec F n ∷ F / [Γ] / [F]
Emptyrecᵛ {F} {n} {l = l} [Γ] [Empty] [F] [n]
        {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [σn] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))) (proj₁ ([n] ⊢Δ [σ]))
  in EmptyrecTerm {F = F} [Γ] [F] ⊢Δ [σ] [σn]
    , λ {σ'} [σ′] [σ≡σ′] →
      let [σ′n] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ′]))
                                  (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))) (proj₁ ([n] ⊢Δ [σ′]))
          [σn≡σ′n] = irrelevanceEqTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                                       (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ)))
                                       (proj₂ ([n] ⊢Δ [σ]) [σ′] [σ≡σ′])
          congTerm = Emptyrec-congTerm {F = F} {F′ = F} [Γ] [F] [F] (reflᵛ {F} {l = l} [Γ] [F])
                                       ⊢Δ [σ] [σ′] [σ≡σ′] [σn] [σ′n] [σn≡σ′n]
      in congTerm

-- Validity of empty elimination congruence.
Emptyrec-congᵛ : ∀ {F F′ n n′ Γ l} ([Γ] : ⊩ᵛ Γ)
          ([Empty]  : Γ ⊩ᵛ⟨ l ⟩ Empty / [Γ])
          ([F]  : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
          ([F′]  : Γ ⊩ᵛ⟨ l ⟩ F′ / [Γ])
          ([F≡F′]  : Γ ⊩ᵛ⟨ l ⟩ F ≡ F′ / [Γ] / [F])
          ([n] : Γ ⊩ᵛ⟨ l ⟩ n ∷ Empty / [Γ] / [Empty])
          ([n′] : Γ ⊩ᵛ⟨ l ⟩ n′ ∷ Empty / [Γ] / [Empty])
          ([n≡n′] : Γ ⊩ᵛ⟨ l ⟩ n ≡ n′ ∷ Empty / [Γ] / [Empty])
        → Γ ⊩ᵛ⟨ l ⟩ Emptyrec F n ≡ Emptyrec F′ n′ ∷ F / [Γ] / [F]
Emptyrec-congᵛ {F} {F′} {n} {n′} {l = l}
             [Γ] [Empty] [F] [F′] [F≡F′]
             [n] [n′] [n≡n′] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [σn] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))) (proj₁ ([n] ⊢Δ [σ]))
      [σn′] = irrelevanceTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                             (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))) (proj₁ ([n′] ⊢Δ [σ]))
      [σn≡σn′] = irrelevanceEqTerm {l′ = l} (proj₁ ([Empty] ⊢Δ [σ]))
                                   (Emptyᵣ (idRed:*: (Emptyⱼ ⊢Δ))) ([n≡n′] ⊢Δ [σ])
      congTerm = Emptyrec-congTerm {F} {F′} [Γ] [F] [F′] [F≡F′]
                                   ⊢Δ [σ] [σ] (reflSubst [Γ] ⊢Δ [σ]) [σn] [σn′] [σn≡σn′]
  in congTerm


text:
module Numeral.Finite.Bound where

open import Lang.Instance
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs

-- For an arbitrary number `n`, `bound-[≤] n` is the same number as `n` semantically but with a different boundary on the type.
-- Example: bound-[≤] p (3: 𝕟(10)) = 3: 𝕟(20) where p: (10 ≤ 20)
bound-[≤] : ∀{a b} → (a ≤ b) → (𝕟(a) → 𝕟(b))
bound-[≤] {𝐒 a} {𝐒 b} _        𝟎     = 𝟎
bound-[≤] {𝐒 a} {𝐒 b} (succ p) (𝐒 n) = 𝐒(bound-[≤] p n)

bound-𝐒 : ∀{n} → 𝕟(n) → 𝕟(ℕ.𝐒(n))
bound-𝐒 = bound-[≤] [≤]-of-[𝐒]

bound-exact : ∀{a b} → (i : 𝕟(a)) → (𝕟-to-ℕ i < b) → 𝕟(b)
bound-exact {𝐒 a} {𝐒 b} 𝟎     (succ _) = 𝟎
bound-exact {𝐒 a} {𝐒 b} (𝐒 i) (succ p) = 𝐒(bound-exact i p)

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:
module Avionics.Real where

open import Algebra.Definitions using (LeftIdentity; RightIdentity; Commutative)
open import Data.Bool using (Bool; _∧_)
open import Data.Float using (Float)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ)
open import Level using (0ℓ; _⊔_) renaming (suc to lsuc)
open import Relation.Binary using (Decidable; _Preserves_⟶_)
open import Relation.Binary.Definitions using (Transitive; Trans)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (False; ⌊_⌋)
open import Relation.Unary using (Pred; _∈_)

infix  4 _<_ _≤_ _<ᵇ_ _≤ᵇ_
infixl 6 _+_ _-_
infixl 7 _*_

infix 4 _≟_

postulate
  ℝ : Set
  -- TODO: `fromFloat` should return `Maybe ℝ`
  fromFloat : Float → ℝ
  toFloat : ℝ → Float
  fromℕ : ℕ → ℝ

  _+_ _*_ _^_ : ℝ → ℝ → ℝ
  -_ abs _^2 : ℝ → ℝ
  e π 0ℝ 1ℝ -1/2 1/2 2ℝ : ℝ

  -- This was inspired on how the standard library handles things.
  -- See: https://plfa.github.io/Decidable/
  _<_ _≤_ : ℝ → ℝ → Set

  _≟_ : Decidable {A = ℝ} _≡_
  _≤?_ : (m n : ℝ) → Dec (m ≤ n)
  _<?_ : (m n : ℝ) → Dec (m < n)

_<ᵇ_ _≤ᵇ_ _≡ᵇ_ : ℝ → ℝ → Bool
p <ᵇ q = ⌊ p <? q ⌋
p ≤ᵇ q = ⌊ p ≤? q ⌋
p ≡ᵇ q = ⌊ p ≟ q ⌋

_≢0 : ℝ → Set
p ≢0 = False (p ≟ 0ℝ)

Subset : Set → Set _
Subset A = Pred A 0ℓ

-- Dangerous definitions, but necessary!
postulate
  ⟨0,∞⟩ [0,∞⟩ [0,1] : Subset ℝ

  1/_ : (p : ℝ) → ℝ
  √_ : (x : ℝ) → ℝ

_÷_ : (p q : ℝ) → ℝ
(p ÷ q) = p * (1/ q)

-- Dangerous definitions, but necessary!
postulate
  m÷n<o≡m<o*n : ∀ m n o → (m ÷ n <ᵇ o) ≡ (m <ᵇ o * n)
  m<o÷n≡m*n<o : ∀ m n o → (m <ᵇ o ÷ n) ≡ (m * n <ᵇ o)

_-_ : ℝ → ℝ → ℝ
p - q = p + (- q)

postulate
  double-neg : ∀ (x y : ℝ) → y - (y - x) ≡ x
  neg-involutive : ∀ x → -(- x) ≡ x
  neg-distrib-+ : ∀ m n → - (m + n) ≡ (- m) + (- n)
  neg-def : ∀ m → 0ℝ - m ≡ - m
  m-m≡0 : ∀ m → m - m ≡ 0ℝ
  neg-distribˡ-* : ∀ x y → - (x * y) ≡ (- x) * y
  √x^2≡absx : ∀ x → √ (x ^2) ≡ abs x

  >0→≢0 : ∀ {x : ℝ} → x ∈ ⟨0,∞⟩ → x ≢0
  >0→≥0 : ∀ {x : ℝ} → x ∈ ⟨0,∞⟩ → x ∈ [0,∞⟩
  >0*>0→>0 : ∀ {p q : ℝ} → p ∈ ⟨0,∞⟩ → q ∈ ⟨0,∞⟩ → (p * q) ∈ ⟨0,∞⟩
  ≢0*≢0→≢0 : ∀ {p q : ℝ} → p ≢0 → q ≢0 → (p * q) ≢0

  2>0 : 2ℝ ∈ ⟨0,∞⟩
  π>0 : π ∈ ⟨0,∞⟩

  e^x>0 : (x : ℝ) → (e ^ x) ∈ ⟨0,∞⟩
  x*x≡x^2 : ∀ x → x * x ≡ x ^2
  x^2*y^2≡⟨xy⟩^2 : ∀ x y → (x ^2) * (y ^2) ≡ (x * y)^2
  1/x^2≡⟨1/x⟩^2 : ∀ x → 1/ (x ^2) ≡ (1/ x)^2
  --√q≥0 : (q : ℝ) → (0≤q : q ∈ [0,∞⟩) → (√ q) {0≤q} ∈ [0,∞⟩
  --q>0→√q>0 : {q : ℝ} → (0<q : q ∈ ⟨0,∞⟩) → (√ q) {>0→≥0 0<q} ∈ ⟨0,∞⟩

  0≤→[0,∞⟩ : {n : ℝ} → 0ℝ ≤ n → n ∈ [0,∞⟩
  0<→⟨0,∞⟩ : {n : ℝ} → 0ℝ < n → n ∈ ⟨0,∞⟩
  [0,∞⟩→0≤ : {n : ℝ} → n ∈ [0,∞⟩ → 0ℝ ≤ n
  ⟨0,∞⟩→0< : {n : ℝ} → n ∈ ⟨0,∞⟩ → 0ℝ < n

  m≤n→m-p≤n-p : {m n p : ℝ} → m ≤ n → m - p ≤ n - p
  m<n→m-p<n-p : {m n p : ℝ} → m < n → m - p < n - p

  -- trans-≤ reduces to: {i j k : ℝ} → i ≤ j → j ≤ k → i ≤ k
  trans-≤ : Transitive _≤_
  <-transˡ : Trans _<_ _≤_ _<_

  --+-identityˡ : LeftIdentity 0ℝ _+_
  --+-identityʳ : RightIdentity 0ℝ _+_
  +-identityˡ : ∀ x → 0ℝ + x ≡ x
  +-identityʳ : ∀ x → x + 0ℝ ≡ x
  --+-comm : Commutative _+_
  +-comm : ∀ m n → m + n ≡ n + m
  --+-assoc : Associative _+_
  +-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o

  *-comm : ∀ m n → m * n ≡ n * m
  *-assoc : ∀ m n o → m * (n * o) ≡ (m * n) * o

  --0ℝ ≟_
  0≟0≡yes0≡0 : (0ℝ ≟ 0ℝ) ≡ yes refl

  -- TODO: These properties should be written for _<_ instead of _<ᵇ_
  abs<x→<x∧-x< : ∀ {u x} → (abs u <ᵇ x) ≡ ((u <ᵇ x) ∧ (- x <ᵇ u))
  --neg-mono-<-> : -_ Preserves _<_ ⟶ (λ a b -> b < a)
  neg-mono-<-> : ∀ m n → (m <ᵇ n) ≡ (- n <ᵇ - m)
  --+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
  +-monoˡ-< : ∀ n o p → (o <ᵇ p) ≡ (n + o <ᵇ n + p)

-- One of the weakest points in the whole library architecture!!!
-- This is wrong, really wrong, but useful
{-# COMPILE GHC ℝ = type Double #-}
{-# COMPILE GHC fromFloat = \x -> x #-}
{-# COMPILE GHC toFloat = \x -> x #-}
{-# COMPILE GHC fromℕ = fromIntegral #-}

{-# COMPILE GHC _<ᵇ_ = (<) #-}
{-# COMPILE GHC _≤ᵇ_ = (<=) #-}
{-# COMPILE GHC _≡ᵇ_ = (==) #-}

{-# COMPILE GHC _+_ = (+) #-}
{-# COMPILE GHC _-_ = (-) #-}
{-# COMPILE GHC _*_ = (*) #-}
{-# COMPILE GHC _^_ = (**) #-}

{-# COMPILE GHC _^2 = (**2) #-}

{-# COMPILE GHC e = 2.71828182845904523536 #-}
{-# COMPILE GHC π = 3.14159265358979323846 #-}
{-# COMPILE GHC 0ℝ = 0 #-}
{-# COMPILE GHC 1ℝ = 1 #-}
{-# COMPILE GHC 2ℝ = 2 #-}
{-# COMPILE GHC -1/2 = -1/2 #-}

-- REAAALY CAREFUL WITH THIS!
-- TODO: Add some runtime checking to this. Fail hard if divisor is zero
{-# COMPILE GHC 1/_ = \x -> (1/x) #-}
{-# COMPILE GHC _÷_ = \x y -> (x/y) #-}
{-# COMPILE GHC √_  = \x -> sqrt x #-}

max_stars_repo_name: helq/safety-envelopes-sentinels

max_issues_repo_name: helq/safety-envelopes-sentinels

max_forks_repo_name: helq/safety-envelopes-sentinels


text:
open import Prelude
open import Nat
open import List
open import Bij

-- The contents of this file were originally written in a different codebase,
-- which was itself a descendant of a prior codebase that had been using non-standard
-- definitions of naturals and other basic definitions. As such this code has
-- inherited these non-standard idioms, as seen in Prelude, Nat, and List. Ideally,
-- this file would be refactored to use the Agda standard library instead, but beyond
-- the significant effort of refactoring, the Agda standard library appears not to be
-- packaged with Agda, and must be installed separately. The difficulties inherent in
-- attempting to use a "standard library" that is not sufficiently standard as to be
-- included with Agda itself, added to the difficulties of refactoring, have led us
-- to continue with the the non-standard forms and definitions. We hope that they are
-- fairly self-explanatory and intuitive. Below we note some of our idioms that may
-- not be obvious:
-- * We use "Some" and "None" instead of "Just" and "Nothing"
-- * abort is used to prove any goal given ⊥
-- * == is used for reflexive equality
-- * Z is zero, 1+ is suc
-- * ≤ is defined as data, < is defined as n < m = n ≤ m ∧ n ≠ m
-- * l⟦ i ⟧ is used to (maybe) get the ith element of list l
-- * ∥ l ∥ is the length of a list
--
-- Many of the definitions and theorems are documented to indicate their equivalents
-- in the Coq standard libraries Coq.FSets.FMapInterface and Coq.FSets.FMapFacts
module Delta (K : Set) {{bij : bij K Nat}} where
  abstract -- almost everything in the module is abstract

    open import delta-lemmas K {{bij}}

    ---- core definitions ----

    data dd (V : Set) : Set where
      DD : dl V → dd V

    -- nil/empty
    ∅ : {V : Set} → dd V
    ∅ = DD []

    -- singleton
    ■_ : {V : Set} → (K ∧ V) → dd V
    ■_ (k , v) = DD <| (nat k , v) :: []

    -- extension/insertion
    -- Corresponds to FMapInterface.add
    _,,_ : ∀{V} → dd V → (K ∧ V) → dd V
    (DD d) ,, (k , v) = DD <| d ,,' (nat k , v)

    infixl 10 _,,_

    -- lookup function
    -- Corresponds to FMapInterface.find
    _⟨_⟩ : {V : Set} → dd V → K → Maybe V
    (DD d) ⟨ k ⟩ = d lkup (nat k)

    -- There doesn't appear to be a corresponding function in FMapInterface
    destruct : ∀{V} → dd V → Maybe ((K ∧ V) ∧ dd V)
    destruct (DD [])
      = None
    destruct (DD ((n , v) :: []))
      = Some ((key n , v) , DD [])
    destruct (DD ((n , v) :: ((m , v') :: dd)))
      = Some ((key n , v) , DD ((m + 1+ n , v') :: dd))

    -- size
    -- Corresponds to FMapInterface.cardinal
    ||_|| : {V : Set} → dd V → Nat
    || DD d || = ∥ d ∥

    -- membership
    -- Corresponds to FMapInterface.MapsTo
    _∈_ : {V : Set} (p : K ∧ V) → (d : dd V) → Set
    _∈_ {V} (k , v) (DD d) = _∈'_ {V} (nat k , v) d

  -- domain (not abstract)
  -- Corresponds to FMapInterface.In
  dom : {V : Set} → dd V → K → Set
  dom {V} d k = Σ[ v ∈ V ] ((k , v) ∈ d)

  -- apartness, i.e. the opposite of dom (not abstract)
  _#_ : {V : Set} → K → dd V → Set
  k # d = dom d k → ⊥

  abstract

    -- maps f across the values of the delta dict
    -- Corresponds to FMapInterface.map
    dltmap : {A B : Set} → (A → B) → dd A → dd B
    dltmap f (DD d) = DD <| map (λ {(hn , hv) → (hn , f hv)}) d

    -- FMapInterface doesn't appear to have a corresponding function
    list⇒dlt : {V : Set} → List (K ∧ V) → dd V
    list⇒dlt d = d |> map (λ where (k , v) → (nat k , v)) |> list⇒dlt' |> DD

    -- converts a delta dict into a list of key-value pairs; the inverse of list⇒dlt
    -- Corresponds to FMapInterface.elements
    dlt⇒list : {V : Set} → dd V → List (K ∧ V)
    dlt⇒list (DD d) = dlt⇒list' d |> map (λ where (n , v) → (key n , v))

    -- union merge A B is the union of A and B,
    -- with (merge a b) being invoked to handle the mappings they have in common
    union : {V : Set} → (V → V → V) → dd V → dd V → dd V
    union merge (DD d1) (DD d2) = DD <| union' merge d1 d2 0

    ---- core theorems ----

    -- The next two theorems show that lookup (_⟨_⟩) is consistent with membership (_∈_)
    -- As such, future theorems which relate to membership can be taken to appropriately
    -- comment on lookup as well.
    -- Corresponds to FMapInterface.find_1
    lookup-cons-1 : {V : Set} {d : dd V} {k : K} {v : V} →
                     (k , v) ∈ d →
                     d ⟨ k ⟩ == Some v
    lookup-cons-1 {V} {DD d} {k} {v} = lookup-cons-1' {V} {d} {nat k} {v}

    -- Corresponds to FMapInterface.find_2
    lookup-cons-2 : {V : Set} {d : dd V} {k : K} {v : V} →
                     d ⟨ k ⟩ == Some v →
                     (k , v) ∈ d
    lookup-cons-2 {V} {DD d} {k} {v} h = lookup-cons-2' {d = d} {nat k} h

    -- membership (_∈_) respects insertion (_,,_)
    -- Corresponds to FMapInterface.add_1
    k,v∈d,,k,v : {V : Set} {d : dd V} {k : K} {v : V} →
                  (k , v) ∈ (d ,, (k , v))
    k,v∈d,,k,v {V} {d = DD d} {k} = n,v∈'d,,n,v {d = d} {nat k}

    -- insertion respects membership
    -- Corresponds to FMapInterface.add_2
    k∈d→k∈d+ : {V : Set} {d : dd V} {k k' : K} {v v' : V} →
                  k ≠ k' →
                  (k , v) ∈ d →
                  (k , v) ∈ (d ,, (k' , v'))
    k∈d→k∈d+ {V} {DD d} {k} {k'} {v} {v'} ne h
      = n∈d→'n∈d+ {V} {d} {nat k} {nat k'} {v} {v'} (inj-cp ne) h

    -- insertion can't generate spurious membership
    -- Corresponds to FMapInterface.add_3
    k∈d+→k∈d : {V : Set} {d : dd V} {k k' : K} {v v' : V} →
                k ≠ k' →
                (k , v) ∈ (d ,, (k' , v')) →
                (k , v) ∈ d
    k∈d+→k∈d {V} {d = DD d} {k} {k'} {v} {v'} ne h
      = n∈d+→'n∈d {V} {d} {nat k} {nat k'} {v} {v'} (inj-cp ne) h

    -- Decidability of membership
    -- This also packages up an appeal to delta dict membership into a form that
    -- lets us retain more information
    -- Corresponds to FMapFacts.In_dec
    mem-dec : {V : Set} (d : dd V) (k : K) → dom d k ∨ k # d
    mem-dec {V} (DD d) k = mem-dec' {V} d (nat k)

    -- delta dicts contain at most one binding for each variable
    -- Corresponds to FMapFacts.MapsTo_fun
    mem-unicity : {V : Set} {d : dd V} {k : K} {v v' : V} →
                   (k , v) ∈ d →
                   (k , v') ∈ d →
                   v == v'
    mem-unicity vh v'h
      with lookup-cons-1 vh | lookup-cons-1 v'h
    ... | vh' | v'h' = someinj (! vh' · v'h')

    -- meaning of nil, i.e. nothing is in nil
    -- Corresponds to FMapFacts.empty_in_iff
    k#∅ : {V : Set} {k : K} → _#_ {V} k ∅
    k#∅ (_ , ())

    -- meaning of the singleton
    ■-def : {V : Set} {k : K} {v : V} → (■ (k , v)) == ∅ ,, (k , v)
    ■-def = refl

    -- Theorem 2: Extensionality
    -- (i.e. if two dicts represent the same mapping from ids to values,
    -- then they are reflexively equal as judged by _==_)
    -- Corresponds to FMapFacts.Equal_Equiv
    extensional : {V : Set} {d1 d2 : dd V} →
                   ((k : K) → d1 ⟨ k ⟩ == d2 ⟨ k ⟩) →
                   d1 == d2
    extensional {V} {DD d1} {DD d2} all-bindings-==
      = ap1 DD <| extensional' {V} {d1} {d2} eqv-nat
        where
        eqv-nat : (n : Nat) → (d1 lkup n) == (d2 lkup n)
        eqv-nat n
          with bij.surj bij n
        ... | k , surj
          with all-bindings-== k
        ... | eq rewrite surj = eq

    -- Theorem 3: Decidable Equality
    -- This doesn't seem to directly correspond to any of the Coq theorems
    ==-dec : {V : Set}
              (d1 d2 : dd V) →
              ((v1 v2 : V) → v1 == v2 ∨ v1 ≠ v2) →
              d1 == d2 ∨ d1 ≠ d2
    ==-dec {V} (DD d1) (DD d2) h
      with ==-dec' {V} d1 d2 h
    ... | Inl refl = Inl refl
    ... | Inr ne   = Inr (λ where refl → ne refl)

    -- The next two theorems specify the behavior of destruct and prove that
    -- it behaves as intended. The third one combines them to match the paper.
    destruct-thm-1 : ∀{V} {d : dd V} →
                       destruct d == None →
                       d == ∅
    destruct-thm-1 {d = DD []} eq = refl
    destruct-thm-1 {d = DD (_ :: [])} ()
    destruct-thm-1 {d = DD (_ :: (_ :: _))} ()

    destruct-thm-2 : ∀{V} {d d' : dd V} {k : K} {v : V} →
                       destruct d == Some ((k , v) , d') →
                       k # d' ∧ d == d' ,, (k , v)
    destruct-thm-2 {d = DD ((n , v) :: [])} refl
      rewrite convert-bij2 {{bij}} {t = n}
        = n#'[] , refl
    destruct-thm-2 {d = DD ((n , v) :: ((m , v') :: t))} refl
      rewrite convert-bij2 {{bij}} {t = n}
      with too-small (n<m→n<s+m n<1+n)
    ... | not-in
      with <dec n (m + 1+ n)
    ... | Inl lt rewrite ! (undelta n m lt) = not-in , refl
    ... | Inr (Inl eq) = abort (n≠n+1+m (eq · (n+1+m==1+n+m · +comm {1+ m})))
    ... | Inr (Inr gt) = abort (<antisym gt (n<m→n<s+m n<1+n))

    -- Theorem 4: Not-So-Easy Destructibility
    destruct-thm : ∀{V} {d d' : dd V} {k : K} {v : V} →
                     (destruct d == None → d == ∅)
                       ∧
                     (destruct d == Some ((k , v) , d') →
                        k # d' ∧ d == d' ,, (k , v))
    destruct-thm = destruct-thm-1 , destruct-thm-2

    -- When using destruct or delete, this theorem is useful for establishing termination
    -- Roughly corresponds to FMapFacts.cardinal_2
    extend-size : {V : Set} {d : dd V} {k : K} {v : V} →
                   k # d →
                   || d ,, (k , v) || == 1+ || d ||
    extend-size {V} {DD d} {k} {v} n#d = extend-size' {V} {d} {nat k} {v} n#d

    -- remove a specific mapping from a delta dict
    -- Roughly corresponds to FMapInterface.remove, and associated theorems
    delete : {V : Set} {d : dd V} {k : K} {v : V} →
              (k , v) ∈ d →
              Σ[ d⁻ ∈ dd V ] (
                 d == d⁻ ,, (k , v) ∧
                 k # d⁻)
    delete {V} {DD d} {k} {v} h
      with delete' {V} {d} {nat k} {v} h
    ... | _ , refl , # = _ , refl , #

    ---- contraction and exchange ----

    -- Theorem 5
    contraction : {V : Set} {d : dd V} {k : K} {v v' : V} →
                   d ,, (k , v') ,, (k , v) == d ,, (k , v)
    contraction {V} {DD d} {k} {v} {v'}
      = ap1 DD <| contraction' {d = d} {nat k} {v} {v'}

    -- Theorem 6
    exchange : {V : Set} {d : dd V} {k1 k2 : K} {v1 v2 : V} →
                k1 ≠ k2 →
                d ,, (k1 , v1) ,, (k2 , v2) == d ,, (k2 , v2) ,, (k1 , v1)
    exchange {V} {DD d} {k1} {k2} {v1} {v2} k1≠k2
      = ap1 DD <| exchange' {d = d} <| inj-cp k1≠k2

    ---- union theorems ----

    k,v∈d1→k∉d2→k,v∈d1∪d2 : {V : Set} {m : V → V → V} {d1 d2 : dd V} {k : K} {v : V} →
                             (k , v) ∈ d1 →
                             k # d2 →
                             (k , v) ∈ union m d1 d2
    k,v∈d1→k∉d2→k,v∈d1∪d2 {d1 = DD d1} {DD d2} k∈d1 k#d2
      = lemma-union'-1 k∈d1 0≤n (tr (λ y → y #' d2) (! (n+m-n==m 0≤n)) k#d2)

    k∉d1→k,v∈d2→k,v∈d1∪d2 : {V : Set} {m : V → V → V} {d1 d2 : dd V} {k : K} {v : V} →
                             k # d1 →
                             (k , v) ∈ d2 →
                             (k , v) ∈ union m d1 d2
    k∉d1→k,v∈d2→k,v∈d1∪d2 {d1 = DD d1} {DD d2} {k} k#d1 k∈d2
      with lemma-union'-2 {n = Z} (tr (λ y → y #' d1) (! n+Z==n) k#d1) k∈d2
    ... | rslt
      rewrite n+Z==n {nat k}
        = rslt

    k∈d1→k∈d2→k∈d1∪d2 : {V : Set} {m : V → V → V} {d1 d2 : dd V} {k : K} {v1 v2 : V} →
                         (k , v1) ∈ d1 →
                         (k , v2) ∈ d2 →
                         (k , m v1 v2) ∈ union m d1 d2
    k∈d1→k∈d2→k∈d1∪d2 {d1 = DD d1} {DD d2} {k} {v1} k∈d1 k∈d2
      with lemma-union'-3 (tr (λ y → (y , v1) ∈' d1) (! n+Z==n) k∈d1) k∈d2
    ... | rslt
      rewrite n+Z==n {nat k}
        = rslt

    k∈d1∪d2→k∈d1∨k∈d2 : {V : Set} {m : V → V → V} {d1 d2 : dd V} {k : K} →
                         dom (union m d1 d2) k →
                         dom d1 k ∨ dom d2 k
    k∈d1∪d2→k∈d1∨k∈d2 {d1 = DD d1} {DD d2} k∈d1∪d2
      with lemma-union'-4 {n = Z} k∈d1∪d2
    k∈d1∪d2→k∈d1∨k∈d2 k∈d1∪d2 | Inl k'∈d1 = Inl k'∈d1
    k∈d1∪d2→k∈d1∨k∈d2 k∈d1∪d2 | Inr (_ , refl , k'∈d2) = Inr k'∈d2

    ---- dltmap theorem ----

    -- The Coq.FSets library uses different theorems to establish to specify map
    dltmap-func : {V1 V2 : Set} {d : dd V1} {f : V1 → V2} {k : K} {v : V1} →
                   dltmap f (d ,, (k , v)) == dltmap f d ,, (k , f v)
    dltmap-func {d = DD d} {f} {k} {v} = ap1 DD (dltmap-func' {d = d})

    ---- dlt <=> list theorems ----

    -- Corresponds to FMapInterface.cardinal_1
    dlt⇒list-size : {V : Set} {d : dd V} → ∥ dlt⇒list d ∥ == || d ||
    dlt⇒list-size {d = DD d} = map-len · dlt⇒list-size'

    -- Corresponds to FMapInterface.elements_1
    dlt⇒list-In-1 : {V : Set} {d : dd V} {k : K} {v : V} →
                      (k , v) ∈ d →
                      (k , v) In dlt⇒list d
    dlt⇒list-In-1 {d = DD d} {k} in'
      rewrite ! <| convert-bij1 {f = k}
      with dlt⇒list-In-1' in'
    ... | in'' rewrite convert-bij2 {{bij}} {t = bij.convert bij k}
      = map-In in''

    -- Corresponds to FMapInterface.elements_2
    dlt⇒list-In-2 : {V : Set} {d : dd V} {k : K} {v : V} →
                      (k , v) In dlt⇒list d →
                      (k , v) ∈ d
    dlt⇒list-In-2 {V} {d = DD d} {k} {v} in'
      with map-In {f = λ where (k' , v') → (nat k' , v')} in'
    ... | in'' rewrite map^2 {f = λ where (k' , v') → (nat k' , v')} {g = λ where (n' , v') → (key n' , v')} {l = dlt⇒list' d}
      = dlt⇒list-In-2' (tr
          (λ y → (nat k , v) In y)
          (map^2 · (map-ext bij-pair-1 · map-id))
          (map-In {f = λ where (k , v) → (nat k , v)} in'))

    list⇒dlt-In : {V : Set} {l : List (K ∧ V)} {k : K} {v : V} →
                    (k , v) ∈ list⇒dlt l →
                    (k , v) In l
    list⇒dlt-In {l = l} {k} {v} in'
      with list⇒dlt-In' {l = map (λ { (k , v) → nat k , v }) l} in' |> map-In {f = λ where (n , v) → key n , v}
    ... | in'' rewrite convert-bij1 {f = k}
      = tr
           (λ y → (k , v) In y)
           (map^2 · (map-ext bij-pair-2 · map-id))
           in''

    list⇒dlt-key-In : {V : Set} {l : List (K ∧ V)} {k : K} {v : V} →
                        (k , v) In l →
                        dom (list⇒dlt l) k
    list⇒dlt-key-In {_} {(k , v) :: l} {k} {v} LInH
      rewrite foldl-++ {l1 = reverse <| map (λ where (k , v) → nat k , v) l} {(nat k , v) :: []} {_,,'_} {[]}
        = _ , tr
           (λ y → (nat k , v) ∈' y)
           (! <| foldl-++ {l1 = reverse <| map (λ where (k , v) → nat k , v) l})
           (n,v∈'d,,n,v {d = list⇒dlt' <| map (λ where (k , v) → nat k , v) l})
    list⇒dlt-key-In {V} {(k' , v') :: l} {k} {v} (LInT in')
      with list⇒dlt-key-In in'
    ... | (_ , in'')
      = _ , tr
         (λ y → (nat k , vv) ∈' y)
         (! <| foldl-++ {l1 = reverse <| map (λ where (k , v) → nat k , v) l})
         lem'
      where
      nat-inj : ∀{k1 k2} → nat k1 == nat k2 → k1 == k2
      nat-inj eq = ! (convert-bij1 {{bij}}) · (ap1 key eq · convert-bij1 {{bij}})
      lem : Σ[ vv ∈ V ] ((nat k , vv) ∈' (list⇒dlt' (map (λ { (k , v) → nat k , v }) l) ,,' (nat k' , v')))
      lem
        with natEQ (nat k) (nat k')
      ... | Inl eq rewrite ! <| nat-inj eq
        = _ , n,v∈'d,,n,v {d = list⇒dlt' (map (λ { (k , v) → nat k , v }) l)}
      ... | Inr ne = _ , n∈d→'n∈d+ ne in''
      vv = π1 lem
      lem' = π2 lem

    -- contrapositives of some previous theorems
    dlt⇒list-In-1-cp : {V : Set} {d : dd V} {k : K} → (Σ[ v ∈ V ] ((k , v) In dlt⇒list d) → ⊥) → k # d
    dlt⇒list-In-1-cp {d = DD d} not-in = λ where (_ , in') → not-in (_ , (dlt⇒list-In-1 in'))
    list⇒dlt-key-In-cp : {V : Set} {l : List (K ∧ V)} {k : K} → k # list⇒dlt l → Σ[ v ∈ V ] ((k , v) In l) → ⊥
    list⇒dlt-key-In-cp k#d' (_ , k∈l) = k#d' (list⇒dlt-key-In k∈l)

    list⇒dlt-order : {V : Set} {l1 l2 : List (K ∧ V)} {k : K} {v1 v2 : V} →
                       (k , v1) ∈ (list⇒dlt ((k , v1) :: l1 ++ ((k , v2) :: l2)))
    list⇒dlt-order {_} {l1} {l2} {k} {v1} {v2}
      = tr
           (λ y → (nat k , v1) ∈' foldl _,,'_ [] (reverse y ++ ((nat k , v1) :: [])))
           (map-++-comm {a = l1})
           (list⇒dlt-order' {l1 = map (λ where (k , v) → nat k , v) l1})

    dlt⇒list-inversion : {V : Set} {d : dd V} → list⇒dlt (dlt⇒list d) == d
    dlt⇒list-inversion {d = DD d} = extensional lem
      where
      lem : (k : K) → (list⇒dlt (dlt⇒list <| DD d) ⟨ k ⟩ == DD d ⟨ k ⟩)
      lem k
        with mem-dec (list⇒dlt (dlt⇒list <| DD d)) k
      ... | Inl (_ , k∈d')
        = lookup-cons-1 k∈d' · (k∈d' |> list⇒dlt-In |> dlt⇒list-In-2 |> lookup-cons-1 {d = DD d} |> !)
      ... | Inr k#d'
        = lookup-cp-2' k#d' · (k#d' |> list⇒dlt-key-In-cp |> dlt⇒list-In-1-cp |> lookup-cp-2' {d = d} |> !)

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module FixityOutOfScopeInRecord where

postulate _+_ : Set

record R : Set where
  infixl 30 _+_

-- Should complain that _+_ is not in (the same) scope
-- in (as) its fixity declaration.


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.Impl.Consensus.Liveness.ProposerElection
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.LBFT
open import Optics.All
open import Util.Lemmas
open import Util.Prelude

module LibraBFT.Impl.Consensus.Liveness.Properties.ProposerElection where

-- TUTORIAL
module isValidProposalMSpec (b : Block) where

  pe      = _^∙ lProposerElection
  mAuthor = b ^∙ bAuthor
  round   = b ^∙ bRound

  contract
    : ∀ pre Post
      → (mAuthor ≡ nothing → Post (Left ProposalDoesNotHaveAnAuthor) pre [])
      → (Maybe-Any (getValidProposer (pe pre) round ≢_) mAuthor
         → Post (Left ProposerForBlockIsNotValidForThisRound) pre [])
      → (Maybe-Any (getValidProposer (pe pre) round ≡_) mAuthor
         → Post (Right unit) pre [])
      → LBFT-weakestPre (isValidProposalM b) Post pre
  -- 1. `isValidProposalM` begins with `RWS-maybe`, so we must provide two cases:
  --    one where `b ^∙ bAuthor` is `nothing` and one where it is `just`
  --    something
  -- 2. When it is nothing, we appeal to the assumed proof
  proj₁ (contract pre Post pfNone pf≢ pfOk) mAuthor≡nothing = pfNone mAuthor≡nothing
  -- 3. When it is something, we step into `isValidProposerM`. This means:
  --    - we use the proposer election of the round manager (`pe` and `pe≡`)
  --    - we apply `isValidProposer` to `pe`  (`isvp-pe` and `isvp-pe≡`)
  --    - we push the pure value `a` into the LBFT monad and apply `isvp-pe` to
  --      it (`.a`, `isvp-pe-a`, and `isvp-pe-a≡`)
  --    - we push the pure value `b ^∙ bRound` (`r` and `r≡`) into the LBFT
  --      monad, and the returned value is the result of applying `isvp-pe-a` to
  --      this
  --    - now out of `isValidProposalM`, we are given an alias `r'` for `r`
  -- > proj₂ (contract Post pre pfNone pf≢ pfOk) a ma≡just-a isvp isvp≡ pe pe≡ isvp-pe isvp-pe≡ .a refl isvp-pe-a isvp-pe-a≡ r r≡ r' r'≡ = {!!}
  -- 4. Since the returned value we want to reason about is directly related to
  --    the behavior of these bound functions which are partial applications of
  --    `isValidProposer`, we perform case-analysis on each of the equality
  --    proofs (we can't pattern match on `ma≡just-a` directly)
  -- > proj₂ (contract pre Post pfNone pf≢ pfOk) a ma≡just-a ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl = {!!}
  -- 5. Now we encounter an `ifD`, which means we must provide two cases, one corresponding to each branch.
  proj₁ (proj₂ (contract pre Post pfNone pf≢ pfOk) a ma≡just-a ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl) vp≡true
  -- 6. The types of `pfOk` and `pf≢` are still "stuck" on the expression
  -- > b ^∙ bAuthor
  --    So, in both the `false` and `true` cases we rewrite by `ma≡just-a`, which
  --    tells us that the result is `just a`
    rewrite ma≡just-a =
  -- 7. To finish, we use `toWitnessF` to convert between the two forms of evidence.
    pfOk (just (toWitnessT vp≡true))
  proj₂ (proj₂ (contract pre Post pfNone pf≢ pfOk) a ma≡just-a ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl ._ refl) vp≡false
    rewrite ma≡just-a =
    pf≢ (just (toWitnessF vp≡false))


text:
module Logic.Identity where

open import Logic.Equivalence
open import Logic.Base

infix 20 _≡_ _≢_

data _≡_ {A : Set}(x : A) : A -> Set where
  refl : x ≡ x

subst : {A : Set}(P : A -> Set){x y : A} -> x ≡ y -> P y -> P x
subst P {x} .{x} refl px = px

sym : {A : Set}{x y : A} -> x ≡ y -> y ≡ x
sym {A} refl = refl

trans : {A : Set}{x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
trans {A} refl xz = xz

cong : {A B : Set}(f : A -> B){x y : A} -> x ≡ y -> f x ≡ f y
cong {A} f refl = refl

cong2 : {A B C : Set}(f : A -> B -> C){x z : A}{y w : B} -> x ≡ z -> y ≡ w -> f x y ≡ f z w
cong2 {A}{B} f refl refl = refl

Equiv : {A : Set} -> Equivalence A
Equiv = record
	{ _==_  = _≡_
	; refl  = \x -> refl
	; sym   = \x y -> sym
	; trans = \x y z -> trans
	}

_≢_ : {A : Set} -> A -> A -> Set
x ≢ y = ¬ (x ≡ y)

sym≢ : {A : Set}{x y : A} -> x ≢ y -> y ≢ x
sym≢ np p = np (sym p)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Lex.NonStrict directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Lex.NonStrict where

open import Data.List.Relation.Binary.Lex.NonStrict public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Lex.NonStrict was deprecated in v1.0.
Use Data.List.Relation.Binary.Lex.NonStrict instead."
#-}


text:
------------------------------------------------------------------------
-- Binomial theorem
------------------------------------------------------------------------

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

module Math.BinomialTheorem.Nat where

-- agda-stdlib
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality
open import Function

-- agda-combinatorics
open import Math.Combinatorics.Function
open import Math.Combinatorics.Function.Properties

-- agda-misc
open import Math.NumberTheory.Summation.Nat
open import Math.NumberTheory.Summation.Nat.Properties

open ≤-Reasoning

private
  lemma₁ : ∀ x y n k → x * (C n k * (x ^ k * y ^ (n ∸ k))) ≡
                       C n k * (x ^ suc k * y ^ (n ∸ k))
  lemma₁ x y n k =
    solve 4 (λ m n o p → m :* (n :* (o :* p)) := n :* (m :* o :* p))
            refl x (C n k) (x ^ k) (y ^ (n ∸ k))
    where open +-*-Solver

  lemma₂ : ∀ x y n k → y * (C n k * (x ^ k * y ^ (n ∸ k))) ≡
                       C n k * (x ^ k * y ^ suc (n ∸ k))
  lemma₂ x y n k =
    solve 4 (λ m n o p → m :* (n :* (o :* p)) := n :* (o :* (m :* p)) )
            refl y (C n k) (x ^ k) (y ^ (n ∸ k))
    where open +-*-Solver

  glemma₃ : ∀ x y m n → C m m * (x ^ suc n * y ^ (n ∸ n)) ≡ x ^ suc n
  glemma₃ x y m n = begin-equality
    C m m * (x ^ suc n * y ^ (n ∸ n))
      ≡⟨ cong₂ (λ u v → u * (x ^ suc n * y ^ v)) (C[n,n]≡1 m) (n∸n≡0 n) ⟩
    1 * (x ^ suc n * 1)
      ≡⟨ *-identityˡ (x ^ suc n * 1) ⟩
    x ^ suc n * 1
      ≡⟨ *-identityʳ (x ^ suc n) ⟩
    x ^ suc n
      ∎

  lemma₃ : ∀ x y n → C n n * (x ^ suc n * y ^ (n ∸ n)) ≡ x ^ suc n
  lemma₃ x y n = glemma₃ x y n n

  lemma₄ : ∀ {k n} → k < n → suc (n ∸ suc k) ≡ suc n ∸ suc k
  lemma₄ k<n = sym $ +-∸-assoc 1 k<n

  lemma₅ : ∀ n → 1 * (1 * n) ≡ n
  lemma₅ n = trans (*-identityˡ (1 * n)) (*-identityˡ n)

  lemma₆ : ∀ x y n → C (suc n) (suc n) * (x ^ suc n * y ^ (n ∸ n)) ≡ x ^ suc n
  lemma₆ x y n = glemma₃ x y (suc n) n

  lemma₇ : ∀ m n o p → m + n + (o + p) ≡ n + o + (m + p)
  lemma₇ = solve 4 (λ m n o p → m :+ n :+ (o :+ p) := n :+ o :+ (m :+ p) ) refl
    where open +-*-Solver

  lemma₈ : ∀ m n o → m + n + o ≡ n + (o + m)
  lemma₈ = solve 3 (λ m n o → m :+ n :+ o := n :+ (o :+ m)) refl
    where open +-*-Solver
{-
(x+y)*(x+y)^n
(x+y)*Σ[k≤n][Cnk*x^k*y^(n∸k)]
-}

theorem : ∀ x y n →
          (x + y) ^ n ≡ Σ[ k ≤ n ] (C n k * (x ^ k * y ^ (n ∸ k)))
theorem x y 0       = begin-equality
  C 0 0 * ((x ^ 0) * y ^ (0 ∸ 0))
    ≡⟨ sym $ Σ≤[0,f]≈f[0] (λ k → C 0 k * (x ^ k * y ^ (0 ∸ k))) ⟩
  Σ≤ 0 (λ k → C 0 k * (x ^ k * y ^ (0 ∸ k)))
    ∎
theorem x y (suc n) = begin-equality
  (x + y) * (x + y) ^ n
    ≡⟨ cong ((x + y) *_) $ theorem x y n ⟩
  (x + y) * Σ[ k ≤ n ] (C n k * (x ^ k * y ^ (n ∸ k)))
    ≡⟨ *-distribʳ-+ (Σ[ k ≤ n ] (C n k * (x ^ k * y ^ (n ∸ k)))) x y ⟩
  x * Σ[ k ≤ n ] (C n k * (x ^ k * y ^ (n ∸ k))) + y * Σ[ k ≤ n ] (C n k * (x ^ k * y ^ (n ∸ k)))
    ≡⟨ sym $ cong₂ _+_ (Σ≤-*-commute n x (λ k → C n k * (x ^ k * y ^ (n ∸ k)))) (Σ≤-*-commute n y (λ k → C n k * (x ^ k * y ^ (n ∸ k)))) ⟩
  Σ[ k ≤ n ] (x * (C n k * (x ^ k * y ^ (n ∸ k)))) + Σ[ k ≤ n ] (y * (C n k * (x ^ k * y ^ (n ∸ k))))
    ≡⟨ cong₂ _+_ (Σ≤-congˡ n (λ k → lemma₁ x y n k)) (Σ≤-congˡ n (λ k → lemma₂ x y n k)) ⟩
  Σ[ k ≤ n ] (C n k * ((x ^ suc k) * y ^ (n ∸ k))) + Σ[ k ≤ n ] (C n k * (x ^ k * y ^ suc (n ∸ k)))
    ≡⟨ cong (Σ[ k ≤ n ] (C n k * (x ^ suc k * y ^ (n ∸ k))) +_) $ Σ<-push-suc n (λ k → C n k * (x ^ k * y ^ suc (n ∸ k))) ⟩
  Σ[ k < n ] (C n k * ((x ^ suc k) * y ^ (n ∸ k))) + C n n * ((x ^ suc n) * y ^ (n ∸ n))
    + (C n 0 * (x ^ 0 * y ^ (suc (n ∸ 0))) + Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ suc (n ∸ suc k))))
    ≡⟨⟩
  Σ[ k < n ] (C n k * ((x ^ suc k) * y ^ (n ∸ k))) + C n n * ((x ^ suc n) * y ^ (n ∸ n))
    + (1 * (1 * y ^ suc n) + Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ suc (n ∸ suc k))))
    ≡⟨ cong₂ _+_ (cong (Σ[ k < n ] (C n k * (x ^ suc k * y ^ (n ∸ k))) +_) $ lemma₃ x y n)
                 (cong₂ _+_ (lemma₅ (y ^ suc n))
                    (Σ<-congˡ-with-< n $ λ k k<n → cong (λ v → C n (suc k) * (x ^ suc k * y ^ v)) $ lemma₄ k<n)) ⟩
  Σ[ k < n ] (C n k * (x ^ suc k * y ^ (n ∸ k))) + x ^ suc n
    + (y ^ suc n + Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ (n ∸ k))))
    ≡⟨ lemma₇ (Σ[ k < n ] (C n k * (x ^ suc k * y ^ (n ∸ k)))) (x ^ suc n) (y ^ suc n) (Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ (n ∸ k)))) ⟩
  x ^ suc n + y ^ suc n + (Σ[ k < n ] (C n k * (x ^ suc k * y ^ (n ∸ k))) +
                          Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ (n ∸ k))))
   ≡⟨ cong (λ v → (x ^ suc n + y ^ suc n) + v) $ lemma ⟩
  x ^ suc n + y ^ suc n + Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))
    ≡⟨ lemma₈ (x ^ suc n) (y ^ suc n) (Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))) ⟩
  y ^ suc n + (Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k))) + x ^ suc n)
    ≡⟨ cong (λ v → y ^ suc n + (Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k))) + v)) $ sym $ lemma₆ x y n ⟩
  y ^ suc n + (Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k))) + C (suc n) (suc n) * (x ^ suc n * y ^ (n ∸ n)))
    ≡⟨⟩
  y ^ suc n + Σ[ k ≤ n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))
   ≡⟨ cong (_+ Σ[ k ≤ n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))) $ sym $ lemma₅ (y ^ suc n) ⟩
  1 * (1 * y ^ suc n) + Σ[ k ≤ n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))
   ≡⟨ sym $ Σ≤-push-suc n (λ k → C (suc n) k * (x ^ k * y ^ (suc n ∸ k))) ⟩
  Σ≤ (suc n) (λ k → C (suc n) k * (x ^ k * y ^ (suc n ∸ k)))
    ∎
  where
  lemma : Σ[ k < n ] (C n k * (x ^ suc k * y ^ (n ∸ k))) +
          Σ[ k < n ] (C n (suc k) * (x ^ suc k * y ^ (n ∸ k))) ≡
          Σ[ k < n ] (C (suc n) (suc k) * (x ^ suc k * y ^ (n ∸ k)))
  lemma = begin-equality
    Σ[ k < n ] (C n k * z k) + Σ[ k < n ] (C n (suc k) * z k)
      ≡⟨ sym $ Σ<-distrib-+ n (λ k → C n k * z k) (λ k → C n (suc k) * z k) ⟩
    Σ[ k < n ] (C n k * z k + C n (suc k) * z k)
      ≡⟨ Σ<-congˡ n (λ k → sym $ *-distribʳ-+ (z k) (C n k) (C n (suc k))) ⟩
    Σ[ k < n ] ((C n k + C n (suc k)) * z k)
      ≡⟨ Σ<-congˡ n (λ k → cong (_* z k) $ sym $ C[1+n,1+k]≡C[n,k]+C[n,1+k] n k) ⟩
    Σ[ k < n ] (C (suc n) (suc k) * z k)
      ∎
    where
    z = λ k → x ^ suc k * y ^ (n ∸ k)

Σ[k≤n]C[n,k]≡2^n : ∀ n → Σ[ k ≤ n ] C n k ≡ 2 ^ n
Σ[k≤n]C[n,k]≡2^n n = begin-equality
  Σ[ k ≤ n ] (C n k)
    ≡⟨ sym $ Σ≤-congˡ n (λ k → begin-equality
        C n k * (1 ^ k * 1 ^ (n ∸ k))
          ≡⟨ cong (C n k *_) $ cong₂ _*_ (^-zeroˡ k) (^-zeroˡ (n ∸ k)) ⟩
        C n k * (1 * 1)
          ≡⟨ *-identityʳ (C n k) ⟩
        C n k
          ∎ ) ⟩
  Σ[ k ≤ n ] (C n k * (1 ^ k * 1 ^ (n ∸ k)))
    ≡⟨ sym $ theorem 1 1 n ⟩
  (1 + 1) ^ n
    ∎


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Combinatory | CL

type
  * : 0-ary

term
  app : *  *  ->  * | _$_ l20
  i   : *
  k   : *
  s   : *

theory
  (IA) x     |> app (i, x) = x
  (KA) x y   |> app (app(k, x), y) = x
  (SA) x y z |> app (app (app (s, x), y), z) = app (app(x, z), app(y, z))
-}

module Combinatory.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data CLₒ : Set where
  appₒ iₒ kₒ sₒ : CLₒ

-- Term signature
CL:Sig : Signature CLₒ
CL:Sig = sig λ
  {  appₒ  → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  ;  iₒ    → ⟼₀ *
  ;  kₒ    → ⟼₀ *
  ;  sₒ    → ⟼₀ *
  }

open Signature CL:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of decision procedures and how to use them
------------------------------------------------------------------------

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

module README.Decidability where

-- Reflects and Dec are defined in Relation.Nullary, and operations on them can
-- be found in Relation.Nullary.Reflects and Relation.Nullary.Decidable.

open import Relation.Nullary as Nullary
open import Relation.Nullary.Reflects
open import Relation.Nullary.Decidable

open import Data.Bool
open import Data.List
open import Data.List.Properties using (∷-injective)
open import Data.Nat
open import Data.Nat.Properties using (suc-injective)
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nary
open import Relation.Nullary.Product

infix 4 _≟₀_ _≟₁_ _≟₂_

-- A proof of `Reflects P b` shows that a proposition `P` has the truth value of
-- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and
-- a proof of `Reflects P false` amounts to a refutation of `P`.

ex₀ : (n : ℕ) → Reflects (n ≡ n) true
ex₀ n = ofʸ refl

ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
ex₁ n = ofⁿ λ ()

ex₂ : (b : Bool) → Reflects (T b) b
ex₂ false = ofⁿ id
ex₂ true  = ofʸ tt

-- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
-- `Dec P` is declared as a record, with fields:
--   does : Bool
--   proof : Reflects P does

ex₃ : (b : Bool) → Dec (T b)
does  (ex₃ b) = b
proof (ex₃ b) = ex₂ b

-- We also have pattern synonyms `yes` and `no`, allowing both fields to be
-- given at once.

ex₄ : (n : ℕ) → Dec (zero ≡ suc n)
ex₄ n = no λ ()

-- It is possible, but not ideal, to define recursive decision procedures using
-- only the `yes` and `no` patterns. The following procedure decides whether two
-- given natural numbers are equal.

_≟₀_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≟₀ zero  = yes refl
zero  ≟₀ suc n = no λ ()
suc m ≟₀ zero  = no λ ()
suc m ≟₀ suc n with m ≟₀ n
... | yes p = yes (cong suc p)
... | no ¬p = no (¬p ∘ suc-injective)

-- In this case, we can see that `does (suc m ≟ suc n)` should be equal to
-- `does (m ≟ n)`, because a `yes` from `m ≟ n` gives rise to a `yes` from the
-- result, and similarly for `no`. However, in the above definition, this
-- equality does not hold definitionally, because we always do a case split
-- before returning a result. To avoid this, we can return the `does` part
-- separately, before any pattern matching.

_≟₁_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≟₁ zero  = yes refl
zero  ≟₁ suc n = no λ ()
suc m ≟₁ zero  = no λ ()
does  (suc m ≟₁ suc n) = does (m ≟₁ n)
proof (suc m ≟₁ suc n) with m ≟₁ n
... | yes p = ofʸ (cong suc p)
... | no ¬p = ofⁿ (¬p ∘ suc-injective)

-- We now get definitional equalities such as the following.

_ : (m n : ℕ) → does (5 + m ≟₁ 3 + n) ≡ does (2 + m ≟₁ n)
_ = λ m n → refl

-- Even better, from a maintainability point of view, is to use `map` or `map′`,
-- both of which capture the pattern of the `does` field remaining the same, but
-- the `proof` field being updated.

_≟₂_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≟₂ zero  = yes refl
zero  ≟₂ suc n = no λ ()
suc m ≟₂ zero  = no λ ()
suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n)

_ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n)
_ = λ m n → refl

-- `map′` can be used in conjunction with combinators such as `_⊎-dec_` and
-- `_×-dec_` to build complex (simply typed) decision procedures.

module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where

  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
  []       ≟ᴸᴬ []       = yes refl
  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) =
    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×-dec xs ≟ᴸᴬ ys)

-- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and*
-- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`.

-- In the case of ≡-equality tests, the pattern
-- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×-dec ... ×-dec xₙ₋₁ ≟ yₙ₋₁)`
-- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`.

module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where

  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
  []       ≟ᴸᴬ []       = yes refl
  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = ≟-mapₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys)


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

module WithoutK2 where

-- Equality defined with two indices.

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

K : {A : Set} (P : {x : A} → x ≡ x → Set) →
    (∀ x → P (refl x)) →
    ∀ {x} (x≡x : x ≡ x) → P x≡x
K P p (refl x) = p x


text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Substitution structure by initiality
module SOAS.Metatheory.Substitution {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  (𝔛 : Familyₛ) (open SOAS.Metatheory.MetaAlgebra ⅀F 𝔛)
  (𝕋:Init : Initial 𝕄etaAlgebras)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as →□ ; open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Abstract.Monoid

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Monoid
open import SOAS.Coalgebraic.Lift

open import SOAS.Metatheory.Algebra ⅀F
open import SOAS.Metatheory.Semantics ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Traversal ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Renaming ⅀F ⅀:Str 𝔛 𝕋:Init
open import SOAS.Metatheory.Coalgebraic ⅀F ⅀:Str 𝔛 𝕋:Init

open Strength ⅀:Str

private
  variable
    Γ Δ : Ctx
    α β : T

-- Substitution is a 𝕋-parametrised traversal into 𝕋
module Substitution = Traversal 𝕋ᴮ 𝕒𝕝𝕘 id 𝕞𝕧𝕒𝕣

𝕤𝕦𝕓 : 𝕋 ⇾̣ 〖 𝕋 , 𝕋 〗
𝕤𝕦𝕓 = Substitution.𝕥𝕣𝕒𝕧

-- The renaming and algebra structures on 𝕋 are compatible, so 𝕤𝕦𝕓 is coalgebraic
𝕤𝕦𝕓ᶜ : Coalgebraic 𝕋ᴮ 𝕋ᴮ 𝕋ᴮ 𝕤𝕦𝕓
𝕤𝕦𝕓ᶜ = Travᶜ.𝕥𝕣𝕒𝕧ᶜ 𝕋ᴮ 𝕒𝕝𝕘 id 𝕞𝕧𝕒𝕣 𝕋ᴮ idᴮ⇒ Renaming.𝕤𝕖𝕞ᵃ⇒

module 𝕤𝕦𝕓ᶜ = Coalgebraic 𝕤𝕦𝕓ᶜ

-- Compatibility of renaming and substitution
compat : {ρ : Γ ↝ Δ} (t : 𝕋 α Γ) → 𝕣𝕖𝕟 t ρ ≡ 𝕤𝕦𝕓 t (𝕧𝕒𝕣 ∘ ρ)
compat {ρ = ρ} t =  begin 𝕣𝕖𝕟 t ρ           ≡˘⟨ 𝕥𝕣𝕒𝕧-η≈id 𝕋ᴮ id refl ⟩
                          𝕤𝕦𝕓 (𝕣𝕖𝕟 t ρ) 𝕧𝕒𝕣  ≡⟨ 𝕤𝕦𝕓ᶜ.f∘r ⟩
                          𝕤𝕦𝕓 t (𝕧𝕒𝕣 ∘ ρ)   ∎ where open ≡-Reasoning

-- Substitution associativity law
𝕤𝕦𝕓-comp : MapEq₂ 𝕋ᴮ 𝕋ᴮ 𝕒𝕝𝕘 (λ t σ ς → 𝕤𝕦𝕓 (𝕤𝕦𝕓 t σ) ς)
                           (λ t σ ς → 𝕤𝕦𝕓 t (λ v → 𝕤𝕦𝕓 (σ v) ς))
𝕤𝕦𝕓-comp = record
  { φ = id
  ; ϕ = 𝕤𝕦𝕓
  ; χ = 𝕞𝕧𝕒𝕣
  ; f⟨𝑣⟩ = 𝕥≈₁ 𝕥⟨𝕧⟩
  ; f⟨𝑚⟩ = trans (𝕥≈₁ 𝕥⟨𝕞⟩) 𝕥⟨𝕞⟩
  ; f⟨𝑎⟩ = λ{ {σ = σ}{ς}{t} → begin
        𝕤𝕦𝕓 (𝕤𝕦𝕓 (𝕒𝕝𝕘 t) σ) ς
    ≡⟨ 𝕥≈₁ 𝕥⟨𝕒⟩ ⟩
        𝕤𝕦𝕓 (𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ)) ς
    ≡⟨ 𝕥⟨𝕒⟩ ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) σ)) ς)
    ≡˘⟨ congr (str-nat₂ 𝕤𝕦𝕓 (⅀₁ 𝕤𝕦𝕓 t) σ) (λ - → 𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 - ς)) ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 (⅀.F₁ (λ { h ς → 𝕤𝕦𝕓 (h ς) }) (⅀₁ 𝕤𝕦𝕓 t)) σ) ς)
    ≡˘⟨ congr ⅀.homomorphism (λ - → 𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 - σ) ς)) ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 (⅀₁ (λ{ t σ → 𝕤𝕦𝕓 (𝕤𝕦𝕓 t σ)}) t) σ) ς)
    ∎ }
  ; g⟨𝑣⟩ = 𝕥⟨𝕧⟩
  ; g⟨𝑚⟩ = 𝕥⟨𝕞⟩
  ; g⟨𝑎⟩ = λ{ {σ = σ}{ς}{t} → begin
        𝕤𝕦𝕓 (𝕒𝕝𝕘 t) (λ v → 𝕤𝕦𝕓 (σ v) ς)
    ≡⟨ 𝕥⟨𝕒⟩ ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (⅀₁ 𝕤𝕦𝕓 t) (λ v → 𝕤𝕦𝕓 (σ v) ς))
    ≡⟨ cong 𝕒𝕝𝕘 (str-dist 𝕋 𝕤𝕦𝕓ᶜ (⅀₁ 𝕤𝕦𝕓 t) (λ {τ} z → σ z) ς) ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 (⅀.F₁ (precomp 𝕋 𝕤𝕦𝕓) (⅀₁ 𝕤𝕦𝕓 t)) σ) ς)
    ≡˘⟨ congr ⅀.homomorphism (λ - → 𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 - σ) ς)) ⟩
        𝕒𝕝𝕘 (str 𝕋ᴮ 𝕋 (str 𝕋ᴮ 〖 𝕋 , 𝕋 〗 (⅀₁ (λ{ t σ ς → 𝕤𝕦𝕓 t (λ v → 𝕤𝕦𝕓 (σ v) ς)}) t) σ) ς)
    ∎ }
  } where open ≡-Reasoning ; open Substitution

-- Coalgebraic monoid structure on 𝕋
𝕋ᵐ : Mon 𝕋
𝕋ᵐ = record
  { η = 𝕧𝕒𝕣
  ; μ = 𝕤𝕦𝕓
  ; lunit = Substitution.𝕥⟨𝕧⟩
  ; runit = λ{ {t = t} → trans (𝕥𝕣𝕒𝕧-η≈𝕤𝕖𝕞 𝕋ᴮ 𝕋ᵃ id refl) 𝕤𝕖𝕞-id }
  ; assoc = λ{ {t = t} → MapEq₂.≈ 𝕤𝕦𝕓-comp t }
  }

open Mon 𝕋ᵐ using ([_/] ; [_,_/]₂ ; lunit ; runit ; assoc) public

𝕋ᴹ : CoalgMon 𝕋
𝕋ᴹ = record { ᴮ = 𝕋ᴮ ; ᵐ = 𝕋ᵐ ; η-compat = refl ; μ-compat = λ{ {t = t} → compat t } }

-- Corollaries: renaming and simultaneous substitution commutes with
-- single-variable substitution
open import SOAS.ContextMaps.Combinators
𝕣𝕖𝕟[/] : (ρ : Γ ↝ Δ)(b : 𝕋 α (β ∙ Γ))(a : 𝕋 β Γ)
      → 𝕣𝕖𝕟 ([ a /] b) ρ ≡ [ (𝕣𝕖𝕟 a ρ) /] (𝕣𝕖𝕟 b (rlift _ ρ))
𝕣𝕖𝕟[/] ρ b a = begin
      𝕣𝕖𝕟 ([ a /] b) ρ
  ≡⟨ 𝕤𝕦𝕓ᶜ.r∘f ⟩
      𝕤𝕦𝕓 b (λ v → 𝕣𝕖𝕟 (add 𝕋 a 𝕧𝕒𝕣 v) ρ)
  ≡⟨ cong (𝕤𝕦𝕓 b) (dext (λ{ new → refl ; (old y) → Renaming.𝕥⟨𝕧⟩})) ⟩
      𝕤𝕦𝕓 b (λ v → add 𝕋 (𝕣𝕖𝕟  a ρ) 𝕧𝕒𝕣 (rlift _ ρ v))
  ≡˘⟨ 𝕤𝕦𝕓ᶜ.f∘r ⟩
      [ 𝕣𝕖𝕟 a ρ /] (𝕣𝕖𝕟 b (rlift _ ρ))
  ∎ where open ≡-Reasoning

𝕤𝕦𝕓[/] : (σ : Γ ~[ 𝕋 ]↝ Δ)(b : 𝕋 α (β ∙ Γ))(a : 𝕋 β Γ)
      → 𝕤𝕦𝕓 ([ a /] b) σ ≡ [ 𝕤𝕦𝕓 a σ /] (𝕤𝕦𝕓 b (lift 𝕋ᴮ ⌈ β ⌋ σ))
𝕤𝕦𝕓[/] {β = β} σ b a = begin
      𝕤𝕦𝕓 ([ a /] b) σ
  ≡⟨ assoc ⟩
      𝕤𝕦𝕓 b (λ v → 𝕤𝕦𝕓 (add 𝕋 a 𝕧𝕒𝕣 v) σ)
  ≡⟨ cong (𝕤𝕦𝕓 b) (dext (λ{ new → sym lunit ; (old v) → sym (begin
        𝕤𝕦𝕓 (𝕣𝕖𝕟 (σ v) old) (add 𝕋 (𝕤𝕦𝕓 a σ) 𝕧𝕒𝕣)
    ≡⟨ 𝕤𝕦𝕓ᶜ.f∘r ⟩
        𝕤𝕦𝕓 (σ v) (λ v → add 𝕋 (𝕤𝕦𝕓 a σ) 𝕧𝕒𝕣 (old v))
    ≡⟨ cong (𝕤𝕦𝕓 (σ v)) (dext (λ{ new → refl ; (old v) → refl})) ⟩
        𝕤𝕦𝕓 (σ v) 𝕧𝕒𝕣
    ≡⟨ runit ⟩
        σ v
    ≡˘⟨ lunit ⟩
        𝕤𝕦𝕓 (𝕧𝕒𝕣 v) σ
    ∎)})) ⟩
      𝕤𝕦𝕓 b (λ v → 𝕤𝕦𝕓 (lift 𝕋ᴮ ⌈ β ⌋ σ v) (add 𝕋 (𝕤𝕦𝕓 a σ) 𝕧𝕒𝕣))
  ≡˘⟨ assoc ⟩
      [ 𝕤𝕦𝕓 a σ /] (𝕤𝕦𝕓 b (lift 𝕋ᴮ ⌈ β ⌋ σ))
  ∎ where open ≡-Reasoning


text:
module BuiltinConstructorsNeededForLiterals where

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

{-# BUILTIN NATURAL Nat #-}

data ⊥ : Set where

empty : Nat → ⊥
empty (zero n) = empty n
empty (suc n) = empty n

bad : ⊥
bad = empty 0

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 --without-K #-}

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.WedgeExtension

module homotopy.Pi2HSusp where

module Pi2HSusp {i} (A : Type i) (gA : has-level ⟨ 1 ⟩ A)
  (cA : is-connected ⟨0⟩ A) (A-H : HSS A)
  (μcoh : HSS.μe- A-H (HSS.e A-H) == HSS.μ-e A-H (HSS.e A-H))
  where

  {- TODO this belongs somewhere else, but where? -}
  private
    Type=-ext : ∀ {i} {A B : Type i} (p q : A == B)
      → ((x : A) → coe p x == coe q x) → p == q
    Type=-ext p q α =
      ! (ua-η p)
      ∙ ap ua (pair= (λ= α) (prop-has-all-paths-↓ (is-equiv-is-prop (coe q))))
      ∙ ua-η q

  open HSpaceStructure A-H
  open ConnectedHSpace A cA A-H

  P : Suspension A → Type i
  P x = Trunc ⟨ 1 ⟩ (north A == x)

  module Codes = SuspensionRec A A A (λ a → ua (μ-equiv a))

  Codes : Suspension A → Type i
  Codes = Codes.f

  Codes-level : (x : Suspension A) → has-level ⟨ 1 ⟩ (Codes x)
  Codes-level = Suspension-elim A gA gA
    (λ _ → prop-has-all-paths-↓ has-level-is-prop)

  encode₀ : {x : Suspension A} → (north A == x) → Codes x
  encode₀ α = transport Codes α e

  encode : {x : Suspension A} → P x → Codes x
  encode {x} = Trunc-rec (Codes-level x) encode₀

  decode' : A → P (north A)
  decode' a = [ (merid A a ∙ ! (merid A e)) ]

  abstract
    transport-Codes-mer : (a a' : A)
      → transport Codes (merid A a) a' == μ a a'
    transport-Codes-mer a a' =
      coe (ap Codes (merid A a)) a'
        =⟨ Codes.glue-β a |in-ctx (λ w → coe w a') ⟩
      coe (ua (μ-equiv a)) a'
        =⟨ coe-β (μ-equiv a) a' ⟩
      μ a a' ∎

    transport-Codes-mer-e-! : (a : A)
      → transport Codes (! (merid A e)) a == a
    transport-Codes-mer-e-! a =
      coe (ap Codes (! (merid A e))) a
        =⟨ ap-! Codes (merid A e) |in-ctx (λ w → coe w a) ⟩
      coe (! (ap Codes (merid A e))) a
        =⟨ Codes.glue-β e |in-ctx (λ w → coe (! w) a) ⟩
      coe (! (ua (μ-equiv e))) a
        =⟨ Type=-ext (ua (μ-equiv e)) idp (λ x → coe-β _ x ∙ μe- x)
          |in-ctx (λ w → coe (! w) a) ⟩
      coe (! idp) a ∎

  abstract
    encode-decode' : (a : A) → encode (decode' a) == a
    encode-decode' a =
      transport Codes (merid A a ∙ ! (merid A e)) e
        =⟨ trans-∙ {B = Codes} (merid A a) (! (merid A e)) e ⟩
      transport Codes (! (merid A e)) (transport Codes (merid A a) e)
        =⟨ transport-Codes-mer a e ∙ μ-e a
          |in-ctx (λ w → transport Codes (! (merid A e)) w) ⟩
      transport Codes (! (merid A e)) a
        =⟨ transport-Codes-mer-e-! a ⟩
      a ∎

  abstract
    homomorphism : (a a' : A)
      → Path {A = Trunc ⟨ 1 ⟩ (north A == south A)}
        [ merid A (μ a a' ) ] [ merid A a' ∙ ! (merid A e) ∙ merid A a ]
    homomorphism = WedgeExt.ext args
      where
      args : WedgeExt.args {a₀ = e} {b₀ = e}
      args = record {m = ⟨-2⟩; n = ⟨-2⟩; cA = cA; cB = cA;
        P = λ a a' → (_ , Trunc-level {n = ⟨ 1 ⟩} _ _);
        f = λ a →  ap [_] $
              merid A (μ a e)
                =⟨ ap (merid A) (μ-e a) ⟩
              merid A a
                =⟨ ap (λ w → w ∙ merid A a) (! (!-inv-r (merid A e)))
                   ∙ ∙-assoc (merid A e) (! (merid A e)) (merid A a)  ⟩
              merid A e ∙ ! (merid A e) ∙ merid A a ∎;
        g = λ a' → ap [_] $
              merid A (μ e a')
                =⟨ ap (merid A) (μe- a') ⟩
              merid A a'
                =⟨ ! (∙-unit-r (merid A a'))
                   ∙ ap (λ w → merid A a' ∙ w) (! (!-inv-l (merid A e))) ⟩
              merid A a' ∙ ! (merid A e) ∙ merid A e ∎ ;
        p = ap (λ {(p₁ , p₂) → ap [_] $
              merid A (μ e e) =⟨ p₁ ⟩
              merid A e       =⟨ p₂ ⟩
              merid A e ∙ ! (merid A e) ∙ merid A e ∎})
             (pair×= (ap (λ x → ap (merid A) x) (! μcoh)) (coh (merid A e)))}
        where coh : {B : Type i} {b b' : B} (p : b == b')
                → ap (λ w → w ∙ p) (! (!-inv-r p)) ∙ ∙-assoc p (! p) p
                  == ! (∙-unit-r p) ∙ ap (λ w → p ∙ w) (! (!-inv-l p))
              coh idp = idp

  decode : {x : Suspension A} → Codes x → P x
  decode {x} = Suspension-elim A {P = λ x → Codes x → P x}
                 decode'
                 (λ a → [ merid A a ])
                 (λ a → ↓-→-from-transp (λ= $ STS a))
                 x
    where
    abstract
      STS : (a a' : A) → transport P (merid A a) (decode' a')
                         == [ merid A (transport Codes (merid A a) a') ]
      STS a a' =
        transport P (merid A a) [ merid A a' ∙ ! (merid A e) ]
          =⟨ transport-Trunc (λ x → north A == x) (merid A a) _ ⟩
        [ transport (λ x → north A == x) (merid A a) (merid A a' ∙ ! (merid A e)) ]
          =⟨ ap [_] (trans-pathfrom {A = Suspension A} (merid A a) _) ⟩
        [ (merid A a' ∙ ! (merid A e)) ∙ merid A a  ]
          =⟨ ap [_] (∙-assoc (merid A a') (! (merid A e)) (merid A a)) ⟩
        [ merid A a' ∙ ! (merid A e) ∙ merid A a  ]
          =⟨ ! (homomorphism a a') ⟩
        [ merid A (μ a a') ]
          =⟨ ap ([_] ∘ merid A) (! (transport-Codes-mer a a')) ⟩
        [ merid A (transport Codes (merid A a) a') ] ∎

  abstract
    decode-encode : {x : Suspension A} (tα : P x)
      → decode {x} (encode {x} tα) == tα
    decode-encode {x} = Trunc-elim
      {P = λ tα → decode {x} (encode {x} tα) == tα}
      (λ _ → =-preserves-level ⟨ 1 ⟩ Trunc-level)
      (J (λ y p → decode {y} (encode {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid A e))))

  main-lemma-eqv : Trunc ⟨ 1 ⟩ (north A == north A) ≃ A
  main-lemma-eqv = equiv encode decode' encode-decode' decode-encode

  ⊙main-lemma : ⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e))) == (A , e)
  ⊙main-lemma = ⊙ua main-lemma-eqv idp

  abstract
    main-lemma-iso : (t1 : 1 ≠ 0) →
         Ω^-Group 1 t1 (⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e)))) Trunc-level
      ≃ᴳ Ω^-Group 1 t1 (⊙Trunc ⟨ 1 ⟩ (A , e)) Trunc-level
    main-lemma-iso _ = (record {f = f; pres-comp = pres-comp} , ie)
      where
      h : fst (⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e)))
            ⊙→ ⊙Trunc ⟨ 1 ⟩ (A , e))
      h = (λ x → [ encode x ]) , idp

      f : Ω (⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e)))) → Ω (⊙Trunc ⟨ 1 ⟩ (A , e))
      f = fst (ap^ 1 h)

      pres-comp : (p q : Ω^ 1 (⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e)))))
        → f (conc^ 1 (ℕ-S≠O _) p q) == conc^ 1 (ℕ-S≠O _) (f p) (f q)
      pres-comp = ap^-conc^ 1 (ℕ-S≠O _) h

      ie : is-equiv f
      ie = is-equiv-ap^ 1 h (snd $ ((unTrunc-equiv A gA)⁻¹ ∘e main-lemma-eqv))

  abstract
    π₂-Suspension : (t1 : 1 ≠ 0) (t2 : 2 ≠ 0)
      → π 2 t2 (⊙Susp (A , e)) == π 1 t1 (A , e)
    π₂-Suspension t1 t2 =
      π 2 t2 (⊙Susp (A , e))
        =⟨ π-inner-iso 1 t1 t2 (⊙Susp (A , e)) ⟩
      π 1 t1 (⊙Ω (⊙Susp (A , e)))
        =⟨ ! (π-Trunc-shift-iso 1 t1 (⊙Ω (⊙Susp (A , e)))) ⟩
      Ω^-Group 1 t1 (⊙Trunc ⟨ 1 ⟩ (⊙Ω (⊙Susp (A , e)))) Trunc-level
        =⟨ group-ua (main-lemma-iso t1) ⟩
      Ω^-Group 1 t1 (⊙Trunc ⟨ 1 ⟩ (A , e)) Trunc-level
        =⟨ π-Trunc-shift-iso 1 t1 (A , e) ⟩
      π 1 t1 (A , e) ∎

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
open import Categories
open import Monads
open import Level
import Monads.CatofAdj

module Monads.CatofAdj.TermAdjHom
  {c d}
  {C : Cat {c}{d}}
  (M : Monad C)
  (A : Cat.Obj (Monads.CatofAdj.CatofAdj M {c ⊔ d}{c ⊔ d})) where

open import Library

open import Functors
open import Adjunctions
open import Monads.EM M
open Monads.CatofAdj M
open import Monads.CatofAdj.TermAdjObj M

open Cat
open Fun
open Adj
open Monad

open ObjAdj

K' : Fun (D A) (D EMObj)
K' = record {
    OMap  = λ X → record {
      acar  = OMap (R (adj A)) X;
      astr  = λ Z f → subst (λ Z → Hom C Z (OMap (R (adj A)) X))
                            (fcong Z (cong OMap (law A)))
                            (HMap (R (adj A)) (right (adj A) f));
      alaw1 = λ {Z} {f} → alaw1lem
         (TFun M)
         (L (adj A))
         (R (adj A))
         (law A)
         (η M)
         (right (adj A))
         (left (adj A))
         (ηlaw A)
         (natleft (adj A) (iden C) (right (adj A) f) (iden (D A)))
         (lawb (adj A) f);
      alaw2 = λ {Z} {W} {k} {f} → alaw2lem
         (TFun M)
         (L (adj A))
         (R (adj A))
         (law A)
         (right (adj A))
         (bind M)
         (natright (adj A))
         (bindlaw A {_}{_}{k})};
    HMap  = λ {X} {Y} f → record {
      amor = HMap (R (adj A)) f;
      ahom = λ {Z} {g} → ahomlem
         (TFun M)
         (L (adj A))
         (R (adj A))
         (law A)
         (right (adj A))
         (natright (adj A))};
    fid   = AlgMorphEq (fid (R (adj A)));
    fcomp = AlgMorphEq (fcomp (R (adj A)))}

Llaw' : K' ○ L (adj A) ≅ L (adj EMObj)
Llaw' = FunctorEq
  _
  _
  (ext (λ X → AlgEq
    (fcong X (cong OMap (law A)))
    ((ext λ Z → dext (λ {f} {f'} p → Llawlem
      (TFun M)
      (L (adj A))
      (R (adj A))
      (law A)
      (right (adj A))
      (bind M)
      (bindlaw A)
      p)))))
  (iext λ X → iext λ Y → ext λ f → AlgMorphEq'
    (AlgEq
      (fcong X (cong OMap (law A)))
      ((ext λ Z → dext (λ {f₁} {f'} p → Llawlem
        (TFun M)
        (L (adj A))
        (R (adj A))
        (law A)
        (right (adj A))
        (bind M)
        (bindlaw A)
        p))))
    (AlgEq
      (fcong Y (cong OMap (law A)))
      ((ext λ Z → dext (λ {f₁} {f'} p → Llawlem
        (TFun M)
        (L (adj A))
        (R (adj A))
        (law A)
        (right (adj A))
        (bind M)
        (bindlaw A)
        p))))
    (dcong
      (refl {x = f})
      (ext (λ _ → cong₂
        (Hom C)
        (fcong X (cong OMap (law A)))
        (fcong Y (cong OMap (law A)))))
      (dicong
        (refl {x = Y})
        (ext (λ z → cong
          (λ F → Hom C X z → Hom C (F X) (F z))
          (cong OMap (law A))))
        (dicong
          (refl {x = X})
          (ext (λ z → cong
            (λ F → ∀ {y} → Hom C z y → Hom C (F z) (F y))
            (cong OMap (law A))))
          (cong HMap (law A))))))

Rlaw' : R (adj A) ≅ R (adj EMObj) ○ K'
Rlaw' = FunctorEq _ _ refl refl

rightlaw' : {X : Obj C} {Y : Obj (D A)} {f : Hom C X (OMap (R (adj A)) Y)} →
            HMap K' (right (adj A) f)
            ≅
            right (adj EMObj)
                  {X}
                  {OMap K' Y}
                  (subst (Hom C X) (fcong Y (cong OMap Rlaw')) f)
rightlaw' {X = X}{Y = Y}{f = f} = AlgMorphEq'
  (AlgEq (fcong X (cong OMap (law A)))
         (ext λ Z → dext (λ p → Llawlem (TFun M)
           (L (adj A))
           (R (adj A))
           (law A)
           (right (adj A))
           (bind M)
           (bindlaw A) p )))
  refl
  (trans (cong  (λ (f₁ : Hom C X (OMap (R (adj A)) Y)) →
           HMap (R (adj A)) (right (adj A) f₁)) (sym (stripsubst (Hom C X) f (fcong Y (cong OMap Rlaw')))) ) (sym (stripsubst (λ Z → Hom C Z (OMap (R (adj A)) Y)) ( ((HMap (R (adj A))
 (right (adj A)
   (subst (Hom C X) (fcong Y (cong (λ r → OMap r) Rlaw')) f))))) (fcong X (cong OMap (law A))))))

EMHom : Hom CatofAdj A EMObj
EMHom = record {
  K        = K';
  Llaw     = Llaw';
  Rlaw     = Rlaw';
  rightlaw = rightlaw'}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

open import lib.Base
open import lib.PathFunctor
open import lib.PathGroupoid
open import lib.Equivalence

{- Structural lemmas about paths over paths

The lemmas here have the form
[↓-something-in]  : introduction rule for the something
[↓-something-out] : elimination  rule for the something
[↓-something-β]   : β-reduction  rule for the something
[↓-something-η]   : η-reduction  rule for the something

The possible somethings are:
[cst] : constant fibration
[cst2] : fibration constant in the second argument
[cst2×] : fibration constant and nondependent in the second argument
[ap] : the path below is of the form [ap f p]
[fst×] : the fibration is [fst] (nondependent product)
[snd×] : the fibration is [snd] (nondependent product)

The rule of prime: The above lemmas should choose
between [_∙_] and [_∙'_] in a way that, if the underlying path is [idp],
then the entire lemma reduces to an identity function.
Otherwise, the lemma would have the suffix [in'] or [out'], meaning that
all the choices of [_∙_] or [_∙'_] are exactly the opposite ones.

You can also go back and forth between dependent paths and homogeneous paths
with a transport on one side with the functions
[to-transp],  [from-transp],  [to-transp-β]
[to-transp!], [from-transp!], [to-transp!-β]

More lemmas about paths over paths are present in the lib.types.* modules
(depending on the type constructor of the fibration)
-}

module lib.PathOver where

{- Dependent paths in a constant fibration -}
module _ {i j} {A : Type i} {B : Type j} where

  ↓-cst-in : {x y : A} {p : x == y} {u v : B}
    → u == v
    → u == v [ (λ _ → B) ↓ p ]
  ↓-cst-in {p = idp} q = q

  ↓-cst-out : {x y : A} {p : x == y} {u v : B}
    → u == v [ (λ _ → B) ↓ p ]
    → u == v
  ↓-cst-out {p = idp} q = q

  ↓-cst-β : {x y : A} (p : x == y) {u v : B} (q : u == v)
    → (↓-cst-out (↓-cst-in {p = p} q) == q)
  ↓-cst-β idp q = idp

  {- Interaction of [↓-cst-in] with [_∙_] -}
  ↓-cst-in-∙ : {x y z : A} (p : x == y) (q : y == z) {u v w : B}
    (p' : u == v) (q' : v == w)
    → ↓-cst-in {p = p ∙ q} (p' ∙ q')
      == ↓-cst-in {p = p} p' ∙ᵈ ↓-cst-in {p = q} q'
  ↓-cst-in-∙ idp idp idp idp = idp

  {- Interaction of [↓-cst-in] with [_∙'_] -}
  ↓-cst-in-∙' : {x y z : A} (p : x == y) (q : y == z) {u v w : B}
    (p' : u == v) (q' : v == w)
    → ↓-cst-in {p = p ∙' q} (p' ∙' q')
      == ↓-cst-in {p = p} p' ∙'ᵈ ↓-cst-in {p = q} q'
  ↓-cst-in-∙' idp idp idp idp = idp

  {- Introduction of an equality between [↓-cst-in]s (used to deduce the
     recursor from the eliminator in HIT with 2-paths) -}
  ↓-cst-in2 : {a a' : A} {u v : B}
    {p₀ : a == a'} {p₁ : a == a'} {q₀ q₁ : u == v} {q : p₀ == p₁}
    → q₀ == q₁
    → (↓-cst-in {p = p₀} q₀ == ↓-cst-in {p = p₁} q₁ [ (λ p → u == v [ (λ _ → B) ↓ p ]) ↓ q ])
  ↓-cst-in2 {p₀ = idp} {p₁ = .idp} {q₀} {q₁} {idp} k = k

-- Dependent paths in a fibration constant in the second argument
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where

  ↓-cst2-in : {x y : A} (p : x == y) {b : C x} {c : C y}
    (q : b == c [ C ↓ p ]) {u : B x} {v : B y}
    → u == v [ B ↓ p ]
    → u == v [ (λ xy → B (fst xy)) ↓ (pair= p q) ]
  ↓-cst2-in idp idp r = r

  ↓-cst2-out : {x y : A} (p : x == y) {b : C x} {c : C y}
    (q : b == c [ C ↓ p ]) {u : B x} {v : B y}
    → u == v [ (λ xy → B (fst xy)) ↓ (pair= p q) ]
    → u == v [ B ↓ p ]
  ↓-cst2-out idp idp r = r

-- Dependent paths in a fibration constant and non dependent in the
-- second argument
module _ {i j k} {A : Type i} {B : A → Type j} {C : Type k} where

  ↓-cst2×-in : {x y : A} (p : x == y) {b c : C}
    (q : b == c) {u : B x} {v : B y}
    → u == v [ B ↓ p ]
    → u == v [ (λ xy → B (fst xy)) ↓ (pair×= p q) ]
  ↓-cst2×-in idp idp r = r

  ↓-cst2×-out : {x y : A} (p : x == y) {b c : C}
    (q : b == c) {u : B x} {v : B y}
    → u == v [ (λ xy → B (fst xy)) ↓ (pair×= p q) ]
    → u == v [ B ↓ p ]
  ↓-cst2×-out idp idp r = r

-- Dependent paths in the universal fibration over the universe
↓-idf-out : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
  → u == v [ (λ x → x) ↓ p ]
  → coe p u == v
↓-idf-out idp = idf _

↓-idf-in : ∀ {i} {A B : Type i} (p : A == B) {u : A} {v : B}
  → coe p u == v
  → u == v [ (λ x → x) ↓ p ]
↓-idf-in idp = idf _

-- Dependent paths over [ap f p]
module _ {i j k} {A : Type i} {B : Type j} (C : B → Type k) (f : A → B) where

  ↓-ap-in : {x y : A} {p : x == y} {u : C (f x)} {v : C (f y)}
    → u == v [ C ∘ f ↓ p ]
    → u == v [ C ↓ ap f p ]
  ↓-ap-in {p = idp} idp = idp

  ↓-ap-out : {x y : A} (p : x == y) {u : C (f x)} {v : C (f y)}
    → u == v [ C ↓ ap f p ]
    → u == v [ C ∘ f ↓ p ]
  ↓-ap-out idp idp = idp

-- Dependent paths over [ap2 f p q]
module _ {i j k l} {A : Type i} {B : Type j} {C : Type k} (D : C → Type l)
  (f : A → B → C) where

  ↓-ap2-in : {x y : A} {p : x == y} {w z : B} {q : w == z}
    {u : D (f x w)} {v : D (f y z)}
    → u == v [ D ∘ uncurry f ↓ pair×= p q ]
    → u == v [ D ↓ ap2 f p q ]
  ↓-ap2-in {p = idp} {q = idp} α = α

  ↓-ap2-out : {x y : A} {p : x == y} {w z : B} {q : w == z}
    {u : D (f x w)} {v : D (f y z)}
    → u == v [ D ↓ ap2 f p q ]
    → u == v [ D ∘ uncurry f ↓ pair×= p q ]
  ↓-ap2-out {p = idp} {q = idp} α = α

apd↓ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → B a → Type k}
  (f : {a : A} (b : B a) → C a b) {x y : A} {p : x == y}
  {u : B x} {v : B y} (q : u == v [ B ↓ p ])
  → f u == f v [ (λ xy → C (fst xy) (snd xy)) ↓ pair= p q ]
apd↓ f {p = idp} idp = idp

apd↓=apd :  ∀ {i j} {A : Type i} {B : A → Type j} (f : (a : A) → B a) {x y : A}
  (p : x == y) → (apd f p == ↓-ap-out _ _ p (apd↓ {A = Unit} f {p = idp} p))
apd↓=apd f idp = idp

-- Paths in the fibrations [fst] and [snd]
module _ {i j} where

  ↓-fst×-out : {A A' : Type i} {B B' : Type j} (p : A == A') (q : B == B')
    {u : A} {v : A'}
    → u == v [ fst ↓ pair×= p q ]
    → u == v [ (λ X → X) ↓ p ]
  ↓-fst×-out idp idp h = h

  ↓-snd×-in : {A A' : Type i} {B B' : Type j} (p : A == A') (q : B == B')
    {u : B} {v : B'}
    → u == v [ (λ X → X) ↓ q ]
    → u == v [ snd ↓ pair×= p q ]
  ↓-snd×-in idp idp h = h

-- Mediating dependent paths with the transport version

module _ {i j} {A : Type i} where

  from-transp : (B : A → Type j) {a a' : A} (p : a == a')
    {u : B a} {v : B a'}
    → (transport B p u == v)
    → (u == v [ B ↓ p ])
  from-transp B idp idp = idp

  to-transp : {B : A → Type j} {a a' : A} {p : a == a'}
    {u : B a} {v : B a'}
    → (u == v [ B ↓ p ])
    → (transport B p u == v)
  to-transp {p = idp} idp = idp

  to-transp-β : (B : A → Type j) {a a' : A} (p : a == a')
    {u : B a} {v : B a'}
    (q : transport B p u == v)
    → to-transp (from-transp B p q) == q
  to-transp-β B idp idp = idp

  to-transp-η : {B : A → Type j} {a a' : A} {p : a == a'}
    {u : B a} {v : B a'}
    (q : u == v [ B ↓ p ])
    → from-transp B p (to-transp q) == q
  to-transp-η {p = idp} idp = idp

  to-transp-equiv : (B : A → Type j) {a a' : A} (p : a == a')
    {u : B a} {v : B a'} → (u == v [ B ↓ p ]) ≃ (transport B p u == v)
  to-transp-equiv B p =
    equiv to-transp (from-transp B p) (to-transp-β B p) (to-transp-η)

  from-transp! : (B : A → Type j)
    {a a' : A} (p : a == a')
    {u : B a} {v : B a'}
    → (u == transport! B p v)
    → (u == v [ B ↓ p ])
  from-transp! B idp idp = idp

  to-transp! : {B : A → Type j}
    {a a' : A} {p : a == a'}
    {u : B a} {v : B a'}
    → (u == v [ B ↓ p ])
    → (u == transport! B p v)
  to-transp! {p = idp} idp = idp

  to-transp!-β : (B : A → Type j)
    {a a' : A} (p : a == a')
    {u : B a} {v : B a'}
    (q : u == transport! B p v)
    → to-transp! (from-transp! B p q) == q
  to-transp!-β B idp idp = idp

  to-transp!-η : {B : A → Type j} {a a' : A} {p : a == a'}
    {u : B a} {v : B a'}
    (q : u == v [ B ↓ p ])
    → from-transp! B p (to-transp! q) == q
  to-transp!-η {p = idp} idp = idp

  to-transp!-equiv : (B : A → Type j) {a a' : A} (p : a == a')
    {u : B a} {v : B a'} → (u == v [ B ↓ p ]) ≃ (u == transport! B p v)
  to-transp!-equiv B p =
    equiv to-transp! (from-transp! B p) (to-transp!-β B p) (to-transp!-η)

{- Various other lemmas -}

{- Used for defining the recursor from the eliminator for 1-HIT -}
apd=cst-in : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a a' : A} {p : a == a'} {q : f a == f a'}
  → apd f p == ↓-cst-in q → ap f p == q
apd=cst-in {p = idp} x = x

↓-apd-out : ∀ {i j k} {A : Type i} {B : A → Type j} (C : (a : A) → B a → Type k)
  {f : Π A B} {x y : A} {p : x == y}
  {q : f x == f y [ B ↓ p ]} (r : apd f p == q)
  {u : C x (f x)} {v : C y (f y)}
  → u == v [ uncurry C ↓ pair= p q ]
  → u == v [ (λ z → C z (f z)) ↓ p ]
↓-apd-out C {p = idp} idp idp = idp

↓-ap-out= : ∀ {i j k} {A : Type i} {B : Type j} (C : (b : B) → Type k)
  (f : A → B) {x y : A} (p : x == y)
  {q : f x == f y} (r : ap f p == q)
  {u : C (f x)} {v : C (f y)}
  → u == v [ C ↓ q ]
  → u == v [ (λ z → C (f z)) ↓ p ]
↓-ap-out= C f idp idp idp = idp

-- No idea what that is
to-transp-weird : ∀ {i j} {A : Type i} {B : A → Type j}
  {u v : A} {d : B u} {d' d'' : B v} {p : u == v}
  (q : d == d' [ B ↓ p ]) (r : transport B p d == d'')
  → (from-transp B p r ∙'ᵈ (! r ∙ to-transp q)) == q
to-transp-weird {p = idp} idp idp = idp

-- Something not really clear yet
module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → C) (g : B → C)
  where

  ↓-swap : {a a' : A} {p : a == a'} {b b' : B} {q : b == b'}
    (r : f a == g b') (s : f a' == g b)
    → (ap f p ∙' s == r [ (λ x → f a == g x)  ↓ q ])
    → (r == s ∙ ap g q  [ (λ x → f x == g b') ↓ p ])
  ↓-swap {p = idp} {q = idp} r s t = (! t) ∙ ∙'-unit-l s ∙ ! (∙-unit-r s)

  ↓-swap! : {a a' : A} {p : a == a'} {b b' : B} {q : b == b'}
    (r : f a == g b') (s : f a' == g b)
    → (r == s ∙ ap g q  [ (λ x → f x == g b') ↓ p ])
    → (ap f p ∙' s == r [ (λ x → f a == g x)  ↓ q ])
  ↓-swap! {p = idp} {q = idp} r s t = ∙'-unit-l s ∙ ! (∙-unit-r s) ∙ (! t)

  ↓-swap-β : {a a' : A} {p : a == a'} {b b' : B} {q : b == b'}
    (r : f a == g b') (s : f a' == g b)
    (t : ap f p ∙' s == r [ (λ x → f a == g x) ↓ q ])
    → ↓-swap! r s (↓-swap r s t) == t
  ↓-swap-β {p = idp} {q = idp} r s t = coh (∙'-unit-l s) (∙-unit-r s) t  where

    coh : ∀ {i} {X : Type i} {x y z t : X} (p : x == y) (q : z == y) (r : x == t)
      → p ∙ ! q ∙ ! (! r ∙ p ∙ ! q) == r
    coh idp idp idp = idp

transp-↓ : ∀ {i j} {A : Type i} (P : A → Type j) {a₁ a₂ : A}
  (p : a₁ == a₂) (y : P a₂) → transport P (! p) y == y [ P ↓ p ]
transp-↓ _ idp _ = idp

transp-ap-↓ : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k) (h : A → B)
  {a₁ a₂ : A} (p : a₁ == a₂) (y : P (h a₂))
  → transport P (! (ap h p)) y == y [ P ∘ h ↓ p ]
transp-ap-↓ _ _ idp _ = idp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda