text:
------------------------------------------------------------------------
-- A variant of set quotients with erased higher constructors
------------------------------------------------------------------------

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

-- Partly following the HoTT book, but adapted for erasure.
--
-- Unlike the HoTT book, but following the cubical library (in which
-- set quotients were implemented by Zesen Qian and Anders Mörtberg),
-- the quotienting relations are not (always) required to be
-- propositional.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining quotients use path equality, but
-- the supplied notion of equality is used for many other things.

import Equality.Path as P

module Quotient.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

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

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J using (Constant)
open import Equality.Path.Isomorphisms eq
import Equality.Path.Isomorphisms.Univalence eq as U
open import Equivalence equality-with-J as Eq using (_≃_)
import Equivalence.Erased equality-with-J as EEq
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as Er using (Erased; Erasedᴾ; [_])
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as PT using (∥_∥; ∣_∣)
open import H-level.Truncation.Propositional.Erased eq as PTᴱ
  using (∥_∥ᴱ; ∣_∣; Surjectiveᴱ)
open import Quotient eq as Q using (_/_)
open import Sum equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

private
  variable
    a a₁ a₂ p r r₁ r₂ : Level
    A A₁ A₂ B         : Type a
    P                 : A → Type p
    R                 : A → A → Type r
    f k x y           : A

------------------------------------------------------------------------
-- A re-export

-- This module re-exports Quotient.Erased.Basics.

open import Quotient.Erased.Basics eq public

------------------------------------------------------------------------
-- Preservation lemmas

-- Two preservation lemmas for functions.

infix 5 _/ᴱ-map-∥∥_ _/ᴱ-map_

_/ᴱ-map-∥∥_ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁→A₂ : A₁ → A₂) →
  @0 (∀ x y → ∥ R₁ x y ∥ → ∥ R₂ (A₁→A₂ x) (A₁→A₂ y) ∥) →
  A₁ /ᴱ R₁ → A₂ /ᴱ R₂
_/ᴱ-map-∥∥_ {R₁ = R₁} {R₂ = R₂} A₁→A₂ R₁→R₂ = rec λ where
  .[]ʳ                                   → [_] ∘ A₁→A₂
  .is-setʳ                               → /ᴱ-is-set
  .[]-respects-relationʳ {x = x} {y = y} →
     R₁ x y                      ↝⟨ ∣_∣ ⟩
     ∥ R₁ x y ∥                  ↝⟨ R₁→R₂ _ _ ⟩
     ∥ R₂ (A₁→A₂ x) (A₁→A₂ y) ∥  ↝⟨ PT.rec /ᴱ-is-set []-respects-relation ⟩□
     [ A₁→A₂ x ] ≡ [ A₁→A₂ y ]   □

_/ᴱ-map_ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁→A₂ : A₁ → A₂) →
  @0 (∀ x y → R₁ x y → R₂ (A₁→A₂ x) (A₁→A₂ y)) →
  A₁ /ᴱ R₁ → A₂ /ᴱ R₂
A₁→A₂ /ᴱ-map R₁→R₂ = A₁→A₂ /ᴱ-map-∥∥ λ x y → PT.∥∥-map (R₁→R₂ x y)

-- Two preservation lemmas for logical equivalences.

/ᴱ-cong-∥∥-⇔ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁⇔A₂ : A₁ ⇔ A₂) →
  @0 (∀ x y → ∥ R₁ x y ∥ → ∥ R₂ (_⇔_.to   A₁⇔A₂ x) (_⇔_.to   A₁⇔A₂ y) ∥) →
  @0 (∀ x y → ∥ R₂ x y ∥ → ∥ R₁ (_⇔_.from A₁⇔A₂ x) (_⇔_.from A₁⇔A₂ y) ∥) →
  A₁ /ᴱ R₁ ⇔ A₂ /ᴱ R₂
/ᴱ-cong-∥∥-⇔ A₁⇔A₂ R₁→R₂ R₂→R₁ = record
  { to   = _⇔_.to   A₁⇔A₂ /ᴱ-map-∥∥ R₁→R₂
  ; from = _⇔_.from A₁⇔A₂ /ᴱ-map-∥∥ R₂→R₁
  }

/ᴱ-cong-⇔ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁⇔A₂ : A₁ ⇔ A₂) →
  @0 (∀ x y → R₁ x y → R₂ (_⇔_.to   A₁⇔A₂ x) (_⇔_.to   A₁⇔A₂ y)) →
  @0 (∀ x y → R₂ x y → R₁ (_⇔_.from A₁⇔A₂ x) (_⇔_.from A₁⇔A₂ y)) →
  A₁ /ᴱ R₁ ⇔ A₂ /ᴱ R₂
/ᴱ-cong-⇔ A₁⇔A₂ R₁→R₂ R₂→R₁ =
  /ᴱ-cong-∥∥-⇔ A₁⇔A₂ (λ x y → PT.∥∥-map (R₁→R₂ x y))
                     (λ x y → PT.∥∥-map (R₂→R₁ x y))

-- Two preservation lemmas for split surjections.

infix 5 _/ᴱ-cong-∥∥-↠_ _/ᴱ-cong-↠_

_/ᴱ-cong-∥∥-↠_ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁↠A₂ : A₁ ↠ A₂) →
  @0 (∀ x y → ∥ R₁ x y ∥ ⇔ ∥ R₂ (_↠_.to A₁↠A₂ x) (_↠_.to A₁↠A₂ y) ∥) →
  A₁ /ᴱ R₁ ↠ A₂ /ᴱ R₂
_/ᴱ-cong-∥∥-↠_ {R₁ = R₁} {R₂ = R₂} A₁↠A₂ R₁⇔R₂ = record
  { logical-equivalence = /ᴱ-cong-∥∥-⇔
      (_↠_.logical-equivalence A₁↠A₂)
      (λ x y → _⇔_.to (R₁⇔R₂ x y))
      (λ x y → ∥ R₂ x y ∥                          ↝⟨ ≡⇒↝ _ (sym $ cong₂ (λ x y → ∥ R₂ x y ∥) (right-inverse-of x) (right-inverse-of y)) ⟩
               ∥ R₂ (to (from x)) (to (from y)) ∥  ↝⟨ _⇔_.from (R₁⇔R₂ _ _) ⟩□
               ∥ R₁ (from x) (from y) ∥            □)
  ; right-inverse-of = elim-prop λ where
      .[]ʳ x →
        [ to (from x) ]  ≡⟨ cong [_] $ right-inverse-of x ⟩∎
        [ x ]            ∎
      .is-propositionʳ _ → /ᴱ-is-set
  }
  where
  open _↠_ A₁↠A₂

_/ᴱ-cong-↠_ :
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁↠A₂ : A₁ ↠ A₂) →
  @0 (∀ x y → R₁ x y ⇔ R₂ (_↠_.to A₁↠A₂ x) (_↠_.to A₁↠A₂ y)) →
  A₁ /ᴱ R₁ ↠ A₂ /ᴱ R₂
A₁↠A₂ /ᴱ-cong-↠ R₁⇔R₂ =
  A₁↠A₂ /ᴱ-cong-∥∥-↠ λ x y → PT.∥∥-cong-⇔ (R₁⇔R₂ x y)

-- Two preservation lemmas for isomorphisms.

infix 5 _/ᴱ-cong-∥∥_ _/ᴱ-cong_

_/ᴱ-cong-∥∥_ :
  {A₁ : Type a₁} {A₂ : Type a₂}
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁↔A₂ : A₁ ↔[ k ] A₂) →
  @0 (∀ x y →
        ∥ R₁ x y ∥ ⇔
        ∥ R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y) ∥) →
  A₁ /ᴱ R₁ ↔[ k ] A₂ /ᴱ R₂
_/ᴱ-cong-∥∥_ {k = k} {R₁ = R₁} {R₂ = R₂} A₁↔A₂′ R₁⇔R₂ =
  from-bijection (record
    { surjection = from-isomorphism A₁↔A₂ /ᴱ-cong-∥∥-↠ λ x y →
        ∥ R₁ x y ∥                                                  ↝⟨ R₁⇔R₂ x y ⟩
        ∥ R₂ (to-implication A₁↔A₂′ x) (to-implication A₁↔A₂′ y) ∥  ↝⟨ ≡⇒↝ _ $ cong₂ (λ f g → ∥ R₂ (f x) (g y) ∥)
                                                                                (to-implication∘from-isomorphism k bijection)
                                                                                (to-implication∘from-isomorphism k bijection) ⟩□
        ∥ R₂ (to x) (to y) ∥                                        □
    ; left-inverse-of = elim-prop λ where
        .[]ʳ x →
          [ from (to x) ]  ≡⟨ cong [_] $ left-inverse-of x ⟩∎
          [ x ]            ∎
        .is-propositionʳ _ → /ᴱ-is-set
    })
  where
  A₁↔A₂ = from-isomorphism A₁↔A₂′

  open _↔_ A₁↔A₂

_/ᴱ-cong_ :
  {A₁ : Type a₁} {A₂ : Type a₂}
  {@0 R₁ : A₁ → A₁ → Type r₁}
  {@0 R₂ : A₂ → A₂ → Type r₂} →
  (A₁↔A₂ : A₁ ↔[ k ] A₂) →
  @0 (∀ x y →
        R₁ x y ⇔ R₂ (to-implication A₁↔A₂ x) (to-implication A₁↔A₂ y)) →
  A₁ /ᴱ R₁ ↔[ k ] A₂ /ᴱ R₂
_/ᴱ-cong_ A₁↔A₂ R₁⇔R₂ =
  A₁↔A₂ /ᴱ-cong-∥∥ λ x y → PT.∥∥-cong-⇔ (R₁⇔R₂ x y)

------------------------------------------------------------------------
-- Some properties

-- [_] is surjective with erased proofs.

Surjectiveᴱ-[] : Surjectiveᴱ ([_] {R = R})
Surjectiveᴱ-[] = elim-prop λ where
  .[]ʳ x             → ∣ x , [ refl _ ] ∣
  .is-propositionʳ _ → PTᴱ.truncation-is-proposition

-- Quotienting by the propositional truncation of a relation is
-- equivalent to quotienting by the relation itself.

/ᴱ-∥∥≃/ᴱ : A /ᴱ (λ x y → ∥ R x y ∥) ≃ A /ᴱ R
/ᴱ-∥∥≃/ᴱ {R = R} = F.id /ᴱ-cong-∥∥ λ x y →
  ∥ ∥ R x y ∥ ∥  ↔⟨ PT.flatten ⟩□
  ∥ R x y ∥      □

-- If R is an equivalence relation, then A /ᴱ R is weakly effective
-- (where this is expressed using ∥_∥ᴱ).
--
-- This proof is based on that of Proposition 2 in "Quotienting the
-- Delay Monad by Weak Bisimilarity" by Chapman, Uustalu and Veltri.

weakly-effective :
  {R : A → A → Type r} →
  @0 Is-equivalence-relation R →
  ∥ R x x ∥ᴱ →
  _≡_ {A = A /ᴱ R} [ x ] [ y ] → ∥ R x y ∥ᴱ
weakly-effective
  {A = A} {r = r} {x = x} {y = y} {R = R} eq ∥Rxx∥ᴱ [x]≡[y] =
                     $⟨ ∥Rxx∥ᴱ ⟩
  R′ x [ x ] .proj₁  ↝⟨ ≡⇒→ (cong (λ y → R′ x y .proj₁) [x]≡[y]) ⟩
  R′ x [ y ] .proj₁  ↔⟨⟩
  ∥ R x y ∥ᴱ         □
  where
  R′ : A → A /ᴱ R → ∃ λ (P : Type r) → Erased (Is-proposition P)
  R′ x = rec λ where
    .[]ʳ y → ∥ R x y ∥ᴱ , [ PTᴱ.truncation-is-proposition ]

    .is-setʳ →                                               $⟨ (λ {_ _} → Is-set-∃-Is-proposition ext U.prop-ext) ⟩
      Is-set (Proposition r)                                 ↝⟨ H-level-cong _ 2
                                                                  (∃-cong λ _ → inverse $ Er.Erased↔ .Er.erased)
                                                                  ⦂ (_ → _) ⟩□
      Is-set (∃ λ (P : Type r) → Erased (Is-proposition P))  □

    .[]-respects-relationʳ {x = y} {y = z} →
      R y z                                        ↝⟨ (λ r → record
                                                         { to   = flip (eq .Is-equivalence-relation.transitive) r
                                                         ; from = flip (eq .Is-equivalence-relation.transitive)
                                                                    (eq .Is-equivalence-relation.symmetric r)
                                                         }) ⟩
      R x y ⇔ R x z                                ↝⟨ EEq._≃ᴱ_.logical-equivalence ∘ PTᴱ.∥∥ᴱ-cong-⇔ ⟩
      ∥ R x y ∥ᴱ ⇔ ∥ R x z ∥ᴱ                      ↔⟨ ⇔↔≡″ ext U.prop-ext ⟩
      (∥ R x y ∥ᴱ , _) ≡ (∥ R x z ∥ᴱ , _)          ↝⟨ cong (Σ-map id Er.[_]→) ⟩□
      (∥ R x y ∥ᴱ , [ _ ]) ≡ (∥ R x z ∥ᴱ , [ _ ])  □

-- If R is an equivalence relation, and R is propositional (for x
-- and y), then A /ᴱ R is effective (for x and y).

effective :
  @0 Is-equivalence-relation R →
  @0 Is-proposition (R x y) →
  R x x →
  _≡_ {A = A /ᴱ R} [ x ] [ y ] → R x y
effective {R = R} {x = x} {y = y} eq prop Rxx =
  [ x ] ≡ [ y ]  ↝⟨ weakly-effective eq ∣ Rxx ∣ ⟩
  ∥ R x y ∥ᴱ     ↔⟨ PTᴱ.∥∥ᴱ↔ prop ⟩□
  R x y          □

-- If R is an equivalence relation, and R is propositional (for x
-- and y), then R x y is equivalent to equality of x and y under [_]
-- (in erased contexts).

@0 related≃[equal] :
  Is-equivalence-relation R →
  Is-proposition (R x y) →
  R x y ≃ _≡_ {A = A /ᴱ R} [ x ] [ y ]
related≃[equal] eq prop =
  Eq.⇔→≃
    prop
    /ᴱ-is-set
    []-respects-relation
    (effective eq prop (eq .Is-equivalence-relation.reflexive))

-- If R is an equivalence relation, then ∥ R x y ∥ is equivalent to
-- equality of x and y under [_] (in erased contexts).

@0 ∥related∥≃[equal] :
  Is-equivalence-relation R →
  ∥ R x y ∥ ≃ _≡_ {A = A /ᴱ R} [ x ] [ y ]
∥related∥≃[equal] {R = R} {x = x} {y = y} eq =
  ∥ R x y ∥      ↝⟨ inverse PT.∥∥ᴱ≃∥∥ ⟩
  ∥ R x y ∥ᴱ     ↝⟨ Eq.⇔→≃
                      PTᴱ.truncation-is-proposition
                      /ᴱ-is-set
                      (PTᴱ.rec λ @0 where
                         .PTᴱ.truncation-is-propositionʳ → /ᴱ-is-set
                         .PTᴱ.∣∣ʳ                        →
                           []-respects-relation)
                      (weakly-effective eq ∣ eq .Is-equivalence-relation.reflexive ∣) ⟩□
  [ x ] ≡ [ y ]  □

-- Quotienting with equality (for a set) amounts to the same thing as
-- not quotienting at all.

/ᴱ≡↔ : @0 Is-set A → A /ᴱ _≡_ ↔ A
/ᴱ≡↔ A-set = record
  { surjection = record
    { logical-equivalence = record
      { from = [_]
      ; to   = rec λ where
          .[]ʳ                   → id
          .[]-respects-relationʳ → id
          .is-setʳ               → A-set
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ _             → refl _
      .is-propositionʳ _ → /ᴱ-is-set
  }

-- Quotienting with a trivial relation amounts to the same thing as
-- using the propositional truncation (with erased proofs).

/ᴱtrivial↔∥∥ᴱ : @0 (∀ x y → R x y) → A /ᴱ R ↔ ∥ A ∥ᴱ
/ᴱtrivial↔∥∥ᴱ {A = A} {R = R} trivial = record
  { surjection = record
    { logical-equivalence = record
      { to = rec-prop λ where
          .[]ʳ             → ∣_∣
          .is-propositionʳ → PTᴱ.truncation-is-proposition
      ; from = PTᴱ.rec λ where
          .PTᴱ.∣∣ʳ                        → [_]
          .PTᴱ.truncation-is-propositionʳ → elim-prop λ @0 where
            .is-propositionʳ _ →
              Π-closure ext 1 λ _ →
              /ᴱ-is-set
            .[]ʳ x → elim-prop λ @0 where
              .is-propositionʳ _ → /ᴱ-is-set
              .[]ʳ y             → []-respects-relation (trivial x y)
      }
    ; right-inverse-of = PTᴱ.elim λ where
        .PTᴱ.∣∣ʳ _                        → refl _
        .PTᴱ.truncation-is-propositionʳ _ →
          ⇒≡ 1 PTᴱ.truncation-is-proposition
    }
  ; left-inverse-of = elim-prop λ where
      .[]ʳ _             → refl _
      .is-propositionʳ _ → /ᴱ-is-set
  }

------------------------------------------------------------------------
-- A property related to ∥_∥ᴱ, proved using _/ᴱ_

-- Having a constant function (with an erased proof of constancy) into
-- a set is equivalent to having a function from a propositionally
-- truncated type (with erased proofs) into the set.
--
-- The statement of this result is adapted from that of
-- Proposition 2.2 in "The General Universal Property of the
-- Propositional Truncation" by Kraus.

Σ→Erased-Constant≃∥∥ᴱ→ :
  @0 Is-set B →
  (∃ λ (f : A → B) → Erased (Constant f)) ≃ (∥ A ∥ᴱ → B)
Σ→Erased-Constant≃∥∥ᴱ→ {B = B} {A = A} B-set =
  (∃ λ (f : A → B) → Erased (Constant f))  ↔⟨ lemma ⟩
  (A /ᴱ (λ _ _ → ⊤) → B)                   ↝⟨ →-cong₁ ext (/ᴱtrivial↔∥∥ᴱ _) ⟩□
  (∥ A ∥ᴱ → B)                             □
  where
  lemma : _ ↔ _
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ (f , [ c ]) → rec λ where
                   .[]ʳ                     → f
                   .[]-respects-relationʳ _ → c _ _
                   .is-setʳ                 → B-set
        ; from = λ f → (f ∘ [_])
                     , [ (λ _ _ → cong f ([]-respects-relation _)) ]
        }
      ; right-inverse-of = λ f → ⟨ext⟩ $ elim λ where
          .[]ʳ _                   → refl _
          .[]-respects-relationʳ _ → B-set _ _
          .is-setʳ _               → mono₁ 2 B-set
      }
    ; left-inverse-of = λ _ → Σ-≡,≡→≡
        (refl _)
        (Er.H-level-Erased 1
           (Π-closure ext 1 λ _ →
            Π-closure ext 1 λ _ →
            B-set)
           _ _)
    }

-- The two directions of the proposition above compute in the
-- "right" way.

_ :
  (@0 B-set : Is-set B) →
  _≃_.to (Σ→Erased-Constant≃∥∥ᴱ→ B-set) f ∣ x ∣ ≡ proj₁ f x
_ = λ _ → refl _

_ :
  (@0 B-set : Is-set B) →
  proj₁ (_≃_.from (Σ→Erased-Constant≃∥∥ᴱ→ B-set) f) x ≡ f ∣ x ∣
_ = λ _ → refl _

------------------------------------------------------------------------
-- Various type formers commute with quotients

-- _⊎_ commutes with quotients.

⊎/ᴱ :
  {@0 R₁ : A₁ → A₁ → Type r} {@0 R₂ : A₂ → A₂ → Type r} →
  (A₁ ⊎ A₂) /ᴱ (R₁ ⊎ᴾ R₂) ≃ (A₁ /ᴱ R₁ ⊎ A₂ /ᴱ R₂)
⊎/ᴱ = Eq.↔→≃
  (rec λ where
     .[]ʳ → ⊎-map [_] [_]

     .is-setʳ → ⊎-closure 0 /ᴱ-is-set /ᴱ-is-set

     .[]-respects-relationʳ {x = inj₁ _} {y = inj₁ _} →
       cong inj₁ ∘ []-respects-relation
     .[]-respects-relationʳ {x = inj₂ _} {y = inj₂ _} →
       cong inj₂ ∘ []-respects-relation)
  Prelude.[ rec (λ where
              .[]ʳ x                 → [ inj₁ x ]
              .[]-respects-relationʳ → []-respects-relation
              .is-setʳ               → /ᴱ-is-set)
          , rec (λ where
              .[]ʳ x                 → [ inj₂ x ]
              .[]-respects-relationʳ → []-respects-relation
              .is-setʳ               → /ᴱ-is-set)
          ]
  Prelude.[ elim-prop (λ where
              .[]ʳ _             → refl _
              .is-propositionʳ _ → ⊎-closure 0 /ᴱ-is-set /ᴱ-is-set)
          , elim-prop (λ where
              .[]ʳ _             → refl _
              .is-propositionʳ _ → ⊎-closure 0 /ᴱ-is-set /ᴱ-is-set)
          ]
  (elim-prop λ where
     .[]ʳ               → Prelude.[ (λ _ → refl _) , (λ _ → refl _) ]
     .is-propositionʳ _ → /ᴱ-is-set)

-- Maybe commutes with quotients.
--
-- Chapman, Uustalu and Veltri mention a similar result in
-- "Quotienting the Delay Monad by Weak Bisimilarity".

Maybe/ᴱ :
  {@0 R : A → A → Type r} →
  Maybe A /ᴱ Maybeᴾ R ≃ Maybe (A /ᴱ R)
Maybe/ᴱ {A = A} {R = R} =
  Maybe A /ᴱ Maybeᴾ R    ↝⟨ ⊎/ᴱ ⟩
  ⊤ /ᴱ Trivial ⊎ A /ᴱ R  ↔⟨ /ᴱtrivial↔∥∥ᴱ _ ⊎-cong F.id ⟩
  ∥ ⊤ ∥ᴱ ⊎ A /ᴱ R        ↔⟨ PTᴱ.∥∥ᴱ↔ (mono₁ 0 ⊤-contractible) ⊎-cong F.id ⟩□
  Maybe (A /ᴱ R)         □

-- A simplification lemma for Maybe/-comm.

Maybe/ᴱ-[] :
  {@0 R : A → A → Type r} →
  _≃_.to (Maybe/ᴱ {R = R}) ∘ [_] ≡ ⊎-map id ([_] {R = R})
Maybe/ᴱ-[] = ⟨ext⟩ λ x →
  _≃_.to Maybe/ᴱ [ x ]                       ≡⟨⟩
  ⊎-map _ id (⊎-map _ id (⊎-map [_] [_] x))  ≡⟨ sym $ ⊎-map-∘ (⊎-map [_] [_] x) ⟩
  ⊎-map _ id (⊎-map [_] [_] x)               ≡⟨ sym $ ⊎-map-∘ x ⟩∎
  ⊎-map id [_] x                             ∎

-- Cartesian products commute with quotients, assuming that the two
-- binary relations involved in the statement are reflexive.

×/ᴱ :
  {@0 R₁ : A₁ → A₁ → Type r₁} {@0 R₂ : A₂ → A₂ → Type r₂} →
  @0 (∀ {x} → R₁ x x) →
  @0 (∀ {x} → R₂ x x) →
  (A₁ × A₂) /ᴱ (R₁ ×ᴾ R₂) ≃ (A₁ /ᴱ R₁ × A₂ /ᴱ R₂)
×/ᴱ {R₁ = R₁} {R₂ = R₂} R₁-refl R₂-refl = Eq.↔→≃
  (rec λ where
     .is-setʳ → ×-closure 2 /ᴱ-is-set /ᴱ-is-set

     .[]ʳ → Σ-map [_] [_]

     .[]-respects-relationʳ {x = x₁ , x₂} {y = y₁ , y₂} →
       R₁ x₁ y₁ × R₂ x₂ y₂                    ↝⟨ Σ-map []-respects-relation
                                                       []-respects-relation ⟩
       [ x₁ ] ≡ [ y₁ ] × [ x₂ ] ≡ [ y₂ ]      ↝⟨ uncurry (cong₂ _,_) ⟩□
       ([ x₁ ] , [ x₂ ]) ≡ ([ y₁ ] , [ y₂ ])  □)
  (uncurry $ rec λ where
     .is-setʳ →
       Π-closure ext 2 λ _ →
       /ᴱ-is-set
     .[]ʳ x → (x ,_) /ᴱ-map λ y₁ y₂ →
       R₂ y₁ y₂           ↝⟨ R₁-refl ,_ ⟩□
       R₁ x x × R₂ y₁ y₂  □
     .[]-respects-relationʳ {x = x₁} {y = x₂} R₁x₁x₂ →
       ⟨ext⟩ $ elim-prop λ @0 where
         .is-propositionʳ _ →
           /ᴱ-is-set
         .[]ʳ y →
           [ (x₁ , y) ]  ≡⟨ []-respects-relation (R₁x₁x₂ , R₂-refl) ⟩∎
           [ (x₂ , y) ]  ∎)
  (uncurry $ elim-prop λ where
     .is-propositionʳ _ →
       Π-closure ext 1 λ _ →
       ×-closure 2 /ᴱ-is-set /ᴱ-is-set
     .[]ʳ _ → elim-prop λ where
       .is-propositionʳ _ →
         ×-closure 2 /ᴱ-is-set /ᴱ-is-set
       .[]ʳ _ →
         refl _)
  (elim-prop λ where
     .is-propositionʳ _ → /ᴱ-is-set
     .[]ʳ _             → refl _)

-- The sigma type former commutes (kind of) with quotients, assuming
-- that the second projections come from propositional types.

Σ/ᴱ :
  @0 (∀ {x} → Is-proposition (P x)) →
  Σ (A /ᴱ R) P ≃ Σ A (P ∘ [_]) /ᴱ (R on proj₁)
Σ/ᴱ {A = A} {R = R} {P = P} prop = Eq.↔→≃
  (uncurry $ elim λ where
     .is-setʳ _ →
       Π-closure ext 2 λ _ →
       /ᴱ-is-set

     .[]ʳ → curry [_]

     .[]-respects-relationʳ {x = x} {y = y} r → ⟨ext⟩ λ P[y] →
       subst (λ x → P x → Σ A (P ∘ [_]) /ᴱ (R on proj₁))
             ([]-respects-relation r)
             (curry [_] x) P[y]                               ≡⟨ subst-→-domain P {f = curry [_] x} ([]-respects-relation r) ⟩

       [ (x , subst P (sym $ []-respects-relation r) P[y]) ]  ≡⟨ []-respects-relation r ⟩∎

       [ (y , P[y]) ]                                         ∎)
  (rec λ where
     .is-setʳ → Σ-closure 2 /ᴱ-is-set (λ _ → mono₁ 1 prop)

     .[]ʳ → Σ-map [_] id

     .[]-respects-relationʳ {x = (x₁ , x₂)} {y = (y₁ , y₂)} →
       R x₁ y₁                        ↝⟨ []-respects-relation ⟩
       [ x₁ ] ≡ [ y₁ ]                ↔⟨ ignore-propositional-component prop ⟩
       ([ x₁ ] , x₂) ≡ ([ y₁ ] , y₂)  □)
  (elim-prop λ where
     .[]ʳ _             → refl _
     .is-propositionʳ _ → /ᴱ-is-set)
  (uncurry $ elim-prop λ where
     .[]ʳ _ _           → refl _
     .is-propositionʳ _ →
       Π-closure ext 1 λ _ →
       Σ-closure 2 /ᴱ-is-set (λ _ → mono₁ 1 prop))

-- Erased commutes with quotients if certain conditions hold.

Erased/ᴱ :
  {@0 A : Type a} {@0 R : A → A → Type r} →
  @0 Is-set A →
  @0 (∀ {x y} → R x y → x ≡ y) →
  Erased A /ᴱ Erasedᴾ R ≃ Erased (A /ᴱ R)
Erased/ᴱ {A = A} {R = R} set R→≡ = Eq.↔→≃
  (rec λ where
     .is-setʳ                       → Er.H-level-Erased 2 /ᴱ-is-set
     .[]ʳ                           → Er.map [_]
     .[]-respects-relationʳ [ Rxy ] →
       Er.[]-cong [ []-respects-relation Rxy ])
  (λ ([ x ]) → [ [ from′ x ] ])
  (λ ([ x ]) →
     Er.[]-cong
       [ flip (elim-prop {P = λ x → [ from′ x ] ≡ x}) x (λ @0 where
           .is-propositionʳ _ → /ᴱ-is-set
           .[]ʳ _             → refl _)
       ])
  (elim-prop λ where
     .is-propositionʳ _ → /ᴱ-is-set
     .[]ʳ _             → refl _)
  where
  @0 from′ : A /ᴱ R → A
  from′ = rec λ @0 where
    .is-setʳ               → set
    .[]ʳ                   → id
    .[]-respects-relationʳ → R→≡

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

-- WORKS
macro
  idT : Term → Term → TC ⊤
  idT = unify

-- FAILS
macro
  test = unify

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2013-11-23
-- postulates are now alsow allowed in old-style mutual blocks

open import Common.Prelude

mutual
  even : Nat → Bool
  even zero    = true
  even (suc n) = odd n

  postulate
    odd : Nat → Bool

-- Error WAS: Postulates are not allowed in mutual blocks


text:
module Preduploid.Functor where

open import Preduploid

open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

open import Level

private
  variable p q r s : Polarity

record Functor {o₁ ℓ₁ o₂ ℓ₂} (𝒞 : Preduploid o₁ ℓ₁) (𝒟 : Preduploid o₂ ℓ₂)
  : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
  private
    module 𝒞 = Preduploid.Preduploid 𝒞
    module 𝒟 = Preduploid.Preduploid 𝒟

  open 𝒟

  field
    F₀ : 𝒞.Ob p -> Ob p
    F₁ : forall {A : 𝒞.Ob p} {B : 𝒞.Ob q} -> A 𝒞.⇒ B -> F₀ A ⇒ F₀ B

    identity : forall {A : 𝒞.Ob p} -> F₁ 𝒞.id ≡ id {A = F₀ A}
    homomorphism : forall {A : 𝒞.Ob p} {B : 𝒞.Ob q} {C : 𝒞.Ob r} {f : A 𝒞.⇒ B} {g : B 𝒞.⇒ C}
      -> F₁ (g 𝒞.⊙ f) ≡ F₁ g ⊙ F₁ f

max_stars_repo_name: elpinal/duploids

max_issues_repo_name: elpinal/duploids

max_forks_repo_name: elpinal/duploids


text:
open import Prelude
open import Algebra
open import Algebra.Monus

module Codata.Segments
  {ℓ}
  (mon : CTMAPOM ℓ)
  where

open CTMAPOM mon

private variable i j : 𝑆

-- This is a type which contains some finite and some infinite lists.
-- The idea is that each entry contains a parameter (w) which says
-- how much coinductive "fuel" it uses.
-- The Colist′ A i type represents a colist which is defined down to depth
-- i; the Colist A type represents a "true" colist, i.e. a colist defined for
-- any given depth.
infixr 5 _◃_
data Colist′ {a} (A : Type a) (i : 𝑆) : Type (a ℓ⊔ ℓ) where
  _◃_ : ∀ w → -- Segment size
          (  (w<i : w < i) → -- If there is enough fuel left (i is the fuel)
                             -- (also the _<_ type is a proposition)
             A × Colist′ A (i ∸ w) -- Produce an element followed by the rest of
                                   -- the list, with w taken out of the fuel.
             ) →
          Colist′ A i

Colist : Type a → Type (a ℓ⊔ ℓ)
Colist A = ∀ {i} → Colist′ A i

-- The main interesting things tyhis type can do are the following:
-- * Infinite lists.
-- * The "fuel" parameter can be an arbitrary monoid, not just ℕ
-- * Finite lists can also be specified, and the way we say something is
--   finite is by taking no fuel.
-- * Everything seems to correspond correctly to the monus axioms.

--------------------------------------------------------------------------------
-- Finite colists
--------------------------------------------------------------------------------

-- By adding a finite prefix you don't have to use any of the fuel.

_∹_ : A → Colist A → Colist A
x ∹ xs = ε ◃ λ _ → x , xs

--------------------------------------------------------------------------------
-- Empty colists
--------------------------------------------------------------------------------

-- To terminate computation you use all the fuel, making an empty list.
-- (I'm not sure how principled this is: semantically I don't know if I like
-- that the size of a segment can depend on the supplied size parameter).
empty : Colist A
empty {i = i} = i ◃ λ i<i → ⊥-elim (irrefl i<i)

--------------------------------------------------------------------------------
-- Finite derived colists
--------------------------------------------------------------------------------

-- singleton
pure : A → Colist A
pure x = x ∹ empty

replicate : ℕ → A → Colist A
replicate zero    x = empty
replicate (suc n) x = x ∹ replicate n x

--------------------------------------------------------------------------------
-- Infinite colists
--------------------------------------------------------------------------------

-- This unfold function produces an infinite list; it needs every size segment
-- be non empty so that each step uses some fuel. This is what provides the
-- termination argument.

module _
    (B : 𝑆 → Type b) -- The seed type
    (ϕ : ∀ {i} → -- At depth i
           B i → -- With this seed
           ∃ w × -- Produce a segment of size w
           (w ≢ ε) × -- w can't be ε, so that we use some of the fuel to prove
                     -- termination
           ((w<i : w < i) → A × B (i ∸ w)) -- And produce the cons constructor.
           )
    -- ^ The step function
    where
    unfold′ : Acc _<_ i → B i → Colist′ A i
    unfold′ a = uncurry _◃_
              ∘ map₂
                (λ { (w≢ε , xs′) w<i →
                       map₂ (case a of
                              λ { (acc wf) →
                                    unfold′ (wf _ (∸‿<-< _ _ w<i w≢ε)) })
                            (xs′ w<i) })
              ∘ ϕ

unfold : (fdc : WellFounded _<_)
         (B : 𝑆 → Type b)
         (ϕ : ∀ {i} → B i → ∃ w × (w ≢ ε) × ((w<i : w < i) → A × B (i ∸ w))) →
         (∀ {i} → B i) → Colist A
unfold fdc B ϕ xs {i} = unfold′ B ϕ (fdc i) xs

-- Here's a simple example using the unfold function: this produces infinitely
-- repeated values, with segment size s.
repeat : (fdc : WellFounded _<_) (s : 𝑆) (s≢ε : s ≢ ε) (x : A) → Colist A
repeat fdc s s≢ε x = unfold fdc (const ⊤) (λ _ → s , s≢ε , const (x , tt)) tt

--------------------------------------------------------------------------------
-- Manipulating colists
--------------------------------------------------------------------------------

-- One important thing to note about the Colist type: it is inductive!
-- Although it does technically represent "coinduction", the constructors and
-- type itself are inductive as far as Agda can see. For that reason functions
-- like map pass the termination checker with no extra ceremony.
map : (A → B) → Colist′ A i → Colist′ B i
map f (w ◃ xs) = w ◃ λ w<i → case xs w<i of λ { (y , ys) → f y , map f ys }

-- You can extract a finite prefix of the colist.
open import Data.List using (List; _∷_; [])

take′ : ∀ i → Colist′ A i → List A
take′ i (w ◃ xs) with w <? i
... | no _ = []
... | yes w<i with xs w<i
... | y , ys = y ∷ take′ _ ys

take : 𝑆 → Colist A → List A
take x xs = take′ x xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.DistributiveLattice
         {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
         where

open DistributiveLattice DL
import Algebra.Properties.Lattice
private
  open module L = Algebra.Properties.Lattice lattice public
    hiding (replace-equality)
open import Algebra.Structures
open import Algebra.FunctionProperties _≈_
open import Relation.Binary
open import Relation.Binary.Reasoning.Setoid setoid
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; module Equivalence)
open import Data.Product using (_,_)

∨-∧-distribˡ : _∨_ DistributesOverˡ _∧_
∨-∧-distribˡ x y z = begin
  x ∨ y ∧ z          ≈⟨ ∨-comm _ _ ⟩
  y ∧ z ∨ x          ≈⟨ ∨-∧-distribʳ _ _ _ ⟩
  (y ∨ x) ∧ (z ∨ x)  ≈⟨ ∨-comm _ _ ⟨ ∧-cong ⟩ ∨-comm _ _ ⟩
  (x ∨ y) ∧ (x ∨ z)  ∎

∨-∧-distrib : _∨_ DistributesOver _∧_
∨-∧-distrib = ∨-∧-distribˡ , ∨-∧-distribʳ

∧-∨-distribˡ : _∧_ DistributesOverˡ _∨_
∧-∨-distribˡ x y z = begin
  x ∧ (y ∨ z)                ≈⟨ ∧-congʳ $ sym (∧-absorbs-∨ _ _) ⟩
  (x ∧ (x ∨ y)) ∧ (y ∨ z)    ≈⟨ ∧-congʳ $ ∧-congˡ $ ∨-comm _ _ ⟩
  (x ∧ (y ∨ x)) ∧ (y ∨ z)    ≈⟨ ∧-assoc _ _ _ ⟩
  x ∧ ((y ∨ x) ∧ (y ∨ z))    ≈⟨ ∧-congˡ $ sym (∨-∧-distribˡ _ _ _) ⟩
  x ∧ (y ∨ x ∧ z)            ≈⟨ ∧-congʳ $ sym (∨-absorbs-∧ _ _) ⟩
  (x ∨ x ∧ z) ∧ (y ∨ x ∧ z)  ≈⟨ sym $ ∨-∧-distribʳ _ _ _ ⟩
  x ∧ y ∨ x ∧ z              ∎

∧-∨-distribʳ : _∧_ DistributesOverʳ _∨_
∧-∨-distribʳ x y z = begin
  (y ∨ z) ∧ x    ≈⟨ ∧-comm _ _ ⟩
  x ∧ (y ∨ z)    ≈⟨ ∧-∨-distribˡ _ _ _ ⟩
  x ∧ y ∨ x ∧ z  ≈⟨ ∧-comm _ _ ⟨ ∨-cong ⟩ ∧-comm _ _ ⟩
  y ∧ x ∨ z ∧ x  ∎

∧-∨-distrib : _∧_ DistributesOver _∨_
∧-∨-distrib = ∧-∨-distribˡ , ∧-∨-distribʳ

-- The dual construction is also a distributive lattice.

∧-∨-isDistributiveLattice : IsDistributiveLattice _≈_ _∧_ _∨_
∧-∨-isDistributiveLattice = record
  { isLattice    = ∧-∨-isLattice
  ; ∨-∧-distribʳ = ∧-∨-distribʳ
  }

∧-∨-distributiveLattice : DistributiveLattice _ _
∧-∨-distributiveLattice = record
  { _∧_                   = _∨_
  ; _∨_                   = _∧_
  ; isDistributiveLattice = ∧-∨-isDistributiveLattice
  }

-- One can replace the underlying equality with an equivalent one.

replace-equality :
  {_≈′_ : Rel Carrier dl₂} →
  (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) → DistributiveLattice _ _
replace-equality {_≈′_} ≈⇔≈′ = record
  { _≈_                   = _≈′_
  ; _∧_                   = _∧_
  ; _∨_                   = _∨_
  ; isDistributiveLattice = record
    { isLattice    = Lattice.isLattice (L.replace-equality ≈⇔≈′)
    ; ∨-∧-distribʳ = λ x y z → to ⟨$⟩ ∨-∧-distribʳ x y z
    }
  } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})


text:
-- Andreas, 2020-03-27, issue #3684
-- Warn about invalid fields instead of hard error.

module TooManyFields where

postulate X : Set

record D : Set where
  field x : X

d : X -> D
d x = record {x = x; y = x}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Logic{ℓ} where

-- open import Logic
-- open import Logic.Classical

-- Everything is computably decidable
-- instance postulate classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P)

Stmt : _
Stmt = Set(ℓ) -- Prop(ℓ)

open import Agda.Primitive public
  renaming (Setω to Stmtω)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Fin, and operations making use of these
-- properties (or other properties not available in Data.Fin)
------------------------------------------------------------------------

module Data.Fin.Properties where

open import Algebra
open import Data.Fin
open import Data.Nat as N
  using (ℕ; zero; suc; s≤s; z≤n; _∸_)
  renaming (_≤_ to _ℕ≤_; _<_ to _ℕ<_; _+_ to _ℕ+_)
import Data.Nat.Properties as N
open import Data.Product
open import Function
open import Function.Equality as FunS using (_⟨$⟩_)
open import Function.Injection using (_↣_)
open import Algebra.FunctionProperties
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; cong; subst)
open import Category.Functor
open import Category.Applicative

------------------------------------------------------------------------
-- Properties

private
  drop-suc : ∀ {o} {m n : Fin o} → Fin.suc m ≡ suc n → m ≡ n
  drop-suc refl = refl

preorder : ℕ → Preorder _ _ _
preorder n = P.preorder (Fin n)

setoid : ℕ → Setoid _ _
setoid n = P.setoid (Fin n)

strictTotalOrder : ℕ → StrictTotalOrder _ _ _
strictTotalOrder n = record
  { Carrier            = Fin n
  ; _≈_                = _≡_
  ; _<_                = _<_
  ; isStrictTotalOrder = record
    { isEquivalence = P.isEquivalence
    ; trans         = N.<-trans
    ; compare       = cmp
    ; <-resp-≈      = P.resp₂ _<_
    }
  }
  where
  cmp : ∀ {n} → Trichotomous _≡_ (_<_ {n})
  cmp zero    zero    = tri≈ (λ())     refl  (λ())
  cmp zero    (suc j) = tri< (s≤s z≤n) (λ()) (λ())
  cmp (suc i) zero    = tri> (λ())     (λ()) (s≤s z≤n)
  cmp (suc i) (suc j) with cmp i j
  ... | tri<  lt ¬eq ¬gt = tri< (s≤s lt)         (¬eq ∘ drop-suc) (¬gt ∘ N.≤-pred)
  ... | tri> ¬lt ¬eq  gt = tri> (¬lt ∘ N.≤-pred) (¬eq ∘ drop-suc) (s≤s gt)
  ... | tri≈ ¬lt  eq ¬gt = tri≈ (¬lt ∘ N.≤-pred) (cong suc eq)    (¬gt ∘ N.≤-pred)

decSetoid : ℕ → DecSetoid _ _
decSetoid n = StrictTotalOrder.decSetoid (strictTotalOrder n)

infix 4 _≟_

_≟_ : {n : ℕ} → Decidable {A = Fin n} _≡_
_≟_ {n} = DecSetoid._≟_ (decSetoid n)

to-from : ∀ n → toℕ (fromℕ n) ≡ n
to-from zero    = refl
to-from (suc n) = cong suc (to-from n)

toℕ-injective : ∀ {n} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
toℕ-injective {zero}  {}      {}      _
toℕ-injective {suc n} {zero}  {zero}  eq = refl
toℕ-injective {suc n} {zero}  {suc j} ()
toℕ-injective {suc n} {suc i} {zero}  ()
toℕ-injective {suc n} {suc i} {suc j} eq =
  cong suc (toℕ-injective (cong N.pred eq))

bounded : ∀ {n} (i : Fin n) → toℕ i ℕ< n
bounded zero    = s≤s z≤n
bounded (suc i) = s≤s (bounded i)

prop-toℕ-≤ : ∀ {n} (x : Fin n) → toℕ x ℕ≤ N.pred n
prop-toℕ-≤ zero                 = z≤n
prop-toℕ-≤ (suc {n = zero}  ())
prop-toℕ-≤ (suc {n = suc n} i)  = s≤s (prop-toℕ-≤ i)

nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ≤ n
nℕ-ℕi≤n n       zero     = begin n ∎
  where open N.≤-Reasoning
nℕ-ℕi≤n zero    (suc ())
nℕ-ℕi≤n (suc n) (suc i)  = begin
  n ℕ-ℕ i ≤⟨ nℕ-ℕi≤n n i ⟩
  n       ≤⟨ N.n≤1+n n ⟩
  suc n   ∎
  where open N.≤-Reasoning

inject-lemma : ∀ {n} {i : Fin n} (j : Fin′ i) →
               toℕ (inject j) ≡ toℕ j
inject-lemma {i = zero}  ()
inject-lemma {i = suc i} zero    = refl
inject-lemma {i = suc i} (suc j) = cong suc (inject-lemma j)

inject+-lemma : ∀ {m} n (i : Fin m) → toℕ i ≡ toℕ (inject+ n i)
inject+-lemma n zero    = refl
inject+-lemma n (suc i) = cong suc (inject+-lemma n i)

inject₁-lemma : ∀ {m} (i : Fin m) → toℕ (inject₁ i) ≡ toℕ i
inject₁-lemma zero    = refl
inject₁-lemma (suc i) = cong suc (inject₁-lemma i)

inject≤-lemma : ∀ {m n} (i : Fin m) (le : m ℕ≤ n) →
                toℕ (inject≤ i le) ≡ toℕ i
inject≤-lemma zero    (N.s≤s le) = refl
inject≤-lemma (suc i) (N.s≤s le) = cong suc (inject≤-lemma i le)

≺⇒<′ : _≺_ ⇒ N._<′_
≺⇒<′ (n ≻toℕ i) = N.≤⇒≤′ (bounded i)

<′⇒≺ : N._<′_ ⇒ _≺_
<′⇒≺ {n} N.≤′-refl    = subst (λ i → i ≺ suc n) (to-from n)
                              (suc n ≻toℕ fromℕ n)
<′⇒≺ (N.≤′-step m≤′n) with <′⇒≺ m≤′n
<′⇒≺ (N.≤′-step m≤′n) | n ≻toℕ i =
  subst (λ i → i ≺ suc n) (inject₁-lemma i) (suc n ≻toℕ (inject₁ i))

toℕ-raise : ∀ {m} n (i : Fin m) → toℕ (raise n i) ≡ n ℕ+ toℕ i
toℕ-raise zero    i = refl
toℕ-raise (suc n) i = cong suc (toℕ-raise n i)

fromℕ≤-toℕ : ∀ {m} (i : Fin m) (i<m : toℕ i ℕ< m) → fromℕ≤ i<m ≡ i
fromℕ≤-toℕ zero    (s≤s z≤n)       = refl
fromℕ≤-toℕ (suc i) (s≤s (s≤s m≤n)) = cong suc (fromℕ≤-toℕ i (s≤s m≤n))

toℕ-fromℕ≤ : ∀ {m n} (m<n : m ℕ< n) → toℕ (fromℕ≤ m<n) ≡ m
toℕ-fromℕ≤ (s≤s z≤n)       = refl
toℕ-fromℕ≤ (s≤s (s≤s m<n)) = cong suc (toℕ-fromℕ≤ (s≤s m<n))

------------------------------------------------------------------------
-- Operations

infixl 6 _+′_

_+′_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (N.pred m ℕ+ n)
i +′ j = inject≤ (i + j) (N._+-mono_ (prop-toℕ-≤ i) ≤-refl)
  where open DecTotalOrder N.decTotalOrder renaming (refl to ≤-refl)

-- reverse {n} "i" = "n ∸ 1 ∸ i".

reverse : ∀ {n} → Fin n → Fin n
reverse {zero}  ()
reverse {suc n} i  = inject≤ (n ℕ- i) (N.n∸m≤n (toℕ i) (suc n))

reverse-prop : ∀ {n} → (i : Fin n) → toℕ (reverse i) ≡ n ∸ suc (toℕ i)
reverse-prop {zero} ()
reverse-prop {suc n} i = begin
  toℕ (inject≤ (n ℕ- i) _)  ≡⟨ inject≤-lemma _ _ ⟩
  toℕ (n ℕ- i)              ≡⟨ toℕ‿ℕ- n i ⟩
  n ∸ toℕ i                 ∎
  where
  open P.≡-Reasoning

  toℕ‿ℕ- : ∀ n i → toℕ (n ℕ- i) ≡ n ∸ toℕ i
  toℕ‿ℕ- n       zero     = to-from n
  toℕ‿ℕ- zero    (suc ())
  toℕ‿ℕ- (suc n) (suc i)  = toℕ‿ℕ- n i

reverse-involutive : ∀ {n} → Involutive _≡_ reverse
reverse-involutive {n} i = toℕ-injective (begin
  toℕ (reverse (reverse i))  ≡⟨ reverse-prop _ ⟩
  n ∸ suc (toℕ (reverse i))  ≡⟨ eq ⟩
  toℕ i                      ∎)
  where
  open P.≡-Reasoning
  open CommutativeSemiring N.commutativeSemiring using (+-comm)

  lem₁ : ∀ m n → (m ℕ+ n) ∸ (m ℕ+ n ∸ m) ≡ m
  lem₁ m n = begin
    m ℕ+ n ∸ (m ℕ+ n ∸ m) ≡⟨ cong (λ ξ → m ℕ+ n ∸ (ξ ∸ m)) (+-comm m n) ⟩
    m ℕ+ n ∸ (n ℕ+ m ∸ m) ≡⟨ cong (λ ξ → m ℕ+ n ∸ ξ) (N.m+n∸n≡m n m) ⟩
    m ℕ+ n ∸ n            ≡⟨ N.m+n∸n≡m m n ⟩
    m                     ∎

  lem₂ : ∀ n → (i : Fin n) → n ∸ suc (n ∸ suc (toℕ i)) ≡ toℕ i
  lem₂ zero    ()
  lem₂ (suc n) i  = begin
    n ∸ (n ∸ toℕ i)                     ≡⟨ cong (λ ξ → ξ ∸ (ξ ∸ toℕ i)) i+j≡k ⟩
    (toℕ i ℕ+ j) ∸ (toℕ i ℕ+ j ∸ toℕ i) ≡⟨ lem₁ (toℕ i) j ⟩
    toℕ i                               ∎
    where
    decompose-n : ∃ λ j → n ≡ toℕ i ℕ+ j
    decompose-n = n ∸ toℕ i , P.sym (N.m+n∸m≡n (prop-toℕ-≤ i))

    j     = proj₁ decompose-n
    i+j≡k = proj₂ decompose-n

  eq : n ∸ suc (toℕ (reverse i)) ≡ toℕ i
  eq = begin
    n ∸ suc (toℕ (reverse i)) ≡⟨ cong (λ ξ → n ∸ suc ξ) (reverse-prop i) ⟩
    n ∸ suc (n ∸ suc (toℕ i)) ≡⟨ lem₂ n i ⟩
    toℕ i                     ∎

-- If there is an injection from a type to a finite set, then the type
-- has decidable equality.

eq? : ∀ {a n} {A : Set a} → A ↣ Fin n → Decidable {A = A} _≡_
eq? inj = Dec.via-injection inj _≟_

-- Quantification over finite sets commutes with applicative functors.

sequence : ∀ {F n} {P : Fin n → Set} → RawApplicative F →
           (∀ i → F (P i)) → F (∀ i → P i)
sequence {F} RA = helper _ _
  where
  open RawApplicative RA

  helper : ∀ n (P : Fin n → Set) → (∀ i → F (P i)) → F (∀ i → P i)
  helper zero    P ∀iPi = pure (λ())
  helper (suc n) P ∀iPi =
    combine <$> ∀iPi zero ⊛ helper n (λ n → P (suc n)) (∀iPi ∘ suc)
    where
    combine : P zero → (∀ i → P (suc i)) → ∀ i → P i
    combine z s zero    = z
    combine z s (suc i) = s i

private

  -- Included just to show that sequence above has an inverse (under
  -- an equivalence relation with two equivalence classes, one with
  -- all inhabited sets and the other with all uninhabited sets).

  sequence⁻¹ : ∀ {F}{A} {P : A → Set} → RawFunctor F →
               F (∀ i → P i) → ∀ i → F (P i)
  sequence⁻¹ RF F∀iPi i = (λ f → f i) <$> F∀iPi
    where open RawFunctor RF


text:
module container.m.level where

open import level
open import sum
open import equality.core
open import equality.calculus
open import function.core
open import function.isomorphism
open import function.extensionality
open import sets.unit
open import sets.nat.core
open import hott.level
open import hott.univalence
open import container.core
open import container.equality
open import container.fixpoint
open import container.m.core
open import container.m.extensionality

private
  module Properties {li la lb}
                    {c : Container li la lb}
                    (hA : ∀ i → contr (Container.A c i)) where
    open Definition c
    open Extensionality c
    open Fixpoint (fix M fixpoint)
      using (head; tail)

    module S where
      module local where
        open Equality c (fix M fixpoint)
          using (equality)
        open Definition equality public

      open Fixpoint (fix local.M local.fixpoint) public
        using (head; tail)
      open local public

    center : ∀ {i} → M i
    center {i} = inf (proj₁ (hA i)) λ _ → ♯ center

    contraction : ∀ {i} (x : M i) → center ≡ x
    contraction {i} x = mext (lem' x)
      where
        coalg : ∀ {i}{x y : M i}
              → center ≡ x
              → Σ (head x ≡ head y) λ p
              → ((b : B (head x)) → center ≡ tail x b)
        coalg {i}{y = y} refl
          = proj₂ (hA i) (head y)
          , λ b → refl

        lem' : ∀ {i}(x : M i) → center ≡M x
        lem' _ = S.unfold (λ _ → coalg) _ refl

    m-contr : ∀ i → contr (M i)
    m-contr i = center , contraction

-- Lemma 14 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
m-level : ∀ {n li la lb} {c : Container li la lb}
         → let open Definition c
         in ((i : I) → h n (A i))
         → (i : I) → h n (M i)
m-level {n = 0} hA i = Properties.m-contr hA i
m-level {n = suc n} {c = c} hA i = λ xs ys
  → retract-level mext mext-inv mext-retraction (ih xs ys)
  where
    open Definition c
    open Extensionality c
    open Fixpoint (fix M fixpoint)
      using (head; tail)

    ih : (xs ys : M i) → h n (xs ≡M ys)
    ih xs ys = m-level (λ { (i , xs , ys) → hA i (head xs) (head ys) })
                        (i , xs , ys)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
import      Lvl
open import Data.Boolean
open import Type

module Data.List.Sorting.InsertionSort {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

open import Data.List
import      Data.List.Functions as List
open import Data.List.Sorting.Functions(_≤?_)

insertion-sort : List(T) → List(T)
insertion-sort = List.foldᵣ insert ∅

module Proofs where
  open import Data.Boolean.Stmt
  open import Data.List.Relation.Permutation
  open import Data.List.Sorting(_≤?_)
  open import Data.List.Sorting.Proofs(_≤?_)
  open import Functional using (_∘₂_)
  open import Logic.Propositional
  open import Relator.Equals
  open import Structure.Relator.Properties
  open import Syntax.Transitivity

  module _ (asym : ∀{x y} → (x ≤? y ≡ not(y ≤? x))) where -- TODO: Use Structure.Relator.Properties.Asymmetry by the relation (IsTrue ∘₂ (_≤?_))
    instance
      insertion-sort-sorted-proof : ∀{l} → Sorted(insertion-sort l)
      insertion-sort-sorted-proof {∅}     = empty
      insertion-sort-sorted-proof {x ⊰ l} = insert-sorted-proof asym (insertion-sort-sorted-proof {l})

    insert-permutation-proof : ∀{x}{l} → ((insert x l) permutes (x ⊰ l))
    insert-permutation-proof {x} {∅} = prepend _permutes_.empty
    insert-permutation-proof {x} {a ⊰ l} with (x ≤? a)
    ... | 𝑇 = reflexivity(_permutes_)
    ... | 𝐹 =
      a ⊰ insert x l 🝖-[ _permutes_.prepend (insert-permutation-proof {x} {l}) ]
      a ⊰ x ⊰ l      🝖-[ _permutes_.swap ]
      x ⊰ a ⊰ l      🝖-end

    instance
      insertion-sort-permutation-proof : ∀{l} → ((insertion-sort l) permutes l)
      insertion-sort-permutation-proof {∅} = _permutes_.empty
      insertion-sort-permutation-proof {x ⊰ l} =
        insertion-sort (x ⊰ l) 🝖-[ insert-permutation-proof ]
        x ⊰ (insertion-sort l) 🝖-[ prepend (insertion-sort-permutation-proof {l}) ]
        x ⊰ l                  🝖-end

    instance
      insertion-sort-sorting-algorithm : SortingAlgorithm(insertion-sort)
      SortingAlgorithm.sorts    insertion-sort-sorting-algorithm {l} = insertion-sort-sorted-proof {l}
      SortingAlgorithm.permutes insertion-sort-sorting-algorithm     = insertion-sort-permutation-proof


text:
module Verifier where

open import ModusPonens using (modusPonens)

check : ∀ {P Q : Set} → (P → Q) → P → Q
check = modusPonens

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
{-# OPTIONS --cubical #-}
module Multidimensional.Data.DirNum.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty
open import Cubical.Data.Prod
open import Cubical.Data.Bool
open import Cubical.Data.Nat

open import Cubical.Relation.Nullary

open import Multidimensional.Data.Dir
open import Multidimensional.Data.DirNum.Base
open import Multidimensional.Data.Extra.Nat

double-lemma : ∀ {r} → (d : DirNum r) →
               doubleℕ (DirNum→ℕ d) ≡ DirNum→ℕ (doubleDirNum+ r d)
double-lemma {r} d = refl

¬↓,d≡↑,d′ : ∀ {n} → ∀ (d d′ : DirNum n) → ¬ (↓ , d) ≡ (↑ , d′)
¬↓,d≡↑,d′ {n} d d′ ↓,d≡↑,d′ = ¬↓≡↑ (cong proj₁ ↓,d≡↑,d′)

¬↑,d≡↓,d′ : ∀ {n} → ∀ (d d′ : DirNum n) → ¬ (↑ , d) ≡ (↓ , d′)
¬↑,d≡↓,d′ {n} d d′ ↑,d≡↓,d′ = ¬↑≡↓ (cong proj₁ ↑,d≡↓,d′)

-- dropping least significant bit preserves equality
-- TODO: this was copied over from Direction.agda ; redefine using DropLeast
dropLeast≡ : ∀ {n} → ∀ (ds ds′ : DirNum n) (d : Dir)
              → ((d , ds) ≡ (d , ds′)) → ds ≡ ds′
dropLeast≡ {n} ds ds′ d d,ds≡d,ds′ = cong proj₂ d,ds≡d,ds′

zero-n→0 : ∀ {r} → DirNum→ℕ (zero-n r) ≡ zero
zero-n→0 {zero} = refl
zero-n→0 {suc r} =
    doubleℕ (DirNum→ℕ (zero-n r))
  ≡⟨ cong doubleℕ (zero-n→0 {r}) ⟩
    doubleℕ zero
  ≡⟨ refl ⟩
    zero
  ∎

zero-n? : ∀ {n} → (x : DirNum n) → Dec (x ≡ zero-n n)
zero-n? {zero} tt = yes refl
zero-n? {suc n} (↓ , ds) with zero-n? ds
... | no ds≠zero-n = no (λ y →
                            ds≠zero-n (dropLeast≡ ds (zero-n n) ↓ y))
... | yes ds≡zero-n = yes (cong (λ y → (↓ , y)) ds≡zero-n)
zero-n? {suc n} (↑ , ds) = no ((¬↑,d≡↓,d′ ds (zero-n n)))

zero-n≡0 : {r : ℕ} → DirNum→ℕ (zero-n r) ≡ zero
zero-n≡0{zero} = refl
zero-n≡0 {suc r} =
    doubleℕ (DirNum→ℕ {r} (zero-n r))
  ≡⟨ cong doubleℕ (zero-n≡0 {r}) ⟩
   0
  ∎

-- x is doubleable as a DirNum precisely when x's most significant bit is 0
-- this should return a Dec
doubleable-n? : {n : ℕ} → (x : DirNum n) → Bool
doubleable-n? {zero} tt = false
doubleable-n? {suc n} (x , x₁) with zero-n? x₁
... | yes _ = true
... | no _ = doubleable-n? x₁

max→ℕ : (r : ℕ) → DirNum→ℕ (max-n r) ≡ predℕ (doublesℕ r 1)
max→ℕ zero = refl
max→ℕ (suc r) =
    suc (doubleℕ (DirNum→ℕ (max-n r)))
  ≡⟨ cong (λ z → suc (doubleℕ z)) (max→ℕ r) ⟩
    suc (doubleℕ (predℕ (doublesℕ r 1)))
  ≡⟨ cong suc (doublePred (doublesℕ r 1)) ⟩
    suc (predℕ (predℕ (doubleℕ (doublesℕ r 1))))
  ≡⟨ cong (λ z → suc (predℕ (predℕ z))) (doubleDoubles r 1) ⟩
    suc (predℕ (predℕ (doublesℕ (suc r) 1)))
  ≡⟨ refl ⟩
    suc (predℕ (predℕ (doublesℕ r 2)))
  ≡⟨ sucPred (predℕ (doublesℕ r 2)) H ⟩
    predℕ (doublesℕ r 2)
  ∎
  where
    G : (r : ℕ) → doubleℕ (doublesℕ r 1) ≡ doublesℕ r 2
    G zero = refl
    G (suc r) = doubleℕ (doublesℕ r 2) ≡⟨ doubleDoubles r 2 ⟩
                 doublesℕ (suc r) 2 ≡⟨ refl ⟩ doublesℕ r (doubleℕ 2) ∎
    H : ¬ predℕ (doublesℕ r 2) ≡ zero
    H = λ h → (predDoublePos (doublesℕ r 1) (doublesPos r 1 snotz)
        ((
          predℕ (doubleℕ (doublesℕ r 1)) ≡⟨ cong predℕ (G r) ⟩
          predℕ (doublesℕ r 2) ≡⟨ h ⟩
          0 ∎
         )))

max? : ∀ {n} → (x : DirNum n) → Dec (x ≡ max-n n)
max? {zero} tt = yes refl
max? {suc n} (↓ , ds) = no ((¬↓,d≡↑,d′ ds (max-n n)))
max? {suc n} (↑ , ds) with max? ds
... | yes ds≡max-n = yes (
          (↑ , ds)
        ≡⟨ cong (λ x → (↑ , x)) ds≡max-n ⟩
          (↑ , max-n n)
        ∎
      )
... | no ¬ds≡max-n = no (λ d,ds≡d,max-n →
                            ¬ds≡max-n ((dropLeast≡ ds (max-n n) ↑ d,ds≡d,max-n)))

maxn+1≡↑maxn : ∀ n → max-n (suc n) ≡ (↑ , (max-n n))
maxn+1≡↑maxn n = refl

maxr≡pred2ʳ : (r : ℕ) (d : DirNum r) →
           d ≡ max-n r → DirNum→ℕ d ≡ predℕ (doublesℕ r (suc zero))
maxr≡pred2ʳ zero d d≡max = refl
maxr≡pred2ʳ (suc r) (↓ , ds) d≡max = ⊥-elim ((¬↓,d≡↑,d′ ds (max-n r)) d≡max)
maxr≡pred2ʳ (suc r) (↑ , ds) d≡max =
     suc (doubleℕ (DirNum→ℕ ds))
   ≡⟨ cong (λ x → suc (doubleℕ x)) (maxr≡pred2ʳ r ds ds≡max) ⟩
     suc (doubleℕ (predℕ (doublesℕ r (suc zero)))) -- 2*(2^r - 1) + 1 = 2^r+1 - 1
   ≡⟨ cong suc (doublePred (doublesℕ r (suc zero))) ⟩
     suc (predℕ (predℕ (doubleℕ (doublesℕ r (suc zero)))))
   ≡⟨ sucPred (predℕ (doubleℕ (doublesℕ r (suc zero)))) (
              (predDoublePos (doublesℕ r (suc zero)) ((doublesPos r 1 snotz)))) ⟩
     predℕ (doubleℕ (doublesℕ r (suc zero)))
   ≡⟨ cong predℕ (doubleDoubles r (suc zero)) ⟩
     predℕ (doublesℕ (suc r) 1)
   ≡⟨ refl ⟩
     predℕ (doublesℕ r 2) -- 2^r*2 - 1 = 2^(r+1) - 1
   ∎
  where
    ds≡max : ds ≡ max-n r
    ds≡max = dropLeast≡ ds (max-n r) ↑ d≡max

-- TODO: rename?
nextsuc-lemma : (r : ℕ) (x : DirNum r) →
         ¬ ((sucDoubleDirNum+ r x) ≡ max-n (suc r)) → ¬ (x ≡ max-n r)
nextsuc-lemma zero tt ¬H = ⊥-elim (¬H refl)
nextsuc-lemma (suc r) (↓ , x) ¬H = ¬↓,d≡↑,d′ x (max-n r)
nextsuc-lemma (suc r) (↑ , x) ¬H =
  λ h → ¬H (H (dropLeast≡ x (max-n r) ↑ h)) --⊥-elim (¬H H)
  where
    H : (x ≡ max-n r) →
         sucDoubleDirNum+ (suc r) (↑ , x) ≡ (↑ , (↑ , max-n r))
    H x≡maxnr =
        sucDoubleDirNum+ (suc r) (↑ , x)
      ≡⟨ cong (λ y → sucDoubleDirNum+ (suc r) (↑ , y)) x≡maxnr ⟩
        sucDoubleDirNum+ (suc r) (↑ , max-n r)
      ≡⟨ refl ⟩
        (↑ , (↑ , max-n r))
      ∎

next≡suc : (r : ℕ) (x : DirNum r) →
            ¬ (x ≡ max-n r) → DirNum→ℕ (next x) ≡ suc (DirNum→ℕ x)
next≡suc zero tt ¬x≡maxnr = ⊥-elim (¬x≡maxnr refl)
next≡suc (suc r) (↓ , x) ¬x≡maxnr = refl
next≡suc (suc r) (↑ , x) ¬x≡maxnr =
    doubleℕ (DirNum→ℕ (next x))
  ≡⟨ cong doubleℕ (next≡suc r x (nextsuc-lemma r x ¬x≡maxnr)) ⟩
    doubleℕ (suc (DirNum→ℕ x))
  ≡⟨ refl ⟩
    suc (suc (doubleℕ (DirNum→ℕ x)))
  ∎

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
{-# OPTIONS --verbose=10 #-}

module leafs where

  open import Data.Nat
  open import Data.Vec
  open import Agda.Builtin.Sigma
  open import Data.Product
  open import Data.Fin using (fromℕ)

  open import trees
  open import optics
  open import lemmas

  leafsTree : {A : Set} -> Tree A -> ∃[ n ] (Vec A n × (Vec A n -> Tree A))
  leafsTree empty = 0 , ([] , λ _ -> empty)
  leafsTree (node empty root empty) =
    (1 , (root ∷ [] , λ v -> node empty (head v) empty))
  leafsTree {A} (node left root right) with leafsTree left | leafsTree right
  ...                                     | (n1 , (g1 , p1)) | (n2 , (g2 , p2)) =
     (n1 + n2 , (g1 ++ g2 , λ v -> node (p1 (take n1 v)) root (p2 (drop n1 v))))

  leafs : {A : Set} -> Traversal (Tree A) (Tree A) A A
  leafs = record{ extract = leafsTree }

  module tests where
    tree1 : Tree ℕ
    tree1 = node (node empty 1 empty) 3 empty

    open Traversal

    leafs1 : Vec ℕ 1
    leafs1 = get leafs tree1

    updatedleafs1 : Tree ℕ
    updatedleafs1 = put leafs (node tree1 5 tree1) (2 ∷ 5 ∷ [])

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Yoneda where

-- Yoneda Lemma.  In total, provides:
-- * the Yoneda Embedding (called embed here) from any Category C into Presheaves C
--   Worth noticing that there is no 'locally small' condition here; however, if one looks at
--   the levels involved, there is indeed a raise from that of C to that of Presheaves C.
-- * The traditional Yoneda lemma (yoneda-inverse) which says that for any object a of C, and
--   any Presheaf F over C (where our presheaves are over Setoids), then
--   Hom[ Presheaves C] (Functor.F₀ embed a , F) ≅ Functor.F₀ F a
--   as Setoids. In addition, Yoneda (yoneda) also says that this isomorphism is natural in a and F.
open import Level
open import Function.Base using (_$_)
open import Function.Bundles using (Inverse)
open import Function.Equality using (Π; _⟨$⟩_; cong)
open import Relation.Binary.Bundles using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product using (πʳ; πˡ; _※_)
open import Categories.Category.Construction.Presheaves using (Presheaves)
open import Categories.Category.Construction.Functors using (eval)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][-,-])
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Presheaf using (Presheaf)
open import Categories.Functor.Construction.LiftSetoids using (LiftSetoids)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

private
  variable
    o ℓ e : Level

module Yoneda (C : Category o ℓ e) where
  open Category C hiding (op) -- uses lots
  open HomReasoning using (_○_; ⟺)
  open MR C using (id-comm)
  open NaturalTransformation using (η; commute)
  open NT-Hom C using (Hom[A,C]⇒Hom[B,C])
  private
    module CE = Category.Equiv C using (refl)
    module C = Category C using (op)

  -- The Yoneda embedding functor
  embed : Functor C (Presheaves C)
  embed = record
    { F₀           = Hom[ C ][-,_]
    ; F₁           = Hom[A,C]⇒Hom[B,C] -- A⇒B induces a NatTrans on the Homs.
    ; identity     = identityˡ ○_
    ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ʳ h₁≈h₂ ○ assoc
    ; F-resp-≈     = λ f≈g h≈i → ∘-resp-≈ f≈g h≈i
    }

  -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor
  yoneda-inverse : (a : Obj) (F : Presheaf C (Setoids ℓ e)) →
    Inverse (Category.hom-setoid (Presheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
  yoneda-inverse a F = record
    { f = λ nat → η nat a ⟨$⟩ id
    ; f⁻¹ = λ x → ntHelper record
        { η       = λ X → record
          { _⟨$⟩_ = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
          ; cong  = λ i≈j → F.F-resp-≈ i≈j SE.refl
          }
        ; commute = λ {X} {Y} Y⇒X {f} {g} f≈g →
          let module SR = SetoidR (F.₀ Y) in
          SR.begin
             F.₁ (id ∘ f ∘ Y⇒X) ⟨$⟩ x   SR.≈⟨ F.F-resp-≈ (identityˡ ○ ∘-resp-≈ˡ f≈g) (SE.refl {x}) ⟩
             F.₁ (g ∘ Y⇒X) ⟨$⟩ x        SR.≈⟨ F.homomorphism SE.refl ⟩
             F.₁ Y⇒X ⟨$⟩ (F.₁ g ⟨$⟩ x)
           SR.∎
        }
    ; cong₁ = λ i≈j → i≈j CE.refl
    ; cong₂ = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
    ; inverse = (λ Fa → F.identity SE.refl) , λ nat {x} {z} z≈y →
        let module S     = Setoid (F.₀ x) in
        S.trans (S.sym (commute nat z CE.refl))
                (cong (η nat x) (identityˡ ○ identityˡ ○ z≈y))
    }
    where
    module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity)
    module SE = Setoid (F.₀ a) using (refl)

  private
    -- in this bifunctor, a presheaf from Presheaves C goes from C to Setoids ℓ e,
    -- but the over Setoids has higher level than the hom setoids.
    Nat[Hom[C][-,c],F] : Bifunctor (Presheaves C) (Category.op C) (Setoids _ _)
    Nat[Hom[C][-,c],F] = Hom[ Presheaves C ][-,-] ∘F (Functor.op embed ∘F πʳ ※ πˡ)

    -- in this bifunctor, it needs to go from Presheaves which maps C to Setoids ℓ e,
    -- so the universe level needs to be lifted.
    FC : Bifunctor (Presheaves C) (Category.op C) (Setoids _ _)
    FC = LiftSetoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ) ∘F eval {C = Category.op C} {D = Setoids ℓ e}

    module yoneda-inverse {a} {F} = Inverse (yoneda-inverse a F)

  -- the two bifunctors above are naturally isomorphic.
  -- it is easy to show yoneda-inverse first then to yoneda.
  yoneda : NaturalIsomorphism Nat[Hom[C][-,c],F] FC
  yoneda = record
    { F⇒G = ntHelper record
      { η       = λ where
        (F , A) → record
          { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α)
          ; cong  = λ i≈j → lift (i≈j CE.refl)
          }
      ; commute = λ where
        {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ)
      }
    ; F⇐G = ntHelper record
      { η       = λ (F , A) → record
          { _⟨$⟩_ = λ x → yoneda-inverse.f⁻¹ (lower x)
          ; cong  = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j)
          }
      ; commute = λ (α , f) eq eq′ → helper′ α f (lower eq) eq′
      }
    ; iso = λ (F , A) → record
        { isoˡ = λ {α β} i≈j {X} y≈z →
          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl)
        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.inverseˡ {F = F} _) (lower eq))
        }
    }
    where helper : {F : Functor C.op (Setoids ℓ e)}
                   {A B : Obj} (f : B ⇒ A)
                   (β γ : NaturalTransformation Hom[ C ][-, A ] F) →
                   Setoid._≈_ (Functor.F₀ Nat[Hom[C][-,c],F] (F , A)) β γ →
                   Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ f ∘ id) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id))
          helper {F} {A} {B} f β γ β≈γ = S.begin
            η β B ⟨$⟩ f ∘ id          S.≈⟨ cong (η β B) (id-comm ○ (⟺ identityˡ)) ⟩
            η β B ⟨$⟩ id ∘ id ∘ f     S.≈⟨ commute β f CE.refl ⟩
            F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩
            F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎
            where
            module F = Functor F using (₀;₁)
            module S = SetoidR (F.₀ B)

          helper′ : ∀ {F G : Functor (Category.op C) (Setoids ℓ e)}
                      {A B Z : Obj}
                      {h i : Z ⇒ B}
                      {X Y : Setoid.Carrier (Functor.F₀ F A)}
                      (α : NaturalTransformation F G)
                      (f : B ⇒ A) →
                      Setoid._≈_ (Functor.F₀ F A) X Y →
                      h ≈ i →
                      Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X)))
                                          (η α Z ⟨$⟩ (Functor.F₁ F (f ∘ i) ⟨$⟩ Y))
          helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin
            G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h (S′.sym (cong (F.₁ f) eq)) ⟩
            η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) (F.F-resp-≈ eq′ S′.refl) ⟩
            η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) (F.homomorphism (Setoid.refl (F.₀ A))) ⟩
            η α Z ⟨$⟩ (F.₁ (f ∘ i) ⟨$⟩ Y)        S.∎
            where
              module F = Functor F using (₀; ₁; homomorphism; F-resp-≈)
              module G = Functor G using (₀; ₁)
              module S = SetoidR (G.₀ Z)
              module S′ = Setoid (F.₀ B) using (refl; sym)

  module yoneda = NaturalIsomorphism yoneda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Pi.Everything where
open import Pi.Syntax     -- Syntax of Pi
open import Pi.Opsem      -- Abstract machine semantics of Pi
open import Pi.AuxLemmas  -- Some auxiliary lemmas about opsem for forward/backward deterministic proof
open import Pi.NoRepeat   -- Forward/backward deterministic lemmas and Non-repeating lemma
open import Pi.Eval       -- Evaluator for Pi
open import Pi.Interp     -- Big-step intepreter of Pi
open import Pi.Invariants -- Some invariants about abstract machine semantics
open import Pi.Properties -- Properties of Pi
open import Pi.Examples   -- Examples
open import Pi.Category   -- Pi Category


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.DiffInt where

open import Cubical.HITs.Ints.DiffInt.Base public
open import Cubical.HITs.Ints.DiffInt.Properties public

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Sum | S

type
  _⊕_ : 2-ary | l30

term
  inl  : α  ->  α ⊕ β
  inr  : β  ->  α ⊕ β
  case : α ⊕ β  α.γ  β.γ  ->  γ

theory
  (lβ) a : α   f : α.γ  g : β.γ |> case (inl(a), x.f[x], y.g[y])      = f[a]
  (rβ) b : β   f : α.γ  g : β.γ |> case (inr(b), x.f[x], y.g[y])      = g[b]
  (cη) s : α ⊕ β  c : (α ⊕ β).γ |> case (s, x.c[inl(x)], y.c[inr(y)]) = c[s]
-}

module Sum.Signature where

open import SOAS.Context

-- Type declaration
data ST : Set where
  _⊕_ : ST → ST → ST
infixl 30 _⊕_

open import SOAS.Syntax.Signature ST public
open import SOAS.Syntax.Build ST public

-- Operator symbols
data Sₒ : Set where
  inlₒ inrₒ : {α β : ST} → Sₒ
  caseₒ : {α β γ : ST} → Sₒ

-- Term signature
S:Sig : Signature Sₒ
S:Sig = sig λ
  { (inlₒ  {α}{β})    → (⊢₀ α) ⟼₁ α ⊕ β
  ; (inrₒ  {α}{β})    → (⊢₀ β) ⟼₁ α ⊕ β
  ; (caseₒ {α}{β}{γ}) → (⊢₀ α ⊕ β) , (α ⊢₁ γ) , (β ⊢₁ γ) ⟼₃ γ
  }

open Signature S:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- New feature by Jesper Cockx in commit be89d4a8b264dd2719cb8c601a2c7f45a95ba220 :
-- disabling the universe check for a data or record type.

-- Andreas, 2018-10-27, re issue #3327: restructured test cases.

module _ where

-- Pragma is naturally attached to definition.

module DataDef where

  data U : Set
  T : U → Set

  {-# NO_UNIVERSE_CHECK #-}
  data U where
    pi : (A : Set)(b : A → U) → U

  T (pi A b) = (x : A) → T (b x)

-- Pragma can also be attached to signature.

module DataSig where

  {-# NO_UNIVERSE_CHECK #-}
  data U : Set
  T : U → Set

  data U where
    pi : (A : Set)(b : A → U) → U

  T (pi A b) = (x : A) → T (b x)

-- Works also for explicit mutual blocks.

module Mutual where

  {-# NO_UNIVERSE_CHECK #-}
  data U : Set where
    pi : (A : Set)(b : A → U) → U

  T : U → Set
  T (pi A b) = (x : A) → T (b x)

-- Records:

module Records where

  {-# NO_UNIVERSE_CHECK #-}
  record R : Set where
    field out : Set

  {-# NO_UNIVERSE_CHECK #-}
  record S : Set

  record S where
    field out : Set

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
open import Nat
open import Prelude
open import core
open import contexts
open import typed-elaboration
open import lemmas-gcomplete
open import lemmas-complete
open import progress-checks
open import finality

module cast-inert where
  -- if a term is compelete and well typed, then the casts inside are all
  -- identity casts and there are no failed casts
  cast-inert : ∀{Δ Γ d τ} →
                  d dcomplete →
                  Δ , Γ ⊢ d :: τ →
                  cast-id d
  cast-inert dc TAConst = CIConst
  cast-inert dc (TAVar x₁) = CIVar
  cast-inert (DCLam dc x₁) (TALam x₂ wt) = CILam (cast-inert dc wt)
  cast-inert (DCAp dc dc₁) (TAAp wt wt₁) = CIAp (cast-inert dc wt) (cast-inert dc₁ wt₁)
  cast-inert () (TAEHole x x₁)
  cast-inert () (TANEHole x wt x₁)
  cast-inert (DCCast dc x x₁) (TACast wt x₂)
    with complete-consistency x₂ x x₁
  ... | refl = CICast (cast-inert dc wt)
  cast-inert () (TAFailedCast wt x x₁ x₂)

  -- in a well typed complete internal expression, every cast is the
  -- identity cast.
  complete-casts : ∀{Γ Δ d τ1 τ2} →
                   Γ , Δ ⊢ d ⟨ τ1 ⇒ τ2 ⟩ :: τ2 →
                   d ⟨ τ1 ⇒ τ2 ⟩ dcomplete →
                   τ1 == τ2
  complete-casts wt comp with cast-inert comp wt
  complete-casts wt comp | CICast qq = refl

  -- relates expressions to the same thing with all identity casts
  -- removed. note that this is a syntactic rewrite and it goes under
  -- binders.
  data no-id-casts : ihexp → ihexp → Set where
    NICConst  : no-id-casts c c
    NICVar    : ∀{x} → no-id-casts (X x) (X x)
    NICLam    : ∀{x τ d d'} → no-id-casts d d' → no-id-casts (·λ x [ τ ] d) (·λ x [ τ ] d')
    NICHole   : ∀{u} → no-id-casts (⦇-⦈⟨ u ⟩) (⦇-⦈⟨ u ⟩)
    NICNEHole : ∀{d d' u} → no-id-casts d d' → no-id-casts (⦇⌜ d ⌟⦈⟨ u ⟩) (⦇⌜ d' ⌟⦈⟨ u ⟩)
    NICAp     : ∀{d1 d2 d1' d2'} → no-id-casts d1 d1' → no-id-casts d2 d2' → no-id-casts (d1 ∘ d2) (d1' ∘ d2')
    NICCast   : ∀{d d' τ} → no-id-casts d d' → no-id-casts (d ⟨ τ ⇒ τ ⟩) d'
    NICFailed : ∀{d d' τ1 τ2} → no-id-casts d d' → no-id-casts (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) (d' ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩)

  -- removing identity casts doesn't change the type
  no-id-casts-type : ∀{Γ Δ d τ d' } → Δ , Γ ⊢ d :: τ →
                                      no-id-casts d d' →
                                      Δ , Γ ⊢ d' :: τ
  no-id-casts-type TAConst NICConst = TAConst
  no-id-casts-type (TAVar x₁) NICVar = TAVar x₁
  no-id-casts-type (TALam x₁ wt) (NICLam nic) = TALam x₁ (no-id-casts-type wt nic)
  no-id-casts-type (TAAp wt wt₁) (NICAp nic nic₁) = TAAp (no-id-casts-type wt nic) (no-id-casts-type wt₁ nic₁)
  no-id-casts-type (TAEHole x x₁) NICHole = TAEHole x x₁
  no-id-casts-type (TANEHole x wt x₁) (NICNEHole nic) = TANEHole x (no-id-casts-type wt nic) x₁
  no-id-casts-type (TACast wt x) (NICCast nic) = no-id-casts-type wt nic
  no-id-casts-type (TAFailedCast wt x x₁ x₂) (NICFailed nic) = TAFailedCast (no-id-casts-type wt nic) x x₁ x₂

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
-- Andreas, 2018-11-03, issue #3364
--
-- Better error when trying to import with new qualified module name.

open import Agda.Builtin.Nat as Builtin.Nat

-- WAS: Error:
-- Not in scope:
--   as at ...
-- when scope checking as

-- NOW: Warning
-- `as' must be followed by an unqualified name
-- when scope checking the declaration
--   open import Agda.Builtin.Nat as Builtin.Nat


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.PartialOrder
  {c ℓ} {A : Type c} (P : PartialOrder A ℓ) where

open PartialOrder P
import Cubical.Relation.Binary.Raw.Construct.NonStrictToStrict _≤_ as Strict

------------------------------------------------------------------------
-- Re-export contents of base module

open import Cubical.Relation.Binary.Reasoning.Base.Double
  isPreorder
  (Strict.<-transitive isPartialOrder)
  Strict.<⇒≤
  (Strict.<-≤-trans transitive antisym)
  (Strict.≤-<-trans transitive antisym)
  public


text:
-- exercises
-- * basic logic properties (implication, and, or, bot, not, forall, exists)
-- * data types
-- * records
-- * non-dep, non-rec, non-indexed case splits
-- * including elimination constants as hints
-- * hidden arguments

open import Auto.Prelude

h0 : (A : Set) → A → A
h0 = {!!}
--h0 = λ A z → z

h1 : (A B : Set) → A → (A → B) → B
h1 = {!!}
--h1 = λ A B z z₁ → z₁ z

h2 : ∀ A B → A ∧ B → B ∧ A
h2 = {!!}
--h2 = λ A B z → ∧-i (_∧_.snd z) (_∧_.fst z)

h3 : ∀ A B C → (A ∧ B) ∧ C → A ∧ (B ∧ C)
h3 = {!!}
--h3 = λ A B C z →
--         ∧-i (_∧_.fst (_∧_.fst z)) (∧-i (_∧_.snd (_∧_.fst z)) (_∧_.snd z))

h4 : (A B C : Set) → A ∨ B → (A → C) → (B → C) → C
h4 A B C x h₁ h₂ = {!-c!}

h5 : ∀ A B → A ∨ B → B ∨ A
h5 A B x = {!-c!}
--h5 A B (∨-i₁ x) = ∨-i₂ x
--h5 A B (∨-i₂ x) = ∨-i₁ x

h6 : ∀ A B C → (A ∨ B) ∨ C → A ∨ (B ∨ C)
h6 A B C x = {!-c!}
--h6 A B C (∨-i₁ (∨-i₁ x)) = ∨-i₁ x
--h6 A B C (∨-i₁ (∨-i₂ x)) = ∨-i₂ (∨-i₁ x)
--h6 A B C (∨-i₂ x) = ∨-i₂ (∨-i₂ x)

h7 : (A : Set) → ⊥ → A
h7 A x = {!-c!}

h8 : ∀ A → A → ¬ (¬ A)
h8 = {!!}
--h8 = λ A z z₁ → z₁ z

h9 : ∀ A → ¬ (¬ (¬ A)) → ¬ A
h9 = {!!}
--h9 = λ A z z₁ → z (λ z₂ → z₂ z₁)

h10 : (∀ A → ¬ (¬ A) → A) →
     (∀ A → A ∨ ¬ A)
h10 = {!!}
--h10 = λ z A →
--         z (A ∨ ((x : A) → ⊥)) (λ z₁ → z₁ (∨-i₂ (λ x → z₁ (∨-i₁ x))))

h11 : (∀ A → A ∨ ¬ A) →
      (∀ A → ¬ (¬ A) → A)
h11 = {!∨-e ⊥-e!}
--h11 = λ z A z₁ →
--          ∨-e A ((x : A) → ⊥) A (z A) (λ z₂ → z₂) (λ z₂ → ⊥-e A (z₁ z₂))

h12 : {X : Set} {P Q : X → Set} → ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x)
h12 = {!!}
--h12 = λ {X} {P} {Q} z → ∧-i (λ x → _∧_.fst (z x)) (λ x → _∧_.snd (z x))

h13 : {X : Set} {P Q : X → Set} → ((x : X) → P x) ∧ ((x : X) → Q x) → ((x : X) → P x ∧ Q x)
h13 = {!!}
--h13 = λ {X} {P} {Q} z x → ∧-i (_∧_.fst z x) (_∧_.snd z x)

n0 : {X : Set} {P Q : X → Set} → Σ X (λ x → P x ∨ Q x) → Σ X P ∨ Σ X Q
--n0 = {!∨-e!}  -- no solution found, not even for the two subproofs
n0 = λ h → ∨-e _ _ _ (Σ.prf h) (λ x → ∨-i₁ (Σ-i (Σ.wit h) x)) (λ x → ∨-i₂ (Σ-i (Σ.wit h) x))

n1 : {X : Set} {P Q : X → Set} → Σ X P ∨ Σ X Q → Σ X (λ x → P x ∨ Q x)
--n1 = {!∨-e!}  -- no solution found, not even for the two subproofs
n1 = λ h → ∨-e _ _ _ h (λ x → Σ-i (Σ.wit x) (∨-i₁ (Σ.prf x))) (λ x → Σ-i (Σ.wit x) (∨-i₂ (Σ.prf x)))

h14 : {X : Set} → (x : X) → Σ X (λ x → ⊤)
h14 = {!!}
--h14 = λ {X} x → Σ-i x (record {})

h15 : {X : Set} → Σ (X → X) (λ x → ⊤)
h15 = {!!}
--h15 = λ {X} → Σ-i (λ x → x) (record {})

h16 : {X : Set} {P : X → Set} → Σ (X → X) (λ f → (x : X) → P (f x) → P x)
h16 = {!!}
--h16 = λ {X} {P} → Σ-i (λ x → x) (λ x x₁ → x₁)

module Drink where

 postulate RAA : (A : Set) → (¬ A → ⊥) → A

 drink : (A : Set) → (a : A)
            → (Drink : A → Set) → Σ A (λ x → (Drink x) → Π A Drink)
 drink A a Drink = {!RAA!}  -- h17
{-
 drink A a Drink = RAA (Σ A (λ z → (x : Drink z) → Π A Drink))
                     (λ z →
                        z
                        (Σ-i a
                         (λ x →
                            fun
                            (λ a₁ →
                               RAA (Drink a₁)
                               (λ z₁ →
                                  z (Σ-i a₁ (λ x₁ → fun (λ a₂ → RAA (Drink a₂) (λ _ → z₁ x₁)))))))))  -- h17
-}


text:
module TLP02 where

open import Data.Bool
open import Data.Nat
open import Data.String
open import Relation.Binary.PropositionalEquality
  as PropEq using (_≡_; refl)

-- ----- Star型の定義 -----
data Star : Set where
  NIL : Star
  TRU : Star
  N   : ℕ → Star
  S   : String → Star
  C   : Star → Star → Star

-- ----- 組込関数の定義 -----
postulate
  CONS : Star → Star → Star
  CAR : Star → Star
  CDR : Star → Star
  ATOM : Star → Star
  IF : Star → Star → Star → Star
  EQUAL : Star → Star → Star
  SIZE : Star → Star
  LT : Star → Star → Star

-- ----- Starから≡に -----
postulate
  ~ : Star → Star
  equal-eq : {x y : Star} → (EQUAL x y) ≡ TRU →  x ≡ y
  ifAP : {q x y : Star} → (IF q (EQUAL x y) TRU) ≡ TRU → (q ≡ TRU → x ≡ y)
  ifEP : {q x y : Star} → (IF q TRU (EQUAL x y)) ≡ TRU → ((~ q) ≡ TRU → x ≡ y)
-- ----- 公理 -----
  equal-same : (x : Star) → (EQUAL (EQUAL x x) TRU) ≡ TRU
  equal-swap : (x y : Star) → (EQUAL (EQUAL x y) (EQUAL y x)) ≡ TRU
  equal-if : (x y : Star) → (IF (EQUAL x y) (EQUAL x y) TRU) ≡ TRU
  atom/cons : (x y : Star) → (EQUAL (ATOM (CONS x y)) NIL) ≡ TRU
  car/cons : (x y : Star) → (EQUAL (CAR (CONS x y)) x) ≡ TRU
  cdr/cons : (x y : Star) → (EQUAL (CDR (CONS x y)) y) ≡ TRU
  cons/car+cdr : (x : Star)
    → (IF (ATOM x) TRU (EQUAL (CONS (CAR x) (CDR x)) x)) ≡ TRU
  if-true : (x y : Star) → (EQUAL (IF TRU x y) x) ≡ TRU
  if-false : (x y : Star) → (EQUAL (IF NIL x y) y) ≡ TRU
  if-same : (x y : Star) → (EQUAL (IF x y y) y) ≡ TRU
  if-nest-A : (x y z : Star) → (IF x (EQUAL (IF x y z) y) TRU) ≡ TRU
  if-nest-E : (x y z : Star) → (IF x TRU (EQUAL (IF x y z) z)) ≡ TRU
  size/car : (x : Star)
    → (IF (ATOM x) TRU (EQUAL (LT (SIZE (CAR x)) (SIZE x)) TRU)) ≡ TRU
  size/cdr : (x : Star)
    → (IF (ATOM x) TRU (EQUAL (LT (SIZE (CDR x)) (SIZE x)) TRU)) ≡ TRU

-- ----- 練習 -----
hoge2 : (ATOM (CONS TRU TRU)) ≡ NIL
hoge2 = equal-eq (atom/cons TRU TRU)

hoge2' : (ATOM (CONS TRU TRU)) ≡ NIL
hoge2'
  rewrite (equal-eq (atom/cons TRU TRU))
    = refl
-- -----

{--
-- ----- 停止性で引っかかる -----
memb?' : Star → Star
memb?' xs =
  (IF (ATOM xs)
       NIL
       (IF (EQUAL (CAR xs) (S "?"))
           TRU
           (memb?' (CDR xs))))
--}
-- ----- memb?の停止性 -----
postulate
  premise : (xs : Star) → (~ (ATOM xs)) ≡ TRU
measure-memb? : (xs : Star)
  → (IF (ATOM xs)
        TRU
        (IF (EQUAL (CAR xs) (S "?"))
            TRU
            (LT (SIZE (CDR xs)) (SIZE xs))))
    ≡ TRU
measure-memb? xs
  rewrite (ifEP (size/cdr xs) (premise xs))
        | (equal-eq (if-same (EQUAL (CAR xs) (S "?")) TRU))
        | (equal-eq (if-same (ATOM xs) TRU)) = refl

-- ----- memb?の定義 -----
postulate
  memb? : Star → Star
  def-memb? : (xs : Star) →
    memb? xs ≡
      (IF (ATOM xs)
          NIL
          (IF (EQUAL (CAR xs) (S "?"))
              TRU
              (memb? (CDR xs))))
-- ----- rembの定義 -----
postulate
  remb : Star → Star
  def-remb : (xs : Star) →
    remb xs ≡
      (IF (ATOM xs)
          (S "'()")
          (IF (EQUAL (CAR xs) (S "?"))
              (remb (CDR xs))
              (CONS (CAR xs)
                 (remb (CDR xs)))))
-- ----- 帰納的な証明 -----
postulate
  premise2 : (xs : Star) → (ATOM xs) ≡ TRU
  premise3 : (xs : Star) → ~ (ATOM xs) ≡ TRU
  atomt : (ATOM (S "'()")) ≡ TRU
memb?/remb : (xs : Star)
  → (IF (ATOM xs)
        (EQUAL (memb? (remb xs)) NIL)
        (IF (EQUAL (memb? (remb (CDR xs))) NIL)
            (EQUAL (memb? (remb xs)) NIL)
            TRU))
    ≡ IF (ATOM xs) TRU (IF (EQUAL (memb? (remb (CDR xs))) NIL) TRU TRU)
memb?/remb xs
  rewrite (def-remb xs)
        | (ifAP (if-nest-A (ATOM xs) (S "'()") ((IF (EQUAL (CAR xs) (S "?"))
              (remb (CDR xs))
              (CONS (CAR xs)
                 (remb (CDR xs)))))) (premise2 xs))
        | (def-memb? ((S "'()")))
        | (atomt)
        | (equal-eq (if-true NIL ((IF (EQUAL (CAR (S "'()")) (S "?"))
                        TRU
                        (memb? (CDR (S "'()")))))))
        | (equal-eq (equal-same NIL))
        | (def-remb xs)
          -- ----- ここで証明ステップが一気に進んだ
        | (ifEP (if-nest-E (ATOM xs) (S "'()") (IF (EQUAL (CAR xs) (S "?"))
              (remb (CDR xs))
              (CONS (CAR xs)
                 (remb (CDR xs))))) (premise3 xs)) = refl

memb?/remb2 : (xs : Star)
  → IF (ATOM xs) TRU (IF (EQUAL (memb? (remb (CDR xs))) NIL) TRU TRU)
    ≡ TRU
memb?/remb2 xs
  rewrite (equal-eq (if-same (EQUAL (memb? (remb (CDR xs))) NIL) TRU))
        | (equal-eq (if-same (ATOM xs) TRU)) = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of algebraic structures defined over some other
-- structure, like modules and vector spaces
--
-- Terminology of bundles:
-- * There are both *semimodules* and *modules*.
--   - For M an R-semimodule, R is a semiring, and M forms a commutative
--     monoid.
--   - For M an R-module, R is a ring, and M forms an Abelian group.
-- * There are all four of *left modules*, *right modules*, *bimodules*,
--   and *modules*.
--   - Left modules have a left-scaling operation.
--   - Right modules have a right-scaling operation.
--   - Bimodules have two sorts of scalars. Left-scaling handles one and
--     right-scaling handles the other. Left-scaling and right-scaling
--     are furthermore compatible.
--   - Modules are bimodules with a single sort of scalars and scalar
--     multiplication must also be commutative. Left-scaling and
--     right-scaling coincide.
------------------------------------------------------------------------

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

module Algebra.Module.Bundles where

open import Algebra.Bundles
open import Algebra.Core
open import Algebra.Module.Structures
open import Algebra.Module.Definitions
open import Function.Base
open import Level
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetR

private
  variable
    r ℓr s ℓs : Level

------------------------------------------------------------------------
-- Left modules
------------------------------------------------------------------------

record LeftSemimodule (semiring : Semiring r ℓr) m ℓm
                      : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open Semiring semiring

  infixr 7 _*ₗ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    isLeftSemimodule : IsLeftSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_

  open IsLeftSemimodule isLeftSemimodule public

  +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
  +ᴹ-commutativeMonoid = record
    { isCommutativeMonoid = +ᴹ-isCommutativeMonoid
    }

  open CommutativeMonoid +ᴹ-commutativeMonoid public
    using () renaming
    ( monoid    to +ᴹ-monoid
    ; semigroup to +ᴹ-semigroup
    ; magma     to +ᴹ-magma
    ; rawMagma  to +ᴹ-rawMagma
    ; rawMonoid to +ᴹ-rawMonoid
    )

record LeftModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open Ring ring

  infixr 8 -ᴹ_
  infixr 7 _*ₗ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    -ᴹ_ : Op₁ Carrierᴹ
    isLeftModule : IsLeftModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_

  open IsLeftModule isLeftModule public

  leftSemimodule : LeftSemimodule semiring m ℓm
  leftSemimodule = record { isLeftSemimodule = isLeftSemimodule }

  open LeftSemimodule leftSemimodule public
    using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)

  +ᴹ-abelianGroup : AbelianGroup m ℓm
  +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }

  open AbelianGroup +ᴹ-abelianGroup public
    using () renaming (group to +ᴹ-group)

------------------------------------------------------------------------
-- Right modules
------------------------------------------------------------------------

record RightSemimodule (semiring : Semiring r ℓr) m ℓm
                       : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open Semiring semiring

  infixl 7 _*ᵣ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ᵣ_ : Opᵣ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    isRightSemimodule : IsRightSemimodule semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ᵣ_

  open IsRightSemimodule isRightSemimodule public

  +ᴹ-commutativeMonoid : CommutativeMonoid m ℓm
  +ᴹ-commutativeMonoid = record
    { isCommutativeMonoid = +ᴹ-isCommutativeMonoid
    }

  open CommutativeMonoid +ᴹ-commutativeMonoid public
    using () renaming
    ( monoid    to +ᴹ-monoid
    ; semigroup to +ᴹ-semigroup
    ; magma     to +ᴹ-magma
    ; rawMagma  to +ᴹ-rawMagma
    ; rawMonoid to +ᴹ-rawMonoid
    )

record RightModule (ring : Ring r ℓr) m ℓm : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open Ring ring

  infixr 8 -ᴹ_
  infixl 7 _*ᵣ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ᵣ_ : Opᵣ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    -ᴹ_ : Op₁ Carrierᴹ
    isRightModule : IsRightModule ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ᵣ_

  open IsRightModule isRightModule public

  rightSemimodule : RightSemimodule semiring m ℓm
  rightSemimodule = record { isRightSemimodule = isRightSemimodule }

  open RightSemimodule rightSemimodule public
    using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)

  +ᴹ-abelianGroup : AbelianGroup m ℓm
  +ᴹ-abelianGroup = record { isAbelianGroup = +ᴹ-isAbelianGroup }

  open AbelianGroup +ᴹ-abelianGroup public
    using () renaming (group to +ᴹ-group)

------------------------------------------------------------------------
-- Bimodules
------------------------------------------------------------------------

record Bisemimodule (R-semiring : Semiring r ℓr) (S-semiring : Semiring s ℓs)
                    m ℓm : Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
  private
    module R = Semiring R-semiring
    module S = Semiring S-semiring

  infixr 7 _*ₗ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ R.Carrier Carrierᴹ
    _*ᵣ_ : Opᵣ S.Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    isBisemimodule : IsBisemimodule R-semiring S-semiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_

  open IsBisemimodule isBisemimodule public

  leftSemimodule : LeftSemimodule R-semiring m ℓm
  leftSemimodule = record { isLeftSemimodule = isLeftSemimodule }

  rightSemimodule : RightSemimodule S-semiring m ℓm
  rightSemimodule = record { isRightSemimodule = isRightSemimodule }

  open LeftSemimodule leftSemimodule public
    using ( +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma
          ; +ᴹ-rawMonoid)

record Bimodule (R-ring : Ring r ℓr) (S-ring : Ring s ℓs) m ℓm
                : Set (r ⊔ s ⊔ ℓr ⊔ ℓs ⊔ suc (m ⊔ ℓm)) where
  private
    module R = Ring R-ring
    module S = Ring S-ring

  infixr 7 _*ₗ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ R.Carrier Carrierᴹ
    _*ᵣ_ : Opᵣ S.Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    -ᴹ_ : Op₁ Carrierᴹ
    isBimodule : IsBimodule R-ring S-ring _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_

  open IsBimodule isBimodule public

  leftModule : LeftModule R-ring m ℓm
  leftModule = record { isLeftModule = isLeftModule }

  rightModule : RightModule S-ring m ℓm
  rightModule = record { isRightModule = isRightModule }

  open LeftModule leftModule public
    using ( +ᴹ-abelianGroup; +ᴹ-commutativeMonoid; +ᴹ-group; +ᴹ-monoid
          ; +ᴹ-semigroup; +ᴹ-magma; +ᴹ-rawMagma; +ᴹ-rawMonoid)

  bisemimodule : Bisemimodule R.semiring S.semiring m ℓm
  bisemimodule = record { isBisemimodule = isBisemimodule }

  open Bisemimodule bisemimodule public
    using (leftSemimodule; rightSemimodule)

------------------------------------------------------------------------
-- Modules over commutative structures
------------------------------------------------------------------------

record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
                  : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open CommutativeSemiring commutativeSemiring

  infixr 7 _*ₗ_
  infixl 7 _*ᵣ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ Carrier Carrierᴹ
    _*ᵣ_ : Opᵣ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    isSemimodule : IsSemimodule commutativeSemiring _≈ᴹ_ _+ᴹ_ 0ᴹ _*ₗ_ _*ᵣ_

  open IsSemimodule isSemimodule public

  private
    module L = LeftDefs Carrier _≈ᴹ_
    module R = RightDefs Carrier _≈ᴹ_

  bisemimodule : Bisemimodule semiring semiring m ℓm
  bisemimodule = record { isBisemimodule = isBisemimodule }

  open Bisemimodule bisemimodule public
    using ( leftSemimodule; rightSemimodule
          ; +ᴹ-commutativeMonoid; +ᴹ-monoid; +ᴹ-semigroup; +ᴹ-magma
          ; +ᴹ-rawMagma; +ᴹ-rawMonoid)

  open SetR ≈ᴹ-setoid

  *ₗ-comm : L.Commutative _*ₗ_
  *ₗ-comm x y m = begin
    x *ₗ y *ₗ m   ≈⟨ ≈ᴹ-sym (*ₗ-assoc x y m) ⟩
    (x * y) *ₗ m  ≈⟨ *ₗ-cong (*-comm _ _) ≈ᴹ-refl ⟩
    (y * x) *ₗ m  ≈⟨ *ₗ-assoc y x m ⟩
    y *ₗ x *ₗ m   ∎

  *ᵣ-comm : R.Commutative _*ᵣ_
  *ᵣ-comm m x y = begin
    m *ᵣ x *ᵣ y   ≈⟨ *ᵣ-assoc m x y ⟩
    m *ᵣ (x * y)  ≈⟨ *ᵣ-cong ≈ᴹ-refl (*-comm _ _) ⟩
    m *ᵣ (y * x)  ≈⟨ ≈ᴹ-sym (*ᵣ-assoc m y x) ⟩
    m *ᵣ y *ᵣ x   ∎

record Module (commutativeRing : CommutativeRing r ℓr) m ℓm
              : Set (r ⊔ ℓr ⊔ suc (m ⊔ ℓm)) where
  open CommutativeRing commutativeRing

  infixr 8 -ᴹ_
  infixr 7 _*ₗ_
  infixl 6 _+ᴹ_
  infix 4 _≈ᴹ_

  field
    Carrierᴹ : Set m
    _≈ᴹ_ : Rel Carrierᴹ ℓm
    _+ᴹ_ : Op₂ Carrierᴹ
    _*ₗ_ : Opₗ Carrier Carrierᴹ
    _*ᵣ_ : Opᵣ Carrier Carrierᴹ
    0ᴹ : Carrierᴹ
    -ᴹ_ : Op₁ Carrierᴹ
    isModule : IsModule commutativeRing _≈ᴹ_ _+ᴹ_ 0ᴹ -ᴹ_ _*ₗ_ _*ᵣ_

  open IsModule isModule public

  bimodule : Bimodule ring ring m ℓm
  bimodule = record { isBimodule = isBimodule }

  open Bimodule bimodule public
    using ( leftModule; rightModule; leftSemimodule; rightSemimodule
          ; +ᴹ-abelianGroup; +ᴹ-group; +ᴹ-commutativeMonoid; +ᴹ-monoid
          ; +ᴹ-semigroup; +ᴹ-magma ; +ᴹ-rawMonoid; +ᴹ-rawMagma)

  semimodule : Semimodule commutativeSemiring m ℓm
  semimodule = record { isSemimodule = isSemimodule }

  open Semimodule semimodule public using (*ₗ-comm; *ᵣ-comm)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The universal binary relation
------------------------------------------------------------------------

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

module Relation.Binary.Construct.Always where

open import Relation.Binary
open import Relation.Binary.Construct.Constant using (Const)
open import Data.Unit using (⊤; tt)
open import Level using (Lift; lift)

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

Always : ∀ {a ℓ} {A : Set a} → Rel A ℓ
Always = Const (Lift _ ⊤)

------------------------------------------------------------------------
-- Properties

module _ {a} (A : Set a) ℓ where

  refl : Reflexive {ℓ = ℓ} {A} Always
  refl = lift tt

  sym : Symmetric {ℓ = ℓ} {A} Always
  sym _ = lift tt

  trans : Transitive {ℓ = ℓ} {A} Always
  trans _ _ = lift tt

  isEquivalence : IsEquivalence {ℓ = ℓ} {A} Always
  isEquivalence = record {}

  setoid : Setoid a ℓ
  setoid = record
    { isEquivalence = isEquivalence
    }

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

-- Version 0.17

Always-setoid = setoid
{-# WARNING_ON_USAGE Always-setoid
"Warning: Always-setoid was deprecated in v0.14.
Please use setoid instead."
#-}


text:
module Oscar.Category.Action where

open import Oscar.Category.Setoid
open import Oscar.Function
open import Oscar.Level

record Action {𝔬} (⋆ : Set 𝔬) 𝔄𝔬 𝔄𝔮
       : Set (𝔬 ⊔ lsuc (𝔄𝔬 ⊔ 𝔄𝔮))
  where

  field
    𝔄 : ⋆ → Setoid 𝔄𝔬 𝔄𝔮
    ⦃ isSetoid ⦄ : ∀ {x} → IsSetoid (Setoid.⋆ (𝔄 x)) 𝔄𝔮

  ↥ : ⋆ → Set 𝔄𝔬
  ↥ = Setoid.⋆ ∘ 𝔄


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

module Cham.Inference where


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

module Categories.Bicategory.Instance.Cats where

-- The category of categories (Cats) is a Bicategory
open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)

open import Categories.Bicategory using (Bicategory)
open import Categories.Category using (Category)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
open import Categories.Category.Instance.One using (One)
open import Categories.Category.Product using (Product; πˡ; πʳ; _※_)
open import Categories.Category.Construction.Functors
open import Categories.Functor.Construction.Constant
import Categories.Morphism.Reasoning as MR

Cats : (o ℓ e : Level) → Bicategory (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e) (suc (o ⊔ ℓ ⊔ e))
Cats o ℓ e = record
  { enriched = record
    { Obj     = Category o ℓ e
    ; hom     = Functors
    ; id      = λ {A} → const {D = Functors A A} {C = One} idF
    ; ⊚       = product
    ; ⊚-assoc = λ {A B C D} →
      let module D = Category D in
      let module C = Category C in record
        { F⇒G = ntHelper record
          { η       = λ { ((F₁ , F₂) , F₃) → F⇒G (associator F₃ F₂ F₁) }
          -- the proof is as below, so write it raw combinator-style
          ; commute = λ { {(G₁ , G₂) , G₃} {(H₁ , H₂) , H₃} ((η₁ , η₂) , η₃) {x} →
            let open Category D in let open HomReasoning in
            identityˡ ○ ⟺ assoc ○ ∘-resp-≈ˡ (⟺ (homomorphism H₁)) ○ ⟺ identityʳ}
        }
        ; F⇐G = ntHelper record
          { η       =  λ { ((F₁ , F₂) , F₃) → F⇐G (associator F₃ F₂ F₁)}
          ; commute = λ { {(G₁ , G₂) , G₃} {(H₁ , H₂) , H₃} ((η₁ , η₂) , η₃) {x} →
            let open Category D in let open HomReasoning in begin
            id ∘ F₁ H₁ (F₁ H₂ (η η₃ x) C.∘ η η₂ (F₀ G₃ x)) ∘ η η₁ (F₀ G₂ (F₀ G₃ x))
                ≈⟨ identityˡ ⟩
            F₁ H₁ (F₁ H₂ (η η₃ x) C.∘ η η₂ (F₀ G₃ x)) ∘ η η₁ (F₀ G₂ (F₀ G₃ x))
                ≈⟨ homomorphism H₁ ⟩∘⟨refl ⟩
            (F₁ H₁ (F₁ H₂ (η η₃ x)) ∘ F₁ H₁ (η η₂ (F₀ G₃ x))) ∘ η η₁ (F₀ G₂ (F₀ G₃ x))
                ≈⟨ assoc ⟩
            F₁ H₁ (F₁ H₂ (η η₃ x)) ∘ F₁ H₁ (η η₂ (F₀ G₃ x)) ∘ η η₁ (F₀ G₂ (F₀ G₃ x))
                ≈˘⟨ identityʳ ⟩
            (F₁ H₁ (F₁ H₂ (η η₃ x)) ∘ F₁ H₁ (η η₂ (F₀ G₃ x)) ∘ η η₁ (F₀ G₂ (F₀ G₃ x))) ∘ id ∎ }
          }
        ; iso = λ X → record { isoˡ = D.identityʳ ; isoʳ = D.identityˡ }
        }
    ; unitˡ = λ {A} {B} → let module B = Category B in let open B.HomReasoning in record
      { F⇒G = ntHelper record { η = λ _ → F⇒G unitorˡ ; commute = λ _ → B.identityˡ }
      ; F⇐G = ntHelper record
        { η       = λ _ → F⇐G unitorˡ
        ; commute = λ f → B.identityˡ ○ ⟺ B.identityʳ ○ ⟺ B.identityʳ
        }
      ; iso = λ _ → record { isoˡ = B.identityˡ ; isoʳ = B.identityʳ }
      }
    ; unitʳ = λ {A} {B} → let open Category B in let open HomReasoning in record
      { F⇒G = ntHelper record
        { η       = λ _ → F⇒G unitorʳ
        ; commute = λ { {_} {Y , _} (f , _) {x} → begin
          id ∘ F₁ Y (Category.id A) ∘ η f x ≈⟨ identityˡ ○ ∘-resp-≈ˡ (identity Y) ○ MR.id-comm-sym B ⟩
          η f x ∘ id                        ∎ }
        }
      ; F⇐G = ntHelper record
         { η       = λ _ → F⇐G unitorʳ
         ; commute = λ { {_} {Y , _} (f , _) {x} → begin
             id ∘ η f x                          ≈˘⟨  identity Y ⟩∘⟨refl ⟩
             F₁ Y (Category.id A) ∘ η f x        ≈˘⟨  identityʳ ⟩
             (F₁ Y (Category.id A) ∘ η f x) ∘ id ∎ }
         }
      ; iso = λ _ → record { isoˡ = identityˡ ; isoʳ = identityʳ }
      }
    }
  ; triangle = λ {_ _ C} → Category.identityʳ C
  ; pentagon = λ {A B C D E} {f g h i} {X} →
      let open Category E in
      let open HomReasoning in begin
        (F₁ i (Category.id D) ∘ id) ∘ id ∘ F₁ i (F₁ h (F₁ g (Category.id B))) ∘ id
          ≈⟨ identityʳ ⟩∘⟨ (identityˡ ○ identityʳ) ⟩
        F₁ i (Category.id D) ∘ F₁ i (F₁ h (F₁ g (Category.id B)))
          ≈⟨ identity i ⟩∘⟨ F-resp-≈ i (F-resp-≈ h (identity g)) ⟩
        id ∘ F₁ i (F₁ h (Category.id C))
          ≈⟨ refl⟩∘⟨ F-resp-≈ i (identity h) ⟩
        id ∘ F₁ i (Category.id D)
          ≈⟨ refl⟩∘⟨ identity i ⟩
        id ∘ id
          ∎
  }
  where
    open NaturalTransformation
    open NaturalIsomorphism
    open Functor


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Application of substitutions to lists, along with various lemmas
------------------------------------------------------------------------

-- This module illustrates how Data.Fin.Substitution.Lemmas.AppLemmas
-- can be used.

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

open import Data.Fin.Substitution.Lemmas
open import Data.Nat using (ℕ)

module Data.Fin.Substitution.List {ℓ} {T : ℕ → Set ℓ} (lemmas₄ : Lemmas₄ T) where

open import Data.List.Base
open import Data.List.Properties
open import Data.Fin.Substitution
import Function as Fun
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

private
  open module L = Lemmas₄ lemmas₄ using (_/_; id; _⊙_)

infixl 8 _//_

_//_ : ∀ {m n} → List (T m) → Sub T m n → List (T n)
ts // ρ = map (λ σ → σ / ρ) ts

appLemmas : AppLemmas (λ n → List (T n)) T
appLemmas = record
  { application = record { _/_ = _//_ }
  ; lemmas₄     = lemmas₄
  ; id-vanishes = λ ts → begin
      ts // id       ≡⟨ map-cong L.id-vanishes ts ⟩
      map Fun.id ts  ≡⟨ map-id ts ⟩
      ts             ∎
  ; /-⊙ = λ {_ _ _ ρ₁ ρ₂} ts → begin
      ts // ρ₁ ⊙ ρ₂               ≡⟨ map-cong L./-⊙ ts ⟩
      map (λ σ → σ / ρ₁ / ρ₂) ts  ≡⟨ map-compose ts ⟩
      ts // ρ₁ // ρ₂              ∎
  }

open AppLemmas appLemmas public
  hiding (_/_) renaming (_/✶_ to _//✶_)


text:
module MutualBlockInLet where

postulate
  A : Set
  a : A

test = let abstract
             x = a
             y = x
       in y

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
open import Relation.Binary.Core

module PLRTree.Push.Heap {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)
                     (trans≤ : Transitive _≤_) where

open import Data.Sum
open import Induction.WellFounded
open import Order.Total _≤_ tot≤
open import PLRTree {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Heap _≤_
open import PLRTree.Heap.Properties _≤_ trans≤
open import PLRTree.Order {A}
open import PLRTree.Order.Properties {A}

lemma-push-≤* : {x y : A}{l r : PLRTree}(t : Tag) → x ≤ y → x ≤* l → x ≤* r → (acc : Acc _≺_ (node t y l r)) → x ≤* (push (node t y l r) acc)
lemma-push-≤* {x} t x≤y (lf≤* .x) x≤*r (acc rs) = nd≤* x≤y (lf≤* x) (lf≤* x)
lemma-push-≤* {x} {y} t x≤y (nd≤* {t'} .{x} {x'} x≤x' x≤*l' x≤*r') (lf≤* .x) (acc rs)
    with tot≤ y x'
... | inj₁ y≤x' = nd≤* x≤y (nd≤* x≤x' (lf≤* x) (lf≤* x)) (lf≤* x)
... | inj₂ x'≤y = nd≤* x≤x' (nd≤* x≤y (lf≤* x) (lf≤* x)) (lf≤* x)
lemma-push-≤* {x} {y} t x≤y (nd≤* {t'} .{x} {x'} {l'} {r'} x≤x' x≤*l' x≤*r') (nd≤* {t''} .{x} {x''} {l''} {r''} x≤x'' x≤*l'' x≤*r'') (acc rs)
    with tot≤ y x' | tot≤ y x'' | tot≤ x' x''
... | inj₁ y≤x' | inj₁ y≤x'' | _ = nd≤* x≤y (nd≤* x≤x' x≤*l' x≤*r') (nd≤* x≤x'' x≤*l'' x≤*r'')
... | inj₁ y≤x' | inj₂ x''≤y | _ rewrite lemma-≡-height t'' y x'' l'' r'' =
           let acc-t''yl''r'' = rs (node t'' y l'' r'') (lemma-≺-right t y (node t' x' l' r') (node t'' x'' l'' r''))
           in nd≤* x≤x'' (nd≤* x≤x' x≤*l' x≤*r') (lemma-push-≤* t'' x≤y x≤*l'' x≤*r'' acc-t''yl''r'')
... | inj₂ x'≤y | inj₁ y≤x'' | _ rewrite lemma-≡-height t' y x' l' r' =
           let acc-t'yl'r' = rs (node t' y l' r') (lemma-≺-left t y (node t' x' l' r') (node t'' x'' l'' r''))
           in nd≤* x≤x' (lemma-push-≤* t' x≤y x≤*l' x≤*r' acc-t'yl'r') (nd≤* x≤x'' x≤*l'' x≤*r'')
... | inj₂ x'≤y | inj₂ x''≤y | inj₁ x'≤x'' rewrite lemma-≡-height t' y x' l' r' =
           let acc-t'yl'r' = rs (node t' y l' r') (lemma-≺-left t y (node t' x' l' r') (node t'' x'' l'' r''))
           in nd≤* x≤x' (lemma-push-≤* t' x≤y x≤*l' x≤*r' acc-t'yl'r') (nd≤* x≤x'' x≤*l'' x≤*r'')
... | inj₂ x'≤y | inj₂ x''≤y | inj₂ x''≤x' rewrite lemma-≡-height t'' y x'' l'' r'' =
           let acc-t''yl''r'' = rs (node t'' y l'' r'') (lemma-≺-right t y (node t' x' l' r') (node t'' x'' l'' r''))
           in nd≤* x≤x'' (nd≤* x≤x' x≤*l' x≤*r') (lemma-push-≤* t'' x≤y x≤*l'' x≤*r'' acc-t''yl''r'')

lemma-push-heap : {l r : PLRTree}(t : Tag)(x : A) → Heap l → Heap r → (acc : Acc _≺_ (node t x l r)) → Heap (push (node t x l r) acc)
lemma-push-heap t x leaf _ _ = node (lf≤* x) (lf≤* x) leaf leaf
lemma-push-heap t x (node {t'} {x'} x'≤*l' x'≤*r' hl' hr') leaf (acc rs)
    with tot≤ x x'
... | inj₁ x≤x' = node (nd≤* x≤x' (lf≤* x) (lf≤* x)) (lf≤* x) (node (lf≤* x') (lf≤* x') leaf leaf) leaf
... | inj₂ x'≤x = node (nd≤* x'≤x (lf≤* x') (lf≤* x')) (lf≤* x') (node (lf≤* x) (lf≤* x) leaf leaf) leaf
lemma-push-heap t x (node {t'} {x'} {l'} {r'} x'≤*l' x'≤*r' hl' hr') (node {t''} {x''} {l''} {r''} x''≤*l'' x''≤*r'' hl'' hr'') (acc rs)
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ =
           let x≤*t'x'l'r' = nd≤* x≤x' (lemma-≤-≤* x≤x' x'≤*l') (lemma-≤-≤* x≤x' x'≤*r') ;
                x≤*t''x''l''r'' = nd≤* x≤x'' (lemma-≤-≤* x≤x'' x''≤*l'') (lemma-≤-≤* x≤x'' x''≤*r'')
           in node x≤*t'x'l'r' x≤*t''x''l''r'' (node x'≤*l' x'≤*r' hl' hr') (node x''≤*l'' x''≤*r'' hl'' hr'')
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height t'' x x'' l'' r'' =
           let acc-t''xl''r'' = rs (node t'' x l'' r'') (lemma-≺-right t x (node t' x' l' r') (node t'' x'' l'' r'')) ;
                x''≤*t'x'l'r' = lemma-≤-≤* x''≤x (nd≤* x≤x' (lemma-≤-≤* x≤x' x'≤*l') (lemma-≤-≤* x≤x' x'≤*r')) ;
                x''≤*push-t''xl''r'' = lemma-push-≤* t'' x''≤x x''≤*l'' x''≤*r'' acc-t''xl''r''
           in node x''≤*t'x'l'r' x''≤*push-t''xl''r'' (node x'≤*l' x'≤*r' hl' hr') (lemma-push-heap t'' x hl'' hr'' acc-t''xl''r'')
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height t' x x' l' r' =
           let acc-t'xl'r' = rs (node t' x l' r') (lemma-≺-left t x (node t' x' l' r') (node t'' x'' l'' r'')) ;
                x'≤*t''x''l''r'' = lemma-≤-≤* x'≤x (nd≤* x≤x'' (lemma-≤-≤* x≤x'' x''≤*l'') (lemma-≤-≤* x≤x'' x''≤*r'')) ;
                x'≤*push-t'xl'r' = lemma-push-≤* t' x'≤x x'≤*l' x'≤*r' acc-t'xl'r'
           in node x'≤*push-t'xl'r' x'≤*t''x''l''r'' (lemma-push-heap t' x hl' hr' acc-t'xl'r') (node x''≤*l'' x''≤*r'' hl'' hr'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height t' x x' l' r' =
           let acc-t'xl'r' = rs (node t' x l' r') (lemma-≺-left t x (node t' x' l' r') (node t'' x'' l'' r'')) ;
                x'≤*t''x''l''r'' = lemma-≤-≤* x'≤x'' (nd≤* refl≤ x''≤*l'' x''≤*r'') ;
                x'≤*push-t'xl'r' = lemma-push-≤* t' x'≤x x'≤*l' x'≤*r' acc-t'xl'r'
           in node x'≤*push-t'xl'r' x'≤*t''x''l''r'' (lemma-push-heap t' x hl' hr' acc-t'xl'r') (node x''≤*l'' x''≤*r'' hl'' hr'')
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height t'' x x'' l'' r'' =
           let acc-t''xl''r'' = rs (node t'' x l'' r'') (lemma-≺-right t x (node t' x' l' r') (node t'' x'' l'' r'')) ;
                x''≤*t'x'l'r' = lemma-≤-≤* x''≤x' (nd≤* refl≤ x'≤*l' x'≤*r') ;
                x''≤*push-t''xl''r'' = lemma-push-≤* t'' x''≤x x''≤*l'' x''≤*r'' acc-t''xl''r''
           in node x''≤*t'x'l'r' x''≤*push-t''xl''r'' (node x'≤*l' x'≤*r' hl' hr') (lemma-push-heap t'' x hl'' hr'' acc-t''xl''r'')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --termination-depth=1 #-}
--{-# OPTIONS -v term:40 #-}

module TerminationWithInsufficientDepth where

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

module Depth2 where

  -- The fix to issue 59 makes this go through.
  -- f : Nat -> Nat
  -- f zero = zero
  -- f (suc zero) = zero
  -- f (suc (suc n)) with zero
  -- ... | m = f (suc n)

  -- Using a helper function, we still need termination-depth
  g : Nat → Nat → Nat
  f : Nat → Nat

  f zero = zero
  f (suc zero) = zero
  f (suc (suc n)) = g n zero

  g n m = f (suc n)

  {- this type checks with --termination-depth >= 2
  calls:

   f -> f_with (-2)
   f_with -> f (+1)

  -}

module Depth3 where

  f : Nat → Nat
  g : Nat → Nat

  f zero = zero
  f (suc zero) = zero
  f (suc (suc zero)) = zero
  f (suc (suc (suc n))) = g n

  g n = f (suc (suc n))