text:
module Tactic.Reflection.Reright where
  open import Prelude hiding (abs)

  open import Container.Traversable

  open import Tactic.Reflection
  open import Tactic.Reflection.Match
  open import Tactic.Reflection.Replace
  open import Tactic.Reflection.Quote

  private
    {-# TERMINATING #-}
    reorderVars : List Nat → Term → Term
    reorderVars xs (var x args) = var (maybe x id (index xs x)) (fmap (reorderVars xs) <$> args)
    reorderVars xs (con c args) = con c ((fmap ∘ fmap) (reorderVars xs) args)
    reorderVars xs (def f args) = def f (fmap (reorderVars xs) <$> args)
    reorderVars xs (lam v t) = lam v (reorderVars (0 ∷ weaken 1 xs) <$> t)
    reorderVars xs (pat-lam cs args) = pat-lam (fmap (reorderVarsInClause xs) cs) ((fmap ∘ fmap) (reorderVars xs) args) where
      reorderVarsInClause : List Nat → Clause → Clause -- TODO reorder patterns?
      reorderVarsInClause xs (clause ps t) = (clause ps (reorderVars xs t))
      reorderVarsInClause xs (absurd-clause ps) = (absurd-clause ps)
    reorderVars xs (pi a b) = pi (reorderVars xs <$> a) (reorderVars (0 ∷ weaken 1 xs) <$> b)
    reorderVars xs (agda-sort (set t)) = agda-sort (set (reorderVars xs t))
    reorderVars xs (agda-sort (lit n)) = agda-sort (lit n)
    reorderVars xs (agda-sort unknown) = agda-sort unknown
    reorderVars xs (lit l) = lit l
    reorderVars xs (meta x args) = meta x $ (fmap ∘ fmap) (reorderVars xs) args
    reorderVars xs unknown = unknown

    {-# TERMINATING #-}
    freeDependencies : List (Arg Type) → Type → Maybe VarSet
    freeDependencies Γ x = foldr _∪_ (freeVars x) <$> mapM go (freeVars x) where
      _∪_ : VarSet → VarSet → VarSet -- REFACTOR this was stolen from Tactic.Reflection.Free
      []       ∪ ys = ys
      xs       ∪ [] = xs
      (x ∷ xs) ∪ (y ∷ ys) with compare x y
      ... | (less    _) = x ∷ (xs ∪ (y ∷ ys))
      ... | (equal   _) = x ∷ (xs ∪ ys)
      ... | (greater _) = y ∷ ((x ∷ xs) ∪ ys)

      go : Nat → Maybe VarSet
      go v = weaken (suc v) $ join $ freeDependencies (drop (suc v) Γ) <$> (unArg <$> index Γ v)

    .test-freeDependencies₁ : freeDependencies [] unknown ≡ just []
    test-freeDependencies₁ = refl

    .test-freeDependencies₂ : freeDependencies (vArg (var₀ 0) ∷ vArg unknown ∷ []) (var₀ 0) ≡ just (0 ∷ 1 ∷ [])
    test-freeDependencies₂ = refl

    .test-freeDependencies₃ : freeDependencies (vArg (var₀ 0) ∷ vArg (var₀ 1) ∷ vArg unknown ∷ vArg unknown ∷ []) (var₀ 0) ≡ just (0 ∷ 1 ∷ 3 ∷ [])
    test-freeDependencies₃ = refl

    .test-freeDependencies₄ : freeDependencies (vArg (var₀ 0) ∷ vArg (var₀ 1) ∷ vArg unknown ∷ vArg unknown ∷ []) (var₀ 1) ≡ just (1 ∷ 3 ∷ [])
    test-freeDependencies₄ = refl

    .test-freeDependencies₅ : freeDependencies (vArg (var₀ 1) ∷ vArg unknown ∷ vArg unknown ∷ []) (var₀ 0) ≡ just (0 ∷ 2 ∷ [])
    test-freeDependencies₅ = refl

    .test-freeDependencies₆ : freeDependencies (vArg (var₀ 0) ∷ vArg (var₀ 1) ∷ vArg unknown ∷ vArg unknown ∷ []) (var₁ 0 (var₀ 1)) ≡ just (0 ∷ 1 ∷ 3 ∷ [])
    test-freeDependencies₆ = refl

    record Request : Set where
      field
        l≡r : Term
        A : Type
        L R : Type
        Γᶜ : List (Arg Type)
        𝐺 : Type

      [iᶜ∣iᶜ∈FVᴬ] : VarSet
      [iᶜ∣iᶜ∈FVᴬ] = maybe [] id $ freeDependencies Γᶜ A -- TODO this is a hack; I don't expect freeDependencies will return 'nothing', but if it does, I hope(!) the rest of the computation will fail

      [iᶜ∣iᶜ∉FVᴬ] : VarSet
      [iᶜ∣iᶜ∉FVᴬ] = filter (not ∘ flip elem [iᶜ∣iᶜ∈FVᴬ]) (from 0 for (length Γᶜ))

      record γᶜ' : Set where
        field
          iᶜ : Nat
          γᶜᵢ : Arg Type
          iᶜ∈FVᴬ : Bool
          iʷ : Nat
          γᶜᵢ∈Γʳ : Bool

        gᶜᵢ : Type
        gᶜᵢ = unArg γᶜᵢ

      Γᶜ' : List γᶜ'
      Γᶜ' = go 0 (length Γᶜ) Γᶜ where
        go : Nat → Nat → List (Arg Type) → List γᶜ'
        go iᶜ 0 _ = []
        go iᶜ _ [] = []
        go iᶜ (suc n) (γᶜᵢ ∷ Γᶜ) = γᶜᵢ' ∷ go (suc iᶜ) n (weaken 1 Γᶜ) where
          γᶜᵢ' = record
            { iᶜ = iᶜ
            ; γᶜᵢ = γᶜᵢ
            ; iᶜ∈FVᴬ = elem iᶜ [iᶜ∣iᶜ∈FVᴬ]
            ; iʷ = if elem iᶜ [iᶜ∣iᶜ∉FVᴬ] then (length (filter (_<? iᶜ) [iᶜ∣iᶜ∉FVᴬ])) else (length [iᶜ∣iᶜ∉FVᴬ] + (length (filter (_≤? iᶜ) [iᶜ∣iᶜ∈FVᴬ])))
            ; γᶜᵢ∈Γʳ = let gᶜᵢ = unArg γᶜᵢ in (isNo $ weaken 1 gᶜᵢ == weaken 1 gᶜᵢ r[ unknown / L ]) && (isNo $ l≡r == var₀ iᶜ)
            }

      [iʷ∣γᶜᵢ∈Γʳ] : VarSet
      [iʷ∣γᶜᵢ∈Γʳ] = iʷ <$> filter γᶜᵢ∈Γʳ Γᶜ' where open γᶜ'

      [iʷ] : List Nat
      [iʷ] = iʷ <$> Γᶜ' where open γᶜ'

      subsetList : {A : Set} → List A → List Nat → Maybe (List A)
      subsetList xs is = traverse (index xs) is

      module _ where
        private
          Γʷ/ᶜ : Maybe (List (Arg Type))
          Γʷ/ᶜ = go [iʷ] Γᶜ where
            go : List Nat → List (Arg Type) → Maybe (List (Arg Type))
            go _ [] = just []
            go [] _ = nothing
            go (iʷ ∷ [iʷ]) (γᶜᵢ ∷ Γᶜ) = _∷_ <$> (strengthen (suc iʷ) $ reorderVars [iʷ] <$> γᶜᵢ) <*> (go [iʷ] Γᶜ)

        Γʷ/ᴬ = join $ subsetList <$> Γʷ/ᶜ <*> pure [iᶜ∣iᶜ∈FVᴬ]
        Γʷ/⁻ᴬ = join $ subsetList <$> Γʷ/ᶜ <*> pure [iᶜ∣iᶜ∉FVᴬ]

      module _ where
        private
          Lʷ = reorderVars [iʷ] L

        Γʷ = caseF Γʷ' of _R[ var₀ (length [iᶜ∣iᶜ∉FVᴬ]) / Lʷ ] where
          Γʷ' : Maybe (List (Arg Type))
          Γʷ' = _++_ <$> Γʷ/⁻ᴬ <*> (_∷_ <$> (strengthen (length [iᶜ∣iᶜ∉FVᴬ] + 1) $ hArg (reorderVars [iʷ] A)) <*> Γʷ/ᴬ) where

        𝐺ʷ = reorderVars [iʷ] 𝐺 r[ var₀ (length [iᶜ∣iᶜ∉FVᴬ]) / Lʷ ]

      module _ where
        private
          Rʷ = reorderVars [iʷ] R

        gʳ : Maybe Type
        gʳ = join $ go <$> gʳ' <*> pure [iʷ∣γᶜᵢ∈Γʳ] <*> pure 𝐺ʷʳ where
          go : List (Arg Type) → List Nat → Type → Maybe Type
          go [] [] 𝐺 = just 𝐺
          go (γʷ ∷ Γʷ) (iʷ ∷ iʷs) 𝐺 = go Γʷ iʷs $ pi (weaken (1 + iʷ) γʷ) $ abs "_" $ weaken 1 𝐺 r[ var₀ 0 / var₀ $ weaken 1 iʷ ]
          go _ _ _ = nothing

          gʳ' : Maybe (List (Arg Type))
          gʳ' = join $ subsetList <$> (caseF Γʷ of _R[ Rʷ / var₀ (length [iᶜ∣iᶜ∉FVᴬ]) ]) <*> pure [iʷ∣γᶜᵢ∈Γʳ]

          𝐺ʷʳ = 𝐺ʷ r[ Rʷ / var₀ (length [iᶜ∣iᶜ∉FVᴬ]) ]

        helper-type : Maybe Type
        helper-type = telPi <$> (_++_ <$> (reverse <$> Γʷ) <*> (_∷_ <$> (pure $ vArg (def₂ (quote _≡_) (var₀ (length [iᶜ∣iᶜ∉FVᴬ])) Rʷ)) <*> ([_] ∘ vArg <$> (weaken 1 <$> gʳ)))) <*> pure (weaken 2 𝐺ʷ)

      make-vars-from-args : List Nat → List (Arg Type) → Maybe (List (Arg Type))
      make-vars-from-args [] [] = pure []
      make-vars-from-args (i ∷ is) (x ∷ xs) = _∷_ <$> pure (var₀ i <$ x) <*> make-vars-from-args is xs
      make-vars-from-args _ _ = nothing

      defineHelper : Name → TC ⊤
      defineHelper n =
        maybe (typeError ( strErr "error constructing helper function type, patterns, or term" ∷
                           strErr "\nhelper-type:" ∷ termErr (maybe unknown id helper-type) ∷
                           strErr "\n`helper-type:" ∷ termErr (` helper-type) ∷
                           strErr "\nhelper-patterns:" ∷ termErr (` helper-patterns) ∷
                           strErr "\nhelper-term:" ∷ termErr (maybe unknown id helper-term) ∷
                           strErr "\ngʳ:" ∷ termErr (` gʳ) ∷
                           strErr "\nΓʷ:" ∷ termErr (` Γʷ) ∷
                           strErr "\n𝐺ʷ:" ∷ termErr (` 𝐺ʷ) ∷
                           strErr "\nl≡r:" ∷ termErr (` l≡r) ∷
                           strErr "\nA:" ∷ termErr (` A) ∷
                           strErr "\nL:" ∷ termErr (` L) ∷
                           strErr "\nR:" ∷ termErr (` R) ∷
                           strErr "\nΓᶜ:" ∷ termErr (` Γᶜ) ∷
                           strErr "\n𝐺:" ∷ termErr (` 𝐺) ∷
                           strErr "\nΓʷ/ᴬ" ∷ termErr (` Γʷ/ᴬ) ∷
                           strErr "\nΓʷ/⁻ᴬ" ∷ termErr (` Γʷ/⁻ᴬ) ∷
                           strErr "\n[iᶜ∣iᶜ∈FVᴬ]" ∷ termErr (` [iᶜ∣iᶜ∈FVᴬ]) ∷
                           strErr "\n[iᶜ∣iᶜ∉FVᴬ]" ∷ termErr (` [iᶜ∣iᶜ∉FVᴬ]) ∷
                           strErr "\n[iʷ]" ∷ termErr (` [iʷ]) ∷
                           [] ))
              (λ {(helper-type , helper-patterns , helper-term) →
                catchTC
                  (define (vArg n) helper-type [ clause helper-patterns helper-term ])
                  (typeError ( strErr "error defining helper function" ∷
                               strErr "\nhelper-type:" ∷ termErr helper-type ∷
                               strErr "\n`helper-type:" ∷ termErr (` helper-type) ∷
                               strErr "\nhelper-patterns:" ∷ termErr (` helper-patterns) ∷
                               strErr "\nhelper-term:" ∷ termErr helper-term ∷
                               strErr "\n`helper-term:" ∷ termErr (` helper-term) ∷
                               strErr "\ngʳ:" ∷ termErr (` gʳ) ∷
                               strErr "\nΓʷ:" ∷ termErr (` Γʷ) ∷
                               strErr "\n𝐺ʷ:" ∷ termErr (` 𝐺ʷ) ∷
                               strErr "\nl≡r:" ∷ termErr (` l≡r) ∷
                               strErr "\nA:" ∷ termErr (` A) ∷
                               strErr "\nL:" ∷ termErr (` L) ∷
                               strErr "\nR:" ∷ termErr (` R) ∷
                               strErr "\nΓᶜ:" ∷ termErr (` Γᶜ) ∷
                               strErr "\n𝐺:" ∷ termErr (` 𝐺) ∷
                               strErr "\nΓʷ/ᴬ" ∷ termErr (` Γʷ/ᴬ) ∷
                               strErr "\nΓʷ/⁻ᴬ" ∷ termErr (` Γʷ/⁻ᴬ) ∷
                               strErr "\n[iᶜ∣iᶜ∈FVᴬ]" ∷ termErr (` [iᶜ∣iᶜ∈FVᴬ]) ∷
                               strErr "\n[iᶜ∣iᶜ∉FVᴬ]" ∷ termErr (` [iᶜ∣iᶜ∉FVᴬ]) ∷
                               strErr "\n[iʷ]" ∷ termErr (` [iʷ]) ∷
                               [] ))
                  })
              (_,_ <$> helper-type <*> (_,_ <$> helper-patterns <*> helper-term))
        where

        helper-patterns : Maybe (List (Arg Pattern))
        helper-patterns = (λ pa w p-a pr → pa ++ w ∷ (p-a ++ pr)) <$> (telePat ∘ reverse <$> Γʷ/ᴬ) <*> just (hArg dot) <*> (telePat ∘ reverse <$> Γʷ/⁻ᴬ) <*> pure (vArg (con₀ (quote refl)) ∷ [ vArg (var "_") ])

        helper-term : Maybe Term
        helper-term = do
          γʷs ← join $ subsetList <$> Γʷ <*> pure [iʷ∣γᶜᵢ∈Γʳ]
          iʷs ← make-vars-from-args [iʷ∣γᶜᵢ∈Γʳ] γʷs
          pure (var 0 (reverse (weaken 1 iʷs)))

      callHelper : Name → Tactic
      callHelper n hole =
        maybe (typeError [ strErr "error constructing helper call" ])
              (unify hole)
              $ helper-call n
        where

        helper-call : Name → Maybe Term
        helper-call n = def n <$> (reverse <$> (_∷_ <$> pure (vArg l≡r) <*> Γʰ)) where
          Γʰ : Maybe $ List $ Arg Term
          Γʰ = (λ xs → take (length [iᶜ∣iᶜ∉FVᴬ]) xs ++ hArg unknown ∷ drop (length [iᶜ∣iᶜ∉FVᴬ]) xs) <$> (join $ make-vars-from-args <$> pure ([iᶜ∣iᶜ∉FVᴬ] ++ [iᶜ∣iᶜ∈FVᴬ]) <*> Γʰ') where
            Γʰ' : Maybe (List (Arg Type))
            Γʰ' = _++_ <$> subsetList Γᶜ [iᶜ∣iᶜ∉FVᴬ] <*> subsetList Γᶜ [iᶜ∣iᶜ∈FVᴬ]

    inferGoal : Term → TC Type
    inferGoal hole = unPi =<< forceFun =<< inferType hole where
      unPi : Type → TC Type
      unPi (pi _ (abs _ (meta x _))) = blockOnMeta! x
      unPi (pi _ (abs _ b)) = maybe (typeError (strErr "error strengthening" ∷ termErr b ∷ [])) pure $ strengthen 1 b
      unPi x = typeError (strErr "goal is not a pi type" ∷ termErr x ∷ [])

    getRequest : Term → Term → TC Request
    getRequest l≡r hole = do
      L≡R ← inferType l≡r
      L≡R-matched ← maybe (typeError (strErr "not an equality" ∷ termErr l≡r ∷ termErr L≡R ∷ [])) pure $
        match 3 (def (quote _≡_) (hArg unknown ∷ (hArg (var₀ 0)) ∷ (vArg (var₀ 1)) ∷ (vArg (var₀ 2)) ∷ [])) L≡R
      𝐺 ← inferGoal hole
      Γᶜ ← getContext
      case L≡R-matched of λ { (A ∷ L ∷ R ∷ []) →
        pure $ record { l≡r = l≡r ; A = A ; L = L ; R = R ; Γᶜ = Γᶜ ; 𝐺 = 𝐺 } }

  macro
    reright : Term → Tactic
    reright l≡r hole = do
      q ← getRequest l≡r hole
      n ← freshName "reright"
      let open Request q
      defineHelper n
      callHelper n hole

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
primitive
  primLevelMax : _

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module 10-localInstances where

import Data.Empty as E
open import Data.String using (String; toList; _≟_)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Nat using (ℕ) renaming (_≟_ to _ℕ≟_)
import Data.List as List
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Function using (_on_; _∘_)

record Eq (A : Set) : Set where
  field eq : A → A → Bool

length : String → ℕ
length = List.length ∘ toList

open Eq {{...}}

eqℕ : Eq ℕ
eqℕ = record { eq = λ x x' → ⌊ x ℕ≟ x' ⌋ }

eqString₁ : String → String → Bool
eqString₁ s₁ s₂ = ⌊ s₁ ≟ s₂ ⌋

eqString₂ : String → String → Bool
eqString₂ = eq on length

test : Bool → Bool
test lengthEq = if eq "abcd" "dcba" then false else true
  where eqLocal = record { eq = if lengthEq then eqString₂ else eqString₁ }

test2 = test true

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
------------------------------------------------------------------------------
-- Draft modules render to HTML (via an external Makefile)
------------------------------------------------------------------------------

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

module RenderToHTML where

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text: {-# OPTIONS --profile=modules --profile=internal #-}

max_stars_repo_name: sseefried/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers in non-reduced form.
------------------------------------------------------------------------

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

module Data.Rational.Unnormalised where

open import Data.Integer.Base as ℤ using (ℤ; ∣_∣; +_; +0; +[1+_]; -[1+_])
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Level using (0ℓ)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_)

------------------------------------------------------------------------
-- Definition

-- Here we define rationals that are not necessarily in reduced form.
-- Consequently there are multiple ways of representing a given rational
-- number, and the performance of the arithmetic operations may suffer
-- due to blowup of the numerator and denominator.

-- Nonetheless they are much easier to reason about. In general proofs
-- are first proved for these unnormalised rationals and then translated
-- into the normalised rationals.

record ℚᵘ : Set where
  constructor mkℚᵘ
  field
    numerator     : ℤ
    denominator-1 : ℕ

  denominatorℕ : ℕ
  denominatorℕ = suc denominator-1

  denominator : ℤ
  denominator = + denominatorℕ

open ℚᵘ public using ()
  renaming
  ( numerator    to ↥_
  ; denominator  to ↧_
  ; denominatorℕ to ↧ₙ_
  )

------------------------------------------------------------------------
-- Equality of rational numbers (does not coincide with _≡_)

infix 4 _≃_
data _≃_ : Rel ℚᵘ 0ℓ where
  *≡* : ∀ {p q} → (↥ p ℤ.* ↧ q) ≡ (↥ q ℤ.* ↧ p) → p ≃ q

------------------------------------------------------------------------
-- Ordering of rationals

infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≱_ _≮_ _≯_

data _≤_ : Rel ℚᵘ 0ℓ where
  *≤* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p) → p ≤ q

data _<_ : Rel ℚᵘ 0ℓ where
  *<* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.< (↥ q ℤ.* ↧ p) → p < q

_≥_ : Rel ℚᵘ 0ℓ
x ≥ y = y ≤ x

_>_ : Rel ℚᵘ 0ℓ
x > y = y < x

_≰_ : Rel ℚᵘ 0ℓ
x ≰ y = ¬ (x ≤ y)

_≱_ : Rel ℚᵘ 0ℓ
x ≱ y = ¬ (x ≥ y)

_≮_ : Rel ℚᵘ 0ℓ
x ≮ y = ¬ (x < y)

_≯_ : Rel ℚᵘ 0ℓ
x ≯ y = ¬ (x > y)

------------------------------------------------------------------------
-- Constructing rationals

infix 4 _≢0
_≢0 : ℕ → Set
n ≢0 = False (n ℕ.≟ 0)

-- An alternative constructor for ℚᵘ. See the constants section below
-- for examples of how to use this operator.

infixl 7 _/_

_/_ : (n : ℤ) (d : ℕ) .{d≢0 : d ≢0} → ℚᵘ
n / suc d = mkℚᵘ n d

------------------------------------------------------------------------------
-- Operations on rationals

infix  8 -_ 1/_
infixl 7 _*_ _÷_
infixl 6 _-_ _+_

-- negation

-_ : ℚᵘ → ℚᵘ
- mkℚᵘ n d = mkℚᵘ (ℤ.- n) d

-- addition

_+_ : ℚᵘ → ℚᵘ → ℚᵘ
p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

-- multiplication

_*_ : ℚᵘ → ℚᵘ → ℚᵘ
p * q = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)

-- subtraction

_-_ : ℚᵘ → ℚᵘ → ℚᵘ
p - q = p + (- q)

-- reciprocal: requires a proof that the numerator is not zero

1/_ : (p : ℚᵘ) → .{n≢0 : ∣ ↥ p ∣ ≢0} → ℚᵘ
1/ mkℚᵘ +[1+ n ] d = mkℚᵘ +[1+ d ] n
1/ mkℚᵘ -[1+ n ] d = mkℚᵘ -[1+ d ] n

-- division: requires a proof that the denominator is not zero

_÷_ : (p q : ℚᵘ) → .{n≢0 : ∣ ↥ q ∣ ≢0} → ℚᵘ
(p ÷ q) {n≢0} = p * (1/_ q {n≢0})

------------------------------------------------------------------------------
-- Some constants

0ℚᵘ : ℚᵘ
0ℚᵘ = + 0 / 1

1ℚᵘ : ℚᵘ
1ℚᵘ = + 1 / 1

½ : ℚᵘ
½ = + 1 / 2

-½ : ℚᵘ
-½ = - ½


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types #-}

open import Codata.Colist
open import Codata.Thunk
open import Size
open import Data.Empty
open import Relation.Binary.PropositionalEquality

module Examples.Colists.Auxiliary.Colist_member {A : Set} where

  data _∈_ : A → Colist A ∞ → Set where
    here : ∀ {x xs} → x ∈ (x ∷ xs)
    there : ∀{x y xs} → x ∈ xs .force → x ∈ (y ∷ xs)

  mem-abs : ∀{x xs} → x ∈ xs → xs ≡ [] → ⊥
  mem-abs {_} {.[]} () refl

max_stars_repo_name: LcicC/inference-systems-agda

max_issues_repo_name: LcicC/inference-systems-agda

max_forks_repo_name: LcicC/inference-systems-agda


text:
-- Andreas, 2022-03-11, issue #5823
-- Make sure we do not weaken the singleton detection too much by checking for loops.

open import Agda.Builtin.Nat

record ⊤ : Set where

record Wrap (A : Set) : Set where
  field unwrap : A

record _×_ (A B : Set) : Set where
  field
    fst : A
    snd : B

-- A singleton record type with nestings of Wrap.

Singleton = (Wrap ⊤ × Wrap (Wrap ⊤)) × Wrap (Wrap (Wrap ⊤ × ⊤) × Wrap ⊤)

-- Agda should solve this meta:

unique : Singleton
unique = _

-- This is fine, even though we pass through 'Wrap' several times.
-- Passing already visited non-recursive records is fine!

mutual
  record S (n : Nat) : Set where
    inductive; eta-equality
    field inn : T n

  T : Nat → Set
  T zero = ⊤
  T (suc n) = T n × S n

-- S n is a eta singleton type for each n because it is terminating.

inh5 : S 5
inh5 = _


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Number.Structures2 where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Foundations.Logic
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)

open import Utils
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions
open import MorePropAlgebra.Consequences
open import MorePropAlgebra.Structures

{-
| name | struct              | apart | abs | order | cauchy | sqrt₀⁺  | exp | final name                                                             |
|------|---------------------|-------|-----|-------|--------|---------|-----|------------------------------------------------------------------------|
| ℕ    | CommSemiring        |  (✓)  | (✓) | lin.  |        | (on x²) |     | LinearlyOrderedCommSemiring                                            |
| ℤ    | CommRing            |  (✓)  | (✓) | lin.  |        | (on x²) |     | LinearlyOrderedCommRing                                                |
| ℚ    | Field               |  (✓)  | (✓) | lin.  |        | (on x²) | (✓) | LinearlyOrderedField                                                   |
| ℝ    | Field               |  (✓)  | (✓) | part. |   ✓    |    ✓    | (✓) | CompletePartiallyOrderedFieldWithSqrt                                  |
| ℂ    | euclidean 2-Product |  (✓)  | (✓) |       |  (✓)   |         |  ?  | EuclideanTwoProductOfCompletePartiallyOrderedFieldWithSqrt             |
| R    | Ring                |   ✓   |  ✓  |       |        |         |  ?  | ApartnessRingWithAbsIntoCompletePartiallyOrderedFieldWithSqrt          |
| G    | Group               |   ✓   |  ✓  |       |        |         |  ?  | ApartnessGroupWithAbsIntoCompletePartiallyOrderedFieldWithSqrt         |
| K    | Field               |   ✓   |  ✓  |       |   ✓    |         |  ?  | CompleteApartnessFieldWithAbsIntoCompletePartiallyOrderedFieldWithSqrt |

-- NOTE: what about conjugation `conj`?
-}

-- we usually mean "CommRing" when writing just "Ring" ⇒ TODO: rename this where applicable

-- this is ℕ
record IsLinearlyOrderedCommSemiring {ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) : Type (ℓ-max ℓ ℓ') where
  constructor islinearlyorderedcommsemiring

  infixl 4 _#_
  infixl 4 _≤_

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

  field
    is-CommSemiring     : [ isCommSemiring 0f 1f _+_ _·_ ]
    <-StrictLinearOrder : [ isStrictLinearOrder _<_ ]
    ≤-Lattice           : [ isLattice _≤_ min max ]
    +-<-ext             : ∀ w x y z → [ (w + x) < (y + z) ] → [ (w < y) ⊔ (x < z) ]
    ·-preserves-<       : ∀ x y z   → [ 0f < z ] → [ x < y ] → [ (x · z) < (y · z) ]

  open IsCommSemiring is-CommSemiring public
  open IsStrictLinearOrder <-StrictLinearOrder public
    renaming
      ( is-irrefl  to <-irrefl
      ; is-trans   to <-trans
      ; is-tricho  to <-trichoᵗ )

  abstract
    <-asym : ∀ a b → [ a < b ] → [ ¬ b < a ] -- [ isAsym _<_ ]
    <-asym = irrefl+trans⇒asym _<_ <-irrefl <-trans

    <-irrefl'' : ∀ a b → ([ a < b ] ⊎ [ b < a ]) → [ ¬(a ≡ₚ b) ]
    <-irrefl'' = isIrrefl'⇔isIrrefl'' _<_ <-asym .fst (isIrrefl⇔isIrrefl' _<_ .fst <-irrefl)

    <-irreflˢ'' : ∀ a b → ([ a < b ] ⊎ [ b < a ]) → ¬ᵗ(a ≡ b)
    <-irreflˢ'' = isIrreflˢ''⇔isIrrefl'' _<_ is-set <-asym .snd <-irrefl''

    <-tricho : ∀ a b → ([ a < b ] ⊎ [ b < a ]) ⊎ (a ≡ b)
    <-tricho = isTrichotomousˢ⇔isTrichotomous _<_ is-set <-irrefl'' <-irreflˢ'' <-asym .snd <-trichoᵗ

    <-StrictPartialOrder : [ isStrictPartialOrder _<_ ]
    <-StrictPartialOrder = strictlinearorder⇒strictpartialorder _<_ <-StrictLinearOrder

    -- ≤-PartialOrder : [ isPartialOrder _≤_ ]
    -- ≤-PartialOrder = {! linearorder⇒partialorder !}

    ≤-LinearOrder : [ isLinearOrder _≤_ ]
    ≤-LinearOrder = ≤'-isLinearOrder <-StrictLinearOrder

    ≤-Preorder : [ isPreorder _≤_ ]
    ≤-Preorder = ≤'-isPreorder <-StrictPartialOrder

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

  #-ApartnessRel : [ isApartnessRel _#_ ]
  #-ApartnessRel = #''-isApartnessRel <-StrictPartialOrder <-asym

  open IsApartnessRel #-ApartnessRel public renaming
    ( is-irrefl  to #-irrefl
    ; is-sym     to #-sym
    ; is-cotrans to #-cotrans
    )

  _ : [ isCommSemiring 0f 1f _+_ _·_             ]; _ = is-CommSemiring
  _ : [ isStrictLinearOrder _<_                  ]; _ = <-StrictLinearOrder
  _ : [ isLattice _≤_ min max                    ]; _ = ≤-Lattice

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

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

isLinearlyOrderedCommSemiring : ∀{ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) → hProp (ℓ-max ℓ ℓ')
isLinearlyOrderedCommSemiring 0f 1f _+_ _·_ _<_ min max .fst = IsLinearlyOrderedCommSemiring 0f 1f _+_ _·_ _<_ min max
isLinearlyOrderedCommSemiring 0f 1f _+_ _·_ _<_ min max .snd = φ where
  abstract φ = {!   !}

-- this is ℤ
record IsLinearlyOrderedCommRing {ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) : Type (ℓ-max ℓ ℓ') where
  constructor islinearlyorderedcommring
  field
    is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0f 1f _+_ _·_ _<_ min max ]
    +-inverse : ∀ x → (x + (- x) ≡ 0f) × ((- x) + x ≡ 0f)

  infixl 6 _-_

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

  +-linv : (x : F) → (- x) + x ≡ 0f
  +-linv x = +-inverse x .snd

  +-rinv : (x : F) → x + (- x) ≡ 0f
  +-rinv x = +-inverse x .fst

  open IsLinearlyOrderedCommSemiring is-LinearlyOrderedCommSemiring public

isLinearlyOrderedCommRing : ∀{ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) → hProp (ℓ-max ℓ ℓ')
isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max .fst = IsLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max
isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max .snd = φ where
  abstract φ = {!   !}

-- this is ℚ
record IsLinearlyOrderedField {ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) : Type (ℓ-max ℓ ℓ') where
  constructor islinearlyorderedfield
  field
    is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0f 1f _+_ _·_ (-_) _<_ min max ]
  open IsLinearlyOrderedCommRing is-LinearlyOrderedCommRing public
  field
    ·-inv'' : ∀ x → [ (∃[ y ] ([ is-set ] (x · y) ≡ˢ 1f)) ⇔ (x # 0f) ]

isLinearlyOrderedField : ∀{ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) → hProp (ℓ-max ℓ ℓ')
isLinearlyOrderedField 0f 1f _+_ _·_ -_ _<_ min max .fst = IsLinearlyOrderedField 0f 1f _+_ _·_ -_ _<_ min max
isLinearlyOrderedField 0f 1f _+_ _·_ -_ _<_ min max .snd = φ where
  abstract φ = {!   !}

-- this is ℝ
record IsCompletePartiallyOrderedFieldWithSqrt {ℓ ℓ'} {F : Type ℓ} (0f 1f : F) (_+_ _·_ : F → F → F) (-_ : F → F) (_<_ : hPropRel F F ℓ') (min max : F → F → F) (sqrt : (x : F) → {{ ! [ ¬(x < 0f) ] }} → F) : Type (ℓ-max ℓ ℓ') where
  constructor iscompletepartiallyorderedfield
  field
    -- 1. 2. 3. 4. 5. 6. (†) and (∗)
    is-PartiallyOrderedField : [ isPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max ]

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{- Definition of join for ◇ and associated lemmas. -}
module TemporalOps.Diamond.Join where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import TemporalOps.Common
open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond.Functor

import Relation.Binary.PropositionalEquality as ≡
open import Data.Product
open import Relation.Binary.HeterogeneousEquality as ≅
            using (_≅_ ; ≅-to-≡ ; ≡-to-≅ ; cong₂)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

-- | Auxiliary definitions for μ

-- Shifting an event by some interval
μ-shift : {A : τ} -> (k n : ℕ) -> ◇ A at n -> ◇ A at (k + n)
μ-shift {A} k n (l , v) = k + l , rew (sym (delay-+ k l n)) v

-- Auxiliary function for μ, taking the comparison of the delay and
-- time index as an argument
μ-compare : (A : τ) -> (n k : ℕ) -> (v : delay ◇ A by k at n)
         -> LeqOrdering k n -> ◇ A at n
μ-compare A .(k + l) k  v snd==[ .k + l ] =
        μ-shift k l (rew (delay-+-left0 k l) v)
μ-compare A n .(n + suc l) v fst==suc[ .n + l ] =
        n + suc l , rew (delay-⊤ n l) top.tt

private module F-◇ = Functor F-◇

-- Join for ◇
μ-◇ : (F-◇ ²) ⟹ F-◇
μ-◇ = record
    { at = μ-◇-at
    ; nat-cond = λ {A} {B} {f} {n} {a}
                -> μ-◇-nat-cond {A} {B} {f} {n} {a}
    }
    where
    open Functor
    private module F-▹ = Functor F-▹
    open ≡.≡-Reasoning

    -- The order of mapping and shifting of events can be interchanged
    μ-shift-fmap : {A B : τ} {f : A ⇴ B} {k l : ℕ} {a : ◇ A at l}
                -> F-◇.fmap f (k + l) (μ-shift {A} k l a)
                 ≡ μ-shift {B} k l (F-◇.fmap f l a)
    μ-shift-fmap {A} {B} {f} {zero} {l} {j , y} = refl
    μ-shift-fmap {A} {B} {f} {suc k} {l} {j , y}
        rewrite μ-shift-fmap {A} {B} {f} {k} {l} {j , y}
        = cong (λ x → suc k + j , x) (fmap-delay-+-k k j l y)

    -- Join for ◇
    μ-◇-at : (A : τ) -> ◇ ◇ A ⇴ ◇ A
    μ-◇-at A n (k , v) = μ-compare A n k v (compareLeq k n)

    -- Naturality proof
    μ-◇-nat-cond : ∀{A B : τ} {f : A ⇴ B} {n : ℕ} {a : ◇ ◇ A at n}
                -> F-◇.fmap f n (μ-◇-at A n a)
                 ≡ μ-◇-at B n (Functor.fmap (F-◇ ²) f n a)
    μ-◇-nat-cond {A} {B} {f} {n} {k , v} with inspect (compareLeq k n)
    -- n = k + l
    μ-◇-nat-cond {A} {B} {f} {.(k + l)} {k , v} | snd==[ .k + l ] with≡ pf =
        begin
            F-◇.fmap f (k + l) (μ-◇-at A (k + l) (k , v))
        ≡⟨⟩ -- Def. of μ-◇-at
            F-◇.fmap f (k + l) (μ-compare A (k + l) k v ⌞ compareLeq k (k + l) ⌟)
        ≡⟨ cong! pf ⟩
            F-◇.fmap f (k + l) (μ-shift k l (rew (delay-+-left0 k l) v))
        ≡⟨ μ-shift-fmap {_}{_}{_}{k}{l}{(rew (delay-+-left0 k l) v)} ⟩
            μ-shift k l (F-◇.fmap f l ⌞ rew (delay-+-left0 k l) v ⌟)
        ≡⟨ cong! (delay-+-left0-eq k l v v′ v≅v′) ⟩
            μ-shift k l (F-◇.fmap f l (rew (delay-+ k 0 l) v′))
        ≡⟨⟩ -- Def. of (F-delay 0).fmap
            μ-shift k l ((Functor.fmap (F-delay 0) (F-◇.fmap f) at l) (rew (delay-+ k 0 l) v′))
        ≡⟨ cong (λ x → μ-shift k l x) (sym (fmap-delay-+-n+k k 0 l v′)) ⟩
            μ-shift k l ⌞ rew (delay-+ k 0 l) ((Functor.fmap (F-delay (k + 0)) (F-◇.fmap f) at (k + l)) v′) ⌟
        ≡⟨ cong!
            (sym (delay-+-left0-eq k l ((Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v)
                                       ((Functor.fmap (F-delay (k + 0)) (F-◇.fmap f) at (k + l)) v′) pr))
         ⟩
            μ-shift k l (rew (delay-+-left0 k l) ((Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v))
        ≡⟨⟩ -- Def. of μ-compare
            μ-compare B (k + l) k ((Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v) (snd==[ k + l ])
        ≡⟨ cong (λ x → μ-compare B (k + l) k ((Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v) x) (sym pf) ⟩
            μ-compare B (k + l) k ((Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v) (compareLeq k (k + l))
        ≡⟨⟩ -- Folding definitions
            μ-◇-at B (k + l) (fmap (F-◇ ²) f (k + l) (k , v))
        ∎
        where
        v′ : delay (◇ A) by (k + 0) at (k + l)
        v′ = rew (delay-+0-left k (k + l)) v
        v≅v′ : v ≅ v′
        v≅v′ = rew-to-≅ (delay-+0-left k (k + l))
        pr : (Functor.fmap (F-delay k) (F-◇.fmap f) at (k + l)) v
           ≅ (Functor.fmap (F-delay (k + 0)) (F-◇.fmap f) at (k + l)) v′
        pr = cong₂ (λ x y → (Functor.fmap (F-delay x) (F-◇.fmap f) at (k + l)) y)
                (≡-to-≅ (sym (+-identityʳ k))) v≅v′

    -- k = suc n + l
    μ-◇-nat-cond {A} {B} {f} {.n} {.(n + suc l) , v} | fst==suc[ n + l ] with≡ pf =
        begin
            F-◇.fmap f n (μ-◇-at A n (n + suc l , v))
        ≡⟨⟩ -- Def. of μ-◇-at
            F-◇.fmap f n (μ-compare A n (n + suc l) v ⌞ compareLeq (n + suc l) n ⌟)
        ≡⟨ cong! pf ⟩
            F-◇.fmap f n (n + suc l , rew (delay-⊤ n l) top.tt)
        ≡⟨⟩ -- Def. of F-◇.fmap
            n + suc l , (Functor.fmap (F-delay (n + suc l)) f at n) (rew (delay-⊤ n l) top.tt)
        ≡⟨ cong (λ x → n + suc l , x) (eq n l) ⟩
            n + suc l , rew (delay-⊤ n l) top.tt
        ≡⟨⟩ -- Def. of μ-compare
            μ-compare B n (n + suc l) ((Functor.fmap (F-delay ((n + suc l))) (F-◇.fmap f) at n) v) (fst==suc[ n + l ])
        ≡⟨ cong (λ x → μ-compare B n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (F-◇.fmap f) at n) v) x) (sym pf) ⟩
            μ-compare B n (n + suc l) ((Functor.fmap (F-delay (n + suc l)) (F-◇.fmap f) at n) v) (compareLeq (n + suc l) n)
        ≡⟨⟩ -- Def. of μ-◇-at
            μ-◇-at B n (Functor.fmap (F-◇ ²) f n (n + suc l , v))
        ∎
        where
        eq : ∀ (n l : ℕ)
          -> (Functor.fmap (F-delay (n + suc l)) f at n) (rew (delay-⊤ n l) top.tt)
           ≡ rew (delay-⊤ n l) top.tt
        eq zero l = refl
        eq (suc n) l = eq n l

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Issue760 where

module M where
  A : Set₂
  A = Set₁

abstract
  B : Set₁
  B = Set

  open M public  -- Not abstract.

  C : Set₁
  C = F where
    F = Set -- where clauses declare an anonymous open public module
            -- but we should not see any error here

InScope : A
InScope = Set

private
  D : Set₁
  D = Set

  open M public  -- Private & public?!

  E : Set₁
  E = F where
    F = Set -- where clauses declare an anonymous open public module
            -- but we should not see any error here


text:
open import prelude

-- Copied pretty much verbatim

data Term : Set where
  true : Term
  false : Term
  if_then_else_end : Term → Term → Term → Term
  zero : Term
  succ : Term → Term
  iszero : Term → Term

data NValue : Term → Set where
  zero : NValue zero
  succ : ∀ {t} → NValue(t) → NValue(succ t)

data Value : Term → Set where
  true : Value true
  false :  Value false
  nv : ∀ {t} → NValue(t) → Value(t)

data _⟶_ : Term → Term → Set where

  E─IfTrue : ∀ {t₂ t₃} →

    -----------------------------------
    if true then t₂ else t₃ end ⟶ t₂

  E─IfFalse : ∀ {t₂ t₃} →

    -----------------------------------
    if false then t₂ else t₃ end ⟶ t₃

  E─IfCong : ∀ {t₁ t₁′ t₂ t₃} →

    (t₁ ⟶ t₁′) →
    ----------------------------------------------------------
    (if t₁ then t₂ else t₃ end ⟶ if t₁′ then t₂ else t₃ end)

  E─SuccCong : ∀ {t₁ t₁′} →

    (t₁ ⟶ t₁′) →
    ----------------------
    (succ t₁ ⟶ succ t₁′)

  E─IsZero :

    ----------------------
    (iszero zero ⟶ true)

  E─IsSucc : ∀ {n} →

    --------------------------
    (iszero (succ n) ⟶ false)

  E─IsCong : ∀ {t₁ t₁′} →

    (t₁ ⟶ t₁′) →
    --------------------------
    (iszero t₁ ⟶ iszero t₁′)

data Redex  : Term → Set where

  redex : ∀ {t t′} →

    t ⟶ t′ →
    --------
    Redex(t)

-- Types

data Type : Set where
  bool : Type
  nat : Type

data _∈_ : Term → Type → Set where

  T-True :

    -----------
    true ∈ bool

  T-False :

    -----------
    false ∈ bool

  T-If : ∀ {t₁ t₂ t₃ T} →

    t₁ ∈ bool →
    t₂ ∈ T →
    t₃ ∈ T →
    -----------------------------
    if t₁ then t₂ else t₃ end ∈ T

  T-Zero :

    ----------
    zero ∈ nat

  T-Succ : ∀ {t₁} →

    t₁ ∈ nat →
    -------------
    succ t₁ ∈ nat

  T-IsZero : ∀ {t₁} →

    t₁ ∈ nat →
    -------------
    iszero t₁ ∈ bool

-- Proving that well-typed terms stay well-typed

preservation : ∀ {t t′ T} → (t ∈ T) → (t ⟶ t′) → (t′ ∈ T)
preservation (T-If p₁ p₂ p₃) E─IfTrue = p₂
preservation (T-If p₁ p₂ p₃) E─IfFalse = p₃
preservation (T-If p₁ p₂ p₃) (E─IfCong q) = T-If (preservation p₁ q) p₂ p₃
preservation (T-Succ p) (E─SuccCong q) = T-Succ (preservation p q)
preservation (T-IsZero p) E─IsZero = T-True
preservation (T-IsZero p) E─IsSucc = T-False
preservation (T-IsZero p) (E─IsCong q) = T-IsZero (preservation p q)

-- Proving that every term is a value or a redex

data ValueOrRedex : Term → Set where

  value : ∀ {t} →

    (Value(t)) →
    ---------------
    ValueOrRedex(t)

  redex : ∀ {t t′} →

    t ⟶ t′ →
    ---------------
    ValueOrRedex(t)

progress : ∀ {t T} → (t ∈ T) → ValueOrRedex(t)
progress T-True = value true
progress T-False = value false
progress (T-If p₁ p₂ p₃) = helper (progress p₁) p₁ where

  helper : ∀ {t₀ t₁ t₂} → ValueOrRedex(t₀) → t₀ ∈ bool → ValueOrRedex(if t₀ then t₁ else t₂ end)
  helper (value true) p = redex E─IfTrue
  helper (value false) p = redex E─IfFalse
  helper (redex r) p = redex (E─IfCong r)
  helper (value (nv ())) T-True
  helper (value (nv ())) T-False
  helper (value (nv ())) (T-If p p₁ p₂)

progress T-Zero = value (nv zero)
progress (T-Succ p) = helper (progress p) p where

  helper : ∀ {t₀} → ValueOrRedex(t₀) → t₀ ∈ nat → ValueOrRedex(succ t₀)
  helper (value (nv n)) p = value (nv (succ n))
  helper (redex r) p = redex (E─SuccCong r)

progress (T-IsZero p) = helper (progress p) p where

  helper : ∀ {t₀} → ValueOrRedex(t₀) → t₀ ∈ nat → ValueOrRedex(iszero t₀)
  helper (value (nv zero)) p = redex E─IsZero
  helper (value (nv (succ x))) p = redex E─IsSucc
  helper (redex r) p = redex (E─IsCong r)

-- Interpreter

data _⟶*_ : Term → Term → Set where

  done : ∀ {t} →

    --------
    t ⟶* t

  redex : ∀ {t t′ t″} →

    t ⟶ t′ →
    t′ ⟶* t″ →
    ----------
    t ⟶* t″

-- An interpreter result

data Result  : Term → Set where

  result : ∀ {t t′} →

    t ⟶* t′ →
    Value(t′) →
    ---------
    Result(t)

-- The interpreter just calls `progress` until it is a value.
-- This might bot terminate!

{-# NON_TERMINATING #-}
interp : ∀ {t T} → (t ∈ T) → Result(t)
interp p = helper₂ p (progress p) where

  helper₁ : ∀ {t t′} → (t ⟶ t′) → Result(t′) → Result(t)
  helper₁ r (result s v) = result (redex r s) v

  helper₂ : ∀ {t T} → (t ∈ T) → ValueOrRedex(t) → Result(t)
  helper₂ p (value v) = result done v
  helper₂ p (redex r) = helper₁ r (interp (preservation p r))

ex = if (iszero zero) then (succ zero) else (zero) end

exNat : (ex ∈ nat)
exNat = T-If (T-IsZero T-Zero) (T-Succ T-Zero) T-Zero

-- Normalize (C-N) interp exNat
-- result
--   (redex (E─IfCong E─IsZero)
--     (redex E─IfTrue
--       done))
--   (nv (succ zero))

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
------------------------------------------------------------------------
-- A definition of the propositional truncation operator that does not
-- use recursive higher inductive types
------------------------------------------------------------------------

-- The definition does use natural numbers. The code is based on van
-- Doorn's "Constructing the Propositional Truncation using
-- Non-recursive HITs".

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

import Equality.Path as P

module H-level.Truncation.Propositional.Non-recursive
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

private
  open module PD = P.Derived-definitions-and-properties eq
    hiding (elim)

open import Prelude

open import Colimit.Sequential eq as C using (Colimit)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F
open import H-level equality-with-J
open import H-level.Closure equality-with-J
import H-level.Truncation.Propositional eq as T
open import H-level.Truncation.Propositional.Non-recursive.Erased eq
  as N using (∥_∥ᴱ)
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹; ∥_∥¹-out-^; ∣_∣-out-^)

private
  variable
    a p : Level
    A B : Type a
    P   : A → Type p
    e x : A

-- The propositional truncation operator.

∥_∥ : Type a → Type a
∥ A ∥ = Colimit ∥ A ∥¹-out-^ O.∣_∣

-- The point constructor.

∣_∣ : A → ∥ A ∥
∣_∣ = C.∣_∣

-- The eliminator.

record Elim {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ             : ∀ x → P ∣ x ∣
    is-propositionʳ : ∀ x → Is-proposition (P x)

open Elim public

elim : Elim P → (x : ∥ A ∥) → P x
elim {A = A} {P = P} e = C.elim λ where
    .C.Elim.∣∣ʳ {n = n} → helper n
    .C.Elim.∣∣≡∣∣ʳ _    → E.is-propositionʳ _ _ _
  where
  module E = Elim e

  helper : ∀ n (x : ∥ A ∥¹-out-^ n) → P C.∣ x ∣
  helper zero    = E.∣∣ʳ
  helper (suc n) = O.elim λ where
    .O.Elim.∣∣ʳ x            → subst P (sym (C.∣∣≡∣∣ x)) (helper n x)
    .O.Elim.∣∣-constantʳ _ _ → E.is-propositionʳ _ _ _

_ : elim e ∣ x ∣ ≡ e .∣∣ʳ x
_ = refl _

-- The propositional truncation operator returns propositions.

∥∥-proposition : Is-proposition ∥ A ∥
∥∥-proposition {A = A} = elim λ where
    .is-propositionʳ → Π≡-proposition ext
    .∣∣ʳ x → C.elim λ where
      .C.Elim.∣∣ʳ              → lemma₁ _ x
      .C.Elim.∣∣≡∣∣ʳ {n = n} y →
        subst (∣ x ∣ ≡_) (C.∣∣≡∣∣ y) (lemma₁ (suc n) x O.∣ y ∣)   ≡⟨ sym trans-subst ⟩

        trans (lemma₁ (1 + n) x O.∣ y ∣) (C.∣∣≡∣∣ y)              ≡⟨⟩

        trans (trans (sym (trans (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n)))
                             (lemma₀ (1 + n) x)))
                 (trans (cong C.∣_∣
                           (O.∣∣-constant
                              (∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
                    (C.∣∣≡∣∣ O.∣ y ∣)))
          (C.∣∣≡∣∣ y)                                             ≡⟨ trans (cong (λ eq → trans (trans eq
                                                                                (trans (cong C.∣_∣ (O.∣∣-constant _ _))
                                                                                (C.∣∣≡∣∣ _)))
                                                                                (C.∣∣≡∣∣ _)) $
                                                                            sym-trans _ _) $
                                                                     trans (trans-assoc _ _ _) $
                                                                     trans (trans-assoc _ _ _) $
                                                                     cong (trans (sym (lemma₀ (1 + n) _))) $
                                                                     sym $ trans-assoc _ _ _ ⟩
        trans (sym (lemma₀ (1 + n) x))
          (trans (trans (sym (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n))))
                    (trans (cong C.∣_∣
                              (O.∣∣-constant
                                 (∣ x ∣-out-^ (1 + n)) O.∣ y ∣))
                       (C.∣∣≡∣∣ O.∣ y ∣)))
             (C.∣∣≡∣∣ y))                                         ≡⟨ cong (λ eq → trans (sym (lemma₀ (1 + n) _))
                                                                                (trans (trans (sym (C.∣∣≡∣∣ _)) eq) (C.∣∣≡∣∣ _))) $ sym $
                                                                     lemma₂ _ _ _ _ _ ⟩
        trans (sym (lemma₀ (1 + n) x))
          (trans (trans (sym (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n))))
                    (trans (C.∣∣≡∣∣ (∣ x ∣-out-^ (1 + n)))
                       (cong C.∣_∣ (O.∣∣-constant _ _))))
             (C.∣∣≡∣∣ y))                                         ≡⟨ cong (λ eq → trans (sym (lemma₀ (1 + n) _)) (trans eq (C.∣∣≡∣∣ _))) $
                                                                     trans-sym-[trans] _ _ ⟩
        trans (sym (lemma₀ (1 + n) x))
          (trans (cong C.∣_∣ (O.∣∣-constant _ _)) (C.∣∣≡∣∣ y))    ≡⟨⟩

        lemma₁ n x y                                              ∎
  where
  lemma₀ : ∀ n (x : A) → C.∣ ∣ x ∣-out-^ n ∣ ≡ ∣ x ∣
  lemma₀ zero    x = ∣ x ∣  ∎
  lemma₀ (suc n) x =
    C.∣ O.∣ ∣ x ∣-out-^ n ∣ ∣  ≡⟨ C.∣∣≡∣∣ (∣ x ∣-out-^ n) ⟩
    C.∣ ∣ x ∣-out-^ n ∣        ≡⟨ lemma₀ n x ⟩∎
    ∣ x ∣                      ∎

  lemma₁ : ∀ n (x : A) (y : ∥ A ∥¹-out-^ n) → ∣ x ∣ ≡ C.∣ y ∣
  lemma₁ n x y =
    ∣ x ∣                      ≡⟨ sym (lemma₀ (suc n) x) ⟩
    C.∣ ∣ x ∣-out-^ (suc n) ∣  ≡⟨⟩
    C.∣ O.∣ ∣ x ∣-out-^ n ∣ ∣  ≡⟨ cong C.∣_∣ (O.∣∣-constant _ _) ⟩
    C.∣ O.∣ y ∣ ∣              ≡⟨ C.∣∣≡∣∣ y ⟩∎
    C.∣ y ∣                    ∎

  lemma₂ :
    ∀ n (x y : ∥ A ∥¹-out-^ n) (p : x ≡ y) (q : O.∣ x ∣ ≡ O.∣ y ∣) →
    trans (C.∣∣≡∣∣ {P = ∥ A ∥¹-out-^} x) (cong C.∣_∣ p) ≡
    trans (cong C.∣_∣ q) (C.∣∣≡∣∣ y)
  lemma₂ n x y p q =
    trans (C.∣∣≡∣∣ x) (cong C.∣_∣ p)                        ≡⟨ PD.elim
                                                                 (λ {x y} p → trans (C.∣∣≡∣∣ x) (cong C.∣_∣ p) ≡
                                                                              trans (cong C.∣_∣ (cong O.∣_∣ p)) (C.∣∣≡∣∣ y))
                                                                 (λ x →
      trans (C.∣∣≡∣∣ x) (cong C.∣_∣ (refl _))                       ≡⟨ cong (trans _) $ cong-refl _ ⟩
      trans (C.∣∣≡∣∣ x) (refl _)                                    ≡⟨ trans-reflʳ _ ⟩
      C.∣∣≡∣∣ x                                                     ≡⟨ sym $ trans-reflˡ _ ⟩
      trans (refl _) (C.∣∣≡∣∣ x)                                    ≡⟨ cong (flip trans _) $ sym $
                                                                       trans (cong (cong C.∣_∣) $ cong-refl _) $
                                                                       cong-refl _ ⟩∎
      trans (cong C.∣_∣ (cong O.∣_∣ (refl _))) (C.∣∣≡∣∣ x)          ∎)
                                                                 p ⟩

    trans (cong C.∣_∣ (cong O.∣_∣ p)) (C.∣∣≡∣∣ y)           ≡⟨ cong (flip trans _) $
                                                               cong-preserves-Constant
                                                                 (λ u v →
      C.∣ u ∣                                                       ≡⟨ sym (C.∣∣≡∣∣ u) ⟩
      C.∣ O.∣ u ∣ ∣                                                 ≡⟨ cong C.∣_∣ (O.∣∣-constant _ _) ⟩
      C.∣ O.∣ v ∣ ∣                                                 ≡⟨ C.∣∣≡∣∣ v ⟩∎
      C.∣ v ∣                                                       ∎)
                                                                 _ _ ⟩∎
    trans (cong C.∣_∣ q) (C.∣∣≡∣∣ y)                        ∎

-- ∥_∥ is pointwise equivalent to T.∥_∥.

∥∥≃∥∥ : ∥ A ∥ ≃ T.∥ A ∥
∥∥≃∥∥ = Eq.⇔→≃
  ∥∥-proposition
  T.truncation-is-proposition
  (elim λ where
     .∣∣ʳ               → T.∣_∣
     .is-propositionʳ _ → T.truncation-is-proposition)
  (T.rec ∥∥-proposition ∣_∣)

-- Functions from T.∥ A ∥ can be expressed as families of functions
-- from ∥ A ∥¹-out-^ that satisfy a certain property.

∥∥→≃ :
  (T.∥ A ∥ → B)
    ≃
  (∃ λ (f : ∀ n → ∥ A ∥¹-out-^ n → B) →
     ∀ n x → f (suc n) O.∣ x ∣ ≡ f n x)
∥∥→≃ {A = A} {B = B} =
  (T.∥ A ∥ → B)                          ↝⟨ →-cong ext (inverse ∥∥≃∥∥) F.id ⟩

  (∥ A ∥ → B)                            ↝⟨ C.universal-property ⟩□

  (∃ λ (f : ∀ n → ∥ A ∥¹-out-^ n → B) →
     ∀ n x → f (suc n) O.∣ x ∣ ≡ f n x)  □

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

-- ∥ A ∥ᴱ implies ∥ A ∥.

∥∥ᴱ→∥∥ : ∥ A ∥ᴱ → ∥ A ∥
∥∥ᴱ→∥∥ = N.elim λ where
  .N.∣∣ʳ               → ∣_∣
  .N.is-propositionʳ _ → ∥∥-proposition

-- In erased contexts ∥ A ∥ᴱ and ∥ A ∥ are equivalent.

@0 ∥∥ᴱ≃∥∥ : ∥ A ∥ᴱ ≃ ∥ A ∥
∥∥ᴱ≃∥∥ = Eq.↔→≃
  ∥∥ᴱ→∥∥
  (elim λ @0 where
     .∣∣ʳ               → N.∣_∣
     .is-propositionʳ _ → N.∥∥ᴱ-proposition)
  (elim λ @0 where
     .∣∣ʳ _             → refl _
     .is-propositionʳ _ → mono₁ 1 ∥∥-proposition)
  (N.elim λ where
     .N.∣∣ʳ _             → refl _
     .N.is-propositionʳ _ → mono₁ 1 N.∥∥ᴱ-proposition)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

module Math.FormalLanguage where

-- agda-stdlib
import Algebra.FunctionProperties as FP
import Algebra.Structures as Structures
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.List as L using (List; []; _++_)
import Data.List.Properties as Lₚ
open import Data.Nat hiding (_⊔_; _^_)
open import Data.Empty
open import Data.Product using (proj₁; proj₂; _,_; _×_; ∃₂; ∃)
open import Function using (_$_)
import Function as F
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Unary hiding (∅; ｛_｝)
import Relation.Unary as U
import Relation.Unary.Properties as Uₚ

-- Equivalence of predicate
infix 4 _≡ᴾ_
_≡ᴾ_ : ∀ {a l} {A : Set a} → Rel (Pred A l) (a ⊔ l)
_≡ᴾ_ P Q = (P ⊆ Q) × (Q ⊆ P)

≡ᴾ-refl : ∀ {a l} {A : Set a} → Reflexive {A = Pred A l} _≡ᴾ_
≡ᴾ-refl = F.id , F.id

≡ᴾ-sym : ∀ {a l} {A : Set a} → Symmetric {A = Pred A l} _≡ᴾ_
≡ᴾ-sym = Data.Product.swap

≡ᴾ-trans : ∀ {a l} {A : Set a} → Transitive {A = Pred A l} _≡ᴾ_
≡ᴾ-trans P≡Q Q≡R = proj₁ Q≡R F.∘ proj₁ P≡Q , proj₂ P≡Q F.∘ proj₂ Q≡R

≡ᴾ-isEquivalence : ∀ {a l} {A : Set a} → IsEquivalence {A = Pred A l} _≡ᴾ_
≡ᴾ-isEquivalence = record
  { refl  = ≡ᴾ-refl
  ; sym   = ≡ᴾ-sym
  ; trans = ≡ᴾ-trans
  }

≡ᴾ-setoid : ∀ {a l} {A : Set a} → Setoid _ _
≡ᴾ-setoid {a} {l} {A} = record
  { Carrier       = Pred A l
  ; _≈_           = _≡ᴾ_
  ; isEquivalence = ≡ᴾ-isEquivalence
  }

∅ : ∀ {a l} {A : Set a} → Pred A l
∅ {l = l} = λ _ → Lift l ⊥

｛_｝ : ∀ {a l} {A : Set a} → A → Pred A (a ⊔ l)
｛_｝{l = l} x = λ y → Lift l (y ≡ x)

Lang : ∀ {s} → Set s → (l : Level) → Set _
Lang Σ l = Pred (List Σ) l

-- TODO Move Math.FormalLanguage.Construct.EmptyLang
data EmptyLang {a l} {A : Set a} : Lang A (a ⊔ l) where
  mkEmptyLang : EmptyLang []

-- TODO Move Math.FormalLanguage.Construct.Concat
-- TODO Hetero
-- Lang A l → Lang B l → Lang (A ⊎ B) l
-- map inj₁ xs ++ map inj₂ ys
-- concatenation of formal language
data _<>_ {a l} {A : Set a} (L₁ L₂ : Lang A l) : Lang A (a ⊔ l) where
  mk<> : ∀ {xs ys} → L₁ xs → L₂ ys → (L₁ <> L₂) (xs ++ ys)

-- TODO Move Math.FormalLanguage.Construct.Concat.Properties
module _ {s l} {Σ : Set s} where
  open FP {A = Lang Σ (s ⊔ l)} _≡ᴾ_

  <>-identityˡ : LeftIdentity (EmptyLang {l = l}) _<>_
  <>-identityˡ L = to , from
    where
    to : EmptyLang <> L ⊆ L
    to (mk<> mkEmptyLang x₁) = x₁
    from : L ⊆ EmptyLang <> L
    from Lx = mk<> mkEmptyLang Lx

  <>-identityʳ  : RightIdentity (EmptyLang {l = l}) _<>_
  <>-identityʳ L = to , from
    where
    to : L <> EmptyLang ⊆ L
    to (mk<> Lx mkEmptyLang) = subst L (sym $ Lₚ.++-identityʳ _) Lx
    from : L ⊆ L <> EmptyLang
    from {xs} x = subst (L <> EmptyLang) (Lₚ.++-identityʳ xs) $
      mk<> {xs = xs} {ys = []} x mkEmptyLang

{- TODO move contents of agda-combinatorics to agda-misc
  <>-dec : ∀ {L₁ L₂ : Lang Σ l} →
    U.Decidable L₁ → U.Decidable L₂ → U.Decidable (L₁ <> L₂)
  <>-dec L₁? L₂? zs with L.filter (L₁? Uₚ.×? L₂?) (splits₂ zs)
  ... | x = ?
-}


text:
module Everything where

import Data.BitVector
import Data.BitVector.ContainmentOrder
import Data.BitVector.NumericOrder
import Data.BitVector.Peano
import Data.BitVector.Properties
import Data.BitVector.Properties.LatticeProperties

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
module objectsInAgda where

open import Data.Product
open import interactiveProgramsAgda hiding (main)
open import NativeIO
open import Data.String.Base

record Interface  :  Set₁ where
  field  Method   :  Set
         Result   :  (m : Method) → Set

open Interface public

record Object (I : Interface) : Set where
  coinductive
  field objectMethod : (m : Method I) → Result I m × Object I

open Object public
open import Size

record IOObject (Iᵢₒ : IOInterface) (I : Interface) (i : Size) : Set where
  coinductive
  field method : ∀{j : Size< i} (m : Method I)
                   → IO Iᵢₒ ∞ (Result I m × IOObject Iᵢₒ I j)

open IOObject public

{- Example Cell -}

data CellMethod A : Set where
    get  :  CellMethod A
    put  :  A → CellMethod A

CellResult             :  ∀{A} → CellMethod A → Set
CellResult   {A} get   =  A
CellResult   (put _)   =  Unit

cellI                  :  (A : Set) → Interface
Method    (cellI A)    =  CellMethod A
Result    (cellI A) m  =  CellResult m

{- A cell as an Object -}

Cell : Set → Set
Cell A = Object (cellI A)

cell : {A : Set} → A → Cell A
objectMethod (cell a) get       = a    , cell a
objectMethod (cell a) (put a')  = unit , cell a'

{- A cell as an IOObject -}

CellC : (i : Size) → Set
CellC = IOObject ConsoleInterface (cellI String)

simpleCell : ∀{i} (s : String) → CellC i
force (method (simpleCell s)  get) =
  do' (putStrLn ("getting (" ++ s ++ ")")) λ _ →
  return (s , simpleCell s)
force (method (simpleCell _) (put s)) =
  do' (putStrLn ("putting (" ++ s ++ ")")) λ _ →
  return (_ , simpleCell s)

program : ∀{i} → CellC ∞  → IO ConsoleInterface i Unit
force (program c) =
  do' getLine          λ s →
  method c (put s)    >>= λ{ (_ , c) →
  method c get        >>= λ{ (s' , c) →
  do (putStrLn s')     λ _ →
  program c }}

main : NativeIO Unit
main = translateIOConsole (program (simpleCell "Start"))

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module trichotomy where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)

open import Negation using (¬_; _≢_)

infix 4 _<_
data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

infix 4 _≮_
_≮_ : ∀ (m n : ℕ) → Set
m ≮ n = ¬ (m < n)

-- 1 + m ≡ 1 + n ならば m ≡ n
sm≡sn→m≡n : ∀ {m n : ℕ} → suc m ≡ suc n → m ≡ n
sm≡sn→m≡n refl = refl

-- m ≢ n ならば 1 + m ≢ 1 + n
m≢n→sm≢sn : ∀ {m n : ℕ} → m ≢ n → suc m ≢ suc n
m≢n→sm≢sn m≢n = λ{ sm≡sn → m≢n (sm≡sn→m≡n sm≡sn) }

-- m ≮ n ならば 1 + m ≮ 1 + n
m≮n→sm≮sn : ∀ {m n : ℕ} → m ≮ n → suc m ≮ suc n
m≮n→sm≮sn m≮n = λ{ (s<s m<n) → m≮n m<n }

-- 三分律の証明
trichotomy : ∀ (m n : ℕ)
  → (m < n × m ≢ n × n ≮ m)
  ⊎ (m ≮ n × m ≡ n × n ≮ m)
  ⊎ (m ≮ n × m ≢ n × n < m)
trichotomy zero    zero                                              = inj₂ (inj₁ ⟨ (λ()) , ⟨ refl , (λ()) ⟩ ⟩)
trichotomy zero    (suc n)                                           = inj₁ ⟨ z<s , ⟨ (λ()) , (λ()) ⟩ ⟩
trichotomy (suc m) zero                                              = inj₂ (inj₂ ⟨ (λ()) , ⟨ (λ()) , z<s ⟩ ⟩)
trichotomy (suc m) (suc n) with trichotomy m n
...                           | inj₁ ⟨ m<n , ⟨ m≢n , n≮m ⟩ ⟩         = inj₁ ⟨ s<s m<n , ⟨ m≢n→sm≢sn m≢n , m≮n→sm≮sn n≮m ⟩ ⟩
...                           | inj₂ (inj₁ ⟨ m≮n , ⟨ refl , n≮m ⟩ ⟩) = inj₂ (inj₁ ⟨ m≮n→sm≮sn m≮n , ⟨ refl , m≮n→sm≮sn n≮m ⟩ ⟩)
...                           | inj₂ (inj₂ ⟨ m≮n , ⟨ m≢n , n<m ⟩ ⟩)  = inj₂ (inj₂ ⟨ m≮n→sm≮sn m≮n , ⟨ m≢n→sm≢sn m≢n , s<s n<m ⟩ ⟩)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
open import Lemmachine.Resource
module Lemmachine.Resolve (c : Resource) where
open import Lemmachine.Request
open import Lemmachine.Response
open import Lemmachine.Utils
open import Data.Bool
open import Data.Nat
open import Data.String
open import Data.Function
open import Data.Maybe
open import Data.List
open import Data.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

O18 : Request → Status
O18 r with Resource.multipleChoices c r
... | false = OK
... | true  = MultipleChoices

O20 : Request → Status
O20 r with Request.reqBody r
... | nothing = NoContent
... | just _ = O18 r

P11 : Request → Status
P11 r with fetchHeader "Location" (Request.headers r)
... | nothing = O20 r
... | just _  = Created

O14 : Request → Status
O14 r with Resource.isConflict c r
... | true  = Conflict
... | false = P11 r

O16 : Request → Status
O16 r with Request.method r
... | PUT = O14 r
... | _ = O18 r

N11 : Request → Status
N11 r with isRedirect r
... | true  = SeeOther
... | false = P11 r

N16 : Request → Status
N16 r with Request.method r
... | POST = N11 r
... | _ = O16 r

M20 : Request → Status
M20 r with Resource.deleteResource c r
... | false = Accepted
... | true = O20 r

M16 : Request → Status
M16 r with Request.method r
... | DELETE = M20 r
... | _ = N16 r

L13+L14+L15+L17 : Request → Status
L13+L14+L15+L17 r with fetchHeader "If-Modified-Since" (Request.headers r)
... | nothing = M16 r
... | just clientDate with isDate clientDate
... | false = M16 r
... | true with isModified now clientDate
... | true = M16 r
... | false with Resource.lastModified c r
... | nothing = M16 r
... | just serverDate with isModified clientDate serverDate
... | true = M16 r
... | false = NotModified

J18 : Request → Status
J18 r with Request.method r
... | HEAD = NotModified
... | GET  = NotModified
... | _    = PreconditionFailed

I12+I13+K13 : Request → Status
I12+I13+K13 r with fetchHeader "If-None-Match" (Request.headers r)
... | nothing = L13+L14+L15+L17 r
... | just clientETag with "*" == clientETag
... | true = J18 r
... | false with Resource.generateETag c r
... | nothing = L13+L14+L15+L17 r
... | just serverETag with clientETag == serverETag
... | true = J18 r
... | false = L13+L14+L15+L17 r

H10+H11+H12 : Request → Status
H10+H11+H12 r with fetchHeader "If-Unmodified-Since" (Request.headers r)
... | nothing = I12+I13+K13 r
... | just clientDate with isDate clientDate
... | false = I12+I13+K13 r
... | true  with Resource.lastModified c r
... | nothing = I12+I13+K13 r
... | just serverDate with isModified clientDate serverDate
... | true = PreconditionFailed
... | false = I12+I13+K13 r

G8+G9+G11 : Request → Status
G8+G9+G11 r with fetchHeader "If-Match" (Request.headers r)
... | nothing = H10+H11+H12 r
... | just clientETag with "*" == clientETag
... | true  = H10+H11+H12 r
... | false with Resource.generateETag c r
... | nothing = PreconditionFailed
... | just serverETag with clientETag == serverETag
... | true = H10+H11+H12 r
... | false = PreconditionFailed

I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 : Request → Status
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r   with Request.method r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | PUT    with Resource.movedPermanently c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | PUT  | just _  = MovedPermanently
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | PUT  | nothing   with Resource.isConflict c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | PUT  | nothing | false   = N11 r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | PUT  | nothing | true    = Conflict
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | _      with Resource.previouslyExisted c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | _    | true      with Resource.movedPermanently c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | _    | true    | just _  = MovedPermanently
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | _    | true    | nothing   with Resource.movedTemporarily c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | _    | true    | nothing | just _  = MovedTemporarily
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | POST | true    | nothing | nothing   with Resource.allowMissingPost c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | POST | true    | nothing | nothing | false = Gone
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | POST | true    | nothing | nothing | true  = N11 r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | _    | true    | nothing | nothing = Gone
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | POST | false     with Resource.allowMissingPost c r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | POST | false   | false = NotFound
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r | POST | false   | true  = N11 r
I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 _ | _    | false   = NotFound

H7 : Request → Status
H7 r with fetchHeader "If-Match" (Request.headers r)
... | just "*"  = PreconditionFailed
... | _ = I7+I4+P3+K7+K5+L5+M5+N5+L7+M7 r

G7 : Request → Status
G7 r with Resource.resourceExists c r
... | true  = G8+G9+G11 r
... | false = H7 r

F6+F7 : Request → Status
F6+F7 r with fetchHeader "Accept-Encoding" (Request.headers r)
... | nothing = G7 r
... | just encoding with fetch encoding (Resource.encodingsProvided c r)
... | just _  = G7 r
... | nothing = NotAcceptable

E5+E6 : Request → Status
E5+E6 r with fetchHeader "Accept-Charset" (Request.headers r)
... | nothing = F6+F7 r
... | just charset with fetch charset (Resource.charsetsProvided c r)
... | just _  = F6+F7 r
... | nothing = NotAcceptable

D4+D5 : Request → Status
D4+D5 r with fetchHeader "Accept-Language" (Request.headers r)
... | nothing = E5+E6 r
... | just language with Resource.languageAvailable c r
... | true    = E5+E6 r
... | false   = NotAcceptable

C3+C4 : Request → Status
C3+C4 r with fetchHeader "Accept" (Request.headers r)
... | nothing = D4+D5 r
... | just contentType with fetchContentType contentType
                              (Resource.contentTypesProvided c r)
... | just _  = D4+D5 r
... | nothing = NotAcceptable

B3 : Request → Status
B3 r with eqMethod (Request.method r) OPTIONS
... | true  = OK
... | false = C3+C4 r

B4 : Request → Status
B4 r with Resource.validEntityLength c r
... | true  = B3 r
... | false = RequestEntityTooLarge

B5 : Request → Status
B5 r with Resource.knownContentType c r
... | true  = B4 r
... | false = UnsupportedMediaType

B6 : Request → Status
B6 r with Resource.validContentHeaders c r
... | true  = B5 r
... | false = NotImplemented

B7 : Request → Status
B7 r with Resource.forbidden c r
... | true  = Forbidden
... | false = B6 r

B8 : Request → Status
B8 r with Resource.isAuthorized c r
... | true  = B7 r
... | false = Unauthorized

B9 : Request → Status
B9 r with Resource.malformedRequest c r
... | true  = BadRequest
... | false = B8 r

B10 : Request → Status
B10 r with any (eqMethod (Request.method r))
               (Resource.allowedMethods c r)
... | true  = B9 r
... | false = MethodNotAllowed

B11 : Request → Status
B11 r with Resource.uriTooLong c r
... | true  = RequestURItooLong
... | false = B10 r

B12 : Request → Status
B12 r with any (eqMethod (Request.method r))
               (Resource.knownMethods c r)
... | true  = B11 r
... | false = NotImplemented

B13 : Request → Status
B13 r with Resource.serviceAvailable c r
... | true  = B12 r
... | false = ServiceUnavailable

resolveStatus : Request → Status
resolveStatus r = B13 r

resolve : Application
resolve r = record {
    status = s
  ; headers = hs $ fetchAccept (Request.headers r) (Resource.contentTypesProvided c r)
  ; body = Resource.body c s
  } where
  s = resolveStatus r
  hs : Maybe String → List ResponseHeader
  hs (just s) = [ "Content-Type" , s ]
  hs nothing = []

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Definition.Typed.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties

-- Weak head expansion of type equality
reduction : ∀ {A A′ B B′ Γ}
          → Γ ⊢ A ⇒* A′
          → Γ ⊢ B ⇒* B′
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A′ ≡ B′
          → Γ ⊢ A ≡ B
reduction D D′ whnfA′ whnfB′ A′≡B′ =
  trans (subset* D) (trans A′≡B′ (sym (subset* D′)))

reduction′ : ∀ {A A′ B B′ Γ}
          → Γ ⊢ A ⇒* A′
          → Γ ⊢ B ⇒* B′
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A ≡ B
          → Γ ⊢ A′ ≡ B′
reduction′ D D′ whnfA′ whnfB′ A≡B =
  trans (sym (subset* D)) (trans A≡B (subset* D′))

-- Weak head expansion of term equality
reductionₜ : ∀ {a a′ b b′ A B Γ}
           → Γ ⊢ A ⇒* B
           → Γ ⊢ a ⇒* a′ ∷ B
           → Γ ⊢ b ⇒* b′ ∷ B
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a′ ≡ b′ ∷ B
           → Γ ⊢ a ≡ b ∷ A
reductionₜ D d d′ whnfB whnfA′ whnfB′ a′≡b′ =
  conv (trans (subset*Term d)
              (trans a′≡b′ (sym (subset*Term d′))))
       (sym (subset* D))

reductionₜ′ : ∀ {a a′ b b′ A B Γ}
           → Γ ⊢ A ⇒* B
           → Γ ⊢ a ⇒* a′ ∷ B
           → Γ ⊢ b ⇒* b′ ∷ B
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a ≡ b ∷ A
           → Γ ⊢ a′ ≡ b′ ∷ B
reductionₜ′ D d d′ whnfB whnfA′ whnfB′ a≡b =
  trans (sym (subset*Term d))
        (trans (conv a≡b (subset* D)) (subset*Term d′))


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Vectors
open import Semirings.Definition
open import Categories.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Examples
open import Groups.Homomorphisms.Lemmas
open import Functions

module Categories.Examples where

SET : {a : _} → Category {lsuc a} {a}
Category.objects (SET {a}) = Set a
Category.arrows (SET {a}) = λ a b → (a → b)
Category.id (SET {a}) = λ x → λ y → y
Category._∘_ (SET {a}) = λ f g → λ x → f (g x)
Category.rightId (SET {a}) = λ f → refl
Category.leftId (SET {a}) = λ f → refl
Category.compositionAssociative (SET {a}) = λ f g h → refl

GROUP : {a b : _} → Category {lsuc a ⊔ lsuc b} {a ⊔ b}
Category.objects (GROUP {a} {b}) = Sg (Set a) (λ A → Sg (A → A → A) (λ _+_ → Sg (Setoid {a} {b} A) (λ S → Group S _+_)))
Category.arrows (GROUP {a}) (A , (_+A_ , (S , G))) (B , (_+B_ , (T , H))) = Sg (A → B) (GroupHom G H)
Category.id (GROUP {a}) (A , (_+A_ , (S , G))) = (λ i → i) , identityHom G
Category._∘_ (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} {C , (_+C_ , (U , I))} (f , fHom) (g , gHom) = (f ∘ g) , groupHomsCompose gHom fHom
Category.rightId (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} (f , fHom) = {!!}
Category.leftId (GROUP {a}) {A , (_+A_ , (S , G))} {B , (_+B_ , (T , H))} (f , fHom) = {!!}
Category.compositionAssociative (GROUP {a}) = {!!}

DISCRETE : {a : _} (X : Set a) → Category {a} {a}
Category.objects (DISCRETE X) = X
Category.arrows (DISCRETE X) = λ a b → a ≡ b
Category.id (DISCRETE X) = λ x → refl
Category._∘_ (DISCRETE X) = λ y=z x=y → transitivity x=y y=z
Category.rightId (DISCRETE X) refl = refl
Category.leftId (DISCRETE X) refl = refl
Category.compositionAssociative (DISCRETE X) refl refl refl = refl


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.RingSolver.RingExpression where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base
open import Cubical.Algebra.RingSolver.AlmostRing
open import Cubical.Algebra.RingSolver.RawRing renaming (⟨_⟩ to ⟨_⟩ᵣ)

private
  variable
    ℓ : Level

infixl 6 _⊕_
infixl 7 _⊗_

-- Expression in a ring on A with n variables
data Expr {ℓ} (A : Type ℓ) (n : ℕ) : Type ℓ where
  K : A → Expr A n
  ∣ : Fin n → Expr A n
  _⊕_ : Expr A n → Expr A n → Expr A n
  _⊗_ : Expr A n → Expr A n → Expr A n
--  _⊛_ : Expr A n → ℕ → Expr A n    -- exponentiation
  ⊝_ : Expr A n → Expr A n

module Eval (R : RawRing {ℓ}) where
  open import Cubical.Data.Vec
  open RawRing R

  ⟦_⟧ : ∀ {n} → Expr ⟨ R ⟩ᵣ n → Vec ⟨ R ⟩ᵣ n → ⟨ R ⟩ᵣ
  ⟦ K r ⟧ v = r
  ⟦ ∣ k ⟧ v = lookup k v
  ⟦ x ⊕ y ⟧ v =  ⟦ x ⟧ v + ⟦ y ⟧ v
  ⟦ x ⊗ y ⟧ v = ⟦ x ⟧ v · ⟦ y ⟧ v
--  ⟦ x ⊛ l ⟧ v =  ⟦ x ⟧ v ^ l
  ⟦ ⊝ x ⟧ v = - ⟦ x ⟧ v

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:
-- The <local hints> in an ATP pragma <prove> can be functions.

module ATPLocalHints3 where

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

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

1-N : N (succ zero)
1-N = sN zN

postulate
  2-N : N (succ (succ zero))
{-# ATP prove 2-N 1-N #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --prop --rewriting --confluence-check #-}

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ; _+_ to _+ℕ_)

infix 4 _≐_
data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  refl : x ≐ x

{-# BUILTIN REWRITE _≐_ #-}

variable
  ℓ : Level
  A B C : Set ℓ
  x y z : A

cong : (f : A → B) → x ≐ y → f x ≐ f y
cong f refl = refl

data ℤ : Set where
  zero : ℤ
  pred suc : ℤ → ℤ

postulate
  pred-suc : (x : ℤ) → pred (suc x) ≐ x
  suc-pred : (x : ℤ) → suc (pred x) ≐ x

{-# REWRITE pred-suc suc-pred #-}

count-suc : ℤ → ℕ
count-suc zero = 0
count-suc (pred x) = count-suc x
count-suc (suc x) = 1 +ℕ count-suc x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Equality

test : (A : Set) (x y : A) → x ≡ y → Set
test A .y y refl with A
test A .y y refl | X = ?

-- Jesper, 2018-12-03, issue #2892:
-- Error message is:
--    Ill-typed pattern after with abstraction:  y
--    (perhaps you can replace it by `_`?)
--    when checking that the clause ;Issue2892.with-14 A X y = ? has type
--    (A w : Set) (x : w) → Set
-- Implementing the suggestion makes the code typecheck, so this
-- behaviour is at least not obviously wrong.


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommAlgebra.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommAlgebra.Base

open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

-- An R-algebra is the same as a CommRing A with a CommRingHom φ : R → A
module CommAlgChar (R : CommRing ℓ) where
 open Iso
 open IsRingHom
 open CommRingTheory

 CommRingWithHom : Type (ℓ-suc ℓ)
 CommRingWithHom = Σ[ A ∈ CommRing ℓ ] CommRingHom R A

 toCommAlg : CommRingWithHom → CommAlgebra R ℓ
 toCommAlg (A , φ , φIsHom) = ⟨ A ⟩ , ACommAlgStr
  where
  open CommRingStr (snd A)
  ACommAlgStr : CommAlgebraStr R ⟨ A ⟩
  CommAlgebraStr.0a ACommAlgStr = 0r
  CommAlgebraStr.1a ACommAlgStr = 1r
  CommAlgebraStr._+_ ACommAlgStr = _+_
  CommAlgebraStr._·_ ACommAlgStr = _·_
  CommAlgebraStr.- ACommAlgStr = -_
  CommAlgebraStr._⋆_ ACommAlgStr r a = (φ r) · a
  CommAlgebraStr.isCommAlgebra ACommAlgStr = makeIsCommAlgebra
   is-set +Assoc +Rid +Rinv +Comm ·Assoc ·Lid ·Ldist+ ·Comm
   (λ _ _ x → cong (λ y →  y · x) (pres· φIsHom _ _) ∙ sym (·Assoc _ _ _))
   (λ _ _ x → cong (λ y → y · x) (pres+ φIsHom _ _) ∙ ·Ldist+ _ _ _)
   (λ _ _ _ → ·Rdist+ _ _ _)
   (λ x → cong (λ y → y · x) (pres1 φIsHom) ∙ ·Lid x)
   (λ _ _ _ → sym (·Assoc _ _ _))

 fromCommAlg : CommAlgebra R ℓ → CommRingWithHom
 fromCommAlg A = (CommAlgebra→CommRing A) , φ , φIsHom
  where
  open CommRingStr (snd R) renaming (_·_ to _·r_) hiding (·Lid)
  open CommAlgebraStr (snd A)
  open AlgebraTheory (CommRing→Ring R) (CommAlgebra→Algebra A)
  φ : ⟨ R ⟩ → ⟨ A ⟩
  φ r = r ⋆ 1a
  φIsHom : IsRingHom (CommRing→Ring R .snd) φ (CommRing→Ring (CommAlgebra→CommRing A) .snd)
  φIsHom = makeIsRingHom (⋆-lid _) (λ _ _ → ⋆-ldist _ _ _)
           λ x y → cong (λ a → (x ·r y) ⋆ a) (sym (·Lid _)) ∙ ⋆Dist· _ _ _ _

 CommRingWithHomRoundTrip : (Aφ : CommRingWithHom) → fromCommAlg (toCommAlg Aφ) ≡ Aφ
 CommRingWithHomRoundTrip (A , φ) = ΣPathP (APath , φPathP)
  where
  open CommRingStr
  -- note that the proofs of the axioms might differ!
  APath : fst (fromCommAlg (toCommAlg (A , φ))) ≡ A
  fst (APath i) = ⟨ A ⟩
  0r (snd (APath i)) = 0r (snd A)
  1r (snd (APath i)) = 1r (snd A)
  _+_ (snd (APath i)) = _+_ (snd A)
  _·_ (snd (APath i)) = _·_ (snd A)
  -_ (snd (APath i)) = -_ (snd A)
  isCommRing (snd (APath i)) = isProp→PathP (λ i → isPropIsCommRing _ _ _ _ _ )
             (isCommRing (snd (fst (fromCommAlg (toCommAlg (A , φ)))))) (isCommRing (snd A)) i

  -- this only works because fst (APath i) = fst A definitionally!
  φPathP : PathP (λ i → CommRingHom R (APath i)) (snd (fromCommAlg (toCommAlg (A , φ)))) φ
  φPathP = RingHomPathP _ _ _ _ _ _ λ i x → ·Rid (snd A) (fst φ x) i

 CommAlgRoundTrip : (A : CommAlgebra R ℓ) → toCommAlg (fromCommAlg A) ≡ A
 CommAlgRoundTrip A = ΣPathP (refl , AlgStrPathP)
  where
  open CommAlgebraStr ⦃...⦄
  instance
   _ = snd A
  AlgStrPathP : PathP (λ i → CommAlgebraStr R ⟨ A ⟩) (snd (toCommAlg (fromCommAlg A))) (snd A)
  CommAlgebraStr.0a (AlgStrPathP i) = 0a
  CommAlgebraStr.1a (AlgStrPathP i) = 1a
  CommAlgebraStr._+_ (AlgStrPathP i) = _+_
  CommAlgebraStr._·_ (AlgStrPathP i) = _·_
  CommAlgebraStr.-_ (AlgStrPathP i) = -_
  CommAlgebraStr._⋆_ (AlgStrPathP i) r x = (⋆-lassoc r 1a x ∙ cong (r ⋆_) (·Lid x)) i
  CommAlgebraStr.isCommAlgebra (AlgStrPathP i) = isProp→PathP
    (λ i → isPropIsCommAlgebra _ _ _ _ _ _ (CommAlgebraStr._⋆_ (AlgStrPathP i)))
    (CommAlgebraStr.isCommAlgebra (snd (toCommAlg (fromCommAlg A)))) isCommAlgebra i

 CommAlgIso : Iso (CommAlgebra R ℓ) CommRingWithHom
 fun CommAlgIso = fromCommAlg
 inv CommAlgIso = toCommAlg
 rightInv CommAlgIso = CommRingWithHomRoundTrip
 leftInv CommAlgIso = CommAlgRoundTrip

 open RingHoms
 isCommRingWithHomHom : (A B : CommRingWithHom) → CommRingHom (fst A) (fst B) → Type ℓ
 isCommRingWithHomHom (_ , f) (_ , g) h = h ∘r f ≡ g

 CommRingWithHomHom : CommRingWithHom → CommRingWithHom → Type ℓ
 CommRingWithHomHom (A , f) (B , g) = Σ[ h ∈ CommRingHom A B ] h ∘r f ≡ g

 toCommAlgebraHom : (A B : CommRingWithHom) (h : CommRingHom (fst A) (fst B))
                  → isCommRingWithHomHom A B h
                  → CommAlgebraHom (toCommAlg A) (toCommAlg B)
 toCommAlgebraHom (A , f) (B , g) h commDiag =
   makeCommAlgebraHom (fst h) (pres1 (snd h)) (pres+ (snd h)) (pres· (snd h)) pres⋆h
   where
   open CommRingStr ⦃...⦄
   instance
    _ = snd A
    _ = snd B
   pres⋆h : ∀ r x → fst h (fst f r · x) ≡ fst g r · fst h x
   pres⋆h r x = fst h (fst f r · x)       ≡⟨ pres· (snd h) _ _ ⟩
                fst h (fst f r) · fst h x ≡⟨ cong (λ φ → fst φ r · fst h x) commDiag ⟩
                fst g r · fst h x ∎

 fromCommAlgebraHom : (A B : CommAlgebra R ℓ) → CommAlgebraHom A B
                    → CommRingWithHomHom (fromCommAlg A) (fromCommAlg B)
 fst (fst (fromCommAlgebraHom A B f)) = fst f
 pres0 (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres0 (snd f)
 pres1 (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres1 (snd f)
 pres+ (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres+ (snd f)
 pres· (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres· (snd f)
 pres- (snd (fst (fromCommAlgebraHom A B f))) = IsAlgebraHom.pres- (snd f)
 snd (fromCommAlgebraHom A B f) =
  RingHom≡ (funExt (λ x → IsAlgebraHom.pres⋆ (snd f) x 1a ∙ cong (x ⋆_) (IsAlgebraHom.pres1 (snd f))))
  where
  open CommAlgebraStr (snd A) using (1a)
  open CommAlgebraStr (snd B) using (_⋆_)

 isCommRingWithHomEquiv : (A B : CommRingWithHom) → CommRingEquiv (fst A) (fst B) → Type ℓ
 isCommRingWithHomEquiv A B e = isCommRingWithHomHom A B (RingEquiv→RingHom e)

 CommRingWithHomEquiv : CommRingWithHom → CommRingWithHom → Type ℓ
 CommRingWithHomEquiv A B = Σ[ e ∈ CommRingEquiv (fst A) (fst B) ] isCommRingWithHomEquiv A B e

 toCommAlgebraEquiv : (A B : CommRingWithHom) (e : CommRingEquiv (fst A) (fst B))
                    → isCommRingWithHomEquiv A B e
                    → CommAlgebraEquiv (toCommAlg A) (toCommAlg B)
 fst (toCommAlgebraEquiv A B e eCommDiag) = e .fst
 snd (toCommAlgebraEquiv A B e eCommDiag) = toCommAlgebraHom A B _ eCommDiag .snd

module CommAlgebraHoms {R : CommRing ℓ} where
  open AlgebraHoms

  idCommAlgebraHom : (A : CommAlgebra R ℓ') → CommAlgebraHom A A
  idCommAlgebraHom A = idAlgebraHom (CommAlgebra→Algebra A)

  compCommAlgebraHom : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') (C : CommAlgebra R ℓ''')
                  → CommAlgebraHom A B → CommAlgebraHom B C → CommAlgebraHom A C
  compCommAlgebraHom A B C = compAlgebraHom {A = CommAlgebra→Algebra A}
                                            {CommAlgebra→Algebra B} {CommAlgebra→Algebra C}

  _∘ca_ : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
        → CommAlgebraHom B C → CommAlgebraHom A B → CommAlgebraHom A C
  g ∘ca f = compCommAlgebraHom _ _ _ f g

  compIdCommAlgebraHom : {A B : CommAlgebra R ℓ'} (f : CommAlgebraHom A B)
                    → compCommAlgebraHom _ _ _ (idCommAlgebraHom A) f ≡ f
  compIdCommAlgebraHom = compIdAlgebraHom

  idCompCommAlgebraHom : {A B : CommAlgebra R ℓ'} (f : CommAlgebraHom A B)
                    → compCommAlgebraHom _ _ _ f (idCommAlgebraHom B) ≡ f
  idCompCommAlgebraHom = idCompAlgebraHom

  compAssocCommAlgebraHom : {A B C D : CommAlgebra R ℓ'}
                         (f : CommAlgebraHom A B) (g : CommAlgebraHom B C) (h : CommAlgebraHom C D)
                       → compCommAlgebraHom _ _ _ (compCommAlgebraHom _ _ _ f g) h
                       ≡ compCommAlgebraHom _ _ _ f (compCommAlgebraHom _ _ _ g h)
  compAssocCommAlgebraHom = compAssocAlgebraHom

module CommAlgebraEquivs {R : CommRing ℓ} where
 open AlgebraEquivs

 compCommAlgebraEquiv : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
                   → CommAlgebraEquiv A B → CommAlgebraEquiv B C → CommAlgebraEquiv A C
 compCommAlgebraEquiv {A = A} {B = B} {C = C} = compAlgebraEquiv {A = CommAlgebra→Algebra A}
                                                           {B = CommAlgebra→Algebra B}
                                                           {C = CommAlgebra→Algebra C}

-- the CommAlgebra version of uaCompEquiv
module CommAlgebraUAFunctoriality {R : CommRing ℓ} where
 open CommAlgebraStr
 open CommAlgebraEquivs

 CommAlgebra≡ : (A B : CommAlgebra R ℓ') → (
   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
   Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
   Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
   Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
   Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
   PathP (λ i → IsCommAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isCommAlgebra (snd A))
                                                                           (isCommAlgebra (snd B)))
   ≃ (A ≡ B)
 CommAlgebra≡ A B = isoToEquiv theIso
   where
   open Iso
   theIso : Iso _ _
   fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
                 , commalgebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
   inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
                , cong (isCommAlgebra ∘ snd) x
   rightInv theIso _ = refl
   leftInv theIso _ = refl

 caracCommAlgebra≡ : {A B : CommAlgebra R ℓ'} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
 caracCommAlgebra≡ {A = A} {B = B} p q P =
   sym (transportTransport⁻ (ua (CommAlgebra≡ A B)) p)
                                    ∙∙ cong (transport (ua (CommAlgebra≡ A B))) helper
                                    ∙∙ transportTransport⁻ (ua (CommAlgebra≡ A B)) q
     where
     helper : transport (sym (ua (CommAlgebra≡ A B))) p ≡ transport (sym (ua (CommAlgebra≡ A B))) q
     helper = Σ≡Prop
                (λ _ → isPropΣ
                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
                          λ _ → isOfHLevelPathP 1 (isPropIsCommAlgebra _ _ _ _ _ _ _) _ _)
               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

 uaCompCommAlgebraEquiv : {A B C : CommAlgebra R ℓ'} (f : CommAlgebraEquiv A B) (g : CommAlgebraEquiv B C)
                  → uaCommAlgebra (compCommAlgebraEquiv f g) ≡ uaCommAlgebra f ∙ uaCommAlgebra g
 uaCompCommAlgebraEquiv f g = caracCommAlgebra≡ _ _ (
   cong ⟨_⟩ (uaCommAlgebra (compCommAlgebraEquiv f g))
     ≡⟨ uaCompEquiv _ _ ⟩
   cong ⟨_⟩ (uaCommAlgebra f) ∙ cong ⟨_⟩ (uaCommAlgebra g)
     ≡⟨ sym (cong-∙ ⟨_⟩ (uaCommAlgebra f) (uaCommAlgebra g)) ⟩
   cong ⟨_⟩ (uaCommAlgebra f ∙ uaCommAlgebra g) ∎)

open CommAlgebraHoms
open CommAlgebraEquivs
open CommAlgebraUAFunctoriality
recPT→CommAlgebra : {R : CommRing ℓ} {A : Type ℓ'} (𝓕  : A → CommAlgebra R ℓ'')
           → (σ : ∀ x y → CommAlgebraEquiv (𝓕 x) (𝓕 y))
           → (∀ x y z → σ x z ≡ compCommAlgebraEquiv (σ x y) (σ y z))
          ------------------------------------------------------
           → ∥ A ∥ → CommAlgebra R ℓ''
recPT→CommAlgebra 𝓕 σ compCoh = GpdElim.rec→Gpd isGroupoidCommAlgebra 𝓕
  (3-ConstantCompChar 𝓕 (λ x y → uaCommAlgebra (σ x y))
                          λ x y z → sym (  cong uaCommAlgebra (compCoh x y z)
                                         ∙ uaCompCommAlgebraEquiv (σ x y) (σ y z)))

contrCommAlgebraHom→contrCommAlgebraEquiv : {R : CommRing ℓ} {A : Type ℓ'}
        (σ : A → CommAlgebra R ℓ'')
      → (∀ x y → isContr (CommAlgebraHom (σ x) (σ y)))
      ----------------------------------------------------------------------------
      → ∀ x y → isContr (CommAlgebraEquiv (σ x) (σ y))
contrCommAlgebraHom→contrCommAlgebraEquiv σ contrHom x y = σEquiv ,
  λ e → Σ≡Prop (λ _ → isPropIsAlgebraHom _ _ _ _)
           (Σ≡Prop isPropIsEquiv (cong fst (contrHom _ _ .snd (CommAlgebraEquiv→CommAlgebraHom e))))
  where
  open Iso
  χ₁ = contrHom x y .fst
  χ₂ = contrHom y x .fst
  χ₁∘χ₂≡id : χ₁ ∘ca χ₂ ≡ idCommAlgebraHom _
  χ₁∘χ₂≡id = isContr→isProp (contrHom _ _) _ _

  χ₂∘χ₁≡id : χ₂ ∘ca χ₁ ≡ idCommAlgebraHom _
  χ₂∘χ₁≡id = isContr→isProp (contrHom _ _) _ _

  σIso : Iso ⟨ σ x ⟩ ⟨ σ y ⟩
  fun σIso = fst χ₁
  inv σIso = fst χ₂
  rightInv σIso = funExt⁻ (cong fst χ₁∘χ₂≡id)
  leftInv σIso = funExt⁻ (cong fst χ₂∘χ₁≡id)

  σEquiv : CommAlgebraEquiv (σ x) (σ y)
  fst σEquiv = isoToEquiv σIso
  snd σEquiv = snd χ₁

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- Record types with manifest fields and "with", based on Randy
-- Pollack's "Dependently Typed Records in Type Theory"
------------------------------------------------------------------------

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

-- The module is parametrised by the type of labels, which should come
-- with decidable equality.

open import Equality
open import Prelude hiding (id; proj₁; proj₂)

module Records-with-with
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)
  (open Derived-definitions-and-properties eq)
  (Label : Type)
  (_≟_ : Decidable-equality Label)
  where

open import Bijection eq using (_↔_; ↑↔)
open import Function-universe eq hiding (_∘_)
open import List eq using (foldr)

------------------------------------------------------------------------
-- A Σ-type with a manifest field

-- A variant of Σ where the value of the second field is "manifest"
-- (given by the first).

infix 4 _,

record Manifest-Σ {a b} (A : Type a) {B : A → Type b}
                  (f : (x : A) → B x) : Type a where
  constructor _,
  field proj₁ : A

  proj₂ : B proj₁
  proj₂ = f proj₁

------------------------------------------------------------------------
-- Signatures and records

mutual

  infixl 5 _,_∶_ _,_≔_

  data Signature s : Type (lsuc s) where
    ∅     : Signature s
    _,_∶_ : (Sig : Signature s)
            (ℓ : Label)
            (A : Record Sig → Type s) →
            Signature s
    _,_≔_ : (Sig : Signature s)
            (ℓ : Label)
            {A : Record Sig → Type s}
            (a : (r : Record Sig) → A r) →
            Signature s

  -- Record is a record type to ensure that the signature can be
  -- inferred from a value of type Record Sig.

  record Record {s} (Sig : Signature s) : Type s where
    eta-equality
    inductive
    constructor rec
    field fun : Record-fun Sig

  Record-fun : ∀ {s} → Signature s → Type s
  Record-fun ∅             = ↑ _ ⊤
  Record-fun (Sig , ℓ ∶ A) =          Σ (Record Sig) A
  Record-fun (Sig , ℓ ≔ a) = Manifest-Σ (Record Sig) a

------------------------------------------------------------------------
-- Labels

-- A signature's labels, starting with the last one.

labels : ∀ {s} → Signature s → List Label
labels ∅             = []
labels (Sig , ℓ ∶ A) = ℓ ∷ labels Sig
labels (Sig , ℓ ≔ a) = ℓ ∷ labels Sig

-- Inhabited if the label is part of the signature.

infix 4 _∈_

_∈_ : ∀ {s} → Label → Signature s → Type
ℓ ∈ Sig =
  foldr (λ ℓ′ → if ℓ ≟ ℓ′ then (λ _ → ⊤) else id)
        ⊥
        (labels Sig)

------------------------------------------------------------------------
-- Projections

-- Signature restriction and projection. (Restriction means removal of
-- a given field and all subsequent fields.)

Restrict : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig →
           Signature s
Restrict ∅              ℓ ()
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no  _ = Restrict Sig ℓ ℓ∈
Restrict (Sig , ℓ′ ≔ a) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = Sig
... | no  _ = Restrict Sig ℓ ℓ∈

Restricted : ∀ {s} (Sig : Signature s) (ℓ : Label) → ℓ ∈ Sig → Type s
Restricted Sig ℓ ℓ∈ = Record (Restrict Sig ℓ ℓ∈)

Proj : ∀ {s} (Sig : Signature s) (ℓ : Label) (ℓ∈ : ℓ ∈ Sig) →
       Restricted Sig ℓ ℓ∈ → Type s
Proj ∅              ℓ ()
Proj (Sig , ℓ′ ∶ A) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = A
... | no  _ = Proj Sig ℓ ℓ∈
Proj (_,_≔_ Sig ℓ′ {A = A} a) ℓ ℓ∈ with ℓ ≟ ℓ′
... | yes _ = A
... | no  _ = Proj Sig ℓ ℓ∈

-- Record restriction and projection.

infixl 5 _∣_

_∣_ : ∀ {s} {Sig : Signature s} → Record Sig →
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} → Restricted Sig ℓ ℓ∈
_∣_ {Sig = ∅}            r       ℓ {}
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₁ r
... | no  _ = _∣_ (Σ.proj₁ r) ℓ {ℓ∈}
_∣_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₁ r
... | no  _ = _∣_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

infixl 5 _·_

_·_ : ∀ {s} {Sig : Signature s} (r : Record Sig)
      (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
      Proj Sig ℓ ℓ∈ (r ∣ ℓ)
_·_ {Sig = ∅}            r       ℓ {}
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Σ.proj₂ r
... | no  _ = _·_ (Σ.proj₁ r) ℓ {ℓ∈}
_·_ {Sig = Sig , ℓ′ ≔ a} (rec r) ℓ {ℓ∈} with ℓ ≟ ℓ′
... | yes _ = Manifest-Σ.proj₂ r
... | no  _ = _·_ (Manifest-Σ.proj₁ r) ℓ {ℓ∈}

------------------------------------------------------------------------
-- With

-- Sig With ℓ ≔ a is the signature Sig, but with the ℓ field set to a.

mutual

  infixl 5 _With_≔_

  _With_≔_ : ∀ {s} (Sig : Signature s) (ℓ : Label) {ℓ∈ : ℓ ∈ Sig} →
             ((r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ ℓ∈ r) → Signature s
  _With_≔_ ∅                ℓ {}   a
  _With_≔_ (Sig , ℓ′ ∶ A)   ℓ {ℓ∈} a with ℓ ≟ ℓ′
  ... | yes _ = Sig                   , ℓ′ ≔ a
  ... | no  _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ∶ A ∘ drop-With
  _With_≔_  (Sig , ℓ′ ≔ a′) ℓ {ℓ∈} a with ℓ ≟ ℓ′
  ... | yes _ = Sig                   , ℓ′ ≔ a
  ... | no  _ = _With_≔_ Sig ℓ {ℓ∈} a , ℓ′ ≔ a′ ∘ drop-With

  drop-With : ∀ {s} {Sig : Signature s} {ℓ : Label} {ℓ∈ : ℓ ∈ Sig}
              {a : (r : Restricted Sig ℓ ℓ∈) → Proj Sig ℓ ℓ∈ r} →
              Record (_With_≔_ Sig ℓ {ℓ∈} a) → Record Sig
  drop-With {Sig = ∅} {ℓ∈ = ()}      r
  drop-With {Sig = Sig , ℓ′ ∶ A} {ℓ} (rec r) with ℓ ≟ ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r , Manifest-Σ.proj₂ r)
  ... | no  _ = rec (drop-With (Σ.proj₁ r) , Σ.proj₂ r)
  drop-With {Sig = Sig , ℓ′ ≔ a} {ℓ} (rec r) with ℓ ≟ ℓ′
  ... | yes _ = rec (Manifest-Σ.proj₁ r ,)
  ... | no  _ = rec (drop-With (Manifest-Σ.proj₁ r) ,)

------------------------------------------------------------------------
-- Alternative definitions of Record, along with some isomorphisms

-- An alternative definition of Record: right-nested, without the
-- record type, and without Manifest-Σ.

Recordʳ : ∀ {s} (Sig : Signature s) → (Record Sig → Type s) → Type s
Recordʳ ∅             κ = κ _
Recordʳ (Sig , ℓ ∶ A) κ = Recordʳ Sig (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_)))
Recordʳ (Sig , ℓ ≔ a) κ = Recordʳ Sig (λ r → κ (rec (r ,)))

-- Manifest-Σ A f is isomorphic to A.

Manifest-Σ↔ :
  ∀ {a b} {A : Type a} {B : A → Type b} {f : (x : A) → B x} →
  Manifest-Σ A f ↔ A
Manifest-Σ↔ = record
  { surjection = record
    { logical-equivalence = record
      { to   = Manifest-Σ.proj₁
      ; from = _,
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → refl _
  }

-- Record is pointwise isomorphic to Record-fun.

Record↔Record-fun :
  ∀ {s} {Sig : Signature s} → Record Sig ↔ Record-fun Sig
Record↔Record-fun = record
  { surjection = record
    { logical-equivalence = record { to = Record.fun ; from = rec }
    ; right-inverse-of    = λ _ → refl _
    }
  ; left-inverse-of = λ _ → refl _
  }

-- Record and Recordʳ are, in a certain sense, isomorphic.

mutual

  Σ-Record↔Recordʳ :
    ∀ {s} (Sig : Signature s) (κ : Record Sig → Type s) →
    Σ (Record Sig) κ ↔ Recordʳ Sig κ
  Σ-Record↔Recordʳ Sig κ =
    Σ (Record Sig) κ              ↝⟨ Σ-cong Record↔Record-fun (λ _ → id) ⟩
    Σ (Record-fun Sig) (κ ∘ rec)  ↝⟨ Σ-Record-fun↔Recordʳ Sig κ ⟩□
    Recordʳ Sig κ                 □

  Σ-Record-fun↔Recordʳ :
    ∀ {s} (Sig : Signature s) (κ : Record Sig → Type s) →
    Σ (Record-fun Sig) (κ ∘ rec) ↔ Recordʳ Sig κ

  Σ-Record-fun↔Recordʳ ∅ κ =
    Σ (↑ _ ⊤) (κ ∘ rec)   ↝⟨ Σ-cong ↑↔ (λ _ → id) ⟩
    Σ ⊤ (κ ∘ rec ∘ lift)  ↝⟨ Σ-left-identity ⟩□
    κ _                   □

  Σ-Record-fun↔Recordʳ (Sig , ℓ ∶ A) κ =
    Σ (Σ (Record Sig) A) (κ ∘ rec)                     ↝⟨ inverse Σ-assoc ⟩
    Σ (Record Sig) (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_)))  ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
    Recordʳ Sig (λ r → Σ (A r) (κ ∘ rec ∘ (r ,_)))     □

  Σ-Record-fun↔Recordʳ (Sig , ℓ ≔ a) κ =
    Σ (Manifest-Σ (Record Sig) a) (κ ∘ rec)  ↝⟨ Σ-cong Manifest-Σ↔ (λ _ → id) ⟩
    Σ (Record Sig) (κ ∘ rec ∘ _,)            ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
    Recordʳ Sig (κ ∘ rec ∘ _,)               □

-- Note that the continuation is initialised with a (lifted) unit
-- type.

Record↔Recordʳ :
  ∀ {s} (Sig : Signature s) →
  Record Sig ↔ Recordʳ Sig (λ _ → ↑ s ⊤)
Record↔Recordʳ Sig =
  Record Sig                 ↝⟨ inverse ×-right-identity ⟩
  Record Sig × ⊤             ↝⟨ id ×-cong inverse ↑↔ ⟩
  Record Sig × ↑ _ ⊤         ↝⟨ Σ-Record↔Recordʳ Sig _ ⟩□
  Recordʳ Sig (λ _ → ↑ _ ⊤)  □

-- Another alternative definition of Record: basically the same as
-- Recordʳ, but the continuation is initialised with the first
-- non-manifest field, if any, to avoid a pointless innermost unit
-- type.

Recʳ : ∀ {s} → Signature s → Type s
Recʳ ∅             = ↑ _ ⊤
Recʳ (Sig , ℓ ∶ A) = Recordʳ Sig A
Recʳ (Sig , ℓ ≔ a) = Recʳ Sig

-- Record and Recʳ are pointwise isomorphic.

mutual

  Record↔Recʳ :
    ∀ {s} {Sig : Signature s} →
    Record Sig ↔ Recʳ Sig
  Record↔Recʳ {Sig = Sig} =
    Record Sig      ↝⟨ Record↔Record-fun ⟩
    Record-fun Sig  ↝⟨ Record-fun↔Recʳ Sig ⟩□
    Recʳ Sig        □

  Record-fun↔Recʳ :
    ∀ {s} (Sig : Signature s) →
    Record-fun Sig ↔ Recʳ Sig

  Record-fun↔Recʳ ∅ = ↑ _ ⊤ □

  Record-fun↔Recʳ (Sig , ℓ ∶ A) =
    Σ (Record Sig) A  ↝⟨ Σ-Record↔Recordʳ Sig A ⟩□
    Recordʳ Sig A     □

  Record-fun↔Recʳ (Sig , ℓ ≔ a) =
    Manifest-Σ (Record Sig) a  ↝⟨ Manifest-Σ↔ ⟩
    Record Sig                 ↝⟨ Record↔Recʳ ⟩□
    Recʳ Sig                   □


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A definition for the permutation relation using setoid equality
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Homogeneous where

open import Data.List.Base using (List; _∷_)
open import Data.List.Relation.Binary.Pointwise as Pointwise
  using (Pointwise)
open import Level using (Level; _⊔_)
open import Relation.Binary

private
  variable
    a r s : Level
    A : Set a

data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
  refl  : ∀ {xs ys} → Pointwise R xs ys → Permutation R xs ys
  prep  : ∀ {xs ys x y} (eq : R x y) → Permutation R xs ys → Permutation R (x ∷ xs) (y ∷ ys)
  swap  : ∀ {xs ys x y x' y'} (eq₁ : R x x') (eq₂ : R y y') → Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y' ∷ x' ∷ ys)
  trans : ∀ {xs ys zs} → Permutation R xs ys → Permutation R ys zs → Permutation R xs zs

------------------------------------------------------------------------
-- The Permutation relation is an equivalence

module _ {R : Rel A r}  where

  sym : Symmetric R → Symmetric (Permutation R)
  sym R-sym (refl xs∼ys)           = refl (Pointwise.symmetric R-sym xs∼ys)
  sym R-sym (prep x∼x' xs↭ys)      = prep (R-sym x∼x') (sym R-sym xs↭ys)
  sym R-sym (swap x∼x' y∼y' xs↭ys) = swap (R-sym y∼y') (R-sym x∼x') (sym R-sym xs↭ys)
  sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)

  isEquivalence : Reflexive R → Symmetric R → IsEquivalence (Permutation R)
  isEquivalence R-refl R-sym = record
    { refl  = refl (Pointwise.refl R-refl)
    ; sym   = sym R-sym
    ; trans = trans
    }

  setoid : Reflexive R → Symmetric R → Setoid _ _
  setoid R-refl R-sym = record
    { isEquivalence = isEquivalence R-refl R-sym
    }

map : ∀ {R : Rel A r} {S : Rel A s} →
      (R ⇒ S) → (Permutation R ⇒ Permutation S)
map R⇒S (refl xs∼ys)         = refl (Pointwise.map R⇒S xs∼ys)
map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Semigroup.Construct.Empty where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Semigroup

open import Cubical.Data.Empty

import Cubical.Algebra.Magma.Construct.Empty as ⊥Magma
open ⊥Magma public hiding (⊥-isMagma; ⊥-Magma)

◯-assoc : Associative _◯_
◯-assoc _ _ _ = isProp⊥ _ _

⊥-isSemigroup : IsSemigroup ⊥ _◯_
⊥-isSemigroup = record
  { isMagma = ⊥Magma.⊥-isMagma
  ; assoc   = ◯-assoc
  }

⊥-Semigroup : Semigroup ℓ-zero
⊥-Semigroup = record { isSemigroup = ⊥-isSemigroup }