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

open import Library

-- Focusing proofs

-- parametrized by positive and negative atoms
-- module Formulas (PosAt NegAt : Set) where

-- module Formulas (Atoms : Set) where

postulate Atoms : Set

-- Polarity + (positive formulas) are those whose introduction requires

data Pol : Set where
  + - : Pol

-- -- Opposite polarities

-- data Op : (p q : Pol) → Set where
--   +- : Op + -
--   -+ : Op - +

-- Atoms : Pol → Set
-- Atoms + = PosAt
-- Atoms - = NegAt

data Form : Pol → Set where
  -- Atom : ∀{p} → Atoms p → Form p
  True : ∀{p} → Form p
  _∧_  : ∀{p} (A B : Form p) → Form p   -- +: tensor (strict tuple), -: record types (lazy tuple)
  -- only positive
  Atom : (P : Atoms) → Form +
  False : Form +
  _∨_  : (A B : Form +) → Form +
  -- only negative
  _⇒_  : (A : Form +) (B : Form -) → Form -
  -- embedding (switching)
  Comp  : (A : Form +) → Form -   -- The F of CBPV.
  Thunk : (A : Form -) → Form +   -- The U of CBPV.

  -- Sw   : ∀{p q} (op : Op p q) (A : Form p) → Form q

infixl 8 _∧_
infixl 7 _∨_
infixr 6 _⇒_

-- Generic hypotheses, taken from a set S.

module _ (S : Set) where

  data Cxt' : Set where
    ε : Cxt'
    _∙_ : (Γ : Cxt') (A : S) → Cxt'

  data Hyp' (A : S) : (Γ : Cxt') → Set where
    top : ∀{Γ} → Hyp' A (Γ ∙ A)
    pop : ∀{B Γ} (x : Hyp' A Γ) → Hyp' A (Γ ∙ B)

  infixl 4 _∙_

-- Contexts only contain negative formulas.
-- This is because we eagerly split positive ones.
-- In CBPV, hypotheses are positive (values).

Cxt = Cxt' (Form -)
Hyp = Hyp' (Form -)

-- Positive atoms in hypotheses via switching.
Atom-   = λ P → Comp (Atom P)
HypAtom = λ P → Hyp (Atom- P)

-- Non-invertible left rules:

module _ (Nf : (A : Form +) (Γ : Cxt) → Set) where

  data Ne' (C : Form -) (Γ : Cxt) : Set where
    hyp    : ∀    (x : Hyp C Γ) → Ne' C Γ
    impE   : ∀{A} (t : Ne' (A ⇒ C) Γ) (u : Nf A Γ) → Ne' C Γ
    andE₁  : ∀{D} (t : Ne' (C ∧ D) Γ) → Ne' C Γ
    andE₂  : ∀{D} (t : Ne' (D ∧ C) Γ) → Ne' C Γ

-- Invertible left rules:

-- Break up a positive formula and add the bits as hypotheses
-- "case tree" / "cover"

-- Produces a cover of Γ.A by splitting A

mutual

  AddHyp = λ A J Γ → AddHyp' Γ J A

  data AddHyp' (Γ : Cxt) (J : Cxt → Set) : (A : Form +) → Set where

    addAtom : ∀{P} (t : J (Γ ∙ Atom- P)) → AddHyp (Atom P)  J Γ
    addNeg  : ∀{A} (t : J (Γ ∙ A))       → AddHyp (Thunk A) J Γ

    trueE   :        (t : J Γ)                     → AddHyp True    J Γ
    andE    : ∀{A B} (t : AddHyp A (AddHyp B J) Γ) → AddHyp (A ∧ B) J Γ

    falseE  :                                                AddHyp False   J Γ
    orE     : ∀{A B} (t : AddHyp A J Γ) (u : AddHyp B J Γ) → AddHyp (A ∨ B) J Γ

module UNUSED where

  addHyp : ∀ (A : Form +) {Γ} {J : Cxt → Set} (j : ∀{Δ} → J Δ) → AddHyp A J Γ
  addHyp (Atom P)  j = addAtom j
  addHyp (Thunk A) j = addNeg j
  addHyp True      j = trueE j
  addHyp False   _ = falseE
  addHyp (A ∧ B) j = andE (addHyp A (addHyp B j))
  addHyp (A ∨ B) j = orE (addHyp A j) (addHyp B j)

module _ (Ne : (A : Form +) (Γ : Cxt) → Set) where

  data Cover' (i : Size) (J : Cxt → Set) (Γ : Cxt) : Set where
    returnC : (t : J Γ) → Cover' i J Γ
    matchC   : ∀{j : Size< i} {A} (t : Ne A Γ) (c : AddHyp A (Cover' j J) Γ) → Cover' i J Γ

-- Left focusing (break a negative hypothesis A down into something positive)
-- "spine"

mutual

  -- Neutrals, containing values (RFoc) as arguments to functions.

  Ne : (i : Size) (C : Form -) (Γ : Cxt) → Set
  Ne  i = Ne' (RFoc i)

  -- Cover monad, containing neutrals of type (Comp A) as scrutinees.

  Cover : (i j : Size) (J : Cxt → Set) (Γ : Cxt) → Set
  Cover i j = Cover' (λ A → Ne j (Comp A)) i

  -- Non-invertible right rules:

  -- Right focusing (proof of a positive goal by decisions)
  -- "normal" / values.

  data RFoc : (i : Size) (A : Form +) (Γ : Cxt) → Set where
    -- Right focusing stops at a negative formulas
    thunk : ∀{i Γ A} (t : RInv i A Γ) → RFoc (↑ i) (Thunk A) Γ
    -- Success:
    hyp   : ∀{i Γ P} (x : HypAtom P Γ) → RFoc (↑ i) (Atom P) Γ
    trueI : ∀{i Γ} → RFoc (↑ i) True Γ
    -- Choices:
    andI  : ∀{i Γ A B} (t : RFoc i A Γ) (u : RFoc i B Γ) → RFoc (↑ i) (A ∧ B) Γ
    orI₁  : ∀{i Γ B A} (t : RFoc i A Γ) → RFoc (↑ i) (A ∨ B) Γ
    orI₂  : ∀{i Γ A B} (u : RFoc i B Γ) → RFoc (↑ i) (A ∨ B) Γ

  -- Invertible right rules:

  -- Right inversion: break a goal into subgoals
  -- "eta" / definitions by copattern matching.

  data RInv : (i : Size) (A : Form -) (Γ : Cxt) → Set where
    -- Right inversion ends at a positive formula
    ret  : ∀{i Γ A} (t : Cover ∞ i (RFoc i A) Γ) → RInv (↑ i) (Comp A) Γ
    -- Goal splitting
    trueI : ∀{i Γ} → RInv (↑ i) True Γ
    andI  : ∀{i Γ A B} (t : RInv i A Γ) (u : RInv i B Γ) → RInv (↑ i) (A ∧ B) Γ
    impI  : ∀{i Γ A B} (t : AddHyp A (RInv i B) Γ) → RInv (↑ i) (A ⇒ B) Γ

-- Pointwise mapping

_→̇_ : (P Q : Cxt → Set) → Set
P →̇ Q = ∀{Γ} → P Γ → Q Γ

mapAddHyp : ∀{P Q} (f : P →̇ Q) → ∀{A} → AddHyp A P →̇ AddHyp A Q
mapAddHyp f (addAtom t) = addAtom (f t)
mapAddHyp f (addNeg t)  = addNeg (f t)
mapAddHyp f (trueE t)   = trueE (f t)
mapAddHyp f falseE      = falseE
mapAddHyp f (andE t)    = andE (mapAddHyp (mapAddHyp f) t) -- By induction on types!
mapAddHyp f (orE t u)   = orE (mapAddHyp f t) (mapAddHyp f u)

mapCover :  ∀{P Q} (f : P →̇ Q) {i j} → Cover i j P →̇ Cover i j Q
mapCover f (returnC t) = returnC (f t)
mapCover f (matchC t c) = matchC t (mapAddHyp (mapCover f) c)  -- Cover should be sized!

-- Cover monad

joinCover : ∀{i j P} → Cover i j (Cover ∞ j P) →̇ Cover ∞ j P
joinCover (returnC t) = t
joinCover (matchC t c) = matchC t (mapAddHyp joinCover c)

-- Context extension (thinning)

infix 3 _≤_

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤  : ∀{Γ} → Γ ≤ Γ
  weak : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ
  lift : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Γ ∙ A ≤ Δ ∙ A

postulate lift-id≤ : ∀{Γ A} → lift id≤ ≡ id≤ {Γ ∙ A}
{-# REWRITE lift-id≤ #-}

-- Category of thinnings

_•_ : ∀{Γ Δ Φ} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) → Γ ≤ Φ
id≤    • σ      = σ
weak τ • σ      = weak (τ • σ)
lift τ • id≤    = lift τ
lift τ • weak σ = weak (τ • σ)
lift τ • lift σ = lift (τ • σ)

•-id : ∀{Γ Δ} (τ : Γ ≤ Δ) → τ • id≤ ≡ τ
•-id id≤      = refl
•-id (weak τ) = cong weak (•-id τ)
•-id (lift τ) = refl

{-# REWRITE •-id #-}

-- Monotonicity

Mon : (P : Cxt → Set) → Set
Mon P = ∀{Γ Δ} (τ : Γ ≤ Δ) → P Δ → P Γ

-- Monotonicity of hypotheses

monH : ∀{A} → Mon (Hyp A)
monH id≤      x       = x
monH (weak τ) x       = pop (monH τ x)
monH (lift τ) top     = top
monH (lift τ) (pop x) = pop (monH τ x)

monH• : ∀{Γ Δ Φ A} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ) (x : Hyp A Φ) → monH (τ • σ) x ≡ monH τ (monH σ x)
monH• id≤      σ        x       = refl
monH• (weak τ) σ        x       = cong pop (monH• τ σ x)
monH• (lift τ) id≤      x       = refl
monH• (lift τ) (weak σ) x       = cong pop (monH• τ σ x)
monH• (lift τ) (lift σ) top     = refl
monH• (lift τ) (lift σ) (pop x) = cong pop (monH• τ σ x)

{-# REWRITE monH• #-}

-- Monotonicity of neutrals

monNe' : ∀{P : Form + → Cxt → Set}
  (monP : ∀{A} → Mon (P A)) →
  ∀{A} → Mon (Ne' P A)
monNe' monP τ (hyp x)    = hyp (monH τ x)
monNe' monP τ (impE t u) = impE (monNe' monP τ t) (monP τ u)
monNe' monP τ (andE₁ t)  = andE₁ (monNe' monP τ t)
monNe' monP τ (andE₂ t)  = andE₂ (monNe' monP τ t)

-- Monotonicity of covers

monAddHyp : ∀{P} (monP : Mon P) → ∀{A} → Mon (AddHyp A P)
monAddHyp monP τ (addAtom t) = addAtom (monP (lift τ) t)
monAddHyp monP τ (addNeg t)  = addNeg (monP (lift τ) t)
monAddHyp monP τ (trueE t)   = trueE (monP τ t)
monAddHyp monP τ falseE      = falseE
monAddHyp monP τ (andE t)    = andE (monAddHyp (monAddHyp monP) τ t)
monAddHyp monP τ (orE t u)   = orE (monAddHyp monP τ t) (monAddHyp monP τ u)

-- Monotonicity of derivations

mutual
  monNe : ∀{i A} → Mon (Ne i A)
  monNe {i} τ t =  monNe' (monRFoc {i}) τ t

  monCover : ∀{i j P} (monP : Mon P) → Mon (Cover i j P)
  monCover         monP τ (returnC t)      = returnC (monP τ t)
  monCover {i} {j} monP τ (matchC {i'} t c) = matchC (monNe τ t)
    (monAddHyp (monCover {i'} {j} monP) τ c)

  monRFoc : ∀{i A} → Mon (RFoc i A)
  monRFoc τ (thunk t)   = thunk (monRInv τ t)
  monRFoc τ (hyp x)     = hyp   (monH τ x)
  monRFoc τ trueI       = trueI
  monRFoc τ (andI t t₁) = andI (monRFoc τ t) (monRFoc τ t₁)
  monRFoc τ (orI₁ t)    = orI₁ (monRFoc τ t)
  monRFoc τ (orI₂ t)    = orI₂ (monRFoc τ t)

  monRInv : ∀{i A} → Mon (RInv i A)
  monRInv τ (ret {i} t)     = ret (monCover (monRFoc {i}) τ t)
  monRInv τ trueI       = trueI
  monRInv τ (andI t t₁) = andI (monRInv τ t) (monRInv τ t₁)
  monRInv τ (impI {i} t)    = impI (monAddHyp (monRInv {i}) τ t)

KFun : (P Q : Cxt → Set) (Γ : Cxt) → Set
KFun P Q Γ = ∀{Δ} (τ : Δ ≤ Γ) → P Δ → Q Δ

_⇒̂_ : (P Q : Cxt → Set) (Γ : Cxt) → Set
_⇒̂_ P Q Γ = ∀{Δ} (τ : Δ ≤ Γ) → P Δ → Q Δ

mapAddHyp' : ∀{P Q Γ} (f : (P ⇒̂ Q) Γ) → ∀{A} → AddHyp A P Γ → AddHyp A Q Γ
mapAddHyp' f (addAtom t) = addAtom (f (weak id≤) t)
mapAddHyp' f (addNeg t)  = addNeg (f (weak id≤) t)
mapAddHyp' f (trueE t)   = trueE (f id≤ t)
mapAddHyp' f falseE      = falseE
mapAddHyp' f (andE t)    = andE (mapAddHyp' (λ τ → mapAddHyp' λ τ' → f (τ' • τ)) t) -- By induction on types!
mapAddHyp' f (orE t u)   = orE (mapAddHyp' f t) (mapAddHyp' f u)

mapCover' :  ∀{P Q Γ} (f : (P ⇒̂ Q) Γ) {i j} (c : Cover i j P Γ) → Cover i j Q Γ
mapCover' f (returnC t) = returnC (f id≤ t)
mapCover' f (matchC t c) = matchC t (mapAddHyp' (λ τ → mapCover' λ τ' → f (τ' • τ)) c)  -- Cover is sized!

-- Remark: Graded monad (andE)

bindAddHyp : ∀{A B J K} (monJ : Mon J) → AddHyp A J →̇ ((J ⇒̂ AddHyp B K) ⇒̂ AddHyp (A ∧ B) K)
bindAddHyp monJ t τ k = andE (mapAddHyp' k (monAddHyp monJ τ t))

-- Semantics

⟦_⟧ : ∀{p} (A : Form p) (Γ : Cxt) → Set
⟦ Atom P ⟧  Γ = HypAtom P Γ
⟦ False ⟧   Γ = ⊥
⟦ A ∨ B ⟧   Γ = ⟦ A ⟧ Γ ⊎ ⟦ B ⟧ Γ
⟦ True ⟧    Γ = ⊤
⟦ A ∧ B ⟧   Γ = ⟦ A ⟧ Γ × ⟦ B ⟧ Γ
⟦ A ⇒ B ⟧   Γ = ∀ {Δ} (τ : Δ ≤ Γ) (a : ⟦ A ⟧ Δ) → ⟦ B ⟧ Δ

⟦ Comp A ⟧ = Cover ∞ ∞ ⟦ A ⟧  -- values to computations
⟦ Thunk A ⟧ = ⟦ A ⟧

-- Monotonicity of semantics

mon⟦_⟧ : ∀{p} (A : Form p) → Mon ⟦ A ⟧
mon⟦ True    ⟧ τ _       = _
mon⟦ A ∧ B   ⟧ τ (a , b) = mon⟦ A ⟧ τ a , mon⟦ B ⟧ τ b
mon⟦ Atom P  ⟧           = monH
mon⟦ False   ⟧ τ ()
mon⟦ A ∨ B   ⟧ τ         = map-⊎ (mon⟦ A ⟧ τ) (mon⟦ B ⟧ τ)
mon⟦ A ⇒ B   ⟧ τ f δ     = f (δ • τ)
mon⟦ Comp A ⟧           = monCover mon⟦ A ⟧
mon⟦ Thunk A ⟧           = mon⟦ A ⟧

-- Reflection and reification.

mutual

  reify- : ∀ (A : Form -) → ⟦ A ⟧ →̇ RInv ∞ A
  reify- True     _       = trueI
  reify- (A ∧ B)  (a , b) = andI (reify- A a) (reify- B b)
  reify- (A ⇒ B)  f       = impI (reflectHyp A λ τ a → reify- B (f τ a))
  reify- (Comp A) c       = ret (mapCover (reify+ A) c)

  reify+ : ∀ (A : Form +) → ⟦ A ⟧ →̇ RFoc ∞ A
  reify+ True _           = trueI
  reify+ (A ∧ B) (a , b)  = andI (reify+ A a) (reify+ B b)
  reify+ (Atom P) x       = hyp x
  reify+ False ()
  reify+ (A ∨ B) (inj₁ a) = orI₁ (reify+ A a)
  reify+ (A ∨ B) (inj₂ b) = orI₂ (reify+ B b)
  reify+ (Thunk A) a      = thunk (reify- A a)

  reflectHyp : ∀ A {Γ} {J} (k : ∀ {Δ} (τ : Δ ≤ Γ) → ⟦ A ⟧ Δ → J Δ) → AddHyp A J Γ
  reflectHyp True      k = trueE (k id≤ _)
  reflectHyp (A ∧ B)   k = andE (reflectHyp A λ τ a →
                                 reflectHyp B λ τ' b → k (τ' • τ) (mon⟦ A ⟧ τ' a , b))  -- need monT
  reflectHyp (Atom P)  k = addAtom (k (weak id≤) top)
  reflectHyp False     k = falseE
  reflectHyp (A ∨ B)   k = orE (reflectHyp A (λ τ a → k τ (inj₁ a)))
                               (reflectHyp B (λ τ b → k τ (inj₂ b)))
  reflectHyp (Thunk A) k = addNeg (k (weak id≤) (reflect A (hyp top)))

  -- Since we only have negative hypotheses, we only need to reflect these

  reflect : ∀ (A : Form -) → Ne ∞ A →̇ ⟦ A ⟧
  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))  -- need monNe
  reflect (Comp A) t = matchC t (reflectHyp A λ τ a → returnC a)

-- Negative propositions are comonadic

paste : ∀ (A : Form -) → Cover ∞ ∞ ⟦ A ⟧ →̇ ⟦ A ⟧
paste True    _     = _
paste (A ∧ B) c     = paste A (mapCover proj₁ c) , paste B (mapCover proj₂ c)
paste (A ⇒ B) c τ a = paste B (mapCover' (λ τ' f → f id≤ (mon⟦ A ⟧ τ' a)) (monCover mon⟦ A ⇒ B ⟧ τ c))
paste (Comp A)      = joinCover

-- Snippets to define evaluation in polarized lambda calculus

module Evaluation where

  -- Environments

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

  monG⟦_⟧ : (Γ : Cxt) → Mon (G⟦ Γ ⟧)
  monG⟦ ε ⟧ = _
  monG⟦ Γ ∙ P ⟧ τ (γ , a) = monG⟦ Γ ⟧ τ γ , mon⟦ P ⟧ τ a

  Ev : (R : Set) (Δ Γ : Cxt) → Set
  Ev R Δ Γ = G⟦ Γ ⟧ Δ → R

  cut : ∀{R P Δ} → ⟦ P ⟧ Δ → AddHyp P (Ev R Δ) →̇ Ev R Δ
  cut x        (addAtom t) γ = t (γ , returnC x)
  cut a        (addNeg t)  γ = t (γ , a)
  cut _        (trueE t)     = t
  cut (a , b)  (andE t)      = cut a (mapAddHyp (cut b) t)
  cut ()       falseE
  cut (inj₁ a) (orE t u)     = cut a t
  cut (inj₂ b) (orE t u)     = cut b u

-- Intuitionistic propositional logic

data IPL : Set where
  Atom        : (P : Atoms) → IPL
  True False  : IPL
  _∨_ _∧_ _⇒_ : (A B : IPL) → IPL

module CallByName where

  _⁻ : IPL → Form -
  Atom P ⁻  = Atom- P
  True ⁻    = True
  False ⁻   = Comp False
  (A ∨ B) ⁻ = Comp (Thunk (A ⁻) ∨ Thunk (B ⁻))
  (A ∧ B) ⁻ = A ⁻ ∧ B ⁻
  (A ⇒ B) ⁻ = Thunk (A ⁻) ⇒ B ⁻

module CallByValue where

  _⁺ : IPL → Form +
  Atom P ⁺  = Atom P
  True ⁺    = True
  False ⁺   = False
  (A ∨ B) ⁺ = A ⁺ ∨ B ⁺
  (A ∧ B) ⁺ = A ⁺ ∧ B ⁺
  (A ⇒ B) ⁺ = Thunk (A ⁺ ⇒ Comp (B ⁺))

mutual

  _⁺ : IPL → Form +
  Atom P ⁺  = Atom P
  True ⁺    = True
  False ⁺   = False
  (A ∨ B) ⁺ = A ⁺ ∨ B ⁺
  (A ∧ B) ⁺ = A ⁺ ∧ B ⁺
  (A ⇒ B) ⁺ = Thunk (A ⁺ ⇒ B ⁻)

  _⁻ : IPL → Form -
  Atom P ⁻  = Atom- P
  True ⁻    = True
  False ⁻   = Comp False
  (A ∨ B) ⁻ = Comp (A ⁺ ∨ B ⁺)
  (A ∧ B) ⁻ = A ⁻ ∧ B ⁻
  (A ⇒ B) ⁻ = A ⁺ ⇒ B ⁻

-- Derivations

infix 2 _⊢_

data _⊢_ (Γ : Cxt' IPL) : (A : IPL) → Set where
  hyp    : ∀{A} (x : Hyp' IPL A Γ) → Γ ⊢ A
  impI   : ∀{A B} (t : Γ ∙ A ⊢ B) → Γ ⊢ A ⇒ B
  impE   : ∀{A B} (t : Γ ⊢ A ⇒ B) (u : Γ ⊢ A) → Γ ⊢ B
  andI   : ∀{A B} (t : Γ ⊢ A) (u : Γ ⊢ B) → Γ ⊢ A ∧ B
  andE₁  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ A
  andE₂  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ B
  orI₁   : ∀{A B} (t : Γ ⊢ A) → Γ ⊢ A ∨ B
  orI₂   : ∀{A B} (t : Γ ⊢ B) → Γ ⊢ A ∨ B
  orE    : ∀{A B C} (t : Γ ⊢ A ∨ B) (u : Γ ∙ A ⊢ C) (v : Γ ∙ B ⊢ C) → Γ ⊢ C
  falseE : ∀{C} (t : Γ ⊢ False) → Γ ⊢ C
  trueI  : Γ ⊢ True

Tm = λ A Γ → Γ ⊢ A

-- Call-by value evaluation

module CBV where

  V⟦_⟧ = λ A → ⟦ A ⁺ ⟧
  C⟦_⟧ = λ A → ⟦ A ⁻ ⟧

  return : ∀ A → V⟦ A ⟧ →̇ C⟦ A ⟧
  return (Atom P) v = returnC v
  return True v = v
  return False v = returnC v
  return (A ∨ B) v = returnC v
  return (A ∧ B) (a , b) = return A a , return B b
  return (A ⇒ B) v = v

  run : ∀ A → C⟦ A ⟧ →̇ Cover ∞ ∞ V⟦ A ⟧
  run (Atom P) c = c
  run True c = returnC c
  run False c = c
  run (A ∨ B) c = c
  run (A ∧ B) c = joinCover (mapCover' (λ τ a → mapCover' (λ τ' b → (mon⟦ A ⁺ ⟧ τ' a , b)) (run B (mon⟦ B ⁻ ⟧ τ (proj₂ c)))) (run A (proj₁ c)))
  run (A ⇒ B) c = returnC c

  -- Fundamental theorem
  -- Extension of ⟦_⟧ to contexts

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

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

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

  -- Variable case.

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

  impIntro : ∀ {A B Γ} (f : KFun (Cover ∞ ∞ ⟦ A ⟧) ⟦ B ⟧ Γ) → ⟦ A ⇒ B ⟧ Γ
  impIntro f τ a = f τ (returnC a)

  -- impElim : ∀ A B {Γ} → (f : C⟦ A ⇒ B ⟧ Γ) (a : C⟦ A ⟧ Γ) → C⟦ B ⟧ Γ
  -- impElim (Atom P) B f = paste (B ⁻) ∘ mapCover' f
  -- impElim False B f = paste (B ⁻) ∘ mapCover' f
  -- impElim True B f = f id≤
  -- impElim (A ∨ A₁) B f = paste (B ⁻) ∘ mapCover' f
  -- impElim (A ∧ A₁) B f = {!paste (B ⁻) ∘ mapCover' f!}
  -- impElim (A ⇒ A₁) B f = f id≤

  impElim : ∀ A B {Γ} → (f : C⟦ A ⇒ B ⟧ Γ) (a : C⟦ A ⟧ Γ) → C⟦ B ⟧ Γ
  impElim A B f a = paste (B ⁻) (mapCover' f (run A a))

  -- A lemma for the orE case.

  orElim : ∀ A B C {Γ} → C⟦ A ∨ B ⟧ Γ → C⟦ A ⇒ C ⟧ Γ → C⟦ B ⇒ C ⟧ Γ → C⟦ C ⟧ Γ
  orElim A B C c g h = paste (C ⁻) (mapCover' (λ τ → [ g τ , h τ ]) c)

  -- A lemma for the falseE case.

  -- Casts an empty cover into any semantic value (by contradiction).

  falseElim : ∀ C → C⟦ False ⟧ →̇ C⟦ C ⟧
  falseElim C = paste (C ⁻) ∘ mapCover ⊥-elim

  -- The fundamental theorem
  eval :  ∀{A Γ} (t : Γ ⊢ A) → G⟦ Γ ⟧ →̇ C⟦ A ⟧
  eval {A} (hyp x)           = return A ∘ lookup x
  eval (impI t)    γ τ a     = eval t (monG τ γ , a)
  eval (impE {A} {B} t u)  γ = impElim A B (eval t γ) (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) γ    = mapCover inj₁ (run A (eval t γ))
  eval (orI₂ {A} {B} t) γ    = mapCover inj₂ (run B (eval t γ))
  eval (orE {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       γ         = _

  _⁺⁺ : (Γ : Cxt' IPL) → Cxt
  ε ⁺⁺ = ε
  (Γ ∙ A) ⁺⁺ = Γ ⁺⁺ ∙ A ⁻

  -- Identity environment

  ide : ∀ Γ → Cover ∞ ∞ G⟦ Γ ⟧ (Γ ⁺⁺)
  ide ε = returnC _
  ide (Γ ∙ A) = {!!}
    -- monG (weak id≤) (ide Γ) , {! reflectHyp (A ⁺) (λ τ a → a) !}
{-
  -- Normalization

  norm : ∀{A : IPL} {Γ : Cxt' IPL} → Tm A Γ → RInv (Γ ⁺⁺) (A ⁻)
  norm t = reify- _ (eval t (ide _))

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

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
postulate
  X : Set
  T : X → Set
  H : ∀ x → T x → Set

g : ∀ x → T x → Set
g x t = ∀ x → H x t

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Fin where

open import Data.Fin.Core public
  using (Fin; Fin-Number; fsuc; fzero)

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
------------------------------------------------------------------------------
-- Conversion rules for the recursive operator rec
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Rec.ConversionRules where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat.Rec

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

private
  -- We follow the same methodology used in
  -- LTC-PCF.Program.Division.EquationsI (see it for the
  -- documentation).

  ----------------------------------------------------------------------------
  -- The steps

  -- Initially, the conversion rule fix-eq is applied.
  rec-s₁ : D → D → D → D
  rec-s₁ n a f = rech (fix rech) · n · a · f

  -- First argument application.
  rec-s₂ : D → D
  rec-s₂ n = lam (λ a → lam (λ f →
               if (iszero₁ n)
                 then a
                 else f · pred₁ n · (fix rech · pred₁ n · a · f)))

  -- Second argument application.
  rec-s₃ : D → D → D
  rec-s₃ n a = lam (λ f →
                 if (iszero₁ n)
                   then a
                   else f · pred₁ n · (fix rech · pred₁ n · a · f))

  -- Third argument application.
  rec-s₄ : D → D → D → D
  rec-s₄ n a f = if (iszero₁ n)
                   then a
                   else f · pred₁ n · (fix rech · pred₁ n · a · f)

  -- Reduction iszero₁ n ≡ b.
  rec-s₅ : D → D → D → D → D
  rec-s₅ n a f b = if b
                     then a
                     else f · pred₁ n · (fix rech · pred₁ n · a · f)

  -- Reduction of iszero₁ n ≡ true
  --
  -- It should be
  -- rec-s₆ : D → D → D → D
  -- rec-s₆ n a f = a
  --
  -- but we do not give a name to this step.

  -- Reduction iszero₁ n ≡ false.
  rec-s₆ : D → D → D → D
  rec-s₆ n a f = f · pred₁ n · (fix rech · pred₁ n · a · f)

  -- Reduction pred₁ (succ n) ≡ n.
  rec-s₇ : D → D → D → D
  rec-s₇ n a f = f · n · (fix rech · n · a · f)

  ----------------------------------------------------------------------------
  -- The execution steps

  -- We follow the same methodology used in
  -- LTC-PCF.Program.Division.EquationsI (see it for the
  -- documentation).

  -- Application of the conversion rule fix-eq.
  proof₀₋₁ : ∀ n a f → fix rech · n · a · f ≡ rec-s₁ n a f
  proof₀₋₁ n a f = subst (λ x → x · n · a · f ≡ rech (fix rech) · n · a · f )
                         (sym (fix-eq rech))
                         refl

  -- Application of the first argument.
  proof₁₋₂ : ∀ n a f → rec-s₁ n a f ≡ rec-s₂ n · a · f
  proof₁₋₂ n a f = subst (λ x → x · a · f ≡ rec-s₂ n · a · f)
                         (sym (beta rec-s₂ n))
                         refl

  -- Application of the second argument.
  proof₂₋₃ : ∀ n a f → rec-s₂ n · a · f ≡ rec-s₃ n a · f
  proof₂₋₃ n a f = subst (λ x → x · f ≡ rec-s₃ n a · f)
                         (sym (beta (rec-s₃ n) a))
                         refl

  -- Application of the third argument.
  proof₃₋₄ : ∀ n a f → rec-s₃ n a · f ≡ rec-s₄ n a f
  proof₃₋₄ n a f = beta (rec-s₄ n a) f

  -- Cases iszero₁ n ≡ b using that proof.
  -- 25 April 2014. Failed with Andreas' --without-K.
  proof₄₋₅ : ∀ n a f b → iszero₁ n ≡ b → rec-s₄ n a f ≡ rec-s₅ n a f b
  proof₄₋₅ n a f .(iszero₁ n) refl = refl

  -- Reduction of if true ... using the conversion rule if-true.
  proof₅₊ : ∀ n a f → rec-s₅ n a f true ≡ a
  proof₅₊ n a f = if-true a

   -- Reduction of if false ... using the conversion rule if-false.
  proof₅₋₆ : ∀ n a f → rec-s₅ n a f false ≡ rec-s₆ n a f
  proof₅₋₆ n a f = if-false (rec-s₆ n a f)

  -- Reduction pred₁ (succ n) ≡ n using the conversion rule pred₁-S.
  proof₆₋₇ : ∀ n a f → rec-s₆ (succ₁ n) a f ≡ rec-s₇ n a f
  proof₆₋₇ n a f = subst (λ x → rec-s₇ x a f ≡ rec-s₇ n a f)
                         (sym (pred-S n))
                         refl

------------------------------------------------------------------------------
-- The conversion rules for rec.

rec-0 : ∀ a {f} → rec zero a f ≡ a
rec-0 a {f} =
  fix rech · zero · a · f  ≡⟨ proof₀₋₁ zero a f ⟩
  rec-s₁ zero a f          ≡⟨ proof₁₋₂ zero a f ⟩
  rec-s₂ zero · a · f      ≡⟨ proof₂₋₃ zero a f ⟩
  rec-s₃ zero a · f        ≡⟨ proof₃₋₄ zero a f ⟩
  rec-s₄ zero a f          ≡⟨ proof₄₋₅ zero a f true iszero-0 ⟩
  rec-s₅ zero a f true     ≡⟨ proof₅₊ zero a f ⟩
  a                        ∎

rec-S : ∀ n a f → rec (succ₁ n) a f ≡ f · n · (rec n a f)
rec-S n a f =
  fix rech · (succ₁ n) · a · f  ≡⟨ proof₀₋₁ (succ₁ n) a f ⟩
  rec-s₁ (succ₁ n) a f          ≡⟨ proof₁₋₂ (succ₁ n) a f ⟩
  rec-s₂ (succ₁ n) · a · f      ≡⟨ proof₂₋₃ (succ₁ n) a f ⟩
  rec-s₃ (succ₁ n) a · f        ≡⟨ proof₃₋₄ (succ₁ n) a f ⟩
  rec-s₄ (succ₁ n) a f          ≡⟨ proof₄₋₅ (succ₁ n) a f false (iszero-S n) ⟩
  rec-s₅ (succ₁ n) a f false    ≡⟨ proof₅₋₆ (succ₁ n) a f ⟩
  rec-s₆ (succ₁ n) a f          ≡⟨ proof₆₋₇ n a f ⟩
  rec-s₇ n a f                  ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Functional semantics for an untyped λ-calculus with constants
------------------------------------------------------------------------

{-# OPTIONS --no-termination-check #-}

module Lambda.Closure.Functional.No-workarounds where

open import Category.Monad
open import Category.Monad.Partiality as Partiality
  using (_⊥; never; OtherKind; other; steps)
open import Codata.Musical.Notation
open import Data.Empty using (⊥-elim)
open import Data.List hiding (lookup)
open import Data.Maybe hiding (_>>=_)
import Data.Maybe.Categorical as Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Function
import Level
open import Relation.Binary using (module Preorder)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Negation

open Partiality._⊥
private
  open module E {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module R {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})

open import Lambda.Syntax
open Closure Tm
open import Lambda.VirtualMachine
open Functional
private
  module VM = Closure Code

------------------------------------------------------------------------
-- A monad with partiality and failure

PF : RawMonad {f = Level.zero} (_⊥ ∘ Maybe)
PF = Maybe.monadT Partiality.monad

module PF where
  open RawMonad PF public

  fail : {A : Set} → Maybe A ⊥
  fail = now nothing

  _>>=-cong_ :
    ∀ {k} {A B : Set} {x₁ x₂ : Maybe A ⊥} {f₁ f₂ : A → Maybe B ⊥} →
    Rel k x₁ x₂ → (∀ x → Rel k (f₁ x) (f₂ x)) →
    Rel k (x₁ >>= f₁) (x₂ >>= f₂)
  _>>=-cong_ {k} {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
    Partiality._>>=-cong_ x₁≈x₂ helper
    where
    helper : ∀ {x y} → x ≡ y →
             Rel k (maybe f₁ fail x) (maybe f₂ fail y)
    helper {x = nothing} P.refl = fail ∎
    helper {x = just x}  P.refl = f₁≈f₂ x

  associative :
    {A B C : Set}
    (x : Maybe A ⊥) (f : A → Maybe B ⊥) (g : B → Maybe C ⊥) →
    (x >>= f >>= g) ≅ (x >>= λ y → f y >>= g)
  associative x f g =
    (x >>= f >>= g)                      ≅⟨ Partiality.associative P.refl x _ _ ⟩
    (x >>=′ λ y → maybe f fail y >>= g)  ≅⟨ Partiality._>>=-cong_ (x ∎) helper ⟩
    (x >>= λ y → f y >>= g)              ∎
    where
    open RawMonad Partiality.monad renaming (_>>=_ to _>>=′_)

    helper : ∀ {y₁ y₂} → y₁ ≡ y₂ →
             (maybe f fail y₁ >>= g) ≅ maybe (λ z → f z >>= g) fail y₂
    helper {y₁ = nothing} P.refl = fail ∎
    helper {y₁ = just y}  P.refl = (f y >>= g) ∎

  >>=-inversion-⇓ :
    ∀ {k} {A B : Set} x {f : A → Maybe B ⊥} {y} →
    (x>>=f⇓ : (x >>= f) ⇓[ k ] just y) →
    ∃ λ z → ∃₂ λ (x⇓ : x ⇓[ k ] just z)
                 (fz⇓ : f z ⇓[ k ] just y) →
                 steps x⇓ + steps fz⇓ ≡ steps x>>=f⇓
  >>=-inversion-⇓ x {f} x>>=f⇓
    with Partiality.>>=-inversion-⇓ {_∼A_ = _≡_} P.refl x x>>=f⇓
  ... | (nothing , x↯ , now ()  , _)
  ... | (just z  , x⇓ , fz⇓     , eq) = (z , x⇓ , fz⇓ , eq)

  >>=-inversion-⇑ :
    ∀ {k} {A B : Set} x {f : A → Maybe B ⊥} →
    (x >>= f) ⇑[ other k ] →
    ¬ ¬ (x ⇑[ other k ] ⊎
         ∃ λ y → x ⇓[ other k ] just y × f y ⇑[ other k ])
  >>=-inversion-⇑ {k} x {f} x>>=f⇑ =
    helper ⟨$⟩ Partiality.>>=-inversion-⇑ P.isEquivalence x x>>=f⇑
    where
    open RawMonad ¬¬-Monad renaming (_<$>_ to _⟨$⟩_)

    helper : (_ ⊎ ∃ λ (y : Maybe _) → _) → _
    helper (inj₁ x⇑                      ) = inj₁ x⇑
    helper (inj₂ (just y  , x⇓,fy⇑)      ) = inj₂ (y , x⇓,fy⇑)
    helper (inj₂ (nothing , x↯,now∼never)) =
      ⊥-elim (Partiality.now≉never (proj₂ x↯,now∼never))

open PF

------------------------------------------------------------------------
-- Semantics

infix 5 _∙_

-- Note that this definition gives us determinism "for free".

mutual

  ⟦_⟧ : ∀ {n} → Tm n → Env n → Maybe Value ⊥
  ⟦ con i ⟧   ρ = return (con i)
  ⟦ var x ⟧   ρ = return (lookup ρ x)
  ⟦ ƛ t ⟧     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ >>= λ v₁ →
                  ⟦ t₂ ⟧ ρ >>= λ v₂ →
                  v₁ ∙ v₂

  _∙_ : Value → Value → Maybe Value ⊥
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = later (♯ (⟦ t₁ ⟧ (v₂ ∷ ρ)))

------------------------------------------------------------------------
-- Example

Ω-loops : ⟦ Ω ⟧ [] ≈ never
Ω-loops = later (♯ Ω-loops)

------------------------------------------------------------------------
-- Some lemmas

-- An abbreviation.

infix 5 _⟦·⟧_

_⟦·⟧_ : Maybe Value ⊥ → Maybe Value ⊥ → Maybe Value ⊥
v₁ ⟦·⟧ v₂ = v₁ >>= λ v₁ → v₂ >>= λ v₂ → v₁ ∙ v₂

-- _⟦·⟧_ preserves equality.

_⟦·⟧-cong_ : ∀ {k v₁₁ v₁₂ v₂₁ v₂₂} →
             Rel k v₁₁ v₂₁ → Rel k v₁₂ v₂₂ →
             Rel k (v₁₁ ⟦·⟧ v₁₂) (v₂₁ ⟦·⟧ v₂₂)
v₁₁≈v₂₁ ⟦·⟧-cong v₁₂≈v₂₂ =
  v₁₁≈v₂₁ >>=-cong λ v₁ →
  v₁₂≈v₂₂ >>=-cong λ v₂ →
  v₁ ∙ v₂ ∎

-- The semantics of application is compositional (with respect to the
-- syntactic equality which is used).

·-comp : ∀ {n} (t₁ t₂ : Tm n) {ρ} →
         ⟦ t₁ · t₂ ⟧ ρ ≅ ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ
·-comp t₁ t₂ = _ ∎

------------------------------------------------------------------------
-- Compiler correctness

module Correctness where

  -- The relation _≈_ does not admit unrestricted use of transitivity
  -- in corecursive proofs, so I have formulated the correctness proof
  -- using a continuation. Note that the proof would perhaps be easier
  -- if the semantics was also formulated in continuation-passing
  -- style.

  mutual

    correct :
      ∀ {n} t {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈ k v) →
      exec ⟨ comp t c , s , comp-env ρ ⟩ ≈ (⟦ t ⟧ ρ >>= k)
    correct (con i) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (Lambda.Syntax.Closure.con i) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (con i) ⟩
      k (con i)                                                    ∎)
    correct (var x) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩  ≡⟨ P.cong (λ v → exec ⟨ c , val v ∷ s , comp-env ρ ⟩) (lookup-hom x ρ) ⟩
      exec ⟨ c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (lookup ρ x) ⟩
      k (lookup ρ x)                                             ∎)
    correct (ƛ t) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (ƛ t ρ) ⟩
      k (ƛ t ρ)                                             ∎)
    correct (t₁ · t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩      ≈⟨ correct t₁ (λ v₁ → correct t₂ (λ v₂ → ∙-correct v₁ v₂ hyp)) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ →  ⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂  >>= k)  ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ → sym $ associative (⟦ t₂ ⟧ ρ) _ _) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → v₁ ∙ v₂) >>= k)  ≅⟨ sym $ associative (⟦ t₁ ⟧ ρ) _ _ ⟩
      (⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ >>= k)                              ≅⟨ _ ∎ ⟩
      (⟦ t₁ · t₂ ⟧ ρ >>= k)                                      ∎

    ∙-correct :
      ∀ {n} v₁ v₂ {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈ k v) →
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , comp-env ρ ⟩ ≈
      (v₁ ∙ v₂ >>= k)
    ∙-correct (con i)   v₂                 _   = fail ∎
    ∙-correct (ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val (ƛ t₁ ρ₁)) ∷ s , comp-env ρ ⟩  ≈⟨ later (♯ (

        exec ⟨ comp t₁ [ ret ] , ret c (comp-env ρ) ∷ s , comp-env (v₂ ∷ ρ₁) ⟩               ≈⟨ correct t₁ (λ v → laterˡ (hyp v)) ⟩
        (⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k)                                                             ∎)) ⟩

      (ƛ t₁ ρ₁ ∙ v₂ >>= k)                                                              ∎

-- Note that the equality that is used here is syntactic.

correct : ∀ t →
          exec ⟨ comp t [] , [] , [] ⟩ ≈
          (⟦ t ⟧ [] >>= λ v → PF.return (comp-val v))
correct t = Correctness.correct t (λ v → return (comp-val v) ∎)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

postulate
  A : Set
  R : A → Set
  M : (a : A) (s t : R a) → Set

variable
  a : A
  s : R a

t : _

postulate
  m : M _ s t

t = _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import LogicalFormulae
open import Groups.Abelian.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Rings.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.EuclideanAlgorithm
open import Numbers.Primes.PrimeNumbers

module Rings.Characteristic {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) where

open import Rings.InitialRing R
open Ring R
open Setoid S
open Equivalence eq
open Group additiveGroup

characteristicWellDefined : (0R ∼ 1R → False) → {n m : ℕ} → Prime n → Prime m → fromN n ∼ 0R → fromN m ∼ 0R → n ≡ m
characteristicWellDefined 0!=1 {n} {m} pN pM n=0 m=0 with divisionDecidable m n
... | inl n|m = equalityCommutative (primeDivPrimeImpliesEqual pM pN n|m)
... | inr notDiv with hcfPrimeIsOne {m} {n} pM notDiv
... | bl = exFalso (0!=1 v)
  where
    t : (n *N extendedHcf.extended1 (euclid n m) ≡ m *N extendedHcf.extended2 (euclid n m) +N extendedHcf.c (euclid n m)) || (n *N extendedHcf.extended1 (euclid n m) +N extendedHcf.c (euclid n m) ≡ m *N extendedHcf.extended2 (euclid n m))
    t = extendedHcf.extendedProof (euclid n m)
    u : (n *N extendedHcf.extended1 (euclid n m) ≡ m *N extendedHcf.extended2 (euclid n m) +N 1) || (n *N extendedHcf.extended1 (euclid n m) +N 1 ≡ m *N extendedHcf.extended2 (euclid n m))
    u with t
    ... | inl x = inl (transitivity x (applyEquality (λ i → m *N extendedHcf.extended2 (euclid n m) +N i) bl))
    ... | inr x = inr (transitivity (applyEquality (n *N extendedHcf.extended1 (euclid n m) +N_) (equalityCommutative bl)) x)
    v : 0R ∼ 1R
    v with u
    ... | inr x = symmetric (transitive (symmetric (transitive (fromNPreserves+ (n *N extendedHcf.extended1 (euclid n m)) 1) (transitive (+WellDefined (transitive (fromNPreserves* n (extendedHcf.extended1 (euclid n m))) (transitive (*WellDefined n=0 reflexive) timesZero')) identRight) identLeft))) (transitive (fromNWellDefined x) (transitive (fromNPreserves* m (extendedHcf.extended2 (euclid n m))) (transitive (*WellDefined m=0 reflexive) timesZero'))))
    ... | inl x = transitive (transitive (transitive (symmetric timesZero') (transitive (*WellDefined (symmetric n=0) reflexive) (transitive (symmetric (fromNPreserves* n (extendedHcf.extended1 (euclid n m)))) (transitive (fromNWellDefined x) (transitive (fromNPreserves+ (m *N extendedHcf.extended2 (euclid n m)) 1) (+WellDefined (fromNPreserves* m (extendedHcf.extended2 (euclid n m))) reflexive)))))) (+WellDefined (transitive (*WellDefined m=0 reflexive) timesZero') (identRight))) identLeft


text:
module TelescopingLet5 where

postulate
  A : Set
  a : A

module B (a : A) where
   postulate
     C : Set
-- B.C : (a : A) → Set

module N = B a
module M' (open N) (c : C) where
  postulate cc : C
-- M.cc : (a : B.A a) → B.A a

E = let open B a in C

module M (open B a) (x : A) where
  D = C
  postulate cc : C
-- M.cc : (a : B.A a) → B.A a

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --termination-depth=2 #-}

module TerminationWithTwoConstructors where

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

f : Nat -> Nat
f zero = zero
f (suc zero) = zero
f (suc (suc n)) with zero
... | m = f (suc n)

{- internal represenation

f : Nat -> Nat
f zero = zero
f (suc zero) = zero
f (suc (suc n)) = faux n zero

faux : Nat -> Nat -> Nat
faux n m = f (suc n)

-}

{- this type checks with --termination-depth >= 2
calls:

 f -> f_with (-2)
 f_with -> f (+1)

-}

max_stars_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------------
-- Testing the erasing of proof terms
------------------------------------------------------------------------------

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

module ProofTerm4 where

postulate
  D   : Set
  _≡_ : D → D → Set
  A   : D → D → D → D → Set

-- We can erase proof terms of type D → ⋯ → D → Set.
foo : ∀ x₁ x₂ x₃ x₄ → A x₁ x₂ x₃ x₄ → x₁ ≡ x₁
foo x₁ x₂ x₃ x₄ h = bar x₁
  where
  -- Since @bar@ is insidere a where clause, we erase the proof
  -- term @h@.
  postulate bar : ∀ x → x ≡ x
  {-# ATP prove bar #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Andreas, 2016-08-04, issue #964
-- Allow open metas and interaction points in imported files

-- {-# OPTIONS -v import:100 #-}
-- {-# OPTIONS -v meta.postulate:20 #-}
-- {-# OPTIONS -v tc.conv.level:50 #-}

open import Common.Level
open import Common.Equality

postulate something : Set₁

open import Common.Issue964.UnsolvedMetas something

test1 : Level
test1 = meta

test2 : (B : Set) → Set test1
test2 B = M.meta2 B

test3 = M.N.meta3

-- Should succeed


text:
module Sets.PredicateSet.Relations{ℓₗ}{ℓₒ} where

import      Lvl
open import Functional
open import Logic.Propositional{ℓₗ Lvl.⊔ ℓₒ}
open import Logic.Predicate{ℓₗ}{ℓₒ}
open import Numeral.Finite
open import Numeral.Natural
import      Relator.Equals
open import Sets.PredicateSet
open import Structure.Function.Domain

Empty : ∀{T} → PredSet{ℓₗ}{ℓₒ}(T) → Stmt
Empty(S) = (∀{x} → (x ∉' S)) where
  _∉'_ = _∉_ {ℓₗ}{ℓₒ}

NonEmpty : ∀{T} → PredSet{ℓₗ}{ℓₒ}(T) → Stmt
NonEmpty(S) = ∃(x ↦ (x ∈' S)) where
  _∈'_ = _∈_ {ℓₗ}{ℓₒ}

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:
{-# OPTIONS --safe #-}

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.IdPi {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Irrelevance as S
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Sigma
open import Definition.LogicalRelation.Substitution.Introductions.Fst
open import Definition.LogicalRelation.Substitution.Introductions.Snd
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.Lambda
open import Definition.LogicalRelation.Substitution.Introductions.Application
open import Definition.LogicalRelation.Substitution.Introductions.Cast
open import Definition.LogicalRelation.Substitution.Introductions.Id
open import Definition.LogicalRelation.Substitution.Introductions.IdUPiPi
open import Definition.LogicalRelation.Substitution.Introductions.Transp
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst
open import Definition.LogicalRelation.Substitution.MaybeEmbed
open import Definition.LogicalRelation.Substitution.Introductions.Universe
open import Definition.LogicalRelation.Substitution.Reduction
open import Definition.LogicalRelation.Substitution.Weakening
open import Definition.LogicalRelation.Substitution.Conversion
open import Definition.LogicalRelation.Substitution.ProofIrrelevance
open import Definition.LogicalRelation.Fundamental.Variable

open import Tools.Product
import Tools.PropositionalEquality as PE

abstract
  Id-Πᵗᵛ : ∀ {A B rA lA lB l Γ t u} ([Γ] : ⊩ᵛ Γ)
           → lA ≤ l
           → lB ≤ l →
             let [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ (proj₂ (levelBounded lA)) [Γ])
             in
             ([A] : Γ ⊩ᵛ⟨ ∞ ⟩ A ^ [ rA , ι lA ] / [Γ])
             ([UB] : Γ ∙ A ^ [ rA , ι lA ] ⊩ᵛ⟨ ∞ ⟩ Univ ! lB ^ [ ! , next lB ] / [Γ] ∙ [A])
             ([A]ₜ : Γ ⊩ᵛ⟨ ∞ ⟩ A ∷ Univ rA lA ^ [ ! , next lA ] / [Γ] / [UA])
             ([B]ₜ : Γ ∙ A ^ [ rA , ι lA ] ⊩ᵛ⟨ ∞ ⟩ B ∷ Univ ! lB ^ [ ! , next lB ] / [Γ] ∙ [A] / (λ {Δ} {σ} → [UB] {Δ} {σ}))
             ([ΠAB] : Γ ⊩ᵛ⟨ ∞ ⟩ Π A ^ rA ° lA ▹ B ° lB ° l ^ [ ! , ι l ] / [Γ])
             ([t]ₜ : Γ ⊩ᵛ⟨ ∞ ⟩ t ∷ Π A ^ rA ° lA ▹ B ° lB ° l ^ [ ! , ι l ] / [Γ] / [ΠAB]) →
             ([u]ₜ : Γ ⊩ᵛ⟨ ∞ ⟩ u ∷ Π A ^ rA ° lA ▹ B ° lB ° l ^ [ ! , ι l ] / [Γ] / [ΠAB]) →
             [ Γ ⊩ᵛ⟨ ∞ ⟩ Id (Π A ^ rA ° lA ▹ B ° lB ° l) t u ≡ Π A ^ rA ° lA ▹ (Id B ((wk1 t) ∘ (var 0) ^ l) ((wk1 u) ∘ (var 0) ^ l)) ° lB ° l ∷ SProp l ^ [ ! , next l ]  / [Γ] ]

  Id-Πᵗᵛ {A} {B} {rA} {lA} {lB} {l} {Γ} {t} {u} [Γ] lA≤ lB≤
            [A] [UB] [A]ₜ [B]ₜ [ΠAB] [t]ₜ [u]ₜ =
    let [SProp] = maybeEmbᵛ {A = Univ _ _} [Γ] (Uᵛ {rU = %} (proj₂ (levelBounded l)) [Γ])
        [UA] = maybeEmbᵛ {A = Univ rA _} [Γ] (Uᵛ (proj₂ (levelBounded lA)) [Γ])
        [ΓA] = _∙_ {A = A} [Γ] [A]
        ⊢AₜΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UA] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([A]ₜ ⊢Δ [σ]))
        [B] = maybeEmbᵛ {A = B} [ΓA] (univᵛ {A = B} [ΓA] (≡is≤ PE.refl) (λ {Δ} {σ} → [UB] {Δ} {σ}) [B]ₜ)
        ⊢BΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([UB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([B]ₜ ⊢Δ [σ]))
        ⊢tΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([ΠAB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([t]ₜ ⊢Δ [σ]))
        ⊢uΔ = λ {Δ} {σ} ⊢Δ [σ] → escapeTerm (proj₁ ([ΠAB] {Δ} {σ} ⊢Δ [σ])) (proj₁ ([u]ₜ ⊢Δ [σ]))
        Id-Π-res = λ A B → Π A ^ rA ° lA ▹ (Id B ((wk1 t) ∘ (var 0) ^ l ) ((wk1 u) ∘ (var 0) ^ l)) ° lB ° l
        [liftσ] = λ {Δ} {σ} ⊢Δ [σ] → liftSubstS {F = A} {σ = σ} {Δ  = Δ} [Γ] ⊢Δ [A] [σ]
        ⊢AΔ = λ {Δ} {σ} ⊢Δ [σ] → escape (proj₁ ([A] {Δ  = Δ} {σ = σ} ⊢Δ [σ]))
        [SPropB] = maybeEmbᵛ {A = SProp lB} [ΓA] (λ {Δ} {σ} → Uᵛ <next [ΓA] {Δ} {σ})
        [wA] = wk1ᵛ {A = A} {F = A} [Γ] [A] [A]
        [wΠ] = wk1ᵛ {A =  Π A ^ rA ° lA ▹ B ° lB ° l} {F = A} [Γ] [A] [ΠAB]
        [wt] = wk1Termᵛ {F = A} {G = Π A ^ rA ° lA ▹ B ° lB ° l} {t = t} [Γ] [A] [ΠAB] [t]ₜ
        [wu] = wk1Termᵛ {F = A} {G = Π A ^ rA ° lA ▹ B ° lB ° l} {t = u} [Γ] [A] [ΠAB] [u]ₜ
        [Id-Π] : Γ ⊩ᵛ Id (Π A ^ rA ° lA ▹ B ° lB ° l) t u ⇒ Id-Π-res A B ∷ SProp l ^ next l / [Γ]
        [Id-Π] = λ {Δ} {σ} ⊢Δ [σ] →
                   PE.subst (λ ret → Δ ⊢ Id (Π (subst σ A) ^ rA ° lA ▹ (subst (liftSubst σ) B) ° lB ° l) (subst σ t) (subst σ u) ⇒ Π subst σ A ^ rA ° lA ▹ ret ° lB ° l ∷ SProp l ^ next l)
                            (PE.cong₂ (λ a b → Id (subst (liftSubst σ) B) (a ∘ (var 0) ^ l) (b ∘ (var 0) ^ l)) (PE.sym (Idsym-subst-lemma σ t)) (PE.sym (Idsym-subst-lemma σ u)))
                            (Id-Π {A = subst σ A} {rA} {lA} {lB} {l} {subst (liftSubst σ) B} {subst σ t} {subst σ u} lA≤ lB≤
                                  (⊢AₜΔ {Δ} {σ} ⊢Δ [σ]) (⊢BΔ (⊢Δ ∙ ⊢AΔ {Δ} {σ} ⊢Δ [σ]) ([liftσ] {Δ} {σ} ⊢Δ [σ])) (⊢tΔ {Δ} {σ} ⊢Δ [σ]) (⊢uΔ {Δ} {σ} ⊢Δ [σ]))
        [UB'] = maybeEmbᵛ {l = next lB} {A = U _} [ΓA] (λ {Δ} {σ} → Uᵛ <next [ΓA] {Δ} {σ})
        [Id-Π-res] : Γ ⊩ᵛ⟨ ∞ ⟩ Id-Π-res A B ∷ SProp l ^ [ ! , next l ] / [Γ] / [SProp]
        [Id-Π-res] = Πᵗᵛ {F = A} {G = Id B ((wk1 t) ∘ (var 0) ^ l) ((wk1 u) ∘ (var 0) ^ l)} lA≤ lB≤ [Γ] [A] (λ {Δ} {σ} → [SPropB] {Δ} {σ}) [A]ₜ
                         (Idᵗᵛ {A = B} {t = (wk1 t) ∘ (var 0) ^ l} {u = (wk1 u) ∘ (var 0) ^ l} [ΓA] [B]
                            (S.irrelevanceTerm′ {A = (wk1d B) [ var 0 ]} {A′ = B} {t = (wk1 t) ∘ (var 0) ^ l}
                                                (wkSingleSubstId B) PE.refl [ΓA] [ΓA]
                                                (substSΠ {wk1 A} {wk1d B} {var 0} [ΓA] [wA] [wΠ] (proj₂ (fundamentalVar here [ΓA]))) [B]
                                                (appᵛ {F = wk1 A} {G = wk1d B} {t = wk1 t} {u = var 0} [ΓA] [wA] [wΠ] [wt] (proj₂ (fundamentalVar here [ΓA]))))
                            (S.irrelevanceTerm′ {A = (wk1d B) [ var 0 ]} {A′ = B} {t = (wk1 u) ∘ (var 0) ^ l}
                                                (wkSingleSubstId B) PE.refl [ΓA] [ΓA]
                                                (substSΠ {wk1 A} {wk1d B} {var 0} [ΓA] [wA] [wΠ] (proj₂ (fundamentalVar here [ΓA]))) [B]
                                                (appᵛ {F = wk1 A} {G = wk1d B} {t = wk1 u} {u = var 0} [ΓA] [wA] [wΠ] [wu] (proj₂ (fundamentalVar here [ΓA]))))
                            (S.irrelevanceTerm {A = Univ _ _} {t = B} [ΓA] [ΓA] (λ {Δ} {σ} → [UB] {Δ} {σ}) (λ {Δ} {σ} → [UB'] {Δ} {σ}) [B]ₜ))
        [id] , [eq] = redSubstTermᵛ {SProp l} {Id (Π A ^ rA ° lA ▹ B ° lB ° l) t u} {Id-Π-res A B}
                                    [Γ] (λ {Δ} {σ} ⊢Δ [σ] → [Id-Π] {Δ} {σ} ⊢Δ [σ])
                                    [SProp] [Id-Π-res]
    in modelsTermEq [SProp] [id] [Id-Π-res] [eq]

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
open import MJ.Types
import MJ.Classtable.Core as Core
import MJ.Classtable.Code as Code

import MJ.Syntax as Syntax
import MJ.Semantics.Values as Values

module MJ.Semantics {c}(Ct : Core.Classtable c)(ℂ : Code.Code Ct) where

-- functional big-step definitional interpreter
-- open import MJ.Semantics.Functional Σ ℂ
open import MJ.Semantics.Monadic Ct ℂ public


text:
open import Data.Product using ( _,_ )
open import Relation.Nullary using ( yes ; no )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox.Interp using
  ( Interp ; _,_ ; ⌊_⌋ ; ind ; ind² ; Surjective ; surj ; ind⁻¹ ; surj✓ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _≲_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind ; _≋_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( interp ; _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans ; con ; rol ; con-≈ ; rol-≈ )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( morph ; ≲-image ; ≲-resp-≈ ; ≲-resp-con ; ≲-resp-rol )
open import Web.Semantic.Util using ( _∘_ ; ExclMiddle₁ ; ExclMiddle ; smaller-excl-middle ; id ; □ ; is ; is! ; is✓ )

-- Note that this construction uses excluded middle
-- (for cardinality reasons, to embed a large set in a small set).

module Web.Semantic.DL.ABox.Interp.Meet ( excl-middle₁ : ExclMiddle₁ ) { Σ : Signature } { X : Set } where

-- This constructs the meet of a set of interpretations,
-- which is the greatest lower bound on surjective interpretations

meet : (Interp Σ X → Set) → Interp Σ X
meet Is =
  ( interp X
    (λ x y → □ (is (excl-middle₁ (∀ I → (I ∈ Is) →
      (⌊ I ⌋ ⊨ ind I x ≈ ind I y)))))
    (λ {x} → is! (λ I I∈Is →
      ≈-refl ⌊ I ⌋))
    (λ {x} {y} x≈y → is! (λ I I∈Is →
      ≈-sym ⌊ I ⌋ (is✓ x≈y I I∈Is)))
    (λ {x} {y} {z} x≈y y≈z → is! (λ I I∈Is →
      ≈-trans ⌊ I ⌋ (is✓ x≈y I I∈Is) (is✓ y≈z I I∈Is)))
    (λ c x → □ (is (excl-middle₁ (∀ I → (I ∈ Is) →
      (ind I x ∈ con ⌊ I ⌋ c)))))
    (λ r xy → □ (is (excl-middle₁ (∀ I → (I ∈ Is) →
      ind² I xy ∈ rol ⌊ I ⌋ r))))
    (λ {x} {y} c x∈c x≈y → is! (λ I I∈Is →
      con-≈ ⌊ I ⌋ c (is✓ x∈c I I∈Is) (is✓ x≈y I I∈Is)))
    (λ {w} {x} {y} {z} r w≈x xy∈r y≈z → is! (λ I I∈Is →
      rol-≈ ⌊ I ⌋ r (is✓ w≈x I I∈Is) (is✓ xy∈r I I∈Is) (is✓ y≈z I I∈Is)))
  , id )

-- meets are surjective

meet-surj : ∀ Is → (meet Is ∈ Surjective)
meet-surj Is = surj (λ x → (x , ≈-refl ⌊ meet Is ⌋))

-- meets are lower bounds

meet-lb : ∀ Is I → (I ∈ Is) → (meet Is ≲ I)
meet-lb Is I I∈Is =
  ( morph (ind I)
      (λ x≈y → is✓ x≈y I I∈Is)
      (λ x∈⟦c⟧ → is✓ x∈⟦c⟧ I I∈Is)
      (λ xy∈⟦r⟧ → is✓ xy∈⟦r⟧ I I∈Is)
  , λ x → ≈-refl ⌊ I ⌋ )

-- meets are greatest lower bounds on surjective interpretations

meet-glb : ∀ Is J → (J ∈ Surjective) → (∀ I → (I ∈ Is) → (J ≲ I)) → (J ≲ meet Is)
meet-glb Is J J∈Surj J≲Is =
  ( morph (ind⁻¹ J∈Surj)
      (λ {x} {y} x≈y → is! (λ I I∈Is →
        ≈-trans ⌊ I ⌋ (≈-sym ⌊ I ⌋ (lemma I I∈Is x)) (≈-trans ⌊ I ⌋ (≲-resp-≈ ≲⌊ J≲Is I I∈Is ⌋ x≈y) (lemma I I∈Is y))))
      (λ {c} {x} x∈⟦c⟧ → is! (λ I I∈Is →
        con-≈ ⌊ I ⌋ c (≲-resp-con ≲⌊ J≲Is I I∈Is ⌋ x∈⟦c⟧) (lemma I I∈Is x)))
      (λ {r} {x} {y} xy∈⟦r⟧ → is! (λ I I∈Is →
        rol-≈ ⌊ I ⌋ r (≈-sym ⌊ I ⌋ (lemma I I∈Is x)) (≲-resp-rol ≲⌊ J≲Is I I∈Is ⌋ xy∈⟦r⟧) (lemma I I∈Is y)))
  , λ x → is! (λ I I∈Is →
      ≈-trans ⌊ I ⌋ (≈-sym ⌊ I ⌋ (lemma I I∈Is (ind J x))) (≲-resp-ind (J≲Is I I∈Is) x)) ) where

  lemma : ∀ I I∈Is x → ⌊ I ⌋ ⊨ ≲-image ≲⌊ J≲Is I I∈Is ⌋ x ≈ ind I (ind⁻¹ J∈Surj x)
  lemma I I∈Is x =
    ≈-trans ⌊ I ⌋ (≲-resp-≈ ≲⌊ J≲Is I I∈Is ⌋ (surj✓ J∈Surj x))
      (≲-resp-ind (J≲Is I I∈Is) (ind⁻¹ J∈Surj x))

-- Mediating morphisms for meets are unique

meet-uniq : ∀ Is (I : Interp Σ X) → (I ∈ Is) → (J≲₁I J≲₂I : meet Is ≲ I) → (J≲₁I ≋ J≲₂I)
meet-uniq Is I I∈Is J≲₁I J≲₂I x = ≈-trans ⌊ I ⌋ (≲-resp-ind J≲₁I x) (≈-sym ⌊ I ⌋ (≲-resp-ind J≲₂I x))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

module MorePropAlgebra.Structures where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Function.Base using (_∋_; _$_)
open import Cubical.Foundations.Function
-- open import Function.Reasoning using (∋-syntax)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax to infix  -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix  -4 ∃[∶]-syntax --
  ; ∀[∶]-syntax to infix  -4 ∀[∶]-syntax --
  ; ∀[]-syntax to infix  -4 ∀[]-syntax   --
  )

open import Utils
open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming
  ( _ᵗ⇒_ to infixr 0 _ᵗ⇒_
  ; ∀ᵖ[∶]-syntax to infix -4 ∀ᵖ[∶]-syntax
  ; ∀ᵖ〚∶〛-syntax to infix -4 ∀ᵖ〚∶〛-syntax
  ; ∀ᵖ!〚∶〛-syntax to infix -4 ∀ᵖ!〚∶〛-syntax
  ; ∀〚∶〛-syntax to infix -4 ∀〚∶〛-syntax
  )
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Consequences

-- taken from the cubical standard library and adapted to hProps:
--   IsSemigroup
--   IsMonoid
--   IsGroup
--   IsAbGroup
--   IsRing
--   IsCommRing

record IsSemigroup {A : Type ℓ} (_·_ : A → A → A) : Type ℓ where
  constructor issemigroup
  field
    is-set   : [ isSetᵖ A ]
    is-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z

  _ : [ isSetᵖ A                  ]; _ = is-set
  _ : [ isAssociativeˢ _·_ is-set ]; _ = is-assoc

isSemigroup : {A : Type ℓ} (_·_ : A → A → A) → hProp ℓ
isSemigroup _·_ .fst = IsSemigroup _·_
isSemigroup _·_ .snd (issemigroup a₀ b₀) (issemigroup a₁ b₁) = φ where
  abstract φ = λ i → let is-set = isSetIsProp a₀ a₁ i in issemigroup is-set (snd (isAssociativeˢ _·_ is-set) b₀ b₁ i)

record IsMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor ismonoid
  field
    is-Semigroup : [ isSemigroup _·_ ]
    is-identity  : ∀ x → (x · ε ≡ x) × (ε · x ≡ x)

  open IsSemigroup is-Semigroup public

  _ : [ isSemigroup _·_          ]; _ = is-Semigroup
  _ : [ isIdentityˢ _·_ is-set ε ]; _ = is-identity

  is-lid : (x : A) → ε · x ≡ x
  is-lid x = is-identity x .snd

  is-rid : (x : A) → x · ε ≡ x
  is-rid x = is-identity x .fst

isMonoid : {A : Type ℓ} (ε : A) (_·_ : A → A → A) → hProp ℓ
isMonoid ε _·_ .fst = IsMonoid ε _·_
isMonoid ε _·_ .snd (ismonoid a₀ b₀) (ismonoid a₁ b₁) = φ where
  abstract φ = λ i → let is-Semigroup = snd (isSemigroup _·_) a₀ a₁ i
                         is-set       = IsSemigroup.is-set is-Semigroup
                     in ismonoid is-Semigroup (snd (isIdentityˢ _·_ is-set ε) b₀ b₁ i)

record IsGroup {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where
  constructor isgroup
  field
    is-Monoid  : [ isMonoid 0g _+_ ]
    is-inverse : ∀ x → (x + (- x) ≡ 0g) × ((- x) + x ≡ 0g)

  open IsMonoid is-Monoid public

  _ : [ isMonoid 0g _+_             ]; _ = is-Monoid
  _ : [ isInverseˢ is-set 0g _+_ -_ ]; _ = is-inverse

  infixl 6 _-_

  _-_ : G → G → G
  x - y = x + (- y)

  is-invl : (x : G) → (- x) + x ≡ 0g
  is-invl x = is-inverse x .snd

  is-invr : (x : G) → x + (- x) ≡ 0g
  is-invr x = is-inverse x .fst

isGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G) → hProp ℓ
isGroup 0g _+_ -_ .fst = IsGroup 0g _+_ -_
isGroup 0g _+_ -_ .snd (isgroup a₀ b₀) (isgroup a₁ b₁) = φ where
  abstract φ = λ i → let is-Monoid = snd (isMonoid 0g _+_) a₀ a₁ i
                         is-set    = IsMonoid.is-set is-Monoid
                     in isgroup is-Monoid (snd (isInverseˢ is-set 0g _+_ -_) b₀ b₁ i)

record IsAbGroup {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G) : Type ℓ where
  constructor isabgroup
  field
    is-Group : [ isGroup 0g _+_ -_ ]
    is-comm  : ∀ x y → x + y ≡ y + x

  open IsGroup is-Group public

  _ : [ isGroup 0g _+_ (-_)       ]; _ = is-Group
  _ : [ isCommutativeˢ _+_ is-set ]; _ = is-comm

isAbGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G) → hProp ℓ
isAbGroup 0g _+_ -_ .fst = IsAbGroup 0g _+_ -_
isAbGroup 0g _+_ -_ .snd (isabgroup a₀ b₀) (isabgroup a₁ b₁) = φ where
  abstract φ = λ i → let is-Group = snd (isGroup 0g _+_ -_) a₀ a₁ i
                         is-set   = IsGroup.is-set is-Group
                     in isabgroup is-Group (snd (isCommutativeˢ _+_ is-set) b₀ b₁ i)

record IsSemiring {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where
  constructor issemiring
  field
    +-Monoid  : [ isMonoid 0r _+_ ]
    ·-Monoid  : [ isMonoid 1r _·_ ]
    +-comm    : ∀ x y → x + y ≡ y + x
    is-dist   : ∀ x y z → (x · (y +  z) ≡ (x · y) + (x · z)) × ((x +  y) · z  ≡ (x · z) + (y · z))

  open IsMonoid +-Monoid public
    renaming
      ( is-assoc     to +-assoc
      ; is-identity  to +-identity
      ; is-lid       to +-lid
      ; is-rid       to +-rid
      ; is-Semigroup to +-Semigroup )

  open IsMonoid ·-Monoid hiding (is-set) public
    renaming
      ( is-assoc     to ·-assoc
      ; is-identity  to ·-identity
      ; is-lid       to ·-lid
      ; is-rid       to ·-rid
      ; is-Semigroup to ·-Semigroup )

  _ : [ isMonoid  0r _+_               ]; _ = +-Monoid
  _ : [ isMonoid  1r _·_               ]; _ = ·-Monoid
  _ : [ isCommutativeˢ _+_ is-set      ]; _ = +-comm
  _ : [ isDistributiveˢ is-set _+_ _·_ ]; _ = is-dist

isSemiring : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) → hProp ℓ
isSemiring 0r 1r _+_ _·_ .fst = IsSemiring 0r 1r _+_ _·_
isSemiring 0r 1r _+_ _·_ .snd (issemiring a₀ b₀ c₀ d₀) (issemiring a₁ b₁ c₁ d₁) = φ where
  abstract φ = λ i → let +-Monoid = snd (isMonoid 0r _+_) a₀ a₁ i
                         ·-Monoid = snd (isMonoid 1r _·_) b₀ b₁ i
                         is-set   = IsMonoid.is-set +-Monoid
                         +-comm   = snd (isCommutativeˢ _+_ is-set) c₀ c₁ i
                         is-dist  = snd (isDistributiveˢ is-set _+_ _·_) d₀ d₁ i
                     in issemiring +-Monoid ·-Monoid +-comm is-dist

record IsCommSemiring {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where
  constructor iscommsemiring
  field
    is-Semiring : [ isSemiring 0r 1r _+_ _·_ ]
    ·-comm    : ∀ x y → x · y ≡ y · x

  open IsSemiring is-Semiring public

  _ : [ isSemiring 0r 1r _+_ _·_       ]; _ = is-Semiring
  _ : [ isCommutativeˢ _+_ is-set      ]; _ = +-comm

isCommSemiring : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) → hProp ℓ
isCommSemiring 0r 1r _+_ _·_ .fst = IsCommSemiring 0r 1r _+_ _·_
isCommSemiring 0r 1r _+_ _·_ .snd (iscommsemiring a₀ b₀) (iscommsemiring a₁ b₁) = φ where
  abstract φ = λ i → let is-Semiring = snd (isSemiring 0r 1r _+_ _·_) a₀ a₁ i
                         is-set   = IsSemiring.is-set is-Semiring
                         ·-comm   = snd (isCommutativeˢ _·_ is-set) b₀ b₁ i
                     in iscommsemiring is-Semiring ·-comm

record IsRing {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where
  constructor isring
  field
    +-AbGroup : [ isAbGroup 0r _+_ -_ ]
    ·-Monoid  : [ isMonoid  1r _·_ ]
    is-dist   : ∀ x y z → (x · (y +  z) ≡ (x · y) + (x · z)) × ((x +  y) · z  ≡ (x · z) + (y · z))

  open IsAbGroup +-AbGroup using (is-set) public

  _ : [ isAbGroup 0r _+_ -_            ]; _ = +-AbGroup
  _ : [ isMonoid  1r _·_               ]; _ = ·-Monoid
  _ : [ isDistributiveˢ is-set _+_ _·_ ]; _ = is-dist

  open IsAbGroup +-AbGroup hiding (is-set) public
    renaming
      ( is-assoc     to +-assoc
      ; is-identity  to +-identity
      ; is-lid       to +-lid
      ; is-rid       to +-rid
      ; is-inverse   to +-inv
      ; is-invl      to +-linv
      ; is-invr      to +-rinv
      ; is-comm      to +-comm
      ; is-Semigroup to +-Semigroup
      ; is-Monoid    to +-Monoid
      ; is-Group     to +-Group )

  open IsMonoid ·-Monoid hiding (is-set) public
    renaming
      ( is-assoc     to ·-assoc
      ; is-identity  to ·-identity
      ; is-lid       to ·-lid
      ; is-rid       to ·-rid
      ; is-Semigroup to ·-Semigroup )

  ·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
  ·-rdist-+ x y z = is-dist x y z .fst

  ·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
  ·-ldist-+ x y z = is-dist x y z .snd

  -- TODO: prove these somewhere

  -- zero-lid : (x : R) → 0r · x ≡ 0r
  -- zero-lid x = zero x .snd

  -- zero-rid : (x : R) → x · 0r ≡ 0r
  -- zero-rid x = zero x .fst

isRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) → hProp ℓ
isRing 0r 1r _+_ _·_ -_ .fst = IsRing 0r 1r _+_ _·_ -_
isRing 0r 1r _+_ _·_ -_ .snd (isring a₀ b₀ c₀) (isring a₁ b₁ c₁) = φ where
  abstract φ = λ i → let +-AbGroup = snd (isAbGroup 0r _+_ -_) a₀ a₁ i
                         ·-Monoid  = snd (isMonoid 1r _·_) b₀ b₁ i
                         is-set    = IsAbGroup.is-set +-AbGroup
                         is-dist   = snd (isDistributiveˢ is-set _+_ _·_) c₀ c₁ i
                     in isring +-AbGroup ·-Monoid is-dist

record IsCommRing {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where
  constructor iscommring
  field
    is-Ring : [ isRing 0r 1r _+_ _·_ -_ ]
    ·-comm  : ∀ x y → x · y ≡ y · x

  open IsRing is-Ring public

  _ : [ isRing 0r 1r _+_ _·_ (-_) ]; _ = is-Ring
  _ : [ isCommutativeˢ _·_ is-set ]; _ = ·-comm

isCommRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) → hProp ℓ
isCommRing 0r 1r _+_ _·_ -_ .fst = IsCommRing 0r 1r _+_ _·_ -_
isCommRing 0r 1r _+_ _·_ -_ .snd (iscommring a₀ b₀) (iscommring a₁ b₁) = φ where
  abstract φ = λ i → let is-Ring = snd (isRing 0r 1r _+_ _·_ -_) a₀ a₁ i
                         is-set  = IsRing.is-set is-Ring
                         ·-comm  = snd (isCommutativeˢ _·_ is-set) b₀ b₁ i
                     in iscommring is-Ring ·-comm

-- Definition 4.1.2.
-- A classical field is a set F with points 0, 1 : F, operations +, · : F → F → F, which is a commutative ring with unit, such that
--   (∀ x : F) x ≠ 0 ⇒ (∃ y : F) x · y = 1.

record IsClassicalField {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_⁻¹ : (x : F) → {{ ! [ ¬'(x ≡ 0f) ] }} → F) : Type ℓ where
  constructor isclassicalfield

  field
    is-set      : [ isSetᵖ F ]
    is-CommRing : [ isCommRing 0f 1f _+_ _·_ -_ ]
    -- WARNING: this is not directly Booij's definition, since Booij does not talk about an inverse operation `_⁻¹`
    --          we need to somehow obtain this operation
    ·-inv       : [ isNonzeroInverseˢ' is-set 0f 1f _·_ _⁻¹ ] -- classical version of `isNonzeroInverse`

  ·-linv : (x : F) {{ p : ! [ ¬' (x ≡ 0f) ] }} → ((x ⁻¹) · x) ≡ 1f -- wow, uses `p` already in `⁻¹`
  ·-linv x {{p}} = snd (·-inv x)

  ·-rinv : (x : F) {{ p : ! [ ¬' (x ≡ 0f) ] }} → (x · (x ⁻¹)) ≡ 1f
  ·-rinv x {{p}} = fst (·-inv x)

  open IsCommRing is-CommRing hiding (is-set) public

isClassicalField : {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_⁻¹ : (x : F) → {{ ! [ ¬'(x ≡ 0f) ] }} → F) → hProp ℓ
isClassicalField 0f 1f _+_ _·_ -_ _⁻¹ .fst = IsClassicalField 0f 1f _+_ _·_ -_ _⁻¹
isClassicalField 0f 1f _+_ _·_ -_ _⁻¹ .snd (isclassicalfield a₀ b₀ c₀) (isclassicalfield a₁ b₁ c₁) = φ where
  abstract φ = λ i → let is-set = isSetIsProp a₀ a₁ i in isclassicalfield is-set (snd (isCommRing 0f 1f _+_ _·_ -_) b₀ b₁ i) (snd (isNonzeroInverseˢ' is-set 0f 1f _·_ _⁻¹) c₀ c₁ i)

-- Definition 4.1.5.
-- A constructive field is a set F with points 0, 1 : F, binary operations +, · : F → F → F, and a binary relation # such that
-- 1. (F, 0, 1, +, ·) is a commutative ring with unit;
-- 2. x : F has a multiplicative inverse iff x # 0;
-- 3. # is tight, i.e. ¬(x # y) ⇒ x = y;
-- 4. + is #-extensional, that is, for all w, x, y, z : F
--    w + x # y + z ⇒ w # y ∨ x # z.

record IsConstructiveField {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_#_ : hPropRel F F ℓ') {- (_⁻¹ : (x : F) → {{[ x # 0f ]}} → F) -} : Type (ℓ-max ℓ ℓ') where
  constructor isconstructivefield

  field
    is-CommRing : [ isCommRing 0f 1f _+_ _·_ -_ ]
  open IsCommRing is-CommRing using (is-set)
  field
    ·-inv''     : ∀ x → [ (∃[ y ] [ is-set ] x · y ≡ˢ 1f) ⇔ x # 0f ]
    -- these should follow:
    --   ·-inv       : [ isNonzeroInverseˢ is-set 0f 1f _·_ _#_ _⁻¹ ]
    --   ·-invnz     : [ isInverseNonzeroˢ is-set 0f 1f _·_ _#_ ]
    --   ·-inv-back : ∀ x y → (x · y ≡ 1f) → [ x # 0f ] × [ y # 0f ]
    +-#-ext     : ∀ w x y z → [ (w + x) # (y + z) ] → [ (w # y) ⊔ (x # z) ]
    #-tight     : ∀ a b → [ ¬(a # b) ] → a ≡ b
    -- #-ApartnessRel  : [ isApartnessRel _#_ ]
  --
  -- ·-linv : (x : F) {{ p : [ x # 0f ] }} → ((x ⁻¹) · x) ≡ 1f -- wow, uses `p` already in `⁻¹`
  -- ·-linv x {{p}} = snd (·-inv x)
  --
  -- ·-rinv : (x : F) {{ p : [ x # 0f ] }} → (x · (x ⁻¹)) ≡ 1f
  -- ·-rinv x {{p}} = fst (·-inv x)

  _ : [ isCommRing 0f 1f _+_ _·_ -_              ]; _ = is-CommRing
  _ : [ isNonzeroInverseˢ'' is-set 0f 1f _·_ _#_ ]; _ = ·-inv''
  _ : [ is-+-#-Extensional _+_ _#_               ]; _ = +-#-ext
  _ : [ isTightˢ''' _#_ is-set                   ]; _ = #-tight

  open IsCommRing is-CommRing hiding (is-set) public
  -- open IsApartnessRelᵖ isApartnessRel public
  --   renaming
  --     ( isIrrefl  to #-irrefl
  --     ; isSym     to #-sym
  --     ; isCotrans to #-cotrans )

isConstructiveField : {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_#_ : hPropRel F F ℓ') {- (_⁻¹ : (x : F) → {{[ x # 0f ]}} → F) -} → hProp (ℓ-max ℓ ℓ')
isConstructiveField 0f 1f _+_ _·_ -_ _#_ {- _⁻¹ -} .fst = IsConstructiveField 0f 1f _+_ _·_ -_ _#_ {- _⁻¹ -}
isConstructiveField 0f 1f _+_ _·_ -_ _#_ {- _⁻¹ -} .snd (isconstructivefield a₀ b₀ c₀ d₀) (isconstructivefield a₁ b₁ c₁ d₁) = φ where
  abstract φ = λ i → let is-CommRing = snd (isCommRing 0f 1f _+_ _·_ -_) a₀ a₁ i
                         is-set      = IsCommRing.is-set is-CommRing
                         in isconstructivefield is-CommRing (snd (isNonzeroInverseˢ'' is-set 0f 1f _·_ _#_) b₀ b₁ i) (snd (is-+-#-Extensional _+_ _#_) c₀ c₁ i) (snd (isTightˢ''' _#_ is-set) d₀ d₁ i)

-- Definition 4.1.8.
-- Let (A, ≤) be a partial order, and let min, max : A → A → A be binary operators on A. We say that (A, ≤, min, max) is a lattice if min computes greatest lower bounds in the sense that for every x, y, z : A, we have
--   z ≤ min(x,y) ⇔ z ≤ x ∧ z ≤ y,
-- and max computes least upper bounds in the sense that for every x, y, z : A, we have
--   max(x,y) ≤ z ⇔ x ≤ z ∧ y ≤ z.

-- Remark 4.1.9.
--   1. From the fact that (A, ≤, min, max) is a lattice, it does not follow that for every x and y,
--        max(x, y) = x ∨ max(x, y) = y,
--      which would hold in a linear order.
--      However, in Lemma 6.7.1 we characterize max as
--        z < max(x, y) ⇔ z < x ∨ z < y,
--     and similarly for min.
--   2. In a partial order, for two fixed elements a and b, all joins and meets of a, b are equal,
--      so that Lemma 2.6.20 the type of joins and the type of meets are propositions.
--      Hence, providing the maps min and max as in the above definition is equivalent to
--      the showing the existence of all binary joins and meets.

-- NOTE: in the non-cubical standard library, we have
--
--   record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
--     field
--       ∨-comm        : Commutative ∨  -- ∀ x y     →                 (x ∨ y) ≈ (y ∨ x)
--       ∨-assoc       : Associative ∨  -- ∀ x y z   →                 ((x ∨ y) ∨ z) ≈ (x ∨ (y ∨ z))
--       ∨-cong        : Congruent₂ ∨   -- ∀ x y u v → x ≈ y → u ≈ v → (x ∨ u) ≈ (y ∨ v)
--       ∧-comm        : Commutative ∧  -- ∀ x y     →                 (x ∧ y) ≈ (y ∧ x)
--       ∧-assoc       : Associative ∧  -- ∀ x y z   →                 ((x ∧ y) ∧ z) ≈ (x ∧ (y ∧ z))
--       ∧-cong        : Congruent₂ ∧   -- ∀ x y u v → x ≈ y → u ≈ v → (x ∧ u) ≈ (y ∧ v)
--       absorptive    : Absorptive ∨ ∧ -- ∀ x y     →                 ((x ∨ (x ∧ y)) ≈ x) × ((x ∧ (x ∨ y)) ≈ x)
--
-- where they derive
--
--   ∨-absorbs-∧ : ∨ Absorbs ∧
--   ∨-absorbs-∧ = proj₁ absorptive
--
--   ∧-absorbs-∨ : ∧ Absorbs ∨
--   ∧-absorbs-∨ = proj₂ absorptive
--
--   ∧-congˡ : LeftCongruent ∧
--   ∧-congˡ y≈z = ∧-cong refl y≈z
--
--   ∧-congʳ : RightCongruent ∧
--   ∧-congʳ y≈z = ∧-cong y≈z refl
--
--   ∨-congˡ : LeftCongruent ∨
--   ∨-congˡ y≈z = ∨-cong refl y≈z
--
--   ∨-congʳ : RightCongruent ∨
--   ∨-congʳ y≈z = ∨-cong y≈z refl
--
-- and additionally we might also proof Lemma 6.7.1 and Lemma 2.6.20 (as mentioned in the remark above)
-- maybe we can proof from a linearorder that we have MinTrichtotomy and MaxTrichtotomy

record IsLattice {A : Type ℓ} (_≤_ : hPropRel A A ℓ') (min max : A → A → A) : Type (ℓ-max ℓ ℓ') where
  constructor islattice
  field
    ≤-PartialOrder : [ isPartialOrder _≤_ ]
    is-min         : ∀ x y z → [ z ≤ (min x y) ⇔ z ≤ x ⊓ z ≤ y ]
    is-max         : ∀ x y z → [ (max x y) ≤ z ⇔ x ≤ z ⊓ y ≤ z ]
    -- glb      : ∀ x y z → z ≤ min x y → z ≤ x × z ≤ y
    -- glb-back : ∀ x y z → z ≤ x × z ≤ y → z ≤ min x y
    -- lub      : ∀ x y z → max x y ≤ z → x ≤ z × y ≤ z
    -- lub-back : ∀ x y z → x ≤ z × y ≤ z → max x y ≤ z

  _ : [ isPartialOrder _≤_ ]; _ = ≤-PartialOrder
  _ : [ isMin _≤_ min      ]; _ = is-min
  _ : [ isMax _≤_ max      ]; _ = is-max

  open IsPartialOrder ≤-PartialOrder public
    renaming
      ( is-refl    to ≤-refl
      ; is-antisym to ≤-antisym
      ; is-trans   to ≤-trans )

isLattice : {A : Type ℓ} (_≤_ : hPropRel A A ℓ') (min max : A → A → A) → hProp (ℓ-max ℓ ℓ')
isLattice _≤_ min max .fst = IsLattice _≤_ min max
isLattice _≤_ min max .snd (islattice a₀ b₀ c₀) (islattice a₁ b₁ c₁) = φ where
  abstract φ = λ i → islattice (snd (isPartialOrder _≤_) a₀ a₁ i) (snd (isMin _≤_ min) b₀ b₁ i) (snd (isMax _≤_ max) c₀ c₁ i)

-- Definition 4.1.10.
-- An ordered field is a set F together with constants 0, 1, operations +, ·, min, max, and a binary relation < such that:
-- 1. (F, 0, 1, +, ·) is a commutative ring with unit;
-- 2. < is a strict [partial] order;
-- 3. x : F has a multiplicative inverse iff x # 0, recalling that # is defined as in Lemma 4.1.7;
-- 4. ≤, as in Lemma 4.1.7, is antisymmetric, so that (F, ≤) is a partial order;
-- 5. (F, ≤, min, max) is a lattice.
-- 6. for all x, y, z, w : F:
--    x + y < z + w ⇒ x < z ∨ y < w, (†)
--    0 < z ∧ x < y ⇒ x z < y z.     (∗)
-- Our notion of ordered fields coincides with The Univalent Foundations Program [89, Definition 11.2.7].

-- NOTE: well, the HOTT book definition organizes things slightly different. Why prefer one approach over the other?

record IsAlmostPartiallyOrderedField {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) {- (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) -} : Type (ℓ-max ℓ ℓ') where
  constructor isalmostpartiallyorderedfield

  infixl 4 _#_
  infixl 4 _≤_

  -- ≤, as in Lemma 4.1.7
  _≤_ : hPropRel F F ℓ'
  x ≤ y = ¬ (y < x)

  field
    -- 1.
    is-CommRing : [ isCommRing 0f 1f _+_ _·_ -_ ]
    -- 2.
    <-StrictPartialOrder : [ isStrictPartialOrder _<_ ]

  open IsCommRing is-CommRing public
  open IsStrictPartialOrder <-StrictPartialOrder public
    renaming
      ( is-irrefl  to <-irrefl
      ; is-trans   to <-trans
      ; is-cotrans to <-cotrans )

  <-asym : [ isAsym _<_ ]
  <-asym = irrefl+trans⇒asym _<_ <-irrefl <-trans

  -- # is defined as in Lemma 4.1.7
  _#_ : hPropRel F F ℓ'
  x # y = [ <-asym x y ] (x < y) ⊎ᵖ (y < x)

  field
    -- 3.
    ·-inv''     : ∀ x → [ (∃[ y ] [ is-set ] x · y ≡ˢ 1f) ⇔ x # 0f ]
    -- ·-rinv     : (x : F) → (p : x # 0f) → x · (_⁻¹ᶠ x {{p}}) ≡ 1f
    -- ·-linv     : (x : F) → (p : x # 0f) → (_⁻¹ᶠ x {{p}}) · x ≡ 1f
    -- ·-inv-back : (x y : F) → (x · y ≡ 1f) → x # 0f × y # 0f
    -- 4. NOTE: we already have ≤-isPartialOrder in ≤-isLattice
    -- ≤-isPartialOrder : IsPartialOrder _≤_
    -- 5.
    ≤-Lattice : [ isLattice _≤_ min max ]

  _ : isSet F                                     ; _ = is-set
  _ : [ isCommRing 0f 1f _+_ _·_ (-_)            ]; _ = is-CommRing
  _ : [ isStrictPartialOrder _<_                 ]; _ = <-StrictPartialOrder
  _ : [ isNonzeroInverseˢ'' is-set 0f 1f _·_ _#_ ]; _ = ·-inv''
  _ : [ isLattice _≤_ min max                    ]; _ = ≤-Lattice

  open IsLattice ≤-Lattice renaming (≤-antisym to ≤-antisymᵗ) public

  ≤-antisym : [ isAntisymˢ _≤_ is-set ]
  ≤-antisym = isAntisymˢ⇔isAntisym _≤_ is-set .snd ≤-antisymᵗ

isAlmostPartiallyOrderedField : {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) {- (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) -} → hProp (ℓ-max ℓ ℓ')
isAlmostPartiallyOrderedField {ℓ = ℓ} {ℓ' = ℓ'} {F = F} 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -} .fst = IsAlmostPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -}
isAlmostPartiallyOrderedField {ℓ = ℓ} {ℓ' = ℓ'} {F = F} 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -} .snd (isalmostpartiallyorderedfield a₀ b₀ c₀ d₀) (isalmostpartiallyorderedfield a₁ b₁ c₁ d₁) = φ where
  abstract φ = λ i → let -- we are doing basically "the same" as in `IsAlmostPartiallyOrderedField`
                         _≤_                  : hPropRel F F ℓ'
                         x ≤ y                = ¬ (y < x) -- ≤, as in Lemma 4.1.7
                         is-CommRing          = snd (isCommRing 0f 1f _+_ _·_ -_) a₀ a₁ i
                         is-set               = IsCommRing.is-set is-CommRing
                         <-StrictPartialOrder = snd (isStrictPartialOrder _<_) b₀ b₁ i
                         open IsStrictPartialOrder <-StrictPartialOrder
                           renaming
                             ( is-irrefl  to <-irrefl
                             ; is-trans   to <-trans
                             ; is-cotrans to <-cotrans )
                         <-asym               : [ isAsym _<_ ]
                         <-asym               = irrefl+trans⇒asym _<_ <-irrefl <-trans
                         _#_                  : hPropRel F F ℓ'
                         x # y                = [ <-asym x y ] (x < y) ⊎ᵖ (y < x) -- # is defined as in Lemma 4.1.7
                         ·-inv''              = snd (isNonzeroInverseˢ'' is-set 0f 1f _·_ _#_) c₀ c₁ i
                         ≤-isLattice          = snd (isLattice _≤_ min max) d₀ d₁ i
                     in isalmostpartiallyorderedfield is-CommRing <-StrictPartialOrder ·-inv'' ≤-isLattice

record IsPartiallyOrderedField {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) {- (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) -} : Type (ℓ-max ℓ ℓ') where
  constructor ispartiallyorderedfield
  field
    -- 1. 2. 3. 4. 5.
    is-AlmostPartiallyOrderedField : [ isAlmostPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ᶠ -} ]
    -- 6. (†)
    +-<-ext : ∀ w x y z → [ (w + x) < (y + z) ] → [ (w < y) ⊔ (x < z) ]
    -- 6. (∗)
    ·-preserves-< : ∀ x y z → [ 0f < z ] → [ x < y ] → [ (x · z) < (y · z) ]

  _ : [ isAlmostPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max ]; _ = is-AlmostPartiallyOrderedField
  _ : [ is-+-<-Extensional _+_ _<_                                 ]; _ = +-<-ext
  _ : [ operation _·_ preserves _<_ when (λ z → 0f < z)            ]; _ = ·-preserves-<

  open IsAlmostPartiallyOrderedField is-AlmostPartiallyOrderedField public

isPartiallyOrderedField : {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) {- (_⁻¹ᶠ : (x : F) → {{x # 0f}} → F) -} → hProp (ℓ-max ℓ ℓ')
isPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -} .fst = IsPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -}
isPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -} .snd (ispartiallyorderedfield a₀ b₀ c₀) (ispartiallyorderedfield a₁ b₁ c₁) = φ where
  abstract φ = λ i → ispartiallyorderedfield (snd (isAlmostPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ᶠ -}) a₀ a₁ i) (snd (is-+-<-Extensional _+_ _<_) b₀ b₁ i) (snd (operation _·_ preserves _<_ when (λ z → 0f < z)) c₀ c₁ i)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- Occurs there are several ways to parse an operator application.
module AmbiguousParseForApplication where

postulate
  X             : Set
  if_then_else_ : X -> X -> X -> X
  if_then_      : X -> X -> X

bad : X -> X
bad x = if x then if x then x else x


text:
module SafeFlagPrimTrustMe-2 where

open import Agda.Builtin.TrustMe


text:
-- Andreas, 2015-09-09 Issue 1643
-- {-# OPTIONS -v tc.mod.apply:20 #-}
-- {-# OPTIONS -v scope:50 -v scope.inverse:100 -v interactive.meta:20 #-}

module _ where

module M where
  postulate A : Set

module N = M  -- This alias used to introduce a display form M.A --> N.A

open M

postulate
  a : A

test : Set
test = a

-- Error WAS: N.A !=< Set of type Set
-- SHOULD BE:   A !=< Set of type Set

{-
ScopeInfo
  current = ModuleAlias
  context = TopCtx
  modules
    scope
    scope ModuleAlias
      private
        names
          A --> [ModuleAlias.M.A]
      public
        modules
          M --> [ModuleAlias.M]
          N --> [ModuleAlias.N]
    scope ModuleAlias.M
      public
        names
          A --> [ModuleAlias.M.A]
    scope ModuleAlias.N
      public
        names
          A --> [ModuleAlias.N.A]
-}


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

open import Cubical.Algebra.OrderedCommMonoid.Base public
open import Cubical.Algebra.OrderedCommMonoid.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- Properties for the equality on streams
------------------------------------------------------------------------------

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

module FOTC.Data.Stream.Equality.PropertiesI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.PropertiesI
open import FOTC.Relation.Binary.Bisimilarity.Type

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

stream-≡→≈ : ∀ {xs ys} → Stream xs → Stream ys → xs ≡ ys → xs ≈ ys
stream-≡→≈ Sxs _ refl = ≈-refl Sxs

≈→Stream₁ : ∀ {xs ys} → xs ≈ ys → Stream xs
≈→Stream₁ {xs} {ys} h = Stream-coind A h' (ys , h)
   where
   A : D → Set
   A ws = ∃[ zs ] ws ≈ zs

   h' : ∀ {xs} → A xs → ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'
   h' (_ , Axs) with ≈-out Axs
   ... | x' , xs' , zs' , prf₁ , prf₂ , prf₃ = x' , xs' , prf₁ , (zs' , prf₃)

≈→Stream₂ : ∀ {xs ys} → xs ≈ ys → Stream ys
≈→Stream₂ {xs} {ys} h = Stream-coind A h' (xs , h)
   where
   A : D → Set
   A zs = ∃[ ws ] ws ≈ zs

   h' : ∀ {ys} → A ys → ∃[ y' ] ∃[ ys' ] ys ≡ y' ∷ ys' ∧ A ys'
   h'  (_ , Ays) with ≈-out Ays
   ... | y' , ys' , zs' , prf₁ , prf₂ , prf₃ = y' , zs' , prf₂ , (ys' , prf₃)

≈→Stream : ∀ {xs ys} → xs ≈ ys → Stream xs ∧ Stream ys
≈→Stream {xs} {ys} h = ≈→Stream₁ h , ≈→Stream₂ h


text:
{- Adjunction between suspension and loop space (Rongji Kang, Oct. 2021)

Main results:

- Ω∙ : ℕ → Pointed ℓ → Pointed ℓ
- ΣΩAdjunction : ((X , x₀) : Pointed ℓ) (Y : Pointed ℓ') → (∙Susp X →∙ Y) ≃ ((X , x₀) →∙ Ω∙ 1 Y)
-}
{-# OPTIONS --safe #-}
module Cubical.HITs.Susp.LoopAdjunction where

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

open import Cubical.Foundations.Pointed.Base
open import Cubical.Data.Nat.Base
open import Cubical.HITs.Susp.Base

private
  variable
    ℓ ℓ' : Level

Ω∙ : ℕ → Pointed ℓ → Pointed ℓ
Ω∙ 0 X = X
Ω∙ 1 (X , x) = (x ≡ x) , refl
Ω∙ (suc (suc n)) X = Ω∙ 1 (Ω∙ (suc n) X)

ΣX→∙YEquiv : ((X , x₀) : Pointed ℓ) ((Y , y₀) : Pointed ℓ')
           → (Susp∙ X →∙ (Y , y₀)) ≃ (Σ[ y ∈ Y ] (X → (y₀ ≡ y)))
ΣX→∙YEquiv (X , x₀) (Y , y₀) =
  isoToEquiv (iso left→right right→left right→left→right left→right→left)
  where
    left→right : (Susp∙ X →∙ (Y , y₀)) → Σ[ y ∈ Y ] (X → (y₀ ≡ y))
    left→right (f , b) .fst = f south
    left→right (f , b) .snd x = sym b ∙ cong f (merid x)

    right→left : (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → (Susp∙ X →∙ (Y , y₀))
    right→left (y , g) .fst north = y₀
    right→left (y , g) .fst south = y
    right→left (y , g) .fst (merid x i) = g x i
    right→left (y , g) .snd = refl

    right→left→right : (g : Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → left→right (right→left g) ≡ g
    right→left→right (y , g) i .fst = y
    right→left→right (y , g) i .snd x = lUnit (g x) (~ i)

    left→right→left : (f : Susp∙ X →∙ (Y , y₀)) → right→left (left→right f) ≡ f
    left→right→left (f , b) i .fst north = b (~ i)
    left→right→left (f , b) i .fst south = f south
    left→right→left (f , b) i .fst (merid x j) =
      hcomp (λ k → λ { (i = i0) → compPath-filler (sym b) (cong f (merid x)) k j
                     ; (i = i1) → f (merid x (j ∧ k))
                     ; (j = i0) → b (~ i)
                     ; (j = i1) → f (merid x k) })
            (b (~ (i ∨ j)))
    left→right→left (f , b) i .snd j = b (~ i ∨ j)

X→∙ΩYEquiv : ((X , x₀) : Pointed ℓ)((Y , y₀) : Pointed ℓ')
           → ((X , x₀) →∙ Ω∙ 1 (Y , y₀)) ≃ (Σ[ y ∈ Y ] (X → (y₀ ≡ y)))
X→∙ΩYEquiv (X , x₀) (Y , y₀) =
  isoToEquiv (iso left→right right→left right→left→right left→right→left)
  where
    left→right : ((X , x₀) →∙ Ω∙ 1 (Y , y₀)) → Σ[ y ∈ Y ] (X → (y₀ ≡ y))
    left→right _ .fst = y₀
    left→right (f , b) .snd = f

    right→left : (Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → ((X , x₀) →∙ Ω∙ 1 (Y , y₀))
    right→left (y , g) .fst x = g x ∙ sym (g x₀)
    right→left (y , g) .snd = rCancel (g x₀)

    right→left→right : (g : Σ[ y ∈ Y ] (X → (y₀ ≡ y))) → left→right (right→left g) ≡ g
    right→left→right (y , g) i .fst = g x₀ i
    right→left→right (y , g) i .snd x j =
      hcomp (λ k → λ { (i = i0) → compPath-filler (g x) (sym (g x₀)) k j
                     ; (i = i1) → g x j
                     ; (j = i0) → y₀
                     ; (j = i1) → g x₀ (i ∨ ~ k) })
            (g x j)

    f-filler : ((X , x₀) →∙ Ω∙ 1 (Y , y₀)) → X → (i j k : I) → Y
    f-filler (f , b) x i j k =
      hfill (λ k' → λ { (i = i0) → compPath-filler (f x) (sym (f x₀)) k' j
                      ; (i = i1) → f x j
                      ; (j = i0) → y₀
                      ; (j = i1) → b i (~ k') })
            (inS (f x j)) k

    bottom : ((X , x₀) →∙ Ω∙ 1 (Y , y₀)) → (i j k : I) → Y
    bottom (f , b) i j k =
      hcomp (λ l → λ { (i = i0) → b (~ l) (k ∧ ~ j)
                     ; (i = i1) → b (j ∨ ~ l) k
                     ; (j = i0) → b (~ l) k
                     ; (j = i1) → y₀
                     ; (k = i0) → y₀
                     ; (k = i1) → b (~ l ∨ i) (~ j) })
            y₀

    left→right→left : (f : (X , x₀) →∙ Ω∙ 1 (Y , y₀)) → right→left (left→right f) ≡ f
    left→right→left (f , b) i .fst x j =
      f-filler (f , b) x i j i1
    left→right→left (f , b) i .snd j k =
      hcomp (λ l → λ { (i = i0) → rCancel-filler (f x₀) l j k
                     ; (i = i1) → b j k
                     ; (j = i0) → f-filler (f , b) x₀ i k l
                     ; (j = i1) → y₀
                     ; (k = i0) → y₀
                     ; (k = i1) → b i (~ l ∧ ~ j) })
            (bottom (f , b) i j k)

{- The Main Theorem -}
ΣΩAdjunction : ((X , x₀) : Pointed ℓ) (Y : Pointed ℓ') → (Susp∙ X →∙ Y) ≃ ((X , x₀) →∙ Ω∙ 1 Y)
ΣΩAdjunction X Y = compEquiv (ΣX→∙YEquiv X Y) (invEquiv (X→∙ΩYEquiv X Y))

max_stars_repo_name: FernandoLarrain/cubical


text:
module Prelude.Fractional where

open import Agda.Primitive

record Fractional {a} (A : Set a) : Set (lsuc a) where
  infixl 7 _/_
  field
    Constraint : A → A → Set a
    _/_ : (x y : A) {{_ : Constraint x y}} → A

  NoConstraint : Set a
  NoConstraint = ∀ {x y} → Constraint x y

open Fractional {{...}} using (_/_) public
{-# DISPLAY Fractional._/_ _ x y = x / y #-}

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

module ky where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong; cong₂; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Rational using (ℚ; _+_; _*_; _-_)
open import Data.Bool
open import Data.Bool.Properties
open import Data.Rational
open import Data.Nat as ℕ using (ℕ; zero; suc; ⌊_/2⌋)
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Agda.Builtin.Size
open import Data.Product
open import Data.Unit
open import Data.Maybe
open import Data.List

TyCon = List Set

data Env : TyCon → Set₁ where
  nil : Env []
  cons : ∀{t Γ} →  t → Env Γ → Env (t ∷ Γ)

data Idx : Set → TyCon → Set₁ where
  fst : ∀{t Γ} → Idx t (t ∷ Γ)
  nxt : ∀{t t' Γ} → Idx t Γ → Idx t (t' ∷ Γ)

get : ∀{t Γ} → Idx t Γ → Env Γ → t
get fst       (cons v _)  = v
get (nxt idx) (cons _ vs) = get idx vs

upd : ∀{t Γ} → Idx t Γ → t -> Env Γ → Env Γ
upd fst       v' (cons _ vs) = cons v' vs
upd (nxt idx) v' (cons v vs) = cons v (upd idx v' vs)

data Exp : TyCon → Set → Set₁ where
  EVal : ∀{t Γ} → t → Exp Γ t
  EVar : ∀{t Γ} → Idx t Γ → Exp Γ t
  EPlus : ∀{Γ} → Exp Γ ℚ → Exp Γ ℚ → Exp Γ ℚ

record Cotree (i : Size) (A : Set) (Γ : TyCon) : Set₁

data Pattern : Size → TyCon → Set₁ where
  mkPattern : ∀{i Γ} →  --{j₁ j₂ : Size< i} →
    (Cotree i Bool Γ → Cotree i Bool Γ → Cotree i Bool Γ) →
    Pattern i Γ

data Com : Size → TyCon → Set → Set₁ where
  CSkip : ∀{i Γ} → Com i Γ ⊤
  CPrim : ∀{i t Γ} → Pattern i Γ → Com i Γ t → Com i Γ t → Com i Γ t
  --CFlip : ∀{i t Γ} → Com i Γ t → Com i Γ t → Com i Γ t
  CUpd : ∀{i t Γ} → Idx t Γ → Exp Γ t → Com i Γ ⊤
  --CAlloc : ∀{t Γ} → Exp Γ t → Com (t ∷ Γ) ⊤
  CIte : ∀{i t Γ} → Exp Γ Bool → Com i Γ t → Com i Γ t → Com i Γ t
  CSeq : ∀{i t Γ} → Com i Γ ⊤ → Com i Γ t → Com i Γ t
  CWhile : ∀{i t Γ} → Exp Γ Bool → Com i Γ t → Com i Γ ⊤

eval : ∀{t Γ} → Env Γ → Exp Γ t → t
eval ρ (EVal v) = v
eval ρ (EVar x) = get x ρ
eval ρ (EPlus e₁ e₂) = eval ρ e₁ + eval ρ e₂

-- Cf. Abel 2017 (Equational Reasoning about Formal Languages in Coalgebraic Style)
record Cotree i A Γ where
  coinductive
  field
    ν : Env Γ -> Maybe (Env Γ)
    δ : ∀{j : Size< i} → Env Γ → A →  Cotree j A Γ

open Cotree

∅ : ∀{i A Γ} → Cotree i A Γ
ν ∅ _   = nothing
δ ∅ _ _ = ∅

flip : ∀(i Γ) → Cotree i Bool Γ → Cotree i Bool Γ → Cotree i Bool Γ
flip i Γ t₁ t₂ = t
  where t : Cotree i Bool Γ
        ν t ρ       = nothing
        δ t ρ true  = t₁
        δ t ρ false = t₂

interp : ∀(i){τ} → ∀(Γ) → Com i Γ τ → Cotree i Bool Γ
interp i Γ CSkip = t
  where t : ∀{j} → Cotree j Bool Γ
        ν t ρ   = just ρ
        δ t ρ _ = ∅
interp i Γ (CPrim (mkPattern f) c₁ c₂) = t
  where t : Cotree i Bool Γ
        ν t ρ   = nothing
        δ t ρ _ = f (interp i Γ c₁) (interp i Γ c₂)
{-interp i Γ (CFlip c₁ c₂) = t
  where t : Cotree i Bool Γ
        ν t ρ       = nothing
        δ t ρ true  = interp i Γ c₁
        δ t ρ false = interp i Γ c₂-}
interp i Γ (CUpd x e) = t
  where t : ∀{j} → Cotree j Bool Γ
        ν t ρ   = just (upd x (eval ρ e) ρ)
        δ t ρ _ = ∅
interp i Γ (CIte e c₁ c₂) = t
  where t : Cotree i Bool Γ
        ν t ρ with eval ρ e
        ...      | true  = ν (interp i Γ c₁) ρ
        ...      | false = ν (interp i Γ c₂) ρ
        δ t ρ b with eval ρ e
        ...        | true  = δ (interp i Γ c₁) ρ b
        ...        | false = δ (interp i Γ c₂) ρ b
interp i Γ (CSeq c₁ c₂) = t
  where t : Cotree i Bool Γ
        ν t ρ   = nothing
        δ t ρ b with ν (interp i Γ c₁) ρ
        ...        | nothing = δ (interp i Γ c₁) ρ  b
        ...        | just ρ' = δ (interp i Γ c₂) ρ' b
interp i Γ (CWhile e c) = t
  where t : Cotree i Bool Γ
        ν t ρ with eval ρ e
        ...      | true  = ν (interp i Γ c) ρ
        ...      | false = just ρ
        δ t ρ b with eval ρ e
        ...        | true  = δ (interp i Γ c) ρ b
        ...        | false = ∅

-- Flip as a derived command
cflip : ∀(i Γ){τ} → Com i Γ τ → Com i Γ τ → Com i Γ τ
cflip i Γ = CPrim (mkPattern (flip i Γ))

max_stars_repo_name: OUPL/Zar

max_issues_repo_name: OUPL/Zar

max_forks_repo_name: OUPL/Zar


text:
open import Agda.Builtin.Coinduction
open import Agda.Builtin.IO
open import Agda.Builtin.Unit

data D : Set where
  c : ∞ D → D

d : D
d = c (♯ d)

postulate
  seq    : {A B : Set} → A → B → B
  return : {A : Set} → A → IO A

{-# COMPILE GHC return = \_   -> return #-}
{-# COMPILE GHC seq    = \_ _ -> seq    #-}

main : IO ⊤
main = seq d (return tt)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Common.Char where

open import Agda.Builtin.Char public
open import Common.Bool

charEq : Char -> Char -> Bool
charEq = primCharEquality


text:
module Data.List.Iterable where

open import Data
open import Data.List
import      Data.List.Functions as List
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Relator.Equals
open import Structure.Container.Iterable
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

instance
  List-iterable : Iterable(List(T))
  Iterable.Element (List-iterable {T = T}) = T
  Iterable.isEmpty List-iterable = List.isEmpty
  Iterable.current List-iterable ∅       = <>
  Iterable.current List-iterable (x ⊰ l) = x
  Iterable.indexStep List-iterable ∅       = <>
  Iterable.indexStep List-iterable (_ ⊰ _) = <>
  Iterable.step List-iterable ∅       = <>
  Iterable.step List-iterable (x ⊰ l) = l

instance
  List-finite-iterable : Iterable.Finite(List-iterable{T = T})
  ∃.witness List-finite-iterable = List.foldᵣ
  ∃.proof List-finite-iterable {iter = ∅}     = [≡]-intro
  ∃.proof List-finite-iterable {iter = x ⊰ l} = [≡]-intro

instance
  List-empty : Iterable.EmptyConstruction(List-iterable{T = T})(∅)
  List-empty = <>

instance
  List-prepend : Iterable.PrependConstruction(List-iterable{T = T})(_⊰_)
  ∃.witness List-prepend = [≡]-intro
  ∃.proof   List-prepend = [∧]-intro [≡]-intro [≡]-intro


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.S2 where

open import Cubical.HITs.S2.Base public

-- open import Cubical.HITs.S2.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module FRP.JS.Size where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size

{-# BUILTIN SIZE    Size #-}
{-# BUILTIN SIZESUC ↑_   #-}
{-# BUILTIN SIZEINF ∞    #-}
{-# COMPILED_JS     ↑_ function(x) { return null; } #-}
{-# COMPILED_JS     ∞  null #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monad.Kleisli where

open import Categories.Category
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation hiding (_≡_; equiv; id)
open import Categories.Monad

Kleisli : ∀ {o ℓ e} {C : Category o ℓ e} → Monad C → Category o ℓ e
Kleisli {C = C} M = record
  { Obj = Obj
  ; _⇒_ = λ A B → (A ⇒ F₀ B)
  ; _≡_ = _≡_
  ; _∘_ = λ f g → (μ.η _ ∘ F₁ f) ∘ g
  ; id = η.η _
  ; assoc = assoc′
  ; identityˡ = identityˡ′
  ; identityʳ = identityʳ′
  ; equiv = equiv
  ; ∘-resp-≡ = λ f≡h g≡i → ∘-resp-≡ (∘-resp-≡ refl (F-resp-≡ f≡h)) g≡i
  }
  where
  module M = Monad M
  open M using (μ; η; F)
  module μ = NaturalTransformation μ
  module η = NaturalTransformation η
  open Functor F
  open Category C
  open Equiv

  .assoc′ : ∀ {A B C D} {f : A ⇒ F₀ B} {g : B ⇒ F₀ C} {h : C ⇒ F₀ D}
          → (μ.η D ∘ (F₁ ((μ.η D ∘ F₁ h) ∘ g))) ∘ f ≡ (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)
  assoc′ {A} {B} {C} {D} {f} {g} {h} =
      begin
        (μ.η D ∘ F₁ ((μ.η D ∘ F₁ h) ∘ g)) ∘ f
      ↓⟨ assoc ⟩
        μ.η D ∘ (F₁ ((μ.η D ∘ F₁ h) ∘ g) ∘ f)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ (F-resp-≡ assoc)) ⟩
        μ.η D ∘ (F₁ (μ.η D ∘ (F₁ h ∘ g)) ∘ f)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ homomorphism) ⟩
        μ.η D ∘ ((F₁ (μ.η D) ∘ F₁ (F₁ h ∘ g)) ∘ f)
      ↓⟨ ∘-resp-≡ʳ assoc ⟩
        μ.η D ∘ (F₁ (μ.η D) ∘ (F₁ (F₁ h ∘ g) ∘ f))
      ↑⟨ assoc ⟩
        (μ.η D ∘ F₁ (μ.η D)) ∘ (F₁ (F₁ h ∘ g) ∘ f)
      ↓⟨ ∘-resp-≡ˡ M.assoc ⟩
        (μ.η D ∘ μ.η (F₀ D)) ∘ (F₁ (F₁ h ∘ g) ∘ f)
      ↓⟨ assoc ⟩
        μ.η D ∘ (μ.η (F₀ D) ∘ (F₁ (F₁ h ∘ g) ∘ f))
      ↑⟨ ∘-resp-≡ʳ assoc ⟩
        μ.η D ∘ ((μ.η (F₀ D) ∘ F₁ (F₁ h ∘ g)) ∘ f)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ (∘-resp-≡ʳ homomorphism)) ⟩
        μ.η D ∘ ((μ.η (F₀ D) ∘ (F₁ (F₁ h) ∘ F₁ g)) ∘ f)
      ↑⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ assoc) ⟩
        μ.η D ∘ (((μ.η (F₀ D) ∘ F₁ (F₁ h)) ∘ F₁ g) ∘ f)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ (∘-resp-≡ˡ (μ.commute h))) ⟩
        μ.η D ∘ (((F₁ h ∘ μ.η C) ∘ F₁ g) ∘ f)
      ↓⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ assoc) ⟩
        μ.η D ∘ ((F₁ h ∘ (μ.η C ∘ F₁ g)) ∘ f)
      ↓⟨ ∘-resp-≡ʳ assoc ⟩
        μ.η D ∘ (F₁ h ∘ ((μ.η C ∘ F₁ g) ∘ f))
      ↑⟨ assoc ⟩
        (μ.η D ∘ F₁ h) ∘ ((μ.η C ∘ F₁ g) ∘ f)
      ∎
    where
    open HomReasoning

  .identityˡ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ (η.η B)) ∘ f ≡ f
  identityˡ′ {A} {B} {f} =
      begin
        (μ.η B ∘ F₁ (η.η B)) ∘ f
      ↓⟨ ∘-resp-≡ˡ M.identityˡ ⟩
        id ∘ f
      ↓⟨ identityˡ ⟩
        f
      ∎
    where
    open HomReasoning

  .identityʳ′ : ∀ {A B} {f : A ⇒ F₀ B} → (μ.η B ∘ F₁ f) ∘ η.η A ≡ f
  identityʳ′ {A} {B} {f} =
      begin
        (μ.η B ∘ F₁ f) ∘ η.η A
      ↓⟨ assoc ⟩
        μ.η B ∘ (F₁ f ∘ η.η A)
      ↑⟨ ∘-resp-≡ʳ (η.commute f) ⟩
        μ.η B ∘ (η.η (F₀ B) ∘ f)
      ↑⟨ assoc ⟩
        (μ.η B ∘ η.η (F₀ B)) ∘ f
      ↓⟨ ∘-resp-≡ˡ M.identityʳ ⟩
        id ∘ f
      ↓⟨ identityˡ ⟩
        f
      ∎
    where
    open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue533 where

data Empty : Set where

empty : {A B : Set} → (B → Empty) → B → A
empty f x with f x
... | ()

fail : ∀ {A : Set} → Empty → A
fail {A} = empty absurd
  where
    absurd : _ → Empty
    absurd ()
-- should check (due to postponed emptyness constraint, see issue 479)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Nat

data S : Set where
  c : S

module _ (A : Set) where
  test : S
  test with c
  ... | q = {!q!}  -- Splitting on q should succeed

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

module _ {A : Set} {n : Nat} (xs : Vec A n) where

  foo : Vec A n → Nat
  foo [] = 0
  foo (x ∷ ys) with x ∷ xs
  ... | zs = {!zs!}
    -- Splitting on zs should succeed here.
    -- Splitting on xs should fail.

max_stars_repo_name: shlevy/agda


text:
data {-sdaf-} Nat {-sdaf-} : {-sdaf-} Set {-sdaf-} where {-sdaf-}
      zero {-sdaf-} : {-sdaf-} Nat {-sdaf-}
      suc {-sdaf-} :{-sdaf-} Nat {-sdaf-} -> {-sdaf-} Nat {-sdaf-}

data Impossible : Set where {-Comment which should not be duplicated-}