text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The partiality monad
------------------------------------------------------------------------

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

module Category.Monad.Partiality where

open import Codata.Musical.Notation
open import Category.Monad
open import Data.Bool.Base using (Bool; false; true)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product as Prod hiding (map)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Level using (_⊔_)
open import Relation.Binary as B hiding (Rel)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable hiding (map)
open import Relation.Nullary.Negation

------------------------------------------------------------------------
-- The partiality monad

data _⊥ {a} (A : Set a) : Set a where
  now   : (x : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

monad : ∀ {f} → RawMonad {f = f} _⊥
monad = record
  { return = now
  ; _>>=_  = _>>=_
  }
  where
  _>>=_ : ∀ {A B} → A ⊥ → (A → B ⊥) → B ⊥
  now x   >>= f = f x
  later x >>= f = later (♯ (♭ x >>= f))

private module M {f} = RawMonad (monad {f})

-- Non-termination.

never : ∀ {a} {A : Set a} → A ⊥
never = later (♯ never)

-- run x for n steps peels off at most n "later" constructors from x.

run_for_steps : ∀ {a} {A : Set a} → A ⊥ → ℕ → A ⊥
run now   x for n     steps = now x
run later x for zero  steps = later x
run later x for suc n steps = run ♭ x for n steps

-- Is the computation done?

isNow : ∀ {a} {A : Set a} → A ⊥ → Bool
isNow (now x)   = true
isNow (later x) = false

------------------------------------------------------------------------
-- Kinds

-- The partiality monad comes with two forms of equality (weak and
-- strong) and one ordering. Strong equality is stronger than the
-- ordering, which is stronger than weak equality.

-- The three relations are defined using a single data type, indexed
-- by a "kind".

data OtherKind : Set where
  geq weak : OtherKind

data Kind : Set where
  strong : Kind
  other  : (k : OtherKind) → Kind

-- Kind equality is decidable.

infix 4 _≟-Kind_

_≟-Kind_ : Decidable (_≡_ {A = Kind})
_≟-Kind_ strong       strong       = yes P.refl
_≟-Kind_ strong       (other k)    = no λ()
_≟-Kind_ (other k)    strong       = no λ()
_≟-Kind_ (other geq)  (other geq)  = yes P.refl
_≟-Kind_ (other geq)  (other weak) = no λ()
_≟-Kind_ (other weak) (other geq)  = no λ()
_≟-Kind_ (other weak) (other weak) = yes P.refl

-- A predicate which is satisfied only for equalities. Note that, for
-- concrete inputs, this predicate evaluates to ⊤ or ⊥.

Equality : Kind → Set
Equality k = False (k ≟-Kind other geq)

------------------------------------------------------------------------
-- Equality/ordering

module Equality {a ℓ} {A : Set a} -- The "return type".
                (_∼_ : A → A → Set ℓ) where

  -- The three relations.

  data Rel : Kind → A ⊥ → A ⊥ → Set (a ⊔ ℓ) where
    now    : ∀ {k x y} (x∼y : x ∼ y)                         → Rel k         (now   x) (now   y)
    later  : ∀ {k x y} (x∼y : ∞ (Rel k         (♭ x) (♭ y))) → Rel k         (later x) (later y)
    laterʳ : ∀ {x y}   (x≈y :    Rel (other weak) x  (♭ y) ) → Rel (other weak)     x  (later y)
    laterˡ : ∀ {k x y} (x∼y :    Rel (other k) (♭ x)    y  ) → Rel (other k) (later x)        y

  infix 4 _≅_ _≳_ _≲_ _≈_

  _≅_ : A ⊥ → A ⊥ → Set _
  _≅_ = Rel strong

  _≳_ : A ⊥ → A ⊥ → Set _
  _≳_ = Rel (other geq)

  _≲_ : A ⊥ → A ⊥ → Set _
  _≲_ = flip _≳_

  _≈_ : A ⊥ → A ⊥ → Set _
  _≈_ = Rel (other weak)

  -- x ⇓ y means that x terminates with y.

  infix 4 _⇓[_]_ _⇓_

  _⇓[_]_ : A ⊥ → Kind → A → Set _
  x ⇓[ k ] y = Rel k x (now y)

  _⇓_ : A ⊥ → A → Set _
  x ⇓ y = x ⇓[ other weak ] y

  -- x ⇓ means that x terminates.

  infix 4 _⇓

  _⇓ : A ⊥ → Set _
  x ⇓ = ∃ λ v → x ⇓ v

  -- x ⇑ means that x does not terminate.

  infix 4 _⇑[_] _⇑

  _⇑[_] : A ⊥ → Kind → Set _
  x ⇑[ k ] = Rel k x never

  _⇑ : A ⊥ → Set _
  x ⇑ = x ⇑[ other weak ]

------------------------------------------------------------------------
-- Lemmas relating the three relations

module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where

  open Equality _∼_ using (Rel; _≅_; _≳_; _≲_; _≈_; _⇓[_]_; _⇑[_])
  open Equality.Rel

  -- All relations include strong equality.

  ≅⇒ : ∀ {k} {x y : A ⊥} → x ≅ y → Rel k x y
  ≅⇒ (now x∼y)   = now x∼y
  ≅⇒ (later x≅y) = later (♯ ≅⇒ (♭ x≅y))

  -- The weak equality includes the ordering.

  ≳⇒ : ∀ {k} {x y : A ⊥} → x ≳ y → Rel (other k) x y
  ≳⇒ (now x∼y)    = now x∼y
  ≳⇒ (later  x≳y) = later (♯ ≳⇒ (♭ x≳y))
  ≳⇒ (laterˡ x≳y) = laterˡ  (≳⇒    x≳y )

  -- Weak equality includes the other relations.

  ⇒≈ : ∀ {k} {x y : A ⊥} → Rel k x y → x ≈ y
  ⇒≈ {strong}     = ≅⇒
  ⇒≈ {other geq}  = ≳⇒
  ⇒≈ {other weak} = id

  -- The relations agree for non-terminating computations.

  never⇒never : ∀ {k₁ k₂} {x : A ⊥} →
                Rel k₁ x never → Rel k₂ x never
  never⇒never (later  x∼never) = later (♯ never⇒never (♭ x∼never))
  never⇒never (laterʳ x≈never) =          never⇒never    x≈never
  never⇒never (laterˡ x∼never) = later (♯ never⇒never    x∼never)

  -- The "other" relations agree when the right-hand side is a value.

  now⇒now : ∀ {k₁ k₂} {x} {y : A} →
            Rel (other k₁) x (now y) → Rel (other k₂) x (now y)
  now⇒now (now x∼y)      = now x∼y
  now⇒now (laterˡ x∼now) = laterˡ (now⇒now x∼now)

------------------------------------------------------------------------
-- Later can be dropped

  laterʳ⁻¹ : ∀ {k} {x : A ⊥} {y} →
             Rel (other k) x (later y) → Rel (other k) x (♭ y)
  laterʳ⁻¹ (later  x∼y)  = laterˡ        (♭ x∼y)
  laterʳ⁻¹ (laterʳ x≈y)  = x≈y
  laterʳ⁻¹ (laterˡ x∼ly) = laterˡ (laterʳ⁻¹ x∼ly)

  laterˡ⁻¹ : ∀ {x} {y : A ⊥} → later x ≈ y → ♭ x ≈ y
  laterˡ⁻¹ (later  x≈y)  = laterʳ         (♭ x≈y)
  laterˡ⁻¹ (laterʳ lx≈y) = laterʳ (laterˡ⁻¹ lx≈y)
  laterˡ⁻¹ (laterˡ x≈y)  = x≈y

  later⁻¹ : ∀ {k} {x y : ∞ (A ⊥)} →
            Rel k (later x) (later y) → Rel k (♭ x) (♭ y)
  later⁻¹ (later  x∼y)  = ♭ x∼y
  later⁻¹ (laterʳ lx≈y) = laterˡ⁻¹ lx≈y
  later⁻¹ (laterˡ x∼ly) = laterʳ⁻¹ x∼ly

------------------------------------------------------------------------
-- The relations are equivalences or partial orders, given suitable
-- assumptions about the underlying relation

  module Equivalence where

    -- Reflexivity.

    refl : Reflexive _∼_ → ∀ {k} → Reflexive (Rel k)
    refl refl-∼ {x = now v}   = now refl-∼
    refl refl-∼ {x = later x} = later (♯ refl refl-∼)

    -- Symmetry.

    sym : Symmetric _∼_ → ∀ {k} → Equality k → Symmetric (Rel k)
    sym sym-∼ eq (now x∼y)           = now (sym-∼ x∼y)
    sym sym-∼ eq (later         x∼y) = later (♯ sym sym-∼ eq (♭ x∼y))
    sym sym-∼ eq (laterʳ        x≈y) = laterˡ  (sym sym-∼ eq    x≈y )
    sym sym-∼ eq (laterˡ {weak} x≈y) = laterʳ  (sym sym-∼ eq    x≈y )
    sym sym-∼ () (laterˡ {geq}  x≳y)

    -- Transitivity.

    private
     module Trans (trans-∼ : Transitive _∼_) where

      now-trans : ∀ {k x y} {v : A} →
                  Rel k x y → Rel k y (now v) → Rel k x (now v)
      now-trans (now    x∼y) (now    y∼z) = now (trans-∼        x∼y   y∼z)
      now-trans (laterˡ x∼y)         y∼z  = laterˡ (now-trans   x∼y   y∼z)
      now-trans         x∼ly (laterˡ y∼z) = now-trans (laterʳ⁻¹ x∼ly) y∼z

      mutual

        later-trans : ∀ {k} {x y : A ⊥} {z} →
                      Rel k x y → Rel k y (later z) → Rel k x (later z)
        later-trans (later  x∼y)        ly∼lz = later  (♯ trans (♭ x∼y) (later⁻¹  ly∼lz))
        later-trans (laterˡ x∼y)         y∼lz = later  (♯ trans    x∼y  (laterʳ⁻¹  y∼lz))
        later-trans (laterʳ x≈y)        ly≈lz =     later-trans    x≈y  (laterˡ⁻¹ ly≈lz)
        later-trans         x≈y  (laterʳ y≈z) = laterʳ (  trans    x≈y             y≈z )

        trans : ∀ {k} {x y z : A ⊥} → Rel k x y → Rel k y z → Rel k x z
        trans {z = now v}   x∼y y∼v  = now-trans   x∼y y∼v
        trans {z = later z} x∼y y∼lz = later-trans x∼y y∼lz

    open Trans public using (trans)

  -- All the relations are preorders.

  preorder : IsPreorder _≡_ _∼_ → Kind → Preorder _ _ _
  preorder pre k = record
    { Carrier    = A ⊥
    ; _≈_        = _≡_
    ; _∼_        = Rel k
    ; isPreorder = record
      { isEquivalence = P.isEquivalence
      ; reflexive     = refl′
      ; trans         = Equivalence.trans (IsPreorder.trans pre)
      }
    }
    where
    refl′ : ∀ {k} {x y : A ⊥} → x ≡ y → Rel k x y
    refl′ P.refl = Equivalence.refl (IsPreorder.refl pre)

  private
    preorder′ : IsEquivalence _∼_ → Kind → Preorder _ _ _
    preorder′ equiv =
      preorder (Setoid.isPreorder (record { isEquivalence = equiv }))

  -- The two equalities are equivalence relations.

  setoid : IsEquivalence _∼_ →
           (k : Kind) {eq : Equality k} → Setoid _ _
  setoid equiv k {eq} = record
    { Carrier       = A ⊥
    ; _≈_           = Rel k
    ; isEquivalence = record
      { refl  = Pre.refl
      ; sym   = Equivalence.sym (IsEquivalence.sym equiv) eq
      ; trans = Pre.trans
      }
    } where module Pre = Preorder (preorder′ equiv k)

  -- The order is a partial order, with strong equality as the
  -- underlying equality.

  ≳-poset : IsEquivalence _∼_ → Poset _ _ _
  ≳-poset equiv = record
    { Carrier        = A ⊥
    ; _≈_            = _≅_
    ; _≤_            = _≳_
    ; isPartialOrder = record
      { antisym    = antisym
      ; isPreorder = record
        { isEquivalence = S.isEquivalence
        ; reflexive     = ≅⇒
        ; trans         = Pre.trans
        }
      }
    }
    where
    module S   = Setoid (setoid equiv strong)
    module Pre = Preorder (preorder′ equiv (other geq))

    antisym : {x y : A ⊥} → x ≳ y → x ≲ y → x ≅ y
    antisym (now    x∼y)  (now    _)    = now x∼y
    antisym (later  x≳y)  (later  x≲y)  = later (♯ antisym        (♭ x≳y)         (♭ x≲y))
    antisym (later  x≳y)  (laterˡ x≲ly) = later (♯ antisym        (♭ x≳y)  (laterʳ⁻¹ x≲ly))
    antisym (laterˡ x≳ly) (later  x≲y)  = later (♯ antisym (laterʳ⁻¹ x≳ly)        (♭ x≲y))
    antisym (laterˡ x≳ly) (laterˡ x≲ly) = later (♯ antisym (laterʳ⁻¹ x≳ly) (laterʳ⁻¹ x≲ly))

  -- Equational reasoning.

  module Reasoning (isEquivalence : IsEquivalence _∼_) where

    private
      module Pre {k}  = Preorder (preorder′ isEquivalence k)
      module S {k eq} = Setoid (setoid isEquivalence k {eq})

    infix  3 _∎
    infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_

    _≡⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≡ y → Rel k y z → Rel k x z
    _ ≡⟨ P.refl ⟩ y∼z = y∼z

    _≅⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≅ y → Rel k y z → Rel k x z
    _ ≅⟨ x≅y ⟩ y∼z = Pre.trans (≅⇒ x≅y) y∼z

    _≳⟨_⟩_ : ∀ {k} x {y z : A ⊥} →
             x ≳ y → Rel (other k) y z → Rel (other k) x z
    _ ≳⟨ x≳y ⟩ y∼z = Pre.trans (≳⇒ x≳y) y∼z

    _≈⟨_⟩_ : ∀ x {y z : A ⊥} → x ≈ y → y ≈ z → x ≈ z
    _ ≈⟨ x≈y ⟩ y≈z = Pre.trans x≈y y≈z

    sym : ∀ {k} {eq : Equality k} {x y : A ⊥} →
          Rel k x y → Rel k y x
    sym {eq = eq} = S.sym {eq = eq}

    _∎ : ∀ {k} (x : A ⊥) → Rel k x x
    x ∎ = Pre.refl

------------------------------------------------------------------------
-- Lemmas related to now and never

  -- Now is not never.

  now≉never : ∀ {k} {x : A} → ¬ Rel k (now x) never
  now≉never (laterʳ hyp) = now≉never hyp

  -- A partial value is either now or never (classically, when the
  -- underlying relation is reflexive).

  now-or-never : Reflexive _∼_ →
                 ∀ {k} (x : A ⊥) →
                 ¬ ¬ ((∃ λ y → x ⇓[ other k ] y) ⊎ x ⇑[ other k ])
  now-or-never refl x = helper <$> excluded-middle
    where
    open RawMonad ¬¬-Monad

    not-now-is-never : (x : A ⊥) → (∄ λ y → x ≳ now y) → x ≳ never
    not-now-is-never (now x)   hyp with hyp (-, now refl)
    ... | ()
    not-now-is-never (later x) hyp =
      later (♯ not-now-is-never (♭ x) (hyp ∘ Prod.map id laterˡ))

    helper : Dec (∃ λ y → x ≳ now y) → _
    helper (yes ≳now) = inj₁ $ Prod.map id ≳⇒ ≳now
    helper (no  ≵now) = inj₂ $ ≳⇒ $ not-now-is-never x ≵now

------------------------------------------------------------------------
-- Map-like results

  -- Map.

  map : ∀ {_∼′_ : A → A → Set a} {k} →
        _∼′_ ⇒ _∼_ → Equality.Rel _∼′_ k ⇒ Equality.Rel _∼_ k
  map ∼′⇒∼ (now x∼y)    = now (∼′⇒∼ x∼y)
  map ∼′⇒∼ (later  x∼y) = later (♯ map ∼′⇒∼ (♭ x∼y))
  map ∼′⇒∼ (laterʳ x≈y) = laterʳ  (map ∼′⇒∼    x≈y)
  map ∼′⇒∼ (laterˡ x∼y) = laterˡ  (map ∼′⇒∼    x∼y)

  -- If a statement can be proved using propositional equality as the
  -- underlying relation, then it can also be proved for any other
  -- reflexive underlying relation.

  ≡⇒ : Reflexive _∼_ →
       ∀ {k x y} → Equality.Rel _≡_ k x y → Rel k x y
  ≡⇒ refl-∼ = map (flip (P.subst (_∼_ _)) refl-∼)

------------------------------------------------------------------------
-- Steps

  -- The number of later constructors (steps) in the terminating
  -- computation x.

  steps : ∀ {k} {x : A ⊥} {y} → x ⇓[ k ] y → ℕ
  steps                (now _)             = zero
  steps .{x = later x} (laterˡ {x = x} x⇓) = suc (steps {x = ♭ x} x⇓)

  module Steps {trans-∼ : Transitive _∼_} where

    left-identity :
      ∀ {k x y} {z : A}
      (x≅y : x ≅ y) (y⇓z : y ⇓[ k ] z) →
      steps (Equivalence.trans trans-∼ (≅⇒ x≅y) y⇓z) ≡ steps y⇓z
    left-identity (now _)     (now _)      = P.refl
    left-identity (later x≅y) (laterˡ y⇓z) =
      P.cong suc $ left-identity (♭ x≅y) y⇓z

    right-identity :
      ∀ {k x} {y z : A}
      (x⇓y : x ⇓[ k ] y) (y≈z : now y ⇓[ k ] z) →
      steps (Equivalence.trans trans-∼ x⇓y y≈z) ≡ steps x⇓y
    right-identity (now x∼y)    (now y∼z) = P.refl
    right-identity (laterˡ x∼y) (now y∼z) =
      P.cong suc $ right-identity x∼y (now y∼z)

------------------------------------------------------------------------
-- Laws related to bind

  -- Never is a left and right "zero" of bind.

  left-zero : {B : Set a} (f : B → A ⊥) → let open M in
              (never >>= f) ≅ never
  left-zero f = later (♯ left-zero f)

  right-zero : ∀ {B} (x : B ⊥) → let open M in
               (x >>= λ _ → never) ≅ never
  right-zero (later x) = later (♯ right-zero (♭ x))
  right-zero (now   x) = never≅never
    where never≅never : never ≅ never
          never≅never = later (♯ never≅never)

  -- Now is a left and right identity of bind (for a reflexive
  -- underlying relation).

  left-identity : Reflexive _∼_ →
                  ∀ {B} (x : B) (f : B → A ⊥) → let open M in
                  (now x >>= f) ≅ f x
  left-identity refl-∼ x f = Equivalence.refl refl-∼

  right-identity : Reflexive _∼_ →
                   (x : A ⊥) → let open M in
                   (x >>= now) ≅ x
  right-identity refl (now   x) = now refl
  right-identity refl (later x) = later (♯ right-identity refl (♭ x))

  -- Bind is associative (for a reflexive underlying relation).

  associative : Reflexive _∼_ →
                ∀ {B C} (x : C ⊥) (f : C → B ⊥) (g : B → A ⊥) →
                let open M in
                (x >>= f >>= g) ≅ (x >>= λ y → f y >>= g)
  associative refl-∼ (now x)   f g = Equivalence.refl refl-∼
  associative refl-∼ (later x) f g =
    later (♯ associative refl-∼ (♭ x) f g)

module _ {s ℓ} {A B : Set s}
         {_∼A_ : A → A → Set ℓ}
         {_∼B_ : B → B → Set ℓ} where

  open Equality
  private
    open module EqA = Equality _∼A_ using () renaming (_⇓[_]_ to _⇓[_]A_; _⇑[_] to _⇑[_]A)
    open module EqB = Equality _∼B_ using () renaming (_⇓[_]_ to _⇓[_]B_; _⇑[_] to _⇑[_]B)

  -- Bind preserves all the relations.

  _>>=-cong_ :
    ∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
    Rel _∼A_ k x₁ x₂ →
    (∀ {x₁ x₂} → x₁ ∼A x₂ → Rel _∼B_ k (f₁ x₁) (f₂ x₂)) →
    Rel _∼B_ k (x₁ >>= f₁) (x₂ >>= f₂)
  now    x₁∼x₂ >>=-cong f₁∼f₂ = f₁∼f₂ x₁∼x₂
  later  x₁∼x₂ >>=-cong f₁∼f₂ = later (♯ (♭ x₁∼x₂ >>=-cong f₁∼f₂))
  laterʳ x₁≈x₂ >>=-cong f₁≈f₂ = laterʳ (x₁≈x₂ >>=-cong f₁≈f₂)
  laterˡ x₁∼x₂ >>=-cong f₁∼f₂ = laterˡ (x₁∼x₂ >>=-cong f₁∼f₂)

  -- Inversion lemmas for bind.

  >>=-inversion-⇓ :
    Reflexive _∼A_ →
    ∀ {k} x {f : A → B ⊥} {y} → let open M in
    (x>>=f⇓ : (x >>= f) ⇓[ k ]B y) →
    ∃ λ z → ∃₂ λ (x⇓ : x ⇓[ k ]A z) (fz⇓ : f z ⇓[ k ]B y) →
                 steps x⇓ + steps fz⇓ ≡ steps x>>=f⇓
  >>=-inversion-⇓ refl (now x) fx⇓ =
    (x , now refl , fx⇓ , P.refl)
  >>=-inversion-⇓ refl (later x) (laterˡ x>>=f⇓) =
    Prod.map id (Prod.map laterˡ (Prod.map id (P.cong suc))) $
      >>=-inversion-⇓ refl (♭ x) x>>=f⇓

  >>=-inversion-⇑ : IsEquivalence _∼A_ →
                    ∀ {k} x {f : A → B ⊥} → let open M in
                    Rel _∼B_ (other k) (x >>= f) never →
                    ¬ ¬ (x ⇑[ other k ]A ⊎
                         ∃ λ y → x ⇓[ other k ]A y × f y ⇑[ other k ]B)
  >>=-inversion-⇑ eqA {k} x {f} ∼never =
    helper <$> now-or-never IsEqA.refl x
    where
    open RawMonad ¬¬-Monad using (_<$>_)
    open M using (_>>=_)
    open Reasoning eqA
    module IsEqA = IsEquivalence eqA

    k≳ = other geq

    is-never : ∀ {x y} →
               x ⇓[ k≳ ]A y → (x >>= f) ⇑[ k≳ ]B →
               ∃ λ z → (y ∼A z) × f z ⇑[ k≳ ]B
    is-never (now    x∼y)  = λ fx⇑ → (_ , IsEqA.sym x∼y , fx⇑)
    is-never (laterˡ ≳now) = is-never ≳now ∘ later⁻¹

    helper : (∃ λ y → x ⇓[ k≳ ]A y) ⊎ x ⇑[ k≳ ]A →
             x ⇑[ other k ]A ⊎
             ∃ λ y → x ⇓[ other k ]A y × f y ⇑[ other k ]B
    helper (inj₂ ≳never)     = inj₁ (≳⇒ ≳never)
    helper (inj₁ (y , ≳now)) with is-never ≳now (never⇒never ∼never)
    ... | (z , y∼z , fz⇑) = inj₂ (z , ≳⇒ (x     ≳⟨ ≳now ⟩
                                          now y ≅⟨ now y∼z ⟩
                                          now z ∎)
                                    , ≳⇒ fz⇑)

module _ {ℓ} {A B : Set ℓ} {_∼_ : B → B → Set ℓ} where

  open Equality

  -- A variant of _>>=-cong_.

  _≡->>=-cong_ :
    ∀ {k} {x₁ x₂ : A ⊥} {f₁ f₂ : A → B ⊥} → let open M in
    Rel _≡_ k x₁ x₂ →
    (∀ x → Rel _∼_ k (f₁ x) (f₂ x)) →
    Rel _∼_ k (x₁ >>= f₁) (x₂ >>= f₂)
  _≡->>=-cong_ {k} {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
    x₁≈x₂ >>=-cong λ {x} x≡x′ →
    P.subst (λ y → Rel _∼_ k (f₁ x) (f₂ y)) x≡x′ (f₁≈f₂ x)

------------------------------------------------------------------------
-- Productivity checker workaround

-- The monad can be awkward to use, due to the limitations of guarded
-- coinduction. The following code provides a (limited) workaround.

module Workaround {a} where

  infixl 1 _>>=_

  data _⊥P : Set a → Set (Level.suc a) where
    now   : ∀ {A} (x : A) → A ⊥P
    later : ∀ {A} (x : ∞ (A ⊥P)) → A ⊥P
    _>>=_ : ∀ {A B} (x : A ⊥P) (f : A → B ⊥P) → B ⊥P

  private

    data _⊥W : Set a → Set (Level.suc a) where
      now   : ∀ {A} (x : A) → A ⊥W
      later : ∀ {A} (x : A ⊥P) → A ⊥W

    mutual

      _>>=W_ : ∀ {A B} → A ⊥W → (A → B ⊥P) → B ⊥W
      now   x >>=W f = whnf (f x)
      later x >>=W f = later (x >>= f)

      whnf : ∀ {A} → A ⊥P → A ⊥W
      whnf (now   x) = now x
      whnf (later x) = later (♭ x)
      whnf (x >>= f) = whnf x >>=W f

  mutual

    private

      ⟦_⟧W : ∀ {A} → A ⊥W → A ⊥
      ⟦ now   x ⟧W = now x
      ⟦ later x ⟧W = later (♯ ⟦ x ⟧P)

    ⟦_⟧P : ∀ {A} → A ⊥P → A ⊥
    ⟦ x ⟧P = ⟦ whnf x ⟧W

  -- The definitions above make sense. ⟦_⟧P is homomorphic with
  -- respect to now, later and _>>=_.

  module Correct where

    private
      open module Eq {A : Set a} = Equality  {A = A} _≡_
      open module R  {A : Set a} = Reasoning (P.isEquivalence {A = A})

    now-hom : ∀ {A} (x : A) → ⟦ now x ⟧P ≅ now x
    now-hom x = now x ∎

    later-hom : ∀ {A} (x : ∞ (A ⊥P)) →
                ⟦ later x ⟧P ≅ later (♯ ⟦ ♭ x ⟧P)
    later-hom x = later (♯ (⟦ ♭ x ⟧P ∎))

    mutual

      private

        >>=-homW : ∀ {A B} (x : B ⊥W) (f : B → A ⊥P) →
                   ⟦ x >>=W f ⟧W ≅ M._>>=_ ⟦ x ⟧W (λ y → ⟦ f y ⟧P)
        >>=-homW (now   x) f = ⟦ f x ⟧P ∎
        >>=-homW (later x) f = later (♯ >>=-hom x f)

      >>=-hom : ∀ {A B} (x : B ⊥P) (f : B → A ⊥P) →
                ⟦ x >>= f ⟧P ≅ M._>>=_ ⟦ x ⟧P (λ y → ⟦ f y ⟧P)
      >>=-hom x f = >>=-homW (whnf x) f

------------------------------------------------------------------------
-- An alternative, but equivalent, formulation of equality/ordering

module AlternativeEquality {a ℓ} where

  private

    El : Setoid a ℓ → Set _
    El = Setoid.Carrier

    Eq : ∀ S → B.Rel (El S) _
    Eq = Setoid._≈_

  open Equality using (Rel)
  open Equality.Rel

  infix  4 _∣_≅P_ _∣_≳P_ _∣_≈P_
  infix  3 _∎
  infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≳⟨_⟩≅_ _≳⟨_⟩≈_ _≈⟨_⟩≅_ _≈⟨_⟩≲_
  infixl 1 _>>=_

  mutual

    -- Proof "programs".

    _∣_≅P_ : ∀ S → B.Rel (El S ⊥) _
    _∣_≅P_ = flip RelP strong

    _∣_≳P_ : ∀ S → B.Rel (El S ⊥) _
    _∣_≳P_ = flip RelP (other geq)

    _∣_≈P_ : ∀ S → B.Rel (El S ⊥) _
    _∣_≈P_ = flip RelP (other weak)

    data RelP S : Kind → B.Rel (El S ⊥) (Level.suc (a ⊔ ℓ)) where

      -- Congruences.

      now   : ∀ {k x y} (xRy : x ⟨ Eq S ⟩ y) → RelP S k (now x) (now y)
      later : ∀ {k x y} (x∼y : ∞ (RelP S k (♭ x) (♭ y))) →
              RelP S k (later x) (later y)
      _>>=_ : ∀ {S′ : Setoid a ℓ} {k} {x₁ x₂}
                {f₁ f₂ : El S′ → El S ⊥} →
              let open M in
              (x₁∼x₂ : RelP S′ k x₁ x₂)
              (f₁∼f₂ : ∀ {x y} → x ⟨ Eq S′ ⟩ y →
                       RelP S k (f₁ x) (f₂ y)) →
              RelP S k (x₁ >>= f₁) (x₂ >>= f₂)

      -- Ordering/weak equality.

      laterʳ : ∀   {x y} (x≈y : RelP S (other weak) x (♭ y)) → RelP S (other weak)     x (later y)
      laterˡ : ∀ {k x y} (x∼y : RelP S (other k) (♭ x)   y)  → RelP S (other k) (later x)       y

      -- Equational reasoning. Note that including full transitivity
      -- for weak equality would make _∣_≈P_ trivial; a similar
      -- problem applies to _∣_≳P_ (A ∣ never ≳P now x would be
      -- provable). Instead the definition of RelP includes limited
      -- notions of transitivity, similar to weak bisimulation up-to
      -- various things.

      _∎      : ∀ {k} x → RelP S k x x
      sym     : ∀ {k x y} {eq : Equality k} (x∼y : RelP S k x y) → RelP S k y x
      _≡⟨_⟩_  : ∀ {k} x {y z} (x≡y : x ≡ y) (y∼z : RelP S k y z) → RelP S k x z
      _≅⟨_⟩_  : ∀ {k} x {y z} (x≅y : S ∣ x ≅P y) (y∼z : RelP S k y z) → RelP S k x z
      _≳⟨_⟩_  : let open Equality (Eq S) in
                ∀     x {y z} (x≳y :     x ≳  y) (y≳z : S ∣ y ≳P z) → S ∣ x ≳P z
      _≳⟨_⟩≅_ : ∀     x {y z} (x≳y : S ∣ x ≳P y) (y≅z : S ∣ y ≅P z) → S ∣ x ≳P z
      _≳⟨_⟩≈_ : ∀     x {y z} (x≳y : S ∣ x ≳P y) (y≈z : S ∣ y ≈P z) → S ∣ x ≈P z
      _≈⟨_⟩≅_ : ∀     x {y z} (x≈y : S ∣ x ≈P y) (y≅z : S ∣ y ≅P z) → S ∣ x ≈P z
      _≈⟨_⟩≲_ : ∀     x {y z} (x≈y : S ∣ x ≈P y) (y≲z : S ∣ z ≳P y) → S ∣ x ≈P z

      -- If any of the following transitivity-like rules were added to
      -- RelP, then RelP and Rel would no longer be equivalent:
      --
      --   x ≳P y → y ≳P z → x ≳P z
      --   x ≳P y → y ≳  z → x ≳P z
      --   x ≲P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳P z → x ≈P z
      --   x ≲  y → y ≈P z → x ≈P z
      --   x ≈P y → y ≳  z → x ≈P z
      --   x ≈P y → y ≈P z → x ≈P z
      --   x ≈P y → y ≈  z → x ≈P z
      --   x ≈  y → y ≈P z → x ≈P z
      --
      -- The reason is that any of these rules would make it possible
      -- to derive that never and now x are related.

  -- RelP is complete with respect to Rel.

  complete : ∀ {S k} {x y : El S ⊥} →
             Equality.Rel (Eq S) k x y → RelP S k x y
  complete (now xRy)    = now xRy
  complete (later  x∼y) = later (♯ complete (♭ x∼y))
  complete (laterʳ x≈y) = laterʳ  (complete    x≈y)
  complete (laterˡ x∼y) = laterˡ  (complete    x∼y)

  -- RelP is sound with respect to Rel.

  private

    -- Proof WHNFs.

    data RelW S : Kind → B.Rel (El S ⊥) (Level.suc (a ⊔ ℓ)) where
      now    : ∀ {k x y} (xRy : x ⟨ Eq S ⟩ y)                 → RelW S k         (now   x) (now   y)
      later  : ∀ {k x y} (x∼y : RelP S k         (♭ x) (♭ y)) → RelW S k         (later x) (later y)
      laterʳ : ∀   {x y} (x≈y : RelW S (other weak) x  (♭ y)) → RelW S (other weak)     x  (later y)
      laterˡ : ∀ {k x y} (x∼y : RelW S (other k) (♭ x)    y)  → RelW S (other k) (later x)        y

    -- WHNFs can be turned into programs.

    program : ∀ {S k x y} → RelW S k x y → RelP S k x y
    program (now    xRy) = now xRy
    program (later  x∼y) = later (♯ x∼y)
    program (laterˡ x∼y) = laterˡ (program x∼y)
    program (laterʳ x≈y) = laterʳ (program x≈y)

    -- Lemmas for WHNFs.

    _>>=W_ : ∀ {A B k x₁ x₂} {f₁ f₂ : El A → El B ⊥} →
             RelW A k x₁ x₂ →
             (∀ {x y} → x ⟨ Eq A ⟩ y → RelW B k (f₁ x) (f₂ y)) →
             RelW B k (M._>>=_ x₁ f₁) (M._>>=_ x₂ f₂)
    now    xRy >>=W f₁∼f₂ = f₁∼f₂ xRy
    later  x∼y >>=W f₁∼f₂ = later  (x∼y >>= program ∘ f₁∼f₂)
    laterʳ x≈y >>=W f₁≈f₂ = laterʳ (x≈y >>=W f₁≈f₂)
    laterˡ x∼y >>=W f₁∼f₂ = laterˡ (x∼y >>=W f₁∼f₂)

    reflW : ∀ {S k} x → RelW S k x x
    reflW {S} (now   x) = now (Setoid.refl S)
    reflW     (later x) = later (♭ x ∎)

    symW : ∀ {S k x y} → Equality k → RelW S k x y → RelW S k y x
    symW {S} eq (now           xRy) = now (Setoid.sym S xRy)
    symW     eq (later         x≈y) = later  (sym {eq = eq} x≈y)
    symW     eq (laterʳ        x≈y) = laterˡ (symW      eq  x≈y)
    symW     eq (laterˡ {weak} x≈y) = laterʳ (symW      eq  x≈y)
    symW     () (laterˡ {geq}  x≈y)

    trans≅W : ∀ {S x y z} →
              RelW S strong x y → RelW S strong y z → RelW S strong x z
    trans≅W {S} (now   xRy) (now   yRz) = now (Setoid.trans S xRy yRz)
    trans≅W     (later x≅y) (later y≅z) = later (_ ≅⟨ x≅y ⟩ y≅z)

    trans≳-W : ∀ {S x y z} → let open Equality (Eq S) in
               x ≳ y → RelW S (other geq) y z → RelW S (other geq) x z
    trans≳-W {S} (now    xRy) (now    yRz) = now (Setoid.trans S xRy yRz)
    trans≳-W     (later  x≳y) (later  y≳z) = later (_ ≳⟨ ♭ x≳y ⟩ y≳z)
    trans≳-W     (later  x≳y) (laterˡ y≳z) = laterˡ (trans≳-W (♭ x≳y) y≳z)
    trans≳-W     (laterˡ x≳y)         y≳z  = laterˡ (trans≳-W    x≳y  y≳z)

    -- Strong equality programs can be turned into WHNFs.

    whnf≅ : ∀ {S x y} → S ∣ x ≅P y → RelW S strong x y
    whnf≅ (now xRy)           = now xRy
    whnf≅ (later x≅y)         = later (♭ x≅y)
    whnf≅ (x₁≅x₂ >>= f₁≅f₂)   = whnf≅ x₁≅x₂ >>=W λ xRy → whnf≅ (f₁≅f₂ xRy)
    whnf≅ (x ∎)               = reflW x
    whnf≅ (sym x≅y)           = symW _ (whnf≅ x≅y)
    whnf≅ (x ≡⟨ P.refl ⟩ y≅z) = whnf≅ y≅z
    whnf≅ (x ≅⟨ x≅y    ⟩ y≅z) = trans≅W (whnf≅ x≅y) (whnf≅ y≅z)

    -- More transitivity lemmas.

    _⟨_⟩≅_ : ∀ {S k} x {y z} →
             RelP S k x y → S ∣ y ≅P z → RelP S k x z
    _⟨_⟩≅_ {k = strong}     x x≅y y≅z = x ≅⟨ x≅y ⟩  y≅z
    _⟨_⟩≅_ {k = other geq}  x x≳y y≅z = x ≳⟨ x≳y ⟩≅ y≅z
    _⟨_⟩≅_ {k = other weak} x x≈y y≅z = x ≈⟨ x≈y ⟩≅ y≅z

    trans∼≅W : ∀ {S k x y z} →
               RelW S k x y → RelW S strong y z → RelW S k x z
    trans∼≅W {S} (now    xRy) (now   yRz) = now (Setoid.trans S xRy yRz)
    trans∼≅W     (later  x∼y) (later y≅z) = later (_ ⟨ x∼y ⟩≅ y≅z)
    trans∼≅W     (laterʳ x≈y) (later y≅z) = laterʳ (trans∼≅W x≈y (whnf≅ y≅z))
    trans∼≅W     (laterˡ x∼y)        y≅z  = laterˡ (trans∼≅W x∼y        y≅z)

    trans≅∼W : ∀ {S k x y z} →
               RelW S strong x y → RelW S k y z → RelW S k x z
    trans≅∼W {S} (now   xRy) (now     yRz) = now (Setoid.trans S xRy yRz)
    trans≅∼W     (later x≅y) (later   y∼z) = later (_ ≅⟨ x≅y ⟩ y∼z)
    trans≅∼W     (later x≅y) (laterˡ  y∼z) = laterˡ (trans≅∼W (whnf≅ x≅y) y∼z)
    trans≅∼W            x≅y  (laterʳ ly≈z) = laterʳ (trans≅∼W        x≅y ly≈z)

    -- Order programs can be turned into WHNFs.

    whnf≳ : ∀ {S x y} → S ∣ x ≳P y → RelW S (other geq) x y
    whnf≳ (now xRy)            = now xRy
    whnf≳ (later  x∼y)         = later (♭ x∼y)
    whnf≳ (laterˡ x≲y)         = laterˡ (whnf≳ x≲y)
    whnf≳ (x₁∼x₂ >>= f₁∼f₂)    = whnf≳ x₁∼x₂ >>=W λ xRy → whnf≳ (f₁∼f₂ xRy)
    whnf≳ (x ∎)                = reflW x
    whnf≳ (sym {eq = ()} x≅y)
    whnf≳ (x ≡⟨ P.refl ⟩  y≳z) = whnf≳ y≳z
    whnf≳ (x ≅⟨ x≅y    ⟩  y≳z) = trans≅∼W (whnf≅ x≅y) (whnf≳ y≳z)
    whnf≳ (x ≳⟨ x≳y    ⟩  y≳z) = trans≳-W        x≳y  (whnf≳ y≳z)
    whnf≳ (x ≳⟨ x≳y    ⟩≅ y≅z) = trans∼≅W (whnf≳ x≳y) (whnf≅ y≅z)

    -- Another transitivity lemma.

    trans≳≈W : ∀ {S x y z} →
               RelW S (other geq) x y → RelW S (other weak) y z →
               RelW S (other weak) x z
    trans≳≈W {S} (now    xRy) (now    yRz) = now (Setoid.trans S xRy yRz)
    trans≳≈W     (later  x≳y) (later  y≈z) = later (_ ≳⟨ x≳y ⟩≈ y≈z)
    trans≳≈W     (laterˡ x≳y)         y≈z  = laterˡ (trans≳≈W        x≳y  y≈z)
    trans≳≈W             x≳y  (laterʳ y≈z) = laterʳ (trans≳≈W        x≳y  y≈z)
    trans≳≈W     (later  x≳y) (laterˡ y≈z) = laterˡ (trans≳≈W (whnf≳ x≳y) y≈z)

    -- All programs can be turned into WHNFs.

    whnf : ∀ {S k x y} → RelP S k x y → RelW S k x y
    whnf (now xRy)            = now xRy
    whnf (later  x∼y)         = later     (♭ x∼y)
    whnf (laterʳ x≈y)         = laterʳ (whnf x≈y)
    whnf (laterˡ x∼y)         = laterˡ (whnf x∼y)
    whnf (x₁∼x₂ >>= f₁∼f₂)    = whnf x₁∼x₂ >>=W λ xRy → whnf (f₁∼f₂ xRy)
    whnf (x ∎)                = reflW x
    whnf (sym {eq = eq} x≈y)  = symW eq (whnf x≈y)
    whnf (x ≡⟨ P.refl ⟩  y∼z) = whnf y∼z
    whnf (x ≅⟨ x≅y    ⟩  y∼z) = trans≅∼W (whnf x≅y) (whnf y∼z)
    whnf (x ≳⟨ x≳y    ⟩  y≳z) = trans≳-W       x≳y  (whnf y≳z)
    whnf (x ≳⟨ x≳y    ⟩≅ y≅z) = trans∼≅W (whnf x≳y) (whnf y≅z)
    whnf (x ≳⟨ x≳y    ⟩≈ y≈z) = trans≳≈W (whnf x≳y) (whnf y≈z)
    whnf (x ≈⟨ x≈y    ⟩≅ y≅z) = trans∼≅W (whnf x≈y) (whnf y≅z)
    whnf (x ≈⟨ x≈y    ⟩≲ y≲z) = symW _ (trans≳≈W (whnf y≲z) (symW _ (whnf x≈y)))

  mutual

    -- Soundness.

    private

      soundW : ∀ {S k x y} → RelW S k x y → Rel (Eq S) k x y
      soundW (now    xRy) = now xRy
      soundW (later  x∼y) = later (♯ sound  x∼y)
      soundW (laterʳ x≈y) = laterʳ  (soundW x≈y)
      soundW (laterˡ x∼y) = laterˡ  (soundW x∼y)

    sound : ∀ {S k x y} → RelP S k x y → Rel (Eq S) k x y
    sound x∼y = soundW (whnf x∼y)

  -- RelP and Rel are equivalent (when the underlying relation is an
  -- equivalence).

  correct : ∀ {S k x y} → RelP S k x y ⇔ Rel (Eq S) k x y
  correct = equivalence sound complete

------------------------------------------------------------------------
-- Another lemma

-- Bind is "idempotent".

idempotent :
  ∀ {ℓ} {A : Set ℓ} (B : Setoid ℓ ℓ) →
  let open M; open Setoid B using (_≈_; Carrier); open Equality _≈_ in
  (x : A ⊥) (f : A → A → Carrier ⊥) →
  (x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳ (x >>= λ y′ → f y′ y′)
idempotent {A = A} B x f = sound (idem x)
  where
  open AlternativeEquality hiding (_>>=_)
  open M
  open Equality.Rel using (laterˡ)
  open Equivalence using (refl)

  idem : (x : A ⊥) →
         B ∣ (x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳P
             (x >>= λ y′ → f y′ y′)
  idem (now   x) = f x x ∎
  idem (later x) = later (♯ (
    (♭ x >>= λ y′ → later x >>= λ y″ → f y′ y″)  ≳⟨ (refl P.refl {x = ♭ x} ≡->>=-cong λ _ →
                                                     laterˡ (refl (Setoid.refl B))) ⟩
    (♭ x >>= λ y′ →     ♭ x >>= λ y″ → f y′ y″)  ≳⟨ idem (♭ x) ⟩≅
    (♭ x >>= λ y′ → f y′ y′)                     ∎))

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

private
 module Example where

  open Data.Nat
  open Workaround

  -- McCarthy's f91:

  f91′ : ℕ → ℕ ⊥P
  f91′ n with n ≤? 100
  ... | yes _ = later (♯ (f91′ (11 + n) >>= f91′))
  ... | no  _ = now (n ∸ 10)

  f91 : ℕ → ℕ ⊥
  f91 n = ⟦ f91′ n ⟧P


text:
open import Algebra using (CommutativeMonoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.PropositionalEquality using () renaming (cong to ≡-cong)

module AKS.Exponentiation {c ℓ} (M : CommutativeMonoid c ℓ) where

open import AKS.Nat using (ℕ; _+_; _<_)
open ℕ
open import AKS.Nat using (ℕ⁺; ℕ+; ⟅_⇓⟆)
open import AKS.Nat using (Acc; acc; <-well-founded)
open import AKS.Binary using (2*; 𝔹; 𝔹⁺; ⟦_⇑⟧; ⟦_⇓⟧; ⟦_⇑⟧⁺; ⟦_⇓⟧⁺; ℕ→𝔹→ℕ; ⌈log₂_⌉)
open 𝔹
open 𝔹⁺
open CommutativeMonoid M
  using (_≈_; isEquivalence; setoid; ε; _∙_; ∙-cong; ∙-congˡ; identityˡ; identityʳ; assoc; comm)
  renaming (Carrier to C)
open IsEquivalence isEquivalence using (refl; sym)
open import Relation.Binary.Reasoning.Setoid setoid

_^ⁱ_ : C → ℕ → C
x ^ⁱ zero = ε
x ^ⁱ suc n = x ∙ x ^ⁱ n

^ⁱ-homo : ∀ x n m → x ^ⁱ (n + m) ≈ x ^ⁱ n ∙ x ^ⁱ m
^ⁱ-homo x zero m = sym (identityˡ (x ^ⁱ m))
^ⁱ-homo x (suc n) m = begin
  x ∙ x ^ⁱ (n + m) ≈⟨ ∙-congˡ (^ⁱ-homo x n m) ⟩
  x ∙ (x ^ⁱ n ∙ x ^ⁱ m) ≈⟨ sym (assoc _ _ _) ⟩
  x ∙ x ^ⁱ n ∙ x ^ⁱ m ∎

∙-^ⁱ-dist : ∀ x y n → (x ∙ y) ^ⁱ n ≈ x ^ⁱ n ∙ y ^ⁱ n
∙-^ⁱ-dist x y zero = sym (identityˡ ε)
∙-^ⁱ-dist x y (suc n) = begin
  x ∙ y ∙ ((x ∙ y) ^ⁱ n) ≈⟨ ∙-congˡ (∙-^ⁱ-dist x y n) ⟩
  x ∙ y ∙ (x ^ⁱ n ∙ y ^ⁱ n) ≈⟨ assoc _ _ _ ⟩
  x ∙ (y ∙ (x ^ⁱ n ∙ y ^ⁱ n)) ≈⟨ ∙-congˡ (comm _ _) ⟩
  x ∙ (x ^ⁱ n ∙ y ^ⁱ n ∙ y) ≈⟨ ∙-congˡ (assoc _ _ _) ⟩
  x ∙ (x ^ⁱ n ∙ (y ^ⁱ n ∙ y)) ≈⟨ ∙-congˡ (∙-congˡ (comm _ _)) ⟩
  x ∙ (x ^ⁱ n ∙ (y ∙ y ^ⁱ n)) ≈⟨ sym (assoc _ _ _) ⟩
  x ∙ (x ^ⁱ n) ∙ (y ∙ (y ^ⁱ n)) ∎

_^ᵇ⁺_ : C → 𝔹⁺ → C
x ^ᵇ⁺ 𝕓1ᵇ = x
x ^ᵇ⁺ (b 0ᵇ) = (x ∙ x) ^ᵇ⁺ b
x ^ᵇ⁺ (b 1ᵇ) = x ∙ (x ∙ x) ^ᵇ⁺ b

_^ᵇ_ : C → 𝔹 → C
x ^ᵇ 𝕓0ᵇ = ε
x ^ᵇ (+ b) = x ^ᵇ⁺ b

_^⁺_ : C → ℕ⁺ → C
x ^⁺ n = x ^ᵇ⁺ ⟦ n ⇑⟧⁺

_^_ : C → ℕ → C
x ^ n = x ^ᵇ ⟦ n ⇑⟧

x^n≈x^ⁱn : ∀ x n → x ^ n ≈ x ^ⁱ n
x^n≈x^ⁱn x n = begin
  x ^ n ≈⟨ loop x ⟦ n ⇑⟧ ⟩
  x ^ⁱ ⟦ ⟦ n ⇑⟧ ⇓⟧ ≡⟨ ≡-cong (λ t → x ^ⁱ t) (ℕ→𝔹→ℕ n) ⟩
  x ^ⁱ n ∎
  where
  even : ∀ x b → (x ∙ x) ^ᵇ⁺ b ≈ x ^ⁱ 2* ⟦ b ⇓⟧⁺
  loop⁺ : ∀ x b → x ^ᵇ⁺ b ≈ x ^ⁱ ⟦ b ⇓⟧⁺

  even x b = begin
    (x ∙ x) ^ᵇ⁺ b ≈⟨ loop⁺ (x ∙ x) b ⟩
    (x ∙ x) ^ⁱ ⟦ b ⇓⟧⁺ ≈⟨ ∙-^ⁱ-dist x x ⟦ b ⇓⟧⁺ ⟩
    x ^ⁱ ⟦ b ⇓⟧⁺ ∙ x ^ⁱ ⟦ b ⇓⟧⁺ ≈⟨ sym (^ⁱ-homo x ⟦ b ⇓⟧⁺ ⟦ b ⇓⟧⁺) ⟩
    x ^ⁱ 2* ⟦ b ⇓⟧⁺ ∎

  loop⁺ x 𝕓1ᵇ = sym (identityʳ x)
  loop⁺ x (b 0ᵇ) = even x b
  loop⁺ x (b 1ᵇ) = ∙-congˡ (even x b)

  loop : ∀ x b → x ^ᵇ b ≈ x ^ⁱ ⟦ b ⇓⟧
  loop x 𝕓0ᵇ = refl
  loop x (+ b) = loop⁺ x b

^-homo : ∀ x n m → x ^ (n + m) ≈ x ^ n ∙ x ^ m
^-homo x n m = begin
  x ^ (n + m)     ≈⟨ x^n≈x^ⁱn x (n + m) ⟩
  x ^ⁱ (n + m)    ≈⟨ ^ⁱ-homo x n m ⟩
  x ^ⁱ n ∙ x ^ⁱ m ≈⟨ ∙-cong (sym (x^n≈x^ⁱn x n)) (sym (x^n≈x^ⁱn x m)) ⟩
  x ^ n ∙ x ^ m   ∎

x^n≈x^⁺n : ∀ x n → x ^ ⟅ n ⇓⟆ ≈ x ^⁺ n
x^n≈x^⁺n x (ℕ+ n) = refl

^-^⁺-homo : ∀ x n m → x ^ (n + ⟅ m ⇓⟆) ≈ x ^ n ∙ x ^⁺ m
^-^⁺-homo x n (ℕ+ m) = ^-homo x n (suc m)

ext: agda

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
{-# OPTIONS --cubical --safe --postfix-projections --guardedness #-}

open import Algebra
open import Prelude
open import Relation.Binary
open import WellFounded
open import Algebra.Monus
open import Data.Maybe

module Control.Comonad.IntervalHeap {s}
  (mon : TMAPOM s)
  (wf : WellFounded (TMAPOM._<_ mon))
  (cancel : Cancellativeˡ (TMAPOM._∙_ mon))
  where

open TMAPOM mon

mutual
  record Heap (A : Type a) : Type (s ℓ⊔ a) where
    inductive; constructor _◃_
    field
      hd : A
      tl : Next A

  record Next {a} (A : Type a) : Type (s ℓ⊔ a) where
    coinductive; constructor ⟪_⟫
    field next : Span A

  data Span {a} (A : Type a) : Type (s ℓ⊔ a) where
    [] : Span A
    until : (s : 𝑆) → (s≢ε : s ≢ ε) → (xs : Heap A) → Span A
open Heap public
open Next public

State : Type a → Type _
State A = 𝑆 → A × 𝑆

pop′ : (s : 𝑆) → Acc _<_ s → Heap A → A × 𝑆
pop′ s₂ a xs with xs .tl .next
pop′ s₂ a xs | [] = xs .hd , ε
pop′ s₂ a xs | until s₁ s₁≢ε ys with s₁ ≤? s₂
pop′ s₂ a xs | until s₁ s₁≢ε ys | no s₁≰s₂ = xs .hd , fst (<⇒≤ s₁≰s₂)
pop′ s₂ (acc wf) xs | until s₁ s₁≢ε ys | yes (k₁ , s₂≡s₁∙k₁) = pop′ k₁ (wf k₁ lemma) ys
  where
  lemma : k₁ < s₂
  lemma (k₂ , k₁≡s₂∙k₂) = s₁≢ε (zeroSumFree s₁ k₂ (sym (cancel k₁ _ _ p)))
    where
    p : k₁ ∙ ε ≡ k₁ ∙ (s₁ ∙ k₂)
    p = ∙ε k₁ ; k₁≡s₂∙k₂ ; cong (_∙ k₂) s₂≡s₁∙k₁ ; cong (_∙ k₂) (comm s₁ k₁) ; assoc k₁ s₁ k₂

pop : Heap A → State A
pop xs s = pop′ s (wf s) xs

mutual
  stepFrom : State A → (s : 𝑆) → Dec (s ≡ ε) → Span A
  stepFrom f s (yes p) = []
  stepFrom f s (no ¬p) = until s ¬p (tabulate (f ∘ (s ∙_)))

  tabulate : State A → Heap A
  tabulate f =
    let x , s = f ε
    in x ◃ λ where .next → stepFrom f s (s ≟ ε)

pop-ε : (xs : Heap A) (a : Acc _<_ ε) → pop′ ε a xs .fst ≡ xs .hd
pop-ε xs _ with xs .tl .next
pop-ε xs _ | [] = refl
pop-ε xs _ | until s s≢ε ys with s ≤? ε
pop-ε xs _ | until s s≢ε ys | no  s≰ε = refl
pop-ε xs _ | until s s≢ε ys | yes s≤ε = ⊥-elim (s≢ε (antisym s≤ε (positive s)))

-- slide : Heap A → Heap A
-- slide xs with xs .tl .next
-- slide xs | [] = xs
-- slide xs | [] = []

-- pop-tl : ∀ (x : A) s₁ (s₁≢ε : s₁ ≢ ε) xs s₂ → pop (x ◃ ⟪ until s₁ s₁≢ε xs ⟫) (s₁ ∙ s₂) ≡ pop xs s₂
-- pop-tl x s₁ s₁≢ε xs s₂ with s₁ ≤? (s₁ ∙ s₂)
-- pop-tl x s₁ s₁≢ε xs s₂ | no  s₁≰s₁∙s₂ = ⊥-elim (s₁≰s₁∙s₂ (s₂ , refl))
-- pop-tl x s₁ s₁≢ε xs s₂ | yes (k , s₁≤s₁∙s₂) =
--   let p = cancel s₁ s₂ k s₁≤s₁∙s₂
--   in {!!} ; cong (λ w → pop′ s₂ w xs) (isPropAcc {!!} (wf s₂))

-- seg-leftInv′ : (x : Heap A) → tabulate (pop x) ≡ x
-- seg-leftInv′ x = {!!}

-- mutual
--   seg-leftInv′ : (xs : Heap A) → stepFrom (pop xs) (pop xs ε .snd) (pop xs ε .snd ≟ ε) ≡ xs .tl .next
--   seg-leftInv′ (x ◃ xs) with pop (x ◃ xs) ε .snd ≟ ε
--   seg-leftInv′ (x ◃ xs) | yes s≡ε = {!!}
--   seg-leftInv′ (x ◃ xs) | no  s≢ε = {!!}

--   seg-leftInv : (x : Heap A) → tabulate (pop x) ≡ x
--   seg-leftInv (x ◃ xs) i .hd = pop-ε (x ◃ xs) (wf ε) i
--   seg-leftInv (x ◃ xs) i .tl .next = seg-leftInv′ (x ◃ xs) i

-- state-iso : Heap A ⇔ State A
-- state-iso .fun = pop
-- state-iso .inv = tabulate
-- state-iso .rightInv = {!!}
-- state-iso .leftInv  = {!!}

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- First-order logic
------------------------------------------------------------------------------

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

module FOL.README where

------------------------------------------------------------------------------
-- Description

-- Formalization of first-order logic using Agda's inductive notions.

------------------------------------------------------------------------------
-- Definition of the connectives and quantifiers
open import FOL.Base

-- Propositional logic theorems
open import FOL.ExclusiveDisjunction.TheoremsATP
open import FOL.ExclusiveDisjunction.TheoremsI
open import FOL.PropositionalLogic.TheoremsATP
open import FOL.PropositionalLogic.TheoremsI

-- First-order logic theorems
open import FOL.TheoremsATP
open import FOL.TheoremsI

-- Logical schemata
open import FOL.SchemataATP

-- Non-empty domains
open import FOL.NonEmptyDomain.TheoremsATP
open import FOL.NonEmptyDomain.TheoremsI

-- Non-intuitionistic logic theorems
open import FOL.NonIntuitionistic.TheoremsATP
open import FOL.NonIntuitionistic.TheoremsI

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
module NTypes.Contractible where

open import Equivalence
open import Types

isContr : ∀ {a} → Set a → Set _
isContr A = Σ A λ x → (y : A) → x ≡ y

contr→eq-⊤ : ∀ {a} {A : Set a} → isContr A → A ≃ ⊤
contr→eq-⊤ h
  = (λ _ → _)
  , ((λ _ → π₁ h) , λ _ → refl)
  , ((λ _ → π₁ h) , π₂ h)

eq-⊤→contr : ∀ {a} {A : Set a} → A ≃ ⊤ → isContr A
eq-⊤→contr (f , (g , α) , (h , β)) = h _ , β

pp-space-contr : ∀ {a} {A : Set a} (x : A) →
  isContr (Σ A λ y → x ≡ y)
pp-space-contr {A = A} x
  = (x , refl)
  , λ y → J
      (λ x y p → Id (Σ A (λ y → x ≡ y)) (x , refl) (y , p))
      (λ _ → refl) _ _ (π₂ y)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatMinusOne.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne.Base
open import Cubical.Reflection.StrictEquiv

-1+Path : ℕ ≡ ℕ₋₁
-1+Path = ua e
  where
  unquoteDecl e = declStrictEquiv e -1+_ 1+_

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{- Delay operator. -}
module TemporalOps.Delay where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.CartesianStrength
open import TemporalOps.Common
open import TemporalOps.Next

open import Data.Nat.Properties using (+-identityʳ ; +-comm ; +-assoc ; +-suc)
open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_ ; ≅-to-≡)
import Relation.Binary.PropositionalEquality as ≡
open import Data.Product
open import Data.Sum

-- General iteration
-- iter f n v = fⁿ(v)
iter : (τ -> τ) -> ℕ -> τ -> τ
iter F zero    A = A
iter F (suc n) A = F (iter F n A)

-- Multi-step delay
delay_by_ : τ -> ℕ -> τ
delay A by zero = A
delay A by suc n = ▹ (delay A by n)
infix 67 delay_by_

-- || Lemmas for the delay operator

-- Extra delay is cancelled out by extra waiting.
delay-+ : ∀{A} -> (n l k : ℕ)
          -> delay A by (n + l) at (n + k) ≡ delay A by l at k
delay-+ zero l k = refl
delay-+ (suc n) = delay-+ n

-- || Derived lemmas - they can all be expressed in terms of delay-+,
-- || but they are given explicitly for simplicity.

-- Delay by n is cancelled out by waiting n extra steps.
delay-+-left0 : ∀{A} -> (n k : ℕ)
              -> delay A by n at (n + k) ≡ A at k
delay-+-left0 zero k = refl
delay-+-left0 (suc n) k = delay-+-left0 n k

-- delay-+-left0 can be converted to delay-+ (heterogeneously).
delay-+-left0-eq : ∀{A : τ} -> (n l : ℕ)
                -> Proof-≡ (delay-+-left0 {A} n l) (delay-+ {A} n 0 l)
delay-+-left0-eq zero l v v′ pf = ≅-to-≡ pf
delay-+-left0-eq (suc n) l = delay-+-left0-eq n l

-- Extra delay by n steps is cancelled out by waiting for n steps.
delay-+-right0 : ∀{A} -> (n l : ℕ)
              -> delay A by (n + l) at n ≡ delay A by l at 0
delay-+-right0 zero l = refl
delay-+-right0 (suc n) l = delay-+-right0 n l

-- Delaying by n is the same as delaying by (n + 0)
delay-+0-left : ∀{A} -> (k n : ℕ)
             -> delay A by k at n ≡ delay A by (k + 0) at n
delay-+0-left {A} k n rewrite +-identityʳ k = refl

-- If the delay is greater than the wait amount, we get unit
delay-⊤ : ∀{A} -> (n k : ℕ)
       -> ⊤ at n ≡ delay A by (n + suc k) at n
delay-⊤ {A} n k = sym (delay-+-right0 n (suc k))

-- Associativity of arguments in the delay lemma
delay-assoc-sym : ∀{A} (n k l j : ℕ)
               -> Proof-≅ (sym (delay-+ {A} n (k + l) (k + j)))
                          (sym (delay-+ {A} (n + k) l j))
delay-assoc-sym zero zero l j v v′ pr = pr
delay-assoc-sym zero (suc k) l j = delay-assoc-sym zero k l j
delay-assoc-sym (suc n) k l j = delay-assoc-sym n k l j

-- Functor instance for delay
F-delay : ℕ -> Endofunctor ℝeactive
F-delay k = record
    { omap = delay_by k
    ; fmap = fmap-delay k
    ; fmap-id = λ {_ n a} -> fmap-delay-id k {_} {n} {a}
    ; fmap-∘ = fmap-delay-∘ k
    ; fmap-cong = fmap-delay-cong k
    }
    where
    -- Lifting of delay
    fmap-delay : {A B : τ} -> (k : ℕ) -> A ⇴ B -> delay A by k ⇴ delay B by k
    fmap-delay zero    f = f
    fmap-delay (suc k) f = Functor.fmap F-▹ (fmap-delay k f)
    -- Delay preserves identities
    fmap-delay-id : ∀ (k : ℕ) {A : τ} {n : ℕ} {a : (delay A by k) n}
             -> (fmap-delay k id at n) a ≡ a
    fmap-delay-id zero = refl
    fmap-delay-id (suc k) {A} {zero} = refl
    fmap-delay-id (suc k) {A} {suc n} = fmap-delay-id k {A} {n}
    -- Delay preserves composition
    fmap-delay-∘ : ∀ (k : ℕ) {A B C : τ} {g : B ⇴ C} {f : A ⇴ B} {n : ℕ} {a : (delay A by k) n}
            -> (fmap-delay k (g ∘ f) at n) a ≡ (fmap-delay k g ∘ fmap-delay k f at n) a
    fmap-delay-∘ zero = refl
    fmap-delay-∘ (suc k) {n = zero} = refl
    fmap-delay-∘ (suc k) {n = suc n} = fmap-delay-∘ k {n = n}
    -- Delay is congruent
    fmap-delay-cong : ∀ (k : ℕ) {A B : τ} {f f′ : A ⇴ B}
            -> ({n : ℕ} {a : A at n} -> f n a ≡ f′ n a)
            -> ({n : ℕ} {a : delay A by k at n}
                -> (fmap-delay k f at n) a
                 ≡ (fmap-delay k f′ at n) a)
    fmap-delay-cong zero e = e
    fmap-delay-cong (suc k) e {zero} = refl
    fmap-delay-cong (suc k) e {suc n} = fmap-delay-cong k e

-- || Lemmas for the interaction of fmap and delay-+

-- Lifted version of the delay-+ lemma
-- Arguments have different types, so we need heterogeneous equality
fmap-delay-+ : ∀ {A B : τ} {f : A ⇴ B} (n k l : ℕ)
            -> Fun-≅ (Functor.fmap (F-delay (n + k)) f at (n + l))
                     (Functor.fmap (F-delay      k)  f at      l)
fmap-delay-+ zero    k l v .v ≅.refl = ≅.refl
fmap-delay-+ (suc n) k l v  v′ pf       = fmap-delay-+ n k l v v′ pf

-- Specialised version with v of type delay A by (n + k) at (n + l)
-- Uses explicit rewrites and homogeneous equality
fmap-delay-+-n+k : ∀ {A B : τ} {f : A ⇴ B} (n k l : ℕ)
               -> (v : delay A by (n + k) at (n + l))
               -> rew (delay-+ n k l) ((Functor.fmap (F-delay (n + k)) f at (n + l)) v)
                ≡ (Functor.fmap (F-delay k) f at l) (rew (delay-+ n k l) v)
fmap-delay-+-n+k {A} n k l v =
    ≅-to-rew-≡ (fmap-delay-+ n k l v v′ v≅v′) (delay-+ n k l)
    where
    v′ : delay A by k at l
    v′ = rew (delay-+ n k l) v
    v≅v′ : v ≅ v′
    v≅v′ = rew-to-≅ (delay-+ n k l)

-- Lifted delay lemma with delay-+-left0
fmap-delay-+-n+0 : ∀ {A B : τ} {f : A ⇴ B} (n l : ℕ)
               -> {v : delay A by n at (n + l)}
               -> rew (delay-+-left0 n l) ((Functor.fmap (F-delay n) f at (n + l)) v)
                ≡ f l (rew (delay-+-left0 n l) v)
fmap-delay-+-n+0 {A} zero l = refl
fmap-delay-+-n+0 {A} (suc n) l = fmap-delay-+-n+0 n l

-- Specialised version with v of type delay A by k at l
-- Uses explicit rewrites and homogeneous equality
fmap-delay-+-k : ∀ {A B : τ} {f : A ⇴ B} (n k l : ℕ)
              ->(v : delay A by k at l)
              -> Functor.fmap (F-delay (n + k)) f (n + l) (rew (sym (delay-+ n k l)) v)
               ≡ rew (sym (delay-+ n k l)) (Functor.fmap (F-delay k) f l v)
fmap-delay-+-k {A} {B} {f} n k l v =
    sym (≅-to-rew-≡ (≅.sym (fmap-delay-+ n k l v′ v v≅v′)) (sym (delay-+ n k l)))
    where
    v′ : delay A by (n + k) at (n + l)
    v′ = rew (sym (delay-+ n k l)) v
    v≅v′ : v′ ≅ v
    v≅v′ = ≅.sym (rew-to-≅ (sym (delay-+ n k l)))

-- Delay is a Cartesian functor
F-cart-delay : ∀ k -> CartesianFunctor (F-delay k) ℝeactive-cart ℝeactive-cart
F-cart-delay k = record
    { u = u-delay k
    ; m = m-delay k
    ; m-nat₁ = m-nat₁-delay k
    ; m-nat₂ = m-nat₂-delay k
    ; associative = assoc-delay k
    ; unital-right = unit-right-delay k
    ; unital-left = λ {B} {n} {a} -> unit-left-delay k {B} {n} {a}
    }
    where
    open CartesianFunctor F-cart-▹

    u-delay : ∀ k -> ⊤ ⇴ delay ⊤ by k
    u-delay zero = λ n _ → top.tt
    u-delay (suc k) zero top.tt = top.tt
    u-delay (suc k) (suc n) top.tt = u-delay k n top.tt

    m-delay : ∀ k (A B : τ) -> (delay A by k ⊗ delay B by k) ⇴ delay (A ⊗ B) by k
    m-delay zero A B = λ n x → x
    m-delay (suc k) A B = Functor.fmap F-▹ (m-delay k A B) ∘ m (delay A by k) (delay B by k)

    m-nat₁-delay : ∀ k {A B C : τ} (f : A ⇴ B)
          -> Functor.fmap (F-delay k) (f * id) ∘ m-delay k A C
           ≈ m-delay k B C ∘ Functor.fmap (F-delay k) f * id
    m-nat₁-delay zero f = refl
    m-nat₁-delay (suc k) f {zero} = refl
    m-nat₁-delay (suc k) f {suc n} = m-nat₁-delay k f

    m-nat₂-delay : ∀ k {A B C : τ} (f : A ⇴ B)
          -> Functor.fmap (F-delay k) (id * f) ∘ m-delay k C A
           ≈ m-delay k C B ∘ id * Functor.fmap (F-delay k) f
    m-nat₂-delay zero f = refl
    m-nat₂-delay (suc k) f {zero} = refl
    m-nat₂-delay (suc k) f {suc n} = m-nat₂-delay k f

    assoc-delay : ∀ k {A B C : τ}
           -> m-delay k A (B ⊗ C) ∘ id * m-delay k B C ∘ assoc-right
            ≈ Functor.fmap (F-delay k) assoc-right ∘ m-delay k (A ⊗ B) C ∘ m-delay k A B * id
    assoc-delay zero = refl
    assoc-delay (suc k) {A} {B} {C} {zero} = refl
    assoc-delay (suc k) {A} {B} {C} {suc n} = assoc-delay k

    unit-right-delay : ∀ k {A : τ} ->
        Functor.fmap (F-delay k) unit-right ∘ m-delay k A ⊤ ∘ (id * u-delay k) ≈ unit-right
    unit-right-delay zero {A} {n} = refl
    unit-right-delay (suc k) {A} {zero} = refl
    unit-right-delay (suc k) {A} {suc n} = unit-right-delay k

    unit-left-delay : ∀ k {B : τ} ->
        Functor.fmap (F-delay k) unit-left ∘ m-delay k ⊤ B ∘ (u-delay k * id) ≈ unit-left
    unit-left-delay zero = refl
    unit-left-delay (suc k) {B} {zero} = refl
    unit-left-delay (suc k) {B} {suc n} = unit-left-delay k

m-delay-+-n+0 : ∀ {A B} k l {a b}
      -> (rew (delay-+-left0 k l)
          (CartesianFunctor.m (F-cart-delay k) A B (k + l) (a , b)))
       ≡ (rew (delay-+-left0 k l) a , rew (delay-+-left0 k l) b)
m-delay-+-n+0 zero l = refl
m-delay-+-n+0 (suc k) l = m-delay-+-n+0 k l

m-delay-+-sym : ∀ {A B} k l m{a b}
      -> rew (sym (delay-+ k m l))
            (CartesianFunctor.m (F-cart-delay m) A B l (a , b))
       ≡ CartesianFunctor.m (F-cart-delay (k + m)) A B (k + l)
            ((rew (sym (delay-+ k m l)) a) , (rew (sym (delay-+ k m l)) b))
m-delay-+-sym zero l m = refl
m-delay-+-sym (suc k) l m = m-delay-+-sym k l m

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:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.Truncation.Properties where
open import Cubical.Data.NatMinusOne
open import Cubical.HITs.Truncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.Equiv.PathSplit
open isPathSplitEquiv
open import Cubical.Modalities.Modality
open Modality

open import Cubical.Data.Empty.Base as ⊥ renaming (rec to ⊥rec ; elim to ⊥elim)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool
open import Cubical.Data.Unit
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification as Null hiding (rec; elim)

open import Cubical.HITs.PropositionalTruncation as PropTrunc
  renaming (∥_∥ to ∥_∥₁; ∣_∣ to ∣_∣₁; squash to squash₁) using ()
open import Cubical.HITs.SetTruncation       as SetTrunc  using (∥_∥₂; ∣_∣₂; squash₂)
open import Cubical.HITs.GroupoidTruncation  as GpdTrunc  using (∥_∥₃; ∣_∣₃; squash₃)
open import Cubical.HITs.2GroupoidTruncation as 2GpdTrunc using (∥_∥₄; ∣_∣₄; squash₄)

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

sphereFill : (n : ℕ) (f : S₊ n → A) → Type _
sphereFill {A = A} n f = Σ[ top ∈ A ] ((x : S₊ n) → top ≡ f x)

isSphereFilled : ℕ → Type ℓ → Type ℓ
isSphereFilled n A = (f : S₊ n → A) → sphereFill n f

isSphereFilled∥∥ : {n : ℕ} → isSphereFilled n (HubAndSpoke A n)
isSphereFilled∥∥ f = (hub f) , (spoke f)

isSphereFilled→isOfHLevel : (n : ℕ) → isSphereFilled n A → isOfHLevel (suc n) A
isSphereFilled→isOfHLevel {A = A} zero h x y = sym (snd (h f) true) ∙ snd (h f) false
  where
    f : Bool → A
    f true = x
    f false = y
isSphereFilled→isOfHLevel {A = A} (suc zero) h x y =
  J (λ y q → (p : x ≡ y) → q ≡ p) (helper x)
  where
  helper : (x : A) (p : x ≡ x) → refl ≡ p
  helper x p i j =
    hcomp (λ k → λ { (i = i0) → h S¹→A .snd base k
                   ; (i = i1) → p j
                   ; (j = i0) → h S¹→A .snd base (i ∨ k)
                   ; (j = i1) → h S¹→A .snd base (i ∨ k)})
          (h S¹→A .snd (loop j) i)
    where
    S¹→A : S¹ → A
    S¹→A base = x
    S¹→A (loop i) = p i
isSphereFilled→isOfHLevel {A = A} (suc (suc n)) h x y =
  isSphereFilled→isOfHLevel (suc n) (helper h x y)
  where
    helper : {n : ℕ} → isSphereFilled (suc (suc n)) A → (x y : A) → isSphereFilled (suc n) (x ≡ y)
    helper {n = n} h x y f = sym (snd (h f') north) ∙ (snd (h f') south) , r
      where
        f' : Susp (S₊ (suc n)) → A
        f' north = x
        f' south = y
        f' (merid u i) = f u i

        r : (s : S₊ (suc n)) → sym (snd (h f') north) ∙ (snd (h f') south) ≡ f s
        r s i j = hcomp
                    (λ k →
                       λ { (i = i1) → snd (h f') (merid s j) k
                         ; (j = i0) → snd (h f') north (k ∨ (~ i))
                         ; (j = i1) → snd (h f') south k
                         })
                  (snd (h f') north (~ i ∧ ~ j))

isOfHLevel→isSphereFilled : (n : ℕ) → isOfHLevel (suc n) A → isSphereFilled n A
isOfHLevel→isSphereFilled zero h f = (f true) , (λ _ → h _ _)
isOfHLevel→isSphereFilled {A = A} (suc zero) h f = (f base) , toPropElim (λ _ → h _ _) refl
isOfHLevel→isSphereFilled {A = A} (suc (suc n)) h =
  helper λ x y → isOfHLevel→isSphereFilled (suc n) (h x y)
  where
    helper : {n : ℕ} → ((x y : A) → isSphereFilled (suc n) (x ≡ y))
                     → isSphereFilled (suc (suc n)) A
    helper {n = n} h f = f north , r
      where
      r : (x : S₊ (suc (suc n))) → f north ≡ f x
      r north = refl
      r south = h (f north) (f south) (λ x → cong f (merid x)) .fst
      r (merid x i) j = hcomp (λ k → λ { (i = i0) → f north
                                       ; (i = i1) → h (f north) (f south) (λ x → cong f (merid x)) .snd x (~ k) j
                                       ; (j = i0) → f north
                                       ; (j = i1) → f (merid x i) }) (f (merid x (i ∧ j)))

isOfHLevelTrunc : (n : ℕ) → isOfHLevel n (∥ A ∥ n)
isOfHLevelTrunc zero = isOfHLevelUnit* 0
isOfHLevelTrunc (suc n) = isSphereFilled→isOfHLevel n isSphereFilled∥∥

rec : {n : HLevel}
      {B : Type ℓ'} →
      isOfHLevel (suc n) B →
      (A → B) →
      hLevelTrunc (suc n) A →
      B
rec h g ∣ x ∣ = g x
rec {n = n} {B = B} hB g (hub f) = isOfHLevel→isSphereFilled n hB (λ x → rec hB g (f x)) .fst
rec {n = n} hB g (spoke f x i) =
  isOfHLevel→isSphereFilled n hB (λ x → rec hB g (f x)) .snd x i

elim : {n : ℕ}
      {B : ∥ A ∥ (suc n) → Type ℓ'}
      (hB : (x : ∥ A ∥ (suc n)) → isOfHLevel (suc n) (B x))
      (g : (a : A) → B (∣ a ∣))
      (x : ∥ A ∥ (suc n)) →
      B x
elim hB g (∣ a ∣ ) = g a
elim {B = B} hB g (hub f) =
  isOfHLevel→isSphereFilled _ (hB (hub f)) (λ x → subst B (sym (spoke f x)) (elim hB g (f x)) ) .fst
elim {B = B} hB g (spoke f x i) =
  toPathP {A = λ i → B (spoke f x (~ i))}
    (sym (isOfHLevel→isSphereFilled _ (hB (hub f)) (λ x → subst B (sym (spoke f x)) (elim hB g (f x))) .snd x))
    (~ i)

elim2 : {n : ℕ}
       {B : ∥ A ∥ (suc n) → ∥ A ∥ (suc n) → Type ℓ'}
       (hB : ((x y : ∥ A ∥ (suc n)) → isOfHLevel (suc n) (B x y)))
       (g : (a b : A) → B ∣ a ∣ ∣ b ∣)
       (x y : ∥ A ∥ (suc n)) →
       B x y
elim2 {n = n} hB g = elim (λ _ → isOfHLevelΠ (suc n) (λ _ → hB _ _)) λ a →
                    elim (λ _ → hB _ _) (λ b → g a b)

elim3 : {n : ℕ}
       {B : (x y z : ∥ A ∥ (suc n)) → Type ℓ'}
       (hB : ((x y z : ∥ A ∥ (suc n)) → isOfHLevel (suc n) (B x y z)))
       (g : (a b c : A) → B (∣ a ∣) ∣ b ∣ ∣ c ∣)
       (x y z : ∥ A ∥ (suc n)) →
       B x y z
elim3 {n = n} hB g = elim2 (λ _ _ → isOfHLevelΠ (suc n) (hB _ _)) λ a b →
                    elim (λ _ → hB _ _ _) (λ c → g a b c)

isContr→isContr∥ : (n : ℕ) → isContr A → isContr (∥ A ∥ n)
isContr→isContr∥ zero _ = tt* , (λ _ _ → tt*)
isContr→isContr∥ (suc n) contr = ∣ fst contr ∣ , (elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
                                                      (λ a i → ∣ snd contr a i ∣))

isOfHLevelMin→isOfHLevel : {n m : ℕ} → isOfHLevel (min n m) A → isOfHLevel n A × isOfHLevel m A
isOfHLevelMin→isOfHLevel {n = zero} {m = m} h = h , isContr→isOfHLevel m h
isOfHLevelMin→isOfHLevel {n = suc n} {m = zero} h = (isContr→isOfHLevel (suc n) h) , h
isOfHLevelMin→isOfHLevel {A = A} {n = suc n} {m = suc m} h =
    subst (λ x → isOfHLevel x A) (helper n m)
          (isOfHLevelPlus (suc n ∸ (suc (min n m))) h)
  , subst (λ x → isOfHLevel x A) ((λ i → m ∸ (minComm n m i) + suc (minComm n m i)) ∙ helper m n)
          (isOfHLevelPlus (suc m ∸ (suc (min n m))) h)
  where
  helper : (n m : ℕ) → n ∸ min n m + suc (min n m) ≡ suc n
  helper zero zero = refl
  helper zero (suc m) = refl
  helper (suc n) zero = cong suc (+-comm n 1)
  helper (suc n) (suc m) = +-suc _ _ ∙ cong suc (helper n m)

ΣTruncElim : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {n m : ℕ}
              {B : (x : ∥ A ∥ (suc n)) → Type ℓ'}
              {C : (Σ[ a ∈ (∥ A ∥ (suc n)) ] (∥ B a ∥ (suc m))) → Type ℓ''}
            → ((x : (Σ[ a ∈ (∥ A ∥ (suc n)) ] (∥ B a ∥ (suc m)))) → isOfHLevel (min (suc n) (suc m)) (C x))
            → ((a : A) (b : B (∣ a ∣)) → C (∣ a ∣ , ∣ b ∣))
            → (x : (Σ[ a ∈ (∥ A ∥ (suc n)) ] (∥ B a ∥ (suc m)))) → (C x)
ΣTruncElim {n = n} {m = m} {B = B} {C = C} hB g (a , b) =
  elim {B = λ a → (b :  (∥ B a ∥ (suc m))) → C (a , b)}
       (λ x → isOfHLevelΠ (suc n) λ b → isOfHLevelMin→isOfHLevel (hB (x , b)) .fst )
       (λ a → elim (λ _ → isOfHLevelMin→isOfHLevel (hB (∣ a ∣ , _)) .snd) λ b → g a b)
       a b

truncIdempotentIso : (n : ℕ) → isOfHLevel n A → Iso (∥ A ∥ n) A
truncIdempotentIso zero hA = isContr→Iso (isOfHLevelUnit* 0) hA
Iso.fun (truncIdempotentIso (suc n) hA) = rec hA λ a → a
Iso.inv (truncIdempotentIso (suc n) hA) = ∣_∣
Iso.rightInv (truncIdempotentIso (suc n) hA) _ = refl
Iso.leftInv (truncIdempotentIso (suc n) hA) = elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ _ → refl

truncIdempotent≃ : (n : ℕ) → isOfHLevel n A → ∥ A ∥ n ≃ A
truncIdempotent≃ n hA = isoToEquiv (truncIdempotentIso n hA)

truncIdempotent : (n : ℕ) → isOfHLevel n A → ∥ A ∥ n ≡ A
truncIdempotent n hA = ua (truncIdempotent≃ n hA)

HLevelTruncModality : ∀ {ℓ} (n : HLevel) → Modality ℓ
isModal       (HLevelTruncModality n) = isOfHLevel n
isModalIsProp (HLevelTruncModality n) = isPropIsOfHLevel n
◯             (HLevelTruncModality n) = hLevelTrunc n
◯-isModal     (HLevelTruncModality n) = isOfHLevelTrunc n
η (HLevelTruncModality zero) _ = tt*
η (HLevelTruncModality (suc n)) = ∣_∣
◯-elim (HLevelTruncModality zero) cB _ tt* = cB tt* .fst
◯-elim (HLevelTruncModality (suc n)) = elim
◯-elim-β (HLevelTruncModality zero) cB f a = cB tt* .snd (f a)
◯-elim-β (HLevelTruncModality (suc n)) = λ _ _ _ → refl
◯-=-isModal (HLevelTruncModality zero) x y = (isOfHLevelUnit* 1 x y) , (isOfHLevelUnit* 2 x y _)
◯-=-isModal (HLevelTruncModality (suc n)) = isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n))

-- universal property

univTrunc : ∀ {ℓ} (n : HLevel) {B : TypeOfHLevel ℓ n} → Iso (hLevelTrunc n A → B .fst) (A → B .fst)
univTrunc zero {B , lev} = isContr→Iso (isOfHLevelΠ 0 (λ _ → lev)) (isOfHLevelΠ 0 λ _ → lev)
Iso.fun (univTrunc (suc n) {B , lev}) g a = g ∣ a ∣
Iso.inv (univTrunc (suc n) {B , lev}) = rec lev
Iso.rightInv (univTrunc (suc n) {B , lev}) b = refl
Iso.leftInv (univTrunc (suc n) {B , lev}) b = funExt (elim (λ x → isOfHLevelPath _ lev _ _)
                                                            λ a → refl)

-- functorial action

map : {n : HLevel} {B : Type ℓ'} (g : A → B)
  → hLevelTrunc n A → hLevelTrunc n B
map {n = zero} g = λ _ → tt*
map {n = suc n} g = rec (isOfHLevelTrunc _) (λ a → ∣ g a ∣)

mapCompIso : {n : HLevel} {B : Type ℓ'} → (Iso A B) → Iso (hLevelTrunc n A) (hLevelTrunc n B)
mapCompIso {n = zero} {B} _ = isContr→Iso (isOfHLevelUnit* 0) (isOfHLevelUnit* 0)
Iso.fun (mapCompIso {n = (suc n)} g) = map (Iso.fun g)
Iso.inv (mapCompIso {n = (suc n)} g) = map (Iso.inv g)
Iso.rightInv (mapCompIso {n = (suc n)} g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ b → cong ∣_∣ (Iso.rightInv g b)
Iso.leftInv (mapCompIso {n = (suc n)} g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ a → cong ∣_∣ (Iso.leftInv g a)

mapId : {n : HLevel} → ∀ t → map {n = n} (idfun A) t ≡ t
mapId {n = 0} tt* = refl
mapId {n = (suc n)} =
  elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) (λ _ → refl)

-- equivalences to prop/set/groupoid truncations

propTruncTrunc1Iso : Iso ∥ A ∥₁ (∥ A ∥ 1)
Iso.fun propTruncTrunc1Iso = PropTrunc.rec (isOfHLevelTrunc 1) ∣_∣
Iso.inv propTruncTrunc1Iso = rec squash₁ ∣_∣₁
Iso.rightInv propTruncTrunc1Iso = elim (λ _ → isOfHLevelPath 1 (isOfHLevelTrunc 1) _ _) (λ _ → refl)
Iso.leftInv propTruncTrunc1Iso = PropTrunc.elim (λ _ → isOfHLevelPath 1 squash₁ _ _) (λ _ → refl)

propTrunc≃Trunc1 : ∥ A ∥₁ ≃ ∥ A ∥ 1
propTrunc≃Trunc1 = isoToEquiv propTruncTrunc1Iso

propTrunc≡Trunc1 : ∥ A ∥₁ ≡ ∥ A ∥ 1
propTrunc≡Trunc1 = ua propTrunc≃Trunc1

setTruncTrunc2Iso : Iso ∥ A ∥₂ (∥ A ∥ 2)
Iso.fun setTruncTrunc2Iso = SetTrunc.rec (isOfHLevelTrunc 2) ∣_∣
Iso.inv setTruncTrunc2Iso = rec squash₂ ∣_∣₂
Iso.rightInv setTruncTrunc2Iso = elim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _) (λ _ → refl)
Iso.leftInv setTruncTrunc2Iso = SetTrunc.elim (λ _ → isOfHLevelPath 2 squash₂ _ _) (λ _ → refl)

setTrunc≃Trunc2 : ∥ A ∥₂ ≃ ∥ A ∥ 2
setTrunc≃Trunc2 = isoToEquiv setTruncTrunc2Iso

propTrunc≡Trunc2 : ∥ A ∥₂ ≡ ∥ A ∥ 2
propTrunc≡Trunc2 = ua setTrunc≃Trunc2

groupoidTruncTrunc3Iso : Iso ∥ A ∥₃ (∥ A ∥ 3)
Iso.fun groupoidTruncTrunc3Iso = GpdTrunc.rec (isOfHLevelTrunc 3) ∣_∣
Iso.inv groupoidTruncTrunc3Iso = rec squash₃ ∣_∣₃
Iso.rightInv groupoidTruncTrunc3Iso = elim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) (λ _ → refl)
Iso.leftInv groupoidTruncTrunc3Iso = GpdTrunc.elim (λ _ → isOfHLevelPath 3 squash₃ _ _) (λ _ → refl)

groupoidTrunc≃Trunc3 : ∥ A ∥₃ ≃ ∥ A ∥ 3
groupoidTrunc≃Trunc3 = isoToEquiv groupoidTruncTrunc3Iso

groupoidTrunc≡Trunc3 : ∥ A ∥₃ ≡ ∥ A ∥ 3
groupoidTrunc≡Trunc3 = ua groupoidTrunc≃Trunc3

2GroupoidTruncTrunc4Iso : Iso ∥ A ∥₄ (∥ A ∥ 4)
Iso.fun 2GroupoidTruncTrunc4Iso = 2GpdTrunc.rec (isOfHLevelTrunc 4) ∣_∣
Iso.inv 2GroupoidTruncTrunc4Iso = rec squash₄ ∣_∣₄
Iso.rightInv 2GroupoidTruncTrunc4Iso = elim (λ _ → isOfHLevelPath 4 (isOfHLevelTrunc 4) _ _) (λ _ → refl)
Iso.leftInv 2GroupoidTruncTrunc4Iso = 2GpdTrunc.elim (λ _ → isOfHLevelPath 4 squash₄ _ _) (λ _ → refl)

2GroupoidTrunc≃Trunc4 : ∥ A ∥₄ ≃ ∥ A ∥ 4
2GroupoidTrunc≃Trunc4 = isoToEquiv 2GroupoidTruncTrunc4Iso

2GroupoidTrunc≡Trunc4 : ∥ A ∥₄ ≡ ∥ A ∥ 4
2GroupoidTrunc≡Trunc4 = ua 2GroupoidTrunc≃Trunc4

isContr→isContrTrunc : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isContr A → isContr (hLevelTrunc n A)
isContr→isContrTrunc zero contr = isOfHLevelUnit* 0
isContr→isContrTrunc (suc n) contr =
  ∣ fst contr ∣ , (elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → cong ∣_∣ (snd contr a))

truncOfProdIso : (n : ℕ) → Iso (hLevelTrunc n (A × B)) (hLevelTrunc n A × hLevelTrunc n B)
truncOfProdIso 0 = isContr→Iso (isOfHLevelUnit* 0) (isOfHLevel× 0 (isOfHLevelUnit* 0) (isOfHLevelUnit* 0))
Iso.fun (truncOfProdIso (suc n)) = rec (isOfHLevelΣ (suc n) (isOfHLevelTrunc (suc n)) (λ _ → isOfHLevelTrunc (suc n))) λ {(a , b) → ∣ a ∣ , ∣ b ∣}
Iso.inv (truncOfProdIso (suc n)) (a , b) = rec (isOfHLevelTrunc (suc n))
                                          (λ a → rec (isOfHLevelTrunc (suc n))
                                                      (λ b → ∣ a , b ∣)
                                                       b)
                                          a
Iso.rightInv (truncOfProdIso (suc n)) (a , b) =
  elim {B = λ a → Iso.fun (truncOfProdIso (suc n)) (Iso.inv (truncOfProdIso (suc n)) (a , b)) ≡ (a , b)}
       (λ _ → isOfHLevelPath (suc n) (isOfHLevelΣ (suc n) (isOfHLevelTrunc (suc n)) (λ _ → isOfHLevelTrunc (suc n))) _ _)
       (λ a → elim {B = λ b → Iso.fun (truncOfProdIso (suc n)) (Iso.inv (truncOfProdIso (suc n)) (∣ a ∣ , b)) ≡ (∣ a ∣ , b)}
                    (λ _ → isOfHLevelPath (suc n) (isOfHLevelΣ (suc n) (isOfHLevelTrunc (suc n)) (λ _ → isOfHLevelTrunc (suc n))) _ _)
                    (λ b → refl) b) a
Iso.leftInv (truncOfProdIso (suc n)) = elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → refl

---- ∥ Ω A ∥ ₙ ≡ Ω ∥ A ∥ₙ₊₁  ----

  {- Proofs of Theorem 7.3.12. and Corollary 7.3.13. in the HoTT book  -}

module ΩTrunc {X : Type ℓ} {n : HLevel} where
  {- We define the fibration P to show a more general result  -}
  P : ∥ X ∥ (2 + n) → ∥ X ∥ (2 + n) → Type ℓ
  P x y =  elim2 (λ _ _  → isOfHLevelTypeOfHLevel (suc n))
                 (λ a b → ∥ a ≡ b ∥ (suc n) , isOfHLevelTrunc (suc n)) x y .fst

  {- We will need P to be of hLevel n + 3  -}
  hLevelP : (a b : ∥ X ∥ (2 + n)) → isOfHLevel (2 + n) (P a b)
  hLevelP  =
    elim2 (λ x y → isProp→isOfHLevelSuc (suc n) (isPropIsOfHLevel (2 + n)))
          (λ a b → isOfHLevelSuc (suc n) (isOfHLevelTrunc (suc n)))

  {- decode function from P x y to x ≡ y -}
  decode-fun : (x y : ∥ X ∥ (2 + n)) → P x y → x ≡ y
  decode-fun =
    elim2 (λ u v → isOfHLevelΠ (2 + n)(λ _ → isOfHLevelSuc (2 + n) (isOfHLevelTrunc (2 + n)) u v))
          decode*
      where
      decode* : (u v : X) → P ∣ u ∣ ∣ v ∣ → Path (∥ X ∥ (2 + n)) ∣ u ∣ ∣ v ∣
      decode* u v =
        rec (isOfHLevelTrunc (2 + n) ∣ u ∣ ∣ v ∣) (cong ∣_∣)

  {- auxiliary function r used to define encode -}
  r : (u : ∥ X ∥ (2 + n)) → P u u
  r = elim (λ x → hLevelP x x) (λ a → ∣ refl ∣)

  {- encode function from x ≡ y to P x y -}
  encode-fun : (x y : ∥ X ∥ (2 + n)) → x ≡ y → P x y
  encode-fun x y p = subst (P x) p (r x)

  {- We need the following two lemmas on the functions behaviour for refl -}
  dec-refl : (x : ∥ X ∥ (2 + n)) → decode-fun x x (r x) ≡ refl
  dec-refl =
    elim (λ x → isOfHLevelSuc (1 + n)
                  (isOfHLevelSuc (1 + n)
                     (isOfHLevelTrunc (2 + n) x x)
                     (decode-fun x x (r x)) refl))
         (λ _ → refl)

  enc-refl : (x : ∥ X ∥ (2 + n)) → encode-fun x x refl ≡ r x
  enc-refl x = transportRefl (r x)

  {- decode-fun is a right-inverse -}
  P-rinv : (u v : ∥ X ∥ (2 + n)) (x : Path (∥ X ∥ (2 + n)) u v)
         → decode-fun u v (encode-fun u v x) ≡ x
  P-rinv u v = J (λ y p → decode-fun u y (encode-fun u y p) ≡ p)
                 (cong (decode-fun u u) (enc-refl u) ∙ dec-refl u)

  {- decode-fun is a left-inverse -}
  P-linv : (u v : ∥ X ∥ (2 + n)) (x : P u v)
         → encode-fun u v (decode-fun u v x) ≡ x
  P-linv =
    elim2 (λ x y → isOfHLevelΠ (2 + n) (λ z → isOfHLevelSuc (2 + n) (hLevelP x y) _ _))
          helper
    where
    helper : (a b : X) (p : P ∣ a ∣ ∣ b ∣)
           → encode-fun _ _ (decode-fun ∣ a ∣ ∣ b ∣ p) ≡ p
    helper a b =
      elim (λ x → hLevelP ∣ a ∣ ∣ b ∣ _ _)
           (J (λ y p → encode-fun ∣ a ∣ ∣ y ∣ (decode-fun _ _ ∣ p ∣) ≡ ∣ p ∣)
              (enc-refl ∣ a ∣))

  {- The final Iso established -}
  IsoFinal : (x y : ∥ X ∥ (2 + n)) → Iso (x ≡ y) (P x y)
  Iso.fun (IsoFinal x y) = encode-fun x y
  Iso.inv (IsoFinal x y) = decode-fun x y
  Iso.rightInv (IsoFinal x y) = P-linv x y
  Iso.leftInv (IsoFinal x y) = P-rinv x y

PathIdTruncIso : {a b : A} (n : HLevel) → Iso (Path (∥ A ∥ (suc n)) ∣ a ∣ ∣ b ∣) (∥ a ≡ b ∥ n)
PathIdTruncIso zero = isContr→Iso ((isOfHLevelTrunc 1 _ _)
                    , isOfHLevelPath 1 (isOfHLevelTrunc 1) ∣ _ ∣ ∣ _ ∣ _) (isOfHLevelUnit* 0)
PathIdTruncIso (suc n) = ΩTrunc.IsoFinal ∣ _ ∣ ∣ _ ∣

PathIdTrunc : {a b : A} (n : HLevel) → (Path (∥ A ∥ (suc n)) ∣ a ∣ ∣ b ∣) ≡ (∥ a ≡ b ∥ n)
PathIdTrunc n = isoToPath (PathIdTruncIso n)

PathΩ : {a : A} (n : HLevel) → (Path (∥ A ∥ (suc n)) ∣ a ∣ ∣ a ∣) ≡ (∥ a ≡ a ∥ n)
PathΩ n = PathIdTrunc n

{- Special case using direct defs of truncations -}
PathIdTrunc₀Iso : {a b : A} → Iso (∣ a ∣₂ ≡ ∣ b ∣₂) ∥ a ≡ b ∥₁
PathIdTrunc₀Iso = compIso (congIso setTruncTrunc2Iso)
                    (compIso (ΩTrunc.IsoFinal ∣ _ ∣ ∣ _ ∣)
                             (invIso propTruncTrunc1Iso))

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

truncOfTruncIso : (n m : HLevel) → Iso (hLevelTrunc n A) (hLevelTrunc n (hLevelTrunc (m + n) A))
truncOfTruncIso zero m = isContr→Iso (isOfHLevelUnit* 0) (isOfHLevelUnit* 0)
Iso.fun (truncOfTruncIso (suc n) zero) = rec (isOfHLevelTrunc (suc n)) λ a → ∣ ∣ a ∣ ∣
Iso.fun (truncOfTruncIso (suc n) (suc m)) = rec (isOfHLevelTrunc (suc n)) λ a → ∣ ∣ a ∣ ∣
Iso.inv (truncOfTruncIso (suc n) zero) =  rec (isOfHLevelTrunc (suc n))
                                               (rec (isOfHLevelTrunc (suc n))
                                                     λ a → ∣ a ∣)
Iso.inv (truncOfTruncIso (suc n) (suc m)) =  rec (isOfHLevelTrunc (suc n))
                                                  (rec (isOfHLevelPlus (suc m) (isOfHLevelTrunc (suc n)))
                                                        λ a → ∣ a ∣)
Iso.rightInv (truncOfTruncIso (suc n) zero) =
  elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _ )
       (elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _ )
              λ a → refl)
Iso.rightInv (truncOfTruncIso (suc n) (suc m)) =
  elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _ )
               (elim (λ x → isOfHLevelPath ((suc m) + (suc n)) (isOfHLevelPlus (suc m) (isOfHLevelTrunc (suc n))) _ _ )
                      λ a → refl)
Iso.leftInv (truncOfTruncIso (suc n) zero) = elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → refl
Iso.leftInv (truncOfTruncIso (suc n) (suc m)) = elim (λ x → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → refl

truncOfTruncEq : (n m : ℕ) → (hLevelTrunc n A) ≃ (hLevelTrunc n (hLevelTrunc (m + n) A))
truncOfTruncEq n m = isoToEquiv (truncOfTruncIso n m)

truncOfTruncIso2 : (n m : HLevel) → Iso (hLevelTrunc (m + n) (hLevelTrunc n A)) (hLevelTrunc n A)
truncOfTruncIso2 n m = truncIdempotentIso (m + n) (isOfHLevelPlus m (isOfHLevelTrunc n))

truncOfΣIso : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : A → Type ℓ'}
       → Iso (hLevelTrunc n (Σ A B)) (hLevelTrunc n (Σ A λ x → hLevelTrunc n (B x)))
truncOfΣIso zero = idIso
Iso.fun (truncOfΣIso (suc n)) = map λ {(a , b) → a , ∣ b ∣}
Iso.inv (truncOfΣIso (suc n)) =
  rec (isOfHLevelTrunc (suc n))
        (uncurry λ a → rec (isOfHLevelTrunc (suc n)) λ b → ∣ a , b ∣)
Iso.rightInv (truncOfΣIso (suc n)) =
  elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
         (uncurry λ a → elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
         λ b → refl)
Iso.leftInv (truncOfΣIso (suc n)) =
  elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ {(a , b) → refl}

max_stars_repo_name: shlevy/cubical

max_issues_repo_name: shlevy/cubical

max_forks_repo_name: shlevy/cubical


text:
module GetTypes where

open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ)
open import Data.List using (List ; map)
open import Data.Vec using (Vec) renaming (map to mapV)
open import Function using (_∘_ ; id)
open import Relation.Binary.PropositionalEquality using (_≗_)

open import Structures using (Shaped ; module Shaped)
open import Instances using (VecShaped)

module ListList where
  record Get : Set₁ where
    field
      get : {A : Set} → List A → List A
      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get

module VecVec where
  record Get : Set₁ where
    field
      getlen : ℕ → ℕ
      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get

module PartialVecVec where
  record Get : Set₁ where
    field
      I : Set
      gl₁ : I → ℕ
      gl₂ : I → ℕ
      get : {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i)
      free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get

VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
VecVec-to-PartialVecVec G = record
  { I = ℕ
  ; gl₁ = id
  ; gl₂ = getlen
  ; get = get
  ; free-theorem = free-theorem
  } where open VecVec.Get G

module PartialShapeShape where
  record Get : Set₁ where
    field
      SourceShape : Set
      SourceContainer : Set → SourceShape → Set
      SourceShapeT : Shaped SourceShape SourceContainer

      ViewShape : Set
      ViewContainer : Set → ViewShape → Set
      ViewShapeT : Shaped ViewShape ViewContainer

      I : Set
      gl₁ : I → SourceShape
      gl₂ : I → ViewShape

    open Shaped SourceShapeT using () renaming (fmap to fmapS)
    open Shaped ViewShapeT using () renaming (fmap to fmapV)

    field
      get : {A : Set} {i : I} → SourceContainer A (gl₁ i) → ViewContainer A (gl₂ i)
      free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get

    open Shaped SourceShapeT public using () renaming (fmap to fmapS)
    open Shaped ViewShapeT public using () renaming (fmap to fmapV)

PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
PartialVecVec-to-PartialShapeShape G = record
  { SourceShapeT = VecShaped
  ; ViewShapeT   = VecShaped
  ; I            = I
  ; gl₁          = gl₁
  ; gl₂          = gl₂
  ; get          = get
  ; free-theorem = free-theorem
  } where open PartialVecVec.Get G

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation with respect to a
-- setoid. This is a generalisation of what is commonly known as Order
-- Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid; Rel)

module Data.List.Relation.Binary.Sublist.Setoid
  {c ℓ} (S : Setoid c ℓ) where

open import Level using (_⊔_)
open import Data.List.Base using (List; []; _∷_)
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Sublist.Heterogeneous as Heterogeneous
import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
  as HeterogeneousCore
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
  as HeterogeneousProperties
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Setoid S renaming (Carrier to A)
open SetoidEquality S

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

infix 4 _⊆_
_⊆_ : Rel (List A) (c ⊔ ℓ)
_⊆_ = Heterogeneous.Sublist _≈_

------------------------------------------------------------------------
-- Re-export definitions and operations from heterogeneous sublists

open HeterogeneousCore _≈_ using ([]; _∷_; _∷ʳ_) public
open Heterogeneous {R = _≈_} hiding (Sublist; []; _∷_; _∷ʳ_) public
  renaming
  (toAny to to∈; fromAny to from∈)

------------------------------------------------------------------------
-- Relational properties holding for Setoid case

⊆-reflexive : _≋_ ⇒ _⊆_
⊆-reflexive = HeterogeneousProperties.fromPointwise

⊆-refl : Reflexive _⊆_
⊆-refl = HeterogeneousProperties.refl refl

⊆-trans : Transitive _⊆_
⊆-trans = HeterogeneousProperties.trans trans

⊆-antisym : Antisymmetric _≋_ _⊆_
⊆-antisym = HeterogeneousProperties.antisym (λ x≈y _ → x≈y)

⊆-isPreorder : IsPreorder _≋_ _⊆_
⊆-isPreorder = record
  { isEquivalence = ≋-isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_
⊆-isPartialOrder = record
  { isPreorder = ⊆-isPreorder
  ; antisym    = ⊆-antisym
  }

⊆-preorder : Preorder c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-preorder = record
  { isPreorder = ⊆-isPreorder
  }

⊆-poset : Poset c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-poset = record
  { isPartialOrder = ⊆-isPartialOrder
  }


text:
module Structure.Function where

import Lvl
open import Lang.Instance
open import Logic.Predicate
open import Logic
open import Structure.Function.Names
open import Structure.Setoid
open import Type

private variable ℓ ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ : Lvl.Level
private variable A B : Type{ℓ}

-- The function `f` "(behaves like)/is a function" in the context of `_≡_` from the Equiv instance.
-- `congruence` is the defining property of a function.
module _
  ⦃ equiv-A : Equiv{ℓₗ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₗ₂}(B) ⦄
  (f : A → B)
  where

  record Function : Stmt{Lvl.of(A) Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂} where
    constructor intro
    field congruence : Congruence₁(f)
  congruence₁ = inst-fn Function.congruence

_→ᶠⁿ_ : (A : Setoid{ℓₗ₁}{ℓₒ₁}) → (B : Setoid{ℓₗ₂}{ℓₒ₂}) → Type{ℓₒ₁ Lvl.⊔ ℓₒ₂ Lvl.⊔ ℓₗ₁ Lvl.⊔ ℓₗ₂}
([∃]-intro A) →ᶠⁿ ([∃]-intro B) = ∃(Function{A = A}{B = B})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

-- Here we define an inductive version of the product type, see below
-- for its uses.

-- See `Cubical.Data.Sigma` for `_×_` defined as a special case of
-- sigma types, which is the generally preferred one.

-- If × is defined using Σ then transp/hcomp will be compute
-- "negatively", that is, they won't reduce unless we project out the
-- first of second component. This is not always what we want so this
-- implementation is done using a datatype which computes positively.

private
  variable
    ℓ ℓ' : Level

data _×_ (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  _,_ : A → B → A × B

infixr 5 _×_

proj₁ : {A : Type ℓ} {B : Type ℓ'} → A × B → A
proj₁ (x , _) = x

proj₂ : {A : Type ℓ} {B : Type ℓ'} → A × B → B
proj₂ (_ , x) = x

private
  variable
    A    : Type ℓ
    B C  : A → Type ℓ

intro : (∀ a → B a) → (∀ a → C a) → ∀ a → B a × C a
intro f g a = f a , g a

map : {B : Type ℓ} {D : B → Type ℓ'}
   → (∀ a → C a) → (∀ b → D b) → (x : A × B) → C (proj₁ x) × D (proj₂ x)
map f g = intro (f ∘ proj₁) (g ∘ proj₂)

×-η : {A : Type ℓ} {B : Type ℓ'} (x : A × B) → x ≡ ((proj₁ x) , (proj₂ x))
×-η (x , x₁) = refl

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:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Concrete.Properties.VotesOnce   as VO
import      LibraBFT.Concrete.Properties.LockedRound as LR
open import LibraBFT.Impl.Consensus.Types hiding (EpochConfigFor)
open        EpochConfig
open import LibraBFT.Yasm.Yasm (ℓ+1 0ℓ) EpochConfig epochId authorsN ConcSysParms NodeId-PK-OK

-- This module collects in one place the obligations an
-- implementation must meet in order to enjoy the properties
-- proved in Abstract.Properties.

module LibraBFT.Concrete.Obligations where
  record ImplObligations : Set₁ where
    field
      -- Structural obligations:
      sps-cor : StepPeerState-AllValidParts

      -- Semantic obligations:
      --
      -- VotesOnce:
      vo₁ : VO.ImplObligation₁
      vo₂ : VO.ImplObligation₂

      -- LockedRound:
      lr₁ : LR.ImplObligation₁

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
open import Nat
open import Prelude
open import contexts
open import dynamics-core

open import canonical-value-forms

module canonical-boxed-forms where
  canonical-boxed-forms-num : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: num →
                            d boxedval →
                            Σ[ n ∈ Nat ] (d == N n)
  canonical-boxed-forms-num (TAVar _) (BVVal ())
  canonical-boxed-forms-num wt (BVVal v) = canonical-value-forms-num wt v

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for boxed values at arrow type
  data cbf-arr : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CBFALam : ∀{Δ d τ1 τ2} →
      Σ[ x ∈ Nat ] Σ[ d' ∈ ihexp ]
        ((d == (·λ x ·[ τ1 ] d')) ×
         (Δ , ■ (x , τ1) ⊢ d' :: τ2)
        )
        → cbf-arr Δ d τ1 τ2
    CBFACastArr : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == (d' ⟨ τ1' ==> τ2' ⇒ τ1 ==> τ2 ⟩)) ×
         (τ1' ==> τ2' ≠ τ1 ==> τ2) ×
         (Δ , ∅ ⊢ d' :: τ1' ==> τ2') ×
         (d' boxedval)
        )
        → cbf-arr Δ d τ1 τ2

  canonical-boxed-forms-arr : ∀{Δ d τ1 τ2 } →
                              Δ , ∅ ⊢ d :: (τ1 ==> τ2)  →
                              d boxedval →
                              cbf-arr Δ d τ1 τ2
  canonical-boxed-forms-arr (TAVar x₁) (BVVal ())
  canonical-boxed-forms-arr (TALam f wt) (BVVal v) = CBFALam (canonical-value-forms-arr (TALam f wt) v)
  canonical-boxed-forms-arr (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-arr (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-arr (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVVal ())
  canonical-boxed-forms-arr (TACast wt x) (BVArrCast x₁ bv) = CBFACastArr (_ , _ , _ , refl , x₁ , wt , bv)
  canonical-boxed-forms-arr (TAFailedCast x x₁ x₂ x₃) (BVVal ())

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for boxed values at sum type
  data cbf-sum : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CBFSInl : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (inl τ2 d')) ×
         (Δ , ∅ ⊢ d' :: τ1) ×
         (d boxedval)
        )
        → cbf-sum Δ d τ1 τ2
    CBFSInr : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ]
        ((d == (inr τ1 d')) ×
         (Δ , ∅ ⊢ d' :: τ2) ×
         (d boxedval)
        )
        → cbf-sum Δ d τ1 τ2
    CBFSCastSum : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == (d' ⟨ τ1' ⊕ τ2' ⇒ τ1 ⊕ τ2 ⟩)) ×
         (τ1' ⊕ τ2' ≠ τ1 ⊕ τ2) ×
         (Δ , ∅ ⊢ d' :: τ1' ⊕ τ2') ×
         (d' boxedval)
        )
        → cbf-sum Δ d τ1 τ2

  canonical-boxed-forms-sum : ∀{Δ d τ1 τ2 } →
                              Δ , ∅ ⊢ d :: (τ1 ⊕ τ2)  →
                              d boxedval →
                              cbf-sum Δ d τ1 τ2
  canonical-boxed-forms-sum (TAInl wt) x = CBFSInl (_ , refl , wt , x)
  canonical-boxed-forms-sum (TAInr wt) x = CBFSInr (_ , refl , wt , x)
  canonical-boxed-forms-sum (TACast wt x₁) (BVSumCast x bv) = CBFSCastSum (_ , _ , _ , refl , x , wt , bv)
  canonical-boxed-forms-sum (TAVar x₁) (BVVal ())
  canonical-boxed-forms-sum (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-sum (TACase wt _ wt₁ _ wt₂) (BVVal ())
  canonical-boxed-forms-sum (TAFst wt) (BVVal ())
  canonical-boxed-forms-sum (TASnd wt) (BVVal ())
  canonical-boxed-forms-sum (TAEHole x₁ x₂) (BVVal ())
  canonical-boxed-forms-sum (TANEHole x₁ wt x₂) (BVVal ())
  canonical-boxed-forms-sum (TACast wt x₁) (BVVal ())
  canonical-boxed-forms-sum (TAFailedCast wt x₁ x₂ x₃) (BVVal ())

  -- this type gives somewhat nicer syntax for the output of the canonical
  -- forms lemma for boxed values at product type
  data cbf-prod : (Δ : hctx) (d : ihexp) (τ1 τ2 : htyp) → Set where
    CBFPPair : ∀{Δ d τ1 τ2} →
      Σ[ d1 ∈ ihexp ] Σ[ d2 ∈ ihexp ]
        ((d == ⟨ d1 , d2 ⟩) ×
         (Δ , ∅ ⊢ d1 :: τ1) ×
         (Δ , ∅ ⊢ d2 :: τ2) ×
         (d1 boxedval) ×
         (d2 boxedval)
        )
        → cbf-prod Δ d τ1 τ2
    CBFPCastProd : ∀{Δ d τ1 τ2} →
      Σ[ d' ∈ ihexp ] Σ[ τ1' ∈ htyp ] Σ[ τ2' ∈ htyp ]
        ((d == (d' ⟨ τ1' ⊠ τ2' ⇒ τ1 ⊠ τ2 ⟩)) ×
         (τ1' ⊠ τ2' ≠ τ1 ⊠ τ2) ×
         (Δ , ∅ ⊢ d' :: τ1' ⊠ τ2') ×
         (d' boxedval)
        )
        → cbf-prod Δ d τ1 τ2
  canonical-boxed-forms-prod : ∀{Δ d τ1 τ2 } →
                               Δ , ∅ ⊢ d :: (τ1 ⊠ τ2)  →
                               d boxedval →
                               cbf-prod Δ d τ1 τ2
  canonical-boxed-forms-prod (TAPair wt wt₁) (BVVal (VPair x x₁)) = CBFPPair (_ , _ , refl , wt , wt₁ , BVVal x , BVVal x₁)
  canonical-boxed-forms-prod (TAPair wt wt₁) (BVPair bv bv₁) = CBFPPair (_ , _ , refl , wt , wt₁ , bv , bv₁)
  canonical-boxed-forms-prod (TACast wt x) (BVProdCast x₁ bv) = CBFPCastProd (_ , _ , _ , refl , x₁ , wt , bv)

  canonical-boxed-forms-hole : ∀{Δ d} →
                               Δ , ∅ ⊢ d :: ⦇-⦈ →
                               d boxedval →
                               Σ[ d' ∈ ihexp ] Σ[ τ' ∈ htyp ]
                                 ((d == d' ⟨ τ' ⇒ ⦇-⦈ ⟩) ×
                                  (τ' ground) ×
                                  (Δ , ∅ ⊢ d' :: τ'))
  canonical-boxed-forms-hole (TAVar x₁) (BVVal ())
  canonical-boxed-forms-hole (TAAp wt wt₁) (BVVal ())
  canonical-boxed-forms-hole (TAEHole x x₁) (BVVal ())
  canonical-boxed-forms-hole (TANEHole x wt x₁) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVVal ())
  canonical-boxed-forms-hole (TACast wt x) (BVHoleCast x₁ bv) = _ , _ , refl , x₁ , wt
  canonical-boxed-forms-hole (TAFailedCast x x₁ x₂ x₃) (BVVal ())

  canonical-boxed-forms-coverage : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d boxedval →
                                   τ ≠ num →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊕ τ2)) →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ⊠ τ2)) →
                                   τ ≠ ⦇-⦈ →
                                   ⊥
  canonical-boxed-forms-coverage TANum bv nn na ns np nh = nn refl
  canonical-boxed-forms-coverage (TAPlus wt wt₁) bv nn na ns np nh = nn refl
  canonical-boxed-forms-coverage (TALam x wt) bv nn na ns np nh = na _ _ refl
  canonical-boxed-forms-coverage (TAAp wt wt₁) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TAInl wt) bv nn na ns np nh = ns _ _ refl
  canonical-boxed-forms-coverage (TAInr wt) bv nn na ns np nh = ns _ _ refl
  canonical-boxed-forms-coverage (TACase wt _ wt₁ _ wt₂) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TAEHole x x₁) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TANEHole x wt x₁) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TACast wt x) (BVArrCast x₁ bv) nn na ns np nh = na _ _ refl
  canonical-boxed-forms-coverage (TACast wt x) (BVSumCast x₁ bv) nn na ns np nh = ns _ _ refl
  canonical-boxed-forms-coverage (TACast wt x) (BVProdCast x₁ bv) nn na ns np nh = np _ _ refl
  canonical-boxed-forms-coverage (TACast wt x) (BVHoleCast x₁ bv) nn na ns np nh = nh refl
  canonical-boxed-forms-coverage (TAFailedCast wt x x₁ x₂) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TAPair wt wt₁) bv nn na ns np nh = np _ _ refl
  canonical-boxed-forms-coverage (TAFst wt) (BVVal ()) nn na ns np nh
  canonical-boxed-forms-coverage (TASnd wt) (BVVal ()) nn na ns np nh

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
------------------------------------------------------------------------
-- The Maybe type
------------------------------------------------------------------------

module Data.Maybe where

------------------------------------------------------------------------
-- The type

open import Data.Maybe.Core public

------------------------------------------------------------------------
-- Some operations

open import Data.Bool using (Bool; true; false)
open import Data.Unit using (⊤)

boolToMaybe : Bool → Maybe ⊤
boolToMaybe true  = just _
boolToMaybe false = nothing

maybeToBool : ∀ {A} → Maybe A → Bool
maybeToBool (just _) = true
maybeToBool nothing  = false

-- A non-dependent eliminator.

maybe : {a b : Set} → (a → b) → b → Maybe a → b
maybe j n (just x) = j x
maybe j n nothing  = n

maybe₀₁ : {a : Set} {b : Set₁} → (a → b) → b → Maybe a → b
maybe₀₁ j n (just x) = j x
maybe₀₁ j n nothing  = n

------------------------------------------------------------------------
-- Maybe monad

open import Data.Function
open import Category.Functor
open import Category.Monad
open import Category.Monad.Identity

functor : RawFunctor Maybe
functor = record
  { _<$>_ = λ f → maybe (just ∘ f) nothing
  }

monadT : ∀ {M} → RawMonad M → RawMonad (λ A → M (Maybe A))
monadT M = record
  { return = M.return ∘ just
  ; _>>=_  = λ m f → M._>>=_ m (maybe f (M.return nothing))
  }
  where module M = RawMonad M

monad : RawMonad Maybe
monad = monadT IdentityMonad

monadZero : RawMonadZero Maybe
monadZero = record
  { monad = monad
  ; ∅     = nothing
  }

monadPlus : RawMonadPlus Maybe
monadPlus = record
  { monadZero = monadZero
  ; _∣_       = _∣_
  }
  where
  _∣_ : ∀ {a} → Maybe a → Maybe a → Maybe a
  nothing ∣ y = y
  just x  ∣ y = just x

------------------------------------------------------------------------
-- Equality

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

drop-just : ∀ {A} {x y : A} → just x ≡ just y → x ≡ y
drop-just refl = refl

decSetoid : ∀ {A} → Decidable (_≡_ {A}) → DecSetoid
decSetoid {A} _A-≟_ = PropEq.decSetoid _≟_
  where
  _≟_ : Decidable (_≡_ {Maybe A})
  just x  ≟ just y  with x A-≟ y
  just x  ≟ just .x | yes refl = yes refl
  just x  ≟ just y  | no  x≢y    = no (x≢y ∘ drop-just)
  just x  ≟ nothing = no λ()
  nothing ≟ just y  = no λ()
  nothing ≟ nothing = yes refl

------------------------------------------------------------------------
-- Any and All

open import Data.Product using (_,_)
open import Data.Empty using (⊥)
import Relation.Nullary.Decidable as Dec

data Any {A} (P : A → Set) : Maybe A → Set where
  just : ∀ {x} (px : P x) → Any P (just x)

data All {A} (P : A → Set) : Maybe A → Set where
  just    : ∀ {x} (px : P x) → All P (just x)
  nothing : All P nothing

IsJust : ∀ {A} → Maybe A → Set
IsJust = Any (λ _ → ⊤)

IsNothing : ∀ {A} → Maybe A → Set
IsNothing = All (λ _ → ⊥)

private

  drop-just-Any : ∀ {A} {P : A → Set} {x} → Any P (just x) → P x
  drop-just-Any (just px) = px

  drop-just-All : ∀ {A} {P : A → Set} {x} → All P (just x) → P x
  drop-just-All (just px) = px

anyDec : ∀ {A} {P : A → Set} →
         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (Any P x)
anyDec p nothing  = no λ()
anyDec p (just x) = Dec.map (just , drop-just-Any) (p x)

allDec : ∀ {A} {P : A → Set} →
         (∀ x → Dec (P x)) → (x : Maybe A) → Dec (All P x)
allDec p nothing  = yes nothing
allDec p (just x) = Dec.map (just , drop-just-All) (p x)

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.String
open import Agda.Builtin.Nat
open import Agda.Builtin.List

infixl 5 _>>=_
_>>=_ = bindTC
pure = returnTC

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (data-cons d) as = con d as
defToTerm _ _ _ = unknown

derefImmediate : Term → TC Term
derefImmediate (def f args) = getDefinition f >>= λ f' → pure (defToTerm f f' args)
derefImmediate x = pure x

macro
  reflect : ∀ {ℓ} {t : Set ℓ} → t → Type → TC ⊤
  reflect {_} {t} x ty = quoteTC x >>= derefImmediate >>= λ x' → quoteTC t >>= checkType x' >>= quoteTC >>= unify ty
  -- reflect {_} {t} x ty = quoteTC x >>= derefImmediate >>= quoteTC >>= unify ty

data Maybe {ℓ} (t : Set ℓ) : Set ℓ where
  just : t → Maybe t
  nothing : Maybe t

listToMaybe : ∀ {ℓ} {t : Set ℓ} → List t → Maybe t
listToMaybe [] = nothing
listToMaybe (x ∷ _) = just x

record Show {ℓ} (t : Set ℓ) : Set ℓ where
  field
     show : t → String

open Show {{...}}

instance
  showN : Show Nat
  showN = record { show = λ _ → "nat" }

  mShow : ∀ {ℓ} {t : Set ℓ} → {{_ : Show t}} → Show (Maybe t)
  mShow = record {
      show = λ { (just x) → show x ;
                 _ → "nothing" }
    }

prog : String
prog =
  let
    x : List Nat
    x = 3 ∷ []
  in
  show (listToMaybe x)

example : Term
example = reflect prog

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base

module HoTT.Base.Inspect where

open variables

data Inspect {i j} {A : 𝒰 i} {P : A → 𝒰 j} (f : Π A P) (x : A) (y : P x) : 𝒰 (i ⊔ j) where
  [_] : y == f x → Inspect f x y

inspect : (f : Π A P) (x : A) → Inspect f x (f x)
inspect f x = [ refl ]

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
{- Next step operator. -}
module TemporalOps.Next where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.CartesianStrength
open import TemporalOps.Common

open import Data.Product
open import Data.Sum

-- One-step delay operator.
▹_ : τ -> τ
(▹ A) zero    = ⊤ zero
(▹ A) (suc n) = A n
infixr 70 ▹_

-- Functor instance for ▹
F-▹ : Endofunctor ℝeactive
F-▹ = record
    { omap      = ▹_
    ; fmap      = fmap-▹
    ; fmap-id   = λ {_ n} -> fmap-▹-id {n = n}
    ; fmap-∘    = λ {_ _ _ _ _ n} -> fmap-▹-∘ {n = n}
    ; fmap-cong = fmap-▹-cong
    }
    where
    -- Lifting of ▹
    fmap-▹ : {A B : τ} -> A ⇴ B -> ▹ A ⇴ ▹ B
    fmap-▹ f zero =  λ _ → top.tt
    fmap-▹ f (suc n) = f n
    -- ▹ preserves identities
    fmap-▹-id : ∀ {A : τ} {n : ℕ} {a : ▹ A at n}
             -> (fmap-▹ id at n) a ≡ a
    fmap-▹-id {n = zero} = refl
    fmap-▹-id {n = suc n} = refl
    -- ▹ preserves composition
    fmap-▹-∘ : ∀ {A B C : τ} {g : B ⇴ C} {f : A ⇴ B} {n : ℕ} {a : ▹ A at n}
            -> (fmap-▹ (g ∘ f) at n) a ≡ (fmap-▹ g ∘ fmap-▹ f at n) a
    fmap-▹-∘ {n = zero}  = refl
    fmap-▹-∘ {n = suc n} = refl
    -- ▹ is congruent
    fmap-▹-cong : ∀{A B : τ} {f f′ : A ⇴ B}
            -> ({n : ℕ} {a : A at n}   -> f n a ≡ f′ n a)
            -> ({n : ℕ} {a : ▹ A at n} -> (fmap-▹ f at n) a
                                        ≡ (fmap-▹ f′ at n) a)
    fmap-▹-cong e {zero} = refl
    fmap-▹-cong e {suc n} = e

-- ▹ is a Cartesian functor
F-cart-▹ : CartesianFunctor F-▹ ℝeactive-cart ℝeactive-cart
F-cart-▹ = record
    { u = u-▹
    ; m = m-▹
    ; m-nat₁ = m-nat₁-▹
    ; m-nat₂ = m-nat₂-▹
    ; associative = λ {A}{B}{C}{n}{a} -> assoc-▹ {A}{B}{C}{n}{a}
    ; unital-right = λ {A}{n}{a} -> unit-right-▹ {A}{n}{a}
    ; unital-left = λ {A}{n}{a} -> unit-left-▹ {A}{n}{a}
    }
    where
    open Functor F-▹

    u-▹ : ⊤ ⇴ ▹ ⊤
    u-▹ zero t = top.tt
    u-▹ (suc n) t = top.tt

    m-▹ : ∀(A B : τ) -> ▹ A ⊗ ▹ B ⇴ ▹ (A ⊗ B)
    m-▹ A B zero _ = top.tt
    m-▹ A B (suc n) p = p

    m-nat₁-▹ : ∀{A B C : τ} (f : A ⇴ B)
          -> fmap (f * id) ∘ m-▹ A C ≈ m-▹ B C ∘ fmap f * id
    m-nat₁-▹ f {zero} {a} = refl
    m-nat₁-▹ f {suc n} {a} = refl

    m-nat₂-▹ : ∀{A B C : τ} (f : A ⇴ B)
          -> fmap (id * f) ∘ m-▹ C A ≈ m-▹ C B ∘ id * fmap f
    m-nat₂-▹ f {zero} {a} = refl
    m-nat₂-▹ f {suc n} {a} = refl

    assoc-▹ : ∀{A B C : τ}
           -> m-▹ A (B ⊗ C) ∘ id * m-▹ B C ∘ assoc-right
            ≈ fmap assoc-right ∘ m-▹ (A ⊗ B) C ∘ m-▹ A B * id
    assoc-▹ {A} {B} {C} {zero} {a} = refl
    assoc-▹ {A} {B} {C} {suc n} {(▹A , ▹B) , ▹C} = refl

    unit-right-▹ : ∀{A : τ} ->
        fmap unit-right ∘ m-▹ A ⊤ ∘ (id * u-▹) ≈ unit-right
    unit-right-▹ {A} {zero} {a} = refl
    unit-right-▹ {A} {suc n} {a} = refl

    unit-left-▹ : ∀{A : τ} ->
        fmap unit-left ∘ m-▹ ⊤ A ∘ (u-▹ * id) ≈ unit-left
    unit-left-▹ {A} {zero} {a} = refl
    unit-left-▹ {A} {suc n} {a} = refl

-- ▹ preserves coproducts
sum-▹ : ∀{A B : τ} -> (▹ A ⊕ ▹ B) ⇴ ▹ (A ⊕ B)
sum-▹ zero v = top.tt
sum-▹ (suc n) v = v


text:
module Luau.RuntimeType where

open import Luau.Value using (Value; nil; addr; number)

data RuntimeType : Set where
  function : RuntimeType
  number : RuntimeType
  nil : RuntimeType

valueType : Value → RuntimeType
valueType nil = nil
valueType (addr x) = function
valueType (number x) = number


text:
------------------------------------------------------------------------
-- An abstraction of various forms of recursion/induction
------------------------------------------------------------------------

-- Note: The types in this module can perhaps be easier to understand
-- if they are normalised. Note also that Agda can do the
-- normalisation for you.

module Induction where

open import Relation.Unary

-- A RecStruct describes the allowed structure of recursion. The
-- examples in Induction.Nat should explain what this is all about.

RecStruct : Set → Set₁
RecStruct a = Pred a → Pred a

-- A recursor builder constructs an instance of a recursion structure
-- for a given input.

RecursorBuilder : ∀ {a} → RecStruct a → Set₁
RecursorBuilder {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal (Rec P)

-- A recursor can be used to actually compute/prove something useful.

Recursor : ∀ {a} → RecStruct a → Set₁
Recursor {a} Rec = (P : Pred a) → Rec P ⊆′ P → Universal P

-- And recursors can be constructed from recursor builders.

build : ∀ {a} {Rec : RecStruct a} →
        RecursorBuilder Rec →
        Recursor Rec
build builder P f x = f x (builder P f x)

-- We can repeat the exercise above for subsets of the type we are
-- recursing over.

SubsetRecursorBuilder : ∀ {a} → Pred a → RecStruct a → Set₁
SubsetRecursorBuilder {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ Rec P

SubsetRecursor : ∀ {a} → Pred a → RecStruct a → Set₁
SubsetRecursor {a} Q Rec = (P : Pred a) → Rec P ⊆′ P → Q ⊆′ P

subsetBuild : ∀ {a} {Q : Pred a} {Rec : RecStruct a} →
              SubsetRecursorBuilder Q Rec →
              SubsetRecursor Q Rec
subsetBuild builder P f x q = f x (builder P f x q)


text:
------------------------------------------------------------------------
-- An equality postulate which evaluates
------------------------------------------------------------------------

module Relation.Binary.PropositionalEquality.TrustMe where

open import Relation.Binary.PropositionalEquality

private
 primitive
   primTrustMe : {A : Set}{a b : A} → a ≡ b

-- trustMe {a = x} {b = y} evaluates to refl if x and y are
-- definitionally equal.
--
-- For an example of the use of trustMe, see Data.String._≟_.

trustMe : {A : Set}{a b : A} → a ≡ b
trustMe = primTrustMe


text:
-- As reported by Andreas on 2017-01-23

open import Common.Equality
open import Common.Product

data Bool : Set where
  true false : Bool

f : (x y : Bool) → Bool
f true y     = y
-- f false x = true  -- Missing case

test : let
     X : Bool → Bool → Bool
     X = {! f !}
  in (∀{x y} → X (f false x) y ≡ y) × (X false false ≡ true)
test = refl , refl

-- If we add the missing clause f false x = true, then X has
-- for instance solution f.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda