text:
open import Base
open import Homotopy.Connected

module Homotopy.Extensions.ProductPushoutToProductToConnected.Magic
  {i j} {D E : Set i} (h : E → D) where

  {-
         k
      E ---> F x
      |    /^
      | ≃ /
      |  / l?
      v /
    (x : D)
  -}

  -- The mapping l and the coherence data.
  extension : (F : D → Set j) (k : ∀ x → F (h x)) → Set (max i j)
  extension F k = Σ (Π D F) (λ l → ∀ x → k x ≡ l (h x))

  -- Specialized J rules.
  private
    -- This is a combination of 2~3 basic rules.
    lemma₁ : ∀ (F : D → Set j) (k : ∀ x → F (h x))
      {l₁ l₂ : ∀ x → F x} (p : l₁ ≡ l₂) (q : ∀ x → k x ≡ l₁ (h x)) a
      → transport (λ l → ∀ x → k x ≡ l (h x)) p q a
      ≡ q a ∘ happly p (h a)
    lemma₁ F k refl q a = ! $ refl-right-unit _

    -- May be generalized later.
    lemma₂ : ∀ {i} {X : Set i} {x₁ x₂ x₃ : X}
      (p₁ : x₁ ≡ x₂) (p₂ : x₂ ≡ x₃) (p₃ : x₁ ≡ x₃)
      → (p₁ ∘ p₂ ≡ p₃) ≡ (p₂ ≡ ! p₁ ∘ p₃)
    lemma₂ refl _ _ = refl

    -- May be generalized later.
    lemma₃ : ∀ {i} {X : Set i} {x₁ x₂ : X}
      (p₁ : x₁ ≡ x₂) (p₂ : x₁ ≡ x₂)
      → (p₁ ≡ p₂) ≡ (p₂ ≡ p₁)
    lemma₃ p₁ p₂ = eq-to-path $ ! , iso-is-eq ! ! opposite-opposite opposite-opposite

    lemma₄ : ∀ {i j} {A A′ : Set i} (B′ : A′ → Set j) (eq : A ≃ A′)
      → Σ A (λ x → (B′ (eq ☆ x))) ≡ Σ A′ B′
    lemma₄ {j = j} B′ eq = equiv-induction
      (λ {A A′} eq → ∀ (B′ : A′ → Set j) → Σ A (λ x → (B′ (eq ☆ x))) ≡ Σ A′ B′)
      (λ A _ → refl)
      eq B′

  -- The main lemma
  module _ {n₁ : ℕ₋₂} (h-is-conn : has-connected-fibers n₁ h) where
    open import Homotopy.Truncation

    extension-is-truncated :
      (F : D → Set j)
      {n₂ : ℕ₋₂} ⦃ F-is-trunc : ∀ x → is-truncated (n₂ +2+ n₁) (F x) ⦄
      (k : ∀ x → F (h x))
      → is-truncated n₂ (extension F k)
    extension-is-truncated F {⟨-2⟩} ⦃ F-is-trunc ⦄ k =
      center , (λ e″ → Σ-eq (path-l e″) (path-coh e″))
        where
          -- The section
          l′ : ∀ x → τ n₁ (hfiber h x) → F x
          l′ x = τ-extend-nondep ⦃ F-is-trunc x ⦄
            λ{(preimage , shift) → transport F shift (k preimage)}

          -- The section
          l : ∀ x → F x
          l x = l′ x (π₁ (h-is-conn x))

          -- The coherence data (commutivity)
          abstract
            coh : ∀ x → k x ≡ l (h x)
            coh x = ap (l′ (h x)) $ π₂ (h-is-conn (h x)) $ proj (x , refl)

          -- The canonical choice of section+coherence
          center : extension F k
          center = l , coh

          -- The path between the canonical choice and others (pointwise).
          abstract
            path-l-pointwise′ : ∀ (e : extension F k) x → τ n₁ (hfiber h x) → π₁ e x ≡ l x
            path-l-pointwise′ = λ{(l″ , coh″) x →
              τ-extend-nondep
              ⦃ ≡-is-truncated n₁ $ F-is-trunc x ⦄
              -- The point is to make all artifacts go away when shift = refl _.
              (λ{(pre , shift) → transport (λ x → l″ x ≡ l x) shift $
                l″ (h pre)
                  ≡⟨ ! $ coh″ pre ⟩
                k pre
                  ≡⟨ coh pre ⟩∎
                l (h pre)
                  ∎})}

          -- The path between the canonical choice and others (pointwise).
          abstract
            path-l-pointwise : ∀ (e : extension F k) x → π₁ e x ≡ l x
            path-l-pointwise = λ e x →
              path-l-pointwise′ e x (π₁ (h-is-conn x))

          -- The path between the canonical choice and others.
          abstract
            path-l : ∀ (e : extension F k) → π₁ e ≡ l
            path-l = funext ◯ path-l-pointwise

          -- The path between the canonical choice and others.
          abstract
            path-coh : ∀ (e : extension F k)
              → transport (λ l → ∀ x → k x ≡ l (h x)) (path-l e) (π₂ e)
              ≡ coh
            path-coh e″ = funext λ x → let coh″ = π₂ e″ in
              transport (λ l → ∀ x → k x ≡ l (h x)) (path-l e″) coh″ x
                ≡⟨ lemma₁ F k (path-l e″) coh″ x ⟩
              coh″ x ∘ happly (path-l e″) (h x)
                ≡⟨ ap (λ p → coh″ x ∘ p (h x)) $ happly-funext (path-l-pointwise e″) ⟩
              coh″ x ∘ (path-l-pointwise′ e″ (h x) (π₁ (h-is-conn (h x))))
                ≡⟨ ap (λ y → π₂ e″ x ∘ (path-l-pointwise′ e″ (h x) y))
                      $ ! $ π₂ (h-is-conn (h x)) $ proj (x , refl) ⟩
              coh″ x ∘ (path-l-pointwise′ e″ (h x) (proj (x , refl)))
                ≡⟨ refl ⟩
              coh″ x ∘ ((! $ coh″ x) ∘ coh x)
                ≡⟨ ! $ concat-assoc (coh″ x) (! $ coh″ x) (coh x) ⟩
              (coh″ x ∘ (! $ coh″ x)) ∘ coh x
                ≡⟨ ap (λ p → p ∘ coh x) $ opposite-right-inverse (coh″ x) ⟩∎
              coh x
                ∎
    extension-is-truncated F {S n₂} ⦃ F-is-trunc ⦄ k = λ e₁ e₂ →
      transport (is-truncated n₂)
      (! $ extension≡-extension′-path e₁ e₂)
      (extension′-is-trunc e₁ e₂) where
        module _ (e₁ e₂ : extension F k) where
          l₁ = π₁ e₁
          l₂ = π₁ e₂
          coh₁ = π₂ e₁
          coh₂ = π₂ e₂

          -- The trick: Make a new F for the path space.
          F′ : ∀ D → Set j
          F′ x = l₁ x ≡ l₂ x

          k′ : ∀ x → F′ (h x)
          k′ x = ! (coh₁ x) ∘ coh₂ x

          F′-is-trunc : ∀ x → is-truncated (n₂ +2+ n₁) (F′ x)
          F′-is-trunc x = F-is-trunc x (l₁ x) (l₂ x)

          extension′ : Set (max i j)
          extension′ = extension F′ k′

          -- Conversion between paths and new extensions.
          abstract
            extension≡-extension′-path : (e₁ ≡ e₂) ≡ extension′
            extension≡-extension′-path =
              e₁ ≡ e₂
                ≡⟨ ! $ eq-to-path $ total-Σ-eq-equiv ⟩
              Σ (l₁ ≡ l₂) (λ l₁≡l₂ → transport (λ l → ∀ x → k x ≡ l (h x)) l₁≡l₂ coh₁ ≡ coh₂)
                ≡⟨ ap (Σ (l₁ ≡ l₂)) (funext λ _ → ! $ eq-to-path $ funext-equiv) ⟩
              Σ (l₁ ≡ l₂) (λ l₁≡l₂ → ∀ x → transport (λ l → ∀ x → k x ≡ l (h x)) l₁≡l₂ coh₁ x ≡ coh₂ x)
                ≡⟨ ap (Σ (l₁ ≡ l₂)) (funext λ l₁≡l₂ → ap (λ p → ∀ x → p x ≡ coh₂ x)
                      $ funext $ lemma₁ F k l₁≡l₂ coh₁) ⟩
              Σ (l₁ ≡ l₂) (λ l₁≡l₂ → ∀ x → coh₁ x ∘ happly l₁≡l₂ (h x) ≡ coh₂ x)
                ≡⟨ ap (Σ (l₁ ≡ l₂)) (funext λ l₁≡l₂ → ap (λ p → ∀ x → p x)
                      $ funext λ x → lemma₂ (coh₁ x) (happly l₁≡l₂ (h x)) (coh₂ x)) ⟩
              Σ (l₁ ≡ l₂) (λ l₁≡l₂ → ∀ x → happly l₁≡l₂ (h x) ≡ ! (coh₁ x) ∘ coh₂ x)
                ≡⟨ ap (Σ (l₁ ≡ l₂)) (funext λ l₁≡l₂ → ap (λ p → ∀ x → p x)
                      $ funext λ x → lemma₃ (happly l₁≡l₂ (h x)) (! (coh₁ x) ∘ coh₂ x)) ⟩
              Σ (l₁ ≡ l₂) (λ l₁≡l₂ → ∀ x → ! (coh₁ x) ∘ coh₂ x ≡ happly l₁≡l₂ (h x))
                ≡⟨ lemma₄ (λ l₁x≡l₂x → ∀ x → ! (coh₁ x) ∘ coh₂ x ≡ l₁x≡l₂x (h x)) happly-equiv ⟩∎
              extension′
                ∎

          -- Recursive calls.
          abstract
            extension′-is-trunc : is-truncated n₂ extension′
            extension′-is-trunc = extension-is-truncated F′ {n₂} ⦃ F′-is-trunc ⦄ k′

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path

open import Cubical.Foundations.SIP

private
  variable
    ℓ ℓ₁ : Level

-- Standard notion of structure from a "functorial" action
-- We don't need all the functor axioms, only F id ≡ id

FunctorialEquivStr : {S : Type ℓ → Type ℓ₁}
  → (∀ {X Y} → (X → Y) → S X → S Y)
  → StrEquiv S ℓ₁
FunctorialEquivStr F (X , s) (Y , t) e = F (e .fst) s ≡ t

functorialUnivalentStr : {S : Type ℓ → Type ℓ₁}
  (F : ∀ {X Y} → (X → Y) → S X → S Y)
  → (∀ {X} s → F (idfun X) s ≡ s)
  → UnivalentStr S (FunctorialEquivStr F)
functorialUnivalentStr F η =
  SNS→UnivalentStr
    (FunctorialEquivStr F)
    (λ s t → pathToEquiv (cong (_≡ t) (η s)))

ext: agda

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Numeral.Natural.Oper.Modulo where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Logic.Propositional.Theorems
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Relator.Equals

infixl 10100 _mod_

-- Modulo is defined using this.
-- This, unlike (_mod_) is keeping internal state of the previous value.
-- `r` is the current result. Should be 0 at the start.
-- `b` is the modulus. This value will not change in the repeated applications of the function.
-- `a'` is the number to take the modulo of.
-- 'b'` is the temporary modulus. Should be `b` at the start.
-- This function works by repeatedly decreasing `a'` and `b'` and at the same time increasing `r` until `b'` is 0.
-- When `b'` is 0, `r` is resetted to 0, and `b'` is resetted to `b`.
-- Almost the same algorithm imperatively:
--   while a'!=0{
--     a'-= 1;
--     b'-= 1;
--     r += 1;
--     if b'==0{
--       r := 0;
--       b':= b;
--     }
--   }
--   return r;
-- Example execution:
--   [ 0 , 2 ] 5 mod' 2
--   = [ 1 , 2 ] 4 mod' 1
--   = [ 2 , 2 ] 3 mod' 0
--   = [ 0 , 2 ] 3 mod' 2
--   = [ 1 , 2 ] 2 mod' 1
--   = [ 2 , 2 ] 1 mod' 0
--   = [ 0 , 2 ] 1 mod' 2
--   = [ 1 , 2 ] 0 mod' 1
--   = 1
-- The above is describing the following code:
--   {-# TERMINATING #-}
--   [_,_]_mod₀'_ : ℕ → ℕ → ℕ → ℕ → ℕ
--   [ _ , 𝟎 ] _     mod₀' _     = 𝟎
--   [ _ , b ] a'    mod₀' 𝟎     = [ 𝟎    , b ] a' mod₀' b
--   [ r , _ ] 𝟎     mod₀' _     = r
--   [ r , b ] 𝐒(a') mod₀' 𝐒(b') = [ 𝐒(r) , b ] a' mod₀' b'
-- Then it is transformed to the following code (So that it terminates):
--   [_,_]_mod₀'_ : ℕ → ℕ → ℕ → ℕ → ℕ
--   [ _ , 𝟎    ] _     mod₀' _     = 𝟎
--   [ _ , 𝐒(_) ] 𝟎     mod₀' 𝟎     = 𝟎
--   [ r , 𝐒(_) ] 𝟎     mod₀' 𝐒(_)  = r
--   [ _ , 𝐒(b) ] 𝐒(a') mod₀' 𝟎     = [ 𝐒(𝟎) , 𝐒(b) ] a' mod₀' b
--   [ r , 𝐒(b) ] 𝐒(a') mod₀' 𝐒(b') = [ 𝐒(r) , 𝐒(b) ] a' mod₀' b'
-- And finally removing the forbidden 𝟎 cases of `b` and `b'` by just interpreting (b=0), (b'=0) in this function as 1's:
--   [ r , _ ] 𝟎     mod' _     = r
--   [ _ , b ] 𝐒(a') mod' 𝟎     = [ 𝟎 , b ] a' mod' b
--   [ r , b ] 𝐒(a') mod' 𝐒(b') = [ 𝐒(r) , b ] a' mod' b'
-- Note: [ r , b ] a mod' b) is like ((a − r) mod b). The other b is actually a state for handling the situation when a is greater than the modulus b.
-- TODO: If it is possible together with the BUILTIN pragma, swap b and b' to avoid confusion. b' is actually a state (like r) and is not the actual base
[_,_]_mod'_ : ℕ → ℕ → ℕ → ℕ → ℕ
[ r , _ ] 𝟎     mod' _     = r
[ _ , b ] 𝐒(a') mod' 𝟎     = [ 𝟎    , b ] a' mod' b
[ r , b ] 𝐒(a') mod' 𝐒(b') = [ 𝐒(r) , b ] a' mod' b'
{-# BUILTIN NATMODSUCAUX [_,_]_mod'_ #-}

-- Difference between the value before and after the floored division operation.
_mod_ : ℕ → (m : ℕ) → .⦃ pos : IsTrue(positive?(m))⦄ → ℕ
a mod 𝐒(m) = [ 𝟎 , m ] a mod' m

_mod₀_ : ℕ → ℕ → ℕ
_ mod₀ 𝟎    = 𝟎
a mod₀ 𝐒(m) = [ 𝟎 , m ] a mod' m

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:
------------------------------------------------------------------------
-- A parametrised coinductive definition that can be used to define
-- various forms of similarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

open import Labelled-transition-system

module Similarity.General
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝_ : Proc → Label → Proc → Type ℓ)
         (⟶→↝ : ∀ {p μ q} → p [ μ ]⟶ q → p [ μ ]↝ q)
         where

open import Equality.Propositional as Eq hiding (Extensionality)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)

open import Indexed-container hiding (⟨_⟩)
open import Relation
open import Similarity.Step lts _[_]↝_ as Step public
  using (StepC)

open Indexed-container public using (force)
open StepC public using (⟨_⟩; challenge)

-- Similarity. Note that this definition is small.

infix 4 _≤_ _≤′_ [_]_≤_ [_]_≤′_

Similarity : Size → Rel₂ ℓ Proc
Similarity i = ν StepC i

Similarity′ : Size → Rel₂ ℓ Proc
Similarity′ i = ν′ StepC i

[_]_≤_ : Size → Proc → Proc → Type ℓ
[_]_≤_ i = curry (Similarity i)

[_]_≤′_ : Size → Proc → Proc → Type ℓ
[_]_≤′_ i = curry (Similarity′ i)

_≤_ : Proc → Proc → Type ℓ
_≤_ = [ ∞ ]_≤_

_≤′_ : Proc → Proc → Type ℓ
_≤′_ = [ ∞ ]_≤′_

-- Similarity is reflexive.

mutual

  reflexive-≤ : ∀ {p i} → [ i ] p ≤ p
  reflexive-≤ =
    StepC.⟨ (λ p⟶p′ → _ , ⟶→↝ p⟶p′ , reflexive-≤′)
          ⟩

  reflexive-≤′ : ∀ {p i} → [ i ] p ≤′ p
  force reflexive-≤′ = reflexive-≤

≡⇒≤ : ∀ {p q} → p ≡ q → p ≤ q
≡⇒≤ refl = reflexive-≤

-- Functions that can be used to aid the instance resolution
-- mechanism.

infix -2 ≤:_ ≤′:_

≤:_ : ∀ {i p q} → [ i ] p ≤ q → [ i ] p ≤ q
≤:_ = id

≤′:_ : ∀ {i p q} → [ i ] p ≤′ q → [ i ] p ≤′ q
≤′:_ = id

-- Bisimilarity of similarity proofs.

infix 4 [_]_≡_ [_]_≡′_

[_]_≡_ : ∀ {p q} → Size → (_ _ : ν StepC ∞ (p , q)) → Type ℓ
[_]_≡_ i = curry (ν-bisimilar i)

[_]_≡′_ : ∀ {p q} → Size → (_ _ : ν′ StepC ∞ (p , q)) → Type ℓ
[_]_≡′_ i = curry (ν′-bisimilar i)

-- An alternative characterisation of bisimilarity of similarity
-- proofs.

[]≡↔ :
  Eq.Extensionality ℓ ℓ →
  ∀ {p q} {i : Size} (p≤q₁ p≤q₂ : ν StepC ∞ (p , q)) →

  [ i ] p≤q₁ ≡ p≤q₂

    ↔

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′≤q′₁ = StepC.challenge p≤q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = StepC.challenge p≤q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′≤q′₁ ≡′ p′≤q′₂)

[]≡↔ ext {p} {q} {i} p≤q₁@(s₁ , f₁) p≤q₂@(s₂ , f₂) =
  [ i ] p≤q₁ ≡ p≤q₂                                                     ↝⟨ ν-bisimilar↔ ext (s₁ , f₁) (s₂ , f₂) ⟩

  (∃ λ (eq : s₁ ≡ s₂) →
   ∀ {o} (p : Container.Position StepC s₁ o) →
   [ i ] f₁ p ≡′ f₂ (subst (λ s → Container.Position StepC s o) eq p))  ↝⟨ Step.⟦StepC⟧₂↔ ext (ν′-bisimilar i) p≤q₁ p≤q₂ ⟩□

  (∀ {p′ μ} (p⟶p′ : p [ μ ]⟶ p′) →
   let q′₁ , q⟶q′₁ , p′≤q′₁ = StepC.challenge p≤q₁ p⟶p′
       q′₂ , q⟶q′₂ , p′≤q′₂ = StepC.challenge p≤q₂ p⟶p′
   in ∃ λ (q′₁≡q′₂ : q′₁ ≡ q′₂) →
        subst (q [ μ ]↝_) q′₁≡q′₂ q⟶q′₁ ≡ q⟶q′₂
          ×
        [ i ] subst (ν′ StepC ∞ ∘ (p′ ,_)) q′₁≡q′₂ p′≤q′₁ ≡′ p′≤q′₂)    □

-- A statement of extensionality for similarity.

Extensionality : Type ℓ
Extensionality = ν′-extensionality StepC

-- This form of extensionality can be used to derive another form (in
-- the presence of extensionality for functions).

extensionality :
  Eq.Extensionality ℓ ℓ →
  Extensionality →
  ∀ {p q} {p≤q₁ p≤q₂ : ν StepC ∞ (p , q)} →
  [ ∞ ] p≤q₁ ≡ p≤q₂ → p≤q₁ ≡ p≤q₂
extensionality ext ν-ext = ν-extensionality ext ν-ext

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
open import Relation.Binary.Core

module BBHeap.Subtyping.Properties {A : Set}
                  (_≤_ : A → A → Set)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Subtyping  _≤_ trans≤
open import BBHeap.Properties  _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Bound.Lower.Order.Properties _≤_ trans≤
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A

subtyping⋘l : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b) → h ⋘ h' → subtyping b''≤b h ⋘ h'
subtyping⋘l b''≤b lf⋘ = lf⋘
subtyping⋘l b''≤b (ll⋘ b≤x b'≤x' l⋘r l'⋘r' l'≃r' r≃l') = ll⋘ (transLeB b''≤b b≤x) b'≤x' l⋘r l'⋘r' l'≃r' r≃l'
subtyping⋘l b''≤b (lr⋘ b≤x b'⋘x' l⋙r l'⋘r' l'≃r' l⋗l') = lr⋘ (transLeB b''≤b b≤x) b'⋘x' l⋙r l'⋘r' l'≃r' l⋗l'

subtyping⋘ : {b b' b'' b''' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b)(b'''≤b' : LeB b''' b') → h ⋘ h' → subtyping b''≤b h ⋘ subtyping b'''≤b' h'
subtyping⋘ b''≤b b'''≤b' lf⋘ = lf⋘
subtyping⋘ b''≤b b'''≤b' (ll⋘ b≤x b'≤x' l⋘r l'⋘r' l'≃r' r≃l') = ll⋘ (transLeB b''≤b b≤x) (transLeB b'''≤b' b'≤x') l⋘r l'⋘r' l'≃r' r≃l'
subtyping⋘ b''≤b b'''≤b' (lr⋘ b≤x b'⋘x' l⋙r l'⋘r' l'≃r' l⋗l') = lr⋘ (transLeB b''≤b b≤x) (transLeB b'''≤b' b'⋘x') l⋙r l'⋘r' l'≃r' l⋗l'

subtyping⋙r : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b' : LeB b'' b') → h ⋙ h' → h ⋙ subtyping b''≤b' h'
subtyping⋙r b''≤b' (⋙lf b≤x) = ⋙lf b≤x
subtyping⋙r b''≤b' (⋙rl b≤x b'≤x' l⋘r l≃r l'⋘r' l⋗r') = ⋙rl b≤x (transLeB b''≤b' b'≤x') l⋘r l≃r l'⋘r' l⋗r'
subtyping⋙r b''≤b' (⋙rr b≤x b'⋘x' l⋘r l≃r l'⋙r' l≃l') = ⋙rr b≤x (transLeB b''≤b' b'⋘x') l⋘r l≃r l'⋙r' l≃l'

subtyping⋙ : {b b' b'' b''' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b)(b'''≤b' : LeB b''' b') → h ⋙ h' → subtyping b''≤b h ⋙ subtyping b'''≤b' h'
subtyping⋙ b''≤b b'''≤b' (⋙lf b≤x) = ⋙lf (transLeB b''≤b b≤x)
subtyping⋙ b''≤b b'''≤b' (⋙rl b≤x b'≤x' l⋘r l≃r l'⋘r' l⋗r') = ⋙rl (transLeB b''≤b b≤x) (transLeB b'''≤b' b'≤x') l⋘r l≃r l'⋘r' l⋗r'
subtyping⋙ b''≤b b'''≤b' (⋙rr b≤x b'⋘x' l⋘r l≃r l'⋙r' l≃l') = ⋙rr (transLeB b''≤b b≤x) (transLeB b'''≤b' b'⋘x') l⋘r l≃r l'⋙r' l≃l'

subtyping≃r : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b' : LeB b'' b') → h ≃ h' → h ≃ subtyping b''≤b' h'
subtyping≃r b''≤b' ≃lf = ≃lf
subtyping≃r b''≤b' (≃nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') = ≃nd b≤x (transLeB b''≤b' b'≤x') l⋘r l'⋘r' l≃r l'≃r' l≃l'

subtyping≃l : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b) → h ≃ h' → subtyping b''≤b h ≃ h'
subtyping≃l b''≤b h≃h' = sym≃ (subtyping≃r b''≤b (sym≃ h≃h'))

subtyping≃ : {b b' b'' b''' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b)(b'''≤b' : LeB b''' b') → h ≃ h' → subtyping b''≤b h ≃ subtyping b'''≤b' h'
subtyping≃ b''≤b b'''≤b' h≃h' = subtyping≃r b'''≤b' (subtyping≃l b''≤b h≃h')

subtyping⋗r : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b' : LeB b'' b') → h ⋗ h' → h ⋗ subtyping b''≤b' h'
subtyping⋗r b''≤b' (⋗lf b≤x) = ⋗lf b≤x
subtyping⋗r b''≤b' (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l') = ⋗nd b≤x (transLeB b''≤b' b'≤x') l⋘r l'⋘r' l≃r l'≃r' l⋗l'

subtyping⋗l : {b b' b'' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b) → h ⋗ h' → subtyping b''≤b h ⋗ h'
subtyping⋗l b''≤b (⋗lf b≤x) = ⋗lf (transLeB b''≤b b≤x)
subtyping⋗l b''≤b (⋗nd b≤x b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l') = ⋗nd (transLeB b''≤b b≤x) b'≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l'

subtyping⋗ : {b b' b'' b''' : Bound}{h : BBHeap b}{h' : BBHeap b'}(b''≤b : LeB b'' b)(b'''≤b' : LeB b''' b') → h ⋗ h' → subtyping b''≤b h ⋗ subtyping b'''≤b' h'
subtyping⋗ b''≤b b'''≤b' h⋗h' = subtyping⋗r b'''≤b' (subtyping⋗l b''≤b h⋗h')

lemma-subtyping# : {b b' : Bound}(b'≤b : LeB b' b)(h : BBHeap b) → # (subtyping b'≤b h) ≡ # h
lemma-subtyping# b'≤b leaf = refl
lemma-subtyping# b'≤b (left b≤x l⋘r) = refl
lemma-subtyping# b'≤b (right b≤x l⋙r) = refl

lemma-subtyping≡ : {b b' : Bound}(b'≤b : LeB b' b)(h : BBHeap b) → (flatten (subtyping b'≤b h)) ≡ flatten h
lemma-subtyping≡ b'≤b leaf = refl
lemma-subtyping≡ b'≤b (left {l = l} {r = r} b≤x l⋘r) rewrite lemma-subtyping≡ b≤x l | lemma-subtyping≡ b≤x r = refl
lemma-subtyping≡ b'≤b (right {l = l} {r = r} b≤x l⋙r) rewrite lemma-subtyping≡ b≤x l | lemma-subtyping≡ b≤x r = refl

lemma-subtyping∼ : {b b' : Bound}(b'≤b : LeB b' b)(h : BBHeap b) → flatten (subtyping b'≤b h) ∼ flatten h
lemma-subtyping∼ b'≤b leaf = ∼[]
lemma-subtyping∼ b'≤b (left b≤x l⋘r) = ∼x /head /head refl∼
lemma-subtyping∼ b'≤b (right b≤x l⋙r) = ∼x /head /head refl∼

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

-- Finished 6pm Th, March 24! yay!
-- Bit thanks to tzaikin for posting his work online (some of his macros
-- were essential for this proof for me) and to the code we saw in class today.

module EH where

open import Level using (_⊔_)
open import Data.Product using (Σ; _,_)
open import Function renaming (_∘_ to _○_)

infixr 8  _∘_     -- path composition
infixr 8  _⋆_     -- horizontal path composition
infix  4  _≡_     -- propositional equality
infix  4  _∼_     -- homotopy between two functions
infix  4  _≃_     -- type of equivalences
-- macros from tzaikin for equational rewriting over non-standard ≡
infixr 4 _≡⟨_⟩_
infix 4  _∎

------------------------------------------------------------------------------
-- A few HoTT primitives

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

pathInd : ∀ {u ℓ} → {A : Set u} →
          (C : {x y : A} → x ≡ y → Set ℓ) →
          (c : (x : A) → C (refl x)) →
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

--

! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = pathInd (λ {x} {y} _ → y ≡ x) refl

_∘_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ {u} {A} {x} {y} {z} p q =
  pathInd {u}
    (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q)
    {x} {y} p z q

-- Handy "macros" (from tzaikin)
_∎ : {A : Set} → (p : A) → p ≡ p
p ∎ = refl p

_≡⟨_⟩_ : {A : Set} → {q r : A} → (p : A) → p ≡ q → q ≡ r → p ≡ r
p ≡⟨ α ⟩ β = α ∘ β

--

RU : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p ∘ refl y)
RU {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ p ∘ (refl y))
    (λ x → refl (refl x))
    {x} {y} p

LU : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
LU {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (refl x) ∘ p)
    (λ x → refl (refl x))
    {x} {y} p

invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p ∘ p ≡ refl y)
invTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! p ∘ p ≡ refl y)
    (λ x → refl (refl x))
    {x} {y} p

invTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p ∘ ! p ≡ refl x)
invTransR {ℓ} {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ∘ ! p ≡ refl x)
    (λ x → refl (refl x))
    {x} {y} p

invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p)
invId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! (! p) ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) →
         (p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
assocP {A} {x} {y} {z} {w} p q r =
  pathInd
    (λ {x} {y} p → (z : A) → (w : A) → (q : y ≡ z) → (r : z ≡ w) →
      p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
    (λ x z w q r →
      pathInd
        (λ {x} {z} q → (w : A) → (r : z ≡ w) →
          (refl x) ∘ (q ∘ r) ≡ ((refl x) ∘ q) ∘ r)
        (λ x w r →
          pathInd
            (λ {x} {w} r →
              (refl x) ∘ ((refl x) ∘ r) ≡
              ((refl x) ∘ (refl x)) ∘ r)
            (λ x → (refl (refl x)))
            {x} {w} r)
        {x} {z} q w r)
    {x} {y} p z w q r

invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) →
          ! (p ∘ q) ≡ ! q ∘ ! p
invComp {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → (z : A) → (q : y ≡ z) → ! (p ∘ q) ≡ ! q ∘ ! p)
    (λ x z q →
      pathInd
        (λ {x} {z} q → ! (refl x ∘ q) ≡ ! q ∘ ! (refl x))
        (λ x → refl (refl x))
        {x} {z} q)
    {x} {y} p z q

--

ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
     (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd -- on p
    (λ {x} {y} p → f x ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

apfTrans : ∀ {u} → {A B : Set u} {x y z : A} →
  (f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q)
apfTrans {u} {A} {B} {x} {y} {z} f p q =
  pathInd {u}
    (λ {x} {y} p → (z : A) → (q : y ≡ z) →
      ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q))
    (λ x z q →
      pathInd {u}
        (λ {x} {z} q →
          ap f (refl x ∘ q) ≡ (ap f (refl x)) ∘ (ap f q))
        (λ x → refl (refl (f x)))
        {x} {z} q)
    {x} {y} p z q

apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) →
         ap f (! p) ≡ ! (ap f p)
apfInv {u} {A} {B} {x} {y} f p =
  pathInd {u}
    (λ {x} {y} p → ap f (! p) ≡ ! (ap f p))
    (λ x → refl (ap f (refl x)))
    {x} {y} p

apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) →
          ap g (ap f p) ≡ ap (g ○ f) p
apfComp {A} {B} {C} {x} {y} f g p =
  pathInd
    (λ {x} {y} p → ap g (ap f p) ≡ ap (g ○ f) p)
    (λ x → refl (ap g (ap f (refl x))))
    {x} {y} p

apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p
apfId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ap id p ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

--

transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} →
  (P : A → Set ℓ') → (p : x ≡ y) → P x → P y
transport {ℓ} {ℓ'} {A} {x} {y} P p =
  pathInd -- on p
    (λ {x} {y} p → (P x → P y))
    (λ _ → id)
    {x} {y} p

apd : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : A → Set ℓ'} {x y : A} → (f : (a : A) → B a) →
  (p : x ≡ y) → (transport B p (f x) ≡ f y)
apd {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd
    (λ {x} {y} p → transport B p (f x) ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

-- Homotopies and equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (ℓ ⊔ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ○ g) ∼ id
    h : B → A
    β : (h ○ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A ≃ B = Σ (A → B) isequiv

postulate
  univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B)

------------------------------------------------------------------------------
-- Path and loop spaces

1-Path : {A : Set} → (a b : A) → Set
1-Path {A} a b = (a ≡ b)

2-Path : {A : Set} → (a b : A) (p q : 1-Path {A} a b) → Set
2-Path {A} a b p q = (p ≡ q)

Ω : (A : Set) → {a : A} → Set
Ω A {a} = 1-Path {A} a a

Ω² : (A : Set) → {a : A} → Set
Ω² A {a} = 2-Path {A} a a (refl a) (refl a)

-- Whiskering Lemmas
--     ___ p ___     ___ r ___
--   /           \ /           \
--  a     α⇓      b     β⇓     c
--   \           / \           /
--     --- q ---     --- s ---

wskR : {A : Set}
           {a b c : A}
           {p q : 1-Path {A} a b} →
           (α : 2-Path {A} a b p q) →
           (r : 1-Path {A} b c) →
           (p ∘ r) ≡ (q ∘ r)
wskR {A} {a} {b} {c} {p} {q} α r =
         (pathInd (λ {b} {c} r →
                     {p q : a ≡ b} →
                     (α : p ≡ q) →
                     2-Path {A} a c (p ∘ r) (q ∘ r))
                  (λ b {p} {q} α →
                    (p ∘ refl b) ≡⟨ ! (RU p) ⟩
                    p ≡⟨ α ⟩
                    q ≡⟨ RU q ⟩
                    (q ∘ refl b) ∎)
                 r)
                 α

wskL : {A : Set}
           {a b c : A}
           {r s : 1-Path {A} b c} →
           (q : 1-Path {A} a b) →
           (β : 2-Path {A} b c r s) →
           (q ∘ r) ≡ (q ∘ s)
wskL {A} {a} {b} {c} {r} {s} q β =
  (pathInd (λ {a} {b} q →
              {r s : b ≡ c} →
              (α : r ≡ s) →
              2-Path {A} a c (q ∘ r) (q ∘ s))
           ((λ b {p} {q} β →
               (refl b ∘ p) ≡⟨ ! (LU p) ⟩
               p ≡⟨ β ⟩
               q ≡⟨ LU q ⟩
               (refl b ∘ q) ∎))
           q)
           β

_⋆_ : {A : Set}
      {a b c : A}
      {p q : 1-Path {A} a b}
      {r s : 1-Path {A} b c}
      (α : 2-Path {A} a b p q) →
      (β : 2-Path {A} b c r s) →
      (p ∘ r) ≡ (q ∘ s)
_⋆_ {A} {a} {b} {c} {p} {q} {r} {s} α β = (wskR α r) ∘ (wskL q β)

Hcomp→compR1 : {A : Set}
              {a : A}
              (α : 2-Path {A} a a (refl a) (refl a)) →
              (wskR α (refl a)) ≡ (! (RU (refl a))) ∘ α ∘ (RU (refl a))
Hcomp→compR1 {A} {a} α = refl
                           (pathInd (λ {x} {y} _ → x ≡ y) refl
                            (pathInd (λ {x} {y} _ → (x₁ : a ≡ a) (x₂ : y ≡ x₁) → x ≡ x₁)
                             (λ x x₁ → pathInd (λ {x₂} {y} _ → x₂ ≡ y) refl) α (refl a)
                             (refl (refl a))))

Hcomp→compL1 : {A : Set}
              {a : A}
              (β : 2-Path {A} a a (refl a) (refl a)) →
              (wskL (refl a) β) ≡ (! (LU (refl a))) ∘ β ∘ (LU (refl a))
Hcomp→compL1 {A} {a} β = refl
                           (pathInd (λ {x} {y} _ → x ≡ y) refl
                            (pathInd (λ {x} {y} _ → (x₁ : a ≡ a) (x₂ : y ≡ x₁) → x ≡ x₁)
                             (λ x x₁ → pathInd (λ {x₂} {y} _ → x₂ ≡ y) refl) β (refl a)
                             (refl (refl a))))

-- proof from pg 81
α⋆β≡α∘β : {A : Set}
             {a : A}
             (α : 2-Path {A} a a (refl a) (refl a)) →
             (β : 2-Path {A} a a (refl a) (refl a)) →
             α ⋆ β ≡ α ∘ β
α⋆β≡α∘β {A} {a} α β =

  α ⋆ β

  ≡⟨ refl (α ⋆ β) ⟩

  (wskR α ra) ∘ (wskL ra β)

  ≡⟨ refl ((!(refl ra) ∘ α ∘ (refl ra)) ∘ (wskL ra β)) ⟩

  (!(refl ra) ∘ (α ∘ (refl ra))) ∘ (wskL ra β)

  ≡⟨  ap (λ p → ((!(refl ra) ∘ p) ∘ (wskL ra β))) (! (RU α)) ⟩

  ((!(refl ra) ∘ α) ∘ (wskL ra β))

  ≡⟨ ap (λ p → (p ∘ (wskL ra β))) (! (LU α)) ⟩

  (α ∘ (wskL ra β))

  ≡⟨ refl (α ∘ (wskL ra β)) ⟩

  (α ∘ (!(refl ra) ∘ β ∘ (refl ra)))

  ≡⟨ ap (λ p → (α ∘ (!(refl ra) ∘ p))) (! (RU β)) ⟩

  (α ∘ (!(refl ra) ∘ β))

  ≡⟨ ap (λ p → (α ∘ p)) (! (LU β)) ⟩

  α ∘ β ∎
  where ra = (refl a)

_⋆'_ : {A : Set}
       {a b c : A}
       {p q : 1-Path {A} a b}
       {r s : 1-Path {A} b c}
       (α : 2-Path {A} a b p q) →
       (β : 2-Path {A} b c r s) →
       (p ∘ r) ≡ (q ∘ s)
_⋆'_ {A} {a} {b} {c} {p} {q} {r} {s} α β = (wskL p β) ∘ (wskR α s)

α⋆'β≡β∘α : {A : Set}
           {a : A}
           (α : 2-Path {A} a a (refl a) (refl a)) →
           (β : 2-Path {A} a a (refl a) (refl a)) →
           α ⋆' β ≡ β ∘ α
α⋆'β≡β∘α {A} {a} α β =
  α ⋆' β

  ≡⟨ refl (α ⋆' β) ⟩

  (wskL ra β) ∘ (!(refl ra) ∘ (α ∘ (refl ra)))

  ≡⟨  ap (λ p → ((wskL ra β) ∘ (!(refl ra) ∘ p))) (! (RU α)) ⟩

  ((wskL ra β) ∘ (!(refl ra) ∘ α))

  ≡⟨ ap (λ p → ((wskL ra β) ∘ p)) (! (LU α)) ⟩

  ((wskL ra β) ∘ α)

  ≡⟨ refl ((wskL ra β) ∘ α) ⟩

  ((!(refl ra) ∘ β ∘ (refl ra)) ∘ α)

  ≡⟨ ap (λ p → ((!(refl ra) ∘ p) ∘ α)) (! (RU β)) ⟩

  ((!(refl ra) ∘ β) ∘ α)

  ≡⟨ ap (λ p → (p ∘ α)) (! (LU β)) ⟩

  β ∘ α ∎

  where ra = (refl a)

-- yuck lots of nested induction
α⋆β≡α⋆'β : {A : Set}
           {a : A}
           (α : 2-Path {A} a a (refl a) (refl a)) →
           (β : 2-Path {A} a a (refl a) (refl a)) →
           α ⋆ β ≡ α ⋆' β
α⋆β≡α⋆'β {A} {a} α β =
  -- induction on α
  pathInd
    (λ α → α ⋆ β ≡ α ⋆' β)
    (λ p →
       -- induction on β
       pathInd
         (λ β → refl p ⋆ β ≡ refl p ⋆' β)
         (λ q →
            -- induction on p
            (pathInd
              (λ {a} {b} p → (c : A) → (q : b ≡ c) →
                 ((refl p ⋆ refl q) ≡ (refl p ⋆' refl q)))
                      (λ a d q →
                         -- induction on q
                         pathInd
                           (λ {a} {d} r →
                              ((refl (refl a) ⋆ refl r) ≡ (refl (refl a) ⋆' refl r)))
                           (λ a → refl (refl (refl a)))
                         q)
               p a q))
             β)
           α

eckmann-hilton : {A : Set} {a : A} (α β : Ω² A {a}) → α ∘ β ≡ β ∘ α
eckmann-hilton {A} {a} α β =
  α ∘ β
  ≡⟨ ! (α⋆β≡α∘β α β) ⟩
  α ⋆ β
  ≡⟨ α⋆β≡α⋆'β α β ⟩
  α ⋆' β
  ≡⟨ α⋆'β≡β∘α α β ⟩
  β ∘ α ∎
------------------------------------------------------------------------------

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
module rename where

open import lib

open import cedille-types
open import ctxt-types
open import is-free
open import syntax-util

renamectxt : Set
renamectxt = stringset × trie string  {- the trie maps vars to their renamed versions,
                                         and the stringset stores all those renamed versions -}

empty-renamectxt : renamectxt
empty-renamectxt = empty-stringset , empty-trie

renamectxt-contains : renamectxt → string → 𝔹
renamectxt-contains (_ , r) s = trie-contains r s

renamectxt-insert : renamectxt → (s1 s2 : string) → renamectxt
renamectxt-insert (ranr , r) s x = stringset-insert ranr x , trie-insert r s x

renamectxt-single : var → var → renamectxt
renamectxt-single = renamectxt-insert empty-renamectxt

renamectxt-lookup : renamectxt → string → maybe string
renamectxt-lookup (ranr , r) s = trie-lookup r s

renamectxt-remove : renamectxt → string → renamectxt
renamectxt-remove (ranr , r) s with trie-lookup r s
renamectxt-remove (ranr , r) s | nothing = ranr , r
renamectxt-remove (ranr , r) s | just s' = stringset-remove ranr s' , trie-remove r s

renamectxt-in-range : renamectxt → string → 𝔹
renamectxt-in-range (ranr , r) s = stringset-contains ranr s

renamectxt-in-field : renamectxt → string → 𝔹
renamectxt-in-field m s = renamectxt-contains m s || renamectxt-in-range m s

renamectxt-rep : renamectxt → string → string
renamectxt-rep r x with renamectxt-lookup r x
renamectxt-rep r x | nothing = x
renamectxt-rep r x | just x' = x'

eq-var : renamectxt → string → string → 𝔹
eq-var r x y = renamectxt-rep r x =string renamectxt-rep r y

pick-new-name : string → string
pick-new-name x = x ^ "'"

{- rename-away-from x g r rename the variable x to be some new name (related to x)
   which does not satisfy the given predicate on names (assuming this is possible),
   and is not in the domain of the renamectxt . -}
{-# NON_TERMINATING #-}
rename-away-from : string → (string → 𝔹) → renamectxt → string
rename-away-from x g r =
  if (g x) then
    rename-away-from (pick-new-name x) g r
  else if (renamectxt-in-field r x) then
    rename-away-from (pick-new-name x) g r
  else x

fresh-var : string → (string → 𝔹) → renamectxt → string
fresh-var = rename-away-from

rename-var-if : {ed : exprd} → ctxt → renamectxt → var → ⟦ ed ⟧ → var
rename-var-if Γ ρ y t =
  if is-free-in check-erased y t || renamectxt-in-range ρ y then
    rename-away-from y (ctxt-binds-var Γ) ρ
  else
    y

renamectxt-insert* : renamectxt → (vs1 vs2 : 𝕃 string) → maybe renamectxt
renamectxt-insert* ρ [] [] = just ρ
renamectxt-insert* ρ (x :: vs1) (y :: vs2) = renamectxt-insert* (renamectxt-insert ρ x y) vs1 vs2
renamectxt-insert* ρ _ _ = nothing

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
------------------------------------------------------------------------------
-- Streams (unbounded lists)
------------------------------------------------------------------------------

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

module FOTC.Data.Stream where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type public

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

postulate
  zeros    : D
  zeros-eq : zeros ≡ zero ∷ zeros
{-# ATP axiom zeros-eq #-}

postulate
  ones    : D
  ones-eq : ones ≡ succ₁ zero ∷ ones
{-# ATP axiom ones-eq #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Interpretation where

open import VariableName
open import FunctionName
open import PredicateName
open import Element
open import Elements
open import TruthValue

record Interpretation : Set
 where
  field
    μ⟦_⟧ : VariableName → Element
    𝑓⟦_⟧ : FunctionName → Elements → Element
    𝑃⟦_⟧ : PredicateName → Elements → TruthValue

open Interpretation public

open import OscarPrelude
open import Term
open import Delay
open import Vector

mutual

  τ⇑⟦_⟧ : Interpretation → {i : Size} → Term → Delay i Element
  τ⇑⟦ I ⟧ (variable 𝑥) = now $ μ⟦ I ⟧ 𝑥
  τ⇑⟦ I ⟧ (function 𝑓 τs) = 𝑓⟦ I ⟧ 𝑓 ∘ ⟨_⟩ <$> τs⇑⟦ I ⟧ τs

  τs⇑⟦_⟧ : Interpretation → {i : Size} → (τs : Terms) → Delay i (Vector Element (arity τs))
  τs⇑⟦ I ⟧ ⟨ ⟨ [] ⟩ ⟩ = now ⟨ [] ⟩
  τs⇑⟦ I ⟧ ⟨ ⟨ τ ∷ τs ⟩ ⟩ = τ⇑⟦ I ⟧ τ >>= (λ t → τs⇑⟦ I ⟧ ⟨ ⟨ τs ⟩ ⟩ >>= λ ts → now ⟨ t ∷ vector ts ⟩)

τs⇓⟦_⟧ : (I : Interpretation) → (τs : Terms) → τs⇑⟦ I ⟧ τs ⇓
τs⇓⟦ I ⟧ ⟨ ⟨ [] ⟩ ⟩ = _ , now⇓
τs⇓⟦ I ⟧ ⟨ ⟨ variable 𝑥 ∷ τs ⟩ ⟩ = _ , τs⇓⟦ I ⟧ ⟨ ⟨ τs ⟩ ⟩ ⇓>>=⇓ now⇓
τs⇓⟦ I ⟧ ⟨ ⟨ function 𝑓₁ τs₁ ∷ τs₂ ⟩ ⟩ =
  _ , τs⇓⟦ I ⟧ τs₁ ⇓>>=⇓ now⇓ >>=⇓ (τs⇓⟦ I ⟧ ⟨ ⟨ τs₂ ⟩ ⟩ ⇓>>=⇓ now⇓)

τ⇓⟦_⟧ : (I : Interpretation) → (τ : Term) → τ⇑⟦ I ⟧ τ ⇓
τ⇓⟦ I ⟧ (variable 𝑥) = _ , now⇓
τ⇓⟦ I ⟧ (function 𝑓 τs) = _ , τs⇓⟦ I ⟧ τs ⇓>>=⇓ now⇓

τ⟦_⟧ : (I : Interpretation) → {i : Size} → (τ : Term) → Element
τ⟦ I ⟧ τ = fst (τ⇓⟦ I ⟧ τ)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Terms used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Term where

open import Data.List.Base hiding (_++_)
import Data.List.Properties as Lₚ
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Product
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Reflection.Abstraction
open import Reflection.Argument
open import Reflection.Argument.Information using (visibility)
import Reflection.Argument.Visibility as Visibility; open Visibility.Visibility
import Reflection.Literal as Literal
import Reflection.Meta as Meta
open import Reflection.Name as Name using (Name)
import Reflection.Pattern as Pattern
open import Relation.Nullary
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Re-exporting the builtin type and constructors

open import Agda.Builtin.Reflection as Builtin public
  using (Sort; Type; Term; Clause)
open Sort public
open Term public renaming (agda-sort to sort)
open Clause public

------------------------------------------------------------------------
-- Handy synonyms

Clauses : Set
Clauses = List Clause

-- Pattern synonyms for more compact presentation

pattern vLam s t           = lam visible   (abs s t)
pattern hLam s t           = lam hidden    (abs s t)
pattern iLam s t           = lam instance′ (abs s t)
pattern Π[_∶_]_ s a ty     = pi a (abs s ty)
pattern vΠ[_∶_]_ s a ty    = Π[ s ∶ (vArg a) ] ty
pattern hΠ[_∶_]_ s a ty    = Π[ s ∶ (hArg a) ] ty
pattern iΠ[_∶_]_ s a ty    = Π[ s ∶ (iArg a) ] ty

----------------------------------------------------------------------
-- Utility functions

getName : Term → Maybe Name
getName (con c args) = just c
getName (def f args) = just f
getName _            = nothing

-- "n ⋯⟅∷⟆ xs" prepends "n" visible unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial inferable arguments.
infixr 5 _⋯⟨∷⟩_
_⋯⟨∷⟩_ : ℕ → Args Term → Args Term
zero  ⋯⟨∷⟩ xs = xs
suc i ⋯⟨∷⟩ xs = unknown ⟨∷⟩ (i ⋯⟨∷⟩ xs)
{-# INLINE _⋯⟨∷⟩_ #-}

-- "n ⋯⟅∷⟆ xs" prepends "n" hidden unknown arguments to the list of
-- arguments. Useful when constructing the list of arguments for a
-- function with initial implicit arguments.
infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ : ℕ → Args Term → Args Term
zero  ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ (i ⋯⟅∷⟆ xs)
{-# INLINE _⋯⟅∷⟆_ #-}

------------------------------------------------------------------------
-- Decidable equality

clause-injective₁ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′
clause-injective₁ refl = refl

clause-injective₂ : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → b ≡ b′
clause-injective₂ refl = refl

clause-injective : ∀ {ps ps′ b b′} → clause ps b ≡ clause ps′ b′ → ps ≡ ps′ × b ≡ b′
clause-injective = < clause-injective₁ , clause-injective₂ >

absurd-clause-injective : ∀ {ps ps′} → absurd-clause ps ≡ absurd-clause ps′ → ps ≡ ps′
absurd-clause-injective refl = refl

infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
        _≟-Clause_ _≟-Clauses_ _≟_
        _≟-Sort_

_≟-AbsTerm_ : DecidableEquality (Abs Term)
_≟-AbsType_ : DecidableEquality (Abs Type)
_≟-ArgTerm_ : DecidableEquality (Arg Term)
_≟-ArgType_ : DecidableEquality (Arg Type)
_≟-Args_    : DecidableEquality (Args Term)
_≟-Clause_  : DecidableEquality Clause
_≟-Clauses_ : DecidableEquality Clauses
_≟_         : DecidableEquality Term
_≟-Sort_    : DecidableEquality Sort

-- Decidable equality 'transformers'
-- We need to inline these because the terms are not sized so termination
-- would not obvious if we were to use higher-order functions such as
-- Data.List.Properties' ≡-dec

abs s a ≟-AbsTerm abs s′ a′ = unAbs-dec (a ≟ a′)
abs s a ≟-AbsType abs s′ a′ = unAbs-dec (a ≟ a′)
arg i a ≟-ArgTerm arg i′ a′ = unArg-dec (a ≟ a′)
arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′)

[]       ≟-Args []       = yes refl
(x ∷ xs) ≟-Args (y ∷ ys) = Lₚ.∷-dec (x ≟-ArgTerm y) (xs ≟-Args ys)
[]       ≟-Args (_ ∷ _)  = no λ()
(_ ∷ _)  ≟-Args []       = no λ()

[]       ≟-Clauses []       = yes refl
(x ∷ xs) ≟-Clauses (y ∷ ys) = Lₚ.∷-dec (x ≟-Clause y) (xs ≟-Clauses ys)
[]       ≟-Clauses (_ ∷ _)  = no λ()
(_ ∷ _)  ≟-Clauses []       = no λ()

clause ps b ≟-Clause clause ps′ b′ =
  Dec.map′ (uncurry (cong₂ clause)) clause-injective (ps Pattern.≟s ps′ ×-dec b ≟ b′)
absurd-clause ps ≟-Clause absurd-clause ps′ =
  Dec.map′ (cong absurd-clause) absurd-clause-injective (ps Pattern.≟s ps′)
clause _ _      ≟-Clause absurd-clause _ = no λ()
absurd-clause _ ≟-Clause clause _ _      = no λ()

var-injective₁ : ∀ {x x′ args args′} → var x args ≡ var x′ args′ → x ≡ x′
var-injective₁ refl = refl

var-injective₂ : ∀ {x x′ args args′} → var x args ≡ var x′ args′ → args ≡ args′
var-injective₂ refl = refl

var-injective :  ∀ {x x′ args args′} → var x args ≡ var x′ args′ → x ≡ x′ × args ≡ args′
var-injective = < var-injective₁ , var-injective₂ >

con-injective₁ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′
con-injective₁ refl = refl

con-injective₂ : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → args ≡ args′
con-injective₂ refl = refl

con-injective : ∀ {c c′ args args′} → con c args ≡ con c′ args′ → c ≡ c′ × args ≡ args′
con-injective = < con-injective₁ , con-injective₂ >

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

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

def-injective : ∀ {f f′ args args′} → def f args ≡ def f′ args′ → f ≡ f′ × args ≡ args′
def-injective = < def-injective₁ , def-injective₂ >

meta-injective₁ : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → x ≡ x′
meta-injective₁ refl = refl

meta-injective₂ : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → args ≡ args′
meta-injective₂ refl = refl

meta-injective : ∀ {x x′ args args′} → meta x args ≡ meta x′ args′ → x ≡ x′ × args ≡ args′
meta-injective = < meta-injective₁ , meta-injective₂ >

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

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

lam-injective : ∀ {v v′ t t′} → lam v t ≡ lam v′ t′ → v ≡ v′ × t ≡ t′
lam-injective = < lam-injective₁ , lam-injective₂ >

pat-lam-injective₁ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′
pat-lam-injective₁ refl = refl

pat-lam-injective₂ : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → args ≡ args′
pat-lam-injective₂ refl = refl

pat-lam-injective : ∀ {cs cs′ args args′} → pat-lam cs args ≡ pat-lam cs′ args′ → cs ≡ cs′ × args ≡ args′
pat-lam-injective = < pat-lam-injective₁ , pat-lam-injective₂ >

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

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

pi-injective : ∀ {t₁ t₁′ t₂ t₂′} → pi t₁ t₂ ≡ pi t₁′ t₂′ → t₁ ≡ t₁′ × t₂ ≡ t₂′
pi-injective = < pi-injective₁ , pi-injective₂ >

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

lit-injective : ∀ {x y} → lit x ≡ lit y → x ≡ y
lit-injective refl = refl

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

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

var x args ≟ var x′ args′ =
  Dec.map′ (uncurry (cong₂ var)) var-injective (x ℕ.≟ x′ ×-dec args ≟-Args args′)
con c args ≟ con c′ args′ =
  Dec.map′ (uncurry (cong₂ con)) con-injective (c Name.≟ c′ ×-dec args ≟-Args args′)
def f args ≟ def f′ args′ =
  Dec.map′ (uncurry (cong₂ def)) def-injective (f Name.≟ f′ ×-dec args ≟-Args args′)
meta x args ≟ meta x′ args′ =
  Dec.map′ (uncurry (cong₂ meta)) meta-injective (x Meta.≟ x′   ×-dec args ≟-Args args′)
lam v t    ≟ lam v′ t′    =
  Dec.map′ (uncurry (cong₂ lam)) lam-injective (v Visibility.≟ v′ ×-dec t ≟-AbsTerm t′)
pat-lam cs args ≟ pat-lam cs′ args′ =
  Dec.map′ (uncurry (cong₂ pat-lam)) pat-lam-injective (cs ≟-Clauses cs′ ×-dec args ≟-Args args′)
pi t₁ t₂   ≟ pi t₁′ t₂′   =
  Dec.map′ (uncurry (cong₂ pi))  pi-injective (t₁ ≟-ArgType t₁′  ×-dec t₂ ≟-AbsType t₂′)
sort s     ≟ sort s′      = Dec.map′ (cong sort)  sort-injective (s ≟-Sort s′)
lit l      ≟ lit l′       = Dec.map′ (cong lit)   lit-injective (l Literal.≟ l′)
unknown    ≟ unknown      = yes refl

var x args ≟ con c args′ = no λ()
var x args ≟ def f args′ = no λ()
var x args ≟ lam v t     = no λ()
var x args ≟ pi t₁ t₂    = no λ()
var x args ≟ sort _      = no λ()
var x args ≟ lit _      = no λ()
var x args ≟ meta _ _    = no λ()
var x args ≟ unknown     = no λ()
con c args ≟ var x args′ = no λ()
con c args ≟ def f args′ = no λ()
con c args ≟ lam v t     = no λ()
con c args ≟ pi t₁ t₂    = no λ()
con c args ≟ sort _      = no λ()
con c args ≟ lit _      = no λ()
con c args ≟ meta _ _    = no λ()
con c args ≟ unknown     = no λ()
def f args ≟ var x args′ = no λ()
def f args ≟ con c args′ = no λ()
def f args ≟ lam v t     = no λ()
def f args ≟ pi t₁ t₂    = no λ()
def f args ≟ sort _      = no λ()
def f args ≟ lit _      = no λ()
def f args ≟ meta _ _    = no λ()
def f args ≟ unknown     = no λ()
lam v t    ≟ var x args  = no λ()
lam v t    ≟ con c args  = no λ()
lam v t    ≟ def f args  = no λ()
lam v t    ≟ pi t₁ t₂    = no λ()
lam v t    ≟ sort _      = no λ()
lam v t    ≟ lit _      = no λ()
lam v t    ≟ meta _ _    = no λ()
lam v t    ≟ unknown     = no λ()
pi t₁ t₂   ≟ var x args  = no λ()
pi t₁ t₂   ≟ con c args  = no λ()
pi t₁ t₂   ≟ def f args  = no λ()
pi t₁ t₂   ≟ lam v t     = no λ()
pi t₁ t₂   ≟ sort _      = no λ()
pi t₁ t₂   ≟ lit _      = no λ()
pi t₁ t₂   ≟ meta _ _    = no λ()
pi t₁ t₂   ≟ unknown     = no λ()
sort _     ≟ var x args  = no λ()
sort _     ≟ con c args  = no λ()
sort _     ≟ def f args  = no λ()
sort _     ≟ lam v t     = no λ()
sort _     ≟ pi t₁ t₂    = no λ()
sort _     ≟ lit _       = no λ()
sort _     ≟ meta _ _    = no λ()
sort _     ≟ unknown     = no λ()
lit _     ≟ var x args  = no λ()
lit _     ≟ con c args  = no λ()
lit _     ≟ def f args  = no λ()
lit _     ≟ lam v t     = no λ()
lit _     ≟ pi t₁ t₂    = no λ()
lit _     ≟ sort _      = no λ()
lit _     ≟ meta _ _    = no λ()
lit _     ≟ unknown     = no λ()
meta _ _   ≟ var x args  = no λ()
meta _ _   ≟ con c args  = no λ()
meta _ _   ≟ def f args  = no λ()
meta _ _   ≟ lam v t     = no λ()
meta _ _   ≟ pi t₁ t₂    = no λ()
meta _ _   ≟ sort _      = no λ()
meta _ _   ≟ lit _       = no λ()
meta _ _   ≟ unknown     = no λ()
unknown    ≟ var x args  = no λ()
unknown    ≟ con c args  = no λ()
unknown    ≟ def f args  = no λ()
unknown    ≟ lam v t     = no λ()
unknown    ≟ pi t₁ t₂    = no λ()
unknown    ≟ sort _      = no λ()
unknown    ≟ lit _       = no λ()
unknown    ≟ meta _ _    = no λ()
pat-lam _ _ ≟ var x args  = no λ()
pat-lam _ _ ≟ con c args  = no λ()
pat-lam _ _ ≟ def f args  = no λ()
pat-lam _ _ ≟ lam v t     = no λ()
pat-lam _ _ ≟ pi t₁ t₂    = no λ()
pat-lam _ _ ≟ sort _      = no λ()
pat-lam _ _ ≟ lit _       = no λ()
pat-lam _ _ ≟ meta _ _    = no λ()
pat-lam _ _ ≟ unknown     = no λ()
var x args  ≟ pat-lam _ _ = no λ()
con c args  ≟ pat-lam _ _ = no λ()
def f args  ≟ pat-lam _ _ = no λ()
lam v t     ≟ pat-lam _ _ = no λ()
pi t₁ t₂    ≟ pat-lam _ _ = no λ()
sort _      ≟ pat-lam _ _ = no λ()
lit _       ≟ pat-lam _ _ = no λ()
meta _ _    ≟ pat-lam _ _ = no λ()
unknown     ≟ pat-lam _ _ = no λ()

set t   ≟-Sort set t′  = Dec.map′ (cong set) set-injective (t ≟ t′)
lit n   ≟-Sort lit n′  = Dec.map′ (cong lit) slit-injective (n ℕ.≟ n′)
unknown ≟-Sort unknown = yes refl
set _   ≟-Sort lit _   = no λ()
set _   ≟-Sort unknown = no λ()
lit _   ≟-Sort set _   = no λ()
lit _   ≟-Sort unknown = no λ()
unknown ≟-Sort set _   = no λ()
unknown ≟-Sort lit _   = no λ()


text:
module Category where

open import Logic.Equivalence
open import Logic.Relations

open Equivalence using () renaming (_==_ to eq)

record Cat : Set2 where
  field
    Obj     : Set1
    _─→_    : Obj -> Obj -> Set
    id      : {A : Obj} -> A ─→ A
    _∘_     : {A B C : Obj} -> B ─→ C -> A ─→ B -> A ─→ C
    Eq      : {A B : Obj} -> Equivalence (A ─→ B)
    cong    : {A B C : Obj}{f₁ f₂ : B ─→ C}{g₁ g₂ : A ─→ B} ->
              eq Eq f₁ f₂ -> eq Eq g₁ g₂ -> eq Eq (f₁ ∘ g₁) (f₂ ∘ g₂)
    idLeft  : {A B : Obj}{f : A ─→ B} -> eq Eq (id ∘ f) f
    idRight : {A B : Obj}{f : A ─→ B} -> eq Eq (f ∘ id) f
    assoc   : {A B C D : Obj}{f : C ─→ D}{g : B ─→ C}{h : A ─→ B} ->
              eq Eq ((f ∘ g) ∘ h) (f ∘ (g ∘ h))

module Category (ℂ : Cat) where

  private module CC = Cat ℂ
  open CC public hiding (_─→_; _∘_)

  private module Eq {A B : Obj} = Equivalence (Eq {A}{B})
  open Eq public hiding (_==_)

  infix	 20 _==_
  infixr 30 _─→_
  infixr 90 _∘_

  _─→_ = CC._─→_

  _==_ : {A B : Obj} -> Rel (A ─→ B)
  _==_ = Eq._==_

  _∘_ : {A B C : Obj} -> B ─→ C -> A ─→ B -> A ─→ C
  _∘_ = CC._∘_

  congL : {A B C : Obj}{f₁ f₂ : B ─→ C}{g : A ─→ B} ->
	  f₁ == f₂ -> f₁ ∘ g == f₂ ∘ g
  congL p = cong p (refl _)

  congR : {A B C : Obj}{f : B ─→ C}{g₁ g₂ : A ─→ B} ->
	  g₁ == g₂ -> f ∘ g₁ == f ∘ g₂
  congR p = cong (refl _) p

module Poly-Cat where

  infix  20 _==_
  infixr 30 _─→_ _─→'_
  infixr 90 _∘_

  private module C = Category

  -- Objects
  data Obj (ℂ : Cat) : Set1 where
--     obj : C.Obj ℂ -> Obj ℂ

--   obj⁻¹ : {ℂ : Cat} -> Obj ℂ -> C.Obj ℂ
--   obj⁻¹ {ℂ} (obj A) = A

  postulate X : Set

  -- Arrows
  data _─→_ {ℂ : Cat}(A B : Obj ℂ) : Set where
    arr : X -> A ─→ B -- C._─→_ ℂ (obj⁻¹ A) (obj⁻¹ B) -> A ─→ B

  postulate
    ℂ : Cat
    A : Obj ℂ
    B : Obj ℂ

  foo : A ─→ B -> X
  foo (arr f) = ?

--   arr⁻¹ : {ℂ : Cat}{A B : Obj ℂ} -> A ─→ B -> C._─→_ ℂ (obj⁻¹ A) (obj⁻¹ B)
--   arr⁻¹ {ℂ}{A}{B} (arr f) = f

open Poly-Cat
open Category hiding (Obj; _─→_)

{-
  id : {ℂ : Cat}{A : Obj ℂ} -> A ─→ A
  id {ℂ} = arr (Pr.id ℂ)

  _∘_ : {ℂ : Cat}{A B C : Obj ℂ} -> B ─→ C -> A ─→ B -> A ─→ C
  _∘_ {ℂ} (arr f) (arr g) = arr (Pr.compose ℂ f g)

  data _==_ {ℂ : Cat}{A B : Obj ℂ}(f g : A ─→ B) : Set where
    eqArr : Pr.equal ℂ (arr⁻¹ f) (arr⁻¹ g) -> f == g

  refl : {ℂ : Cat}{A B : Obj ℂ}{f : A ─→ B} -> f == f
  refl {ℂ} = eqArr (Pr.refl ℂ)

  sym : {ℂ : Cat}{A B : Obj ℂ}{f g : A ─→ B} -> f == g -> g == f
  sym {ℂ} (eqArr fg) = eqArr (Pr.sym ℂ fg)

  trans : {ℂ : Cat}{A B : Obj ℂ}{f g h : A ─→ B} -> f == g -> g == h -> f == h
  trans {ℂ} (eqArr fg) (eqArr gh) = eqArr (Pr.trans ℂ fg gh)

  cong : {ℂ : Cat}{A B C : Obj ℂ}{f₁ f₂ : B ─→ C}{g₁ g₂ : A ─→ B} ->
	 f₁ == f₂ -> g₁ == g₂ -> f₁ ∘ g₁ == f₂ ∘ g₂
  cong {ℂ} {f₁ = arr _}{f₂ = arr _}{g₁ = arr _}{g₂ = arr _}
	   (eqArr p) (eqArr q) = eqArr (Pr.cong ℂ p q)

  congL : {ℂ : Cat}{A B C : Obj ℂ}{f₁ f₂ : B ─→ C}{g : A ─→ B} ->
	  f₁ == f₂ -> f₁ ∘ g == f₂ ∘ g
  congL p = cong p refl

  congR : {ℂ : Cat}{A B C : Obj ℂ}{f : B ─→ C}{g₁ g₂ : A ─→ B} ->
	  g₁ == g₂ -> f ∘ g₁ == f ∘ g₂
  congR q = cong refl q

  Eq : {ℂ : Cat}{A B : Obj ℂ} -> Equivalence (A ─→ B)
  Eq = equiv _==_ (\x -> refl) (\x y -> sym) (\x y z -> trans)

  idL : {ℂ : Cat}{A B : Obj ℂ}{f : A ─→ B} -> id ∘ f == f
  idL {ℂ}{f = arr _} = eqArr (Pr.idL ℂ)

  idR : {ℂ : Cat}{A B : Obj ℂ}{f : A ─→ B} -> f ∘ id == f
  idR {ℂ}{f = arr _} = eqArr (Pr.idR ℂ)

  assoc : {ℂ : Cat}{A B C D : Obj ℂ}{f : C ─→ D}{g : B ─→ C}{h : A ─→ B} ->
	  (f ∘ g) ∘ h == f ∘ (g ∘ h)
  assoc {ℂ}{f = arr _}{g = arr _}{h = arr _} = eqArr (Pr.assoc ℂ)
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Primitive

data Unit : Set where unit : Unit

record Container a : Set (lsuc a) where
  constructor _◁_
  field
    Shape : Set a
    Pos   : Shape → Set a
open Container public

data Free {a : Level} (C : Container a) (A : Unit → Set a) : Set a where
  pure : A unit                                 → Free C A
  impure : (s : Shape C) → (Pos C s → Free C A) → Free C A

ROp : ∀ a → Container (lsuc a)
ROp a = Set a ◁ λ x → x

rop : {a : Level} {A : Unit → Set a} → Free (ROp a) A
rop {_} {A} = impure (A unit) pure

rop′ : {a : Level} {A : Unit → Set (lsuc a)} → Free (ROp a) A
rop′ {a} {A} = rop {a} -- This should not work, A : Set (suc a) is too large.
                       -- Passing it as an implicit parameter {A} gives the expected error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module Prelude.List.Relations.All where

open import Prelude.Equality
open import Prelude.Nat
open import Prelude.Empty
open import Prelude.Unit
open import Prelude.Product
open import Prelude.Number
open import Prelude.List.Base

open import Prelude.Applicative

open import Agda.Primitive

infixr 5 _∷_
data All {a b} {A : Set a} (P : A → Set b) : List A → Set (a ⊔ b) where
  []  : All P []
  _∷_ : ∀ {x xs} (p : P x) (ps : All P xs) → All P (x ∷ xs)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

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

module Data.Rational.Base where

open import Function using (id)
open import Data.Integer as ℤ using (ℤ; ∣_∣; +_; -[1+_])
open import Data.Nat.GCD
open import Data.Nat.Divisibility as ℕDiv using (divides; 0∣⇒≡0)
open import Data.Nat.Coprimality as C using (Coprime; Bézout-coprime)
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Data.Product
open import Level using (0ℓ)
open import Relation.Nullary.Decidable using (False)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Rel)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; subst; cong; cong₂; module ≡-Reasoning)

open ≡-Reasoning

------------------------------------------------------------------------
-- Rational numbers in reduced form. Note that there is exactly one
-- way to represent every rational number.

record ℚ : Set where
  constructor mkℚ
  field
    numerator     : ℤ
    denominator-1 : ℕ
    .isCoprime    : Coprime ∣ numerator ∣ (suc denominator-1)

  denominatorℕ : ℕ
  denominatorℕ = suc denominator-1

  denominator : ℤ
  denominator = + denominatorℕ

open ℚ public using ()
  renaming
  ( numerator    to ↥_
  ; denominator  to ↧_
  ; denominatorℕ to ↧ₙ_
  )

------------------------------------------------------------------------
-- Equality of rational numbers (coincides with _≡_)

infix 4 _≃_

_≃_ : Rel ℚ 0ℓ
p ≃ q = (↥ p ℤ.* ↧ q) ≡ (↥ q ℤ.* ↧ p)

------------------------------------------------------------------------
-- Ordering of rationals

infix 4 _≤_

data _≤_ : Rel ℚ 0ℓ where
  *≤* : ∀ {p q} → (↥ p ℤ.* ↧ q) ℤ.≤ (↥ q ℤ.* ↧ p) → p ≤ q

------------------------------------------------------------------------
-- Negation

pattern +0       = + 0
pattern +[1+_] n = + suc n

-_ : ℚ → ℚ
- mkℚ -[1+ n ] d prf = mkℚ +[1+ n ] d prf
- mkℚ +0       d prf = mkℚ +0       d prf
- mkℚ +[1+ n ] d prf = mkℚ -[1+ n ] d prf

------------------------------------------------------------------------
-- Constructing rationals

infix 4 _≢0
_≢0 : ℕ → Set
n ≢0 = False (n ℕ.≟ 0)

-- A constructor for ℚ that takes two natural numbers, say 6 and 21,
-- and returns them in a normalized form, e.g. say 2 and 7

normalize : ∀ m n .{m≢0 : m ≢0} .{n≢0 : n ≢0} → ℚ
normalize (suc m) (suc n) with gcd (suc m) (suc n)
... | zero  , GCD.is (1+m∣0 , _) _ = contradiction (0∣⇒≡0 1+m∣0) λ()
... | suc g , G@(GCD.is (divides (suc p) refl , divides (suc q) refl) _)
  = mkℚ (+ suc p) q (Bézout-coprime (Bézout.identity G))

-- A constructor for ℚ that (unlike mkℚ) automatically normalises it's
-- arguments. See the constants section below for how to use this operator.

infixl 7 _/_

_/_ : (n : ℤ) (d : ℕ) → .{d≢0 : d ≢0} → ℚ
_/_ +0       d {d≢0} = mkℚ +0 0 (C.sym (C.1-coprimeTo 0))
_/_ +[1+ n ] d {d≢0} =   normalize (suc n) d {_} {d≢0}
_/_ -[1+ n ] d {d≢0} = - normalize (suc n) d {_} {d≢0}

------------------------------------------------------------------------------
-- Some constants

0ℚ : ℚ
0ℚ = + 0 / 1

1ℚ : ℚ
1ℚ = + 1 / 1

½ : ℚ
½ = + 1 / 2

-½ : ℚ
-½ = - ½

------------------------------------------------------------------------------
-- Operations on rationals

infix  8 -_ 1/_
infixl 7 _*_ _÷_
infixl 6 _-_ _+_

-- addition

_+_ : ℚ → ℚ → ℚ
p + q = (↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)

-- multiplication

_*_ : ℚ → ℚ → ℚ
p * q = (↥ p ℤ.* ↥ q) / (↧ₙ p ℕ.* ↧ₙ q)

-- subtraction

_-_ : ℚ → ℚ → ℚ
p - q = p + (- q)

-- reciprocal: requires a proof that the numerator is not zero

1/_ : (p : ℚ) → .{n≢0 : ∣ ↥ p ∣ ≢0} → ℚ
1/ mkℚ +[1+ n ] d prf = mkℚ +[1+ d ] n (C.sym prf)
1/ mkℚ -[1+ n ] d prf = mkℚ -[1+ d ] n (C.sym prf)

-- division: requires a proof that the denominator is not zero

_÷_ : (p q : ℚ) → .{n≢0 : ∣ ↥ q ∣ ≢0} → ℚ
(p ÷ q) {n≢0} = p * (1/_ q {n≢0})


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Ring.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring.Base

private
  variable
    ℓ : Level

{-
  some basic calculations (used for example in QuotientRing.agda),
  that should become obsolete or subject to change once we have a
  ring solver (see https://github.com/agda/cubical/issues/297)
-}
module Theory (R' : Ring {ℓ}) where

  open RingStr (snd R')
  private R = ⟨ R' ⟩
  implicitInverse : (x y : R)
                 → x + y ≡ 0r
                 → y ≡ - x
  implicitInverse x y p =
    y               ≡⟨ sym (+-lid y) ⟩
    0r + y          ≡⟨ cong (λ u → u + y) (sym (+-linv x)) ⟩
    (- x + x) + y   ≡⟨ sym (+-assoc _ _ _) ⟩
    (- x) + (x + y) ≡⟨ cong (λ u → (- x) + u) p ⟩
    (- x) + 0r      ≡⟨ +-rid _ ⟩
    - x             ∎

  equalByDifference : (x y : R)
                      → x - y ≡ 0r
                      → x ≡ y
  equalByDifference x y p =
    x               ≡⟨ sym (+-rid _) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+-linv y)) ⟩
    x + ((- y) + y) ≡⟨ +-assoc _ _ _ ⟩
    (x - y) + y     ≡⟨ cong (λ u → u + y) p ⟩
    0r + y          ≡⟨ +-lid _ ⟩
    y               ∎

  0-selfinverse : - 0r ≡ 0r
  0-selfinverse = sym (implicitInverse _ _ (+-rid 0r))

  0-idempotent : 0r + 0r ≡ 0r
  0-idempotent = +-lid 0r

  +-idempotency→0 : (x : R) → x ≡ x + x → x ≡ 0r
  +-idempotency→0 x p =
    x               ≡⟨ sym (+-rid x) ⟩
    x + 0r          ≡⟨ cong (λ u → x + u) (sym (+-rinv _)) ⟩
    x + (x + (- x)) ≡⟨ +-assoc _ _ _ ⟩
    (x + x) + (- x) ≡⟨ cong (λ u → u + (- x)) (sym p) ⟩
    x + (- x)       ≡⟨ +-rinv _ ⟩
    0r              ∎

  0-rightNullifies : (x : R) → x · 0r ≡ 0r
  0-rightNullifies x =
              let x·0-is-idempotent : x · 0r ≡ x · 0r + x · 0r
                  x·0-is-idempotent =
                    x · 0r               ≡⟨ cong (λ u → x · u) (sym 0-idempotent) ⟩
                    x · (0r + 0r)        ≡⟨ ·-rdist-+ _ _ _ ⟩
                    (x · 0r) + (x · 0r)  ∎
              in (+-idempotency→0 _ x·0-is-idempotent)

  0-leftNullifies : (x : R) → 0r · x ≡ 0r
  0-leftNullifies x =
              let 0·x-is-idempotent : 0r · x ≡ 0r · x + 0r · x
                  0·x-is-idempotent =
                    0r · x               ≡⟨ cong (λ u → u · x) (sym 0-idempotent) ⟩
                    (0r + 0r) · x        ≡⟨ ·-ldist-+ _ _ _ ⟩
                    (0r · x) + (0r · x)  ∎
              in +-idempotency→0 _ 0·x-is-idempotent

  -commutesWithRight-· : (x y : R) →  x · (- y) ≡ - (x · y)
  -commutesWithRight-· x y = implicitInverse (x · y) (x · (- y))

                               (x · y + x · (- y)     ≡⟨ sym (·-rdist-+ _ _ _) ⟩
                               x · (y + (- y))        ≡⟨ cong (λ u → x · u) (+-rinv y) ⟩
                               x · 0r                 ≡⟨ 0-rightNullifies x ⟩
                               0r ∎)

  -commutesWithLeft-· : (x y : R) →  (- x) · y ≡ - (x · y)
  -commutesWithLeft-· x y = implicitInverse (x · y) ((- x) · y)

                              (x · y + (- x) · y     ≡⟨ sym (·-ldist-+ _ _ _) ⟩
                              (x - x) · y            ≡⟨ cong (λ u → u · y) (+-rinv x) ⟩
                              0r · y                 ≡⟨ 0-leftNullifies y ⟩
                              0r ∎)

  -isDistributive : (x y : R) → (- x) + (- y) ≡ - (x + y)
  -isDistributive x y =
    implicitInverse _ _
         ((x + y) + ((- x) + (- y)) ≡⟨ sym (+-assoc _ _ _) ⟩
          x + (y + ((- x) + (- y))) ≡⟨ cong
                                         (λ u → x + (y + u))
                                         (+-comm _ _) ⟩
          x + (y + ((- y) + (- x))) ≡⟨ cong (λ u → x + u) (+-assoc _ _ _) ⟩
          x + ((y + (- y)) + (- x)) ≡⟨ cong (λ u → x + (u + (- x)))
                                            (+-rinv _) ⟩
          x + (0r + (- x))           ≡⟨ cong (λ u → x + u) (+-lid _) ⟩
          x + (- x)                 ≡⟨ +-rinv _ ⟩
          0r ∎)

  translatedDifference : (x a b : R) → a - b ≡ (x + a) - (x + b)
  translatedDifference x a b =
              a - b                       ≡⟨ cong (λ u → a + u)
                                                  (sym (+-lid _)) ⟩
              (a + (0r + (- b)))          ≡⟨ cong (λ u → a + (u + (- b)))
                                                  (sym (+-rinv _)) ⟩
              (a + ((x + (- x)) + (- b))) ≡⟨ cong (λ u → a + u)
                                                  (sym (+-assoc _ _ _)) ⟩
              (a + (x + ((- x) + (- b)))) ≡⟨ (+-assoc _ _ _) ⟩
              ((a + x) + ((- x) + (- b))) ≡⟨ cong (λ u → u + ((- x) + (- b)))
                                                  (+-comm _ _) ⟩
              ((x + a) + ((- x) + (- b))) ≡⟨ cong (λ u → (x + a) + u)
                                                  (-isDistributive _ _) ⟩
              ((x + a) - (x + b)) ∎

  +-assoc-comm1 : (x y z : R) → x + (y + z) ≡ y + (x + z)
  +-assoc-comm1 x y z = +-assoc x y z ∙∙ cong (λ x → x + z) (+-comm x y) ∙∙ sym (+-assoc y x z)

  +-assoc-comm2 : (x y z : R) → x + (y + z) ≡ z + (y + x)
  +-assoc-comm2 x y z = +-assoc-comm1 x y z ∙∙ cong (λ x → y + x) (+-comm x z) ∙∙ +-assoc-comm1 y z x

module HomTheory {R S : Ring {ℓ}} (f′ : RingHom  R S) where
  open Theory ⦃...⦄
  open RingStr ⦃...⦄
  open RingHom f′
  private
    instance
      _ = R
      _ = S
      _ = snd R
      _ = snd S

  homPres0 : f 0r ≡ 0r
  homPres0 = +-idempotency→0 (f 0r)
               (f 0r        ≡⟨ sym (cong f 0-idempotent) ⟩
                f (0r + 0r) ≡⟨ isHom+ _ _ ⟩
                f 0r + f 0r ∎)

  -commutesWithHom : (x : ⟨ R ⟩) → f (- x) ≡ - (f x)
  -commutesWithHom x = implicitInverse _ _
                         (f x + f (- x)   ≡⟨ sym (isHom+ _ _) ⟩
                          f (x + (- x))   ≡⟨ cong f (+-rinv x) ⟩
                          f 0r            ≡⟨ homPres0 ⟩
                          0r ∎)

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
-- Andreas, 2017-01-12, issue #2386

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

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

{-# BUILTIN EQUALITY Eq #-}

-- Should be accepted.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

data ⊤ : Set where
  tt : ⊤

data _≡_ (a : ⊤) : {B : Set} → B → Set where
  refl : a ≡ a

foo : ⊤
foo = (λ (z : ⊤) (q : bar ≡ {!!}) → tt) bar refl
  where
    bar : ⊤
    bar = {!!}

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed W-types aka Petersson-Synek trees
------------------------------------------------------------------------

module Data.W.Indexed where

open import Level
open import Data.Container.Indexed.Core
open import Data.Product
open import Relation.Unary

-- The family of indexed W-types.

module _ {ℓ c r} {O : Set ℓ} (C : Container O O c r) where

  open Container C

  data W (o : O) : Set (ℓ ⊔ c ⊔ r) where
    sup : ⟦ C ⟧ W o → W o

  -- Projections.

  head : W ⊆ Command
  head (sup (c , _)) = c

  tail : ∀ {o} (w : W o) (r : Response (head w)) → W (next (head w) r)
  tail (sup (_ , k)) r = k r

  -- Induction, (primitive) recursion and iteration.

  ind : ∀ {ℓ} (P : Pred (Σ O W) ℓ) →
        (∀ {o} (cs : ⟦ C ⟧ W o) → □ C P (o , cs) → P (o , sup cs)) →
        ∀ {o} (w : W o) → P (o , w)
  ind P φ (sup (c , k)) = φ (c , k) (λ r → ind P φ (k r))

  rec : ∀ {ℓ} {X : Pred O ℓ} → (⟦ C ⟧ (W ∩ X) ⊆ X) → W ⊆ X
  rec φ (sup (c , k))= φ (c , λ r → (k r , rec φ (k r)))

  iter : ∀ {ℓ} {X : Pred O ℓ} → (⟦ C ⟧ X ⊆ X) → W ⊆ X
  iter φ (sup (c , k))= φ (c , λ r → iter φ (k r))


text:
module SystemF.Syntax.Type.Constructors where

open import Prelude
open import SystemF.Syntax.Type
open import SystemF.Substitutions.Types

-- church numerals
tnat : Type 0
tnat = ∀' (((tvar zero) →' (tvar zero)) →' (tvar zero) →' (tvar zero))

-- Type of the polymorphic identity
tid' : ∀ {n} → Type n
tid' = ∀' ((tvar zero) →' (tvar zero))

-- Top/terminal/unit type
⊤' : ∀ {n} → Type n
⊤' = tid'

-- Bottom/initial/zero type
⊥' : ∀ {n} → Type n
⊥' = ∀' (tvar zero)

-- n-ary function type
infixr 7 _→ⁿ_
_→ⁿ_ : ∀ {n k} → Vec (Type n) k → Type n → Type n
[]       →ⁿ z = z
(a ∷ as) →ⁿ z = as →ⁿ a →' z

-- Record/finite tuple
rec : ∀ {n k} → Vec (Type n) k → Type n
rec []       = ⊤'
rec (a ∷ as) = ∀' ((map tp-weaken (a ∷ as) →ⁿ tvar zero) →' tvar zero)

-- tuple
_×'_ : ∀ {n} → Type n → Type n → Type n
a ×' b = rec (a ∷ b ∷ [])


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

module Categories.Category.Finite.Fin.Construction.Discrete where

open import Data.Product using (∃; _,_)
open import Data.Nat using (ℕ)
open import Data.Fin
open import Data.Fin.Patterns
open import Function using (case_of_)

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_ ; refl; ≡-≟-identity; ≢-≟-identity)

open import Categories.Category.Finite.Fin
open import Categories.Category

private
  card : ∀ {n} (j k : Fin n) → ℕ
  card {ℕ.suc n} 0F 0F           = 1
  card {ℕ.suc n} 0F (suc k)      = 0
  card {ℕ.suc n} (suc j) 0F      = 0
  card {ℕ.suc n} (suc j) (suc k) = card j k

  id : ∀ {n} (a : Fin n) → Fin (card a a)
  id {ℕ.suc n} 0F      = 0F
  id {ℕ.suc n} (suc a) = id a

  comp : ∀ n {a b c : Fin n} → Fin (card b c) → Fin (card a b) → Fin (card a c)
  comp (ℕ.suc n) {0F} {0F} {0F} f g = 0F
  comp (ℕ.suc n) {suc a} {suc b} {suc c} f g = comp n f g

  assoc : ∀ n {a b c d : Fin n}
            {f : Fin (card a b)} {g : Fin (card b c)} {h : Fin (card c d)} →
            (comp n (comp n h g) f) ≡ comp n h (comp n g f)
  assoc (ℕ.suc n) {0F} {0F} {0F} {0F} {f} {g} {h}             = refl
  assoc (ℕ.suc n) {suc a} {suc b} {suc c} {suc d} {f} {g} {h} = assoc n

  identityˡ : ∀ n {a b : Fin n} {f : Fin (card a b)} → comp n (id b) f ≡ f
  identityˡ (ℕ.suc n) {0F} {0F} {0F}      = refl
  identityˡ (ℕ.suc n) {suc a} {suc b} {f} = identityˡ n

  identityʳ : ∀ n {a b : Fin n} {f : Fin (card a b)} → comp n f (id a) ≡ f
  identityʳ (ℕ.suc n) {0F} {0F} {0F}      = refl
  identityʳ (ℕ.suc n) {suc a} {suc b} {f} = identityʳ n

module _ (n : ℕ) where

  DiscreteShape : FinCatShape
  DiscreteShape = record
    { size     = n
    ; ∣_⇒_∣    = card {n}
    ; hasShape = record
      { id        = id {n} _
      ; _∘_       = comp n
      ; assoc     = assoc n
      ; identityˡ = identityˡ n
      ; identityʳ = identityʳ n
      }
    }

Discrete : ∀ n → Category _ _ _
Discrete n = FinCategory (DiscreteShape n)

module Discrete n = Category (Discrete n)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2016-05-10, issue 1848, reported by Nisse

-- {-# OPTIONS -v tc.lhs.top:20 #-}

data D : Set where
  c : D → D

postulate
  P : D → Set

foo : (x : D) → P x
foo _ = {!!}

-- checked lhs:
--   ps    =  _
--   delta =  (x : D)
--   qs    =  [r(x = VarP (0,"x"))]

-- The unnamed variable is part of the context:

-- Goal: P .x
-- ————————————————————————————————————————————————————————————
-- .x : D

bar : (x : D) → P x
bar (c _) = {!!}

-- WAS:
-- checked lhs:
--   ps    =  _
--   delta =  (_ : D)
--   qs    =  [r(x = ConP Issue1848.D.c ... [r(_ = VarP (0,"_"))])]

-- The unnamed variable is not part of the context:

-- Goal: P (c _)
-- ————————————————————————————————————————————————————————————

-- This can, in more complicated situations, make the goal type harder
-- to understand.

-- NOW:
-- Unnamed variable should be displayed in the context, e.g., as ".x"


text:
open import GGT

-- Throughout the following assume A is a (right) Action
module GGT.Theory
  {a b ℓ₁ ℓ₂}
  (A : Action a b ℓ₁ ℓ₂)
  where

open import Level
open import Relation.Unary hiding (_\\_; _⇒_)
open import Relation.Binary
open import Algebra
open import Data.Product

open Action A renaming (setoid to Ω')
open import Relation.Binary.Reasoning.MultiSetoid
-- open import Relation.Binary.Reasoning.Setoid Ω' would be enough

open Group G renaming (setoid to S)
open import GGT.Group.Structures {a} {ℓ₂} {ℓ₁}
open import GGT.Group.Bundles {a} {ℓ₂} {ℓ₁}
open import Function.Bundles
open import Function.Base using (_on_)

orbitalEq : IsEquivalence _ω_
orbitalEq = record { refl =  r ;
                     sym  =  s ;
                     trans = t } where
  open Setoid Ω' renaming (sym to σ)
  r : Reflexive _ω_
  r {o} = ε , actId o

  s : Symmetric _ω_
  s {x} {y} ( g , x·g≡y ) = (g ⁻¹ , y·g⁻¹≡x) where
    y·g⁻¹≡x = σ x≡y·g⁻¹ where
      x≡y·g⁻¹ = begin⟨ Ω' ⟩
                  x              ≈˘⟨ actId x ⟩
                  x · ε          ≈˘⟨ G-ext (inverseʳ _) ⟩
                  x · (g ∙ g ⁻¹) ≈⟨ actAssoc _ _ _ ⟩
                  x · g · g ⁻¹   ≈⟨ ·-cong (g ⁻¹) x·g≡y ⟩
                  y · g ⁻¹ ∎
  t : Transitive _ω_
  t {x} {y} {z} ( g , x·g≡y ) ( h , y·h≡z ) = ( g ∙ h , x·gh≡z ) where
    x·gh≡z : _
    x·gh≡z = begin⟨ Ω' ⟩
              x · (g ∙ h) ≈⟨ actAssoc _ _ _ ⟩
              x · g · h ≈⟨ ·-cong _ x·g≡y ⟩
              y · h ≈⟨ y·h≡z ⟩
              z ∎

ω≤≋ : _≋_ ⇒ _ω_
ω≤≋ {o} {o'} o≋o' = (ε , oε≋o' ) where
  oε≋o' = begin⟨ Ω' ⟩
            o · ε ≈⟨ actId o ⟩
            o ≈⟨ o≋o' ⟩
            o' ∎

stabIsSubGroup : ∀ (o : Ω) → (stab o) ≤ G
stabIsSubGroup o = record { ε∈ = actId o ;
                            ∙-⁻¹-closed = itis ;
                            r = resp } where
  itis = λ {x} {y} px py → begin⟨ Ω' ⟩
                        (o · (x - y))  ≡⟨⟩
                        o · x ∙ (y ⁻¹) ≈⟨ actAssoc o x (y ⁻¹) ⟩
                        o · x · y ⁻¹ ≈⟨ ·-cong (y ⁻¹) px ⟩
                        o · y ⁻¹  ≈˘⟨ ·-cong (y ⁻¹) py ⟩
                        o · y · y ⁻¹ ≈˘⟨ actAssoc o y (y ⁻¹) ⟩
                        o · (y ∙ y ⁻¹) ≈⟨ G-ext (inverseʳ y) ⟩
                        o · ε ≈⟨ actId o ⟩
                        o ∎
  resp : ∀ {x y : Carrier} → x ≈ y → ((stab o) x) → ((stab o) y)
  resp {x} {y} x~y xfixeso = begin⟨ Ω' ⟩
                               o · y ≈˘⟨ G-ext x~y ⟩
                               o · x ≈⟨ xfixeso ⟩
                               o ∎

Stab : Ω → SubGroup G
Stab o = record { P = stab o;
                  isSubGroup = stabIsSubGroup o}

orbitalCorr : {o : Ω} → Bijection (Stab o \\ G) (Orbit o)
orbitalCorr {o} = record { f = f ;
                           cong = cc ;
                           bijective = inj ,′ surj } where
  open Setoid (Stab o \\ G) renaming (_≈_ to _≈₁_; Carrier to G')
  open Setoid (Orbit o)     renaming (_≈_ to _≈₂_)
  open Setoid S renaming (refl to r)

  f : G' → Σ Ω (o ·G)
  f x = (o · x , ( x , G-ext r))

  cc : f Preserves _≈₁_ ⟶ _≈₂_
  cc {g} {h} g≈₁h = begin⟨ Ω' ⟩  -- f h ≈₂ f g
                      o · g ≈˘⟨ actId (o · g) ⟩
                      o · g · ε ≈˘⟨ G-ext (inverseˡ h) ⟩
                      o · g · (h ⁻¹ ∙ h ) ≈˘⟨ actAssoc o g (h ⁻¹ ∙ h ) ⟩
                      o · (g  ∙ (h ⁻¹ ∙ h )) ≈˘⟨ G-ext (assoc _ _ _) ⟩
                      o · ((g  ∙ h ⁻¹) ∙ h ) ≈⟨ actAssoc _ _ h ⟩
                      o · (g  ∙ h ⁻¹) · h ≈⟨ ·-cong h g≈₁h ⟩
                      -- g≈₁h ⇒ P (g ∙ h ⁻¹) ⇒ (g ∙ h ⁻¹) ∈ Stab o
                      o · h ∎
  inj : _
  -- o · g = o · h ⇒ g ∙ h ⁻¹ ∈ Stab o
  inj {g} {h} fg≈₂fh = begin⟨ Ω' ⟩
                         o · g ∙ h ⁻¹ ≈⟨ actAssoc _ _ _ ⟩
                         o · g · h ⁻¹ ≈⟨ ·-cong _ fg≈₂fh ⟩
                         o · h · h ⁻¹ ≈˘⟨ actAssoc _ _ _ ⟩
                         o · (h ∙ h ⁻¹) ≈⟨ G-ext (inverseʳ h)⟩
                         o · ε ≈⟨ actId o ⟩
                         o ∎

  surj : _
  surj (_ , p) = p

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


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

module Ch1-5 where

open import Data.Product

open import Ch2-1

uniq : ∀ {a b} {A : Set a} {B : Set b}
  → (x : A × B)
  → ((proj₁ x , proj₂ x) ≡ x)
uniq (fst , snd) = refl

ind : ∀ {a b c} {A : Set a} {B : Set b}
  → (C : A × B → Set c)
  → ((x : A) → (y : B) → C (x , y))
  → (p : A × B)
  → C p
ind C c (fst , snd) = c fst snd

-- Definition 1.5.2
Definition-1-5-2 : ∀ {a b c} {A : Set a} {B : Set b}
  → (C : Set c)
  → (f : A → B → C)
  → A × B
  → C
Definition-1-5-2 {_} {_} {_} {A} {B} C f (fst , snd) = f fst snd

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


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

open import Generics.Prelude hiding (lookup; pi; curry)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
import Generics.Helpers as Helpers

open import Relation.Binary.HeterogeneousEquality.Core using (_≅_; refl)

module Generics.Constructions.Cong
  {P I ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {ℓ} A)
  {p}
  where

open HasDesc H

private
  variable
    V       : ExTele P
    i i₁ i₂ : ⟦ I ⟧tel p
    v v₁ v₂ : ⟦ V ⟧tel p

-----------------------
-- Type of congruences

levelCongCon : (C : ConDesc P V I) → Level
levelCongCon (var _) = ℓ
levelCongCon (π {ℓ} _ _ C) = ℓ ⊔ levelCongCon C
levelCongCon (A ⊗ B) = levelIndArg A ℓ ⊔ levelCongCon B

CongCon : (C   : ConDesc P V I)
          (mk₁ : ∀ {i₁} → ⟦ C ⟧Con A′ (p , v₁ , i₁) → ⟦ D ⟧Data A′ (p , i₁))
          (mk₂ : ∀ {i₂} → ⟦ C ⟧Con A′ (p , v₂ , i₂) → ⟦ D ⟧Data A′ (p , i₂))
        → Set (levelCongCon C)
-- If non-inductive arguments are equal
CongCon (π (n , ai) S C) mk₁ mk₂
  = {s₁ : < relevance ai > S _}
    {s₂ : < relevance ai > S _}
  → s₁ ≅ s₂
  → CongCon C (λ x → mk₁ (s₁ , x))
              (λ x → mk₂ (s₂ , x))
-- And inductive arguments  are equal
CongCon (A ⊗ B) mk₁ mk₂
  = {f₁ : ⟦ A ⟧IndArg A′ _}
    {f₂ : ⟦ A ⟧IndArg A′ _}
  → f₁ ≅ f₂
  → CongCon B (λ x → mk₁ (f₁ , x))
              (λ x → mk₂ (f₂ , x))
-- Then applying the constructor to both sets should lead
-- to equal values
CongCon (var f) mk₁ mk₂
  = constr (mk₁ refl) ≅ constr (mk₂ refl)

Cong : ∀ k → Set (levelCongCon (lookupCon D k))
Cong k = CongCon (lookupCon D k) (k ,_) (k ,_)

----------------------
-- Generic congruence

deriveCong : ∀ k → Cong k
deriveCong k = congCon (lookupCon D k)
  where
   congCon : (C : ConDesc P V I)
             {mk : ∀ {i} → ⟦ C ⟧Con A′ (p , v , i) → ⟦ D ⟧Data A′ (p , i)}
           → CongCon C mk mk
   congCon (var f) = refl
   congCon (π ai S C) refl = congCon C
   congCon (A ⊗ B) refl = congCon B

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

module VectorLemmas where

open import Level using (Level)

open import Data.Vec
  using (Vec; tabulate; []; _∷_; lookup; allFin)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import  Data.Vec.Properties
  using (lookup-++-≥; lookup∘tabulate; tabulate-∘; tabulate∘lookup;
     tabulate-allFin)
open import Function using (id;_∘_;flip)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; cong₂; subst; trans; proof-irrelevance; module ≡-Reasoning)
open import Data.Nat using (ℕ; zero; suc; _+_; z≤n; _*_)
open import Data.Nat.Properties.Simple using (+-comm; +-right-identity)
open import Data.Fin using (Fin; zero; suc; inject+; raise; reduce≥)
open import Data.Fin.Properties using (toℕ-injective)

open import Data.Sum using (_⊎_; [_,_]′; inj₁; inj₂) renaming (map to map⊎)

open import SubstLemmas
open import FinNatLemmas
open import FiniteFunctions

------------------------------------------------------------------------------
-- Lemmas about map and tabulate

-- to make things look nicer
_!!_ : ∀ {m} {A : Set} → Vec A m → Fin m → A
v !! i = lookup i v

-- this is actually in Data.Vec.Properties, but over an arbitrary
-- Setoid.  Specialize

map-id : ∀ {a n} {A : Set a} (xs : Vec A n) → mapV id xs ≡ xs
map-id [] = refl
map-id (x ∷ xs) = cong (_∷_ x) (map-id xs)

map-++-commute : ∀ {a b m n} {A : Set a} {B : Set b}
                 (f : B → A) (xs : Vec B m) {ys : Vec B n} →
                 mapV f (xs ++V ys) ≡ mapV f xs ++V mapV f ys
map-++-commute f []       = refl
map-++-commute f (x ∷ xs) = cong (λ z → f x ∷ z) (map-++-commute f  xs)

-- this is too, but is done "point free", this version is more convenient

map-∘ : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c}
        (f : B → C) (g : A → B) → (xs : Vec A n) →
        mapV (f ∘ g) xs ≡ (mapV f ∘ mapV g) xs
map-∘ f g [] = refl
map-∘ f g (x ∷ xs) = cong (_∷_ (f (g x))) (map-∘ f g xs)

-- this looks trivial, why can't I find it?

lookup-map : ∀ {a b} {n : ℕ} {A : Set a} {B : Set b} →
  (i : Fin n) → (f : A → B) →
  (v : Vec A n) → lookup i (mapV f v) ≡ f (lookup i v)
lookup-map {n = 0} () _ _
lookup-map {n = suc n} zero f (x ∷ v) = refl
lookup-map {n = suc n} (suc i) f (x ∷ v) = lookup-map i f v

-- These are 'generalized' lookup into left/right parts of a Vector which
-- does not depend on the values in the Vector at all.

look-left : ∀ {m n} {a b c : Level} {A : Set a} {B : Set b} {C : Set c} →
  (i : Fin m) → (f : A → C) → (g : B → C) → (vm : Vec A m) → (vn : Vec B n) →
  lookup (inject+ n i) (mapV f vm ++V mapV g vn) ≡ f (lookup i vm)
look-left {0} () _ _ _ _
look-left {suc _} zero f g (x ∷ vm) vn = refl
look-left {suc _} (suc i) f g (x ∷ vm) vn = look-left i f g vm vn

look-right : ∀ {m n} {a b c : Level} {A : Set a} {B : Set b} {C : Set c} →
  (i : Fin n) → (f : A → C) → (g : B → C) → (vm : Vec A m) → (vn : Vec B n) →
  lookup (raise m i) (mapV f vm ++V mapV g vn) ≡ g (lookup i vn)
look-right {0} i f g vn vm = lookup-map i g vm
look-right {suc m} {0} () _ _ _ _
look-right {suc m} {suc n} i f g (x ∷ vn) vm = look-right i f g vn vm

-- variant
left!! : ∀ {m n} {C : Set} →
  (i : Fin m) → (f : Fin m → C) → {g : Fin n → C} →
  (tabulate f ++V tabulate g) !! (inject+ n i) ≡ f i
left!! {zero} () _
left!! {suc _} zero f = refl
left!! {suc _} (suc i) f = left!! i (f ∘ suc)

right!! : ∀ {m n} {C : Set} →
  (i : Fin n) → {f : Fin m → C} → (g : Fin n → C) →
  (tabulate f ++V tabulate g) !! (raise m i) ≡ g i
right!! {zero} i g = lookup∘tabulate g i
right!! {suc _} {0} () _
right!! {suc m} {suc _} i g = right!! {m} i g

-- similar to lookup-++-inject+ from library

lookup-++-raise : ∀ {m n} {a : Level} {A : Set a} →
  (vm : Vec A m) (vn : Vec A n) (i : Fin n) →
  lookup (raise m i) (vm ++V vn) ≡ lookup i vn
lookup-++-raise {0} vn vm i =
  begin (lookup i (vn ++V vm)
           ≡⟨ lookup-++-≥ vn vm i z≤n ⟩
         lookup (reduce≥ i z≤n) vm
            ≡⟨ refl ⟩
         lookup i vm ∎)
  where open ≡-Reasoning --
lookup-++-raise {suc m} {0} _ _ ()
lookup-++-raise {suc m} {suc n} (x ∷ vn) vm i = lookup-++-raise vn vm i

-- concat (map (map f) xs) = map f (concat xs)
concat-map : ∀ {a b m n} {A : Set a} {B : Set b} →
  (xs : Vec (Vec A n) m) → (f : A → B) →
  concatV (mapV (mapV f) xs) ≡ mapV f (concatV xs)
concat-map [] f = refl
concat-map (xs ∷ xss) f =
  begin (concatV (mapV (mapV f) (xs ∷ xss))
           ≡⟨ refl ⟩
         concatV (mapV f xs ∷ mapV (mapV f) xss)
           ≡⟨  refl ⟩
         mapV f xs ++V concatV (mapV (mapV f) xss)
           ≡⟨ cong (_++V_ (mapV f xs)) (concat-map xss f) ⟩
         mapV f xs ++V mapV f (concatV xss)
           ≡⟨ sym (map-++-commute f xs) ⟩
         mapV f (xs ++V concatV xss)
           ≡⟨ refl ⟩
         mapV f (concatV (xs ∷ xss)) ∎)
  where open ≡-Reasoning

map-map-map : ∀ {a b c m n} {A : Set a} {B : Set b} {C : Set c} →
  (f  : B → C) → (g : A → Vec B n) → (xs : Vec A m) →
  mapV (mapV f) (mapV g xs) ≡ mapV (mapV f ∘ g) xs
map-map-map f g xss = sym (map-∘ (mapV f) g xss)

splitV+ : ∀ {m n} {a : Level} {A : Set a} {f : Fin (m + n) → A} → Vec A (m + n)
splitV+ {m} {n} {f = f} = tabulate {m} (f ∘ inject+ n) ++V tabulate {n} (f ∘ raise m)

splitVOp+ : ∀ {m} {n} {a : Level} {A : Set a} {f : Fin (n + m) → A} → Vec A (m + n)
splitVOp+ {m} {n} {f = f} = tabulate {m} (f ∘ raise n) ++V tabulate {n} (f ∘ inject+ m)

-- f can be implicit since this is mostly used in equational reasoning, where it can be inferred!
tabulate-split : ∀ {m n} {a : Level} {A : Set a} → {f : Fin (m + n) → A} →
  tabulate {m + n} f ≡ splitV+ {m} {n} {f = f}
tabulate-split {0} = refl
tabulate-split {suc m} {f = f} = cong (_∷_ (f zero)) (tabulate-split {m} {f = f ∘ suc})

lookup-subst : ∀ {m m' n}
  (i : Fin n) (xs : Vec (Fin m) n) (eq : m ≡ m') →
  lookup i (subst (λ s → Vec (Fin s) n) eq xs) ≡
  subst Fin eq (lookup i xs)
lookup-subst i xs refl = refl

-- lookup is associative on Fin vectors
lookupassoc : ∀ {m₁ m₂ m₃ m₄} → (π₁ : Vec (Fin m₂) m₁)
  (π₂ : Vec (Fin m₃) m₂) (π₃ : Vec (Fin m₄) m₃) → (i : Fin m₁) →
  lookup (lookup i π₁) (tabulate (λ j → lookup (lookup j π₂) π₃)) ≡
  lookup (lookup i (tabulate (λ j → lookup (lookup j π₁) π₂))) π₃
lookupassoc π₁ π₂ π₃ i =
  begin (lookup (lookup i π₁) (tabulate (λ j → lookup (lookup j π₂) π₃))
           ≡⟨ lookup∘tabulate (λ j → lookup (lookup j π₂) π₃) (lookup i π₁) ⟩
         lookup (lookup (lookup i π₁) π₂) π₃
           ≡⟨ cong
                (λ x → lookup x π₃)
                (sym (lookup∘tabulate (λ j → lookup (lookup j π₁) π₂) i)) ⟩
         lookup (lookup i (tabulate (λ j → lookup (lookup j π₁) π₂))) π₃ ∎)
  where open ≡-Reasoning

-- This should generalize a lot, but that can be done later
subst-lookup-tabulate-raise : ∀ {m n : ℕ} → (z : Fin n) →
  subst Fin (+-comm n m) (lookup z (tabulate (λ i → subst Fin (+-comm m n) (raise m i)))) ≡
  raise m z
subst-lookup-tabulate-raise {m} {n} z =
 begin (subst Fin (+-comm n m) (lookup z (tabulate (λ i → subst Fin (+-comm m n) (raise m i))))
      ≡⟨ cong (subst Fin (+-comm n m))
             (lookup∘tabulate (λ i → subst Fin (+-comm m n) (raise m i)) z) ⟩
    subst Fin (+-comm n m) (subst Fin (+-comm m n) (raise m z))
      ≡⟨ subst-subst (+-comm n m) (+-comm m n)
                 (proof-irrelevance (sym (+-comm n m)) (+-comm m n)) (raise m z) ⟩
    raise m z
     ∎)
  where open ≡-Reasoning

subst-lookup-tabulate-inject+ : ∀ {m n : ℕ} → (z : Fin m) →
  subst Fin (+-comm n m) (lookup z (tabulate (λ i → subst Fin (+-comm m n) (inject+ n i)))) ≡
  inject+ n z
subst-lookup-tabulate-inject+ {m} {n} z =
 begin (subst Fin (+-comm n m) (lookup z (tabulate (λ i → subst Fin (+-comm m n) (inject+ n i))))
      ≡⟨ cong (subst Fin (+-comm n m))
             (lookup∘tabulate (λ i → subst Fin (+-comm m n) (inject+ n i)) z) ⟩
    subst Fin (+-comm n m) (subst Fin (+-comm m n) (inject+ n z))
      ≡⟨ subst-subst (+-comm n m) (+-comm m n)
                 (proof-irrelevance (sym (+-comm n m)) (+-comm m n)) (inject+ n z) ⟩
    inject+ n z
     ∎)
  where open ≡-Reasoning

-- a kind of inverse for splitAt
unSplit : {m n : ℕ} {A : Set} → (f : Fin (m + n) → A) →
  tabulate {m} (f ∘ (inject+ n)) ++V tabulate {n} (f ∘ (raise m)) ≡ tabulate f
unSplit {0} {n} f = refl
unSplit {suc m} f = cong (λ x → (f zero) ∷ x) (unSplit {m} (f ∘ suc))

-- nested tabulate-lookup
denest-tab-!! : {A B C : Set} {k : ℕ} → (f : B → C) → (g : A → B) → (v : Vec A k) →
    tabulate (λ i → f (tabulate (λ j → g (v !! j)) !! i)) ≡ mapV (f ∘ g) v
denest-tab-!! f g v =
  begin (
    tabulate (λ i → f (tabulate (λ j → g (v !! j)) !! i))
        ≡⟨ tabulate-∘ f (λ i → tabulate (λ j → g (v !! j)) !! i) ⟩
    mapV f (tabulate  (λ i → tabulate (λ j → g (v !! j)) !! i) )
        ≡⟨ cong (mapV f) (tabulate∘lookup (tabulate (λ j → g (v !! j)))) ⟩
    mapV f (tabulate (λ j → g (v !! j)))
        ≡⟨ cong (mapV f) (tabulate-∘ g (flip lookup v)) ⟩
    mapV f (mapV g (tabulate (flip lookup v)))
        ≡⟨ sym (map-∘ f g _) ⟩
    mapV (f ∘ g) (tabulate (flip lookup v))
        ≡⟨ cong (mapV (f ∘ g)) (tabulate∘lookup v) ⟩
    mapV (f ∘ g) v ∎)
  where open ≡-Reasoning

tab++[]≡tab∘̂unite+ : ∀ {m} {A : Set} (f : Fin m → A) (eq : m + 0 ≡ m) →
  tabulate f ++V [] ≡ tabulate (λ j → f (subst Fin eq j))
tab++[]≡tab∘̂unite+ {zero} f eq = refl
tab++[]≡tab∘̂unite+ {suc m} f eq = cong₂ _∷_ (cong f pf₁) pf₂
  where
    pf₁ : zero ≡ subst Fin eq zero
    pf₁ = toℕ-injective (sym (toℕ-invariance zero eq))
    pf₃ : ∀ j → suc (subst Fin (+-right-identity m) j) ≡ subst Fin eq (suc j)
    pf₃ j = toℕ-injective (trans (cong suc (toℕ-invariance j (+-right-identity m)))
                                 (sym (toℕ-invariance (suc j) eq)))
    pf₂ : tabulate (f ∘ suc) ++V [] ≡ tabulate (λ j → f (subst Fin eq (suc j)))
    pf₂ = trans (tab++[]≡tab∘̂unite+ (f ∘ suc) (+-right-identity m))
                (finext (λ j → cong f (pf₃ j)))

-- Move to its own spot later
merge-[,] : {A B C D E : Set} → {h : A → C} → {i : B → D} → {f : C → E}
  → {g : D → E} → (x : A ⊎ B) →
    [ f , g ]′ ( map⊎ h i x ) ≡ [ (f ∘ h) , (g ∘ i) ]′ x
merge-[,] (inj₁ x) = refl
merge-[,] (inj₂ y) = refl

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
import      Lvl
open import Type

module Structure.Logic.Constructive.BoundedPredicate
  {ℓₗ}  {Formula : Type{ℓₗ}}
  {ℓₘₗ} (Proof : Formula → Type{ℓₘₗ})
  {ℓₚ}  {Predicate : Type{ℓₚ}}
  {ℓₒ}  {Domain : Type{ℓₒ}}
  (_$_ : Predicate → (x : Domain) → ∀{B : Domain → Formula} → Proof(B(x)) → Formula)
  where

import      Logic.Predicate as Meta
open import Type.Dependent using (Σ)
open import Type.Properties.Inhabited using (◊)
import      Structure.Logic.Constructive.Propositional as Propositional
open import Syntax.Function

private variable P : Predicate
private variable X Y Q : Formula
private variable x y z : Domain
private variable B : Domain → Formula

-- Rules of universal quantification (for all).
record BoundedUniversal(∀ₗ : (Domain → Formula) → Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    intro : (∀{x} → (bx : Proof(B(x))) → Proof((P $ x) {B} bx)) → Proof(∀ₗ B P)
    elim  : Proof(∀ₗ B P) → ∀{x} → (bx : Proof(B(x))) → Proof((P $ x) {B} bx)
∀ₗ = \ ⦃(Meta.[∃]-intro ▫) : Meta.∃(BoundedUniversal)⦄ → ▫
module ∀ₛ {▫} ⦃ p ⦄ = BoundedUniversal {▫} p

-- Rules of existential quantification (exists).
record BoundedExistential(∃ : (Domain → Formula) → Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    intro : (bx : Proof(B(x))) → Proof((P $ x) {B} bx) → Proof(∃ B P)
    elim  : (∀{x} → (bx : Proof(B(x))) → Proof((P $ x) {B} bx) → Proof(Q)) → (Proof(∃ B P) → Proof(Q))
∃ = \ ⦃(Meta.[∃]-intro ▫) : Meta.∃(BoundedExistential)⦄ → ▫
module ∃ₛ {▫} ⦃ p ⦄ = BoundedExistential {▫} p

record BoundedExistentialWitness(∃ : (Domain → Formula) → Predicate → Formula) : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    witness : Proof(∃ B P) → Domain
    bound   : (p : Proof(∃ B P)) → Proof(B(witness p))
    proof   : (p : Proof(∃ B P)) → Proof((P $ witness p) {B} (bound p))

record Logic : Type{ℓₘₗ Lvl.⊔ Lvl.of(Formula) Lvl.⊔ Lvl.of(Domain) Lvl.⊔ Lvl.of(Predicate)} where
  field
    ⦃ propositional ⦄ : Propositional.Logic(Proof)
    ⦃ universal ⦄     : Meta.∃(BoundedUniversal)
    ⦃ existential ⦄   : Meta.∃(BoundedExistential)

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import HoTT

module groups.Pointed where

infix 60 ⊙[_,_]ᴳˢ ⊙[_,_]ᴳ

record ⊙GroupStructure {i : ULevel} (GEl : Type i) : Type (lsucc i) where
  constructor ⊙[_,_]ᴳˢ
  field
    de⊙ᴳˢ : GroupStructure GEl
    ptᴳˢ : GEl
  open GroupStructure de⊙ᴳˢ public
open ⊙GroupStructure using (de⊙ᴳˢ; ptᴳˢ) public

record ⊙Group (i : ULevel) : Type (lsucc i) where
  constructor ⊙[_,_]ᴳ
  field
    de⊙ᴳ : Group i
    ptᴳ : Group.El de⊙ᴳ
  open Group de⊙ᴳ public
  ⊙exp = Group.exp de⊙ᴳ ptᴳ
open ⊙Group using (de⊙ᴳ; ptᴳ) public

⊙Group₀ = ⊙Group lzero

infix 0 _⊙→ᴳ_
_⊙→ᴳ_ : ∀ {i j} → ⊙Group i → ⊙Group j → Type (lmax i j)
⊙G ⊙→ᴳ ⊙H = Σ (de⊙ᴳ ⊙G →ᴳ de⊙ᴳ ⊙H) (λ φ → GroupHom.f φ (ptᴳ ⊙G) == ptᴳ ⊙H)

infix 30 _⊙≃ᴳ_
_⊙≃ᴳ_ : ∀ {i j} → ⊙Group i → ⊙Group j → Type (lmax i j)
⊙G ⊙≃ᴳ ⊙H = Σ (de⊙ᴳ ⊙G ≃ᴳ de⊙ᴳ ⊙H) (λ φ → GroupIso.f φ (ptᴳ ⊙G) == ptᴳ ⊙H)

infixl 120 _⊙⁻¹ᴳ
_⊙⁻¹ᴳ : ∀ {i j} {⊙G : ⊙Group i} {⊙H : ⊙Group j} → ⊙G ⊙≃ᴳ ⊙H → ⊙H ⊙≃ᴳ ⊙G
_⊙⁻¹ᴳ (iso , iic) = iso ⁻¹ᴳ , ! (equiv-adj (GroupIso.f-equiv iso) iic)

⊙exp-hom : ∀ {i} (⊙G : ⊙Group i)
  → ⊙[ ℤ-group , 1 ]ᴳ ⊙→ᴳ ⊙G
⊙exp-hom ⊙[ G , pt ]ᴳ = exp-hom G pt , idp

is-struct-infinite-cyclic : ∀ {i} {El : Type i} → ⊙GroupStructure El → Type i
is-struct-infinite-cyclic ⊙[ G , g ]ᴳˢ = is-equiv (GroupStructure.exp G g)

is-infinite-cyclic : ∀ {i} → ⊙Group i → Type i
is-infinite-cyclic ⊙[ G , g ]ᴳ =
  is-struct-infinite-cyclic ⊙[ Group.group-struct G , g ]ᴳˢ

isomorphism-preserves-infinite-cyclic : ∀ {i j}
  → {⊙G : ⊙Group i} {⊙H : ⊙Group j} → ⊙G ⊙≃ᴳ ⊙H
  → is-infinite-cyclic ⊙G
  → is-infinite-cyclic ⊙H
isomorphism-preserves-infinite-cyclic
  {⊙G = ⊙[ G , g ]ᴳ} {⊙H = ⊙[ H , h ]ᴳ} (iso , pres-pt) ⊙G-iic =
  is-eq _ (is-equiv.g ⊙G-iic ∘ GroupIso.g iso) to-from from-to
  where
    abstract
      lemma : Group.exp H h ∼ GroupIso.f iso ∘ Group.exp G g
      lemma i = ! $
        GroupIso.f iso (Group.exp G g i)
          =⟨ GroupIso.pres-exp iso g i ⟩
        Group.exp H (GroupIso.f iso g) i
          =⟨ ap (λ x → Group.exp H x i) pres-pt ⟩
        Group.exp H h i
          =∎

      to-from : ∀ x → Group.exp H h (is-equiv.g ⊙G-iic (GroupIso.g iso x)) == x
      to-from x =
        Group.exp H h (is-equiv.g ⊙G-iic (GroupIso.g iso x))
          =⟨ lemma (is-equiv.g ⊙G-iic (GroupIso.g iso x)) ⟩
        GroupIso.f iso (Group.exp G g (is-equiv.g ⊙G-iic (GroupIso.g iso x)))
          =⟨ ap (GroupIso.f iso) (is-equiv.f-g ⊙G-iic (GroupIso.g iso x)) ⟩
        GroupIso.f iso (GroupIso.g iso x)
          =⟨ GroupIso.f-g iso x ⟩
        x
          =∎

      from-to : ∀ i → is-equiv.g ⊙G-iic (GroupIso.g iso (Group.exp H h i)) == i
      from-to i =
        is-equiv.g ⊙G-iic (GroupIso.g iso (Group.exp H h i))
          =⟨ ap (is-equiv.g ⊙G-iic ∘ GroupIso.g iso) (lemma i) ⟩
        is-equiv.g ⊙G-iic (GroupIso.g iso (GroupIso.f iso (Group.exp G g i)))
          =⟨ ap (is-equiv.g ⊙G-iic) (GroupIso.g-f iso (Group.exp G g i)) ⟩
        is-equiv.g ⊙G-iic (Group.exp G g i)
          =⟨ is-equiv.g-f ⊙G-iic i ⟩
        i
          =∎

isomorphism-preserves'-infinite-cyclic : ∀ {i j}
  → {⊙G : ⊙Group i} {⊙H : ⊙Group j} → ⊙G ⊙≃ᴳ ⊙H
  → is-infinite-cyclic ⊙H
  → is-infinite-cyclic ⊙G
isomorphism-preserves'-infinite-cyclic iso iic =
  isomorphism-preserves-infinite-cyclic (iso ⊙⁻¹ᴳ) iic

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
data Nat : Set where
  nohana : Nat
  kibou  : Nat -> Nat

one = kibou nohana
two = kibou one


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

open import HoTT
open import homotopy.EilenbergMacLane1
open import homotopy.EilenbergMacLane

{- Given sequence of groups (Gₙ : n ≥ 1) such that Gₙ is abelian for n > 1,
 - we can construct a space X such that πₙ(X) == Gₙ.
 - (We can also make π₀(X) whatever we want but this isn't done here.) -}

module homotopy.SpaceFromGroups where

{- From a sequence of spaces (Fₙ) such that Fₙ is n-connected and
 - n+1-truncated, construct a space X such that πₙ₊₁(X) == πₙ₊₁(Fₙ) -}
module SpaceFromEMs {i} (F : ℕ → Ptd i)
  {{pF : {n : ℕ} → has-level ⟨ S n ⟩ (de⊙ (F n))}}
  {{cF : (n : ℕ) → is-connected ⟨ n ⟩ (de⊙ (F n))}} where

  X : Ptd i
  X = ⊙FinTuples F

  πS-X : (n : ℕ) → πS n X ≃ᴳ πS n (F n)
  πS-X n =
    πS n (⊙FinTuples F)
      ≃ᴳ⟨ prefix-lemma n O F ⟩
    πS n (⊙FinTuples (λ k → F (n + k)))
      ≃ᴳ⟨ πS-emap n (⊙fin-tuples-cons (λ k → F (n + k))) ⁻¹ᴳ ⟩
    πS n (F (n + O) ⊙× ⊙FinTuples (λ k → F (n + S k)))
      ≃ᴳ⟨ πS-× n (F (n + O)) (⊙FinTuples (λ k → F (n + S k))) ⟩
    πS n (F (n + O)) ×ᴳ πS n (⊙FinTuples (λ k → F (n + S k)))
      ≃ᴳ⟨ ×ᴳ-emap (idiso (πS n (F (n + O))) )
         (contr-iso-0ᴳ _ $
           connected-at-level-is-contr {{⟨⟩}}
             {{Trunc-preserves-conn {n = 0} $ Ω^-conn _ (S n) _ $
               transport
                 (λ k → is-connected k
                          (FinTuples (λ k → F (n + S k))))
                 (+2+-comm 0 ⟨ n ⟩₋₁)
                 (ncolim-conn _ _ {{connected-lemma _ _ (λ k →
                   transport (λ s → is-connected ⟨ s ⟩ (de⊙ (F (n + S k))))
                     (+-βr n k ∙ +-comm (S n) k)
                     (cF (n + S k)))}})}}) ⟩
    πS n (F (n + O)) ×ᴳ 0ᴳ
      ≃ᴳ⟨ ×ᴳ-unit-r _ ⟩
    πS n (F (n + O))
      ≃ᴳ⟨ transportᴳ-iso (λ k → πS n (F k)) (+-unit-r n) ⟩
    πS n (F n)
      ≃ᴳ∎
    where
    {- In computing πₙ₊₁, spaces before Fₙ are ignored because of their
     - truncation level -}
    prefix-lemma : (n : ℕ) (m : ℕ) (F : ℕ → Ptd i)
      {{_ : {k : ℕ} → has-level ⟨ S m + k ⟩ (de⊙ (F k))}}
      → πS (m + n) (⊙FinTuples F)
        ≃ᴳ πS (m + n) (⊙FinTuples (λ k → F (n + k)))
    prefix-lemma O m F = idiso _
    prefix-lemma (S n) m F =
      πS (m + S n) (⊙FinTuples F)
        ≃ᴳ⟨ πS-emap (m + S n) (⊙fin-tuples-cons F) ⁻¹ᴳ ⟩
      πS (m + S n) (F O ⊙× ⊙FinTuples (F ∘ S))
        ≃ᴳ⟨ πS-× (m + S n) (F O) (⊙FinTuples (F ∘ S)) ⟩
      πS (m + S n) (F O) ×ᴳ πS (m + S n) (⊙FinTuples (F ∘ S))
        ≃ᴳ⟨ ×ᴳ-emap lemma₁ lemma₂ ⟩
      0ᴳ ×ᴳ πS (m + S n) (⊙FinTuples (λ k → F (S (n + k))))
        ≃ᴳ⟨ ×ᴳ-unit-l _ ⟩
      πS (m + S n) (⊙FinTuples (λ k → F (S (n + k))))
        ≃ᴳ∎
      where
      {- ignore first space -}
      lemma₁ : πS (m + S n) (F O) ≃ᴳ 0ᴳ
      lemma₁ =
        πS->level-econv (m + S n) _ (F O)
          (⟨⟩-monotone-< (<-ap-S (<-+-l m (O<S n))))

      {- ignore the rest by recursive call -}
      lemma₂ : πS (m + S n) (⊙FinTuples (F ∘ S))
        ≃ᴳ πS (m + S n) (⊙FinTuples (λ k → F (S (n + k))))
      lemma₂ =
        πS (m + S n) (⊙FinTuples (F ∘ S))
          ≃ᴳ⟨ transportᴳ-iso (λ s → πS s (⊙FinTuples (F ∘ S))) (+-βr m n) ⟩
        πS (S m + n) (⊙FinTuples (F ∘ S))
          ≃ᴳ⟨ prefix-lemma n (S m) (F ∘ S)
                {{λ {k} → transport (λ s → has-level ⟨ s ⟩ (de⊙ (F (S k))))
                     (+-βr (S m) k) ⟨⟩}} ⟩
        πS (S m + n) (⊙FinTuples (λ k → F (S (n + k))))
          ≃ᴳ⟨ transportᴳ-iso (λ s → πS s (⊙FinTuples (λ k → F (S (n + k))))) (+-βr m n) ⁻¹ᴳ ⟩
        πS (m + S n) (⊙FinTuples (λ k → F (S (n + k))))
          ≃ᴳ∎

    connected-lemma : (m : ℕ) (F : ℕ → Ptd i)
      (cA' : (n : ℕ) → is-connected ⟨ n + m ⟩ (de⊙ (F n)))
      (n : ℕ) → is-connected ⟨ m ⟩ (FinTuplesType F n)
    connected-lemma m F cA' O =
      Trunc-preserves-level ⟨ m ⟩ ⟨⟩
    connected-lemma m F cA' (S n) = ×-conn
      (cA' O)
      (connected-lemma m (F ∘ S)
        (λ n → connected-≤T (⟨⟩-monotone-≤ (inr ltS)) {{cA' (S n)}}) n)

{- Given sequence of groups (Gₙ : n ≥ 1) such that Gₙ is abelian for n > 1,
 - construct a space X such that πₙ(X) == Gₙ. -}
module SpaceFromGroups {i} (G : ℕ → Group i)
  (abG-S : (n : ℕ) → is-abelian (G (S n))) where

  private
    F : ℕ → Ptd i
    F O = ⊙EM₁ (G O)
    F (S n) = EMExplicit.⊙EM (G (S n) , abG-S n) (S (S n))

    instance
      pF : (n : ℕ) → has-level ⟨ S n ⟩ (de⊙ (F n))
      pF O = EM₁-level {G = G O}
      pF (S n) = EMExplicit.EM-level (G (S n) , abG-S n) (S (S n))

      cF : (n : ℕ) → is-connected ⟨ n ⟩ (de⊙ (F n))
      cF O = EM₁-conn {G = G O}
      cF (S n) = EMExplicit.EM-conn (G (S n) , abG-S n) (S n)

    module M = SpaceFromEMs F

  X = M.X

  πS-X : (n : ℕ) → πS n X ≃ᴳ G n
  πS-X O = π₁-EM₁ (G O) ∘eᴳ M.πS-X O
  πS-X (S n) =
    EMExplicit.πS-diag (G (S n) , abG-S n) (S n) ∘eᴳ M.πS-X (S n)


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

module Examples.OpSem where

open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst)
open import Luau.Syntax using (Block; var; val; nil; local_←_; _∙_; done; return; block_is_end)
open import Luau.Heap using (∅)

ex1 : ∅ ⊢ (local (var "x") ← val nil ∙ return (var "x") ∙ done) ⟶ᴮ (return (val nil) ∙ done) ⊣ ∅
ex1 = subst nil

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau