text:
------------------------------------------------------------------------
-- This module establishes that the recognisers are as expressive as
-- possible when the alphabet is Bool (this could be generalised to
-- arbitrary finite alphabets), whereas this is not the case when the
-- alphabet is ℕ
------------------------------------------------------------------------

module TotalRecognisers.LeftRecursion.ExpressiveStrength where

open import Algebra
open import Codata.Musical.Notation
open import Data.Bool as Bool hiding (_∧_)
open import Data.Empty
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using (_⇔_; equivalence; module Equivalence)
open import Data.List
import Data.List.Properties as ListProp
open import Data.List.Reverse
open import Data.Nat as Nat
open import Data.Nat.InfinitelyOften as Inf
import Data.Nat.Properties as NatProp
open import Data.Product
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation
private
  module ListMonoid {A : Set} = Monoid (ListProp.++-monoid A)
  module NatOrder             = DecTotalOrder NatProp.≤-decTotalOrder

import TotalRecognisers.LeftRecursion
open TotalRecognisers.LeftRecursion Bool using (_∧_; left-zero)
private
  open module LR {Tok : Set} = TotalRecognisers.LeftRecursion Tok
    hiding (P; ∞⟨_⟩P; _∧_; left-zero; _∷_)

  P : Set → Bool → Set
  P Tok = LR.P {Tok}

  ∞⟨_⟩P : Bool → Set → Bool → Set
  ∞⟨ b ⟩P Tok n = LR.∞⟨_⟩P {Tok} b n

open import TotalRecognisers.LeftRecursion.Lib Bool hiding (_∷_)

------------------------------------------------------------------------
-- A boring lemma

private

  lemma : (f : List Bool → Bool) →
          (false ∧ f [ true ] ∨ false ∧ f [ false ]) ∨ f [] ≡ f []
  lemma f = cong₂ (λ b₁ b₂ → (b₁ ∨ b₂) ∨ f [])
                  (left-zero (f [ true  ]))
                  (left-zero (f [ false ]))

------------------------------------------------------------------------
-- Expressive strength

-- For every grammar there is an equivalent decidable predicate.

grammar⇒pred : ∀ {Tok n} (p : P Tok n) →
               ∃ λ (f : List Tok → Bool) → ∀ {s} → s ∈ p ⇔ T (f s)
grammar⇒pred p =
  ((λ s → ⌊ s ∈? p ⌋) , λ {_} → equivalence fromWitness toWitness)

-- When the alphabet is Bool the other direction holds: for every
-- decidable predicate there is a corresponding grammar.
--
-- Note that the grammars constructed by the proof are all "infinite
-- LL(1)".

pred⇒grammar : (f : List Bool → Bool) →
               ∃ λ (p : P Bool (f [])) → ∀ {s} → s ∈ p ⇔ T (f s)
pred⇒grammar f =
  (p f , λ {s} → equivalence (p-sound f) (p-complete f s))
  where
  p : (f : List Bool → Bool) → P Bool (f [])
  p f = cast (lemma f)
      ( ♯? (sat id ) · ♯ p (f ∘ _∷_ true )
      ∣ ♯? (sat not) · ♯ p (f ∘ _∷_ false)
      ∣ accept-if-true (f [])
      )

  p-sound : ∀ f {s} → s ∈ p f → T (f s)
  p-sound f (cast (∣-right s∈)) with AcceptIfTrue.sound (f []) s∈
  ... | (refl , ok) = ok
  p-sound f (cast (∣-left (∣-left (t∈ · s∈)))) with drop-♭♯ (f [ true  ]) t∈
  ... | sat {t = true}  _  = p-sound (f ∘ _∷_ true ) s∈
  ... | sat {t = false} ()
  p-sound f (cast (∣-left (∣-right (t∈ · s∈)))) with drop-♭♯ (f [ false ]) t∈
  ... | sat {t = false} _  = p-sound (f ∘ _∷_ false) s∈
  ... | sat {t = true}  ()

  p-complete : ∀ f s → T (f s) → s ∈ p f
  p-complete f [] ok =
    cast (∣-right {n₁ = false ∧ f [ true ] ∨ false ∧ f [ false ]} $
      AcceptIfTrue.complete ok)
  p-complete f (true  ∷ bs) ok =
    cast (∣-left $ ∣-left $
      add-♭♯ (f [ true  ]) (sat _) ·
      p-complete (f ∘ _∷_ true ) bs ok)
  p-complete f (false ∷ bs) ok =
    cast (∣-left $ ∣-right {n₁ = false ∧ f [ true ]} $
      add-♭♯ (f [ false ]) (sat _) ·
      p-complete (f ∘ _∷_ false) bs ok)

-- An alternative proof which uses a left recursive definition of the
-- grammar to avoid the use of a cast.

pred⇒grammar′ : (f : List Bool → Bool) →
                ∃ λ (p : P Bool (f [])) → ∀ {s} → s ∈ p ⇔ T (f s)
pred⇒grammar′ f =
  (p f , λ {s} → equivalence (p-sound f) (p-complete f s))
  where
  extend : {A B : Set} → (List A → B) → A → (List A → B)
  extend f x = λ xs → f (xs ∷ʳ x)

  p : (f : List Bool → Bool) → P Bool (f [])
  p f = ♯ p (extend f true ) · ♯? (sat id )
      ∣ ♯ p (extend f false) · ♯? (sat not)
      ∣ accept-if-true (f [])

  p-sound : ∀ f {s} → s ∈ p f → T (f s)
  p-sound f (∣-right s∈) with AcceptIfTrue.sound (f []) s∈
  ... | (refl , ok) = ok
  p-sound f (∣-left (∣-left (s∈ · t∈))) with drop-♭♯ (f [ true  ]) t∈
  ... | sat {t = true}  _  = p-sound (extend f true ) s∈
  ... | sat {t = false} ()
  p-sound f (∣-left (∣-right (s∈ · t∈))) with drop-♭♯ (f [ false ]) t∈
  ... | sat {t = false} _  = p-sound (extend f false) s∈
  ... | sat {t = true}  ()

  p-complete′ : ∀ f {s} → Reverse s → T (f s) → s ∈ p f
  p-complete′ f [] ok =
    ∣-right {n₁ = false} $ AcceptIfTrue.complete ok
  p-complete′ f (bs ∶ rs ∶ʳ true ) ok =
    ∣-left {n₁ = false} $ ∣-left {n₁ = false} $
      p-complete′ (extend f true ) rs ok ·
      add-♭♯ (f [ true  ]) (sat _)
  p-complete′ f (bs ∶ rs ∶ʳ false) ok =
    ∣-left {n₁ = false} $ ∣-right {n₁ = false} $
      p-complete′ (extend f false) rs ok ·
      add-♭♯ (f [ false ]) (sat _)

  p-complete : ∀ f s → T (f s) → s ∈ p f
  p-complete f s = p-complete′ f (reverseView s)

-- If infinite alphabets are allowed the result is different: there
-- are decidable predicates which cannot be realised as grammars. The
-- proof below shows that a recogniser for natural number strings
-- cannot accept exactly the strings of the form "nn".

module NotExpressible where

  -- A "pair" is a string containing two equal elements.

  pair : ℕ → List ℕ
  pair n = n ∷ n ∷ []

  -- OnlyPairs p is inhabited iff p only accepts pairs and empty
  -- strings. (Empty strings are allowed due to the presence of the
  -- nonempty combinator.)

  OnlyPairs : ∀ {n} → P ℕ n → Set
  OnlyPairs p = ∀ {n s} → n ∷ s ∈ p → s ≡ [ n ]

  -- ManyPairs p is inhabited iff p accepts infinitely many pairs.

  ManyPairs : ∀ {n} → P ℕ n → Set
  ManyPairs p = Inf (λ n → pair n ∈ p)

  -- AcceptsNonEmptyString p is inhabited iff p accepts a non-empty
  -- string.

  AcceptsNonEmptyString : ∀ {Tok n} → P Tok n → Set
  AcceptsNonEmptyString p = ∃₂ λ t s → t ∷ s ∈ p

  -- If a recogniser does not accept any non-empty string, then it
  -- either accepts the empty string or no string at all.

  nullable-or-fail : ∀ {Tok n} {p : P Tok n} →
                     ¬ AcceptsNonEmptyString p →
                     [] ∈ p ⊎ (∀ s → ¬ s ∈ p)
  nullable-or-fail {p = p} ¬a with [] ∈? p
  ... | yes []∈p = inj₁ []∈p
  ... | no  []∉p = inj₂ helper
    where
    helper : ∀ s → ¬ s ∈ p
    helper []      = []∉p
    helper (t ∷ s) = ¬a ∘ _,_ t ∘ _,_ s

  -- If p₁ · p₂ accepts infinitely many pairs, and nothing but pairs
  -- (or the empty string), then at most one of p₁ and p₂ accepts a
  -- non-empty string. This follows because p₁ and p₂ are independent
  -- of each other. For instance, if p₁ accepted n and p₂ accepted i
  -- and j, then p₁ · p₂ would accept both ni and nj, and if p₁
  -- accepted mm and p₂ accepted n then p₁ · p₂ would accept mmn.

  at-most-one : ∀ {n₁ n₂} {p₁ : ∞⟨ n₂ ⟩P ℕ n₁} {p₂ : ∞⟨ n₁ ⟩P ℕ n₂} →
                OnlyPairs (p₁ · p₂) →
                ManyPairs (p₁ · p₂) →
                AcceptsNonEmptyString (♭? p₁) →
                AcceptsNonEmptyString (♭? p₂) → ⊥
  at-most-one op mp (n₁ , s₁ , n₁s₁∈p₁) (n₂ , s₂ , n₂s₂∈p₂)
    with op (n₁s₁∈p₁ · n₂s₂∈p₂)
  at-most-one _ _ (_ , _ ∷ []    , _) (_ , _ , _) | ()
  at-most-one _ _ (_ , _ ∷ _ ∷ _ , _) (_ , _ , _) | ()
  at-most-one {p₁ = p₁} {p₂} op mp
              (n , [] , n∈p₁) (.n , .[] , n∈p₂) | refl =
    twoDifferentWitnesses mp helper
    where
    ¬pair : ∀ {i s} → s ∈ p₁ · p₂ → n ≢ i → s ≢ pair i
    ¬pair (_·_ {s₁ = []}          _ ii∈p₂) n≢i refl with op (n∈p₁ · ii∈p₂)
    ... | ()
    ¬pair (_·_ {s₁ = i  ∷ []}     i∈p₁  _) n≢i refl with op (i∈p₁ · n∈p₂)
    ¬pair (_·_ {s₁ = .n ∷ []}     n∈p₁  _) n≢n refl | refl = n≢n refl
    ¬pair (_·_ {s₁ = i ∷ .i ∷ []} ii∈p₁ _) n≢i refl with op (ii∈p₁ · n∈p₂)
    ... | ()
    ¬pair (_·_ {s₁ = _ ∷ _ ∷ _ ∷ _} _ _) _ ()

    helper : ¬ ∃₂ λ i j → i ≢ j × pair i ∈ p₁ · p₂ × pair j ∈ p₁ · p₂
    helper (i  , j , i≢j , ii∈ , jj∈) with Nat._≟_ n i
    helper (.n , j , n≢j , nn∈ , jj∈) | yes refl = ¬pair jj∈ n≢j refl
    helper (i  , j , i≢j , ii∈ , jj∈) | no  n≢i  = ¬pair ii∈ n≢i refl

  -- OnlyPairs and ManyPairs are mutually exclusive.

  ¬pairs : ∀ {n} (p : P ℕ n) → OnlyPairs p → ManyPairs p → ⊥
  ¬pairs fail op mp = witness mp (helper ∘ proj₂)
    where
    helper : ∀ {t} → ¬ pair t ∈ fail
    helper ()
  ¬pairs empty op mp = witness mp (helper ∘ proj₂)
    where
    helper : ∀ {t} → ¬ pair t ∈ empty
    helper ()
  ¬pairs (sat f) op mp = witness mp (helper ∘ proj₂)
    where
    helper : ∀ {t} → ¬ pair t ∈ sat f
    helper ()
  ¬pairs (nonempty p) op mp =
    ¬pairs p (op ∘ nonempty) (Inf.map helper mp)
    where
    helper : ∀ {n} → pair n ∈ nonempty p → pair n ∈ p
    helper (nonempty pr) = pr
  ¬pairs (cast eq p) op mp = ¬pairs p (op ∘ cast) (Inf.map helper mp)
    where
    helper : ∀ {n} → pair n ∈ cast eq p → pair n ∈ p
    helper (cast pr) = pr

  -- The most interesting cases are _∣_ and _·_. For the choice
  -- combinator we make use of the fact that if p₁ ∣ p₂ accepts
  -- infinitely many pairs, then at least one of p₁ and p₂ do. (We are
  -- deriving a contradiction, so the use of classical reasoning is
  -- unproblematic.)

  ¬pairs (p₁ ∣ p₂) op mp = commutes-with-∪ (Inf.map split mp) helper
    where
    helper : ¬ (ManyPairs p₁ ⊎ ManyPairs p₂)
    helper (inj₁ mp₁) = ¬pairs p₁ (op ∘ ∣-left)            mp₁
    helper (inj₂ mp₂) = ¬pairs p₂ (op ∘ ∣-right {p₁ = p₁}) mp₂

    split : ∀ {s} → s ∈ p₁ ∣ p₂ → s ∈ p₁ ⊎ s ∈ p₂
    split (∣-left  s∈p₁) = inj₁ s∈p₁
    split (∣-right s∈p₂) = inj₂ s∈p₂

  -- For the sequencing combinator we make use of the fact that the
  -- argument recognisers cannot both accept non-empty strings.

  ¬pairs (p₁ · p₂) op mp =
    excluded-middle λ a₁? →
    excluded-middle λ a₂? →
    helper a₁? a₂?
    where
    continue : {n n′ : Bool} (p : ∞⟨ n′ ⟩P ℕ n) → n′ ≡ true →
               OnlyPairs (♭? p) → ManyPairs (♭? p) → ⊥
    continue p eq with forced? p
    continue p refl | true = ¬pairs p
    continue p ()   | false

    helper : Dec (AcceptsNonEmptyString (♭? p₁)) →
             Dec (AcceptsNonEmptyString (♭? p₂)) → ⊥
    helper (yes a₁) (yes a₂) = at-most-one op mp a₁ a₂

    helper (no ¬a₁) _ with nullable-or-fail ¬a₁
    ... | inj₁ []∈p₁ =
      continue p₂ (⇒ []∈p₁) (op ∘ _·_ []∈p₁) (Inf.map right mp)
      where
      right : ∀ {s} → s ∈ p₁ · p₂ → s ∈ ♭? p₂
      right (_·_ {s₁ = []}    _ ∈p₂) = ∈p₂
      right (_·_ {s₁ = _ ∷ _} ∈p₁ _) = ⊥-elim (¬a₁ (-, -, ∈p₁))
    ... | inj₂ is-fail = witness mp (∉ ∘ proj₂)
      where
      ∉ : ∀ {s} → ¬ s ∈ p₁ · p₂
      ∉ (∈p₁ · _) = is-fail _ ∈p₁

    helper _ (no ¬a₂) with nullable-or-fail ¬a₂
    ... | inj₁ []∈p₂ =
      continue p₁ (⇒ []∈p₂)
               (op ∘ (λ ∈p₁ → cast∈ (proj₂ ListMonoid.identity _) refl
                              (∈p₁ · []∈p₂)))
               (Inf.map left mp)
      where
      left : ∀ {s} → s ∈ p₁ · p₂ → s ∈ ♭? p₁
      left (_·_ {s₂ = _ ∷ _}        _ ∈p₂) = ⊥-elim (¬a₂ (-, -, ∈p₂))
      left (_·_ {s₁ = s₁} {s₂ = []} ∈p₁ _) =
        cast∈ (sym $ proj₂ ListMonoid.identity s₁) refl ∈p₁
    ... | inj₂ is-fail = witness mp (∉ ∘ proj₂)
      where
      ∉ : ∀ {s} → ¬ s ∈ p₁ · p₂
      ∉ (_ · ∈p₂) = is-fail _ ∈p₂

  -- Note that it is easy to decide whether a string is a pair or not.

  pair? : List ℕ → Bool
  pair? (m ∷ n ∷ []) = ⌊ Nat._≟_ m n ⌋
  pair? _            = false

  -- This means that there are decidable predicates over token strings
  -- which cannot be realised using the recogniser combinators.

  not-realisable :
    ¬ ∃₂ (λ n (p : P ℕ n) → ∀ {s} → s ∈ p ⇔ T (pair? s))
  not-realisable (_ , p , hyp) = ¬pairs p op mp
    where
    op : OnlyPairs p
    op {n} {[]}         s∈p = ⊥-elim (Equivalence.to hyp ⟨$⟩ s∈p)
    op {n} { m ∷ []}    s∈p with toWitness (Equivalence.to hyp ⟨$⟩ s∈p)
    op {n} {.n ∷ []}    s∈p | refl = refl
    op {n} {_  ∷ _ ∷ _} s∈p = ⊥-elim (Equivalence.to hyp ⟨$⟩ s∈p)

    mp : ManyPairs p
    mp (i , ¬pair) =
      ¬pair i NatOrder.refl $ Equivalence.from hyp ⟨$⟩ fromWitness refl

not-expressible :
  ∃₂ λ (Tok : Set) (f : List Tok → Bool) →
    ¬ ∃₂ (λ n (p : P Tok n) → ∀ {s} → s ∈ p ⇔ T (f s))
not-expressible = (ℕ , pair? , not-realisable)
  where open NotExpressible

max_stars_repo_name: nad/parser-combinators


text:
module Lemmachine.Spike where
open import Data.Fin
open import Data.Digit

-- 3.9 Quality Values

DIGIT = Decimal

data qvalue : DIGIT → DIGIT → DIGIT → Set where
  zero : (d₁ d₂ d₃ : DIGIT) → qvalue d₁ d₂ d₃
  one : qvalue zero zero zero

ext: agda

max_issues_repo_name: larrytheliquid/Lemmachine


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Commutativity where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category

private
  variable
    ℓ ℓ' : Level

module _ {C : Precategory ℓ ℓ'} where
  open Precategory C

  compSq : ∀ {x y z w u v} {f : C [ x , y ]} {g h} {k : C [ z , w ]} {l} {m} {n : C [ u , v ]}
       -- square 1
       → f ⋆ g ≡ h ⋆ k
       -- square 2 (sharing g)
       → k ⋆ l ≡ m ⋆ n
       → f ⋆ (g ⋆ l) ≡ (h ⋆ m) ⋆ n
  compSq {f = f} {g} {h} {k} {l} {m} {n} p q
    = f ⋆ (g ⋆ l)
    ≡⟨ sym (⋆Assoc _ _ _) ⟩
      (f ⋆ g) ⋆ l
    ≡⟨ cong (_⋆ l) p ⟩
      (h ⋆ k) ⋆ l
    ≡⟨ ⋆Assoc _ _ _ ⟩
      h ⋆ (k ⋆ l)
    ≡⟨ cong (h ⋆_) q ⟩
      h ⋆ (m ⋆ n)
    ≡⟨ sym (⋆Assoc _ _ _) ⟩
      (h ⋆ m) ⋆ n
    ∎

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic induction
------------------------------------------------------------------------

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

module Induction.Lexicographic where

open import Data.Product
open import Induction
open import Level

-- The structure of lexicographic induction.

Σ-Rec : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : A → Set b} →
        RecStruct A (ℓ₁ ⊔ b) ℓ₂ → (∀ x → RecStruct (B x) ℓ₁ ℓ₃) →
        RecStruct (Σ A B) _ _
Σ-Rec RecA RecB P (x , y) =
  -- Either x is constant and y is "smaller", ...
  RecB x (λ y' → P (x , y')) y
    ×
  -- ...or x is "smaller" and y is arbitrary.
  RecA (λ x' → ∀ y' → P (x' , y')) x

_⊗_ : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} →
      RecStruct A (ℓ₁ ⊔ b) ℓ₂ → RecStruct B ℓ₁ ℓ₃ →
      RecStruct (A × B) _ _
RecA ⊗ RecB = Σ-Rec RecA (λ _ → RecB)

-- Constructs a recursor builder for lexicographic induction.

Σ-rec-builder :
  ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : A → Set b}
    {RecA : RecStruct A (ℓ₁ ⊔ b) ℓ₂}
    {RecB : ∀ x → RecStruct (B x) ℓ₁ ℓ₃} →
  RecursorBuilder RecA → (∀ x → RecursorBuilder (RecB x)) →
  RecursorBuilder (Σ-Rec RecA RecB)
Σ-rec-builder {RecA = RecA} {RecB = RecB} recA recB P f (x , y) =
  (p₁ x y p₂x , p₂x)
  where
  p₁ : ∀ x y →
       RecA (λ x' → ∀ y' → P (x' , y')) x →
       RecB x (λ y' → P (x , y')) y
  p₁ x y x-rec = recB x
                      (λ y' → P (x , y'))
                      (λ y y-rec → f (x , y) (y-rec , x-rec))
                      y

  p₂ : ∀ x → RecA (λ x' → ∀ y' → P (x' , y')) x
  p₂ = recA (λ x → ∀ y → P (x , y))
            (λ x x-rec y → f (x , y) (p₁ x y x-rec , x-rec))

  p₂x = p₂ x

[_⊗_] : ∀ {a b ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b}
          {RecA : RecStruct A (ℓ₁ ⊔ b) ℓ₂} {RecB : RecStruct B ℓ₁ ℓ₃} →
        RecursorBuilder RecA → RecursorBuilder RecB →
        RecursorBuilder (RecA ⊗ RecB)
[ recA ⊗ recB ] = Σ-rec-builder recA (λ _ → recB)

------------------------------------------------------------------------
-- Example

private

  open import Data.Nat
  open import Induction.Nat as N

  -- The Ackermann function à la Rózsa Péter.

  ackermann : ℕ → ℕ → ℕ
  ackermann m n =
    build [ N.recBuilder ⊗ N.recBuilder ]
          (λ _ → ℕ)
          (λ { (zero  , n)     _                   → 1 + n
             ; (suc m , zero)  (_         , ackm•) → ackm• 1
             ; (suc m , suc n) (ack[1+m]n , ackm•) → ackm• ack[1+m]n
             })
          (m , n)


text:
{-

This file contains:

- Fibers of induced map between set truncations is the set truncation of fibers
  modulo a certain equivalence relation defined by π₁ of the base.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.SetTruncation.Fibers where

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Path
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as Prop
open import Cubical.HITs.SetTruncation as Set
open import Cubical.HITs.SetQuotients as SetQuot

open import Cubical.Relation.Binary

private
  variable
    ℓ ℓ' : Level

module _
  {X : Type ℓ }
  {Y : Type ℓ'}
  (f : X → Y) where

  private
    ∥f∥₂ : ∥ X ∥₂ → ∥ Y ∥₂
    ∥f∥₂ = Set.map f

  module _ (y : Y) where

    open Iso

    isSetFiber∥∥₂ : isSet (fiber ∥f∥₂ ∣ y ∣₂)
    isSetFiber∥∥₂ = isOfHLevelΣ 2 squash₂ (λ _ → isProp→isSet (squash₂ _ _))

    fiberRel : ∥ fiber f y ∥₂ → ∥ fiber f y ∥₂ → Type ℓ
    fiberRel a b = Set.map fst a ≡ Set.map fst b

    private
      proj : ∥ fiber f y ∥₂ / fiberRel → ∥ X ∥₂
      proj = SetQuot.rec squash₂ (Set.map fst) (λ _ _ p → p)

    ∥fiber∥₂/R→fiber∥∥₂ : ∥ fiber f y ∥₂ / fiberRel → fiber ∥f∥₂ ∣ y ∣₂
    ∥fiber∥₂/R→fiber∥∥₂ = SetQuot.rec isSetFiber∥∥₂ ∥fiber∥₂→fiber∥∥₂ feq
      where
      fiber→fiber∥∥₂ : fiber f y → fiber ∥f∥₂ ∣ y ∣₂
      fiber→fiber∥∥₂ (x , p) = ∣ x ∣₂ , cong ∣_∣₂ p

      ∥fiber∥₂→fiber∥∥₂ : ∥ fiber f y ∥₂ → fiber ∥f∥₂ ∣ y ∣₂
      ∥fiber∥₂→fiber∥∥₂ = Set.rec isSetFiber∥∥₂ fiber→fiber∥∥₂

      feq : (a b : ∥ fiber f y ∥₂) (r : fiberRel a b) → ∥fiber∥₂→fiber∥∥₂ a ≡ ∥fiber∥₂→fiber∥∥₂ b
      feq =
        Set.elim2 (λ _ _ → isProp→isSet (isPropΠ (λ _ → isSetFiber∥∥₂ _ _))) λ _ _ p →
        ΣPathP (p , isSet→isSet' squash₂ _ _ _ _)

    mereFiber→∥fiber∥₂/R : (x : X) → ∥ f x ≡ y ∥ → ∥ fiber f y ∥₂ / fiberRel
    mereFiber→∥fiber∥₂/R x = Prop.rec→Set squash/ (λ p → [ ∣ _ , p ∣₂ ]) (λ _ _ → eq/ _ _ refl)

    fiber∥∥₂→∥fiber∥₂/R : fiber ∥f∥₂ ∣ y ∣₂ → ∥ fiber f y ∥₂ / fiberRel
    fiber∥∥₂→∥fiber∥₂/R =
      uncurry
        (Set.elim (λ _ → isSetΠ λ _ → squash/) λ x p →
          mereFiber→∥fiber∥₂/R x (PathIdTrunc₀Iso .fun p))

    ∥fiber∥₂/R→fiber∥∥₂→fst : (q : ∥ fiber f y ∥₂ / fiberRel) → ∥fiber∥₂/R→fiber∥∥₂ q .fst ≡ proj q
    ∥fiber∥₂/R→fiber∥∥₂→fst =
      SetQuot.elimProp (λ _ → squash₂ _ _)
        (Set.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ _ → refl))

    fiber∥∥₂→∥fiber∥₂/R→proj : (x : fiber ∥f∥₂ ∣ y ∣₂) → proj (fiber∥∥₂→∥fiber∥₂/R x) ≡ x .fst
    fiber∥∥₂→∥fiber∥₂/R→proj =
      uncurry
        (Set.elim (λ _ → isSetΠ λ _ → isProp→isSet (squash₂ _ _)) λ x p →
          Prop.elim {P = λ t → proj (mereFiber→∥fiber∥₂/R x t) ≡ ∣ x ∣₂}
            (λ _ → squash₂ _ _)
            (λ _ → refl)
            (PathIdTrunc₀Iso .fun p))

    ∥fiber∥₂/R→fiber∥∥₂→∥fiber∥₂/R :
      (x : ∥ fiber f y ∥₂ / fiberRel) → fiber∥∥₂→∥fiber∥₂/R (∥fiber∥₂/R→fiber∥∥₂ x) ≡ x
    ∥fiber∥₂/R→fiber∥∥₂→∥fiber∥₂/R =
      SetQuot.elimProp (λ _ → squash/ _ _)
        (Set.elim (λ _ → isProp→isSet (squash/ _ _))
          (λ _ → eq/ _ _ refl))

    fiber∥∥₂→∥fiber∥₂/R→fiber∥∥₂ :
      (x : fiber ∥f∥₂ ∣ y ∣₂) → ∥fiber∥₂/R→fiber∥∥₂ (fiber∥∥₂→∥fiber∥₂/R x) ≡ x
    fiber∥∥₂→∥fiber∥₂/R→fiber∥∥₂ x =
      Σ≡Prop
        (λ _ → squash₂ _ _)
        (∥fiber∥₂/R→fiber∥∥₂→fst (fiber∥∥₂→∥fiber∥₂/R x) ∙ fiber∥∥₂→∥fiber∥₂/R→proj x)

    Iso-∥fiber∥₂/R-fiber∥∥₂ : Iso (∥ fiber f y ∥₂ / fiberRel) (fiber ∥f∥₂ ∣ y ∣₂)
    Iso-∥fiber∥₂/R-fiber∥∥₂ .fun = ∥fiber∥₂/R→fiber∥∥₂
    Iso-∥fiber∥₂/R-fiber∥∥₂ .inv = fiber∥∥₂→∥fiber∥₂/R
    Iso-∥fiber∥₂/R-fiber∥∥₂ .leftInv = ∥fiber∥₂/R→fiber∥∥₂→∥fiber∥₂/R
    Iso-∥fiber∥₂/R-fiber∥∥₂ .rightInv = fiber∥∥₂→∥fiber∥₂/R→fiber∥∥₂

    -- main results

    ∥fiber∥₂/R≃fiber∥∥₂ : ∥ fiber f y ∥₂ / fiberRel ≃ fiber ∥f∥₂ ∣ y ∣₂
    ∥fiber∥₂/R≃fiber∥∥₂ = isoToEquiv Iso-∥fiber∥₂/R-fiber∥∥₂

    -- the relation is an equivalence relation

    open BinaryRelation
    open isEquivRel

    isEquivRelFiberRel : isEquivRel fiberRel
    isEquivRelFiberRel .reflexive _ = refl
    isEquivRelFiberRel .symmetric _ _ = sym
    isEquivRelFiberRel .transitive _ _ _ = _∙_

    -- alternative characterization of the relation in terms of equality in Y and fiber f y

    ∣transport∣ : ∥ y ≡ y ∥₂ → ∥ fiber f y ∥₂ → ∥ fiber f y ∥₂
    ∣transport∣ = Set.rec2 squash₂ (λ s (x , q) → ∣ x , q ∙ s ∣₂)

    fiberRel2 : (x x' : ∥ fiber f y ∥₂) → Type (ℓ-max ℓ ℓ')
    fiberRel2 x x' = ∥ Σ[ s ∈ ∥ y ≡ y ∥₂ ] ∣transport∣ s x ≡ x' ∥

    fiberRel2→1 : ∀ x x' → fiberRel2 x x' → fiberRel x x'
    fiberRel2→1 =
      Set.elim2 (λ _ _ → isSetΠ λ _ → isOfHLevelPath 2 squash₂ _ _) λ _ _ →
      Prop.rec (squash₂ _ _)
        (uncurry
          (Set.elim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 squash₂ _ _) λ _ →
            cong (Set.map fst)))

    fiberRel1→2 : ∀ x x' → fiberRel x x' → fiberRel2 x x'
    fiberRel1→2 =
      Set.elim2 (λ _ _ → isSetΠ λ _ → isProp→isSet squash) λ a b p →
      Prop.rec squash
        (λ q →
          let
            filler = doubleCompPath-filler (sym (a .snd)) (cong f q) (b .snd)
          in
            ∣ ∣ filler i1 ∣₂ , cong ∣_∣₂ (ΣPathP (q , adjustLemma (flipSquare filler))) ∣)
        (PathIdTrunc₀Iso .Iso.fun p)
      where
      adjustLemma : {x y z w : Y} {p : x ≡ y} {q : x ≡ z} {r : z ≡ w} {s : y ≡ w}
        → PathP (λ i → p i ≡ r i) q s
        → PathP (λ i → p i ≡ w) (q ∙ r) s
      adjustLemma {p = p} {q} {r} {s} α i j =
        hcomp
          (λ k → λ
            { (i = i0) → compPath-filler q r k j
            ; (i = i1) → s j
            ; (j = i0) → p i
            ; (j = i1) → r (i ∨ k)})
          (α i j)

    fiberRel1≃2 : ∀ x x' → fiberRel x x' ≃ fiberRel2 x x'
    fiberRel1≃2 _ _ =
      propBiimpl→Equiv (squash₂ _ _) squash (fiberRel1→2 _ _) (fiberRel2→1 _ _)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2021 Victor C Miraldo.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Data.Unit.NonEta
open import Data.Empty
open import Data.Sum
open import Data.Product
open import Data.Product.Properties
open import Data.Fin hiding (_<_; _≤_)
open import Data.Fin.Properties using () renaming (_≟_ to _≟Fin_)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Properties using (∷-injective; length-map)
open import Data.List.Relation.Unary.Any renaming (map to Any-map)
open import Data.List.Relation.Unary.All renaming (lookup to All-lookup; map to All-map)
open import Data.List.Relation.Unary.All.Properties hiding (All-map)
open import Data.List.Relation.Unary.Any.Properties renaming (map⁺ to Any-map⁺)
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Data.Bool hiding (_<_; _≤_)
open import Data.Maybe renaming (map to Maybe-map)
open import Function

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Core
open import Relation.Nullary

-- This module defines the DepRel type, which represents the class of AAOSLs we
-- consider, and proves properties about any DepRel.

module AAOSL.Abstract.DepRel where

 open import AAOSL.Lemmas
 open import AAOSL.Abstract.Hash

 -- TODO-1: make names same as paper (lvlof -> maxlvl, etc.)
 -- The important bit is that we must have a dependency relation
 -- between these indexes.
 record DepRel : Set₁ where
   field
     lvlof      : ℕ → ℕ
     lvlof-z    : lvlof 0 ≡ 0
     lvlof-s    : ∀ m → 0 < lvlof (suc m)

   HopFrom    : ℕ → Set
   HopFrom    = Fin ∘ lvlof

   field
     hop-tgt        : {m : ℕ} → HopFrom m → ℕ

     hop-tgt-inj    : {m : ℕ}{h h' : HopFrom m}
                    → hop-tgt h ≡ hop-tgt h'
                    → h ≡ h'

     hop-<    : {m : ℕ}(h : HopFrom m)
              → hop-tgt h < m

     -- This property requires that any pair of hops is either nested or
     -- non-overlapping. When nonoverlapping, one end may coincide and
     -- when nested, both ends may coincide. As a diagram,
     --
     --                          h₂
     --            ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝
     --            ∣                             ∣
     --            ∣             h₁              ∣
     --            ∣         ⌜⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⁻⌝      |
     --            |         |            |      |
     --         tgt h₂  <I  tgt h₁  ⋯     j₁     j₂
     --                                   ↑
     --                            The only option for j₁
     --                            is right here. It can be
     --                            the same as j₂ though.
     --                            For more intuition on this, check
     --                            Hops.agda
     --
     hops-nested-or-nonoverlapping : ∀{j₁ j₂}{h₁ : HopFrom j₁}{h₂ : HopFrom j₂}
       → hop-tgt h₂ < hop-tgt h₁
       → hop-tgt h₁ < j₂
       → j₁ ≤ j₂

   _≟Hop_ : {s : ℕ}(h l : HopFrom s) → Dec (h ≡ l)
   _≟Hop_ = _≟Fin_


text:
-- Andreas, 2012-01-30, bug reported by Nisse
-- {-# OPTIONS -v tc.term.absurd:50 -v tc.signature:30 -v tc.conv.atom:30 -v tc.conv.elim:50 #-}
module Issue557 where

data ⊥ : Set where

postulate
  A : Set
  a : (⊥ → ⊥) → A
  F : A → Set
  f : (a : A) → F a

module M (I : Set → Set) where

  x : A
  x = a (λ ())

y : A
y = M.x (λ A → A)

z : F y
z = f y

-- cause was absurd lambda in a module, i.e., under a telescope (I : Set -> Set)
-- (λ ()) must be replaced by (absurd I) not just by (absurd)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Real.Complete where

import Prelude
import Data.Real.Gauge
import Data.Rational

open Prelude
open Data.Real.Gauge
open Data.Rational

Complete : Set -> Set
Complete A = Gauge -> A

unit : {A : Set} -> A -> Complete A
unit x ε = x

join : {A : Set} -> Complete (Complete A) -> Complete A
join f ε = f ε2 ε2
  where
    ε2 = ε / fromNat 2

infixr 10 _==>_

data _==>_ (A B : Set) : Set where
  uniformCts : (Gauge -> Gauge) -> (A -> B) -> A ==> B

modulus : {A B : Set} -> (A ==> B) -> Gauge -> Gauge
modulus (uniformCts μ _) = μ

forgetUniformCts : {A B : Set} -> (A ==> B) -> A -> B
forgetUniformCts (uniformCts _ f) = f

mapC : {A B : Set} -> (A ==> B) -> Complete A -> Complete B
mapC (uniformCts μ f) x ε = f (x (μ ε))

bind : {A B : Set} -> (A ==> Complete B) -> Complete A -> Complete B
bind f x = join $ mapC f x

mapC2 : {A B C : Set} -> (A ==> B ==> C) -> Complete A -> Complete B -> Complete C
mapC2 f x y ε = mapC ≈fx y ε2
  where
    ε2  = ε / fromNat 2
    ≈fx = mapC f x ε2

_○_ : {A B C : Set} -> (B ==> C) -> (A ==> B) -> A ==> C
f ○ g = uniformCts μ h
  where
    μ = modulus f ∘ modulus g
    h = forgetUniformCts f ∘ forgetUniformCts g

constCts : {A B : Set} -> A -> B ==> A
constCts a = uniformCts (const $ fromNat 1) (const a)


text:
module Issue1148 where

foo : Set → Set
foo = {!!}

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Any predicate transformer for fresh lists
------------------------------------------------------------------------

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

module Data.List.Fresh.Relation.Unary.Any where

open import Level using (Level; _⊔_; Lift)
open import Data.Empty
open import Data.Product using (∃; _,_; -,_)
open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
open import Function.Equivalence using (_⇔_; equivalence)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Unary  as U
open import Relation.Binary as B using (Rel)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)

private
  variable
    a p q r : Level
    A : Set a

module _ {A : Set a} {R : Rel A r} (P : Pred A p) where

  data Any : List# A R → Set (p ⊔ a ⊔ r) where
    here  : ∀ {x xs pr} → P x → Any (cons x xs pr)
    there : ∀ {x xs pr} → Any xs → Any (cons x xs pr)

module _ {R : Rel A r} {P : Pred A p} {x} {xs : List# A R} {pr} where

  head : ¬ Any P xs → Any P (cons x xs pr) → P x
  head ¬tail (here p)   = p
  head ¬tail (there ps) = ⊥-elim (¬tail ps)

  tail : ¬ P x → Any P (cons x xs pr) → Any P xs
  tail ¬head (here p)   = ⊥-elim (¬head p)
  tail ¬head (there ps) = ps

  toSum : Any P (cons x xs pr) → P x ⊎ Any P xs
  toSum (here p) = inj₁ p
  toSum (there ps) = inj₂ ps

  fromSum : P x ⊎ Any P xs → Any P (cons x xs pr)
  fromSum = [ here , there ]′

  ⊎⇔Any : (P x ⊎ Any P xs) ⇔ Any P (cons x xs pr)
  ⊎⇔Any = equivalence fromSum toSum

module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where

  map : {xs : List# A R} → ∀[ P ⇒ Q ] → Any P xs → Any Q xs
  map p⇒q (here p)  = here (p⇒q p)
  map p⇒q (there p) = there (map p⇒q p)

module _ {R : Rel A r} {P : Pred A p} where

  witness : {xs : List# A R} → Any P xs → ∃ P
  witness (here p)   = -, p
  witness (there ps) = witness ps

  remove   : (xs : List# A R) → Any P xs → List# A R
  remove-# : ∀ {x} {xs : List# A R} p → x # xs → x # (remove xs p)

  remove (_ ∷# xs)      (here _)  = xs
  remove (cons x xs pr) (there k) = cons x (remove xs k) (remove-# k pr)

  remove-# (here x)  (p , ps) = ps
  remove-# (there k) (p , ps) = p , remove-# k ps

infixl 4 _─_
_─_ = remove

module _ {R : Rel A r} {P : Pred A p} (P? : Decidable P) where

  any? : (xs : List# A R) → Dec (Any P xs)
  any? []        = no (λ ())
  any? (x ∷# xs) = Dec.map ⊎⇔Any (P? x ⊎-dec any? xs)


text:
module Prelude where

open import Level public hiding (zero) renaming (suc to sucℓ)
open import Size public
open import Function public

open import Data.List using (List; _∷_; []; [_]) public
open import Data.Unit using (⊤; tt) public
open import Data.Nat using (ℕ; suc; zero; _+_) public
open import Data.Sum using (inj₁; inj₂) renaming (_⊎_ to _⊕_)public
open import Data.Product public hiding (map; zip)
open import Codata.Thunk public

open import Relation.Unary hiding (_∈_; Empty) public
open import Relation.Binary.PropositionalEquality hiding ([_]) public

open import Relation.Ternary.Separation public
open import Relation.Ternary.Separation.Allstar public


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

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

record Box (P : Set) : Set where
  constructor box
  field
    unbox : P
open Box public

postulate
  A : Set
  a : A
  f : Box A → A
  f= : f (box a) ≡ a
{-# REWRITE f= #-}

[a] : Box A
unbox [a] = a

-- Works thanks to eta
test1 : [a] ≡ box a
test1 = refl

-- Should work as well
test2 : f [a] ≡ f (box a)
test2 = refl

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


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

module Data.Word8 where

import Data.Word8.Primitive as Prim
open Prim renaming (primWord8fromNat to to𝕎; primWord8toNat to from𝕎) public

open import Agda.Builtin.Bool using (Bool; true; false)
open import Relation.Nullary using (yes; no)
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

infix 4 _≟_

_≟_ : Decidable {A = Word8} _≡_
w₁ ≟ w₂ with w₁ == w₂
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _

-- toℕ : Word8 → Nat
-- toℕ = primWord8toNat

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


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

module Issue939 where

record Sigma (A : Set)(P : A → Set) : Set where
  field
    fst : A
    .snd : P fst
open Sigma

postulate
  A : Set
  P : A → Set
  x : A
  .p : P x

ex : Sigma A P
ex = record
       { fst = x
       ; snd = p
       }

ex' : Sigma A P
fst ex' = x
snd ex' = p

-- Giving p yields the following error:
-- Identifier p is declared irrelevant, so it cannot be used here
-- when checking that the expression p has type P (fst ex')

-- Fixed.  Andreas, 2013-11-05


text:
module plfa-code.Decidable where

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

data Bool : Set where
  true  : Bool
  false : Bool

open Data.Nat using (_≤_; z≤n; s≤s)

infix 4 _≤ᵇ_

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

_ : (2 ≤ᵇ 4) ≡ true
_ =
  begin
    2 ≤ᵇ 4
  ≡⟨⟩
    1 ≤ᵇ 3
  ≡⟨⟩
    0 ≤ᵇ 2
  ≡⟨⟩
    true
  ∎

_ : (4 ≤ᵇ 2) ≡ false
_ =
  begin
    4 ≤ᵇ 2
  ≡⟨⟩
    3 ≤ᵇ 1
  ≡⟨⟩
    2 ≤ᵇ 0
  ≡⟨⟩
    false
  ∎

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

T→≡ : ∀ (b : Bool) → T b → b ≡ true
T→≡ true tt = refl
T→≡ false ()

≡→T : ∀ {b : Bool} → b ≡ true → T b
≡→T refl  =  tt

≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ zero    n       tt  =  z≤n
≤ᵇ→≤ (suc m) zero    ()
≤ᵇ→≤ (suc m) (suc n) t   =  s≤s (≤ᵇ→≤ m n t)

≤→≤ᵇ : ∀ {m n : ℕ} → m ≤ n → T (m ≤ᵇ n)
≤→≤ᵇ z≤n        =  tt
≤→≤ᵇ (s≤s m≤n)  =  ≤→≤ᵇ m≤n

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

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

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

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero ≤? n = yes z≤n
suc m ≤? zero = no ¬s≤z
suc m ≤? suc n with m ≤? n
...               | yes m≤n  =  yes (s≤s m≤n)
...               | no ¬m≤n  =  no (¬s≤s ¬m≤n)

---------- practice ----------
open Eq using (cong)

_<?_ : ∀ (m n : ℕ) → Dec (m < n)
zero <? zero = no (λ ())
zero <? suc n = yes z<s
suc m <? zero = no (λ ())
suc m <? suc n with m <? n
...               | yes m<n  =  yes (s<s m<n)
...               | no ¬m<n  =  no λ{ (s<s m<n) → ¬m<n m<n}

_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
zero ≡ℕ? zero = yes refl
zero ≡ℕ? suc n = no (λ ())
suc m ≡ℕ? zero = no (λ ())
suc m ≡ℕ? suc n with m ≡ℕ? n
(suc m ≡ℕ? suc n) | yes m≡n = yes (cong suc m≡n)
(suc m ≡ℕ? suc n) | no ¬m≡n = no λ{ refl → ¬m≡n refl}

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

_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)
m ≤?′ n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}
...        | true   | p        | _            = yes (p tt)
...        | false  | _        | ¬p           = no ¬p

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

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

toWitness : ∀ {A : Set} {D : Dec A} → T ⌊ D ⌋ → A
toWitness {A} {yes x} tt = x
toWitness {A} {no ¬x} ()

fromWitness : ∀ {A : Set} {D : Dec A} → A → T ⌊ D ⌋
fromWitness {A} {yes x} _ = tt
fromWitness {A} {no ¬x} x = ¬x x

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

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

infixr 6 _∧_

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

infixr 6 _×-dec_

_×-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A × B)
yes x ×-dec yes y = yes ⟨ x , y ⟩
no ¬x ×-dec _     = no λ{ ⟨ x , y ⟩ → ¬x x}
_     ×-dec no ¬y = no λ{ ⟨ x , y ⟩ → ¬y y}

infixr 5 _∨_

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

infixr 5 _⊎-dec_

_⊎-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⊎ B)
yes x ⊎-dec _     = yes (inj₁ x)
_     ⊎-dec yes y = yes (inj₂ y)
no ¬x ⊎-dec no ¬y = no λ{ (inj₁ x) → ¬x x ; (inj₂ y) → ¬y y }

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

¬? : ∀ {A : Set} → Dec A → Dec (¬ A)
¬? (yes x)  =  no (¬¬-intro x)
¬? (no ¬x)  =  yes ¬x

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

_→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
_     →-dec yes y = yes (λ _ → y)
no ¬x →-dec _     = yes (λ x → ⊥-elim (¬x x))
yes x →-dec no ¬y = no (λ f → ¬y (f x))

---------- practice ----------
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (yes x) (yes y) = refl
∧-× (yes x) (no ¬y) = refl
∧-× (no x)  _       = refl

-- I think there is a typo, so I write ∨-⊎ instead of the origin ∨-×
∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-⊎ (yes x) _       = refl
∨-⊎ (no ¬x) (yes y) = refl
∨-⊎ (no ¬x) (no ¬y) = refl

not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ (yes x) = refl
not-¬ (no ¬x) = refl

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
module IrrelevantProjections where
import Common.Irrelevance

record [_] (A : Set) : Set where
  field
    .inflate : A

open [_] using (inflate)

-- Should fail, since proj isn't declared irrelevant.
proj : ∀ {A} → [ A ] → A
proj x = inflate x


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

open import HoTT

module homotopy.SuspAdjointLoop where

module SuspAdjointLoop {i j} (X : Ptd i) (Y : Ptd j) where

  private
    A = fst X; a₀ = snd X
    B = fst Y; b₀ = snd Y

  R : {b : B}
    → Σ (Suspension A → B) (λ h → h (north A) == b)
    → Σ (A → (b == b)) (λ k → k a₀ == idp)
  R (h , idp) =
    (λ a → ap h (merid A a ∙ ! (merid A a₀))) ,
    ap (ap h) (!-inv-r (merid A a₀))

  L : {b : B}
    → Σ (A → (b == b)) (λ k → k a₀ == idp)
    → Σ (Suspension A → B) (λ h → h (north A) == b)
  L {b} (k , _) = (SuspensionRec.f A b b k) , idp

  {- Show that R ∘ L ∼ idf -}

  R-L : {b : B} → ∀ K → R {b} (L K) == K
  R-L {b} (k , kpt) = ⊙λ= R-L-fst R-L-snd
    where
    R-L-fst : (a : A)
      → ap (SuspensionRec.f A b b k) (merid A a ∙ ! (merid A a₀)) == k a
    R-L-fst a =
      ap-∙ (SuspensionRec.f A b b k) (merid A a) (! (merid A a₀))
      ∙ ap2 _∙_ (SuspensionRec.glue-β A b b k a)
                (ap-! (SuspensionRec.f A b b k) (merid A a₀)
                 ∙ ap ! (SuspensionRec.glue-β A b b k a₀ ∙ kpt))
      ∙ ∙-unit-r (k a)

    -- lemmas generalize to do some path induction for R-L-snd
    lemma₁ : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {a₁ a₂ : A}
      (p : a₁ == a₂) {q r : f a₁ == f a₂} {s : f a₁ == f a₁}
      (α : ap f p == q) (β : q == r) (γ : q ∙ ! r == s) (δ : s == idp)
      (σ : !-inv-r r == transport (λ t → t ∙ ! r == idp) β (γ ∙ δ))
      → ap (ap f) (!-inv-r p)
        == (ap-∙ f p (! p) ∙ ap2 _∙_ α (ap-! f p ∙ ap ! (α ∙ β)) ∙ γ) ∙ δ
    lemma₁ f idp idp idp γ idp σ = σ

    lemma₂ : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
      → idp == transport (λ t → t ∙ idp == idp) α (∙-unit-r p ∙ α)
    lemma₂ idp = idp

    R-L-snd : ap (ap (SuspensionRec.f A b b k)) (!-inv-r (merid A a₀))
           == R-L-fst a₀ ∙ kpt
    R-L-snd =
      ap (ap (SuspensionRec.f A b b k)) (!-inv-r (merid A a₀))
        =⟨ lemma₁ (SuspensionRec.f A b b k) (merid A a₀)
             (SuspensionRec.glue-β A b b k a₀)
             kpt (∙-unit-r (k a₀)) kpt (lemma₂ kpt) ⟩
      R-L-fst a₀ ∙ kpt ∎

  {- Show that L ∘ R ∼ idf -}

  L-R : {b : B} → ∀ H → L {b} (R H) == H
  L-R (h , idp) = ⊙λ= L-R-fst idp
    where
    fst-lemma : ∀ {i j} {A : Type i} {B : Type j} {x y z : A}
      (f : A → B) (p : x == y) (q : z == y)
      → ap f p == ap f (p ∙ ! q) ∙' ap f q
    fst-lemma _ idp idp = idp

    L-R-fst : (σ : Suspension A) →
      SuspensionRec.f A (h (north _)) (h (north _)) (fst (R (h , idp))) σ == h σ
    L-R-fst = Suspension-elim A
      idp
      (ap h (merid A a₀))
      (λ a → ↓-='-in $
        ap h (merid A a)
          =⟨ fst-lemma h (merid A a) (merid A a₀) ⟩
        ap h (merid A a ∙ ! (merid A a₀)) ∙' ap h (merid A a₀)
          =⟨ ! (SuspensionRec.glue-β A _ _ (fst (R (h , idp))) a)
             |in-ctx (λ w → w ∙' (ap h (merid A a₀))) ⟩
        ap (fst (L (R (h , idp)))) (merid A a) ∙' ap h (merid A a₀)
        ∎)

  {- Show that R respects basepoint -}

  pres-ident : {b : B}
    → R {b} ((λ _ → b) , idp) == ((λ _ → idp) , idp)
  pres-ident {b} = ⊙λ=
    (λ a → ap-cst b (merid A a ∙ ! (merid A a₀)))
    (ap (ap (λ _ → b)) (!-inv-r (merid A a₀))
       =⟨ lemma (merid A a₀) b ⟩
     ap-cst b (merid A a₀ ∙ ! (merid A a₀))
       =⟨ ! (∙-unit-r _) ⟩
     ap-cst b (merid A a₀ ∙ ! (merid A a₀)) ∙ idp ∎)
    where
    lemma : ∀ {i j} {A : Type i} {B : Type j} {x y : A} (p : x == y) (b : B)
      → ap (ap (λ _ → b)) (!-inv-r p) == ap-cst b (p ∙ ! p)
    lemma idp b = idp

  {- Show that if there is a composition operation ⊙ on B, then R respects
     that composition, that is R {b ⊙ c} (F ⊙ G) == R {b} F ∙ R {c} G -}

  -- lift a composition operation on the codomain to the function space
  comp-lift : ∀ {i j} {A : Type i} {B C D : Type j}
    (a : A) (b : B) (c : C) (_⊙_ : B → C → D)
    → Σ (A → B) (λ f → f a == b)
    → Σ (A → C) (λ g → g a == c)
    → Σ (A → D) (λ h → h a == b ⊙ c)
  comp-lift a b c _⊙_ (f , fpt) (g , gpt) =
    (λ x → f x ⊙ g x) , ap2 _⊙_ fpt gpt

  pres-comp-fst : ∀ {i j} {A : Type i} {B : Type j} (f g : A → B)
    (_⊙_ : B → B → B) {a₁ a₂ : A} (p : a₁ == a₂)
    → ap (λ x → f x ⊙ g x) p == ap2 _⊙_ (ap f p) (ap g p)
  pres-comp-fst f g _⊙_ idp = idp

  pres-comp-snd : ∀ {i j} {A : Type i} {B : Type j} (f g : A → B)
    (_⊙_ : B → B → B) {a₁ a₂ : A} (q : a₁ == a₂)
    → ap (ap (λ x → f x ⊙ g x)) (!-inv-r q)
      == pres-comp-fst f g _⊙_ (q ∙ ! q)
         ∙ ap2 (ap2 _⊙_) (ap (ap f) (!-inv-r q)) (ap (ap g) (!-inv-r q))
  pres-comp-snd f g _⊙_ idp = idp

  pres-comp : {b c : B} (_⊙_ : B → B → B)
    (F : Σ (Suspension A → B) (λ f → f (north A) == b))
    (G : Σ (Suspension A → B) (λ f → f (north A) == c))
    → R (comp-lift (north A) b c _⊙_ F G)
      == comp-lift a₀ idp idp (ap2 _⊙_) (R F) (R G)
  pres-comp _⊙_ (f , idp) (g , idp) = ⊙λ=
    (λ a → pres-comp-fst f g _⊙_ (merid A a ∙ ! (merid A a₀)))
    (pres-comp-snd f g _⊙_ (merid A a₀))

  eqv : fst (⊙Susp X ⊙→ Y) ≃ fst (X ⊙→ ⊙Ω Y)
  eqv = equiv R L R-L L-R

  ⊙path : (⊙Susp X ⊙→ Y) == (X ⊙→ ⊙Ω Y)
  ⊙path = ⊙ua eqv pres-ident

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


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

-- Monoidal natural transformations between lax and strong symmetric
-- monoidal functors.
--
-- NOTE. Symmetric monoidal natural transformations are really just
-- monoidal natural transformations that happen to go between
-- symmetric monoidal functors.  No additional conditions are
-- necessary.  Nevertheless, the definitions in this module are useful
-- when one is working in a symmetric monoidal setting.  They also
-- help Agda's type checker by bundling the (symmetric monoidal)
-- categories and functors involved.
--
-- See
--  * John Baez, Some definitions everyone should know,
--    https://math.ucr.edu/home/baez/qg-fall2004/definitions.pdf
--  * https://ncatlab.org/nlab/show/monoidal+natural+transformation

module Categories.NaturalTransformation.Monoidal.Symmetric where

open import Level

open import Categories.Category.Monoidal using (SymmetricMonoidalCategory)
import Categories.Functor.Monoidal.Symmetric as BMF
open import Categories.Functor.Monoidal.Properties using ()
  renaming (∘-SymmetricMonoidal to _∘Fˡ_; ∘-StrongSymmetricMonoidal to _∘Fˢ_)
open import Categories.NaturalTransformation as NT using (NaturalTransformation)
import Categories.NaturalTransformation.Monoidal as MNT

module Lax where
  open BMF.Lax using (SymmetricMonoidalFunctor)
  open MNT.Lax using (IsMonoidalNaturalTransformation)
  open SymmetricMonoidalFunctor using ()
    renaming (F to UF; monoidalFunctor to MF)

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural transformations between symmetric monoidal functors.

    record SymmetricMonoidalNaturalTransformation
           (F G : SymmetricMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U          : NaturalTransformation (UF F) (UF G)
        isMonoidal : IsMonoidalNaturalTransformation (MF F) (MF G) U

      open NaturalTransformation           U          public
      open IsMonoidalNaturalTransformation isMonoidal public

  -- To shorten some definitions

  private
    _⇛_ = SymmetricMonoidalNaturalTransformation
    module U = MNT.Lax

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Conversions

    ⌊_⌋ : {F G : SymmetricMonoidalFunctor C D} →
          F ⇛ G → U.MonoidalNaturalTransformation (MF F) (MF G)
    ⌊ α ⌋ = record { U = U ; isMonoidal = isMonoidal }
      where open SymmetricMonoidalNaturalTransformation α

    ⌈_⌉ : {F G : SymmetricMonoidalFunctor C D} →
          U.MonoidalNaturalTransformation (MF F) (MF G) → F ⇛ G
    ⌈ α ⌉ = record { U = U ; isMonoidal = isMonoidal }
      where open U.MonoidalNaturalTransformation α

    -- Identity and compositions

    infixr 9 _∘ᵥ_

    id : {F : SymmetricMonoidalFunctor C D} → F ⇛ F
    id = ⌈ U.id ⌉

    _∘ᵥ_ : {F G H : SymmetricMonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
    α ∘ᵥ β   = ⌈ ⌊ α ⌋ U.∘ᵥ ⌊ β ⌋ ⌉

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {E : SymmetricMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_

    _∘ₕ_ : {F G : SymmetricMonoidalFunctor C D}
           {H I : SymmetricMonoidalFunctor D E} →
           H ⇛ I → F ⇛ G → (H ∘Fˡ F) ⇛ (I ∘Fˡ G)
    α ∘ₕ β = ⌈ ⌊ α ⌋ U.∘ₕ ⌊ β ⌋ ⌉

    _∘ˡ_ : {F G : SymmetricMonoidalFunctor C D}
           (H : SymmetricMonoidalFunctor D E) → F ⇛ G → (H ∘Fˡ F) ⇛ (H ∘Fˡ G)
    H ∘ˡ α = id {F = H} ∘ₕ α

    _∘ʳ_ : {G H : SymmetricMonoidalFunctor D E} →
           G ⇛ H → (F : SymmetricMonoidalFunctor C D) → (G ∘Fˡ F) ⇛ (H ∘Fˡ F)
    α ∘ʳ F = α ∘ₕ id {F = F}

module Strong where
  open BMF.Strong using (SymmetricMonoidalFunctor)
  open MNT.Strong using (IsMonoidalNaturalTransformation)
  open SymmetricMonoidalFunctor using () renaming
    ( F                         to UF
    ; monoidalFunctor           to MF
    ; laxSymmetricMonoidalFunctor to laxBMF
    )

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Monoidal natural transformations between symmetric strong
    -- monoidal functors.

    record SymmetricMonoidalNaturalTransformation
           (F G : SymmetricMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where

      field
        U          : NaturalTransformation (UF F) (UF G)
        isMonoidal : IsMonoidalNaturalTransformation (MF F) (MF G) U

      laxBNT : Lax.SymmetricMonoidalNaturalTransformation (laxBMF F) (laxBMF G)
      laxBNT = record { U = U ; isMonoidal = isMonoidal }
      open Lax.SymmetricMonoidalNaturalTransformation laxBNT public
        hiding (U; isMonoidal)

  -- To shorten some definitions

  private
    _⇛_ = SymmetricMonoidalNaturalTransformation
    module U = MNT.Strong

  module _ {o ℓ e o′ ℓ′ e′}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

    -- Conversions

    ⌊_⌋ : {F G : SymmetricMonoidalFunctor C D} →
          F ⇛ G → U.MonoidalNaturalTransformation (MF F) (MF G)
    ⌊ α ⌋ = record { U = U ; isMonoidal = isMonoidal }
      where open SymmetricMonoidalNaturalTransformation α

    ⌈_⌉ : {F G : SymmetricMonoidalFunctor C D} →
          U.MonoidalNaturalTransformation (MF F) (MF G) → F ⇛ G
    ⌈ α ⌉ = record { U = U ; isMonoidal = isMonoidal }
      where open U.MonoidalNaturalTransformation α

    -- Identity and compositions

    infixr 9 _∘ᵥ_

    id : {F : SymmetricMonoidalFunctor C D} → F ⇛ F
    id = ⌈ U.id ⌉

    _∘ᵥ_ : {F G H : SymmetricMonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
    α ∘ᵥ β   = ⌈ ⌊ α ⌋ U.∘ᵥ ⌊ β ⌋ ⌉

  module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
           {C : SymmetricMonoidalCategory o ℓ e}
           {D : SymmetricMonoidalCategory o′ ℓ′ e′}
           {E : SymmetricMonoidalCategory o″ ℓ″ e″} where

    infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_

    _∘ₕ_ : {F G : SymmetricMonoidalFunctor C D}
           {H I : SymmetricMonoidalFunctor D E} →
           H ⇛ I → F ⇛ G → (H ∘Fˢ F) ⇛ (I ∘Fˢ G)
    -- NOTE: this definition is clearly equivalent to
    --
    --   α ∘ₕ β = ⌈ ⌊ α ⌋ U.∘ₕ ⌊ β ⌋ ⌉
    --
    -- but the latter takes an unreasonably long time to typecheck,
    -- while the unfolded version typechecks almost immediately.
    α ∘ₕ β = record
      { U               = C.U
      ; isMonoidal      = record
        { ε-compat      = C.ε-compat
        ; ⊗-homo-compat = C.⊗-homo-compat
        }
      }
      where module C = U.MonoidalNaturalTransformation (⌊ α ⌋ U.∘ₕ ⌊ β ⌋)

    _∘ˡ_ : {F G : SymmetricMonoidalFunctor C D}
           (H : SymmetricMonoidalFunctor D E) → F ⇛ G → (H ∘Fˢ F) ⇛ (H ∘Fˢ G)
    H ∘ˡ α = id {F = H} ∘ₕ α

    _∘ʳ_ : {G H : SymmetricMonoidalFunctor D E} →
           G ⇛ H → (F : SymmetricMonoidalFunctor C D) → (G ∘Fˢ F) ⇛ (H ∘Fˢ F)
    α ∘ʳ F = α ∘ₕ id {F = F}

max_stars_repo_name: sstucki/agda-categories

max_issues_repo_name: sstucki/agda-categories

max_forks_repo_name: sstucki/agda-categories


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

module Properties.DecSubtyping where

open import Agda.Builtin.Equality using (_≡_; refl)
open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; scalar-scalar; function-scalar; function-ok; function-ok₁; function-ok₂; function-err; function-tgt; left; right; _,_)
open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
open import Luau.TypeSaturation using (saturate)
open import Properties.Contradiction using (CONTRADICTION; ¬)
open import Properties.Functions using (_∘_)
open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; fun-top; fun-function; fun-¬scalar)
open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_)
open import Properties.Equality using (_≢_)

-- Honest this terminates, since saturation maintains the depth of nested arrows
{-# TERMINATING #-}
dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
dec-subtypingˢᶠ : ∀ {F G} → FunType F → Saturated F → FunType G → Either (F ≮: G) (F <:ᵒ G)
dec-subtypingᶠ : ∀ {F G} → FunType F → FunType G → Either (F ≮: G) (F <: G)
dec-subtypingᶠⁿ : ∀ {F U} → FunType F → Normal U → Either (F ≮: U) (F <: U)
dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)

dec-subtypingˢⁿ T U with dec-language _ (scalar T)
dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)

dec-subtypingˢᶠ {F} {S ⇒ T} Fᶠ (defn sat-∩ sat-∪) (Sⁿ ⇒ Tⁿ) = result (top Fᶠ (λ o → o)) where

  data Top G : Set where

    defn : ∀ Sᵗ Tᵗ →

      Overloads F (Sᵗ ⇒ Tᵗ) →
      (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
      -------------
      Top G

  top : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Top G
  top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
  top (Gᶠ ∩ Hᶠ) G⊆F with top Gᶠ (G⊆F ∘ left) | top Hᶠ (G⊆F ∘ right)
  top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ with sat-∪ p q
  top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ | defn n r r₁ = defn _ _ n
    (λ { (left o) → <:-trans (<:-trans (p₁ o) <:-∪-left) r ; (right o) → <:-trans (<:-trans (q₁ o) <:-∪-right) r })

  result : Top F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
  result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ oᵗ)
  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness s Ss ¬Sᵗs) = Left (witness (function-err s) (ov-language Fᶠ (λ o → function-err (<:-impl-⊇ (srcᵗ o) s ¬Sᵗs))) (function-err Ss))
  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where

    data LargestSrc (G : Type) : Set where

      yes : ∀ S₀ T₀ →

        Overloads F (S₀ ⇒ T₀) →
        T₀ <: T →
        (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
        -----------------------
        LargestSrc G

      no : ∀ S₀ T₀ →

        Overloads F (S₀ ⇒ T₀) →
        T₀ ≮: T →
        (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T₀ <: T′) →
        -----------------------
        LargestSrc G

    largest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → LargestSrc G
    largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F with dec-subtypingⁿ  T′ⁿ Tⁿ
    largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Left T′≮:T = no S′ T′ (G⊆F here) T′≮:T λ { here → <:-refl }
    largest {S′ ⇒ T′} (S′ⁿ ⇒ T′ⁿ) G⊆F | Right T′<:T = yes S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl })
    largest (Gᶠ ∩ Hᶠ) GH⊆F with largest Gᶠ (GH⊆F ∘ left) | largest Hᶠ (GH⊆F ∘ right)
    largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ with sat-∩ o₁ o₂
    largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt with dec-subtypingⁿ (normal-overload-tgt Fᶠ o) Tⁿ
    largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Left T₀≮:T = no _ _ o T₀≮:T (λ { (left o) → <:-trans tgt (<:-trans <:-∩-left (tgt₁ o)) ; (right o) → <:-trans tgt (<:-trans <:-∩-right (tgt₂ o)) })
    largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ | defn o src tgt | Right T₀<:T = yes _ _ o T₀<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
    largest (Gᶠ ∩ Hᶠ) GH⊆F | no S₁ T₁ o₁ T₁≮:T tgt₁ | yes S₂ T₂ o₂ T₂<:T src₂ = yes S₂ T₂ o₂ T₂<:T (λ { (left o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₁ o) T₁≮:T)) ; (right o) p → src₂ o p })
    largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | no S₂ T₂ o₂ T₂≮:T tgt₂ = yes S₁ T₁ o₁ T₁<:T (λ { (left o) p → src₁ o p ; (right o) p → CONTRADICTION (<:-impl-¬≮: p (<:-trans-≮: (tgt₂ o) T₂≮:T)) })
    largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ with sat-∪ o₁ o₂
    largest (Gᶠ ∩ Hᶠ) GH⊆F | yes S₁ T₁ o₁ T₁<:T src₁ | yes S₂ T₂ o₂ T₂<:T src₂ | defn o src tgt = yes _ _ o (<:-trans tgt (<:-∪-lub T₁<:T T₂<:T))
      (λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src)
         ; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src)
         })

    result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
    result₀ (no S₀ T₀ o₀ (witness t T₀t ¬Tt) tgt₀) = Left (witness (function-tgt t) (ov-language Fᶠ (λ o → function-tgt (tgt₀ o t T₀t))) (function-tgt ¬Tt))
    result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtypingⁿ Sⁿ (normal-overload-src Fᶠ o₀)
    result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right λ { here → defn o₀ S<:S₀ T₀<:T }
    result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where

      data SmallestTgt (G : Type) : Set where

        defn : ∀ S₁ T₁ →

          Overloads F (S₁ ⇒ T₁) →
          Language S₁ s →
          (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
          -----------------------
          SmallestTgt G

      smallest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → SmallestTgt G
      smallest {S′ ⇒ T′} _ G⊆F with dec-language S′ s
      smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) }
      smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl })
      smallest (Gᶠ ∩ Hᶠ) GH⊆F with smallest Gᶠ (GH⊆F ∘ left) | smallest Hᶠ (GH⊆F ∘ right)
      smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ with sat-∩ o₁ o₂
      smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ | defn o src tgt = defn _ _ o (src s (R₁s , R₂s))
        (λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s)
           ; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)
           })

      result₁ : SmallestTgt F → (F ≮: (S ⇒ T))
      result₁ (defn S₁ T₁ o₁ S₁s tgt₁) with dec-subtypingⁿ (normal-overload-tgt Fᶠ o₁) Tⁿ
      result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp s ¬S₀s (src₀ o₁ T₁<:T s S₁s))
      result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness t T₁t ¬Tt) = witness (function-ok s t) (ov-language Fᶠ lemma) (function-ok Ss ¬Tt) where

        lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
        lemma {S′} o with dec-language S′ s
        lemma {S′} o | Left ¬S′s = function-ok₁ ¬S′s
        lemma {S′} o | Right S′s = function-ok₂ (tgt₁ o S′s t T₁t)

dec-subtypingˢᶠ F Fˢ (G ∩ H) with dec-subtypingˢᶠ F Fˢ G | dec-subtypingˢᶠ F Fˢ H
dec-subtypingˢᶠ F Fˢ (G ∩ H) | Left F≮:G | _ = Left (≮:-∩-left F≮:G)
dec-subtypingˢᶠ F Fˢ (G ∩ H) | _ | Left F≮:H = Left (≮:-∩-right F≮:H)
dec-subtypingˢᶠ F Fˢ (G ∩ H) | Right F<:G | Right F<:H = Right (λ { (left o) → F<:G o ; (right o) → F<:H o })

dec-subtypingᶠ F G with dec-subtypingˢᶠ (normal-saturate F) (saturated F) G
dec-subtypingᶠ F G | Left H≮:G = Left (<:-trans-≮: (saturate-<: F) H≮:G)
dec-subtypingᶠ F G | Right H<:G = Right (<:-trans (<:-saturate F) (<:ᵒ-impl-<: (normal-saturate F) G H<:G))

dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
dec-subtypingᶠⁿ T unknown = Right <:-unknown
dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , fun-¬scalar V T p))
dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)

dec-subtypingⁿ never U = Right <:-never
dec-subtypingⁿ unknown unknown = Right <:-refl
dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)

dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U)
dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))
dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U)))

-- As a corollary, for saturated functions
-- <:ᵒ coincides with <:, that is F is a subtype of (S ⇒ T) precisely
-- when one of its overloads is.

<:-impl-<:ᵒ : ∀ {F G} → FunType F → Saturated F → FunType G → (F <: G) → (F <:ᵒ G)
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G with dec-subtypingˢᶠ Fᶠ Fˢ Gᶠ
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G | Left F≮:G = CONTRADICTION (<:-impl-¬≮: F<:G F≮:G)
<:-impl-<:ᵒ {F} {G} Fᶠ Fˢ Gᶠ F<:G | Right F<:ᵒG = F<:ᵒG

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


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

open import HoTT

module homotopy.JoinFunc where

 module F {i j k l}  {A : Type i} {B : Type j} {C : Type k} {D : Type l} (f : A → C) (g : B → D) where

   fg-glue : (ab : A × B) → left (f (fst ab)) == right (g (snd ab)) :> (C * D)
   fg-glue (a , b) = glue (f a , g b)

   to : A * B → C * D
   to = To.f  module M where

     module To = PushoutRec (left ∘ f) (right ∘ g) fg-glue

   open M public

 module _  {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l} where
  _**_[_] : (A → C) → (B → D) → A * B → C * D
  f ** g [ ab ] = M.to ab where
                module M = F f g

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: UlrikBuchholtz/HoTT-Agda

max_forks_repo_name: UlrikBuchholtz/HoTT-Agda


text:
module Function.Multi where

open import Data
open import Data.Tuple
open import Data.Tuple.Raise
open import Data.Tuple.RaiseTypeᵣ
open import Functional
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Numeral.Natural
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable n : ℕ

infixr 0 _⇉_

-- The type of a multivariate function (nested by repeated application of (_→_)) of different types and levels constructed by a tuple list of types.
-- This is useful when one needs a function of arbitrary length or by arbitrary argument types.
-- Essentially:
--   ((A,B,C,D,..) ⇉ R)
--   = (A → (B → (C → (D → (.. → R)))))
--   = (A → B → C → D → .. → R)
-- Example:
--   open import Syntax.Number
--   f : (Unit{0} , Unit{1} , Unit{2}) ⇉ Unit{3}
--   f <> <> <> = <>
_⇉_ : ∀{ℓ𝓈 : Lvl.Level ^ n} → Types(ℓ𝓈) → Type{ℓ} → Type{ℓ Lvl.⊔ (Lvl.⨆ ℓ𝓈)}
_⇉_ {n = 0}       _        B = B
_⇉_ {n = 1}       A        B = A → B
_⇉_ {n = 𝐒(𝐒(n))} (A , As) B = A → (As ⇉ B)
-- TODO: Does it work with Functional.swap(foldᵣ(_→ᶠ_)) ?

_⇉ᵢₘₚₗ_ : ∀{ℓ𝓈 : Lvl.Level ^ n} → Types(ℓ𝓈) → Type{ℓ} → Type{ℓ Lvl.⊔ (Lvl.⨆ ℓ𝓈)}
_⇉ᵢₘₚₗ_ {n = 0}       _        B = B
_⇉ᵢₘₚₗ_ {n = 1}       A        B = {A} → B
_⇉ᵢₘₚₗ_ {n = 𝐒(𝐒(n))} (A , As) B = {A} → (As ⇉ᵢₘₚₗ B)

_⇉ᵢₙₛₜ_ : ∀{ℓ𝓈 : Lvl.Level ^ n} → Types(ℓ𝓈) → Type{ℓ} → Type{ℓ Lvl.⊔ (Lvl.⨆ ℓ𝓈)}
_⇉ᵢₙₛₜ_ {n = 0}       _        B = B
_⇉ᵢₙₛₜ_ {n = 1}       A        B = ⦃ A ⦄ → B
_⇉ᵢₙₛₜ_ {n = 𝐒(𝐒(n))} (A , As) B = ⦃ A ⦄ → (As ⇉ᵢₙₛₜ B)

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:
------------------------------------------------------------------------------
-- Equivalence of definitions of total lists
------------------------------------------------------------------------------

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

module LFPs.List where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
module LFP where

  -- List is a least fixed-point of a functor

  -- The functor.
  ListF : (D → Set) → D → Set
  ListF A xs = xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')

  -- List is the least fixed-point of ListF. i.e.
  postulate
    List : D → Set

    -- List is a pre-fixed point of ListF, i.e.
    --
    -- ListF List ≤ List.
    --
    -- Peter: It corresponds to the introduction rules.
    List-in : ∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ List xs') →
              List xs

    -- The higher-order version.
    List-in-ho : {xs : D} → ListF List xs → List xs

    -- List is the least pre-fixed point of ListF, i.e.
    --
    -- ∀ A. ListF A ≤ A ⇒ List ≤ A.
    --
    -- Peter: It corresponds to the elimination rule of an inductively
    -- defined predicate.
    List-ind :
      (A : D → Set) →
      (∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs') → A xs) →
      ∀ {xs} → List xs → A xs

    -- Higher-order version.
    List-ind-ho :
      (A : D → Set) →
      (∀ {xs} → ListF A xs → A xs) →
      ∀ {xs} → List xs → A xs

  ----------------------------------------------------------------------------
  -- List-in and List-in-ho are equivalents

  List-in-fo : ∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ List xs') →
               List xs
  List-in-fo = List-in-ho

  List-in-ho' : {xs : D} → ListF List xs → List xs
  List-in-ho' = List-in-ho

  ----------------------------------------------------------------------------
  -- List-ind and List-ind-ho are equivalents

  List-ind-fo :
    (A : D → Set) →
    (∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs') → A xs) →
    ∀ {xs} → List xs → A xs
  List-ind-fo = List-ind-ho

  List-ind-ho' :
    (A : D → Set) →
    (∀ {xs} → ListF A xs → A xs) →
    ∀ {xs} → List xs → A xs
  List-ind-ho' = List-ind

  ----------------------------------------------------------------------------
  -- The data constructors of List.
  lnil : List []
  lnil = List-in (inj₁ refl)

  lcons : ∀ x {xs} → List xs → List (x ∷ xs)
  lcons x {xs} Lxs = List-in (inj₂ (x , xs , refl , Lxs))

  ----------------------------------------------------------------------------
  -- The type theoretical induction principle for List.
  List-ind' : (A : D → Set) →
              A [] →
              (∀ x {xs} → A xs → A (x ∷ xs)) →
              ∀ {xs} → List xs → A xs
  List-ind' A A[] is = List-ind A prf
    where
    prf : ∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs') → A xs
    prf (inj₁ xs≡[])                  = subst A (sym xs≡[]) A[]
    prf (inj₂ (x' , xs' , h₁ , Axs')) = subst A (sym h₁) (is x' Axs')

  ----------------------------------------------------------------------------
  -- Example

  xs : D
  xs = 0' ∷ true ∷ 1' ∷ false ∷ []

  xs-List : List xs
  xs-List = lcons 0' (lcons true (lcons 1' (lcons false lnil)))

------------------------------------------------------------------------------
module Data where

  data List : D → Set where
    lnil  : List []
    lcons : ∀ x {xs} → List xs → List (x ∷ xs)

  -- Induction principle.
  List-ind : (A : D → Set) →
             A [] →
             (∀ x {xs} → A xs → A (x ∷ xs)) →
             ∀ {xs} → List xs → A xs
  List-ind A A[] h lnil          = A[]
  List-ind A A[] h (lcons x Lxs) = h x (List-ind A A[] h Lxs)

  ----------------------------------------------------------------------------
  -- List-in

  List-in : ∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ List xs') →
            List xs
  List-in {xs} h = case prf₁ prf₂ h
    where
    prf₁ : xs ≡ [] → List xs
    prf₁ xs≡[] = subst List (sym xs≡[]) lnil

    prf₂ : ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ List xs' → List xs
    prf₂ (x' , xs' , prf , Lxs') =  subst List (sym prf) (lcons x' Lxs')

  ----------------------------------------------------------------------------
  -- The fixed-point induction principle for List.

  List-ind' :
    (A : D → Set) →
    (∀ {xs} → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs') → A xs) →
    ∀ {xs} → List xs → A xs
  List-ind' A h Lxs = List-ind A h₁ h₂ Lxs
    where
    h₁ : A []
    h₁ = h (inj₁ refl)

    h₂ : ∀ y {ys} → A ys → A (y ∷ ys)
    h₂ y {ys} Ays = h (inj₂ (y , ys , refl , Ays))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-

https://github.com/mietek/lamport-timestamps

An Agda formalisation of Lamport timestamps.

Made by Miëtek Bak.  Published under the MIT X11 license.

-}

module Everything where

import Prelude

-- Processes, clocks, timestamps, messages, and events are defined as abstract interfaces.

import AbstractInterfaces
import BasicConcreteImplementations

-- Lamport’s clock condition yields a strict total order on events across all processes.

import OrdersAndEqualities

max_stars_repo_name: mietek/lamport-timestamps

max_issues_repo_name: mietek/lamport-timestamps

max_forks_repo_name: mietek/lamport-timestamps


text:
------------------------------------------------------------------------
-- A language of parser equivalence proofs
------------------------------------------------------------------------

-- This module defines yet another set of equivalence relations and
-- preorders for parsers. For symmetric kinds these relations are
-- equalities (compatible equivalence relations) by construction, and
-- they are sound and complete with respect to the previously defined
-- equivalences (see TotalParserCombinators.Congruence.Sound for the
-- soundness proof). This means that parser and language equivalence
-- are also equalities. The related orderings are compatible
-- preorders.

module TotalParserCombinators.Congruence where

open import Codata.Musical.Notation
open import Data.List
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat hiding (_^_)
open import Data.Product
open import Data.Vec.Recursive
open import Function
open import Function.Related using (Symmetric-kind; ⌊_⌋)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.CoinductiveEquality as CE
  using (_∼[_]c_; _∷_)
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics
  hiding ([_-_]_⊛_; [_-_]_>>=_)

infixl 50 [_-_]_⊛_ [_-_-_-_]_⊛_ _<$>_
infix  10 [_-_]_>>=_ [_-_-_-_]_>>=_
infixl  5 _∣_
infix   5 _∷_
infix   4 _∼[_]P_ ∞⟨_⟩_∼[_]P_ _≅P_ _≈P_
infix   3 _∎
infixr  2 _∼⟨_⟩_ _≅⟨_⟩_

------------------------------------------------------------------------
-- Helper functions

flatten₁ : {A : Set} → Maybe (Maybe A ^ 2) → Maybe A
flatten₁ nothing        = nothing
flatten₁ (just (m , _)) = m

flatten₂ : {A : Set} → Maybe (Maybe A ^ 2) → Maybe A
flatten₂ nothing        = nothing
flatten₂ (just (_ , m)) = m

------------------------------------------------------------------------
-- Equivalence proof programs

mutual

  _≅P_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
  p₁ ≅P p₂ = p₁ ∼[ parser ]P p₂

  _≈P_ : ∀ {Tok R xs₁ xs₂} → Parser Tok R xs₁ → Parser Tok R xs₂ → Set₁
  p₁ ≈P p₂ = p₁ ∼[ language ]P p₂

  data _∼[_]P_ {Tok} :
         ∀ {R xs₁ xs₂} →
         Parser Tok R xs₁ → Kind → Parser Tok R xs₂ → Set₁ where

    -- This constructor, which corresponds to CE._∷_, ensures that the
    -- relation is complete.

    _∷_ : ∀ {k R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁}
            {p₂ : Parser Tok R xs₂}
          (xs₁≈xs₂ : xs₁ List-∼[ k ] xs₂)
          (Dp₁≈Dp₂ : ∀ t → ∞ (D t p₁ ∼[ k ]P D t p₂)) →
          p₁ ∼[ k ]P p₂

    -- Equational reasoning.

    _∎     : ∀ {k R xs} (p : Parser Tok R xs) → p ∼[ k ]P p

    _∼⟨_⟩_ : ∀ {k R xs₁ xs₂ xs₃}
               (p₁ : Parser Tok R xs₁)
               {p₂ : Parser Tok R xs₂}
               {p₃ : Parser Tok R xs₃}
             (p₁≈p₂ : p₁ ∼[ k ]P p₂) (p₂≈p₃ : p₂ ∼[ k ]P p₃) →
             p₁ ∼[ k ]P p₃

    _≅⟨_⟩_ : ∀ {k R xs₁ xs₂ xs₃}
               (p₁ : Parser Tok R xs₁)
               {p₂ : Parser Tok R xs₂}
               {p₃ : Parser Tok R xs₃}
             (p₁≅p₂ : p₁ ≅P p₂) (p₂≈p₃ : p₂ ∼[ k ]P p₃) →
             p₁ ∼[ k ]P p₃

    sym : ∀ {k : Symmetric-kind} {R xs₁ xs₂}
            {p₁ : Parser Tok R xs₁}
            {p₂ : Parser Tok R xs₂}
          (p₁≈p₂ : p₁ ∼[ ⌊ k ⌋ ]P p₂) → p₂ ∼[ ⌊ k ⌋ ]P p₁

    -- Congruences.

    return : ∀ {k R} {x₁ x₂ : R}
             (x₁≡x₂ : x₁ ≡ x₂) → return x₁ ∼[ k ]P return x₂

    fail : ∀ {k R} → fail {R = R} ∼[ k ]P fail {R = R}

    token : ∀ {k} → token ∼[ k ]P token

    _∣_ : ∀ {k R xs₁ xs₂ xs₃ xs₄}
            {p₁ : Parser Tok R xs₁}
            {p₂ : Parser Tok R xs₂}
            {p₃ : Parser Tok R xs₃}
            {p₄ : Parser Tok R xs₄}
          (p₁≈p₃ : p₁ ∼[ k ]P p₃) (p₂≈p₄ : p₂ ∼[ k ]P p₄) →
          p₁ ∣ p₂ ∼[ k ]P p₃ ∣ p₄

    _<$>_ : ∀ {k R₁ R₂} {f₁ f₂ : R₁ → R₂} {xs₁ xs₂}
              {p₁ : Parser Tok R₁ xs₁}
              {p₂ : Parser Tok R₁ xs₂}
            (f₁≗f₂ : f₁ ≗ f₂) (p₁≈p₂ : p₁ ∼[ k ]P p₂) →
            f₁ <$> p₁ ∼[ k ]P f₂ <$> p₂

    [_-_]_⊛_ :
      ∀ {k R₁ R₂} xs₁xs₂ fs₁fs₂ →
      let xs₁ = flatten₁ xs₁xs₂; xs₂ = flatten₂ xs₁xs₂
          fs₁ = flatten₁ fs₁fs₂; fs₂ = flatten₂ fs₁fs₂ in
        {p₁ : ∞⟨ xs₁ ⟩Parser Tok (R₁ → R₂) (flatten fs₁)}
        {p₂ : ∞⟨ fs₁ ⟩Parser Tok  R₁       (flatten xs₁)}
        {p₃ : ∞⟨ xs₂ ⟩Parser Tok (R₁ → R₂) (flatten fs₂)}
        {p₄ : ∞⟨ fs₂ ⟩Parser Tok  R₁       (flatten xs₂)}
      (p₁≈p₃ : ∞⟨ xs₁xs₂ ⟩ p₁ ∼[ k ]P p₃)
      (p₂≈p₄ : ∞⟨ fs₁fs₂ ⟩ p₂ ∼[ k ]P p₄) →
      p₁ ⊛ p₂ ∼[ k ]P p₃ ⊛ p₄

    [_-_]_>>=_ :
      ∀ {k R₁ R₂} (f₁f₂ : Maybe (Maybe (R₁ → List R₂) ^ 2)) xs₁xs₂ →
      let f₁  = flatten₁ f₁f₂;   f₂  = flatten₂ f₁f₂
          xs₁ = flatten₁ xs₁xs₂; xs₂ = flatten₂ xs₁xs₂ in
        {p₁ : ∞⟨ f₁ ⟩Parser Tok R₁ (flatten xs₁)}
        {p₂ : (x : R₁) → ∞⟨ xs₁ ⟩Parser Tok R₂ (apply f₁ x)}
        {p₃ : ∞⟨ f₂ ⟩Parser Tok R₁ (flatten xs₂)}
        {p₄ : (x : R₁) → ∞⟨ xs₂ ⟩Parser Tok R₂ (apply f₂ x)}
      (p₁≈p₃ : ∞⟨ f₁f₂ ⟩ p₁ ∼[ k ]P p₃)
      (p₂≈p₄ : ∀ x → ∞⟨ xs₁xs₂ ⟩ p₂ x ∼[ k ]P p₄ x) →
      p₁ >>= p₂ ∼[ k ]P p₃ >>= p₄

    nonempty : ∀ {k R xs₁ xs₂}
                 {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
               (p₁≈p₂ : p₁ ∼[ k ]P p₂) → nonempty p₁ ∼[ k ]P nonempty p₂

    cast : ∀ {k R xs₁ xs₂ xs₁′ xs₂′}
             {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
             {xs₁≈xs₁′ : xs₁ List-∼[ bag ] xs₁′}
             {xs₂≈xs₂′ : xs₂ List-∼[ bag ] xs₂′}
           (p₁≈p₂ : p₁ ∼[ k ]P p₂) →
           cast xs₁≈xs₁′ p₁ ∼[ k ]P cast xs₂≈xs₂′ p₂

  -- Certain proofs can be coinductive if both sides are delayed.

  ∞⟨_⟩_∼[_]P_ :
    ∀ {Tok R xs₁ xs₂} {A : Set} (m₁m₂ : Maybe (Maybe A ^ 2)) →
    ∞⟨ flatten₁ m₁m₂ ⟩Parser Tok R xs₁ → Kind →
    ∞⟨ flatten₂ m₁m₂ ⟩Parser Tok R xs₂ → Set₁
  ∞⟨ nothing ⟩ p₁ ∼[ k ]P p₂ = ∞ (♭  p₁ ∼[ k ]P ♭  p₂)
  ∞⟨ just _  ⟩ p₁ ∼[ k ]P p₂ =    ♭? p₁ ∼[ k ]P ♭? p₂

------------------------------------------------------------------------
-- Some derived combinators

[_-_-_-_]_⊛_ :
  ∀ {k Tok R₁ R₂} xs₁ xs₂ fs₁ fs₂
    {p₁ : ∞⟨ xs₁ ⟩Parser Tok (R₁ → R₂) (flatten fs₁)}
    {p₂ : ∞⟨ fs₁ ⟩Parser Tok  R₁       (flatten xs₁)}
    {p₃ : ∞⟨ xs₂ ⟩Parser Tok (R₁ → R₂) (flatten fs₂)}
    {p₄ : ∞⟨ fs₂ ⟩Parser Tok  R₁       (flatten xs₂)} →
  ♭? p₁ ∼[ k ]P ♭? p₃ → ♭? p₂ ∼[ k ]P ♭? p₄ → p₁ ⊛ p₂ ∼[ k ]P p₃ ⊛ p₄
[ xs₁ - xs₂ - fs₁ - fs₂ ] p₁≈p₃ ⊛ p₂≈p₄ =
  [ just (xs₁ , xs₂) - just (fs₁ , fs₂) ] p₁≈p₃ ⊛ p₂≈p₄

[_-_-_-_]_>>=_ :
  ∀ {k Tok R₁ R₂} (f₁ f₂ : Maybe (R₁ → List R₂)) xs₁ xs₂
    {p₁ : ∞⟨ f₁ ⟩Parser Tok R₁ (flatten xs₁)}
    {p₂ : (x : R₁) → ∞⟨ xs₁ ⟩Parser Tok R₂ (apply f₁ x)}
    {p₃ : ∞⟨ f₂ ⟩Parser Tok R₁ (flatten xs₂)}
    {p₄ : (x : R₁) → ∞⟨ xs₂ ⟩Parser Tok R₂ (apply f₂ x)} →
  ♭? p₁ ∼[ k ]P ♭? p₃ → (∀ x → ♭? (p₂ x) ∼[ k ]P ♭? (p₄ x)) →
  p₁ >>= p₂ ∼[ k ]P p₃ >>= p₄
[ f₁ - f₂ - xs₁ - xs₂ ] p₁≈p₃ >>= p₂≈p₄ =
  [ just (f₁ , f₂) - just (xs₁ , xs₂) ] p₁≈p₃ >>= p₂≈p₄

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

complete : ∀ {k Tok R xs₁ xs₂}
             {p₁ : Parser Tok R xs₁}
             {p₂ : Parser Tok R xs₂} →
           p₁ ∼[ k ] p₂ → p₁ ∼[ k ]P p₂
complete = complete′ ∘ CE.complete
  where
  complete′ : ∀ {k Tok R xs₁ xs₂}
                {p₁ : Parser Tok R xs₁}
                {p₂ : Parser Tok R xs₂} →
              p₁ ∼[ k ]c p₂ → p₁ ∼[ k ]P p₂
  complete′ (xs₁≈xs₂ ∷ Dp₁≈Dp₂) =
    xs₁≈xs₂ ∷ λ t → ♯ complete′ (♭ (Dp₁≈Dp₂ t))

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Logics.Or where

open import Function
open import Logics.And

------------------------------------------------------------------------
-- definitions

infixl 4 _∨_

data _∨_ (P Q : Set) : Set where
  ∨-intro₀ : P → P ∨ Q
  ∨-intro₁ : Q → P ∨ Q

------------------------------------------------------------------------
-- internal stuffs

private

  p→r+q→r+p∨q=r : ∀ {P Q n} {R : Set n} → (P → R) → (Q → R) → (P ∨ Q) → R
  p→r+q→r+p∨q=r pr _ (∨-intro₀ p) = pr p
  p→r+q→r+p∨q=r _ qr (∨-intro₁ q) = qr q

  ∨-comm′ : ∀ {P Q} → (P ∨ Q) → (Q ∨ P)
  ∨-comm′ (∨-intro₀ p) = ∨-intro₁ p
  ∨-comm′ (∨-intro₁ q) = ∨-intro₀ q

  ∨-assoc₀ : ∀ {P Q R} → ((P ∨ Q) ∨ R) → (P ∨ (Q ∨ R))
  ∨-assoc₀ (∨-intro₀ (∨-intro₀ x)) = ∨-intro₀ x
  ∨-assoc₀ (∨-intro₀ (∨-intro₁ x)) = ∨-intro₁ $ ∨-intro₀ x
  ∨-assoc₀ (∨-intro₁ x) = ∨-intro₁ $ ∨-intro₁ x

  ∨-assoc₁ : ∀ {P Q R} → (P ∨ (Q ∨ R)) → ((P ∨ Q) ∨ R)
  ∨-assoc₁ (∨-intro₀ x) = ∨-intro₀ $ ∨-intro₀ x
  ∨-assoc₁ (∨-intro₁ (∨-intro₀ x)) = ∨-intro₀ $ ∨-intro₁ x
  ∨-assoc₁ (∨-intro₁ (∨-intro₁ x)) = ∨-intro₁ x

  ∨-elim : ∀ {P Q n} {R : Set n} → (P → R) → (Q → R) → (P ∨ Q) → R
  ∨-elim = p→r+q→r+p∨q=r

  ∨-comm : ∀ {P Q} → (P ∨ Q) ⇔ (Q ∨ P)
  ∨-comm = ∧-intro ∨-comm′ ∨-comm′

  ∨-assoc : ∀ {P Q R} → (P ∨ (Q ∨ R)) ⇔ ((P ∨ Q) ∨ R)
  ∨-assoc = ∧-intro ∨-assoc₁ ∨-assoc₀

------------------------------------------------------------------------
-- public aliases

or-elim : ∀ {P Q n} {R : Set n} → (P → R) → (Q → R) → (P ∨ Q) → R
or-elim = ∨-elim

or-comm : ∀ {P Q} → (P ∨ Q) ⇔ (Q ∨ P)
or-comm = ∨-comm

or-assoc : ∀ {P Q R} → (P ∨ (Q ∨ R)) ⇔ ((P ∨ Q) ∨ R)
or-assoc = ∨-assoc


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.coherent where

open import sum
open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.core
open import function.isomorphism.core
open import function.overloading
open import overloading.core

coherent : ∀ {i j} {X : Set i}{Y : Set j} → X ≅ Y → Set _
coherent f = ∀ x → ap to (iso₁ x) ≡ iso₂ (to x)
  -- this definition says that the two possible proofs that
  --     to (from (to x)) ≡ to x
  -- are equal
  where
    open _≅_ f

coherent' : ∀ {i j} {X : Set i}{Y : Set j} → X ≅ Y → Set _
coherent' f = ∀ y → ap from (iso₂ y) ≡ iso₁ (from y)
  where
    open _≅_ f

-- coherent isomorphisms
_≅'_ : ∀ {i j} → (X : Set i)(Y : Set j) → Set _
X ≅' Y = Σ (X ≅ Y) coherent

instance
  iso'-is-fun : ∀ {i j}{X : Set i}{Y : Set j}
              → Coercion (X ≅' Y) (X → Y)
  iso'-is-fun = record
    { coerce = λ isom → apply (proj₁ isom) }

  iso'-is-iso : ∀ {i j}{X : Set i}{Y : Set j}
              → Coercion (X ≅' Y) (X ≅ Y)
  iso'-is-iso = record
    { coerce = proj₁ }

-- technical lemma: substiting a fixpoint proof into itself is like
-- applying the function
lem-subst-fixpoint : ∀ {i}{X : Set i}
                     (f : X → X)(x : X)
                     (p : f x ≡ x)
                   → subst (λ x → f x ≡ x) (sym p) p
                   ≡ ap f p
lem-subst-fixpoint {i}{X} f x p = begin
    subst (λ x → f x ≡ x) (p ⁻¹) p
  ≡⟨ lem (f x) (sym p) ⟩
    ap f (sym (sym p)) · p · sym p
  ≡⟨ ap (λ z → ap f z · p · sym p)
           (double-inverse p) ⟩
    ap f p · p · sym p
  ≡⟨ associativity (ap f p) p (sym p) ⟩
    ap f p · (p · sym p)
  ≡⟨ ap (λ z → ap f p · z) (left-inverse p) ⟩
    ap f p · refl
  ≡⟨ left-unit (ap f p) ⟩
    ap f p
  ∎
  where
    open ≡-Reasoning
    lem : (y : X) (q : x ≡ y)
        → subst (λ z → f z ≡ z) q p
        ≡ ap f (sym q) · p · q
    lem .x refl = sym (left-unit p)

lem-whiskering : ∀ {i} {X : Set i}
                 (f : X → X) (H : (x : X) → f x ≡ x)
                 (x : X) → ap f (H x) ≡ H (f x)
lem-whiskering f H x = begin
    ap f (H x)
  ≡⟨ sym (lem-subst-fixpoint f x (H x)) ⟩
    subst (λ z → f z ≡ z) (sym (H x)) (H x)
  ≡⟨ ap' H (sym (H x)) ⟩
    H (f x)
  ∎
  where
    open ≡-Reasoning

lem-homotopy-nat : ∀ {i j}{X : Set i}{Y : Set j}
                   {x x' : X}{f g : X → Y}
                   (H : (x : X) → f x ≡ g x) (p : x ≡ x')
                 → H x · ap g p ≡ ap f p · H x'
lem-homotopy-nat H refl = left-unit _

co-coherence : ∀ {i j}{X : Set i}{Y : Set j}
               (isom : X ≅ Y)
             → coherent isom
             → coherent' isom
co-coherence (iso f g H K) coherence y =
  subst (λ z → ap g (K z) ≡ H (g z)) (K y) lem
  where
    open ≡-Reasoning

    lem : ap g (K (f (g y)))
        ≡ H (g (f (g y)))
    lem = begin
        ap g (K (f (g y)))
      ≡⟨ ap (ap g) (sym (coherence (g y))) ⟩
        ap g (ap f (H (g y)))
      ≡⟨ ap-hom f g _ ⟩
        ap (g ∘ f) (H (g y))
      ≡⟨ lem-whiskering (g ∘ f) H (g y) ⟩
        H (g (f (g y)))
      ∎

sym≅' : ∀ {i j}{X : Set i}{Y : Set j}
      → X ≅' Y → Y ≅' X
sym≅' (isom , γ) = sym≅ isom , co-coherence isom γ

--- Vogt's lemma. See http://ncatlab.org/nlab/show/homotopy+equivalence
vogt-lemma : ∀ {i j}{X : Set i}{Y : Set j} → (isom : X ≅ Y)
           → let open _≅_ isom
              in Σ ((y : Y) → to (from y) ≡ y) λ iso' →
                 coherent (iso to from iso₁ iso')
vogt-lemma {X = X}{Y = Y} isom = K' , γ
  where
    open _≅_ isom
      renaming (to to f ; from to g ; iso₁ to H ; iso₂ to K)

    -- Outline of the proof
    -- --------------------
    --
    -- We want to find a homotopy K' : f g → id such that f K' ≡ H f.
    --
    -- To do so, we first prove that the following diagram of
    -- homotopies:
    --
    --                     f H g f
    --          f g f g f ---------> f g f
    --              |                  |
    --     f g K f  |                  | K f
    --              |                  |
    --              v                  v
    --            f g f -------------> f
    --                       f H
    --
    -- commutes. We then observe that f appears on the right side of
    -- every element in the diagram, except the bottom row, so if we
    -- define:
    --
    --     K' = (f g K) ⁻¹ · (f H g f) · (K f)
    --
    -- we get that K' f must be equal to the bottom row, which is
    -- exactly the required coherence condition.

    open ≡-Reasoning

    -- the diagram above commutes
    lem : (x : X)
        → ap f (H (g (f x))) · K (f x)
        ≡ ap (f ∘ g) (K (f x)) · ap f (H x)
    lem x = begin
        ap f (H (g (f x))) · K (f x)
      ≡⟨ ap (λ z → ap f z · K (f x))
              (sym (lem-whiskering (g ∘ f) H x)) ⟩
        ap f (ap (g ∘ f) (H x)) · K (f x)
      ≡⟨ ap (λ z → z · K (f x))
              (ap-hom (g ∘ f) f (H x)) ⟩
        ap (f ∘ g ∘ f) (H x) · K (f x)
      ≡⟨ sym (lem-homotopy-nat (λ x → K (f x)) (H x)) ⟩
        K (f (g (f x))) · ap f (H x)
      ≡⟨ ap (λ z → z · ap f (H x))
              (sym (lem-whiskering (f ∘ g) K (f x))) ⟩
        ap (f ∘ g) (K (f x)) · ap f (H x)
      ∎

    K' : (y : Y) → f (g y) ≡ y
    K' y = ap (f ∘ g) (sym (K y))
         · ap f (H (g y))
         · K y

    iso' = iso f g H K'

    -- now we can just compute using the groupoid laws
    γ : coherent iso'
    γ x = sym $ begin
        K' (f x)
      ≡⟨ refl ⟩
        ap (f ∘ g) (sym (K (f x))) ·
        ap f (H (g (f x))) · K (f x)
      ≡⟨ associativity (ap (f ∘ g) (sym (K (f x))))
               (ap f (H (g (f x))))
               (K (f x)) ⟩
        ap (f ∘ g) (sym (K (f x))) ·
        (ap f (H (g (f x))) · K (f x))
      ≡⟨ ap (λ z → ap (f ∘ g) (sym (K (f x))) · z) (lem x) ⟩
        ap (f ∘ g) (sym (K (f x))) ·
        (ap (f ∘ g) (K (f x)) · ap f (H x))
      ≡⟨ ap (λ z → z · (ap (f ∘ g) (K (f x)) · ap f (H x)))
              (ap-inv (f ∘ g) (K (f x))) ⟩
        sym (ap (f ∘ g) (K (f x))) ·
        (ap (f ∘ g) (K (f x)) · ap f (H x))
      ≡⟨ sym (associativity (sym (ap (f ∘ g) (K (f x))))
                       (ap (f ∘ g) (K (f x)))
                       (ap f (H x))) ⟩
        ( sym (ap (f ∘ g) (K (f x))) ·
          ap (f ∘ g) (K (f x)) ) ·
        ap f (H x)
      ≡⟨ ap (λ z → z · ap f (H x))
               (right-inverse (ap (f ∘ g) (K (f x)))) ⟩
        refl · ap f (H x)
      ≡⟨ right-unit (ap f (H x)) ⟩
        ap f (H x)
      ∎

≅⇒≅' : ∀ {i j} {X : Set i}{Y : Set j} → X ≅ Y → X ≅' Y
≅⇒≅' {X = X}{Y = Y} isom = iso to from iso₁ (proj₁ v) , proj₂ v
  where
    open _≅_ isom
    open import sum
    abstract
      v : Σ ((y : Y) → to (from y) ≡ y) λ iso₂'
        → coherent (iso to from iso₁ iso₂')
      v = vogt-lemma isom

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
open import Prelude

module Implicits.Improved.Stack.Expressiveness where

open import Coinduction
open import Data.Fin.Substitution
open import Implicits.Oliveira.Types
open import Implicits.Oliveira.Terms
open import Implicits.Oliveira.Contexts
open import Implicits.Oliveira.Substitutions
open import Implicits.Oliveira.Deterministic.Resolution as D
open import Implicits.Oliveira.Ambiguous.Resolution as A
open import Implicits.Improved.Stack.Resolution as F
open import Implicits.Improved.Infinite.Resolution as ∞

module Finite⊆Infinite where

  p : ∀ {ν} {a} {Δ : ICtx ν} {s} → Δ F.& s ⊢ᵣ a → Δ ∞.⊢ᵣ a
  p (r-simp a a↓τ) = r-simp a (lem a↓τ)
    where
      lem : ∀ {ν} {a τ r} {Δ : ICtx ν} {r∈Δ : r List.∈ Δ} {s : Stack Δ} →
            Δ F.& s , r∈Δ ⊢ a ↓ τ → Δ ∞.⊢ a ↓ τ
      lem (i-simp τ) = i-simp τ
      lem (i-iabs _ ⊢ᵣa b↓τ) = i-iabs (♯ (p ⊢ᵣa)) (lem b↓τ)
      lem (i-tabs b a[/b]↓τ) = i-tabs b (lem a[/b]↓τ)
  p (r-iabs x) = r-iabs (p x)
  p (r-tabs x) = r-tabs (p x)

module Finite⊆OliveiraAmbiguous where

  p : ∀ {ν} {a} {Δ : ICtx ν} {s} → Δ F.& s ⊢ᵣ a → Δ A.⊢ᵣ a
  p (r-simp a a↓τ) = lem a↓τ (r-ivar a)
    where
      lem : ∀ {ν} {a r τ} {Δ : ICtx ν} {r∈Δ : r List.∈ Δ} {s} →
            Δ F.& s , r∈Δ ⊢ a ↓ τ → Δ A.⊢ᵣ a → Δ A.⊢ᵣ simpl τ
      lem (i-simp τ) K⊢ᵣτ = K⊢ᵣτ
      lem (i-iabs _ ⊢ᵣa b↓τ) K⊢ᵣa⇒b = lem b↓τ (r-iapp K⊢ᵣa⇒b (p ⊢ᵣa))
      lem (i-tabs b a[/b]↓τ) K⊢ᵣ∀a = lem a[/b]↓τ (r-tapp b K⊢ᵣ∀a)
  p (r-iabs x) = r-iabs (p x)
  p (r-tabs x) = r-tabs (p x)

module OliveiraDeterministic⊆Finite where

  open FirstLemmas

  -- Oliveira's termination condition is part of the well-formdness of types
  -- So we assume here that ⊢term x holds for all types x
  p : ∀ {ν} {a : Type ν} {Δ : ICtx ν} s →
      (∀ {μ} (x : Type μ) → ⊢term x) → Δ D.⊢ᵣ a → Δ F.& s ⊢ᵣ a
  p s term (r-simp {ρ = r} x r↓a) =
    r-simp (proj₁ $ FirstLemmas.first⟶∈ x) (lem (proj₁ $ first⟶∈ x) s r↓a)
    where
      lem : ∀ {ν r'} {Δ : ICtx ν} (r∈Δ : r' List.∈ Δ) {a r} s → Δ D.⊢ r ↓ a → Δ F.& s , r∈Δ ⊢ r ↓ a
      lem r∈Δ s (i-simp a) = i-simp a
      lem r∈Δ s (i-iabs {ρ₁ = ρ₁} ⊢ᵣρ₁ ρ₂↓τ) =
        i-iabs (push< s r∈Δ {!!}) (p (s push ρ₁ for r∈Δ) term ⊢ᵣρ₁) (lem r∈Δ s ρ₂↓τ)
      lem r∈Δ s (i-tabs b x₁) = i-tabs b (lem r∈Δ s x₁)
  p s term (r-iabs ρ₁ {ρ₂ = ρ₂} x) = r-iabs (p (s prepend ρ₂) term x)
  p s term (r-tabs x) = r-tabs (p (stack-weaken s) term x)


text:
module PointedFrac where

open import Data.Sum
open import Data.Product

record ∙_ (A : Set) : Set where
  constructor ⇡
  field
    focus : A

open ∙_

-- Paths between values---identical to dynamic semantics?
data _⟷_ : {A B : Set} → ∙ A → ∙ B → Set1 where
  id : {A : Set} → (x : A) → (⇡ x) ⟷ (⇡ x)
  swap₊₁ : {A B : Set} → {x : A} → _⟷_ {A ⊎ B} {B ⊎ A} (⇡ (inj₁ x)) (⇡ (inj₂ x))
  swap₊₂ : {A B : Set} → {y : B} → _⟷_ {A ⊎ B} {B ⊎ A} (⇡ (inj₂ y)) (⇡ (inj₁ y))
  swap× : {A B : Set} → {x : A} → {y : B} → ⇡ (x , y) ⟷ ⇡ (y , x)
  -- ...and so on

-- shorter arrow for a shorter definition!
data _↔_ : Set → Set → Set1 where
  id : {A : Set} → A ↔ A
  swap₊ : {A B : Set} → (A ⊎ B) ↔ (B ⊎ A)
  swap× : {A B : Set} → (A × B) ↔ (B × A)

-- Theorem, equivalent to stepping: if c : A ↔ B and v : A, then there exists v' : B and c' : (∙ v) ⟷ (∙ v')
eval : {A B : Set} → (A ↔ B) → (v : A) → Σ[ v' ∈ B ] ((⇡ v) ⟷ (⇡ v'))
eval id v = v , id v
eval swap₊ (inj₁ x) = inj₂ x , swap₊₁
eval swap₊ (inj₂ y) = inj₁ y , swap₊₂
eval swap× (x , y) = (y , x) , swap×

-- Theorem, equivalent to backwards stepping:
-- if c : A ↔ B and v' : B, then there exists v : A and c' : (∙ v) ⟷ (∙ v')
evalB : {A B : Set} → (A ↔ B) → (v' : B) → Σ[ v ∈ A ] ((⇡ v) ⟷ (⇡ v'))
evalB id v = v , id v
evalB swap₊ (inj₁ x) = inj₂ x , swap₊₂
evalB swap₊ (inj₂ y) = inj₁ y , swap₊₁
evalB swap× (x , y) = (y , x) , swap×

-- if c : A ↔ B and v : A, then evalB c (eval c v) ⟷ v
right-inv : {A B : Set} → (c : A ↔ B) → (v : A) → ⇡ (proj₁ (evalB c (proj₁ (eval c v)))) ⟷ ⇡ v
right-inv id v = id v
right-inv swap₊ (inj₁ x) = id (inj₁ x)
right-inv swap₊ (inj₂ y) = id (inj₂ y)
right-inv swap× v = id v

-- left-inv should be just as easy.

-- we should also be able to make a statement about proj₂ associated with back-and-forth

-- and create a function that maps c to its inverse, and 'prove' eval c = evalB @ inverse c

-- "forget" the extra structure
↓ : {A B : Set} → {x : A} → {y : B} → (⇡ x) ⟷ (⇡ y) → A ↔ B
↓ {A} {.A} {x} (id .x) = id
↓ swap₊₁ = swap₊
↓ swap₊₂ = swap₊
↓ swap× = swap×

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual