text:
------------------------------------------------------------------------
-- Two eliminators for Delay-monad.Alternative.Delay (A / R)
------------------------------------------------------------------------

-- This module is largely based on (but perhaps not quite identical
-- to) the development underlying Theorem 1 in "Quotienting the Delay
-- Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

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

module Delay-monad.Alternative.Eliminators where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (↑)

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms.Univalence equality-with-paths
import Equivalence equality-with-J as Eq
open import Equivalence-relation equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
open import Quotient equality-with-paths
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Delay-monad.Alternative
open import Delay-monad.Alternative.Equivalence
open import Delay-monad.Alternative.Properties

------------------------------------------------------------------------
-- A map function

private

  module _ {a b} {A : Type a} {B : Type b} where

    -- A map function for Maybe.

    mapᴹ : (A → B) → Maybe A → Maybe B
    mapᴹ = ⊎-map id

    -- If mapᴹ f x does not have a value, then x does not have a
    -- value.

    mapᴹ-↑ : ∀ {f : A → B} x → mapᴹ f x ↑ → x ↑
    mapᴹ-↑ nothing  _  = refl
    mapᴹ-↑ (just _) ()

    -- The function mapᴹ f preserves LE.

    mapᴹ-LE : ∀ {f : A → B} {x y} →
              LE x y → LE (mapᴹ f x) (mapᴹ f y)
    mapᴹ-LE =
      ⊎-map (cong (mapᴹ _)) (Σ-map (cong (mapᴹ _)) (_∘ mapᴹ-↑ _))

    -- The function mapᴹ f ∘_ preserves Increasing.

    mapᴹ-Increasing : ∀ {f : A → B} {g} →
                      Increasing g → Increasing (mapᴹ f ∘ g)
    mapᴹ-Increasing = mapᴹ-LE ∘_

-- A map function for Delay.

map : ∀ {a b} {A : Type a} {B : Type b} →
      (A → B) → Delay A → Delay B
map f = Σ-map (mapᴹ f ∘_) mapᴹ-Increasing

------------------------------------------------------------------------
-- The first eliminator

private
  variable
    a r : Level
    A B : Type a
    R   : A → A → Type r
    f   : A → B

-- Some abstract redefinitions, intended to make the code type-check
-- faster.

private

  abstract

    ℕ→/-comm-to′ : (ℕ → A) / (ℕ →ᴾ R) → (ℕ → A / R)
    ℕ→/-comm-to′ = ℕ→/-comm-to

    ℕ→/-comm-to′-[] : ℕ→/-comm-to′ {R = R} [ f ] ≡ [_] ∘ f
    ℕ→/-comm-to′-[] = refl

  ℕ→/-comm′ :
    {A : Type a} {R : A → A → Type r} →
    Axiom-of-countable-choice (a ⊔ r) →
    Is-equivalence-relation R →
    (∀ {x y} → Is-proposition (R x y)) →
    (ℕ → A) / (ℕ →ᴾ R) ↔ (ℕ → A / R)
  ℕ→/-comm′ {A = A} {R} cc R-equiv R-prop = record
    { surjection = record
      { logical-equivalence = record
        { to   = ℕ→/-comm-to′
        ; from = from
        }
      ; right-inverse-of = to∘from
      }
    ; left-inverse-of = from∘to
    }
    where
    iso = ℕ→/-comm cc prop-ext R-equiv R-prop

    abstract

      from : (ℕ → A / R) → (ℕ → A) / (ℕ →ᴾ R)
      from = _↔_.from iso

      to∘from : ∀ f → ℕ→/-comm-to′ (from f) ≡ f
      to∘from = _↔_.right-inverse-of iso

      from∘to : ∀ f → from (ℕ→/-comm-to′ f) ≡ f
      from∘to = _↔_.left-inverse-of iso

  abstract

    Maybe/-comm′ : Maybe A / Maybeᴾ R ↔ Maybe (A / R)
    Maybe/-comm′ = Maybe/-comm

    Maybe/-comm′-[] :
      _↔_.to Maybe/-comm′ ∘ [_] ≡ ⊎-map id ([_] {R = R})
    Maybe/-comm′-[] = Maybe/-comm-[]

-- There is a function from (ℕ → Maybe A) / (ℕ →ᴾ Maybeᴾ R) to
-- Delay (A / R).

→Maybe/→ : (ℕ → Maybe A) / (ℕ →ᴾ Maybeᴾ R) → Delay (A / R)
→Maybe/→ f =
  _↠_.to →↠Delay-function (_↔_.to Maybe/-comm′ ∘ ℕ→/-comm-to′ f)

-- A "computation" rule for →Maybe/→.

→Maybe/→-[] :
  →Maybe/→ [ f ] ≡
  _↠_.to →↠Delay-function (_↔_.to (Maybe/-comm′ {R = R}) ∘ [_] ∘ f)
→Maybe/→-[] =
  cong (λ g → _↠_.to →↠Delay-function (_↔_.to Maybe/-comm′ ∘ g))
    ℕ→/-comm-to′-[]

-- The definitions below make use of some assumptions: countable
-- choice and a propositional equivalence relation R.

module _
  {a r} {A : Type a} {R : A → A → Type r}
  (cc : Axiom-of-countable-choice (a ⊔ r))
  (R-equiv : Is-equivalence-relation R)
  (R-prop : ∀ {x y} → Is-proposition (R x y))
  where

  private

    -- An abbreviation.

    ℕ→/-comm″ =
      ℕ→/-comm′ cc
        (Maybeᴾ-preserves-Is-equivalence-relation R-equiv)
        (λ {x} → Maybeᴾ-preserves-Is-proposition R-prop {x = x})

  -- →Maybe/→ has a right inverse.

  →Maybe/↠ :
    (ℕ → Maybe A) / (ℕ →ᴾ Maybeᴾ R) ↠ Delay (A / R)
  →Maybe/↠ =
    (ℕ → Maybe A) / (ℕ →ᴾ Maybeᴾ R)  ↔⟨ ℕ→/-comm″ ⟩
    (ℕ → Maybe A / Maybeᴾ R)         ↔⟨ ∀-cong ext (λ _ → Maybe/-comm′) ⟩
    (ℕ → Maybe (A / R))              ↝⟨ →↠Delay-function ⟩□
    Delay (A / R)                    □

  private

    to-→Maybe/↠ : _↠_.to →Maybe/↠ ≡ →Maybe/→
    to-→Maybe/↠ = refl

  -- On part of the domain of →Maybe/→ the right inverse is also a
  -- left inverse.

  →Maybe/↠-partial-left-inverse :
    (x : Delay A) →
    _↠_.from →Maybe/↠ (→Maybe/→ [ proj₁ x ]) ≡ [ proj₁ x ]
  →Maybe/↠-partial-left-inverse (f , inc) =
    _↠_.from →Maybe/↠ (→Maybe/→ [ f ])                                 ≡⟨ cong (_↠_.from →Maybe/↠) →Maybe/→-[] ⟩

    _↔_.from ℕ→/-comm″ (λ n →
      _↔_.from Maybe/-comm′ $
      _↠_.from →↠Delay-function
        (_↠_.to →↠Delay-function (_↔_.to Maybe/-comm′ ∘ [_] ∘ f))
        n)                                                             ≡⟨ cong (λ g → _↔_.from ℕ→/-comm″ λ n →
                                                                                _↔_.from Maybe/-comm′ (_↠_.from →↠Delay-function
                                                                                (_↠_.to →↠Delay-function (g ∘ f))
                                                                                n)) $
                                                                            Maybe/-comm′-[] ⟩
    _↔_.from ℕ→/-comm″ (λ n →
      _↔_.from Maybe/-comm′ $
      _↠_.from →↠Delay-function
        (_↠_.to →↠Delay-function (mapᴹ [_] ∘ f))
        n)                                                             ≡⟨⟩

    _↔_.from ℕ→/-comm″ (λ n →
      _↔_.from Maybe/-comm′ $
      _↠_.from →↠Delay-function
        (_↠_.to →↠Delay-function
           (_↠_.from →↠Delay-function (map [_] (f , inc))))
        n)                                                             ≡⟨ cong (λ x → _↔_.from ℕ→/-comm″ λ n →
                                                                                _↔_.from Maybe/-comm′ (_↠_.from →↠Delay-function x n)) $
                                                                            _↠_.right-inverse-of →↠Delay-function (map [_] (f , inc)) ⟩
    _↔_.from ℕ→/-comm″ (λ n →
      _↔_.from Maybe/-comm′ $
      _↠_.from →↠Delay-function (map [_] (f , inc)) n)                 ≡⟨⟩

    _↔_.from ℕ→/-comm″ (λ n → _↔_.from Maybe/-comm′ $ mapᴹ [_] (f n))  ≡⟨ cong (λ g → _↔_.from ℕ→/-comm″ λ n → _↔_.from Maybe/-comm′ (g (f n))) $
                                                                            sym Maybe/-comm′-[] ⟩
    _↔_.from ℕ→/-comm″ (λ n →
      _↔_.from Maybe/-comm′ (_↔_.to Maybe/-comm′ [ f n ]))             ≡⟨ cong (_↔_.from ℕ→/-comm″) (⟨ext⟩ λ n →
                                                                            _↔_.left-inverse-of Maybe/-comm′ [ f n ]) ⟩

    _↔_.from ℕ→/-comm″ (λ n → [ f n ])                                 ≡⟨ cong (_↔_.from ℕ→/-comm″) $ sym ℕ→/-comm-to′-[] ⟩

    _↔_.from ℕ→/-comm″ (ℕ→/-comm-to′ [ f ])                            ≡⟨ _↔_.left-inverse-of ℕ→/-comm″ [ f ] ⟩∎

    [ f ]                                                              ∎

  -- A quotient-like eliminator for Delay (A / R).

  Delay/-elim₁ :
    ∀ {p} (P : Delay (A / R) → Type p)
    (p-[] : (f : ℕ → Maybe A) → P (→Maybe/→ [ f ])) →
    (∀ {f g} (r : (ℕ →ᴾ Maybeᴾ R) f g) →
     subst P (cong →Maybe/→
                   ([]-respects-relation {x = f} {y = g} r))
             (p-[] f) ≡
     p-[] g) →
    (∀ x → Is-set (P x)) →
    ∀ x → P x
  Delay/-elim₁ = ↠-eliminator →Maybe/↠

  -- Simplification lemma for Delay/-elim₁.

  Delay/-elim₁-[] :
    ∀ {p} (P : Delay (A / R) → Type p)
    (p-[] : (f : ℕ → Maybe A) → P (→Maybe/→ [ f ]))
    (ok :
       ∀ {f g} (r : (ℕ →ᴾ Maybeᴾ R) f g) →
       subst P (cong →Maybe/→
                     ([]-respects-relation {x = f} {y = g} r))
               (p-[] f) ≡
       p-[] g)
    (P-set : ∀ x → Is-set (P x)) (x : Delay A) →
    Delay/-elim₁ P p-[] ok P-set (→Maybe/→ [ proj₁ x ]) ≡
    p-[] (proj₁ x)
  Delay/-elim₁-[] P p-[] ok P-set x =
    ↠-eliminator-[] →Maybe/↠ P p-[] ok P-set
      (_↠_.from →↠Delay-function x)
      (→Maybe/↠-partial-left-inverse x)

------------------------------------------------------------------------
-- The second eliminator

-- Pointwise lifting of binary relations to the delay monad.

Delayᴾ :
  ∀ {a r} {A : Type a} →
  (A → A → Type r) →
  Delay A → Delay A → Type r
Delayᴾ R = (ℕ →ᴾ Maybeᴾ R) on proj₁

module _
  {a r} {A : Type a} {R : A → A → Type r}
  where

  -- The function map ([_] {R = R}) respects Delayᴾ R.

  map-[]-cong :
    ∀ x y → Delayᴾ R x y → map ([_] {R = R}) x ≡ map [_] y
  map-[]-cong x y r =
    _↔_.to (equality-characterisation /-is-set)
      (⟨ext⟩ λ n → lemma (proj₁ x n) (proj₁ y n) (r n))
    where
    lemma : ∀ x y → Maybeᴾ R x y →
            mapᴹ [_] x ≡ mapᴹ [_] y
    lemma nothing  nothing  = const refl
    lemma (just x) (just y) = cong inj₂ ∘ []-respects-relation
    lemma nothing  (just y) ()
    lemma (just x) nothing  ()

  -- The function
  -- _↠_.from →↠Delay-function ∘ _↠_.to →↠Delay-function respects
  -- ℕ →ᴾ Maybeᴾ R.

  from-to-→↠Delay-function-cong :
    let open _↠_ →↠Delay-function in
    (f g : ℕ → Maybe A) →
    (ℕ →ᴾ Maybeᴾ R) f g →
    (ℕ →ᴾ Maybeᴾ R) (from (to f)) (from (to g))
  from-to-→↠Delay-function-cong f g r =
    helper f g r (f 0) (g 0) (r 0)
    where
    helper :
      ∀ f g → (ℕ →ᴾ Maybeᴾ R) f g →
      ∀ x y → Maybeᴾ R x y →
      (ℕ →ᴾ Maybeᴾ R)
        (proj₁ (Delay⇔Delay.from (Delay⇔Delay.To.to′ f x)))
        (proj₁ (Delay⇔Delay.from (Delay⇔Delay.To.to′ g y)))
    helper f g rs (just x) (just y) r n       = r
    helper f g rs nothing  nothing  r zero    = r
    helper f g rs nothing  nothing  r (suc n) =
      helper (f ∘ suc) (g ∘ suc) (rs ∘ suc) (f 1) (g 1) (rs 1) n

    helper _ _ _ (just _) nothing  ()
    helper _ _ _ nothing  (just _) ()

  -- A simplification lemma for →Maybe/→.

  →Maybe/→-[]′ :
    (f : ℕ → Maybe A) →
    →Maybe/→ [ f ] ≡
    map ([_] {R = R}) (_↠_.to →↠Delay-function f)
  →Maybe/→-[]′ f = _↔_.to (equality-characterisation /-is-set)
    (proj₁ (→Maybe/→ [ f ])                                           ≡⟨ cong proj₁ →Maybe/→-[] ⟩
     proj₁ (_↠_.to →↠Delay-function (_↔_.to Maybe/-comm′ ∘ [_] ∘ f))  ≡⟨ cong (λ g → proj₁ (_↠_.to →↠Delay-function (g ∘ f))) $ Maybe/-comm′-[] ⟩
     proj₁ (_↠_.to →↠Delay-function (mapᴹ [_] ∘ f))                   ≡⟨ ⟨ext⟩ (helper f (f 0)) ⟩
     mapᴹ [_] ∘ proj₁ (_↠_.to →↠Delay-function f)                     ≡⟨⟩
     proj₁ (map [_] (_↠_.to →↠Delay-function f))                      ∎)
    where
    helper :
       ∀ f x n →
       proj₁ (Delay⇔Delay.from
                (Delay⇔Delay.To.to′ (mapᴹ [_] ∘ f) (mapᴹ [_] x))) n ≡
       mapᴹ [_] (proj₁ (Delay⇔Delay.from (Delay⇔Delay.To.to′ f x)) n)
    helper f (just x) n       = refl
    helper f nothing  zero    = refl
    helper f nothing  (suc n) = helper (f ∘ suc) (f 1) n

-- The definitions below make use of some assumptions: countable
-- choice and a propositional equivalence relation R.

module _
  {a p r} {A : Type a} {R : A → A → Type r}
  (cc : Axiom-of-countable-choice (a ⊔ r))
  (R-equiv : Is-equivalence-relation R)
  (R-prop : ∀ {x y} → Is-proposition (R x y))
  (P : Delay (A / R) → Type p)
  (p-[] : (x : Delay A) → P (map [_] x))
  (ok : ∀ {x y} (r : Delayᴾ R x y) →
        subst P (map-[]-cong x y r) (p-[] x) ≡ p-[] y)
  (P-set : ∀ x → Is-set (P x))
  where

  private

    lemma₁ = sym ∘ →Maybe/→-[]′ {R = R}

    lemma₂ :
      ∀ {f g} r →
      subst P
        (cong →Maybe/→ ([]-respects-relation {x = f} {y = g} r))
        (subst P (lemma₁ f) (p-[] (_↠_.to →↠Delay-function f))) ≡
      subst P (lemma₁ g) (p-[] (_↠_.to →↠Delay-function g))
    lemma₂ {f} {g} r =
      let p  = p-[] (_↠_.to →↠Delay-function f)
          r′ = cong →Maybe/→ ([]-respects-relation {x = f} {y = g} r)
          r″ = trans (trans (lemma₁ f) r′) (sym (lemma₁ g))
      in
      subst P r′ (subst P (lemma₁ f) p)                               ≡⟨ subst-subst P (lemma₁ f) r′ p ⟩

      subst P (trans (lemma₁ f) r′) p                                 ≡⟨ cong (λ eq → subst P eq p) $
                                                                           sym $ trans-[trans-sym]- _ (lemma₁ g) ⟩
      subst P (trans r″ (lemma₁ g)) p                                 ≡⟨ sym $ subst-subst P
                                                                                (trans (trans (lemma₁ f) r′) (sym (lemma₁ g)))
                                                                                (lemma₁ g)
                                                                                p ⟩
      subst P (lemma₁ g) (subst P r″ p)                               ≡⟨ cong (λ eq → subst P (lemma₁ g) (subst P eq p)) $
                                                                           Delay-closure 0 /-is-set
                                                                             r″
                                                                             (map-[]-cong (_↠_.to →↠Delay-function f)
                                                                                (_↠_.to →↠Delay-function g)
                                                                                (from-to-→↠Delay-function-cong f g r)) ⟩
      subst P (lemma₁ g)
        (subst P (map-[]-cong (_↠_.to →↠Delay-function f)
                              (_↠_.to →↠Delay-function g)
                              (from-to-→↠Delay-function-cong f g r))
                 p)                                                   ≡⟨ cong (subst P (lemma₁ g)) (ok _) ⟩∎

      subst P (lemma₁ g) (p-[] (_↠_.to →↠Delay-function g))           ∎

  -- A second quotient-like eliminator for Delay (A / R).
  --
  -- This eliminator corresponds to Theorem 1 in "Quotienting the
  -- Delay Monad by Weak Bisimilarity" by Chapman, Uustalu and
  -- Veltri.

  Delay/-elim₂ : ∀ x → P x
  Delay/-elim₂ =
    Delay/-elim₁ cc R-equiv R-prop P
    (λ f → subst P (lemma₁ f) (p-[] (_↠_.to →↠Delay-function f)))
    lemma₂ P-set

  -- Simplification lemma for Delay/-elim₂.

  Delay/-elim₂-[] : ∀ x → Delay/-elim₂ (map [_] x) ≡ p-[] x
  Delay/-elim₂-[] x =
    Delay/-elim₁ cc R-equiv R-prop P
      (λ f → subst P (lemma₁ f) (p-[] (_↠_.to →↠Delay-function f)))
      lemma₂ P-set (map [_] x)                                           ≡⟨ sym $ dcong
                                                                                (Delay/-elim₁ cc R-equiv R-prop P
                                                                                (λ f → subst P (lemma₁ f)
                                                                                (p-[] (_↠_.to →↠Delay-function f)))
                                                                                lemma₂ P-set)
                                                                                lemma₃ ⟩
    subst P lemma₃
      (Delay/-elim₁ cc R-equiv R-prop P
         (λ f → subst P (lemma₁ f) (p-[] (_↠_.to →↠Delay-function f)))
         lemma₂ P-set (→Maybe/→ [ proj₁ x ]))                            ≡⟨ cong (subst P lemma₃) $
                                                                              Delay/-elim₁-[] cc R-equiv R-prop P _ lemma₂ P-set x ⟩
    subst P lemma₃
      (subst P (lemma₁ (proj₁ x))
         (p-[] (_↠_.to →↠Delay-function (proj₁ x))))                     ≡⟨ subst-subst P (lemma₁ (proj₁ x)) lemma₃ _ ⟩

    subst P (trans (lemma₁ (proj₁ x)) lemma₃)
      (p-[] (_↠_.to →↠Delay-function (proj₁ x)))                         ≡⟨ cong (λ p → subst P p (p-[] (_↠_.to →↠Delay-function (proj₁ x)))) $
                                                                              trans--[trans-sym]
                                                                                (lemma₁ (proj₁ x))
                                                                                (cong (map [_]) $ _↠_.right-inverse-of →↠Delay-function x) ⟩
    subst P (cong (map [_]) $ _↠_.right-inverse-of →↠Delay-function x)
      (p-[] (_↠_.to →↠Delay-function (proj₁ x)))                         ≡⟨ sym $ subst-∘ P (map [_]) (_↠_.right-inverse-of →↠Delay-function x) ⟩

    subst (P ∘ map [_]) (_↠_.right-inverse-of →↠Delay-function x)
      (p-[] (_↠_.to →↠Delay-function (proj₁ x)))                         ≡⟨ dcong p-[] (_↠_.right-inverse-of →↠Delay-function x) ⟩∎

    p-[] x                                                               ∎
    where
    lemma₃ =
      →Maybe/→ [ proj₁ x ]                         ≡⟨ sym $ lemma₁ (proj₁ x) ⟩
      map [_] (_↠_.to →↠Delay-function (proj₁ x))  ≡⟨ cong (map [_]) $ _↠_.right-inverse-of →↠Delay-function x ⟩∎
      map [_] x                                    ∎

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module test.Negation where

open import Type
open import Declarative
open import Builtin
open import Builtin.Constant.Type
open import Builtin.Constant.Term Ctx⋆ Kind * # _⊢⋆_ con size⋆

-- zerepoch/zerepoch-core/test/data/negation.plc

open import Declarative.StdLib.Bool

negate : ∀{Γ} → Γ ⊢ boolean ⇒ boolean
negate {Γ} = ƛ (if ·⋆ boolean · ` Z · false · true)

ext: agda

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text: module Structure.Logic where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Int.Base where

open import Cubical.Core.Everything

open import Cubical.Data.Nat

data Int : Type₀ where
  pos    : (n : ℕ) → Int
  negsuc : (n : ℕ) → Int

neg : (n : ℕ) → Int
neg zero = pos zero
neg (suc n) = negsuc n

sucInt : Int → Int
sucInt (pos n)          = pos (suc n)
sucInt (negsuc zero)    = pos zero
sucInt (negsuc (suc n)) = negsuc n

predInt : Int → Int
predInt (pos zero)    = negsuc zero
predInt (pos (suc n)) = pos n
predInt (negsuc n)    = negsuc (suc n)

-- Natural number and negative integer literals for Int

open import Cubical.Data.Nat.Literals public

instance
  fromNatInt : HasFromNat Int
  fromNatInt = record { Constraint = λ _ → Unit ; fromNat = λ n → pos n }

instance
  fromNegInt : HasFromNeg Int
  fromNegInt = record { Constraint = λ _ → Unit ; fromNeg = λ n → neg 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:
{-

This file proves the higher groupoid structure of types
for homogeneous and heterogeneous paths

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.GroupoidLaws where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level
    A : Type ℓ
    x y z w v : A

_⁻¹ : (x ≡ y) → (y ≡ x)
x≡y ⁻¹ = sym x≡y

infix 40 _⁻¹

-- homogeneous groupoid laws

symInvo : (p : x ≡ y) → p ≡ p ⁻¹ ⁻¹
symInvo p = refl

rUnit : (p : x ≡ y) → p ≡ p ∙ refl
rUnit p j i = compPath-filler p refl j i

-- The filler of left unit: lUnit-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∨ i)))
-- (refl i) (λ j → compPath-filler refl p i j)) (λ k i → (p (~ k ∧ i ))) (lUnit p)

lUnit-filler : {x y : A} (p : x ≡ y) → I → I → I → A
lUnit-filler {x = x} p j k i =
  hfill (λ j → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∨ j )
                  ; (k = i0) → p i
               -- ; (k = i1) → compPath-filler refl p j i
                  }) (inS (p (~ k ∧ i ))) j

lUnit : (p : x ≡ y) → p ≡ refl ∙ p
lUnit p j i = lUnit-filler p i1 j i

symRefl : refl {x = x} ≡ refl ⁻¹
symRefl i = refl

compPathRefl : refl {x = x} ≡ refl ∙ refl
compPathRefl = rUnit refl

-- The filler of right cancellation: rCancel-filler p =
-- PathP (λ i → PathP (λ j → PathP (λ k → A) x (p (~ j ∧ ~ i)))
-- (λ j → compPath-filler p (p ⁻¹) i j) (refl i)) (λ j i → (p (i ∧ ~ j))) (rCancel p)

rCancel-filler : ∀ {x y : A} (p : x ≡ y) → (k j i : I) → A
rCancel-filler {x = x} p k j i =
  hfill (λ k → λ { (i = i0) → x
                  ; (i = i1) → p (~ k ∧ ~ j)
               -- ; (j = i0) → compPath-filler p (p ⁻¹) k i
                  ; (j = i1) → x
                  }) (inS (p (i ∧ ~ j))) k

rCancel : (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
rCancel {x = x} p j i = rCancel-filler p i1 j i

rCancel-filler' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → (i j k : I) → A
rCancel-filler' {x = x} {y} p i j k =
  hfill
    (λ i → λ
      { (j = i1) → p (~ i ∧ k)
      ; (k = i0) → x
      ; (k = i1) → p (~ i)
      })
    (inS (p k))
    (~ i)

rCancel' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
rCancel' p j k = rCancel-filler' p i0 j k

lCancel : (p : x ≡ y) → p ⁻¹ ∙ p ≡ refl
lCancel p = rCancel (p ⁻¹)

assoc : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
  p ∙ q ∙ r ≡ (p ∙ q) ∙ r
assoc p q r k = (compPath-filler p q k) ∙ compPath-filler' q r (~ k)

-- heterogeneous groupoid laws

symInvoP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
     PathP (λ j → PathP (λ i → symInvo (λ i → A i) j i) x y) p (symP (symP p))
symInvoP p = refl

rUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → rUnit (λ i → A i) j i) x y) p (compPathP p refl)
rUnitP p j i = compPathP-filler p refl j i

lUnitP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
  PathP (λ j → PathP (λ i → lUnit (λ i → A i) j i) x y) p (compPathP refl p)
lUnitP {A = A} {x = x} p k i =
  comp (λ j → lUnit-filler (λ i → A i) j k i)
       (λ j → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∨ j )
                ; (k = i0) → p i
                }) (p (~ k ∧ i ))

rCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → rCancel (λ i → A i) j i) x x) (compPathP p (symP p)) refl
rCancelP {A = A} {x = x} p j i =
  comp (λ k → rCancel-filler (λ i → A i) k j i)
       (λ k → λ { (i = i0) → x
                ; (i = i1) → p (~ k ∧ ~ j)
                ; (j = i1) → x
                }) (p (i ∧ ~ j))

lCancelP : {A : I → Type ℓ} → {x : A i0} → {y : A i1} → (p : PathP A x y) →
   PathP (λ j → PathP (λ i → lCancel (λ i → A i) j i) y y) (compPathP (symP p) p) refl
lCancelP p = rCancelP (symP p)

assocP : {A : I → Type ℓ} {x : A i0} {y : A i1} {B_i1 : Type ℓ} {B : (A i1) ≡ B_i1} {z : B i1}
  {C_i1 : Type ℓ} {C : (B i1) ≡ C_i1} {w : C i1} (p : PathP A x y) (q : PathP (λ i → B i) y z) (r : PathP (λ i → C i) z w) →
  PathP (λ j → PathP (λ i → assoc (λ i → A i) B C j i) x w) (compPathP p (compPathP q r)) (compPathP (compPathP p q) r)
assocP {A = A} {B = B} {C = C} p q r k i =
    comp (\ j' → hfill  (λ j → λ {
                     (i = i0) → A i0
                   ; (i = i1) → compPath-filler' (λ i₁ → B i₁) (λ i₁ → C i₁) (~ k) j })
                     (inS (compPath-filler (λ i₁ → A i₁) (λ i₁ → B i₁) k i)) j')
     (λ j → λ
      { (i = i0) → p i0
      ; (i = i1) →
        comp (\ j' → hfill ((λ l → λ
            { (j = i0) → B k
            ; (j = i1) → C l
            ; (k = i1) → C (j ∧ l)
            })) (inS (B ( j ∨ k)) ) j')
          (λ l → λ
            { (j = i0) → q k
            ; (j = i1) → r l
            ; (k = i1) → r (j ∧ l)
            })
          (q (j ∨ k))
      })
    (compPathP-filler p q k i)

-- Loic's code below

-- some exchange law for doubleCompPath and refl

invSides-filler : {x y z : A} (p : x ≡ y) (q : x ≡ z) → Square p (sym q) q (sym p)
invSides-filler {x = x} p q i j =
  hcomp (λ k → λ { (i = i0) → p (k ∧ j)
                 ; (i = i1) → q (~ j ∧ k)
                 ; (j = i0) → q (i ∧ k)
                 ; (j = i1) → p (~ i ∧ k)})
        x

leftright : {ℓ : Level} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) →
            (refl ∙∙ p ∙∙ q) ≡ (p ∙∙ q ∙∙ refl)
leftright p q i j =
  hcomp (λ t → λ { (j = i0) → p (i ∧ (~ t))
                 ; (j = i1) → q (t ∨ i) })
        (invSides-filler q (sym p) (~ i) j)

-- equating doubleCompPath and a succession of two compPath

split-leftright : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (refl ∙∙ (p ∙∙ q ∙∙ refl) ∙∙ r)
split-leftright p q r j i =
  hcomp (λ t → λ { (i = i0) → p (~ j ∧ ~ t)
                 ; (i = i1) → r t })
        (doubleCompPath-filler p q refl j i)

split-leftright' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y) (r : y ≡ z) →
                  (p ∙∙ q ∙∙ r) ≡ (p ∙∙ (refl ∙∙ q ∙∙ r) ∙∙ refl)
split-leftright' p q r j i =
  hcomp (λ t → λ { (i = i0) → p (~ t)
                 ; (i = i1) → r (j ∨ t) })
        (doubleCompPath-filler refl q r j i)

doubleCompPath-elim : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                      (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ (p ∙ q) ∙ r
doubleCompPath-elim p q r = (split-leftright p q r) ∙ (λ i → (leftright p q (~ i)) ∙ r)

doubleCompPath-elim' : {ℓ : Level} {A : Type ℓ} {w x y z : A} (p : w ≡ x) (q : x ≡ y)
                       (r : y ≡ z) → (p ∙∙ q ∙∙ r) ≡ p ∙ (q ∙ r)
doubleCompPath-elim' p q r = (split-leftright' p q r) ∙ (sym (leftright p (q ∙ r)))

cong-∙ : ∀ {B : Type ℓ} (f : A → B) (p : x ≡ y) (q : y ≡ z)
         → cong f (p ∙ q) ≡ (cong f p) ∙ (cong f q)
cong-∙ f p q j i = hcomp (λ k → λ { (j = i0) → f (compPath-filler p q k i)
                                  ; (i = i0) → f (p i0)
                                  ; (i = i1) → f (q k) })
                         (f (p i))

cong-∙∙ : ∀ {B : Type ℓ} (f : A → B) (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
          → cong f (p ∙∙ q ∙∙ r) ≡ (cong f p) ∙∙ (cong f q) ∙∙ (cong f r)
cong-∙∙ f p q r j i = hcomp (λ k → λ { (j = i0) → f (doubleCompPath-filler p q r k i)
                                     ; (i = i0) → f (p (~ k))
                                     ; (i = i1) → f (r k) })
                            (f (q i))

hcomp-unique : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (hcomp u (outS u0) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
hcomp-unique {φ = φ} u u0 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))

lid-unique : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
               (h1 h2 : ∀ i → A [ (φ ∨ ~ i) ↦ (\ { (φ = i1) → u i 1=1; (i = i0) → outS u0}) ])
               → (outS (h1 i1) ≡ outS (h2 i1)) [ φ ↦ (\ { (φ = i1) → (\ i → u i1 1=1)}) ]
lid-unique {φ = φ} u u0 h1 h2 = inS (\ i → hcomp (\ k → \ { (φ = i1) → u k 1=1
                                                            ; (i = i0) → outS (h1 k)
                                                            ; (i = i1) → outS (h2 k) })
                                                   (outS u0))

transp-hcomp : ∀ {ℓ} (φ : I) {A' : Type ℓ}
                     (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A') ]) (let B = \ (i : I) → outS (A i))
                 → ∀ {ψ} (u : I → Partial ψ (B i0)) → (u0 : B i0 [ ψ ↦ u i0 ]) →
                 (transp (\ i → B i) φ (hcomp u (outS u0)) ≡ hcomp (\ i o → transp (\ i → B i) φ (u i o)) (transp (\ i → B i) φ (outS u0)))
                   [ ψ ↦ (\ { (ψ = i1) → (\ i → transp (\ i → B i) φ (u i1 1=1))}) ]
transp-hcomp φ A u u0 = inS (sym (outS (hcomp-unique
               ((\ i o → transp (\ i → B i) φ (u i o))) (inS (transp (\ i → B i) φ (outS u0)))
                 \ i → inS (transp (\ i → B i) φ (hfill u u0 i)))))
  where
    B = \ (i : I) → outS (A i)

hcomp-cong : ∀ {ℓ} {A : Type ℓ} {φ} → (u : I → Partial φ A) → (u0 : A [ φ ↦ u i0 ]) →
                                     (u' : I → Partial φ A) → (u0' : A [ φ ↦ u' i0 ]) →
             (ueq : ∀ i → PartialP φ (\ o → u i o ≡ u' i o)) → (outS u0 ≡ outS u0') [ φ ↦ (\ { (φ = i1) → ueq i0 1=1}) ]
             → (hcomp u (outS u0) ≡ hcomp u' (outS u0')) [ φ ↦ (\ { (φ = i1) → ueq i1 1=1 }) ]
hcomp-cong u u0 u' u0' ueq 0eq = inS (\ j → hcomp (\ i o → ueq i o j) (outS 0eq j))

congFunct-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {x y z : A} (f : A → B) (p : x ≡ y) (q : y ≡ z)
                → I → I → I → B
congFunct-filler {x = x} f p q i j z =
  hfill (λ k → λ { (i = i0) → f x
                  ; (i = i1) → f (q k)
                  ; (j = i0) → f (compPath-filler p q k i)})
        (inS (f (p i)))
        z

congFunct : ∀ {ℓ} {B : Type ℓ} (f : A → B) (p : x ≡ y) (q : y ≡ z) → cong f (p ∙ q) ≡ cong f p ∙ cong f q
congFunct f p q j i = congFunct-filler f p q i j i1

-- congFunct for dependent types
congFunct-dep : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y z : A} (f : (a : A) → B a) (p : x ≡ y) (q : y ≡ z)
         → PathP (λ i → PathP (λ j → B (compPath-filler p q i j)) (f x) (f (q i))) (cong f p) (cong f (p ∙ q))
congFunct-dep {B = B} {x = x} f p q i j = f (compPath-filler p q i j)

cong₂Funct : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} {B : Type ℓ'} (f : A → A → B) →
        (p : x ≡ y) →
        {u v : A} (q : u ≡ v) →
        cong₂ f p q ≡ cong (λ x → f x u) p ∙ cong (f y) q
cong₂Funct {x = x} {y = y} f p {u = u} {v = v} q j i =
  hcomp (λ k → λ { (i = i0) → f x u
                  ; (i = i1) → f y (q k)
                  ; (j = i0) → f (p i) (q (i ∧ k))})
       (f (p i) u)

symDistr-filler : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → I → I → I → A
symDistr-filler {A = A} {z = z} p q i j k =
  hfill (λ k → λ { (i = i0) → q (k ∨ j)
                  ; (i = i1) → p (~ k ∧ j) })
        (inS (invSides-filler q (sym p) i j))
        k

symDistr : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) → sym (p ∙ q) ≡ sym q ∙ sym p
symDistr p q i j = symDistr-filler p q j i i1

-- we can not write hcomp-isEquiv : {ϕ : I} → (p : I → Partial ϕ A) → isEquiv (λ (a : A [ ϕ ↦ p i0 ]) → hcomp p a)
-- due to size issues. But what we can write (compare to hfill) is:
hcomp-equivFillerSub : {ϕ : I} → (p : I → Partial ϕ A) → (a : A [ ϕ ↦ p i0 ])
                     → (i : I)
                     → A [ ϕ ∨ i ∨ ~ i ↦ (λ { (i = i0) → outS a
                                            ; (i = i1) → hcomp (λ i → p (~ i)) (hcomp p (outS a))
                                            ; (ϕ = i1) → p i0 1=1 }) ]
hcomp-equivFillerSub {ϕ = ϕ} p a i =
  inS (hcomp (λ k → λ { (i = i1) → hfill (λ j → p (~ j)) (inS (hcomp p (outS a))) k
                      ; (i = i0) → outS a
                      ; (ϕ = i1) → p (~ k ∧ i) 1=1 })
             (hfill p a i))

hcomp-equivFiller : {ϕ : I} → (p : I → Partial ϕ A) → (a : A [ ϕ ↦ p i0 ])
                  → (i : I) → A
hcomp-equivFiller p a i = outS (hcomp-equivFillerSub p a i)

pentagonIdentity : (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) → (s : w ≡ v)
                      →
            (assoc p q (r ∙ s) ∙ assoc (p ∙ q) r s)
                              ≡
   cong (p ∙_) (assoc q r s) ∙∙ assoc p (q ∙ r) s ∙∙ cong (_∙ s) (assoc p q r)

pentagonIdentity {x = x} {y} p q r s =
        (λ i →
              (λ j → cong (p ∙_) (assoc q r s) (i ∧ j))
           ∙∙ (λ j → lemma₀₀ i j ∙ lemma₀₁ i j)
           ∙∙ (λ j → lemma₁₀ i j ∙ lemma₁₁ i j)
        )
   where

    lemma₀₀ : ( i j : I) → _ ≡ _
    lemma₀₀ i j i₁ =
         hcomp
        (λ k → λ { (j = i0) → p i₁
                 ; (i₁ = i0) → x
                 ; (i₁ = i1) → hcomp
                                 (λ k₁ → λ { (i = i0) → (q (j ∧ k))
                                           ; (k = i0) → y
                                           ; (j = i0) → y
                                           ; (j = i1)(k = i1) → r (k₁ ∧ i)})
                                 (q (j ∧ k))
        }) (p i₁)

    lemma₀₁ : ( i j : I) → hcomp
                       (λ k → λ {(i = i0) → q j
                               ; (j = i0) → y
                               ; (j = i1) → r (k ∧ i)
                          })
                       (q j) ≡ _
    lemma₀₁ i j i₁ = (hcomp
                        (λ k → λ { (j = i1) → hcomp
                                                (λ k₁ → λ { (i₁ = i0) → r i
                                                          ; (k = i0) → r i
                                                          ; (i = i1) → s (k₁ ∧  k ∧  i₁)
                                                          ; (i₁ = i1)(k = i1) → s k₁ })
                                                (r ((i₁ ∧ k) ∨ i))
                                  ; (i₁ = i0) → compPath-filler q r i j
                                  ; (i₁ = i1) → hcomp
                                                  (λ k₁ → λ { (k = i0) → r i
                                                            ; (k = i1) → s k₁
                                                            ; (i = i1) → s (k ∧ k₁)})
                                                  (r (i ∨ k))})
                         (hfill
                             (λ k → λ { (j = i1) → r k
                                      ; (i₁ = i1) → r k
                                      ; (i₁ = i0)(j = i0) → y })
                             (inS (q (i₁ ∨ j))) i))

    lemma₁₁ : ( i j : I) → (r (i ∨ j)) ≡ _
    lemma₁₁ i j i₁ =
           hcomp
             (λ k → λ { (i = i1) → s (i₁ ∧ k)
                      ; (j = i1) → s (i₁ ∧ k)
                      ; (i₁ = i0) → r (i ∨ j)
                      ; (i₁ = i1) → s k
              }) (r (i ∨ j ∨ i₁))

    lemma₁₀-back :  I → I → I → _
    lemma₁₀-back i j i₁ =
        hcomp
         (λ k → λ {
           (i₁ = i0) → x
         ; (i₁ = i1) → hcomp
                         (λ k₁ → λ { (k = i0) → q (j ∨ ~ i)
                                   ; (k = i1) → r (k₁ ∧ j)
                                   ; (j = i0) → q (k ∨ ~ i)
                                   ; (j = i1) → r (k₁ ∧ k)
                                   ; (i = i0) → r (k ∧ j ∧ k₁)
                         })
                         (q (k ∨ j ∨ ~ i))
         ; (i = i0)(j = i0) → (p ∙ q) i₁
         })
        (hcomp
           (λ k → λ { (i₁ = i0) → x
                    ; (i₁ = i1) → q ((j ∨ ~ i ) ∧ k)
                    ; (j = i0)(i = i1) → p i₁
            })
            (p i₁))

    lemma₁₀-front : I → I → I → _
    lemma₁₀-front i j i₁ =
       (((λ _ → x) ∙∙ compPath-filler p q j ∙∙
         (λ i₁ →
             hcomp
                (λ k → λ { (i₁ = i0) → q j
                         ; (i₁ = i1) → r (k ∧ (j ∨ i))
                         ; (j = i0)(i = i0) → q i₁
                         ; (j = i1) → r (i₁ ∧ k)
               })
            (q (j ∨ i₁))
         )) i₁)

    compPath-filler-in-filler :
                (p : _ ≡ y) → (q : _ ≡ _ )
              → _≡_ {A = Square (p ∙ q) (p ∙ q) (λ _ → x) (λ _ → z)}
               (λ i j → hcomp
                          (λ i₂ →
                           λ { (j = i0) → x
                             ; (j = i1) → q (i₂ ∨ ~ i)
                             ; (i = i0) → (p ∙ q) j
                            })
                          (compPath-filler p q (~ i) j))
               (λ _ → p ∙ q)
    compPath-filler-in-filler p q z i j =
       hcomp
         (λ k → λ {
            (j = i0) → p i0
          ; (j = i1) → q (k ∨ ~ i ∧ ~ z)
          ; (i = i0) → hcomp
                       (λ i₂ → λ {
                         (j = i0) → p i0
                        ;(j = i1) → q ((k ∨  ~ z) ∧ i₂)
                        ;(z = i1) (k = i0) → p j
                       })
                      (p j)
          ; (i = i1) →  compPath-filler p (λ i₁ → q (k ∧ i₁)) k j
          ; (z = i0) → hfill
                         ((λ i₂ → λ { (j = i0) → p i0
                             ; (j = i1) → q (i₂ ∨ ~ i)
                             ; (i = i0) → (p ∙ q) j
                            }))
                         (inS ((compPath-filler p q (~ i) j))) k
          ; (z = i1) → compPath-filler p q k j
         })
         (compPath-filler p q (~ i ∧ ~ z) j)

    cube-comp₋₀₋ :
        (c : I → I → I → A)
      → {a' : Square _ _ _ _}
      → (λ i i₁ → c i i0 i₁) ≡ a'
      → (I → I → I → A)
    cube-comp₋₀₋ c p i j k =
       hcomp
         (λ l → λ {
            (i = i0) → c i0 j k
           ;(i = i1) → c i1 j k
           ;(j = i0) → p l i k
           ;(j = i1) → c i i1 k
           ;(k = i0) → c i j i0
           ;(k = i1) → c i j i1
          })
        (c i j k)

    cube-comp₀₋₋ :
        (c : I → I → I → A)
      → {a' : Square _ _ _ _}
      → (λ i i₁ → c i0 i i₁) ≡ a'
      → (I → I → I → A)
    cube-comp₀₋₋ c p i j k =
       hcomp
         (λ l → λ {
            (i = i0) → p l j k
           ;(i = i1) → c i1 j k
           ;(j = i0) → c i i0 k
           ;(j = i1) → c i i1 k
           ;(k = i0) → c i j i0
           ;(k = i1) → c i j i1
          })
        (c i j k)

    lemma₁₀-back' : _
    lemma₁₀-back' k j i₁ =
       (cube-comp₋₀₋ (lemma₁₀-back)
         (compPath-filler-in-filler p q)) k j i₁

    lemma₁₀ : ( i j : I) → _ ≡ _
    lemma₁₀ i j i₁ =
        (cube-comp₀₋₋ lemma₁₀-front (sym lemma₁₀-back')) i j i₁

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


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

-- {-# OPTIONS -v rewriting:100 -v tc.conv.atom:30 -v tc.inj.use:30 #-}

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero + n = n
(suc m) + n = suc (m + n)

postulate
  plus-zero : ∀ x → (x + zero) ≡ x

{-# REWRITE plus-zero #-}

mutual
  secret-number : Nat
  secret-number = _

  test : ∀ x → (x + secret-number) ≡ x
  test x = refl

  reveal : secret-number ≡ zero
  reveal = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Andreas and James, 2013-11-19

{-# OPTIONS --copatterns  #-}
-- {-# OPTIONS -v tc.cover.splittree:15 -v tc.cc:15 #-}

open import Common.Level
open import Common.Product

mutual
  data Delay (A : Set) : Set where
    later : ∞Delay A → Delay A

  record ∞Delay (A : Set) : Set where
    coinductive
    constructor delay
    field
      force : Delay A
open ∞Delay public

data Def {A : Set} : Delay A → Set where
  later⇓ : ∀ (x : ∞Delay A) → Def (force x) → Def (later x)

data Ty : Set where
  _⇒_ : (a b : Ty) → Ty

data Tm (Γ : Ty) : (a : Ty) → Set where
  abs : ∀ a b (t : Tm (Γ ⇒ a) b) → Tm Γ (a ⇒ b)

data Val : (a : Ty) → Set where
  lam : ∀ Γ a b (t : Tm (Γ ⇒ a) b) → Val (a ⇒ b)

postulate
  eval : ∀ Γ a → Tm Γ a → Delay (Val a)

∞apply : ∀ a b → Val (a ⇒ b) → ∞Delay (Val b)
force (∞apply .a .b (lam Γ a b t)) = eval (Γ ⇒ a) b t

β-expand : ∀ Γ a b (t : Tm (Γ ⇒ a) b) →
  Def (eval (Γ ⇒ a) b t) → Def (later (∞apply a b (lam Γ a b t)))
β-expand Γ a b t = later⇓ (∞apply a b (lam Γ a b t))

-- This line failed because of a missing reduction (due to wrong split tree).

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Prelude
open import Level using (Level) renaming (zero to lz; suc to ls)
open import Data.List.Properties as ListProps renaming (∷-injective to ∷-inj)
open import Data.String
open import Data.Nat as Nat using (decTotalOrder; _≤_; s≤s; z≤n)
open import Relation.Binary using (module DecTotalOrder)

module RW.Language.RTerm where

  open import Reflection renaming (Term to AgTerm; Type to AgType)
    public

  open DecTotalOrder Nat.decTotalOrder using (total)

  postulate
    unsuportedSyntax : ∀{a}{A : Set a} → String → A
    error            : ∀{a}{A : Set a} → String → A

  open Eq {{...}}

  -- We'll consider constructor and definitions
  -- as just names; we just need to know how to
  -- translate them back into a correct AgTerm.
  --
  -- Function type is represented with the impl constructor.
  data RTermName : Set where
    rcon : Name → RTermName
    rdef : Name → RTermName
    impl : RTermName

  showRTermName : RTermName → String
  showRTermName (rcon x) = showName x
  showRTermName (rdef x) = showName x
  showRTermName impl     = "→"

  ----------------------------------------
  -- Equalities associated with RTermNames

  rcon-inj : ∀{x y} → rcon x ≡ rcon y → x ≡ y
  rcon-inj refl = refl

  rdef-inj : ∀{x y} → rdef x ≡ rdef y → x ≡ y
  rdef-inj refl = refl

  _≟-RTermName_ : (n m : RTermName) → Dec (n ≡ m)
  rcon x ≟-RTermName rcon y with x ≟-Name y
  ...| yes x≡y = yes (cong rcon x≡y)
  ...| no  x≢y = no (x≢y ∘ rcon-inj)
  rdef x ≟-RTermName rdef y with x ≟-Name y
  ...| yes x≡y = yes (cong rdef x≡y)
  ...| no  x≢y = no (x≢y ∘ rdef-inj)
  impl ≟-RTermName impl     = yes refl
  rcon _ ≟-RTermName rdef _ = no (λ ())
  rcon _ ≟-RTermName impl   = no (λ ())
  rdef _ ≟-RTermName rcon _ = no (λ ())
  rdef _ ≟-RTermName impl   = no (λ ())
  impl ≟-RTermName rcon _   = no (λ ())
  impl ≟-RTermName rdef _   = no (λ ())

  -- Now we'll define a very handy term representation.
  -- We aim to reduce the amount of boilerplate code
  -- needed to handle Agda's complex term representation.
  --
  -- The phantom A will allow us to use multiple representations
  -- for unification variables and still prove termination
  -- by using a (Fin n), before unifying.
  data RTerm {a}(A : Set a) : Set a where
    -- Out-of-bound variables. We use a phantom type A
    -- to be able to (almost) seamless convert from
    -- ℕ to (Fin n).
    ovar : (x : A) → RTerm A

    -- Variables bound inside the term itself, from
    -- rlam's.
    ivar : (n : ℕ) → RTerm A

    -- Agda Literals
    rlit : (l : Literal) → RTerm A

    -- Lambda Abstraction
    rlam : RTerm A → RTerm A

    -- Applications
    rapp : (n : RTermName)(ts : List (RTerm A)) → RTerm A

  -- Equality Rules induced by RTerm's constructors

  ovar-inj : ∀{a}{A : Set a}{x y : A} → ovar {a} {A} x ≡ ovar {a} {A} y → x ≡ y
  ovar-inj refl = refl

  ivar-inj : ∀{a A x y} → ivar {a} {A} x ≡ ivar {a} {A} y → x ≡ y
  ivar-inj refl = refl

  rlit-inj : ∀{a A x y} → rlit {a} {A} x ≡ rlit {a} {A} y → x ≡ y
  rlit-inj refl = refl

  rlam-inj : ∀{a A x y} → rlam {a} {A} x ≡ rlam {a} {A} y → x ≡ y
  rlam-inj refl = refl

  rapp-inj : ∀{a A n₁ n₂ l₁ l₂}
           → rapp {a} {A} n₁ l₁ ≡ rapp {a} {A} n₂ l₂
           → n₁ ≡ n₂ × l₁ ≡ l₂
  rapp-inj refl = refl , refl

  --------------------------
  -- Generalized Comparison

  mutual
    compRTerm : ∀{A} ⦃ eqA : Eq A ⦄
              → (m n : RTerm A)
              → Dec (m ≡ n)
    compRTerm ⦃ eq f ⦄ (ovar x) (ovar y) with f x y
    ...| yes x≡y = yes (cong ovar x≡y)
    ...| no  x≢y = no (x≢y ∘ ovar-inj)
    compRTerm (ivar x) (ivar y) with x ≟-ℕ y
    ...| yes x≡y = yes (cong ivar x≡y)
    ...| no  x≢y = no (x≢y ∘ ivar-inj)
    compRTerm (rlit x) (rlit y) with x ≟-Lit y
    ...| yes x≡y = yes (cong rlit x≡y)
    ...| no  x≢y = no (x≢y ∘ rlit-inj)
    compRTerm (rlam x) (rlam y) with compRTerm x y
    ...| yes x≡y = yes (cong rlam x≡y)
    ...| no  x≢y = no (x≢y ∘ rlam-inj)
    compRTerm (rapp x ax) (rapp y ay) with x ≟-RTermName y
    ...| no  x≢y = no (x≢y ∘ p1 ∘ rapp-inj)
    ...| yes x≡y rewrite x≡y with compRTerm* ax ay
    ...| no  ax≢ay = no (ax≢ay ∘ p2 ∘ rapp-inj)
    ...| yes ax≡ay = yes (cong (rapp y) ax≡ay)
    compRTerm (ovar _) (ivar _)   = no (λ ())
    compRTerm (ovar _) (rlit _)   = no (λ ())
    compRTerm (ovar _) (rlam _)   = no (λ ())
    compRTerm (ovar _) (rapp _ _) = no (λ ())
    compRTerm (ivar _) (ovar _)   = no (λ ())
    compRTerm (ivar _) (rlit _)   = no (λ ())
    compRTerm (ivar _) (rlam _)   = no (λ ())
    compRTerm (ivar _) (rapp _ _) = no (λ ())
    compRTerm (rlit _) (ovar _)   = no (λ ())
    compRTerm (rlit _) (ivar _)   = no (λ ())
    compRTerm (rlit _) (rlam _)   = no (λ ())
    compRTerm (rlit _) (rapp _ _) = no (λ ())
    compRTerm (rlam _) (ovar _)   = no (λ ())
    compRTerm (rlam _) (ivar _)   = no (λ ())
    compRTerm (rlam _) (rlit _)   = no (λ ())
    compRTerm (rlam _) (rapp _ _) = no (λ ())
    compRTerm (rapp _ _) (ovar _) = no (λ ())
    compRTerm (rapp _ _) (ivar _) = no (λ ())
    compRTerm (rapp _ _) (rlit _) = no (λ ())
    compRTerm (rapp _ _) (rlam _) = no (λ ())

    compRTerm* : ∀{A} ⦃ eqA : Eq A ⦄
               → (x y : List (RTerm A))
               → Dec (x ≡ y)
    compRTerm* [] [] = yes refl
    compRTerm* (_ ∷ _) []  = no (λ ())
    compRTerm* [] (_ ∷ _)  = no (λ ())
    compRTerm* (x ∷ xs) (y ∷ ys)
      with compRTerm x y
    ...| no  x≢y = no (x≢y ∘ p1 ∘ ∷-inj)
    ...| yes x≡y rewrite x≡y with compRTerm* xs ys
    ...| no  xs≢ys = no (xs≢ys ∘ p2 ∘ ∷-inj)
    ...| yes xs≡ys = yes (cong (_∷_ y) xs≡ys)

  instance
    eq-RTerm : {A : Set}{{ eqA : Eq A }} → Eq (RTerm A)
    eq-RTerm = eq compRTerm

  -- Infix version

  _≟-RTerm_ : ∀{A} ⦃ eqA : Eq A ⦄ → (x y : RTerm A) → Dec (x ≡ y)
  _≟-RTerm_ = compRTerm

  ------------------------------
  -- Term Replacement Functions

  {-# TERMINATING #-}
  replace : ∀{a b}{A : Set a}{B : Set b}
          → (ovar-f : A → RTerm B)
          → (ivar-f : ℕ → RTerm B)
          → RTerm A → RTerm B
  replace f g (ovar x) = f x
  replace f g (ivar n) = g n
  replace _ _ (rlit l) = rlit l
  replace f g (rlam x) = rlam (replace f g x)
  replace f g (rapp n ts) = rapp n (map (replace f g) ts)

  -- This is basically fmap...
  replace-A : ∀{a b}{A : Set a}{B : Set b}
            → (A → RTerm B) → RTerm A → RTerm B
  replace-A f = replace f ivar

  -- equipped with a few usefull functor lemmas.
  lemma-replace-rlam : ∀{a b}{A : Set a}{B : Set b}{f : A → RTerm B}{t : RTerm A}
                     → replace-A f (rlam t) ≡ rlam (replace-A f t)
  lemma-replace-rlam = refl

  lemma-replace-rapp : ∀{a b}{A : Set a}{B : Set b}{f : A → RTerm B}{ts : List (RTerm A)}{n : RTermName}
                     → replace-A f (rapp n ts) ≡ rapp n (map (replace-A f) ts)
  lemma-replace-rapp = refl

  _◇-A_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
        → (B → RTerm C) → (A → RTerm B)
        → A → RTerm C
  f ◇-A g = replace-A f ∘ g

  replace-ivar : ∀{a}{A : Set a}
               → (ℕ → RTerm A) → RTerm A → RTerm A
  replace-ivar f = replace ovar f

  ----------------------
  -- Counting utilities

  {-# TERMINATING #-}
  count : ∀{a}{A : Set a} → RTerm A → ℕ × ℕ
  count (ovar _) = 1 , 0
  count (ivar _) = 0 , 1
  count (rlit _) = 0 , 0
  count (rlam x) = count x
  count (rapp _ xs) = sum2 (map count xs)
    where
      sum2 : List (ℕ × ℕ) → ℕ × ℕ
      sum2 [] = 0 , 0
      sum2 ((a , b) ∷ xs) with sum2 xs
      ...| a' , b' = a + a' , b + b'

  #-A : ∀{a}{A : Set a} → RTerm A → ℕ
  #-A = p1 ∘ count

  #-ivar : ∀{a}{A : Set a} → RTerm A → ℕ
  #-ivar = p2 ∘ count

  -----------------------------------
  -- Conversion from AgTerm to RTerm

    -- compute the difference between two natural numbers, given an
  -- ordering between them.
  Δ_ : ∀ {m n} → m ≤ n → ℕ
  Δ z≤n {k} = k
  Δ s≤s  p  = Δ p

  -- correctness proof of the difference operator Δ.
  Δ-correct : ∀ {m n} (p : m ≤ n) → n ≡ m + Δ p
  Δ-correct  z≤n    = refl
  Δ-correct (s≤s p) = cong suc (Δ-correct p)

  _-Δ-_ : ∀{m}(n : ℕ)(p : m ≤ n) → ℕ
  n       -Δ- z≤n     = n
  (suc n) -Δ- s≤s prf = n -Δ- prf

  private
    convertℕ : ∀{a}{A : Set a} → ℕ → RTerm A
    convertℕ zero    = rapp (rcon (quote zero)) []
    convertℕ (suc n) = rapp (rcon (quote suc)) (convertℕ n ∷ [])

    mutual
      convert' : ℕ → AgTerm → RTerm ⊥
      convert' d (var x []) with total d x
      ...| i1 d≤x = ivar (x ∸ d)
      ...| i2 d>x = ivar x
      convert' d (lit (nat n)) = convertℕ n
      convert' d (con c args)
        = rapp (rcon c) (convertChildren d args)
      convert' d (def c args)
        = rapp (rdef c) (convertChildren d args)
      convert' d (pi (arg (arg-info visible _) (el _ t₁)) (abs _ (el _ t₂)))
        = rapp impl (convert' d t₁ ∷ convert' (suc d) t₂ ∷ [])
      convert' d (pi _ (abs _ (el _ t₂))) = convert' (suc d) t₂
      convert' d (lam _ (abs _ l))
        = rlam (convert' (suc d) l)
      convert' _ (pat-lam _ _)
        = unsuportedSyntax "Pattern-Matching lambdas."
      convert' _ (sort _)
        = unsuportedSyntax "Sorts."
      convert' _ unknown
        = unsuportedSyntax "Unknown."
      convert' _ (var _ (_ ∷ _))
        = unsuportedSyntax "Variables with arguments."
      convert' _ (lit _)
        = unsuportedSyntax "Non-ℕ literals."
      convert' _ (quote-goal _)
        = unsuportedSyntax "Reflection constructs not supported"
      convert' _ (quote-term _)
        = unsuportedSyntax "Reflection constructs not supported"
      convert' _ quote-context
        = unsuportedSyntax "Reflection constructs not supported"
      convert' _ (unquote-term _ _)
        = unsuportedSyntax "Reflection constructs not supported"

      convertChildren : ℕ → List (Arg AgTerm) → List (RTerm ⊥)
      convertChildren d [] = []
      convertChildren d (arg (arg-info visible _) x ∷ xs)
        = convert' d x ∷ convertChildren d xs
      convertChildren d (_ ∷ xs) = convertChildren d xs

  Ag2RTerm : AgTerm → RTerm ⊥
  Ag2RTerm a = convert' 0 a

  ------------------------------------------
  -- Handling Types

  Ag2RType : AgType → RTerm ⊥
  Ag2RType (el _ t) = Ag2RTerm t

  -----------------------------------------
  -- Converting Back to Agda

  open import RW.Utils.Monads using (MonadState; ST; get; inc) renaming (module Monad to MonadClass)
  open MonadClass {{...}}

  private
    mutual
      trevnoc' : RTerm ⊥ → AgTerm
      trevnoc' (ovar ())
      trevnoc' (ivar n) = var n []
      trevnoc' (rlit l) = lit l
      trevnoc' (rlam t) = lam visible (abs "_" (trevnoc' t))
      trevnoc' (rapp (rcon x) ts) = con x (trevnocChildren ts)
      trevnoc' (rapp (rdef x) ts) = def x (trevnocChildren ts)
      trevnoc' (rapp impl (t1 ∷ t2 ∷ [])) = pi (arg (arg-info visible relevant)
               (el unknown (trevnoc' t1)))
               (abs "_" (el unknown (trevnoc' t2)))
      trevnoc' (rapp impl _) = error "impl should have two arguments... always."

      trevnocChildren : List (RTerm ⊥) → List (Arg AgTerm)
      trevnocChildren []        = []
      trevnocChildren (x ∷ xs)  = arg (arg-info visible relevant) (trevnoc' x) ∷ trevnocChildren xs

  R2AgTerm : RTerm ⊥ → AgTerm
  R2AgTerm = trevnoc'

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 21-image where

import 20-sequences
open 20-sequences public

{- We give the formal specification of propositional truncation. -}

precomp-Prop :
  { l1 l2 l3 : Level} {A : UU l1} (P : hProp l2) →
  (A → type-Prop P) → (Q : hProp l3) →
  (type-Prop P → type-Prop Q) → A → type-Prop Q
precomp-Prop P f Q g = g ∘ f

universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : hProp l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-propositional-truncation l P f =
  (Q : hProp l) → is-equiv (precomp-Prop P f Q)

universal-property-propositional-truncation' :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : hProp l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-propositional-truncation' l {A = A} P f =
  (Q : hProp l) → (A → type-Prop Q) → (type-Prop P → type-Prop Q)

universal-property-propositional-truncation-simplify :
  { l1 l2 : Level} {A : UU l1} (P : hProp l2)
  ( f : A → type-Prop P) →
  ( (l : Level) → universal-property-propositional-truncation' l P f) →
  ( (l : Level) → universal-property-propositional-truncation l P f)
universal-property-propositional-truncation-simplify P f up-P l Q =
  is-equiv-is-prop
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( up-P l Q)

precomp-Π-Prop :
  { l1 l2 l3 : Level} {A : UU l1} (P : hProp l2) →
  ( f : A → type-Prop P) (Q : type-Prop P → hProp l3) →
  ( g : (p : type-Prop P) → type-Prop (Q p)) → (x : A) → type-Prop (Q (f x))
precomp-Π-Prop P f Q g x = g (f x)

dependent-universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : hProp l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
dependent-universal-property-propositional-truncation l P f =
  (Q : type-Prop P → hProp l) → is-equiv (precomp-Π-Prop P f Q)

{- We introduce the image inclusion of a map. -}

precomp-emb :
  { l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} ( i : B ↪ X) (q : hom-slice f (map-emb i)) →
  {C : UU l4} ( j : C ↪ X) (r : hom-slice (map-emb i) (map-emb j)) →
  hom-slice f (map-emb j)
precomp-emb f i q j r =
  pair
    ( ( map-hom-slice (map-emb i) (map-emb j) r) ∘
      ( map-hom-slice f (map-emb i) q))
    ( ( triangle-hom-slice f (map-emb i) q) ∙h
      ( ( triangle-hom-slice (map-emb i) (map-emb j) r) ·r
        ( map-hom-slice f (map-emb i) q)))

is-prop-hom-slice :
  { l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) → is-prop (hom-slice f (map-emb i))
is-prop-hom-slice {X = X} f i =
  is-prop-is-equiv
    ( (x : X) → fib f x → fib (map-emb i) x)
    ( fiberwise-hom-hom-slice f (map-emb i))
    ( is-equiv-fiberwise-hom-hom-slice f (map-emb i))
    ( is-prop-Π
      ( λ x → is-prop-Π
        ( λ p → is-prop-map-is-emb (map-emb i) (is-emb-map-emb i) x)))

universal-property-image :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) → is-equiv (precomp-emb f i q j)

universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image' l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) →
    hom-slice f (map-emb j) → hom-slice (map-emb i) (map-emb j)

universal-property-image-universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  universal-property-image' l f i q → universal-property-image l f i q
universal-property-image-universal-property-image' l f i q up' C j =
  is-equiv-is-prop
    ( is-prop-hom-slice (map-emb i) j)
    ( is-prop-hom-slice f j)
    ( up' C j)

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


text:
open import Agda.Primitive
open import Common.Reflection
open import Common.Prelude

macro
  deBruijn : Nat → Term → TC ⊤
  deBruijn n = unify (lam visible (abs "x" (var n [])))

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

module _ {n} {a} {A : Set a} (xs : Vec A n) where

  ok : Nat → Nat → Nat
  ok k = deBruijn 5

  -- Should give a nice error, not 'panic: variable @6 out of scope'.
  not-ok : Nat → Nat → Nat
  not-ok k = deBruijn 6

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- Other common operations and lemmas. -}
module TemporalOps.Common.Other where

open import Relation.Binary.HeterogeneousEquality as ≅ hiding (inspect)
open import Relation.Binary.PropositionalEquality hiding (inspect)

-- Time indexing (for clarity, synonym of function appliation at any level)
_at_ : ∀ {a b} {A : Set a} {B : A → Set b} →
      ((x : A) → B x) → ((x : A) → B x)
f at n = f n
infixl 45 _at_

-- Inspect idiom
data Singleton {a} {A : Set a} (x : A) : Set a where
  _with≡_ : (y : A) → x ≡ y → Singleton x

inspect : ∀ {a} {A : Set a} (x : A) → Singleton x
inspect x = x with≡ refl

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Selective.Examples.Fibonacci where

open import Selective.ActorMonad
open import Prelude

open import Debug
open import Data.Nat.Show using (show)

data End : Set where
  END : End

ℕ-message : MessageType
ℕ-message = [ ValueType ℕ ]ˡ

End-message : MessageType
End-message = [ ValueType End ]ˡ

Client-to-Server : InboxShape
Client-to-Server = ℕ-message ∷ [ End-message ]ˡ

Server-to-Client : InboxShape
Server-to-Client = [ ℕ-message ]ˡ

ServerInterface : InboxShape
ServerInterface = [ ReferenceType Server-to-Client ]ˡ ∷ Client-to-Server

ClientInterface : InboxShape
ClientInterface = [ ReferenceType Client-to-Server ]ˡ ∷ Server-to-Client

ServerRefs : TypingContext
ServerRefs = [ Server-to-Client ]ˡ

constServerRefs : {A : Set₁} → (A → TypingContext)
constServerRefs _ = ServerRefs

data ServerAction : Set₁ where
  Next : ℕ → ServerAction
  Done : ServerAction

server : ∀ {i} → ActorM i ServerInterface ⊤₁ [] constServerRefs
server = wait-for-client ∞>> run-fibonacci 1
  where
    wait-for-client = selective-receive (λ {
      (Msg Z _) → true
      ; (Msg (S _) _) → false }) >>= λ {
        record { msg = (Msg Z _) } → return tt
        ; record { msg = (Msg (S _) _) ; msg-ok = () } }
    wait-for-value : ∀ {i} → ∞ActorM i ServerInterface ServerAction ServerRefs constServerRefs
    wait-for-value = selective-receive (λ {
      (Msg Z _) → false
      ; (Msg (S Z) _) → true
      ; (Msg (S (S Z)) _) → true
      ; (Msg (S (S (S ()))) x₁) }) >>= λ {
        record { msg = (Msg Z _) ; msg-ok = () }
        ; record { msg = (Msg (S Z) (n ∷ [])) } → return₁ (Next n)
        ; record { msg = (Msg (S (S Z)) _) } → return₁ Done
        ; record { msg = (Msg (S (S (S ()))) _) }
        }
    run-fibonacci : ℕ → ∀ {i} → ∞ActorM i ServerInterface ⊤₁ ServerRefs constServerRefs
    run-fibonacci x .force = begin do
      Next n ← wait-for-value
        where Done → return _
      let next = x + n
      Z ![t: Z ] [ lift next ]ᵃ
      (run-fibonacci next)

ClientRefs : TypingContext
ClientRefs = [ Client-to-Server ]ˡ

constClientRefs : {A : Set₁} → (A → TypingContext)
constClientRefs _ = ClientRefs

client : ∀ {i} → ActorM i ClientInterface ⊤₁ [] constClientRefs
client = wait-for-server ∞>> run 10 0
  where
    wait-for-server : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] constClientRefs
    wait-for-server = selective-receive (λ {
      (Msg Z _) → true
      ; (Msg (S _) _) → false }) >>= λ {
        record { msg = (Msg Z _) ; msg-ok = msg-ok } → return tt
        ; record { msg = (Msg (S _) _) ; msg-ok = () }
        }
    wait-for-value : ∀ {i} → ∞ActorM i ClientInterface (Lift (lsuc lzero) ℕ) ClientRefs constClientRefs
    wait-for-value = do
      record { msg = Msg (S Z) (n ∷ []) } ← selective-receive (λ {
        (Msg Z _) → false
        ; (Msg (S Z) _) → true
        ; (Msg (S (S ())) _) })
        where
          record { msg = (Msg Z _) ; msg-ok = () }
          record { msg = (Msg (S (S ())) x₁) }
      return n
    run : ℕ → ℕ → ∀ {i} → ∞ActorM i ClientInterface ⊤₁ ClientRefs constClientRefs
    run zero x = Z ![t: S Z ] [ lift END ]ᵃ
    run (suc todo) x .force = begin do
      (Z ![t: Z ] ((lift x) ∷ []))
      (lift n) ← wait-for-value
      let next = x + n
      run (debug (show next) todo) next

spawner : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → ClientInterface ∷ [ ServerInterface ]ˡ)
spawner = do
  spawn server
  spawn client
  S Z ![t: Z ] [ [ Z ]>: ⊆-suc ⊆-refl ]ᵃ
  Z ![t: Z ] [ [ S Z ]>: ⊆-suc ⊆-refl ]ᵃ

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
module Issue427 where

data T : Set where
  tt : T

test = (λ {s : T} {t : T} → t) {tt} {tt}

f : {s t : T} → T
f = tt

test₂ = (let x = tt in λ {s : T} {t : T} → x) {tt} {tt}


text:
module ColDivSeq where

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

-- -----------------------------------------------
data OneCounter : Set where
  ZeroCounter : OneCounter

data LTOneCounter : ℕ → Set where
  Is : (ℕ → LTOneCounter 0) → OneCounter → LTOneCounter 0

data CollatzIsTrue : Set where
  -- 再帰する時に引数を減らしたから、こっちも減らすべき？
  -- いやちがうな
  Is : (LTOneCounter 0) → CollatzIsTrue

data Hoge : Set where
  Is : CollatzIsTrue → Hoge

-- 1x+1&3x+1DoNotHave2Counter : ℕ → (m : ℕ) → n:ℕ → (Hoge) →「R(m)=1かつR(n)=1かつm≠nかつR(m)≠R(n)」🔴
-- 　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　↑ m, nは存在量化する
1x+1&3x+1isLT1Counter : ℕ → (m : ℕ) → ℕ → (Hoge) → LTOneCounter m
1x+1&3x+1isLT1Counter d m n = {!!}

fToA : ℕ → Hoge
-- ↓CollatzIsTrueにdがあらわれてないと、
-- 1x+1と3x+1のどちらを証明したか分からない
final : ℕ → CollatzIsTrue
fToA d = Is (final d)
final zero = {!!}
final (suc d) = Is (1x+1&3x+1isLT1Counter 1 0 2 (fToA d))


text:
module Numeral.Natural.Coprime where

open import Logic
import      Lvl
open import Numeral.Natural
open import Numeral.Natural.Relation.Divisibility
open import Relator.Equals

private variable n x y : ℕ

-- Two numbers are coprime when their only divisor is 1.
record Coprime (x : ℕ) (y : ℕ) : Stmt{Lvl.𝟎} where
  constructor intro
  field proof : (n ∣ x) → (n ∣ y) → (n ≡ 1)


text:
open import Data.Empty
open import Data.List renaming (_∷_ to _∷ₗ_ ; [_] to [_]ₗ)
open import Data.Maybe
open import Data.Product
open import Data.Sum
open import Data.Unit

open import AEff
open import AwaitingComputations
open import EffectAnnotations
open import Finality
open import Preservation
open import ProcessPreservation
open import ProcessProgress
open import Progress
open import Renamings
open import Substitutions
open import Types

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Relation.Nullary
open import Relation.Nullary.Negation

module ProcessFinality where

-- SMALL-STEP OPERATIONAL SEMANTICS FOR WELL-TYPED PROCESSES
-- WITH INLINED EVALUATION CONTEXT RULES

infix 10 _[_]↝↝_

data _[_]↝↝_ {Γ : Ctx} : {o o' : O} {PP : PType o} {QQ : PType o'} → Γ ⊢P⦂ PP → PP ⇝ QQ → Γ ⊢P⦂ QQ → Set where

  -- RUNNING INDIVIDUAL COMPUTATIONS

  run   : {X : VType}
          {o : O}
          {i : I}
          {M N : Γ ⊢M⦂ X ! (o , i)} →
          M ↝↝ N →
          ---------------------------
          (run M) [ id ]↝↝ (run N)

  -- BROADCAST RULES

  ↑-∥ₗ   : {o o' : O}
           {PP : PType o}
           {QQ : PType o'}
           {op : Σₛ} →
           (p : op ∈ₒ o) →
           (V : Γ ⊢V⦂ `` (payload op)) →
           (P : Γ ⊢P⦂ PP) →
           (Q : Γ ⊢P⦂ QQ) →
           ------------------------------------------
           ((↑ op p V P) ∥ Q)
           [ par ⇝-refl (⇝-↓ₚ {op = op}) ]↝↝
           ↑ op (∪ₒ-inl op p) V (P ∥ ↓ op V Q)

  ↑-∥ᵣ   : {o o' : O}
           {PP : PType o}
           {QQ : PType o'}
           {op : Σₛ} →
           (p : op ∈ₒ o') →
           (V : Γ ⊢V⦂ `` (payload op)) →
           (P : Γ ⊢P⦂ PP) →
           (Q : Γ ⊢P⦂ QQ) →
           ------------------------------------------
           (P ∥ (↑ op p V Q))
           [ par (⇝-↓ₚ {op = op}) ⇝-refl ]↝↝
           ↑ op (∪ₒ-inr op p) V (↓ op V P ∥ Q)

  -- INTERRUPT PROPAGATION RULES

  ↓-run : {X : VType}
          {o : O}
          {i : I}
          {op : Σₛ} →
          (V : Γ ⊢V⦂ `` (payload op)) →
          (M : Γ ⊢M⦂ X ! (o , i)) →
          -----------------------------
          ↓ op V (run M)
          [ id ]↝↝
          run (↓ op V M)

  ↓-∥   : {o o' : O}
          {PP : PType o}
          {QQ : PType o'}
          {op : Σₛ}
          (V : Γ ⊢V⦂ `` (payload op)) →
          (P : Γ ⊢P⦂ PP) →
          (Q : Γ ⊢P⦂ QQ) →
          -----------------------------
          ↓ op V (P ∥ Q)
          [ ⇝-refl ]↝↝
          ((↓ op V P) ∥ (↓ op V Q))

  ↓-↑   : {o : O}
          {PP : PType o}
          {op : Σₛ}
          {op' : Σₛ} →
          (p : op' ∈ₒ o) →
          (V : Γ ⊢V⦂ ``(payload op)) →
          (W : Γ ⊢V⦂ ``(payload op')) →
          (P : Γ ⊢P⦂ PP) →
          -----------------------------------
          ↓ op V (↑ op' p W P)
          [ ⇝-refl ]↝↝
          ↑ op' (↓ₚₚ-⊑ₒ PP op' p) W (↓ op V P)

  -- SIGNAL HOISTING RULE

  ↑     : {X : VType}
          {o : O}
          {i : I} →
          {op : Σₛ} →
          (p : op ∈ₒ o) →
          (V : Γ ⊢V⦂ `` (payload op)) →
          (M : Γ ⊢M⦂ X ! (o , i)) →
          -----------------------------
          run (↑ op p V M)
          [ id ]↝↝
          ↑ op p V (run M)

  -- EVALUATION CONTEXT RULES

  context-∥ₗ : {o o' o'' : O}
               {PP : PType o}
               {PP' : PType o''}
               {QQ : PType o'}
               {P : Γ ⊢P⦂ PP}
               {P' : Γ ⊢P⦂ PP'}
               {Q : Γ ⊢P⦂ QQ}
               {p : PP ⇝ PP'} →
               P [ p ]↝↝ P' →
               ------------------
               P ∥ Q
               [ par p ⇝-refl ]↝↝
               P' ∥ Q

  context-∥ᵣ : {o o' o'' : O}
               {PP : PType o}
               {QQ : PType o'}
               {QQ' : PType o''}
               {P : Γ ⊢P⦂ PP}
               {Q : Γ ⊢P⦂ QQ}
               {Q' : Γ ⊢P⦂ QQ'}
               {r : QQ ⇝ QQ'} →
               Q [ r ]↝↝ Q' →
               ------------------
               P ∥ Q
               [ par ⇝-refl r ]↝↝
               P ∥ Q'

  context-↑ : {o o' : O}
              {PP : PType o}
              {PP' : PType o'}
              {op : Σₛ}
              {p : op ∈ₒ o} →
              {V : Γ ⊢V⦂ ``(payload op)}
              {P : Γ ⊢P⦂ PP}
              {P' : Γ ⊢P⦂ PP'}
              {r : PP ⇝ PP'} →
              P [ r ]↝↝ P' →
              --------------------------
              ↑ op p V P
              [ r ]↝↝
              ↑ op (⇝-⊑ₒ r op p) V P'

  context-↓ : {o o' : O}
              {PP : PType o}
              {PP' : PType o'}
              {op : Σₛ}
              {V : Γ ⊢V⦂ ``(payload op)}
              {P : Γ ⊢P⦂ PP}
              {P' : Γ ⊢P⦂ PP'}
              {r : PP ⇝ PP'} →
              P [ r ]↝↝ P' →
              ----------------------
              ↓ op V P
              [ ⇝-↓ₚ-cong r ]↝↝
              ↓ op V P'

-- ONE-TO-ONE CORRESPONDENCE BETWEEN THE TWO SETS OF REDUCTION RULES

[]↝↝-to-[]↝ : {Γ : Ctx}
              {o o' : O}
              {PP : PType o}
              {QQ : PType o'}
              {P : Γ ⊢P⦂ PP}
              {Q : Γ ⊢P⦂ QQ}
              {r : PP ⇝ QQ} →
              P [ r ]↝↝ Q →
              -----------------
              P [ r ]↝ Q

[]↝↝-to-[]↝ (run r) =
  run (↝↝-to-↝ r)
[]↝↝-to-[]↝ (↑-∥ₗ p V P Q) =
  ↑-∥ₗ p V P Q
[]↝↝-to-[]↝ (↑-∥ᵣ p V P Q) =
  ↑-∥ᵣ p V P Q
[]↝↝-to-[]↝ (↓-run V M) =
  ↓-run V M
[]↝↝-to-[]↝ (↓-∥ V P Q) =
  ↓-∥ V P Q
[]↝↝-to-[]↝ (↓-↑ p V W P) =
  ↓-↑ p V W P
[]↝↝-to-[]↝ (↑ p V M) =
  ↑ p V M
[]↝↝-to-[]↝ (context-∥ₗ r) =
  context (_ ∥ₗ _) ([]↝↝-to-[]↝ r)
[]↝↝-to-[]↝ (context-∥ᵣ r) =
  context (_ ∥ᵣ _) ([]↝↝-to-[]↝ r)
[]↝↝-to-[]↝ (context-↑ r) =
  context (↑ _ _ _ _) ([]↝↝-to-[]↝ r)
[]↝↝-to-[]↝ (context-↓ r) =
  context (↓ _ _ _) ([]↝↝-to-[]↝ r)

≡-app₂ : {X : Set}
         {Y Z : X → Set}
         {f g : (x : X) → Y x → Z x} →
         f ≡ g →
         (x : X) →
         (y : Y x) →
         -----------------------------
         f x y ≡ g x y

≡-app₂ refl x y =
  refl

[]↝-context-to-[]↝↝-aux : {Γ : Ctx}
                          {o o' : O}
                          {op : Σₛ}
                          {p : op ∈ₒ o}
                          {PP : PType o}
                          {QQ : PType o'} →
                          (F : Γ ⊢F⦂ PP) →
                          (r : proj₂ (hole-ty-f F) ⇝ QQ) →
                          ----------------------------------------------------------
                          ⇝-⊑ₒ (proj₂ (proj₂ (⇝-f-⇝ F r))) op p ≡ ⇝-f-∈ₒ F r op p

[]↝-context-to-[]↝↝-aux {Γ} {o} {o'} {op} {p} F r =
  ≡-app₂ (⊑ₒ-irrelevant (⇝-⊑ₒ (proj₂ (proj₂ (⇝-f-⇝ F r)))) (⇝-f-∈ₒ F r)) op p

mutual

  []↝-context-to-[]↝↝ : {Γ : Ctx}
                        {o o' : O}
                        {PP : PType o}
                        {QQ : PType o'} →
                        (F : Γ ⊢F⦂ PP) →
                        {P : Γ ⊢P⦂ proj₂ (hole-ty-f F)}
                        {Q : Γ ⊢P⦂ QQ}
                        {r : proj₂ (hole-ty-f F) ⇝ QQ} →
                        P [ r ]↝ Q →
                        -----------------------------------------------------------------------------
                        F [ P ]f
                        [ proj₂ (proj₂ (⇝-f-⇝ F r)) ]↝↝
                        (⇝-f F r) [ subst-i PType (λ o QQ → Γ ⊢P⦂ QQ) (⇝-f-tyₒ F r) (⇝-f-ty F r) Q ]f

  []↝-context-to-[]↝↝ [-] r =
    []↝-to-[]↝↝ r
  []↝-context-to-[]↝↝ (F ∥ₗ Q) r =
    context-∥ₗ ([]↝-context-to-[]↝↝ F r)
  []↝-context-to-[]↝↝ (P ∥ᵣ F) r =
    context-∥ᵣ ([]↝-context-to-[]↝↝ F r)
  []↝-context-to-[]↝↝ {Γ} {o} {o'} {PP} {QQ} (↑ op p V F) {P} {Q} {r'} r
    rewrite sym ([]↝-context-to-[]↝↝-aux {op = op} {p = p} F r') =
      context-↑ ([]↝-context-to-[]↝↝ F r)
  []↝-context-to-[]↝↝ (↓ op V F) r =
    context-↓ ([]↝-context-to-[]↝↝ F r)

  []↝-to-[]↝↝ : {Γ : Ctx}
                {o o' : O}
                {PP : PType o}
                {QQ : PType o'}
                {P : Γ ⊢P⦂ PP}
                {Q : Γ ⊢P⦂ QQ}
                {r : PP ⇝ QQ} →
                P [ r ]↝ Q →
                -----------------
                P [ r ]↝↝ Q

  []↝-to-[]↝↝ (run r) =
    run (↝-to-↝↝ r)
  []↝-to-[]↝↝ (↑-∥ₗ p V P Q) =
    ↑-∥ₗ p V P Q
  []↝-to-[]↝↝ (↑-∥ᵣ p V P Q) =
    ↑-∥ᵣ p V P Q
  []↝-to-[]↝↝ (↓-run V M) =
    ↓-run V M
  []↝-to-[]↝↝ (↓-∥ V P Q) =
    ↓-∥ V P Q
  []↝-to-[]↝↝ (↓-↑ p V W P) =
    ↓-↑ p V W P
  []↝-to-[]↝↝ (↑ p V M) =
    ↑ p V M
  []↝-to-[]↝↝ (context F r) =
    []↝-context-to-[]↝↝ _ r

-- FINALITY OF RESULT FORMS

par-finality-↝↝ : {o o' : O}
                  {PP : PType o}
                  {QQ : PType o'}
                  {P : [] ⊢P⦂ PP} →
                  {Q : [] ⊢P⦂ QQ} →
                  ParResult⟨ P ⟩ →
                  (r : PP ⇝ QQ) →
                  P [ r ]↝↝ Q →
                  -----------------
                  ⊥

par-finality-↝↝ (run R) .id (run r) =
  run-finality-↝↝ R r
par-finality-↝↝ (run R) .id (↑ p V M) =
  run-↑-⊥ R
par-finality-↝↝ (par R S) .(par _ ⇝-refl) (context-∥ₗ r') =
  par-finality-↝↝ R _ r'
par-finality-↝↝ (par R S) .(par ⇝-refl _) (context-∥ᵣ r') =
  par-finality-↝↝ S _ r'

proc-finality-↝↝ : {o o' : O}
                  {PP : PType o}
                  {QQ : PType o'}
                  {P : [] ⊢P⦂ PP} →
                  {Q : [] ⊢P⦂ QQ} →
                  ProcResult⟨ P ⟩ →
                  (r : PP ⇝ QQ) →
                  P [ r ]↝↝ Q →
                  -----------------
                  ⊥

proc-finality-↝↝ (proc R) r r' =
  par-finality-↝↝ R r r'
proc-finality-↝↝ (signal R) r (context-↑ r') =
  proc-finality-↝↝ R r r'

{- LEMMA 4.2 -}

proc-finality : {o o' : O}
                {PP : PType o}
                {QQ : PType o'}
                {P : [] ⊢P⦂ PP} →
                {Q : [] ⊢P⦂ QQ} →
                ProcResult⟨ P ⟩ →
                (r : PP ⇝ QQ) →
                P [ r ]↝ Q →
                -----------------
                ⊥

proc-finality R r r' =
  proc-finality-↝↝ R r ([]↝-to-[]↝↝ r')

max_stars_repo_name: danelahman/aeff-agda

max_issues_repo_name: danelahman/aeff-agda

max_forks_repo_name: danelahman/aeff-agda


text:
{-

This file contains:

- Properties of groupoid truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.GroupoidTruncation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.GroupoidTruncation.Base

recGroupoidTrunc : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (gB : isGroupoid B) → (A → B) → (∥ A ∥₁ → B)
recGroupoidTrunc gB f ∣ x ∣₁ = f x
recGroupoidTrunc gB f (squash₁ _ _ _ _ r s i j k) =
  gB _ _ _ _
    (λ m n → recGroupoidTrunc gB f (r m n))
    (λ m n → recGroupoidTrunc gB f (s m n))
    i j k

groupoidTruncFib : ∀ {ℓ ℓ'} {A : Type ℓ} (P : A → Type ℓ')
              {a b : A} (sPb : isGroupoid (P b))
              {p q : a ≡ b} {r s : p ≡ q} (u : r ≡ s) {a1 : P a} {b1 : P b}
              {p1 : PathP (λ i → P (p i)) a1 b1}
              {q1 : PathP (λ i → P (q i)) a1 b1}
              (r1 : PathP (λ i → PathP (λ j → P (r i j)) a1 b1) p1 q1)
              (s1 : PathP (λ i → PathP (λ j → P (s i j)) a1 b1) p1 q1)
            → PathP (λ i → PathP (λ j → PathP (λ k → P (u i j k)) a1 b1) p1 q1) r1 s1
groupoidTruncFib P {a} {b} sPb u {a1} {b1} {p1} {q1} r1 s1 i j k =
  hcomp (λ l → λ { (i = i0) → r1 j k
                 ; (i = i1) → s1 j k
                 ; (j = i0) → p1 k
                 ; (j = i1) → q1 k
                 ; (k = i0) → a1
                 ; (k = i1) → sPb b1 b1 refl refl (λ i j → Lb i j i1) refl l i j
                 })
        (Lb i j k)
  where
  L : (i j : I) → P b
  L i j = comp (λ k → P (u i j k))
               (λ k → λ { (i = i0) → r1 j k
                        ; (i = i1) → s1 j k
                        ; (j = i0) → p1 k
                        ; (j = i1) → q1 k })
               a1
  Lb : PathP (λ i → PathP (λ j → PathP (λ k → P (u i j k)) a1 (L i j)) p1 q1) r1 s1
  Lb i j k = fill (λ k → P (u i j k))
                  (λ k → λ { (i = i0) → r1 j k
                           ; (i = i1) → s1 j k
                           ; (j = i0) → p1 k
                           ; (j = i1) → q1 k })
                  (inS a1) k

groupoidTruncElim : ∀ {ℓ ℓ'} (A : Type ℓ) (B : ∥ A ∥₁ → Type ℓ')
                    (bG : (x : ∥ A ∥₁) → isGroupoid (B x))
                    (f : (x : A) → B ∣ x ∣₁) (x : ∥ A ∥₁) → B x
groupoidTruncElim A B bG f (∣ x ∣₁) = f x
groupoidTruncElim A B bG f (squash₁ x y p q r s i j k) =
  groupoidTruncFib B (bG y)
                   (squash₁ x y p q r s)
                   (λ i j → groupoidTruncElim A B bG f (r i j))
                   (λ i j → groupoidTruncElim A B bG f (s i j))
                   i j k

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module Thesis.SIRelBigStep.Lang where

open import Thesis.SIRelBigStep.Types public
open import Thesis.SIRelBigStep.Syntax public
open import Thesis.SIRelBigStep.DenSem public
open import Thesis.SIRelBigStep.OpSem public
open import Thesis.SIRelBigStep.SemEquiv public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import Categories.Category
open import Categories.Category.CartesianClosed.Locally

module Categories.Category.CartesianClosed.Locally.Properties {o ℓ e} {C : Category o ℓ e}
  (LCCC : Locally C) where

open import Categories.Category.CartesianClosed
open import Categories.Category.Slice
open import Categories.Category.Slice.Properties
open import Categories.Functor
open import Categories.Functor.Slice

private
  module C = Category C
  open C
  open Locally LCCC
  variable
    A B : Obj

module _ (f : A ⇒ B) where
  open CartesianClosed (sliceCCC B)

  private
    C/A   = Slice C A
    C/B   = Slice C B
    C/B/f = Slice C/B (sliceobj f)

    fObj : SliceObj C B
    fObj = sliceobj f

    i : Slice⇒ C ⊤ (fObj ^ fObj)
    i = λg π₂

    J : Functor C/A C/B/f
    J = slice⇒slice-slice C f

    I : Functor (Slice C/B (fObj ^ fObj)) C/B
    I = pullback-functorial C/B slice-pullbacks i

    K : Functor C/B/f (Slice C/B (fObj ^ fObj))
    K = Base-F C/B (fObj ⇨-)

  -- this functor should be the right adjoint functor of (BaseChange* C pullbacks f).
  BaseChange⁎ : Functor C/A C/B
  BaseChange⁎ = I ∘F K ∘F J

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
------------------------------------------------------------------------
-- Types used (only) when calling out to Haskell via the FFI
------------------------------------------------------------------------

module Foreign.Haskell where

open import Coinduction
open import Data.Colist as C using ([]; _∷_)

------------------------------------------------------------------------
-- Simple types

-- A unit type.

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

-- Potentially infinite lists.

infixr 5 _∷_

codata Colist (A : Set) : Set where
  []  : Colist A
  _∷_ : (x : A) (xs : Colist A) → Colist A

{-# COMPILED_DATA Colist [] [] (:) #-}

fromColist : ∀ {A} → C.Colist A → Colist A
fromColist []       = []
fromColist (x ∷ xs) = x ∷ fromColist (♭ xs)

toColist : ∀ {A} → Colist A → C.Colist A
toColist []       = []
toColist (x ∷ xs) = x ∷ ♯ toColist xs

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- {-# OPTIONS -v tc.meta:100 #-}
-- Andreas, 2011-04-20
-- see Abel Pientka TLCA 2011
module PruningNonMillerPattern where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

test : let X : Nat -> Nat -> Nat
           X = _
           Y : Nat -> Nat -> Nat
           Y = _
       in  (C : Set) ->
           (({x y : Nat} -> X x x ≡ suc (Y x y)) ->
            ({x y : Nat} -> Y x x ≡ x)           ->
            ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
test C k = k refl refl refl
{- none of these equations is immediately solvable.  However,
   from 1. we deduce that Y does not depend on its second argument, thus
   from 2. we solve Y x y = x, and then
   eqn. 3. simplifies to X x y = X x x, thus, X does not depend on its second arg,
   we can then solve using 1.  X x y = suc x
-}

-- a variant, where pruning is even triggered from a non-pattern
test' : let X : Nat -> Nat -> Nat
            X = _
            Y : Nat -> Nat -> Nat
            Y = _
        in  (C : Set) ->
            (({x y : Nat} -> X x (suc x) ≡ suc (Y x y)) ->  -- non-pattern lhs
             ({x y : Nat} -> Y x x ≡ x)           ->
             ({x y : Nat} -> X (Y x y) y ≡ X x x) -> C) -> C
test' C k = k refl refl refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Categories.Category.Cocomplete where

open import Level

open import Categories.Category using (Category)
open import Categories.Functor using (Functor)
open import Categories.Diagram.Colimit using (Colimit)

Cocomplete : (o ℓ e : Level) {o′ ℓ′ e′ : Level} (C : Category o′ ℓ′ e′) → Set _
Cocomplete o ℓ e C = ∀ {J : Category o ℓ e} (F : Functor J C) → Colimit F

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------------
-- Some proofs related to the power function
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Pow.PropertiesATP where

open import FOT.FOTC.Data.Nat.Pow

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP

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

postulate 0^0≡1 : 0' ^ 0' ≡ 1'
{-# ATP prove 0^0≡1 #-}

0^Sx≡0 : ∀ {n} → N n → 0' ^ succ₁ n ≡ 0'
0^Sx≡0 {.zero} nzero  = prf
  where postulate prf : 0' ^ succ₁ zero ≡ 0'
        {-# ATP prove prf #-}

0^Sx≡0 (nsucc {n} Nn) = prf
  where postulate prf : 0' ^ succ₁ (succ₁ n) ≡ 0'
        {-# ATP prove prf #-}

thm₁ : ∀ {n} → N n → 5' ≤ n → n ^ 5' ≤ 5' ^ n
thm₁ nzero h = prf
  where postulate prf : zero ^ 5' ≤ 5' ^ zero
        {-# ATP prove prf #-}
thm₁ (nsucc {n} Nn) h = prf (thm₁ Nn) h
  where
  postulate prf : (5' ≤ n → n ^ 5' ≤ 5' ^ n) →
                  5' ≤ succ₁ n →
                  succ₁ n ^ 5' ≤ 5' ^ succ₁ n
  -- 2018-06-28: The ATPs could not prove the theorem (300 sec).
  -- {-# ATP prove prf 5-N #-}

thm₂ : ∀ {n} → N n →
       ((2' ^ n) ∸ 1') + 1' + ((2' ^ n) ∸ 1') ≡ 2' ^ (n + 1') ∸ 1'
thm₂ nzero = prf
  where
  postulate prf : ((2' ^ zero) ∸ 1') + 1' + ((2' ^ zero) ∸ 1') ≡
                  2' ^ (zero + 1') ∸ 1'
  {-# ATP prove prf #-}
thm₂ (nsucc {n} Nn) = prf (thm₂ Nn)
  where
  postulate prf : ((2' ^ n) ∸ 1') + 1' + ((2' ^ n) ∸ 1') ≡
                  2' ^ (n + 1') ∸ 1' →
                  ((2' ^ succ₁ n) ∸ 1') + 1' + ((2' ^ succ₁ n) ∸ 1') ≡
                  2' ^ (succ₁ n + 1') ∸ 1'
  -- 2018-06-28: The ATPs could not prove the theorem (300 sec).
  -- {-# ATP prove prf #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module induction where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_)

-- -------------------------------
-- (zero + n) + p ≡ zero + (n + p)
--
-- (m + n) + p ≡ m + (n + p)
-- ---------------------------------
-- (suc m + n) + p ≡ suc m + (n + p)

-- 1)
-- In the beginning, we know nothing.

-- On the first day, we know zero.
-- 0 : ℕ

-- On the second day, we know one and about associativity of 0.
-- 0 : ℕ
-- 1 : ℕ    (0 + 0) + 0 ≡ 0 + (0 + 0)

-- On the third day, we know two and about associativity of 1.
-- 0 : ℕ
-- 1 : ℕ    (0 + 0) + 0 ≡ 0 + (0 + 0)
-- 2 : ℕ    (0 + 1) + 0 ≡ 0 + (1 + 0)    (0 + 1) + 1 ≡ 0 + (1 + 1)    (0 + 0) + 1 ≡ 0 + (0 + 1)    (1 + 0) + 0 ≡ 1 + (0 + 0)

-- On the fourth day, we know two and about associativity of 2.
-- 0 : ℕ
-- 1 : ℕ    (0 + 0) + 0 ≡ 0 + (0 + 0)
-- 2 : ℕ    (0 + 1) + 0 ≡ 0 + (1 + 0)    (0 + 1) + 1 ≡ 0 + (1 + 1)    (0 + 0) + 1 ≡ 0 + (0 + 1)    (1 + 0) + 0 ≡ 1 + (0 + 0)    (1 + 0) + 1 ≡ 1 + (0 + 1)    (1 + 1) + 0 ≡ 1 + (1 + 0)    (1 + 1) + 1 ≡ 1 + (1 + 1)
-- 3 : ℕ    (0 + 2) + 0 ≡ 0 + (2 + 0)    (0 + 2) + 2 ≡ 0 + (2 + 2)    (0 + 0) + 2 ≡ 0 + (0 + 2)    (0 + 2) + 1 ≡ 0 + (2 + 1)    (0 + 1) + 2 ≡ 0 + (1 + 2)    (2 + 0) + 0 ≡ 2 + (0 + 0)    (2 + 1) + 0 ≡ 2 + (1 + 0)    (2 + 2) + 0 ≡ 2 + (2 + 0)    (2 + 0) + 1 ≡ 2 + (0 + 1)    (2 + 0) + 2 ≡ 2 + (0 + 2)    (2 + 1) + 1 ≡ 2 + (1 + 1)    (2 + 1) + 2 ≡ 2 + (1 + 2)    (2 + 2) + 1 ≡ 2 + (2 + 1)    (2 + 2) + 2 ≡ 2 + (2 + 2)

-- 2)
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    n + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc (m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ cong suc (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identityʳ (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ cong suc (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identityʳ m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ cong suc (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎

+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
  begin
    m + (n + p)
  ≡⟨ sym (+-assoc m n p) ⟩
    (m + n) + p
  ≡⟨ cong (_+ p) (+-comm m n) ⟩
    (n + m) + p
  ≡⟨ +-assoc n m p ⟩
    n + (m + p)
  ∎

-- +-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
-- +-swap m n p rewrite sym (+-assoc m n p)
--                 | cong (_+ p) (+-comm m n)
--                 | +-assoc n m p
--                 = refl

-- 3)
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p =
  begin
    (zero + n) * p
  ≡⟨⟩
    n * p
  ≡⟨⟩
    zero * p + n * p
  ∎
*-distrib-+ (suc m) n p =
  begin
    ((suc m) + n) * p
  ≡⟨⟩
    suc (m + n) * p
  ≡⟨⟩
    p + ((m + n) * p)
  ≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
    p + (m * p + n * p)
  ≡⟨ sym (+-assoc p (m * p) (n * p))⟩
    (p + m * p) + n * p
  ≡⟨⟩
    (suc m) * p + n * p
  ∎

-- 4)
*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p =
  begin
    (zero * n) * p
  ≡⟨⟩
    zero * p
  ≡⟨⟩
    zero
  ≡⟨⟩
    zero * n
  ≡⟨⟩
    zero * (n * p)
  ∎
*-assoc (suc m) n p =
  begin
    (suc m * n) * p
  ≡⟨⟩
    (n + m * n) * p
  ≡⟨ *-distrib-+ n (m * n) p ⟩
    (n * p) + (m * n) * p
  ≡⟨ cong ((n * p) +_) (*-assoc m n p) ⟩
    (n * p) + m * (n * p)
  ≡⟨⟩
    suc m * (n * p)
  ∎

-- 5)
*-absorbingʳ : ∀ (m : ℕ) → m * zero ≡ zero
*-absorbingʳ zero =
  begin
    zero * zero
  ≡⟨⟩
    zero
  ∎
*-absorbingʳ (suc m) =
  begin
    suc m * zero
  ≡⟨⟩
    zero + m * zero
  ≡⟨ cong (zero +_) (*-absorbingʳ m) ⟩
    zero + zero
  ≡⟨⟩
    zero
  ∎

*-suc : ∀ (m n : ℕ) → m * suc n ≡ m + m * n
*-suc zero n =
  begin
    zero * (suc n)
  ≡⟨⟩
    zero
  ≡⟨⟩
    zero * n
  ≡⟨⟩
    zero + zero * n
  ∎
*-suc (suc m) n =
  begin
    suc m * suc n
  ≡⟨⟩
    (suc n) + (m * suc n)
  ≡⟨ cong ((suc n) +_) (*-suc m n) ⟩
    (suc n) + (m + m * n)
  ≡⟨⟩
    suc (n + (m + m * n))
  ≡⟨ cong suc (sym (+-assoc n m (m * n))) ⟩
    suc ((n + m) + m * n)
  ≡⟨ cong (λ {term → suc (term + m * n)}) (+-comm n m) ⟩
    suc ((m + n) + m * n)
  ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
    suc (m + (n + m * n))
  ≡⟨⟩
    suc (m + (suc m * n))
  ≡⟨⟩
    suc m + suc m * n
  ∎

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm m zero =
  begin
    m * zero
  ≡⟨ *-absorbingʳ m ⟩
    zero
  ≡⟨⟩
    zero * m
  ∎
*-comm m (suc n) =
  begin
    m * suc n
  ≡⟨ *-suc m n ⟩
    m + m * n
  ≡⟨ cong (m +_) (*-comm m n) ⟩
    m + n * m
  ≡⟨⟩
    suc n * m
  ∎

-- 6)
0∸n≡0 : ∀ (n : ℕ) → zero ∸ n ≡ zero
0∸n≡0 zero =
  begin
    zero ∸ zero
  ≡⟨⟩
    zero
  ∎
0∸n≡0 (suc n) =
  begin
    zero ∸ suc n
  ≡⟨⟩
    zero
  ∎
-- No induction needed, just prove it holds for 0 and for suc n. (Holds because of definition of ∸)

-- 7)
0∸n≡0∸n+p : ∀ (n p : ℕ) → zero ∸ n ≡ zero ∸ (n + p)
0∸n≡0∸n+p n zero  =
  begin
    zero ∸ n
  ≡⟨ cong (zero ∸_) (sym (+-identityʳ n)) ⟩
    zero ∸ (n + zero)
  ∎
0∸n≡0∸n+p n (suc p)  =
  begin
    zero ∸ n
  ≡⟨ 0∸n≡0 n ⟩
    zero
  ≡⟨⟩
    zero ∸ suc (n + p)
  ≡⟨ cong (zero ∸_) (sym (+-suc n p)) ⟩
    zero ∸ (n + suc p)
  ∎

∸-+-assoc : ∀ (m n p : ℕ) → (m ∸ n) ∸ p ≡ m ∸ (n + p)
∸-+-assoc zero n p =
  begin
    (zero ∸ n) ∸ p
  ≡⟨ cong (_∸ p) (0∸n≡0 n) ⟩
    zero ∸ p
  ≡⟨ 0∸n≡0 p ⟩
    zero
  ≡⟨ sym (0∸n≡0 n) ⟩
    zero ∸ n
  ≡⟨  0∸n≡0∸n+p n p ⟩
    zero ∸ (n + p)
  ∎
∸-+-assoc (suc m) zero p =
  begin
    (suc m ∸ zero) ∸ p
  ≡⟨⟩
    suc m ∸ (zero + p)
  ∎
∸-+-assoc (suc m) (suc n) p =
  begin
    (suc m ∸ suc n) ∸ p
  ≡⟨⟩
    (m ∸ n) ∸ p
  ≡⟨ ∸-+-assoc m n p ⟩
    m ∸ (n + p)
  ≡⟨⟩
    suc m ∸ suc (n + p)
  ≡⟨⟩
    suc m ∸ (suc n + p)
  ∎

-- 8)
*-identityˡ : ∀ (n : ℕ) → 1 * n ≡ n
*-identityˡ n =
  begin
    1 * n
  ≡⟨⟩
    (suc zero) * n
  ≡⟨⟩
    n + (zero * n)
  ≡⟨⟩
    n + zero
  ≡⟨ +-identityʳ n ⟩
    n
  ∎

^-distribˡ-+-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
^-distribˡ-+-* m zero p =
  begin
    m ^ (zero + p)
  ≡⟨⟩
    m ^ p
  ≡⟨ sym (*-identityˡ (m ^ p)) ⟩
    1 * m ^ p
  ≡⟨⟩
    (m ^ zero) * (m ^ p)
  ∎
^-distribˡ-+-* m (suc n) p =
  begin
    m ^ (suc n + p)
  ≡⟨⟩
    m ^ suc (n + p)
  ≡⟨⟩
    m * (m ^ (n + p))
  ≡⟨ cong (m *_) (^-distribˡ-+-* m n p) ⟩
    m * (m ^ n * m ^ p)
  ≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
    (m * m ^ n) * m ^ p
  ≡⟨⟩
    (m ^ suc n) * (m ^ p)
  ∎

^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
^-distribʳ-* m n zero =
  begin
    (m * n) ^ zero
  ≡⟨⟩
    1
  ≡⟨⟩
    1 * 1
  ≡⟨⟩
    (m ^ zero) * (n ^ zero)
  ∎
^-distribʳ-* m n (suc p) =
  begin
    (m * n) ^ (suc p)
  ≡⟨⟩
    (m * n) * (m * n) ^ p
  ≡⟨ cong ((m * n) *_) (^-distribʳ-* m n p) ⟩
    (m * n) * ((m ^ p) * (n ^ p))
  ≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
    ((m * n) * (m ^ p)) * (n ^ p)
  ≡⟨ cong (_* (n ^ p)) (*-assoc m n (m ^ p)) ⟩
    (m * (n * (m ^ p))) * (n ^ p)
  ≡⟨ cong (λ {term → (m * term) * (n ^ p)}) (*-comm n (m ^ p)) ⟩
    (m * ((m ^ p) * n)) * (n ^ p)
  ≡⟨ cong (_* (n ^ p)) (sym (*-assoc m (m ^ p) n)) ⟩
    (m * (m ^ p) * n) * (n ^ p)
  ≡⟨ *-assoc (m * (m ^ p)) n (n ^ p) ⟩
    m * (m ^ p) * (n * (n ^ p))
  ≡⟨⟩
    (m ^ suc p) * (n ^ suc p)
  ∎

^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
^-*-assoc m n zero =
  begin
    (m ^ n) ^ zero
  ≡⟨⟩
    1
  ≡⟨⟩
    m ^ zero
  ≡⟨ cong (m ^_) (sym (*-absorbingʳ n)) ⟩
    m ^ (n * zero)
  ∎
^-*-assoc m n (suc p) =
  begin
    (m ^ n) ^ suc p
  ≡⟨⟩
    (m ^ n) * (m ^ n) ^ p
  ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n p) ⟩
    (m ^ n) * (m ^ (n * p))
  ≡⟨ cong (λ {term → (m ^ n) * (m ^ term)}) (*-comm n p) ⟩
    (m ^ n) * (m ^ (p * n))
  ≡⟨ sym (^-distribˡ-+-* m n (p * n)) ⟩
    m ^ (n + p * n)
  ≡⟨⟩
    m ^ (suc p * n)
  ≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
    m ^ (n * suc p)
  ∎

-- 9)
data Bin : Set where
  - : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc - = - I
inc (rest O) = rest I
inc (rest I) = (inc rest) O

to : ℕ → Bin
to zero = - O
to (suc n) = inc (to n)

from : Bin → ℕ
from - = 0
from (rest O) = 2 * from rest
from (rest I) = 2 * from rest + 1

bin-inverse-suc-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
bin-inverse-suc-inc - =
  begin
    from (inc -)
  ≡⟨⟩
    from (- I)
  ≡⟨⟩
    2 * from - + 1
  ≡⟨⟩
    2 * 0 + 1
  ≡⟨⟩
    0 + 1
  ≡⟨⟩
    1
  ≡⟨⟩
    suc 0
  ≡⟨⟩
    suc (from -)
  ∎
bin-inverse-suc-inc (b O) =
  begin
    from (inc (b O))
  ≡⟨⟩
    from (b I)
  ≡⟨⟩
    2 * from b + 1
  ≡⟨ +-comm (2 * from b) 1 ⟩
    suc (2 * from b)
  ≡⟨⟩
    suc (from (b O))
  ∎
bin-inverse-suc-inc (b I) =
  begin
    from (inc (b I))
  ≡⟨⟩
    from ((inc b) O)
  ≡⟨⟩
    2 * from (inc b)
  ≡⟨ cong (2 *_) (bin-inverse-suc-inc b) ⟩
    2 * suc (from b)
  ≡⟨ *-comm 2 (suc (from b)) ⟩
     suc (from b) * 2
  ≡⟨⟩
    (1 + from b) * 2
  ≡⟨ *-distrib-+ 1 (from b) 2 ⟩
    1 * 2 + from b * 2
  ≡⟨ cong (1 * 2 +_) (*-comm (from b) 2) ⟩
    1 * 2 + 2 * from b
  ≡⟨⟩
    2 + 2 * from b
  ≡⟨⟩
    suc 1 + 2 * from b
  ≡⟨⟩
    suc (1 + 2 * from b)
  ≡⟨ cong (suc) (+-comm 1 (2 * from b)) ⟩
    suc (2 * from b + 1)
  ≡⟨⟩
    suc (from (b I))
  ∎

-- ∀ (b : Bin) → to (from b) ≡ b
-- This does not work, as "from" is a surjective function. Both "-" and "- O" from Bin map into 0 from ℕ. Surjective functions have no left inverse.
-- 0 would have to map into two values, making the inverse of "from" not a function.

-- This works, as "to" is an injective function. 0 from ℕ maps (according to our definition) into "- O" in Bin. Injective functions have a left inverse.
-- "from" is a left inverse to "to". Note that there are infinitely many left inverses, since "-" could be mapped to any value in ℕ.
from∘to≡idₗ : ∀ (n : ℕ) → from (to n) ≡ n
from∘to≡idₗ zero =
  begin
    from (to zero)
  ≡⟨⟩
    from (- O)
  ≡⟨⟩
    2 * from -
  ≡⟨⟩
    2 * 0
  ≡⟨⟩
    zero
  ∎
from∘to≡idₗ (suc n) =
  begin
    from (to (suc n))
  ≡⟨⟩
    from (inc (to n))
  ≡⟨ bin-inverse-suc-inc (to n) ⟩
    suc (from (to n))
  ≡⟨ cong suc (from∘to≡idₗ n) ⟩
    suc n
  ∎

max_stars_repo_name: aronerben/agda-playground

max_issues_repo_name: aronerben/agda-playground

max_forks_repo_name: aronerben/agda-playground


text:
module LecDiff where

open import CS410-Prelude
open import CS410-Nat
open import LecSigma

data Data : Set1 where
  _+D_ _*D_  : Data -> Data -> Data
  label      : Set -> Data
  rec        : Data

infixr 4 _+D_
infixr 5 _*D_

[[_]] : Data -> Set -> Set
[[ S +D T ]]   R  = [[ S ]] R + [[ T ]] R
[[ S *D T ]]   R  = [[ S ]] R * [[ T ]] R
[[ label X ]]  R  = X
[[ rec ]]      R  = R

data Mu (D : Data) : Set where
  <_> : [[ D ]] (Mu D) -> Mu D

-- example: Natural Numbers

NAT : Data
NAT = label One +D rec

pattern ZERO  = < inl <> >
pattern SUC n = < inr n >

#_ : Nat -> Mu NAT
# zero = ZERO
# (suc n) = SUC (# n)

_+DN_ : Mu NAT -> Mu NAT -> Mu NAT
ZERO  +DN n  = n
SUC m +DN n  = SUC (m +DN n)

_<=DN_ : Mu NAT -> Mu NAT -> Two
ZERO   <=DN  n      =  tt
SUC m  <=DN  ZERO   =  ff
SUC m  <=DN  SUC n  =  m <=DN n

-- example: binary trees with nodes labelled by numbers

BST : Data
BST = label One  +D  rec *D label (Mu NAT) *D rec

pattern LEAF = < inl <> >
pattern NODE l n r = < inr (l , n , r) >

insert : Mu NAT -> Mu BST -> Mu BST
insert x LEAF          = NODE LEAF x LEAF
insert x (NODE l y r)  with x <=DN y
insert x (NODE l y r)  | tt = NODE (insert x l) y r
insert x (NODE l y r)  | ff = NODE l y (insert x r)

myBST : Mu BST
myBST = NODE (NODE (NODE LEAF (# 1) LEAF) (# 2) LEAF)
             (# 4)
             (NODE (NODE LEAF (# 5) LEAF) (# 7) LEAF)

myBST' : Mu BST
myBST' = insert (# 3) myBST

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

Diff : Data -> Data
Diff (S +D T)   = Diff S +D Diff T
Diff (S *D T)   = Diff S *D T  +D  S *D Diff T
Diff (label X)  = label Zero
Diff rec        = label One

plug : {R : Set}(D : Data) -> [[ Diff D ]] R -> R -> [[ D ]] R
plug (S +D T) (inl s') r = inl (plug S s' r)
plug (S +D T) (inr t') r = inr (plug T t' r)
plug (S *D T) (inl (s' , t)) r = plug S s' r , t
plug (S *D T) (inr (s , t')) r = s , plug T t' r
plug (label X) () r
plug rec       <> r = r

Shape : Data -> Set
Shape D = [[ D ]] One

Positions : (D : Data) -> Shape D -> Set
Positions (D +D E) (inl d) = Positions D d
Positions (D +D E) (inr e) = Positions E e
Positions (D *D E) (d , e) = Positions D d + Positions E e
Positions (label X) x = Zero
Positions rec <> = One