text:
open import Nat
open import Prelude
open import dynamics-core
open import disjointness

module elaboration-generality where
  mutual
    elaboration-generality-synth : {Γ : tctx} {e : hexp} {τ : htyp} {d : ihexp} {Δ : hctx} →
                                   Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                                   Γ ⊢ e => τ
    elaboration-generality-synth ESNum = SNum
    elaboration-generality-synth (ESPlus dis apt x₁ x₂) =
      SPlus (elaboration-generality-ana x₁) (elaboration-generality-ana x₂)
    elaboration-generality-synth (ESAsc x) = SAsc (elaboration-generality-ana x)
    elaboration-generality-synth (ESVar x₁) = SVar x₁
    elaboration-generality-synth (ESLam apt ex) with elaboration-generality-synth ex
    ... | ih = SLam apt ih
    elaboration-generality-synth (ESAp dis _ a x₁ x₂ x₃) =
      SAp a x₁ (elaboration-generality-ana x₃)
    elaboration-generality-synth (ESPair x x₁ x₂ x₃) =
      SPair (elaboration-generality-synth x₂) (elaboration-generality-synth x₃)
    elaboration-generality-synth ESEHole = SEHole
    elaboration-generality-synth (ESNEHole dis ex) = SNEHole (elaboration-generality-synth ex)
    elaboration-generality-synth (ESFst wt x₁ x₂) = SFst wt x₁
    elaboration-generality-synth (ESSnd wt x₁ x₂) = SSnd wt x₁

    elaboration-generality-ana : {Γ : tctx} {e : hexp} {τ τ' : htyp} {d : ihexp} {Δ : hctx} →
                                 Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                                 Γ ⊢ e <= τ
    elaboration-generality-ana (EALam apt m ex) = ALam apt m (elaboration-generality-ana ex)
    elaboration-generality-ana (EASubsume x x₁ x₂ x₃) =
      ASubsume (elaboration-generality-synth x₂) x₃
    elaboration-generality-ana EAEHole = ASubsume SEHole TCHole1
    elaboration-generality-ana (EANEHole dis x) =
      ASubsume (SNEHole (elaboration-generality-synth x)) TCHole1
    elaboration-generality-ana (EAInl x x₁) = AInl x (elaboration-generality-ana x₁)
    elaboration-generality-ana (EAInr x x₁) = AInr x (elaboration-generality-ana x₁)
    elaboration-generality-ana (EACase x x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ x₉ x₁₀ x₁₁) =
      ACase x₆ x₇ x₉ (elaboration-generality-synth x₈)
                     (elaboration-generality-ana x₁₀)
                     (elaboration-generality-ana x₁₁)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
postulate A : Set

record R : Set where
  field f : A

record S : Set where
  field g : A

test : R → A
test record{g = a} = a

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Primitive using (lsuc; _⊔_)
open import Data.Fin using (Fin)

open import MultiSorted.AlgebraicTheory

module MultiSorted.Substitution {ℓ} {𝓈 ℴ} {Σ : Signature {𝓈} {ℴ}} (T : Theory ℓ Σ) where

  open Theory T

  -- an equality is preserved by the action of the identity
  eq-id-action : ∀ {Γ : Context} {A} {u v : Term Γ A} → (⊢ Γ ∥ (u [ id-s ]s) ≈ (v [ id-s ]s) ⦂ A) → (⊢ Γ ∥ u ≈ v ⦂ A)
  eq-id-action {u = u} {v = v} p = eq-tran (id-action {a = u}) (eq-tran p (eq-symm (id-action {a = v})))

  -- equality of substitutions
  _≈s_ : ∀ {Γ Δ : Context} → Γ ⇒s Δ → Γ ⇒s Δ → Set (lsuc (ℓ ⊔ 𝓈 ⊔ ℴ))
  _≈s_ {Γ} {Δ} σ ρ = ∀ x → ⊢ Γ ∥ σ x ≈ ρ x ⦂ sort-of Δ x

  infix 5 _≈s_

  -- reflexivity of the equality of substitutions
  refl-subst : ∀ {γ δ : Context} {f : γ ⇒s δ} → f ≈s f
  refl-subst = λ x → eq-refl

  -- symmetry of the equality of substitutions
  symm-subst : ∀ {Γ Δ : Context} {f g : Γ ⇒s Δ} → f ≈s g → g ≈s f
  symm-subst {Γ} {Δ} {f} {g} p = λ x → eq-symm (p x)

  -- transitivity of the equality of substitutions
  trans-subst : ∀ {Γ Δ : Context} {f g h : Γ ⇒s Δ} → f ≈s g → g ≈s h → f ≈s h
  trans-subst {Γ} {Δ} {f} {g} {h} p q = λ x → eq-tran (p x) (q x)

  -- neutrality of tm-var
  tm-var-id : ∀ {Γ} {A} {t : Term Γ A} → ⊢ Γ ∥ t [ id-s ]s ≈ t ⦂ A
  tm-var-id {t = tm-var x} = eq-refl
  tm-var-id {t = tm-oper f ts} = eq-congr (λ i → tm-var-id)

  -- any two substitutions into the empty context are equal
  empty-ctx-subst-unique : ∀ {Γ : Context} {σ ρ : Γ ⇒s ctx-empty} → σ ≈s ρ
  empty-ctx-subst-unique ()

  -- composition of substitutions is functorial
  subst-∘s : ∀ {Γ Δ Θ} {ρ : Δ ⇒s Γ} {σ : Θ ⇒s Δ} {A} (t : Term Γ A) →
           ⊢ Θ ∥ (t [ ρ ]s) [ σ ]s ≈ t [ ρ ∘s σ ]s ⦂ A
  subst-∘s (tm-var x) = eq-refl
  subst-∘s (tm-oper f ts) = eq-congr (λ i → subst-∘s (ts i))

  -- substitution preserves equality
  eq-subst : ∀ {Γ Δ : Context} {σ : Γ ⇒s Δ} {A} {u v : Term Δ A} →
             ⊢ Δ ∥ u ≈ v ⦂ A → ⊢ Γ ∥ u [ σ ]s ≈ v [ σ ]s ⦂ A
  eq-subst eq-refl = eq-refl
  eq-subst (eq-symm ξ) = eq-symm (eq-subst ξ)
  eq-subst (eq-tran ζ ξ) = eq-tran (eq-subst ζ) (eq-subst ξ)
  eq-subst (eq-congr ξ) = eq-congr (λ i → eq-subst (ξ i))
  eq-subst {σ = σ} (eq-axiom ε ρ) = eq-tran (subst-∘s (ax-lhs ε)) (eq-tran (eq-axiom ε (ρ ∘s σ)) (eq-symm (subst-∘s (ax-rhs ε))))

 -- equivalent substitutions act the same on terms
  equiv-subst : ∀ {Γ Δ : Context} {σ τ : Γ ⇒s Δ} {A} (u : Term Δ A) →
                σ ≈s τ → ⊢ Γ ∥ u [ σ ]s ≈ u [ τ ]s ⦂ A
  equiv-subst (tm-var x) ξ = ξ x
  equiv-subst (tm-oper f ts) ξ = eq-congr (λ i → equiv-subst (ts i) ξ)

 -- equivalent substitution preserve equality
  equiv-eq-subst : ∀ {Γ Δ : Context} {σ τ : Γ ⇒s Δ} {A} {u v : Term Δ A} →
                   σ ≈s τ → ⊢ Δ ∥ u ≈ v ⦂ A → ⊢ Γ ∥ u [ σ ]s ≈ v [ τ ]s ⦂ A
  equiv-eq-subst {u = u} p eq-refl = equiv-subst u p
  equiv-eq-subst p (eq-symm q) = eq-symm  (equiv-eq-subst (symm-subst p) q)
  equiv-eq-subst p (eq-tran q r) = eq-tran (eq-subst q) (equiv-eq-subst p r)
  equiv-eq-subst p (eq-congr ξ) = eq-congr λ i → equiv-eq-subst p (ξ i)
  equiv-eq-subst {σ = σ} {τ = τ} p (eq-axiom ε θ) = eq-tran (eq-subst (eq-axiom ε θ)) (equiv-subst (ax-rhs ε [ θ ]s) p)

  -- the pairing of two substitutions
  ⟨_,_⟩s : ∀ {Γ Δ Θ} (σ : Γ ⇒s Δ) (ρ : Γ ⇒s Θ) → Γ ⇒s ctx-concat Δ Θ
  ⟨ σ , ρ ⟩s (var-inl x) = σ x
  ⟨ σ , ρ ⟩s (var-inr y) = ρ y

  -- composition of substitutions preserves equality
  ∘s-resp-≈s : ∀ {Γ Δ Θ} {σ₁ σ₂ : Γ ⇒s Δ} {τ₁ τ₂ : Δ ⇒s Θ} →
               τ₁ ≈s τ₂ → σ₁ ≈s σ₂ → τ₁ ∘s σ₁ ≈s τ₂ ∘s σ₂
  ∘s-resp-≈s ξ ζ z = equiv-eq-subst ζ (ξ z)

  -- the action of a substitution on an equation
  open Equation
  _[_]s-eq : ∀ (ε : Equation Σ) {Γ : Context} ( σ : Γ ⇒s (eq-ctx ε)) → Equation Σ
  _[_]s-eq ε {Γ} σ = Γ ∥ ((eq-lhs ε) [ σ ]s) ≈ ((eq-rhs ε) [ σ ]s) ⦂ (eq-sort ε)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

------------------------------------------------------------------------
-- Lists, based on the Kleene star and plus.
--
-- These lists are exatcly equivalent to normal lists, except the "cons"
-- case is split into its own data type. This lets us write all the same
-- functions as before, but it has 2 advantages:
--
-- * Some functions are easier to express on the non-empty type. For
--   instance, head can be clearly expressed without the need for
--   maybes.
-- * It can make some proofs easier. By using the non-empty type where
--   possible, we can avoid an extra pattern match, which can really
--   simplify certain proofs.

module Data.List.Kleene.Base where

open import Data.Product as Product using (_×_; _,_; map₂; map₁; proj₁; proj₂)
open import Data.Nat     as ℕ       using (ℕ; suc; zero)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing)
open import Data.Sum     as Sum     using (_⊎_; inj₁; inj₂)
open import Algebra

open import Function

------------------------------------------------------------------------
-- Definitions

infixr 5 _&_ ∹_
mutual
  -- Non-Empty Lists
  record _⁺ {a} (A : Set a) : Set a where
    inductive
    constructor _&_
    field
      head : A
      tail : A ⋆

  -- Possibly Empty Lists
  data _⋆ {a} (A : Set a) : Set a where
    [] : A ⋆
    ∹_ : A ⁺ → A ⋆
open _⁺ public

------------------------------------------------------------------------
-- FoldMap

module _ {c ℓ a} (sgrp : Semigroup c ℓ) {A : Set a} where
  open Semigroup sgrp

  foldMap⁺ : (A → Carrier) → A ⁺ → Carrier
  foldMap⁺ f (x & []) = f x
  foldMap⁺ f (x & ∹ xs) = f x ∙ foldMap⁺ f xs

module _ {c ℓ a} (mon : Monoid c ℓ) {A : Set a} where
  open Monoid mon

  foldMap⋆ : (A → Carrier) → A ⋆ → Carrier
  foldMap⋆ f [] = ε
  foldMap⋆ f (∹ xs) = foldMap⁺ semigroup f xs

------------------------------------------------------------------------
-- Folds

module _ {a b} {A : Set a} {B : Set b} (f : A → B → B) (b : B) where
  foldr⁺ : A ⁺ → B
  foldr⋆ : A ⋆ → B

  foldr⁺ (x & xs) = f x (foldr⋆ xs)

  foldr⋆ [] = b
  foldr⋆ (∹ xs) = foldr⁺ xs

module _ {a b} {A : Set a} {B : Set b} (f : B → A → B) where
  foldl⁺ : B → A ⁺ → B
  foldl⋆ : B → A ⋆ → B

  foldl⁺ b (x & xs) = foldl⋆ (f b x) xs

  foldl⋆ b [] = b
  foldl⋆ b (∹ xs) = foldl⁺ b xs

------------------------------------------------------------------------
-- Concatenation

module _ {a} {A : Set a} where
  _⁺++⁺_ : A ⁺ → A ⁺ → A ⁺
  _⁺++⋆_ : A ⁺ → A ⋆ → A ⁺
  _⋆++⁺_ : A ⋆ → A ⁺ → A ⁺
  _⋆++⋆_ : A ⋆ → A ⋆ → A ⋆

  head (xs ⁺++⋆ ys) = head xs
  tail (xs ⁺++⋆ ys) = tail xs ⋆++⋆ ys

  xs ⋆++⋆ ys = foldr⋆ (λ x zs → ∹ x & zs) ys xs

  xs ⁺++⁺ ys = foldr⁺ (λ x zs → x & ∹ zs) ys xs

  []     ⋆++⁺ ys = ys
  (∹ xs) ⋆++⁺ ys = xs ⁺++⁺ ys

------------------------------------------------------------------------
-- Mapping

module _ {a b} {A : Set a} {B : Set b} (f : A → B) where
  map⁺ : A ⁺ → B ⁺
  map⋆ : A ⋆ → B ⋆

  head (map⁺ xs) = f (head xs)
  tail (map⁺ xs) = map⋆ (tail xs)

  map⋆ [] = []
  map⋆ (∹ xs) = ∹ map⁺ xs

------------------------------------------------------------------------
-- Applicative Operations

module _ {a} {A : Set a} where
  pure⁺ : A → A ⁺
  pure⋆ : A → A ⋆

  head (pure⁺ x) = x
  tail (pure⁺ x) = []

  pure⋆ x = ∹ pure⁺ x

module _ {a b} {A : Set a} {B : Set b} where
  _⋆<*>⋆_ : (A → B) ⋆ → A ⋆ → B ⋆
  _⁺<*>⋆_ : (A → B) ⁺ → A ⋆ → B ⋆
  _⋆<*>⁺_ : (A → B) ⋆ → A ⁺ → B ⋆
  _⁺<*>⁺_ : (A → B) ⁺ → A ⁺ → B ⁺

  []     ⋆<*>⋆ xs = []
  (∹ fs) ⋆<*>⋆ xs = fs ⁺<*>⋆ xs

  fs ⁺<*>⋆ xs = map⋆ (head fs) xs ⋆++⋆ (tail fs ⋆<*>⋆ xs)

  []     ⋆<*>⁺ xs = []
  (∹ fs) ⋆<*>⁺ xs = ∹ fs ⁺<*>⁺ xs

  fs ⁺<*>⁺ xs = map⁺ (head fs) xs ⁺++⋆ (tail fs ⋆<*>⁺ xs)

------------------------------------------------------------------------
-- Monadic Operations

module _ {a b} {A : Set a} {B : Set b} where
  _⁺>>=⁺_ : A ⁺ → (A → B ⁺) → B ⁺
  _⁺>>=⋆_ : A ⁺ → (A → B ⋆) → B ⋆
  _⋆>>=⁺_ : A ⋆ → (A → B ⁺) → B ⋆
  _⋆>>=⋆_ : A ⋆ → (A → B ⋆) → B ⋆

  (x & xs) ⁺>>=⁺ k = k x ⁺++⋆ (xs ⋆>>=⁺ k)

  (x & xs) ⁺>>=⋆ k = k x ⋆++⋆ (xs ⋆>>=⋆ k)

  []     ⋆>>=⋆ k = []
  (∹ xs) ⋆>>=⋆ k = xs ⁺>>=⋆ k

  []     ⋆>>=⁺ k = []
  (∹ xs) ⋆>>=⁺ k = ∹ xs ⁺>>=⁺ k

------------------------------------------------------------------------
-- Scans

module Scanr {a b} {A : Set a} {B : Set b} (f : A → B → B) (b : B) where
  cons : A → B ⁺ → B ⁺
  head (cons x xs) = f x (head xs)
  tail (cons x xs) = ∹ xs

  scanr⁺ : A ⁺ → B ⁺
  scanr⋆ : A ⋆ → B ⁺

  scanr⋆ = foldr⋆ cons (b & [])
  scanr⁺ = foldr⁺ cons (b & [])
open Scanr public using (scanr⁺; scanr⋆)

module _ {a b} {A : Set a} {B : Set b} (f : B → A → B) where
  scanl⁺ : B → A ⁺ → B ⁺
  scanl⋆ : B → A ⋆ → B ⁺

  head (scanl⁺ b xs) = b
  tail (scanl⁺ b xs) = ∹ scanl⋆ (f b (head xs)) (tail xs)

  head (scanl⋆ b xs) = b
  tail (scanl⋆ b []) = []
  tail (scanl⋆ b (∹ xs)) = ∹ scanl⋆ (f b (head xs)) (tail xs)

  scanl₁ : B → A ⁺ → B ⁺
  scanl₁ b xs = scanl⋆ (f b (head xs)) (tail xs)

------------------------------------------------------------------------
-- Accumulating maps

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} (f : B → A → (B × C)) where
  mapAccumL⋆ : B → A ⋆ → (B × C ⋆)
  mapAccumL⁺ : B → A ⁺ → (B × C ⁺)

  mapAccumL⋆ b [] = b , []
  mapAccumL⋆ b (∹ xs) = map₂ ∹_ (mapAccumL⁺ b xs)

  mapAccumL⁺ b (x & xs) =
    let y , ys = f b x
        z , zs = mapAccumL⋆ y xs
    in z , (ys & zs)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} (f : A → B → (C × B)) (b : B) where
  mapAccumR⋆ : A ⋆ → (C ⋆ × B)
  mapAccumR⁺ : A ⁺ → (C ⁺ × B)

  mapAccumR⋆ [] = [] , b
  mapAccumR⋆ (∹ xs) = map₁ ∹_ (mapAccumR⁺ xs)

  mapAccumR⁺ (x & xs) =
    let ys , y = mapAccumR⋆ xs
        zs , z = f x y
    in (zs & ys) , z

------------------------------------------------------------------------
-- Non-Empty Folds

module _ {a} {A : Set a} where
  last : A ⁺ → A
  last (x & []) = x
  last (_ & (∹ xs)) = last xs

module _ {a} {A : Set a} (f : A → A → A) where
  foldr1 : A ⁺ → A
  foldr1 (x & []) = x
  foldr1 (x & (∹ xs)) = f x (foldr1 xs)

  foldl1 : A ⁺ → A
  foldl1 (x & xs) = foldl⋆ f x xs

module _ {a b} {A : Set a} {B : Set b} (f : A → Maybe B → B) where
  foldrMay⋆ : A ⋆ → Maybe B
  foldrMay⁺ : A ⁺ → B

  foldrMay⋆ [] = nothing
  foldrMay⋆ (∹ xs) = just (foldrMay⁺ xs)

  foldrMay⁺ xs = f (head xs) (foldrMay⋆ (tail xs))

------------------------------------------------------------------------
-- Indexing

module _ {a} {A : Set a} where
  _[_]⋆ : A ⋆ → ℕ → Maybe A
  _[_]⁺ : A ⁺ → ℕ → Maybe A

  []     [ _ ]⋆ = nothing
  (∹ xs) [ i ]⋆ = xs [ i ]⁺

  xs [ zero  ]⁺ = just (head xs)
  xs [ suc i ]⁺ = tail xs [ i ]⋆

  applyUpTo⋆ : (ℕ → A) → ℕ → A ⋆
  applyUpTo⁺ : (ℕ → A) → ℕ → A ⁺

  applyUpTo⋆ f zero    = []
  applyUpTo⋆ f (suc n) = ∹ applyUpTo⁺ f n

  head (applyUpTo⁺ f n) = f zero
  tail (applyUpTo⁺ f n) = applyUpTo⋆ (f ∘ suc) n

upTo⋆ : ℕ → ℕ ⋆
upTo⋆ = applyUpTo⋆ id

upTo⁺ : ℕ → ℕ ⁺
upTo⁺ = applyUpTo⁺ id

------------------------------------------------------------------------
-- Manipulation

module _ {a} {A : Set a} (x : A) where
  intersperse⁺ : A ⁺ → A ⁺
  intersperse⋆ : A ⋆ → A ⋆

  head (intersperse⁺ xs) = head xs
  tail (intersperse⁺ xs) = prepend (tail xs)
    where
    prepend : A ⋆ → A ⋆
    prepend [] = []
    prepend (∹ xs) = ∹ x & ∹ intersperse⁺ xs

  intersperse⋆ [] = []
  intersperse⋆ (∹ xs) = ∹ intersperse⁺ xs

module _ {a} {A : Set a} where
  _⁺<|>⁺_ : A ⁺ → A ⁺ → A ⁺
  _⁺<|>⋆_ : A ⁺ → A ⋆ → A ⁺
  _⋆<|>⁺_ : A ⋆ → A ⁺ → A ⁺
  _⋆<|>⋆_ : A ⋆ → A ⋆ → A ⋆

  head (xs ⁺<|>⁺ ys) = head xs
  tail (xs ⁺<|>⁺ ys) = ∹ (ys ⁺<|>⋆ tail xs)

  head (xs ⁺<|>⋆ ys) = head xs
  tail (xs ⁺<|>⋆ ys) = ys ⋆<|>⋆ tail xs

  []     ⋆<|>⁺ ys = ys
  (∹ xs) ⋆<|>⁺ ys = xs ⁺<|>⁺ ys

  []     ⋆<|>⋆ ys = ys
  (∹ xs) ⋆<|>⋆ ys = ∹ (xs ⁺<|>⋆ ys)

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) where
  ⁺zipWith⁺ : A ⁺ → B ⁺ → C ⁺
  ⋆zipWith⁺ : A ⋆ → B ⁺ → C ⋆
  ⁺zipWith⋆ : A ⁺ → B ⋆ → C ⋆
  ⋆zipWith⋆ : A ⋆ → B ⋆ → C ⋆

  head (⁺zipWith⁺ xs ys) = f (head xs) (head ys)
  tail (⁺zipWith⁺ xs ys) = ⋆zipWith⋆ (tail xs) (tail ys)

  ⋆zipWith⁺ [] ys = []
  ⋆zipWith⁺ (∹ xs) ys = ∹ ⁺zipWith⁺ xs ys

  ⁺zipWith⋆ xs [] = []
  ⁺zipWith⋆ xs (∹ ys) = ∹ ⁺zipWith⁺ xs ys

  ⋆zipWith⋆ [] ys = []
  ⋆zipWith⋆ (∹ xs) ys = ⁺zipWith⋆ xs ys

module Unzip {a b c} {A : Set a} {B : Set b} {C : Set c} (f : A → B × C) where
  cons : B × C → B ⋆ × C ⋆ → B ⁺ × C ⁺
  head (proj₁ (cons x xs)) = proj₁ x
  tail (proj₁ (cons x xs)) = proj₁ xs
  head (proj₂ (cons x xs)) = proj₂ x
  tail (proj₂ (cons x xs)) = proj₂ xs

  unzipWith⋆ : A ⋆ → B ⋆ × C ⋆
  unzipWith⁺ : A ⁺ → B ⁺ × C ⁺

  unzipWith⋆ = foldr⋆ (λ x xs → Product.map ∹_ ∹_ (cons (f x) xs)) ([] , [])

  unzipWith⁺ xs = cons (f (head xs)) (unzipWith⋆ (tail xs))
open Unzip using (unzipWith⁺; unzipWith⋆) public

module Partition {a b c} {A : Set a} {B : Set b} {C : Set c} (f : A → B ⊎ C) where
  cons : B ⊎ C → B ⋆ × C ⋆ → B ⋆ × C ⋆
  proj₁ (cons (inj₁ x) xs) = ∹ x & proj₁ xs
  proj₂ (cons (inj₁ x) xs) = proj₂ xs
  proj₂ (cons (inj₂ x) xs) = ∹ x & proj₂ xs
  proj₁ (cons (inj₂ x) xs) = proj₁ xs

  partitionSumsWith⋆ : A ⋆ → B ⋆ × C ⋆
  partitionSumsWith⁺ : A ⁺ → B ⋆ × C ⋆

  partitionSumsWith⋆ = foldr⋆ (cons ∘ f) ([] , [])

  partitionSumsWith⁺ = foldr⁺ (cons ∘ f) ([] , [])
open Partition using (partitionSumsWith⁺; partitionSumsWith⋆) public

module _ {a} {A : Set a} where
  ⋆transpose⋆ : (A ⋆) ⋆ → (A ⋆) ⋆
  ⋆transpose⁺ : (A ⋆) ⁺ → (A ⁺) ⋆
  ⁺transpose⋆ : (A ⁺) ⋆ → (A ⋆) ⁺
  ⁺transpose⁺ : (A ⁺) ⁺ → (A ⁺) ⁺

  ⋆transpose⋆ [] = []
  ⋆transpose⋆ (∹ xs) = map⋆ ∹_ (⋆transpose⁺ xs)

  ⋆transpose⁺ (x & []) = map⋆ pure⁺ x
  ⋆transpose⁺ (x & (∹ xs)) = ⋆zipWith⋆ (λ y z → y & ∹ z) x (⋆transpose⁺ xs)

  ⁺transpose⋆ [] = [] & []
  ⁺transpose⋆ (∹ xs) = map⁺ ∹_ (⁺transpose⁺ xs)

  ⁺transpose⁺ (x & []) = map⁺ pure⁺ x
  ⁺transpose⁺ (x & (∹ xs)) = ⁺zipWith⁺ (λ y z → y & ∹ z) x (⁺transpose⁺ xs)

module _ {a} {A : Set a} where
  tails⋆ : A ⋆ → (A ⁺) ⋆
  tails⁺ : A ⁺ → (A ⁺) ⁺

  head (tails⁺ xs) = xs
  tail (tails⁺ xs) = tails⋆ (tail xs)

  tails⋆ [] = []
  tails⋆ (∹ xs) = ∹ tails⁺ xs

module _ {a} {A : Set a} where
  reverse⋆ : A ⋆ → A ⋆
  reverse⋆ = foldl⋆ (λ xs x → ∹ x & xs) []

  reverse⁺ : A ⁺ → A ⁺
  reverse⁺ (x & xs) = foldl⋆ (λ ys y → y & (∹ ys)) (x & []) xs

max_stars_repo_name: oisdk/agda-kleene-lists

max_issues_repo_name: oisdk/agda-kleene-lists

max_forks_repo_name: oisdk/agda-kleene-lists


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Unary.Raw where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude using (isProp)

open import Cubical.Data.Empty hiding (rec)
open import Cubical.Data.Unit.Base using (⊤)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum.Base using (_⊎_; rec)
open import Cubical.Foundations.Function

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.Decidable using (IsYes)

open import Cubical.Relation.Unary using (RawPred)

private
  variable
    a b c ℓ ℓ₁ ℓ₂ : Level
    A : Type a
    B : Type b
    C : Type c

------------------------------------------------------------------------
-- Special sets

-- The empty set.

∅ : RawPred A _
∅ = λ _ → ⊥

-- The singleton set.

｛_｝ : A → RawPred A _
｛ x ｝ = _≡ x

-- The universal set.

U : RawPred A _
U = λ _ → ⊤

------------------------------------------------------------------------
-- Membership

infix 6 _∈_ _∉_

_∈_ : A → RawPred A ℓ → Type _
x ∈ P = P x

_∉_ : A → RawPred A ℓ → Type _
x ∉ P = ¬ x ∈ P

------------------------------------------------------------------------
-- Subset relations

infix 6 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_

_⊆_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q

_⊇_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊇ Q = Q ⊆ P

_⊈_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊈ Q = ¬ (P ⊆ Q)

_⊉_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊉ Q = ¬ (P ⊇ Q)

_⊂_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊂ Q = P ⊆ Q × Q ⊈ P

_⊃_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊃ Q = Q ⊂ P

_⊄_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊄ Q = ¬ (P ⊂ Q)

_⊅_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⊅ Q = ¬ (P ⊃ Q)

------------------------------------------------------------------------
-- Properties of sets

infix 10 Satisfiable Universal IUniversal

-- Emptiness - no element satisfies P.

Empty : RawPred A ℓ → Type _
Empty P = ∀ x → x ∉ P

-- Satisfiable - at least one element satisfies P.

Satisfiable : RawPred A ℓ → Type _
Satisfiable {A = A} P = ∃[ x ∈ A ] x ∈ P

syntax Satisfiable P = ∃⟨ P ⟩

-- Universality - all elements satisfy P.

Universal : RawPred A ℓ → Type _
Universal P = ∀ x → x ∈ P

syntax Universal P = Π[ P ]

-- Implicit universality - all elements satisfy P.

IUniversal : RawPred A ℓ → Type _
IUniversal P = ∀ {x} → x ∈ P

syntax IUniversal P = ∀[ P ]

-- Decidability - it is possible to determine if an arbitrary element
-- satisfies P.

Decidable : RawPred A ℓ → Type _
Decidable P = ∀ x → Dec (P x)

-- Disjointness - Any element satisfying both P and Q is contradictory.

_⊃⊂_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
_⊃⊂_ P Q = ∀ {x} → x ∈ P → x ∈ Q → ⊥

-- Positive version of non-disjointness, dual to inclusion.

_≬_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
_≬_ {A = A} P Q = ∃[ x ∈ A ] x ∈ P × x ∈ Q

------------------------------------------------------------------------
-- Operations on sets

infix 10 ⋃ ⋂
infixr 9 _⊢_
infixr 8 _⇒_
infixr 7 _∩_
infixr 6 _∪_
infix 5 _≬_

-- Complement.

∁ : RawPred A ℓ → RawPred A ℓ
∁ P = λ x → x ∉ P

-- Implication.

_⇒_ : RawPred A ℓ₁ → RawPred A ℓ₂ → RawPred A _
P ⇒ Q = λ x → x ∈ P → x ∈ Q

-- Union.

_∪_ : RawPred A ℓ₁ → RawPred A ℓ₂ → RawPred A _
P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

-- Intersection.

_∩_ : RawPred A ℓ₁ → RawPred A ℓ₂ → RawPred A _
P ∩ Q = λ x → x ∈ P × x ∈ Q

-- Infinitary union.

⋃ : ∀ {i} (I : Type i) → (I → RawPred A ℓ) → RawPred A _
⋃ I P = λ x → Σ[ i ∈ I ] P i x

syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

-- Infinitary intersection.

⋂ : ∀ {i} (I : Type i) → (I → RawPred A ℓ) → RawPred A _
⋂ I P = λ x → (i : I) → P i x

syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

-- Preimage.

_⊢_ : (A → B) → RawPred B ℓ → RawPred A ℓ
f ⊢ P = λ x → P (f x)

------------------------------------------------------------------------
-- Preservation under operations

_Preserves_⟶_ : (A → B) → RawPred A ℓ₁ → RawPred B ℓ₂ → Type _
f Preserves P ⟶ Q = P ⊆ f ⊢ Q

_Preserves_ : (A → A) → RawPred A ℓ → Type _
f Preserves P = f Preserves P ⟶ P

-- A binary variant of _Preserves_⟶_.

_Preserves₂_⟶_⟶_ : (A → B → C) → RawPred A ℓ₁ → RawPred B ℓ₂ → RawPred C ℓ → Type _
_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y} → x ∈ P → y ∈ Q → x ∙ y ∈ R

_Preserves₂_ : (A → A → A) → RawPred A ℓ → Type _
_∙_ Preserves₂ P = _∙_ Preserves₂ P ⟶ P ⟶ P

------------------------------------------------------------------------
-- Logical equivalence

_⇔_ : RawPred A ℓ₁ → RawPred A ℓ₂ → Type _
P ⇔ Q = Π[ P ⇒ Q ∩ Q ⇒ P ]

------------------------------------------------------------------------
-- Predicate combinators

-- These differ from the set operations above, as the carrier set of the
-- resulting predicates are not the same as the carrier set of the
-- component predicates.

infixr  2 _⟨×⟩_
infixr  2 _⟨⊙⟩_
infixr  1 _⟨⊎⟩_
infixr  0 _⟨→⟩_
infixl  9 _⟨·⟩_
infix  10 _~
infixr  9 _⟨∘⟩_
infixr  2 _//_ _\\_

-- Product.

_⟨×⟩_ : RawPred A ℓ₁ → RawPred B ℓ₂ → RawPred (A × B) _
(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q

-- Sum over one element.

_⟨⊎⟩_ : RawPred A ℓ → RawPred B ℓ → RawPred (A ⊎ B) _
P ⟨⊎⟩ Q = rec P Q

-- Sum over two elements.

_⟨⊙⟩_ : RawPred A ℓ₁ → RawPred B ℓ₂ → RawPred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q

-- Implication.

_⟨→⟩_ : RawPred A ℓ₁ → RawPred B ℓ₂ → RawPred (A → B) _
(P ⟨→⟩ Q) f = f Preserves P ⟶ Q

-- Product.

_⟨·⟩_ : (P : RawPred A ℓ₁) (Q : RawPred B ℓ₂) →
        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
(P ⟨·⟩ Q) (p , f) = f p

-- Converse.

_~ : RawPred (A × B) ℓ → RawPred (B × A) ℓ
P ~ = P ∘ λ { (x , y) → y , x }

-- Composition.

_⟨∘⟩_ : RawPred (A × B) ℓ₁ → RawPred (B × C) ℓ₂ → RawPred (A × C) _
_⟨∘⟩_ {B = B} P Q (x , z) = ∃[ y ∈ B ] (x , y) ∈ P × (y , z) ∈ Q

-- Post-division.

_//_ : RawPred (A × C) ℓ₁ → RawPred (B × C) ℓ₂ → RawPred (A × B) _
(P // Q) (x , y) = Q ∘ (y ,_) ⊆ P ∘ (x ,_)

-- Pre-division.

_\\_ : RawPred (A × C) ℓ₁ → RawPred (A × B) ℓ₂ → RawPred (B × C) _
P \\ Q = (P ~ // Q ~) ~


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
------------------------------------------------------------------------

module Algebra where

open import Relation.Binary
open import Algebra.FunctionProperties
open import Algebra.Structures
open import Function
open import Level

------------------------------------------------------------------------
-- Semigroups, (commutative) monoids and (abelian) groups

record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier     : Set c
    _≈_         : Rel Carrier ℓ
    _∙_         : Op₂ Carrier
    isSemigroup : IsSemigroup _≈_ _∙_

  open IsSemigroup isSemigroup public

  setoid : Setoid _ _
  setoid = record { isEquivalence = isEquivalence }

-- A raw monoid is a monoid without any laws.

record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier

record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier  : Set c
    _≈_      : Rel Carrier ℓ
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid _≈_ _∙_ ε

  open IsMonoid isMonoid public

  semigroup : Semigroup _ _
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (setoid)

  rawMonoid : RawMonoid _ _
  rawMonoid = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    ; ε   = ε
    }

record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier             : Set c
    _≈_                 : Rel Carrier ℓ
    _∙_                 : Op₂ Carrier
    ε                   : Carrier
    isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε

  open IsCommutativeMonoid isCommutativeMonoid public

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (setoid; semigroup; rawMonoid)

record Group c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isGroup : IsGroup _≈_ _∙_ ε _⁻¹

  open IsGroup isGroup public

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (setoid; semigroup; rawMonoid)

record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ
    _∙_            : Op₂ Carrier
    ε              : Carrier
    _⁻¹            : Op₁ Carrier
    isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹

  open IsAbelianGroup isAbelianGroup public

  group : Group _ _
  group = record { isGroup = isGroup }

  open Group group public using (setoid; semigroup; monoid; rawMonoid)

  commutativeMonoid : CommutativeMonoid _ _
  commutativeMonoid =
    record { isCommutativeMonoid = isCommutativeMonoid }

------------------------------------------------------------------------
-- Various kinds of semirings

record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0#

  open IsNearSemiring isNearSemiring public

  +-monoid : Monoid _ _
  +-monoid = record { isMonoid = +-isMonoid }

  open Monoid +-monoid public
         using (setoid)
         renaming ( semigroup to +-semigroup
                  ; rawMonoid to +-rawMonoid)

  *-semigroup : Semigroup _ _
  *-semigroup = record { isSemigroup = *-isSemigroup }

record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier              : Set c
    _≈_                  : Rel Carrier ℓ
    _+_                  : Op₂ Carrier
    _*_                  : Op₂ Carrier
    0#                   : Carrier
    isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0#

  open IsSemiringWithoutOne isSemiringWithoutOne public

  nearSemiring : NearSemiring _ _
  nearSemiring = record { isNearSemiring = isNearSemiring }

  open NearSemiring nearSemiring public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid
               ; *-semigroup
               )

  +-commutativeMonoid : CommutativeMonoid _ _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                           : Set c
    _≈_                               : Rel Carrier ℓ
    _+_                               : Op₂ Carrier
    _*_                               : Op₂ Carrier
    0#                                : Carrier
    1#                                : Carrier
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  +-commutativeMonoid : CommutativeMonoid _ _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
         using (setoid)
         renaming ( semigroup to +-semigroup
                  ; rawMonoid to +-rawMonoid
                  ; monoid    to +-monoid
                  )

  *-monoid : Monoid _ _
  *-monoid = record { isMonoid = *-isMonoid }

  open Monoid *-monoid public
         using ()
         renaming ( semigroup to *-semigroup
                  ; rawMonoid to *-rawMonoid
                  )

record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#

  open IsSemiring isSemiring public

  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
  semiringWithoutAnnihilatingZero = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    }

  open SemiringWithoutAnnihilatingZero
         semiringWithoutAnnihilatingZero public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid
               ; +-commutativeMonoid
               ; *-semigroup; *-rawMonoid; *-monoid
               )

  semiringWithoutOne : SemiringWithoutOne _ _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
         using (nearSemiring)

record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                         : Set c
    _≈_                             : Rel Carrier ℓ
    _+_                             : Op₂ Carrier
    _*_                             : Op₂ Carrier
    0#                              : Carrier
    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0#

  open IsCommutativeSemiringWithoutOne
         isCommutativeSemiringWithoutOne public

  semiringWithoutOne : SemiringWithoutOne _ _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid
               ; +-commutativeMonoid
               ; *-semigroup
               ; nearSemiring
               )

record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ
    _+_                   : Op₂ Carrier
    _*_                   : Op₂ Carrier
    0#                    : Carrier
    1#                    : Carrier
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#

  open IsCommutativeSemiring isCommutativeSemiring public

  semiring : Semiring _ _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid
               ; +-commutativeMonoid
               ; *-semigroup; *-rawMonoid; *-monoid
               ; nearSemiring; semiringWithoutOne
               ; semiringWithoutAnnihilatingZero
               )

  *-commutativeMonoid : CommutativeMonoid _ _
  *-commutativeMonoid =
    record { isCommutativeMonoid = *-isCommutativeMonoid }

  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
  commutativeSemiringWithoutOne = record
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
    }

------------------------------------------------------------------------
-- (Commutative) rings

-- A raw ring is a ring without any laws.

record RawRing c : Set (suc c) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  field
    Carrier : Set c
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier

record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isRing  : IsRing _≈_ _+_ _*_ -_ 0# 1#

  open IsRing isRing public

  +-abelianGroup : AbelianGroup _ _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  semiring : Semiring _ _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid
               ; +-commutativeMonoid
               ; *-semigroup; *-rawMonoid; *-monoid
               ; nearSemiring; semiringWithoutOne
               ; semiringWithoutAnnihilatingZero
               )

  open AbelianGroup +-abelianGroup public
         using () renaming (group to +-group)

  rawRing : RawRing _
  rawRing = record
    { _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsCommutativeRing isCommutativeRing public

  ring : Ring _ _
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open Ring ring public using (rawRing; +-group; +-abelianGroup)
  open CommutativeSemiring commutativeSemiring public
         using ( setoid
               ; +-semigroup; +-rawMonoid; +-monoid; +-commutativeMonoid
               ; *-semigroup; *-rawMonoid; *-monoid; *-commutativeMonoid
               ; nearSemiring; semiringWithoutOne
               ; semiringWithoutAnnihilatingZero; semiring
               ; commutativeSemiringWithoutOne
               )

------------------------------------------------------------------------
-- (Distributive) lattices and boolean algebras

record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier   : Set c
    _≈_       : Rel Carrier ℓ
    _∨_       : Op₂ Carrier
    _∧_       : Op₂ Carrier
    isLattice : IsLattice _≈_ _∨_ _∧_

  open IsLattice isLattice public

  setoid : Setoid _ _
  setoid = record { isEquivalence = isEquivalence }

record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ
    _∨_                   : Op₂ Carrier
    _∧_                   : Op₂ Carrier
    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_

  open IsDistributiveLattice isDistributiveLattice public

  lattice : Lattice _ _
  lattice = record { isLattice = isLattice }

  open Lattice lattice public using (setoid)

record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 ¬_
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ
    _∨_              : Op₂ Carrier
    _∧_              : Op₂ Carrier
    ¬_               : Op₁ Carrier
    ⊤                : Carrier
    ⊥                : Carrier
    isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥

  open IsBooleanAlgebra isBooleanAlgebra public

  distributiveLattice : DistributiveLattice _ _
  distributiveLattice =
    record { isDistributiveLattice = isDistributiveLattice }

  open DistributiveLattice distributiveLattice public
         using (setoid; lattice)


text:
-- Some extra properties of integers.

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

module Integer.Properties where

-- imports from stdlib.
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality as PE
  using (_≡_ ; refl ; sym ; cong ; trans ; cong₂)

open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Data.Product as P using (_×_ ; _,_ ; ∃ ; proj₁ ; proj₂)
open import Data.Nat as Nat using (ℕ ; suc ; zero ; z≤n)
import Data.Nat.Solver as NS
open import Data.Integer as Int
  using (ℤ ; ∣_∣ ; +_ ; +[1+_] ; -[1+_] ; 1ℤ ; +<+ ; -<- ; -≤- ; -<+ ; -≤+ ; +≤+ ; 0ℤ ; NonNegative ; +0)
import Data.Integer.Properties as IntP
open import Function

-- imports from local.
open import Instances

-- Triangle equality.
tri-eq : ∀ (a b : ℤ) .{{_ : NonNegative a}} .{{_ : NonNegative b}} -> ∣ a + b ∣ ≡ ∣ a ∣ + ∣ b ∣
tri-eq (+_ a) (+_ b) = begin
  ∣ + a + + b ∣ ≡⟨ refl ⟩
  ∣ + (a + b) ∣ ≡⟨ refl ⟩
  a + b        ≡⟨ refl ⟩
  ∣ + a ∣ + ∣ + b ∣ ∎
    where
      open PE.≡-Reasoning

-- For all a, a * a is always non-negative.
a*a=+b : ∀ a -> ∃ λ b → a * a ≡ + b
a*a=+b (+_ a) = (a * a) , IntP.pos-distrib-* a a
a*a=+b (-[1+_] a) = suc a * suc a , refl

0≤a*a : ∀ {a} → 0ℤ ≤ a * a
0≤a*a {a} rewrite proj₂ $ a*a=+b a = +≤+ Nat.z≤n

-- For non-zero natrual number a, a * a is always positive.
a*a-pos : ∀ (a : ℕ) .{{_ : Nat.NonZero a}} -> ∃ λ n → a * a ≡ suc n
a*a-pos (suc b) = b * b + 2 * b , claim
  where
    claim : suc b * suc b ≡ suc (b * b + 2 * b)
    claim =
      begin
          suc b * suc b   ≡⟨ refl ⟩
      (1 + b) * (1 + b)   ≡⟨ solve 1 (λ b → (con 1 :+ b) :* (con 1 :+ b) := con 1 :+ (b :* b :+ con 2 :* b)) refl b ⟩
      1 + (b * b + 2 * b)  ≡⟨ refl ⟩
      suc (b * b + 2 * b) ∎
        where
          open NS.+-*-Solver
          open PE.≡-Reasoning

a*a-pos' : ∀ (a : ℤ) .{{_ : NonZero a}} -> ∃ λ n → a * a ≡ + (suc n)
a*a-pos' +[1+ n ] rewrite proj₂ $ a*a-pos (suc n) = (proj₁ $ a*a-pos (suc n)) , refl
a*a-pos' -[1+ n ] rewrite proj₂ $ a*a-pos (suc n) = (proj₁ $ a*a-pos (suc n)) , refl

-- For an non-zero integer a, ∣ a * a ∣ is always positive.
∣a*a∣-pos : ∀ (a : ℤ) .{{_ : NonZero a}} -> ∃ λ n → ∣ a * a ∣ ≡ suc n
∣a*a∣-pos (+ (suc b)) = b * b + 2 * b , claim
  where
    claim : suc b * suc b ≡ suc (b * b + 2 * b)
    claim = proj₂ $ a*a-pos (suc b)
∣a*a∣-pos (-[1+_] b) = b * b + 2 * b , claim
  where
    claim : suc b * suc b ≡ suc (b * b + 2 * b)
    claim = proj₂ $ a*a-pos (suc b)

+∣a*a∣=a*a : ∀ (a : ℤ) -> + ∣ a * a ∣ ≡ a * a
+∣a*a∣=a*a a = IntP.0≤i⇒+∣i∣≡i (0≤a*a {a})

pos : ∀ {a : ℤ} -> ¬ a ≡ 0ℤ -> 0ℤ < a * a
pos {+_ zero} n0 with n0 refl
... | ()
pos {a@(+[1+ n ])} n0 rewrite proj₂ $ a*a-pos' a = +<+ (Nat.s≤s Nat.z≤n)
pos {a@(-[1+ n ])} n0 rewrite proj₂ $ a*a-pos' a = +<+ (Nat.s≤s Nat.z≤n)

pos' : ∀ {a} -> 0ℤ < a -> Nat.NonZero ∣ a ∣
pos' {(+_ zero)} (+<+ ())
pos' {+[1+ n ]} l = record { nonZero = _ }

-- ∣ a * a + b * b ∣ is not zero if one of a and b is.
∣aa+bb∣-nonzero : ∀ a b -> ¬ a ≡ 0ℤ ⊎ ¬ b ≡ 0ℤ -> Nat.NonZero ∣ a * a + b * b ∣
∣aa+bb∣-nonzero a b (inj₁ x) = pos' (IntP.+-mono-<-≤ (pos x) (0≤a*a {b}))
∣aa+bb∣-nonzero a b (inj₂ y) = pos' (IntP.+-mono-≤-< (0≤a*a {a}) (pos y))

-- ----------------------------------------------------------------------
-- Properties of aa + bb

-- A special case of tri-eq.
tri-eq' : ∀ a b -> ∣ a * a + b * b ∣ ≡ ∣ a * a ∣ + ∣ b * b ∣
tri-eq' a b = begin
      let (sa , sae) = (a*a=+b a) in let (sb , sbe) = a*a=+b b in
       ∣ a * a + b * b ∣  ≡⟨ cong (λ x → ∣ x ∣) (cong₂ _+_ sae sbe) ⟩
       ∣ + sa + + sb ∣  ≡⟨ (tri-eq (+ sa) (+ sb)) ⟩
       ∣ + sa ∣ + ∣ + sb ∣  ≡⟨ cong₂ _+_ (cong ∣_∣ (sym sae)) (cong ∣_∣ (sym sbe)) ⟩
       ∣ a * a ∣ + ∣ b * b ∣ ∎
        where
          open PE.≡-Reasoning

-- A property of a pair of integers.
a=0×b=0⇒aa+bb=0 : ∀ {a b : ℤ} -> a ≡ 0ℤ × b ≡ 0ℤ -> a * a + b * b ≡ 0ℤ
a=0×b=0⇒aa+bb=0 {.0ℤ} {.0ℤ} (refl , refl) = refl

aa+bb=0⇒a=0×b=0 : ∀ {a b : ℤ} -> a * a + b * b ≡ 0ℤ -> a ≡ 0ℤ × b ≡ 0ℤ
aa+bb=0⇒a=0×b=0 {a} {b} eq = P.map x^2=0⇒x=0 x^2=0⇒x=0 $ z+z (0≤a*a {a}) (0≤a*a {b}) eq
  where
    z+z : ∀ {x y} -> 0ℤ ≤ x -> 0ℤ ≤ y -> x + y ≡ 0ℤ -> x ≡ 0ℤ × y ≡ 0ℤ
    z+z {.+0} {.(+ _)} (+≤+ {n = zero} z≤n) (+≤+ z≤n) x+y=0 = (refl , x+y=0)
    z+z {.(+[1+ n ])} {.+0} (+≤+ {n = ℕ.suc n} z≤n) (+≤+ {n = zero} m≤n) ()
    z+z {.(+[1+ n ])} {.(+[1+ n₁ ])} (+≤+ {n = ℕ.suc n} z≤n) (+≤+ {n = ℕ.suc n₁} m≤n) ()

    x^2=0⇒x=0 : ∀ {x} -> x * x ≡ 0ℤ -> x ≡ 0ℤ
    x^2=0⇒x=0 {+_ zero} eq = refl

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
module FRP.LTL.RSet where

open import FRP.LTL.RSet.Core public using ( RSet ; ⟨_⟩ ; ⟦_⟧ )

-- Propositional logic

open import FRP.LTL.RSet.Unit public using ( T )
open import FRP.LTL.RSet.Empty public using ( F )
open import FRP.LTL.RSet.Product public using ( _∧_ ; fst ; snd ; _&&&_ )
open import FRP.LTL.RSet.Sum public using ( _∨_ )
open import FRP.LTL.RSet.Stateless public using ( _⇒_ )

-- LTL

open import FRP.LTL.RSet.Next public using ( ○ )
open import FRP.LTL.RSet.Future public using ( ◇ )
open import FRP.LTL.RSet.Globally public using ( □ ; [_] )
open import FRP.LTL.RSet.Until public using ( _U_ )
open import FRP.LTL.RSet.Causal public using ( _⊵_ ; arr ; identity ; _⋙_ )
open import FRP.LTL.RSet.Decoupled public using ( _▹_ )

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:
{-# OPTIONS --without-K #-}

module A2 where

open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

infix  4  _≡_   -- propositional equality
infixr 10 _◎_
infixr 30 _⟷_

------------------------------------------------------------------------------
-- Our own version of refl that makes 'a' explicit

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

sym : ∀ {ℓ} {A : Set ℓ} {a b : A} → (a ≡ b) → (b ≡ a)
sym {a = a} {b = .a} (refl .a) = refl a

trans : ∀ {ℓ} {A : Set ℓ} {a b c : A} → (a ≡ b) → (b ≡ c) → (a ≡ c)
trans {a = a} {b = .a} {c = .a} (refl .a) (refl .a) = refl a

------------------------------------------------------------------------------
{--
Types are higher groupoids:
- 0 is empty
- 1 has one element and one path refl
- sum type is disjoint union; paths are component wise
- product type is cartesian product; paths are pairs of paths
--}

mutual

  data U : Set where
    ZERO  : U
    ONE   : U
    PLUS  : U → U → U
    TIMES : U → U → U
    ID    : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧ → U

  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧        = ⊥
  ⟦ ONE ⟧         = ⊤
  ⟦ PLUS t t' ⟧   = ⟦ t ⟧ ⊎ ⟦ t' ⟧
  ⟦ TIMES t t' ⟧  = ⟦ t ⟧ × ⟦ t' ⟧
  ⟦ ID {t₁} {t₂} c v₁ v₂ ⟧ = Paths {t₁} {t₂} c v₁ v₂

  data _⟷_ : U → U → Set where
    -- semiring axioms
    unite₊  : {t : U} → PLUS ZERO t ⟷ t
    uniti₊  : {t : U} → t ⟷ PLUS ZERO t
    swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
    assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
    assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
    unite⋆  : {t : U} → TIMES ONE t ⟷ t
    uniti⋆  : {t : U} → t ⟷ TIMES ONE t
    swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
    assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
    assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
    distz   : {t : U} → TIMES ZERO t ⟷ ZERO
    factorz : {t : U} → ZERO ⟷ TIMES ZERO t
    dist    : {t₁ t₂ t₃ : U} →
              TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
    factor  : {t₁ t₂ t₃ : U} →
              PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
    -- equivalence relation and 2 combinators
    id⟷    : {t : U} → t ⟷ t
    sym⟷   : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
    _⊕_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
    _⊗_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)
   -- and one level up
{-
    lid : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
          ID (id⟷ ◎ c) v₁ v₂ ⟷ ID c v₁ v₂
    rid : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
          ID (c ◎ id⟷) v₁ v₂ ⟷ ID c v₁ v₂
    linv : {t₁ t₂ : U} {v : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
           ID ((sym⟷ c) ◎ c) v v ⟷ ID {t₂} {t₂} id⟷ v v
    rinv : {t₁ t₂ : U} {v : ⟦ t₁ ⟧} {c : t₁ ⟷ t₂} →
           ID (c ◎ (sym⟷ c)) v v ⟷ ID {t₁} {t₁} id⟷ v v
    invinv : {t₁ t₂ : U} {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {c : t₁ ⟷ t₂} →
           ID (sym⟷ (sym⟷ c)) v₁ v₂ ⟷ ID {t₁} {t₂} c v₁ v₂
    assoc : {t₁ t₂ t₃ t₄ : U}
            {v₁ : ⟦ t₁ ⟧} {v₂ : ⟦ t₂ ⟧} {v₃ : ⟦ t₃ ⟧} {v₄ : ⟦ t₄ ⟧}
            {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
            ID (c₁ ◎ (c₂ ◎ c₃)) v₁ v₄ ⟷ ID ((c₁ ◎ c₂) ◎ c₃) v₁ v₄
-}
-- add the other direction for lid, rid, linv, rinv, invinv, and assoc

  data Unite₊ {t : U} : ⊥ ⊎ ⟦ t ⟧ → ⟦ t ⟧ → Set where
    val_unite₊ : (v₁ : ⊥ ⊎ ⟦ t ⟧) → (v₂ : ⟦ t ⟧) → Unite₊ v₁ v₂

  Paths : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧ → Set
  Paths unite₊ (inj₁ ())
  Paths {PLUS ZERO t} {.t} unite₊ (inj₂ v) v' = (v ≡ v') × Unite₊ {t} (inj₂ v) v'
  Paths uniti₊ v (inj₁ ())
  Paths uniti₊ v (inj₂ v') = (v ≡ v')
  Paths swap₊ (inj₁ v) (inj₁ v') = ⊥
  Paths swap₊ (inj₁ v) (inj₂ v') = (v ≡ v')
  Paths swap₊ (inj₂ v) (inj₁ v') = (v ≡ v')
  Paths swap₊ (inj₂ v) (inj₂ v') = ⊥
  Paths assocl₊ (inj₁ v) (inj₁ (inj₁ v')) = (v ≡ v')
  Paths assocl₊ (inj₁ v) (inj₁ (inj₂ v')) = ⊥
  Paths assocl₊ (inj₁ v) (inj₂ v') = ⊥
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₁ (inj₁ v')) = ⊥
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₁ (inj₂ v')) = (v ≡ v')
  Paths assocl₊ (inj₂ (inj₁ v)) (inj₂ v') = ⊥
  Paths assocl₊ (inj₂ (inj₂ v)) (inj₁ v') = ⊥
  Paths assocl₊ (inj₂ (inj₂ v)) (inj₂ v') = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₁ v)) (inj₁ v') = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₁ v)) (inj₂ v') = ⊥
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₁ v') = ⊥
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₂ (inj₁ v')) = (v ≡ v')
  Paths assocr₊ (inj₁ (inj₂ v)) (inj₂ (inj₂ v')) = ⊥
  Paths assocr₊ (inj₂ v) (inj₁ v') = ⊥
  Paths assocr₊ (inj₂ v) (inj₂ (inj₁ v')) = ⊥
  Paths assocr₊ (inj₂ v) (inj₂ (inj₂ v')) = (v ≡ v')
  Paths unite⋆ (tt , v) v' = (v ≡ v')
  Paths uniti⋆ v (tt , v') = (v ≡ v')
  Paths swap⋆ (v₁ , v₂) (v₂' , v₁') = (v₁ ≡ v₁') × (v₂ ≡ v₂')
  Paths assocl⋆ (v₁ , (v₂ , v₃)) ((v₁' , v₂') , v₃') =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths assocr⋆ ((v₁ , v₂) , v₃) (v₁' , (v₂' , v₃')) =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths distz (() , v)
  Paths factorz ()
  Paths dist (inj₁ v₁ , v₃) (inj₁ (v₁' , v₃')) = (v₁ ≡ v₁') × (v₃ ≡ v₃')
  Paths dist (inj₁ v₁ , v₃) (inj₂ (v₂' , v₃')) = ⊥
  Paths dist (inj₂ v₂ , v₃) (inj₁ (v₁' , v₃')) = ⊥
  Paths dist (inj₂ v₂ , v₃) (inj₂ (v₂' , v₃')) = (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths factor (inj₁ (v₁ , v₃)) (inj₁ v₁' , v₃') =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  Paths factor (inj₁ (v₁ , v₃)) (inj₂ v₂' , v₃') = ⊥
  Paths factor (inj₂ (v₂ , v₃)) (inj₁ v₁' , v₃') = ⊥
  Paths factor (inj₂ (v₂ , v₃)) (inj₂ v₂' , v₃') =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  Paths {t} id⟷ v v' = (v ≡ v')
  Paths (sym⟷ c) v v' = PathsB c v v'
  Paths (_◎_ {t₁} {t₂} {t₃} c₁ c₂) v v' =
    Σ[ u ∈ ⟦ t₂ ⟧ ] (Paths c₁ v u × Paths c₂ u v')
  Paths (c₁ ⊕ c₂) (inj₁ v) (inj₁ v') = Paths c₁ v v'
  Paths (c₁ ⊕ c₂) (inj₁ v) (inj₂ v') = ⊥
  Paths (c₁ ⊕ c₂) (inj₂ v) (inj₁ v') = ⊥
  Paths (c₁ ⊕ c₂) (inj₂ v) (inj₂ v') = Paths c₂ v v'
  Paths (c₁ ⊗ c₂) (v₁ , v₂) (v₁' , v₂') =
    Paths c₁ v₁ v₁' × Paths c₂ v₂ v₂'
{-
  Paths lid (v , refl .v , p) q = (p ≡ q)
  Paths rid (v , p , refl .v) q = (p ≡ q)
  Paths (linv {t₁} {v = v} {c}) (w , proj₂ , proj₃) y = {!!}
  Paths rinv (proj₁ , proj₂ , proj₃) y = {!!}
  Paths (invinv {c = c}) x y = {!!}
  Paths assoc (v₂ , proj₂ , v₃ , proj₄ , proj₅) (w₃ , (w₂ , proj₈ , proj₉) , proj₁₀) = v₂ ≡ w₂ × v₃ ≡ w₃
-}

  PathsB : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₂ ⟧ → ⟦ t₁ ⟧ → Set
  PathsB unite₊ v (inj₁ ())
  PathsB unite₊ v (inj₂ v') = (v ≡ v')
  PathsB uniti₊ (inj₁ ())
  PathsB uniti₊ (inj₂ v) v' = (v ≡ v')
  PathsB swap₊ (inj₁ v) (inj₁ v') = ⊥
  PathsB swap₊ (inj₁ v) (inj₂ v') = (v ≡ v')
  PathsB swap₊ (inj₂ v) (inj₁ v') = (v ≡ v')
  PathsB swap₊ (inj₂ v) (inj₂ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₁ v)) (inj₁ v') = (v ≡ v')
  PathsB assocl₊ (inj₁ (inj₁ v)) (inj₂ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₁ v') = ⊥
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₂ (inj₁ v')) = (v ≡ v')
  PathsB assocl₊ (inj₁ (inj₂ v)) (inj₂ (inj₂ v')) = ⊥
  PathsB assocl₊ (inj₂ v) (inj₁ v') = ⊥
  PathsB assocl₊ (inj₂ v) (inj₂ (inj₁ v')) = ⊥
  PathsB assocl₊ (inj₂ v) (inj₂ (inj₂ v')) = (v ≡ v')
  PathsB assocr₊ (inj₁ v) (inj₁ (inj₁ v')) = (v ≡ v')
  PathsB assocr₊ (inj₁ v) (inj₁ (inj₂ v')) = ⊥
  PathsB assocr₊ (inj₁ v) (inj₂ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₁ (inj₁ v')) = ⊥
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₁ (inj₂ v')) = (v ≡ v')
  PathsB assocr₊ (inj₂ (inj₁ v)) (inj₂ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₂ v)) (inj₁ v') = ⊥
  PathsB assocr₊ (inj₂ (inj₂ v)) (inj₂ v') = (v ≡ v')
  PathsB unite⋆ v (tt , v') = (v ≡ v')
  PathsB uniti⋆ (tt , v) v' = (v ≡ v')
  PathsB swap⋆ (v₁ , v₂) (v₂' , v₁') = (v₁ ≡ v₁') × (v₂ ≡ v₂')
  PathsB assocl⋆ ((v₁ , v₂) , v₃) (v₁' , (v₂' , v₃')) =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB assocr⋆ (v₁ , (v₂ , v₃)) ((v₁' , v₂') , v₃') =
    (v₁ ≡ v₁') × (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB distz ()
  PathsB factorz (() , v)
  PathsB dist (inj₁ (v₁ , v₃)) (inj₁ v₁' , v₃') =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  PathsB dist (inj₁ (v₁ , v₃)) (inj₂ v₂' , v₃') = ⊥
  PathsB dist (inj₂ (v₂ , v₃)) (inj₁ v₁' , v₃') = ⊥
  PathsB dist (inj₂ (v₂ , v₃)) (inj₂ v₂' , v₃') =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB factor (inj₁ v₁ , v₃) (inj₁ (v₁' , v₃')) =
    (v₁ ≡ v₁') × (v₃ ≡ v₃')
  PathsB factor (inj₁ v₁ , v₃) (inj₂ (v₂' , v₃')) = ⊥
  PathsB factor (inj₂ v₂ , v₃) (inj₁ (v₁' , v₃')) = ⊥
  PathsB factor (inj₂ v₂ , v₃) (inj₂ (v₂' , v₃')) =
    (v₂ ≡ v₂') × (v₃ ≡ v₃')
  PathsB {t} id⟷ v v' = (v ≡ v')
  PathsB (sym⟷ c) v v' = Paths c v v'
  PathsB (_◎_ {t₁} {t₂} {t₃} c₁ c₂) v v' =
    Σ[ u ∈ ⟦ t₂ ⟧ ] (PathsB c₂ v u × PathsB c₁ u v')
  PathsB (c₁ ⊕ c₂) (inj₁ v) (inj₁ v') = PathsB c₁ v v'
  PathsB (c₁ ⊕ c₂) (inj₁ v) (inj₂ v') = ⊥
  PathsB (c₁ ⊕ c₂) (inj₂ v) (inj₁ v') = ⊥
  PathsB (c₁ ⊕ c₂) (inj₂ v) (inj₂ v') = PathsB c₂ v v'
  PathsB (c₁ ⊗ c₂) (v₁ , v₂) (v₁' , v₂') =
    PathsB c₁ v₁ v₁' × PathsB c₂ v₂ v₂'
{-
  PathsB rid q (a , p , refl .a) = q ≡ p
  PathsB lid x y = {!!}
  PathsB linv x y = {!!}
  PathsB rinv = {!!}
  PathsB invinv = {!!}
  PathsB assoc = {!!}
-}
------------------------------------------------------------------------------
-- Examples...

BOOL : U
BOOL = PLUS ONE ONE

BOOL² : U
BOOL² = TIMES BOOL BOOL

FALSE : ⟦ BOOL ⟧
FALSE = inj₂ tt

TRUE : ⟦ BOOL ⟧
TRUE = inj₁ tt

e₁ : ⟦ ID {BOOL²} {BOOL²} id⟷ (FALSE , TRUE) (FALSE , TRUE) ⟧
e₁ = refl (FALSE , TRUE)

e₂ : ⟦ ID {BOOL²} {BOOL²} (id⟷ ⊗ id⟷) (FALSE , TRUE) (FALSE , TRUE) ⟧
e₂ = (refl FALSE , refl TRUE)
---------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 3zero, 2zerozero7

                Hello Agda!

                Ulf Norell

-}

-- Records are labeled sigma types.

module R where

{-

  A very simple record.

-}

data Nat : Set where
  zero : Nat
  succ : Nat

record Point : Set where
  field x : Nat
        y : Nat

-- A record can be seen as a one constructor datatype. In this case:
data Point' : Set where
  mkPoint : (x : Nat)(y : Nat) -> Point'

-- There are a few differences, though:

-- To construct a record you use the syntax record { ..; x = e; .. }
origin : Point
origin = record { x = zero; y = zero }

-- instead of
origin' : Point'
origin' = mkPoint zero zero

-- What's more interesting is that you get projection functions
-- for free when you declare a record. More precisely, you get a module
-- parameterised over a record, containing functions corresponding to the
-- fields. In the Point example you get:
{-
  module Point (p : Point) where
    x : Nat
    y : Nat
-}

-- So Point.x : Point -> Nat is the projection function for the field x.
getX : Point -> Nat
getX = Point.x
-- getX = x

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
open import Oscar.Prelude

module Oscar.Class.Fmap where

module _ where
  open import Oscar.Data.Proposequality
  open import Oscar.Class.IsFunctor
  open import Oscar.Class.Reflexivity
  import Oscar.Class.Reflexivity.Function
  open import Oscar.Class.Surjidentity

  record Fmap {𝔬₁ 𝔬₂} (𝓕 : Ø 𝔬₁ → Ø 𝔬₂) : Ø (↑̂ (↑̂ 𝔬₁ ∙̂ 𝔬₂)) where
    constructor ∁
    field
      fmap : ∀ {𝔄 𝔅} → (𝔄 → 𝔅) → 𝓕 𝔄 → 𝓕 𝔅 -- level-polymorphic functors cannot be represented by `Functor` or any other type in universe < ω.
      ⦃ isFunctor ⦄ : IsFunctor
                         Function⟦ 𝔬₁ ⟧
                           Proposextensequality ε (flip _∘′_)
                         (MFunction 𝓕)
                           Proposextensequality ε (flip _∘′_)
                         fmap
    fmap-id-law : ∀ {𝔄} → fmap ¡[ 𝔄 ] ≡̇ ¡
    fmap-id-law = surjidentity

  open Fmap ⦃ … ⦄ public using (fmap)

-- level-polymorphic functor
module _
  (𝔉 : ∀ {𝔣} → Ø 𝔣 → Ø 𝔣)
  𝔬₁ 𝔬₂
  where
  𝓯map = ∀ {𝔒₁ : Ø 𝔬₁} {𝔒₂ : Ø 𝔬₂} (f : 𝔒₁ → 𝔒₂) → 𝔉 𝔒₁ → 𝔉 𝔒₂
  record 𝓕map : Ø ↑̂ (𝔬₁ ∙̂ 𝔬₂) where field fmap′ : 𝓯map
open 𝓕map ⦃ … ⦄ public


text:
module SyntaxRaw where

import Level
open import Data.Empty
open import Data.Unit as Unit
open import Data.Nat
open import Data.List as List renaming ([] to Ø; [_] to [_]L)
open import Data.List.Properties using (++-monoid)
open import NonEmptyList as NList
open import Data.Vec as Vec hiding ([_]; _++_)
open import Data.Product as Prod
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

open import Common.Context as Context

open import Algebra
open Monoid {{ ... }} hiding (refl)

data Phantom {A : Set} (a : A) : Set where
  phantom : Phantom a

record Univ (P : Phantom tt) : Set where
  field
    x : ⊤

U : Set
U = Σ (Phantom tt) Univ

∗ : U
∗ = (phantom , record { x = tt })

length' : {A : Set} → List A → ℕ
length' Ø = 0
length' (x ∷ xs) = suc (length' xs)

length'-hom : {A : Set} → (l₁ l₂ : List A) →
             length' (l₁ ++ l₂) ≡ length' l₁ + length' l₂
length'-hom Ø        l₂ = refl
length'-hom (x ∷ l₁) l₂ = cong suc (length'-hom l₁ l₂)

length'ᵣ-1 : {A : Set} (l : List A) (a : A) →
             (length' l) + 1 ≡ length' (l ++ a ∷ Ø)
length'ᵣ-1 Ø a = refl
length'ᵣ-1 (x ∷ l) a = cong suc (length'ᵣ-1 l a)

length'-commute₁ : {A : Set} (l : List A) (a : A) →
                   length' (a ∷ l) ≡ length' (l ++ a ∷ Ø)
length'-commute₁ Ø a = refl
length'-commute₁ (x ∷ l) a = cong suc (length'-commute₁ l a)

mvVar : ∀ {A} (Γ₁ Γ₂ : List A) (x : A) → Γ₂ ++ x ∷ Γ₁ ≡ Γ₂ ↑ x ++ Γ₁
mvVar Γ₁ Ø x = refl
mvVar Γ₁ (y ∷ Γ₂) x = cong (λ u → y ∷ u) (mvVar Γ₁ Γ₂ x)

mvVar-length : ∀ {A} (Γ₁ Γ₂ : List A) (x : A) →
               length' (Γ₂ ++ x ∷ Γ₁) ≡ length' (Γ₂ ↑ x ++ Γ₁)
mvVar-length Γ₁ Γ₂ x = cong length' (mvVar Γ₁ Γ₂ x)

data FP : Set where
  μ : FP
  ν : FP

RawCtx : Set
RawCtx = Ctx U

instance ctx-monoid : Monoid _ _
ctx-monoid = ++-monoid U

RawVar : RawCtx → U → Set
RawVar = Var

TyCtx : Set
TyCtx = Ctx RawCtx

instance tyctx-monoid : Monoid _ _
tyctx-monoid = ++-monoid RawCtx

TyVar : TyCtx → RawCtx → Set
TyVar = Var

CtxMor : (TyCtx → RawCtx → RawCtx → Set) → RawCtx → RawCtx → Set
CtxMor R Γ₁ Γ₂ = Vec (R Ø Γ₁ Ø) (length' Γ₂)

FpData : (TyCtx → RawCtx → RawCtx → Set) → TyCtx → RawCtx → Set
FpData R Θ Γ = NList (Σ RawCtx (λ Γ' → CtxMor R Γ' Γ × R (Γ ∷ Θ) Γ' Ø))

-- | List of types, context morphisms and terms (Aₖ, fₖ, gₖ) such that
--            Γₖ, x : Aₖ[C/X] ⊢ gₖ : C fₖ or
--            Γₖ, x : C fₖ ⊢ gₖ : Aₖ[C/X],
-- which are the premisses of the rule for recursion and corecursion,
-- respectively.
FpMapData : (TyCtx → RawCtx → RawCtx → Set) → RawCtx → Set
FpMapData R Γ = NList (Σ RawCtx λ Γ' →
                         R [ Γ ]L Γ' Ø × CtxMor R Γ' Γ × R Ø (∗ ∷ Γ') Ø)

-- | Types and objects with their corresponding (untyped) type, object
-- variable contexts and parameter contexts.
-- Note that, if Θ | Γ₁ ⊢ M ⊸ Γ₂, i.e., M : Raw Θ Γ₁ Γ₂,
-- then Γ₂ needs to be read in reverse. The reason is that Γ₂ signifies
-- parameters that are instantiated in application-style. Also, variables
-- can be moved for types like in
-- Γ₁, x : A ⊢ B : Γ₂(∗)  → Γ₁ ⊢ λx.B : (x : A) ⊸ Γ₂(∗).
data Raw : TyCtx → RawCtx → RawCtx → Set where
  ----- Common constructors
  instRaw : {Θ : TyCtx} {Γ₁ Γ₂ : RawCtx} {A : U} →
            Raw Θ Γ₁ (Γ₂ ↑ A) → Raw Ø Γ₁ Ø → Raw Θ Γ₁ Γ₂

  ----- Object constructors
  unitRaw : (Γ : RawCtx) → Raw Ø Γ Ø
  objVarRaw : {Γ : RawCtx} {A : U} → RawVar Γ A → Raw Ø Γ Ø
  -- | initial/final dialgebra. dialgRaw ρ k is either αₖ or ξₖ, depending on ρ.
  dialgRaw : (Δ : RawCtx) (Γ : RawCtx) (A : U) → FP → ℕ → Raw Ø Δ (A ∷ Γ)
  recRaw : (Γ Δ : RawCtx) → FpMapData Raw Γ → FP → Raw Ø Δ (∗ ∷ Γ)

  ----- Type constructors
  ⊤-Raw : (Θ : TyCtx) (Γ : RawCtx) → Raw Θ Γ Ø
  tyVarRaw : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ : RawCtx} → TyVar Θ Γ₂ → Raw Θ Γ₁ Γ₂
  paramAbstrRaw : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) {A : U} →
                  Raw Θ (A ∷ Γ₁) Γ₂ → Raw Θ Γ₁ (Γ₂ ↑ A)
  -- | Constructor for fixed points. The first component is intended to be
  -- the context morphism, the second is the type.
  fpRaw : {Θ : TyCtx} {Γ₂ : RawCtx} (Γ₁ : RawCtx) →
          FP → FpData Raw Θ Γ₂ → Raw Θ Γ₁ Γ₂

weakenObjVar : (Γ₁ : RawCtx) {Γ₂ : RawCtx} →
               (A : U) {B : U} → RawVar (Γ₁ ++ Γ₂) B → RawVar (Γ₁ ++ A ∷ Γ₂) B
weakenObjVar Ø         A x           = succ _ x
weakenObjVar (._ ∷ Γ₁) A zero        = zero
weakenObjVar (B ∷ Γ₁)  A (succ ._ x) = succ _ (weakenObjVar Γ₁ A x)

weaken : {Θ : TyCtx} (Γ₁ : RawCtx) {Γ₂ Γ₃ : RawCtx} →
         (A : U) → Raw Θ (Γ₁ ++ Γ₂) Γ₃ → Raw Θ (Γ₁ ++ A ∷ Γ₂) Γ₃
weaken Γ₁ {Γ₂} A (instRaw t s)                     =
  instRaw (weaken Γ₁ A t) (weaken Γ₁ A s)
weaken Γ₁ {Γ₂} A (unitRaw .(Γ₁ ++ Γ₂))             = unitRaw _
weaken Γ₁ {Γ₂} A (objVarRaw x)         =
  objVarRaw (weakenObjVar Γ₁ A x)
weaken Γ₁ {Γ₂} A (dialgRaw .(Γ₁ ++ Γ₂) Γ B ρ k)    = dialgRaw _ Γ B ρ k
weaken Γ₁ {Γ₂} A (recRaw Γ .(Γ₁ ++ Γ₂) gs ρ)       = recRaw Γ _ gs ρ
weaken Γ₁ {Γ₂} A (⊤-Raw Θ .(Γ₁ ++ Γ₂))             = ⊤-Raw Θ _
weaken Γ₁ {Γ₂} A (tyVarRaw .(Γ₁ ++ Γ₂) X)          = tyVarRaw _ X
weaken Γ₁ {Γ₂} A (paramAbstrRaw .(Γ₁ ++ Γ₂) {B} C) =
  paramAbstrRaw (Γ₁ ++ A ∷ Γ₂) (weaken (B ∷ Γ₁) A C)
weaken Γ₁ {Γ₂} A (fpRaw .(Γ₁ ++ Γ₂) ρ D)           = fpRaw _ ρ D

weaken₁ : ∀ {Θ Γ₁ Γ₂} → (A : U) → Raw Θ Γ₁ Γ₂ → Raw Θ (A ∷ Γ₁) Γ₂
weaken₁ = weaken Ø

ctxid : (Γ : RawCtx) → CtxMor Raw Γ Γ
ctxid Ø = []
ctxid (A ∷ Γ) = (objVarRaw {A ∷ Γ} {A} zero)
                ∷ Vec.map (weaken Ø A) (ctxid Γ)

-- | Build the instantiation "t f" of a raw term t by a context morphism f
instWCtxMor : {Θ : TyCtx} {Γ₁ Γ₂ Γ₃ : RawCtx} →
              Raw Θ Γ₁ (Γ₃ ++ Γ₂) → CtxMor Raw Γ₁ Γ₂ → Raw Θ Γ₁ Γ₃
instWCtxMor {Θ} {Γ₁} {Ø} {Γ₃} t [] = subst (Raw Θ Γ₁) (proj₂ identity Γ₃) t
instWCtxMor {Θ} {Γ₁} {x ∷ Γ₂} {Γ₃} t (s ∷ f) =
  instRaw (instWCtxMor (subst (Raw Θ Γ₁) (mvVar _ Γ₃ x) t) f) s

-- | Retrieve the term to be substituted for a variable from a context morphism
get : {R : TyCtx → RawCtx → RawCtx → Set} {Γ₁ Γ₂ : RawCtx} {A : U} →
      CtxMor R Γ₂ Γ₁ → RawVar Γ₁ A → R Ø Γ₂ Ø
get {R} {Ø}       []     ()
get {R} {_ ∷ Γ₁} (M ∷ f) zero        = M
get {R} {_ ∷ Γ₁} (M ∷ f) (succ ._ x) = get {R} f x

-- | Extends a context morphism to be the identity on a new variable
extend : {Γ₁ Γ₂ : RawCtx} →
         (A : U) → CtxMor Raw Γ₂ Γ₁ → CtxMor Raw (A ∷ Γ₂) (A ∷ Γ₁)
extend {Γ₁} {Γ₂} A f = (objVarRaw {A ∷ Γ₂} {A} zero) ∷ (Vec.map (weaken₁ A) f)

-- | Substitution on raw terms
substRaw : ∀ {Θ Γ₁ Γ Γ₂} → Raw Θ Γ₁ Γ → CtxMor Raw Γ₂ Γ₁ → Raw Θ Γ₂ Γ
substRaw (instRaw M N)         f = instRaw (substRaw M f) (substRaw N f)
substRaw (unitRaw Γ)           f = unitRaw _
substRaw (objVarRaw x)         f = get {Raw} f x
substRaw (dialgRaw Δ Γ A ρ k)  f = dialgRaw _ Γ A ρ k
substRaw (recRaw Γ Δ gs ρ)     f = recRaw Γ _ gs ρ
substRaw (⊤-Raw Θ Γ)           f = ⊤-Raw Θ _
substRaw (tyVarRaw Γ₁ X)       f = tyVarRaw _ X
substRaw (paramAbstrRaw Γ₁ A)  f = paramAbstrRaw _ (substRaw A (extend _ f))
substRaw (fpRaw Γ₁ ρ D)        f = fpRaw _ ρ D

-- | Context morphism that projects on arbitrary prefix of a context
ctxProjRaw : (Γ₁ Γ₂ : RawCtx) → CtxMor Raw (Γ₂ ++ Γ₁) Γ₁
ctxProjRaw Γ₁ Ø = ctxid Γ₁
ctxProjRaw Γ₁ (A ∷ Γ₂) = Vec.map (weaken₁ A) (ctxProjRaw Γ₁ Γ₂)

-- | Extend one step weakening to weakening by arbitrary contexts
weaken' : ∀ {Θ Γ₁ Γ₃} →
          (Γ₂ : RawCtx) → Raw Θ Γ₁ Γ₃ → Raw Θ (Γ₂ ++ Γ₁) Γ₃
weaken' {Γ₁ = Γ₁} Γ₂ t = substRaw t (ctxProjRaw Γ₁ Γ₂)

-----------------------------------------
--- Examples
-----------------------------------------

_︵_ : {A : Set} → A → A → List A
a ︵ b = a ∷ b ∷ Ø

-- | Binary product type
ProdRaw : (Γ : RawCtx) → Raw (Γ ︵ Γ) Ø Γ
ProdRaw Γ = fpRaw Ø ν D
  where
    Δ = Γ ︵ Γ

    A : TyVar (Γ ∷ Δ) Γ
    A = succ Γ zero

    B : TyVar (Γ ∷ Δ) Γ
    B = succ Γ (succ Γ zero)

    D₁ = (Γ , ctxid Γ , instWCtxMor (tyVarRaw Γ A) (ctxid Γ))

    D₂ = (Γ , ctxid Γ , instWCtxMor (tyVarRaw Γ B) (ctxid Γ))

    D : FpData Raw Δ Γ
    D = D₁ ∷ [ D₂ ]

max_stars_repo_name: StillerHarpo/CoindDepTypes

max_issues_repo_name: StillerHarpo/CoindDepTypes

max_forks_repo_name: StillerHarpo/CoindDepTypes


text:
{-# OPTIONS --copatterns #-}

module CS410-Indexed where

open import CS410-Prelude
open import CS410-Nat

-- some notation for working with indexed sets

_-:>_ _*:_ _+:_ : {I : Set}(S T : I -> Set) -> I -> Set

(S -:> T) i = S i -> T i   -- index-respecting functions
(S *: T) i = S i * T i     -- index-matching pairs
(S +: T) i = S i + T i     -- index-consistent choice

infixr 3 _-:>_
infixr 5 _*:_

-- wrapping in the brackets means "works for all indices"

[_] : {I : Set}(X : I -> Set) -> Set
[ X ] = forall {i} -> X i

-- each set I gives us a category, I -> Set, whose objects are
-- indexed sets A : I -> Set, and whose arrows are
-- things in [ A -:> B ]

-- what is a functor between categories of indexed sets?

record FunctorIx {I J : Set}(F : (I -> Set) -> (J -> Set)) : Set1 where
  field
    mapIx : {A B : I -> Set} -> [ A -:> B ] -> [ F A -:> F B ]

-- what is a monad on indexed sets?
-- it's the usual kit for monads, instantiated for the kinds of
-- "arrows" that we use for indexed sets, the index-respecting functions

record MonadIx {W : Set}(F : (W -> Set) -> (W -> Set)) : Set1 where
  field
    retIx : forall {P} -> [ P -:> F P ]
    extendIx : forall {P Q} -> [ P -:> F Q ] -> [ F P -:> F Q ]
  _?>=_ : forall {P Q w} ->
          F P w -> (forall {v} -> P v -> F Q v) -> F Q w
  fp ?>= k = extendIx k fp

-- every MonadIx gives a FunctorIx

monadFunctorIx : forall {W}{F} -> MonadIx {W} F -> FunctorIx {W}{W} F
monadFunctorIx M = record { mapIx = \ f -> extendIx (retIx o f) }
  where open MonadIx M

-- indexed containers, also known as interaction strutures, give us
-- functors

record _=>_ (I J : Set) : Set1 where
  constructor _<!_/_
  field
    Shape     : J -> Set
    Position  : (j : J) -> Shape j -> Set
    index     : (j : J)(s : Shape j) -> Position j s -> I

IC : forall {I J} -> I => J -> (I -> Set) -> (J -> Set)
IC {I}{J} C X j = Sg (Shape j) \ s -> (p : Position j s) -> X (index j s p)
  where open _=>_ C

icFunctorIx : forall {I J}(C : I => J) -> FunctorIx (IC C)
icFunctorIx C = record { mapIx = \ {f (s , k) -> s , \ p -> f (k p) }  }
  where open _=>_ C

-- iterating an indexed container whose input (child) and output (parent) index
-- types are the same gives us "strategy trees"

data FreeIx {I}(C : I => I)(X : I -> Set)(i : I) : Set where
  ret : (X -:> FreeIx C X) i
  do  : (IC C (FreeIx C X) -:> FreeIx C X) i

-- and they're monadic

freeMonadIx : forall {I}(C : I => I) -> MonadIx (FreeIx C)
freeMonadIx C = record { retIx = ret ; extendIx = graft } where
  graft : forall {P Q} -> [ P -:> FreeIx C Q ] -> [ FreeIx C P -:> FreeIx C Q ]
  graft k (ret p) = k p
  graft k (do (s , f)) = do (s , \ p -> graft k (f p))

-- potentially infinite strategies

data Iterating {I}(C : I => I)(X : I -> Set)(i : I) : Set

record IterIx {I}(C : I => I)(X : I -> Set)(i : I) : Set where
  coinductive
  constructor step
  field
    force : Iterating C X i
open IterIx public

data Iterating {i} C X i where
  ret : (X -:> Iterating C X) i
  do  : (IC C (IterIx C X) -:> Iterating C X) i

iterMonadIx : forall {I}(C : I => I) -> MonadIx (IterIx C)
iterMonadIx C = record { retIx = retHelp ; extendIx = extHelp } where
  open _=>_ C
  retHelp : forall {P} -> [ P -:> IterIx C P ]
  force (retHelp p) = ret p
  extHelp : forall {P Q} -> [ P -:> IterIx C Q ] -> [ IterIx C P -:> IterIx C Q ]
  force (extHelp k t) with force t
  force (extHelp k t) | ret p = force (k p)
  force (extHelp k t) | do (s , f)  = do (s , \ p -> extHelp k (f p))


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Reduction {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product

-- Weak head expansion of valid terms.
redSubstTermᵛ : ∀ {A t u l Γ}
              → ([Γ] : ⊩ᵛ Γ)
              → Γ ⊩ᵛ t ⇒ u ∷ A / [Γ]
              → ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
              → Γ ⊩ᵛ⟨ l ⟩ u ∷ A / [Γ] / [A]
              → (Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A])
              ×ω₃ (Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A])
redSubstTermᵛ [Γ] t⇒u [A] [u] =
  (λ ⊢Δ [σ] →
     let [σA] = proj₁ ([A] ⊢Δ [σ])
         [σt] , [σt≡σu] = redSubstTerm (t⇒u ⊢Δ [σ])
                                       (proj₁ ([A] ⊢Δ [σ]))
                                       (proj₁ ([u] ⊢Δ [σ]))
     in  [σt]
     ,   (λ [σ′] [σ≡σ′] →
            let [σ′A] = proj₁ ([A] ⊢Δ [σ′])
                [σA≡σ′A] = proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]
                [σ′t] , [σ′t≡σ′u] = redSubstTerm (t⇒u ⊢Δ [σ′])
                                                 (proj₁ ([A] ⊢Δ [σ′]))
                                                 (proj₁ ([u] ⊢Δ [σ′]))
            in  transEqTerm [σA] [σt≡σu]
                            (transEqTerm [σA] ((proj₂ ([u] ⊢Δ [σ])) [σ′] [σ≡σ′])
                                         (convEqTerm₂ [σA] [σ′A] [σA≡σ′A]
                                                      (symEqTerm [σ′A] [σ′t≡σ′u])))))
  , (λ ⊢Δ [σ] → proj₂ (redSubstTerm (t⇒u ⊢Δ [σ])
                                    (proj₁ ([A] ⊢Δ [σ]))
                                    (proj₁ ([u] ⊢Δ [σ]))))

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 --without-K --rewriting #-}

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
import homotopy.WedgeExtension as WedgeExt

module homotopy.Pi2HSusp {i} {X : Ptd i} {{_ : has-level 1 (de⊙ X)}}
  {{_ : is-connected 0 (de⊙ X)}} (H-X : HSS X)
  where

  {- TODO this belongs somewhere else, but where? -}
  private
    Type=-ext : ∀ {i} {A B : Type i} (p q : A == B)
      → (coe p ∼ coe q) → p == q
    Type=-ext p q α =
      ! (ua-η p)
      ∙ ap ua (Subtype=-out is-equiv-prop (λ= α))
      ∙ ua-η q

  module μ = ConnectedHSpace H-X
  μ = μ.μ
  private
    A = de⊙ X
    e = pt X

  P : Susp A → Type i
  P x = Trunc 1 (north == x)

  module Codes = SuspRec A A (λ a → ua (μ.r-equiv a))

  Codes : Susp A → Type i
  Codes = Codes.f

  Codes-level : (x : Susp A) → has-level 1 (Codes x)
  Codes-level = Susp-elim ⟨⟩ ⟨⟩
    (λ _ → prop-has-all-paths-↓)

  encode'₀ : {x : Susp A} → (north == x) → Codes x
  encode'₀ α = transport Codes α e

  encode' : {x : Susp A} → P x → Codes x
  encode' {x} = Trunc-rec {{Codes-level x}} encode'₀

  import homotopy.SuspAdjointLoop as SAL
  {- This should be [[_] ∘ η] where [η] is the functor in SuspAdjointLoop.agda -}
  decodeN' : A → P north
  decodeN' = [_] ∘ fst (SAL.η X)

  abstract
    transport-Codes-mer : (a a' : A)
      → transport Codes (merid a) a' == μ a a'
    transport-Codes-mer a a' =
      coe (ap Codes (merid a)) a'
        =⟨ Codes.merid-β a |in-ctx (λ w → coe w a') ⟩
      coe (ua (μ.r-equiv a)) a'
        =⟨ coe-β (μ.r-equiv a) a' ⟩
      μ a a' ∎

    transport-Codes-mer-e-! : (a : A)
      → transport Codes (! (merid e)) a == a
    transport-Codes-mer-e-! a =
      coe (ap Codes (! (merid e))) a
        =⟨ ap-! Codes (merid e) |in-ctx (λ w → coe w a) ⟩
      coe (! (ap Codes (merid e))) a
        =⟨ Codes.merid-β e |in-ctx (λ w → coe (! w) a) ⟩
      coe (! (ua (μ.r-equiv e))) a
        =⟨ Type=-ext (ua (μ.r-equiv e)) idp (λ x → coe-β _ x ∙ μ.unit-l x)
          |in-ctx (λ w → coe (! w) a) ⟩
      coe (! idp) a ∎

  abstract
    encode'-decodeN' : (a : A) → encode' (decodeN' a) == a
    encode'-decodeN' a =
      transport Codes (merid a ∙ ! (merid e)) e
        =⟨ transp-∙ {B = Codes} (merid a) (! (merid e)) e ⟩
      transport Codes (! (merid e)) (transport Codes (merid a) e)
        =⟨ transport-Codes-mer a e ∙ μ.unit-r a
          |in-ctx (λ w → transport Codes (! (merid e)) w) ⟩
      transport Codes (! (merid e)) a
        =⟨ transport-Codes-mer-e-! a ⟩
      a ∎

  abstract
    homomorphism : (a a' : A)
      → Path {A = Trunc 1 (north == south)}
        [ merid (μ a a' ) ] [ merid a' ∙ ! (merid e) ∙ merid a ]
    homomorphism = WedgeExt.ext args
      where
      args : WedgeExt.args {a₀ = e} {b₀ = e}
      args = record {m = -1; n = -1;
        P = λ a a' → (_ , ⟨⟩);
        f = λ a →  ap [_] $
              merid (μ a e)
                =⟨ ap merid (μ.unit-r a) ⟩
              merid a
                =⟨ ap (λ w → w ∙ merid a) (! (!-inv-r (merid e)))
                   ∙ ∙-assoc (merid e) (! (merid e)) (merid a)  ⟩
              merid e ∙ ! (merid e) ∙ merid a ∎;
        g = λ a' → ap [_] $
              merid (μ e a')
                =⟨ ap merid (μ.unit-l a') ⟩
              merid a'
                =⟨ ! (∙-unit-r (merid a'))
                   ∙ ap (λ w → merid a' ∙ w) (! (!-inv-l (merid e))) ⟩
              merid a' ∙ ! (merid e) ∙ merid e ∎ ;
        p = ap (λ {(p₁ , p₂) → ap [_] $
              merid (μ e e) =⟨ p₁ ⟩
              merid e       =⟨ p₂ ⟩
              merid e ∙ ! (merid e) ∙ merid e ∎})
             (pair×= (ap (λ x → ap merid x) (! μ.coh)) (coh (merid e)))}
        where coh : {B : Type i} {b b' : B} (p : b == b')
                → ap (λ w → w ∙ p) (! (!-inv-r p)) ∙ ∙-assoc p (! p) p
                  == ! (∙-unit-r p) ∙ ap (λ w → p ∙ w) (! (!-inv-l p))
              coh idp = idp

  decode' : {x : Susp A} → Codes x → P x
  decode' {x} = Susp-elim {P = λ x → Codes x → P x}
                 decodeN'
                 (λ a → [ merid a ])
                 (λ a → ↓-→-from-transp (λ= $ STS a))
                 x
    where
    abstract
      STS : (a a' : A) → transport P (merid a) (decodeN' a')
                         == [ merid (transport Codes (merid a) a') ]
      STS a a' =
        transport P (merid a) [ merid a' ∙ ! (merid e) ]
          =⟨ transport-Trunc (north ==_) (merid a) _ ⟩
        [ transport (north ==_) (merid a) (merid a' ∙ ! (merid e)) ]
          =⟨ ap [_] (transp-cst=idf {A = Susp A} (merid a) _) ⟩
        [ (merid a' ∙ ! (merid e)) ∙ merid a ]
          =⟨ ap [_] (∙-assoc (merid a') (! (merid e)) (merid a)) ⟩
        [ merid a' ∙ ! (merid e) ∙ merid a ]
          =⟨ ! (homomorphism a a') ⟩
        [ merid (μ a a') ]
          =⟨ ap ([_] ∘ merid) (! (transport-Codes-mer a a')) ⟩
        [ merid (transport Codes (merid a) a') ] ∎

  abstract
    decode'-encode' : {x : Susp A} (tα : P x)
      → decode' {x} (encode' {x} tα) == tα
    decode'-encode' {x} = Trunc-elim
      {P = λ tα → decode' {x} (encode' {x} tα) == tα}
      -- FIXME: Agda very slow (looping?) when omitting the next line
      {{λ _ → =-preserves-level Trunc-level}}
      (J (λ y p → decode' {y} (encode' {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid e))))

  eq' : Trunc 1 (Ω (⊙Susp X)) ≃ A
  eq' = equiv encode' decodeN' encode'-decodeN' decode'-encode'

  ⊙decodeN : ⊙Trunc 1 X ⊙→ ⊙Trunc 1 (⊙Ω (⊙Susp X))
  ⊙decodeN = ⊙Trunc-fmap (SAL.η X)

  decodeN : Trunc 1 A → Trunc 1 (Ω (⊙Susp X))
  decodeN = fst ⊙decodeN

  encodeN : Trunc 1 (Ω (⊙Susp X)) → Trunc 1 A
  encodeN = [_] ∘ encode' {x = north}

  eq : Trunc 1 (Ω (⊙Susp X)) ≃ Trunc 1 A
  eq = encodeN ,
    replace-inverse (snd ((unTrunc-equiv A)⁻¹ ∘e eq'))
      {decodeN}
      (Trunc-elim (λ _ → idp))

  ⊙eq : ⊙Trunc 1 (⊙Ω (⊙Susp X)) ⊙≃ ⊙Trunc 1 X
  ⊙eq = ≃-to-⊙≃ eq idp

  ⊙eq⁻¹ : ⊙Trunc 1 X ⊙≃ ⊙Trunc 1 (⊙Ω (⊙Susp X))
  ⊙eq⁻¹ = ⊙decodeN , snd (eq ⁻¹)

  iso : Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp X)))
      ≃ᴳ Ω^S-group 0 (⊙Trunc 1 X)
  iso = Ω^S-group-emap 0 ⊙eq

  abstract
    π₂-Susp : πS 1 (⊙Susp X) ≃ᴳ πS 0 X
    π₂-Susp =
      πS 1 (⊙Susp X)
        ≃ᴳ⟨ πS-Ω-split-iso 0 (⊙Susp X) ⟩
      πS 0 (⊙Ω (⊙Susp X))
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 (⊙Ω (⊙Susp X)) ⁻¹ᴳ ⟩
      Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp X)))
        ≃ᴳ⟨ iso ⟩
      Ω^S-group 0 (⊙Trunc 1 X)
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 X ⟩
      πS 0 X ≃ᴳ∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Categories.Category
open import Categories.Object.Terminal

-- Various constructors of Product Objects

module Categories.Object.Product.Construction {o ℓ e} (C : Category o ℓ e) (T : Terminal C) where

open import Categories.Object.Exponential C hiding (repack)
open import Categories.Object.Product C
open Category C
open Terminal T
open HomReasoning

-- we can get some products
[⊤×⊤]-product : Product ⊤ ⊤
[⊤×⊤]-product = record
  { A×B       = ⊤
  ; π₁        = !
  ; π₂        = !
  ; ⟨_,_⟩     = λ _ _ → !
  ; project₁  = !-unique₂
  ; project₂  = !-unique₂
  ; unique = λ _ _ → !-unique _
  }

[⊤×_]-product : (X : Obj) → Product ⊤ X
[⊤×_]-product X = record
  { A×B = X
  ; π₁ = !
  ; π₂ = id
  ; ⟨_,_⟩ = λ _ y → y
  ; project₁ = !-unique₂
  ; project₂ = identityˡ
  ; unique = λ _ id∘h≈j → ⟺ id∘h≈j ○ identityˡ
  }

[_×⊤]-product : (X : Obj) → Product X ⊤
[_×⊤]-product X = Reversible [⊤× X ]-product

-- and some exponentials too
[_↑⊤]-exponential : (B : Obj) → Exponential ⊤ B
[ B ↑⊤]-exponential = record
  { B^A = B
  ; product = [ B ×⊤]-product
  ; eval = id
  ; λg = λ {X} X×⊤ X⇒B → X⇒B ∘ repack [ X ×⊤]-product X×⊤
  ; β = λ p {g} → begin
    id ∘ (g ∘ [ p ]⟨ id , ! ⟩) ∘ [ p ]π₁    ≈⟨ identityˡ ○ assoc ⟩
    g ∘ [ p ]⟨ id , ! ⟩ ∘ [ p ]π₁           ≈⟨ refl⟩∘⟨ [ p ]⟨⟩∘ ⟩
    g ∘ [ p ]⟨ id ∘ [ p ]π₁ , ! ∘ [ p ]π₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ p identityˡ !-unique₂ ⟩
    g ∘ [ p ]⟨ [ p ]π₁ , [ p ]π₂ ⟩          ≈⟨ refl⟩∘⟨ η p ○ identityʳ ⟩
    g                                      ∎
  ; λ-unique = λ {X} p {g} {h} h-comm → begin
    h                                   ≈˘⟨ identityʳ ⟩
    h ∘ id                              ≈˘⟨  refl⟩∘⟨ project₁ p ⟩
    h ∘ [ p ]π₁ ∘ [ p ]⟨ id , ! ⟩        ≈˘⟨ assoc ⟩
    (h ∘ [ p ]π₁) ∘ [ p ]⟨ id , ! ⟩      ≈˘⟨ identityˡ ⟩∘⟨refl ⟩
    (id ∘ h ∘ [ p ]π₁) ∘ [ p ]⟨ id , ! ⟩ ≈⟨ h-comm ⟩∘⟨refl ⟩
    g ∘ repack [ X ×⊤]-product p ∎
  }
  where open Product

[⊤↑_]-exponential : (A : Obj) → Exponential A ⊤
[⊤↑ A ]-exponential = record
  { B^A       = ⊤
  ; product   = [⊤× A ]-product
  ; eval      = !
  ; λg        = λ _ _ → !
  ; β         = λ _   → !-unique₂
  ; λ-unique  = λ _ _ → !-unique₂
  }

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Group where

open import Cubical.Structures.Group.Base public
open import Cubical.Structures.Group.Properties public
open import Cubical.Structures.Group.Morphism public
open import Cubical.Structures.Group.MorphismProperties public

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Haskell.Prim.Applicative where

open import Haskell.Prim
open import Haskell.Prim.Either
open import Haskell.Prim.Foldable
open import Haskell.Prim.Functor
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Monoid
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Applicative

record Applicative (f : Set → Set) : Set₁ where
  infixl 4 _<*>_
  field
    pure  : a → f a
    _<*>_ : f (a → b) → f a → f b
    overlap ⦃ super ⦄ : Functor f

  _<*_ : f a → f b → f a
  x <* y = const <$> x <*> y

  _*>_ : f a → f b → f b
  x *> y = const id <$> x <*> y

open Applicative ⦃ ... ⦄ public

instance
  iApplicativeList : Applicative List
  iApplicativeList .pure x      = x ∷ []
  iApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs

  iApplicativeMaybe : Applicative Maybe
  iApplicativeMaybe .pure = Just
  iApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
  iApplicativeMaybe ._<*>_ _        _        = Nothing

  iApplicativeEither : Applicative (Either a)
  iApplicativeEither .pure = Right
  iApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
  iApplicativeEither ._<*>_ (Left e)  _         = Left e
  iApplicativeEither ._<*>_ _         (Left e)  = Left e

  iApplicativeFun : Applicative (λ b → a → b)
  iApplicativeFun .pure        = const
  iApplicativeFun ._<*>_ f g x = f x (g x)

  iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
  iApplicativeTuple₂ .pure x                = mempty , x
  iApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x

  iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
  iApplicativeTuple₃ .pure x                          = mempty , mempty , x
  iApplicativeTuple₃ ._<*>_ (a , b , f) (a₁ , b₁ , x) = a <> a₁ , b <> b₁ , f x

  iApplicativeTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
                       Applicative (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
  iApplicativeTuple₄ .pure x                          = mempty ∷ mempty ∷ mempty ∷ x ∷ []
  iApplicativeTuple₄ ._<*>_ (a ∷ b ∷ c ∷ f ∷ []) (a₁ ∷ b₁ ∷ c₁ ∷ x ∷ []) =
    a <> a₁ ∷ b <> b₁ ∷ c <> c₁ ∷ f x ∷ []


text:
module Data.FixedTree.Properties where

import      Lvl
open import Data using (Unit ; <>)
open import Data.Boolean
open import Data.FixedTree
open import Data.Tuple.Raise
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Functional as Fn
open import Logic.Propositional
open import Numeral.Finite
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Natural
open import Type

private variable ℓ ℓᵢ ℓₗ ℓₙ ℓₒ : Lvl.Level
private variable n : ℕ
private variable N N₁ N₂ L T A B : Type{ℓ}

-- A tree is full when every node has no or all children.
data Full {L : Type{ℓₗ}}{N : Type{ℓₙ}}{n} : FixedTree(n) L N → Type{ℓₗ Lvl.⊔ ℓₙ} where
  leaf   : ∀{l} → Full(Leaf l)
  single : ∀{a}{l} → Full(Node a (Raise.repeat(n) (Leaf l))) -- TODO: All the leaves should not be forced to all have the same data
  step   : ∀{a : N}{ca : N ^ n}{cc : ((FixedTree(n) L N) ^ n) ^ n} → (∀{i : 𝕟(n)} → Full(Node (Raise.index i ca) (Raise.index i cc))) → Full(Node a (Raise.map₂{n} Node ca cc))
  -- step  : ∀{a : T}{ca : T ^ n}{cc : (FixedTree(n)(T) ^ n) ^ n} → Raise.reduceOrᵣ{n}(_⨯_) Unit (Raise.map₂(Full ∘₂ Node) ca cc) → Full(Node a (Raise.map₂{n} Node ca cc))

-- A tree is perfect at depth `n` when all leaves are at height `n`.
-- In other words, a tree is perfect when all leaves are at the same height.
data Perfect {L : Type{ℓₗ}}{N : Type{ℓₙ}}{n} : FixedTree(n) L N → ℕ → Type{ℓₗ Lvl.⊔ ℓₙ} where
  leaf : ∀{l} → Perfect(Leaf l)(𝟎)
  step : ∀{a}{c}{h} → (∀{i : 𝕟(n)} → Perfect(Raise.index i c)(h)) → Perfect(Node a c)(𝐒(h))

data Complete {L : Type{ℓₗ}}{N : Type{ℓₙ}}{n} : FixedTree(n) L N → ℕ → Bool → Type{ℓₗ Lvl.⊔ ℓₙ} where
  perfect-leaf : ∀{l} → Complete(Leaf l)(𝟎)(𝑇)
  imperfect-leaf : ∀{l} → Complete(Leaf l)(𝐒(𝟎))(𝐹)
  step : ∀{a}{c}{h}{t : 𝕟(n)} → (∀{i : 𝕟(n)} → Complete(Raise.index i c)(h)(i ≤? t)) → Complete(Node a c)(𝐒(h))(t ≤? maximum{n})

data DepthOrdered {L : Type{ℓₗ}}{N : Type{ℓₙ}} (_≤_ : N → N → Type{ℓₒ}) {n} : FixedTree(n) L N → Type{ℓₗ Lvl.⊔ ℓₙ Lvl.⊔ ℓₒ} where
  leaf : ∀{l} → DepthOrdered(_≤_)(Leaf l)
  step : ∀{p}{c : (FixedTree(n) L N) ^ n} → (∀{i : 𝕟(n)} → (\{(Leaf _) → Unit ; (Node a c) → (p ≤ a) ∧ DepthOrdered(_≤_)(Node a c)}) $ (Raise.index i c)) → DepthOrdered(_≤_)(Node p c)

Heap : ∀{L : Type{ℓₗ}}{N : Type{ℓₙ}} → (N → N → Type{ℓₒ}) → ∀{n} → FixedTree(n) L N → ℕ → Bool → Type
Heap(_≤_) tree height perfect = DepthOrdered(_≤_)(tree) ∧ Complete(tree)(height)(perfect)

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:
{-# OPTIONS --without-K #-}

open import Types
open import Functions
open import Paths
open import HLevel
open import Equivalences

module Univalence {i} where

postulate  -- Univalence axiom
  univalence : (A B : Set i) → is-equiv (path-to-eq {i} {A} {B})

path-to-eq-equiv : {A B : Set i} → ((A ≡ B) ≃ (A ≃ B))
path-to-eq-equiv = (path-to-eq , univalence _ _)

eq-to-path-equiv : {A B : Set i} → ((A ≃ B) ≃ (A ≡ B))
eq-to-path-equiv = path-to-eq-equiv ⁻¹

eq-to-path : {A B : Set i} → (A ≃ B → A ≡ B)
eq-to-path {A} {B} = π₁ eq-to-path-equiv

eq-to-path-right-inverse : {A B : Set i} (f : A ≃ B)
  → path-to-eq (eq-to-path f) ≡ f
eq-to-path-right-inverse = inverse-right-inverse path-to-eq-equiv

path-to-eq-right-inverse : {A B : Set i} (f : A ≡ B)
  → eq-to-path (path-to-eq f) ≡ f
path-to-eq-right-inverse = inverse-left-inverse path-to-eq-equiv

-- Transport in the structural fibration of a universe

trans-id : {A B : Set i} (f : A ≡ B) (u : A)
  → transport (λ X → X) f u ≡ (path-to-eq f) ☆ u
trans-id refl u = refl

trans-id! : {A B : Set i} (f : A ≡ B) (u : B)
  → transport (λ X → X) (! f) u ≡ inverse (path-to-eq f) u
trans-id! refl u = refl

trans-id-eq-to-path : {A B : Set i} (f : A ≃ B) (u : A)
  → transport (λ X → X) (eq-to-path f) u ≡ f ☆ u
trans-id-eq-to-path {A} {B} f u =
  trans-id (eq-to-path f) u
  ∘ ap (λ (t : A ≃ B) → t ☆ u) (eq-to-path-right-inverse f)

trans-id-!eq-to-path : {A B : Set i} (f : A ≃ B) (u : B)
  → transport (λ X → X) (! (eq-to-path f)) u ≡ inverse f u
trans-id-!eq-to-path {A} {B} f u =
  trans-id! (eq-to-path f) u
  ∘ ap (λ (t : A ≃ B) → inverse t u) (eq-to-path-right-inverse f)

-- Not used
--
-- trans-id→A : ∀ {i j} (A : Set j) {X Y : Set i} (e : X ≡ Y) (f : X → A)
--   (a : Y) → transport (λ (X : Set i) → X → A) e f a
--     ≡ f (inverse (path-to-eq e) a)
-- trans-id→A A (refl _) f a = refl _

-- trans-id→A-eq-to-path : ∀ {i j} (A : Set j) {X Y : Set i} (e : X ≃ Y)
--   (f : X → A) (a : Y)
--   → transport (λ (X : Set i) → X → A) (eq-to-path e) f a ≡ f (inverse e a)
-- trans-id→A-eq-to-path A e f a =
--   trans-id→A A (eq-to-path e) f a
--   ∘ ap (λ u → f (inverse u a)) (eq-to-path-right-inverse e)

-- trans-cst→X : ∀ {i j} (A : Set j) {X Y : Set i} (e : X ≡ Y) (f : A → X)
--   (a : A) → transport (λ (X : Set i) → A → X) e f a
--     ≡ π₁ (path-to-eq e) (f a)
-- trans-cst→X A (refl _) f a = refl _

-- trans-cst→X-eq-to-path : ∀ {i j} (A : Set j) {X Y : Set i} (e : X ≃ Y)
--   (f : A → X) (a : A)
--   → transport (λ (X : Set i) → A → X) (eq-to-path e) f a ≡ π₁ e (f a)
-- trans-cst→X-eq-to-path A e f a =
--   trans-cst→X A (eq-to-path e) f a
--   ∘ ap (λ u → π₁ u (f a)) (eq-to-path-right-inverse e)

-- Induction along equivalences

equiv-induction : ∀ {j} (P : {A B : Set i} (f : A ≃ B) → Set j)
  (d : (A : Set i) → P (id-equiv A)) {A B : Set i} (f : A ≃ B)
  → P f
equiv-induction P d f =
  transport P (eq-to-path-right-inverse f)
    (equiv-induction-int P d (eq-to-path f)) where

  equiv-induction-int : ∀ {j}
    (P : {A : Set i} {B : Set i} (f : A ≃ B) → Set j)
    (d : (A : Set i) → P (id-equiv A)) {A B : Set i} (p : A ≡ B)
    → P (path-to-eq p)
  equiv-induction-int P d refl = d _

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Fragment.Tactic.Utils where

open import Reflection hiding (name; Type; _≟_)
open import Reflection.Term using (_≟_)

open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Data.Nat.Show using (show)
open import Data.String using (String) renaming (_++_ to _⟨S⟩_)
open import Data.List using (List; []; _∷_; _++_; drop; take; reverse)
open import Data.Vec using (Vec; []; _∷_; map; toList)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Product using (_×_; _,_)

open import Relation.Nullary using (yes; no; _because_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

vra : ∀ {a} {A : Set a} → A → Arg A
vra = arg (arg-info visible relevant)

hra : ∀ {a} {A : Set a} → A → Arg A
hra = arg (arg-info hidden relevant)

infixr 5 λ⦅_⦆→_ λ⦃_⦄→_

λ⦅_⦆→_ : String → Term → Term
λ⦅ x ⦆→ body = lam visible (abs x body)

λ⦃_⦄→_ : String → Term → Term
λ⦃ x ⦄→ body = lam hidden (abs x body)

constructors : Definition → List Name
constructors (data-type _ cs) = cs
constructors _                = []

apply : Term → List (Arg Term) → Term
apply (var x xs) args      = var x (xs ++ args)
apply (con x xs) args      = con x (xs ++ args)
apply (def x xs) args      = def x (xs ++ args)
apply (meta x xs) args     = meta x (xs ++ args)
apply (pat-lam cs xs) args = pat-lam cs (xs ++ args)
apply x _                  = x

prod : ∀ {a} {A : Set a} → ℕ → List A → List A
prod n xs = reverse (drop n (reverse xs))

ekat : ∀ {a} {A : Set a} → ℕ → List A → List A
ekat n xs = reverse (take n (reverse xs))

find : ∀ {a} {A : Set a} → (A → TC Bool) → List A → TC (Maybe A)
find p [] = return nothing
find p (x ∷ xs)
  = do p? ← p x
       if p? then return (just x)
             else find p xs

mapList : ∀ {a b} {A : Set a} {B : Set b}
          → List (A → B) → List A → List B
mapList [] _              = []
mapList _ []              = []
mapList (f ∷ fs) (x ∷ xs) = f x ∷ mapList fs xs

unapply : Term → ℕ → Term
unapply (var x args) n      = var x (prod n args)
unapply (con x args) n      = con x (prod n args)
unapply (def x args) n      = def x (prod n args)
unapply (meta x args) n     = meta x (prod n args)
unapply (pat-lam cs args) n = pat-lam cs (prod n args)
unapply x _                 = x

equalTypes : Term → Term → Bool
equalTypes τ τ' with τ ≟ τ'
...                | yes _ = true
...                | _     = false

flatten : ∀ {a} {A : Set a} → TC (TC A) → TC A
flatten x
  = do x' ← x
       x'

listTC : ∀ {a} {A : Set a} → List (TC A) → TC (List A)
listTC []       = return []
listTC (x ∷ xs)
  = do x' ← x
       xs' ← listTC xs
       return (x' ∷ xs')

n-ary : ∀ (n : ℕ) → Term → Term
n-ary zero body    = body
n-ary (suc n) body = λ⦅ "x" ⟨S⟩ show n ⦆→ (n-ary n body)

debrujin : ∀ (n : ℕ) → Vec Term n
debrujin zero    = []
debrujin (suc n) = (var n []) ∷ debrujin n

η-convert : ∀ (n : ℕ) → Term → TC Term
η-convert n t = runSpeculative inner
  where inner : TC (Term × Bool)
        inner
          = do t ← normalise (n-ary n (apply t (toList (map vra (debrujin n)))))
               return (t , false)

prefix : ℕ → Term → Term → TC Bool
prefix n x y
  = do y ← catchTC (η-convert n (unapply y n)) (return y)
       let (b because _) = x ≟ y
       return b

extract-type-arg : Term → TC Term
extract-type-arg (pi (arg _ x) _) = return x
extract-type-arg x                = typeError (termErr x ∷ strErr "isn't a pi type" ∷ [])

extract-name : Term → TC Name
extract-name (def x _) = return x
extract-name x         = typeError (termErr x ∷ strErr "isn't an application of a definition" ∷ [])

extract-definition : Term → TC Definition
extract-definition x
  = do x' ← normalise x
       η ← extract-name x'
       getDefinition η

extract-constructors : Term → TC (List Name)
extract-constructors x
  = do δ ← extract-definition x
       return (constructors δ)

fin : ℕ → Term
fin zero    = con (quote Fin.zero) []
fin (suc n) = con (quote Fin.suc) (vra (fin n) ∷ [])

vec : ∀ {n : ℕ} → Vec Term n → Term
vec []       = con (quote Vec.[]) []
vec (x ∷ xs) = con (quote Vec._∷_) (vra x ∷ vra (vec xs) ∷ [])

vec-len : Term → TC ℕ
vec-len (def (quote Vec) (_ ∷ _ ∷ (arg _ n) ∷ [])) = unquoteTC n
vec-len t = typeError (termErr t ∷ strErr "isn't a" ∷ nameErr (quote Vec) ∷ [])

panic : ∀ {a} {A : Set a} → Term → TC A
panic x = typeError (termErr x ∷ [])

strip-telescope : Term → TC (Term × List (Arg String))
strip-telescope (pi (vArg _) (abs s x))
  = do (τ , acc) ← strip-telescope x
       return (τ , vra s ∷ acc)
strip-telescope (pi (hArg _) (abs s x))
  = do (τ , acc) ← strip-telescope x
       return (τ , hra s ∷ acc)
strip-telescope (pi _ _) =
  typeError (strErr "no support for irrelevant goals" ∷ [])
strip-telescope t        = return (t , [])

restore-telescope : List (Arg String) → Term → TC Term
restore-telescope [] t = return t
restore-telescope (vArg x ∷ xs) t
  = do t ← restore-telescope xs t
       return (λ⦅ x ⦆→ t)
restore-telescope (hArg x ∷ xs) t
  = do t ← restore-telescope xs t
       return (λ⦃ x ⦄→ t)
restore-telescope (_ ∷ _) _ =
  typeError (strErr "no support for irrelevant goals" ∷ [])

hasType : Term → Term → TC Bool
hasType τ t = runSpeculative inner
  where inner = do τ' ← inferType t
                   return (equalTypes τ τ' , false)

insert : List Term → Term → List Term
insert [] n       = n ∷ []
insert (x ∷ xs) n with x ≟ n
...                  | yes _ = x ∷ xs
...                  | no _  = x ∷ insert xs n

indexOf : List Term → Term → Maybe ℕ
indexOf [] t = nothing
indexOf (x ∷ xs) t with x ≟ t | indexOf xs t
...                   | yes _ | _       = just 0
...                   | no _  | just n  = just (suc n)
...                   | no _  | nothing = nothing

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

   Copyright (c) 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 Util.Prelude

-- This module defines types used in the specification of a SystemModel.
module Yasm.Types where

-- Actions that can be performed by peers.
--
-- For now, the SystemModel supports only one kind of action: to send a
-- message. Later it might include things like logging, crashes, assertion
-- failures, etc. For example, if an assertion fires, this
-- could "kill the process" and make it not send any messages in the future.
-- We could also then prove that the handlers do not crash, certain
-- messages are logged under certain circumstances, etc.
--
-- Alternatively, certain actions can be kept outside the system model by
-- defining an application-specific PeerState type (see `Yasm.Base`).
-- For example:
--
-- > libraHandle : Msg → Status × Log × LState → Status × LState × List Action
-- > libraHandle _ (Crashed , l , s) = Crashed , s , [] -- i.e., crashed peers never send messages
-- >
-- > handle = filter isSend ∘ libraHandle
data Action (Msg : Set) : Set where
  send : (m : Msg) → Action Msg

-- Injectivity of `send`.
action-send-injective : ∀ {Msg}{m m' : Msg} → send m ≡ send m' → m ≡ m'
action-send-injective refl = refl