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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Unit.Base
open import Cubical.Data.Prod.Base

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

isContrUnit : isContr Unit
isContrUnit = tt , λ {tt → refl}

isPropUnit : isProp Unit
isPropUnit _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit

isSetUnit : isSet Unit
isSetUnit = isProp→isSet isPropUnit

isOfHLevelUnit : (n : HLevel) → isOfHLevel n Unit
isOfHLevelUnit n = isContr→isOfHLevel n isContrUnit

diagonal-unit : Unit ≡ Unit × Unit
diagonal-unit = isoToPath (iso (λ x → tt , tt) (λ x → tt) (λ {(tt , tt) i → tt , tt}) λ {tt i → tt})

fibId : ∀ {ℓ} (A : Type ℓ) → (fiber (λ (x : A) → tt) tt) ≡ A
fibId A = isoToPath
            (iso fst
                 (λ a → a , refl)
                 (λ _ → refl)
                 (λ a i → fst a
                         , isOfHLevelSuc 1 isPropUnit _ _ (snd a) refl i))

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.PropositionalTruncation.Base
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

private
  variable
    ℓA ℓA' ℓ ℓ' ℓ≅A ℓ≅A' ℓB : Level

-- Rel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
-- Rel A B ℓ' = A → B → Type ℓ'

Rel : (A : Type ℓA) (B : Type ℓB) (ℓ : Level) → Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓA ℓB))
Rel A B ℓ = A → B → Type ℓ

PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)

idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
idPropRel A .fst a a' = ∥ a ≡ a' ∥
idPropRel A .snd _ _ = squash

invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
  → PropRel A B ℓ' → PropRel B A ℓ'
invPropRel R .fst b a = R .fst a b
invPropRel R .snd b a = R .snd a b

compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
  → PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
compPropRel R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥
compPropRel R S .snd _ _ = squash

graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
graphRel f a b = f a ≡ b

module _ {ℓ ℓ' : Level} {A : Type ℓ} (_R_ : Rel A A ℓ') where
  -- R is reflexive
  isRefl : Type (ℓ-max ℓ ℓ')
  isRefl = (a : A) → a R a

  -- R is symmetric
  isSym : Type (ℓ-max ℓ ℓ')
  isSym = (a b : A) → a R b → b R a

  -- R is transitive
  isTrans : Type (ℓ-max ℓ ℓ')
  isTrans = (a b c : A)  → a R b → b R c → a R c

  record isEquivRel : Type (ℓ-max ℓ ℓ') where
    constructor equivRel
    field
      reflexive : isRefl
      symmetric : isSym
      transitive : isTrans

  isPropValued : Type (ℓ-max ℓ ℓ')
  isPropValued = (a b : A) → isProp (a R b)

  isEffective : Type (ℓ-max ℓ ℓ')
  isEffective =
    (a b : A) → isEquiv (eq/ {R = _R_} a b)

  -- the total space corresponding to the binary relation w.r.t. a
  relSinglAt : (a : A) → Type (ℓ-max ℓ ℓ')
  relSinglAt a = Σ[ a' ∈ A ] (a R a')

  -- the statement that the total space is contractible at any a
  contrRelSingl : Type (ℓ-max ℓ ℓ')
  contrRelSingl = (a : A) → isContr (relSinglAt a)

  -- assume a reflexive binary relation
  module _ (ρ : isRefl) where
    -- identity is the least reflexive relation
    ≡→R : {a a' : A} → a ≡ a' → a R a'
    -- ≡→R {a} {a'} p = subst (λ z → a R z) p (ρ a)
    ≡→R {a} {a'} p = J (λ z q → a R z) (ρ a) p

    -- what it means for a reflexive binary relation to be univalent
    isUnivalent : Type (ℓ-max ℓ ℓ')
    isUnivalent = (a a' : A) → isEquiv (≡→R {a} {a'})

    -- helpers for contrRelSingl→isUnivalent
    private
      module _ (a : A) where
        -- wrapper for ≡→R
        f = λ (a' : A) (p : a ≡ a') → ≡→R {a} {a'} p

        -- the corresponding total map that univalence
        -- of R will be reduced to
        totf : singl a → Σ[ a' ∈ A ] (a R a')
        totf (a' , p) = (a' , f a' p)

    -- if the total space corresponding to R is contractible
    -- then R is univalent
    -- because the singleton at a is also contractible
    contrRelSingl→isUnivalent : contrRelSingl → isUnivalent
    contrRelSingl→isUnivalent c a = q
      where
        abstract
          q = fiberEquiv (λ a' → a ≡ a')
                   (λ a' → a R a')
                   (f a)
                   (snd (propBiimpl→Equiv (isContr→isProp (isContrSingl a))
                                           (isContr→isProp (c a))
                                           (totf a)
                                           (λ _ → fst (isContrSingl a))))

    -- converse map. proof idea:
    -- equivalences preserve contractability,
    -- singletons are contractible
    -- and by the univalence assumption the total map is an equivalence
    isUnivalent→contrRelSingl : isUnivalent → contrRelSingl
    isUnivalent→contrRelSingl u a = q
      where
        abstract
          q = isContrRespectEquiv
                               (totf a , totalEquiv (a ≡_)
                                                    (a R_)
                                                    (f a)
                                                    λ a' → u a a')
                               (isContrSingl a)

    isUnivalent' : Type (ℓ-max ℓ ℓ')
    isUnivalent' = (a a' : A) → (a ≡ a') ≃ a R a'

    private
      module _ (e : isUnivalent') (a : A) where
        -- wrapper for ≡→R
        g = λ (a' : A) (p : a ≡ a') → e a a' .fst p

        -- the corresponding total map that univalence
        -- of R will be reduced to
        totg : singl a → Σ[ a' ∈ A ] (a R a')
        totg (a' , p) = (a' , g a' p)

      isUnivalent'→contrRelSingl : isUnivalent' → contrRelSingl
      isUnivalent'→contrRelSingl u a = q
        where
          abstract
            q = isContrRespectEquiv
                                 (totg u a , totalEquiv (a ≡_) (a R_) (g u a) λ a' → u a a' .snd)
                                 (isContrSingl a)

    isUnivalent'→isUnivalent : isUnivalent' → isUnivalent
    isUnivalent'→isUnivalent u = contrRelSingl→isUnivalent (isUnivalent'→contrRelSingl u)

    isUnivalent→isUnivalent' : isUnivalent → isUnivalent'
    isUnivalent→isUnivalent' u a a' = ≡→R {a} {a'} , u a a'

record RelIso {A : Type ℓA} (_≅_ : Rel A A ℓ≅A)
              {A' : Type ℓA'} (_≅'_ : Rel A' A' ℓ≅A') : Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A')) where
  constructor reliso
  field
    fun : A → A'
    inv : A' → A
    rightInv : (a' : A') → fun (inv a') ≅' a'
    leftInv : (a : A) → inv (fun a) ≅ a

RelIso→Iso : {A : Type ℓA} {A' : Type ℓA'}
             (_≅_ : Rel A A ℓ≅A) (_≅'_ : Rel A' A' ℓ≅A')
             {ρ : isRefl _≅_} {ρ' : isRefl _≅'_}
             (uni : isUnivalent _≅_ ρ) (uni' : isUnivalent _≅'_ ρ')
             (f : RelIso _≅_ _≅'_)
             → Iso A A'
Iso.fun (RelIso→Iso _ _ _ _ f) = RelIso.fun f
Iso.inv (RelIso→Iso _ _ _ _ f) = RelIso.inv f
Iso.rightInv (RelIso→Iso _ _≅'_ {ρ' = ρ'} _ uni' f) a'
  = invEquiv (≡→R _≅'_ ρ' , uni' (RelIso.fun f (RelIso.inv f a')) a') .fst (RelIso.rightInv f a')
Iso.leftInv (RelIso→Iso _≅_ _ {ρ = ρ} uni _ f) a
  = invEquiv (≡→R _≅_ ρ , uni (RelIso.inv f (RelIso.fun f a)) a) .fst (RelIso.leftInv f a)

EquivRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] isEquivRel R

EquivPropRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivPropRel A ℓ' = Σ[ R ∈ PropRel A A ℓ' ] isEquivRel (R .fst)

ext: agda

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

module Number.Bundles2 where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
-- open import Cubical.Foundations.Logic
-- open import Cubical.Structures.Ring
-- open import Cubical.Structures.Group
-- open import Cubical.Structures.AbGroup

open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_)

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Consequences
open import Number.Structures2

{-
| name | struct              | apart | abs | order | cauchy | sqrt₀⁺  | exp | final name                                                             |
|------|---------------------|-------|-----|-------|--------|---------|-----|------------------------------------------------------------------------|
| ℕ    | CommSemiring        |  (✓)  | (✓) | lin.  |        | (on x²) |     | LinearlyOrderedCommSemiring                                            |
| ℤ    | CommRing            |  (✓)  | (✓) | lin.  |        | (on x²) |     | LinearlyOrderedCommRing                                                |
| ℚ    | Field               |  (✓)  | (✓) | lin.  |        | (on x²) | (✓) | LinearlyOrderedField                                                   |
| ℝ    | Field               |  (✓)  | (✓) | part. |   ✓    |    ✓    | (✓) | CompletePartiallyOrderedFieldWithSqrt                                  |
| ℂ    | euclidean 2-Product |  (✓)  | (✓) |       |  (✓)   |         |  ?  | EuclideanTwoProductOfCompletePartiallyOrderedFieldWithSqrt             |
| R    | Ring                |   ✓   |  ✓  |       |        |         |  ?  | ApartnessRingWithAbsIntoCompletePartiallyOrderedFieldWithSqrt          |
| G    | Group               |   ✓   |  ✓  |       |        |         |  ?  | ApartnessGroupWithAbsIntoCompletePartiallyOrderedFieldWithSqrt         |
| K    | Field               |   ✓   |  ✓  |       |   ✓    |         |  ?  | CompleteApartnessFieldWithAbsIntoCompletePartiallyOrderedFieldWithSqrt |
-}

record LinearlyOrderedCommSemiring {ℓ ℓ'} : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor linearlyorderedcommsemiring
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
    is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0f 1f _+_ _·_ _<_ min max ] -- defines `_≤_` and `_#_`

  infixl 7 _·_
  infixl 5 _+_
  infixl 4 _<_

  open IsLinearlyOrderedCommSemiring is-LinearlyOrderedCommSemiring public

record LinearlyOrderedCommRing {ℓ ℓ'} : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor linearlyorderedcommring
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
    is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max ] -- defines `_≤_` and `_#_`

  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _<_

  open IsLinearlyOrderedCommRing is-LinearlyOrderedCommRing public

record LinearlyOrderedField {ℓ ℓ'} : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor linearlyorderedfield
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
    is-LinearlyOrderedField : [ isLinearlyOrderedField 0f 1f _+_ _·_ -_ _<_ min max ] -- defines `_≤_` and `_#_`

  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _<_

  open IsLinearlyOrderedField is-LinearlyOrderedField public

-- NOTE: this smells like "CPO" https://en.wikipedia.org/wiki/Complete_partial_order
record CompletePartiallyOrderedFieldWithSqrt {ℓ ℓ' : Level} : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier : Type ℓ
    is-set   : isSet Carrier
    0f      : Carrier
    1f      : Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
    min     : Carrier → Carrier → Carrier
    max     : Carrier → Carrier → Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    <-irrefl  : [ isIrrefl   _<_ ]
    <-trans   : [ isTrans    _<_ ]
    <-cotrans : [ isCotrans  _<_ ]

  -- NOTE: these intermediate definitions are restricted and behave like let-definitions
  --       e.g. they show up in goal contexts and they do not allow for `where` blocks

  _-_ : Carrier → Carrier → Carrier
  a - b = a + (- b)

  <-asym : [ isAsym  _<_ ]
  <-asym = irrefl+trans⇒asym _<_ <-irrefl <-trans

  _#_ : hPropRel Carrier Carrier ℓ'
  x # y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)

  field
    #-tight : [ isTightˢ''' _#_ is-set ]

  _≤_ : hPropRel Carrier Carrier ℓ'
  x ≤ y = ¬ᵖ(y < x)

  _>_ = flip _<_
  _≥_ = flip _≤_

  ≤-refl : [ isRefl _≤_ ]
  ≤-refl = <-irrefl

  ≤-trans : [ isTrans  _≤_ ]
  ≤-trans = <-cotrans⇒≤-trans _<_ <-cotrans

  -- if x > y then x > y ≥ x, wich contradicts 4. Hence ¬(x > y). Similarly, ¬(y > x), so ¬(x ≠ y) and therefore by axiom R2(3), x = y.
  -- NOTE: this makes use of #-tight to proof ≤-antisym
  --       but we are alrady using ≤-antisym to proof #-tight
  --       so I guess that we have to assume one of them?
  --       Bridges lists tightness a property of _<_, so he seems to assume #-tight
  --       Booij assumes `≤-isLattice : IsLattice _≤_ min max` which gives ≤-refl, ≤-antisym and ≤-trans and proofs #-tight from it
  -- ≤-antisym : (∀ x y → [ ¬ᵖ (x # y) ] → x ≡ y) → [ isAntisymˢ is-set _≤_ ]
  ≤-antisym : [ isAntisymˢ _≤_ is-set ]
  ≤-antisym = fst (isTightˢ'''⇔isAntisymˢ _<_ is-set <-asym) #-tight

  -- NOTE: we have `R3-8 = ∀[ x ] ∀[ y ] (¬(x ≤ y) ⇔ ¬ ¬(y < x))`
  --       so I guess that we do not have `dne-over-< : ¬ ¬(y < x) ⇔ (y < x)`
  --       and that would be my plan to prove `≤-cotrans` with `<-asym`
  -- ≤-cotrans : [ isCotrans  _≤_ ]
  -- ≤-cotrans x y x≤y z = [ (x ≤ z) ⊔ (z ≤ y) ] ∋  {! (≤-antisym x y x≤y)  !}

  abs : Carrier → Carrier
  abs x = max x (- x)

  field
    -- `R3.12` in [Bridges 1999]
    -- bridges-R2-2  : ∀ x y → [ y < x ] → ∀ z → [ (z < x) ⊔ (y < z) ]
    sqrt : (x : Carrier) → {{ ! [ 0f ≤ x ] }} → Carrier
    0≤sqrt : ∀ x → {{ p : ! [ 0f ≤ x ] }} → [ 0f ≤ sqrt x {{p}} ]
    0≤x² : ∀ x → [ 0f ≤ (x · x) ]

  instance _ = λ {x} → !! 0≤x² x

  field
    -- NOTE: all "interface" instance arguments (i.e. those that appear in the goal) need to be passed in as arguments
    -- sqrt-of-²  : ∀ x → {{ p₁ : ! [ 0f ≤ x ] }} → {{ p₂ : ! [ 0f ≤ x · x ] }} → sqrt (x · x) {{p₂}} ≡ x
    -- sqrt-unique-existence : ∀ x → {{ p : ! [ 0f ≤ x ] }} → Σ[ y ∈ Carrier ] y · y ≡ x
    -- sqrt-uniqueness : ∀ x y z → {{ p : ! [ 0f ≤ x ] }} → y · y ≡ x → z · z ≡ x → y ≡ z
    ·-uniqueness : ∀ x y → {{ p₁ : ! [ 0f ≤ x ] }} → {{ p₂ : ! [ 0f ≤ y ] }} → x · x ≡ y · y → x ≡ y
    sqrt-existence   : ∀ x   → {{ p  : ! [ 0f ≤ x ] }} → sqrt x {{p}} · sqrt x {{p}} ≡ x
    sqrt-preserves-· : ∀ x y → {{ p₁ : ! [ 0f ≤ x ] }} → {{ p₁ : ! [ 0f ≤ y ] }} → {{ p₁ : ! [ 0f ≤ x · y ] }} → sqrt (x · y) ≡ sqrt x · sqrt y
    sqrt0≡0 : {{ p : ! [ 0f ≤ 0f ] }} → sqrt 0f {{p}} ≡ 0f
    sqrt1≡1 : {{ p : ! [ 0f ≤ 1f ] }} → sqrt 1f {{p}} ≡ 1f
    -- √x √x = x ⇒ √xx = x
    -- √x √x √x √x = x x
    -- √(√x √x √x √x) = √(x x)

  -- ²-of-sqrt' : ∀ x → {{ p : ! [ 0f ≤ x ] }} → sqrt x {{p}} · sqrt x {{p}} ≡ x
  -- ²-of-sqrt' x {{p}} = let y = sqrt x; instance q = !! 0≤sqrt x in transport (
  --   sqrt (y · y) ≡ y ≡⟨ {!   !} ⟩
  --   sqrt (y · y) · sqrt (y · y) ≡ y · sqrt (y · y) ≡⟨ {!   !} ⟩
  --   sqrt (y · y) · sqrt (y · y) ≡ y · y ≡⟨ {! λ x → x  !} ⟩
  --   sqrt x · sqrt x ≡ x ∎) (sqrt-of-² y)
  --    {!   !} ⇒⟨ {!   !} ⟩
  --    {!   !} ◼) {! (sqrt-of-² y ) !}
  -- sqrt (x · x) ≡ x
  -- sqrt (x · x) · sqrt (x · x) ≡ x · sqrt (x · x)
  -- sqrt (x · x) · sqrt (x · x) ≡ x · x
  -- x = sqrt y
  -- sqrt y · sqrt y ≡ y

  sqrt-test : (x y z : Carrier) → [ 0f ≤ x ] → [ 0f ≤ y ] → Carrier
  sqrt-test x y z 0≤x 0≤y = let instance _ = !! 0≤x
                                instance _ = !! 0≤y
                            in (sqrt x) + (sqrt y) + (sqrt (z · z))

  field
    _⁻¹ : (x : Carrier) → {{p : [ x # 0f ]}} → Carrier

  _/_ : (x y : Carrier) → {{p : [ y # 0f ]}} → Carrier
  (x / y) {{p}} = x · (y ⁻¹) {{p}}

  infix  9 _⁻¹
  infixl 7 _·_
  infixl 7 _/_
  infix  6 -_
  infix  5 _-_
  infixl 5 _+_
  infixl 4 _#_
  infixl 4 _≤_
  infixl 4 _<_

open import MorePropAlgebra.Bridges1999

-- mkBridges : ∀{ℓ ℓ'} → CompletePartiallyOrderedFieldWithSqrt {ℓ} {ℓ'} → BooijResults {ℓ} {ℓ'}
-- mkBridges CPOFS = record { CompletePartiallyOrderedFieldWithSqrt CPOFS }

-----------8<--------------------------------------------8<------------------------------------------8<------------------

{- currently, we have that IsAbs works on "rigs" (rings where `-_` is not necessary)
   but in our applications, we do want to take the square root immediately on modules
   therefore, `abs` is defined here as always mapping into `CompletePartiallyOrderedFieldWithSqrt` although more general `abs`es would be possible
-}

module _ -- mathematical structures with `abs` into the real numbers
  {ℝℓ ℝℓ' : Level}
  (ℝbundle : CompletePartiallyOrderedFieldWithSqrt {ℝℓ} {ℝℓ'})
  where
  module ℝ = CompletePartiallyOrderedFieldWithSqrt ℝbundle
  open ℝ using () renaming (Carrier to ℝ; is-set to is-setʳ; _≤_ to _≤ʳ_; 0f to 0ʳ; 1f to 1ʳ; _+_ to _+ʳ_; _·_ to _·ʳ_; -_ to -ʳ_; _-_ to _-ʳ_)

  -- this makes the complex numbers ℂ
  module EuclideanTwoProductOfCompletePartiallyOrderedFieldWithSqrt where
    Carrier : Type ℝℓ
    Carrier = ℝ × ℝ

    re im : Carrier → ℝ
    re = fst
    im = snd

    0f : Carrier
    0f = 0ʳ , 0ʳ

    1f : Carrier
    1f = 1ʳ , 0ʳ

    _+_ : Carrier → Carrier → Carrier
    (ar , ai) + (br , bi) = (ar +ʳ br) , (ai +ʳ bi)

    _·_ : Carrier → Carrier → Carrier
    (ar , ai) · (br , bi) = (ar ·ʳ br -ʳ ai ·ʳ bi) , (ar ·ʳ bi +ʳ br ·ʳ ai)

    -_ : Carrier → Carrier
    - (ar , ai) = (-ʳ ar , -ʳ ai)

    is-set : isSet Carrier
    is-set = isSetΣ ℝ.is-set (λ _ → ℝ.is-set)

  -- this makes the `R` in `RModule`
  record ApartnessRingWithAbsIntoCompletePartiallyOrderedFieldWithSqrt {ℓ ℓ' : Level} : Type (ℓ-suc (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℝℓ ℝℓ'))) where
    field
      Carrier : Type ℓ
      0f      : Carrier
      1f      : Carrier
      _+_     : Carrier → Carrier → Carrier
      _·_     : Carrier → Carrier → Carrier
      -_      : Carrier → Carrier
      _#_     : hPropRel Carrier Carrier ℓ'
      abs     : Carrier → ℝ

  -- this makes the `G` in `GModule`
  record ApartnessGroupWithAbsIntoCompletePartiallyOrderedFieldWithSqrt {ℓ ℓ' : Level} : Type (ℓ-suc (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℝℓ ℝℓ'))) where
    field
      Carrier : Type ℓ
      1f      : Carrier
      _·_     : Carrier → Carrier → Carrier
      _⁻¹     : Carrier → Carrier
      _#_     : hPropRel Carrier Carrier ℓ'
      abs     : Carrier → ℝ

  -- this makes the `K` in `KModule`
  record CompleteApartnessFieldWithAbsIntoCompletePartiallyOrderedFieldWithSqrt {ℓ ℓ' : Level} : Type (ℓ-suc (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℝℓ ℝℓ'))) where
    field
      Carrier : Type ℓ
      0f      : Carrier
      1f      : Carrier
      _+_     : Carrier → Carrier → Carrier
      _·_     : Carrier → Carrier → Carrier
      -_      : Carrier → Carrier
      _#_     : hPropRel Carrier Carrier ℓ'
      _⁻¹     : (x : Carrier) → {{p : [ x # 0f ]}} → Carrier
      abs     : Carrier → ℝ
      is-set  : isSet Carrier
      is-abs  : [ isAbs is-set 0f _+_ _·_ is-setʳ 0ʳ _+ʳ_ _·ʳ_ _≤ʳ_ abs ]

    -- TODO: complete this

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- {-# OPTIONS -v tc.meta.assign:50 #-}
module Issue483c where

import Common.Level

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

data ⊥ : Set where
record ⊤ : Set where

refute : .⊥ → ⊥
refute ()

mk⊤ : ⊥ → ⊤
mk⊤ ()

X   : .⊤ → ⊥
bad : .(x : ⊥) → X (mk⊤ x) ≡ refute x
X     = _
bad x = refl

false : ⊥
false = X _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Lemmas related to bisimilarity and CCS, implemented using the
-- coinductive definition of bisimilarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Bisimilarity.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.CCS.General
open import Equational-reasoning
open import Labelled-transition-system.CCS Name

open import Bisimilarity CCS
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

------------------------------------------------------------------------
-- Congruence lemmas

-- Some lemmas used to prove the congruence results below as well as
-- similar results in Similarity.CCS.

module Cong-lemmas
  ({R} R′ : Proc ∞ → Proc ∞ → Type ℓ)
  ⦃ _ : Convertible R R′ ⦄
  ⦃ _ : Convertible R′ R′ ⦄
  ⦃ _ : Convertible _∼_ R′ ⦄
  ⦃ _ : Transitive R′ R′ ⦄
  (left-to-right :
   ∀ {P Q} → R P Q →
   ∀ {P′ μ} → P [ μ ]⟶ P′ → ∃ λ Q′ → Q [ μ ]⟶ Q′ × R′ P′ Q′)
  where

  private

    infix -2 R′:_

    R′:_ : ∀ {P Q} → R′ P Q → R′ P Q
    R′:_ = id

    infix -3 lr-result

    lr-result :
      ∀ {P′ Q Q′} μ → R′ P′ Q′ → Q [ μ ]⟶ Q′ →
      ∃ λ Q′ → Q [ μ ]⟶ Q′ × R′ P′ Q′
    lr-result _ P′∼′Q′ Q⟶Q′ = _ , Q⟶Q′ , P′∼′Q′

    syntax lr-result μ P′∼′Q′ Q⟶Q′ = P′∼′Q′ [ μ ]⟵ Q⟶Q′

  ∣-cong :
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    ∀ {P₁ P₂ Q₁ Q₂ S₁ μ} →
    R P₁ P₂ → R Q₁ Q₂ → P₁ ∣ Q₁ [ μ ]⟶ S₁ →
    ∃ λ S₂ → P₂ ∣ Q₂ [ μ ]⟶ S₂ × R′ S₁ S₂
  ∣-cong _∣-cong′_ P₁∼P₂ Q₁∼Q₂ = λ where
    (par-left  tr)  → Σ-map (_∣ _)
                        (Σ-map par-left
                               (_∣-cong′ convert Q₁∼Q₂))
                        (left-to-right P₁∼P₂ tr)
    (par-right tr)  → Σ-map (_ ∣_)
                        (Σ-map par-right
                               (convert P₁∼P₂ ∣-cong′_))
                        (left-to-right Q₁∼Q₂ tr)
    (par-τ tr₁ tr₂) → Σ-zip _∣_ (Σ-zip par-τ _∣-cong′_)
                        (left-to-right P₁∼P₂ tr₁)
                        (left-to-right Q₁∼Q₂ tr₂)

  ⊕-cong :
    ∀ {P₁ P₁′ P₂ P₂′ S μ} →
    R P₁ P₁′ → R P₂ P₂′ → P₁ ⊕ P₂ [ μ ]⟶ S →
    ∃ λ S′ → P₁′ ⊕ P₂′ [ μ ]⟶ S′ × R′ S S′
  ⊕-cong {P₁} {P₁′} {P₂} {P₂′} {S} {μ} P₁∼P₁′ P₂∼P₂′ = λ where
    (sum-left P₁⟶S) → case left-to-right P₁∼P₁′ P₁⟶S of λ where
      (S′ , P₁′⟶S′ , S∼′S′) →
        S          ∼⟨ S∼′S′ ⟩■
        S′
          [ μ ]⟵   ←⟨ ⟶: sum-left P₁′⟶S′ ⟩■
        P₁′ ⊕ P₂′

    (sum-right P₂⟶S) → case left-to-right P₂∼P₂′ P₂⟶S of λ where
      (S′ , P₂′⟶S′ , S∼′S′) →
        S          ∼⟨ S∼′S′ ⟩■
        S′
          [ μ ]⟵   ←⟨ ⟶: sum-right P₂′⟶S′ ⟩■
        P₁′ ⊕ P₂′

  ·-cong :
    ∀ {P₁ P₂ Q₁ μ μ′} →
    R′ (force P₁) (force P₂) → μ · P₁ [ μ′ ]⟶ Q₁ →
    ∃ λ Q₂ → μ · P₂ [ μ′ ]⟶ Q₂ × R′ Q₁ Q₂
  ·-cong {P₁} {P₂} {μ = μ} P₁∼P₂ action =
    force P₁  ∼⟨ P₁∼P₂ ⟩■
    force P₂
      [ μ ]⟵  ←⟨ ⟶: action ⟩■
    μ · P₂

  ⟨ν⟩-cong :
    (∀ {a P P′} → R′ P P′ → R′ (⟨ν a ⟩ P) (⟨ν a ⟩ P′)) →
    ∀ {a μ P P′ Q} →
    R P P′ → ⟨ν a ⟩ P [ μ ]⟶ Q →
    ∃ λ Q′ → ⟨ν a ⟩ P′ [ μ ]⟶ Q′ × R′ Q Q′
  ⟨ν⟩-cong ⟨ν⟩-cong′ {a} {μ} {P′ = P′} P∼P′
           (restriction {P′ = Q} a∉μ P⟶Q) =
    case left-to-right P∼P′ P⟶Q of λ where
      (Q′ , P′⟶Q′ , Q∼′Q′) →
        ⟨ν a ⟩ Q   ∼⟨ ⟨ν⟩-cong′ Q∼′Q′ ⟩■
        ⟨ν a ⟩ Q′
          [ μ ]⟵   ←⟨ ⟶: restriction a∉μ P′⟶Q′ ⟩■
        ⟨ν a ⟩ P′

  !-cong :
    (∀ {μ P P₀} →
     ! P [ μ ]⟶ P₀ →
     (∃ λ P′ → P [ μ ]⟶ P′ × P₀ ∼ ! P ∣ P′)
       ⊎
     (μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
      P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ ×
      P₀ ∼ (! P ∣ P′) ∣ P″)) →
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    (∀ {P P′} → R′ P P′ → R′ (! P) (! P′)) →
    ∀ {P P′ Q μ} →
    R P P′ → ! P [ μ ]⟶ Q →
    ∃ λ Q′ → ! P′ [ μ ]⟶ Q′ × R′ Q Q′
  !-cong 6-1-3-2 _∣-cong′_ !-cong′_ {P} {P′} {Q} {μ} P∼P′ !P⟶Q =
    case 6-1-3-2 !P⟶Q of λ where

      (inj₁ (P″ , P⟶P″ , Q∼!P∣P″)) →
        let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
        in
        Q          ∼⟨ R′: convert Q∼!P∣P″ ⟩
        ! P  ∣ P″  ∼⟨ (!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′ ⟩■
        ! P′ ∣ Q′
          [ μ ]⟵   ←⟨ ⟶: replication (par-right P′⟶Q′) ⟩■
        ! P′

      (inj₂ (refl , P″ , P‴ , a , P⟶P″ , P⟶P‴ , Q∼!P∣P″∣P‴)) →
        let Q′ , P′⟶Q′ , P″∼′Q′ = left-to-right P∼P′ P⟶P″
            Q″ , P′⟶Q″ , P‴∼′Q″ = left-to-right P∼P′ P⟶P‴
        in
        Q                 ∼⟨ R′: convert Q∼!P∣P″∣P‴ ⟩
        (! P ∣ P″) ∣ P‴   ∼⟨ ((!-cong′ convert P∼P′) ∣-cong′ P″∼′Q′) ∣-cong′ P‴∼′Q″ ⟩■
        (! P′ ∣ Q′) ∣ Q″
          [ τ ]⟵          ←⟨ ⟶: replication (par-τ (replication (par-right P′⟶Q′)) P′⟶Q″) ⟩■
        ! P′

private
  module CL {i} = Cong-lemmas [ i ]_∼′_ left-to-right

------------------------------------------------------------------------
-- Various lemmas related to _∣_

mutual

  -- _∣_ is commutative.

  ∣-comm : ∀ {P Q i} → [ i ] P ∣ Q ∼ Q ∣ P
  ∣-comm {i = i} = ⟨ lr , Σ-map id (Σ-map id symmetric) ∘ lr ⟩
    where
    lr : ∀ {P P′ Q μ} →
         P ∣ Q [ μ ]⟶ P′ →
         ∃ λ Q′ → Q ∣ P [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (par-left tr)   = _ , par-right tr , ∣-comm′
    lr (par-right tr)  = _ , par-left tr , ∣-comm′
    lr (par-τ tr₁ tr₂) =
        _
      , par-τ tr₂ (subst (λ a → _ [ name a ]⟶ _)
                         (sym $ co-involutive _)
                         tr₁)
      , ∣-comm′

  ∣-comm′ : ∀ {P Q i} → [ i ] P ∣ Q ∼′ Q ∣ P
  force ∣-comm′ = ∣-comm

mutual

  -- _∣_ is associative.

  ∣-assoc : ∀ {P Q R i} → [ i ] P ∣ (Q ∣ R) ∼ (P ∣ Q) ∣ R
  ∣-assoc {i = i} = ⟨ lr , rl ⟩
    where
    lr : ∀ {P Q R P′ μ} →
         P ∣ (Q ∣ R) [ μ ]⟶ P′ →
         ∃ λ Q′ → (P ∣ Q) ∣ R [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (par-left tr)               = _ , par-left (par-left tr)    , ∣-assoc′
    lr (par-right (par-left tr))   = _ , par-left (par-right tr)   , ∣-assoc′
    lr (par-right (par-right tr))  = _ , par-right tr              , ∣-assoc′
    lr (par-right (par-τ tr₁ tr₂)) = _ , par-τ (par-right tr₁) tr₂ , ∣-assoc′
    lr (par-τ tr₁ (par-left tr₂))  = _ , par-left (par-τ tr₁ tr₂)  , ∣-assoc′
    lr (par-τ tr₁ (par-right tr₂)) = _ , par-τ (par-left tr₁) tr₂  , ∣-assoc′

    rl : ∀ {P Q R Q′ μ} →
         (P ∣ Q) ∣ R [ μ ]⟶ Q′ →
         ∃ λ P′ → P ∣ (Q ∣ R) [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
    rl (par-left (par-left tr))    = _ , par-left tr               , ∣-assoc′
    rl (par-left (par-right tr))   = _ , par-right (par-left tr)   , ∣-assoc′
    rl (par-left (par-τ tr₁ tr₂))  = _ , par-τ tr₁ (par-left tr₂)  , ∣-assoc′
    rl (par-right tr)              = _ , par-right (par-right tr)  , ∣-assoc′
    rl (par-τ (par-left tr₁) tr₂)  = _ , par-τ tr₁ (par-right tr₂) , ∣-assoc′
    rl (par-τ (par-right tr₁) tr₂) = _ , par-right (par-τ tr₁ tr₂) , ∣-assoc′

  ∣-assoc′ : ∀ {P Q R i} → [ i ] P ∣ (Q ∣ R) ∼′ (P ∣ Q) ∣ R
  force ∣-assoc′ = ∣-assoc

-- ∅ is a left identity of _∣_.

∣-left-identity : ∀ {i P} → [ i ] ∅ ∣ P ∼ P
∣-left-identity =
  ⟨ (λ { (par-right tr) → (_ , tr , λ { .force → ∣-left-identity })
       ; (par-left ())
       ; (par-τ () _)
       })
  , (λ tr → (_ , par-right tr , λ { .force → ∣-left-identity }))
  ⟩

∣-left-identity′ : ∀ {P i} → [ i ] ∅ ∣ P ∼′ P
force ∣-left-identity′ = ∣-left-identity

-- ∅ is a right identity of _∣_.

∣-right-identity : ∀ {P} → P ∣ ∅ ∼ P
∣-right-identity {P} =
  P ∣ ∅  ∼⟨ ∣-comm ⟩
  ∅ ∣ P  ∼⟨ ∣-left-identity ⟩■
  P

mutual

  -- _∣_ preserves bisimilarity.

  infix 6 _∣-cong_ _∣-cong′_

  _∣-cong_ : ∀ {i P P′ Q Q′} →
             [ i ] P ∼ Q → [ i ] P′ ∼ Q′ → [ i ] P ∣ P′ ∼ Q ∣ Q′
  P∼Q ∣-cong P′∼Q′ =
    ⟨ lr P∼Q P′∼Q′
    , Σ-map id (Σ-map id symmetric) ∘
      lr (symmetric P∼Q) (symmetric P′∼Q′)
    ⟩
    where
    lr = CL.∣-cong _∣-cong′_

  _∣-cong′_ : ∀ {i P P′ Q Q′} →
              [ i ] P ∼′ Q → [ i ] P′ ∼′ Q′ → [ i ] P ∣ P′ ∼′ Q ∣ Q′
  force (P∼P′ ∣-cong′ Q∼Q′) = force P∼P′ ∣-cong force Q∼Q′

-- An alternative proof that is closer to the one in the paper.

infix 6 _∣-congP_

_∣-congP_ : ∀ {i P P′ Q Q′} →
            [ i ] P ∼ Q → [ i ] P′ ∼ Q′ → [ i ] P ∣ P′ ∼ Q ∣ Q′
_∣-congP_ {i} = λ p q →
  ⟨ lr p q
  , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p) (symmetric q)
  ⟩
  where
  lr : ∀ {P P′ P″ Q Q′ μ} →
       [ i ] P ∼ Q → [ i ] P′ ∼ Q′ → P ∣ P′ [ μ ]⟶ P″ →
       ∃ λ Q″ → Q ∣ Q′ [ μ ]⟶ Q″ × [ i ] P″ ∼′ Q″
  lr p q (par-left tr) =
    let (_ , tr′          , p′) = left-to-right p tr
    in  (_ , par-left tr′ , λ { .force → force p′ ∣-congP q })

  lr p q (par-right tr) =
    let (_ , tr′           , q′) = left-to-right q tr
    in  (_ , par-right tr′ , λ { .force → p ∣-congP force q′ })

  lr p q (par-τ tr₁ tr₂) =
    let (_ , tr₁′            , p′) = left-to-right p tr₁
        (_ , tr₂′            , q′) = left-to-right q tr₂
    in  (_ , par-τ tr₁′ tr₂′ , λ { .force → force p′ ∣-congP force q′ })

------------------------------------------------------------------------
-- Exercise 6.1.2 from "Enhancements of the bisimulation proof method"
-- by Pous and Sangiorgi

private

  -- A compact proof.

  6-1-2-compact : ∀ {P i} → [ i ] ! P ∣ P ∼ ! P
  6-1-2-compact =
    ⟨ (λ tr → _ , replication tr , reflexive)
    , (λ { (replication tr) → _ , tr , reflexive })
    ⟩

-- A less compact proof.

6-1-2 : ∀ {P i} → [ i ] ! P ∣ P ∼ ! P
6-1-2 {P} =
  ⟨ (λ {P′} {μ} tr →
       P′   ∼⟨ ∼′: reflexive ⟩■
       P′   [ μ ]⟵⟨ replication tr ⟩
       ! P)
  , (λ { {q′ = P′} {μ = μ} (replication tr) →
         ! P ∣ P  [ μ ]⟶⟨ tr ⟩ʳˡ
         P′       ∼⟨ ∼′: reflexive ⟩■
         P′ })
  ⟩

------------------------------------------------------------------------
-- Exercise 6.1.3 (2) from "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi, plus some rearrangement lemmas

private
  module 6-1-3-2 = Bisimilarity.CCS.General.6-1-3-2 (record
    { _∼_       = _∼_
    ; step-∼    = step-∼
    ; finally-∼ = Equational-reasoning.finally₂
    ; reflexive = reflexive
    ; symmetric = symmetric
    ; ∣-comm    = ∣-comm
    ; ∣-assoc   = ∣-assoc
    ; _∣-cong_  = _∣-cong_
    ; 6-1-2     = 6-1-2
    })

6-1-3-2 :
  ∀ {P μ R} →
  ! P [ μ ]⟶ R →
  (∃ λ P′ → P [ μ ]⟶ P′ × R ∼ ! P ∣ P′)
    ⊎
  (μ ≡ τ × ∃ λ P′ → ∃ λ P″ → ∃ λ a →
   P [ name a ]⟶ P′ × P [ name (co a) ]⟶ P″ × R ∼ (! P ∣ P′) ∣ P″)
6-1-3-2 = 6-1-3-2.6-1-3-2

swap-rightmost : ∀ {P Q R} → (P ∣ Q) ∣ R ∼ (P ∣ R) ∣ Q
swap-rightmost = 6-1-3-2.swap-rightmost

swap-in-the-middle : ∀ {P Q R S} →
                     (P ∣ Q) ∣ (R ∣ S) ∼ (P ∣ R) ∣ (Q ∣ S)
swap-in-the-middle {P} {Q} {R} {S} =
  (P ∣ Q) ∣ (R ∣ S)  ∼⟨ swap-rightmost ⟩
  (P ∣ (R ∣ S)) ∣ Q  ∼⟨ ∣-assoc ∣-cong reflexive ⟩
  ((P ∣ R) ∣ S) ∣ Q  ∼⟨ symmetric ∣-assoc ⟩
  (P ∣ R) ∣ (S ∣ Q)  ∼⟨ reflexive ∣-cong ∣-comm ⟩■
  (P ∣ R) ∣ (Q ∣ S)

------------------------------------------------------------------------
-- More preservation lemmas

-- _⊕_ preserves bisimilarity.

infix 8 _⊕-cong_ _⊕-cong′_

_⊕-cong_ : ∀ {i P P′ Q Q′} →
           [ i ] P ∼ P′ → [ i ] Q ∼ Q′ → [ i ] P ⊕ Q ∼ P′ ⊕ Q′
_⊕-cong_ {i} P∼P′ Q∼Q′ =
  ⟨ CL.⊕-cong P∼P′ Q∼Q′
  , Σ-map id (Σ-map id symmetric) ∘
    CL.⊕-cong {i = i} (symmetric P∼P′) (symmetric Q∼Q′)
  ⟩

_⊕-cong′_ : ∀ {i P P′ Q Q′} →
            [ i ] P ∼′ P′ → [ i ] Q ∼′ Q′ → [ i ] P ⊕ Q ∼′ P′ ⊕ Q′
force (P∼P′ ⊕-cong′ Q∼Q′) = force P∼P′ ⊕-cong force Q∼Q′

-- _·_ preserves bisimilarity.

infix 12 _·-cong_ _·-cong′_

_·-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ∼′ force P′ → [ i ] μ · P ∼ μ′ · P′
refl ·-cong P∼P′ =
  ⟨ CL.·-cong P∼P′
  , Σ-map id (Σ-map id symmetric) ∘ CL.·-cong (symmetric P∼P′)
  ⟩

_·-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ∼′ force P′ → [ i ] μ · P ∼′ μ′ · P′
force (μ≡μ′ ·-cong′ P∼P′) = μ≡μ′ ·-cong P∼P′

-- An alternative proof that is closer to the one in the paper.

·-congP : ∀ {i μ P Q} → [ i ] force P ∼′ force Q → [ i ] μ · P ∼ μ · Q
·-congP p =
  ⟨ (λ { action → _ , action , p })
  , (λ { action → _ , action , p })
  ⟩

-- _∙_ preserves bisimilarity.

infix 12 _∙-cong_ _∙-cong′_

_∙-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] P ∼ P′ → [ i ] μ ∙ P ∼ μ′ ∙ P′
refl ∙-cong P∼P′ = refl ·-cong convert {a = ℓ} P∼P′

_∙-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] P ∼′ P′ → [ i ] μ ∙ P ∼′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P∼P′) = μ≡μ′ ∙-cong force P∼P′

-- _∙ turns equality into bisimilarity.

infix 12 _∙-cong _∙-cong′

_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ∼ μ′ ∙
refl ∙-cong = reflexive

_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ∼′ μ′ ∙
refl ∙-cong′ = reflexive

mutual

  -- !_ preserves bisimilarity.

  infix 10 !-cong_ !-cong′_

  !-cong_ : ∀ {i P P′} →
            [ i ] P ∼ P′ → [ i ] ! P ∼ ! P′
  !-cong P∼P′ =
    ⟨ lr P∼P′
    , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼P′)
    ⟩
    where
    lr = CL.!-cong 6-1-3-2 _∣-cong′_ !-cong′_

  !-cong′_ : ∀ {i P P′} → [ i ] P ∼′ P′ → [ i ] ! P ∼′ ! P′
  force (!-cong′ P∼P′) = !-cong force P∼P′

-- An alternative proof that is closer to the one in the paper.

!-congP : ∀ {i P Q} → [ i ] P ∼ Q → [ i ] ! P ∼ ! Q
!-congP {i} = λ p →
  ⟨ lr p
  , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric p)
  ⟩
  where
  lr : ∀ {P Q R μ} →
       [ i ] P ∼ Q → ! P [ μ ]⟶ R →
       ∃ λ S → ! Q [ μ ]⟶ S × [ i ] R ∼′ S
  lr {P} {Q} {R} P∼Q !P⟶R with 6-1-3-2 !P⟶R
  ... | inj₁ (P′ , P⟶P′ , R∼!P∣P′) =
    let (Q′ , Q⟶Q′ , P′∼′Q′) = left-to-right P∼Q P⟶P′
    in
    ( ! Q ∣ Q′
    , replication (par-right Q⟶Q′)
    , (R         ∼⟨ R∼!P∣P′ ⟩
       ! P ∣ P′  ∼⟨ (λ { .force → !-congP P∼Q }) ∣-cong′ P′∼′Q′ ⟩
       ! Q ∣ Q′  ■
      )
    )
  ... | inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , R∼!P∣P′∣P″) =
    let (Q′ , Q⟶Q′ , P′∼′Q′) = left-to-right P∼Q P⟶P′
        (Q″ , Q⟶Q″ , P″∼′Q″) = left-to-right P∼Q P⟶P″
    in
    ( (! Q ∣ Q′) ∣ Q″
    , replication (par-τ (replication (par-right Q⟶Q′)) Q⟶Q″)
    , (R                ∼⟨ R∼!P∣P′∣P″ ⟩
       (! P ∣ P′) ∣ P″  ∼⟨ ((λ { .force → !-congP P∼Q }) ∣-cong′ P′∼′Q′)
                             ∣-cong′ P″∼′Q″ ⟩
       (! Q ∣ Q′) ∣ Q″  ■
      )
    )

mutual

  -- ⟨ν_⟩ preserves bisimilarity.

  ⟨ν_⟩-cong : ∀ {i a a′ P P′} →
              a ≡ a′ → [ i ] P ∼ P′ → [ i ] ⟨ν a ⟩ P ∼ ⟨ν a′ ⟩ P′
  ⟨ν refl ⟩-cong = λ P∼P′ →
    ⟨ lr P∼P′
    , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼P′)
    ⟩
    where
    lr = CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′

  ⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
               a ≡ a′ → [ i ] P ∼′ P′ → [ i ] ⟨ν a ⟩ P ∼′ ⟨ν a′ ⟩ P′
  force (⟨ν a≡a′ ⟩-cong′ P∼P′) = ⟨ν a≡a′ ⟩-cong (force P∼P′)

-- _[_] preserves bisimilarity. (This result is related to Exercise
-- 6.2.10 in "Enhancements of the bisimulation proof method"
-- by Pous and Sangiorgi.)

infix 5 _[_]-cong _[_]-cong′

_[_]-cong :
  ∀ {i n Ps Qs}
  (C : Context ∞ n) → (∀ x → [ i ] Ps x ∼ Qs x) →
  [ i ] C [ Ps ] ∼ C [ Qs ]
hole x   [ Ps∼Qs ]-cong = Ps∼Qs x
∅        [ Ps∼Qs ]-cong = reflexive
C₁ ∣ C₂  [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ∣-cong (C₂ [ Ps∼Qs ]-cong)
C₁ ⊕ C₂  [ Ps∼Qs ]-cong = (C₁ [ Ps∼Qs ]-cong) ⊕-cong (C₂ [ Ps∼Qs ]-cong)
μ · C    [ Ps∼Qs ]-cong = refl ·-cong λ { .force → force C [ Ps∼Qs ]-cong }
⟨ν a ⟩ C [ Ps∼Qs ]-cong = ⟨ν refl ⟩-cong (C [ Ps∼Qs ]-cong)
! C      [ Ps∼Qs ]-cong = !-cong (C [ Ps∼Qs ]-cong)

_[_]-cong′ :
  ∀ {i n Ps Qs}
  (C : Context ∞ n) → (∀ x → [ i ] Ps x ∼′ Qs x) →
  [ i ] C [ Ps ] ∼′ C [ Qs ]
force (C [ Ps∼Qs ]-cong′) = C [ (λ x → force (Ps∼Qs x)) ]-cong

-- The proof of _[_]-cong uses 6-1-3-2 (in !-cong_). The following
-- direct proof does not use 6-1-3-2 (but it does use
-- extensionality).

module _ (ext : Proc-extensionality) where

 mutual

  infix 5 _[_]-cong₂ _[_]-cong₂′

  _[_]-cong₂ :
    ∀ {i n Ps Qs}
    (C : Context ∞ n) → (∀ x → [ i ] Ps x ∼ Qs x) →
    [ i ] C [ Ps ] ∼ C [ Qs ]
  _[_]-cong₂ {i} C Ps∼Qs =
    ⟨ lr C Ps∼Qs
    , Σ-map id (Σ-map id symmetric) ∘ lr C (symmetric ∘ Ps∼Qs)
    ⟩
    where

    infix 5 _[_][_]-cong₁ _[_][_]-cong₂

    _[_][_]-cong₁ :
      ∀ {n P Q Ps Qs} →
      (C : Context ∞ (suc n)) →
      [ i ] P ∼′ Q →
      (∀ x → [ i ] Ps x ∼ Qs x) →
      [ i ] C [ [ const P , Ps ] ] ∼′ C [ [ const Q , Qs ] ]
    force (C [ P∼′Q ][ Ps∼Qs ]-cong₁) =
      C [ [ const (force P∼′Q) , Ps∼Qs ] ]-cong₂

    _[_][_]-cong₂ :
      ∀ {P Q R S} →
      (C : Context ∞ 2) →
      [ i ] P ∼′ Q →
      [ i ] R ∼′ S →
      [ i ] C [ [ const P , [ const R , (λ ()) ] ] ] ∼′
            C [ [ const Q , [ const S , (λ ()) ] ] ]
    force (C [ P∼′Q ][ R∼′S ]-cong₂) =
      C [ [ const (force P∼′Q)
          , [ const (force R∼′S) , (λ ()) ]
          ] ]-cong₂

    lr : ∀ {n Ps Qs P′ μ} (C : Context ∞ n) →
         (∀ x → [ i ] Ps x ∼ Qs x) →
         C [ Ps ] [ μ ]⟶ P′ →
         ∃ λ Q′ → C [ Qs ] [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr (hole x)   Ps∼Qs tr                  = left-to-right (Ps∼Qs x) tr
    lr ∅          Ps∼Qs ()
    lr (C₁ ∣ C₂)  Ps∼Qs (par-left tr)       = Σ-map (_∣ _) (Σ-map par-left (λ b → subst (λ P → [ i ] _ ∼′ _ ∣ P) (ext $ weaken-[] C₂) $
                                                                                subst (λ P → [ i ] _ ∣ P ∼′ _) (ext $ weaken-[] C₂) $
                                                                                hole fzero ∣ weaken C₂ [ b ][ Ps∼Qs ]-cong₁)) (lr C₁ Ps∼Qs tr)
    lr (C₁ ∣ C₂)  Ps∼Qs (par-right tr)      = Σ-map (_ ∣_) (Σ-map par-right (λ b → subst (λ P → [ i ] _ ∼′ P ∣ _) (ext $ weaken-[] C₁) $
                                                                                subst (λ P → [ i ] P ∣ _ ∼′ _) (ext $ weaken-[] C₁) $
                                                                                weaken C₁ ∣ hole fzero [ b ][ Ps∼Qs ]-cong₁)) (lr C₂ Ps∼Qs tr)
    lr (C₁ ∣ C₂)  Ps∼Qs (par-τ tr₁ tr₂)     = Σ-zip _∣_ (Σ-zip par-τ (λ b₁ b₂ → hole fzero ∣ hole (fsuc fzero) [ b₁ ][ b₂ ]-cong₂))
                                                (lr C₁ Ps∼Qs tr₁) (lr C₂ Ps∼Qs tr₂)
    lr (C₁ ⊕ C₂)  Ps∼Qs (sum-left tr)       = Σ-map id (Σ-map sum-left id) (lr C₁ Ps∼Qs tr)
    lr (C₁ ⊕ C₂)  Ps∼Qs (sum-right tr)      = Σ-map id (Σ-map sum-right id) (lr C₂ Ps∼Qs tr)
    lr (μ · C)    Ps∼Qs action              = _ , action , λ { .force → force C [ Ps∼Qs ]-cong₂ }
    lr (⟨ν a ⟩ C) Ps∼Qs (restriction a∉ tr) = Σ-map ⟨ν a ⟩ (Σ-map (restriction a∉) (λ b → ⟨ν a ⟩ (hole fzero) [ b ][ Ps∼Qs ]-cong₁))
                                                (lr C Ps∼Qs tr)
    lr (! C)      Ps∼Qs (replication tr)    = Σ-map id (Σ-map replication id) (lr (! C ∣ C) Ps∼Qs tr)

  _[_]-cong₂′ :
    ∀ {i n Ps Qs}
    (C : Context ∞ n) → (∀ x → [ i ] Ps x ∼′ Qs x) →
    [ i ] C [ Ps ] ∼′ C [ Qs ]
  force (C [ Ps∼′Qs ]-cong₂′) = C [ (λ x → force (Ps∼′Qs x)) ]-cong₂

-- A variant of _[_]-cong for weakly guarded contexts.
--
-- Note that the input uses the primed variant of bisimilarity.
--
-- I got the idea for this lemma from Lemma 23 in Schäfer and Smolka's
-- "Tower Induction and Up-to Techniques for CCS with Fixed Points".

infix 5 _[_]-cong-w

_[_]-cong-w :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Weakly-guarded C → (∀ x → [ i ] Ps x ∼′ Qs x) →
  [ i ] C [ Ps ] ∼ C [ Qs ]
∅              [ Ps∼Qs ]-cong-w = reflexive
W₁ ∣ W₂        [ Ps∼Qs ]-cong-w = (W₁ [ Ps∼Qs ]-cong-w) ∣-cong
                                  (W₂ [ Ps∼Qs ]-cong-w)
action {C = C} [ Ps∼Qs ]-cong-w = refl ·-cong (force C [ Ps∼Qs ]-cong′)
⟨ν⟩ W          [ Ps∼Qs ]-cong-w = ⟨ν refl ⟩-cong (W [ Ps∼Qs ]-cong-w)
! W            [ Ps∼Qs ]-cong-w = !-cong (W [ Ps∼Qs ]-cong-w)
W₁ ⊕ W₂        [ Ps∼Qs ]-cong-w = (W₁ [ Ps∼Qs ]-cong-w) ⊕-cong
                                  (W₂ [ Ps∼Qs ]-cong-w)

-- Very strong bisimilarity is contained in bisimilarity.

mutual

  ≡→∼ : ∀ {i P Q} → Equal i P Q → [ i ] P ∼ Q
  ≡→∼ ∅              = reflexive
  ≡→∼ (eq₁ ∣ eq₂)    = ≡→∼ eq₁ ∣-cong ≡→∼ eq₂
  ≡→∼ (eq₁ ⊕ eq₂)    = ≡→∼ eq₁ ⊕-cong ≡→∼ eq₂
  ≡→∼ (refl · eq)    = refl ·-cong ≡→∼′ eq
  ≡→∼ (⟨ν refl ⟩ eq) = ⟨ν refl ⟩-cong (≡→∼ eq)
  ≡→∼ (! eq)         = !-cong ≡→∼ eq

  ≡→∼′ : ∀ {i P Q} → Equal′ i P Q → [ i ] P ∼′ Q
  force (≡→∼′ eq) = ≡→∼ (force eq)

------------------------------------------------------------------------
-- Unique solutions

-- If the set of equations corresponding (in a certain sense) to a
-- family of weakly guarded contexts has two families of solutions,
-- then those solutions are pairwise bisimilar.
--
-- This result is very similar to a proposition in Milner's
-- "Communication and Concurrency".

mutual

  unique-solutions :
    ∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
    (∀ x → Weakly-guarded (C x)) →
    (∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
    (∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
    ∀ x → [ i ] Ps x ∼ Qs x
  unique-solutions {i} {Ps = Ps} {Qs} {C} w ∼C[Ps] ∼C[Qs] x =
    Ps x        ∼⟨ ∼C[Ps] x ⟩
    C x [ Ps ]  ∼⟨ ∼: ⟨ lr ∼C[Ps] ∼C[Qs] , Σ-map id (Σ-map id symmetric) ∘ lr ∼C[Qs] ∼C[Ps] ⟩ ⟩
    C x [ Qs ]  ∼⟨ symmetric (∼C[Qs] x) ⟩■
    Qs x
    where
    lr :
      ∀ {Ps Qs μ P} →
      (∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
      (∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
      C x [ Ps ] [ μ ]⟶ P →
      ∃ λ Q → C x [ Qs ] [ μ ]⟶ Q × [ i ] P ∼′ Q
    lr {Ps} {Qs} {μ} ∼C[Ps] ∼C[Qs] ⟶P =
      case 6-2-15 (C x) (w x) ⟶P of λ where
        (C′ , refl , trs) →
          C′ [ Ps ]   ∼⟨ C′ [ unique-solutions′ w ∼C[Ps] ∼C[Qs] ]-cong′ ⟩■
          C′ [ Qs ]   [ μ ]⟵⟨ trs Qs ⟩
          C x [ Qs ]

  unique-solutions′ :
    ∀ {i n} {Ps Qs : Fin n → Proc ∞} {C : Fin n → Context ∞ n} →
    (∀ x → Weakly-guarded (C x)) →
    (∀ x → [ i ] Ps x ∼ C x [ Ps ]) →
    (∀ x → [ i ] Qs x ∼ C x [ Qs ]) →
    ∀ x → [ i ] Ps x ∼′ Qs x
  force (unique-solutions′ w ∼C[Ps] ∼C[Qs] x) = unique-solutions w ∼C[Ps] ∼C[Qs] x

-- For every family of weakly guarded contexts there is a family of
-- processes that satisfies the corresponding equations.

solutions-exist :
  ∀ {n} {C : Fin n → Context ∞ n} →
  (∀ x → Weakly-guarded (C x)) →
  ∃ λ Ps → ∀ x → Ps x ∼ C x [ Ps ]
solutions-exist {n} {C} w = Ps , Ps∼
  where

  mutual

    Ps : ∀ {i} → Fin n → Proc i
    Ps x = P₁ (w x)

    P₁ : ∀ {i} {C : Context ∞ n} → Weakly-guarded C → Proc i
    P₁ ∅                        = ∅
    P₁ (w₁ ∣ w₂)                = P₁ w₁ ∣ P₁ w₂
    P₁ (w₁ ⊕ w₂)                = P₁ w₁ ⊕ P₁ w₂
    P₁ (action {μ = μ} {C = C}) = μ · λ { .force → P₂ (force C) }
    P₁ (⟨ν⟩ {a = a} w)          = ⟨ν a ⟩ (P₁ w)
    P₁ (! w)                    = ! P₁ w

    P₂ : ∀ {i} → Context ∞ n → Proc i
    P₂ (hole x)   = Ps x
    P₂ ∅          = ∅
    P₂ (C₁ ∣ C₂)  = P₂ C₁ ∣ P₂ C₂
    P₂ (C₁ ⊕ C₂)  = P₂ C₁ ⊕ P₂ C₂
    P₂ (μ · C)    = μ · λ { .force → P₂ (force C) }
    P₂ (⟨ν a ⟩ C) = ⟨ν a ⟩ (P₂ C)
    P₂ (! C)      = ! P₂ C

  P₂∼ : ∀ {i} (C : Context ∞ n) → [ i ] P₂ C ∼ C [ Ps ]
  P₂∼ (hole x)   = reflexive
  P₂∼ ∅          = reflexive
  P₂∼ (C₁ ∣ C₂)  = P₂∼ C₁ ∣-cong P₂∼ C₂
  P₂∼ (C₁ ⊕ C₂)  = P₂∼ C₁ ⊕-cong P₂∼ C₂
  P₂∼ (μ · C)    = refl ·-cong λ { .force → P₂∼ (force C) }
  P₂∼ (⟨ν a ⟩ C) = ⟨ν refl ⟩-cong (P₂∼ C)
  P₂∼ (! C)      = !-cong P₂∼ C

  P₁∼ : {C : Context ∞ n} (w : Weakly-guarded C) → P₁ w ∼ C [ Ps ]
  P₁∼ ∅                = reflexive
  P₁∼ (w₁ ∣ w₂)        = P₁∼ w₁ ∣-cong P₁∼ w₂
  P₁∼ (w₁ ⊕ w₂)        = P₁∼ w₁ ⊕-cong P₁∼ w₂
  P₁∼ (action {C = C}) = refl ·-cong λ { .force → P₂∼ (force C) }
  P₁∼ (⟨ν⟩ {a = a} w)  = ⟨ν refl ⟩-cong (P₁∼ w)
  P₁∼ (! w)            = !-cong P₁∼ w

  Ps∼ : ∀ x → Ps x ∼ C x [ Ps ]
  Ps∼ x = P₁∼ (w x)

------------------------------------------------------------------------
-- Some lemmas related to _⊕_

-- _⊕_ is idempotent.

⊕-idempotent : ∀ {P} → P ⊕ P ∼ P
⊕-idempotent {P} =
  ⟨ lr
  , (λ {R} P⟶R →
       P ⊕ P  ⟶⟨ sum-left P⟶R ⟩ʳˡ
       R      ∼⟨ ∼′: reflexive ⟩■
       R)
  ⟩
  where
  lr : ∀ {Q μ} → P ⊕ P [ μ ]⟶ Q → ∃ λ R → P [ μ ]⟶ R × Q ∼′ R
  lr {Q} (sum-left P⟶Q) =
    Q  ∼⟨ ∼′: reflexive ⟩■
    Q  ⟵⟨ P⟶Q ⟩
    P

  lr {Q} (sum-right P⟶Q) =
    Q  ∼⟨ ∼′: reflexive ⟩■
    Q  ⟵⟨ P⟶Q ⟩
    P

⊕-idempotent′ : ∀ {P} → P ⊕ P ∼′ P
force ⊕-idempotent′ = ⊕-idempotent

-- _⊕_ is commutative.

⊕-comm : ∀ {P Q} → P ⊕ Q ∼ Q ⊕ P
⊕-comm = ⟨ lr , Σ-map id (Σ-map id symmetric) ∘ lr ⟩
  where
  lr : ∀ {P Q R μ} →
       P ⊕ Q [ μ ]⟶ R → ∃ λ R′ → Q ⊕ P [ μ ]⟶ R′ × R ∼′ R′
  lr {P} {Q} {R} = λ where
    (sum-left  P⟶R) →
      R      ■ ⟵⟨ sum-right P⟶R ⟩
      Q ⊕ P

    (sum-right Q⟶R) →
      R      ■ ⟵⟨ sum-left Q⟶R ⟩
      Q ⊕ P

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
-- A certified implementation of the extended Euclidian algorithm,
-- which in addition to the gcd also computes the coefficients of
-- Bézout's identity. That is, integers x and y, such that
-- ax + by = gcd a b.

-- See https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm
-- for details.

module Numeric.Nat.GCD.Extended where

open import Prelude
open import Control.WellFounded
open import Numeric.Nat.Divide
open import Numeric.Nat.DivMod
open import Numeric.Nat.GCD
open import Tactic.Nat
open import Tactic.Cong

-- Bézout coefficients always have opposite signs, so we can represent
-- a Bézout identity using only natural numbers, keeping track of which
-- coefficient is the positive one.
data BézoutIdentity (d a b : Nat) : Set where
  bézoutL : (x y : Nat) → a * x ≡ d + b * y → BézoutIdentity d a b
  bézoutR : (x y : Nat) → b * y ≡ d + a * x → BézoutIdentity d a b

-- The result of the extended gcd algorithm is the same as for the normal
-- one plus a BézoutIdentity.
record ExtendedGCD (a b : Nat) : Set where
  no-eta-equality
  constructor gcd-res
  field d      : Nat
        isGCD  : IsGCD d a b
        bézout : BézoutIdentity d a b

private
  -- This is what the recursive calls compute. At the top we get
  -- ExtendedGCD′ a b a b, which we can turn into ExtendedGCD a b.
  -- We need this because the correctness of the Bézout coefficients
  -- is established going down and the correctness of the gcd going
  -- up.
  record ExtendedGCD′ (a b r₀ r₁ : Nat) : Set where
    no-eta-equality
    constructor gcd-res
    field d      : Nat
          isGCD  : IsGCD d r₀ r₁
          bézout : BézoutIdentity d a b

  -- Erasing the proof objects.
  eraseBézout : ∀ {a b d} → BézoutIdentity d a b → BézoutIdentity d a b
  eraseBézout (bézoutL x y eq) = bézoutL x y (eraseEquality eq)
  eraseBézout (bézoutR x y eq) = bézoutR x y (eraseEquality eq)

  -- Convert from ExtendedGCD′ as we erase, because why not.
  eraseExtendedGCD : ∀ {a b} → ExtendedGCD′ a b a b → ExtendedGCD a b
  eraseExtendedGCD (gcd-res d p i) = gcd-res d (eraseIsGCD p) (eraseBézout i)

private

  -- The algorithm computes a sequence of coefficients xᵢ and yᵢ (sᵢ and tᵢ on
  -- Wikipedia) that terminates in the Bézout coefficients for a and b. The
  -- invariant is that they satisfy the Bézout identity for the current remainder.
  -- Moreover, at each step they flip sign, so we can represent two consecutive
  -- pairs of coefficients as follows.
  data BézoutState (a b r₀ r₁ : Nat) : Set where
    bézoutLR : ∀ x₀ x₁ y₀ y₁ (eq₀ : a * x₀ ≡ r₀ + b * y₀)
                             (eq₁ : b * y₁ ≡ r₁ + a * x₁) → BézoutState a b r₀ r₁
    bézoutRL : ∀ x₀ x₁ y₀ y₁ (eq₀ : b * y₀ ≡ r₀ + a * x₀)
                             (eq₁ : a * x₁ ≡ r₁ + b * y₁) → BézoutState a b r₀ r₁

  -- In the base case the last remainder is 0, and the second to last is the gcd,
  -- so we get the Bézout coefficients from the first components in the state.
  getBézoutIdentity : ∀ {d a b} → BézoutState a b d 0 → BézoutIdentity d a b
  getBézoutIdentity (bézoutLR x₀ _ y₀ _ eq₀ _) = bézoutL x₀ y₀ eq₀
  getBézoutIdentity (bézoutRL x₀ _ y₀ _ eq₀ _) = bézoutR x₀ y₀ eq₀

  -- It's important for compile time performance to be strict in the computed
  -- coefficients. Can't do a dependent force here due to the proof object. Note
  -- that we only have to be strict in x₁ and y₁, since x₀ and y₀ are simply
  -- the x₁ and y₁ of the previous state.
  forceState : ∀ {a b r₀ r₁} {C : Set} → BézoutState a b r₀ r₁ → (BézoutState a b r₀ r₁ → C) → C
  forceState (bézoutLR x₀ x₁ y₀ y₁ eq₀ eq₁) k =
    force′ x₁ λ x₁′ eqx → force′ y₁ λ y₁′ eqy →
    k (bézoutLR x₀ x₁′ y₀ y₁′ eq₀ (case eqx of λ where refl → case eqy of λ where refl → eq₁))
  forceState (bézoutRL x₀ x₁ y₀ y₁ eq₀ eq₁) k =
    force′ x₁ λ x₁′ eqx → force′ y₁ λ y₁′ eqy →
    k (bézoutRL x₀ x₁′ y₀ y₁′ eq₀ (case eqx of λ where refl → case eqy of λ where refl → eq₁))

  -- We're starting of the algorithm with two first remainders being a and b themselves.
  -- The corresponding coefficients are x₀, x₁ = 1, 0 and y₀, y₁ = 0, 1.
  initialState : ∀ {a b} → BézoutState a b a b
  initialState = bézoutLR 1 0 0 1 auto auto

  module _ {r₀ r₁ r₂} q where
    -- The proof that new coefficients satisfy the invariant.
    -- Note alternating sign: x₀ pos, x₁ neg, x₂ pos.
    lemma : (a b x₀ x₁ y₀ y₁ : Nat) →
            q * r₁ + r₂ ≡ r₀ →
            a * x₀ ≡ r₀ + b * y₀ →
            b * y₁ ≡ r₁ + a * x₁ →
            a * (x₀ + q * x₁) ≡ r₂ + b * (y₀ + q * y₁)
    lemma a b x₀ x₁ y₀ y₁ refl eq₀ eq₁ =
        a * (x₀ + q * x₁)
          ≡⟨ by eq₀ ⟩
        r₂ + b * y₀ + q * (r₁ + a * x₁)
          ≡⟨ by-cong eq₁ ⟩
        r₂ + b * y₀ + q * (b * y₁)
          ≡⟨ auto ⟩
        r₂ + b * (y₀ + q * y₁) ∎

    -- The sequence of coefficients is defined by
    --   xᵢ₊₁ = xᵢ₋₁ + q * xᵢ
    --   yᵢ₊₁ = yᵢ₋₁ + q * yᵢ
    -- where q is defined by the step in the normal Euclidian algorithm
    --   rᵢ₊₁ = rᵢ₋₁ + q * rᵢ
    bézoutState-step : ∀ {a b} → q * r₁ + r₂ ≡ r₀ → BézoutState a b r₀ r₁ → BézoutState a b r₁ r₂
    bézoutState-step {a} {b} eq (bézoutLR x₀ x₁ y₀ y₁ eq₀ eq₁) =
      bézoutRL x₁ (x₀ + q * x₁) y₁ (y₀ + q * y₁) eq₁ (lemma a b x₀ x₁ y₀ y₁ eq eq₀ eq₁)
    bézoutState-step {a} {b} eq (bézoutRL x₀ x₁ y₀ y₁ eq₀ eq₁) =
      bézoutLR x₁ (x₀ + q * x₁) y₁ (y₀ + q * y₁) eq₁ (lemma b a y₀ y₁ x₀ x₁ eq eq₀ eq₁)

    extendedGCD-step : ∀ {a b} → q * r₁ + r₂ ≡ r₀ → ExtendedGCD′ a b r₁ r₂ → ExtendedGCD′ a b r₀ r₁
    extendedGCD-step eq (gcd-res d p i) = gcd-res d (isGCD-step q eq p) i

private
  extendedGCD-acc : {a b : Nat} → (r₀ r₁ : Nat) →
                    BézoutState a b r₀ r₁ →
                    Acc _<_ r₁ → ExtendedGCD′ a b r₀ r₁
  extendedGCD-acc r₀ zero s _ =
    gcd-res r₀ (is-gcd (factor 1 auto) (factor! 0) λ k p _ → p) (getBézoutIdentity s)
  extendedGCD-acc r₀ (suc r₁) s (acc wf) =
    forceState s λ s → -- make sure to be strict in xᵢ and yᵢ
    case r₀ divmod suc r₁ of λ where
      (qr q r₂ lt eq) →
        extendedGCD-step q eq (extendedGCD-acc (suc r₁) r₂ (bézoutState-step q eq s) (wf r₂ lt))

-- The extended Euclidian algorithm. Easily handles inputs of several hundred digits.
extendedGCD : (a b : Nat) → ExtendedGCD a b
extendedGCD a b = eraseExtendedGCD (extendedGCD-acc a b initialState (wfNat b))

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Naturals where

import  Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

-- type definition
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- bind builtin (aka Haskell integers) to my natural type
{-# BUILTIN NATURAL ℕ #-}

-- define addition proof
-- base case for identity rule
-- inductive case for associative rule
_+_ : ℕ → ℕ → ℕ
zero + n  = n
suc m + n = suc (m + n)

-- 2 + 3 proposition is reflexive
-- that means addition is a binary
-- relation that relates to itself
_ : 2 + 3 ≡ 5
_ = refl

-- same for 3 + 4 propositon
-- i manually proved it
_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 0)) + suc 3
  ≡⟨⟩
    suc (suc (suc 0)) + suc (suc 2)
  ≡⟨⟩
    suc (suc (suc 0)) + suc (suc (suc 1))
  ≡⟨⟩
    suc (suc (suc 0)) + suc (suc (suc (suc 0)))
  ≡⟨⟩
    7
  ∎
-- after addition we can efine
-- multiplication in terms of it
-- note the base case and the inductive case
_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)

_ =
  begin
    2 * 3
  ≡⟨⟩
    3 + (1 * 3)
  ≡⟨⟩
    3 + (3 + (0 * 3))
  ≡⟨⟩
    3 + (3 + 0)
  ≡⟨⟩
    6
  ∎

_ =
  begin
    3 * 4
  ≡⟨⟩
    4 + (2 * 4)
  ≡⟨⟩
    4 + (4 + (1 * 4))
  ≡⟨⟩
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩
    12
  ∎

-- with multiplication we then can
-- define exponentiation
-- note that `m ^ zero` /= `zero ^ m`
_^_ : ℕ → ℕ → ℕ
n ^ zero  = 1
m ^ suc n = m * (m ^ n)

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
    3 * (3 ^ 3)
  ≡⟨⟩
    3 * (3 * (3 ^ 2))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ 0))))
  ≡⟨⟩
    81
  ∎

_∸_ : ℕ → ℕ → ℕ
m ∸ zero      = m
zero ∸ suc n  = zero
suc m ∸ suc n = m ∸ n

_ : 3 ∸ 2 ≡ 1
_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ : 2 ∸ 3 ≡ 0
_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

_ : 5 ∸ 3 ≡ 2
_ =
  begin
    5 ∸ 3
  ≡⟨⟩
    4 ∸ 2
  ≡⟨⟩
    3 ∸ 1
  ≡⟨⟩
    2 ∸ 0
  ≡⟨⟩
    2
  ∎

_ : 3 ∸ 5 ≡ 0
_ =
  begin
    3 ∸ 5
  ≡⟨⟩
    2 ∸ 4
  ≡⟨⟩
    1 ∸ 3
  ≡⟨⟩
    0 ∸ 2
  ≡⟨⟩
    0
  ∎

-- here we define the precedence
-- of operators. all they are left associative
-- and addiction and monus have precedence less
-- than multiplication
infixl 6 _+_ _∸_
infixl 7 _*_
infixl 8 _^_

-- binding aforementioned operators
-- to the relevant Haskell integer operators
{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

max_stars_repo_name: matdsoupe/paradigmas

max_issues_repo_name: matdsoupe/paradigmas

max_forks_repo_name: matdsoupe/paradigmas


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

open import Sets.Cardinality.Infinite.Definition
open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Groups.FreeGroup.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Decidable.Sets
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Semirings.Definition
open import Functions.Definition
open import Functions.Lemmas
open import Groups.Isomorphisms.Definition
open import Groups.FreeGroup.Word
open import Groups.FreeGroup.Group
open import Groups.FreeGroup.UniversalProperty
open import Groups.Abelian.Definition
open import Groups.QuotientGroup.Definition
open import Groups.Lemmas
open import Groups.Homomorphisms.Lemmas

module Groups.FreeGroup.Lemmas {a : _} {A : Set a} (decA : DecidableSet A) where

freeGroupNonAbelian : AbelianGroup (freeGroup decA) → (a : A) → Sg (A → True) Bijection
freeGroupNonAbelian record { commutative = commutative } a = (λ _ → record {}) , b
  where
    b : Bijection (λ _ → record {})
    Bijection.inj b {x} {y} _ with decA x y
    ... | inl pr = pr
    ... | inr neq = exFalso (neq (ofLetterInjective (prependLetterInjective' decA t)))
      where
        t : prependLetter {decA = decA} (ofLetter x) (prependLetter (ofLetter y) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl) ≡ prependLetter (ofLetter y) (prependLetter (ofLetter x) empty (wordEmpty refl)) (wordEnding (succIsPositive 0) refl)
        t = commutative {prependLetter (ofLetter x) empty (wordEmpty refl)} {prependLetter (ofLetter y) empty (wordEmpty refl)}
    Bijection.surj b record {} = a , refl

private
  iso : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decA → ReducedWord decB
  iso decB {f} bij = universalPropertyFunction decA (freeGroup decB) λ a → freeEmbedding decB (f a)

  isoHom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decA) (freeGroup decB) (iso decB bij)
  isoHom decB {f} bij = universalPropertyHom decA (freeGroup decB) λ a → iso decB bij (freeEmbedding decA a)

  iso2 : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → ReducedWord decB → ReducedWord decA
  iso2 decB {f} bij = universalPropertyFunction decB (freeGroup decA) λ b → freeEmbedding decA (Invertible.inverse (bijectionImpliesInvertible bij) b)

  iso2Hom : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → GroupHom (freeGroup decB) (freeGroup decA) (iso2 decB bij)
  iso2Hom decB {f} bij = universalPropertyHom decB (freeGroup decA) λ b → iso2 decB bij (freeEmbedding decB b)

  fixesF : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : A) → iso2 decB bij (iso decB bij (freeEmbedding decA x)) ≡ freeEmbedding decA x
  fixesF decB {f} bij x with Bijection.surj bij (f x)
  ... | _ , pr rewrite Bijection.inj bij pr = refl

  fixesF' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : B) → iso decB bij (iso2 decB bij (freeEmbedding decB x)) ≡ freeEmbedding decB x
  fixesF' decB {f} bij x with Bijection.surj bij x
  ... | _ , pr rewrite pr = refl

  uniq : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → x ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
  uniq decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF decB bij) x
  uniqLemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ universalPropertyFunction decA (freeGroup decA) (λ x → iso2 decB bij (iso decB bij (freeEmbedding decA x))) x
  uniqLemm decB {f} bij x = universalPropertyUniqueness decA (freeGroup decA) (λ i → freeEmbedding decA (underlying (Bijection.surj bij (f i)))) {λ i → iso2 decB bij (iso decB bij i)} (groupHomsCompose (isoHom decB bij) (iso2Hom decB bij)) (λ _ → refl) x
  uniq! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decA) → iso2 decB bij (iso decB bij x) ≡ x
  uniq! decB bij x = transitivity (uniqLemm decB bij x) (equalityCommutative (uniq decB bij x))

  uniq' : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → x ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
  uniq' decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) {id} (record { wellDefined = id ; groupHom = refl }) (fixesF' decB bij) x
  uniq'Lemm : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ universalPropertyFunction decB (freeGroup decB) (λ x → iso decB bij (iso2 decB bij (freeEmbedding decB x))) x
  uniq'Lemm decB {f} bij x = universalPropertyUniqueness decB (freeGroup decB) (λ i → freeEmbedding decB (f (Invertible.inverse (bijectionImpliesInvertible bij) i))) {λ i → iso decB bij (iso2 decB bij i)} (groupHomsCompose (iso2Hom decB bij) (isoHom decB bij)) (λ _ → refl) x
  uniq'! : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → (bij : Bijection f) → (x : ReducedWord decB) → iso decB bij (iso2 decB bij x) ≡ x
  uniq'! decB bij x = transitivity (uniq'Lemm decB bij x) (equalityCommutative (uniq' decB bij x))

  inBijection : {b : _} {B : Set b} (decB : DecidableSet B) {f : A → B} (bij : Bijection f) → Bijection (iso decB bij)
  inBijection decB bij = invertibleImpliesBijection (record { inverse = iso2 decB bij ; isLeft = uniq'! decB bij ; isRight = uniq! decB bij })

freeGroupFunctorWellDefined : {b : _} {B : Set b} (decB : DecidableSet B) → {f : A → B} → Bijection f → GroupsIsomorphic (freeGroup decA) (freeGroup decB)
GroupsIsomorphic.isomorphism (freeGroupFunctorWellDefined decB {f} bij) = iso decB bij
GroupIso.groupHom (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)) = universalPropertyHom decA (freeGroup decB) λ a → freeEmbedding decB (f a)
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} {y} pr = Bijection.inj (inBijection decB bij) pr
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) refl = refl
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (GroupsIsomorphic.proof (freeGroupFunctorWellDefined decB {f} bij)))) {x} = Bijection.surj (inBijection decB bij) x

{-
freeGroupFunctorInjective : {b : _} {B : Set b} (decB : DecidableSet B) → GroupsIsomorphic (freeGroup decA) (freeGroup decB) → Sg (A → B) (λ f → Bijection f)
freeGroupFunctorInjective decB iso = {!!}

everyGroupQuotientOfFreeGroup : {b : _} → (S : Setoid {a} {b} A) → {_+_ : A → A → A} → (G : Group S _+_) → GroupsIsomorphic G (quotientGroupByHom (freeGroup decA) (universalPropertyHom decA {!!} {!!}))
everyGroupQuotientOfFreeGroup = {!!}

everyFGGroupQuotientOfFGFreeGroup : {!!}
everyFGGroupQuotientOfFGFreeGroup = {!!}

freeGroupTorsionFree : {!!}
freeGroupTorsionFree = {!!}
-}

private
  mapNToGrp : (a : A) → (n : ℕ) → ReducedWord decA
  mapNToGrpLen : (a : A) → (n : ℕ) → wordLength decA (mapNToGrp a n) ≡ n
  mapNToGrpFirstLetter : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → firstLetter decA (mapNToGrp a (succ n)) pr ≡ (ofLetter a)
  lemma : (a : A) → (n : ℕ) → .(pr : 0 <N wordLength decA (mapNToGrp a (succ n))) → ofLetter a ≡ freeInverse (firstLetter decA (mapNToGrp a (succ n)) pr) → False

  lemma a zero _ ()
  lemma a (succ n) _ ()

  mapNToGrp a zero = empty
  mapNToGrp a 1 = prependLetter (ofLetter a) empty (wordEmpty refl)
  mapNToGrp a (succ (succ n)) = prependLetter (ofLetter a) (mapNToGrp a (succ n)) (wordEnding (identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n)))) (freeCompletionEqualFalse decA λ p → lemma a n ((identityOfIndiscernablesRight _<N_ (succIsPositive n) (equalityCommutative (mapNToGrpLen a (succ n))))) p))

  mapNToGrpFirstLetter a zero pr = refl
  mapNToGrpFirstLetter a (succ n) pr = refl

  mapNToGrpLen a zero = refl
  mapNToGrpLen a (succ zero) = refl
  mapNToGrpLen a (succ (succ n)) = applyEquality succ (mapNToGrpLen a (succ n))

  mapNToGrpInj : (a : A) → (x y : ℕ) → mapNToGrp a x ≡ mapNToGrp a y → x ≡ y
  mapNToGrpInj a zero zero pr = refl
  mapNToGrpInj a zero (succ zero) ()
  mapNToGrpInj a zero (succ (succ y)) ()
  mapNToGrpInj a (succ zero) zero ()
  mapNToGrpInj a (succ (succ x)) zero ()
  mapNToGrpInj a (succ zero) (succ zero) pr = refl
  mapNToGrpInj a (succ zero) (succ (succ y)) pr = exFalso (naughtE (transitivity (applyEquality (wordLength decA) (prependLetterInjective decA pr)) (mapNToGrpLen a (succ y))))
  mapNToGrpInj a (succ (succ x)) (succ 0) pr = exFalso (naughtE (transitivity (equalityCommutative (applyEquality (wordLength decA) (prependLetterInjective decA pr))) (mapNToGrpLen a (succ x))))
  mapNToGrpInj a (succ (succ x)) (succ (succ y)) pr = applyEquality succ (mapNToGrpInj a (succ x) (succ y) (prependLetterInjective decA pr))

freeGroupInfinite : (nonempty : A) → DedekindInfiniteSet (ReducedWord decA)
DedekindInfiniteSet.inj (freeGroupInfinite nonempty) = mapNToGrp nonempty
DedekindInfiniteSet.isInjection (freeGroupInfinite nonempty) {x} {y} = mapNToGrpInj nonempty x y


text:
open import Agda.Primitive.Cubical

test : (J : IUniv) → J → J
test J j = primHComp {φ = i0} (λ k → λ ()) j

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.meta:45 #-}

-- Andreas, 2014-12-07 found a bug in pruning

open import Common.Prelude
open import Common.Product
open import Common.Equality

postulate
  f : Bool → Bool

test : let
    X : Bool → Bool → Bool
    X = _
    Y : Bool
    Y = _
  in ∀ b → Y ≡ f (X b (f (if true then true else b))) ×
            (∀ a → X a (f b) ≡ f b)
test b = refl , λ a → refl

-- ERROR WAS:

-- Cannot instantiate the metavariable _22 to solution f b since it
-- contains the variable b which is not in scope of the metavariable
-- or irrelevant in the metavariable but relevant in the solution
-- when checking that the expression refl has type (_22 ≡ f b)

-- Here, Agda complains although there is a solution

--   X a b = b
--   Y = f (f true)

-- Looking at the first constraint

--   Y = f (X b (f (if true then true else b)))

-- agda prunes *both* arguments of X since they have rigid occurrences
-- of b.  However, the second occurrences goes away by normalization:

--   Y = f (X b (f true))

-- For efficiency reasons, see issue 415 , Agda first does not
-- normalize during occurs check.  Thus, the free variable check for
-- the arg (if true then true else b) returns b as rigid, which means
-- we have a neutral term (f (...b...)) with a rigid occurrence of bad
-- variable b, and we prune this argument of meta X.  This is unsound,
-- since the free variable check only returns a superset of the actual
-- (semantic) variable dependencies.

-- NOW: metas should be unsolved.


text:
-- 2012-02-13 Andreas: testing correct polarity of data types
-- sized types are the only source of subtyping, I think...

{-# OPTIONS --sized-types #-}
module DataPolarity where

open import Common.Size

data Nat : {size : Size} -> Set where
  zero : {size : Size} -> Nat {↑ size}
  suc  : {size : Size} -> Nat {size} -> Nat {↑ size}

data Pair (A : Set) : Set where
  _,_ : A -> A -> Pair A

split : {i : Size} → Nat {i} → Pair (Nat {i})
split zero = zero , zero
split (suc n) with split n
... | (l , r) = suc r , l
-- this should work, due to the monotonicity of Pair
-- without subtyping, Agda would complain about i != ↑ i

MyPair : Nat → Set → Set
MyPair zero A = Pair A
MyPair (suc n) A = MyPair n A
-- polarity should be preserved by functions

mysplit : {i : Size} → (n : Nat {i}) → MyPair (suc zero) (Nat {i})
mysplit zero = zero , zero
mysplit (suc n) with mysplit n
... | (l , r) = suc r , l

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --allow-unsolved-metas #-}

module Control.Lens where

open import Function using (id; _∘_; const; flip)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Util.Equality

open import Control.Functor renaming (Comp to _•_)
open import Control.Functor.NaturalTransformation renaming (Id to Nid; Comp to _·_)

-- S-combinator.

apply : ∀ {A B C : Set} → (A → B → C) → (A → B) → A → C
apply f g a = f a (g a)

-- Flipped S-combinator (flipped apply).

flipply : ∀ {O A B : Set} → (A → O → B) → (O → A) → O → B
flipply f g o = f (g o) o

record GetSetLens (O I : Set) : Set where

  -- Operations.

  field
    get : O → I
    set : I → O → O

  -- Laws.

  field
    set-set : ∀ {i j} → set i ∘ set j   ≡ set i
    get-set : ∀ {i}   → get ∘ set i     ≡ const i
    set-get :           flipply set get ≡ id      -- ∀ {o} → set (get o) o ≡ o

-- A variant of GetSetLens

record GetsModifyLens (O I : Set) : Set₁ where

  -- Operations.

  field
    gets   : ∀ {J} → (I → J) → O → J
    modify : (I → I) → O → O

  -- Laws.

  field
    -- modify is an endofunctor in the discrete category I.

    modify-id     :

      modify id ≡ id

    modify-∘ : ∀ {f g} →

      modify g ∘ modify f ≡ modify (g ∘ f)

    -- Free theorem for gets.

    gets-free     : ∀ {J K} {f : J → K} (g : I → J) →

      f ∘ gets g ≡ gets (f ∘ g)

    gets-modify   : ∀ {J} {f : I → I} {g : I → J} →

      gets g ∘ modify f ≡ gets (g ∘ f)

    -- set (get o) o ≡ o
    -- modify (const (gets id o)) o ≡ o
    -- modify (const (gets f  o)) o ≡ modify f o
    -- modify (λ i → g (gets f o) i) o ≡ modify (λ i → g i (f i)) o
    -- apply (flip modify) (g ∘ gets f) ≡ modify (apply g f)

    modify-gets   : ∀ {J} {g : I → J} (s : J → I → I) →

      flipply modify (s ∘ gets g) ≡ modify (flipply s g)

  getSetLens : GetSetLens O I
  getSetLens = record
    { get     = gets id
    ; set     = modify ∘ const
    ; set-set = modify-∘
    ; get-set = get-set
    ; set-get = set-get
    }
    where
      get : O → I
      get = gets id

      set : I → O → O
      set = modify ∘ const

      get-set : ∀ {i} → get ∘ set i ≡ const i
      get-set {i} =
        begin
          get ∘ set i                ≡⟨⟩
          gets id ∘ modify (const i) ≡⟨ gets-modify ⟩
          gets (id ∘ const i)        ≡⟨⟩
          gets (const i ∘ id)        ≡⟨ sym (gets-free id)  ⟩
          const i ∘ get              ≡⟨⟩
          const i
        ∎

      set-get : flipply set get ≡ id
      set-get = begin
        flipply set get                     ≡⟨⟩
        flipply (modify ∘ const) (gets id)  ≡⟨⟩
        flipply modify (const ∘ gets id)    ≡⟨ modify-gets const ⟩
        modify (flipply const id)           ≡⟨⟩
        modify id                           ≡⟨ modify-id ⟩
        id                                  ∎

  open GetSetLens getSetLens public

-- van Laarhoven lenses

record Lens (O I : Set) : Set₁ where

  -- Single operation: Functorial modify.
  field
    modify! : ∀ (FF : Functor) → let F = Functor.F FF in
      (I → F I) → (O → F O)

  -- Laws
  -- 0. Free theorem:
  field

    modify!-free : (FF GG : Functor) (N : NatTrans FF GG) →

      let open Functor FF using () renaming (F to F; map to mapF) in
      let open Functor GG using () renaming (F to G; map to mapG) in
      let open NatTrans N using () renaming (eta to η) in

      (f : I → F I) →

        η ∘ modify! FF f ≡ modify! GG (η ∘ f)

  -- 1. Identity law:  -- Generalize?

    modify!-id :

        modify! Id id ≡ id

  -- 2. Composition law:

    modify!-∘ : (FF GG : Functor) →

      let open Functor FF using () renaming (F to F; map to mapF) in
      let open Functor GG using () renaming (F to G; map to mapG) in

      {f : I → F I} →
      {g : I → G I} →

        mapF (modify! GG g) ∘ modify! FF f

          ≡  modify! (FF • GG) (mapF g ∘ f)

  getsModifyLens : GetsModifyLens O I
  getsModifyLens  = record
    { gets        = gets
    ; modify      = modify
    ; modify-id   = modify!-id
    ; modify-∘    = modify-∘
    ; gets-free   = λ {J}{K}{f} g → gets-free f g
    ; gets-modify = gets-modify
    ; modify-gets = modify-gets
    }
    where

    -- gets and modify

      gets : ∀ {J} → (I → J) → (O → J)
      gets {J = J} = modify! (Const J)

      modify : (I → I) → O → O
      modify = modify! Id

      -- Laws of gets and modify.

      modify-∘ : ∀ {f g} → modify g ∘ modify f ≡ modify (g ∘ f)
      modify-∘ = modify!-∘ Id Id

      gets-free : ∀ {J K} (f : J → K) (g : I → J) → f ∘ gets g ≡ gets (f ∘ g)
      gets-free {J = J}{K = K} f g = modify!-free (Const J) (Const K) (ConstNat f) g

      gets-modify : ∀ {J} {f : I → I} {g : I → J} →
        gets g ∘ modify f ≡ gets (g ∘ f)
      gets-modify {J = J} = modify!-∘ Id (Const J)

      modify-gets : ∀ {J} {g : I → J} (s : J → I → I) →
        flipply modify (s ∘ gets g) ≡ modify (flipply s g)
      modify-gets = {!!}  -- TODO! Difficult.

  open GetsModifyLens getsModifyLens public

-- Every GetSetLens is a van Laarhoven lens ??

lensFromGetSet : ∀ {O I} → GetSetLens O I → Lens O I
lensFromGetSet {O = O}{I = I} l = record
  { modify!      = modify!
  ; modify!-free = {!!}
  ; modify!-id   = set-get
  ; modify!-∘    = modify!-∘
  }
  where
    open GetSetLens l

    module Define-modify! (FF : Functor) where
      open Functor FF

      modify! : (I → F I) → (O → F O)
      modify! f = apply (map ∘ flip set) (f ∘ get)

      derivation-of-modify : ∀ f → modify! f ≡ apply (map ∘ flip set) (f ∘ get)
      derivation-of-modify f = begin
        modify! f
        ≡⟨⟩  (λ o → f (get o) <&> λ i → set i o)
        ≡⟨⟩  (λ o → ((λ o → map (λ i → set i o)) o) ((f ∘ get) o))
        ≡⟨⟩  apply (λ o → map (λ i → set i o)) (f ∘ get)
        ≡⟨⟩  apply (λ o → map (flip set o)) (f ∘ get)
        ≡⟨⟩  apply (map ∘ flip set) (f ∘ get)
        ∎
    open Define-modify!

    modify!-free : (FF GG : Functor) (N : NatTrans FF GG) →

      let open Functor FF using () renaming (F to F; map to mapF) in
      let open Functor GG using () renaming (F to G; map to mapG) in
      let open NatTrans N using () renaming (eta to η) in

      (f : I → F I) →

        η ∘ modify! FF f ≡ modify! GG (η ∘ f)

    modify!-free FF GG N f = fun-ext λ o → begin

        η (modify! FF f o)                       ≡⟨⟩

        η (mapF (λ i → set i o) (f (get o)))     ≡⟨ app-naturality (flip set) (f ∘ get) o ⟩

        mapG (λ i → set i o) (η (f (get o)))     ≡⟨⟩

        modify! GG (η ∘ f) o                     ∎

      where
        open Functor FF using () renaming (F to F; map to mapF; map-∘ to mapF-∘)
        open Functor GG using () renaming (F to G; map to mapG; map-∘ to mapG-∘)
        open NatTrans N using (app-naturality) renaming (eta to η)

    modify!-id : modify! Id id ≡ id
    modify!-id = fun-ext λ o → begin
      (Functor.map Id) (λ i → set i o) (id (get o))  ≡⟨⟩
      (λ i → set i o) (get o)                        ≡⟨⟩
      set (get o) o                                  ≡⟨⟩
      flipply set get o                              ≡⟨ app-≡ o set-get ⟩
      id o                                           ≡⟨⟩
      o                                              ∎

    modify!-∘ : (FF GG : Functor) →

      let open Functor FF using () renaming (F to F; map to mapF) in
      let open Functor GG using () renaming (F to G; map to mapG) in

      {f : I → F I} →
      {g : I → G I} →

        mapF (modify! GG g) ∘ modify! FF f

          ≡  modify! (FF • GG) (mapF g ∘ f)

    modify!-∘ FF GG {f = f} {g = g} = fun-ext λ o → begin

      mapF (modify! GG g) (modify! FF f o)                           ≡⟨⟩

      mapF  (λ o → mapG (λ i → set i o) (g (get o)))
                  (mapF (λ i → set i o) (f (get o)))                 ≡⟨ app-≡ _ (sym mapF-∘) ⟩

      mapF ((λ o → mapG (λ i → set i o) (g (get o)))
                      ∘ (λ i → set i o))(f (get o))                  ≡⟨⟩

      mapF (λ j → mapG (λ i → set i (set j o)) (g (get (set j o))))
           (f (get o))                                               ≡⟨ {!set-set!} ⟩

      mapF (λ j → mapG (λ i → set i o) (g (get (set j o))))
           (f (get o))                                               ≡⟨ {!get-set!} ⟩

      mapF (λ j → mapG (λ i → set i o) (g j))
           (f (get o))                                               ≡⟨⟩

      mapF (mapG (λ i → set i o) ∘ g) (f (get o))                    ≡⟨ app-≡ _ mapF-∘ ⟩

      mapF (mapG (λ i → set i o)) (mapF g (f (get o)))               ≡⟨⟩

      mapFG (λ i → set i o) (mapF g (f (get o)))                     ≡⟨⟩

      modify! (FF • GG) (mapF g ∘ f) o                               ∎

      where
        open Functor FF using () renaming (F to F; map to mapF; map-∘ to mapF-∘)
        open Functor GG using () renaming (F to G; map to mapG; map-∘ to mapG-∘)
        mapFG = Functor.map (FF • GG)
{-
  Lens operations:

    get : Lens I O → O → I
    get l o = l (mapK I) id o

    set : Len I O → I → O → O
    set l i o = l mapId (const i) o

  Lens laws:

  a. set-set

       set l i ∘ set l j = set l i

     Prove from 2.

  b. get-set

       get l (set l i o) = i

     Prove from 0. + 2.

  c. set-get

     set l o (get l o) = o

       This states that set is surjective, it is equivalent to

     ∀ o → ∃₂ λ i o′ → set l o′ i = o

  Independence of 0, 1, 2.
  -----------------------

  A. 0 does not imply 2.  Counterexample:

    -- An impossible lens, since ⊤ contains nothing, especially not Bool

    l : Lens Bool ⊤
    l map f = map (const tt) (f true)

      ( get l _   = false )
      ( set l _ _ = tt    )

    does not satisfy 2.  (Lens composition)

      mapId (l (mapK Bool) id) ∘ l mapId not
    = const ((mapK Bool) (const tt) true)
    = const true

      l (mapK Bool) (id ∘ not)
    = const ((mapK Bool) (const tt) (not true)
    = const false

  B. 0, 2 are not sufficent to prove c.  Counterexample:

    -- Lens focusing on nothing.

    l : Lens ⊤ Bool

    l map f _ = map (const true) (f tt)

      ( get l _   = tt   )
      ( set l _ _ = true )
      so,  set l false (get l false) /= false

    Proof of 2:

-}

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
-- This module closely follows a section of Martín Escardó's HoTT lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#unicharac
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.ContrFormulation where

open import Util.Data.Product using (map₂)
open import Util.Prelude
open import Util.HoTT.Equiv
open import Util.HoTT.HLevel.Core
open import Util.HoTT.Singleton
open import Util.HoTT.Univalence.Axiom
open import Util.HoTT.Univalence.Statement

private
  variable
    α β γ : Level

UnivalenceContr : ∀ α → Set (lsuc α)
UnivalenceContr α = (A : Set α) → IsContr (Σ[ B ∈ Set α ] (A ≃ B))

UnivalenceProp : ∀ α → Set (lsuc α)
UnivalenceProp α = (A : Set α) → IsProp (Σ[ B ∈ Set α ] (A ≃ B))

abstract
  IsEquiv→Σ-IsContr : {A : Set α} {B : A → Set β} (x : A)
    → (f : ∀ y → x ≡ y → B y)
    → (∀ y → IsEquiv (f y))
    → IsContr (Σ A B)
  IsEquiv→Σ-IsContr {A = A} {B = B} x f f-equiv
    = ≃-pres-IsContr Singleton≃ΣB IsContr-Singleton′
    where
      ≡≃B : ∀ y → (x ≡ y) ≃ B y
      ≡≃B y .forth = f y
      ≡≃B y .isEquiv = f-equiv y

      Singleton≃ΣB : Singleton′ x ≃ Σ A B
      Singleton≃ΣB = Σ-≃⁺ ≡≃B

  Σ-IsContr→IsEquiv : {A : Set α} {B : A → Set β} (x : A)
    → (f : ∀ y → x ≡ y → B y)
    → IsContr (Σ A B)
    → ∀ y → IsEquiv (f y)
  Σ-IsContr→IsEquiv {A = A} {B = B} x f Σ-contr
    = IsEquiv-map₂-f→IsEquiv-f f f-equiv
    where
      f-equiv : IsEquiv (map₂ f)
      f-equiv = IsContr→IsEquiv IsContr-Singleton′ Σ-contr (map₂ f)

  Univalence→UnivalenceContr : Univalence α → UnivalenceContr α
  Univalence→UnivalenceContr ua A = IsEquiv→Σ-IsContr A (λ B → ≡→≃) (λ B → ua)

  UnivalenceContr→Univalence : UnivalenceContr α → Univalence α
  UnivalenceContr→Univalence ua {A} {B}
    = Σ-IsContr→IsEquiv A (λ B → ≡→≃) (ua A) B

  univalenceContr : (A : Set α) → IsContr (Σ[ B ∈ Set α ] (A ≃ B))
  univalenceContr = Univalence→UnivalenceContr univalence

  UnivalenceContr→UnivalenceProp : UnivalenceContr α → UnivalenceProp α
  UnivalenceContr→UnivalenceProp ua = IsContr→IsProp ∘ ua

  UnivalenceProp→UnivalenceContr : UnivalenceProp α → UnivalenceContr α
  UnivalenceProp→UnivalenceContr ua A
    = IsProp∧Pointed→IsContr (ua A) (A , ≃-refl)

  Univalence→UnivalenceProp : Univalence α → UnivalenceProp α
  Univalence→UnivalenceProp
    = UnivalenceContr→UnivalenceProp ∘ Univalence→UnivalenceContr

  UnivalenceProp→Univalence : UnivalenceProp α → Univalence α
  UnivalenceProp→Univalence
    = UnivalenceContr→Univalence ∘ UnivalenceProp→UnivalenceContr

  univalenceProp : ∀ {α} → UnivalenceProp α
  univalenceProp = Univalence→UnivalenceProp univalence

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-# OPTIONS --safe --no-sized-types #-}

open import Agda.Builtin.Size

record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream A j

open Stream

destroy-guardedness : ∀ {A i} → Stream A i → Stream A i
destroy-guardedness xs .head = xs .head
destroy-guardedness xs .tail = xs .tail

repeat : ∀ {A i} → A → Stream A i
repeat x .head = x
repeat x .tail = destroy-guardedness (repeat x)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group.Notation where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Algebra.Group.Base

module GroupNotationG {ℓ : Level} ((_ , G) : Group {ℓ}) where
  0ᴳ = GroupStr.0g G
  _+ᴳ_ = GroupStr._+_ G
  -ᴳ_ = GroupStr.-_ G
  _-ᴳ_ = GroupStr._-_ G
  lIdᴳ = GroupStr.lid G
  rIdᴳ = GroupStr.rid G
  lCancelᴳ = GroupStr.invl G
  rCancelᴳ = GroupStr.invr G
  assocᴳ = GroupStr.assoc G
  setᴳ = GroupStr.is-set G

module GroupNotationᴴ {ℓ : Level} ((_ , G) : Group {ℓ}) where
  0ᴴ = GroupStr.0g G
  _+ᴴ_ = GroupStr._+_ G
  -ᴴ_ = GroupStr.-_ G
  _-ᴴ_ = GroupStr._-_ G
  lIdᴴ = GroupStr.lid G
  rIdᴴ = GroupStr.rid G
  lCancelᴴ = GroupStr.invl G
  rCancelᴴ = GroupStr.invr G
  assocᴴ = GroupStr.assoc G
  setᴴ = GroupStr.is-set G

module GroupNotation₀ {ℓ : Level} ((_ , G) : Group {ℓ}) where
  0₀ = GroupStr.0g G
  _+₀_ = GroupStr._+_ G
  -₀_ = GroupStr.-_ G
  _-₀_ = GroupStr._-_ G
  lId₀ = GroupStr.lid G
  rId₀ = GroupStr.rid G
  lCancel₀ = GroupStr.invl G
  rCancel₀ = GroupStr.invr G
  assoc₀ = GroupStr.assoc G
  set₀ = GroupStr.is-set G

module GroupNotation₁ {ℓ : Level} ((_ , G) : Group {ℓ}) where
  0₁ = GroupStr.0g G
  _+₁_ = GroupStr._+_ G
  -₁_ = GroupStr.-_ G
  _-₁_ = GroupStr._-_ G
  lId₁ = GroupStr.lid G
  rId₁ = GroupStr.rid G
  lCancel₁ = GroupStr.invl G
  rCancel₁ = GroupStr.invr G
  assoc₁ = GroupStr.assoc G
  set₁ = GroupStr.is-set G


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

module Set where

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


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

-- Enriched category over a Monoidal category V

open import Categories.Category using (module Commutation) renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Enriched.Category {o ℓ e} {V : Setoid-Category o ℓ e}
                                    (M : Monoidal V) where

open import Level

open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
open import Categories.Morphism.Reasoning V using (pullˡ; pullʳ; pushˡ)

open Setoid-Category V renaming (Obj to ObjV; id to idV)
  using (_⇒_; _∘_)
open Commutation V
open Monoidal M using (unit; _⊗₀_; _⊗₁_; module associator; module unitorˡ;
  module unitorʳ; assoc-commute-from)
open Shorthands

record Category (v : Level) : Set (o ⊔ ℓ ⊔ e ⊔ suc v) where
  field
    Obj : Set v
    hom : (A B : Obj)   → ObjV
    id  : {A : Obj}     → unit ⇒ hom A A
    ⊚   : {A B C : Obj} → hom B C ⊗₀ hom A B ⇒ hom A C

    ⊚-assoc : {A B C D : Obj} →
      [ (hom C D ⊗₀ hom B C) ⊗₀ hom A B ⇒ hom A D ]⟨
        ⊚ ⊗₁ idV          ⇒⟨ hom B D ⊗₀ hom A B ⟩
        ⊚
      ≈ associator.from   ⇒⟨ hom C D ⊗₀ (hom B C ⊗₀ hom A B) ⟩
        idV ⊗₁ ⊚          ⇒⟨ hom C D ⊗₀ hom A C ⟩
        ⊚
      ⟩
    unitˡ : {A B : Obj} →
      [ unit ⊗₀ hom A B ⇒ hom A B ]⟨
        id ⊗₁ idV         ⇒⟨ hom B B ⊗₀ hom A B ⟩
        ⊚
      ≈ unitorˡ.from
      ⟩
    unitʳ : {A B : Obj} →
      [ hom A B ⊗₀ unit ⇒ hom A B ]⟨
        idV ⊗₁ id         ⇒⟨ hom A B ⊗₀ hom A A ⟩
        ⊚
      ≈ unitorʳ.from
      ⟩

  -- A version of ⊚-assoc using generalized hom-variables.
  --
  -- In this version of associativity, the generalized variables f, g
  -- and h represent V-morphisms, or rather, morphism-valued maps,
  -- such as V-natural transformations or V-functorial actions.  This
  -- version is therefore well-suited for proving derived equations,
  -- such as functorial laws or commuting diagrams, that involve such
  -- maps.  For examples, see Underlying.assoc below, or the modules
  -- Enriched.Functor and Enriched.NaturalTransformation.

  ⊚-assoc-var : {X Y Z : ObjV} {A B C D : Obj}
                {f : X ⇒ hom C D} {g : Y ⇒ hom B C} {h : Z ⇒ hom A B} →
      [ (X ⊗₀ Y) ⊗₀ Z ⇒ hom A D ]⟨
        (⊚ ∘ f ⊗₁ g) ⊗₁ h  ⇒⟨ hom B D ⊗₀ hom A B ⟩
        ⊚
      ≈ associator.from    ⇒⟨ X ⊗₀ (Y ⊗₀ Z) ⟩
        f ⊗₁ (⊚ ∘ g ⊗₁ h)  ⇒⟨ hom C D ⊗₀ hom A C ⟩
        ⊚
      ⟩
  ⊚-assoc-var {f = f} {g} {h} = begin
    ⊚ ∘ (⊚ ∘ f ⊗₁ g) ⊗₁ h                 ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
    ⊚ ∘ ⊚ ⊗₁ idV ∘ (f ⊗₁ g) ⊗₁ h          ≈⟨ pullˡ ⊚-assoc ⟩
    (⊚ ∘ idV ⊗₁ ⊚ ∘ α⇒) ∘ (f ⊗₁ g) ⊗₁ h   ≈⟨ pullʳ (pullʳ assoc-commute-from) ⟩
    ⊚ ∘ idV ⊗₁ ⊚ ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒     ≈˘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ α⇒            ∎

-- The usual shorthand for hom-objects of an arbitrary category.

infix 15 _[_,_]

_[_,_] : ∀ {c} (C : Category c) (X Y : Category.Obj C) → ObjV
_[_,_] = Category.hom

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-
This second-order term syntax 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.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Combinatory.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

-- Inductive term declaration
module CL:Terms (𝔛 : Familyₛ) where

  data CL : Familyₛ where
    var  : ℐ ⇾̣ CL
    mvar : 𝔛 α Π → Sub CL Π Γ → CL α Γ

    _$_ : CL * Γ → CL * Γ → CL * Γ
    I   : CL * Γ
    K   : CL * Γ
    S   : CL * Γ

  infixl 20 _$_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  CLᵃ : MetaAlg CL
  CLᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (appₒ ⋮ a , b) → _$_ a b
      (iₒ   ⋮ _)     → I
      (kₒ   ⋮ _)     → K
      (sₒ   ⋮ _)     → S
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module CLᵃ = MetaAlg CLᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : CL ⇾̣ 𝒜
    𝕊 : Sub CL Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (_$_ a b) = 𝑎𝑙𝑔 (appₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  I        = 𝑎𝑙𝑔 (iₒ   ⋮ tt)
    𝕤𝕖𝕞  K        = 𝑎𝑙𝑔 (kₒ   ⋮ tt)
    𝕤𝕖𝕞  S        = 𝑎𝑙𝑔 (sₒ   ⋮ tt)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ CLᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ CL α Γ) → 𝕤𝕖𝕞 (CLᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (appₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (iₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (kₒ   ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (sₒ   ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ CL ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : CL ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ CLᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : CL α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub CL Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (_$_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! I = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! K = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! S = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
CL:Syn : Syntax
CL:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = CL:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open CL:Terms 𝔛 in record
    { ⊥ = CL ⋉ CLᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax CL:Syn public
open CL:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands CLᵃ public
open import SOAS.Metatheory CL:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Definition.Conversion.Consequences.Completeness where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Conversion

open import Definition.Conversion.EqRelInstance
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Escape
open import Definition.LogicalRelation.Fundamental

open import Tools.Product

-- Algorithmic equality is derivable from judgemental equality of types.
completeEq : ∀ {A B Γ} → Γ ⊢ A ≡ B → Γ ⊢ A [conv↑] B
completeEq A≡B =
  let [Γ] , [A] , [B] , [A≡B] = fundamentalEq A≡B
  in  escapeEqᵛ [Γ] [A] [A≡B]

-- Algorithmic equality is derivable from judgemental equality of terms.
completeEqTerm : ∀ {t u A Γ} → Γ ⊢ t ≡ u ∷ A → Γ ⊢ t [conv↑] u ∷ A
completeEqTerm t≡u =
  let [Γ] , modelsTermEq [A] [t] [u] [t≡u] = fundamentalTermEq t≡u
  in  escapeEqTermᵛ [Γ] [A] [t≡u]


text:
------------------------------------------------------------------------------
-- All the Peano arithmetic modules
------------------------------------------------------------------------------

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

module PA.Everything where

open import PA.Axiomatic.Mendelson.Base
open import PA.Axiomatic.Mendelson.Base.Consistency.Axioms
open import PA.Axiomatic.Mendelson.PropertiesATP
open import PA.Axiomatic.Mendelson.PropertiesI
open import PA.Axiomatic.Mendelson.Relation.Binary.EqReasoning
open import PA.Axiomatic.Mendelson.Relation.Binary.PropositionalEqualityI
open import PA.Axiomatic.Mendelson.Relation.Binary.PropositionalEqualityATP

open import PA.Axiomatic.Standard.Base
open import PA.Axiomatic.Standard.Base.Consistency.Axioms
open import PA.Axiomatic.Standard.PropertiesATP
open import PA.Axiomatic.Standard.PropertiesI

open import PA.Inductive.Base
open import PA.Inductive.Base.Core
open import PA.Inductive.Existential
open import PA.Inductive.PropertiesATP
open import PA.Inductive.PropertiesI
open import PA.Inductive.PropertiesByInduction
open import PA.Inductive.PropertiesByInductionATP
open import PA.Inductive.PropertiesByInductionI
open import PA.Inductive.Relation.Binary.EqReasoning
open import PA.Inductive.Relation.Binary.PropositionalEquality

open import PA.Inductive2Mendelson
open import PA.Inductive2Standard

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Computability.Data.Fin.Opposite where

open import Computability.Prelude
open import Data.Nat using (_≤_; _<_; s≤s; z≤n)
open import Data.Nat.Properties using (≤-step)
open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ; fromℕ<; toℕ; opposite)

opposite-fromℕ : ∀ k → opposite (fromℕ k) ≡ zero
opposite-fromℕ zero = refl
opposite-fromℕ (suc k) rewrite opposite-fromℕ k = refl

opposite-inject₁-suc : ∀{k}(i : Fin k) → opposite (inject₁ i) ≡ suc (opposite i)
opposite-inject₁-suc zero = refl
opposite-inject₁-suc (suc i) rewrite opposite-inject₁-suc i = refl

opposite-opposite : ∀{k}(i : Fin k) → opposite (opposite i) ≡ i
opposite-opposite {suc k} zero rewrite opposite-fromℕ k = refl
opposite-opposite (suc i)
  rewrite opposite-inject₁-suc (opposite i)
        | opposite-opposite i = refl

opposite-fromℕ< : ∀ a b (lt : a < b) → opposite (fromℕ< (≤-step lt)) ≡ suc (opposite (fromℕ< lt))
opposite-fromℕ< zero .(suc _) (s≤s le) = refl
opposite-fromℕ< (suc a) .(suc _) (s≤s le) rewrite opposite-fromℕ< _ _ le = refl

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
module Type.Properties.Decidable.Proofs where

open import Data
open import Data.Proofs
open import Data.Boolean using (if_then_else_)
open import Data.Boolean.Stmt
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
import      Lvl
open import Data.Boolean using (Bool ; 𝑇 ; 𝐹)
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Lang.Inspect
open import Logic
open import Logic.Classical
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural
open import Relator.Equals.Proofs.Equiv
open import Type.Properties.Decidable
open import Type.Properties.Empty
open import Type.Properties.Inhabited
open import Type.Properties.Singleton.Proofs
open import Type

private variable ℓ ℓₚ : Lvl.Level
private variable A B C P Q R T : Type{ℓ}
private variable b b₁ b₂ d : Bool
private variable f : A → B

module _ (P : Stmt{ℓ}) where
  decider-classical : ⦃ dec : Decider₀(P)(d) ⦄ → Classical(P)
  Classical.excluded-middle (decider-classical ⦃ dec = dec ⦄) = elim(\_ → (P ∨ (¬ P))) [∨]-introₗ [∨]-introᵣ dec

  classical-decidable : ⦃ classical : Classical(P) ⦄ → Decidable(0)(P)
  ∃.witness classical-decidable = Either.isLeft(excluded-middle(P))
  ∃.proof   classical-decidable with excluded-middle(P) | inspect Either.isLeft(excluded-middle(P))
  ... | Either.Left  p  | _ = true  p
  ... | Either.Right np | _ = false np

  module _ {ℓ₂} {x y : R} {Pred : (P ∨ (¬ P)) → R → Type{ℓ₂}} where
    decider-if-intro : ∀{f} ⦃ dec : Decider₀(P)(f) ⦄ → ((p : P) → Pred(Either.Left p)(x)) → ((np : (¬ P)) → Pred(Either.Right np)(y)) → Pred(excluded-middle(P) ⦃ decider-classical ⦄)(if f then x else y)
    decider-if-intro {f = 𝑇} ⦃ true  p  ⦄ fp _   = fp  p
    decider-if-intro {f = 𝐹} ⦃ false np ⦄ _  fnp = fnp np

decider-to-classical : ⦃ dec : Decider₀(P)(d) ⦄ → Classical(P)
decider-to-classical{P = P} = decider-classical(P)

classical-to-decidable : ⦃ classical : Classical(P) ⦄ → Decidable(0)(P)
classical-to-decidable{P = P} = classical-decidable(P)

classical-to-decider : ⦃ classical : Classical(P) ⦄ → Decider(0)(P)([∃]-witness classical-to-decidable)
classical-to-decider{P = P} = [∃]-proof classical-to-decidable

decider-true : ⦃ dec : Decider₀(P)(b) ⦄ → (P ↔ IsTrue(b))
decider-true ⦃ dec = true  p ⦄  = [↔]-intro (const p) (const <>)
decider-true ⦃ dec = false np ⦄ = [↔]-intro empty (empty ∘ np)

decider-false : ⦃ dec : Decider₀(P)(b) ⦄ → ((P → Empty{ℓ}) ↔ IsFalse(b))
decider-false ⦃ dec = true  p ⦄  = [↔]-intro empty (empty ∘ apply p)
decider-false ⦃ dec = false np ⦄ = [↔]-intro (const(empty ∘ np)) (const <>)

isempty-decider : ⦃ empty : IsEmpty(P) ⦄ → Decider₀(P)(𝐹)
isempty-decider ⦃ intro p ⦄ = false (empty ∘ p)

inhabited-decider : ⦃ inhab : (◊ P) ⦄ → Decider₀(P)(𝑇)
inhabited-decider ⦃ intro ⦃ p ⦄ ⦄ = true p

empty-decider : Decider₀(Empty{ℓ})(𝐹)
empty-decider = isempty-decider

unit-decider : Decider₀(Unit{ℓ})(𝑇)
unit-decider = inhabited-decider ⦃ unit-is-pos ⦄

instance
  tuple-decider : ⦃ dec-P : Decider₀(P)(b₁) ⦄ → ⦃ dec-Q : Decider₀(Q)(b₂) ⦄ → Decider₀(P ⨯ Q)(b₁ && b₂)
  tuple-decider ⦃ true  p ⦄  ⦃ true  q ⦄  = true(p , q)
  tuple-decider ⦃ true  p ⦄  ⦃ false nq ⦄ = false(nq ∘ Tuple.right)
  tuple-decider ⦃ false np ⦄ ⦃ true  q ⦄  = false(np ∘ Tuple.left)
  tuple-decider ⦃ false np ⦄ ⦃ false nq ⦄ = false(np ∘ Tuple.left)

instance
  either-decider : ⦃ dec-P : Decider₀(P)(b₁) ⦄ → ⦃ dec-Q : Decider₀(Q)(b₂) ⦄ → Decider₀(P ‖ Q)(b₁ || b₂)
  either-decider ⦃ true  p ⦄  ⦃ true  q ⦄  = true (Either.Left p)
  either-decider ⦃ true  p ⦄  ⦃ false nq ⦄ = true (Either.Left p)
  either-decider ⦃ false np ⦄ ⦃ true  q ⦄  = true (Either.Right q)
  either-decider ⦃ false np ⦄ ⦃ false nq ⦄ = false (Either.elim np nq)

instance
  function-decider : ⦃ dec-P : Decider₀(P)(b₁) ⦄ → ⦃ dec-Q : Decider₀(Q)(b₂) ⦄ → Decider₀(P → Q)((! b₁) || b₂)
  function-decider ⦃ true  p ⦄  ⦃ true  q ⦄  = true (const q)
  function-decider ⦃ true  p ⦄  ⦃ false nq ⦄ = false (apply p ∘ (nq ∘_))
  function-decider ⦃ false np ⦄ ⦃ true  q ⦄  = true (const q)
  function-decider ⦃ false np ⦄ ⦃ false nq ⦄ = true (empty ∘ np)

instance
  not-decider : ⦃ dec : Decider₀(P)(b) ⦄ → Decider₀(¬ P)(! b)
  not-decider = function-decider {b₂ = 𝐹} ⦃ dec-Q = empty-decider ⦄

instance
  IsTrue-decider : Decider₀(IsTrue(b))(b)
  IsTrue-decider {𝑇} = true <>
  IsTrue-decider {𝐹} = false id

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Data.List.Properties where

open import Data.List
open import Prelude
open import Data.Fin

map-length : (f : A → B) (xs : List A)
           → length xs ≡ length (map f xs)
map-length f [] _ = zero
map-length f (x ∷ xs) i = suc (map-length f xs i)

map-ind : (f : A → B) (xs : List A)
        → PathP (λ i → Fin (map-length f xs i) → B) (f ∘ (xs !_)) (map f xs !_)
map-ind f [] i ()
map-ind f (x ∷ xs) i f0 = f x
map-ind f (x ∷ xs) i (fs n) = map-ind f xs i n

tab-length : ∀ n (f : Fin n → A) → length (tabulate n f) ≡ n
tab-length zero f _ = zero
tab-length (suc n) f i = suc (tab-length n (f ∘ fs) i)

tab-distrib : ∀ n (f : Fin n → A) m → ∃[ i ] (f i ≡ tabulate n f ! m)
tab-distrib (suc n) f f0 = f0 , refl
tab-distrib (suc n) f (fs m) = let i , p = tab-distrib n (f ∘ fs) m in fs i , p

tab-id : ∀ n (f : Fin n → A) → PathP (λ i → Fin (tab-length n f i) → A) (_!_ (tabulate n f)) f
tab-id zero f _ ()
tab-id (suc n) f i f0 = f f0
tab-id (suc n) f i (fs m) = tab-id n (f ∘ fs) i m

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper