text:
------------------------------------------------------------------------
-- A memoising backend
------------------------------------------------------------------------

-- This code has bitrotted.

-- Following Frost/Szydlowski and Frost/Hafiz/Callaghan (but without
-- the left recursion fix). An improvement has been made: The user
-- does not have to insert memoisation annotations manually. Instead
-- all grammar nonterminals are memoised. This is perhaps a bit less
-- flexible, but less error-prone, since there is no need to guarantee
-- that all "keys" (arguments to the memoise combinator) are unique
-- (assuming that the nonterminal equality is strong enough).

open import Relation.Binary
import Relation.Binary.PropositionalEquality  as PropEq
import Relation.Binary.PropositionalEquality1 as PropEq1
open PropEq  using (_≡_)
open PropEq1 using (_≡₁_)
open import StructurallyRecursiveDescentParsing.Index
open import Data.Product as Prod

module StructurallyRecursiveDescentParsing.Memoised

  -- In order to be able to store results in a memo table (and avoid
  -- having to lift the table code to Set1) the result types have to
  -- come from the following universe:

  {Result : Set} (⟦_⟧ : Result → Set)

  -- Nonterminals also have to be small enough:

  {NT : Index → Result → Set} {LargeNT : NonTerminalType}
  (resultType : ∀ {i r} → LargeNT i r → Result)
  (resultTypeCorrect : ∀ {i r} (x : LargeNT i r) →
                       ⟦ resultType x ⟧ ≡₁ r)
  (notTooLarge : ∀ {i r} (x : LargeNT i r) → NT i (resultType x))

  -- Furthermore nonterminals need to be ordered, so that they can be
  -- used as memo table keys:

  {_≈_ _<_ : Rel (∃₂ NT)}
  (ntOrdered : IsStrictTotalOrder _≈_ _<_)

  -- And the underlying equality needs to be strong enough:

  (indicesEqual : _≈_ =[ (λ irx → (proj₁ irx , proj₁ (proj₂ irx))) ]⇒
                  _≡_ {Index × Result})

  -- Token type:

  {Tok : Set}

  where

open import Data.Bool renaming (true to ⊤; false to ⊥)
import Data.Nat as Nat
open Nat using (ℕ; zero; suc; pred; z≤n; s≤s)
import Data.Nat.Properties as NatProp
open import Function using (_∘_; _on_)
import Data.Vec  as Vec;  open Vec  using (Vec;  []; _∷_)
import Data.List as List; open List using (List; []; _∷_)
open import Data.Sum
open import Data.Maybe
open import Relation.Binary.OrderMorphism hiding (_∘_)
open _⇒-Poset_
import Relation.Binary.On as On
import Relation.Binary.Props.StrictTotalOrder as STOProps
open STOProps NatProp.strictTotalOrder

import StructurallyRecursiveDescentParsing.Memoised.Monad as Monad
open import StructurallyRecursiveDescentParsing.Type
open import StructurallyRecursiveDescentParsing.Utilities
  renaming (_∘_ to _∘′_)

------------------------------------------------------------------------
-- Some monotone functions

MonoFun : Set
MonoFun = poset ⇒-Poset poset

suc-mono : _≤_ =[ suc ]⇒ _≤_
suc-mono (inj₁ i<j)    = inj₁ (s≤s i<j)
suc-mono (inj₂ ≡-refl) = inj₂ ≡-refl

pred-mono : _≤_ =[ pred ]⇒ _≤_
pred-mono (inj₁ (s≤s (z≤n {zero})))  = inj₂ PropEq.refl
pred-mono (inj₁ (s≤s (z≤n {suc j}))) = inj₁ (s≤s z≤n)
pred-mono (inj₁ (s≤s (s≤s i<j)))     = inj₁ (s≤s i<j)
pred-mono (inj₂ PropEq.refl)         = inj₂ PropEq.refl

sucM : MonoFun
sucM = record
  { fun      = suc
  ; monotone = suc-mono
  }

predM : MonoFun
predM = record
  { fun      = pred
  ; monotone = pred-mono
  }

maybePredM : Empty → MonoFun
maybePredM e = if e then id else predM

lemma : ∀ e pos → fun (maybePredM e) pos ≤ pos
lemma ⊤ pos       = refl
lemma ⊥ zero      = refl
lemma ⊥ (suc pos) = inj₁ (Poset.refl Nat.poset)

------------------------------------------------------------------------
-- Parser monad

data Key : MonoFun → Result → Set where
  key : ∀ {e c r} (nt : NT (e ◇ c) r) → Key (maybePredM e) r

shuffle : ∃₂ Key → ∃₂ NT
shuffle (._ , _ , key x) = (, , x)

_≈K_ : Rel (∃₂ Key)
_≈K_ = _≈_ on shuffle

_<K_ : Rel (∃₂ Key)
_<K_ = _<_ on shuffle

ordered : IsStrictTotalOrder _≈K_ _<K_
ordered = On.isStrictTotalOrder shuffle ntOrdered

funsEqual : _≈K_ =[ proj₁ ]⇒ _≡_
funsEqual {(._ , _ , key _)} {(._ , _ , key _)} eq =
  PropEq.cong (maybePredM ∘ empty ∘ proj₁) (indicesEqual eq)

resultsEqual : _≈K_ =[ (λ rfk → proj₁ (proj₂ rfk)) ]⇒ _≡_
resultsEqual {(._ , _ , key _)} {(._ , _ , key _)} eq =
  PropEq.cong proj₂ (indicesEqual eq)

open Monad
       (StrictTotalOrder.isStrictTotalOrder NatProp.strictTotalOrder)
       (Vec Tok)
       ⟦_⟧
       ordered
       (λ {k₁} {k₂} → funsEqual    {k₁} {k₂})
       (λ {k₁} {k₂} → resultsEqual {k₁} {k₂})
open PM
  renaming ( return to return′
           ; _>>=_  to _>>=′_
           ; _=<<_  to _=<<′_
           ; ∅      to fail′
           ; _∣_    to _∣′_
           )

cast : ∀ {bnd f A₁ A₂} → A₁ ≡₁ A₂ → P bnd f A₁ → P bnd f A₂
cast refl p = p

------------------------------------------------------------------------
-- Run function for the parsers

-- Some helper functions.

private

  -- Extracts the first element from the input, if any.

  eat : ∀ {bnd} (inp : Input≤ bnd) →
        Maybe Tok × Input≤ (pred (position inp))
  eat {bnd} xs = helper (bounded xs) (string xs)
    where
    helper : ∀ {pos} → pos ≤ bnd → Vec Tok pos →
             Maybe Tok × Input≤ (pred pos)
    helper _  []       = (nothing , [] isBounded∶ refl)
    helper le (c ∷ cs) = (just c  , cs isBounded∶ refl)

  -- Fails if it encounters nothing.

  fromJust : ∀ {bnd} → Maybe Tok → P bnd idM Tok
  fromJust nothing  = fail′
  fromJust (just c) = return′ c

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

private

 module Dummy (g : Grammar LargeNT Tok) where

  mutual
    parse : ∀ n {e c R} →
            Parser LargeNT Tok (e ◇ c) R →
            P n (if e then idM else predM) R
    parse n       (return x)          = return′ x
    parse n       (_∣_ {⊤}     p₁ p₂) = parse  n      p₁   ∣′ parse↑ n    p₂
    parse n       (_∣_ {⊥} {⊤} p₁ p₂) = parse↑ n      p₁   ∣′ parse  n    p₂
    parse n       (_∣_ {⊥} {⊥} p₁ p₂) = parse  n      p₁   ∣′ parse  n    p₂
    parse n       (p₁ ?>>= p₂)        = parse  n      p₁ >>=′ parse  n ∘′ p₂
    parse (suc n) (p₁ !>>= p₂)        = parse (suc n) p₁ >>=′ parse↑ n ∘′ p₂
    parse zero    (p₁ !>>= p₂)        = fail′
    parse n       fail                = fail′
    parse n       token               = fromJust =<<′ gmodify predM eat
    parse n       (! x)               = memoParse n x

    parse↑ : ∀ n {e c R} → Parser LargeNT Tok (e ◇ c) R → P n idM R
    parse↑ n {e} p = adjustBound (lemma e) (parse n p)

    memoParse : ∀ n {R e c} → LargeNT (e ◇ c) R →
                P n (if e then idM else predM) R
    memoParse n x = cast₁ (memoise k (cast₂ (parse n (g x))))
      where
      k     = key (notTooLarge x)
      cast₁ = cast (resultTypeCorrect x)
      cast₂ = cast (sym (resultTypeCorrect x))

-- Exported run function.

parse : ∀ {i R} →
        Grammar LargeNT Tok → Parser LargeNT Tok i R →
        List Tok → List (R × List Tok)
parse g p toks =
  List.map (Prod.map id (λ xs → Vec.toList (string xs))) $
  run (Vec.fromList toks) (Dummy.parse g _ p)

-- A variant which only returns parses which leave no remaining input.

parse-complete : ∀ {i R} →
                 Grammar Tok LargeNT → Parser Tok LargeNT i R →
                 List Tok → List R
parse-complete g p s =
  List.map proj₁ (List.filter (List.null ∘ proj₂) (parse g p s))

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

postulate
  _↦_ : {A : Set} → A → A → Set
{-# BUILTIN REWRITE _↦_ #-}

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

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

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

apd : {A : Set} {B : A → Set} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → f x == f y [ B ↓ p ]
apd f idp = idp

module Disk where

module _ where

  postulate -- HIT
    Disk : Set
    baseD : Disk
    loopD : baseD == baseD
    drumD : loopD == idp

  module DiskElim {P : Disk → Set}
    (baseD* : P baseD )
    (loopD* : baseD* == baseD* [ P ↓ loopD ] )
    (drumD* : loopD* == idp [ ((λ p → baseD* == baseD* [ P ↓ p ] ) ) ↓ drumD ] ) where

    postulate
      f : (x : Disk) → P x
      baseD-β : f baseD ↦ baseD*
      {-# REWRITE baseD-β #-}

    postulate
      loopD-ι : apd f loopD ↦ loopD*
    {-# REWRITE loopD-ι #-}

    postulate
      drumD-ι : apd (apd f) drumD ↦ drumD*
    {-# REWRITE drumD-ι #-}

    loopD-β : apd f loopD == loopD*
    loopD-β = idp

    drumD-β : apd (apd f) drumD == drumD*
    drumD-β = idp

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where

import Algebra.Properties.AbelianGroup as AGP
open import Data.Product
open import Function
import Relation.Binary.EqReasoning as EqR

open Ring R
open EqR setoid

open AGP +-abelianGroup public
  renaming ( ⁻¹-involutive to -‿involutive
           ; left-identity-unique to +-left-identity-unique
           ; right-identity-unique to +-right-identity-unique
           ; identity-unique to +-identity-unique
           ; left-inverse-unique to +-left-inverse-unique
           ; right-inverse-unique to +-right-inverse-unique
           ; ⁻¹-∙-comm to -‿+-comm
           )

-‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
-‿*-distribˡ x y = begin
  - x * y                        ≈⟨ sym $ proj₂ +-identity _ ⟩
  - x * y + 0#                   ≈⟨ refl ⟨ +-cong ⟩ sym (proj₂ -‿inverse _) ⟩
  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc _ _ _  ⟩
  - x * y + x * y + - (x * y)    ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-cong ⟩ refl ⟩
  (- x + x) * y + - (x * y)      ≈⟨ (proj₁ -‿inverse _ ⟨ *-cong ⟩ refl)
                                      ⟨ +-cong ⟩
                                    refl ⟩
  0# * y + - (x * y)             ≈⟨ proj₁ zero _ ⟨ +-cong ⟩ refl ⟩
  0# + - (x * y)                 ≈⟨ proj₁ +-identity _ ⟩
  - (x * y)                      ∎

-‿*-distribʳ : ∀ x y → x * - y ≈ - (x * y)
-‿*-distribʳ x y = begin
  x * - y                        ≈⟨ sym $ proj₁ +-identity _ ⟩
  0# + x * - y                   ≈⟨ sym (proj₁ -‿inverse _) ⟨ +-cong ⟩ refl ⟩
  - (x * y) + x * y + x * - y    ≈⟨ +-assoc _ _ _  ⟩
  - (x * y) + (x * y + x * - y)  ≈⟨ refl ⟨ +-cong ⟩ sym (proj₁ distrib _ _ _)  ⟩
  - (x * y) + x * (y + - y)      ≈⟨ refl ⟨ +-cong ⟩ (refl ⟨ *-cong ⟩ proj₂ -‿inverse _) ⟩
  - (x * y) + x * 0#             ≈⟨ refl ⟨ +-cong ⟩ proj₂ zero _ ⟩
  - (x * y) + 0#                 ≈⟨ proj₂ +-identity _ ⟩
  - (x * y)                      ∎


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[X]X-A where

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

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
open import Cubical.Data.Empty as ⊥

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient

open import Cubical.Relation.Nullary

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Functions

module Properties-Equiv-QuotientXn-A
  (Ar@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  open CommRingStr Astr using ()
    renaming
    ( 0r        to 0A
    ; 1r        to 1A
    ; _+_       to _+A_
    ; -_        to -A_
    ; _·_       to _·A_
    ; +Assoc    to +AAssoc
    ; +Identity to +AIdentity
    ; +Lid      to +ALid
    ; +Rid      to +ARid
    ; +Inv      to +AInv
    ; +Linv     to +ALinv
    ; +Rinv     to +ARinv
    ; +Comm     to +AComm
    ; ·Assoc    to ·AAssoc
    ; ·Identity to ·AIdentity
    ; ·Lid      to ·ALid
    ; ·Rid      to ·ARid
    ; ·Rdist+   to ·ARdist+
    ; ·Ldist+   to ·ALdist+
    ; is-set    to isSetA     )

  open CommRingStr (snd (A[X1,···,Xn] Ar n) ) using ()
    renaming
    ( 0r        to 0PA
    ; 1r        to 1PA
    ; _+_       to _+PA_
    ; -_        to -PA_
    ; _·_       to _·PA_
    ; +Assoc    to +PAAssoc
    ; +Identity to +PAIdentity
    ; +Lid      to +PALid
    ; +Rid      to +PARid
    ; +Inv      to +PAInv
    ; +Linv     to +PALinv
    ; +Rinv     to +PARinv
    ; +Comm     to +PAComm
    ; ·Assoc    to ·PAAssoc
    ; ·Identity to ·PAIdentity
    ; ·Lid      to ·PALid
    ; ·Rid      to ·PARid
    ; ·Comm     to ·PAComm
    ; ·Rdist+   to ·PARdist+
    ; ·Ldist+   to ·PALdist+
    ; is-set    to isSetPA     )

  open CommRingStr (snd (A[X1,···,Xn]/<X1,···,Xn> Ar n)) using ()
    renaming
    ( 0r        to 0PAI
    ; 1r        to 1PAI
    ; _+_       to _+PAI_
    ; -_        to -PAI_
    ; _·_       to _·PAI_
    ; +Assoc    to +PAIAssoc
    ; +Identity to +PAIIdentity
    ; +Lid      to +PAILid
    ; +Rid      to +PAIRid
    ; +Inv      to +PAIInv
    ; +Linv     to +PAILinv
    ; +Rinv     to +PAIRinv
    ; +Comm     to +PAIComm
    ; ·Assoc    to ·PAIAssoc
    ; ·Identity to ·PAIIdentity
    ; ·Lid      to ·PAILid
    ; ·Rid      to ·PAIRid
    ; ·Rdist+   to ·PAIRdist+
    ; ·Ldist+   to ·PAILdist+
    ; is-set    to isSetPAI     )

  open RingTheory

  discreteVecℕn = VecPath.discreteA→discreteVecA discreteℕ n

-----------------------------------------------------------------------------
-- Direct sens

  PA→A : A[x1,···,xn] Ar n → A
  PA→A = Poly-Rec-Set.f Ar n _ isSetA
          0A
          base-trad
          _+A_
          +AAssoc
          +ARid
          +AComm
          base-0P-eq
          base-Poly+-eq
        where
        base-trad : (v : Vec ℕ n) → (a : A) → A
        base-trad v a with (discreteVecℕn v (replicate 0))
        ... | yes p = a
        ... | no ¬p = 0A

        base-0P-eq : (v : Vec ℕ n) → base-trad v 0A ≡ 0A
        base-0P-eq v with (discreteVecℕn v (replicate 0))
        ... | yes p = refl
        ... | no ¬p = refl

        base-Poly+-eq : (v : Vec ℕ n) → (a b : A) → base-trad v a +A base-trad v b ≡ base-trad v (a +A b)
        base-Poly+-eq v a b with (discreteVecℕn v (replicate 0))
        ... | yes p = refl
        ... | no ¬p = +ARid _

  PA→A-pres1 :  PA→A 1PA ≡ 1A
  PA→A-pres1 with (discreteVecℕn (replicate 0) (replicate 0))
  ... | yes p = refl
  ... | no ¬p = ⊥.rec (¬p refl)

  PA→A-pres+ : (P Q : A[x1,···,xn] Ar n) → PA→A (P +PA Q) ≡ PA→A P +A PA→A Q
  PA→A-pres+ P Q = refl

  PA→A-pres· : (P Q : A[x1,···,xn] Ar n) → PA→A (P ·PA Q) ≡ PA→A P ·A PA→A Q
  PA→A-pres· = Poly-Ind-Prop.f _ _ _
               (λ P u v i Q → isSetA _ _ (u Q) (v Q) i)
               (λ Q → sym (0LeftAnnihilates (CommRing→Ring Ar) _))
               (λ v a → Poly-Ind-Prop.f _ _ _ (λ Q → isSetA _ _)
                         (sym (0RightAnnihilates (CommRing→Ring Ar) _))
                         (λ v' a' → base-base-eq a a' v v')
                         λ {U V} ind-U ind-V → cong₂ _+A_ ind-U ind-V ∙ sym (·ARdist+ _ _ _))
               λ {U V} ind-U ind-V Q → cong₂ _+A_ (ind-U Q) (ind-V Q) ∙ sym (·ALdist+ _ _ _)
               where
               base-base-eq : (a a' : A) → (v v' : Vec ℕ n) →
                              PA→A (base v a ·PA base v' a') ≡ PA→A (base v a) ·A PA→A (base v' a')
               base-base-eq a a' v v' with (discreteVecℕn (v +n-vec v') (replicate 0))
                                           | (discreteVecℕn v (replicate 0))
                                           | (discreteVecℕn v' (replicate 0))
               ... | yes r | yes p | yes e = refl
               ... | yes r | yes p | no ¬q = ⊥.rec (¬q (snd (+n-vecSplitReplicate0 v v' r)))
               ... | yes r | no ¬p | q     = ⊥.rec (¬p (fst (+n-vecSplitReplicate0 v v' r)))
               ... | no ¬r | yes p | yes q = ⊥.rec (¬r (cong₂ _+n-vec_ p q ∙ +n-vec-rid _))
               ... | no ¬r | yes p | no ¬q = sym (0RightAnnihilates (CommRing→Ring Ar) _)
               ... | no ¬r | no ¬p | yes q = sym (0LeftAnnihilates (CommRing→Ring Ar) _)
               ... | no ¬r | no ¬p | no ¬q = sym (0RightAnnihilates (CommRing→Ring Ar) _)

  PA→A-cancel : (k : Fin n) → PA→A (<X1,···,Xn> Ar n k) ≡ 0A
  PA→A-cancel k with (discreteVecℕn (δℕ-Vec n (toℕ k)) (replicate 0))
  ... | yes p = ⊥.rec (δℕ-Vec-k<n→≢ n (toℕ k) (toℕ<n k) p)
  ... | no ¬p = refl

  PAr→Ar : CommRingHom (A[X1,···,Xn] Ar n) Ar
  fst PAr→Ar = PA→A
  snd PAr→Ar = makeIsRingHom PA→A-pres1 PA→A-pres+ PA→A-pres·

  PAIr→Ar : CommRingHom (A[X1,···,Xn]/<X1,···,Xn> Ar n) Ar
  PAIr→Ar = Quotient-FGideal-CommRing-CommRing.f (A[X1,···,Xn] Ar n) Ar PAr→Ar (<X1,···,Xn> Ar n) PA→A-cancel

  PAI→A : A[x1,···,xn]/<x1,···,xn> Ar n → A
  PAI→A = fst PAIr→Ar

-----------------------------------------------------------------------------
-- Converse sens

  A→PA : A → A[x1,···,xn] Ar n
  A→PA a = (base (replicate 0) a)

  A→PA-pres1 : A→PA 1A ≡ 1PA
  A→PA-pres1 = refl

  A→PA-pres+ : (a a' : A) → A→PA (a +A a') ≡ (A→PA a) +PA (A→PA a')
  A→PA-pres+ a a' = sym (base-poly+ _ _ _)

  A→PA-pres· : (a a' : A) → A→PA (a ·A a') ≡ (A→PA a) ·PA (A→PA a')
  A→PA-pres· a a' = cong (λ X → base X (a ·A a')) (sym (+n-vec-rid _))

  A→PAI : A → (A[x1,···,xn]/<x1,···,xn> Ar n)
  A→PAI = [_] ∘ A→PA

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

  e-sect : (a : A) → PAI→A (A→PAI a) ≡ a
  e-sect a with (discreteVecℕn (replicate 0) (replicate 0))
  ... | yes p = refl
  ... | no ¬p = ⊥.rec (¬p refl)

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

  open RingStr
  open IsRing

  e-retr : (x : A[x1,···,xn]/<x1,···,xn> Ar n) → A→PAI (PAI→A x) ≡ x
  e-retr = SQ.elimProp (λ _ → isSetPAI _ _)
           (Poly-Ind-Prop.f _ _ _ (λ _ → isSetPAI _ _)
           base0-eq
           base-eq
           λ {U V} ind-U ind-V → cong [_] (A→PA-pres+ _ _) ∙ cong₂ _+PAI_ ind-U ind-V)
           where
           base0-eq : A→PAI (PAI→A [ 0P ]) ≡ [ 0P ]
           base0-eq = cong [_] (base-0P (replicate 0))

           base-eq : (v : Vec ℕ n) → (a : A ) → [ A→PA (PA→A (base v a)) ] ≡ [ base v a ]
           base-eq v a with (discreteVecℕn v (replicate 0))
           ... | yes p = cong [_] (cong (λ X → base X a) (sym p))
           ... | no ¬p with (pred-vec-≢0 v ¬p)
           ... | k , v' , infkn , eqvv' = eq/ (base (replicate 0) 0A)
                                             (base v a) ∣ ((genδ-FinVec n k (base v' (-A a)) 0PA) , helper) ∣₁
               where
               helper : _
               helper = cong (λ X → X poly+ base v (-A a)) (base-0P (replicate 0))
                        ∙ +PALid (base v (-A a))
                        ∙ sym (
                          genδ-FinVec-ℕLinearCombi ((A[X1,···,Xn] Ar n)) n k infkn (base v' (-A a)) (<X1,···,Xn> Ar n)
                          ∙ cong₂ base (cong (λ X → v' +n-vec δℕ-Vec n X) (toFromId' n k infkn)) (·ARid _)
                          ∙ cong (λ X → base X (-A a)) (sym eqvv'))

-----------------------------------------------------------------------------
-- Equiv

module _
  (Ar@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  open Iso
  open Properties-Equiv-QuotientXn-A Ar n

  Equiv-QuotientX-A : CommRingEquiv (A[X1,···,Xn]/<X1,···,Xn> Ar n) Ar
  fst Equiv-QuotientX-A = isoToEquiv is
    where
    is : Iso (A[x1,···,xn]/<x1,···,xn> Ar n) A
    fun is = PAI→A
    inv is = A→PAI
    rightInv is = e-sect
    leftInv is = e-retr
  snd Equiv-QuotientX-A = snd PAIr→Ar

-- Warning this doesn't prove Z[X]/X ≅ ℤ because you get two definition,
-- see notation Multivariate-Quotient-notationZ for more details

max_stars_repo_name: xekoukou/cubical

max_issues_repo_name: xekoukou/cubical

max_forks_repo_name: xekoukou/cubical


text:
open import Categories
open import Functors
open import RMonads

module RMonads.CatofRAdj.TermRAdjHom {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}
                                     {J : Fun C D}(M : RMonad J) where

open import Library
open import RAdjunctions
open import RMonads.CatofRAdj M
open import Categories.Terminal
open import RMonads.REM M
open import RMonads.REM.Adjunction M
open import RAdjunctions.RAdj2RMon
open import RMonads.CatofRAdj.TermRAdjObj M

open Cat
open Fun
open RAdj

alaw1lem : ∀{e f}{E : Cat {e}{f}}(T : Fun C D)(L : Fun C E)(R : Fun E D)
  (p : R ○ L ≅ T)
  (η : ∀ {X} → Hom D (OMap J X) (OMap T X)) →
  (right : ∀ {X Y} → Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y) →
  (left : ∀ {X Y} → Hom E (OMap L X) Y → Hom D (OMap J X) (OMap R Y)) →
  (ηlaw : ∀ {X} → left (iden E {OMap L X}) ≅ η {X}) →
  ∀ {X}{Z}{f : Hom D (OMap J Z) (OMap R X)} →
  (nat : comp D (HMap R (right f)) (comp D (left (iden E)) (HMap J (iden C)))
         ≅
         left (comp E (right f) (comp E (iden E) (HMap L (iden C))))) →
  (lawb : left (right f) ≅ f) →
  f
  ≅
  comp D (subst (λ Z → Hom D Z (OMap R X))
                (fcong Z (cong OMap p))
                (HMap R (right f)))
         η
alaw1lem {E = E} .(R ○ L) L R refl η right left ηlaw {X}{Z}{f} nat lawb =
  trans (trans (trans (sym lawb)
                      (cong left
                            (trans (sym (idr E))
                                   (cong (comp E (right f))
                                         (trans (sym (fid L))
                                                (sym (idl E)))))))
               (trans (sym nat)
                      (cong (comp D (HMap R (right f)))
                            (trans (cong (comp D (left (iden E))) (fid J))
                                   (idr D)))))
        (cong (comp D (HMap R (right f))) ηlaw)

alaw2lem : ∀{e f}{E : Cat {e}{f}}(T : Fun C D)(L : Fun C E)(R : Fun E D)
  (p : R ○ L ≅ T) →
  (right : ∀ {X Y} → Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y) →
  (bind : ∀{X Y} →
          Hom D (OMap J X) (OMap T Y) → Hom D (OMap T X) (OMap T Y)) →
  (natright : {X X' : Obj C} {Y Y' : Obj E} (f : Hom C X' X)
    (g : Hom E Y Y') (h : Hom D (OMap J X) (OMap R Y)) →
    right (comp D (HMap R g) (comp D h (HMap J f)))
    ≅
    comp E g (comp E (right h) (HMap L f))) →
  ∀{X}{Z}{W}
  {k : Hom D (OMap J Z) (OMap T W)}
  {f : Hom D (OMap J W) (OMap R X)} →
  (bindlaw : HMap R (right (subst (Hom D (OMap J Z))
                           (fcong W (cong OMap (sym p)))
                           k))
             ≅
             bind k) →
  subst (λ Z → Hom D Z (OMap R X))
  (fcong Z (cong OMap p))
  (HMap R
   (right
    (comp D
     (subst (λ Z → Hom D Z (OMap R X))
      (fcong W (cong OMap p)) (HMap R (right f)))
     k)))
  ≅
  comp D
  (subst (λ Z → Hom D Z (OMap R X))
   (fcong W (cong OMap p)) (HMap R (right f)))
  (bind k)
alaw2lem {E = E} .(R ○ L) L R refl right bind natright {k = k}{f = f} bl =
  trans (trans (cong (HMap R)
                     (trans (cong (λ k → right (comp D (HMap R (right f)) k))
                                  (trans (sym (idr D)) (cong (comp D k)
                                                             (sym (fid J)))))
                            (trans (trans (natright (iden C) (right f) k)
                                          (trans (sym (ass E))
                                                 (cong (comp E
                                                             (comp E
                                                                   (right f)
                                                                   (right k)))
                                                       (fid L))))
                                   (idr E))))
               (fcomp R))
        (cong (comp D (HMap R (right f))) bl)

ahomlem : ∀{e f}{E : Cat {e}{f}}(T : Fun C D)(L : Fun C E)(R : Fun E D)
  (p : R ○ L ≅ T) →
  (right : ∀ {X Y} → Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y) →
  (natright : {X X' : Obj C} {Y Y' : Obj E} (f : Hom C X' X)
    (g : Hom E Y Y') (h : Hom D (OMap J X) (OMap R Y)) →
    right (comp D (HMap R g) (comp D h (HMap J f)))
    ≅
    comp E g (comp E (right h) (HMap L f))) →
  {X : Obj E}{Y : Obj E}{f : Hom E X Y} →
  {Z : Obj C} {g : Hom D (OMap J Z) (OMap R X)} →
  comp D (HMap R f)
  (subst (λ Z → Hom D Z (OMap R X))
   (fcong Z (cong OMap p))
   (HMap R (right g)))
  ≅
  subst (λ Z → Hom D Z (OMap R Y))
  (fcong Z (cong OMap p))
  (HMap R (right (comp D (HMap R f) g)))
ahomlem {E = E} .(R ○ L) L R refl right natright {X}{Y}{f}{Z}{g} =
  trans (sym (fcomp R))
        (cong (HMap R)
              (trans (trans (sym (idr E))
                            (trans (cong (comp E (comp E f (right g)))
                                         (sym (fid L)))
                                   (trans (ass E)
                                          (sym (natright (iden C) f g)))))
                     (cong (λ g → right (comp D (HMap R f) g))
                           (trans (cong (comp D g) (fid J)) (idr D)))))
open ObjAdj

Llawlem : ∀{e f}{E : Cat {e}{f}}(T : Fun C D)(L : Fun C E)(R : Fun E D)
  (p : R ○ L ≅ T) →
  (right : ∀{X Y} → Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y) →
  (bind : ∀{X Y} →
          Hom D (OMap J X) (OMap T Y) → Hom D (OMap T X) (OMap T Y)) →
  (bindlaw : {X Y : Obj C} {f : Hom D (OMap J X) (OMap T Y)} →
    HMap R
    (right
     (subst (Hom D (OMap J X)) (fcong Y (cong OMap (sym p))) f))
    ≅ bind f) →
  ∀{X Z} →
  {f  : Hom D (OMap J Z) (OMap R (OMap L X))}
  {f' : Hom D (OMap J Z) (OMap T X)} → (q  : f ≅ f') →
  subst (λ Z → Hom D Z (OMap R (OMap L X)))
  (fcong Z (cong OMap p)) (HMap R (right f))
  ≅ bind f'
Llawlem .(R ○ L) L R refl right bind bindlaw {X}{Z}{f}{.f} refl = bindlaw

K : ∀{e f}(A : Obj (CatofAdj {e}{f})) → Fun (E A) (E EMObj)
K A = record {
  OMap = λ X → record {
    acar = OMap (R (adj A)) X;
    astr = λ {Z} f →
      subst (λ Z₁ → Hom D Z₁ (OMap (R (adj A)) X))
            (fcong Z (cong OMap (law A)))
            (HMap (R (adj A)) (right (adj A) f));
    alaw1 = λ {Z} {f} →
      alaw1lem
               (TFun M)
               (L (adj A))
               (R (adj A))
               (law A)
               η
               (right (adj A))
               (left (adj A))
               (ηlaw A)
               (natleft (adj A) (iden C) (right (adj A) f) (iden (E A)))
               (lawb (adj A) f);
    alaw2 = λ {Z} {W} {k} {f} →
      alaw2lem
               (TFun M)
               (L (adj A))
               (R (adj A))
               (law A)
               (right (adj A))
               bind
               (natright (adj A))
               (bindlaw A {_} {_} {k})};
  HMap = λ {X} {Y} f → record {
    amor = HMap (R (adj A)) f;
    ahom = λ {Z} {g} →
      ahomlem
              (TFun M)
              (L (adj A))
              (R (adj A))
              (law A)
              (right (adj A))
              (natright (adj A)) };
    fid = RAlgMorphEq (fid (R (adj A)));
    fcomp = RAlgMorphEq (fcomp (R (adj A)))}
  where open RMonad M

Llaw' : ∀{e f}(A : Obj (CatofAdj {e}{f})) →
        K A ○ L (adj A) ≅ L (adj EMObj)
Llaw' A = FunctorEq _ _
  (ext λ X → AlgEq (fcong X (cong OMap (law A)))
                   (iext λ Z → dext λ {f} {f'} →
                     Llawlem (TFun M)
                             (L (adj A))
                             (R (adj A))
                             (law A)
                             (right (adj A))
                             bind
                             (bindlaw A)))
  (iext λ X → iext λ Y → ext λ f →
      lemZ
      (AlgEq (fcong X (cong OMap (law A)))
       (iext λ Z →
          dext
          (Llawlem (TFun M) (L (adj A)) (R (adj A)) (law A) (right (adj A))
           bind (bindlaw A))))
      (AlgEq (fcong Y (cong OMap (law A)))
       (iext λ Z →
          dext
          (Llawlem (TFun M) (L (adj A)) (R (adj A)) (law A) (right (adj A))
           bind (bindlaw A))))
      (cong' refl
       (ext
        (λ _ →
           cong₂ (Hom D) (fcong X (cong OMap (law A)))
           (fcong Y (cong OMap (law A)))))
       (icong' refl
        (ext
         (λ Z →
            cong₂ (λ x y → Hom C X Z → Hom D x y) (fcong X (cong OMap (law A)))
            (fcong Z (cong OMap (law A)))))
        (icong' refl
         (ext
          (λ Z →
             cong
             (λ (F : Obj C → Obj D) →
                {Y₁ : Obj C} → Hom C Z Y₁ → Hom D (F Z) (F Y₁))
             (cong OMap (law A))))
         (cong HMap (law A)) (refl {x = X}))
        (refl {x = Y}))
       (refl {x = f})))
  where open RMonad M

Rlaw' : ∀{e f}(A : Obj (CatofAdj {e}{f})) →
        R (adj A) ≅ R (adj EMObj) ○ K A
Rlaw' A = FunctorEq _ _ refl refl

rightlaw' : ∀{e f}(A : Obj (CatofAdj {e}{f})) →
           {X : Obj C}{Y : Obj (E A)} →
           {f : Hom D (OMap J X) (OMap (R (adj A)) Y)} →
           HMap (K A) (right (adj A) f)
           ≅
           right (adj EMObj) {X} {OMap (K A) Y}
                 (subst (Hom D (OMap J X)) (fcong Y (cong OMap (Rlaw' A))) f)
rightlaw' A {X}{Y}{f} = lemZ
  (AlgEq (fcong X (cong OMap (law A)))
   (iext λ Z →
      dext
      (λ {g} {g'} p →
         Llawlem (TFun M) (L (adj A)) (R (adj A)) (law A) (right (adj A))
         bind (bindlaw A) p)))
  refl
  (trans
   (cong
    (λ (f₁ : Hom D (OMap J X) (OMap (R (adj A)) Y)) →
       HMap (R (adj A)) (right (adj A) f₁))
    (sym
       (stripsubst (Hom D (OMap J X)) f
        (fcong Y (cong OMap (Rlaw' A))))))
   (sym
    (stripsubst (λ (Z : Obj D) → Hom D Z (OMap (R (adj A)) Y)) _
     (fcong X (cong OMap (law A))))))
  where open RMonad M

EMHom : {A : Obj CatofAdj} → Hom CatofAdj A EMObj
EMHom {A} = record {
  K    = K A;
  Llaw = Llaw' A;
  Rlaw = Rlaw' A;
  rightlaw = rightlaw' A }

-- -}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatMinusOne.Base where

open import Cubical.Core.Primitives
open import Cubical.Data.Nat
open import Cubical.Data.Empty

record ℕ₋₁ : Type₀ where
  constructor -1+_
  field
    n : ℕ

pattern neg1 = -1+ zero
pattern ℕ→ℕ₋₁ n = -1+ (suc n)

1+_ : ℕ₋₁ → ℕ
1+_ (-1+ n) = n

suc₋₁ : ℕ₋₁ → ℕ₋₁
suc₋₁ (-1+ n) = -1+ (suc n)

-- Natural number and negative integer literals for ℕ₋₁

open import Cubical.Data.Nat.Literals public

instance
  fromNatℕ₋₁ : HasFromNat ℕ₋₁
  fromNatℕ₋₁ = record { Constraint = λ _ → Unit ; fromNat = ℕ→ℕ₋₁ }

instance
  fromNegℕ₋₁ : HasFromNeg ℕ₋₁
  fromNegℕ₋₁ = record { Constraint = λ { (suc (suc _)) → ⊥ ; _ → Unit }
                       ; fromNeg = λ { zero → 0 ; (suc zero) → neg1 } }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import HoTT
open import cohomology.ChainComplex
open import cohomology.Theory
open import groups.KernelImage
open import cw.CW

module cw.cohomology.ReconstructedCohomologyGroups {i : ULevel} (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  open import cw.cohomology.Descending OT
  open import cw.cohomology.ReconstructedCochainComplex OT
  open import cw.cohomology.ReconstructedZerothCohomologyGroup OT
  open import cw.cohomology.ReconstructedFirstCohomologyGroup OT
  open import cw.cohomology.ReconstructedHigherCohomologyGroups OT

  abstract
    reconstructed-cohomology-group : ∀ m {n} (⊙skel : ⊙Skeleton {i} n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      → C m ⊙⟦ ⊙skel ⟧ ≃ᴳ cohomology-group (cochain-complex ⊙skel) m
    reconstructed-cohomology-group (pos 0) ⊙skel ac =
      zeroth-cohomology-group ⊙skel ac
    reconstructed-cohomology-group (pos 1) ⊙skel ac =
      first-cohomology-group ⊙skel ac
    reconstructed-cohomology-group (pos (S (S m))) ⊙skel ac =
      higher-cohomology-group m ⊙skel ac
    reconstructed-cohomology-group (negsucc m) ⊙skel ac =
      lift-iso {j = i} ∘eᴳ trivial-iso-0ᴳ (C-cw-at-negsucc ⊙skel m ac)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Qsort where
open import Sec4                -- The module with definition of propositions
import Sec2

-- postulate needed for ≤ on A
postulate leq : {A : Set} → A → A → Prop
postulate geq : {A : Set} → A → A → Prop
postulate tot-list : {A : Set} → (a b : A) → (leq a  b) ∨ (leq b a)
postulate trans-list :  {A : Set} → (a b c : A) → (leq a b) → (leq b c) → (leq a c)

{-
  Definition of a list
-}
data List (A : Set) : Set where
  []  : List A                  -- Empty list
  _∷_ : A → List A → List A     -- Cons

-- Proposition stating what is a non empty list
nelist : {A : Set} → (List A) → Prop
nelist [] = ⊥
nelist (x ∷ x₁) = ⊤

-- Head function that only works on non empty list
head : {A : Set} → (l : List A) → (p : nelist l) → A
head [] ()                      -- This can never happen
head (x ∷ _) ⋆ = x              -- This is the head of the list

-- The tail of the list only works on non empty list
tail : {A : Set} → (l : List A) → (p : nelist l) → (List A)
tail [] ()
tail (_ ∷ l) ⋆ = l

data Bool : Set where
  True  : Bool
  False : Bool

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

-- Addition of natural numbers
_+_ : ℕ → ℕ → ℕ
Z + y = y
S x + y = S (x + y)

-- Relation on natural numbers
_≤_ : ℕ → ℕ → Prop
Z ≤ Z = ⊤
Z ≤ (S y) = ⊤
S x ≤ Z = ⊥
S x ≤ S y = x ≤ y

-- {-# BUILTIN NATURAL ℕ #-}
-- {-# BUILTIN BOOL Bool #-}

-- ≤ is reflexive
≤-ref : ∀ (x : ℕ) → (x ≤ x) → (x ≤ x)
≤-ref _ y = y

-- ≤ is not symmetric
-- ≤-sym : ∀ (x y : ℕ) → (x ≤ y) → (y ≤ x)
-- ≤-sym Z Z p = ⋆
-- ≤-sym Z (S y) ⋆ = {!!}
-- ≤-sym (S x) Z ()
-- ≤-sym (S x) (S y) p = ≤-sym x y p

-- ≤ is transitive
≤-trans : ∀ (x y z : ℕ) → (x ≤ y) → (y ≤ z) → (x ≤ z)
≤-trans Z Z Z p1 p2 = ⋆
≤-trans Z Z (S z) p1 p2 = ⋆
≤-trans Z (S y) Z p1 p2 = ⋆
≤-trans Z (S y) (S z) p1 p2 = ⋆
≤-trans (S x) Z z () p2
≤-trans (S x) (S y) Z p1 ()
≤-trans (S x) (S y) (S z) p1 p2 = ≤-trans x y z p1 p2

-- length of a list
length : {A : Set} → (List A) → ℕ
length [] = Z
length (x ∷ l) = (S Z) + (length l)

-- filter' on a list
filter' : {A : Set} → (A → Bool) → (l : List A)
         → List A
filter' f [] = []
filter' f (x ∷ l) with (f x)
filter' f (x ∷ l) | True = (x ∷ (filter' f l))
filter' f (x ∷ l) | False = filter' f l

≤-cong : ∀ (x y : ℕ) → (x ≤ y) → (x ≤ (S y))
≤-cong Z y p = ⋆
≤-cong (S x) Z ()
≤-cong (S x) (S y) p = ≤-cong x y p

thm-filter' : {A : Set} → (l : List A) → (f : A → Bool) → length (filter' f l) ≤ S (length l)
thm-filter' [] f = ⋆
thm-filter' (x ∷ l) f with (f x)
thm-filter' (x ∷ l) f | True = thm-filter' l f
thm-filter' (x ∷ l) f | False = ≤-cong (length (filter' f l)) (S (length l)) (thm-filter' l  f)

filter : {A : Set} → (A → Bool) → (l : List A)
         → Exists (List A) (λ l' → (length l') ≤ (length l))
filter f [] = [ [] , ⋆ ]
filter f (x ∷ l) = [ filter' f l , thm-filter' l f ]

-- append two lists
_++_ : {A : Set} → (l : List A) → (l' : List A) → (List A)
[] ++ l' = l'
(x ∷ l) ++ l' = (x ∷ (l ++ l'))

leq-nat : ℕ → ℕ → Bool
leq-nat Z  _ = True
leq-nat (S n) Z = False
leq-nat (S n) (S m) = leq-nat n m

_<_ : ℕ → ℕ → Bool
Z < (S _) = True
Z < Z = False
(S n) < (S m) = n < m
(S n) < Z = False

_>_ : ℕ → ℕ → Bool
m > n = n < m

-- The sorting algorithm
-- The trick here is that we are reducing qsort on "n"
qsort' : ∀ (n : ℕ) → ∀ (l : List ℕ) → (p : (length l) ≤ n) → (List ℕ)
qsort' Z [] p = []
qsort' Z (x ∷ l) ()
qsort' (S n) [] p = []
qsort' (S n) (x ∷ l) p =
                       let
                         ll = (filter (leq-nat x) l)
                         rr = (filter ((_>_) x) l)
                         pl = elim2-exists ll
                         pr = elim2-exists rr
                         left = qsort' n (elim1-exists ll) (≤-trans (length (elim1-exists ll)) (length l) n pl p)
                         right = qsort' n (elim1-exists rr) (≤-trans (length (elim1-exists rr)) (length l) n pr p)
                       in
                       (left ++ (x ∷ [])) ++ right

l' : {A : Set} → (l : List A) → (length l ≤ length l)
l' [] = ⋆
l' (x ∷ l) = l' l

qsort : ∀ (l : List ℕ) → List ℕ
qsort l = qsort' (length l) l (l' l)

-- XXX: definition of an sorted list
all-sorted-list : {A : Set} → (a : A)
                   → (l : List A)
                   → Prop
all-sorted-list a [] = ⊤
all-sorted-list a (x ∷ l) = leq a x ∧ (all-sorted-list a l)

sorted-list : {A : Set} → List A → Prop
sorted-list [] = ⊤
sorted-list (x ∷ l) = (all-sorted-list x l) ∧ (sorted-list l)

lem-qsort' : (x₁ : ℕ) → (l : List ℕ) → sorted-list
      ((qsort' (S (length l)) (filter' (leq-nat x₁) l)
        (≤-trans (length (filter' (leq-nat x₁) l)) (S (length l))
         (S (length l)) (thm-filter' l (leq-nat x₁)) (l' l))
        ++ (x₁ ∷ []))
       ++
       qsort' (S (length l)) (filter' (_>_ x₁) l)
       (≤-trans (length (filter' (_>_ x₁) l)) (S (length l))
        (S (length l)) (thm-filter' l (_>_ x₁)) (l' l)))
lem-qsort' x [] = and ⋆ ⋆
lem-qsort' x (x₁ ∷ l) = {!!}

lem-qsort : (l : List ℕ) → (x : ℕ) →
  sorted-list
      ((qsort' (length l) (elim1-exists (filter (leq-nat x) l))
        (≤-trans (length (elim1-exists (filter (leq-nat x) l))) (length l)
         (length l) (elim2-exists (filter (leq-nat x) l)) (l' l))
        ++ (x ∷ []))
       ++
       qsort' (length l) (elim1-exists (filter (_>_ x) l))
       (≤-trans (length (elim1-exists (filter (_>_ x) l))) (length l)
        (length l) (elim2-exists (filter (_>_ x) l)) (l' l)))
lem-qsort [] x = and ⋆ ⋆
lem-qsort (x ∷ l) x₁ = lem-qsort' x₁ l

-- Theorem that given a list, qsort will actually sort the list
thm-qsort : ∀ (l : List ℕ) → sorted-list (qsort l)
thm-qsort [] = ⋆
thm-qsort (x ∷ l) = lem-qsort l x


text:
-- Andreas, 2021-07-25, issue #5478 reported by mrohman

{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --double-check #-}

-- {-# OPTIONS -v impossible:70 #-}
-- {-# OPTIONS -v tc:20 #-}
-- {-# OPTIONS -v tc.interaction:30 #-}
-- {-# OPTIONS -v tc.meta:25 #-}
-- {-# OPTIONS -v tc.rec:20 #-}
-- {-# OPTIONS -v tc.cc:25 #-}
-- {-# OPTIONS -v tc.record.eta.contract:20 #-}

record ⊤ : Set where

record R (A : Set) : Set₁ where
  foo : ⊤
  foo = {!!} -- works with _ instead of ?
  field
    X : Set

-- 2021-07-28, issue #5463, reported by laMudri

open import Agda.Primitive

record Foo (o : Level) : Set (lsuc o) where

  field
    Obj : Set o
    Hom : Set o

  Sub : Set {!!}
  Sub = Hom

  field
    id : Set o

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Scenario:
--  * start with B only
--  * write 'f B = B'
--  * add constructor A
--  * want to deal with it first to preserve alphabetical ordering of clauses
--  * add 'f t = ?' *above* 'f B = B'

-- WAS: split t, get A and B
-- WANT: split t, get A only

data Type : Set where
  A B : Type

f : Type → Type
f t = {!!}
f B = B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT
open import cohomology.Theory
open import groups.ExactSequence
open import groups.HomSequence
open import homotopy.CofiberSequence

module cohomology.LongExactSequence {i} (CT : CohomologyTheory i)
  {X Y : Ptd i} (n : ℤ) (f : X ⊙→ Y) where

open CohomologyTheory CT
open import cohomology.PtdMapSequence CT

co∂ : C n X →ᴳ C (succ n) (⊙Cofiber f)
co∂ = record {f = CEl-fmap (succ n) ⊙extract-glue ∘ GroupIso.g (C-Susp n X); pres-comp = lemma} where
  abstract lemma = ∘ᴳ-pres-comp (C-fmap (succ n) ⊙extract-glue) (GroupIso.g-hom (C-Susp n X))

⊙∂-before-Susp : ⊙Cofiber f ⊙→ ⊙Susp X
⊙∂-before-Susp = ⊙extract-glue

∂-before-Susp : Cofiber (fst f) → Susp (de⊙ X)
∂-before-Susp = extract-glue

abstract
  ∂-before-Susp-glue-β : ∀ x →
    ap ∂-before-Susp (cfglue x) == merid x
  ∂-before-Susp-glue-β = ExtractGlue.glue-β

C-cofiber-seq : HomSequence (C n Y) (C (succ n) X)
C-cofiber-seq =
  C n Y                   →⟨ C-fmap n f                  ⟩ᴳ
  C n X                   →⟨ co∂                         ⟩ᴳ
  C (succ n) (⊙Cofiber f) →⟨ C-fmap (succ n) (⊙cfcod' f) ⟩ᴳ
  C (succ n) Y            →⟨ C-fmap (succ n) f           ⟩ᴳ
  C (succ n) X            ⊣|ᴳ

private
  C-iterated-cofiber-seq = C-seq (succ n) (iterated-cofiber-seq f)

  C-iterated-cofiber-seq-is-exact : is-exact-seq C-iterated-cofiber-seq
  C-iterated-cofiber-seq-is-exact =
    C-exact (succ n) (⊙cfcod²' f) , C-exact (succ n) (⊙cfcod' f) , C-exact (succ n) f , lift tt

  -- An intermediate sequence for proving exactness of [C-cofiber-seq].
  C-cofiber-seq' = C-seq (succ n) (cyclic-cofiber-seq f)

  C-cofiber-seq'-is-exact : is-exact-seq C-cofiber-seq'
  C-cofiber-seq'-is-exact =
    seq-equiv-preserves'-exact
      (C-seq-emap (succ n) (iterated-equiv-cyclic f))
      C-iterated-cofiber-seq-is-exact

  -- Now the final sequence
  C-cofiber-seq'-to-C-cofiber-seq :
    HomSeqMap C-cofiber-seq' C-cofiber-seq
      (GroupIso.f-hom (C-Susp n Y)) (idhom _)
  C-cofiber-seq'-to-C-cofiber-seq =
    GroupIso.f-hom (C-Susp n Y) ↓⟨ C-Susp-fmap n f ⟩ᴳ
    GroupIso.f-hom (C-Susp n X) ↓⟨ comm-sqrᴳ (λ x → ap (CEl-fmap (succ n) ⊙extract-glue) (! $ GroupIso.g-f (C-Susp n X) x)) ⟩ᴳ
    idhom _                     ↓⟨ comm-sqrᴳ (λ _ → idp) ⟩ᴳ
    idhom _                     ↓⟨ comm-sqrᴳ (λ _ → idp) ⟩ᴳ
    idhom _                     ↓|ᴳ

  C-cofiber-seq'-equiv-C-cofiber-seq :
    HomSeqEquiv C-cofiber-seq' C-cofiber-seq
      (GroupIso.f-hom (C-Susp n Y)) (idhom _)
  C-cofiber-seq'-equiv-C-cofiber-seq =
    C-cofiber-seq'-to-C-cofiber-seq ,
    (GroupIso.f-is-equiv (C-Susp n Y) , GroupIso.f-is-equiv (C-Susp n X) , idf-is-equiv _ , idf-is-equiv _ , idf-is-equiv _)

abstract
  C-cofiber-seq-is-exact : is-exact-seq C-cofiber-seq
  C-cofiber-seq-is-exact = seq-equiv-preserves-exact
    C-cofiber-seq'-equiv-C-cofiber-seq C-cofiber-seq'-is-exact

C-cofiber-exact-seq : ExactSequence (C n Y) (C (succ n) X)
C-cofiber-exact-seq = C-cofiber-seq , C-cofiber-seq-is-exact

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Cubical.Path
open import Agda.Primitive
open import Agda.Primitive.Cubical

private
  variable
    a p : Level
    A   : Set a
    P   : A → Set p
    x y : A

refl : x ≡ x
refl {x = x} = λ _ → x

subst : (P : A → Set p) → x ≡ y → P x → P y
subst P eq p = primTransp (λ i → P (eq i)) i0 p

record Erased (@0 A : Set a) : Set a where
  constructor [_]
  field
    @0 erased : A

[]-cong : {@0 A : Set a} {@0 x y : A} → @0 x ≡ y → [ x ] ≡ [ y ]
[]-cong eq = λ i → [ eq i ]

data Box : @0 Set → Set₁ where
  [_] : ∀ {A} → A → Box A

unbox : ∀ {@0 A} → Box A → A
unbox [ x ] = x

postulate
  @0 not : Bool ≡ Bool

should-be-true : Bool
should-be-true =
  unbox (subst (λ ([ A ]) → Box A) ([]-cong refl) [ true ])

should-be-false : Bool
should-be-false =
  unbox (subst (λ ([ A ]) → Box A) ([]-cong not) [ true ])


text:
module Issue3879.Fin where

open import Agda.Builtin.Nat

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

pattern 0F = zero


text:
module UnifyTerm where

open import Data.Fin using (Fin; suc; zero)
open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)

data Term (n : ℕ) : Set where
  i : (x : Fin n) -> Term n
  leaf : Term n
  _fork_ : (s t : Term n) -> Term n

_~>_ : (m n : ℕ) -> Set
m ~> n = Fin m -> Term n

▹ : ∀ {m n} -> (r : Fin m -> Fin n) -> Fin m -> Term n
▹ r = i ∘ r

_◃_ : ∀ {m n} -> (f : m ~> n) -> Term m -> Term n
f ◃ i x = f x
f ◃ leaf = leaf
f ◃ (s fork t) = (f ◃ s) fork (f ◃ t)

_≐_ : {m n : ℕ} -> (Fin m -> Term n) -> (Fin m -> Term n) -> Set
f ≐ g = ∀ x -> f x ≡ g x

◃ext : ∀ {m n} {f g : Fin m -> Term n} -> f ≐ g -> ∀ t -> f ◃ t ≡ g ◃ t
◃ext p (i x) = p x
◃ext p leaf = refl
◃ext p (s fork t) = cong₂ _fork_ (◃ext p s) (◃ext p t)

_◇_ : ∀ {l m n : ℕ } -> (f : Fin m -> Term n) (g : Fin l -> Term m) -> Fin l -> Term n
f ◇ g = (f ◃_) ∘ g

≐-cong : ∀ {m n o} {f : m ~> n} {g} (h : _ ~> o) -> f ≐ g -> (h ◇ f) ≐ (h ◇ g)
≐-cong h f≐g t = cong (h ◃_) (f≐g t)

≐-sym : ∀ {m n} {f : m ~> n} {g} -> f ≐ g -> g ≐ f
≐-sym f≐g = sym ∘ f≐g

module Sub where
  fact1 : ∀ {n} -> (t : Term n) -> i ◃ t ≡ t
  fact1 (i x) = refl
  fact1 leaf = refl
  fact1 (s fork t) = cong₂ _fork_ (fact1 s) (fact1 t)

  fact2 : ∀ {l m n} -> (f : Fin m -> Term n) (g : _) (t : Term l)
    -> (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
  fact2 f g (i x) = refl
  fact2 f g leaf = refl
  fact2 f g (s fork t) = cong₂ _fork_ (fact2 f g s) (fact2 f g t)

  fact3 : ∀ {l m n} (f : Fin m -> Term n) (r : Fin l -> Fin m) -> (f ◇ (▹ r)) ≡ (f ∘ r)
  fact3 f r = refl -- ext (λ _ -> refl)

◃ext' : ∀ {m n o} {f : Fin m -> Term n}{g : Fin m -> Term o}{h} -> f ≐ (h ◇ g) -> ∀ t -> f ◃ t ≡ h ◃ (g ◃ t)
◃ext' p t = trans (◃ext p t) (Sub.fact2 _ _ t)
s : ℕ -> ℕ
s = suc

thin : ∀ {n} -> (x : Fin (s n)) (y : Fin n) -> Fin (s n)
thin zero y = suc y
thin (suc x) zero = zero
thin (suc x) (suc y) = suc (thin x y)

p : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
p (suc x) = x
p zero = zero

module Thin where
  fact1 : ∀ {n} x y z -> thin {n} x y ≡ thin x z -> y ≡ z
  fact1 zero y .y refl = refl
  fact1 (suc x) zero zero r = refl
  fact1 (suc x) zero (suc z) ()
  fact1 (suc x) (suc y) zero ()
  fact1 (suc x) (suc y) (suc z) r = cong suc (fact1 x y z (cong p r))

  fact2 : ∀ {n} x y -> ¬ thin {n} x y ≡ x
  fact2 zero y ()
  fact2 (suc x) zero ()
  fact2 (suc x) (suc y) r = fact2 x y (cong p r)

  fact3 : ∀{n} x y -> ¬ x ≡ y -> ∃ λ y' -> thin {n} x y' ≡ y
  fact3 zero zero ne = ⊥-elim (ne refl)
  fact3 zero (suc y) _ = y , refl
  fact3 {zero} (suc ()) _ _
  fact3 {suc n} (suc x) zero ne = zero , refl
  fact3 {suc n} (suc x) (suc y) ne with y | fact3 x y (ne ∘ cong suc)
  ... | .(thin x y') | y' , refl = suc y' , refl

open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})

thick : ∀ {n} -> (x y : Fin (suc n)) -> Maybe (Fin n)
thick zero zero = nothing
thick zero (suc y) = just y
thick {zero} (suc ()) _
thick {suc _} (suc x) zero = just zero
thick {suc _} (suc x) (suc y) = suc <$> (thick x y)

open import Data.Sum

_≡Fin_ : ∀ {n} -> (x y : Fin n) -> Dec (x ≡ y)
zero ≡Fin zero = yes refl
zero ≡Fin suc y = no λ ()
suc x ≡Fin zero = no λ ()
suc {suc _} x ≡Fin suc y with x ≡Fin y
...              | yes r = yes (cong suc r)
...              | no r = no λ e -> r (cong p e)
suc {zero} () ≡Fin _

module Thick where
  half1 : ∀ {n} (x : Fin (suc n)) -> thick x x ≡ nothing
  half1 zero = refl
  half1 {suc _} (suc x) = cong (_<$>_ suc) (half1 x)
  half1 {zero} (suc ())

  half2 : ∀ {n} (x : Fin (suc n)) y -> ∀ y' -> thin x y' ≡ y -> thick x y ≡ just y'
  half2 zero zero y' ()
  half2 zero (suc y) .y refl = refl
  half2 {suc n} (suc x) zero zero refl = refl
  half2 {suc _} (suc _) zero (suc _) ()
  half2 {suc n} (suc x) (suc y) zero ()
  half2 {suc n} (suc x) (suc .(thin x y')) (suc y') refl with thick x (thin x y') | half2 x (thin x y') y' refl
  ...                                                       | .(just y')          | refl = refl
  half2 {zero} (suc ()) _ _ _

  fact1 : ∀ {n} (x : Fin (suc n)) y r
    -> thick x y ≡ r
    -> x ≡ y × r ≡ nothing ⊎ ∃ λ y' -> thin x y' ≡ y × r ≡ just y'
  fact1 x y .(thick x y) refl with x ≡Fin y
  fact1 x .x ._ refl | yes refl = inj₁ (refl , half1 x)
  ... | no el with Thin.fact3 x y el
  ...            | y' , thinxy'=y = inj₂ (y' , ( thinxy'=y , half2 x y y' thinxy'=y ))

check : ∀{n} (x : Fin (suc n)) (t : Term (suc n)) -> Maybe (Term n)
check x (i y) = i <$> thick x y
check x leaf = just leaf
check x (s fork t) = _fork_ <$> check x s ⊛ check x t

_for_ : ∀ {n} (t' : Term n) (x : Fin (suc n)) -> Fin (suc n) -> Term n
(t' for x) y = maybe′ i t' (thick x y)

data AList : ℕ -> ℕ -> Set where
  anil : ∀ {n} -> AList n n
  _asnoc_/_ : ∀ {m n} (σ : AList m n) (t' : Term m) (x : Fin (suc m))
               -> AList (suc m) n

sub : ∀ {m n} (σ : AList m n) -> Fin m -> Term n
sub anil = i
sub (σ asnoc t' / x) = sub σ ◇ (t' for x)

_++_ : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> AList l n
ρ ++ anil = ρ
ρ ++ (σ asnoc t' / x) = (ρ ++ σ) asnoc t' / x

++-assoc : ∀ {l m n o} (ρ : AList l m) (σ : AList n _) (τ : AList o _) -> ρ ++ (σ ++ τ) ≡ (ρ ++ σ) ++ τ
++-assoc ρ σ anil = refl
++-assoc ρ σ (τ asnoc t / x) = cong (λ s -> s asnoc t / x) (++-assoc ρ σ τ)

module SubList where
  anil-id-l : ∀ {m n} (σ : AList m n) -> anil ++ σ ≡ σ
  anil-id-l anil = refl
  anil-id-l (σ asnoc t' / x) = cong (λ σ -> σ asnoc t' / x) (anil-id-l σ)

  fact1 : ∀ {l m n} (ρ : AList m n) (σ : AList l m) -> sub (ρ ++ σ) ≐ (sub ρ ◇ sub σ)
  fact1 ρ anil v = refl
  fact1 {suc l} {m} {n} r (s asnoc t' / x) v = trans hyp-on-terms ◃-assoc
    where
      t = (t' for x) v
      hyp-on-terms = ◃ext (fact1 r s) t
      ◃-assoc = Sub.fact2 (sub r) (sub s) t

_∃asnoc_/_ : ∀ {m} (a : ∃ (AList m)) (t' : Term m) (x : Fin (suc m))
  -> ∃ (AList (suc m))
(n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

flexFlex : ∀ {m} (x y : Fin m) -> ∃ (AList m)
flexFlex {suc m} x y with thick x y
...              | just y' = m , anil asnoc i y' / x
...              | nothing = suc m , anil
flexFlex {zero} () _

flexRigid : ∀ {m} (x : Fin m) (t : Term m) -> Maybe (∃(AList m))
flexRigid {suc m} x t with check x t
...                   | just t' = just (m , anil asnoc t' / x)
...                   | nothing = nothing
flexRigid {zero} () _


text:
open import Function.Equivalence as FE using ()
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Decidable using (False; map)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; sym; cong; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)
open ≡-Reasoning

open import Data.Product using (_×_; _,_; uncurry)

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)

module AKS.Rational.Base where

open import Data.Integer using (ℤ; +_; +0; +[1+_]; -[1+_]; ∣_∣) renaming (_+_ to _+ℤ_; _*_ to _*ℤ_; -_ to -ℤ_; _≟_ to _≟ℤ_)
open import Data.Integer.DivMod using () renaming (_divℕ_ to _/ℤ_)
open import Data.Integer.Properties using (∣-n∣≡∣n∣)
open import AKS.Nat using (ℕ; suc; ≢⇒¬≟; ¬≟⇒≢) renaming (_+_ to _+ℕ_; _*_ to _*ℕ_; _≟_ to _≟ℕ_)
open import AKS.Nat using (n≢0∧m≢0⇒n*m≢0)
open import AKS.Nat.Divisibility using () renaming (_/_ to _/ℕ_)
open import AKS.Nat.GCD using (gcd; _⊥_; gcd[a,1]≡1; b≢0⇒gcd[a,b]≢0; gcd[0,a]≡1⇒a≡1; ⊥-respˡ; ⊥-sym)

record ℚ : Set where
  constructor ℚ✓
  field
    numerator : ℤ
    denominator : ℕ
    den≢0 : False (denominator ≟ℕ 0)
    coprime : ∣ numerator ∣ ⊥ denominator

fromℤ : ℤ → ℚ
fromℤ n = record
  { numerator = n
  ; denominator = 1
  ; den≢0 = tt
  ; coprime = gcd[a,1]≡1 (∣ n ∣)
  }

fromℕ : ℕ → ℚ
fromℕ n = fromℤ (+ n)

instance
  ℚ-number : Number ℚ
  ℚ-number = record
    { Constraint = λ _ → ⊤
    ; fromNat = λ n → fromℕ n
    }

open import AKS.Unsafe using (trustMe; TODO)

open import Data.Fin using (Fin)
open import Data.Nat.DivMod using (_divMod_; result)

∣a/ℤb∣≡∣a∣/ℕb : ∀ a b {b≢0} → ∣ (a /ℤ b) {b≢0} ∣ ≡ (∣ a ∣ /ℕ b) {b≢0}
∣a/ℤb∣≡∣a∣/ℕb (+ n) b {b≢0} = refl
∣a/ℤb∣≡∣a∣/ℕb (-[1+ x ]) b {b≢0} with (suc x divMod b) {b≢0}
... | result q Fin.zero eq rewrite ∣-n∣≡∣n∣ (+ q) = trustMe
... | result q (Fin.suc r) eq = trustMe

a/d⊥b/d : ∀ a b d {d≢0} → gcd a b ≡ d → (a /ℕ d) {d≢0} ⊥ (b /ℕ d) {d≢0}
a/d⊥b/d a b d gcd[a,b]≡d = begin
  gcd (a /ℕ d) (b /ℕ d) ≡⟨ trustMe ⟩
  1 ∎

a≢0⇒a/b≢0 : ∀ a b (a≢0 : False (a ≟ℕ 0)) {b≢0} → (a /ℕ b) {b≢0} ≢ 0
a≢0⇒a/b≢0 (suc a) (suc b) a≢0 = TODO

canonical : ∀ (num : ℤ) (den : ℕ) {den≢0 : False (den ≟ℕ 0)} → ℚ
canonical num den {den≢0} = construct num den {den≢0} (gcd ∣ num ∣ den) {≢⇒¬≟ (b≢0⇒gcd[a,b]≢0 (∣ num ∣) den (¬≟⇒≢ den≢0))} refl
  where
  construct : ∀ num den {den≢0 : False (den ≟ℕ 0)} d {d≢0 : False (d ≟ℕ 0)} → gcd ∣ num ∣ den ≡ d → ℚ
  construct num den {den≢0} d {d≢0} gcd[num,den]≡d = record
    { numerator = (num /ℤ d) {d≢0}
    ; denominator = (den /ℕ d) {d≢0}
    ; den≢0 = ≢⇒¬≟ (a≢0⇒a/b≢0 den d den≢0)
    ; coprime = ⊥-respˡ {den /ℕ d} (sym (∣a/ℤb∣≡∣a∣/ℕb num d)) (a/d⊥b/d ∣ num ∣ den d gcd[num,den]≡d)
    }

infixl 6 _+_
_+_ : ℚ → ℚ → ℚ
(ℚ✓ num₁ den₁ den₁≢0 _) + (ℚ✓ num₂ den₂ den₂≢0 _) = canonical (num₁ *ℤ (+ den₂) +ℤ num₂ *ℤ (+ den₁)) (den₁ *ℕ den₂) {≢⇒¬≟ (n≢0∧m≢0⇒n*m≢0 (¬≟⇒≢ den₁≢0) (¬≟⇒≢ den₂≢0))}

infix  8 -_
-_ : ℚ → ℚ
- (ℚ✓ num den den≢0 num⊥den) = ℚ✓ (-ℤ num) den den≢0 (⊥-respˡ {den} (sym (∣-n∣≡∣n∣ num)) num⊥den)

infixl 7 _*_
_*_ : ℚ → ℚ → ℚ
(ℚ✓ num₁ den₁ den₁≢0 _) * (ℚ✓ num₂ den₂ den₂≢0 _) = canonical (num₁ *ℤ num₂) (den₁ *ℕ den₂) {≢⇒¬≟ (n≢0∧m≢0⇒n*m≢0 (¬≟⇒≢ den₁≢0) (¬≟⇒≢ den₂≢0))}

infix 8 _⁻¹
_⁻¹ : ∀ (q : ℚ) {q≢0 : q ≢ 0} → ℚ
(ℚ✓ +0 den den≢0 num⊥den ⁻¹) {q≢0} with gcd[0,a]≡1⇒a≡1 den num⊥den
(ℚ✓ +0 .1 tt refl ⁻¹) {q≢0} | refl = contradiction refl q≢0
(ℚ✓ +[1+ num ] (suc den) den≢0 num⊥den) ⁻¹ = ℚ✓ +[1+ den ] (suc num) tt (⊥-sym {suc num} {suc den} num⊥den)
(ℚ✓ -[1+ num ] (suc den) den≢0 num⊥den) ⁻¹ = ℚ✓ -[1+ den ] (suc num) tt (⊥-sym {suc num} {suc den} num⊥den)

infixl 7 _/_
_/_ : ∀ (p q : ℚ) {q≢0 : q ≢ 0} → ℚ
_/_ p q {q≢0}= p * (q ⁻¹) {q≢0}

_≟_ : Decidable {A = ℚ} _≡_
(ℚ✓ num₁ (suc den₁) tt num₁⊥den₁) ≟ (ℚ✓ num₂ (suc den₂) tt num₂⊥den₂)
  = map (FE.equivalence forward backward) (num₁ ≟ℤ num₂ ×-dec den₁ ≟ℕ den₂)
  where
  forward : ∀ {num₁ num₂} {den₁ den₂} {num₁⊥den₁ num₂⊥den₂} → num₁ ≡ num₂ × den₁ ≡ den₂ → ℚ✓ num₁ (suc den₁) tt num₁⊥den₁ ≡ ℚ✓ num₂ (suc den₂) tt num₂⊥den₂
  forward {num₁} {num₂} {den₁} {den₂} {num₁⊥den₁} {num₂⊥den₂} (refl , refl) = cong (λ pf → ℚ✓ num₁ (suc den₁) tt pf) (≡-irrelevant num₁⊥den₁ num₂⊥den₂)
  backward : ∀ {num₁ num₂} {den₁ den₂} {num₁⊥den₁ num₂⊥den₂} → ℚ✓ num₁ (suc den₁) tt num₁⊥den₁ ≡ ℚ✓ num₂ (suc den₂) tt num₂⊥den₂ → num₁ ≡ num₂ × den₁ ≡ den₂
  backward refl = (refl , refl)

≢0 : ∀ {p : ℚ} {p≢0 : False (p ≟ 0)} → p ≢ 0
≢0 {p} with p ≟ 0
≢0 {p} | no p≢0 = p≢0

test = ((1 / 2) {≢0} + (3 / 4) {≢0}) ⁻¹

open import Data.String using (String; _++_)
open import Data.Nat.Show using () renaming (show to show-ℕ)

show-ℤ : ℤ → String
show-ℤ (+ n) = show-ℕ n
show-ℤ (-[1+ n ]) = "-" ++ show-ℕ (suc n)

show-ℚ : ℚ → String
show-ℚ (ℚ✓ num 1 _ _) = show-ℤ num
show-ℚ (ℚ✓ num den _ _) = show-ℤ num ++ "/" ++ show-ℕ den

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

-- Scope checker allowed definition in different module than signature

module _ where

module N where
  record R : Set where

open N hiding (module R)

module M where
  record R where  -- should be rejected since signature lives in different module

  inhabited-R : R
  inhabited-R = _

data ⊥ : Set where

record R where
  field absurd : ⊥

boom : ⊥
boom = R.absurd M.inhabited-R


text:
{-# OPTIONS --universe-polymorphism #-}

module NoPanic where

postulate
  Level : Set
  lzero : Level
  lsuc  : Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC  lsuc  #-}

module M {A : Set} where

  postulate
    I : A → ∀ a → Set a
    i : ∀ (x : A) {a} → I x a
    f : {B : Set} → B
    a : A

  Foo : Set₁
  Foo with i (f a)
  Foo | _ = Set

-- Old (bad) error message:

-- NoPanic.agda:24,3-16
-- Panic: Pattern match failure in do expression at
-- src/full/Agda/TypeChecking/Rules/Term.hs:646:7-18
-- when checking that the expression _22 {A} has type Level

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Ual.Ord where

open import Agda.Primitive
open import Ual.Void
open import Ual.Eq
open import Ual.Either
open import Ual.Both

record Ord {a} (A : Set a) : Set (lsuc a) where
  infix 30 _<_
  infix 30 _>_
  infix 30 _≤_
  infix 30 _≥_
  field
    ⦃ eqA ⦄     : Eq A
    _<_        : A → A → Set
  _>_ : A → A → Set
  x > y = x ≠ y ∧ ¬ (x < y)
  _≤_ : A → A → Set
  x ≤ y = x == y ∨ x < y
  _≥_ : A → A → Set
  x ≥ y = x == y ∨ x > y
  field
    ltNotEq : {x y : A} → x < y → x ≠ y
    symLt   : {x y : A} → x < y → y > x
    symGt   : {x y : A} → x > y → y < x
    transLt : {x y z : A} → x < y → y < z → x < z
    transLe : {x y z : A} → x ≤ y → y ≤ z → x ≤ z

  symLe : {x y : A} → x ≤ y → y ≥ x
  symLe (orL eq) = orL (sym ⦃ eqA ⦄ eq)
  symLe (orR lt) = orR (symLt lt)
  symGe : {x y : A} → x ≥ y → y ≤ x
  symGe (orL eq) = orL (sym ⦃ eqA ⦄ eq)
  symGe (orR gt) = orR (symGt gt)

  transGt : {x y z : A} → x > y → y > z → x > z
  transGt gt1 gt2 = symLt (transLt (symGt gt2) (symGt gt1))
  transGe : {x y z : A} → x ≥ y → y ≥ z → x ≥ z
  transGe ge1 ge2 = symLe (transLe (symGe ge2) (symGe ge1))

open Ord ⦃ ... ⦄ public

data Order {a} {A : Set a} ⦃ ordA : Ord A ⦄ : A → A → Set where
  less    : {x y : A} → x < y → Order x y
  equal   : {x y : A} → x == y → Order x y
  greater : {x y : A} → x > y → Order x y

record Compare {a} (A : Set a) : Set (lsuc a) where
  field
    ⦃ ordA ⦄ : Ord A
    compare  : (x : A) → (y : A) → Order x y

max_stars_repo_name: brunoczim/ual

max_issues_repo_name: brunoczim/ual

max_forks_repo_name: brunoczim/ual


text:
record R : Set₁ where
  field
    ⟨_+_⟩ : Set

open R

-- Name parts coming from projections can not be used as part of
-- variables.

F : Set → Set
F + = +


text:
------------------------------------------------------------------------
-- IO
------------------------------------------------------------------------

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

module IO-monad where

open import Monad.Raw
open import Prelude
open import String

------------------------------------------------------------------------
-- The IO type former

open import Agda.Builtin.IO public using (IO)

------------------------------------------------------------------------
-- The IO monad

postulate
  returnIO : ∀ {a} {A : Type a} → A → IO A
  bindIO   : ∀ {a b} {A : Type a} {B : Type b} →
             IO A → (A → IO B) → IO B

{-# COMPILE GHC returnIO = \_ _ -> return    #-}
{-# COMPILE GHC bindIO   = \_ _ _ _ -> (>>=) #-}

instance

  io-monad : ∀ {ℓ} → Raw-monad (IO {a = ℓ})
  Raw-monad.return io-monad = returnIO
  Raw-monad._>>=_  io-monad = bindIO

------------------------------------------------------------------------
-- Some IO primitives

-- Note that some commands may raise exceptions when executed.

postulate
  putStr      : String → IO ⊤
  putStrLn    : String → IO ⊤
  exitFailure : IO ⊤
  getArgs     : IO (List String)

{-# FOREIGN GHC
  import qualified Data.Text
  import qualified Data.Text.IO
  import qualified System.Environment
  import qualified System.Exit
#-}

-- Note that the GHC code below ignores potential problems. For
-- instance, putStr could raise an exception.

{-# COMPILE GHC putStr      = Data.Text.IO.putStr #-}
{-# COMPILE GHC putStrLn    = Data.Text.IO.putStrLn #-}
{-# COMPILE GHC exitFailure = System.Exit.exitFailure #-}
{-# COMPILE GHC getArgs     = fmap (map Data.Text.pack)
                                System.Environment.getArgs #-}

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

-- This issue demonstrates that a failing termination check,
-- subsequently blocking reductions, makes some `impossible'
-- cases possible in the conversion checker.

module Issue921 where

infix 3 _==_
postulate
  _==_ : {A : Set} → A → A → Set
  transport : {A : Set} (B : A → Set) {x y : A} (p : x == y) → (B x → B y)
  ! : {A : Set} {x y : A} → (x == y → y == x)

infixr 1 _,_
record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

infix 4 _≃_

_≃_ : ∀ (A : Set) (B : Set) → Set
A ≃ B = Σ (A → B) (λ _ → B → A)

postulate
  <– : {A : Set} {B : Set} → (A ≃ B) → B → A

infixr 4 _∘e_
_∘e_ : {A : Set} {B : Set} {C : Set} → B ≃ C → A ≃ B → A ≃ C
e1 ∘e e2 = ({!!} , λ c → snd e2 (snd e1 c))

module _ {A : Set} {B : A → Set} {C : (a : A) → B a → Set} where
  Σ-assoc : Σ (Σ A B) (λ z → C (fst z) (snd z)) ≃ Σ A (λ a → Σ (B a) (C a))
  Σ-assoc = ({!!} , λ {(a , (b , c)) → ((a , b) , c)})

data Ctx : Set

postulate
  Ty : Ctx → Set

data Ctx where
  _·_ : (Γ : Ctx) → Ty {!!} → Ctx

infix 5 _ctx-⇛_
_ctx-⇛_ : Ctx → Ctx → Set

-- swap these two lines and the internal error disappears
Tm : Σ Ctx Ty → Set
Γ ctx-⇛ (Δ · A) = Σ {!!} {!!}

infix 10 _*_

postulate
  _*_  : {Γ Δ : Ctx} (m : Γ ctx-⇛ Δ) → Ty {!!} → Ty {!!}

pullback : {Γ Δ : Ctx} {A : Ty Δ} → Tm (Δ , A) → (m : Γ ctx-⇛ Δ) → Tm (Γ , m * A)

infix 7 _·_
data Xtc (Γ : Ctx) : Set where
  _·_ : (A : Ty {!!}) → Xtc {!!} → Xtc Γ

infix 6 _⋯_
_⋯_ : (Γ : Ctx) → Xtc Γ → Ctx
Γ ⋯ (A · s) = (Γ · A) ⋯ s

module xtc where
  infix 5 _⇛_∣_
  _⇛_∣_ : (Γ : Ctx) {Δ : Ctx} (m : Γ ctx-⇛ Δ) → Xtc Δ → Set
  Γ ⇛ m ∣ A · T = Σ (Tm (Γ , m * A)) (λ t → Γ ⇛ (m , t) ∣ T)

  infix 5 _⇛_
  _⇛_ : (Γ : Ctx) → Σ Ctx (λ Δ → Xtc Δ) → Set
  Γ ⇛ (Δ , T) = Σ (Γ ctx-⇛ Δ) (λ m → Γ ⇛ m ∣ T)

  eq : {Γ Δ : Ctx} {T : Xtc Δ} → Γ ctx-⇛ Δ ⋯ T ≃ Γ ⇛ (Δ , T)
  eq {T = A · T} = Σ-assoc ∘e eq

weaken : (Γ : Ctx) {T : Xtc Γ} → Γ ⋯ T ctx-⇛ Γ

infix 10 _○_

_○_ : {Γ Δ Θ : Ctx} → Δ ctx-⇛ Θ → Γ ctx-⇛ Δ → Γ ctx-⇛ Θ

postulate
  _○=_ : {Γ Δ Θ : Ctx} (n : Δ ctx-⇛ Θ) (m : Γ ctx-⇛ {!!}) {A : Ty {!!}} → (n ○ m) * A == m * (n * A)

Tm P = Σ Ctx λ Γ → Σ (Ty {!!}) λ A → Σ (Xtc (Γ · A)) λ T → (Γ · A ⋯ T , weaken Γ {A · T} * A) == P

weaken (Γ · A) {T} = (weaken Γ {A · T} , (Γ , A , T , {!!}))

_○_ {Θ = Θ · _} (n , x) m = (n ○ m , transport (λ z → Tm (_ , z)) (! (n ○= m)) (pullback x m))

weaken-○-scope : {Γ Δ : Ctx} {T : Xtc Δ} (ms : Γ xtc.⇛ (Δ , T)) → weaken Δ {T} ○ snd xtc.eq ms == fst ms

pullback-var : {Γ Δ : Ctx} {A : Ty {!!}} {T : Xtc (Δ · A)}
               (ms : Γ xtc.⇛ (Δ , A · T))
             → Tm (Γ , snd xtc.eq ms * (weaken Δ {A · T} * A))
pullback-var {Γ} {Δ} {A} {T} ms =
  transport (λ z → Tm (Γ , z)) (weaken Δ {A · T} ○= snd xtc.eq ms)
    (transport (λ z → Tm (Γ , z * A)) (! (weaken-○-scope ms))
      (fst (snd ms)))

pullback (Δ' , _ , T , p) = transport (λ P → (m : _ ctx-⇛ fst P) → Tm (_ , m * snd P)) p (<– {!!} pullback-var)

weaken-○-scope {Γ} {Δ · A} {T} ((m , t) , ts) = {!!} where
  helper3 : transport (λ z → Tm (Γ , z))
                      (! (fst (weaken (Δ · A)) ○= snd xtc.eq ((m , t) , ts)))
                      (pullback-var {!!})
         == transport (λ z → Tm (Γ , z * A))
                      (! (weaken-○-scope (m , t , ts)))
                      t
  helper3 = {!!}


text:
open import Relation.Binary.Core

module InsertSort.Impl2.Correctness.Permutation.Base {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum
open import InsertSort.Impl2 _≤_ tot≤
open import List.Permutation.Base A
open import OList _≤_

lemma-forget-insert : {b : Bound} → (x : A) → (b≤x : LeB b (val x)) → (xs : OList b) → forget (insert b≤x xs) / x ⟶ forget xs
lemma-forget-insert x b≤x onil = /head
lemma-forget-insert x b≤x (:< {x = y} b≤y ys)
    with tot≤ x y
... | inj₁ x≤y = /head
... | inj₂ y≤x = /tail (lemma-forget-insert x (lexy y≤x) ys)

theorem-insertSort∼ : (xs : List A) → xs ∼ forget (insertSort xs)
theorem-insertSort∼ [] = ∼[]
theorem-insertSort∼ (x ∷ xs) = ∼x /head (lemma-forget-insert x lebx (insertSort xs)) (theorem-insertSort∼ xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue731 where

data empty : Set where

foo : empty → _
foo ()

bar : empty → Set
bar = foo

{- But when I want to know what are the constraints (C-c C-= in
emacs), I get the following error instead:

No binding for builtin thing LEVELZERO, use {-# BUILTIN LEVELZERO
name #-} to bind it to 'name'
when checking that the expression foo has type empty → Set

I’m not sure it is a bug, but it seems a bit strange to get an error
message when doing C-c C-= -}

-- Now displays correctly:
-- _4 := foo [blocked by problem 3]
-- [3] _2 =< Set : Set _1
-- _1 = (.Agda.Primitive.lsuc .Agda.Primitive.lzero)
-- _1 = (.Agda.Primitive.lsuc .Agda.Primitive.lzero)


text:
record R : Set₁ where
  field
    A : Set

open R ⦃ … ⦄

-- The inferred type of A is ⦃ r : R ⦄ → Set. However, the following
-- code is rejected:

X : R → Set
X r = A ⦃ r = r ⦄

-- WAS: Function does not accept argument ⦃ r = r ⦄
-- when checking that ⦃ r = r ⦄ is a valid argument to a function of
-- type ⦃ r = r₁ : R ⦄ → Set

-- SHOULD: succeed


text:
-- 2017-11-01, issue #2668 reported by brprice
--
--     This seems to have been fixed in 2.5.3 (specifically, commit
--     8518b8e seems to have solved this, along with #2727 and #2726)

-- {-# OPTIONS -v tc.mod.apply:20 #-}
-- {-# OPTIONS -v tc.proj.like:40 #-}
-- {-# OPTIONS -v tc.signature:60 #-}

-- {-# OPTIONS -v tc.with:60 #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

module _ (Q : Set) where -- parameter needed to trigger issue

-- has to pattern match: `badRefl _ = refl` typechecks
badRefl : (n : Nat) → n ≡ n
badRefl zero = refl
badRefl (suc n) = refl

-- has to wrap: `Wrap = Nat` (and changing uses of wrap) typechecks

data Wrap : Set where
  wrap  : (n : Nat) → Wrap

record Rec (A : Set) : Set where
  field
    recW : (m : Nat) → Wrap

  foo : A → Wrap → Wrap
  foo _ (wrap i) = recW i

Thin : Rec Nat
Thin = record { recW = wrap }

module Th = Rec Thin

test : ∀ (th : Nat)(t : Wrap)
   → Th.foo th t ≡ Th.foo th t

  -- If we don't go via Th, it typechecks
  --   → Rec.foo Thin th t ≡ Rec.foo Thin th t

-- test = {!Rec.foo!}
test th t with badRefl th
... | p = refl

-- ERROR WAS:
-- Expected a hidden argument, but found a visible argument
-- when checking that the type
--   (Q : Set) (th : Nat) → th ≡ th → (t : Wrap) →
--     Rec.foo (record { recW = wrap }) th t ≡
--     Rec.foo (record { recW = wrap }) th t
-- of the generated with function is well-formed

-- Should succeed


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

open import HoTT
open import cohomology.Theory
open import groups.Exactness
open import groups.HomSequence
open import groups.ExactSequence

open import cw.CW

module cw.cohomology.Descending {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cw.cohomology.TipAndAugment OT
open import cw.cohomology.WedgeOfCells OT
open import cohomology.LongExactSequence cohomology-theory

private
  C-cw-descend-at-succ : ∀ {n} (⊙skel : ⊙Skeleton (S n))
      {m} (m≠n : m ≠ ℕ-to-ℤ n) (Sm≠n : succ m ≠ ℕ-to-ℤ n)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → C (succ m) ⊙⟦ ⊙skel ⟧ ≃ᴳ C (succ m) ⊙⟦ ⊙cw-init ⊙skel ⟧
  C-cw-descend-at-succ ⊙skel {m} m≠n Sm≠n ac =
    Exact2.G-trivial-and-L-trivial-implies-H-iso-K
      (exact-seq-index 2 $ C-cofiber-exact-seq m (⊙cw-incl-last ⊙skel))
      (exact-seq-index 0 $ C-cofiber-exact-seq (succ m) (⊙cw-incl-last ⊙skel))
      (CXₙ/Xₙ₋₁-≠-is-trivial ⊙skel (succ-≠ m≠n) ac)
      (CXₙ/Xₙ₋₁-≠-is-trivial ⊙skel (succ-≠ Sm≠n) ac)

C-cw-descend : ∀ {n} (⊙skel : ⊙Skeleton (S n))
    {m} (m≠n : m ≠ ℕ-to-ℤ n) (m≠Sn : m ≠ ℕ-to-ℤ (S n))
  → ⊙has-cells-with-choice 0 ⊙skel i
  → C m ⊙⟦ ⊙skel ⟧ ≃ᴳ C m ⊙⟦ ⊙cw-init ⊙skel ⟧
C-cw-descend ⊙skel {m = negsucc m} -Sm≠n -Sm≠Sn
  = C-cw-descend-at-succ ⊙skel (pred-≠ -Sm≠Sn) -Sm≠n
C-cw-descend ⊙skel {m = pos O} O≠n O≠Sn
  = C-cw-descend-at-succ ⊙skel (pred-≠ O≠Sn) O≠n
C-cw-descend ⊙skel {m = pos (S n)} Sm≠n Sm≠Sn
  = C-cw-descend-at-succ ⊙skel (pred-≠ Sm≠Sn) Sm≠n

abstract
  C-cw-at-higher : ∀ {n} (⊙skel : ⊙Skeleton n) {m} (n<m : n < m)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (C (ℕ-to-ℤ m) ⊙⟦ ⊙skel ⟧)
  C-cw-at-higher {n = O} ⊙skel 0<n ac =
    CX₀-≠-is-trivial ⊙skel (ℕ-to-ℤ-≠ (≠-inv (<-to-≠ 0<n))) ac
  C-cw-at-higher {n = S n} ⊙skel Sn<m ac =
    iso-preserves'-trivial
      (C-cw-descend ⊙skel
        (ℕ-to-ℤ-≠ (≠-inv (<-to-≠ (<-trans ltS Sn<m))))
        (ℕ-to-ℤ-≠ (≠-inv (<-to-≠ Sn<m)))
        ac)
      (C-cw-at-higher (⊙cw-init ⊙skel) (<-trans ltS Sn<m) (⊙init-has-cells-with-choice ⊙skel ac))

  C-cw-at-negsucc : ∀ {n} (⊙skel : ⊙Skeleton n) m
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (C (negsucc m) ⊙⟦ ⊙skel ⟧)
  C-cw-at-negsucc {n = O} ⊙skel m ac =
    CX₀-≠-is-trivial ⊙skel (ℤ-negsucc≠pos m O) ac
  C-cw-at-negsucc {n = S n} ⊙skel m ac =
    iso-preserves'-trivial
      (C-cw-descend ⊙skel
        (ℤ-negsucc≠pos _ n)
        (ℤ-negsucc≠pos _ (S n))
        ac)
      (C-cw-at-negsucc (⊙cw-init ⊙skel) m (⊙init-has-cells-with-choice ⊙skel ac))

C-cw-descend-at-lower : ∀ {n} (⊙skel : ⊙Skeleton (S n)) {m} (m<n : m < n)
  → ⊙has-cells-with-choice 0 ⊙skel i
  → C (ℕ-to-ℤ m) ⊙⟦ ⊙skel ⟧ ≃ᴳ C (ℕ-to-ℤ m) ⊙⟦ ⊙cw-init ⊙skel ⟧
C-cw-descend-at-lower ⊙skel m<n ac =
  C-cw-descend ⊙skel (ℕ-to-ℤ-≠ (<-to-≠ m<n)) (ℕ-to-ℤ-≠ (<-to-≠ (ltSR m<n))) ac

{-
favonia: it turns out easier (?) to do the descending step by step

C-cw-to-diag-at-lower : ∀ n {m} (Sn≤m : S n ≤ m) (⊙skel : ⊙Skeleton m)
  → ⊙has-cells-with-choice 0 ⊙skel i
  → C (ℕ-to-ℤ n) ⊙⟦ ⊙skel ⟧ ≃ᴳ C (ℕ-to-ℤ n) ⊙⟦ ⊙cw-take Sn≤m ⊙skel ⟧
C-cw-to-diag-at-lower _ (inl idp) _ _ = idiso _
C-cw-to-diag-at-lower n (inr ltS) ⊙skel ac =
  C-cw-descend (ℕ-to-ℤ n) (ℕ-to-ℤ-≠ (<-to-≠ ltS)) (ℕ-to-ℤ-≠ (<-to-≠ (ltSR ltS))) ⊙skel ac
C-cw-to-diag-at-lower n {S m} (inr (ltSR lt)) ⊙skel ac =
      C-cw-to-diag-at-lower n (inr lt) (⊙cw-init ⊙skel) (⊙init-has-cells-with-choice ⊙skel ac)
  ∘eᴳ C-cw-descend (ℕ-to-ℤ n) (ℕ-to-ℤ-≠ n≠m) (ℕ-to-ℤ-≠ n≠Sm) ⊙skel ac
  where
    n≠Sm : n ≠ S m
    n≠Sm = <-to-≠ (<-trans ltS (ltSR lt))

    n≠m : n ≠ m
    n≠m = <-to-≠ (<-trans ltS lt)
-}


text:
module Issue558 where

data Nat : Set where
  Z : Nat
  S : Nat → Nat

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

plus : Nat → Nat → Nat
plus Z n = n
plus (S n) m = S (plus n m)

record Addable (τ : Set) : Set where
 constructor addable
 field
  _+_ : τ → τ → τ

open module AddableIFS {t : Set} {{r : Addable t}} = Addable {t} r

record CommAddable (τ : Set) : Set where
 constructor commAddable
 field
  foo : Addable τ
  comm : (a b : τ) → (a + b) ≡ (b + a)

natAdd : Addable Nat
natAdd = record {_+_ = plus}

postulate commPlus : (a b : Nat) → plus a b ≡ plus b a

commAdd : CommAddable Nat
commAdd = record {foo = natAdd; comm = commPlus}

open CommAddable {{...}}

test : (Z + Z) ≡ Z
test = comm Z Z

a : {x y : Nat} → (S (S Z) + (x + y)) ≡ ((x + y) + S (S Z))
a {x}{y} = comm (S (S Z)) (x + y) -- ERROR!

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

data Nat : Set where
  zero : Nat
  suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)
{-# BUILTIN NATPLUS _+_ #-} -- Without this, the internal error disappears.

postulate
  _≡_ : Nat → Nat → Set
{-# BUILTIN REWRITE _≡_ #-}

postulate
  a b n : Nat
  Q : Nat → Set
  R : (m n : Nat) → Q (m + n) → Set
  +S : (n + a) ≡ b
{-# REWRITE +S #-}

variable
  m : Nat -- Explicitly quantifying over m, the internal error disappears.

postulate
  bug : (q : Q n) → R m n q

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.Base where

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.AbGroup

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' ℓ'' : Level

record IsRing {R : Type ℓ}
              (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isring

  field
    +IsAbGroup : IsAbGroup 0r _+_ -_
    ·IsMonoid  : IsMonoid 1r _·_
    ·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
    ·DistL+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
    -- This is in the Agda stdlib, but it's redundant
    -- zero             : (x : R) → (x · 0r ≡ 0r) × (0r · x ≡ 0r)

  open IsAbGroup +IsAbGroup public
    renaming
      ( isSemigroup  to +IsSemigroup
      ; isMonoid     to +IsMonoid
      ; isGroup      to +IsGroup )

  open IsMonoid ·IsMonoid public
    renaming
      ( isSemigroup to ·IsSemigroup )
    hiding
      ( is-set ) -- We only want to export one proof of this

unquoteDecl IsRingIsoΣ = declareRecordIsoΣ IsRingIsoΣ (quote IsRing)

record RingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where

  constructor ringstr

  field
    0r      : A
    1r      : A
    _+_     : A → A → A
    _·_     : A → A → A
    -_      : A → A
    isRing  : IsRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsRing isRing public

Ring : ∀ ℓ → Type (ℓ-suc ℓ)
Ring ℓ = TypeWithStr ℓ RingStr

isSetRing : (R : Ring ℓ) → isSet ⟨ R ⟩
isSetRing R = R .snd .RingStr.isRing .IsRing.·IsMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

module _ {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
               (is-setR : isSet R)
               (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
               (+IdR : (x : R) → x + 0r ≡ x)
               (+InvR : (x : R) → x + (- x) ≡ 0r)
               (+Comm : (x y : R) → x + y ≡ y + x)
               (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
               (·IdR : (x : R) → x · 1r ≡ x)
               (·IdL : (x : R) → 1r · x ≡ x)
               (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
               (·DistL+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
  where

  makeIsRing : IsRing 0r 1r _+_ _·_ -_
  makeIsRing .IsRing.+IsAbGroup = makeIsAbGroup is-setR +Assoc +IdR +InvR +Comm
  makeIsRing .IsRing.·IsMonoid = makeIsMonoid is-setR ·Assoc ·IdR ·IdL
  makeIsRing .IsRing.·DistR+ = ·DistR+
  makeIsRing .IsRing.·DistL+ = ·DistL+

module _ {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
               (is-setR : isSet R)
               (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
               (+IdR : (x : R) → x + 0r ≡ x)
               (+InvR : (x : R) → x + (- x) ≡ 0r)
               (+Comm : (x y : R) → x + y ≡ y + x)
               (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
               (·IdR : (x : R) → x · 1r ≡ x)
               (·IdL : (x : R) → 1r · x ≡ x)
               (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
               (·DistL+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
  where

  makeRing : Ring ℓ
  makeRing .fst = R
  makeRing .snd .RingStr.0r = 0r
  makeRing .snd .RingStr.1r = 1r
  makeRing .snd .RingStr._+_ = _+_
  makeRing .snd .RingStr._·_ = _·_
  makeRing .snd .RingStr.-_ = -_
  makeRing .snd .RingStr.isRing =
    makeIsRing is-setR +Assoc +IdR +InvR +Comm
                       ·Assoc ·IdR ·IdL ·DistR+ ·DistL+

record IsRingHom {A : Type ℓ} {B : Type ℓ'} (R : RingStr A) (f : A → B) (S : RingStr B)
  : Type (ℓ-max ℓ ℓ')
  where

  -- Shorter qualified names
  private
    module R = RingStr R
    module S = RingStr S

  field
    pres0 : f R.0r ≡ S.0r
    pres1 : f R.1r ≡ S.1r
    pres+ : (x y : A) → f (x R.+ y) ≡ f x S.+ f y
    pres· : (x y : A) → f (x R.· y) ≡ f x S.· f y
    pres- : (x : A) → f (R.- x) ≡ S.- (f x)

unquoteDecl IsRingHomIsoΣ = declareRecordIsoΣ IsRingHomIsoΣ (quote IsRingHom)

RingHom : (R : Ring ℓ) (S : Ring ℓ') → Type (ℓ-max ℓ ℓ')
RingHom R S = Σ[ f ∈ (⟨ R ⟩ → ⟨ S ⟩) ] IsRingHom (R .snd) f (S .snd)

IsRingEquiv : {A : Type ℓ} {B : Type ℓ'} (M : RingStr A) (e : A ≃ B) (N : RingStr B)
  → Type (ℓ-max ℓ ℓ')
IsRingEquiv M e N = IsRingHom M (e .fst) N

RingEquiv : (R : Ring ℓ) (S : Ring ℓ') → Type (ℓ-max ℓ ℓ')
RingEquiv R S = Σ[ e ∈ (⟨ R ⟩ ≃ ⟨ S ⟩) ] IsRingEquiv (R .snd) e (S .snd)

_$_ : {R : Ring ℓ} {S : Ring ℓ'} → (φ : RingHom R S) → (x : ⟨ R ⟩) → ⟨ S ⟩
φ $ x = φ .fst x

RingEquiv→RingHom : {A B : Ring ℓ} → RingEquiv A B → RingHom A B
RingEquiv→RingHom (e , eIsHom) = e .fst , eIsHom

RingHomIsEquiv→RingEquiv : {A B : Ring ℓ} (f : RingHom A B)
                         → isEquiv (fst f) → RingEquiv A B
fst (fst (RingHomIsEquiv→RingEquiv f fIsEquiv)) = fst f
snd (fst (RingHomIsEquiv→RingEquiv f fIsEquiv)) = fIsEquiv
snd (RingHomIsEquiv→RingEquiv f fIsEquiv) = snd f

isPropIsRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsRing 0r 1r _+_ _·_ -_)
isPropIsRing 0r 1r _+_ _·_ -_ =
  isOfHLevelRetractFromIso 1 IsRingIsoΣ
    (isPropΣ (isPropIsAbGroup 0r _+_ (-_)) λ abgrp →
     isProp× (isPropIsMonoid 1r _·_)
             (isProp× (isPropΠ3 λ _ _ _ → abgrp .is-set _ _)
                      (isPropΠ3 λ _ _ _ → abgrp .is-set _ _)))
  where
  open IsAbGroup

isPropIsRingHom : {A : Type ℓ} {B : Type ℓ'} (R : RingStr A) (f : A → B) (S : RingStr B)
  → isProp (IsRingHom R f S)
isPropIsRingHom R f S = isOfHLevelRetractFromIso 1 IsRingHomIsoΣ
                        (isProp×4 (isSetRing (_ , S) _ _)
                                  (isSetRing (_ , S) _ _)
                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
                                  (isPropΠ2 λ _ _ → isSetRing (_ , S) _ _)
                                  (isPropΠ λ _ → isSetRing (_ , S) _ _))

isSetRingHom : (R : Ring ℓ) (S : Ring ℓ') → isSet (RingHom R S)
isSetRingHom R S = isSetΣSndProp (isSetΠ (λ _ → isSetRing S)) (λ f → isPropIsRingHom (snd R) f (snd S))

isSetRingEquiv : (A : Ring ℓ) (B : Ring ℓ') → isSet (RingEquiv A B)
isSetRingEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 (isSetRing A) (isSetRing B))
                                   (λ e → isPropIsRingHom (snd A) (fst e) (snd B))

RingHomPathP : (R S T : Ring ℓ) (p : S ≡ T) (φ : RingHom R S) (ψ : RingHom R T)
             → PathP (λ i → R .fst → p i .fst) (φ .fst) (ψ .fst)
             → PathP (λ i → RingHom R (p i)) φ ψ
RingHomPathP R S T p φ ψ q = ΣPathP (q , isProp→PathP (λ _ → isPropIsRingHom _ _ _) _ _)

RingHom≡ : {R S : Ring ℓ} {φ ψ : RingHom R S} → fst φ ≡ fst ψ → φ ≡ ψ
RingHom≡ = Σ≡Prop λ f → isPropIsRingHom _ f _

𝒮ᴰ-Ring : DUARel (𝒮-Univ ℓ) RingStr ℓ
𝒮ᴰ-Ring =
  𝒮ᴰ-Record (𝒮-Univ _) IsRingEquiv
    (fields:
      data[ 0r ∣ null ∣ pres0 ]
      data[ 1r ∣ null ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ un ∣ pres- ]
      prop[ isRing ∣ (λ _ _ → isPropIsRing _ _ _ _ _) ])
 where
  open RingStr
  open IsRingHom

  -- faster with some sharing
  null = autoDUARel (𝒮-Univ _) (λ A → A)
  un = autoDUARel (𝒮-Univ _) (λ A → A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

RingPath : (R S : Ring ℓ) → RingEquiv R S ≃ (R ≡ S)
RingPath = ∫ 𝒮ᴰ-Ring .UARel.ua

uaRing : {A B : Ring ℓ} → RingEquiv A B → A ≡ B
uaRing {A = A} {B = B} = equivFun (RingPath A B)

isGroupoidRing : isGroupoid (Ring ℓ)
isGroupoidRing _ _ = isOfHLevelRespectEquiv 2 (RingPath _ _) (isSetRingEquiv _ _)

open RingStr
open IsRingHom

-- TODO: Induced structure results are temporarily inconvenient while we transition between algebra
-- representations
module _ (R : Ring ℓ) {A : Type ℓ}
  (0a 1a : A)
  (add mul : A → A → A)
  (inv : A → A)
  (e : ⟨ R ⟩ ≃ A)
  (p0 : e .fst (R .snd .0r) ≡ 0a)
  (p1 : e .fst (R .snd .1r) ≡ 1a)
  (p+ : ∀ x y → e .fst (R .snd ._+_ x y) ≡ add (e .fst x) (e .fst y))
  (p· : ∀ x y → e .fst (R .snd ._·_ x y) ≡ mul (e .fst x) (e .fst y))
  (pinv : ∀ x → e .fst (R .snd .-_ x) ≡ inv (e .fst x))
  where

  private
    module R = RingStr (R .snd)

    BaseΣ : Type (ℓ-suc ℓ)
    BaseΣ = Σ[ B ∈ Type ℓ ] B × B × (B → B → B) × (B → B → B) × (B → B)

    FamilyΣ : BaseΣ → Type ℓ
    FamilyΣ (B , u0 , u1 , a , m , i) = IsRing u0 u1 a m i

    inducedΣ : FamilyΣ (A , 0a , 1a , add , mul , inv)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel BaseΣ) (e , p0 , p1 , p+ , p· , pinv))
        R.isRing

  InducedRing : Ring ℓ
  InducedRing .fst = A
  0r (InducedRing .snd) = 0a
  1r (InducedRing .snd) = 1a
  _+_ (InducedRing .snd) = add
  _·_ (InducedRing .snd) = mul
  - InducedRing .snd = inv
  isRing (InducedRing .snd) = inducedΣ

  InducedRingEquiv : RingEquiv R InducedRing
  fst InducedRingEquiv = e
  pres0 (snd InducedRingEquiv) = p0
  pres1 (snd InducedRingEquiv) = p1
  pres+ (snd InducedRingEquiv) = p+
  pres· (snd InducedRingEquiv) = p·
  pres- (snd InducedRingEquiv) = pinv

  InducedRingPath : R ≡ InducedRing
  InducedRingPath = RingPath _ _ .fst InducedRingEquiv

-- Rings have an abelian group and a monoid

module _ ((A , (ringstr 0r 1r _+_ _·_ -_ R)) : Ring ℓ) where
  Ring→AbGroup : AbGroup ℓ
  Ring→AbGroup .fst = A
  Ring→AbGroup .snd .AbGroupStr.0g = 0r
  Ring→AbGroup .snd .AbGroupStr._+_ = _+_
  Ring→AbGroup .snd .AbGroupStr.-_ = -_
  Ring→AbGroup .snd .AbGroupStr.isAbGroup = IsRing.+IsAbGroup R

  Ring→MultMonoid : Monoid ℓ
  Ring→MultMonoid = monoid A 1r _·_ (IsRing.·IsMonoid R)

Ring→Group : Ring ℓ → Group ℓ
Ring→Group = AbGroup→Group ∘ Ring→AbGroup

Ring→AddMonoid : Ring ℓ → Monoid ℓ
Ring→AddMonoid = Group→Monoid ∘ Ring→Group

-- Smart constructor for ring homomorphisms
-- that infers the other equations from pres1, pres+, and pres·

module _ {R : Ring ℓ} {S : Ring ℓ'} {f : ⟨ R ⟩ → ⟨ S ⟩} where

  private
    module R = RingStr (R .snd)
    module S = RingStr (S .snd)

  module _
    (p1 : f R.1r ≡ S.1r)
    (p+ : (x y : ⟨ R ⟩) → f (x R.+ y) ≡ f x S.+ f y)
    (p· : (x y : ⟨ R ⟩) → f (x R.· y) ≡ f x S.· f y)
    where

    open IsRingHom
    private
      isGHom : IsGroupHom (Ring→Group R .snd) f (Ring→Group S .snd)
      isGHom = makeIsGroupHom p+

    makeIsRingHom : IsRingHom (R .snd) f (S .snd)
    makeIsRingHom .pres0 = isGHom .IsGroupHom.pres1
    makeIsRingHom .pres1 = p1
    makeIsRingHom .pres+ = p+
    makeIsRingHom .pres· = p·
    makeIsRingHom .pres- = isGHom .IsGroupHom.presinv

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Data.Tree where

open import Data.Tree.Base public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import sets.nat.ordering.leq.core public
open import sets.nat.ordering.leq.level public
open import sets.nat.ordering.leq.decide public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module InfConj where

open import Data.Bool
open import Data.Sum
open import Relation.Binary.PropositionalEquality

record Stream (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    hd : A
    tl : Stream A
open Stream public

-- | Partial elements
record D (A : Set) : Set where
  coinductive
  field step : A ⊎ D A
open D public

-- | Lift ⊎ to relations
data _⊎'_ {A B : Set} (R : A → A → Set) (S : B → B → Set) : A ⊎ B → A ⊎ B → Set where
  inj₁' : {x y : A} → R x y → (R ⊎' S) (inj₁ x) (inj₁ y)
  inj₂' : {x y : B} → S x y → (R ⊎' S) (inj₂ x) (inj₂ y)

-- | Bisimilarity for partial elements
record _~_ {A : Set} (x y : D A) : Set where
  coinductive
  field step~ : (_≡_ ⊎' _~_) (x .step) (y .step)
open _~_ public

-- | Injection into D
η : {A : Set} → A → D A
η a .step = inj₁ a

-- | Conjunction for partial Booleans
_∧'_ : D Bool → D Bool → D Bool
(x ∧' y) .step with x .step  | y .step
(x ∧' y) .step | inj₁ false  | v           = inj₁ false
(x ∧' y) .step | inj₁ true   | v           = v
(x ∧' y) .step | inj₂ x'     | inj₁ false  = inj₁ false
(x ∧' y) .step | inj₂ x'     | inj₁ true   = inj₂ x'
(x ∧' y) .step | inj₂ x'     | inj₂ y'     = inj₂ (x' ∧' y')

-- | Infinite conjunction
⋀∞ : Stream Bool → D Bool
⋀∞ s .step with s .hd
⋀∞ s .step | false = inj₁ false
⋀∞ s .step | true = inj₂ (⋀∞ (s .tl))

-- | Constant stream
K : {A : Set} → A → Stream A
K a .hd = a
K a .tl = K a

-- | Non-terminating computation
⊥ : {A : Set} → D A
⊥ .step = inj₂ ⊥

-- | Infinite conjunction of constant stream does not terminate
prop : ⋀∞ (K true) ~ ⊥
prop .step~ = inj₂' prop

-- | If there is an entry "false" in the stream, then the infinite conjunction
-- terminates. Here is just an example.
ex : ⋀∞ (false ∷ K true) ~ η false
ex .step~ = inj₁' refl

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- List membership and some related definitions
open import Level using (Level; _⊔_)
open import Relation.Binary
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
open import Relation.Nullary
open import Data.List
open import Data.List.Any
open import Function
import Relation.Binary.InducedPreorders as Ind
open import Data.Product as Prod using (∃; _×_; _,_)
module Membership-old {c ℓ : Level} (S : Setoid c ℓ) where

  private
    open module  S = Setoid S using (_≈_) renaming (Carrier to A)
    open module LS = Setoid (ListEq.setoid S)
      using () renaming (_≈_ to _≋_)

  -- If a predicate P respects the underlying equality then Any P
  -- respects the list equality.

  lift-resp : ∀ {p} {P : A → Set p} →
              P Respects _≈_ → Any P Respects _≋_
  lift-resp resp []            ()
  lift-resp resp (x≈y ∷ xs≈ys) (here px)   = here (resp x≈y px)
  lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
    there (lift-resp resp xs≈ys pxs)

  -- List membership.

  infix 4 _∈_ _∉_

  _∈_ : A → List A → Set _
  x ∈ xs = Any (_≈_ x) xs

  _∉_ : A → List A → Set _
  x ∉ xs = ¬ x ∈ xs

  -- Subsets.

  infix 4 _⊆_ _⊈_

  _⊆_ : List A → List A → Set _
  xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

  _⊈_ : List A → List A → Set _
  xs ⊈ ys = ¬ xs ⊆ ys

  -- Equality is respected by the predicate which is used to define
  -- _∈_.

  ∈-resp-≈ : ∀ {x} → (_≈_ x) Respects _≈_
  ∈-resp-≈ = flip S.trans

  -- List equality is respected by _∈_.

  ∈-resp-list-≈ : ∀ {x} → _∈_ x Respects _≋_
  ∈-resp-list-≈ = lift-resp ∈-resp-≈

  -- _⊆_ is a preorder.

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = Ind.InducedPreorder₂ (ListEq.setoid S) _∈_ ∈-resp-list-≈

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    open PreR ⊆-preorder public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

    infix 1 _∈⟨_⟩_

    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

  -- A variant of List.map.

  map-with-∈ : ∀ {b} {B : Set b}
               (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
  map-with-∈ []       f = []
  map-with-∈ (x ∷ xs) f = f (here S.refl) ∷ map-with-∈ xs (f ∘ there)

  -- Finds an element satisfying the predicate.

  find : ∀ {p} {P : A → Set p} {xs} →
         Any P xs → ∃ λ x → x ∈ xs × P x
  find (here px)   = (_ , here S.refl , px)
  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)

  lose : ∀ {p} {P : A → Set p} {x xs} →
         P Respects _≈_ → x ∈ xs → P x → Any P xs
  lose resp x∈xs px = Data.List.Any.map (flip resp px) x∈xs

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
data ⊤ : Set where tt : ⊤

record R : Set where
  constructor r
  field .x : ⊤

f : R → R
R.x (f (r x)) = {!x!}


text:
-- {-# OPTIONS -v tc.with:40 #-}

id : (A : Set) → A → A
id A = {!id′!}
 -- C-c C-h produces:       id′ : ∀ {A} → A
 -- when it should produce: id′ : ∀ {A} → A → A

f : (A : Set) (B : A → Set) (a : A) → B a
f A B a = {!g A a!}
  -- Before: ∀ {A} {B : A → Set} A₁ (a : A₁) → B a
  -- After:  ∀ A (a : A) {B : A → Set} → B a

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

open import Base

open import Homotopy.PushoutDef

module Homotopy.PushoutIsPushout {i} (d : pushout-diag i) where

import Homotopy.PushoutUP as PushoutUP
open PushoutUP d (λ _ → unit) -- A B C f g (λ _ → unit)

pushout-cocone : cocone (pushout d)
pushout-cocone = (left , right , glue)

factor-pushout : (E : Set i) → (cocone E → (pushout d → E))
factor-pushout E (A→top , B→top , h) = pushout-rec-nondep E A→top B→top h

abstract
  pushout-is-pushout : is-pushout (pushout d) pushout-cocone
  pushout-is-pushout E ⦃ tt ⦄ = iso-is-eq _ (factor-pushout E)
    (λ y → ap (λ u → _ , _ , u)
               (funext (λ x → pushout-β-glue-nondep E (cocone.A→top y)
                                    (cocone.B→top y) (cocone.h y) x)))
    (λ f → funext (pushout-rec _ (λ _ → refl) (λ _ → refl)
      (λ c → trans-app≡app
             (pushout-rec-nondep E (f ◯ left) (f ◯ right)
              (λ c' → ap f (glue c')))
             f (glue c) refl
             ∘ (ap (λ u → ! u ∘ ap f (glue c))
                  (pushout-β-glue-nondep E (f ◯ left) (f ◯ right)
                   (λ c' → ap f (glue c')) c)
                  ∘ opposite-left-inverse (ap f (glue c))))))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS -v tc.force:60 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.List

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

  [_] : A → List A
  [ x ] = x ∷ []

  data FSet : List A → Set a where
    sg  : (x : A) → FSet [ x ]
        -- ^ should be forced

  HOLE : Set
  HOLE = {!!}  -- just to force make bugs to look at the output


text:
module Numeral.Natural.Function.FlooredLogarithm where

open import Data
open import Data.Boolean.Stmt
open import Numeral.Natural
open import Numeral.Natural.Inductions
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.FlooredDivision.Proofs
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Structure.Relator.Ordering
open        Structure.Relator.Ordering.Strict.Properties

⌊log⌋ : (b : ℕ) → ⦃ _ : IsTrue(b ≥? 2) ⦄ → (n : ℕ) → ⦃ _ : IsTrue(n ≥? 1) ⦄ → ℕ
⌊log⌋ b@(𝐒(𝐒 _)) n = wellfounded-recursion (_<_) f(n) where
  f : (n : ℕ) → ((prev : ℕ) ⦃ _ : (prev < n) ⦄ → ℕ) → ℕ
  f 𝟎          _    = 𝟎
  f (𝐒 𝟎)      _    = 𝟎
  f n@(𝐒(𝐒 _)) prev = 𝐒(prev((n ⌊/⌋ b)) ⦃ [⌊/⌋]-ltₗ {b = b} ⦄)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural Literals
------------------------------------------------------------------------

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

module Data.Nat.Literals where

open import Agda.Builtin.FromNat
open import Agda.Builtin.Nat
open import Data.Unit

number : Number Nat
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ n → n
  }


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

module Fragment.Setoid.Morphism.Base where

open import Level using (Level; _⊔_)
open import Function using (_∘_; Congruent)

import Relation.Binary.PropositionalEquality as PE
open import Relation.Binary using (Setoid)

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level

module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where

  open Setoid S renaming (Carrier to A; _≈_ to _≈₁_)
  open Setoid T renaming (Carrier to B; _≈_ to _≈₂_)

  infixr 1 _↝_

  record _↝_ : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      ∣_∣      : A → B
      ∣_∣-cong : Congruent _≈₁_ _≈₂_ ∣_∣

open _↝_ public

lift : ∀ {A : Set a} {B : Setoid b ℓ₂}
       → (A → Setoid.Carrier B)
       → (PE.setoid A ↝ B)
lift {B = B} f
  = record { ∣_∣ = f
           ; ∣_∣-cong = reflexive ∘ (PE.cong f)
           }
     where open Setoid B

id : ∀ {A : Setoid a ℓ₁} → A ↝ A
id = record { ∣_∣ = λ x → x ; ∣_∣-cong = λ x → x }

_·_ : ∀ {A : Setoid a ℓ₁} {B : Setoid b ℓ₂} {C : Setoid c ℓ₃}
      → B ↝ C → A ↝ B → A ↝ C
g · f = record { ∣_∣      = ∣ g ∣ ∘ ∣ f ∣
               ; ∣_∣-cong = ∣ g ∣-cong ∘ ∣ f ∣-cong
               }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

module Data.Unit.Properties where

open import Data.Unit
open import Prelude

isProp⊤ : isProp ⊤
isProp⊤ _ _ = refl

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
postulate
  R : Set → Set1
  r : {X : Set} {{ _ : R X }} → X → Set
  A : Set
  a : A

instance
  RI : R A
  -- RI = {!!} -- uncommenting lets instance resolution succeed

foo : r a


text:
module Numeral.Natural.Relation.Divisibility.Proofs.Product where

open import Data.Tuple
open import Functional
open import Logic
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Numeral.Integer
import      Numeral.Integer.Oper as ℤ
open import Numeral.Integer.Proofs
import      Numeral.Integer.Relation.Divisibility as ℤ
import      Numeral.Integer.Relation.Divisibility.Proofs as ℤ
open import Numeral.Natural
open import Numeral.Natural.Coprime
open import Numeral.Natural.Coprime.Proofs
open import Numeral.Natural.Function.GreatestCommonDivisor.Extended
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Oper
open import Numeral.Natural.Prime
open import Numeral.Natural.Relation.Divisibility
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Structure.Relator
open import Syntax.Transitivity

private variable n x y d p : ℕ

-- When d and x does not have any common divisors, thus no common prime divisors, it means that all common prime divisors lies in d and y.
-- Also called: Generalized Euclid's lemma.
coprime-divides-of-[⋅] : (d ∣ (x ⋅ y)) → Coprime(d)(x) → (d ∣ y)
coprime-divides-of-[⋅] {d}{x}{y} dxy coprim
  with [∃]-intro (a , b) ⦃ p ⦄ ← gcd-linearCombination-existence {d}{x}
  = sub₂((ℤ._∣_) on₂ (+ₙ_))(_∣_) (substitute₂ᵣ(ℤ._∣_) {+ₙ d} eq div) where
    eq =
      ((+ₙ d) ℤ.⋅ a ℤ.⋅ (+ₙ y)) ℤ.+ ((+ₙ x) ℤ.⋅ b ℤ.⋅ (+ₙ y)) 🝖[ _≡_ ]-[ distributivityᵣ(ℤ._⋅_)(ℤ._+_) {(+ₙ d) ℤ.⋅ a}{(+ₙ x) ℤ.⋅ b}{+ₙ y} ]-sym
      (((+ₙ d) ℤ.⋅ a) ℤ.+ ((+ₙ x) ℤ.⋅ b)) ℤ.⋅ (+ₙ y)          🝖[ _≡_ ]-[ congruence₂ₗ(ℤ._⋅_)(+ₙ y) {_}{+ₙ 1} (p 🝖 congruence₁(+ₙ_) ([↔]-to-[→] Coprime-gcd coprim)) ]
      (+ₙ 1) ℤ.⋅ (+ₙ y)                                       🝖[ _≡_ ]-[ identityₗ(ℤ._⋅_)(+ₙ 1) ]
      (+ₙ y)                                                  🝖-end

    r-eq : (+ₙ(x ⋅ y)) ℤ.⋅ b ≡ (+ₙ x) ℤ.⋅ b ℤ.⋅ (+ₙ y)
    r-eq =
      (+ₙ (x ⋅ y)) ℤ.⋅ b        🝖[ _≡_ ]-[ congruence₂ₗ(ℤ._⋅_)(b) (preserving₂(+ₙ_)(_⋅_)(ℤ._⋅_)) ]
      ((+ₙ x) ℤ.⋅ (+ₙ y)) ℤ.⋅ b 🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {a = +ₙ x}{b = +ₙ y}{c = b} ]
      ((+ₙ x) ℤ.⋅ b) ℤ.⋅ (+ₙ y) 🝖-end

    div : (+ₙ d) ℤ.∣ ((+ₙ d) ℤ.⋅ a ℤ.⋅ (+ₙ y) ℤ.+ (+ₙ x) ℤ.⋅ b ℤ.⋅ (+ₙ y))
    div = ℤ.divides-with-[+] {+ₙ d}{(+ₙ d) ℤ.⋅ a ℤ.⋅ (+ₙ y)}{(+ₙ x) ℤ.⋅ b ℤ.⋅ (+ₙ y)}
      (ℤ.divides-with-[⋅] {+ₙ d}{(+ₙ d) ℤ.⋅ a} ([∨]-introₗ (ℤ.divides-with-[⋅] {+ₙ d}{+ₙ d} ([∨]-introₗ (reflexivity(_∣_))))))
      (substitute₂ᵣ(ℤ._∣_) {+ₙ d} r-eq (ℤ.divides-with-[⋅] {+ₙ d}{+ₙ(x ⋅ y)} ([∨]-introₗ dxy)))

-- A prime number dividing a product means that the prime divides one of its factors.
-- Obvious intuitively because prime numbers are the "smallest units" in the context of divisibility.
-- Also called: Euclid's lemma.
prime-divides-of-[⋅] : Prime(p) → (p ∣ (x ⋅ y)) → ((p ∣ x) ∨ (p ∣ y))
prime-divides-of-[⋅] {p}{x}{y} prim pxy with Prime-to-div-or-coprime {y = x} prim
... | [∨]-introₗ div    = [∨]-introₗ div
... | [∨]-introᵣ coprim = [∨]-introᵣ (coprime-divides-of-[⋅] pxy coprim)

Coprime-of-[⋅] : ∀{x y z} → Coprime(x)(y) → Coprime(x)(z) → Coprime(x)(y ⋅ z)
Coprime-of-[⋅] {x}{y}{z} xy (intro xz) = intro (\{n} → nx ↦ nyz ↦ xz nx (coprime-divides-of-[⋅] {n}{y}{z} nyz (divides-to-converse-coprime nx xy)))

Coprime-of-[^]ₗ : Coprime(x)(y) ← Coprime(x)(y ^ 𝐒(n))
Coprime-of-[^]ₗ {x}{y}{ℕ.𝟎}   p         = p
Coprime-of-[^]ₗ {x}{y}{ℕ.𝐒 n} (intro p) = Coprime-of-[^]ₗ {n = n} (intro \{d} dx dyn → p dx (divides-with-[⋅] {d}{y}{y ^ 𝐒(n)} ([∨]-introᵣ dyn)))

Coprime-of-[^]ᵣ : Coprime(x)(y) → Coprime(x)(y ^ n)
Coprime-of-[^]ᵣ {x}{y}{ℕ.𝟎}   p = symmetry(Coprime) Coprime-of-1
Coprime-of-[^]ᵣ {x}{y}{ℕ.𝐒 n} p = Coprime-of-[⋅] p (Coprime-of-[^]ᵣ {n = n} p)

-- Coprime-[+][⋅] : Coprime(x)(y) ↔ Coprime(x + y)(x ⋅ y)


text:
open import Agda.Primitive

variable
  @0 ℓ : Level
  A : Set ℓ

levelOf : A → Level
levelOf {a} _ = a

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda