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

open import HoTT
open import homotopy.PtdAdjoint
open import groups.FromSusp
open import groups.ToOmega

module groups.SuspAdjointLoop {i} where

  import homotopy.SuspAdjointLoop {i} as A

  module _ (X Y : Ptd i) where

    private
      pres-comp : preserves-comp
        (GroupStructure.comp (⊙→Ω-group-structure (⊙Susp X) Y))
        (GroupStructure.comp (⊙→Ω-group-structure X (⊙Ω Y)))
        (–> (A.eq X (⊙Ω Y)))
    abstract
      pres-comp h₁ h₂ =
        B.nat-cod h₁ h₂ ⊙Ω-∙
        ∙ ap (_⊙∘ ⊙fanout (–> (A.eq X (⊙Ω Y)) h₁) (–> (A.eq X (⊙Ω Y)) h₂))
             arr2-lemma
        where
        module A× = RightAdjoint× A.hadj
        module B = RightAdjointBinary A.hadj

        ap2-lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
          (f : A × B → C) {r s : A × B} (p : r == s)
          → ap f p == ap2 (curry f) (ap fst p) (ap snd p)
        ap2-lemma f idp = idp

        ⊙ap2-lemma : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
          (f : X ⊙× Y ⊙→ Z)
          → ⊙Ω-fmap f == ⊙Ω-fmap2 f ⊙∘ ⊙fanout (⊙Ω-fmap ⊙fst) (⊙Ω-fmap ⊙snd)
        ⊙ap2-lemma (f , idp) = ⊙λ=' (ap2-lemma f) idp

        arr2-lemma : B.arr2 ⊙Ω-∙ == ⊙Ω-∙
        arr2-lemma =
          ⊙Ω-fmap ⊙Ω-∙ ⊙∘ A×.⊙out _ _
            =⟨ ⊙ap2-lemma ⊙Ω-∙ |in-ctx _⊙∘ A×.⊙out _ _ ⟩
          (⊙Ω-fmap2 ⊙Ω-∙ ⊙∘ A×.⊙into _ _) ⊙∘ A×.⊙out _ _
            =⟨ ⊙λ= $ ⊙∘-assoc (⊙Ω-fmap2 ⊙Ω-∙) (A×.⊙into _ _) (A×.⊙out _ _) ⟩
          ⊙Ω-fmap2 ⊙Ω-∙ ⊙∘ (A×.⊙into _ _ ⊙∘ A×.⊙out _ _)
            =⟨ A×.⊙into-out _ _ |in-ctx ⊙Ω-fmap2 ⊙Ω-∙ ⊙∘_ ⟩
          ⊙Ω-fmap2 ⊙Ω-∙
            =⟨ ⊙Ω-fmap2-∙ ⟩
          ⊙Ω-∙ ∎

    ⊙→Ω-iso-⊙→Ω : ⊙→Ω-group-structure (⊙Susp X) Y ≃ᴳˢ ⊙→Ω-group-structure X (⊙Ω Y)
    ⊙→Ω-iso-⊙→Ω = ≃-to-≃ᴳˢ (A.eq X (⊙Ω Y)) pres-comp

    Trunc-⊙→Ω-iso-Trunc-⊙→Ω : Trunc-⊙→Ω-group (⊙Susp X) Y ≃ᴳ Trunc-⊙→Ω-group X (⊙Ω Y)
    Trunc-⊙→Ω-iso-Trunc-⊙→Ω = Trunc-group-emap ⊙→Ω-iso-⊙→Ω

  abstract
    Trunc-⊙→Ω-iso-Trunc-⊙→Ω-nat-dom : {X Y : Ptd i} (f : X ⊙→ Y) (Z : Ptd i)
      → fst (Trunc-⊙→Ω-iso-Trunc-⊙→Ω X Z) ∘ᴳ Trunc-⊙→Ω-group-fmap-dom (⊙Susp-fmap f) Z
        == Trunc-⊙→Ω-group-fmap-dom f (⊙Ω Z) ∘ᴳ fst (Trunc-⊙→Ω-iso-Trunc-⊙→Ω Y Z)
    Trunc-⊙→Ω-iso-Trunc-⊙→Ω-nat-dom f Z = group-hom= $ λ= $ Trunc-elim
      (λ g → ap [_] (! (A.nat-dom f (⊙Ω Z) g)))

  module _ (X Y : Ptd i) where

    private
      pres-comp'' : ∀ h₀ h₁ →
          fst (<– (A.eq X Y) (GroupStructure.comp (⊙→Ω-group-structure X Y) (–> (A.eq X Y) h₀) (–> (A.eq X Y) h₁)))
        ∼ fst (GroupStructure.comp (Susp⊙→-group-structure X Y) h₀ h₁)
    abstract
      pres-comp'' (h₀ , idp) (h₁ , h₁-pt) =
        Susp-elim
          idp
          (! h₁-pt ∙ ap h₁ (merid (pt X)))
          (λ x → ↓-='-in' $
            ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt)) ∘ pinch X) (merid x)
              =⟨ ap-∘ (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (pinch X) (merid x)  ⟩
            ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (ap (pinch X) (merid x))
              =⟨ ap (ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt)))) (Pinch.merid-β X x) ⟩
            ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
              =⟨ ap-∙∙ (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
            ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (ap winl (σloop X x))
            ∙ ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) wglue
            ∙ ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) (ap winr (merid x))
              =⟨ ap3 (λ p q r → p ∙ q ∙ r)
                   (∘-ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) winl (σloop X x))
                   (⊙WedgeRec.glue-β (h₀ , idp) (h₁ , h₁-pt))
                   (∘-ap (fst (⊙Wedge-rec (h₀ , idp) (h₁ , h₁-pt))) winr (merid x)) ⟩
            ap h₀ (σloop X x) ∙ ! h₁-pt ∙ ap h₁ (merid x)
              =⟨ lemma h₁ (ap h₀ (σloop X x)) h₁-pt (merid x) (merid (pt X)) h₁-pt ⟩
            (ap h₀ (σloop X x) ∙ (! h₁-pt ∙ ap h₁ (σloop X x) ∙' h₁-pt)) ∙' (! h₁-pt ∙ ap h₁ (merid (pt X)))
              =⟨ ap (λ p → p ∙' (! h₁-pt ∙ ap h₁ (merid (pt X)))) $
                  ap h₀ (σloop X x) ∙ (! h₁-pt ∙ ap h₁ (σloop X x) ∙' h₁-pt)
                    =⟨ ! $ ap (ap h₀ (σloop X x) ∙_) (Ω-fmap-β (h₁ , h₁-pt) (σloop X x)) ⟩
                  ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x)
                    =⟨ ! $ A.Eta.merid-β Y (ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x)) ⟩
                  ap (fst (A.ε Y)) (merid (ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x)))
                    =⟨ ! $ ap (ap (fst (A.ε Y))) (SuspFmap.merid-β (λ x → ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x)) x) ⟩
                  ap (fst (A.ε Y)) (ap (Susp-fmap (λ x → ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x))) (merid x))
                    =⟨ ∘-ap (fst (A.ε Y)) (Susp-fmap (λ x → ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x))) (merid x) ⟩
                  ap (fst (A.ε Y) ∘ Susp-fmap (λ x → ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x))) (merid x)
                    =∎ ⟩
            ap (fst (A.ε Y) ∘ Susp-fmap (λ x → ap h₀ (σloop X x) ∙ Ω-fmap (h₁ , h₁-pt) (σloop X x))) (merid x)
            ∙' (! h₁-pt ∙ ap h₁ (merid (pt X)))
              =∎)
        where
        lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
          {a₀ a₁ a₂ : A} {b₀ b₁ b₂ : B} (p₀ : b₀ == b₁) (p₁ : f a₀ == b₁)
          (p₂ : a₀ == a₁) (p₃ : a₂ == a₁) (p₄ : f a₂ == b₂)
          → p₀ ∙ ! p₁ ∙ ap f p₂ == (p₀ ∙ (! p₁ ∙ ap f (p₂ ∙ ! p₃) ∙' p₄)) ∙' (! p₄ ∙ ap f p₃)
        lemma f idp idp idp idp idp = idp

      private
        pres-comp' : ∀ h₀ h₁ →
             <– (A.eq X Y) (GroupStructure.comp (⊙→Ω-group-structure X Y) (–> (A.eq X Y) h₀) (–> (A.eq X Y) h₁))
          ⊙∼ GroupStructure.comp (Susp⊙→-group-structure X Y) h₀ h₁
      abstract
        pres-comp' (h₀ , idp) (h₁ , h₁-pt) =
          pres-comp'' (h₀ , idp) (h₁ , h₁-pt) , idp

      private
        pres-comp : preserves-comp
          (GroupStructure.comp (Susp⊙→-group-structure X Y))
          (GroupStructure.comp (⊙→Ω-group-structure X Y))
          (–> (A.eq X Y))
      abstract
        pres-comp h₀ h₁ =
          –> (A.eq X Y) (GroupStructure.comp (Susp⊙→-group-structure X Y) h₀ h₁)
            =⟨ ! (ap (–> (A.eq X Y)) (⊙λ= (pres-comp' h₀ h₁))) ⟩
          –> (A.eq X Y) (<– (A.eq X Y) (GroupStructure.comp (⊙→Ω-group-structure X Y) (–> (A.eq X Y) h₀) (–> (A.eq X Y) h₁)))
            =⟨ <–-inv-r (A.eq X Y) (GroupStructure.comp (⊙→Ω-group-structure X Y) (–> (A.eq X Y) h₀) (–> (A.eq X Y) h₁)) ⟩
          GroupStructure.comp (⊙→Ω-group-structure X Y) (–> (A.eq X Y) h₀) (–> (A.eq X Y) h₁)
            =∎

    Susp⊙→-iso-⊙→Ω : Susp⊙→-group-structure X Y ≃ᴳˢ ⊙→Ω-group-structure X Y
    Susp⊙→-iso-⊙→Ω = ≃-to-≃ᴳˢ (A.eq X Y) pres-comp

    Trunc-Susp⊙→-iso-Trunc-⊙→Ω : Trunc-Susp⊙→-group X Y ≃ᴳ Trunc-⊙→Ω-group X Y
    Trunc-Susp⊙→-iso-Trunc-⊙→Ω = Trunc-group-emap Susp⊙→-iso-⊙→Ω

  module _ (X Y : Ptd i) where

    private
      pres-comp : preserves-comp
        (GroupStructure.comp (Susp⊙→-group-structure X Y))
        (GroupStructure.comp (Susp⊙→-group-structure (⊙Susp X) (⊙Susp Y)))
        (⊙Susp-fmap :> ((⊙Susp X ⊙→ Y) → _))
    abstract
      pres-comp = ∼-preserves-preserves-comp
        (GroupStructure.comp (Susp⊙→-group-structure X Y))
        (GroupStructure.comp (Susp⊙→-group-structure (⊙Susp X) (⊙Susp Y)))
        (λ f →
          <– (A.eq (⊙Susp X) (⊙Susp Y)) (<– (A.eq X (⊙Ω (⊙Susp Y))) (⊙Ω-fmap (A.η Y) ⊙∘ –> (A.eq X Y) f))
            =⟨ ap (<– (A.eq (⊙Susp X) (⊙Susp Y)) ∘ <– (A.eq X (⊙Ω (⊙Susp Y)))) $ A.nat-cod X (A.η Y) f ⟩
          <– (A.eq (⊙Susp X) (⊙Susp Y)) (<– (A.eq X (⊙Ω (⊙Susp Y))) (–> (A.eq X (⊙Ω (⊙Susp Y))) (A.η Y ⊙∘ f)))
            =⟨ ap (<– (A.eq (⊙Susp X) (⊙Susp Y))) $ <–-inv-l (A.eq X (⊙Ω (⊙Susp Y))) (A.η Y ⊙∘ f)  ⟩
          <– (A.eq (⊙Susp X) (⊙Susp Y)) (A.η Y ⊙∘ f)
            =⟨ ap (<– (A.eq (⊙Susp X) (⊙Susp Y))) $ A.η-natural f ⟩
          <– (A.eq (⊙Susp X) (⊙Susp Y)) (–> (A.eq (⊙Susp X) (⊙Susp Y)) (⊙Susp-fmap f))
            =⟨ <–-inv-l (A.eq (⊙Susp X) (⊙Susp Y)) (⊙Susp-fmap f) ⟩
          ⊙Susp-fmap f
            =∎)
        (GroupStructureHom.pres-comp $
              GroupStructureIso.g-shom (Susp⊙→-iso-⊙→Ω (⊙Susp X) (⊙Susp Y))
          ∘ᴳˢ GroupStructureIso.g-shom (⊙→Ω-iso-⊙→Ω X (⊙Susp Y))
          ∘ᴳˢ ⊙→Ω-group-structure-fmap-codom X (A.η Y)
          ∘ᴳˢ GroupStructureIso.f-shom (Susp⊙→-iso-⊙→Ω X Y))

    Susp⊙→-Susp-fmap-shom : Susp⊙→-group-structure X Y →ᴳˢ Susp⊙→-group-structure (⊙Susp X) (⊙Susp Y)
    Susp⊙→-Susp-fmap-shom = group-structure-hom ⊙Susp-fmap pres-comp

    Trunc-Susp⊙→-Susp-fmap-hom : Trunc-Susp⊙→-group X Y →ᴳ Trunc-Susp⊙→-group (⊙Susp X) (⊙Susp Y)
    Trunc-Susp⊙→-Susp-fmap-hom = Trunc-group-fmap Susp⊙→-Susp-fmap-shom

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Relation.Binary.Core

module BHeap.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import BHeap.Heap _≤_
open import BHeap.Height _≤_ tot≤

ext: agda

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --cubical-compatible --show-implicit #-}

module WithoutK3 where

-- Homogeneous equality.

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

-- The J rule.

J : {A : Set} (P : {x y : A} → x ≡ y → Set) →
    (∀ x → P (refl {x = x})) →
    ∀ {x y} (x≡y : x ≡ y) → P x≡y
J P p refl = p _

-- Heterogeneous equality.

data _≅_ {A : Set} (x : A) : {B : Set} → B → Set₁ where
  refl : x ≅ x

-- Substitutivity.

subst : {A : Set} {x y : A} (P : A → Set) → x ≅ y → P x → P y
subst P refl p = p

-- The K rule. (The implementation is based on a construction in Conor
-- McBride's PhD thesis.)

K : {A : Set} {x : A} (P : {x : A} → x ≡ x → Set) →
    (∀ x → P (refl {x = x})) →
    ∀ {x} (p : x ≡ x) → P p
K P p x≡x =
  J (λ {x y} (p : x ≡ y) → (x≡x : x ≡ x) → p ≅ x≡x → P x≡x)
    (λ x x≡x refl≅x≡x → subst P refl≅x≡x (p x))
    x≡x x≡x refl


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

module Data.ByteString where

import Data.ByteString.Primitive as Prim
import Data.ByteString.Utf8 as Utf8

open import Data.Word8 using (Word8)
open import Data.Nat using (ℕ)
open import Data.Colist using (Colist)
open import Data.List using (List)
open import Data.String using (String)
open import Data.Bool using (Bool; true; false)
open import Data.Product using (_×_)
open import Data.Tuple using (Pair→×)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

data ByteStringKind : Set where
  Lazy Strict : ByteStringKind

ByteString : ByteStringKind → Set
ByteString Lazy = Prim.ByteStringLazy
ByteString Strict = Prim.ByteStringStrict

empty : ∀ {k} → ByteString k
empty {Lazy} = Prim.emptyLazy
empty {Strict} = Prim.emptyStrict

null : ∀ {k} → ByteString k → Bool
null {Lazy} = Prim.nullLazy
null {Strict} = Prim.nullStrict

length : ∀ {k} → ByteString k → ℕ
length {Lazy} bs = Prim.int64Toℕ (Prim.lengthLazy bs)
length {Strict} bs = Prim.IntToℕ (Prim.lengthStrict bs)

unsafeHead : ∀ {k} → ByteString k → Word8
unsafeHead {Lazy} = Prim.headLazy
unsafeHead {Strict} = Prim.headStrict

unsafeTail : ∀ {k} → ByteString k → ByteString k
unsafeTail {Lazy} = Prim.tailLazy
unsafeTail {Strict} = Prim.tailStrict

unsafeIndex : ∀ {k} → ByteString k → ℕ → Word8
unsafeIndex {Lazy} bs ix = Prim.indexLazy bs (Prim.ℕToInt64 ix)
unsafeIndex {Strict} bs ix = Prim.indexStrict bs (Prim.ℕToInt ix)

unsafeSplitAt : ∀ {k} → ℕ → ByteString k → (ByteString k) × (ByteString k)
unsafeSplitAt {Lazy} ix bs = Pair→× (Prim.splitAtLazy (Prim.ℕToInt64 ix) bs)
unsafeSplitAt {Strict} ix bs = Pair→× (Prim.splitAtStrict (Prim.ℕToInt ix) bs)

ByteStringRep : ByteStringKind → Set
ByteStringRep Lazy = Colist Word8
ByteStringRep Strict = List Word8

unpack : ∀ {k} → ByteString k → ByteStringRep k
unpack {Lazy} = Prim.Colist←Lazy
unpack {Strict} = Prim.List←Strict

pack : ∀ {k} → ByteStringRep k → ByteString k
pack {Lazy} = Prim.Colist→Lazy
pack {Strict} = Prim.List→Strict

infix 4 _≟_

_≟_ : ∀ {k} → Decidable {A = ByteString k} _≡_
_≟_ {Lazy} s₁ s₂ with Prim.lazy≟lazy s₁ s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _
_≟_ {Strict} s₁ s₂ with Prim.strict≟strict s₁ s₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- behind _==_ is the same idea as in Data.String
infix 4 _==_

_==_ : ∀ {k} → ByteString k → ByteString k → Bool
_==_ {k} s₁ s₂ = ⌊ s₁ ≟ s₂ ⌋

_++_ : ByteString Lazy → ByteString Lazy → ByteString Lazy
_++_ = Prim.appendLazy

fromChunks : List (ByteString Strict) → ByteString Lazy
fromChunks = Prim.fromChunks

toChunks : ByteString Lazy → List (ByteString Strict)
toChunks = Prim.toChunks

toLazy : ByteString Strict → ByteString Lazy
toLazy = Prim.toLazy

toStrict : ByteString Lazy → ByteString Strict
toStrict = Prim.toStrict

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module Base.Free where

-- Reexport definitions from Agda's standard library that are needed by the
-- generated code.
open import Function            using (case_of_)      public
open import Data.Bool           using (if_then_else_) public
open import Size                using (Size; ↑_)      public

-- The `Free` monad over a container with shapes `S` and postions `P`.
data Free (S : Set) (P : S → Set) (A : Set) : Set where
  pure : A → Free S P A

  impure : (s : S) → (pf : P s → Free S P A) → Free S P A

infixl 1 _>>=_
_>>=_ : {S : Set} {P : S → Set} {A : Set} {B : Set} → Free S P A → (A → Free S P B) → Free S P B
pure   x    >>= k = k x
impure s pf >>= k = impure s λ p → pf p >>= k

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Presheaves.Facts where

open import Cats.Category.Presheaves.Facts.Exponential public using
  ( hasExponentials )

open import Cats.Category
open import Cats.Category.Presheaves

import Cats.Category.Fun.Facts as Fun
import Cats.Category.Setoids.Facts

module _ {lo la l≈} {C : Category lo la l≈} {l l′} where

  -- We don't just re-export the following definitions from Fun because
  -- we want to fill in their instance arguments.

  instance
    hasBinaryProducts : HasBinaryProducts (Presheaves C l l′)
    hasBinaryProducts = Fun.hasBinaryProducts

    hasTerminal : HasTerminal (Presheaves C l l′)
    hasTerminal = Fun.hasTerminal

    hasFiniteProducts : HasFiniteProducts (Presheaves C l l′)
    hasFiniteProducts = Fun.hasFiniteProducts

isCCC : ∀ {l} {C : Category l l l} → IsCCC (Presheaves C l l)
isCCC = record { hasFiniteProducts = Fun.hasFiniteProducts }
-- record {} complains about ambiguity. Don't know if this is my fault or a bug.

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
open import Relation.Binary.Core

module PLRTree.Drop.Heap {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)
                     (trans≤ : Transitive _≤_) where

open import PLRTree {A}
open import PLRTree.Compound {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.DropLast.Heap _≤_ tot≤
open import PLRTree.Heap _≤_
open import PLRTree.Order.Properties {A}
open import PLRTree.Push.Heap _≤_ tot≤ trans≤

lemma-drop-heap : {t : PLRTree} → Heap t → Heap (drop t)
lemma-drop-heap leaf = leaf
lemma-drop-heap (node {t} {x} (lf≤* .x) (lf≤* .x) leaf leaf) = leaf
lemma-drop-heap (node {t} {x} {r = node t' x' l' r'} (lf≤* .x) (nd≤* x≤x' x≤*l' x≤*r') leaf (node x'≤*l' x'≤*r' hl' hr'))
    with dropLast (node t x leaf (node t' x' l' r')) | lemma-dropLast-heap (node {t} (lf≤* x) (nd≤* {t'} x≤x' x≤*l' x≤*r') leaf (node x'≤*l' x'≤*r' hl' hr'))
... | leaf | leaf = leaf
... | node t'' x'' l'' r'' | node x''≤*l'' x''≤*r'' hl'' hr'' =
           let z = last (node t x leaf (node t' x' l' r')) compound
           in lemma-push-heap t'' z hl'' hr'' (≺-wf (node t'' z l'' r''))
lemma-drop-heap (node {t} {x} {l = node t' x' l' r'} {r} (nd≤* x≤x' x≤*l' x≤*r') x≤*r (node x'≤*l' x'≤*r' hl' hr') hr)
    with dropLast (node t x (node t' x' l' r') r) | lemma-dropLast-heap (node {t} (nd≤* {t'} x≤x' x≤*l' x≤*r') x≤*r (node x'≤*l' x'≤*r' hl' hr') hr)
... | leaf | leaf = leaf
... | node t'' x'' l'' r'' | node x''≤*l'' x''≤*r'' hl'' hr'' =
           let z = last (node t x (node t' x' l' r') r) compound
           in lemma-push-heap t'' z hl'' hr'' (≺-wf (node t'' z l'' r''))


text:
module explore where
import Explore.BigDistr
import Explore.BinTree
import Explore.Core
import Explore.Dice
import Explore.Examples
import Explore.Explorable
import Explore.Fin
import Explore.Group
import Explore.GuessingGameFlipping
import Explore.Isomorphism
import Explore.Monad
import Explore.One
import Explore.Product
import Explore.Properties
import Explore.README
import Explore.Subset
import Explore.Sum
import Explore.Summable
import Explore.Two
import Explore.Universe
import Explore.Universe.Base
import Explore.Universe.FromE
import Explore.Universe.Type
import Explore.Zero
-- BROKEN import Explore.Explorable.Fun
-- BROKEN import Explore.Function.Fin

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Bool where

data Bool : Set where
  false : Bool
  true  : Bool

data IsTrue : Bool -> Set where
  isTrue : IsTrue true

open import Vec
open import All

allEnvs : {n : Nat} -> List (Vec Bool n)
allEnvs {zero } = ε :: []
allEnvs {suc n} = map (_►_ false) allEnvs ++ map (_►_ true) allEnvs

∈++left : {A : Set}{x : A}{xs ys : List A} -> x ∈ xs -> x ∈ (xs ++ ys)
∈++left (hd p) = hd p
∈++left (tl q) = tl (∈++left q)

∈++right : {A : Set}{x : A}{xs ys : List A} -> x ∈ ys -> x ∈ (xs ++ ys)
∈++right {xs = []}      p = p
∈++right {xs = x :: xs} p = tl (∈++right {xs = xs} p)

∈map : {A B : Set}{f : A -> B}{x : A}{xs : List A} -> x ∈ xs -> f x ∈ map f xs
∈map (hd refl) = hd refl
∈map (tl q)    = tl (∈map q)

covered : {n : Nat} -> (xs : Vec Bool n) -> xs ∈ allEnvs
covered ε            = hd refl
covered (false ► xs) = ∈++left (∈map (covered xs))
covered (true  ► xs) = ∈++right {xs = map (_►_ false) allEnvs}
                                (∈map (covered xs))

Sat : {A : Set} -> (A -> Bool) -> A -> Set
Sat f x = IsTrue (f x)

lem₁ : {n : Nat}(f : Vec Bool n -> Bool) ->
      All (Sat f) allEnvs -> (xs : Vec Bool n) -> Sat f xs
lem₁ f p xs with p ! covered xs
... | (.xs , p , refl) = p

data False : Set where

¬_ : Set -> Set
¬ P = P -> False

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

¬IsTrue-false : ¬ IsTrue false
¬IsTrue-false ()

decide : {A : Set}(p : A -> Bool)(x : A) ->
         Sat p x ∨ ¬ Sat p x
decide p x with p x
... | true  = inl isTrue
... | false = inr ¬IsTrue-false

all : {A : Set}(p : A -> Bool)(xs : List A) ->
      All (Sat p) xs ∨ Some (\x -> ¬ Sat p x) xs
all p [] = inl ∅
all p (x :: xs) with decide p x
... | inr ¬px = inr (hd ¬px)
... | inl px  with all p xs
...   | inl ps = inl (px ▹ ps)
...   | inr q  = inr (tl q)

data NoProof : Set where
  no-proof : NoProof

Proof : {n : Nat} -> (Vec Bool n -> Bool) -> Set
Proof {n} f with all f allEnvs
... | inl _ = (xs : Vec Bool n) -> Sat f xs
... | inr _ = NoProof

prove : {n : Nat}(f : Vec Bool n -> Bool) -> Proof f
prove f with all f allEnvs
... | inl ps = lem₁ f ps
... | inr _  = no-proof

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Nat
open import Prelude
open import dynamics-core
open import contexts
open import lemmas-consistency
open import lemmas-disjointness
open import lemmas-matching
open import weakening

module typed-elaboration where
  mutual
    typed-elaboration-synth : {Γ : tctx} {e : hexp} {τ : htyp} {d : ihexp} {Δ : hctx} →
                            Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                            Δ , Γ ⊢ d :: τ
    typed-elaboration-synth ESNum = TANum
    typed-elaboration-synth (ESPlus dis apt x₁ x₂)
      with typed-elaboration-ana x₁ | typed-elaboration-ana x₂
    ... | con1 , ih1 | con2 , ih2 = TAPlus (TACast (weaken-ta-Δ1 apt ih1) con1) (TACast (weaken-ta-Δ2 apt ih2) con2)
    typed-elaboration-synth (ESVar x₁) = TAVar x₁
    typed-elaboration-synth (ESLam x₁ ex) = TALam x₁ (typed-elaboration-synth ex)
    typed-elaboration-synth (ESAp {Δ1 = Δ1} _ d x₁ x₂ x₃ x₄)
      with typed-elaboration-ana x₃ | typed-elaboration-ana x₄
    ... | con1 , ih1 | con2 , ih2  = TAAp (TACast (weaken-ta-Δ1 d ih1) con1) (TACast (weaken-ta-Δ2 {Δ1 = Δ1} d ih2) con2)
    typed-elaboration-synth (ESEHole {Γ = Γ} {u = u}) with natEQ u u
    ... | Inr u≠u = abort (u≠u refl)
    ... | Inl refl = TAEHole (x∈■ u (Γ , ⦇-⦈)) (STAId (λ x τ z → z))
    typed-elaboration-synth (ESNEHole {Γ = Γ} {τ = τ} {u = u} {Δ = Δ} (d1 , d2) ex)
                            with typed-elaboration-synth ex
    ... | ih1 = TANEHole {Δ = Δ ,, (u , Γ , ⦇-⦈)} (ctx-top Δ u (Γ , ⦇-⦈) (d2 u (lem-domsingle _ _))) (weaken-ta-Δ2 (d2 , d1) ih1) (STAId (λ x τ₁ z → z))
    typed-elaboration-synth (ESAsc x)
      with typed-elaboration-ana x
    ... | con , ih = TACast ih con
    typed-elaboration-synth (ESPair x x₁ x₂ x₃)
      with typed-elaboration-synth x₂ | typed-elaboration-synth x₃
    ... | ih1 | ih2 = TAPair (weaken-ta-Δ1 x₁ ih1) (weaken-ta-Δ2 x₁ ih2)
    typed-elaboration-synth (ESFst x x₁ x₂)
      with typed-elaboration-ana x₂
    ... | con , ih = TAFst (TACast ih con)
    typed-elaboration-synth (ESSnd x x₁ x₂)
      with typed-elaboration-ana x₂
    ... | con , ih = TASnd (TACast ih con)

    typed-elaboration-ana : {Γ : tctx} {e : hexp} {τ τ' : htyp} {d : ihexp} {Δ : hctx} →
                            Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                            (τ' ~ τ) × (Δ , Γ ⊢ d :: τ')
    typed-elaboration-ana (EALam x₁ MAHole ex)
      with typed-elaboration-ana ex
    ... | con , D = TCHole1 , TALam x₁ D
    typed-elaboration-ana (EALam x₁ MAArr ex)
      with typed-elaboration-ana ex
    ... | con , D = TCArr TCRefl con , TALam x₁ D
    typed-elaboration-ana (EASubsume x x₁ x₂ x₃) = ~sym x₃ , typed-elaboration-synth x₂
    typed-elaboration-ana (EAEHole {Γ = Γ} {u = u}) = TCRefl , TAEHole (x∈■ u (Γ , _)) (STAId (λ x τ z → z))
    typed-elaboration-ana (EANEHole {Γ = Γ} {u = u} {τ = τ} {Δ = Δ} (d1 , d2) x)
      with typed-elaboration-synth x
    ... | ih1 = TCRefl , TANEHole {Δ = Δ ,, (u , Γ , τ)} (ctx-top Δ u (Γ , τ) (d2 u (lem-domsingle _ _)) ) (weaken-ta-Δ2 (d2 , d1) ih1) (STAId (λ x₁ τ₁ z → z))
    typed-elaboration-ana (EAInl MSHole x₁)
      with typed-elaboration-ana x₁
    ... | con , D = TCHole1 , TAInl D
    typed-elaboration-ana (EAInl MSSum x₁)
      with typed-elaboration-ana x₁
    ... | con , D = TCSum con TCRefl , TAInl D
    typed-elaboration-ana (EAInr MSHole x₁)
      with typed-elaboration-ana x₁
    ... | con , D = TCHole1 , TAInr D
    typed-elaboration-ana (EAInr MSSum x₁)
      with typed-elaboration-ana x₁
    ... | con , D = TCSum TCRefl con , TAInr D
    typed-elaboration-ana (EACase x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁)
      with typed-elaboration-synth x₈ |
           typed-elaboration-ana x₁₀ | typed-elaboration-ana x₁₁
    ... | D | con1 , D1 | con2 , D2 =
      let Δ##Δ1∪Δ2 = ##-comm (disjoint-parts (##-comm x₃) (##-comm x₄))
      in let wtd   = TACast (weaken-ta-Δ1 Δ##Δ1∪Δ2 D) (▸sum-consist x₉)
      in let wtd1  = TACast (weaken-ta-Δ2 Δ##Δ1∪Δ2 (weaken-ta-Δ1 x₅ D1)) con1
      in let wtd2  = TACast (weaken-ta-Δ2 Δ##Δ1∪Δ2 (weaken-ta-Δ2 x₅ D2)) con2
      in let wt    = TACase wtd x₆ wtd1 x₇ wtd2
      in TCRefl , wt

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

-- Adjoint Functor Theorem
module Categories.Adjoint.AFT where

open import Level
open import Data.Product
open import Data.Product using (Σ)

open import Categories.Category
open import Categories.Category.Complete
open import Categories.Category.Complete.Properties
open import Categories.Category.Construction.Cones
open import Categories.Category.Construction.Comma
open import Categories.Functor
open import Categories.Functor.Limits
open import Categories.Functor.Properties
open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Cone.Properties
open import Categories.Morphism as Mor
open import Categories.Morphism.Universal

import Categories.Adjoint.AFT.SolutionSet as SS
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

module _ {R : Functor C D} where
  private
    module C = Category C
    module D = Category D
    module R = Functor R

    o-level : Level
    o-level = C.o-level ⊔ C.ℓ-level ⊔ D.ℓ-level ⊔ D.e-level

    ℓ-level : Level
    ℓ-level = C.o-level ⊔ C.ℓ-level ⊔ D.ℓ-level ⊔ D.e-level

    e-level : Level
    e-level = C.o-level ⊔ C.ℓ-level ⊔ D.ℓ-level ⊔ D.e-level

  open SS R using (SolutionSet′)

  module _ {L : Functor D C} (L⊣R : L ⊣ R) where
    private
      module L = Functor L
      open Adjoint L⊣R

    L⊣R⇒solutionSet′ : SolutionSet′
    L⊣R⇒solutionSet′ = record
      { S₀      = λ {_ X} _ → L.₀ X
      ; S₁      = Radjunct
      ; ϕ       = λ _ → unit.η _
      ; commute = λ _ → LRadjunct≈id
      }

  module _ (Com  : Complete o-level ℓ-level e-level C)
           (Rcon : Continuous o-level ℓ-level e-level R)
           (s    : SolutionSet′) where
    open SolutionSet′ s
    open D.Equiv
    open D.HomReasoning
    open MR D

    private
      module _ X where
        X↙R : Category (C.o-level ⊔ D.ℓ-level) (C.ℓ-level ⊔ D.e-level) C.e-level
        X↙R = X ↙ R
        module X↙R = Category X↙R

        s′ : SolutionSet X↙R
        s′ = record
          { D   = D′
          ; arr = arr′
          }
          where D′ : X↙R.Obj → X↙R.Obj
                D′ Z = record
                  { f = ϕ Z.f
                  }
                  where module Z = CommaObj Z

                arr′ : ∀ Z → X↙R [ D′ Z , Z ]
                arr′ Z = record
                  { h       = S₁ Z.f
                  ; commute = commute _ ○ ⟺ D.identityʳ
                  }
                  where module Z = CommaObj Z
                        open D.HomReasoning

        module _ {J : Category o-level ℓ-level e-level} (F : Functor J X↙R) where
          module J = Category J
          module F = Functor F

          F′ : Functor J C
          F′ = Cod _ _ ∘F F

          LimF′ : Limit F′
          LimF′ = Com F′
          module LimF′ = Limit LimF′

          RLimF′ : Cone (R ∘F F′)
          RLimF′ = F-map-Coneˡ R LimF′.limit
          module RLimF′ = Cone _ RLimF′

          LimRF′ : Limit (R ∘F F′)
          LimRF′ = record
            { terminal = record
              { ⊤             = RLimF′
              ; ⊤-is-terminal = Rcon LimF′
              }
            }
          module LimRF′ = Limit LimRF′

          coneF : Cone (R ∘F F′)
          coneF = record
            { N    = X
            ; apex = record
              { ψ       = λ j → CommaObj.f (F.₀ j)
              ; commute = λ f → Comma⇒.commute (F.₁ f) ○ D.identityʳ
              }
            }

          ⊤-arr : Cone⇒ (R ∘F F′) coneF RLimF′
          ⊤-arr = LimRF′.rep-cone coneF
          module ⊤-arr = Cone⇒ (R ∘F F′) ⊤-arr

          ⊤ : Cone F
          ⊤ = record
            { N    = record
              { f = ⊤-arr.arr
              }
            ; apex = record
              { ψ       = λ j → record
                { h       = LimF′.proj j
                ; commute = begin
                  R.₁ (LimF′.proj j) D.∘ ⊤-arr.arr ≈⟨ ⊤-arr.commute ⟩
                  CommaObj.f (F.₀ j)               ≈˘⟨ D.identityʳ ⟩
                  CommaObj.f (F.₀ j) D.∘ D.id      ∎
                }
              ; commute = λ f → -, LimF′.limit-commute f
              }
            }

          K-conv : Cone F → Cone F′
          K-conv = F-map-Coneˡ (Cod _ _)

          K-conv′ : Cone F → Cone (R ∘F F′)
          K-conv′ K = F-map-Coneˡ R (K-conv K)

          ! : (K : Cone F) → Cones F [ K , ⊤ ]
          ! K = record
            { arr     = record
              { h       = LimF′.rep (K-conv K)
              ; commute = ⟺ (LimRF′.terminal.!-unique (record
                { arr     = R.₁ (LimF′.rep (K-conv K)) D.∘ CommaObj.f N
                ; commute = λ {j} → begin
                  LimRF′.proj j D.∘ R.₁ (LimF′.rep (K-conv K)) D.∘ CommaObj.f N
                    ≈⟨ pullˡ ([ R ]-resp-∘ LimF′.commute) ⟩
                  R.₁ (Comma⇒.h (ψ j)) D.∘ CommaObj.f N
                    ≈⟨ Comma⇒.commute (ψ j) ⟩
                  CommaObj.f (F.F₀ j) D.∘ D.id
                    ≈⟨ D.identityʳ ⟩
                  CommaObj.f (F.₀ j)
                    ∎
                })) ○ ⟺ D.identityʳ
              }
            ; commute = -, LimF′.commute
            }
            where open Cone _ K

          !-unique : {K : Cone F} (f : Cones F [ K , ⊤ ]) → Cones F [ ! K ≈ f ]
          !-unique f = -, LimF′.terminal.!-unique record
            { arr     = Comma⇒.h f.arr
            ; commute = proj₂ f.commute
            }
            where module f = Cone⇒ _ f

          complete : Limit F
          complete = record
            { terminal = record
              { ⊤             = ⊤
              ; ⊤-is-terminal = record
                { !        = ! _
                ; !-unique = !-unique
                }
              }
            }

        solutionSet′⇒universalMorphism : UniversalMorphism X R
        solutionSet′⇒universalMorphism = record
          { initial = SolutionSet⇒Initial {o′ = 0ℓ} {0ℓ} {0ℓ} {C = X ↙ R} complete s′
          }

    solutionSet⇒adjoint : Σ (Functor D C) (λ L → L ⊣ R)
    solutionSet⇒adjoint = universalMophisms⇒adjoint solutionSet′⇒universalMorphism

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

module Equiv where

open import Agda.Builtin.Cubical.Glue public
  using ( isEquiv
        ; equiv-proof
        ; _≃_)

open import Cubical.Foundations.Everything public using (ua)
open import Cubical.Foundations.Equiv public
  using (equivToIso; isPropIsEquiv)
  renaming (compEquiv to trans-≃; invEquiv to sym-≃)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

data ⊥ : Set where

data Zero : Set where
  zero : Zero

data One : Set where
  suc : Zero → One

one : One
one = suc zero

data _≤_ : One → Zero → Set where

leq : ∀ m n → Nat → Nat → m ≤ n → ⊥
leq (suc m) zero = λ i j ()

test : Nat → one ≤ zero → ⊥
test = leq one zero 5

-- Normalise: test
-- Expected:  λ j ()


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

module Cubical.Categories.Functor where

open import Cubical.Categories.Functor.Base public
open import Cubical.Categories.Functor.Properties public
open import Cubical.Categories.Functor.Compose public

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Oscar.Data.Maybe.properties where

open import Data.Maybe public using (maybe)


text:
module STLC2.Kovacs.Convertibility where

open import STLC2.Kovacs.Substitution public

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

-- Convertibility (_~_ ; ~refl ; _~⁻¹ ; lam ; app ; β ; η)
infix 3 _∼_
data _∼_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set
  where
    refl∼    : ∀ {Γ A} → {M : Γ ⊢ A}
                       → M ∼ M

    _⁻¹∼     : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
                       → (p : M₁ ∼ M₂)
                       → M₂ ∼ M₁

    _⦙∼_     : ∀ {Γ A} → {M₁ M₂ M₃ : Γ ⊢ A}
                       → (p : M₁ ∼ M₂) (q : M₂ ∼ M₃)
                       → M₁ ∼ M₃

    ƛ∼       : ∀ {Γ A B} → {M₁ M₂ : Γ , A ⊢ B}
                         → (p : M₁ ∼ M₂)
                         → ƛ M₁ ∼ ƛ M₂

    _∙∼_     : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⇒ B} {N₁ N₂ : Γ ⊢ A}
                         → (p : M₁ ∼ M₂) (q : N₁ ∼ N₂)
                         → M₁ ∙ N₁ ∼ M₂ ∙ N₂

    _,∼_     : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A} {N₁ N₂ : Γ ⊢ B}
                         → (p : M₁ ∼ M₂) (q : N₁ ∼ N₂)
                         → M₁ , N₁ ∼ M₂ , N₂

    π₁∼      : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⩕ B}
                         → (p : M₁ ∼ M₂)
                         → π₁ M₁ ∼ π₁ M₂

    π₂∼      : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⩕ B}
                         → (p : M₁ ∼ M₂)
                         → π₂ M₁ ∼ π₂ M₂

    φ∼       : ∀ {Γ C} → {M₁ M₂ : Γ ⊢ ⫫}
                       → (p : M₁ ∼ M₂)
                       → φ {C = C} M₁ ∼ φ M₂

    ι₁∼      : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A}
                         → (p : M₁ ∼ M₂)
                         → ι₁ {B = B} M₁ ∼ ι₁ M₂

    ι₂∼      : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ B}
                         → (p : M₁ ∼ M₂)
                         → ι₂ {A = A} M₁ ∼ ι₂ M₂

    _⁇∼_∥∼_  : ∀ {Γ A B C} → {M₁ M₂ : Γ ⊢ A ⩖ B}
                              {N₁₁ N₁₂ : Γ , A ⊢ C} {N₂₁ N₂₂ : Γ , B ⊢ C}
                           → (p : M₁ ∼ M₂) (q₁ : N₁₁ ∼ N₁₂) (q₂ : N₂₁ ∼ N₂₂)
                           → M₁ ⁇ N₁₁ ∥ N₂₁ ∼ M₂ ⁇ N₁₂ ∥ N₂₂

    red⇒    : ∀ {Γ A B} → (M : Γ , A ⊢ B) (N : Γ ⊢ A)
                         → (ƛ M) ∙ N ∼ cut N M

    red⩕₁    : ∀ {Γ A B} → (M : Γ ⊢ A) (N : Γ ⊢ B)
                         → π₁ (M , N) ∼ M

    red⩕₂    : ∀ {Γ A B} → (M : Γ ⊢ A) (N : Γ ⊢ B)
                         → π₂ (M , N) ∼ N

    red⩖₁    : ∀ {Γ A B C} → (M : Γ ⊢ A) (N₁ : Γ , A ⊢ C) (N₂ : Γ , B ⊢ C)
                           → ι₁ M ⁇ N₁ ∥ N₂ ∼ cut M N₁

    red⩖₂    : ∀ {Γ A B C} → (M : Γ ⊢ B) (N₁ : Γ , A ⊢ C) (N₂ : Γ , B ⊢ C)
                           → ι₂ M ⁇ N₁ ∥ N₂ ∼ cut M N₂

    exp⇒    : ∀ {Γ A B} → (M : Γ ⊢ A ⇒ B)
                         → M ∼ ƛ (wk M ∙ 0)

    exp⩕     : ∀ {Γ A B} → (M : Γ ⊢ A ⩕ B)
                         → M ∼ π₁ M , π₂ M

    exp⫪    : ∀ {Γ} → (M : Γ ⊢ ⫪)
                     → M ∼ τ

    exp⩖     : ∀ {Γ A B} → (M : Γ ⊢ A ⩖ B)
                         → M ∼ M ⁇ ι₁ 0 ∥ ι₂ 0

    comm⫫∙  : ∀ {Γ A B} → (M : Γ ⊢ ⫫) (N : Γ ⊢ A)
                         → _∙_ {A = A} {B} (φ M) N ∼ φ M

    comm⫫π₁ : ∀ {Γ A B} → (M : Γ ⊢ ⫫)
                         → π₁ {A = A} {B} (φ M) ∼ φ M

    comm⫫π₂ : ∀ {Γ A B} → (M : Γ ⊢ ⫫)
                         → π₂ {A = A} {B} (φ M) ∼ φ M

    comm⫫φ  : ∀ {Γ C} → (M : Γ ⊢ ⫫)
                       → φ {C = C} (φ M) ∼ φ M

    comm⫫⁇∥ : ∀ {Γ A B C} → (M : Γ ⊢ ⫫) (N₁ : Γ , A ⊢ C) (N₂ : Γ , B ⊢ C)
                           → φ M ⁇ N₁ ∥ N₂ ∼ φ M

    comm⩖∙   : ∀ {Γ A B C D} → (M : Γ ⊢ A ⩖ B)
                                (N₁ : Γ , A ⊢ C ⇒ D)
                                (N₂ : Γ , B ⊢ C ⇒ D)
                                (O : Γ ⊢ C)
                             → (M ⁇ N₁ ∥ N₂) ∙ O ∼
                                M ⁇ (N₁ ∙ wk O) ∥ (N₂ ∙ wk O)

    comm⩖π₁  : ∀ {Γ A B C D} → (M : Γ ⊢ A ⩖ B)
                                (N₁ : Γ , A ⊢ C ⩕ D)
                                (N₂ : Γ , B ⊢ C ⩕ D)
                             → π₁ (M ⁇ N₁ ∥ N₂) ∼
                                M ⁇ (π₁ N₁) ∥ (π₁ N₂)

    comm⩖π₂  : ∀ {Γ A B C D} → (M : Γ ⊢ A ⩖ B)
                                (N₁ : Γ , A ⊢ C ⩕ D)
                                (N₂ : Γ , B ⊢ C ⩕ D)
                             → π₂ (M ⁇ N₁ ∥ N₂) ∼
                                M ⁇ (π₂ N₁) ∥ (π₂ N₂)

    comm⩖φ   : ∀ {Γ A B C} → (M : Γ ⊢ A ⩖ B)
                              (N₁ : Γ , A ⊢ ⫫)
                              (N₂ : Γ , B ⊢ ⫫)
                           → φ {C = C} (M ⁇ N₁ ∥ N₂) ∼
                              M ⁇ (φ N₁) ∥ (φ N₂)

    comm⩖⁇∥  : ∀ {Γ A B C D E} → (M : Γ ⊢ A ⩖ B)
                                  (N₁ : Γ , A ⊢ C ⩖ D)
                                  (N₂ : Γ , B ⊢ C ⩖ D)
                                  (O₁ : Γ , C ⊢ E)
                                  (O₂ : Γ , D ⊢ E)
                               → (M ⁇ N₁ ∥ N₂) ⁇ O₁ ∥ O₂ ∼
                                  M ⁇ (N₁ ⁇ liftwk O₁ ∥ liftwk O₂)
                                    ∥ (N₂ ⁇ liftwk O₁ ∥ liftwk O₂)

≡→∼ : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
               → M₁ ≡ M₂
               → M₁ ∼ M₂
≡→∼ refl = refl∼

instance
  per∼ : ∀ {Γ A} → PER (Γ ⊢ A) _∼_
  per∼ =
    record
      { _⁻¹ = _⁻¹∼
      ; _⦙_ = _⦙∼_
      }

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

renwk : ∀ {Γ Γ′ A B} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ A)
                     → (wk {B} ∘ ren η) M ≡
                        (ren (liftₑ η) ∘ wk) M
renwk η M = ren○ (wkₑ idₑ) η M ⁻¹
          ⦙ (λ η′ → ren (wkₑ η′) M) & ( rid○ η
                                       ⦙ lid○ η ⁻¹
                                       )
          ⦙ ren○ (liftₑ η) (wkₑ idₑ) M

renliftwk : ∀ {Γ Γ′ A B C} → (η : Γ′ ⊇ Γ) (M : Γ , A ⊢ B)
                           → (liftwk {C} ∘ ren (liftₑ η)) M ≡
                              (ren (liftₑ (liftₑ η)) ∘ liftwk) M
renliftwk η M = ren○ (liftₑ (wkₑ idₑ)) (liftₑ η) M ⁻¹
              ⦙ (λ η′ → ren (liftₑ (wkₑ η′)) M) & ( rid○ η
                                                   ⦙ lid○ η ⁻¹
                                                   )
              ⦙ ren○ (liftₑ (liftₑ η)) (liftₑ (wkₑ idₑ)) M

rencut : ∀ {Γ Γ′ A B} → (η : Γ′ ⊇ Γ) (M : Γ ⊢ A) (N : Γ , A ⊢ B)
                      → (cut (ren η M) ∘ ren (liftₑ η)) N ≡
                         (ren η ∘ cut M) N
rencut η M N = sub◑ (idₛ , ren η M) (liftₑ η) N ⁻¹
             ⦙ (λ σ → sub (σ , ren η M) N) & ( rid◑ η
                                              ⦙ lid◐ η ⁻¹
                                              )
             ⦙ sub◐ η (idₛ , M) N

-- (~ₑ)
ren∼ : ∀ {Γ Γ′ A} → {M₁ M₂ : Γ ⊢ A}
                  → (η : Γ′ ⊇ Γ) → M₁ ∼ M₂
                  → ren η M₁ ∼ ren η M₂

ren∼ η refl∼                   = refl∼
ren∼ η (p ⁻¹∼)                 = ren∼ η p ⁻¹
ren∼ η (p ⦙∼ q)                = ren∼ η p ⦙ ren∼ η q
ren∼ η (ƛ∼ p)                  = ƛ∼ (ren∼ (liftₑ η) p)
ren∼ η (p ∙∼ q)                = ren∼ η p ∙∼ ren∼ η q
ren∼ η (p ,∼ q)                = ren∼ η p ,∼ ren∼ η q
ren∼ η (π₁∼ p)                 = π₁∼ (ren∼ η p)
ren∼ η (π₂∼ p)                 = π₂∼ (ren∼ η p)
ren∼ η (φ∼ p)                  = φ∼ (ren∼ η p)
ren∼ η (ι₁∼ p)                 = ι₁∼ (ren∼ η p)
ren∼ η (ι₂∼ p)                 = ι₂∼ (ren∼ η p)
ren∼ η (p ⁇∼ q₁ ∥∼ q₂)         = ren∼ η p ⁇∼ ren∼ (liftₑ η) q₁
                                          ∥∼ ren∼ (liftₑ η) q₂

ren∼ η (red⇒ M N)
  = coe (((ƛ (ren (liftₑ η) M) ∙ ren η N) ∼_)
         & rencut η N M)
        (red⇒ (ren (liftₑ η) M) (ren η N))

ren∼ η (red⩕₁ M N)             = red⩕₁ (ren η M) (ren η N)
ren∼ η (red⩕₂ M N)             = red⩕₂ (ren η M) (ren η N)

ren∼ η (red⩖₁ M N₁ N₂)
  = coe (((ι₁ (ren η M) ⁇ ren (liftₑ η) N₁
                        ∥ ren (liftₑ η) N₂) ∼_)
         & rencut η M N₁)
        (red⩖₁ (ren η M)
               (ren (liftₑ η) N₁)
               (ren (liftₑ η) N₂))

ren∼ η (red⩖₂ M N₁ N₂)
  = coe (((ι₂ (ren η M) ⁇ ren (liftₑ η) N₁
                        ∥ ren (liftₑ η) N₂) ∼_)
         & rencut η M N₂)
        (red⩖₂ (ren η M)
               (ren (liftₑ η) N₁)
               (ren (liftₑ η) N₂))

ren∼ η (exp⇒ M)
  = coe ((λ M′ → ren η M ∼ ƛ (M′ ∙ 0))
         & renwk η M)
        (exp⇒ (ren η M))

ren∼ η (exp⩕ M)                = exp⩕ (ren η M)
ren∼ η (exp⫪ M)               = exp⫪ (ren η M)
ren∼ η (exp⩖ M)                = exp⩖ (ren η M)
ren∼ η (comm⫫∙ M N)           = comm⫫∙ (ren η M) (ren η N)
ren∼ η (comm⫫π₁ M)            = comm⫫π₁ (ren η M)
ren∼ η (comm⫫π₂ M)            = comm⫫π₂ (ren η M)
ren∼ η (comm⫫φ M)             = comm⫫φ (ren η M)
ren∼ η (comm⫫⁇∥ M N₁ N₂)      = comm⫫⁇∥ (ren η M)
                                          (ren (liftₑ η) N₁)
                                          (ren (liftₑ η) N₂)

ren∼ η (comm⩖∙ M N₁ N₂ O)
  = coe ((((ren η M ⁇ ren (liftₑ η) N₁
                    ∥ ren (liftₑ η) N₂) ∙ ren η O ) ∼_)
         & ((λ N₁′ N₂′ → ren η M ⁇ N₁′ ∥ N₂′)
            & ((λ O′ → ren (liftₑ η) N₁ ∙ O′)
               & renwk η O)
            ⊗ ((λ O′ → ren (liftₑ η) N₂ ∙ O′)
               & renwk η O)))
        (comm⩖∙ (ren η M)
                (ren (liftₑ η) N₁)
                (ren (liftₑ η) N₂)
                (ren η O))

ren∼ η (comm⩖π₁ M N₁ N₂)       = comm⩖π₁ (ren η M)
                                         (ren (liftₑ η) N₁)
                                         (ren (liftₑ η) N₂)
ren∼ η (comm⩖π₂ M N₁ N₂)       = comm⩖π₂ (ren η M)
                                         (ren (liftₑ η) N₁)
                                         (ren (liftₑ η) N₂)
ren∼ η (comm⩖φ M N₁ N₂)        = comm⩖φ (ren η M)
                                        (ren (liftₑ η) N₁)
                                        (ren (liftₑ η) N₂)

ren∼ η (comm⩖⁇∥ M N₁ N₂ O₁ O₂)
  = coe ((((ren η M ⁇ ren (liftₑ η) N₁
                    ∥ ren (liftₑ η) N₂) ⁇ ren (liftₑ η) O₁
                                        ∥ ren (liftₑ η) O₂) ∼_)
         & ((λ N₁′ N₂′ → ren η M ⁇ N₁′ ∥ N₂′)
            & ((λ O₁′ O₂′ → ren (liftₑ η) N₁ ⁇ O₁′ ∥ O₂′)
               & renliftwk η O₁ ⊗ renliftwk η O₂)
            ⊗ ((λ O₁′ O₂′ → ren (liftₑ η) N₂ ⁇ O₁′ ∥ O₂′)
               & renliftwk η O₁ ⊗ renliftwk η O₂)))
        (comm⩖⁇∥ (ren η M)
                 (ren (liftₑ η) N₁)
                 (ren (liftₑ η) N₂)
                 (ren (liftₑ η) O₁)
                 (ren (liftₑ η) O₂))

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
module Algebra.Dioid where

record Dioid A (_≡_ : A -> A -> Set) : Set where
  field
    zero : A
    one  : A
    _+_  : A -> A -> A
    _*_  : A -> A -> A

    reflexivity  : ∀ {r     : A} ->                   r ≡ r
    symmetry     : ∀ {r s   : A} -> r ≡ s ->          s ≡ r
    transitivity : ∀ {r s t : A} -> r ≡ s -> s ≡ t -> r ≡ t

    +left-congruence  : ∀ {r s t : A} -> r ≡ s -> (r + t) ≡ (s + t)
    -- +right-congruence holds but as a theorem, please see below
    *left-congruence  : ∀ {r s t : A} -> r ≡ s -> (r * t) ≡ (s * t)
    *right-congruence : ∀ {r s t : A} -> r ≡ s -> (t * r) ≡ (t * s)

    +idempotence   : ∀ {r : A}      -> (r + r)       ≡ r
    +commutativity : ∀ {r s : A}    -> (r + s)       ≡ (s + r)
    +associativity : ∀ {r s t : A}  -> (r + (s + t)) ≡ ((r + s) + t)
    +zero-identity : ∀ {r : A}      -> (r + zero)    ≡ r

    *associativity  : ∀ {r s t : A} -> (r * (s * t)) ≡ ((r * s) * t)
    *left-zero      : ∀ {r : A}     -> (zero * r)    ≡ zero
    *right-zero     : ∀ {r : A}     -> (r * zero)    ≡ zero
    *left-identity  : ∀ {r : A}     -> (one * r)     ≡ r
    *right-identity : ∀ {r : A}     -> (r * one)     ≡ r

    left-distributivity  : ∀ {r s t : A} -> (r * (s + t)) ≡ ((r * s) + (r * t))
    right-distributivity : ∀ {r s t : A} -> ((r + s) * t) ≡ ((r * t) + (s * t))

  -- For convenience to avoid `Dioid._+_ d r s`
  plus : A -> A -> A
  plus x y = x + y

  times : A -> A -> A
  times x y = x * y

+right-congruence : ∀ {D eq} {d : Dioid D eq} {r s t : D} -> eq r s -> eq (Dioid.plus d t r) (Dioid.plus d t s)
+right-congruence {_} {_} {d} {r} {s} {t} e = trans commut (trans (Dioid.+left-congruence d e) commut)
  where
    trans = Dioid.transitivity d
    commut = Dioid.+commutativity d

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs


text:
------------------------------------------------------------------------
-- Pointers to results from the paper
------------------------------------------------------------------------

module README.Pointers-to-results-from-the-paper where

open import Prelude using (Type)
open import Prelude.Size using (∞)

import Colist
import Conat
import Omniscience

import Delay-monad
import Delay-monad.Bisimilarity
import Delay-monad.Monad
import Delay-monad.Quantitative-weak-bisimilarity

import Only-allocation
import Unbounded-space
import Upper-bounds

import Lambda.Compiler
import Lambda.Compiler-correctness
import Lambda.Compiler-correctness.Sizes-match
import Lambda.Compiler-correctness.Steps-match
import Lambda.Delay-crash
import Lambda.Delay-crash-trace
import Lambda.Interpreter
import Lambda.Interpreter.Stack-sizes
import Lambda.Interpreter.Stack-sizes.Counterexample
import Lambda.Interpreter.Stack-sizes.Example
import Lambda.Interpreter.Steps
import Lambda.Interpreter.Steps.Counterexample
import Lambda.Virtual-machine
import Lambda.Virtual-machine.Instructions
import Lambda.Syntax

------------------------------------------------------------------------
-- Section 2

-- Conatural numbers.

Conat  = Conat.Conat
Conat′ = Conat.Conat′

-- Infinity.

infinity = Conat.infinity

-- Ordering.

[_]_≤_  = Conat.[_]_≤_
[_]_≤′_ = Conat.[_]_≤′_

-- Bisimilarity.

[_]_∼N_ = Conat.[_]_∼_

------------------------------------------------------------------------
-- Section 3

-- Programs.

Stmt    = Only-allocation.Stmt
Program = Only-allocation.Program

-- Colists.

Colist = Colist.Colist

-- The interpreter.

modify = Unbounded-space.modify
⟦_⟧₁   = Unbounded-space.⟦_⟧
⟦_⟧′   = Unbounded-space.⟦_⟧′

-- Upper bounds.

[_]_⊑_  = Upper-bounds.[_]_⊑_
[_]_⊑′_ = Upper-bounds.[_]_⊑′_

-- The □ predicate.

□ = Colist.□

-- Least upper bounds.

LUB = Upper-bounds.LUB

-- Least upper bounds are unique up to bisimilarity.

lub-unique = Upper-bounds.lub-unique

-- Antisymmetry for conatural numbers.

antisymmetric = Conat.antisymmetric-≤

-- WLPO.

WLPO = Omniscience.WLPO

-- WLPO is classically valid: it follows from excluded middle and
-- extensionality for functions.

LEM→WLPO = Omniscience.LEM→WLPO

-- WLPO is logically equivalent to one formulation of "least upper
-- bounds exist for every colist".

wlpo⇔lub = Unbounded-space.wlpo⇔lub

-- Maximum heap usage.

Heap-usage = Unbounded-space.Heap-usage

-- This was not mentioned in the paper, but WLPO is also logically
-- equivalent to one formulation of "maximum heap usages exist for
-- every program".

wlpo⇔max = Unbounded-space.wlpo⇔max

-- The maximum heap usage is unique up to bisimilarity.

max-unique = Unbounded-space.max-unique

-- Some examples.

bounded   = Only-allocation.bounded
bounded₂  = Only-allocation.bounded₂
unbounded = Only-allocation.unbounded
_∷′_      = Colist._∷′_

-- The example programs have infinitely long traces.

bounded-loops   = Unbounded-space.bounded-loops
bounded₂-loops  = Unbounded-space.bounded₂-loops
unbounded-loops = Unbounded-space.unbounded-loops

-- Properties showing that the example programs have certain maximum
-- heap usages.

max-bounded-1   = Unbounded-space.max-bounded-1
max-bounded₂-2  = Unbounded-space.max-bounded₂-2
max-unbounded-∞ = Unbounded-space.max-unbounded-∞

-- If no natural number is an upper bound of the heap usage of p, then
-- the maximum heap usage of p is infinity.

no-finite-max→infinite-max = Unbounded-space.no-finite-max→infinite-max

-- If no natural number is an upper bound of ms, but the conatural
-- number m is, then m is bisimilar to infinity.

no-finite→infinite = Upper-bounds.no-finite→infinite

------------------------------------------------------------------------
-- Section 4

-- The optimiser.

opt = Unbounded-space.opt

-- The optimiser improves the space complexity of at least one
-- program.

opt-improves = Unbounded-space.opt-improves

-- The semantics of optimise bounded-space₂ matches that of
-- bounded-space.

opt-bounded₂∼bounded = Unbounded-space.opt-bounded₂∼bounded

-- Bisimilarity of colists.

[_]_∼L_ = Colist.[_]_∼_

-- The maximum heap usage of an optimised program is at most as high
-- as that of the original program (assuming that these maximums
-- exist).

opt-correct = Unbounded-space.opt-correct

-- The [_]_≲_ relation.

[_]_≲_  = Upper-bounds.[_]_≲_
[_]_≲′_ = Upper-bounds.[_]_≲′_

-- If ms has the least upper bound m, and ns has the least upper bound
-- n, then ms is bounded by ns if and only if m is bounded by n.

≲⇔least-upper-bounds-≤ = Upper-bounds.≲⇔least-upper-bounds-≤

-- Four combinators that can be used to prove that one colist is
-- bounded by another.

[]≲     = Upper-bounds.[]≲
consʳ-≲ = Upper-bounds.consʳ-≲
consˡ-≲ = Upper-bounds.consˡ-≲
cons′-≲ = Upper-bounds.cons′-≲
Bounded = Upper-bounds.Bounded

-- If consʳ-≲ had taken the primed variant of the relation as an
-- argument instead, then one could have proved that any colist was
-- bounded by any infinite colist, and this leads to a contradiction.

consʳ-≲′→≲-infinite = Upper-bounds.consʳ-≲′→≲-infinite
¬-consʳ-≲′          = Upper-bounds.¬-consʳ-≲′

-- The [_]_≲_ relation is a preorder. (The transitivity result has a
-- type signature that differs slightly from that given in the paper.)

reflexive-≲  = Upper-bounds._□≲
transitive-≲ = Upper-bounds.step-≲

-- Transitivity cannot be made size-preserving in the second argument.

¬-transitivity-size-preservingʳ =
  Upper-bounds.¬-transitivity-size-preservingʳ

-- A size-preserving variant of transitivity. (This result has a
-- type signature that differs slightly from that given in the paper.)

transitive-∼≲ = Upper-bounds.step-∼≲

-- The main lemma used to prove that the maximum heap usage of an
-- optimised program is at most as high as that of the original
-- program (assuming that these maximums exist).

opt-correct-≲ = Unbounded-space.opt-correct-≲

------------------------------------------------------------------------
-- Section 5

-- The delay monad.

Delay = Delay-monad.Delay

-- The non-terminating computation never.

never = Delay-monad.never

-- Monad instance.

monad-instance₁ = Delay-monad.Monad.delay-raw-monad

-- Strong bisimilarity.

[_]_∼D_ = Delay-monad.Bisimilarity.[_]_∼_

-- Monad laws.

left-identity₁  = Delay-monad.Monad.left-identity′
right-identity₁ = Delay-monad.Monad.right-identity′
associativity₁  = Delay-monad.Monad.associativity′

-- Weak bisimilarity. (This relation is not defined in exactly the
-- same way as in the paper.)

[_]_≈D_ = Delay-monad.Bisimilarity.[_]_≈_

------------------------------------------------------------------------
-- Section 6

-- Terms.

Tm = Lambda.Syntax.Tm

-- Environments and values. (The code uses a definition which is
-- parametrised by the type of terms. The same definition is used also
-- for virtual machine environments and values.)

Env   = Lambda.Syntax.Closure.Env
Value = Lambda.Syntax.Closure.Value

-- DelayC (called Delay-crash in the code) and crash.

DelayC = Lambda.Delay-crash.Delay-crash

crash : {A : Type} → DelayC A ∞
crash = Lambda.Delay-crash.crash

-- The computation crash (in fact, any computation of the form now x)
-- is not weakly bisimilar to never.

now≉never = Delay-monad.Bisimilarity.now≉never

-- The interpreter.

_∙_  = Lambda.Interpreter._∙_
⟦_⟧₂ = Lambda.Interpreter.⟦_⟧
⟦if⟧ = Lambda.Interpreter.⟦if⟧

------------------------------------------------------------------------
-- Section 7

-- DelayCT (called Delay-crash-trace in the code).

DelayCT = Lambda.Delay-crash-trace.Delay-crash-trace
trace   = Lambda.Delay-crash-trace.trace
delayC  = Lambda.Delay-crash-trace.delay-crash

-- Monad instance.

monad-instance₂ = Lambda.Delay-crash-trace.raw-monad

-- Strong bisimilarity.

[_]_∼DCT_ = Lambda.Delay-crash-trace.[_]_∼_

-- Monad laws.

left-identity₂  = Lambda.Delay-crash-trace.left-identity
right-identity₂ = Lambda.Delay-crash-trace.right-identity
associativity₂  = Lambda.Delay-crash-trace.associativity

-- Instructions and code.

Instr = Lambda.Virtual-machine.Instructions.Instr
Code  = Lambda.Virtual-machine.Instructions.Code

-- Environments and values. (The code uses a definition which is
-- parametrised by the type of terms. The same definition is used also
-- for the interpreter's environments and values.)

VM-Env   = Lambda.Syntax.Closure.Env
VM-Value = Lambda.Syntax.Closure.Value

-- Stack elements and stacks.

Stack-element = Lambda.Virtual-machine.Instructions.Stack-element
Stack         = Lambda.Virtual-machine.Instructions.Stack

-- States.

State = Lambda.Virtual-machine.Instructions.State

-- The virtual machine.

Result      = Lambda.Virtual-machine.Instructions.Result
step        = Lambda.Virtual-machine.step
exec⁺       = Lambda.Virtual-machine.exec⁺
exec⁺′      = Lambda.Virtual-machine.exec⁺′
exec        = Lambda.Virtual-machine.exec
stack-sizes = Lambda.Virtual-machine.stack-sizes

------------------------------------------------------------------------
-- Section 8

-- Tail context information.

In-tail-context = Lambda.Compiler.In-tail-context

-- The compilation functions.

comp      = Lambda.Compiler.comp
comp-body = Lambda.Compiler.comp-body
comp-name = Lambda.Compiler.comp-name
comp-env  = Lambda.Compiler.comp-env
comp-val  = Lambda.Compiler.comp-val
comp₀     = Lambda.Compiler.comp₀

-- Compiler correctness.

compiler-correct = Lambda.Compiler-correctness.correct

-- The key lemma used to prove compiler correctness.

key-lemma₁ = Lambda.Compiler-correctness.⟦⟧-correct
Cont-OK    = Lambda.Compiler-correctness.Cont-OK
Stack-OK   = Lambda.Compiler-correctness.Stack-OK

------------------------------------------------------------------------
-- Section 9

-- The instrumented interpreter.

[_,_]_∙S_    = Lambda.Interpreter.Stack-sizes.[_,_]_∙_
⟦_⟧S         = Lambda.Interpreter.Stack-sizes.⟦_⟧
δ            = Lambda.Interpreter.Stack-sizes.δ
⟦if⟧S        = Lambda.Interpreter.Stack-sizes.⟦if⟧
scanl        = Colist.scanl
numbers      = Lambda.Interpreter.Stack-sizes.numbers
stack-sizesS = Lambda.Interpreter.Stack-sizes.stack-sizes

-- The instrumented semantics produces computations that are strongly
-- bisimilar to those produced by the other semantics.

⟦⟧∼⟦⟧ = Lambda.Interpreter.Stack-sizes.⟦⟧∼⟦⟧

-- If the trace of stack sizes produced by the instrumented semantics
-- has the least upper bound i, and the corresponding trace produced
-- by the virtual machine has the least upper bound v, then i and v
-- are bisimilar.

maximum-stack-sizes-match =
  Lambda.Compiler-correctness.Sizes-match.maximum-stack-sizes-match

-- The trace of stack sizes produced by the virtual machine is not
-- necessarily bisimilar to that produced by the instrumented
-- interpreter.

stack-sizes-not-bisimilar =
  Lambda.Interpreter.Stack-sizes.Counterexample.stack-sizes-not-bisimilar

-- The trace of stack sizes produced by the virtual machine and that
-- produced by the instrumented interpreter are upper bounds of each
-- other.

stack-sizes-related =
  Lambda.Compiler-correctness.Sizes-match.stack-sizes-related

-- The [_]_≂_ relation.

[_]_≂_  = Upper-bounds.[_]_≂_
[_]_≂′_ = Upper-bounds.[_]_≂′_

-- Colists that are related by this relation have the same least upper
-- bounds (if any).

LUB-cong = Upper-bounds.LUB-cong

-- Some combinators that can be used to prove that two colists are
-- bounded by each other.

consʳ-≂ = Upper-bounds.consʳ-≂
consˡ-≂ = Upper-bounds.consˡ-≂
cons-≂  = Upper-bounds.cons-≂
cons′-≂ = Upper-bounds.cons′-≂

-- The [_]_≂_ relation is an equivalence relation. (The
-- transitivity-like results have type signatures that differ slightly
-- from those given in the paper.)

reflexive-≂   = Upper-bounds._□≂
symmetric-≂   = Upper-bounds.symmetric-≂
transitive-≂  = Upper-bounds.step-≂
transitive-∼≂ = Upper-bounds.step-∼≂
transitive-≂∼ = Upper-bounds.step-≂∼

-- The [_]_≂″_ relation.

[_]_≂″_ = Upper-bounds.[_]_≂″_

-- [_]_≂′_ and [_]_≂″_ are pointwise logically equivalent.

≂′⇔≂″ = Upper-bounds.≂′⇔≂″

-- This was not mentioned in the paper, but a corresponding relation
-- can also be defined for [_]_≲′_.

[_]_≲″_ = Upper-bounds.[_]_≲″_
≲′⇔≲″   = Upper-bounds.≲′⇔≲″

-- The key lemma used to prove correctness.

key-lemma₂ = Lambda.Compiler-correctness.Sizes-match.⟦⟧-correct

-- A non-terminating program that requires unbounded stack space.

Ω                          = Lambda.Syntax.Ω
Ω-loops                    = Lambda.Interpreter.Ω-loops′
Ω-requires-unbounded-space =
  Lambda.Interpreter.Stack-sizes.Ω-requires-unbounded-space

-- A non-terminating program that runs in bounded stack space.

go               = Lambda.Interpreter.Stack-sizes.Example.go
go-loops         = Lambda.Interpreter.Stack-sizes.Example.go-loops
go-bounded-stack =
  Lambda.Interpreter.Stack-sizes.Example.go-bounded-stack

------------------------------------------------------------------------
-- Section 10

-- The uninstrumented interpreter does not provide a suitable cost
-- measure, in the sense that there is a family of programs for which
-- the running "time" (number of steps) of the corresponding compiled
-- programs on the virtual machine is not linear in the running time
-- on the interpreter.

not-suitable-cost-measure =
  Lambda.Interpreter.Steps.Counterexample.not-suitable-cost-measure

-- The instrumented interpreter.

✓_    = Lambda.Interpreter.Steps.✓_
_∙T_  = Lambda.Interpreter.Steps._∙_
⟦_⟧T  = Lambda.Interpreter.Steps.⟦_⟧
⟦if⟧T = Lambda.Interpreter.Steps.⟦if⟧

-- The cost measure provided by the instrumented interpreter is
-- "suitable", in the sense that the cost of running a compiled
-- program on the virtual machine is linear in the cost of running the
-- corresponding source program on the interpreter, and vice versa.

the-cost-measure-is-suitable =
  Lambda.Compiler-correctness.Steps-match.steps-match

-- Quantitative weak bisimilarity.

[_∣_∣_∣_∣_]_≈D_ =
  Delay-monad.Quantitative-weak-bisimilarity.[_∣_∣_∣_∣_]_≈_

-- A characterisation of quantitative weak bisimilarity.

≈⇔≈×steps≤steps² =
  Delay-monad.Quantitative-weak-bisimilarity.≈⇔≈×steps≤steps²

-- The left-to-right direction of the characterisation can be made
-- size-preserving.

≈→≈×steps≤steps² =
  Delay-monad.Quantitative-weak-bisimilarity.≈→≈×steps≤steps²

-- The right-to-left direction of the characterisation can be made
-- size-preserving if and only if the carrier type is uninhabited
-- (assuming that Agda is not buggy).

≈×steps≤steps²→≈⇔uninhabited =
  Delay-monad.Quantitative-weak-bisimilarity.≈×steps≤steps²→≈⇔uninhabited

-- Weakening.

weaken = Delay-monad.Quantitative-weak-bisimilarity.weaken

-- Two transitivity-like results.

transitive-≳∼ = Delay-monad.Quantitative-weak-bisimilarity.transitive-≳∼
transitive-≈∼ = Delay-monad.Quantitative-weak-bisimilarity.transitive-≈∼
transitive-∼≈ = Delay-monad.Quantitative-weak-bisimilarity.transitive-∼≈

-- The key lemma used to prove that the cost measure is "suitable".

key-lemma₃ = Lambda.Compiler-correctness.Steps-match.⟦⟧-correct

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
module Data.Lens.Proofs.LensPostulates where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws

---- Lens postulates
-- These are provable using the isomorphism to the getter+setter style
-- However, defining this isomorphism is quite a bit of work, so I didn't do it for now

postulate
    -- view (l1 ∘ l2) ≡ view l2 ∘ view l1
    -- This is clearly true from how view works
    prop-view-compose : {a b c : Set}
        -> (l1 : ValidLens a b)
        -> (l2 : ValidLens b c)
        -> (v : a)
        -> (view ((toLens l1) ∘ (toLens l2))) v ≡ (view (toLens l2) ∘ view (toLens l1)) v
    -- set (l1 ∘ l2) ≡ over l1 (set l2 t) v
    -- This is clearly true from how set works
    prop-set-compose : {a b c : Set}
        -> (l1 : ValidLens a b)
        -> (l2 : ValidLens b c)
        -> (v : a) (t : c)
        -> (set ((toLens l1) ∘ (toLens l2))) t v ≡ over (toLens l1) (set (toLens l2) t) v
    -- over l ≡ set l (view l v) v
    -- This is clearly true from how over works
    prop-over-is-setget : {a b : Set}
        -> (l : ValidLens a b)
        -> (f : b -> b) (v : a)
        -> over (toLens l) f v ≡ set (toLens l) (f (view (toLens l) v)) v

-- We can merge postulate 2 and 3

prop-set-compose-dir : {a b c : Set}
    -> (l1 : ValidLens a b)
    -> (l2 : ValidLens b c)
    -> (v : a) (t : c)
    -> (set ((toLens l1) ∘ (toLens l2))) t v ≡ set (toLens l1) ((set (toLens l2) t) (view (toLens l1) v)) v
prop-set-compose-dir vl1@(CValidLens l1 vs1 sv1 ss1) vl2@(CValidLens l2 vs2 sv2 ss2) v t =
    begin
        set (l1 ∘ l2) t v
    =⟨ prop-set-compose vl1 vl2 v t ⟩
        over l1 (set l2 t) v
    =⟨ prop-over-is-setget vl1 (set l2 t) v ⟩
        set l1 ((set l2 t) (view l1 v)) v
    end

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
module examplesPaperJFP.Collatz where

open import Data.Nat.Base
open import Data.Nat.DivMod
open import Data.Fin using (Fin; zero; suc)

open import examplesPaperJFP.Colists

collatzStep            :  ℕ → ListF ℕ ℕ
collatzStep 1          =  nil
collatzStep n          with n divMod 2
... | result q zero _  =  cons n q
... | _                =  cons n (1 + 3 * n)

collatzSequence  :  ℕ → Colist ℕ
collatzSequence  =  unfold collatzStep

open Colist
open import Data.List

displayList : Colist ℕ → ℕ → List ℕ
displayList s 0 = []
displayList s (suc m) with  force s
... | nil = []
... | (cons k s′) =  k ∷ displayList s′ m

displayCollatz : ℕ → ℕ → List ℕ
displayCollatz n m = displayList (collatzSequence n) m

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
import      Lvl
open import Type

module Type.Univalence where

open import Functional
import      Logic.Predicate
import      Relator.Equals
import      Relator.Equals.Proofs
import      Type.Cardinality
import      Type.Cardinality.Proofs
import      Type.Functions
import      Type.Functions.Inverse

module _ {ℓₗ ℓₒ : Lvl.Level} where
  open Logic.Predicate
  open Relator.Equals{ℓₗ Lvl.⊔ ℓₒ}{Lvl.𝐒(ℓₒ)}
  open Type.Cardinality {ℓₗ}
  open Type.Cardinality.Proofs {ℓₗ}
  open Type.Functions

  UnivalenceAxiom : Type{ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ)}
  UnivalenceAxiom = ∀{X Y : Type{ℓₒ}} → Bijective{ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ)} ([≡]-to-[≍] {ℓₒ} {X}{Y})

module _ {ℓₗ ℓₒ : Lvl.Level} {univalence : UnivalenceAxiom} where
  open Logic.Predicate
  open Relator.Equals
  open Relator.Equals.Proofs
  open Type.Cardinality
  open Type.Cardinality.Proofs
  open Type.Functions.Inverse

  instance
    [≡][≍]-bijection : ∀{X Y} → ((X ≡ Y) ≍ (X ≍ Y))
    [≡][≍]-bijection {X}{Y} = [∃]-intro ([≡]-to-[≍] {ℓₗ}{ℓₒ} {X}{Y}) ⦃ univalence{X}{Y} ⦄

  [≍]-to-[≡] : ∀{X Y : Type{ℓₒ}} → (X ≍ Y) → (X ≡ Y)
  [≍]-to-[≡] {X}{Y} = inv([≡]-to-[≍] {ℓₗ}{ℓₒ} {X}{Y}) ⦃ univalence {X}{Y} ⦄

module _ {ℓₗ ℓₒ₁ ℓₒ₂ : Lvl.Level} {univalence : UnivalenceAxiom {ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₁)}{ℓₒ₁}} where
  open Logic.Predicate
  open Relator.Equals
  open Relator.Equals.Proofs
  open Type.Cardinality {ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₁)}
  open Type.Cardinality.Proofs {ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₁)}
  open Type.Functions

  _≡₂_ = _≡_ {ℓₗ}{ℓₒ₂}
  _≡ₗ_ = _≡_ {ℓₗ}

  -- For any type function P from an universe Type{ℓₒ₁} to Type{ℓₒ₂}
  -- where subst, a substitution for P holds using (_≍_)
  -- and where the substitution by reflexivity using (_≍_) gives the exact same proof (is a identity function),
  -- then this substitution will give the same results as the standard substitution rule for equalities (_≡_) for this P.
  postulate transport-theorem : ∀{P : Type{ℓₒ₁} → Type{ℓₒ₂}}
                      → (subst : (∀{X Y} → (X ≍ Y) → P(X) → P(Y)))
                      → (subst-id : (∀{X} → (px : P(X)) → (subst([≍]-reflexivity) (px) ≡₂ px)))
                      → ∀{X Y}
                      → (xy : (X ≍ Y))
                      → (px : P(X))
                      → (subst(xy) (px) ≡₂ [≡]-substitutionᵣ {ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₁)}{Lvl.𝐒(ℓₒ₁)} ([≍]-to-[≡] {ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₁)}{ℓₒ₁} {univalence} (xy)) {P} px)
  -- transport-theorem {P} (subst) (subst-id) ([∃]-intro bijection ⦃ bijective ⦄) px =
    -- subst(xy) (px)
    -- = subst(inv bijection (bijection xy)) (px)
    -- = [≡]-substitutionᵣ (bijection xy) {P} (px)

  postulate substitution-is-bijective : ∀{P : Type{ℓₒ₁} → Type{ℓₒ₂}}
                      → (subst : (∀{X Y} → (X ≍ Y) → P(X) → P(Y)))
                      → (subst-id : (∀{X} → (px : P(X)) → (subst([≍]-reflexivity) (px) ≡₂ px)))
                      → ∀{X Y}{xy : (X ≍ Y)} → Bijective{ℓₗ Lvl.⊔ Lvl.𝐒(ℓₒ₂)} (subst(xy))

  -- TODO: univalence should probably have other level parameters from this point on

  postulate [∘]ₗ-bijective : ∀{ℓₒ₃}{X : Type{ℓₒ₁}}{Y : Type{ℓₒ₂}}{Z : Type{ℓₒ₃}}{g : X → Y} → Bijective{ℓₗ}(g) → Bijective{ℓₗ}(\(f : Y → Z) → f ∘ g)

  postulate [∘]ₗ-cancellationᵣ : ∀{ℓₒ₃}{X : Type{ℓₒ₁}}{Y : Type{ℓₒ₂}}{Z : Type{ℓₒ₃}}{f g : Y → Z}{h : X → Y} → Bijective{ℓₗ}(h) → (f ∘ h ≡ₗ  g ∘ h) → (f ≡ₗ g)

  -- subst{T} P {x}{y} xy fx = [≡]-substitutionᵣ{T}{x}{y} (xy) {P} fx

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:
module static where

open import Data.Nat using (ℕ; _+_; zero; suc)
open import Data.Fin using (Fin; toℕ; zero; suc)
open import Data.Vec using (lookup; _∷_; [])
open import Data.Bool using (Bool; true; false)
open import LSsyntax
open import Relation.Binary.PropositionalEquality -- using (_≡_; refl)

-- inference rules for typed terms
data STyped {n} (Γ : Ctx n) : GType → Set where
    Sx   : ∀ {S} (v : Fin n) → S ≡ lookup v Γ → STyped Γ S
    Sb   : Bool → (ℓ : Label) → STyped Γ (bool ℓ)
    _S∧_ : ∀ {t₁ t₂} → STyped Γ t₁ → STyped Γ t₂ → STyped Γ (bool (getLabel t₁ ~⋎~ getLabel t₂))
    _S∨_ : ∀ {t₁ t₂} → STyped Γ t₁ → STyped Γ t₂ → STyped Γ (bool (getLabel t₁ ~⋎~ getLabel t₂))
    Sif  : ∀ {t t₁ t₂} → STyped Γ t → STyped Γ t₁ → STyped Γ t₂ → STyped Γ (bool (getLabel (t₁ :∨: t₂) ~⋎~ getLabel t))
    S∙   : ∀ {t₁ ℓ t₂ t₃} → STyped Γ ((t₁ ⇒ ℓ) t₂) → STyped Γ t₃ → t₃ ≾ t₁ → STyped Γ (bool ((getLabel t₂) ~⋎~ ℓ))
    Sλ   : ∀ t₁ {t₂} ℓ → STyped (t₁ ∷ Γ) t₂ → STyped Γ ((t₁ ⇒ ℓ) t₂)

erase : ∀ {n} {Γ : Ctx n} {t} → STyped Γ t → Term
erase (Sx v x)      = var (toℕ v)
erase (Sb b ℓ)      = litBool b ℓ
erase (t₁ S∧ t₂)    = (erase t₁) ∧ erase t₂
erase (t₁ S∨ t₂)    = (erase t₁) ∨ (erase t₂)
erase (Sif b t₁ t₂) = if (erase b) then (erase t₁) else (erase t₂)
erase (S∙ t₁ t₂ _)  = (erase t₁) ∙ (erase t₂)
erase (Sλ t₁ ℓ t)   = lam t₁ (erase t) ℓ

data Fromℕ (n : ℕ) : ℕ → Set where
    yes : (m : Fin n) → Fromℕ n (toℕ m)
    no  : (m : ℕ) → Fromℕ n (n + m)

fromℕ : ∀ n m → Fromℕ n m
fromℕ zero m = no m
fromℕ (suc n) zero = yes zero
fromℕ (suc n) (suc m) with fromℕ n m
fromℕ (suc n) (suc .(toℕ m)) | yes m = yes (suc m)
fromℕ (suc n) (suc .(n + m)) | no m = no m

data Check {n} (Γ : Ctx n) : Term → Set where
    yes : (τ : GType) (t : STyped Γ τ) → Check Γ (erase t)
    no  : {e : Term} → Check Γ e

staticCheck : ∀ {n} (Γ : Ctx n) (t : Term) → Check Γ t
staticCheck {n} Γ (var v) with fromℕ n v
staticCheck {n} Γ (var .(toℕ m)) | yes m = yes (lookup m Γ) (Sx m refl)
staticCheck {n} Γ (var .(n + m)) | no m = no

staticCheck Γ (litBool x ℓ) = yes (bool ℓ) (Sb x ℓ)

staticCheck Γ (lam x t ℓ) with staticCheck (x ∷ Γ) t
staticCheck Γ (lam x .(erase t) ℓ) | yes τ t = yes ((x ⇒ ℓ) τ) (Sλ x ℓ t)
staticCheck Γ (lam x t ℓ) | no = no

staticCheck Γ (t ∧ t₁) with staticCheck Γ t | staticCheck Γ t₁
staticCheck Γ (.(erase t₁) ∧ .(erase t)) | yes τ₁ t₁ | (yes τ t) = yes (bool (getLabel τ₁ ~⋎~ getLabel τ)) (t₁ S∧ t)
staticCheck Γ (.(erase t) ∧ t₁) | yes τ t | no = no
staticCheck Γ (t₁ ∧ .(erase t)) | no | yes τ t = no
staticCheck Γ (t ∧ t₁) | no | no = no

staticCheck Γ (t ∨ t₁) with staticCheck Γ t | staticCheck Γ t₁
staticCheck Γ (.(erase t₁) ∨ .(erase t)) | yes τ₁ t₁ | (yes τ t) = yes (bool (getLabel τ₁ ~⋎~ getLabel τ)) (t₁ S∨ t)
staticCheck Γ (.(erase t) ∨ t₁) | yes τ t | no = no
staticCheck Γ (t₁ ∨ .(erase t)) | no | yes τ t = no
staticCheck Γ (t ∨ t₁) | no | no = no

staticCheck Γ (t ∙ t₁) with staticCheck Γ t | staticCheck Γ t₁
staticCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ) τ₂) t | (yes τ₁ t₁) with τ₁ ≾? τ
staticCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ) τ₂) t | (yes τ₁ t₁) | (yes .τ₁ .τ) = yes (bool (getLabel τ₂ ~⋎~ ℓ)) (S∙ t t₁ (yes τ₁ τ))
staticCheck Γ (.(erase t) ∙ .(erase t₁)) | yes ((τ ⇒ ℓ) τ₂) t | (yes τ₁ t₁) | (no .τ₁ .τ) = no
staticCheck Γ (.(erase t) ∙ .(erase t₁)) | yes err t | (yes τ₁ t₁) = no
staticCheck Γ (.(erase t) ∙ .(erase t₁)) | yes (bool x) t | (yes τ₁ t₁) = no
staticCheck Γ (.(erase t) ∙ t₁) | yes τ t | no = no
staticCheck Γ (t₁ ∙ .(erase t)) | no | yes τ t = no
staticCheck Γ (t ∙ t₁) | no | no = no

staticCheck Γ (if b then t₁ else t₂) with staticCheck Γ b
staticCheck Γ (if .(erase t) then t₁ else t₂) | yes τ t with staticCheck Γ t₁ | staticCheck Γ t₂
staticCheck Γ (if .(erase t₂) then .(erase t₁) else .(erase t)) | yes τ₂ t₂ | (yes τ₁ t₁) | (yes τ t) = yes (bool (getLabel (τ₁ :∨: τ) ~⋎~ getLabel τ₂)) (Sif t₂ t₁ t)
staticCheck Γ (if .(erase t₁) then .(erase t) else t₂)          | yes τ₁ t₁ | (yes τ t)   | no = no
staticCheck Γ (if .(erase t₂) then t₁ else .(erase t))          | yes τ₁ t₂ | no          | (yes τ t) = no
staticCheck Γ (if .(erase t) then t₁ else t₂)                   | yes τ t   | no          | no = no
staticCheck Γ (if b then t₁ else t₂)                            | no = no

staticCheck Γ error = no

-- examples from Section 3.5

-- Type : yes ((bool ⊥ ⇒ ⊥) (bool ⊥)) (Sλ (bool ⊥) ⊥ (Sx zero refl S∧ Sx zero refl))
f : Term
f = lam (bool ⊥) (var 0 ∨ var 0) ⊥

-- Type : yes ((bool ✭ ⇒ ⊥) (bool ✭)) (Sλ (bool ✭) ⊥ (Sx zero refl S∨ Sx zero refl))
g : Term
g = lam (bool ✭) (var 0 ∧ var 0) ⊥

-- Type : yes (bool ⊤) (Sb false ⊤)
v : Term
v = litBool false ⊤

test₁ : staticCheck [] (f ∙ v) ≡ no
test₁ = refl

max_stars_repo_path: Agda/Gradual Security/static.agda

max_stars_repo_name: kellino/TypeSystems

max_issues_repo_path: Agda/Gradual Security/static.agda

max_issues_repo_name: kellino/TypeSystems

max_forks_repo_path: Agda/Gradual Security/static.agda

max_forks_repo_name: kellino/TypeSystems


text:
module sets.nat.core where

open import level
open import decidable
open import equality.core
open import function.core
open import function.isomorphism.core
open import sets.empty

infixr 8 _^_
infixl 7 _*_
infixl 6 _+_

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

{-# BUILTIN NATURAL ℕ    #-}

pred : ℕ → ℕ
pred zero    = zero
pred (suc n) = n

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

_*_ : ℕ → ℕ → ℕ
0 * n = zero
suc m * n = n + m * n

_^_ : ℕ → ℕ → ℕ
n ^ 0 = 1
n ^ (suc m) = n * (n ^ m)

suc-inj : injective suc
suc-inj = ap pred

_≟_ : (a b : ℕ) → Dec (a ≡ b)
zero  ≟ zero  = yes refl
zero  ≟ suc _ = no (λ ())
suc _ ≟ zero  = no (λ ())
suc a ≟ suc b with a ≟ b
suc a ≟ suc b | yes a≡b = yes $ ap suc a≡b
suc a ≟ suc b | no ¬a≡b = no $ (λ sa≡sb → ¬a≡b (ap pred sa≡sb))

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module _ where

module First where
  postulate
    C  : Set → Set
    it : {A : Set} ⦃ _ : C A ⦄ → A
    X  : Set

module Second where
  open First
  postulate instance iCX : C X

module Nested where
  open First
  x : X
  x = it   -- Second.iCX is in scope


text:
-- Andreas, 2016-07-08
-- Better error message for private modules

module _ where

module M where
  private module Private where

module ShouldFail = M.Private

-- Current:
-- No such module M.Private

-- Better:
-- M.Private is not in scope since it is declared as private
-- Or (simpler):
-- M.Private exists but is not in scope here

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Base
open import Homotopy.TruncatedHIT
open import Integers

module Algebra.FreeGroup {i} (A : Set i) where

{-
The definition is the following

    (0)data freegroup : Set i where
      e : freegroup
      _·_   : A → freegroup → freegroup
      _⁻¹·_ : A → freegroup → freegroup
      right-inverse-· : (x : A) (u : freegroup) → x · (x ⁻¹· u) ≡ u
      left-inverse-·  : (x : A) (u : freegroup) → x ⁻¹· (x · u) ≡ u

("(0)data" means that it’s a higher inductive 0-truncated type)
-}

private
  data #freegroup : Set i where
    #e  : #freegroup
    #·  : A → #freegroup → #freegroup
    #⁻¹· : A → #freegroup → #freegroup

    #top : (f : hSⁿ ⟨0⟩ → #freegroup) → #freegroup

freegroup : Set i
freegroup = #freegroup

e : freegroup
e = #e

_·_ : A → freegroup → freegroup
_·_ = #·

_⁻¹·_ : A → freegroup → freegroup
_⁻¹·_ = #⁻¹·

postulate  -- HIT
  right-inverse-· : (x : A) (u : freegroup) → x · (x ⁻¹· u) ≡ u
  left-inverse-·  : (x : A) (u : freegroup) → x ⁻¹· (x · u) ≡ u

top : (f : hSⁿ ⟨0⟩ → freegroup) → freegroup
top = #top

postulate  -- HIT
  rays : (f : hSⁿ ⟨0⟩ → freegroup) (x : hSⁿ ⟨0⟩) → top f ≡ f x

#freegroup-rec : ∀ {j} (P : freegroup → Set j)
  (base : P e)
  (g   : (x : A) (u : freegroup) → P u → P (x · u))
  (g'  : (x : A) (u : freegroup) → P u → P (x ⁻¹· u))
  (gg' : (x : A) (u : freegroup) (t : P u)
         → transport P (right-inverse-· x u) (g x _ (g' x u t)) ≡ t)
  (g'g : (x : A) (u : freegroup) (t : P u)
         → transport P (left-inverse-· x u) (g' x _ (g x u t)) ≡ t)
  (top* :  (f : hSⁿ ⟨0⟩ → freegroup) (p : (x : hSⁿ ⟨0⟩) → P (f x)) → P (top f))
  (rays* : (f : hSⁿ ⟨0⟩ → freegroup) (p : (x : hSⁿ ⟨0⟩) → P (f x)) (x : hSⁿ ⟨0⟩)
         → transport P (rays f x) (top* f p) ≡ p x)
  → ((t : freegroup) → P t)
#freegroup-rec P base g g' gg' g'g top* rays* #e = base
#freegroup-rec P base g g' gg' g'g top* rays* (#· x u) =
  g x u (#freegroup-rec P base g g' gg' g'g top* rays* u)
#freegroup-rec P base g g' gg' g'g top* rays* (#⁻¹· x u) =
  g' x u (#freegroup-rec P base g g' gg' g'g top* rays* u)
#freegroup-rec P base g g' gg' g'g top* rays* (#top f) =
  top* f (λ x → #freegroup-rec P base g g' gg' g'g top* rays* (f x))

#freegroup-rec-nondep : ∀ {j} (B : Set j)
  (base : B)
  (g   : A → B → B)
  (g'  : A → B → B)
  (gg' : (x : A) (u : B) → (g x (g' x u)) ≡ u)
  (g'g : (x : A) (u : B) → (g' x (g x u)) ≡ u)
  (top* :  (f : hSⁿ ⟨0⟩ → freegroup) (p : hSⁿ ⟨0⟩ → B) → B)
  (rays* : (f : hSⁿ ⟨0⟩ → freegroup) (p : hSⁿ ⟨0⟩ → B) (x : hSⁿ ⟨0⟩)
    → top* f p ≡ p x)
  → freegroup → B
#freegroup-rec-nondep P base g g' gg' g'g top* rays* #e = base
#freegroup-rec-nondep P base g g' gg' g'g top* rays* (#· x u) =
  g x (#freegroup-rec-nondep P base g g' gg' g'g top* rays* u)
#freegroup-rec-nondep P base g g' gg' g'g top* rays* (#⁻¹· x u) =
  g' x (#freegroup-rec-nondep P base g g' gg' g'g top* rays* u)
#freegroup-rec-nondep P base g g' gg' g'g top* rays* (#top f) =
  top* f (λ x → #freegroup-rec-nondep P base g g' gg' g'g top* rays* (f x))

freegroup-rec : ∀ {j} (P : freegroup → Set j)
  (base : P e)
  (g   : (x : A) (u : freegroup) → P u → P (x · u))
  (g'  : (x : A) (u : freegroup) → P u → P (x ⁻¹· u))
  (gg' : (x : A) (u : freegroup) (t : P u)
         → transport P (right-inverse-· x u) (g x _ (g' x u t)) ≡ t)
  (g'g : (x : A) (u : freegroup) (t : P u)
         → transport P (left-inverse-· x u) (g' x _ (g x u t)) ≡ t)
  (p : (u : freegroup) → is-set (P u))
  → ((t : freegroup) → P t)
freegroup-rec P base g g' gg' g'g p =
  #freegroup-rec P base g g' gg' g'g
                 (λ f p₁ → π₁ (u f p₁))
                 (λ f p₁ → π₂ (u f p₁)) where
  u = truncated-has-filling-dep freegroup P ⟨0⟩ (λ ()) (λ f → (top f , rays f))

freegroup-rec-nondep : ∀ {j} (B : Set j)
  (base : B)
  (g   : A → B → B)
  (g'  : A → B → B)
  (gg' : (x : A) (u : B) → (g x (g' x u)) ≡ u)
  (g'g : (x : A) (u : B) → (g' x (g x u)) ≡ u)
  (p : is-set B)
  → freegroup → B
freegroup-rec-nondep B base g g' gg' g'g p =
  #freegroup-rec-nondep B base g g' gg' g'g
                        (λ _ p → π₁ (u p))
                        (λ _ p → π₂ (u p)) where
  u = truncated-has-spheres-filled ⟨0⟩ _ p

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.List.Relation.Binary.Permutation where

open import Prelude
open import Data.List
open import Data.Fin
open import Data.Fin.Properties
open import Data.List.Membership
open import Cubical.Foundations.Equiv
import Function.Isomorphism as Isomorphism
open import Relation.Binary
open import Cubical.Foundations.Prelude using (J; _∧_)
open import Cubical.Foundations.Transport using (isSet-subst)
open import Cubical.Data.Sigma.Properties
open import Data.Nat.Properties using (znots; snotz)

infixr 0 _↝_
_↝_ : {A : Type a} (xs ys : List A) → Type a
xs ↝ ys = ∀ x → x ∈ xs → x ∈ ys

infix 4 _↭_
_↭_ : {A : Type a} (xs ys : List A) → Type a
xs ↭ ys = ∀ x → (x ∈ xs) ⇔ (x ∈ ys)

reflₚ : ∀ {xs : List A} → xs ↭ xs
reflₚ _ = Isomorphism.refl-⇔

symₚ : {xs ys : List A} → xs ↭ ys → ys ↭ xs
symₚ xs↭ys x = Isomorphism.sym-⇔ (xs↭ys x)

transₚ : {xs ys zs : List A} → xs ↭ ys → ys ↭ zs → xs ↭ zs
transₚ xs↭ys ys↭zs x = Isomorphism.trans-⇔ (xs↭ys x) (ys↭zs x)

consₚ : ∀ x {xs ys : List A} → xs ↭ ys → x ∷ xs ↭ x ∷ ys
consₚ _ xs↭ys _ .fun       (f0   , x≡x )    = f0 , x≡x
consₚ _ xs↭ys _ .fun       (fs n  , x∈xs)    = push (xs↭ys _ .fun (n , x∈xs))
consₚ _ xs↭ys _ .inv       (f0   , x≡x )    = f0 , x≡x
consₚ _ xs↭ys _ .inv       (fs n  , x∈xs)    = push (xs↭ys _ .inv (n , x∈xs))
consₚ _ xs↭ys _ .leftInv   (f0   , x≡x)     = refl
consₚ _ xs↭ys _ .leftInv   (fs n  , x∈xs) i  = push (xs↭ys _ .leftInv (n , x∈xs) i)
consₚ _ xs↭ys _ .rightInv  (f0   , x≡x)     = refl
consₚ _ xs↭ys _ .rightInv  (fs n  , x∈xs) i  = push (xs↭ys _ .rightInv (n , x∈xs) i)

swapₚ-to : ∀ (x₁ x₂ : A) xs → x₁ ∷ x₂ ∷ xs ↝ x₂ ∷ x₁ ∷ xs
swapₚ-to _ _ _ _ (f0 , x≡x₁) = fs f0 , x≡x₁
swapₚ-to _ _ _ _ (fs f0 , x≡x₂) = f0 , x≡x₂
swapₚ-to _ _ _ _ (fs (fs n) , x∈xs) = fs (fs n) , x∈xs

swapₚ-inv : ∀ (x₁ x₂ : A) xs x x∈xs → swapₚ-to x₂ x₁ xs x (swapₚ-to x₁ x₂ xs x x∈xs) ≡ x∈xs
swapₚ-inv _ _ _ _ (f0 , x≡x₁) = refl
swapₚ-inv _ _ _ _ (fs f0 , x≡x₂) = refl
swapₚ-inv _ _ _ _ (fs (fs n) , x∈xs) = refl

swapₚ : ∀ x₁ x₂ (xs : List A) → x₁ ∷ x₂ ∷ xs ↭ x₂ ∷ x₁ ∷ xs
swapₚ x₁ x₂ xs x .fun = swapₚ-to x₁ x₂ xs x
swapₚ x₁ x₂ xs x .inv = swapₚ-to x₂ x₁ xs x
swapₚ x₁ x₂ xs x .leftInv  = swapₚ-inv x₁ x₂ xs x
swapₚ x₁ x₂ xs x .rightInv = swapₚ-inv x₂ x₁ xs x

Fin-length : (xs : List A) → ∃ x × (x ∈ xs) ⇔ Fin (length xs)
Fin-length xs .inv n = xs ! n , n , refl
Fin-length xs .fun (x , n , p) = n
Fin-length xs .leftInv (x , n , p) i .fst = p i
Fin-length xs .leftInv (x , n , p) i .snd .fst = n
Fin-length xs .leftInv (x , n , p) i .snd .snd j = p (i ∧ j)
Fin-length xs .rightInv n = refl

Fin-length-cong : (xs ys : List A) →
                xs ↭ ys →
                Fin (length xs) ⇔ Fin (length ys)
Fin-length-cong xs ys xs↭ys =
  sym-⇔ (Fin-length xs) ⟨ trans-⇔ ⟩ iso-Σ xs↭ys ⟨ trans-⇔ ⟩ Fin-length ys

index-commutes : ∀ (x : A) xs ys →
                 (xs↭ys : xs ↭ ys) (x∈xs : x ∈ xs) →
                 fst (xs↭ys x .fun x∈xs) ≡ Fin-length-cong xs ys xs↭ys .fun (x∈xs .fst)
index-commutes x xs ys xs↭ys (n , p) =
  J (λ y y∈xs → xs↭ys y .fun (n , y∈xs) .fst ≡ xs↭ys (xs ! n) .fun (n , refl) .fst) refl p

index-equality-preserved : ∀ (x : A) xs ys (p q : x ∈ xs) →
                           (xs↭ys : xs ↭ ys) →
                           fst p ≡ fst q →
                           xs↭ys x .fun p .fst ≡ xs↭ys x .fun q .fst
index-equality-preserved x xs ys p q xs↭ys ip≡iq =
  xs↭ys x .fun p .fst ≡⟨ index-commutes x xs ys xs↭ys p ⟩
  Fin-length-cong xs ys xs↭ys .fun (p .fst) ≡⟨ cong (Fin-length-cong xs ys xs↭ys .fun) ip≡iq ⟩
  Fin-length-cong xs ys xs↭ys .fun (q .fst) ≡˘⟨ index-commutes x xs ys xs↭ys q ⟩
  xs↭ys x .fun q .fst ∎
  where open import Path.Reasoning

perm-inj : ∀ (x : A) xs ys n →
         (xs↭ys : x ∷ xs ↭ x ∷ ys) →
         ∀ z
         (z∈ys : x ≡ z)
         (x∈ys : x ≡ z)
         (z∈xs : xs ! n ≡ z)
         (p₁ : xs↭ys z .fun (fs n , z∈xs) ≡ (f0 , z∈ys))
         (p₂ : xs↭ys z .fun (f0 , z∈ys) ≡ (f0 , x∈ys)) →
         ⊥
perm-inj x xs ys n xs↭ys z z∈ys x∈ys z∈xs p₁ p₂ = znots (cong FinToℕ p₆)
  where
  open import Path.Reasoning

  p₃ = fs n , z∈xs ≡˘⟨ xs↭ys z .leftInv (fs n , z∈xs) ⟩
       xs↭ys z .inv (xs↭ys z .fun (fs n , z∈xs)) ≡⟨ cong (xs↭ys z .inv) p₁ ⟩
       xs↭ys z .inv (f0 , z∈ys) ∎

  p₄ = f0 , z∈ys ≡˘⟨ xs↭ys z .leftInv (f0 , z∈ys) ⟩
       xs↭ys z .inv (xs↭ys z .fun (f0 , z∈ys)) ≡⟨ cong (xs↭ys z .inv) p₂ ⟩
       xs↭ys z .inv (f0 , x∈ys) ∎

  p₅ = index-equality-preserved z (x ∷ ys) (x ∷ xs) (f0 , x∈ys) (f0 , z∈ys) (sym-⇔ ∘ xs↭ys) refl

  p₆ = f0 ≡⟨ cong fst p₄ ⟩
       xs↭ys z .inv (f0 , x∈ys) .fst ≡⟨ p₅ ⟩
       xs↭ys z .inv (f0 , z∈ys) .fst ≡˘⟨ cong fst p₃ ⟩
       fs n ∎

tailₚ-to : ∀ x (xs ys : List A) → x ∷ xs ↭ x ∷ ys → ∀ z → z ∈ xs → z ∈ ys
tailₚ-to x xs ys xs↭ys z (n , z∈xs) with xs↭ys z .fun (fs n , z∈xs) | inspect (xs↭ys z .fun) (fs n , z∈xs)
... | fs m , z∈ys | _ = m , z∈ys
... | f0 , z∈ys | 〖 p₁ 〗 with xs↭ys z .fun (f0 , z∈ys) | inspect (xs↭ys z .fun) (f0 , z∈ys)
... | fs o , x∈ys | _ = o , x∈ys
... | f0 , x∈ys | 〖 p₂ 〗 = ⊥-elim (perm-inj x xs ys n xs↭ys z z∈ys x∈ys z∈xs p₁ p₂)

pred-∈-eq : ∀ (x y : A) xs i j →
          (x∈xs₁ : xs ! i ≡ x) →
          (x∈xs₂ : xs ! j ≡ x) →
          Path (x ∈ y ∷ xs) (fs i , x∈xs₁) (fs j , x∈xs₂) →
          (i , x∈xs₁) ≡ (j , x∈xs₂)
pred-∈-eq x y xs i j x∈xs₁ x∈xs₂ =
  J (λ { (fs n , x∈xs₃) _ → (i , x∈xs₁) ≡ (n , x∈xs₃)
       ; (f0     , x∈xs₃) → ⊥-elim ∘ snotz ∘ cong FinToℕ ∘ cong fst })
  refl

open import Path.Reasoning

tailₚ-inv : ∀ x (xs ys : List A) →
            (xs↭ys : x ∷ xs ↭ x ∷ ys) →
            ∀ z (i : z ∈ ys) →
            tailₚ-to x xs ys xs↭ys z (tailₚ-to x ys xs (sym-⇔ ∘ xs↭ys) z i)  ≡ i
tailₚ-inv x xs ys xs↭ys z (n , z∈ys) with xs↭ys z .inv (fs n , z∈ys) | inspect (xs↭ys z .inv) (fs n , z∈ys)
... | fs m , z∈xs  | 〖 p₁ 〗 with xs↭ys z .fun (fs m , z∈xs) | inspect (xs↭ys z .fun) (fs m , z∈xs)
... | fs o , z∈ys₂ | 〖 p₂ 〗 = pred-∈-eq z x ys o n z∈ys₂ z∈ys p₃

  where p₃ = fs o , z∈ys₂ ≡˘⟨ p₂ ⟩
             xs↭ys z .fun (fs m , z∈xs) ≡˘⟨ cong (xs↭ys z .fun) p₁ ⟩
             xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ xs↭ys z .rightInv (fs n , z∈ys) ⟩
             fs n , z∈ys ∎

... | f0     , z∈ys₂ | 〖 p₂ 〗 with xs↭ys z .fun (f0 , z∈ys₂) | inspect (xs↭ys z .fun) (f0 , z∈ys₂)
... | f0     , x∈ys₃ | 〖 p₃ 〗 = ⊥-elim (perm-inj x xs ys m xs↭ys z z∈ys₂ x∈ys₃ z∈xs p₂ p₃)
... | fs o , x∈ys₃ | 〖 p₃ 〗 = ⊥-elim (snotz (cong (FinToℕ ∘ fst) p₄))

  where p₄ = fs n , z∈ys ≡˘⟨ xs↭ys z .rightInv (fs n , z∈ys) ⟩
             xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ cong (xs↭ys z .fun) p₁ ⟩
             xs↭ys z .fun (fs m , z∈xs) ≡⟨ p₂ ⟩
             f0 , z∈ys₂ ∎

tailₚ-inv x xs ys xs↭ys z (n , z∈ys) | f0 , z∈xs | 〖 p₁ 〗
  with xs↭ys z .inv (f0 , z∈xs) | inspect (xs↭ys z .inv) (f0 , z∈xs)
... | f0     , z∈ys₂ | 〖 p₂ 〗 = ⊥-elim (perm-inj x ys xs n (sym-⇔ ∘ xs↭ys) z z∈xs z∈ys₂ z∈ys p₁ p₂)
... | fs o , z∈ys₂ | 〖 p₂ 〗 with xs↭ys z .fun (fs o , z∈ys₂) | inspect (xs↭ys z .fun) (fs o , z∈ys₂)
... | fs m , z∈ys₃ | 〖 p₃ 〗 = ⊥-elim (snotz (cong (FinToℕ ∘ fst) p₄))

  where p₄ = fs m , z∈ys₃ ≡˘⟨ p₃ ⟩
             xs↭ys z .fun (fs o , z∈ys₂) ≡˘⟨ cong (xs↭ys z .fun) p₂ ⟩
             xs↭ys z .fun (xs↭ys z .inv (f0 , z∈xs)) ≡⟨ xs↭ys z .rightInv (f0 , z∈xs) ⟩
             f0 , z∈xs ∎

... | f0     , z∈ys₃ | 〖 p₃ 〗 with xs↭ys z .fun (f0 , z∈ys₃) | inspect (xs↭ys z .fun) (f0 , z∈ys₃)
... | f0     , z∈ys₄ | 〖 p₄ 〗 = ⊥-elim (perm-inj x xs ys o xs↭ys z z∈ys₃ z∈ys₄ z∈ys₂ p₃ p₄)
... | fs l , z∈ys₄ | 〖 p₄ 〗 = pred-∈-eq z x ys l n z∈ys₄ z∈ys p₇
  where

  p₅ : Path (z ∈ x ∷ ys) (f0 , z∈xs) (f0 , z∈ys₃)
  p₅ = (f0 , z∈xs) ≡˘⟨ xs↭ys z .rightInv (f0 , z∈xs) ⟩
       xs↭ys z .fun (xs↭ys z .inv (f0 , z∈xs)) ≡⟨ cong (xs↭ys z .fun) p₂ ⟩
       xs↭ys z .fun (fs o , z∈ys₂) ≡⟨ p₃ ⟩
       (f0 , z∈ys₃) ∎

  p₆ = z∈xs ≡˘⟨ isSet-subst {B = λ n → (x ∷ ys) ! n ≡ z} (Discrete→isSet discreteFin) (cong fst p₅) z∈xs ⟩
       subst (λ n → (x ∷ ys) ! n ≡ z) (cong fst p₅) z∈xs
     ≡⟨ PathΣ→ΣPathTransport (f0 , z∈xs) (f0 , z∈ys₃) p₅ .snd ⟩
       z∈ys₃ ∎

  p₇ = fs l , z∈ys₄ ≡˘⟨ p₄ ⟩
       xs↭ys z .fun (f0 , z∈ys₃) ≡˘⟨ cong (xs↭ys z .fun ∘ _,_ f0) p₆ ⟩
       xs↭ys z .fun (f0 , z∈xs) ≡˘⟨ cong (xs↭ys z .fun) p₁ ⟩
       xs↭ys z .fun (xs↭ys z .inv (fs n , z∈ys)) ≡⟨ xs↭ys z .rightInv (fs n , z∈ys) ⟩
       fs n , z∈ys ∎

tailₚ : ∀ x (xs ys : List A) →
        x ∷ xs ↭ x ∷ ys →
        xs ↭ ys
tailₚ x xs ys x∷xs↭x∷ys k .fun = tailₚ-to x xs ys x∷xs↭x∷ys k
tailₚ x xs ys x∷xs↭x∷ys k .inv = tailₚ-to x ys xs (sym-⇔ ∘ x∷xs↭x∷ys) k
tailₚ x xs ys x∷xs↭x∷ys k .rightInv = tailₚ-inv x xs ys x∷xs↭x∷ys k
tailₚ x xs ys x∷xs↭x∷ys k .leftInv  v = cong (λ z → tailₚ-to x ys xs (sym-⇔ ∘ x∷xs↭x∷ys) k (tailₚ-to x xs ys z k v)) (funExt (λ h → sym (sym-sym-iso (x∷xs↭x∷ys h)) ))  ; tailₚ-inv x ys xs (sym-⇔ ∘ x∷xs↭x∷ys) k v

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module ImportTests.ExtractFunction where

open import ExtractFunction
open import Data.Nat
open import Data.Bool
checkFunction1 : ℕ
checkFunction1 = function1 2 3

checkFunction2 : ℕ
checkFunction2 = function2 4 true


text:
@0 F : @0 Set → Set
F A = λ { → A }

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module Cubical.HITs.FreeComMonoids.Base where

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

private variable
  ℓ : Level
  A : Type ℓ

data FreeComMonoid (A : Type ℓ) : Type ℓ where
  ⟦_⟧       : A → FreeComMonoid A
  ε         : FreeComMonoid A
  _·_       : FreeComMonoid A → FreeComMonoid A → FreeComMonoid A
  comm      : ∀ x y   → x · y ≡ y · x
  identityᵣ : ∀ x     → x · ε ≡ x
  identityₗ : ∀ x     → ε · x ≡ x
  assoc     : ∀ x y z → x · (y · z) ≡ (x · y) · z
  trunc     : isSet (FreeComMonoid A)

module Elim {ℓ'} {B : FreeComMonoid A → Type ℓ'}
  (⟦_⟧*       : (x : A) → B ⟦ x ⟧)
  (ε*         : B ε)
  (_·*_       : ∀ {x y}   → B x → B y → B (x · y))
  (comm*      : ∀ {x y}   → (xs : B x) (ys : B y)
    → PathP (λ i → B (comm x y i)) (xs ·* ys) (ys ·* xs))
  (identityᵣ* : ∀ {x}     → (xs : B x)
    → PathP (λ i → B (identityᵣ x i)) (xs ·* ε*) xs)
  (identityₗ* : ∀ {x}     → (xs : B x)
    → PathP (λ i → B (identityₗ x i)) (ε* ·* xs) xs)
  (assoc*     : ∀ {x y z} → (xs : B x) (ys : B y) (zs : B z)
    → PathP (λ i → B (assoc x y z i)) (xs ·* (ys ·* zs)) ((xs ·* ys) ·* zs))
  (trunc*     : ∀ xs → isSet (B xs)) where

  f : (xs : FreeComMonoid A) → B xs
  f ⟦ x ⟧ = ⟦ x ⟧*
  f ε = ε*
  f (xs · ys) = f xs ·* f ys
  f (comm xs ys i) = comm* (f xs) (f ys) i
  f (identityᵣ xs i) = identityᵣ* (f xs) i
  f (identityₗ xs i) = identityₗ* (f xs) i
  f (assoc xs ys zs i) = assoc* (f xs) (f ys) (f zs) 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 : FreeComMonoid A → Type ℓ'}
  (BProp : {xs : FreeComMonoid A} → isProp (B xs))
  (⟦_⟧*       : (x : A) → B ⟦ x ⟧)
  (ε*         : B ε)
  (_·*_       : ∀ {x y}   → B x → B y → B (x · y)) where

  f : (xs : FreeComMonoid A) → B xs
  f = Elim.f ⟦_⟧* ε* _·*_
    (λ {x y} xs ys → toPathP (BProp (transport (λ i → B (comm x y i)) (xs ·* ys)) (ys ·* xs)))
    (λ {x} xs → toPathP (BProp (transport (λ i → B (identityᵣ x i)) (xs ·* ε*)) xs))
    (λ {x} xs → toPathP (BProp (transport (λ i → B (identityₗ x i)) (ε* ·* xs)) xs))
    (λ {x y z} xs ys zs → toPathP (BProp (transport (λ i → B (assoc x y z i)) (xs ·* (ys ·* zs))) ((xs ·* ys) ·* zs)))
    (λ _ → (isProp→isSet BProp))

module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B)
  (⟦_⟧*       : (x : A) → B)
  (ε*         : B)
  (_·*_       : B → B → B)
  (comm*      : (x y : B) → x ·* y ≡ y ·* x)
  (identityᵣ* : (x : B) → x ·* ε* ≡ x)
  (identityₗ* : (x : B) → ε* ·* x ≡ x)
  (assoc*     : (x y z : B) → x ·* (y ·* z) ≡ (x ·* y) ·* z)
  where

  f : FreeComMonoid A → B
  f = Elim.f ⟦_⟧* ε* _·*_ comm* identityᵣ* identityₗ* assoc* (const BType)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
--{-# OPTIONS --allow-unsolved-metas #-}
module Theorem1 where

open import OscarPrelude

open import HasSatisfaction
open import HasSubstantiveDischarge

open import LiteralFormula

open import 𝑱udgement
open import HasSalvation

open import Membership

open import Interpretation
open import HasNegation

open import IsLiteralFormula

Theorem1 : (Φ : 𝑱udgement LiteralFormula) → ⊨ Φ ↔ ▷ Φ
Theorem1 Φ@(χs ⊢ ι) = Theorem1a , Theorem1b where
  Theorem1a : ⊨ Φ → ▷ Φ
  Theorem1a ⊨Φ with ▷? Φ
  … | yes ▷Φ = ▷Φ
  … | no ⋫Φ =
    let I , I⊨χs , I⊭ι = Lemma1a in
      ⊥-elim ∘ I⊭ι $ ⊨Φ I I⊨χs
    where
    Lemma1a : ∃ λ I → I ⊨ χs × I ⊭ ι
    Lemma1a = {!!}

{-
To construct the interpretation, consider a unique list, τ₀, τ₁, …, τₙ, of terms in ι ∷ χs. For each term, τ, we find <TODO> interpretations, 𝓘, such that for any I ∈ 𝓘, and any i ∈ 0, …, n, τ⟦ I ⟧ τᵢ = i. For each formula φ ∈ ι ∷ χs, we find <TODO> an interpretation I ∈ 𝓘 such that 𝑃⟦ I ⟧ φ = true when φ ∈ χs and 𝑃⟦ I ⟧ φ = false when φ = ι.
For all terms in ι ∷ χs, find a coding into Nat that uniquely determines each term. To do this, compute the maximum functional depth of terms, D, the maximal arity of terms, A, the maximal function name, F, and the maximal variable name, V. Each term can then be coded into Fin V + (D₀ = F + F * V + F * V ^ 2 + ... + F * V ^ A) + (D₀ ...
Encode each term in a discrimination network. Each new term stored is assigned a unique id
-}

  Theorem1b : ▷ Φ → ⊨ Φ
  Theorem1b (left ◁χs) I I⊨χs = {!!}
  Theorem1b (right χs≽ι) I I⊨χs = {!!}


text:
-- Andreas, 2011-04-15
module NotStronglyRigidOccurrence where

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

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

-- Jason C. Read, PhD thesis, p. 109
test : (k : Nat) ->
       let X : (Nat -> Nat) -> Nat
           X = _
       in (f : Nat -> Nat) -> X f ≡ suc (f (X (\ x -> k)))
test k f = refl -- {a = suc (f (suc k))}
-- leads to _30 : _22 k f ≡ suc (f (_22 k (λ x → k)))
-- this should give yellow, because above solution for _22 exists

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --rewriting #-}
module Oscar.AgdaRewriting where

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

record ⊤ : Set where
  constructor tt

data List (A : Set) : Set where
  ∅ : List A
  _∷_ : A → List A → List A

Nat = List ⊤
pattern ‼ xs = tt ∷ xs
syntax ‼ xs = ! xs

open import Agda.Builtin.Nat using (zero; suc) renaming (Nat to ℕ; _+_ to _+ℕ_)

toNat : ℕ → Nat
toNat zero = ∅
toNat (suc x) = tt ∷ toNat x

toℕ : Nat → ℕ
toℕ ∅ = zero
toℕ (x ∷ x₁) = suc (toℕ x₁)

ℕ-iso : ∀ n → toℕ (toNat n) ≡ n
ℕ-iso zero = refl
ℕ-iso (suc n) rewrite ℕ-iso n = refl

Nat-iso : ∀ n → toNat (toℕ n) ≡ n
Nat-iso ∅ = refl
Nat-iso (x ∷ n) rewrite Nat-iso n = refl

--{-# REWRITE ℕ-iso #-}

infixl 6 _+Nat_
_+Nat_ : Nat → Nat → Nat
m +Nat n = toNat (toℕ m +ℕ toℕ n)

infixl 7 _*Nat_
_*Nat_ : Nat → Nat → Nat
∅ *Nat _ = ∅
_ *Nat ∅ = ∅
(_ ∷ m) *Nat (_ ∷ n) = _ ∷ m +Nat n +Nat m *Nat n

NatComputation : Nat
NatComputation = toNat 5 *Nat toNat 7

butnowinℕ : ℕ
butnowinℕ = toℕ NatComputation

showme : ℕ
showme = {!!}

-- postulate
--   Nat≡ℕ : Nat ≡ ℕ

-- {-# REWRITE Nat≡ℕ #-}

-- data Fin : Nat → Set where
--   ∅ : ∀ {n} → Fin (! n)
--   ! : ∀ {n} → Fin n → Fin (! n)

-- -- record ⊤ : Set where
-- --   constructor tt

-- -- data List (A : Set) : Set where
-- --   ∅ : List A
-- --   _∷_ : A → List A → List A

-- -- Nat = List ⊤
-- -- pattern ‼ xs = tt ∷ xs

-- -- data Fin : Nat → Set where
-- --   ∅ : ∀ {n} → Fin (‼ n)
-- --   ! : ∀ {n} → Fin n → Fin (‼ n)


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

open import Algebra

module Data.FingerTree.Reasoning
  {r m}
  (ℳ : Monoid r m)
  where

open Monoid ℳ renaming (Carrier to 𝓡)

open import Data.FingerTree.MonoidSolver ℳ using (solve-macro)

open import Data.Unit using (⊤)
open import Reflection using (TC; Term)

macro
  _↯ : Term → Term → TC ⊤
  _↯ = solve-macro

infixr 2 ∙≫_ ≪∙_
∙≫_ : ∀ {x y z} → x ≈ y → z ∙ x ≈ z ∙ y
∙≫_ = ∙-cong refl

≪∙_ : ∀ {x y z} → x ≈ y → x ∙ z ≈ y ∙ z
≪∙ x = ∙-cong x refl

infixl 1 _⍮_
_⍮_ : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
_⍮_ = trans

infixl 1 trans⁻¹
trans⁻¹ : ∀ {x y z : 𝓡} → y ≈ z → x ≈ y → x ≈ z
trans⁻¹ x y = trans y x

syntax trans⁻¹ y≈z x≈y = x≈y ⍮′ y≈z

infixr 2 _↢_ ↣-syntax ↣↣-syntax
_↢_ : ∀ x {y} → x ≈ y → x ≈ y
_ ↢ x≈y = x≈y

↣-syntax : ∀ {x} y → x ≈ y → x ≈ y
↣-syntax _ x≈y = x≈y

syntax ↣-syntax y x≈y = x≈y ↣ y

↣↣-syntax : ∀ x y → x ≈ y → x ≈ y
↣↣-syntax _ _ x≈y = x≈y

syntax ↣↣-syntax x y x≈y = x ↣⟨ x≈y ⟩↣ y

infixl 6 _∙>_ _<∙_
_∙>_ : ∀ x {y z} → y ≈ z → x ∙ y ≈ x ∙ z
_ ∙> y≈z = ∙≫ y≈z

_<∙_ : ∀ {x y} → x ≈ y → ∀ z → x ∙ z ≈ y ∙ z
x≈y <∙ _ = ≪∙ x≈y

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
module BBHeap.Perfect {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_

data Perfect {b : Bound} : BBHeap b → Set where
  plf : Perfect (leaf {b})
  pnd : {x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋘r : l ⋘ r) → l ≃ r → Perfect (left b≤x l⋘r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue478 where

record Ko (Q : Set) : Set₁ where
 field
  T : Set

module Bo (P : Set) (ko : Ko P) where
  open Ko ko

  err : T
  err = Set

{- The error message was:
  Set₁ !=< T P ko of type Set₂
  when checking that the expression Set has type T P ko

  We now get the desired error message:

  Set₁ !=< T of type Set₂
  when checking that the expression Set has type T

-}

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


text:
{-# OPTIONS --cubical --safe #-}
module Ag08 where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything
open import Cubical.Data.Everything

-- maybe helpful when case splitting
record Reveal_·_is_ {a b} {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (ℓ-max a b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

-- Lift is necessary for Bool and Bool ≡ Bool are of different level. :-P
Bool≡[Bool≡Bool] : Lift Bool ≡ (Bool ≡ Bool)
Bool≡[Bool≡Bool] = {!!}

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
{-# OPTIONS --without-K #-}
open import Data.Nat
open import Data.Two
open import Data.Zero
open import Data.Fin.NP
open import Type
open import Function
open import Relation.Binary.PropositionalEquality.NP

import Explore.Universe.Base
open import Explore.Core
open import Explore.Zero
open import Explore.One
open import Explore.Two
open import Explore.Universe.Type

-- Exploring Fin comes in two flavors Regular & Custom
-- We recommend Regular if you want to work for arbitrary values of n.
-- We recommend Custom if you want to work for particular values of n (2, 6...).
module Explore.Fin where

module Regular n = Explore.Universe.Base (≃ᵁ (Finᵁ n) (Fin n) (Finᵁ≃Fin n))

module Custom where
  module _ n where
    open Explore.Universe.Base (≃ᵁ (Finᵁ' n) (Fin n) (Finᵁ'≃Fin n))
      public

  Finᵉ0-𝟘ᵉ : (λ {M : ★₀} (ε : M) op f → explore 0 ε op (f ∘ Fin▹𝟘)) ≡ 𝟘ᵉ
  Finᵉ0-𝟘ᵉ = refl

  Finᵉ1-𝟙ᵉ : (λ {M : ★₀} (ε : M) op f → explore 1 ε op (f ∘ Fin▹𝟙)) ≡ 𝟙ᵉ
  Finᵉ1-𝟙ᵉ = refl

  Finᵉ2-𝟚ᵉ : (λ {M : ★₀} (ε : M) op f → explore 2 ε op (f ∘ Fin▹𝟚)) ≡ 𝟚ᵉ
  Finᵉ2-𝟚ᵉ = refl

module ByHand {ℓ} where
  Finᵉ' : ∀ n → Explore ℓ (Fin n)
  Finᵉ' zero    z _⊕_ f = z
  Finᵉ' (suc n) z _⊕_ f = f zero ⊕ Finᵉ' n z _⊕_ (f ∘ suc)

  -- Finᵉ and Finᵉ' are extensionally equal.
  -- Moreover the simplicity of the proof shows that the two functions are computing
  -- in the same way.
  Finᵉ-Finᵉ' : ∀ n {M} (ε : M) (_⊕_ : M → M → M) (f : Fin n → M) → Regular.explore n ε _⊕_ f ≡ Finᵉ' n ε _⊕_ f
  Finᵉ-Finᵉ' zero    ε _⊕_ f = idp
  Finᵉ-Finᵉ' (suc n) ε _⊕_ f = ap (_⊕_ (f zero))
                                  (Finᵉ-Finᵉ' n ε _⊕_ (f ∘ suc))

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore