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

open import Cubical.Core.Everything

module Cubical.Algebra.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Relation.Binary.Base using (Rel)
open import Cubical.Relation.Binary.Definitions

open import Cubical.Algebra.Base
open import Cubical.Algebra.Definitions
open import Cubical.Data.Sum.Base using (inl; inr)
open import Cubical.Data.Sigma using (_,_)
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Relation.Binary.Reasoning.Equality

private
  variable
    ℓ : Level
    A : Type ℓ

----------------------------------------------------------------------
-- Operation properties are propositions

private
  isPropImpΠ2 : ∀ {ℓ′ ℓ′′} {B : A → Type ℓ′} {C : ∀ x → B x → Type ℓ′′} →
                  (∀ x y → isProp (C x y)) → isProp (∀ {x y} → C x y)
  isPropImpΠ2 isPropC f g i {x} {y} = isPropC x y (f {x} {y}) (g {x} {y}) i

module _ (isSetA : isSet A) where

  isPropAssociative : (_•_ : Op₂ A) → isProp (Associative _•_)
  isPropAssociative _ = isPropΠ3 λ _ _ _ → isSetA _ _

  isPropCommutative : (_•_ : Op₂ A) → isProp (Commutative _•_)
  isPropCommutative _ = isPropΠ2 λ _ _ → isSetA _ _

  isPropLeftIdentity : (_•_ : Op₂ A) (e : A) → isProp (LeftIdentity e _•_)
  isPropLeftIdentity _ _ = isPropΠ λ _ → isSetA _ _

  isPropRightIdentity : (_•_ : Op₂ A) (e : A) → isProp (RightIdentity e _•_)
  isPropRightIdentity _ _ = isPropΠ λ _ → isSetA _ _

  isPropIdentity : (_•_ : Op₂ A) (e : A) → isProp (Identity e _•_)
  isPropIdentity _•_ e = isProp× (isPropLeftIdentity _•_ e) (isPropRightIdentity _•_ e)

  isPropLeftZero : (_•_ : Op₂ A) (z : A) → isProp (LeftZero z _•_)
  isPropLeftZero _ _ = isPropΠ λ _ → isSetA _ _

  isPropRightZero : (_•_ : Op₂ A) (z : A) → isProp (RightZero z _•_)
  isPropRightZero _ _ = isPropΠ λ _ → isSetA _ _

  isPropZero : (_•_ : Op₂ A) (z : A) → isProp (Zero z _•_)
  isPropZero _•_ z = isProp× (isPropLeftZero _•_ z) (isPropRightZero _•_ z)

  isPropLeftInverse : (_•_ : Op₂ A) (_⁻¹ : Op₁ A) (e : A) → isProp (LeftInverse e _⁻¹ _•_)
  isPropLeftInverse _ _ _ = isPropΠ λ _ → isSetA _ _

  isPropRightInverse : (_•_ : Op₂ A) (_⁻¹ : Op₁ A) (e : A) → isProp (RightInverse e _⁻¹ _•_)
  isPropRightInverse _ _ _ = isPropΠ λ _ → isSetA _ _

  isPropInverse : (_•_ : Op₂ A) (_⁻¹ : Op₁ A) (e : A) → isProp (Inverse e _⁻¹ _•_)
  isPropInverse _•_ _⁻¹ e = isProp× (isPropLeftInverse _•_ _⁻¹ e) (isPropRightInverse _•_ _⁻¹ e)

  isPropLeftConical : (_•_ : Op₂ A) (e : A) → isProp (LeftConical e _•_)
  isPropLeftConical _ _ = isPropΠ3 λ _ _ _ → isSetA _ _

  isPropRightConical : (_•_ : Op₂ A) (e : A) → isProp (RightConical e _•_)
  isPropRightConical _ _ = isPropΠ3 λ _ _ _ → isSetA _ _

  isPropConical : (_•_ : Op₂ A) (e : A) → isProp (Conical e _•_)
  isPropConical _•_ e = isProp× (isPropLeftConical _•_ e) (isPropRightConical _•_ e)

  isPropDistrˡ : (_*_ _+_ : Op₂ A) → isProp (_*_ DistributesOverˡ _+_)
  isPropDistrˡ _ _ = isPropΠ3 λ _ _ _ → isSetA _ _

  isPropDistrʳ : (_*_ _+_ : Op₂ A) → isProp (_*_ DistributesOverʳ _+_)
  isPropDistrʳ _ _ = isPropΠ3 λ _ _ _ → isSetA _ _

  isPropDistr : (_*_ _+_ : Op₂ A) → isProp (_*_ DistributesOver _+_)
  isPropDistr _*_ _+_ = isProp× (isPropDistrˡ _*_ _+_) (isPropDistrʳ _*_ _+_)

  isPropIdempotentOn : (_•_ : Op₂ A) (x : A) → isProp (_•_ IdempotentOn x)
  isPropIdempotentOn _ _ = isSetA _ _

  isPropIdempotent : (_•_ : Op₂ A) → isProp (Idempotent _•_)
  isPropIdempotent _•_ = isPropΠ λ x → isPropIdempotentOn _•_ x

  isPropIdempotentFun : (f : Op₁ A) → isProp (IdempotentFun f)
  isPropIdempotentFun _ = isPropΠ λ _ → isSetA _ _

  isPropSelective : (_•_ : Op₂ A) → isProp (Selective _•_)
  isPropSelective _ = isPropΠ2 λ _ _ → squash

  isPropAbsorbs : (_⋀_ _⋁_ : Op₂ A) → isProp (_⋀_ Absorbs _⋁_)
  isPropAbsorbs _ _ = isPropΠ2 λ _ _ → isSetA _ _

  isPropAbsorptive : (_⋀_ _⋁_ : Op₂ A) → isProp (Absorptive _⋀_ _⋁_)
  isPropAbsorptive _⋀_ _⋁_ = isProp× (isPropAbsorbs _⋀_ _⋁_) (isPropAbsorbs _⋁_ _⋀_)

  isPropInvolutive : (f : Op₁ A) → isProp (Involutive f)
  isPropInvolutive _ = isPropΠ λ _ → isSetA _ _

  isPropLeftCancel : (_•_ : Op₂ A) → isProp (LeftCancellative _•_)
  isPropLeftCancel _ = isPropΠ λ _ → isPropImpΠ2 λ _ _ → isPropΠ λ _ → isSetA _ _

  isPropRightCancel : (_•_ : Op₂ A) → isProp (RightCancellative _•_)
  isPropRightCancel _ = isPropImpΠ2 λ _ _ → isPropΠ2 λ _ _ → isSetA _ _

  isPropCancellative : (_•_ : Op₂ A) → isProp (Cancellative _•_)
  isPropCancellative _•_ = isProp× (isPropLeftCancel _•_) (isPropRightCancel _•_)

  isPropInterchangeable : (_•_ _◦_ : Op₂ A) → isProp (Interchangeable _•_ _◦_)
  isPropInterchangeable _ _ = isPropΠ2 λ _ _ → isPropΠ2 λ _ _ → isSetA _ _

  sel⇒idem : {_•_ : Op₂ A} → Selective _•_ → Idempotent _•_
  sel⇒idem {_•_ = _•_} sel x = rec (isPropIdempotentOn _•_ x)
    (λ { (inl p) → p
       ; (inr p) → p
      })
    (sel x x)

module _ {ℓ′} {B : Type ℓ′} (isSetB : isSet B) where

  isPropHomomorphic₀ : (f : A → B) (x : A) (y : B) → isProp (Homomorphic₀ f x y)
  isPropHomomorphic₀ _ _ _ = isSetB _ _

  isPropHomomorphic₁ : (f : A → B) (g : Op₁ A) (h : Op₁ B) → isProp (Homomorphic₁ f g h)
  isPropHomomorphic₁ _ _ _ = isPropΠ λ _ → isSetB _ _

  isPropHomomorphic₂ : (f : A → B) (• : Op₂ A) (◦ : Op₂ B) → isProp (Homomorphic₂ f • ◦)
  isPropHomomorphic₂ _ _ _ = isPropΠ2 λ _ _ → isSetB _ _

id-unique′ : ∀ {_•_ : Op₂ A} {e i} → LeftIdentity e _•_ → RightIdentity i _•_ → e ≡ i
id-unique′ {_} {_} {_•_} {e} {i} idˡ idʳ =
  e     ≡˘⟨ idʳ e ⟩
  e • i ≡⟨ idˡ i ⟩
  i     ∎

id-unique : ∀ {_•_ : Op₂ A} {e i} → Identity e _•_ → Identity i _•_ → e ≡ i
id-unique (idˡ , _) (_ , idʳ) = id-unique′ idˡ idʳ

id-collapseʳ : ∀ {_•_ : Op₂ A} {e i} → LeftIdentity e _•_ → RightIdentity i _•_ → Identity e _•_
id-collapseʳ {_} {_} {_•_} idˡ idʳ = idˡ , subst (λ e → RightIdentity e _•_) (sym (id-unique′ idˡ idʳ)) idʳ

id-collapseˡ : ∀ {_•_ : Op₂ A} {e i} → LeftIdentity e _•_ → RightIdentity i _•_ → Identity i _•_
id-collapseˡ {_} {_} {_•_} idˡ idʳ = subst (λ e → LeftIdentity e _•_) (id-unique′ idˡ idʳ) idˡ , idʳ

------------------------------------------------------------------------
-- Magma-like Algebra

module _ {_•_ : Op₂ A} (comm : Commutative _•_) where

  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
  comm+cancelˡ⇒cancelʳ cancelˡ {x = x} {y} z eq = cancelˡ z (
    z • x ≡⟨ comm z x ⟩
    x • z ≡⟨ eq ⟩
    y • z ≡⟨ comm y z ⟩
    z • y ∎)

  comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ x (
    y • x ≡⟨ comm y x ⟩
    x • y ≡⟨ eq ⟩
    x • z ≡⟨ comm x z ⟩
    z • x ∎)

------------------------------------------------------------------------
-- Monoid-like Algebra

module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where

  comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_
  comm+idˡ⇒idʳ idˡ x =
    x • e ≡⟨ comm x e ⟩
    e • x ≡⟨ idˡ x ⟩
    x     ∎

  comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_
  comm+idʳ⇒idˡ idʳ x =
    e • x ≡⟨ comm e x ⟩
    x • e ≡⟨ idʳ x ⟩
    x     ∎

  comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_
  comm+zeˡ⇒zeʳ zeˡ x =
    x • e ≡⟨ comm x e ⟩
    e • x ≡⟨ zeˡ x ⟩
    e     ∎

  comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_
  comm+zeʳ⇒zeˡ zeʳ x =
    e • x ≡⟨ comm e x ⟩
    x • e ≡⟨ zeʳ x ⟩
    e     ∎

------------------------------------------------------------------------
-- Group-like Algebra

module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where

  comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_
  comm+invˡ⇒invʳ invˡ x =
    x • (x ⁻¹) ≡⟨ comm x (x ⁻¹) ⟩
    (x ⁻¹) • x ≡⟨ invˡ x ⟩
    e          ∎

  comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
  comm+invʳ⇒invˡ invʳ x =
    (x ⁻¹) • x ≡⟨ comm (x ⁻¹) x ⟩
    x • (x ⁻¹) ≡⟨ invʳ x ⟩
    e          ∎

module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} where

  assoc+id+invʳ⇒invʳ-unique : Associative _•_ →
                              Identity e _•_ → RightInverse e _⁻¹ _•_ →
                              ∀ x y → (x • y) ≡ e → x ≡ (y ⁻¹)
  assoc+id+invʳ⇒invʳ-unique assoc (idˡ , idʳ) invʳ x y eq =
    x                ≡⟨ sym (idʳ x) ⟩
    x • e            ≡˘⟨ cong (x •_) (invʳ y) ⟩
    x • (y • (y ⁻¹)) ≡˘⟨ assoc x y (y ⁻¹) ⟩
    (x • y) • (y ⁻¹) ≡⟨ cong (_• (y ⁻¹)) eq ⟩
    e • (y ⁻¹)       ≡⟨ idˡ (y ⁻¹) ⟩
    y ⁻¹             ∎

  assoc+id+invˡ⇒invˡ-unique : Associative _•_ →
                              Identity e _•_ → LeftInverse e _⁻¹ _•_ →
                              ∀ x y → (x • y) ≡ e → y ≡ (x ⁻¹)
  assoc+id+invˡ⇒invˡ-unique assoc (idˡ , idʳ) invˡ x y eq =
    y                ≡˘⟨ idˡ y ⟩
    e • y            ≡˘⟨ cong (_• y) (invˡ x) ⟩
    ((x ⁻¹) • x) • y ≡⟨ assoc (x ⁻¹) x y ⟩
    (x ⁻¹) • (x • y) ≡⟨ cong ((x ⁻¹) •_) eq ⟩
    (x ⁻¹) • e       ≡⟨ idʳ (x ⁻¹) ⟩
    x ⁻¹             ∎

  assoc+idˡ+invˡ⇒cancelˡ : Associative _•_ →
                          LeftIdentity e _•_ → LeftInverse e _⁻¹ _•_ →
                          LeftCancellative _•_
  assoc+idˡ+invˡ⇒cancelˡ assoc idˡ invˡ x {y} {z} eq =
    y                ≡˘⟨ idˡ y ⟩
    e • y            ≡˘⟨ cong (_• y) (invˡ x) ⟩
    ((x ⁻¹) • x) • y ≡⟨ assoc (x ⁻¹) x y ⟩
    (x ⁻¹) • (x • y) ≡⟨ cong ((x ⁻¹) •_) eq ⟩
    (x ⁻¹) • (x • z) ≡˘⟨ assoc (x ⁻¹) x z ⟩
    ((x ⁻¹) • x) • z ≡⟨ cong (_• z) (invˡ x) ⟩
    e • z            ≡⟨ idˡ z ⟩
    z                ∎

  assoc+idʳ+invʳ⇒cancelʳ : Associative _•_ →
                          RightIdentity e _•_ → RightInverse e _⁻¹ _•_ →
                          RightCancellative _•_
  assoc+idʳ+invʳ⇒cancelʳ assoc idʳ invʳ {x} {y} z eq =
    x                ≡˘⟨ idʳ x ⟩
    x • e            ≡˘⟨ cong (x •_) (invʳ z) ⟩
    x • (z • (z ⁻¹)) ≡˘⟨ assoc x z (z ⁻¹) ⟩
    (x • z) • (z ⁻¹) ≡⟨ cong (_• (z ⁻¹)) eq ⟩
    (y • z) • (z ⁻¹) ≡⟨ assoc y z (z ⁻¹) ⟩
    y • (z • (z ⁻¹)) ≡⟨ cong (y •_) (invʳ z) ⟩
    y • e            ≡⟨ idʳ y ⟩
    y                ∎

----------------------------------------------------------------------
-- Bisemigroup-like Algebra

module _ {_*_ _+_ : Op₂ A} (*-comm : Commutative _*_) where

  comm+distrˡ⇒distrʳ :  _*_ DistributesOverˡ _+_ → _*_ DistributesOverʳ _+_
  comm+distrˡ⇒distrʳ distrˡ x y z =
    (y + z) * x       ≡⟨ *-comm (y + z) x ⟩
    x * (y + z)       ≡⟨ distrˡ x y z ⟩
    (x * y) + (x * z) ≡⟨ cong₂ _+_ (*-comm x y) (*-comm x z) ⟩
    (y * x) + (z * x) ∎

  comm+distrʳ⇒distrˡ : _*_ DistributesOverʳ _+_ → _*_ DistributesOverˡ _+_
  comm+distrʳ⇒distrˡ distrʳ x y z =
    x * (y + z)       ≡⟨ *-comm x (y + z) ⟩
    (y + z) * x       ≡⟨ distrʳ x y z ⟩
    (y * x) + (z * x) ≡⟨ cong₂ _+_ (*-comm y x) (*-comm z x) ⟩
    (x * y) + (x * z) ∎

----------------------------------------------------------------------
-- Ring-like Algebra

module _ {_+_ _*_ : Op₂ A} { -_ : Op₁ A} {0# : A} where

  assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                LeftZero 0# _*_
  assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x =
    0# * x                              ≡⟨ sym (idʳ _) ⟩
    (0# * x) + 0#                       ≡˘⟨ cong ((0# * x) +_) (invʳ _) ⟩
    (0# * x) + ((0# * x) + (-(0# * x))) ≡˘⟨ +-assoc _ _ _ ⟩
    ((0# * x) + (0# * x)) + (-(0# * x)) ≡˘⟨ cong (_+ (-(0# * x))) (distribʳ _ _ _) ⟩
    ((0# + 0#) * x) + (-(0# * x))       ≡⟨ cong (λ v → (v * x) + (-(0# * x))) (idʳ 0#) ⟩
    (0# * x) + (-(0# * x))              ≡⟨ invʳ _ ⟩
    0#                                  ∎

  assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
                                RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
                                RightZero 0# _*_
  assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x =
     x * 0#                              ≡⟨ sym (idʳ _) ⟩
     (x * 0#) + 0#                       ≡˘⟨ cong ((x * 0#) +_) (invʳ _) ⟩
     (x * 0#) + ((x * 0#) + (-(x * 0#))) ≡˘⟨ +-assoc _ _ _ ⟩
     ((x * 0#) + (x * 0#)) + (-(x * 0#)) ≡˘⟨ cong (_+ (-(x * 0#))) (distribˡ _ _ _) ⟩
     (x * (0# + 0#)) + (-(x * 0#))       ≡⟨ cong (λ v → (x * v) + (-(x * 0#))) (idʳ 0#) ⟩
     (x * 0#) + (-(x * 0#))              ≡⟨ invʳ _ ⟩
     0#                                  ∎

----------------------------------------------------------------------
-- Other

module _ {c ℓ} {A : Type c} (R : Rel A ℓ) (reflexive : Reflexive R) (• : Op₂ A) where

  cong₂⇒lcong : Congruent₂ R • → LeftCongruent R •
  cong₂⇒lcong cong₂ {x} {y} {z} yRz = cong₂ reflexive yRz

  cong₂⇒rcong : Congruent₂ R • → RightCongruent R •
  cong₂⇒rcong cong₂ {x} {y} {z} yRz = cong₂ yRz reflexive

module _ {c ℓ} {A : Type c} (R : Rel A ℓ) (transitive : Transitive R) (• : Op₂ A) where

  lcong+rcong⇒cong₂ : LeftCongruent R • → RightCongruent R • → Congruent₂ R •
  lcong+rcong⇒cong₂ lcong rcong xRy uRv = transitive (lcong uRv) (rcong xRy)


text:
{-

Macros (autoDesc, AutoStructure, AutoEquivStr, autoUnivalentStr) for automatically generating structure definitions.

For example:

  autoDesc (λ (X : Type₀) → X → X × ℕ)   ↦   function+ var (var , constant ℕ)

We prefer to use the constant structure whenever possible, e.g., [autoDesc (λ (X : Type₀) → ℕ → ℕ)]
is [constant (ℕ → ℕ)] rather than [function (constant ℕ) (constant ℕ)].

Writing [auto* (λ X → ⋯)] doesn't seem to work, but [auto* (λ (X : Type ℓ) → ⋯)] does.

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Structures.Auto where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.List
open import Cubical.Data.Bool
open import Cubical.Data.Maybe

open import Cubical.Structures.Macro as Macro

import Agda.Builtin.Reflection as R

-- Magic number
private
  FUEL = 10000

-- Mark part of a structure definition to use transport-based structured equivalences
abstract
  Transp[_] : ∀ {ℓ} → Type ℓ → Type ℓ
  Transp[ A ] = A

-- Some reflection utilities
private
  _>>=_ = R.bindTC
  _<|>_ = R.catchTC

  _>>_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → R.TC A → R.TC B → R.TC B
  f >> g = f >>= λ _ → g

  infixl 4 _>>=_ _>>_ _<|>_

  varg : ∀ {ℓ} {A : Type ℓ} → A → R.Arg A
  varg = R.arg (R.arg-info R.visible R.relevant)

  tLevel = R.def (quote Level) []

  tType : R.Term → R.Term
  tType ℓ = R.def (quote Type) [ varg ℓ ]

  tTranspDesc : R.Term → R.Term
  tTranspDesc ℓ = R.def (quote TranspDesc) [ varg ℓ ]

  tDesc : R.Term → R.Term
  tDesc ℓ = R.def (quote Desc) [ varg ℓ ]

  func : (ℓ ℓ' : Level) → Type (ℓ-suc (ℓ-max ℓ ℓ'))
  func ℓ ℓ' = Type ℓ → Type ℓ'

  tStruct : R.Term → R.Term → R.Term
  tStruct ℓ ℓ' = R.def (quote func) (varg ℓ ∷ varg ℓ' ∷ [])

  newMeta = R.checkType R.unknown

-- We try to build a descriptor by unifying the provided structure with combinators we're aware of. We
-- redefine the structure combinators as the *Shape terms below so that we don't depend on the specific way
-- these are defined in other files (order of implicit arguments and so on); the syntactic analysis that goes
-- on here means that we would get mysterious errors if those changed.
private
  constantShape : ∀ {ℓ'} (ℓ : Level) (A : Type ℓ') → (Type ℓ → Type ℓ')
  constantShape _ A _ = A

  pointedShape : (ℓ : Level) → Type ℓ → Type ℓ
  pointedShape _ X = X

  productShape : ∀ {ℓ₀ ℓ₁} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → (Type ℓ → Type ℓ₁) → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  productShape _ A₀ A₁ X = A₀ X × A₁ X

  functionShape :  ∀ {ℓ₀ ℓ₁} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → (Type ℓ → Type ℓ₁) → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  functionShape _ A₀ A₁ X = A₀ X → A₁ X

  maybeShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type ℓ₀
  maybeShape _ A₀ X = Maybe (A₀ X)

  transpShape : ∀ {ℓ₀} (ℓ : Level)
    → (Type ℓ → Type ℓ₀) → Type ℓ → Type ℓ₀
  transpShape _ A₀ X = Transp[ A₀ X ]

private
  -- Build transport structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildTranspDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildTranspDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildTranspDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryProduct t <|> tryFunction t <|> tryMaybe t <|>
    R.typeError (R.strErr "Can't automatically generate a transp structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (tType ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote TranspDesc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote TranspDesc.var) [])

    tryFunction : R.Term → R.TC R.Term
    tryFunction t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote functionShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildTranspDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildTranspDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote TranspDesc.function) (varg d₀ ∷ varg d₁ ∷ []))

    tryProduct : R.Term → R.TC R.Term
    tryProduct t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote productShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildTranspDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildTranspDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote TranspDesc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildTranspDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote TranspDesc.maybe) (varg d₀ ∷ []))

  autoTranspDesc' : R.Term → R.Term → R.TC Unit
  autoTranspDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tTranspDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildTranspDesc FUEL ℓ ℓ' t >>= R.unify hole

  -- Build structure descriptor from a function [t : Type ℓ → Type ℓ']
  buildDesc : ℕ → R.Term → R.Term → R.Term → R.TC R.Term
  buildDesc zero ℓ ℓ' t = R.typeError (R.strErr "Ran out of fuel! at \n" ∷ R.termErr t ∷ [])
  buildDesc (suc fuel) ℓ ℓ' t =
    tryConstant t <|> tryPointed t <|> tryProduct t <|> tryFunction t <|>
    tryMaybe t <|> tryTransp t <|>
    R.typeError (R.strErr "Can't automatically generate a structure for\n" ∷ R.termErr t ∷ [])
    where
    tryConstant : R.Term → R.TC R.Term
    tryConstant t =
      newMeta (tType ℓ') >>= λ A →
      R.unify t (R.def (quote constantShape) (varg ℓ ∷ varg A ∷ [])) >>
      R.returnTC (R.con (quote Desc.constant) (varg A ∷ []))

    tryPointed : R.Term → R.TC R.Term
    tryPointed t =
      R.unify t (R.def (quote pointedShape) (varg ℓ ∷ [])) >>
      R.returnTC (R.con (quote Desc.var) [])

    tryProduct : R.Term → R.TC R.Term
    tryProduct t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote productShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote Desc._,_) (varg d₀ ∷ varg d₁ ∷ []))

    tryFunction : R.Term → R.TC R.Term
    tryFunction t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta tLevel >>= λ ℓ₁ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      newMeta (tStruct ℓ ℓ₁) >>= λ A₁ →
      R.unify t (R.def (quote functionShape) (varg ℓ ∷ varg A₀ ∷ varg A₁ ∷ [])) >>
      buildTranspDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      buildDesc fuel ℓ ℓ₁ A₁ >>= λ d₁ →
      R.returnTC (R.con (quote Desc.function+) (varg d₀ ∷ varg d₁ ∷ []))

    tryMaybe : R.Term → R.TC R.Term
    tryMaybe t =
      newMeta tLevel >>= λ ℓ₀ →
      newMeta (tStruct ℓ ℓ₀) >>= λ A₀ →
      R.unify t (R.def (quote maybeShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildDesc fuel ℓ ℓ₀ A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.maybe) (varg d₀ ∷ []))

    tryTransp : R.Term → R.TC R.Term
    tryTransp t =
      newMeta (tStruct ℓ ℓ') >>= λ A₀ →
      R.unify t (R.def (quote transpShape) (varg ℓ ∷ varg A₀ ∷ [])) >>
      buildTranspDesc fuel ℓ ℓ' A₀ >>= λ d₀ →
      R.returnTC (R.con (quote Desc.transpDesc) (varg d₀ ∷ []))

  autoDesc' : R.Term → R.Term → R.TC Unit
  autoDesc' t hole =
    R.inferType hole >>= λ H →
    newMeta tLevel >>= λ ℓ →
    newMeta tLevel >>= λ ℓ' →
    R.unify (tDesc ℓ) H >>
    R.checkType t (tStruct ℓ ℓ') >>
    buildDesc FUEL ℓ ℓ' t >>= R.unify hole

macro
  -- (Type ℓ → Type ℓ₁) → TranspDesc ℓ
  autoTranspDesc : R.Term → R.Term → R.TC Unit
  autoTranspDesc = autoTranspDesc'

  -- (S : Type ℓ → Type ℓ₁) → EquivAction (AutoStructure S)
  autoEquivAction : R.Term → R.Term → R.TC Unit
  autoEquivAction t hole =
    newMeta (tTranspDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote transpMacroAction) [ varg d ]) >>
    autoTranspDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → TransportStr (autoEquivAction S)
  autoTransportStr : R.Term → R.Term → R.TC Unit
  autoTransportStr t hole =
    newMeta (tTranspDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote transpMacroTransportStr) [ varg d ]) >>
    autoTranspDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → Desc ℓ
  autoDesc : R.Term → R.Term → R.TC Unit
  autoDesc = autoDesc'

  -- (S : Type ℓ → Type ℓ₁) → (Type ℓ → Type ℓ₁)
  -- Removes Transp[_] annotations
  AutoStructure : R.Term → R.Term → R.TC Unit
  AutoStructure t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroStructure) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → StrEquiv (AutoStructure S) _
  AutoEquivStr : R.Term → R.Term → R.TC Unit
  AutoEquivStr t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroEquivStr) [ varg d ]) >>
    autoDesc' t d

  -- (S : Type ℓ → Type ℓ₁) → UnivalentStr (AutoStructure S) (AutoEquivStr S)
  autoUnivalentStr : R.Term → R.Term → R.TC Unit
  autoUnivalentStr t hole =
    newMeta (tDesc R.unknown) >>= λ d →
    R.unify hole (R.def (quote MacroUnivalentStr) [ varg d ]) >>
    autoDesc' t d

ext: agda

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
{-

Please do not move this file. Changes should only be made if
necessary.

This file contains benchmarks for the paper:

Synthetic Cohomology Theory in Cubical Agda

Command to run the benchmarks and get timings:

agda -v profile.definitions:10 Benchmarks.agda

This assumes that there is no Benchmarks.agdai file. If there is one,
then it should be removed before the above command is run.

-}

{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Experiments.ZCohomology.Benchmarks where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Int
open import Cubical.HITs.Sn
open import Cubical.Algebra.Group hiding (ℤ ; Bool)
open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Torus
open import Cubical.ZCohomology.Groups.KleinBottle
open import Cubical.ZCohomology.Groups.WedgeOfSpheres
open import Cubical.ZCohomology.Groups.RP2
open import Cubical.Data.Sigma

open import Cubical.HITs.KleinBottle
open import Cubical.HITs.RPn.Base

open IsGroupHom
open Iso

-- S¹ (everything fast)
module S1-tests where

  ϕ : coHom 1 (S₊ 1) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 0))

  ϕ⁻¹ : ℤ → coHom 1 (S₊ 1)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 0))

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 30ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 1) ≡ 1    -- <10ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- <10ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 10ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 11ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ -3 +ₕ ϕ⁻¹ 4) ≡ 1    -- 29ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ -5 +ₕ ϕ⁻¹ -2) ≡ -7    -- 28ms
  test₇ = refl

-- S²
module S2-tests where

  ϕ : coHom 2 (S₊ 2) → ℤ
  ϕ = fun (fst (Hⁿ-Sⁿ≅ℤ 1))

  ϕ⁻¹ : ℤ → coHom 2 (S₊ 2)
  ϕ⁻¹ = inv (fst (Hⁿ-Sⁿ≅ℤ 1))

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 13ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 1) ≡ 1    -- 16ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 278ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 290ms
  test₄ = refl

{-
  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- nope
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 1) ≡ 2    -- nope
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ 2 +ₕ ϕ⁻¹ 4) ≡ 6    -- nope
  test₇ = refl
-}

module S1∨S1∨S2-tests₁ where -- everything fast

  ϕ : coHom 1 S²⋁S¹⋁S¹ → ℤ × ℤ
  ϕ = fun (fst H¹-S²⋁S¹⋁S¹)

  ϕ⁻¹ : ℤ × ℤ → coHom 1 S²⋁S¹⋁S¹
  ϕ⁻¹ = inv (fst H¹-S²⋁S¹⋁S¹)

  test₁ : ϕ (ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- <10ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ (3 , 1)) ≡ (3 , 1)    -- 21ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ (0 , 0) +ₕ ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 15ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ (0 , 1) +ₕ ϕ⁻¹ (1 , 0)) ≡ (1 , 1)    -- 21ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ (3 , 2) +ₕ ϕ⁻¹ (-1 , 5)) ≡ (2 , 7)    -- 47ms
  test₅ = refl

module S1∨S1∨S2-tests₂ where

  ϕ : coHom 2 S²⋁S¹⋁S¹ → ℤ
  ϕ = fun (fst H²-S²⋁S¹⋁S¹)

  ϕ⁻¹ : ℤ → coHom 2 S²⋁S¹⋁S¹
  ϕ⁻¹ = inv (fst H²-S²⋁S¹⋁S¹)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 157ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 119ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 1,820ms
  test₃ = refl

module Torus-test₁ where -- fast

  ϕ : coHom 1 (S₊ 1 × S₊ 1) → ℤ × ℤ
  ϕ = fun (fst H¹-T²≅ℤ×ℤ)

  ϕ⁻¹ : ℤ × ℤ → coHom 1 (S₊ 1 × S₊ 1)
  ϕ⁻¹ = inv (fst H¹-T²≅ℤ×ℤ)

  test₁ : ϕ (ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- <10ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ (3 , 1)) ≡ (3 , 1)    -- 18ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ (0 , 0) +ₕ ϕ⁻¹ (0 , 0)) ≡ (0 , 0)    -- 15ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ (0 , 1) +ₕ ϕ⁻¹ (1 , 0)) ≡ (1 , 1)    -- 20ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ (-3 , 2) +ₕ ϕ⁻¹ (-1 , 5)) ≡ (-4 , 7)    -- 44ms
  test₅ = refl

module Torus-test₂ where

  ϕ : coHom 2 (S₊ 1 × S₊ 1) → ℤ
  ϕ = fun (fst H²-T²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 2 (S₊ 1 × S₊ 1)
  ϕ⁻¹ = inv (fst H²-T²≅ℤ)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- 121ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 142ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- 3,674ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 3,772ms
  test₄ = refl

{-
  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- nope
  test₅ = refl
-}

module Klein-test₁ where -- fast

  ϕ : coHom 1 KleinBottle → ℤ
  ϕ = fun (fst H¹-𝕂²≅ℤ)

  ϕ⁻¹ : ℤ → coHom 1 KleinBottle
  ϕ⁻¹ = inv (fst H¹-𝕂²≅ℤ)

  test₁ : ϕ (ϕ⁻¹ 0) ≡ 0    -- <10ms
  test₁ = refl

  test₂ : ϕ (ϕ⁻¹ 3) ≡ 3    -- 12ms
  test₂ = refl

  test₃ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 0) ≡ 0    -- <10ms
  test₃ = refl

  test₄ : ϕ (ϕ⁻¹ 0 +ₕ ϕ⁻¹ 1) ≡ 1    -- 11ms
  test₄ = refl

  test₅ : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 0) ≡ 1    -- 12ms
  test₅ = refl

  test₆ : ϕ (ϕ⁻¹ -3 +ₕ ϕ⁻¹ 4) ≡ 1    -- 29ms
  test₆ = refl

  test₇ : ϕ (ϕ⁻¹ -5 +ₕ ϕ⁻¹ -2) ≡ -7    -- 29ms
  test₇ = refl

  -- The example in the paper:
  test : ϕ (ϕ⁻¹ 1 +ₕ ϕ⁻¹ 2) ≡ 3     -- 15ms
  test = refl

module Klein-test₂ where
  ϕ : coHom 2 KleinBottle → Bool
  ϕ = fun (fst H²-𝕂²≅Bool)

  ϕ⁻¹ : Bool → coHom 2 KleinBottle
  ϕ⁻¹ = inv (fst H²-𝕂²≅Bool)

{-
  test₀ : ϕ (0ₕ _) ≡ true -- fails already here...
  test₀ = refl
-}

module RP2-test₂ where
  ϕ : coHom 2 RP² → Bool
  ϕ = fun (fst H²-RP²≅Bool)

  ϕ⁻¹ : Bool → coHom 2 RP²
  ϕ⁻¹ = inv (fst H²-RP²≅Bool)

  test₀ : ϕ (0ₕ _) ≡ true    -- 1,210ms (unlike for Klein, this works)
  test₀ = refl

{-
  test₁ : ϕ (ϕ⁻¹ true) ≡ true    -- nope
  test₁ = refl
-}


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

module Categories.Functor.Instance.Core where

-- Core Functor (from Cats to Groupoids).
-- This is the right-adjoint of the forgetful functor from Groupoids to
-- Cats (see Categories.Functor.Adjoint.Instance.Core)

open import Level using (_⊔_)

open import Categories.Category using (Category)
import Categories.Category.Construction.Core as C
open import Categories.Category.Groupoid using (Groupoid)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Instance.Groupoids using (Groupoids)
open import Categories.Functor using (Functor; _∘F_; id)
open import Categories.Functor.Properties using ([_]-resp-≅; [_]-resp-≃)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)
import Categories.Morphism as Morphism
open import Categories.Morphism.IsoEquiv using (⌞_⌟)
import Categories.Morphism.Reasoning as MR

Core : ∀ {o ℓ e} → Functor (Cats o ℓ e) (Groupoids o (ℓ ⊔ e) e)
Core {o} {ℓ} {e} = record
   { F₀ = CoreGrpd
   ; F₁ = CoreFunctor
   ; identity     = CoreId
   ; homomorphism = λ {A B C F G} → CoreHom {A} {B} {C} {F} {G}
   ; F-resp-≈     = CoreRespNI
   }
   where
     CoreGrpd : Category o ℓ e → Groupoid o (ℓ ⊔ e) e
     CoreGrpd C = record
       { category   = C.Core C
       ; isGroupoid = C.Core-isGroupoid C
       }

     CoreFunctor : {A B : Category o ℓ e} →
                   Functor A B → Functor (C.Core A) (C.Core B)
     CoreFunctor {A} {B} F = record
       { F₀ = F₀
       ; F₁ = [ F ]-resp-≅
       ; identity     = ⌞ identity     ⌟
       ; homomorphism = ⌞ homomorphism ⌟
       ; F-resp-≈     = [ F ]-resp-≃
       }
       where open Functor F

     CoreId : {A : Category o ℓ e} → NaturalIsomorphism (CoreFunctor {A} id) id
     CoreId {A} = record
       { F⇒G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym A ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm A ⌟ }
       ; F⇐G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym A ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm A ⌟ }
       ; iso = λ _ → record { isoˡ = ⌞ identity² ⌟ ; isoʳ = ⌞ identity² ⌟ }
       }
       where
         open Category A
         open Morphism A

     CoreHom : {A B C : Category o ℓ e}
               {F : Functor A B} {G : Functor B C} →
               NaturalIsomorphism (CoreFunctor (G ∘F F))
                                  (CoreFunctor G ∘F CoreFunctor F)
     CoreHom {A} {B} {C} {F} {G} = record
       { F⇒G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym C ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm C ⌟ }
       ; F⇐G = record { η = λ _ → ≅.refl ; commute = λ _ → ⌞ MR.id-comm-sym C ⌟ ; sym-commute = λ _ → ⌞ MR.id-comm C ⌟ }
       ; iso = λ _ → record { isoˡ = ⌞ identity² ⌟ ; isoʳ = ⌞ identity² ⌟ }
       }
       where
         open Category C
         open Morphism C

     CoreRespNI : {A B : Category o ℓ e} {F G : Functor A B} →
                  NaturalIsomorphism F G →
                  NaturalIsomorphism (CoreFunctor F) (CoreFunctor G)
     CoreRespNI {A} {B} {F} {G} μ = record
       { F⇒G = record { η = λ _ →       FX≅GX ; commute = λ _ → ⌞ ⇒.commute _ ⌟ ; sym-commute = λ _ → ⌞ ⇒.sym-commute _ ⌟ }
       ; F⇐G = record { η = λ _ → ≅.sym FX≅GX ; commute = λ _ → ⌞ ⇐.commute _ ⌟ ; sym-commute = λ _ → ⌞ ⇐.sym-commute _ ⌟ }
       ; iso = λ X → record { isoˡ = ⌞ iso.isoˡ X ⌟ ; isoʳ = ⌞ iso.isoʳ X ⌟ }
       }
       where
         open NaturalIsomorphism μ
         open Morphism B

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning the excluded middle axiom.
------------------------------------------------------------------------

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

module Axiom.ExcludedMiddle where

open import Level
open import Relation.Nullary

------------------------------------------------------------------------
-- Definition

-- The classical statement of excluded middle says that every
-- statement/set is decidable (i.e. it either holds or it doesn't hold).

ExcludedMiddle : (ℓ : Level) → Set (suc ℓ)
ExcludedMiddle ℓ = {P : Set ℓ} → Dec P


text:
module CyclicModuleDependency where

import CyclicModuleDependency

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2013-05-02 This ain't a bug, it is a feature.
-- {-# OPTIONS -v scope.name:10 #-}
-- {-# OPTIONS -v scope:10 #-}
-- {-# OPTIONS -v scope.mod.inst:30 #-}
module _ where

module M (_ : Set₁) where

  record R : Set₁ where
    field
      X : Set

open M Set using (R)

X : R → Set
X = R.X

-- A glimpse at the scope (showing only concrete names, though)
--  modules
--   * scope Issue836a
--     private names   R --> [Issue836a._.R]
--     public  modules M --> [Issue836a.M]
--   * scope Issue836a.M
--     public  names   R --> [Issue836a.M.R]
--     public  modules R --> [Issue836a.M.R]
--   * scope Issue836a.M.R
--     public  names   X --> [Issue836a.M.R.X]
--   * scope Issue836a._
--     public  names   R --> [Issue836a._.R]
--     public  modules R --> [Issue836a._.R]
--   * scope Issue836a._.R
--     public  names   X --> [Issue836a._.R.X]

-- Nisse:
-- The open directive did not mention the /module/ R, so (I think
-- that) the code above should be rejected.

-- Andreas
-- NO, it is a feature that projections can also be accessed via
-- the record /type/.

-- The following directive is (and should be) rejected:

-- open R

-- Bug.agda:19,6-7
-- No such module R
-- when scope checking the declaration
--   open R


text:
-- There was a bug where the arguments to a let function got reversed.
module LetLHS where

f : {A B : Set} -> A -> B -> A
f {A}{B} = let const : A -> B -> A
               const x y = x
           in const

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Testing the translation of the propositional functions
------------------------------------------------------------------------------

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

module PropositionalFunction2 where

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

postulate
  D   : Set
  P   : D → Set
  a   : D
  _∨_ : Set → Set → Set

A : D → Set
A x = P x ∨ P x
{-# ATP definition A #-}

-- In this case the propositional function uses predicates and logical
-- constants.
postulate foo : A a → A a
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Examples.Max where
open import Data.Empty
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Data.List hiding (sum)
open import Data.Vec hiding (init)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
import DTGP

data Word : Set where
  nat : ℕ → Word
  sucSuc times : Word

pre : Word → ℕ → ℕ
pre (nat _) n = n
pre sucSuc n = 1 + n
pre times n = 2 + n

post : Word → ℕ → ℕ
post (nat _) n = 1 + n
post sucSuc n = 1 + n
post times n = 1 + n

open DTGP pre post Data.Nat._≟_

eval : ∀ {inp out} → Term inp out → Vec ℕ inp → Vec ℕ out
eval [] is = is
eval (nat o ∷ xs) is with eval xs is
... | os = o ∷ os
eval (sucSuc ∷ xs) is with eval xs is
... | o ∷ os = (2 + o) ∷ os
eval (times ∷ xs) is with eval xs is
... | o₂ ∷ o₁ ∷ os = (o₁ * o₂) ∷ os

score : Term 0 1 → ℕ
score xs = sum (eval xs [])

open Evolution score

match : (w : Word) (out : ℕ) → Dec (∃ λ n → out ≡ pre w n)
match (nat _) n = yes (n , refl)
match sucSuc zero = no ¬p where
  ¬p : Σ ℕ (λ n → 0 ≡ suc n) → ⊥
  ¬p (_ , ())
match sucSuc (suc n) = yes (n , refl)
match times zero = no ¬p where
  ¬p : Σ ℕ (λ n → 0 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match times (suc zero) = no ¬p where
  ¬p : Σ ℕ (λ n → 1 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match times (suc (suc n)) = yes (n , refl)

open Initialization match

choices : List Word
choices = nat 1 ∷ nat 2 ∷ nat 3 ∷ sucSuc ∷ times ∷ []

population : Population _ _ _
population = fromList (init 4 0 1 choices)

answer : Population _ _ _
answer = evolve 1337 1 population

max_stars_repo_name: larrytheliquid/dtgp

max_issues_repo_name: larrytheliquid/dtgp

max_forks_repo_name: larrytheliquid/dtgp


text:
------------------------------------------------------------------------------
-- Testing the use of numeric literals
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.NumericLiterals where

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

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

data ℕ : Set where
  z : ℕ
  s : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

toD : ℕ → D
toD z     = zero
toD (s n) = succ₁ (toD n)

ten : D
ten = toD 10

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module RW.Data.RTrie where

  open import RW.Data.RTrie.Decl public
  open import RW.Data.RTrie.Insert
    using (insertTerm) public
  open import RW.Data.RTrie.Lookup
    renaming (lookup to lookupTerm) public

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
open import Data.String using ( String )
open import Data.ByteString using ( ByteString ; Style ; lazy ; strict )
open import Data.ByteString.UTF8 using ( toString ; fromString )
open import System.IO.Primitive using ( HandleR ; HandleW ; hOpenR ; hOpenW ; hCloseR ; hCloseW ; hGetStrict ; hGetLazy ; hPutStrict ; hPutLazy )

-- A proposed binding for the Haskell IO library.

-- The semantics is strict IO, there is no visibility for semi-closed handles.

module System.IO where

open System.IO.Primitive public using ( Unit ; IO ; unit ; return ; _>>=_ ; commit ; onCommit ; stdin ; stdout ; stderr )

-- Command is a synonym for IO Unit

Command : Set
Command = IO Unit

skip : Command
skip = return unit

-- Other operations are defined in terms of _>>=_

infixl 1 _>>_
infixl 4 _<$>_ _<*>_

_>>_ : {A B : Set} → (IO A) → (IO B) → (IO B)
a >> b = a >>= (λ x → b)

_<$>_ : {A B : Set} → (A → B) → (IO A) → (IO B)
_<$>_ f a = a >>= (λ x → return (f x))

_<*>_ : {A B : Set} → (IO (A → B)) → (IO A) → (IO B)
_<*>_ f a = f >>= (λ x → x <$> a)

-- TODO: Use the new "syntax" construct to define do-like notation?

-- TODO: RW and Append mode?

data IOMode : Set where
  read write : IOMode

Handle : IOMode → Set
Handle read = HandleR
Handle write = HandleW

-- TODO: There should really be a separate type for file paths,
-- and some sanity-checking to support protection against
-- injection attacks.

hOpen : {m : IOMode} → String → IO (Handle m)
hOpen {read} = hOpenR
hOpen {write} = hOpenW

hGetBytes : {s : Style} → (Handle read) → IO (ByteString s)
hGetBytes {lazy}   = hGetLazy
hGetBytes {strict} = hGetStrict

getBytes : {s : Style} → IO (ByteString s)
getBytes = hGetBytes stdin

hPutBytes : {s : Style} → (Handle write) → (ByteString s) → Command
hPutBytes {lazy}   = hPutLazy
hPutBytes {strict} = hPutStrict

putBytes : {s : Style} → (ByteString s) → Command
putBytes = hPutBytes stdout

hClose : {m : IOMode} → (Handle m) → Command
hClose {read} = hCloseR
hClose {write} = hCloseW

-- TODO: Better handling of codecs, don't just hard-wire UTF-8!
-- TODO: Lazy vs strict strings?
-- Default arguments would help a lot here.

hGetStr : (Handle read) → (IO String)
hGetStr hdl = toString <$> hGetBytes {lazy} hdl

getStr : (IO String)
getStr = hGetStr stdin

hPutStr : (Handle write) → String → Command
hPutStr hdl s = hPutBytes {lazy} hdl (fromString s)

putStr : String → Command
putStr = hPutStr stdout

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Implicits.Resolution.Infinite.Undecidable where

open import Prelude hiding (Bool; Dec)

open import Data.Fin.Substitution
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary.Decidable as DecM using ()
open import Relation.Nullary

open import Extensions.ListFirst
open import SystemF.Everything as F using ()

open import Implicits.Resolution.Ambiguous.Resolution as A
open import Implicits.Resolution.Deterministic.Resolution as D
open import Implicits.Resolution.Infinite.Resolution as I
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Resolution.Ambiguous.Undecidable using () renaming (module Undecidable to AUndec)
open import Implicits.Resolution.Infinite.Expressiveness

private
  -- type of inhabitation problem decider
  ?:-dec : Set
  ?:-dec = ∀ {n ν} (Γ : F.Ctx ν n) (a : F.Type ν) → Dec (∃ λ t → Γ F.⊢ t ∈ a)

-- assuming that System F have an EBNF form
-- and assuming that System F type inhabitation is undecidable,
-- we prove that Infinite resolution is undecidable
module Undecidable
  (?:-undec : ¬ ?:-dec)
  (nf : ∀ {ν n} {Γ : F.Ctx ν n} {t a} → Γ F.⊢ t ∈ a → ∃ λ (t₂ : F.Term ν n) → Γ F.⊢ t₂ ⇑ a)
  where

  open Infinite⇔Ambiguous nf
  open AUndec ?:-undec using () renaming (undecidable to ⊢ᵣᵃ-undec; ⊢ᵣ-Dec to ⊢ᵣᵃ-Dec)

  -- type of decider for infinite resolution
  ⊢ᵣ-Dec : Set
  ⊢ᵣ-Dec = ∀ {ν} (Δ : ICtx ν) (a : Type ν) → Dec (Δ I.⊢ᵣ a)

  -- proof that such a decider would imply a decider for ambiguous resolution
  reduction : ⊢ᵣ-Dec → ⊢ᵣᵃ-Dec
  reduction f Δ x = DecM.map (equivalent Δ x) (f Δ x)

  -- completing the proof
  undecidable : ¬ ⊢ᵣ-Dec
  undecidable f =  ⊢ᵣᵃ-undec (reduction f)


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

open import Base

module Spaces.Interval where

private
  data #I : Set where
    #zer : #I
    #one : #I

I : Set
I = #I

zer : I
zer = #zer

one : I
one = #one

postulate  -- HIT
  seg : zer ≡ one

I-rec : ∀ {i} (P : I → Set i) (x₀ : P zer) (x₁ : P one)
  (p : transport P seg x₀ ≡ x₁)
  → ((t : I) → P t)
I-rec P x₀ x₁ p #zer = x₀
I-rec P x₀ x₁ p #one = x₁

postulate  -- HIT
  β : ∀ {i} (P : I → Set i) (x₀ : P zer) (x₁ : P one)
      (p : transport P seg x₀ ≡ x₁)
      → apd (I-rec P x₀ x₁ p) seg ≡ p

I-rec-nondep : ∀ {i} (C : Set i) (x₀ x₁ : C) (p : x₀ ≡ x₁) → (I → C)
I-rec-nondep C x₀ x₁ p #zer = x₀
I-rec-nondep C x₀ x₁ p #one = x₁

postulate  -- HIT
  β-nondep : ∀ {i} (C : Set i) (x₀ x₁ : C) (p : x₀ ≡ x₁)
             → ap (I-rec-nondep C x₀ x₁ p) seg ≡ p

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- {-# OPTIONS --show-implicit --show-irrelevant #-}
module Data.QuadTree.FunctorProofs.Valid-QuadrantFunctor where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Logic
open import Data.QuadTree.InternalAgda
open import Agda.Primitive
open import Data.QuadTree.FunctorProofs.FunctorLaws
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes
open import Data.QuadTree.Implementation.Functors
open import Data.QuadTree.Implementation.QuadrantLenses

ValidFunctor-Quadrant-IdentityLaw : (dep : Nat) -> IdentityLaw (λ y -> VQuadrant y {dep}) {{quadrantFunctor dep}}
ValidFunctor-Quadrant-IdentityLaw dep (CVQuadrant (Leaf v)) = refl
ValidFunctor-Quadrant-IdentityLaw dep@(S deps) (CVQuadrant qd@(Node (Leaf a) (Leaf b) (Leaf c) (Leaf d)) {p}) =
    ifcFalse (a == b && b == c && c == d) (notTrueToFalse $ andSndI {a = (depth qd <= dep)} p)
ValidFunctor-Quadrant-IdentityLaw dep@(S deps) (CVQuadrant (Node a@(Leaf _) b@(Leaf _) c@(Leaf _) d@(Node _ _ _ _)) {p}) =
    cong4 combine
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant a))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant b))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant c))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant d))
ValidFunctor-Quadrant-IdentityLaw dep@(S deps) (CVQuadrant (Node a@(Leaf _) b@(Leaf _) c@(Node _ _ _ _) d) {p}) =
    cong4 combine
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant a))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant b))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant c))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant d))
ValidFunctor-Quadrant-IdentityLaw dep@(S deps) (CVQuadrant (Node a@(Leaf _) b@(Node _ _ _ _) c d) {p}) =
    cong4 combine
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant a))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant b))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant c))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant d))
ValidFunctor-Quadrant-IdentityLaw dep@(S deps) (CVQuadrant (Node a@(Node _ _ _ _) b c d) {p}) =
    cong4 combine
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant a))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant b))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant c))
        (ValidFunctor-Quadrant-IdentityLaw deps (CVQuadrant d))

postulate
    eq-subst : {a b : Set} {{eqA : Eq a}} {{eqB : Eq b}} -> (f : a -> b) -> (x y : a)
        -> (x == y) ≡ (f x == f y)

combine-fmap : {t s : Set} {{eqT : Eq t}} {{eqS : Eq s}} {dep : Nat} -> (a b c d : VQuadrant t {dep})
    -> (f : t -> s)
    -> combine (fmapₑ (quadrantFunctor dep) f a) (fmapₑ (quadrantFunctor dep) f b) (fmapₑ (quadrantFunctor dep) f c) (fmapₑ (quadrantFunctor dep) f d)
        ≡ fmapₑ (quadrantFunctor (S dep)) f (combine a b c d)
combine-fmap {t} {s} {dep = dep} (CVQuadrant a@(Leaf va)) (CVQuadrant b@(Leaf vb)) (CVQuadrant c@(Leaf vc)) (CVQuadrant d@(Leaf vd)) f =
    ifc (va == vb && vb == vc && vc == vd)
    then (λ {{p}} ->
        begin
            (ifc (f va == f vb) && (f vb == f vc) && (f vc == f vd) then _ else _)
        =⟨ ifcTrue _ (useEq (cong3 (λ e1 e2 e3 -> e1 && e2 && e3) (eq-subst f va vb) (eq-subst f vb vc) (eq-subst f vc vd)) p) ⟩
            fmapₑ (quadrantFunctor (S dep)) f (CVQuadrant (Leaf va))
        =⟨ cong (fmapₑ (quadrantFunctor (S dep)) f) (sym $ ifcTrue ((va == vb) && (vb == vc) && (vc == vd)) p) ⟩
            fmapₑ (quadrantFunctor (S dep)) f (ifc (va == vb) && (vb == vc) && (vc == vd) then CVQuadrant (Leaf va) else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)))
        end)
    else (λ {{p}} ->
        begin
            (ifc (f va == f vb) && (f vb == f vc) && (f vc == f vd) then _ else _)
        =⟨ sym $ cong
            {y = (CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)) {andCombine (zeroLteAny dep) (falseToNotTrue p)})}
            p1 (ifcFalse ((va == vb) && (vb == vc) && (vc == vd)) p) ⟩
            fmapₑ (quadrantFunctor (S dep)) f (ifc (va == vb) && (vb == vc) && (vc == vd) then CVQuadrant (Leaf va) else CVQuadrant (Node (Leaf va) (Leaf vb) (Leaf vc) (Leaf vd)))
        end) where
    p1 : VQuadrant t {S dep} -> VQuadrant s {S dep}
    p1 q = (fmapₑ (quadrantFunctor (S dep)) f) q
combine-fmap (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) f = refl
combine-fmap (CVQuadrant (Leaf _)) (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) (CVQuadrant d) f = refl
combine-fmap (CVQuadrant (Leaf _)) (CVQuadrant (Node _ _ _ _)) (CVQuadrant c) (CVQuadrant d) f = refl
combine-fmap (CVQuadrant (Node _ _ _ _)) (CVQuadrant b) (CVQuadrant c) (CVQuadrant d) f = refl

ValidFunctor-Quadrant-CompositionLaw : (dep : Nat) -> CompositionLaw (λ y -> VQuadrant y {dep}) {{quadrantFunctor dep}}
ValidFunctor-Quadrant-CompositionLaw dep (CVQuadrant (Leaf x)) f g = refl
ValidFunctor-Quadrant-CompositionLaw dep@(S deps) {t1} {t2} {t3} cvq@(CVQuadrant qd@(Node a@(Leaf va) b@(Leaf vb) c@(Leaf vc) d@(Leaf vd)) {p}) f g =
    begin
        combine (mgf sa) (mgf sb) (mgf sc) (mgf sd)
    =⟨ cong4 combine
        (ValidFunctor-Quadrant-CompositionLaw deps sa f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sb f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sc f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sd f g) ⟩
        combine (mg $ mf sa) (mg $ mf sb) (mg $ mf sc) (mg $ mf sd)
    =⟨ combine-fmap (mf sa) (mf sb) (mf sc) (mf sd) g ⟩
        fmapₑ (quadrantFunctor dep) g (combine (mf sa) (mf sb) (mf sc) (mf sd))
    end where
        mf = fmapₑ (quadrantFunctor deps) f
        mg = fmapₑ (quadrantFunctor deps) g
        mgf = fmapₑ (quadrantFunctor deps) (g ∘ f)
        sa = (CVQuadrant a {aSub {dep = deps} a b c d p})
        sb = (CVQuadrant b {bSub {dep = deps} a b c d p})
        sc = (CVQuadrant c {cSub {dep = deps} a b c d p})
        sd = (CVQuadrant d {dSub {dep = deps} a b c d p})
ValidFunctor-Quadrant-CompositionLaw dep@(S deps) cvq@(CVQuadrant (Node a@(Leaf va) b@(Leaf vb) c@(Leaf vc) d@(Node _ _ _ _)) {p}) f g =
    begin
        combine (mgf sa) (mgf sb) (mgf sc) (mgf sd)
    =⟨ cong4 combine
        (ValidFunctor-Quadrant-CompositionLaw deps sa f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sb f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sc f g)
        (ValidFunctor-Quadrant-CompositionLaw deps sd f g) ⟩
        combine (mg $ mf sa) (mg $ mf sb) (mg $ mf sc) (mg $ mf sd)
    =⟨ combine-fmap (mf sa) (mf sb) (mf sc) (mf sd) g ⟩
        fmapₑ (quadrantFunctor dep) g (combine (mf sa) (mf sb) (mf sc) (mf sd))
    end where
        mf = fmapₑ (quadrantFunctor deps) f
        mg = fmapₑ (quadrantFunctor deps) g
        mgf = fmapₑ (quadrantFunctor deps) (g ∘ f)
        sa = (CVQuadrant a {aSub {dep = deps} a b c d p})
        sb = (CVQuadrant b {bSub {dep = deps} a b c d p})
        sc = (CVQuadrant c {cSub {dep = deps} a b c d p})
        sd = (CVQuadrant d {dSub {dep = deps} a b c d p})
ValidFunctor-Quadrant-CompositionLaw dep@(S deps) cvq@(CVQuadrant (Node a@(Leaf _) b@(Leaf _) c@(Node _ _ _ _) d) {p}) f g =
    trans
        (cong4 combine
            (ValidFunctor-Quadrant-CompositionLaw deps sa f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sb f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sc f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sd f g))
        (combine-fmap (mf sa) (mf sb) (mf sc) (mf sd) g)
    where
        mf = fmapₑ (quadrantFunctor deps) f
        sa = (CVQuadrant a {aSub {dep = deps} a b c d p})
        sb = (CVQuadrant b {bSub {dep = deps} a b c d p})
        sc = (CVQuadrant c {cSub {dep = deps} a b c d p})
        sd = (CVQuadrant d {dSub {dep = deps} a b c d p})
ValidFunctor-Quadrant-CompositionLaw dep@(S deps) cvq@(CVQuadrant (Node a@(Leaf _) b@(Node _ _ _ _) c d) {p}) f g =
    trans
        (cong4 combine
            (ValidFunctor-Quadrant-CompositionLaw deps sa f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sb f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sc f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sd f g))
        (combine-fmap (mf sa) (mf sb) (mf sc) (mf sd) g)
    where
        mf = fmapₑ (quadrantFunctor deps) f
        sa = (CVQuadrant a {aSub {dep = deps} a b c d p})
        sb = (CVQuadrant b {bSub {dep = deps} a b c d p})
        sc = (CVQuadrant c {cSub {dep = deps} a b c d p})
        sd = (CVQuadrant d {dSub {dep = deps} a b c d p})
ValidFunctor-Quadrant-CompositionLaw dep@(S deps) cvq@(CVQuadrant (Node a@(Node _ _ _ _) b c d) {p}) f g =
    trans
        (cong4 combine
            (ValidFunctor-Quadrant-CompositionLaw deps sa f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sb f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sc f g)
            (ValidFunctor-Quadrant-CompositionLaw deps sd f g))
        (combine-fmap (mf sa) (mf sb) (mf sc) (mf sd) g)
    where
        mf = fmapₑ (quadrantFunctor deps) f
        sa = (CVQuadrant a {aSub {dep = deps} a b c d p})
        sb = (CVQuadrant b {bSub {dep = deps} a b c d p})
        sc = (CVQuadrant c {cSub {dep = deps} a b c d p})
        sd = (CVQuadrant d {dSub {dep = deps} a b c d p})

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module ModuleInstInLet where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

module List (Elem : Set) where

  data List : Set where
    []   : List
    _::_ : Elem -> List -> List

xs : let open List Nat
     in  List
xs = List._::_ zero List.[]

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --no-termination-check #-}
-- TODO: switch the termination checker back on.

open import Coinduction using ( ∞ ; ♭ ; ♯_ )
open import Data.Bool using ( Bool ; true ; false )
open import Data.Maybe using ( Maybe ; just ; nothing )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Product using ( ∃ ; _,_ )
open import Data.ByteString using ( ByteString ; strict ; null )
open import System.IO using ( IO ; Command ; return ; _>>_ ; _>>=_ ; skip ; getBytes ; putBytes ; commit )
open import System.IO.Transducers.Lazy using ( _⇒_ ; _⤇_ ; inp ; out ; done ; ι⁻¹ )
open import System.IO.Transducers.Session using ( I ; Σ ; Bytes )
open import System.IO.Transducers.Strict using ( _⇛_ )

module System.IO.Transducers.IO where

infixl 5 _$_

postulate
  IOError : Set
  _catch_ : ∀ {A} → (IO A) → (IOError → (IO A)) → (IO A)
{-# COMPILED_TYPE IOError IOError #-}
{-# COMPILED _catch_ (\ _ -> catch) #-}

_$_ : ∀ {A V F T} → (Σ {A} V F ⤇ T) → (a : A) → (♭ F a ⤇ T)
inp P   $ a = ♭ P a
out b P $ a = out b (P $ a)

getBytes? : IO (Maybe (ByteString strict))
getBytes? = (getBytes >>= λ x → return (just x)) catch (λ e → return nothing)

runI : (I ⤇ Bytes) → Command
runI (out true (out x P)) = putBytes x >> commit >> runI P
runI (out false P)        = skip

mutual

  run? : (Bytes ⤇ Bytes) → (Maybe (ByteString strict)) → Command
  run? P (just b) = run' (P $ true $ b)
  run? P nothing = runI (P $ false)

  run' : (Bytes ⤇ Bytes) → Command
  run' (out true (out b P)) = putBytes b >> commit >> run' P
  run' (out false P)        = skip
  run' P                    = getBytes? >>= run? P

run : (Bytes ⇒ Bytes) → Command
run P = run' (ι⁻¹ P)


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

module EqBool where

open import Data.Bool

record HasEqBool {a} (A : Set a) : Set a where
  field _==_ : A → A → Bool

open HasEqBool ⦃ ... ⦄ public

open import Data.List as List using (List; _∷_; [])

==[] : ∀ {a} {A : Set a} → ⦃ _ : HasEqBool A ⦄ → List A → List A → Bool
==[] [] [] = true
==[] [] (x ∷ ys) = false
==[] (x ∷ xs) [] = false
==[] (x ∷ xs) (y ∷ ys) = x == y ∧ ==[] xs ys

instance
  eqList : ∀ {a} {A : Set a} → ⦃ _ : HasEqBool A ⦄ → HasEqBool (List A)
  _==_ ⦃ eqList ⦄ = ==[]

open import Data.Nat using (ℕ)
instance
  eqNat : HasEqBool ℕ
  _==_ ⦃ eqNat ⦄ = Agda.Builtin.Nat._==_
    where import Agda.Builtin.Nat

instance
  eqBool : HasEqBool Bool
  _==_ ⦃ eqBool ⦄ false false = true
  _==_ ⦃ eqBool ⦄ false true = false
  _==_ ⦃ eqBool ⦄ true y = y

open import Data.String using (String)
instance
  eqString : HasEqBool String
  _==_ ⦃ eqString ⦄ = Data.String._==_
    where import Data.String

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module L0 where

open import Common

-- Syntax

data Name : Set where
 d n j m : Name

data Pred1 : Set where
 M B : Pred1

data Pred2 : Set where
 K L : Pred2

data Expr : Set where
  _⦅_⦆ : Pred1 -> Name -> Expr
  _⦅_,_⦆ : Pred2 -> Name -> Name -> Expr
  ¬ : Expr -> Expr
  [_∧_] : Expr -> Expr -> Expr
  [_∨_] : Expr -> Expr -> Expr
  [_⇒_] : Expr -> Expr -> Expr
  [_⇔_] : Expr -> Expr -> Expr

example1 : Expr
example1 = [ K ⦅ d , j ⦆ ∧ M ⦅ d ⦆  ]
example2 : Expr
example2 = ¬ [ M ⦅ d ⦆ ∨ B ⦅ m ⦆ ]
example3 : Expr
example3 = [ L ⦅ n , j ⦆ ⇒ [ B ⦅ d ⦆ ∨ ¬ (K ⦅ m , m ⦆) ] ]
example4 : Expr
example4 = [ ¬ (¬ (¬ (B ⦅ n ⦆))) ⇔ ¬ (M ⦅ n ⦆) ]

-- Semantics

data Person : Set where
  Richard_Nixon : Person
  Noam_Chomsky : Person
  John_Mitchell : Person
  Muhammad_Ali : Person

instance
  eqPerson : Eq Person
  -- _==_ ⦃ eqPerson ⦄ x y =  isEq x y (refl {!x y!})
  _==_ ⦃ eqPerson ⦄ Richard_Nixon Richard_Nixon = true
  _==_ ⦃ eqPerson ⦄ Noam_Chomsky Noam_Chomsky = true
  _==_ ⦃ eqPerson ⦄ John_Mitchell John_Mitchell = true
  _==_ ⦃ eqPerson ⦄ Muhammad_Ali Muhammad_Ali = true
  _==_ ⦃ eqPerson ⦄ _ _ = false

_∈_ : {A : Set} {{_ : Eq A}} -> A -> PSet A -> Bool
x ∈ ⦃⦄ = false
x ∈ (x₁ :: xs) = (x == x₁) || (x ∈ xs)

⟦_⟧ₙ : Name -> Person
⟦ d ⟧ₙ = Richard_Nixon
⟦ n ⟧ₙ = Noam_Chomsky
⟦ j ⟧ₙ = John_Mitchell
⟦ m ⟧ₙ = Muhammad_Ali

⟦_⟧ₚ₁ : Pred1 -> PSet Person
⟦ x ⟧ₚ₁ = {!!}

⟦_⟧ₚ₂ : Pred2 -> PSet (Pair Person)
⟦ x ⟧ₚ₂ = {!!}

⟦_⟧ₑ : Expr -> Bool
{-# TERMINATING #-}
⟦ x ⦅ x₁ ⦆ ⟧ₑ = ⟦ x₁ ⟧ₙ ∈ ⟦ x ⟧ₚ₁
⟦ x ⦅ x₁ , x₂ ⦆ ⟧ₑ = < ⟦ x₁ ⟧ₙ , ⟦ x₂ ⟧ₙ > ∈ ⟦ x ⟧ₚ₂
⟦ ¬ x ⟧ₑ = neg ⟦ x ⟧ₑ
⟦ [ x ∧ x₁ ] ⟧ₑ = ⟦ x ⟧ₑ && ⟦ x₁ ⟧ₑ
⟦ [ x ∨ x₁ ] ⟧ₑ = ⟦ x ⟧ₑ || ⟦ x₁ ⟧ₑ
⟦ [ x ⇒ x₁ ] ⟧ₑ = (neg ⟦ x₁ ⟧ₑ) || ⟦ x ⟧ₑ
⟦ [ x ⇔ x₁ ] ⟧ₑ = ⟦ [ x ⇒ x₁ ] ⟧ₑ && ⟦ [ x₁ ⇒ x ] ⟧ₑ

max_stars_repo_name: daherb/Agda-Montague

max_issues_repo_name: daherb/Agda-Montague

max_forks_repo_name: daherb/Agda-Montague


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

open import Prelude
open import Relation.Binary

module Relation.Binary.Construct.Bounded {e} {E : Type e} {r₁ r₂} (totalOrder : TotalOrder E r₁ r₂) where

open TotalOrder totalOrder renaming (refl to ≤-refl)
import Data.Unit.UniversePolymorphic as Poly
import Data.Empty.UniversePolymorphic as Poly

data [∙] : Type e where
  [⊥] [⊤] : [∙]
  [_] : E → [∙]

_[≤]_ : [∙] → [∙] → Type _
[⊥]   [≤] _     = Poly.⊤
_     [≤] [⊤]   = Poly.⊤
[⊤]   [≤] _     = Poly.⊥
_     [≤] [⊥]   = Poly.⊥
[ x ] [≤] [ y ] = x ≤ y

_[<]_ : [∙] → [∙] → Type _
[⊤]   [<] _     = Poly.⊥
_     [<] [⊥]   = Poly.⊥
[⊥]   [<] _     = Poly.⊤
_     [<] [⊤]   = Poly.⊤
[ x ] [<] [ y ] = x < y

b-pord : PartialOrder [∙] _
b-pord .PartialOrder.preorder .Preorder._≤_ = _[≤]_
b-pord .PartialOrder.preorder .Preorder.refl {[⊥]} = Poly.tt
b-pord .PartialOrder.preorder .Preorder.refl {[⊤]} = Poly.tt
b-pord .PartialOrder.preorder .Preorder.refl {[ x ]} = ≤-refl
b-pord .PartialOrder.preorder .Preorder.trans {[⊥]} {y} {z} x≤y y≤z = Poly.tt
b-pord .PartialOrder.preorder .Preorder.trans {[⊤]} {[⊤]} {[⊤]} x≤y y≤z = Poly.tt
b-pord .PartialOrder.preorder .Preorder.trans {[ x ]} {[⊤]} {[⊤]} x≤y y≤z = Poly.tt
b-pord .PartialOrder.preorder .Preorder.trans {[ x ]} {[ y ]} {[⊤]} x≤y y≤z = Poly.tt
b-pord .PartialOrder.preorder .Preorder.trans {[ x ]} {[ y ]} {[ z ]} x≤y y≤z = ≤-trans x≤y y≤z
b-pord .PartialOrder.antisym {[⊥]} {[⊥]} x≤y y≤x i = [⊥]
b-pord .PartialOrder.antisym {[⊤]} {[⊤]} x≤y y≤x i = [⊤]
b-pord .PartialOrder.antisym {[ x ]} {[ y ]} x≤y y≤x i = [ antisym x≤y y≤x i ]

b-sord : StrictPartialOrder [∙] _
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder._<_ = _[<]_
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder.trans {[⊥]} {[ x ]} {[⊤]} x<y y<z = Poly.tt
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder.trans {[⊥]} {[ x ]} {[ x₁ ]} x<y y<z = Poly.tt
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder.trans {[ x ]} {[ x₁ ]} {[⊤]} x<y y<z = Poly.tt
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder.trans {[ x ]} {[ x₁ ]} {[ x₂ ]} x<y y<z = <-trans x<y y<z
b-sord .StrictPartialOrder.strictPreorder .StrictPreorder.irrefl {[ x ]} x<x = irrefl x<x
b-sord .StrictPartialOrder.conn {[⊥]} {[⊥]} x≮y y≮x = refl
b-sord .StrictPartialOrder.conn {[⊥]} {[⊤]} x≮y y≮x = ⊥-elim (x≮y Poly.tt)
b-sord .StrictPartialOrder.conn {[⊥]} {[ x ]} x≮y y≮x = ⊥-elim (x≮y Poly.tt)
b-sord .StrictPartialOrder.conn {[⊤]} {[⊥]} x≮y y≮x = ⊥-elim (y≮x Poly.tt)
b-sord .StrictPartialOrder.conn {[⊤]} {[⊤]} x≮y y≮x = refl
b-sord .StrictPartialOrder.conn {[⊤]} {[ x ]} x≮y y≮x = ⊥-elim (y≮x Poly.tt)
b-sord .StrictPartialOrder.conn {[ x ]} {[⊥]} x≮y y≮x = ⊥-elim (y≮x Poly.tt)
b-sord .StrictPartialOrder.conn {[ x ]} {[⊤]} x≮y y≮x = ⊥-elim (x≮y Poly.tt)
b-sord .StrictPartialOrder.conn {[ x ]} {[ x₁ ]} x≮y y≮x = cong [_] (conn x≮y y≮x)

b-ord : TotalOrder [∙] _ _
b-ord .TotalOrder.strictPartialOrder = b-sord
b-ord .TotalOrder.partialOrder = b-pord
b-ord .TotalOrder._<?_ [⊥] [⊥] = no λ ()
b-ord .TotalOrder._<?_ [⊥] [⊤] = yes _
b-ord .TotalOrder._<?_ [⊥] [ y ] = yes _
b-ord .TotalOrder._<?_ [⊤] [⊥] = no λ ()
b-ord .TotalOrder._<?_ [⊤] [⊤] = no λ ()
b-ord .TotalOrder._<?_ [⊤] [ y ] = no λ ()
b-ord .TotalOrder._<?_ [ x ] [⊥] = no λ ()
b-ord .TotalOrder._<?_ [ x ] [⊤] = yes _
b-ord .TotalOrder._<?_ [ x ] [ y ] = x <? y
b-ord .TotalOrder.≰⇒> {[⊥]} {y} x≰y = ⊥-elim (x≰y Poly.tt)
b-ord .TotalOrder.≰⇒> {[⊤]} {[⊥]} x≰y = Poly.tt
b-ord .TotalOrder.≰⇒> {[⊤]} {[⊤]} x≰y = ⊥-elim (x≰y Poly.tt)
b-ord .TotalOrder.≰⇒> {[⊤]} {[ x ]} x≰y = Poly.tt
b-ord .TotalOrder.≰⇒> {[ x ]} {[⊥]} x≰y = Poly.tt
b-ord .TotalOrder.≰⇒> {[ x ]} {[⊤]} x≰y = ⊥-elim (x≰y Poly.tt)
b-ord .TotalOrder.≰⇒> {[ x ]} {[ x₁ ]} x≰y = ≰⇒> x≰y
b-ord .TotalOrder.≮⇒≥ {x} {[⊥]} x≮y = Poly.tt
b-ord .TotalOrder.≮⇒≥ {[⊥]} {[⊤]} x≮y = ⊥-elim (x≮y Poly.tt)
b-ord .TotalOrder.≮⇒≥ {[⊤]} {[⊤]} x≮y = Poly.tt
b-ord .TotalOrder.≮⇒≥ {[ x ]} {[⊤]} x≮y = ⊥-elim (x≮y Poly.tt)
b-ord .TotalOrder.≮⇒≥ {[⊥]} {[ x₁ ]} x≮y = ⊥-elim (x≮y Poly.tt)
b-ord .TotalOrder.≮⇒≥ {[⊤]} {[ x₁ ]} x≮y = Poly.tt
b-ord .TotalOrder.≮⇒≥ {[ x ]} {[ y ]} x≮y = ≮⇒≥ x≮y

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------

-- The definitions of lexicographic ordering used here are suitable if
-- the argument order is a strict partial order.

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

module Data.List.Relation.Binary.Lex.Strict where

open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤; tt)
open import Function using (_∘_; id)
open import Data.Product using (_,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.List.Base using (List; []; _∷_)
open import Level using (_⊔_)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary
open import Relation.Binary.Consequences
open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; []; _∷_; head; tail)

open import Data.List.Relation.Binary.Lex.Core as Core public
  using (base; halt; this; next; ¬≤-this; ¬≤-next)

----------------------------------------------------------------------
-- Strict lexicographic ordering.

module _ {a ℓ₁ ℓ₂} {A : Set a} where

  Lex-< : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
          Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-< = Core.Lex ⊥

  -- Properties

  module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _<_ = Lex-< _≈_ _≺_

    ¬[]<[] : ¬ [] < []
    ¬[]<[] (base ())

    <-irreflexive : Irreflexive _≈_ _≺_ → Irreflexive _≋_ _<_
    <-irreflexive irr []            (base ())
    <-irreflexive irr (x≈y ∷ xs≋ys) (this x<y)     = irr x≈y x<y
    <-irreflexive irr (x≈y ∷ xs≋ys) (next _ xs⊴ys) =
      <-irreflexive irr xs≋ys xs⊴ys

    <-asymmetric : Symmetric _≈_ → _≺_ Respects₂ _≈_ → Asymmetric _≺_ →
                   Asymmetric _<_
    <-asymmetric sym resp as = asym
      where
      irrefl : Irreflexive _≈_ _≺_
      irrefl = asym⟶irr resp sym as

      asym : Asymmetric _<_
      asym (halt)           ()
      asym (base bot)       _                = bot
      asym (this x<y)       (this y<x)       = as x<y y<x
      asym (this x<y)       (next y≈x ys⊴xs) = irrefl (sym y≈x) x<y
      asym (next x≈y xs⊴ys) (this y<x)       = irrefl (sym x≈y) y<x
      asym (next x≈y xs⊴ys) (next y≈x ys⊴xs) = asym xs⊴ys ys⊴xs

    <-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
                      Asymmetric _≺_ → Antisymmetric _≋_ _<_
    <-antisymmetric = Core.antisymmetric

    <-transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   Transitive _≺_ → Transitive _<_
    <-transitive = Core.transitive

    <-compare : Symmetric _≈_ → Trichotomous _≈_ _≺_ →
                Trichotomous _≋_ _<_
    <-compare sym tri []       []       = tri≈ ¬[]<[] []    ¬[]<[]
    <-compare sym tri []       (y ∷ ys) = tri< halt   (λ()) (λ())
    <-compare sym tri (x ∷ xs) []       = tri> (λ())  (λ()) halt
    <-compare sym tri (x ∷ xs) (y ∷ ys) with tri x y
    ... | tri< x<y x≉y y≮x =
          tri< (this x<y) (x≉y ∘ head) (¬≤-this (x≉y ∘ sym) y≮x)
    ... | tri> x≮y x≉y y<x =
          tri> (¬≤-this x≉y x≮y) (x≉y ∘ head) (this y<x)
    ... | tri≈ x≮y x≈y y≮x with <-compare sym tri xs ys
    ...   | tri< xs<ys xs≉ys ys≮xs =
            tri< (next x≈y xs<ys) (xs≉ys ∘ tail) (¬≤-next y≮x ys≮xs)
    ...   | tri≈ xs≮ys xs≈ys ys≮xs =
            tri≈ (¬≤-next x≮y xs≮ys) (x≈y ∷ xs≈ys) (¬≤-next y≮x ys≮xs)
    ...   | tri> xs≮ys xs≉ys ys<xs =
            tri> (¬≤-next x≮y xs≮ys) (xs≉ys ∘ tail) (next (sym x≈y) ys<xs)

    <-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _<_
    <-decidable = Core.decidable (no id)

    <-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                  _<_ Respects₂ _≋_
    <-respects₂ = Core.respects₂

    <-isStrictPartialOrder : IsStrictPartialOrder _≈_ _≺_ →
                             IsStrictPartialOrder _≋_ _<_
    <-isStrictPartialOrder spo = record
      { isEquivalence = Pointwise.isEquivalence isEquivalence
      ; irrefl        = <-irreflexive irrefl
      ; trans         = Core.transitive isEquivalence <-resp-≈ trans
      ; <-resp-≈      = Core.respects₂ isEquivalence <-resp-≈
      } where open IsStrictPartialOrder spo

    <-isStrictTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                           IsStrictTotalOrder _≋_ _<_
    <-isStrictTotalOrder sto = record
      { isEquivalence = Pointwise.isEquivalence isEquivalence
      ; trans         = <-transitive isEquivalence <-resp-≈ trans
      ; compare       = <-compare Eq.sym compare
      } where open IsStrictTotalOrder sto

<-strictPartialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ →
                       StrictPartialOrder _ _ _
<-strictPartialOrder spo = record
  { isStrictPartialOrder = <-isStrictPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

<-strictTotalOrder : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
                       StrictTotalOrder _ _ _
<-strictTotalOrder sto = record
  { isStrictTotalOrder = <-isStrictTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto

----------------------------------------------------------------------
-- Non-strict lexicographic ordering.

module _ {a ℓ₁ ℓ₂} {A : Set a} where

  Lex-≤ : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
          Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
  Lex-≤ = Core.Lex ⊤

  -- Properties

  ≤-reflexive : (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
                Pointwise _≈_ ⇒ Lex-≤ _≈_ _≺_
  ≤-reflexive _≈_ _≺_ []            = base tt
  ≤-reflexive _≈_ _≺_ (x≈y ∷ xs≈ys) =
    next x≈y (≤-reflexive _≈_ _≺_ xs≈ys)

  module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where

    private
      _≋_ = Pointwise _≈_
      _≤_ = Lex-≤ _≈_ _≺_

    ≤-antisymmetric : Symmetric _≈_ → Irreflexive _≈_ _≺_ →
                      Asymmetric _≺_ → Antisymmetric _≋_ _≤_
    ≤-antisymmetric = Core.antisymmetric

    ≤-transitive : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   Transitive _≺_ → Transitive _≤_
    ≤-transitive = Core.transitive

    -- Note that trichotomy is an unnecessarily strong precondition for
    -- the following lemma.

    ≤-total : Symmetric _≈_ → Trichotomous _≈_ _≺_ → Total _≤_
    ≤-total _   _   []       []       = inj₁ (base tt)
    ≤-total _   _   []       (x ∷ xs) = inj₁ halt
    ≤-total _   _   (x ∷ xs) []       = inj₂ halt
    ≤-total sym tri (x ∷ xs) (y ∷ ys) with tri x y
    ... | tri< x<y _ _ = inj₁ (this x<y)
    ... | tri> _ _ y<x = inj₂ (this y<x)
    ... | tri≈ _ x≈y _ with ≤-total sym tri xs ys
    ...   | inj₁ xs≲ys = inj₁ (next      x≈y  xs≲ys)
    ...   | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)

    ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
    ≤-decidable = Core.decidable (yes tt)

    ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                  _≤_ Respects₂ _≋_
    ≤-respects₂ = Core.respects₂

    ≤-isPreorder : IsEquivalence _≈_ → Transitive _≺_ →
                   _≺_ Respects₂ _≈_ → IsPreorder _≋_ _≤_
    ≤-isPreorder eq tr resp = record
      { isEquivalence = Pointwise.isEquivalence eq
      ; reflexive     = ≤-reflexive _≈_ _≺_
      ; trans         = Core.transitive eq resp tr
      }

    ≤-isPartialOrder : IsStrictPartialOrder _≈_ _≺_ →
                       IsPartialOrder _≋_ _≤_
    ≤-isPartialOrder  spo = record
      { isPreorder = ≤-isPreorder isEquivalence trans <-resp-≈
      ; antisym    = Core.antisymmetric Eq.sym irrefl asym
      }
      where open IsStrictPartialOrder spo

    ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ → IsTotalOrder _≋_ _≤_
    ≤-isTotalOrder sto = record
      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
      ; total          = ≤-total Eq.sym compare
      }
      where open IsStrictTotalOrder sto

    ≤-isDecTotalOrder : IsStrictTotalOrder _≈_ _≺_ →
                        IsDecTotalOrder _≋_ _≤_
    ≤-isDecTotalOrder sto = record
      { isTotalOrder = ≤-isTotalOrder sto
      ; _≟_          = Pointwise.decidable _≟_
      ; _≤?_         = ≤-decidable _≟_ _<?_
      }
      where open IsStrictTotalOrder sto

≤-preorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
≤-preorder pre = record
  { isPreorder = ≤-isPreorder isEquivalence trans ∼-resp-≈
  } where open Preorder pre

≤-partialOrder : ∀ {a ℓ₁ ℓ₂} → StrictPartialOrder a ℓ₁ ℓ₂ → Poset _ _ _
≤-partialOrder spo = record
  { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
  } where open StrictPartialOrder spo

≤-decTotalOrder : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
                  DecTotalOrder _ _ _
≤-decTotalOrder sto = record
  { isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
  } where open StrictTotalOrder sto


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

module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base where
{-
  The free commutative algebra over a commutative ring,
  or in other words the ring of polynomials with coefficients in a given ring.
  Note that this is a constructive definition, which entails that polynomials
  cannot be represented by lists of coefficients, where the last one is non-zero.
  For rings with decidable equality, that is still possible.

  I learned about this (and other) definition(s) from David Jaz Myers.
  You can watch him talk about these things here:
  https://www.youtube.com/watch?v=VNp-f_9MnVk

  This file contains
  * the definition of the free commutative algebra on a type I over a commutative ring R as a HIT
    (let us call that R[I])
  * a prove that the construction is an commutative R-algebra
  * definitions of the induced maps appearing in the universal property of R[I],
    that is:  * for any map I → A, where A is a commutative R-algebra,
                the induced algebra homomorphism R[I] → A
                ('inducedHom')
              * for any hom R[I] → A, the 'restricttion to variables' I → A
                ('evaluateAt')
  * a proof that the two constructions are inverse to each other
    ('homRetrievable' and 'mapRetrievable')
  * a proof, that the corresponding pointwise equivalence of functors is natural
    ('naturalR', 'naturalL')
-}
open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommAlgebra.Base

private
  variable
    ℓ ℓ' : Level

module Construction (R : CommRing ℓ) where
  open CommRingStr (snd R) using (1r; 0r) renaming (_+_ to _+r_; _·_ to _·r_)

  data R[_] (I : Type ℓ') : Type (ℓ-max ℓ ℓ') where
    var : I → R[ I ]
    const : fst R → R[ I ]
    _+_ : R[ I ] → R[ I ] → R[ I ]
    -_ : R[ I ] → R[ I ]
    _·_ : R[ I ] → R[ I ] → R[ I ]            -- \cdot

    +-assoc : (x y z : R[ I ]) → x + (y + z) ≡ (x + y) + z
    +-rid : (x : R[ I ]) → x + (const 0r) ≡ x
    +-rinv : (x : R[ I ]) → x + (- x) ≡ (const 0r)
    +-comm : (x y : R[ I ]) → x + y ≡ y + x

    ·-assoc : (x y z : R[ I ]) → x · (y · z) ≡ (x · y) · z
    ·-lid : (x : R[ I ]) → (const 1r) · x ≡ x
    ·-comm : (x y : R[ I ]) → x · y ≡ y · x

    ldist : (x y z : R[ I ]) → (x + y) · z ≡ (x · z) + (y · z)

    +HomConst : (s t : fst R) → const (s +r t) ≡ const s + const t
    ·HomConst : (s t : fst R) → const (s ·r t) ≡ (const s) · (const t)

    0-trunc : (x y : R[ I ]) (p q : x ≡ y) → p ≡ q

  _⋆_ : {I : Type ℓ'} → fst R → R[ I ] → R[ I ]
  r ⋆ x = const r · x

  ⋆-assoc : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s ·r t) ⋆ x ≡ s ⋆ (t ⋆ x)
  ⋆-assoc s t x = const (s ·r t) · x       ≡⟨ cong (λ u → u · x) (·HomConst _ _) ⟩
                  (const s · const t) · x  ≡⟨ sym (·-assoc _ _ _) ⟩
                  const s · (const t · x)  ≡⟨ refl ⟩
                  s ⋆ (t ⋆ x) ∎

  ⋆-ldist-+ : {I : Type ℓ'} → (s t : fst R) (x : R[ I ]) → (s +r t) ⋆ x ≡ (s ⋆ x) + (t ⋆ x)
  ⋆-ldist-+ s t x = (s +r t) ⋆ x             ≡⟨ cong (λ u → u · x) (+HomConst _ _) ⟩
                    (const s + const t) · x  ≡⟨ ldist _ _ _ ⟩
                    (s ⋆ x) + (t ⋆ x) ∎

  ⋆-rdist-+ : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → s ⋆ (x + y) ≡ (s ⋆ x) + (s ⋆ y)
  ⋆-rdist-+ s x y = const s · (x + y)             ≡⟨ ·-comm _ _ ⟩
                    (x + y) · const s             ≡⟨ ldist _ _ _ ⟩
                    (x · const s) + (y · const s) ≡⟨ cong (λ u → u + (y · const s)) (·-comm _ _) ⟩
                    (s ⋆ x) + (y · const s)       ≡⟨ cong (λ u → (s ⋆ x) + u) (·-comm _ _)  ⟩
                    (s ⋆ x) + (s ⋆ y) ∎

  ⋆-assoc-· : {I : Type ℓ'} → (s : fst R) (x y : R[ I ]) → (s ⋆ x) · y ≡ s ⋆ (x · y)
  ⋆-assoc-· s x y = (s ⋆ x) · y ≡⟨ sym (·-assoc _ _ _) ⟩
                    s ⋆ (x · y) ∎

  0a : {I : Type ℓ'} → R[ I ]
  0a = (const 0r)

  1a : {I : Type ℓ'} → R[ I ]
  1a = (const 1r)

  isCommAlgebra : {I : Type ℓ'} → IsCommAlgebra R {A = R[ I ]} 0a 1a _+_ _·_ -_ _⋆_
  isCommAlgebra = makeIsCommAlgebra 0-trunc
                                    +-assoc +-rid +-rinv +-comm
                                    ·-assoc ·-lid ldist ·-comm
                                    ⋆-assoc ⋆-rdist-+ ⋆-ldist-+ ·-lid ⋆-assoc-·

_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
(R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
  where
  open Construction R

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Issue256 where

open import Common.Level

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x

level : ∀ {ℓ} → Set ℓ → Level
level {ℓ} _ = ℓ

-- termination check should fail for the following definition
ℓ : Level
ℓ = const lzero (Set ℓ)

-- A : Set (lsuc {!ℓ!})
-- A = Set (level A)


text:
module FunctionName where

open import OscarPrelude

record FunctionName : Set
 where
  constructor ⟨_⟩
  field
    name : Nat

open FunctionName public

instance EqFunctionName : Eq FunctionName
Eq._==_ EqFunctionName _ = decEq₁ (cong name) ∘ (_≟_ on name $ _)


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

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.cubical.Square
open import lib.types.Lift
open import lib.types.Nat
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.types.Unit

{- Sequential colimits -}

module lib.types.NatColim where

module _ {i} {D : ℕ → Type i} where

  private
    data #ℕColim-aux (d : (n : ℕ) → D n → D (S n)) : Type i where
      #ncin : (n : ℕ) → D n → #ℕColim-aux d

    data #ℕColim (d : (n : ℕ) → D n → D (S n)) : Type i where
      #ncolim : #ℕColim-aux d → (Unit → Unit) → #ℕColim d

  ℕColim : (d : (n : ℕ) → D n → D (S n)) → Type i
  ℕColim d = #ℕColim d

  ncin : {d : (n : ℕ) → D n → D (S n)} → (n : ℕ) → D n → ℕColim d
  ncin n x = #ncolim (#ncin n x) _

  postulate  -- HIT
    ncglue : {d : (n : ℕ) → D n → D (S n)}
      (n : ℕ) → (x : D n) → ncin {d = d} n x == ncin (S n) (d n x)

  module ℕColimElim (d : (n : ℕ) → D n → D (S n))
    {j} {P : ℕColim d → Type j}
    (ncin* : (n : ℕ) (x : D n) → P (ncin n x))
    (ncglue* : (n : ℕ) (x : D n)
      → ncin* n x == ncin* (S n) (d n x) [ P ↓ ncglue n x ])
    where

    f : Π (ℕColim d) P
    f = f-aux phantom where

      f-aux : Phantom ncglue* → Π (ℕColim d) P
      f-aux phantom (#ncolim (#ncin n x) _) = ncin* n x

    postulate  -- HIT
      ncglue-β : (n : ℕ) (x : D n) → apd f (ncglue n x) == ncglue* n x

  open ℕColimElim public using () renaming (f to ℕColim-elim)

  module ℕColimRec (d : (n : ℕ) → D n → D (S n))
    {j} {A : Type j}
    (ncin* : (n : ℕ) → D n → A)
    (ncglue* : (n : ℕ) → (x : D n) → ncin* n x == ncin* (S n) (d n x))
    where

    private
      module M = ℕColimElim d ncin* (λ n x → ↓-cst-in (ncglue* n x))

    f : ℕColim d → A
    f = M.f

    ncglue-β : (n : ℕ) (x : D n) → ap f (ncglue n x) == ncglue* n x
    ncglue-β n x = apd=cst-in {f = f} (M.ncglue-β n x)

⊙ℕColim : ∀ {i} {D : ℕ → Ptd i} (d : (n : ℕ) → fst (D n ⊙→ D (S n))) → Ptd i
⊙ℕColim {D = D} d = ⊙[ ℕColim (fst ∘ d) , ncin 0 (snd (D 0)) ]

{- Can define a function [nc-raise d : ℕColim d → ℕColim d]
   so that [inn (S n) ∘ d = nc-raise d ∘ inn n] -}

module ℕCRaise {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n)) =
  ℕColimRec d {A = ℕColim d}
    (λ n x → ncin (S n) (d n x))
    (λ n x → ncglue (S n) (d n x))

nc-raise : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n))
  → ℕColim d → ℕColim d
nc-raise d = ℕCRaise.f d

nc-raise-= : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n)) (c : ℕColim d)
  → c == nc-raise d c
nc-raise-= d = ℕColimElim.f d
  (λ n x → ncglue n x)
  (λ n x → ↓-='-from-square $
    ap-idf (ncglue n x) ∙v⊡ connection2 ⊡v∙ (! (ℕCRaise.ncglue-β d n x)))

{- Lift an element of D₀ to any level -}

nc-lift : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n))
  (n : ℕ) → D O → D n
nc-lift d O x = x
nc-lift d (S n) x = d n (nc-lift d n x)

nc-lift-= : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n))
  (n : ℕ) (x : D O)
  → ncin {d = d} O x == ncin n (nc-lift d n x)
nc-lift-= d O x = idp
nc-lift-= d (S n) x = nc-lift-= d n x ∙ ncglue n (nc-lift d n x)

{- Lift an element of D₀ to the 'same level' as some element of ℕColim d -}

module ℕCMatch {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n)) (x : D O) =
  ℕColimRec d {A = ℕColim d}
    (λ n _ → ncin n (nc-lift d n x))
    (λ n _ → ncglue n (nc-lift d n x))

nc-match = ℕCMatch.f

nc-match-=-base : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n))
  (x : D O) (c : ℕColim d)
  → ncin O x == nc-match d x c
nc-match-=-base d x = ℕColimElim.f d
  (λ n _ → nc-lift-= d n x)
  (λ n y → ↓-cst=app-from-square $
    disc-to-square idp ⊡v∙ ! (ℕCMatch.ncglue-β d x n y))

{- If all Dₙ are m-connected, then the colim is m-connected -}

ncolim-conn : ∀ {i} {D : ℕ → Type i} (d : (n : ℕ) → D n → D (S n)) (m : ℕ₋₂)
  → ((n : ℕ) → is-connected m (D n))
  → is-connected m (ℕColim d)
ncolim-conn {D = D} d ⟨-2⟩ cD = -2-conn (ℕColim d)
ncolim-conn {D = D} d (S m) cD =
  Trunc-rec (prop-has-level-S is-contr-is-prop)
    (λ x → ([ ncin O x ] ,
            (Trunc-elim (λ _ → =-preserves-level _ Trunc-level) $
              λ c → ap [_] (nc-match-=-base d x c) ∙ nc-match-=-point x c)))
    (fst (cD O))
  where
  nc-match-=-point : (x : D O) (c : ℕColim d)
    → [_] {n = S m} (nc-match d x c) == [ c ]
  nc-match-=-point x = ℕColimElim.f d
    (λ n y → ap (Trunc-fmap (ncin n))
                (contr-has-all-paths (cD n) [ nc-lift d n x ] [ y ]))
      (λ n y → ↓-='-from-square $
        (ap-∘ [_] (nc-match d x) (ncglue n y)
         ∙ ap (ap [_]) (ℕCMatch.ncglue-β d x n y))
        ∙v⊡
        ! (ap-idf _)
        ∙h⊡
        (square-symmetry $
          natural-square
            (Trunc-elim (λ _ → =-preserves-level _ Trunc-level)
               (λ c → ap [_] (nc-raise-= d c)))
            (ap (Trunc-fmap (ncin n))
                (contr-has-all-paths (cD n) [ nc-lift d n x ] [ y ])))
        ⊡h∙
        (∘-ap (Trunc-fmap (nc-raise d)) (Trunc-fmap (ncin n))
              (contr-has-all-paths (cD n) [ nc-lift d n x ] [ y ])
         ∙ vert-degen-path
             (natural-square
               (λ t → Trunc-fmap-∘ (nc-raise d) (ncin n) t
                      ∙ ! (Trunc-fmap-∘ (ncin (S n)) (d n) t))
               (contr-has-all-paths (cD n) [ nc-lift d n x ] [ y ]))
         ∙ ap-∘ (Trunc-fmap (ncin (S n))) (Trunc-fmap (d n))
                (contr-has-all-paths (cD n) [ nc-lift d n x ] [ y ])
         ∙ ap (ap (Trunc-fmap (ncin (S n))))
              (contr-has-all-paths (=-preserves-level _ (cD (S n))) _ _)))

{- Type of finite tuples -}

FinTuplesType : ∀ {i} → (ℕ → Ptd i) → ℕ → Ptd i
FinTuplesType F O = ⊙Lift ⊙Unit
FinTuplesType F (S n) = F O ⊙× FinTuplesType (F ∘ S) n

fin-tuples-map : ∀ {i} (F : ℕ → Ptd i) (n : ℕ)
  → fst (FinTuplesType F n ⊙→ FinTuplesType F (S n))
fin-tuples-map F O = (_ , idp)
fin-tuples-map F (S n) =
  ((λ {(x , r) → (x , fst (fin-tuples-map (F ∘ S) n) r)}) ,
   pair×= idp (snd (fin-tuples-map (F ∘ S) n)))

⊙FinTuples : ∀ {i} → (ℕ → Ptd i) → Ptd i
⊙FinTuples {i} F = ⊙ℕColim (fin-tuples-map F)

FinTuples : ∀ {i} → (ℕ → Ptd i) → Type i
FinTuples = fst ∘ ⊙FinTuples

module FinTuplesCons {i} (F : ℕ → Ptd i) where

  module Into (x : fst (F O)) =
    ℕColimRec (fst ∘ fin-tuples-map (F ∘ S)) {A = fst (⊙FinTuples F)}
      (λ n r → ncin (S n) (x , r))
      (λ n r → ncglue (S n) (x , r))

  into = uncurry Into.f

  out-ncin : (n : ℕ)
    → fst (FinTuplesType F n) → fst (F O ⊙× ⊙FinTuples (F ∘ S))
  out-ncin O x = (snd (F O) , ncin O _)
  out-ncin (S n) (x , r) = (x , ncin n r)

  out-ncglue : (n : ℕ) (r : fst (FinTuplesType F n))
    → out-ncin n r == out-ncin (S n) (fst (fin-tuples-map F n) r)
  out-ncglue O x = idp
  out-ncglue (S n) (x , r) = pair= idp (ncglue n r)

  module Out = ℕColimRec _ out-ncin out-ncglue
  out = Out.f

  into-out-ncin : (n : ℕ) (r : fst (FinTuplesType F n))
    → into (out-ncin n r) == ncin n r
  into-out-ncin O x = ! (ncglue O x)
  into-out-ncin (S n) (x , r) = idp

  into-out-ncglue : (n : ℕ) (r : fst (FinTuplesType F n))
    → into-out-ncin n r == into-out-ncin (S n) (fst (fin-tuples-map F n) r)
      [ (λ s → into (out s) == s) ↓ ncglue n r ]
  into-out-ncglue O x =
    ↓-∘=idf-from-square into out $
      ap (ap into) (Out.ncglue-β O x)
      ∙v⊡ bl-square (ncglue O x)
  into-out-ncglue (S n) (x , r) =
    ↓-∘=idf-from-square into out $
      (ap (ap into) (Out.ncglue-β (S n) (x , r))
       ∙ ∘-ap into (_,_ x) (ncglue n r)
       ∙ Into.ncglue-β x n r)
      ∙v⊡ vid-square

  into-out : (r : fst (⊙FinTuples F)) → into (out r) == r
  into-out = ℕColimElim.f _
    into-out-ncin
    into-out-ncglue

  out-into : (t : fst (F O ⊙× ⊙FinTuples (F ∘ S))) → out (into t) == t
  out-into = uncurry $ λ x → ℕColimElim.f _
    (λ n r → idp)
    (λ n r → ↓-='-from-square $
      (ap-∘ out (Into.f x) (ncglue n r)
       ∙ ap (ap out) (Into.ncglue-β x n r)
       ∙ Out.ncglue-β (S n) (x , r))
      ∙v⊡ vid-square)

fin-tuples-cons : ∀ {i} (F : ℕ → Ptd i)
  → fst (F O) × FinTuples (F ∘ S) ≃ FinTuples F
fin-tuples-cons {i} F = equiv into out into-out out-into
  where open FinTuplesCons F

⊙fin-tuples-cons : ∀ {i} (F : ℕ → Ptd i)
  → (F O ⊙× ⊙FinTuples (F ∘ S)) ⊙≃ ⊙FinTuples F
⊙fin-tuples-cons F = ⊙≃-in (fin-tuples-cons F) (! (ncglue O _))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Bug where

data A : Set where
  a : A

h : A -> A
h a = a

data B : A -> Set where
  b : (x : A) -> B (h x)

data _==_ : {x₁ x₂ : A} -> B x₁ -> B x₂ -> Set where
  eqb : {x : A} -> b x == b x

-- The problem here is that we get the constraint h x = h x, which when x is a
-- meta variable we don't solve. This constraint blocks the solution y := b x
-- and so we don't see that y should be dotted. Either explicitly dotting y or
-- binding x removes the problem.
bad : {x : A}{y : B x} -> y == y -> A
bad eqb = ?
-- bad .{h x} .{b x} (eqb {x}) = ?    -- works
-- bad .{y = _} eqb            = ?    -- works
-- bad (eqb {_})               = ?    -- works

-- The above example is solved by checking syntactic equality on blocked terms.
-- This doesn't work below:

infixl 70 _/_
infixl 50 _▻_
infix  40 _∋_ _⊢ _⇒_ _≛_ _≈∋_

mutual

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) -> Γ ⊢ -> Ctxt

  data _⊢ : (Γ : Ctxt) -> Set where
    ✶  : {Γ : Ctxt} -> Γ ⊢

  data _⇒_ : Ctxt -> Ctxt -> Set where
    wk : {Γ : Ctxt} (σ : Γ ⊢) -> Γ ⇒ Γ ▻ σ

  data _∋_ : (Γ : Ctxt) -> Γ ⊢ -> Set where
    vz : {Γ : Ctxt} (τ : Γ ⊢) -> Γ ▻ τ ∋ τ / wk τ

  _/_ : {Γ Δ : Ctxt} -> Γ ⊢ -> Γ ⇒ Δ -> Δ ⊢
  ✶ / ρ = ✶

data _≛_ : {Γ¹ Γ² : Ctxt} -> Γ¹ ⊢ -> Γ² ⊢ -> Set where

data _≈∋_ :  {Γ¹ Γ² : Ctxt} {τ¹ : Γ¹ ⊢} {τ² : Γ² ⊢}
          -> Γ¹ ∋ τ¹ -> Γ² ∋ τ² -> Set where

  vzCong : {Γ¹ : Ctxt} {τ¹ : Γ¹ ⊢}
           {Γ² : Ctxt} {τ² : Γ² ⊢}
    -> τ¹ ≛ τ² -> vz τ¹ ≈∋ vz τ²

f : {Γ¹ : Ctxt} {σ¹ : Γ¹ ⊢} {v¹ : Γ¹ ∋ σ¹}
    {Γ² : Ctxt} {σ² : Γ² ⊢} {v² : Γ² ∋ σ²}
    {Γ³ : Ctxt} {σ³ : Γ³ ⊢} {v³ : Γ³ ∋ σ³}
  -> v¹ ≈∋ v² -> v² ≈∋ v³ -> v¹ ≈∋ v³
f (vzCong eqσ¹²) (vzCong eqσ²³) = ?

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module sv20.assign2.Second_old2 where
-- ------------------------------------------------------------------------

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (≡-decSetoid)
open import Data.List using (List; []; _∷_; _++_)
open import Relation.Binary using (Setoid; DecSetoid)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Relation.Nullary using (¬_; Dec; yes; no)

-- ℕsetoid : Setoid lzero lzero
-- ℕsetoid = record {
--     Carrier = ℕ
--   ; _≈_ = _≡_
--   ; isEquivalence = record {
--       refl = refl
--     ; sym = sym
--     ; trans = trans
--     }
-- }

-- open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
--   using (Pointwise)
--
-- ℕ×ℕdecsetoid : DecSetoid lzero lzero
-- ℕ×ℕdecsetoid = record {
--     Carrier = ℕ × ℕ
--   ; _≈_ = _≡_
--   ; isDecEquivalence = record
--     { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
--     ; _≟_           = ? -- _≟_
--     }
--   }

import Data.List.Relation.Binary.Subset.Setoid as SubSetoid
open SubSetoid (DecSetoid.setoid ≡-decSetoid) using (_⊆_)

--import Data.List.Membership.Setoid
--module ListSetoid = Data.List.Membership.Setoid (ℕsetoid)
--open ListSetoid using (_∈_)

open import Data.List.Membership.DecSetoid (≡-decSetoid) using () renaming (_∈?_ to _∈ℕ?_)
--open import Data.List.Membership.DecSetoid (ℕ×ℕdecsetoid) using () renaming (_∈?_ to _∈ℕ×ℕ?_)
open import Data.List.Relation.Unary.Any using (Any; index; map; here; there)

--simple : [] ⊆ (2 ∷ [])
--simple ()
--
--simple₂ : (1 ∷ []) ⊆ (2 ∷ 1 ∷ [])
--simple₂ (here px) = there (here px)

--Look at:
-- https://agda.github.io/agda-stdlib/Data.List.Relation.Binary.Subset.Propositional.Properties.html
-- https://agda.github.io/agda-stdlib/Data.List.Relation.Binary.Subset.Setoid.html#692
-- https://agda.github.io/agda-stdlib/Relation.Binary.Structures.html#1522

--simple₃ : 1 ∈ (2 ∷ 1 ∷ [])
--simple₃ = ?

-- ⟨Set⟩ are basically lists in Athena. Which is not what a set should be but
-- the professor doesn't care about this, so I can implement this using lists
-- data relation {a b : Set} (A : ⟨Set⟩ a) (B : ⟨Set⟩ b) : ⟨Set⟩ (a × b) where
--
--relation = _×_
--
--range-theorem-2 : ∀ {a b} {A : ⟨Set⟩ a} {B : ⟨Set⟩ b}
--                  (F G : ⟨Set⟩ (a × b))
--                → Range (F intersect G) ⊆ (Range F) intersect (Range G)
--
--range-theorem-2 : ∀ {a b} {A : ⟨Set⟩ a} {B : ⟨Set⟩ b}
--                  (F G : ⟨Set⟩ (a × b))
--                → Range (F ∩ G) ⊆ (Range F) ∩ (Range G)
--
--dom-theorem-3 : ∀ {A B : ⟨Set⟩}
--                (F G : A × B)
--              → (Dom F) diff (Dom G) ⊆ Dom (F diff G)
--
--range-theorem-3 : ∀ {a b} {A : ⟨Set⟩ a} {B : ⟨Set⟩ b}
--                  (F G : A × B)
--                → (Range F) diff (Range G) ⊆ Range (F diff G)

dom : ∀ {A B : Set} → List (A × B) → List A
dom [] = []
dom (⟨ x , _ ⟩ ∷ ls) = x ∷ dom ls

range : ∀ {A B : Set} → List (A × B) → List B
range [] = []
range (⟨ _ , y ⟩ ∷ ls) = y ∷ range ls

_∩ℕ_ : List ℕ → List ℕ → List ℕ
--_∩ : List A → List A → List A
[] ∩ℕ _ = []
--xs ∩ ys = ?
(x ∷ xs) ∩ℕ ys with x ∈ℕ? ys
...               | yes _ = x ∷ (xs ∩ℕ ys)
...               | no  _ = xs ∩ℕ ys

--_intersectℕ×ℕ_ : List (ℕ × ℕ) → List (ℕ × ℕ) → List (ℕ × ℕ)
----_intersect_ : List A → List A → List A
--[] intersectℕ×ℕ _ = []
----xs intersect ys = ?
--(x ∷ xs) intersectℕ×ℕ ys with x ∈ℕ×ℕ? ys
--...               | yes _ = x ∷ (xs intersectℕ×ℕ ys)
--...               | no  _ = xs intersectℕ×ℕ ys

simple-theorem : (F G : List ℕ)
               → (F ∩ℕ G) ⊆ F
simple-theorem []       _  p = p
simple-theorem (x ∷ xs) ys = ? -- NO IDEA HOW TO PROCEDE EVEN WITH THE "SIMPLEST" OF CASES
--simple-theorem (x ∷ xs) ys = ?
-- λ x xs ys x₁ → x₁ ListSetoid.∈ ((x ∷ xs) intersectℕ ys) → x₁ ListSetoid.∈ x ∷ xs}
--simple-theorem [] _ p      = p
--simple-theorem (x ∷ xs) [] = ?
--simple-theorem (x ∷ xs) (y ∷ ys) = ?

-- (2 ∷ 3 ∷ 60 ∷ []) intersectℕ (1 ∷ 3 ∷ 2 ∷ [])

-- (⟨ 2 , 0 ⟩ ∷ ⟨ 3 , 2 ⟩ ∷ ⟨ 60 , 1 ⟩ ∷ []) intersectℕ (1 ∷ 3 ∷ 2 ∷ [])

--module Intersect {a ℓ} (DS : DecSetoid a ℓ) where
--  open import Data.List.Membership.DecSetoid (DS) using (_∈?_)
--  --open DecSetoid DS using (_≟_)
--
--  A = DecSetoid.Carrier DS
--
--  --_intersect_ : List ℕ → List ℕ → List ℕ
--  _intersect_ : List A → List A → List A
--  [] intersect ys = ys
--  --xs intersect ys = ?
--  (x ∷ xs) intersect ys with x ∈? ys
--  ...               | yes _ = x ∷ (xs intersect ys)
--  ...               | no  _ = xs intersect ys
--
--
--import Data.List.Relation.Binary.Subset.Setoid as SubSetoid
--
--module Range-Theorem-2 {a ℓ} (DS₁ : DecSetoid a ℓ) (DS₂ : DecSetoid a ℓ) where
--  A = DecSetoid.Carrier DS₁
--  B = DecSetoid.Carrier DS₂
--
--  DSboth : DecSetoid a ℓ
--  DSboth = record {
--      Carrier = A × B
--    ; _≈_ = ?
--    ; isDecEquivalence = ?
--    }
--
--  open Intersect (DSboth) using (_intersect_)
--  open Intersect (DS₂) using () renaming (_intersect_ to _intersect₂_)
--
--  S₂setoid : Setoid a ℓ
--  S₂setoid = record {
--      Carrier = B
--    ; _≈_ = DecSetoid._≈_ DS₂
--    ; isEquivalence = Setoid.isEquivalence (DecSetoid.setoid DS₂)
--    }
--  open SubSetoid (S₂setoid) using (_⊆_)
--
--  range-theorem-2 : --∀ {A B : Set}
--                    (F G : List (A × B))
--                    --(F G : List (ℕ × ℕ))
--                  → range (F intersect G) ⊆ (range F) intersect₂ (range G)
--  range-theorem-2 [] _ p      = p
--  range-theorem-2 (x ∷ xs) [] = ?
--  range-theorem-2 (x ∷ xs) (y ∷ ys) = ?

--open import Data.AVL.Sets using (⟨Set⟩; empty; insert; delete)


text:
module Issue307 where

postulate A : Set

_! : A → A
x ! = x

! : A → A
! x = x

data D : Set where
  d : D → D

syntax d x = x d

f : D → D
f (x d) = x

g : D → D
g (d x) = x


text:
-- Andreas, 2015-09-09 Issue 1643
-- {-# OPTIONS -v tc.mod.apply:20 #-}
-- {-# OPTIONS -v tc.signature:30 #-}
-- {-# OPTIONS -v tc.display:100  #-}
-- {-# OPTIONS -v scope:50 -v scope.inverse:100 -v interactive.meta:20 #-}

module _ where

module M where
  postulate A : Set

module N = M  -- This alias used to introduce a display form M.A --> N.A

open N

postulate
  a : A

test : Set
test = a

-- ERROR SHOULD BE:   A !=< Set of type Set


text:
module PatternSynonymNoParse where

pattern f x = a b


text:
------------------------------------------
-- Mathematical induction derived from Z
------------------------------------------

module sv20.assign2.SetTheory.PMI where

open import sv20.assign2.SetTheory.Logic
open import sv20.assign2.SetTheory.ZAxioms
open import sv20.assign2.SetTheory.Algebra
open import sv20.assign2.SetTheory.Subset
open import sv20.assign2.SetTheory.Pairs

-- Axiom of infinity
postulate
  infinity : ∃ (λ I → ∅ ∈ I ∧ ∀ x → x ∈ I → x ∪ singleton x ∈ I)

succ : 𝓢 → 𝓢
succ x = x ∪ singleton x

-- Inductive property
Inductive : 𝓢 → Set
Inductive A = ∅ ∈ A ∧ ((x : 𝓢) → x ∈ A → succ x ∈ A)

-- An inductive set.
I : 𝓢
I = proj₁ infinity

formulaN : 𝓢 → Set
formulaN x = (A : 𝓢) → Inductive A → x ∈ A

fullN : ∃ (λ B → {z : 𝓢} → z ∈ B ⇔ z ∈ I ∧ formulaN z)
fullN = sub formulaN I

ℕ : 𝓢
ℕ = proj₁ fullN

x∈ℕ→x∈InductiveSet : (x : 𝓢) → x ∈ ℕ → (A : 𝓢) → Inductive A → x ∈ A
x∈ℕ→x∈InductiveSet x h = ∧-proj₂ (∧-proj₁ (proj₂ _ fullN) h)

-- PMI version from Ivorra Castillo (n.d.), Teorema 8.13.
PMI : (A : 𝓢) → A ⊆ ℕ → ∅ ∈ A → ((n : 𝓢) → n ∈ A → succ n ∈ A) → A ≡ ℕ
PMI A h₁ h₂ h₃ = equalitySubset A ℕ (prf₁ , prf₂)
  where
  prf₁ : (z : 𝓢) → z ∈ A → z ∈ ℕ
  prf₁ z h = h₁ z h

  inductiveA : Inductive A
  inductiveA = h₂ , h₃

  prf₂ : (z : 𝓢) → z ∈ ℕ → z ∈ A
  prf₂ z h = x∈ℕ→x∈InductiveSet z h A inductiveA

-- References
--
-- Suppes, Patrick (1960). Axiomatic Set Theory.
-- The University Series in Undergraduate Mathematics.
-- D. Van Nostrand Company, inc.
--
-- Enderton, Herbert B. (1977). Elements of Set Theory.
-- Academic Press Inc.
--
-- Ivorra Castillo, Carlos (n.d.). Lógica y Teoría de
-- Conjuntos. https://www.uv.es/ivorra/


text:
module tmp where

open import univ
open import cwf
open import Base
open import Nat
open import help
open import proofs

{- TODO: Prove

  w = ƛ ((w // wk) ∙ vz)    (η)

  ƛ v // σ = ƛ (v // (σ ∘ wk ,, vz))
  w ∙ u // σ = (w // σ) ∙ (u // σ)

-}

{-
lem-tmp : {Γ : Con}{A : Type Γ}(B : Type (Γ , A)) ->
	  Π A B =Ty Π A (B / (wk ∘ wk ,, castElem ? vz) / [ vz ])
lem-tmp B = ?

lem-η : {Γ : Con}{A : Type Γ}{B : Type (Γ , A)}(w : Elem Γ (Π A B)) ->
	w =El castElem (lem-tmp B)
	      (ƛ {A = A}
		 (castElem (symTy (lem-Π/ B wk)) (w // wk {A = A}) ∙ vz)
	      )
lem-η (elem (el < w , pw >)) = ?
-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on containers
------------------------------------------------------------------------

module Data.Container.FreeMonad where

open import Level
open import Function using (_∘_)
open import Data.Empty using (⊥-elim)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product
open import Data.Container
open import Data.Container.Combinator using (const; _⊎_)
open import Data.W
open import Category.Monad

infixl 1 _⋆C_
infix  1 _⋆_

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

-- The free monad construction over a container and a set is, in
-- universal algebra terminology, also known as the term algebra over a
-- signature (a container) and a set (of variable symbols). The return
-- of the free monad corresponds to variables and the bind operator
-- corresponds to (parallel) substitution.

-- A useful intuition is to think of containers describing single
-- operations and the free monad construction over a container and a set
-- describing a tree of operations as nodes and elements of the set as
-- leafs. If one starts at the root, then any path will pass finitely
-- many nodes (operations described by the container) and eventually end
-- up in a leaf (element of the set) -- hence the Kleene star notation
-- (the type can be read as a regular expression).

_⋆C_ : ∀ {c} → Container c → Set c → Container c
C ⋆C X = const X ⊎ C

_⋆_ : ∀ {c} → Container c → Set c → Set c
C ⋆ X = μ (C ⋆C X)

do : ∀ {c} {C : Container c} {X} → ⟦ C ⟧ (C ⋆ X) → C ⋆ X
do (s , k) = sup (inj₂ s) k

rawMonad : ∀ {c} {C : Container c} → RawMonad (_⋆_ C)
rawMonad = record { return = return; _>>=_ = _>>=_ }
  where
  return : ∀ {c} {C : Container c} {X} → X → C ⋆ X
  return x = sup (inj₁ x) (⊥-elim ∘ lower)

  _>>=_ : ∀ {c} {C : Container c} {X Y} → C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
  sup (inj₁ x) _ >>= k = k x
  sup (inj₂ s) f >>= k = do (s , λ p → f p >>= k)