text:
------------------------------------------------------------------------
-- M-types for indexed containers, defined coinductively (in Cubical
-- Agda)
------------------------------------------------------------------------

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

import Equality.Path as P

module Container.Indexed.M.Codata
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

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

open import Bijection equality-with-J using (_↔_)
open import Container.Indexed equality-with-J
import Container.Indexed.M.Function equality-with-J as F
import Container.Indexed.Variant equality-with-J as V
open import Container.Indexed.Variant.M.Codata eq as VM using (out-M)
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import Univalence-axiom equality-with-J

private
  variable
    a iℓ s p : Level
    A I      : Type a
    i x      : A
    C        : Container I s p
    n        : ℕ

------------------------------------------------------------------------
-- The M-type and some basic results

-- An M-type for a given container.
--
-- This definition is similar to one in "Indexed containers" by
-- Altenkirch, Ghani, Hancock, McBride and Morris.

record M {I : Type iℓ} (C : Container I s p) (i : I) :
         Type (iℓ ⊔ s ⊔ p) where
  coinductive
  constructor in-M
  field
    out-M : ⟦ C ⟧ (M C) i

open M public

-- An η-law.

η : in-M (out-M x) ≡ x
η = _↔_.from ≡↔≡ η′
  where
  η′ : in-M (out-M x) P.≡ x
  η′ {x = x} _ .out-M = x .out-M

-- M C is, in a certain sense, a fixpoint of ⟦ C ⟧.

M-fixpoint : ⟦ C ⟧ (M C) i ≃ M C i
M-fixpoint = Eq.↔→≃ in-M out-M (λ _ → η) refl

-- A coalgebra defined using M and out-M.

M-coalgebra : (C : Container I s p) → Coalgebra C
M-coalgebra C = M C , λ _ → out-M

------------------------------------------------------------------------
-- Some conversion lemmas

-- One can convert between M and VM.M.

M≃M :
  ∀ p {I : Type i} {C : V.Container I s (i ⊔ p)} {i} →
  M (_⇔_.to (V.Container⇔Container p) C) i ≃ VM.M C i
M≃M p {C = C} =
  Eq.↔→≃ to from
    (λ c → _↔_.from ≡↔≡ (to-from c))
    (λ c → _↔_.from ≡↔≡ (from-to c))
  where
  to : M (_⇔_.to (V.Container⇔Container p) C) i → VM.M C i
  to x .out-M .proj₁     = x .out-M .proj₁
  to x .out-M .proj₂ i p = to (x .out-M .proj₂ (i , p))

  from : VM.M C i → M (_⇔_.to (V.Container⇔Container p) C) i
  from x .out-M .proj₁         = x .out-M .proj₁
  from x .out-M .proj₂ (i , p) = from (x .out-M .proj₂ i p)

  to-from : (x : VM.M C i) → to (from x) P.≡ x
  to-from x i .out-M .proj₁     = x .out-M .proj₁
  to-from x i .out-M .proj₂ j p = to-from (x .out-M .proj₂ j p) i

  from-to :
    (x : M (_⇔_.to (V.Container⇔Container p) C) i) →
    from (to x) P.≡ x
  from-to x i .out-M .proj₁   = x .out-M .proj₁
  from-to x i .out-M .proj₂ p = from-to (x .out-M .proj₂ p) i

-- M-coalgebra is related to VM.M-coalgebra (assuming univalence).

M-coalgebra≡M-coalgebra :
  ∀ p {I : Type i} (C : V.Container I s (i ⊔ p)) →
  Univalence (i ⊔ s ⊔ p) →
  M-coalgebra (_⇔_.to (V.Container⇔Container p) C) ≡
  _≃_.to (V.Coalgebra≃Coalgebra p C ext) (VM.M-coalgebra C)
M-coalgebra≡M-coalgebra p C univ =
  Σ-≡,≡→≡
    (⟨ext⟩ lemma₁)
    (⟨ext⟩ λ i → ⟨ext⟩ λ x →

     subst (λ P → P ⇾ ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P)
       (⟨ext⟩ lemma₁) (λ _ → out-M) i x                                ≡⟨ cong (_$ x) $ sym $
                                                                          push-subst-application _ _ ⟩
     subst (λ P → P i → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁) out-M x                                          ≡⟨ subst-→ ⟩

     subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁)
       (subst (_$ i) (sym (⟨ext⟩ lemma₁)) x .out-M)                    ≡⟨ cong (subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i) _) $
                                                                          cong out-M $
                                                                          cong (flip (subst (_$ i)) _) $ sym $
                                                                          ext-sym lemma₁ ⟩
     subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁)
       (subst (_$ i) (⟨ext⟩ (sym ∘ lemma₁)) x .out-M)                  ≡⟨ cong (subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i) _) $
                                                                          cong out-M $
                                                                          subst-ext id (sym ∘ lemma₁) ⟩
     subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁)
       (subst id (sym (lemma₁ i)) x .out-M)                            ≡⟨ cong (subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i) _) $
                                                                          cong out-M $
                                                                          subst-id-in-terms-of-inverse∘≡⇒↝ equivalence {A≡B = lemma₁ i} ⟩
     subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁)
       (_≃_.from (≡⇒≃ (lemma₁ i)) x .out-M)                            ≡⟨ cong (subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i) _) $
                                                                          cong (λ (eq : M (_⇔_.to (V.Container⇔Container p) C) i ≃ VM.M C i) →
                                                                                _≃_.from eq x .out-M) $
                                                                          _≃_.right-inverse-of (≡≃≃ univ) _ ⟩
     subst (λ P → ⟦ _⇔_.to (V.Container⇔Container p) C ⟧ P i)
       (⟨ext⟩ lemma₁)
       (_≃_.from (M≃M p {i = i}) x .out-M)                             ≡⟨⟩

     subst (λ P → ∃ λ (s : V.Shape C i) →
                    ((i , _) : ∃ (V.Position C s)) → P i)
       (⟨ext⟩ lemma₁)
       (_≃_.from (M≃M p {i = i}) x .out-M)                             ≡⟨ push-subst-pair-× _ _ ⟩

     ( x .out-M .proj₁
     , subst (λ P → ((i , _) : ∃ (V.Position C (x .out-M .proj₁))) →
                    P i)
       (⟨ext⟩ lemma₁)
       (_≃_.from (M≃M p {i = i}) x .out-M .proj₂)
     )                                                                 ≡⟨ cong (x .out-M .proj₁ ,_) $
                                                                          ⟨ext⟩ (lemma₃ i x) ⟩∎
     Σ-map id uncurry (x .out-M)                                       ∎)
  where
  lemma₁ = λ _ → ≃⇒≡ univ (M≃M p)

  lemma₂ : ∀ _ _ _ → _
  lemma₂ _ _ p =
    sym (Σ-≡,≡→≡ (sym (⟨ext⟩ lemma₁)) (refl p′))                ≡⟨ cong sym $ cong (Σ-≡,≡→≡ (sym (⟨ext⟩ lemma₁))) $ sym $
                                                                   trans-symʳ _ ⟩
    sym (Σ-≡,≡→≡ (sym (⟨ext⟩ lemma₁))
           (trans (subst-const _) (sym (subst-const _))))       ≡⟨ cong sym $ Σ-≡,≡→≡-subst-const _ _ ⟩

    sym (cong₂ _,_ (sym (⟨ext⟩ lemma₁)) (sym (subst-const _)))  ≡⟨ cong sym cong₂-sym ⟩

    sym (sym (cong₂ _,_ (⟨ext⟩ lemma₁) (subst-const _)))        ≡⟨ sym-sym _ ⟩∎

    cong₂ _,_ (⟨ext⟩ lemma₁) (subst-const _)                    ∎
    where
    p′ = subst (const _) (sym (⟨ext⟩ lemma₁)) p

  lemma₃ : ∀ _ _ _ → _
  lemma₃ i x (i′ , p′) =
    subst (λ P → ((i , _) : ∃ _) → P i)
    (⟨ext⟩ lemma₁)
    (_≃_.from (M≃M p {i = i}) x .out-M .proj₂)
    (i′ , p′)                                               ≡⟨ subst-∀ ⟩

    subst (λ ((P , i , _) : _ × ∃ _) → P i)
      (sym $ Σ-≡,≡→≡ (sym (⟨ext⟩ lemma₁)) (refl _))
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ $
       subst (const _) (sym (⟨ext⟩ lemma₁)) (i′ , p′))      ≡⟨ cong (flip (subst (λ ((P , i , _) : _ × ∃ _) → P i)) _) $
                                                               lemma₂ i x _ ⟩
    subst (λ ((P , i , _) : _ × ∃ _) → P i)
      (cong₂ _,_ (⟨ext⟩ lemma₁) (subst-const _))
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ $
       subst (const _) (sym (⟨ext⟩ lemma₁)) (i′ , p′))      ≡⟨ elim₁
                                                                 (λ {q} eq →
                                                                    subst (λ ((P , i , _) : _ × ∃ _) → P i)
                                                                      (cong₂ _,_ (⟨ext⟩ lemma₁) eq)
                                                                      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ q) ≡
                                                                    subst (λ ((P , i , _) : _ × ∃ (V.Position C (x .out-M .proj₁))) → P i)
                                                                      (cong₂ {u = i′ , p′} _,_ (⟨ext⟩ lemma₁) (refl _))
                                                                      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ (i′ , p′)))
                                                                 (refl _)
                                                                 _ ⟩
    subst (λ ((P , i , _) : _ × ∃ _) → P i)
      (cong₂ _,_ (⟨ext⟩ lemma₁) (refl _))
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ (i′ , p′))  ≡⟨ cong (flip (subst (λ ((P , i , _) : _ × ∃ _) → P i)) _) $
                                                               cong₂-reflʳ _ ⟩
    subst (λ ((P , i , _) : _ × ∃ _) → P i)
      (cong (_, i′ , p′) (⟨ext⟩ lemma₁))
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ (i′ , p′))  ≡⟨ sym $ subst-∘ _ _ _ ⟩

    subst (_$ i′) (⟨ext⟩ lemma₁)
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ (i′ , p′))  ≡⟨ subst-ext _ _ ⟩

    subst id (lemma₁ i′)
      (_≃_.from (M≃M p {i = i}) x .out-M .proj₂ (i′ , p′))  ≡⟨⟩

    subst id (≃⇒≡ univ (M≃M p {i = i′}))
      (_≃_.from (M≃M p {i = i′}) (x .out-M .proj₂ i′ p′))   ≡⟨ subst-id-in-terms-of-≡⇒↝ equivalence ⟩

    _≃_.to (≡⇒≃ (≃⇒≡ univ (M≃M p {i = i′})))
      (_≃_.from (M≃M p {i = i′}) (x .out-M .proj₂ i′ p′))   ≡⟨ cong (λ eq → _≃_.to eq (_≃_.from (M≃M p {i = i′}) (x .out-M .proj₂ i′ p′))) $
                                                               _≃_.right-inverse-of (≡≃≃ univ) _ ⟩
    _≃_.to (M≃M p {i = i′})
      (_≃_.from (M≃M p {i = i′}) (x .out-M .proj₂ i′ p′))   ≡⟨ _≃_.right-inverse-of (M≃M p {i = i′}) _ ⟩

    x .out-M .proj₂ i′ p′                                   ≡⟨⟩

    Σ-map id uncurry (x .out-M) .proj₂ (i′ , p′)            ∎

------------------------------------------------------------------------
-- Lemmas related to lift-positions

-- Lifting the position type family using lift-positions does not
-- affect the resulting M type (up to pointwise equivalence).

M≃M-lift-positions : M C i ≃ M (lift-positions C) i
M≃M-lift-positions =
  Eq.↔→≃ to from
    (λ c → _↔_.from ≡↔≡ (to-from c))
    (λ c → _↔_.from ≡↔≡ (from-to c))
  where
  to : M C i → M (lift-positions C) i
  to x .out-M .proj₁          = x .out-M .proj₁
  to x .out-M .proj₂ (lift p) = to (x .out-M .proj₂ p)

  from : M (lift-positions C) i → M C i
  from x .out-M .proj₁   = x .out-M .proj₁
  from x .out-M .proj₂ p = from (x .out-M .proj₂ (lift p))

  to-from : (x : M (lift-positions C) i) → to (from x) P.≡ x
  to-from x i .out-M .proj₁   = x .out-M .proj₁
  to-from x i .out-M .proj₂ p = to-from (x .out-M .proj₂ p) i

  from-to : (x : M C i) → from (to x) P.≡ x
  from-to x i .out-M .proj₁   = x .out-M .proj₁
  from-to x i .out-M .proj₂ p = from-to (x .out-M .proj₂ p) i

-- M-coalgebra C is related to M-coalgebra (lift-positions C)
-- (assuming univalence).

≡M-coalgebra-lift-positions :
  {I : Type i} {C : Container I s p} →
  Univalence (i ⊔ s ⊔ p) →
  Coalgebra≃Coalgebra-lift-positions _ (M-coalgebra C) ≡
  M-coalgebra (lift-positions C)
≡M-coalgebra-lift-positions {C = C} univ =
  Σ-≡,≡→≡
    (⟨ext⟩ lemma)
    (⟨ext⟩ λ i → ⟨ext⟩ λ x →

     subst (λ P → P ⇾ ⟦ lift-positions C ⟧ P)
       (⟨ext⟩ lemma)
       ((Σ-map id (_∘ lower) ∘_) ∘ (λ _ → out-M))
       i x                                                             ≡⟨ cong (_$ x) $ sym $
                                                                          push-subst-application _ _ ⟩
     subst (λ P → P i → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma) (Σ-map id (_∘ lower) ∘ out-M) x                   ≡⟨ subst-→ ⟩

     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       (Σ-map id (_∘ lower) $
        subst (_$ i) (sym (⟨ext⟩ lemma)) x .out-M)                     ≡⟨ cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $
                                                                          cong (Σ-map id (_∘ lower)) $ cong out-M $
                                                                          cong (flip (subst (_$ i)) _) $ sym $
                                                                          ext-sym lemma ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       (Σ-map id (_∘ lower) $
        subst (_$ i) (⟨ext⟩ (sym ∘ lemma)) x .out-M)                   ≡⟨ cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $
                                                                          cong (Σ-map id (_∘ lower)) $ cong out-M $
                                                                          subst-ext id (sym ∘ lemma) ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       (Σ-map id (_∘ lower) $
        subst id (sym (lemma i)) x .out-M)                             ≡⟨ cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $
                                                                          cong (Σ-map id (_∘ lower)) $ cong out-M $
                                                                          subst-id-in-terms-of-inverse∘≡⇒↝ equivalence {A≡B = lemma i} ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       (Σ-map id (_∘ lower) $
        _≃_.from (≡⇒≃ (lemma i)) x .out-M)                             ≡⟨ cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $
                                                                          cong (λ (eq : M C i ≃ M (lift-positions C) i) →
                                                                                Σ-map id (_∘ lower) (_≃_.from eq x .out-M)) $
                                                                          _≃_.right-inverse-of (≡≃≃ univ) _ ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       (Σ-map id (_∘ lower) $
        _≃_.from M≃M-lift-positions x .out-M)                          ≡⟨⟩

     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       ( x .out-M .proj₁
       , _≃_.from M≃M-lift-positions ∘ x .out-M .proj₂
       )                                                               ≡⟨ (cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $ cong (_ ,_) $
                                                                           ⟨ext⟩ λ p →
                                                                           cong (λ eq → _≃_.from eq (x .out-M .proj₂ p)) $ sym $
                                                                           _≃_.right-inverse-of (≡≃≃ univ) _) ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       ( x .out-M .proj₁
       , _≃_.from (≡⇒≃ (lemma _)) ∘ x .out-M .proj₂
       )                                                               ≡⟨ (cong (subst (λ P → ⟦ lift-positions C ⟧ P i) _) $ cong (_ ,_) $
                                                                           ⟨ext⟩ λ p →
                                                                           cong (λ (f : ∀ i → M C i ≡ M (lift-positions C) i) →
                                                                                _≃_.from (≡⇒≃ (f _)) (x .out-M .proj₂ p)) $ sym $
                                                                           _≃_.left-inverse-of (Eq.extensionality-isomorphism bad-ext) _) ⟩
     subst (λ P → ⟦ lift-positions C ⟧ P i)
       (⟨ext⟩ lemma)
       ( x .out-M .proj₁
       , _≃_.from (≡⇒≃ (ext⁻¹ (⟨ext⟩ lemma) _)) ∘ x .out-M .proj₂
       )                                                               ≡⟨ elim₁
                                                                            (λ eq →
                                                                               subst (λ P → ⟦ lift-positions C ⟧ P i)
                                                                                eq
                                                                                ( x .out-M .proj₁
                                                                                , _≃_.from (≡⇒≃ (ext⁻¹ eq _)) ∘ x .out-M .proj₂
                                                                                ) ≡
                                                                               x .out-M)
                                                                            (
         subst (λ P → ⟦ lift-positions C ⟧ P i)
           (refl _)
           ( x .out-M .proj₁
           , _≃_.from (≡⇒≃ (ext⁻¹ (refl (M (lift-positions C))) _)) ∘
             x .out-M .proj₂
           )                                                                 ≡⟨ subst-refl _ _ ⟩

           x .out-M .proj₁
         , _≃_.from (≡⇒≃ (ext⁻¹ (refl (M (lift-positions C))) _)) ∘
           x .out-M .proj₂                                                   ≡⟨ (cong (_ ,_) $ ⟨ext⟩ λ p →
                                                                                cong (λ eq → _≃_.from eq (x .out-M .proj₂ p)) $
                                                                                trans (cong ≡⇒≃ $ ext⁻¹-refl (M (lift-positions C))) $
                                                                                ≡⇒↝-refl) ⟩∎
         x .out-M                                                            ∎)
                                                                            (⟨ext⟩ lemma) ⟩∎
     x .out-M                                                          ∎)
  where
  lemma = λ _ → ≃⇒≡ univ M≃M-lift-positions

------------------------------------------------------------------------
-- Finality

private

  -- M-coalgebra C is sometimes a final coalgebra (assuming
  -- univalence). Note that the last index argument of C is not
  -- unrestricted.

  M-final′ :
    ∀ p {I : Type i} {C : Container I s (i ⊔ p)} →
    Univalence (i ⊔ s ⊔ p) →
    Univalence (i ⊔ p) →
    Final′ (M-coalgebra C)
  M-final′ p {C = C} univ₁ univ₂ =                                    $⟨ VM.M-final′ C′ ⟩
    V.Final′ (VM.M-coalgebra C′)                                      ↝⟨ subst V.Final′ $ sym $ _≃_.to-from C≃C $ sym $
                                                                         M-coalgebra≡M-coalgebra p C′ univ₁ ⟩
    V.Final′ (_≃_.from C≃C (M-coalgebra (_⇔_.to C⇔C C′)))             ↔⟨ V.Final′≃Final′ p C′ ext ext
                                                                           (_≃_.from C≃C (M-coalgebra (_⇔_.to C⇔C C′))) ⟩
    Final′ (_≃_.to C≃C $ _≃_.from C≃C $ M-coalgebra (_⇔_.to C⇔C C′))  ↝⟨ subst Final′ (_≃_.right-inverse-of C≃C (M-coalgebra (_⇔_.to C⇔C C′))) ⟩
    Final′ (M-coalgebra (_⇔_.to C⇔C C′))                              ↝⟨ subst (Final′ ∘ M-coalgebra) $
                                                                         _≃_.right-inverse-of (V.Container≃Container p ext univ₂) _ ⟩□
    Final′ (M-coalgebra C)                                            □
    where
    C⇔C = V.Container⇔Container p
    C′  = _⇔_.from C⇔C C
    C≃C = V.Coalgebra≃Coalgebra p C′ ext

  -- M-coalgebra C is sometimes a final coalgebra (assuming univalence).
  -- Note that the last index argument of C is not unrestricted.

  M-final″ :
    ∀ p {I : Type i} {C : Container I s (i ⊔ p)} →
    Univalence (i ⊔ s ⊔ p) →
    Univalence (i ⊔ p) →
    Final (M-coalgebra C)
  M-final″ p {C = C} univ₁ univ₂ =
    block λ b →
    Final′→Final
      ext
      ( F.M-coalgebra b ext C
      , F.M-final b ext ext
      )
      ( M-coalgebra C
      , M-final′ p univ₁ univ₂
      )

-- M-coalgebra C is a final coalgebra (assuming univalence).
--
-- TODO: Can this be proved directly, without using VM.M-final′ or
-- univalence?

M-final :
  {I : Type i} {C : Container I s p} →
  Univalence (i ⊔ s ⊔ p) →
  Univalence (i ⊔ p) →
  Final (M-coalgebra C)
M-final {p = p} {C = C} univ₁ univ₂ =                        $⟨ M-final″ p univ₁ univ₂ ⟩
  Final (M-coalgebra (lift-positions C))                     ↔⟨⟩

  (∀ Y → Contractible (Y ⇨ M-coalgebra (lift-positions C)))  ↝⟨ (Π-cong-contra-→ (Coalgebra≃Coalgebra-lift-positions _) λ Y →
                                                                 H-level-cong _ 0 (
      Coalgebra≃Coalgebra-lift-positions _ Y ⇨
      M-coalgebra (lift-positions C)                               ↝⟨ ≡⇒↝ _ $ cong (Coalgebra≃Coalgebra-lift-positions _ Y ⇨_) $ sym $
                                                                      ≡M-coalgebra-lift-positions univ₁ ⟩
      Coalgebra≃Coalgebra-lift-positions _ Y ⇨
      Coalgebra≃Coalgebra-lift-positions _ (M-coalgebra C)         ↝⟨ inverse $ ⇨≃⇨-lift-positions ext _ (M-coalgebra C) ⟩□

      Y ⇨ M-coalgebra C                                            □)) ⟩

  (∀ Y → Contractible (Y ⇨ M-coalgebra C))                   ↔⟨⟩

  Final (M-coalgebra C)                                      □

------------------------------------------------------------------------
-- H-levels

-- If the shape types of C have h-level n, then M C i has h-level n
-- (assuming univalence).

H-level-M :
  {I : Type i} {C : Container I s p} →
  Univalence (i ⊔ s ⊔ p) →
  Univalence (i ⊔ p) →
  (∀ i → H-level n (Shape C i)) →
  ∀ {i} → H-level n (M C i)
H-level-M {C = C} univ₁ univ₂ h =
  F.H-level-final-coalgebra
    ext
    (M-coalgebra C , M-final univ₁ univ₂)
    h

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Data.Strict.Primitive where

data Strict (A : Set) : Set where
  ! : A → Strict A

{-# IMPORT Data.Strict.AgdaFFI #-}
{-# COMPILED_DATA Strict Data.Strict.AgdaFFI.Strict Data.Strict.AgdaFFI.Strict #-}

ext: agda

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


text:
------------------------------------------------------------------------------
-- Definition of FOTC streams using the Agda co-inductive combinators
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Stream.TypeSL where

open import Codata.Musical.Notation
open import Data.Product renaming ( _×_ to _∧_ )
open import Relation.Binary.PropositionalEquality

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

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/List.agda).
infixr 8 _∷_

data D : Set where
  _∷_ : D → D → D

data Stream : D → Set where
  consS : ∀ x {xs} → ∞ (Stream xs) → Stream (x ∷ xs)

Stream-out : ∀ {xs} → Stream xs →
             ∃ λ x' → ∃ λ xs' → Stream xs' ∧ xs ≡ x' ∷ xs'
Stream-out (consS x' {xs'} Sxs') = x' , xs' , ♭ Sxs' , refl

{-# NON_TERMINATING #-}
Stream-coind :
  (A : D → Set) →
  (∀ {xs} → A xs → ∃ λ x' → ∃ λ xs' → xs ≡ x' ∷ xs' ∧ A xs') →
  ∀ {xs} → A xs → Stream xs
Stream-coind A h Axs with h Axs
... | x' , xs' , prf₁ , Axs' = subst Stream (sym prf₁) prf₂
  where
  prf₂ : Stream (x' ∷ xs')
  prf₂ = consS x' (♯ Stream-coind A h Axs')

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text: module Numeral.Rational.SternBrocot where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module FFI.Data.Aeson where

open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.String using (String)

open import FFI.Data.ByteString using (ByteString)
open import FFI.Data.HaskellString using (HaskellString; pack)
open import FFI.Data.Maybe using (Maybe)
open import FFI.Data.Either using (Either; mapLeft)
open import FFI.Data.Scientific using (Scientific)
open import FFI.Data.Vector using (Vector)

{-# FOREIGN GHC import qualified Data.Aeson #-}
{-# FOREIGN GHC import qualified Data.Aeson.Key #-}
{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}

postulate
  KeyMap : Set → Set
  Key : Set
  fromString : String → Key
  toString : Key → String
  lookup : ∀ {A} → Key -> KeyMap A -> Maybe A
{-# POLARITY KeyMap ++ #-}
{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}

data Value : Set where
  object : KeyMap Value → Value
  array : Vector Value → Value
  string : String → Value
  number : Scientific → Value
  bool : Bool → Value
  null : Value
{-# COMPILE GHC Value = data Data.Aeson.Value (Data.Aeson.Object|Data.Aeson.Array|Data.Aeson.String|Data.Aeson.Number|Data.Aeson.Bool|Data.Aeson.Null) #-}

Object = KeyMap Value
Array = Vector Value

postulate
  decode : ByteString → Maybe Value
  eitherHDecode : ByteString → Either HaskellString Value
{-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
{-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}

eitherDecode : ByteString → Either String Value
eitherDecode bytes = mapLeft pack (eitherHDecode bytes)

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
------------------------------------------------------------------------
-- Various utility functions
------------------------------------------------------------------------

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

module Utilities where

open import Data.Bool
open import Data.Bool.Properties using (T-∧)
open import Data.Char
import Data.Char.Properties as Char
open import Data.List
open import Data.List.NonEmpty as List⁺
open import Data.Nat
import Data.Nat.Properties as NP
open import Data.Product
open import Data.String as String using (String)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence
  using () renaming (module Equivalence to Eq)
open import Relation.Binary
import Relation.Binary.Properties.StrictTotalOrder as STO
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Some comparison operators

-- Is one number strictly smaller than another?

_<?ℕ_ : ℕ → ℕ → Bool
n₁ <?ℕ n₂ = ⌊ n₁ NP.<? n₂ ⌋

-- Is one character smaller than or equal to another?

_≤?C_ : Char → Char → Bool
c₁ ≤?C c₂ = ⌊ DecTotalOrder._≤?_
                (STO.decTotalOrder Char.<-strictTotalOrder)
                c₁ c₂ ⌋

------------------------------------------------------------------------
-- Conversion of strings satisfying given predicates to annotated
-- lists

private
  mutual

    str′ : {p : Char → Bool}
           (s : List Char) → T (all p s) → List (∃ (T ∘ p))
    str′ []       _  = []
    str′ (t ∷ ts) ok = List⁺.toList (str⁺′ (t ∷ ts) ok)

    str⁺′ : {p : Char → Bool}
            (s : List⁺ Char) → T (all p (List⁺.toList s)) →
            List⁺ (∃ (T ∘ p))
    str⁺′ (t ∷ ts) ok =
      let (ok₁ , ok₂) = Eq.to T-∧ ⟨$⟩ ok in
      (t , ok₁) ∷ str′ ts ok₂

str : {p : Char → Bool}
      (s : String)
      {ok : T (all p $ String.toList s)} →
      List (∃ (T ∘ p))
str s {ok} = str′ (String.toList s) ok

str⁺ : {p : Char → Bool}
       (s : String)
       {ok₁ : T (all p $ String.toList s)}
       {ok₂ : T (not $ null $ String.toList s)} →
       List⁺ (∃ (T ∘ p))
str⁺ s {ok₂ = _} with String.toList s
str⁺ s {ok₂ = ()} | []
str⁺ s {ok₁ = ok} | c ∷ cs = str⁺′ (c ∷ cs) ok

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
------------------------------------------------------------------------
-- Booleans
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module Examples.Bool where

open import Codata.Musical.Notation
open import Data.Bool
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Grammar.Infinite using (Grammar)
import Pretty
open import Renderer

module _ where

  open Grammar.Infinite

  bool : Grammar Bool
  bool = true  <$ string′ "true"
       ∣ false <$ string′ "false"

open Pretty

bool-printer : Pretty-printer bool
bool-printer true  = left  (<$ text)
bool-printer false = right (<$ text)

test₁ : render 4 (bool-printer true) ≡ "true"
test₁ = refl

test₂ : render 0 (bool-printer false) ≡ "false"
test₂ = refl


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

module Cubical.Categories.Additive.Instances.Terminal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Categories.Category
open import Cubical.Categories.Additive.Base
open import Cubical.Categories.Instances.Discrete

open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.AbGroup.Instances.Unit

open import Cubical.Data.Unit

private
  variable
    ℓ ℓ' : Level

open PreaddCategory
open PreaddCategoryStr
open AdditiveCategory
open AdditiveCategoryStr

private
  terminalCategory : Category ℓ ℓ
  terminalCategory = DiscreteCategory (Unit* , isOfHLevelUnit* 3)

  terminalAbGroupStr : AbGroupStr {ℓ = ℓ} Unit*
  terminalAbGroupStr = snd UnitAbGroup

  homProp : (x y : Category.ob {ℓ = ℓ} terminalCategory) → isProp (terminalCategory [ x , y ])
  homProp x y = isOfHLevelUnit* 2 x y

  homContr : (x y : Category.ob {ℓ = ℓ} terminalCategory) → isContr (terminalCategory [ x , y ])
  homContr x y = isProp→isContrPath (isOfHLevelUnit* 1) x y

  terminalPreAdd : PreaddCategory ℓ ℓ
  cat terminalPreAdd = terminalCategory
  homAbStr (preadd terminalPreAdd) =
    λ x y →
      subst
        AbGroupStr
        (sym (isContr→≡Unit* (homContr x y)))
        terminalAbGroupStr
  ⋆distl+ (preadd terminalPreAdd) = λ _ _ _ _ → refl
  ⋆distr+ (preadd terminalPreAdd) = λ _ _ _ → refl

terminalAdditiveCategory : AdditiveCategory ℓ ℓ
preaddcat terminalAdditiveCategory = terminalPreAdd
ZeroObject.z (zero (addit terminalAdditiveCategory)) = tt*
ZeroObject.zInit (zero (addit terminalAdditiveCategory)) y = homContr _ _
ZeroObject.zTerm (zero (addit terminalAdditiveCategory)) y = homContr _ _
biprod (addit terminalAdditiveCategory) x y = trivProd
  where trivProd : Biproduct terminalPreAdd x y
        Biproduct.x⊕y trivProd = tt*
        Biproduct.i₁ trivProd = refl
        Biproduct.i₂ trivProd = refl
        Biproduct.π₁ trivProd = refl
        Biproduct.π₂ trivProd = refl
        IsBiproduct.i₁⋆π₁ (Biproduct.isBipr trivProd) = homProp _ _ _ _
        IsBiproduct.i₁⋆π₂ (Biproduct.isBipr trivProd) = homProp _ _ _ _
        IsBiproduct.i₂⋆π₁ (Biproduct.isBipr trivProd) = homProp _ _ _ _
        IsBiproduct.i₂⋆π₂ (Biproduct.isBipr trivProd) = homProp _ _ _ _
        IsBiproduct.∑π⋆i (Biproduct.isBipr trivProd) = homProp _ _ _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- A view of the syntax
------------------------------------------------------------------------

module RecursiveTypes.Syntax.UnfoldedOrFixpoint where

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution

-- Unfolded types, i.e. types where the outermost construction is
-- not a fixpoint.

infixr 10 _⟶_

data Unfolded {n} : Ty n → Set where
  ⊥   : Unfolded ⊥
  ⊤   : Unfolded ⊤
  var : ∀ x → Unfolded (var x)
  _⟶_ : (τ₁ τ₂ : Ty n) → Unfolded (τ₁ ⟶ τ₂)

-- A view of types as either unfolded (U) or fixpoints (Μ).

data U∨Μ {n} : Ty n → Set where
  unfolded : ∀ {σ} (u : Unfolded σ) → U∨Μ σ
  fixpoint : ∀ {τ₁ τ₂} (u : U∨Μ unfold[μ τ₁ ⟶ τ₂ ]) → U∨Μ (μ τ₁ ⟶ τ₂)

u∨μ : ∀ {n} (σ : Ty n) → U∨Μ σ
u∨μ ⊥           = unfolded ⊥
u∨μ ⊤           = unfolded ⊤
u∨μ (var x)     = unfolded (var x)
u∨μ (τ₁ ⟶ τ₂)   = unfolded (τ₁ ⟶ τ₂)
u∨μ (μ τ₁ ⟶ τ₂) =
  fixpoint (unfolded ((τ₁ [0≔ μ τ₁ ⟶ τ₂ ]) ⟶ (τ₂ [0≔ μ τ₁ ⟶ τ₂ ])))

u∨μ⁻¹ : ∀ {n} {σ : Ty n} → U∨Μ σ → Ty n
u∨μ⁻¹ {σ = σ} _ = σ

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- We define ZigZag-complete relations and prove that quasi equivalence relations
-- give rise to equivalences on the set quotients.
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.ZigZag.Base where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.Relation.Binary.Base

open BinaryRelation
open isEquivRel

private
 variable
  ℓ ℓ' : Level

isZigZagComplete : {A B : Type ℓ} (R : A → B → Type ℓ') → Type (ℓ-max ℓ ℓ')
isZigZagComplete R = ∀ {a b a' b'} → R a b → R a' b → R a' b' → R a b'

ZigZagRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
ZigZagRel A B ℓ' = Σ[ R ∈ (A → B → Type ℓ') ] (isZigZagComplete R)

record isQuasiEquivRel {A B : Type ℓ} (R : A → B → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  field
    zigzag : isZigZagComplete R
    fwd : A → B
    fwdRel : (a : A) → R a (fwd a)
    bwd : B → A
    bwdRel : (b : B) → R (bwd b) b

open isQuasiEquivRel

QuasiEquivRel : (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
QuasiEquivRel A B ℓ' =
  Σ[ R ∈ PropRel A B ℓ' ] isQuasiEquivRel (R .fst)

invQER : {A B : Type ℓ} {ℓ' : Level} → QuasiEquivRel A B ℓ' → QuasiEquivRel B A ℓ'
invQER (R , qer) .fst = invPropRel R
invQER (R , qer) .snd .zigzag aRb aRb' a'Rb' = qer .zigzag a'Rb' aRb' aRb
invQER (R , qer) .snd .fwd = qer .bwd
invQER (R , qer) .snd .fwdRel = qer .bwdRel
invQER (R , qer) .snd .bwd = qer .fwd
invQER (R , qer) .snd .bwdRel = qer .fwdRel

QER→EquivRel : {A B : Type ℓ}
  → QuasiEquivRel A B ℓ' → EquivPropRel A ℓ'
QER→EquivRel (R , sim) .fst .fst a₀ a₁ = R .fst a₀ (sim .fwd a₁)
QER→EquivRel (R , sim) .fst .snd _ _ = R .snd _ _
QER→EquivRel (R , sim) .snd .reflexive a = sim .fwdRel a
QER→EquivRel (R , sim) .snd .symmetric a₀ a₁ r =
  sim .zigzag (sim .fwdRel a₁) r (sim .fwdRel a₀)
QER→EquivRel (R , sim) .snd .transitive a₀ a₁ a₂ r s =
  sim .zigzag r (sim .fwdRel a₁) s

-- The following result is due to Carlo Angiuli
module QER→Equiv {A B : Type ℓ} (R : QuasiEquivRel A B ℓ') where

  private
    sim = R .snd
    f = sim .fwd
    g = sim .bwd

  Rᴸ = QER→EquivRel R .fst .fst
  Rᴿ = QER→EquivRel (invQER R) .fst .fst

  Thm : (A / Rᴸ) ≃ (B / Rᴿ)
  Thm = isoToEquiv (iso φ ψ η ε)
    where
    φ : _
    φ [ a ] = [ f a ]
    φ (eq/ a₀ a₁ r i) = eq/ _ _ (sim .zigzag (sim .bwdRel (f a₁)) r (sim .fwdRel a₀)) i
    φ (squash/ _ _ p q j i) = squash/ _ _ (cong φ p) (cong φ q) j i

    ψ : _
    ψ [ b ] = [ g b ]
    ψ (eq/ b₀ b₁ s i) = eq/ _ _ (sim .zigzag (sim .bwdRel b₀) s (sim .fwdRel (g b₁))) i
    ψ (squash/ _ _ p q j i) = squash/ _ _ (cong ψ p) (cong ψ q) j i

    η = elimProp (λ _ → squash/ _ _) (λ b → eq/ _ _ (sim .fwdRel (g b)))

    ε = elimProp (λ _ → squash/ _ _) (λ a → eq/ _ _ (sim .bwdRel (f a)))

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --without-K #-}
module equality where

open import equality.core public
open import equality.reasoning public
open import equality.groupoid public
open import equality.calculus public
open import equality.inspect public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Productivity (char : Set) where

  open import Common.Coinduction

  infix  50 _⋆ _+
  infixl 40 _⊛_
  infixl 30 _∣_

  data P : Set where
    ε   : P
    sym : char -> P
    _⊛_ : ∞ P -> ∞ P -> P
    _∣_ : ∞ P -> ∞ P -> P

  mutual

    _⋆ : P -> P
    p ⋆ = ♯ ε ∣ ♯ (p +)

    _+ : P -> P
    p + = ♯ p ⊛ ♯ (p ⋆)

  _sepBy_ : P -> P -> P
  p sepBy sep = ♯ p ⊛ ♯ ((♯ sep ⊛ ♯ p) ⋆)

  postulate
    addOp  : P
    mulOp  : P
    number : P
    openP  : char
    closeP : char

  -- Not guarded:

  mutual
    expr   = term sepBy addOp
    term   = factor sepBy mulOp
    factor = ♯ number ∣ ♯ (♯ (♯ sym openP ⊛ ♯ expr) ⊛ ♯ sym closeP)

  -- Guarded and incomprehensible:

  mutual
    expr₁ = ♯ term₁ ⊛ ♯ expr₂
    expr₂ = ♯ ε ∣ ♯ expr₃
    expr₃ = ♯ (♯ addOp ⊛ ♯ term₁) ⊛ ♯ expr₂

    term₁ = ♯ factor₁ ⊛ ♯ term₂
    term₂ = ♯ ε ∣ ♯ term₃
    term₃ = ♯ (♯ mulOp ⊛ ♯ factor₁) ⊛ ♯ term₂

    factor₁ = ♯ number ∣ ♯ (♯ (♯ sym openP ⊛ ♯ expr₁) ⊛ ♯ sym closeP)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- 2012-10-20 Andreas
module Issue721a where

data Bool : Set where
  false true : Bool

record Foo (b : Bool) : Set where
  field
    _*_ : Bool → Bool → Bool

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

test : (F : Foo false) (x : Bool) → let open Foo F in _*_ x ≡ (λ x → x)
test F x = x
-- Don't want to see .Issue632._.* in the error message

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module ExtractCaseSplit where

open import Data.Maybe
open import Agda.Builtin.Bool

not : Bool -> Bool
not true = false
not false = true

func : Maybe Bool -> Bool

func nothing = false
func (just x) = not x

open import Data.List

func2 : List Bool -> Bool
func2 [] = true
func2 (x ∷ x₁) = not (func2 x₁)


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; refl ; trans ; cong₂ )
open import Relation.Unary using ( ∅ ; _∪_ )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )
open import Web.Semantic.Util using ( id ; _∘_ ; Subset ; ⁅_⁆ )

module Web.Semantic.DL.ABox where

infixr 5 _∼_ _∈₁_ _∈₂_
infixr 4 _,_

data ABox (Σ : Signature) (X : Set) : Set where
  ε : ABox Σ X
  _,_ : (A B : ABox Σ X) → ABox Σ X
  _∼_ : (x y : X) → ABox Σ X
  _∈₁_ : (x : X) → (c : CN Σ) → ABox Σ X
  _∈₂_ : (xy : X × X) → (r : RN Σ) → ABox Σ X

⟨ABox⟩ : ∀ {Σ X Y} → (X → Y) → ABox Σ X → ABox Σ Y
⟨ABox⟩ f ε              = ε
⟨ABox⟩ f (A , B)        = (⟨ABox⟩ f A , ⟨ABox⟩ f B)
⟨ABox⟩ f (x ∼ y)        = (f x ∼ f y)
⟨ABox⟩ f (x ∈₁ C)       = (f x ∈₁ C)
⟨ABox⟩ f ((x , y) ∈₂ R) = ((f x , f y) ∈₂ R)

⟨ABox⟩-resp-id : ∀ {Σ X} (A : ABox Σ X) → (⟨ABox⟩ id A ≡ A)
⟨ABox⟩-resp-id ε = refl
⟨ABox⟩-resp-id (A , B) = cong₂ _,_ (⟨ABox⟩-resp-id A) (⟨ABox⟩-resp-id B)
⟨ABox⟩-resp-id (x ∼ y) = refl
⟨ABox⟩-resp-id (x ∈₁ c) = refl
⟨ABox⟩-resp-id ((x , y) ∈₂ r) = refl

⟨ABox⟩-resp-∘ : ∀ {Σ X Y Z} (f : Y → Z) (g : X → Y) (A : ABox Σ X) → (⟨ABox⟩ f (⟨ABox⟩ g A) ≡ ⟨ABox⟩ (f ∘ g) A)
⟨ABox⟩-resp-∘ f g ε = refl
⟨ABox⟩-resp-∘ f g (A , B) = cong₂ _,_ (⟨ABox⟩-resp-∘ f g A) (⟨ABox⟩-resp-∘ f g B)
⟨ABox⟩-resp-∘ f g (x ∼ y) = refl
⟨ABox⟩-resp-∘ f g (x ∈₁ c) = refl
⟨ABox⟩-resp-∘ f g ((x , y) ∈₂ r) = refl

⟨ABox⟩-resp-∘² : ∀ {Σ W X Y Z} (f : Y → Z) (g : X → Y) (h : W → X) →
  ∀ (A : ABox Σ W) → (⟨ABox⟩ f (⟨ABox⟩ g (⟨ABox⟩ h A)) ≡ ⟨ABox⟩ (f ∘ g ∘ h) A)
⟨ABox⟩-resp-∘² f g h A =
  trans (⟨ABox⟩-resp-∘ f g (⟨ABox⟩ h A)) (⟨ABox⟩-resp-∘ (f ∘ g) h A)

Assertions : ∀ {Σ X} → ABox Σ X → Subset (ABox Σ X)
Assertions ε         = ∅
Assertions (A , B)   = (Assertions A) ∪ (Assertions B)
Assertions (x ∼ y)   = ⁅ x ∼ y ⁆
Assertions (x ∈₁ c)  = ⁅ x ∈₁ c ⁆
Assertions (xy ∈₂ r) = ⁅ xy ∈₂ r ⁆

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
-- Andreas, 2014-05-02  Negative fixities allow now.

module _ where

infix -1 _+_
infix 0  _*_

postulate
  _+_ : Set1 → Set2 → Set1
  _*_ : Set2 → Set2 → Set2

test = Set + Set1 * Set1


text:
-- Product of type-many categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Constructions.Product where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor.Base
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude

private
  variable
    ℓA ℓC ℓC' : Level

open Category

ΠC : (A : Type ℓA) → (catC : A → Category ℓC ℓC') → Category (ℓ-max ℓA ℓC) (ℓ-max ℓA ℓC')
ob (ΠC A catC) = (a : A) → ob (catC a)
Hom[_,_] (ΠC A catC) c c' = (a : A) → catC a [ c a , c' a ]
id (ΠC A catC) a = id (catC a)
_⋆_ (ΠC A catC) g f a = g a ⋆⟨ catC a ⟩ f a
⋆IdL (ΠC A catC) f = funExt λ a → ⋆IdL (catC a) (f a)
⋆IdR (ΠC A catC) f = funExt λ a → ⋆IdR (catC a) (f a)
⋆Assoc (ΠC A catC) h g f = funExt λ a → ⋆Assoc (catC a) (h a) (g a) (f a)
isSetHom (ΠC A catC) = isSetΠ (λ a → isSetHom (catC a))


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

module Cubical.Categories.Category.Properties where

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category.Base hiding (isSetHom)

open Precategory

private
  variable
    ℓ ℓ' : Level

module _ {C : Precategory ℓ ℓ'} ⦃ isC : isCategory C ⦄ where
  open isCategory isC
  -- isSet where your allowed to compare paths where one side is only
  -- equal up to path. Is there a generalization of this?
  isSetHomP1 : ∀ {x y : C .ob} {n : C [ x , y ]}
              → isOfHLevelDep 1 (λ m → m ≡ n)
  isSetHomP1 {x = x} {y} {n} = isOfHLevel→isOfHLevelDep 1 (λ m → isSetHom m n)

  -- isSet where the arrows can be between non-definitionally equal obs
  isSetHomP2l : ∀ {y : C .ob}
              → isOfHLevelDep 2 (λ x → C [ x , y ])
  isSetHomP2l = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom {x = a})

  isSetHomP2r : ∀ {x : C .ob}
              → isOfHLevelDep 2 (λ y → C [ x , y ])
  isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom {y = a})

-- opposite of opposite is definitionally equal to itself
involutiveOp : ∀ {C : Precategory ℓ ℓ'} → (C ^op) ^op ≡ C
involutiveOp = refl

module _ {C : Precategory ℓ ℓ'} where
  -- Other useful operations on categories

  -- whisker the parallel morphisms g and g' with f
  lPrecatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g') → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
  lPrecatWhisker f _ _ p = cong (_⋆_ C f) p

  rPrecatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f') → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g
  rPrecatWhisker _ _ g p = cong (λ v → v ⋆⟨ C ⟩ g) p

  -- working with equal objects
  idP : ∀ {x x'} {p : x ≡ x'} → C [ x , x' ]
  idP {x = x} {x'} {p} = subst (λ v → C [ x , v ]) p (C .id x)

  -- heterogeneous seq
  seqP : ∀ {x y y' z} {p : y ≡ y'}
       → (f : C [ x , y ]) (g : C [ y' , z ])
       → C [ x , z ]
  seqP {x = x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g)

  -- also heterogeneous seq, but substituting on the left
  seqP' : ∀ {x y y' z} {p : y ≡ y'}
       → (f : C [ x , y ]) (g : C [ y' , z ])
       → C [ x , z ]
  seqP' {x = x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g

  -- show that they're equal
  seqP≡seqP' : ∀ {x y y' z} {p : y ≡ y'}
             → (f : C [ x , y ]) (g : C [ y' , z ])
             → seqP {p = p} f g ≡ seqP' {p = p} f g
  seqP≡seqP' {x = x} {z = z} {p = p} f g i =
    (toPathP {A = λ i' → C [ x , p i' ]} {f} refl i)
      ⋆⟨ C ⟩
    (toPathP {A = λ i' → C [ p (~ i') , z ]} {x = g} (sym refl) (~ i))

  -- seqP is equal to normal seq when y ≡ y'
  seqP≡seq : ∀ {x y z}
             → (f : C [ x , y ]) (g : C [ y , z ])
             → seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g
  seqP≡seq {y = y} {z} f g i = f ⋆⟨ C ⟩ toPathP {A = λ _ → C [ y , z ]} {x = g} refl (~ i)

  -- whiskering with heterogenous seq -- (maybe should let z be heterogeneous too)
  lPrecatWhiskerP : {x y z y' : C .ob} {p : y ≡ y'}
                  → (f : C [ x , y ]) (g : C [ y , z ]) (g' : C [ y' , z ])
                  → (r : PathP (λ i → C [ p i , z ]) g g')
                  → f ⋆⟨ C ⟩ g ≡ seqP {p = p} f g'
  lPrecatWhiskerP f g g' r = cong (λ v → f ⋆⟨ C ⟩ v) (sym (fromPathP (symP r)))

  rPrecatWhiskerP : {x y' y z : C .ob} {p : y' ≡ y}
                  → (f' : C [ x , y' ]) (f : C [ x , y ]) (g : C [ y , z ])
                  → (r : PathP (λ i → C [ x , p i ]) f' f)
                  → f ⋆⟨ C ⟩ g ≡ seqP' {p = p} f' g
  rPrecatWhiskerP f' f g r = cong (λ v → v ⋆⟨ C ⟩ g) (sym (fromPathP r))

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:
module Assume where

postulate
  assume : ∀ {a} {A : Set a} → A

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
{-# OPTIONS --sized-types #-}
module BinTree where

open import Data.Nat
open import Data.List
open import Data.List.Properties
open import Size

data Bin {T : Set} {i : Size} : Set where
  Leaf : Bin {T} {i}
  Node : T → Bin {T} {i} → Bin {T} {i} → Bin {T} {i}

data Rose {T : Set} {i : Size} : Set where
  Empty : Rose {T} {i}
  R : T → List (Rose {T} {i}) → Rose {T} {i}

BinListToBin : {T : Set} → List (Bin {T}) → Bin {T}
BinListToBin [] = Leaf
BinListToBin (Leaf ∷ bs) = BinListToBin bs
BinListToBin (Node x b b₁ ∷ bs) = Node x b (BinListToBin bs)

Seperate : {T : Set} → Bin {T} → List (Bin {T})
Seperate Leaf = []
Seperate (Node x b b₁) = Node x b Leaf ∷ Seperate b₁

RoseToBin : {i : Size} → {T : Set} → Rose {T} {∞} → Bin {T} {∞}
RoseToBin Empty = Leaf
RoseToBin (R x x₁) = Node x (BinListToBin (map RoseToBin x₁)) Leaf

BinToRose : {T : Set} → Bin {T} → Rose {T}
BinToRose Leaf = Empty
BinToRose (Node x b b₁) = R x (map BinToRose (Seperate b₁))

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import Algebra.Structures.Bundles.Field

module Algebra.Structures.Field.Utils
  {k ℓ} (K : Field k ℓ)
  where

open Field K hiding (zero)

open import Data.Fin
import Data.Nat as Nat

private
  K' : Set k
  K' = Carrier

δ : ∀ {n p} -> Fin n -> Fin p -> K'
δ zero zero = 1#
δ (suc i) zero = 0#
δ zero (suc j) = 0#
δ (suc i) (suc j) = δ i j

δ-comm : ∀ {n p} (i : Fin n) (j : Fin p) -> δ i j ≈ δ j i
δ-comm zero zero = refl
δ-comm (suc i) zero = refl
δ-comm zero (suc j) = refl
δ-comm (suc i) (suc j) = δ-comm i j

δ-cancelˡ : ∀ {n p} (j : Fin p) -> δ {Nat.suc n} zero (suc j) ≈ 0#
δ-cancelˡ zero = refl
δ-cancelˡ (suc j) = refl

δ-cancelʳ : ∀ {n p} (i : Fin n) -> δ {p = Nat.suc p} (suc i) zero ≈ 0#
δ-cancelʳ {n} {p} i = trans (δ-comm (suc i) (zero {Nat.suc p})) (δ-cancelˡ {p} {n} i)

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
module Data.Num.Bij where

open import Data.List hiding ([_])
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_)
import Level
--------------------------------------------------------------------------------
-- Bijective Numeration
--
--  A numeral system which has a unique representation for every non-negative
--  interger
--  http://en.wikipedia.org/wiki/Bijective_numeration
--------------------------------------------------------------------------------

-- zeroless binary number

infixl 7 _*B_
infixl 6 _+B_

data DigitB : Set where
    one : DigitB
    two : DigitB

Bij : Set
Bij = List DigitB

incrB : Bij → Bij
incrB []        = one ∷ []
incrB (one ∷ a) = two ∷ a
incrB (two ∷ a) = one ∷ incrB a

-- addition
_+B_ : Bij → Bij → Bij
[]         +B b        = b
a          +B []       = a
(one ∷ as) +B (one ∷ bs) = two ∷ as +B bs
(one ∷ as) +B (two ∷ bs) = one ∷ incrB (as +B bs)
(two ∷ as) +B (one ∷ bs) = one ∷ incrB (as +B bs)
(two ∷ as) +B (two ∷ bs) = two ∷ incrB (as +B bs)

-- arithmetic shift
*2_ : Bij → Bij
*2 []         = []
*2 (one ∷ as) = two ∷ *2 as
*2 (two ∷ as) = two ∷ incrB (*2 as)

-- multiplication
_*B_ : Bij → Bij → Bij
[]         *B b = []
(one ∷ as) *B b =      b +B (*2 (as *B b))
(two ∷ as) *B b = b +B b +B (*2 (as *B b))

--------------------------------------------------------------------------------
-- Ordering
--------------------------------------------------------------------------------

infix 4 _≤-digitB_ _≤B_ _<B_

data _≤-digitB_ : Rel DigitB Level.zero where
    1≤1 : one ≤-digitB one
    1≤2 : one ≤-digitB two
    2≤2 : two ≤-digitB two

data _≤B_ : Rel Bij Level.zero where
    []≤all : ∀ {n} → [] ≤B n
    ≤here : ∀ {as bs a b}           -- compare the least digit
            → {a≤b : a ≤-digitB b}
            → {as≡bs : as ≡ bs}
            → a ∷ as ≤B b ∷ bs
    ≤there : ∀ {as bs a b}
             → (as<bs : incrB as ≤B bs) -- compare the rest digits
             → a ∷ as ≤B b ∷ bs

_<B_ : Rel Bij Level.zero
a <B b = incrB a ≤B b

{-

decr : Bij → Bij
decr [] = []
decr (one ∷ a) = a
decr (two ∷ a) = one ∷ a

_-_ : Bij → Bij → Bij
[] - bs = []
as - [] = as
(one ∷ as) - (one ∷ bs) = as - bs
(one ∷ as) - (two ∷ bs) = one ∷ decr (as - bs)
(two ∷ as) - (one ∷ bs) = one ∷ as - bs
(two ∷ as) - (two ∷ bs) = as - bs
-}

--------------------------------------------------------------------------------
--  typeclass for converting data types to Bij
--  http://people.cs.kuleuven.be/~dominique.devriese/agda-instance-arguments/icfp001-Devriese.pdf

record Conversion (t : Set) : Set where
    constructor conversion
    field
        [_] : t   → Bij
        !_! : Bij → t
        -- split morphism
        -- !_! is a section of [_]
        -- [_] is a retraction of !_!
        -- [!!]-id : ∀ n → [ ! n ! ] ≡ n

[_] : ∀ {t} → {{convT : Conversion t}} → t → Bij
[_] {{convT}} = Conversion.[ convT ]

!_! : ∀ {t} → {{convT : Conversion t}} → Bij → t
!_! {{convT}} = Conversion.! convT !

--[!!]-id : ∀ {t} → {{convT : Conversion t}} → (n : Bij) → [ ! n ! ] ≡ n
--[!!]-id {{convT}} = Conversion.[!!]-id convT

-- alias, more meaningful than the forgettable [_] and !_! (replace them some day)
toBij = [_]
fromBij = !_!

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

open import GroupoidStructure
open import NTypes
open import NTypes.Negation
open import PathOperations
open import Transport
open import Types

stable : ∀ {a} → Set a → Set a
stable A = ¬ ¬ A → A

dec : ∀ {a} → Set a → Set a
dec A = A ⊎ ¬ A

dec→stable : ∀ {a} {A : Set a} → dec A → stable A
dec→stable {A = A} = case (λ _ → stable A)
  (λ  a   _ → a)
  (λ ¬a ¬¬a → 0-elim (¬¬a ¬a))

dec-eq : ∀ {a} → Set a → Set a
dec-eq A = (x y : A) → dec (x ≡ y)

stable-eq : ∀ {a} → Set a → Set a
stable-eq A = (x y : A) → stable (x ≡ y)

dec-eq→stable-eq : ∀ {a} {A : Set a} → dec-eq A → stable-eq A
dec-eq→stable-eq dec x y = dec→stable (dec x y)

-- Lemma 2.9.6 from HoTT book.
lemma : ∀ {a b c} {A : Set a} {B : A → Set b} {C : A → Set c}
  {x y : A} (p : x ≡ y) (f : B x → C x) (g : B y → C y) →
  tr _ p f ≡ g → (b : B x) → tr _ p (f b) ≡ g (tr _ p b)
lemma {B = B} {C = C} = J
  (λ x y p → (f : B x → C x) (g : B y → C y) →
    tr _ p f ≡ g → (b : B x) → tr _ p (f b) ≡ g (tr _ p b))
  (λ _ _ _ → happly) _ _

stable-eq→set : ∀ {a} {A : Set a} → stable-eq A → isSet A
stable-eq→set {A = A} h _ _ p q = J
  (λ x y p → (q : x ≡ y) → q ≡ p)
  K _ _ q p
  where
  K : (x : A) (p : x ≡ x) → p ≡ refl
  K x p
    = id·p _ ⁻¹
    · ap (λ z → z · p)
      (p⁻¹·p (h x x r)) ⁻¹
    · p·q·r (h x x r ⁻¹) (h x x r) p ⁻¹
    · ap (λ z → h x x r ⁻¹ · z)
      ( tr-post x p (h x x r) ⁻¹
      · lemma p (h x x) (h x x) (apd (h x) p) r
      · ap (h x x)
        (¬-isProp (tr (λ v → ¬ ¬ (x ≡ v)) p r) r)
      )
    · p⁻¹·p (h x x r)
    where
    -- Choice of r doesn't matter.
    r : ¬ ¬ (x ≡ x)
    r c = c refl

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X] where

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

open import Cubical.Data.Nat using (ℕ ; zero ; suc)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.Sigma

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- Lift

open IsRingHom
open CommRingStr

module _
  (A'@(A , Astr) : CommRing ℓ)
  (B'@(B , Bstr) : CommRing ℓ)
  (n : ℕ)
  where

  private
    PA = PolyCommRing A' n
    PB = PolyCommRing B' n

  makeCommRingHomPoly : (f : CommRingHom A' B') → CommRingHom (PolyCommRing A' n) (PolyCommRing B' n)
  fst (makeCommRingHomPoly (f , fstr)) = DS-Rec-Set.f _ _ _ _ trunc
                                         (0r (snd PB))
                                         (λ v a → base v (f a))
                                         (_+_ (snd PB))
                                         (+Assoc (snd PB))
                                         (+IdR (snd PB))
                                         (+Comm (snd PB))
                                         (λ v → (cong (base v) (pres0 fstr)) ∙ (base-neutral v))
                                         (λ v a b → (base-add v (f a) (f b)) ∙ (cong (base v) (sym (pres+ fstr a b))))
  snd (makeCommRingHomPoly (f , fstr)) = makeIsRingHom
                                         (cong (base (replicate zero)) (pres1 fstr))
                                         (λ _ _ → refl)
                                         (DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ λ _ → trunc _ _)
                                             (λ _ → refl)
                                             (λ v a → DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                                                                    refl
                                                                    (λ v' b → cong (base (v +n-vec v')) (pres· fstr a b))
                                                                    (λ {U V} ind-U ind-V → cong₂ (_+_ (snd PB)) ind-U  ind-V))
                                             λ {U V} ind-U ind-V Q → cong₂ (_+_ (snd PB)) (ind-U Q) (ind-V Q))

-----------------------------------------------------------------------------
-- Lift preserve equivalence

module _
  (A'@(A , Astr) : CommRing ℓ)
  (B'@(B , Bstr) : CommRing ℓ)
  (n : ℕ)
  where

  private
    PA = PolyCommRing A' n
    PB = PolyCommRing B' n

  open Iso
  open RingEquivs

  lift-equiv-poly : (e : CommRingEquiv A' B') → CommRingEquiv (PolyCommRing A' n) (PolyCommRing B' n)
  fst (lift-equiv-poly (e , fstr)) = isoToEquiv is
    where
    f = fst e
    g = invEq e
    gstr : IsRingHom (snd (CommRing→Ring B')) g (snd (CommRing→Ring A'))
    gstr = isRingHomInv (e , fstr)

    is : Iso (fst PA) (fst PB)
    fun is = fst (makeCommRingHomPoly A' B' n (f , fstr))
    inv is = fst (makeCommRingHomPoly B' A' n (g , gstr))
    rightInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                  refl
                  (λ v a → cong (base v) (secEq e a))
                  λ {U V} ind-U ind-V → cong₂ (_+_ (snd PB)) ind-U ind-V
    leftInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                 refl
                 (λ v a → cong (base v) (retEq e a))
                 λ {U V} ind-U ind-V → cong₂ (_+_ (snd PA)) ind-U ind-V
  snd (lift-equiv-poly (e , fstr)) = snd (makeCommRingHomPoly A' B' n ((fst e) , fstr))


text:
module Imports.Issue5357-D where
A : Set₁
A = Set₁

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

data _≅_ {ℓ} {A : Set ℓ} (x : A) : {B : Set ℓ} → B → Set where
  refl : x ≅ x

{-# BUILTIN REWRITE _≅_ #-}


text:
-- Andreas, 2011-04-07

module IrrelevantTelescopeRecord where

record Wrap .(A : Set) : Set where
  field
    out : A
-- cannot use A, because it is declared irrelevant


text:
{-# BUILTIN STRING String #-}

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

nonEmpty : String → Set
nonEmpty "" = Bool
nonEmpty _  = ⊤

foo : ∀ s → nonEmpty s → Bool
foo "" true  = true
foo "" false = false
foo s  p     = false


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Representable where

open import Level

open import Categories.Category
open import Categories.Agda
open import Categories.Functor using (Functor)
open import Categories.Functor.Hom
open import Categories.NaturalIsomorphism

record Representable {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ suc ℓ ⊔ suc e) where
  open Category C
  open Hom C
  field
    F : Functor C (ISetoids ℓ e) -- should this be a parameter to the record?
    A : Obj
    Iso : NaturalIsomorphism F Hom[ A ,-]

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Define the integers as a HIT by identifying +0 and -0
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Ints.QuoInt.Base where

open import Cubical.Core.Everything

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

open import Cubical.Data.Int hiding (abs; sgn)
open import Cubical.Data.Nat

data ℤ : Type₀ where
  pos    : (n : ℕ) → ℤ
  neg    : (n : ℕ) → ℤ
  posneg : pos 0 ≡ neg 0

recℤ : ∀ {l} {A : Type l} → (pos' neg' : ℕ → A) → pos' 0 ≡ neg' 0 → ℤ → A
recℤ pos' neg' eq (pos m)    = pos' m
recℤ pos' neg' eq (neg m)    = neg' m
recℤ pos' neg' eq (posneg i) = eq i

indℤ : ∀ {l} (P : ℤ → Type l)
       → (pos' : ∀ n → P (pos n))
       → (neg' : ∀ n → P (neg n))
       → (λ i → P (posneg i)) [ pos' 0 ≡ neg' 0 ]
       → ∀ z → P z
indℤ P pos' neg' eq (pos n) = pos' n
indℤ P pos' neg' eq (neg n) = neg' n
indℤ P pos' neg' eq (posneg i) = eq i

Int→ℤ : Int → ℤ
Int→ℤ (pos n) = pos n
Int→ℤ (negsuc n) = neg (suc n)

ℤ→Int : ℤ → Int
ℤ→Int (pos n) = pos n
ℤ→Int (neg zero) = pos 0
ℤ→Int (neg (suc n)) = negsuc n
ℤ→Int (posneg _) = pos 0

ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n
ℤ→Int→ℤ (pos n) _       = pos n
ℤ→Int→ℤ (neg zero) i    = posneg i
ℤ→Int→ℤ (neg (suc n)) _ = neg (suc n)
ℤ→Int→ℤ (posneg j) i    = posneg (j ∧ i)

Int→ℤ→Int : ∀ (n : Int) → ℤ→Int (Int→ℤ n) ≡ n
Int→ℤ→Int (pos n) _ = pos n
Int→ℤ→Int (negsuc n) _ = negsuc n

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

isSetℤ : isSet ℤ
isSetℤ = subst isSet Int≡ℤ isSetInt

sucℤ : ℤ → ℤ
sucℤ (pos n)       = pos (suc n)
sucℤ (neg zero)    = pos 1
sucℤ (neg (suc n)) = neg n
sucℤ (posneg _)    = pos 1

predℤ : ℤ → ℤ
predℤ (pos zero)    = neg 1
predℤ (pos (suc n)) = pos n
predℤ (neg n)       = neg (suc n)
predℤ (posneg _)    = neg 1

sucPredℤ : ∀ n → sucℤ (predℤ n) ≡ n
sucPredℤ (pos zero)    = sym posneg
sucPredℤ (pos (suc _)) = refl
sucPredℤ (neg _)       = refl
sucPredℤ (posneg i) j  = posneg (i ∨ ~ j)

predSucℤ : ∀ n → predℤ (sucℤ n) ≡ n
predSucℤ (pos _)       = refl
predSucℤ (neg zero)    = posneg
predSucℤ (neg (suc _)) = refl
predSucℤ (posneg i) j  = posneg (i ∧ j)

_+ℤ_ : ℤ → ℤ → ℤ
m +ℤ (pos (suc n)) = sucℤ   (m +ℤ pos n)
m +ℤ (neg (suc n)) = predℤ  (m +ℤ neg n)
m +ℤ _             = m

sucPathℤ : ℤ ≡ ℤ
sucPathℤ  = isoToPath (iso sucℤ predℤ sucPredℤ predSucℤ)

-- We do the same trick as in Cubical.Data.Int to prove that addition
-- is an equivalence
addEqℤ : ℕ → ℤ ≡ ℤ
addEqℤ zero    = refl
addEqℤ (suc n) = addEqℤ n ∙ sucPathℤ

predPathℤ : ℤ ≡ ℤ
predPathℤ = isoToPath (iso predℤ sucℤ predSucℤ sucPredℤ)

subEqℤ : ℕ → ℤ ≡ ℤ
subEqℤ zero    = refl
subEqℤ (suc n) = subEqℤ n ∙ predPathℤ

addℤ : ℤ → ℤ → ℤ
addℤ m (pos n)    = transport (addEqℤ n) m
addℤ m (neg n)    = transport (subEqℤ n) m
addℤ m (posneg _) = m

isEquivAddℤ : (m : ℤ) → isEquiv (λ n → addℤ n m)
isEquivAddℤ (pos n)    = isEquivTransport (addEqℤ n)
isEquivAddℤ (neg n)    = isEquivTransport (subEqℤ n)
isEquivAddℤ (posneg _) = isEquivTransport refl

addℤ≡+ℤ : addℤ ≡ _+ℤ_
addℤ≡+ℤ i  m (pos (suc n)) = sucℤ   (addℤ≡+ℤ i m (pos n))
addℤ≡+ℤ i  m (neg (suc n)) = predℤ  (addℤ≡+ℤ i m (neg n))
addℤ≡+ℤ i  m (pos zero)    = m
addℤ≡+ℤ i  m (neg zero)    = m
addℤ≡+ℤ _  m (posneg _)    = m

isEquiv+ℤ : (m : ℤ) → isEquiv (λ n → n +ℤ m)
isEquiv+ℤ = subst (λ _+_ → (m : ℤ) → isEquiv (λ n → n + m)) addℤ≡+ℤ isEquivAddℤ

data Sign : Type₀ where
  pos neg : Sign

sign : ℤ → Sign
sign (pos n)       = pos
sign (neg 0)       = pos
sign (neg (suc n)) = neg
sign (posneg i)    = pos

abs : ℤ → ℕ
abs (pos n) = n
abs (neg n) = n
abs (posneg i) = 0

signed : Sign → ℕ → ℤ
signed Sign.pos n = pos n
signed Sign.neg n = neg n

signed-inv : ∀ z → signed (sign z) (abs z) ≡ z
signed-inv (pos n)       = refl
signed-inv (neg zero)    = posneg
signed-inv (neg (suc n)) = refl
signed-inv (posneg i)    = \ j → posneg (i ∧ j)
{-

 The square for   signed-inv (posneg i)

              posneg i
       --------------------->
       ^                     ^
       |                     |
 pos 0 |                     | posneg j
       |                     |
       |                     |
       |                     |
       ---------------------->
         = pos 0
         = signed Sign.pos 0
         signed (sign (posneg i))
                (abs (posneg i))
-}

-- * Multiplication

_*S_ : Sign → Sign → Sign
pos *S neg = neg
neg *S pos = neg
_   *S _   = pos

_*ℤ_ : ℤ → ℤ → ℤ
m *ℤ n = signed (sign m *S sign n) (abs m * abs n)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module examplesPaperJFP.exampleFinFun where

open import examplesPaperJFP.finn

open import Data.Nat

toℕ : ∀ {n} → Fin n → ℕ
toℕ  zero     =  0
toℕ  (suc n)  =  suc (toℕ n)

mutual
  _+e_ : ∀ {n m} →  Even n   →  Even m  →  Even  (n + m)
  0p      +e  p  =  p
  sucp p  +e  q  =  sucp  (p +o q)

  _+o_ : ∀ {n m}  →  Odd n   →  Even m  →  Odd   (n + m)
  sucp p  +o  q  =  sucp  (p +e q)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Singleton where

open import Data.List
  using (List ; [] ; _∷_)
open import Data.List.All
  using (All ; [] ; _∷_)
open import Membership
  using (_∈_; _⊆_ ; _∷_ ; [])

[_]ˡ : ∀{a}{A : Set a} → A → List A
[ a ]ˡ = a ∷ []

[_]ᵃ : ∀{a p} {A : Set a} {P : A → Set p} {x : A} → P x → All P (x ∷ [])
[ p ]ᵃ = p ∷ []

[_]ᵐ :  ∀{a} {A : Set a} {x : A} {ys : List A} → (x ∈ ys) → ((x ∷ []) ⊆ ys)
[ p ]ᵐ = p ∷ []

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
-- Coalgebraic strength over an endofunctor
module SOAS.Coalgebraic.Strength {T : Set} where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core {T}
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted

open import SOAS.Coalgebraic.Map

private
  variable
    Γ Δ Θ : Ctx
    α : T

-- Pointed coalgebraic strength for a family endofunctor
record Strength (Fᶠ : Functor 𝔽amiliesₛ 𝔽amiliesₛ) : Set₁ where
  open Functor Fᶠ
  open Coalgₚ

  field
    -- Strength transformation that lifts a 𝒫-substitution over an endofunctor F₀
    str : {𝒫 : Familyₛ}(𝒫ᴮ : Coalgₚ 𝒫)(𝒳 : Familyₛ)
        → F₀ 〖 𝒫 , 𝒳 〗 ⇾̣ 〖 𝒫 , F₀ 𝒳 〗

    -- Naturality conditions for the two components
    str-nat₁ : {𝒫 𝒬 𝒳 : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}{𝒬ᴮ : Coalgₚ 𝒬}
             → {f : 𝒬 ⇾̣ 𝒫} (fᴮ⇒ : Coalgₚ⇒ 𝒬ᴮ 𝒫ᴮ f)
             → (h : F₀ 〖 𝒫 , 𝒳 〗 α Γ) (σ : Γ ~[ 𝒬 ]↝ Δ)
      → str 𝒫ᴮ 𝒳 h (f ∘ σ)
      ≡ str 𝒬ᴮ 𝒳 (F₁ (λ{ h′ ς → h′ (λ v → f (ς v))}) h) σ

    str-nat₂ : {𝒫 𝒳 𝒴 : Familyₛ}{𝒫ᴮ : Coalgₚ 𝒫}
             → (f : 𝒳 ⇾̣ 𝒴)(h : F₀ 〖 𝒫 , 𝒳 〗 α Γ)(σ : Γ ~[ 𝒫 ]↝ Δ)
      → str 𝒫ᴮ 𝒴 (F₁ (λ{ h′ ς → f (h′ ς)}) h) σ
      ≡ F₁ f (str 𝒫ᴮ 𝒳 h σ)

    -- Unit law
    str-unit : (𝒳 : Familyₛ)(h : F₀ 〖 ℐ , 𝒳 〗 α Γ)
      → str ℐᴮ 𝒳 h id
      ≡ F₁ (i 𝒳) h

    -- Associativity law for a particular pointed coalgebraic map f
    str-assoc  : (𝒳 : Familyₛ){𝒫 𝒬 ℛ : Familyₛ}
                 {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
                 {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
                 (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f) (open Coalgebraic fᶜ)
                 (h : F₀ 〖 ℛ , 𝒳 〗 α Γ)(σ : Γ ~[ 𝒫 ]↝ Δ)(ς : Δ ~[ 𝒬 ]↝ Θ)
      → str ℛᴮ 𝒳 h (λ v → f (σ v) ς)
      ≡ str 𝒬ᴮ 𝒳 (str 〖𝒫,𝒴〗ᴮ 〖 𝒬 , 𝒳 〗 (F₁ (L 𝒬 ℛ 𝒳) h) (f ∘ σ)) ς

  module _ (𝒳 {𝒫 𝒬 ℛ} : Familyₛ) where

    -- Precompose an internal hom by a parametrised map
    precomp : (f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗) → 〖 ℛ , 𝒳 〗 ⇾̣ 〖 𝒫 , 〖 𝒬 , 𝒳 〗 〗
    precomp f h σ ς = h (λ v → f (σ v) ς)

    -- Corollary: strength distributes over pointed coalgebraic maps
    str-dist : {𝒫ᴮ : Coalgₚ 𝒫} {𝒬ᴮ : Coalgₚ 𝒬} {ℛᴮ : Coalgₚ ℛ}
               {f : 𝒫 ⇾̣ 〖 𝒬 , ℛ 〗}
               (fᶜ : Coalgebraic 𝒫ᴮ 𝒬ᴮ ℛᴮ f)
               (h : F₀ 〖 ℛ , 𝒳 〗 α Γ)(σ : Γ ~[ 𝒫 ]↝ Δ)(ς : Δ ~[ 𝒬 ]↝ Θ)
      → str ℛᴮ 𝒳 h (λ v → f (σ v) ς)
      ≡ str 𝒬ᴮ 𝒳 (str 𝒫ᴮ 〖 𝒬 , 𝒳 〗 (F₁ (precomp f) h) σ) ς
    str-dist {𝒫ᴮ = 𝒫ᴮ} {𝒬ᴮ} {ℛᴮ} {f} fᶜ h σ ς =
      begin
          str ℛᴮ 𝒳 h (λ v → f (σ v) ς)
      ≡⟨ str-assoc 𝒳 fᶜ h σ ς ⟩
          str 𝒬ᴮ 𝒳 (str 〖𝒫,𝒴〗ᴮ 〖 𝒬 , 𝒳 〗 (F₁ (L 𝒬 ℛ 𝒳) h) (f ∘ σ)) ς
      ≡⟨ cong (λ - → str 𝒬ᴮ 𝒳 - ς) (str-nat₁ fᴮ⇒ (F₁ (L 𝒬 ℛ 𝒳) h) σ) ⟩
          str 𝒬ᴮ 𝒳 (str 𝒫ᴮ 〖 𝒬 , 𝒳 〗 (F₁ 〖 f , 〖 𝒬 , 𝒳 〗 〗ₗ
                                        (F₁ (L 𝒬 ℛ 𝒳) h)) σ) ς
      ≡˘⟨ cong (λ - → str 𝒬ᴮ 𝒳 (str 𝒫ᴮ 〖 𝒬 , 𝒳 〗 - σ) ς) homomorphism ⟩
          str 𝒬ᴮ 𝒳 (str 𝒫ᴮ 〖 𝒬 , 𝒳 〗 (F₁ (precomp f) h) σ) ς
      ∎
      where
      open ≡-Reasoning
      open Coalgebraic fᶜ renaming (ᴮ⇒ to fᴮ⇒)

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Categories.Category

module Categories.Functor.Core where

open import Level

private
  variable
    o ℓ e o′ ℓ′ e′ : Level

record Functor (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  eta-equality
  private module C = Category C
  private module D = Category D

  field
    F₀ : C.Obj → D.Obj
    F₁ : ∀ {A B} (f : C [ A , B ]) → D [ F₀ A , F₀ B ]

    identity     : ∀ {A} → D [ F₁ (C.id {A}) ≈ D.id ]
    homomorphism : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]} →
                     D [ F₁ (C [ g ∘ f ]) ≈ D [ F₁ g ∘ F₁ f ] ]
    F-resp-≈     : ∀ {A B} {f g : C [ A , B ]} → C [ f ≈ g ] → D [ F₁ f ≈ F₁ g ]

  -- nice shorthands
  ₀ = F₀
  ₁ = F₁

  op : Functor C.op D.op
  op = record
    { F₀           = F₀
    ; F₁           = F₁
    ; identity     = identity
    ; homomorphism = homomorphism
    ; F-resp-≈     = F-resp-≈
    }

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


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

open import Bundles

module Properties.ConstructiveField {ℓ ℓ'} (F : ConstructiveField {ℓ} {ℓ'}) where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`

open import Function.Base using (it) -- instance search

open import MoreLogic
open MoreLogic.Reasoning
import MoreAlgebra

-- Lemma 4.1.6.
-- For a constructive field (F, 0, 1, +, ·, #), the following hold.
-- 1. 1 # 0.
-- 2. Addition + is #-compatible in the sense that for all x, y, z : F
--    x # y ⇔ x + z # y + z.
-- 3. Multiplication · is #-extensional in the sense that for all w, x, y, z : F
--    w · x # y · z ⇒ w # y ∨ x # z.

open ConstructiveField F

open import Cubical.Structures.Ring
R = (makeRing 0f 1f _+_ _·_ -_ is-set +-assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+)
open Cubical.Structures.Ring.Theory R
open MoreAlgebra.Properties.Ring R

-- Lemma 4.1.6.1
1f#0f : 1f # 0f
1f#0f with ·-identity 1f
1f#0f | 1·1≡1 , _ = fst (·-inv-back _ _ 1·1≡1)

-- Lemma 4.1.6.2
--   For #-compatibility of +, suppose x # y, that is, (x +z) −z # (y +z) −z.
--   Then #-extensionality gives (x + z # y + z) ∨ (−z # −z), where the latter case is excluded by irreflexivity of #.
+-#-compatible : ∀(x y z : Carrier) → x # y → x + z # y + z
+-#-compatible x y z x#y with
  let P = transport (λ i →  a+b-b≡a x z i # a+b-b≡a y z i ) x#y
  in  +-#-extensional _ _ _ _ P
... | inl x+z#y+z = x+z#y+z
... | inr  -z#-z  = ⊥-elim (#-irrefl _ -z#-z)

-- The other direction is similar.
+-#-compatible-inv : ∀(x y z : Carrier) → x + z # y + z → x # y
+-#-compatible-inv _ _ _ x+z#y+z with +-#-extensional _ _ _ _ x+z#y+z
... | inl x#y = x#y
... | inr z#z = ⊥-elim (#-irrefl _ z#z)

-- Lemma 4.1.6.3
·-#-extensional-case1 : ∀(w x y z : Carrier) → w · x # y · z → w · x # w · z → x # z
·-#-extensional-case1 w x y z w·x#y·z w·x#w·z =
  let
    instance -- this allows to use ⁻¹ᶠ without an instance argument
      w·[z-x]#0f =
        ( w · x         # w ·  z         ⇒⟨ +-#-compatible _ _ (- (w · x)) ⟩
          w · x - w · x # w ·  z - w · x ⇒⟨ transport (λ i →  (fst (+-inv (w · x)) i) # a·b-a·c≡a·[b-c] w z x i) ⟩
                     0f # w · (z - x)    ⇒⟨ #-sym _ _ ⟩
          w ·   (z - x) # 0f             ◼) w·x#w·z
  in  (    w  · (z - x) # 0f                      ⇒⟨ (λ _ → ·-rinv (w · (z - x)) it ) ⟩  -- NOTE: "plugging in" the instance did not work, ∴ `it`
           w  · (z - x) · (w · (z - x)) ⁻¹ᶠ  ≡ 1f ⇒⟨ transport (λ i → ·-comm w (z - x) i · (w · (z - x)) ⁻¹ᶠ ≡ 1f) ⟩
      (z - x) ·  w      · (w · (z - x)) ⁻¹ᶠ  ≡ 1f ⇒⟨ transport (λ i → ·-assoc (z - x) w ((w · (z - x)) ⁻¹ᶠ) (~ i) ≡ 1f) ⟩
      (z - x) · (w      · (w · (z - x)) ⁻¹ᶠ) ≡ 1f ⇒⟨ fst ∘ (·-inv-back _ _)  ⟩
         z    - x       # 0f                      ⇒⟨ +-#-compatible _ _ x ⟩
        (z    - x) + x  # 0f + x                  ⇒⟨ transport (λ i → +-assoc z (- x) x (~ i) # snd (+-identity x) i) ⟩
         z + (- x  + x) #      x                  ⇒⟨ transport (λ i → z + snd (+-inv x) i # x) ⟩
         z +      0f    # x                       ⇒⟨ transport (λ i → fst (+-identity z) i # x) ⟩
         z              # x                       ⇒⟨ #-sym _ _ ⟩
         x              # z                       ◼) it -- conceptually we would plug `w·[z-x]#0f` in, but this breaks the very first step

·-#-extensional : ∀(w x y z : Carrier) → w · x # y · z → (w # y) ⊎ (x # z)
·-#-extensional w x y z w·x#y·z with #-cotrans _ _ w·x#y·z (w · z)
... | inl w·x#w·z =    inr (·-#-extensional-case1 w x y z w·x#y·z w·x#w·z) -- first case
... | inr w·z#y·z = let z·w≡z·y = (transport (λ i → ·-comm w z i # ·-comm y z i) w·z#y·z)
                    in inl (·-#-extensional-case1 _ _ _ _ z·w≡z·y z·w≡z·y) -- second case reduced to first case

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module sets.bool where

open import sets.empty     using (⊥)
open import sets.unit      using (⊤)
open import decidable using (Dec; yes; no)
open import equality.core        using (_≡_; refl)
open import level     using (Level)

infixr 6 _∧_
infixr 5 _∨_ _xor_
infix  0 if_then_else_

data Bool : Set where
  true false : Bool

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

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

if_then_else_ : {a : Level} {A : Set a} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

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

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

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b

_≟_ : (a b : Bool) → Dec (a ≡ b)
true  ≟ true  = yes refl
false ≟ false = yes refl
true  ≟ false = no λ ()
false ≟ true  = no λ ()

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
open import Relation.Binary.Core

module BBHeap.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap.Complete.Base _≤_
open import BBHeap.Drop _≤_ tot≤ trans≤
open import BBHeap.DropLast _≤_
open import BBHeap.Heap _≤_
open import BBHeap.Height.Convert _≤_ tot≤
open import BBHeap.Height.Log _≤_ tot≤
open import BBHeap.Last

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting