text:
module MLib.Algebra.PropertyCode.Core where

open import MLib.Prelude
open import MLib.Finite
import MLib.Finite.Properties as FiniteProps
open import MLib.Algebra.PropertyCode.RawStruct

import Relation.Unary as U using (Decidable)
open import Relation.Binary as B using (Setoid)

open List.All using (All; _∷_; [])
open import Data.List.Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)

open import Data.Vec.N-ary

open import Data.Product.Relation.SigmaPropositional as OverΣ using (OverΣ)

open import Data.Bool using (T)

open import Category.Applicative

open LeftInverse using () renaming (_∘_ to _∘ⁱ_)
open FE using (_⇨_; cong)
open import Function.Equivalence using (Equivalence)

open Table using (Table)
open Algebra using (IdempotentCommutativeMonoid)

--------------------------------------------------------------------------------
--  Extra theorems about bools
--------------------------------------------------------------------------------

open Bool

module BoolExtra where
  _⇒_ : Bool → Bool → Bool
  false ⇒ false = true
  false ⇒ true = true
  true ⇒ false = false
  true ⇒ true = true

  true⇒ : ∀ {x} → true ⇒ x ≡ x
  true⇒ {false} = ≡.refl
  true⇒ {true} = ≡.refl

  MP : ∀ {x y} → T (x ⇒ y) → T x → T y
  MP {false} {false} _ ()
  MP {false} {true} _ _ = tt
  MP {true} {false} ()
  MP {true} {true} _ _ = tt

  abs : ∀ {x y} → (T x → T y) → T (x ⇒ y)
  abs {false} {false} f = tt
  abs {false} {true} f = tt
  abs {true} {false} f = f tt
  abs {true} {true} f = tt

  ∧-elim : ∀ {x y} → T (x ∧ y) → T x × T y
  ∧-elim {false} {false} ()
  ∧-elim {false} {true} ()
  ∧-elim {true} {false} ()
  ∧-elim {true} {true} p = tt , tt

--------------------------------------------------------------------------------
--  Universe of properties
--------------------------------------------------------------------------------

data PropKind : Set where
  associative commutative idempotent selective cancellative
    leftIdentity rightIdentity
    leftZero rightZero
    distributesOverˡ distributesOverʳ
    : PropKind

opArities : PropKind → List ℕ
opArities associative      = 2 ∷ []
opArities commutative      = 2 ∷ []
opArities idempotent       = 2 ∷ []
opArities selective        = 2 ∷ []
opArities cancellative     = 2 ∷ []
opArities leftIdentity     = 0 ∷ 2 ∷ []
opArities rightIdentity    = 0 ∷ 2 ∷ []
opArities leftZero         = 0 ∷ 2 ∷ []
opArities rightZero        = 0 ∷ 2 ∷ []
opArities distributesOverˡ = 2 ∷ 2 ∷ []
opArities distributesOverʳ = 2 ∷ 2 ∷ []

module _ {c ℓ k} {K : ℕ → Set k} (rawStruct : RawStruct K c ℓ) where
  open RawStruct rawStruct
  open Algebra.FunctionProperties _≈_

  interpret : (π : PropKind) → All K (opArities π) → Set (c ⊔ˡ ℓ)
  interpret associative      (∙ ∷ [])     = Associative ⟦ ∙ ⟧
  interpret commutative      (∙ ∷ [])     = Commutative ⟦ ∙ ⟧
  interpret idempotent       (∙ ∷ [])     = Idempotent ⟦ ∙ ⟧
  interpret selective        (∙ ∷ [])     = Selective ⟦ ∙ ⟧
  interpret cancellative     (∙ ∷ [])     = Cancellative ⟦ ∙ ⟧
  interpret leftIdentity     (ε ∷ ∙ ∷ []) = LeftIdentity ⟦ ε ⟧ ⟦ ∙ ⟧
  interpret rightIdentity    (ε ∷ ∙ ∷ []) = RightIdentity ⟦ ε ⟧ ⟦ ∙ ⟧
  interpret leftZero         (ω ∷ ∙ ∷ []) = LeftZero ⟦ ω ⟧ ⟦ ∙ ⟧
  interpret rightZero        (ω ∷ ∙ ∷ []) = RightZero ⟦ ω ⟧ ⟦ ∙ ⟧
  interpret distributesOverˡ (* ∷ + ∷ []) = ⟦ * ⟧ DistributesOverˡ ⟦ + ⟧
  interpret distributesOverʳ (* ∷ + ∷ []) = ⟦ * ⟧ DistributesOverʳ ⟦ + ⟧

Property : ∀ {k} (K : ℕ → Set k) → Set k
Property K = ∃ (All K ∘ opArities)

module PropertyC where
  natsEqual : ℕ → ℕ → Bool
  natsEqual Nat.zero Nat.zero = true
  natsEqual Nat.zero (Nat.suc y) = false
  natsEqual (Nat.suc x) Nat.zero = false
  natsEqual (Nat.suc x) (Nat.suc y) = natsEqual x y

  aritiesMatch : List ℕ → List ℕ → Bool
  aritiesMatch [] [] = true
  aritiesMatch [] (x ∷ ys) = false
  aritiesMatch (x ∷ xs) [] = false
  aritiesMatch (x ∷ xs) (y ∷ ys) = natsEqual x y ∧ aritiesMatch xs ys

  natsEqual-correct : ∀ {m n} → T (natsEqual m n) → m ≡ n
  natsEqual-correct {Nat.zero} {Nat.zero} p = ≡.refl
  natsEqual-correct {Nat.zero} {Nat.suc n} ()
  natsEqual-correct {Nat.suc m} {Nat.zero} ()
  natsEqual-correct {Nat.suc m} {Nat.suc n} p = ≡.cong Nat.suc (natsEqual-correct p)

  aritiesMatch-correct : ∀ {xs ys} → T (aritiesMatch xs ys) → xs ≡ ys
  aritiesMatch-correct {[]} {[]} p = ≡.refl
  aritiesMatch-correct {[]} {x ∷ ys} ()
  aritiesMatch-correct {x ∷ xs} {[]} ()
  aritiesMatch-correct {x ∷ xs} {y ∷ ys} p =
    let q , r = BoolExtra.∧-elim {natsEqual x y} p
    in ≡.cong₂ _∷_ (natsEqual-correct q) (aritiesMatch-correct r)

  _on_ : ∀ {k} {K : ℕ → Set k} {n : ℕ} (π : PropKind) {_ : T (aritiesMatch (opArities π) (n ∷ []))} → K n → Property K
  _on_ {K = K} π {match} κ = π , ≡.subst (All K) (≡.sym (aritiesMatch-correct {opArities π} match)) (κ ∷ [])

  _is_for_ : ∀ {k} {K : ℕ → Set k} {m n : ℕ} → K m → (π : PropKind) {_ : T (aritiesMatch (opArities π) (m ∷ n ∷ []))} → K n → Property K
  _is_for_ {K = K} α π {match} ∙ = π , ≡.subst (All K) (≡.sym (aritiesMatch-correct {opArities π} match)) (α ∷ ∙ ∷ [])

  _⟨_⟩ₚ_ = _is_for_

⟦_⟧P : ∀ {c ℓ k} {K : ℕ → Set k} → Property K → RawStruct K c ℓ → Set (c ⊔ˡ ℓ)
⟦ π , ops ⟧P rawStruct = interpret rawStruct π ops

PropKind-IsFiniteSet : IsFiniteSet PropKind _
PropKind-IsFiniteSet = record
  { ontoFin = record
    { to = ≡.→-to-⟶ to
    ; from = ≡.→-to-⟶ from
    ; left-inverse-of = left-inverse-of
    }
  }
  where
    open Fin using (#_) renaming (zero to z; suc to s_)

    N = 11

    to : PropKind → Fin N
    to associative      = # 0
    to commutative      = # 1
    to idempotent       = # 2
    to selective        = # 3
    to cancellative     = # 4
    to leftIdentity     = # 5
    to rightIdentity    = # 6
    to leftZero         = # 7
    to rightZero        = # 8
    to distributesOverˡ = # 9
    to distributesOverʳ = # 10

    from : Fin N → PropKind
    from z                       = associative
    from (s z)                   = commutative
    from (s s z)                 = idempotent
    from (s s s z)               = selective
    from (s s s s z)             = cancellative
    from (s s s s s z)           = leftIdentity
    from (s s s s s s z)         = rightIdentity
    from (s s s s s s s z)       = leftZero
    from (s s s s s s s s z)     = rightZero
    from (s s s s s s s s s z)   = distributesOverˡ
    from (s s s s s s s s s s z) = distributesOverʳ
    from (s s s s s s s s s s s ())

    left-inverse-of : ∀ x → from (to x) ≡ x
    left-inverse-of associative      = ≡.refl
    left-inverse-of commutative      = ≡.refl
    left-inverse-of idempotent       = ≡.refl
    left-inverse-of selective        = ≡.refl
    left-inverse-of cancellative     = ≡.refl
    left-inverse-of leftIdentity     = ≡.refl
    left-inverse-of rightIdentity    = ≡.refl
    left-inverse-of leftZero         = ≡.refl
    left-inverse-of rightZero        = ≡.refl
    left-inverse-of distributesOverˡ = ≡.refl
    left-inverse-of distributesOverʳ = ≡.refl

finitePropKind : FiniteSet _ _
finitePropKind = record { isFiniteSetoid = PropKind-IsFiniteSet }

--------------------------------------------------------------------------------
--  Subsets of properties over a particular operator code type
--------------------------------------------------------------------------------

record Code k : Set (sucˡ k) where
  field
    K : ℕ → Set k
    boundAt : ℕ → ℕ
    isFiniteAt : ∀ n → IsFiniteSet (K n) (boundAt n)

  finiteSetAt : ℕ → FiniteSet _ _
  finiteSetAt n = record { isFiniteSetoid = isFiniteAt n }

  module K n = FiniteSet (finiteSetAt n)

  module Property where
    finiteSet : FiniteSet _ _
    finiteSet = record
      { isFiniteSetoid =
          Σ-isFiniteSetoid PropKind-IsFiniteSet (All-finiteSet finiteSetAt ∘ opArities)
      }

    open FiniteSet finiteSet public
    open FiniteProps finiteSet public

    ≈⇒≡ : ∀ {π π′} → π ≈ π′ → π ≡ π′
    ≈⇒≡ {π , κ} {.π , κ′} (≡.refl , snd) with All′.PW-≡ _ snd
    ≈⇒≡ {π , κ} {.π , .κ} (≡.refl , snd) | ≡.refl = ≡.refl

record IsSubcode {k k′} (sub : Code k) (sup : Code k′) : Set (k ⊔ˡ k′) where
  constructor subcode

  private
    module Sub = Code sub
    module Sup = Code sup

  field
    subK→supK : ∀ {n} → Sub.K n → Sup.K n
    supK→subK : ∀ {n} → Sup.K n → Maybe (Sub.K n)
    acrossSub : ∀ {n} (κ : Sub.K n) → supK→subK (subK→supK κ) ≡ just κ

mapProperty :
  ∀ {k k′} {K : ℕ → Set k} {K′ : ℕ → Set k′}
  → (∀ {n} → K′ n → K n)
  → Property K′
  → Property K
mapProperty f (π , κs) = π , List.All.map f κs

record Properties {k} (code : Code k) : Set k where
  constructor properties

  open Code code using (K; module Property)

  field
    hasProperty : Property K → Bool

  hasPropertyF : Property.setoid ⟶ ≡.setoid Bool
  _⟨$⟩_ hasPropertyF = hasProperty
  cong hasPropertyF (≡.refl , q) rewrite All′.PW-≡ K q = ≡.refl

open Properties public

module _ {k} {code : Code k} where
  open Code code using (K; module Property)

  Property-Func : Setoid _ _
  Property-Func = Property.setoid ⇨ ≡.setoid Bool

  Properties-setoid : Setoid _ _
  Properties-setoid = record
    { Carrier = Properties code
    ; _≈_ = λ Π Π′ → hasPropertyF Π ≈ hasPropertyF Π′
    ; isEquivalence = record
      { refl = λ {Π} → refl {hasPropertyF Π}
      ; sym = λ {Π} {Π′} → sym {hasPropertyF Π} {hasPropertyF Π′}
      ; trans = λ {Π} {Π′} {Π′′} → trans {hasPropertyF Π} {hasPropertyF Π′} {hasPropertyF Π′′}
      }
    }
    where
    open Setoid Property-Func

  Properties↞Func : LeftInverse Properties-setoid Property-Func
  Properties↞Func = record
    { to = record { _⟨$⟩_ = hasPropertyF ; cong = id }
    ; from = record { _⟨$⟩_ = properties ∘ _⟨$⟩_ ; cong = id }
    ; left-inverse-of = left-inverse-of
    }
    where
    open Setoid Property.setoid using (_≈_)
    left-inverse-of : ∀ (Π : Properties code) {π π′} → π ≈ π′ → hasProperty Π π ≡ hasProperty Π π′
    left-inverse-of Π (≡.refl , p) rewrite All′.PW-≡ K p = ≡.refl

  -- Properties↞ℕ : LeftInverse Properties-setoid (≡.setoid ℕ)
  -- Properties↞ℕ = asNat Property.finiteSet ∘ⁱ Properties↞Func

  -- Evaluates to 'true' only when every property is present.

  hasAll : Properties code → Bool
  hasAll Π = Property.foldMap Bool.∧-idempotentCommutativeMonoid (hasProperty Π)

  implies : Properties code → Properties code → Bool
  implies Π₁ Π₂ = Property.foldMap Bool.∧-idempotentCommutativeMonoid (λ π → hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π)

  -- The full set of properties

  True : Properties code
  hasProperty True _ = true

  -- The empty set of properties

  False : Properties code
  hasProperty False _ = false

  -- Inhabited if the given property is present. Suitable for use as an instance
  -- argument.

  record _∈ₚ_ (π : Property K) (Π : Properties code) : Set where
    instance constructor fromTruth
    field
      truth : T (hasProperty Π π)

  open _∈ₚ_

  -- Inhabited if the first set of properties implies the second. Suitable for
  -- use as an instance argument but difficult to work with.

  record _⇒ₚ_ (Π₁ Π₂ : Properties code) : Set where
    instance constructor fromTruth
    field
      truth : T (implies Π₁ Π₂)

  ⊨ : Properties code → Set
  ⊨ Π = True ⇒ₚ Π

  -- Inhabited if the first set of properties implies the second. Unsuitable for
  -- use as an instance argument, but easy to work with.

  _→ₚ_ : Properties code → Properties code → Set k
  Π₁ →ₚ Π₂ = ∀ π → π ∈ₚ Π₁ → π ∈ₚ Π₂

  ⊢ : Properties code → Set k
  ⊢ Π = True →ₚ Π

  -- The two forms of implication are equivalent to each other, as we would hope

  →ₚ-⇒ₚ : {Π₁ Π₂ : Properties code} → Π₁ →ₚ Π₂ → Π₁ ⇒ₚ Π₂
  →ₚ-⇒ₚ {Π₁} {Π₂} p = _⇒ₚ_.fromTruth (Equivalence.from T-≡ ⟨$⟩ impl-true)
    where
    open ≡.Reasoning

    icm = Bool.∧-idempotentCommutativeMonoid

    impl-pointwise : ∀ π → hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π ≡ true
    impl-pointwise π = Equivalence.to T-≡ ⟨$⟩ BoolExtra.abs (truth ∘ p π ∘ fromTruth)

    impl-true : implies Π₁ Π₂ ≡ true
    impl-true = begin
      implies Π₁ Π₂                 ≡⟨⟩
      Property.foldMap icm (λ π → hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π) ≡⟨ Property.foldMap-cong icm impl-pointwise ⟩
      Property.foldMap icm (λ _ → true) ≡⟨ proj₁ (IdempotentCommutativeMonoid.identity icm) _ ⟩
      true ∧ Property.foldMap icm (λ _ → true) ≡⟨ Property.foldMap-const icm ⟩
      true ∎

  ⇒ₚ-→ₚ : {Π₁ Π₂ : Properties code} → Π₁ ⇒ₚ Π₂ → Π₁ →ₚ Π₂
  ⇒ₚ-→ₚ {Π₁} {Π₂} (fromTruth p) π (fromTruth q) = fromTruth (BoolExtra.MP (Equivalence.from T-≡ ⟨$⟩ impl-π) q)
    where
      i = Property.toIx π

      open ≡.Reasoning
      icm = Bool.∧-idempotentCommutativeMonoid
      module ∧ = IdempotentCommutativeMonoid icm

      implies-true : implies Π₁ Π₂ ≡ true
      implies-true = Equivalence.to T-≡ ⟨$⟩ p

      implies-F : Property.setoid ⟶ ≡.setoid Bool
      implies-F = record
        { _⟨$⟩_ = λ π → hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π
        ; cong = λ { {π} {π′} p → ≡.cong₂ BoolExtra._⇒_ (cong (hasPropertyF Π₁) p) (cong (hasPropertyF Π₂) p)}
        }

      impl-π : hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π ≡ true
      impl-π = begin
        hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π                     ≡⟨ ≡.sym (proj₂ ∧.identity _) ⟩
        (hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π) ∧ true            ≡⟨ ∧.∙-cong (≡.refl {x = hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π}) (≡.sym implies-true) ⟩
        (hasProperty Π₁ π BoolExtra.⇒ hasProperty Π₂ π) ∧ implies Π₁ Π₂   ≡⟨ Property.enumₜ-complete icm implies-F π ⟩
        implies Π₁ Π₂                                                     ≡⟨ implies-true ⟩
        true ∎

  -- Form a set of properties from a single property

  singleton : Property K → Properties code
  hasProperty (singleton π) π′ = ⌊ π Property.≟ π′ ⌋

  -- Union of two sets of properties

  _∪ₚ_ : Properties code → Properties code → Properties code
  hasProperty (Π₁ ∪ₚ Π₂) π = hasProperty Π₁ π ∨ hasProperty Π₂ π

  -- Form a set of properties from a list of properties

  fromList : List (Property K) → Properties code
  fromList = List.foldr (_∪ₚ_ ∘ singleton) False

  π-∈ₚ-singleton : ∀ {π} → π ∈ₚ singleton π
  truth (π-∈ₚ-singleton {π}) with π Property.≟ π
  truth (π-∈ₚ-singleton {π}) | yes p = _
  truth (π-∈ₚ-singleton {π}) | no ¬p = ¬p Property.refl

  _⊆_ : Properties code → Properties code → Properties code
  hasProperty (Π₁ ⊆ Π₂) π = not (hasProperty Π₁ π) ∨ hasProperty Π₂ π

  →ₚ-trans : ∀ {Π₁ Π₂ Π₃} → Π₁ →ₚ Π₂ → Π₂ →ₚ Π₃ → Π₁ →ₚ Π₃
  →ₚ-trans {Π₁} p q π = q π ∘ p π

  ⇒ₚ-trans : ∀ {Π₁ Π₂ Π₃} → Π₁ ⇒ₚ Π₂ → Π₂ ⇒ₚ Π₃ → Π₁ ⇒ₚ Π₃
  ⇒ₚ-trans {Π₁} p q = →ₚ-⇒ₚ (→ₚ-trans (⇒ₚ-→ₚ p) (⇒ₚ-→ₚ q))

  ⇒ₚ-MP : ∀ {Π Π′ π} → π ∈ₚ Π′ → Π′ ⇒ₚ Π → π ∈ₚ Π
  ⇒ₚ-MP {Π = Π} {Π′} {π} hasπ has⇒ = ⇒ₚ-→ₚ has⇒ π hasπ

  ⇒ₚ-weaken : ∀ {Π Π′ Π′′ : Properties code} (hasΠ′ : Π′ ⇒ₚ Π) ⦃ hasΠ′′ : Π′′ ⇒ₚ Π′ ⦄ → Π′′ ⇒ₚ Π
  ⇒ₚ-weaken hasΠ′ ⦃ hasΠ′′ ⦄ = ⇒ₚ-trans hasΠ′′ hasΠ′

module _ {k k′} {sub : Code k} {sup : Code k′} (isSub : IsSubcode sub sup) where
  private
    module Sub = Code sub
    module Sup = Code sup

  open IsSubcode isSub public

  subcodeProperties : Properties sup → Properties sub
  hasProperty (subcodeProperties Π) = hasProperty Π ∘ mapProperty subK→supK

  supcodeProperties : Properties sub → Properties sup
  hasProperty (supcodeProperties Π) (π , κs) with List.All.traverse supK→subK κs
  hasProperty (supcodeProperties Π) (π , κs) | just κs′ = hasProperty Π (π , κs′)
  hasProperty (supcodeProperties Π) (π , κs) | nothing = false

  fromSubcode :
    ∀ {π} {Π : Properties sup}
    → π ∈ₚ subcodeProperties Π
    → mapProperty subK→supK π ∈ₚ Π
  fromSubcode (fromTruth truth) = fromTruth truth

  fromSupcode :
    ∀ {π} {Π : Properties sup}
    → mapProperty subK→supK π ∈ₚ Π
    → π ∈ₚ subcodeProperties Π
  fromSupcode (fromTruth truth) = fromTruth truth

  fromSupcode′ : ∀ {π} {Π : Properties sub} →
    π ∈ₚ Π → mapProperty subK→supK π ∈ₚ supcodeProperties Π
  fromSupcode′ {π , κs} π∈Π ._∈ₚ_.truth with lem
    where
    open ≡.Reasoning
    lem : List.All.traverse supK→subK (List.All.map subK→supK κs) ≡ just κs
    lem = begin
      List.All.traverse supK→subK (List.All.map subK→supK κs) ≡⟨ List-All.traverse-map supK→subK subK→supK κs ⟩
      List.All.traverse (supK→subK ∘ subK→supK) κs ≡⟨ List-All.traverse-cong (supK→subK ∘ subK→supK) just acrossSub κs ⟩
      List.All.traverse just κs ≡⟨ List-All.traverse-just κs ⟩
      just κs ∎
  fromSupcode′ {π , κs} π∈Π ._∈ₚ_.truth | p rewrite p = π∈Π ._∈ₚ_.truth

  module _
    {c ℓ}
    (sup-rawStruct : RawStruct Sup.K c ℓ)
    (sub-isRawStruct : IsRawStruct (RawStruct._≈_ sup-rawStruct) (RawStruct.appOp sup-rawStruct ∘ subK→supK)) where

    sub-rawStruct : RawStruct Sub.K c ℓ
    sub-rawStruct = record { isRawStruct = sub-isRawStruct }

    reinterpret :
      ∀ (π : Property Sub.K)
      → ⟦ mapProperty subK→supK π ⟧P sup-rawStruct → ⟦ π ⟧P sub-rawStruct
    reinterpret (associative      , ∙ ∷ [])     = id
    reinterpret (commutative      , ∙ ∷ [])     = id
    reinterpret (idempotent       , ∙ ∷ [])     = id
    reinterpret (selective        , ∙ ∷ [])     = id
    reinterpret (cancellative     , ∙ ∷ [])     = id
    reinterpret (leftIdentity     , α ∷ ∙ ∷ []) = id
    reinterpret (rightIdentity    , α ∷ ∙ ∷ []) = id
    reinterpret (leftZero         , α ∷ ∙ ∷ []) = id
    reinterpret (rightZero        , α ∷ ∙ ∷ []) = id
    reinterpret (distributesOverˡ , * ∷ + ∷ []) = id
    reinterpret (distributesOverʳ , * ∷ + ∷ []) = id


text:
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ; _≟[_]_ )
open import FRP.JS.Nat using ( ℕ ; _≟_ ; _+_ ; _*_ ; _∸_ ; _/_ ; _/?_ ; _≤_ ; _<_ ; show ; float )
open import FRP.JS.Float using ( ℝ ) renaming ( _≟_ to _≟r_ )
open import FRP.JS.String using () renaming ( _≟_ to _≟s_ )
open import FRP.JS.QUnit using ( TestSuite ; ok ; ok! ; test ; _,_ )

module FRP.JS.Test.Nat where

infixr 2 _≟?r_

_≟?r_ : Maybe ℝ → Maybe ℝ → Bool
x ≟?r y = x ≟[ _≟r_ ] y

tests : TestSuite
tests =
  ( test "≟"
    ( ok "0 ≟ 0" (0 ≟ 0)
    , ok "1 ≟ 1" (1 ≟ 1)
    , ok "2 ≟ 2" (2 ≟ 2)
    , ok "0 != 1" (not (0 ≟ 1))
    , ok "0 != 2" (not (0 ≟ 2))
    , ok "1 != 2" (not (1 ≟ 2))
    , ok "1 != 0" (not (1 ≟ 0)) )
  , test "+"
    ( ok "0 + 0" (0 + 0 ≟ 0)
    , ok "1 + 1" (1 + 1 ≟ 2)
    , ok "37 + 0" (37 + 0 ≟ 37)
    , ok "37 + 1" (37 + 1 ≟ 38)
    , ok "37 + 5" (37 + 5 ≟ 42) )
  , test "*"
    ( ok "0 * 0" (0 * 0 ≟ 0)
    , ok "1 * 1" (1 * 1 ≟ 1)
    , ok "37 * 0" (37 * 0 ≟ 0)
    , ok "37 * 1" (37 * 1 ≟ 37)
    , ok "37 * 5" (37 * 5 ≟ 185) )
  , test "∸"
    ( ok "0 ∸ 0" (0 ∸ 0 ≟ 0)
    , ok "1 ∸ 1" (1 ∸ 1 ≟ 0)
    , ok "37 ∸ 0" (37 ∸ 0 ≟ 37)
    , ok "37 ∸ 1" (37 ∸ 1 ≟ 36)
    , ok "37 ∸ 5" (37 ∸ 5 ≟ 32)
    , ok "5 ∸ 37" (5 ∸ 37 ≟ 0) )
  , test "/"
    ( ok "1 / 1" (1 / 1 ≟r 1.0)
    , ok "37 / 1" (37 / 1 ≟r 37.0)
    , ok "37 / 5" (37 / 5 ≟r 7.4)
    , ok "0 /? 0" (0 /? 0 ≟?r nothing)
    , ok "1 /? 1" (1 /? 1 ≟?r just 1.0)
    , ok "37 /? 0" (37 /? 0 ≟?r nothing)
    , ok "37 /? 1" (37 /? 1 ≟?r just 37.0)
    , ok "37 /? 5" (37 /? 5 ≟?r just 7.4) )
  , test "≤"
    ( ok "0 ≤ 0" (0 ≤ 0)
    , ok "0 ≤ 1" (0 ≤ 1)
    , ok "1 ≤ 0" (not (1 ≤ 0))
    , ok "1 ≤ 1" (1 ≤ 1)
    , ok "37 ≤ 0" (not (37 ≤ 0))
    , ok "37 ≤ 1" (not (37 ≤ 1))
    , ok "37 ≤ 5" (not (37 ≤ 5))
    , ok "5 ≤ 37" (5 ≤ 37) )
  , test "<"
    ( ok "0 < 0" (not (0 < 0))
    , ok "0 < 1" (0 < 1)
    , ok "1 < 0" (not (1 < 0))
    , ok "1 < 1" (not (1 < 1))
    , ok "37 < 0" (not (37 < 0))
    , ok "37 < 1" (not (37 < 1))
    , ok "37 < 5" (not (37 < 5))
    , ok "5 < 37" (5 < 37) )
  , test "show"
    ( ok "show 0" (show 0 ≟s "0")
    , ok "show 1" (show 1 ≟s "1")
    , ok "show 5" (show 5 ≟s "5")
    , ok "show 37" (show 37 ≟s "37") )
  , test "float"
    ( ok "float 0" (float 0 ≟r 0.0)
    , ok "float 1" (float 1 ≟r 1.0)
    , ok "float 5" (float 5 ≟r 5.0)
    , ok "float 37" (float 37 ≟r 37.0) )
  )

ext: agda

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra hiding (⟨_⟩a)

private
  variable
    ℓ ℓ′ : Level

record IsCommAlgebra (R : CommRing {ℓ}) {A : Type ℓ}
                     (0a : A) (1a : A)
                     (_+_ : A → A → A) (_·_ : A → A → A) (-_ : A → A)
                     (_⋆_ : ⟨ R ⟩ → A → A) : Type ℓ where

  constructor iscommalgebra

  field
    isAlgebra : IsAlgebra (CommRing→Ring R) 0a 1a _+_ _·_ -_ _⋆_
    ·-comm    : (x y : A) → x · y ≡ y · x

  open IsAlgebra isAlgebra public

record CommAlgebra (R : CommRing {ℓ}) : Type (ℓ-suc ℓ) where

  constructor commalgebra

  field
    Carrier        : Type ℓ
    0a             : Carrier
    1a             : Carrier
    _+_            : Carrier → Carrier → Carrier
    _·_            : Carrier → Carrier → Carrier
    -_             : Carrier → Carrier
    _⋆_            : ⟨ R ⟩ → Carrier → Carrier
    isCommAlgebra  : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_

  open IsCommAlgebra isCommAlgebra public

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

  ⟨_⟩a : CommAlgebra R → Type ℓ
  ⟨_⟩a = CommAlgebra.Carrier

  CommAlgebra→Algebra : (A : CommAlgebra R) → Algebra (CommRing→Ring R)
  CommAlgebra→Algebra (commalgebra Carrier _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
    algebra Carrier _ _ _ _ _ _ isAlgebra

  CommAlgebra→CommRing : (A : CommAlgebra R) → CommRing {ℓ}
  CommAlgebra→CommRing (commalgebra Carrier _ _ _ _ _ _
                          (iscommalgebra isAlgebra ·-comm)) =
    _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)

  CommAlgebraEquiv : (R S : CommAlgebra R) → Type ℓ
  CommAlgebraEquiv R S = AlgebraEquiv (CommAlgebra→Algebra R) (CommAlgebra→Algebra S)

  makeIsCommAlgebra : {A : Type ℓ} {0a 1a : A}
                      {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
                      (isSet-A : isSet A)
                      (+-assoc :  (x y z : A) → x + (y + z) ≡ (x + y) + z)
                      (+-rid : (x : A) → x + 0a ≡ x)
                      (+-rinv : (x : A) → x + (- x) ≡ 0a)
                      (+-comm : (x y : A) → x + y ≡ y + x)
                      (·-assoc :  (x y z : A) → x · (y · z) ≡ (x · y) · z)
                      (·-lid : (x : A) → 1a · x ≡ x)
                      (·-ldist-+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
                      (·-comm : (x y : A) → x · y ≡ y · x)
                      (⋆-assoc : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                      (⋆-ldist : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                      (⋆-rdist : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                      (⋆-lid   : (x : A) → 1r ⋆ x ≡ x)
                      (⋆-lassoc : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
                    → IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_
  makeIsCommAlgebra {A} {0a} {1a} {_+_} {_·_} { -_} {_⋆_} isSet-A
                    +-assoc +-rid +-rinv +-comm
                    ·-assoc ·-lid ·-ldist-+ ·-comm
                    ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid ⋆-lassoc
   = iscommalgebra
     (makeIsAlgebra
       isSet-A
       +-assoc +-rid +-rinv +-comm
       ·-assoc
         (λ x → x · 1a ≡⟨ ·-comm _ _ ⟩ 1a · x ≡⟨ ·-lid _ ⟩ x ∎)
         ·-lid
         (λ x y z → x · (y + z)       ≡⟨ ·-comm _ _ ⟩
                    (y + z) · x       ≡⟨ ·-ldist-+ _ _ _ ⟩
                    (y · x) + (z · x) ≡⟨ cong (λ u → (y · x) + u) (·-comm _ _) ⟩
                    (y · x) + (x · z) ≡⟨ cong (λ u → u + (x · z)) (·-comm _ _) ⟩
                    (x · y) + (x · z) ∎)
         ·-ldist-+
       ⋆-assoc
         ⋆-ldist
         ⋆-rdist
         ⋆-lid
         ⋆-lassoc
         λ r x y → r ⋆ (x · y) ≡⟨ cong (λ u → r ⋆ u) (·-comm _ _) ⟩
                   r ⋆ (y · x) ≡⟨ sym (⋆-lassoc _ _ _) ⟩
                   (r ⋆ y) · x ≡⟨ ·-comm _ _ ⟩
                   x · (r ⋆ y) ∎)
     ·-comm

module CommAlgebraΣTheory (R : CommRing {ℓ}) where

  open AlgebraΣTheory (CommRing→Ring R)

  CommAlgebraAxioms : (A : Type ℓ) (s : RawAlgebraStructure A) → Type ℓ
  CommAlgebraAxioms A (_+_ , _·_ , 1a , _⋆_) = AlgebraAxioms A (_+_ , _·_ , 1a , _⋆_)
                                      × ((x y : A) → x · y ≡ y · x)

  CommAlgebraStructure : Type ℓ → Type ℓ
  CommAlgebraStructure = AxiomsStructure RawAlgebraStructure CommAlgebraAxioms

  CommAlgebraΣ : Type (ℓ-suc ℓ)
  CommAlgebraΣ = TypeWithStr ℓ CommAlgebraStructure

  CommAlgebraEquivStr : StrEquiv CommAlgebraStructure ℓ
  CommAlgebraEquivStr = AxiomsEquivStr RawAlgebraEquivStr CommAlgebraAxioms

  isPropCommAlgebraAxioms : (A : Type ℓ) (s : RawAlgebraStructure A)
                       → isProp (CommAlgebraAxioms A s)
  isPropCommAlgebraAxioms A (_+_ , _·_ , 1a , _⋆_) =
    isPropΣ (isPropAlgebraAxioms A (_+_ , _·_ , 1a , _⋆_))
           λ isAlgebra → isPropΠ2 λ _ _ → (isSetAlgebraΣ (A , _ , isAlgebra)) _ _

  CommAlgebra→CommAlgebraΣ : CommAlgebra R → CommAlgebraΣ
  CommAlgebra→CommAlgebraΣ (commalgebra _ _ _ _ _ _ _ (iscommalgebra G C)) =
    _ , _ , Algebra→AlgebraΣ (algebra _ _ _ _ _ _ _ G) .snd .snd , C

  CommAlgebraΣ→CommAlgebra : CommAlgebraΣ → CommAlgebra R
  CommAlgebraΣ→CommAlgebra (_ , _ , G , C) =
    commalgebra _ _ _ _ _ _ _ (iscommalgebra (AlgebraΣ→Algebra (_ , _ , G) .Algebra.isAlgebra) C)

  CommAlgebraIsoCommAlgebraΣ : Iso (CommAlgebra R) CommAlgebraΣ
  CommAlgebraIsoCommAlgebraΣ =
    iso CommAlgebra→CommAlgebraΣ CommAlgebraΣ→CommAlgebra (λ _ → refl) (λ _ → refl)

  commAlgebraUnivalentStr : UnivalentStr CommAlgebraStructure CommAlgebraEquivStr
  commAlgebraUnivalentStr = axiomsUnivalentStr _ isPropCommAlgebraAxioms rawAlgebraUnivalentStr

  CommAlgebraΣPath : (A B : CommAlgebraΣ) → (A ≃[ CommAlgebraEquivStr ] B) ≃ (A ≡ B)
  CommAlgebraΣPath = SIP commAlgebraUnivalentStr

  CommAlgebraEquivΣ : (A B : CommAlgebra R) → Type ℓ
  CommAlgebraEquivΣ A B = CommAlgebra→CommAlgebraΣ A ≃[ CommAlgebraEquivStr ] CommAlgebra→CommAlgebraΣ B

  CommAlgebraPath : (A B : CommAlgebra R) → (CommAlgebraEquiv A B) ≃ (A ≡ B)
  CommAlgebraPath A B =
    CommAlgebraEquiv A B   ≃⟨ strictIsoToEquiv AlgebraEquivΣPath ⟩
    CommAlgebraEquivΣ A B  ≃⟨ CommAlgebraΣPath _ _ ⟩
    CommAlgebra→CommAlgebraΣ A ≡ CommAlgebra→CommAlgebraΣ B
      ≃⟨ isoToEquiv (invIso (congIso CommAlgebraIsoCommAlgebraΣ)) ⟩
    A ≡ B ■

CommAlgebraPath : (R : CommRing {ℓ}) → (A B : CommAlgebra R) → (CommAlgebraEquiv A B) ≃ (A ≡ B)
CommAlgebraPath = CommAlgebraΣTheory.CommAlgebraPath

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


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

module Data.Binary.Relations where

open import Data.Binary.Relations.Raw
open import Data.Binary.Definitions
open import Data.Binary.Operations.Addition
open import Relation.Binary
open import Relation.Nullary
import Data.Empty.Irrelevant as Irrel

infix 4 _≤_ _<_
record _≤_ (x y : 𝔹) : Set where
  constructor ≤!
  field
    .proof : ⟅ I ⟆ x ≺ y

record _<_ (x y : 𝔹) : Set where
  constructor <!
  field
    .proof : ⟅ O ⟆ x ≺ y

_≤?_ : Decidable _≤_
x ≤? y with I ! x ≺? y
(x ≤? y) | yes x₁ = yes (≤! x₁)
(x ≤? y) | no x₁ = no λ p → Irrel.⊥-elim (x₁ (_≤_.proof p))

_<?_ : Decidable _<_
x <? y with O ! x ≺? y
(x <? y) | yes x₁ = yes (<! x₁)
(x <? y) | no x₁ = no λ p → Irrel.⊥-elim (x₁ (_<_.proof p))

<⇒≤ : ∀ {x y} → x < y → x ≤ y
<⇒≤ {x} {y} x<y = ≤! (weaken x y (_<_.proof x<y))

≤-trans : Transitive _≤_
≤-trans {i} {j} {k} i≤j j≤k = ≤! (≺-trans I I i j k (_≤_.proof i≤j) (_≤_.proof j≤k))

<-trans : Transitive _<_
<-trans {i} {j} {k} i<j j<k = <! (≺-trans O O i j k (_<_.proof i<j) (_<_.proof j<k))

n≤m+n : ∀ x y → x ≤ y + x
n≤m+n x y = ≤! (≺-add y x)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module Test where

open import Agda.Builtin.Bool
  using (Bool; false; true)
open import Agda.Builtin.Unit

_∧_
  : Bool
  → Bool
  → Bool
false ∧ x
  = false
_ ∧ y
  = y

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
------------------------------------------------------------------------------
-- The gcd program is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the gcd program using
-- the Euclid's algorithm.

-- N.B This module does not contain combined proofs, but it imports
-- modules which contain combined proofs.

module FOTC.Program.GCD.Total.CorrectnessProofATP where

open import FOTC.Base
open import FOTC.Data.Nat.Type
open import FOTC.Program.GCD.Total.CommonDivisorATP using ( gcdCD )
open import FOTC.Program.GCD.Total.Definitions using ( gcdSpec )
open import FOTC.Program.GCD.Total.DivisibleATP using ( gcdDivisible )
open import FOTC.Program.GCD.Total.GCD using ( gcd )

------------------------------------------------------------------------------
-- The gcd is correct.
postulate gcdCorrect : ∀ {m n} → N m → N n → gcdSpec m n (gcd m n)
{-# ATP prove gcdCorrect gcdCD gcdDivisible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Base

module Spaces.Circle where

{-
Idea :

data S¹ : Set where
  base : S¹
  loop : base ≡ base

I’m using Dan Licata’s trick to have a higher inductive type with definitional
reduction rule for [base]
-}

private
  data #S¹ : Set where
    #base : #S¹

S¹ : Set
S¹ = #S¹

base : S¹
base = #base

postulate  -- HIT
  loop : base ≡ base

S¹-rec : ∀ {i} (P : S¹ → Set i) (x : P base) (p : transport P loop x ≡ x)
  → ((t : S¹) → P t)
S¹-rec P x p #base = x

postulate  -- HIT
  S¹-β-loop : ∀ {i} (P : S¹ → Set i) (x : P base) (p : transport P loop x ≡ x)
      → apd (S¹-rec P x p) loop ≡ p

S¹-rec-nondep : ∀ {i} (A : Set i) (x : A) (p : x ≡ x) → (S¹ → A)
S¹-rec-nondep A x p #base = x

postulate  -- HIT
  S¹-β-loop-nondep : ∀ {i} (A : Set i) (x : A) (p : x ≡ x)
    → ap (S¹-rec-nondep A x p) loop ≡ p

-- S¹-rec-nondep : ∀ {i} (A : Set i) (x : A) (p : x ≡ x) → (S¹ → A)
-- S¹-rec-nondep A x p = S¹-rec (λ _ → A) x (trans-cst loop x ∘ p)

-- β-nondep : ∀ {i} (A : Set i) (x : A) (p : x ≡ x)
--   → ap (S¹-rec-nondep A x p) loop ≡ p
-- β-nondep A x p =
--   apd-trivial (S¹-rec-nondep A x p) loop ∘
--   (whisker-left (! (trans-cst loop _)) (β (λ _ → A) x (trans-cst loop _ ∘ p))
--   ∘ (! (concat-assoc (! (trans-cst loop _)) (trans-cst loop _) p)
--   ∘ whisker-right p (opposite-left-inverse (trans-cst loop _))))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical #-}
module _ where

open import Agda.Builtin.Equality

uip : ∀ {a} {A : Set a} {x y : A} (p q : x ≡ y) → p ≡ q
uip refl refl = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

-- 2015-02-17 Jesper and Andreas

postulate
  A : Set
  R : A → A → Set
  f : A → A
  g : A → A
  r : R (f _) (g _)

{-# BUILTIN REWRITE R #-}
{-# REWRITE r #-}


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

module Type.Cubical.Univalence where

open import Function.Axioms
open import Functional
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Structure.Function.Domain using (intro ; Inverseₗ ; Inverseᵣ)
open import Structure.Relator.Properties
open import Structure.Type.Identity
open import Type.Cubical.Path.Equality
open import Type.Cubical.Equiv
open import Type.Cubical
open import Type.Properties.MereProposition
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T A B P Q : Type{ℓ}

-- TODO: Move
primitive primGlue : (A : Type{ℓ₁}) → ∀{i : Interval} → (T : Interval.Partial i (Type{ℓ₂})) → (e : Interval.PartialP i (\o → T(o) ≍ A)) → Type{ℓ₂}

type-extensionalityₗ : (A ≡ B) ← (A ≍ B)
type-extensionalityₗ {A = A}{B = B} ab i = primGlue(B)
  (\{(i = Interval.𝟎) → A  ; (i = Interval.𝟏) → B})
  (\{(i = Interval.𝟎) → ab ; (i = Interval.𝟏) → reflexivity(_≍_)})

module _ ⦃ prop-P : MereProposition{ℓ}(P) ⦄ ⦃ prop-Q : MereProposition{ℓ}(Q) ⦄ where
  propositional-extensionalityₗ : (P ≡ Q) ← (P ↔ Q)
  propositional-extensionalityₗ pq = type-extensionalityₗ([∃]-intro pq ⦃ intro ⦄) where
    instance
      l : Inverseₗ([↔]-to-[←] pq)([↔]-to-[→] pq)
      Inverseᵣ.proof l = uniqueness(Q)

    instance
      r : Inverseᵣ([↔]-to-[←] pq)([↔]-to-[→] pq)
      Inverseᵣ.proof r = uniqueness(P)

module _ {P Q : T → Type} ⦃ prop-P : ∀{x} → MereProposition{ℓ}(P(x)) ⦄ ⦃ prop-Q : ∀{x} → MereProposition{ℓ}(Q(x)) ⦄ where
  prop-set-extensionalityₗ : (P ≡ Q) ← (∀{x} → P(x) ↔ Q(x))
  prop-set-extensionalityₗ pq = functionExtensionalityOn P Q (propositional-extensionalityₗ pq)

-- module _ ⦃ uip-P : UniqueIdentityProofs{ℓ}(P) ⦄ ⦃ uip-Q : UniqueIdentityProofs{ℓ}(Q) ⦄ where

-- TODO: Actual proof of univalence

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K #-}
module container.m.from-nat where

open import container.m.from-nat.core public
open import container.m.from-nat.cone public
open import container.m.from-nat.coalgebra public
open import container.m.from-nat.bisimulation public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------------
-- Testing the translation of the logical constants
------------------------------------------------------------------------------

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

module LogicalConstants where

infix  5 ¬_
infixr 4 _∧_
infixr 3 _∨_
infixr 2 _⇒_
infixr 1 _↔_ _⇔_

------------------------------------------------------------------------------
-- Propositional logic

-- The logical constants

-- The logical constants are hard-coded in our implementation,
-- i.e. the following symbols must be used (it is possible to use Agda
-- non-dependent function space → instead of ⇒).
postulate
  ⊥ ⊤         : Set -- N.B. the name of the tautology symbol is "\top" not T.
  ¬_          : Set → Set -- N.B. the right hole.
  _∧_ _∨_     : Set → Set → Set
  _⇒_ _↔_ _⇔_ : Set → Set → Set

-- We postulate some formulae (which are translated as 0-ary
-- predicates).
postulate A B C : Set

-- Testing the conditional using the non-dependent function type.
postulate A→A : A → A
{-# ATP prove A→A #-}

-- Testing the conditional using the hard-coded function type.
postulate A⇒A : A ⇒ A
{-# ATP prove A⇒A #-}

-- The introduction and elimination rules for the propositional
-- connectives are theorems.
postulate
  →I  : (A → B) → A ⇒ B
  →E  : (A ⇒ B) → A → B
  ∧I  : A → B → A ∧ B
  ∧E₁ : A ∧ B → A
  ∧E₂ : A ∧ B → B
  ∨I₁ : A → A ∨ B
  ∨I₂ : B → A ∨ B
  ∨E  : (A ⇒ C) → (B ⇒ C) → A ∨ B → C
  ⊥E  : ⊥ → A
  ¬E : (¬ A → ⊥) → A
{-# ATP prove →I #-}
{-# ATP prove →E #-}
{-# ATP prove ∧I #-}
{-# ATP prove ∧E₁ #-}
{-# ATP prove ∧E₂ #-}
{-# ATP prove ∨I₁ #-}
{-# ATP prove ∨I₂ #-}
{-# ATP prove ∨E #-}
{-# ATP prove ⊥E #-}
{-# ATP prove ¬E #-}

-- Testing other logical constants.
postulate
  thm₁ : A ∧ ⊤ → A
  thm₂ : A ∨ ⊥ → A
  thm₃ : A ↔ A
  thm₄ : A ⇔ A
{-# ATP prove thm₁ #-}
{-# ATP prove thm₂ #-}
{-# ATP prove thm₃ #-}
{-# ATP prove thm₄ #-}

------------------------------------------------------------------------------
-- Predicate logic

--- The universe of discourse.
postulate D : Set

-- The propositional equality is hard-coded in our implementation, i.e. the
-- following symbol must be used.
postulate _≡_ : D → D → Set

-- Testing propositional equality.
postulate refl : ∀ {x} → x ≡ x
{-# ATP prove refl #-}

-- The quantifiers are hard-coded in our implementation, i.e. the
-- following symbols must be used (it is possible to use Agda
-- dependent function space ∀ x → A instead of ⋀).
postulate
  ∃ : (A : D → Set) → Set
  ⋀ : (A : D → Set) → Set

-- We postulate some formulae and propositional functions.
postulate
  A¹ B¹ : D → Set
  A²    : D → D → Set

-- The introduction and elimination rules for the quantifiers are
-- theorems.
postulate
  ∀I₁ : ((x : D) → A¹ x) → ⋀ A¹
  ∀I₂ : ((x : D) → A¹ x) → ∀ x → A¹ x
  ∀E₁ : (t : D) → ⋀ A¹ → A¹ t
  ∀E₂ : (t : D) → (∀ x → A¹ x) → A¹ t
{-# ATP prove ∀I₁ #-}
{-# ATP prove ∀I₂ #-}
{-# ATP prove ∀E₁ #-}
{-# ATP prove ∀E₂ #-}

postulate ∃I : (t : D) → A¹ t → ∃ A¹
{-# ATP prove ∃I #-}

postulate ∃E : ∃ A¹ → ((x : D) → A¹ x → A) → A
{-# ATP prove ∃E #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Tarski-style semantics with contexts as concrete worlds, and glueing for α, ▻, and □.
-- Implicit syntax.

module BasicIS4.Semantics.TarskiOvergluedImplicit where

open import BasicIS4.Syntax.Common public
open import Common.Semantics public

-- Intuitionistic Tarski models.

record Model : Set₁ where
  infix 3 _⊩ᵅ_
  field
    -- Forcing for atomic propositions; monotonic.
    _⊩ᵅ_   : Cx Ty → Atom → Set
    mono⊩ᵅ : ∀ {P Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ᵅ P → Γ′ ⊩ᵅ P

open Model {{…}} public

module ImplicitSyntax
    (_[⊢]_   : Cx Ty → Ty → Set)
    (mono[⊢] : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ [⊢] A → Γ′ [⊢] A)
  where

  -- Forcing in a particular model.

  module _ {{_ : Model}} where
    infix 3 _⊩_
    _⊩_ : Cx Ty → Ty → Set
    Γ ⊩ α P   = Glue (Γ [⊢] (α P)) (Γ ⊩ᵅ P)
    Γ ⊩ A ▻ B = ∀ {Γ′} → Γ ⊆ Γ′ → Glue (Γ′ [⊢] (A ▻ B)) (Γ′ ⊩ A → Γ′ ⊩ B)
    Γ ⊩ □ A   = ∀ {Γ′} → Γ ⊆ Γ′ → Glue (Γ′ [⊢] (□ A)) (Γ′ ⊩ A)
    Γ ⊩ A ∧ B = Γ ⊩ A × Γ ⊩ B
    Γ ⊩ ⊤    = 𝟙

    infix 3 _⊩⋆_
    _⊩⋆_ : Cx Ty → Cx Ty → Set
    Γ ⊩⋆ ∅     = 𝟙
    Γ ⊩⋆ Ξ , A = Γ ⊩⋆ Ξ × Γ ⊩ A

  -- Monotonicity with respect to context inclusion.

  module _ {{_ : Model}} where
    mono⊩ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩ A → Γ′ ⊩ A
    mono⊩ {α P}   η s = mono[⊢] η (syn s) ⅋ mono⊩ᵅ η (sem s)
    mono⊩ {A ▻ B} η s = λ η′ → s (trans⊆ η η′)
    mono⊩ {□ A}   η s = λ η′ → s (trans⊆ η η′)
    mono⊩ {A ∧ B} η s = mono⊩ {A} η (π₁ s) , mono⊩ {B} η (π₂ s)
    mono⊩ {⊤}    η s = ∙

    mono⊩⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊩⋆ Ξ → Γ′ ⊩⋆ Ξ
    mono⊩⋆ {∅}     η ∙        = ∙
    mono⊩⋆ {Ξ , A} η (ts , t) = mono⊩⋆ {Ξ} η ts , mono⊩ {A} η t

  -- Additional useful equipment.

  module _ {{_ : Model}} where
    _⟪$⟫_ : ∀ {A B Γ} → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ B
    s ⟪$⟫ a = sem (s refl⊆) a

    ⟪S⟫ : ∀ {A B C Γ} → Γ ⊩ A ▻ B ▻ C → Γ ⊩ A ▻ B → Γ ⊩ A → Γ ⊩ C
    ⟪S⟫ s₁ s₂ a = (s₁ ⟪$⟫ a) ⟪$⟫ (s₂ ⟪$⟫ a)

    ⟪↓⟫ : ∀ {A Γ} → Γ ⊩ □ A → Γ ⊩ A
    ⟪↓⟫ s = sem (s refl⊆)

  -- Forcing in a particular world of a particular model, for sequents.

  module _ {{_ : Model}} where
    infix 3 _⊩_⇒_
    _⊩_⇒_ : Cx Ty → Cx Ty → Ty → Set
    w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

    infix 3 _⊩_⇒⋆_
    _⊩_⇒⋆_ : Cx Ty → Cx Ty → Cx Ty → Set
    w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

  -- Entailment, or forcing in all worlds of all models, for sequents.

  infix 3 _⊨_
  _⊨_ : Cx Ty → Ty → Set₁
  Γ ⊨ A = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒ A

  infix 3 _⊨⋆_
  _⊨⋆_ : Cx Ty → Cx Ty → Set₁
  Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : Cx Ty} → w ⊩ Γ ⇒⋆ Ξ

  -- Additional useful equipment, for sequents.

  module _ {{_ : Model}} where
    lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
    lookup top     (γ , a) = a
    lookup (pop i) (γ , b) = lookup i γ

    _⟦$⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B
    (s₁ ⟦$⟧ s₂) γ = s₁ γ ⟪$⟫ s₂ γ

    ⟦S⟧ : ∀ {A B C Γ w} → w ⊩ Γ ⇒ A ▻ B ▻ C → w ⊩ Γ ⇒ A ▻ B → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ C
    ⟦S⟧ s₁ s₂ a γ = ⟪S⟫ (s₁ γ) (s₂ γ) (a γ)

    ⟦↓⟧ : ∀ {A Γ w} → w ⊩ Γ ⇒ □ A → w ⊩ Γ ⇒ A
    ⟦↓⟧ s γ = ⟪↓⟫ (s γ)

    _⟦,⟧_ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A → w ⊩ Γ ⇒ B → w ⊩ Γ ⇒ A ∧ B
    (a ⟦,⟧ b) γ = a γ , b γ

    ⟦π₁⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ A
    ⟦π₁⟧ s γ = π₁ (s γ)

    ⟦π₂⟧ : ∀ {A B Γ w} → w ⊩ Γ ⇒ A ∧ B → w ⊩ Γ ⇒ B
    ⟦π₂⟧ s γ = π₂ (s γ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module lib-safe where

open import datatypes-safe public
open import logic public
open import thms public
open import termination public
open import error public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------------
-- Conversion rules for the Collatz function
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Collatz.ConversionRulesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOT.FOTC.Program.Collatz.CollatzConditionals

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Program.Collatz.Data.Nat

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

private
  -- The steps

  -- Initially, the equation collatz-eq is used.

  collatz-s₁ : D → D
  collatz-s₁ n = if (iszero₁ n)
                   then 1'
                   else (if (iszero₁ (pred₁ n))
                           then 1'
                           else (if (even n)
                                   then collatz (div n 2')
                                   else collatz (3' * n + 1')))

  -- First if_then_else_ iszero₁ n = b.
  collatz-s₂ : D → D → D
  collatz-s₂ n b = if b
                     then 1'
                     else (if (iszero₁ (pred₁ n))
                             then 1'
                             else (if (even n)
                                     then collatz (div n 2')
                                     else collatz (3' * n + 1')))

  -- First if_then_else_ when if true ....
  collatz-s₃ : D → D
  collatz-s₃ n = 1'

  -- First if_then_else_ when if false ....
  collatz-s₄ : D → D
  collatz-s₄ n = if (iszero₁ (pred₁ n))
                   then 1'
                   else (if (even n)
                           then collatz (div n 2')
                           else collatz (3' * n + 1'))

  -- Second if_then_else_ iszero₁ (pred₁ n) = b.
  collatz-s₅ : D → D → D
  collatz-s₅ n b = if b
                     then 1'
                     else (if (even n)
                             then collatz (div n 2')
                             else collatz (3' * n + 1'))

  -- Second if_then_else_ when if true ....
  collatz-s₆ : D → D
  collatz-s₆ n = 1'

  -- Second if_then_else_ when if false ....
  collatz-s₇ : D → D
  collatz-s₇ n = if (even n) then collatz (div n 2') else collatz (3' * n + 1')

  -- Third if_then_else_ even n b.
  collatz-s₈ : D → D → D
  collatz-s₈ n b = if b then collatz (div n 2') else collatz (3' * n + 1')

  -- Third if_then_else_ when if true ....
  collatz-s₉ : D → D
  collatz-s₉ n = collatz (div n 2')

  -- Third if_then_else_ when if false ....
  collatz-s₁₀ : D → D
  collatz-s₁₀ n = collatz (3' * n + 1')

  ----------------------------------------------------------------------------
  -- The execution steps

  proof₀₋₁ : ∀ n → collatz n ≡ collatz-s₁ n
  proof₀₋₁ n = collatz-eq n

  proof₁₋₂ : ∀ {n b} → iszero₁ n ≡ b → collatz-s₁ n ≡ collatz-s₂ n b
  proof₁₋₂ {n} {b} h = subst (λ x → collatz-s₂ n x ≡ collatz-s₂ n b)
                             (sym h)
                             refl

  proof₂₋₃ : ∀ n → collatz-s₂ n true ≡ collatz-s₃ n
  proof₂₋₃ n = if-true (collatz-s₃ n)

  proof₂₋₄ : ∀ n → collatz-s₂ n false ≡ collatz-s₄ n
  proof₂₋₄ n = if-false (collatz-s₄ n)

  proof₄₋₅ : ∀ {n b} → iszero₁ (pred₁ n) ≡ b → collatz-s₄ n ≡ collatz-s₅ n b
  proof₄₋₅ {n} {b} h = subst (λ x → collatz-s₅ n x ≡ collatz-s₅ n b)
                             (sym h)
                             refl

  proof₅₋₆ : ∀ n → collatz-s₅ n true ≡ collatz-s₆ n
  proof₅₋₆ n = if-true (collatz-s₆ n)

  proof₅₋₇ : ∀ n → collatz-s₅ n false ≡ collatz-s₇ n
  proof₅₋₇ n = if-false (collatz-s₇ n)

  proof₇₋₈ : ∀ {n b} → even n ≡ b → collatz-s₇ n ≡ collatz-s₈ n b
  proof₇₋₈ {n} {b} h = subst (λ x → collatz-s₈ n x ≡ collatz-s₈ n b)
                             (sym h)
                             refl

  proof₈₋₉ : ∀ n → collatz-s₈ n true ≡ collatz-s₉ n
  proof₈₋₉ n = if-true (collatz-s₉ n)

  proof₈₋₁₀ : ∀ n → collatz-s₈ n false ≡ collatz-s₁₀ n
  proof₈₋₁₀ n = if-false (collatz-s₁₀ n)

------------------------------------------------------------------------------
-- Conversion rules for the Collatz function

collatz-0 : collatz zero ≡ 1'
collatz-0 =
  collatz    zero      ≡⟨ proof₀₋₁ zero ⟩
  collatz-s₁ zero      ≡⟨ proof₁₋₂ iszero-0 ⟩
  collatz-s₂ zero true ≡⟨ proof₂₋₃ zero ⟩
  1'                  ∎

collatz-1 : collatz 1' ≡ 1'
collatz-1 =
  collatz 1'
    ≡⟨ proof₀₋₁ 1' ⟩
  collatz-s₁ 1'
    ≡⟨ proof₁₋₂ (iszero-S zero) ⟩
  collatz-s₂ 1' false
    ≡⟨ proof₂₋₄ 1'  ⟩
  collatz-s₄ 1'
    ≡⟨ proof₄₋₅ (subst (λ x → iszero₁ x ≡ true) (sym (pred-S zero)) iszero-0) ⟩
  collatz-s₅ 1' true
    ≡⟨ proof₅₋₆ 1' ⟩
  1' ∎

collatz-even : ∀ {n} → Even (succ₁ (succ₁ n)) →
               collatz (succ₁ (succ₁ n)) ≡ collatz (div (succ₁ (succ₁ n)) 2')
collatz-even {n} h =
  collatz (succ₁ (succ₁ n))
    ≡⟨ proof₀₋₁ (succ₁ (succ₁ n)) ⟩
  collatz-s₁ (succ₁ (succ₁ n))
    ≡⟨ proof₁₋₂ (iszero-S (succ₁ n)) ⟩
  collatz-s₂ (succ₁ (succ₁ n)) false
    ≡⟨ proof₂₋₄ (succ₁ (succ₁ n)) ⟩
  collatz-s₄ (succ₁ (succ₁ n))
    ≡⟨ proof₄₋₅ (subst (λ x → iszero₁ x ≡ false)
                       (sym (pred-S (succ₁ n)))
                       (iszero-S n))
    ⟩
  collatz-s₅ (succ₁ (succ₁ n)) false
    ≡⟨ proof₅₋₇ (succ₁ (succ₁ n)) ⟩
  collatz-s₇ (succ₁ (succ₁ n))
    ≡⟨ proof₇₋₈ h ⟩
  collatz-s₈ (succ₁ (succ₁ n)) true
    ≡⟨ proof₈₋₉ (succ₁ (succ₁ n)) ⟩
  collatz (div (succ₁ (succ₁ n)) 2') ∎

collatz-noteven : ∀ {n} → NotEven (succ₁ (succ₁ n)) →
                  collatz (succ₁ (succ₁ n)) ≡
                  collatz (3' * (succ₁ (succ₁ n)) + 1')
collatz-noteven {n} h =
  collatz (succ₁ (succ₁ n))
    ≡⟨ proof₀₋₁ (succ₁ (succ₁ n)) ⟩
  collatz-s₁ (succ₁ (succ₁ n))
    ≡⟨ proof₁₋₂ (iszero-S (succ₁ n)) ⟩
  collatz-s₂ (succ₁ (succ₁ n)) false
    ≡⟨ proof₂₋₄ (succ₁ (succ₁ n)) ⟩
  collatz-s₄ (succ₁ (succ₁ n))
    ≡⟨ proof₄₋₅ (subst (λ x → iszero₁ x ≡ false)
                       (sym (pred-S (succ₁ n)))
                       (iszero-S n))
    ⟩
  collatz-s₅ (succ₁ (succ₁ n)) false
    ≡⟨ proof₅₋₇ (succ₁ (succ₁ n)) ⟩
  collatz-s₇ (succ₁ (succ₁ n))
    ≡⟨ proof₇₋₈ h ⟩
  collatz-s₈ (succ₁ (succ₁ n)) false
    ≡⟨ proof₈₋₁₀ (succ₁ (succ₁ n)) ⟩
  collatz (3' * (succ₁ (succ₁ n)) + 1') ∎


text:
-- An ATP-pragma must appear in the same module where its argument is
-- defined.

-- This error is detected by TypeChecking.Monad.Signature.

module ATPImports where

open import Imports.ATP-A

{-# ATP axiom p #-}

postulate foo : a ≡ b
{-# ATP prove foo #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

open import HoTT
import homotopy.ConstantToSetExtendsToProp as ConstExt
open import homotopy.Pigeonhole

module homotopy.FinSet where

-- the explicit type of finite sets, carrying the cardinality on its sleeve
FinSet-exp : Type₁
FinSet-exp = Σ ℕ λ n → BAut (Fin n)

FinSet-prop : SubtypeProp Type₀ (lsucc lzero)
FinSet-prop = (λ A → Trunc -1 (Σ ℕ λ n → Fin n == A)) , λ A → Trunc-level

-- the implicit type of finite sets, hiding the cardinality in prop. trunc.
FinSet : Type₁
FinSet = Subtype FinSet-prop

FinSet= : {A B : FinSet} → fst A == fst B → A == B
FinSet= = Subtype=-out FinSet-prop

FinFS : ℕ → FinSet
FinFS n = Fin n , [ n , idp ]

UnitFS : FinSet
UnitFS = ⊤ , [ S O , ua Fin-equiv-Coprod ∙ ap (λ C → C ⊔ ⊤) (ua Fin-equiv-Empty)
                     ∙ ua (Coprod-unit-l ⊤) ]

Fin-inj-lemma : {n m : ℕ} → n < m → Fin m == Fin n → ⊥
Fin-inj-lemma {n} {m} n<m p = i≠j (<– (ap-equiv (coe-equiv p) i j) q)
  where
    i : Fin m
    i = fst (pigeonhole n<m (coe p))

    j : Fin m
    j = fst (snd (pigeonhole n<m (coe p)))

    i≠j : i ≠ j
    i≠j = fst (snd (snd (pigeonhole n<m (coe p))))

    q : coe p i == coe p j
    q = snd (snd (snd (pigeonhole n<m (coe p))))

Fin-inj : (n m : ℕ) → Fin n == Fin m → n == m
Fin-inj n m p with ℕ-trichotomy n m
Fin-inj n m p | inl q = q
Fin-inj n m p | inr (inl q) = ⊥-rec (Fin-inj-lemma q (! p))
Fin-inj n m p | inr (inr q) = ⊥-rec (Fin-inj-lemma q p)

FinSet-aux-prop : (A : Type₀) → SubtypeProp ℕ (lsucc lzero)
FinSet-aux-prop A = (λ n → Trunc -1 (Fin n == A)) , (λ n → Trunc-level)

FinSet-aux : (A : FinSet) → Subtype (FinSet-aux-prop (fst A))
FinSet-aux (A , tz) = CE.ext tz
  where
    to : (Σ ℕ λ n → Fin n == A) → Subtype (FinSet-aux-prop A)
    to (n , p) = n , [ p ]

    to-const : (z₁ z₂ : Σ ℕ λ n → Fin n == A) → to z₁ == to z₂
    to-const (n₁ , p₁) (n₂ , p₂) = Subtype=-out (FinSet-aux-prop A) (Fin-inj n₁ n₂ (p₁ ∙ ! p₂))

    module CE =
      ConstExt ⦃ Subtype-level (FinSet-aux-prop A) ⦄ to to-const

card : FinSet → ℕ
card A = fst (FinSet-aux A)

card-conv : (A : FinSet) (n : ℕ) → Trunc -1 (Fin n == fst A) → card A == n
card-conv (A , tz) n = Trunc-rec λ p → ap card (FinSet= {A , tz} {FinFS n} (! p))

FinSet-econv : FinSet-exp ≃ FinSet
FinSet-econv = equiv to from to-from from-to
  where
    to : FinSet-exp → FinSet
    to (n , A , tp) = A , Trunc-rec (λ p → [ n , p ]) tp

    from : FinSet → FinSet-exp
    from A = card A , fst A , snd (FinSet-aux A)

    to-from : (A : FinSet) → to (from A) == A
    to-from A = pair= idp (prop-has-all-paths (snd (to (from A))) (snd A))

    from-to : (A : FinSet-exp) → from (to A) == A
    from-to A = pair= (card-conv (to A) (fst A) (snd (snd A)))
      (↓-Subtype-in (λ n → BAut-prop (Fin n)) (↓-cst-in idp))

FinSet-elim-prop : ∀ {j} {P : FinSet → Type j} (p : (A : FinSet) → has-level -1 (P A))
                   (d : (n : ℕ) → P (FinFS n)) → (A : FinSet) → P A
FinSet-elim-prop {j} {P} p d (A , tz) = Trunc-elim ⦃ λ tw → p (A , tw) ⦄
  (λ {(n , p) → transport P (FinSet= p) (d n)}) tz

finset-has-dec-eq : (A : FinSet) → has-dec-eq (fst A)
finset-has-dec-eq = FinSet-elim-prop (λ A → has-dec-eq-is-prop) λ n → Fin-has-dec-eq

-- todo: closure of FinSet under product, coproduct, exponential, etc.

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --sized-types #-}
module SList (A : Set) where

open import Data.List
open import Data.Product
open import Size

data SList : {ι : Size} → Set where
  snil : {ι : Size}
                   → SList {↑ ι}
  _∙_ : {ι : Size}(x : A)
                   → SList {ι}
                   → SList {↑ ι}

size : List A → SList
size [] = snil
size (x ∷ xs) = x ∙ (size xs)

unsize : {ι : Size} → SList {ι} → List A
unsize snil = []
unsize (x ∙ xs) = x ∷ unsize xs

unsize× : {ι : Size} → SList {ι} × SList {ι} → List A × List A
unsize× (xs , ys) = unsize xs , unsize ys

_⊕_ : SList → SList → SList
snil ⊕ ys = ys
(x ∙ xs) ⊕ ys = x ∙ (xs ⊕ ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.NProd where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Instances.NProd
open import Cubical.Algebra.AbGroup

private variable
  ℓ : Level

open AbGroupStr

NProd-AbGroup : (G : (n : ℕ) → Type ℓ) → (Gstr : (n : ℕ) → AbGroupStr (G n)) → AbGroup ℓ
NProd-AbGroup G Gstr = Group→AbGroup (NProd-Group G (λ n → AbGroupStr→GroupStr (Gstr n)))
                                      λ f g → funExt λ n → +Comm (Gstr n) _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Data.Maybe where

data Maybe (a : Set) : Set where
  nothing : Maybe a
  just	  : a -> Maybe a

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

module Issue1719.Common where

ofType : ∀ {i} (A : Set i) → A → A
ofType A x = x

syntax ofType A x = x :> A

infixr 3 ofType

postulate
  _↦_ : ∀ {i} {A : Set i} → A → A → Set i
  idr : ∀ {i} {A : Set i} {a : A} → a ↦ a
{-# BUILTIN REWRITE _↦_ #-}

infixr 3 _==_

data _==_ {i} {A : Set i} (a : A) : A → Set i where
  idp : a == a

HetEq : ∀ {i} {A B : Set i} (e : A == B) (a : A) (b : B) → Set i
HetEq idp a b = (a == b)

PathOver : ∀ {i j} {A : Set i} (B : A → Set j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set j
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

postulate
  PathOver-rewr : ∀ {i j} {A : Set i} {B : Set j} {x y : A} (p : x == y) (u v : B) →
    (PathOver (λ _ → B) p u v) ↦ (u == v)
  {-# REWRITE PathOver-rewr #-}

-- Note that this is both [ap] and [apd], as a [PathOver] in a constant family
-- reduces to the usual identity type.
ap : ∀ {i j} {A : Set i} {B : A → Set j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → PathOver B p (f x) (f y)
ap f idp = idp

postulate
  ap-cst : ∀ {i j} {A : Set i} {B : Set j} (b : B) {x y : A} (p : x == y) →
    ap (λ _ → b) p ↦ idp
  {-# REWRITE ap-cst #-}


text:
module A where

import B
import C

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence where

open import Util.HoTT.Univalence.Axiom public
open import Util.HoTT.Univalence.Beta public
open import Util.HoTT.Univalence.ContrFormulation public using
  ( UnivalenceContr ; UnivalenceProp ; univalenceContr ; univalenceProp )
open import Util.HoTT.Univalence.Statement public

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module plfa.part1.Induction where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = cong suc (+-assoc m n p)

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-commu : ∀ (m n : ℕ) → m + n ≡ n + m
+-commu zero zero = refl
+-commu zero (suc n) = cong suc (+-commu zero n)
+-commu (suc m) zero = cong suc (+-commu m zero)
+-commu (suc m) (suc n)
  rewrite +-suc m n
  rewrite +-suc n m = cong suc (cong suc (+-commu m n))

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ m rewrite +-commu m zero = refl

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p rewrite +-commu m (n + p)
             rewrite +-assoc n p m
             rewrite +-commu p m = refl

*-assoc : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-assoc zero n p = refl
*-assoc (suc m) n p
  rewrite +-commu (suc m) n
  rewrite +-assoc p (m * p) (n * p) = cong (λ n → p + n) (*-assoc m n p)

max_stars_repo_name: UnsoundWitch/proofs

max_issues_repo_name: sym-cereal/proofs

max_forks_repo_name: sym-cereal/proofs


text:
------------------------------------------------------------------------
-- Specifications of output-restricted deques (single-ended queues
-- with cons)
------------------------------------------------------------------------

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

open import Equality

module Queue {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Bijection eq as Bijection using (_↔_)
import Equivalence eq as Eq
open import Function-universe eq as F hiding (id; _∘_)
open import List eq as L hiding (map)
open import Maybe eq
open import Surjection eq using (_↠_)

private
  variable
    a ℓ ℓ₁ ℓ₂ : Level
    A B       : Type a
    P Q       : ∀ {ℓ} → Type ℓ → Type ℓ
    p q x     : A
    f         : A → B
    xs        : List A

-- A specification of when (and how) a type constructor implements
-- output-restricted deques.

record Is-queue
         -- A family of queue types.
         (Q : ∀ {ℓ} → Type ℓ → Type ℓ)
         -- Some operations are only available for carrier types
         -- satisfying this predicate.
         (P : ∀ {ℓ} → Type ℓ → Type ℓ)
         ℓ :
         Type (lsuc ℓ) where
  field

    -- Conversion functions.

    to-List           : {A : Type ℓ} → P A → Q A → List A
    from-List         : {A : Type ℓ} → List A → Q A
    to-List-from-List : to-List p (from-List xs) ≡ xs

    -- Enqueues an element.

    enqueue         : {A : Type ℓ} → A → Q A → Q A
    to-List-enqueue : to-List p (enqueue x q) ≡ to-List p q ++ x ∷ []

    -- Dequeues an element, if possible.

    dequeue         : {A : Type ℓ} → P A → Q A → Maybe (A × Q A)
    to-List-dequeue : ⊎-map id (Σ-map id (to-List p)) (dequeue p q) ≡
                      _↔_.to List↔Maybe[×List] (to-List p q)

    -- The "inverse" of the dequeue operation.

    dequeue⁻¹         : {A : Type ℓ} → Maybe (A × Q A) → Q A
    to-List-dequeue⁻¹ :
      to-List p (dequeue⁻¹ x) ≡
      _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id (to-List p)) x)

-- This module exports universe-polymorphic queue
-- operations/properties.

module Is-queue⁺ ⦃ is-queue : ∀ {ℓ} → Is-queue Q P ℓ ⦄ where

  private
    module Q {ℓ} = Is-queue (is-queue {ℓ = ℓ})
  open Q public

  -- A split surjection from queues to lists.

  Queue↠List : P A → Q A ↠ List A
  Queue↠List p = record
    { logical-equivalence = record
      { to   = to-List p
      ; from = from-List
      }
    ; right-inverse-of = λ _ → to-List-from-List
    }

  -- An empty queue.

  empty : Q A
  empty = dequeue⁻¹ nothing

  to-List-empty : to-List p empty ≡ ([] ⦂ List A)
  to-List-empty {p = p} =
    to-List p empty                                                       ≡⟨⟩
    to-List p (dequeue⁻¹ nothing)                                         ≡⟨ to-List-dequeue⁻¹ ⟩
    _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id (to-List p)) nothing)  ≡⟨⟩
    []                                                                    ∎

  -- Adds an element to the front of a queue.

  cons : A → Q A → Q A
  cons x q = dequeue⁻¹ (just (x , q))

  to-List-cons : to-List p (cons x q) ≡ x ∷ to-List p q
  to-List-cons {p = p} {x = x} {q = q} =
    to-List p (cons x q)                                ≡⟨⟩

    to-List p (dequeue⁻¹ (just (x , q)))                ≡⟨ to-List-dequeue⁻¹ ⟩

    _↔_.from List↔Maybe[×List]
      (⊎-map id (Σ-map id (to-List p)) (just (x , q)))  ≡⟨⟩

    x ∷ to-List p q                                     ∎

open Is-queue⁺ public

-- A specification of when (and how) a type constructor implements
-- output-restricted deques with a map function.

record Is-queue-with-map
         (Q : ∀ {ℓ} → Type ℓ → Type ℓ)
         ⦃ is-queue : ∀ {ℓ} → Is-queue Q P ℓ ⦄
         ℓ₁ ℓ₂ :
         Type (lsuc (ℓ₁ ⊔ ℓ₂)) where
  field

    -- A map function.

    map         : {A : Type ℓ₁} {B : Type ℓ₂} →
                  (A → B) → Q A → Q B
    to-List-map : {p₁ : P B} {p₂ : P A} →
                  to-List p₁ (map f q) ≡ L.map f (to-List p₂ q)

-- This module exports universe-polymorphic queue
-- operations/properties.

module Is-queue-with-map⁺
  ⦃ is-queue : ∀ {ℓ} → Is-queue Q P ℓ ⦄
  ⦃ is-queue-with-map : ∀ {ℓ₁ ℓ₂} → Is-queue-with-map Q ℓ₁ ℓ₂ ⦄
  where

  private
    module Q {ℓ₁ ℓ₂} =
      Is-queue-with-map (is-queue-with-map {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂})
  open Q public

open Is-queue-with-map⁺ public

-- A specification of when (and how) a type constructor implements
-- output-restricted deques with unique representations.

record Is-queue-with-unique-representations
         (Q : ∀ {ℓ} → Type ℓ → Type ℓ)
         ⦃ is-queue : ∀ {ℓ} → Is-queue Q P ℓ ⦄
         ℓ :
         Type (lsuc ℓ) where
  field

    -- The from-List function is a left inverse of to-List.

    from-List-to-List :
      {A : Type ℓ} {p : P A} {q : Q A} →
      from-List (to-List p q) ≡ q

-- This module exports universe-polymorphic queue
-- operations/properties.

module Is-queue-with-unique-representations⁺
  ⦃ is-queue : ∀ {ℓ} → Is-queue Q P ℓ ⦄
  ⦃ is-queue-with-unique-representations :
      ∀ {ℓ} → Is-queue-with-unique-representations Q ℓ ⦄
  where

  private
    module Q {ℓ} =
      Is-queue-with-unique-representations
        (is-queue-with-unique-representations {ℓ = ℓ})
  open Q public

  -- A bijection between queues and lists.

  Queue↔List : P A → Q A ↔ List A
  Queue↔List p = record
    { surjection      = Queue↠List p
    ; left-inverse-of = λ _ → from-List-to-List
    }

  -- There is a bijection between equality of two queues and equality
  -- of the corresponding lists.

  ≡-for-lists↔≡ :
    {A : Type a} {p : P A} {q₁ q₂ : Q A} →
    to-List p q₁ ≡ to-List p q₂ ↔ q₁ ≡ q₂
  ≡-for-lists↔≡ {p = p} {q₁ = q₁} {q₂ = q₂} =
    to-List p q₁ ≡ to-List p q₂  ↔⟨ Eq.≃-≡ $ Eq.↔⇒≃ $ Queue↔List _ ⟩□
    q₁ ≡ q₂                      □

  -- A variant of Queue↔List.

  Maybe[×Queue]↔List : P A → Maybe (A × Q A) ↔ List A
  Maybe[×Queue]↔List {A = A} p =
    Maybe (A × Q A)     ↝⟨ F.id ⊎-cong F.id ×-cong Queue↔List p ⟩
    Maybe (A × List A)  ↝⟨ inverse List↔Maybe[×List] ⟩□
    List A              □

  -- The function dequeue p is an inverse of dequeue⁻¹.

  Queue↔Maybe[×Queue] : P A → Q A ↔ Maybe (A × Q A)
  Queue↔Maybe[×Queue] {A = A} p =
    Bijection.with-other-function
      (Bijection.with-other-inverse
         (Q A              ↝⟨ Queue↔List p ⟩
          List A           ↝⟨ inverse (Maybe[×Queue]↔List p) ⟩□
          Maybe (A × Q A)  □)
         dequeue⁻¹
         (λ x →
            _↔_.from-to (inverse $ Queue↔List p) (
              to-List p (dequeue⁻¹ x)          ≡⟨ to-List-dequeue⁻¹ ⟩∎
              _↔_.to (Maybe[×Queue]↔List p) x  ∎)))
      (dequeue p)
      (λ q → _↔_.to-from (Maybe[×Queue]↔List p) (
         _↔_.to (Maybe[×Queue]↔List p) (dequeue p q)        ≡⟨⟩

         _↔_.from List↔Maybe[×List]
           (⊎-map id (Σ-map id (to-List p)) (dequeue p q))  ≡⟨ cong (_↔_.from List↔Maybe[×List]) to-List-dequeue ⟩

         _↔_.from List↔Maybe[×List]
           (_↔_.to List↔Maybe[×List] (to-List p q))         ≡⟨ _↔_.left-inverse-of List↔Maybe[×List] _ ⟩∎

         to-List p q                                        ∎))

  _ : {A : Type a} {p : P A} →
      _↔_.to (Queue↔Maybe[×Queue] p) ≡ dequeue p
  _ = refl _

  _ : {A : Type a} {p : P A} →
      _↔_.from (Queue↔Maybe[×Queue] p) ≡ dequeue⁻¹
  _ = refl _

  -- The function from-List can be expressed using enqueue and empty.

  from-List≡foldl-enqueue-empty :
    {A : Type a} {xs : List A} →
    P A → from-List xs ≡ foldl (flip enqueue) empty xs
  from-List≡foldl-enqueue-empty {A = A} {xs = xs} p =
    _↔_.to ≡-for-lists↔≡ (
      to-List p (from-List xs)                   ≡⟨ to-List-from-List ⟩
      xs                                         ≡⟨⟩
      [] ++ xs                                   ≡⟨ cong (_++ _) $ sym to-List-empty ⟩
      to-List p empty ++ xs                      ≡⟨ lemma _ _ ⟩∎
      to-List p (foldl (flip enqueue) empty xs)  ∎)
    where
    lemma :
      ∀ xs (q : Q A) →
      to-List p q ++ xs ≡ to-List p (foldl (flip enqueue) q xs)
    lemma [] q =
      to-List p q ++ []  ≡⟨ ++-right-identity _ ⟩∎
      to-List p q        ∎
    lemma (x ∷ xs) q =
      to-List p q ++ x ∷ xs                              ≡⟨ ++-associative (to-List _ _) _ _ ⟩
      (to-List p q ++ x ∷ []) ++ xs                      ≡⟨ cong (_++ _) $ sym to-List-enqueue ⟩
      to-List p (enqueue x q) ++ xs                      ≡⟨ lemma _ _ ⟩
      to-List p (foldl (flip enqueue) (enqueue x q) xs)  ≡⟨⟩
      to-List p (foldl (flip enqueue) q (x ∷ xs))        ∎

  -- A corollary.

  to-List-foldl-enqueue-empty :
    {A : Type a} {p : P A} (xs : List A) →
    to-List p (foldl (flip enqueue) empty xs) ≡ xs
  to-List-foldl-enqueue-empty {p = p} xs =
    to-List p (foldl (flip enqueue) empty xs)  ≡⟨ cong (to-List p) $ sym $ from-List≡foldl-enqueue-empty p ⟩
    to-List p (from-List xs)                   ≡⟨ to-List-from-List ⟩∎
    xs                                         ∎

open Is-queue-with-unique-representations⁺ public

instance

  -- Lists can be seen as queues.

  List-is-queue : Is-queue List (λ _ → ↑ _ ⊤) ℓ
  List-is-queue .Is-queue.to-List   = λ _ → id
  List-is-queue .Is-queue.from-List = id
  List-is-queue .Is-queue.enqueue   = λ x xs → xs ++ x ∷ []
  List-is-queue .Is-queue.dequeue   = λ _ → _↔_.to List↔Maybe[×List]
  List-is-queue .Is-queue.dequeue⁻¹ = _↔_.from List↔Maybe[×List]

  List-is-queue .Is-queue.to-List-from-List               = refl _
  List-is-queue .Is-queue.to-List-enqueue                 = refl _
  List-is-queue .Is-queue.to-List-dequeue {q = []}        = refl _
  List-is-queue .Is-queue.to-List-dequeue {q = _ ∷ _}     = refl _
  List-is-queue .Is-queue.to-List-dequeue⁻¹ {x = nothing} = refl _
  List-is-queue .Is-queue.to-List-dequeue⁻¹ {x = just _}  = refl _

  List-is-queue-with-map : Is-queue-with-map List ℓ₁ ℓ₂
  List-is-queue-with-map .Is-queue-with-map.map         = L.map
  List-is-queue-with-map .Is-queue-with-map.to-List-map = refl _

  List-is-queue-with-unique-representations :
    Is-queue-with-unique-representations List ℓ
  List-is-queue-with-unique-representations
    .Is-queue-with-unique-representations.from-List-to-List = refl _

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2017-12-04, issue #2862, reported by m0davis
-- Regression in development version 2.5.4

-- Scope checker allowed definition in different module than signature

-- {-# OPTIONS -v scope.data.def:30 #-}

open import Agda.Builtin.Equality

data N : Set

module Z where
  data N where  -- should be rejected since signature lives in different module
    zero : N
  unitary-N : (x y : N) → x ≡ y
  unitary-N zero zero = refl

data N where
  zero : N
  suc : N → N

data ⊥ : Set where

one : N
one = suc zero

¬zero≡one : zero ≡ one → ⊥
¬zero≡one ()

zero≡one : zero ≡ one
zero≡one = Z.unitary-N zero one

boom : ⊥
boom = ¬zero≡one zero≡one


text:
module Acc where

data Acc ( A : Set ) ( Lt : A -> A -> Set) : A -> Set where
  acc :    (   b : A )
        -> ( ( a : A ) -> Lt a b  ->  Acc A Lt a )
        -> ( Acc A Lt b )

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

data Lt : Nat -> Nat -> Set where
  ltzero : ( x : Nat ) -> Lt zero (succ x)
  ltsucc : ( x : Nat ) -> (y : Nat) -> Lt x y -> Lt (succ x) (succ y)

ltstep : (x : Nat) ->  Lt x (succ x)
ltstep zero = ltzero _
ltstep (succ x) = ltsucc _ _ (ltstep x)

notLt0 : ( x : Nat ) -> Lt x zero -> (C : Set) -> C
notLt0 x ()

wkLt : ( x y : Nat ) -> Lt (succ x) (succ y) -> Lt x y
wkLt zero (succ y) _ = ltzero y
wkLt x zero (ltsucc .x .zero ())
wkLt x y (ltsucc .x .y p) = p

{-
wkLt1 : ( x y : Nat ) -> Lt (succ x) y -> Lt x y
wkLt1 x zero ()
wkLt1 zero (succ y) _ = ltzero y
wkLt1 (succ x) (succ y) (ltsucc .(succ x)  .y p) = ltsucc x y (wkLt1 x y p)
-}

wkLt2 : (x y : Nat ) -> Lt x y -> Lt x (succ y)
wkLt2 x zero ()
wkLt2 zero y p = ltzero y
wkLt2 (succ x) (succ y) (ltsucc .x .y p) = ltsucc x (succ y) (wkLt2 x y p)

ltcase : ( x : Nat ) -> ( y : Nat ) -> Lt x (succ y) ->
         ( P : Nat -> Set ) -> ( (x' : Nat ) -> Lt x' y -> P x') -> P y -> P x
ltcase zero zero      _ P hx' hy = hy
ltcase zero (succ y') _ P hx' hy = hx' zero (ltzero y')
ltcase (succ x') zero (ltsucc .x' .zero ()) _ _ _
ltcase (succ x') (succ y') (ltsucc .x' .(succ y') p) P hx' hy =
  ltcase x' y' p (\ n -> P (succ n))
    (\ x'' p' -> hx' (succ x'') (ltsucc x'' y' p')) hy

accSucc : (x : Nat) -> Acc Nat Lt x -> Acc Nat Lt (succ x)
accSucc x (acc .x h) = acc (succ x) (\ y p -> ltcase y x p (Acc Nat Lt) h (acc x h))

accLt : ( x : Nat ) -> Acc Nat Lt x
accLt zero = acc zero (\a -> \p -> notLt0 a p (Acc Nat Lt a) )
accLt (succ x) = accSucc x (accLt x)

-- subtraction x - y

sub : Nat -> Nat -> Nat
sub zero y = zero
sub (succ x) zero = succ x
sub (succ x) (succ y) = sub x y

subLt : (x y : Nat) -> Lt (sub (succ x) (succ y)) (succ x)
subLt zero y = ltzero _
subLt (succ x') zero = ltstep (succ x')
subLt (succ x') (succ y') = wkLt2 _ _ (subLt x' y')

-- division  x / (y + 1)

div' : (x y : Nat) -> Acc Nat Lt x -> Nat
div' zero _ _ = zero
div' (succ x') y' (acc ._ h) = succ (div' z y' (h _ p))
  where z = sub (succ x') (succ y')
        p = subLt x' y'

----

data WO ( A : Set ) ( Lt : A -> A -> Set ) : Set where
  wo : ((x : A) -> Acc A Lt x) -> WO A Lt

woLt : WO Nat Lt
woLt = wo accLt

max_stars_repo_name: andreasabel/miniagda

max_issues_repo_name: andreasabel/miniagda

max_forks_repo_name: andreasabel/miniagda


text:
module Binders.Var where

data Var  (a b : Set) :   Set where
     Free :  a -> Var a b
     Bound : b -> Var a b


text:
module LearnYouAgda where
  data ℕ : Set where
    zero : ℕ
--    one  : ℕ
    suc  : ℕ -> ℕ

-- define arithmetic operations
  _+_ : ℕ → ℕ → ℕ
  zero + zero = zero
  zero + n    = n
  (suc n) + n′ = suc (n + n′)

max_stars_repo_name: supeterlau/bedev

max_issues_repo_name: supeterlau/bedev

max_forks_repo_name: supeterlau/bedev


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

open import Base
open import Homotopy.TruncatedHIT
open import Integers

module Algebra.FreeGroupProps {i} (A : Set i) ⦃ p : is-set A ⦄ where

import Algebra.FreeGroup
open Algebra.FreeGroup A

abstract
  freegroup-is-set : is-set freegroup
  freegroup-is-set =
    spheres-filled-is-truncated _ freegroup (λ ()) (λ f → (top f , rays f))

x·-is-equiv : (x : A) → is-equiv (λ u → x · u)
x·-is-equiv x = iso-is-eq (λ u → x · u)
  (λ u → x ⁻¹· u)
  (right-inverse-· x)
  (left-inverse-· x)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Modality
open import lib.types.Truncation

module lib.modalities.Truncation where

Trunc-modality : ∀ {i} n → Modality i
Trunc-modality n = record {
  is-local = has-level n;
  is-local-is-prop = has-level-is-prop;
  ◯ = Trunc n;
  ◯-is-local = Trunc-level;
  η = [_];
  ◯-elim = λ f → Trunc-elim {{f}};
  ◯-elim-β = λ _ _ _ → idp;
  ◯-=-is-local = λ _ _ → =-preserves-level Trunc-level}

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Categories.Bicategory using (Bicategory)

-- A Pseudofunctor is a homomorphism of Bicategories
-- Follow Bénabou's definition, which is basically that of a Functor

-- Note that what is in nLab is an "exploded" version of the simpler version below

module Categories.Pseudofunctor {o ℓ e t o′ ℓ′ e′ t′}
                                (C : Bicategory o ℓ e t)
                                (D : Bicategory o′ ℓ′ e′ t′)
                                where

open import Level
open import Data.Product using (_,_)

import Categories.Bicategory.Extras as BicategoryExtras
open import Categories.Category using (Category; _[_,_]; module Commutation)
open import Categories.Category.Instance.One using (shift)
open import Categories.Category.Product using (_⁂_)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_)

open BicategoryExtras using (module ComHom)
open Category using (Obj)
open NaturalIsomorphism using (F⇒G; F⇐G)

private
  module C = BicategoryExtras C
  module D = BicategoryExtras D

record Pseudofunctor : Set (o ⊔ ℓ ⊔ e ⊔ t ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ t′) where

  field
    P₀ : C.Obj → D.Obj
    P₁ : {x y : C.Obj} → Functor (C.hom x y) (D.hom (P₀ x) (P₀ y))
    -- For maximal generality, shift the levels of One. P preserves id
    P-identity : {A : C.Obj} →  D.id {P₀ A} ∘F shift o′ ℓ′ e′ ≃ P₁ ∘F (C.id {A})
    -- P preserves composition
    P-homomorphism : {x y z : C.Obj} → D.⊚ ∘F (P₁ ⁂ P₁) ≃ P₁ ∘F C.⊚ {x} {y} {z}
    -- P preserves ≃

  module P₁ {x} {y} = Functor (P₁ {x} {y})
  module unitˡ {A} = NaturalTransformation (F⇒G (P-identity {A}))
  module unitʳ {A} = NaturalTransformation (F⇐G (P-identity {A}))
  module Hom {x} {y} {z} = NaturalTransformation (F⇒G (P-homomorphism {x} {y} {z}))

  -- For notational convenience, shorten some functor applications
  private
    F₀   = λ {x y} f → Functor.F₀ (P₁ {x} {y}) f
    F₁   = λ {x y f g} α → Functor.F₁ (P₁ {x} {y}) {f} {g} α
    Pid  = λ {A} → NaturalTransformation.η (F⇒G (P-identity {A})) _
    Phom = λ {x} {y} {z} f,g →
           NaturalTransformation.η (F⇒G (P-homomorphism {x} {y} {z})) f,g

  field
    unitaryˡ : {x y : C.Obj} →
               let open ComHom D in
               {f : Obj (C.hom x y)} →
               [ D.id₁ D.⊚₀ F₀ f     ⇒ F₀ f ]⟨
                 Pid D.⊚₁ D.id₂      ⇒⟨ F₀ C.id₁ D.⊚₀ F₀ f ⟩
                 Phom (C.id₁ , f)    ⇒⟨ F₀ (C.id₁ C.⊚₀ f) ⟩
                 F₁ C.unitorˡ.from
               ≈ D.unitorˡ.from
               ⟩
    unitaryʳ : {x y : C.Obj} →
               let open ComHom D in
               {f : Obj (C.hom x y)} →
               [ F₀ f D.⊚₀ D.id₁     ⇒ F₀ f ]⟨
                 D.id₂ D.⊚₁ Pid      ⇒⟨ F₀ f D.⊚₀ F₀ C.id₁ ⟩
                 Phom (f , C.id₁)    ⇒⟨ F₀ (f C.⊚₀ C.id₁) ⟩
                 F₁ C.unitorʳ.from
               ≈ D.unitorʳ.from
               ⟩

    assoc : {x y z w : C.Obj} →
            let open ComHom D in
            {f : Obj (C.hom x y)} {g : Obj (C.hom y z)} {h : Obj (C.hom z w)} →
            [ (F₀ h D.⊚₀ F₀ g) D.⊚₀ F₀ f    ⇒ F₀ (h C.⊚₀ (g C.⊚₀ f)) ]⟨
              Phom (h , g) D.⊚₁ D.id₂       ⇒⟨ F₀ (h C.⊚₀ g) D.⊚₀ F₀ f ⟩
              Phom (_ , f)                  ⇒⟨ F₀ ((h C.⊚₀ g) C.⊚₀ f) ⟩
              F₁ C.associator.from
            ≈ D.associator.from             ⇒⟨ F₀ h D.⊚₀ (F₀ g D.⊚₀ F₀ f) ⟩
              D.id₂ D.⊚₁ Phom (g , f)       ⇒⟨ F₀ h D.⊚₀ F₀ (g C.⊚₀ f) ⟩
              Phom (h , _)
            ⟩

  -- Useful shorthands

  ₀        = P₀
  module ₁ = P₁

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:
{-# OPTIONS --allow-unsolved-metas --universe-polymorphism #-}

module Issue203 where

postulate
  Level : Set
  zero : Level
  suc  : Level → Level
  max : Level → Level → Level

{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO zero #-}
{-# BUILTIN LEVELSUC suc #-}
{-# BUILTIN LEVELMAX max #-}

-- Should work but give unsolved metas (type of b)
data ↓ {a b} (A : Set a) : Set a where
  [_] : (x : A) → ↓ A

mutual -- avoid freezing

  -- Shouldn't instantiate the level of Σ to a
  data Σ {a b} (A : Set a) (B : A → Set b) : Set _ where
    _,_ : (x : A) (y : B x) → Σ A B

  instantiateToMax : ∀ {a b}(A : Set a)(B : A → Set b) → Set (max a b)
  instantiateToMax = Σ

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Test where

-- To compile code: stack exec -- agda Test.agda -c
-- or: agda Test.agda -c --ghc-flag=-dynamic
open import IO

-- All of these are not necessary but they help to reduce clutter when looking
-- at the types of the different things in the code
import Agda.Builtin.List as List
open import Agda.Builtin.Unit using (⊤)
open List using (_∷_)
import Agda.Builtin.String as String

main = run (putStrLn "Hello, World!")

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : { A : Set } → Bool → A → A → A
if true then t else e = t
if false then t else e = e


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

module TypeTheory.HoTT.Function.Properties where

-- agda-stdlib
open import Axiom.Extensionality.Propositional
open import Level

-- agda-misc
open import TypeTheory.HoTT.Base

private
  variable
    a b : Level
    A : Set a
    B : Set b

module _ {a b} {A : Set a} {B : Set b} where
  isProp-→ : Extensionality a b → isProp B → isProp (A → B)
  isProp-→ ext B-isProp f g = ext λ x → B-isProp (f x) (g x)


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

open import Agda.Primitive
open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules

{- Type theory for globular sets -}
module GSeTT.Uniqueness-Derivations where

  has-all-paths-∈ : ∀ {Γ x A} → Γ ⊢C → has-all-paths (x # A ∈ Γ)
  has-all-paths-∈ {Γ :: (y , B)} {x} {A} (cc Γ⊢ γ⊢A idp) (inl x∈Γ) (inl x∈'Γ) = ap inl (has-all-paths-∈ Γ⊢ x∈Γ x∈'Γ)
  has-all-paths-∈ {Γ :: (y , B)} {x} {A} (cc Γ⊢ γ⊢A idp) (inl x∈Γ) (inr (idp , idp)) = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  has-all-paths-∈ {Γ :: (y , B)} {x} {A} (cc Γ⊢ γ⊢A idp) (inr (idp , idp)) (inl x∈Γ) = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  has-all-paths-∈ {Γ :: (y , B)} {x} {A} (cc Γ⊢ γ⊢A idp) (inr (idp , idp)) (inr (p' , q')) =
    ap inr (,= (is-prop-has-all-paths (is-setℕ x (length Γ)) idp p') (is-prop-has-all-paths ((eqdec-is-set eqdec-PreTy) A B) idp q'))

  has-all-paths-⊢C : ∀ {Γ} → has-all-paths (Γ ⊢C)
  has-all-paths-⊢T : ∀ {Γ A} → has-all-paths (Γ ⊢T A)
  has-all-paths-⊢t : ∀ {Γ A t} → has-all-paths (Γ ⊢t t # A)
  has-all-paths-⊢S : ∀ {Δ Γ γ} → has-all-paths (Δ ⊢S γ > Γ)

  has-all-paths-⊢C {nil} ec ec = idp
  has-all-paths-⊢C {Γ :: (x , A)} (cc Γ⊢ Γ⊢A p) (cc Γ⊢' Γ⊢'A q) = ap³ cc ((has-all-paths-⊢C Γ⊢ Γ⊢')) ((has-all-paths-⊢T Γ⊢A Γ⊢'A)) (is-prop-has-all-paths (is-setℕ x (length Γ)) p q)

  has-all-paths-⊢T {Γ} {∗} (ob Γ⊢) (ob Γ⊢') = ap ob (has-all-paths-⊢C Γ⊢ Γ⊢')
  has-all-paths-⊢T {Γ} {⇒ A t u} (ar Γ⊢t:A Γ⊢u:A) (ar Γ⊢'t:A Γ⊢'u:A) = ap² ar (has-all-paths-⊢t Γ⊢t:A Γ⊢'t:A) (has-all-paths-⊢t Γ⊢u:A Γ⊢'u:A)

  has-all-paths-⊢t {Γ} {A} {Var x} (var Γ⊢ x∈Γ) (var Γ⊢' x∈'Γ) = ap² var (has-all-paths-⊢C Γ⊢ Γ⊢') (has-all-paths-∈ Γ⊢ x∈Γ x∈'Γ)

  has-all-paths-⊢S {Δ} {Γ} {<>} (es Δ⊢) (es Δ⊢')= ap es (has-all-paths-⊢C Δ⊢ Δ⊢')
  has-all-paths-⊢S {Δ} {Γ :: (y , A)} {γ :: (x , t)} (sc Δ⊢γ Γ+⊢ Δ⊢t p) (sc Δ⊢'γ Γ+⊢' Δ⊢'t q) =
    ap⁴ sc (has-all-paths-⊢S Δ⊢γ Δ⊢'γ) (has-all-paths-⊢C Γ+⊢ Γ+⊢') (has-all-paths-⊢t Δ⊢t Δ⊢'t) (is-prop-has-all-paths (is-setℕ y x) p q)

  is-prop-⊢C : ∀ Γ → is-prop (Γ ⊢C)
  is-prop-⊢T : ∀ Γ A → is-prop (Γ ⊢T A)
  is-prop-⊢t : ∀ Γ A t → is-prop (Γ ⊢t t # A)
  is-prop-⊢S : ∀ Δ Γ γ → is-prop (Δ ⊢S γ > Γ)

  is-prop-⊢C Γ = has-all-paths-is-prop has-all-paths-⊢C
  is-prop-⊢T Γ A = has-all-paths-is-prop has-all-paths-⊢T
  is-prop-⊢t Γ A t = has-all-paths-is-prop has-all-paths-⊢t
  is-prop-⊢S Γ Δ γ = has-all-paths-is-prop has-all-paths-⊢S

  Γ⊢→length∉ : ∀ {Γ A n} → length Γ ≤ n → Γ ⊢C → ¬ (n # A ∈ Γ)
  Γ⊢→length∉ {.(_ :: (length _ , _))} Sl≤n (cc Γ⊢ x₁ idp) (inl n∈Γ) = Γ⊢→length∉ (Sn≤m→n≤m Sl≤n) Γ⊢ n∈Γ
  Γ⊢→length∉ {.(_ :: (length _ , _))} Sl≤l (cc Γ⊢ x₁ idp) (inr (idp , idp)) = Sn≰n _ Sl≤l

  unique-type : ∀ {Γ t u A B} → (Γ ⊢t t # A) → (Γ ⊢t u # B) →  t == u → A == B
  unique-type {Γ :: a} (var _ (inr (idp , idp))) (var _ (inr (idp , idp))) _ = idp
  unique-type {Γ :: .(_ , _)} (var x (inl x∈Γ)) (var (cc Γ⊢ _ p) (inl x'∈Γ)) idp = unique-type (var Γ⊢ x∈Γ) (var Γ⊢ x'∈Γ ) idp
  unique-type {Γ :: .(_ , _)} (var _ (inl x∈Γ)) (var (cc Γ⊢ _ idp) (inr (idp , idp))) idp = ⊥-elim (Γ⊢→length∉ (n≤n _) Γ⊢ x∈Γ)
  unique-type {Γ :: .(_ , _)} (var (cc Γ⊢ _ idp) (inr (idp , idp))) (var _ (inl x∈Γ)) idp = ⊥-elim (Γ⊢→length∉ (n≤n _) Γ⊢ x∈Γ)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
import SOAS.Families.Core

-- Combinators for context maps
module SOAS.ContextMaps.Combinators {T : Set}
  (open SOAS.Families.Core {T})
  (𝒳 : Familyₛ) where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting
open import SOAS.Variable
open import SOAS.Families.Isomorphism
open import SOAS.Families.BCCC

private
  variable
    Γ Γ′ Δ Δ′ Θ : Ctx
    α β τ : T

-- Sub from the empty context
empty : ∅ ~[ 𝒳 ]↝ Δ
empty ()

-- Combine two maps into the same context by concatenating the domain
copair : Γ ~[ 𝒳 ]↝ Θ → Δ ~[ 𝒳 ]↝ Θ → (Γ ∔ Δ) ~[ 𝒳 ]↝ Θ
copair {∅} σ ς v = ς v
copair {α ∙ Γ} σ ς new = σ new
copair {α ∙ Γ} σ ς (old v) = copair {Γ} (σ ∘ old) ς v

copair≈₁ : {σ₁ σ₂ : Γ ~[ 𝒳 ]↝ Θ}(ς : Δ ~[ 𝒳 ]↝ Θ){v : ℐ α (Γ ∔ Δ)}
         → ({τ : T}(v : ℐ τ Γ) → σ₁ v ≡ σ₂ v)
         → copair σ₁ ς v ≡ copair σ₂ ς v
copair≈₁ ς {v} p = cong (λ - → copair (λ {τ} → - {τ}) ς v) (dext (λ y → p y))
copair≈₂ : (σ : Γ ~[ 𝒳 ]↝ Θ){ς₁ ς₂ : Δ ~[ 𝒳 ]↝ Θ}{v : ℐ α (Γ ∔ Δ)}
         → ({τ : T}(v : ℐ τ Δ) → ς₁ v ≡ ς₂ v)
         → copair σ ς₁ v ≡ copair σ ς₂ v
copair≈₂ σ {v = v} p = cong (λ - → copair σ (λ {τ} → - {τ}) v) (dext (λ y → p y))

-- Split a map from a combined context into two maps
split : (Γ ∔ Δ) ~[ 𝒳 ]↝ Θ → Γ ~[ 𝒳 ]↝ Θ × Δ ~[ 𝒳 ]↝ Θ
split {∅} σ = (λ ()) , σ
split {α ∙ Γ} σ with split {Γ} (σ ∘ old)
... | ς₁ , ς₂ = (λ{ new → σ new ; (old v) → ς₁ v}) , ς₂

-- Expand the codomain of a renaming
expandʳ : ({Γ} Δ : Ctx) → Γ ↝ Γ ∔ Δ
expandʳ {α ∙ Γ} Δ new = new
expandʳ {α ∙ Γ} Δ (old v) = old (expandʳ Δ v)

expandˡ : (Γ {Δ} : Ctx) → Δ ↝ Γ ∔ Δ
expandˡ ∅ v = v
expandˡ (α ∙ Γ) v = old (expandˡ Γ v)

-- Special cases of the above, when one of the contexts is a singleton
-- and the map from the singleton context is isomorphic to a term

-- Add a term to a context map
add : 𝒳 α Δ → Γ ~[ 𝒳 ]↝ Δ → (α ∙ Γ) ~[ 𝒳 ]↝ Δ
add t σ new = t
add t σ (old v) = σ v

-- Consider a term as a context map from the singleton context
asMap : 𝒳 α Γ → ⌊ α ⌋ ~[ 𝒳 ]↝ Γ
asMap t new = t

-- Separate a compound context map into a term and a residual map
detach : (τ ∙ Γ) ~[ 𝒳 ]↝ Δ → 𝒳 τ Δ × (Γ ~[ 𝒳 ]↝ Δ)
detach {_}{∅} σ = σ new , (λ ())
detach {_}{(α ∙ Γ)} σ = σ new , σ ∘ old

add[new][old] : (σ : τ ∙ Γ ~[ 𝒳 ]↝ Δ)(v : ℐ α (τ ∙ Γ))
             → add (σ new) (σ ∘ old) v ≡ σ v
add[new][old] σ new = refl
add[new][old] σ (old v) = refl

-- Remove a term from a compound context map
remove : (τ ∙ Γ) ~[ 𝒳 ]↝ Δ → Γ ~[ 𝒳 ]↝ Δ
remove {_} {∅} σ = λ ()
remove {_} {α ∙ Γ} σ = σ ∘ old

-- Add and remove are inverses
add∘remove : (σ : (τ ∙ Γ) ~[ 𝒳 ]↝ Δ) (v : ℐ α (τ ∙ Γ))
           → add (σ new) (remove σ) v
           ≡ σ v
add∘remove σ new = refl
add∘remove σ (old new) = refl
add∘remove σ (old (old v)) = refl

remove∘add : (σ : Γ ~[ 𝒳 ]↝ Δ) (t : 𝒳 τ Δ)(v : ℐ α Γ)
           → remove (add t σ) v
           ≡ σ v
remove∘add σ t new = refl
remove∘add σ t (old v) = refl

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-

Constant structure: _ ↦ A

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Foundations.SIP

private
  variable
    ℓ ℓ' : Level

-- Structured isomorphisms

module _ (A : Type ℓ') where

  ConstantStructure : Type ℓ → Type ℓ'
  ConstantStructure _ = A

  ConstantEquivStr : StrEquiv {ℓ} ConstantStructure ℓ'
  ConstantEquivStr (_ , a) (_ , a') _ = a ≡ a'

  constantUnivalentStr : UnivalentStr {ℓ} ConstantStructure ConstantEquivStr
  constantUnivalentStr e = idEquiv _

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
record R : Set₁ where
  field
    _! : Set → Set

open R

F : Set → Set
F ! = !


text:
open import MJ.Types
open import MJ.Classtable

module MJ.Syntax {c}(Σ : Classtable c) where

open import MJ.Syntax.Typed Σ public


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

module Data.Sigma.Base where

open import Agda.Builtin.Sigma
  using (Σ; _,_; fst; snd)
  public
open import Level

infixr 4.5 ∃-syntax
∃-syntax : ∀ {a b} {A : Type a} (B : A → Type b) → Type (a ℓ⊔ b)
∃-syntax {A = A} = Σ A

syntax ∃-syntax (λ x → e) = ∃ x × e

infixr 4.5 Σ⦂-syntax
Σ⦂-syntax : (A : Type a) (B : A → Type b) → Type (a ℓ⊔ b)
Σ⦂-syntax = Σ

syntax Σ⦂-syntax t (λ x → e) = Σ[ x ⦂ t ] × e

infixr 4.5 _×_
_×_ : (A : Type a) → (B : Type b) → Type (a ℓ⊔ b)
A × B = Σ A λ _ → B

curry : ∀ {A : Type a} {B : A → Type b} {C : Σ A B → Type c} →
          ((p : Σ A B) → C p) →
          ((x : A) → (y : B x) → C (x , y))
curry f x y = f (x , y)
{-# INLINE curry #-}

uncurry : ∀ {A : Type a} {B : A → Type b} {C : Σ A B → Type c} →
            ((x : A) → (y : B x) → C (x , y)) →
            ((p : Σ A B) → C p)
uncurry f (x , y) = f x y
{-# INLINE uncurry #-}

map-Σ : ∀ {p q} {P : A → Set p} {Q : B → Set q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
map-Σ f g (x , y) = f x , g y
{-# INLINE map-Σ #-}

map₁ : (A → B) → A × C → B × C
map₁ f = map-Σ f (λ x → x)
{-# INLINE map₁ #-}

map₁-Σ : ∀ {A : Set a} {B : Set b} {C : B → Set b}
       → (f : A → B) → Σ A (λ x → C (f x)) → Σ B C
map₁-Σ f (x , y) = f x , y
{-# INLINE map₁-Σ #-}

map₂ : ∀ {A : Set a} {B : A → Set b} {C : A → Set c} →
        (∀ {x} → B x → C x) → Σ A B → Σ A C
map₂ f = map-Σ (λ x → x) f
{-# INLINE map₂ #-}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Open1 where

module M where

  data ⊤
    : Set
    where

    tt
      : ⊤

module N where

  open M

  v
    : ⊤
  v
    = tt

open M
open N

module O where

  w
    : ⊤
  w
    = tt

  x
    : ⊤
  x
    = tt

module P where

  open O
    using (w)
    renaming (x to x')

  y
    : ⊤
  y
    = w

open P

module Q where

  open O
    hiding (w)
    renaming (x to x'')

  z
    : ⊤
  z
    = x''

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module Issue561 where

open import Common.Prelude

open import Common.MAlonzo using ()
  -- if I do not include this, I get compilation errors
  -- MAlonzo/Code/Common/Prelude.hs:8:7:
  --   Not in scope: type constructor or class `Common.FFI.Nat'

primitive
  primIsDigit : Char → Bool

postulate
  return : ∀ {A} → A → IO A

main : IO Bool
main = return true

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Testing the --schematic-functions option
------------------------------------------------------------------------------

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

-- Fails because requires the above option.

module RequiredOption.SchematicFunctions where

postulate
  D   : Set
  fix : (D → D) → D
  _≡_ : D → D → Set

postulate fix-f : (f : D → D) → fix f ≡ f (fix  f)
{-# ATP axiom fix-f #-}

-- We need to have at least one conjecture to generate a TPTP file.
postulate refl : ∀ d → d ≡ d
{-# ATP prove refl #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Problem2 where

open import Problem1

infixr 40 _►_

data Vec (A : Set) : Nat -> Set where
  ε   : Vec A zero
  _►_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

-- 2.1

vec : {A : Set}{n : Nat} -> A -> Vec A n
vec {n = zero } x = ε
vec {n = suc n} x = x ► vec x

-- 2.2

infixl 80 _<*>_

_<*>_ : {A B : Set}{n : Nat} -> Vec (A -> B) n -> Vec A n -> Vec B n
ε        <*> ε        = ε
(f ► fs) <*> (x ► xs) = f x ► fs <*> xs

-- 2.3

map : {A B : Set}{n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f xs = vec f <*> xs

-- 2.4

zip : {A B C : Set}{n : Nat} -> (A -> B -> C) ->
      Vec A n -> Vec B n -> Vec C n
zip f xs ys = vec f <*> xs <*> ys

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue790 where

open import Common.Level   renaming (lzero to zero; lsuc to suc)
open import Common.Prelude using (Bool; true; false; zero; suc) renaming (Nat to ℕ)

even? : ℕ -> Bool
even? 0             = true
even? (suc (suc n)) = even? n
even? _             = false

-- Name overlap between Level's suc and Nat's suc should not matter,
-- since only one is a constructor.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural number division
------------------------------------------------------------------------

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

module Data.Nat.DivMod where

open import Agda.Builtin.Nat using (div-helper; mod-helper)

open import Data.Fin using (Fin; toℕ; fromℕ≤)
open import Data.Fin.Properties using (toℕ-fromℕ≤)
open import Data.Nat as Nat
open import Data.Nat.DivMod.Core
open import Data.Nat.Properties using (≤⇒≤″; +-assoc; +-comm; +-identityʳ)
open import Function using (_$_)
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

------------------------------------------------------------------------
-- Basic operations

infixl 7 _div_ _%_

-- Integer division

_div_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
(a div 0) {}
(a div suc n) = div-helper 0 n a n

-- Integer remainder (mod)

_%_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
(a % 0) {}
(a % suc n) = mod-helper 0 n a n

------------------------------------------------------------------------
-- Properties

a≡a%n+[a/n]*n : ∀ a n → a ≡ a % suc n + (a div (suc n)) * suc n
a≡a%n+[a/n]*n a n = division-lemma 0 0 a n

a%1≡0 : ∀ a → a % 1 ≡ 0
a%1≡0 = a[modₕ]1≡0

a%n<n : ∀ a n → a % suc n < suc n
a%n<n a n = s≤s (a[modₕ]n<n 0 a n)

n%n≡0 : ∀ n → suc n % suc n ≡ 0
n%n≡0 n = n[modₕ]n≡0 0 n

a%n%n≡a%n : ∀ a n → a % suc n % suc n ≡ a % suc n
a%n%n≡a%n a n = modₕ-idem 0 a n

[a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n
[a+n]%n≡a%n a n = a+n[modₕ]n≡a[modₕ]n 0 a n

[a+kn]%n≡a%n : ∀ a k n → (a + k * (suc n)) % suc n ≡ a % suc n
[a+kn]%n≡a%n a zero    n = cong (_% suc n) (+-identityʳ a)
[a+kn]%n≡a%n a (suc k) n = begin
  (a + (m + k * m)) % m ≡⟨ cong (_% m) (sym (+-assoc a m (k * m))) ⟩
  (a + m + k * m)   % m ≡⟨ [a+kn]%n≡a%n (a + m) k n ⟩
  (a + m)           % m ≡⟨ [a+n]%n≡a%n a n ⟩
  a                 % m ∎
  where m = suc n

kn%n≡0 : ∀ k n → k * (suc n) % suc n ≡ 0
kn%n≡0 = [a+kn]%n≡a%n 0

%-distribˡ-+ : ∀ a b n → (a + b) % suc n ≡ (a % suc n + b % suc n) % suc n
%-distribˡ-+ a b n = begin
  (a + b)                           % m ≡⟨ cong (λ v → (v + b) % m) (a≡a%n+[a/n]*n a n) ⟩
  (a % m +  a div m * m + b)        % m ≡⟨ cong (_% m) (+-assoc (a % m) _ b) ⟩
  (a % m + (a div m * m + b))       % m ≡⟨ cong (λ v → (a % m + v) % m) (+-comm _ b) ⟩
  (a % m + (b + a div m * m))       % m ≡⟨ cong (_% m) (sym (+-assoc (a % m) b _)) ⟩
  (a % m +  b + a div m * m)        % m ≡⟨ [a+kn]%n≡a%n (a % m + b) (a div m) n ⟩
  (a % m +  b)                      % m ≡⟨ cong (λ v → (a % m + v) % m) (a≡a%n+[a/n]*n b n) ⟩
  (a % m + (b % m + (b div m) * m)) % m ≡⟨ sym (cong (_% m) (+-assoc (a % m) (b % m) _)) ⟩
  (a % m +  b % m + (b div m) * m)  % m ≡⟨ [a+kn]%n≡a%n (a % m + b % m) (b div m) n ⟩
  (a % m +  b % m)                  % m ∎
  where m = suc n

------------------------------------------------------------------------
--  A specification of integer division.

record DivMod (dividend divisor : ℕ) : Set where
  constructor result
  field
    quotient  : ℕ
    remainder : Fin divisor
    property  : dividend ≡ toℕ remainder + quotient * divisor

_mod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
(a mod 0) {}
(a mod suc n) = fromℕ≤ (a%n<n a n)

_divMod_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} →
           DivMod dividend divisor
(a divMod 0) {}
(a divMod suc n) = result (a div suc n) (a mod suc n) $ begin
  a                                   ≡⟨ a≡a%n+[a/n]*n a n ⟩
  a % suc n                + [a/n]*n  ≡⟨ cong (_+ [a/n]*n) (sym (toℕ-fromℕ≤ (a%n<n a n))) ⟩
  toℕ (fromℕ≤ (a%n<n a n)) + [a/n]*n  ∎
  where
  [a/n]*n = a div suc n * suc n


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise equality over lists using propositional equality
------------------------------------------------------------------------

-- Note think carefully about using this module as pointwise
-- propositional equality can usually be replaced with propositional
-- equality.

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

open import Relation.Binary

module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where

open import Data.List.Base
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Re-export everything from setoid equality

open SetoidEquality (P.setoid A) public

------------------------------------------------------------------------
-- ≋ is propositional

≋⇒≡ : _≋_ ⇒ _≡_
≋⇒≡ []               = P.refl
≋⇒≡ (P.refl ∷ xs≈ys) = P.cong (_ ∷_) (≋⇒≡ xs≈ys)

≡⇒≋ : _≡_ ⇒ _≋_
≡⇒≋ P.refl = ≋-refl


text:
module Data.Union where

open import Data.List using (List; _∷_; [_]; [])
open import Data.List.Relation.Unary.Any using (here; there; _─_)
open import Data.List.Membership.Propositional using (_∈_)

open import Data.Maybe using (Maybe; just; nothing; _>>=_)

open import Level using (Level; _⊔_)

open import Function using (_∘_)

-- ----------------------------------------------------------------------
-- Definition
--
-- A union of the family B defined by the list of tags ts
-- of type A

data Union {a b} (A : Set a) (B : A → Set b) : List A → Set (a ⊔ b) where
  here : ∀ {t ts} → B t → Union A B (t ∷ ts)
  there : ∀ {t ts} → Union A B ts → Union A B (t ∷ ts)

-- ----------------------------------------------------------------------
-- Injection and projections to (and from) unions

private
  variable
    a b : Level
    A : Set a
    B : A → Set b
    t : A
    ts ts′ : List A

inj : t ∈ ts → B t → Union A B ts
inj (here t≡t′) x rewrite t≡t′ = here x
inj (there t∈ts) x = there (inj t∈ts x)

`_ : ⦃ t ∈ ts ⦄ → B t → Union A B ts
`_ ⦃ t∈ts ⦄ x = inj t∈ts x

proj : t ∈ ts → Union A B ts → Maybe (B t)
proj (here t≡t′) (here x) rewrite t≡t′ = just x
proj (there t∈ts) (here x) = nothing
proj (here t≡t′) (there x) = nothing
proj (there t∈ts) (there x) = proj t∈ts x

`proj : ⦃ t ∈ ts ⦄ → Union A B ts → Maybe (B t)
`proj ⦃ t∈ts ⦄ x = proj t∈ts x

proj₀ : Union A B [ t ] → B t
proj₀ (here x) = x

remove : Union A B ts → (i : t ∈ ts) → Maybe (Union A B (ts ─ i))
remove (here x) (here _) = nothing
remove (here x) (there _) = just (here x)
remove (there x) (here _) = just x
remove (there x) (there t∈ts) = remove x t∈ts >>= just ∘ there

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union


text:
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ) renaming ( _≟[_]_  to _≟?[_]_ )
open import FRP.JS.Nat using ( ℕ ; zero ; suc ; _≟_ ; _<_ )
open import FRP.JS.Object using ( Object ; IObject ; [] ; _↦_∷_ ; object ; ⟪⟫ ; ⟪_ ; _↦_,_ ; _↦_⟫ ; _≟[_]_ ; _⊆[_]_ ; lookup ; lookup? ; map ; filter )
open import FRP.JS.QUnit using ( TestSuite ; ok ; test ; _,_ )

module FRP.JS.Test.Object where

_≟*_ : Object ℕ → Object ℕ → Bool
xs ≟* ys = xs ≟[ _≟_ ] ys

_⊆*_ : Object ℕ → Object ℕ → Bool
xs ⊆* ys = xs ⊆[ _≟_ ] ys

_≟?_ : Maybe ℕ → Maybe ℕ → Bool
xs ≟? ys = xs ≟?[ _≟_ ] ys

_≟??_ : Maybe (Maybe ℕ) → Maybe (Maybe ℕ) → Bool
xs ≟?? ys = xs ≟?[ _≟?_ ] ys

iincr : ∀ {ks ks✓} → IObject ℕ ks ks✓ → IObject ℕ ks ks✓
iincr []           = []
iincr (k ↦ n ∷ ns) = k ↦ suc n ∷ iincr ns

incr : Object ℕ → Object ℕ
incr (object ns) = object (iincr ns)

⟪a↦0⟫     = ⟪ "a" ↦ 0 ⟫
⟪a↦1⟫     = ⟪ "a" ↦ 1 ⟫
⟪a↦0,b↦1⟫ = ⟪ "a" ↦ 0 , "b" ↦ 1 ⟫
⟪a↦1,b↦2⟫ = ⟪ "a" ↦ 1 , "b" ↦ 2 ⟫
⟪b↦0⟫     = ⟪ "b" ↦ 0 ⟫
⟪b↦2⟫     = ⟪ "b" ↦ 2 ⟫
⟪a↦n⟫     = ⟪ "a" ↦ nothing {A = ℕ} ⟫
⟪a↦j0⟫    = ⟪ "a" ↦ just 0 ⟫

tests : TestSuite
tests =
  ( test "≟"
    ( ok "⟪⟫ ≟ ⟪⟫" (⟪⟫ ≟* ⟪⟫)
    , ok "⟪a↦0⟫ ≟ ⟪⟫" (not (⟪a↦0⟫ ≟* ⟪⟫))
    , ok "⟪⟫ ≟ ⟪a↦0⟫" (not (⟪⟫ ≟* ⟪a↦0⟫))
    , ok "⟪a↦0⟫ ≟ ⟪a↦0⟫" (⟪a↦0⟫ ≟* ⟪a↦0⟫)
    , ok "⟪a↦0⟫ ≟ ⟪a↦1⟫" (not (⟪a↦0⟫ ≟* ⟪a↦1⟫))
    , ok "⟪a↦0⟫ ≟ ⟪a↦0,b↦1⟫" (not (⟪a↦0⟫ ≟* ⟪a↦0,b↦1⟫))
    , ok "⟪a↦0,b↦1⟫ ≟ ⟪a↦0⟫" (not (⟪a↦0,b↦1⟫ ≟* ⟪a↦0⟫))
    , ok "⟪a↦0,b↦1⟫ ≟ ⟪a↦0,b↦1⟫" (⟪a↦0,b↦1⟫ ≟* ⟪a↦0,b↦1⟫) )
  , test "⊆"
    ( ok "⟪⟫ ⊆ ⟪⟫" (⟪⟫ ⊆* ⟪⟫)
    , ok "⟪a↦0⟫ ⊆ ⟪⟫" (not (⟪a↦0⟫ ⊆* ⟪⟫))
    , ok "⟪⟫ ⊆ ⟪a↦0⟫" (⟪⟫ ⊆* ⟪a↦0⟫)
    , ok "⟪a↦0⟫ ⊆ ⟪a↦0⟫" (⟪a↦0⟫ ⊆* ⟪a↦0⟫)
    , ok "⟪a↦0⟫ ⊆ ⟪a↦1⟫" (not (⟪a↦0⟫ ⊆* ⟪a↦1⟫))
    , ok "⟪a↦0⟫ ⊆ ⟪a↦0,b↦1⟫" (⟪a↦0⟫ ⊆* ⟪a↦0,b↦1⟫)
    , ok "⟪a↦0,b↦1⟫ ⊆ ⟪a↦0⟫" (not (⟪a↦0,b↦1⟫ ⊆* ⟪a↦0⟫))
    , ok "⟪a↦0,b↦1⟫ ⊆ ⟪a↦0,b↦1⟫" (⟪a↦0,b↦1⟫ ⊆* ⟪a↦0,b↦1⟫) )
  , test "lookup"
    ( ok "lookup ⟪a↦0⟫ a" (lookup ⟪a↦0⟫ "a" ≟ 0)
    , ok "lookup ⟪a↦0,b↦1⟫ a" (lookup ⟪a↦0,b↦1⟫ "b" ≟ 1)
    , ok "lookup ⟪a↦0,b↦1⟫ a" (lookup ⟪a↦0,b↦1⟫ "a" ≟ 0)
    , ok "lookup ⟪a↦0,b↦1⟫ b" (lookup ⟪a↦0,b↦1⟫ "b" ≟ 1)
    , ok "lookup ⟪a↦j0⟫ a" (lookup ⟪a↦j0⟫ "a" ≟? just 0)
    , ok "lookup ⟪a↦n⟫ a" (lookup ⟪a↦n⟫ "a" ≟? nothing)
    , ok "lookup? ⟪⟫    a" (lookup? ⟪⟫ "a" ≟? nothing)
    , ok "lookup? ⟪a↦0⟫ a" (lookup? ⟪a↦0⟫ "a" ≟? just 0)
    , ok "lookup? ⟪a↦0⟫ b" (lookup? ⟪a↦0⟫ "b" ≟? nothing)
    , ok "lookup? ⟪a↦0,b↦1⟫ a" (lookup? ⟪a↦0,b↦1⟫ "a" ≟? just 0)
    , ok "lookup? ⟪a↦0,b↦1⟫ b" (lookup? ⟪a↦0,b↦1⟫ "b" ≟? just 1)
    , ok "lookup? ⟪a↦0,b↦1⟫ c" (lookup? ⟪a↦0,b↦1⟫ "c" ≟? nothing)
    , ok "lookup? ⟪a↦j0⟫ a" (lookup? ⟪a↦j0⟫ "a" ≟?? just (just 0))
    , ok "lookup? ⟪a↦n⟫ a" (lookup? ⟪a↦n⟫ "a" ≟?? just nothing) )
  , test "map"
    ( ok "map suc ⟪⟫" (map suc ⟪⟫ ≟* ⟪⟫)
    , ok "map suc ⟪a↦0⟫" (map suc ⟪a↦0⟫ ≟* ⟪a↦1⟫)
    , ok "map suc ⟪a↦0,b↦1⟫" (map suc ⟪a↦0,b↦1⟫ ≟* ⟪a↦1,b↦2⟫)
    , ok "incr ⟪⟫" (map suc ⟪⟫ ≟* incr ⟪⟫)
    , ok "incr ⟪a↦0⟫" (map suc ⟪a↦0⟫ ≟* incr ⟪a↦0⟫)
    , ok "incr ⟪a↦0,b↦1⟫" (map suc ⟪a↦0,b↦1⟫ ≟* incr ⟪a↦0,b↦1⟫) )
  , test "filter"
    ( ok "filter 0< ⟪a↦1,b↦2⟫" (filter (_<_ 0) ⟪a↦1,b↦2⟫ ≟* ⟪a↦1,b↦2⟫)
    , ok "filter 1< ⟪a↦1,b↦2⟫" (filter (_<_ 1) ⟪a↦1,b↦2⟫ ≟* ⟪b↦2⟫)
    , ok "filter 2< ⟪a↦1,b↦2⟫" (filter (_<_ 2) ⟪a↦1,b↦2⟫ ≟* ⟪⟫) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js