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

module Luau.ResolveOverloads where

open import FFI.Data.Either using (Left; Right)
open import Luau.Subtyping using (_<:_; _≮:_; Language; witness; scalar; unknown; never; function-ok)
open import Luau.Type using (Type ; _⇒_; _∩_; _∪_; unknown; never)
open import Luau.TypeSaturation using (saturate)
open import Luau.TypeNormalization using (normalize)
open import Properties.Contradiction using (CONTRADICTION)
open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never; <:-∪-left; <:-∪-right)
open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)

-- The domain of a normalized type
srcⁿ : Type → Type
srcⁿ (S ⇒ T) = S
srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
srcⁿ never = unknown
srcⁿ T = never

-- To get the domain of a type, we normalize it first We need to do
-- this, since if we try to use it on non-normalized types, we get
--
-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
-- src(never) = unknown
--
-- so src doesn't respect type equivalence.
src : Type → Type
src (S ⇒ T) = S
src T = srcⁿ(normalize T)

-- Calculate the result of applying a function type `F` to an argument type `V`.
-- We do this by finding an overload of `F` that has the most precise type,
-- that is an overload `(Sʳ ⇒ Tʳ)` where `V <: Sʳ` and moreover
-- for any other such overload `(S ⇒ T)` we have that `Tʳ <: T`.

-- For example if `F` is `(number -> number) & (nil -> nil) & (number? -> number?)`
-- then to resolve `F` with argument type `number`, we pick the `number -> number`
-- overload, but if the argument is `number?`, we pick `number? -> number?`./

-- Not all types have such a most precise overload, but saturated ones do.

data ResolvedTo F G V : Set where

  yes : ∀ Sʳ Tʳ →

    Overloads F (Sʳ ⇒ Tʳ) →
    (V <: Sʳ) →
    (∀ {S T} → Overloads G (S ⇒ T) → (V <: S) → (Tʳ <: T)) →
    --------------------------------------------
    ResolvedTo F G V

  no :

    (∀ {S T} → Overloads G (S ⇒ T) → (V ≮: S)) →
    --------------------------------------------
    ResolvedTo F G V

Resolved : Type → Type → Set
Resolved F V = ResolvedTo F F V

target : ∀ {F V} → Resolved F V → Type
target (yes _ T _ _ _) = T
target (no _) = unknown

-- We can resolve any saturated function type
resolveˢ : ∀ {F G V} → FunType G → Saturated F → Normal V → (G ⊆ᵒ F) → ResolvedTo F G V
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F with dec-subtypingⁿ Vⁿ Sⁿ
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Left V≮:S = no (λ { here → V≮:S })
resolveˢ (Sⁿ ⇒ Tⁿ) (defn sat-∩ sat-∪) Vⁿ G⊆F | Right V<:S = yes _ _ (G⊆F here) V<:S (λ { here _ → <:-refl })
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F with resolveˢ Gᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ left) | resolveˢ Hᶠ (defn sat-∩ sat-∪) Vⁿ (G⊆F ∘ right)
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ with sat-∩ o₁ o₂
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ | defn o p₁ p₂ =
  yes _ _ o (<:-trans (<:-∩-glb V<:S₁ V<:S₂) p₁) (λ { (left o) p → <:-trans p₂ (<:-trans <:-∩-left (tgt₁ o p)) ; (right o) p → <:-trans p₂ (<:-trans <:-∩-right (tgt₂ o p)) })
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | yes S₁ T₁ o₁ V<:S₁ tgt₁ | no src₂ =
  yes _ _ o₁ V<:S₁ (λ { (left o) p → tgt₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (src₂ o)) })
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | yes S₂ T₂ o₂ V<:S₂ tgt₂ =
  yes _ _ o₂ V<:S₂ (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (src₁ o)) ; (right o) p → tgt₂ o p })
resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Vⁿ G⊆F | no src₁ | no src₂ =
  no (λ { (left o) → src₁ o ; (right o) → src₂ o })

-- Which means we can resolve any normalized type, by saturating it first
resolveᶠ : ∀ {F V} → FunType F → Normal V → Type
resolveᶠ Fᶠ Vⁿ = target (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o))

resolveⁿ : ∀ {F V} → Normal F → Normal V → Type
resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Vⁿ
resolveⁿ (Fᶠ ∩ Gᶠ) Vⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Vⁿ
resolveⁿ (Sⁿ ∪ Tˢ) Vⁿ = unknown
resolveⁿ unknown Vⁿ = unknown
resolveⁿ never Vⁿ = never

-- Which means we can resolve any type, by normalizing it first
resolve : Type → Type → Type
resolve F V = resolveⁿ (normal F) (normal V)

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sum combinators for propositional equality preserving functions
------------------------------------------------------------------------

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

module Data.Sum.Function.Propositional where

open import Data.Sum
open import Data.Sum.Function.Setoid
open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡)
open import Function.Equivalence as Eq using (_⇔_; module Equivalence)
open import Function.Injection as Inj using (_↣_; module Injection)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (_↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj using (_↠_; module Surjection)

------------------------------------------------------------------------
-- Combinators for various function types

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where

  _⊎-⇔_ : A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
  _⊎-⇔_ A⇔B C⇔D =
    Inverse.equivalence (Pointwise-≡↔≡ B D) ⟨∘⟩
    (A⇔B ⊎-equivalence C⇔D) ⟨∘⟩
    Eq.sym (Inverse.equivalence (Pointwise-≡↔≡ A C))
    where open Eq using () renaming (_∘_ to _⟨∘⟩_)

  _⊎-↣_ : A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D)
  _⊎-↣_ A↣B C↣D =
    Inverse.injection (Pointwise-≡↔≡ B D) ⟨∘⟩
    (A↣B ⊎-injection C↣D) ⟨∘⟩
    Inverse.injection (Inv.sym (Pointwise-≡↔≡ A C))
    where open Inj using () renaming (_∘_ to _⟨∘⟩_)

  _⊎-↞_ : A ↞ B → C ↞ D → (A ⊎ C) ↞ (B ⊎ D)
  _⊎-↞_ A↞B C↞D =
    Inverse.left-inverse (Pointwise-≡↔≡ B D) ⟨∘⟩
    (A↞B ⊎-left-inverse C↞D) ⟨∘⟩
    Inverse.left-inverse (Inv.sym (Pointwise-≡↔≡ A C))
    where open LeftInv using () renaming (_∘_ to _⟨∘⟩_)

  _⊎-↠_ : A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D)
  _⊎-↠_ A↠B C↠D =
    Inverse.surjection (Pointwise-≡↔≡ B D) ⟨∘⟩
    (A↠B ⊎-surjection C↠D) ⟨∘⟩
    Inverse.surjection (Inv.sym (Pointwise-≡↔≡ A C))
    where open Surj using () renaming (_∘_ to _⟨∘⟩_)

  _⊎-↔_ : A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
  _⊎-↔_ A↔B C↔D =
    Pointwise-≡↔≡ B D ⟨∘⟩
    (A↔B ⊎-inverse C↔D) ⟨∘⟩
    Inv.sym (Pointwise-≡↔≡ A C)
    where open Inv using () renaming (_∘_ to _⟨∘⟩_)

module _ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} where

  _⊎-cong_ : ∀ {k} → A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
  _⊎-cong_ {implication}         = map
  _⊎-cong_ {reverse-implication} = λ f g → lam (map (app-← f) (app-← g))
  _⊎-cong_ {equivalence}         = _⊎-⇔_
  _⊎-cong_ {injection}           = _⊎-↣_
  _⊎-cong_ {reverse-injection}   = λ f g → lam (app-↢ f ⊎-↣ app-↢ g)
  _⊎-cong_ {left-inverse}        = _⊎-↞_
  _⊎-cong_ {surjection}          = _⊎-↠_
  _⊎-cong_ {bijection}           = _⊎-↔_

ext: agda


text:
module product where

open import level
open import unit public

----------------------------------------------------------------------
-- types
----------------------------------------------------------------------

data Σ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  _,_ : (a : A) → (b : B a) → Σ A B

data Σi {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') : Set (ℓ ⊔ ℓ') where
  ,_ : {a : A} → (b : B a) → Σi A B
_×_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A × B = Σ A (λ x → B)

_i×_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
A i× B = Σi A (λ x → B)

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 2 Σ-syntax
infixr 3 _×_ _i×_ _∧_
infixr 4 _,_
infix  4 ,_

-- This provides the syntax: Σ[ x ∈ A ] B it is taken from the Agda
-- standard library. This style is nice when working in Set.
Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------
fst : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A × B → A
fst (a , b) = a

snd : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A × B → B
snd (a , b) = b

trans-× : ∀{ℓ₁ ℓ₂ ℓ₃}
         {A : Set ℓ₁}{B : Set ℓ₂}
         {C : Set ℓ₃}
       → (C → A)
       → (C → B)
       → (C → A × B)
trans-× f g c = f c , g c

⟨_,_⟩ : ∀{ℓ₁ ℓ₂ ℓ₃ ℓ₄}
         {A : Set ℓ₁}{B : Set ℓ₂}
         {C : Set ℓ₃}{D : Set ℓ₄}
       → (A → C)
       → (B → D)
       → (A × B → C × D)
⟨ f , g ⟩ (a , b) = f a , g b

twist-× : ∀{ℓ₁ ℓ₂}
     {A : Set ℓ₁}{B : Set ℓ₂}
    → A × B
    → B × A
twist-× (a , b) = (b , a)

rl-assoc-× : ∀{ℓ₁ ℓ₂ ℓ₃}
             {A : Set ℓ₁}{B : Set ℓ₂}
             {C : Set ℓ₃}
           → A × (B × C)
           → (A × B) × C
rl-assoc-× (a , b , c) =  ((a , b) , c)

lr-assoc-× : ∀{ℓ₁ ℓ₂ ℓ₃}
             {A : Set ℓ₁}{B : Set ℓ₂}
             {C : Set ℓ₃}
           → (A × B) × C
           → A × (B × C)
lr-assoc-× ((a , b) , c) = (a , b , c)

func-× : ∀{ℓ₁ ℓ₂ ℓ₃ ℓ₄}{A : Set ℓ₁}{B : Set ℓ₂}{C : Set ℓ₃}{D : Set ℓ₄} → (A → C) → (B → D) → (A × B) → (C × D)
func-× f g (x , y) = (f x , g y)

×-diag : ∀{ℓ}{X : Set ℓ} → X → X × X
×-diag x = (x , x)

----------------------------------------------------------------------
-- some logical notation
----------------------------------------------------------------------
_∧_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
_∧_ = _×_

∃ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') → Set (ℓ ⊔ ℓ')
∃ = Σ

∃i : ∀ {ℓ ℓ'} (A : Set ℓ) (B : A → Set ℓ') → Set (ℓ ⊔ ℓ')
∃i = Σi

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Common.Nat
open import Common.IO
open import Common.Unit

record Test : Set where
  field
    a b c : Nat

f : Test -> Nat
f r = a + b + c
  where open Test r

open Test

g : Nat
g = (f (record {a = 100; b = 120; c = 140})) + a m + b m + c m
  where m = record {c = 400; a = 200; b = 300}

main : IO Unit
main = printNat g

-- Expected Output: 1260

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import M-types.Base

module M-types.Coalg.Bisim (A : Ty ℓ) (B : A → Ty ℓ) where
    open import M-types.Coalg.Core A B

    TyBisim : Coalg → Ty (ℓ-suc ℓ)
    TyBisim X =
        ∑[ coalg ∈ Coalg ]
        CoalgMor coalg X × CoalgMor coalg X

    coalg = pr₀

    spanRel : {X : Coalg} →
        ∏[ ∼ ∈ TyBisim X ] SpanRel (ty X)
    spanRel (coalg , ρ₀ , ρ₁) = (ty coalg , fun ρ₀ , fun ρ₁)

    tyLift : {X : Coalg} →
        ∏[ ∼ ∈ TyBisim X ] ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        (x₀ ⟨ spanRel {X} ∼ ⟩ x₁ → (obs X x₀) ⟨ P-SpanRel (spanRel {X} ∼) ⟩ (obs X x₁))
    tyLift ∼ x₀ x₁ (s , refl , refl) =
        (
            obs (coalg ∼) s ,
            ≡-apply (com (ρ₀ ∼)⁻¹) s ,
            ≡-apply (com (ρ₁ ∼)⁻¹) s
        )

    ≡-TyBisim : {X : Coalg} →
        TyBisim X
    ≡-TyBisim {X} =
        (
            X ,
            (id , refl) ,
            (id , refl)
        )

    P-TyBisim : {X : Coalg} →
        TyBisim X → TyBisim (P-Coalg X)
    P-TyBisim {X} ∼ =
        (
            P-Coalg (coalg ∼) ,
            P-CoalgMor {coalg ∼} {X} (ρ₀ ∼) ,
            P-CoalgMor {coalg ∼} {X} (ρ₁ ∼)
        )

    TyBisimMor : {X : Coalg} →
        TyBisim X → TyBisim X → Ty ℓ
    TyBisimMor {X} ∼ ≈ =
        ∑[ mor ∈ SpanRelMor (spanRel {X} ∼) (spanRel {X} ≈) ]
        obs (coalg ≈) ∘ fun mor ≡ P-Fun (fun mor) ∘ obs (coalg ∼)

    FunBisim : Coalg → Ty (ℓ-suc ℓ)
    FunBisim X =
        ∑[ depRel ∈ (ty X → ty X → Ty ℓ) ]
        ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        (depRel x₀ x₁ → (P-DepRel depRel) (obs X x₀) (obs X x₁))

    depRel : {X : Coalg} →
        ∏[ ∼ ∈ FunBisim X ] DepRel (ty X)
    depRel = pr₀

    funLift : {X : Coalg} →
        ∏[ ∼ ∈ FunBisim X ] ∏[ d₀ ∈ ty X ] ∏[ d₁ ∈ ty X ]
        (d₀ [ depRel ∼ ] d₁ → (obs X d₀) [ P-DepRel (depRel ∼) ] (obs X d₁))
    funLift = pr₁

    ≡-funLift : {X : Coalg} →
        ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        (≡-depRel x₀ x₁ → P-DepRel ≡-depRel (obs X x₀) (obs X x₁))
    ≡-funLift x x refl = (refl , λ b → refl)

    ≡-funBisim : {X : Coalg} →
        FunBisim X
    ≡-funBisim {X} = (≡-depRel , ≡-funLift)

    P-FunBisim : {X : Coalg} →
        FunBisim X → FunBisim (P-Coalg X)
    P-FunBisim {X} ∼ =
        (
            P-DepRel (depRel ∼) ,
            λ (a₀ , d₀) → λ (a₁ , d₁) → λ (p , e) → (
                p ,
                λ b₀ → pr₁ ∼ (d₀ b₀) (d₁ (tra B p b₀)) (e b₀)
            )
        )

    FunBisimMor : {X : Coalg} →
        FunBisim X → FunBisim X → Ty ℓ
    FunBisimMor {X} ∼ ≈ =
        ∑[ mor ∈ DepRelMor (depRel ∼) (depRel ≈) ]
        ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        funLift ≈ x₀ x₁ ∘ mor x₀ x₁ ≡
        P-DepRelMor mor (obs X x₀) (obs X x₁) ∘ funLift ∼ x₀ x₁

    fun-tra : {a₀ a₁ : A} {C : Ty ℓ} →
        ∏[ p ∈ a₀ ≡ a₁ ] ∏[ f₁ ∈ (B a₁ → C) ]
        tra (λ a → (B a → C)) p (f₁ ∘ (tra B p)) ≡ f₁
    fun-tra refl f₁ = refl

    apply-pr₁ : {X : Coalg} {(a₀ , d₀) (a₁ , d₁) : P (ty X)} →
        ∏[ p ∈ (a₀ , d₀) ≡ (a₁ , d₁) ] ∏[ b₀ ∈ B a₀ ]
        d₀ b₀ ≡ d₁ (tra B (ap pr₀ p) b₀)
    apply-pr₁ refl b = refl

    TyBisim→FunBisim : {X : Coalg} →
        TyBisim X → FunBisim X
    TyBisim→FunBisim {X} ∼ =
        (
            (λ x₀ → λ x₁ → x₀ ⟨ spanRel {X} ∼ ⟩ x₁) ,
            (λ x₀ → λ x₁ → λ {(s , refl , refl) → let
                q₀ :
                    obs X x₀ ≡ (
                        pr₀ (obs (coalg ∼) s) ,
                        fun (ρ₀ ∼) ∘ pr₁ (obs (coalg ∼) s)
                    )
                q₀ = ≡-apply (com (ρ₀ ∼)) s

                q₁ :
                    obs X x₁ ≡ (
                        pr₀ (obs (coalg ∼) s) ,
                        fun (ρ₁ ∼) ∘ pr₁ (obs (coalg ∼) s)
                    )
                q₁ = ≡-apply (com (ρ₁ ∼)) s
            in (
                 (ap pr₀ q₀) · (ap pr₀ q₁) ⁻¹ ,
                 λ b₀ → (
                     pr₁ (obs (coalg ∼) s) (tra B (ap pr₀ q₀) b₀) ,
                     (apply-pr₁ {X} q₀ b₀) ⁻¹ ,
                     (apply-pr₁ {X} (q₁ ⁻¹) (tra B (ap pr₀ q₀) b₀)) ·
                     ap (pr₁ (obs X x₁)) (≡-apply (
                         tra-con B (ap pr₀ q₀) (ap pr₀ (q₁ ⁻¹)) ·
                         ap (λ r → tra B (ap pr₀ q₀ · r)) ((ap-inv pr₀ q₁) ⁻¹)
                     ) b₀)
                 )
            )})
        )

    FunBisim→TyBisim : {X : Coalg} →
        FunBisim X → TyBisim X
    FunBisim→TyBisim {X} ∼ =
        (
            (
                (∑[ x₀ ∈ ty X ] ∑[ x₁ ∈ ty X ] x₀ [ depRel ∼ ] x₁) ,
                λ (x₀ , x₁ , s) → (
                    pr₀ (obs X x₀) ,
                    λ b₀ → (
                        pr₁ (obs X x₀) b₀ ,
                        pr₁ (obs X x₁) (tra B (pr₀ (funLift ∼ x₀ x₁ s)) b₀) ,
                        pr₁ (funLift ∼ x₀ x₁ s) b₀
                    )
                )
            ) , (
                pr₀ ,
                funext (λ (x₀ , x₁ , s) → refl)
            ) , (
                pr₀ ∘ pr₁ ,
                funext (λ (x₀ , x₁ , s) → ≡-pair (
                    pr₀ (funLift ∼ x₀ x₁ s) ,
                    fun-tra (pr₀ (funLift ∼ x₀ x₁ s)) (pr₁ (obs X x₁))
                ) ⁻¹)
            )
        )

    TyBisim→FunBisim-pres : {X : Coalg} →
        ∏[ ∼ ∈ TyBisim X ] ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        (x₀ [ depRel {X} (TyBisim→FunBisim {X} ∼) ] x₁) ≡ (x₀ ⟨ spanRel {X} ∼ ⟩ x₁)
    TyBisim→FunBisim-pres {X} ∼ x₀ x₁ = SpanRel→DepRel-pres (spanRel {X} ∼) x₀ x₁

    FunBisim→TyBisim-pres : {X : Coalg} →
        ∏[ ∼ ∈ FunBisim X ] ∏[ x₀ ∈ ty X ] ∏[ x₁ ∈ ty X ]
        (x₀ ⟨ spanRel {X} (FunBisim→TyBisim {X} ∼) ⟩ x₁) ≃ (x₀ [ depRel {X} ∼ ] x₁)
    FunBisim→TyBisim-pres ∼ x₀ x₁ = DepRel→SpanRel-pres (depRel ∼) x₀ x₁

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module STypeCongruence where

open import Data.Fin

open import DualCoinductive

open import Direction

open COI

-- holes for session types

mutual
  data TypeH : Set where
      TPair-l : TypeH → (T₂ : Type) → TypeH
      TPair-r : (T₁ : Type) → TypeH → TypeH
      TChan   : (sh : STypeH) → TypeH

  data STypeH : Set where
    hole : STypeH
    transmit-s : (d : Dir) (T : Type) (sh : STypeH) → STypeH
    transmit-t : (d : Dir) (th : TypeH) (S : SType) → STypeH

-- apply a hole to a session type

apply-hole-T : TypeH → SType → Type
apply-hole-S : STypeH → SType → SType

apply-hole-T (TPair-l th T₂) S = TPair (apply-hole-T th S) T₂
apply-hole-T (TPair-r T₁ th) S = TPair T₁ (apply-hole-T th S)
apply-hole-T (TChan sh) S = TChan (apply-hole-S sh S)

apply-hole-S hole S = S
apply-hole-S (transmit-s d T sh) S = delay (transmit d T (apply-hole-S sh S))
apply-hole-S (transmit-t d th S₁) S = delay (transmit d (apply-hole-T th S) S₁)

-- test congruences

≈-cong-transmit : ∀ {d t S₁ S₂} → S₁ ≈ S₂ → transmit d t S₁ ≈' transmit d t S₂
≈-cong-transmit S1≈S2 = eq-transmit _ ≈ᵗ-refl S1≈S2

≈-cong-transmit-t : ∀ {d T₁ T₂ S} → T₁ ≈ᵗ T₂ → transmit d T₁ S ≈' transmit d T₂ S
≈-cong-transmit-t T1≈T2 = eq-transmit _ T1≈T2 ≈-refl

≈-cong-choice : ∀ {d m alt₁ alt₂} → ((i : Fin m) → alt₁ i ≈ alt₂ i) → choice d m alt₁ ≈' choice d m alt₂
≈-cong-choice f = eq-choice _ f

-- full congruences

≈-cong-hole-S : ∀ {sh S₁ S₂} → S₁ ≈ S₂ → apply-hole-S sh S₁ ≈ apply-hole-S sh S₂
≈-cong-hole-T : ∀ {th S₁ S₂} → S₁ ≈ S₂ → apply-hole-T th S₁ ≈ᵗ apply-hole-T th S₂

≈-cong-hole-S {hole} S1≈S2 = S1≈S2
≈-cong-hole-S {transmit-s d T sh} S1≈S2 =
  record { force = ≈-cong-transmit (≈-cong-hole-S S1≈S2 ) }
≈-cong-hole-S {transmit-t d th S} S1≈S2 =
  record { force = ≈-cong-transmit-t (≈-cong-hole-T S1≈S2) }

≈-cong-hole-T {TPair-l th T₂} S1≈S2 = eq-pair (≈-cong-hole-T S1≈S2) ≈ᵗ-refl
≈-cong-hole-T {TPair-r T₁ th} S1≈S2 = eq-pair ≈ᵗ-refl (≈-cong-hole-T S1≈S2)
≈-cong-hole-T {TChan sh} S1≈S2 = eq-chan (≈-cong-hole-S S1≈S2)

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --termination-depth=2  #-}

module _ where

open import Common.Prelude

module A where

  mutual

    f : Nat → Nat
    f zero = zero
    f (suc zero) = suc zero
    f (suc (suc x)) = g x

    g : Nat → Nat
    g x = f (suc ?)

  -- This should not fail termination checking,
  -- as ? := x is a terminating instance.

module B where

  mutual

    f : Nat → Nat
    f zero = zero
    f (suc zero) = suc zero
    f (suc (suc x)) = g ?

    g : Nat → Nat
    g x = f (suc x)

  -- This should not fail termination checking,
  -- as ? := x is a terminating instance.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Type.Properties.Singleton {ℓ ℓₑ} where

import      Lvl
open import Lang.Instance
open import Structure.Setoid
open import Type

-- A type is a singleton type when it has exactly one inhabitant (there is only one object with this type).
-- In other words: There is an unique inhabitant of type T.
-- Also called:
-- • "singleton type"
-- • "unit type"
-- • "contractible"
record IsUnit (T : Type{ℓ}) ⦃ _ : Equiv{ℓₑ}(T) ⦄ : Type{ℓ Lvl.⊔ ℓₑ} where
  constructor intro
  field
    unit : T
    uniqueness : ∀{x : T} → (x ≡ unit)
open IsUnit ⦃ ... ⦄ using (unit)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --guarded #-}
module _ where

primitive
  primLockUniv : _

postulate
  A B : primLockUniv
  c : A → B
  foo : (@tick x y : B) → Set

bar2 : (@tick x : A) → Set
bar2 x = foo (c x) (c x)

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- Equivalence of the two variants of declarative kinding of Fω with
-- interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Declarative.Equivalence where

open import Data.Product using (proj₁)

open import FOmegaInt.Syntax
import FOmegaInt.Typing                   as Original
open import FOmegaInt.Kinding.Declarative as Extended
open import FOmegaInt.Kinding.Declarative.Validity

private
  module O where
    open Original public
    open Typing   public

  module E where
    open Extended public
    open Kinding  public

open Syntax
open TermCtx
open Kinding
open KindedSubstitution
open Original.Typing
  hiding (_ctx; _⊢_wf; _⊢_kd; _⊢Tp_∈_; _⊢_<∷_; _⊢_<:_∈_; _⊢_≅_; _⊢_≃_∈_)

-- Soundness of extended declarative (sub)kinding w.r.t. original
-- declarative (sub)kinding.
--
-- This soundness proof simply forgets about all the validity
-- conditions in the extended rules.

mutual

  sound-wf : ∀ {n} {Γ : Ctx n} {a} → Γ ⊢ a wf → Γ O.⊢ a wf
  sound-wf (wf-kd k-kd) = wf-kd (sound-kd k-kd)
  sound-wf (wf-tp a∈*)  = wf-tp (sound-Tp∈ a∈*)

  sound-ctx : ∀ {n} {Γ : Ctx n} → Γ ctx → Γ O.ctx
  sound-ctx E.[]             = O.[]
  sound-ctx (a-wf E.∷ Γ-ctx) = sound-wf a-wf O.∷ sound-ctx Γ-ctx

  sound-kd : ∀ {n} {Γ : Ctx n} {k} → Γ ⊢ k kd → Γ O.⊢ k kd
  sound-kd (kd-⋯ a∈* b∈*)   = kd-⋯ (sound-Tp∈ a∈*) (sound-Tp∈ b∈*)
  sound-kd (kd-Π j-kd k-kd) = kd-Π (sound-kd j-kd) (sound-kd k-kd)

  sound-Tp∈ : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Tp a ∈ k → Γ O.⊢Tp a ∈ k
  sound-Tp∈ (∈-var x Γ-ctx Γ[x]≡kd-k) =
    ∈-var x (sound-ctx Γ-ctx) Γ[x]≡kd-k
  sound-Tp∈ (∈-⊥-f Γ-ctx)         = ∈-⊥-f (sound-ctx Γ-ctx)
  sound-Tp∈ (∈-⊤-f Γ-ctx)         = ∈-⊤-f (sound-ctx Γ-ctx)
  sound-Tp∈ (∈-∀-f k-kd a∈*)      = ∈-∀-f (sound-kd k-kd) (sound-Tp∈ a∈*)
  sound-Tp∈ (∈-→-f a∈* b∈*)       = ∈-→-f (sound-Tp∈ a∈*) (sound-Tp∈ b∈*)
  sound-Tp∈ (∈-Π-i j-kd a∈k k-kd) = ∈-Π-i (sound-kd j-kd) (sound-Tp∈ a∈k)
  sound-Tp∈ (∈-Π-e a∈Πjk b∈j k-kd k[b]-kd) =
    ∈-Π-e (sound-Tp∈ a∈Πjk) (sound-Tp∈ b∈j)
  sound-Tp∈ (∈-s-i a∈b⋯c)     = ∈-s-i (sound-Tp∈ a∈b⋯c)
  sound-Tp∈ (∈-⇑ a∈j j<∷k)    = ∈-⇑ (sound-Tp∈ a∈j) (sound-<∷ j<∷k)

  sound-<∷ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j <∷ k → Γ O.⊢ j <∷ k
  sound-<∷ (<∷-⋯ a₂<:a₁∈* b₁<:b₂∈*)      =
    <∷-⋯ (sound-<: a₂<:a₁∈*) (sound-<: b₁<:b₂∈*)
  sound-<∷ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) =
    <∷-Π (sound-<∷ j₂<∷j₁) (sound-<∷ k₁<∷k₂) (sound-kd Πj₁k₁-kd)

  sound-<: : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ∈ k → Γ O.⊢ a <: b ∈ k
  sound-<: (<:-refl a∈k) = <:-refl (sound-Tp∈ a∈k)
  sound-<: (<:-trans a<:b∈k b<:c∈k) =
    <:-trans (sound-<: a<:b∈k) (sound-<: b<:c∈k)
  sound-<: (<:-β₁ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
    <:-β₁ (sound-Tp∈ a∈k) (sound-Tp∈ b∈j)
  sound-<: (<:-β₂ a∈k b∈j a[b]∈k[b] k-kd k[b]-kd) =
    <:-β₂ (sound-Tp∈ a∈k) (sound-Tp∈ b∈j)
  sound-<: (<:-η₁ a∈Πjk) = <:-η₁ (sound-Tp∈ a∈Πjk)
  sound-<: (<:-η₂ a∈Πjk) = <:-η₂ (sound-Tp∈ a∈Πjk)
  sound-<: (<:-⊥ a∈b⋯c)  = <:-⊥ (sound-Tp∈ a∈b⋯c)
  sound-<: (<:-⊤ a∈b⋯c)  = <:-⊤ (sound-Tp∈ a∈b⋯c)
  sound-<: (<:-∀ k₂<∷k₁ a₁<:a₂∈* ∀k₁a₁∈*) =
    <:-∀ (sound-<∷ k₂<∷k₁) (sound-<: a₁<:a₂∈*) (sound-Tp∈ ∀k₁a₁∈*)
  sound-<: (<:-→ a₂<:a₁∈* b₁<:b₂∈*) =
    <:-→ (sound-<: a₂<:a₁∈*) (sound-<: b₁<:b₂∈*)
  sound-<: (<:-λ a₁<:a₂∈Πjk Λj₁a₁∈Πjk Λj₂a₂∈Πjk) =
    <:-λ (sound-<: a₁<:a₂∈Πjk)
         (sound-Tp∈ Λj₁a₁∈Πjk) (sound-Tp∈ Λj₂a₂∈Πjk)
  sound-<: (<:-· a₁<:a₂∈Πjk b₁≃b₁∈j b₁∈j k-kd k[b₁]-kd) =
    <:-· (sound-<: a₁<:a₂∈Πjk) (sound-≃ b₁≃b₁∈j)
  sound-<: (<:-⟨| a∈b⋯c)        = <:-⟨| (sound-Tp∈ a∈b⋯c)
  sound-<: (<:-|⟩ a∈b⋯c)        = <:-|⟩ (sound-Tp∈ a∈b⋯c)
  sound-<: (<:-⋯-i a₁<:a₂∈b⋯c)  = <:-⋯-i (sound-<: a₁<:a₂∈b⋯c)
  sound-<: (<:-⇑ a₁<:a₂∈j j<∷k) =
    <:-⇑ (sound-<: a₁<:a₂∈j) (sound-<∷ j<∷k)

  sound-≃ : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a ≃ b ∈ k → Γ O.⊢ a ≃ b ∈ k
  sound-≃ (<:-antisym a<:b∈k b<:a∈k) =
    <:-antisym (sound-<: a<:b∈k) (sound-<: b<:a∈k)

sound-≅ : ∀ {n} {Γ : Ctx n} {j k} → Γ ⊢ j ≅ k → Γ O.⊢ j ≅ k
sound-≅ (<∷-antisym j<∷k k<∷j) =
  <∷-antisym (sound-<∷ j<∷k) (sound-<∷ k<∷j)

-- Completeness of extended declarative (sub)kinding w.r.t. original
-- declarative (sub)kinding.
--
-- This proves that the validity conditions in the extended rules are
-- in fact redundant, i.e. they follow from validity properties of the
-- remaining premises (of the rules in question)

mutual

  complete-wf : ∀ {n} {Γ : Ctx n} {a} → Γ O.⊢ a wf → Γ ⊢ a wf
  complete-wf (wf-kd k-kd) = wf-kd (complete-kd k-kd)
  complete-wf (wf-tp a∈*)  = wf-tp (complete-Tp∈ a∈*)

  complete-ctx : ∀ {n} {Γ : Ctx n} → Γ O.ctx → Γ ctx
  complete-ctx O.[]             = E.[]
  complete-ctx (a-wf O.∷ Γ-ctx) = complete-wf a-wf E.∷ complete-ctx Γ-ctx

  complete-kd : ∀ {n} {Γ : Ctx n} {k} → Γ O.⊢ k kd → Γ ⊢ k kd
  complete-kd (kd-⋯ a∈* b∈*)   = kd-⋯ (complete-Tp∈ a∈*) (complete-Tp∈ b∈*)
  complete-kd (kd-Π j-kd k-kd) = kd-Π (complete-kd j-kd) (complete-kd k-kd)

  complete-Tp∈ : ∀ {n} {Γ : Ctx n} {a k} → Γ O.⊢Tp a ∈ k → Γ ⊢Tp a ∈ k
  complete-Tp∈ (∈-var x Γ-ctx Γ[x]≡kd-k) =
    ∈-var x (complete-ctx Γ-ctx) Γ[x]≡kd-k
  complete-Tp∈ (∈-⊥-f Γ-ctx)     = ∈-⊥-f (complete-ctx Γ-ctx)
  complete-Tp∈ (∈-⊤-f Γ-ctx)     = ∈-⊤-f (complete-ctx Γ-ctx)
  complete-Tp∈ (∈-∀-f k-kd a∈*)  = ∈-∀-f (complete-kd k-kd) (complete-Tp∈ a∈*)
  complete-Tp∈ (∈-→-f a∈* b∈*)   = ∈-→-f (complete-Tp∈ a∈*) (complete-Tp∈ b∈*)
  complete-Tp∈ (∈-Π-i j-kd a∈k)  =
    ∈-Π-i (complete-kd j-kd) a∈k′ k-kd
    where
      a∈k′ = complete-Tp∈ a∈k
      k-kd = Tp∈-valid a∈k′
  complete-Tp∈ (∈-Π-e a∈Πjk b∈j) with Tp∈-valid (complete-Tp∈ a∈Πjk)
  ... | (kd-Π j-kd k-kd) =
    ∈-Π-e (complete-Tp∈ a∈Πjk) b∈j′ k-kd k[b]-kd
    where
      b∈j′    = complete-Tp∈ b∈j
      k[b]-kd = kd-[] k-kd (∈-tp b∈j′)
  complete-Tp∈ (∈-s-i a∈b⋯c)     = ∈-s-i (complete-Tp∈ a∈b⋯c)
  complete-Tp∈ (∈-⇑ a∈j j<∷k)    = ∈-⇑ (complete-Tp∈ a∈j) (complete-<∷ j<∷k)

  complete-<∷ : ∀ {n} {Γ : Ctx n} {j k} → Γ O.⊢ j <∷ k → Γ ⊢ j <∷ k
  complete-<∷ (<∷-⋯ a₂<:a₁∈* b₁<:b₂∈*)      =
    <∷-⋯ (complete-<: a₂<:a₁∈*) (complete-<: b₁<:b₂∈*)
  complete-<∷ (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) =
    <∷-Π (complete-<∷ j₂<∷j₁) (complete-<∷ k₁<∷k₂) (complete-kd Πj₁k₁-kd)

  complete-<: : ∀ {n} {Γ : Ctx n} {a b k} → Γ O.⊢ a <: b ∈ k → Γ ⊢ a <: b ∈ k
  complete-<: (<:-refl a∈k) = <:-refl (complete-Tp∈ a∈k)
  complete-<: (<:-trans a<:b∈k b<:c∈k) =
    <:-trans (complete-<: a<:b∈k) (complete-<: b<:c∈k)
  complete-<: (<:-β₁ a∈k b∈j) =
    <:-β₁ a∈k′ b∈j′ a[b]∈k[b] k-kd k[b]-kd
    where
      a∈k′ = complete-Tp∈ a∈k
      b∈j′ = complete-Tp∈ b∈j
      k-kd = Tp∈-valid a∈k′
      a[b]∈k[b] = Tp∈-[] a∈k′ (∈-tp b∈j′)
      k[b]-kd   = kd-[] k-kd (∈-tp b∈j′)
  complete-<: (<:-β₂ a∈k b∈j) =
    <:-β₂ a∈k′ b∈j′ a[b]∈k[b] k-kd k[b]-kd
    where
      a∈k′ = complete-Tp∈ a∈k
      b∈j′ = complete-Tp∈ b∈j
      k-kd = Tp∈-valid a∈k′
      a[b]∈k[b] = Tp∈-[] a∈k′ (∈-tp b∈j′)
      k[b]-kd   = kd-[] k-kd (∈-tp b∈j′)
  complete-<: (<:-η₁ a∈Πjk) = <:-η₁ (complete-Tp∈ a∈Πjk)
  complete-<: (<:-η₂ a∈Πjk) = <:-η₂ (complete-Tp∈ a∈Πjk)
  complete-<: (<:-⊥ a∈b⋯c)  = <:-⊥ (complete-Tp∈ a∈b⋯c)
  complete-<: (<:-⊤ a∈b⋯c)  = <:-⊤ (complete-Tp∈ a∈b⋯c)
  complete-<: (<:-∀ k₂<∷k₁ a₁<:a₂∈* ∀k₁a₁∈*) =
    <:-∀ (complete-<∷ k₂<∷k₁) (complete-<: a₁<:a₂∈*) (complete-Tp∈ ∀k₁a₁∈*)
  complete-<: (<:-→ a₂<:a₁∈* b₁<:b₂∈*) =
    <:-→ (complete-<: a₂<:a₁∈*) (complete-<: b₁<:b₂∈*)
  complete-<: (<:-λ a₁<:a₂∈Πjk Λj₁a₁∈Πjk Λj₂a₂∈Πjk) =
    <:-λ (complete-<: a₁<:a₂∈Πjk)
         (complete-Tp∈ Λj₁a₁∈Πjk) (complete-Tp∈ Λj₂a₂∈Πjk)
  complete-<: (<:-· a₁<:a₂∈Πjk b₁≃b₁∈j)
    with <:-valid-kd (complete-<: a₁<:a₂∈Πjk)
  ... | (kd-Π j-kd k-kd) =
    <:-· (complete-<: a₁<:a₂∈Πjk) b₁≃b₂∈j′ b₁∈j k-kd k[b₁]-kd
    where
      b₁≃b₂∈j′ = complete-≃ b₁≃b₁∈j
      b₁∈j     = proj₁ (≃-valid b₁≃b₂∈j′)
      k[b₁]-kd = kd-[] k-kd (∈-tp b₁∈j)
  complete-<: (<:-⟨| a∈b⋯c)        = <:-⟨| (complete-Tp∈ a∈b⋯c)
  complete-<: (<:-|⟩ a∈b⋯c)        = <:-|⟩ (complete-Tp∈ a∈b⋯c)
  complete-<: (<:-⋯-i a₁<:a₂∈b⋯c)  = <:-⋯-i (complete-<: a₁<:a₂∈b⋯c)
  complete-<: (<:-⇑ a₁<:a₂∈j j<∷k) =
    <:-⇑ (complete-<: a₁<:a₂∈j) (complete-<∷ j<∷k)

  complete-≃ : ∀ {n} {Γ : Ctx n} {a b k} → Γ O.⊢ a ≃ b ∈ k → Γ ⊢ a ≃ b ∈ k
  complete-≃ (<:-antisym a<:b∈k b<:a∈k) =
    <:-antisym (complete-<: a<:b∈k) (complete-<: b<:a∈k)

complete-≅ : ∀ {n} {Γ : Ctx n} {j k} → Γ O.⊢ j ≅ k → Γ ⊢ j ≅ k
complete-≅ (<∷-antisym j<∷k k<∷j) =
  <∷-antisym (complete-<∷ j<∷k) (complete-<∷ k<∷j)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
------------------------------------------------------------------------
-- Lists of identifiers
------------------------------------------------------------------------

-- This example is based on one in Swierstra and Chitil's "Linear,
-- bounded, functional pretty-printing".

{-# OPTIONS --guardedness #-}

module Examples.Identifier-list where

open import Codata.Musical.Notation
open import Data.List
import Data.List.NonEmpty as List⁺
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Examples.Identifier
open import Grammar.Infinite as Grammar
  using (Grammar) hiding (module Grammar)
open import Pretty using (Pretty-printer)
open import Renderer
open import Utilities

identifier-list-body : Grammar (List Identifier)
identifier-list-body =
    return []
  ∣ List⁺.toList <$> (identifier-w sep-by symbol′ ",")
  where open Grammar

identifier-list : Grammar (List Identifier)
identifier-list = symbol′ "[" ⊛> identifier-list-body <⊛ symbol′ "]"
  where open Grammar

open Pretty

identifier-list-printer : Pretty-printer identifier-list
identifier-list-printer ns = symbol ⊛> body ns <⊛ symbol
  where
  body : Pretty-printer identifier-list-body
  body []       = left nil
  body (n ∷ ns) =
    right (<$> (<$> identifier-w-printer n
                  ⊛
                map⋆ (λ n → group symbol-line ⊛>
                            identifier-w-printer n)
                     ns))

identifiers : List Identifier
identifiers = str⁺ "aaa" ∷ str⁺ "bbbbb" ∷ str⁺ "ccc" ∷
              str⁺ "dd" ∷ str⁺ "eee" ∷ []

test₁ : render 80 (identifier-list-printer identifiers) ≡
        "[aaa, bbbbb, ccc, dd, eee]"
test₁ = refl

test₂ : render 11 (identifier-list-printer identifiers) ≡
        "[aaa,\nbbbbb, ccc,\ndd, eee]"
test₂ = refl

test₃ : render 8 (identifier-list-printer identifiers) ≡
        "[aaa,\nbbbbb,\nccc, dd,\neee]"
test₃ = refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
{-
Comments of the following form are parsed automatically by [extract.py] in order
to convert them to LaTeX and include them in the pdf.

{-<nameofbloc>-}
code
code
code
{-</>-}

-}

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

open import PathInduction
open import Pushout

module JamesTwoMaps {i} (A : Type i) (⋆A : A) where

-- We first define [J], [ι], [α] and [β].
-- We need [JS] to make the termination checker happy.

{-<defJiab>-}
J   : ℕ → Type i
JS  : ℕ → Type i
ι   : (n : ℕ) → J n → JS n
α   : (n : ℕ) → A → J n → JS n
β   : (n : ℕ) (x : J n) → α n ⋆A x == ι n x

data J0 : Type i where
  ε : J0

J 0 = J0
J (S n) = JS n

JS 0 = A
JS (S n) = Pushout (span (A × JS n) (JS n) X f g)  module JS where

  X : Type i
  X = Pushout (span (A × J n) (JS n) (J n) (λ x → (⋆A , x)) (ι n))

  f : X → A × JS n
  f = Pushout-rec (λ {(a , x) → (a , ι n x)}) (λ y → (⋆A , y)) (λ x → idp)

  g : X → JS n
  g = Pushout-rec (λ {(a , x) → α n a x}) (λ y → y) (β n)

ι 0 ε = ⋆A
ι (S n) x = inr x

α 0 a ε = a
α (S n) a x = inl (a , x)

β 0 ε = idp
β (S n) x = push (inr x)
{-</>-}

-- We can now define [γ] and [η]

{-<defge>-}
γ : (n : ℕ) (a : A) (x : J n) → α (S n) a (ι n x) == ι (S n) (α n a x)
γ n a x = push (inl (a , x))

η : (n : ℕ) (x : J n)
  → Square (γ n ⋆A x) idp (ap (ι (S n)) (β n x)) (β (S n) (ι n x))
η n x = natural-square push (push x) α-f-push ι-g-push  where

  α-f-push : ap (uncurry (α (S n)) ∘ JS.f n) (push x) == idp
  α-f-push =  ap-∘ (uncurry (α (S n))) (JS.f n) (push x)
              ∙ ap (ap (uncurry (α (S n)))) (push-β _)

  ι-g-push : ap (ι (S n) ∘ JS.g n) (push x) == ap (ι (S n)) (β n x)
  ι-g-push =  ap-∘ (ι (S n)) (JS.g n) (push x)
              ∙ ap (ap (ι (S n))) (push-β _)
{-</>-}

-- We define the more convenient elimination principle for JSS n:

{-<JSSElim>-}
module _ {l} (n : ℕ) {P : JS (S n) → Type l}
  (ι* : (x : JS n) → P (ι (S n) x))
  (α* : (a : A) (x : JS n) → P (α (S n) a x))
  (β* : (x : JS n) → α* ⋆A x == ι* x [ P ↓ β (S n) x ])
  (γ* : (a : A) (x : J n) → α* a (ι n x) == ι* (α n a x) [ P ↓ γ n a x ])
  (η* : (x : J n) → SquareOver P (η n x)  (γ* ⋆A x)
                                          idp
                                          (↓-ap-in P inr (apd ι* (β n x)))
                                          (β* (ι n x)))
  where

  JSS-elim : (x : JS (S n)) → P x
  JSS-elim = Pushout-elim (uncurry α*) ι* JSS-elim-push  where

    JSS-elim-push : (x : JS.X n) → uncurry α* (JS.f n x) == ι* (JS.g n x) [ P ↓ push x ]
    JSS-elim-push = Pushout-elim (uncurry γ*) β*
          (λ x → ↓-PathOver-from-square
               (adapt-SquareOver
                 (↓-ap-in-coh P (uncurry α*)) (↓-ap-in-coh P ι*)
                 (η* x)))
{-</>-}

{-<JSSRec>-}
module _ {l} (n : ℕ) {X : Type l}
  (ι* : JS n → X)
  (α* : A → JS n → X)
  (β* : (x : JS n) → α* ⋆A x == ι* x)
  (γ* : (a : A) (x : J n) → α* a (ι n x) == ι* (α n a x))
  (η* : (x : J n) → Square (γ* ⋆A x) idp (ap ι* (β n x)) (β* (ι n x)))
  where

  JSS-rec : JS (S n) → X
  JSS-rec = Pushout-rec (uncurry α*) ι* JSS-rec-push  module _ where

    JSS-rec-push : (c : JS.X n) → uncurry α* (JS.f n c) == ι* (JS.g n c)
    JSS-rec-push = Pushout-elim (uncurry γ*) β* (λ x → ↓-='-from-square (α-f-push x) (ι-g-push x) (η* x))  where

      α-f-push : (x : J n) → ap ((uncurry α*) ∘ (JS.f n)) (push x) == idp
      α-f-push x = ap-∘ _ _ (push x) ∙ ap (ap (uncurry α*)) (push-β x)

      ι-g-push : (x : J n) → ap (ι* ∘ (JS.g n)) (push x) == ap ι* (β n x)
      ι-g-push x = ap-∘ ι* _ (push x) ∙ ap (ap ι*) (push-β x)

module _ {l} (n : ℕ) {X : Type l}
  {ι* : JS n → X}
  {α* : A → JS n → X}
  {β* : (x : JS n) → α* ⋆A x == ι* x}
  {γ* : (a : A) (x : J n) → α* a (ι n x) == ι* (α n a x)}
  {η* : (x : J n) → Square (γ* ⋆A x) idp (ap ι* (β n x)) (β* (ι n x))}
  where

  private JSS-rec' = JSS-rec n ι* α* β* γ* η*
  private JSS-rec-push' = JSS-rec-push n ι* α* β* γ* η*

  β-β : (x : JS n) → ap JSS-rec' (β (S n) x) == β* x
  β-β x = push-β (inr x)

  γ-β : (a : A) (x : J n) → ap JSS-rec' (γ n a x) == γ* a x
  γ-β a x = push-β (inl (a , x))

  η-β : (x : J n) → FlatCube (ap-square JSS-rec' (η n x))
                             (η* x)
                             (γ-β ⋆A x)
                             idp
                             (∘-ap JSS-rec' inr (β n x))
                             (β-β (ι n x))
  η-β x = adapt-flatcube ∙idp
                         (& coh (ap-∘3 JSS-rec' inl  _ (push x)) (natural-square (ap-∘ JSS-rec' inl)  (push-β x) idp (ap-∘ (ap JSS-rec') (ap inl)  _)) (ap-∙ _ _ _))
                         (& coh (ap-∘3 JSS-rec' inr _ (push x)) (natural-square (ap-∘ JSS-rec' inr) (push-β x) idp (ap-∘ (ap JSS-rec') (ap inr) _)) (ap-∙ _ _ _))
                         ∙idp
            ((& (ap-square-natural-square JSS-rec') (push x) push idp idp
            /∙³ & natural-square-homotopy push-β (push x)
            ∙fc & natural-square== JSS-rec-push' (push x) idp idp
            ∙³/ natural-square-β JSS-rec-push' (push x) (push-βd x)))  where

    coh : Coh ({A : Type l} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} (sq1 : Square p q r s)
                {e : A} {t : c == e} {f : A} {u : d == f} {v : e == f} (sq2 : Square s t u v)
                {ru : b == f} (ru= : ru == r ∙ u)
                → idp ∙ ! (p ∙ ru) ∙ q ∙ t == ! v)
    coh = path-induction
{-</>-}

-- Let’s now define JA

{-<defJA>-}
postulate
  JA  : Type i
  εJ  : JA
  αJ  : A → JA → JA
  δJ  : (x : JA) → x == αJ ⋆A x

module _ {l} {P : JA → Type l}
  (εJ*  : P εJ)
  (αJ*  : (a : A) (x : JA) → P x → P (αJ a x))
  (δJ*  : (x : JA) (y : P x) → y == αJ* ⋆A x y [ P ↓ (δJ x)]) where

  postulate
    JA-elim  : (x : JA) → P x
    εJ-β     : JA-elim εJ ↦ εJ*
    αJ-β     : (a : A) (x : JA) → JA-elim (αJ a x) ↦ αJ* a x (JA-elim x)
    {-# REWRITE εJ-β #-}
    {-# REWRITE αJ-β #-}
    δJ-βd'   : (x : JA) → apd JA-elim (δJ x) == δJ* x (JA-elim x)
{-</>-}

δJ-βd : ∀ {l} {P : JA → Type l}
  {εJ* : P εJ}
  {αJ* : (a : A) (x : JA) → P x → P (αJ a x)}
  {δJ* : (x : JA) (y : P x) → y == αJ* ⋆A x y [ P ↓ (δJ x)]}
  → (x : JA) → apd (JA-elim εJ* αJ* δJ*) (δJ x) == δJ* x (JA-elim εJ* αJ* δJ* x)
δJ-βd = δJ-βd' _ _ _

JA-rec : ∀ {l} {P : Type l}
  (εJ* : P)
  (αJ* : (a : A) → P → P)
  (δJ* : (y : P) → y == αJ* ⋆A y)
  → JA → P
JA-rec εJ* αJ* δJ* = JA-elim εJ* (λ a x y → αJ* a y) (λ x y → ↓-cst-in (δJ* y))

δJ-β : ∀ {l} {P : Type l}
  {εJ* : P}
  {αJ* : (a : A) → P → P}
  {δJ* : (y : P) → y == αJ* ⋆A y}
  → (x : JA) → ap (JA-rec εJ* αJ* δJ*) (δJ x) == δJ* (JA-rec εJ* αJ* δJ* x)
δJ-β x = apd=cst-in (δJ-βd x)

-- We define the structure on JA

{-<defgJeJ>-}
module _ {i} {X : Type i} (α : A → X → X) (δ : (x : X) → x == α ⋆A x) where

  γ-ify : (a : A) (x : X) → α a (α ⋆A x) == α ⋆A (α a x)
  γ-ify a x = ! (ap (α a) (δ x)) ∙ δ (α a x)

  η-ify : (x : X) → γ-ify ⋆A x == idp
  η-ify = λ x → & coh (natural-square δ (δ x) (ap-idf (δ x)) idp)  module ηIfy where

    coh : Coh  ({A : Type i} {a b : A} {p : a == b}
               {c : A} {q r : b == c} (sq : Square p p q r)
               → ! q ∙ r == idp)
    coh = path-induction

γJ : (a : A) (x : JA) → αJ a (αJ ⋆A x) == αJ ⋆A (αJ a x)
γJ = γ-ify αJ δJ

ηJ : (x : JA) → γJ ⋆A x == idp
ηJ = η-ify αJ δJ
{-</>-}

-- The functions [inJS-ι], [inJS-α] and [inJS-β] are to be thought of as
-- reduction rules.
{-<definJpushJ>-}
inJ   : (n : ℕ) → J n → JA
inJS  : (n : ℕ) → J (S n) → JA

inJS-ι  : (n : ℕ) (x : J n) → inJS n (ι n x) == αJ ⋆A (inJ n x)
inJS-α  : (n : ℕ) (a : A) (x : J n) → inJS n (α n a x) == αJ a (inJ n x)
inJS-β  : (n : ℕ) (x : J n) → Square (ap (inJS n) (β n x)) (inJS-α n ⋆A x) (inJS-ι n x) idp

inJ 0 ε = εJ
inJ (S n) x = inJS n x

inJS 0 a = αJ a εJ
inJS (S n) = JSS-rec n ι* α* β* γ* η*  module InJS where

  ι* : JS n → JA
  ι* x = αJ ⋆A (inJS n x)

  α* : A → JS n → JA
  α* a x = αJ a (inJS n x)

  β* : (x : JS n) → α* ⋆A x == ι* x
  β* x = idp

  γ* : (a : A) (x : J n) → α* a (ι n x) == ι* (α n a x)
  γ* a x = ap (αJ a) (inJS-ι n x) ∙ γJ a (inJ n x) ∙ ! (ap (αJ ⋆A) (inJS-α n a x))

  η* : (x : J n) → Square (γ* ⋆A x) idp (ap (αJ ⋆A ∘ inJS n) (β n x)) (β* (ι n x))
  η* x = & coh  (ηJ (inJ n x))
                (ap-square (αJ ⋆A) (inJS-β n x))
                (ap-∘ (αJ ⋆A) (inJS n) _)  module η* where

        coh :  Coh  ({A : Type i} {a b : A} {p : a == b} {c : A} {r : c == b}
                    {q : b == b} (q= : q == idp) {t : c == a} (sq : Square t r p idp)
                    {t' : c == a} (t= : t' == t)
               → Square (p ∙ q ∙ ! r) idp t' idp)
        coh = path-induction

inJS-ι 0 ε = idp
inJS-ι (S n) x = idp

inJS-α 0 a ε = idp
inJS-α (S n) a x = idp

inJS-β 0 ε = ids
inJS-β (S n) x = horiz-degen-square (push-β _)

pushJ : (n : ℕ) (x : J n) → inJ n x == inJ (S n) (ι n x)
pushJ n x = δJ (inJ n x) ∙ ! (inJS-ι n x)
{-</>-}

-- [inJS-β] applied for [n = S n] gives a degenerate square.
-- It is sometimes more convenient to see it as a 2-path as belown.
inJS-βS : (n : ℕ) (x : J (S n)) → ap (inJS (S n)) (β (S n) x) == idp
inJS-βS n x = push-β _

-- We give reduction rules for [inJS (S n)] applied to [γ] and [η] which are
-- more convenient to use

inJSS-γ : (n : ℕ) (a : A) (x : J n) → Square (ap (inJS (S n)) (γ n a x)) (ap (αJ a) (inJS-ι n x)) (ap (αJ ⋆A) (inJS-α n a x)) (γJ a (inJ n x))
inJSS-γ n a x = & coh (γ-β n a x)  module InJSγ where

  coh : Coh ({A : Type i} {a c : A} {q : a == c} {d : A} {s : c == d} {b : A} {r : b == d} {p : a == b}
        → p == q ∙ s ∙ ! r
        → Square p q r s)
  coh = path-induction

ap-inJSS-ι : (n : ℕ) {x y : J (S n)} (p : x == y) → ap (inJS (S n)) (ap (ι (S n)) p) == ap (αJ ⋆A) (ap (inJS n) p)
ap-inJSS-ι n p = ∘-ap (inJS (S n)) (ι (S n)) p ∙ ap-∘ (αJ ⋆A) (inJS n) p

inJSS-η : (n : ℕ) (x : J n) → Cube (ap-square (inJS (S n)) (η n x))
                                   (horiz-degen-square (ηJ (inJ n x)))
                                   (inJSS-γ n ⋆A x)
                                   vid-square
                                   (ap-inJSS-ι n (β n x) |∙ ap-square (αJ ⋆A) (inJS-β n x))
                                   (inJS-βS n (ι n x) |∙ vid-square)
inJSS-η n x = & coh (η-β n x)  where

  coh : {A : Type i} {a : A} → Coh ({r : a == a} {right : r == idp}
        {b : A} {s : b == a} {c : A} {t : b == c} {u : c == c} {to : u == idp}
        {s' : b == a} {down : s == s'} {s'' : b == a} {down' : s' == s''}
        {p : a == c} {down2 : Square s'' t p idp}
        {q : a == b} {sq : q == p ∙ u ∙ ! t} {from : Square q idp s r}
        → FlatCube from (& (InJS.η*.coh n x) to down2 down') sq idp down right
        → Cube from (horiz-degen-square to) (& (InJSγ.coh n ⋆A x) sq) vid-square ((down ∙ down') |∙ down2) (right |∙ vid-square))
  coh = path-induction

-- This function is used to apply a function to the result of [inJSS-η]
ap-shapeInJSη : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a : A}
  → Coh ({r : a == a} {right : r == idp} {b : A} {q : a == b}
  {c : A} {p : a == c} {u : c == c} {to : u == idp} {t : b == c} {left : Square q p t u}
  {s' : b == a} {down3 : Square s' t p idp} {s : b == a} {down1 : s == s'}
  {from : Square q idp s r}
  → Cube from (horiz-degen-square to) left vid-square (down1 |∙ down3) (right |∙ vid-square)
  → {ft : f b == f c} (ft= : ap f t == ft) {fp : f a == f c} (fp= : ap f p == fp)
  → Cube (ap-square f from) (horiz-degen-square (ap (ap f) to))
         (adapt-square (ap-square f left) fp= ft=) vid-square
         (adapt-square (ap (ap f) down1 |∙ ap-square f down3) ft= fp=) (ap (ap f) right |∙ vid-square))
ap-shapeInJSη f = path-induction

-- Definition of J∞A

{-<defJiA>-}
postulate
  J∞A    : Type i
  in∞    : (n : ℕ) (x : J n) → J∞A
  push∞  : (n : ℕ) (x : J n) → in∞ n x == in∞ (S n) (ι n x)

module _ {l} {P : J∞A → Type l}
  (in∞*    : (n : ℕ) (x : J n) → P (in∞ n x))
  (push∞*  : (n : ℕ) (x : J n) → in∞* n x == in∞* (S n) (ι n x) [ P ↓ (push∞ n x) ])  where

  postulate
    J∞A-elim   : (x : J∞A) → P x
    in∞-β      : (n : ℕ) (x : J n) → J∞A-elim (in∞ n x) ↦ in∞* n x
    {-# REWRITE in∞-β #-}
    push∞-βd'  : (n : ℕ) (x : J n) → apd J∞A-elim (push∞ n x) == push∞* n x
{-</>-}

push∞-βd : ∀ {l} {P : J∞A → Type l}
  {in∞* : (n : ℕ) (x : J n) → P (in∞ n x)}
  {push∞* : (n : ℕ) (x : J n) → in∞* n x == in∞* (S n) (ι n x) [ P ↓ (push∞ n x) ]}
  → (n : ℕ) (x : J n) → apd (J∞A-elim in∞* push∞*) (push∞ n x) == push∞* n x
push∞-βd = push∞-βd' _ _

J∞A-rec : ∀ {l} {P : Type l}
  (in∞* : (n : ℕ) (x : J n) → P)
  (push∞* : (n : ℕ) (x : J n) → in∞* n x == in∞* (S n) (ι n x))
  → J∞A → P
J∞A-rec in∞* push∞* = J∞A-elim in∞* (λ n x → ↓-cst-in (push∞* n x))

push∞-β : ∀ {l} {P : Type l}
  {in∞* : (n : ℕ) (x : J n) → P}
  {push∞* : (n : ℕ) (x : J n) → in∞* n x == in∞* (S n) (ι n x)}
  → (n : ℕ) (x : J n) → ap (J∞A-rec in∞* push∞*) (push∞ n x) == push∞* n x
push∞-β n x = apd=cst-in (push∞-βd n x)

-- Structure on J∞A

{-<defstructinf>-}
ε∞ : J∞A
ε∞ = in∞ 0 ε

α∞ : A → J∞A → J∞A
α∞ a = J∞A-rec α∞-in∞ α∞-push∞  module _ where

  α∞-in∞ : (n : ℕ) (x : J n) → J∞A
  α∞-in∞ n x = in∞ (S n) (α n a x)

  α∞-push∞ : (n : ℕ) (x : J n) → α∞-in∞ n x == α∞-in∞ (S n) (ι n x)
  α∞-push∞ n x = push∞ (S n) (α n a x) ∙ ! (ap (in∞ (S (S n))) (γ n a x))

δ∞ : (x : J∞A) → x == α∞ ⋆A x
δ∞ = J∞A-elim δ∞-in∞ (λ n x → ↓-='-from-square (ap-idf (push∞ n x)) idp (δ∞-push∞ n x))
  module _ where

  δ∞-in∞ : (n : ℕ) (x : J n) → in∞ n x == α∞ ⋆A (in∞ n x)
  δ∞-in∞ n x = push∞ n x ∙ ! (ap (in∞ (S n)) (β n x))

  δ∞-push∞ : (n : ℕ) (x : J n) → Square  (δ∞-in∞ n x)
                                         (push∞ n x)
                                         (ap (α∞ ⋆A) (push∞ n x))
                                         (δ∞-in∞ (S n) (ι n x))
  δ∞-push∞ = λ n x →
    & coh  (push∞ n x)
           (ap-square (in∞ (S (S n))) (η n x))
           (natural-square (push∞ (S n)) (β n x) idp (ap-∘ _ _ _))
           (push∞-β n x)
             module δ∞Push∞ where

    coh : Coh  ({A : Type i} {a b : A} (p : a == b) {d : A} {s : d == b}
               {c : A} {r : b == c} {f : A} {u : f == c} {e : A} {t : e == c}
               {w : f == e} (eta : Square w idp t u)
               {v : d == e} (nat : Square v s t r)
               {vw : d == f} (vw= : vw == v ∙ ! w)
               → Square (p ∙ ! s) p vw (r ∙ ! u))
    coh = path-induction
{-</>-}

    ap-coh : {A B : Type i} (g : A → B) →
             Coh ({a b : A} {p : a == b} {d : A} {s : d == b}
                 {c : A} {r : b == c} {f : A} {u : f == c} {e : A} {t : e == c}
                 {w : f == e} {eta : Square w idp t u}
                 {v : d == e} {nat : Square v s t r}
                 {vw : d == f} {vw= : vw == v ∙ ! w}
                 → FlatCube (ap-square g (& coh p eta nat vw=))
                            (& coh (ap g p) (ap-square g eta) (ap-square g nat) (ap-shape-∙! g vw=))
                            (ap-∙! g p s) idp idp (ap-∙! g r u))
    ap-coh g = path-induction

ap-α∞-in∞ : (n : ℕ) (a : A) {x y : J n} (p : x == y) → ap (α∞ a) (ap (in∞ n) p) == ap (in∞ (S n)) (ap (α n a) p)
ap-α∞-in∞ n a p = ∘-ap _ _ _ ∙ ap-∘ _ _ _

δ∞-in∞-β : (n : ℕ) (x : J n) → Square (δ∞ (in∞ n x)) idp (ap (in∞ (S n)) (β n x)) (push∞ n x)
δ∞-in∞-β = λ n x → & coh  module δ∞Inβ where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : c == b} → Square (p ∙ ! q) idp q p)
  coh = path-induction

-- [γ∞] and the reduction rule for [γ∞ a (in∞ n x)] (3.2.6)

{-<gammainfin>-}
γ∞ : (a : A) (x : J∞A) → α∞ a (α∞ ⋆A x) == α∞ ⋆A (α∞ a x)
γ∞ = γ-ify α∞ δ∞

γ∞-in  : (a : A) (n : ℕ) (x : J n)
       → Square  (γ∞ a (in∞ n x))
                 (ap (in∞ (S (S n))) (ap (α (S n) a) (β n x)))
                 (ap (in∞ (S (S n))) (β (S n) (α n a x)))
                 (ap (in∞ (S (S n))) (γ n a x))
γ∞-in = λ a n x → & coh (push∞-β n x) (ap-∙! _ _ _) (ap-α∞-in∞ (S n) a (β n x))
                  module γ∞In where

  coh : Coh  ({A : Type i} {a d : A} {r : a == d} {b : A} {s : b == d}
             {c : A} {t' : c == b} {e : A} {u : e == d}
             {rs' : a == b} (rs= : rs' == r ∙ ! s)
             {fpq : a == c} (fpq= : fpq == rs' ∙ ! t')
             {t : c == b} (t= : t' == t)
             → Square (! fpq ∙ (r ∙ ! u)) t u s)
  coh = path-induction
{-</>-}

-- [η∞] and the reduction rule for [η∞ a (in∞ n x)] (3.2.7)

comp-square : {A : Type i} {a b c : A} {p : a == b} {q : b == c} → Square idp p (p ∙ q) q
comp-square {p = idp} {q = idp} = ids

skew : ∀ {i} {A : Type i} {a b c d : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} → Square p q r s → Square idp q (p ∙ r) s
skew ids = ids

ope1 : {A B : Type i} (f : A → B) {a b c : A} {p : a == b} {q : c == b}
       {fp : _} (fp= : ap f p == fp)
       {fq : _} (fq= : ap f q == fq)
       {fpq : _} (fpq= : ap f (p ∙ ! q) == fpq)
       → fpq == fp ∙ ! fq
ope1 f {p = idp} {q = idp} idp idp idp = idp

_∙!²_ : {A : Type i} {a b c : A} {p p' : a == b} (p= : p == p') {q q' : c == b} (q= : q == q')
        → (p ∙ ! q) == (p' ∙ ! q')
idp ∙!² idp = idp

ope1-idf : {A B : Type i} (f : A → B) → Coh ({b c : A} {q : c == b} {a : B} {p : a == f b}
         → ope1 (λ z → z) (ap-idf p) (∘-ap (λ z → z) f q ∙ idp) (ap-idf (p ∙ ! (ap f q))) == idp)
ope1-idf f = path-induction

natural-square-∙! : {A B : Type i} {a b c : A} (p : a == b) (q : c == b) → Coh ({f g : A → B} (h : (a : A) → f a == g a)
         {fp : _} {fp= : ap f p == fp}
         {gp : _} {gp= : ap g p == gp}
         {fq : _} {fq= : ap f q == fq}
         {gq : _} {gq= : ap g q == gq}
         {fpq : _ } {fpq= : ap f (p ∙ ! q) == fpq}
         {gpq : _ } {gpq= : ap g (p ∙ ! q) == gpq}
         → FlatCube (natural-square h (p ∙ ! q) fpq= gpq=) (natural-square h p fp= gp= ∙□ !² (natural-square h q fq= gq=)) idp (ope1 f fp= fq= fpq=) (ope1 g gp= gq= gpq=) idp)
natural-square-∙! {a = a} idp idp = path-induction

vcomp! : {A : Type i} {a b c d e f : A} {p : a == b} {q : a == c} {r : b == d} {s : c == d} {t : e == b} {u : f == d} {v : e == f}
         (sq1 : Square p q r s) (sq2 : Square t v r u)
       → Square (p ∙ ! t) q v (s ∙ ! u)
vcomp! {t = idp} ids ids = ids

natural-square∙! : {A B : Type i} {a b : A} (p : a == b)
       → Coh ({f g : A → B} (k : (a : A) → f a == g a) {h : A → B} (l : (a : A) → h a == g a)
              {fp : _} {fp= : ap f p == fp}
              {gp : _} {gp= : ap g p == gp}
              {hp : _} {hp= : ap h p == hp}
             → natural-square (λ x → k x ∙ ! (l x)) p fp= hp= == vcomp! (natural-square k p fp= gp=) (natural-square l p hp= gp=))
natural-square∙! {a = a} idp = path-induction

η∞ : (x : J∞A) → γ∞ ⋆A x == idp
η∞ = η-ify α∞ δ∞

η∞-in  : (n : ℕ) (x : J n)
       → Cube  (horiz-degen-square (η∞ (in∞ n x)))
               (ap-square (in∞ (S (S n))) (η n x))
               (γ∞-in ⋆A n x)
               vid-square
               comp-square
               (skew (ap-square (in∞ (S (S n))) (natural-square (β (S n)) (β n x) idp idp)))
η∞-in n x = & coh  (push∞-β n x)
                   (& (coh-ope1 (α∞ ⋆A)))
                   (& (ope1-idf (in∞ (S n))))
                   (natural-square-β δ∞ (push∞ n x) (push∞-βd n x))
                   (& (ap-square-natural-square (in∞ (S (S n)))) (β n x) (β (S n)) ∙idp ∙idp)
                   (& (natural-square∙! (β n x)) (push∞ (S n)) (ap (in∞ (S (S n))) ∘ β (S n)))
                   (& (natural-square-∘ (β n x) (in∞ (S n))) δ∞ idp idp)
                   (& (natural-square-∙! (push∞ n x) (ap (in∞ (S n)) (β n x))) δ∞)
                where

  coh-ope1 : {A B : Type i} (f : A → B)
           → Coh ({x y : A} {p : x == y}
                  {z : A} {q : z == y} {fq : f z == f y} {r : ap f q == fq}
                  → ap-∙! f p q == ope1 f idp r idp ∙ (idp ∙!² ! r))
  coh-ope1 f = path-induction

  -- X = apin∞SS
  coh : Coh ({A : Type i} {a b : A} {push∞Sα : a == b} {c : A} {apin∞Sβ : a == c} {d : A} {XapιSβ : b == d}
        {f : A} {Xγ : f == b} {XβSι : f == d} {apinη : Square Xγ idp XapιSβ XβSι}
        {push∞Sι : c == d} {natpush∞Sβ : Square push∞Sα apin∞Sβ XapιSβ push∞Sι}
        {e : A} {XβSα : e == b} {XapαSβ : e == f} {natβSβ : Square XβSα XapαSβ XapιSβ XβSι}
        {g : A} {p : g == c}
        {rs : a == f}
        (rs= : rs == push∞Sα ∙ ! Xγ)
        {z : _}
        {z= : z == rs ∙ ! XapαSβ}
        {t : _} {t= : t == XapαSβ}
        {fpq= : z == rs ∙ ! t}
        (fpq== : fpq= == z= ∙ (idp ∙!² ! t=))
        {pq=' : _} (pq== : pq=' == idp)
        {α' : _} (α= : α' == (& δ∞Push∞.coh p apinη natpush∞Sβ rs=))
        {γ' : _} (γ= : natβSβ == γ')
        {βγ : _} (βγ=comp : βγ == vcomp! natpush∞Sβ γ')
        {βγ' : _} (βγ= : βγ == βγ')
        {sq : _} (sq= : FlatCube sq (α' ∙□ !² βγ') idp pq=' z= idp)
      → Cube (horiz-degen-square (& (ηIfy.coh α∞ δ∞) sq))
             apinη
             (& γ∞In.coh rs= fpq= t=)
             vid-square
             comp-square
             (skew natβSβ))
  coh = path-induction

-- The two maps

{-<twomaps>-}
to : J∞A → JA
to = J∞A-rec inJ pushJ

from : JA → J∞A
from = JA-rec ε∞ α∞ δ∞
{-</>-}

-- Rules which better match the intuitive definition of [pushJ n x]
to-push∞ : (n : ℕ) (x : J n) → Square (ap to (push∞ n x)) idp (inJS-ι n x) (δJ (inJ n x))
to-push∞ n x = & coh (push∞-β n x)  where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : c == b} {r : a == c} (r= : r == p ∙ ! q) → Square r idp q p)
  coh = path-induction

to-push∞-S : (n : ℕ) (x : J (S n)) → ap to (push∞ (S n) x) == δJ (inJ (S n) x)
to-push∞-S n x = horiz-degen-path (to-push∞ (S n) x)

ap-from-αJ : (a : A) {x y : JA} (p : x == y) → ap from (ap (αJ a) p) == ap (α∞ a) (ap from p)
ap-from-αJ a p = ∘-ap _ _ _ ∙ ap-∘ _ _ _

ap-square-from-αJ : (a : A) {x y z t : JA} {p : x == y} {q : x == z} {r : y == t} {s : z == t} (sq : Square p q r s)
  → FlatCube (ap-square from (ap-square (αJ a) sq))
             (ap-square (α∞ a) (ap-square from sq))
             (ap-from-αJ _ _) (ap-from-αJ _ _)
             (ap-from-αJ _ _) (ap-from-αJ _ _)
ap-square-from-αJ a ids = idfc

-- Abbreviation for the natural square of [δJ]
ap-δJ : {x y : JA} (p : x == y) → Square (δJ x) p (ap (αJ ⋆A) p) (δJ y)
ap-δJ p = natural-square δJ p (ap-idf p) idp

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
module Numeric.Nat.LCM where

open import Prelude
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.GCD
open import Numeric.Nat.GCD.Extended
open import Numeric.Nat.GCD.Properties
open import Numeric.Nat.Properties
open import Tactic.Nat

--- Least common multiple ---

record IsLCM m a b : Set where
  no-eta-equality
  constructor is-lcm
  field
    a|m : a Divides m
    b|m : b Divides m
    l   : ∀ k → a Divides k → b Divides k → m Divides k

record LCM a b : Set where
  no-eta-equality
  constructor lcm-res
  field
    m : Nat
    isLCM : IsLCM m a b

open LCM using () renaming (m to get-lcm) public

eraseIsLCM : ∀ {a b m} → IsLCM m a b → IsLCM m a b
eraseIsLCM (is-lcm a|m b|m g) = is-lcm (fast-divides a|m) (fast-divides b|m)
                                       λ k a|k b|k → fast-divides (g k a|k b|k)

eraseLCM : ∀ {a b} → LCM a b → LCM a b
eraseLCM (lcm-res m p) = lcm-res m (eraseIsLCM p)

private
  lem-is-lcm : ∀ {a b d} (g : IsGCD d a b) →
               IsLCM (is-gcd-factor₁ g * b) a b
  lem-is-lcm {a} {b} {0} (is-gcd (factor q eq) d|b g)
             rewrite a ≡⟨ by eq ⟩ 0 ∎ | divides-zero d|b | q * 0 ≡⟨ auto ⟩ 0 ∎ =
    is-lcm divides-refl divides-refl (λ _ 0|k _ → 0|k)
  lem-is-lcm {a} {b} {d@(suc d′)} isg@(is-gcd (factor! q) d|b@(factor! q′) g) =
    is-lcm (divides-mul-cong-l q d|b)
           (divides-mul-r q divides-refl) least
    where
      lem : IsGCD d a b
      lem = is-gcd (factor! q) d|b g

      lem₂ : Coprime q q′
      lem₂ = is-gcd-factors-coprime lem

      least : ∀ k → a Divides k → b Divides k → (q * b) Divides k
      least k (factor qa qa=k) (factor qb qb=k) =
        case lem₄ of λ where
          (factor! qqb) → factor qqb (by qb=k)
        where
          lem₃ : qa * q ≡ q′ * qb
          lem₃ = mul-inj₁ (qa * q) (q′ * qb) (suc d′)
                 (by (qa=k ⟨≡⟩ʳ qb=k))

          lem₄ : q Divides qb
          lem₄ = coprime-divide-mul-l q q′ qb (is-gcd-factors-coprime isg)
                 (factor qa lem₃)

lcm : ∀ a b → LCM a b
lcm a b = eraseLCM $
  case gcd a b of λ where
    (gcd-res d g) →
      lcm-res (is-gcd-factor₁ g * b) (lem-is-lcm g)

lcm! : Nat → Nat → Nat
lcm! a b = get-lcm (lcm a b)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Vector where

infixr 10 _∷_

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

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

infixl 6 _+_

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

data Vec (A : Set) : ℕ → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

_++_ : ∀ {A n m} → Vec A n → Vec A m → Vec A (n + m)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

infix 4 _≡_

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

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

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

vec : ∀ {A} (k : ℕ) → Set
vec {A} k = Vec A k

plus_zero : {n : ℕ} → n + 0 ≡ n
plus_zero {zero}  = refl
plus_zero {suc n} = cong suc plus_zero

plus_suc : {n : ℕ} → n + (suc 0) ≡ suc n
plus_suc {zero}  = refl
plus_suc {suc n} = cong suc (plus_suc {n})

reverse : ∀ {A n} → Vec A n → Vec A n
reverse []       = []
reverse {A} {suc n} (x ∷ xs) = subst vec (plus_suc {n}) (reverse xs ++ (x ∷ []))

max_stars_repo_name: aavogt/wiwinwlh

max_issues_repo_name: aavogt/wiwinwlh

max_forks_repo_name: aavogt/wiwinwlh


text:
module Data.Vec.Exts where

open import Data.Fin
open import Data.Maybe
open import Data.Nat
open import Data.Vec using (Vec; []; _∷_)
open import Relation.Nullary
open import Relation.Unary
open import Data.Vec.Relation.Unary.Any

findIndex : {n : ℕ} {A : Set} {P : A -> Set} -> Decidable P -> Vec A n -> Maybe (Fin n)
findIndex P? xs with any? P? xs
... | yes ix = just (index ix)
... | no _ = nothing

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module Ag10 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import Ag09 using (_≃_; _≲_; extensionality; _⇔_)
open Ag09.≃-Reasoning
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
open import Data.Empty using (⊥; ⊥-elim)
import Function.Equivalence using (_⇔_)

⇔≃× : ∀ {A B : Set} → (A ⇔ B) ≃ ((A → B) × (B → A))
⇔≃× =
  record
  { to = λ{ x → ⟨ Ag09._⇔_.to x , Ag09._⇔_.from x ⟩}
  ; from = λ{ ⟨ x , y ⟩ → record { to = x ; from = y } }
  ; from∘to = λ{ x → refl }
  ; to∘from = λ{ x → refl }
  }

⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A)
⊎-comm =
  record
  { to = λ{ (inj₁ x) → inj₂ x ; (inj₂ y) → inj₁ y }
  ; from =  λ{ (inj₁ x) → inj₂ x ; (inj₂ y) → inj₁ y}
  ; from∘to = λ{ (inj₁ x) → refl ; (inj₂ y) → refl }
  ; to∘from = λ{ (inj₁ x) → refl ; (inj₂ y) → refl}
  }

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc =
  record
  { to = λ{ (inj₁ (inj₁ x)) → inj₁ x ; (inj₁ (inj₂ y)) → inj₂ (inj₁ y) ; (inj₂ z) → inj₂ (inj₂ z) }
  ; from = λ{ (inj₁ x) → inj₁ (inj₁ x) ; (inj₂ (inj₁ y)) → inj₁ (inj₂ y) ; (inj₂ (inj₂ z)) → inj₂ z }
  ; from∘to = λ{ (inj₁ (inj₁ x)) → refl ; (inj₁ (inj₂ y)) → refl ; (inj₂ z) → refl }
  ; to∘from = λ{ (inj₁ x) → refl ; (inj₂ (inj₁ y)) → refl ; (inj₂ (inj₂ z)) → refl }
  }

⊥-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
⊥-identityˡ =
    record
    { to = λ{ (inj₂ a) → a }
    ; from = λ{ a → (inj₂ a) }
    ; from∘to = λ{ (inj₂ a) → refl }
    ; to∘from = λ{ a → refl }
    }

⊥-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
⊥-identityʳ {A} =
    ≃-begin
      (A ⊎ ⊥)
    ≃⟨ ⊎-comm ⟩
      (⊥ ⊎ A)
    ≃⟨ ⊥-identityˡ ⟩
      A
    ≃-∎

⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-× ⟨ inj₁ x , snd ⟩ = inj₁ x
⊎-weak-× ⟨ inj₂ y , snd ⟩ = inj₂ ⟨ y , snd ⟩

⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎ (inj₁ ⟨ fst , snd ⟩) = ⟨ inj₁ fst , inj₁ snd ⟩
⊎×-implies-×⊎ (inj₂ ⟨ fst , snd ⟩) = ⟨ inj₂ fst , inj₂ snd ⟩

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module Issue846.Imports where

open import Data.Nat public using (ℕ; zero; suc; _≤_; _∸_)
open import Data.List public using (List; []; _∷_)
open import Data.Bool public using (Bool; true; false; not)
open import Data.Nat.DivMod public using (_mod_)
open import Data.Fin public using (Fin; toℕ; zero; suc)
open import Relation.Binary.PropositionalEquality public using (_≡_; _≢_; cong)

open import Relation.Binary public using (nonEmpty) -- this is the bad guy

open import Issue846.DivModUtils public using (1'; lem-sub-p)

record Move : Set where
  constructor pick
  field
    picked : ℕ
    1≤n    : 1 ≤ picked
    n≤6    : picked ≤ 6
open Move using (picked)

Strategy = ℕ → Move

{-# NO_TERMINATION_CHECK #-}
play : ℕ → Strategy → Strategy → List ℕ
play 0 _ _ = []
play n p1 p2 = n ∷ play (n ∸ picked (p1 n)) p2 p1

postulate
  opt : Strategy

evenList : {A : Set} → List A → Bool
evenList [] = true
evenList (_ ∷ xs) = not (evenList xs)

winner : ℕ → Strategy → Strategy → Bool
winner n p1 p2 = evenList (play n p1 p2)

postulate
  opt-is-opt : ∀ n s → n mod 7 ≢ 1' → winner n opt s ≡ true

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- FOTC terms properties
------------------------------------------------------------------------------

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

module FOTC.Base.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base

------------------------------------------------------------------------------
-- Congruence properties

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong refl = refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong refl = refl

·-cong : ∀ {a b c d} → a ≡ b → c ≡ d → a · c ≡ b · d
·-cong refl refl = refl

succCong : ∀ {m n} → m ≡ n → succ₁ m ≡ succ₁ n
succCong refl = refl

predCong : ∀ {m n} → m ≡ n → pred₁ m ≡ pred₁ n
predCong refl = refl

ifCong₁ : ∀ {b b' t t'} → b ≡ b' →
          (if b then t else t') ≡ (if b' then t else t')
ifCong₁ refl = refl

ifCong₂ : ∀ {b t₁ t₂ t} → t₁ ≡ t₂ →
          (if b then t₁ else t) ≡ (if b then t₂ else t)
ifCong₂ refl = refl

ifCong₃ : ∀ {b t t₁ t₂} → t₁ ≡ t₂ →
          (if b then t else t₁) ≡ (if b then t else t₂)
ifCong₃ refl = refl

------------------------------------------------------------------------------
-- Injective properties

succInjective : ∀ {m n} → succ₁ m ≡ succ₁ n → m ≡ n
succInjective {m} {n} h =
  m                ≡⟨ sym (pred-S m) ⟩
  pred₁ (succ₁ m)  ≡⟨ predCong h ⟩
  pred₁ (succ₁ n)  ≡⟨ pred-S n ⟩
  n                ∎

------------------------------------------------------------------------------
-- Discrimination rules

S≢0 : ∀ {n} → succ₁ n ≢ zero
S≢0 S≡0 = 0≢S (sym S≡0)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- {-# OPTIONS -v interaction.case:20 -v tc.cover:20 #-}
-- Andreas, 2015-05-29, issue reported by Stevan Andjelkovic

record Cont : Set₁ where
  constructor _◃_
  field
    Sh  : Set
    Pos : Sh → Set

open Cont

data W (C : Cont) : Set where
  sup : (s : Sh C) (k : Pos C s → W C) → W C

-- If I case split on w:
bogus : {C : Cont} → W C → Set
bogus w = {!w!}

-- WAS internally :  bogus {Sh ◃ Pos} w = ?
-- WAS after split:  bogus {Sh ◃ Pos} (sup s k) = ?
-- NOW internally :  bogus {_} w = ?
-- NOW as expected:  bogus (sup s k) = ?


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Pullback where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.PropositionalTruncation.Base

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Cospan
open import Cubical.Categories.Limits.Limits

private
  variable
    ℓ ℓ' : Level

module _ (C : Category ℓ ℓ') where

  open Category C
  open Functor

  record Cospan : Type (ℓ-max ℓ ℓ') where
    constructor cospan
    field
      l m r : ob
      s₁ : C [ l , m ]
      s₂ : C [ r , m ]

  open Cospan

  isPullback : (cspn : Cospan) →
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → Type (ℓ-max ℓ ℓ')
  isPullback cspn {c} p₁ p₂ H =
    ∀ {d} (h : C [ d , cspn .l ]) (k : C [ d , cspn .r ])
          (H' : h ⋆ cspn .s₁ ≡ k ⋆ cspn .s₂)
    → ∃![ hk ∈ C [ d , c ] ] (h ≡ hk ⋆ p₁) × (k ≡ hk ⋆ p₂)

  isPropIsPullback : (cspn : Cospan) →
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → isProp (isPullback cspn p₁ p₂ H)
  isPropIsPullback cspn p₁ p₂ H =
    isPropImplicitΠ (λ x → isPropΠ3 λ h k H' → isPropIsContr)

  record Pullback (cspn : Cospan) : Type (ℓ-max ℓ ℓ') where
    field
      pbOb  : ob
      pbPr₁ : C [ pbOb , cspn .l ]
      pbPr₂ : C [ pbOb , cspn .r ]
      pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂
      univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes

  open Pullback

  pullbackArrow :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → C [ c , pb . pbOb ]
  pullbackArrow pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .fst

  pullbackArrowPr₁ :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
    p₁ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₁ pb
  pullbackArrowPr₁ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .fst

  pullbackArrowPr₂ :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
    p₂ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₂ pb
  pullbackArrowPr₂ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .snd

  pullbackArrowUnique :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂)
    (pbArrow' : C [ c , pb .pbOb ])
    (H₁ : p₁ ≡ pbArrow' ⋆ pbPr₁ pb) (H₂ : p₂ ≡ pbArrow' ⋆ pbPr₂ pb)
    → pullbackArrow pb p₁ p₂ H ≡ pbArrow'
  pullbackArrowUnique pb p₁ p₂ H pbArrow' H₁ H₂ =
    cong fst (pb .univProp p₁ p₂ H .snd (pbArrow' , (H₁ , H₂)))

  Pullbacks : Type (ℓ-max ℓ ℓ')
  Pullbacks = (cspn : Cospan) → Pullback cspn

  hasPullbacks : Type (ℓ-max ℓ ℓ')
  hasPullbacks = ∥ Pullbacks ∥₁

-- Pullbacks from limits
module _ {C : Category ℓ ℓ'} where
  open Category C
  open Functor
  open Pullback
  open LimCone
  open Cone
  open Cospan

  Cospan→Func : Cospan C → Functor CospanCat C
  Cospan→Func (cospan l m r f g) .F-ob ⓪ = l
  Cospan→Func (cospan l m r f g) .F-ob ① = m
  Cospan→Func (cospan l m r f g) .F-ob ② = r
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {①} k = f
  Cospan→Func (cospan l m r f g) .F-hom {②} {①} k = g
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id
  Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id
  Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id
  Cospan→Func (cospan l m r f g) .F-id {⓪} = refl
  Cospan→Func (cospan l m r f g) .F-id {①} = refl
  Cospan→Func (cospan l m r f g) .F-id {②} = refl
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {⓪} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {①} {①} φ ψ = sym (⋆IdR _)
  Cospan→Func (cospan l m r f g) .F-seq {①} {①} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {②} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {①} {①} φ ψ = sym (⋆IdR _)

  LimitsOfShapeCospanCat→Pullbacks : LimitsOfShape CospanCat C → Pullbacks C
  pbOb (LimitsOfShapeCospanCat→Pullbacks H cspn) = lim (H (Cospan→Func cspn))
  pbPr₁ (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOut (H (Cospan→Func cspn)) ⓪
  pbPr₂ (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOut (H (Cospan→Func cspn)) ②
  pbCommutes (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOutCommutes (H (Cospan→Func cspn)) {v = ①} tt
                          ∙ sym (limOutCommutes (H (Cospan→Func cspn)) tt)
  univProp (LimitsOfShapeCospanCat→Pullbacks H cspn) {d = d} h k H' =
    uniqueExists (limArrow (H (Cospan→Func cspn)) d cc)
                 ( sym (limArrowCommutes (H (Cospan→Func cspn)) d cc ⓪)
                 , sym (limArrowCommutes (H (Cospan→Func cspn)) d cc ②))
                 (λ _ → isProp× (isSetHom _ _) (isSetHom _ _))
                 λ a' ha' → limArrowUnique (H (Cospan→Func cspn)) d cc a'
                               (λ { ⓪ → sym (ha' .fst)
                                  ; ① → cong (a' ⋆_) (sym (limOutCommutes (H (Cospan→Func cspn)) {⓪} {①} tt))
                                      ∙∙ sym (⋆Assoc _ _ _)
                                      ∙∙ cong (_⋆ cspn .s₁) (sym (ha' .fst))
                                  ; ② → sym (ha' .snd) })
    where
    cc : Cone (Cospan→Func cspn) d
    coneOut cc ⓪ = h
    coneOut cc ① = h ⋆ cspn .s₁
    coneOut cc ② = k
    coneOutCommutes cc {⓪} {⓪} e = ⋆IdR h
    coneOutCommutes cc {⓪} {①} e = refl
    coneOutCommutes cc {①} {①} e = ⋆IdR _
    coneOutCommutes cc {②} {①} e = sym H'
    coneOutCommutes cc {②} {②} e = ⋆IdR k

  Limits→Pullbacks : Limits C → Pullbacks C
  Limits→Pullbacks H = LimitsOfShapeCospanCat→Pullbacks (H CospanCat)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.Liveness.RoundState as RoundState
import      LibraBFT.Impl.IO.OBM.GenKeyFile             as GenKeyFile
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
import      LibraBFT.Impl.IO.OBM.Start                  as Start
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Time
import      LibraBFT.Impl.Types.BlockInfo               as BlockInfo
import      LibraBFT.Impl.Types.ValidatorSigner         as ValidatorSigner
open import LibraBFT.Impl.Consensus.RoundManager
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.ByteString
open import Util.Encode
open import Util.Hash
open import Util.KVMap as KVMap
open import Util.Lemmas
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base
import      Yasm.Types as YT

-- This module connects implementation handlers to the interface of the SystemModel.

module LibraBFT.Impl.Handle where

open EpochConfig

------------------------------------------------------------------------------
-- This function works with any implementation of a RoundManager.

-- NOTE: The system layer only cares about this step function.
-- 0 is given as a timestamp.
peerStep : NodeId → NetworkMsg → RoundManager → RoundManager × List (YT.Action NetworkMsg)
peerStep nid msg st = runHandler st (handle nid msg 0)
 where
  -- This invokes an implementation handler.
  runHandler : RoundManager → LBFT Unit → RoundManager × List (YT.Action NetworkMsg)
  runHandler st handler = ×-map₂ (outputsToActions {st}) (proj₂ (LBFT-run handler st))

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

-- This connects the implementation handler to the system model so it can be initialized.

module InitHandler where
  {-
  IMPL-DIFF: In Haskell, nodes are started with a filepath of a file containing
  - number of faults allowed
  - genesis LedgerInfoWithSignatures
  - network addresses/name and secret and public keys of all nodes in the genesis epoch

  Main reads/checks that file then calls a network specific 'run' functions (e.g., ZMQ.hs)
  that setup the network handlers then eventually call 'Start.startViaConsensusProvider'.

  That functions calls 'ConsensusProvider.startConsensus' which returns
  '(EpochManager, [Output]'.

  'Start.startViaConsensusProvider' then goes on to create and wire up internal communication
  channels and starts threads.  The most relevant thread starts up
  `(EpochManager.obmStartLoop epochManager output ...)' to handle the initialization output
  and then to handle new messages from the network.

  In Agda below,
  - we assume 'BootstrapInfo' known to all peers
    - i.e., the same info that Haskell creates via 'GenKeyFile.create'
    - the assumed info is given to 'mkSysInitAndHandlers' in 'InitAndHandlers'
  - System initialization calls 'initHandler'
  - 'initHandler' eventually calls 'initialize'
  - 'initialize' calls 'State.startViaConsensusProvider'
    when then calls 'ConsensusProvider.startConsensus' which returns
    '(EpochManager, List Output)', just like Haskell.
  - Since there is no network, internal channels and threads, this is the end of this process.

  Note: although both the Haskell and Agda version support non-uniform voting, the
  above initialization process assumes one-vote per peer.
  -}

  postulate -- TODO-2: Eliminate when/if timestamps are modeled
    now : Instant

  proposalGenerator : ProposalGenerator
  proposalGenerator = ProposalGenerator∙new 0

  initialize-ed : Instant → GenKeyFile.NfLiwsVsVvPe → EitherD ErrLog (EpochManager × List Output)
  initialize-ed now nfLiwsVsVvPe =
    Start.startViaConsensusProvider-ed-abs
      now nfLiwsVsVvPe
      (TxTypeDependentStuffForNetwork∙new
        proposalGenerator
        (StateComputer∙new BlockInfo.gENESIS_VERSION))

  abstract
    initialize-ed-abs  = initialize-ed
    initialize-ed-abs≡ : initialize-ed-abs ≡ initialize-ed
    initialize-ed-abs≡ = refl

  mkNfLiwsVsVvPe : BootstrapInfo → ValidatorSigner → GenKeyFile.NfLiwsVsVvPe
  mkNfLiwsVsVvPe bsi vs = (bsi ^∙ bsiNumFaults , bsi ^∙ bsiLIWS , vs , bsi ^∙ bsiVV , bsi ^∙ bsiPE)

  -- No need to break this one into steps, no decision points
  initEMWithOutput-ed : BootstrapInfo → ValidatorSigner
                      → EitherD ErrLog (EpochManager × List Output)
  initEMWithOutput-ed  bsi vs =
    initialize-ed-abs now (mkNfLiwsVsVvPe bsi vs)

  abstract
    initEMWithOutput-e-abs : BootstrapInfo → ValidatorSigner
                           → Either ErrLog (EpochManager × List Output)
    initEMWithOutput-e-abs bsi vs = toEither $ initEMWithOutput-ed bsi vs

    initEMWithOutput-ed-abs = initEMWithOutput-ed
    initEMWithOutput-ed-abs≡ : initEMWithOutput-ed-abs ≡ initEMWithOutput-ed
    initEMWithOutput-ed-abs≡ = refl

    -- This shows that the Either and EitherD versions are equivalent.
    -- This is a first step towards eliminating the painful VariantOf stuff,
    -- so we can have the version that looks (almost) exactly like the Haskell,
    -- and the EitherD variant, broken into explicit steps, etc. for proving.
    initEMWithOutput≡
      : ∀ {bsi : BootstrapInfo} {vs : ValidatorSigner}
      → initEMWithOutput-e-abs bsi vs ≡ EitherD-run (initEMWithOutput-ed-abs bsi vs)
    initEMWithOutput≡ {bsi} {vs} = refl

  getEmRm-ed : EpochManager → EitherD ErrLog RoundManager
  getEmRm-ed em =
    case em ^∙ emProcessor of λ where
      nothing  → LeftD fakeErr
      (just p) → case p of λ where
                   (RoundProcessorRecovery _) → LeftD fakeErr
                   (RoundProcessorNormal rm)  → RightD rm
  abstract
    getEmRm-ed-abs : EpochManager → EitherD ErrLog RoundManager
    getEmRm-ed-abs = getEmRm-ed

    getEmRm-ed-abs≡ : getEmRm-ed-abs ≡ getEmRm-ed
    getEmRm-ed-abs≡ = refl

    getEmRm-e-abs : EpochManager → Either ErrLog RoundManager
    getEmRm-e-abs = toEither ∘ getEmRm-ed-abs

  postulate -- TODO
   getEMRM≡
    : ∀ {em : EpochManager}
    → getEmRm-e-abs em ≡ EitherD-run (getEmRm-ed-abs em)

  -- Below is a small exploration in how we define, use, and prove properties about functions in the
  -- Either monad.  We would like to:
  --
  -- * use the EitherD-weakestPre machinery to help structure proofs
  -- * avoid functions being "unrolled" in proof states to make them more readable and proofs more
  --   robust to change
  -- * break functions in to smaller pieces with names and explicit type signatures, making it
  --   easier to employ the EitherD machinery, especially for those not yet fluent using it
  -- * be able to easily compare the Agda code to the Haskell code it models
  --
  -- These desires entail some tradeoffs.  The exploration below helps to illustrate the
  -- possibilities.  We first express the initRMWithOutput function in several different ways, with
  -- different suffixes to clarify which is which.
  --
  -- * initRMWithOutput-e
  --   - An Either version that is virtually identical to the Haskell
  -- * initRMWithOutput-ed
  --   - An EitherD version broken into steps

  -- * Abstract versions of each of these, two for initRMWithOutput-e (initRMWithOutput-e-abs and
  --   initRMWithOutput-e-abs1) and one for initRMWithOutput-ed (initRMWithOutput-ed-abs).
  --   initRMWithOutput-e-abs is defined simply using initRMWithOutput-ed and toEither, whereas
  --   initRMWithOutput-e-abs1 is defined using initRMWithOutput-e.  We also prove below a number of
  --   properties showing that these are all equivalent (in the sense that the Either versions
  --   return the same value as EitherD-run when given the EitherD version).  These proofs serve as
  --   useful rewrites in various proofs, as illustrated in the proof of
  --   initRMWithOutputSpec.contract and of initRMWithOutput-e-versions-≡ below.
  --
  -- While it is nice to have both versions and prove their equivalence (one for relating to Haskell
  -- code, one for proving using the EitherD machinery), it does entail extra work and may be
  -- overkill.  With a little experience, it's probably not too difficult in most cases to compare
  -- the original Haskell code to the EitherD version broken into steps, and to convince oneself
  -- that the latter faithfully reflects the former.  If we keep some examples (such as this one)
  -- showing a function written in Either and an "equivalent" one written in EitherD, broken into
  -- steps, etc. for proof convenience, then this may help people who are not (yet) comfortable with
  -- this translation to become more comfortable.
  --
  -- In some cases, the EitherD proof-friendly version may depart further from the Haskell-like
  -- version, and for such cases, it may be worthwhile to write the Haskell-equivalent version.
  -- This makes proving that the Either and EitherD versions are "equivalent" a bit more work
  -- (compare initRMWithOutput≡ and initRMWithOutput≡' below, and note in particular that the latter
  -- requires properties about the functions called as well).  Of course, writing both versions is
  -- too extra work too.  In general, it's question of judgement whether we're OK with considering
  -- that the Either version defined using toEither and the EitherD version is sufficiently
  -- obviously equivalent to the Haskell code we're modeling.
  --
  -- Tentative conclusion
  --
  -- Default to writing the proof-friendly EitherD version and defining the Either version in terms
  -- of it.  For cases in which the correspondence is judged not to be obvious enough, we can add an
  -- explicit Either version and prove that is is equivalent.
  --
  -- Calling convention
  --
  -- When calling a function within and EitherD function, we should call an abstract version of that
  -- function, which ensures modularity of proofs and readability of proof states by avoiding Agda
  -- "unrolling" defintions prematurely.  Similarly, for cases in which we do write an explicit
  -- Either version and prove it equivalent, we should also call an abstract version of Either
  -- functions.

  -- Relationship to "VariantFor"
  --
  -- We have previously defined variants for functions in EitherLike monads using EL-func (search
  -- for VariantFor).  In light of the above exploration, perhaps that machinery adds less value
  -- than it is worth?  It seems we can get everything we need from following simple conventions as
  -- outlined above.

  initRMWithOutput-e : BootstrapInfo → ValidatorSigner → Either ErrLog (RoundManager × List Output)
  initRMWithOutput-e bsi vs = do
    (em , lo) ← initEMWithOutput-e-abs bsi vs
    rm        ← getEmRm-e-abs em
    Right (rm , lo)

  module initRMWithOutput-ed (bsi : BootstrapInfo) (vs : ValidatorSigner) where
    step₀ : EitherD ErrLog (RoundManager × List Output)
    step₁ : EpochManager × List Output → EitherD ErrLog (RoundManager × List Output)

    step₀ = do
      (em , lo) ← initEMWithOutput-ed-abs bsi vs
      step₁ (em , lo)

    step₁ (em , lo) = do
      rm        ← getEmRm-ed-abs em
      RightD (rm , lo)

  abstract
    initRMWithOutput-e-abs initRMWithOutput-e-abs1
      : BootstrapInfo → ValidatorSigner
      → Either ErrLog (RoundManager × List Output)
    -- Avoids duplication, but eliminates version that looks exactly like the Haskell
    initRMWithOutput-e-abs bsi vs = toEither $ initRMWithOutput-ed.step₀ bsi vs

    initRMWithOutput-ed-abs  = initRMWithOutput-ed.step₀
    initRMWithOutput-ed-abs≡ : initRMWithOutput-ed-abs ≡ initRMWithOutput-ed.step₀
    initRMWithOutput-ed-abs≡ = refl

    initRMWithOutput-e-abs1 = initRMWithOutput-e
    initRMWithOutput-e-abs1≡ : initRMWithOutput-e-abs1 ≡ initRMWithOutput-e
    initRMWithOutput-e-abs1≡ = refl

    initRMWithOutput≡ :
      ∀ {bsi : BootstrapInfo} {vs : ValidatorSigner}
      → initRMWithOutput-e-abs bsi vs ≡ EitherD-run (initRMWithOutput-ed-abs bsi vs)
    initRMWithOutput≡ {bsi} {vs} = refl

  initRMWithOutput≡'
    : ∀ {bsi : BootstrapInfo} {vs : ValidatorSigner}
    → initRMWithOutput-e-abs1 bsi vs ≡ EitherD-run (initRMWithOutput-ed.step₀ bsi vs)
  initRMWithOutput≡' {bsi} {vs} rewrite initRMWithOutput-e-abs1≡ | initEMWithOutput≡ {bsi} {vs}
     with EitherD-run (initEMWithOutput-ed-abs bsi vs)
  ... | Left  x = refl
  ... | Right (em , lo) rewrite getEMRM≡ {em}
     with EitherD-run (getEmRm-ed-abs em)
  ... | Left x  = refl
  ... | Right y = refl

  -- Not used, just for satisfying ourselves that the versions really are equivalent, and
  -- demonstrating the use of the various equivalences for rewriting.
  initRMWithOutput-e-versions-≡ :
    ∀ {bsi} {vs}
    → initRMWithOutput-e-abs1 bsi vs ≡ initRMWithOutput-e-abs bsi vs
  initRMWithOutput-e-versions-≡ {bsi} {vs}
    rewrite initRMWithOutput≡' {bsi} {vs}
          | initRMWithOutput≡  {bsi} {vs}
          | initRMWithOutput-ed-abs≡ = refl

  initHandler : Author → BootstrapInfo → Maybe (RoundManager × List (YT.Action NetworkMsg))
  initHandler pid bsi =
   case ValidatorSigner.obmGetValidatorSigner pid (bsi ^∙ bsiVSS) of λ where
     (Left _)   → nothing
     (Right vs) →
       case initRMWithOutput-e-abs bsi vs of λ where
         (Left _)          → nothing
         (Right (rm , lo)) → just (rm , outputsToActions {State = rm} lo)

  initAndHandlers : SystemInitAndHandlers ℓ-RoundManager ConcSysParms
  initAndHandlers =
    mkSysInitAndHandlers
      fakeBootstrapInfo
      fakeInitRM
      initHandler
      peerStep
   where
    postulate -- TODO-1: eliminate by constructing inhabitants
      bs : BlockStore
      pe : ProposerElection
      rs : RoundState
      sr : SafetyRules
      vv : BootstrapInfo → ValidatorVerifier
    -- For uninitialised peers, so we know nothing about their state.
    -- Construct a value of type `RoundManager` to ensure it is inhabitable.
    fakeInitRM : RoundManager
    fakeInitRM = RoundManager∙new
      ObmNeedFetch∙new
      (EpochState∙new 1 (vv fakeBootstrapInfo))
      bs rs pe proposalGenerator sr false


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax PDiff | PD

type
  * : 0-ary

term
  zero  : * | 𝟘
  add   : *  *  ->  * | _⊕_ l20
  one   : * | 𝟙
  mult  : *  *  ->  * | _⊗_ l20
  neg   : *  ->  * | ⊖_ r50
  pd : *.*  *  ->  * | ∂_∣_

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
  (⊗C) a b |> mult(a, b) = mult(b, a)
  (∂⊕) a : * |> x : * |- d0 (add (x, a)) = one
  (∂⊗) a : * |> x : * |- d0 (mult(a, x)) = a
  (∂C) f : (*,*).* |> x : *  y : * |- d1 (d0 (f[x,y])) = d0 (d1 (f[x,y]))
  (∂Ch₂) f : (*,*).*  g h : *.* |> x : * |- d0 (f[g[x], h[x]]) = add (mult(pd(z. f[z, h[x]], g[x]), d0(g[x])), mult(pd(z. f[g[x], z], h[x]), d0(h[x])))
  (∂Ch₁) f g : *.* |> x : * |- d0 (f[g[x]]) = mult (pd (z. f[z], g[x]), d0(g[x]))
-}

module PDiff.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import PDiff.Signature
open import PDiff.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution PD:Syn
open import SOAS.Metatheory.SecondOrder.Equality PD:Syn

private
  variable
    α β γ τ : *T
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ PD) α Γ → (𝔐 ▷ PD) α Γ → Set where
  𝟘U⊕ᴸ : ⁅ * ⁆̣             ▹     ∅     ⊢               𝟘 ⊕ 𝔞 ≋ₐ 𝔞
  ⊕A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹     ∅     ⊢         (𝔞 ⊕ 𝔟) ⊕ 𝔠 ≋ₐ 𝔞 ⊕ (𝔟 ⊕ 𝔠)
  ⊕C   : ⁅ * ⁆ ⁅ * ⁆̣       ▹     ∅     ⊢               𝔞 ⊕ 𝔟 ≋ₐ 𝔟 ⊕ 𝔞
  𝟙U⊗ᴸ : ⁅ * ⁆̣             ▹     ∅     ⊢               𝟙 ⊗ 𝔞 ≋ₐ 𝔞
  ⊗A   : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹     ∅     ⊢         (𝔞 ⊗ 𝔟) ⊗ 𝔠 ≋ₐ 𝔞 ⊗ (𝔟 ⊗ 𝔠)
  ⊗D⊕ᴸ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹     ∅     ⊢         𝔞 ⊗ (𝔟 ⊕ 𝔠) ≋ₐ (𝔞 ⊗ 𝔟) ⊕ (𝔞 ⊗ 𝔠)
  𝟘X⊗ᴸ : ⁅ * ⁆̣             ▹     ∅     ⊢               𝟘 ⊗ 𝔞 ≋ₐ 𝟘
  ⊖N⊕ᴸ : ⁅ * ⁆̣             ▹     ∅     ⊢           (⊖ 𝔞) ⊕ 𝔞 ≋ₐ 𝟘
  ⊗C   : ⁅ * ⁆ ⁅ * ⁆̣       ▹     ∅     ⊢               𝔞 ⊗ 𝔟 ≋ₐ 𝔟 ⊗ 𝔞
  ∂⊕   : ⁅ * ⁆̣             ▹   ⌊ * ⌋   ⊢         ∂₀ (x₀ ⊕ 𝔞) ≋ₐ 𝟙
  ∂⊗   : ⁅ * ⁆̣             ▹   ⌊ * ⌋   ⊢         ∂₀ (𝔞 ⊗ x₀) ≋ₐ 𝔞
  ∂C   : ⁅ * · * ⊩ * ⁆̣     ▹ ⌊ * ∙ * ⌋ ⊢  ∂₁ ∂₀ 𝔞⟨ x₀ ◂ x₁ ⟩ ≋ₐ ∂₀ ∂₁ 𝔞⟨ x₀ ◂ x₁ ⟩
  ∂Ch₂ : ⁅ * · * ⊩ * ⁆ ⁅ * ⊩ * ⁆ ⁅ * ⊩ * ⁆̣ ▹ ⌊ * ⌋
       ⊢ ∂₀ 𝔞⟨ (𝔟⟨ x₀ ⟩) ◂ (𝔠⟨ x₀ ⟩) ⟩ ≋ₐ ((∂ 𝔞⟨ x₀ ◂ (𝔠⟨ x₁ ⟩) ⟩ ∣ 𝔟⟨ x₀ ⟩) ⊗ (∂₀ 𝔟⟨ x₀ ⟩))
                                       ⊕ ((∂ 𝔞⟨ (𝔟⟨ x₁ ⟩) ◂ x₀ ⟩ ∣ 𝔠⟨ x₀ ⟩) ⊗ (∂₀ 𝔠⟨ x₀ ⟩))

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

-- Derived equations
𝟘U⊕ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊕ 𝟘 ≋ 𝔞
𝟘U⊕ᴿ = tr (ax ⊕C with《 𝔞 ◃ 𝟘 》) (ax 𝟘U⊕ᴸ with《 𝔞 》)
𝟙U⊗ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊗ 𝟙 ≋ 𝔞
𝟙U⊗ᴿ = tr (ax ⊗C with《 𝔞 ◃ 𝟙 》) (ax 𝟙U⊗ᴸ with《 𝔞 》)
⊗D⊕ᴿ : ⁅ * ⁆ ⁅ * ⁆ ⁅ * ⁆̣ ▹ ∅ ⊢ (𝔞 ⊕ 𝔟) ⊗ 𝔠 ≋ (𝔞 ⊗ 𝔠) ⊕ (𝔟 ⊗ 𝔠)
⊗D⊕ᴿ = begin
  (𝔞 ⊕ 𝔟) ⊗ 𝔠       ≋⟨ ax ⊗C with《 𝔞 ⊕ 𝔟 ◃ 𝔠 》 ⟩
  𝔠 ⊗ (𝔞 ⊕ 𝔟)       ≋⟨ ax ⊗D⊕ᴸ with《 𝔠 ◃ 𝔞 ◃ 𝔟 》 ⟩
  (𝔠 ⊗ 𝔞) ⊕ (𝔠 ⊗ 𝔟)  ≋⟨ cong₂[ ax ⊗C with《 𝔠 ◃ 𝔞 》 ][ ax ⊗C with《 𝔠 ◃ 𝔟 》 ]inside ◌ᵈ ⊕ ◌ᵉ ⟩
  (𝔞 ⊗ 𝔠) ⊕ (𝔟 ⊗ 𝔠)  ∎
𝟘X⊗ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊗ 𝟘 ≋ 𝟘
𝟘X⊗ᴿ = tr (ax ⊗C with《 𝔞 ◃ 𝟘 》) (ax 𝟘X⊗ᴸ with《 𝔞 》)
⊖N⊕ᴿ : ⁅ * ⁆̣ ▹ ∅ ⊢ 𝔞 ⊕ (⊖ 𝔞) ≋ 𝟘
⊖N⊕ᴿ = tr (ax ⊕C with《 𝔞 ◃ (⊖ 𝔞) 》) (ax ⊖N⊕ᴸ with《 𝔞 》)

-- Derivative of a variable is 1
∂id : ⁅⁆ ▹ ⌊ * ⌋ ⊢ ∂₀ x₀ ≋ 𝟙
∂id = begin
      ∂₀ x₀       ≋⟨ cong[ thm 𝟘U⊕ᴿ with《 x₀ 》 ]inside ∂₀ ◌ᵃ ⟩ₛ
      ∂₀ (x₀ ⊕ 𝟘) ≋⟨ ax ∂⊕ with《 𝟘 》 ⟩
      𝟙           ∎

-- Derivative of 0 is 0
∂𝟘 : ⁅⁆ ▹ ⌊ * ⌋ ⊢ ∂₀ 𝟘 ≋ 𝟘
∂𝟘 = begin
      ∂₀ 𝟘         ≋⟨ cong[ ax 𝟘X⊗ᴸ with《 x₀ 》 ]inside ∂₀ ◌ᵃ ⟩ₛ
      ∂₀ (𝟘 ⊗ x₀)  ≋⟨ ax ∂⊗ with《 𝟘 》 ⟩
      𝟘            ∎

-- Unary chain rule
∂Ch₁ : ⁅ * ⊩ * ⁆ ⁅ * ⊩ * ⁆̣ ▹ ⌊ * ⌋
     ⊢ ∂₀ 𝔞⟨ (𝔟⟨ x₀ ⟩) ⟩ ≋ (∂ 𝔞⟨ x₀ ⟩ ∣ 𝔟⟨ x₀ ⟩) ⊗ (∂₀ 𝔟⟨ x₀ ⟩)
∂Ch₁ = begin
      ∂₀ (𝔞⟨ (𝔟⟨ x₀ ⟩) ⟩)
  ≋⟨ ax ∂Ch₂ with《 𝔞⟨ x₀ ⟩ ◃ 𝔟⟨ x₀ ⟩ ◃ 𝟘 》 ⟩
        (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩))
      ⊕ ((∂ 𝔞⟨ (𝔟⟨ x₁ ⟩) ⟩ ∣ 𝟘) ⊗ (∂₀ 𝟘))
  ≋⟨ cong[ thm ∂𝟘 ]inside (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩)) ⊕
                          ((∂ 𝔞⟨ (𝔟⟨ x₁ ⟩) ⟩ ∣ 𝟘) ⊗ ◌ᶜ) ⟩
        (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩))
      ⊕ (∂ 𝔞⟨ (𝔟⟨ x₁ ⟩) ⟩ ∣ 𝟘) ⊗ 𝟘
  ≋⟨ cong[ thm 𝟘X⊗ᴿ with《 (∂ 𝔞⟨ (𝔟⟨ x₁ ⟩) ⟩ ∣ 𝟘) 》 ]inside (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩)) ⊕ ◌ᶜ ⟩
        (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩))
      ⊕ 𝟘
  ≋⟨ thm 𝟘U⊕ᴿ with《 (∂ 𝔞⟨ x₀ ⟩ ∣ (𝔟⟨ x₀ ⟩)) ⊗ (∂₀ (𝔟⟨ x₀ ⟩)) 》 ⟩
      (∂ 𝔞⟨ x₀ ⟩ ∣ 𝔟⟨ x₀ ⟩) ⊗ (∂₀ 𝔟⟨ x₀ ⟩)
  ∎

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

module Definition.Typed.Reduction where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties

-- Weak head expansion of type equality
reduction : ∀ {A A′ B B′ r Γ}
          → Γ ⊢ A ⇒* A′ ^ r
          → Γ ⊢ B ⇒* B′ ^ r
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A′ ≡ B′ ^ r
          → Γ ⊢ A ≡ B ^ r
reduction D D′ whnfA′ whnfB′ A′≡B′ =
  trans (subset* D) (trans A′≡B′ (sym (subset* D′)))

reduction′ : ∀ {A A′ B B′ r Γ}
          → Γ ⊢ A ⇒* A′ ^ r
          → Γ ⊢ B ⇒* B′ ^ r
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A ≡ B ^ r
          → Γ ⊢ A′ ≡ B′ ^ r
reduction′ D D′ whnfA′ whnfB′ A≡B =
  trans (sym (subset* D)) (trans A≡B (subset* D′))

-- Weak head expansion of term equality
reductionₜ : ∀ {a a′ b b′ A B l Γ}
           → Γ ⊢ A ⇒* B ^ [ ! , l ]
           → Γ ⊢ a ⇒* a′ ∷ B ^ l
           → Γ ⊢ b ⇒* b′ ∷ B ^ l
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a′ ≡ b′ ∷ B ^ [ ! , l ]
           → Γ ⊢ a ≡ b ∷ A ^ [ ! , l ]
reductionₜ D d d′ whnfB whnfA′ whnfB′ a′≡b′ =
  conv (trans (subset*Term d)
              (trans a′≡b′ (sym (subset*Term d′))))
       (sym (subset* D))

reductionₜ′ : ∀ {a a′ b b′ A B l Γ}
           → Γ ⊢ A ⇒* B ^ [ ! , l ]
           → Γ ⊢ a ⇒* a′ ∷ B ^ l
           → Γ ⊢ b ⇒* b′ ∷ B ^ l
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a ≡ b ∷ A ^ [ ! , l ]
           → Γ ⊢ a′ ≡ b′ ∷ B ^ [ ! , l ]
reductionₜ′ D d d′ whnfB whnfA′ whnfB′ a≡b =
  trans (sym (subset*Term d))
        (trans (conv a≡b (subset* D)) (subset*Term d′))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt