text:
------------------------------------------------------------------------
-- Propositional truncation
------------------------------------------------------------------------

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

-- Partly following the HoTT book.

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the propositional truncation uses
-- path equality, but the supplied notion of equality is used for many
-- other things.

import Equality.Path as P

module H-level.Truncation.Propositional
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Dec
open import Prelude
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J as Bijection using (_↔_)
open import Embedding equality-with-J as Embedding hiding (id; _∘_)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased equality-with-J using (_≃ᴱ_)
open import Equivalence.Erased.Contractible-preimages equality-with-J
  as ECP using (_⁻¹ᴱ_)
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as E
  using (Erased; erased; Very-stableᴱ-≡; Erased-singleton)
import Erased.Stability equality-with-J as ES
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
import H-level.Truncation.Church equality-with-J as Trunc
open import H-level.Truncation.Propositional.Erased eq as TE
  using (∥_∥ᴱ; Surjectiveᴱ)
open import Injection equality-with-J using (_↣_)
open import Monad equality-with-J
open import Preimage equality-with-J as Preimage using (_⁻¹_)
open import Surjection equality-with-J as Surjection
  using (_↠_; Split-surjective)

private
  variable
    a b c d p r ℓ       : Level
    A A₁ A₂ B B₁ B₂ C D : Type a
    P Q                 : A → Type p
    R                   : A → A → Type r
    A↠B f k s x y       : A

-- Propositional truncation.

data ∥_∥ (A : Type a) : Type a where
  ∣_∣                        : A → ∥ A ∥
  truncation-is-propositionᴾ : P.Is-proposition ∥ A ∥

-- The truncation produces propositions.

truncation-is-proposition : Is-proposition ∥ A ∥
truncation-is-proposition =
  _↔_.from (H-level↔H-level 1) truncation-is-propositionᴾ

-- A dependent eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (p : P x) (q : P y) →
      P.[ (λ i → P (truncation-is-propositionᴾ x y i)) ] p ≡ q

open Elimᴾ′ public

elimᴾ′ : Elimᴾ′ P → (x : ∥ A ∥) → P x
elimᴾ′ {A = A} {P = P} e = helper
  where
  module E′ = Elimᴾ′ e

  helper : (x : ∥ A ∥) → P x
  helper ∣ x ∣                              = E′.∣∣ʳ x
  helper (truncation-is-propositionᴾ x y i) =
    E′.truncation-is-propositionʳ (helper x) (helper y) i

-- A possibly more useful dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (x : ∥ A ∥) → P.Is-proposition (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : ∥ A ∥) → P x
elimᴾ e = elimᴾ′ e′
  where
  module E′ = Elimᴾ e

  e′ : Elimᴾ′ _
  e′ .∣∣ʳ                            = E′.∣∣ʳ
  e′ .truncation-is-propositionʳ _ _ =
    P.heterogeneous-irrelevance E′.truncation-is-propositionʳ

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                        : A → B
    truncation-is-propositionʳ : P.Is-proposition B

open Recᴾ public

recᴾ : Recᴾ A B → ∥ A ∥ → B
recᴾ r = elimᴾ e
  where
  module R = Recᴾ r

  e : Elimᴾ _
  e .∣∣ʳ                          = R.∣∣ʳ
  e .truncation-is-propositionʳ _ = R.truncation-is-propositionʳ

-- A dependently typed eliminator.

record Elim′ {A : Type a} (P : ∥ A ∥ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    truncation-is-propositionʳ :
      (x : ∥ A ∥) → Is-proposition (P x)

open Elim′ public

elim′ : Elim′ P → (x : ∥ A ∥) → P x
elim′ e = elimᴾ e′
  where
  module E′ = Elim′ e

  e′ : Elimᴾ _
  e′ .∣∣ʳ                        = E′.∣∣ʳ
  e′ .truncation-is-propositionʳ =
    _↔_.to (H-level↔H-level 1) ∘ E′.truncation-is-propositionʳ

elim :
  (P : ∥ A ∥ → Type p) →
  (∀ x → Is-proposition (P x)) →
  ((x : A) → P ∣ x ∣) →
  (x : ∥ A ∥) → P x
elim _ p f = elim′ λ where
  .∣∣ʳ                        → f
  .truncation-is-propositionʳ → p

-- Primitive "recursion".

record Rec′ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                        : A → B
    truncation-is-propositionʳ : Is-proposition B

open Rec′ public

rec′ : Rec′ A B → ∥ A ∥ → B
rec′ r = recᴾ r′
  where
  module R = Rec′ r

  r′ : Recᴾ _ _
  r′ .∣∣ʳ                        = R.∣∣ʳ
  r′ .truncation-is-propositionʳ =
    _↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ

rec : Is-proposition B → (A → B) → ∥ A ∥ → B
rec p f = rec′ λ where
  .∣∣ʳ                        → f
  .truncation-is-propositionʳ → p

-- A map function.

∥∥-map : (A → B) → ∥ A ∥ → ∥ B ∥
∥∥-map f = rec truncation-is-proposition (∣_∣ ∘ f)

-- The propositional truncation defined here is isomorphic to the one
-- defined in H-level.Truncation.Church.

∥∥↔∥∥ :
  ∀ ℓ {a} {A : Type a} →
  ∥ A ∥ ↔ Trunc.∥ A ∥ 1 (a ⊔ ℓ)
∥∥↔∥∥ ℓ = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec (Trunc.truncation-has-correct-h-level 1 ext)
                   Trunc.∣_∣₁
      ; from = lower {ℓ = ℓ} ∘
               Trunc.rec 1
                         (↑-closure 1 truncation-is-proposition)
                         (lift ∘ ∣_∣)
      }
    ; right-inverse-of = λ _ →
        Trunc.truncation-has-correct-h-level 1 ext _ _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- If A is merely inhabited (with erased proofs), then A is merely
-- inhabited.

∥∥ᴱ→∥∥ : ∥ A ∥ᴱ → ∥ A ∥
∥∥ᴱ→∥∥ = TE.rec λ where
  .TE.∣∣ʳ                        → ∣_∣
  .TE.truncation-is-propositionʳ → truncation-is-proposition

-- In an erased context the propositional truncation operator defined
-- in H-level.Truncation.Propositional.Erased is equivalent to the one
-- defined here.

@0 ∥∥ᴱ≃∥∥ : ∥ A ∥ᴱ ≃ ∥ A ∥
∥∥ᴱ≃∥∥ = Eq.⇔→≃
  TE.truncation-is-proposition
  truncation-is-proposition
  ∥∥ᴱ→∥∥
  (rec TE.truncation-is-proposition TE.∣_∣)

mutual

  -- If A and B are logically equivalent, then functions of any kind can
  -- be constructed from ∥ A ∥ to ∥ B ∥.

  ∥∥-cong-⇔ : ∀ {k} → A ⇔ B → ∥ A ∥ ↝[ k ] ∥ B ∥
  ∥∥-cong-⇔ A⇔B = ∥∥-cong-⇔′ (∣_∣ ∘ _⇔_.to A⇔B) (∣_∣ ∘ _⇔_.from A⇔B)

  -- A variant of the previous result.

  ∥∥-cong-⇔′ : ∀ {k} → (A → ∥ B ∥) → (B → ∥ A ∥) → ∥ A ∥ ↝[ k ] ∥ B ∥
  ∥∥-cong-⇔′ A→∥B∥ B→∥A∥ =
    from-equivalence $
    Eq.⇔→≃
      truncation-is-proposition
      truncation-is-proposition
      (rec truncation-is-proposition A→∥B∥)
      (rec truncation-is-proposition B→∥A∥)

-- The truncation operator preserves all kinds of functions.

private

  ∥∥-cong-↣ : A ↣ B → ∥ A ∥ ↣ ∥ B ∥
  ∥∥-cong-↣ f = record
    { to        = ∥∥-map (_↣_.to f)
    ; injective = λ _ → truncation-is-proposition _ _
    }

∥∥-cong : A ↝[ k ] B → ∥ A ∥ ↝[ k ] ∥ B ∥
∥∥-cong {k = implication}         = ∥∥-map
∥∥-cong {k = logical-equivalence} = ∥∥-cong-⇔
∥∥-cong {k = surjection}          = ∥∥-cong-⇔ ∘ _↠_.logical-equivalence
∥∥-cong {k = bijection}           = ∥∥-cong-⇔ ∘ from-isomorphism
∥∥-cong {k = equivalence}         = ∥∥-cong-⇔ ∘ from-isomorphism
∥∥-cong {k = equivalenceᴱ}        = ∥∥-cong-⇔ ∘ _≃ᴱ_.logical-equivalence
∥∥-cong {k = injection}           = ∥∥-cong-↣
∥∥-cong {k = embedding}           =
  _↔_.to (↣↔Embedding ext
            (mono₁ 1 truncation-is-proposition)
            (mono₁ 1 truncation-is-proposition)) ∘
  ∥∥-cong-↣ ∘ Embedding.injection

-- A form of idempotence for binary sums.

idempotent : ∥ A ⊎ A ∥ ↔ ∥ A ∥
idempotent = ∥∥-cong-⇔ (record { to = [ id , id ]; from = inj₁ })

-- A generalised flattening lemma.

flatten′ :
  (F : (Type ℓ → Type ℓ) → Type f) →
  (∀ {G H} → (∀ {A} → G A → H A) → F G → F H) →
  (F ∥_∥ → ∥ F id ∥) →
  ∥ F ∥_∥ ∥ ↔ ∥ F id ∥
flatten′ _ map f = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec truncation-is-proposition f
      ; from = ∥∥-map (map ∣_∣)
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- Nested truncations can be flattened.

flatten : ∥ ∥ A ∥ ∥ ↔ ∥ A ∥
flatten {A = A} = flatten′ (λ F → F A) (λ f → f) id

private

  -- Another flattening lemma, given as an example of how flatten′ can
  -- be used.

  ∥∃∥∥∥↔∥∃∥ : {B : A → Type b} →
              ∥ ∃ (∥_∥ ∘ B) ∥ ↔ ∥ ∃ B ∥
  ∥∃∥∥∥↔∥∃∥ {B = B} =
    flatten′ (λ F → ∃ (F ∘ B))
             (λ f → Σ-map id f)
             (uncurry λ x → ∥∥-map (x ,_))

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∥ A ∥ → (A → ∥ B ∥) → ∥ B ∥
x >>=′ f = _↔_.to flatten (∥∥-map f x)

-- The universe-polymorphic variant of bind is associative.

>>=′-associative :
  (x : ∥ A ∥) {f : A → ∥ B ∥} {g : B → ∥ C ∥} →
  x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=′-associative x {f} {g} = elim
  (λ x → x >>=′ (λ x₁ → f x₁ >>=′ g) ≡ x >>=′ f >>=′ g)
  (λ _ → ⇒≡ 1 truncation-is-proposition)
  (λ _ → refl _)
  x

instance

  -- The propositional truncation operator is a monad.

  raw-monad : ∀ {ℓ} → Raw-monad (∥_∥ {a = ℓ})
  Raw-monad.return raw-monad = ∣_∣
  Raw-monad._>>=_  raw-monad = _>>=′_

  monad : ∀ {ℓ} → Monad (∥_∥ {a = ℓ})
  Monad.raw-monad monad           = raw-monad
  Monad.left-identity monad x f   = refl _
  Monad.associativity monad x _ _ = >>=′-associative x
  Monad.right-identity monad      = elim
    _
    (λ _ → ⇒≡ 1 truncation-is-proposition)
    (λ _ → refl _)

-- Surjectivity.

Surjective :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Surjective f = ∀ b → ∥ f ⁻¹ b ∥

-- The property Surjective f is a proposition.

Surjective-propositional : {f : A → B} → Is-proposition (Surjective f)
Surjective-propositional =
  Π-closure ext 1 λ _ →
  truncation-is-proposition

-- In an erased context surjectivity with erased proofs is equivalent
-- to surjectivity.
--
-- It appears to me as if neither direction of this equivalence can be
-- established if the erasure annotation is removed.

@0 Surjectiveᴱ≃Surjective : Surjectiveᴱ f ≃ Surjective f
Surjectiveᴱ≃Surjective {f = f} =
  (∀ y → ∥ f ⁻¹ᴱ y ∥ᴱ)  ↝⟨ (∀-cong ext λ _ → ∥∥ᴱ≃∥∥) ⟩
  (∀ y → ∥ f ⁻¹ᴱ y ∥)   ↝⟨ (∀-cong ext λ _ → ∥∥-cong (inverse ECP.⁻¹≃⁻¹ᴱ)) ⟩□
  (∀ y → ∥ f ⁻¹  y ∥)   □

-- The function ∣_∣ is surjective.

∣∣-surjective : Surjective (∣_∣ {A = A})
∣∣-surjective = elim
  _
  (λ _ → truncation-is-proposition)
  (λ x → ∣ x , refl _ ∣)

-- Split surjective functions are surjective.

Split-surjective→Surjective :
  {f : A → B} → Split-surjective f → Surjective f
Split-surjective→Surjective s = λ b → ∣ s b ∣

-- Being both surjective and an embedding is equivalent to being an
-- equivalence.
--
-- This is Corollary 4.6.4 from the first edition of the HoTT book
-- (the proof is perhaps not quite identical).

surjective×embedding≃equivalence :
  {f : A → B} →
  (Surjective f × Is-embedding f) ≃ Is-equivalence f
surjective×embedding≃equivalence {f = f} =
  (Surjective f × Is-embedding f)          ↔⟨ ∀-cong ext (λ _ → ∥∥↔∥∥ lzero) ×-cong F.id ⟩
  (Trunc.Surjective _ f × Is-embedding f)  ↝⟨ Trunc.surjective×embedding≃equivalence lzero ext ⟩□
  Is-equivalence f                         □

-- If the underlying type is a proposition, then truncations of the
-- type are isomorphic to the type itself.

∥∥↔ : Is-proposition A → ∥ A ∥ ↔ A
∥∥↔ A-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec A-prop id
      ; from = ∣_∣
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = λ _ → truncation-is-proposition _ _
  }

-- A type is a proposition if it is equivalent to the propositional
-- truncation of some type.

≃∥∥→Is-proposition : A ≃ ∥ B ∥ → Is-proposition A
≃∥∥→Is-proposition A≃∥B∥ a₁ a₂ =     $⟨ truncation-is-proposition _ _ ⟩
  _≃_.to A≃∥B∥ a₁ ≡ _≃_.to A≃∥B∥ a₂  ↝⟨ Eq.≃-≡ A≃∥B∥ ⟩□
  a₁ ≡ a₂                            □

-- A simple isomorphism involving propositional truncation.

∥∥×↔ : ∥ A ∥ × A ↔ A
∥∥×↔ =
  drop-⊤-left-× λ a →
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      truncation-is-proposition
      ∣ a ∣

-- A variant of ∥∥×↔, introduced to ensure that the right-inverse-of
-- proof is, by definition, simple.

∥∥×≃ : (∥ A ∥ × A) ≃ A
∥∥×≃ = Eq.↔→≃
  proj₂
  (λ x → ∣ x ∣ , x)
  refl
  (λ _ → cong (_, _) (truncation-is-proposition _ _))

_ : _≃_.right-inverse-of ∥∥×≃ x ≡ refl _
_ = refl _

-- A variant of ∥∥×≃.

Erased-∥∥×≃ : (Erased ∥ A ∥ × A) ≃ A
Erased-∥∥×≃ = Eq.↔→≃
  proj₂
  (λ x → E.[ ∣ x ∣ ] , x)
  refl
  (λ (_ , x) →
     cong (_, x) (E.[]-cong E.[ truncation-is-proposition _ _ ]))

_ : _≃_.right-inverse-of Erased-∥∥×≃ x ≡ refl _
_ = refl _

-- ∥_∥ commutes with _×_.

∥∥×∥∥↔∥×∥ : (∥ A ∥ × ∥ B ∥) ↔ ∥ A × B ∥
∥∥×∥∥↔∥×∥ = record
  { surjection = record
    { logical-equivalence = record
      { from = λ p → ∥∥-map proj₁ p , ∥∥-map proj₂ p
      ; to   = λ { (x , y) →
                   rec truncation-is-proposition
                       (λ x → rec truncation-is-proposition
                                  (λ y → ∣ x , y ∣)
                                  y)
                       x }
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      ×-closure 1 truncation-is-proposition
                  truncation-is-proposition
        _ _
  }

-- Variants of proj₁-closure.

private

  H-level-×₁-lemma :
    (A → ∥ B ∥) →
    ∀ n → H-level (suc n) (A × B) → H-level (suc n) A
  H-level-×₁-lemma inhabited n h =
    [inhabited⇒+]⇒+ n λ a →
    rec (H-level-propositional ext (suc n))
        (λ b → proj₁-closure (λ _ → b) (suc n) h)
        (inhabited a)

H-level-×₁ :
  (A → ∥ B ∥) →
  ∀ n → H-level n (A × B) → H-level n A
H-level-×₁ inhabited zero h =
  propositional⇒inhabited⇒contractible
    (H-level-×₁-lemma inhabited 0 (mono₁ 0 h))
    (proj₁ (proj₁ h))
H-level-×₁ inhabited (suc n) =
  H-level-×₁-lemma inhabited n

H-level-×₂ :
  (B → ∥ A ∥) →
  ∀ n → H-level n (A × B) → H-level n B
H-level-×₂ {B = B} {A = A} inhabited n =
  H-level n (A × B)  ↝⟨ H-level.respects-surjection (from-bijection ×-comm) n ⟩
  H-level n (B × A)  ↝⟨ H-level-×₁ inhabited n ⟩□
  H-level n B        □

-- If A is merely inhabited, then the truncation of A is isomorphic to
-- the unit type.

inhabited⇒∥∥↔⊤ : ∥ A ∥ → ∥ A ∥ ↔ ⊤
inhabited⇒∥∥↔⊤ ∥a∥ =
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      truncation-is-proposition
      ∥a∥

-- If A is not inhabited, then the propositional truncation of A is
-- isomorphic to the empty type.

not-inhabited⇒∥∥↔⊥ : ¬ A → ∥ A ∥ ↔ ⊥ {ℓ = ℓ}
not-inhabited⇒∥∥↔⊥ {A = A} =
  ¬ A        ↝⟨ (λ ¬a ∥a∥ → rec ⊥-propositional ¬a ∥a∥) ⟩
  ¬ ∥ A ∥    ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
  ∥ A ∥ ↔ ⊥  □

-- The negation of the truncation of A is isomorphic to the negation
-- of A.

¬∥∥↔¬ : ¬ ∥ A ∥ ↔ ¬ A
¬∥∥↔¬ {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → f ∘ ∣_∣
      ; from = rec ⊥-propositional
      }
    ; right-inverse-of = λ _ → ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _ → ¬-propositional ext _ _
  }

-- The function λ R x y → ∥ R x y ∥ preserves Is-equivalence-relation.

∥∥-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (λ x y → ∥ R x y ∥)
∥∥-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = ∣ reflexive ∣
  ; symmetric  = symmetric ⟨$⟩_
  ; transitive = λ p q → transitive ⟨$⟩ p ⊛ q
  }
  where
  open Is-equivalence-relation R-equiv

mutual

  -- The propositional truncation's universal property.

  universal-property :
    Is-proposition B →
    (∥ A ∥ → B) ≃ (A → B)
  universal-property B-prop = universal-property-Π (λ _ → B-prop)

  -- A generalisation of the universal property.

  universal-property-Π :
    (∀ x → Is-proposition (P x)) →
    ((x : ∥ A ∥) → P x) ≃ ((x : A) → P ∣ x ∣)
  universal-property-Π {A = A} {P = P} P-prop =
    ((x : ∥ A ∥) → P x)      ↝⟨ Eq.⇔→≃ prop truncation-is-proposition
                                  (λ f → ∣ f ∘ ∣_∣ ∣) (rec prop (elim _ P-prop)) ⟩
    ∥ ((x : A) → P ∣ x ∣) ∥  ↔⟨ ∥∥↔ (Π-closure ext 1 λ _ → P-prop _) ⟩□
    ((x : A) → P ∣ x ∣)      □
    where
    prop = Π-closure ext 1 λ _ → P-prop _

private

  -- The universal property computes in the right way.

  _ :
    (B-prop : Is-proposition B)
    (f : ∥ A ∥ → B) →
    _≃_.to (universal-property B-prop) f ≡ f ∘ ∣_∣
  _ = λ _ _ → refl _

  _ :
    (B-prop : Is-proposition B)
    (f : A → B) (x : A) →
    _≃_.from (universal-property B-prop) f ∣ x ∣ ≡ f x
  _ = λ _ _ _ → refl _

-- If there is a function f : A → ∥ B ∥, then f is an equivalence if
-- and only if the second projection from A × B is an equivalence.

equivalence-to-∥∥≃proj₂-equivalence :
  (f : A → ∥ B ∥) →
  Is-equivalence f ≃ Is-equivalence (proj₂ ⦂ (A × B → B))
equivalence-to-∥∥≃proj₂-equivalence {A = A} {B = B} f = Eq.⇔→≃
  (Eq.propositional ext _)
  (Eq.propositional ext _)
  (λ eq → _≃_.is-equivalence
            (A × B      ↝⟨ (×-cong₁ λ _ → Eq.⟨ _ , eq ⟩) ⟩
             ∥ B ∥ × B  ↝⟨ ∥∥×≃ ⟩□
             B          □))
  from
  where
  from : Is-equivalence proj₂ → Is-equivalence f
  from eq = _≃_.is-equivalence $ Eq.⇔→≃
    A-prop
    truncation-is-proposition
    _
    (rec A-prop (proj₁ ∘ _≃_.from Eq.⟨ _ , eq ⟩))
    where
    A-prop₁ : B → Is-proposition A
    A-prop₁ b a₁ a₂ =                  $⟨ refl _ ⟩
      b ≡ b                            ↔⟨⟩
      proj₂ (a₁ , b) ≡ proj₂ (a₂ , b)  ↔⟨ Eq.≃-≡ Eq.⟨ _ , eq ⟩ ⟩
      (a₁ , b) ≡ (a₂ , b)              ↝⟨ cong proj₁ ⟩□
      a₁ ≡ a₂                          □

    A-prop : Is-proposition A
    A-prop = [inhabited⇒+]⇒+ 0
      (A                 ↝⟨ f ⟩
       ∥ B ∥             ↝⟨ rec (H-level-propositional ext 1) A-prop₁ ⟩□
       Is-proposition A  □)

-- There is an equivalence between "A is equivalent to ∥ B ∥" and
-- "there is a function from A to ∥ B ∥ and the second projection is
-- an equivalence from A × B to B".

≃∥∥≃→∥∥×proj₂-equivalence :
  (A ≃ ∥ B ∥) ≃ ((A → ∥ B ∥) × Is-equivalence (proj₂ ⦂ (A × B → B)))
≃∥∥≃→∥∥×proj₂-equivalence {A = A} {B = B} =
  A ≃ ∥ B ∥                                           ↔⟨ Eq.≃-as-Σ ⟩
  (∃ λ (f : A → ∥ B ∥) → Is-equivalence f)            ↝⟨ ∃-cong equivalence-to-∥∥≃proj₂-equivalence ⟩□
  (A → ∥ B ∥) × Is-equivalence (proj₂ ⦂ (A × B → B))  □

-- The following three results come from "Generalizations of Hedberg's
-- Theorem" by Kraus, Escardó, Coquand and Altenkirch.

-- Types with constant endofunctions are "h-stable" (meaning that
-- "mere inhabitance" implies inhabitance).

constant-endofunction⇒h-stable : {f : A → A} → Constant f → ∥ A ∥ → A
constant-endofunction⇒h-stable {A = A} {f = f} c =
  ∥ A ∥                    ↝⟨ rec (fixpoint-lemma f c) (λ x → f x , c (f x) x) ⟩
  (∃ λ (x : A) → f x ≡ x)  ↝⟨ proj₁ ⟩□
  A                        □

-- Having a constant endofunction is logically equivalent to being
-- h-stable.

constant-endofunction⇔h-stable :
  (∃ λ (f : A → A) → Constant f) ⇔ (∥ A ∥ → A)
constant-endofunction⇔h-stable = record
  { to = λ { (_ , c) → constant-endofunction⇒h-stable c }
  ; from = λ f → f ∘ ∣_∣ , λ x y →

      f ∣ x ∣  ≡⟨ cong f $ truncation-is-proposition _ _ ⟩∎
      f ∣ y ∣  ∎
  }

-- A type is a set if and only if it is "h-separated" (which means
-- that all its equality types are h-stable).

Is-set⇔h-separated :
  Is-set A ⇔ ((x y : A) → ∥ x ≡ y ∥ → x ≡ y)
Is-set⇔h-separated {A = A} = record
  { to   = λ A-set _ _ → rec A-set id
  ; from =
      ((x y : A) → ∥ x ≡ y ∥ → x ≡ y)                     ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ →
                                                              _⇔_.from constant-endofunction⇔h-stable) ⟩
      ((x y : A) → ∃ λ (f : x ≡ y → x ≡ y) → Constant f)  ↝⟨ constant⇒set ⟩□
      Is-set A                                            □
  }

-- If A is decided, then ∥ A ∥ is decided.

Dec→Dec-∥∥ : Dec A → Dec ∥ A ∥
Dec→Dec-∥∥ (yes a) = yes ∣ a ∣
Dec→Dec-∥∥ (no ¬A) = no (_↔_.from ¬∥∥↔¬ ¬A)

-- If a binary relation can be decided, then the propositional
-- truncation of the relation can also be decided.

decidable→decidable-∥∥ :
  {P : A → B → Type p} →
  ((x : A) (y : B) → Dec (P x y)) →
  ((x : A) (y : B) → Dec ∥ P x y ∥)
decidable→decidable-∥∥ dec =
  λ x y → Dec→Dec-∥∥ (dec x y)

-- If A is decided, then one can convert between ∥ A ∥ and A.

Dec→∥∥⇔ :
  Dec A → ∥ A ∥ ⇔ A
Dec→∥∥⇔ _       ._⇔_.from = ∣_∣
Dec→∥∥⇔ (yes a) ._⇔_.to   = λ _ → a
Dec→∥∥⇔ (no ¬A) ._⇔_.to   = ⊥-elim ∘ rec ⊥-propositional ¬A

-- Variants of the following two lemmas were communicated to me by
-- Nicolai Kraus. They are closely related to Lemma 2.1 in his paper
-- "The General Universal Property of the Propositional Truncation".

-- A variant of ∥∥×≃.

drop-∥∥ :
  {B : A → Type b} →
  (A → ∥ C ∥) →
  (∥ C ∥ → ∀ x → B x) ≃ (∀ x → B x)
drop-∥∥ {C = C} {B = B} inh =
  Eq.with-other-inverse
    ((∥ C ∥ → ∀ a → B a)  ↔⟨ Π-comm ⟩
     (∀ a → ∥ C ∥ → B a)  ↝⟨ (∀-cong ext λ a → drop-⊤-left-Π ext (inhabited⇒∥∥↔⊤ (inh a))) ⟩□
     (∀ a → B a)          □)
    (λ f _ → f)
    (λ f → ⟨ext⟩ λ _ → ⟨ext⟩ λ a →
       _    ≡⟨ subst-const _ ⟩∎
       f a  ∎)

-- Another variant of ∥∥×≃.

push-∥∥ :
  {B : A → Type b} {C : (∀ x → B x) → Type c} →
  (A → ∥ D ∥) →
  (∥ D ∥ → ∃ λ (f : ∀ x → B x) → C f) ≃
  (∃ λ (f : ∀ x → B x) → ∥ D ∥ → C f)
push-∥∥ {D = D} {B = B} {C = C} inh =
  (∥ D ∥ → ∃ λ (f : ∀ c → B c) → C f)            ↔⟨ ΠΣ-comm ⟩
  (∃ λ (f : ∥ D ∥ → ∀ c → B c) → ∀ b → C (f b))  ↝⟨ (Σ-cong-contra (inverse $ drop-∥∥ inh) λ _ → F.id) ⟩□
  (∃ λ (f : ∀ c → B c) → ∥ D ∥ → C f)            □

-- Having a coherently constant function into a groupoid is equivalent
-- to having a function from a propositionally truncated type into the
-- groupoid. This result is Proposition 2.3 in "The General Universal
-- Property of the Propositional Truncation" by Kraus.

Coherently-constant :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Coherently-constant f =
  ∃ λ (c : Constant f) →
  ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃

coherently-constant-function≃∥inhabited∥⇒inhabited :
  {A : Type a} {B : Type b} →
  H-level 3 B →
  (∃ λ (f : A → B) → Coherently-constant f) ≃ (∥ A ∥ → B)
coherently-constant-function≃∥inhabited∥⇒inhabited
  {a = a} {b = b} {A = A} {B} B-groupoid =

  (∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ Trunc.coherently-constant-function≃∥inhabited∥⇒inhabited lzero ext B-groupoid ⟩
  (Trunc.∥ A ∥ 1 (a ⊔ b) → B)                ↝⟨ →-cong₁ ext (inverse $ ∥∥↔∥∥ (a ⊔ b)) ⟩□
  (∥ A ∥ → B)                                □

private

  -- One direction of the proposition above computes in the right way.

  to-coherently-constant-function≃∥inhabited∥⇒inhabited :
    (h : H-level 3 B)
    (f : ∃ λ (f : A → B) → Coherently-constant f) (x : A) →
    _≃_.to (coherently-constant-function≃∥inhabited∥⇒inhabited h)
      f ∣ x ∣ ≡
    proj₁ f x
  to-coherently-constant-function≃∥inhabited∥⇒inhabited _ _ _ = refl _

-- Having a constant function into a set is equivalent to having a
-- function from a propositionally truncated type into the set. The
-- statement of this result is that of Proposition 2.2 in "The General
-- Universal Property of the Propositional Truncation" by Kraus, but
-- it uses a different proof: as observed by Kraus this result follows
-- from Proposition 2.3.

constant-function≃∥inhabited∥⇒inhabited :
  {A : Type a} {B : Type b} →
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ≃ (∥ A ∥ → B)
constant-function≃∥inhabited∥⇒inhabited
  {a = a} {b = b} {A = A} {B} B-set =

  (∃ λ (f : A → B) → Constant f)  ↝⟨ Trunc.constant-function≃∥inhabited∥⇒inhabited lzero ext B-set ⟩
  (Trunc.∥ A ∥ 1 (a ⊔ b) → B)     ↝⟨ →-cong₁ ext (inverse $ ∥∥↔∥∥ (a ⊔ b)) ⟩□
  (∥ A ∥ → B)                     □

private

  -- One direction of the proposition above computes in the right way.

  to-constant-function≃∥inhabited∥⇒inhabited :
    (B-set : Is-set B)
    (f : ∃ λ (f : A → B) → Constant f) (x : A) →
    _≃_.to (constant-function≃∥inhabited∥⇒inhabited B-set) f ∣ x ∣ ≡
    proj₁ f x
  to-constant-function≃∥inhabited∥⇒inhabited _ _ _ = refl _

-- The axiom of choice, in one of the alternative forms given in the
-- HoTT book (§3.8).

Axiom-of-choice : (a b : Level) → Type (lsuc (a ⊔ b))
Axiom-of-choice a b =
  {A : Type a} {B : A → Type b} →
  Is-set A → (∀ x → ∥ B x ∥) → ∥ (∀ x → B x) ∥

-- The axiom of choice can be turned into a bijection.

choice-bijection :
  {A : Type a} {B : A → Type b} →
  Axiom-of-choice a b → Is-set A →
  (∀ x → ∥ B x ∥) ↔ ∥ (∀ x → B x) ∥
choice-bijection choice A-set = record
  { surjection = record
    { logical-equivalence = record
      { to   = choice A-set
      ; from = λ f x → ∥∥-map (_$ x) f
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      (Π-closure ext 1 λ _ →
       truncation-is-proposition) _ _
  }

-- The axiom of countable choice, stated in a corresponding way.

Axiom-of-countable-choice : (b : Level) → Type (lsuc b)
Axiom-of-countable-choice b =
  {B : ℕ → Type b} → (∀ x → ∥ B x ∥) → ∥ (∀ x → B x) ∥

-- The axiom of countable choice can be turned into a bijection.

countable-choice-bijection :
  {B : ℕ → Type b} →
  Axiom-of-countable-choice b →
  (∀ x → ∥ B x ∥) ↔ ∥ (∀ x → B x) ∥
countable-choice-bijection cc = record
  { surjection = record
    { logical-equivalence = record
      { to   = cc
      ; from = λ f x → ∥∥-map (_$ x) f
      }
    ; right-inverse-of = λ _ → truncation-is-proposition _ _
    }
  ; left-inverse-of = λ _ →
      (Π-closure ext 1 λ _ →
       truncation-is-proposition) _ _
  }

------------------------------------------------------------------------
-- Definitions related to truncated binary sums

-- Truncated binary sums.

infixr 1 _∥⊎∥_

_∥⊎∥_ : Type a → Type b → Type (a ⊔ b)
A ∥⊎∥ B = ∥ A ⊎ B ∥

-- Introduction rules.

∣inj₁∣ : A → A ∥⊎∥ B
∣inj₁∣ = ∣_∣ ∘ inj₁

∣inj₂∣ : B → A ∥⊎∥ B
∣inj₂∣ = ∣_∣ ∘ inj₂

-- _∥⊎∥_ is pointwise propositional.

∥⊎∥-propositional : Is-proposition (A ∥⊎∥ B)
∥⊎∥-propositional = truncation-is-proposition

-- _∥⊎∥_ preserves all kinds of functions.

infixr 1 _∥⊎∥-cong_

_∥⊎∥-cong_ : A₁ ↝[ k ] A₂ → B₁ ↝[ k ] B₂ → A₁ ∥⊎∥ B₁ ↝[ k ] A₂ ∥⊎∥ B₂
A₁↝A₂ ∥⊎∥-cong B₁↝B₂ = ∥∥-cong (A₁↝A₂ ⊎-cong B₁↝B₂)

-- _∥⊎∥_ is commutative.

∥⊎∥-comm : A ∥⊎∥ B ↔ B ∥⊎∥ A
∥⊎∥-comm = ∥∥-cong ⊎-comm

-- If one truncates the types to the left or right of _∥⊎∥_, then one
-- ends up with an isomorphic type.

truncate-left-∥⊎∥ : A ∥⊎∥ B ↔ ∥ A ∥ ∥⊎∥ B
truncate-left-∥⊎∥ =
  inverse $ flatten′ (λ F → F _ ⊎ _) (λ f → ⊎-map f id) [ ∥∥-map inj₁ , ∣inj₂∣ ]

truncate-right-∥⊎∥ : A ∥⊎∥ B ↔ A ∥⊎∥ ∥ B ∥
truncate-right-∥⊎∥ {A = A} {B = B} =
  A ∥⊎∥ B      ↝⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A      ↝⟨ truncate-left-∥⊎∥ ⟩
  ∥ B ∥ ∥⊎∥ A  ↝⟨ ∥⊎∥-comm ⟩□
  A ∥⊎∥ ∥ B ∥  □

-- _∥⊎∥_ is associative.

∥⊎∥-assoc : A ∥⊎∥ (B ∥⊎∥ C) ↔ (A ∥⊎∥ B) ∥⊎∥ C
∥⊎∥-assoc {A = A} {B = B} {C = C} =
  ∥ A ⊎ ∥ B ⊎ C ∥ ∥  ↝⟨ inverse truncate-right-∥⊎∥ ⟩
  ∥ A ⊎ B ⊎ C ∥      ↝⟨ ∥∥-cong ⊎-assoc ⟩
  ∥ (A ⊎ B) ⊎ C ∥    ↝⟨ truncate-left-∥⊎∥ ⟩□
  ∥ ∥ A ⊎ B ∥ ⊎ C ∥  □

-- ⊥ is a left and right identity of _∥⊎∥_ if the other argument is a
-- proposition.

∥⊎∥-left-identity : Is-proposition A → ⊥ {ℓ = ℓ} ∥⊎∥ A ↔ A
∥⊎∥-left-identity {A = A} A-prop =
  ∥ ⊥ ⊎ A ∥  ↝⟨ ∥∥-cong ⊎-left-identity ⟩
  ∥ A ∥      ↝⟨ ∥∥↔ A-prop ⟩□
  A          □

∥⊎∥-right-identity : Is-proposition A → A ∥⊎∥ ⊥ {ℓ = ℓ} ↔ A
∥⊎∥-right-identity {A = A} A-prop =
  A ∥⊎∥ ⊥  ↔⟨ ∥⊎∥-comm ⟩
  ⊥ ∥⊎∥ A  ↔⟨ ∥⊎∥-left-identity A-prop ⟩□
  A        □

-- _∥⊎∥_ is idempotent for propositions.

∥⊎∥-idempotent : Is-proposition A → A ∥⊎∥ A ↔ A
∥⊎∥-idempotent {A = A} A-prop =
  ∥ A ⊎ A ∥  ↝⟨ idempotent ⟩
  ∥ A ∥      ↝⟨ ∥∥↔ A-prop ⟩□
  A          □

-- Sometimes a truncated binary sum is isomorphic to one of its
-- summands.

drop-left-∥⊎∥ :
  Is-proposition B → (A → B) → A ∥⊎∥ B ↔ B
drop-left-∥⊎∥ B-prop A→B =
  _≃_.bijection $
  Eq.⇔→≃ ∥⊎∥-propositional B-prop
    (rec B-prop [ to-implication A→B , id ]) ∣inj₂∣

drop-right-∥⊎∥ :
  Is-proposition A → (B → A) → A ∥⊎∥ B ↔ A
drop-right-∥⊎∥ {A = A} {B = B} A-prop B→A =
  A ∥⊎∥ B  ↝⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A  ↝⟨ drop-left-∥⊎∥ A-prop B→A ⟩□
  A        □

drop-⊥-right-∥⊎∥ :
  Is-proposition A → ¬ B → A ∥⊎∥ B ↔ A
drop-⊥-right-∥⊎∥ A-prop ¬B =
  drop-right-∥⊎∥ A-prop (⊥-elim ∘ ¬B)

drop-⊥-left-∥⊎∥ :
  Is-proposition B → ¬ A → A ∥⊎∥ B ↔ B
drop-⊥-left-∥⊎∥ B-prop ¬A =
  drop-left-∥⊎∥ B-prop (⊥-elim ∘ ¬A)

-- A type of functions from a truncated binary sum to a family of
-- propositions can be expressed as a binary product of function
-- types.

Π∥⊎∥↔Π×Π :
  (∀ x → Is-proposition (P x)) →
  ((x : A ∥⊎∥ B) → P x)
    ↔
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))
Π∥⊎∥↔Π×Π {A = A} {B = B} {P = P} P-prop =
  ((x : A ∥⊎∥ B) → P x)                                ↔⟨ universal-property-Π P-prop ⟩
  ((x : A ⊎ B) → P ∣ x ∣)                              ↝⟨ Π⊎↔Π×Π ext ⟩□
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))  □

-- Two distributivity laws for Σ and _∥⊎∥_.

Σ-∥⊎∥-distrib-left :
  Is-proposition A →
  Σ A (λ x → P x ∥⊎∥ Q x) ↔ Σ A P ∥⊎∥ Σ A Q
Σ-∥⊎∥-distrib-left {P = P} {Q = Q} A-prop =
  (∃ λ x → ∥ P x ⊎ Q x ∥)      ↝⟨ inverse $ ∥∥↔ (Σ-closure 1 A-prop λ _ → ∥⊎∥-propositional) ⟩
  ∥ (∃ λ x → ∥ P x ⊎ Q x ∥) ∥  ↝⟨ flatten′ (λ F → (∃ λ x → F (P x ⊎ Q x))) (λ f → Σ-map id f) (uncurry λ x → ∥∥-map (x ,_)) ⟩
  ∥ (∃ λ x → P x ⊎ Q x) ∥      ↝⟨ ∥∥-cong ∃-⊎-distrib-left ⟩□
  ∥ ∃ P ⊎ ∃ Q ∥                □

Σ-∥⊎∥-distrib-right :
  (∀ x → Is-proposition (P x)) →
  Σ (A ∥⊎∥ B) P ↔ Σ A (P ∘ ∣inj₁∣) ∥⊎∥ Σ B (P ∘ ∣inj₂∣)
Σ-∥⊎∥-distrib-right {A = A} {B = B} {P = P} P-prop =
  _≃_.bijection $
  Eq.⇔→≃ prop₂ prop₁
    (uncurry $
     elim _ (λ _ → Π-closure ext 1 λ _ → prop₁) λ where
       (inj₁ x) y → ∣ inj₁ (x , y) ∣
       (inj₂ x) y → ∣ inj₂ (x , y) ∣)
    (rec prop₂ [ Σ-map ∣inj₁∣ id , Σ-map ∣inj₂∣ id ])
  where
  prop₁ = ∥⊎∥-propositional
  prop₂ = Σ-closure 1 ∥⊎∥-propositional P-prop

-- A variant of one of De Morgan's laws.

¬∥⊎∥¬↔¬× :
  Dec (¬ A) → Dec (¬ B) →
  ¬ A ∥⊎∥ ¬ B ↔ ¬ (A × B)
¬∥⊎∥¬↔¬× {A = A} {B = B} dec-¬A dec-¬B = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec (¬-propositional ext) ¬⊎¬→×¬
      ; from = ∣_∣ ∘ _↠_.from (¬⊎¬↠¬× ext dec-¬A dec-¬B)
      }
    ; right-inverse-of = λ _ → ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _ → ∥⊎∥-propositional _ _
  }

-- If ∥ A ∥ is decided, then A ∥⊎∥ B is equivalent to A ∥⊎∥ ¬ A × B.

∥⊎∥≃∥⊎∥¬× :
  Dec ∥ A ∥ →
  (A ∥⊎∥ B) ≃ (A ∥⊎∥ ¬ A × B)
∥⊎∥≃∥⊎∥¬× (yes ∥A∥) = Eq.⇔→≃
  ∥⊎∥-propositional
  ∥⊎∥-propositional
  (const (∥∥-map inj₁ ∥A∥))
  (id ∥⊎∥-cong proj₂)
∥⊎∥≃∥⊎∥¬× (no ¬∥A∥) = Eq.⇔→≃
  ∥⊎∥-propositional
  ∥⊎∥-propositional
  (id ∥⊎∥-cong (¬∥A∥ ∘ ∣_∣) ,_)
  (id ∥⊎∥-cong proj₂)

-- If ∥ B ∥ is decided, then A ∥⊎∥ B is equivalent to ¬ B × A ∥⊎∥ B.

∥⊎∥≃¬×∥⊎∥ :
  Dec ∥ B ∥ →
  (A ∥⊎∥ B) ≃ (¬ B × A ∥⊎∥ B)
∥⊎∥≃¬×∥⊎∥ {B = B} {A = A} dec-∥B∥ =
  A ∥⊎∥ B        ↔⟨ ∥⊎∥-comm ⟩
  B ∥⊎∥ A        ↝⟨ ∥⊎∥≃∥⊎∥¬× dec-∥B∥ ⟩
  B ∥⊎∥ ¬ B × A  ↔⟨ ∥⊎∥-comm ⟩□
  ¬ B × A ∥⊎∥ B  □

------------------------------------------------------------------------
-- Code related to Erased-singleton

-- A corollary of erased-singleton-with-erased-center-propositional.

↠→↔Erased-singleton :
  {@0 y : B}
  (A↠B : A ↠ B) →
  Very-stableᴱ-≡ B →
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ ↔ Erased-singleton y
↠→↔Erased-singleton {A = A} {y = y} A↠B s =
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥  ↝⟨ ∥∥-cong-⇔ (Surjection.Σ-cong-⇔ A↠B λ _ → F.id) ⟩
  ∥ Erased-singleton y ∥                         ↝⟨ ∥∥↔ (E.erased-singleton-with-erased-center-propositional s) ⟩□
  Erased-singleton y                             □

mutual

  -- The right-to-left direction of the previous lemma does not depend
  -- on the assumption of stability.

  ↠→Erased-singleton→ :
    {@0 y : B}
    (A↠B : A ↠ B) →
    Erased-singleton y →
    ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥
  ↠→Erased-singleton→ = _  -- Agda can infer the definition.

  _ : _↔_.from (↠→↔Erased-singleton A↠B s) x ≡
      ↠→Erased-singleton→ A↠B x
  _ = refl _

-- A corollary of Σ-Erased-Erased-singleton↔ and ↠→↔Erased-singleton.

Σ-Erased-∥-Σ-Erased-≡-∥↔ :
  (A↠B : A ↠ B) →
  Very-stableᴱ-≡ B →
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥) ↔
  B
Σ-Erased-∥-Σ-Erased-≡-∥↔ {A = A} {B = B} A↠B s =
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥)  ↝⟨ (∃-cong λ _ → ↠→↔Erased-singleton A↠B s) ⟩

  (∃ λ (x : Erased B) → Erased-singleton (erased x))        ↝⟨ E.Σ-Erased-Erased-singleton↔ ⟩□

  B                                                         □

mutual

  -- Again the right-to-left direction of the previous lemma does not
  -- depend on the assumption of stability.

  →Σ-Erased-∥-Σ-Erased-≡-∥ :
    (A↠B : A ↠ B) →
    B →
    ∃ λ (x : Erased B) →
      ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥
  →Σ-Erased-∥-Σ-Erased-≡-∥ = _  -- Agda can infer the definition.

  _ : _↔_.from (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) x ≡
      →Σ-Erased-∥-Σ-Erased-≡-∥ A↠B x
  _ = refl _

-- In an erased context the left-to-right direction of
-- Σ-Erased-∥-Σ-Erased-≡-∥↔ returns the erased first component.

@0 to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡ :
  ∀ (A↠B : A ↠ B) (s : Very-stableᴱ-≡ B) x →
  _↔_.to (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) x ≡ erased (proj₁ x)
to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡ A↠B s (E.[ x ] , y) =
  _↔_.to (Σ-Erased-∥-Σ-Erased-≡-∥↔ A↠B s) (E.[ x ] , y)  ≡⟨⟩
  proj₁ (_↔_.to (↠→↔Erased-singleton A↠B s) y)           ≡⟨ erased (proj₂ (_↔_.to (↠→↔Erased-singleton A↠B s) y)) ⟩∎
  x                                                      ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2016-04-18 Issue 1834 regression (extracted from larger test case)
-- {-# OPTIONS -v tc.cover:30 #-}

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

record Stream (A : Set) : Set where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A
open Stream

weird' : (n : ℕ) → Stream ℕ
head (weird' zero)    = zero
tail (weird' zero)    = weird' zero
(     weird' (suc n)) = n ∷ tail (weird' n)

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Unary.Subtype where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Relation.Unary
open import Cubical.Data.Nat

private
  variable
    a ℓ ℓ′ : Level
    A : Type a

Subtype : (P : Pred A ℓ) → Type _
Subtype {A = A} P = Σ[ x ∈ A ] x ∈ P

module _ (P : Pred A ℓ) where

  isOfHLevelSubtype : ∀ n → isOfHLevel (suc n) A → isOfHLevel (suc n) (Subtype P)
  isOfHLevelSubtype n hA = isOfHLevelΣ (suc n) hA (λ _ → isProp→isOfHLevelSuc n (isProp[ P ] _))

  isSetSubtype : isSet A → isSet (Subtype P)
  isSetSubtype = isOfHLevelSubtype 1

inclusion : (P : Pred A ℓ) (Q : Pred A ℓ′) → P ⊆ Q → Subtype P → Subtype Q
inclusion P Q P⊆Q = λ (x , Px) → (x , P⊆Q Px)

⇔-equiv : (P : Pred A ℓ) (Q : Pred A ℓ′) → P ⇔ Q → Subtype P ≃ Subtype Q
⇔-equiv P Q (P⊆Q , Q⊆P) = isoToEquiv (iso (inclusion P Q P⊆Q) (inclusion Q P Q⊆P)
                                            (λ (x , Qx) → cong (x ,_) (Q x .snd _ _))
                                            (λ (x , Px) → cong (x ,_) (P x .snd _ _))
                                       )


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.FunExtEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Vec
open import Cubical.Data.Nat

open import Cubical.Reflection.StrictEquiv

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ : Level

-- Function extensionality is an equivalence
module _ {A : Type ℓ} {B : A → I → Type ℓ₁}
  {f : (x : A) → B x i0} {g : (x : A) → B x i1} where

  funExtEquiv : (∀ x → PathP (B x) (f x) (g x)) ≃ PathP (λ i → ∀ x → B x i) f g
  unquoteDef funExtEquiv = defStrictEquiv funExtEquiv funExt funExt⁻

  funExtPath : (∀ x → PathP (B x) (f x) (g x)) ≡ PathP (λ i → ∀ x → B x i) f g
  funExtPath = ua funExtEquiv

  funExtIso : Iso (∀ x → PathP (B x) (f x) (g x)) (PathP (λ i → ∀ x → B x i) f g)
  funExtIso = iso funExt funExt⁻ (λ x → refl {x = x}) (λ x → refl {x = x})

-- Function extensionality for binary functions
funExt₂ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
          {f : (x : A) → (y : B x) → C x y i0}
          {g : (x : A) → (y : B x) → C x y i1}
          → ((x : A) (y : B x) → PathP (C x y) (f x y) (g x y))
          → PathP (λ i → ∀ x y → C x y i) f g
funExt₂ p i x y = p x y i

-- Function extensionality for binary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → I → Type ℓ₂}
         {f : (x : A) → (y : B x) → C x y i0}
         {g : (x : A) → (y : B x) → C x y i1} where
  private
    appl₂ : PathP (λ i → ∀ x y → C x y i) f g → ∀ x y → PathP (C x y) (f x y) (g x y)
    appl₂ eq x y i = eq i x y

  funExt₂Equiv : (∀ x y → PathP (C x y) (f x y) (g x y)) ≃ (PathP (λ i → ∀ x y → C x y i) f g)
  unquoteDef funExt₂Equiv = defStrictEquiv funExt₂Equiv funExt₂ appl₂

  funExt₂Path : (∀ x y → PathP (C x y) (f x y) (g x y)) ≡ (PathP (λ i → ∀ x y → C x y i) f g)
  funExt₂Path = ua funExt₂Equiv

-- Function extensionality for ternary functions
funExt₃ : {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
          {D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
          {f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
          {g : (x : A) → (y : B x) → (z : C x y) → D x y z i1}
        → ((x : A) (y : B x) (z : C x y) → PathP (D x y z) (f x y z) (g x y z))
        → PathP (λ i → ∀ x y z → D x y z i) f g
funExt₃ p i x y z = p x y z i

-- Function extensionality for ternary functions is an equivalence
module _ {A : Type ℓ} {B : A → Type ℓ₁} {C : (x : A) → B x → Type ℓ₂}
         {D : (x : A) → (y : B x) → C x y → I → Type ℓ₃}
         {f : (x : A) → (y : B x) → (z : C x y) → D x y z i0}
         {g : (x : A) → (y : B x) → (z : C x y) → D x y z i1} where
  private
    appl₃ : PathP (λ i → ∀ x y z → D x y z i) f g → ∀ x y z → PathP (D x y z) (f x y z) (g x y z)
    appl₃ eq x y z i = eq i x y z

  funExt₃Equiv : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≃ (PathP (λ i → ∀ x y z → D x y z i) f g)
  unquoteDef funExt₃Equiv = defStrictEquiv funExt₃Equiv funExt₃ appl₃

  funExt₃Path : (∀ x y z → PathP (D x y z) (f x y z) (g x y z)) ≡ (PathP (λ i → ∀ x y z → D x y z i) f g)
  funExt₃Path = ua funExt₃Equiv

-- n-ary non-dependent funext
nAryFunExt : {X : Type ℓ} {Y : I → Type ℓ₁} (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
           → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
           → PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExt zero fX fY p        = p []
nAryFunExt (suc n) fX fY p i x = nAryFunExt n (fX x) (fY x) (λ xs → p (x ∷ xs)) i

-- n-ary funext⁻
nAryFunExt⁻ : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
           → PathP (λ i → nAryOp n X (Y i)) fX fY
           → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
nAryFunExt⁻ zero fX fY p [] = p
nAryFunExt⁻ (suc n) fX fY p (x ∷ xs) = nAryFunExt⁻ n (fX x) (fY x) (λ i → p i x) xs

nAryFunExtEquiv : (n : ℕ) {X : Type ℓ} {Y : I → Type ℓ₁} (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
  → ((xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs)) ≃ PathP (λ i → nAryOp n X (Y i)) fX fY
nAryFunExtEquiv n {X} {Y} fX fY = isoToEquiv (iso (nAryFunExt n fX fY) (nAryFunExt⁻ n fX fY)
                                              (linv n fX fY) (rinv n fX fY))
  where
  linv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
    (p : PathP (λ i → nAryOp n X (Y i)) fX fY)
    → nAryFunExt n fX fY (nAryFunExt⁻ n fX fY p) ≡ p
  linv zero fX fY p          = refl
  linv (suc n) fX fY p i j x = linv n (fX x) (fY x) (λ k → p k x) i j

  rinv : (n : ℕ) (fX : nAryOp n X (Y i0)) (fY : nAryOp n X (Y i1))
         (p : (xs : Vec X n) → PathP Y (fX $ⁿ xs) (fY $ⁿ map (λ x → x) xs))
       → nAryFunExt⁻ n fX fY (nAryFunExt n fX fY p) ≡ p
  rinv zero fX fY p i []          = p []
  rinv (suc n) fX fY p i (x ∷ xs) = rinv n (fX x) (fY x) (λ ys i → p (x ∷ ys) i) i xs

-- Funext when the domain also depends on the interval

funExtDep : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
  {f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
  → ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
  → PathP (λ i → (x : A i) → B i x) f g
funExtDep {A = A} {B} {f} {g} h i x =
  comp
    (λ k → B i (coei→i A i x k))
    (λ k → λ
      { (i = i0) → f (coei→i A i0 x k)
      ; (i = i1) → g (coei→i A i1 x k)
      })
    (h (λ j → coei→j A i j x) i)

funExtDep⁻ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
  {f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
  → PathP (λ i → (x : A i) → B i x) f g
  → ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
funExtDep⁻ q p i = q i (p i)

funExtDepEquiv : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ₁}
  {f : (x : A i0) → B i0 x} {g : (x : A i1) → B i1 x}
  → ({x₀ : A i0} {x₁ : A i1} (p : PathP A x₀ x₁) → PathP (λ i → B i (p i)) (f x₀) (g x₁))
  ≃ PathP (λ i → (x : A i) → B i x) f g
funExtDepEquiv {A = A} {B} {f} {g} = isoToEquiv isom
  where
  open Iso
  isom : Iso _ _
  isom .fun = funExtDep
  isom .inv = funExtDep⁻
  isom .rightInv q m i x =
    comp
      (λ k → B i (coei→i A i x (k ∨ m)))
      (λ k → λ
        { (i = i0) → f (coei→i A i0 x (k ∨ m))
        ; (i = i1) → g (coei→i A i1 x (k ∨ m))
        ; (m = i1) → q i x
        })
      (q i (coei→i A i x m))
  isom .leftInv h m p i =
    comp
      (λ k → B i (lemi→i m k))
      (λ k → λ
        { (i = i0) → f (lemi→i m k)
        ; (i = i1) → g (lemi→i m k)
        ; (m = i1) → h p i
        })
      (h (λ j → lemi→j j m) i)
    where
    lemi→j : ∀ j → coei→j A i j (p i) ≡ p j
    lemi→j j =
      coei→j (λ k → coei→j A i k (p i) ≡ p k) i j (coei→i A i (p i))

    lemi→i : PathP (λ m → lemi→j i m ≡ p i) (coei→i A i (p i)) refl
    lemi→i =
      sym (coei→i (λ k → coei→j A i k (p i) ≡ p k) i (coei→i A i (p i)))
      ◁ λ m k → lemi→j i (m ∨ k)

heteroHomotopy≃Homotopy : {A : I → Type ℓ} {B : (i : I) → Type ℓ₁}
  {f : A i0 → B i0} {g : A i1 → B i1}
  → ({x₀ : A i0} {x₁ : A i1} → PathP A x₀ x₁ → PathP B (f x₀) (g x₁))
  ≃ ((x₀ : A i0) → PathP B (f x₀) (g (transport (λ i → A i) x₀)))
heteroHomotopy≃Homotopy {A = A} {B} {f} {g} = isoToEquiv isom
  where
  open Iso
  isom : Iso _ _
  isom .fun h x₀ = h (isContrSinglP A x₀ .fst .snd)
  isom .inv k {x₀} {x₁} p =
    subst (λ fib → PathP B (f x₀) (g (fib .fst))) (isContrSinglP A x₀ .snd (x₁ , p)) (k x₀)
  isom .rightInv k = funExt λ x₀ →
    cong (λ α → subst (λ fib → PathP B (f x₀) (g (fib .fst))) α (k x₀))
      (isProp→isSet isPropSinglP (isContrSinglP A x₀ .fst) _
        (isContrSinglP A x₀ .snd (isContrSinglP A x₀ .fst))
        refl)
    ∙ transportRefl (k x₀)
  isom .leftInv h j {x₀} {x₁} p =
    transp
      (λ i → PathP B (f x₀) (g (isContrSinglP A x₀ .snd (x₁ , p) (i ∨ j) .fst)))
      j
      (h (isContrSinglP A x₀ .snd (x₁ , p) j .snd))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module Data.Num.Bijection where

open import Data.Num.Core
open import Data.Num.Surjection
open import Data.Num.Injection

open import Data.Nat
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)

open import Function.Bijection
open Bijective

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Nullary.Negation

data BijectionView : ℕ → ℕ → ℕ → Set where
    Bij     : ∀ {b d o} → SurjCond b d o → InjCond b d o → BijectionView b d o
    NonSurj : ∀ {b d o} → NonSurjCond b d o              → BijectionView b d o
    NonInj  : ∀ {b d o} → NonInjCond b d o               → BijectionView b d o

bijectionView : (b d o : ℕ) → BijectionView b d o
bijectionView b d o with surjectionView b d o | injectionView b d o
bijectionView b d o | Surj c₁    | Inj c₂    = Bij c₁ c₂
bijectionView b d o | Surj _     | NonInj c₁ = NonInj c₁
bijectionView b d o | NonSurj c₁ | _         = NonSurj c₁

IsBijective : ℕ → ℕ → ℕ → Set
IsBijective b d o with bijectionView b d o
IsBijective b d o | Bij _ _   = ⊤
IsBijective b d o | NonSurj _ = ⊥
IsBijective b d o | NonInj _  = ⊥

SurjCond∧InjCond⇒Bijective : ∀ {b} {d} {o} → SurjCond b d o → InjCond b d o → Bijective (Num⟶ℕ b d o)
SurjCond∧InjCond⇒Bijective surjCond injCond = record
    { injective = InjCond⇒Injective injCond
    ; surjective = SurjCond⇒Surjective surjCond
    }

NonSurjCond⇏Bijective : ∀ {b} {d} {o} → NonSurjCond b d o → ¬ (Bijective (Num⟶ℕ b d o))
NonSurjCond⇏Bijective reason claim = NonSurjCond⇏Surjective reason (surjective claim)

NonInjCond⇏Bijective : ∀ {b} {d} {o} → NonInjCond b d o → ¬ (Bijective (Num⟶ℕ b d o))
NonInjCond⇏Bijective reason claim = NonInjCond⇏Injective reason (injective claim)

Bijective? : ∀ b d o → Dec (Bijective (Num⟶ℕ b d o))
Bijective? b d o with bijectionView b d o
Bijective? b d o | Bij surjCond injCond = yes (record
    { injective = InjCond⇒Injective injCond
    ; surjective = SurjCond⇒Surjective surjCond
    })
Bijective? b d o | NonSurj reason       = no (NonSurjCond⇏Bijective reason)
Bijective? b d o | NonInj reason        = no (NonInjCond⇏Bijective reason)

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Utils where

open import Relation.Binary.PropositionalEquality

open import Data.List

listHeadEq : ∀ {α} {A : Set α} {x y : A} -> {xt yt : List A} -> x ∷ xt ≡ y ∷ yt -> x ≡ y
listHeadEq refl = refl

listTailEq : ∀ {α} {A : Set α} {x y : A} -> {xt yt : List A} -> x ∷ xt ≡ y ∷ yt -> xt ≡ yt
listTailEq refl = refl

max_stars_repo_name: JoeyEremondi/agda-parikh

max_issues_repo_name: JoeyEremondi/agda-parikh

max_forks_repo_name: JoeyEremondi/agda-parikh


text:
module trie where

open import bool
open import char
open import list
open import maybe
open import product
open import string
open import unit

cal : Set → Set
cal A = 𝕃 (char × A)

empty-cal : ∀{A : Set} → cal A
empty-cal = []

cal-lookup : ∀ {A : Set} → cal A → char → maybe A
cal-lookup [] _ = nothing
cal-lookup ((c , a) :: l) c' with c =char c'
... | tt = just a
... | ff = cal-lookup l c'

cal-insert : ∀ {A : Set} → cal A → char → A → cal A
cal-insert [] c a = (c , a) :: []
cal-insert ((c' , a') :: l) c a with c =char c'
... | tt = (c , a) :: l
... | ff = (c' , a') :: (cal-insert l c a)

cal-remove : ∀ {A : Set} → cal A → char → cal A
cal-remove [] _ = []
cal-remove ((c , a) :: l) c' with c =char c'
... | tt = cal-remove l c'
... | ff = (c , a) :: cal-remove l c'

cal-add : ∀{A : Set} → cal A → char → A → cal A
cal-add l c a = (c , a) :: l

test-cal-insert = cal-insert (('a' , 1) :: ('b' , 2) :: []) 'b' 20

data trie (A : Set) : Set where
  Node : maybe A → cal (trie A) → trie A

empty-trie : ∀{A : Set} → trie A
empty-trie = (Node nothing empty-cal)

trie-lookup-h : ∀{A : Set} → trie A → 𝕃 char → maybe A
trie-lookup-h (Node odata ts) (c :: cs) with cal-lookup ts c
trie-lookup-h (Node odata ts) (c :: cs) | nothing = nothing
trie-lookup-h (Node odata ts) (c :: cs) | just t = trie-lookup-h t cs
trie-lookup-h (Node odata ts) [] = odata

trie-lookup : ∀{A : Set} → trie A → string → maybe A
trie-lookup t s = trie-lookup-h t (string-to-𝕃char s)

trie-contains : ∀{A : Set} → trie A → string → 𝔹
trie-contains t s with trie-lookup t s
trie-contains t s | nothing = ff
trie-contains t s | just _ = tt

trie-insert-h : ∀{A : Set} → trie A → 𝕃 char → A → trie A
trie-insert-h (Node odata ts) [] x = (Node (just x) ts)
trie-insert-h (Node odata ts) (c :: cs) x with cal-lookup ts c
trie-insert-h (Node odata ts) (c :: cs) x | just t =
  (Node odata (cal-insert ts c (trie-insert-h t cs x)))
trie-insert-h (Node odata ts) (c :: cs) x | nothing =
  (Node odata (cal-add ts c (trie-insert-h empty-trie cs x)))

trie-insert : ∀{A : Set} → trie A → string → A → trie A
trie-insert t s x = trie-insert-h t (string-to-𝕃char s) x

trie-remove-h : ∀{A : Set} → trie A → 𝕃 char → trie A
trie-remove-h (Node odata ts) (c :: cs) with cal-lookup ts c
trie-remove-h (Node odata ts) (c :: cs) | nothing = Node odata ts
trie-remove-h (Node odata ts) (c :: cs) | just t = Node odata (cal-insert ts c (trie-remove-h t cs))
trie-remove-h (Node odata ts) [] = Node nothing ts

trie-remove : ∀{A : Set} → trie A → string → trie A
trie-remove t s = trie-remove-h t (string-to-𝕃char s)

trie-map : ∀{A B : Set} → (A → B) → trie A → trie B
trie-cal-map : ∀{A B : Set} → (A → B) → cal (trie A) → cal (trie B)
trie-map f (Node x x₁) = Node (maybe-map f x) (trie-cal-map f x₁)
trie-cal-map f [] = []
trie-cal-map f ((c , t) :: cs) =
  (c , trie-map f t) :: trie-cal-map f cs

trie-to-string-h : ∀{A : Set} → string → (A → string) → trie A → 𝕃 char → string
trie-cal-to-string-h : ∀{A : Set} → string → (A → string) → cal (trie A) → 𝕃 char → string
trie-to-string-h sep d (Node (just x) c) prev-str =
  (𝕃char-to-string (reverse prev-str)) ^ sep ^ (d x) ^ "\n" ^ (trie-cal-to-string-h sep d c prev-str)
trie-to-string-h sep d (Node nothing c) prev-str = trie-cal-to-string-h sep d c prev-str
trie-cal-to-string-h sep d [] prev-str = ""
trie-cal-to-string-h sep d ((c , t) :: cs) prev-str =
  (trie-to-string-h sep d t (c :: prev-str)) ^ (trie-cal-to-string-h sep d cs prev-str)

{- trie-to-string sep d t returns a string representation of the trie t,
   where each mapping from string s to data x is printed as
     s sep d x
   where sep is a string and d returns a string for any element A of the trie. -}
trie-to-string : ∀{A : Set} → string → (A → string) → trie A → string
trie-to-string sep d t = trie-to-string-h sep d t []

trie-mappings-h : ∀{A : Set} → trie A → 𝕃 char → 𝕃 (string × A)
trie-cal-mappings-h : ∀{A : Set} → cal (trie A) → 𝕃 char → 𝕃 (string × A)
trie-mappings-h (Node (just x) c) prev-str = (𝕃char-to-string (reverse prev-str) , x) :: (trie-cal-mappings-h c prev-str)
trie-mappings-h (Node nothing c) prev-str = (trie-cal-mappings-h c prev-str)
trie-cal-mappings-h [] prev-str = []
trie-cal-mappings-h ((c , t) :: cs) prev-str = trie-mappings-h t (c :: prev-str) ++ (trie-cal-mappings-h cs prev-str)

trie-mappings : ∀{A : Set} → trie A → 𝕃 (string × A)
trie-mappings t = trie-mappings-h t []

-- return a list of all the strings which have associated data in the trie
trie-strings : ∀{A : Set} → trie A → 𝕃 string
trie-strings t = map fst (trie-mappings t)

trie-nonempty : ∀{A : Set} → trie A → 𝔹
trie-cal-nonempty : ∀{A : Set} → cal (trie A) → 𝔹
trie-nonempty (Node (just x) t) = tt
trie-nonempty (Node nothing c) = trie-cal-nonempty c
trie-cal-nonempty [] = ff
trie-cal-nonempty ((a , t) :: c) = trie-nonempty t || trie-cal-nonempty c

----------------------------------------------------------------------
-- stringset
----------------------------------------------------------------------

stringset : Set
stringset = trie ⊤

stringset-contains : stringset → string → 𝔹
stringset-contains ss s = trie-contains ss s

stringset-insert : stringset → string → stringset
stringset-insert ss s = trie-insert ss s triv

stringset-remove : stringset → string → stringset
stringset-remove ss s = trie-remove ss s

stringset-insert𝕃 : stringset → 𝕃 char → stringset
stringset-insert𝕃 ss s = trie-insert-h ss s triv

empty-stringset : stringset
empty-stringset = empty-trie

stringset-insert* : stringset → 𝕃 string → stringset
stringset-insert* s [] = s
stringset-insert* s (x :: xs) = stringset-insert (stringset-insert* s xs) x

stringset-strings : ∀{A : Set} → trie A → 𝕃 string
stringset-strings t = map fst (trie-mappings t)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import HoTT

-- TODO Is it possible to have a more generic [→-group] construction?

module groups.ToOmega where

⊙→Ω-group-structure : ∀ {i j} (X : Ptd i) (Y : Ptd j)
  → GroupStructure (X ⊙→ ⊙Ω Y)
⊙→Ω-group-structure X Y = record {M} where
  module M where
    ident : (X ⊙→ ⊙Ω Y)
    ident = ⊙cst

    comp : (X ⊙→ ⊙Ω Y) → (X ⊙→ ⊙Ω Y) → (X ⊙→ ⊙Ω Y)
    comp F G = ⊙Ω-∙ ⊙∘ ⊙fanout F G

    inv : (X ⊙→ ⊙Ω Y) → (X ⊙→ ⊙Ω Y)
    inv F = (! ∘ fst F) , ap ! (snd F)
    abstract
      unit-l-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
        → ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt {a₀ = idp} idp α) idp == α
      unit-l-lemma idp = idp

      unit-l : ∀ G → comp ident G == G
      unit-l G = ⊙λ=' (λ _ → idp) (unit-l-lemma (snd G))

      assoc-lemma : ∀ {i} {A : Type i} {x : A} {p q r : x == x}
        (α : p == idp) (β : q == idp) (γ : r == idp)
        →  ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt (⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt α β) idp) γ) idp
        == ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt α (⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt β γ) idp)) idp
         [ _== idp ↓ ∙-assoc p q r ]
      assoc-lemma idp idp idp = idp

      assoc : ∀ F G H → comp (comp F G) H == comp F (comp G H)
      assoc F G H = ⊙λ='
        (λ x → ∙-assoc (fst F x) (fst G x) (fst H x))
        (assoc-lemma (snd F) (snd G) (snd H))

      inv-l-lemma : ∀ {i} {A : Type i} {x : A} {p : x == x} (α : p == idp)
        → ⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt (ap ! α) α) idp == idp [ _== idp ↓ !-inv-l p ]
      inv-l-lemma idp = idp

      inv-l : ∀ F → comp (inv F) F == ident
      inv-l F = ⊙λ=' (!-inv-l ∘ fst F) (inv-l-lemma (snd F))

Trunc-⊙→Ω-group : ∀ {i j} (X : Ptd i) (Y : Ptd j) → Group (lmax i j)
Trunc-⊙→Ω-group X Y = Trunc-group (⊙→Ω-group-structure X Y)

{- [Trunc-→Ω-group] is functorial in the first argument -}

⊙→Ω-group-structure-fmap-dom : ∀ {i j k} {X : Ptd i} {Y : Ptd j}
  (f : X ⊙→ Y) (Z : Ptd k)
  → (⊙→Ω-group-structure Y Z →ᴳˢ ⊙→Ω-group-structure X Z)
⊙→Ω-group-structure-fmap-dom F Z = group-structure-hom (_⊙∘ F)
  (λ g₁ g₂ → ⊙λ= (⊙∘-assoc ⊙Ω-∙ (⊙fanout g₁ g₂) F)
           ∙ ap (⊙Ω-∙ ⊙∘_) (⊙fanout-pre∘ g₁ g₂ F))

Trunc-⊙→Ω-group-fmap-dom : ∀ {i j k} {X : Ptd i} {Y : Ptd j}
  (f : X ⊙→ Y) (Z : Ptd k)
  → (Trunc-⊙→Ω-group Y Z →ᴳ Trunc-⊙→Ω-group X Z)
Trunc-⊙→Ω-group-fmap-dom F Z =
  Trunc-group-fmap $ ⊙→Ω-group-structure-fmap-dom F Z

⊙→Ω-group-structure-emap-dom : ∀ {i j k} {X : Ptd i} {Y : Ptd j}
  (e : X ⊙≃ Y) (Z : Ptd k)
  → (⊙→Ω-group-structure Y Z ≃ᴳˢ ⊙→Ω-group-structure X Z)
⊙→Ω-group-structure-emap-dom (F , F-is-equiv) Z =
  ⊙→Ω-group-structure-fmap-dom F Z , pre⊙∘-is-equiv (F , F-is-equiv)

Trunc-⊙→Ω-group-emap-dom : ∀ {i j k} {X : Ptd i} {Y : Ptd j}
  (e : X ⊙≃ Y) (Z : Ptd k)
  → (Trunc-⊙→Ω-group Y Z ≃ᴳ Trunc-⊙→Ω-group X Z)
Trunc-⊙→Ω-group-emap-dom F Z =
  Trunc-group-emap $ ⊙→Ω-group-structure-emap-dom F Z

Trunc-⊙→Ω-group-fmap-dom-idf : ∀ {i j} {X : Ptd i} (Y : Ptd j)
  → Trunc-⊙→Ω-group-fmap-dom (⊙idf X) Y == idhom (Trunc-⊙→Ω-group X Y)
Trunc-⊙→Ω-group-fmap-dom-idf Y = group-hom= $ λ= $ Trunc-elim (λ _ → idp)

Trunc-⊙→Ω-group-fmap-dom-∘ : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y) (W : Ptd l)
  → Trunc-⊙→Ω-group-fmap-dom (g ⊙∘ f) W
    == Trunc-⊙→Ω-group-fmap-dom f W ∘ᴳ Trunc-⊙→Ω-group-fmap-dom g W
Trunc-⊙→Ω-group-fmap-dom-∘ g f W = group-hom= $ λ= $
  Trunc-elim (λ h → ap [_] (! (⊙λ= $ ⊙∘-assoc h g f)))

⊙→Ω-group-structure-fmap-codom : ∀ {i j k} (X : Ptd i) {Y : Ptd j} {Z : Ptd k}
  → Y ⊙→ Z → (⊙→Ω-group-structure X Y →ᴳˢ ⊙→Ω-group-structure X Z)
⊙→Ω-group-structure-fmap-codom X {Y} {Z} F = group-structure-hom
    (⊙Ω-fmap F ⊙∘_)
    (λ G H → ⊙λ=' (λ x → Ω-fmap-∙ F ((fst G) x) ((fst H) x))
                  (lemma (snd F) (snd G) (snd H)))
    where
      abstract
        lemma : ∀ {ptZ : de⊙ Z} (α : (fst F) (pt Y) == ptZ)
          {gpt hpt : Ω Y} (β : gpt == idp) (γ : hpt == idp)
          →  ⊙∘-pt (Ω-fmap (fst F , α)) (⊙∘-pt (fst ⊙Ω-∙) (⊙fanout-pt β γ) idp) (snd (⊙Ω-fmap (fst F , α)))
          == ⊙∘-pt (fst ⊙Ω-∙)
               (⊙fanout-pt
                 (⊙∘-pt (Ω-fmap (fst F , α)) β (snd (⊙Ω-fmap (fst F , α))))
                 (⊙∘-pt (Ω-fmap (fst F , α)) γ (snd (⊙Ω-fmap (fst F , α))))
               ) idp
           [ _== idp ↓ Ω-fmap-∙ (fst F , α) gpt hpt ]
        lemma idp idp idp = idp

Trunc-⊙→Ω-group-fmap-codom : ∀ {i j k} (X : Ptd i) {Y : Ptd j} {Z : Ptd k}
  → Y ⊙→ Z → Trunc-⊙→Ω-group X Y →ᴳ Trunc-⊙→Ω-group X Z
Trunc-⊙→Ω-group-fmap-codom X = Trunc-group-fmap ∘ ⊙→Ω-group-structure-fmap-codom X

⊙→Ω-group-structure-emap-codom : ∀ {i j k} (X : Ptd i) {Y : Ptd j} {Z : Ptd k}
  → Y ⊙≃ Z → ⊙→Ω-group-structure X Y ≃ᴳˢ ⊙→Ω-group-structure X Z
⊙→Ω-group-structure-emap-codom X (F , F-is-equiv) =
  ⊙→Ω-group-structure-fmap-codom X F , post⊙∘-is-equiv (⊙Ω-emap (F , F-is-equiv))

Trunc-⊙→Ω-group-emap-codom : ∀ {i j k} (X : Ptd i) {Y : Ptd j} {Z : Ptd k}
  → Y ⊙≃ Z → Trunc-⊙→Ω-group X Y ≃ᴳ Trunc-⊙→Ω-group X Z
Trunc-⊙→Ω-group-emap-codom X = Trunc-group-emap ∘ ⊙→Ω-group-structure-emap-codom X

-- TODO Check naming convensions.
-- TODO Use [CommSquareᴳ].
Trunc-⊙→Ω-group-fmap-nat : ∀ {i₀ i₁ j₀ j₁}
  {X₀ : Ptd i₀} {X₁ : Ptd i₁} {Y₀ : Ptd j₀} {Y₁ : Ptd j₁}
  (F : X₀ ⊙→ X₁) (G : Y₀ ⊙→ Y₁)
  →  Trunc-⊙→Ω-group-fmap-dom   F  Y₁ ∘ᴳ Trunc-⊙→Ω-group-fmap-codom X₁ G
  == Trunc-⊙→Ω-group-fmap-codom X₀ G  ∘ᴳ Trunc-⊙→Ω-group-fmap-dom   F  Y₀
Trunc-⊙→Ω-group-fmap-nat F G = group-hom= $ λ= $ Trunc-elim
  (λ k → ap [_] $ ⊙λ= $ ⊙∘-assoc (⊙Ω-fmap G) k F)

{- Not used.
Trunc-⊙→Ω-group-emap-nat : ∀ {i₀ i₁ j₀ j₁}
  {X₀ : Ptd i₀} {X₁ : Ptd i₁} {Y₀ : Ptd j₀} {Y₁ : Ptd j₁}
  (F : X₀ ⊙≃ X₁) (G : Y₀ ⊙≃ Y₁)
  →  Trunc-⊙→Ω-group-emap-dom   F  Y₁ ∘ᴳ Trunc-⊙→Ω-group-emap-codom X₁ G
  == Trunc-⊙→Ω-group-emap-codom X₀ G  ∘ᴳ Trunc-⊙→Ω-group-emap-dom   F  Y₀
Trunc-⊙→Ω-group-emap-nat F G = group-hom=-to-iso= $ Trunc-⊙→Ω-group-fmap-nat F G
-}

{- Pointed maps out of bool -}

Trunc-⊙Bool→Ω-iso-π₁ : ∀ {i} (X : Ptd i)
  → Trunc-⊙→Ω-group ⊙Bool X ≃ᴳ πS 0 X
Trunc-⊙Bool→Ω-iso-π₁ {i} X = Trunc-group-emap (≃-to-≃ᴳˢ (⊙Bool→-equiv-idf (⊙Ω X)) (λ _ _ → idp))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Proc where

open import Basics

module ProcDef (U : Set)(T : U -> Set)(Name : U -> Set) where

  LT : U -> Set
  LT a = Lift (T a)

  record Tran (a b : U) : Set where
    field
      upV   : T b -> LT a
      downV : T a -> LT b

  mapLT : {a b : U} -> (T a -> LT b) -> List (T a) -> List (T b)
  mapLT f [] = []
  mapLT f (x :: xs) with f x
  ... | bot    = mapLT f xs
  ... | lift y = y :: mapLT f xs

  infixr 40 _!_ _!_+_
  infix  40 >_
  infixr 30 _||_ _/|_

  data Proc (a : U) : Set where
    o     : Proc a
    >_    : (T a -> Proc a) -> Proc a
    _!_   : LT a -> Proc a -> Proc a
    _!_+_ : LT a -> Proc a -> (T a -> Proc a) -> Proc a
    _||_  : Proc a -> Proc a -> Proc a
    _/|_  : {b : U} -> Tran a b -> Proc b -> Proc a
    def   : Name a -> Proc a

  Env : Set
  Env = (a : U) -> Name a -> Proc a

record Param : Set1 where
  field
    U    : Set
    T    : U -> Set
    Name : U -> Set
    env  : ProcDef.Env U T Name

module Process (param : Param) where

  private open module Par = Param param      public
  private open module Pro = ProcDef U T Name public

  infixr 40 _!g_ _!_+g_
  infix  40 >g_
  infixr 30 _||g_ _/|g_

  data Guard {a : U} : Proc a -> Set where
    og     : Guard o
    >g_    : (f : T a -> Proc a)                          -> Guard (> f)
    _!g_   : (w : LT a)(p : Proc a)                       -> Guard (w ! p)
    _!_+g_ : (w : LT a)(p : Proc a)(f : T a -> Proc a)    -> Guard (w ! p + f)
    _||g_  : {p1 p2 : Proc a} -> Guard p1 -> Guard p2     -> Guard (p1 || p2)
    _/|g_  : {b : U}(φ : Tran a b){p : Proc b} -> Guard p -> Guard (φ /| p)
    defg   : (x : Name a) -> Guard (env a x)              -> Guard (def x)

  infix 20 _-[_]->_ _-!_!->_

  open Tran

  data _-[_]->_ {a : U} : Proc a -> LT a -> Proc a -> Set where
    qtau   : {p : Proc a}                    -> p -[ bot ]-> p
    rx-o   : {v : T a}                       -> o -[ lift v ]-> o
    rx-!   : {v : T a}{w : LT a}{p : Proc a} -> w ! p -[ lift v ]-> w ! p
    rx->   : {v : T a}{f : T a -> Proc a}    -> > f -[ lift v ]-> f v
    rx-+   : {v : T a}{w : LT a}{p : Proc a}{f : T a -> Proc a} ->
             w ! p + f -[ lift v ]-> f v
    rx-||  : {v : T a}{p1 p2 p1' p2' : Proc a} ->
             p1 -[ lift v ]-> p1' ->
             p2 -[ lift v ]-> p2' ->
             p1 || p2 -[ lift v ]-> p1' || p2'
    rx-/|  : {v : T a}{b : U}{φ : Tran a b}{q q' : Proc b} ->
             q -[ downV φ v ]-> q'   ->
             φ /| q -[ lift v ]-> φ /| q'
    rx-def : {v : T a}{p : Proc a}{x : Name a} ->
             env a x -[ lift v ]-> p ->
             def x -[ lift v ]-> p

  data _-!_!->_ {a : U} : Proc a -> LT a -> Proc a -> Set where
    tx-!   : {w : LT a}{p : Proc a} -> w ! p -! w !-> p
    tx-+   : {w : LT a}{p : Proc a}{f : T a -> Proc a} ->
             w ! p + f -! w !-> p
    tx-!|  : {w : LT a}{p p' q q' : Proc a} ->
             p -! w !-> p' -> q -[ w ]-> q' ->
             p || q -! w !-> p' || q'
    tx-|!  : {w : LT a}{p p' q q' : Proc a} ->
             p -[ w ]-> p' -> q -! w !-> q' ->
             p || q -! w !-> p' || q'
    tx-/|  : {b : U}{w : LT b}{φ : Tran a b}{q q' : Proc b} ->
             q -! w !-> q' ->
             φ /| q -! upV φ =<< w !-> φ /| q'
    tx-def : {w : LT a}{p : Proc a}{x : Name a} ->
             env a x -! w !-> p ->
             def x -! w !-> p

  data Silent {a : U} : Proc a -> Set where
    silent-o   : Silent o
    silent->   : {f : T a -> Proc a} -> Silent (> f)
    silent-||  : {p1 p2 : Proc a} ->
                 Silent p1 -> Silent p2 -> Silent (p1 || p2)
    silent-def : {x : Name a} ->
                 Silent (env _ x) -> Silent (def x)
    silent-/|  : {b : U}{φ : Tran a b}{p : Proc b} ->
                 Silent p -> Silent (φ /| p)

  infixr 40 _>!>_ _>*>_

  data _-[_]->*_ {a : U} : Proc a -> List (T a) -> Proc a -> Set where
    rnop  : {p : Proc a} -> p -[ [] ]->* p
    _>?>_ : {p q r : Proc a}{x : T a}{xs : List (T a)} ->
            p -[ lift x  ]->  q ->
            q -[ xs      ]->* r ->
            p -[ x :: xs ]->* r

  rx-||* : forall {a xs}{p1 p2 q1 q2 : Proc a} ->
           p1 -[ xs ]->* p2 ->
           q1 -[ xs ]->* q2 ->
           p1 || q1 -[ xs ]->* p2 || q2
  rx-||* rnop rnop = rnop
  rx-||* (s1 >?> t1) (s2 >?> t2) = rx-|| s1 s2 >?> rx-||* t1 t2

  rx-/|* : forall {a b xs}{φ : Tran a b}{p q : Proc b} ->
           p -[ mapLT (downV φ) xs ]->* q ->
           φ /| p -[ xs ]->* φ /| q
  rx-/|* {xs = []}      rnop      = rnop
  rx-/|* {xs = x :: xs}{φ = φ} t  with it (downV φ x) refl
  rx-/|* {xs = x :: xs}{φ}{p}{q} t | it bot eq =
      rx-/| (lem₁ eq) >?> rx-/|* (lem₂ eq t)
    where
      lem₁ : forall {w} -> w == bot -> p -[ w ]-> p
      lem₁ refl = qtau

      lem₂ : downV φ x == bot ->
             p -[ mapLT (downV φ) (x :: xs) ]->* q ->
             p -[ mapLT (downV φ) xs ]->* q
      lem₂ eq   h with downV φ x
      lem₂ refl h | .bot = h
  rx-/|* {a}{b}{x :: xs}{φ}{p}{q} t | it (lift y) eq =
      rx-/| (lem₁ eq t) >?> rx-/|* (lem₂ eq t)
    where
      Eqn = downV φ x == lift y
      Asm = p -[ mapLT (downV φ) (x :: xs) ]->* q

      r : Eqn -> Asm -> Proc b
      r eq t with downV φ x
      r refl (_>?>_ {q = q} _ _) | ._ = q

      lem₁ : (eq : Eqn)(h : Asm) -> p -[ downV φ x ]-> r eq h
      lem₁ eq   t with downV φ x
      lem₁ refl (s >?> _) | ._ = s

      lem₂ : (eq : Eqn)(h : Asm) -> r eq h -[ mapLT (downV φ) xs ]->* q
      lem₂ eq   t with downV φ x
      lem₂ refl (_ >?> t) | ._ = t

  data _-!_!->*_ {a : U} : Proc a -> List (T a) -> Proc a -> Set where
    tnop : {p : Proc a} -> p -! [] !->* p
    _>!>_ : {p q r : Proc a}{x : T a}{xs : List (T a)} ->
            p -! lift x  !->  q ->
            q -! xs      !->* r ->
            p -! x :: xs !->* r
    _>*>_ : {p q r : Proc a}{xs : List (T a)} ->
            p -! bot !->  q ->
            q -! xs  !->* r ->
            p -! xs  !->* r

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Relation.Binary.Core

module Bound.Total.Order.Properties {A : Set}
                 (_≤_ : A → A → Set)
                 (trans≤ : Transitive _≤_)  where

open import Bound.Total A
open import Bound.Total.Order _≤_

lemma-LeB≤ : {x y : A} → LeB (val x) (val y) → x ≤ y
lemma-LeB≤ (lexy x≤y) = x≤y

transLeB : {a b c : Bound} → LeB a b → LeB b c → LeB a c
transLeB lebx _ = lebx
transLeB _ lext = lext
transLeB (lexy x≤y) (lexy y≤z) = lexy (trans≤ x≤y y≤z)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module STLC.Examples where

-- This file contains a few example programs for the definitional
-- interpreter for STLC in Section 2.

open import Data.Maybe.Base
open import Data.List.Base
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.List.Membership.Propositional
open import Data.Integer hiding (suc)
open import Relation.Binary.PropositionalEquality -- for de Bruijn numerals

open import STLC.Semantics

-- The identity function: λ x . x
--
-- Variables are represented as de Bruijn indices, assumed to have
-- been elaborated from a surface language with names to the nameless
-- representation used in the abstract syntax in `STLC.Semantics`.
idexpr : Expr [] (unit ⇒ unit)
idexpr = ƛ (var (here refl))

-- id () = ()
test-idexpr : eval 2 (idexpr · unit) [] ≡ just unit
test-idexpr = refl

-- curried addition: λ x . λ y . y + x
curry+ : Expr [] (int ⇒ (int ⇒ int))
curry+ = ƛ (ƛ (iop _+_ (var (here refl)) (var (there (here refl)))))

-- 1 + 1 = 2
test-curry+ : eval 3 ((curry+ · (num (+ 1))) · (num (+ 1))) [] ≡ just (num (+ 2))
test-curry+ = refl


text:
------------------------------------------------------------------------------
-- The predicate names are translated as constant names
------------------------------------------------------------------------------

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

module PredicateNameConstantName where

postulate
  D : Set
  P : D → Set

postulate foo : ∀ d → P d → P d
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Simple where

postulate
  Nat  : Set
  zero : Nat

  -- we want
  -- ?0 zero = zero
  -- and then
  -- ?0 x = x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.QuadTree.Implementation.PropDepthRelation where

open import Haskell.Prelude
open import Data.Logic

---- Properties of depth

lteTransitiveWeird : (x y d : Nat) -> IsTrue (x < y) -> (y <= d) ≡ ((x <= d) && (y <= d))
lteTransitiveWeird zero zero zero xlty = refl
lteTransitiveWeird zero zero (suc d) xlty = refl
lteTransitiveWeird zero (suc y) zero xlty = refl
lteTransitiveWeird zero (suc y) (suc d) xlty = refl
lteTransitiveWeird (suc x) (suc y) zero xlty = refl
lteTransitiveWeird (suc x) (suc y) (suc d) xlty = lteTransitiveWeird x y d xlty

lteTransitiveWeirdInv : (x y d : Nat) -> IsFalse (x < y) -> (x <= d) ≡ ((x <= d) && (y <= d))
lteTransitiveWeirdInv zero zero zero xnlty = refl
lteTransitiveWeirdInv zero zero (suc d) xnlty = refl
lteTransitiveWeirdInv (suc x) zero zero xnlty = refl
lteTransitiveWeirdInv (suc x) zero (suc d) xnlty =
  begin
    (suc x <= suc d)
  =⟨ sym $ boolAndTrue (suc x <= suc d) ⟩
    (suc x <= suc d) && true
  =⟨⟩
    ((suc x <= suc d) && (zero <= suc d))
  end
lteTransitiveWeirdInv (suc x) (suc y) zero xnlty = refl
lteTransitiveWeirdInv (suc x) (suc y) (suc d) xnlty = lteTransitiveWeirdInv x y d xnlty

ifComparisonMap : (x y d : Nat) -> ((x <= d) && (y <= d)) ≡ (if x < y then (y <= d) else (x <= d))
ifComparisonMap x y d = ifc x < y
  then (λ {{xlty}} ->
    begin
      (x <= d) && (y <= d)
    =⟨ sym $ lteTransitiveWeird x y d xlty ⟩
      y <= d
    =⟨ sym $ ifTrue (x < y) xlty ⟩
      (if x < y then (y <= d) else (x <= d))
    end
  )
  else (λ {{xnlty}} ->
    begin
      (x <= d) && (y <= d)
    =⟨ sym $ lteTransitiveWeirdInv x y d xnlty ⟩
      x <= d
    =⟨ sym $ ifFalse (x < y) xnlty ⟩
      (if x < y then (y <= d) else (x <= d))
    end
  )

propMaxLte : (x y d : Nat) -> ((x <= d) && (y <= d)) ≡ (max x y <= d)
propMaxLte x y d =
  begin
    (x <= d) && (y <= d)
  =⟨ ifComparisonMap x y d ⟩
    (if x < y then (y <= d) else (x <= d))
  =⟨ propFnIf (λ v -> v <= d) ⟩
    (if x < y then y else x) <= d
  =⟨⟩
    max x y <= d
  end

propAndMap : (a b c d : Bool) -> a ≡ c -> b ≡ d -> (a && b) ≡ (c && d)
propAndMap false false false false ac bd = refl
propAndMap false true false true ac bd = refl
propAndMap true false true false ac bd = refl
propAndMap true true true true ac bd = refl

propMaxLte4 : (w x y z d : Nat) -> (((w <= d) && (x <= d)) && ((y <= d) && (z <= d))) ≡ (max (max w x) (max y z) <= d)
propMaxLte4 w x y z d =
  begin
    ((w <= d) && (x <= d)) && ((y <= d) && (z <= d))
  =⟨ propAndMap ((w <= d) && (x <= d)) ((y <= d) && (z <= d)) (max w x <= d) (max y z <= d) (propMaxLte w x d) (propMaxLte y z d) ⟩
    (max w x <= d) && (max y z <= d)
  =⟨ propMaxLte (if w < x then x else w) (if y < z then z else y) d ⟩
    (max (max w x) (max y z) <= d)
  end

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
open import trie-core
open import string
open import maybe

module trie-functions (trie-lookup : ∀{A : Set} → trie A → string → maybe A)
                      (trie-insert : ∀{A : Set} → trie A → string → A → trie A)
                      (trie-remove : ∀{A : Set} → trie A → string → trie A) where

open import bool
open import char
open import list
open import product
open import unit
open import eq
open import nat

trie-contains : ∀{A : Set} → trie A → string → 𝔹
trie-contains t s with trie-lookup t s
trie-contains t s | nothing = ff
trie-contains t s | just _ = tt

trie-map : ∀{A B : Set} → (A → B) → trie A → trie B
trie-cal-map : ∀{A B : Set} → (A → B) → cal (trie A) → cal (trie B)
trie-map f (Node x x₁) = Node (maybe-map f x) (trie-cal-map f x₁)
trie-cal-map f [] = []
trie-cal-map f ((c , t) :: cs) =
  (c , trie-map f t) :: trie-cal-map f cs

trie-to-string-h : ∀{A : Set} → string → (A → string) → trie A → 𝕃 char → string
trie-cal-to-string-h : ∀{A : Set} → string → (A → string) → cal (trie A) → 𝕃 char → string
trie-to-string-h sep d (Node (just x) c) prev-str =
  (𝕃char-to-string (reverse prev-str)) ^ sep ^ (d x) ^ "\n" ^ (trie-cal-to-string-h sep d c prev-str)
trie-to-string-h sep d (Node nothing c) prev-str = trie-cal-to-string-h sep d c prev-str
trie-cal-to-string-h sep d [] prev-str = ""
trie-cal-to-string-h sep d ((c , t) :: cs) prev-str =
  (trie-to-string-h sep d t (c :: prev-str)) ^ (trie-cal-to-string-h sep d cs prev-str)

{- trie-to-string sep d t returns a string representation of the trie t,
   where each mapping from string s to data x is printed as
     s sep d x
   where sep is a string and d returns a string for any element A of the trie. -}
trie-to-string : ∀{A : Set} → string → (A → string) → trie A → string
trie-to-string sep d t = trie-to-string-h sep d t []

trie-mappings-h : ∀{A : Set} → trie A → 𝕃 char → 𝕃 (string × A)
trie-cal-mappings-h : ∀{A : Set} → cal (trie A) → 𝕃 char → 𝕃 (string × A)
trie-mappings-h (Node (just x) c) prev-str = (𝕃char-to-string (reverse prev-str) , x) :: (trie-cal-mappings-h c prev-str)
trie-mappings-h (Node nothing c) prev-str = (trie-cal-mappings-h c prev-str)
trie-cal-mappings-h [] prev-str = []
trie-cal-mappings-h ((c , t) :: cs) prev-str = trie-mappings-h t (c :: prev-str) ++ (trie-cal-mappings-h cs prev-str)

trie-mappings : ∀{A : Set} → trie A → 𝕃 (string × A)
trie-mappings t = trie-mappings-h t []

-- return a list of all the strings which have associated data in the trie
trie-strings : ∀{A : Set} → trie A → 𝕃 string
trie-strings t = map fst (trie-mappings t)

trie-size : ∀{A : Set} → trie A → ℕ
trie-size t = length (trie-strings t)

trie-nonempty : ∀{A : Set} → trie A → 𝔹
trie-cal-nonempty : ∀{A : Set} → cal (trie A) → 𝔹
trie-nonempty (Node (just x) t) = tt
trie-nonempty (Node nothing c) = trie-cal-nonempty c
trie-cal-nonempty [] = ff
trie-cal-nonempty ((a , t) :: c) = trie-nonempty t || trie-cal-nonempty c

----------------------------------------------------------------------
-- list-tries, which map strings to lists of values
----------------------------------------------------------------------

𝕃trie : Set → Set
𝕃trie A = trie (𝕃 A)

𝕃trie-lookup : ∀{A : Set} → 𝕃trie A → string → 𝕃 A
𝕃trie-lookup t s with trie-lookup t s
... | nothing = []
... | just l = l

𝕃trie-add : ∀{A : Set} → trie (𝕃 A) → string → A → trie (𝕃 A)
𝕃trie-add t s a = trie-insert t s (a :: 𝕃trie-lookup t s)

𝕃trie-add* : ∀{A : Set} → trie (𝕃 A) → string → 𝕃 A → trie (𝕃 A)
𝕃trie-add* t s aa = trie-insert t s (aa ++ 𝕃trie-lookup t s)

----------------------------------------------------------------------
-- stringset
----------------------------------------------------------------------

stringset : Set
stringset = trie ⊤

stringset-contains : stringset → string → 𝔹
stringset-contains ss s = trie-contains ss s

stringset-insert : stringset → string → stringset
stringset-insert ss s = trie-insert ss s triv

stringset-remove : stringset → string → stringset
stringset-remove ss s = trie-remove ss s

stringset-insert𝕃 : stringset → 𝕃 char → stringset
stringset-insert𝕃 ss s = trie-insert-h ss s triv

empty-stringset : stringset
empty-stringset = empty-trie

stringset-insert* : stringset → 𝕃 string → stringset
stringset-insert* s [] = s
stringset-insert* s (x :: xs) = stringset-insert (stringset-insert* s xs) x

stringset-strings : ∀{A : Set} → trie A → 𝕃 string
stringset-strings t = map fst (trie-mappings t)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by decidable total orders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.DecTotalOrder
  {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where

open DecTotalOrder DT hiding (trans)

import Relation.Binary.Construct.Converse as Converse
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- _≥_ - the flipped relation is also a total order

open TotalOrderProperties public
  using
  ( _≥_
  ; ≥-refl
  ; ≥-reflexive
  ; ≥-trans
  ; ≥-antisym
  ; ≥-total
  ; ≥-isPreorder
  ; ≥-isPartialOrder
  ; ≥-isTotalOrder
  ; ≥-preorder
  ; ≥-poset
  ; ≥-totalOrder
  )

≥-isDecTotalOrder : IsDecTotalOrder _≈_ _≥_
≥-isDecTotalOrder = Converse.isDecTotalOrder isDecTotalOrder

≥-decTotalOrder : DecTotalOrder _ _ _
≥-decTotalOrder = record
  { isDecTotalOrder = ≥-isDecTotalOrder
  }

open DecTotalOrder ≥-decTotalOrder public
  using () renaming (_≤?_ to _≥?_)

------------------------------------------------------------------------
-- _<_ - the strict version is a strict total order

open TotalOrderProperties public
  using
  ( _<_
  ; <-resp-≈
  ; <-respʳ-≈
  ; <-respˡ-≈
  ; <-irrefl
  ; <-asym
  ; <-trans
  ; <-isStrictPartialOrder
  ; <-strictPartialOrder
  ; <⇒≉
  ; ≤∧≉⇒<
  ; <⇒≱
  ; ≤⇒≯
  ; ≰⇒>
  )

<-isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder = ToStrict.<-isStrictTotalOrder₂ isDecTotalOrder

<-strictTotalOrder : StrictTotalOrder _ _ _
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

open StrictTotalOrder <-strictTotalOrder public
  using () renaming (compare to <-compare)

≮⇒≥ : ∀ {x y} → ¬ (x < y) → y ≤ x
≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.2

strictTotalOrder = <-strictTotalOrder
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v1.2.
Please use <-strictTotalOrder instead."
#-}


text:
{-# OPTIONS --without-K #-}
module hott.level.sets where

open import hott.level.sets.core public
open import hott.level.sets.extra public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Basics where

id : ∀ {a}{A : Set a} → A → A
id x = x

_∘_ : ∀ {a b c}{A : Set a}{B : Set b}{C : Set c} → (f : B → C) → (g : A → B) → (A → C)
f ∘ g = λ x → f (g x)

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-# OPTIONS --cubical --allow-unsolved-metas #-}

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical
open import Agda.Builtin.Bool

postulate
  Index : Set
  i     : Index

data D : Index →  Set where
  c : D i

cong : {A B : Set} (x y : A) (f : A → B) → x ≡ y → f x ≡ f y
cong _ _ f x≡y = λ i → f (x≡y i)

refl : {A : Set} {x : A} → x ≡ x
refl {x = x} = λ _ → x

subst :
  {A : Set} {x y : A}
  (P : A → Set) → x ≡ y → P x → P y
subst P eq p = primTransp (λ i → P (eq i)) i0 p

postulate
  subst-refl :
    {A : Set} {x : A} (P : A → Set) {p : P x} →
    subst P refl p ≡ p

f : {i : Index} (xs : D i) → D i
f c = c

works : f (subst D refl c) ≡ c
works = cong (subst D refl c) c f (subst-refl D)

-- There is no type error here, just a meta to solve.
-- The original problem was assuming injectivity of f.
should-work-too : f (subst D refl c) ≡ c
should-work-too = cong _ _ f (subst-refl D)

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Reflexivity where

module Reflexivity'
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  (x : 𝔒)
  = ℭLASS (_∼_) (x ∼ x)

module Reflexivity
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  class = ∀ {x} → Reflexivity'.class _∼_ x
  type = ∀ {x} → Reflexivity'.type _∼_ x
  method : ⦃ _ : class ⦄ → type
  method = Reflexivity'.method _∼_ _

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
  where
  reflexivity = Reflexivity.method _∼_
  ε = reflexivity

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  where
  reflexivity[_] = Reflexivity.method _∼_
  ε[_] = reflexivity


text:
-- Andreas, 2019-07-23, issue #3937 reported by gallais

f : let ... = ? in ?
f = ?

-- WAS: internal error

-- Expected: Could not parse the left-hand side ...


text:
{-
 Definition of a basis of a distributive lattice as a generating sub-meet-semilattice
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.DistLattice.Basis where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Powerset

open import Cubical.Functions.Embedding

open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.FinData
open import Cubical.Data.Bool

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.BigOp
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.DistLattice.BigOps

private
  variable
    ℓ : Level

module _ (L' : DistLattice ℓ) where
 private L = fst L'
 open DistLatticeStr (snd L')
 open Join L'

 record IsGenSublattice (M : Semilattice ℓ) (e : fst M → L) : Type ℓ where
  constructor
   isgensublattice
  open SemilatticeStr (snd M) renaming (ε to 0s ; _·_ to _∧s_)
  field
   isInj : ∀ x y → e x ≡ e y → x ≡ y
   pres0 : e 0s ≡ 0l
   resp∧ : ∀ x y → e (x ∧s y) ≡ e x ∧l e y
   ⋁Gen : ∀ (x : L) → ∃[ n ∈ ℕ ] Σ[ α ∈ FinVec (fst M) n ] (⋁ (e ∘ α) ≡ x)

 -- TODO: prove equivalence with the more set-theoretical definition
 record IsBasis (S : ℙ L) : Type ℓ where
  constructor
   isbasis
  field
   contains1 : 1l ∈ S
   ∧lClosed : ∀ (x y : L) → x ∈ S → y ∈ S → x ∧l y ∈ S
   ⋁Basis : ∀ (x : L) → ∃[ n ∈ ℕ ] Σ[ α ∈ FinVec L n ] (∀ i → α i ∈ S) × (⋁ α ≡ x)

 open IsBasis
 open SemilatticeStr
 Basis→MeetSemilattice : (S : ℙ L) → IsBasis S → Semilattice ℓ
 fst (Basis→MeetSemilattice S isBasisS) = Σ[ l ∈ L ] (l ∈ S)
 ε (snd (Basis→MeetSemilattice S isBasisS)) = 1l , isBasisS .contains1
 _·_ (snd (Basis→MeetSemilattice S isBasisS)) x y = fst x ∧l fst y
                                                  , isBasisS .∧lClosed _ _ (snd x) (snd y)
 isSemilattice (snd (Basis→MeetSemilattice S isBasisS)) = makeIsSemilattice
   (isSetΣ (isSetDistLattice L') λ _ → isProp→isSet (S _ .snd))
     (λ _ _ _ → Σ≡Prop (λ _ → S _ .snd) (∧lAssoc _ _ _))
       (λ _ → Σ≡Prop (λ _ → S _ .snd) (∧lRid _))
         (λ _ → Σ≡Prop (λ _ → S _ .snd) (∧lLid _))
           (λ _ _ → Σ≡Prop (λ _ → S _ .snd) (∧lComm _ _))
             λ _ → Σ≡Prop (λ _ → S _ .snd) (∧lIdem _)

max_stars_repo_name: FernandoLarrain/cubical


text:
module WellTypedTermsModel where

open import Library
open import WellTypedTerms
open import RMonads.REM
open import FunctorCat
open import Categories.Sets

-- interpretation of types

Val : Ty → Set
Val ι       = ⊤
Val (σ ⇒ τ) = Val σ → Val τ

-- interpretation of contexts

Env : Con → Set
Env Γ = ∀{σ} →  Var Γ σ → Val σ

_<<_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ)
(γ << v) vz     = v
(γ << v) (vs x) = γ x

-- intepretation of terms

eval : ∀{Γ σ} → Env Γ → Tm Γ σ → Val σ
eval γ (var x)   = γ x
eval γ (app t u) = eval γ t (eval γ u)
eval γ (lam t)   = λ v → eval (γ << v) t

substeval : ∀{σ τ}(p : σ ≅ τ){Γ : Con}{γ : Env Γ}(t : Tm Γ σ) →
      (subst Val p  ∘ eval γ) t ≅ (eval γ ∘ subst (Tm Γ) p) t
substeval refl t = refl

wk<< : ∀{Γ Δ}(α  : Ren Γ Δ)(β : Env Δ){σ}(v : Val σ) →
          ∀{ρ}(y : Var (Γ < σ) ρ) →
          ((β ∘ α) << v) y ≅ (β << v) (wk α y)
wk<< α β v vz     = refl
wk<< α β v (vs y) = refl

reneval : ∀{Γ Δ σ}(α : Ren Γ Δ)(β : Env Δ)(t : Tm Γ σ) →
          eval (β ∘ α) t ≅ (eval β ∘ ren α) t
reneval α β (var x)   = refl
reneval α β (app t u) =
  proof
  eval (β ∘ α) t (eval (β ∘ α) u)
  ≅⟨ cong₂ (λ f x → f x) (reneval α β t) (reneval α β u) ⟩
  eval β (ren α t) (eval β (ren α u))
  ∎
reneval α β (lam t)   = ext λ v →
  proof
  eval ((β ∘ α) << v) t
  ≅⟨ cong (λ (γ : Env _) → eval γ t) (iext λ _ → ext (wk<< α β v)) ⟩
  eval ((β << v) ∘ wk α) t
  ≅⟨ reneval (wk α) (β << v) t ⟩
  eval (β << v) (ren (wk α) t)
  ∎

lifteval : ∀{Γ Δ σ τ}(α : Sub Γ Δ)(β : Env Δ)(v : Val σ)(y : Var (Γ < σ) τ) →
            ((eval β ∘ α) << v) y ≅ (eval (β << v) ∘ lift α) y
lifteval α β v vz     = refl
lifteval α β v (vs x) =
  proof
  eval β (α x)
  ≅⟨ reneval vs (β << v) (α x) ⟩
  eval (β << v) (ren vs (α x))
  ∎

subeval : ∀{Γ Δ σ}(α : Sub Γ Δ)(β : Env Δ)(t : Tm Γ σ) →
          eval (eval β ∘ α) t ≅ (eval β ∘ sub α) t
subeval α β (var x)   = refl
subeval α β (app t u) =
  proof
  eval (eval β ∘ α) t (eval (eval β ∘ α) u)
  ≅⟨ cong₂ (λ f x → f x) (subeval α β t) (subeval α β u) ⟩
  eval β (sub α t) (eval β (sub α u))
  ∎
subeval α β (lam t)   = ext λ v →
  proof
  eval ((eval β ∘ α) << v) t
  ≅⟨ cong (λ (γ : Env _) → eval γ t) (iext λ _ → ext (lifteval α β v)) ⟩
  eval (eval (β << v) ∘ lift α) t
  ≅⟨ subeval (lift α) (β << v) t ⟩
  eval (β << v) (sub (lift α) t)
  ∎

modelRAlg : RAlg TmRMonad
modelRAlg = record {
  acar  = Val;
  astr  = λ {Γ} → λ γ → eval γ;
  alaw1 = refl;
  alaw2 = λ {Γ Δ α γ} → iext λ σ → ext (subeval α γ)}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Class.Traversable where

open import Class.Monad
open import Level

record Traversable {a} (T : Set a -> Set a) : Set (suc a) where
  field
    sequence : ∀ {M : Set a -> Set a} {{_ : Monad M}} {A : Set a} -> T (M A) -> M (T A)

open Traversable {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
open import Coinduction using ( ♯_ )
open import Data.Bool using ( Bool ; true ; false ; not )
open import Data.ByteString using ( null )
open import Data.ByteString.UTF8 using ( fromString ) renaming ( span to #span )
open import Data.Natural using ( Natural )
open import Data.Product using ( _×_ ; _,_ )
open import Data.Char using ( Char )
open import System.IO.Transducers.Lazy using ( _⇒_ ; inp ; out ; done ; _⟫_ ; π₁ ; π₂ ; _[&]_ )
open import System.IO.Transducers.Weight using ( weight )
open import System.IO.Transducers.Stateful using ( loop )
open import System.IO.Transducers.Session using ( ⟨_⟩ ; _&_ ; ¿ ; * ; _&*_ ; Bytes ; Bytes' ; Strings )
open import System.IO.Transducers.Strict using ( _⇛_ )

module System.IO.Transducers.UTF8 where

mutual

  -- TODO: span isn't doing the right thing when char boundaries fail to line up with bytestring boundaries

  span+ : (Char → Bool) → Bytes' ⇛ (Bytes & Bytes)
  span+ φ x with #span φ x
  span+ φ x | (x₁ , x₂) with null x₁ | null x₂
  span+ φ x | (x₁ , x₂) | true  | true  = inp (♯ span φ)
  span+ φ x | (x₁ , x₂) | true  | false = out false (out true (out x₂ done))
  span+ φ x | (x₁ , x₂) | false | true  = out true (out x₁ (inp (♯ span φ)))
  span+ φ x | (x₁ , x₂) | false | false = out true (out x₁ (out false (out true (out x₂ done))))

  span : (Char → Bool) → Bytes ⇛ (Bytes & Bytes)
  span φ false = out false (out false done)
  span φ true  = inp (♯ span+ φ)

break : (Char → Bool) → Bytes ⇛ (Bytes & Bytes)
break φ = span (λ x → not (φ x))

mutual

  nonempty+ : Bytes' & Bytes ⇛ ¿ Bytes & Bytes
  nonempty+ x with null x
  nonempty+ x | true  = inp (♯ nonempty)
  nonempty+ x | false = out true (out true (out x done))

  nonempty : Bytes & Bytes ⇛ ¿ Bytes & Bytes
  nonempty true  = inp (♯ nonempty+)
  nonempty false = out false done

split? : (Char → Bool) → Bytes ⇒ (¿ Bytes & Bytes)
split? φ = inp (♯ span φ) ⟫ π₂ {Bytes} ⟫ inp (♯ break φ) ⟫ inp (♯ nonempty)

split : (Char → Bool) → Bytes ⇒ * Bytes
split φ = loop {Bytes} (split? φ) ⟫ π₁

-- TODO: decode

encode : Strings ⇛ Bytes
encode true  = out true (inp (♯ λ s → out (fromString s) (inp (♯ encode))))
encode false = out false done

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io