text:
------------------------------------------------------------------------
-- Pointed types and loop spaces
------------------------------------------------------------------------

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

-- Partly following the HoTT book.

open import Equality

module Pointed-type
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (_×_)

open import Bijection eq as B using (_↔_)
open import Equivalence eq as E using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level eq
open import Surjection eq using (_↠_)
open import Univalence-axiom eq

private
  variable
    a b ℓ : Level
    A B   : Type a
    x y   : A
    p q   : x ≡ y
    k     : Kind

------------------------------------------------------------------------
-- The definition of pointed types

-- Pointed types.

Pointed-type : ∀ ℓ → Type (lsuc ℓ)
Pointed-type a = ∃ λ (A : Type a) → A

------------------------------------------------------------------------
-- Based maps

-- Based maps (generalised to several kinds of underlying
-- "functions").

infix 4 _↝[_]ᴮ_ _→ᴮ_ _≃ᴮ_

_↝[_]ᴮ_ : Pointed-type a → Kind → Pointed-type b → Type (a ⊔ b)
(A , x) ↝[ k ]ᴮ (B , y) =
  ∃ λ (f : A ↝[ k ] B) → to-implication f x ≡ y

-- Based maps.

_→ᴮ_ : Pointed-type a → Pointed-type b → Type (a ⊔ b)
_→ᴮ_ = _↝[ implication ]ᴮ_

-- Based equivalences.

_≃ᴮ_ : Pointed-type a → Pointed-type b → Type (a ⊔ b)
_≃ᴮ_ = _↝[ equivalence ]ᴮ_

private
  variable
    P P₁ P₂ Q Q₁ Q₂ R : Pointed-type a
    P→Q               : P →ᴮ Q
    P≃Q               : P ≃ᴮ Q

-- Based equivalences can be converted to based maps.

≃ᴮ→→ᴮ : P ≃ᴮ Q → P →ᴮ Q
≃ᴮ→→ᴮ = Σ-map _≃_.to id

-- Based equivalences are equivalent to equalities (assuming
-- univalence).

≃ᴮ≃≡ : {P Q : Pointed-type a} → Univalence a → (P ≃ᴮ Q) ≃ (P ≡ Q)
≃ᴮ≃≡ {P = A , x} {Q = B , y} univ =
  (∃ λ (A≃B : A ≃ B) → _≃_.to A≃B x ≡ y)    ↝⟨ (inverse $
                                                Σ-cong (≡≃≃ univ) λ A≃B →
                                                ≡⇒≃ $ cong (_≡ _) $
                                                subst-id-in-terms-of-≡⇒↝ equivalence) ⟩
  (∃ λ (A≡B : A ≡ B) → subst id A≡B x ≡ y)  ↔⟨ B.Σ-≡,≡↔≡ ⟩□
  (A , x) ≡ (B , y)                         □

-- _↝[ k ]ᴮ_ is reflexive.

↝ᴮ-refl : P ↝[ k ]ᴮ P
↝ᴮ-refl {k = k} = F.id , cong (_$ _) (to-implication-id k)

-- _↝[ k ]ᴮ_ is transitive.

↝ᴮ-trans : P ↝[ k ]ᴮ Q → Q ↝[ k ]ᴮ R → P ↝[ k ]ᴮ R
↝ᴮ-trans {P = _ , x} {k = k} {Q = _ , y} {R = _ , z}
  (A↝B , p) (B↝C , q) =
    B↝C F.∘ A↝B
  , (to-implication (B↝C F.∘ A↝B) x             ≡⟨ cong (_$ _) $ to-implication-∘ k ⟩
     to-implication B↝C (to-implication A↝B x)  ≡⟨ cong (to-implication B↝C) p ⟩
     to-implication B↝C y                       ≡⟨ q ⟩∎
     z                                          ∎)

-- _≃ᴮ_ is symmetric.

≃ᴮ-sym : P ≃ᴮ Q → Q ≃ᴮ P
≃ᴮ-sym (A≃B , p) = inverse A≃B , _≃_.to-from A≃B p

-- "Equational" reasoning combinators.

infix  -1 _□ᴮ finallyᴮ
infixr -2 stepᴮ

-- For an explanation of why stepᴮ is defined in this way, see
-- Equality.step-≡.

stepᴮ : (P : Pointed-type a) {Q : Pointed-type b} →
        Q ↝[ k ]ᴮ R → P ↝[ k ]ᴮ Q → P ↝[ k ]ᴮ R
stepᴮ _ = flip ↝ᴮ-trans

syntax stepᴮ P Q↝R P↝Q = P ↝ᴮ⟨ P↝Q ⟩ Q↝R

finallyᴮ :
  (P : Pointed-type a) (Q : Pointed-type b) →
  P ↝[ k ]ᴮ Q → P ↝[ k ]ᴮ Q
finallyᴮ _ _ P↝Q = P↝Q

syntax finallyᴮ P Q P↝Q = P ↝ᴮ⟨ P↝Q ⟩□ Q □

_□ᴮ : (P : Pointed-type a) → P ↝[ k ]ᴮ P
_ □ᴮ = ↝ᴮ-refl

-- There is a split surjection from based maps from
-- (Maybe A , nothing) to functions.

Maybe→ᴮ↠→ : (Maybe A , nothing) →ᴮ (B , x) ↠ (A → B)
Maybe→ᴮ↠→ {A = A} {B = B} {x = x} = record
  { logical-equivalence = record
    { to   = (Maybe A , nothing) →ᴮ (B , x)  ↝⟨ proj₁ ⟩
             (Maybe A → B)                   ↝⟨ _∘ inj₂ ⟩□
             (A → B)                         □
    ; from = λ f → [ (λ _ → x) , f ] , refl x
    }
  ; right-inverse-of = refl
  }

-- Based maps from (Maybe A , nothing) are isomorphic to functions
-- (assuming extensionality).

Maybe→ᴮ↔→ :
  ∀ {A : Type a} {B : Type b} {x} →
  (Maybe A , nothing) →ᴮ (B , x) ↝[ a ∣ b ] (A → B)
Maybe→ᴮ↔→ {A = A} {B} {x} = generalise-ext?
  (_↠_.logical-equivalence Maybe→ᴮ↠→)
  (λ ext →
       refl
     , (λ (f , eq) → Σ-≡,≡→≡
          (apply-ext (E.good-ext ext)
             [ (λ _ →
                  x          ≡⟨ sym eq ⟩∎
                  f nothing  ∎)
             , (λ _ → refl _)
             ])
          (subst (λ f → f nothing ≡ x)
                 (apply-ext (E.good-ext ext)
                    [ (λ _ → sym eq) , (λ _ → refl _) ])
                 (refl x)                                 ≡⟨ E.subst-good-ext ext _ _ ⟩

           subst (_≡ x) (sym eq) (refl x)                 ≡⟨ subst-trans _ ⟩

           trans eq (refl x)                              ≡⟨ trans-reflʳ _ ⟩∎

           eq                                             ∎)))

-- A corollary.

Bool→ᴮ↔ :
  ∀ {A : Type a} {x} →
  (Bool , true) →ᴮ (A , x) ↝[ lzero ∣ a ] A
Bool→ᴮ↔ {A = A} {x = x} ext =
  (Bool , true) →ᴮ (A , x)  ↝⟨ Maybe→ᴮ↔→ ext ⟩
  (⊤ → A)                   ↔⟨ Π-left-identity ⟩□
  A                         □

------------------------------------------------------------------------
-- Loop spaces

-- The loop space of a pointed type.

Ω : Pointed-type ℓ → Pointed-type ℓ
Ω (A , x) = (x ≡ x) , refl x

-- Iterated loop spaces.
--
-- The HoTT book uses Ω[ n ] ∘ Ω rather than Ω ∘ Ω[ n ]. I prefer
-- the following definition, because with the other definition the
-- type of Equality.Groupoid.Ω[2+n]-commutative would not be
-- well-formed. (See also Ω∘Ω[]≡Ω[]∘Ω.)

Ω[_] : ℕ → Pointed-type ℓ → Pointed-type ℓ
Ω[ zero  ] = id
Ω[ suc n ] = Ω ∘ Ω[ n ]

-- A rearrangement lemma for Ω and Ω[_].

Ω∘Ω[]≡Ω[]∘Ω : ∀ n → Ω (Ω[ n ] P) ≡ Ω[ n ] (Ω P)
Ω∘Ω[]≡Ω[]∘Ω {P = P} zero =
  Ω P  ∎
Ω∘Ω[]≡Ω[]∘Ω {P = P} (suc n) =
  Ω (Ω[ suc n ] P)  ≡⟨⟩
  Ω (Ω (Ω[ n ] P))  ≡⟨ cong Ω $ Ω∘Ω[]≡Ω[]∘Ω n ⟩
  Ω (Ω[ n ] (Ω P))  ≡⟨⟩
  Ω[ suc n ] (Ω P)  ∎

-- Ω preserves based maps.

Ω-cong-→ᴮ : P →ᴮ Q → Ω P →ᴮ Ω Q
Ω-cong-→ᴮ {P = A , x} {Q = B , y} (to , to≡) =
    (x ≡ x        ↝⟨ cong to ⟩
     to x ≡ to x  ↔⟨ ≡⇒≃ $ cong₂ _≡_ to≡ to≡ ⟩□
     y ≡ y        □)
  , (≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to (refl x))      ≡⟨ cong (≡⇒→ (cong₂ _≡_ to≡ to≡)) $ cong-refl _ ⟩
     ≡⇒→ (cong₂ _≡_ to≡ to≡) (refl (to x))           ≡⟨ elim¹
                                                          (λ to≡ → ≡⇒→ (cong₂ _≡_ to≡ to≡) (refl (to x)) ≡
                                                                   refl _)
                                                          (
         ≡⇒→ (cong₂ _≡_ (refl _) (refl _)) (refl _)        ≡⟨ cong (λ eq → ≡⇒→ eq (refl _)) $ cong₂-refl _≡_ ⟩
         ≡⇒→ (refl _) (refl _)                             ≡⟨ cong (λ eq → _≃_.to eq (refl _)) ≡⇒↝-refl ⟩∎
         refl _                                                       ∎)
                                                          _ ⟩∎
     refl y                                          ∎)

-- Ω preserves based equivalences.

Ω-cong-≃ᴮ : P ≃ᴮ Q → Ω P ≃ᴮ Ω Q
Ω-cong-≃ᴮ {P = A , x} {Q = B , y} (A≃B , to≡) =
    (x ≡ x                        ↝⟨ inverse $ E.≃-≡ A≃B ⟩
     _≃_.to A≃B x ≡ _≃_.to A≃B x  ↝⟨ ≡⇒↝ _ $ cong₂ _≡_ to≡ to≡ ⟩□
     y ≡ y                        □)
  , proj₂ (Ω-cong-→ᴮ (_≃_.to A≃B , to≡))

-- Ω[ n ] preserves based maps.

Ω[_]-cong-→ᴮ : ∀ n → P →ᴮ Q → Ω[ n ] P →ᴮ Ω[ n ] Q
Ω[ zero  ]-cong-→ᴮ A→B = A→B
Ω[ suc n ]-cong-→ᴮ A→B = Ω-cong-→ᴮ (Ω[ n ]-cong-→ᴮ A→B)

-- Ω[ n ] preserves based equivalences.

Ω[_]-cong-≃ᴮ : ∀ n → P ≃ᴮ Q → Ω[ n ] P ≃ᴮ Ω[ n ] Q
Ω[ zero  ]-cong-≃ᴮ A≃B = A≃B
Ω[ suc n ]-cong-≃ᴮ A≃B = Ω-cong-≃ᴮ (Ω[ n ]-cong-≃ᴮ A≃B)

-- ≃ᴮ→→ᴮ commutes with Ω-cong-≃ᴮ/Ω-cong-→ᴮ.

≃ᴮ→→ᴮ-Ω-cong-≃ᴮ :
  (P≃Q : P ≃ᴮ Q) →
  ≃ᴮ→→ᴮ (Ω-cong-≃ᴮ P≃Q) ≡ Ω-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q)
≃ᴮ→→ᴮ-Ω-cong-≃ᴮ _ = refl _

-- ≃ᴮ→→ᴮ commutes with Ω[ n ]-cong-≃ᴮ/Ω[ n ]-cong-→ᴮ.

≃ᴮ→→ᴮ-Ω[_]-cong-≃ᴮ :
  ∀ n →
  ≃ᴮ→→ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q) ≡
  Ω[ n ]-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q)
≃ᴮ→→ᴮ-Ω[_]-cong-≃ᴮ {P≃Q = P≃Q} = λ where
  zero    → refl _
  (suc n) →
    ≃ᴮ→→ᴮ (Ω-cong-≃ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q))  ≡⟨⟩
    Ω-cong-→ᴮ (≃ᴮ→→ᴮ (Ω[ n ]-cong-≃ᴮ P≃Q))  ≡⟨ cong Ω-cong-→ᴮ ≃ᴮ→→ᴮ-Ω[ n ]-cong-≃ᴮ ⟩
    Ω-cong-→ᴮ (Ω[ n ]-cong-→ᴮ (≃ᴮ→→ᴮ P≃Q))  ∎

-- A lemma relating Ω-cong-→ᴮ and ↝ᴮ-refl.

proj₁-Ω-cong-→ᴮ-↝ᴮ-refl :
  proj₁ (Ω-cong-→ᴮ ↝ᴮ-refl) p ≡ p
proj₁-Ω-cong-→ᴮ-↝ᴮ-refl {p = p} =
  ≡⇒→
    (cong₂ _≡_
       (cong (_$ _) (refl _))
       (cong (_$ _) (refl _)))
    (cong id p)                 ≡⟨ cong₂ ≡⇒→
                                     (trans (cong₂ (cong₂ _≡_)
                                               (cong-refl _)
                                               (cong-refl _)) $
                                      cong₂-refl _≡_)
                                     (sym $ cong-id _) ⟩

  ≡⇒→ (refl _) p                ≡⟨ cong (_$ _) ≡⇒→-refl ⟩∎

  p                             ∎

-- A lemma relating Ω-cong-≃ᴮ and ↝ᴮ-refl.

proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl :
  _≃_.to (proj₁ (Ω-cong-≃ᴮ ↝ᴮ-refl)) p ≡ p
proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl = proj₁-Ω-cong-→ᴮ-↝ᴮ-refl

-- A lemma relating Ω-cong-→ᴮ and trans.

Ω-cong-→ᴮ-trans :
  proj₁ (Ω-cong-→ᴮ P→Q) (trans p q) ≡
  trans (proj₁ (Ω-cong-→ᴮ P→Q) p)
        (proj₁ (Ω-cong-→ᴮ P→Q) q)
Ω-cong-→ᴮ-trans {P→Q = to , to≡} {p = p} {q = q} =
  ≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to (trans p q))            ≡⟨ cong (≡⇒→ (cong₂ _≡_ to≡ to≡)) $
                                                              cong-trans _ _ _ ⟩
  ≡⇒→ (cong₂ _≡_ to≡ to≡)
    (trans (cong to p) (cong to q))                        ≡⟨ lemma _ ⟩

  trans
    (trans (sym to≡)
       (trans (cong to p) (cong to q)))
    to≡                                                    ≡⟨ trans (cong (flip trans _) $ sym $ trans-assoc _ _ _) $
                                                              trans-assoc _ _ _ ⟩
  trans
    (trans (sym to≡) (cong to p))
    (trans (cong to q) to≡)                                ≡⟨ cong (trans _) $ sym $
                                                              trans--[trans-sym] _ _ ⟩
  trans (trans (sym to≡) (cong to p))
    (trans to≡ (trans (sym to≡) (trans (cong to q) to≡)))  ≡⟨ trans (cong (trans _) $ cong (trans _) $ sym $ trans-assoc _ _ _) $
                                                              sym $ trans-assoc _ _ _ ⟩
  trans
    (trans (trans (sym to≡) (cong to p)) to≡)
    (trans (trans (sym to≡) (cong to q)) to≡)              ≡⟨ sym $ cong₂ trans (lemma _) (lemma _) ⟩∎

  trans
    (≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to p))
    (≡⇒→ (cong₂ _≡_ to≡ to≡) (cong to q))                  ∎
  where
  lemma = λ p →
    ≡⇒→ (cong₂ _≡_ to≡ to≡) p                          ≡⟨⟩
    ≡⇒→ (trans (cong (_≡ _) to≡) (cong (_ ≡_) to≡)) p  ≡⟨ cong (_$ p) $ ≡⇒↝-trans equivalence ⟩
    ≡⇒→ (cong (_ ≡_) to≡) (≡⇒→ (cong (_≡ _) to≡) p)    ≡⟨ sym $ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
    subst (_ ≡_) to≡ (≡⇒→ (cong (_≡ _) to≡) p)         ≡⟨ sym trans-subst ⟩
    trans (≡⇒→ (cong (_≡ _) to≡) p) to≡                ≡⟨ cong (flip trans _) $ sym $ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
    trans (subst (_≡ _) to≡ p) to≡                     ≡⟨ cong (flip trans _) subst-trans-sym ⟩∎
    trans (trans (sym to≡) p) to≡                      ∎

-- A lemma relating Ω-cong-≃ᴮ and trans.

Ω-cong-≃ᴮ-trans :
  (P≃Q : P ≃ᴮ Q) →
  _≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) (trans p q) ≡
  trans (_≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) p)
        (_≃_.to (proj₁ (Ω-cong-≃ᴮ P≃Q)) q)
Ω-cong-≃ᴮ-trans _ = Ω-cong-→ᴮ-trans

-- A lemma relating Ω[_]-cong-→ᴮ and trans.

Ω[1+_]-cong-→ᴮ-trans :
  ∀ n {p q} →
  proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) (trans p q) ≡
  trans (proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) p)
        (proj₁ (Ω[ 1 + n ]-cong-→ᴮ P→Q) q)
Ω[1+ _ ]-cong-→ᴮ-trans = Ω-cong-→ᴮ-trans

-- A lemma relating Ω[_]-cong-≃ᴮ and trans.

Ω[1+_]-cong-≃ᴮ-trans :
  ∀ n {p q} (P≃Q : P ≃ᴮ Q) →
  _≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) (trans p q) ≡
  trans (_≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) p)
        (_≃_.to (proj₁ (Ω[ 1 + n ]-cong-≃ᴮ P≃Q)) q)
Ω[1+ n ]-cong-≃ᴮ-trans P≃Q = Ω-cong-≃ᴮ-trans (Ω[ n ]-cong-≃ᴮ P≃Q)

-- A has h-level 1 + n iff the iterated loop space Ω[ n ] (A , x) is
-- contractible for every x : A.

+⇔∀contractible-Ω[] :
  ∀ n →
  H-level (1 + n) A
    ⇔
  ((x : A) → Contractible (proj₁ $ Ω[ n ] (A , x)))
+⇔∀contractible-Ω[] {A = A} zero =
  Is-proposition A      ↝⟨ record { to   = propositional⇒inhabited⇒contractible
                                  ; from = [inhabited⇒contractible]⇒propositional
                                  } ⟩□
  (A → Contractible A)  □

+⇔∀contractible-Ω[] {A = A} (suc zero) =
  Is-set A                            ↝⟨ 2+⇔∀1+≡ 0 ⟩
  ((x : A) → Is-proposition (x ≡ x))  ↝⟨ (∀-cong _ λ x → record { to   = flip propositional⇒inhabited⇒contractible (refl x)
                                                                ; from = mono₁ 0
                                                                }) ⟩□
  ((x : A) → Contractible (x ≡ x))    □

+⇔∀contractible-Ω[] {A = A} (suc (suc n)) =
  H-level (3 + n) A                                                  ↝⟨ 2+⇔∀1+≡ (1 + n) ⟩

  ((x : A) → H-level (2 + n) (x ≡ x))                                ↝⟨ (∀-cong _ λ _ → +⇔∀contractible-Ω[] (suc n)) ⟩

  ((x : A) (p : x ≡ x) →
   Contractible (proj₁ $ Ω[ 1 + n ] ((x ≡ x) , p)))                  ↝⟨ (∀-cong _ λ _ → ∀-cong _ λ _ → H-level-cong _ _ $ proj₁ $
                                                                         Ω[ 1 + n ]-cong-≃ᴮ $ lemma _) ⟩

  ((x : A) → x ≡ x → Contractible (proj₁ $ Ω[ 1 + n ] (Ω (A , x))))  ↝⟨ (∀-cong _ λ x → _↠_.logical-equivalence $ inhabited→↠ (refl x)) ⟩

  ((x : A) → Contractible (proj₁ $ Ω[ 1 + n ] (Ω (A , x))))          ↝⟨ (∀-cong _ λ _ → ≡⇒↝ _ $ cong (Contractible ∘ proj₁) $ sym $
                                                                         Ω∘Ω[]≡Ω[]∘Ω (1 + n)) ⟩□
  ((x : A) → Contractible (proj₁ $ Ω[ 2 + n ] (A , x)))              □
  where
  lemma : (p : x ≡ x) → ((x ≡ x) , p) ≃ᴮ Ω (A , x)
  lemma p = E.↔⇒≃ (inverse $ flip-trans-isomorphism p)
          , (trans p (sym p)  ≡⟨ trans-symʳ _ ⟩∎
             refl _           ∎)

------------------------------------------------------------------------
-- Products

-- The product of two pointed types.

infixr 2 _×_

_×_ : Pointed-type a → Pointed-type b → Pointed-type (a ⊔ b)
(A , x) × (B , y) = (A P.× B) , (x , y)

-- The first projection.

proj₁ᴾ : (P × Q) →ᴮ P
proj₁ᴾ = proj₁ , refl _

-- The second projection.

proj₂ᴾ : (P × Q) →ᴮ Q
proj₂ᴾ = proj₂ , refl _

-- The operator _×_ preserves based maps and equivalences.

infixr 2 _×-cong-→ᴮ_ _×-cong-≃ᴮ_

_×-cong-→ᴮ_ : P₁ →ᴮ P₂ → Q₁ →ᴮ Q₂ → (P₁ × Q₁) →ᴮ (P₂ × Q₂)
(f₁ , eq₁) ×-cong-→ᴮ (f₂ , eq₂) =
    (f₁ ×-cong f₂)
  , cong₂ _,_ eq₁ eq₂

_×-cong-≃ᴮ_ : P₁ ≃ᴮ P₂ → Q₁ ≃ᴮ Q₂ → (P₁ × Q₁) ≃ᴮ (P₂ × Q₂)
(f₁ , eq₁) ×-cong-≃ᴮ (f₂ , eq₂) =
    (f₁ ×-cong f₂)
  , cong₂ _,_ eq₁ eq₂

-- Ω commutes with _×_.

Ω-× : Ω (P × Q) ≃ᴮ (Ω P × Ω Q)
Ω-× {P = A , x} {Q = B , y} =
    ((x , y) ≡ (x , y)  ↝⟨ E.↔⇒≃ (inverse ≡×≡↔≡) ⟩□
     x ≡ x P.× y ≡ y    □)
  , ((cong proj₁ (refl (x , y)) , cong proj₂ (refl (x , y)))  ≡⟨ cong₂ _,_ (cong-refl _) (cong-refl _) ⟩∎
     (refl x , refl y)                                        ∎)

-- Ω[ n ] commutes with _×_.

Ω[_]-× : ∀ n → Ω[ n ] (P × Q) ≃ᴮ (Ω[ n ] P × Ω[ n ] Q)
Ω[_]-× {P = P} {Q = Q} = λ where
  zero    → P × Q  □ᴮ
  (suc n) →
    Ω (Ω[ n ] (P × Q))           ↝ᴮ⟨ Ω-cong-≃ᴮ Ω[ n ]-× ⟩
    Ω (Ω[ n ] P × Ω[ n ] Q)      ↝ᴮ⟨ Ω-× ⟩□
    Ω (Ω[ n ] P) × Ω (Ω[ n ] Q)  □

-- A lemma relating Ω[ 1 ]-× and Ω-×.

Ω[1]-× : _≃_.to (proj₁ Ω[ 1 ]-×) p ≡ _≃_.to (proj₁ Ω-×) p
Ω[1]-× {p = p} =
  _≃_.to (proj₁ Ω[ 1 ]-×) p                                  ≡⟨⟩
  _≃_.to (proj₁ Ω-×) (_≃_.to (proj₁ (Ω-cong-≃ᴮ ↝ᴮ-refl)) p)  ≡⟨ cong (_≃_.to (proj₁ Ω-×)) proj₁-Ω-cong-≃ᴮ-↝ᴮ-refl ⟩∎
  _≃_.to (proj₁ Ω-×) p                                       ∎

-- A lemma relating Ω-× and trans.

Ω-×-trans :
  _≃_.to (proj₁ Ω-×) (trans p q) ≡
  Σ-zip trans trans
    (_≃_.to (proj₁ Ω-×) p)
    (_≃_.to (proj₁ Ω-×) q)
Ω-×-trans {p = p} {q = q} =
  _≃_.to (proj₁ Ω-×) (trans p q)         ≡⟨⟩

  ( cong proj₁ (trans p q)
  , cong proj₂ (trans p q)
  )                                      ≡⟨ cong₂ _,_
                                              (cong-trans _ _ _)
                                              (cong-trans _ _ _) ⟩
  ( trans (cong proj₁ p) (cong proj₁ q)
  , trans (cong proj₂ p) (cong proj₂ q)
  )                                      ≡⟨⟩

  Σ-zip trans trans
    (_≃_.to (proj₁ Ω-×) p)
    (_≃_.to (proj₁ Ω-×) q)               ∎

-- A lemma relating Ω[_]-× and trans.

Ω[1+_]-×-trans :
  ∀ n {p q : proj₁ (Ω[ suc n ] (P × Q))} →
  _≃_.to (proj₁ Ω[ suc n ]-×) (trans p q) ≡
  Σ-zip trans trans
    (_≃_.to (proj₁ Ω[ suc n ]-×) p)
    (_≃_.to (proj₁ Ω[ suc n ]-×) q)
Ω[1+ n ]-×-trans {p = p} {q = q} =
  _≃_.to (proj₁ Ω-×)
    (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) (trans p q))  ≡⟨ cong (_≃_.to (proj₁ Ω-×)) $ Ω-cong-≃ᴮ-trans Ω[ n ]-× ⟩

  _≃_.to (proj₁ Ω-×)
    (trans (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) p)
           (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) q))    ≡⟨ Ω-×-trans ⟩∎

  Σ-zip trans trans
    (_≃_.to (proj₁ Ω-×)
       (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) p))
    (_≃_.to (proj₁ Ω-×)
       (_≃_.to (proj₁ (Ω-cong-≃ᴮ Ω[ n ]-×)) q))        ∎


text:
------------------------------------------------------------------------
-- Parser indices
------------------------------------------------------------------------

module RecursiveDescent.Index where

open import Data.Bool
open import Data.Product.Record
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Function

------------------------------------------------------------------------
-- Indices to the parser type

-- Does the parser accept empty strings?

Empty : Set
Empty = Bool

-- The proper left corners of the parser, represented as a tree. See
-- the definition of RecursiveDescent.(Coi|I)nductive.Internal.Parser.

data Corners : Set where
  leaf : Corners
  step : Corners -> Corners
  node : Corners -> Corners -> Corners

Index : Set
Index = Empty × Corners

-- The parser type signature. The second argument is the result type.

ParserType : Set1
ParserType = Index -> Set -> Set

ParserType₁ : Set2
ParserType₁ = Index -> Set -> Set1

------------------------------------------------------------------------
-- Operations on indices

infixr 50 _·I_
infixr 40 _∣I_

0I : Index
0I = (false , leaf)

1I : Index
1I = (true , leaf)

_∣I_ : Index -> Index -> Index
i₁ ∣I i₂ = (proj₁ i₁ ∨ proj₁ i₂ , node (proj₂ i₁) (proj₂ i₂))

_·I_ : Index -> Index -> Index
i₁ ·I i₂ = ( proj₁ i₁ ∧ proj₁ i₂
           , (if proj₁ i₁ then node (proj₂ i₁) (proj₂ i₂)
                          else step (proj₂ i₁))
           )

------------------------------------------------------------------------
-- Testing indices for equality

infix 15 _Index-≟_ _Corners-≟_

private

  drop-step : forall {c₁ c₂} -> step c₁ ≡ step c₂ -> c₁ ≡ c₂
  drop-step refl = refl

  drop-node₁ : forall {c₁ c₂ c₃ c₄} ->
               node c₁ c₂ ≡ node c₃ c₄ -> c₁ ≡ c₃
  drop-node₁ refl = refl

  drop-node₂ : forall {c₁ c₂ c₃ c₄} ->
               node c₁ c₂ ≡ node c₃ c₄ -> c₂ ≡ c₄
  drop-node₂ refl = refl

_Corners-≟_ : Decidable {Corners} _≡_
leaf       Corners-≟ leaf         = yes refl
step c₁    Corners-≟ step  c₂     with c₁ Corners-≟ c₂
step c₁    Corners-≟ step .c₁     | yes refl   = yes refl
step c₁    Corners-≟ step  c₂     | no  ¬c₁≡c₂ = no (¬c₁≡c₂ ∘ drop-step)
node c₁ c₂ Corners-≟ node  c₃  c₄ with c₁ Corners-≟ c₃ | c₂ Corners-≟ c₄
node c₁ c₂ Corners-≟ node .c₁ .c₂ | yes refl   | yes refl = yes refl
node c₁ c₂ Corners-≟ node  c₃  c₄ | no  ¬c₁≡c₂ | _          = no (¬c₁≡c₂ ∘ drop-node₁)
node c₁ c₂ Corners-≟ node  c₃  c₄ | _          | no  ¬c₁≡c₂ = no (¬c₁≡c₂ ∘ drop-node₂)
leaf       Corners-≟ step _       = no \()
leaf       Corners-≟ node _ _     = no \()
step _     Corners-≟ leaf         = no \()
step _     Corners-≟ node _ _     = no \()
node _ _   Corners-≟ leaf         = no \()
node _ _   Corners-≟ step _       = no \()

_Index-≟_ : Decidable {Index} _≡_
i₁ Index-≟ i₂ with proj₁ i₁ ≟ proj₁ i₂
                 | proj₂ i₁ Corners-≟ proj₂ i₂
... | yes e₁≡e₂ | yes c₁≡c₂ = yes (cong₂ (_,_) e₁≡e₂ c₁≡c₂)
... | no ¬e₁≡e₂ | _         = no (¬e₁≡e₂ ∘ cong proj₁)
... | _         | no ¬c₁≡c₂ = no (¬c₁≡c₂ ∘ cong proj₂)

ext: agda

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Agda.Primitive
open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules

{- Decidability of type cheking for the type theory for globular sets -}
module GSeTT.Dec-Type-Checking where

  dec-⊢C : ∀ Γ → dec (Γ ⊢C)
  dec-⊢T : ∀ Γ A → dec (Γ ⊢T A)
  dec-⊢t : ∀ Γ A t → dec (Γ ⊢t t # A)
  dec-⊢S : ∀ Δ Γ γ → dec (Δ ⊢S γ > Γ)

  private
    Γ+⊢→Γ⊢ : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → Γ ⊢C
    Γ+⊢→Γ⊢ (cc Γ⊢ _ idp) = Γ⊢

    Γ+⊢→x=l : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → x == length Γ
    Γ+⊢→x=l (cc _ _ idp) = idp

    Γ+⊢→Γ⊢A : ∀ {Γ x A} → (Γ :: (x , A)) ⊢C → Γ ⊢T A
    Γ+⊢→Γ⊢A (cc _ Γ⊢A _) = Γ⊢A

    Γ⊢t⇒u→Γ⊢A : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢T A
    Γ⊢t⇒u→Γ⊢A (ar Γ⊢t:A Γ⊢u:A) = Γ⊢t:A→Γ⊢A Γ⊢t:A

    Γ⊢t⇒u→Γ⊢t : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t t # A
    Γ⊢t⇒u→Γ⊢t (ar Γ⊢t:A Γ⊢u:A) = Γ⊢t:A

    Γ⊢t⇒u→Γ⊢u : ∀ {Γ A t u} → Γ ⊢T ⇒ A t u → Γ ⊢t u # A
    Γ⊢t⇒u→Γ⊢u (ar Γ⊢t:A Γ⊢u:A) = Γ⊢u:A

    Γ⊢x:A→x∈Γ : ∀ {Γ x A} → Γ ⊢t Var x # A → x # A ∈ Γ
    Γ⊢x:A→x∈Γ (var _ x∈Γ) = x∈Γ

    Δ⊢<>:Γ→Γ=nil : ∀ {Δ Γ} → Δ ⊢S nil > Γ → Γ == nil
    Δ⊢<>:Γ→Γ=nil (es _) = idp

    Δ⊢γ:⊘→γ=nil : ∀ {Δ γ} → Δ ⊢S γ > nil → γ == nil
    Δ⊢γ:⊘→γ=nil (es _) = idp

    Δ⊢γ+:Γ+→x=y : ∀ {Δ Γ x A γ y t} → Δ ⊢S (γ :: (y , t)) > (Γ :: (x , A)) → x == y
    Δ⊢γ+:Γ+→x=y (sc _ _ _ idp) = idp

    Δ⊢γ+:Γ+→Δ⊢t : ∀ {Δ Γ x A γ y t} → Δ ⊢S (γ :: (y , t)) > (Γ :: (x , A)) → Δ ⊢t t # (A [ γ ]Pre-Ty)
    Δ⊢γ+:Γ+→Δ⊢t (sc _ _ Δ⊢t idp) = Δ⊢t

    Δ⊢γ+:Γ+→Δ⊢γ : ∀ {Δ Γ x A γ y t} → Δ ⊢S (γ :: (y , t)) > (Γ :: (x , A)) → Δ ⊢S γ > Γ
    Δ⊢γ+:Γ+→Δ⊢γ (sc Δ⊢γ:Γ _ _ idp) = Δ⊢γ:Γ

  eqdec-Ty : eqdec Pre-Ty
  eqdec-Tm : eqdec Pre-Tm

  eqdec-Ty ∗ ∗ = inl idp
  eqdec-Ty ∗ (⇒ _ _ _) = inr λ{()}
  eqdec-Ty (⇒ _ _ _) ∗ = inr λ{()}
  eqdec-Ty (⇒ A t u) (⇒ B t' u') with eqdec-Ty A B | eqdec-Tm t t' | eqdec-Tm u u'
  ...                                      | inl idp       | inl idp       | inl idp      = inl idp
  ...                                      | inl idp       | inl idp       | inr u≠u'     = inr λ p → u≠u' (snd (=⇒ p))
  ...                                      | inl idp       | inr t≠t'      | _            = inr λ p → t≠t' (snd (fst (=⇒ p)))
  ...                                      | inr A≠B       | _             | _            = inr λ p → A≠B (fst (fst (=⇒ p)))
  eqdec-Tm (Var x) (Var y) with eqdecℕ x y
  ...                               | inl idp = inl idp
  ...                               | inr x≠y = inr λ p → x≠y (=Var p)

  dec-∈ : ∀ Γ x A → dec (x # A ∈ Γ)
  dec-∈ nil x A = inr λ x → x
  dec-∈ (Γ :: (y , B)) x A with (eqdecℕ y x) | (eqdec-Ty B A)
  ...                       | inl idp         | inl idp = inl (inr (idp , idp))
  ...                       | inl idp         | inr B≠A       with dec-∈ Γ x A
  ...                                                         | inl x∈Γ = inl (inl x∈Γ)
  ...                                                         | inr x∉Γ = inr λ {(inl x∈Γ) → x∉Γ x∈Γ ; (inr (_ , A=B)) → B≠A (A=B ^)}
  dec-∈ (Γ :: (y , B)) x A | inr y≠x         | _   with dec-∈ Γ x A
  ...                                               | inl x∈Γ = inl (inl x∈Γ)
  ...                                               | inr x∉Γ = inr λ{ (inl x∈Γ) → x∉Γ x∈Γ ; (inr (x=y , _)) → y≠x (x=y ^)}

  dec-⊢C nil = inl ec
  dec-⊢C (Γ :: (x , A)) with dec-⊢C Γ | eqdecℕ x (length Γ) | dec-⊢T Γ A
  ...                        | inl Γ⊢ | inl idp              | inl Γ⊢A      = inl (cc Γ⊢ Γ⊢A idp)
  ...                        | inl  _ | inl idp              | inr Γ⊬A      = inr λ Γ+⊢ → Γ⊬A (Γ+⊢→Γ⊢A Γ+⊢)
  ...                        | inl Γ⊢ | inr n≠l              | _            = inr λ Γ+⊢ → n≠l (Γ+⊢→x=l Γ+⊢)
  ...                        | inr Γ⊬ | _                    | _            = inr λ Γ+⊢ → Γ⊬ (Γ+⊢→Γ⊢ Γ+⊢)
  dec-⊢T Γ ∗ with dec-⊢C Γ
  ...             | inl Γ⊢ = inl (ob Γ⊢)
  ...             | inr Γ⊬ = inr λ Γ⊢* → Γ⊬ (Γ⊢A→Γ⊢ Γ⊢*)
  dec-⊢T Γ (⇒ A t u) with dec-⊢t Γ A t | dec-⊢t Γ A u
  ...                     | inl Γ⊢t:A    | inl Γ⊢u:A = inl (ar Γ⊢t:A Γ⊢u:A)
  ...                     | inl _        | inr Γ⊬u:A = inr λ Γ⊢t⇒u → Γ⊬u:A (Γ⊢t⇒u→Γ⊢u Γ⊢t⇒u)
  ...                     | inr Γ⊬t:A    | _         = inr λ Γ⊢t⇒u → Γ⊬t:A (Γ⊢t⇒u→Γ⊢t Γ⊢t⇒u)

  dec-⊢t Γ A (Var x) with dec-⊢C Γ       | dec-∈ Γ x A
  ...                     | inl Γ⊢          | inl x∈Γ      = inl (var Γ⊢ x∈Γ)
  ...                     | inl _           | inr x∉Γ      = inr λ Γ⊢x:A → x∉Γ (Γ⊢x:A→x∈Γ Γ⊢x:A)
  ...                     | inr Γ⊬          | _            = inr λ Γ⊢x:A → Γ⊬ (Γ⊢t:A→Γ⊢ Γ⊢x:A)
  dec-⊢S Δ nil nil with dec-⊢C Δ
  ...              | inl Δ⊢ = inl (es Δ⊢)
  ...              | inr Δ⊬ = inr λ Δ⊢<>:⊘ → Δ⊬ (Δ⊢γ:Γ→Δ⊢ Δ⊢<>:⊘)
  dec-⊢S Δ (Γ :: _) nil = inr λ Δ⊢<>:Γ → cons≠nil (Δ⊢<>:Γ→Γ=nil Δ⊢<>:Γ)
  dec-⊢S Δ nil (γ :: a) = inr λ Δ⊢γ:⊘ → cons≠nil (Δ⊢γ:⊘→γ=nil Δ⊢γ:⊘)
  dec-⊢S Δ (Γ :: (x , A)) (γ :: (y , t)) with dec-⊢S Δ Γ γ | dec-⊢C (Γ :: (x , A)) | dec-⊢t Δ (A [ γ ]Pre-Ty) t | eqdecℕ x y
  ...                                    | inl Δ⊢γ:Γ       | inl Γ+⊢               | inl Δ⊢t                    | inl idp    = inl (sc Δ⊢γ:Γ Γ+⊢ Δ⊢t idp)
  ...                                    | inl _           | inl _                 | inl _                      | inr x≠y    = inr λ Δ⊢γ+:Γ+ → x≠y (Δ⊢γ+:Γ+→x=y Δ⊢γ+:Γ+)
  ...                                    | inl _           | inl _                 | inr Δ⊬t                    | _          = inr λ Δ⊢γ+:Γ+ → Δ⊬t (Δ⊢γ+:Γ+→Δ⊢t Δ⊢γ+:Γ+)
  ...                                    | inl _           | inr Γ+⊬               | _                          | _          = inr λ Δ⊢γ+:Γ+ → Γ+⊬ (Δ⊢γ:Γ→Γ⊢ Δ⊢γ+:Γ+)
  ...                                    | inr Δ⊬γ         | _                     | _                          | _          = inr λ Δ⊢γ+:Γ+ → Δ⊬γ (Δ⊢γ+:Γ+→Δ⊢γ Δ⊢γ+:Γ+)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

-- here we define the structure version of a cartesian category
module Categories.Category.Cartesian.Structure where

open import Level

open import Categories.Category
open import Categories.Category.Cartesian
open import Categories.Category.Monoidal

record CartesianCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U         : Category o ℓ e  -- U for underlying
    cartesian : Cartesian U

  module U = Category U
  module cartesian = Cartesian cartesian

  open U public
  open cartesian public

  monoidalCategory : MonoidalCategory o ℓ e
  monoidalCategory = record
    { U        = U
    ; monoidal = monoidal
    }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module ClashingModuleImport where

X = TODO--I-haven't-fully-understood-this-one

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Full β-reduction in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Reduction.Full where

open import Data.Fin using (suc; zero)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.List using ([]; _∷_)
open import Data.Sum using ([_,_])
open import Data.Product using (_,_; ∃; _×_)
open import Function using (flip; _∘_)
open import Relation.Binary using (Setoid; Preorder)
import Relation.Binary.Construct.Closure.Equivalence as EqClos
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (ε; _◅_; gmap)
import Relation.Binary.Construct.Closure.Symmetric as SymClos
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import Relation.Binary.Reduction
import Function.Equivalence as Equiv

open import FOmegaInt.Syntax

open Syntax
open Substitution using (_[_]; weaken)

----------------------------------------------------------------------
-- Full β-reduction and equality relations

infixl 9  _·₁_ _·₂_ _⊡₁_ _⊡₂_
infixr 7  _⇒₁_ _⇒₂_
infix  6  _⋯₁_ _⋯₂_
infix  5  _→β_ _Kd→β_

mutual

  -- The compatible closure of a binary term relation.

  data Compat (_∼_ : TRel Term) {n} : Term n → Term n → Set where
    ⌈_⌉  : ∀ {a₁ a₂} → a₁ ∼ a₂                  → Compat _∼_ a₁ a₂
    Π₁   : ∀ {k₁ k₂} → KdCompat _∼_ k₁ k₂ → ∀ a → Compat _∼_ (Π k₁ a) (Π k₂ a)
    Π₂   : ∀ {a₁ a₂} k → Compat _∼_ a₁ a₂       → Compat _∼_ (Π k a₁) (Π k a₂)
    _⇒₁_ : ∀ {a₁ a₂} → Compat _∼_ a₁ a₂   → ∀ b → Compat _∼_ (a₁ ⇒ b) (a₂ ⇒ b)
    _⇒₂_ : ∀ {b₁ b₂} a → Compat _∼_ b₁ b₂       → Compat _∼_ (a ⇒ b₁) (a ⇒ b₂)
    Λ₁   : ∀ {k₁ k₂} → KdCompat _∼_ k₁ k₂ → ∀ a → Compat _∼_ (Λ k₁ a) (Λ k₂ a)
    Λ₂   : ∀ {a₁ a₂} k → Compat _∼_ a₁ a₂       → Compat _∼_ (Λ k a₁) (Λ k a₂)
    ƛ₁   : ∀ {a₁ a₂} → Compat _∼_ a₁ a₂   → ∀ b → Compat _∼_ (ƛ a₁ b) (ƛ a₂ b)
    ƛ₂   : ∀ {b₁ b₂} a → Compat _∼_ b₁ b₂       → Compat _∼_ (ƛ a b₁) (ƛ a b₂)
    _·₁_ : ∀ {a₁ a₂} → Compat _∼_ a₁ a₂   → ∀ b → Compat _∼_ (a₁ · b) (a₂ · b)
    _·₂_ : ∀ {b₁ b₂} a → Compat _∼_ b₁ b₂       → Compat _∼_ (a · b₁) (a · b₂)
    _⊡₁_ : ∀ {a₁ a₂} → Compat _∼_ a₁ a₂   → ∀ b → Compat _∼_ (a₁ ⊡ b) (a₂ ⊡ b)
    _⊡₂_ : ∀ {b₁ b₂} a → Compat _∼_ b₁ b₂       → Compat _∼_ (a ⊡ b₁) (a ⊡ b₂)

  data KdCompat (_∼_ : TRel Term) {n} : Kind Term n → Kind Term n → Set where
    _⋯₁_ : ∀ {a₁ a₂} → Compat _∼_ a₁ a₂ → ∀ b   → KdCompat _∼_ (a₁ ⋯ b) (a₂ ⋯ b)
    _⋯₂_ : ∀ {b₁ b₂} a → Compat _∼_ b₁ b₂       → KdCompat _∼_ (a ⋯ b₁) (a ⋯ b₂)
    Π₁   : ∀ {j₁ j₂} → KdCompat _∼_ j₁ j₂ → ∀ b → KdCompat _∼_ (Π j₁ b) (Π j₂ b)
    Π₂   : ∀ {k₁ k₂} k → KdCompat _∼_ k₁ k₂     → KdCompat _∼_ (Π k k₁) (Π k k₂)

-- β-contraction.
data BetaCont {n} : Term n → Term n → Set where
  cont-Tp· : ∀ k a b → BetaCont ((Λ k a) · b) (a [ b ])
  cont-Tm· : ∀ a b c → BetaCont ((ƛ a b) · c) (b [ c ])
  cont-⊡   : ∀ k a b → BetaCont ((Λ k a) ⊡ b) (a [ b ])

-- One-step β-reduction.

_→β_ : TRel Term
_→β_ = Compat BetaCont

_Kd→β_ : TRel (Kind Term)
_Kd→β_ = KdCompat BetaCont

-- Full β-reduction and equality.

β-reduction : Reduction Term
β-reduction = record { _→1_ = _→β_ }

β-reductionKind : Reduction (Kind Term)
β-reductionKind = record { _→1_ = _Kd→β_ }

open Reduction β-reduction public hiding (_→1_)
  renaming (_→*_ to _→β*_; _↔_ to _≡β_)

open Reduction β-reductionKind public hiding (_→1_)
  renaming (_→*_ to _Kd→β*_; _↔_ to _Kd≡β_)

----------------------------------------------------------------------
-- Simple properties of the β-reductions/equalities

-- Inclusions.

→β⇒→β* = →1⇒→* β-reduction
→β*⇒≡β = →*⇒↔  β-reduction
→β⇒≡β  = →1⇒↔  β-reduction

-- Reduction is a preorders.

→β*-preorder   = →*-preorder β-reduction
Kd→β*-preorder = →*-preorder β-reductionKind

-- Preorder reasoning for reduction.

module →β*-Reasoning    = →*-Reasoning β-reduction
module Kd→β*-Reasoning  = →*-Reasoning β-reductionKind

-- Raw terms and kinds together with β-equality form setoids.

≡β-setoid   = ↔-setoid β-reduction
Kd≡β-setoid = ↔-setoid β-reductionKind

-- Equational reasoning for the equality.

module ≡β-Reasoning   = ↔-Reasoning β-reduction
module Kd≡β-Reasoning = ↔-Reasoning β-reductionKind

-- Multistep and equality congruence lemmas.

module CongLemmas (_∼_ : TRel Term) where

  private
    reduction : Reduction Term
    reduction = record { _→1_ = Compat _∼_ }

    reductionKd : Reduction (Kind Term)
    reductionKd = record { _→1_ = KdCompat _∼_ }

    module O  {n} = Preorder (→*-preorder reduction   n)
    module S  {n} = Setoid   (↔-setoid    reduction   n)
    module OK {n} = Preorder (→*-preorder reductionKd n)
    module SK {n} = Setoid   (↔-setoid    reductionKd n)

  open Reduction reduction
  open Reduction reductionKd using () renaming (_→*_ to _Kd→*_; _↔_ to _Kd↔_)

  -- A Congruence lemma for _⌞∙⌟_.

  →1-⌞∙⌟₁ : ∀ {n} {a₁ a₂ : Term n} → a₁ →1 a₂ → ∀ bs → a₁ ⌞∙⌟ bs →1 a₂ ⌞∙⌟ bs
  →1-⌞∙⌟₁ a₁∼a₂ []       = a₁∼a₂
  →1-⌞∙⌟₁ a₁∼a₂ (b ∷ bs) = →1-⌞∙⌟₁ (a₁∼a₂ ·₁ b) bs

  -- Multistep congruence lemmas for transitive closures.

  →*-Π : ∀ {n} {k₁ k₂ : Kind Term n} {a₁ a₂} →
         k₁ Kd→* k₂ → a₁ →* a₂ → Π k₁ a₁ →* Π k₂ a₂
  →*-Π {a₁ = a₁} k₁→*k₂ a₁→*a₂ =
    O.trans (gmap (flip Π a₁) (λ j→k → Π₁ j→k a₁) k₁→*k₂)
            (gmap (Π _) (Π₂ _) a₁→*a₂)

  →*-⇒ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
         a₁ →* a₂ → b₁ →* b₂ → a₁ ⇒ b₁ →* a₂ ⇒ b₂
  →*-⇒ {b₁ = b₁} a₁→*a₂ b₁→*b₂ =
    O.trans (gmap (_⇒ b₁) (_⇒₁ b₁) a₁→*a₂) (gmap (_ ⇒_) (_ ⇒₂_) b₁→*b₂)

  →*-Λ : ∀ {n} {k₁ k₂ : Kind Term n} {a₁ a₂} →
         k₁ Kd→* k₂ → a₁ →* a₂ → Λ k₁ a₁ →* Λ k₂ a₂
  →*-Λ {a₁ = a₁} k₁→*k₂ a₁→*a₂ =
    O.trans (gmap (flip Λ a₁) (λ j→k → Λ₁ j→k a₁) k₁→*k₂)
            (gmap (Λ _) (Λ₂ _) a₁→*a₂)

  →*-ƛ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
         a₁ →* a₂ → b₁ →* b₂ → ƛ a₁ b₁ →* ƛ a₂ b₂
  →*-ƛ {b₁ = b₁} a₁→*a₂ b₁→*b₂ =
    O.trans (gmap (flip ƛ b₁) (flip ƛ₁ b₁) a₁→*a₂) (gmap (ƛ _) (ƛ₂ _) b₁→*b₂)

  →*-· : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
         a₁ →* a₂ → b₁ →* b₂ → a₁ · b₁ →* a₂ · b₂
  →*-· {b₁ = b₁} a₁→*a₂ b₁→*b₂ =
    O.trans (gmap (_· b₁) (_·₁ b₁) a₁→*a₂) (gmap (_ ·_) (_ ·₂_) b₁→*b₂)

  →*-⊡ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
         a₁ →* a₂ → b₁ →* b₂ → a₁ ⊡ b₁ →* a₂ ⊡ b₂
  →*-⊡ {b₁ = b₁} a₁→*a₂ b₁→*b₂ =
    O.trans (gmap (_⊡ b₁) (_⊡₁ b₁) a₁→*a₂) (gmap (_ ⊡_) (_ ⊡₂_) b₁→*b₂)

  Kd→*-⋯ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
         a₁ →* a₂ → b₁ →* b₂ → a₁ ⋯ b₁ Kd→* a₂ ⋯ b₂
  Kd→*-⋯ {b₁ = b₁} a₁→*a₂ b₁→*b₂ =
    OK.trans (gmap (_⋯ b₁) (_⋯₁ b₁) a₁→*a₂) (gmap (_ ⋯_) (_ ⋯₂_) b₁→*b₂)

  Kd→*-Π : ∀ {n} {j₁ j₂ : Kind Term n} {k₁ k₂} →
         j₁ Kd→* j₂ → k₁ Kd→* k₂ → Π j₁ k₁ Kd→* Π j₂ k₂
  Kd→*-Π {k₁ = k₁} j₁→*j₂ k₁→*k₂ =
    OK.trans (gmap (flip Π k₁) (λ j→k → Π₁ j→k k₁) j₁→*j₂)
             (gmap (Π _) (Π₂ _) k₁→*k₂)

  →*-⌞∙⌟₁ : ∀ {n} {a₁ a₂ : Term n} → a₁ →* a₂ → ∀ bs → a₁ ⌞∙⌟ bs →* a₂ ⌞∙⌟ bs
  →*-⌞∙⌟₁ a₁→*a₂ bs = gmap (_⌞∙⌟ bs) (flip →1-⌞∙⌟₁ bs) a₁→*a₂

  -- Congruence lemmas for equivalences closures.

  ↔-Π : ∀ {n} {k₁ k₂ : Kind Term n} {a₁ a₂} →
        k₁ Kd↔ k₂ → a₁ ↔ a₂ → Π k₁ a₁ ↔ Π k₂ a₂
  ↔-Π {a₁ = a₁} k₁↔k₂ a₁↔a₂ =
    S.trans (EqClos.gmap (flip Π a₁) (λ j→k → Π₁ j→k a₁) k₁↔k₂)
            (EqClos.gmap (Π _)       (Π₂ _)              a₁↔a₂)

  ↔-⇒ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
        a₁ ↔ a₂ → b₁ ↔ b₂ → a₁ ⇒ b₁ ↔ a₂ ⇒ b₂
  ↔-⇒ {b₁ = b₁} a₁↔a₂ b₁↔b₂ =
    S.trans (EqClos.gmap (_⇒ b₁) (_⇒₁ b₁) a₁↔a₂)
            (EqClos.gmap (_ ⇒_)  (_ ⇒₂_)  b₁↔b₂)

  ↔-Λ : ∀ {n} {k₁ k₂ : Kind Term n} {a₁ a₂} →
        k₁ Kd↔ k₂ → a₁ ↔ a₂ → Λ k₁ a₁ ↔ Λ k₂ a₂
  ↔-Λ {a₁ = a₁} k₁↔k₂ a₁↔a₂ =
    S.trans (EqClos.gmap (flip Λ a₁) (λ j→k → Λ₁ j→k a₁) k₁↔k₂)
            (EqClos.gmap (Λ _)       (Λ₂ _)              a₁↔a₂)

  ↔-ƛ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
        a₁ ↔ a₂ → b₁ ↔ b₂ → ƛ a₁ b₁ ↔ ƛ a₂ b₂
  ↔-ƛ {b₁ = b₁} a₁↔a₂ b₁↔b₂ =
    S.trans (EqClos.gmap (flip ƛ b₁) (flip ƛ₁ b₁) a₁↔a₂)
            (EqClos.gmap (ƛ _)       (ƛ₂ _)       b₁↔b₂)

  ↔-· : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
        a₁ ↔ a₂ → b₁ ↔ b₂ → a₁ · b₁ ↔ a₂ · b₂
  ↔-· {b₁ = b₁} a₁↔a₂ b₁↔b₂ =
    S.trans (EqClos.gmap (_· b₁) (_·₁ b₁) a₁↔a₂)
            (EqClos.gmap (_ ·_)  (_ ·₂_)  b₁↔b₂)

  ↔-⊡ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
        a₁ ↔ a₂ → b₁ ↔ b₂ → a₁ ⊡ b₁ ↔ a₂ ⊡ b₂
  ↔-⊡ {b₁ = b₁} a₁↔a₂ b₁↔b₂ =
    S.trans (EqClos.gmap (_⊡ b₁) (_⊡₁ b₁) a₁↔a₂)
            (EqClos.gmap (_ ⊡_)  (_ ⊡₂_)  b₁↔b₂)

  Kd↔-⋯ : ∀ {n} {a₁ a₂ : Term n} {b₁ b₂} →
          a₁ ↔ a₂ → b₁ ↔ b₂ → a₁ ⋯ b₁ Kd↔ a₂ ⋯ b₂
  Kd↔-⋯ {b₁ = b₁} a₁↔a₂ b₁↔b₂ =
    SK.trans (EqClos.gmap (_⋯ b₁) (_⋯₁ b₁) a₁↔a₂)
             (EqClos.gmap (_ ⋯_)  (_ ⋯₂_)  b₁↔b₂)

  Kd↔-Π : ∀ {n} {j₁ j₂ : Kind Term n} {k₁ k₂} →
          j₁ Kd↔ j₂ → k₁ Kd↔ k₂ → Π j₁ k₁ Kd↔ Π j₂ k₂
  Kd↔-Π {k₁ = k₁} j₁↔j₂ k₁↔k₂ =
    SK.trans (EqClos.gmap (flip Π k₁) (λ j→k → Π₁ j→k k₁) j₁↔j₂)
             (EqClos.gmap (Π _)       (Π₂ _)              k₁↔k₂)

  ↔-⌞∙⌟₁ : ∀ {n} {a₁ a₂ : Term n} → a₁ ↔ a₂ → ∀ bs → a₁ ⌞∙⌟ bs ↔ a₂ ⌞∙⌟ bs
  ↔-⌞∙⌟₁ a₁↔a₂ bs = EqClos.gmap (_⌞∙⌟ bs) (flip →1-⌞∙⌟₁ bs) a₁↔a₂

open CongLemmas BetaCont public renaming
  ( →1-⌞∙⌟₁ to →β-⌞∙⌟₁
  ; →*-Π    to →β*-Π
  ; →*-⇒    to →β*-⇒
  ; →*-Λ    to →β*-Λ
  ; →*-ƛ    to →β*-ƛ
  ; →*-·    to →β*-·
  ; →*-⊡    to →β*-⊡
  ; Kd→*-⋯  to Kd→β*-⋯
  ; Kd→*-Π  to Kd→β*-Π
  ; →*-⌞∙⌟₁ to →β*-⌞∙⌟₁
  ; ↔-Π     to ≡β-Π
  ; ↔-⇒     to ≡β-⇒
  ; ↔-Λ     to ≡β-Λ
  ; ↔-ƛ     to ≡β-ƛ
  ; ↔-·     to ≡β-·
  ; ↔-⊡     to ≡β-⊡
  ; Kd↔-⋯   to Kd≡β-⋯
  ; Kd↔-Π   to Kd≡β-Π
  ; ↔-⌞∙⌟₁  to ≡β-⌞∙⌟₁
  )

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


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

open import Cubical.Core.Everything

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

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

private
  variable
    ℓ ℓ' : Level

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

infixr 5 _×_

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

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

-- We still export the version using Σ
_×Σ_ : (A : Type ℓ) (B : Type ℓ') → Type (ℓ-max ℓ ℓ')
A ×Σ B = Σ A (λ _ → B)

infixr 5 _×Σ_

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

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

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

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --safe --no-qualified-instances #-}
-- Bytecode; i.e., instruction sequences;
-- agnostic about the exact instructions, but opiniated about labels
open import Data.List hiding (concat)

module JVM.Syntax.Bytecode {ℓ} (T : Set ℓ) (I : T → T → List T → Set ℓ) where

open import Level
open import Function using (_∘_)
open import Data.Unit
open import Relation.Unary hiding (_∈_; Empty)
open import Relation.Binary.PropositionalEquality
open import Relation.Ternary.Data.ReflexiveTransitive as Star
open import Relation.Ternary.Core
open import Relation.Ternary.Structures
open import Relation.Ternary.Structures.Syntax
open import Relation.Ternary.Data.Bigplus
open import Relation.Ternary.Data.IndexedMonoid

open import Data.Sum
open import Data.Product

open import JVM.Model T

open import JVM.Syntax.Labeling T

data Code : T → T → Pred Intf ℓ where
  labeled : ∀ {τ₁ τ₂} → ∀[ Up (Labeling τ₁) ✴ Down (I τ₁ τ₂) ⇒ Code τ₁ τ₂ ]
  instr   : ∀ {τ₁ τ₂} → ∀[ Down (I τ₁ τ₂) ⇒ Code τ₁ τ₂ ]

getInstr : ∀ {τ₁ τ₂} → ∀[ Code τ₁ τ₂ ⇒ Down (I τ₁ τ₂) ✴ Code τ₁ τ₂ ]
getInstr c@(labeled (l ∙⟨ σ ⟩ i@(↓ _))) =
  let (i ∙⟨ σ ⟩ l∙i) = ✴-swap (✴-assocₗ (l ∙⟨ σ ⟩ copy i))
  in i ∙⟨ σ ⟩ labeled l∙i
getInstr (instr i@(↓ _)) = i ∙⟨ ∙-copy i ⟩ (instr i)

module _ where
  open Disjoint using (bags; bags-isMonoid; bags-isSemigroup; bags-isCommutative; empty-unique)

  label : ∀ {τ₁ τ₂} → ∀[ Up (Labeling τ₁) ⇒ Code τ₁ τ₂ ─✴ Code τ₁ τ₂ ]
  label l ⟨ σ ⟩ instr i   = labeled (l ∙⟨ σ ⟩ i)
  label l ⟨ σ ⟩ labeled (l₂∙i) with ✴-assocₗ (l ∙⟨ σ ⟩ l₂∙i)
  ... | l₁∙l₂ ∙⟨ σ′ ⟩ i with upMap (↑ (✴-curry (arrow concat))) ⟨ ∙-idˡ ⟩ zipUp l₁∙l₂
  ... | ls = labeled (ls ∙⟨ σ′ ⟩ i)

⟪_↝_⟫ : T → T → Pred Intf ℓ
⟪ τ₁ ↝ τ₂ ⟫ = Star Code τ₁ τ₂

⟪_↝_⟫+ : T → T → Pred Intf ℓ
⟪ τ₁ ↝ τ₂ ⟫+ = Plus Code τ₁ τ₂

⟪_↜_⟫ : T → T → Pred Intf ℓ
⟪ τ₂ ↜ τ₁ ⟫ = Star (flip Code) τ₁ τ₂
  where open import Function using (flip)

module _ (nop : ∀ {τ} → I τ τ []) where

  label-start : ∀ {τ₁ τ₂} → ∀[ Up (Labeling τ₁) ⇒ ⟪ τ₁ ↝ τ₂ ⟫ ─✴ ⟪ τ₁ ↝ τ₂ ⟫ ]
  label-start l ⟨ σ ⟩ nil            = labeled (l ∙⟨ σ ⟩ ↓ nop) ▹⟨ ∙-idʳ ⟩ nil
  label-start l ⟨ σ ⟩ (i ▹⟨ σ₂ ⟩ is) =
    let _ , σ₃ , σ₄ = ∙-assocₗ σ σ₂ in
    (label l ⟨ σ₃ ⟩ i) ▹⟨ σ₄ ⟩ is


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

open import Cubical.HITs.Colimit.Base public
open import Cubical.HITs.Colimit.Examples public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Presheaves.Facts.Exponential where

open import Data.Product using (_,_)
open import Relation.Binary using (Setoid)

open import Cats.Category
open import Cats.Category.Fun using (Fun ; ≈-intro ; ≈-elim)
open import Cats.Category.Presheaves using (Presheaves)
open import Cats.Category.Setoids as Setoids using (≈-intro ; ≈-elim)
open import Cats.Functor using (Functor)
open import Cats.Trans using (Trans ; component ; natural)

import Cats.Category.Fun.Facts.Product as Product
import Cats.Category.Setoids.Facts

open Functor
open HasBinaryProducts {{...}}
open Setoids._⇒_

module _ {l} {ℂ : Category l l l} where

  private
    module ℂ = Category ℂ
    open Category (Presheaves ℂ l l)
    module $ (F : Obj) {x : Category.Obj ℂ} = Setoid (fobj F x)

  -- Could replace this with transposeBifunctor₂ HomF, but that would introduce
  -- even more redundant compositions with the identity.
  y : ℂ.Obj → Obj
  y d = record
    { fobj = λ c → ℂ.Hom c d
    ; fmap = λ f → record
      { arr = (ℂ._∘ f)
      ; resp = ℂ.∘-resp-l
      }
    ; fmap-resp = λ eq₁ → ≈-intro λ eq₂ → ℂ.∘-resp eq₂ eq₁
    ; fmap-id = ≈-intro λ eq → ℂ.≈.trans ℂ.id-r eq
    ; fmap-∘ = ≈-intro λ eq → ℂ.≈.trans ℂ.assoc (ℂ.∘-resp-l eq)
    }

  _↝_ : (F G : Obj) → Obj
  F ↝ G = record
    { fobj = λ d → Hom (y d × F) G
    ; fmap = λ {d} {d′} f → record
      { arr = λ α → record
        { component = λ d → record
          { arr = λ where
              (g , c) → arr (component α d) (f ℂ.∘ g , c)
          ; resp = λ where
              (eq₁ , eq₂) → resp (component α d) (ℂ.∘-resp-r eq₁ , eq₂)
          }
        ; natural = λ {e} {e′} {g} → ≈-intro λ where
            {h , c} {h′ , c′} (h≈h′ , c≈c′) →
              $.trans G (resp (component α e′) (ℂ.unassoc , $.refl F))
                (≈-elim (natural α) (ℂ.∘-resp-r h≈h′ , c≈c′))
        }
      ; resp = λ α≈β → ≈-intro (≈-intro λ where
          (f≈g , h≈i) → ≈-elim (≈-elim α≈β) (ℂ.∘-resp-r f≈g , h≈i))
      }
    ; fmap-resp = λ f≈g → ≈-intro λ α≈β → ≈-intro (≈-intro λ where
        (c≈d , h≈i) → ≈-elim (≈-elim α≈β) ((ℂ.∘-resp f≈g c≈d) , h≈i))
    ; fmap-id = ≈-intro λ α≈β → ≈-intro (≈-intro λ where
        (c≈d , h≈i) → ≈-elim (≈-elim α≈β) ((ℂ.≈.trans ℂ.id-l c≈d) , h≈i))
    ; fmap-∘ = ≈-intro λ α≈β → ≈-intro (≈-intro λ where
        (c≈d , h≈i) → ≈-elim (≈-elim α≈β) ((ℂ.≈.trans ℂ.unassoc (ℂ.∘-resp-r c≈d)) , h≈i))
    }

  Eval : ∀ F G → F ↝ G × F ⇒ G
  Eval F G = record
    { component = λ c → record
      { arr = λ where
          (α , x) → arr (component α c) (ℂ.id , x)
      ; resp = λ where
          (α≈β , f≈g) → ≈-elim (≈-elim α≈β) (ℂ.≈.refl , f≈g)
      }
    ; natural = λ {c} {d} → ≈-intro λ where
        {α , f} {β , g} (α≈β , f≈g) →
          $.trans G
            (≈-elim (≈-elim α≈β)
              (ℂ.≈.trans ℂ.id-r (ℂ.≈.sym ℂ.id-l) , resp (fmap F _) f≈g))
            (≈-elim (natural β) (ℂ.≈.refl , $.refl F))
    }

  Curry : ∀ E F G → E × F ⇒ G → E ⇒ F ↝ G
  Curry E F G α = record
    { component = λ d → record
      { arr = λ x → record
        { component = λ c → record
          { arr = λ where
              (f , y) → arr (component α c) (arr (fmap E f) x , y)
          ; resp = λ where
              (c≈d , x≈y) → resp (component α c)
                (≈-elim (fmap-resp E c≈d) ($.refl E) , x≈y)
          }
        ; natural = ≈-intro λ where
            (f≈g , x≈y) → $.trans G
              (resp (component α _)
                (($.sym E (≈-elim (fmap-∘ E) ($.refl E))) , ($.refl F)))
              (≈-elim (natural α) (≈-elim (fmap-resp E f≈g) ($.refl E) , x≈y))
        }
      ; resp = λ x≈y → ≈-intro (≈-intro λ where
          (f≈g , c≈d) → resp (component α _) ((≈-elim (fmap-resp E f≈g) x≈y) , c≈d))
      }
    ; natural = ≈-intro λ x≈y → ≈-intro (≈-intro λ where
        (f≈g , c≈d) → resp (component α _)
          ( $.trans E (≈-elim (fmap-∘ E) x≈y)
              (≈-elim (fmap-resp E (ℂ.∘-resp-r f≈g)) ($.refl E))
          , c≈d ))
    }

  instance
    hasExponentials : HasExponentials (Presheaves ℂ l l)
    hasExponentials = record
      { hasBinaryProducts = Product.hasBinaryProducts
      ; _↝′_ = λ F G → record
        { Cᴮ = F ↝ G
        ; eval = Eval F G
        ; curry′ = λ {E} α → record
          { arr = Curry E F G α
          ; prop = ≈-intro (≈-intro λ where
              (x≈y , u≈v) → resp (component α _) (≈-elim (fmap-id E) x≈y , u≈v))
          ; unique = λ {α} α≈ → ≈-intro (≈-intro (λ x≈y → ≈-intro (≈-intro (λ where
              (f≈g , u≈v) → $.trans G
                (≈-elim (≈-elim (≈.sym α≈)) (≈-elim (fmap-resp E f≈g) ($.refl E) , u≈v))
                ($.trans G
                  (≈-elim (≈-elim (≈-elim (natural α) x≈y)) (ℂ.≈.refl , ($.refl F)))
                  (resp (component (arr (component α _) _) _) (ℂ.id-r , ($.refl F))))))))
          }
        }
      }

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
{-# OPTIONS --copatterns --sized-types #-}

module SDE where

open import Size
open import Function
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Sum as Sum

open import Streams

-- | Signatures
record Sig : Set₁ where
  field
    ∥_∥ : Set
    ar : ∥_∥ → Set
open Sig public

-- | Extension of signature Σ, on objects
⟪_⟫ : Sig → Set → Set
⟪ Σ ⟫ X = ⨿ ∥ Σ ∥ λ f → (ar Σ f → X)

-- | Extension of signature Σ, on morphisms
⟪_⟫₁ : (Σ : Sig) {A B : Set} → (A → B) → ⟪ Σ ⟫ A → ⟪ Σ ⟫ B
⟪_⟫₁ Σ f (s , α) = (s , f ∘ α)

-- | Terms over a given signature together with some basic operations.
module Terms (Σ : Sig) where

  -- | Terms built from the signature Σ with variables in V.
  data T (V : Set) : Set where
    sup : ⟪ Σ ⟫ (T V) ⊎ V → T V

  -- | Recursion on terms.
  rec : ∀{V X} → (f : ⟪ Σ ⟫ X ⊎ V → X) → T V → X
  rec f (sup (inj₁ (s , α))) = f (inj₁ (s , λ i → rec f (α i)))
  rec f (sup (inj₂ y))       = f (inj₂ y)

  -- | Functor T, on morphisms
  T₁ : ∀ {V W} → (V → W) → T V → T W
  T₁ f = rec (sup ∘ Sum.map id f)

  -- | Injection of variables into terms.
  η : ∀{V} → V → T V
  η = sup ∘ inj₂

-- | Interpretation of SDEs that use the given signature and set of variables.
module SDE-Impl (Σ : Sig) (X : Set) where

  open Terms Σ

  -- | Variables for streams and their derivatives.
  V : Set
  V = X ⊎ X

  -- | An SDE consists of an assignment of outputs and terms for
  -- each symbol in the signature. Note that both output and the
  -- terms may depend on the outputs of the arguments of the corresponding
  -- symbol.
  SDE : Set → Set
  SDE A = (f : ∥ Σ ∥) → ((ar Σ f → A) → A) × ((ar Σ f → A) → T V)

  -- | Interpretation of terms over the symbols defined by the given SDE
  -- as streams.
  ⟦_⟧₁ : ∀ {A} → SDE A → ((f : ∥ Σ ∥) → ar Σ f → X) → T V →
         ∀{i} → (X → Stream {i} A) → ∀ {j : Size< i} → Stream {j} A

  -- | Interpretation of symbols defined by the given SDE as streams.
  ⟦_⟧ : ∀ {A} → SDE A → ((f : ∥ Σ ∥) → ar Σ f → X) → (f : ∥ Σ ∥) →
        ∀{i} → (X → Stream {i} A) → Stream {i} A
  hd (⟦ E ⟧ vars f vals) = f-out (hd ∘ vals ∘ vars f)
    where f-out = proj₁ (E f)
  tl (⟦ E ⟧ vars f vals) = ⟦ E ⟧₁ vars (f-step (hd ∘ vals ∘ vars f)) vals
    where f-step = proj₂ (E f)

  -- Interpret terms by induction. This map is assumed to be called from the
  -- tail case of ⟦_⟧.

  -- For a symbol, we just use its interpretation but on the tails of the
  -- argument streams
  ⟦ E ⟧₁ vars (sup (inj₁ (f , α)))  vals = ⟦ E ⟧ vars f (λ x → tl (vals x))
  -- A variable is just interpreted by its valuation.
  ⟦ E ⟧₁ vars (sup (inj₂ (inj₁ x))) vals = vals x
  -- A variable denoting a derivative is interpreted by the derivative of
  -- the corresponding stream.
  ⟦ E ⟧₁ vars (sup (inj₂ (inj₂ x))) vals = tl (vals x)

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Andreas, 2021-12-31, issue #5712, reported by Trebor-Huang

-- {-# OPTIONS -v tc.cover.cover:10 #-}

open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

nothing : Term → TC ⊤
nothing hole = returnTC _

record Foo : Set1 where
  field
    A : Set
    @(tactic nothing) foo : A → A
open Foo

F : Foo
F .A     = ⊤
F .foo n = _

-- Should succeed.
-- There was an internal error, because the coverage checker did
-- not expand the last clause due to the presence of a tactic (#5358).
-- However, in this case, there is a user argument that forces the
-- expansion.  This is now recognized by the coverage checker.


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

module Fragment.Examples.CSemigroup.Arith.Base where

open import Fragment.Examples.Semigroup.Arith.Base public
open import Data.Nat.Properties
  using (*-isCommutativeSemigroup; +-isCommutativeSemigroup)

+-csemigroup = csemigroup→model +-isCommutativeSemigroup
*-csemigroup = csemigroup→model *-isCommutativeSemigroup

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Functor where

import Logic.Identity as Id
import Category
import Logic.ChainReasoning

open Category
open Poly-Cat

private
 module Fun where

  data Functor (ℂ ⅅ : Cat) : Set1 where
    functor : (F     : Obj ℂ -> Obj ⅅ)
	      (map   : {A B : Obj ℂ} -> A ─→ B -> F A ─→ F B)
	      (mapId : {A : Obj ℂ} -> map (id {A = A}) == id)
	      (mapCompose : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
			    map (f ∘ g) == map f ∘ map g
	      ) -> Functor ℂ ⅅ

open Fun public

module Projections where

  Map : {ℂ ⅅ : Cat} -> Functor ℂ ⅅ -> Obj ℂ -> Obj ⅅ
  Map (functor F _ _ _) = F

  map : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
	{A B : Obj ℂ} -> A ─→ B -> Map F A ─→ Map F B
  map (functor _ m _ _) = m

  mapId : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
	  {A : Obj ℂ} -> map F id == id {A = Map F A}
  mapId (functor _ _ i _) = i

  mapCompose : {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ)
	       {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
	       map F (f ∘ g) == map F f ∘ map F g
  mapCompose (functor _ _ _ c) = c

module Functor {ℂ ⅅ : Cat}(F : Functor ℂ ⅅ) where

  module P = Projections

  Map : Obj ℂ -> Obj ⅅ
  Map = P.Map F

  map : {A B : Obj ℂ} -> A ─→ B -> Map A ─→ Map B
  map = P.map F

  mapId : {A : Obj ℂ} -> map id == id {A = Map A}
  mapId = P.mapId F

  mapCompose : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
	       map (f ∘ g) == map f ∘ map g
  mapCompose = P.mapCompose F

module Functors where

  Id : {ℂ : Cat} -> Functor ℂ ℂ
  Id = functor (\A -> A) (\f -> f) (\{A} -> refl) (\{A}{B}{C}{f}{g} -> refl)

  _○_ : {ℂ ℚ ℝ : Cat} -> Functor ℚ ℝ -> Functor ℂ ℚ -> Functor ℂ ℝ
  _○_ {ℂ}{ℚ}{ℝ} F G = functor FG m mid mcomp
    where

      module F = Functor F
      module G = Functor G

      FG : Obj ℂ -> Obj ℝ
      FG A = F.Map (G.Map A)

      m : {A B : Obj ℂ} -> A ─→ B -> FG A ─→ FG B
      m f = F.map (G.map f)

      mid : {A : Obj ℂ} -> m (id {A = A}) == id
      mid = chain> F.map (G.map id)
	       === F.map id   by ? -- cong F.map G.mapId
	       === id	      by F.mapId
	where
	  open module Chain = Logic.ChainReasoning.Mono.Homogenous _==_
			      (\f -> refl)
			      (\f g h -> trans)

      mcomp : {A B C : Obj ℂ}{f : B ─→ C}{g : A ─→ B} ->
	      m (f ∘ g) == m f ∘ m g
      mcomp {f = f}{g = g} =
	chain> F.map (G.map (f ∘ g))
	   === F.map (G.map f ∘ G.map g)
	       by ? -- cong F.map G.mapCompose
	   === F.map (G.map f) ∘ F.map (G.map g)
	       by F.mapCompose
	where
	  open module Chain = Logic.ChainReasoning.Mono.Homogenous _==_
			      (\f -> refl)
			      (\f g h -> trans)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Examples where

open import Data.Maybe using (just ; nothing)
open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉)
open import Data.Nat.Properties using (cancel-+-left)
import Algebra.Structures
open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L_)
open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map)
open import Function using (id)
import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)

open import Structures using (Shaped)
import GetTypes
import FreeTheorems
import BFF

open GetTypes.PartialVecVec using (Get)
open FreeTheorems.PartialVecVec using (assume-get)
open BFF.PartialVecBFF using (bff)

ℕ-decSetoid = Relation.Binary.DecTotalOrder.Eq.decSetoid Data.Nat.decTotalOrder

reverse' : Get
reverse' = assume-get id id reverse

double' : Get
double' = assume-get id g f
  where g : ℕ → ℕ
        g zero = zero
        g (suc n) = suc (suc (g n))
        f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n)
        f []      = []
        f (x ∷ v) = x ∷ x ∷ f v

double'' : Get
double'' = assume-get id _ (λ v → v ++ v)

tail' : Get
tail' = assume-get suc id tail

tail-example : bff ℕ-decSetoid tail' 2 (8 ∷ 5 ∷ []) (3 ∷ 1 ∷ []) ≡ just (just 8 ∷ just 3 ∷ just 1 ∷ [])
tail-example = refl

take' : ℕ → Get
take' n = assume-get (_+_ n) _ (take n)

drop' : ℕ → Get
drop' n = assume-get (_+_ n) _ (drop n)

sieve' : Get
sieve' = assume-get id _ f
  where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
        f []           = []
        f (x ∷ [])     = x ∷ []
        f (x ∷ _ ∷ xs) = x ∷ f xs

sieve-example : bff ℕ-decSetoid sieve' 4 (0 ∷ 2 ∷ []) (1 ∷ 3 ∷ []) ≡ just (just 1 ∷ just 2 ∷ just 3 ∷ nothing ∷ [])
sieve-example = refl

intersperse-len : ℕ → ℕ
intersperse-len zero          = zero
intersperse-len (suc zero)    = suc zero
intersperse-len (suc (suc n)) = suc (suc (intersperse-len (suc n)))

intersperse : {A : Set} {n : ℕ} → A → Vec A n → Vec A (intersperse-len n)
intersperse s []          = []
intersperse s (x ∷ [])    = x ∷ []
intersperse s (x ∷ y ∷ v) = x ∷ s ∷ intersperse s (y ∷ v)

intersperse' : Get
intersperse' = assume-get suc intersperse-len f
  where f : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A (intersperse-len n)
        f (s ∷ v)        = intersperse s v

intersperse-neg-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ nothing
intersperse-neg-example = refl

intersperse-pos-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 2 ∷ 5 ∷ []) ≡ just (map just (2 ∷ 1 ∷ 3 ∷ 5 ∷ []))
intersperse-pos-example = refl

data PairVec (α : Set) (β : Set) : List α → Set where
  []P : PairVec α β []L
  _,_∷P_ : (x : α) → β → {l : List α} → PairVec α β l → PairVec α β (x ∷L l)

PairVecFirstShaped : (α : Set) → Shaped (List α) (PairVec α)
PairVecFirstShaped α = record
  { arity = length
  ; content = content
  ; fill = fill
  ; isShaped = record
    { content-fill = content-fill
    ; fill-content = fill-content
    } }
  where content : {β : Set} {s : List α} → PairVec α β s → Vec β (length s)
        content []P          = []
        content (a , b ∷P p) = b ∷ content p

        fill : {β : Set} → (s : List α) → Vec β (length s) → PairVec α β s
        fill []L      v       = []P
        fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v

        content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
        content-fill []P          = refl
        content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)

        fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
        fill-content []L      []      = refl
        fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module STLC.Coquand.Convertibility where

open import STLC.Coquand.Substitution public

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

-- Convertibility
infix  3 _∼_
data _∼_ : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A → Set
  where
    refl∼ : ∀ {Γ A} → {M : Γ ⊢ A}
                    → M ∼ M

    _⁻¹∼  : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
                    → (p : M₁ ∼ M₂)
                    → M₂ ∼ M₁

    _⦙∼_  : ∀ {Γ A} → {M₁ M₂ M₃ : Γ ⊢ A}
                    → (p : M₁ ∼ M₂) (q : M₂ ∼ M₃)
                    → M₁ ∼ M₃

    ƛ∼    : ∀ {Γ A B} → {M₁ M₂ : Γ , A ⊢ B}
                      → (p : M₁ ∼ M₂)
                      → ƛ M₁ ∼ ƛ M₂

    _∙∼_  : ∀ {Γ A B} → {M₁ M₂ : Γ ⊢ A ⇒ B} {N₁ N₂ : Γ ⊢ A}
                      → (p : M₁ ∼ M₂) (q : N₁ ∼ N₂)
                      → M₁ ∙ N₁ ∼ M₂ ∙ N₂

    red⇒ : ∀ {Γ Ξ A B} → (σ : Γ ⊢⋆ Ξ) (M : Ξ , A ⊢ B) (N : Γ ⊢ A)
                        → sub σ (ƛ M) ∙ N ∼ sub (σ , N) M

    exp⇒ : ∀ {Γ A B} → (M : Γ ⊢ A ⇒ B)
                      → M ∼ ƛ (wk M ∙ 0)

≡→∼ : ∀ {Γ A} → {M₁ M₂ : Γ ⊢ A}
               → M₁ ≡ M₂
               → M₁ ∼ M₂
≡→∼ refl = refl∼

instance
  per∼ : ∀ {Γ A} → PER (Γ ⊢ A) _∼_
  per∼ =
    record
      { _⁻¹ = _⁻¹∼
      ; _⦙_ = _⦙∼_
      }

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

renred⇒ : ∀ {Γ Γ′ Ξ A B} → {η : Γ′ ∋⋆ Γ}
                          → (σ : Γ ⊢⋆ Ξ) (M : Ξ , A ⊢ B) (N : Γ ⊢ A)
                          → ren η (sub σ (ƛ M) ∙ N) ∼ ren η (sub (σ , N) M)
renred⇒ {η = η} σ M N = ƛ∼ (≡→∼ (sublift◑ η σ M ⁻¹)) ∙∼ refl∼
                       ⦙ red⇒ (η ◑ σ) M (ren η N)
                       ⦙ ≡→∼ ( (λ σ′ → sub σ′ M)
                                & ((⌊ η ⌋ ● σ ,_) & ⌊sub⌋ η N ⁻¹)
                              ⦙ sub◑ η (σ , N) M
                              )

renexp⇒𝓋 : ∀ {Γ Γ′ A B} → {η : Γ′ ∋⋆ Γ}
                         → (i : Γ ∋ A ⇒ B)
                         → ren η (𝓋 i) ∼ ren η (ƛ (wk (𝓋 i) ∙ 0))
renexp⇒𝓋 {η = η} i = exp⇒ (𝓋 (getᵣ η i))
                    ⦙ ƛ∼ (≡→∼ (𝓋 & ( get○ (wkᵣ idᵣ) η i ⁻¹
                                    ⦙ (λ η′ → getᵣ η′ i)
                                      & ( wklid○ η
                                        ⦙ liftwkrid○ η ⁻¹
                                        )
                                    ⦙ get○ (liftᵣ η) (wkᵣ idᵣ) i
                                    )) ∙∼ refl∼)

renexp⇒ƛ : ∀ {Γ Γ′ A B} → {η : Γ′ ∋⋆ Γ}
                         → (M : Γ , A ⊢ B)
                         → ren η (ƛ M) ∼ ren η (ƛ (wk (ƛ M) ∙ 0))
renexp⇒ƛ {η = η} M = exp⇒ (ƛ (ren (liftᵣ η) M))
                    ⦙ ƛ∼ (ƛ∼ (≡→∼ ( renlift○ (wkᵣ idᵣ) η M ⁻¹
                                   ⦙ (λ η′ → ren η′ M)
                                     & (liftᵣ & ( wklid○ η
                                                ⦙ wkrid○ η ⁻¹
                                                ⦙ zap○ (wkᵣ η) idᵣ 0 ⁻¹
                                                ))
                                   ⦙ renlift○ (liftᵣ η) (wkᵣ idᵣ) M
                                   )) ∙∼ refl∼)

renexp⇒∙ : ∀ {Γ Γ′ A B C} → {η : Γ′ ∋⋆ Γ}
                           → (M : Γ ⊢ A ⇒ B ⇒ C) (N : Γ ⊢ A)
                           → ren η (M ∙ N) ∼ ren η (ƛ (wk (M ∙ N) ∙ 0))
renexp⇒∙ {η = η} M N = exp⇒ (ren η M ∙ ren η N)
                      ⦙ ƛ∼ ((≡→∼ ( ren○ (wkᵣ idᵣ) η M ⁻¹
                                  ⦙ (λ η′ → ren η′ M)
                                    & ( wklid○ η
                                      ⦙ wkrid○ η ⁻¹
                                      ⦙ wk○ η idᵣ ⁻¹
                                      )
                                  ⦙ renliftwk○ η idᵣ M
                                  )
                             ∙∼
                             ≡→∼ ( ren○ (wkᵣ idᵣ) η N ⁻¹
                                  ⦙ (λ η′ → ren η′ N)
                                    & ( wklid○ η
                                      ⦙ wkrid○ η ⁻¹
                                      ⦙ wk○ η idᵣ ⁻¹
                                      )
                                  ⦙ renliftwk○ η idᵣ N
                                  )) ∙∼ refl∼)

ren∼ : ∀ {Γ Γ′ A} → {η : Γ′ ∋⋆ Γ} {M₁ M₂ : Γ ⊢ A}
                  → M₁ ∼ M₂
                  → ren η M₁ ∼ ren η M₂
ren∼ refl∼           = refl∼
ren∼ (p ⁻¹∼)         = ren∼ p ⁻¹
ren∼ (p ⦙∼ q)        = ren∼ p ⦙ ren∼ q
ren∼ (ƛ∼ p)          = ƛ∼ (ren∼ p)
ren∼ (p ∙∼ q)        = ren∼ p ∙∼ ren∼ q
ren∼ (red⇒ σ M N)   = renred⇒ σ M N
ren∼ (exp⇒ (𝓋 i))   = renexp⇒𝓋 i
ren∼ (exp⇒ (ƛ M))   = renexp⇒ƛ M
ren∼ (exp⇒ (M ∙ N)) = renexp⇒∙ M N

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

subred⇒ : ∀ {Γ Ξ Φ A B} → {σ₁ : Γ ⊢⋆ Ξ}
                         → (σ₂ : Ξ ⊢⋆ Φ) (M : Φ , A ⊢ B) (N : Ξ ⊢ A)
                         → sub σ₁ (sub σ₂ (ƛ M) ∙ N) ∼ sub σ₁ (sub (σ₂ , N) M)
subred⇒ {σ₁ = σ₁} σ₂ M N = ƛ∼ (≡→∼ (sublift● σ₁ σ₂ M ⁻¹)) ∙∼ refl∼
                          ⦙ red⇒ (σ₁ ● σ₂) M (sub σ₁ N)
                          ⦙ ≡→∼ (sub● σ₁ (σ₂ , N) M)

subexp⇒𝓋 : ∀ {Γ Ξ A B} → {σ : Γ ⊢⋆ Ξ}
                        → (i : Ξ ∋ A ⇒ B)
                        → sub σ (𝓋 i) ∼ sub σ (ƛ (wk (𝓋 i) ∙ 0))
subexp⇒𝓋 {σ = σ} i = exp⇒ (getₛ σ i)
                    ⦙ ƛ∼ (≡→∼ ( natgetₛ σ i ⁻¹
                               ⦙ (λ σ′ → getₛ σ′ i) & liftwkrid◐ σ ⁻¹
                               ⦙ get◐ (liftₛ σ) (wkᵣ idᵣ) i
                               ) ∙∼ refl∼)

subexp⇒ƛ : ∀ {Γ Ξ A B} → {σ : Γ ⊢⋆ Ξ}
                        → (M : Ξ , A ⊢ B)
                        → sub σ (ƛ M) ∼ sub σ (ƛ (wk (ƛ M) ∙ 0))
subexp⇒ƛ {σ = σ} M = ƛ∼ ( ≡→∼ ( (λ σ′ → sub σ′ M)
                                  & ((_, 0)
                                     & ( rid◐ (wkₛ σ) ⁻¹
                                       ⦙ zap◐ (wkₛ σ) idᵣ 0 ⁻¹
                                       ⦙ zap◐ (liftₛ σ) (wkᵣ idᵣ) 0 ⁻¹
                                       ))
                                ⦙ sub◐ (liftₛ σ , 0) (liftᵣ (wkᵣ idᵣ)) M
                                )
                         ⦙ red⇒ (liftₛ σ) (ren (liftᵣ (wkᵣ idᵣ)) M) 0 ⁻¹
                         )

subexp⇒∙ : ∀ {Γ Ξ A B C} → {σ : Γ ⊢⋆ Ξ}
                          → (M : Ξ ⊢ A ⇒ B ⇒ C) (N : Ξ ⊢ A)
                          → sub σ (M ∙ N) ∼ sub σ (ƛ (wk (M ∙ N) ∙ 0))
subexp⇒∙ {σ = σ} M N = exp⇒ (sub σ M ∙ sub σ N)
                      ⦙ ƛ∼ ((≡→∼ ( sub◑ (wkᵣ idᵣ) σ M ⁻¹
                                  ⦙ (λ σ′ → sub σ′ M)
                                    & ( wklid◑ σ
                                      ⦙ wkrid◐ σ ⁻¹
                                      ⦙ wk◐ σ idᵣ ⁻¹
                                      )
                                  ⦙ subliftwk◐ σ idᵣ M
                                  )
                             ∙∼
                             ≡→∼ ( sub◑ (wkᵣ idᵣ) σ N ⁻¹
                                  ⦙ (λ σ′ → sub σ′ N)
                                    & ( wklid◑ σ
                                      ⦙ wkrid◐ σ ⁻¹
                                      ⦙ wk◐ σ idᵣ ⁻¹
                                      )
                                  ⦙ subliftwk◐ σ idᵣ N
                                  )) ∙∼ refl∼)

sub∼ : ∀ {Γ Ξ A} → {σ : Γ ⊢⋆ Ξ} {M₁ M₂ : Ξ ⊢ A}
                 → M₁ ∼ M₂
                 → sub σ M₁ ∼ sub σ M₂
sub∼ refl∼           = refl∼
sub∼ (p ⁻¹∼)         = sub∼ p ⁻¹
sub∼ (p ⦙∼ q)        = sub∼ p ⦙ sub∼ q
sub∼ (ƛ∼ p)          = ƛ∼ (sub∼ p)
sub∼ (p ∙∼ q)        = sub∼ p ∙∼ sub∼ q
sub∼ (red⇒ σ M N)   = subred⇒ σ M N
sub∼ (exp⇒ (𝓋 i))   = subexp⇒𝓋 i
sub∼ (exp⇒ (ƛ M))   = subexp⇒ƛ M
sub∼ (exp⇒ (M ∙ N)) = subexp⇒∙ M N

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

-- Convertibility of substitutions
infix 3 _∼⋆_
data _∼⋆_ : ∀ {Γ Ξ} → Γ ⊢⋆ Ξ → Γ ⊢⋆ Ξ → Set
  where
    ∅   : ∀ {Γ} → ∅ {Γ} ∼⋆ ∅

    _,_ : ∀ {Γ Ξ A} → {σ₁ σ₂ : Γ ⊢⋆ Ξ} {M₁ M₂ : Γ ⊢ A}
                    → (χ : σ₁ ∼⋆ σ₂) (p : M₁ ∼ M₂)
                    → σ₁ , M₁ ∼⋆ σ₂ , M₂

refl∼⋆ : ∀ {Γ Ξ} → {σ : Γ ⊢⋆ Ξ}
                 → σ ∼⋆ σ
refl∼⋆ {σ = ∅}     = ∅
refl∼⋆ {σ = σ , M} = refl∼⋆ , refl∼

_⁻¹∼⋆ : ∀ {Γ Ξ} → {σ₁ σ₂ : Γ ⊢⋆ Ξ}
                → σ₁ ∼⋆ σ₂
                → σ₂ ∼⋆ σ₁
∅       ⁻¹∼⋆ = ∅
(χ , p) ⁻¹∼⋆ = χ ⁻¹∼⋆ , p ⁻¹

_⦙∼⋆_ : ∀ {Γ Ξ} → {σ₁ σ₂ σ₃ : Γ ⊢⋆ Ξ}
                → σ₁ ∼⋆ σ₂ → σ₂ ∼⋆ σ₃
                → σ₁ ∼⋆ σ₃
∅        ⦙∼⋆ ∅        = ∅
(χ₁ , p) ⦙∼⋆ (χ₂ , q) = (χ₁ ⦙∼⋆ χ₂) , (p ⦙ q)

≡→∼⋆ : ∀ {Γ Ξ} → {σ₁ σ₂ : Γ ⊢⋆ Ξ}
                → σ₁ ≡ σ₂
                → σ₁ ∼⋆ σ₂
≡→∼⋆ refl = refl∼⋆

instance
  per∼⋆ : ∀ {Γ Ξ} → PER (Γ ⊢⋆ Ξ) _∼⋆_
  per∼⋆ =
    record
      { _⁻¹ = _⁻¹∼⋆
      ; _⦙_ = _⦙∼⋆_
      }

wk∼⋆ : ∀ {A Γ Ξ} → {σ₁ σ₂ : Γ ⊢⋆ Ξ}
                 → σ₁ ∼⋆ σ₂
                 → wkₛ {A} σ₁ ∼⋆ wkₛ σ₂
wk∼⋆ ∅       = ∅
wk∼⋆ (χ , p) = wk∼⋆ χ , ren∼ p

lift∼⋆ : ∀ {A Γ Ξ} → {σ₁ σ₂ : Γ ⊢⋆ Ξ}
                   → σ₁ ∼⋆ σ₂
                   → liftₛ {A} σ₁ ∼⋆ liftₛ σ₂
lift∼⋆ ∅       = ∅ , refl∼
lift∼⋆ (χ , p) = wk∼⋆ χ , ren∼ p , refl∼

-- NOTE: Needs getₛ σ₁ i ∼ getₛ σ₂ i
-- ◐∼⋆ : ∀ {Γ Ξ Ξ′} → {σ₁ σ₂ : Γ ⊢⋆ Ξ′} {η : Ξ′ ∋⋆ Ξ}
--                  → σ₁ ∼⋆ σ₂ → σ₁ ◐ η ∼⋆ σ₂ ◐ η
-- ◐∼⋆ {η = ∅}        χ = ∅
-- ◐∼⋆ {η = [ η , i ]} χ = [ ◐∼⋆ χ , {!!} ]

◑∼⋆ : ∀ {Γ Γ′ Ξ} → {η : Γ′ ∋⋆ Γ} {σ₁ σ₂ : Γ ⊢⋆ Ξ}
                 → σ₁ ∼⋆ σ₂
                 → η ◑ σ₁ ∼⋆ η ◑ σ₂
◑∼⋆ ∅       = ∅
◑∼⋆ (χ , p) = ◑∼⋆ χ , sub∼ p

-- NOTE: Needs a more general sub∼
-- ●∼⋆ : ∀ {Γ Ξ Φ} → {σ₁ σ₂ : Γ ⊢⋆ Ξ} {τ₁ τ₂ : Ξ ⊢⋆ Φ}
--                 → σ₁ ∼⋆ σ₂ → τ₁ ∼⋆ τ₂
--                 → σ₁ ● τ₁ ∼⋆ σ₂ ● τ₂
-- ●∼⋆ χ₁ ∅         = ∅
-- ●∼⋆ χ₁ [ χ₂ , p ] = [ ●∼⋆ χ₁ χ₂ , {!!} ]

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


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

module Data.Bag where

open import Prelude
open import Algebra
open import Path.Reasoning

infixr 5 _∷_
data ⟅_⟆ (A : Type a) : Type a where
  []     : ⟅ A ⟆
  _∷_    : A → ⟅ A ⟆ → ⟅ A ⟆
  com    : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc  : isSet ⟅ A ⟆

record Elim {a ℓ}
             (A : Type a)
             (P : ⟅ A ⟆ → Type ℓ)
             : Type (a ℓ⊔ ℓ) where
  constructor elim
  field
    ⟅_⟆-set : ∀ {xs} → isSet (P xs)
    ⟅_⟆[] : P []
    ⟅_⟆_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
  private z = ⟅_⟆[]; f = ⟅_⟆_∷_⟨_⟩
  field
    ⟅_⟆-com : (∀ x y xs pxs →
      PathP  (λ i → P (com x y xs i))
             (f x (y ∷ xs) (f y xs pxs))
             (f y (x ∷ xs) (f x xs pxs)))
  ⟅_⟆⇓ : (xs : ⟅ A ⟆) → P xs
  ⟅ [] ⟆⇓ = z
  ⟅ x ∷ xs ⟆⇓ = f x xs ⟅ xs ⟆⇓
  ⟅ com x y xs i ⟆⇓ = ⟅_⟆-com x y xs ⟅ xs ⟆⇓ i
  ⟅ trunc xs ys x y i j ⟆⇓ =
    isOfHLevel→isOfHLevelDep 2
      (λ xs → ⟅_⟆-set {xs})
      ⟅ xs ⟆⇓ ⟅ ys ⟆⇓
      (cong ⟅_⟆⇓ x) (cong ⟅_⟆⇓ y)
      (trunc xs ys x y)
      i j

open Elim

infixr 0 elim-syntax
elim-syntax  : ∀ {a ℓ}
             → (A : Type a)
             → (⟅ A ⟆ → Type ℓ)
             → Type (a ℓ⊔ ℓ)
elim-syntax = Elim

syntax elim-syntax A (λ xs → Pxs) = xs ⦂⟅ A ⟆→ Pxs

record ElimProp {a ℓ} (A : Type a) (P : ⟅ A ⟆ → Type ℓ) : Type (a ℓ⊔ ℓ) where
  constructor elim-prop
  field
    ⟦_⟧-prop : ∀ {xs} → isProp (P xs)
    ⟦_⟧[] : P []
    ⟦_⟧_∷_⟨_⟩ : ∀ x xs → P xs → P (x ∷ xs)
  private z = ⟦_⟧[]; f = ⟦_⟧_∷_⟨_⟩
  ⟦_⟧⇑ = elim
          (isProp→isSet ⟦_⟧-prop)
          z f
          (λ x y xs pxs → toPathP (⟦_⟧-prop (transp (λ i → P (com x y xs i)) i0
            (f x (y ∷ xs) (f y xs pxs))) (f y (x ∷ xs) (f x xs pxs))))
  ⟦_⟧⇓ = ⟅ ⟦_⟧⇑ ⟆⇓

open ElimProp

infixr 0 elim-prop-syntax
elim-prop-syntax : ∀ {a ℓ} → (A : Type a) → (⟅ A ⟆ → Type ℓ) → Type (a ℓ⊔ ℓ)
elim-prop-syntax = ElimProp

syntax elim-prop-syntax A (λ xs → Pxs) = xs ⦂⟅ A ⟆→∥ Pxs ∥

record [⟅_⟆→_] {a b} (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  constructor rec
  field
    [_]-set  : isSet B
    [_]_∷_ : A → B → B
    [_][]    : B
  private f = [_]_∷_; z = [_][]
  field
    [_]-com : ∀ x y xs → f x (f y xs) ≡ f y (f x xs)
  [_]⇑ = elim [_]-set z (λ x _ → f x) (λ x y _ → [_]-com x y)
  [_]↓ = ⟅ [_]⇑ ⟆⇓
open [⟅_⟆→_]

infixr 5 _∪_
_∪_ : ⟅ A ⟆ → ⟅ A ⟆ → ⟅ A ⟆
_∪_ = λ xs ys → [ ys ∪′ ]↓ xs
  where
  _∪′ : ⟅ A ⟆ → [⟅ A ⟆→ ⟅ A ⟆ ]
  [ ys ∪′ ]-set = trunc
  [ ys ∪′ ] x ∷ xs = x ∷ xs
  [ ys ∪′ ][] = ys
  [ ys ∪′ ]-com = com

∪-assoc : (xs ys zs : ⟅ A ⟆) →
  (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs)
∪-assoc = λ xs ys zs → ⟦ ∪-assoc′ ys zs ⟧⇓ xs
  where
  ∪-assoc′ : ∀ ys zs →
    xs ⦂⟅ A ⟆→∥ (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs) ∥
  ⟦ ∪-assoc′ ys zs ⟧-prop = trunc _ _
  ⟦ ∪-assoc′ ys zs ⟧[] = refl
  ⟦ ∪-assoc′ ys zs ⟧ x ∷ xs ⟨ P ⟩ = cong (x ∷_) P

∪-cons  : ∀ (x : A) xs ys
        → (x ∷ xs) ∪ ys ≡ xs ∪ (x ∷ ys)
∪-cons = λ x xs ys → ⟦ ∪-cons′ x ys ⟧⇓ xs
  where
  ∪-cons′ : ∀ x ys →
    xs ⦂⟅ A ⟆→∥ (x ∷ xs) ∪ ys ≡ xs ∪ (x ∷ ys) ∥
  ⟦ ∪-cons′ x ys ⟧-prop = trunc _ _
  ⟦ ∪-cons′ x ys ⟧[] = refl
  ⟦ ∪-cons′ x ys ⟧ y ∷ xs ⟨ P ⟩ = cong (_∪ ys) (com x y xs) ; cong (y ∷_) P

∪-idʳ : (xs : ⟅ A ⟆) → xs ∪ [] ≡ xs
∪-idʳ = ⟦ ∪-idʳ′ ⟧⇓
  where
  ∪-idʳ′ : xs ⦂⟅ A ⟆→∥ xs ∪ [] ≡ xs ∥
  ⟦ ∪-idʳ′ ⟧-prop = trunc _ _
  ⟦ ∪-idʳ′ ⟧[] = refl
  ⟦ ∪-idʳ′ ⟧ x ∷ xs ⟨ P ⟩ = cong (x ∷_) P

∪-comm : (xs ys : ⟅ A ⟆) → xs ∪ ys ≡ ys ∪ xs
∪-comm {A = A} = λ xs ys → ⟦ ∪-comm′ ys ⟧⇓ xs
  where
  ∪-comm′ : (ys : ⟅ A ⟆) →
    xs ⦂⟅ A ⟆→∥ xs ∪ ys ≡ ys ∪ xs ∥
  ⟦ ∪-comm′ ys ⟧-prop = trunc _ _
  ⟦ ∪-comm′ ys ⟧[] = sym (∪-idʳ ys)
  ⟦ ∪-comm′ ys ⟧ x ∷ xs ⟨ P ⟩ =
    (x ∷ xs) ∪ ys ≡⟨ cong (x ∷_) P ⟩
    (x ∷ ys) ∪ xs ≡⟨ ∪-cons x ys xs ⟩
    ys ∪ x ∷ xs ∎

⟅⟆-commutative-monoid : ∀ {a} (A : Type a) → CommutativeMonoid _
Monoid.𝑆 (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) = ⟅ A ⟆
Monoid._∙_ (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) = _∪_
Monoid.ε (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) = []
Monoid.assoc (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) = ∪-assoc
Monoid.ε∙ (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) _ = refl
Monoid.∙ε (CommutativeMonoid.monoid (⟅⟆-commutative-monoid A)) = ∪-idʳ
CommutativeMonoid.comm (⟅⟆-commutative-monoid A) = ∪-comm

module _ {ℓ} (mon : CommutativeMonoid ℓ) (sIsSet : isSet (CommutativeMonoid.𝑆 mon)) where
  open CommutativeMonoid mon
  ⟦_⟧ : (A → 𝑆) → ⟅ A ⟆ → 𝑆
  ⟦_⟧ = λ h → [ ⟦ h ⟧′ ]↓
    where
    ⟦_⟧′ : (A → 𝑆) → [⟅ A ⟆→ 𝑆 ]
    [ ⟦ h ⟧′ ] x ∷ xs = h x ∙ xs
    [ ⟦ h ⟧′ ][] = ε
    [ ⟦ h ⟧′ ]-com x y xs =
      h x ∙ (h y ∙ xs)
        ≡˘⟨ assoc _ _ _ ⟩
      (h x ∙ h y) ∙ xs
        ≡⟨ cong (_∙ xs) (comm _ _) ⟩
      (h y ∙ h x) ∙ xs
        ≡⟨ assoc _ _ _ ⟩
      h y ∙ (h x ∙ xs) ∎
    [ ⟦ h ⟧′ ]-set = sIsSet

record ⟦_≡_⟧ {a b} {A : Type a} {B : Type b}
            (h : ⟅ A ⟆ → B)
            (xf : [⟅ A ⟆→ B ])
            : Type (a ℓ⊔ b) where
  constructor elim-univ
  field
    ⟦_≡⟧_∷_ : ∀ x xs → h (x ∷ xs) ≡ [ xf ] x ∷ h xs
    ⟦_≡⟧[] : h [] ≡ [ xf ][]
  ⟦_≡⟧⇓ : ∀ xs → h xs ≡ [ xf ]↓ xs
  ⟦_≡⟧⇓ = ⟦ ≡⇓′ ⟧⇓
    where
    ≡⇓′ : xs ⦂⟅ A ⟆→∥ h xs ≡ [ xf ]↓ xs ∥
    ⟦ ≡⇓′ ⟧-prop = [ xf ]-set _ _
    ⟦ ≡⇓′ ⟧[] = ⟦_≡⟧[]
    ⟦ ≡⇓′ ⟧ x ∷ xs ⟨ P ⟩ = ⟦_≡⟧_∷_ x _ ; cong ([ xf ] x ∷_) P
open ⟦_≡_⟧

record ⟦_⊚_≡_⟧ {a b c} {A : Type a} {B : Type b} {C : Type c}
               (h : B → C)
               (xf : [⟅ A ⟆→ B ])
               (yf : [⟅ A ⟆→ C ])
               : Type (a ℓ⊔ b ℓ⊔ c)
    where
  constructor elim-fuse
  field
    ⟦_∘≡⟧_∷_ : ∀ x xs → h ([ xf ] x ∷ xs) ≡ [ yf ] x ∷ h xs
    ⟦_∘≡⟧[] : h [ xf ][] ≡ [ yf ][]
  ⟦_∘≡⟧⇓ : ∀ xs → h ([ xf ]↓ xs) ≡ [ yf ]↓ xs
  ⟦_∘≡⟧⇓ = ⟦ ≡⇓′ ⟧⇓
    where
    ≡⇓′ : xs ⦂⟅ A ⟆→∥ h ([ xf ]↓ xs) ≡ [ yf ]↓ xs ∥
    ⟦ ≡⇓′ ⟧-prop = [ yf ]-set _ _
    ⟦ ≡⇓′ ⟧[] = ⟦_∘≡⟧[]
    ⟦ ≡⇓′ ⟧ x ∷ xs ⟨ P ⟩ = ⟦_∘≡⟧_∷_ x _ ; cong ([ yf ] x ∷_) P
open ⟦_⊚_≡_⟧

map-alg : (A → B) → [⟅ A ⟆→ ⟅ B ⟆ ]
[ map-alg f ]-set = trunc
[ map-alg f ][] = []
[ map-alg f ] x ∷ xs = f x ∷ xs
[ map-alg f ]-com x y = com (f x) (f y)

map : (A → B) → ⟅ A ⟆ → ⟅ B ⟆
map f = [ map-alg f ]↓

[_]∘_ : [⟅ B ⟆→ C ] → (A → B) → [⟅ A ⟆→ C ]
[ [ g ]∘ f ]-set      = [ g ]-set
[ [ g ]∘ f ][]        = [ g ][]
[ [ g ]∘ f ] x ∷ xs   = [ g ] f x ∷ xs
[ [ g ]∘ f ]-com x y  = [ g ]-com (f x) (f y)

map-fuse  : ∀ (g : [⟅ B ⟆→ C ]) (f : A → B)
          → [ g ]↓ ∘ map f ≡ [ [ g ]∘ f ]↓
map-fuse g f = funExt ⟦ map-fuse′ g f ∘≡⟧⇓
  where
  map-fuse′  : (g : [⟅ B ⟆→ C ]) (f : A → B)
             → ⟦ [ g ]↓ ⊚ map-alg f ≡ [ g ]∘ f ⟧
  ⟦ map-fuse′ g f ∘≡⟧ x ∷ xs = refl
  ⟦ map-fuse′ g f ∘≡⟧[] = refl

bind : ⟅ A ⟆ → (A → ⟅ B ⟆) → ⟅ B ⟆
bind xs f = ⟦ ⟅⟆-commutative-monoid _ ⟧ trunc f xs

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
record R (A : Set) : Set₁ where
  field
    P : A → Set
    p : (x : A) → P x

module M (r : (A : Set) → R A) where

  open module R′ {A : Set} = R (r A) public

postulate
  r : (A : Set) → R A
  A : Set

open M r

internal-error : (x : A) → P x
internal-error x = p

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-08-23, issue #2714

-- Make sure we produce a warning about missing main function
-- even though we import a module with --no-main.

open import Issue2712

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

open import Common.Prelude

case_of_ : {A B : Set} → A → (A → B) → B
case x of f = f x
{-# INLINE case_of_ #-}

patlam : Nat → Nat
patlam zero = zero
patlam (suc n) =
  case n of λ
  { zero    → zero
  ; (suc m) → m + patlam n
  }

static : {A : Set} → A → A
static x = x
{-# STATIC static #-}

-- The static here will make the compiler get to the pattern lambda in the body of patlam
-- before compiling patlam. If we're not careful this might make the pattern lambda not
-- inline in the body of patlam.
foo : Nat → Nat
foo n = static (patlam (suc n))

main : IO Unit
main = printNat (foo 5)


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Function using (_∘_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin hiding (_+_; #_)

open import DeBruijn

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

⟪_⟫ : ∀ {n m} → Subst n m → Term n → Term m
⟪ σ ⟫ = subst σ

ids : ∀ {n} → Subst n n
ids x = # x

↑ : ∀ {n} → Subst n (suc n)
↑ x = # (suc x)

infix 6 _•_

_•_ : ∀ {n m} → Term m → Subst n m → Subst (suc n) m
(M • σ) zero    = M
(M • σ) (suc x) = σ x

infixr 5 _⨟_

_⨟_ : ∀ {n k m} → Subst n k → Subst k m → Subst n m
σ ⨟ τ = ⟪ τ ⟫ ∘ σ

ren : ∀ {n m} → Rename n m → Subst n m
ren ρ = ids ∘ ρ

sub-head : ∀ {n m} {M : Term m} {σ : Subst n m}
         → ⟪ M • σ ⟫ (# zero) ≡ M
sub-head = refl

sub-tail : ∀ {n m} {M : Term m} {σ : Subst n m}
         → (↑ ⨟ M • σ) ≡ σ
sub-tail = extensionality λ x → refl

sub-idL : ∀ {n m} {σ : Subst n m}
       → ids ⨟ σ ≡ σ
sub-idL = extensionality λ x → refl

sub-dist :  ∀ {n m k} {σ : Subst n m} {τ : Subst m k} {M : Term m}
         → ((M • σ) ⨟ τ) ≡ ((subst τ M) • (σ ⨟ τ))
sub-dist {n}{m}{k}{σ}{τ}{M} = extensionality λ x → lemma {x = x}
  where
  lemma : ∀ {x : Fin (suc n)} → ((M • σ) ⨟ τ) x ≡ ((subst τ M) • (σ ⨟ τ)) x
  lemma {x = zero} = refl
  lemma {x = suc x} = refl

cong-ext : ∀ {n m}{ρ ρ′ : Rename n m}
  → (ρ ≡ ρ′)
    ---------------------------------
  → ext ρ ≡ ext ρ′
cong-ext{n}{m}{ρ}{ρ′} rr = extensionality λ x → lemma {x}
  where
  lemma : ∀ {x : Fin (suc n)} → ext ρ x ≡ ext ρ′ x
  lemma {zero} = refl
  lemma {suc y} = cong suc (cong-app rr y)

cong-rename : ∀ {n m}{ρ ρ′ : Rename n m}{M M′ : Term n}
  → ρ ≡ ρ′
  → M ≡ M′
    ------------------------
  → rename ρ M ≡ rename ρ′ M
cong-rename {M = # x} rr refl = cong #_ (cong-app rr x)
cong-rename {ρ = ρ} {ρ′ = ρ′} {M = ƛ N} rr refl =
   cong ƛ_ (cong-rename {ρ = ext ρ}{ρ′ = ext ρ′}{M = N} (cong-ext rr) refl)
cong-rename {M = L · M} rr refl =
   cong₂ _·_ (cong-rename rr refl) (cong-rename rr refl)

cong-exts : ∀ {n m}{σ σ′ : Subst n m}
   → σ ≡ σ′
     ----------------
   → exts σ ≡ exts σ′
cong-exts{n}{m}{σ}{σ′} ss = extensionality λ x → lemma {x}
   where
   lemma : ∀ {x} → exts σ x ≡ exts σ′ x
   lemma {zero} = refl
   lemma {suc x} = cong (rename suc) (cong-app (ss) x)

cong-sub : ∀ {n m}{σ σ′ : Subst n m}{M M′ : Term n}
  → σ ≡ σ′
  → M ≡ M′
    -----------------------
  → subst σ M ≡ subst σ′ M′
cong-sub {n}{m}{σ}{σ′}{# x} ss refl = cong-app ss x
cong-sub {n}{m}{σ}{σ′}{ƛ M} ss refl =
   cong ƛ_ (cong-sub {σ = exts σ}{σ′ = exts σ′} {M = M} (cong-exts ss) refl)
cong-sub {n}{m}{σ}{σ′}{L · M} ss refl =
   cong₂ _·_ (cong-sub {M = L} ss refl) (cong-sub {M = M} ss refl)

cong-sub-zero : ∀ {n} {M M′ : Term n}
  → M ≡ M′
    ----------------------------
  → subst-zero M ≡ subst-zero M′
cong-sub-zero {n}{M}{M′} mm′ =
   extensionality λ x → cong (λ z → subst-zero z x) mm′

cong-cons : ∀ {n m}{M N : Term m}{σ τ : Subst n m}
  → M ≡ N
  → σ ≡ τ
    -----------------
  → (M • σ) ≡ (N • τ)
cong-cons{n}{m}{M}{N}{σ}{τ} refl st = extensionality lemma
  where
  lemma : (x : Fin (suc n)) → (M • σ) x ≡ (M • τ) x
  lemma zero = refl
  lemma (suc x) = cong-app st x

cong-seq : ∀ {n m k}{σ σ′ : Subst n m}{τ τ′ : Subst m k}
  → (σ ≡ σ′) → (τ ≡ τ′)
  → (σ ⨟ τ) ≡ (σ′ ⨟ τ′)
cong-seq {n}{m}{k}{σ}{σ′}{τ}{τ′} ss′ tt′ = extensionality lemma
  where
  lemma : (x : Fin n) → (σ ⨟ τ) x ≡ (σ′ ⨟ τ′) x
  lemma x =
     begin
       (σ ⨟ τ) x
     ≡⟨⟩
       subst τ (σ x)
     ≡⟨ cong (subst τ) (cong-app ss′ x) ⟩
       subst τ (σ′ x)
     ≡⟨ cong-sub{M = σ′ x} tt′ refl ⟩
       subst τ′ (σ′ x)
     ≡⟨⟩
       (σ′ ⨟ τ′) x
     ∎

ren-ext : ∀ {n m} {ρ : Rename n m}
        → ren (ext ρ) ≡ exts (ren ρ)
ren-ext {n}{m}{ρ} = extensionality λ x → lemma {x = x}
  where
  lemma : ∀ {x : Fin (suc n)} → (ren (ext ρ)) x ≡ exts (ren ρ) x
  lemma {x = zero} = refl
  lemma {x = suc x} = refl

rename-subst-ren : ∀ {n m} {ρ : Rename n m} {M : Term n}
                 → rename ρ M ≡ ⟪ ren ρ ⟫ M
rename-subst-ren {M = # x} = refl
rename-subst-ren {n}{ρ = ρ}{M = ƛ N} =
  begin
      rename ρ (ƛ N)
    ≡⟨⟩
      ƛ rename (ext ρ) N
    ≡⟨ cong ƛ_ (rename-subst-ren {ρ = ext ρ}{M = N}) ⟩
      ƛ ⟪ ren (ext ρ) ⟫ N
    ≡⟨ cong ƛ_ (cong-sub{M = N} ren-ext refl) ⟩
      ƛ ⟪ exts (ren ρ) ⟫ N
    ≡⟨⟩
      ⟪ ren ρ ⟫ (ƛ N)
  ∎
rename-subst-ren {M = L · M} = cong₂ _·_ rename-subst-ren rename-subst-ren

exts-cons-shift : ∀ {n m} {σ : Subst n m}
                → exts σ  ≡ (# zero • (σ ⨟ ↑))
exts-cons-shift = extensionality λ x → lemma{x = x}
  where
  lemma : ∀ {n m} {σ : Subst n m} {x : Fin (suc n)}
                  → exts σ x ≡ (# zero • (σ ⨟ ↑)) x
  lemma {x = zero} = refl
  lemma {x = suc y} = rename-subst-ren

subst-zero-cons-ids : ∀ {n}{M : Term n}
                 → subst-zero M ≡ (M • ids)
subst-zero-cons-ids = extensionality λ x → lemma {x = x}
  where
  lemma : ∀ {n}{M : Term n}{x : Fin (suc n)}
        → subst-zero M x ≡ (M • ids) x
  lemma {x = zero} = refl
  lemma {x = suc x} = refl

exts-ids : ∀ {n}
         → exts ids ≡ ids {suc n}
exts-ids {n} = extensionality lemma
  where lemma : (x : Fin (suc n)) → exts ids x ≡ ids x
        lemma zero = refl
        lemma (suc x) = refl

sub-id : ∀ {n} {M : Term n}
         → ⟪ ids ⟫ M ≡ M
sub-id {M = # x} = refl
sub-id {M = ƛ N} =
   begin
     ⟪ ids ⟫ (ƛ N)
   ≡⟨⟩
     ƛ ⟪ exts ids ⟫ N
   ≡⟨ cong ƛ_ (cong-sub{M = N} exts-ids refl)  ⟩
     ƛ ⟪ ids ⟫ N
   ≡⟨ cong ƛ_ sub-id ⟩
     ƛ N
   ∎
sub-id {M = L · M} = cong₂ _·_ sub-id sub-id

sub-idR : ∀ {n m} {σ : Subst n m}
       → (σ ⨟ ids) ≡ σ
sub-idR {n}{σ = σ} =
          begin
            σ ⨟ ids
          ≡⟨⟩
            ⟪ ids ⟫ ∘ σ
          ≡⟨ extensionality (λ x → sub-id) ⟩
            σ
          ∎

compose-ext : ∀ {n m k}{ρ : Rename m k} {ρ′ : Rename n m}
            → ((ext ρ) ∘ (ext ρ′)) ≡ ext (ρ ∘ ρ′)
compose-ext = extensionality λ x → lemma {x = x}
  where
  lemma : ∀ {n m k}{ρ : Rename m k} {ρ′ : Rename n m} {x : Fin (suc n)}
              → ((ext ρ) ∘ (ext ρ′)) x ≡ ext (ρ ∘ ρ′) x
  lemma {x = zero} = refl
  lemma {x = suc x} = refl

compose-rename : ∀ {n m k}{M : Term n}{ρ : Rename m k}{ρ′ : Rename n m}
  → rename ρ (rename ρ′ M) ≡ rename (ρ ∘ ρ′) M
compose-rename {M = # x} = refl
compose-rename {n}{m}{k}{ƛ N}{ρ}{ρ′} = cong ƛ_ G
  where
  G : rename (ext ρ) (rename (ext ρ′) N) ≡ rename (ext (ρ ∘ ρ′)) N
  G =
      begin
        rename (ext ρ) (rename (ext ρ′) N)
      ≡⟨ compose-rename{ρ = ext ρ}{ρ′ = ext ρ′} ⟩
        rename ((ext ρ) ∘ (ext ρ′)) N
      ≡⟨ cong-rename compose-ext refl ⟩
        rename (ext (ρ ∘ ρ′)) N
      ∎
compose-rename {M = L · M} = cong₂ _·_ compose-rename compose-rename

commute-subst-rename : ∀ {n m}{M : Term n}{σ : Subst n m}
                        {ρ : ∀ {n} → Rename n (suc n)}
     → (∀ {x : Fin n} → exts σ (ρ x) ≡ rename ρ (σ x))
     → subst (exts σ) (rename ρ M) ≡ rename ρ (subst σ M)
commute-subst-rename {M = # x} r = r
commute-subst-rename{n}{m}{ƛ N}{σ}{ρ} r =
   cong ƛ_ (commute-subst-rename{suc n}{suc m}{N}
               {exts σ}{ρ = ρ′} (λ {x} → H {x}))
   where
   ρ′ : ∀ {n} → Rename n (suc n)
   ρ′ {zero} = λ ()
   ρ′ {suc n} = ext ρ

   H : {x : Fin (suc n)} → exts (exts σ) (ext ρ x) ≡ rename (ext ρ) (exts σ x)
   H {zero} = refl
   H {suc y} =
     begin
       exts (exts σ) (ext ρ (suc y))
     ≡⟨⟩
       rename suc (exts σ (ρ y))
     ≡⟨ cong (rename suc) r ⟩
       rename suc (rename ρ (σ y))
     ≡⟨ compose-rename ⟩
       rename (suc ∘ ρ) (σ y)
     ≡⟨ cong-rename refl refl ⟩
       rename ((ext ρ) ∘ suc) (σ y)
     ≡⟨ sym compose-rename ⟩
       rename (ext ρ) (rename suc (σ y))
     ≡⟨⟩
       rename (ext ρ) (exts σ (suc y))
     ∎
commute-subst-rename {M = L · M}{ρ = ρ} r =
   cong₂ _·_ (commute-subst-rename{M = L}{ρ = ρ} r)
             (commute-subst-rename{M = M}{ρ = ρ} r)

exts-seq : ∀ {n m m′} {σ₁ : Subst n m} {σ₂ : Subst m m′}
         → (exts σ₁ ⨟ exts σ₂) ≡ exts (σ₁ ⨟ σ₂)
exts-seq = extensionality λ x → lemma {x = x}
  where
  lemma : ∀ {n m m′}{x : Fin (suc n)} {σ₁ : Subst n m}{σ₂ : Subst m m′}
     → (exts σ₁ ⨟ exts σ₂) x ≡ exts (σ₁ ⨟ σ₂) x
  lemma {x = zero} = refl
  lemma {x = suc x}{σ₁}{σ₂} =
     begin
       (exts σ₁ ⨟ exts σ₂) (suc x)
     ≡⟨⟩
       ⟪ exts σ₂ ⟫ (rename suc (σ₁ x))
     ≡⟨ commute-subst-rename{M = σ₁ x}{σ = σ₂}{ρ = suc} refl ⟩
       rename suc (⟪ σ₂ ⟫ (σ₁ x))
     ≡⟨⟩
       rename suc ((σ₁ ⨟ σ₂) x)
     ∎

sub-sub : ∀ {n m k}{M : Term n} {σ₁ : Subst n m}{σ₂ : Subst m k}
            → ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ M) ≡ ⟪ σ₁ ⨟ σ₂ ⟫ M
sub-sub {M = # x} = refl
sub-sub {n}{m}{k}{ƛ N}{σ₁}{σ₂} =
   begin
     ⟪ σ₂ ⟫ (⟪ σ₁ ⟫ (ƛ N))
   ≡⟨⟩
     ƛ ⟪ exts σ₂ ⟫ (⟪ exts σ₁ ⟫ N)
   ≡⟨ cong ƛ_ (sub-sub{M = N}{σ₁ = exts σ₁}{σ₂ = exts σ₂}) ⟩
     ƛ ⟪ exts σ₁ ⨟ exts σ₂ ⟫ N
   ≡⟨ cong ƛ_ (cong-sub{M = N} exts-seq refl) ⟩
     ƛ ⟪ exts ( σ₁ ⨟ σ₂) ⟫ N
   ∎
sub-sub {M = L · M} = cong₂ _·_ (sub-sub{M = L}) (sub-sub{M = M})

rename-subst : ∀ {n m m′}{M : Term n}{ρ : Rename n m}{σ : Subst m m′}
             → ⟪ σ ⟫ (rename ρ M) ≡ ⟪ σ ∘ ρ ⟫ M
rename-subst {n}{m}{m′}{M}{ρ}{σ} =
   begin
     ⟪ σ ⟫ (rename ρ M)
   ≡⟨ cong ⟪ σ ⟫ (rename-subst-ren{M = M}) ⟩
     ⟪ σ ⟫ (⟪ ren ρ ⟫ M)
   ≡⟨ sub-sub{M = M} ⟩
     ⟪ ren ρ ⨟ σ ⟫ M
   ≡⟨⟩
     ⟪ σ ∘ ρ ⟫ M
   ∎

sub-assoc : ∀ {n m k Ψ} {σ : Subst n m} {τ : Subst m k} {θ : Subst k Ψ}
          → (σ ⨟ τ) ⨟ θ ≡ (σ ⨟ τ ⨟ θ)
sub-assoc {n}{m}{k}{Ψ}{σ}{τ}{θ} = extensionality λ x → lemma{x = x}
  where
  lemma : ∀ {x : Fin n} → ((σ ⨟ τ) ⨟ θ) x ≡ (σ ⨟ τ ⨟ θ) x
  lemma {x} =
      begin
        ((σ ⨟ τ) ⨟ θ) x
      ≡⟨⟩
        ⟪ θ ⟫ (⟪ τ ⟫ (σ x))
      ≡⟨ sub-sub{M = σ x} ⟩
        ⟪ τ ⨟ θ ⟫ (σ x)
      ≡⟨⟩
        (σ ⨟ τ ⨟ θ) x
      ∎

subst-zero-exts-cons : ∀ {n m}{σ : Subst n m}{M : Term m}
                     → exts σ ⨟ subst-zero M ≡ (M • σ)
subst-zero-exts-cons {n}{m}{σ}{M} =
    begin
      exts σ ⨟ subst-zero M
    ≡⟨ cong-seq exts-cons-shift subst-zero-cons-ids ⟩
      (# zero • (σ ⨟ ↑)) ⨟ (M • ids)
    ≡⟨ sub-dist ⟩
      (⟪ M • ids ⟫ (# zero)) • ((σ ⨟ ↑) ⨟ (M • ids))
    ≡⟨ cong-cons (sub-head{σ = ids}) refl ⟩
      M • ((σ ⨟ ↑) ⨟ (M • ids))
    ≡⟨ cong-cons refl (sub-assoc{σ = σ}) ⟩
      M • (σ ⨟ (↑ ⨟ (M • ids)))
    ≡⟨ cong-cons refl (cong-seq{σ = σ} refl (sub-tail{M = M}{σ = ids})) ⟩
      M • (σ ⨟ ids)
    ≡⟨ cong-cons refl (sub-idR{σ = σ}) ⟩
      M • σ
    ∎

subst-commute : ∀ {n m} {N : Term (suc n)} {M : Term n} {σ : Subst n m}
  → ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ] ≡ ⟪ σ ⟫ (N [ M ])
subst-commute {n}{m}{N}{M}{σ} =
  begin
    ⟪ exts σ ⟫ N [ ⟪ σ ⟫ M ]
  ≡⟨⟩
    ⟪ subst-zero (⟪ σ ⟫ M) ⟫ (⟪ exts σ ⟫ N)
  ≡⟨ cong-sub {M = ⟪ exts σ ⟫ N} subst-zero-cons-ids refl ⟩
    ⟪ ⟪ σ ⟫ M • ids ⟫ (⟪ exts σ ⟫ N)
  ≡⟨ sub-sub {M = N} ⟩
    ⟪ (exts σ) ⨟ ((⟪ σ ⟫ M) • ids) ⟫ N
  ≡⟨ cong-sub {M = N} (cong-seq exts-cons-shift refl) refl ⟩
  ⟪ (# zero • (σ ⨟ ↑)) ⨟ (⟪ σ ⟫ M • ids) ⟫ N
  ≡⟨ cong-sub {M = N} (sub-dist {M = # zero}) refl ⟩
    ⟪ ⟪ ⟪ σ ⟫ M • ids ⟫ (# zero) • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N
  ≡⟨⟩
    ⟪ ⟪ σ ⟫ M • ((σ ⨟ ↑) ⨟ (⟪ σ ⟫ M • ids)) ⟫ N
  ≡⟨ cong-sub {M = N} (cong-cons refl (sub-assoc {σ = σ})) refl ⟩
    ⟪ ⟪ σ ⟫ M • (σ ⨟ ↑ ⨟ ⟪ σ ⟫ M • ids) ⟫ N
  ≡⟨ cong-sub {M = N} refl refl ⟩
    ⟪ ⟪ σ ⟫ M • (σ ⨟ ids) ⟫ N
  ≡⟨ cong-sub {M = N} (cong-cons refl (sub-idR {σ = σ})) refl ⟩
    ⟪ ⟪ σ ⟫ M • σ ⟫ N
  ≡⟨ cong-sub {M = N} (cong-cons refl (sub-idL {σ = σ})) refl ⟩
    ⟪ ⟪ σ ⟫ M • (ids ⨟ σ) ⟫ N
  ≡⟨ cong-sub {M = N} (sym sub-dist) refl ⟩
    ⟪ M • ids ⨟ σ ⟫ N
  ≡⟨ sym (sub-sub {M = N}) ⟩
    ⟪ σ ⟫ (⟪ M • ids ⟫ N)
  ≡⟨ cong ⟪ σ ⟫ (sym (cong-sub {M = N} subst-zero-cons-ids refl)) ⟩
    ⟪ σ ⟫ (N [ M ])
  ∎

rename-subst-commute : ∀ {n m} {N : Term (suc n)} {M : Term n} {ρ : Rename n m }
  → (rename (ext ρ) N) [ rename ρ M ] ≡ rename ρ (N [ M ])
rename-subst-commute {n}{m}{N}{M}{ρ} =
  begin
    (rename (ext ρ) N) [ rename ρ M ]
  ≡⟨ cong-sub (cong-sub-zero (rename-subst-ren {M = M})) (rename-subst-ren {M = N}) ⟩
    (⟪ ren (ext ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ]
  ≡⟨ cong-sub refl (cong-sub {M = N} ren-ext refl) ⟩
    (⟪ exts (ren ρ) ⟫ N) [ ⟪ ren ρ ⟫ M ]
  ≡⟨ subst-commute {N = N} ⟩
    subst (ren ρ) (N [ M ])
  ≡⟨ sym (rename-subst-ren) ⟩
    rename ρ (N [ M ])
  ∎

infix 8 _〔_〕

_〔_〕 : ∀ {n} → Term (suc (suc n)) → Term n → Term (suc n)
_〔_〕 N M = subst (exts (subst-zero M)) N

substitution-lemma : ∀ {n} {M : Term (suc (suc n))} {N : Term (suc n)} {L : Term n}
  → M [ N ] [ L ] ≡ (M 〔 L 〕) [ (N [ L ]) ]
substitution-lemma {M = M}{N = N}{L = L} =
  sym (subst-commute {N = M}{M = N}{σ = subst-zero L})

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
module Category.Functor.Either where
open import Agda.Primitive using (_⊔_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Category.Functor     using (RawFunctor    ; module RawFunctor    )
open import Category.Applicative using (RawApplicative; module RawApplicative)
open import Function using (_∘_)

Either : ∀ {l₁ l₂} (A : Set l₁) (B : Set l₂) → Set (l₁ ⊔ l₂)
Either = _⊎_

eitherFunctor : ∀ {l₁ l₂} {A : Set l₁} → RawFunctor (Either {l₁} {l₂} A)
eitherFunctor = record
  { _<$>_ = λ f → λ { (inj₁ z) → inj₁ z ; (inj₂ a) → inj₂ (f a) }
  }

eitherApplicative : ∀ {l₁} {A : Set l₁} → RawApplicative (Either {l₁} {l₁} A)
eitherApplicative = record
  { pure = inj₂
  ; _⊛_ = λ { (inj₁ a) → λ _ → inj₁ a ; (inj₂ f) → λ { (inj₁ a) → inj₁ a ; (inj₂ b) → inj₂ (f b) } }
  }

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.FiniteMultiset.Base where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetTruncation
open import Cubical.Foundations.HLevels

private
  variable
    A : Type₀

infixr 5 _∷_

data FMSet (A : Type₀) : Type₀ where
  []    : FMSet A
  _∷_   : (x : A) → (xs : FMSet A) → FMSet A
  comm  : ∀ x y xs → x ∷ y ∷ xs ≡ y ∷ x ∷ xs
  trunc : isSet (FMSet A)

pattern [_] x = x ∷ []

module FMSetElim {ℓ} {B : FMSet A → Type ℓ}
  ([]* : B []) (_∷*_ : (x : A) {xs : FMSet A} → B xs → B (x ∷ xs))
  (comm* : (x y : A) {xs : FMSet A} (b : B xs)
         → PathP (λ i → B (comm x y xs i)) (x ∷* (y ∷* b)) (y ∷* (x ∷* b)))
  (trunc* : (xs : FMSet A) → isSet (B xs)) where

  f : (xs : FMSet A) → B xs
  f [] = []*
  f (x ∷ xs) = x ∷* f xs
  f (comm x y xs i) = comm* x y (f xs) i
  f (trunc xs zs p q i j) =
    isOfHLevel→isOfHLevelDep {n = 2} trunc*  (f xs) (f zs) (cong f p) (cong f q) (trunc xs zs p q) i j

module FMSetElimProp {ℓ} {B : FMSet A → Type ℓ} (BProp : {xs : FMSet A} → isProp (B xs))
  ([]* : B []) (_∷*_ : (x : A) {xs : FMSet A} → B xs → B (x ∷ xs)) where

  f : (xs : FMSet A) → B xs
  f = FMSetElim.f []* _∷*_
        (λ x y {xs} b →
          toPathP (BProp (transp (λ i → B (comm x y xs i)) i0 (x ∷* (y ∷* b))) (y ∷* (x ∷* b))))
        (λ xs → isProp→isSet BProp)

module FMSetRec {ℓ} {B : Type ℓ} (BType : isSet B)
  ([]* : B) (_∷*_ : A → B → B)
  (comm* : (x y : A) (b : B) → x ∷* (y ∷* b) ≡ y ∷* (x ∷* b)) where

  f : FMSet A → B
  f = FMSetElim.f []* (λ x b → x ∷* b) (λ x y b → comm* x y b) (λ _ → BType)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- Σ type (also used as existential) and
-- cartesian product (also used as conjunction).

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

module Tools.Product where

open import Agda.Primitive
open import Agda.Builtin.Sigma public using (Σ; _,_)
open import Agda.Builtin.Sigma using (fst; snd)

infixr 2 _×_

-- Dependent pair type (aka dependent sum, Σ type).

private
  variable
      ℓ₁ ℓ₂ ℓ₃ : Level

proj₁ : ∀ {A : Set ℓ₁} {B : A → Set ℓ₂} → Σ A B → A
proj₁ = fst

proj₂ : ∀ {A : Set ℓ₁} {B : A → Set ℓ₂} → (S : Σ A B) → B (fst S)
proj₂ = snd

-- Existential quantification.

∃ : {A : Set ℓ₁} → (A → Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
∃ = Σ _

∃₂ : {A : Set ℓ₁} {B : A → Set ℓ₂}
     (C : (x : A) → B x → Set ℓ₃) → Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)
∃₂ C = ∃ λ a → ∃ λ b → C a b

-- Cartesian product.

_×_ : (A : Set ℓ₁) (B : Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
A × B = Σ A (λ x → B)


text:
-- When defining types by recursion it is sometimes difficult to infer implicit
-- arguments. This module illustrates the problem and shows how to get around
-- it for the example of vectors of a given length.

module DataByRecursion where

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

data Nil : Set where
  nil' : Nil

data Cons (A As : Set) : Set where
  _::'_ : A -> As -> Cons A As

mutual
  Vec' : Set -> Nat -> Set
  Vec' A  zero   = Nil
  Vec' A (suc n) = Cons A (Vec A n)

  data Vec (A : Set)(n : Nat) : Set where
    vec : Vec' A n -> Vec A n

nil : {A : Set} -> Vec A zero
nil = vec nil'

_::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
x :: xs = vec (x ::' xs)

map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n
map {zero}  f (vec nil')       = nil
map {suc n} f (vec (x ::' xs)) = f x :: map f xs

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
module FSC where

-- focused sequent calculus

{-
open import Relation.Binary.PropositionalEquality
open import Data.Nat hiding (_>_)
-}

open import StdLibStuff

open import Syntax

data FSC-Ctx (n : ℕ) : Ctx n → Set where
 ε : FSC-Ctx n ε
 _∷_ : {Γ : Ctx n} → (t : Type n) → FSC-Ctx n Γ → FSC-Ctx n (t ∷ Γ)
 _∷h_ : {Γ : Ctx n} → Form Γ $o → FSC-Ctx n Γ → FSC-Ctx n Γ

data HVar {n : ℕ} : {Γ-t : Ctx n} → FSC-Ctx n Γ-t → Set where
 zero : {Γ-t : Ctx n} {h : Form Γ-t $o} {Γ : FSC-Ctx n Γ-t} → HVar (h ∷h Γ)
 succ : {Γ-t : Ctx n} {h : Form Γ-t $o} {Γ : FSC-Ctx n Γ-t} → HVar Γ → HVar (h ∷h Γ)
 skip : {Γ-t : Ctx n} {t : Type n} {Γ : FSC-Ctx n Γ-t} → HVar Γ → HVar (t ∷ Γ)

lookup-hyp : {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) → HVar Γ → Form Γ-t $o
lookup-hyp .(h ∷h Γ) (zero {._} {h} {Γ}) = h
lookup-hyp .(h ∷h Γ) (succ {._} {h} {Γ} x) = lookup-hyp Γ x
lookup-hyp .(t ∷ Γ) (skip {Γ-t} {t} {Γ} x) = weak (lookup-hyp Γ x)

mutual
 data _⊢_ {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) : Form Γ-t $o → Set where
  ||-I-l : {F G : Form Γ-t $o} →
         Γ ⊢ F →
         Γ ⊢ (F || G)
  ||-I-r : {F G : Form Γ-t $o} →
         Γ ⊢ G →
         Γ ⊢ (F || G)
  &-I : {F G : Form Γ-t $o} →
         Γ ⊢ F →   Γ ⊢ G →
         Γ ⊢ (F & G)
  ?-I : {t : Type n} {F : Form (t ∷ Γ-t) $o}
   (G : Form Γ-t t) →
   Γ ⊢ sub G F →
   Γ ⊢ (?[ t ] F)
  ?'-I : {t : Type n} {F : Form Γ-t (t > $o)}
   (G : Form Γ-t t) →
   Γ ⊢ (F · G) →
   Γ ⊢ (?'[ t ] F)
  =>-I : {F G : Form Γ-t $o} →
        (F ∷h Γ) ⊢ G →
        Γ ⊢ (F => G)
  ~-I : {F : Form Γ-t $o} →
        (F ∷h Γ) ⊢ $false →
        Γ ⊢ (~ F)
  !-I : {t : Type n} {F : Form (t ∷ Γ-t) $o} →
   (t ∷ Γ) ⊢ F →
   Γ ⊢ (![ t ] F)
  !'-I : {t : Type n} {F : Form Γ-t (t > $o)} →
   (t ∷ Γ) ⊢ (weak F · ($ this {refl})) →
   Γ ⊢ (!'[ t ] F)
  $true-I :
   Γ ⊢ $true
  ==-I : {t : Type n} {F G : Form Γ-t t} →
   Γ ⊢ t ∋ F == G →
   Γ ⊢ (F == G)  -- compute eq

  elim : {F : Form Γ-t $o} →
   (x : HVar Γ) →
   Γ , lookup-hyp Γ x ⊢ F →
   Γ ⊢ F
  ac : {t : Type n} {F : Form Γ-t $o} →
   Γ , (![ t > $o ] ((?[ t ] ($ (next this) {refl} · $ this {refl})) => ($ this {refl} · (ι t ($ (next this) {refl} · $ this {refl}))))) ⊢ F →
   Γ ⊢ F
  ac' : {t : Type n} {F : Form Γ-t $o} →
   Γ , (![ t > $o ] ((?'[ t ] ($ this {refl})) => ($ this {refl} · (ι' t ($ this {refl}))))) ⊢ F →
   Γ ⊢ F

  raa : {F : Form Γ-t $o} →
   Γ ⊢ (~ (~ F)) →
   Γ ⊢ F

  reduce : {t u : Type n} {F : Form Γ-t u → Form Γ-t $o} {G : Form (t ∷ Γ-t) u} {H : Form Γ-t t} →
   Γ ⊢ (F (sub H G)) →
   Γ ⊢ (F ((^[ t ] G) · H))

 data _,_⊢_ {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) : Form Γ-t $o → Form Γ-t $o → Set where
  use : {F G : Form Γ-t $o} →
   Γ ⊢ $o ∋ G ↔ F →
   Γ , F ⊢ G
  $false-E : {H : Form Γ-t $o} →
   Γ , $false ⊢ H
  ~-E : {F H : Form Γ-t $o} →
   Γ ⊢ F →
   Γ , ~ F ⊢ H
  ||-E : {F G H : Form Γ-t $o} →
   Γ ⊢ (F => H) →
   Γ ⊢ (G => H) →
   Γ , F || G ⊢ H

  &-E-l : {F G H : Form Γ-t $o} →
   Γ , F ⊢ H →
   Γ , F & G ⊢ H
  &-E-r : {F G H : Form Γ-t $o} →
   Γ , G ⊢ H →
   Γ , F & G ⊢ H
  ?-E : {t : Type n} {F : Form (t ∷ Γ-t) $o} {H : Form Γ-t $o} →
   Γ , sub (ι t F) F ⊢ H →
   Γ , ?[ t ] F ⊢ H
  ?'-E : {t : Type n} {F : Form Γ-t (t > $o)} {H : Form Γ-t $o} →
   Γ , (F · ι' t F) ⊢ H →
   Γ , ?'[ t ] F ⊢ H
  =>-E : {F G H : Form Γ-t $o} →
   Γ ⊢ F →
   Γ , G ⊢ H →
   Γ , F => G ⊢ H
  !-E : {t : Type n} {F : Form (t ∷ Γ-t) $o} {H : Form Γ-t $o}
   (G : Form Γ-t t) →
   Γ , sub G F ⊢ H →
   Γ , ![ t ] F ⊢ H
  !'-E : {t : Type n} {F : Form Γ-t (t > $o)} {H : Form Γ-t $o}
   (G : Form Γ-t t) →
   Γ , (F · G) ⊢ H →
   Γ , !'[ t ] F ⊢ H
  r-bool-ext : {F G H : Form Γ-t $o} →
   Γ , ((F => G) & (G => F)) ⊢ H →
   Γ , F == G ⊢ H  -- compute eq
  r-fun-ext : {t u : Type n} {F G : Form Γ-t (t > u)} {H : Form Γ-t $o}
   (I : Form Γ-t t) →
   Γ , (F · I) == (G · I) ⊢ H →
   Γ , F == G ⊢ H  -- compute eq

  reduce : {t u : Type n} {F : Form Γ-t u → Form Γ-t $o} {G : Form (t ∷ Γ-t) u} {H : Form Γ-t t} {I : Form Γ-t $o} →
   Γ , (F (sub H G)) ⊢ I →
   Γ , (F ((^[ t ] G) · H)) ⊢ I

 data _⊢_∋_==_ {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) : (t : Type n) (F G : Form Γ-t t) → Set where
  simp : {t : Type n} {F G : Form Γ-t t} →
   Γ ⊢ t ∋ F ↔ G →
   Γ ⊢ t ∋ F == G
  step : {t : Type n} {F G : Form Γ-t t} (F' G' : Form Γ-t t) →
   (x : HVar Γ) →
   Γ , lookup-hyp Γ x ⊢ F' == G' →
   Γ ⊢ t ∋ F ↔ F' →
   Γ ⊢ t ∋ G' == G →
   Γ ⊢ t ∋ F == G
  bool-ext :  {F G : Form Γ-t $o} →
   Γ ⊢ ((F => G) & (G => F)) →
   Γ ⊢ $o ∋ F == G
  fun-ext : {t u : Type n} {F G : Form Γ-t (t > u)} →
   (t ∷ Γ) ⊢ u ∋ ((weak F) · $ this {refl}) == ((weak G) · $ this {refl}) →
   Γ ⊢ (t > u) ∋ F == G

 data _⊢_∋_↔_ {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) : (t : Type n) → Form Γ-t t → Form Γ-t t → Set where
  head-var : (t : Type n) (x : Var Γ-t) (p : lookup-Var Γ-t x ≡ t) →
   Γ ⊢ t ∋ $ x {p} ↔ $ x {p}
  head-const : (t : Type n) (c : Form Γ-t t) →
   Γ ⊢ t ∋ c ↔ c
  head-app : (t₁ t₂ : Type n) (F₁ F₂ : Form Γ-t (t₁ > t₂)) (G₁ G₂ : Form Γ-t t₁) →
   Γ ⊢ (t₁ > t₂) ∋ F₁ == F₂ → Γ ⊢ t₁ ∋ G₁ == G₂ →
   Γ ⊢ t₂ ∋ (F₁ · G₁) ↔ (F₂ · G₂)
  head-lam : (t₁ t₂ : Type n) (F₁ F₂ : Form (t₁ ∷ Γ-t) t₂) →
   (t₁ ∷ Γ) ⊢ t₂ ∋ F₁ == F₂ →
   Γ ⊢ (t₁ > t₂) ∋ (lam t₁ F₁) ↔ (lam t₁ F₂)
  head-lam-eta-left : (t₁ t₂ : Type n) (F₁ : Form Γ-t (t₁ > t₂)) (F₂ : Form (t₁ ∷ Γ-t) t₂) →
   (t₁ ∷ Γ) ⊢ t₂ ∋ (weak F₁ · $ this {refl}) == F₂ →
   Γ ⊢ (t₁ > t₂) ∋ F₁ ↔ lam t₁ F₂
  head-lam-eta-right : (t₁ t₂ : Type n) (F₁ : Form Γ-t (t₁ > t₂)) (F₂ : Form (t₁ ∷ Γ-t) t₂) →
   (t₁ ∷ Γ) ⊢ t₂ ∋ F₂ == (weak F₁ · $ this {refl}) →
   Γ ⊢ (t₁ > t₂) ∋ lam t₁ F₂ ↔ F₁

  reduce-l : {t u v : Type n} {F₁ : Form Γ-t v → Form Γ-t t} {G : Form (u ∷ Γ-t) v} {H : Form Γ-t u} {F₂ : Form Γ-t t} →
   Γ ⊢ t ∋ (F₁ (sub H G)) ↔ F₂ →
   Γ ⊢ t ∋ (F₁ ((^[ u ] G) · H)) ↔ F₂
  reduce-r : {t u v : Type n} {F₂ : Form Γ-t v → Form Γ-t t} {G : Form (u ∷ Γ-t) v} {H : Form Γ-t u} {F₁ : Form Γ-t t} →
   Γ ⊢ t ∋ F₁ ↔ (F₂ (sub H G)) →
   Γ ⊢ t ∋ F₁ ↔ (F₂ ((^[ u ] G) · H))

 data _,_⊢_==_ {n : ℕ} {Γ-t : Ctx n} {t : Type n} (Γ : FSC-Ctx n Γ-t) : Form Γ-t $o → Form Γ-t t → Form Γ-t t → Set where
  use : {F G : Form Γ-t t} →
   Γ , F == G ⊢ F == G
  use' : {F G : Form Γ-t t} {H : Form Γ-t $o} →
   headNorm 2 (F == G) ≡ headNorm 2 H →
   Γ , H ⊢ F == G
  use-sym : {F G : Form Γ-t t} →
   Γ , F == G ⊢ G == F  -- compute eq

  &-E-l : {F G : Form Γ-t $o} {H₁ H₂ : Form Γ-t t} →
   Γ , F ⊢ H₁ == H₂ →
   Γ , F & G ⊢ H₁ == H₂
  &-E-r : {F G : Form Γ-t $o} {H₁ H₂ : Form Γ-t t} →
   Γ , G ⊢ H₁ == H₂ →
   Γ , F & G ⊢ H₁ == H₂
  ?-E : {u : Type n} {F : Form (u ∷ Γ-t) $o} {H₁ H₂ : Form Γ-t t} →
   Γ , sub (ι u F) F ⊢ H₁ == H₂ →
   Γ , ?[ u ] F ⊢ H₁ == H₂
  ?'-E : {u : Type n} {F : Form Γ-t (u > $o)} {H₁ H₂ : Form Γ-t t} →
   Γ , (F · ι' u F) ⊢ H₁ == H₂ →
   Γ , ?'[ u ] F ⊢ H₁ == H₂
  =>-E : {F G : Form Γ-t $o} {H₁ H₂ : Form Γ-t t} →
   Γ ⊢ F →
   Γ , G ⊢ H₁ == H₂ →
   Γ , F => G ⊢ H₁ == H₂
  !-E : {u : Type n} {F : Form (u ∷ Γ-t) $o} {H₁ H₂ : Form Γ-t t}
   (G : Form Γ-t u) →
   Γ , sub G F ⊢ H₁ == H₂ →
   Γ , ![ u ] F ⊢ H₁ == H₂
  !'-E : {u : Type n} {F : Form Γ-t (u > $o)} {H₁ H₂ : Form Γ-t t}
   (G : Form Γ-t u) →
   Γ , (F · G) ⊢ H₁ == H₂ →
   Γ , !'[ u ] F ⊢ H₁ == H₂
  r-bool-ext : {F G : Form Γ-t $o} {H I : Form Γ-t t} →
   Γ , ((F => G) & (G => F)) ⊢ H == I →
   Γ , F == G ⊢ H == I  -- compute eq
  r-fun-ext : {u v : Type n} {F G : Form Γ-t (u > v)} {H I : Form Γ-t t}
   (J : Form Γ-t u) →
   Γ , (F · J) == (G · J) ⊢ H == I →
   Γ , F == G ⊢ H == I  -- compute eq

  reduce : {u v : Type n} {F : Form Γ-t v → Form Γ-t $o} {G : Form (u ∷ Γ-t) v} {H : Form Γ-t u} {I₁ I₂ : Form Γ-t t} →
   Γ , (F (sub H G)) ⊢ I₁ == I₂ →
   Γ , (F ((^[ u ] G) · H)) ⊢ I₁ == I₂

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
-- Andreas, 2016-09-20, issue #2197 reported by m0davis

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.pos:20 -v tc.meta.eta:20 #-}

record R : Set where
  inductive

  field
    foo : R

  bar : R
  bar = {!!}

-- This used to loop due to infinite eta-expansion.
-- Should check now.


text:
module Common.Issue481ParametrizedModule (A : Set1) where

id : A → A
id x = x

postulate
  Bla : Set


text: test = forall _⦇_ → Set