text:
module Data.Num.Bounded where

open import Data.Num.Core
open import Data.Num.Maximum

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

------------------------------------------------------------------------
-- a system is bounded if there exists the greatest number
Bounded : ∀ b d o → Set
Bounded b d o = Σ[ xs ∈ Numeral b d o ] Maximum xs

Bounded-NullBase : ∀ d o → Bounded 0 (suc d) o
Bounded-NullBase d o = (greatest-digit d ∙) , (Maximum-NullBase-Greatest (greatest-digit d ∙) (greatest-digit-is-the-Greatest d))

Bounded-NoDigits : ∀ b o → ¬ (Bounded b 0 o)
Bounded-NoDigits b o (xs , claim) = NoDigits-explode xs

Bounded-AllZeros : ∀ b → Bounded (suc b) 1 0
Bounded-AllZeros b = (z ∙) , Maximum-AllZeros (z ∙)

Bounded-Proper : ∀ b d o → 2 ≤ suc (d + o) → ¬ (Bounded (suc b) (suc d) o)
Bounded-Proper b d o proper (xs , claim) =
    contradiction claim (Maximum-Proper xs proper)

Bounded? : ∀ b d o → Dec (Bounded b d o)
Bounded? b d o with numView b d o
Bounded? _ _ _ | NullBase d o
    = yes (Bounded-NullBase d o)
Bounded? _ _ _ | NoDigits b o
    = no (Bounded-NoDigits b o)
Bounded? _ _ _ | AllZeros b
    = yes (Bounded-AllZeros b)
Bounded? _ _ _ | Proper b d o proper
    = no (Bounded-Proper b d o proper)

--------------------------------------------------------------------------------
-- Misc

Maximum⇒Bounded : ∀ {b d o}
    → (xs : Numeral b d o)
    → Maximum xs
    → Bounded b d o
Maximum⇒Bounded xs max = xs , max

-- contraposition of Maximum⇒Bounded
¬Bounded⇒¬Maximum : ∀ {b d o}
    → (xs : Numeral b d o)
    → ¬ (Bounded b d o)
    → ¬ (Maximum xs)
¬Bounded⇒¬Maximum xs = contraposition (Maximum⇒Bounded xs)

-- begin
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ≡⟨ {!   !} ⟩
--     {!   !}
-- ∎

-- start
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- ≤⟨ {!   !} ⟩
--     {!   !}
-- □

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

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

open import Algebra.Bundles

module Algebra.Properties.DistributiveLattice
  {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
  where

open DistributiveLattice DL
import Algebra.Properties.Lattice as LatticeProperties
open import Algebra.Structures
open import Algebra.Definitions _≈_
open import Relation.Binary
open import Relation.Binary.Reasoning.Setoid setoid
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product using (_,_)

------------------------------------------------------------------------
-- Export properties of lattices

open LatticeProperties lattice public
  hiding (replace-equality)

------------------------------------------------------------------------
-- Other properties

∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_
∨-distribˡ-∧ x y z = begin
  x ∨ y ∧ z          ≈⟨ ∨-comm _ _ ⟩
  y ∧ z ∨ x          ≈⟨ ∨-distribʳ-∧ _ _ _ ⟩
  (y ∨ x) ∧ (z ∨ x)  ≈⟨ ∨-comm _ _ ⟨ ∧-cong ⟩ ∨-comm _ _ ⟩
  (x ∨ y) ∧ (x ∨ z)  ∎

∨-distrib-∧ : _∨_ DistributesOver _∧_
∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧

∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ x y z = begin
  x ∧ (y ∨ z)                ≈⟨ ∧-congʳ $ sym (∧-absorbs-∨ _ _) ⟩
  (x ∧ (x ∨ y)) ∧ (y ∨ z)    ≈⟨ ∧-congʳ $ ∧-congˡ $ ∨-comm _ _ ⟩
  (x ∧ (y ∨ x)) ∧ (y ∨ z)    ≈⟨ ∧-assoc _ _ _ ⟩
  x ∧ ((y ∨ x) ∧ (y ∨ z))    ≈⟨ ∧-congˡ $ sym (∨-distribˡ-∧ _ _ _) ⟩
  x ∧ (y ∨ x ∧ z)            ≈⟨ ∧-congʳ $ sym (∨-absorbs-∧ _ _) ⟩
  (x ∨ x ∧ z) ∧ (y ∨ x ∧ z)  ≈⟨ sym $ ∨-distribʳ-∧ _ _ _ ⟩
  x ∧ y ∨ x ∧ z              ∎

∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_
∧-distribʳ-∨ x y z = begin
  (y ∨ z) ∧ x    ≈⟨ ∧-comm _ _ ⟩
  x ∧ (y ∨ z)    ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
  x ∧ y ∨ x ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∨-cong ⟩ ∧-comm _ _ ⟩
  y ∧ x ∨ z ∧ x  ∎

∧-distrib-∨ : _∧_ DistributesOver _∨_
∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨

-- The dual construction is also a distributive lattice.

∧-∨-isDistributiveLattice : IsDistributiveLattice _≈_ _∧_ _∨_
∧-∨-isDistributiveLattice = record
  { isLattice    = ∧-∨-isLattice
  ; ∨-distribʳ-∧ = ∧-distribʳ-∨
  }

∧-∨-distributiveLattice : DistributiveLattice _ _
∧-∨-distributiveLattice = record
  { isDistributiveLattice = ∧-∨-isDistributiveLattice
  }

-- One can replace the underlying equality with an equivalent one.

replace-equality : {_≈′_ : Rel Carrier dl₂} →
                   (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) →
                   DistributiveLattice _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_                   = _≈′_
  ; _∧_                   = _∧_
  ; _∨_                   = _∨_
  ; isDistributiveLattice = record
    { isLattice    = Lattice.isLattice
                       (LatticeProperties.replace-equality lattice ≈⇔≈′)
    ; ∨-distribʳ-∧ = λ x y z → to ⟨$⟩ ∨-distribʳ-∧ x y z
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

∨-∧-distribˡ = ∨-distribˡ-∧
{-# WARNING_ON_USAGE ∨-∧-distribˡ
"Warning: ∨-∧-distribˡ was deprecated in v1.1.
Please use ∨-distribˡ-∧ instead."
#-}
∨-∧-distrib = ∨-distrib-∧
{-# WARNING_ON_USAGE ∨-∧-distrib
"Warning: ∨-∧-distrib was deprecated in v1.1.
Please use ∨-distrib-∧ instead."
#-}
∧-∨-distribˡ = ∧-distribˡ-∨
{-# WARNING_ON_USAGE ∧-∨-distribˡ
"Warning: ∧-∨-distribˡ was deprecated in v1.1.
Please use ∧-distribˡ-∨ instead."
#-}
∧-∨-distribʳ = ∧-distribʳ-∨
{-# WARNING_ON_USAGE ∧-∨-distribʳ
"Warning: ∧-∨-distribʳ was deprecated in v1.1.
Please use ∧-distribʳ-∨ instead."
#-}
∧-∨-distrib = ∧-distrib-∨
{-# WARNING_ON_USAGE ∧-∨-distrib
"Warning: ∧-∨-distrib was deprecated in v1.1.
Please use ∧-distrib-∨ instead."
#-}

ext: agda


text:
data ⊥ : Set where

postulate
  M : Set → Set
  A : Set
  _>>=_ : ∀ {A B} → M A → (A → M B) → M B
  ma : M A
  f  : A → M ⊥
  pure : ∀ {A} → A → M A

absurd-do : ∀ {A} → M A
absurd-do = do
  x  ← ma
  () ← f x

atabsurd-do : ∀ {A} → M A
atabsurd-do = do
  x      ← ma
  (y@()) ← f x -- I don't know why you would do that but we can support it

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-03-27, issue #2183
-- Better error message for splitting on non-visible dot pattern.

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

data Fin : Nat → Set where
  fzero : ∀ n → Fin (suc n)

test : ∀ n (i : Fin n) → Set
test n (fzero m)  = {!n!}  -- C-c C-c

-- Current error:
-- Cannot split on variable n, because it is bound to term  suc m
-- when checking that the expression ? has type Set

-- Desired behavior: succeed.


text:
module Formalization.ClassicalPropositionalLogic.Place where

open import Data.Boolean
open import Data.Tuple as Tuple using (_,_ ; _⨯_)
import      Lvl
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Functional as Fn using (_∘_ ; const)
open import Sets.PredicateSet using (PredSet)
open import Type

private variable ℓₚ ℓᵢ ℓ : Lvl.Level
private variable T A B I : Type{ℓ}
private variable f : A → B

module _ (P : Type{ℓₚ}) where
  private variable s e : Bool
  private variable p : P
  private variable φ ψ γ : Formula(P)

  record Index(I : Type{ℓ}) : Type{ℓ} where
    field
      id : I
      ∧ₗ : I → I
      ∧ᵣ : I → I
      ∨ₗ : I → I
      ∨ᵣ : I → I
      ⟶ₗ : I → I
      ⟶ᵣ : I → I

      ∧ₗ₀ : I → I
      ∧ᵣ₀ : I → I
      ∨ₗ₀ : I → I
      ∨ᵣ₀ : I → I
      ⟶ₗ₀ : I → I
      ⟶ᵣ₀ : I → I

  module _ (ind : Index(I)) where
    private variable i : I

    data Context : I → (Formula(P) → Formula(P)) → Type{Lvl.of(I) Lvl.⊔ ℓₚ} where
      identity     : Context(Index.id ind) Fn.id
      conjunctionₗ : Context(Index.∧ₗ₀ ind i) f → Context(Index.∧ₗ ind i) ((φ ∧_) ∘ f)
      conjunctionᵣ : Context(Index.∧ᵣ₀ ind i) f → Context(Index.∧ᵣ ind i) ((_∧ φ) ∘ f)
      disjunctionₗ : Context(Index.∨ₗ₀ ind i) f → Context(Index.∨ₗ ind i) ((φ ∨_) ∘ f)
      disjunctionᵣ : Context(Index.∨ᵣ₀ ind i) f → Context(Index.∨ᵣ ind i) ((_∨ φ) ∘ f)
      implicationₗ : Context(Index.⟶ₗ₀ ind i) f → Context(Index.⟶ₗ ind i) ((φ ⟶_) ∘ f)
      implicationᵣ : Context(Index.⟶ᵣ₀ ind i) f → Context(Index.⟶ᵣ ind i) ((_⟶ φ) ∘ f)

  Place : Bool → Bool → (Formula(P) → Formula(P)) → Type
  Place s e = Context index (s , e) where
    index : Index(Bool ⨯ Bool)
    Index.id index = (𝑇 , e)
    Index.∧ₗ index = Fn.id
    Index.∧ᵣ index = Fn.id
    Index.∨ₗ index = Fn.id
    Index.∨ᵣ index = Fn.id
    Index.⟶ₗ index = Fn.id
    Index.⟶ᵣ index = Tuple.map Fn.id (const 𝑇)
    Index.∧ₗ₀ index = Fn.id
    Index.∧ᵣ₀ index = Fn.id
    Index.∨ₗ₀ index = Fn.id
    Index.∨ᵣ₀ index = Fn.id
    Index.⟶ₗ₀ index = Fn.id
    Index.⟶ᵣ₀ index = Tuple.map not (const 𝑇)
  {-
  -- (Place s e F φ) means that the formula F lies on a (strictly (e = 𝐹) / not strictly (e = 𝑇)) (positive (s = 𝑇) / negative (s = 𝐹)) position in the formula φ.
  -- Also called: Occurrence, part, (strictly) positive/negative subformula.
  data Place : Bool → Bool → Formula(P) → Formula(P) → Type{ℓₚ} where
    refl         : Place 𝑇 e φ φ
    conjunctionₗ : Place s e γ φ       → Place s e γ (φ ∧ ψ)
    conjunctionᵣ : Place s e γ ψ       → Place s e γ (φ ∧ ψ)
    disjunctionₗ : Place s e γ φ       → Place s e γ (φ ∨ ψ)
    disjunctionᵣ : Place s e γ ψ       → Place s e γ (φ ∨ ψ)
    implicationₗ : Place (not s) e γ φ → Place s 𝑇 γ (φ ⟶ ψ)
    implicationᵣ : Place s e γ ψ       → Place s e γ (φ ⟶ ψ)
  -}

  StrictlyPositive = Place 𝑇 𝐹
  StrictlyNegative = Place 𝐹 𝐹
  Positive         = Place 𝑇 𝑇
  Negative         = Place 𝐹 𝑇

  strictly-negative-to-strictly-positive : Place 𝐹 𝐹 f → Place 𝑇 𝐹 f
  strictly-negative-to-strictly-positive (conjunctionₗ p) = conjunctionₗ (strictly-negative-to-strictly-positive p)
  strictly-negative-to-strictly-positive (conjunctionᵣ p) = conjunctionᵣ (strictly-negative-to-strictly-positive p)
  strictly-negative-to-strictly-positive (disjunctionₗ p) = disjunctionₗ (strictly-negative-to-strictly-positive p)
  strictly-negative-to-strictly-positive (disjunctionᵣ p) = disjunctionᵣ (strictly-negative-to-strictly-positive p)
  strictly-negative-to-strictly-positive (implicationₗ p) = implicationₗ (strictly-negative-to-strictly-positive p)

  strictly-to-not-strictly : Place s 𝐹 f → Place s 𝑇 f
  strictly-to-not-strictly identity         = identity
  strictly-to-not-strictly (conjunctionₗ p) = conjunctionₗ (strictly-to-not-strictly p)
  strictly-to-not-strictly (conjunctionᵣ p) = conjunctionᵣ (strictly-to-not-strictly p)
  strictly-to-not-strictly (disjunctionₗ p) = disjunctionₗ (strictly-to-not-strictly p)
  strictly-to-not-strictly (disjunctionᵣ p) = disjunctionᵣ (strictly-to-not-strictly p)
  strictly-to-not-strictly (implicationₗ p) = implicationₗ (strictly-to-not-strictly p)

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:
---------------------------------------------------------------------------
-- Normalization by Evaluation for Intuitionistic Propositional Logic
--
-- We employ a monadic interpreter for the soundness part,
-- and a special class of monads, called cover monads,
-- for the completeness part.
--
-- Normalization is completeness after soundness.
--
-- We give two instances of a cover monad: the free cover monad
-- and the continuation monad with normal forms as answer type.
---------------------------------------------------------------------------

{-# OPTIONS --postfix-projections #-}

open import Library

module NfModelMonad (Base : Set) where

import Formulas   ; open module Form = Formulas    Base
import Derivations; open module Der  = Derivations Base

---------------------------------------------------------------------------
-- Specification of a strong monad on presheaves.
-- Devoid of monad laws.

record Monad : Set₁ where

  -- Presheaf transformer.

  field
    C     : (P : Cxt → Set) (Γ : Cxt) → Set
    monC  : ∀{P} (monP : Mon P) → Mon (C P)

  -- Strong functor.

  field
    mapC' : ∀{P Q} → ⟨ P ⇒̂ Q ⊙ C P ⟩→̇ C Q

  -- Ordinary functor: an instance of mapC'.

  mapC : ∀{P Q} → (P →̇ Q) → (C P →̇ C Q)
  mapC f = mapC' λ τ → f

  -- Monad.

  field
    return : ∀{P} (monP : Mon P) → P →̇ C P
    joinC  : ∀{P} → C (C P) →̇ C P

  -- Kleisli extension.

  extC : ∀{P Q} → (P →̇ C Q) → C P →̇ C Q
  extC f = joinC ∘ mapC f

  -- Strong bind.

  bindC' : ∀{P Q} (monP : Mon P) → C P →̇ (P ⇒̂ C Q) ⇒̂ C Q
  bindC' monP c τ k = joinC (mapC' k (monC monP τ c))

---------------------------------------------------------------------------
-- A model of IPL parametrized by a strong monad.

module Soundness (monad : Monad) (open Monad monad) where

  -- The negative connectives True, ∧, and ⇒ are explained as usual by η-expansion
  -- and the meta-level connective.

  -- The positive connectives False and ∨ are inhabited by case trees.
  -- In case False, the tree has no leaves.
  -- In case A ∨ B, each leaf must be in the semantics of either A or B.

  T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
  T⟦ Atom P ⟧   = C (Ne' (Atom P))
  T⟦ False  ⟧   = C λ Δ → ⊥
  T⟦ A ∨ B  ⟧   = C λ Δ → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ
  T⟦ True   ⟧ Γ = ⊤
  T⟦ A ∧ B  ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
  T⟦ A ⇒ B  ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ B ⟧ Δ

  -- Monotonicity of the model is proven by induction on the proposition,
  -- using monotonicity of covers and the built-in monotonicity at implication.

  -- monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ

  monFalse : Mon (λ Γ → ⊥)
  monFalse τ ()

  mutual
    monT : ∀ A → Mon T⟦ A ⟧
    monT (Atom P)          = monC monNe
    monT False             = monC monFalse
    monT (A ∨ B)           = monC (monOr A B)
    monT True              = _
    monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
    monT (A ⇒ B) τ f σ     = f (σ • τ)

    monOr : ∀ A B → Mon (λ Γ → T⟦ A ⟧ Γ ⊎ T⟦ B ⟧ Γ)
    monOr A B τ = map-⊎ (monT A τ) (monT B τ)

  returnOr : ∀ A B {Γ} → T⟦ A ⟧ Γ ⊎ T⟦ B ⟧ Γ → T⟦ A ∨ B ⟧ Γ
  returnOr A B = return (monOr A B)

  -- We can run computations of semantic values.
  -- This replaces the paste (weak sheaf condition) of Beth models.

  run : ∀ A → C T⟦ A ⟧ →̇ T⟦ A ⟧
  run (Atom P)      = joinC
  run False         = joinC
  run (A ∨ B)       = joinC
  run True          = _
  run (A ∧ B)       = < run A ∘ mapC proj₁ , run B ∘ mapC proj₂  >
  run (A ⇒ B) c τ a = run B $ mapC' (λ δ f → f id≤ (monT A δ a)) $ monC (monT (A ⇒ B)) τ c

  -- Remark: A variant of run in the style of bind.

  run' : ∀ {P} (monP : Mon P) A → C P →̇ (P ⇒̂ T⟦ A ⟧) ⇒̂ T⟦ A ⟧
  run' monP (Atom p)          = bindC' monP
  run' monP False             = bindC' monP
  run' monP (A ∨ B)           = bindC' monP
  run' monP True              = _
  run' monP (A ∧ B) c τ k     = run' monP A c τ (λ σ → proj₁ ∘ k σ) , run' monP B c τ (λ σ → proj₂ ∘ k σ)
  run' monP (A ⇒ B) c τ k σ a = run' monP B c (σ • τ) λ σ' p → k (σ' • σ) p id≤ (monT A σ' a)

  -- Fundamental theorem (interpretation / soundness).

  -- Pointwise extension of T⟦_⟧ to contexts.

  G⟦_⟧ : ∀ (Γ Δ : Cxt) → Set
  G⟦ ε     ⟧ Δ = ⊤
  G⟦ Γ ∙ A ⟧ Δ = G⟦ Γ ⟧ Δ × T⟦ A ⟧ Δ

  -- monG : ∀{Γ Δ Φ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ → G⟦ Γ ⟧ Φ

  monG : ∀{Γ} → Mon G⟦ Γ ⟧
  monG {ε}     τ _       = _
  monG {Γ ∙ A} τ (γ , a) = monG τ γ , monT A τ a

  -- Variable case.

  lookup : ∀{Γ A} (x : Hyp A Γ) → G⟦ Γ ⟧ →̇ T⟦ A ⟧
  lookup top     = proj₂
  lookup (pop x) = lookup x ∘ proj₁

  -- A lemma for the orE case.

  orElim : ∀ A B C → ⟨ T⟦ A ∨ B ⟧ ⊙ T⟦ A ⇒ C ⟧ ⊙ T⟦ B ⇒ C ⟧ ⟩→̇ T⟦ C ⟧
  orElim A B C c g h = run C (mapC' (λ τ → [ g τ , h τ ]) c)

  orElim' : ∀ A B C → ⟨ T⟦ A ∨ B ⟧ ⊙ T⟦ A ⇒ C ⟧ ⊙ T⟦ B ⇒ C ⟧ ⟩→̇ T⟦ C ⟧
  orElim' A B C c g h = run' (monOr A B) C c id≤ λ τ → [ g τ , h τ ]

  -- A lemma for the falseE case.
  -- Casts an empty cover into any semantic value (by contradiction).

  falseElim : ∀ C → T⟦ False ⟧ →̇ T⟦ C ⟧
  falseElim C = run C ∘ mapC ⊥-elim

  -- The fundamental theorem

  eval :  ∀{A Γ} (t : Γ ⊢ A) → G⟦ Γ ⟧ →̇ T⟦ A ⟧
  eval (hyp x)           = lookup x
  eval (impI t)    γ τ a = eval t (monG τ γ , a)
  eval (impE t u)  γ     = eval t γ id≤ (eval u γ)
  eval (andI t u)  γ     = eval t γ , eval u γ
  eval (andE₁ t)         = proj₁ ∘ eval t
  eval (andE₂ t)         = proj₂ ∘ eval t
  eval (orI₁ {A} {B} t) γ = returnOr A B (inj₁ (eval t γ))
  eval (orI₂ {A} {B} t) γ = returnOr A B (inj₂ (eval t γ))
  eval (orE {A = A} {B} {C} t u v) γ = orElim A B C (eval t γ)
    (λ τ a → eval u (monG τ γ , a))
    (λ τ b → eval v (monG τ γ , b))
  eval {C} (falseE t) γ  = falseElim C (eval t γ)
  eval trueI       γ     = _

---------------------------------------------------------------------------
-- A strong monad with services to provide a cover.
-- Devoid of laws.

record CoverMonad : Set₁ where
  field
    monad : Monad
  open Monad monad public renaming (C to Cover)

  -- Services for case distinction.

  field
    falseC  : ∀{P} → Ne' False →̇ Cover P
    orC     : ∀{P Γ C D} (t : Ne Γ (C ∨ D))
                (c : Cover P (Γ ∙ C))
                (d : Cover P (Γ ∙ D)) → Cover P Γ

  -- Service for reification of into case trees.

  field
    runNf : ∀{A} → Cover (Nf' A) →̇ Nf' A

  -- A continuation version of runNf.

  runNf' : ∀ {A P} (monP : Mon P) → Cover P →̇ (P ⇒̂ Nf' A) ⇒̂ Nf' A
  runNf' monP c τ k = runNf (mapC' k (monC monP τ c))

---------------------------------------------------------------------------
-- Completeness of IPL via a cover monad.

module Completeness (covM : CoverMonad) (open CoverMonad covM) where
  open Soundness monad

  -- Reflection / reification, proven simultaneously by induction on the proposition.

  -- Reflection is η-expansion (and recursively reflection);
  -- at positive connections we build a case tree with a single scrutinee: the neutral
  -- we are reflecting.

  -- At implication, we need reification, which produces introductions
  -- and reifies the stored case trees.

  mutual

    fresh : ∀ {Γ} A → T⟦ A ⟧ (Γ ∙ A)
    fresh A = reflect A (hyp top)

    reflect : ∀ A → Ne' A →̇ T⟦ A ⟧
    reflect (Atom P) t     = return monNe t
    reflect False    t     = falseC t
    reflect (A ∨ B)  t     = orC t (returnOr A B (inj₁ (fresh A)))
                                   (returnOr A B (inj₂ (fresh B)))
    reflect True     t     = _
    reflect (A ∧ B)  t     = reflect A (andE₁ t) , reflect B (andE₂ t)
    reflect (A ⇒ B)  t τ a = reflect B (impE (monNe τ t) (reify A a))

    reify : ∀ A → T⟦ A ⟧ →̇ Nf' A
    reify (Atom P)        = runNf ∘ mapC ne
    reify False           = runNf ∘ mapC ⊥-elim
    reify (A ∨ B)         = runNf ∘ mapC [ orI₁ ∘ reify A , orI₂ ∘ reify B ]
    reify True _          = trueI
    reify (A ∧ B) (a , b) = andI (reify A a) (reify B b)
    reify (A ⇒ B) ⟦f⟧     = impI (reify B (⟦f⟧ (weak id≤) (fresh A)))

---------------------------------------------------------------------------
-- Normalization is completeness (reification) after soundness (evaluation)

module Normalization (covM : CoverMonad) (open CoverMonad covM) where
  open Soundness monad
  open Completeness covM

  -- Identity environment, constructed by reflection.

  freshG : ∀ Γ → G⟦ Γ ⟧ Γ
  freshG ε       = _
  freshG (Γ ∙ A) = monG (weak id≤) (freshG Γ) , fresh A

  -- A variant (no improvement).

  freshG' : ∀ Γ {Δ} (τ : Δ ≤ Γ) → G⟦ Γ ⟧ Δ
  freshG' ε       τ = _
  freshG' (Γ ∙ A) τ = freshG' Γ (τ • weak id≤) , monT A τ (fresh A)

  -- Normalization

  norm : ∀{A} → Tm A →̇ Nf' A
  norm t = reify _ (eval t (freshG _))

---------------------------------------------------------------------------
-- Case tree instance of cover monad

module CaseTree where

  data Cover (P : Cxt → Set) (Γ : Cxt) : Set where
    returnC : (p : P Γ) → Cover P Γ
    falseC  : (t : Ne Γ False) → Cover P Γ
    orC     : ∀{C D} (t : Ne Γ (C ∨ D))
                (c : Cover P (Γ ∙ C))
                (d : Cover P (Γ ∙ D)) → Cover P Γ

  return : ∀{P} (monP : Mon P) → P →̇ Cover P
  return monP p = returnC p

  -- Syntactic paste.

  runNf : ∀{A} → Cover (Nf' A) →̇ Nf' A
  runNf (returnC p) = p
  runNf (falseC t)  = falseE t
  runNf (orC t c d) = orE t (runNf c) (runNf d)

  -- Weakening covers:  A case tree in Γ can be transported to a thinning Δ
  -- by weakening all the scrutinees.

  monC : ∀{P} → (monP : Mon P) → Mon (Cover P)
  monC monP τ (returnC p) = returnC (monP τ p)
  monC monP τ (falseC t)  = falseC (monNe τ t)
  monC monP τ (orC t c d) = orC (monNe τ t) (monC monP (lift τ) c)
                                            (monC monP (lift τ) d)
  -- Monad.

  mapC : ∀{P Q} → (P →̇ Q) → (Cover P →̇ Cover Q)
  mapC f (returnC p) = returnC (f p)
  mapC f (falseC t)  = falseC t
  mapC f (orC t c d) = orC t (mapC f c) (mapC f d)

  joinC : ∀{P} → Cover (Cover P) →̇ Cover P
  joinC (returnC p) = p
  joinC (falseC t)  = falseC t
  joinC (orC t c d) = orC t (joinC c) (joinC d)

  -- Strong functoriality.

  mapC' : ∀{P Q Γ} → KFun P Q Γ → Cover P Γ → Cover Q Γ
  mapC' f (returnC p) = returnC (f id≤ p)
  mapC' f (falseC t)  = falseC t
  mapC' f (orC t c d) = orC t (mapC' (λ τ → f (τ • weak id≤)) c)
                              (mapC' (λ τ → f (τ • weak id≤)) d)

caseTreeMonad : CoverMonad
caseTreeMonad = record {monad = record{CaseTree}; CaseTree}

-- A normalization function using case trees.

open Normalization caseTreeMonad using () renaming (norm to normCaseTree)

---------------------------------------------------------------------------
-- Continuation instance of cover monad

module Continuation where

  record Cover (P : Cxt → Set) (Γ : Cxt) : Set where
    field runNf' : ∀ {A} → ((P ⇒̂ Nf' A) ⇒̂ Nf' A) Γ
  open Cover

  -- Services.

  runNf : ∀{A} → Cover (Nf' A) →̇ Nf' A
  runNf {A} {Γ} c = c .runNf' id≤ (λ τ → id)

  falseC : ∀{P} → Ne' False →̇ Cover P
  falseC t .runNf' τ k = falseE (monNe τ t)

  orC : ∀{P Γ C D} (t : Ne Γ (C ∨ D))
          (c : Cover P (Γ ∙ C))
          (d : Cover P (Γ ∙ D)) → Cover P Γ

  orC t c d .runNf' τ k = orE (monNe τ t)
    (c .runNf' (lift τ) (λ δ → k (δ • weak id≤)))
    (d .runNf' (lift τ) (λ δ → k (δ • weak id≤)))

  -- Monad infrastructure.

  monC : ∀{P} → (monP : Mon P) → Mon (Cover P)
  monC monP τ c .runNf' τ₁ k = c .runNf' (τ₁ • τ) k

  mapC' : ∀{P Q} → ⟨ P ⇒̂ Q ⊙ Cover P ⟩→̇ Cover Q
  mapC' k c .runNf' τ l = c .runNf' τ λ δ p → l δ (k (δ • τ) p)

  mapC : ∀{P Q} → (P →̇ Q) → (Cover P →̇ Cover Q)
  mapC f = mapC' λ τ → f

  return : ∀{P} (monP : Mon P) → P →̇ Cover P
  return monP p .runNf' τ k = k id≤ (monP τ p)

  joinC : ∀{P} → Cover (Cover P) →̇ Cover P
  joinC c .runNf' τ k = c .runNf' τ λ δ c' → c' .runNf' id≤ λ δ' → k (δ' • δ)

  extC : ∀{P Q} → (P →̇ Cover Q) → Cover P →̇ Cover Q
  extC f = joinC ∘ mapC f

  bindC' : ∀{P Q} → Cover P →̇ (P ⇒̂ Cover Q) ⇒̂ Cover Q
  bindC' c τ k .runNf' τ' k' = c .runNf' (τ' • τ) λ σ p → k (σ • τ') p .runNf' id≤ λ σ' → k' (σ' • σ)

continuationMonad : CoverMonad
continuationMonad = record{monad = record{Continuation}; Continuation}

-- A normalization function using continuations.

open Normalization continuationMonad using () renaming (norm to normContinuation)

-- Q.E.D.

-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module M where

Foo : Set
Foo = Set

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
{-# OPTIONS --safe --without-K #-}
module Data.List.Membership.Propositional.Distinct where

open import Data.List using (List)
import Relation.Binary.PropositionalEquality as P
open import Data.List.Membership.Setoid.Distinct as D hiding (Distinct) public

Distinct : ∀ {a} {A : Set a} → List A → Set a
Distinct {A = A} = D.Distinct {S = P.setoid A}

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
module Inst (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El
import Cxt
open Cxt Kind
import Loc
open Loc Kind
import Term
open Term Gnd U El
import Shift
open Shift Gnd U El

mutual
  winst : {G : Cxt}{C : Kind}{L : Loc}{I : Kind}
          (x : L ! I) -> G [ L bar x / Term C ]- I ->
          {T : Kind}(t : L [ Term C ]- T) -> [| Good G t |] ->
          G [ L bar x / Term C ]- T
  winst x i [ s ]     sg = G[ winsts x i s sg ]
  winst x i (fn A f)  fg = Gfn A \ a -> winst x i (f a) (fg a)
  winst x i (\\ b)    bg = G\\ (winst (pop x) (shift popH i) b bg)
  winst x i (h $ s)   pg = wing x i h (fst pg) (winsts x i s (snd pg))

  winsts : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind}
           (x : L ! I) -> G [ L bar x / Term C ]- I ->
           {T : Kind}(s : L [ Args C Z ]- T) -> [| Good G s |] ->
           G [ L bar x / Args C Z ]- T
  winsts x i (a ^ s)   sg = a G^ winsts x i s sg
  winsts x i (r & s)   pg = winst x i r (fst pg) G& winsts x i s (snd pg)
  winsts x i nil       _  = Gnil

  wing : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind}
         (x : L ! I) -> G [ L bar x / Term C ]- I ->
         {T : Kind}(h : L [ Head ]- T) -> [| Good G h |] ->
         G [ L bar x / Args C Z ]- T ->
         G [ L bar x / Term C ]- Ty Z
  wing x i (` k)     kg s = (` k -! kg) G$ s
  wing x i (# y)     _  s with varQV x y
  wing x i (# .x)    _  s  | vSame = go i s
  wing x i (# .(x thin y)) _ s | vDiff y = (# y -! _) G$ s

  go : {G : Cxt}{C : Kind}{L : Loc}{Z : Gnd}{I : Kind} ->
       G [ L / Term C ]- I -> G [ L / Args C Z ]- I ->
       G [ L / Term C ]- Ty Z
  go (fn A f -! fg) ((a ^ s) -! sg) = go (f a -! fg a) (s -! sg)
  go (\\ b -! bg) ((r & s) -! pg) =
    go (winst top (r -! fst pg) b bg) (s -! snd pg)
  go t (nil -! _) = t

inst : {G : Cxt}{C : Kind}{L : Loc}{I : Kind}
       (x : L ! I) -> G [ L bar x / Term C ]- I ->
       {T : Kind} -> G [ L / Term C ]- T -> G [ L bar x / Term C ]- T
inst x i (t -! tg) = winst x i t tg

_$$_ : {G : Cxt}{C S T : Kind}{L : Loc} ->
       G [! C !]- (S |> T) -> G [! C !]- S -> G [! C !]- T
(\\ b -! bg) $$ sg = inst top sg (b -! bg)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2015-05-06 issue reported by andor.penzes@prezi.com

record CoList : Set

data   CoList : Set where

record CoList where

-- Error WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Concrete/Definitions.hs:479

-- Error should be:
-- Duplicate definition of CoList


text:
------------------------------------------------------------------------
-- Sequential colimits
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- The definition of sequential colimits and the statement of the
-- non-dependent universal property are based on those in van Doorn's
-- "Constructing the Propositional Truncation using Non-recursive
-- HITs".

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining sequential colimits uses path
-- equality, but the supplied notion of equality is used for many
-- other things.

import Equality.Path as P

module Colimit.Sequential
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude

open import Bijection equality-with-J using (_↔_)
import Colimit.Sequential.Erased eq as E
import Colimit.Sequential.Very-erased eq as VE
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence P.equality-with-J as PEq
open import Function-universe equality-with-J hiding (id; _∘_)

private
  variable
    a b p q : Level
    A B     : Type a
    P       : A → Type p
    n       : ℕ
    e x     : A

------------------------------------------------------------------------
-- The type

-- Sequential colimits.

data Colimit (P : ℕ → Type p) (step : ∀ {n} → P n → P (suc n)) :
             Type p where
  ∣_∣    : P n → Colimit P step
  ∣∣≡∣∣ᴾ : (x : P n) → ∣ step x ∣ P.≡ ∣ x ∣

-- A variant of ∣∣≡∣∣ᴾ.

∣∣≡∣∣ : {step : ∀ {n} → P n → P (suc n)} (x : P n) →
        _≡_ {A = Colimit P step} ∣ step x ∣ ∣ x ∣
∣∣≡∣∣ x = _↔_.from ≡↔≡ (∣∣≡∣∣ᴾ x)

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ
         {P : ℕ → Type p} {step : ∀ {n} → P n → P (suc n)}
         (Q : Colimit P step → Type q) : Type (p ⊔ q) where
  no-eta-equality
  field
    ∣∣ʳ    : (x : P n) → Q ∣ x ∣
    ∣∣≡∣∣ʳ :
      (x : P n) →
      P.[ (λ i → Q (∣∣≡∣∣ᴾ x i)) ] ∣∣ʳ (step x) ≡ ∣∣ʳ x

open Elimᴾ public

elimᴾ :
  {step : ∀ {n} → P n → P (suc n)} {Q : Colimit P step → Type q} →
  Elimᴾ Q → (x : Colimit P step) → Q x
elimᴾ {P = P} {step = step} {Q = Q} e = helper
  where
  module E′ = Elimᴾ e

  helper : (x : Colimit P step) → Q x
  helper ∣ x ∣        = E′.∣∣ʳ x
  helper (∣∣≡∣∣ᴾ x i) = E′.∣∣≡∣∣ʳ x i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ
         (P : ℕ → Type p) (step : ∀ {n} → P n → P (suc n))
         (B : Type b) : Type (p ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : P n → B
    ∣∣≡∣∣ʳ : (x : P n) → ∣∣ʳ (step x) P.≡ ∣∣ʳ x

open Recᴾ public

recᴾ :
  {step : ∀ {n} → P n → P (suc n)} →
  Recᴾ P step B → Colimit P step → B
recᴾ r = elimᴾ λ where
    .∣∣ʳ    → R.∣∣ʳ
    .∣∣≡∣∣ʳ → R.∣∣≡∣∣ʳ
  where
  module R = Recᴾ r

-- A dependent eliminator.

record Elim
         {P : ℕ → Type p} {step : ∀ {n} → P n → P (suc n)}
         (Q : Colimit P step → Type q) : Type (p ⊔ q) where
  no-eta-equality
  field
    ∣∣ʳ    : (x : P n) → Q ∣ x ∣
    ∣∣≡∣∣ʳ : (x : P n) → subst Q (∣∣≡∣∣ x) (∣∣ʳ (step x)) ≡ ∣∣ʳ x

open Elim public

elim :
  {step : ∀ {n} → P n → P (suc n)} {Q : Colimit P step → Type q} →
  Elim Q → (x : Colimit P step) → Q x
elim e = elimᴾ λ where
    .∣∣ʳ      → E′.∣∣ʳ
    .∣∣≡∣∣ʳ x → subst≡→[]≡ (E′.∣∣≡∣∣ʳ x)
  where
  module E′ = Elim e

-- A "computation" rule.

elim-∣∣≡∣∣ : dcong (elim e) (∣∣≡∣∣ x) ≡ Elim.∣∣≡∣∣ʳ e x
elim-∣∣≡∣∣ = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec
         (P : ℕ → Type p) (step : ∀ {n} → P n → P (suc n))
         (B : Type b) : Type (p ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ    : P n → B
    ∣∣≡∣∣ʳ : (x : P n) → ∣∣ʳ (step x) ≡ ∣∣ʳ x

open Rec public

rec :
  {step : ∀ {n} → P n → P (suc n)} →
  Rec P step B → Colimit P step → B
rec r = recᴾ λ where
    .∣∣ʳ      → R.∣∣ʳ
    .∣∣≡∣∣ʳ x → _↔_.to ≡↔≡ (R.∣∣≡∣∣ʳ x)
  where
  module R = Rec r

-- A "computation" rule.

rec-∣∣≡∣∣ :
  {step : ∀ {n} → P n → P (suc n)} {r : Rec P step B} {x : P n} →
  cong (rec r) (∣∣≡∣∣ x) ≡ Rec.∣∣≡∣∣ʳ r x
rec-∣∣≡∣∣ = cong-≡↔≡ (refl _)

------------------------------------------------------------------------
-- The universal property

-- The universal property of the sequential colimit.

universal-property :
  {step : ∀ {n} → P n → P (suc n)} →
  (Colimit P step → B) ≃
  (∃ λ (f : ∀ n → P n → B) → ∀ n x → f (suc n) (step x) ≡ f n x)
universal-property {P = P} {B = B} {step = step} =
  Eq.↔→≃ to from to∘from from∘to
  where
  to :
    (Colimit P step → B) →
    ∃ λ (f : ∀ n → P n → B) → ∀ n x → f (suc n) (step x) ≡ f n x
  to h = (λ _ → h ∘ ∣_∣)
       , (λ _ x →
            h ∣ step x ∣  ≡⟨ cong h (∣∣≡∣∣ x) ⟩∎
            h ∣ x ∣       ∎)

  from :
    (∃ λ (f : ∀ n → P n → B) → ∀ n x → f (suc n) (step x) ≡ f n x) →
    Colimit P step → B
  from (f , g) = rec λ where
    .∣∣ʳ    → f _
    .∣∣≡∣∣ʳ → g _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f , g) = cong (f ,_) $ ⟨ext⟩ λ n → ⟨ext⟩ λ x →
    cong (rec _) (∣∣≡∣∣ x)  ≡⟨ rec-∣∣≡∣∣ ⟩∎
    g n x                   ∎

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣ʳ    _ → refl _
    .∣∣≡∣∣ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣≡∣∣ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-cong ⟩

      trans (sym (cong (from (to h)) (∣∣≡∣∣ x)))
        (trans (refl _) (cong h (∣∣≡∣∣ x)))                 ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                 rec-∣∣≡∣∣
                                                                 (trans-reflˡ _) ⟩

      trans (sym (cong h (∣∣≡∣∣ x))) (cong h (∣∣≡∣∣ x))     ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                ∎

-- A dependently typed variant of the sequential colimit's universal
-- property.

universal-property-Π :
  {step : ∀ {n} → P n → P (suc n)} →
  {Q : Colimit P step → Type q} →
  ((x : Colimit P step) → Q x) ≃
  (∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
     ∀ n x → subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x)
universal-property-Π {P = P} {step = step} {Q = Q} =
  Eq.↔→≃ to from to∘from from∘to
  where
  to :
    ((x : Colimit P step) → Q x) →
    ∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
      ∀ n x → subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x
  to h = (λ _ → h ∘ ∣_∣)
       , (λ _ x →
            subst Q (∣∣≡∣∣ x) (h ∣ step x ∣)  ≡⟨ dcong h (∣∣≡∣∣ x) ⟩∎
            h ∣ x ∣                           ∎)

  from :
    (∃ λ (f : ∀ n (x : P n) → Q ∣ x ∣) →
       ∀ n x → subst Q (∣∣≡∣∣ x) (f (suc n) (step x)) ≡ f n x) →
    (x : Colimit P step) → Q x
  from (f , g) = elim λ where
    .∣∣ʳ    → f _
    .∣∣≡∣∣ʳ → g _

  to∘from : ∀ p → to (from p) ≡ p
  to∘from (f , g) = cong (f ,_) $ ⟨ext⟩ λ n → ⟨ext⟩ λ x →
    dcong (elim _) (∣∣≡∣∣ x)  ≡⟨ elim-∣∣≡∣∣ ⟩∎
    g n x                     ∎

  from∘to : ∀ h → from (to h) ≡ h
  from∘to h = ⟨ext⟩ $ elim λ where
    .∣∣ʳ    _ → refl _
    .∣∣≡∣∣ʳ x →
      subst (λ z → from (to h) z ≡ h z) (∣∣≡∣∣ x) (refl _)  ≡⟨ subst-in-terms-of-trans-and-dcong ⟩

      trans (sym (dcong (from (to h)) (∣∣≡∣∣ x)))
        (trans (cong (subst Q (∣∣≡∣∣ x)) (refl _))
           (dcong h (∣∣≡∣∣ x)))                             ≡⟨ cong₂ (λ p q → trans (sym p) q)
                                                                 elim-∣∣≡∣∣
                                                                 (trans (cong (flip trans _) $
                                                                         cong-refl _) $
                                                                  trans-reflˡ _) ⟩

      trans (sym (dcong h (∣∣≡∣∣ x))) (dcong h (∣∣≡∣∣ x))   ≡⟨ trans-symˡ _ ⟩∎

      refl _                                                ∎

------------------------------------------------------------------------
-- Some conversion functions

-- E.Colimitᴱ P step implies Colimit P step.

Colimitᴱ→Colimit :
  {step : ∀ {n} → P n → P (suc n)} →
  E.Colimitᴱ P step → Colimit P step
Colimitᴱ→Colimit = E.rec λ where
  .E.∣∣ʳ    → ∣_∣
  .E.∣∣≡∣∣ʳ → ∣∣≡∣∣

-- In erased contexts E.Colimitᴱ P step is equivalent to
-- Colimit P step.

@0 Colimitᴱ≃Colimit :
  {step : ∀ {n} → P n → P (suc n)} →
  E.Colimitᴱ P step ≃ Colimit P step
Colimitᴱ≃Colimit = Eq.↔→≃
  Colimitᴱ→Colimit
  Colimit→Colimitᴱ
  (elim λ @0 where
     .∣∣ʳ _    → refl _
     .∣∣≡∣∣ʳ x →
       subst (λ x → Colimitᴱ→Colimit (Colimit→Colimitᴱ x) ≡ x)
         (∣∣≡∣∣ x) (refl _)                                     ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Colimitᴱ→Colimit ∘ Colimit→Colimitᴱ)
                     (∣∣≡∣∣ x)))
         (trans (refl _) (cong id (∣∣≡∣∣ x)))                   ≡⟨ cong₂ (trans ∘ sym)
                                                                     (trans (sym $ cong-∘ _ _ _) $
                                                                      trans (cong (cong Colimitᴱ→Colimit) rec-∣∣≡∣∣) $
                                                                      E.rec-∣∣≡∣∣)
                                                                     (trans (trans-reflˡ _) $
                                                                      sym $ cong-id _) ⟩

       trans (sym (∣∣≡∣∣ x)) (∣∣≡∣∣ x)                          ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                   ∎)
  (E.elim λ where
     .E.∣∣ʳ _    → refl _
     .E.∣∣≡∣∣ʳ x →
       subst (λ x → Colimit→Colimitᴱ (Colimitᴱ→Colimit x) ≡ x)
         (E.∣∣≡∣∣ x) (refl _)                                   ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Colimit→Colimitᴱ ∘ Colimitᴱ→Colimit)
                     (E.∣∣≡∣∣ x)))
         (trans (refl _) (cong id (E.∣∣≡∣∣ x)))                 ≡⟨ cong₂ (trans ∘ sym)
                                                                     (trans (sym $ cong-∘ _ _ _) $
                                                                      trans (cong (cong Colimit→Colimitᴱ) E.rec-∣∣≡∣∣) $
                                                                      rec-∣∣≡∣∣)
                                                                     (trans (trans-reflˡ _) $
                                                                      sym $ cong-id _) ⟩

       trans (sym (E.∣∣≡∣∣ x)) (E.∣∣≡∣∣ x)                      ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                   ∎)
  where
  Colimit→Colimitᴱ = rec λ @0 where
    .∣∣ʳ    → E.∣_∣
    .∣∣≡∣∣ʳ → E.∣∣≡∣∣

-- Some instances of VE.Colimitᴱ can be converted to instances of
-- Colimit. Note that P₀ and P₊ target the same universe.

Very-Colimitᴱ→Colimit :
  {P₀ : Type p}
  {P₊ : ℕ → Type p}
  {step₀ : P₀ → P₊ zero} →
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)} →
  VE.Colimitᴱ P₀ P₊ step₀ step₊ →
  Colimit
    (ℕ-rec P₀ (λ n _ → P₊ n))
    (λ {n} → ℕ-rec {P = λ n → ℕ-rec P₀ (λ n _ → P₊ n) n → P₊ n}
                   step₀ (λ _ _ → step₊) n)
Very-Colimitᴱ→Colimit = VE.rec λ where
  .VE.∣∣₀ʳ     → ∣_∣ {n = 0}
  .VE.∣∣₊ʳ     → ∣_∣
  .VE.∣∣₊≡∣∣₀ʳ → ∣∣≡∣∣
  .VE.∣∣₊≡∣∣₊ʳ → ∣∣≡∣∣

-- In erased contexts there are equivalences between some instances of
-- VE.Colimitᴱ and some instances of Colimit.

@0 Very-Colimitᴱ≃Colimit :
  {P₀ : Type p}
  {P₊ : ℕ → Type p}
  {step₀ : P₀ → P₊ zero} →
  {step₊ : ∀ {n} → P₊ n → P₊ (suc n)} →
  VE.Colimitᴱ P₀ P₊ step₀ step₊ ≃
  Colimit
    (ℕ-rec P₀ (λ n _ → P₊ n))
    (λ {n} → ℕ-rec {P = λ n → ℕ-rec P₀ (λ n _ → P₊ n) n → P₊ n}
                   step₀ (λ _ _ → step₊) n)
Very-Colimitᴱ≃Colimit = Eq.↔→≃
  Very-Colimitᴱ→Colimit
  Colimit→Colimitᴱ
  (elim λ @0 where
     .∣∣ʳ {n = zero} _    → refl _
     .∣∣ʳ {n = suc _} _   → refl _
     .∣∣≡∣∣ʳ {n = zero} x →
       subst (λ x → Very-Colimitᴱ→Colimit (Colimit→Colimitᴱ x) ≡ x)
         (∣∣≡∣∣ x) (refl _)                                          ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Very-Colimitᴱ→Colimit ∘ Colimit→Colimitᴱ)
                     (∣∣≡∣∣ x)))
         (trans (refl _) (cong id (∣∣≡∣∣ x)))                        ≡⟨ cong₂ (trans ∘ sym)
                                                                          (trans (sym $ cong-∘ _ _ _) $
                                                                           trans (cong (cong Very-Colimitᴱ→Colimit) rec-∣∣≡∣∣) $
                                                                           VE.rec-∣∣₊≡∣∣₀)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

       trans (sym (∣∣≡∣∣ x)) (∣∣≡∣∣ x)                               ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                        ∎
     .∣∣≡∣∣ʳ {n = suc _} x →
       subst (λ x → Very-Colimitᴱ→Colimit (Colimit→Colimitᴱ x) ≡ x)
         (∣∣≡∣∣ x) (refl _)                                          ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Very-Colimitᴱ→Colimit ∘ Colimit→Colimitᴱ)
                     (∣∣≡∣∣ x)))
         (trans (refl _) (cong id (∣∣≡∣∣ x)))                        ≡⟨ cong₂ (trans ∘ sym)
                                                                          (trans (sym $ cong-∘ _ _ _) $
                                                                           trans (cong (cong Very-Colimitᴱ→Colimit) rec-∣∣≡∣∣) $
                                                                           VE.rec-∣∣₊≡∣∣₊)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

       trans (sym (∣∣≡∣∣ x)) (∣∣≡∣∣ x)                               ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                        ∎)
  (VE.elim λ where
     .VE.∣∣₀ʳ _     → refl _
     .VE.∣∣₊ʳ _     → refl _
     .VE.∣∣₊≡∣∣₀ʳ x →
       subst (λ x → Colimit→Colimitᴱ (Very-Colimitᴱ→Colimit x) ≡ x)
         (VE.∣∣₊≡∣∣₀ x) (refl _)                                     ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Colimit→Colimitᴱ ∘ Very-Colimitᴱ→Colimit)
                     (VE.∣∣₊≡∣∣₀ x)))
         (trans (refl _) (cong id (VE.∣∣₊≡∣∣₀ x)))                   ≡⟨ cong₂ (trans ∘ sym)
                                                                          (trans (sym $ cong-∘ _ _ _) $
                                                                           trans (cong (cong Colimit→Colimitᴱ) VE.rec-∣∣₊≡∣∣₀) $
                                                                           rec-∣∣≡∣∣)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

       trans (sym (VE.∣∣₊≡∣∣₀ x)) (VE.∣∣₊≡∣∣₀ x)                     ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                        ∎
     .VE.∣∣₊≡∣∣₊ʳ x →
       subst (λ x → Colimit→Colimitᴱ (Very-Colimitᴱ→Colimit x) ≡ x)
         (VE.∣∣₊≡∣∣₊ x) (refl _)                                     ≡⟨ subst-in-terms-of-trans-and-cong ⟩

       trans (sym (cong (Colimit→Colimitᴱ ∘ Very-Colimitᴱ→Colimit)
                     (VE.∣∣₊≡∣∣₊ x)))
         (trans (refl _) (cong id (VE.∣∣₊≡∣∣₊ x)))                   ≡⟨ cong₂ (trans ∘ sym)
                                                                          (trans (sym $ cong-∘ _ _ _) $
                                                                           trans (cong (cong Colimit→Colimitᴱ) VE.rec-∣∣₊≡∣∣₊) $
                                                                           rec-∣∣≡∣∣)
                                                                          (trans (trans-reflˡ _) $
                                                                           sym $ cong-id _) ⟩

       trans (sym (VE.∣∣₊≡∣∣₊ x)) (VE.∣∣₊≡∣∣₊ x)                     ≡⟨ trans-symˡ _ ⟩∎

       refl _                                                        ∎)
  where
  Colimit→Colimitᴱ = rec λ @0 where
    .∣∣ʳ {n = zero}     → VE.∣_∣₀
    .∣∣ʳ {n = suc _}    → VE.∣_∣₊
    .∣∣≡∣∣ʳ {n = zero}  → VE.∣∣₊≡∣∣₀
    .∣∣≡∣∣ʳ {n = suc _} → VE.∣∣₊≡∣∣₊

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

{-
  Adapted from Ulrik's work in Lean (released under Apache License 2.0)
  https://github.com/leanprover/lean/blob/master/hott/homotopy/cellcomplex.hlean
-}

open import HoTT

module cw.CW where

open import cw.Attached public

{-
  Naming convension: most of them have the "cw-" prefix
-}

-- skeleton

Skeleton : ∀ {i} → ℕ → Type (lsucc i)
Realizer : ∀ {i} {n : ℕ} → Skeleton {i} n → Type i

Skeleton {i} O = Type i
Skeleton {i} (S n) =
  Σ (Skeleton {i} n)
    (λ s → Σ (Type i) λ A → Attaching (Realizer s) A (Sphere n))

Realizer {n = O} A = A
Realizer {n = S n} (s , (A , attaching)) = Attached attaching

⟦_⟧ = Realizer

-- Take a prefix of a skeleton

cw-take : ∀ {i} {m n : ℕ} (m≤n : m ≤ n) → Skeleton {i} n → Skeleton {i} m
cw-take (inl idp)        skel       = skel
cw-take (inr ltS)        (skel , _) = skel
cw-take (inr (ltSR m≤n)) (skel , _) = cw-take (inr m≤n) skel

cw-head : ∀ {i} {n : ℕ} → Skeleton {i} n → Type i
cw-head {n = O}   = cw-take (inl idp)
cw-head {n = S n} = cw-take (inr (O<S n))

incl^ : ∀ {i} {n : ℕ} (skel : Skeleton {i} n)
  → cw-head skel → ⟦ skel ⟧
incl^ {n = O}       skel       c = c
incl^ {n = S O}     (skel , _) c = incl c
incl^ {n = S (S n)} (skel , _) c = incl (incl^ skel c)

-- Pointedness

⊙Skeleton : ∀ {i} (n : ℕ) → Type (lsucc i)
⊙Skeleton n = Σ (Skeleton n) cw-head

⊙Realizer : ∀ {i} {n : ℕ} → ⊙Skeleton {i} n → Ptd i
⊙Realizer (skel , pt) = ⟦ skel ⟧ , incl^ skel pt

⊙⟦_⟧ = ⊙Realizer

-- Access the [m]th cells

cells-last : ∀ {i} {n : ℕ} → Skeleton {i} n → Type i
cells-last {n = O}   skel            = skel
cells-last {n = S n} (_ , cells , _) = cells

cells-nth : ∀ {i} {m n : ℕ} (m≤n : m ≤ n) → Skeleton {i} n → Type i
cells-nth m≤n = cells-last ∘ cw-take m≤n

-- Access the [m]th dimensional attaching map

Sphere₋₁ : ℕ → Type₀
Sphere₋₁ O = Empty
Sphere₋₁ (S n) = Sphere n

Realizer₋₁ : ∀ {i} {n : ℕ} → Skeleton {i} n → Type i
Realizer₋₁ {n = O}   _          = Lift Empty
Realizer₋₁ {n = S n} (skel , _) = ⟦ skel ⟧

⟦_⟧₋₁ = Realizer₋₁

attaching-last : ∀ {i} {n : ℕ} (s : Skeleton {i} n)
  → cells-last s → (Sphere₋₁ n → ⟦ s ⟧₋₁)
attaching-last {n = O}    _                  = λ{_ ()}
attaching-last {n = S n} (_ , _ , attaching) = attaching

attaching-nth : ∀ {i} {m n : ℕ} (m≤n : m ≤ n) (skel : Skeleton {i} n)
  → cells-nth m≤n skel → Sphere₋₁ m → ⟦ cw-take m≤n skel ⟧₋₁
attaching-nth m≤n = attaching-last ∘ cw-take m≤n

-- Misc

-- Extra conditions on CW complexes
-- XXX Needs a better name
has-dec-cells : ∀ {i} {n} → Skeleton {i} n → Type i
has-dec-cells {n = 0} skel = has-dec-eq skel
has-dec-cells {n = S n} (skel , cells , _) = has-dec-cells skel × has-dec-eq cells

-- Extra conditions on CW complexes for constructive degrees
-- The ideas is that boundaries maps need to be pointed after contraction
-- XXX Needs a better name
is-aligned : ∀ {i} {n} → Skeleton {i} n → Type i
is-aligned {n = 0} _ = Lift ⊤
is-aligned {n = 1} _ = Lift ⊤
is-aligned {n = S (S n)} (skel , _ , boundary) =
  is-aligned skel × (∀ c → hfiber incl (boundary c north))

{- Some basic CWs -}

-- Empty

CWEmpty-skel : Skeleton {lzero} 0
CWEmpty-skel = Empty
CWEmpty = ⟦ CWEmpty-skel ⟧

CWEmpty≃Empty : CWEmpty ≃ Empty
CWEmpty≃Empty = ide _

CWEmpty-is-aligned : is-aligned CWEmpty-skel
CWEmpty-is-aligned = lift tt

-- Unit

CWUnit-skel : Skeleton {lzero} 0
CWUnit-skel = Unit
CWUnit = ⟦ CWUnit-skel ⟧

CWUnit≃Unit : CWUnit ≃ Unit
CWUnit≃Unit = ide _

CWUnit-is-aligned : is-aligned CWUnit-skel
CWUnit-is-aligned = lift tt

{- Basic transformation  -}

-- dimension lifting

cw-lift₁ : ∀ {i} {n : ℕ} → Skeleton {i} n → Skeleton {i} (S n)
cw-lift₁ skel = skel , Lift Empty , λ{(lift ()) _}

-- This slightly extends the naming convension
-- to two skeletons being extensionally equal.
cw-lift₁-equiv : ∀ {i} {n} (skel : Skeleton {i} n)
  → ⟦ cw-lift₁ skel ⟧ ≃ ⟦ skel ⟧
cw-lift₁-equiv skel = equiv to incl to-incl incl-to
  where
    to : ⟦ cw-lift₁ skel ⟧ → ⟦ skel ⟧
    to = Attached-rec (idf ⟦ skel ⟧) (λ{(lift ())}) (λ{(lift ()) _})

    to-incl : ∀ x → to (incl x) == x
    to-incl _ = idp

    incl-to : ∀ x → incl (to x) == x
    incl-to = Attached-elim (λ _ → idp) (λ{(lift ())}) (λ{(lift ()) _})

cw-lift : ∀ {i} {n m : ℕ} → n < m → Skeleton {i} n → Skeleton {i} m
cw-lift ltS = cw-lift₁
cw-lift (ltSR lt) = cw-lift₁ ∘ cw-lift lt

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Inductive.Examples.Unit where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product
open import Data.List
open import Data.Vec

⊤ : Set
⊤ = Inductive (([] , []) ∷ [])

unit : ⊤
unit = construct zero [] []

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a preorder
------------------------------------------------------------------------

-- I think that the idea behind this library is originally Ulf
-- Norell's. I have adapted it to my tastes and mixfix operators,
-- though.

-- If you need to use several instances of this module in a given
-- file, then you can use the following approach:
--
--   import Relation.Binary.PreorderReasoning as Pre
--
--   f x y z = begin
--     ...
--       ∎
--     where open Pre preorder₁
--
--   g i j = begin
--     ...
--       ∎
--     where open Pre preorder₂

open import Relation.Binary

module Relation.Binary.PreorderReasoning
         {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

open Preorder P

infix  4 _IsRelatedTo_
infix  2 _∎
infixr 2 _∼⟨_⟩_ _≈⟨_⟩_ _≈⟨⟩_
infix  1 begin_

-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.

data _IsRelatedTo_ (x y : Carrier) : Set p₃ where
  relTo : (x∼y : x ∼ y) → x IsRelatedTo y

begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y

_∼⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
_ ∼⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

_≈⟨_⟩_ : ∀ x {y z} → x ≈ y → y IsRelatedTo z → x IsRelatedTo z
_ ≈⟨ x≈y ⟩ relTo y∼z = relTo (trans (reflexive x≈y) y∼z)

_≈⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≈⟨⟩ x∼y = x∼y

_∎ : ∀ x → x IsRelatedTo x
_∎ _ = relTo refl


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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Structures.GL
  {k ℓᵏ} (K : Field k ℓᵏ)
  {a ℓ}
  where

open import Relation.Binary using (Setoid)
open import Algebra.Linear.Structures.Bundles
open import Algebra.Linear.Morphism.Bundles K
open import Categories.Category

open LinearMap

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text: module Imports.TheWrongName where


text:
-- Prop has been removed from the language
module PropNoMore where

postulate
  X : Prop


text:
{-A
Polynomials over commutative rings
==================================
-}
{-# OPTIONS --safe #-}

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

module Cubical.Algebra.Polynomials where

open import Cubical.HITs.PropositionalTruncation
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Nat renaming (_+_ to _Nat+_; _·_ to _Nat·_) hiding (·-comm)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty.Base renaming (rec to ⊥rec )
open import Cubical.Data.Bool

open import Cubical.Algebra.Group hiding (Bool)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

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

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

module PolyMod (R' : CommRing ℓ) where
  private
    R = fst R'
  open CommRingStr (snd R') public

-------------------------------------------------------------------------------------------
-- First definition of a polynomial.
-- A polynomial a₁ +  a₂x + ... + aⱼxʲ of degree j is represented as a list [a₁, a₂, ...,aⱼ]
-- modulo trailing zeros.
-------------------------------------------------------------------------------------------

  data Poly : Type ℓ where
    []    : Poly
    _∷_  : (a : R) → (p : Poly) → Poly
    drop0 : 0r ∷ [] ≡ []

  infixr 5 _∷_

  module Elim (B      : Poly → Type ℓ')
              ([]*    : B [])
              (cons*  : (r : R) (p : Poly) (b : B p) → B (r ∷ p))
              (drop0* : PathP (λ i → B (drop0 i)) (cons* 0r [] []*) []*) where

   f : (p : Poly) → B p
   f [] = []*
   f (x ∷ p) = cons* x p (f p)
   f (drop0 i) = drop0* i

  -- Given a proposition (as type) ϕ ranging over polynomials, we prove it by:
  -- ElimProp.f ϕ ⌜proof for base case []⌝ ⌜proof for induction case a ∷ p⌝
  --           ⌜proof that ϕ actually is a proposition over the domain of polynomials⌝
  module ElimProp (B : Poly → Type ℓ')
                  ([]* : B [])
                  (cons* : (r : R) (p : Poly) (b : B p) → B (r ∷ p))
                  (BProp : {p : Poly} → isProp (B p)) where
   f : (p : Poly) → B p
   f = Elim.f B []* cons* (toPathP (BProp (transport (λ i → B (drop0 i)) (cons* 0r [] []*)) []*))

  module Rec (B : Type ℓ')
             ([]* : B)
             (cons* : R → B → B)
             (drop0* : cons* 0r []* ≡ []*)
             (Bset : isSet B) where
    f : Poly → B
    f = Elim.f (λ _ → B) []* (λ r p b → cons* r b) drop0*

  module RecPoly ([]* : Poly) (cons* : R → Poly → Poly) (drop0* : cons* 0r []* ≡ []*) where
    f : Poly → Poly
    f [] = []*
    f (a ∷ p) = cons* a (f p)
    f (drop0 i) = drop0* i

--------------------------------------------------------------------------------------------------
-- Second definition of a polynomial. The purpose of this second definition is to
-- facilitate the proof that the first definition is a set. The two definitions are
-- then shown to be equivalent.
-- A polynomial a₀ +  a₁x + ... + aⱼxʲ of degree j is represented as a function f
-- such that for i ∈ ℕ we have  f(i) = aᵢ if i ≤ j, and 0 for i > j
--------------------------------------------------------------------------------------------------

  PolyFun : Type ℓ
  PolyFun = Σ[ p ∈ (ℕ → R) ] (∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → p m ≡ 0r))

  isSetPolyFun : isSet PolyFun
  isSetPolyFun = isSetΣSndProp (isSetΠ (λ x → isSetCommRing R')) λ f x y → squash x y

  --construction of the function that represents the polynomial
  Poly→Fun : Poly → (ℕ → R)
  Poly→Fun [] = (λ _ → 0r)
  Poly→Fun (a ∷ p) = (λ n → if isZero n then a else Poly→Fun p (predℕ n))
  Poly→Fun (drop0 i) = lemma i
    where
    lemma : (λ n → if isZero n then 0r else 0r) ≡ (λ _ → 0r)
    lemma i zero = 0r
    lemma i (suc n) = 0r

  Poly→Prf : (p : Poly) → ∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → (Poly→Fun p m ≡ 0r))
  Poly→Prf = ElimProp.f (λ p →  ∃[ n ∈ ℕ ] ((m : ℕ) → n ≤ m → (Poly→Fun p m ≡ 0r)))
                        ∣ 0 , (λ m ineq → refl) ∣
                        (λ r p → map ( λ (n , ineq) → (suc n) ,
                                       λ { zero h → ⊥rec (znots (sym (≤0→≡0 h))) ;
                                           (suc m) h → ineq m (pred-≤-pred h)
                                         }
                                     )
                        )
                        squash

  Poly→PolyFun : Poly → PolyFun
  Poly→PolyFun p = (Poly→Fun p) , (Poly→Prf p)

----------------------------------------------------
-- Start of code by Anders Mörtberg and Evan Cavallo

  at0 : (ℕ → R) → R
  at0 f = f 0

  atS : (ℕ → R) → (ℕ → R)
  atS f n = f (suc n)

  polyEq : (p p' : Poly) → Poly→Fun p ≡ Poly→Fun p' → p ≡ p'
  polyEq [] [] _ = refl
  polyEq [] (a ∷ p') α =
    sym drop0 ∙∙ cong₂ _∷_ (cong at0 α) (polyEq [] p' (cong atS α)) ∙∙ refl
  polyEq [] (drop0 j) α k =
    hcomp
      (λ l → λ
        { (j = i1) → drop0 l
        ; (k = i0) → drop0 l
        ; (k = i1) → drop0 (j ∧ l)
        })
      (is-set 0r 0r (cong at0 α) refl j k ∷ [])
  polyEq (a ∷ p) [] α =
    refl ∙∙ cong₂ _∷_ (cong at0 α) (polyEq p [] (cong atS α)) ∙∙ drop0
  polyEq (a ∷ p) (a₁ ∷ p') α =
    cong₂ _∷_ (cong at0 α) (polyEq p p' (cong atS α))
  polyEq (a ∷ p) (drop0 j) α k =
    hcomp -- filler
      (λ l → λ
        { (k = i0) → a ∷ p
        ; (k = i1) → drop0 (j ∧ l)
        ; (j = i0) → at0 (α k) ∷ polyEq p [] (cong atS α) k
        })
      (at0 (α k) ∷ polyEq p [] (cong atS α) k)
  polyEq (drop0 i) [] α k =
    hcomp
      (λ l → λ
        { (i = i1) → drop0 l
        ; (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → drop0 l
        })
      (is-set 0r 0r (cong at0 α) refl i k ∷ [])
  polyEq (drop0 i) (a ∷ p') α k =
    hcomp -- filler
      (λ l → λ
        { (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → a ∷ p'
        ; (i = i0) → at0 (α k) ∷ polyEq [] p' (cong atS α) k
        })
      (at0 (α k) ∷ polyEq [] p' (cong atS α) k)
  polyEq (drop0 i) (drop0 j) α k =
    hcomp
      (λ l → λ
        { (k = i0) → drop0 (i ∧ l)
        ; (k = i1) → drop0 (j ∧ l)
        ; (i = i0) (j = i0) → at0 (α k) ∷ []
        ; (i = i1) (j = i1) → drop0 l
        })
      (is-set 0r 0r (cong at0 α) refl (i ∧ j) k ∷ [])

  PolyFun→Poly+ : (q : PolyFun) → Σ[ p ∈ Poly ] Poly→Fun p ≡ q .fst
  PolyFun→Poly+ (f , pf) = rec lem (λ x → rem1 f (x .fst) (x .snd) ,
                                               funExt (rem2 f (fst x) (snd x))
                                   ) pf
    where
    lem : isProp (Σ[ p ∈ Poly ] Poly→Fun p ≡ f)
    lem (p , α) (p' , α') =
      ΣPathP (polyEq p p' (α ∙ sym α'), isProp→PathP (λ i → (isSetΠ λ _ → is-set) _ _) _ _)

    rem1 : (p : ℕ → R) (n : ℕ) → ((m : ℕ) → n ≤ m → p m ≡ 0r) → Poly
    rem1 p zero h = []
    rem1 p (suc n) h = p 0 ∷ rem1 (λ x → p (suc x)) n (λ m x → h (suc m) (suc-≤-suc x))

    rem2 : (f : ℕ → R) (n : ℕ) → (h : (m : ℕ) → n ≤ m → f m ≡ 0r) (m : ℕ) →
                                                                 Poly→Fun (rem1 f n h) m ≡ f m
    rem2 f zero h m = sym (h m zero-≤)
    rem2 f (suc n) h zero = refl
    rem2 f (suc n) h (suc m) = rem2 (λ x → f (suc x)) n (λ k p → h (suc k) (suc-≤-suc p)) m

  PolyFun→Poly : PolyFun → Poly
  PolyFun→Poly q = PolyFun→Poly+ q .fst

  PolyFun→Poly→PolyFun : (p : Poly) → PolyFun→Poly (Poly→PolyFun p) ≡ p
  PolyFun→Poly→PolyFun p = polyEq _ _ (PolyFun→Poly+ (Poly→PolyFun p) .snd)

--End of code by Mörtberg and Cavallo
-------------------------------------

  isSetPoly : isSet Poly
  isSetPoly = isSetRetract Poly→PolyFun
                           PolyFun→Poly
                           PolyFun→Poly→PolyFun
                           isSetPolyFun

-------------------------------------------------
-- The rest of the file uses the first definition
-------------------------------------------------

  open CommRingTheory R'
  open RingTheory (CommRing→Ring R')
  open GroupTheory (Ring→Group (CommRing→Ring R'))

  pattern [_] x = x ∷ []

---------------------------------------
-- Definition
-- Identity for addition of polynomials
---------------------------------------
  0P : Poly
  0P = []

  --ReplicatePoly(n,p) returns 0 ∷ 0 ∷ ... ∷ [] (n zeros)
  ReplicatePoly0 : (n : ℕ)  → Poly
  ReplicatePoly0 zero  = 0P
  ReplicatePoly0 (suc n) = 0r ∷ ReplicatePoly0 n

  --The empty polynomial has multiple equal representations on the form 0 + 0x + 0 x² + ...
  replicatePoly0Is0P : ∀ (n : ℕ) → ReplicatePoly0 n ≡ 0P
  replicatePoly0Is0P zero = refl
  replicatePoly0Is0P (suc n) = (cong (0r ∷_) (replicatePoly0Is0P n)) ∙ drop0

-----------------------------
-- Definition
-- subtraction of polynomials
-----------------------------
  Poly- : Poly → Poly
  Poly- [] = []
  Poly- (a ∷ p) = (- a) ∷ (Poly- p)
  Poly- (drop0 i) = (cong (_∷ []) (inv1g) ∙ drop0) i

  -- Double negation (of subtraction of polynomials) is the identity mapping
  Poly-Poly- : (p : Poly) → Poly- (Poly- p) ≡ p
  Poly-Poly- = ElimProp.f (λ x → Poly- (Poly- x) ≡ x)
                          refl
                          (λ a p e → cong (_∷ (Poly- (Poly- p)))
                                          (-Idempotent a) ∙ cong (a ∷_ ) (e))
                          (isSetPoly _ _)

---------------------------
-- Definition
-- addition for polynomials
---------------------------
  _Poly+_ : Poly → Poly → Poly
  p Poly+ [] = p
  [] Poly+ (drop0 i) = drop0 i
  [] Poly+ (b ∷ q) = b ∷ q
  (a ∷ p) Poly+ (b ∷ q) = (a + b) ∷ (p Poly+ q)
  (a ∷ p) Poly+ (drop0 i) = +Rid a i ∷ p
  (drop0 i) Poly+ (a ∷ q) = lem q i  where
                                 lem : ∀ q → (0r + a) ∷ ([] Poly+ q) ≡ a ∷ q
                                 lem = ElimProp.f (λ q → (0r + a) ∷ ([] Poly+ q) ≡ a ∷ q)
                                                  (λ i → (+Lid a i ∷ []))
                                                  (λ r p _ → λ i → +Lid a i ∷ r ∷ p )
                                                  (isSetPoly _ _)
  (drop0 i) Poly+ (drop0 j) =  isSet→isSet' isSetPoly  (cong ([_] ) (+Rid 0r)) drop0
                                                       (cong ([_] ) (+Lid 0r)) drop0 i j

  -- [] is the left identity for Poly+
  Poly+Lid : ∀ p → ([] Poly+ p ≡ p)
  Poly+Lid =  ElimProp.f (λ p → ([] Poly+ p ≡ p) )
                         refl
                         (λ r p prf → refl)
                         (λ x y → isSetPoly _ _ x y)

  -- [] is the right identity for Poly+
  Poly+Rid : ∀ p → (p Poly+ [] ≡ p)
  Poly+Rid p = refl

  --Poly+ is Associative
  Poly+Assoc : ∀ p q r → p Poly+ (q Poly+ r) ≡ (p Poly+ q) Poly+ r
  Poly+Assoc =
    ElimProp.f (λ p → (∀ q r → p Poly+ (q Poly+ r) ≡ (p Poly+ q) Poly+ r))
               (λ q r → Poly+Lid (q Poly+ r) ∙ cong (_Poly+ r)  (sym (Poly+Lid q)))
               (λ a p prf → ElimProp.f ((λ q → ∀ r → ((a ∷ p) Poly+ (q Poly+ r)) ≡
                                                   (((a ∷ p) Poly+ q) Poly+ r)))
                                       (λ r → cong ((a ∷ p) Poly+_) (Poly+Lid r))
                                       (λ b q prf2 →
                                       ElimProp.f
                                         (λ r → ((a ∷ p) Poly+ ((b ∷ q) Poly+ r)) ≡
                                                 ((a + b ∷ (p Poly+ q)) Poly+ r))
                                         refl
                                         (λ c r prfp → cong ((a + (b + c))∷_)
                                                            (prf q r) ∙
                                                            (cong (_∷ ((p Poly+ q) Poly+ r))
                                                                  (+Assoc a b c)))
                                         (isSetPoly _ _))
                                       λ x y i r → isSetPoly (x r i0) (y r i1) (x r) (y r) i)
                λ x y i q r  → isSetPoly _ _ (x q r) (y q r) i

  -- for any polynomial, p, the additive inverse is given by Poly- p
  Poly+Inverses : ∀ p → p Poly+ (Poly- p) ≡ []
  Poly+Inverses = ElimProp.f ( λ p → p Poly+ (Poly- p) ≡ [])
                             refl --(Poly+Lid (Poly- []))
                             (λ r p prf → cong (r + - r ∷_) prf ∙
                                          (cong (_∷ [])  (+Rinv r) ∙ drop0))
                             (isSetPoly _ _)

  --Poly+ is commutative
  Poly+Comm : ∀ p q → p Poly+ q ≡ q Poly+ p
  Poly+Comm = ElimProp.f (λ p → (∀ q → p Poly+ q ≡ q Poly+ p))
                         (λ q → Poly+Lid q)
                         (λ a p prf → ElimProp.f (λ q → ((a ∷ p) Poly+ q) ≡ (q Poly+ (a ∷ p)))
                                                 refl
                                                 (λ b q prf2 → cong (_∷ (p Poly+ q)) (+Comm a b) ∙
                                                               cong ((b + a) ∷_) (prf q))
                                                 (isSetPoly _ _)
                         )
                         (λ {p} → isPropΠ (λ q → isSetPoly (p Poly+ q) (q Poly+ p)))

--------------------------------------------------------------
-- Definition
-- multiplication of a polynomial by a (constant) ring element
--------------------------------------------------------------
  _PolyConst*_ : (R) → Poly → Poly
  r PolyConst* [] = []
  r PolyConst* (a ∷ p) = (r · a) ∷ (r PolyConst* p)
  r PolyConst* (drop0 i) = lem r i where
                                 lem : ∀ r → [ r · 0r ] ≡ []
                                 lem =  λ r → [ r · 0r ] ≡⟨ cong (_∷ []) (0RightAnnihilates r) ⟩
                                        [ 0r ] ≡⟨ drop0 ⟩
                                        [] ∎

  -- For any polynomial p we have: 0 _PolyConst*_ p = []
  0rLeftAnnihilatesPoly : ∀ q → 0r PolyConst* q ≡ [ 0r ]
  0rLeftAnnihilatesPoly = ElimProp.f (λ q → 0r PolyConst* q ≡ [ 0r ])
                                         (sym drop0)
                                         (λ r p prf → cong ((0r · r) ∷_) prf ∙
                                                      cong (_∷ [ 0r ]) (0LeftAnnihilates r) ∙
                                                      cong (0r ∷_) drop0 )
                                         λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: 1 _PolyConst*_ p = p
  PolyConst*Lid : ∀ q → 1r PolyConst* q ≡ q
  PolyConst*Lid = ElimProp.f (λ q → 1r PolyConst* q ≡ q ) refl
                             (λ a p prf → cong (_∷ (1r PolyConst* p)) (·Lid a) ∙
                                          cong (a ∷_) (prf) )
                             λ x y → isSetPoly _ _ x y

--------------------------------
-- Definition
-- Multiplication of polynomials
--------------------------------
  _Poly*_ : Poly → Poly → Poly
  [] Poly* q = []
  (a ∷ p) Poly* q = (a PolyConst* q) Poly+ (0r ∷ (p Poly* q))
  (drop0 i) Poly* q = lem q i where
                               lem : ∀ q → (0r PolyConst* q) Poly+ [ 0r ] ≡ []
                               lem = λ q → ((0r PolyConst* q) Poly+ [ 0r ]) ≡⟨ cong ( _Poly+ [ 0r ] ) (0rLeftAnnihilatesPoly q)⟩
                                           ([ 0r ] Poly+ [ 0r ]) ≡⟨ cong (_∷ []) 0Idempotent  ∙ drop0 ⟩
                                           [] ∎

--------------------
--Definition
--Identity for Poly*
--------------------
  1P : Poly
  1P = [ 1r ]

  -- For any polynomial p we have: p Poly* [] = []
  0PRightAnnihilates : ∀ q → 0P Poly* q ≡ 0P
  0PRightAnnihilates = ElimProp.f (λ q → 0P Poly* q ≡ 0P)
                                  refl
                                  (λ r p prf → prf)
                                  λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: [] Poly* p = []
  0PLeftAnnihilates : ∀ p → p Poly* 0P ≡ 0P
  0PLeftAnnihilates = ElimProp.f (λ p → p Poly* 0P ≡ 0P )
                                 refl
                                 (λ r p prf → cong (0r ∷_) prf ∙ drop0)
                                 λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: p Poly* [ 1r ] = p
  Poly*Lid : ∀ q → 1P Poly* q ≡ q
  Poly*Lid =
    ElimProp.f (λ q → 1P Poly* q ≡ q)
               drop0
               (λ r p prf → lemma r p)
               (λ x y → isSetPoly _ _ x y)
                 where
                 lemma : ∀ r p → 1r · r + 0r ∷ (1r PolyConst* p) ≡ r ∷ p
                 lemma =
                   λ r p → 1r · r + 0r ∷ (1r PolyConst* p) ≡⟨ cong (_∷ (1r PolyConst* p) )
                                                                   (+Rid (1r · r)) ⟩
                           1r · r ∷ (1r PolyConst* p) ≡⟨ cong (_∷ 1r PolyConst* p) (·Lid r) ⟩
                           r ∷ (1r PolyConst* p) ≡⟨ cong (r ∷_) (PolyConst*Lid p) ⟩
                           r ∷ p ∎

  -- Distribution of indeterminate: (p + q)x = px + qx
  XLDistrPoly+ : ∀ p q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q))
  XLDistrPoly+ =
    ElimProp.f (λ p → ∀ q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q)) )
               (λ q → (cong (0r ∷_) (Poly+Lid q)) ∙
                      cong (0r ∷_) (sym (Poly+Lid q)) ∙
                      sym (cong (_∷ [] Poly+ q) (+Lid 0r)))
               (λ a p prf → ElimProp.f (λ q → 0r ∷ ((a ∷ p) Poly+ q) ≡
                                         ((0r ∷ a ∷ p) Poly+ (0r ∷ q)))
                                       (cong (_∷ a ∷ p ) (sym (+Lid 0r)))
                                       (λ b q prf2 → cong (_∷ a + b ∷ (p Poly+ q)) (sym (+Lid 0r)))
                                       (λ x y i → isSetPoly (x i0) (x i1) x y i))
               (λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- Distribution of a constant ring element over added polynomials p, q: a (p + q) = ap + aq
  PolyConst*LDistrPoly+ : ∀ a p q → a PolyConst* (p Poly+ q) ≡
                                    (a PolyConst* p) Poly+ (a PolyConst* q)
  PolyConst*LDistrPoly+ =
    λ a → ElimProp.f (λ p → ∀ q → a PolyConst* (p Poly+ q) ≡
                                  (a PolyConst* p) Poly+ (a PolyConst* q))
                     (λ q → cong (a PolyConst*_) (Poly+Lid q) ∙
                            (sym (Poly+Lid (a PolyConst* q))))
                     (λ b p prf → ElimProp.f (λ q → (a PolyConst* ((b ∷ p) Poly+ q)) ≡
                                                    (a PolyConst* (b ∷ p)) Poly+ (a PolyConst* q))
                                             refl
                                             (λ c q prf2  → cong (_∷ (a PolyConst* (p Poly+ q)))
                                                                 (·Rdist+ a b c) ∙
                                                            cong (a · b + a · c ∷_) (prf q))
                                             (isSetPoly _ _))
                     (λ x y i q  → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  --Poly* left distributes over Poly+
  Poly*LDistrPoly+ : ∀ p q r → p Poly* (q Poly+ r) ≡ (p Poly* q) Poly+ (p Poly* r)
  Poly*LDistrPoly+ =
    ElimProp.f
      (λ p → ∀ q r → p Poly* (q Poly+ r) ≡ (p Poly* q) Poly+ (p Poly* r))
      (λ _ _ → refl)
      (λ a p prf q r → ((a PolyConst* (q Poly+ r)) Poly+
                        (0r ∷(p Poly*(q Poly+ r)))) ≡⟨
                                                      cong (_Poly+ (0r ∷ (p Poly* (q Poly+ r))))
                                                           (PolyConst*LDistrPoly+ a q r)
                                                     ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ (p Poly* (q Poly+ r)))) ≡⟨
                                        cong (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+_)
                                             (cong (0r ∷_) (prf q r))
                                       ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ ((p Poly* q) Poly+ (p Poly* r)))) ≡⟨
                                                  cong (((a PolyConst* q) Poly+
                                                         (a PolyConst* r)) Poly+_)
                                                  (XLDistrPoly+ (p Poly* q) (p Poly* r))
                                                 ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        ((0r ∷ (p Poly* q)) Poly+ (0r ∷ (p Poly* r)))) ≡⟨
                                                         Poly+Assoc ((a PolyConst* q) Poly+
                                                                      (a PolyConst* r))
                                                                    (0r ∷ (p Poly* q))
                                                                    (0r ∷ (p Poly* r))
                                                        ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ (p Poly* q))) Poly+ (0r ∷ (p Poly* r)) ≡⟨ cong (_Poly+ (0r ∷ (p Poly* r)))
                                                             (sym (Poly+Assoc (a PolyConst* q)
                                                                              (a PolyConst* r)
                                                                              (0r ∷ (p Poly* q))))
                                                    ⟩
      (((a PolyConst* q) Poly+ ((a PolyConst* r) Poly+
        (0r ∷ (p Poly* q)))) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                         cong (_Poly+ (0r ∷ (p Poly* r)))
                                                              (cong ((a PolyConst* q) Poly+_)
                                                                    (Poly+Comm (a PolyConst* r)
                                                                               (0r ∷ (p Poly* q))))
                                                         ⟩
      (((a PolyConst* q) Poly+ ((0r ∷ (p Poly* q)) Poly+
        (a PolyConst* r))) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                       cong (_Poly+ (0r ∷ (p Poly* r)))
                                                            (Poly+Assoc (a PolyConst* q)
                                                                        (0r ∷ (p Poly* q))
                                                                        (a PolyConst* r))
                                                            ⟩
      ((((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) Poly+
        (a PolyConst* r)) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                      sym (Poly+Assoc ((a PolyConst* q) Poly+
                                                                         (0r ∷ (p Poly* q)))
                                                                      ((a PolyConst* r))
                                                                      ((0r ∷ (p Poly* r))))
                                                     ⟩
      ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) Poly+
        ((a PolyConst* r) Poly+ (0r ∷ (p Poly* r))) ∎)
      (λ x y i q r → isSetPoly _ _ (x q r) (y q r) i)

  -- The constant multiplication of a ring element, a, with a polynomial, p, can be
  -- expressed by polynomial multiplication with the singleton polynomial [ a ]
  PolyConst*r=Poly*[r] : ∀ a p → a PolyConst* p ≡ p Poly* [ a ]
  PolyConst*r=Poly*[r] =
    λ a → ElimProp.f (λ p → a PolyConst* p ≡ p Poly* [ a ])
                     refl
                     ( λ r p prf →  a · r ∷ (a PolyConst* p) ≡⟨
                                                              cong (a · r ∷_) prf
                                                             ⟩
                       a · r ∷ (p Poly* [ a ]) ≡⟨
                                                 cong (a · r ∷_)
                                                      (sym (Poly+Lid (p Poly* [ a ])))
                                                ⟩
                       a · r ∷ ([] Poly+ (p Poly* [ a ])) ≡⟨
                                                            cong (_∷ ([] Poly+ (p Poly* [ a ])))
                                                                 (·Comm a r )
                                                           ⟩
                       r · a ∷ ([] Poly+ (p Poly* [ a ])) ≡⟨
                                                            cong (_∷ ([] Poly+ (p Poly* [ a ])))
                                                                 (sym (+Rid (r · a)))
                                                           ⟩
                       r · a + 0r ∷ ([] Poly+ (p Poly* [ a ])) ∎)
                     ( λ x y i → isSetPoly (x i0) (x i1) x y i)

  -- Connection between the constant multiplication and the multiplication in the ring
  PolyConst*Nested· : ∀ a b p → a PolyConst* (b PolyConst* p) ≡ (a · b) PolyConst* p
  PolyConst*Nested· =
    λ a b → ElimProp.f (λ p → a PolyConst* (b PolyConst* p) ≡ (a · b) PolyConst* p)
                       refl
                       (λ c p prf → cong ((a · (b · c)) ∷_) prf ∙
                                    cong (_∷ ((a · b) PolyConst* p)) (·Assoc a b c))
                       (isSetPoly _ _)

  -- We can move the indeterminate from left to outside: px * q = (p * q)x
  0r∷LeftAssoc : ∀ p q → (0r ∷ p) Poly* q ≡ 0r ∷ (p Poly* q)
  0r∷LeftAssoc =
    ElimProp.f (λ p → ∀ q → (0r ∷ p) Poly* q ≡ 0r ∷ (p Poly* q))
               (λ q → cong (_Poly+ [ 0r ])((cong (_Poly+ []) (0rLeftAnnihilatesPoly q))) ∙
                      cong (_∷ []) (+Lid 0r))
               (λ r p b q → cong (_Poly+ (0r ∷ ((r PolyConst* q) Poly+ (0r ∷ (p Poly* q)))))
                                 ((0rLeftAnnihilatesPoly q) ∙ drop0))
               (λ x y i q → isSetPoly _ _ (x q) (y q) i)

  --Associativity of constant multiplication in relation to polynomial multiplication
  PolyConst*AssocPoly* : ∀ a p q → a PolyConst* (p Poly* q) ≡ (a PolyConst* p) Poly* q
  PolyConst*AssocPoly* =
    λ a → ElimProp.f (λ p → ∀ q → a PolyConst* (p Poly* q) ≡ (a PolyConst* p) Poly* q)
                     (λ q → refl)
                     (λ b p prf q → a PolyConst* ((b PolyConst* q) Poly+
                                    (0r ∷ (p Poly* q))) ≡⟨
                                                          PolyConst*LDistrPoly+ a
                                                                                (b PolyConst* q)
                                                                                (0r ∷ (p Poly* q))
                                                         ⟩
                     (a PolyConst* (b PolyConst* q)) Poly+
                      (a PolyConst* (0r ∷ (p Poly* q))) ≡⟨
                                             cong (_Poly+ (a · 0r ∷ (a PolyConst* (p Poly* q))))
                                                  (PolyConst*Nested· a b q)
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (a PolyConst* (0r ∷ (p Poly* q))) ≡⟨
                                                    cong (((a · b) PolyConst* q) Poly+_)
                                                         (cong (a · 0r  ∷_)
                                                               (PolyConst*r=Poly*[r] a
                                                                                (p Poly* q)))
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (a · 0r ∷ ((p Poly* q) Poly* [ a ])) ≡⟨
                                                         cong (((a · b) PolyConst* q) Poly+_)
                                                              (cong (_∷ ((p Poly* q) Poly* [ a ]))
                                                                    (0RightAnnihilates a))  ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ ((p Poly* q) Poly* [ a ])) ≡⟨
                                            cong (((a · b) PolyConst* q) Poly+_)
                                                 (cong (0r ∷_)
                                                       (sym (PolyConst*r=Poly*[r] a (p Poly* q))))
                                                        ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ (a PolyConst* (p Poly* q))) ≡⟨
                                                         cong (((a · b) PolyConst* q) Poly+_)
                                                              (cong (0r ∷_) (prf q))
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ ((a PolyConst* p) Poly* q)) ∎)
                     (λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- We can move the indeterminate from left to outside: p * qx = (p * q)x
  0r∷RightAssoc : ∀ p q → p Poly* (0r ∷  q) ≡ 0r ∷ (p Poly* q)
  0r∷RightAssoc =
    ElimProp.f (λ p → ∀ q → p Poly* (0r ∷  q) ≡ 0r ∷ (p Poly* q))
               (λ q → sym drop0)
               (λ a p prf q → ((a ∷ p) Poly* (0r ∷ q)) ≡⟨
                                                        cong ( a · 0r + 0r ∷_)
                                                             (cong ((a PolyConst* q) Poly+_ )
                                                                   (prf q))
                                                        ⟩
               a · 0r + 0r ∷ ((a PolyConst* q) Poly+
                 (0r ∷ (p Poly* q))) ≡⟨
                                       cong (_∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))))
                                            ((+Rid (a · 0r)))
                                      ⟩
               a · 0r ∷ ((a PolyConst* q) Poly+
                 (0r ∷ (p Poly* q))) ≡⟨
                                      cong (_∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))))
                                           (0RightAnnihilates a) ⟩
               0r ∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) ∎)
               (λ x y i q  → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- We can move the indeterminate around: px * q = p * qx
  0r∷Comm : ∀ p q → (0r ∷ p) Poly* q ≡ p Poly* (0r ∷ q)
  0r∷Comm = ElimProp.f (λ p → ∀ q → (0r ∷ p) Poly* q ≡ p Poly* (0r ∷ q))
                         (λ q → (cong ((0r PolyConst* q) Poly+_) drop0) ∙
                                                0rLeftAnnihilatesPoly q ∙
                                                                 drop0  )
                         (λ a p prf q → ((0r ∷ a ∷ p) Poly* q) ≡⟨ 0r∷LeftAssoc (a ∷ p) q ⟩
                                        0r ∷ ((a ∷ p) Poly* q) ≡⟨ sym (0r∷RightAssoc (a ∷ p) q) ⟩
                                      ((a ∷ p) Poly* (0r ∷ q)) ∎
                       )
                       λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i

  --Poly* is commutative
  Poly*Commutative : ∀ p q → p Poly* q ≡ q Poly* p
  Poly*Commutative =
    ElimProp.f (λ p → ∀ q → p Poly* q ≡ q Poly* p)
               (λ q → sym (0PLeftAnnihilates q))
               (λ a p prf q → (a PolyConst* q) Poly+ (0r ∷ (p Poly* q)) ≡⟨
                                       cong ((a PolyConst* q) Poly+_)
                                            (cong (0r ∷_) (prf q)) ⟩
               ((a PolyConst* q) Poly+ (0r ∷ (q Poly* p))) ≡⟨
                                                            cong ((a PolyConst* q) Poly+_)
                                                            (sym (0r∷LeftAssoc q p))
                                                            ⟩
               ((a PolyConst* q) Poly+ ((0r ∷ q) Poly* p)) ≡⟨
                                      cong (_Poly+ ((0r PolyConst* p) Poly+ (0r ∷ (q Poly* p))))
                                           (PolyConst*r=Poly*[r] a q) ⟩
               ((q Poly* [ a ]) Poly+ ((0r ∷ q) Poly* p)) ≡⟨
                                                           cong ((q Poly* [ a ]) Poly+_)
                                                                (0r∷Comm q p)
                                                           ⟩
               ((q Poly* [ a ]) Poly+ (q Poly* (0r ∷ p))) ≡⟨
                                                           sym (Poly*LDistrPoly+ q [ a ] (0r ∷ p))
                                                           ⟩
               (((q Poly* ([ a ] Poly+ (0r ∷ p))))) ≡⟨
                                                     cong (q Poly*_)
                                                          (Poly+Comm [ a ] (0r ∷ p))
                                                     ⟩
               ((q Poly* ((0r ∷ p) Poly+ [ a ]))) ≡⟨
                                                   refl
                                                   ⟩
               (q Poly* ((0r + a) ∷ p)) ≡⟨ cong (q Poly*_)
                                                (cong (_∷ p) (+Lid a))
                                         ⟩
               (q Poly* (a ∷ p)) ∎)
               (λ x y i q → isSetPoly _ _ (x q ) (y q) i)

  --1P is the right identity of Poly*.
  Poly*Rid : ∀ p → p Poly* 1P ≡ p
  Poly*Rid = λ p → (Poly*Commutative p 1P ∙ Poly*Lid p)

  --Polynomial multiplication right distributes over polynomial addition.
  Poly*RDistrPoly+ : ∀ p q r → (p Poly+ q) Poly* r ≡ (p Poly* r) Poly+ (q Poly* r)
  Poly*RDistrPoly+ = λ p q r → sym (Poly*Commutative r (p Poly+ q)) ∙
                                       Poly*LDistrPoly+ r p q ∙
                                       cong (_Poly+ (r Poly* q)) (Poly*Commutative r p) ∙
                                       cong ((p Poly* r) Poly+_) (Poly*Commutative r q)

  --Polynomial multiplication is associative
  Poly*Associative : ∀ p q r → p Poly* (q Poly* r) ≡  (p Poly* q) Poly* r
  Poly*Associative =
    ElimProp.f (λ p → ∀ q r → p Poly* (q Poly* r) ≡  (p Poly* q) Poly* r )
               (λ _ _ → refl)
               (λ a p prf q r  →
                 ((a ∷ p) Poly* (q Poly* r)) ≡⟨
                                               cong (_Poly+ (0r ∷ (p Poly* (q Poly* r))))
                                                    (PolyConst*AssocPoly* a q r)
                                              ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r ∷ (p Poly* (q Poly* r)))) ≡⟨
                                                 sym (cong (((a PolyConst* q) Poly* r) Poly+_)
                                                           (cong (_∷ (p Poly* (q Poly* r)))
                                                                 (+Lid 0r)))
                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ (p Poly* (q Poly* r)))) ≡⟨
                                                 cong (((a PolyConst* q) Poly* r) Poly+_)
                                                      (cong (0r + 0r ∷_)
                                                            (sym (Poly+Lid (p Poly* (q Poly* r)))))
                                                      ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ ([] Poly+ (p Poly* (q Poly* r))))) ≡⟨
                                                         cong (((a PolyConst* q) Poly* r) Poly+_)
                                                              (cong (0r + 0r ∷_)
                                                                    (cong ([] Poly+_)
                                                                          (prf q r)))
                                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ ([] Poly+ ((p Poly* q) Poly* r)))) ≡⟨
                                                  cong (((a PolyConst* q) Poly* r) Poly+_)
                                                       (cong (_Poly+ (0r ∷ ((p Poly* q) Poly* r)))
                                                             (sym (0rLeftAnnihilatesPoly r)))
                                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  ((0r PolyConst* r) Poly+ (0r ∷ ((p Poly* q) Poly* r)))) ≡⟨
                                                     sym (Poly*RDistrPoly+ (a PolyConst* q)
                                                                           (0r ∷ (p Poly* q)) r)
                                                                           ⟩
                 ((((a ∷ p) Poly* q) Poly* r)) ∎)
               (λ x y i q r  → isSetPoly _ _ (x q r) (y q r) i)

----------------------------------------------------------------------------------------------
-- An instantiation of Polynomials as a commutative ring can be found in CommRing/Instances --
----------------------------------------------------------------------------------------------

max_stars_repo_name: AkermanRydbeck/cubical

max_issues_repo_name: AkermanRydbeck/cubical

max_forks_repo_name: AkermanRydbeck/cubical


text:
------------------------------------------------------------------------
-- Empty type
------------------------------------------------------------------------

module Data.Empty where

data ⊥ : Set where

⊥-elim : {whatever : Set} → ⊥ → whatever
⊥-elim ()

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------------
-- Testing the translation of wild card patterns
------------------------------------------------------------------------------

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

module WildCardPattern where

infix 4 _≡_

postulate
  D    : Set
  zero : D
  succ : D → D

-- The identity type.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- The LTC natural numbers type.
data N : D → Set where
  zN : N zero
  sN : ∀ {n} → N n → N (succ n)

foo : ∀ m n → N m → N n → n ≡ n
foo m n _ _ = prf
  where
  postulate prf : n ≡ n
  {-# ATP prove prf #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Transitivity
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.Symmetry
open import Oscar.Class.Hmap
open import Oscar.Class.Leftunit

module Oscar.Class.Hmap.Transleftidentity where

instance
  Relprop'idFromTransleftidentity : ∀
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    (let _∼_ = Arrow 𝔄 𝔅)
    {ℓ̇} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ̇}
    {transitivity : Transitivity.type _∼_}
    {reflexivity : Reflexivity.type _∼_}
    {ℓ}
    ⦃ _ : Transleftidentity.class _∼_ _∼̇_ reflexivity transitivity ⦄
    ⦃ _ : ∀ {x y} → Symmetry.class (_∼̇_ {x} {y}) ⦄
    → ∀ {m n}
    → Hmap.class (λ (f : m ∼ n) (P : LeftExtensionṖroperty ℓ _∼_ _∼̇_ m) → π₀ (π₀ P) f)
                 (λ f P → π₀ (π₀ P) (transitivity f reflexivity))
  Relprop'idFromTransleftidentity .⋆ _ (_ , P₁) = P₁ $ symmetry transleftidentity


text:
module Subset where

data Subset (A : Set) (P : A -> Set) : Set where
  inn : (a : A) -> .(P a) -> Subset A P

out : forall {A P} -> Subset A P -> A
out (inn a p) = a


text:
module Bool where

import Logic
open Logic

data Bool : Set where
  false : Bool
  true  : Bool

infixr 5 _&&_

_&&_ : Bool -> Bool -> Bool
true  && x = x
false && _ = false

not : Bool -> Bool
not true  = false
not false = true

IsTrue : Bool -> Set
IsTrue true  = True
IsTrue false = False

IsFalse : Bool -> Set
IsFalse x = IsTrue (not x)

module BoolEq where

  _==_ : Bool -> Bool -> Bool
  true  == x = x
  false == x = not x

  subst : {x y : Bool}(P : Bool -> Set) -> IsTrue (x == y) -> P x -> P y
  subst {true}{true}   _ _ px = px
  subst {false}{false} _ _ px = px
  subst {true}{false}  _ () _
  subst {false}{true}  _ () _

  isTrue== : {x : Bool} -> IsTrue x -> IsTrue (x == true)
  isTrue== {true} _ = tt
  isTrue== {false} ()

infix 1 if_then_else_

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

open BoolEq

if'_then_else_ : {A : Set} -> (x : Bool) -> (IsTrue x -> A) -> (IsFalse x -> A) -> A
if' true  then f else g = f tt
if' false then f else  g = g tt

isTrue&&₁ : {x y : Bool} -> IsTrue (x && y) -> IsTrue x
isTrue&&₁ {true} _ = tt
isTrue&&₁ {false} ()

isTrue&&₂ : {x y : Bool} -> IsTrue (x && y) -> IsTrue y
isTrue&&₂ {true} p = p
isTrue&&₂ {false} ()


text:
-- {-# OPTIONS -v tc.term.let.pattern:20 #-}
-- Andreas, 2013-05-06 deep let-bound patterns were translated wrongly
module Issue843 {A B C : Set} (a : A) (b : B) (c : C) where

open import Common.Product
open import Common.Equality

T : Set
T = A × B × C

val : T
val = a , (b , c)

-- This was translated wrongly:
ap : {R : Set} (f : T → R) → R
ap f =
  let x , (y , z) = a , (b , c) -- val
  in f (x , (y , z))

works : {R : Set} (f : T → R) → R
works f =
  let x , yz = val
  in let y , z = yz
  in f (x , (y , z))

ap′ : {R : Set} (f : T → R) → R
ap′ f = f (proj₁ val , (proj₁ (proj₂ val) , proj₂ (proj₂ val)))

test : ∀ {R} (f : T → R) → ap f ≡ f (a , (b , c))
test f = refl

{- WAS:
The type of  test f  reduces to

Goal: f (a , proj₂ a , c) ≡ f (a , b , c)

even though it should reduce to

f (a , b , c) ≡ f (a , b , c)

And indeed, refl doesn't fit there. Typechecking the example where the hole has been replaced with refl produces:

D:\Agda\Strange.agda:21,10-14
proj₂ a != b of type B

when checking that the expression refl has type
ap f ≡ f (a , b , c)

With ap′, the goal reduces correctly and refl is accepted.

I'm using a development version of Agda, about one day old. 64bit Windows 7, if it matters.
-}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda