text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Functions
------------------------------------------------------------------------

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

module Function.Nary.NonDependent where

------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------

open import Level using (Level; 0ℓ; _⊔_; Lift)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Product using (_×_; _,_)
open import Data.Product.Nary.NonDependent
open import Function.Base using (_∘′_; _$′_; const; flip)
open import Relation.Unary using (IUniversal)
open import Relation.Binary.PropositionalEquality

private
  variable
    a b r : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Re-exporting the basic operations

open import Function.Nary.NonDependent.Base public

------------------------------------------------------------------------
-- Additional operations on Levels

ltabulate : ∀ n → (Fin n → Level) → Levels n
ltabulate zero    f = _
ltabulate (suc n) f = f zero , ltabulate n (f ∘′ suc)

lreplicate : ∀ n → Level → Levels n
lreplicate n ℓ = ltabulate n (const ℓ)

0ℓs : ∀[ Levels ]
0ℓs = lreplicate _ 0ℓ

------------------------------------------------------------------------
-- Congruence

module _ n {ls} {as : Sets n ls} {R : Set r} (f : as ⇉ R) where

  private
    g : Product n as → R
    g = uncurryₙ n f

-- Congruentₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--                   a₁₁ ≡ a₁₂ → ⋯ → aₙ₁ ≡ aₙ₂ →
--                   f a₁₁ ⋯ aₙ₁ ≡ f a₁₂ ⋯ aₙ₂

  Congruentₙ : Set (r Level.⊔ ⨆ n ls)
  Congruentₙ = ∀ {l r} → Equalₙ n l r ⇉ (g l ≡ g r)

  congₙ : Congruentₙ
  congₙ = curryₙ n (cong g ∘′ fromEqualₙ n)

-- Congruence at a specific location

module _ m n {ls ls'} {as : Sets m ls} {bs : Sets n ls'}
         (f : as ⇉ (A → bs ⇉ B)) where

  private
    g : Product m as → A → Product n bs → B
    g vs a ws = uncurryₙ n (uncurryₙ m f vs a) ws

  congAt : ∀ {vs ws a₁ a₂} → a₁ ≡ a₂ → g vs a₁ ws ≡ g vs a₂ ws
  congAt {vs} {ws} = cong (λ a → g vs a ws)

------------------------------------------------------------------------
-- Injectivity

module _ n {ls} {as : Sets n ls} {R : Set r} (con : as ⇉ R) where

-- Injectiveₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--                   con a₁₁ ⋯ aₙ₁ ≡ con a₁₂ ⋯ aₙ₂ →
--                   a₁₁ ≡ a₁₂ × ⋯ × aₙ₁ ≡ aₙ₂

  private
    c : Product n as → R
    c = uncurryₙ n con

  Injectiveₙ : Set (r Level.⊔ ⨆ n ls)
  Injectiveₙ = ∀ {l r} → c l ≡ c r → Product n (Equalₙ n l r)

  injectiveₙ : (∀ {l r} → c l ≡ c r → l ≡ r) → Injectiveₙ
  injectiveₙ con-inj eq = toEqualₙ n (con-inj eq)


text:
{-

  Functions building UARels and DUARels on Σ-types

-}
{-# OPTIONS --safe #-}
module Cubical.Displayed.Sigma where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Subst
open import Cubical.Displayed.Morphism
open import Cubical.Displayed.Constant

private
  variable
    ℓ ℓA ℓA' ℓP ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C : Level

-- UARel on a Σ-type

∫ˢ : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
  → UARel (Σ A B) (ℓ-max ℓ≅A ℓB)
∫ˢ 𝒮ˢ-B = ∫ (Subst→DUA 𝒮ˢ-B)

_×𝒮_ : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) {B : Type ℓB} (𝒮-B : UARel B ℓ≅B)
  → UARel (A × B) (ℓ-max ℓ≅A ℓ≅B)
𝒮-A ×𝒮 𝒮-B = ∫ (𝒮ᴰ-const 𝒮-A 𝒮-B)

-- Projection UARel morphisms

𝒮-fst : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : A → Type ℓB} {𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B}
  → UARelHom (∫ 𝒮ᴰ-B) 𝒮-A
𝒮-fst .UARelHom.fun = fst
𝒮-fst .UARelHom.rel = fst
𝒮-fst .UARelHom.ua p = refl

𝒮-snd : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : Type ℓB} {𝒮-B : UARel B ℓ≅B}
  → UARelHom (𝒮-A ×𝒮 𝒮-B) 𝒮-B
𝒮-snd .UARelHom.fun = snd
𝒮-snd .UARelHom.rel = snd
𝒮-snd .UARelHom.ua p = refl

-- Lift a DUARel to live over a Σ-type

𝒮ᴰ-Lift : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : A → Type ℓC} (𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C)
  → DUARel (∫ 𝒮ᴰ-C) (λ (a , _) → B a) ℓ≅B
𝒮ᴰ-Lift _  𝒮ᴰ-B _ = 𝒮ᴰ-reindex 𝒮-fst 𝒮ᴰ-B

-- DUARel on a Σ-type

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} {ℓ≅B : Level} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : Σ A B → Type ℓC} {ℓ≅C : Level} (𝒮ᴰ-C : DUARel (∫ 𝒮ᴰ-B) C ℓ≅C)
  where

  open UARel 𝒮-A
  private
    module B = DUARel 𝒮ᴰ-B
    module C = DUARel 𝒮ᴰ-C

  𝒮ᴰ-Σ : DUARel 𝒮-A (λ a → Σ[ b ∈ B a ] C (a , b)) (ℓ-max ℓ≅B ℓ≅C)
  DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-Σ (b , c) p (b' , c') =
    Σ[ q ∈ b B.≅ᴰ⟨ p ⟩ b' ]  (c C.≅ᴰ⟨ p , q ⟩ c')
  DUARel.uaᴰ 𝒮ᴰ-Σ (b ,  c) p (b' , c') =
    compEquiv
      (Σ-cong-equiv (B.uaᴰ b p b') (λ q → C.uaᴰ c (p , q) c'))
      ΣPath≃PathΣ

-- DUARel on a non-dependent Σ-type

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} {ℓ≅B : Level} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : A → Type ℓC} {ℓ≅C : Level} (𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C)
  where

  _×𝒮ᴰ_ : DUARel 𝒮-A (λ a → B a × C a) (ℓ-max ℓ≅B ℓ≅C)
  _×𝒮ᴰ_ = 𝒮ᴰ-Σ 𝒮ᴰ-B (𝒮ᴰ-Lift 𝒮-A 𝒮ᴰ-C 𝒮ᴰ-B)

-- SubstRel on a Σ-type

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
  {C : Σ A B → Type ℓC} (𝒮ˢ-C : SubstRel (∫ˢ 𝒮ˢ-B) C)
  where

  open UARel 𝒮-A
  open SubstRel
  private
    module B = SubstRel 𝒮ˢ-B
    module C = SubstRel 𝒮ˢ-C

  𝒮ˢ-Σ : SubstRel 𝒮-A (λ a → Σ[ b ∈ B a ] C (a , b))
  𝒮ˢ-Σ .act p = Σ-cong-equiv (B.act p) (λ b → C.act (p , refl))
  𝒮ˢ-Σ .uaˢ p _ =
    fromPathP
      (DUARel.uaᴰ (𝒮ᴰ-Σ (Subst→DUA 𝒮ˢ-B) (Subst→DUA 𝒮ˢ-C))  _ p _ .fst (refl , refl))

-- SubstRel on a non-dependent product

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
  {C : A → Type ℓC} (𝒮ˢ-C : SubstRel 𝒮-A C)
  where

  open UARel 𝒮-A
  open SubstRel
  private
    module B = SubstRel 𝒮ˢ-B
    module C = SubstRel 𝒮ˢ-C

  _×𝒮ˢ_ : SubstRel 𝒮-A (λ a → B a × C a)
  _×𝒮ˢ_ .act p = ≃-× (B.act p) (C.act p)
  _×𝒮ˢ_ .uaˢ p (b , c) = ΣPathP (B.uaˢ p b , C.uaˢ p c)

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Martin-Löf identity type without the K axiom
-- (we do not assume uniqueness of identity proofs).

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

module Tools.PropositionalEquality where

-- We reexport Agda's builtin equality type.

open import Agda.Builtin.Equality public using (_≡_; refl)
open import Tools.Empty

-- Inequality.

infix 4 _≢_

_≢_ : {A : Set} → A → A → Set
a ≢ b = a ≡ b → ⊥

-- Symmetry.

sym : {A : Set} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

-- Transitivity.

trans : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

-- Non-dependent congruence rules.

cong : {A B : Set} {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl

cong₂ : ∀ {A B C : Set} {a a′ b b′}
        (f : A → B → C) → a ≡ a′ → b ≡ b′
      → f a b ≡ f a′ b′
cong₂ f refl refl = refl

cong₃ : ∀ {A B C D : Set} {a a′ b b′ c c′}
        (f : A → B → C → D) → a ≡ a′ → b ≡ b′ → c ≡ c′
      → f a b c ≡ f a′ b′ c′
cong₃ f refl refl refl = refl

cong₄ : ∀ {A B C D E : Set} {a a′ b b′ c c′ d d′}
        (f : A → B → C → D → E) → a ≡ a′ → b ≡ b′ → c ≡ c′ → d ≡ d′
      → f a b c d ≡ f a′ b′ c′ d′
cong₄ f refl refl refl refl = refl

-- Substitution (type-cast).

subst : {A : Set} {a b : A} {ℓ : Agda.Primitive.Level} (F : A → Set ℓ) → a ≡ b → F a → F b
subst F refl f = f

-- Two substitutions simultaneously.

subst₂ : ∀ {A B : Set} {a a′ b b′} {ℓ : Agda.Primitive.Level} (F : A → B → Set ℓ)
       → a ≡ a′ → b ≡ b′ → F a b → F a′ b′
subst₂ F refl refl f = f

-- Three substitutions simultaneously.

subst₃ : ∀ {A B C : Set} {a a′ b b′ c c′} (F : A → B → C → Set)
       → a ≡ a′ → b ≡ b′ → c ≡ c′ → F a b c → F a′ b′ c′
subst₃ F refl refl refl f = f

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


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

open import Cubical.Foundations.Everything renaming (Iso to _≅_)
open import Cubical.Data.List
open import Cubical.Data.Unit
open import Cubical.Data.Prod hiding (map)
open import Cubical.Data.Nat

module Cubical.Data.List.Dependent where

open _≅_

data ListP {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) : (as : List A) → Type (ℓ-max ℓA ℓB) where
  [] : ListP B []
  _∷_ : {x : A} (y : B x) {xs : List A} (ys : ListP B xs) → ListP B (x ∷ xs)

-- Represent ListP via known operations in order to derive properties more easily.
RepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → Type (ℓ-max ℓA ℓB)
RepListP B [] = Lift Unit
RepListP B (a ∷ as) = B a × RepListP B as

isoRepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → ListP B as ≅ RepListP B as
fun (isoRepListP B []) bs = lift tt
inv (isoRepListP B []) u = []
rightInv (isoRepListP B []) u = refl
leftInv (isoRepListP B []) [] = refl
fun (isoRepListP B (a ∷ as)) (b ∷ bs) = b , fun (isoRepListP B as) bs
inv (isoRepListP B (a ∷ as)) (b , br) = b ∷ inv (isoRepListP B as) br
rightInv (isoRepListP B (a ∷ as)) (b , br) i = b , rightInv (isoRepListP B as) br i
leftInv (isoRepListP B (a ∷ as)) (b ∷ bs) i = b ∷ leftInv (isoRepListP B as) bs i

equivRepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → ListP B as ≃ RepListP B as
equivRepListP B as = isoToEquiv (isoRepListP B as)

pathRepListP : ∀ {ℓA ℓB} {A : Type ℓA} (B : A → Type ℓB) (as : List A) → ListP B as ≡ RepListP B as
pathRepListP B as = ua (equivRepListP B as)

private
  isOfHLevelSucSuc-RepListP : ∀ {ℓA ℓB} (n : HLevel)
    → {A : Type ℓA}
    → {B : A → Type ℓB} → ((a : A) → isOfHLevel (suc (suc n)) (B a))
    → (as : List A)
    → isOfHLevel (suc (suc n)) (RepListP B as)
  isOfHLevelSucSuc-RepListP n isHB [] = isOfHLevelLift (suc (suc n)) (isOfHLevelUnit (suc (suc n)))
  isOfHLevelSucSuc-RepListP n isHB (a ∷ as) = isOfHLevelProd (suc (suc n)) (isHB a) (isOfHLevelSucSuc-RepListP n isHB as)

isOfHLevelSucSuc-ListP : ∀ {ℓA ℓB} (n : HLevel)
  → {A : Type ℓA}
  → {B : A → Type ℓB} → ((a : A) → isOfHLevel (suc (suc n)) (B a))
  → {as : List A}
  → isOfHLevel (suc (suc n)) (ListP B as)
isOfHLevelSucSuc-ListP n {A} {B} isHB {as} =
  subst⁻ (isOfHLevel (suc (suc n))) (pathRepListP B as) (isOfHLevelSucSuc-RepListP n isHB as)

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

mapP : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'} {B : A → Type ℓB} {B' : A' → Type ℓB'}
  (f : A → A') (g : (a : A) → B a → B' (f a)) → ∀ as → ListP B as → ListP B' (map f as)
mapP f g [] [] = []
mapP f g (a ∷ as) (b ∷ bs) = g _ b ∷ mapP f g as bs

mapOverIdfun : ∀ {ℓA ℓB ℓB'} {A : Type ℓA} {B : A → Type ℓB} {B' : A → Type ℓB'}
  (g : (a : A) → B a → B' a) → ∀ as → ListP B as → ListP B' as
mapOverIdfun g [] [] = []
mapOverIdfun g (a ∷ as) (b ∷ bs) = g a b ∷ mapOverIdfun g as bs

mapOverIdfun-idfun : ∀ {ℓA ℓB} {A : Type ℓA} {B : A → Type ℓB} as → mapOverIdfun (λ a → idfun _) as ≡ (idfun (ListP B as))
mapOverIdfun-idfun [] i [] = []
mapOverIdfun-idfun (a ∷ as) i (b ∷ bs) = b ∷ mapOverIdfun-idfun as i bs

mapOverIdfun-∘ : ∀ {ℓA ℓB ℓB' ℓB''} {A : Type ℓA} {B : A → Type ℓB} {B' : A → Type ℓB'} {B'' : A → Type ℓB''}
  (h : (a : A) → B' a → B'' a) (g : (a : A) → B a → B' a) → ∀ as
  → mapOverIdfun (λ a → h a ∘ g a) as ≡ mapOverIdfun h as ∘ mapOverIdfun g as
mapOverIdfun-∘ h g [] i [] = []
mapOverIdfun-∘ h g (a ∷ as) i (b ∷ bs) = h a (g a b) ∷ mapOverIdfun-∘ h g as i bs

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

module Data.Unit.UniversePolymorphic where

open import Level

record ⊤ {ℓ} : Type ℓ where constructor tt

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

module Formalization where

open import Agda.Primitive using (lsuc)

open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

open import Level

-- Recall Lemma 1.12

ind₌ : ∀{a b}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set b) → ((x : A) → C x x refl) → {x y : A} → (p : x ≡ y) → C x y p
ind₌ C c {x}{y} p rewrite p = c y

-- Types are higher groupoids
-- --------------------------

-- This is the *central* idea of HoTT.  A Type isn't just an atomic entity, it's a homotopic space.
-- An ∞-groupoid consists of
--   ∘ a collection of objects
--   ∘ a collection of morphisms between objects, and then morphisms between morphisms, and so on
--   ∘ equipped with some complex algebraic structure
--
-- a morphism at level k is called a k- morphism. Morphisms at each level have
--   ∘ identity
--   ∘ composition
--   ∘ inverse operations
--
-- which are weak in the sense that they satisfy the groupoid laws (associativity
-- of composition, identity is a unit for composition, inverses cancel) only up
-- to morphisms at the next level, and this weakness gives rise to further structure.

-- Example
--
-- Because associativity of composition of morphisms p (q r) = (p q) r is itself a higher-dimensional morphism
-- we need additional operators to talk about them.  For example:

{- Mac Lane's Pentagon
 ---------------------

 All the various ways to reassociate p (q (r s))

                                  /- ((p q) r) s -\
                                 /                 \
                      (p (q r)) s                   (p q) (r s)
                                |                   |
                                |                   |
                      p ((q r) s) ----------------- p (q (r s))

-}

-- Moreover, all of this higher groupoid structure comes automagically from the induction principle
-- on Id.

-- "Informally, the induction principle for identity types says that if we
-- construct an object (or prove a statement) which depends on an inhabitant
-- p : x == y of an identity type,
data _==_ {i} {A : Set i} (a : A) : A → Set (lsuc i) where
  idp : a == a -- then it suffices to perform the construction (or the proof) in
               -- the special case when x and y are the same (judgmentally)
               -- and p is the reflexivity element reflx : x = x (judgmentally)

-- Lemma 2.1.1 "Paths can be reversed"

-- first proof

_⁻¹ : ∀ {i} {A : Set i}{x y : A} → (x ≡ y) → (y ≡ x)
_⁻¹ {i} {A} = λ p → ind₌ D d  p where
  D : (x y : A) → x ≡ y → Set i
  D = λ x y p → (y ≡ x)

  d : (x : A) → D x x refl
  d = λ x → refl

-- second proof

inv-sym : ∀ {i} {A : Set i}{x y : A} → (x ≡ y) → (y ≡ x)
inv-sym refl = refl

-- Lemma 2.1.2 & 2.1.3 "paths can be concatenated (strung together)"

-- First proof.  We need the type family D : Π (x, y : A) Π (p : x ≡ y) → Type.  From that we
--               produce an element d : D x x reflₓ (simply identity) then apply the induction
--               principle above to D and d.
composite : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite {i} {A} {_}{_}{z} p = ind₌ D d p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y _ = y ≡ z → x ≡ z

  d : (x₁ : A) → D x₁ x₁ refl
  d _ = λ x → x

-- Second proof. We need the type family D : Π (x, y : A) Π (p : x ≡ y) → Type again.  From that
--               we produce an element d (x) : D x x reflₓ again, but rather than the identity we go a
--               step further and define E : Π (x z : A) Π (q : x ≡ z) → Type.  We then produce an
--               element e (x) : E x x reflₓ.  Induction on D d then unfolds to induction on D then E e.
composite' : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite' {i} {A} {_}{_}{z} = ind₌ D d where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y _ = y ≡ z → x ≡ z

  d : (x : A) → D x x refl
  d x = ind₌ E e where
    E : (x z : A) → (q : x ≡ z) → Set i
    E x z _ = x ≡ z

    e : (x : A) → E x x refl
    e x = refl

-- Third proof.  Everything is reflexivity you fool.  The hell did you do all that work for before?
composite'' : ∀ {i} {A : Set i}{x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
composite'' refl refl = refl

--   Equality   |        Homotopy        |     ∞-Groupoid
-- reflexivity  | constant path          | identity morphism
-- symmetry     | inversion of paths     | inverse morphism
-- transitivity | concatenation of paths | composition of morphisms

open import Function

-- Lemma 2.1.4
-- These are all propositional equalities living in the type of identity types.
-- Topologically they are paths of paths, and we can form a homotopy between them.

-- For my next trick, I will need composition of paths

-- Reflexivity right
lem-1-r : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → p ≡ (composite p refl)
lem-1-r {i} {A} {x}{y} {p} = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = p ≡ composite p refl

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

-- Reflexivity left
lem-1-l : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → p ≡ (composite refl p)
lem-1-l {i} {A} {x}{y} {p} = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = p ≡ composite refl p

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

lem-2-l : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → composite ((p)⁻¹) p ≡ refl
lem-2-l {i} {A} {x}{y} {p} = ind₌ D d p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y p = composite ((p)⁻¹) p ≡ refl

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

lem-2-r : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → composite p ((p)⁻¹) ≡ refl
lem-2-r {i} {A} {x}{y} {p} = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = composite p ((p)⁻¹) ≡ refl

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ x → refl

-- Inversion of identity
lem-3 : ∀ {i} {A : Set i}{x y : A}{p : x ≡ y} → ((p)⁻¹)⁻¹ ≡ p
lem-3 {i} {A} {x}{y} {p} = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = ((p)⁻¹)⁻¹ ≡ p

  d : (x₁ : A) → D x₁ x₁ refl
  d = λ _ → refl

{-
-- Transitivity of identity
lem-4 : ∀ {i} {A : Set i}{x y z w : A}{p : x ≡ y}{q : y ≡ z}{r : z ≡ w} → composite p (composite q r) ≡ composite (composite p q) r
lem-4 {i} {A} {_}{_}{z} = ind₌ D₁ d₁ where
  D₁ : (x y : A) → (x ≡ y) → Set i
  D₁ x y p = (z w : A)(q : y ≡ z)(r : z ≡ w) → composite p (composite q r) ≡ composite (composite p q) r

  d₁ : (x₁ : A) → D₁ x₁ x₁ refl
  d₁ _ = ind₌ D₂ d₂ where
    D₂ : (x z : A) → (q : x ≡ z) → Set i
    D₂ x z q = (w : A)(r : z ≡ w) → composite refl (composite q r) ≡ composite (composite refl q) r

    d₂ :  (x₂ : A) → D₂ x₂ x₂ refl
    d₂ _ = ind₌ D₃ d₃ where
       D₃ : (x w : A) → (r : x ≡ w) → Set i
       D₃ x w r = (composite refl (composite refl r)) ≡ (composite (composite refl refl) r)

       d₃ : (x₃ : A) → D₃ x₃ x₃ refl
       d₃ _ = composite refl (composite refl refl) ≡ composite (composite refl refl) refl
-}

-- Lemma 2.1.6

open import Data.Product using (Σ ; _,_ ; proj₁ ; proj₂)
open import Data.Nat using (ℕ ; suc)

-- We need pointed sets for this part
Set• : ∀ i → Set _
Set• i = Σ (Set i) λ X → X

-- The loop space of a type is
--  - A base point
--  - A loop (reflexivity) about that point
Ω₁ : ∀ {i} → Set• i → Set• i
Ω₁ (X , x) = ((x ≡ x) , refl)

-- Construct arbitrary n-dimensional loop spaces
Ωⁿ : ∀ {i} → ℕ → Set• i → Set• _
Ωⁿ 0 x = x
Ωⁿ (suc n) x = Ωⁿ n (Ω₁ x)

-- Projects the type from an n-dimensional loop space
Ω : ∀ {i} → ℕ → {X : Set i} → X → Set i
Ω n {X} x = proj₁ (Ωⁿ n (X , x))

-- Projects the loop from an n-dimensional loop space
loop : ∀ {i} n {X : Set i}(x : X) → Ω n x
loop n {X} x = proj₂ (Ωⁿ n (X , x))

-- Composition operation on n-dimensional loop spaces
_×_ : ∀ {i} n {A : Set i}{x : A} → Ω n x → Ω n x → Ω n x
_×_ n {A} {x} x₁ x₂ = loop n x

-- 2.2.1

-- We're type theorists, so we like functor-looking things.
-- Paths are functor looking things.
-- We like paths
-- They respect equality and are all continuous-like
ap : ∀ {i j} {A : Set i}{B : Set j}{x y : A}{f : A → B} → (x ≡ y) → (f x ≡ f y)
ap {i}{j} {A}{B} {x}{y}{f} p = ind₌ D d p where
  D : (x y : A) → (p : x ≡ y) → Set j
  D x y p = f x ≡ f y

  d : (x : A) → D x x refl
  d = λ x → refl

ap₂ : ∀ {i j k} {A : Set i}{B : Set j}{C : Set k}{x x′ : A}{y y′ : B}(f : A → B → C) → (x ≡ x′) → (y ≡ y′) → (f x y ≡ f x′ y′)
ap₂ f p q = composite (ap {f = λ _ → f _ _} p) (ap {f = f _} q)

ap' : ∀ {i j} {A : Set i}{B : Set j}{x y : A} → (f : A → B) → ((x ≡ y) → (f x ≡ f y))
ap' f refl = refl

-- 2.3

-- The dependently typed version of `ap` takes a type family and relates its instantiations with p
transport : ∀ {i} {A : Set i}{P : A → Set i}{x y : A} → (p : x ≡ y) → (P x → P y)
transport {i} {A}{P} {x}{y} p = ind₌ D d p where
    D : (x y : A) → (p : x ≡ y) → Set i
    D x y p = P x → P y

    d : (x : A) → D x x refl
    d = λ x → id
-- Topologically, we can view transport as a "path lifting" operation
-- That is, we lift the path p to a path in the space ∑[ x ∈ A ] P(x) provided we have a
-- base point u in the lifted space.
--
-- Basically, P respects equality
path-lifting : ∀ {a p}{A : Set a}{x y : A}{P : A → Set p} → (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , u)
path-lifting = λ {a} {p} {A} {x} {y} {P} u → cong (λ z → z , u)

-- Look, transport works in the "upper" space too!
apd : ∀ {i} {A : Set i}{P : A → Set i}{f : (x : A) → P x}{x y : A} → (p : x ≡ y) → (transport p (f x) ≡ f y)
apd {i} {A}{P} {f}{x}{y} p = ind₌ D d p where
  D : (x y : A) → (p : x ≡ y) → Set i
  D x y p = transport p (f x) ≡ f y

  d : (x : A) → D x x refl
  d = λ x → refl

-- By induction, it suffices to assume p is refl.  Because of course it does.
apd' : ∀ {i} {A : Set i}{P : A → Set i}{f : (x : A) → P x}{x y : A} → (p : x ≡ y) → (transport p (f x) ≡ f y)
apd' refl = refl

-- We can also fix B and make transport work like fmap with equalities.
transportconst : ∀ {i} {A : Set i}{B : Set i}{P : A → B}{x y : A} → (p : x ≡ y) → (b : B) → transport p b ≡ b
transportconst {i} {A}{B}{P} {x}{y} p b = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = transport p b ≡ b

  d : (x : A) → D x x refl
  d = λ x → refl

{-
lem-2-3-8 : ∀ {i} {A : Set i}{B : Set i}{f : A → B}{x y : A} → (p : x ≡ y) → apd p ≡ transportconst (ap p) (f x)
lem-2-3-8 {i} {A}{B}{f} {x}{y} p = ind₌ D d p where
  D : (x y : A) → (x ≡ y) → Set i
  D x y p = apd p ≡ transportconst (f x) ∘ ap p

  d : (x : A) → D x x refl
  d = refl
-}

{-
lem-2-3-9 : ∀ {i} {A : Set i}{P : A → Set i}{x y z : A} → (p : x ≡ y) → (q : y ≡ z) → (u : P x) → transport q (transport p u) ≡ transport (p ∘ q) u
lem-2-3-9 = ?
-}

-- Homotopies

-- Under Propositions-as-Types two functions are the same if they give the same outputs on the
-- same inputs.  Which looks like this: a type whose terms are proofs of that^
_∼_ : ∀ {a b} {A : Set a}{P : A → Set b} → (f g : (x : A) → P x) → Set (a ⊔ b)
_∼_ {a}{b} {A}{P} f g = (x : A) → f x ≡ g x

-- 2.4.2

lem-2-4-2 : ∀ {a} {A : Set a}{B : Set a} → (f : A → B) → f ∼ f
lem-2-4-2 f = λ _ → refl

lem-2-4-2' : ∀ {a} {A : Set a}{B : Set a} → (f g : A → B) → (f ∼ g) → (g ∼ f)
lem-2-4-2' f g x x₁ = sym (x x₁)

-- For any A and B, a quasi-inverse of f is a triple with
--    ∘ A way back (an inverse for the homomorphism)
--    ∘ Homotopies:
--        ⊚ α : f ∘ g ∼ id
--        ⊚ β : g ∘ f ∼ id
-- For now, because I am lazy, the presence of a quasi-inverse will count
-- as our definition of equivalence for now.  Sorry.
record IsEquiv {i j}{A : Set i}{B : Set j}(to : A → B) : Set (i ⊔ j) where
  field
    from : B → A
    iso₁ : (x : A) → from (to x) ≡ x
    iso₂ : (y : B) → to (from y) ≡ y

-- Example 2.4.7: Identity is an equivalence.
id-is-equiv : ∀ {i} (A : Set i) → IsEquiv (id {i}{A})
id-is-equiv {i} A = record
  { from = id {i}{A}
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl
  }

-- Type equivalence is also an equivalence, just on the Universe because:
--    ∘ id-is-equiv works for it, therefore A ≃ A
--    ∘ With A ≃ B, we can always make B ≃ A
--    ∘ With A ≃ B and B ≃ C we have A ≃ C
_≃_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A ≃ B = Σ (A → B) IsEquiv

open import Data.Product renaming (_×_ to _×p_)

split-path : ∀ {i j}{A : Set i}{B : Set j}{x y : A ×p B} → x ≡ y → (proj₁ x ≡ proj₁ y) ×p (proj₂ x ≡ proj₂ y)
split-path p = ap {f = proj₁} p , ap {f = proj₂} p

pair₌ : ∀ {i j}{A : Set i}{B : Set j}{x y : A ×p B} → (proj₁ x ≡ proj₁ y) ×p (proj₂ x ≡ proj₂ y) → x ≡ y
pair₌ (p , q) = ap₂ _,_ p q

instance
  split-is-equiv : ∀ {i j}{A : Set i}{B : Set j}{x y : A ×p B} → IsEquiv (pair₌ {x = x}{y = y})
  split-is-equiv {x = x}{y = y} = record
    { from = split-path
    ; iso₁ = λ pq →
            ind₌ (λ _ _ p → ∀ {b₁ b₂} (q : b₁ ≡ b₂) →
              split-path (pair₌ (p , q)) ≡ (p , q))
            (λ _ q → ind₌
              (λ _ _ q →
                split-path (pair₌ (refl , q)) ≡ (refl , q))
              (λ _ → refl) q)
                (proj₁ pq) (proj₂ pq)
    ; iso₂ = ind₌ (λ _ _ p → pair₌ (split-path p) ≡ p) (λ _ → refl)
    }

{-
happly : ∀ {i}{A : Set i}{f g : A → Set i} → (f ≡ g) → ((x : A) → f x ≡ g x)
happly p x = ap' (λ u → u x)
-}

-- 2.10

-- This says, when you get down to it, id on universes is a
-- type family with a total space of pointed types.  Turns out
-- Ω isn't just for horses.
idtoeqv : ∀ {i} {A : Set i}{B : Set i} → (A ≡ B) → (A ≃ B)
idtoeqv {_}{A} refl = (id , id-is-equiv A)

-- With idtoeqv in hand, we have to ask Agda nicely to make idtoeqv an equivalence.

postulate -- Just kidding
  ua : ∀ {i} {A : Set i}{B : Set i} → (A ≃ B) ≃ (A ≡ B)
-- ^This says "equivalent types may be identified"

-- 2.12

{-
data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : (x : A) → A ⊎ B
  inr : (y : B) → A ⊎ B

code : ∀ {a b}{{A : Set a}}{{B : Set b}} → A ⊎ B → Set (a ⊔ b)
code (inl a) = ?
code (inr b) = ⊥

code-lem : ∀ {a b}{{A : Set a}}{{B : Set b}} → (x : A ⊎ B) → (a₀ : A) → ((inl a₀ ≡ x) ≃ code x)
code-lem {{A}} {{B}} x a₀ = ? where
    encode : (x : A ⊎ B) → (p : inl a₀ ≡ x) → code x
    encode x p = transport p refl

    decode : (x : A ⊎ B) → (c : code x) → inl a₀ ≡ x
    decode x c = ?
-}

open import Data.Nat
open import Data.Unit
open import Data.Empty

code : ℕ → ℕ → Set
code ℕ.zero ℕ.zero = ⊤
code ℕ.zero (ℕ.suc m) = ⊥
code (ℕ.suc n) ℕ.zero = ⊥
code (ℕ.suc n) (ℕ.suc m) = code n m

-- 2.13

natcode-lem : ∀ {m n : ℕ} → (m ≡ n) → code m n
natcode-lem {x}{y} p = encode {x}{y} p where
  encode : ∀ {m n : ℕ} → (m ≡ n) → code m n
  encode {m}{n} p = transport p (r m) where
    r : (n : ℕ) → code n n
    r ℕ.zero = tt
    r (ℕ.suc n) = r n

  decode : ∀ {m n : ℕ} → code m n → (m ≡ n)
  decode {ℕ.zero} {ℕ.zero} tt = refl
  decode {ℕ.zero} {ℕ.suc _} ()
  decode {ℕ.suc _} {ℕ.zero} ()
  decode {ℕ.suc m} {ℕ.suc n} c = cong ℕ.suc (decode c)

  enc-dec-quasi : ∀ {n : ℕ} → decode {n}{n} (encode {n}{n} refl) ≡ refl
  enc-dec-quasi {ℕ.zero} = refl
  enc-dec-quasi {ℕ.suc n₁} = {! !}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module UniDB.Morph.WeakenOne where

open import UniDB.Spec

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

data Weaken₁ : MOR where
  weaken₁ : {γ : Dom} → Weaken₁ γ (suc γ)

instance
  iLkWeaken₁ : {T : STX} {{vrT : Vr T}} → Lk T Weaken₁
  lk {{iLkWeaken₁ {T}}} weaken₁ i = vr {T} (suc i)

  iLkRenWeaken₁ : {T : STX} {{vrT : Vr T}} → LkRen T Weaken₁
  lk-ren {{iLkRenWeaken₁}} weaken₁ i = refl

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
------------------------------------------------------------------------
-- A type for values that should be erased at run-time
------------------------------------------------------------------------

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

open import Equality
import Erased.Basics
import Erased.Level-1

module Erased
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)
  (ax : ∀ {ℓ} → Erased.Level-1.[]-cong-axiomatisation eq ℓ)
  where

-- Re-exported definitions.

private
  module E₁ = Erased.Level-1 eq
open E₁ public
  hiding (module Erased-cong;
          module []-cong;
          module []-cong₁;
          module []-cong₂; module []-cong₂-⊔;
          module Extensionality)
open E₁.[]-cong ax public
import Erased.Level-2 eq as E₂
open E₂.[]-cong ax public
open import Erased.Stability eq as ES public
  hiding (module []-cong;
          module []-cong₁; module []-cong₁-lsuc;
          module []-cong₂; module []-cong₂-⊔₁; module []-cong₂-⊔₂;
          module Extensionality)
open ES.[]-cong ax public

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Common.Level

postulate
  ℓ : Level

data D : Set (lsuc ℓ) where
  c : (ℓ : Level) → Set ℓ → D

-- Bad error:
-- The type of the constructor does not fit in the sort of the
-- datatype, since Set (lsuc ℓ) is not less or equal than Set (lsuc ℓ)
-- when checking the constructor c in the declaration of D

-- Jesper, 2018-12-09: new, better error:
-- Set (lsuc ℓ₁) is not less or equal than Set (lsuc ℓ)
-- when checking that the type (ℓ₁ : Level) → Set ℓ₁ → D of the
-- constructor c fits in the sort Set (lsuc ℓ) of the datatype.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.Concept using ( Concept ; ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊓_ ; _⊔_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 ; neg )
open import Web.Semantic.DL.Concept.Model using ( _⟦_⟧₁ ; ⟦⟧₁-resp-≈ )
open import Web.Semantic.DL.FOL using  ( Formula ; true ; false ; _∧_ ; _∈₁_ ; _∈₂_ ; _∈₁_⇒_ ; _∼_ ; _∼_⇒_ ; ∀₁ )
open import Web.Semantic.DL.FOL.Model using ( _⊨f_ )
open import Web.Semantic.DL.Role.Skolemization using ( rskolem ; rskolem⇒ ; rskolem-sound ; rskolem⇒-sound )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( True ; tt )

module Web.Semantic.DL.Concept.Skolemization {Σ : Signature} where

CSkolems : Set → Concept Σ → Set
CSkolems Δ ⟨ c ⟩ = True
CSkolems Δ ¬⟨ c ⟩ = True
CSkolems Δ ⊤ = True
CSkolems Δ ⊥ = True
CSkolems Δ (C ⊓ D) = (CSkolems Δ C) × (CSkolems Δ D)
CSkolems Δ (C ⊔ D) = (Δ → Bool) × (CSkolems Δ C) × (CSkolems Δ D)
CSkolems Δ (∀[ R ] C) = CSkolems Δ C
CSkolems Δ (∃⟨ R ⟩ C) = (Δ → Δ) × (CSkolems Δ C)
CSkolems Δ (≤1 R) = True
CSkolems Δ (>1 R) = (Δ → Δ) × (Δ → Δ)

cskolem : ∀ {Δ} C → (CSkolems Δ C) → Δ → Formula Σ Δ
cskolem ⟨ c ⟩ Φ x = x ∈₁ c
cskolem ¬⟨ c ⟩ Φ x = x ∈₁ c ⇒ false
cskolem ⊤ Φ x = true
cskolem ⊥ Φ x = false
cskolem (C ⊓ D) (Φ , Ψ) x = (cskolem C Φ x) ∧ (cskolem D Ψ x)
cskolem (C ⊔ D) (φ , Φ , Ψ) x = if (φ x) then (cskolem C Φ x) else (cskolem D Ψ x)
cskolem (∀[ R ] C) Φ x = ∀₁ λ y → rskolem⇒ R x y (cskolem C Φ y)
cskolem (∃⟨ R ⟩ C) (φ , Ψ) x = (rskolem R x (φ x)) ∧ (cskolem C Ψ (φ x))
cskolem (≤1 R) Φ x = ∀₁ λ y → ∀₁ λ z → rskolem⇒ R x y (rskolem⇒ R x z (y ∼ z))
cskolem (>1 R) (φ , ψ) x = (rskolem R x (φ x)) ∧ (rskolem R x (ψ x)) ∧ (φ x ∼ ψ x ⇒ false)

cskolem-sound : ∀ I C Φ x → (I ⊨f cskolem C Φ x) → (x ∈ I ⟦ C ⟧₁)
cskolem-sound I ⟨ c ⟩ Φ x x∈⟦c⟧ = x∈⟦c⟧
cskolem-sound I ¬⟨ c ⟩ Φ x x∉⟦c⟧ = x∉⟦c⟧
cskolem-sound I ⊤ Φ x _ = tt
cskolem-sound I ⊥ Φ x ()
cskolem-sound I (C ⊓ D) (Φ , Ψ) x (Fx , Gx) =
  (cskolem-sound I C Φ x Fx , cskolem-sound I D Ψ x Gx)
cskolem-sound I (C ⊔ D) (φ , Φ , Ψ) x  F∨Gx with φ x
cskolem-sound I (C ⊔ D) (φ , Φ , Ψ) x  Fx | true  = inj₁ (cskolem-sound I C Φ x Fx)
cskolem-sound I (C ⊔ D) (φ , Φ , Ψ) x  Gx | false = inj₂ (cskolem-sound I D Ψ x Gx)
cskolem-sound I (∀[ R ] C) Φ x ∀RFx =
  λ y xy∈R → cskolem-sound I C Φ y (rskolem⇒-sound I R x y (cskolem C Φ y) (∀RFx y) xy∈R)
cskolem-sound I (∃⟨ R ⟩ C) (φ , Ψ) x (xy∈R , Fy) =
  ( φ x , rskolem-sound I R x (φ x) xy∈R , cskolem-sound I C Ψ (φ x) Fy )
cskolem-sound I (≤1 R) Φ x ≤1Rx =
  λ y z xy∈R xz∈R → rskolem⇒-sound I R x z (y ∼ z)
    (rskolem⇒-sound I R x y (rskolem⇒ R x z (y ∼ z)) (≤1Rx y z) xy∈R) xz∈R
cskolem-sound I (>1 R) (φ , ψ) x  (xy∈R , xz∈R , y≁z) =
  (φ x , ψ x , rskolem-sound I R x (φ x) xy∈R , rskolem-sound I R x (ψ x) xz∈R , y≁z)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

open import Data.Nat hiding ( _≟_ )
open import Data.Fin renaming ( _<_ to _<<_ ) hiding (_≤_)
-- open import Data.Fin.Properties  hiding ( ≤-refl )
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality
open import logic
open import nat
open import Data.Nat.Properties hiding ( _≟_ )

open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )

record FiniteSet ( Q : Set ) : Set  where
     field
        finite : ℕ
        Q←F : Fin finite → Q
        F←Q : Q → Fin finite
        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
        finiso← : (f : Fin finite ) → F←Q ( Q←F f ) ≡ f
     exists1 : (m : ℕ ) → m Data.Nat.≤ finite → (Q → Bool) → Bool
     exists1  zero  _ _ = false
     exists1 ( suc m ) m<n p = p (Q←F (fromℕ< {m} {finite} m<n)) \/ exists1 m (<to≤ m<n) p
     exists : ( Q → Bool ) → Bool
     exists p = exists1 finite ≤-refl p

     open import Data.List
     list1 : (m : ℕ ) → m Data.Nat.≤ finite → (Q → Bool) → List Q
     list1  zero  _ _ = []
     list1 ( suc m ) m<n p with bool-≡-? (p (Q←F (fromℕ< {m} {finite} m<n))) true
     ... | yes _ = Q←F (fromℕ< {m} {finite} m<n) ∷ list1 m (<to≤ m<n) p
     ... | no  _ = list1 m (<to≤ m<n) p
     to-list : ( Q → Bool ) → List Q
     to-list p = list1 finite ≤-refl p

     equal? : Q → Q → Bool
     equal? q0 q1 with F←Q q0 ≟ F←Q q1
     ... | yes p = true
     ... | no ¬p = false

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
import cedille-options
open import general-util
module spans (options : cedille-options.options) {mF : Set → Set} {{mFm : monad mF}} where
open import cedille-types
open import constants
open import conversion
open import ctxt
open import free-vars
open import syntax-util
open import type-util
open import to-string options
open import subst
open import datatype-util
open import json

--------------------------------------------------
-- span datatype
--------------------------------------------------

err-m : Set
err-m = maybe string

data span : Set where
  mk-span : string → posinfo → posinfo → 𝕃 tagged-val {- extra information for the span -} → err-m → span

span-to-json : span → json
span-to-json (mk-span name s e tvs err?) =
  json-array $ json-string name :: json-raw [[ s ]] :: json-raw [[ e ]] :: [ tagged-vals-to-json (maybe-else' err? tvs λ err → ("error" , [[ err ]] , []) :: tvs) ]

data error-span : Set where
  mk-error-span : string → posinfo → posinfo → 𝕃 tagged-val → string → error-span

data spans : Set where
  regular-spans : maybe error-span → 𝕃 span → spans
  global-error : string {- error message -} → maybe span → spans

is-error-span : span → 𝔹
is-error-span (mk-span _ _ _ _ err) = isJust err

get-span-error : span → err-m
get-span-error (mk-span _ _ _ _ err) = err

get-spans-error : spans → maybe (string × 𝕃 tagged-val)
get-spans-error (global-error e _) = just $ e , []
get-spans-error (regular-spans e? _) = maybe-map (λ {(mk-error-span _ _ _ tvs e) → e , tvs}) e?

get-tagged-vals : span → 𝕃 tagged-val
get-tagged-vals (mk-span _ _ _ tvs _) = tvs

spans-have-error : spans → 𝔹
spans-have-error (regular-spans es ss) = isJust es
spans-have-error (global-error _ _) = tt

empty-spans : spans
empty-spans = regular-spans nothing []

spans-to-json' : spans → 𝕃 (string × json)
spans-to-json' (regular-spans _ ss) = [ "spans" , json-array (map span-to-json ss) ]
spans-to-json' (global-error e s) =
  ("error" , json-string e) :: maybe-else' s [] λ s → [ "global-error" , span-to-json s ]

spans-to-json : spans → json
spans-to-json = json-object ∘ spans-to-json'

print-file-id-table : ctxt → 𝕃 tagged-val
print-file-id-table Γ = h [] (ctxt.id-list Γ) where
  h : ∀ {i} → 𝕃 tagged-val → 𝕍 string i → 𝕃 tagged-val
  h ts [] = ts
  h {i} ts (fn :: fns) = h (strRunTag "fileid" empty-ctxt (strAdd fn) :: ts) fns

add-span : span → spans → spans
add-span s@(mk-span dsc pi pi' tv nothing) (regular-spans es ss) =
  regular-spans es (s :: ss)
add-span s@(mk-span dsc pi pi' tv (just err)) (regular-spans es ss) =
  regular-spans (just (mk-error-span dsc pi pi' tv err)) (s :: ss)
add-span s (global-error e e') =
  global-error e e'

--------------------------------------------------
-- spanM, a state monad for spans
--------------------------------------------------

spanM : Set → Set
spanM A = spans → mF (A × spans)

instance
  spanM-monad : monad spanM
  return ⦃ spanM-monad ⦄ = curry return
  _>>=_ ⦃ spanM-monad ⦄ m₁ m₂ ss = m₁ ss >>= uncurry m₂

  spanM-functor : functor spanM
  fmap ⦃ spanM-functor ⦄ g m ss = m ss >>= uncurry λ a ss' → return (g a , ss')

  spanM-applicative : applicative spanM
  pure ⦃ spanM-applicative ⦄ = return
  _<*>_ ⦃ spanM-applicative ⦄ mab ma ss =
    mab ss >>= uncurry λ f ss₁ →
    ma ss₁ >>= uncurry λ a →
    return (f a)

spanMok : spanM ⊤
spanMok = return triv

get-error : ∀ {A : Set} → (maybe error-span → spanM A) → spanM A
get-error m ss@(global-error _ _) = m nothing ss
get-error m ss@(regular-spans nothing _) = m nothing ss
get-error m ss@(regular-spans (just es) _) = m (just es) ss

set-error : maybe (error-span) → spanM ⊤
set-error es ss@(global-error _ _) = return2 triv ss
set-error es (regular-spans _ ss) = return2 triv (regular-spans es ss)

spanM-push : ∀ {A} → mF A → spanM A
spanM-push mf ss = mf >>= λ a → return2 a ss

-- discard changes made by the first computation
_>>=spand_ : ∀{A B : Set} → spanM A → (A → spanM B) → spanM B
_>>=spand_{A} m m' ss = m ss >>= λ where (v , _) → m' v ss

spanM-add : span → spanM ⊤
spanM-add s ss = return (triv , add-span s ss)

infixr 2 [-_-]_
[-_-]_ : ∀ {X} → span → spanM X → spanM X
[- s -] m = spanM-add s >> m

debug-span : posinfo → posinfo → 𝕃 tagged-val → span
debug-span pi pi' tvs = mk-span "Debug" pi pi' tvs nothing

spanM-debug : posinfo → posinfo → 𝕃 tagged-val → spanM ⊤
--spanM-debug pi pi' tvs = spanM-add (debug-span pi pi' tvs)
spanM-debug pi pi' tvs = spanMok

check-ret : ∀ {Y : Set} → maybe Y → Set → Set
check-ret {Y} T t = if isJust T then t else (t × Y)

return-when : ∀ {X Y} {m : maybe Y} → X → Y → spanM (check-ret m X)
return-when {X} {Y} {nothing} x u = return2 x u
return-when {X} {Y} {just _} x u = return x

case-ret : ∀ {X Y} {m : maybe Y} → spanM (X × Y) → (Y → spanM X) → spanM (check-ret m X)
case-ret {X} {Y} {nothing} n j = n
case-ret {X} {Y} {just y} n j = j y

case-ret-body : ∀ {X Y} {m : maybe Y} → spanM (check-ret m X) → (X → Y → spanM (check-ret m X)) → spanM (check-ret m X)
case-ret-body {X} {Y} {nothing} m f = m >>= uncurry f
case-ret-body {X} {Y} {just y} m f = m >>= λ x → f x y

with-clear-error : ∀ {A} → spanM A → spanM A
with-clear-error m =
  get-error λ es → set-error nothing >> m >>= λ a → set-error es >> return a

--------------------------------------------------
-- tagged-val constants
--------------------------------------------------

to-string-tag-tk : (tag : string) → ctxt → tpkd → tagged-val
to-string-tag-tk t Γ (Tkt T) = to-string-tag t Γ T
to-string-tag-tk t Γ (Tkk k) = to-string-tag t Γ k

location-data : location → tagged-val
location-data (file-name , pi) = strRunTag "location" empty-ctxt (strAdd file-name >>str strAdd " - " >>str strAdd pi)

var-location-data : ctxt → var → tagged-val
var-location-data Γ x =
  location-data (maybe-else missing-location snd
    (trie-lookup (ctxt.i Γ) x ||-maybe trie-lookup (ctxt.i Γ) (qualif-var Γ x)))

explain : string → tagged-val
explain = strRunTag "explanation" empty-ctxt ∘ strAdd

reason : string → tagged-val
reason = strRunTag "reason" empty-ctxt ∘ strAdd

expected-type : ctxt → type → tagged-val
expected-type = to-string-tag "expected-type"

expected-type-subterm : ctxt → type → tagged-val
expected-type-subterm = to-string-tag "expected-type of the subterm"

missing-expected-type : tagged-val
missing-expected-type = strRunTag "expected-type" empty-ctxt $ strAdd "[missing]"

expected-kind : ctxt → kind → tagged-val
expected-kind = to-string-tag "expected kind"

expected-kind-if : ctxt → maybe kind → 𝕃 tagged-val
expected-kind-if _ nothing = []
expected-kind-if Γ (just k) = [ expected-kind Γ k ]

expected-type-if : ctxt → maybe type → 𝕃 tagged-val
expected-type-if _ nothing = []
expected-type-if Γ (just tp) = [ expected-type Γ tp ]

type-data : ctxt → type → tagged-val
type-data = to-string-tag "type"

type-data-if : ctxt → maybe type → 𝕃 tagged-val
type-data-if Γ = maybe-else [] λ T → [ type-data Γ T ]

warning-data : string → tagged-val
warning-data = strRunTag "warning" empty-ctxt ∘ strAdd

check-for-type-mismatch : ctxt → string → type → type → err-m
check-for-type-mismatch Γ s tp tp' =
  if conv-type Γ tp tp' then nothing else just ("The expected type does not match the " ^ s ^ " type")

check-for-type-mismatch-if : ctxt → string → maybe type → type → err-m
check-for-type-mismatch-if Γ s T? T = T? >>= check-for-type-mismatch Γ s T

check-for-kind-mismatch : ctxt → string → kind → kind → err-m
check-for-kind-mismatch Γ s kd kd' =
  if conv-kind Γ kd kd' then nothing else just ("The expected kind does not match the " ^ s ^ " kind")

check-for-kind-mismatch-if : ctxt → string → maybe kind → kind → err-m
check-for-kind-mismatch-if Γ s k? k = k? >>= check-for-kind-mismatch Γ s k

check-for-tpkd-mismatch-if : ctxt → string → maybe tpkd → tpkd → err-m
check-for-tpkd-mismatch-if Γ check tk? tk =
  tk? >>= either-else
    (either-else' tk (check-for-type-mismatch Γ check)
      λ kd tp → just "Expected a kind classifier, but got a type")
    (either-else' tk (λ tp kd → just "Expected a type classifier, but got a kind")
      (check-for-kind-mismatch Γ check))

summary-data : {ed : exprd} → (name : string) → ctxt → ⟦ ed ⟧ → tagged-val
summary-data name Γ t = strRunTag "summary" Γ (strVar name >>str strAdd " : " >>str to-stringe t)

head-kind : ctxt → kind → tagged-val
head-kind = to-string-tag "the kind of the head"

head-type : ctxt → type → tagged-val
head-type = to-string-tag "the type of the head"

arg-type : ctxt → type → tagged-val
arg-type = to-string-tag "computed arg type"

arg-exp-type : ctxt → type → tagged-val
arg-exp-type = to-string-tag "expected arg type"

type-app-head : ctxt → type → tagged-val
type-app-head = to-string-tag "the head"

term-app-head : ctxt → term → tagged-val
term-app-head = to-string-tag "the head"

term-argument : ctxt → term → tagged-val
term-argument = to-string-tag "the argument"

type-argument : ctxt → type → tagged-val
type-argument = to-string-tag "the argument"

contextual-type-argument : ctxt → type → tagged-val
contextual-type-argument = to-string-tag "contextual type arg"

arg-argument : ctxt → arg → tagged-val
arg-argument Γ = either-else (term-argument Γ) (type-argument Γ) ∘ arg-to-tmtp

kind-data : ctxt → kind → tagged-val
kind-data = to-string-tag "kind"

kind-data-if : ctxt → maybe kind → 𝕃 tagged-val
kind-data-if Γ (just k) = [ kind-data Γ k ]
kind-data-if _ nothing = []

super-kind-data : tagged-val
super-kind-data = strRunTag "superkind" empty-ctxt $ strAdd "□"

symbol-data : string → tagged-val
symbol-data = strRunTag "symbol" empty-ctxt ∘ strAdd

tk-data : ctxt → tpkd → tagged-val
tk-data Γ (Tkk k) = kind-data Γ k
tk-data Γ (Tkt t) = type-data Γ t

checking-to-string : checking-mode → string
checking-to-string checking = "checking"
checking-to-string synthesizing = "synthesizing"
checking-to-string untyped = "untyped"

checking-data : checking-mode → tagged-val
checking-data = strRunTag "checking-mode" empty-ctxt ∘' strAdd ∘' checking-to-string

checked-meta-var : var → tagged-val
checked-meta-var = strRunTag "checked meta-var" empty-ctxt ∘ strAdd

ll-data : exprd → tagged-val
ll-data = strRunTag "language-level" empty-ctxt ∘' strAdd ∘' exprd-name

ll-data-term = ll-data TERM
ll-data-type = ll-data TYPE
ll-data-kind = ll-data KIND

binder-data : ctxt → posinfo → var → (atk : tpkd) → erased? → maybe (if tk-is-type atk then term else type) → (from to : posinfo) → tagged-val
binder-data Γ pi x atk me val s e =
  strRunTag "binder" Γ $
  strAdd "symbol:" >>str
  strAdd x >>str
  atk-val atk val >>str
  strAdd "§from:" >>str
  strAdd s >>str
  strAdd "§to:" >>str
  strAdd e >>str
  loc >>str
  strErased?
  where
  loc : strM
  loc = strAdd "§fn:" >>str strAdd (ctxt.fn Γ) >>str strAdd "§pos:" >>str strAdd pi
  strErased? : strM
  strErased? =
    strAdd "§erased:" >>str
    strAdd (if me then "true" else "false")
  val? : ∀ {ed} → maybe ⟦ ed ⟧ → strM
  val? = maybe-else strEmpty λ x →
    strAdd "§value:" >>str
    to-stringe x
  atk-val : (atk : tpkd) → maybe (if tk-is-type atk then term else type) → strM
  atk-val (Tkt T) t? =
    strAdd "§type:" >>str
    to-stringe T >>str
    val? t?
  atk-val (Tkk k) T? =
    strAdd "§kind:" >>str
    to-stringe k >>str
    val? T?

punctuation-data : tagged-val
punctuation-data = strRunTag "punctuation" empty-ctxt $ strAdd "true"

not-for-navigation : tagged-val
not-for-navigation = strRunTag "not-for-navigation" empty-ctxt $ strAdd "true"

is-erased : type → 𝔹
is-erased (TpVar _) = tt
is-erased _ = ff

keywords = "keywords"
keyword-application = "application"
keyword-locale = "meta-var-locale"

keywords-data : 𝕃 string → tagged-val
keywords-data kws = keywords , h kws , [] where
  h : 𝕃 string → rope
  h [] = [[]]
  h (k :: []) = [[ k ]]
  h (k :: ks) = [[ k ]] ⊹⊹ [[ " " ]] ⊹⊹ h ks

keywords-app : (is-locale : 𝔹) → tagged-val
keywords-app l = keywords-data ([ keyword-application ] ++ (if l then [ keyword-locale ] else []))

keywords-app-if-typed : checking-mode → (is-locale : 𝔹) → 𝕃 tagged-val
keywords-app-if-typed untyped l = []
keywords-app-if-typed _ l = [ keywords-app l ]

error-if-not-eq : ctxt → type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq Γ (TpEq t1 t2) tvs = expected-type Γ (TpEq t1 t2) :: tvs , nothing
error-if-not-eq Γ tp tvs = expected-type Γ tp :: tvs , just "This term is being checked against the following type, but an equality type was expected"

error-if-not-eq-maybe : ctxt → maybe type → 𝕃 tagged-val → 𝕃 tagged-val × err-m
error-if-not-eq-maybe Γ (just tp) = error-if-not-eq Γ tp
error-if-not-eq-maybe _ _ tvs = tvs , nothing

params-data : ctxt → params → 𝕃 tagged-val
params-data _ [] = []
params-data Γ ps = [ params-to-string-tag "parameters" Γ ps ]

--------------------------------------------------
-- span-creating functions
--------------------------------------------------

Star-name : string
Star-name = "Star"

parens-span : posinfo → posinfo → span
parens-span pi pi' = mk-span "parentheses" pi pi' [] nothing

data decl-class : Set where
  decl-param : decl-class
  decl-index : decl-class

decl-class-name : decl-class → string
decl-class-name decl-param = "parameter"
decl-class-name decl-index = "index"

Decl-span : ctxt → decl-class → posinfo → posinfo → var → tpkd → erased? → posinfo → posinfo → span
Decl-span Γ dc pi pi' v atk me pi'' pi''' = mk-span ((if tk-is-type atk then "Term " else "Type ") ^ (decl-class-name dc))
                                      pi pi''' [ binder-data Γ pi' v atk me nothing pi'' pi''' ] nothing

TpVar-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
TpVar-span Γ pi v check tvs =
  mk-span name pi (posinfo-plus-str pi (unqual-local v))
    (checking-data check :: ll-data-type :: var-location-data Γ v :: symbol-data (unqual-local v) :: tvs)
  where
  v' = unqual-local v
  name = if stringset-contains (ctxt.μ̲ Γ) (qualif-var Γ v)
           then "Datatype variable"
           else "Type variable"

Var-span : ctxt → posinfo → string → checking-mode → 𝕃 tagged-val → err-m → span
Var-span Γ pi v check tvs =
  mk-span name pi (posinfo-plus-str pi v')
    (checking-data check :: ll-data-term :: var-location-data Γ v :: symbol-data v' :: tvs)
  where
  v' = unqual-local v
  name : string
  name with qual-lookup Γ v'
  ...| just (_ , _ , ctr-def _ _ _ _ _ , _) = "Constructor variable"
  ...| _ = "Term variable"

KdVar-span : ctxt → (posinfo × var) → (end-pi : posinfo) → params → checking-mode → 𝕃 tagged-val → err-m → span
KdVar-span Γ (pi , v) pi' ps check tvs =
  mk-span "Kind variable" pi pi'
    (checking-data check :: ll-data-kind :: var-location-data Γ v :: symbol-data (unqual-local v) :: super-kind-data :: (params-data Γ ps ++ tvs))

var-span-with-tags : erased? → ctxt → posinfo → string → checking-mode → tpkd → 𝕃 tagged-val → err-m → span
var-span-with-tags _ Γ pi x check (Tkk k) tags = TpVar-span Γ pi x check ({-keywords-data-var ff ::-} [ kind-data Γ k ] ++ tags)
var-span-with-tags e Γ pi x check (Tkt t) tags = Var-span Γ pi x check ({-keywords-data-var e ::-} [ type-data Γ t ] ++ tags)

var-span :  erased? → ctxt → posinfo → string → checking-mode → tpkd → err-m → span
var-span e Γ pi x check tk = var-span-with-tags e Γ pi x check tk []

redefined-var-span : ctxt → posinfo → var → span
redefined-var-span Γ pi x = mk-span "Variable definition" pi (posinfo-plus-str pi x)
                             [ var-location-data Γ x ] (just "This symbol was defined already")

TpAppt-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
TpAppt-span pi pi' check tvs = mk-span "Application of a type to a term" pi pi' (checking-data check :: ll-data-type :: tvs)

TpApp-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
TpApp-span pi pi' check tvs = mk-span "Application of a type to a type" pi pi' (checking-data check :: ll-data-type :: tvs)

App-span : (is-locale : 𝔹) → posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
App-span l pi pi' check tvs = mk-span "Application of a term to a term" pi pi' (checking-data check :: ll-data-term :: keywords-app-if-typed check l ++ tvs)

AppTp-span : (is-locale : 𝔹) → posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
AppTp-span l pi pi' check tvs = mk-span "Application of a term to a type" pi pi' (checking-data check :: ll-data-term :: keywords-app-if-typed check l ++ tvs)

TpQuant-span : ctxt → erased? → posinfo → posinfo → var → tpkd → ex-tp → checking-mode → 𝕃 tagged-val → err-m → span
TpQuant-span Γ me pi pi' x atk body check tvs err =
  let err-if-type-pi = ifMaybej ( ~ (tk-is-type atk || me))
                          "Π-types must bind a term, not a type (use ∀ instead)"
      name = if me then "Implicit dependent function type" else "Dependent function type" in
  mk-span name pi (type-end-pos body) (checking-data check :: ll-data-type :: binder-data Γ pi' x atk me nothing (type-start-pos body) (type-end-pos body) :: tvs) (if isJust err-if-type-pi then err-if-type-pi else err)

TpLambda-span : ctxt → posinfo → posinfo → var → tpkd → ex-tp → checking-mode → 𝕃 tagged-val → err-m → span
TpLambda-span Γ pi pi' x atk body check tvs =
  mk-span "Type-level lambda abstraction" pi (type-end-pos body)
    (checking-data check :: ll-data-type :: binder-data Γ pi' x atk NotErased nothing (type-start-pos body) (type-end-pos body) :: tvs)

Iota-span : ctxt → posinfo → posinfo → var → type → ex-tp → checking-mode → 𝕃 tagged-val → err-m → span
Iota-span Γ pi pi' x t1 t2 check tvs = mk-span "Iota-abstraction" pi (type-end-pos t2) (explain "A dependent intersection type" :: checking-data check :: binder-data Γ pi' x (Tkt t1) ff nothing (type-start-pos t2) (type-end-pos t2) :: ll-data-type :: tvs)

TpArrow-span : ex-tp → ex-tp → checking-mode → 𝕃 tagged-val → err-m → span
TpArrow-span t1 t2 check tvs = mk-span "Arrow type" (type-start-pos t1) (type-end-pos t2) (checking-data check :: ll-data-type :: tvs)

TpEq-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
TpEq-span pi pi' check tvs = mk-span "Equation" pi pi'
                             (explain "Equation between terms" :: checking-data check :: ll-data-type :: tvs)

Star-span : posinfo → checking-mode → err-m → span
Star-span pi check = mk-span Star-name pi (posinfo-plus pi 1) (checking-data check :: [ ll-data-kind ])

KdAbs-span : ctxt → posinfo → posinfo → var → tpkd → ex-kd → checking-mode → err-m → span
KdAbs-span Γ pi pi' x atk k check =
  mk-span "Pi kind" pi (kind-end-pos k)
    (checking-data check :: ll-data-kind :: binder-data Γ pi' x atk ff nothing (kind-start-pos k) (kind-end-pos k) :: [ super-kind-data ])

KdArrow-span : ex-tk → ex-kd → checking-mode → err-m → span
KdArrow-span k k' check = mk-span "Arrow kind" (tk-start-pos k) (kind-end-pos k') (checking-data check :: ll-data-kind :: [ super-kind-data ])

{- [[file:../cedille-mode.el::(defun%20cedille-mode-filter-out-special(data)][Frontend]]  -}
special-tags : 𝕃 string
special-tags =
  "symbol" :: "location" :: "language-level" :: "checking-mode" :: "summary"
  :: "binder" :: "bound-value" :: "keywords" :: []

error-span-filter-special : error-span → error-span
error-span-filter-special (mk-error-span dsc pi pi' tvs msg) =
  mk-error-span dsc pi pi' tvs' msg
  where tvs' = (flip filter) tvs λ tag → list-any (_=string (fst tag)) special-tags

erasure : ctxt → term → tagged-val
erasure Γ t = to-string-tag "erasure" Γ (erase t)

erased-marg-span : ctxt → posinfo → posinfo → maybe type → span
erased-marg-span Γ pi pi' mtp = mk-span "Erased module parameter" pi pi'
  (maybe-else [] (λ tp → [ type-data Γ tp ]) mtp)
  (just "An implicit module parameter variable occurs free in the erasure of the term")

Lam-span-erased : erased? → string
Lam-span-erased Erased = "Erased lambda abstraction (term-level)"
Lam-span-erased NotErased = "Lambda abstraction (term-level)"

Lam-span : ctxt → checking-mode → posinfo → posinfo → erased? → var → tpkd → ex-tm → 𝕃 tagged-val → err-m → span
Lam-span Γ c pi pi' l x atk t tvs = mk-span (Lam-span-erased l) pi (term-end-pos t)
                                           (ll-data-term :: binder-data Γ pi' x atk l nothing (term-start-pos t) (term-end-pos t) :: checking-data c :: tvs)

compileFail-in : ctxt → term → 𝕃 tagged-val × err-m
compileFail-in Γ t with is-free-in compileFail-qual | t
...| is-free | tₒ with erase tₒ | hnf Γ (record unfold-all { unfold-defs = ff }) tₒ
...| tₑ | tₙ with is-free tₒ
...| ff = [] , nothing
...| tt with is-free tₙ | is-free tₑ
...| tt | _ = [ to-string-tag "normalized term" Γ tₙ ] , just "compileFail occurs in the normalized term"
...| ff | ff = [ to-string-tag "the term" Γ tₒ ] , just "compileFail occurs in an erased position"
...| ff | tt = [] , nothing

DefTerm-span : ctxt → posinfo → var → (checked : checking-mode) → maybe type → term → posinfo → 𝕃 tagged-val → span
DefTerm-span Γ pi x checked tp t pi' tvs =
  h ((h-summary tp) ++ ({-erasure Γ t ::-} tvs)) pi x checked tp pi'
  where h : 𝕃 tagged-val → posinfo → var → (checked : checking-mode) → maybe type → posinfo → span
        h tvs pi x checking _ pi' =
          mk-span "Term-level definition (checking)" pi pi' tvs nothing
        h tvs pi x _ (just tp) pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' (to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs pi x _ nothing pi' =
          mk-span "Term-level definition (synthesizing)" pi pi' ((strRunTag "synthesized type" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing
        h-summary : maybe type → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just tp) = (checking-data checking :: [ summary-data x Γ tp ])

CheckTerm-span : ctxt → (checked : checking-mode) → maybe type → ex-tm → posinfo → 𝕃 tagged-val → span
CheckTerm-span Γ checked tp t pi' tvs =
  h ({-erasure Γ t ::-} tvs) checked tp (term-start-pos t) pi'
  where h : 𝕃 tagged-val → (checked : checking-mode) → maybe type → posinfo → posinfo → span
        h tvs checking _ pi pi' =
          mk-span "Checking a term" pi pi' (checking-data checking :: tvs) nothing
        h tvs _ (just tp) pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: to-string-tag "synthesized type" Γ tp :: tvs) nothing
        h tvs _ nothing pi pi' =
          mk-span "Synthesizing a type for a term" pi pi' (checking-data synthesizing :: (strRunTag "synthesized type" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing

normalized-type : ctxt → type → tagged-val
normalized-type = to-string-tag "normalized type"

DefType-span : ctxt → posinfo → var → (checked : checking-mode) → maybe kind → type → posinfo → 𝕃 tagged-val → span
DefType-span Γ pi x checked mk tp pi' tvs =
  h ((h-summary mk) ++ tvs) checked mk
  where h : 𝕃 tagged-val → checking-mode → maybe kind → span
        h tvs checking _ = mk-span "Type-level definition (checking)" pi pi' tvs nothing
        h tvs _ (just k) =
          mk-span "Type-level definition (synthesizing)" pi pi' (to-string-tag "synthesized kind" Γ k :: tvs) nothing
        h tvs _ nothing =
          mk-span "Type-level definition (synthesizing)" pi pi' ( (strRunTag "synthesized kind" empty-ctxt $ strAdd "[nothing]") :: tvs) nothing
        h-summary : maybe kind → 𝕃 tagged-val
        h-summary nothing = [(checking-data synthesizing)]
        h-summary (just k) = (checking-data checking :: [ summary-data x Γ k ])

DefKind-span : ctxt → posinfo → var → kind → posinfo → span
DefKind-span Γ pi x k pi' = mk-span "Kind-level definition" pi pi' (kind-data Γ k :: [ summary-data x Γ (Var "□") ]) nothing

DefDatatype-span : ctxt → posinfo → posinfo → var → params → (reg Mu bound : kind) → (mu : type) → (cast : type) → ctrs → ex-kd → posinfo → span
DefDatatype-span Γ pi pi' x ps k kₘᵤ kₓ Tₘᵤ Tₜₒ cs kₑₓ pi'' =
  mk-span "Datatype definition" pi pi'' (binder-data Γ pi' x (Tkk kₓ) ff nothing (kind-end-pos kₑₓ) pi'' :: summary-data x Γ k :: summary-data (data-Is/ x) Γ kₘᵤ :: summary-data (data-is/ x) Γ Tₘᵤ :: summary-data (data-to/ x) Γ Tₜₒ :: to-string-tag (data-Is/ x) Γ kₘᵤ :: to-string-tag (data-is/ x) Γ Tₘᵤ :: to-string-tag (data-to/ x) Γ Tₜₒ :: []) nothing

{-unchecked-term-span : term → span
unchecked-term-span t = mk-span "Unchecked term" (term-start-pos t) (term-end-pos t)
                           (ll-data-term :: not-for-navigation :: [ explain "This term has not been type-checked"]) nothing-}

Beta-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Beta-span pi pi' check tvs = mk-span "Beta axiom" pi pi'
                     (checking-data check :: ll-data-term :: explain "A term constant whose type states that β-equal terms are provably equal" :: tvs)

hole-span : ctxt → posinfo → maybe type → checking-mode → 𝕃 tagged-val → span
hole-span Γ pi tp check tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (checking-data check :: ll-data-term :: expected-type-if Γ tp ++ tvs)
    (just "This hole remains to be filled in")

tp-hole-span : ctxt → posinfo → maybe kind → checking-mode → 𝕃 tagged-val → span
tp-hole-span Γ pi k check tvs =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (checking-data check :: ll-data-type :: expected-kind-if Γ k ++ tvs)
    (just "This hole remains to be filled in")

kd-hole-span : posinfo → checking-mode → span
kd-hole-span pi check =
  mk-span "Hole" pi (posinfo-plus pi 1)
    (checking-data check :: ll-data-kind :: [])
    (just "This hole remains to be filled in")

expected-to-string : checking-mode → string
expected-to-string checking = "expected"
expected-to-string synthesizing = "synthesized"
expected-to-string untyped = "untyped"

Epsilon-span : posinfo → left-right → minus? → ex-tm → checking-mode → 𝕃 tagged-val → err-m → span
Epsilon-span pi lr m t check tvs = mk-span "Epsilon" pi (term-end-pos t)
                                         (checking-data check :: ll-data-term :: tvs ++
                                         [ explain ("Normalize " ^ side lr ^ " of the "
                                                   ^ expected-to-string check ^ " equation, using " ^ maybeMinus-description m
                                                   ^ " reduction" ) ])
  where side : left-right → string
        side EpsLeft = "the left-hand side"
        side EpsRight = "the right-hand side"
        side EpsBoth = "both sides"
        maybeMinus-description : minus? → string
        maybeMinus-description EpsHnf = "head"
        maybeMinus-description EpsHanf = "head-applicative"

optGuide-spans : ctxt → maybe ex-guide → checking-mode → spanM ⊤
optGuide-spans Γ nothing _ = spanMok
optGuide-spans Γ (just (ExGuide pi x tp)) expected =
  spanM-add (Var-span Γ pi x expected [] nothing)

Rho-span : posinfo → ex-tm → ex-tm → checking-mode → 𝔹 → ℕ ⊎ var → 𝕃 tagged-val → err-m → span
Rho-span pi t t' expected r (inj₂ x) tvs =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: explain ("Rewrite all places where " ^ x ^ " occurs in the " ^ expected-to-string expected ^ " type, using an equation. ") :: tvs)
Rho-span pi t t' expected r (inj₁ numrewrites) tvs err =
  mk-span "Rho" pi (term-end-pos t')
    (checking-data expected :: ll-data-term :: tvs ++
    (explain ("Rewrite terms in the "
      ^ expected-to-string expected ^ " type, using an equation. "
      ^ (if r then "" else "Do not ") ^ "Beta-reduce the type as we look for matches") :: fst h)) (snd h)
  where h : 𝕃 tagged-val × err-m
        h = if isJust err
              then [] , err
              else if numrewrites =ℕ 0
                then [] , just "No rewrites could be performed"
                else [ strRunTag "Number of rewrites" empty-ctxt (strAdd $ ℕ-to-string numrewrites) ] , err

Phi-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Phi-span pi pi' expected tvs = mk-span "Phi" pi pi' (checking-data expected :: ll-data-term :: tvs)

Chi-span : ctxt → posinfo → maybe type → ex-tm → checking-mode → 𝕃 tagged-val → err-m → span
Chi-span Γ pi m t' check tvs = mk-span "Chi" pi (term-end-pos t')  (ll-data-term :: checking-data check :: tvs ++ helper m)
  where helper : maybe type → 𝕃 tagged-val
        helper (just T) =  explain ("Check a term against an asserted type") :: [ to-string-tag "the asserted type" Γ T ]
        helper nothing = [ explain ("Change from checking mode (outside the term) to synthesizing (inside)") ]

VarSigma-span : posinfo → ex-tm → checking-mode → 𝕃 tagged-val → err-m → span
VarSigma-span pi t check tvs =
  mk-span "VarSigma" pi (term-end-pos t)
     (ll-data-term :: checking-data check :: explain "Swap the sides of the equation synthesized for the body of this term" :: tvs)

Delta-span : posinfo → ex-tm → checking-mode → 𝕃 tagged-val → err-m → span
Delta-span pi t check tvs =
  mk-span "Delta" pi (term-end-pos t)
    (ll-data-term :: explain "Prove anything you want from a contradiction" :: checking-data check :: tvs)

Opaque-span : posinfo → posinfo → span
Opaque-span p₁ p₂ =
  mk-span "Opaque" p₁ p₂ [ explain "Mark a definition as opaque, for the purposes of conversion checking" ] nothing

Open-span : opacity → posinfo → var → ex-tm → checking-mode → 𝕃 tagged-val → err-m → span
Open-span o pi x t check tvs =
  elim-pair (if o
    then ("Open" , "Open an opaque definition")
    else ("Close" , "Hide a definition")) λ name expl →
  mk-span name pi (term-end-pos t)
    (ll-data-term :: explain expl :: checking-data check :: tvs)

motive-label : string
motive-label = "the motive"

the-motive : ctxt → type → tagged-val
the-motive = to-string-tag motive-label

Theta-span : ctxt → posinfo → theta → ex-tm → 𝕃 lterm → checking-mode → 𝕃 tagged-val → err-m → span
Theta-span Γ pi u t ls check tvs = mk-span "Theta" pi (lterms-end-pos (term-end-pos t) ls) (ll-data-term :: checking-data check :: tvs ++ do-explain u)
  where do-explain : theta → 𝕃 tagged-val
        do-explain Abstract = [ explain ("Perform an elimination with the first term, after abstracting it from the expected type") ]
        do-explain (AbstractVars vs) = [ strRunTag "explanation" Γ (strAdd "Perform an elimination with the first term, after abstracting the listed variables (" >>str vars-to-string vs >>str strAdd ") from the expected type") ]
        do-explain AbstractEq = [ explain ("Perform an elimination with the first term, after abstracting it with an equation "
                                         ^ "from the expected type") ]

Mu-span : ctxt → posinfo → posinfo → (motive? : maybe type) → checking-mode → 𝕃 tagged-val → err-m → span
Mu-span Γ pi pi' motive? check tvs = mk-span "Mu" pi pi' (ll-data-term :: checking-data check :: explain ("Pattern match on a term" ^ (if isJust motive? then ", with a motive" else "")) :: tvs)

Sigma-span : ctxt → posinfo → posinfo → (motive? : maybe type) → checking-mode → 𝕃 tagged-val → err-m → span
Sigma-span Γ pi pi' motive? check tvs = mk-span "Sigma" pi pi' (ll-data-term :: checking-data check :: explain ("Pattern match on a term" ^ (if isJust motive? then ", with a motive" else "")) :: tvs)

pattern-span : posinfo → var → 𝕃 ex-case-arg → span
pattern-span pi x as = mk-span "Pattern" pi (snd $ foldr (λ a r → if fst r then r else (tt , (case a of λ {(ExCaseArg me pi x) → posinfo-plus-str pi x}))) (ff , posinfo-plus-str pi x) as) [] nothing

pattern-clause-span : posinfo → ex-tm → 𝕃 tagged-val → span
pattern-clause-span pi t tvs = mk-span "Pattern clause" pi (term-end-pos t) tvs nothing

pattern-ctr-span : ctxt → posinfo → var → case-args → 𝕃 tagged-val → err-m → span
pattern-ctr-span Γ pi x as tvs =
  mk-span "Pattern constructor" pi (posinfo-plus-str pi x) (checking-data synthesizing :: var-location-data Γ x :: ll-data-term :: symbol-data x :: args-data ++ tvs)
  where
  args-data : 𝕃 tagged-val
  args-data = if iszero (length as) then [] else [ params-to-string-tag "args" Γ (map (λ {(CaseArg me x tk?) → Param me x (maybe-else' tk? (Tkt (TpHole pi-gen)) id)}) as) ]

File-span : ctxt → posinfo → posinfo → string → span
File-span Γ pi pi' filename = mk-span ("Cedille source file (" ^ filename ^ ")") pi pi' (print-file-id-table Γ) nothing

Module-span : posinfo → posinfo → span
Module-span pi pi' = mk-span "Module declaration" pi pi' [ not-for-navigation ] nothing

Module-header-span : posinfo → posinfo → span
Module-header-span pi pi' = mk-span "Module header" pi pi' [ not-for-navigation ] nothing

DefDatatype-header-span : posinfo → span
DefDatatype-header-span pi = mk-span "Data" pi (posinfo-plus-str pi "data") [ not-for-navigation ] nothing

Import-span : posinfo → string → posinfo → 𝕃 tagged-val → err-m → span
Import-span pi file pi' tvs = mk-span ("Import of another source file") pi pi' (("Path" , [[ file ]] , []) :: location-data (file , first-position) :: tvs)

Import-module-span : ctxt → (posinfo × var) → params → 𝕃 tagged-val → err-m → span
Import-module-span Γ (pi , mn) ps tvs = mk-span "Imported module" pi (posinfo-plus-str pi mn) (params-data Γ ps ++ tvs)

punctuation-span : string → posinfo → posinfo → span
punctuation-span name pi pi'  = mk-span name pi pi' ( punctuation-data ::  not-for-navigation :: [] ) nothing

whitespace-span : posinfo → posinfo → span
whitespace-span pi pi'  = mk-span "Whitespace" pi pi' [ not-for-navigation ] nothing

comment-span : posinfo → posinfo → span
comment-span pi pi'  = mk-span "Comment" pi pi' [ not-for-navigation ] nothing

IotaPair-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaPair-span pi pi' c tvs =
  mk-span "Iota pair" pi pi' (explain "Inhabit a iota-type (dependent intersection type)" :: checking-data c :: ll-data-term :: tvs)

IotaProj-span : ex-tm → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
IotaProj-span t pi' c tvs = mk-span "Iota projection" (term-start-pos t) pi' (checking-data c :: ll-data-term :: tvs)

Let-span : erased? → posinfo → posinfo → checking-mode → 𝕃 tagged-val → err-m → span
Let-span me pi pi' c tvs =
  mk-span (if me then "Erased Term Let" else "Term Let") pi pi' (ll-data-term :: checking-data c :: tvs)

TpLet-span : posinfo → posinfo → checking-mode → 𝕃 tagged-val → span
TpLet-span pi pi' c tvs =
  mk-span "Type Let" pi pi' (ll-data-type :: checking-data c :: tvs) nothing


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

-- Let us assume that extensionality of functions cannot be proved
-- inside "plain" Agda. In that case the code below shows that the
-- REWRITE functionality is not a conservative extension, even if we
-- only use propositional equality as the rewriting relation, and do
-- not use any postulates.

-- Jesper, 2019-05-13: This example is not confluent!

module RewriteExt-confluence where

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

data Unit : Set where
  unit : Unit

module _ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
         (f≡g : ∀ x → f x ≡ g x) where

  private

    id : Unit → (x : A) → B x → B x
    id unit _ x = x

    f≡g′ : ∀ u x → id u x (f x) ≡ g x
    f≡g′ unit = f≡g

    {-# REWRITE f≡g′ #-}

    ext′ : ∀ u → (λ x → id u x (f x)) ≡ g
    ext′ u = refl

  ext : f ≡ g
  ext = ext′ unit


text:
module #15 where

{-
  Show that indiscernability of identicals follows from path induction
-}

open import Data.Product
open import Relation.Binary.PropositionalEquality

id : ∀{x}{A : Set x} → A → A
id x = x

ind₌ : ∀{a}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set) → ((x : A) → C x x refl) → (x y : A) → (p : x ≡ y) → C x y p
ind₌ C c x y p rewrite p =  c y

based-ind₌ : ∀{x}{A : Set x} → (a : A) → (C : (x : A) → (a ≡ x) → Set) → C a refl → (x : A) → (p : a ≡ x) → C x p
based-ind₌ a C c b p rewrite p = c

indiscernability-of-identicals : {A : Set}{C : A → Set} → Σ[ f ∈ ((x y : A) → (x ≡ y) → C x → C y) ]((x : A) → f x x refl ≡ id {A = C x})
indiscernability-of-identicals {A} {C} = transport , (λ _ → refl)
  where
    transport : (x y : A) → (p : x ≡ y) → C x → C y
    transport = ind₌ (λ x y _ → C x → C y) (λ x z → z)


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.CommRings where

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

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Categories.Category

open Category
open CommRingHoms

CommRingsCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ
ob CommRingsCategory                     = CommRing _
Hom[_,_] CommRingsCategory               = CommRingHom
id CommRingsCategory {R}                 = idCommRingHom R
_⋆_ CommRingsCategory {R} {S} {T}        = compCommRingHom R S T
⋆IdL CommRingsCategory {R} {S}           = compIdCommRingHom {R = R} {S}
⋆IdR CommRingsCategory {R} {S}           = idCompCommRingHom {R = R} {S}
⋆Assoc CommRingsCategory {R} {S} {T} {U} = compAssocCommRingHom {R = R} {S} {T} {U}
isSetHom CommRingsCategory               = isSetRingHom _ _

max_stars_repo_name: mzeuner/cubical

max_issues_repo_name: mzeuner/cubical

max_forks_repo_name: mzeuner/cubical


text:
open import Data.Bool as Bool using (Bool; false; true; if_then_else_; not)
open import Data.String using (String)
open import Data.Nat using (ℕ; _+_; _≟_; suc; _>_; _<_; _∸_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List as l using (List; filter; map; take; foldl; length)
open import Data.List.Properties
open import Data.Maybe using (to-witness)
open import Data.Fin using (fromℕ; _-_; zero)
open import Data.Product as Prod using (∃; ∃₂; _×_; _,_; Σ)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Level using (Level)
open import Data.Vec as v using (Vec; fromList; toList; last; length; []; _∷_; [_]; _∷ʳ_; _++_; lookup; head; initLast; filter; map)
open import Data.Vec.Bounded as vb using ([]; _∷_; fromVec; filter; Vec≤)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; _≗_; cong₂)
open import Data.Nat.Properties using (+-comm)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (does)
open import Data.Vec.Bounded.Base using (padRight; ≤-cast)
import Data.Nat.Properties as ℕₚ
open import Relation.Nullary.Decidable.Core using (dec-false)

-- essentially a List String

record Todo : Set where
  field
    text      : String

AddTodo :
  ∀ {n : ℕ} →
    (Vec Todo n) →
      String →
        (Vec Todo (1 + n))
AddTodo todos text =
  todos ∷ʳ
  record
    { text = text
    }

AddTodoAddsNewListItem :
  ∀ {n : ℕ} →
    (todos : Vec Todo n) (text : String) →
      v.length (AddTodo todos text) ≡ v.length todos + 1
AddTodoAddsNewListItem []    text = refl
AddTodoAddsNewListItem todos text = +-comm 1 (v.length todos)

AddTodoLastAddedElementIsTodo :
  ∀ {n} (todos : Vec Todo n) (text : String) →
    last (AddTodo todos text) ≡
      record
        { text = text
        }
AddTodoLastAddedElementIsTodo todos text = vecLast todos
  where
    vecLast : ∀ {a} {A : Set a} {l} {n : ℕ} (xs : Vec A n) → last (xs ∷ʳ l) ≡ l
    vecLast []       = refl
    vecLast (_ ∷ xs) = P.trans (prop (xs ∷ʳ _)) (vecLast xs)
      where
        prop : ∀ {a} {A : Set a} {n x} (xs : Vec A (suc n)) → last (x v.∷ xs) ≡ last xs
        prop xs with initLast xs
        ...        | _ , _ , refl = refl

AddTodoAddedTodoHasGivenText :
  ∀ {n} (todos : Vec Todo n) (text : String) →
    Todo.text (last (AddTodo todos text)) ≡ text
AddTodoAddedTodoHasGivenText todos text
  rewrite
    (AddTodoLastAddedElementIsTodo todos text) =
      refl

max_stars_repo_name: frankymacster/redux

max_issues_repo_name: frankymacster/redux

max_forks_repo_name: frankymacster/redux


text:
{-# OPTIONS --no-termination-check #-}
module optionsPragma where

-- Only goes through with the termination checker turned off.
Foo : Set
Foo = Foo


text:
data ⊥ : Set where

data Bool : Set where
  false true : Bool

data _≡_ (x : Bool) : Bool → Set where
  refl : x ≡ x

true≠false : false ≡ true → ⊥
true≠false ()

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just : A → Maybe A

data Eq {A : Set} (_≈_ : A → A → Set) : Maybe A → Maybe A → Set where
  just    : ∀ {x y} (x≈y : x ≈ y) → Eq _≈_ (just x) (just y)
  nothing : Eq _≈_ nothing nothing

drop-just : ∀ {A : Set} {_≈_ : A → A → Set} {x y : A} →
            Eq _≈_ (just x) (just y) → x ≈ y
drop-just (just x≈y) = x≈y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Control.Monad.Writer where

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.Identity
open import Control.Monad.Transformer

record WriterT {a} (W : Set a) (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor writerT
  field runWriterT : M (A × W)

open WriterT public

module _ {a} {W : Set a} {M : Set a → Set a} where

  instance
    FunctorWriterT : {{_ : Functor M}} → Functor {a = a} (WriterT W M)
    runWriterT (fmap {{ FunctorWriterT }} f m) = first f <$> runWriterT m

    FunctorZeroWriterT : {{_ : FunctorZero M}} → FunctorZero {a = a} (WriterT W M)
    runWriterT (empty {{FunctorZeroWriterT}}) = empty

    AlternativeWriterT : {{_ : Alternative M}} → Alternative {a = a} (WriterT W M)
    runWriterT (_<|>_ {{AlternativeWriterT}} x y) = runWriterT x <|> runWriterT y

  module _ {{_ : Monoid W}} {{_ : Monad M}} where

    private
      bindWriterT : ∀ {A B} → WriterT W M A → (A → WriterT W M B) → WriterT W M B
      runWriterT (bindWriterT m f) = do
        (x , w₁) ← runWriterT m
        (y , w₂) ← (runWriterT (f x))
        return (y , w₁ <> w₂)

    instance
      ApplicativeWriterT : Applicative {a = a} (WriterT W M)
      runWriterT (pure {{ApplicativeWriterT}} x) = return (x , mempty)
      _<*>_ {{ApplicativeWriterT}} = monadAp bindWriterT

      MonadWriterT : Monad {a = a} (WriterT W M)
      _>>=_  {{MonadWriterT}} = bindWriterT

    liftWriterT : {A : Set a} → M A → WriterT W M A
    runWriterT (liftWriterT m) = (_, mempty) <$> m

    writer : {A : Set a} → A × W → WriterT W M A
    runWriterT (writer (x , w)) = return (x , w)

    tell : W → WriterT W M ⊤′
    runWriterT (tell w) = return (tt , w)

    listens : {A B : Set a} → (W → B) → WriterT W M A → WriterT W M (A × B)
    runWriterT (listens f m) = do
      (x , w) ← runWriterT m
      return ((x , f w) , w)

    listen : {A : Set a} → WriterT W M A → WriterT W M (A × W)
    listen = listens id

    pass : {A : Set a} → WriterT W M (A × (W → W)) → WriterT W M A
    runWriterT (pass m) = do
      ((x , f) , w) ← runWriterT m
      return (x , f w)

    censor : {A : Set a} → (W → W) → WriterT W M A → WriterT W M A
    censor f m = pass ((_, f) <$> m)

instance
  TransformerWriterT : ∀ {a} {W : Set a} {{_ : Monoid W}} → Transformer (WriterT W)
  lift {{TransformerWriterT}} = liftWriterT

Writer : ∀ {a} (W : Set a) (A : Set a) → Set a
Writer W = WriterT W Identity

runWriter : ∀ {a} {W : Set a} {A : Set a} → Writer W A → A × W
runWriter m = runIdentity (runWriterT m)

execWriter : ∀ {a} {W : Set a} {A : Set a} → Writer W A → W
execWriter = snd ∘ runWriter

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
------------------------------------------------------------------------------
-- A Peano arithmetic proof without using a where clause
------------------------------------------------------------------------------

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

module LogicalFramework.CommAddition where

open import Common.FOL.Relation.Binary.EqReasoning

open import PA.Axiomatic.Standard.Base

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

postulate
  +-rightIdentity : ∀ n → n + zero ≡ n
  x+Sy≡S[x+y]     : ∀ m n → m + succ n ≡ succ (m + n)
  succCong        : ∀ {m n} → m ≡ n → succ m ≡ succ n

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity = PA₃

A : ℕ → Set
A m = ∀ n → m + n ≡ n + m

A0 : A zero
A0 n = zero + n   ≡⟨ +-leftIdentity n ⟩
       n          ≡⟨ sym (+-rightIdentity n) ⟩
       n + zero   ∎

is : ∀ m → A m → A (succ m)
is m ih n = succ m + n   ≡⟨ PA₄ m n ⟩
            succ (m + n) ≡⟨ succCong (ih n) ⟩
            succ (n + m) ≡⟨ sym (x+Sy≡S[x+y] n m) ⟩
            n + succ m   ∎

+-comm : ∀ m n → m + n ≡ n + m
+-comm = ℕ-ind A A0 is

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module 747Decidable where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym) -- added sym
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _≤_; z≤n; s≤s)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using ()
  renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)

-- Copied from 747Isomorphism.

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

-- Copied from 747Relations.

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

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

-- Recall that the constructors for _≤_ are z≤n and s≤s.

-- Here are a couple of examples to show how to prove inequalities
-- (or their negations).

2≤4 : 2 ≤ 4
2≤4 = {!!}

¬4≤2 : ¬ (4 ≤ 2)
¬4≤2 = {!!}

-- This should be familiar.

data Bool : Set where
  true  : Bool
  false : Bool

-- We can define a Boolean comparison function.

infix 4 _≤ᵇ_

_≤ᵇ_ : ℕ → ℕ → Bool
m ≤ᵇ n = {!!}

-- PLFA steps through these computations using equational reasoning.

_ : (2 ≤ᵇ 4) ≡ true
_ =  refl

_ : (4 ≤ᵇ 2) ≡ false
_ = refl

-- Relating evidence and computation.

T : Bool → Set
T true   =  ⊤
T false  =  ⊥

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ b t = {!!}

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T e = {!!}

≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ m n t = {!!}

≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)
≤→≤ᵇ m≤n = {!!}

-- Getting the best of both worlds!

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

-- Helpers for defining _≤?_
-- If you don't use these, the examples below won't normalize.

¬s≤z : ∀ {m : ℕ} → ¬ (suc m ≤ zero)
¬s≤z = {!!}

¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n)
¬s≤s = {!!}

-- Decidable ≤.

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤? n = {!!}

_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
_ = refl

_ : 4 ≤? 2 ≡ no (¬s≤s (¬s≤s ¬s≤z))
_ = refl

-- We can also evaluate the LHS of these using C-c C-n.

-- 747/PLFA exercise: DecLT (3 point)
-- Decidable strict equality.
-- You will need these helper functions as we did above.

¬z<z : ¬ (zero < zero)
¬z<z = {!!}

¬s<s : ∀ {m n : ℕ} → ¬ (m < n) → ¬ (suc m < suc n)
¬s<s = {!!}

¬s<z : ∀ {n : ℕ} → ¬ (suc n < zero)
¬s<z = {!!}

_<?_ : ∀ (m n : ℕ) → Dec (m < n)
m <? n = {!!}

-- Some tests.

_ : 2 <? 4 ≡ yes (s<s (s<s (z<s)))
_ = refl

_ : 4 <? 2 ≡ no (¬s<s (¬s<s ¬s<z))
_ = refl

_ : 3 <? 3 ≡ no (¬s<s (¬s<s (¬s<s ¬z<z)))
_ = refl

-- 747/PLFA exercise: DecNatEq (3 points)
-- Decidable equality for natural numbers.

_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n) -- split m,n
m ≡ℕ? n = {!!}

-- Reusing ≤ᵇ and proofs of equivalence with ≤ to decide ≤.

_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?′ n = {!!}

-- Erasing Dec down to Bool (or "isYes").

⌊_⌋ : ∀ {A : Set} → Dec A → Bool
⌊ yes x ⌋ = true
⌊ no x ⌋ = false

_≤ᵇ′_ : ℕ → ℕ → Bool
m ≤ᵇ′ n  =  ⌊ m ≤? n ⌋

-- If D is Dec A, then T ⌊ D ⌋ is inhabited exactly when A is inhabited.

toWitness : ∀ {A : Set} {D : Dec A} → T ⌊ D ⌋ → A
toWitness t = {!!}

fromWitness : ∀ {A : Set} {D : Dec A} → A → T ⌊ D ⌋
fromWitness a = {!!}

-- Similar ideas when it is the "no" witnesses we want to handle.

isNo : ∀ {A : Set} → Dec A → Bool
isNo (yes _) = false
isNo (no _)  = true

toWitnessFalse : ∀ {A : Set} {D : Dec A} → T (isNo D) → ¬ A
toWitnessFalse = {!!}

fromWitnessFalse : ∀ {A : Set} {D : Dec A} → ¬ A → T (isNo D)
fromWitnessFalse = {!!}

-- Agda standard library definitions for use of these.

True : ∀ {A : Set} → (D : Dec A) → Set
True Q = T ⌊ Q ⌋

False : ∀ {A : Set} → (D : Dec A) → Set
False Q = T (isNo Q)

-- A concrete example.

≤ᵇ′→≤ : ∀ {m n : ℕ} → T (m ≤ᵇ′ n) → m ≤ n
≤ᵇ′→≤  =  toWitness

≤→≤ᵇ′ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ′ n)
≤→≤ᵇ′  =  fromWitness

-- Conclusion: use Decidables instead of Booleans!

-- Logical connectives for Decidables.

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
true ∧ true = true
true ∧ false = false
false ∧ y = false

infixr 6 _×-dec_

_×-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A × B)
da ×-dec db = {!!}

infixr 5 _∨_

_∨_ : Bool → Bool → Bool
true ∨ y = true
false ∨ y = y

infixr 5 _⊎-dec_

_⊎-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
da ⊎-dec db = {!!}

not : Bool → Bool
not true  = false
not false = true

¬? : ∀ {A : Set} → Dec A → Dec (¬ A)
¬? da = {!!}

-- A Boolean version of implication.

_⊃_ : Bool → Bool → Bool
true ⊃ true = true
true ⊃ false = false
false ⊃ y = true

_→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
da →-dec db = {!!}

-- 747/PLFA exercise: ErasBoolDec (3 points)
-- Erasure relates boolean and decidable operations.

∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× da db = {!!}

∨-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-× da db = {!!}

not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ da = {!!}

-- 747/PLFA exercise: iff-erasure.

_iff_ : Bool → Bool → Bool
true iff true = true
true iff false = false
false iff true = false
false iff false = true

_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
da ⇔-dec db = {!!}

iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ da db = {!!}

-- Proof by reflection.
-- Or, getting Agda to construct proofs at compile time.

-- A guarded version of monus.

minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus m zero _ = m
minus (suc m) (suc n) (s≤s m≤n) = minus m n m≤n

-- But we have to provide proofs.

_ : minus 5 3 (s≤s (s≤s (s≤s z≤n))) ≡ 2
_ = refl

-- Agda will fill in an implicit record type if it can fill in all fields.
-- Since ⊤ is defined as a record type with no fields...
-- We can get Agda to compute a value of type True (n ≤? m).

_-_ : (m n : ℕ) {n≤m : True (n ≤? m)} → ℕ
_-_ m n {n≤m} = minus m n (toWitness n≤m)

_ : 5 - 3 ≡ 2
_ = refl

-- We will later use this to get Agda to compute parts of proofs
-- that would be annoying for us to provide.

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


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

open import HoTT
open import homotopy.SuspProduct
open import homotopy.SuspSmash
open import homotopy.JoinSusp
open import cohomology.Theory

module cohomology.SphereProduct {i} (CT : CohomologyTheory i)
  (n : ℤ) (m : ℕ) (X : Ptd i) where

  open CohomologyTheory CT
  open import cohomology.Wedge CT

  private
    space-eq : ⊙Susp (⊙Sphere m ⊙× X)
            ⊙≃ ⊙Sphere (S m) ⊙∨ (⊙Susp X ⊙∨ ⊙Susp^ (S m) X)
    space-eq =
      ⊙∨-emap (⊙ide (⊙Sphere (S m)))
        (⊙∨-emap (⊙ide (⊙Susp X))
          (⊙*-Sphere-l m X ⊙∘e SuspSmash.⊙eq (⊙Sphere m) X))
      ⊙∘e SuspProduct.⊙eq (⊙Sphere m) X

  C-Sphere× : C n (⊙Sphere m ⊙× X)
           ≃ᴳ C n (⊙Lift (⊙Sphere m)) ×ᴳ (C n X ×ᴳ C n (⊙Susp^ m X))
  C-Sphere× =
    C n (⊙Sphere m ⊙× X)
      ≃ᴳ⟨ C-Susp n (⊙Sphere m ⊙× X) ⁻¹ᴳ ⟩
    C (succ n) (⊙Susp (⊙Sphere m ⊙× X))
      ≃ᴳ⟨ C-emap (succ n) (space-eq ⊙⁻¹) ⟩
    C (succ n) (⊙Sphere (S m) ⊙∨ (⊙Susp X ⊙∨ ⊙Susp^ (S m) X))
      ≃ᴳ⟨ C-emap (succ n) (⊙∨-emap (⊙Susp-emap (⊙lower-equiv {X = ⊙Sphere m})) (⊙ide _)) ⟩
    C (succ n) (⊙Susp (⊙Lift {j = i} (⊙Sphere m)) ⊙∨ (⊙Susp X ⊙∨ ⊙Susp^ (S m) X))
      ≃ᴳ⟨ C-Wedge (succ n) (⊙Susp (⊙Lift (⊙Sphere m))) (⊙Susp X ⊙∨ ⊙Susp^ (S m) X) ⟩
    C (succ n) (⊙Susp (⊙Lift (⊙Sphere m))) ×ᴳ C (succ n) (⊙Susp X ⊙∨ ⊙Susp^ (S m) X)
      ≃ᴳ⟨ ×ᴳ-emap (C-Susp n (⊙Lift (⊙Sphere m)))
              ( ×ᴳ-emap (C-Susp n X) (C-Susp n (⊙Susp^ m X))
            ∘eᴳ C-Wedge (succ n) (⊙Susp X) (⊙Susp^ (S m) X)) ⟩
    C n (⊙Lift (⊙Sphere m)) ×ᴳ (C n X ×ᴳ C n (⊙Susp^ m X))
      ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Examples.Parity where
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Bool hiding (not)
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Product hiding (map)
open import Data.List hiding (and; or; sum; map; [_])
open import Data.Vec hiding (init)
import DTGP

data Word : Set where
  not and or : Word

pre : Word → ℕ → ℕ
pre not n = 1 + n
pre and n = 2 + n
pre or  n = 2 + n

post : Word → ℕ → ℕ
post not n = 1 + n
post and n = 1 + n
post or  n = 1 + n

even : ℕ → Bool
even zero = true
even (suc zero) = false
even (suc (suc zero)) = true
even (suc n) = even n

trues : ∀ {n} → Vec Bool n → ℕ
trues [] = 0
trues (true ∷ xs) = suc (trues xs)
trues (false ∷ xs) = trues xs

evenParity : ∀ {n} → Vec Bool n → Bool
evenParity xs = even (trues xs)

open DTGP pre post Data.Nat._≟_

eval : ∀ {inp out} → Term inp out → Vec Bool inp → Vec Bool out
eval [] is = is
eval (not ∷ xs) is with eval xs is
... | o ∷ os = Data.Bool.not o ∷ os
eval (and ∷ xs) is with eval xs is
... | o₂ ∷ o₁ ∷ os = (o₁ ∧ o₂) ∷ os
eval (or ∷ xs) is with eval xs is
... | o₂ ∷ o₁ ∷ os = (o₁ ∨ o₂) ∷ os

bitEqual : ∀ {m n} → Vec Bool m → Vec Bool n → Bool
bitEqual [] [] = true
bitEqual (_ ∷ _) [] = false
bitEqual [] (_ ∷ _) = false
bitEqual (x ∷ xs) (y ∷ ys) = x ∧ y ∧ bitEqual xs ys

scores : ∀ {inp out n} → Vec (Vec Bool inp) n → Term inp out → ℕ
scores ass xs = sum (map (λ as →
  if (bitEqual (eval xs as) [ evenParity as ])
  then 1 else 0)
  ass)

fitnessCases : Vec (Vec Bool _) _
fitnessCases =
    (true ∷ true ∷ [])
  ∷ (true ∷ false ∷ [])
  ∷ (false ∷ true ∷ [])
  ∷ (false ∷ false ∷ [])
  ∷ []

_==_ : ℕ → ℕ → Bool
zero == zero = true
zero == suc _ = false
suc _ == zero = false
suc m == suc n = m == n

score : Term _ _ → ℕ
score xs = scores fitnessCases xs

open Evolution score

match : (w : Word) (out : ℕ) → Dec (∃ λ n → out ≡ pre w n)
match not zero = no ¬p where
  ¬p : Σ ℕ (λ n → 0 ≡ suc n) → ⊥
  ¬p (_ , ())
match not (suc n) = yes (n , refl)
match and zero = no ¬p where
  ¬p : Σ ℕ (λ n → 0 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match and (suc zero) = no ¬p where
  ¬p : Σ ℕ (λ n → 1 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match and (suc (suc n)) = yes (n , refl)
match or zero = no ¬p where
  ¬p : Σ ℕ (λ n → 0 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match or (suc zero) = no ¬p where
  ¬p : Σ ℕ (λ n → 1 ≡ suc (suc n)) → ⊥
  ¬p (_ , ())
match or (suc (suc n)) = yes (n , refl)

open Initialization match

choices : List Word
choices = not ∷ and ∷ or ∷ []

population : Population _ _ _
population = fromList (init 4 2 1 choices)

answer : Population _ _ _
answer = evolve 1337 1 population

max_stars_repo_name: larrytheliquid/dtgp

max_issues_repo_name: larrytheliquid/dtgp

max_forks_repo_name: larrytheliquid/dtgp


text:
-- Andreas, 2017-02-20, issue #2467
-- Proper error on missing BUILTIN REWRITE

{-# OPTIONS --rewriting #-}

postulate A : Set

{-# REWRITE A #-}

-- Should fail with error like


text:
-- Andreas, 2019-05-29, issue #3818, reported by Matthew Daggitt

-- An external module name, i.e., the object of `import`,
-- should not be considered clashing with an internal module name.

module _ where

module Issue3818 where
  module M where         -- Internal module Issue3818.M.

open import Issue3818.M  -- Name unambiguous, since referring to file.

-- Should succeed instead of complaining about ambiguous Issue3818.M.