text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.CartesianClosed.Properties where

open import Level
open import Data.Product using (Σ; _,_; Σ-syntax; proj₁; proj₂)

open import Categories.Category
open import Categories.Category.CartesianClosed

module _ {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
  open Category 𝒞
  open CartesianClosed 𝓥
  open HomReasoning

  PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
  PointSurjective {A = A} {X = X} {Y = Y} ϕ =
    ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)

  lawvere-fixed-point : ∀ {A B : Obj} → (ϕ : A ⇒ B ^ A) → PointSurjective ϕ → (f : B ⇒ B) → Σ[ s ∈ ⊤ ⇒ B ] f ∘ s ≈ s
  lawvere-fixed-point {A = A} {B = B} ϕ surjective f = g ∘ x , g-fixed-point
    where
      g : A ⇒ B
      g = f ∘ eval′ ∘ ⟨ ϕ , id ⟩

      x : ⊤ ⇒ A
      x = proj₁ (surjective  g)

      g-surjective : eval′ ∘ first ϕ ∘ ⟨ x , x ⟩ ≈ g ∘ x
      g-surjective = proj₂ (surjective g) x

      lemma : ∀ {A B C D} → (f : B ⇒ C) → (g : B ⇒ D) → (h : A ⇒ B) → (f ⁂ g) ∘ ⟨ h , h ⟩ ≈ ⟨ f , g ⟩ ∘ h
      lemma f g h = begin
        (f ⁂ g) ∘ ⟨ h , h ⟩ ≈⟨  ⁂∘⟨⟩ ⟩
        ⟨ f ∘ h , g ∘ h ⟩   ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ f , g ⟩ ∘ h       ∎

      g-fixed-point : f ∘ (g ∘ x) ≈ g ∘ x
      g-fixed-point = begin
        f ∘ g ∘ x                        ≈⟨  refl⟩∘⟨ sym g-surjective ⟩
        f ∘ eval′ ∘ first ϕ ∘ ⟨ x , x ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ lemma ϕ id x ⟩
        f ∘ eval′ ∘ ⟨ ϕ , id ⟩ ∘ x       ≈˘⟨ ∘-resp-≈ˡ sym-assoc ○ assoc ○ assoc ⟩
        (f ∘ eval′ ∘ ⟨ ϕ , id ⟩) ∘ x     ≈⟨ refl ⟩
        g ∘ x                            ∎

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

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

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

module FOTC.Program.GCD.Partial.CorrectnessProofI where

open import FOTC.Base
open import FOTC.Data.Nat.Divisibility.NotBy0.PropertiesI
  using ( 0∤x ; x∣S→x≤S )
open import FOTC.Data.Nat.Type
open import FOTC.Program.GCD.Partial.CommonDivisorI using ( gcdCD )
open import FOTC.Program.GCD.Partial.Definitions
open import FOTC.Program.GCD.Partial.DivisibleI using ( gcdDivisible )
open import FOTC.Program.GCD.Partial.GCD using ( gcd )

import FOTC.Program.GCD.Partial.GreatestAnyCommonDivisor
open module GreatestAnyCommonDivisorI =
  FOTC.Program.GCD.Partial.GreatestAnyCommonDivisor x∣S→x≤S 0∤x
  using ( gcdGACD )

open import FOTC.Program.GCD.Partial.TotalityI using ( gcd-N )

------------------------------------------------------------------------------
-- The gcd is correct.
gcdCorrect : ∀ {m n} → N m → N n → x≢0≢y m n → gcdSpec m n (gcd m n)
gcdCorrect Nm Nn m≢0≢n = gcdCD Nm Nn m≢0≢n
                         , gcdGACD (gcd-N Nm Nn m≢0≢n)
                                   (gcdCD Nm Nn m≢0≢n)
                                   (gcdDivisible Nm Nn m≢0≢n)

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Common.Equality

module M where

  record R : Set₁ where
    field
      X : Set

open M using (R)

X : R → Set
X = R.X

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

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

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

-- open R

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

module N where

  data D : Set₁ where
    c : Set → D

open N using (D) renaming (module D to MD)

twoWaysToQualify : D.c ≡ MD.c
twoWaysToQualify = refl

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module AnyBoolean where
open import Data.Bool
open import Data.Nat
open import Data.List hiding (any)
open import Relation.Binary.PropositionalEquality

even : ℕ → Bool
even zero = true
even (suc zero) = false
even (suc (suc n)) = even n

test-6-even : even 6 ≡ true
test-6-even = refl

odd : ℕ → Bool
odd zero = false
odd (suc zero) = true
odd (suc (suc n)) = odd n

test-5-odd : odd 5 ≡ true
test-5-odd = refl

any : {A : Set} → (A → Bool) → List A → Bool
any _ [] = false
any p (x ∷ xs) with p x
... | true = true
... | false = any p xs

test-any-even-true :
  any even (3 ∷ 6 ∷ 9 ∷ []) ≡ true
test-any-even-true = refl

test-any-even-false :
  any even (3 ∷ 7 ∷ 9 ∷ []) ≡ false
test-any-even-false = refl

test-any-odd-true :
  any odd (4 ∷ 7 ∷ 10 ∷ []) ≡ true
test-any-odd-true = refl

test-any-odd-false :
  any odd (4 ∷ 8 ∷ 10 ∷ []) ≡ false
test-any-odd-false = refl


text:
------------------------------------------------------------------------------
-- Definition of the gcd of two natural numbers using the Euclid's algorithm
------------------------------------------------------------------------------

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

module LTC-PCF.Program.GCD.Partial.GCD where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Loop

------------------------------------------------------------------------------
-- In GHC ≤ 7.0.4 the gcd is a partial function, i.e. gcd 0 0 = undefined.

-- Let T = D → D → D be a type. Instead of defining gcdh : T → T, we
-- use the LTC-PCF λ-abstraction and application to avoid use a
-- polymorphic fixed-point operator.

gcdh : D → D
gcdh g = lam (λ m → lam (λ n →
           if (iszero₁ n)
             then (if (iszero₁ m) then error else m)
             else (if (iszero₁ m)
                     then n
                     else (if (gt m n)
                             then g · (m ∸ n) · n
                             else g · m · (n ∸ m)))))

gcd : D → D → D
gcd m n = fix gcdh · m · n


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

module Interval where

open import Pitch

open import Data.Bool       using (Bool; true; false; _∨_; _∧_; not; if_then_else_)
open import Data.Integer    using (+_; _-_; sign; ∣_∣)
open import Data.Fin        using (toℕ)
open import Data.Nat        using (ℕ; _≡ᵇ_)
open import Data.Nat.DivMod using (_mod_)
open import Data.Product    using (_×_; _,_; Σ; proj₁; proj₂)
open import Data.Sign       using (Sign)

open import Function        using (_∘_)

open import Relation.Binary.PropositionalEquality using (_≡_)

PitchPair : Set
PitchPair = Pitch × Pitch

data Interval : Set where
  interval : ℕ → Interval

infix 4 _==_

_==_ : Interval → Interval → Bool
(interval a) == (interval b) = a ≡ᵇ b

intervalWithinOctave : Interval → Interval
intervalWithinOctave (interval i) = interval (toℕ (i mod chromaticScaleSize))

SignedInterval : Set
SignedInterval = Sign × Interval

-- Names for intervals
per1  = interval 0
min2  = interval 1
maj2  = interval 2
min3  = interval 3
maj3  = interval 4
per4  = interval 5
aug4  = interval 6
per5  = interval 7
min6  = interval 8
maj6  = interval 9
min7  = interval 10
maj7  = interval 11
per8  = interval 12
min9  = interval 13
maj9  = interval 14
min10 = interval 15
maj10 = interval 16

isConsonant : Interval → Bool
isConsonant iv =
  (i == per1)  ∨
  (i == min3)  ∨
  (i == maj3)  ∨
  (i == per5)  ∨
  (i == min6)  ∨
  (i == maj6)  ∨
  (i == per8)
  where i = intervalWithinOctave iv

isDissonant : Interval → Bool
isDissonant = not ∘ isConsonant

isPerfect : Interval → Bool
isPerfect iv =
  (i == per1)  ∨
  (i == per4)  ∨
  (i == per5)  ∨
  (i == per8)
  where i = intervalWithinOctave iv

isUnison : Interval → Bool
isUnison i = i == per1

isThird : Interval → Bool
isThird i = (i == min3) ∨ (i == maj3)

-- Half or whole step; ignores key for now.
isStep : Interval → Bool
isStep i =
  (i == min2)  ∨
  (i == maj2)

PitchInterval : Set
PitchInterval = Pitch × Interval

pitchIntervalToPitchPair : PitchInterval → PitchPair
pitchIntervalToPitchPair (p , interval n) = (p , transposePitch (+ n)  p)

secondPitch : PitchInterval → Pitch
secondPitch = proj₂ ∘ pitchIntervalToPitchPair

pitchPairToSignedInterval : PitchPair → SignedInterval
pitchPairToSignedInterval (pitch p , pitch q) =
  let d = (+ q) - (+ p)
  in sign d , interval ∣ d ∣

-- Assumes p ≤ q
pitchPairToPitchInterval : PitchPair → PitchInterval
pitchPairToPitchInterval pq = proj₁ pq , proj₂ (pitchPairToSignedInterval pq)

stepUp : Pitch → Pitch → Bool
stepUp p q with pitchPairToSignedInterval (p , q)
... | Sign.- , _ = false
... | Sign.+ , i = isStep i

stepDown : Pitch → Pitch → Bool
stepDown p q with pitchPairToSignedInterval (p , q)
... | Sign.- , i = isStep i
... | Sign.+ , _ = false

-- Check if q is a passing tone between p and r
-- The interval between end points need to be a 3rd
isPassingTone : Pitch → Pitch → Pitch → Bool
isPassingTone p q r =
  (stepUp p q ∧ stepUp q r) ∨ (stepDown p q ∧ stepDown q r) ∨
  (isThird (proj₂ (pitchPairToSignedInterval (p , r))))

moveUp : Pitch → Pitch → Bool
moveUp p q with pitchPairToSignedInterval (p , q)
... | Sign.- , _ = false
... | Sign.+ , i = true

moveDown : Pitch → Pitch → Bool
moveDown p q with pitchPairToSignedInterval (p , q)
... | Sign.- , i = true
... | Sign.+ , _ = false

-- Check if q is left by step in the opposite direction from its approach
isOppositeStep : Pitch → Pitch → Pitch → Bool
isOppositeStep p q r = (moveUp p q ∧ stepDown q r) ∨ (moveDown p q ∧ stepUp q r)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
------------------------------------------------------------------------------
-- All the LTC-PCF modules
------------------------------------------------------------------------------

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

module LTC-PCF.Everything where

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties

open import LTC-PCF.Data.Bool
open import LTC-PCF.Data.Bool.Properties
open import LTC-PCF.Data.Bool.Type

open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Divisibility.By0
open import LTC-PCF.Data.Nat.Divisibility.By0.Properties
open import LTC-PCF.Data.Nat.Divisibility.NotBy0
open import LTC-PCF.Data.Nat.Divisibility.NotBy0.Properties
open import LTC-PCF.Data.Nat.Induction.NonAcc.Lexicographic
open import LTC-PCF.Data.Nat.Induction.NonAcc.WF
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.ConversionRules
open import LTC-PCF.Data.Nat.Inequalities.EliminationProperties
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Data.Nat.Rec
open import LTC-PCF.Data.Nat.Rec.ConversionRules
open import LTC-PCF.Data.Nat.Type
open import LTC-PCF.Data.Nat.UnaryNumbers
open import LTC-PCF.Data.Nat.UnaryNumbers.Totality

open import LTC-PCF.Loop

open import LTC-PCF.Program.Division.ConversionRules
open import LTC-PCF.Program.Division.CorrectnessProof
open import LTC-PCF.Program.Division.Division
open import LTC-PCF.Program.Division.Result
open import LTC-PCF.Program.Division.Specification
open import LTC-PCF.Program.Division.Totality

open import LTC-PCF.Program.GCD.Partial.CommonDivisor
open import LTC-PCF.Program.GCD.Partial.ConversionRules
open import LTC-PCF.Program.GCD.Partial.CorrectnessProof
open import LTC-PCF.Program.GCD.Partial.Definitions
open import LTC-PCF.Program.GCD.Partial.Divisible
open import LTC-PCF.Program.GCD.Partial.GCD
open import LTC-PCF.Program.GCD.Partial.GreatestAnyCommonDivisor
open import LTC-PCF.Program.GCD.Partial.GreatestAnyCommonDivisor
open import LTC-PCF.Program.GCD.Partial.Totality

open import LTC-PCF.Program.GCD.Total.CommonDivisor
open import LTC-PCF.Program.GCD.Total.CorrectnessProof
open import LTC-PCF.Program.GCD.Total.ConversionRules
open import LTC-PCF.Program.GCD.Total.Definitions
open import LTC-PCF.Program.GCD.Total.Divisible
open import LTC-PCF.Program.GCD.Total.GCD
open import LTC-PCF.Program.GCD.Total.Totality


text:
module Tactic.Nat where

open import Prelude
open import Tactic.Nat.Generic (quote _≤_) (quote id) (quote id) public

{-

All tactics know about addition, multiplication and subtraction
of natural numbers, and can prove equalities and inequalities (_<_).
The available tactics are:

  * auto

    Prove an equation or inequality.

  * by eq

    Prove the goal using the given assumption. For equalities it simplifies
    the goal and the assumption and checks if they match any of the following
    forms (up to symmetry):

          a ≡ b → a ≡ b
      a + b ≡ 0 → a ≡ 0

    For inequalities, to prove a < b -> c < d, it simplifies the assumption and
    goal and then tries to prove c′ ≤ a′ and b′ ≤ d′.

    When proving that an inequality follows from an equality a ≡ b, the equality
    is weakened to a ≤ b before applying the above procedure.

    Proving an equality from an inequality works if the inequality simplifies to
    a ≤ 0 (or a < 0 in which case it's trivial). It then reduces that to a ≡ 0
    and tries to prove the goal from that.

  * refute eq

    Proves an arbitrary proposition given a false equation. Works for equations
    that simplify to 0 ≡ suc n (or symmetric) or n < 0, for some n.

  * simplify-goal ?

    Simplify the current goal and let you keep working on the new goal.
    In most cases 'by prf' works better than
    'simplify-goal prf' since it will also simplify prf. The advantage
    of simplify-goal is that it allows holes in prf.

  * simplify eq λ x → ?

    Simplify the given equation (and the current goal) and bind the simplified
    equation to x in the new goal.

  * induction

    Prove a goal ∀ n → P n using induction. Applies 'auto' in the base case
    and 'by IH' in the step case.
-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module cantor where

  data Empty : Set where

  data One : Set where
    one : One

  data coprod (A : Set1) (B : Set1) : Set1 where
    inl : ∀ (a : A) -> coprod A B
    inr : ∀ (b : B) -> coprod A B

  postulate exmid : ∀ (A : Set1) -> coprod A (A -> Empty)

  data Eq1 {A : Set1} (x : A) : A -> Set1 where
    refleq1 : Eq1 x x

  cast : ∀ { A B } -> Eq1 A B -> A -> B
  cast refleq1 a = a

  Eq1cong : ∀ {f g : Set -> Set} a -> Eq1 f g -> Eq1 (f a) (g a)
  Eq1cong a refleq1 = refleq1

  Eq1sym : ∀ {A : Set1} { x y : A } -> Eq1 x y -> Eq1 y x
  Eq1sym refleq1 = refleq1

  Eq1trans : ∀ {A : Set1} { x y z : A } -> Eq1 x y -> Eq1 y z -> Eq1 x z
  Eq1trans refleq1 refleq1 = refleq1

  data I : (Set -> Set) -> Set where

  Iinj : ∀ { x y : Set -> Set } -> Eq1 (I x) (I y) -> Eq1 x y
  Iinj refleq1 = refleq1

  data invimageI (a : Set) : Set1 where
    invelmtI : forall x -> (Eq1 (I x) a) -> invimageI a

  J : Set -> (Set -> Set)
  J a with exmid (invimageI a)
  J a | inl (invelmtI x y) = x
  J a | inr b = λ x → Empty

  data invimageJ (x : Set -> Set) : Set1 where
    invelmtJ : forall a -> (Eq1 (J a) x) -> invimageJ x

  IJIeqI : ∀ x -> Eq1 (I (J (I x))) (I x)
  IJIeqI x with exmid (invimageI (I x))
  IJIeqI x | inl (invelmtI x' y) = y
  IJIeqI x | inr b with b (invelmtI x refleq1)
  IJIeqI x | inr b | ()

  J_srj : ∀ (x : Set -> Set) -> invimageJ x
  J_srj x = invelmtJ (I x) (Iinj (IJIeqI x))

  cantor : Set -> Set
  cantor a with exmid (Eq1 (J a a) Empty)
  cantor a | inl a' = One
  cantor a | inr b = Empty

  OneNeqEmpty : Eq1 One Empty -> Empty
  OneNeqEmpty p = cast p one

  cantorone : ∀ a -> Eq1 (J a a) Empty -> Eq1 (cantor a) One
  cantorone a p with exmid (Eq1 (J a a) Empty)
  cantorone a p | inl a' = refleq1
  cantorone a p | inr b with b p
  cantorone a p | inr b | ()

  cantorempty : ∀ a -> (Eq1 (J a a) Empty -> Empty) -> Eq1 (cantor a) Empty
  cantorempty a p with exmid (Eq1 (J a a) Empty)
  cantorempty a p | inl a' with p a'
  cantorempty a p | inl a' | ()
  cantorempty a p | inr b = refleq1

  cantorcase : ∀ a -> Eq1 cantor (J a) -> Empty
  cantorcase a pf with exmid (Eq1 (J a a) Empty)
  cantorcase a pf | inl a' = OneNeqEmpty (Eq1trans (Eq1trans (Eq1sym (cantorone a a')) (Eq1cong a pf)) a')
  cantorcase a pf | inr b = b (Eq1trans (Eq1sym (Eq1cong a pf)) (cantorempty a b))

  absurd : Empty
  absurd with (J_srj cantor)
  absurd | invelmtJ a y = cantorcase a (Eq1sym y)


text:
------------------------------------------------------------------------
-- Precedence-correct expressions
------------------------------------------------------------------------

module Mixfix.Expr where

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

open import Mixfix.Fixity
open import Mixfix.Operator

------------------------------------------------------------------------
-- An abstract definition of precedence graphs

-- The interface of precedence graphs.

record PrecedenceGraphInterface : Set₁ where
  field
    -- Precedence graphs.
    PrecedenceGraph : Set

    -- Precedence levels.
    Precedence : PrecedenceGraph → Set

    -- The operators of the given precedence.
    ops : (g : PrecedenceGraph) →
          Precedence g → (fix : Fixity) → List (∃ (Operator fix))

    -- The immediate successors of the precedence level.
    ↑ : (g : PrecedenceGraph) → Precedence g → List (Precedence g)

    -- All precedence levels in the graph.
    anyPrecedence : (g : PrecedenceGraph) → List (Precedence g)

-- When a precedence graph is given the following module may be
-- convenient to avoid having to write "g" all the time.

module PrecedenceGraph
         (i : PrecedenceGraphInterface)
         (g : PrecedenceGraphInterface.PrecedenceGraph i)
         where

  PrecedenceGraph : Set
  PrecedenceGraph = PrecedenceGraphInterface.PrecedenceGraph i

  Precedence : Set
  Precedence = PrecedenceGraphInterface.Precedence i g

  ops : Precedence → (fix : Fixity) → List (∃ (Operator fix))
  ops = PrecedenceGraphInterface.ops i g

  ↑ : Precedence → List Precedence
  ↑ = PrecedenceGraphInterface.↑ i g

  anyPrecedence : List Precedence
  anyPrecedence = PrecedenceGraphInterface.anyPrecedence i g

------------------------------------------------------------------------
-- Precedence-correct operator applications

-- Parameterised on a precedence graph.

module PrecedenceCorrect
         (i : PrecedenceGraphInterface)
         (g : PrecedenceGraphInterface.PrecedenceGraph i)
         where

  open PrecedenceGraph i g public

  mutual

    infixl 4 _⟨_⟩ˡ_
    infixr 4 _⟨_⟩ʳ_
    infix  4 _⟨_⟩_ _⟨_⟫ ⟪_⟩_ _∙_

    -- Expr ps contains expressions where the outermost operator has
    -- one of the precedences in ps.

    data Expr (ps : List Precedence) : Set where
      _∙_ : ∀ {p assoc} (p∈ps : p ∈ ps) (e : ExprIn p assoc) → Expr ps

    -- ExprIn p assoc contains expressions where the outermost
    -- operator has precedence p (is /in/ precedence level p) and the
    -- associativity assoc.

    data ExprIn (p : Precedence) : Associativity → Set where
      ⟪_⟫    :                    (op : Inner (ops p closed      ))                     → ExprIn p non
      _⟨_⟫   : (l : Outer p left) (op : Inner (ops p postfx      ))                     → ExprIn p left
      ⟪_⟩_   :                    (op : Inner (ops p prefx       )) (r : Outer p right) → ExprIn p right
      _⟨_⟩_  : (l : Expr (↑ p)  ) (op : Inner (ops p (infx non  ))) (r : Expr (↑ p)   ) → ExprIn p non
      _⟨_⟩ˡ_ : (l : Outer p left) (op : Inner (ops p (infx left ))) (r : Expr (↑ p)   ) → ExprIn p left
      _⟨_⟩ʳ_ : (l : Expr (↑ p)  ) (op : Inner (ops p (infx right))) (r : Outer p right) → ExprIn p right

    -- Outer p fix contains expressions where the head operator either
    --   ⑴ has precedence p and associativity assoc or
    --   ⑵ binds strictly tighter than p.

    data Outer (p : Precedence) (assoc : Associativity) : Set where
      similar : (e : ExprIn p assoc) → Outer p assoc
      tighter : (e : Expr (↑ p))     → Outer p assoc

    -- Inner ops contains the internal parts (operator plus
    -- internal arguments) of operator applications. The operators
    -- have to be members of ops.

    data Inner {fix} (ops : List (∃ (Operator fix))) : Set where
      _∙_ : ∀ {arity op}
            (op∈ops : (arity , op) ∈ ops)
            (args : Vec (Expr anyPrecedence) arity) →
            Inner ops

  -- "Weakening".

  weakenE : ∀ {p ps} → Expr ps → Expr (p ∷ ps)
  weakenE (p∈ps ∙ e) = there p∈ps ∙ e

  weakenI : ∀ {fix ops} {op : ∃ (Operator fix)} →
            Inner ops → Inner (op ∷ ops)
  weakenI (op∈ops ∙ args) = there op∈ops ∙ args

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Algebra
open import Cubical.Algebra.Semigroup.Morphism
open import Cubical.Algebra.Magma.Submagma

open import Cubical.Relation.Unary
open import Cubical.Relation.Unary.Subtype

record IsSubsemigroup {c ℓ} (S : Semigroup c) (Member : Pred ⟨ S ⟩ ℓ) : Type (ℓ-max c ℓ) where
  constructor issubsemigroup

  private module S = Semigroup S

  field
    closed : S._•_ Preserves₂ Member

  isSubmagma : IsSubmagma S.magma Member
  isSubmagma = record { closed = closed }

  open IsSubmagma isSubmagma hiding (closed) public

  assoc : Associative _•_
  assoc _ _ _ = ΣPathTransport→PathΣ _ _ (S.assoc _ _ _ , isProp[ Member ] _ _ _)

  isSemigroup : IsSemigroup Carrier _•_
  isSemigroup = record
    { isMagma = isMagma
    ; assoc = assoc
    }

  semigroup : Semigroup _
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup using (_^_) public

record Subsemigroup {c} (S : Semigroup c) ℓ : Type (ℓ-max c (ℓ-suc ℓ)) where
  constructor mksubsemigroup

  private module S = Semigroup S

  field
    Member : Pred ⟨ S ⟩ ℓ
    isSubsemigroup : IsSubsemigroup S Member

  open IsSubsemigroup isSubsemigroup public

  submagma : Submagma S.magma ℓ
  submagma = record { isSubmagma = isSubmagma }

instance
  SubsemigroupCarrier : ∀ {c ℓ} {S : Semigroup c} → HasCarrier (Subsemigroup S ℓ) _
  SubsemigroupCarrier = record { ⟨_⟩ = Subsemigroup.Carrier }

module _ {ℓ} (S : Semigroup ℓ) where
  open Semigroup S

  ∅-isSubsemigroup : IsSubsemigroup S ∅
  ∅-isSubsemigroup = record { closed = λ () }

  ∅-subsemigroup : Subsemigroup S _
  ∅-subsemigroup = record { isSubsemigroup = ∅-isSubsemigroup }

  U-isSubsemigroup : IsSubsemigroup S U
  U-isSubsemigroup = record {} -- trivial

  U-subsemigroup : Subsemigroup S _
  U-subsemigroup = record { isSubsemigroup = U-isSubsemigroup }


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.CohomologyRings.Unit where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Int
open import Cubical.Data.Vec
open import Cubical.Data.FinData

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int renaming (ℤGroup to ℤG)
open import Cubical.Algebra.DirectSum.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.Polynomials.Multivariate.Base renaming (base to baseP)
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.A[X]X-A
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-notationZ

open import Cubical.HITs.Truncation
open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.Groups.Unit

open Iso

module Equiv-Unit-Properties where

  open CommRingStr (snd ℤCR) using ()
    renaming
    ( 0r        to 0ℤ
    ; 1r        to 1ℤ
    ; _+_       to _+ℤ_
    ; -_        to -ℤ_
    ; _·_       to _·ℤ_
    ; +Assoc    to +ℤAssoc
    ; +Identity to +ℤIdentity
    ; +Lid      to +ℤLid
    ; +Rid      to +ℤRid
    ; +Inv      to +ℤInv
    ; +Linv     to +ℤLinv
    ; +Rinv     to +ℤRinv
    ; +Comm     to +ℤComm
    ; ·Assoc    to ·ℤAssoc
    ; ·Identity to ·ℤIdentity
    ; ·Lid      to ·ℤLid
    ; ·Rid      to ·ℤRid
    ; ·Rdist+   to ·ℤRdist+
    ; ·Ldist+   to ·ℤLdist+
    ; is-set    to isSetℤ     )

  open RingStr (snd (H*R Unit)) using ()
    renaming
    ( 0r        to 0H*
    ; 1r        to 1H*
    ; _+_       to _+H*_
    ; -_        to -H*_
    ; _·_       to _cup_
    ; +Assoc    to +H*Assoc
    ; +Identity to +H*Identity
    ; +Lid      to +H*Lid
    ; +Rid      to +H*Rid
    ; +Inv      to +H*Inv
    ; +Linv     to +H*Linv
    ; +Rinv     to +H*Rinv
    ; +Comm     to +H*Comm
    ; ·Assoc    to ·H*Assoc
    ; ·Identity to ·H*Identity
    ; ·Lid      to ·H*Lid
    ; ·Rid      to ·H*Rid
    ; ·Rdist+   to ·H*Rdist+
    ; ·Ldist+   to ·H*Ldist+
    ; is-set    to isSetH*     )

  open CommRingStr (snd ℤ[X]) using ()
    renaming
    ( 0r        to 0Pℤ
    ; 1r        to 1Pℤ
    ; _+_       to _+Pℤ_
    ; -_        to -Pℤ_
    ; _·_       to _·Pℤ_
    ; +Assoc    to +PℤAssoc
    ; +Identity to +PℤIdentity
    ; +Lid      to +PℤLid
    ; +Rid      to +PℤRid
    ; +Inv      to +PℤInv
    ; +Linv     to +PℤLinv
    ; +Rinv     to +PℤRinv
    ; +Comm     to +PℤComm
    ; ·Assoc    to ·PℤAssoc
    ; ·Identity to ·PℤIdentity
    ; ·Lid      to ·PℤLid
    ; ·Rid      to ·PℤRid
    ; ·Rdist+   to ·PℤRdist+
    ; ·Ldist+   to ·PℤLdist+
    ; is-set    to isSetPℤ     )

  open CommRingStr (snd ℤ[X]/X) using ()
    renaming
    ( 0r        to 0PℤI
    ; 1r        to 1PℤI
    ; _+_       to _+PℤI_
    ; -_        to -PℤI_
    ; _·_       to _·PℤI_
    ; +Assoc    to +PℤIAssoc
    ; +Identity to +PℤIIdentity
    ; +Lid      to +PℤILid
    ; +Rid      to +PℤIRid
    ; +Inv      to +PℤIInv
    ; +Linv     to +PℤILinv
    ; +Rinv     to +PℤIRinv
    ; +Comm     to +PℤIComm
    ; ·Assoc    to ·PℤIAssoc
    ; ·Identity to ·PℤIIdentity
    ; ·Lid      to ·PℤILid
    ; ·Rid      to ·PℤIRid
    ; ·Rdist+   to ·PℤIRdist+
    ; ·Ldist+   to ·PℤILdist+
    ; is-set    to isSetPℤI     )

-----------------------------------------------------------------------------
-- Direct Sens on ℤ[x]

  ℤ[x]→H*-Unit : ℤ[x] → H* Unit
  ℤ[x]→H*-Unit = Poly-Rec-Set.f _ _ _ isSetH*
                  0H*
                  base-trad
                  _+H*_
                  +H*Assoc
                  +H*Rid
                  +H*Comm
                  base-neutral-eq
                  base-add-eq
               where
               base-trad : _
               base-trad (zero ∷ []) a = base zero (inv (fst H⁰-Unit≅ℤ) a)
               base-trad (suc n ∷ []) a = 0H*

               base-neutral-eq :  _
               base-neutral-eq (zero ∷ []) = base-neutral _
               base-neutral-eq (suc n ∷ []) = refl

               base-add-eq : _
               base-add-eq (zero ∷ []) a b = base-add _ _ _
               base-add-eq (suc n ∷ []) a b = +H*Rid _

  ℤ[x]→H*-Unit-pres1Pℤ : ℤ[x]→H*-Unit (1Pℤ) ≡ 1H*
  ℤ[x]→H*-Unit-pres1Pℤ = refl

  ℤ[x]→H*-Unit-pres+ : (x y : ℤ[x]) → ℤ[x]→H*-Unit (x +Pℤ y) ≡ ℤ[x]→H*-Unit x +H* ℤ[x]→H*-Unit y
  ℤ[x]→H*-Unit-pres+ x y = refl

-- Proving the morphism on the cup product

  T0 : (z : ℤ) → coHom 0 Unit
  T0 = λ z → inv (fst H⁰-Unit≅ℤ) z

  T0g : IsGroupHom (ℤG .snd) (fst (invGroupIso H⁰-Unit≅ℤ) .fun) (coHomGr 0 Unit .snd)
  T0g = snd (invGroupIso H⁰-Unit≅ℤ)

    -- idea : control of the unfolding + simplification of T0 on the left
  pres·-base-case-00 : (a : ℤ) → (b : ℤ) →
                        T0 (a ·ℤ b) ≡ (T0 a) ⌣ (T0 b)
  pres·-base-case-00 (pos zero)       b = (IsGroupHom.pres1 T0g)
  pres·-base-case-00 (pos (suc n))    b = ((IsGroupHom.pres· T0g b (pos n ·ℤ b)))
                                          ∙ (cong (λ X → (T0 b) +ₕ X) (pres·-base-case-00 (pos n) b))
  pres·-base-case-00 (negsuc zero)    b = IsGroupHom.presinv T0g b
  pres·-base-case-00 (negsuc (suc n)) b = cong T0 (+ℤComm (-ℤ b) (negsuc n ·ℤ b)) -- ·ℤ and ·₀ are defined asymetrically !
                                          ∙ IsGroupHom.pres· T0g (negsuc n ·ℤ b) (-ℤ b)
                                          ∙ cong₂ _+ₕ_ (pres·-base-case-00 (negsuc n) b)
                                                         (IsGroupHom.presinv T0g b)

  pres·-base-case-int : (n : ℕ) → (a : ℤ) → (m : ℕ) → (b : ℤ) →
                ℤ[x]→H*-Unit (baseP (n ∷ []) a ·Pℤ baseP (m ∷ []) b)
              ≡ ℤ[x]→H*-Unit (baseP (n ∷ []) a) cup ℤ[x]→H*-Unit (baseP (m ∷ []) b)
  pres·-base-case-int zero    a zero    b = cong (base 0) (pres·-base-case-00 a b)
  pres·-base-case-int zero    a (suc m) b = refl
  pres·-base-case-int (suc n) a m       b = refl

  pres·-base-case-vec : (v : Vec ℕ 1) → (a : ℤ) → (v' : Vec ℕ 1) → (b : ℤ) →
                ℤ[x]→H*-Unit (baseP v a ·Pℤ baseP v' b)
              ≡ ℤ[x]→H*-Unit (baseP v a) cup ℤ[x]→H*-Unit (baseP v' b)
  pres·-base-case-vec (n ∷ []) a (m ∷ []) b = pres·-base-case-int n a m b

  ℤ[x]→H*-Unit-pres· : (x y : ℤ[x]) → ℤ[x]→H*-Unit (x ·Pℤ y) ≡ ℤ[x]→H*-Unit x cup ℤ[x]→H*-Unit y
  ℤ[x]→H*-Unit-pres· = Poly-Ind-Prop.f _ _ _
                         (λ x p q i y j → isSetH* _ _ (p y) (q y) i j)
                         (λ y → refl)
                         base-case
                         λ {U V} ind-U ind-V y → cong₂ _+H*_ (ind-U y) (ind-V y)
    where
    base-case : _
    base-case (n ∷ []) a = Poly-Ind-Prop.f _ _ _ (λ _ → isSetH* _ _)
                           (sym (RingTheory.0RightAnnihilates (H*R Unit) _))
                           (λ v' b → pres·-base-case-vec (n ∷ []) a v' b)
                           λ {U V} ind-U ind-V → (cong₂ _+H*_ ind-U ind-V) ∙ sym (·H*Rdist+ _ _ _)

    -- raising to the product
  ℤ[x]→H*-Unit-cancelX : (k : Fin 1) → ℤ[x]→H*-Unit (<X> k) ≡ 0H*
  ℤ[x]→H*-Unit-cancelX zero = refl

  ℤ[X]→H*-Unit : RingHom (CommRing→Ring ℤ[X]) (H*R Unit)
  fst ℤ[X]→H*-Unit = ℤ[x]→H*-Unit
  snd ℤ[X]→H*-Unit = makeIsRingHom ℤ[x]→H*-Unit-pres1Pℤ ℤ[x]→H*-Unit-pres+ ℤ[x]→H*-Unit-pres·

  ℤ[X]/X→H*R-Unit : RingHom (CommRing→Ring ℤ[X]/X) (H*R Unit)
  ℤ[X]/X→H*R-Unit = Quotient-FGideal-CommRing-Ring.f ℤ[X] (H*R Unit) ℤ[X]→H*-Unit <X> ℤ[x]→H*-Unit-cancelX

  ℤ[x]/x→H*-Unit : ℤ[x]/x → H* Unit
  ℤ[x]/x→H*-Unit = fst ℤ[X]/X→H*R-Unit

-----------------------------------------------------------------------------
-- Converse Sens on ℤ[X]

  H*-Unit→ℤ[x] : H* Unit → ℤ[x]
  H*-Unit→ℤ[x] = DS-Rec-Set.f _ _ _ _ isSetPℤ
                  0Pℤ
                  base-trad
                  _+Pℤ_
                  +PℤAssoc
                  +PℤRid
                  +PℤComm
                  base-neutral-eq
                  base-add-eq
               where
               base-trad : (n : ℕ) → coHom n Unit → ℤ[x]
               base-trad zero a = baseP (0 ∷ []) (fun (fst H⁰-Unit≅ℤ) a)
               base-trad (suc n) a = 0Pℤ

               base-neutral-eq : _
               base-neutral-eq zero = base-0P _
               base-neutral-eq (suc n) = refl

               base-add-eq : _
               base-add-eq zero a b = base-poly+ _ _ _
                                      ∙ cong (baseP (0 ∷ [])) (sym (IsGroupHom.pres· (snd H⁰-Unit≅ℤ) a b))
               base-add-eq (suc n) a b = +PℤRid _

  H*-Unit→ℤ[x]-pres+ : (x y : H* Unit) → H*-Unit→ℤ[x] ( x +H* y) ≡ H*-Unit→ℤ[x] x +Pℤ H*-Unit→ℤ[x] y
  H*-Unit→ℤ[x]-pres+ x y = refl

  H*-Unit→ℤ[x]/x : H* Unit → ℤ[x]/x
  H*-Unit→ℤ[x]/x = [_] ∘ H*-Unit→ℤ[x]

  H*-Unit→ℤ[x]/x-pres+ : (x y : H* Unit) → H*-Unit→ℤ[x]/x (x +H* y) ≡ (H*-Unit→ℤ[x]/x x) +PℤI (H*-Unit→ℤ[x]/x y)
  H*-Unit→ℤ[x]/x-pres+ x y = cong [_] (H*-Unit→ℤ[x]-pres+ x y)

-----------------------------------------------------------------------------
-- Section

  e-sect : (x : H* Unit) → ℤ[x]/x→H*-Unit (H*-Unit→ℤ[x]/x x) ≡ x
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong ℤ[x]/x→H*-Unit (H*-Unit→ℤ[x]/x-pres+ U V)
                                  ∙ IsRingHom.pres+ (snd ℤ[X]/X→H*R-Unit) (H*-Unit→ℤ[x]/x U) (H*-Unit→ℤ[x]/x V)
                                  ∙ cong₂ _+H*_ ind-U ind-V
           where
           base-case : _
           base-case zero a = cong (base 0) (leftInv (fst H⁰-Unit≅ℤ) a)
           base-case (suc n) a = (sym (base-neutral (suc n)))
                                 ∙ (cong (base (suc n)) ((isContr→isProp (isContrHⁿ-Unit n) _ a)))

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (x : ℤ[x]/x) → H*-Unit→ℤ[x]/x (ℤ[x]/x→H*-Unit x) ≡ x
  e-retr = SQ.elimProp (λ _ → isSetPℤI _ _)
           (Poly-Ind-Prop.f _ _ _ (λ _ → isSetPℤI _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V)
           where
           base-case : _
           base-case (zero ∷ []) a = refl
           base-case (suc n ∷ []) a = eq/ 0Pℤ (baseP (suc n ∷ []) a) ∣ ((λ x → baseP (n ∷ []) (-ℤ a)) , foo) ∣₁
             where
             foo : (0P poly+ baseP (suc n ∷ []) (- a)) ≡ (baseP (n +n 1 ∷ []) (- a · pos 1) poly+ 0P)
             foo = (0P poly+ baseP (suc n ∷ []) (- a)) ≡⟨ +PℤLid _ ⟩
                   baseP (suc n ∷ []) (- a) ≡⟨ cong₂ baseP (cong (λ X → X ∷ []) (sym ((+-suc n 0)
                                              ∙ (cong suc (+-zero n))))) (sym (·ℤRid _)) ⟩
                   baseP (n +n suc 0 ∷ []) (- a ·ℤ 1ℤ) ≡⟨ refl ⟩
                   baseP (n +n 1 ∷ []) (- a · pos 1) ≡⟨ sym (+PℤRid _) ⟩
                   (baseP (n +n 1 ∷ []) (- a · pos 1) poly+ 0P) ∎

-----------------------------------------------------------------------------
-- Computation of the Cohomology Ring

module _ where

  open Equiv-Unit-Properties
  open RingEquivs

  Unit-CohomologyRingP : RingEquiv (CommRing→Ring ℤ[X]/X) (H*R Unit)
  fst Unit-CohomologyRingP = isoToEquiv is
    where
    is : Iso ℤ[x]/x (H* Unit)
    fun is = ℤ[x]/x→H*-Unit
    inv is = H*-Unit→ℤ[x]/x
    rightInv is = e-sect
    leftInv is = e-retr
  snd Unit-CohomologyRingP = snd ℤ[X]/X→H*R-Unit

  CohomologyRing-UnitP : RingEquiv (H*R Unit) (CommRing→Ring ℤ[X]/X)
  CohomologyRing-UnitP = invEquivRing Unit-CohomologyRingP

  Unit-CohomologyRingℤ : RingEquiv (CommRing→Ring ℤCR) (H*R Unit)
  Unit-CohomologyRingℤ = compRingEquiv (invEquivRing Equiv-ℤ[X]/X-ℤ) Unit-CohomologyRingP

  CohomologyRing-Unitℤ : RingEquiv (H*R Unit) (CommRing→Ring ℤCR)
  CohomologyRing-Unitℤ = compRingEquiv CohomologyRing-UnitP Equiv-ℤ[X]/X-ℤ

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
-- Andreas, 2016-12-30, issue #1886

-- Make sure we do not duplicate types of parameters.

-- {-# OPTIONS --allow-unsolved-metas #-}
-- {-# OPTIONS -v tc.data:40 -v scope.data.def:40 -v tc.decl:10 -v tc:20 #-}

data D {A : Set} (x y : {!!}) : Set where

-- Expected: only one type and one sort meta.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- 2014-08-25 reported by Wolfram Kahl, test case shrunk by Ulf, fixed by Andreas and Ulf
-- {-# OPTIONS --show-implicit -v tc.cover.splittree:10 -v tc.with:40 -v tc.cc:12 #-}
postulate K : Set

data SUList : K → Set where
  cons : ∀ {k} (es : SUList k) → SUList k

data Tri : Set where
  tri< tri> : Tri

postulate
  k : K
  compareK : Tri
  dummy : Set
  es : SUList k

diff : SUList k → SUList k → Tri → Set
diff (cons _) _     tri< = K
diff es₁ (cons es₂) tri> = diff es₁ es₂ compareK

test = diff (cons es) (cons es) tri>
-- normalizing  test
-- gives WRONG  diff (cons k es) es compareK
-- should be    diff (cons {k} es) es compareK
-- Problem was in the clause compiler

-- Trigger the bug:
from : (es : SUList k) (c : Tri) → diff (cons es) (cons es) c → Set
from es tri< d = K
from es tri> d with dummy
... | _ = K

-- WAS:
-- Expected a hidden argument, but found a visible argument
-- when checking that the type
-- Set → (es₁ : SUList k) (d : diff (cons k es₁) es₁ compareK) → Set
-- of the generated with function is well-formed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of pointwise equality for containers
------------------------------------------------------------------------

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

module Data.Container.Relation.Binary.Pointwise.Properties where

open import Axiom.Extensionality.Propositional
open import Data.Container.Core
open import Data.Container.Relation.Binary.Pointwise
open import Data.Product using (_,_; Σ-syntax; -,_)
open import Level using (_⊔_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; cong)

module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where

  refl : Reflexive R → Reflexive (Pointwise C R)
  refl R-refl = P.refl , λ p → R-refl

  sym : Symmetric R → Symmetric (Pointwise C R)
  sym R-sym (P.refl , f) = P.refl , λ p → R-sym (f p)

  trans : Transitive R → Transitive (Pointwise C R)
  trans R-trans (P.refl , f) (P.refl , g) = P.refl , λ p → R-trans (f p) (g p)

private

  -- Note that, if propositional equality were extensional, then
  -- Eq _≡_ and _≡_ would coincide.

  Eq⇒≡ : ∀ {s p x} {C : Container s p} {X : Set x} {xs ys : ⟦ C ⟧ X} →
         Extensionality p x → Pointwise C _≡_ xs ys → xs ≡ ys
  Eq⇒≡ ext (P.refl , f≈f′) = cong -,_ (ext f≈f′)


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

open import LogicalFormulae
open import Setoids.Setoids
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Groups.SymmetricGroups.Definition
open import Groups.Actions.Definition
open import Sets.EquivalenceRelations

module Groups.ActionIsSymmetry {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (gAction : GroupAction G T) where

open Group G
open GroupAction gAction

actionPermutation : (g : A) → SymmetryGroupElements T
actionPermutation g = sym {f = λ x → action g x} (record { inj = record { injective = inj ; wellDefined = actionWellDefined2 } ; surj = record { surjective = surj ; wellDefined = actionWellDefined2 } })
  where
    open Setoid T
    open Equivalence eq
    inj : {x y : B} → (Setoid._∼_ T (action g x) (action g y)) → Setoid._∼_ T x y
    inj {x} {y} gx=gy = transitive (symmetric identityAction) (transitive (transitive (symmetric (actionWellDefined1 (invLeft {g}))) (transitive (transitive associativeAction (transitive (actionWellDefined2 gx=gy) (symmetric associativeAction))) (actionWellDefined1 (invLeft {g})))) identityAction)
    surj : {x : B} → Sg B (λ a → action g a ∼ x)
    surj {x} = action (inverse g) x , transitive (symmetric associativeAction) (transitive (actionWellDefined1 invRight) identityAction)

actionPermutationMapIsHom : GroupHom G (symmetricGroup T) actionPermutation
GroupHom.groupHom actionPermutationMapIsHom = associativeAction
GroupHom.wellDefined actionPermutationMapIsHom x=y = actionWellDefined1 x=y


text:
module tests.Arith where

open import Prelude.IO
open import Prelude.Nat
open import Prelude.Unit

test : Nat
test = 4

foobar : Nat -> Nat
foobar Z = Z
foobar (S n) = S (S n)

main : IO Unit
main =
--  n <- readNat ,
  printNat 0 ,,
  printNat (0 + 1) ,,
  printNat (1 * 2) ,,
  printNat (S (S (S (S Z))) - S Z) ,,
  printNat test    ,,
  printNat (foobar 4) ,,
--  printNat n ,,
  return unit

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists
------------------------------------------------------------------------

module Data.List where

open import Data.Nat
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
open import Data.Bool
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Product as Prod using (_×_; _,_)
open import Function
open import Algebra
import Relation.Binary.PropositionalEquality as PropEq
import Algebra.FunctionProperties as FunProp

infixr 5 _∷_ _++_

------------------------------------------------------------------------
-- Types

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

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

{-# IMPORT Data.FFI #-}
{-# COMPILED_DATA List Data.FFI.AgdaList [] (:) #-}

------------------------------------------------------------------------
-- Some operations

-- * Basic functions

[_] : ∀ {a} {A : Set a} → A → List A
[ x ] = x ∷ []

_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- Snoc.

infixl 5 _∷ʳ_

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
xs ∷ʳ x = xs ++ [ x ]

null : ∀ {a} {A : Set a} → List A → Bool
null []       = true
null (x ∷ xs) = false

-- * List transformations

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
replicate zero    x = []
replicate (suc n) x = x ∷ replicate n x

zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
          → (A → B → C) → List A → List B → List C
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
zipWith f _        _        = []

zip : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
zip = zipWith (_,_)

intersperse : ∀ {a} {A : Set a} → A → List A → List A
intersperse x []           = []
intersperse x (y ∷ [])     = [ y ]
intersperse x (y ∷ z ∷ zs) = y ∷ x ∷ intersperse x (z ∷ zs)

-- * Reducing lists (folds)

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

foldl : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
foldl c n []       = n
foldl c n (x ∷ xs) = foldl c (c n x) xs

-- ** Special folds

concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []

concatMap : ∀ {a b} {A : Set a} {B : Set b} →
            (A → List B) → List A → List B
concatMap f = concat ∘ map f

and : List Bool → Bool
and = foldr _∧_ true

or : List Bool → Bool
or = foldr _∨_ false

any : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
any p = or ∘ map p

all : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
all p = and ∘ map p

sum : List ℕ → ℕ
sum = foldr _+_ 0

product : List ℕ → ℕ
product = foldr _*_ 1

length : ∀ {a} {A : Set a} → List A → ℕ
length = foldr (λ _ → suc) 0

reverse : ∀ {a} {A : Set a} → List A → List A
reverse = foldl (λ rev x → x ∷ rev) []

-- * Building lists

-- ** Scans

scanr : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → B) → B → List A → List B
scanr f e []       = e ∷ []
scanr f e (x ∷ xs) with scanr f e xs
... | []     = []                -- dead branch
... | y ∷ ys = f x y ∷ y ∷ ys

scanl : ∀ {a b} {A : Set a} {B : Set b} →
        (A → B → A) → A → List B → List A
scanl f e []       = e ∷ []
scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs

-- ** Unfolding

-- Unfold. Uses a measure (a natural number) to ensure termination.

unfold : ∀ {a b} {A : Set a} (B : ℕ → Set b)
         (f : ∀ {n} → B (suc n) → Maybe (A × B n)) →
         ∀ {n} → B n → List A
unfold B f {n = zero}  s = []
unfold B f {n = suc n} s with f s
... | nothing       = []
... | just (x , s') = x ∷ unfold B f s'

-- downFrom 3 = 2 ∷ 1 ∷ 0 ∷ [].

downFrom : ℕ → List ℕ
downFrom n = unfold Singleton f (wrap n)
  where
  data Singleton : ℕ → Set where
    wrap : (n : ℕ) → Singleton n

  f : ∀ {n} → Singleton (suc n) → Maybe (ℕ × Singleton n)
  f {n} (wrap .(suc n)) = just (n , wrap n)

-- ** Conversions

fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
fromMaybe (just x) = [ x ]
fromMaybe nothing  = []

-- * Sublists

-- ** Extracting sublists

take : ∀ {a} {A : Set a} → ℕ → List A → List A
take zero    xs       = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : ∀ {a} {A : Set a} → ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
splitAt zero    xs       = ([] , xs)
splitAt (suc n) []       = ([] , [])
splitAt (suc n) (x ∷ xs) with splitAt n xs
... | (ys , zs) = (x ∷ ys , zs)

takeWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
takeWhile p []       = []
takeWhile p (x ∷ xs) with p x
... | true  = x ∷ takeWhile p xs
... | false = []

dropWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
dropWhile p []       = []
dropWhile p (x ∷ xs) with p x
... | true  = dropWhile p xs
... | false = x ∷ xs

span : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
span p []       = ([] , [])
span p (x ∷ xs) with p x
... | true  = Prod.map (_∷_ x) id (span p xs)
... | false = ([] , x ∷ xs)

break : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
break p = span (not ∘ p)

inits : ∀ {a} {A : Set a} → List A → List (List A)
inits []       = [] ∷ []
inits (x ∷ xs) = [] ∷ map (_∷_ x) (inits xs)

tails : ∀ {a} {A : Set a} → List A → List (List A)
tails []       = [] ∷ []
tails (x ∷ xs) = (x ∷ xs) ∷ tails xs

infixl 5 _∷ʳ'_

data InitLast {a} {A : Set a} : List A → Set a where
  []    : InitLast []
  _∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)

initLast : ∀ {a} {A : Set a} (xs : List A) → InitLast xs
initLast []               = []
initLast (x ∷ xs)         with initLast xs
initLast (x ∷ .[])        | []       = [] ∷ʳ' x
initLast (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y

-- * Searching lists

-- ** Searching with a predicate

-- A generalised variant of filter.

gfilter : ∀ {a b} {A : Set a} {B : Set b} →
          (A → Maybe B) → List A → List B
gfilter p []       = []
gfilter p (x ∷ xs) with p x
... | just y  = y ∷ gfilter p xs
... | nothing =     gfilter p xs

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p = gfilter (λ x → if p x then just x else nothing)

partition : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
partition p []       = ([] , [])
partition p (x ∷ xs) with p x | partition p xs
... | true  | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)

------------------------------------------------------------------------
-- List monoid

monoid : ∀ {ℓ} → Set ℓ → Monoid _ _
monoid A = record
  { Carrier  = List A
  ; _≈_      = _≡_
  ; _∙_      = _++_
  ; ε        = []
  ; isMonoid = record
    { isSemigroup = record
      { isEquivalence = PropEq.isEquivalence
      ; assoc         = assoc
      ; ∙-cong        = cong₂ _++_
      }
    ; identity = ((λ _ → refl) , identity)
    }
  }
  where
  open PropEq
  open FunProp _≡_

  identity : RightIdentity [] _++_
  identity []       = refl
  identity (x ∷ xs) = cong (_∷_ x) (identity xs)

  assoc : Associative _++_
  assoc []       ys zs = refl
  assoc (x ∷ xs) ys zs = cong (_∷_ x) (assoc xs ys zs)

------------------------------------------------------------------------
-- List monad

open import Category.Monad

monad : ∀ {ℓ} → RawMonad (List {ℓ})
monad = record
  { return = λ x → x ∷ []
  ; _>>=_  = λ xs f → concat (map f xs)
  }

monadZero : ∀ {ℓ} → RawMonadZero (List {ℓ})
monadZero = record
  { monad = monad
  ; ∅     = []
  }

monadPlus : ∀ {ℓ} → RawMonadPlus (List {ℓ})
monadPlus = record
  { monadZero = monadZero
  ; _∣_       = _++_
  }

------------------------------------------------------------------------
-- Monadic functions

private
 module Monadic {m} {M : Set m → Set m} (Mon : RawMonad M) where

  open RawMonad Mon

  sequence : ∀ {A} → List (M A) → M (List A)
  sequence []       = return []
  sequence (x ∷ xs) = _∷_ <$> x ⊛ sequence xs

  mapM : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (List B)
  mapM f = sequence ∘ map f

open Monadic public


text:
open import Everything

module Test.Transassociativity where

test-transassociativity-≡ : ∀
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  ⦃ _ : Transitivity.class _∼_ ⦄
  ⦃ _ : Transassociativity!.class _∼_ Proposequality ⦄
  → ∀ {w x y z} (f : w ∼ x) (g : x ∼ y) (h : y ∼ z) → (h ∙ g) ∙ f ≡ h ∙ g ∙ f
test-transassociativity-≡ f g h rewrite transassociativity![ Proposequality ] f g h = ∅ -- transassociativity


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

open import Agda.Builtin.Unit
open import Agda.Builtin.Equality

data Unit : Set where unit : Unit

A : Unit → Set
A unit = ⊤

postulate
  a b : (u : Unit) → A u

mutual
  _X : Unit
  _X = {!unit!}

  test : a _X ≡ b _X
  test = refl


text:
module Issue289 where

data D : Set where
  d : D

record ⊤ : Set where

foo : (x y : D) → ⊤
foo d y = {!y!}

-- WAS:
-- Right hand side must be a single hole when making a case
-- distinction.
-- when checking that the expression ? has type ⊤

-- NOW: (Andreas, 2013-03-22)
-- Since goal is solved, further case distinction is not supported;
-- try `Solve constraints' instead
-- when checking that the expression ? has type ⊤


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

module 04-inductive-types where

import 03-natural-numbers
open 03-natural-numbers public

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

-- Section 4.2 The unit type

-- Definition 4.2.1

data unit : UU lzero where
  star : unit

𝟙 = unit

ind-unit : {i : Level} {P : unit → UU i} → P star → ((x : unit) → P x)
ind-unit p star = p

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

-- Section 4.3 The empty type

-- Definition 4.3.1

data empty : UU lzero where

𝟘 = empty

ind-empty : {i : Level} {P : empty → UU i} → ((x : empty) → P x)
ind-empty ()

ex-falso : {i : Level} {A : UU i} → empty → A
ex-falso = ind-empty

-- Definition 4.3.2

¬ : {i : Level} → UU i → UU i
¬ A = A → empty

-- Proposition 4.3.3

functor-neg : {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  (P → Q) → (¬ Q → ¬ P)
functor-neg f nq p = nq (f p)

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

-- Section 4.4 The booleans

-- Definition 4.4.1

data bool : UU lzero where
  true false : bool

-- Example 4.4.2

neg-𝟚 : bool → bool
neg-𝟚 true = false
neg-𝟚 false = true

conjunction-𝟚 : bool → (bool → bool)
conjunction-𝟚 true true = true
conjunction-𝟚 true false = false
conjunction-𝟚 false true = false
conjunction-𝟚 false false = false

disjunction-𝟚 : bool → (bool → bool)
disjunction-𝟚 true true = true
disjunction-𝟚 true false = true
disjunction-𝟚 false true = true
disjunction-𝟚 false false = false

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

-- Section 4.5 Coproducts

-- Definition 4.5.1

data coprod {i j : Level} (A : UU i) (B : UU j) : UU (i ⊔ j)  where
  inl : A → coprod A B
  inr : B → coprod A B

ind-coprod : {i j k : Level} {A : UU i} {B : UU j} (C : coprod A B → UU k) →
  ((x : A) → C (inl x)) → ((y : B) → C (inr y)) →
  (t : coprod A B) → C t
ind-coprod C f g (inl x) = f x
ind-coprod C f g (inr x) = g x

-- Remark 4.5.2

functor-coprod :
  {l1 l2 l1' l2' : Level} {A : UU l1} {B : UU l2} {A' : UU l1'} {B' : UU l2'} →
  (A → A') → (B → B') → coprod A B → coprod A' B'
functor-coprod f g (inl x) = inl (f x)
functor-coprod f g (inr y) = inr (g y)

-- Proposition 4.5.3

coprod-elim-left :
  {i j : Level} (A : UU i) (B : UU j) →
  ¬ B → coprod A B → A
coprod-elim-left A B nb (inl a) = a
coprod-elim-left A B nb (inr b) = ex-falso (nb b)

coprod-elim-right :
  {i j : Level} (A : UU i) (B : UU j) →
  ¬ A → coprod A B → B
coprod-elim-right A B na (inl a) = ex-falso (na a)
coprod-elim-right A B na (inr b) = b

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

-- Section 4.6 Dependent pair types

-- Definition 4.6.1

data Σ {i j : Level} (A : UU i) (B : A → UU j) : UU (i ⊔ j) where
  pair : (x : A) → (B x → Σ A B)

ind-Σ : {i j k : Level} {A : UU i} {B : A → UU j} {C : Σ A B → UU k} →
  ((x : A) (y : B x) → C (pair x y)) → ((t : Σ A B) → C t)
ind-Σ f (pair x y) = f x y

-- Remark 4.6.2

ev-pair :
  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : Σ A B → UU l3} →
  ((t : Σ A B) → C t) → (x : A) (y : B x) → C (pair x y)
ev-pair f x y = f (pair x y)

-- Definition 4.6.3

pr1 : {i j : Level} {A : UU i} {B : A → UU j} → Σ A B → A
pr1 (pair a b) = a

pr2 : {i j : Level} {A : UU i} {B : A → UU j} → (t : Σ A B) → B (pr1 t)
pr2 (pair a b) = b

-- Definition 4.6.4

prod : {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
prod A B = Σ A (λ a → B)

pair' :
  {i j : Level} {A : UU i} {B : UU j} → A → B → prod A B
pair' = pair

_×_ :  {i j : Level} (A : UU i) (B : UU j) → UU (i ⊔ j)
A × B = prod A B

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

-- Section 4.7 The type of integers

-- Definition 4.7.1

-- The type of integers

ℤ : UU lzero
ℤ = coprod ℕ (coprod unit ℕ)

-- Inclusion of the negative integers

in-neg : ℕ → ℤ
in-neg n = inl n

-- Negative one

neg-one-ℤ : ℤ
neg-one-ℤ = in-neg zero-ℕ

-- Zero

zero-ℤ : ℤ
zero-ℤ = inr (inl star)

-- One

one-ℤ : ℤ
one-ℤ = inr (inr zero-ℕ)

-- Inclusion of the positive integers

in-pos : ℕ → ℤ
in-pos n = inr (inr n)

-- Inclusion of the natural numbers

int-ℕ : ℕ → ℤ
int-ℕ zero-ℕ = zero-ℤ
int-ℕ (succ-ℕ n) = in-pos n

-- Proposition 4.7.2

ind-ℤ :
  {i : Level} (P : ℤ → UU i) →
  P neg-one-ℤ → ((n : ℕ) → P (inl n) → P (inl (succ-ℕ n))) →
  P zero-ℤ →
  P one-ℤ → ((n : ℕ) → P (inr (inr (n))) → P (inr (inr (succ-ℕ n)))) →
  (k : ℤ) → P k
ind-ℤ P p-1 p-S p0 p1 pS (inl zero-ℕ) = p-1
ind-ℤ P p-1 p-S p0 p1 pS (inl (succ-ℕ x)) =
  p-S x (ind-ℤ P p-1 p-S p0 p1 pS (inl x))
ind-ℤ P p-1 p-S p0 p1 pS (inr (inl star)) = p0
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr zero-ℕ)) = p1
ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (succ-ℕ x))) =
  pS x (ind-ℤ P p-1 p-S p0 p1 pS (inr (inr (x))))

-- Definition 4.7.3

succ-ℤ : ℤ → ℤ
succ-ℤ (inl zero-ℕ) = zero-ℤ
succ-ℤ (inl (succ-ℕ x)) = inl x
succ-ℤ (inr (inl star)) = one-ℤ
succ-ℤ (inr (inr x)) = inr (inr (succ-ℕ x))

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

-- Exercises

-- Exercise 4.1 (a)

pred-ℤ : ℤ → ℤ
pred-ℤ (inl x) = inl (succ-ℕ x)
pred-ℤ (inr (inl star)) = inl zero-ℕ
pred-ℤ (inr (inr zero-ℕ)) = inr (inl star)
pred-ℤ (inr (inr (succ-ℕ x))) = inr (inr x)

-- Exercise 4.1 (b)

-- Addition on ℤ

add-ℤ : ℤ → ℤ → ℤ
add-ℤ (inl zero-ℕ) l = pred-ℤ l
add-ℤ (inl (succ-ℕ x)) l = pred-ℤ (add-ℤ (inl x) l)
add-ℤ (inr (inl star)) l = l
add-ℤ (inr (inr zero-ℕ)) l = succ-ℤ l
add-ℤ (inr (inr (succ-ℕ x))) l = succ-ℤ (add-ℤ (inr (inr x)) l)

add-ℤ' : ℤ → ℤ → ℤ
add-ℤ' x y = add-ℤ y x

-- The negative of an integer

neg-ℤ : ℤ → ℤ
neg-ℤ (inl x) = inr (inr x)
neg-ℤ (inr (inl star)) = inr (inl star)
neg-ℤ (inr (inr x)) = inl x

-- Exercise 4.1 (c)

-- Multiplication on ℤ

mul-ℤ : ℤ → ℤ → ℤ
mul-ℤ (inl zero-ℕ) l = neg-ℤ l
mul-ℤ (inl (succ-ℕ x)) l = add-ℤ (neg-ℤ l) (mul-ℤ (inl x) l)
mul-ℤ (inr (inl star)) l = zero-ℤ
mul-ℤ (inr (inr zero-ℕ)) l = l
mul-ℤ (inr (inr (succ-ℕ x))) l = add-ℤ l (mul-ℤ (inr (inr x)) l)

mul-ℤ' : ℤ → ℤ → ℤ
mul-ℤ' x y = mul-ℤ y x

-- Exercise 4.2

¬¬ : {l : Level} → UU l → UU l
¬¬ P = ¬ (¬ P)

¬¬¬ : {l : Level} → UU l → UU l
¬¬¬ P = ¬ (¬ (¬ P))

-- Exercise 4.2 (a)

no-fixed-points-neg :
  {l1 : Level} (A : UU l1) → ¬ ((A → ¬ A) × (¬ A → A))
no-fixed-points-neg A (pair f g) =
  ( λ (h : ¬ A) → h (g h)) (λ (a : A) → f a a)

-- Exercise 4.2 (b)

intro-dn : {l : Level} {P : UU l} → P → ¬¬ P
intro-dn p f = f p

-- Exercise 4.2 (c)

functor-dn : {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  (P → Q) → (¬¬ P → ¬¬ Q)
functor-dn f = functor-neg (functor-neg f)

-- Exercise 4.2 (d)

{- In this exercise we were asked to show that (A + ¬A) implies (¬¬A → A). In
   other words, we get double negation elimination for the types that are
   decidable. -}

double-negation-elim-is-decidable :
  {i : Level} (P : UU i) → coprod P (¬ P) → (¬¬ P → P)
double-negation-elim-is-decidable P (inl x) p = x
double-negation-elim-is-decidable P (inr x) p = ind-empty (p x)

-- Exercise 4.2 (e)

dn-is-decidable : {l : Level} {P : UU l} → ¬¬ (coprod P (¬ P))
dn-is-decidable {P = P} f =
  functor-neg (inr {A = P} {B = ¬ P}) f
    ( functor-neg (inl {A = P} {B = ¬ P}) f)

-- Exercise 4.2 (f)

dn-dn-elim : {l : Level} {P : UU l} → ¬¬ (¬¬ P → P)
dn-dn-elim {P = P} f =
  ( λ (np : ¬ P) → f (λ (nnp : ¬¬ P) → ind-empty {P = λ x → P} (nnp np)))
    ( λ (p : P) → f (λ (nnp : ¬¬ P) → p))

-- Exercise 4.2 (g)

tautology-4-2-f :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  ¬¬ (((P → Q) → P) → P)
tautology-4-2-f {P = P} {Q} f =
  ( λ (np : ¬ P) → f (λ h → h (λ p → ex-falso (np p))))
  ( λ (p : P) → f (λ h → p))

-- Exercise 4.2 (h)

dn-linearity-implication :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  ¬¬ (coprod (P → Q) (Q → P))
dn-linearity-implication {P = P} {Q = Q} f =
  ( λ (np : ¬ P) →
    functor-neg (inl {A = P → Q} {B = Q → P}) f (λ p → ind-empty (np p)))
    ( λ (p : P) →
      functor-neg (inr {A = P → Q} {B = Q → P}) f (λ q → p))

-- Exercise 4.2 (i)

dn-elim-neg : {l : Level} (P : UU l) → ¬¬¬ P → ¬ P
dn-elim-neg P f p = f (λ g → g p)

-- Exercise 4.2 (j)

dn-extend :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  (P → ¬¬ Q) → (¬¬ P → ¬¬ Q)
dn-extend {P = P} {Q = Q} f = dn-elim-neg (¬ Q) ∘ (functor-dn f)

-- Exercise 4.2 (k)

dn-elim-exp :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  ¬¬ (P → ¬¬ Q) → (P → ¬¬ Q)
dn-elim-exp {P = P} {Q = Q} f p =
  dn-elim-neg (¬ Q) (functor-dn (λ (g : P → ¬¬ Q) → g p) f)

-- Exercise 4.2 (l)

dn-elim-prod :
  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
  ¬¬ ((¬¬ P) × (¬¬ Q)) → (¬¬ P) × (¬¬ Q)
dn-elim-prod {P = P} {Q = Q} f =
  pair
    ( dn-elim-neg (¬ P) (functor-dn pr1 f))
    ( dn-elim-neg (¬ Q) (functor-dn pr2 f))

-- Exercise 4.3

-- Exercise 4.3 (a)

data list {l : Level} (A : UU l) : UU l where
  nil : list A
  cons : A → list A → list A

in-list : {l : Level} {A : UU l} → A → list A
in-list a = cons a nil

-- Exercise 4.3 (b)

fold-list :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) (μ : A → (B → B)) →
  list A → B
fold-list b μ nil = b
fold-list b μ (cons a l) = μ a (fold-list b μ l)

-- Exercise 4.3 (c)

length-list :
  {l : Level} {A : UU l} → list A → ℕ
length-list = fold-list zero-ℕ (λ a → succ-ℕ)

-- Exercise 4.3 (d)

sum-list-ℕ :
  list ℕ → ℕ
sum-list-ℕ = fold-list zero-ℕ add-ℕ

-- Exercise 4.3 (e)

concat-list :
  {l : Level} {A : UU l} → list A → (list A → list A)
concat-list {l} {A} = fold-list id (λ a f → (cons a) ∘ f)

-- Exercise 4.3 (f)

flatten-list :
  {l : Level} {A : UU l} → list (list A) → list A
flatten-list = fold-list nil concat-list

-- Exercise 4.3 (g)

reverse-list :
  {l : Level} {A : UU l} → list A → list A
reverse-list nil = nil
reverse-list (cons a l) = concat-list (reverse-list l) (in-list a)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
-- Andreas, 2016-12-30, issues #555 and #1886, reported by nad

-- Hidden parameters can be omitted in the repetition
-- of the parameter list.

record R {a} (A : Set a) : Set a

record R A where
  field f : A

data D {a} (A : Set a) : Set a

data D A where
  c : A → D A

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module BuiltinSucWarning where

data Nat : Set where
  zero : Nat
  suc  : (n : Nat) → Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC suc #-}

foo : Nat
foo = 13


text:
------------------------------------------------------------------------------
-- Non-intuitionistic logic theorems
------------------------------------------------------------------------------

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

module FOL.NonIntuitionistic.TheoremsATP where

open import FOL.Base hiding ( pem )

------------------------------------------------------------------------------
-- The principle of the excluded middle.
postulate pem : ∀ {A} → A ∨ ¬ A
{-# ATP prove pem #-}

-- The principle of indirect proof (proof by contradiction).
postulate ¬-elim : ∀ {A} → (¬ A → ⊥) → A
{-# ATP prove ¬-elim #-}

-- Double negation elimination.
postulate ¬¬-elim : ∀ {A} → ¬ ¬ A → A
{-# ATP prove ¬¬-elim #-}

-- The reductio ab absurdum rule. (Some authors uses this name for the
-- principle of indirect proof).
postulate raa : ∀ {A} → (¬ A → A) → A
{-# ATP prove raa #-}

-- ∃ in terms of ∀ and ¬.
postulate ¬∃¬→∀ : {A : D → Set} → ¬ (∃[ x ] ¬ A x) → ∀ {x} → A x
{-# ATP prove ¬∃¬→∀ #-}


text:
------------------------------------------------------------------------
-- Subtyping defined in terms of finite approximations
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Semantic.Inductive where

open import Data.Nat
open import Data.Fin
open import Codata.Musical.Notation

open import RecursiveTypes.Syntax
open import RecursiveTypes.Semantics

-- Finite trees.

infixr 10 _⟶_

data FinTree (n : ℕ) : Set where
  ⊥   : FinTree n
  ⊤   : FinTree n
  var : (x : Fin n) → FinTree n
  _⟶_ : (σ τ : FinTree n) → FinTree n

-- Functions which prune a possibly infinite tree.

infix 8 _↑_ _↓_

mutual

  _↑_ : ∀ {n} → Tree n → ℕ → FinTree n
  τ     ↑ zero  = ⊤
  ⊥     ↑ suc k = ⊥
  ⊤     ↑ suc k = ⊤
  var x ↑ suc k = var x
  σ ⟶ τ ↑ suc k = (♭ σ ↓ k) ⟶ (♭ τ ↑ k)

  _↓_ : ∀ {n} → Tree n → ℕ → FinTree n
  τ     ↓ zero  = ⊥
  ⊥     ↓ suc k = ⊥
  ⊤     ↓ suc k = ⊤
  var x ↓ suc k = var x
  σ ⟶ τ ↓ suc k = (♭ σ ↑ k) ⟶ (♭ τ ↓ k)

-- Subtyping for finite trees.

infix 4 _≤Fin_ _≤↓_ _≤↑_ _≤Ind_

data _≤Fin_ {n} : FinTree n → FinTree n → Set where
  ⊥    : ∀ {τ} → ⊥ ≤Fin τ
  ⊤    : ∀ {σ} → σ ≤Fin ⊤
  refl : ∀ {τ} → τ ≤Fin τ
  _⟶_  : ∀ {σ₁ σ₂ τ₁ τ₂}
         (τ₁≤σ₁ : τ₁ ≤Fin σ₁) (σ₂≤τ₂ : σ₂ ≤Fin τ₂) →
         σ₁ ⟶ σ₂ ≤Fin τ₁ ⟶ τ₂

-- Subtyping for possibly infinite trees, defined in terms of
-- subtyping for finite trees.

_≤↓_ : ∀ {n} → Tree n → Tree n → Set
σ ≤↓ τ = ∀ k → σ ↓ k ≤Fin τ ↓ k

_≤↑_ : ∀ {n} → Tree n → Tree n → Set
σ ≤↑ τ = ∀ k → σ ↑ k ≤Fin τ ↑ k

-- Subtyping for recursive types, defined in terms of subtyping for
-- possibly infinite trees.

_≤Ind_ : ∀ {n} → Ty n → Ty n → Set
σ ≤Ind τ = ⟦ σ ⟧ ≤↓ ⟦ τ ⟧

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module Computability.Data.Nat.Iteration where

open import Computability.Prelude

iterate : {A : Set} → (A → A) → ℕ → A → A
iterate f zero a = a
iterate f (suc n) a = f (iterate f n a)

split-iterate : {A : Set}(f : A → A)(a : A)
              → (n m : ℕ)
              → iterate f (n + m) a ≡ iterate f n (iterate f m a)
split-iterate f a zero m = refl
split-iterate f a (suc n) m rewrite split-iterate f a n m = refl

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Coprimality
------------------------------------------------------------------------

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

module Data.Nat.Coprimality where

open import Data.Empty
open import Data.Fin using (toℕ; fromℕ≤)
open import Data.Fin.Properties using (toℕ-fromℕ≤)
open import Data.Nat
open import Data.Nat.Divisibility
open import Data.Nat.GCD
open import Data.Nat.GCD.Lemmas
open import Data.Nat.Primality
open import Data.Nat.Properties
open import Data.Product as Prod
open import Function
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; cong; subst; module ≡-Reasoning)
open import Relation.Nullary
open import Relation.Binary

------------------------------------------------------------------------
-- Coprime m n is inhabited iff m and n are coprime (relatively
-- prime), i.e. if their only common divisor is 1.

Coprime : Rel ℕ 0ℓ
Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1

------------------------------------------------------------------------
-- Relationship between GCD and coprimality

coprime-gcd : ∀ {m n} → Coprime m n → GCD m n 1
coprime-gcd {m} {n} c = GCD.is (1∣ m , 1∣ n) greatest
  where
  greatest : ∀ {d} → d ∣ m × d ∣ n → d ∣ 1
  greatest cd with c cd
  ... | refl = 1∣ 1

gcd-coprime : ∀ {m n} → GCD m n 1 → Coprime m n
gcd-coprime g cd with GCD.greatest g cd
... | divides q eq = i*j≡1⇒j≡1 q _ (P.sym eq)

------------------------------------------------------------------------
-- Coprime is decidable.

private
  0≢1 : 0 ≢ 1
  0≢1 ()

  2+≢1 : ∀ {n} → suc (suc n) ≢ 1
  2+≢1 ()

coprime? : Decidable Coprime
coprime? i j with gcd i j
... | (0           , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime-gcd)
... | (1           , g) = yes (gcd-coprime g)
... | (suc (suc d) , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime-gcd)

-- The coprimality relation is symmetric.

sym : Symmetric Coprime
sym c = c ∘ swap

-- Everything is coprime to 1.

1-coprimeTo : ∀ m → Coprime 1 m
1-coprimeTo m = ∣1⇒≡1 ∘ proj₁

-- Nothing except for 1 is coprime to 0.

0-coprimeTo-m⇒m≡1 : ∀ {m} → Coprime 0 m → m ≡ 1
0-coprimeTo-m⇒m≡1 {m} c = c (m ∣0 , ∣-refl)

-- If m and n are coprime, then n + m and n are also coprime.

coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)

-- If the "gcd" in Bézout's identity is non-zero, then the "other"
-- divisors are coprime.

Bézout-coprime : ∀ {i j d} →
                 Bézout.Identity (suc d) (i * suc d) (j * suc d) →
                 Coprime i j
Bézout-coprime (Bézout.+- x y eq) (divides q₁ refl , divides q₂ refl) =
  lem₁₀ y q₂ x q₁ eq
Bézout-coprime (Bézout.-+ x y eq) (divides q₁ refl , divides q₂ refl) =
  lem₁₀ x q₁ y q₂ eq

-- Coprime numbers satisfy Bézout's identity.

coprime-Bézout : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j
coprime-Bézout = Bézout.identity ∘ coprime-gcd

-- If i divides jk and is coprime to j, then it divides k.

coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor {k} c (divides q eq′) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′)
... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′)

-- If d is a common divisor of mk and nk, and m and n are coprime,
-- then d divides k.

coprime-factors : ∀ {d m n k} →
                  Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k
coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c
... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂)
... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁)

-- A variant of GCD.

data GCD′ : ℕ → ℕ → ℕ → Set where
  gcd-* : ∀ {d} q₁ q₂ (c : Coprime q₁ q₂) →
          GCD′ (q₁ * d) (q₂ * d) d

-- The two definitions are equivalent.

gcd-gcd′ : ∀ {d m n} → GCD m n d → GCD′ m n d
gcd-gcd′         g with GCD.commonDivisor g
gcd-gcd′ {zero}  g | (divides q₁ refl , divides q₂ refl)
  with q₁ * 0 | *-comm 0 q₁ | q₂ * 0 | *-comm 0 q₂
... | .0 | refl | .0 | refl = gcd-* 1 1 (1-coprimeTo 1)
gcd-gcd′ {suc d} g | (divides q₁ refl , divides q₂ refl) =
  gcd-* q₁ q₂ (Bézout-coprime (Bézout.identity g))

gcd′-gcd : ∀ {m n d} → GCD′ m n d → GCD m n d
gcd′-gcd (gcd-* q₁ q₂ c) = GCD.is (n∣m*n q₁ , n∣m*n q₂) (coprime-factors c)

-- Calculates (the alternative representation of) the gcd of the
-- arguments.

gcd′ : ∀ m n → ∃ λ d → GCD′ m n d
gcd′ m n = Prod.map id gcd-gcd′ (gcd m n)

-- Primality implies coprimality.

prime⇒coprime : ∀ m → Prime m →
                ∀ n → 0 < n → n < m → Coprime m n
prime⇒coprime 0             () _ _  _     _
prime⇒coprime 1             () _ _  _     _
prime⇒coprime (suc (suc m)) _  0 () _     _
prime⇒coprime (suc (suc m)) _  _ _  _ {1} _                       = refl
prime⇒coprime (suc (suc m)) p  _ _  _ {0} (divides q 2+m≡q*0 , _) =
  ⊥-elim $ i+1+j≢i 0 (begin
    2 + m  ≡⟨ 2+m≡q*0 ⟩
    q * 0  ≡⟨ *-zeroʳ q ⟩
    0      ∎)
  where open ≡-Reasoning
prime⇒coprime (suc (suc m)) p (suc n) _ 1+n<2+m {suc (suc i)}
              (2+i∣2+m , 2+i∣1+n) =
  ⊥-elim (p _ 2+i′∣2+m)
  where
  i<m : i < m
  i<m = +-cancelˡ-< 2 (begin-strict
    2 + i ≤⟨ ∣⇒≤ 2+i∣1+n ⟩
    1 + n <⟨ 1+n<2+m ⟩
    2 + m ∎)
    where open ≤-Reasoning

  2+i′∣2+m : 2 + toℕ (fromℕ≤ i<m) ∣ 2 + m
  2+i′∣2+m = subst (_∣ 2 + m)
    (P.sym (cong (2 +_) (toℕ-fromℕ≤ i<m)))
    2+i∣2+m


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

open import Categories.Category

-- a zero object is both terminal and initial.
module Categories.Object.Zero {o ℓ e} (C : Category o ℓ e) where

open import Level using (_⊔_)

open import Categories.Object.Terminal C
open import Categories.Object.Initial C

open import Categories.Morphism C

open Category C
open HomReasoning

record Zero : Set (o ⊔ ℓ ⊔ e) where
 field
   zero : Obj
   !    : ∀ {A} → zero ⇒ A
   ¡    : ∀ {A} → A ⇒ zero

 zero⇒ : ∀ {A B : Obj} → A ⇒ B
 zero⇒ {A} = ! ∘ ¡

 field
   !-unique : ∀ {A} (f : zero ⇒ A) → ! ≈ f
   ¡-unique : ∀ {A} (f : A ⇒ zero) → ¡ ≈ f

 ¡-unique₂ : ∀ {A} (f g : A ⇒ zero) → f ≈ g
 ¡-unique₂ f g = ⟺ (¡-unique f) ○ ¡-unique g

 !-unique₂ : ∀ {A} (f g : zero ⇒ A) → f ≈ g
 !-unique₂ f g = ⟺ (!-unique f) ○ !-unique g

 initial : Initial
 initial = record
   { ⊥        = zero
   ; ⊥-is-initial = record
     { !        = !
     ; !-unique = !-unique
     }
   }

 terminal : Terminal
 terminal = record
   { ⊤        = zero
   ; ⊤-is-terminal = record
     { !        = ¡
     ; !-unique = ¡-unique
     }
   }

 module initial  = Initial initial
 module terminal = Terminal terminal

 !-Mono : ∀ {A} → Mono (! {A})
 !-Mono = from-⊤-is-Mono {t = terminal} !

 ¡-Epi : ∀ {A} → Epi (¡ {A})
 ¡-Epi = to-⊥-is-Epi {i = initial} ¡

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: FintanH/agda-categories

max_forks_repo_name: FintanH/agda-categories


text:
-- Andreas, 2014-01-21, Issue 1209 reported by Andrea

{-# OPTIONS --cubical-compatible #-}
{-# OPTIONS --copatterns #-}
{-# OPTIONS --sized-types #-}

open import Common.Size

record R (i : Size) : Set where
  coinductive
  field
    force : (j : Size< i) → R j

postulate
  f : ∀ {i} → R i → R i

t : (i : Size) → R i
R.force (t i) j = f (t j)

-- should termination check


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some algebraic structures (not packed up with sets, operations,
-- etc.)
------------------------------------------------------------------------

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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)

-- The structures are parameterised by an equivalence relation

module Algebra.Structures {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Algebra.FunctionProperties _≈_
import Algebra.FunctionProperties.Consequences as Consequences
open import Data.Product using (_,_; proj₁; proj₂)
open import Level using (_⊔_)

------------------------------------------------------------------------
-- Semigroups

record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∙-cong        : Congruent₂ ∙

  open IsEquivalence isEquivalence public

  setoid : Setoid a ℓ
  setoid = record { isEquivalence = isEquivalence }

  ∙-congˡ : LeftCongruent ∙
  ∙-congˡ y≈z = ∙-cong refl y≈z

  ∙-congʳ : RightCongruent ∙
  ∙-congʳ y≈z = ∙-cong y≈z refl

record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    assoc   : Associative ∙

  open IsMagma isMagma public

record IsBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    idem        : Idempotent ∙

  open IsSemigroup isSemigroup public

record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isBand : IsBand ∧
    comm   : Commutative ∧

  open IsBand isBand public
    renaming (∙-cong to ∧-cong; ∙-congˡ to ∧-congˡ; ∙-congʳ to ∧-congʳ)

------------------------------------------------------------------------
-- Monoids

record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identity    : Identity ε ∙

  open IsSemigroup isSemigroup public

  identityˡ : LeftIdentity ε ∙
  identityˡ = proj₁ identity

  identityʳ : RightIdentity ε ∙
  identityʳ = proj₂ identity

record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isSemigroup : IsSemigroup ∙
    identityˡ   : LeftIdentity ε ∙
    comm        : Commutative ∙

  open IsSemigroup isSemigroup public

  identityʳ : RightIdentity ε ∙
  identityʳ = Consequences.comm+idˡ⇒idʳ setoid comm identityˡ

  identity : Identity ε ∙
  identity = (identityˡ , identityʳ)

  isMonoid : IsMonoid ∙ ε
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = identity
    }

record IsIdempotentCommutativeMonoid (∙ : Op₂ A)
                                     (ε : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeMonoid : IsCommutativeMonoid ∙ ε
    idem                : Idempotent ∙

  open IsCommutativeMonoid isCommutativeMonoid public

------------------------------------------------------------------------
-- Groups

record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  field
    isMonoid  : IsMonoid _∙_ ε
    inverse   : Inverse ε _⁻¹ _∙_
    ⁻¹-cong   : Congruent₁ _⁻¹

  open IsMonoid isMonoid public

  infixl 7 _-_
  _-_ : Op₂ A
  x - y = x ∙ (y ⁻¹)

  inverseˡ : LeftInverse ε _⁻¹ _∙_
  inverseˡ = proj₁ inverse

  inverseʳ : RightInverse ε _⁻¹ _∙_
  inverseʳ = proj₂ inverse

  uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
  uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
                setoid ∙-cong assoc identity inverseʳ

  uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
  uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
                setoid ∙-cong assoc identity inverseˡ

record IsAbelianGroup (∙ : Op₂ A)
                      (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
  field
    isGroup : IsGroup ∙ ε ⁻¹
    comm    : Commutative ∙

  open IsGroup isGroup public

  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
  isCommutativeMonoid = record
    { isSemigroup = isSemigroup
    ; identityˡ   = identityˡ
    ; comm        = comm
    }

------------------------------------------------------------------------
-- Semirings

record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isMonoid    : IsMonoid + 0#
    *-isSemigroup : IsSemigroup *
    distribʳ      : * DistributesOverʳ +
    zeroˡ         : LeftZero 0# *

  open IsMonoid +-isMonoid public
    renaming
    ( assoc       to +-assoc
    ; ∙-cong      to +-cong
    ; ∙-congˡ     to +-congˡ
    ; ∙-congʳ     to +-congʳ
    ; identity    to +-identity
    ; identityˡ   to +-identityˡ
    ; identityʳ   to +-identityʳ
    ; isMagma     to +-isMagma
    ; isSemigroup to +-isSemigroup
    )

  open IsSemigroup *-isSemigroup public
    using ()
    renaming
    ( assoc    to *-assoc
    ; ∙-cong   to *-cong
    ; ∙-congˡ  to *-congˡ
    ; ∙-congʳ  to *-congʳ
    ; isMagma  to *-isMagma
    )

record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isSemigroup         : IsSemigroup *
    distrib               : * DistributesOver +
    zero                  : Zero 0# *

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

  zeroˡ : LeftZero 0# *
  zeroˡ = proj₁ zero

  zeroʳ : RightZero 0# *
  zeroʳ = proj₂ zero

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

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

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

  distribˡ : * DistributesOverˡ +
  distribˡ = proj₁ distrib

  distribʳ : * DistributesOverʳ +
  distribʳ = proj₂ distrib

  open IsCommutativeMonoid +-isCommutativeMonoid public
    renaming
    ( assoc       to +-assoc
    ; ∙-cong      to +-cong
    ; ∙-congˡ     to +-congˡ
    ; ∙-congʳ     to +-congʳ
    ; identity    to +-identity
    ; identityˡ   to +-identityˡ
    ; identityʳ   to +-identityʳ
    ; comm        to +-comm
    ; isMagma     to +-isMagma
    ; isSemigroup to +-isSemigroup
    ; isMonoid    to +-isMonoid
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; ∙-cong      to *-cong
    ; ∙-congˡ     to *-congˡ
    ; ∙-congʳ     to *-congʳ
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero + * 0# 1#
    zero : Zero 0# *

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

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

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

record IsCommutativeSemiringWithoutOne
         (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
  field
    isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
    *-comm               : Commutative *

  open IsSemiringWithoutOne isSemiringWithoutOne public

record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
    *-isCommutativeMonoid : IsCommutativeMonoid * 1#
    distribʳ              : * DistributesOverʳ +
    zeroˡ                 : LeftZero 0# *

  private
    module +-CM = IsCommutativeMonoid +-isCommutativeMonoid
    open module *-CM = IsCommutativeMonoid *-isCommutativeMonoid public
           using () renaming (comm to *-comm)

  distribˡ : * DistributesOverˡ +
  distribˡ = Consequences.comm+distrʳ⇒distrˡ
              +-CM.setoid +-CM.∙-cong *-comm distribʳ

  distrib : * DistributesOver +
  distrib = (distribˡ , distribʳ)

  zeroʳ : RightZero 0# *
  zeroʳ = Consequences.comm+zeˡ⇒zeʳ +-CM.setoid *-comm zeroˡ

  zero : Zero 0# *
  zero = (zeroˡ , zeroʳ)

  isSemiring : IsSemiring + * 0# 1#
  isSemiring = record
    { isSemiringWithoutAnnihilatingZero = record
      { +-isCommutativeMonoid = +-isCommutativeMonoid
      ; *-isMonoid            = *-CM.isMonoid
      ; distrib               = distrib
      }
    ; zero                    = zero
    }

  open IsSemiring isSemiring public
    hiding
    ( distrib; distribʳ; distribˡ
    ; zero; zeroˡ; zeroʳ
    ; +-isCommutativeMonoid
    )

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

------------------------------------------------------------------------
-- Rings

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

  open IsAbelianGroup +-isAbelianGroup public
    renaming
    ( assoc               to +-assoc
    ; ∙-cong              to +-cong
    ; ∙-congˡ             to +-congˡ
    ; ∙-congʳ             to +-congʳ
    ; identity            to +-identity
    ; identityˡ           to +-identityˡ
    ; identityʳ           to +-identityʳ
    ; inverse             to -‿inverse
    ; inverseˡ            to -‿inverseˡ
    ; inverseʳ            to -‿inverseʳ
    ; ⁻¹-cong             to -‿cong
    ; comm                to +-comm
    ; isMagma             to +-isMagma
    ; isSemigroup         to +-isSemigroup
    ; isMonoid            to +-isMonoid
    ; isCommutativeMonoid to +-isCommutativeMonoid
    ; isGroup             to +-isGroup
    )

  open IsMonoid *-isMonoid public
    using ()
    renaming
    ( assoc       to *-assoc
    ; ∙-cong      to *-cong
    ; ∙-congˡ     to *-congˡ
    ; ∙-congʳ     to *-congʳ
    ; identity    to *-identity
    ; identityˡ   to *-identityˡ
    ; identityʳ   to *-identityʳ
    ; isMagma     to *-isMagma
    ; isSemigroup to *-isSemigroup
    )

  zeroˡ : LeftZero 0# *
  zeroˡ = Consequences.assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid
           +-cong *-cong +-assoc (proj₂ distrib) +-identityʳ -‿inverseʳ

  zeroʳ : RightZero 0# *
  zeroʳ = Consequences.assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid
           +-cong *-cong +-assoc (proj₁ distrib) +-identityʳ -‿inverseʳ

  zero : Zero 0# *
  zero = (zeroˡ , zeroʳ)

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

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

  open IsSemiring isSemiring public
    using (distribˡ; distribʳ; isNearSemiring; isSemiringWithoutOne)

record IsCommutativeRing
         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isRing : IsRing + * - 0# 1#
    *-comm : Commutative *

  open IsRing isRing public

  *-isCommutativeMonoid : IsCommutativeMonoid * 1#
  *-isCommutativeMonoid =  record
    { isSemigroup = *-isSemigroup
    ; identityˡ   = *-identityˡ
    ; comm        = *-comm
    }

  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
  isCommutativeSemiring = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isCommutativeMonoid = *-isCommutativeMonoid
    ; distribʳ              = distribʳ
    ; zeroˡ                 = zeroˡ
    }

  open IsCommutativeSemiring isCommutativeSemiring public
    using ( isCommutativeSemiringWithoutOne )

------------------------------------------------------------------------
-- Lattices

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

record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    ∨-comm        : Commutative ∨
    ∨-assoc       : Associative ∨
    ∨-cong        : Congruent₂ ∨
    ∧-comm        : Commutative ∧
    ∧-assoc       : Associative ∧
    ∧-cong        : Congruent₂ ∧
    absorptive    : Absorptive ∨ ∧

  open IsEquivalence isEquivalence public

  ∨-absorbs-∧ : ∨ Absorbs ∧
  ∨-absorbs-∧ = proj₁ absorptive

  ∧-absorbs-∨ : ∧ Absorbs ∨
  ∧-absorbs-∨ = proj₂ absorptive

  ∧-congˡ : LeftCongruent ∧
  ∧-congˡ y≈z = ∧-cong refl y≈z

  ∧-congʳ : RightCongruent ∧
  ∧-congʳ y≈z = ∧-cong y≈z refl

  ∨-congˡ : LeftCongruent ∨
  ∨-congˡ y≈z = ∨-cong refl y≈z

  ∨-congʳ : RightCongruent ∨
  ∨-congʳ y≈z = ∨-cong y≈z refl

record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isLattice    : IsLattice ∨ ∧
    ∨-∧-distribʳ : ∨ DistributesOverʳ ∧

  open IsLattice isLattice public

record IsBooleanAlgebra
         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
  field
    isDistributiveLattice : IsDistributiveLattice ∨ ∧
    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
    ¬-cong                : Congruent₁ ¬

  open IsDistributiveLattice isDistributiveLattice public


text:
-- Andreas, 2014-09-02

module _ where

module Data where
  data D : Set where
    A : D

module _ (A : Set) where

  open Data using (D; A)

  x : D
  x = A


text:
-- Andreas, 2011-04-07

module IrrelevantFamilyIndex where

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

-- irrelevant index
data Fin : .Nat -> Set where
  zero : .(n : Nat) -> Fin (suc n)
  suc  : .(n : Nat) -> Fin n -> Fin (suc n)

t : Fin zero
t = zero zero

-- the following is ok, since Fin _ is really just Nat
toNat : Fin zero -> Nat
toNat (zero _)  = zero
toNat (suc _ i) = suc (toNat i)

data Pos : Nat -> Set where
  pos : (n : Nat) -> Pos (suc n)

f : (n : Nat) -> Fin n -> Pos n
f .(suc n) (zero n)  = pos n
f .(suc n) (suc n i) = pos n
-- cannot infer value of dot pattern

{-
f : (n : Nat) -> Fin n -> Pos n
f .(suc _) (zero _)  = pos _
f .(suc _) (suc _ _) = pos _

f' : (n : Nat) -> Fin n -> Pos n
f' _ (zero _)  = pos _
f' _ (suc _ _) = pos _
-}

max_stars_repo_name: asr/agda-kanso


text:
{- Copyright © 2015 Benjamin Barenblat

Licensed under the Apache License, Version 2.0 (the ‘License’); you may not use
this file except in compliance with the License.  You may obtain a copy of the
License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed
under the License is distributed on an ‘AS IS’ BASIS, WITHOUT WARRANTIES OR
CONDITIONS OF ANY KIND, either express or implied.  See the License for the
specific language governing permissions and limitations under the License. -}

module B.Prelude.Product where

import Data.Product

open Data.Product
  using (_×_; proj₁; proj₂; _,_; _,′_; curry; uncurry; uncurry′)
  public

module Product where

max_stars_repo_name: bbarenblat/B

max_issues_repo_name: bbarenblat/B

max_forks_repo_name: bbarenblat/B


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- N-ary products
------------------------------------------------------------------------

-- Vectors (as in Data.Vec) also represent n-ary products, so what is
-- the point of this module? The n-ary products below are intended to
-- be used with a fixed n, in which case the nil constructor can be
-- avoided: pairs are represented as pairs (x , y), not as triples
-- (x , y , unit).

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

module Data.Product.N-ary where

open import Data.Nat as Nat hiding (_^_)
open import Data.Fin hiding (lift)
open import Data.Product as P using (_×_ ; _,_ ; ∃₂ ; uncurry)
open import Data.Sum using (_⊎_)
open import Data.Unit
open import Data.Empty
open import Function
open import Level using (Lift; lift)
open import Relation.Binary.PropositionalEquality using (_≡_)

-- Types and patterns
------------------------------------------------------------------------

pattern 2+_ n = suc (suc n)

infix 8 _^_
_^_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ
A ^ 0    = Lift _ ⊤
A ^ 1    = A
A ^ 2+ n = A × A ^ suc n

pattern [] = lift tt

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

  infix 3 _∈[_]_
  _∈[_]_ : A → ∀ n → A ^ n → Set a
  a ∈[ 0    ] as      = Lift _ ⊥
  a ∈[ 1    ] a′      = a ≡ a′
  a ∈[ 2+ n ] a′ , as = a ≡ a′ ⊎ a ∈[ suc n ] as

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

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

  cons : ∀ n → A → A ^ n → A ^ suc n
  cons 0       a _  = a
  cons (suc n) a as = a , as

  uncons : ∀ n → A ^ suc n → A × A ^ n
  uncons 0        a        = a , lift tt
  uncons (suc n)  (a , as) = a , as

  head : ∀ n → A ^ suc n → A
  head n as = P.proj₁ (uncons n as)

  tail : ∀ n → A ^ suc n → A ^ n
  tail n as = P.proj₂ (uncons n as)

  lookup : ∀ {n} (k : Fin n) → A ^ n → A
  lookup {suc n} zero    = head n
  lookup {suc n} (suc k) = lookup k ∘′ tail n

  replicate : ∀ n → A → A ^ n
  replicate 0      a = []
  replicate 1      a = a
  replicate (2+ n) a = a , replicate (suc n) a

  tabulate : ∀ n → (Fin n → A) → A ^ n
  tabulate 0      f = []
  tabulate 1      f = f zero
  tabulate (2+ n) f = f zero , tabulate (suc n) (f ∘′ suc)

  append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n)
  append 0      n xs       ys = ys
  append 1      n x        ys = cons n x ys
  append (2+ m) n (x , xs) ys = x , append (suc m) n xs ys

  splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n
  splitAt 0       n xs = [] , xs
  splitAt (suc m) n xs =
    let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
    cons m (head (m Nat.+ n) xs) ys , zs

-- Manipulating N-ary products
------------------------------------------------------------------------

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

  map : (A → B) → ∀ n → A ^ n → B ^ n
  map f 0      as       = lift tt
  map f 1      a        = f a
  map f (2+ n) (a , as) = f a , map f (suc n) as

  ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n
  ap 0      fs       ts       = []
  ap 1      f        t        = f t
  ap (2+ n) (f , fs) (t , ts) = f t , ap (suc n) fs ts

module _ {a p} {A : Set a} {P : ℕ → Set p} where

  foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
          ∀ n → A ^ n → P n
  foldr p0 p1 p2+ 0      as       = p0
  foldr p0 p1 p2+ 1      a        = p1 a
  foldr p0 p1 p2+ (2+ n) (a , as) = p2+ n a (foldr p0 p1 p2+ (suc n) as)

foldl : ∀ {a p} {A : Set a} (P : ℕ → Set p) →
        P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
        ∀ n → A ^ n → P n
foldl P p0 p1 p2+ 0      as       = p0
foldl P p0 p1 p2+ 1      a        = p1 a
foldl P p0 p1 p2+ (2+ n) (a , as) = let p1′ = p1 a in
  foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) (suc n) as

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

  reverse : ∀ n → A ^ n → A ^ n
  reverse = foldl (A ^_) [] id (λ n → _,_)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

  zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
  zipWith f 0      as       bs       = []
  zipWith f 1      a        b        = f a b
  zipWith f (2+ n) (a , as) (b , bs) = f a b , zipWith f (suc n) as bs

  unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
  unzipWith f 0      as       = [] , []
  unzipWith f 1      a        = f a
  unzipWith f (2+ n) (a , as) = P.zip _,_ _,_ (f a) (unzipWith f (suc n) as)

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

  zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n
  zip = zipWith _,_

  unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
  unzip = unzipWith id


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Concrete.System.Parameters
import LibraBFT.Concrete.Properties.VotesOnce as VO
import LibraBFT.Concrete.Properties.LockedRound as LR

open import LibraBFT.Yasm.Properties ConcSysParms

-- This module collects in one place the obligations an
-- implementation must meet in order to enjoy the properties
-- proved in Abstract.Properties.

module LibraBFT.Concrete.Obligations where

  record ImplObligations : Set₁ where
    field
      -- Structural obligations:
      sps-cor : StepPeerState-AllValidParts

      -- Semantic obligations:
      --
      -- VotesOnce:
      vo₁ : VO.ImplObligation₁
      vo₂ : VO.ImplObligation₂

      -- LockedRound:
      lr₁ : LR.ImplObligation₁


text:
-- Andreas, 2016-11-03, issue #2291, reported by Aerate

-- {-# OPTIONS -v interaction.helper:100 #-}

record Foo : Set where
  coinductive
  field one : Foo
open Foo

someFoo : Foo
someFoo .one = {! {R} -> Foo.one R !}

-- WAS: C-c C-h gives:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs:1248

-- NOW:
-- Expected an argument of the form f e1 e2 .. en
-- when checking that the expression ? has type Foo


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

open import Cubical.Core.Everything

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

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

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

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

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

diagonal-unit : Unit ≡ Unit × Unit
diagonal-unit = isoToPath (iso (λ x → tt , tt) (λ x → tt) (λ {(tt , tt) i → tt , tt}) λ {tt i → tt})
  where open import Cubical.Foundations.Isomorphism


text:
module Axiom.FunctionExtensionality where

open import Level using (zero)
open import Relation.Binary.PropositionalEquality

postulate
  fun-ext : Extensionality zero zero

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


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

open import Oscar.Prelude
open import Oscar.Class

-- classes
open import Oscar.Class.Transitivity

-- data
open import Oscar.Data.Substitunction
open import Oscar.Data.Term

module Test.EquivalentCandidates where

module _
  {a}
  where

  instance

    𝓣ransitivityFunction₁ : Transitivity.class Function⟦ a ⟧
    𝓣ransitivityFunction₁ .⋆ f g = g ∘ f

    𝓣ransitivityFunction₂ : Transitivity.class Function⟦ a ⟧
    𝓣ransitivityFunction₂ .⋆ f g = g ∘ f

module _ (𝔓 : Ø₀) where

  open Substitunction 𝔓
  open Term 𝔓

  non-unique non-unique-2-hole unique-1-hole unsolved-meta :
    ∀ {m n} (f : Substitunction m n) → Substitunction m n
  non-unique {m} {n} f = {!transitivity {𝔒 = Ø₀} f (¡ {𝔒 = Term n})!}
  {-
  Candidates:
    [ 𝓣ransitivityFunction₁ : {a : Ł} → Transitivity.class Function⟦ a ⟧
    , 𝓣ransitivityFunction₂ : {a : Ł} → Transitivity.class Function⟦ a ⟧ ]
  -}
  non-unique-2-hole f = {!transitivity {𝔒 = Ø₀} {!!} {!!}!}
  {-
  Candidates:
    [ 𝓣ransitivityFunction₁ : {a : Ł} → Transitivity.class Function⟦ a ⟧
    , 𝓣ransitivityFunction₂ : {a : Ł} → Transitivity.class Function⟦ a ⟧ ]
  -}
  unique-1-hole f = transitivity {_∼_ = Function} f {!!}
  unsolved-meta {m} {n} f = transitivity {𝔒 = Ø₀} ⦃ {!!} ⦄ f (¡ {𝔒 = Term n})


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

open import MultiSorted.AlgebraicTheory

import MultiSorted.Interpretation as Interpretation
import MultiSorted.SyntacticCategory as SyntacticCategory
import MultiSorted.Substitution as Substitution
import Agda.Builtin.Equality as Eq
open import Relation.Binary.PropositionalEquality using (_≡_; refl ; cong)

module MultiSorted.UniversalInterpretation
  {ℓt}
  {𝓈 ℴ}
  {Σ : Signature {𝓈} {ℴ}}
  (T : Theory ℓt Σ) where

  open Theory T
  open Substitution T
  open SyntacticCategory T

  -- The universal interpretation in the syntactic category
  interp-oper-𝒮 : ∀ (f : oper) → (prod-𝒮 (oper-arity f)) ⇒s (ctx-slot (oper-sort f))
  interp-oper-𝒮 f _ = tm-oper f λ i → tm-var i

  ℐ : Interpretation.Interpretation Σ cartesian-𝒮
  ℐ =
    record
     { interp-sort = ctx-slot
     ; interp-ctx = producted-𝒮
     ; interp-oper = interp-oper-𝒮
     }

  open Interpretation.Interpretation ℐ

  interp-term-self : ∀ {Γ} {A} (t : Term Γ A) (y : var (interp-sort A)) → ⊢ Γ ∥ (interp-term t y) ≈ t ⦂ A
  interp-term-self (tm-var x) _ = eq-refl
  interp-term-self (tm-oper f xs) _ =  eq-congr (λ i → interp-term-self (xs i) var-var)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt