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 3 ¬_
¬_ : 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  σ) [ 0 ]≡ a
  there : {n : Data.Nat.ℕ} {σ : List A} {a x : A}  σ [ n ]≡ a  (x  σ) [ Data.Nat.suc n ]≡ a