text:
------------------------------------------------------------------------
-- Inductive axiomatisation of subtyping
------------------------------------------------------------------------

module RecursiveTypes.Subtyping.Axiomatic.Inductive where

open import Codata.Musical.Notation
open import Data.Nat using (ℕ; zero; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Relation.Unary.Any as Any using (Any)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (module Inverse)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

open import RecursiveTypes.Syntax
open import RecursiveTypes.Syntax.UnfoldedOrFixpoint
open import RecursiveTypes.Substitution using (unfold[μ_⟶_])
import RecursiveTypes.Subterm as ST
import RecursiveTypes.Subterm.RestrictedHypothesis as Restricted
open import RecursiveTypes.Subtyping.Semantic.Coinductive as Sem
  using (_≤Coind_)
open import RecursiveTypes.Subtyping.Axiomatic.Coinductive as Ax
  using (_≤_; ⊥; ⊤; _⟶_; unfold; fold; _∎; _≤⟨_⟩_)

------------------------------------------------------------------------
-- Definition

infixr 10 _⟶_
infix  4  _⊢_≤_
infix  3  _∎
infixr 2  _≤⟨_⟩_

-- This inductive subtyping relation is parameterised on a list of
-- hypotheses. Note Brandt and Henglein's unusual definition of _⟶_.

data _⊢_≤_ {n} (A : List (Hyp n)) : Ty n → Ty n → Set where
  -- Structural rules.
  ⊥   : ∀ {τ} → A ⊢ ⊥ ≤ τ
  ⊤   : ∀ {σ} → A ⊢ σ ≤ ⊤
  _⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂} →
        let H = σ₁ ⟶ σ₂ ≲ τ₁ ⟶ τ₂ in
        (τ₁≤σ₁ : H ∷ A ⊢ τ₁ ≤ σ₁) (σ₂≤τ₂ : H ∷ A ⊢ σ₂ ≤ τ₂) →
        A ⊢ σ₁ ⟶ σ₂ ≤ τ₁ ⟶ τ₂

  -- Rules for folding and unfolding μ.
  unfold : ∀ {τ₁ τ₂} → A ⊢ μ τ₁ ⟶ τ₂ ≤ unfold[μ τ₁ ⟶ τ₂ ]
  fold   : ∀ {τ₁ τ₂} → A ⊢ unfold[μ τ₁ ⟶ τ₂ ] ≤ μ τ₁ ⟶ τ₂

  -- Reflexivity.
  _∎ : ∀ τ → A ⊢ τ ≤ τ

  -- Transitivity.
  _≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃}
           (τ₁≤τ₂ : A ⊢ τ₁ ≤ τ₂) (τ₂≤τ₃ : A ⊢ τ₂ ≤ τ₃) → A ⊢ τ₁ ≤ τ₃

  -- Hypothesis.
  hyp : ∀ {σ τ} (σ≤τ : (σ ≲ τ) ∈ A) → A ⊢ σ ≤ τ

------------------------------------------------------------------------
-- Soundness

-- A hypothesis is valid if there is a corresponding proof.

Valid : ∀ {n} → (Ty n → Ty n → Set) → Hyp n → Set
Valid _≤_ (σ₁ ≲ σ₂) = σ₁ ≤ σ₂

module Soundness where

  -- The soundness proof uses my trick to show that the code is
  -- productive.

  infixr 10 _⟶_
  infix   4 _≤P_ _≤W_
  infixr  2 _≤⟨_⟩_

  mutual

    -- Soundness proof programs.

    data _≤P_ {n} : Ty n → Ty n → Set where
      sound : ∀ {A σ τ} →
              (valid : All (Valid _≤W_) A) (σ≤τ : A ⊢ σ ≤ τ) → σ ≤P τ

    -- Weak head normal forms of soundness proof programs. Note that
    -- _⟶_ takes (suspended) /programs/ as arguments, while _≤⟨_⟩_
    -- takes /WHNFs/.

    data _≤W_ {n} : Ty n → Ty n → Set where
      done   : ∀ {σ τ} (σ≤τ : σ ≤ τ) → σ ≤W τ
      _⟶_    : ∀ {σ₁ σ₂ τ₁ τ₂}
               (τ₁≤σ₁ : ∞ (τ₁ ≤P σ₁)) (σ₂≤τ₂ : ∞ (σ₂ ≤P τ₂)) →
               σ₁ ⟶ σ₂ ≤W τ₁ ⟶ τ₂
      _≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃}
               (τ₁≤τ₂ : τ₁ ≤W τ₂) (τ₂≤τ₃ : τ₂ ≤W τ₃) → τ₁ ≤W τ₃

  -- The following two functions compute the WHNF of a soundness
  -- program. Note the circular, but productive, definition of proof
  -- below.

  soundW : ∀ {n} {σ τ : Ty n} {A} →
           All (Valid _≤W_) A → A ⊢ σ ≤ τ → σ ≤W τ
  soundW valid ⊥                     = done ⊥
  soundW valid ⊤                     = done ⊤
  soundW valid unfold                = done unfold
  soundW valid fold                  = done fold
  soundW valid (τ ∎)                 = done (τ ∎)
  soundW valid (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = τ₁ ≤⟨ soundW valid τ₁≤τ₂ ⟩
                                             soundW valid τ₂≤τ₃
  soundW valid (hyp σ≤τ)             = All.lookup valid σ≤τ
  soundW valid (τ₁≤σ₁ ⟶ σ₂≤τ₂)       = proof
    where
    proof : _ ≤W _
    proof = ♯ sound (proof ∷ valid) τ₁≤σ₁ ⟶
            ♯ sound (proof ∷ valid) σ₂≤τ₂

  whnf : ∀ {n} {σ τ : Ty n} →
         σ ≤P τ → σ ≤W τ
  whnf (sound valid σ≤τ) = soundW valid σ≤τ

  -- Computes actual proofs.

  mutual

    ⟦_⟧W : ∀ {n} {σ τ : Ty n} → σ ≤W τ → σ ≤ τ
    ⟦ done σ≤τ            ⟧W = σ≤τ
    ⟦ τ₁≤σ₁ ⟶ σ₂≤τ₂       ⟧W = ♯ ⟦ ♭ τ₁≤σ₁ ⟧P ⟶ ♯ ⟦ ♭ σ₂≤τ₂ ⟧P
    ⟦ τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃ ⟧W = τ₁ ≤⟨ ⟦ τ₁≤τ₂ ⟧W ⟩ ⟦ τ₂≤τ₃ ⟧W

    ⟦_⟧P : ∀ {n} {σ τ : Ty n} → σ ≤P τ → σ ≤ τ
    ⟦ σ≤τ ⟧P = ⟦ whnf σ≤τ ⟧W

-- The subtyping relation defined above is sound with respect to the
-- others.

sound : ∀ {n A} {σ τ : Ty n} →
        All (Valid _≤_) A → A ⊢ σ ≤ τ → σ ≤ τ
sound {n} valid σ≤τ =
  ⟦ S.sound (All.map (λ {h} → done′ h) valid) σ≤τ ⟧P
  where
  open module S = Soundness

  done′ : (σ₁≲σ₂ : Hyp n) → Valid _≤_ σ₁≲σ₂ → Valid _≤W_ σ₁≲σ₂
  done′ (_ ≲ _) = done

------------------------------------------------------------------------
-- The subtyping relation is decidable

module Decidable {n} (χ₁ χ₂ : Ty n) where

  open Restricted χ₁ χ₂

  -- The proof below is not optimised for speed. (See Gapeyev, Levin
  -- and Pierce's "Recursive Subtyping Revealed" from ICFP '00 for
  -- more information about the complexity of subtyping algorithms.)

  mutual

    -- A wrapper which applies the U∨Μ view.

    _⊢_,_≤?_,_ : ∀ {A ℓ} → A ⊕ ℓ →
                 ∀ σ → Subterm σ → ∀ τ → Subterm τ →
                 ⟨ A ⟩⋆ ⊢ σ ≤ τ ⊎ (¬ σ ≤Coind τ)
    T ⊢ σ , σ⊑ ≤? τ , τ⊑ = T ⊩ u∨μ σ , σ⊑ ≤? u∨μ τ , τ⊑

    -- _⊩_,_≤?_,_ unfolds fixpoints. Note that at least one U∨Μ
    -- argument becomes smaller in each recursive call, while ℓ, an
    -- upper bound on the number of pairs of types yet to be
    -- inspected, is preserved.

    _⊩_,_≤?_,_ : ∀ {A ℓ} → A ⊕ ℓ →
                 ∀ {σ τ} → U∨Μ σ → Subterm σ → U∨Μ τ → Subterm τ →
                 ⟨ A ⟩⋆ ⊢ σ ≤ τ ⊎ (¬ σ ≤Coind τ)

    T ⊩ fixpoint {σ₁} {σ₂} u , σ⊑ ≤? τ , τ⊑ =
      Sum.map (λ ≤τ → μ σ₁ ⟶ σ₂           ≤⟨ unfold ⟩
                      unfold[μ σ₁ ⟶ σ₂ ]  ≤⟨ ≤τ ⟩
                      u∨μ⁻¹ τ             ∎)
              (λ ≰τ ≤τ → ≰τ (Sem.trans Sem.fold ≤τ))
              (T ⊩ u , anti-mono ST.unfold′ σ⊑ ≤? τ , τ⊑)
    T ⊩ σ , σ⊑ ≤? fixpoint {τ₁} {τ₂} u , τ⊑ =
      Sum.map (λ σ≤ → u∨μ⁻¹ σ             ≤⟨ σ≤ ⟩
                      unfold[μ τ₁ ⟶ τ₂ ]  ≤⟨ fold ⟩
                      μ τ₁ ⟶ τ₂           ∎)
              (λ σ≰ σ≤ → σ≰ (Sem.trans σ≤ Sem.unfold))
              (T ⊩ σ , σ⊑ ≤? u , anti-mono ST.unfold′ τ⊑)

    T ⊩ unfolded σ , σ⊑ ≤? unfolded τ , τ⊑ = T ⊪ σ , σ⊑ ≤? τ , τ⊑

    -- _⊪_,_≤?_,_ handles the structural cases. Note that ℓ becomes
    -- smaller in each recursive call.

    _⊪_,_≤?_,_ : ∀ {A ℓ} → A ⊕ ℓ →
                 ∀ {σ} → Unfolded σ → Subterm σ →
                 ∀ {τ} → Unfolded τ → Subterm τ →
                 ⟨ A ⟩⋆ ⊢ σ ≤ τ ⊎ (¬ σ ≤Coind τ)
    T ⊪ ⊥ , _ ≤? τ , _ = inj₁ ⊥
    T ⊪ σ , _ ≤? ⊤ , _ = inj₁ ⊤

    T ⊪ var x , _ ≤? var y , _ = helper (var x ≡? var y)
      where
      helper : ∀ {A x y} → Dec ((Ty n ∋ var x) ≡ var y) →
               ⟨ A ⟩⋆ ⊢ var x ≤ var y ⊎ ¬ var x ≤Coind var y
      helper (yes refl) = inj₁ (var _ ∎)
      helper (no  x≠y)  = inj₂ (x≠y ∘ Sem.var:≤∞⟶≡)

    _⊪_,_≤?_,_ {A} T (σ₁ ⟶ σ₂) σ⊑ (τ₁ ⟶ τ₂) τ⊑ =
      helper (lookupOrInsert T H)
      where
      H = (-, σ⊑) ≲ (-, τ⊑)

      helper₂ :
        ⟨ H ∷ A ⟩⋆ ⊢ τ₁      ≤ σ₁      ⊎ ¬ τ₁      ≤Coind σ₁      →
        ⟨ H ∷ A ⟩⋆ ⊢      σ₂ ≤      τ₂ ⊎ ¬      σ₂ ≤Coind      τ₂ →
        ⟨     A ⟩⋆ ⊢ σ₁ ⟶ σ₂ ≤ τ₁ ⟶ τ₂ ⊎ ¬ σ₁ ⟶ σ₂ ≤Coind τ₁ ⟶ τ₂
      helper₂ (inj₁ ≤₁) (inj₁ ≤₂) = inj₁ (≤₁ ⟶ ≤₂)
      helper₂ (inj₂ ≰ ) (_      ) = inj₂ (≰ ∘  Sem.left-proj)
      helper₂ (_      ) (inj₂ ≰ ) = inj₂ (≰ ∘ Sem.right-proj)

      helper : ∀ {ℓ} → Any (_≈_ H) A ⊎ (∃ λ n → ℓ ≡ suc n × H ∷ A ⊕ n) →
               ⟨ A ⟩⋆ ⊢ σ₁ ⟶ σ₂ ≤ τ₁ ⟶ τ₂ ⊎ ¬ σ₁ ⟶ σ₂ ≤Coind τ₁ ⟶ τ₂
      helper (inj₁ σ≲τ)             = inj₁ $ hyp $ Inverse.to map↔ ⟨$⟩ σ≲τ
      helper (inj₂ (_ , refl , T′)) = helper₂
        (T′ ⊢ τ₁ , anti-mono ST.⟶ˡ′ τ⊑ ≤? σ₁ , anti-mono ST.⟶ˡ′ σ⊑)
        (T′ ⊢ σ₂ , anti-mono ST.⟶ʳ′ σ⊑ ≤? τ₂ , anti-mono ST.⟶ʳ′ τ⊑)

    T ⊪ ⊤       , _ ≤? ⊥       , _ = inj₂ (λ ())
    T ⊪ ⊤       , _ ≤? var x   , _ = inj₂ (λ ())
    T ⊪ ⊤       , _ ≤? τ₁ ⟶ τ₂ , _ = inj₂ (λ ())
    T ⊪ var x   , _ ≤? ⊥       , _ = inj₂ (λ ())
    T ⊪ var x   , _ ≤? τ₁ ⟶ τ₂ , _ = inj₂ (λ ())
    T ⊪ σ₁ ⟶ σ₂ , _ ≤? ⊥       , _ = inj₂ (λ ())
    T ⊪ σ₁ ⟶ σ₂ , _ ≤? var x   , _ = inj₂ (λ ())

  -- Finally we have to prove that an upper bound ℓ actually exists.

  dec : [] ⊢ χ₁ ≤ χ₂ ⊎ (¬ χ₁ ≤ χ₂)
  dec = Sum.map id (λ σ≰τ → σ≰τ ∘ Ax.sound)
          (empty ⊢ χ₁ , inj₁ ST.refl ≤? χ₂ , inj₂ ST.refl)

infix 4 []⊢_≤?_ _≤?_

-- The subtyping relation defined above is decidable (when the set of
-- assumptions is empty).

[]⊢_≤?_ : ∀ {n} (σ τ : Ty n) → Dec ([] ⊢ σ ≤ τ)
[]⊢ σ ≤? τ with Decidable.dec σ τ
... | inj₁ σ≤τ = yes σ≤τ
... | inj₂ σ≰τ = no (σ≰τ ∘ sound [])

-- The other subtyping relations can also be decided.

_≤?_ : ∀ {n} (σ τ : Ty n) → Dec (σ ≤ τ)
σ ≤? τ with Decidable.dec σ τ
... | inj₁ σ≤τ = yes (sound [] σ≤τ)
... | inj₂ σ≰τ = no σ≰τ

------------------------------------------------------------------------
-- Completeness

-- Weakening (at the end of the list of assumptions).

weaken : ∀ {n A A′} {σ τ : Ty n} →
         A ⊢ σ ≤ τ → A ++ A′ ⊢ σ ≤ τ
weaken ⊥                     = ⊥
weaken ⊤                     = ⊤
weaken unfold                = unfold
weaken fold                  = fold
weaken (τ ∎)                 = τ ∎
weaken (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = τ₁ ≤⟨ weaken τ₁≤τ₂ ⟩ weaken τ₂≤τ₃
weaken (hyp h)               = hyp (Inverse.to ++↔ ⟨$⟩ inj₁ h)
weaken (τ₁≤σ₁ ⟶ σ₂≤τ₂)       = weaken τ₁≤σ₁ ⟶ weaken σ₂≤τ₂

-- The subtyping relation defined above is complete with respect to
-- the others.

complete : ∀ {n A} {σ τ : Ty n} →
           σ ≤ τ → A ⊢ σ ≤ τ
complete {σ = σ} {τ} σ≤τ with Decidable.dec σ τ
... | inj₁ []⊢σ≤τ = weaken []⊢σ≤τ
... | inj₂ σ≰τ    with σ≰τ σ≤τ
...   | ()

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Prelude

module Implicits.Semantics.Context where

open import Implicits.Syntax
open import Implicits.Semantics.Type
open import SystemF.Everything as F using ()

open import Data.Vec

⟦_⟧ctx→ : ∀ {ν n} → Ctx ν n → F.Ctx ν n
⟦ Γ ⟧ctx→ = map ⟦_⟧tp→ Γ

ext: agda


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.CommutingSquare

module lib.types.Span where

record Span {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor span
  field
    A : Type i
    B : Type j
    C : Type k
    f : C → A
    g : C → B

private
  span=-raw : ∀ {i j k} {A A' : Type i} (p : A == A')
    {B B' : Type j} (q : B == B') {C C' : Type k} (r : C == C')
    {f : C → A} {f' : C' → A'}
    (s : f == f' [ (λ CA → fst CA → snd CA) ↓ pair×= r p ])
    {g : C → B} {g' : C' → B'}
    (t : g == g' [ (λ CB → fst CB → snd CB) ↓ pair×= r q ])
    → (span A B C f g) == (span A' B' C' f' g')
  span=-raw idp idp idp idp idp = idp

abstract
  span= : ∀ {i j k} {A A' : Type i} (p : A ≃ A')
    {B B' : Type j} (q : B ≃ B') {C C' : Type k} (r : C ≃ C')
    {f : C → A} {f' : C' → A'} (s : (a : C) → (–> p) (f a) == f' (–> r a))
    {g : C → B} {g' : C' → B'} (t : (b : C) → (–> q) (g b) == g' (–> r b))
    → (span A B C f g) == (span A' B' C' f' g')
  span= p q r {f} {f'} s {g} {g'} t = span=-raw
    (ua p)
    (ua q)
    (ua r)
    (↓-→-in (λ α → ↓-snd×-in (ua r) (ua p) (↓-idf-ua-in p (
                   s _
                   ∙ ap f' (↓-idf-ua-out r (↓-fst×-out (ua r) (ua p) α))))))
    (↓-→-in (λ β → ↓-snd×-in (ua r) (ua q) (↓-idf-ua-in q (
                   t _
                   ∙ ap g' (↓-idf-ua-out r (↓-fst×-out (ua r) (ua q) β))))))

record ⊙Span {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor ⊙span
  field
    X : Ptd i
    Y : Ptd j
    Z : Ptd k
    f : Z ⊙→ X
    g : Z ⊙→ Y

⊙Span-to-Span : ∀ {i j k} → ⊙Span {i} {j} {k} → Span {i} {j} {k}
⊙Span-to-Span (⊙span X Y Z f g) = span (de⊙ X) (de⊙ Y) (de⊙ Z) (fst f) (fst g)

{- Helper for path induction on pointed spans -}
⊙span-J : ∀ {i j k l} (P : ⊙Span {i} {j} {k} → Type l)
  → ({A : Type i} {B : Type j} {Z : Ptd k} (f : de⊙ Z → A) (g : de⊙ Z → B)
     → P (⊙span ⊙[ A , f (pt Z) ] ⊙[ B , g (pt Z) ] Z (f , idp) (g , idp)))
  → Π ⊙Span P
⊙span-J P t (⊙span ⊙[ A , ._ ] ⊙[ B , ._ ] Z (f , idp) (g , idp)) = t f g

{- Span-flipping functions -}
Span-flip : ∀ {i j k} → Span {i} {j} {k} → Span {j} {i} {k}
Span-flip (span A B C f g) = span B A C g f

⊙Span-flip : ∀ {i j k} → ⊙Span {i} {j} {k} → ⊙Span {j} {i} {k}
⊙Span-flip (⊙span X Y Z f g) = ⊙span Y X Z g f

record SpanMap {i₀ j₀ k₀ i₁ j₁ k₁} (span₀ : Span {i₀} {j₀} {k₀}) (span₁ : Span {i₁} {j₁} {k₁})
  : Type (lmax (lmax (lmax i₀ j₀) k₀) (lmax (lmax i₁ j₁) k₁)) where
  constructor span-map
  module span₀ = Span span₀
  module span₁ = Span span₁
  field
    hA : span₀.A → span₁.A
    hB : span₀.B → span₁.B
    hC : span₀.C → span₁.C
    f-commutes : CommSquare span₀.f span₁.f hC hA
    g-commutes : CommSquare span₀.g span₁.g hC hB

SpanMap-∘ : ∀ {i₀ j₀ k₀ i₁ j₁ k₁ i₂ j₂ k₂} {span₀ : Span {i₀} {j₀} {k₀}}
  {span₁ : Span {i₁} {j₁} {k₁}} {span₂ : Span {i₂} {j₂} {k₂}}
  → SpanMap span₁ span₂ → SpanMap span₀ span₁ → SpanMap span₀ span₂
SpanMap-∘ span-map₁₂ span-map₀₁ = record {
  hA = span-map₁₂.hA ∘ span-map₀₁.hA;
  hB = span-map₁₂.hB ∘ span-map₀₁.hB;
  hC = span-map₁₂.hC ∘ span-map₀₁.hC;
  f-commutes = CommSquare-∘v span-map₁₂.f-commutes span-map₀₁.f-commutes;
  g-commutes = CommSquare-∘v span-map₁₂.g-commutes span-map₀₁.g-commutes}
  where module span-map₀₁ = SpanMap span-map₀₁
        module span-map₁₂ = SpanMap span-map₁₂

SpanEquiv : ∀ {i₀ j₀ k₀ i₁ j₁ k₁} (span₀ : Span {i₀} {j₀} {k₀}) (span₁ : Span {i₁} {j₁} {k₁})
  → Type (lmax (lmax (lmax i₀ j₀) k₀) (lmax (lmax i₁ j₁) k₁))
SpanEquiv span₀ span₁ = Σ (SpanMap span₀ span₁)
  (λ span-map → is-equiv (SpanMap.hA span-map)
              × is-equiv (SpanMap.hB span-map)
              × is-equiv (SpanMap.hC span-map))

SpanEquiv-inverse : ∀ {i₀ j₀ k₀ i₁ j₁ k₁} {span₀ : Span {i₀} {j₀} {k₀}} {span₁ : Span {i₁} {j₁} {k₁}}
  → SpanEquiv span₀ span₁ → SpanEquiv span₁ span₀
SpanEquiv-inverse (span-map hA hB hC f-commutes g-commutes , hA-ise , hB-ise , hC-ise)
  = ( span-map hA.g hB.g hC.g
      (CommSquare-inverse-v f-commutes hC-ise hA-ise)
      (CommSquare-inverse-v g-commutes hC-ise hB-ise)
    , ( is-equiv-inverse hA-ise
      , is-equiv-inverse hB-ise
      , is-equiv-inverse hC-ise))
  where module hA = is-equiv hA-ise
        module hB = is-equiv hB-ise
        module hC = is-equiv hC-ise

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT

module homotopy.AnyUniversalCoverIsPathSet {i} (X : Ptd i) where

private
  a₁ = pt X

path-set-is-universal : is-universal (path-set-cover X)
path-set-is-universal = has-level-in ([ pt X , idp₀ ] ,
  Trunc-elim
    {P = λ xp₀ → [ pt X , idp₀ ] == xp₀}
    (λ{(x , p₀) → Trunc-elim
      {P = λ p₀ → [ pt X , idp₀ ] == [ x , p₀ ]}
      (λ p → ap [_] $ pair= p (lemma p))
      p₀ }))
  where
    lemma : ∀ {x} (p : pt X == x) → idp₀ == [ p ] [ (pt X =₀_) ↓ p ]
    lemma idp = idp

module _ {j} (univ-cov : ⊙UniversalCover X j) where
  private
    module univ-cov = ⊙UniversalCover univ-cov
    instance _ = univ-cov.is-univ

    -- One-to-one mapping between the universal cover
    -- and the truncated path spaces from one point.

    [path] : ∀ (a⇑₁ a⇑₂ : univ-cov.TotalSpace) → a⇑₁ =₀ a⇑₂
    [path] a⇑₁ a⇑₂ = –> (Trunc=-equiv [ a⇑₁ ] [ a⇑₂ ])
      (contr-has-all-paths [ a⇑₁ ] [ a⇑₂ ])

    abstract
      [path]-has-all-paths :
        ∀ {a⇑₁ a⇑₂ : univ-cov.TotalSpace}
        → has-all-paths (a⇑₁ =₀ a⇑₂)
      [path]-has-all-paths {a⇑₁} {a⇑₂} =
        transport has-all-paths (ua (Trunc=-equiv [ a⇑₁ ] [ a⇑₂ ])) $
          contr-has-all-paths {{has-level-apply (raise-level -2 univ-cov.is-univ) [ a⇑₁ ] [ a⇑₂ ]}}

    to : ∀ {a₂} → univ-cov.Fiber a₂ → a₁ =₀ a₂
    to {a₂} a⇑₂ = ap₀ fst ([path] (a₁ , univ-cov.pt) (a₂ , a⇑₂))

    from : ∀ {a₂} → a₁ =₀ a₂ → univ-cov.Fiber a₂
    from p = cover-trace univ-cov.cov univ-cov.pt p

    abstract
      to-from : ∀ {a₂} (p : a₁ =₀ a₂) → to (from p) == p
      to-from = Trunc-elim
        (λ p → lemma p)
        where
          lemma : ∀ {a₂} (p : a₁ == a₂) → to (from [ p ]) == [ p ]
          lemma idp =
            ap₀ fst ([path] (a₁ , univ-cov.pt) (a₁ , univ-cov.pt))
              =⟨ ap (ap₀ fst)
                    $ [path]-has-all-paths
                      ([path] (a₁ , univ-cov.pt) (a₁ , univ-cov.pt))
                      (idp₀ :> ((a₁ , univ-cov.pt) =₀ (a₁ , univ-cov.pt))) ⟩
            (idp₀ :> (a₁ =₀ a₁))
              ∎

      from-to : ∀ {a₂} (a⇑₂ : univ-cov.Fiber a₂) → from (to a⇑₂) == a⇑₂
      from-to {a₂} a⇑₂ = Trunc-elim
        {{λ p → =-preserves-level
                {x = from (ap₀ fst p)}
                {y = a⇑₂}
                univ-cov.Fiber-is-set}}
        (λ p → to-transp $ snd= p)
        ([path] (a₁ , univ-cov.pt) (a₂ , a⇑₂))

  theorem : ∀ a₂ → univ-cov.Fiber a₂ ≃ (a₁ =₀ a₂)
  theorem a₂ = to , is-eq _ from to-from from-to


text:
------------------------------------------------------------------------
-- Heterogeneous equality
------------------------------------------------------------------------

module Relation.Binary.HeterogeneousEquality where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)
open import Data.Function
open import Data.Product

------------------------------------------------------------------------
-- Heterogeneous equality

infix 4 _≅_ _≇_ _≅₁_ _≇₁_

data _≅_ {a : Set} (x : a) : {b : Set} → b → Set where
  refl : x ≅ x

data _≅₁_ {a : Set₁} (x : a) : {b : Set₁} → b → Set where
  refl : x ≅₁ x

-- Nonequality.

_≇_ : {a : Set} → a → {b : Set} → b → Set
x ≇ y = ¬ x ≅ y

_≇₁_ : {a : Set₁} → a → {b : Set₁} → b → Set
x ≇₁ y = ¬ x ≅₁ y

------------------------------------------------------------------------
-- Conversion

≡-to-≅ : ∀ {a} {x y : a} → x ≡ y → x ≅ y
≡-to-≅ refl = refl

≅-to-≡ : ∀ {a} {x y : a} → x ≅ y → x ≡ y
≅-to-≡ refl = refl

------------------------------------------------------------------------
-- Some properties

reflexive : ∀ {a} → _⇒_ {a} _≡_ (λ x y → x ≅ y)
reflexive refl = refl

sym : ∀ {a b} {x : a} {y : b} → x ≅ y → y ≅ x
sym refl = refl

trans : ∀ {a b c} {x : a} {y : b} {z : c} → x ≅ y → y ≅ z → x ≅ z
trans refl refl = refl

subst : ∀ {a} → Substitutive {a} (λ x y → x ≅ y)
subst P refl p = p

subst₂ : ∀ {A B} (P : A → B → Set) →
         ∀ {x₁ x₂ y₁ y₂} → x₁ ≅ x₂ → y₁ ≅ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

subst₁ : ∀ {a} (P : a → Set₁) → ∀ {x y} → x ≅ y → P x → P y
subst₁ P refl p = p

subst-removable : ∀ {a} (P : a → Set) {x y} (eq : x ≅ y) z →
                  subst P eq z ≅ z
subst-removable P refl z = refl

≡-subst-removable : ∀ {a} (P : a → Set) {x y} (eq : x ≡ y) z →
                    PropEq.subst P eq z ≅ z
≡-subst-removable P refl z = refl

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

cong₂ : ∀ {A : Set} {B : A → Set} {C : ∀ x → B x → Set} {x y u v}
        (f : (x : A) (y : B x) → C x y) → x ≅ y → u ≅ v → f x u ≅ f y v
cong₂ f refl refl = refl

resp₂ : ∀ {a} (∼ : Rel a) → ∼ Respects₂ (λ x y → x ≅ y)
resp₂ _∼_ = subst⟶resp₂ _∼_ subst

isEquivalence : ∀ {a} → IsEquivalence {a} (λ x y → x ≅ y)
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : Set → Setoid
setoid a = record
  { carrier       = a
  ; _≈_           = λ x y → x ≅ y
  ; isEquivalence = isEquivalence
  }

decSetoid : ∀ {a} → Decidable (λ x y → _≅_ {a} x y) → DecSetoid
decSetoid dec = record
  { _≈_              = λ x y → x ≅ y
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} → IsPreorder {a} (λ x y → x ≅ y) (λ x y → x ≅ y)
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  ; ∼-resp-≈      = resp₂ (λ x y → x ≅ y)
  }

isPreorder-≡ : ∀ {a} → IsPreorder {a} _≡_ (λ x y → x ≅ y)
isPreorder-≡ = record
  { isEquivalence = PropEq.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans
  ; ∼-resp-≈      = PropEq.resp₂ (λ x y → x ≅ y)
  }

preorder : Set → Preorder
preorder a = record
  { carrier    = a
  ; _≈_        = _≡_
  ; _∼_        = λ x y → x ≅ y
  ; isPreorder = isPreorder-≡
  }

------------------------------------------------------------------------
-- The inspect idiom

-- See Relation.Binary.PropositionalEquality.Inspect.

data Inspect {a : Set} (x : a) : Set where
  _with-≅_ : (y : a) (eq : y ≅ x) → Inspect x

inspect : ∀ {a} (x : a) → Inspect x
inspect x = x with-≅ refl

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

module ≅-Reasoning where

  -- The code in Relation.Binary.EqReasoning cannot handle
  -- heterogeneous equalities, hence the code duplication here.

  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≅⟨_⟩_ _≡⟨_⟩_
  infix  1 begin_

  data _IsRelatedTo_ {A} (x : A) {B} (y : B) : Set where
    relTo : (x≅y : x ≅ y) → x IsRelatedTo y

  begin_ : ∀ {A} {x : A} {B} {y : B} → x IsRelatedTo y → x ≅ y
  begin relTo x≅y = x≅y

  _≅⟨_⟩_ : ∀ {A} (x : A) {B} {y : B} {C} {z : C} →
           x ≅ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)

  _≡⟨_⟩_ : ∀ {A} (x : A) {y} {C} {z : C} →
           x ≡ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≡⟨ x≡y ⟩ relTo y≅z = relTo (trans (reflexive x≡y) y≅z)

  _∎ : ∀ {A} (x : A) → x IsRelatedTo x
  _∎ _ = relTo refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --type-in-type #-}  -- yes, there will be some cheating in this lecture

module Lec3 where

open import Lec1Done
open import Lec2Done

postulate
  extensionality : {S : Set}{T : S -> Set}
                   {f g : (x : S) -> T x} ->
                   ((x : S) -> f x == g x) ->
                   f == g

record Category : Set where
  field

    -- two types of thing
    Obj  : Set                  -- "objects"
    _~>_ : Obj -> Obj -> Set    -- "arrows" or "morphisms"
                                -- or "homomorphisms"

    -- two operations
    id~>        : {T : Obj} ->      T ~> T
    _>~>_       : {R S T : Obj} ->  R ~> S  ->  S ~> T  ->  R ~> T

    -- three laws
    law-id~>>~> : {S T : Obj}     (f : S ~> T) ->
                    (id~> >~> f) == f
    law->~>id~> : {S T : Obj}     (f : S ~> T) ->
                    (f >~> id~>) == f
    law->~>>~>  : {Q R S T : Obj} (f : Q ~> R)(g : R ~> S)(h : S ~> T) ->
                    ((f >~> g) >~> h) == (f >~> (g >~> h))

-- Sets and functions are the classic example of a category.
{-(-}
SET : Category
SET = record
        { Obj = Set
        ; _~>_ = \ S T -> S -> T
        ; id~> = id
        ; _>~>_ = _>>_
        ; law-id~>>~> = \ f -> refl f
        ; law->~>id~> = \ f -> refl f
        ; law->~>>~> = \ f g h -> refl (\ x -> h (g (f x)))
        }
{-)-}

unique->= : (m n : Nat)(p q : m >= n) -> p == q
unique->= m zero p q = refl <>
unique->= zero (suc n) () ()
unique->= (suc m) (suc n) p q = unique->= m n p q

-- A PREORDER is a category where there is at most one arrow between
-- any two objects. (So arrows are unique.)
{-(-}
NAT->= : Category
NAT->= = record
           { Obj = Nat
           ; _~>_ = _>=_
           ; id~> = \ {n} -> refl->= n
           ; _>~>_ = \ {m}{n}{p} m>=n n>=p -> trans->= m n p m>=n n>=p
           ; law-id~>>~> = \ {S} {T} f -> unique->= S T (trans->= S S T (refl->= S) f) f
           ; law->~>id~> = \ {S} {T} f -> unique->= S T (trans->= S T T f (refl->= T)) f
           ; law->~>>~> = \ {Q} {R} {S} {T} f g h ->
                              unique->= Q T _ _ {-(trans->= Q S T (trans->= Q R S f g) h)
                              (trans->= Q R T f (trans->= R S T g h)) -}
           } where
{-)-}

-- A MONOID is a category with Obj = One.
-- The values in the monoid are the *arrows*.
{-(-}
ONE-Nat : Category
ONE-Nat = record
            { Obj = One
            ; _~>_ = \ _ _ -> Nat
            ; id~> = zero
            ; _>~>_ = _+N_
            ; law-id~>>~> = zero-+N
            ; law->~>id~> = +N-zero
            ; law->~>>~> = assocLR-+N
            }
{-)-}

{-(-}
eqUnique : {X : Set}{x y : X}{p q : x == y} -> p == q
eqUnique {p = refl x} {q = refl .x} = refl (refl x)

-- A DISCRETE category is one where the only arrows are the identities.
DISCRETE : (X : Set) -> Category
DISCRETE X = record
               { Obj = X
               ; _~>_ = _==_
               ; id~> = \ {x} -> refl x
               ; _>~>_ = \ { (refl x) (refl .x) -> refl x }
               ; law-id~>>~> = \ {S} {T} f ->
                                   eqUnique
               ; law->~>id~> = \ {S} {T} f ->
                                   eqUnique
               ; law->~>>~> = \ {Q} {R} {S} {T} f g h -> eqUnique
               }
{-)-}

module FUNCTOR where
  open Category

  record _=>_ (C D : Category) : Set where  -- "Functor from C to D"
    field
      -- two actions
      F-Obj : Obj C -> Obj D
      F-map : {S T : Obj C} -> _~>_ C S T -> _~>_ D (F-Obj S) (F-Obj T)

      -- two laws
      F-map-id~> : {T : Obj C} -> F-map (id~> C {T}) == id~> D {F-Obj T}
      F-map->~>  : {R S T : Obj C}(f : _~>_ C R S)(g : _~>_ C S T) ->
                     F-map (_>~>_ C f g) == _>~>_ D (F-map f) (F-map g)

open FUNCTOR

module FOO (C : Category) where
  open Category C
  X : Set
  X = Obj

postulate vmap : {n : Nat}{S T : Set} → (S → T) → Vec S n → Vec T n

{-+}
VEC : Nat -> SET => SET
VEC n = record { F-Obj = \ X -> Vec X n
               ; F-map = vmap
               ; F-map-id~> = extensionality {!!}
               ; F-map->~> = {!!}
               }
{+-}

{-(-}
VTAKE : Set -> NAT->= => SET
VTAKE X = record { F-Obj = Vec X
                 ; F-map = \ {m}{n} m>=n xs -> vTake m n m>=n xs
                 ; F-map-id~> = \ {n} -> extensionality (vTakeIdFact n)
                 ; F-map->~> = \ {m}{n}{p} m>=n n>=p ->
                     extensionality (vTakeCpFact m n p m>=n n>=p)
                 }
{-)-}

{-(-}
ADD : Nat -> NAT->= => NAT->=
ADD d = record { F-Obj = (d +N_) -- \ x -> d +N x
               ; F-map = \ {m}{n} -> help d m n
               ; F-map-id~> = \ {T} ->
                                  unique->= (d +N T) (d +N T) (help d T T (refl->= T))
                                  (refl->= (d +N T))
               ; F-map->~> = \ {R} {S} {T} f g ->
                                 unique->= (d +N R) (d +N T) (help d R T (trans->= R S T f g))
                                 (trans->= (d +N R) (d +N S) (d +N T) (help d R S f) (help d S T g))
               } where
               help : forall d m n -> m >= n -> (d +N m) >= (d +N n)
               help zero m n m>=n = m>=n
               help (suc d) m n m>=n =  help d m n m>=n
{-)-}

{-(-}
CATEGORY : Category
CATEGORY = record
             { Obj = Category
             ; _~>_ = _=>_
             ; id~> = record
               { F-Obj = id
               ; F-map = id
               ; F-map-id~> = {!!}
               ; F-map->~> = {!!}
               }
             ; _>~>_ = \ F G -> record
               { F-Obj = F-Obj F >> F-Obj G
               ; F-map = F-map F >> F-map G
               ; F-map-id~> = {!!}
               ; F-map->~> = {!!}
               }
             ; law-id~>>~> = {!!}
             ; law->~>id~> = {!!}
             ; law->~>>~> = {!!}
             } where open _=>_
{-)-}

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

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

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


text:
{-

Based on Nicolai Kraus' blog post:
  The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible
  https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-ℕ-‖ℕ‖-is-nearly-invertible/

Defines [recover], which definitionally satisfies `recover ∣ x ∣ ≡ x` ([recover∣∣]) for homogeneous types

Also see the follow-up post by Jason Gross:
  Composition is not what you think it is! Why “nearly invertible” isn’t.
  https://homotopytypetheory.org/2014/02/24/composition-is-not-what-you-think-it-is-why-nearly-invertible-isnt/

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

module Cubical.HITs.PropositionalTruncation.MagicTrick where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous

open import Cubical.HITs.PropositionalTruncation.Base
open import Cubical.HITs.PropositionalTruncation.Properties

module Recover {ℓ} (A∙ : Pointed ℓ) (h : isHomogeneous A∙) where
  private
    A = typ A∙
    a = pt A∙

  toEquivPtd : ∥ A ∥ → Σ[ B∙ ∈ Pointed ℓ ] (A , a) ≡ B∙
  toEquivPtd = recPropTrunc (isContr→isProp (_ , λ p → contrSingl (snd p)))
                            (λ x → (A , x) , h x)
  private
    B∙ : ∥ A ∥ → Pointed ℓ
    B∙ tx = fst (toEquivPtd tx)

  -- the key observation is that B∙ ∣ x ∣ is definitionally equal to (A , x)
  private
    obvs : ∀ x → B∙ ∣ x ∣ ≡ (A , x)
    obvs x = refl -- try it: `C-c C-n B∙ ∣ x ∣` gives `(A , x)`

  -- thus any truncated element (of a homogeneous type) can be recovered by agda's normalizer!

  recover : ∀ (tx : ∥ A ∥) → typ (B∙ tx)
  recover tx = pt (B∙ tx)

  recover∣∣ : ∀ (x : A) → recover ∣ x ∣ ≡ x
  recover∣∣ x = refl -- try it: `C-c C-n recover ∣ x ∣` gives `x`

  private
    -- notice that the following typechecks because typ (B∙ ∣ x ∣) is definitionally equal to to A, but
    --  `recover : ∥ A ∥ → A` does not because typ (B∙ tx) is not definitionally equal to A (though it is
    --  judegmentally equal to A by cong typ (snd (toEquivPtd tx)) : A ≡ typ (B∙ tx))
    obvs2 : A → A
    obvs2 = recover ∘ ∣_∣

    -- one might wonder if (cong recover (squash ∣ x ∣ ∣ y ∣)) therefore has type x ≡ y, but thankfully
    --  typ (B∙ (squash ∣ x ∣ ∣ y ∣ i)) is *not* A (it's a messy hcomp involving h x and h y)
    recover-squash : ∀ x y → -- x ≡ y -- this raises an error
                             PathP (λ i → typ (B∙ (squash ∣ x ∣ ∣ y ∣ i))) x y
    recover-squash x y = cong recover (squash ∣ x ∣ ∣ y ∣)

-- Demo, adapted from:
-- https://bitbucket.org/nicolaikraus/agda/src/e30d70c72c6af8e62b72eefabcc57623dd921f04/trunc-inverse.lagda

private
  open import Cubical.Data.Nat
  open Recover (ℕ , zero) (isHomogeneousDiscrete discreteℕ)

  -- only `∣hidden∣` is exported, `hidden` is no longer in scope
  module _ where
    private
      hidden : ℕ
      hidden = 17

    ∣hidden∣ : ∥ ℕ ∥
    ∣hidden∣ = ∣ hidden ∣

  -- we can still recover the value, even though agda can no longer see `hidden`!
  test : recover ∣hidden∣ ≡ 17
  test = refl -- try it: `C-c C-n recover ∣hidden∣` gives `17`
              --         `C-c C-n hidden` gives an error

  -- Finally, note that the definition of recover is independent of the proof that A is homogeneous. Thus we
  --  still can definitionally recover information hidden by ∣_∣ as long as we permit holes. Try replacing
  --  `isHomogeneousDiscrete discreteℕ` above with a hole (`?`) and notice that everything still works

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


text:
open import Oscar.Prelude

module Oscar.Data.List where

open import Agda.Builtin.List public
  using ()
  renaming ([] to ∅)
  renaming (_∷_ to _,_)
⟨_⟩¶ = Agda.Builtin.List.List

List⟨_⟩ = ⟨_⟩¶


text:
module Oscar.Class.IsSemigroupoid where

open import Oscar.Class.Associativity
open import Oscar.Class.Equivalence
open import Oscar.Class.Extensionality₂
open import Oscar.Function
open import Oscar.Level
open import Oscar.Relation

record Semigroup
  {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
    (_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n)
  {ℓ}
    (_≋_ : ∀ {m n} → m ► n → m ► n → Set ℓ)
  : Set (𝔞 ⊔ 𝔰 ⊔ ℓ) where
  field
    ⦃ ′equivalence ⦄ : ∀ {m n} → Equivalence (_≋_ {m} {n})
    ⦃ ′associativity ⦄ : Associativity _◅_ _≋_
    ⦃ ′extensionality₂ ⦄ : ∀ {l m n} →
      Extensionality₂
        (_≋_ {m} {n})
        (_≋_ {l})
        (λ ⋆ → _≋_ ⋆)
        (λ ⋆ → _◅_ ⋆)
        (λ ⋆ → _◅_ ⋆)

open Semigroup ⦃ … ⦄ public hiding (′equivalence; ′associativity)

-- instance

--   Semigroup⋆ : ∀
--     {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
--       {_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n}
--     {ℓ}
--       {_≋_ : ∀ {m n} → m ► n → m ► n → Set ℓ}
--     ⦃ _ : ∀ {m n} → Equivalence (_≋_ {m} {n}) ⦄
--     ⦃ _ : Associativity _◅_ _≋_ ⦄
--     → Semigroup _◅_ _≋_
--   Semigroup.′equivalence Semigroup⋆ = it
--   Semigroup.′associativity Semigroup⋆ = it

-- -- -- record Semigroup
-- -- --   {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- --     (_◅_ : ∀ {m n} → m ► n → ∀ {l} → l ► m → l ► n)
-- -- --   {𝔱} {▸ : 𝔄 → Set 𝔱}
-- -- --     (_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n)
-- -- --   {ℓ}
-- -- --     (_≋_ : ∀ {n} → ▸ n → ▸ n → Set ℓ)
-- -- --   : Set (𝔞 ⊔ 𝔰 ⊔ 𝔱 ⊔ ℓ) where
-- -- --   field
-- -- --     ⦃ ′equivalence ⦄ : ∀ {n} → Equivalence (_≋_ {n})
-- -- --     ⦃ ′associativity ⦄ : Associativity _◅_ _◃_ _≋_

-- -- -- open Semigroup ⦃ … ⦄ public hiding (′equivalence; ′associativity)

-- -- -- instance
-- -- --   Semigroup⋆ : ∀
-- -- --     {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- --       {_◅_ : ∀ {m n} → m ► n → ∀ {l} → l ► m → l ► n}
-- -- --     {𝔱} {▸ : 𝔄 → Set 𝔱}
-- -- --       {_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n}
-- -- --     {ℓ}
-- -- --       {_≋_ : ∀ {n} → ▸ n → ▸ n → Set ℓ}
-- -- --     ⦃ _ : ∀ {n} → Equivalence (_≋_ {n}) ⦄
-- -- --     ⦃ _ : Associativity _◅_ _◃_ _≋_ ⦄
-- -- --     → Semigroup _◅_ _◃_ _≋_
-- -- --   Semigroup.′equivalence Semigroup⋆ = it
-- -- --   Semigroup.′associativity Semigroup⋆ = it


text:
import cedille-options

module communication-util (options : cedille-options.options) where

open import general-util
open import toplevel-state options {IO}

logRopeh : filepath → rope → IO ⊤
logRopeh logFilePath r with cedille-options.options.generate-logs options
...| ff = return triv
...| tt = getCurrentTime >>= λ time →
          withFile logFilePath AppendMode λ hdl →
            hPutRope hdl ([[ "([" ^ utcToString time ^ "] " ]] ⊹⊹ r ⊹⊹ [[ ")\n" ]])
logRope : toplevel-state → rope → IO ⊤
logRope s = logRopeh (toplevel-state.logFilePath s)

logMsg : toplevel-state → (message : string) → IO ⊤
logMsg s msg = logRope s [[ msg ]]

logMsg' : filepath → (message : string) → IO ⊤
logMsg' logFilePath msg = logRopeh logFilePath [[ msg ]]

sendProgressUpdate : string → IO ⊤
sendProgressUpdate msg = putStr "progress: " >> putStr msg >> putStr "\n"

progressUpdate : (filename : string) → {-(do-check : 𝔹) → -} IO ⊤
progressUpdate filename {-do-check-} =
  if cedille-options.options.show-progress-updates options then
    sendProgressUpdate ((if {-do-check-} tt then "Checking " else "Skipping ") ^ filename)
  else
    return triv

max_stars_repo_name: mudathirmahgoub/cedille

max_issues_repo_name: mudathirmahgoub/cedille

max_forks_repo_name: mudathirmahgoub/cedille


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of Delay
------------------------------------------------------------------------

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

module Codata.Delay.Categorical where

open import Codata.Delay
open import Function
open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Data.These using (leftMost)

functor : ∀ {i ℓ} → RawFunctor {ℓ} (λ A → Delay A i)
functor = record { _<$>_ = λ f → map f }

module Sequential where

  applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i)
  applicative = record
    { pure = now
    ; _⊛_  = λ df da → bind df (λ f → map f da)
    }

  applicativeZero : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i)
  applicativeZero = record
    { applicative = applicative
    ; ∅           = never
    }

  monad : ∀ {i ℓ} → RawMonad {ℓ} (λ A → Delay A i)
  monad = record
    { return = now
    ; _>>=_  = bind
    }

  monadZero : ∀ {i ℓ} → RawMonadZero {ℓ} (λ A → Delay A i)
  monadZero = record
    { monad           = monad
    ; applicativeZero = applicativeZero
    }

module Zippy where

  applicative : ∀ {i ℓ} → RawApplicative {ℓ} (λ A → Delay A i)
  applicative = record
    { pure = now
    ; _⊛_  = zipWith id
    }

  applicativeZero : ∀ {i ℓ} → RawApplicativeZero {ℓ} (λ A → Delay A i)
  applicativeZero = record
    { applicative = applicative
    ; ∅           = never
    }

  alternative : ∀ {i ℓ} → RawAlternative {ℓ} (λ A → Delay A i)
  alternative = record
    { applicativeZero = applicativeZero
    ; _∣_             = alignWith leftMost
    }


text:
open import Data.Product using ( _×_ ; _,_ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import FRP.LTL.RSet.Core using ( RSet )
open import FRP.LTL.Time.Bound using
  ( Time∞ ; fin ; _≼_ ; _≺_ ; ≼-refl ; _≼-trans_ ; _≼-asym_ ; _≼-total_ ; _≺-transˡ_
  ; ≺-impl-≼ ; ≡-impl-≼ ; ≡-impl-≽ ; ≺-impl-⋡ ; src )
open import FRP.LTL.Time.Interval using
  ( Interval ; [_⟩ ; _⊑_ ; _~_ ; _,_ ; lb ; ub ; lb≼ ; ≺ub ; Int ; _⌢_∵_
  ; ⊑-impl-≼ ; ⊑-impl-≽ ; lb≺ub ; ⊑-refl ; _⊑-trans_ ; ⌢-inj₁ ; ⌢-inj₂ ; sing )
open import FRP.LTL.Util using ( ≡-relevant ; ⊥-elim )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Unary using ( _∈_ )

module FRP.LTL.ISet.Core where

infixr 4 _,_

-- Monotone interval types

-- An MSet is a pair (A , split , subsum) where
-- A : Interval → Set
-- if σ : A [ s≼t≼u ⟩ then (split s≼t t≼u σ) : (A [ s≼t ⟩ × A [ t≼u ⟩)
-- if i ⊑ j and σ : A j then subsum i⊑j σ : A i

-- Note that subsum and split are interderivable, but
-- we provide both for efficiency.

-- In previous versions of MSet, we also included comp (an inverse of split)
-- and id (a unit for comp) but &&& and loop have been rewritten to avoid needing comp.

data MSet : Set₁ where
  _,_ : (A : Interval → Set) →
    ((∀ i j i~j → A (i ⌢ j ∵ i~j) → (A i × A j)) × (∀ i j → (i ⊑ j) → A j → A i)) →
    MSet

-- The underlying "unboxed" elements of an MSet

U⟦_⟧ : MSet → Interval → Set
U⟦ A , _ ⟧ = A

-- A "boxed" element of an MSet. This is used rather than the unboxed
-- representation because it's invertable, and so plays much better
-- with the type inference algorithm.

data B⟦_⟧ (A : MSet) (i : Interval) : Set where
  [_] : U⟦ A ⟧ i → B⟦ A ⟧ i

unbox : ∀ {A i} → B⟦ A ⟧ i → U⟦ A ⟧ i
unbox [ a ] = a

splitB⟦_⟧ : ∀ A i j i~j → B⟦ A ⟧ (i ⌢ j ∵ i~j) → (B⟦ A ⟧ i × B⟦ A ⟧ j)
splitB⟦ A , split , subsum ⟧ i j i~j [ σ ] with split i j i~j σ
... | (σ₁ , σ₂) = ([ σ₁ ] , [ σ₂ ])

subsumB⟦_⟧ : ∀ A i j → (i ⊑ j) → B⟦ A ⟧ j → B⟦ A ⟧ i
subsumB⟦ A , split , subsum ⟧ i j i⊑j [ σ ] = [ subsum i j i⊑j σ ]

-- Interval types

data ISet : Set₁ where
  [_] : MSet → ISet
  _⇛_ : MSet → ISet → ISet

-- Non-monotone semantics of ISets

I⟦_⟧ : ISet → Interval → Set
I⟦ [ A ] ⟧ i = B⟦ A ⟧ i
I⟦ A ⇛ B ⟧ i = B⟦ A ⟧ i → I⟦ B ⟧ i

-- Monotone semantics of ISets

M⟦_⟧ : ISet → Interval → Set
M⟦ [ A ] ⟧ i = B⟦ A ⟧ i
M⟦ A ⇛ B ⟧ i = ∀ j → (j ⊑ i) → I⟦ A ⇛ B ⟧ j

-- User-level semantics

⟦_⟧ : ISet → Set
⟦ A ⟧ = ∀ {i} → I⟦ A ⟧ i

-- Translation of ISet into MSet

splitM⟦_⟧ : ∀ A i j i~j → M⟦ A ⟧ (i ⌢ j ∵ i~j) → (M⟦ A ⟧ i × M⟦ A ⟧ j)
splitM⟦ [ A ] ⟧ i j i~j σ = splitB⟦ A ⟧ i j i~j σ
splitM⟦ A ⇛ B ⟧ i j i~j f = (f₁ , f₂) where

  f₁ : ∀ k → (k ⊑ i) → B⟦ A ⟧ k → I⟦ B ⟧ k
  f₁ k k⊑i = f k (⊑-impl-≽ k⊑i , ⊑-impl-≼ k⊑i ≼-trans ≡-impl-≼ i~j ≼-trans ≺-impl-≼ (lb≺ub j))

  f₂ : ∀ k → (k ⊑ j) → B⟦ A ⟧ k → I⟦ B ⟧ k
  f₂ k k⊑j = f k (≺-impl-≼ (lb≺ub i) ≼-trans ≡-impl-≼ i~j ≼-trans ⊑-impl-≽ k⊑j , ⊑-impl-≼ k⊑j)

subsumM⟦_⟧ : ∀ A i j → (i ⊑ j) → M⟦ A ⟧ j → M⟦ A ⟧ i
subsumM⟦ [ A ] ⟧ i j i⊑j σ = subsumB⟦ A ⟧ i j i⊑j σ
subsumM⟦ A ⇛ B ⟧ i j i⊑j f = λ h h⊑i → f h (h⊑i ⊑-trans i⊑j)

mset : ISet → MSet
mset A =  ( M⟦ A ⟧ , splitM⟦ A ⟧ , subsumM⟦ A ⟧ )

-- Translations back and forth between M⟦ A ⟧ and I⟦ A ⟧

m→i : ∀ {A i} → M⟦ A ⟧ i → I⟦ A ⟧ i
m→i {[ A ]} {i} σ = σ
m→i {A ⇛ B} {i} f = f i ⊑-refl

i→m : ∀ {A i} → (∀ j → (j ⊑ i) → I⟦ A ⟧ j) → M⟦ A ⟧ i
i→m {[ A ]} {i} σ = σ i ⊑-refl
i→m {A ⇛ B} {i} f = f

-- Embedding of RSet into ISet

⌈_⌉ : RSet → ISet
⌈ A ⌉ = [ (λ i → ∀ t → .(t ∈ Int i) → A t) , split , subsum ] where

  split : ∀ i j i~j → (∀ t → .(t ∈ Int (i ⌢ j ∵ i~j)) → A t) →
    ((∀ t → .(t ∈ Int i) → A t) × (∀ t → .(t ∈ Int j) → A t))
  split i j i~j σ =
    ( (λ t t∈i → σ t (lb≼ t∈i , ≺ub t∈i ≺-transˡ ≡-impl-≼ i~j ≼-trans ≺-impl-≼ (lb≺ub j)))
    , (λ t t∈j → σ t (≺-impl-≼ (lb≺ub i) ≼-trans ≡-impl-≼ i~j ≼-trans lb≼ t∈j , ≺ub t∈j)) )

  subsum : ∀ i j → (i ⊑ j) → (∀ t → .(t ∈ Int j) → A t) → (∀ t → .(t ∈ Int i) → A t)
  subsum i j i⊑j σ t t∈i = σ t (⊑-impl-≽ i⊑j ≼-trans lb≼ t∈i , ≺ub t∈i ≺-transˡ ⊑-impl-≼ i⊑j)

-- Embedding of ISet into RSet

⌊_⌋ : ISet → RSet
⌊ A ⌋ t = M⟦ A ⟧ (sing t)

-- Embedding of Set into ISet

data Always (A : Set) (i : Interval) : Set where
  const : A → Always A i
  var : ∀ j → .(i ⊑ j) → (∀ t → .(t ∈ Int j) → A) → Always A i

⟨_⟩ : Set → ISet
⟨ A ⟩ =  [ Always A , split , subsum ] where

  split : ∀ i j i~j → Always A (i ⌢ j ∵ i~j) → (Always A i × Always A j)
  split i j i~j (const a) = (const a , const a)
  split i j i~j (var k i⌢j⊑k f) =
    ( var k (⌢-inj₁ i j i~j ⊑-trans i⌢j⊑k) f
    , var k (⌢-inj₂ i j i~j ⊑-trans i⌢j⊑k) f )

  subsum : ∀ i j → (i ⊑ j) → Always A j → Always A i
  subsum i j i⊑j (const a)     = const a
  subsum i j i⊑j (var k j⊑k f) = var k (i⊑j ⊑-trans j⊑k) f

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


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

   Copyright (c) 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.Consensus.Types
open import Optics.All
import      Util.KVMap                          as Map
open import Util.Prelude

module LibraBFT.Impl.Consensus.TestUtils.MockSharedStorage where

new : ValidatorSet → MockSharedStorage
new = mkMockSharedStorage
  Map.empty
  Map.empty
  Map.empty
  nothing
  nothing

newObmWithLIWS : ValidatorSet → LedgerInfoWithSignatures → MockSharedStorage
newObmWithLIWS vs obmLIWS =
  new vs & mssLis ∙~ Map.singleton (obmLIWS ^∙ liwsVersion) obmLIWS


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of binary relations to sigma types
------------------------------------------------------------------------

module Relation.Binary.Sigma.Pointwise where

open import Data.Product as Prod
open import Level
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection; Injective)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; module LeftInverse;
         _LeftInverseOf_; _RightInverseOf_)
open import Function.Related as Related
  using (_∼[_]_; lam; app-←; app-↢)
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
import Relation.Binary as B
open import Relation.Binary.Indexed as I using (_at_)
import Relation.Binary.HeterogeneousEquality as H
import Relation.Binary.PropositionalEquality as P

------------------------------------------------------------------------
-- Pointwise lifting

infixr 4 _,_

data REL {a₁ a₂ b₁ b₂ ℓ₁ ℓ₂}
         {A₁ : Set a₁} (B₁ : A₁ → Set b₁)
         {A₂ : Set a₂} (B₂ : A₂ → Set b₂)
         (_R₁_ : B.REL A₁ A₂ ℓ₁) (_R₂_ : I.REL B₁ B₂ ℓ₂) :
         B.REL (Σ A₁ B₁) (Σ A₂ B₂) (a₁ ⊔ a₂ ⊔ b₁ ⊔ b₂ ⊔ ℓ₁ ⊔ ℓ₂) where
  _,_ : {x₁ : A₁} {y₁ : B₁ x₁} {x₂ : A₂} {y₂ : B₂ x₂}
        (x₁Rx₂ : x₁ R₁ x₂) (y₁Ry₂ : y₁ R₂ y₂) →
        REL B₁ B₂ _R₁_ _R₂_ (x₁ , y₁) (x₂ , y₂)

Rel : ∀ {a b ℓ₁ ℓ₂} {A : Set a} (B : A → Set b)
      (_R₁_ : B.Rel A ℓ₁) (_R₂_ : I.Rel B ℓ₂) → B.Rel (Σ A B) _
Rel B = REL B B

------------------------------------------------------------------------
-- Rel preserves many properties

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b}
         {R₁ : B.Rel A ℓ₁} {R₂ : I.Rel B ℓ₂} where

  refl : B.Reflexive R₁ → I.Reflexive B R₂ →
         B.Reflexive (Rel B R₁ R₂)
  refl refl₁ refl₂ {x = (x , y)} = (refl₁ , refl₂)

  symmetric : B.Symmetric R₁ → I.Symmetric B R₂ →
              B.Symmetric (Rel B R₁ R₂)
  symmetric sym₁ sym₂ (x₁Rx₂ , y₁Ry₂) = (sym₁ x₁Rx₂ , sym₂ y₁Ry₂)

  transitive : B.Transitive R₁ → I.Transitive B R₂ →
               B.Transitive (Rel B R₁ R₂)
  transitive trans₁ trans₂ (x₁Rx₂ , y₁Ry₂) (x₂Rx₃ , y₂Ry₃) =
    (trans₁ x₁Rx₂ x₂Rx₃ , trans₂ y₁Ry₂ y₂Ry₃)

  isEquivalence : B.IsEquivalence R₁ → I.IsEquivalence B R₂ →
                  B.IsEquivalence (Rel B R₁ R₂)
  isEquivalence eq₁ eq₂ = record
    { refl  = refl (B.IsEquivalence.refl eq₁)
                   (I.IsEquivalence.refl eq₂)
    ; sym   = symmetric (B.IsEquivalence.sym eq₁)
                        (I.IsEquivalence.sym eq₂)
    ; trans = transitive (B.IsEquivalence.trans eq₁)
                         (I.IsEquivalence.trans eq₂)
    }

setoid : ∀ {b₁ b₂ i₁ i₂} →
         (A : B.Setoid b₁ b₂) → I.Setoid (B.Setoid.Carrier A) i₁ i₂ →
         B.Setoid _ _
setoid s₁ s₂ = record
  { isEquivalence = isEquivalence (B.Setoid.isEquivalence s₁)
                                  (I.Setoid.isEquivalence s₂)
  }

------------------------------------------------------------------------
-- The propositional equality setoid over sigma types can be
-- decomposed using Rel

Rel↔≡ : ∀ {a b} {A : Set a} {B : A → Set b} →
        Inverse (setoid (P.setoid A) (H.indexedSetoid B))
                (P.setoid (Σ A B))
Rel↔≡ {a} {b} {A} {B} = record
  { to         = record { _⟨$⟩_ = id; cong = to-cong   }
  ; from       = record { _⟨$⟩_ = id; cong = from-cong }
  ; inverse-of = record
    { left-inverse-of  = uncurry (λ _ _ → (P.refl , H.refl))
    ; right-inverse-of = λ _ → P.refl
    }
  }
  where
  open I using (_=[_]⇒_)

  to-cong : Rel B P._≡_ (λ x y → H._≅_ x y) =[ id {a = a ⊔ b} ]⇒ P._≡_
  to-cong (P.refl , H.refl) = P.refl

  from-cong : P._≡_ =[ id {a = a ⊔ b} ]⇒ Rel B P._≡_ (λ x y → H._≅_ x y)
  from-cong {i = (x , y)} P.refl = (P.refl , H.refl)

------------------------------------------------------------------------
-- Some properties related to "relatedness"

⟶ : ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′)
    (f : A₁ → A₂) → (∀ {x} → (B₁ at x) ⟶ (B₂ at f x)) →
    setoid (P.setoid A₁) B₁ ⟶ setoid (P.setoid A₂) B₂
⟶ {A₁ = A₁} {A₂} {B₁} B₂ f g = record
  { _⟨$⟩_ = fg
  ; cong  = fg-cong
  }
  where
  open B.Setoid (setoid (P.setoid A₁) B₁)
    using () renaming (_≈_ to _≈₁_)
  open B.Setoid (setoid (P.setoid A₂) B₂)
    using () renaming (_≈_ to _≈₂_)
  open B using (_=[_]⇒_)

  fg = Prod.map f (_⟨$⟩_ g)

  fg-cong : _≈₁_ =[ fg ]⇒ _≈₂_
  fg-cong (P.refl , ∼) = (P.refl , F.cong g ∼)

equivalence :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : I.Setoid A₁ b₁ b₁′} {B₂ : I.Setoid A₂ b₂ b₂′}
  (A₁⇔A₂ : A₁ ⇔ A₂) →
  (∀ {x} → _⟶_ (B₁ at x) (B₂ at (Equivalence.to   A₁⇔A₂ ⟨$⟩ x))) →
  (∀ {y} → _⟶_ (B₂ at y) (B₁ at (Equivalence.from A₁⇔A₂ ⟨$⟩ y))) →
  Equivalence (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
equivalence {B₁ = B₁} {B₂} A₁⇔A₂ B-to B-from = record
  { to   = ⟶ B₂ (_⟨$⟩_ (to   A₁⇔A₂)) B-to
  ; from = ⟶ B₁ (_⟨$⟩_ (from A₁⇔A₂)) B-from
  } where open Equivalence

private

  subst-cong : ∀ {i a p} {I : Set i} {A : I → Set a}
               (P : ∀ {i} → A i → A i → Set p) {i i′} {x y : A i}
               (i≡i′ : P._≡_ i i′) →
               P x y → P (P.subst A i≡i′ x) (P.subst A i≡i′ y)
  subst-cong P P.refl p = p

equivalence-↞ :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    (B₁ : I.Setoid A₁ b₁ b₁′) {B₂ : I.Setoid A₂ b₂ b₂′}
  (A₁↞A₂ : A₁ ↞ A₂) →
  (∀ {x} → Equivalence (B₁ at (LeftInverse.from A₁↞A₂ ⟨$⟩ x))
                       (B₂ at x)) →
  Equivalence (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
equivalence-↞ B₁ {B₂} A₁↞A₂ B₁⇔B₂ =
  equivalence (LeftInverse.equivalence A₁↞A₂) B-to B-from
  where
  B-to : ∀ {x} → _⟶_ (B₁ at x) (B₂ at (LeftInverse.to A₁↞A₂ ⟨$⟩ x))
  B-to = record
    { _⟨$⟩_ = λ x → Equivalence.to B₁⇔B₂ ⟨$⟩
                      P.subst (I.Setoid.Carrier B₁)
                         (P.sym $ LeftInverse.left-inverse-of A₁↞A₂ _)
                         x
    ; cong  = F.cong (Equivalence.to B₁⇔B₂) ∘
              subst-cong (λ {x} → I.Setoid._≈_ B₁ {x} {x})
                         (P.sym (LeftInverse.left-inverse-of A₁↞A₂ _))
    }

  B-from : ∀ {y} → _⟶_ (B₂ at y) (B₁ at (LeftInverse.from A₁↞A₂ ⟨$⟩ y))
  B-from = Equivalence.from B₁⇔B₂

equivalence-↠ :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′)
  (A₁↠A₂ : A₁ ↠ A₂) →
  (∀ {x} → Equivalence (B₁ at x) (B₂ at (Surjection.to A₁↠A₂ ⟨$⟩ x))) →
  Equivalence (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
equivalence-↠ {B₁ = B₁} B₂ A₁↠A₂ B₁⇔B₂ =
  equivalence (Surjection.equivalence A₁↠A₂) B-to B-from
  where
  B-to : ∀ {x} → B₁ at x ⟶ B₂ at (Surjection.to A₁↠A₂ ⟨$⟩ x)
  B-to = Equivalence.to B₁⇔B₂

  B-from : ∀ {y} → B₂ at y ⟶ B₁ at (Surjection.from A₁↠A₂ ⟨$⟩ y)
  B-from = record
    { _⟨$⟩_ = λ x → Equivalence.from B₁⇔B₂ ⟨$⟩
                      P.subst (I.Setoid.Carrier B₂)
                         (P.sym $ Surjection.right-inverse-of A₁↠A₂ _)
                         x
    ; cong  = F.cong (Equivalence.from B₁⇔B₂) ∘
              subst-cong (λ {x} → I.Setoid._≈_ B₂ {x} {x})
                         (P.sym (Surjection.right-inverse-of A₁↠A₂ _))
    }

⇔ : ∀ {a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
    (A₁⇔A₂ : A₁ ⇔ A₂) →
    (∀ {x} → B₁ x → B₂ (Equivalence.to   A₁⇔A₂ ⟨$⟩ x)) →
    (∀ {y} → B₂ y → B₁ (Equivalence.from A₁⇔A₂ ⟨$⟩ y)) →
    Σ A₁ B₁ ⇔ Σ A₂ B₂
⇔ {B₁ = B₁} {B₂} A₁⇔A₂ B-to B-from =
  Inverse.equivalence (Rel↔≡ {B = B₂}) ⟨∘⟩
  equivalence A₁⇔A₂
    (Inverse.to (H.≡↔≅ B₂) ⊚ P.→-to-⟶ B-to ⊚ Inverse.from (H.≡↔≅ B₁))
    (Inverse.to (H.≡↔≅ B₁) ⊚ P.→-to-⟶ B-from ⊚ Inverse.from (H.≡↔≅ B₂))
    ⟨∘⟩
  Eq.sym (Inverse.equivalence (Rel↔≡ {B = B₁}))
  where
  open Eq using () renaming (_∘_ to _⟨∘⟩_)
  open F  using () renaming (_∘_ to _⊚_)

⇔-↠ : ∀ {a₁ a₂ b₁ b₂}
        {A₁ : Set a₁} {A₂ : Set a₂}
        {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
      (A₁↠A₂ : A₁ ↠ A₂) →
      (∀ {x} → _⇔_ (B₁ x) (B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x))) →
      _⇔_ (Σ A₁ B₁) (Σ A₂ B₂)
⇔-↠ {B₁ = B₁} {B₂} A₁↠A₂ B₁⇔B₂ =
  Inverse.equivalence (Rel↔≡ {B = B₂}) ⟨∘⟩
  equivalence-↠ (H.indexedSetoid B₂) A₁↠A₂
    (λ {x} → Inverse.equivalence (H.≡↔≅ B₂) ⟨∘⟩
             B₁⇔B₂ {x} ⟨∘⟩
             Inverse.equivalence (Inv.sym (H.≡↔≅ B₁))) ⟨∘⟩
  Eq.sym (Inverse.equivalence (Rel↔≡ {B = B₁}))
  where open Eq using () renaming (_∘_ to _⟨∘⟩_)

injection :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′) →
  (A₁↣A₂ : A₁ ↣ A₂) →
  (∀ {x} → Injection (B₁ at x) (B₂ at (Injection.to A₁↣A₂ ⟨$⟩ x))) →
  Injection (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
injection {B₁ = B₁} B₂ A₁↣A₂ B₁↣B₂ = record
  { to        = to
  ; injective = inj
  }
  where
  to = ⟶ B₂ (_⟨$⟩_ (Injection.to A₁↣A₂)) (Injection.to B₁↣B₂)

  inj : Injective to
  inj (x , y) =
    Injection.injective A₁↣A₂ x ,
    lemma (Injection.injective A₁↣A₂ x) y
    where
    lemma :
      ∀ {x x′}
        {y : I.Setoid.Carrier B₁ x} {y′ : I.Setoid.Carrier B₁ x′} →
      P._≡_ x x′ →
      (eq : I.Setoid._≈_ B₂ (Injection.to B₁↣B₂ ⟨$⟩ y)
                            (Injection.to B₁↣B₂ ⟨$⟩ y′)) →
      I.Setoid._≈_ B₁ y y′
    lemma P.refl = Injection.injective B₁↣B₂

↣ : ∀ {a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
    (A₁↣A₂ : A₁ ↣ A₂) →
    (∀ {x} → B₁ x ↣ B₂ (Injection.to A₁↣A₂ ⟨$⟩ x)) →
    Σ A₁ B₁ ↣ Σ A₂ B₂
↣ {B₁ = B₁} {B₂} A₁↣A₂ B₁↣B₂ =
  Inverse.injection (Rel↔≡ {B = B₂}) ⟨∘⟩
  injection (H.indexedSetoid B₂) A₁↣A₂
    (λ {x} → Inverse.injection (H.≡↔≅ B₂) ⟨∘⟩
             B₁↣B₂ {x} ⟨∘⟩
             Inverse.injection (Inv.sym (H.≡↔≅ B₁))) ⟨∘⟩
  Inverse.injection (Inv.sym (Rel↔≡ {B = B₁}))
  where open Inj using () renaming (_∘_ to _⟨∘⟩_)

left-inverse :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    (B₁ : I.Setoid A₁ b₁ b₁′) {B₂ : I.Setoid A₂ b₂ b₂′} →
  (A₁↞A₂ : A₁ ↞ A₂) →
  (∀ {x} → LeftInverse (B₁ at (LeftInverse.from A₁↞A₂ ⟨$⟩ x))
                       (B₂ at x)) →
  LeftInverse (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
left-inverse B₁ {B₂} A₁↞A₂ B₁↞B₂ = record
  { to              = Equivalence.to   eq
  ; from            = Equivalence.from eq
  ; left-inverse-of = left
  }
  where
  eq = equivalence-↞ B₁ A₁↞A₂ (LeftInverse.equivalence B₁↞B₂)

  left : Equivalence.from eq LeftInverseOf Equivalence.to eq
  left (x , y) =
    LeftInverse.left-inverse-of A₁↞A₂ x ,
    I.Setoid.trans B₁
      (LeftInverse.left-inverse-of B₁↞B₂ _)
      (lemma (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x)))
    where
    lemma :
      ∀ {x x′ y} (eq : P._≡_ x x′) →
      I.Setoid._≈_ B₁ (P.subst (I.Setoid.Carrier B₁) eq y) y
    lemma P.refl = I.Setoid.refl B₁

↞ : ∀ {a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
    (A₁↞A₂ : A₁ ↞ A₂) →
    (∀ {x} → B₁ (LeftInverse.from A₁↞A₂ ⟨$⟩ x) ↞ B₂ x) →
    Σ A₁ B₁ ↞ Σ A₂ B₂
↞ {B₁ = B₁} {B₂} A₁↞A₂ B₁↞B₂ =
  Inverse.left-inverse (Rel↔≡ {B = B₂}) ⟨∘⟩
  left-inverse (H.indexedSetoid B₁) A₁↞A₂
    (λ {x} → Inverse.left-inverse (H.≡↔≅ B₂) ⟨∘⟩
             B₁↞B₂ {x} ⟨∘⟩
             Inverse.left-inverse (Inv.sym (H.≡↔≅ B₁))) ⟨∘⟩
  Inverse.left-inverse (Inv.sym (Rel↔≡ {B = B₁}))
  where open LeftInv using () renaming (_∘_ to _⟨∘⟩_)

surjection :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′) →
  (A₁↠A₂ : A₁ ↠ A₂) →
  (∀ {x} → Surjection (B₁ at x) (B₂ at (Surjection.to A₁↠A₂ ⟨$⟩ x))) →
  Surjection (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
surjection {B₁} B₂ A₁↠A₂ B₁↠B₂ = record
  { to         = Equivalence.to eq
  ; surjective = record
    { from             = Equivalence.from eq
    ; right-inverse-of = right
    }
  }
  where
  eq = equivalence-↠ B₂ A₁↠A₂ (Surjection.equivalence B₁↠B₂)

  right : Equivalence.from eq RightInverseOf Equivalence.to eq
  right (x , y) =
    Surjection.right-inverse-of A₁↠A₂ x ,
    I.Setoid.trans B₂
      (Surjection.right-inverse-of B₁↠B₂ _)
      (lemma (P.sym $ Surjection.right-inverse-of A₁↠A₂ x))
    where
    lemma : ∀ {x x′ y} (eq : P._≡_ x x′) →
            I.Setoid._≈_ B₂ (P.subst (I.Setoid.Carrier B₂) eq y) y
    lemma P.refl = I.Setoid.refl B₂

↠ : ∀ {a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
    (A₁↠A₂ : A₁ ↠ A₂) →
    (∀ {x} → B₁ x ↠ B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x)) →
    Σ A₁ B₁ ↠ Σ A₂ B₂
↠ {B₁ = B₁} {B₂} A₁↠A₂ B₁↠B₂ =
  Inverse.surjection (Rel↔≡ {B = B₂}) ⟨∘⟩
  surjection (H.indexedSetoid B₂) A₁↠A₂
    (λ {x} → Inverse.surjection (H.≡↔≅ B₂) ⟨∘⟩
             B₁↠B₂ {x} ⟨∘⟩
             Inverse.surjection (Inv.sym (H.≡↔≅ B₁))) ⟨∘⟩
  Inverse.surjection (Inv.sym (Rel↔≡ {B = B₁}))
  where open Surj using () renaming (_∘_ to _⟨∘⟩_)

inverse :
  ∀ {a₁ a₂ b₁ b₁′ b₂ b₂′}
    {A₁ : Set a₁} {A₂ : Set a₂}
    {B₁ : I.Setoid A₁ b₁ b₁′} (B₂ : I.Setoid A₂ b₂ b₂′) →
  (A₁↔A₂ : A₁ ↔ A₂) →
  (∀ {x} → Inverse (B₁ at x) (B₂ at (Inverse.to A₁↔A₂ ⟨$⟩ x))) →
  Inverse (setoid (P.setoid A₁) B₁) (setoid (P.setoid A₂) B₂)
inverse {B₁ = B₁} B₂ A₁↔A₂ B₁↔B₂ = record
  { to         = Surjection.to   surj
  ; from       = Surjection.from surj
  ; inverse-of = record
    { left-inverse-of  = left
    ; right-inverse-of = Surjection.right-inverse-of surj
    }
  }
  where
  surj = surjection B₂ (Inverse.surjection A₁↔A₂)
                       (Inverse.surjection B₁↔B₂)

  left : Surjection.from surj LeftInverseOf Surjection.to surj
  left (x , y) =
    Inverse.left-inverse-of A₁↔A₂ x ,
    I.Setoid.trans B₁
      (lemma (P.sym (Inverse.left-inverse-of A₁↔A₂ x))
             (P.sym (Inverse.right-inverse-of A₁↔A₂
                       (Inverse.to A₁↔A₂ ⟨$⟩ x))))
      (Inverse.left-inverse-of B₁↔B₂ y)
    where
    lemma :
      ∀ {x x′ y} → P._≡_ x x′ →
      (eq : P._≡_ (Inverse.to A₁↔A₂ ⟨$⟩ x) (Inverse.to A₁↔A₂ ⟨$⟩ x′)) →
      I.Setoid._≈_ B₁
        (Inverse.from B₁↔B₂ ⟨$⟩ P.subst (I.Setoid.Carrier B₂) eq y)
        (Inverse.from B₁↔B₂ ⟨$⟩ y)
    lemma P.refl P.refl = I.Setoid.refl B₁

↔ : ∀ {a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂}
      {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
    (A₁↔A₂ : A₁ ↔ A₂) →
    (∀ {x} → B₁ x ↔ B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
    Σ A₁ B₁ ↔ Σ A₂ B₂
↔ {B₁ = B₁} {B₂} A₁↔A₂ B₁↔B₂ =
  Rel↔≡ {B = B₂} ⟨∘⟩
  inverse (H.indexedSetoid B₂) A₁↔A₂
    (λ {x} → H.≡↔≅ B₂ ⟨∘⟩ B₁↔B₂ {x} ⟨∘⟩ Inv.sym (H.≡↔≅ B₁)) ⟨∘⟩
  Inv.sym (Rel↔≡ {B = B₁})
  where open Inv using () renaming (_∘_ to _⟨∘⟩_)

private

  swap-coercions :
    ∀ {k a₁ a₂ b₁ b₂}
      {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : A₁ → Set b₁} (B₂ : A₂ → Set b₂)
    (A₁↔A₂ : _↔_ A₁ A₂) →
    (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
    ∀ {x} → B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x) ∼[ k ] B₂ x
  swap-coercions {k} {B₁ = B₁} B₂ A₁↔A₂ eq {x} =
    B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x)                         ∼⟨ eq ⟩
    B₂ (Inverse.to A₁↔A₂ ⟨$⟩ (Inverse.from A₁↔A₂ ⟨$⟩ x))  ↔⟨ B.Setoid.reflexive (Related.setoid Related.bijection _)
                                                               (P.cong B₂ $ Inverse.right-inverse-of A₁↔A₂ x) ⟩
    B₂ x                                                  ∎
    where open Related.EquationalReasoning

cong : ∀ {k a₁ a₂ b₁ b₂}
         {A₁ : Set a₁} {A₂ : Set a₂}
         {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
       (A₁↔A₂ : _↔_ A₁ A₂) →
       (∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
       Σ A₁ B₁ ∼[ k ] Σ A₂ B₂
cong {Related.implication}                   = λ A₁↔A₂ → Prod.map (_⟨$⟩_ (Inverse.to A₁↔A₂))
cong {Related.reverse-implication} {B₂ = B₂} = λ A₁↔A₂ B₁←B₂ → lam (Prod.map (_⟨$⟩_ (Inverse.from A₁↔A₂))
                                                                             (app-← (swap-coercions B₂ A₁↔A₂ B₁←B₂)))
cong {Related.equivalence}                   = ⇔-↠ ∘ Inverse.surjection
cong {Related.injection}                     = ↣ ∘ Inverse.injection
cong {Related.reverse-injection}   {B₂ = B₂} = λ A₁↔A₂ B₁↢B₂ → lam (↣ (Inverse.injection (Inv.sym A₁↔A₂))
                                                                      (app-↢ (swap-coercions B₂ A₁↔A₂ B₁↢B₂)))
cong {Related.left-inverse}                  = λ A₁↔A₂ → ↞ (Inverse.left-inverse A₁↔A₂) ∘ swap-coercions _ A₁↔A₂
cong {Related.surjection}                    = ↠ ∘ Inverse.surjection
cong {Related.bijection}                     = ↔


text:
open import FRP.JS.QUnit using ( TestSuites ; suite ; _,_ )

import FRP.JS.Test.Bool
import FRP.JS.Test.Nat
import FRP.JS.Test.Int
import FRP.JS.Test.Float
import FRP.JS.Test.String
import FRP.JS.Test.Maybe
import FRP.JS.Test.List
import FRP.JS.Test.Array
import FRP.JS.Test.Object
import FRP.JS.Test.JSON
import FRP.JS.Test.Behaviour
import FRP.JS.Test.DOM
import FRP.JS.Test.Compiler

module FRP.JS.Test where

tests : TestSuites
tests =
  ( suite "Bool"      FRP.JS.Test.Bool.tests
  , suite "Nat"       FRP.JS.Test.Nat.tests
  , suite "Int"       FRP.JS.Test.Int.tests
  , suite "Float"     FRP.JS.Test.Float.tests
  , suite "String"    FRP.JS.Test.String.tests
  , suite "Maybe"     FRP.JS.Test.Maybe.tests
  , suite "List"      FRP.JS.Test.List.tests
  , suite "Array"     FRP.JS.Test.Array.tests
  , suite "Object"    FRP.JS.Test.Object.tests
  , suite "JSON"      FRP.JS.Test.JSON.tests
  , suite "Behaviour" FRP.JS.Test.Behaviour.tests
  , suite "DOM"       FRP.JS.Test.DOM.tests
  , suite "Compiler"  FRP.JS.Test.Compiler.tests )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-# OPTIONS --safe #-}
module STLC.Operational.Base where

open import STLC.Syntax
open import Data.Empty using (⊥-elim)
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin; _≟_; punchOut; punchIn)
  renaming (zero to fzero; suc to fsuc)
open import Relation.Binary.PropositionalEquality using (_≢_; refl; sym)
open import Relation.Nullary using (yes; no)
open import Function.Base using (_∘_)

private
  variable
    n : ℕ
    a : Type
    fin : Fin n

-- | Increments the variables that are free relative to the inserted "pivot" variable.
lift : Term n → Fin (suc n) → Term (suc n)
lift (abs ty body) v = abs ty (lift body (fsuc v))
lift (app f x) v = app (lift f v) (lift x v)
lift (var n) v = var (punchIn v n)
lift ⋆ v = ⋆
lift (pair x y) v = pair (lift x v) (lift y v)
lift (projₗ p) v = projₗ (lift p v)
lift (projᵣ p) v = projᵣ (lift p v)

-- | Inserts a binding in the middle of the context.
liftΓ : Ctx n → Fin (suc n) → Type → Ctx (suc n)
liftΓ Γ fzero t = Γ ,- t
liftΓ (Γ ,- A) (fsuc v) t = (liftΓ Γ v t) ,- A

infix 7 _[_≔_]

_[_≔_] : Term (suc n) → Fin (suc n) → Term n → Term n
(abs ty body) [ v ≔ def ] = abs ty (body [ fsuc v ≔ lift def fzero ])
(app f x)     [ v ≔ def ] = app (f [ v ≔ def ]) (x [ v ≔ def ])
(var n)       [ v ≔ def ] with v ≟ n
... | yes refl = def
... | no neq = var (punchOut {i = v} {j = n} λ { refl → neq (sym refl)})
⋆             [ v ≔ def ] = ⋆
(pair x y)    [ v ≔ def ] = pair (x [ v ≔ def ]) (y [ v ≔ def ])
(projₗ p)     [ v ≔ def ] = projₗ (p [ v ≔ def ])
(projᵣ p)     [ v ≔ def ] = projᵣ (p [ v ≔ def ])

max_stars_repo_name: TypesLogicsCats/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


text:
{-# OPTIONS --safe --without-K #-}
module CF.Types where

open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥)
open import Data.Product
open import Data.List as L
open import Data.String
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Decidable
open import Relation.Nullary

data Ty : Set where
  void : Ty
  int  : Ty
  bool : Ty

variable
  a b c r s t   : Ty
  as bs cs      : List Ty


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

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

module _ where

variable
  ℓ ℓ′ ℓ₁ ℓ₂ : Level
  A B C : Set ℓ
  k l m n : Nat

lone ltwo lthree : Level
lone = lsuc lzero
ltwo = lsuc lone
lthree = lsuc ltwo

set0 : Set₂
set0 = Set₀

set1 : Set₂
set1 = Set₁

lift : Set ℓ → Set (ℓ ⊔ ℓ′)
lift x = x

data List (A : Set ℓ) : Set ℓ where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

List-test₁ : (A : Set) → List {lone} A
List-test₁ A = []

lower-List : ∀ ℓ′ {A : Set ℓ} → List {ℓ ⊔ ℓ′} A → List A
lower-List ℓ [] = []
lower-List ℓ (x ∷ xs) = x ∷ lower-List ℓ xs

lower-List-test₁ : {A : Set} → List {lthree} A → List {lone} A
lower-List-test₁ = lower-List lthree

map : (f : A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs

map00 : {A B : Set} (f : A → B) → List A → List B
map00 = map

map01 : {A : Set} {B : Set₁} (f : A → B) → List A → List B
map01 = map

map10 : {A : Set₁} {B : Set} (f : A → B) → List A → List B
map10 = map

map20 : {A : Set₂} {B : Set} (f : A → B) → List A → List B
map20 = map

data Vec (A : Set ℓ) : Nat → Set ℓ where
  [] : Vec A 0
  _∷_ : A → Vec A n → Vec A (suc n)

module Without-Cumulativity where

  N-ary-level : Level → Level → Nat → Level
  N-ary-level ℓ₁ ℓ₂ zero    = ℓ₂
  N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n

  N-ary : ∀ n → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
  N-ary zero    A B = B
  N-ary (suc n) A B = A → N-ary n A B

module With-Cumulativity where

  N-ary : Nat → Set ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
  N-ary zero    A B = B
  N-ary (suc n) A B = A → N-ary n A B

  curryⁿ : (Vec A n → B) → N-ary n A B
  curryⁿ {n = zero}  f = f []
  curryⁿ {n = suc n} f = λ x → curryⁿ λ xs → f (x ∷ xs)

  _$ⁿ_ : N-ary n A B → (Vec A n → B)
  f $ⁿ []       = f
  f $ⁿ (x ∷ xs) = f x $ⁿ xs

  ∀ⁿ : ∀ {A : Set ℓ} n → N-ary n A (Set ℓ′) → Set (ℓ ⊔ ℓ′)
  ∀ⁿ zero    P = P
  ∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Container Morphisms
------------------------------------------------------------------------

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

module Data.Container.Morphism where

open import Data.Container.Core
import Function as F

module _ {s p} (C : Container s p) where

  id : C ⇒ C
  id .shape    = F.id
  id .position = F.id

module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         where

  infixr 9 _∘_
  _∘_ : C₂ ⇒ C₃ → C₁ ⇒ C₂ → C₁ ⇒ C₃
  (f ∘ g) .shape    = shape    f F.∘′ shape    g
  (f ∘ g) .position = position g F.∘′ position f


text:
module AbstractInterfaceExample where

open import Function
open import Data.Bool
open import Data.String

-- * One-parameter interface for the type `a' with only one method.

record VoiceInterface (a : Set) : Set where
  constructor voice-interface
  field say-method-of : a → String

open VoiceInterface

-- * An overloaded method.

say : {a : Set} → ⦃ _ : VoiceInterface a ⦄ → a → String
say ⦃ instance ⦄ = say-method-of instance

-- * Some data types.

data Cat : Set where
  cat : Bool → Cat

crazy! = true
plain-cat = false

-- | This cat is crazy?
crazy? : Cat → Bool
crazy? (cat x) = x

-- | A 'plain' dog.
data Dog : Set where
  dog : Dog

-- * Implementation of the interface (and method).

instance-for-cat : VoiceInterface Cat
instance-for-cat = voice-interface case where
  case : Cat → String
  case x with crazy? x
  ... | true = "meeeoooowwwww!!!"
  ... | false = "meow!"

instance-for-dog : VoiceInterface Dog
instance-for-dog = voice-interface $ const "woof!"

-- * and then:
--
-- say dog => "woof!"
-- say (cat crazy!) => "meeeoooowwwww!!!"
-- say (cat plain-cat) => "meow!"
--

max_stars_repo_name: mullikine/RosettaCodeData

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
module Dave.Isomorphism where
    open import Dave.Equality
    open import Dave.Functions

    infix 0 _≃_
    record _≃_ (A B : Set) : Set where
        field
            to : A → B
            from : B → A
            from∘to : ∀ (x : A) → from (to x) ≡ x
            to∘from : ∀ (x : B) → to (from x) ≡ x
    open _≃_

    {- Another way to define Isomporphism throug data -}
    data _≃′_ (A B : Set) : Set where
        mk-≃′ : ∀ (to : A → B) →
                ∀ (from : B → A) →
                ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
                ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
                A ≃′ B

    to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
    to′ (mk-≃′ f g g∘f f∘g) = f

    from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
    from′ (mk-≃′ f g g∘f f∘g) = g

    from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (x : A) → from′ A≃B (to′ A≃B x) ≡ x)
    from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

    to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B) → (∀ (y : B) → to′ A≃B (from′ A≃B y) ≡ y)
    to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

    ≃-refl : ∀ {A : Set} → A ≃ A
    ≃-refl = record
        {
            to = λ x → x;
            from = λ y → y;
            from∘to = λ x → refl;
            to∘from = λ y → refl
        }

    ≃-sym : ∀ {A B : Set} → A ≃ B → B ≃ A
    ≃-sym A≃B = record
        {
            to = from A≃B ;
            from = to A≃B ;
            from∘to = to∘from A≃B ;
            to∘from = from∘to A≃B
        }

    ≃-trans : ∀ {A B C : Set} → A ≃ B → B ≃ C → A ≃ C
    ≃-trans A≃B B≃C = record
        {
            to = (to B≃C) ∘ (to A≃B);
            from = (from A≃B) ∘ (from B≃C);
            from∘to = λ x → begin
                (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x) ≡⟨⟩
                from A≃B (from B≃C (to B≃C (to A≃B x))) ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
                from A≃B (to A≃B x) ≡⟨ from∘to A≃B x ⟩
                x ∎;
            to∘from = λ x → begin
                (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) x) ≡⟨⟩
                to B≃C (to A≃B (from A≃B (from B≃C x))) ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C x)) ⟩
                to B≃C (from B≃C x) ≡⟨ to∘from B≃C x ⟩
                x ∎
        }

    module ≃-Reasoning where

        infix  1 ≃-begin_
        infixr 2 _≃⟨_⟩_
        infix  3 _≃-∎

        ≃-begin_ : ∀ {A B : Set}
            → A ≃ B
            -----
            → A ≃ B
        ≃-begin A≃B = A≃B

        _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
            → A ≃ B
            → B ≃ C
            -----
            → A ≃ C
        A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

        _≃-∎ : ∀ (A : Set)
            -----
            → A ≃ A
        A ≃-∎ = ≃-refl

    open ≃-Reasoning public


text:
open import Relation.Binary.Core

module Mergesort.Impl2.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import List.Properties A
open import LRTree {A}
open import Mergesort.Impl2 _≤_ tot≤
open import OList _≤_

lemma-merge'-empty : {b : Bound}(xs : OList b) → merge' xs (onil {b}) ≡ xs
lemma-merge'-empty onil = refl
lemma-merge'-empty (:< b≤x xs) = refl

mutual
  lemma-merge' : {b : Bound}(xs ys : OList b) → (forget xs ++ forget ys) ∼ forget (merge' xs ys)
  lemma-merge' onil ys = refl∼
  lemma-merge' xs onil rewrite ++id (forget xs) | lemma-merge'-empty xs = refl∼
  lemma-merge' (:< {x = x} b≤x xs) (:< {x = y} b≤y ys)
      with tot≤ x y
  ... | inj₁ x≤y  = ∼x /head /head (lemma-merge' xs (:< (lexy x≤y) ys))
  ... | inj₂ y≤x =
                  let f'xxsyf'ys∼yf'xxsf'ys = ∼x (lemma++/ {y} {forget (:< b≤x xs)}) /head refl∼ ;
                       yf'xxsf'ys∼yf'm'xxsys = ∼x /head /head (lemma-merge'xs (lexy y≤x) xs ys)
                  in trans∼ f'xxsyf'ys∼yf'xxsf'ys yf'xxsf'ys∼yf'm'xxsys

  lemma-merge'xs : {b : Bound}{x : A} → (b≤x : LeB b (val x))(xs : OList (val x))(ys : OList b) → (forget (:< b≤x xs) ++ forget ys) ∼ forget (merge'xs b≤x xs ys)
  lemma-merge'xs b≤x xs onil rewrite ++id (forget xs) | lemma-merge'-empty xs = refl∼
  lemma-merge'xs {x = x} b≤x xs (:< {x = y} b≤y ys)
      with tot≤ x y
  ... | inj₁ x≤y = ∼x /head /head (lemma-merge' xs (:< (lexy x≤y) ys))
  ... | inj₂ y≤x =
                  let f'xxsyf'ys∼yf'xxsf'ys = ∼x (lemma++/ {y} {forget (:< b≤x xs)}) /head refl∼ ;
                       yf'xxsf'ys∼yf'm'xxsys = ∼x /head /head (lemma-merge'xs (lexy y≤x) xs ys)
                  in trans∼ f'xxsyf'ys∼yf'xxsf'ys yf'xxsf'ys∼yf'm'xxsys

lemma-insert : (x : A)(t : LRTree) → (x ∷ flatten t) ∼ flatten (insert x t)
lemma-insert x empty = ∼x /head /head ∼[]
lemma-insert x (leaf y) = ∼x (/tail /head) /head (∼x /head /head ∼[])
lemma-insert x (node left l r) = lemma++∼r (lemma-insert x l)
lemma-insert x (node right l r) =
                let xlr∼lxr = ∼x /head (lemma++/ {x} {flatten l}) refl∼ ;
                     lxr∼lrᵢ = lemma++∼l {flatten l} (lemma-insert x r)
                in trans∼ xlr∼lxr lxr∼lrᵢ

lemma-deal : (xs : List A) → xs ∼ flatten (deal xs)
lemma-deal [] = ∼[]
lemma-deal (x ∷ xs) = trans∼ (∼x /head /head (lemma-deal xs)) (lemma-insert x (deal xs))

lemma-merge : (t : LRTree) → flatten t ∼ forget (merge t)
lemma-merge empty = ∼[]
lemma-merge (leaf x) = ∼x /head /head ∼[]
lemma-merge (node t l r) =
                let flfr∼f'm'lf'm'r = lemma++∼ (lemma-merge l) (lemma-merge r) ;
                     f'm'lf'm'r∼m''m''lm''r = lemma-merge' (merge l) (merge r)
                in trans∼ flfr∼f'm'lf'm'r f'm'lf'm'r∼m''m''lm''r

theorem-mergesort-∼ : (xs : List A) → xs ∼ (forget (mergesort xs))
theorem-mergesort-∼ xs = trans∼ (lemma-deal xs) (lemma-merge (deal xs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Data.Integer where

open import Level

open import Data.Nat using (ℕ; suc; zero)
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Bool

data ℤ : Type where
  ⁺   : ℕ → ℤ
  ⁻suc : ℕ → ℤ

⁻ : ℕ → ℤ
⁻ zero    = ⁺ zero
⁻ (suc n) = ⁻suc n

{-# DISPLAY ⁻suc n = ⁻ suc n #-}

negate : ℤ → ℤ
negate (⁺ x) = ⁻ x
negate (⁻suc x) = ⁺ (suc x)

{-# DISPLAY negate x = ⁻ x #-}

infixl 6 _+_

_-suc_ : ℕ → ℕ → ℤ
x -suc y =
  if y ℕ.<ᴮ x
    then ⁺ (x ℕ.∸ (suc y))
    else ⁻suc (y ℕ.∸ x)

_+_ : ℤ → ℤ → ℤ
⁺    x + ⁺    y = ⁺ (x ℕ.+ y)
⁺    x + ⁻suc y = x -suc y
⁻suc x + ⁺    y = y -suc x
⁻suc x + ⁻suc y = ⁻suc (suc x ℕ.+ y)

_*-suc_ : ℕ → ℕ → ℤ
zero  *-suc m = ⁺ zero
suc n *-suc m = ⁻suc (n ℕ.+ m ℕ.+ n ℕ.* m)

infixl 7 _*_
_*_ : ℤ → ℤ → ℤ
⁺    x * ⁺    y = ⁺ (x ℕ.* y)
⁺    x * ⁻suc y = x *-suc y
⁻suc x * ⁺    y = y *-suc x
⁻suc x * ⁻suc y = ⁺ (suc x ℕ.* suc y)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground