text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Quadricity
open import Oscar.Class.Injectivity
open import Oscar.Class.Congruity
open import Oscar.Class.Leftstar
open import Oscar.Class.Properthing
open import Oscar.Class.Smap
open import Oscar.Class.Symmetry
open import Oscar.Data.Fin
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Data.Surjcollation
open import Oscar.Data.Surjextenscollation
open import Oscar.Data.Proposequality
open import Oscar.Property.Setoid.Proposequality
open import Oscar.Property.Setoid.Proposextensequality
open import Oscar.Property.Functor.SubstitunctionExtensionTerm
open import Oscar.Property.Thickandthin.FinTermProposequalityMaybeProposequality
import Oscar.Class.Congruity.Proposequality
import Oscar.Class.Congruity.Proposextensequality
import Oscar.Class.Surjection.⋆
open import Oscar.Property.Setoid.ṖropertyEquivalence
import Oscar.Class.Properthing.Ṗroperty
open import Oscar.Data.ProductIndexEquivalence
import Oscar.Data.ExtensionṖroperty
open import Oscar.Data.ProperlyExtensionNothing
import Oscar.Class.Properthing.ExtensionṖroperty
import Oscar.Class.Smap.TransitiveExtensionLeftṖroperty
import Oscar.Class.Smap.ExtensionṖroperty
import Oscar.Class.[ExtensibleType].Proposequality
import Oscar.Class.HasEquivalence.ExtensionṖroperty
import Oscar.Class.HasEquivalence.Ṗroperty
import Oscar.Class.HasEquivalence.Substitunction
open import Oscar.Class.Reflexivity
open import Oscar.Class.Similarity
open import Oscar.Class.Quadricity
open import Oscar.Class.Surjection
open import Oscar.Class.Leftunit

module Oscar.Property.Propergroup.Substitunction where

module _
  {𝔭} {𝔓 : Ø 𝔭}
  {ℓ : Ł}
  where
  open Substitunction 𝔓

  instance

    𝓢urjectextenscongruityArrowṖropertySubstitunction : Similarity,smaphomarrow!.class Substitunction (LeftṖroperty ℓ Substitunction) _≈_
    𝓢urjectextenscongruityArrowṖropertySubstitunction .⋆ _ (∁ P⇔Q) .π₀ = P⇔Q

    𝓢urjectextenscongruityArrowExtensionṖropertySubstitunction : Similarity,smaphomarrow!.class Substitunction (LeftExtensionṖroperty ℓ Substitunction _≈_) _≈_
    𝓢urjectextenscongruityArrowExtensionṖropertySubstitunction .⋆ _ (∁ (∁ P⇔Q)) .π₀ = ∁ P⇔Q -- P⇔Q

module _
  {𝔭} {𝔓 : Ø 𝔭}
  where
  open Term 𝔓

  module S = Surjcollation (Arrow Fin Term) _≡_
  module Ṡ = Surjextenscollation (Arrow Fin Term) _≡̇_

  instance

    𝒫roperfact1UnifiesSubstitunctionFork : ∀ {n} → Properfact1.class S._⟹_ (_fork_ {n = n})
    𝒫roperfact1UnifiesSubstitunctionFork .⋆ _ _ _ _ .π₀ = (λ s≡t → injectivity₂,₀,₁ s≡t , injectivity₂,₀,₂ s≡t) , uncurry (congruity₂ _fork_)

    𝒫roperfact1ExtensionalUnifiesSubstitunctionFork : ∀ {n} → Properfact1.class Ṡ._⟹_ (_fork_ {n = n})
    𝒫roperfact1ExtensionalUnifiesSubstitunctionFork .⋆ _ _ _ _ .π₀ .π₀ = (λ s≡t → injectivity₂,₀,₁ s≡t , injectivity₂,₀,₂ s≡t) , uncurry (congruity₂ _fork_)

  instance

    𝓕actsurj3Regular : ∀ {ℓ} → Leftunit,equivalence,smaphomarrow!.class (Arrow Fin Term) (LeftṖroperty ℓ (Arrow Fin Term))
    𝓕actsurj3Regular .⋆ .π₀ = ¡ , ¡

    𝓕actsurj3Extension : ∀ {ℓ} → Leftunit,smaphomarrow.class (Arrow Fin Term) (LeftExtensionṖroperty ℓ (Arrow Fin Term) (Pointwise Proposequality)) ε surjection smaparrow _≈_
    𝓕actsurj3Extension .⋆ .π₀ .π₀ = ¡ , ¡

  open Substitunction 𝔓

  instance

    𝓕actsurj4Regular : ∀ {ℓ} → Leftstar,smaphomarrow!.class (LeftṖroperty ℓ (Arrow Fin Term)) (Arrow Fin Term) Nothing
    𝓕actsurj4Regular .⋆ _ (∁ nop) .π₀ = nop

    𝓕actsurj4Extension : ∀ {ℓ} → Leftstar,smaphomarrow!.class (LeftExtensionṖroperty ℓ Substitunction (Pointwise Proposequality)) (Arrow Fin Term) Nothing
    𝓕actsurj4Extension .⋆ _ (∁ nop) .π₀ = nop

  instance

    𝓕actsurj6Extension : ∀ {ℓ} → Similarity,cosmaphomarrow!.class Substitunction (ArrowExtensionṖroperty ℓ Fin Term Proposequality) _≈_ _≈_
    𝓕actsurj6Extension .⋆ P f≐g .π₀ .π₀ {f = h} = π₁ P (congruity (smap h) ∘ f≐g) , π₁ P (symmetry (congruity (smap h) ∘ f≐g)) -- FIXME replacing symmetry with Sym.[] fails

ext: agda


text:
-- Andreas, 2014-06-27
-- {-# OPTIONS -v tc.lhs:40 #-}
{-# OPTIONS --copatterns #-}

record Coind : Set where
  coinductive
  field ind : Coind

open Coind

loop : Set -> Coind
ind A (loop B) = ind (loop A)

-- WAS: Internal error.

-- NOW: Proper error.
-- Cannot eliminate type Coind with pattern ind A (did you supply too many arguments?)
-- when checking that the clause ind A (loop B) = ind (loop A) has
-- type Set → Coind

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.String
open import Agda.Builtin.Equality

test : String → String → String
test "x" b = "left"
test a "x" = "right"
test a b = "nowhere"

_ : test "a" "x" ≡ "right"
_ = refl


text:
{-

The naive, but incorrect, way to define the integers as a HIT.

This file mainly contains a proof that IsoInt ≢ Int, and ends with a
 demonstration of how the same proof strategy fails for BiInvInt.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.IsoInt.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Int
open import Cubical.Data.Nat
open import Cubical.Data.Empty

open import Cubical.Relation.Nullary

data IsoInt : Type₀ where
  zero : IsoInt
  suc : IsoInt -> IsoInt

  -- suc is an isomorphism:
  pred : IsoInt -> IsoInt
  suc-pred : ∀ z -> suc (pred z) ≡ z
  pred-suc : ∀ z -> pred (suc z) ≡ z

suc-iso : Iso IsoInt IsoInt
suc-iso = record { fun = suc ; inv = pred ; rightInv = suc-pred ; leftInv = pred-suc }

-- this submodule is adapted from Section 5 of
--  http://www.cs.ru.nl/~herman/PUBS/HIT-programming.pdf

module NonTrivial where

  -- these two paths are distinct!
  p₁ p₂ : Path IsoInt (suc (pred (suc zero))) (suc zero)
  p₁ i = suc-pred (suc zero) i
  p₂ i = suc (pred-suc zero i)

  -- to prove this we map into S¹, sending p₁ to refl and p₂ to loop

  open import Cubical.HITs.S1

  toS¹ : IsoInt → S¹
  toS¹ zero           = base
  toS¹ (suc x)        = toS¹ x
  toS¹ (pred x)       = toS¹ x
  toS¹ (suc-pred x i) = refl {x = toS¹ x} i
  toS¹ (pred-suc x i) = rotLoop (toS¹ x) i

  p₁≡refl : cong toS¹ p₁ ≡ refl
  p₁≡refl = refl

  p₂≡loop : cong toS¹ p₂ ≡ loop
  p₂≡loop = refl

  -- this is enough to show that p₁ and p₂ cannot be equal
  p₁≢p₂ : ¬ (p₁ ≡ p₂)
  p₁≢p₂ eq = znots 0≡1
    where -- using winding numbers, p₁ ≡ p₂ implies 0 ≡ 1
          0≡1 : 0 ≡ 1
          0≡1 = injPos (cong (winding ∘ cong toS¹) eq)

¬isSet-IsoInt : ¬ (isSet IsoInt)
¬isSet-IsoInt pf = NonTrivial.p₁≢p₂ (pf _ _ NonTrivial.p₁ NonTrivial.p₂)

¬Int≡IsoInt : ¬ (Int ≡ IsoInt)
¬Int≡IsoInt p = ¬isSet-IsoInt (subst isSet p isSetInt)

private

  -- Note: this same proof strategy fails for BiInvInt!

  open import Cubical.HITs.Ints.BiInvInt hiding (zero; suc; pred; suc-pred; pred-suc)
  import Cubical.HITs.Ints.BiInvInt as BiI

  p₁ p₂ : Path BiInvInt (BiI.suc (BiI.pred (BiI.suc BiI.zero))) (BiI.suc BiI.zero)
  p₁ i = BiI.suc-pred (BiI.suc BiI.zero) i
  p₂ i = BiI.suc (BiI.pred-suc BiI.zero i)

  open import Cubical.HITs.S1

  toS¹ : BiInvInt → S¹
  toS¹ BiI.zero            = base
  toS¹ (BiI.suc x)         = toS¹ x
  toS¹ (BiI.predr x)       = toS¹ x
  toS¹ (BiI.predl x)       = toS¹ x
  toS¹ (BiI.suc-predr x i) = refl {x = toS¹ x} i
  toS¹ (BiI.predl-suc x i) = rotLoop (toS¹ x) i

  -- still p₂ maps to loop...
  p₂≡loop : cong toS¹ p₂ ≡ loop
  p₂≡loop = refl

  open import Cubical.Foundations.GroupoidLaws

  -- ...but now so does p₁!
  p₁≡loop : cong toS¹ p₁ ≡ loop
  p₁≡loop = sym (decodeEncode base (cong toS¹ p₁)) ∙ sym (lUnit loop)

  -- if we use BiI.predr instead of BiI.pred (≡ BiI.predl) in p₁ and p₂,
  --  both paths in S¹ are refl

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:
-- Andreas, 2017-01-12, issue #2386

postulate
  F : ∀{a}{A : Set a} → A → A

data Eq (A : Set) : (x y : F A) → Set where
  refl : (x : F A) → Eq A x x

{-# BUILTIN EQUALITY Eq #-}

-- Expected error:
-- The type of BUILTIN EQUALITY must be a polymorphic relation
-- when checking the pragma BUILTIN EQUALITY Eq

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-08-27 Rewrite rules in parametrized modules are fine.
-- Jesper, 2015-10-14 Semantics of rewrite rules in parametrized modules has
--                    changed (see issue 1652)
-- Jesper, 2015-11-9  Rewrite rules in parametrized modules are now
--                    generalized to the top-context automatically

{-# OPTIONS --rewriting #-}

open import Common.Nat
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

module _ (y z : Nat) where

  assoc+ : ∀ x → (x + y) + z ≡ x + (y + z)
  assoc+ zero = refl
  assoc+ (suc x) rewrite assoc+ x = refl

  {-# REWRITE assoc+ #-}

test : ∀{x y} → (x + 0) + y ≡ x + y
test = refl


text:
------------------------------------------------------------------------
-- Some examples
------------------------------------------------------------------------

module Contractive.Examples where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Data.Nat
open import Data.Nat.Properties
import Data.Vec as Vec
open Vec using (_∷_; [])
open import Function
open import Contractive
import Contractive.Stream as S
open import StreamProg using (Ord; lt; eq; gt; merge)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open COFE (S.cofe 0)

fibF : ContractiveFun (S.cofe 0)
fibF = record
  { F             = F
  ; isContractive = isCon _ _ _
  }
  where
  F = λ xs → 0 ∷ ♯ (1 ∷ ♯ zipWith _+_ xs (tail xs))

  lemma₁ : ∀ _∙_ (xs ys : Stream ℕ) n →
           take n (zipWith _∙_ xs ys) ≡
           Vec.zipWith _∙_ (take n xs) (take n ys)
  lemma₁ _∙_ _        _        zero    = refl
  lemma₁ _∙_ (x ∷ xs) (y ∷ ys) (suc n) =
    cong (_∷_ (x ∙ y)) (lemma₁ _∙_ (♭ xs) (♭ ys) n)

  lemma₂ : ∀ (xs ys : Stream ℕ) n →
           Eq n xs ys → take n xs ≡ take n ys
  lemma₂ _        _         zero    _   = refl
  lemma₂ (x ∷ xs) ( y ∷ ys) (suc n) hyp
    with cong Vec.head hyp | take n (♭ xs) | lemma₂ (♭ xs) (♭ ys) n (cong Vec.tail hyp)
  lemma₂ (x ∷ xs) (.x ∷ ys) (suc n) hyp | refl | .(take n (♭ ys)) | refl = refl

  isCon : ∀ (xs ys : Stream ℕ) n →
          (∀ {m} → m <′ n → Eq m xs ys) →
          Eq n (F xs) (F ys)
  isCon _        _        zero    _   = refl
  isCon (x ∷ xs) (y ∷ ys) (suc n) hyp = cong (λ zs → 0 ∷ 1 ∷ zs) (begin
    take n (zipWith _+_ (x ∷ xs) (♭ xs))               ≡⟨ lemma₁ _+_ (x ∷ xs) (♭ xs) n ⟩
    Vec.zipWith _+_ (take n (x ∷ xs)) (take n (♭ xs))  ≡⟨ cong₂ (Vec.zipWith _+_)
                                                                (lemma₂ _ _ n (hyp ≤′-refl))
                                                                (cong Vec.tail (hyp ≤′-refl)) ⟩
    Vec.zipWith _+_ (take n (y ∷ ys)) (take n (♭ ys))  ≡⟨ sym $ lemma₁ _+_ (y ∷ ys) (♭ ys) n ⟩
    take n (zipWith _+_ (y ∷ ys) (♭ ys))               ∎)

fib : Stream ℕ
fib = ContractiveFun.fixpoint fibF

-- Note that I could not be bothered to finish the following
-- definition.

hammingF : ContractiveFun (S.cofe 0)
hammingF = record
  { F             = F
  ; isContractive = isCon _ _ _
  }
  where
  toOrd : ∀ {m n} → Ordering m n → Ord
  toOrd (less _ _)    = lt
  toOrd (equal _)     = eq
  toOrd (greater _ _) = gt

  cmp : ℕ → ℕ → Ord
  cmp m n = toOrd (compare m n)

  F = λ (xs : _) → 0 ∷ ♯ merge cmp (map (_*_ 2) xs) (map (_*_ 3) xs)

  postulate
    lemma : ∀ n → cmp (2 * suc n) (3 * suc n) ≡ lt

  isCon : ∀ (xs ys : Stream ℕ) n →
          (∀ {m} → m <′ n → Eq m xs ys) →
          Eq n (F xs) (F ys)
  isCon _        _         zero    _   = refl
  isCon (x ∷ xs) (y  ∷ ys) (suc n) hyp with cong Vec.head (hyp (s≤′s z≤′n))
  isCon (0 ∷ xs) (.0 ∷ ys) (suc n) hyp | refl =
    cong (λ zs → 0 ∷ 0 ∷ zs) (begin
      take n (merge cmp (map (_*_ 2) (♭ xs)) (map (_*_ 3) (♭ xs)))  ≡⟨ iCantBeBothered ⟩
      take n (merge cmp (map (_*_ 2) (♭ ys)) (map (_*_ 3) (♭ ys)))  ∎)
    where postulate iCantBeBothered : _
  isCon (suc x ∷ xs) (.(suc x) ∷ ys) (suc n) hyp | refl
    with cmp (2 * suc x) (3 * suc x) | lemma x
  isCon (suc x ∷ xs) (.(suc x) ∷ ys) (suc n) hyp | refl | .lt | refl =
    cong (λ zs → 0 ∷ 2 * suc x ∷ zs) (begin
      take n (merge cmp (map (_*_ 2) (♭ xs))
                        (map (_*_ 3) (suc x ∷ xs)))  ≡⟨ iCantBeBothered ⟩
      take n (merge cmp (map (_*_ 2) (♭ ys))
                        (map (_*_ 3) (suc x ∷ ys)))  ∎)
    where postulate iCantBeBothered : _

hamming : Stream ℕ
hamming = ContractiveFun.fixpoint hammingF

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Categories.Definition where

record Category {a b : _} : Set (lsuc (a ⊔ b)) where
  field
    objects : Set a
    arrows : objects → objects → Set b
    id : (x : objects) → arrows x x
    _∘_ : {x y z : objects} → arrows y z → arrows x y → arrows x z
    rightId : {x y : objects} → (f : arrows x y) → (id y) ∘ f ≡ f
    leftId : {x y : objects} → (f : arrows x y) → f ∘ (id x) ≡ f
    compositionAssociative : {x y z w : objects} → (f : arrows z w) → (g : arrows y z) → (h : arrows x y) → (f ∘ (g ∘ h)) ≡ (f ∘ g) ∘ h


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

-- The Simplex category Δ
module Categories.Category.Instance.Simplex where

open import Level using (0ℓ)
open import Data.Product
open import Data.Fin.Base using (Fin; zero; suc; _≤_; _<_; inject₁; punchIn)
open import Data.Nat.Base using (ℕ; zero; suc; z≤n; s≤s)
open import Function renaming (id to idF; _∘_ to _∙_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong)

open import Categories.Category.Core using (Category)

--------------------------------------------------------------------------------
-- The Simplex Category
--
-- Classically, the category Δ is defined as follows:
--   * Objects are Natural Numbers
--   * Morphisms 'm ⇒ n' are order-preserving maps 'Fin m → Fin n'
--
-- We _can_ define this version of Δ, but it is generally /not/ the version we want.
-- Most of the time we work with Δ, we only care about 2 classes of maps:
--   * Face maps 'δᵢ : n ⇒ (1 + n)' whose image omits 'i'
--   * Boundary maps 'σᵢ : (1 + n) ⇒ n' such that 'σᵢ i = σᵢ (i + 1) = i'
-- It turns out that all of the maps of Δ can be decomposed into compositions
-- of these 2 classes of maps[1], so most texts will define Functors out of Δ
-- based solely how they act on these morphisms.
--
-- Therefore, we want our definition of Δ to put these morphisms front and center,
-- by encoding our homs as follows:

infix 4 _Δ⇒_
infixr 9 _⊚_

data _Δ⇒_ : ℕ → ℕ → Set where
  ε  : ∀ {n} → n Δ⇒ n
  δ  : ∀ {n} → (i : Fin (suc n)) → n Δ⇒ (suc n)
  σ  : ∀ {n} → (j : Fin n) → (suc n) Δ⇒ n
  _⊚_ : ∀ {l m n} → m Δ⇒ n → l Δ⇒ m → l Δ⇒ n

-- However, this raises some tricky questions about equality of morphisms. It is tempting
-- to use the Simplical Identities[2] directly as our notion of equality:
--   * δᵢ ∘ δⱼ = δⱼ₊₁ ∘ δᵢ if i ≤ j
--   * σⱼ ∘ σᵢ = σᵢ ∘ σⱼ₊₁ if i ≤ j
--   * σⱼ ∘ δᵢ = δᵢ ∘ σⱼ₋₁ if i < j
--   * σⱼ ∘ δᵢ = id        if i = j or i = j + 1
--   * σⱼ ∘ δᵢ = δᵢ₋₁ ∘ σⱼ if j + 1 < i
--
-- However, working with these isn't exactly pleasant and will prove these
-- as theorems later. Instead of quotienting by these identities,
-- we appeal to the denotational semantics of our formal chains of morphisms.
-- In this case we interpret our morphisms as maps between finite ordinals:

face : ∀ {n} → Fin (ℕ.suc n) → Fin n → Fin (ℕ.suc n)
face = punchIn

degen : ∀ {n} → Fin n → Fin (ℕ.suc n) → Fin n
degen Fin.zero    Fin.zero    = Fin.zero
degen Fin.zero    (Fin.suc k) = k
degen (Fin.suc i) Fin.zero    = Fin.zero
degen (Fin.suc i) (Fin.suc k) = Fin.suc (degen i k)

⟦_⟧ : ∀ {m n} → m Δ⇒ n → (Fin m → Fin n)
⟦ ε ⟧ x = x
⟦ δ i ⟧ x = face i x
⟦ σ j ⟧ x = degen j x
⟦ f ⊚ g ⟧ x = ⟦ f ⟧ (⟦ g ⟧ x)

-- Now, we can define equality of morphisms by appealing to our semantics!
infix  4 _≗_

-- We wrap this in a record so that we don't compute away what the original morphsims were.
record _≗_ {m n} (f g : m Δ⇒ n) : Set where
  constructor Δ-eq
  field
    Δ-pointwise : ∀ {x} → ⟦ f ⟧ x ≡ ⟦ g ⟧ x

open _≗_ public

-- Now, we get the same benefits of being able to do induction on our input
-- arguments when trying to prove equalities, as well as being able to define functors
-- out of Δ via their action on face/degeneracy maps.

Δ : Category 0ℓ 0ℓ 0ℓ
Δ = record
  { Obj = ℕ
  ; _⇒_ = _Δ⇒_
  ; _≈_ = _≗_
  ; id = ε
  ; _∘_ = _⊚_
  ; assoc = Δ-eq refl
  ; sym-assoc = Δ-eq refl
  ; identityˡ = Δ-eq refl
  ; identityʳ = Δ-eq refl
  ; identity² = Δ-eq refl
  ; equiv = record
    { refl = Δ-eq refl
    ; sym = λ eq → Δ-eq (sym (Δ-pointwise eq))
    ; trans = λ eq₁ eq₂ → Δ-eq (trans (Δ-pointwise eq₁) (Δ-pointwise eq₂))
    }
  ; ∘-resp-≈ = λ {_ _ _ f g h i} eq₁ eq₂ → Δ-eq (trans (cong ⟦ f ⟧ (Δ-pointwise eq₂)) (Δ-pointwise eq₁))
  }

-- For completeness, here are the aforementioned simplical identities. These may seem /slightly/
-- different than the ones presented before, but it's just re-indexing to avoid having to use 'pred'.
open Category Δ

-- δᵢ ∘ δⱼ = δⱼ₊₁ ∘ δᵢ if i ≤ j
face-comm : ∀ {n} (i j : Fin (suc n))  → i ≤ j → δ (inject₁ i) ∘ δ j ≈ δ (suc j) ∘ δ i
face-comm zero    _       z≤n      = Δ-eq refl
face-comm (suc i) (suc j) (s≤s le) = Δ-eq (λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (face-comm i j le)) })

-- σⱼ ∘ σᵢ = σᵢ ∘ σⱼ₊₁ if i ≤ j
degen-comm : ∀ {n} (i j : Fin n) → i ≤ j → σ j ∘ σ (inject₁ i) ≈ σ i ∘ σ (suc j)
degen-comm zero    zero    z≤n      = Δ-eq λ { {zero} → refl ; {suc x} → refl }
degen-comm zero    (suc _) z≤n      = Δ-eq λ { {zero} → refl ; {suc x} → refl }
degen-comm (suc i) (suc j) (s≤s le) = Δ-eq (λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (degen-comm i j le)) })

-- σⱼ ∘ δᵢ = δᵢ ∘ σⱼ₋₁ if i < j
degen-face-comm : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i < suc j → σ (suc j) ∘ δ (inject₁ i) ≈ δ i ∘ σ j
degen-face-comm zero    _       (s≤s _)  = Δ-eq refl
degen-face-comm (suc i) (suc j) (s≤s le) = Δ-eq (λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (degen-face-comm i j le)) })

-- σⱼ ∘ δᵢ = id        if i = j
degen-face-id : ∀ {n} (i j : Fin n) → i ≡ j → σ j ∘ δ (inject₁ i) ≈ id
degen-face-id zero    zero    refl = Δ-eq refl
degen-face-id (suc i) (suc i) refl = Δ-eq (λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (degen-face-id i i refl)) })

-- σⱼ ∘ δᵢ = id        if i = j + 1
degen-face-suc-id : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i ≡ suc j → σ j ∘ δ i ≈ id
degen-face-suc-id (suc zero)    zero    refl = Δ-eq λ { {zero} → refl ; {suc x} → refl }
degen-face-suc-id (suc (suc i)) (suc i) refl = Δ-eq λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (degen-face-suc-id (suc i) i refl)) }

-- σⱼ ∘ δᵢ = δᵢ₋₁ ∘ σⱼ if j + 1 < i
degen-face-suc-comm : ∀ {n} (i : Fin (suc n)) (j : Fin n) → suc j < i → σ (inject₁ j) ∘ δ (suc i) ≈ δ i ∘ σ j
degen-face-suc-comm (suc (suc i)) zero  (s≤s (s≤s z≤n))   = Δ-eq (λ { {zero} → refl ; {suc x} → refl })
degen-face-suc-comm (suc (suc i)) (suc j) (s≤s le)        = Δ-eq (λ { {zero} → refl ; {suc x} → cong suc (Δ-pointwise (degen-face-suc-comm (suc i) j le)) })

-- Further Work:
-- If we had a means of decomposing any monotone map 'Fin n ⇒ Fin m' into a series of face/boundary
-- maps, we would be able to compute normal forms in Δ by using normalization by evaluation. This is
-- very promising, as it would let us define a reflection tactic to automatically perform
-- proofs about chains of morphisms in Δ.

-- Footnotes:
-- 1. For a proof of this, see Categories for The Working Mathematician VII.5
-- 2. See https://ncatlab.org/nlab/show/simplex+category

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Sums and cocartesian categories
module CategoryTheory.BCCCs.Cocartesian where

open import CategoryTheory.Categories

open import Relation.Binary using (IsEquivalence)

module _ {n} (ℂ : Category n) where

    open Category ℂ

    -- Initial object in a category
    record InitialObj : Set (lsuc n) where
        field
            -- | Data
            -- The initial object
            ⊥ : obj
            -- Canonical morphism
            ¡ : {A : obj} -> (⊥ ~> A)

            -- | Laws
            -- Need to show that the canonical morphism ! is unique
            ¡-unique : {A : obj} -> (m : ⊥ ~> A)
                  -> m ≈ ¡

    -- Sum of two objects
    -- Based on github.com/copumpkin/categories
    record Sum (A B : obj) : Set (lsuc n) where
        infix 10 [_⁏_]
        field
            -- | Data
            -- Sum of A and B
            A⊕B : obj
            -- First injection
            ι₁ : A ~> A⊕B
            -- Second injection
            ι₂ : B ~> A⊕B
            -- Canonical mediator
            [_⁏_] : ∀{S} -> (A ~> S) -> (B ~> S) -> (A⊕B ~> S)

            -- | Laws
            -- [_⁏_] expresses that given another candidate sum S
            -- and candidate injections to A and B there is a morphism
            -- from A⊕B to S. We need to check that this mediator makes
            -- the sum diagram commute and is unique.

            ι₁-comm : ∀{S} -> {i₁ : A ~> S} {i₂ : B ~> S}
                   -> [ i₁ ⁏ i₂ ] ∘ ι₁ ≈ i₁
            ι₂-comm : ∀{S} -> {i₁ : A ~> S} {i₂ : B ~> S}
                   -> [ i₁ ⁏ i₂ ] ∘ ι₂ ≈ i₂
            ⊕-unique  : ∀{S} -> {i₁ : A ~> S} {i₂ : B ~> S} {m : A⊕B ~> S}
                   -> m ∘ ι₁ ≈ i₁ -> m ∘ ι₂ ≈ i₂ -> [ i₁ ⁏ i₂ ] ≈ m

        -- η-expansion of function sums (via morphisms)
        ⊕-η-exp : ∀{S} -> {m : A⊕B ~> S}
               -> [ m ∘ ι₁ ⁏ m ∘ ι₂ ] ≈ m
        ⊕-η-exp = ⊕-unique r≈ r≈

        -- Summing of injection functions is the identity
        ⊕-η-id : [ ι₁ ⁏ ι₂ ] ≈ id
        ⊕-η-id = ⊕-unique id-left id-left

        -- Congruence over function summing
        [⁏]-cong : ∀{S} -> {i₁ j₁ : A ~> S} {i₂ j₂ : B ~> S}
               -> i₁ ≈ j₁ -> i₂ ≈ j₂
               -> [ i₁ ⁏ i₂ ] ≈ [ j₁ ⁏ j₂ ]
        [⁏]-cong pr1 pr2 = ⊕-unique (ι₁-comm ≈> pr1 [sym]) (ι₂-comm ≈> pr2 [sym])

-- Type class for cocartesian categories
record Cocartesian {n} (ℂ : Category n) : Set (lsuc n) where
    open Category ℂ
    field
        -- | Data
        -- Initial object
        init : InitialObj ℂ
        -- Binary sums for all pairs of objects
        sum : ∀(A B : obj) -> Sum ℂ A B

    open InitialObj init public
    open module S {A} {B} = Sum (sum A B) public

    -- Shorthand for sum object
    infixl 22 _⊕_
    _⊕_ : (A B : obj) -> obj
    A ⊕ B = A⊕B {A} {B}

    -- Parallel sum of morphisms
    infixl 65 _⊹_
    _⊹_ : {A B P Q : obj} -> (A ~> P) -> (B ~> Q)
       -> (A ⊕ B ~> P ⊕ Q)
    _⊹_ {A} {B} {P} {Q} f g = [ ι₁ ∘ f ⁏ ι₂ ∘ g ]

    -- Sum of three morphisms
    [_⁏_⁏_] : ∀{S A B C : obj} -> (A ~> S) -> (B ~> S) -> (C ~> S) -> (A ⊕ B ⊕ C ~> S)
    [ f ⁏ g ⁏ h ] = [ [ f ⁏ g ] ⁏ h ]

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 BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedHilbert where

open import BasicIPC.Syntax.ClosedHilbert public
open import BasicIPC.Semantics.TarskiGluedClosedHilbert public

-- Internalisation of syntax as syntax representation in a particular model.

module _ {{_ : Model}} where
  [_] : ∀ {A} → ⊢ A → [⊢] A
  [ app t u ] = [app] [ t ] [ u ]
  [ ci ]      = [ci]
  [ ck ]      = [ck]
  [ cs ]      = [cs]
  [ cpair ]   = [cpair]
  [ cfst ]    = [cfst]
  [ csnd ]    = [csnd]
  [ unit ]    = [unit]

-- Soundness with respect to all models, or evaluation, for closed terms only.

eval₀ : ∀ {A} → ⊢ A → ⊨ A
eval₀ (app t u) = eval₀ t ⟪$⟫ eval₀ u
eval₀ ci        = [ci] ⅋ I
eval₀ ck        = [ck] ⅋ ⟪K⟫
eval₀ cs        = [cs] ⅋ ⟪S⟫′
eval₀ cpair     = [cpair] ⅋ _⟪,⟫′_
eval₀ cfst      = [cfst] ⅋ π₁
eval₀ csnd      = [csnd] ⅋ π₂
eval₀ unit      = ∙

-- Correctness of evaluation with respect to conversion.

eval₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → eval₀ t ≡ eval₀ t′
eval₀✓ refl⋙           = refl
eval₀✓ (trans⋙ p q)    = trans (eval₀✓ p) (eval₀✓ q)
eval₀✓ (sym⋙ p)        = sym (eval₀✓ p)
eval₀✓ (congapp⋙ p q)  = cong² _⟪$⟫_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congi⋙ p)      = cong I (eval₀✓ p)
eval₀✓ (congk⋙ p q)    = cong² K (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congs⋙ p q r)  = cong³ ⟪S⟫ (eval₀✓ p) (eval₀✓ q) (eval₀✓ r)
eval₀✓ (congpair⋙ p q) = cong² _,_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congfst⋙ p)    = cong π₁ (eval₀✓ p)
eval₀✓ (congsnd⋙ p)    = cong π₂ (eval₀✓ p)
eval₀✓ beta▻ₖ⋙         = refl
eval₀✓ beta▻ₛ⋙         = refl
eval₀✓ beta∧₁⋙         = refl
eval₀✓ beta∧₂⋙         = refl
eval₀✓ eta∧⋙           = refl
eval₀✓ eta⊤⋙          = refl

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_    = λ P → ⊢ α P
      ; [⊢]_   = ⊢_
      ; [app]   = app
      ; [ci]    = ci
      ; [ck]    = ck
      ; [cs]    = cs
      ; [cpair] = cpair
      ; [cfst]  = cfst
      ; [csnd]  = csnd
      ; [unit]  = unit
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ⊨ A → ⊢ A
quot₀ s = reifyʳ s

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ⊢ A → ⊢ A
norm₀ = quot₀ ∘ eval₀

-- Correctness of normalisation with respect to conversion.

norm₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → norm₀ t ≡ norm₀ t′
norm₀✓ p = cong reifyʳ (eval₀✓ p)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- Andreas, 2012-04-18 make sure with functions of irrelevant functions
-- are also irrelevant
module IrrelevantWith where

import Common.Level
open import Common.Irrelevance

.unsq : ∀ {a}{A : Set a} → Squash A → A
unsq sq with Set
... | _ = unsquash sq

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Rationals.HITQ.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Relation.Nullary

open import Cubical.Data.Int

open import Cubical.Data.Nat as ℕ hiding (_·_)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

-- ℚ as a higher inductive type

data ℚ : Type₀ where
  con : (u : ℤ) (a : ℤ) → ¬ (a ≡ 0) → ℚ
  path : ∀ u a v b {p q} → (u · b) ≡ (v · a) → con u a p ≡ con v b q
  trunc : isSet ℚ

[_] : ℤ × ℕ₊₁ → ℚ
[ a , 1+ b ] = con a (pos (suc b)) (ℕ.snotz ∘ cong abs)

module Elim {ℓ} {B : ℚ → Type ℓ}
  (con* : ∀ u a (p : ¬ (a ≡ 0)) → B (con u a p))
  (path* : ∀ u a v b {p q} (eq : (u · b) ≡ (v · a))
    → PathP (λ i → B (path u a v b {p} {q} eq i)) (con* u a p) (con* v b q))
  (trunc* : (q : ℚ) → isSet (B q))
  where

  f : (q : ℚ) → B q
  f (con u a x) = con* u a x
  f (path u a v b x i) = path* u a v b x i
  f (trunc xs ys p q i j) =
    isOfHLevel→isOfHLevelDep 2 trunc*  (f xs) (f ys) (cong f p) (cong f q) (trunc xs ys p q) i j

module ElimProp {ℓ} {B : ℚ → Type ℓ} {BProp : {q : ℚ} → isProp (B q)}
  (con* : ∀ u a (p : ¬ (a ≡ 0)) → B (con u a p))
  where

  f : (q : ℚ) → B q
  f = Elim.f con*
    (λ u a v b {p} {q} eq →
      toPathP (BProp (transport (λ i → B (path u a v b eq i)) (con* u a p)) (con* v b q)))
    λ q → isProp→isSet BProp

module Rec {ℓ} {B : Type ℓ} {BType : isSet B}
  (con* : ∀ u a (p : ¬ (a ≡ 0)) → B)
  (path* : ∀ u a v b {p q} (eq : (u · b) ≡ (v · a))
    → con* u a p ≡ con* v b q) where

  f : ℚ → B
  f = Elim.f con* path* λ _ → BType

module Rec2 {ℓ} {B : Type ℓ} {BType : isSet B}
  (con* : ∀ u a (p : ¬ (a ≡ 0)) v b (q : ¬ (b ≡ 0)) → B)
  (path*₁ : ∀ u₁ a₁ {p₁}
    u₂ a₂ v₂ b₂ {p₂ q₂}
    (eq₁ : (u₁ · b₂) ≡ (v₂ · a₁))
    → con* u₁ a₁ p₁ u₂ a₂ p₂ ≡ con* v₂ b₂ q₂ u₂ a₂ p₂)
  (path*₂ : ∀ u₁ a₁ {p₁}
    u₂ a₂ v₂ b₂ {p₂ q₂}
    (eq₂ : (u₂ · b₂) ≡ (v₂ · a₂))
    → con* u₁ a₁ p₁ u₂ a₂ p₂ ≡ con* u₁ a₁ p₁ v₂ b₂ q₂)
  where

  f : ℚ → ℚ → B
  f = Rec.f {BType = λ x y p q i j w → BType (x w) (y w) (λ k → p k w) (λ k → q k w) i j}
    (λ u a p → Rec.f {BType = BType} (con* u a p) (path*₂ u a {p}))
    λ u a v b eq → funExt (ElimProp.f {BProp = BType _ _}
      λ u₂ a₂ p₂ → path*₁ _ _ _ _ _ _ eq)

--- Natural number and negative integer literals for ℚ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℚ : HasFromNat ℚ
  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → [ pos n , 1 ] }

instance
  fromNegℚ : HasFromNeg ℚ
  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ neg n , 1 ] }

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module Cubical.Data.Fin.Recursive where

open import Cubical.Data.Fin.Recursive.Base public
open import Cubical.Data.Fin.Recursive.Properties public


text:
------------------------------------------------------------------------
-- A small definition of a dependently typed language, using the
-- technique from McBride's "Outrageous but Meaningful Coincidences"
------------------------------------------------------------------------

{-# OPTIONS --type-in-type #-}

-- The code contains an example, a partial definition of categories,
-- which triggers the use of an enormous amount of memory (with the
-- development version of Agda which is current at the time of
-- writing). I'm not entirely sure if the code is correct: 2.5G heap
-- doesn't seem to suffice to typecheck this code. /NAD

module Language where

------------------------------------------------------------------------
-- Prelude

open import Prelude

subst : {A : Set} {x y : A} (P : A -> Set) ->
        x == y -> P x -> P y
subst P = J (\ x y _ -> P x -> P y) (\ x p -> p)

Empty : Set
Empty = (A : Set) -> A

record Unit : Set
record Unit where
  constructor tt

open Unit

data Either (A : Set) (B : Set) : Set
data Either A B where
  left  : A -> Either A B
  right : B -> Either A B

record Sigma (A : Set) (B : A -> Set) : Set
record Sigma A B where
  constructor pair
  field
    fst : A
    snd : B fst

open Sigma

uncurry : {A : Set} {B : A -> Set} {C : Sigma A B -> Set} ->
          ((x : A) (y : B x) -> C (pair x y)) ->
          ((p : Sigma A B) -> C p)
uncurry f p = f (fst p) (snd p)

Times : Set -> Set -> Set
Times A B = Sigma A (\ _ -> B)

------------------------------------------------------------------------
-- A universe

data U : Set

El : U -> Set

data U where
  set   : U
  el    : Set -> U
  sigma : (a : U) -> (El a -> U) -> U
  pi    : (a : U) -> (El a -> U) -> U

El set         = Set
El (el A)      = A
El (sigma a b) = Sigma (El a) (\ x -> El (b x))
El (pi a b)    = (x : El a) -> El (b x)

-- Abbreviations.

fun : U -> U -> U
fun a b = pi a (\ _ -> b)

times : U -> U -> U
times a b = sigma a (\ _ -> b)

-- Example.

raw-categoryU : U
raw-categoryU =
  sigma set (\ obj ->
  sigma (fun (el obj) (fun (el obj) set)) (\ hom ->
  times
    (pi (el obj) (\ x -> el (hom x x)))
    (pi (el obj) (\ x -> pi (el obj) (\ y -> pi (el obj) (\ z ->
       fun (el (hom x y)) (fun (el (hom y z)) (el (hom x z)))))))))

------------------------------------------------------------------------
-- Contexts

-- Contexts.

data Ctxt : Set

-- Types.

Ty : Ctxt -> Set

-- Environments.

Env : Ctxt -> Set

data Ctxt where
  empty : Ctxt
  snoc  : (G : Ctxt) -> Ty G -> Ctxt

Ty G = Env G -> U

Env empty      = Unit
Env (snoc G s) = Sigma (Env G) (\ g -> El (s g))

-- Variables (de Bruijn indices).

Var : (G : Ctxt) -> Ty G -> Set
Var empty      t = Empty
Var (snoc G s) t =
  Either ((\ g -> s (fst g)) == t)
         (Sigma _ (\ u -> Times ((\ g -> u (fst g)) == t) (Var G u)))

zero : {G : _} {s : _} ->
       Var (snoc G s) (\ g -> s (fst g))
zero = left refl

suc : {G : _} {s : _} {t : _}
      (x : Var G t) ->
      Var (snoc G s) (\ g -> t (fst g))
suc x = right (pair _ (pair refl x))

-- A lookup function.

lookup : (G : Ctxt) (s : Ty G) -> Var G s -> (g : Env G) -> El (s g)
lookup empty      _ absurd     _ = absurd _
lookup (snoc _ _) _ (left  eq) g = subst (\ f -> El (f g)) eq (snd g)
lookup (snoc _ _) t (right p)  g =
  subst (\ f -> El (f g)) (fst (snd p)) (lookup _ _ (snd (snd p)) (fst g))

{-

------------------------------------------------------------------------
-- A language

-- Syntax for types.

data Type (G : Ctxt) (s : Ty G) : Set

-- Terms.

data Term (G : Ctxt) (s : Ty G) : Set

-- The semantics of a term.

eval : {G : _} {s : _} -> Term G s -> (g : Env G) -> El (s g)

data Type G s where
  set''   : s == (\ _ -> set) -> Type G s
  el''    : (x : Term G (\ _ -> set)) ->
            (\ g -> el (eval x g)) == s ->
            Type G s
  sigma'' : {t : _} {u : _} ->
            Type G t ->
            Type (snoc G t) u ->
            (\ g -> sigma (t g) (\ v -> u (pair g v))) == s ->
            Type G s
  pi''    : {t : _} {u : _} ->
            Type G t ->
            Type (snoc G t) u ->
            (\ g -> pi (t g) (\ v -> u (pair g v))) == s ->
            Type G s

data Term G s where
  var   : Var G s -> Term G s
  lam'' : {t : _} {u : _} ->
          Term (snoc G t) (uncurry u) ->
          (\ g -> pi (t g) (\ v -> u g v)) == s ->
          Term G s
  app'' : {t : _} {u : (g : Env G) -> El (t g) -> U} ->
          Term G (\ g -> pi (t g) (\ v -> u g v)) ->
          (t2 : Term G t) ->
          (\ g -> u g (eval t2 g)) == s ->
          Term G s

eval (var x)          g = lookup _ _ x g
eval (lam'' t eq)     g = subst (\ f -> El (f g)) eq
                            (\ v -> eval t (pair g v))
eval (app'' t1 t2 eq) g = subst (\ f -> El (f g)) eq
                            (eval t1 g (eval t2 g))

-- Abbreviations.

set' : {G : _} -> Type G (\ _ -> set)
set' = set'' refl

el' : {G : _}
      (x : Term G (\ _ -> set)) ->
      Type G (\ g -> el (eval x g))
el' x = el'' x refl

sigma' : {G : _} {t : _} {u : _} ->
         Type G t ->
         Type (snoc G t) u ->
         Type G (\ g -> sigma (t g) (\ v -> u (pair g v)))
sigma' s t = sigma'' s t refl

pi' : {G : _} {t : _} {u : _} ->
      Type G t ->
      Type (snoc G t) u ->
      Type G (\ g -> pi (t g) (\ v -> u (pair g v)))
pi' s t = pi'' s t refl

lam : {G : _} {t : _} {u : _} ->
      Term (snoc G t) (uncurry u) ->
      Term G (\ g -> pi (t g) (\ v -> u g v))
lam t = lam'' t refl

app : {G : _} {t : _} {u : (g : Env G) -> El (t g) -> U} ->
      Term G (\ g -> pi (t g) (\ v -> u g v)) ->
      (t2 : Term G t) ->
      Term G (\ g -> u g (eval t2 g))
app t1 t2 = app'' t1 t2 refl

-- Example.

raw-category : Type empty (\ _ -> raw-categoryU)
raw-category =
     -- Objects.
   sigma' set'
     -- Morphisms.
  (sigma' (pi' (el' (var zero)) (pi' (el' (var (suc zero))) set'))
     -- Identity.
  (sigma' (pi' (el' (var (suc zero)))
               (el' (app (app (var (suc zero)) (var zero)) (var zero))))
     -- Composition.
     (pi' (el' (var (suc (suc zero))))                                 -- X.
     (pi' (el' (var (suc (suc (suc zero)))))                           -- Y.
     (pi' (el' (var (suc (suc (suc (suc zero))))))                     -- Z.
     (pi' (el' (app (app (var (suc (suc (suc (suc zero)))))
                         (var (suc (suc zero))))
                    (var (suc zero))))                                 -- Hom X Y.
     (pi' (el' (app (app (var (suc (suc (suc (suc (suc zero))))))
                         (var (suc (suc zero))))
                    (var (suc zero))))                                 -- Hom Y Z.
          (el' (app (app (var (suc (suc (suc (suc (suc (suc zero)))))))
                         (var (suc (suc (suc (suc zero))))))
                    (var (suc (suc zero))))))                          -- Hom X Z.
  ))))))
-}

max_stars_repo_name: larrytheliquid/agda


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

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Groups.Definition
open import Groups.Lemmas
open import Fields.Fields
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Semirings.Definition
open import Numbers.Modulo.Definition
open import Orders.Total.Definition

module Fields.CauchyCompletion.BaseExpansion {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

open Setoid S
open SetoidTotalOrder (TotallyOrderedRing.total order)
open SetoidPartialOrder pOrder
open Equivalence eq
open PartiallyOrderedRing pRing
open Ring R
open Group additiveGroup
open Field F
open import Fields.Orders.Limits.Definition {F = F} (record { oRing = order })
open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
open import Fields.Orders.Limits.Lemmas {F = F} (record { oRing = order })

open import Fields.Lemmas F
open import Fields.Orders.Lemmas {F = F} record { oRing = order }
open import Rings.Orders.Total.Lemmas order
open import Rings.Orders.Total.AbsoluteValue order
open import Rings.Orders.Partial.Lemmas pRing
open import Fields.CauchyCompletion.Definition order F
open import Fields.CauchyCompletion.Setoid order F
open import Fields.CauchyCompletion.Addition order F
open import Fields.CauchyCompletion.Comparison order F
open import Fields.CauchyCompletion.Approximation order F
open import Rings.InitialRing R
open import Rings.Orders.Partial.Bounded pRing
open import Rings.Orders.Total.Bounded order
open import Rings.Orders.Total.Cauchy order

-- TODO this is not necessarily true :( the bounded sequence could oscillate between 1 and -1
cauchyTimesBoundedIsCauchy : {s : Sequence A} → cauchy s → {t : Sequence A} → Bounded t → cauchy (apply _*_ s t)
cauchyTimesBoundedIsCauchy {s} cau {t} (K , bounded) e 0<e with allInvertible K (boundNonzero (K , bounded))
... | 1/K , prK with cau (1/K * e) (orderRespectsMultiplication (reciprocalPositive K 1/K (boundGreaterThanZero (K , bounded)) (transitive *Commutative prK)) 0<e)
... | N , cauPr = N , ans
  where
    ans : {m n : ℕ} (N<m : N <N m) (N<n : N <N n) → (abs (index (apply _*_ s t) m + inverse (index (apply _*_ s t) n))) < e
    ans N<m N<n with cauPr N<m N<n
    ... | r = {!!}

boundedTimesCauchyIsCauchy : {s : Sequence A} → cauchy s → {t : Sequence A} → Bounded t → cauchy (apply _*_ t s)
boundedTimesCauchyIsCauchy {s} cau {t} bou = cauchyWellDefined (ans s t) (cauchyTimesBoundedIsCauchy cau bou)
  where
    ans : (s t : Sequence A) (m : ℕ) → index (apply _*_ s t) m ∼ index (apply _*_ t s) m
    ans s t m rewrite indexAndApply t s _*_ {m} | indexAndApply s t _*_ {m} = *Commutative

private
  digitExpansionSeq : {n : ℕ} → .(0<n : 0 <N n) → Sequence (ℤn n 0<n) → Sequence A
  Sequence.head (digitExpansionSeq {n} 0<n seq) = fromN (ℤn.x (Sequence.head seq))
  Sequence.tail (digitExpansionSeq {n} 0<n seq) = digitExpansionSeq 0<n (Sequence.tail seq)

  powerSeq : (i : A) → (start : A) → Sequence A
  Sequence.head (powerSeq i start) = start
  Sequence.tail (powerSeq i start) = powerSeq i (start * i)

  powerSeqInduction : (i : A) (start : A) → (m : ℕ) → (index (powerSeq i start) (succ m)) ∼ i * (index (powerSeq i start) m)
  powerSeqInduction i start zero = *Commutative
  powerSeqInduction i start (succ m) = powerSeqInduction i (start * i) m

  ofBaseExpansionSeq : {n : ℕ} → .(0<n : 0 <N n) → Sequence (ℤn n 0<n) → Sequence A
  ofBaseExpansionSeq {succ n} 0<n seq = apply _*_ (digitExpansionSeq 0<n seq) (powerSeq pow pow)
    where
      pow : A
      pow = underlying (allInvertible (fromN (succ n)) (charNotN n))

  powerSeqPositive : {i : A} → (0R < i) → {s : A} → (0R < s) → (m : ℕ) → 0R < index (powerSeq i s) m
  powerSeqPositive {i} 0<i {s} 0<s zero = 0<s
  powerSeqPositive {i} 0<i {s} 0<s (succ m) = <WellDefined reflexive (symmetric (powerSeqInduction i s m)) (orderRespectsMultiplication 0<i (powerSeqPositive 0<i 0<s m))

  powerSeqConvergesTo0 : (i : A) → (0R < i) → (i < 1R) → {s : A} → (0R < s) → (powerSeq i s) ~> 0G
  powerSeqConvergesTo0 i 0<i i<1 {s} 0<s e 0<e = {!!}

  powerSeqConverges : (i : A) → (0R < i) → (i < 1R) → {s : A} → (0R < s) → cauchy (powerSeq i s)
  powerSeqConverges i 0<i i<1 {s} 0<s = convergentSequenceCauchy nontrivial {r = 0R} (powerSeqConvergesTo0 i 0<i i<1 0<s)

  0<n : {n : ℕ} → 1 <N n → 0 <N n
  0<n 1<n = TotalOrder.<Transitive ℕTotalOrder (le 0 refl) 1<n

  digitExpansionBoundedLemma : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → index (digitExpansionSeq _ seq) m < fromN n
  digitExpansionBoundedLemma {n} 0<n seq zero with Sequence.head seq
  ... | record { x = x ; xLess = xLess } = fromNPreservesOrder (0<1 nontrivial) {x} {n} ((squash<N xLess))
  digitExpansionBoundedLemma 0<n seq (succ m) = digitExpansionBoundedLemma 0<n (Sequence.tail seq) m

  digitExpansionBoundedLemma2 : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → inverse (fromN n) < index (digitExpansionSeq 0<n seq) m
  digitExpansionBoundedLemma2 {n} 0<n seq zero = <WellDefined identLeft (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition {_} {fromN (ℤn.x (Sequence.head seq)) + fromN n} (<WellDefined reflexive (fromNPreserves+ (ℤn.x (Sequence.head seq)) n) (fromNPreservesOrder (0<1 nontrivial) {0} {ℤn.x (Sequence.head seq) +N n} (canAddToOneSideOfInequality' _ (squash<N 0<n)))) (inverse (fromN n)))
  digitExpansionBoundedLemma2 0<n seq (succ m) = digitExpansionBoundedLemma2 0<n (Sequence.tail seq) m

  digitExpansionBounded : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → Bounded (digitExpansionSeq 0<n seq)
  digitExpansionBounded {n} 0<n seq = fromN n , λ m → ((digitExpansionBoundedLemma2 0<n seq m) ,, digitExpansionBoundedLemma 0<n seq m)

private
  1/nPositive : (n : ℕ) → 0R < underlying (allInvertible (fromN (succ n)) (charNotN n))
  1/nPositive n with allInvertible (fromN (succ n)) (charNotN n)
  ... | a , b = reciprocalPositive (fromN (succ n)) a (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)) (transitive *Commutative b)

  1/n<1 : (n : ℕ) → (0 <N n) → underlying (allInvertible (fromN (succ n)) (charNotN n)) < 1R
  1/n<1 n 1<n with allInvertible (fromN (succ n)) (charNotN n)
  ... | a , b = reciprocal<1 (fromN (succ n)) a (<WellDefined identRight reflexive (fromNPreservesOrder (0<1 nontrivial) {1} {succ n} (succPreservesInequality 1<n))) (transitive *Commutative b)

-- Construct the real that is the given base-n expansion between 0 and 1.
ofBaseExpansion : {n : ℕ} → .(1<n : 1 <N n) → (fromN n ∼ 0R → False) → Sequence (ℤn n (0<n 1<n)) → CauchyCompletion
ofBaseExpansion {succ n} 1<n charNotN seq = record { elts = ofBaseExpansionSeq (0<n 1<n) seq ; converges = boundedTimesCauchyIsCauchy (powerSeqConverges _ (1/nPositive n) (1/n<1 n (canRemoveSuccFrom<N (squash<N 1<n))) (1/nPositive n)) (digitExpansionBounded (0<n 1<n) seq)}

toBaseExpansion : {n : ℕ} → .(1<n : 1 <N n) → (fromN n ∼ 0R → False) → (a : CauchyCompletion) → 0R r<C a → a <Cr 1R → Sequence (ℤn n (0<n 1<n))
Sequence.head (toBaseExpansion {n} 1<n charNotN c 0<c c<1) = {!!}
 -- TOOD: approximate c to within 1/n^2, extract the first decimal of the result.
Sequence.tail (toBaseExpansion {n} 1<n charNotN c 0<c c<1) = toBaseExpansion 1<n charNotN {!!} {!!} {!!}

baseExpansionProof : {n : ℕ} → .{1<n : 1 <N n} → {charNotN : fromN n ∼ 0R → False} → (as : CauchyCompletion) → (0<a : 0R r<C as) → (a<1 : as <Cr 1R) → Setoid._∼_ cauchyCompletionSetoid (ofBaseExpansion 1<n charNotN (toBaseExpansion 1<n charNotN as 0<a a<1)) as
baseExpansionProof = {!!}


text:
module Builtin.Reflection where

open import Prelude hiding (abs)
open import Prelude.Equality.Unsafe
open import Builtin.Float
open import Container.Traversable
open import Control.Monad.Zero

open import Agda.Builtin.Reflection as Builtin
open Builtin public
  hiding ( primQNameEquality
         ; primQNameLess
         ; primShowQName
         ; primMetaEquality
         ; primMetaLess
         ; primShowMeta )

--- Names ---

instance
  ShowName : Show Name
  showsPrec {{ShowName}} _ x = showString (primShowQName x)

instance
  EqName : Eq Name
  _==_ {{EqName}} x y with primQNameEquality x y
  ... | true  = yes unsafeEqual
  ... | false = no unsafeNotEqual

data LessName (x y : Name) : Set where
  less-name : primQNameLess x y ≡ true → LessName x y

private
  cmpName : ∀ x y → Comparison LessName x y
  cmpName x y with inspect (primQNameLess x y)
  ... | true  with≡ eq = less (less-name eq)
  ... | false with≡ _  with inspect (primQNameLess y x)
  ...   | true with≡ eq = greater (less-name eq)
  ...   | false with≡ _ = equal unsafeEqual

instance
  OrdName : Ord Name
  OrdName = defaultOrd cmpName

  OrdLawsName : Ord/Laws Name
  Ord/Laws.super OrdLawsName    = it
  less-antirefl {{OrdLawsName}} (less-name eq) = unsafeNotEqual eq
  less-trans    {{OrdLawsName}} (less-name _)  (less-name _)   = less-name unsafeEqual

--- Meta variables ---

instance
  ShowMeta : Show Meta
  showsPrec {{ShowMeta}} _ x = showString (primShowMeta x)

instance
  EqMeta : Eq Meta
  _==_ {{EqMeta}} x y with primMetaEquality x y
  ... | true  = yes unsafeEqual
  ... | false = no  unsafeNotEqual

data LessMeta (x y : Meta) : Set where
  less-meta : primMetaLess x y ≡ true → LessMeta x y

private
  cmpMeta : ∀ x y → Comparison LessMeta x y
  cmpMeta x y with inspect (primMetaLess x y)
  ... | true  with≡ eq = less (less-meta eq)
  ... | false with≡ _  with inspect (primMetaLess y x)
  ...   | true with≡ eq = greater (less-meta eq)
  ...   | false with≡ _ = equal unsafeEqual

instance
  OrdMeta : Ord Meta
  OrdMeta = defaultOrd cmpMeta

  OrdLawsMeta : Ord/Laws Meta
  Ord/Laws.super OrdLawsMeta = it
  less-antirefl {{OrdLawsMeta}} (less-meta eq) = unsafeNotEqual eq
  less-trans    {{OrdLawsMeta}} (less-meta _)  (less-meta _)   = less-meta unsafeEqual

--- Literals ---

instance
  ShowLiteral : Show Literal
  showsPrec {{ShowLiteral}} _ (nat n)    = shows n
  showsPrec {{ShowLiteral}} _ (word64 n) = shows n
  showsPrec {{ShowLiteral}} _ (float x)  = shows x
  showsPrec {{ShowLiteral}} _ (char c)   = shows c
  showsPrec {{ShowLiteral}} _ (string s) = shows s
  showsPrec {{ShowLiteral}} _ (name x)   = shows x
  showsPrec {{ShowLiteral}} _ (meta x)   = shows x

--- Terms ---

pattern vArg x = arg (arg-info visible relevant) x
pattern hArg x = arg (arg-info hidden relevant) x
pattern iArg x = arg (arg-info instance′ relevant) x

unArg : ∀ {A} → Arg A → A
unArg (arg _ x) = x

getArgInfo : ∀ {A} → Arg A → ArgInfo
getArgInfo (arg i _) = i

getVisibility : ∀ {A} → Arg A → Visibility
getVisibility (arg (arg-info v _) _) = v

getRelevance : ∀ {A} → Arg A → Relevance
getRelevance (arg (arg-info _ r) _) = r

isVisible : ∀ {A} → Arg A → Bool
isVisible (arg (arg-info visible _) _) = true
isVisible _ = false

instance
  FunctorArg : Functor Arg
  fmap {{FunctorArg}} f (arg i x) = arg i (f x)

  TraversableArg : Traversable Arg
  traverse {{TraversableArg}} f (arg i x) = ⦇ (arg i) (f x) ⦈

unAbs : ∀ {A} → Abs A → A
unAbs (abs _ x) = x

instance
  FunctorAbs : Functor Abs
  fmap {{FunctorAbs}} f (abs s x) = abs s (f x)

  TraversableAbs : Traversable Abs
  traverse {{TraversableAbs}} f (abs s x) = ⦇ (abs s) (f x) ⦈

absurd-lam : Term
absurd-lam = pat-lam (absurd-clause (vArg absurd ∷ []) ∷ []) []

--- TC monad ---

mapTC : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → TC A → TC B
mapTC f m = bindTC m λ x → returnTC (f x)

instance
  FunctorTC : ∀ {a} → Functor {a} TC
  fmap {{FunctorTC}} = mapTC

  ApplicativeTC : ∀ {a} → Applicative {a} TC
  pure  {{ApplicativeTC}} = returnTC
  _<*>_ {{ApplicativeTC}} = monadAp bindTC

  MonadTC : ∀ {a} → Monad {a} TC
  _>>=_  {{MonadTC}} = bindTC

  FunctorTC′ : ∀ {a b} → Functor′ {a} {b} TC
  fmap′ {{FunctorTC′}} = mapTC

  ApplicativeTC′ : ∀ {a b} → Applicative′ {a} {b} TC
  _<*>′_ {{ApplicativeTC′}} = monadAp′ bindTC

  MonadTC′ : ∀ {a b} → Monad′ {a} {b} TC
  _>>=′_ {{MonadTC′}} = bindTC

  FunctorZeroTC : ∀ {a} → FunctorZero {a} TC
  empty {{FunctorZeroTC}} = typeError []

  AlternativeTC : ∀ {a} → Alternative {a} TC
  _<|>_ {{AlternativeTC}} = catchTC

Tactic = Term → TC ⊤

give : Term → Tactic
give v = λ hole → unify hole v

define : Arg Name → Type → List Clause → TC ⊤
define f a cs = declareDef f a >> defineFun (unArg f) cs

newMeta : Type → TC Term
newMeta = checkType unknown

newMeta! : TC Term
newMeta! = newMeta unknown

typeErrorS : ∀ {a} {A : Set a} → String → TC A
typeErrorS s = typeError (strErr s ∷ [])

blockOnMeta! : ∀ {a} {A : Set a} → Meta → TC A
blockOnMeta! x = commitTC >>=′ λ _ → blockOnMeta x

inferNormalisedType : Term → TC Type
inferNormalisedType t = withNormalisation true (inferType t)

--- Convenient wrappers ---

-- Zero for non-datatypes
getParameters : Name → TC Nat
getParameters d =
  caseM getDefinition d of λ
  { (data-type n _) → pure n
  ; _ → pure 0 }

getConstructors : Name → TC (List Name)
getConstructors d =
  caseM getDefinition d of λ
  { (data-type _ cs) → pure cs
  ; (record-type c _) → pure (c ∷ [])
  ; _ → typeError (strErr "Cannot get constructors of non-data or record type" ∷ nameErr d ∷ [])
  }

getClauses : Name → TC (List Clause)
getClauses d =
  caseM getDefinition d of λ
  { (function cs) → pure cs
  ; _ → typeError (strErr "Cannot get constructors of non-function type" ∷ nameErr d ∷ [])
  }

-- Get the constructor of a record type (or single-constructor data type)
recordConstructor : Name → TC Name
recordConstructor r =
  caseM getConstructors r of λ
  { (c ∷ []) → pure c
  ; _ → typeError $ strErr "Cannot get constructor of non-record type" ∷ nameErr r ∷ [] }

-- Injectivity of constructors

arg-inj₁ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → i ≡ i′
arg-inj₁ refl = refl

arg-inj₂ : ∀ {A i i′} {x x′ : A} → arg i x ≡ arg i′ x′ → x ≡ x′
arg-inj₂ refl = refl

arg-info-inj₁ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
arg-info-inj₁ refl = refl

arg-info-inj₂ : ∀ {v v′ r r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
arg-info-inj₂ refl = refl

abs-inj₁ : ∀ {A s s′} {x x′ : A} → abs s x ≡ abs s′ x′ → s ≡ s′
abs-inj₁ refl = refl

abs-inj₂ : ∀ {A s s′} {x x′ : A} → abs s x ≡ abs s′ x′ → x ≡ x′
abs-inj₂ refl = refl

--- Terms ---

var-inj₁ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → x ≡ x′
var-inj₁ refl = refl

var-inj₂ : ∀ {x x′ args args′} → Term.var x args ≡ var x′ args′ → args ≡ args′
var-inj₂ refl = refl

con-inj₁ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → c ≡ c′
con-inj₁ refl = refl

con-inj₂ : ∀ {c c′ args args′} → Term.con c args ≡ con c′ args′ → args ≡ args′
con-inj₂ refl = refl

def-inj₁ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′
def-inj₁ refl = refl

def-inj₂ : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → args ≡ args′
def-inj₂ refl = refl

meta-inj₁ : ∀ {f f′ args args′} → Term.meta f args ≡ meta f′ args′ → f ≡ f′
meta-inj₁ refl = refl

meta-inj₂ : ∀ {f f′ args args′} → Term.meta f args ≡ meta f′ args′ → args ≡ args′
meta-inj₂ refl = refl

lam-inj₁ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′
lam-inj₁ refl = refl

lam-inj₂ : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → t ≡ t′
lam-inj₂ refl = refl

pat-lam-inj₁ : ∀ {v v′ t t′} → pat-lam v t ≡ pat-lam v′ t′ → v ≡ v′
pat-lam-inj₁ refl = refl

pat-lam-inj₂ : ∀ {v v′ t t′} → pat-lam v t ≡ pat-lam v′ t′ → t ≡ t′
pat-lam-inj₂ refl = refl

pi-inj₁ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′
pi-inj₁ refl = refl

pi-inj₂ : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₂ ≡ t₂′
pi-inj₂ refl = refl

sort-inj : ∀ {x y} → agda-sort x ≡ agda-sort y → x ≡ y
sort-inj refl = refl

lit-inj : ∀ {x y} → Term.lit x ≡ lit y → x ≡ y
lit-inj refl = refl

--- Sorts ---

set-inj : ∀ {x y} → set x ≡ set y → x ≡ y
set-inj refl = refl

slit-inj : ∀ {x y} → Sort.lit x ≡ lit y → x ≡ y
slit-inj refl = refl

--- Patterns ---

pcon-inj₁ : ∀ {x y z w} → Pattern.con x y ≡ con z w → x ≡ z
pcon-inj₁ refl = refl

pcon-inj₂ : ∀ {x y z w} → Pattern.con x y ≡ con z w → y ≡ w
pcon-inj₂ refl = refl

pvar-inj : ∀ {x y} → Pattern.var x ≡ var y → x ≡ y
pvar-inj refl = refl

plit-inj : ∀ {x y} → Pattern.lit x ≡ lit y → x ≡ y
plit-inj refl = refl

proj-inj : ∀ {x y} → Pattern.proj x ≡ proj y → x ≡ y
proj-inj refl = refl

--- Clauses ---

clause-inj₁ : ∀ {x y z w} → clause x y ≡ clause z w → x ≡ z
clause-inj₁ refl = refl

clause-inj₂ : ∀ {x y z w} → clause x y ≡ clause z w → y ≡ w
clause-inj₂ refl = refl

absurd-clause-inj : ∀ {x y} → absurd-clause x ≡ absurd-clause y → x ≡ y
absurd-clause-inj refl = refl

--- Literals ---

nat-inj : ∀ {x y} → nat x ≡ nat y → x ≡ y
nat-inj refl = refl

word64-inj : ∀ {x y} → word64 x ≡ word64 y → x ≡ y
word64-inj refl = refl

float-inj : ∀ {x y} → float x ≡ float y → x ≡ y
float-inj refl = refl

char-inj : ∀ {x y} → char x ≡ char y → x ≡ y
char-inj refl = refl

string-inj : ∀ {x y} → string x ≡ string y → x ≡ y
string-inj refl = refl

name-inj : ∀ {x y} → name x ≡ name y → x ≡ y
name-inj refl = refl

meta-inj : ∀ {x y} → Literal.meta x ≡ meta y → x ≡ y
meta-inj refl = refl

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
-- Strict A is a datatype isomorphic to A, with constructor ! : A → Strict A
-- Semantically it has no impact, but its constructor is strict, so it can be
-- used to force evaluation of a term to whnf by pattern-matching.

open import Data.Strict.Primitive using ()

module Data.Strict where

open Data.Strict.Primitive public using ( Strict ; ! )

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Container.Relation.Unary.Any directly.
------------------------------------------------------------------------

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

module Data.Container.Any where

open import Data.Container.Relation.Unary.Any public
open import Data.Container.Relation.Unary.Any.Properties public


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

module Invertibility where

open import Size
open import Codata.Delay renaming (length to dlength ; map to dmap )
open import Codata.Thunk using (Thunk ; force)
open import Relation.Binary.PropositionalEquality
open import Data.Vec.Relation.Unary.All using (All ; [] ; _∷_)

open import Data.Product

open import Syntax
open import Value
open import Definitional

open import Data.List using (List ; [] ; _∷_ ; length)
open import Data.Vec  using ([] ; _∷_)

open import Level renaming (zero to lzero ; suc to lsuc)
open import Function using () renaming (case_of_ to CASE_OF_)

open import Relation.Nullary
open import Data.Empty

open import PInj
open _⊢F_⇔_

-- m ⟶ v states that computation of m terminates in v, which is
-- suitable for structural induction more than ⇓.
data _⟶_ : {A : Set} (m : DELAY A ∞) (v : A) -> Set₁ where
  now⟶   : ∀ {A : Set} (v : A) -> Now v ⟶ v
  later⟶ : ∀ {A : Set} {x : Thunk (DELAY A) ∞} -> ∀ (v : A)
             -> (ev : force x ⟶ v)
             -> Later x ⟶ v
  bind⟶ :
    ∀ {A B : Set} {m : DELAY A ∞} {f : A -> DELAY B ∞} (u : A) (v : B)
    -> m ⟶ u
    -> f u ⟶ v
    -> Bind m f ⟶ v

-- We will check that m ⟶ v conincides with the termination of thawed
-- computation (d : runD m ⇓) that results in v (that is, extract d ≡
-- v).

module _ where
  open import Data.Nat
  open import Data.Nat.Properties
  private
    -- It is unclear that we can prove the statement ⇓-⟶ by the
    -- indunction on m⇓, as it is not immediately clear that m⇓ does
    -- not involve infinite number of binds. So, we base ourselves on
    -- the number of 'later' and prove that the descruction of "bind"
    -- cannot increase the number ('lemma', below).

    -- steps
    len : ∀ {A : Set} {m : Delay A ∞} -> m ⇓ -> ℕ
    len (now _)   = ℕ.zero
    len (later x) = ℕ.suc (len x)

    -- Destruction cannot increase "steps"
    lemma :
      ∀ {A B : Set} -> (m : Delay A ∞) (f : A -> Delay B ∞)
      -> (mf⇓ : bind m f ⇓) -> Σ (m ⇓) λ m⇓ → Σ (f (extract m⇓) ⇓) λ fu⇓ -> (extract mf⇓ ≡ extract fu⇓ × len m⇓ ≤ len mf⇓ × len fu⇓ ≤ len mf⇓)
    lemma (now x) f bd = (now x) , bd , refl , z≤n , ≤-refl
    lemma (later x) f (later bd) with lemma (force x) f bd
    ... | m⇓ , f⇓ , eq , rel₁ , rel₂ = later m⇓ , f⇓ , eq , s≤s rel₁ , ≤-step rel₂

    -- A generalized statement for induction.
    aux : ∀ {A : Set} n -> (m : DELAY A ∞) -> (m⇓ : runD m ⇓) -> len m⇓ ≤ n -> m ⟶ extract m⇓
    aux n (Now x) (now .x) ctr = now⟶ x
    aux zero    (Later x) (later m⇓) ()
    aux (suc n) (Later x) (later m⇓) (s≤s ctr) = later⟶ _ (aux n (force x) m⇓ ctr)
    aux n (Bind m f) mf⇓ ctr with lemma (runD m) _ mf⇓
    ... | m⇓ , fu⇓ , eq , rel₁ , rel₂ with aux n m m⇓ (≤-trans rel₁ ctr)
    ... | m⟶u with aux n (f (extract m⇓)) fu⇓ (≤-trans rel₂ ctr)
    ... | fu⟶v rewrite eq = bind⟶ {m = m} {f} (extract m⇓) (extract fu⇓) m⟶u fu⟶v

  ⇓-⟶ : ∀ {A : Set} (m : DELAY A ∞)  -> (m⇓ : runD m ⇓) -> m ⟶ extract m⇓
  ⇓-⟶ m m⇓ = aux (len m⇓) m m⇓ (≤-refl)

-- In contrast, the opposite direction is straightforward, thanks to
-- the frozen bind.
⟶-⇓ : ∀ {A : Set} (m : DELAY A ∞) (v : A)
        -> m ⟶ v -> Σ[ m⇓ ∈ runD m ⇓ ] (extract m⇓ ≡ v)
⟶-⇓ .(Now v) v (now⟶ .v) = now v , refl
⟶-⇓ .(Later _) v (later⟶ .v m⟶v) with ⟶-⇓ _ v m⟶v
... | m⇓ , refl = later m⇓ , refl
⟶-⇓ .(Bind m f) v (bind⟶ {m = m} {f} u .v m⟶u fu⟶v)
  with ⟶-⇓ _ u m⟶u | ⟶-⇓ _ v fu⟶v
... | m⇓ , refl | fu⇓ , refl = bind-⇓ m⇓ fu⇓ , lemma m⇓ fu⇓
  where
    lemma :
      ∀ {ℓ} {A B : Set ℓ} {m : Delay A ∞} {f : A → Delay B ∞}
      -> (m⇓ : m ⇓) -> (fu⇓ : f (extract m⇓) ⇓)
      -> extract (bind-⇓ m⇓ {f = f} fu⇓) ≡ extract fu⇓
    lemma (now a) fu⇓ = refl
    lemma {f = f} (later m⇓) fu⇓ rewrite lemma {f = f} m⇓ fu⇓ = refl

-- Never does not terminate.
¬Never⟶ : ∀ {A : Set} {v : A} -> ¬ (Never ⟶ v)
¬Never⟶ (later⟶ _ x) = ¬Never⟶ x

-- A useful variant of now⟶
now⟶≡ : ∀ {A : Set} {v v' : A} -> v' ≡ v -> Now v' ⟶ v
now⟶≡ refl = now⟶ _

-- Several properties on value environments (for forward and backward
-- evaluations) and manipulations on them.

RValEnv-∅-canon : ∀ {Θ} (ρ : RValEnv Θ ∅) -> ρ ≡ emptyRValEnv
RValEnv-∅-canon {[]} [] = refl
RValEnv-∅-canon {x ∷ Θ} (skip ρ) = cong skip (RValEnv-∅-canon {Θ} ρ)

lkup-unlkup : ∀ {Θ A} {x : Θ ∋ A} {Ξ} -> (ok : varOk● Θ x Ξ) (ρ :  RValEnv Θ Ξ) -> unlkup ok (lkup ok ρ) ≡ ρ
lkup-unlkup (there ok) (skip ρ) = cong skip (lkup-unlkup ok ρ)
lkup-unlkup (here ad) (x ∷ ρ) with all-zero-canon ad ρ
... | refl = refl

unlkup-lkup : ∀ {Θ A} {x : Θ ∋ A} {Ξ} -> (ok : varOk● Θ x Ξ) (v : Value [] ∅ A) -> lkup ok (unlkup ok v) ≡ v
unlkup-lkup (there ok) v = unlkup-lkup ok v
unlkup-lkup (here ad) v = refl

split-merge :
  ∀ {Θ Ξ₁ Ξ₂}
  -> (ano : all-no-omega (Ξ₁ +ₘ Ξ₂))
  -> ∀ (ρ : RValEnv Θ (Ξ₁ +ₘ Ξ₂))
  -> mergeRValEnv ano (proj₁ (splitRValEnv ρ)) (proj₂ (splitRValEnv ρ)) ≡ ρ
split-merge {[]} {[]} {[]} ano [] = refl
split-merge {x ∷ Θ} {Multiplicity₀.zero ∷ Ξ₁} {Multiplicity₀.zero ∷ Ξ₂} (px ∷ ano) (skip ρ)
  rewrite split-merge {Θ} {Ξ₁} {Ξ₂} ano ρ = refl
split-merge {x ∷ Θ} {Multiplicity₀.zero ∷ Ξ₁} {one ∷ Ξ₂} (px ∷ ano) (v ∷ ρ)
  rewrite split-merge {Θ} {Ξ₁} {Ξ₂} ano ρ = refl
split-merge {x ∷ Θ} {one ∷ Ξ₁} {Multiplicity₀.zero ∷ Ξ₂} (px ∷ ano) (v ∷ ρ)
    rewrite split-merge {Θ} {Ξ₁} {Ξ₂} ano ρ = refl

merge-split :
  ∀ {Θ Ξ₁ Ξ₂}
  -> (ano : all-no-omega (Ξ₁ +ₘ Ξ₂))
  -> (ρ₁ : RValEnv Θ Ξ₁)
  -> (ρ₂ : RValEnv Θ Ξ₂)
  -> splitRValEnv (mergeRValEnv ano ρ₁ ρ₂) ≡ (ρ₁ , ρ₂)
merge-split {[]} {[]} {[]} ano [] [] = refl
merge-split {x ∷ Θ} {zero ∷ Ξ₁} {zero ∷ Ξ₂} (px ∷ ano) (skip ρ₁) (skip ρ₂) rewrite merge-split ano ρ₁ ρ₂ = refl
merge-split {x ∷ Θ} {zero ∷ Ξ₁} {one ∷ Ξ₂} (px ∷ ano) (skip ρ₁) (v ∷ ρ₂) rewrite merge-split ano ρ₁ ρ₂ = refl
merge-split {x ∷ Θ} {one ∷ Ξ₁} {zero ∷ Ξ₂} (_ ∷ ano) (v ∷ ρ₁) (skip ρ₂) rewrite merge-split ano ρ₁ ρ₂  = refl
merge-split {x ∷ Θ} {one ∷ Ξ₁} {one ∷ Ξ₂} (() ∷ ano) ρ₁ ρ₂

-- Round-trip properties (corresponding to Lemma 3.3 in the paper)

forward-backward :
  ∀ {Θ Ξ A}
  -> (ano : all-no-omega Ξ)
  -> (E : Residual Θ Ξ (A ●))
  -> let h = evalR ∞ ano E
     in ∀ ρ v -> Forward h ρ ⟶ v -> Backward h v ⟶ ρ

forward-backward ano unit● ρ v fwd with RValEnv-∅-canon ρ
... | refl = now⟶ emptyRValEnv
forward-backward ano (letunit● E E₁) ρ v fwd with all-no-omega-dist _ _ ano
forward-backward ano (letunit● E E₁) ρ v (bind⟶ (unit refl) .v fwd fwd₁) | ano₁ , ano₂ =
    let bwd  = forward-backward ano₁ E  _ _ fwd
        bwd₁ = forward-backward ano₂ E₁ _ _ fwd₁
    in bind⟶ _ _ bwd₁ (bind⟶ _ _ bwd (now⟶≡ (split-merge ano ρ)))

forward-backward ano (pair● E₁ E₂) ρ (pair {Ξ₁ = []} {[]} spΞ v₁ v₂) fwd with all-no-omega-dist _ _ ano
forward-backward ano (pair● E₁ E₂) ρ (pair {_} {[]} {[]} spΞ v₁ v₂) (bind⟶ _ _ fwd₁ (bind⟶ _ _ fwd₂ (now⟶ _))) | ano₁ , ano₂ =
    let bwd₁ = forward-backward ano₁ E₁ _ _ fwd₁
        bwd₂ = forward-backward ano₂ E₂ _ _ fwd₂
    in bind⟶ _ _ bwd₁ (bind⟶ _ _ bwd₂ (now⟶≡ (split-merge ano ρ)))
forward-backward ano (letpair● E E₁) ρ v fwd
  with all-no-omega-dist _ _ ano
forward-backward ano (letpair● E E₁) ρ v (bind⟶ (pair {Ξ₁ = []} {[]} refl v₁ v₂) .v fwd fwd₁) | ano₁ , ano₂ =
   let bwd  = forward-backward ano₁ E _ _ fwd
       bwd₁ = forward-backward (one ∷ one ∷ ano₂) E₁ _ _ fwd₁
   in bind⟶ _ _ bwd₁ (bind⟶ _ _ bwd (now⟶≡ (split-merge ano ρ)))

forward-backward ano (inl● E) ρ _ (bind⟶ u _ fwd (now⟶ _)) = forward-backward ano E _ _ fwd
forward-backward ano (inr● E) ρ _ (bind⟶ u _ fwd (now⟶ _)) = forward-backward ano E _ _ fwd

forward-backward ano (case● E refl θ₁ t₁ θ₂ t₂ v₁) ρ v fwd
  with all-no-omega-dist _ _ ano
forward-backward ano (case● E refl θ₁ t₁ θ₂ t₂ v₁) ρ v (bind⟶ (inl u) .v fwd (bind⟶ (red r₁) .v ev₁ (later⟶ .v (bind⟶ _ .v fwd₁ (bind⟶ (inl (unit refl)) .v ap (now⟶ _)))))) | ano₀ , ano- =
  bind⟶ _ _ ap (
  bind⟶ _ _ ev₁ (later⟶ _ (
  bind⟶ _ _ (forward-backward (one ∷ ano-) r₁ _ _ fwd₁) (bind⟶ _ _ (forward-backward ano₀ E _ _ fwd) (now⟶≡ (split-merge ano ρ))))))
forward-backward ano (case● E refl θ₁ t₁ θ₂ t₂ v₁) ρ v (bind⟶ (inl u) .v fwd (bind⟶ (red r₁) .v ev₁ (later⟶ .v (bind⟶ u₁ .v fwd₁ (bind⟶ (inr (unit refl)) .v ap nev))))) | ano₀ , ano- = ⊥-elim (¬Never⟶ nev)

forward-backward ano (case● E refl θ₁ t₁ θ₂ t₂ v₁) ρ v (bind⟶ (inr u) .v fwd (bind⟶ (red r₁) .v ev₁ (later⟶ .v (bind⟶ u₁ .v fwd₁ (bind⟶ (inl (unit refl)) .v ap nev))))) | ano₀ , ano- = ⊥-elim (¬Never⟶ nev)
forward-backward ano (case● E refl θ₁ t₁ θ₂ t₂ v₁) ρ v (bind⟶ (inr u) .v fwd (bind⟶ (red r₁) .v ev₁ (later⟶ .v (bind⟶ _ .v fwd₁ (bind⟶ (inr (unit refl)) .v ap (now⟶ _)))))) | ano₀ , ano- =
  bind⟶ _ _ ap (
  bind⟶ _ _ ev₁ (later⟶ _ (
  bind⟶ _ _ (forward-backward (one ∷ ano-) r₁ _ _ fwd₁) (bind⟶ _ _ (forward-backward ano₀ E _ _ fwd) (now⟶≡ (split-merge ano ρ))))))

forward-backward ano (var● x ok) ρ .(lkup ok ρ) (now⟶ _) rewrite lkup-unlkup ok ρ = now⟶ ρ
forward-backward ano (pin E (clo .omega refl θ t)) ρ (pair {Ξ₁ = []} {[]} refl v₁ v₂) fwd
  with all-no-omega-dist _ _ ano
forward-backward ano (pin E (clo .omega refl θ t)) ρ (pair {_} {[]} {[]} refl v₁ v₂)
                (bind⟶ _ _ fwd (later⟶ _ (bind⟶ (red r) _ ev (bind⟶ _ _ fwd₂ (now⟶ _))))) | ano₁ , ano₂ =
  later⟶ ρ (bind⟶ _ _ ev
              (bind⟶ _ ρ (forward-backward ano₂ r _ _ fwd₂)
              (bind⟶ _ _ (forward-backward ano₁ E _ _ fwd) (now⟶≡ (split-merge ano ρ)))))

backward-forward :
  ∀ {Θ Ξ A}
  -> (ano : all-no-omega Ξ)
  -> (E : Residual Θ Ξ (A ●))
  -> let h = evalR ∞ ano E
     in ∀ ρ v -> Backward h v ⟶ ρ -> Forward h ρ ⟶ v

backward-forward ano unit● ρ (unit refl) bwd = now⟶ (unit refl)
backward-forward ano (letunit● E E₁) ρ v (bind⟶ ρ₂ _ bwd₂ (bind⟶ ρ₁ _ bwd₁ (now⟶ _))) with all-no-omega-dist _ _ ano
... | ano₁ , ano₂ rewrite merge-split ano ρ₁ ρ₂  =
  bind⟶ _ _ (backward-forward ano₁ E _ _ bwd₁) (backward-forward ano₂ E₁ _ _ bwd₂)

backward-forward ano (pair● E₁ E₂) ρ (pair {Ξ₁ = []} {[]} refl v₁ v₂) (bind⟶ ρ₁ _ bwd₁ (bind⟶ ρ₂ _ bwd₂ (now⟶ _)))
  with all-no-omega-dist _ _ ano
... | ano₁ , ano₂ rewrite merge-split ano ρ₁ ρ₂ =
  bind⟶ _ _ (backward-forward ano₁ E₁ _ _ bwd₁) (bind⟶ _ _ (backward-forward ano₂ E₂ _ _ bwd₂) (now⟶ (pair refl v₁ v₂)))

backward-forward ano (letpair● E E₁) ρ v (bind⟶ (v₁ ∷ v₂ ∷ ρ₂) _ bwd₂ (bind⟶ ρ₁ _ bwd₁ (now⟶ _)))
  with all-no-omega-dist _ _ ano
... | ano₁ , ano₂ rewrite merge-split ano ρ₁ ρ₂ =
  bind⟶ _ _ (backward-forward ano₁ E _ _ bwd₁) (backward-forward (one ∷ one ∷ ano₂) E₁ _ _ bwd₂)

backward-forward ano (inl● E) ρ (inl v) bwd = bind⟶ _ _ (backward-forward ano E ρ v bwd) (now⟶ (inl v))
backward-forward ano (inl● E) ρ (inr v) bwd = ⊥-elim (¬Never⟶ bwd)

backward-forward ano (inr● E) ρ (inl v) bwd = ⊥-elim (¬Never⟶ bwd)
backward-forward ano (inr● E) ρ (inr v) bwd = bind⟶ _ _ (backward-forward ano E ρ v bwd) (now⟶ (inr v))

backward-forward
  ano (case● E refl θ₁ t₁ θ₂ t₂ ϕ) ρ v
  (bind⟶ u _ ap bwd)
  with all-no-omega-dist _ _ ano
backward-forward
  ano (case● E refl θ₁ t₁ θ₂ t₂ ϕ) ρ v
  (bind⟶ (inl u) .ρ ap (bind⟶ (red r) _ ev (later⟶ _ (bind⟶ (v₁ ∷ ρ-) _ bwd- (bind⟶ ρ₀ _ bwd₀ (now⟶ _)))))) | ano₀ , ano- rewrite merge-split ano ρ₀ ρ- =
  bind⟶ _ _ (backward-forward ano₀ E _ _ bwd₀)
  (bind⟶ _ _ ev (later⟶ _
  (bind⟶ _ _ (backward-forward (one ∷ ano-) r _ _ bwd-)
  (bind⟶ _ _ ap (now⟶ v)))))
backward-forward
  ano (case● E refl θ₁ t₁ θ₂ t₂ ϕ) ρ v
  (bind⟶ (inr u) .ρ ap (bind⟶ (red r) _ ev (later⟶ _ (bind⟶ (v₁ ∷ ρ-) _ bwd- (bind⟶ ρ₀ _ bwd₀ (now⟶ _)))))) | ano₀ , ano- rewrite merge-split ano ρ₀ ρ- =
  bind⟶ _ _ (backward-forward ano₀ E _ _ bwd₀)
  (bind⟶ _ _ ev (later⟶ _
  (bind⟶ _ _ (backward-forward (one ∷ ano-) r _ _ bwd-)
  (bind⟶ _ _ ap (now⟶ v)))))

backward-forward ano (var● x ok) .(unlkup ok v) v (now⟶ _) rewrite unlkup-lkup ok v = now⟶ v

backward-forward ano (pin E (clo .omega refl θ t)) ρ (pair {_} {[]} {[]} refl v₁ v₂)
  (later⟶ _ (bind⟶ (red r) _ ev (bind⟶ ρ₂ _ bwd₂ (bind⟶ ρ₁ _ bwd₁ (now⟶ _)))))
  with all-no-omega-dist _ _ ano
... | ano₁ , ano₂ rewrite merge-split ano ρ₁ ρ₂ =
  bind⟶ _ _ (backward-forward ano₁ E _ _ bwd₁)
  (later⟶ _ (bind⟶ _ _ ev (bind⟶ _ _ (backward-forward ano₂ r _ _ bwd₂) (now⟶ (pair refl v₁ v₂)))))

max_stars_repo_name: kztk-m/sparcl-agda

max_issues_repo_name: kztk-m/sparcl-agda

max_forks_repo_name: kztk-m/sparcl-agda


text:
module Issue628 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN SUC suc #-}
{-# BUILTIN ZERO zero #-}

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

data ⊥ : Set where

0≢1+n : ∀ {n} -> 0 ≡ suc n → ⊥
0≢1+n ()

divSucAux : (k m n j : ℕ) -> ℕ
divSucAux k m zero j = k
divSucAux k m (suc n) zero = divSucAux (suc k) m n m
divSucAux k m (suc n) (suc j) = divSucAux k m n j
{-# BUILTIN NATDIVSUCAUX divSucAux #-}

oh-noes : ⊥
oh-noes = 0≢1+n {divSucAux 0 0 0 1} refl

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import IO using ( _>>_ ; putStr ; run )

module System.IO.Examples.HelloRaw where

main = run (putStr "Hello, World\n")


text:
module Examples.DivergingContext where

open import Prelude

data TC : Set where
  tc-int : TC
  tc-bool : TC

_tc≟_ : (a b : TC) → Dec (a ≡ b)
tc-int tc≟ tc-int = yes refl
tc-int tc≟ tc-bool = no (λ ())
tc-bool tc≟ tc-int = no (λ ())
tc-bool tc≟ tc-bool = yes refl

open import Implicits.Oliveira.Types TC _tc≟_
open import Implicits.Oliveira.Terms TC _tc≟_
open import Implicits.Oliveira.Contexts TC _tc≟_
open import Implicits.Oliveira.WellTyped TC _tc≟_
open import Implicits.Oliveira.Substitutions TC _tc≟_
open import Implicits.Oliveira.Types.Unification TC _tc≟_
open import Implicits.Improved.Infinite.Resolution TC _tc≟_
open import Data.Maybe
open import Data.List
open import Coinduction
open import Data.List.Any.Membership using (map-mono)
open import Data.List.Any
open Membership-≡

Int : ∀ {ν} → Type ν
Int = simpl (tc tc-int)

module Ex₁ where

  r : Type zero
  r = (∀' (((simpl (x →' x)) ⇒ (simpl (x →' (simpl (x →' x))))) ⇒ x))
    where
      x = (simpl (tvar zero))

  Δ : ICtx zero
  Δ = r ∷ []

  -- Exploiting coinductive definition here to show that there is an infinite derivation
  -- of any type under the context Δ with the special characteristic that the context grows to
  -- infinity as well!
  --
  -- This may not be immediately obvious, but it can be seen by exploring the first argument of 'p'
  -- in the recursive calls, denoting the growing context.
  -- Also note that the element added to the context won't ever match the goal.
  -- This is not proven here, but an argument for it is made in the form of ¬r↓goal
  p : ∀ Δ' a → Δ ⊆ Δ' → Δ' ⊢ᵣ simpl a
  p Δ' a f = r-simp (f (here refl))
    (i-tabs
      (simpl a)
      (i-iabs (♯ r-iabs (p (new-r ∷ Δ') new-goal (λ x → there (f x)))) (i-simp a)))
    where
      new-r = simpl (simpl a →' simpl a)
      new-goal = (simpl a →' simpl (simpl a →' simpl a))

      ¬r↓goal : ¬ (new-r ∷ Δ') ⊢ new-r ↓ new-goal
      ¬r↓goal ()


text:
-- Andreas, 2016-06-08
-- Better error message when case splitting is invoked in location
-- where there is nothing to split

record R : Set where
  field f : {!!}

-- C-c C-c RET here gives:
-- Cannot split here, as we are not in a function definition


text:
module Numeral.Natural.Proofs where

import Lvl
open import Numeral.Natural
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function
open import Structure.Function.Domain

private variable n : ℕ

[𝐒]-not-0 : (𝐒(n) ≢ 𝟎)
[𝐒]-not-0 ()

𝐒-not-self : (𝐒(n) ≢ n)
𝐒-not-self ()

instance
  [𝐒]-injectivity : Injective(𝐒)
  Injective.proof([𝐒]-injectivity) = congruence₁(𝐏)

instance
  [𝐏][𝐒]-inverseᵣ : Inverseᵣ(𝐏)(𝐒)
  [𝐏][𝐒]-inverseᵣ = intro [≡]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Data.Graph

module Data.Graph.Path.Finite {ℓᵥ ℓₑ} (g : FiniteGraph ℓᵥ ℓₑ) where

open import Category.Monad
open import Data.Bool as Bool
open import Data.Graph.Path.Cut g hiding (_∈_)
open import Data.List as List hiding (_∷ʳ_)
open import Data.List.Any as Any
open import Data.List.Any.Properties
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties hiding (finite)
open import Data.List.Categorical as ListCat
open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Nat.Properties
open import Data.Product as Σ
open import Data.Unit using (⊤; tt)
open import Data.Sum as ⊎
open import Data.Vec as Vec using (Vec; []; _∷_)
import Level as ℓ
open import Finite
open import Function
open import Function.Equality using (Π)
open import Function.Equivalence using (Equivalence)
open import Function.Inverse using (Inverse)
open import Function.LeftInverse using (LeftInverse; leftInverse)
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive hiding (_>>=_)
open import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary.HeterogeneousEquality as ≅
open import Relation.Nullary hiding (module Dec)
open import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Negation

open Π using (_⟨$⟩_)
open Equivalence using (to; from)
open FiniteGraph g
open Inverse using (to; from)
open IsFinite
open RawMonad {ℓᵥ ℓ.⊔ ℓₑ} ListCat.monad

isubst : ∀ {ℓ₁ ℓ₂ ℓ₃} {I : Set ℓ₁}
  (A : I → Set ℓ₂) (B : ∀ {k} → A k → Set ℓ₃)
  {i j : I} {x : A i} {y : A j} →
  i ≡ j → x ≅ y →
  B x → B y
isubst A B refl refl = id

True-unique : ∀ {ℓ} {A : Set ℓ} (A? : Dec A) (x y : True A?) → x ≡ y
True-unique A? x y with A?
True-unique A? tt tt | yes a = refl
True-unique A? () y | no ¬a

True-unique-≅ : ∀
  {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂}
  (A? : Dec A) (B? : Dec B)
  (x : True A?) (y : True B?) →
  x ≅ y
True-unique-≅ A? B? x y with A? | B?
True-unique-≅ A? B? tt tt | yes a | yes b = refl
True-unique-≅ A? B? x () | _ | no ¬b
True-unique-≅ A? B? () y | no ¬a | _

∃-≅ : ∀
  {ℓ₁ ℓ₂} {A : Set ℓ₁} {P : A → Set ℓ₂}
  {x y : A} {p : P x} {q : P y} →
  x ≡ y → p ≅ q → (∃ P ∋ (x , p)) ≡ (y , q)
∃-≅ refl refl = refl

nexts : ∀ {a b n} → Path a b n → List (∃ λ b → Path a b (suc n))
nexts {a} {b} p = List.map (λ where (_ , e) → -, p ∷ʳ e) (elements (edgeFinite b))

∈-nexts : ∀ {a c n} →
  (pf : IsFinite (∃ λ b → Path a b n)) →
  (p : Path a c (suc n)) →
  (c , p) ∈ (elements pf >>= (nexts ∘ proj₂))
∈-nexts pf p =
  case unsnoc p of λ where
    (_ , p′ , e′ , refl) →
      to >>=-∈↔ ⟨$⟩
        (-,
          membership pf (-, p′) ,
          ∈-map⁺ (membership (edgeFinite _) (-, e′)))

Path-finite : ∀ n a → IsFinite (∃ λ b → Path a b n)
Path-finite zero a = finite List.[ -, [] ] λ where (_ , []) → here refl
Path-finite (suc n) a =
  let pf = Path-finite n a in
    finite (elements pf >>= (nexts ∘ proj₂)) (∈-nexts pf ∘ proj₂)

≤-top? : ∀ {x y} → x ≤ suc y → x ≤ y ⊎ x ≡ suc y
≤-top? z≤n = inj₁ z≤n
≤-top? {y = zero} (s≤s z≤n) = inj₂ refl
≤-top? {y = suc y} (s≤s p) =
  case ≤-top? p of λ where
    (inj₁ le) → inj₁ (s≤s le)
    (inj₂ refl) → inj₂ refl

Path≤-finite : ∀ n a → IsFinite (∃ λ b → Path≤ a b n)
Path≤-finite zero a = finite List.[ -, -, z≤n , [] ] λ where (_ , _ , z≤n , []) → here refl
Path≤-finite (suc n) a =
  let
    finite xs elem = Path≤-finite n a
    finite xs′ elem′ = Path-finite (suc n) a
  in
    finite
      (List.map (Σ.map₂ (Σ.map₂ (Σ.map₁ ≤-step))) xs List.++
        List.map (Σ.map₂ (_,_ (suc n) ∘ _,_ ≤-refl)) xs′)
      λ where
        (b , m , le , p) → case ≤-top? le of λ where
          (inj₁ le′) →
            to ++↔ ⟨$⟩
              inj₁
                (to map-∈↔ ⟨$⟩
                  (-, (elem (b , m , le′ , p)) ,
                    ≡.cong (λ q → b , m , q , p) (≤-irrelevance le (≤-step le′))))
          (inj₂ refl) →
            to (++↔ {xs = List.map _ xs}) ⟨$⟩
              inj₂
                (to map-∈↔ ⟨$⟩
                  (-, elem′ (-, p) ,
                    ≡.cong (λ q → b , m , q , p) (≤-irrelevance le (s≤s ≤-refl))))

AcyclicPath-finite : ∀ a → IsFinite (∃₂ λ b n → ∃ λ (p : Path a b n) → True (acyclic? p))
AcyclicPath-finite a =
  via-left-inverse (IsFinite.filter (Path≤-finite (size vertexFinite) a) _) $
    leftInverse
      (λ where (b , n , p , acp) → (b , n , acyclic-length-≤ p (toWitness acp) , p) , acp)
      (λ where ((b , n , le , p) , acp) → b , n , p , acp)
      λ where _ → refl

AcyclicStar : Vertex → Vertex → Set _
AcyclicStar a b = ∃ λ (p : Star Edge a b) → True (acyclic? (fromStar p))

AcyclicStar-finite : ∀ a → IsFinite (∃ (AcyclicStar a))
AcyclicStar-finite a =
  via-left-inverse (AcyclicPath-finite a) $
    leftInverse
      (λ where
        (b , p , acp) →
          b , starLength p , fromStar p , acp)
      (λ where
        (b , n , p , acp) →
          b , toStar p ,
            isubst (Path a b) (True ∘ acyclic?)
              (starLength-toStar p) (fromStar-toStar p)
              acp)
      (λ where
        (b , p , acp) →
          ≡.cong (b ,_) $
            ∃-≅
              (≡.sym (toStar-fromStar p))
              (True-unique-≅ _ _ _ _))


text:
-- Andreas, AIM XXXV, 2022-05-09, issue #5728
-- Give a proper error rather than crashing.

test : Set
test with Set
...

-- This used to be an internal error.
-- Expected error now:
-- The right-hand side can only be omitted if there is an absurd
-- pattern, () or {}, in the left-hand side.


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

open import HoTT
open import cohomology.Theory
open import groups.Cokernel
open import groups.Exactness
open import groups.HomSequence
open import groups.ExactSequence

open import cw.CW

module cw.cohomology.TipGrid {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 1) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.Descending OT
open import cw.cohomology.WedgeOfCells OT ⊙skel
open import cw.cohomology.TipAndAugment OT (⊙cw-init ⊙skel)
open import cw.cohomology.TipCoboundary OT ⊙skel
import cohomology.LongExactSequence

{-
   X₀ --> X₁
   |      |
   v      v
   1 -> X₁/X₀
-}

private
  module LES n = cohomology.LongExactSequence cohomology-theory n (⊙cw-incl-last ⊙skel)

Ker-cw-co∂-head' : C 0 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker cw-co∂-head'
Ker-cw-co∂-head' = Exact2.G-trivial-implies-H-iso-ker
  (exact-seq-index 2 $ LES.C-cofiber-exact-seq -1)
  (exact-seq-index 0 $ LES.C-cofiber-exact-seq 0)
  (CXₙ/Xₙ₋₁-<-is-trivial ltS ac)

{- NOT USED

Ker-cw-co∂-head : G ×ᴳ C 0 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker cw-co∂-head
Ker-cw-co∂-head = lemma ∘eᴳ ×ᴳ-emap (idiso G) Ker-cw-co∂-head' where
  lemma : G ×ᴳ Ker.grp cw-co∂-head' ≃ᴳ Ker.grp cw-co∂-head
  lemma = group-hom (λ{(g , (h , is-ker)) → ((g , h) , is-ker)})
    (λ _ _ → Subtype=-out (Ker.subEl-prop cw-co∂-head) idp) ,
    is-eq _ (λ{((g , h) , is-ker) → (g , (h , is-ker))}) (λ _ → idp) (λ _ → idp)
-}

private
  -- separate lemmas to speed up the type checking
  abstract
    lemma-exact₀ : is-exact (C-fmap 1 (⊙cfcod' (⊙cw-incl-last ⊙skel)))
      (C-fmap 1 (⊙cw-incl-last ⊙skel))
    lemma-exact₀ = exact-seq-index 2 $ LES.C-cofiber-exact-seq 0

    lemma-trivial : is-trivialᴳ (C 1 (⊙cw-head ⊙skel))
    lemma-trivial = CX₀-≠-is-trivial (pos-≠ (ℕ-S≠O 0))
      (⊙init-has-cells-with-choice ⊙skel ac)

Coker-cw-co∂-head : CokerCo∂Head.grp ≃ᴳ C 1 ⊙⟦ ⊙skel ⟧
Coker-cw-co∂-head = Exact2.L-trivial-implies-coker-iso-K
  co∂-head-incl-exact lemma-exact₀ CX₁/X₀-is-abelian lemma-trivial

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

module Cubical.Homotopy.Loopspace where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Truncation hiding (elim2) renaming (rec to trRec)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv.HalfAdjoint
open Iso

{- loop space of a pointed type -}
Ω : {ℓ : Level} → Pointed ℓ → Pointed ℓ
Ω (_ , a) = ((a ≡ a) , refl)

{- n-fold loop space of a pointed type -}
Ω^_ : ∀ {ℓ} → ℕ → Pointed ℓ → Pointed ℓ
(Ω^ 0) p = p
(Ω^ (suc n)) p = Ω ((Ω^ n) p)

{- homotopy Group -}
π : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → Type ℓ
π n A = ∥ typ ((Ω^ n) A) ∥ 2

{- loop space map -}
Ω→ : ∀ {ℓA ℓB} {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → (Ω A →∙ Ω B)
Ω→ (f , f∙) = (λ p → (sym f∙ ∙ cong f p) ∙ f∙) , cong (λ q → q ∙ f∙) (sym (rUnit (sym f∙))) ∙ lCancel f∙

{- Commutativity of loop spaces -}
isComm∙ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ
isComm∙ A = (p q : typ (Ω A)) → p ∙ q ≡ q ∙ p

Eckmann-Hilton : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → isComm∙ ((Ω^ (suc n)) A)
Eckmann-Hilton n α β =
  transport (λ i → cong (λ x → rUnit x (~ i)) α ∙ cong (λ x → lUnit x (~ i)) β
                 ≡ cong (λ x → lUnit x (~ i)) β ∙ cong (λ x → rUnit x (~ i)) α)
             λ i → (λ j → α (j ∧ ~ i) ∙ β (j ∧ i)) ∙ λ j → α (~ i ∨ j) ∙ β (i ∨ j)

isCommA→isCommTrunc : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → isComm∙ A
                    → isOfHLevel (suc n) (typ A)
                    → isComm∙ (∥ typ A ∥ (suc n) , ∣ pt A ∣)
isCommA→isCommTrunc {A = (A , a)} n comm hlev p q =
    ((λ i j → (leftInv (truncIdempotentIso (suc n) hlev) ((p ∙ q) j) (~ i)))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (cong (trRec hlev (λ x → x)) (p ∙ q)))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) p q i)))
 ∙ ((λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (comm (cong (trRec hlev (λ x → x)) p) (cong (trRec hlev (λ x → x)) q) i))
 ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) q p (~ i)))
 ∙∙ (λ i j → (leftInv (truncIdempotentIso (suc n) hlev) ((q ∙ p) j) i)))

ptdIso→comm : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Type ℓ'} (e : Iso (typ A) B) → isComm∙ A → isComm∙ (B , fun e (pt A))
ptdIso→comm {A = (A , a)} {B = B} e comm p q =
       sym (rightInv (congIso e) (p ∙ q))
    ∙∙ (cong (fun (congIso e)) ((invCongFunct e p q)
                            ∙∙ (comm (inv (congIso e) p) (inv (congIso e) q))
                            ∙∙ (sym (invCongFunct e q p))))
    ∙∙ rightInv (congIso e) (q ∙ p)

{- Homotopy group version -}
π-comp : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → ∥ typ ((Ω^ (suc n)) A) ∥₂
      → ∥ typ ((Ω^ (suc n)) A) ∥₂ → ∥ typ ((Ω^ (suc n)) A) ∥₂
π-comp n = elim2 (λ _ _ → isSetSetTrunc) λ p q → ∣ p ∙ q ∣₂

Eckmann-Hilton-π : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (p q : ∥ typ ((Ω^ (2 + n)) A) ∥₂)
               → π-comp (1 + n) p q ≡ π-comp (1 + n) q p
Eckmann-Hilton-π  n = elim2 (λ x y → isOfHLevelPath 2 isSetSetTrunc _ _)
                             λ p q → cong ∣_∣₂ (Eckmann-Hilton n p q)


text:
------------------------------------------------------------------------
-- Fω with interval kinds
------------------------------------------------------------------------

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

-- Author: Sandro Stucki
-- Copyright (c) 2017-2021 EPFL

-- The code in this repository contains an Agda mechanization of the
-- type system Fω extended with interval kinds ("F omega int").  An
-- interval kind `A..B' represents a type interval bounded by a pair
-- of types `A', `B'.  It is inhabited by all proper types `C : A..B'
-- that are both supertypes of `A' and subtypes of `B'.  Interval
-- kinds are flexible enough to express various features found in
-- other type systems, such as
--
--  * F-<:-style bounded polymorphism,
--  * bounded type operators,
--  * singleton kinds and first-class type definitions.
--
-- The mechanization includes a small-step operational call-by-value
-- semantics, declarative and canonical presentations of typing and
-- kinding, along with (syntactic) proofs of various meta-theoretic
-- properties, such as
--
--  * weak normalization of types (and kinds) via hereditary substitution,
--  * subject reduction for types (w.r.t. full β-reduction),
--  * type safety (progress & preservation) w.r.t. to the CBV semantics,
--  * undecidability of subtyping.
--
-- For more details on Fω with interval kinds, see my PhD thesis
-- "Higher-Order Subtyping with Type Intervals", which is available at
--
--   http://dx.doi.org/10.5075/epfl-thesis-8014
--
-- The code makes heavy use of the Agda standard library, which is
-- freely available at
--
--   https://github.com/agda/agda-stdlib/
--
-- The code has been tested using Agda 2.6.1.3 and version 1.6 of
-- the Agda standard library.

module README where

------------------------------------------------------------------------
-- Modules related to Fω with interval kinds.

-- Syntax of (untyped) terms along with support for substitutions,
-- (untyped) hereditary substitutions and normalization.
open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.SingleVariableSubstitution
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization

-- Weak equality of (untyped) terms up to kind annotations in
-- abstractions.
open import FOmegaInt.Syntax.WeakEquality

-- Variants of β-reduction/equivalence and properties thereof.
open import FOmegaInt.Reduction.Cbv
open import FOmegaInt.Reduction.Full

-- Typing, kinding, subtyping, etc. along with corresponding
-- substitution lemmas.
open import FOmegaInt.Typing

-- An alternate presentation of kinding and subtyping that is better
-- suited for proving functionality and validity lemmas, along with a
-- proof that the two presentations are equivalent.
open import FOmegaInt.Kinding.Declarative
open import FOmegaInt.Kinding.Declarative.Validity
open import FOmegaInt.Kinding.Declarative.Equivalence

-- Soundness of normalization w.r.t. to declarative kinding.
open import FOmegaInt.Kinding.Declarative.Normalization

-- Simple kinding of types, (hereditary) substitution lemmas.
open import FOmegaInt.Kinding.Simple

-- Lemmas about η-expansion of simply kinded and normalization and
-- simultaneous simplification of declaratively kinded types.
open import FOmegaInt.Kinding.Simple.EtaExpansion
open import FOmegaInt.Kinding.Simple.Normalization

-- Canonical kinding of types along with (hereditary) substitution,
-- validity and inversion lemmas for canonical kinding and subtyping.
open import FOmegaInt.Kinding.Canonical
open import FOmegaInt.Kinding.Canonical.HereditarySubstitution
open import FOmegaInt.Kinding.Canonical.Validity
open import FOmegaInt.Kinding.Canonical.Inversion

-- Lifting of weak (untyped) kind and type equality to canonical kind
-- and type equality.
open import FOmegaInt.Kinding.Canonical.WeakEquality

-- Equivalence of canonical and declarative kinding.
open import FOmegaInt.Kinding.Canonical.Equivalence

-- Generation of typing and inversion of declarative subtyping in the
-- empty context.
open import FOmegaInt.Typing.Inversion

-- Type safety (preservation/subject reduction and progress).
open import FOmegaInt.Typing.Preservation
open import FOmegaInt.Typing.Progress

-- Encodings and properties of higher-order extremal types, interval
-- kinds and bounded quantifiers.
open import FOmegaInt.Typing.Encodings

-- A reduced variant of the canonical system to be used in the
-- undecidability proof.
open import FOmegaInt.Kinding.Canonical.Reduced

-- Setup for the undecidability proof: syntax and lemmas for the SK
-- combinator calculus, and support for encoding/decoding SK terms and
-- equality proofs into types and subtyping derivations.
open import FOmegaInt.Undecidable.SK
open import FOmegaInt.Undecidable.Encoding
open import FOmegaInt.Undecidable.Decoding

-- Undecidability of subtyping
open import FOmegaInt.Undecidable

------------------------------------------------------------------------
-- Modules containing generic functionality

-- Extra lemmas that are derivable in the substitution framework of
-- the Agda standard library, as well as support for binary (term)
-- relations lifted to substitutions, typed substitutions, and typed
-- relations lifted to substitutions.
open import Data.Context
open import Data.Context.WellFormed
open import Data.Context.Properties
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Relation
open import Data.Fin.Substitution.Typed
open import Data.Fin.Substitution.TypedRelation

-- Support for generic reduction relations.
open import Relation.Binary.Reduction

-- Relational reasoning for transitive relations.
open import Relation.Binary.TransReasoning

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
-- Check if sharing is properly used for evaluation.
-- E.g. (\x -> putStrLn x; putStrLn x) (computeString)
-- should only evaluate computeString once.
-- Doing the evaluation twice should still yield the correct result,
-- but will incur a performance penalty.

-- MAlonzo: seems to use proper sharing for this example with ghc -O,
-- but not with ghc -O0. The sharing for -O0 is not introduced by MAlonzo,
-- but by the cleverness of GHC.

module Sharing where

open import Common.Prelude
open import Common.IO

{-# IMPORT Debug.Trace #-}

postulate
  primTrace : {b : Set} → String → b → b
{-# COMPILED primTrace (\_ -> Debug.Trace.trace) #-}
{-# COMPILED_UHC primTrace (\_ -> UHC.Agda.Builtins.primTrace) #-}

main : IO Unit
main = (λ x → putStrLn x ,, putStrLn x ) (primTrace "Eval" "hoi")


text:
open import Algebra
open import Data.Product
open import Data.Bool
open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Decidable

module LM {A : Set} = Monoid (Data.List.Properties.++-monoid A)

infixr 4 _⇒_

data Type : Set where
  o : Type
  _⇒_ : Type → Type → Type

Env = List Type

Type≡? : (A B : Type) → Dec (A ≡ B)
Type≡? o o = yes refl
Type≡? o (B ⇒ B₁) = no (λ ())
Type≡? (A ⇒ A₁) o = no (λ ())
Type≡? (A ⇒ B) (A' ⇒ B') with Type≡? A A'
Type≡? (A ⇒ B) (.A ⇒ B') | yes refl with Type≡? B B'
Type≡? (A ⇒ B) (.A ⇒ .B) | yes refl | yes refl = yes refl
Type≡? (A ⇒ B) (.A ⇒ B') | yes refl | no ¬p = no (λ {refl → ¬p refl})
Type≡? (A ⇒ B) (A' ⇒ B') | no ¬p = no (λ {refl → ¬p refl})

Env≡? : (Γ Δ : Env) → Dec (Γ ≡ Δ)
Env≡? [] [] = yes refl
Env≡? [] (x ∷ Δ) = no (λ ())
Env≡? (x ∷ Γ) [] = no (λ ())
Env≡? (A ∷ Γ) (A' ∷ Δ) with Type≡? A A'
Env≡? (A ∷ Γ) (A' ∷ Δ) | yes p with Env≡? Γ Δ
Env≡? (A ∷ Γ) (.A ∷ .Γ) | yes refl | yes refl = yes refl
Env≡? (A ∷ Γ) (A' ∷ Δ) | yes p | no ¬q = no (λ {refl → ¬q refl})
Env≡? (A ∷ Γ) (A' ∷ Δ) | no ¬p = no (λ {refl → ¬p refl})

data Var : Env → Type → Set where
  Z : ∀ {Γ : Env} {A : Type} → Var (A ∷ Γ) A
  S : ∀ {Γ : Env} {A B : Type} → Var Γ B → Var (A ∷ Γ) B

data Exp : Env → Type → Set where
  var : ∀ {Γ : Env} {A : Type} → Var Γ A → Exp Γ A
  abs : ∀ {Γ : Env} {A B : Type} → Exp (A ∷ Γ) B → Exp Γ (A ⇒ B)
  app : ∀ {Γ : Env} {A B : Type} → Exp Γ (A ⇒ B) → Exp Γ A → Exp Γ B

data PH (X : Type → Set) : Type → Set where
  var : ∀ {A : Type} → X A → PH X A
  abs : ∀ {A B : Type} → (X A → PH X B) → PH X (A ⇒ B)
  app : ∀ {A B : Type} → PH X (A ⇒ B) → PH X A → PH X B

-- logical prediacte on PH
PHᴾ : ∀ {X}(Xᴾ : ∀ {A} → X A → Set) → ∀ {A} → PH X A → Set
PHᴾ Xᴾ (var a)   = Xᴾ a
PHᴾ Xᴾ (abs t)   = ∀ a → Xᴾ a → PHᴾ Xᴾ (t a)
PHᴾ Xᴾ (app t u) = PHᴾ Xᴾ t × PHᴾ Xᴾ u

postulate
  free-thm :
    ∀ {A}(t : ∀ {X} → PH X A) → ∀ X (Xᴾ : ∀ {A} → X A → Set) → PHᴾ {X} Xᴾ t

PH' : Type → Set
PH' = PH (λ _ → Env)

VarOK? : ∀ Γ A Δ → Dec (∃ λ Ξ → (Ξ ++ A ∷ Δ) ≡ Γ)
VarOK? []       A Δ = no (λ {([] , ()) ; (_ ∷ _ , ())})
VarOK? (A' ∷ Γ) A Δ with Env≡? (A' ∷ Γ) (A ∷ Δ)
VarOK? (A' ∷ Γ) .A' .Γ | yes refl = yes ([] , refl)
VarOK? (A' ∷ Γ) A Δ | no ¬p with VarOK? Γ A Δ
VarOK? (A' ∷ Γ) A Δ | no ¬p | yes (Σ , refl) =
  yes (A' ∷ Σ , refl)
VarOK? (A' ∷ Γ) A Δ | no ¬p | no ¬q
  = no λ { ([] , refl) → ¬p refl ; (x ∷ Σ , s) → ¬q (Σ , proj₂ (∷-injective s))}

OK : ∀ {A} → Env → PH' A → Set
OK {A} Γ t = ∀ Δ → PHᴾ (λ {B} Σ → True (VarOK? (Δ ++ Γ) B Σ)) t

toVar : ∀ {Γ Σ A} → (∃ λ Ξ → (Ξ ++ A ∷ Σ) ≡ Γ) → Var Γ A
toVar ([]    , refl) = Z
toVar (x ∷ Ξ , refl) = S (toVar (Ξ , refl))

toExp' : ∀ {Γ A} (t : PH' A) → OK {A} Γ t → Exp Γ A
toExp' (var x) p = var (toVar (toWitness (p [])))
toExp' {Γ} (abs {A} {B} t) p =
  abs (toExp' (t Γ)
      λ Δ → subst (λ z → PHᴾ (λ {B₁} Σ₁ → True (VarOK? z B₁ Σ₁)) (t Γ))
                   (LM.assoc Δ (A ∷ []) Γ)
                   (p (Δ ++ A ∷ []) Γ (fromWitness (Δ , sym (LM.assoc Δ (A ∷ []) Γ)))))
toExp' (app t u) p =
  app (toExp' t (proj₁ ∘ p)) (toExp' u (proj₂ ∘ p))

toExp : ∀ {A} → (∀ {X} → PH X A) → Exp [] A
toExp {A} t = toExp' t λ Δ → free-thm t _ _

-- examples
------------------------------------------------------------

t0 : ∀ {X} → PH X ((o ⇒ o) ⇒ o ⇒ o)
t0 = abs var

t1 : ∀ {X} → PH X ((o ⇒ o) ⇒ o ⇒ o)
t1 = abs λ f → abs λ x → app (var f) (app (var f) (var x))

test1 : toExp t0 ≡ abs (var Z)
test1 = refl

test2 : toExp t1 ≡ abs (abs (app (var (S Z)) (app (var (S Z)) (var Z))))
test2 = refl


text:
{-# OPTIONS --safe #-}
module JVM.Syntax.Values where

open import Data.Bool
open import Data.Integer.Base
open import Relation.Unary
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax

open import JVM.Types

data Const : Ty → Set where
  null : ∀ {c} → Const (ref c)
  num  : ℤ     → Const int
  bool : Bool  → Const boolean


text:
{-# OPTIONS --type-in-type #-}

-- Yeah, that's type-in-type. I'm a sissy, I want to use the stdlib, I
-- don't want to reimplement ℕ, ⊤, etc. in Set1.

module ILabel where

open import Data.String

open import Data.Empty
open import Data.Unit

open import Data.Product

open import Data.Maybe
open import Data.Nat

open import Relation.Binary.PropositionalEquality

--****************************************************************
-- A universe of labels
--****************************************************************

infixr 5 _∷_

data AllowedBy : Set -> Set where
  ε    : forall {T} ->
         AllowedBy T
  _∷_  : {S : Set}{T : S -> Set} ->
         (s : S)(ts : AllowedBy (T s)) -> AllowedBy ((x : S) -> T x)

UId = String

-- The universe (that's a tiny one):

data Label : Set where
  label : (u : UId)(T : Set)(ts : AllowedBy T) -> Label

--****************************************************************
-- IDesc & co.
--****************************************************************

data IDesc (I : Set1) : Set1 where
  var    : I -> IDesc I
  const  : Set -> IDesc I
  prod   : IDesc I -> IDesc I -> IDesc I
  sigma  : (S : Set) -> (S -> IDesc I) -> IDesc I
  pi     : (S : Set) -> (S -> IDesc I) -> IDesc I

desc : {I : Set1} -> IDesc I -> (I -> Set) -> Set
desc (var i) P = P i
desc (const X) P = X
desc (prod D D') P = desc D P × desc D' P
desc (sigma S T) P = Σ S (\s -> desc (T s) P)
desc (pi S T) P = (s : S) -> desc (T s) P

-- We (may) stuck a label on the fix-point:

data IMu {I : Set1}(L : Maybe (I -> Label))(R : I -> IDesc I)(i : I) : Set where
  con : desc (R i) (\j -> IMu L R j) -> IMu L R i

--****************************************************************
-- Example: Nat
--****************************************************************

data NatConst : Set where
  Ze : NatConst
  Su : NatConst

natCases : NatConst -> IDesc ⊤
natCases Ze = const ⊤
natCases Suc = var _

NatD : ⊤ → IDesc ⊤
NatD _ = sigma NatConst natCases

Nat : Set
Nat = IMu (just (\ _ -> label "Nat" Set ε)) NatD _

--****************************************************************
-- Example: Vector
--****************************************************************

data VecConst : ℕ -> Set where
  Vnil : VecConst 0
  Vcons : {n : ℕ} -> VecConst (1 + n)

vecDChoice : Set -> (n : ℕ) -> VecConst n -> IDesc ℕ
vecDChoice X 0 Vnil = const ⊤
vecDChoice X (suc n) Vcons = prod (const X) (var n)

vecD : Set -> ℕ -> IDesc ℕ
vecD X n = sigma (VecConst n) (vecDChoice X n)

vec : Set -> ℕ -> Set
vec X n = IMu (just (\n -> label "Vec" (ℕ -> Set) (n ∷ ε))) (vecD X) n

--****************
-- Example: Fin
--****************

data FinConst : ℕ -> Set where
  Fz : {n : ℕ} -> FinConst (1 + n)
  Fs : {n : ℕ} -> FinConst (1 + n)

finDChoice : (n : ℕ) -> FinConst n -> IDesc ℕ
finDChoice 0 ()
finDChoice (suc n) Fz = const ⊤
finDChoice (suc n) Fs = var n

finD : ℕ -> IDesc ℕ
finD n = sigma (FinConst n) (finDChoice n)

fin : ℕ -> Set
fin n = IMu (just (\ n -> label "Fin" (ℕ -> Set) (n ∷ ε))) finD n

--****************
-- Example: Identity type
--****************

-- data Id (A : Set) (a : A) : A -> Set := (refl : Id A a a)

data IdConst : Set where
  Refl : IdConst

idD : (A : Set)(a : A)(b : A) -> IDesc A
idD A a b = sigma IdConst (\ _ -> const (a ≡ b))

id : (A : Set)(a : A)(b : A) -> Set
id A a b = IMu (just (\ b -> label "Id" ((A : Set)(a : A)(b : A) -> Set) (A ∷ a ∷ b ∷ ε))) (idD A a) b

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
------------------------------------------------------------------------
-- Propositional equality
------------------------------------------------------------------------

module Relation.Binary.PropositionalEquality1 where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

------------------------------------------------------------------------
-- Propositional equality

infix 4 _≡₁_ _≢₁_

data _≡₁_ {a : Set₁} (x : a) : a → Set where
  refl : x ≡₁ x

-- Nonequality.

_≢₁_ : {a : Set₁} → a → a → Set
x ≢₁ y = ¬ x ≡₁ y

------------------------------------------------------------------------
-- Some properties

reflexive : ∀ {a} (x : a) → x ≡₁ x
reflexive _ = refl

sym : ∀ {a} {x y : a} → x ≡₁ y → y ≡₁ x
sym refl = refl

trans : ∀ {a} {x y z : a} → x ≡₁ y → y ≡₁ z → x ≡₁ z
trans refl refl = refl

subst : {a b : Set} → a ≡₁ b → a → b
subst refl x = x

cong : ∀ {a b} (f : a → b) → ∀ {x y} → x ≡₁ y → f x ≡₁ f y
cong _ refl = refl

cong₂ : ∀ {a b c} (f : a → b → c) →
        ∀ {x₁ x₂ y₁ y₂} → x₁ ≡₁ x₂ → y₁ ≡₁ y₂ → f x₁ y₁ ≡₁ f x₂ y₂
cong₂ _ refl refl = refl

cong₀₁ : ∀ {a b} (f : a → b) → ∀ {x y} → x ≡ y → f x ≡₁ f y
cong₀₁ _ refl = refl

cong₁₀ : ∀ {a b} (f : a → b) → ∀ {x y} → x ≡₁ y → f x ≡ f y
cong₁₀ _ refl = refl

max_issues_repo_name: larrytheliquid/Lemmachine