{-# OPTIONS --without-K #-}
open import Algebra.Bundles
open import Level
open import Data.List
import Data.Nat

module SchlehdorfBasics (A… : CommutativeRing Level.zero Level.zero) where

open CommutativeRing A… renaming (Carrier to A)

open import Relation.Unary hiding (Pred; ∅) public
open import Data.Nat hiding (_+_; _*_)
open import Data.Product hiding (_,_) public
open import Data.Sum using (_⊎_) public
open import Data.List using (List; _∷ʳ_; _++_) public

Pred = λ X → Relation.Unary.Pred {Level.zero} X 0ℓ

⊥ : Set
⊥ = 1# ≈ 0#

∅ : Pred A
∅ _ = ⊥

infix  ¬_
¬_ : Set → Set
¬ X = X → ⊥

data Dec (X : Set) : Set where
  yes : X → Dec X
  no  : (X → ⊥) → Dec X

ExcludedMiddle : Set₁
ExcludedMiddle = (X : Set) → Dec X

data ⟨_⟩ (X : A → Set) : A → Set where
  Base : {x : A} → X x → ⟨ X ⟩ x
  Zero : ⟨ X ⟩ 0#
  Add  : {a b : A} → ⟨ X ⟩ a → ⟨ X ⟩ b → ⟨ X ⟩ (a + b)
  Mult : {r a : A} → ⟨ X ⟩ a → ⟨ X ⟩ (r * a)
  Eq   : {a b : A} → a ≈ b → ⟨ X ⟩ a → ⟨ X ⟩ b

⟨_,_⟩ = λ X a → ⟨ X ∪ ｛ a ｝ ⟩

data ｛_∥_｝ {X : Set} (x : X) (P : Set) : Pred X where
  In : P → ｛ x ∥ P ｝ x
  

data comprehension-syntax {X : Set} (F : Pred X) (P : X → Set) : Pred X where
  In : {x : X} → F x → P x → comprehension-syntax F P x

syntax comprehension-syntax A (λ x → B) = ｛ x ∶ A ∥ B ｝

data _[_]≡_ : List A → Data.Nat.ℕ → A → Set where
  here  : {σ : List A} {a : A} → (a ∷ σ) [  ]≡ a
  there : {n : Data.Nat.ℕ} {σ : List A} {a x : A} → σ [ n ]≡ a → (x ∷ σ) [ Data.Nat.suc n ]≡ a