text:
module Issue442 where

postulate
  A : Set
  f : (P : A → A → Set) → (∀ {x} → P x x) →
      (∀ {x y z} → P y z → P x y → A) → A
  P : A → A → Set
  reflP : ∀ {x} → P x x
  g : ∀ {x y z} → P y z → P x y → A

a : A
a = f _ (λ {x} → reflP {x}) g

-- Test case was:
-- {-# OPTIONS --allow-unsolved-metas #-}
-- a = f _ reflP g


text:
module Numeric.Rational where

open import Prelude
open import Numeric.Nat.GCD
open import Numeric.Nat.GCD.Extended
open import Numeric.Nat.GCD.Properties
open import Numeric.Nat.Prime
open import Numeric.Nat.Prime.Properties
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.Properties
open import Tactic.Nat
open import Tactic.Nat.Coprime

record Rational : Set where
  no-eta-equality
  constructor ratio
  field numerator   : Nat
        denominator : Nat
        ⦃ d>0 ⦄    : NonZero denominator
        n⊥d        : Coprime numerator denominator

open Rational public using (numerator; denominator)

infixl 7 mkratio
syntax mkratio p q = p :/ q
mkratio : (p q : Nat) {{_ : NonZero q}} → Rational
mkratio p q = gcdReduce-r p q λ p′ q′ _ _ _ prf → ratio p′ q′ prf

mkratio-sound : (p q : Nat) {{_ : NonZero q}} → p * denominator (mkratio p q) ≡ q * numerator (mkratio p q)
mkratio-sound p q with gcd p q
... | gcd-res d (is-gcd (factor! p′) (factor! q′) _) = auto

NonZeroQ : Rational → Set
NonZeroQ x = NonZero (numerator x)

infixl 6 _+Q_ _-Q_
infixl 7 _*Q_ _/Q_

_+Q_ : Rational → Rational → Rational
ratio n₁ d₁ n₁/d₁ +Q ratio n₂ d₂ n₂/d₂ =
  gcdReduce   d₁ d₂                   λ d₁′ d₂′ g eq₁ eq₂ d₁′/d₂′ →
  gcdReduce-r (n₁ * d₂′ + n₂ * d₁′) g λ s′ g′ g₁ eqs eqg s′/g′ →
  let instance _ = mul-nonzero d₁′ d₂′
               _ = mul-nonzero (d₁′ * d₂′) g′
  in ratio s′ (d₁′ * d₂′ * g′) $
     let[ _ := lemma s′ n₁ d₁ n₂ d₂ d₁′ d₂′ g g₁ eqs  eq₁ n₁/d₁ d₁′/d₂′ ]
     let[ _ := lemma s′ n₂ d₂ n₁ d₁ d₂′ d₁′ g g₁ (by eqs) eq₂ n₂/d₂ auto-coprime ]
     auto-coprime
  where
    lemma : ∀ s′ n₁ d₁ n₂ d₂ d₁′ d₂′ g g₁ →
              s′ * g₁ ≡ n₁ * d₂′ + n₂ * d₁′ →
              d₁′ * g ≡ d₁ →
              Coprime n₁ d₁ → Coprime d₁′ d₂′ → Coprime s′ d₁′
    lemma s′ n₁ d₁ n₂ d₂ d₁′ d₂′ g g₁ eqs refl n₁/d₁ d₁′/d₂′ =
      coprimeByPrimes s′ d₁′ λ p isP p|s′ p|d₁′ →
          let p|n₁d₂′ : p Divides (n₁ * d₂′)
              p|n₁d₂′ = divides-sub-r {n₁ * d₂′} {n₂ * d₁′}
                          (transport (p Divides_) eqs (divides-mul-l g₁ p|s′))
                          (divides-mul-r n₂ p|d₁′)
              p|d₁ : p Divides d₁
              p|d₁ = divides-mul-l g p|d₁′
              p/n₁ : Coprime p n₁
              p/n₁ = case prime-coprime/divide p n₁ isP of λ where
                       (left p/n₁)  → p/n₁
                       (right p|n₁) → ⊥-elim (prime-divide-coprime p n₁ d₁ isP n₁/d₁ p|n₁ p|d₁)
              p|d₂′ : p Divides d₂′
              p|d₂′ = coprime-divide-mul-l p n₁ d₂′ p/n₁ p|n₁d₂′
          in divide-coprime p d₁′ d₂′ d₁′/d₂′ p|d₁′ p|d₂′

-- Specification for addition
slowAddQ : Rational → Rational → Rational
slowAddQ (ratio p q _) (ratio p₁ q₁ _) =
  mkratio (p * q₁ + p₁ * q) (q * q₁) ⦃ mul-nonzero q q₁ ⦄

_-Q_ : Rational → Rational → Rational
ratio p q _ -Q ratio p₁ q₁ _ =
  mkratio (p * q₁ - p₁ * q) (q * q₁) ⦃ mul-nonzero q q₁ ⦄

-- Fast multiplication based on the same technique as the fast addition, except it's much
-- simpler for multiplication.
_*Q_ : Rational → Rational → Rational
ratio n₁ d₁ _ *Q ratio n₂ d₂ _ =
  gcdReduce-r n₁ d₂ λ n₁′ d₂′ g₁ n₁′g₁=n₁ d₂′g₁=d₂ _ →
  gcdReduce-r n₂ d₁ λ n₂′ d₁′ g₂ n₂′g₂=n₂ d₁′g₂=d₁ _ →
  let instance _ = mul-nonzero d₁′ d₂′ in
  ratio (n₁′ * n₂′) (d₁′ * d₂′) $
    case₄ n₁′g₁=n₁ , d₂′g₁=d₂ , n₂′g₂=n₂ , d₁′g₂=d₁ of λ where
      refl refl refl refl → auto-coprime

-- Specification for multiplication
slowMulQ : Rational → Rational → Rational
slowMulQ (ratio p q _) (ratio p₁ q₁ _) = mkratio (p * p₁) (q * q₁) {{mul-nonzero q q₁}}

recip : (x : Rational) {{_ : NonZeroQ x}} → Rational
recip (ratio 0 q eq) {{}}
recip (ratio (suc p) q eq) = ratio q (suc p) auto-coprime

_/Q_ : (x y : Rational) {{_ : NonZeroQ y}} → Rational
x /Q y = x *Q recip y

instance
  FracQ : Fractional Rational
  Fractional.Constraint FracQ _ y = NonZeroQ y
  Fractional._/_        FracQ x y = x /Q y

{-# DISPLAY _+Q_ a b = a + b #-}
{-# DISPLAY _-Q_ a b = a - b #-}
{-# DISPLAY _*Q_ a b = a * b #-}
{-# DISPLAY ratio a b refl = a / b #-}

instance
  NumberRational : Number Rational
  Number.Constraint NumberRational _ = ⊤
  fromNat {{NumberRational}} n = n :/ 1

  SemiringRational : Semiring Rational
  zro {{SemiringRational}} = 0 :/ 1
  one {{SemiringRational}} = 1 :/ 1
  _+_ {{SemiringRational}} = _+Q_
  _*_ {{SemiringRational}} = _*Q_

  ShowRational : Show Rational
  showsPrec {{ShowRational}} _ (ratio p 1 _) = shows p
  showsPrec {{ShowRational}} _ (ratio p q _) = shows p ∘ showString "/" ∘ shows q

-- Ordering --

private
  module _ {p q eq p₁ q₁ eq₁} {{_ : NonZero q}} {{_ : NonZero q₁}} where
    ratio-inj₁ : ratio p q eq ≡ ratio p₁ q₁ eq₁ → p ≡ p₁
    ratio-inj₁ refl = refl

    ratio-inj₂ : ratio p q eq ≡ ratio p₁ q₁ eq₁ → q ≡ q₁
    ratio-inj₂ refl = refl

cong-ratio : ∀ {p q eq p₁ q₁ eq₁} {nzq : NonZero q} {nzq₁ : NonZero q₁} →
             p ≡ p₁ → q ≡ q₁ → ratio p q ⦃ nzq ⦄ eq ≡ ratio p₁ q₁ ⦃ nzq₁ ⦄ eq₁
cong-ratio {q = zero} {nzq = ()}
cong-ratio {q = suc q} refl refl = ratio _ _ $≡ smashed

instance
  EqRational : Eq Rational
  _==_ {{EqRational}} (ratio p q prf) (ratio p₁ q₁ prf₁) with p == p₁ | q == q₁
  ... | no p≠p₁  | _        = no (p≠p₁ ∘ ratio-inj₁)
  ... | yes _    | no q≠q₁  = no (q≠q₁ ∘ ratio-inj₂)
  ... | yes p=p₁ | yes q=q₁ = yes (cong-ratio p=p₁ q=q₁)

data LessQ (x y : Rational) : Set where
  lessQ : numerator x * denominator y < numerator y * denominator x → LessQ x y

private
  lem-unique : ∀ n₁ d₁ n₂ d₂ ⦃ _ : NonZero d₁ ⦄ ⦃ _ : NonZero d₂ ⦄ →
                 Coprime n₁ d₁ → Coprime n₂ d₂ →
                 n₁ * d₂ ≡ n₂ * d₁ → n₁ ≡ n₂ × d₁ ≡ d₂
  lem-unique n₁ d₁ n₂ d₂ n₁⊥d₁ n₂⊥d₂ eq =
    let n₁|n₂ : n₁ Divides n₂
        n₁|n₂ = coprime-divide-mul-r n₁ n₂ d₁ n₁⊥d₁ (factor d₂ (by eq))
        n₂|n₁ : n₂ Divides n₁
        n₂|n₁ = coprime-divide-mul-r n₂ n₁ d₂ n₂⊥d₂ (factor d₁ (by eq))
        d₁|d₂ : d₁ Divides d₂
        d₁|d₂ = coprime-divide-mul-r d₁ d₂ n₁ auto-coprime (factor n₂ (by eq))
        d₂|d₁ : d₂ Divides d₁
        d₂|d₁ = coprime-divide-mul-r d₂ d₁ n₂ auto-coprime (factor n₁ (by eq))
    in divides-antisym n₁|n₂ n₂|n₁ , divides-antisym d₁|d₂ d₂|d₁

compareQ : ∀ x y → Comparison LessQ x y
compareQ (ratio n₁ d₁ n₁⊥d₁) (ratio n₂ d₂ n₂⊥d₂) =
  case compare (n₁ * d₂) (n₂ * d₁) of λ where
    (less lt)    → less (lessQ lt)
    (equal eq)   → equal (uncurry cong-ratio (lem-unique n₁ d₁ n₂ d₂ n₁⊥d₁ n₂⊥d₂ eq))
    (greater gt) → greater (lessQ gt)

instance
  OrdQ : Ord Rational
  OrdQ = defaultOrd compareQ

ext: agda

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
------------------------------------------------------------------------
-- Semantics of the simplified parsers
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Simplified.Semantics where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool
open import Data.List
import Data.List.Properties
private
  module LM {Tok : Set} = Monoid (Data.List.Properties.++-monoid Tok)
open import Data.Product as Prod
open import Function
open import Data.Empty
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import StructurallyRecursiveDescentParsing.Simplified
open import TotalParserCombinators.Parser using (○; ◌)
open import TotalParserCombinators.Semantics as Semantics
  using ([_-_]_>>=_) renaming (_∈_·_ to _∈′_·_)
open Semantics._∈_·_

------------------------------------------------------------------------
-- Semantics

-- The semantics of the parsers. x ∈ p · s means that x can be the
-- result of applying the parser p to the string s. Note that the
-- semantics is defined inductively.

infixl 10 _?>>=_ _!>>=_
infix   4 _∈_·_

data _∈_·_ {Tok} : ∀ {R e} → R → Parser Tok e R → List Tok → Set1 where
  return : ∀ {R} {x : R} → x ∈ return x · []
  token  : ∀ {x} → x ∈ token · [ x ]
  ∣ˡ     : ∀ {R x e₁ e₂ s} {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
           (x∈p₁ : x ∈ p₁ · s) → x ∈ p₁ ∣ p₂ · s
  ∣ʳ     : ∀ {R x e₂ s} e₁ {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
           (x∈p₂ : x ∈ p₂ · s) → x ∈ p₁ ∣ p₂ · s
  _?>>=_ : ∀ {R₁ R₂ x y e₂ s₁ s₂}
             {p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
           (x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ p₂ x · s₂) →
           y ∈ p₁ ?>>= p₂ · s₁ ++ s₂
  _!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s₁ s₂}
             {p₁ : Parser Tok false R₁}
             {p₂ : (x : R₁) → ∞ (Parser Tok (e₂ x) R₂)}
           (x∈p₁ : x ∈ p₁ · s₁) (y∈p₂x : y ∈ ♭ (p₂ x) · s₂) →
           y ∈ p₁ !>>= p₂ · s₁ ++ s₂

------------------------------------------------------------------------
-- _∈_·_ is correct with respect to _∈′_·_

sound : ∀ {Tok e R} {p : Parser Tok e R} {x s} →
        x ∈ p · s → x ∈′ ⟦ p ⟧ · s
sound return              = return
sound token               = token
sound (∣ˡ x∈p₁)           = cast (∣-left               (sound x∈p₁))
sound (∣ʳ _ {p₁} x∈p₂)    = cast (∣-right (initial p₁) (sound x∈p₂))
sound (_?>>=_ {p₂ = p₂}
              x∈p₁ y∈p₂x) = cast ([_-_]_>>=_ ○ ○ {p₂ = λ x → ⟦ p₂ x ⟧}
                                             (sound x∈p₁) (sound y∈p₂x))
sound (x∈p₁ !>>= y∈p₂x)   = [ ○ - ◌ ] sound x∈p₁ >>= sound y∈p₂x

complete : ∀ {Tok e R} (p : Parser Tok e R) {x s} →
           x ∈′ ⟦ p ⟧ · s → x ∈ p · s
complete (return x)       return                   = return
complete fail             ()
complete token            token                    = token
complete (p₁ ∣ p₂)        (cast (∣-left     x∈p₁)) = ∣ˡ    (complete p₁ x∈p₁)
complete (_∣_ {e₁} p₁ p₂) (cast (∣-right ._ x∈p₂)) = ∣ʳ e₁ (complete p₂ x∈p₂)
complete (p₁ ?>>= p₂)     (cast (x∈p₁ >>= y∈p₂x))  = complete p₁ x∈p₁ ?>>= complete    (p₂ _)  y∈p₂x
complete (p₁ !>>= p₂)           (x∈p₁ >>= y∈p₂x)   = complete p₁ x∈p₁ !>>= complete (♭ (p₂ _)) y∈p₂x

------------------------------------------------------------------------
-- A lemma

-- A simple cast lemma.

cast∈ : ∀ {Tok e R} {p p′ : Parser Tok e R} {x x′ s s′} →
        x ≡ x′ → p ≡ p′ → s ≡ s′ → x ∈ p · s → x′ ∈ p′ · s′
cast∈ P.refl P.refl P.refl x∈ = x∈

------------------------------------------------------------------------
-- A variant of the semantics

-- The statement x ⊕ s₂ ∈ p · s means that there is some s₁ such that
-- s ≡ s₁ ++ s₂ and x ∈ p · s₁. This variant of the semantics is
-- perhaps harder to understand, but sometimes easier to work with
-- (and it is proved equivalent to the semantics above).

infix 4 _⊕_∈_·_

data _⊕_∈_·_ {Tok} : ∀ {R e} → R → List Tok →
                     Parser Tok e R → List Tok → Set1 where
  return : ∀ {R} {x : R} {s} → x ⊕ s ∈ return x · s
  token  : ∀ {x s} → x ⊕ s ∈ token · x ∷ s
  ∣ˡ     : ∀ {R x e₁ e₂ s s₁}
             {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
           (x∈p₁ : x ⊕ s₁ ∈ p₁ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
  ∣ʳ     : ∀ {R x e₂ s s₁} e₁
             {p₁ : Parser Tok e₁ R} {p₂ : Parser Tok e₂ R}
           (x∈p₂ : x ⊕ s₁ ∈ p₂ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
  _?>>=_ : ∀ {R₁ R₂ x y e₂ s s₁ s₂}
             {p₁ : Parser Tok true R₁} {p₂ : R₁ → Parser Tok e₂ R₂}
           (x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ p₂ x · s₁) →
           y ⊕ s₂ ∈ p₁ ?>>= p₂ · s
  _!>>=_ : ∀ {R₁ R₂ x y} {e₂ : R₁ → Bool} {s s₁ s₂}
             {p₁ : Parser Tok false R₁}
             {p₂ : (x : R₁) → ∞ (Parser Tok (e₂ x) R₂)}
           (x∈p₁ : x ⊕ s₁ ∈ p₁ · s) (y∈p₂x : y ⊕ s₂ ∈ ♭ (p₂ x) · s₁) →
           y ⊕ s₂ ∈ p₁ !>>= p₂ · s

-- The definition is sound and complete with respect to the one above.

⊕-sound′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
           x ⊕ s₂ ∈ p · s → ∃ λ s₁ → (s ≡ s₁ ++ s₂) × (x ∈ p · s₁)
⊕-sound′ return            = ([]    , P.refl , return)
⊕-sound′ {x = x} token     = ([ x ] , P.refl , token)
⊕-sound′ (∣ˡ x∈p₁)         with ⊕-sound′ x∈p₁
⊕-sound′ (∣ˡ x∈p₁)         | (s₁ , P.refl , x∈p₁′) = (s₁ , P.refl , ∣ˡ    x∈p₁′)
⊕-sound′ (∣ʳ e₁ x∈p₁)      with ⊕-sound′ x∈p₁
⊕-sound′ (∣ʳ e₁ x∈p₁)      | (s₁ , P.refl , x∈p₁′) = (s₁ , P.refl , ∣ʳ e₁ x∈p₁′)
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ ?>>= y∈p₂x) | (s₁ , P.refl , x∈p₁′) | (s₂ , P.refl , y∈p₂x′) =
                             (s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _)
                                       , x∈p₁′ ?>>= y∈p₂x′)
⊕-sound′ (x∈p₁ !>>= y∈p₂x) with ⊕-sound′ x∈p₁ | ⊕-sound′ y∈p₂x
⊕-sound′ (x∈p₁ !>>= y∈p₂x) | (s₁ , P.refl , x∈p₁′) | (s₂ , P.refl , y∈p₂x′) =
                             (s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _)
                                       , x∈p₁′ !>>= y∈p₂x′)

⊕-sound : ∀ {Tok R e x s} {p : Parser Tok e R} →
          x ⊕ [] ∈ p · s → x ∈ p · s
⊕-sound x∈p with ⊕-sound′ x∈p
⊕-sound x∈p | (s , P.refl , x∈p′) with s ++ [] | proj₂ LM.identity s
⊕-sound x∈p | (s , P.refl , x∈p′) | .s | P.refl = x∈p′

extend : ∀ {Tok R e x s s′ s″} {p : Parser Tok e R} →
         x ⊕ s′ ∈ p · s → x ⊕ s′ ++ s″ ∈ p · s ++ s″
extend return            = return
extend token             = token
extend (∣ˡ x∈p₁)         = ∣ˡ    (extend x∈p₁)
extend (∣ʳ e₁ x∈p₂)      = ∣ʳ e₁ (extend x∈p₂)
extend (x∈p₁ ?>>= y∈p₂x) = extend x∈p₁ ?>>= extend y∈p₂x
extend (x∈p₁ !>>= y∈p₂x) = extend x∈p₁ !>>= extend y∈p₂x

⊕-complete : ∀ {Tok R e x s} {p : Parser Tok e R} →
             x ∈ p · s → x ⊕ [] ∈ p · s
⊕-complete return            = return
⊕-complete token             = token
⊕-complete (∣ˡ x∈p₁)         = ∣ˡ    (⊕-complete x∈p₁)
⊕-complete (∣ʳ e₁ x∈p₂)      = ∣ʳ e₁ (⊕-complete x∈p₂)
⊕-complete (x∈p₁ ?>>= y∈p₂x) = extend (⊕-complete x∈p₁) ?>>=
                                       ⊕-complete y∈p₂x
⊕-complete (x∈p₁ !>>= y∈p₂x) = extend (⊕-complete x∈p₁) !>>=
                                       ⊕-complete y∈p₂x

⊕-complete′ : ∀ {Tok R e x s₂ s} {p : Parser Tok e R} →
              (∃ λ s₁ → s ≡ s₁ ++ s₂ × x ∈ p · s₁) →
              x ⊕ s₂ ∈ p · s
⊕-complete′ (s₁ , P.refl , x∈p) = extend (⊕-complete x∈p)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- Interpretation of signature arities
module SOAS.Syntax.Arguments {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Families.Core {T}

open import Data.List.Base using ([] ; _∷_ ; List)
open import Data.Product
open import Data.Unit

-- List of arities as a product of terms in extended contexts
Arg : List (Ctx × T) → Familyₛ → Family
Arg []             𝒳 Γ = ⊤
Arg ((Θ , τ) ∷ []) 𝒳 Γ = 𝒳 τ (Θ ∔ Γ)
Arg ((Θ , τ) ∷ as) 𝒳 Γ = 𝒳 τ (Θ ∔ Γ) × Arg as 𝒳 Γ

-- Functorial action and laws
Arg₁ : {𝒳 𝒴 : Familyₛ} (as : List (Ctx × T))
     → (𝒳 ⇾̣ 𝒴) → Arg as 𝒳 ⇾ Arg as 𝒴
Arg₁ [] f tt = tt
Arg₁ ((Θ , τ) ∷ []) f t = f t
Arg₁ ((Θ , τ) ∷ (Θ′ , τ′) ∷ as) f (t , ts) = (f t) , (Arg₁ ((Θ′ , τ′) ∷ as) f ts)

Arg-id : {𝒳 : Familyₛ}{Γ : Ctx}(as : List (Ctx × T))(ts : Arg as 𝒳 Γ)
       → Arg₁ as id ts ≡ ts
Arg-id [] ts = refl
Arg-id (x ∷ []) t = refl
Arg-id (x ∷ y ∷ ys) (t , ts) = cong (_ ,_) (Arg-id (y ∷ ys) ts)

Arg-∘ : {𝒳 𝒴 𝒵 : Familyₛ}{Γ : Ctx}(as : List (Ctx × T))
      → {f : 𝒳 ⇾̣ 𝒴}{g : 𝒴 ⇾̣ 𝒵}
      → (ts : Arg as 𝒳 Γ)
      → Arg₁ as (g ∘ f) ts
      ≡ Arg₁ as g (Arg₁ as f ts)
Arg-∘ [] ts = refl
Arg-∘ (x ∷ []) t = refl
Arg-∘ (x ∷ y ∷ ys) (t , ts) = cong (_ ,_) (Arg-∘ (y ∷ ys) ts)

Arg-resp : {𝒳 𝒴 : Familyₛ}{Γ : Ctx}(as : List (Ctx × T))
         → {f g : 𝒳 ⇾̣ 𝒴}
         → ({τ : T}{Δ : Ctx}(x : 𝒳 τ Δ) → f x ≡ g x)
         → (ts : Arg as 𝒳 Γ)
         → Arg₁ as f ts ≡ Arg₁ as g ts
Arg-resp [] p ts = refl
Arg-resp (x ∷ []) p t = p t
Arg-resp (x ∷ y ∷ ys) p (t , ts) = cong₂ _,_ (p t) (Arg-resp (y ∷ ys) p ts)

ArgF : List (Ctx × T) → Functor 𝔽amiliesₛ 𝔽amilies
ArgF as = record
  { F₀ = Arg as
  ; F₁ = Arg₁ as
  ; identity = Arg-id as _
  ; homomorphism = Arg-∘ as _
  ; F-resp-≈ = λ p → Arg-resp as (λ _ → p) _
  }

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
------------------------------------------------------------------------
-- Definitions of functions that generate list or vector
------------------------------------------------------------------------

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

module Math.Combinatorics.VecFunction where

-- agda-stdlib
open import Data.List
open import Data.List.NonEmpty as NE using (List⁺)
open import Data.Nat
import Data.Nat.Properties as ℕₚ
open import Data.Product as Prod using (_×_; _,_)
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

-- agda-combinatorics
import Math.Combinatorics.ListFunction as ListFun

module _ {a} {A : Set a} where

  applyEach : ∀ {n} → (A → A) → Vec A n → Vec (Vec A n) n
  applyEach f []       = []
  applyEach f (x ∷ xs) = (f x ∷ xs) ∷ Vec.map (x ∷_) (applyEach f xs)

module _ {a} {A : Set a} where
  -- combinations
  combinations : ∀ k → List A → List (Vec A k)
  combinations 0       xs       = [ [] ]
  combinations (suc k) []       = []
  combinations (suc k) (x ∷ xs) =
    map (x ∷_) (combinations k xs) ++ combinations (suc k) xs

  combinationsWithComplement : ∀ m {n} → Vec A (m + n) →
                               List (Vec A m × Vec A n)
  combinationsWithComplement 0                 xs       = [ [] , xs ]
  combinationsWithComplement m@(suc _) {0}     xs       =
    [ subst (Vec A) (ℕₚ.+-identityʳ m) xs , [] ]
  combinationsWithComplement (suc m)   {suc n} (x ∷ xs) =
    map (Prod.map₁ (x ∷_)) (combinationsWithComplement m xs) ++
    map (Prod.map₂ (x ∷_)) (combinationsWithComplement (suc m) xs′)
      where xs′ = subst (Vec A) (ℕₚ.+-suc m n) xs

  splits₂ : ∀ {n} → Vec A n → Vec (List A × List A) (1 + n)
  splits₂ []           = ([] , []) ∷ []
  splits₂ xxs@(x ∷ xs) = ([] , Vec.toList xxs) ∷
                         Vec.map (Prod.map₁ (x ∷_)) (splits₂ xs)

  splits : ∀ k → List A → List (Vec (List A) k)
  splits 0             xs = []
  splits 1             xs = [ xs ∷ [] ]
  splits (suc (suc k)) xs = concatMap f (splits (suc k) xs)
    where
    f : Vec (List A) (suc k) → List (Vec (List A) (suc (suc k)))
    f (ys ∷ yss) =
      map (λ { (as , bs) → as ∷ bs ∷ yss }) (ListFun.splits₂ ys)

  splits⁺₂ : ∀ {n} → Vec A (1 + n) → Vec (List⁺ A × List⁺ A) n
  splits⁺₂ (x ∷ [])     = []
  splits⁺₂ (x ∷ y ∷ xs) =
    (x NE.∷ [] , y NE.∷ Vec.toList xs) ∷
    Vec.map (Prod.map₁ (x NE.∷⁺_)) (splits⁺₂ (y ∷ xs))

  splits⁺ : ∀ k → List⁺ A → List (Vec (List⁺ A) k)
  splits⁺ 0             xs = []
  splits⁺ 1             xs = [ xs ∷ [] ]
  splits⁺ (suc (suc k)) xs = concatMap f (splits⁺ (suc k) xs)
    where
    f : Vec (List⁺ A) (suc k) → List (Vec (List⁺ A) (suc (suc k)))
    f (ys ∷ yss) =
      map (λ { (as , bs) → as ∷ bs ∷ yss }) (ListFun.splits⁺₂ ys)

  partitions : ∀ k → List A → List (Vec (List A) k)
  partitions 0       []       = [ [] ]
  partitions 0       (x ∷ xs) = []
  partitions (suc k) []       = []
  partitions (suc k) (x ∷ xs) =
    map ([ x ] ∷_) (partitions k xs) ++
    concatMap (Vec.toList ∘ applyEach (x ∷_)) (partitions (suc k) xs)


text:
module ListAppend where

open import Prelude

append : forall {A} -> List A -> List A -> List A
append xs ys = {!!}

appendP1 : forall {x l l'} -> append (cons x l) l' == cons x (append l l')
appendP1 = refl

appendP2 : forall {l} -> append nil l == l
appendP2 = refl

max_stars_repo_name: carlostome/martin

max_issues_repo_name: carlostome/martin

max_forks_repo_name: carlostome/martin


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

module Lists.Definition where

data List {a : _} (A : Set a) : Set a where
  [] : List A
  _::_ : (x : A) (xs : List A) → List A
infixr 10 _::_
{-# BUILTIN LIST List #-}

[_] : {a : _} {A : Set a} → (a : A) → List A
[ a ] = a :: []

_++_ : {a : _} {A : Set a} → List A → List A → List A
[] ++ m = m
(x :: l) ++ m = x :: (l ++ m)


text:
record ⊤ : Set where
  no-eta-equality
  constructor tt

data D : ⊤ → Set where
  d : (x : ⊤) → D x

test : (g : D tt) → Set
test (d tt) = ⊤

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Function.Fiber where

open import Level
open import Data.Sigma.Base
open import Path
open import Cubical.Foundations.Everything using (fiber) public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

module AKS.Nat.WellFounded where

open import AKS.Nat.Base using (ℕ; _+_; _∸_; _≤_; _<_; lte)
open ℕ
open import AKS.Nat.Properties using (+-identityʳ; +-suc; ∸-mono-<ˡ; ∸-mono-<ʳ; suc-injective)

data Acc {A : Set} (_≺_ : A → A → Set) (bound : A) : Set where
  acc : (∀ {lower : A} → lower ≺ bound → Acc _≺_ lower)
      → Acc _≺_ bound

subrelation
    : ∀ {A : Set} {B : Set}
        {_≺₁_ : A → A → Set}
        {_≺₂_ : B → B → Set}
        {f : B → A}
        {n : B}
    → (∀ {x y} → x ≺₂ y → f x ≺₁ f y)
    → Acc _≺₁_ (f n)
    → Acc _≺₂_ n
subrelation ≺₂⇒≺₁ (acc down) =
  acc λ x≺₂n → subrelation ≺₂⇒≺₁ (down (≺₂⇒≺₁ x≺₂n))

data _≤ⁱ_ : ℕ → ℕ → Set where
  ≤-same : ∀ {n} → n ≤ⁱ n
  ≤-step : ∀ {n m} → n ≤ⁱ m → n ≤ⁱ suc m

_<ⁱ_ : ℕ → ℕ → Set
n <ⁱ m = suc n ≤ⁱ m

<⇒<ⁱ : ∀ {n m} → n < m → n <ⁱ m
<⇒<ⁱ {n} {m} (lte zero refl) rewrite +-identityʳ n = ≤-same
<⇒<ⁱ {n} {m} (lte (suc k) refl) = ≤-step (<⇒<ⁱ (lte k (sym (+-suc n k))))

<-well-founded : ∀ {n} → Acc _<_ n
<-well-founded {n} = wf₁ n
  where
  wf₁ : ∀ t → Acc _<_ t
  wf₂ : ∀ t b → b <ⁱ t → Acc _<_ b
  wf₁ t = acc λ {b} b<t → wf₂ t b (<⇒<ⁱ b<t)
  wf₂ (suc t) b ≤-same = wf₁ t
  wf₂ (suc t) b (≤-step b<ⁱt) = wf₂ t b b<ⁱt

record [_,_] (low : ℕ) (high : ℕ) : Set where
  inductive
  constructor acc
  field
    downward : ∀ {mid} → low ≤ mid → mid < high → [ low , mid ]
    upward : ∀ {mid} → low < mid → mid ≤ high → [ mid , high ]

binary-search : ∀ {n m} → [ n , m ]
binary-search {n} {m} = loop n m <-well-founded
  where
  loop : ∀ low high → Acc _<_ (high ∸ low) → [ low , high ]
  loop low high (acc next) = acc
    (λ {mid} low≤mid mid<high → loop low mid (next {mid ∸ low} (∸-mono-<ˡ low≤mid mid<high)))
    (λ {mid} low<mid mid≤high → loop mid high (next {high ∸ mid} (∸-mono-<ʳ mid≤high low<mid)))

open import AKS.Unsafe using (trustMe)

record Interval : Set where
  constructor [_,_∣_]
  field
    inf : ℕ
    sup : ℕ
    inf≤sup : inf ≤ sup
open Interval

width : Interval → ℕ
width i = sup i ∸ inf i

data _⊂_ (i₁ : Interval) (i₂ : Interval) : Set where
  downward : inf i₂ ≤ inf i₁ → sup i₁ < sup i₂ → i₁ ⊂ i₂
  upward : inf i₂ < inf i₁ → sup i₁ ≤ sup i₂ → i₁ ⊂ i₂

∸-monoˡ-< : ∀ {l₁ h₁ l₂ h₂} → l₁ ≤ h₁ → l₂ ≤ h₂ → l₂ ≤ l₁ → h₁ < h₂ → h₁ ∸ l₁ < h₂ ∸ l₂
∸-monoˡ-< {l₁} {h₁} {l₂} {h₂} l₁≤h₁ l₂≤h₂ l₂≤l₁ h₁<h₂ = lte ((h₂ ∸ l₂) ∸ suc (h₁ ∸ l₁)) trustMe -- TODO: EVIL

∸-monoʳ-< : ∀ {l₁ h₁ l₂ h₂} → l₁ ≤ h₁ → l₂ ≤ h₂ → l₂ < l₁ → h₁ ≤ h₂ → h₁ ∸ l₁ < h₂ ∸ l₂
∸-monoʳ-< {l₁} {h₁} {l₂} {h₂} l₁≤h₁ l₂≤h₂ l₂<l₁ h₁≤h₂ = lte ((h₂ ∸ l₂) ∸ suc (h₁ ∸ l₁)) trustMe

⊂⇒< : ∀ {i₁ i₂} → i₁ ⊂ i₂ → width i₁ < width i₂
⊂⇒< {[ inf-i₁ , sup-i₁ ∣ inf-i₁≤sup-i₁ ]} {[ inf-i₂ , sup-i₂ ∣ inf-i₂≤sup-i₂ ]} (downward inf-i₂≤inf-i₁ sup-i₁<sup-i₂)
  = ∸-monoˡ-< inf-i₁≤sup-i₁ inf-i₂≤sup-i₂ inf-i₂≤inf-i₁ sup-i₁<sup-i₂
⊂⇒< {[ inf-i₁ , sup-i₁ ∣ inf-i₁≤sup-i₁ ]} {[ inf-i₂ , sup-i₂ ∣ inf-i₂≤sup-i₂ ]} (upward inf-i₂<inf-i₁ sup-i₁≤sup-i₂)
  = ∸-monoʳ-< inf-i₁≤sup-i₁ inf-i₂≤sup-i₂ inf-i₂<inf-i₁ sup-i₁≤sup-i₂

⊂-well-founded : ∀ {i} → Acc _⊂_ i
⊂-well-founded = subrelation ⊂⇒< <-well-founded

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
{-# OPTIONS --without-K #-}
module NTypes where

open import Equivalence
open import FunExt
open import GroupoidStructure
open import NTypes.Contractible
open import PathOperations
open import Transport
open import Types

isProp : ∀ {a} → Set a → Set _
isProp A = (x y : A) → x ≡ y

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

set→id-prop : ∀ {a} {A : Set a} →
  isSet A → {x y : A} → isProp (x ≡ y)
set→id-prop A-set = A-set _ _

id-prop→set : ∀ {a} {A : Set a} →
  ({x y : A} → isProp (x ≡ y)) → isSet A
id-prop→set f _ _ = f

prop-eq : ∀ {a b} {A : Set a} {B : Set b} → A ≃ B → isProp A → isProp B
prop-eq (f , (g , α) , (h , β)) A-prop x y =
  tr id
    ( ap (λ z → z ≡ f (g y)) (α x)
    · ap (λ z → x ≡ z)       (α y)
    )
    (ap f (A-prop (g x) (g y)))

-- Levels.
is-[_-2]-type : ℕ → ∀ {a} → Set a → Set a
is-[ n -2]-type = ind (λ _ → Set _ → Set _)
  (λ _ r A → (x y : A) → r (x ≡ y))
  isContr
  n

-- isProp and is-(-1)-type.
prop→-1-type : ∀ {a} {A : Set a} →
  isProp A → is-[ 1 -2]-type A
prop→-1-type {A = A} A-prop x y
  = A-prop x y
  , path
  where
  split-path : {x y : A} (p : x ≡ y) →
    A-prop x y ≡ p · A-prop y y
  split-path = J
    (λ x y p → A-prop x y ≡ p · A-prop y y)
    (λ _ → refl) _ _

  path : {x y : A} (p : x ≡ y) → A-prop x y ≡ p
  path = J
    (λ x y p → A-prop x y ≡ p)
    (λ x → split-path (A-prop x x ⁻¹) · p⁻¹·p (A-prop x x))
    _ _

-1-type→prop : ∀ {a} {A : Set a} →
  is-[ 1 -2]-type A → isProp A
-1-type→prop A-1 x y = π₁ (A-1 x y)

-- isSet and is-0-type.
set→0-type : ∀ {a} {A : Set a} →
  isSet A → is-[ 2 -2]-type A
set→0-type A-set x y = prop→-1-type (A-set x y)

0-type→set : ∀ {a} {A : Set a} →
  is-[ 2 -2]-type A → isSet A
0-type→set A0 x y = -1-type→prop (A0 x y)

-- Cumulativity.
n-type-suc : ∀ n {a} {A : Set a} →
  is-[ n -2]-type A → is-[ suc n -2]-type A
n-type-suc n = ind
  (λ n → ∀ {A} → is-[ n -2]-type A → is-[ suc n -2]-type A)
  (λ _ r h x y → r (h x y))
  (λ     h → prop→-1-type λ x y → π₂ h x ⁻¹ · π₂ h y)
  n

-- From lectures.
prop→set : ∀ {a} {A : Set a} →
  isProp A → isSet A
prop→set A-prop x y p q = lem p · lem q ⁻¹
  where
  g : _
  g = A-prop x

  lem : (p : x ≡ y) → p ≡ g x ⁻¹ · g y
  lem p
    = id·p p ⁻¹
    · ap (λ z → z · p)
      (p⁻¹·p (g x)) ⁻¹
    · p·q·r (g x ⁻¹) (g x) p ⁻¹
    · ap (λ z → g x ⁻¹ · z)
      ( tr-post x p (g x) ⁻¹
      · apd g p
      )

isProp-is-prop : ∀ {a} {A : Set a} →
  isProp (isProp A)
isProp-is-prop f g =
  funext λ x →
  funext λ y →
  prop→set f _ _ (f x y) (g x y)

isSet-is-prop : ∀ {a} {A : Set a} →
  isProp (isSet A)
isSet-is-prop f g =
  funext λ x →
  funext λ y →
  funext λ p →
  funext λ q →
  prop→set (f x y) _ _ (f x y p q) (g x y p q)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
module InstanceMeta where

data Bool : Set where
  true false : Bool

data Maybe (A : Set) : Set where
  Nothing : Maybe A
  Just : A → Maybe A

record Eq (A : Set) : Set where
  constructor eq
  field
    _==_ : A → A → Bool
open Eq {{...}} public

instance
  eq-Bool : Eq Bool
  eq-Bool = eq aux  where

    aux : Bool → Bool → Bool
    aux true true = true
    aux false false = true
    aux _ _ = false

  eq-Maybe : {A : Set} {{_ : Eq A}} → Eq (Maybe A)
  eq-Maybe {A} = eq aux  where

    aux : Maybe A → Maybe A → Bool
    aux Nothing Nothing = true
    aux (Just y) (Just z) = (y == z)
    aux _ _ = false

test : Bool
test = {!!} == {!!}
-- This should not loop, only produce unsolved metas

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- The alternating bit protocol (ABP) is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the ABP following the
-- formalization in Dybjer and Sander (1989).

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

module FOTC.Program.ABP.CorrectnessProofATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP using ( not-Bool )
open import FOTC.Data.Stream.Type
open import FOTC.Data.Stream.Equality.PropertiesATP
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Lemma1ATP
open import FOTC.Program.ABP.Lemma2ATP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- Main theorem.
abpCorrect : ∀ {b os₁ os₂ is} → Bit b → Fair os₁ → Fair os₂ → Stream is →
             is ≈ abpTransfer b os₁ os₂ is
abpCorrect {b} {os₁} {os₂} {is} Bb Fos₁ Fos₂ Sis = ≈-coind B h₁ h₂
  where
  postulate h₁ : ∀ {ks ls} → B ks ls →
                 ∃[ k' ] ∃[ ks' ] ∃[ ls' ]
                   ks ≡ k' ∷ ks' ∧ ls ≡ k' ∷ ls' ∧ B ks' ls'
  {-# ATP prove h₁ lemma₁ lemma₂ not-Bool #-}

  postulate h₂ : B is (abpTransfer b os₁ os₂ is)
  {-# ATP prove h₂ #-}

------------------------------------------------------------------------------
-- abpTransfer produces a Stream.
postulate
  abpTransfer-Stream : ∀ {b os₁ os₂ is} →
                       Bit b →
                       Fair os₁ →
                       Fair os₂ →
                       Stream is →
                       Stream (abpTransfer b os₁ os₂ is)
{-# ATP prove abpTransfer-Stream ≈→Stream₂ abpCorrect #-}

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Sessions.Semantics.Expr where

open import Prelude
open import Data.Fin

open import Relation.Unary.PredicateTransformer hiding (_⊔_)
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Reader

open import Sessions.Syntax.Types
open import Sessions.Syntax.Values
open import Sessions.Syntax.Expr
open import Sessions.Semantics.Commands
open import Sessions.Semantics.Runtime

open import Relation.Ternary.Separation.Construct.List Type
open import Relation.Ternary.Separation.Monad.Free Cmd δ
  hiding (⟪_⟫)
open import Relation.Ternary.Separation.Monad.Error

open ErrorTrans Free {{monad = free-monad}} public
open ReaderTransformer id-morph Val (ErrorT Free) {{error-monad}}
  renaming (Reader to M)
  public
open Monads using (Monad; str; _&_)
open Monad reader-monad

mutual
  eval⊸ : ∀ {Γ} → ℕ → Exp (a ⊸ b) Γ → ∀[ Val a ⇒ⱼ M Γ [] (Val b) ]
  eval⊸ n e v = do
    (clos e env) ×⟨ σ₂ ⟩ v ← ►eval n e & v
    empty                  ← append (cons (v ×⟨ ⊎-comm σ₂ ⟩ env))
    ►eval n e

  ►eval : ℕ → Exp a Γ → ε[ M Γ [] (Val a) ]
  app (►eval zero    e) _ _ = partial (pure (inj₁ err))
  ►eval (suc n) e = eval n e

  ⟪_⟫ : ∀ {Γ Φ} → (c : Cmd Φ) → M Γ Γ (δ c) Φ
  app (⟪_⟫ c) (inj E) σ =
    partial (impure (c ×⟨ σ ⟩
      wand λ r σ' → pure (inj₂ (r ×⟨ ⊎-comm σ' ⟩ E))))

  eval : ℕ → Exp a Γ → ε[ M Γ [] (Val a) ]

  eval n unit = do
    return tt

  eval n (var refl) = do
    (v :⟨ σ ⟩: nil) ← ask
    case ⊎-id⁻ʳ σ of λ where
      refl → return v

  eval n (lam a e) = do
    env ← ask
    return (clos e env)

  eval n (ap (f ×⟨ Γ≺ ⟩ e)) = do
    v ← frame (⊎-comm Γ≺) (►eval n e)
    eval⊸ n f v

  eval n (pairs (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    v₁ ← frame Γ≺ (►eval n e₁)
    v₂⋆v₂ ← ►eval n e₂ & v₁
    return (pairs (✴-swap v₂⋆v₂))

  eval n (letunit (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    tt ← frame Γ≺ (►eval n e₁)
    ►eval n e₂

  eval n (letpair (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    pairs (v₁ ×⟨ σ ⟩ v₂) ← frame Γ≺ (►eval n e₁)
    empty ← prepend (cons (v₁ ×⟨ σ ⟩ singleton v₂))
    ►eval n e₂

  eval n (send (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    v₁ ← frame Γ≺ (►eval n e₁)
    cref φ ×⟨ σ ⟩ v₁ ← ►eval n e₂ & v₁
    φ' ← ⟪ send (φ ×⟨ σ ⟩ v₁) ⟫
    return (cref φ')

  eval n (recv e) = do
    cref φ ← ►eval n e
    v ×⟨ σ ⟩ φ' ← ⟪ receive φ ⟫
    return (pairs (cref φ' ×⟨ ⊎-comm σ ⟩ v))

  eval n (mkchan α) = do
    φₗ ×⟨ σ ⟩ φᵣ ← ⟪ mkchan α  ⟫
    return (pairs (cref φₗ ×⟨ σ ⟩ cref φᵣ))

  eval n (fork e) = do
    clos body env ← ►eval n e
    empty ←
      ⟪ fork (app (runReader (cons (tt ×⟨ ⊎-idˡ ⟩ env))) (►eval n body) ⊎-idʳ) ⟫
    return tt

  eval n (terminate e) = do
    cref φ ← ►eval n e
    empty ← ⟪ close φ ⟫
    return tt


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

module Categories.Category.Instance.Properties.Setoids where

open import Level
open import Relation.Binary using (Setoid; module Setoid; Preorder)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
import Relation.Binary.Reasoning.Setoid as RS
open import Function.Equality using (Π)
open import Relation.Binary.Indexed.Heterogeneous using (_=[_]⇒_)
open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_)
import Relation.Binary.Construct.Symmetrize as Symmetrize
open Symmetrize hiding (setoid; trans; sym)
open import Data.Unit using (⊤; tt)

open import Categories.Category using (Category; _[_,_])
open import Categories.Functor
open import Categories.Category.Instance.Setoids
open import Categories.Diagram.Cocone
open import Categories.Category.Construction.Cocones hiding (Cocone)
open import Categories.Diagram.Cone
open import Categories.Category.Complete
open import Categories.Category.Cocomplete

Setoids-Cocomplete : (o ℓ e c ℓ′ : Level) → Cocomplete o ℓ e (Setoids (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′))
Setoids-Cocomplete o ℓ e c ℓ′ {J} F = record { initial = record
  { ⊥ = record
    { N = ⇛-Setoid
    ; coapex = record
      { ψ = λ j → record
        { _⟨$⟩_ = j ,_
        ; cong = λ i≈k → disorient (slish (J.id , identity i≈k))
        }
      ; commute = λ {X} X⇒Y x≈y → disorient (slash (X⇒Y , cong (F₁ X⇒Y) (Setoid.sym (F₀ X) x≈y)))
      }
    }
  ; ! = λ {A} → record
    { arr = record
      { _⟨$⟩_ = to-coapex A
      ; cong = λ eq → minimal ⇛-preorder (Cocone.N A) (to-coapex A) (coapex-cong A) eq
      }
    ; commute = λ {X} x≈y → cong (Coapex.ψ (Cocone.coapex A) X) x≈y
    }
  ; !-unique = λ {A} cocone⇒ x⇛y → Setoid.trans (Cocone.N A)
               (Setoid.sym (Cocone.N A) (Cocone⇒.commute cocone⇒ (refl (F₀ _))))
               (cong (Cocone⇒.arr cocone⇒) x⇛y)
  } }
  where
    open Setoid
    open Π
    open Functor F
    D = Cocones F
    module J = Category J
    C = Setoids _ _
    setoid : J.Obj → Category.Obj C
    setoid j = F₀ j
    module S (j : J.Obj) = Setoid (setoid j)
    open S using () renaming (_≈_ to _[_≈_])
    vertex-carrier = Σ[ j ∈ J.Obj ] Carrier (setoid j)
    _⇛_ : (x y : vertex-carrier) → Set _
    (X , x) ⇛ (Y , y) = Σ[ f ∈ J [ X , Y ] ] ( Y [ (F₁ f ⟨$⟩ x) ≈ y ])
    ⇛-preorder : Preorder _ _ _
    ⇛-preorder = record
      { Carrier = vertex-carrier
      ; _≈_ = _≡_
      ; _∼_ = _⇛_
      ; isPreorder = record
        { isEquivalence = ≡.isEquivalence
        ; reflexive = λ { {i , Fi} {.i , .Fi} ≡.refl → J.id , Functor.identity F (refl (F₀ i))}
        ; trans = λ { {i , Fi} {j , Fj} {k , Fk} i≈j j≈k → proj₁ j≈k J.∘ proj₁ i≈j ,
          let S = F₀ k in
          let open RS S in begin
          F₁ (proj₁ j≈k J.∘ proj₁ i≈j) ⟨$⟩ Fi       ≈⟨ homomorphism (refl (F₀ i)) ⟩
          F₁ (proj₁ j≈k) ⟨$⟩ (F₁ (proj₁ i≈j) ⟨$⟩ Fi) ≈⟨ cong (F₁ (proj₁ j≈k)) (proj₂ i≈j)  ⟩
          F₁ (proj₁ j≈k) ⟨$⟩ Fj                     ≈⟨ proj₂ j≈k ⟩
          Fk ∎}
        }
      }
    ⇛-Setoid : Setoid (o ⊔ c) (o ⊔ ℓ ⊔ c ⊔ ℓ′)
    ⇛-Setoid = Symmetrize.setoid ⇛-preorder
    to-coapex : (A : Cocone F) → vertex-carrier → Carrier (Cocone.N A)
    to-coapex A (j , Fj) = Cocone.ψ A j ⟨$⟩ Fj
    coapex-cong : (A : Cocone F) → _⇛_ =[ to-coapex A ]⇒ (_≈_ (Cocone.N A))
    coapex-cong A {X , x} {Y , y} (f , fx≈y) = Setoid.trans A.N
        (Setoid.sym A.N (A.commute f (refl (F₀ X))))
        (cong (A.ψ Y) fx≈y)
      where module A = Cocone A

Setoids-Complete : (o ℓ e c ℓ′ : Level) → Complete o ℓ e (Setoids (ℓ′ ⊔ ℓ ⊔ o) (o ⊔ ℓ′))
Setoids-Complete o ℓ e c ℓ′ {J} F = record { terminal = record
  { ⊤ = record
    { N = record
      { Carrier = Σ
          ((j : Category.Obj J) → Setoid.Carrier (F₀ j))
          (λ P → ∀ {X Y} (f : J [ X , Y ]) → Setoid._≈_ (F₀ Y) (F₁ f Π.⟨$⟩ P X) (P Y))
      ; _≈_ = λ f g → ∀ (j : Category.Obj J) → Setoid._≈_ (F₀ j) (proj₁ f j) (proj₁ g j)
      ; isEquivalence = record
        { refl = λ j → Setoid.refl (F₀ j)
        ; sym = λ a≈b j → Setoid.sym (F₀ j) (a≈b j)
        ; trans = λ a≈b b≈c j → Setoid.trans (F₀ j) (a≈b j) (b≈c j)
        }
      }
    ;  apex = record
      { ψ = λ j → record
        { _⟨$⟩_ = λ x → proj₁ x j
        ; cong = λ x → x j
        }
      ; commute = λ {X} {Y} X⇒Y {x} {y} f≈g → Setoid.trans (F₀ Y) (proj₂ x X⇒Y) (f≈g Y)
      }
    }
  ; ! = λ {A} → record
    { arr = record
      { _⟨$⟩_ = λ x → (λ j → ψ A j Π.⟨$⟩ x) , λ {X} {Y} f → commute A f (Setoid.refl (N A))
      ; cong = λ a≈b j → Π.cong (ψ A j) a≈b
      }
    ; commute = λ {j} x≈y → Π.cong (ψ A j) x≈y
    }
  ; !-unique = λ {A} f x≈y j → Setoid.sym (F₀ j) (Cone⇒.commute f (Setoid.sym (N A) x≈y))
  } }
  where
    open Functor F
    S : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
    S = Setoids c ℓ
    open Category S
    open Cone

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module 040-monoid where

-- We need semigroups.

open import 030-semigroup

-- The next useful structure is a monoid, which is a semigroup with
-- (left and right) identity element.

record Monoid
  {M : Set}
  (_==_ : M -> M -> Set)
  (_*_ : M -> M -> M)
  (id : M)
  : Set1 where

  field
    semigroup : SemiGroup _==_ _*_
    r*id==r : ∀ {r} -> (r * id) == r
    id*r==r : ∀ {r} -> (id * r) == r

  open SemiGroup semigroup public

  -- Should we define powers? We cannot do this yet: we need natural
  -- numbers first, which we do not have yet.

  -- Let us prove some facts.

  -- Identity can occur on either side of the equality.
  r==r*id : ∀ {r} -> r == (r * id)
  r==r*id = symm r*id==r
  r==id*r : ∀ {r} -> r == (id * r)
  r==id*r = symm id*r==r

  -- The identity element is unique (both left and right).
  idleftunique : ∀ {r} -> (∀ {s} -> (r * s) == s) -> (r == id)
  idleftunique r*s==s = trans r==r*id r*s==s

  idrightunique : ∀ {r} -> (∀ {s} -> (s * r) == s) -> (r == id)
  idrightunique s*r==s = trans r==id*r s*r==s

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
open import Agda.Builtin.Coinduction
open import Agda.Builtin.Equality

record Reveal_·_is_ {A : Set} {B : A → Set}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set where
  constructor [_]
  field eq : f x ≡ y

inspect : {A : Set} {B : A → Set}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

infix 4 _≈_

data _≈_ {A} : Stream A → Stream A → Set where
  _∷_ : ∀ {x y xs ys}
        (x≡ : x ≡ y) (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ y ∷ ys

map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

map₂ : ∀ {A B} → (A → B) → Stream A → Stream B
map₂ f (x ∷ xs) with ♭ xs
map₂ f (x ∷ xs) | y ∷ ys = f x ∷ ♯ (f y ∷ ♯ map₂ f (♭ ys))

map≈map₂ : ∀ {A B} →
           (f : A → B) → (xs : Stream A) → map f xs ≈ map₂ f xs
map≈map₂ {A} f (x ∷ xs) with ♭ xs | inspect ♭ xs
map≈map₂ {A} f (x ∷ xs) | y ∷ ys | [ eq ] = refl ∷ ♯ helper eq
  where
  map-f-y∷ys = _

  helper : ∀ {xs} → xs ≡ y ∷ ys → map f xs ≈ map-f-y∷ys
  helper refl = refl ∷ ♯ map≈map₂ f (♭ ys)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
import      Lvl
open import Structure.Setoid
open import Type

module Automaton.Deterministic where

open import Data.List renaming (∅ to ε ; _⊰_ to _·_)
open import Data.List.Setoid
open import Data.List.Functions using (postpend ; _++_)
open import Data.List.Proofs
open import Functional
open import Logic
open import Sets.ExtensionalPredicateSet using (PredSet ; intro ; _∈_ ; _∋_ ; ⊶ ; [∋]-binaryRelator)
import      Structure.Function.Names as Names
open import Structure.Operator
open import Structure.Relator.Properties

-- According to http://www.cse.chalmers.se/edu/course/TMV027/lec5.pdf

private variable ℓₚ ℓₛ ℓₑ₁ ℓₐ ℓₑ₂ : Lvl.Level

module _
  {ℓₚ}
  (State : Type{ℓₛ}) ⦃ equiv-state : Equiv{ℓₑ₁}(State) ⦄
  (Alphabet : Type{ℓₐ}) ⦃ equiv-alphabet : Equiv{ℓₑ₂}(Alphabet) ⦄
  where

  -- Deterministic Automata
  -- `State`      (Q)  is the set of states.
  -- `Alphabet`   (Σ)  is the set of symbols/the alphabet.
  -- `transition` (δ)  is the transition function.
  -- `start`      (q₀) is the start state.
  -- `Final`      (F)  is the subset of State which are the final/accepting states.
  record Deterministic : Type{ℓₛ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓₐ Lvl.⊔ Lvl.𝐒(ℓₚ)} where
    constructor deterministic
    field
      transition : State → Alphabet → State
      ⦃ transition-binaryOperator ⦄ : BinaryOperator(transition)
      start      : State
      Final      : PredSet{ℓₚ}(State)

    Word = List(Alphabet)

    -- Chained transition using a word (list of characters).
    wordTransition : State → Word → State
    wordTransition initialState ε       = initialState
    wordTransition initialState (a · l) = wordTransition (transition initialState a) l

    module LetterNotation where
      Q  = State
      Σ  = Alphabet
      δ  = transition
      δ̂  = wordTransition
      q₀ = start
      F  = Final

    -- A word is accepted by the automaton when it can transition from the start state to a final state.
    AcceptsWord : Word → Stmt
    AcceptsWord = (_∈ Final) ∘ wordTransition start

    transitionedAutomaton : Alphabet → Deterministic
    transition (transitionedAutomaton _) = transition
    start      (transitionedAutomaton c) = transition start c
    Final      (transitionedAutomaton _) = Final

    wordTransitionedAutomaton : Word → Deterministic
    transition (wordTransitionedAutomaton _) = transition
    start      (wordTransitionedAutomaton w) = wordTransition start w
    Final      (wordTransitionedAutomaton _) = Final

module _
  {State : Type{ℓₛ}} ⦃ equiv-state : Equiv{ℓₑ₁}(State) ⦄
  {Alphabet : Type{ℓₐ}} ⦃ equiv-alphabet : Equiv{ℓₑ₂}(Alphabet) ⦄
  {d : Deterministic{ℓₚ = ℓₚ}(State)(Alphabet)}
  where

  open import Data.List.Equiv
  open import Structure.Operator.Properties
  open import Syntax.Transitivity

  open Deterministic(d)

  instance
    wordTransition-binaryOperator : BinaryOperator(wordTransition)
    wordTransition-binaryOperator = intro p where
      p : Names.Congruence₂(wordTransition)
      p {x₂ = ε}       {y₂ = ε}       xy1 xy2 = xy1
      p {x₂ = c₁ · w₁} {y₂ = c₂ · w₂} xy1 xy2 = p{x₂ = w₁}{y₂ = w₂} (congruence₂(transition) xy1 ([⊰]-generalized-cancellationᵣ xy2)) ([⊰]-generalized-cancellationₗ xy2)

  wordTransition-postpend : ∀{s}{w}{a} → ((wordTransition s (postpend a w)) ≡ transition (wordTransition s w) a)
  wordTransition-postpend {s}{ε}    {a} = reflexivity(_≡_) {x = transition s a}
  wordTransition-postpend {s}{x · w}{a} = wordTransition-postpend {transition s x}{w}{a}

  -- Note: ((swap ∘ wordTransition) d (w₁ ++ w₂) ⊜ (swap ∘ wordTransition) d w₂ ∘ (swap ∘ wordTransition) d w₁)
  wordTransition-[++] : ∀{s}{w₁ w₂} → (wordTransition s (w₁ ++ w₂) ≡ (wordTransition (wordTransition s w₁) w₂))
  wordTransition-[++] {s = s} {w₁ = w₁} {w₂ = ε} =
    wordTransition s (w₁ ++ ε)             🝖[ _≡_ ]-[ congruence₂ᵣ(wordTransition)(s) (identityᵣ(_++_)(ε) {w₁}) ]
    wordTransition s w₁                    🝖[ _≡_ ]-[]
    wordTransition (wordTransition s w₁) ε 🝖-end
  wordTransition-[++] {s = s} {w₁ = w₁} {w₂ = c₂ · w₂} =
    wordTransition s (w₁ ++ (c₂ · w₂))                      🝖[ _≡_ ]-[ congruence₂ᵣ(wordTransition)(s) ([++]-middle-prepend-postpend{l₁ = w₁}) ]-sym
    wordTransition s (postpend c₂ w₁ ++ w₂)                 🝖[ _≡_ ]-[ wordTransition-[++] {s = s}{w₁ = postpend c₂ w₁}{w₂ = w₂} ]
    wordTransition (wordTransition s (postpend c₂ w₁)) w₂   🝖[ _≡_ ]-[ congruence₂ₗ(wordTransition)(w₂) (wordTransition-postpend{s = s}{w = w₁}) ]
    wordTransition (transition (wordTransition s w₁) c₂) w₂ 🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module PiFrac.AuxLemmas where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import PiFrac.Syntax
open import PiFrac.Opsem

Lemma₁ : ∀ {A B C D v v' κ κ'} {c : A ↔ B} {c' : C ↔ D}
       → ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c' ∣ v' ∣ κ' ］
       → (A ≡ C × B ≡ D)
Lemma₁ ↦₁ = refl , refl
Lemma₁ ↦₂ = refl , refl
Lemma₁ ↦η = refl , refl
Lemma₁ ↦ε₁ = refl , refl

Lemma₂ : ∀ {A B v v' κ κ'} {c c' : A ↔ B}
       → ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c' ∣ v' ∣ κ' ］
       → c ≡ c' × κ ≡ κ'
Lemma₂ ↦₁ = refl , refl
Lemma₂ ↦₂ = refl , refl
Lemma₂ ↦η = refl , refl
Lemma₂ ↦ε₁ = refl , refl

Lemma₃ : ∀ {A B v v' κ} {c : A ↔ B}
       → (r : ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ v' ∣ κ ］)
       → base c ⊎ dual c ⊎ A ≡ B
Lemma₃ (↦₁ {b = b}) = inj₁ b
Lemma₃ ↦₂ = inj₂ (inj₂ refl)
Lemma₃ ↦η = inj₂ (inj₁ tt)
Lemma₃ ↦ε₁ = inj₂ (inj₁ tt)

Lemma₄ : ∀ {A v v' κ} {c : A ↔ A}
       → (r : ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ v' ∣ κ ］)
       → base c ⊎ c ≡ id↔
Lemma₄ {c = swap₊} ↦₁ = inj₁ tt
Lemma₄ {c = swap⋆} ↦₁ = inj₁ tt
Lemma₄ ↦₂ = inj₂ refl

Lemma₅ : ∀ {A B v v' b κ} {c : A ↔ B ×ᵤ 𝟙/ b}
        → (r : ⟨ c ∣ v ∣ κ ⟩ ↦ ［ c ∣ v' ∣ κ ］)
        → base c ⊎ (b , ↻) ≡ v' ⊎ ¬ (dual c)
Lemma₅ (↦₁ {b = b}) = inj₁ b
Lemma₅ ↦₂ = inj₂ (inj₂ (λ ()))
Lemma₅ ↦η = inj₂ (inj₁ refl)

Lemma₆ : ∀ {A v v' κ} → v ≢ v' → ∄[ st' ] (st' ↦ ［ ηₓ {A} v ∣ v' , ↻ ∣ κ ］)
Lemma₆ neq (⟨ _ ∣ v ∣ _ ⟩ , r) with Lemma₁ r
... | refl , refl with Lemma₂ r
... | refl , refl with Lemma₅ r
... | inj₂ (inj₁ refl) = neq refl
... | inj₂ (inj₂ nd) = nd tt


text:
------------------------------------------------------------------------------
-- Testing anonymous module
------------------------------------------------------------------------------

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

-- No top-level module

postulate
  D   : Set
  _≡_ : D → D → Set

postulate foo : ∀ t → t ≡ t
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Tactic.Nat.Subtract.Lemmas where

open import Prelude
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Container.Bag
open import Tactic.Nat.Simpl
open import Prelude.Nat.Properties
open import Prelude.List.Properties
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Auto
open import Tactic.Nat.Simpl

open import Tactic.Nat.Subtract.Exp

sub-cancel : (a : Nat) → a - a ≡ 0
sub-cancel zero = refl
sub-cancel (suc a) = sub-cancel a

sub-add-r : (a b c : Nat) → a - (b + c) ≡ a - b - c
sub-add-r  a       zero    c      = refl
sub-add-r zero    (suc b)  zero   = refl
sub-add-r zero    (suc b) (suc c) = refl
sub-add-r (suc a) (suc b)  c      = sub-add-r a b c

lem-sub-zero : (a b c : Nat) → b + c ≡ a → c ≡ a - b
lem-sub-zero ._  zero   c refl = refl
lem-sub-zero ._ (suc b) c refl = lem-sub-zero _ b c refl

lem-zero-sub : (a b c : Nat) → b ≡ a + c → 0 ≡ a - b
lem-zero-sub  zero   ._  zero   refl = refl
lem-zero-sub  zero   ._ (suc c) refl = refl
lem-zero-sub (suc a) ._  c      refl = lem-zero-sub a _ c refl

lem-sub : (a b u v : Nat) → b + u ≡ a + v → u - v ≡ a - b
lem-sub  zero    zero   u ._ refl = sub-cancel u
lem-sub  zero   (suc b) u ._ refl = sym $ lem-zero-sub u (suc b + u) (suc b) auto
lem-sub (suc a)  zero  ._  v refl = sym $ lem-sub-zero (suc a + v) v (suc a) auto
lem-sub (suc a) (suc b) u  v eq   = lem-sub a b u v (suc-inj eq)

sub-mul-distr-l : (a b c : Nat) → (a - b) * c ≡ a * c - b * c
sub-mul-distr-l zero b c = (_* c) $≡ lem-zero-sub 0 b b refl ʳ⟨≡⟩ lem-zero-sub 0 (b * c) (b * c) refl
sub-mul-distr-l (suc a) zero c = refl
sub-mul-distr-l (suc a) (suc b) c =
  sub-mul-distr-l a b c ⟨≡⟩
  lem-sub (suc a * c) (suc b * c) (a * c) (b * c) auto

sub-mul-distr-r : (a b c : Nat) → a * (b - c) ≡ a * b - a * c
sub-mul-distr-r a b c =
  auto ⟨≡⟩ sub-mul-distr-l b c a
       ⟨≡⟩ cong₂ _-_ (mul-commute b a) (mul-commute c a)

-- The evaluator that doesn't generate x * 1 + 0 is the same as the
-- one that does.

lem-eval-sns-sn : ∀ n ρ → ⟦ n ⟧sns ρ ≡ ⟦ n ⟧sn ρ

private
  lem-eval-sns-sn-t : ∀ t ρ → ⟦ t ⟧sts ρ ≡ ⟦ t ⟧st ρ
  lem-eval-sns-sn-a : ∀ a ρ → ⟦ a ⟧sas ρ ≡ ⟦ a ⟧sa ρ

  lem-eval-sns-sn-a (var x) ρ = refl
  lem-eval-sns-sn-a (a ⟨-⟩ b) ρ = _-_ $≡ lem-eval-sns-sn a ρ *≡ lem-eval-sns-sn b ρ

  lem-eval-sns-sn-t []          ρ = refl
  lem-eval-sns-sn-t (x ∷ [])    ρ = lem-eval-sns-sn-a x ρ ⟨≡⟩ auto
  lem-eval-sns-sn-t (x ∷ y ∷ t) ρ = _*_ $≡ lem-eval-sns-sn-a x ρ *≡ lem-eval-sns-sn-t (y ∷ t) ρ

lem-eval-sns-sn []                 ρ = refl
lem-eval-sns-sn ((k , t) ∷ [])     ρ = _*_ k $≡ lem-eval-sns-sn-t t ρ ⟨≡⟩ auto
lem-eval-sns-sn ((k , t) ∷ t₁ ∷ n) ρ = _+_ $≡ (_*_ k $≡ lem-eval-sns-sn-t t ρ)
                                         *≡ lem-eval-sns-sn (t₁ ∷ n) ρ

-- The evaluation that the termination checker lets us write is the
-- same as the one we want to write.

private
  lem-eval-sn-n-t : ∀ t ρ → ⟦ t ⟧st ρ ≡ productR (map (atomEnv ρ) t)
  lem-eval-sn-n-t [] ρ = refl
  lem-eval-sn-n-t (x ∷ t) ρ = (⟦ x ⟧sa ρ *_) $≡ lem-eval-sn-n-t t ρ

lem-eval-sn-n   : ∀ n ρ → ⟦ n ⟧sn ρ ≡ ⟦ n ⟧n (atomEnv ρ)
lem-eval-sn-n []            ρ = refl
lem-eval-sn-n ((k , t) ∷ n) ρ = _+_ $≡ (_*_ k $≡ lem-eval-sn-n-t t ρ) *≡ lem-eval-sn-n n ρ

private
  lem-env : ∀ ρ x → atomEnvS ρ x ≡ atomEnv ρ x
  lem-env ρ (var x) = refl
  lem-env ρ (a ⟨-⟩ b) = _-_ $≡ lem-eval-sns-sn a ρ *≡ lem-eval-sns-sn b ρ

-- Combining the above equalities.

lem-eval-sn-nS : ∀ n ρ → ⟦ n ⟧sn ρ ≡ ⟦ n ⟧n (atomEnvS ρ)
lem-eval-sn-nS n ρ = lem-eval-sn-n n ρ ⟨≡⟩ʳ lem-eval-env (atomEnvS ρ) (atomEnv ρ) (lem-env ρ) n

lem-eval-sns-nS : ∀ n ρ → ⟦ n ⟧sns ρ ≡ ⟦ n ⟧n (atomEnvS ρ)
lem-eval-sns-nS n ρ = lem-eval-sns-sn n ρ ⟨≡⟩ lem-eval-sn-nS n ρ

lem-eval-sns-ns : ∀ n ρ → ⟦ n ⟧sns ρ ≡ ⟦ n ⟧ns (atomEnvS ρ)
lem-eval-sns-ns n ρ = lem-eval-sns-nS n ρ ⟨≡⟩ʳ ns-sound n (atomEnvS ρ)

⟨-⟩-sound′ : ∀ a b ρ → ⟦ a -nf′ b ⟧n (atomEnv ρ) ≡ ⟦ a ⟧n (atomEnv ρ) - ⟦ b ⟧n (atomEnv ρ)
⟨-⟩-sound′ a b ρ with cancel a b | λ i j → cancel-complete′ i j a b (atomEnv ρ)
⟨-⟩-sound′ a b ρ | d      , []     | complete =
  let u = ⟦ a ⟧n (atomEnv ρ)
      v = ⟦ b ⟧n (atomEnv ρ)
      k = ⟦ d ⟧n (atomEnv ρ) in
  lem-sub-zero u v k (complete v u auto ⟨≡⟩ auto)
⟨-⟩-sound′ a b ρ | []     , d ∷ ds | complete =
  let u = ⟦ a      ⟧n (atomEnv ρ)
      v = ⟦ b      ⟧n (atomEnv ρ)
      k = ⟦ d ∷ ds ⟧n (atomEnv ρ) in
  lem-zero-sub u v k (auto ⟨≡⟩ complete v u auto)
⟨-⟩-sound′ a b ρ | u ∷ us , v ∷ vs | complete =
  let eval = λ x → ⟦ x ⟧n (atomEnv ρ) in
  (⟦ u ∷ us ⟧sn ρ - ⟦ v ∷ vs ⟧sn ρ) * 1 + 0 + 0
    ≡⟨ auto ⟩
  ⟦ u ∷ us ⟧sn ρ - ⟦ v ∷ vs ⟧sn ρ
    ≡⟨ cong₂ _-_ (lem-eval-sn-n (u ∷ us) ρ) (lem-eval-sn-n (v ∷ vs) ρ) ⟩
  eval (u ∷ us) - eval (v ∷ vs)
    ≡⟨ lem-sub (eval a) (eval b) (eval (u ∷ us)) (eval (v ∷ vs)) (complete (eval b) (eval a) auto) ⟩
  eval a - eval b ∎

⟨-⟩-sound : ∀ a b ρ → ⟦ a -nf b ⟧n (atomEnv ρ) ≡ ⟦ a ⟧n (atomEnv ρ) - ⟦ b ⟧n (atomEnv ρ)
⟨-⟩-sound a b ρ with is-subtraction a
⟨-⟩-sound a b ρ  | no     = ⟨-⟩-sound′ a b ρ
⟨-⟩-sound ._ c ρ | a ⟨-⟩ b =
  let eval = λ x → ⟦ x ⟧n (atomEnv ρ) in
  ⟨-⟩-sound′ a (b +nf c) ρ ⟨≡⟩
  (eval a -_) $≡ ⟨+⟩-sound b c (atomEnv ρ) ⟨≡⟩
  sub-add-r (eval a) (eval b) (eval c) ⟨≡⟩
  (_- eval c) $≡ (_-_ $≡ lem-eval-sn-n a ρ *≡ lem-eval-sn-n b ρ) ʳ⟨≡⟩
  (_- eval c) $≡ auto

⟨*⟩-sound₁ : ∀ a b ρ → ⟦ a *nf₁ b ⟧n (atomEnv ρ) ≡ ⟦ a ⟧n (atomEnv ρ) * ⟦ b ⟧n (atomEnv ρ)

private
  sound-mul-ktm′ : ∀ t a ρ → ⟦ t *ktm′ a ⟧n (atomEnv ρ) ≡ ⟦ t ⟧t (atomEnv ρ) * ⟦ a ⟧n (atomEnv ρ)

  sound-mul-tm : ∀ s t ρ → ⟦ s *tm t ⟧n (atomEnv ρ) ≡ ⟦ s ⟧t (atomEnv ρ) * ⟦ t ⟧t (atomEnv ρ)
  sound-mul-tm s t ρ with is-subtraction-tm t
  sound-mul-tm (x , a) (y , b) ρ | no =
    follows-from (x * y *_ $≡ map-merge a b (atomEnv ρ))
  sound-mul-tm s ._ ρ | a ⟨-⟩ b =
    let eval  x = ⟦ x ⟧n (atomEnv ρ)
        evalt x = ⟦ x ⟧t (atomEnv ρ) in
    ⟨-⟩-sound (s *ktm′ a) (s *ktm′ b) ρ ⟨≡⟩
    _-_ $≡ sound-mul-ktm′ s a ρ *≡ sound-mul-ktm′ s b ρ ⟨≡⟩
    sub-mul-distr-r (evalt s) (eval a) (eval b) ʳ⟨≡⟩
    (evalt s *_) $≡ (_-_ $≡ lem-eval-sn-n a ρ *≡ lem-eval-sn-n b ρ) ʳ⟨≡⟩
    auto

  sound-mul-ktm′ t [] ρ = auto
  sound-mul-ktm′ t (x ∷ a) ρ =
    let eval  x = ⟦ x ⟧n (atomEnv ρ)
        evalt x = ⟦ x ⟧t (atomEnv ρ) in
    ⟨+⟩-sound (t *tm x) (t *ktm′ a) (atomEnv ρ) ⟨≡⟩
    _+_ $≡ sound-mul-tm t x ρ *≡ sound-mul-ktm′ t a ρ ⟨≡⟩ʳ
    mul-distr-l (evalt t) (evalt x) (eval a)

  sound-mul-ktm : ∀ t a ρ → ⟦ t *ktm a ⟧n (atomEnv ρ) ≡ ⟦ t ⟧t (atomEnv ρ) * ⟦ a ⟧n (atomEnv ρ)
  sound-mul-ktm t a ρ with is-subtraction-tm t
  sound-mul-ktm t  a ρ | no = sound-mul-ktm′ t a ρ
  sound-mul-ktm ._ c ρ | a ⟨-⟩ b =
    let eval x = ⟦ x ⟧n (atomEnv ρ) in
    ⟨-⟩-sound (a *nf₁ c) (b *nf₁ c) ρ ⟨≡⟩
    _-_ $≡ ⟨*⟩-sound₁ a c ρ *≡ ⟨*⟩-sound₁ b c ρ ⟨≡⟩
    sub-mul-distr-l (eval a) (eval b) (eval c) ʳ⟨≡⟩
    (_* eval c) $≡ (_-_ $≡ lem-eval-sn-n a ρ *≡ lem-eval-sn-n b ρ) ʳ⟨≡⟩
    auto

⟨*⟩-sound₁ [] b ρ = refl
⟨*⟩-sound₁ (t ∷ a) b ρ =
  let eval x = ⟦ x ⟧n (atomEnv ρ)
      evalt x = ⟦ x ⟧t (atomEnv ρ) in
  ⟨+⟩-sound (t *ktm b) (a *nf₁ b) (atomEnv ρ) ⟨≡⟩
  _+_ $≡ sound-mul-ktm t b ρ *≡ ⟨*⟩-sound₁ a b ρ ⟨≡⟩ʳ
  mul-distr-r (evalt t) (eval a) (eval b)

sound-sub : ∀ e ρ → ⟦ e ⟧se ρ ≡ ⟦ normSub e ⟧sn ρ
sound-sub (var x) ρ = auto
sound-sub (lit 0) ρ = refl
sound-sub (lit (suc n)) ρ = auto
sound-sub (e ⟨+⟩ e₁) ρ =
  cong₂ _+_ (sound-sub e  ρ ⟨≡⟩ lem-eval-sn-n (normSub e)  ρ)
            (sound-sub e₁ ρ ⟨≡⟩ lem-eval-sn-n (normSub e₁) ρ) ⟨≡⟩
  ⟨+⟩-sound (normSub e) (normSub e₁) (atomEnv ρ) ʳ⟨≡⟩ʳ
  lem-eval-sn-n (normSub (e ⟨+⟩ e₁)) ρ
sound-sub (e ⟨*⟩ e₁) ρ =
  cong₂ _*_ (sound-sub e  ρ ⟨≡⟩ lem-eval-sn-n (normSub e)  ρ)
            (sound-sub e₁ ρ ⟨≡⟩ lem-eval-sn-n (normSub e₁) ρ) ⟨≡⟩
  ⟨*⟩-sound₁ (normSub e) (normSub e₁) ρ ʳ⟨≡⟩ʳ
  lem-eval-sn-n (normSub (e ⟨*⟩ e₁)) ρ
sound-sub (e ⟨-⟩ e₁) ρ =
  cong₂ _-_ (sound-sub e  ρ ⟨≡⟩ lem-eval-sn-n (normSub e)  ρ)
            (sound-sub e₁ ρ ⟨≡⟩ lem-eval-sn-n (normSub e₁) ρ) ⟨≡⟩
  ⟨-⟩-sound (normSub e) (normSub e₁) ρ ʳ⟨≡⟩ʳ
  lem-eval-sn-n (normSub (e ⟨-⟩ e₁)) ρ

liftNFSubEq : ∀ e₁ e₂ ρ → ⟦ normSub e₁ ⟧sn ρ ≡ ⟦ normSub e₂ ⟧sn ρ → ⟦ e₁ ⟧se ρ ≡ ⟦ e₂ ⟧se ρ
liftNFSubEq e₁ e₂ ρ eq = eraseEquality $ sound-sub e₁ ρ ⟨≡⟩ eq ⟨≡⟩ʳ sound-sub e₂ ρ

unliftNFSubEq : ∀ e₁ e₂ ρ → ⟦ e₁ ⟧se ρ ≡ ⟦ e₂ ⟧se ρ → ⟦ normSub e₁ ⟧sn ρ ≡ ⟦ normSub e₂ ⟧sn ρ
unliftNFSubEq e₁ e₂ ρ eq = eraseEquality $ sound-sub e₁ ρ ʳ⟨≡⟩ eq ⟨≡⟩ sound-sub e₂ ρ

SubExpEq : SubExp → SubExp → Env Var → Set
SubExpEq e₁ e₂ ρ = ⟦ e₁ ⟧se ρ ≡ ⟦ e₂ ⟧se ρ

CancelSubEq : SubExp → SubExp → Env Var → Set
CancelSubEq e₁ e₂ ρ = NFEqS (cancel (normSub e₁) (normSub e₂)) (atomEnvS ρ)

simplifySubEq : ∀ e₁ e₂ (ρ : Env Var) → CancelSubEq e₁ e₂ ρ → SubExpEq e₁ e₂ ρ
simplifySubEq e₁ e₂ ρ H = liftNFSubEq e₁ e₂ ρ $
  lem-eval-sn-nS (normSub e₁) ρ ⟨≡⟩
  cancel-sound (normSub e₁) (normSub e₂) (atomEnvS ρ) H ⟨≡⟩ʳ
  lem-eval-sn-nS (normSub e₂) ρ

complicateSubEq : ∀ e₁ e₂ ρ → SubExpEq e₁ e₂ ρ → CancelSubEq e₁ e₂ ρ
complicateSubEq e₁ e₂ ρ H =
  cancel-complete (normSub e₁) (normSub e₂) (atomEnvS ρ) $
  lem-eval-sn-nS (normSub e₁) ρ ʳ⟨≡⟩
  unliftNFSubEq e₁ e₂ ρ H ⟨≡⟩
  lem-eval-sn-nS (normSub e₂) ρ

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function using (id; _∘_)

open import Cubical.Data.Unit
open import Cubical.Data.Empty

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Relation.Unary

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ : Level
    A : Type ℓ

------------------------------------------------------------------------
-- Special sets

Empty∅ : Empty {A = A} ∅
Empty∅ _ ()

UniversalU : Π[ U {A = A} ]
UniversalU _ = tt

∁∅≡U : ∁ ∅ ≡ U {A = A}
∁∅≡U = ⇔toPath _ _ ((λ _ → tt) , λ _ ())

∁U≡∅ : ∁ U ≡ ∅ {A = A}
∁U≡∅ = ⇔toPath _ _ ((λ f → f tt) , λ ())

------------------------------------------------------------------------
-- Propositions

module _ (P : Pred A ℓ₁) (Q : Pred A ℓ₂) where

  isProp⊆ : isProp (P ⊆ Q)
  isProp⊆ = isPropImplicitΠ λ _ → isPropΠ λ _ → isProp[ Q ] _

  isProp⊂ : isProp (P ⊂ Q)
  isProp⊂ = isProp× isProp⊆ (isPropΠ λ _ → isProp⊥)

  isProp⇔ : isProp (P ⇔ Q)
  isProp⇔ = isProp× isProp⊆ (isPropImplicitΠ λ _ → isPropΠ λ _ → isProp[ P ] _)

module _ (P : Pred A ℓ) where

  isPropEmpty : isProp (Empty P)
  isPropEmpty = isPropΠ2 λ _ _ → isProp⊥

  isPropSatisfiable : isProp ∃⟨ P ⟩
  isPropSatisfiable = squash

  isPropUniversal : isProp Π[ P ]
  isPropUniversal = isPropΠ isProp[ P ]

------------------------------------------------------------------------
-- Predicate equivalence

⇔-reflexive : (P : Pred A ℓ) → P ⇔ P
⇔-reflexive P = id , id

⇔-symmetric : (P : Pred A ℓ₁) (Q : Pred A ℓ₂) → P ⇔ Q → Q ⇔ P
⇔-symmetric P Q (x , y) = (y , x)

⇔-transitive : (P : Pred A ℓ₁) (Q : Pred A ℓ₂) (R : Pred A ℓ₃) →
                  P ⇔ Q → Q ⇔ R → P ⇔ R
⇔-transitive P Q R (x , y) (w , z) = w ∘ x , y ∘ z


text:
module EffectUtil where

open import Data.List
open import Data.List.All
open import Data.List.Any
open import Level
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function
open import Category.Monad
open import Data.Product
-- open import EffectUtil

open import Membership-equality hiding (_⊆_; set)

infix 3 _⊆_

-- Sublist without re-ordering, to be improved later...
data _⊆_ {a}{A : Set a} : List A → List A → Set a where
  []   : ∀ {ys} → [] ⊆ ys
  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
  skip : ∀ {x xs ys} → xs ⊆ ys → xs ⊆ x ∷ ys

singleton-⊆ : ∀ {a} {A : Set a} {x : A} {xs : List A} → x ∈ xs → [ x ] ⊆ xs
singleton-⊆ (here refl) = keep []
singleton-⊆ (there mem) = skip (singleton-⊆ mem)

reflexive-⊆ : ∀ {a} {A : Set a} {xs : List A} → xs ⊆ xs
reflexive-⊆ {xs = []} = []
reflexive-⊆ {xs = x ∷ xs} = keep reflexive-⊆

max_stars_repo_name: Zalastax/singly-typed-actors

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
-- Andreas, 2016-04-26 flight home from AIM XXIII

module _ where

module M (A : Set) where
  record R : Set where
    field f : A

module H {A} = M A

open M using (R)
open M.R using (f)  -- f : {A : Set} → R A → A
open H.R using (f)  -- f : {A : Set} → R A → A

r : ∀ A (a : A) → R A
f (r A a) = a

test : ∀ A (a : A) → A
test A a = f (r A a)

test' : ∀ A (a : A) → A
test' A a = f {A = _} (r A a)


text:
module Numeral.PositiveInteger.Oper where

open import Numeral.PositiveInteger

infixl 10010 _+_
infixl 10020 _⋅_
infixl 10030 _^_

-- Addition
_+_ : ℕ₊ → ℕ₊ → ℕ₊
x + 𝟏    = 𝐒(x)
x + 𝐒(y) = 𝐒(x + y)

-- Multiplication
_⋅_ : ℕ₊ → ℕ₊ → ℕ₊
x ⋅ 𝟏    = x
x ⋅ 𝐒(y) = x + (x ⋅ y)

-- Exponentiation
_^_ : ℕ₊ → ℕ₊ → ℕ₊
x ^ 𝟏    = x
x ^ 𝐒(y) = x ⋅ (x ^ y)

-- Factorial
_! : ℕ₊ → ℕ₊
𝟏 !    = 𝟏
𝐒(x) ! = 𝐒(x) ⋅ (x !)

open import Data.Option
open import Data.Option.Functions
-- Truncated subtraction
_−₀_ : ℕ₊ → ℕ₊ → Option(ℕ₊)
𝟏    −₀ _    = None
𝐒(x) −₀ 𝟏    = Some x
𝐒(x) −₀ 𝐒(y) = x −₀ y

open import Data.Boolean
open import Type
_≤?_ : ℕ₊ → ℕ₊ → Bool
𝟏    ≤? _    = 𝑇
𝐒(x) ≤? 𝟏    = 𝐹
𝐒(x) ≤? 𝐒(y) = x ≤? y


text:
------------------------------------------------------------------------
-- Examples for modalities
------------------------------------------------------------------------

module CTL.ModalityExamples where

open import Library

open import FStream.Containers
open import FStream.Core

open import CTL.Modalities

readDouble : ⟦ ReaderC ℕ ⟧ ℕ
readDouble = fmap (_* 2) ask

readSuc : ⟦ ReaderC ℕ ⟧ ℕ
readSuc = fmap (suc) ask

alwaysPos : (n : ℕ) → runReader readSuc n > 0
alwaysPos n = s≤s z≤n

alwaysPosC : □ (_> 0) readSuc
alwaysPosC = λ p → s≤s z≤n

sometimes3 : ◇ (_≡ 3) readSuc
sometimes3 = suc (suc zero) , refl

sometimes5 : ◇ (_≡ 5) readSuc
sometimes5 = suc (suc (suc (suc zero))) , refl

-- It is always the case that constantly readSuc outputs ℕ > 0,
-- regardless of the environment
always>0 : AG (map (_> 0) (constantly readSuc))
nowA (always>0 p) = alwaysPos p
laterA (always>0 p) = {!!}

{-nowA always>0 = λ p → s≤s z≤n
laterA always>0 = λ p → always>0
-}

{-
nowA always>0 p = s≤s z≤n
laterA always>0 p = always>0
-}

-- Sums all values in the reader-environment
sumFrom : ℕ → FStream (ReaderC ℕ) ℕ
proj₁ (inF (sumFrom n0)) = tt
head (proj₂ (inF (sumFrom n0)) n) = n0 + n
tail (proj₂ (inF (sumFrom n0)) n) = sumFrom (n0 + n)

sum : FStream (ReaderC ℕ) ℕ
sum = sumFrom 0

-- Eventually the sum is greater than 2
eventuallysometimes>2 : EF (map (_> 2) sum)
-- ... having 3 as input, this is of course the case after 1 step
eventuallysometimes>2 = ? --alreadyE (suc (suc (suc zero)) , s≤s (s≤s (s≤s z≤n)))

-- Always somehow the sum is greater than 2
alwaysSomehow>2 : ∀ {i} → EG {i} (map (_> 2) sum)
alwaysSomehow>2 = {!!}

{-proj₁ alwaysSomehow>2 = suc (suc (suc zero))
nowE' (proj₂ alwaysSomehow>2) = s≤s (s≤s (s≤s z≤n))
proj₁ (laterE' (proj₂ alwaysSomehow>2)) = zero
proj₂ (laterE' (proj₂ alwaysSomehow>2)) = {!   !}
-}

{-
nowE alwaysSomehow>2 = (ℕ.suc (ℕ.suc (ℕ.suc ℕ.zero)) , s≤s (s≤s (s≤s z≤n)))
laterE alwaysSomehow>2 = ℕ.zero , alwaysSomehow>2
-}

--

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.CommRings where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Powerset

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FiberedProduct
open import Cubical.Algebra.CommRing.Instances.Unit

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Limits.Limits

open import Cubical.HITs.PropositionalTruncation

open Category hiding (_∘_)
open isUnivalent
open CatIso
open Functor
open CommRingStr
open RingHoms
open IsRingHom

private
  variable
    ℓ ℓ' ℓ'' : Level

CommRingsCategory : Category (ℓ-suc ℓ) ℓ
ob CommRingsCategory                     = CommRing _
Hom[_,_] CommRingsCategory               = CommRingHom
id CommRingsCategory {R}                 = idCommRingHom R
_⋆_ CommRingsCategory {R} {S} {T}        = compCommRingHom R S T
⋆IdL CommRingsCategory {R} {S}           = compIdCommRingHom {R = R} {S}
⋆IdR CommRingsCategory {R} {S}           = idCompCommRingHom {R = R} {S}
⋆Assoc CommRingsCategory {R} {S} {T} {U} = compAssocCommRingHom {R = R} {S} {T} {U}
isSetHom CommRingsCategory               = isSetRingHom _ _

forgetfulFunctor : Functor CommRingsCategory (SET ℓ)
F-ob forgetfulFunctor R    = R .fst , CommRingStr.is-set (snd R)
F-hom forgetfulFunctor f x = f .fst x
F-id forgetfulFunctor      = funExt (λ _ → refl)
F-seq forgetfulFunctor f g = funExt (λ _ → refl)

open Iso

CommRingIsoIsoCatIso : {R S : CommRing ℓ} → Iso (CommRingIso R S) (CatIso CommRingsCategory R S)
mor (fun CommRingIsoIsoCatIso e) = (e .fst .fun) , (e .snd)
inv (fun (CommRingIsoIsoCatIso {R = R} {S}) e) =
    e .fst .inv
  , makeIsRingHom (sym (cong (e .fst .inv) (pres1 (e .snd))) ∙ e .fst .leftInv _)
                  (λ x y → let rem = e .fst .rightInv _
                                  ∙∙ (λ i → S .snd ._+_ (e .fst .rightInv x (~ i)) (e .fst .rightInv y (~ i)))
                                  ∙∙ sym (pres+ (e .snd) _ _)
                            in injCommRingIso {R = R} {S} e _ _ rem)
                  (λ x y → let rem = e .fst .rightInv _
                                  ∙∙ (λ i → S .snd ._·_ (e .fst .rightInv x (~ i)) (e .fst .rightInv y (~ i)))
                                  ∙∙ sym (pres· (e .snd) _ _)
                           in injCommRingIso {R = R} {S} e _ _ rem)
sec (fun CommRingIsoIsoCatIso e) = RingHom≡ (funExt (e .fst .rightInv))
ret (fun CommRingIsoIsoCatIso e) = RingHom≡ (funExt (e .fst .leftInv))
fun (fst (inv CommRingIsoIsoCatIso e)) = e .mor .fst
inv (fst (inv CommRingIsoIsoCatIso e)) = e .inv .fst
rightInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .sec i) x
leftInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .ret i) x
snd (inv CommRingIsoIsoCatIso e) = e .mor .snd
rightInv CommRingIsoIsoCatIso x = CatIso≡ _ _ (RingHom≡ refl) (RingHom≡ refl)
leftInv (CommRingIsoIsoCatIso {R = R} {S}) x =
  Σ≡Prop (λ x → isPropIsRingHom (CommRingStr→RingStr (R .snd))
                                (x .fun)
                                (CommRingStr→RingStr (S .snd)))
         (Iso≡Set (is-set (snd R)) (is-set (snd S)) _ _ (λ _ → refl) (λ _ → refl))

isUnivalentCommRingsCategory : ∀ {ℓ} → isUnivalent {ℓ = ℓ-suc ℓ} CommRingsCategory
univ isUnivalentCommRingsCategory R S = subst isEquiv (funExt rem) (≡≃CatIso .snd)
  where
  CommRingEquivIso≡ : Iso (CommRingEquiv R S) (R ≡ S)
  CommRingEquivIso≡ = equivToIso (CommRingPath R S)

  ≡≃CatIso : (R ≡ S) ≃ (CatIso CommRingsCategory R S)
  ≡≃CatIso = isoToEquiv (compIso (invIso CommRingEquivIso≡)
                                 (compIso (CommRingEquivIsoCommRingIso R S) CommRingIsoIsoCatIso))

  rem : ∀ p → ≡≃CatIso .fst p ≡ pathToIso p
  rem p = CatIso≡ _ _
                 (RingHom≡ (funExt (λ x → cong (transport (λ i → fst (p i))) (sym (transportRefl x)))))
                 (RingHom≡ (funExt (λ x → sym (transportRefl _))))

TerminalCommRing : Terminal {ℓ-suc ℓ-zero} CommRingsCategory
fst TerminalCommRing = UnitCommRing
fst (fst (snd TerminalCommRing y)) _ = tt*
snd (fst (snd TerminalCommRing y)) = makeIsRingHom refl (λ _ _ → refl) (λ _ _ → refl)
snd (snd TerminalCommRing y) f = RingHom≡ (funExt (λ _ → refl))

open Pullback

{-
   A x_C B -----> A
      |           |
      |           | α
      |           |
      V           V
      B --------> C
            β
-}
PullbackCommRingsCategory : Pullbacks {ℓ-suc ℓ} CommRingsCategory
pbOb (PullbackCommRingsCategory (cospan A C B α β))             = fiberedProduct A B C α β
pbPr₁ (PullbackCommRingsCategory (cospan A C B α β))            = fiberedProductPr₁ A B C α β
pbPr₂ (PullbackCommRingsCategory (cospan A C B α β))            = fiberedProductPr₂ A B C α β
pbCommutes (PullbackCommRingsCategory (cospan A C B α β))       = fiberedProductPr₁₂Commutes A B C α β
univProp (PullbackCommRingsCategory (cospan A C B α β)) {d = D} = fiberedProductUnivProp A B C α β D

-- General limits
module _ {ℓJ ℓJ' : Level} where

  open LimCone
  open Cone

  LimitsCommRingsCategory : Limits {ℓJ} {ℓJ'} CommRingsCategory
  fst (lim (LimitsCommRingsCategory J D)) =
    lim {J = J} (completeSET J (funcComp forgetfulFunctor D)) .fst
  0r (snd (lim (LimitsCommRingsCategory J D))) =
    cone (λ v _ → 0r (snd (F-ob D v)))
         (λ e → funExt (λ _ → F-hom D e .snd .pres0))
  1r (snd (lim (LimitsCommRingsCategory J D))) =
    cone (λ v _ → 1r (snd (F-ob D v)))
         (λ e → funExt (λ _ → F-hom D e .snd .pres1))
  _+_ (snd (lim (LimitsCommRingsCategory J D))) x y =
    cone (λ v _ → _+_ (snd (F-ob D v)) _ _)
         ( λ e → funExt (λ _ → F-hom D e .snd .pres+ _ _
         ∙ λ i → _+_ (snd (F-ob D _)) (coneOutCommutes x e i tt*) (coneOutCommutes y e i tt*)))
  _·_ (snd (lim (LimitsCommRingsCategory J D))) x y =
    cone (λ v _ → _·_ (snd (F-ob D v)) _ _)
         ( λ e → funExt (λ _ → F-hom D e .snd .pres· _ _
         ∙ λ i → _·_ (snd (F-ob D _)) (coneOutCommutes x e i tt*) (coneOutCommutes y e i tt*)))
  (- snd (lim (LimitsCommRingsCategory J D))) x =
    cone (λ v _ → -_ (snd (F-ob D v)) _)
         ( λ e → funExt (λ z → F-hom D e .snd .pres- _
         ∙ λ i → -_ (snd (F-ob D _)) (coneOutCommutes x e i tt*)))
  isCommRing (snd (lim (LimitsCommRingsCategory J D))) =
    makeIsCommRing
      (isSetCone (funcComp forgetfulFunctor D) (Unit* , _))
      (λ _ _ _ → cone≡ (λ v → funExt (λ _ → snd (F-ob D v) .+Assoc _ _ _)))
      (λ _ → cone≡ (λ v → funExt (λ _ → +Rid (snd (F-ob D v)) _)))
      (λ _ → cone≡ (λ v → funExt (λ _ → +Rinv (snd (F-ob D v)) _)))
      (λ _ _ → cone≡ (λ v → funExt (λ _ → snd (F-ob D v) .+Comm _ _)))
      (λ _ _ _ → cone≡ (λ v → funExt (λ _ → snd (F-ob D v) .·Assoc _ _ _)))
      (λ _ → cone≡ (λ v → funExt (λ _ → ·Rid (snd (F-ob D v)) _)))
      (λ _ _ _ → cone≡ (λ v → funExt (λ _ → ·Rdist+ (snd (F-ob D v)) _ _ _)))
      (λ _ _ → cone≡ (λ v → funExt (λ _ → snd (F-ob D v) .·Comm _ _)))
  fst (coneOut (limCone (LimitsCommRingsCategory J D)) v) =
    coneOut (limCone (completeSET J (funcComp forgetfulFunctor D))) v
  pres0 (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = refl
  pres1 (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = refl
  pres+ (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ _ → refl
  pres· (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ _ → refl
  pres- (snd (coneOut (limCone (LimitsCommRingsCategory J D)) v)) = λ _ → refl
  coneOutCommutes (limCone (LimitsCommRingsCategory J D)) e =
    RingHom≡ (coneOutCommutes (limCone (completeSET J (funcComp forgetfulFunctor D))) e)
  univProp (LimitsCommRingsCategory J D) c cc =
    uniqueExists
      ( (λ x → limArrow (completeSET J (funcComp forgetfulFunctor D))
                        (fst c , snd c .is-set)
                        (cone (λ v _ → coneOut cc v .fst x)
                              (λ e → funExt (λ _ → funExt⁻ (cong fst (coneOutCommutes cc e)) x))) x)
      , makeIsRingHom
          (cone≡ (λ v → funExt (λ _ → coneOut cc v .snd .pres1)))
          (λ x y → cone≡ (λ v → funExt (λ _ → coneOut cc v .snd .pres+ _ _)))
          (λ x y → cone≡ (λ v → funExt (λ _ → coneOut cc v .snd .pres· _ _))))
      (λ _ → RingHom≡ refl)
      (isPropIsConeMor cc (limCone (LimitsCommRingsCategory J D)))
      (λ a' x → Σ≡Prop (λ _ → isPropIsRingHom _ _ _)
                       (funExt (λ y → cone≡ λ v → funExt (λ _ → sym (funExt⁻ (cong fst (x v)) y)))))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module DualTail where

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Product
open import Data.Vec hiding (map)
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Direction
open import Extensionality
open import DualCoinductive

-- session types restricted to tail recursion
-- can be recognized by type of TChan constructor

data Type : Set
data SType (n : ℕ) : Set
data GType (n : ℕ) : Set

data Type where
  TUnit TInt : Type
  TPair : (t₁ t₂ : Type) → Type
  TChan : (s : SType 0) → Type

data SType n where
  gdd : (g : GType n) → SType n
  rec : (g : GType (suc n)) → SType n
  var : (x : Fin n) → SType n

data GType n where
  transmit : (d : Dir) (t : Type) (s : SType n) → GType n
  choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
  end : GType n

-- naive definition of duality for tail recursive session types
-- message types are ignored as they are closed

dualS : SType n → SType n
dualG : GType n → GType n

dualS (gdd g) = gdd (dualG g)
dualS (rec g) = rec (dualG g)
dualS (var x) = var x

dualG (transmit d t s) = transmit (dual-dir d) t (dualS s)
dualG (choice d m alt) = choice (dual-dir d) m (dualS ∘ alt)
dualG end = end

-- instead of unrolling and substituting, we maintain a stack of bodies of recursive types

data Stack : ℕ → Set where
  ε : Stack 0
  ⟪_,_⟫ : Stack n → GType (suc n) → Stack (suc n)

-- the dual of a stack

dual-stack : Stack n → Stack n
dual-stack ε = ε
dual-stack ⟪ σ , g ⟫ = ⟪ dual-stack σ , dualG g ⟫

-- obtain an entry from the stack
-- technically m = n - i, but we don't need to know

get : (i : Fin n) → Stack n → Σ ℕ λ m → Stack m × GType (suc m)
get 0F ⟪ σ , x ⟫ = _ , (σ , x)
get (suc i) ⟪ σ , x ⟫ = get i σ

-- relate a stack entry to the corresponding entry on the dual stack

get-dual-stack : (x : Fin n) (σ : Stack n) →
  get x (dual-stack σ) ≡ map id (map dual-stack dualG) (get x σ)
get-dual-stack 0F ⟪ σ , x ⟫ = refl
get-dual-stack (suc x) ⟪ σ , x₁ ⟫ = get-dual-stack x σ

-- mapping tail recursive session types to coinductive session types
-- relies on a stack to unfold variables on the fly

tail2coiT : Type → COI.Type
tail2coiS : Stack n → SType n → COI.SType
tail2coiG : Stack n → GType n → COI.STypeF COI.SType

tail2coiT TUnit = COI.TUnit
tail2coiT TInt = COI.TInt
tail2coiT (TPair t t₁) = COI.TPair (tail2coiT t) (tail2coiT t₁)
tail2coiT (TChan s) = COI.TChan (tail2coiS ε s)

COI.SType.force (tail2coiS σ (gdd g)) = tail2coiG σ g
COI.SType.force (tail2coiS σ (rec g)) = tail2coiG ⟪ σ , g ⟫ g
COI.SType.force (tail2coiS σ (var x))
  with get x σ
... | m , σ' , gxs = tail2coiG ⟪ σ' , gxs ⟫ gxs

tail2coiG σ (transmit d t s) = COI.transmit d (tail2coiT t) (tail2coiS σ s)
tail2coiG σ (choice d m alt) = COI.choice d m (tail2coiS σ ∘ alt)
tail2coiG σ end = COI.end

-- get coinductive bisimulation in scope

_≈_ = COI._≈_
_≈'_ = COI._≈'_

-- main proposition

dual-tailS : (σ : Stack n) (s : SType n) →
  COI.dual (tail2coiS σ s) ≈ tail2coiS (dual-stack σ) (dualS s)
dual-tailG : (σ : Stack n) (g : GType n) →
  COI.dualF (tail2coiG σ g) ≈' tail2coiG (dual-stack σ) (dualG g)

COI.Equiv.force (dual-tailS σ (gdd g)) = dual-tailG σ g
COI.Equiv.force (dual-tailS σ (rec g)) = dual-tailG ⟪ σ , g ⟫ g
COI.Equiv.force (dual-tailS σ (var x))
  rewrite get-dual-stack x σ
  with get x σ
... | m , σ' , g = dual-tailG ⟪ σ' , g ⟫ g

dual-tailG σ (transmit d t s) = COI.eq-transmit (dual-dir d) COI.≈ᵗ-refl (dual-tailS σ s)
dual-tailG σ (choice d m alt) = COI.eq-choice (dual-dir d) (dual-tailS σ ∘ alt)
dual-tailG σ end = COI.eq-end

-- corrolary for SType 0

dual-tail : ∀ s → COI.dual (tail2coiS ε s) ≈ tail2coiS ε (dualS s)
dual-tail = dual-tailS ε

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering where

open import sets.nat.ordering.lt public
open import sets.nat.ordering.leq public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module CompilingCoinduction where

open import Common.Coinduction

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

{-# COMPILED_DATA List [] [] (:) #-}

postulate
  Char : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}

-- Strings --

postulate
  String : Set

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

postulate
  putStrLn : ∞ String → IO Unit

{-# COMPILED putStrLn putStrLn #-}

main = putStrLn (♯ "a")

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Indexed monads
------------------------------------------------------------------------

-- Note that currently the monad laws are not included here.

module Category.Monad.Indexed where

open import Data.Function
open import Category.Applicative.Indexed

record RawIMonad {I : Set} (M : IFun I) : Set₁ where
  infixl 1 _>>=_ _>>_
  infixr 1 _=<<_

  field
    return : ∀ {i A} → A → M i i A
    _>>=_  : ∀ {i j k A B} → M i j A → (A → M j k B) → M i k B

  _>>_ : ∀ {i j k A B} → M i j A → M j k B → M i k B
  m₁ >> m₂ = m₁ >>= λ _ → m₂

  _=<<_ : ∀ {i j k A B} → (A → M j k B) → M i j A → M i k B
  f =<< c = c >>= f

  join : ∀ {i j k A} → M i j (M j k A) → M i k A
  join m = m >>= id

  rawIApplicative : RawIApplicative M
  rawIApplicative = record
    { pure = return
    ; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
    }

  open RawIApplicative rawIApplicative public

record RawIMonadZero {I : Set} (M : IFun I) : Set₁ where
  field
    monad : RawIMonad M
    ∅     : ∀ {i j A} → M i j A

  open RawIMonad monad public

record RawIMonadPlus {I : Set} (M : IFun I) : Set₁ where
  infixr 3 _∣_
  field
    monadZero : RawIMonadZero M
    _∣_       : ∀ {i j A} → M i j A → M i j A → M i j A

  open RawIMonadZero monadZero public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Data.HSTrie where

open import Class.Map
open import Data.List
open import Data.String
open import Data.String.Instance
open import Data.Maybe

private
  variable
    A B : Set

{-#
  FOREIGN GHC
  import Data.Trie
  import Data.Text.Encoding
#-}

postulate
  HSTrie : Set -> Set
  emptyTrie : HSTrie A
  insertTrie : String -> A -> HSTrie A -> HSTrie A
  deleteTrie : String -> HSTrie A -> HSTrie A
  lookupTrie : String -> HSTrie A -> Maybe A
  fmapTrie : (A -> B) -> HSTrie A -> HSTrie B
  trieKeysPrim : HSTrie A -> List String
  submapTrie : String -> HSTrie A -> HSTrie A

{-# COMPILE GHC HSTrie = type Trie #-}
{-# COMPILE GHC emptyTrie = \ _ -> empty #-}
{-# COMPILE GHC insertTrie = \ _ s -> insert (encodeUtf8 s) #-}
{-# COMPILE GHC deleteTrie = \ _ s -> delete (encodeUtf8 s) #-}
{-# COMPILE GHC lookupTrie = \ _ s -> Data.Trie.lookup (encodeUtf8 s) #-}
{-# COMPILE GHC fmapTrie = \ _ _ -> fmap #-}
{-# COMPILE GHC trieKeysPrim = \ _ -> fmap decodeUtf8 . keys #-}
{-# COMPILE GHC submapTrie = \ _ s -> submap (encodeUtf8 s) #-}

instance
  NDTrie-Map : MapClass String HSTrie
  NDTrie-Map = record
           { insert = insertTrie
           ; remove = deleteTrie
           ; lookup = lookupTrie
           ; mapSnd = fmapTrie
           ; emptyMap = emptyTrie
           }

trieKeys : HSTrie A -> List String
trieKeys = trieKeysPrim

lookupHSTrie : String -> HSTrie A -> HSTrie A
lookupHSTrie = submapTrie

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------------
-- Equivalence: N as the least fixed-point and N using Agda's data constructor
------------------------------------------------------------------------------

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

module LFPs.N where

open import FOTC.Base
open import FOTC.Base.PropertiesI

------------------------------------------------------------------------------
-- Auxiliary definitions and properties

flip : {A B C : Set} → (A → B → C) → B → A → C
flip f b a = f a b

cong : (f : D → D) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

------------------------------------------------------------------------------
module LFP where

  infixl 9 _+_

  -- N is a least fixed-point of a functor

  -- The functor.
  NatF : (D → Set) → D → Set
  NatF A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')

  -- The natural numbers are the least fixed-point of NatF.
  postulate
    N : D → Set

    -- N is a pre-fixed point of NatF, i.e.
    --
    -- NatF N ≤ N.
    --
    -- Peter: It corresponds to the introduction rules.
    N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') → N n

    -- The higher-order version.
    N-in-ho : ∀ {n} → NatF N n → N n

    -- N is the least pre-fixed point of NatF, i.e.
    --
    -- ∀ A. NatF A ≤ A ⇒ N ≤ A.
    --
    -- Peter: It corresponds to the elimination rule of an inductively
    -- defined predicate.
    N-ind :
      (A : D → Set) →
      (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
      ∀ {n} → N n → A n

    -- Higher-order version.
    N-ind-ho :
      (A : D → Set) → (∀ {n} → NatF A n → A n) → ∀ {n} → N n → A n

  ----------------------------------------------------------------------------
  -- N-in and N-in-ho are equivalents

  N-in₁ : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') → N n
  N-in₁ = N-in-ho

  N-in-ho₁ : ∀ {n} → NatF N n → N n
  N-in-ho₁ = N-in₁

  ----------------------------------------------------------------------------
  -- N-ind and N-ind-ho are equivalents

  N-ind-fo :
    (A : D → Set) →
    (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
    ∀ {n} → N n → A n
  N-ind-fo = N-ind-ho

  N-ind-ho' :
    (A : D → Set) → (∀ {n} → NatF A n → A n) → ∀ {n} → N n → A n
  N-ind-ho' = N-ind

  ----------------------------------------------------------------------------
  -- The data constructors of N.
  nzero : N zero
  nzero = N-in (inj₁ refl)

  nsucc : ∀ {n} → N n → N (succ₁ n)
  nsucc Nn = N-in (inj₂ (_ , refl , Nn))

  ----------------------------------------------------------------------------
  -- Because N is the least pre-fixed point of NatF (i.e. N-in and
  -- N-ind), we can proof that N is also a post-fixed point of NatF.

  -- N is a post-fixed point of NatF.
  N-out : ∀ {n} → N n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n')
  N-out = N-ind A h
    where
    A : D → Set
    A m = m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ N m')

    h : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ A m') → A m
    h (inj₁ m≡0)              = inj₁ m≡0
    h (inj₂ (m' , prf , Am')) = inj₂ (m' , prf , helper Am')
      where
      helper : A m' → N m'
      helper (inj₁ prf')                = subst N (sym prf') nzero
      helper (inj₂ (m'' , prf' , Am'')) = subst N (sym prf') (nsucc Am'')

  -- The higher-order version.
  N-out-ho : ∀ {n} → N n → NatF N n
  N-out-ho = N-out

  ----------------------------------------------------------------------------
  -- The induction principle for N *with* the hypothesis N n in the
  -- induction step using N-ind.

  N-ind₁ : (A : D → Set) →
           A zero →
           (∀ {n} → N n → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₁ A A0 h Nn = ∧-proj₂ (N-ind B h' Nn)
    where
    B : D → Set
    B n = N n ∧ A n

    h' : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ B m') → B m
    h' (inj₁ m≡0) = subst B (sym m≡0) (nzero , A0)
    h' (inj₂ (m' , prf , Nm' , Am')) =
      (subst N (sym prf) (nsucc Nm')) , subst A (sym prf) (h Nm' Am')

  ----------------------------------------------------------------------------
  -- The induction principle for N *without* the hypothesis N n in the
  -- induction step using N-ind

  N-ind₂ : (A : D → Set) →
           A zero →
           (∀ {n} → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₂ A A0 h = N-ind A h'
    where
    h' : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ A m') → A m
    h' (inj₁ m≡0)              = subst A (sym m≡0) A0
    h' (inj₂ (m' , prf , Am')) = subst A (sym prf) (h Am')

  ----------------------------------------------------------------------------
  -- Example: We will use N-ind as the induction principle on N.

  postulate
    _+_  : D → D → D
    +-0x : ∀ d → zero + d        ≡ d
    +-Sx : ∀ d e → (succ₁ d) + e ≡ succ₁ (d + e)

  +-leftIdentity : ∀ n → zero + n ≡ n
  +-leftIdentity n = +-0x n

  +-N : ∀ {m n} → N m → N n → N (m + n)
  +-N {n = n} Nm Nn = N-ind A h Nm
    where
    A : D → Set
    A i = N (i + n)

    h : ∀ {m} → m ≡ zero ∨ (∃[ m' ] m ≡ succ₁ m' ∧ A m') → A m
    h (inj₁ m≡0) = subst N (cong (flip _+_ n) (sym m≡0)) A0
      where
      A0 : A zero
      A0 = subst N (sym (+-leftIdentity n)) Nn
    h (inj₂ (m' , prf , Am')) =
      subst N (cong (flip _+_ n) (sym prf)) (is Am')
      where
      is : ∀ {i} → A i → A (succ₁ i)
      is {i} Ai = subst N (sym (+-Sx i n)) (nsucc Ai)

  ----------------------------------------------------------------------------
  -- Example: A proof using N-out.

  pred-N : ∀ {n} → N n → N (pred₁ n)
  pred-N {n} Nn = case h₁ h₂ (N-out Nn)
    where
    h₁ : n ≡ zero → N (pred₁ n)
    h₁ n≡0 = subst N (sym (trans (predCong n≡0) pred-0)) nzero

    h₂ : ∃[ n' ] n ≡ succ₁ n' ∧ N n' → N (pred₁ n)
    h₂ (n' , prf , Nn') = subst N (sym (trans (predCong prf) (pred-S n'))) Nn'

  ----------------------------------------------------------------------------
  -- From/to N as a least fixed-point to/from N as data type.

  data N' : D → Set where
    nzero' : N' zero
    nsucc' : ∀ {n} → N' n → N' (succ₁ n)

  N'→N : ∀ {n} → N' n → N n
  N'→N nzero'      = nzero
  N'→N (nsucc' Nn) = nsucc (N'→N Nn)

  -- Using N-ind₁.
  N→N' : ∀ {n} → N n → N' n
  N→N' = N-ind₁ N' nzero' (λ _ → nsucc')

  -- Using N-ind₂.
  N→N'₁ : ∀ {n} → N n → N' n
  N→N'₁ = N-ind₂ N' nzero' nsucc'

------------------------------------------------------------------------------
module Data where

  data N : D → Set where
    nzero : N zero
    nsucc : ∀ {n} → N n → N (succ₁ n)

  -- The induction principle for N *with* the hypothesis N n in the
  -- induction step.
  N-ind₁ : (A : D → Set) →
           A zero →
           (∀ {n} → N n → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₁ A A0 h nzero      = A0
  N-ind₁ A A0 h (nsucc Nn) = h Nn (N-ind₁ A A0 h Nn)

  -- The induction principle for N *without* the hypothesis N n in the
  -- induction step.
  N-ind₂ : (A : D → Set) →
           A zero →
           (∀ {n} → A n → A (succ₁ n)) →
           ∀ {n} → N n → A n
  N-ind₂ A A0 h nzero      = A0
  N-ind₂ A A0 h (nsucc Nn) = h (N-ind₂ A A0 h Nn)

  ----------------------------------------------------------------------------
  -- N-in.

  N-in : ∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ N n') → N n
  N-in {n} h = case prf₁ prf₂ h
    where
    prf₁ : n ≡ zero → N n
    prf₁ n≡0 = subst N (sym n≡0) nzero

    prf₂ : ∃[ n' ] n ≡ succ₁ n' ∧ N n' → N n
    prf₂ (n' , prf , Nn') = subst N (sym prf) (nsucc Nn')

  ----------------------------------------------------------------------------
  -- From N-ind₂ to N-ind.

  N-ind' :
    (A : D → Set) →
    (∀ {n} → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n') → A n) →
    ∀ {n} → N n → A n
  N-ind' A h = N-ind₂ A h₁ h₂
    where
    h₁ :  A zero
    h₁ = h (inj₁ refl)

    h₂ : ∀ {m} → A m → A (succ₁ m)
    h₂ {m} Am = h (inj₂ (m , refl , Am))


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

open import Agda.Primitive.Cubical

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2016-09-08, issue #2167 reported by effectfully

loop : Set₁
loop = .Set

-- WAS: looping of type checker
-- NOW: proper error about invalid dotted expression


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

open import Categories.Category

module Categories.Category.Cartesian.Properties {o ℓ e} (C : Category o ℓ e) where

open import Level using (_⊔_)
open import Function using (_$_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (Σ; _,_; proj₁) renaming (_×_ to _&_)
open import Data.Product.Properties
open import Data.List as List
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Membership.Propositional
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.Vec.Relation.Unary.Any as AnyV using (here; there)
open import Data.Vec.Relation.Unary.Any.Properties
open import Data.Vec.Membership.Propositional renaming (_∈_ to _∈ᵥ_)

open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality as ≡ using (refl; _≡_)

import Data.List.Membership.Propositional.Properties as ∈ₚ
import Data.Vec.Membership.Propositional.Properties as ∈ᵥₚ

open import Categories.Category.Cartesian C

open import Categories.Diagram.Pullback C
open import Categories.Diagram.Equalizer C
open import Categories.Morphism.Reasoning C

private
  open Category C
  open HomReasoning
  variable
    A B X Y : Obj
    f g : A ⇒ B

-- all binary products and pullbacks implies equalizers
module _ (prods : BinaryProducts) (pullbacks : ∀ {A B X} (f : A ⇒ X) (g : B ⇒ X) → Pullback f g) where
  open BinaryProducts prods
  open HomReasoning

  prods×pullbacks⇒equalizers : Equalizer f g
  prods×pullbacks⇒equalizers {f = f} {g = g} = record
    { arr       = pb′.p₁
    ; equality  = begin
      f ∘ pb′.p₁           ≈⟨ refl⟩∘⟨ helper₁ ⟩
      f ∘ pb.p₁ ∘ pb′.p₂   ≈⟨ pullˡ pb.commute ⟩
      (g ∘ pb.p₂) ∘ pb′.p₂ ≈˘⟨ pushʳ helper₂ ⟩
      g ∘ pb′.p₁           ∎
    ; equalize  = λ {_ i} eq → pb′.universal $ begin
      ⟨ id , id ⟩ ∘ i                                       ≈⟨ ⟨⟩∘ ⟩
      ⟨ id ∘ i , id ∘ i ⟩                                   ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
      ⟨ i ,  i ⟩                                            ≈˘⟨ ⟨⟩-cong₂ pb.p₁∘universal≈h₁ pb.p₂∘universal≈h₂ ⟩
      ⟨ pb.p₁ ∘ pb.universal eq , pb.p₂ ∘ pb.universal eq ⟩ ≈˘⟨ ⟨⟩∘ ⟩
      h ∘ pb.universal eq                                   ∎
    ; universal = ⟺ pb′.p₁∘universal≈h₁
    ; unique    = λ eq → pb′.unique (⟺ eq) (pb.unique (pullˡ (⟺ helper₁) ○ ⟺ eq) (pullˡ (⟺ helper₂) ○ ⟺ eq))
    }
    where pb : Pullback f g
          pb         = pullbacks _ _
          module pb  = Pullback pb
          h          = ⟨ pb.p₁ , pb.p₂ ⟩
          pb′ : Pullback ⟨ id , id ⟩ h
          pb′        = pullbacks _ _
          module pb′ = Pullback pb′
          helper₁ : pb′.p₁ ≈ pb.p₁ ∘ pb′.p₂
          helper₁    = begin
            pb′.p₁                    ≈˘⟨ cancelˡ project₁ ⟩
            π₁ ∘ ⟨ id , id ⟩ ∘ pb′.p₁ ≈⟨ refl⟩∘⟨ pb′.commute ⟩
            π₁ ∘ h ∘ pb′.p₂           ≈⟨ pullˡ project₁ ⟩
            pb.p₁ ∘ pb′.p₂            ∎
          helper₂ : pb′.p₁ ≈ pb.p₂ ∘ pb′.p₂
          helper₂    = begin
            pb′.p₁                    ≈˘⟨ cancelˡ project₂ ⟩
            π₂ ∘ ⟨ id , id ⟩ ∘ pb′.p₁ ≈⟨ refl⟩∘⟨ pb′.commute ⟩
            π₂ ∘ h ∘ pb′.p₂           ≈⟨ pullˡ project₂ ⟩
            pb.p₂ ∘ pb′.p₂            ∎

module Prods (car : Cartesian) where
  open Cartesian car

  -- for lists

  prod : List Obj → Obj
  prod objs = foldr _×_ ⊤ objs

  π[_] : ∀ {x xs} → x ∈ xs → prod xs ⇒ x
  π[ here refl ]  = π₁
  π[ there x∈xs ] = π[ x∈xs ] ∘ π₂

  data _⇒_* : Obj → List Obj → Set (o ⊔ ℓ) where
    _~[] : ∀ x → x ⇒ [] *
    _∷_  : ∀ {x y ys} → x ⇒ y → x ⇒ ys * → x ⇒ y ∷ ys *

  ⟨_⟩* : ∀ {x ys} (fs : x ⇒ ys *) → x ⇒ prod ys
  ⟨ x ~[] ⟩*  = !
  ⟨ f ∷ fs ⟩* = ⟨ f , ⟨ fs ⟩* ⟩

  ∈⇒mor : ∀ {x y ys} (fs : x ⇒ ys *) (y∈ys : y ∈ ys) → x ⇒ y
  ∈⇒mor (x ~[]) ()
  ∈⇒mor (f ∷ fs) (here refl)  = f
  ∈⇒mor (f ∷ fs) (there y∈ys) = ∈⇒mor fs y∈ys

  project* : ∀ {x y ys} (fs : x ⇒ ys *) (y∈ys : y ∈ ys) → π[ y∈ys ] ∘ ⟨ fs ⟩* ≈ ∈⇒mor fs y∈ys
  project* (x ~[]) ()
  project* (f ∷ fs) (here refl)  = project₁
  project* (f ∷ fs) (there y∈ys) = pullʳ project₂ ○ project* fs y∈ys

  uniqueness* : ∀ {x ys} {g h : x ⇒ prod ys} → (∀ {y} (y∈ys : y ∈ ys) → π[ y∈ys ] ∘ g ≈ π[ y∈ys ] ∘ h) → g ≈ h
  uniqueness* {x} {[]} uni     = !-unique₂
  uniqueness* {x} {y ∷ ys} uni = unique′ (uni (here ≡.refl)) (uniqueness* λ y∈ys → sym-assoc ○ uni (there y∈ys) ○ assoc)

  module _ {a} {A : Set a} (f : A → Obj) where

    uniqueness*′ : ∀ {x ys} {g h : x ⇒ prod (map f ys)} → (∀ {y} (y∈ys : y ∈ ys) → π[ ∈ₚ.∈-map⁺ f y∈ys ] ∘ g ≈ π[ ∈ₚ.∈-map⁺ f y∈ys ] ∘ h) → g ≈ h
    uniqueness*′ {x} {[]} uni = !-unique₂
    uniqueness*′ {x} {y ∷ ys} uni = unique′ (uni (here ≡.refl)) (uniqueness*′ λ y∈ys → sym-assoc ○ uni (there y∈ys) ○ assoc)

    module _ {x} (g : ∀ a → x ⇒ f a) where

      build-mors : (l : List A) → x ⇒ map f l *
      build-mors []      = _ ~[]
      build-mors (y ∷ l) = g y ∷ build-mors l

      build-proj≡ : ∀ {a l} (a∈l : a ∈ l) → g a ≡ ∈⇒mor (build-mors l) (∈ₚ.∈-map⁺ f a∈l)
      build-proj≡ (here refl) = ≡.refl
      build-proj≡ (there a∈l) = build-proj≡ a∈l

      build-proj : ∀ {a l} (a∈l : a ∈ l) → g a ≈ π[ ∈ₚ.∈-map⁺ f a∈l ] ∘ ⟨ build-mors l ⟩*
      build-proj {_} {l} a∈l = reflexive (build-proj≡ a∈l) ○ ⟺ (project* (build-mors l) _)

    build-⟨⟩*∘ : ∀ {x y} (g : ∀ a → x ⇒ f a) (h : y ⇒ x) → ∀ l → ⟨ build-mors g l ⟩* ∘ h ≈ ⟨ build-mors (λ a → g a ∘ h) l ⟩*
    build-⟨⟩*∘ g h []      = !-unique₂
    build-⟨⟩*∘ g h (x ∷ l) = begin
      ⟨ build-mors g (x ∷ l) ⟩* ∘ h                   ≈⟨ ⟨⟩∘ ⟩
      ⟨ g x ∘ h , ⟨ build-mors g l ⟩* ∘ h ⟩           ≈⟨ ⟨⟩-congˡ (build-⟨⟩*∘ g h l) ⟩
      ⟨ g x ∘ h , ⟨ build-mors (λ a → g a ∘ h) l ⟩* ⟩ ∎

    build-uniqueness* : ∀ {x} {g h : ∀ a → x ⇒ f a} → (∀ a → g a ≈ h a) → ∀ l → ⟨ build-mors g l ⟩* ≈ ⟨ build-mors h l ⟩*
    build-uniqueness* {x} {g} {h} uni []      = Equiv.refl
    build-uniqueness* {x} {g} {h} uni (y ∷ l) = ⟨⟩-cong₂ (uni y) (build-uniqueness* uni l)

  -- for vectors

  prodᵥ : ∀ {n} → Vec Obj (suc n) → Obj
  prodᵥ v = Vec.foldr₁ _×_ v

  π[_]ᵥ : ∀ {n x} {xs : Vec Obj (suc n)} → x ∈ᵥ xs → prodᵥ xs ⇒ x
  π[_]ᵥ {.0} {.x} {x ∷ []} (here refl)           = id
  π[_]ᵥ {.(suc _)} {.x} {x ∷ y ∷ xs} (here refl) = π₁
  π[_]ᵥ {.(suc _)} {x} {_ ∷ y ∷ xs} (there x∈xs) = π[ x∈xs ]ᵥ ∘ π₂

  data [_]_⇒ᵥ_* : ∀ n → Obj → Vec Obj n → Set (o ⊔ ℓ) where
    _~[] : ∀ x → [ 0 ] x ⇒ᵥ [] *
    _∷_  : ∀ {x y n} {ys : Vec Obj n} → x ⇒ y → [ n ] x ⇒ᵥ ys * → [ suc n ] x ⇒ᵥ y ∷ ys *

  ⟨_⟩ᵥ* : ∀ {n x ys} (fs : [ suc n ] x ⇒ᵥ ys *) → x ⇒ prodᵥ ys
  ⟨ f ∷ (x ~[]) ⟩ᵥ*  = f
  ⟨ f ∷ (g ∷ fs) ⟩ᵥ* = ⟨ f , ⟨ g ∷ fs ⟩ᵥ* ⟩

  ∈⇒morᵥ : ∀ {n x y ys} (fs : [ n ] x ⇒ᵥ ys *) (y∈ys : y ∈ᵥ ys) → x ⇒ y
  ∈⇒morᵥ (x ~[]) ()
  ∈⇒morᵥ (f ∷ fs) (here refl)  = f
  ∈⇒morᵥ (f ∷ fs) (there y∈ys) = ∈⇒morᵥ fs y∈ys

  projectᵥ* : ∀ {n x y ys} (fs : [ suc n ] x ⇒ᵥ ys *) (y∈ys : y ∈ᵥ ys) → π[ y∈ys ]ᵥ ∘ ⟨ fs ⟩ᵥ* ≈ ∈⇒morᵥ fs y∈ys
  projectᵥ* (f ∷ (x ~[])) (here ≡.refl) = identityˡ
  projectᵥ* (f ∷ g ∷ fs) (here ≡.refl)  = project₁
  projectᵥ* (f ∷ g ∷ fs) (there y∈ys)   = pullʳ project₂ ○ projectᵥ* (g ∷ fs) y∈ys

  uniquenessᵥ* : ∀ {x n ys} {g h : x ⇒ prodᵥ {n} ys} → (∀ {y} (y∈ys : y ∈ᵥ ys) → π[ y∈ys ]ᵥ ∘ g ≈ π[ y∈ys ]ᵥ ∘ h) → g ≈ h
  uniquenessᵥ* {x} {.0} {y ∷ []} uni           = ⟺ identityˡ ○ uni (here ≡.refl) ○ identityˡ
  uniquenessᵥ* {x} {.(suc _)} {y ∷ z ∷ ys} uni = unique′ (uni (here ≡.refl)) (uniquenessᵥ* (λ y∈ys → sym-assoc ○ uni (there y∈ys) ○ assoc))

  module _ {a} {A : Set a} (f : A → Obj) where

    uniquenessᵥ*′ : ∀ {x n ys} {g h : x ⇒ prodᵥ {n} (Vec.map f ys)} → (∀ {y} (y∈ys : y ∈ᵥ ys) → π[ ∈ᵥₚ.∈-map⁺ f y∈ys ]ᵥ ∘ g ≈ π[ ∈ᵥₚ.∈-map⁺ f y∈ys ]ᵥ ∘ h) → g ≈ h
    uniquenessᵥ*′ {x} {.0} {y ∷ []} uni           = ⟺ identityˡ ○ uni (here ≡.refl) ○ identityˡ
    uniquenessᵥ*′ {x} {.(suc _)} {y ∷ z ∷ ys} uni = unique′ (uni (here ≡.refl)) (uniquenessᵥ*′ (λ y∈ys → sym-assoc ○ uni (there y∈ys) ○ assoc))

    module _ {x} (g : ∀ a → x ⇒ f a) where

      buildᵥ-mors : ∀ {n} (l : Vec A n) → [ n ] x ⇒ᵥ Vec.map f l *
      buildᵥ-mors []          = _ ~[]
      buildᵥ-mors (y ∷ [])    = g y ∷ _ ~[]
      buildᵥ-mors (y ∷ z ∷ l) = g y ∷ buildᵥ-mors (z ∷ l)

      buildᵥ-proj≡ : ∀ {a n} {l : Vec A n} (a∈l : a ∈ᵥ l) → g a ≡ ∈⇒morᵥ (buildᵥ-mors l) (∈ᵥₚ.∈-map⁺ f a∈l)
      buildᵥ-proj≡ {_} {_} {y ∷ []} (here refl)    = ≡.refl
      buildᵥ-proj≡ {_} {_} {y ∷ z ∷ l} (here refl) = ≡.refl
      buildᵥ-proj≡ {_} {_} {y ∷ z ∷ l} (there a∈l) = buildᵥ-proj≡ a∈l

      buildᵥ-proj : ∀ {a n} {l : Vec A (suc n)} (a∈l : a ∈ᵥ l) → g a ≈ π[ ∈ᵥₚ.∈-map⁺ f a∈l ]ᵥ ∘ ⟨ buildᵥ-mors l ⟩ᵥ*
      buildᵥ-proj {_} {_} {l} a∈l = reflexive (buildᵥ-proj≡ a∈l) ○ ⟺ (projectᵥ* (buildᵥ-mors l) _)

    buildᵥ-⟨⟩*∘ : ∀ {x y} (g : ∀ a → x ⇒ f a) (h : y ⇒ x) → ∀ {n} (l : Vec A (suc n)) → ⟨ buildᵥ-mors g l ⟩ᵥ* ∘ h ≈ ⟨ buildᵥ-mors (λ a → g a ∘ h) l ⟩ᵥ*
    buildᵥ-⟨⟩*∘ g h (x ∷ [])        = Equiv.refl
    buildᵥ-⟨⟩*∘ g h (x ∷ y ∷ [])    = ⟨⟩∘
    buildᵥ-⟨⟩*∘ g h (x ∷ y ∷ z ∷ l) = begin
      ⟨ g x , ⟨ buildᵥ-mors g (y ∷ z ∷ l) ⟩ᵥ* ⟩ ∘ h                 ≈⟨ ⟨⟩∘ ⟩
      ⟨ g x ∘ h , ⟨ buildᵥ-mors g (y ∷ z ∷ l) ⟩ᵥ* ∘ h ⟩             ≈⟨ ⟨⟩-congˡ (buildᵥ-⟨⟩*∘ g h (y ∷ z ∷ l)) ⟩
      ⟨ g x ∘ h , ⟨ buildᵥ-mors (λ a₁ → g a₁ ∘ h) (y ∷ z ∷ l) ⟩ᵥ* ⟩ ∎

    buildᵥ-uniqueness* : ∀ {x} {g h : ∀ a → x ⇒ f a} → (∀ a → g a ≈ h a) → ∀ {n} (l : Vec A (suc n)) → ⟨ buildᵥ-mors g l ⟩ᵥ* ≈ ⟨ buildᵥ-mors h l ⟩ᵥ*
    buildᵥ-uniqueness* {x} {g} {h} uni (y ∷ []) = uni y
    buildᵥ-uniqueness* {x} {g} {h} uni (y ∷ z ∷ []) = ⟨⟩-cong₂ (uni y) (uni z)
    buildᵥ-uniqueness* {x} {g} {h} uni (y ∷ z ∷ w ∷ l) = ⟨⟩-cong₂ (uni y) (buildᵥ-uniqueness* uni (z ∷ w ∷ l))

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  A : Set
  a b : A
  f : Level → A
  g h : Level
  f-g : f (lsuc g) ≡ a
  f-h : f (lsuc h) ≡ b
  g-h : g ≡ h

{-# REWRITE f-g f-h g-h #-}