text:
------------------------------------------------------------------------
-- Lemmas about the initial bag index
------------------------------------------------------------------------

module TotalParserCombinators.InitialBag where

open import Category.Monad
open import Data.List
import Data.List.Categorical
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties as M
  hiding (⊛-∈↔)
open import Data.List.Relation.Binary.BagAndSetEquality
  using () renaming (_∼[_]_ to _List-∼[_]_)
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.Any.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Product
open import Data.Sum
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_)
import Function.Related as Related
open import Level
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl)
open import Relation.Binary.HeterogeneousEquality as H
  using (refl) renaming (_≅_ to _≅′_)

open Inv.Inverse
open RawMonadPlus {f = zero} Data.List.Categorical.monadPlus
  using () renaming (_⊛_ to _⊛′_)
open Related using (SK-sym)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics

------------------------------------------------------------------------
-- Optimisation

private

  abstract

    ⊛-∈↔ : ∀ {A B : Set} (fs : List (A → B)) {xs y} →
           (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ (fs ⊛′ xs)
    ⊛-∈↔ = M.⊛-∈↔

------------------------------------------------------------------------
-- Sanity check: The initial set index is correctly defined

mutual

  complete : ∀ {Tok R xs x} {p : Parser Tok R xs} →
             x ∈ p · [] → x ∈ xs
  complete x∈p = complete′ x∈p refl

  private

    complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
                x ∈ p · s → s ≡ [] → x ∈ xs
    complete′ return                                                    refl = to return↔            ⟨$⟩ refl
    complete′ (∣-left      x∈p₁)                                        refl = to ++↔                ⟨$⟩ inj₁ (complete x∈p₁)
    complete′ (∣-right xs₁ x∈p₂)                                        refl = to (++↔ {P = _≡_ _}
                                                                                {xs = xs₁})   ⟨$⟩ inj₂ (complete x∈p₂)
    complete′ (<$> x∈p)                                                 refl = to (map-∈↔ _)         ⟨$⟩ (_ , complete x∈p , refl)
    complete′ (_⊛_   {s₁ = []} {xs = just _}                f∈p₁ x∈p₂)  refl = to (⊛-∈↔ _)           ⟨$⟩ (_ , _ , complete f∈p₁
                                                                                , complete x∈p₂ , refl)
    complete′ (_>>=_ {s₁ = []} {xs = just xs} {f = just _}  x∈p₁ y∈p₂x) refl = to (>>=-∈↔ {xs = xs}) ⟨$⟩ (_ , complete x∈p₁
                                                                                , complete y∈p₂x)
    complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p)                            refl = to xs₁≈xs₂            ⟨$⟩ complete x∈p

    complete′ (_⊛_   {s₁ = []} {xs = nothing}               f∈p₁ x∈p₂)  refl with complete x∈p₂
    ... | ()
    complete′ (_>>=_ {s₁ = []} {xs = nothing}               x∈p₁ y∈p₂x) refl with complete x∈p₁
    ... | ()
    complete′ (_>>=_ {s₁ = []} {xs = just _}  {f = nothing} x∈p₁ y∈p₂x) refl with complete y∈p₂x
    ... | ()

    complete′ token                     ()
    complete′ (_⊛_    {s₁ = _ ∷ _} _ _) ()
    complete′ (_>>=_  {s₁ = _ ∷ _} _ _) ()
    complete′ (nonempty _)              ()

mutual

  sound : ∀ {Tok R xs x} (p : Parser Tok R xs) →
          x ∈ xs → x ∈ p · []
  sound (return x)              (here refl) = return
  sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs with from (++↔ {P = _≡_ _} {xs = xs₁}) ⟨$⟩ x∈xs
  ... | inj₁ x∈xs₁ = ∣-left      (sound p₁ x∈xs₁)
  ... | inj₂ x∈xs₂ = ∣-right xs₁ (sound p₂ x∈xs₂)
  sound (f <$> p) x∈xs with from (map-∈↔ f) ⟨$⟩ x∈xs
  ... | (y , y∈xs , refl) = <$> sound p y∈xs
  sound (_⊛_ {fs = fs} {just xs} p₁ p₂) y∈ys
    with from (⊛-∈↔ (flatten fs) {xs = xs}) ⟨$⟩ y∈ys
  sound (_⊛_ {fs = nothing} {just xs} p₁ p₂)  y∈ys | (f′ , x′ , ()    , x′∈xs , refl)
  sound (_⊛_ {fs = just fs} {just xs} p₁ p₂)  y∈ys | (f′ , x′ , f′∈fs , x′∈xs , refl) =
    _⊛_ {fs = ○} {xs = ○} (sound p₁ f′∈fs) (sound p₂ x′∈xs)
  sound (_>>=_ {xs = zs} {f = just f} p₁ p₂) y∈ys
    with from (>>=-∈↔ {xs = flatten zs} {f = f}) ⟨$⟩ y∈ys
  ... | (x , x∈zs , y∈fx) =
    _>>=_ {xs = zs} {f = just f} (sound p₁ x∈zs) (sound′ (p₂ x) x∈zs y∈fx)
  sound (cast xs₁≈xs₂ p) x∈xs = cast (sound p (from xs₁≈xs₂ ⟨$⟩ x∈xs))

  sound (return _)                 (there ())
  sound fail                       ()
  sound token                      ()
  sound (_⊛_   {xs = nothing} _ _) ()
  sound (_>>=_ {f  = nothing} _ _) ()
  sound (nonempty _)               ()

  private

    sound′ : ∀ {Tok R₁ R₂ x y xs} {zs : Maybe (List R₁)}
               (p : ∞⟨ zs ⟩Parser Tok R₂ xs) →
               x ∈ flatten zs → y ∈ xs → y ∈ ♭? p · []
    sound′ {zs = just _}  p _  = sound p
    sound′ {zs = nothing} p ()

mutual

  sound∘complete : ∀ {Tok R xs x} {p : Parser Tok R xs}
                   (x∈p : x ∈ p · []) →
                   sound p (complete x∈p) ≡ x∈p
  sound∘complete x∈p = H.≅-to-≡ (sound∘complete′ x∈p refl)

  private

    sound∘complete′ : ∀ {Tok R xs x s} {p : Parser Tok R xs}
                      (x∈p : x ∈ p · s) (s≡[] : s ≡ []) →
                      sound p (complete′ x∈p s≡[]) ≅′ x∈p
    sound∘complete′ return                                refl = refl
    sound∘complete′ (∣-left {xs₁ = xs₁} {xs₂ = xs₂} x∈p₁) refl
      rewrite left-inverse-of (++↔ {P = _≡_ _} {xs = xs₁} {ys = xs₂}) (inj₁ (complete x∈p₁)) =
        H.cong _∈_·_.∣-left (sound∘complete′ x∈p₁ refl)
    sound∘complete′ (∣-right xs₁ x∈p₂) refl
      rewrite left-inverse-of (++↔ {P = _≡_ _} {xs = xs₁}) (inj₂ (complete x∈p₂)) =
        H.cong (_∈_·_.∣-right xs₁) (sound∘complete′ x∈p₂ refl)
    sound∘complete′ (<$>_ {f = f} x∈p) refl
      rewrite left-inverse-of (map-∈↔ f) (_ , complete x∈p , refl) =
        H.cong _∈_·_.<$>_ (sound∘complete′ x∈p refl)
    sound∘complete′ (_⊛_ {s₁ = []} {fs = fs} {xs = just xs} f∈p₁ x∈p₂) refl
      with complete f∈p₁ | complete x∈p₂
      | from inv ⟨$⟩ (to inv ⟨$⟩ (_ , _ , complete f∈p₁ , complete x∈p₂ , refl))
      | left-inverse-of inv (_ , _ , complete f∈p₁ , complete x∈p₂ , refl)
      | sound∘complete f∈p₁ | sound∘complete x∈p₂
      where inv = ⊛-∈↔ (flatten fs) {xs = xs}
    sound∘complete′ (_⊛_ {s₁ = []} {fs = nothing} {xs = just xs} _ _) refl | () | _ | _ | _ | _ | _
    sound∘complete′ (_⊛_ {s₁ = []} {fs = just fs} {xs = just xs} {p₁ = p₁} {p₂ = p₂}
                         .(sound p₁ ∈fs) .(sound p₂ ∈xs)) refl
      | ∈fs | ∈xs | ._ | refl | refl | refl = refl
    sound∘complete′ (_>>=_ {x = x} {y = y} {s₁ = []} {xs = just _} {f = just f} {p₁ = p₁} {p₂ = p₂} x∈p₁ y∈p₂x) refl
      rewrite left-inverse-of (>>=-∈↔ {f = f}) (_ , complete x∈p₁ , complete y∈p₂x)
         with sound p₁ (complete x∈p₁)
            | sound∘complete x∈p₁
            | sound′ (p₂ x) (complete x∈p₁) (complete y∈p₂x)
            | helper (p₂ x) (complete x∈p₁) y∈p₂x
         where
         helper : ∀ {Tok R₁ R₂ x y ys} {xs : Maybe (List R₁)}
                  (p : ∞⟨ xs ⟩Parser Tok R₂ ys) →
                  (x∈xs : x ∈ flatten xs) (y∈p : y ∈ ♭? p · []) →
                  sound′ p x∈xs (complete y∈p) ≡ y∈p
         helper {xs = nothing} p () _
         helper {xs = just _}  p _  y∈p = sound∘complete y∈p
    ... | ._ | refl | ._ | refl = refl
    sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} x∈p)             refl with complete x∈p | sound∘complete x∈p
    sound∘complete′ (cast {xs₁≈xs₂ = xs₁≈xs₂} .(sound _ x∈xs)) refl | x∈xs | refl
      rewrite left-inverse-of xs₁≈xs₂ x∈xs = refl

    sound∘complete′ (_⊛_    {s₁ = []} {xs = nothing}              _    x∈p₂)  refl with complete x∈p₂
    ... | ()
    sound∘complete′ (_>>=_  {s₁ = []} {xs = nothing}              x∈p₁ y∈p₂x) refl with complete x∈p₁
    ... | ()
    sound∘complete′ (_>>=_  {s₁ = []} {xs = just _} {f = nothing} x∈p₁ y∈p₂x) refl with complete y∈p₂x
    ... | ()

    sound∘complete′ token                     ()
    sound∘complete′ (_⊛_    {s₁ = _ ∷ _} _ _) ()
    sound∘complete′ (_>>=_  {s₁ = _ ∷ _} _ _) ()
    sound∘complete′ (nonempty _)              ()

complete∘sound : ∀ {Tok R xs x}
                 (p : Parser Tok R xs) (x∈p : x ∈ xs) →
                 complete (sound p x∈p) ≡ x∈p
complete∘sound (return x)              (here refl) = refl
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) x∈xs
  with from             (++↔ {P = _≡_ _} {xs = xs₁}) ⟨$⟩ x∈xs
     | right-inverse-of (++↔ {P = _≡_ _} {xs = xs₁})     x∈xs
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to ++↔                          ⟨$⟩ inj₁ x∈xs₁) | inj₁ x∈xs₁ | refl =
  P.cong (_⟨$⟩_ (to ++↔)                          ∘ inj₁) $ complete∘sound p₁ x∈xs₁
complete∘sound (_∣_ {xs₁ = xs₁} p₁ p₂) .(to (++↔ {P = _≡_ _} {xs = xs₁}) ⟨$⟩ inj₂ x∈xs₂) | inj₂ x∈xs₂ | refl =
  P.cong (_⟨$⟩_ (to (++↔ {P = _≡_ _} {xs = xs₁})) ∘ inj₂) $ complete∘sound p₂ x∈xs₂
complete∘sound (f <$> p) x∈xs
  with             from (map-∈↔ f) ⟨$⟩ x∈xs
     | right-inverse-of (map-∈↔ f)     x∈xs
complete∘sound (f <$> p) .(to (map-∈↔ f) ⟨$⟩ (y , y∈xs , refl)) | (y , y∈xs , refl) | refl =
  P.cong (λ y∈ → to (map-∈↔ _) ⟨$⟩ (y , y∈ , refl))
         (complete∘sound p y∈xs)
complete∘sound (_⊛_ {fs = fs} {just xs} p₁ p₂) y∈ys
  with from             (⊛-∈↔ (flatten fs) {xs = xs}) ⟨$⟩ y∈ys
     | right-inverse-of (⊛-∈↔ (flatten fs) {xs = xs})     y∈ys
complete∘sound (_⊛_ {fs = nothing} {xs = just xs} p₁ p₂)
               y∈ys                                                | (f′ , x′ , ()    , x′∈xs , refl) | _
complete∘sound (_⊛_ {fs = just fs} {xs = just xs} p₁ p₂)
               .(to (⊛-∈↔ _) ⟨$⟩ (f′ , x′ , f′∈fs , x′∈xs , refl)) | (f′ , x′ , f′∈fs , x′∈xs , refl) | refl =
  P.cong₂ (λ f′∈ x′∈ → to (⊛-∈↔ _) ⟨$⟩ (f′ , x′ , f′∈ , x′∈ , refl))
          (complete∘sound p₁ f′∈fs)
          (complete∘sound p₂ x′∈xs)
complete∘sound (_>>=_ {xs = zs}      {just f} p₁ p₂) y∈ys
  with from             (>>=-∈↔ {xs = flatten zs} {f = f}) ⟨$⟩ y∈ys
     | right-inverse-of (>>=-∈↔ {xs = flatten zs} {f = f})     y∈ys
complete∘sound (_>>=_ {xs = nothing} {just f} p₁ p₂) ._                                           | (x , ()   , y∈fx) | refl
complete∘sound (_>>=_ {xs = just zs} {just f} p₁ p₂) .(to (>>=-∈↔ {f = f}) ⟨$⟩ (x , x∈zs , y∈fx)) | (x , x∈zs , y∈fx) | refl =
  P.cong₂ (λ x∈ y∈ → to (>>=-∈↔ {f = f}) ⟨$⟩ (x , x∈ , y∈))
          (complete∘sound p₁ x∈zs)
          (complete∘sound (p₂ x) y∈fx)
complete∘sound (cast xs₁≈xs₂ p) x∈xs
  rewrite complete∘sound p (from xs₁≈xs₂ ⟨$⟩ x∈xs) =
    right-inverse-of xs₁≈xs₂ x∈xs

complete∘sound (return _)                 (there ())
complete∘sound fail                       ()
complete∘sound token                      ()
complete∘sound (_⊛_   {xs = nothing} _ _) ()
complete∘sound (_>>=_ {f  = nothing} _ _) ()
complete∘sound (nonempty _)               ()

correct : ∀ {Tok R xs x} {p : Parser Tok R xs} → x ∈ p · [] ↔ x ∈ xs
correct {p = p} = record
  { to         = P.→-to-⟶ complete
  ; from       = P.→-to-⟶ $ sound p
  ; inverse-of = record
    { left-inverse-of  = sound∘complete
    ; right-inverse-of = complete∘sound p
    }
  }

------------------------------------------------------------------------
-- Equal parsers have equal initial bags/sets

-- Note that this property holds also for the subbag and subset
-- relations.

cong : ∀ {k Tok R xs₁ xs₂}
         {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂} →
       p₁ ∼[ k ] p₂ → initial-bag p₁ List-∼[ k ] initial-bag p₂
cong {xs₁ = xs₁} {xs₂} {p₁} {p₂} p₁≈p₂ {x} =
  (x ∈ xs₁)    ↔⟨ SK-sym correct ⟩
  x ∈ p₁ · []  ∼⟨ p₁≈p₂ ⟩
  x ∈ p₂ · []  ↔⟨ correct ⟩
  (x ∈ xs₂)    ∎
  where open Related.EquationalReasoning

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
-- 2012-03-16 Andreas, fixing shift/reduce conflict introduced by record update
module Issue549 where

record M.R { A } : Set where
-- gives: Not a valid identifier M.R

-- If you remove the A, you get: Not a valid pattern
-- since then it is parsed as a record update expression

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Spire.Type
module Spire.Denotational where

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

data Term : Set → Set₁
eval : {A : Set} → Term A → A

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

data Term where
  {- Type introduction -}
  `⊥ `⊤ `Bool `ℕ `Desc `Type : ∀{ℓ} → Term (Type ℓ)
  `Π `Σ : ∀{ℓ}
    (A : Term (Type ℓ))
    (B : ⟦ ℓ ∣ eval A ⟧ → Term (Type ℓ))
    → Term (Type ℓ)
  `⟦_⟧ : ∀{ℓ}
    (A : Term (Type ℓ))
    → Term (Type (suc ℓ))
  `⟦_⟧ᵈ : ∀{ℓ}
    (D : Term (Desc ℓ))
    (X : Term (Type ℓ))
    → Term (Type ℓ)
  `μ : ∀{ℓ}
    (D : Term (Desc ℓ))
    → Term (Type ℓ)

  {- Type elimination -}
  `elimType : ∀{ℓ}
    (P : (n : ℕ) → Type n → Term (Type ℓ))
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `⊥) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `⊤) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `Bool) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `ℕ) ⟧)
    → ((n : ℕ) (A : Type n) (B : ⟦ n ∣ A ⟧ → Type n)
       (rec₁ : ⟦ ℓ ∣ eval (P n A) ⟧)
       (rec₂ : (a : ⟦ n ∣ A ⟧) → ⟦ ℓ ∣ eval (P n (B a)) ⟧)
       → Term ⟦ ℓ ∣ eval (P n (`Π A B)) ⟧)
    → ((n : ℕ) (A : Type n) (B : ⟦ n ∣ A ⟧ → Type n)
       (rec₁ : ⟦ ℓ ∣ eval (P n A) ⟧)
       (rec₂ : (a : ⟦ n ∣ A ⟧) → ⟦ ℓ ∣ eval (P n (B a)) ⟧)
       → Term ⟦ ℓ ∣ eval (P n (`Σ A B)) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `Desc) ⟧)
    → ((n : ℕ) (D : Desc n) (X : Type n)
       (rec : ⟦ ℓ ∣ eval (P n X) ⟧)
       → Term ⟦ ℓ ∣ eval (P n (`⟦ D ⟧ᵈ X)) ⟧)
    → ((n : ℕ) (D : Desc n) → Term ⟦ ℓ ∣ eval (P n (`μ D)) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `Type) ⟧)
    → ((n : ℕ) (A : Type n)
        (rec : ⟦ ℓ ∣ eval (P n A) ⟧)
        → Term ⟦ ℓ ∣ eval (P (suc n) `⟦ A ⟧) ⟧)
    → (n : Term ℕ)
    (A : Term (Type (eval n)))
    → Term ⟦ ℓ ∣ eval (P (eval n) (eval A)) ⟧

  {- Desc introduction -}
  `⊤ᵈ `Xᵈ : ∀{ℓ} → Term (Desc ℓ)
  `Πᵈ `Σᵈ : ∀{ℓ}
    (A : Term (Type ℓ))
    (B : ⟦ ℓ ∣ eval A ⟧ → Term (Desc (suc ℓ)))
    → Term (Desc (suc ℓ))

  {- Desc elimination -}
  `elimDesc : ∀{ℓ}
    (P : (n : ℕ) → Desc n → Term (Type ℓ))
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `⊤) ⟧)
    → ((n : ℕ) → Term ⟦ ℓ ∣ eval (P n `X) ⟧)
    → ((n : ℕ) (A : Type n) (D : ⟦ n ∣ A ⟧ → Desc (suc n))
       (rec : (a : ⟦ n ∣ A ⟧) → ⟦ ℓ ∣ eval (P (suc n) (D a)) ⟧)
       → Term ⟦ ℓ ∣ eval (P (suc n) (`Π A D)) ⟧)
    → ((n : ℕ) (A : Type n) (D : ⟦ n ∣ A ⟧ → Desc (suc n))
       (rec : (a : ⟦ n ∣ A ⟧) → ⟦ ℓ ∣ eval (P (suc n) (D a)) ⟧)
       → Term ⟦ ℓ ∣ eval (P (suc n) (`Σ A D)) ⟧)
    → (n : Term ℕ)
    (D : Term (Desc (eval n)))
    → Term ⟦ ℓ ∣ eval (P (eval n) (eval D)) ⟧

  {- Value introduction -}
  `tt : Term ⊤
  `true `false : Term Bool
  `zero : Term ℕ
  `suc : Term ℕ → Term ℕ
  `λ : ∀{A} {B : A → Set}
    (f : (a : A) → Term (B a))
    → Term ((a : A) → B a)
  _`,_ : ∀{A B}
    (a : Term A)
    (b : Term (B (eval a)))
    → Term (Σ A B)
  `con : ∀{ℓ D}
    (x : Term (⟦ ℓ ∣ D ⟧ᵈ (μ D)))
    → Term (μ D)

  {- Value elimination -}
  `elim⊥ : ∀{A}
    → Term ⊥
    → Term A
  `elimBool : ∀{ℓ}
    (P : Bool → Term (Type ℓ))
    (pt : Term ⟦ ℓ ∣ eval (P true) ⟧)
    (pf : Term ⟦ ℓ ∣ eval (P false) ⟧)
    (b : Term Bool)
    → Term ⟦ ℓ ∣ eval (P (eval b)) ⟧
  `elimℕ : ∀{ℓ}
    (P : ℕ → Term (Type ℓ))
    (pz : Term ⟦ ℓ ∣ eval (P zero) ⟧)
    (ps : (n : ℕ) → ⟦ ℓ ∣ eval (P n) ⟧ → Term ⟦ ℓ ∣ eval (P (suc n)) ⟧)
    (n : Term ℕ)
    → Term ⟦ ℓ ∣ eval (P (eval n)) ⟧
  `proj₁ : ∀{A B}
    (ab : Term (Σ A B))
    → Term A
  `proj₂ : ∀{A B}
    (ab : Term (Σ A B))
    → Term (B (proj₁ (eval ab)))
  _`$_ : ∀{A} {B : A → Set}
    (f : Term ((a : A) → B a))
    (a : Term A)
    → Term (B (eval a))
  `des : ∀{ℓ} {D : Desc ℓ}
    → (Term (μ D))
    → Term (⟦ ℓ ∣ D ⟧ᵈ (μ D))

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

{- Type introduction -}
eval `⊥ = `⊥
eval `⊤ = `⊤
eval `Bool = `Bool
eval `ℕ = `ℕ
eval `Desc = `Desc
eval `Type = `Type
eval (`Π A B) = `Π (eval A) (λ a → eval (B a))
eval (`Σ A B) = `Σ (eval A) (λ a → eval (B a))
eval (`μ D) = `μ (eval D)
eval (`⟦ D ⟧ᵈ X) = `⟦ eval D ⟧ᵈ (eval X)
eval `⟦ A ⟧ = `⟦ eval A ⟧

{- Type elimination -}
eval (`elimType {ℓ = ℓ} P p⊥ p⊤ pBool pℕ pΠ pΣ pDesc p⟦D⟧ᵈ pμ pType p⟦A⟧ n A) =
  elimType (λ n A → ⟦ ℓ ∣ eval (P n A) ⟧)
    (λ n → eval (p⊥ n)) (λ n → eval (p⊤ n)) (λ n → eval (pBool n)) (λ n → eval (pℕ n))
    (λ n A B rec₁ rec₂ → eval (pΠ n A B rec₁ rec₂))
    (λ n A B rec₁ rec₂ → eval (pΣ n A B rec₁ rec₂))
    (λ n → eval (pDesc n))
    (λ n D X rec → eval (p⟦D⟧ᵈ n D X rec))
    (λ n D → eval (pμ n D))
    (λ n → eval (pType n))
    (λ n A rec → eval (p⟦A⟧ n A rec))
    (eval n)
    (eval A)

{- Desc introduction -}
eval `⊤ᵈ = `⊤
eval `Xᵈ = `X
eval (`Πᵈ A D) = `Π (eval A) (λ a → eval (D a))
eval (`Σᵈ A D) = `Σ (eval A) (λ a → eval (D a))

{- Desc elimination -}
eval (`elimDesc {ℓ = ℓ} P p⊤ pX pΠ pΣ n D) =
  elimDesc (λ n D → ⟦ ℓ ∣ eval (P n D) ⟧)
    (λ n → eval (p⊤ n)) (λ n → eval (pX n))
    (λ n A D rec → eval (pΠ n A D rec))
    (λ n A D rec → eval (pΣ n A D rec))
    (eval n)
    (eval D)

{- Value introduction -}
eval `tt = tt
eval `true = true
eval `false = false
eval `zero = zero
eval (`suc n) = suc (eval n)
eval (`λ f) = λ a → eval (f a)
eval (a `, b) = eval a , eval b
eval (`con x) = con (eval x)

{- Value elimination -}
eval (`elim⊥ bot) = elim⊥ (eval bot)
eval (`elimBool {ℓ = ℓ} P pt pf b) =
  elimBool (λ b → ⟦ ℓ ∣ eval (P b) ⟧)
    (eval pt) (eval pf) (eval b)
eval (`elimℕ {ℓ = ℓ} P pz ps n) =
  elimℕ (λ n → ⟦ ℓ ∣ eval (P n) ⟧)
    (eval pz) (λ n pn → eval (ps n pn)) (eval n)
eval (`proj₁ ab) = proj₁ (eval ab)
eval (`proj₂ ab) = proj₂ (eval ab)
eval (f `$ a) = (eval f) (eval a)
eval (`des {ℓ = ℓ} x) = des {ℓ = ℓ} (eval x)

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
open import Coinduction using ( ∞ ; ♯_ ; ♭ )
open import Data.Product using ( _,_ )
open import FRP.LTL.ISet.Core using ( ISet ; M⟦_⟧ ; splitM⟦_⟧ ; ⟦_⟧ ; ⌈_⌉ ; [_] )
open import FRP.LTL.ISet.Product using ( _∧_ )
open import FRP.LTL.ISet.Stateless using ( _⇒_ )
open import FRP.LTL.Time.Bound using ( Time∞ ; fin ; +∞ ; _≼_ ; _≺_ ; ≼-refl ; ≺-impl-≼ ; ≺-impl-⋡ ; _≺-trans_ ; _≼-case_ ; lt ; eq ; gt ; t≺+∞ )
open import FRP.LTL.Time.Interval using ( [_⟩ )
open import FRP.LTL.Util using ( ⊥-elim ; ≡-relevant )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

module FRP.LTL.ISet.Decoupled where

data _∙_⊷_∙_ (A : ISet) (s : Time∞) (B : ISet) (u : Time∞) : Set where
  inp : .(s ≺ u) → .(u ≺ +∞) →
    (∀ {t} .(s≺t : s ≺ t) → M⟦ A ⟧ [ s≺t ⟩ → ∞ (A ∙ t ⊷ B ∙ u)) →
      (A ∙ s ⊷ B ∙ u)
  out : ∀ {v} .(u≺v : u ≺ v) →
    M⟦ B ⟧ [ u≺v ⟩ → ∞ (A ∙ s ⊷ B ∙ v) →
      (A ∙ s ⊷ B ∙ u)
  done : .(u ≡ +∞) →
    (A ∙ s ⊷ B ∙ u)

_▹_ : ISet → ISet → ISet
A ▹ B = ⌈ (λ t → A ∙ fin t ⊷ B ∙ fin t) ⌉

_/_/_ : ∀ {A B s t u} → (A ∙ s ⊷ B ∙ u) → .(s≺t : s ≺ t) → M⟦ A ⟧ [ s≺t ⟩ → (A ∙ t ⊷ B ∙ u)
inp s≺u u≺∞ P / s≺t / σ = ♭ (P s≺t σ)
out u≺v τ P   / s≺t / σ = out u≺v τ (♯ (♭ P / s≺t / σ))
done u≡∞      / s≺t / σ = done u≡∞

mutual

  ≻-tr : ∀ {A B C s u} .(s≻u : u ≺ s) → M⟦ B ⟧ [ s≻u ⟩ →
    ((A ∧ B) ∙ u ⊷ (A ∧ C) ∙ u) → (B ∙ s ⊷ C ∙ u)
  ≻-tr s≻u σ (inp u≺u u≺∞ P) = ⊥-elim (≺-impl-⋡ u≺u ≼-refl)
  ≻-tr {A} {B} {C} {s} {u} s≻u σ (out {v} u≺v [ ρ , τ ] P)
    with s ≼-case v
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | lt s≺v
    with splitM⟦ A ⟧ [ s≻u ⟩ [ s≺v ⟩ refl ρ
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | lt s≺v | (ρ₁ , ρ₂) =
    out u≺v τ (♯ ≺-tr s≺v ρ₂ (♭ P / s≻u / [ ρ₁ , σ ]))
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | eq s≡v
    with ≡-relevant s≡v
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | eq s≡v | refl =
    out u≺v τ (♯ tr (♭ P / s≻u / [ ρ , σ ]))
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | gt s≻v
    with splitM⟦ B ⟧ [ u≺v ⟩ [ s≻v ⟩ refl σ
  ≻-tr {A} {B} {C} s≻u σ (out u≺v [ ρ , τ ] P) | gt s≻v | (σ₁ , σ₂) =
    out u≺v τ (♯ ≻-tr s≻v σ₂ (♭ P / u≺v / [ ρ , σ₁ ]))
  ≻-tr s≻u σ (done u≡∞) = done u≡∞

  ≺-tr : ∀ {A B C s u} .(s≺u : s ≺ u) → M⟦ A ⟧ [ s≺u ⟩ →
    ((A ∧ B) ∙ s ⊷ (A ∧ C) ∙ u) → (B ∙ s ⊷ C ∙ u)
  ≺-tr {A} {B} {C} {s} {+∞}    s≺u ρ P = done refl
  ≺-tr {A} {B} {C} {s} {fin u} s≺u ρ P = inp s≺u t≺+∞ Q where

    Q : ∀ {t} .(s≺t : s ≺ t) → M⟦ B ⟧ [ s≺t ⟩ → ∞ (B ∙ t ⊷ C ∙ fin u)
    Q {t} s≺t σ  with t ≼-case (fin u)
    Q s≺t σ | lt t≺u with splitM⟦ _ ⟧ [ s≺t ⟩ [ t≺u ⟩ refl ρ
    Q s≺t σ | lt t≺u | (ρ₁ , ρ₂) = ♯ ≺-tr t≺u ρ₂ (P / s≺t / [ ρ₁ , σ ])
    Q s≺t σ | eq t≡u with ≡-relevant t≡u
    Q s≺t σ | eq t≡u | refl = ♯ tr (P / s≺u / [ ρ , σ ])
    Q s≺t σ | gt t≻u with splitM⟦ _ ⟧ [ s≺u ⟩ [ t≻u ⟩ refl σ
    Q s≺t σ | gt t≻u | (σ₁ , σ₂) = ♯ (≻-tr t≻u σ₂ (P / s≺u / [ ρ , σ₁ ]))

  tr : ∀ {A B C s} → ((A ∧ B) ∙ s ⊷ (A ∧ C) ∙ s) → (B ∙ s ⊷ C ∙ s)
  tr (inp s≺s s≺∞ P)       = ⊥-elim (≺-impl-⋡ s≺s ≼-refl)
  tr (out s≺u [ ρ , τ ] P) = out s≺u τ (♯ ≺-tr s≺u ρ (♭ P))
  tr (done s≡∞)            = done s≡∞

loop : ∀ {A B C} → ⟦ ((A ∧ B) ▹ (A ∧ C)) ⇒ (B ▹ C) ⟧
loop [ [ f ] ] = [ (λ t t∈i → tr (f t t∈i)) ]

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Abstract.Types
open import LibraBFT.Abstract.Types.EpochConfig
open WithAbsVote

-- This module defines the notion of one Record r "extending" another
-- Record r' (denoted r' ← r), ensuring rules about rounds and that r
-- correctly identifies r'

module LibraBFT.Abstract.Records.Extends
    (UID    : Set)
    (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
    (NodeId : Set)
    (𝓔      : EpochConfig UID NodeId)
    (𝓥     : VoteEvidence UID NodeId 𝓔)
  where

  open import LibraBFT.Abstract.Records UID _≟UID_ NodeId 𝓔 𝓥

  -- Most of the conditions in section 4.2 of the paper (see
  -- LibraBFT.Abstract.RecordChain.Properties) would be checked
  -- by the implementation to validate data received.
  --
  -- In the Abstract model, however, we are only concerned with
  -- proving the properties; only round numbers and identifiers
  -- for previous records are actually critical to thm S5!
  data _←_ : Record → Record → Set where
    I←B : {b : Block}
        → 0 < getRound b
        → bPrevQC b ≡ nothing
        → I ← B b
    Q←B : {q : QC} {b : Block}
        → getRound q < getRound b
        → just (qCertBlockId q) ≡ bPrevQC b
        → Q q ← B b
    B←Q : {b : Block} {q : QC}
        → getRound q ≡ getRound b
        → bId b ≡ qCertBlockId q
        → B b ← Q q

  -- Equivalent records extend equivalent records (modulo injectivity
  -- failure of bId).
  ←-≈Rec : ∀{r₀ r₁ s₀ s₁} → s₀ ← r₀ → s₁ ← r₁
           → r₀ ≈Rec r₁
           → NonInjective-≡ bId ⊎ (s₀ ≈Rec s₁)
  ←-≈Rec (I←B x x₁) (I←B x₂ x₃) hyp = inj₂ eq-I
  ←-≈Rec (I←B x x₁) (Q←B x₂ x₃) (eq-B refl)
    = ⊥-elim (maybe-⊥ (sym x₃) x₁)
  ←-≈Rec (Q←B x x₁) (I←B x₂ x₃) (eq-B refl)
    = ⊥-elim (maybe-⊥ (sym x₁) x₃)
  ←-≈Rec (Q←B {q₀} x refl) (Q←B {q₁} x₂ refl) (eq-B refl)
    = inj₂ (eq-Q refl) -- Here is where we wouldn't be able to
                       -- complete the proof if we required round equality
                       -- in eq-Q
  ←-≈Rec (B←Q {b₀} x refl) (B←Q {b₁} w refl) (eq-Q refl)
    with b₀ ≟Block b₁
  ...| no  hb  = inj₁ ((b₀ , b₁) , (λ x → hb x) , refl)
  ...| yes prf = inj₂ (eq-B prf)

  ←-irrelevant : Irrelevant _←_
  ←-irrelevant (I←B r₁ h₁) (I←B r₂ h₂)
    = cong₂ I←B (≤-irrelevant r₁ r₂) (≡-irrelevant h₁ h₂)
  ←-irrelevant (Q←B r₁ h₁) (Q←B r₂ h₂)
    = cong₂ Q←B (≤-irrelevant r₁ r₂) (≡-irrelevant h₁ h₂)
  ←-irrelevant (B←Q r₁ h₁) (B←Q r₂ h₂)
    = cong₂ B←Q (≡-irrelevant r₁ r₂) (≡-irrelevant h₁ h₂)

  ←-round-≤ : ∀{r₀ r₁} → r₀ ← r₁ → round r₀ ≤ round r₁
  ←-round-≤ (I←B r h)    = z≤n
  ←-round-≤ (Q←B r h)    = <⇒≤ r
  ←-round-≤ (B←Q refl h) = ≤-refl

  ←←-round-< : ∀{r r₀ r₁} → r ← r₀ → r₀ ← r₁
             → round r < round r₁
  ←←-round-< (I←B r h)     (B←Q refl _) = r
  ←←-round-< (Q←B r h)     rr           = ≤-trans r (←-round-≤ rr)
  ←←-round-< (B←Q refl h)  (Q←B prf _)  = prf

  -- LemmaS1, clause 2: injectivity of _←_
  lemmaS1-2 : ∀{r₀ r₁ r₂ r₂'}
            → r₂ ≈Rec r₂'
            → r₀ ← r₂ → r₁ ← r₂'
            → uid r₀ ≡ uid r₁
  lemmaS1-2 {i₀} {i₁} {b} hyp (I←B _ i₀←b) (I←B _ i₁←b) = refl
  lemmaS1-2 {q}  {i}  {b} (eq-B refl) (Q←B _ ())   (I←B _ refl)
  lemmaS1-2 {i}  {q}  {b} (eq-B refl) (I←B _ refl) (Q←B _ ())
  lemmaS1-2 {q₀} {q₁} {b} (eq-B refl) (Q←B _ refl) (Q←B _ refl) = refl
  lemmaS1-2 {b₀} {b₁} {q} (eq-Q refl) (B←Q _ refl) (B←Q _ refl) = refl

  -- A better name for lemmaS1-2
  ←-inj : ∀{r₀ r₁ r₂}
        → r₀ ← r₂ → r₁ ← r₂
        → uid r₀ ≡ uid r₁
  ←-inj = lemmaS1-2 ≈Rec-refl

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
{-

This file contains:

- 3×3 lemma for pushouts
  Written by: Loïc Pujet, April 2019

-}

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

module Cubical.HITs.Pushout.Properties where

open import Cubical.Core.Glue

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

open import Cubical.Data.Prod.Base
open import Cubical.Data.Unit

open import Cubical.HITs.Pushout.Base

{-

  3×3 lemma for pushouts

Let Aᵢⱼ denote a type, fᵢⱼ a map and Hᵢⱼ a homotopy. Given a diagram of the following shape:

A00 ←—f01—— A02 ——f03—→ A04
 ↑           ↑           ↑
f10   H11   f12   H13   f14
 |           |           |
A20 ←—f21—— A22 ——f23—→ A24
 |           |           |
f30   H31   f32   H33   f34
 ↓           ↓           ↓
A40 ←—f41—— A42 ——f43—→ A44

one can build its colimit from pushouts in two ways:
- either build pushouts A□0, A□2, A□4 of the lines and then build the pushout A□○ of the resulting
  diagram A□0 ←—f□1—— A□2 ——f□3—→ A□4 ;
- or build pushouts of the columns and build the pushout A○□ of the resulting diagram A0□ ← A2□ → A4□.

Then the lemma states there is an equivalence A□○ ≃ A○□.

-}

module 3x3-span
  (A00 A02 A04 A20 A22 A24 A40 A42 A44 : Type₀)

  (f10 : A20 → A00)
  (f12 : A22 → A02)
  (f14 : A24 → A04)

  (f30 : A20 → A40)
  (f32 : A22 → A42)
  (f34 : A24 → A44)

  (f01 : A02 → A00)
  (f21 : A22 → A20)
  (f41 : A42 → A40)

  (f03 : A02 → A04)
  (f23 : A22 → A24)
  (f43 : A42 → A44)

  (H11 : ∀ x → f01 (f12 x) ≡ f10 (f21 x))
  (H13 : ∀ x → f03 (f12 x) ≡ f14 (f23 x))
  (H31 : ∀ x → f41 (f32 x) ≡ f30 (f21 x))
  (H33 : ∀ x → f43 (f32 x) ≡ f34 (f23 x))
  where

  -- pushouts of the lines
  A□0 : Type₀
  A□0 = Pushout f10 f30

  A□2 : Type₀
  A□2 = Pushout f12 f32

  A□4 : Type₀
  A□4 = Pushout f14 f34

  -- maps between pushouts
  f□1 : A□2 → A□0
  f□1 (inl x) = inl (f01 x)
  f□1 (inr x) = inr (f41 x)
  f□1 (push a j) = ((λ i → inl (H11 a i))
                   ∙∙ push (f21 a)
                   ∙∙ (λ i → inr (H31 a (~ i)))) j

  f□3 : A□2 → A□4
  f□3 (inl x) = inl (f03 x)
  f□3 (inr x) = inr (f43 x)
  f□3 (push a j) = ((λ i → inl (H13 a i))
                   ∙∙ push (f23 a)
                   ∙∙ (λ i → inr (H33 a (~ i)))) j

  -- total pushout
  A□○ : Type₀
  A□○ = Pushout f□1 f□3

  -- pushouts of the columns
  A0□ : Type₀
  A0□ = Pushout f01 f03

  A2□ : Type₀
  A2□ = Pushout f21 f23

  A4□ : Type₀
  A4□ = Pushout f41 f43

  -- maps between pushouts
  f1□ : A2□ → A0□
  f1□ (inl x) = inl (f10 x)
  f1□ (inr x) = inr (f14 x)
  f1□ (push a j) = ((λ i → inl (H11 a (~ i)))
                   ∙∙ push (f12 a)
                   ∙∙ (λ i → inr (H13 a i))) j

  f3□ : A2□ → A4□
  f3□ (inl x) = inl (f30 x)
  f3□ (inr x) = inr (f34 x)
  f3□ (push a j) = ((λ i → inl (H31 a (~ i)))
                   ∙∙ push (f32 a)
                   ∙∙ (λ i → inr (H33 a i))) j

  -- total pushout
  A○□ : Type₀
  A○□ = Pushout f1□ f3□

  -- forward map of the equivalence A□○ ≃ A○□
  forward-l : A□0 → A○□
  forward-l (inl x) = inl (inl x)
  forward-l (inr x) = inr (inl x)
  forward-l (push a i) = push (inl a) i

  forward-r : A□4 → A○□
  forward-r (inl x) = inl (inr x)
  forward-r (inr x) = inr (inr x)
  forward-r (push a i) = push (inr a) i

  forward-filler : A22 → I → I → I → A○□
  forward-filler a i j = hfill (λ t → λ { (i = i0) → inl (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) j (~ t))
                                 ; (i = i1) → inr (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) j (~ t))
                                 ; (j = i0) → forward-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) i t)
                                 ; (j = i1) → forward-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) i t) })
                        (inS (push (push a j) i))

  A□○→A○□ : A□○ → A○□
  A□○→A○□ (inl x) = forward-l x
  A□○→A○□ (inr x) = forward-r x
  A□○→A○□ (push (inl x) i) = inl (push x i)
  A□○→A○□ (push (inr x) i) = inr (push x i)
  A□○→A○□ (push (push a i) j) = forward-filler a i j i1

  -- backward map
  backward-l : A0□ → A□○
  backward-l (inl x) = inl (inl x)
  backward-l (inr x) = inr (inl x)
  backward-l (push a i) = push (inl a) i

  backward-r : A4□ → A□○
  backward-r (inl x) = inl (inr x)
  backward-r (inr x) = inr (inr x)
  backward-r (push a i) = push (inr a) i

  backward-filler : A22 → I → I → I → A□○
  backward-filler a i j = hfill (λ t → λ { (i = i0) → inl (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) j (~ t))
                                 ; (i = i1) → inr (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) j (~ t))
                                 ; (j = i0) → backward-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) i t)
                                 ; (j = i1) → backward-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) i t) })
                        (inS (push (push a j) i))

  A○□→A□○ : A○□ → A□○
  A○□→A□○ (inl x) = backward-l x
  A○□→A□○ (inr x) = backward-r x
  A○□→A□○ (push (inl x) i) = inl (push x i)
  A○□→A□○ (push (inr x) i) = inr (push x i)
  A○□→A□○ (push (push a i) j) = backward-filler a i j i1

  -- first homotopy
  homotopy1-l : ∀ x → A□○→A○□ (backward-l x) ≡ inl x
  homotopy1-l (inl x) = refl
  homotopy1-l (inr x) = refl
  homotopy1-l (push a i) = refl

  homotopy1-r : ∀ x → A□○→A○□ (backward-r x) ≡ inr x
  homotopy1-r (inl x) = refl
  homotopy1-r (inr x) = refl
  homotopy1-r (push a i) = refl

  A○□→A□○→A○□ : ∀ x → A□○→A○□ (A○□→A□○ x) ≡ x
  A○□→A□○→A○□ (inl x) = homotopy1-l x
  A○□→A□○→A○□ (inr x) = homotopy1-r x
  A○□→A□○→A○□ (push (inl x) i) k = push (inl x) i
  A○□→A□○→A○□ (push (inr x) i) k = push (inr x) i
  A○□→A□○→A○□ (push (push a i) j) k =
    hcomp (λ t → λ { (i = i0) → forward-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) j (~ t))
                   ; (i = i1) → forward-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) j (~ t))
                   ; (j = i0) → homotopy1-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) i t) k
                   ; (j = i1) → homotopy1-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) i t) k
                   ; (k = i0) → A□○→A○□ (backward-filler a i j t)
                   ; (k = i1) → forward-filler a j i (~ t) })
          (forward-filler a j i i1)

  -- second homotopy
  homotopy2-l : ∀ x → A○□→A□○ (forward-l x) ≡ inl x
  homotopy2-l (inl x) = refl
  homotopy2-l (inr x) = refl
  homotopy2-l (push a i) = refl

  homotopy2-r : ∀ x → A○□→A□○ (forward-r x) ≡ inr x
  homotopy2-r (inl x) = refl
  homotopy2-r (inr x) = refl
  homotopy2-r (push a i) = refl

  A□○→A○□→A□○ : ∀ x → A○□→A□○ (A□○→A○□ x) ≡ x
  A□○→A○□→A□○ (inl x) = homotopy2-l x
  A□○→A○□→A□○ (inr x) = homotopy2-r x
  A□○→A○□→A□○ (push (inl x) i) k = push (inl x) i
  A□○→A○□→A□○ (push (inr x) i) k = push (inr x) i
  A□○→A○□→A□○ (push (push a i) j) k =
    hcomp (λ t → λ { (i = i0) → backward-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) j (~ t))
                   ; (i = i1) → backward-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) j (~ t))
                   ; (j = i0) → homotopy2-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) i t) k
                   ; (j = i1) → homotopy2-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) i t) k
                   ; (k = i0) → A○□→A□○ (forward-filler a i j t)
                   ; (k = i1) → backward-filler a j i (~ t) })
          (backward-filler a j i i1)

  -- equivalence
  Pushout3x3 : A□○ ≡ A○□
  Pushout3x3 = isoToPath (iso A□○→A○□ A○□→A□○ A○□→A□○→A○□ A□○→A○□→A□○)

Pushout3x3 : ∀ A00 A02 A04 A20 A22 A24 A40 A42 A44 f10 f12 f14 f30 f32 f34 f01 f21 f41 f03 f23 f43 H11 H13 H31 H33 →
  3x3-span.A□○ A00 A02 A04 A20 A22 A24 A40 A42 A44 f10 f12 f14 f30 f32 f34 f01 f21 f41 f03 f23 f43 H11 H13 H31 H33
  ≡ 3x3-span.A○□ A00 A02 A04 A20 A22 A24 A40 A42 A44 f10 f12 f14 f30 f32 f34 f01 f21 f41 f03 f23 f43 H11 H13 H31 H33
Pushout3x3 = 3x3-span.Pushout3x3

max_stars_repo_name: loic-p/cubical

max_issues_repo_name: loic-p/cubical

max_forks_repo_name: loic-p/cubical


text:
-- Andreas, 2016-01-03, issue reported by mechvel
module _ where

-- With hidden parameter, things work

module Works0 {A : Set} where

  postulate
    P : (a : A) → Set

  record Works (a : A) : Set where

    f : P a → Set
    f p with p
    ... | _ = A

-- With visible parameter, the error is triggered
-- because it is turned hidden inside the record section

module Fails (A : Set) where

  postulate
    P : (a : A) → Set

  -- Modules do not touch visibility of parameters, so things work.
  module Works (a : A) where

    f : P a → Set
    f p with p
    ... | _ = A

  -- Records have some magic to make record parameters hidden
  -- in record section.
  -- This leads to an error in @checkInternal@.

  record Fails (a : A) : Set where

    f : P a → Set
    f p with p
    ... | _ = A

-- ERROR WAS:
-- Expected a visible argument, but found a hidden argument
-- when checking that the type (w p : P a) → Set of the
-- generated with function is well-formed

-- Should succeed.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-06-11

{-# OPTIONS --copatterns #-}

open import Common.Size

module _ {C : Set} {R : C → Set} where

mutual
  record IO (i : Size) (A : Set) : Set where
    coinductive
    constructor delay
    field
      force : {j : Size< i} → IO' j A

  data IO' (i : Size) (A : Set) : Set where
    do     : (c : C) (f : R c → IO i A) → IO' i A
    return : (a : A) → IO' i A

open IO

module Works where

  _>>=_ : ∀{i A B} (m : IO i A) (k : A → IO i B) → IO i B
  force (m >>= k) with force m
  force (m >>= k) {j} | do c f   = do c λ x → f x >>= k
  force (m >>= k) {j} | return a = force (k a)

_>>=_ : ∀{i A B} (m : IO i A) (k : A → IO i B) → IO i B
force (m >>= k) with force m
force (m >>= k) | do c f   = do c λ x → f x >>= k
force (m >>= k) | return a = force (k a)

-- Error WAS:
-- Too few arguments given in with-clause
-- when checking that the clause
-- force (m >>= k) with force m
-- force (m >>= k) | do c f = do c (λ x → f x >>= k)
-- force (m >>= k) | return a = force (k a)
-- has type {i : Size} {A B : Set} → IO i A → (A → IO i B) → IO i B


text:
module Test01 where

hoge : {A : Set} → A → A
hoge x = x

open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; subst)
open import Function using (id)

lemma1 : {X Y : Set} → (X ≡ (X → Y)) → X
lemma1 p rewrite p = (λ x → let f = subst id p x in f x)

curry : {X Y : Set} → (X ≡ (X → Y)) → Y
curry p = (let f = subst id p (lemma1 p) in f (lemma1 p))

open import Data.Bool
open import Data.Nat
open import Data.Empty

postulate
  First : ℕ → Set
  All   : ℕ → Set
  fToA  : ((n : ℕ) → First n) → ((n : ℕ) → All n)
  fToA2 : (z : ℕ) → (First z → All z)
  tekito : (z : ℕ) → ((All z → ⊥) → (First z → ⊥)) → First (suc z)
  contra : (z : ℕ) → ((All z → ⊥) → (First z → ⊥)) → (First z → All z)

mutual
  -- 失敗
  contraFirstToAll : (z : ℕ) → ((All z → ⊥) → (First z → ⊥))
  -- contraFirstToAll z allToVoid _ = let foo = (contra z (contraFirstToAll z)) (limitedDivSeq z) in  allToVoid foo
  contraFirstToAll z allToVoid _ = let foo = fToA (λ k → limitedDivSeq k) in  allToVoid (foo z)

  limitedDivSeq : (n : ℕ) → First n
  limitedDivSeq zero    = {!   !}
  limitedDivSeq (suc n) = let bar = contraFirstToAll n in tekito n bar

-- Idris
{-
postulate foo : (t : Nat) -> LT' t (S t)
contraFirstToAll :
  (z : Nat) -> (((AllLimited . B.allDivSeq) z -> Void) -> ((FirstLimited . B.allDivSeq) z -> Void))
contraFirstToAll Z     allToVoid _ = allToVoid IsAllLimited00
contraFirstToAll (S z) _         _ = wfInd {P=(\z=>Void)} {rel=LT'} step (S z) where
  step : (x : Nat) -> ((y : Nat) -> LT' y x -> Void) -> Void
  step Z     _  = believe_me "ここには来ない"
  step (S x) rs = rs x (foo x)
-- ?rhs1 が書けない！！
contraFirstToAll :
  (z : Nat) -> (((AllLimited . B.allDivSeq) z -> Void) -> ((FirstLimited . B.allDivSeq) z -> Void))
contraFirstToAll Z     allToVoid _ = allToVoid IsAllLimited00
contraFirstToAll (S z) _         _ = step (S z) SIsNotZ (wellFounded {rel=LT'} (S z)) where
  step : (x : Nat) -> Not (x = Z) -> Accessible LT' x -> Void
  step Z     p _           = void (p Refl)
  step (S x) p (Access rs) = step x ?rhs1 (rs x (foo x))
-}


text:
-- This demonstrates a known issue:
-- The parser is not aware of strings, thus,
-- a closing block comment delimiter inside a string
-- is taken as a closing block comment delimiter.

-- Without nested comments:

{- This is commented-out.
test = "A weird string with comment closing -} and other garbage @#$% that appears now as Agda code!"
-}

-- With nested comments:

{-
{- This is commented-out.
test = "A weird string with comment closing -} and other garbage @#$%!"
-- NB: this confuses even Agda (at the time of writing, version 2.6.1).
-}
This should be still commented-out. -}

-- The reverse situation:

test = "Never put comment opening {- inside a string!"

postulate
  ThisShouldNotBeCommentedOut : Set

-- -} This should be text, not code!!

-- SNAFU.


text:
open import Function
open import Relation.Nullary
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Sum
open import Data.Product

delim : ∀ {α β} {A : Set α} {B : Dec A -> Set β}
      -> (d : Dec A) -> (∀ x -> B (yes x)) -> (∀ c -> B (no c)) -> B d
delim (yes x) f g = f x
delim (no  c) f g = g c

drec = λ {α β} {A : Set α} {B : Set β} -> delim {A = A} {B = λ _ -> B}

dcong₂ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x y v w}
       -> (f : A -> B -> C)
       -> (∀ {x y} -> f x v ≡ f y w -> x ≡ y × v ≡ w)
       -> Dec (x ≡ y)
       -> Dec (v ≡ w)
       -> Dec (f x v ≡ f y w)
dcong₂ f inj d₁ d₂ = drec d₁
    (λ p₁ -> drec d₂
      (λ p₂ -> yes (cong₂ f p₁ p₂))
      (λ c  -> no (c ∘ proj₂ ∘ inj)))
    (λ c  -> no (c ∘ proj₁ ∘ inj))

infixl 5 _▻_
infixr 6 _⇒_
infix  4 _≟ᵗ_ _≟ᶜ_ _∈_ _⊂[_]_ _⊂?_ _⊢_
infixr 6 vs_
infixr 5 ƛ_
infixl 7 _·_

data Type : Set where
  ⋆   : Type
  _⇒_ : Type -> Type -> Type

data Con : Set where
  ε   : Con
  _▻_ : Con -> Type -> Con

data _∈_ σ : Con -> Set where
  vz  : ∀ {Γ}   -> σ ∈ Γ ▻ σ
  vs_ : ∀ {Γ τ} -> σ ∈ Γ     -> σ ∈ Γ ▻ τ

data _⊢_ Γ : Type -> Set where
  var : ∀ {σ}   -> σ ∈ Γ     -> Γ ⊢ σ
  ƛ_  : ∀ {σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ
  _·_ : ∀ {σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ     -> Γ ⊢ τ

⇒-inj : ∀ {σ₁ σ₂ τ₁ τ₂} -> σ₁ ⇒ τ₁ ≡ σ₂ ⇒ τ₂ -> σ₁ ≡ σ₂ × τ₁ ≡ τ₂
⇒-inj refl = refl , refl

▻-inj : ∀ {Γ₁ Γ₂ σ₁ σ₂} -> Γ₁ ▻ σ₁ ≡ Γ₂ ▻ σ₂ -> Γ₁ ≡ Γ₂ × σ₁ ≡ σ₂
▻-inj refl = refl , refl

_≟ᵗ_ : Decidable (_≡_ {A = Type})
⋆         ≟ᵗ ⋆         = yes refl
(σ₁ ⇒ τ₁) ≟ᵗ (σ₂ ⇒ τ₂) = dcong₂ _⇒_ ⇒-inj (σ₁ ≟ᵗ σ₂) (τ₁ ≟ᵗ τ₂)
⋆         ≟ᵗ (σ₂ ⇒ τ₂) = no λ()
(σ₁ ⇒ τ₁) ≟ᵗ ⋆         = no λ()

_≟ᶜ_ : Decidable (_≡_ {A = Con})
ε     ≟ᶜ ε     = yes refl
Γ ▻ σ ≟ᶜ Δ ▻ τ = dcong₂ _▻_ ▻-inj (Γ ≟ᶜ Δ) (σ ≟ᵗ τ)
ε     ≟ᶜ Δ ▻ τ = no λ()
Γ ▻ σ ≟ᶜ ε     = no λ()

data _⊂[_]_ : Con -> Type -> Con -> Set where
  stop : ∀ {Γ σ}     -> Γ ⊂[ σ ] Γ ▻ σ
  skip : ∀ {Γ Δ σ τ} -> Γ ⊂[ σ ] Δ     -> Γ ⊂[ σ ] Δ ▻ τ

sub : ∀ {Γ Δ σ} -> Γ ⊂[ σ ] Δ -> σ ∈ Δ
sub  stop    = vz
sub (skip p) = vs (sub p)

⊂-inj : ∀ {Γ Δ σ τ} -> Γ ⊂[ σ ] Δ ▻ τ -> Γ ⊂[ σ ] Δ ⊎ Γ ≡ Δ × σ ≡ τ
⊂-inj  stop    = inj₂ (refl , refl)
⊂-inj (skip p) = inj₁ p

_⊂?_ : ∀ {σ} -> Decidable _⊂[ σ ]_
_⊂?_     Γ  ε      = no λ()
_⊂?_ {σ} Γ (Δ ▻ τ) with λ c₁ -> drec (Γ ⊂? Δ) (yes ∘ skip) (λ c₂ -> no ([ c₂ , c₁ ] ∘ ⊂-inj))
... | r with σ ≟ᵗ τ
... | no  c₁ = r (c₁ ∘ proj₂)
... | yes p₁ rewrite p₁ with Γ ≟ᶜ Δ
... | no  c₁ = r (c₁ ∘ proj₁)
... | yes p₂ rewrite p₂ = yes stop

⊢_ : Type -> Set
⊢ σ = ∀ {Γ} -> Γ ⊢ σ

⟦_⟧ᵗ : Type -> Set
⟦ ⋆     ⟧ᵗ = ⊢ ⋆
⟦ σ ⇒ τ ⟧ᵗ = ⟦ σ ⟧ᵗ -> ⟦ τ ⟧ᵗ

mutual
  ↑ : ∀ {σ} -> ⊢ σ -> ⟦ σ ⟧ᵗ
  ↑ {⋆}     t = t
  ↑ {σ ⇒ τ} f = λ x -> ↑ (f · ↓ x)

  ↓ : ∀ {σ} -> ⟦ σ ⟧ᵗ -> ⊢ σ
  ↓ {⋆}     t = t
  ↓ {σ ⇒ τ} f = λ {Γ} -> ƛ (↓ (f (varˢ Γ σ)))

  varˢ : ∀ Γ σ -> ⟦ σ ⟧ᵗ
  varˢ Γ σ = ↑ (λ {Δ} -> var (diff Δ Γ σ)) where
    diff : ∀ Δ Γ σ -> σ ∈ Δ
    diff Δ Γ σ = drec (Γ ⊂? Δ) sub ⊥ where postulate ⊥ : _

data ⟦_⟧ᶜ : Con -> Set where
  Ø   : ⟦ ε ⟧ᶜ
  _▷_ : ∀ {Γ σ} -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ -> ⟦ Γ ▻ σ ⟧ᶜ

lookupᵉ : ∀ {Γ σ} -> σ ∈ Γ -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ
lookupᵉ  vz    (ρ ▷ x) = x
lookupᵉ (vs v) (ρ ▷ x) = lookupᵉ v ρ

idᵉ : ∀ {Γ} -> ⟦ Γ ⟧ᶜ
idᵉ {ε}     = Ø
idᵉ {Γ ▻ σ} = idᵉ ▷ varˢ Γ σ

⟦_⟧ : ∀ {Γ σ} -> Γ ⊢ σ -> ⟦ Γ ⟧ᶜ -> ⟦ σ ⟧ᵗ
⟦ var v ⟧ ρ = lookupᵉ v ρ
⟦ ƛ b   ⟧ ρ = λ x -> ⟦ b ⟧ (ρ ▷ x)
⟦ f · x ⟧ ρ = ⟦ f ⟧ ρ (⟦ x ⟧ ρ)

eval : ∀ {Γ σ} -> Γ ⊢ σ -> ⟦ σ ⟧ᵗ
eval t = ⟦ t ⟧ idᵉ

norm : ∀ {Γ σ} -> Γ ⊢ σ -> Γ ⊢ σ
norm t = ↓ (eval t)

Term : Type -> Set
Term σ = ε ⊢ σ

I : Term (⋆ ⇒ ⋆)
I = ↓ id

K : Term (⋆ ⇒ ⋆ ⇒ ⋆)
K = ↓ const

S : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
S = ↓ _ˢ_

B : Term ((⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
B = ↓ _∘′_

C : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆ ⇒ ⋆)
C = ↓ flip

W : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆)
W = ↓ λ f x -> f x x

P : Term ((⋆ ⇒ ⋆ ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆ ⇒ ⋆ ⇒ ⋆)
P = ↓ _on_

O : Term (((⋆ ⇒ ⋆) ⇒ ⋆) ⇒ (⋆ ⇒ ⋆) ⇒ ⋆)
O = ↓ λ g f -> f (g f)

test₁ : norm (ε ▻ ⋆ ⇒ ⋆ ▻ ⋆ ⊢ ⋆ ∋ (ƛ var (vs vs vz) · var vz) · var vz) ≡ var (vs vz) · var vz
test₁ = refl

test₂ : S ≡ ƛ ƛ ƛ var (vs vs vz) · var vz · (var (vs vz) · var vz)
test₂ = refl


text:
open import Prelude
open import core

module lemmas-consistency where
  -- type consistency is symmetric
  ~sym : {t1 t2 : htyp} → t1 ~ t2 → t2 ~ t1
  ~sym TCRefl = TCRefl
  ~sym TCHole1 = TCHole2
  ~sym TCHole2 = TCHole1
  ~sym (TCArr p1 p2) = TCArr (~sym p1) (~sym p2)

  -- type consistency isn't transitive
  not-trans : ((t1 t2 t3 : htyp) → t1 ~ t2 → t2 ~ t3 → t1 ~ t3) → ⊥
  not-trans t with t (b ==> b) ⦇-⦈ b TCHole1 TCHole2
  ... | ()

  --  every pair of types is either consistent or not consistent
  ~dec : (t1 t2 : htyp) → ((t1 ~ t2) + (t1 ~̸ t2))
    -- this takes care of all hole cases, so we don't consider them below
  ~dec _ ⦇-⦈ = Inl TCHole1
  ~dec ⦇-⦈ _ = Inl TCHole2
    -- num cases
  ~dec b b = Inl TCRefl
  ~dec b (t2 ==> t3) = Inr ICBaseArr1
    -- arrow cases
  ~dec (t1 ==> t2) b = Inr ICBaseArr2
  ~dec (t1 ==> t2) (t3 ==> t4) with ~dec t1 t3 | ~dec t2 t4
  ... | Inl x | Inl y = Inl (TCArr x y)
  ... | Inl _ | Inr y = Inr (ICArr2 y)
  ... | Inr x | _     = Inr (ICArr1 x)

  -- no pair of types is both consistent and not consistent
  ~apart : {t1 t2 : htyp} → (t1 ~̸ t2) → (t1 ~ t2) → ⊥
  ~apart ICBaseArr1 ()
  ~apart ICBaseArr2 ()
  ~apart (ICArr1 x) TCRefl = ~apart x TCRefl
  ~apart (ICArr1 x) (TCArr y y₁) = ~apart x y
  ~apart (ICArr2 x) TCRefl = ~apart x TCRefl
  ~apart (ICArr2 x) (TCArr y y₁) = ~apart x y₁

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.List where

open import Data.Star
open import Data.Unit
open import Relation.Binary.Simple
open import Data.Star.Nat

-- Lists.

List : Set → Set
List a = Star (Const a) tt tt

-- Nil and cons.

[] : ∀ {a} → List a
[] = ε

infixr 5 _∷_

_∷_ : ∀ {a} → a → List a → List a
_∷_ = _◅_

-- The sum of the elements in a list containing natural numbers.

sum : List ℕ → ℕ
sum = fold (Star Always) _+_ zero


text:
open import Agda.Builtin.Sigma

dup : ∀ {A : Set} → A → Σ A λ _ → A
dup x = x , x

postulate
  A : Set

module M {x : A} where
  y = x

data X : Set where
  mkX : ∀ {x : A}
    → let
        (_ , _) = dup x
        open M {x}
      in
      X

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module MissingDefinition where

T : Set -> Set

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Base

module Spaces.WedgeCircles {i} (A : Set i) where

{-
The idea is

data wedge-circles : Set (suc i) where
  base : wedge-circles
  loops : A → base ≡ base
-}

private
  data #wedge-circles : Set (suc i) where
    #base : #wedge-circles

wedge-circles : Set (suc i)
wedge-circles = #wedge-circles

base : wedge-circles
base = #base

postulate  -- HIT
  loops : A → base ≡ base

wedge-circles-rec : ∀ {i} (P : wedge-circles → Set i) (x : P base)
  (p : (t : A) → transport P (loops t) x ≡ x) → ((t : wedge-circles) → P t)
wedge-circles-rec P x p #base = x

postulate  -- HIT
  β : ∀ {i} (P : wedge-circles → Set i) (x : P base)
      (p : (t : A) → transport P (loops t) x ≡ x) (t : A)
      → apd (wedge-circles-rec P x p) (loops t) ≡ p t

wedge-circles-rec-nondep : ∀ {i} (B : Set i) (x : B) (p : A → x ≡ x)
  → (wedge-circles → B)
wedge-circles-rec-nondep B x p #base = x

postulate  -- HIT
  β-nondep : ∀ {i} (B : Set i) (x : B) (p : A → x ≡ x) (t : A)
      → ap (wedge-circles-rec-nondep B x p) (loops t) ≡ p t

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Categories.Category

-- we use duality to prove properties about coequalizer
module Categories.Diagram.Coequalizer.Properties {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Categories.Diagram.Coequalizer C using (Coequalizer; IsCoequalizer)
open import Categories.Morphism C
import Categories.Morphism.Reasoning as MR
open import Categories.Diagram.Equalizer op
open import Categories.Diagram.Equalizer.Properties op
open import Categories.Diagram.Duality C
open import Categories.Diagram.KernelPair C
open import Categories.Diagram.Pullback C
open import Categories.Morphism.Regular C

import Relation.Binary.Reasoning.Setoid as SR

open Pullback hiding (universal; unique)

private
  variable
    A B : Obj
    f g : A ⇒ B

module _ (coe : Coequalizer f g) where
  open Coequalizer coe

  private
    equalizer : Equalizer f g
    equalizer = Coequalizer⇒coEqualizer coe

  open Equalizer equalizer
    using (unique′; unique-diagram)
    renaming ( id-equalize      to id-coequalize
             ; equalize-resp-≈  to coequalize-resp-≈
             ; equalize-resp-≈′ to coequalize-resp-≈′
             )
    public

-- a regular epi is a coequalizer of its kernel pair
regular-is-coeq-kp : {A B : Obj} (f : A ⇒ B) → RegularEpi f → (kp : KernelPair f) → IsCoequalizer (p₁ kp) (p₂ kp) f
regular-is-coeq-kp {A} {B} f record { C = D ; h = h ; g = g ; coequalizer = coeq } kp = record
  { equality   = IsPullback.commute (isPullback kp)
  ; coequalize = λ {_}{u} u∘p₁≈u∘p₂ → coequalize (u∘h≈u∘g u u∘p₁≈u∘p₂)
  ; universal  = universal
  ; unique     = unique
  }

  where
    open IsCoequalizer coeq
    pb-univ : D ⇒ P kp
    pb-univ = IsPullback.universal (isPullback kp) equality

    u∘h≈u∘g : {X : Obj} → (u : A ⇒ X) → u ∘ (p₁ kp) ≈ u ∘ (p₂ kp) → u ∘ h ≈ u ∘ g
    u∘h≈u∘g {X} u u∘p₁≈u∘p₂ = begin
      u ∘ h                   ≈˘⟨ refl⟩∘⟨ p₁∘universal≈h₁ kp ⟩
      u ∘ (p₁ kp  ∘ pb-univ)  ≈⟨ pullˡ u∘p₁≈u∘p₂ ⟩
      (u ∘ p₂ kp) ∘ pb-univ   ≈⟨ pullʳ (p₂∘universal≈h₂ kp) ⟩
      u ∘ g                   ∎
      where
        open Category.HomReasoning C
        open MR C

retract-coequalizer : ∀ {X Y} {f : Y ⇒ X} {g : X ⇒ Y} → f RetractOf g → IsCoequalizer (g ∘ f) id f
retract-coequalizer f∘g≈id = IscoEqualizer⇒IsCoequalizer (section-equalizer f∘g≈id)

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


text:
------------------------------------------------------------------------------
-- Properties related with lists using instances of the induction principle
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.List.Induction.Instances.PropertiesATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Totality properties

lengthList-N-ind-instance :
  N (length []) →
  (∀ x {xs} → N (length xs) → N (length (x ∷ xs))) →
  ∀ {xs} → List xs → N (length xs)
lengthList-N-ind-instance = List-ind (λ as → N (length as))

postulate lengthList-N : ∀ {xs} → List xs → N (length xs)
{-# ATP prove lengthList-N lengthList-N-ind-instance #-}

++-List-ind-instance :
  ∀ {ys} →
  List ([] ++ ys) →
  (∀ x {xs} → List (xs ++ ys) → List ((x ∷ xs) ++ ys)) →
  ∀ {xs} → List xs → List (xs ++ ys)
++-List-ind-instance {ys} = List-ind (λ as → List (as ++ ys))

postulate ++-List : ∀ {xs ys} → List xs → List ys → List (xs ++ ys)
{-# ATP prove ++-List ++-List-ind-instance #-}

map-List-ind-instance :
  ∀ {f} →
  List (map f []) →
  (∀ x {xs} → List (map f xs) → List (map f (x ∷ xs))) →
  ∀ {xs} → List xs → List (map f xs)
map-List-ind-instance {f} = List-ind (λ as → List (map f as))

postulate map-List : ∀ f {xs} → List xs → List (map f xs)
{-# ATP prove map-List map-List-ind-instance #-}

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

++-assoc-ind-instance :
  ∀ {ys zs} →
  ([] ++ ys) ++ zs ≡ [] ++ ys ++ zs →
  (∀ x {xs} →
    (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs →
    ((x ∷ xs) ++ ys) ++ zs ≡ (x ∷ xs) ++ ys ++ zs) →
  ∀ {xs} → List xs → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
++-assoc-ind-instance {ys} {zs} =
  List-ind (λ as → (as ++ ys) ++ zs ≡ as ++ ys ++ zs )

postulate
  ++-assoc : ∀ {xs} → List xs → ∀ ys zs → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
{-# ATP prove ++-assoc ++-assoc-ind-instance #-}

map-++-ind-instance :
  ∀ {f} {ys} →
  map f ([] ++ ys) ≡ map f [] ++ map f ys →
  (∀ x {xs} → map f (xs ++ ys) ≡ map f xs ++ map f ys →
    map f ((x ∷ xs) ++ ys) ≡ map f (x ∷ xs) ++ map f ys) →
  ∀ {xs} → List xs → map f (xs ++ ys) ≡ map f xs ++ map f ys
map-++-ind-instance {f} {ys} =
  List-ind (λ as → map f (as ++ ys) ≡ map f as ++ map f ys)

postulate
  map-++ : ∀ f {xs} → List xs → ∀ ys →
           map f (xs ++ ys) ≡ map f xs ++ map f ys
{-# ATP prove map-++ map-++-ind-instance #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module plfa.part1.Bin where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _*_; _+_)
open import Data.Nat.Properties using (+-suc)

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩    = ⟨⟩ I
inc (b O) = b I
inc (b I) = (inc b) O

to : ℕ → Bin
to zero    = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin → ℕ
from ⟨⟩    = 0
from (b O) = 2 * from b
from (b I) = suc (2 * from b)

inc-suc-law : ∀ b → from (inc b) ≡ suc (from b)
inc-suc-law ⟨⟩ = refl
inc-suc-law (b O) = refl
inc-suc-law (b I) rewrite
    inc-suc-law b
  | +-suc (suc (from b)) ((from b) + 0) = refl

from-to-identity : ∀ n → from (to n) ≡ n
from-to-identity zero = refl
from-to-identity (suc n) rewrite
    inc-suc-law (to n)
  | from-to-identity n = refl


text:
module Oscar.Class.Equivalence where

open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transitivity
open import Oscar.Function
open import Oscar.Level

record Equivalence {a} {A : Set a} {ℓ} (_≋_ : A → A → Set ℓ) : Set (a ⊔ ℓ) where
  field
    ⦃ ′reflexivity ⦄ : Reflexivity _≋_
    ⦃ ′symmetry ⦄ : Symmetry _≋_
    ⦃ ′transitivity ⦄ : Transitivity _≋_

open Equivalence ⦃ … ⦄ public hiding (′reflexivity; ′symmetry; ′transitivity)

instance

  Equivalence⋆ : ∀
    {a} {A : Set a} {ℓ} {_≋_ : A → A → Set ℓ}
    ⦃ _ : Reflexivity _≋_ ⦄
    ⦃ _ : Symmetry _≋_ ⦄
    ⦃ _ : Transitivity _≋_ ⦄
    → Equivalence _≋_
  Equivalence.′reflexivity Equivalence⋆ = it
  Equivalence.′symmetry Equivalence⋆ = it
  Equivalence.′transitivity Equivalence⋆ = it


text:
module sv20.assign2.Second_old4 where

open import Data.Bool as Bool using (Bool; true; false; T; _∨_; _∧_)
--open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Level using (Level; _⊔_; 0ℓ) renaming (suc to lsuc)
--open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Function using (_∘_)
--import Relation.Binary.PropositionalEquality as Eq
--open Eq using (_≡_; refl; subst)

Subset : ∀ {α} (A : Set α) -> Set _
Subset A = A → Bool

_∈_ : ∀ {α} {A : Set α} → A → Subset A → Set
a ∈ p = T (p a)

--odd : Subset ℕ
--odd 0 = false
--odd 1 = true
--odd (suc (suc n)) = odd n
--
--_ : 3 ∈ odd
--_ = tt
--
--_ : Subset Set  -- I'm not actually sure, what this is
--_ = λ _ → true

-- _ : true ∈ odd -- Doesn't make sense. Type inference fails
--_ = ?

--∈or∉ : ∀ {A : Set} (SubA : Subset A) (a : A) → (a ∈ SubA) ⊎ ¬ (a ∈ SubA)
--∈or∉ subset a with subset a
--...              | true  = inj₁ tt
--...              | false = inj₂ ⊥-elim
--
--empty-⊥ : ∀ (sub : Subset ⊥) (a : ⊥) → ¬ (a ∈ sub)
--empty-⊥ _ ()

--¬⊥ : ∀ (A : Set) → ¬ (⊥ ∈ A)  -- doesn't make any sense
--¬⊥ = ?

Relation : ∀ {α β} (A : Set α) (B : Set β) → Set (α ⊔ β)
Relation A B = Subset (A × B)

--equalℕ : Relation ℕ ℕ
--equalℕ ⟨ zero    , zero    ⟩ = true
--equalℕ ⟨ zero    , (suc n) ⟩ = false
--equalℕ ⟨ (suc m) , zero    ⟩ = false
--equalℕ ⟨ (suc m) , (suc n) ⟩ = equalℕ ⟨ m , n ⟩

--_ : equalℕ ⟨ 3 , 4 ⟩ ≡ false
--_ = refl

_∪_ : ∀ {A : Set} → Subset A → Subset A → Subset A
A ∪ B = λ x → (A x) ∨ (B x)

_∩_ : ∀ {A : Set} → Subset A → Subset A → Subset A
A ∩ B = λ x → (A x) ∧ (B x)

_⊆_ : ∀ {A : Set} → Subset A → Subset A → Set
A ⊆ B = ∀ x → x ∈ A → x ∈ B

wholeSet : ∀ (A : Set) → Subset A
wholeSet _ = λ _ → true

--odd⊆ℕ : odd ⊆ wholeSet ℕ
----odd⊆ℕ zero ()
----odd⊆ℕ 1 tt = tt
----odd⊆ℕ (suc (suc n)) _ = tt
---- or, simply
--odd⊆ℕ _ _ = tt

-- In general
∀subset⊆set : ∀ {A : Set} {sub : Subset A} → sub ⊆ wholeSet A
∀subset⊆set = λ _ _ → tt

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A

record Range (A B : Set) : Set where
  field
    range : Relation A B → Subset B
    def : ∀ (rel : Relation A B) (b : B)
        → (∃[ a ] (⟨ a , b ⟩ ∈ rel))
          ⇔ (b ∈ range rel)

--lemma : ∀ {A B : Set}
--        (F G : Relation A B)
--        (b : B)
--      → ∃[ a ] (⟨ a , b ⟩ ∈ (F ∩ G))
--      → ∃[ a ] ((⟨ a , b ⟩ ∈ F) × (⟨ a , b ⟩ ∈ G))
--lemma f g b ⟨ a , f∩ga ⟩ with f ⟨ a , b ⟩ | g ⟨ a , b ⟩
--...                         | true        | true         = ⟨ ? , ⟨ ? , ? ⟩ ⟩
--...                         | true        | false        = ⊥-elim f∩ga
--...                         | false       | true         = ⊥-elim f∩ga
--...                         | false       | false        = ⊥-elim f∩ga
--
--module range-props {A B : Set} (rng : Range A B) where
--  range = Range.range rng
--  def   = Range.def rng
--
--  range-∩-⊆ : (F G : Relation A B)
--            → range (F ∩ G) ⊆ (range F ∩ range G)
--  range-∩-⊆ f g b = ?
--    where
--      --def-rngf-→ = _⇔_.to (def f b)
--
--      -- b ∈ range (f ∩ g) → ∃[ a ] (⟨ a , b ⟩ ∈ (f ∩ g))
--      def-rngf-← = _⇔_.from (def (f ∩ g) b)
--      -- b ∈ range (f ∩ g) → ∃[ a ] ((⟨ a , b ⟩ ∈ F) × (⟨ a , b ⟩ ∈ G))
--      lemma' = (lemma f g b) ∘ def-rngf-←

-- Class exercise
-- Dammit! All definitions of subset I have found for agda make this problem not a problem
exercise103a : ∀ {a} {A B : Subset a}
             → (∀ x → x ∈ A → x ∈ B)
             → A ⊆ B
exercise103a ∀x→x∈A→x∈B = ∀x→x∈A→x∈B


text:
-- Andreas, 2018-05-11, issue #3049 reported by Ulf
-- Positivity checker too optimistic about polarity of arguments
-- beyond the formal function arity.

-- Backwards-compatible version of the test case.

-- {-# OPTIONS -v tc.pos.args:100 #-}

module Issue3049 where

data Bool : Set where
  true false : Bool

T : Bool → Set₁
T true  = Set → Set
T false = Set

bad : ∀ b → T b
bad true   = λ A → A → A   -- negative A
bad false  = Bool

F : Bool → ∀ b → T b
F true  b       = bad b  -- is not (can't be) eta-expanded
F false true    = λ A → A
F false false   = Bool

-- Should fail positivity check:

data D : Set where
  nop : (b : Bool) → F b true D → D

data ⊥ : Set where

d : D
d = nop true (λ x → x)

!d : D → ⊥
!d (nop true  f) = !d (f d)
!d (nop false x) = !d x

loop : ⊥
loop = !d d


text:
-- Andreas, 2012-10-20
module Issue481NonExistentModule where

open import NonExistentModule Set
-- test the error message and location

max_stars_repo_name: np/agda-git-experiment


text:
module Haskell.Prim.Traversable where

open import Haskell.Prim
open import Haskell.Prim.Applicative
open import Haskell.Prim.Functor
open import Haskell.Prim.Foldable
open import Haskell.Prim.Monad
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Traversable

record Traversable (t : Set → Set) : Set₁ where
  field
    traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
    overlap ⦃ functor ⦄ : Functor t
    overlap ⦃ foldable ⦄ : Foldable t

  sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
  sequenceA = traverse id

  mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
  mapM = traverse

  sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
  sequence = sequenceA

open Traversable ⦃ ... ⦄ public

instance
  iTraversableList : Traversable List
  iTraversableList .traverse f []       = pure []
  iTraversableList .traverse f (x ∷ xs) = ⦇ f x ∷ traverse f xs ⦈

  iTraversableMaybe : Traversable Maybe
  iTraversableMaybe .traverse f Nothing  = pure Nothing
  iTraversableMaybe .traverse f (Just x) = Just <$> f x

  iTraversableEither : Traversable (Either a)
  iTraversableEither .traverse f (Left  x) = pure (Left x)
  iTraversableEither .traverse f (Right y) = Right <$> f y

  iTraversablePair : Traversable (a ×_)
  iTraversablePair .traverse f (x , y) = (x ,_) <$> f y


text:
open import Data.List using ( List ; [] ; _∷_ )
open import Data.List.Any using ( here ; there )
open import Data.Product using ( _,_ ; proj₁ ; proj₂ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Binary.PropositionalEquality using
  ( refl ; sym ; trans ; subst₂ )
open import Relation.Unary using ( _∈_ ; _⊆_ )
open import Web.Semantic.DL.ABox using
  ( ABox ; ε ; _,_ ; _∼_ ; ⟨ABox⟩ ; Assertions
  ; ⟨ABox⟩-resp-id ; ⟨ABox⟩-resp-∘ ; ⟨ABox⟩-resp-∘² )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; _,_ ; ⌊_⌋ ; ind ; _*_ )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _,_ )
open import Web.Semantic.DL.ABox.Model using
  ( _⊨a_ ; *-resp-⟨ABox⟩ ; ⊨a-resp-⊇ )
open import Web.Semantic.DL.Category.Object using
  ( Object ; _,_ ; IN ; fin ; iface )
open import Web.Semantic.DL.Category.Morphism using
  ( _⇒_ ; _,_ ; BN ; impl )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Integrity using
  ( Unique ; Mediator ; Initial ; _⊕_⊨_ ; _,_ )
open import Web.Semantic.DL.KB using ( _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox ; _,_ )
open import Web.Semantic.DL.TBox.Interp using
  ( _⊨_≈_ ; ≈-refl ; ≈-sym ; ≈-trans )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-refl ; ≲-image )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.Util using
  ( id ; _∘_ ; False ; tt ; ⊎-swap ; ⊎-assoc ; ⊎-assoc⁻¹ ; ⊎-unit₁ ; ⊎-unit₂
  ; _∈ˡ_ ; _⊕_⊕_ ; inode ; bnode ; enode )

module Web.Semantic.DL.Category.Wiring {Σ : Signature} where

wires : ∀ {X Y} → (Y → X) → List Y → ABox Σ (X ⊕ False ⊕ Y)
wires f [] = ε
wires f (y ∷ ys) = (inode (f y) ∼ enode y , wires f ys)

wires-≈ : ∀ {X Y y ys I} (f : Y → X) → (y ∈ˡ ys) → (I ⊨a wires f ys) →
  (⌊ I ⌋ ⊨ ind I (inode (f y)) ≈ ind I (enode y))
wires-≈ f (here refl)  (x≈y , xs≈ys) = x≈y
wires-≈ f (there y∈ys) (x≈y , xs≈ys) = wires-≈ f y∈ys xs≈ys

wires-≈⁻¹ : ∀ {X Y I} (f : Y → X) →
  (∀ y → ⌊ I ⌋ ⊨ ind I (inode (f y)) ≈ ind I (enode y)) →
    ∀ ys → (I ⊨a wires f ys)
wires-≈⁻¹ f ∀y∙x≈y []       = tt
wires-≈⁻¹ f ∀y∙x≈y (y ∷ ys) = (∀y∙x≈y y , wires-≈⁻¹ f ∀y∙x≈y ys)

wired : ∀ {X Y} → (Y → X) → (X ⊕ False ⊕ Y) → X
wired f (inode x) = x
wired f (bnode ())
wired f (enode y) = f y

wired-init : ∀ {X Y} (f : Y → X) ys → (∀ y → y ∈ˡ ys) →
  (I : Interp Σ X) → (S : TBox Σ) → (⌊ I ⌋ ⊨t S) →
    (wired f * I ∈ Initial I (S , wires f ys))
wired-init f ys ∀y∙y∈ys (I , i) S I⊨S =
  ( (≲-refl I , λ x → ≈-refl I)
  , (I⊨S , wires-≈⁻¹ f (λ x → ≈-refl I) ys)
  , mediator ) where

  mediator : Mediator (I , i) (I , i ∘ wired f)
    (≲-refl I , λ x → ≈-refl I) (S , wires f ys)
  mediator (K , k) (I≲K , i≲k) (K⊨S , K⊨F) =
    ((I≲K , j≲k) , (λ x → ≈-refl K) , uniq ) where

    j≲k : ∀ x → K ⊨ ≲-image I≲K (i (wired f x)) ≈ k x
    j≲k (inode x) = i≲k x
    j≲k (bnode ())
    j≲k (enode y) = ≈-trans K (i≲k (f y)) (wires-≈ f (∀y∙y∈ys y) K⊨F)

    uniq : Unique (I , i) (I , i ∘ wired f) (K , k)
      (≲-refl I , λ x → ≈-refl I) (I≲K , i≲k)
    uniq J≲₁K J≲₂K I≲K≋I≲J≲₁K I≲K≋I≲J≲₂K x =
      ≈-trans K (≈-sym K (I≲K≋I≲J≲₁K x)) (I≲K≋I≲J≲₂K x)

wires✓ : ∀ {X Y ys} (f : Y → X) → (∀ y → y ∈ˡ ys) →
  (S T : TBox Σ) (A : ABox Σ X) (B : ABox Σ Y) →
    (Assertions (⟨ABox⟩ f B) ⊆ Assertions A) →
      (I : Interp Σ X) → (I ⊨ (S , T) , A) → (I ⊕ S , wires f ys ⊨ T , B)
wires✓ {X} {Y} {ys} f ∀y∙y∈ys S T A B B⊆A I I⊨STA =
  (J , J-init , (J⊨T , J⊨B)) where

  J : Interp Σ (X ⊕ False ⊕ Y)
  J = wired f * I

  J⊨T : ⌊ J ⌋ ⊨t T
  J⊨T = proj₂ (proj₁ I⊨STA)

  J⊨B : enode * J ⊨a B
  J⊨B = *-resp-⟨ABox⟩ f I B (⊨a-resp-⊇ I (⟨ABox⟩ f B) A B⊆A (proj₂ I⊨STA))

  J-init : J ∈ Initial I (S , wires f ys)
  J-init = wired-init f ys ∀y∙y∈ys I S (proj₁ (proj₁ I⊨STA))

wiring-impl : ∀ {S T : TBox Σ} → (A B : Object S T) (f : IN B → IN A) →
  ABox Σ (IN A ⊕ False ⊕ IN B)
wiring-impl A B f =
  wires f (proj₁ (fin B))

wiring-impl✓ : ∀ {S T : TBox Σ} → (A B : Object S T) (f : IN B → IN A) →
  (Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) →
    ∀ I → (I ⊨ (S , T) , iface A) → (I ⊕ (S , wiring-impl A B f) ⊨ (T , iface B))
wiring-impl✓ {S} {T} (X , X∈Fin , A) (Y , Y∈Fin , B) f B⊆A =
  wires✓ f (proj₂ Y∈Fin) S T A B B⊆A

wiring : ∀ {S T : TBox Σ} → (A B : Object S T) (f : IN B → IN A) →
  (Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) →
    (A ⇒ B)
wiring A B f B⊆A =
  ( False , wiring-impl A B f , wiring-impl✓ A B f B⊆A )

id✓ : ∀ {S T : TBox Σ} → (A : Object S T) →
  (Assertions (⟨ABox⟩ id (iface A)) ⊆ Assertions (iface A))
id✓ A = subst₂ Assertions (⟨ABox⟩-resp-id (iface A)) refl

identity : ∀ {S T : TBox Σ} → (A : Object S T) → (A ⇒ A)
identity A = wiring A A id (id✓ A)

⊎-swap✓ : ∀ {S T : TBox Σ} → (A B : Object S T) →
  Assertions (⟨ABox⟩ ⊎-swap (iface (B ⊗ A))) ⊆ Assertions (iface (A ⊗ B))
⊎-swap✓ A B (inj₁ b∈B) =
  inj₂ (subst₂ Assertions (⟨ABox⟩-resp-∘ ⊎-swap inj₁ (iface B)) refl b∈B)
⊎-swap✓ A B (inj₂ a∈A) =
  inj₁ (subst₂ Assertions (⟨ABox⟩-resp-∘ ⊎-swap inj₂ (iface A)) refl a∈A)

symm : ∀ {S T : TBox Σ} → (A B : Object S T) → ((A ⊗ B) ⇒ (B ⊗ A))
symm A B = wiring (A ⊗ B) (B ⊗ A) ⊎-swap (⊎-swap✓ A B)

⊎-assoc⁻¹✓ : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  (Assertions (⟨ABox⟩ ⊎-assoc⁻¹ (iface (A ⊗ (B ⊗ C))))) ⊆
    (Assertions (iface ((A ⊗ B) ⊗ C)))
⊎-assoc⁻¹✓ A B C (inj₁ a∈A) = inj₁ (inj₁ (subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘ ⊎-assoc⁻¹ inj₁ (iface A))
    (sym (⟨ABox⟩-resp-∘ inj₁ inj₁ (iface A))))
  refl a∈A))
⊎-assoc⁻¹✓ A B C (inj₂ (inj₁ b∈B)) = inj₁ (inj₂ (subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘² ⊎-assoc⁻¹ inj₂ inj₁ (iface B))
    (sym (⟨ABox⟩-resp-∘ inj₁ inj₂ (iface B))))
  refl b∈B))
⊎-assoc⁻¹✓ A B C (inj₂ (inj₂ c∈C)) = inj₂ (subst₂ Assertions
  (⟨ABox⟩-resp-∘² ⊎-assoc⁻¹ inj₂ inj₂ (iface C))
  refl c∈C)

assoc : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  (((A ⊗ B) ⊗ C) ⇒ (A ⊗ (B ⊗ C)))
assoc A B C = wiring ((A ⊗ B) ⊗ C) (A ⊗ (B ⊗ C)) ⊎-assoc⁻¹ (⊎-assoc⁻¹✓ A B C)

⊎-assoc✓ : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  (Assertions (⟨ABox⟩ ⊎-assoc (iface ((A ⊗ B) ⊗ C)))) ⊆
    (Assertions (iface (A ⊗ (B ⊗ C))))
⊎-assoc✓ A B C (inj₁ (inj₁ a∈A)) = inj₁ (subst₂ Assertions
  (⟨ABox⟩-resp-∘² ⊎-assoc inj₁ inj₁ (iface A))
  refl a∈A)
⊎-assoc✓ A B C (inj₁ (inj₂ b∈B)) = inj₂ (inj₁ (subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘² ⊎-assoc inj₁ inj₂ (iface B))
    (sym (⟨ABox⟩-resp-∘ inj₂ inj₁ (iface B))))
  refl b∈B))
⊎-assoc✓ A B C (inj₂ c∈C) = inj₂ (inj₂ (subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘ ⊎-assoc inj₂ (iface C))
    (sym (⟨ABox⟩-resp-∘ inj₂ inj₂ (iface C))))
  refl c∈C))

assoc⁻¹ : ∀ {S T : TBox Σ} → (A B C : Object S T) →
  ((A ⊗ (B ⊗ C)) ⇒ ((A ⊗ B) ⊗ C))
assoc⁻¹ A B C = wiring (A ⊗ (B ⊗ C)) ((A ⊗ B) ⊗ C) ⊎-assoc (⊎-assoc✓ A B C)

inj₂✓ : ∀ {S T : TBox Σ} → (A : Object S T) →
  (Assertions (⟨ABox⟩ inj₂ (iface A))) ⊆
    (Assertions (iface (I ⊗ A)))
inj₂✓ A = inj₂

unit₁ : ∀ {S T : TBox Σ} (A : Object S T) → ((I ⊗ A) ⇒ A)
unit₁ A = wiring (I ⊗ A) A inj₂ (inj₂✓ A)

⊎-unit₁✓ : ∀ {S T : TBox Σ} → (A : Object S T) →
  Assertions (⟨ABox⟩ ⊎-unit₁ (iface (I ⊗ A))) ⊆ Assertions (iface A)
⊎-unit₁✓ A (inj₁ ())
⊎-unit₁✓ A (inj₂ a∈A) = subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘ ⊎-unit₁ inj₂ (iface A)) (⟨ABox⟩-resp-id (iface A)))
  refl a∈A

unit₁⁻¹ : ∀ {S T : TBox Σ} (A : Object S T) → (A ⇒ (I ⊗ A))
unit₁⁻¹ A = wiring A (I ⊗ A) ⊎-unit₁ (⊎-unit₁✓ A)

inj₁✓ : ∀ {S T : TBox Σ} → (A : Object S T) →
  (Assertions (⟨ABox⟩ inj₁ (iface A))) ⊆
    (Assertions (iface (A ⊗ I)))
inj₁✓ A = inj₁

unit₂ : ∀ {S T : TBox Σ} (A : Object S T) → ((A ⊗ I) ⇒ A)
unit₂ A = wiring (A ⊗ I) A inj₁ (inj₁✓ A)

⊎-unit₂✓ : ∀ {S T : TBox Σ} (A : Object S T) →
  Assertions (⟨ABox⟩ ⊎-unit₂ (iface (A ⊗ I))) ⊆ Assertions (iface A)
⊎-unit₂✓ A (inj₁ a∈A) = subst₂ Assertions
  (trans (⟨ABox⟩-resp-∘ ⊎-unit₂ inj₁ (iface A)) (⟨ABox⟩-resp-id (iface A)))
  refl a∈A
⊎-unit₂✓ A (inj₂ ())

unit₂⁻¹ : ∀ {S T : TBox Σ} (A : Object S T) → (A ⇒ (A ⊗ I))
unit₂⁻¹ A = wiring A (A ⊗ I) ⊎-unit₂ (⊎-unit₂✓ A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module _ where

module Test₁ where

  module A where

    infixl 0 _+_

    data D : Set where
      •   : D
      _+_ : D → D → D

  module B where

    data D : Set where
      •   : D
      _+_ : D → D → D

  open A
  open B

  Foo : A.D
  Foo = • + • + •

module Test₂ where

  module A where

    data D : Set where
      •   : D
      _+_ : D → D → D

  module B where

    data D : Set where
      •   : D
      _+_ : D → D → D

  open A
  open B

  Foo : A.D
  Foo = • + •

module Test₃ where

  module A where

    data D : Set where
      • : D
      c : D → D → D

    syntax c x y = x + y

  module B where

    data D : Set where
      • : D
      c : D → D → D

    syntax c x y = x + y

  open A
  open B

  Foo : A.D
  Foo = • + •


text:
postulate
  A : Set
  B : Set
  t : B

data C : (b : B) → Set

foo : (b : B) → C b → B

data C where
  c : (x : C t) → C (foo t x)

foo b x = {!x!}


text:
module Syntax.Implication.Dependent where

open import Functional using (id)
open import Functional.Dependent
import      Lvl
open import Type

private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level

_⇒-[_]_ : ∀(X : Type{ℓ₁}){Y : ∀{_ : X} → Type{ℓ₂}}{Z : ∀{x : X}{_ : Y{x}} → Type{ℓ₃}} → (P : (x : X) → Y{x}) → (∀{x : X} → (y : Y{x}) → Z{x}{y}) → ((x : X) → Z{x}{P(x)})
_⇒-[_]_ = const(swap(_∘_))
infixr 0.98 _⇒-[_]_
{-# INLINE _⇒-[_]_ #-}

_⇒-[]_ : ∀(X : Type{ℓ₁}){Y : ∀{_ : X} → Type{ℓ₂}} → ((x : X) → Y{x}) → ((x : X) → Y{x})
_⇒-[]_ = const id
infixr 0.98 _⇒-[]_
{-# INLINE _⇒-[]_ #-}

_⇒-end : ∀(X : Type{ℓ₁}) → (X → X)
_⇒-end = const id
infixr 0.99 _⇒-end
{-# INLINE _⇒-end #-}

_⇒_ = apply
infixl 0.97 _⇒_
{-# INLINE _⇒_ #-}

-- TODO: Change these to be similar to the ones in Syntax.Implication
•_⇒₁_ = apply
infixl 0.97 •_⇒₁_
{-# INLINE •_⇒₁_ #-}

•_•_⇒₂_ : ∀{X : Type{ℓ₁}}{Y : ∀{_ : X} → Type{ℓ₂}}{Z : ∀{x : X}{_ : Y{x}} → Type{ℓ₃}} → (x : X) → (y : Y{x}) → ((x : X) → (y : Y{x}) → Z{x}{y}) → Z{x}{y}
• a • b ⇒₂ P = P ⇒ apply a ⇒ apply b
infixl 0.97 •_•_⇒₂_
{-# INLINE •_•_⇒₂_ #-}

•_•_•_⇒₃_ : ∀{X : Type{ℓ₁}}{Y : ∀{_ : X} → Type{ℓ₂}}{Z : ∀{x : X}{_ : Y{x}} → Type{ℓ₃}}{W : ∀{x : X}{y : Y{x}}{_ : Z{x}{y}} → Type{ℓ₄}} → (x : X) → (y : Y{x}) → (z : Z{x}{y}) → ((x : X) → (y : Y{x}) → (z : Z{x}{y}) → W{x}{y}{z}) → W{x}{y}{z}
• a • b • c ⇒₃ P = P ⇒ apply a ⇒ apply b ⇒ apply c
infixl 0.97 •_•_•_⇒₃_
{-# INLINE •_•_•_⇒₃_ #-}

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 Numeral.Natural.Oper where

open import Numeral.Natural

infixl 10010 _+_
infix  10010 _−₀_ _𝄩_
infixl 10020 _⋅_
-- infix  10020 _/₀_
infixl 10030 _^_

-- TODO: It would require a great amount of work, but consider changing the induction to being on the left side instead of the right on _+_ and _⋅_. It will then mirror how lists (a similar structure) uses induction in its definition. The advantage of having it on the right side as it is now is that induction using the full operator name is easier: ℕ-induction(_+_ a) vs ℕ-induction(a ↦ _+_ a b)

-- Addition
_+_ : ℕ → ℕ → ℕ
x + 𝟎 = x
x + 𝐒(y) = 𝐒(x + y)
{-# BUILTIN NATPLUS _+_ #-}

-- Multiplication
_⋅_ : ℕ → ℕ → ℕ
_ ⋅ 𝟎 = 𝟎
x ⋅ 𝐒(y) = x + (x ⋅ y)
{-# BUILTIN NATTIMES _⋅_ #-}

-- Exponentiation
_^_ : ℕ → ℕ → ℕ
x ^ 𝟎 = 𝐒(𝟎)
x ^ 𝐒(y) = x ⋅ (x ^ y)

-- Factorial
_! : ℕ → ℕ
𝟎 ! = 𝐒(𝟎)
𝐒(x) ! = 𝐒(x) ⋅ (x !)

-- Distance (Absolute subtraction) (Interval length)
_𝄩_ : ℕ → ℕ → ℕ
𝟎    𝄩 𝟎    = 𝟎
𝐒(x) 𝄩 𝟎    = 𝐒(x)
𝟎    𝄩 𝐒(x) = 𝐒(x)
𝐒(x) 𝄩 𝐒(y) = x 𝄩 y

-- Closed total subtraction (monus)
_−₀_ : ℕ → ℕ → ℕ
x    −₀ 𝟎    = x
𝟎    −₀ 𝐒(_) = 𝟎
𝐒(x) −₀ 𝐒(y) = x −₀ y
{-# BUILTIN NATMINUS _−₀_ #-}

-- Closed total ceiled division (rounding up)
{-# TERMINATING #-}
_⌈/₀⌉_ : ℕ → ℕ → ℕ
𝟎 ⌈/₀⌉ y = 𝟎
{-# CATCHALL #-}
x ⌈/₀⌉ 𝟎 = 𝟎
{-# CATCHALL #-}
x ⌈/₀⌉ y = 𝐒((x −₀ y) ⌈/₀⌉ y)

-- Hyperoperation: (a ↑[n]↑ b) where (n=0)⇒(_ ↦ 𝐒) , (n=1)⇒(+) , (n=2)⇒(⋅) , (n=3)⇒(^)
_↑[_]↑_ : ℕ → ℕ → ℕ → ℕ
_ ↑[ 0          ]↑ b = 𝐒(b)
a ↑[ 1          ]↑ 0 = a
_ ↑[ 2          ]↑ 0 = 0
_ ↑[ 𝐒(𝐒(𝐒(n))) ]↑ 0 = 1
{-# CATCHALL #-}
a ↑[ 𝐒(n)       ]↑ (𝐒(b)) = a ↑[ n ]↑ (a ↑[ n ]↑ b)


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

{- Here, truncations with propositional computational behaviour are defined.
   This lack of a definitional β-rule enabled us to talk about this notion
   inside type theory without truncations, albeit complicating setup and proofs.

   After definition and basic accessories concerning universal properties,
   recursion and elimination, we prove that truncation is functorial.
   With this, we turn our attention to the problem of uniqueness of truncation,
   i.e. the type of truncations of a given type being propositional. -}
module Universe.Trunc.Basics where

open import lib.Basics
open import lib.NType2
open import lib.Equivalences2
open import lib.types.Unit
open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Paths

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse
open import Universe.Trunc.Universal

-- *** Definition 6.4 ***
record trunc-ty {i} (n : ℕ₋₂) (A : Type i)
                (j : ULevel) : Type (lsucc (i ⊔ j)) where
  constructor ty-cons
  field
    type : n -Type i
    cons : A → ⟦ type ⟧
    univ : univ-Type type cons j

module _ {i} {n : ℕ₋₂} {A : Type i} where
  trunc-ty-lower : ∀ {j₀} (j₁ : ULevel) → trunc-ty n A (j₀ ⊔ j₁) → trunc-ty n A j₀
  trunc-ty-lower {j₀} j₁ (ty-cons t c u) = ty-cons t c (univ-lower t c (j₀ ⊔ j₁) u)

{- Since Agda does not support specifying ordering relations on universe levels,
   we encounter an awkward dependency inversion: the index k needs to be
   specified in the module arguments, since the truncation type depends on it,
   even though we would rather have it at each individual definition.
   This shortcoming will be the source of many explicitely specified levels. -}
module trunc-props {i} {n : ℕ₋₂} {A : Type i} {j k} (tr : trunc-ty n A (i ⊔ j ⊔ k)) where
  open trunc-ty tr

  up : (U : n -Type k) → (⟦ type ⟧ → ⟦ U ⟧) ≃ (A → ⟦ U ⟧)
  up U = ((λ f → f ∘ cons) , univ-lower type cons (i ⊔ j ⊔ k) univ U)

  dup : (U : ⟦ type ⟧ → n -Type k) → ((ta : ⟦ type ⟧) → ⟦ U ta ⟧) ≃ ((a : A) → ⟦ U (cons a) ⟧)
  dup U = ((λ f → f ∘ cons) , with-univ.duniv type cons (univ-lower type cons (i ⊔ j ⊔ k) univ) U)

  abstract
    rec : (U : n -Type k) → (A → ⟦ U ⟧) → ⟦ type ⟧ → ⟦ U ⟧
    rec U = <– (up U)

    elim : (U : ⟦ type ⟧ → n -Type k) → ((a : A) → ⟦ U (cons a) ⟧) → (ta : ⟦ type ⟧) → ⟦ U ta ⟧
    elim U = <– (dup U)

    rec-β : {U : n -Type k} {f : A → ⟦ U ⟧} (a : A) → rec U f (cons a) == f a
    rec-β {U} {f} a = app= (<–-inv-r (up U) f) a

    elim-β : {U : ⟦ type ⟧ → n -Type k} {f : (a : A) → ⟦ U (cons a) ⟧} (a : A) → elim U f (cons a) == f a
    elim-β {U} {f} a = app= (<–-inv-r (dup U) f) a

{- Truncation acts as a functor.
   While tedious, we state all lemmata in their most general form.
   Instead of assuming an n-truncation operator, we individually assume
   a truncation for each type we need. While seeming overly convoluted
   at first, this generality will actually pay off with an unconventional
   use of fmap-equiv in showing that trunc-ty is propositional. -}
module trunc-functor {n : ℕ₋₂} where
  open trunc-ty
  open trunc-props

  -- The functorial action of truncation (truncation preserves maps).
  module _ {ia ib j} where
    module fmap {A : Type ia} {B : Type ib}
                (TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
                (TrB : trunc-ty n B (ia ⊔ ib ⊔ j))
                (f : A → B) where
      map : ⟦ type TrA ⟧ → ⟦ type TrB ⟧
      map = rec {j = ia ⊔ ib ⊔ j} TrA (type TrB) (cons TrB ∘ f)

      β : (a : A) → map (cons TrA a) == cons TrB (f a)
      β = rec-β TrA {type TrB}

  -- The functorial action preserves the identity.
  module _ {i j} {A : Type i} (TrA : trunc-ty n A (i ⊔ j)) where
    private
      module I  = fmap {j = i ⊔ j} TrA TrA (idf _)

    fmap-fuse-id : (ta : ⟦ type TrA ⟧) → I.map ta == ta
    fmap-fuse-id = elim {j = i ⊔ j} TrA (λ ta → Path-≤ (type TrA) (I.map ta) ta) I.β

  -- The functorial action preserves composition.
  module _ {ia ib ic j} where
    private
      l : ULevel
      l = ia ⊔ ib ⊔ ic ⊔ j

    module _ {A : Type ia} {B : Type ib} {C : Type ic}
             (TrA : trunc-ty n A l)
             (TrB : trunc-ty n B l)
             (TrC : trunc-ty n C l)
             (f : A → B) (g : B → C) where
      private
        module F  = fmap {j = l} TrA TrB f
        module G  = fmap {j = l} TrB TrC g
        module GF = fmap {j = l} TrA TrC (g ∘ f)

      open trunc-props

      fmap-fuse-∘ : (ta : ⟦ type TrA ⟧) → GF.map ta == G.map (F.map ta)
      fmap-fuse-∘ = elim {j = l} TrA (λ ta →
                      Path-≤ (type TrC) (GF.map ta) (G.map (F.map ta))) $ λ a →
        GF.map (cons TrA a)        =⟨ GF.β a ⟩
        cons TrC (g (f a))         =⟨ ! (G.β (f a)) ⟩
        G.map (cons TrB (f a))     =⟨ ap G.map (! (F.β a)) ⟩
        G.map (F.map (cons TrA a)) ∎

  {- Corollary: truncation preserves equivalences.
     The below general form produces a unexpected benefit: the underlying
     type of a truncation is unique up to constructor-preserving equivalence. -}
  module _ where
    private
      module _ {ia ib j} where
        private
          l : ULevel
          l = ia ⊔ ib ⊔ j

        module half {A : Type ia} {B : Type ib}
                    (TrA : trunc-ty n A l)
                    (TrB : trunc-ty n B l)
                    (e : A ≃ B) where
          module F  = fmap {j = l} TrA TrB (–> e)
          module G  = fmap {j = l} TrB TrA (<– e)
          module BB = fmap {j = l} TrB TrB

          f-g : (tb : ⟦ type TrB ⟧) → F.map (G.map tb) == tb
          f-g tb =
              F.map (G.map tb)
            =⟨ ! (fmap-fuse-∘ {j = l} TrB TrA TrB (<– e) (–> e) tb) ⟩
              BB.map (–> e ∘ <– e) tb
            =⟨ app= (ap BB.map (λ= (<–-inv-r e))) tb ⟩
              BB.map (idf _) tb
            =⟨ fmap-fuse-id {j = l} TrB tb ⟩
              tb
            ∎

    module _ {ia ib j} where
      module _ {A : Type ia} {B : Type ib}
               (TrA : trunc-ty n A (ia ⊔ ib ⊔ j))
               (TrB : trunc-ty n B (ia ⊔ ib ⊔ j))
               (e : A ≃ B) where
        private
          module H = half {j = j} TrA TrB e
          module K = half {j = j} TrB TrA (e ⁻¹)

        fmap-equiv : ⟦ type TrA ≃-≤ type TrB ⟧
        fmap-equiv = equiv H.F.map K.F.map H.f-g K.f-g

{- The type of n-truncations of A is propositional:
   truncations are unique if existent. -}
module _ {i} {n : ℕ₋₂} {A : Type i} where
  open trunc-ty
  open trunc-functor

  {- For the purpose of this module, it will be easier
     for us to regard trunc-ty as a left-associatived Σ-type.
     In this way, we may examine the equality on the first component
     while disregarding the second one, which is a proposition. -}
  private
    e : ∀ {j} → trunc-ty n A j ≃ Σ (Σ _ _) _
    e = equiv (λ {(ty-cons t c u) → ((t , c) , u)})
              (λ {((t , c) , u) → ty-cons t c u})
              (λ _ → idp) (λ _ → idp)

    {- First, let us structurally decompose the combined equality
      over the type and cons record fields of trunc-ty.
      Note that this kind of lemma would be superfluous in
      a proof assistant fully supporting univalent foundations. -}
    path : (U V : Σ (n -Type i) (λ ty → A → ⟦ ty ⟧))
         → (U == V) ≃ Σ (⟦ fst U ⟧ ≃ ⟦ fst V ⟧) (λ e → –> e ∘ snd U == snd V)
    path ((X , u) , f) ((Y , v) , g) = equiv-Σ eq₁ (_⁻¹ ∘ eq₂)
                                     ∘e =Σ-eqv _ _ ⁻¹ where
      eq₁ : ((X , u) == (Y , v)) ≃ (X ≃ Y)
      eq₁ =
        (X , u) == (Y , v)                   ≃⟨ =Σ-eqv _ _ ⁻¹ ⟩
        Σ (X == Y) (λ p → u == v [ _ ↓ p ])  ≃⟨ Σ₂-contr h ⟩
        X == Y                               ≃⟨ ua-equiv ⁻¹ ⟩
        X ≃ Y                                ≃∎ where

        h : (p : X == Y) → is-contr (u == v [ _ ↓ p ])
        h _ = =-[-↓-]-level (λ _ → has-level-is-prop)

      eq₂ : (e : X ≃ Y) → (–> e ∘ f == g) ≃ (f == g [ _ ↓ <– eq₁ e ])
      eq₂ = λ e →
        –> e ∘ f == g                    ≃⟨ app=-equiv ⟩
        (∀ a → –> e (f a) == g a)        ≃⟨ equiv-Π-r (λ a → ↓-idf-ua-equiv e) ⟩
        (∀ a → f a == g a [ _ ↓ ua e ])  ≃⟨ ↓-cst→app-equiv ⟩
        (f == g [ _ ↓ ua e ])            ≃⟨ ↓-cst2-equiv _ _ ⟩
        (f == g [ _ ↓ <– eq₁ e ])        ≃∎

  module _ {j} where
    {- Important special case of the general form of fmap-equiv:
       the underlying type of a truncation is unique
       up to constructor-preserving equivalence. -}
    module unique (Tr₁ : trunc-ty n A (i ⊔ j))
                  (Tr₂ : trunc-ty n A (i ⊔ j)) where
      type-equiv : ⟦ type Tr₁ ≃-≤ type Tr₂ ⟧
      type-equiv = fmap-equiv {j = j} Tr₁ Tr₂ (ide _)

      cons-path : –> type-equiv ∘ cons Tr₁ == cons Tr₂
      cons-path = λ= (fmap.β {j = j} Tr₁ Tr₂ (idf _))

      type-cons-path : Path {A = Σ (n -Type i) (λ ty → A → ⟦ ty ⟧)}
                            (fst (–> e Tr₁)) (fst (–> e Tr₂))
      type-cons-path = <– (path _ _) (type-equiv , cons-path)

    -- *** Lemma 6.7 ***
    -- We are now ready to prove propositionality of trunc-ty.
    trunc-ty-prop : is-prop (trunc-ty n A _)
    trunc-ty-prop = all-paths-is-prop $ λ Tr₀ Tr₁ → <– (equiv-ap e _ _) (pair=
      (unique.type-cons-path Tr₀ Tr₁)
      (prop-has-all-paths-↓ (Π-level (λ _ → is-equiv-is-prop _))))

    trunc-inhab-contr : trunc-ty n A _ → is-contr (trunc-ty n A _)
    trunc-inhab-contr Tr = (Tr , prop-has-all-paths trunc-ty-prop _)

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
record _×_ (A B : Set) : Set where
  no-eta-equality
  constructor _,_
  field
    fst : A
    snd : B

open _×_

swap : ∀ {A B} → A × B → B × A
swap (x , y) = y , x

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

-- This should fail since we don't have eta for _×_.
fails : ∀ {A B} (p : A × B) → swap p ≡ (snd p , fst p)
fails p = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
-- Author: Makoto Takeyama

module ParenDepTac where

----------------------------------------------------------------------
-- Preliminary
----------------------------------------------------------------------

infix 3  _≡_
data _≡_ {A : Set}(x : A) : A -> Set where
  refl : x ≡ x

subst : {A : Set}(C : A -> Set){x y : A} -> x ≡ y -> C y -> C x
subst C refl c = c

sym : {A : Set}{x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

cong : {A B : Set}(f : A -> B){x y : A} -> x ≡ y -> f x ≡ f y
cong f refl = refl

infixl 2 _`tran`_
_`tran`_ : {A : Set}{x y z : A} -> x ≡ y -> y ≡ z -> x ≡ z
refl `tran` refl = refl

data FALSE : Set where
data TRUE  : Set where tt : TRUE

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

_+_ : Nat -> Nat -> Nat
zer   + n = n
suc m + n = suc ( m + n )

----------------------------------------------------------------------
-- Strings of parentheses
----------------------------------------------------------------------

infix 5 ≪_ ≫_
data Parens : Set where
  ε  : Parens
  ≪_ : Parens -> Parens
  ≫_ : Parens -> Parens

infixr 5 _·_

_·_ : Parens -> Parens -> Parens
ε    · ys = ys
≪ xs · ys = ≪ (xs · ys)
≫ xs · ys = ≫ (xs · ys)

·ass : (xs : Parens){ys zs : Parens} -> xs · (ys · zs) ≡ (xs · ys) · zs
·ass ε      = refl
·ass (≪ xs) = cong ≪_ (·ass xs)
·ass (≫ xs) = cong ≫_ (·ass xs)

·unitR : {xs : Parens} -> xs · ε ≡ xs
·unitR {ε}    = refl
·unitR {≪ xs} = cong ≪_ ·unitR
·unitR {≫ xs} = cong ≫_ ·unitR

_≫' : Parens -> Parens
xs ≫' = xs · ≫ ε
_≪' : Parens -> Parens
xs ≪' = xs · ≪ ε

----------------------------------------------------------------------
-- A poorman's tactics for equational reasoning
----------------------------------------------------------------------

infixr 5 _⊙_
data Exp : Set where
  Var : Nat    -> Exp
  Lit : Parens -> Exp
  _⊙_ : Exp -> Exp -> Exp

nf0 : Exp -> Exp -> Exp
nf0 (Var x)   e0 = Var x ⊙ e0
nf0 (Lit a)   e0 = Lit a ⊙ e0
nf0 (e1 ⊙ e2) e0 = nf0 e1 (nf0 e2 e0)

nf : Exp -> Exp
nf e = nf0 e (Lit ε)

Env = Nat -> Parens

module withEnv(ρ : Env) where

  ⟦_⟧ : Exp -> Parens
  ⟦ Var x   ⟧ = ρ x
  ⟦ Lit a   ⟧ = a
  ⟦ e1 ⊙ e2 ⟧ = ⟦ e1 ⟧ · ⟦ e2 ⟧

  nfSound0 : (e e0 : Exp) -> ⟦ e ⊙ e0 ⟧ ≡ ⟦ nf0 e e0 ⟧
  nfSound0 (Var x)   e0 = refl
  nfSound0 (Lit a)   e0 = refl
  nfSound0 (e1 ⊙ e2) e0 = sym (·ass ⟦ e1 ⟧) `tran`
                          cong (_·_ ⟦ e1 ⟧) (nfSound0 e2 e0)  `tran`
                          nfSound0 e1 (nf0 e2 e0)

  nfSound : (e : Exp) -> ⟦ e ⟧ ≡ ⟦ nf e ⟧
  nfSound e = sym ·unitR `tran` nfSound0 e (Lit ε)

  tac : (e1 e2 : Exp) -> nf e1 ≡ nf e2 -> ⟦ e1 ⟧ ≡ ⟦ e2 ⟧
  tac e1 e2 p = nfSound e1 `tran` subst (\x -> ⟦ x ⟧ ≡ ⟦ nf e2 ⟧) p refl `tran`
                sym (nfSound e2)

module tac4 (a0 a1 a2 a3 : Parens) where
  ρ : Env
  ρ zer                         = a0
  ρ (suc zer)                   = a1
  ρ (suc (suc zer))             = a2
  ρ (suc (suc (suc zer)))       = a3
  ρ (suc (suc (suc (suc _  )))) = ε
  open module tac4' = withEnv ρ public using (tac)

v0 = Var zer
v1 = Var (suc zer)
v2 = Var (suc (suc zer))
v3 = Var (suc (suc (suc zer)))
[≪] = Lit (≪ ε)
[≫] = Lit (≫ ε)

----------------------------------------------------------------------
-- Derivations of S and T grammars
--     indexed by their underlying strings
----------------------------------------------------------------------

infix  3 _∈S _∈T
infix  4 <_> _⟨_⟩
infixl 4 _•_

data  _∈S : Parens -> Set where
  εS  : ε ∈S
  <_> : {xs    : Parens} -> xs ∈S -> ≪ xs ≫' ∈S
  _•_ : {xs ys : Parens} -> xs ∈S -> ys ∈S -> xs · ys ∈S

data _∈T : Parens -> Set where
  εT   : ε ∈T
  _⟨_⟩ : {xs ys : Parens} -> xs ∈T -> ys ∈T -> xs · ≪ ys ≫' ∈T

----------------------------------------------------------------------
-- Equivalence of S and T grammars
----------------------------------------------------------------------

infixl 3 _○_
_○_ : {xs ys : Parens} -> xs ∈T -> ys ∈T -> xs · ys ∈T
t ○ εT                 = subst _∈T ·unitR    t
_○_ {xs} t (t1 ⟨ t2 ⟩) = subst _∈T (·ass xs) ((t ○ t1) ⟨ t2 ⟩)

S⊂T : {xs : Parens} -> xs ∈S -> xs ∈T
S⊂T εS        = εT
S⊂T (< s >)   = εT ⟨ S⊂T s ⟩
S⊂T (s1 • s2) = S⊂T s1 ○ S⊂T s2

T⊂S : {xs : Parens} -> xs ∈T -> xs ∈S
T⊂S εT          = εS
T⊂S (t1 ⟨ t2 ⟩) = T⊂S t1 • < T⊂S t2 >

----------------------------------------------------------------------
-- Recursively defined test function
----------------------------------------------------------------------

Test : Nat -> Parens -> Set
Test n       (≪ xs) = Test (suc n) xs
Test (suc n) (≫ xs) = Test n       xs
Test zer     (≫ xs) = FALSE
Test (suc n)  ε     = FALSE
Test zer      ε     = TRUE

----------------------------------------------------------------------
-- Soundness of Test
----------------------------------------------------------------------

lemTest : (m : Nat)(xs : Parens) -> Test m xs ->
          (n : Nat)(ys : Parens) -> Test n ys ->
          Test (m + n) (xs · ys)
lemTest m       (≪ xs) p  = lemTest (suc m) xs p
lemTest (suc m) (≫ xs) p  = lemTest m       xs p
lemTest zer     (≫ xs) ()
lemTest (suc m) ε      ()
lemTest zer     ε      tt = \ n ys q -> q

sound : {xs : Parens} -> xs ∈S -> Test zer xs
sound εS                  = tt
sound (<_>{xs} s)         = lemTest zer xs (sound s) (suc zer) (≫ ε) tt
sound (_•_{xs}{ys} s1 s2) = lemTest zer xs (sound s1) zer ys (sound s2)

----------------------------------------------------------------------
-- Completeness of Test
----------------------------------------------------------------------

complete : (xs : Parens) -> Test zer xs -> xs ∈S
complete xs0 p0 = parse init εS xs0 p0
  where
  data St : Nat -> Parens -> Set where
    init : St zer ε
    _*_≪ : {n  : Nat} ->
           {xs : Parens} -> St n xs ->
           {ys : Parens} -> ys ∈S   ->
           St (suc n) (xs · ys ≪')

  stPar : forall {n xs} -> St n xs -> Parens
  stPar {xs = xs} _ = xs

  ∈SPar : forall {xs} -> xs ∈S -> Parens
  ∈SPar {xs} _ = xs

  parse : {n  : Nat} ->
          {xs : Parens} -> St n xs   ->
          {ys : Parens} -> ys ∈S     ->
          (zs : Parens) -> Test n zs ->
          xs · ys · zs ∈S

  -- <SHIFT>  (st        ,  s ,  ≪ zs )  ↦  (st * s ≪ , εS         , zs)
  -- <REDUCE> (st * s3 ≪ ,  s ,  ≫ zs )  ↦  (st       , s3 • < s > , zs)
  -- <FINISH> (init      ,  s ,  ε    )  ↦  s

  parse {_} {xs} st {ys} s (≪ zs) p = subst _∈S eq (parse (st * s ≪) εS zs p)
    where open module foo = tac4 xs ys zs ε
          eq = tac (v0 ⊙ v1 ⊙ [≪]  ⊙ v2) ((v0 ⊙ v1 ⊙ [≪]) ⊙ v2) refl

  parse (st * s3 ≪) {ys} s (≫ zs) p
                                    = subst _∈S eq (parse st (s3 • < s >) zs p)
    where open module foo = tac4 (stPar st) (∈SPar s3) ys zs
          eq = tac ((v0 ⊙  v1 ⊙ [≪]) ⊙ v2 ⊙ [≫]  ⊙ v3)
                   ( v0 ⊙ (v1 ⊙ [≪]  ⊙ v2 ⊙ [≫]) ⊙ v3) refl

  parse ( _ * _ ≪) _ ε      ()

  parse init       _ (≫ zs) ()
  parse init       s ε      tt = subst _∈S ·unitR s

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso