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

module Definition.Typed.Consequences.RelevanceUnicity where

open import Definition.Untyped hiding (U≢ℕ; U≢Π; U≢ne; ℕ≢Π; ℕ≢ne; Π≢ne; U≢Empty; ℕ≢Empty; Empty≢Π; Empty≢ne)
open import Definition.Untyped.Properties using (subst-Univ-either)
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Typed.Consequences.Equality
import Definition.Typed.Consequences.Inequality as Ineq
open import Definition.Typed.Consequences.Inversion
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.PiNorm
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
open import Tools.Empty
open import Tools.Sum using (_⊎_; inj₁; inj₂)
import Tools.PropositionalEquality as PE

ℕ-relevant-term : ∀ {Γ A r} → Γ ⊢ ℕ ∷ A ^ r → Whnf A → A PE.≡ Univ ! ⁰
ℕ-relevant-term [ℕ] whnfA = let [[N]] , e = inversion-ℕ [ℕ]
                             in U≡A-whnf (sym (PE.subst (λ r → _ ⊢ _ ≡ _ ^ r) e [[N]])) whnfA

ℕ-relevant : ∀ {Γ r} → Γ ⊢ ℕ ^ r → r PE.≡ [ ! , ι ⁰ ]
ℕ-relevant (univ [ℕ]) = let er , el = Univ-PE-injectivity (ℕ-relevant-term [ℕ] Uₙ)
                         in PE.cong₂ (λ x y → [ x , ι y ]) er el

Empty-irrelevant-term : ∀ {Γ A lEmpty r} → Γ ⊢ Empty lEmpty ∷ A ^ r → Whnf A → A PE.≡ SProp lEmpty
Empty-irrelevant-term [Empty] whnfA = let [[Empty]] , e = inversion-Empty [Empty]
                                      in U≡A-whnf (sym (PE.subst (λ r → _ ⊢ _ ≡ _ ^ r) e [[Empty]])) whnfA

Empty-irrelevant : ∀ {Γ lEmpty r} → Γ ⊢ Empty lEmpty ^ r → r PE.≡ [ % , ι lEmpty ]
Empty-irrelevant (univ [Empty]) = let er , el = Univ-PE-injectivity (Empty-irrelevant-term [Empty] Uₙ)
                                  in PE.cong₂ (λ x y → [ x , ι y ]) er el

Univ-relevant-term : ∀ {Γ A rU lU r} → Γ ⊢ Univ rU lU ∷ A ^ r → Whnf A → A PE.≡ U ¹ × lU PE.≡ ⁰
Univ-relevant-term [U] whnfA = U≡A-whnf (sym (proj₁ (inversion-U [U]))) whnfA , proj₂ (proj₂ (inversion-U [U]))

Univ-relevant : ∀ {Γ rU lU r} → Γ ⊢ Univ rU lU ^ r → r PE.≡ [ ! , next lU ]
Univ-relevant (Uⱼ _) = PE.refl
Univ-relevant (univ [U]) = let er , el = Univ-PE-injectivity (proj₁ (Univ-relevant-term [U] Uₙ))
                           in PE.cong₂ (λ x y → [ x , y ]) er
                                       (PE.trans (PE.cong ι el) (PE.cong next (PE.sym  (proj₂ (Univ-relevant-term [U] Uₙ)))))
mutual
  Univ-uniq′ : ∀ {Γ A T₁ T₂ r₁ r₂ l₁ l₁' l₂ l₂'} → Γ ⊢ T₁ ≡ Univ r₁ l₁ ^ [ ! , l₁' ] → Γ ⊢ T₂ ≡ Univ r₂ l₂ ^ [ ! , l₂' ]
    → next l₁ PE.≡ l₁' → next l₂ PE.≡ l₂'
    → ΠNorm A
    → Γ ⊢ A ∷ T₁ ^ [ ! , l₁' ] → Γ ⊢ A ∷ T₂ ^ [ ! , l₂' ] → r₁ PE.≡ r₂ × l₁' PE.≡ l₂'
  Univ-uniq′ e₁ e₂ el₁ el₂ w (univ 0<1 x₁) (univ 0<1 x₃) =
    let er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.refl
  Univ-uniq′ e₁ e₂ el₁ PE.refl w (ℕⱼ x) y =
    let e₁′ , el₁′  = Uinjectivity e₁
        e₂′ , el₂′ = Uinjectivity (trans (sym e₂) (proj₁ (inversion-ℕ y)) )
    in PE.sym (PE.trans e₂′ e₁′) , PE.cong next (PE.sym el₂′)
  Univ-uniq′ e₁ e₂ el₁ el₂ w (Emptyⱼ x) y =
    let e₁′ , el₁′  = Uinjectivity e₁
        e₂′ , el₂′ = Uinjectivity (trans (sym e₂) (proj₁ (inversion-Empty y)) )
    in PE.sym (PE.trans e₂′ e₁′) , PE.trans (PE.cong next (PE.sym el₂′)) el₂
  Univ-uniq′ e₁ e₂ el₁ el₂ w (Πⱼ a ▹ b ▹ x ▹ x₁) (Πⱼ a' ▹ b' ▹ y ▹ y₁) =
    let er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
        res = Univ-uniq′ (refl (Ugenⱼ (wfTerm x₁))) (refl (Ugenⱼ (wfTerm x₁)))
                                                    PE.refl PE.refl (ΠNorm-Π w) x₁ y₁
    in PE.trans (PE.sym er₁) (PE.trans (proj₁ res) er₂) , PE.refl
  Univ-uniq′ e₁ e₂ el₁ el₂ (∃ₙ w) (∃ⱼ x ▹ x₁) (∃ⱼ y ▹ y₁) =
    let er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
        _ , el = Univ-uniq w x y
    in  PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ w (var _ x) (var _ y) =
    let T≡T , e = varTypeEq′ x y
        _ , el = typelevel-injectivity e
        ⊢T≡T = PE.subst (λ T → _ ⊢ _ ≡ T ^ _) T≡T (refl (proj₁ (syntacticEq e₁)))
    in proj₁ (Uinjectivity (trans (trans (sym e₁) ⊢T≡T) (PE.subst (λ lx → _ ⊢ _ ≡ _ ^ [ _ , lx ]) (PE.sym el) e₂))) , el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne ()) (lamⱼ x x₁ x₂ X) y
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (∘ₙ n)) (_∘ⱼ_ {G = G} x x₁) (_∘ⱼ_ {G = G₁} y y₁) =
    let F≡F , rF≡rF , lF≡lF , lG≡lG , G≡G = injectivity (proj₂ (neTypeEq n x y))
        r≡r , _ = Uinjectivity (trans (sym e₁) (trans (substitutionEq G≡G (substRefl (singleSubst x₁)) (wfEq F≡F))
                                               (PE.subst (λ lx → _ ⊢ _ ≡ _ ^ [ _ , ι lx ]) (PE.sym lG≡lG) e₂)))
    in r≡r , PE.cong ι lG≡lG
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne ()) (zeroⱼ x) y
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne ()) (sucⱼ X) y
  Univ-uniq′ e₁ e₂ el₁ el₂ w (natrecⱼ x x₁ x₂ x₃) (natrecⱼ x₄ y y₁ y₂) = proj₁ (Uinjectivity (trans (sym e₁) e₂)) , PE.refl
  Univ-uniq′ e₁ e₂ el₁ el₂ w (Emptyrecⱼ x x₁) (Emptyrecⱼ y y₁) = proj₁ (Uinjectivity (trans (sym e₁) e₂)) , PE.refl
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (Idₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq (ne x) X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (Idℕₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq ℕₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (Idℕ0ₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq ℕₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (IdℕSₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq ℕₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (IdUₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq Uₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (IdUℕₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq Uₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ (ne (IdUΠₙ x)) (Idⱼ X X₁ X₂) (Idⱼ {l = ll} Y Y₁ Y₂) =
    let _ , el = Univ-uniq Uₙ X Y
        er₁ , _ = Uinjectivity e₁
        er₂ , _ = Uinjectivity e₂
    in PE.trans (PE.sym er₁) er₂ , PE.cong next el
  Univ-uniq′ e₁ e₂ el₁ el₂ w (castⱼ X X₁ X₂ X₃) (castⱼ y y₁ y₂ y₃) = proj₁ (Uinjectivity (trans (sym e₁) e₂)) , PE.refl
  Univ-uniq′ e₁ e₂ el₁ el₂ w (conv x x₁) y = Univ-uniq′ (trans x₁ e₁) e₂ el₁ el₂ w x y
  Univ-uniq′ e₁ e₂ el₁ el₂ w x (conv y y₁) = Univ-uniq′ e₁ (trans y₁ e₂) el₁ el₂ w x y

  Univ-uniq : ∀ {Γ A r₁ r₂ l₁ l₂} → ΠNorm A
    → Γ ⊢ A ∷ Univ r₁ l₁ ^ [ ! , next l₁ ] → Γ ⊢ A ∷ Univ r₂ l₂ ^ [ ! , next l₂ ] → r₁ PE.≡ r₂ × l₁ PE.≡ l₂
  Univ-uniq n ⊢A₁ ⊢A₂ =
    let ⊢Γ = wfTerm ⊢A₁
        er , el =  Univ-uniq′ (refl (Ugenⱼ ⊢Γ)) (refl (Ugenⱼ ⊢Γ)) PE.refl PE.refl n ⊢A₁ ⊢A₂
    in er , next-inj el

relevance-unicity′ : ∀ {Γ A r₁ r₂ l₁ l₂} → ΠNorm A → Γ ⊢ A ^ [ r₁ , l₁ ] → Γ ⊢ A ^ [ r₂ , l₂ ] → r₁ PE.≡ r₂ × l₁ PE.≡ l₂
relevance-unicity′ n (Uⱼ x) (Uⱼ x₁) = PE.refl , PE.refl
relevance-unicity′ n (Uⱼ x) (univ x₁) = let _ , _ , ¹≡⁰ = inversion-U x₁ in ⊥-elim (⁰≢¹ (PE.sym  ¹≡⁰))
relevance-unicity′ n (univ x) (Uⱼ x₁) = let _ , _ , ¹≡⁰ = inversion-U x in ⊥-elim (⁰≢¹ (PE.sym  ¹≡⁰))
relevance-unicity′ n (univ x) (univ x₁) = let er , el = Univ-uniq n x x₁ in er , PE.cong ι el

relevance-unicity : ∀ {Γ A r₁ r₂ l₁ l₂} → Γ ⊢ A ^ [ r₁ , l₁ ] → Γ ⊢ A ^ [ r₂ , l₂ ] → r₁ PE.≡ r₂ × l₁ PE.≡ l₂
relevance-unicity ⊢A₁ ⊢A₂ with doΠNorm ⊢A₁
... | _ with doΠNorm ⊢A₂
relevance-unicity ⊢A₁ ⊢A₂ | B , nB , ⊢B , rB | C , nC , ⊢C , rC =
  let e = detΠNorm* nB nC rB rC
  in relevance-unicity′ nC (PE.subst _ e ⊢B) ⊢C

-- inequalities at any relevance
U≢ℕ : ∀ {r r′ l l′ Γ} → Γ ⊢ Univ r l ≡ ℕ ^ [ r′ , l′ ] → ⊥
U≢ℕ U≡ℕ = Ineq.U≢ℕ! (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ])
                              (proj₁ (relevance-unicity (proj₂ (syntacticEq U≡ℕ))
                                                 (univ (ℕⱼ (wfEq U≡ℕ)))))
                              U≡ℕ)

U≢Π : ∀ {rU lU  F rF G lF lG lΠ r Γ} → Γ ⊢ Univ rU lU ≡ Π F ^ rF ° lF ▹ G ° lG ° lΠ  ^ [ r , ι lΠ ] → ⊥
U≢Π U≡Π =
  let r≡! , _ = relevance-unicity (proj₁ (syntacticEq U≡Π)) (Ugenⱼ (wfEq U≡Π))
  in Ineq.U≢Π! (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡! U≡Π)

U≢ne : ∀ {rU lU r l K Γ} → Neutral K → Γ ⊢ Univ rU lU ≡ K ^ [ r , ι l ] → ⊥
U≢ne neK U≡K =
  let r≡! , _ = relevance-unicity (proj₁ (syntacticEq U≡K)) (Ugenⱼ (wfEq U≡K))
  in Ineq.U≢ne! neK (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡! U≡K)

ℕ≢Π : ∀ {F rF G lF lG r Γ} → Γ ⊢ ℕ ≡ Π F ^ rF ° lF ▹ G ° lG ° ⁰ ^ [ r , ι ⁰ ] → ⊥
ℕ≢Π ℕ≡Π =
  let r≡! , _ = relevance-unicity (proj₁ (syntacticEq ℕ≡Π)) (univ (ℕⱼ (wfEq ℕ≡Π)))
  in Ineq.ℕ≢Π! (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡! ℕ≡Π)

Empty≢Π : ∀ {F rF G lF lG lΠ r Γ} → Γ ⊢ Empty lΠ ≡ Π F ^ rF ° lF ▹ G ° lG ° lΠ  ^ [ r , ι lΠ ] → ⊥
Empty≢Π Empty≡Π =
  let r≡% , _ = relevance-unicity (proj₁ (syntacticEq Empty≡Π)) (univ (Emptyⱼ (wfEq Empty≡Π)))
  in Ineq.Empty≢Π% (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡% Empty≡Π)

ℕ≢ne : ∀ {K r Γ} → Neutral K → Γ ⊢ ℕ ≡ K ^ [ r , ι ⁰ ] → ⊥
ℕ≢ne neK ℕ≡K =
  let r≡! , _ = relevance-unicity (proj₁ (syntacticEq ℕ≡K)) (univ (ℕⱼ (wfEq ℕ≡K)))
  in Ineq.ℕ≢ne! neK (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡! ℕ≡K)

Empty≢ne : ∀ {K r l Γ} → Neutral K → Γ ⊢ Empty l ≡ K ^ [ r , ι l ] → ⊥
Empty≢ne neK Empty≡K =
  let r≡% , _ = relevance-unicity (proj₁ (syntacticEq Empty≡K)) (univ (Emptyⱼ (wfEq Empty≡K)))
  in Ineq.Empty≢ne% neK (PE.subst (λ rx → _ ⊢ _ ≡ _ ^ [ rx , _ ]) r≡% Empty≡K)

-- U != Empty is given easily by relevances
U≢Empty : ∀ {Γ rU lU lEmpty r′} → Γ ⊢ Univ rU lU ≡ Empty lEmpty ^ r′ → ⊥
U≢Empty U≡Empty =
  let ⊢U , ⊢Empty = syntacticEq U≡Empty
      e₁ , _ = relevance-unicity ⊢U (Ugenⱼ (wfEq U≡Empty))
      e₂ , _ = relevance-unicity ⊢Empty (univ (Emptyⱼ (wfEq U≡Empty)))
  in !≢% (PE.trans (PE.sym e₁) e₂)

-- ℕ and Empty also by relevance
ℕ≢Empty : ∀ {Γ r l} → Γ ⊢ ℕ ≡ Empty l ^ r → ⊥
ℕ≢Empty ℕ≡Empty =
  let ⊢ℕ , ⊢Empty = syntacticEq ℕ≡Empty
      e₁ , _ = relevance-unicity ⊢ℕ (univ (ℕⱼ (wfEq ℕ≡Empty)))
      e₂ , _ = relevance-unicity ⊢Empty (univ (Emptyⱼ (wfEq ℕ≡Empty)))
  in !≢% (PE.trans (PE.sym e₁) e₂)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
------------------------------------------------------------------------
-- Breadth-first labelling of trees
------------------------------------------------------------------------

-- This module just defines breadth-first labelling. For a full
-- development including a specification and proof, see BreadthFirst.

module BreadthFirstWithoutProof where

open import Codata.Musical.Notation
open import Codata.Musical.Stream
open import Data.Product

open import Tree using (Tree; leaf; node)

------------------------------------------------------------------------
-- Universe

data U : Set₁ where
  tree   : (a : U) → U
  stream : (a : U) → U
  _⊗_    : (a b : U) → U
  ⌈_⌉    : (A : Set) → U

El : U → Set
El (tree a)   = Tree (El a)
El (stream a) = Stream (El a)
El (a ⊗ b)    = El a × El b
El ⌈ A ⌉      = A

------------------------------------------------------------------------
-- Programs

infixr 5 _∷_
infixr 4 _,_

mutual

  data ElP : U → Set₁ where
    ↓   : ∀ {a} (w : ElW a) → ElP a
    fst : ∀ {a b} (p : ElP (a ⊗ b)) → ElP a
    snd : ∀ {a b} (p : ElP (a ⊗ b)) → ElP b
    lab : ∀ {A B} (t : Tree A) (bss : ElP (stream ⌈ Stream B ⌉)) →
          ElP (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)

  -- The term WHNF is a bit of a misnomer here; only recursive
  -- /coinductive/ arguments are suspended (in the form of programs).

  data ElW : U → Set₁ where
    leaf : ∀ {a} → ElW (tree a)
    node : ∀ {a}
           (l : ∞ (ElP (tree a))) (x : ElW a) (r : ∞ (ElP (tree a))) →
           ElW (tree a)
    _∷_  : ∀ {a} (x : ElW a) (xs : ∞ (ElP (stream a))) → ElW (stream a)
    _,_  : ∀ {a b} (x : ElW a) (y : ElW b) → ElW (a ⊗ b)
    ⌈_⌉  : ∀ {A} (x : A) → ElW ⌈ A ⌉

fstW : ∀ {a b} → ElW (a ⊗ b) → ElW a
fstW (x , y) = x

sndW : ∀ {a b} → ElW (a ⊗ b) → ElW b
sndW (x , y) = y

-- Uses the n-th stream to label the n-th level in the tree. Returns
-- the remaining stream elements (for every level).

labW : ∀ {A B} → Tree A → ElW (stream ⌈ Stream B ⌉) →
       ElW (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)
labW leaf         bss                = (leaf , bss)
labW (node l _ r) (⌈ b ∷ bs ⌉ ∷ bss) =
  (node (♯ fst x) ⌈ b ⌉ (♯ fst y) , ⌈ ♭ bs ⌉ ∷ ♯ snd y)
  where
  x = lab (♭ l) (♭ bss)
  y = lab (♭ r) (snd x)

whnf : ∀ {a} → ElP a → ElW a
whnf (↓ w)       = w
whnf (fst p)     = fstW (whnf p)
whnf (snd p)     = sndW (whnf p)
whnf (lab t bss) = labW t (whnf bss)

mutual

  ⟦_⟧W : ∀ {a} → ElW a → El a
  ⟦ leaf       ⟧W = leaf
  ⟦ node l x r ⟧W = node (♯ ⟦ ♭ l ⟧P) ⟦ x ⟧W (♯ ⟦ ♭ r ⟧P)
  ⟦ x ∷ xs     ⟧W = ⟦ x ⟧W ∷ ♯ ⟦ ♭ xs ⟧P
  ⟦ (x , y)    ⟧W = (⟦ x ⟧W , ⟦ y ⟧W)
  ⟦ ⌈ x ⌉      ⟧W = x

  ⟦_⟧P : ∀ {a} → ElP a → El a
  ⟦ p ⟧P = ⟦ whnf p ⟧W

------------------------------------------------------------------------
-- Breadth-first labelling

label′ : ∀ {A B} → Tree A → Stream B →
         ElP (tree ⌈ B ⌉ ⊗ stream ⌈ Stream B ⌉)
label′ t bs = lab t (↓ (⌈ bs ⌉ ∷ ♯ snd (label′ t bs)))

label : ∀ {A B} → Tree A → Stream B → Tree B
label t bs = ⟦ fst (label′ t bs) ⟧P

ext: agda

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module System.IO.Transducers.Properties where

open import System.IO.Transducers.Properties.Category public
open import System.IO.Transducers.Properties.Monoidal public
open import System.IO.Transducers.Properties.LaxBraided public
open import System.IO.Transducers.Properties.Equivalences public

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


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

module lib.types.EilenbergMacLane1 where

open import lib.types.EilenbergMacLane1.Core public
open import lib.types.EilenbergMacLane1.Recursion public
open import lib.types.EilenbergMacLane1.DoubleElim public
open import lib.types.EilenbergMacLane1.DoublePathElim public
open import lib.types.EilenbergMacLane1.FunElim public
open import lib.types.EilenbergMacLane1.PathElim public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --without-K #-}
module sets.list.core where

open import sum
import sets.vec.core as V
open import sets.nat.core

List : ∀ {i} → Set i → Set i
List A = Σ ℕ (V.Vec A)

module _ {i}{A : Set i} where
  vec-to-list : ∀ {n} → V.Vec A n → List A
  vec-to-list {n} xs = n , xs

  [] : List A
  [] = 0 , V.[]

  infixr 4 _∷_
  _∷_ : A → List A → List A
  x ∷ (n , xs) = suc n , x V.∷ xs

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2013-04-06
-- Interaction point buried in postponed type checking problem

module Issue1083 where

data Bool : Set where true false : Bool

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

postulate
  f : {x : Bool} → T x

test : (x : Bool) → T x
test true = f {!!}
test false = {!!}

-- Constraints show: _10 := (_ : T _x_9) ? : Bool
-- So there is a question mark which has never been seen by the type checker.
-- It is buried in a postponed type-checking problem.

-- Interaction points should probably be created by the scope checker,
-- and then hooked up to meta variables by the type checker.

-- This is how it works now.

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2020-05-16, issue #4649
-- Allow --safe flag in -I mode

{-# OPTIONS --safe #-}

data Unit : Set where
  unit : Unit

test : Unit
test = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
data N : Set = zero | suc (n:N)
data B : Set = true | false

data False : Set =
data True  : Set = tt

F : B -> Set
F true  = N
F false = B

G : (x:B) -> F x -> Set
G false _      = N
G true zero    = B
G true (suc n) = N

(==) : B -> B -> Set
true == true = True
false == false = True
_ == _ = False

data Equal (x,y:B) : Set where
  equal : x == y -> Equal x y

refl : (x:B) -> Equal x x
refl true = equal tt
refl false = equal tt

postulate
  f : (x:B) -> (y : F x) -> G x y -> N -- Equal x true -> N

h : N
h = f _ false zero --(refl true)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Oscar.Prelude

module Oscar.Data.Constraint where

data Constraint {𝔞} {𝔄 : Ø 𝔞} (𝒶 : 𝔄) : Ø₀ where
  instance ∅ : Constraint 𝒶


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reverse view
------------------------------------------------------------------------

module Data.List.Reverse where

open import Data.List
open import Data.Nat
import Data.Nat.Properties as Nat
open import Induction.Nat
open import Relation.Binary.PropositionalEquality

-- If you want to traverse a list from the end, then you can use the
-- reverse view of it.

infixl 5 _∶_∶ʳ_

data Reverse {A : Set} : List A → Set where
  []     : Reverse []
  _∶_∶ʳ_ : ∀ xs (rs : Reverse xs) (x : A) → Reverse (xs ∷ʳ x)

reverseView : ∀ {A} (xs : List A) → Reverse xs
reverseView {A} xs = <-rec Pred rev (length xs) xs refl
  where
  Pred : ℕ → Set
  Pred n = (xs : List A) → length xs ≡ n → Reverse xs

  lem : ∀ xs {x : A} → length xs <′ length (xs ∷ʳ x)
  lem []       = ≤′-refl
  lem (x ∷ xs) = Nat.s≤′s (lem xs)

  rev : (n : ℕ) → <-Rec Pred n → Pred n
  rev n                   rec xs         eq   with initLast xs
  rev n                   rec .[]        eq   | []       = []
  rev .(length (xs ∷ʳ x)) rec .(xs ∷ʳ x) refl | xs ∷ʳ' x
    with rec (length xs) (lem xs) xs refl
  rev ._ rec .([]      ∷ʳ x) refl | ._ ∷ʳ' x | [] = _ ∶ [] ∶ʳ x
  rev ._ rec .(ys ∷ʳ y ∷ʳ x) refl | ._ ∷ʳ' x | ys ∶ rs ∶ʳ y =
    _ ∶ (_ ∶ rs ∶ʳ y) ∶ʳ x


text:
-- Andreas, 2013-02-21 issue seems to have been fixed along with issue 796
-- {-# OPTIONS -v tc.decl:10 #-}
module Issue4 where

open import Common.Equality

abstract

  abstract -- a second abstract seems to have no effect

    T : Set -> Set
    T A = A

  see-through : ∀ {A} → T A ≡ A
  see-through = refl

  data Ok (A : Set) : Set where
    ok : T (Ok A) → Ok A

opaque : ∀ {A} → T A ≡ A
opaque = see-through

data Bad (A : Set) : Set where
  bad : T (Bad A) -> Bad A

max_stars_repo_name: larrytheliquid/agda


text:
-- It is recommended to use Cubical.Algebra.CommRing.Instances.Int
-- instead of this file.

{-# OPTIONS --safe #-}
module Cubical.Algebra.AbGroup.Instances.DiffInt where

open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetQuotients

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Data.Int.MoreInts.DiffInt
  renaming (
    _+_ to _+ℤ_
  )

DiffℤasAbGroup : AbGroup ℓ-zero
DiffℤasAbGroup = makeAbGroup {G = ℤ}
                             [ (0 , 0) ]
                             _+ℤ_
                             -ℤ_
                             ℤ-isSet
                             +ℤ-assoc
                             (λ x → zero-identityʳ 0 x)
                             (λ x → -ℤ-invʳ x)
                             +ℤ-comm

max_stars_repo_name: FernandoLarrain/cubical


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Lambda {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Introductions.Pi

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Valid lambda term construction.
lamᵛ : ∀ {F G t Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
       ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
       ([t] : Γ ∙ F ⊩ᵛ⟨ l ⟩ t ∷ G / [Γ] ∙″ [F] / [G])
     → Γ ⊩ᵛ⟨ l ⟩ lam t ∷ Π F ▹ G / [Γ] / Πᵛ {F} {G} [Γ] [F] [G]
lamᵛ {F} {G} {t} {Γ} {l} [Γ] [F] [G] [t] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let ⊢F = escape (proj₁ ([F] ⊢Δ [σ]))
      [liftσ] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
      [ΠFG] = Πᵛ {F} {G} [Γ] [F] [G]
      Πᵣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext =
        extractMaybeEmbΠ (Π-elim (proj₁ ([ΠFG] ⊢Δ [σ])))
      lamt : ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           → Δ ⊩⟨ l ⟩ subst σ (lam t) ∷ subst σ (Π F ▹ G) / proj₁ ([ΠFG] ⊢Δ [σ])
      lamt {Δ} {σ} ⊢Δ [σ] =
        let [liftσ] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]
            [σF] = proj₁ ([F] ⊢Δ [σ])
            ⊢F = escape [σF]
            ⊢wk1F = T.wk (step id) (⊢Δ ∙ ⊢F) ⊢F
            [σG] = proj₁ ([G] (⊢Δ ∙ ⊢F) [liftσ])
            ⊢G = escape [σG]
            [σt] = proj₁ ([t] (⊢Δ ∙ ⊢F) [liftσ])
            ⊢t = escapeTerm [σG] [σt]
            wk1t[0] = irrelevanceTerm″
                        PE.refl
                        (PE.sym (wkSingleSubstId (subst (liftSubst σ) t)))
                        [σG] [σG] [σt]
            β-red′ = PE.subst (λ x → _ ⊢ _ ⇒ _ ∷ x)
                              (wkSingleSubstId (subst (liftSubst σ) G))
                              (β-red ⊢wk1F (T.wkTerm (lift (step id))
                                                     (⊢Δ ∙ ⊢F ∙ ⊢wk1F) ⊢t)
                                                     (var (⊢Δ ∙ ⊢F) here))
            Πᵣ F′ G′ D′ ⊢F′ ⊢G′ A≡A′ [F]′ [G]′ G-ext =
              extractMaybeEmbΠ (Π-elim (proj₁ ([ΠFG] ⊢Δ [σ])))
        in  Πₜ (lam (subst (liftSubst σ) t)) (idRedTerm:*: (lamⱼ ⊢F ⊢t)) lamₙ
               (≅-η-eq ⊢F (lamⱼ ⊢F ⊢t) (lamⱼ ⊢F ⊢t) lamₙ lamₙ
                       (escapeTermEq [σG]
                         (reflEqTerm [σG]
                           (proj₁ (redSubstTerm β-red′ [σG] wk1t[0])))))
               (λ {_} {Δ₁} {a} {b} ρ ⊢Δ₁ [a] [b] [a≡b] →
                  let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ ρ [σ]
                      [a]′ = irrelevanceTerm′ (wk-subst F) ([F]′ ρ ⊢Δ₁)
                                              (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                      [b]′ = irrelevanceTerm′ (wk-subst F) ([F]′ ρ ⊢Δ₁)
                                              (proj₁ ([F] ⊢Δ₁ [ρσ])) [b]
                      [a≡b]′ = irrelevanceEqTerm′ (wk-subst F) ([F]′ ρ ⊢Δ₁)
                                                  (proj₁ ([F] ⊢Δ₁ [ρσ])) [a≡b]
                      ⊢F₁′ = escape (proj₁ ([F] ⊢Δ₁ [ρσ]))
                      ⊢F₁ = escape ([F]′ ρ ⊢Δ₁)
                      [G]₁ = proj₁ ([G] (⊢Δ₁ ∙ ⊢F₁′)
                                        (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ]))
                      [G]₁′ = irrelevanceΓ′
                                (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                                (PE.sym (wk-subst-lift G)) [G]₁
                      [t]′ = irrelevanceTermΓ″
                               (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                               (PE.sym (wk-subst-lift G))
                               (PE.sym (wk-subst-lift t))
                               [G]₁ [G]₁′
                               (proj₁ ([t] (⊢Δ₁ ∙ ⊢F₁′)
                                           (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ])))
                      ⊢a = escapeTerm ([F]′ ρ ⊢Δ₁) [a]
                      ⊢b = escapeTerm ([F]′ ρ ⊢Δ₁) [b]
                      ⊢t = escapeTerm [G]₁′ [t]′
                      G[a]′ = proj₁ ([G] ⊢Δ₁ ([ρσ] , [a]′))
                      G[a] = [G]′ ρ ⊢Δ₁ [a]
                      t[a] = irrelevanceTerm″
                               (PE.sym (singleSubstWkComp a σ G))
                               (PE.sym (singleSubstWkComp a σ t))
                               G[a]′ G[a]
                               (proj₁ ([t] ⊢Δ₁ ([ρσ] , [a]′)))
                      G[b]′ = proj₁ ([G] ⊢Δ₁ ([ρσ] , [b]′))
                      G[b] = [G]′ ρ ⊢Δ₁ [b]
                      t[b] = irrelevanceTerm″
                               (PE.sym (singleSubstWkComp b σ G))
                               (PE.sym (singleSubstWkComp b σ t))
                               G[b]′ G[b]
                               (proj₁ ([t] ⊢Δ₁ ([ρσ] , [b]′)))
                      lamt∘a≡t[a] = proj₂ (redSubstTerm (β-red ⊢F₁ ⊢t ⊢a) G[a] t[a])
                      G[a]≡G[b] = G-ext ρ ⊢Δ₁ [a] [b] [a≡b]
                      t[a]≡t[b] = irrelevanceEqTerm″
                                    (PE.sym (singleSubstWkComp a σ t))
                                    (PE.sym (singleSubstWkComp b σ t))
                                    (PE.sym (singleSubstWkComp a σ G))
                                    G[a]′ G[a]
                                    (proj₂ ([t] ⊢Δ₁ ([ρσ] , [a]′)) ([ρσ] , [b]′)
                                                (reflSubst [Γ] ⊢Δ₁ [ρσ] , [a≡b]′))
                      t[b]≡lamt∘b =
                        convEqTerm₂ G[a] G[b] G[a]≡G[b]
                          (symEqTerm G[b] (proj₂ (redSubstTerm (β-red ⊢F₁ ⊢t ⊢b)
                                                               G[b] t[b])))
                  in  transEqTerm G[a] lamt∘a≡t[a]
                             (transEqTerm G[a] t[a]≡t[b] t[b]≡lamt∘b))
               (λ {_} {Δ₁} {a} ρ ⊢Δ₁ [a] →
                  let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ ρ [σ]
                      [a]′ = irrelevanceTerm′ (wk-subst F) ([F]′ ρ ⊢Δ₁)
                                              (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                      ⊢F₁′ = escape (proj₁ ([F] ⊢Δ₁ [ρσ]))
                      ⊢F₁ = escape ([F]′ ρ ⊢Δ₁)
                      [G]₁ = proj₁ ([G] (⊢Δ₁ ∙ ⊢F₁′)
                                        (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ]))
                      [G]₁′ = irrelevanceΓ′
                                (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                                (PE.sym (wk-subst-lift G)) [G]₁
                      [t]′ = irrelevanceTermΓ″
                               (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                               (PE.sym (wk-subst-lift G))
                               (PE.sym (wk-subst-lift t))
                               [G]₁ [G]₁′
                               (proj₁ ([t] (⊢Δ₁ ∙ ⊢F₁′)
                                           (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ])))
                      ⊢a = escapeTerm ([F]′ ρ ⊢Δ₁) [a]
                      ⊢t = escapeTerm [G]₁′ [t]′
                      G[a]′ = proj₁ ([G] ⊢Δ₁ ([ρσ] , [a]′))
                      G[a] = [G]′ ρ ⊢Δ₁ [a]
                      t[a] = irrelevanceTerm″ (PE.sym (singleSubstWkComp a σ G))
                                               (PE.sym (singleSubstWkComp a σ t))
                                               G[a]′ G[a]
                                               (proj₁ ([t] ⊢Δ₁ ([ρσ] , [a]′)))
                  in  proj₁ (redSubstTerm (β-red ⊢F₁ ⊢t ⊢a) G[a] t[a]))
  in  lamt ⊢Δ [σ]
  ,   (λ {σ′} [σ′] [σ≡σ′] →
         let [liftσ′] = liftSubstS {F = F} [Γ] ⊢Δ [F] [σ′]
             Πᵣ F″ G″ D″ ⊢F″ ⊢G″ A≡A″ [F]″ [G]″ G-ext′ =
               extractMaybeEmbΠ (Π-elim (proj₁ ([ΠFG] ⊢Δ [σ′])))
             ⊢F′ = escape (proj₁ ([F] ⊢Δ [σ′]))
             [G]₁ = proj₁ ([G] (⊢Δ ∙ ⊢F) [liftσ])
             [G]₁′ = proj₁ ([G] (⊢Δ ∙ ⊢F′) [liftσ′])
             [σΠFG≡σ′ΠFG] = proj₂ ([ΠFG] ⊢Δ [σ]) [σ′] [σ≡σ′]
             ⊢t = escapeTerm [G]₁ (proj₁ ([t] (⊢Δ ∙ ⊢F) [liftσ]))
             ⊢t′ = escapeTerm [G]₁′ (proj₁ ([t] (⊢Δ ∙ ⊢F′) [liftσ′]))
             neuVar = neuTerm ([F]′ (step id) (⊢Δ ∙ ⊢F))
                              (var 0) (var (⊢Δ ∙ ⊢F) here)
                              (~-var (var (⊢Δ ∙ ⊢F) here))
             σlamt∘a≡σ′lamt∘a : ∀ {ρ Δ₁ a} → ([ρ] : ρ ∷ Δ₁ ⊆ Δ) (⊢Δ₁ : ⊢ Δ₁)
                 → ([a] : Δ₁ ⊩⟨ l ⟩ a ∷ U.wk ρ (subst σ F) / [F]′ [ρ] ⊢Δ₁)
                 → Δ₁ ⊩⟨ l ⟩ U.wk ρ (subst σ (lam t)) ∘ a
                           ≡ U.wk ρ (subst σ′ (lam t)) ∘ a
                           ∷ U.wk (lift ρ) (subst (liftSubst σ) G) [ a ]
                           / [G]′ [ρ] ⊢Δ₁ [a]
             σlamt∘a≡σ′lamt∘a {_} {Δ₁} {a} ρ ⊢Δ₁ [a] =
                let [ρσ] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ ρ [σ]
                    [ρσ′] = wkSubstS [Γ] ⊢Δ ⊢Δ₁ ρ [σ′]
                    [ρσ≡ρσ′] = wkSubstSEq [Γ] ⊢Δ ⊢Δ₁ ρ [σ] [σ≡σ′]
                    ⊢F₁′ = escape (proj₁ ([F] ⊢Δ₁ [ρσ]))
                    ⊢F₁ = escape ([F]′ ρ ⊢Δ₁)
                    ⊢F₂′ = escape (proj₁ ([F] ⊢Δ₁ [ρσ′]))
                    ⊢F₂ = escape ([F]″ ρ ⊢Δ₁)
                    [σF≡σ′F] = proj₂ ([F] ⊢Δ₁ [ρσ]) [ρσ′] [ρσ≡ρσ′]
                    [a]′ = irrelevanceTerm′ (wk-subst F) ([F]′ ρ ⊢Δ₁)
                                            (proj₁ ([F] ⊢Δ₁ [ρσ])) [a]
                    [a]″ = convTerm₁ (proj₁ ([F] ⊢Δ₁ [ρσ]))
                                      (proj₁ ([F] ⊢Δ₁ [ρσ′]))
                                      [σF≡σ′F] [a]′
                    ⊢a = escapeTerm ([F]′ ρ ⊢Δ₁) [a]
                    ⊢a′ = escapeTerm ([F]″ ρ ⊢Δ₁)
                            (irrelevanceTerm′ (PE.sym (wk-subst F))
                                              (proj₁ ([F] ⊢Δ₁ [ρσ′]))
                                              ([F]″ ρ ⊢Δ₁)
                                              [a]″)
                    G[a]′ = proj₁ ([G] ⊢Δ₁ ([ρσ] , [a]′))
                    G[a]₁′ = proj₁ ([G] ⊢Δ₁ ([ρσ′] , [a]″))
                    G[a] = [G]′ ρ ⊢Δ₁ [a]
                    G[a]″ = [G]″ ρ ⊢Δ₁
                                   (irrelevanceTerm′ (PE.sym (wk-subst F))
                                                     (proj₁ ([F] ⊢Δ₁ [ρσ′]))
                                                     ([F]″ ρ ⊢Δ₁)
                                                     [a]″)
                    [σG[a]≡σ′G[a]] = irrelevanceEq″
                                       (PE.sym (singleSubstWkComp a σ G))
                                       (PE.sym (singleSubstWkComp a σ′ G))
                                       G[a]′ G[a]
                                       (proj₂ ([G] ⊢Δ₁ ([ρσ] , [a]′))
                                              ([ρσ′] , [a]″)
                                              (consSubstSEq {t = a} {A = F}
                                                [Γ] ⊢Δ₁ [ρσ] [ρσ≡ρσ′] [F] [a]′))
                    [G]₁ = proj₁ ([G] (⊢Δ₁ ∙ ⊢F₁′)
                                      (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ]))
                    [G]₁′ = irrelevanceΓ′
                              (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                              (PE.sym (wk-subst-lift G)) [G]₁
                    [G]₂ = proj₁ ([G] (⊢Δ₁ ∙ ⊢F₂′)
                                      (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ′]))
                    [G]₂′ = irrelevanceΓ′
                              (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                              (PE.sym (wk-subst-lift G)) [G]₂
                    [t]′ = irrelevanceTermΓ″
                             (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                             (PE.sym (wk-subst-lift G)) (PE.sym (wk-subst-lift t))
                             [G]₁ [G]₁′
                             (proj₁ ([t] (⊢Δ₁ ∙ ⊢F₁′)
                                         (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ])))
                    [t]″ = irrelevanceTermΓ″
                              (PE.cong (λ x → _ ∙ x) (PE.sym (wk-subst F)))
                              (PE.sym (wk-subst-lift G)) (PE.sym (wk-subst-lift t))
                              [G]₂ [G]₂′
                              (proj₁ ([t] (⊢Δ₁ ∙ ⊢F₂′)
                                          (liftSubstS {F = F} [Γ] ⊢Δ₁ [F] [ρσ′])))
                    ⊢t = escapeTerm [G]₁′ [t]′
                    ⊢t′ = escapeTerm [G]₂′ [t]″
                    t[a] = irrelevanceTerm″
                             (PE.sym (singleSubstWkComp a σ G))
                             (PE.sym (singleSubstWkComp a σ t)) G[a]′ G[a]
                             (proj₁ ([t] ⊢Δ₁ ([ρσ] , [a]′)))
                    t[a]′ = irrelevanceTerm″
                              (PE.sym (singleSubstWkComp a σ′ G))
                              (PE.sym (singleSubstWkComp a σ′ t))
                              G[a]₁′ G[a]″
                              (proj₁ ([t] ⊢Δ₁ ([ρσ′] , [a]″)))
                    [σlamt∘a≡σt[a]] = proj₂ (redSubstTerm (β-red ⊢F₁ ⊢t ⊢a)
                                                          G[a] t[a])
                    [σ′t[a]≡σ′lamt∘a] =
                      convEqTerm₂ G[a] G[a]″ [σG[a]≡σ′G[a]]
                        (symEqTerm G[a]″
                           (proj₂ (redSubstTerm (β-red ⊢F₂ ⊢t′ ⊢a′)
                                                G[a]″ t[a]′)))
                    [σt[a]≡σ′t[a]] = irrelevanceEqTerm″
                                       (PE.sym (singleSubstWkComp a σ t))
                                       (PE.sym (singleSubstWkComp a σ′ t))
                                       (PE.sym (singleSubstWkComp a σ G))
                                       G[a]′ G[a]
                                       (proj₂ ([t] ⊢Δ₁ ([ρσ] , [a]′))
                                              ([ρσ′] , [a]″)
                                              (consSubstSEq {t = a} {A = F}
                                                [Γ] ⊢Δ₁ [ρσ] [ρσ≡ρσ′] [F] [a]′))
                in  transEqTerm G[a] [σlamt∘a≡σt[a]]
                                (transEqTerm G[a] [σt[a]≡σ′t[a]]
                                             [σ′t[a]≡σ′lamt∘a])
         in  Πₜ₌ (lam (subst (liftSubst σ) t)) (lam (subst (liftSubst σ′) t))
                 (idRedTerm:*: (lamⱼ ⊢F ⊢t))
                 (idRedTerm:*: (conv (lamⱼ ⊢F′ ⊢t′)
                                     (sym (≅-eq (escapeEq (proj₁ ([ΠFG] ⊢Δ [σ]))
                                                              [σΠFG≡σ′ΠFG])))))
                 lamₙ lamₙ
                 (≅-η-eq ⊢F (lamⱼ ⊢F ⊢t)
                      (conv (lamⱼ ⊢F′ ⊢t′)
                            (sym (≅-eq (escapeEq (proj₁ ([ΠFG] ⊢Δ [σ]))
                                              [σΠFG≡σ′ΠFG]))))
                      lamₙ lamₙ
                      (escapeTermEq
                        (proj₁ ([G] (⊢Δ ∙ ⊢F) [liftσ]))
                        (irrelevanceEqTerm′
                          (idWkLiftSubstLemma σ G)
                          ([G]′ (step id) (⊢Δ ∙ ⊢F) neuVar)
                          (proj₁ ([G] (⊢Δ ∙ ⊢F) [liftσ]))
                          (σlamt∘a≡σ′lamt∘a (step id) (⊢Δ ∙ ⊢F) neuVar))))
                  (lamt ⊢Δ [σ])
                  (convTerm₂ (proj₁ ([ΠFG] ⊢Δ [σ]))
                             (proj₁ ([ΠFG] ⊢Δ [σ′]))
                             [σΠFG≡σ′ΠFG]
                             (lamt ⊢Δ [σ′]))
                  σlamt∘a≡σ′lamt∘a)

-- Reducibility of η-equality under a valid substitution.
η-eqEqTerm : ∀ {f g F G Γ Δ σ l}
             ([Γ] : ⊩ᵛ Γ)
             ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
           → let [ΠFG] = Πᵛ {F} {G} [Γ] [F] [G] in
             Γ ∙ F ⊩ᵛ⟨ l ⟩ wk1 f ∘ var 0 ≡ wk1 g ∘ var 0 ∷ G
                          / [Γ] ∙″ [F] / [G]
           → (⊢Δ   : ⊢ Δ)
             ([σ]  : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
           → Δ ⊩⟨ l ⟩ subst σ f ∷ Π subst σ F ▹ subst (liftSubst σ) G
               / proj₁ ([ΠFG] ⊢Δ [σ])
           → Δ ⊩⟨ l ⟩ subst σ g ∷ Π subst σ F ▹ subst (liftSubst σ) G
               / proj₁ ([ΠFG] ⊢Δ [σ])
           → Δ ⊩⟨ l ⟩ subst σ f ≡ subst σ g ∷ Π subst σ F ▹ subst (liftSubst σ) G
               / proj₁ ([ΠFG] ⊢Δ [σ])
η-eqEqTerm {f} {g} {F} {G} {Γ} {Δ} {σ} [Γ] [F] [G] [f0≡g0] ⊢Δ [σ]
           (Πₜ f₁ [ ⊢t , ⊢u , d ] funcF f≡f [f] [f]₁)
           (Πₜ g₁ [ ⊢t₁ , ⊢u₁ , d₁ ] funcG g≡g [g] [g]₁) =
  let [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ ⊢t₁ , ⊢u₁ , d₁ ]
      [ΠFG] = Πᵛ {F} {G} [Γ] [F] [G]
      [σΠFG] = proj₁ ([ΠFG] ⊢Δ [σ])
      Πᵣ F′ G′ D′ ⊢F ⊢G A≡A [F]′ [G]′ G-ext = extractMaybeEmbΠ (Π-elim [σΠFG])
      [σF] = proj₁ ([F] ⊢Δ [σ])
      [wk1F] = wk (step id) (⊢Δ ∙ ⊢F) [σF]
      var0′ = var (⊢Δ ∙ ⊢F) here
      var0 = neuTerm [wk1F] (var 0) var0′ (~-var var0′)
      var0≡0 = neuEqTerm [wk1F] (var 0) (var 0) var0′ var0′ (~-var var0′)
      [σG]′ = [G]′ (step id) (⊢Δ ∙ ⊢F) var0
      [σG] = proj₁ ([G] (⊢Δ ∙ ⊢F) (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      σf0≡σg0 = escapeTermEq [σG]
                                 ([f0≡g0] (⊢Δ ∙ ⊢F)
                                          (liftSubstS {F = F} [Γ] ⊢Δ [F] [σ]))
      σf0≡σg0′ =
        PE.subst₂
          (λ x y → Δ ∙ subst σ F ⊢ x ≅ y ∷ subst (liftSubst σ) G)
          (PE.cong₂ _∘_ (PE.trans (subst-wk f) (PE.sym (wk-subst f))) PE.refl)
          (PE.cong₂ _∘_ (PE.trans (subst-wk g) (PE.sym (wk-subst g))) PE.refl)
          σf0≡σg0
      ⊢ΠFG = escape [σΠFG]
      f≡f₁′ = proj₂ (redSubst*Term d [σΠFG] (Πₜ f₁ (idRedTerm:*: ⊢u) funcF f≡f [f] [f]₁))
      g≡g₁′ = proj₂ (redSubst*Term d₁ [σΠFG] (Πₜ g₁ (idRedTerm:*: ⊢u₁) funcG g≡g [g] [g]₁))
      eq′  = irrelevanceEqTerm′ (cons0wkLift1-id σ G) [σG]′ [σG]
                                (app-congTerm [wk1F] [σG]′ (wk (step id) (⊢Δ ∙ ⊢F) [σΠFG])
                                              (wkEqTerm (step id) (⊢Δ ∙ ⊢F) [σΠFG] f≡f₁′) var0 var0 var0≡0)
      eq₁′ = irrelevanceEqTerm′ (cons0wkLift1-id σ G) [σG]′ [σG]
                                (app-congTerm [wk1F] [σG]′ (wk (step id) (⊢Δ ∙ ⊢F) [σΠFG])
                                              (wkEqTerm (step id) (⊢Δ ∙ ⊢F) [σΠFG] g≡g₁′) var0 var0 var0≡0)
      eq   = escapeTermEq [σG] eq′
      eq₁  = escapeTermEq [σG] eq₁′
  in  Πₜ₌ f₁ g₁ [d] [d′] funcF funcG
          (≅-η-eq ⊢F ⊢u ⊢u₁ funcF funcG
                  (≅ₜ-trans (≅ₜ-sym eq) (≅ₜ-trans σf0≡σg0′ eq₁)))
          (Πₜ f₁ [d] funcF f≡f [f] [f]₁)
          (Πₜ g₁ [d′] funcG g≡g [g] [g]₁)
          (λ {ρ} {Δ₁} {a} [ρ] ⊢Δ₁ [a] →
             let [F]″ = proj₁ ([F] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ]))
                 [a]′ = irrelevanceTerm′
                          (wk-subst F) ([F]′ [ρ] ⊢Δ₁)
                          [F]″ [a]
                 fEq = PE.cong₂ _∘_ (PE.trans (subst-wk f) (PE.sym (wk-subst f))) PE.refl
                 gEq = PE.cong₂ _∘_ (PE.trans (subst-wk g) (PE.sym (wk-subst g))) PE.refl
                 GEq = PE.sym (PE.trans (subst-wk (subst (liftSubst σ) G))
                                        (PE.trans (substCompEq G)
                                                  (cons-wk-subst ρ σ a G)))
                 f≡g = irrelevanceEqTerm″ fEq gEq GEq
                         (proj₁ ([G] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ] , [a]′)))
                         ([G]′ [ρ] ⊢Δ₁ [a])
                         ([f0≡g0] ⊢Δ₁ (wkSubstS [Γ] ⊢Δ ⊢Δ₁ [ρ] [σ] , [a]′))
                 [ρσΠFG] = wk [ρ] ⊢Δ₁ [σΠFG]
                 [f]′ : Δ ⊩⟨ _ ⟩ f₁ ∷ Π F′ ▹ G′ / [σΠFG]
                 [f]′ = Πₜ f₁ (idRedTerm:*: ⊢u) funcF f≡f [f] [f]₁
                 [ρf]′ = wkTerm [ρ] ⊢Δ₁ [σΠFG] [f]′
                 [g]′ : Δ ⊩⟨ _ ⟩ g₁ ∷ Π F′ ▹ G′ / [σΠFG]
                 [g]′ = Πₜ g₁ (idRedTerm:*: ⊢u₁) funcG g≡g [g] [g]₁
                 [ρg]′ = wkTerm [ρ] ⊢Δ₁ [σΠFG] [g]′
                 [f∘u] = appTerm ([F]′ [ρ] ⊢Δ₁) ([G]′ [ρ] ⊢Δ₁ [a]) [ρσΠFG] [ρf]′ [a]
                 [g∘u] = appTerm ([F]′ [ρ] ⊢Δ₁) ([G]′ [ρ] ⊢Δ₁ [a]) [ρσΠFG] [ρg]′ [a]
                 [tu≡fu] = proj₂ (redSubst*Term (app-subst* (wkRed*Term [ρ] ⊢Δ₁ d)
                                                            (escapeTerm ([F]′ [ρ] ⊢Δ₁) [a]))
                                                ([G]′ [ρ] ⊢Δ₁ [a]) [f∘u])
                 [gu≡t′u] = proj₂ (redSubst*Term (app-subst* (wkRed*Term [ρ] ⊢Δ₁ d₁)
                                                             (escapeTerm ([F]′ [ρ] ⊢Δ₁) [a]))
                                                 ([G]′ [ρ] ⊢Δ₁ [a]) [g∘u])
             in  transEqTerm ([G]′ [ρ] ⊢Δ₁ [a]) (symEqTerm ([G]′ [ρ] ⊢Δ₁ [a]) [tu≡fu])
                             (transEqTerm ([G]′ [ρ] ⊢Δ₁ [a]) f≡g [gu≡t′u]))

-- Validity of η-equality.
η-eqᵛ : ∀ {f g F G Γ l}
        ([Γ] : ⊩ᵛ Γ)
        ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
        ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / ([Γ] ∙″ [F]))
      → let [ΠFG] = Πᵛ {F} {G} [Γ] [F] [G] in
        Γ ⊩ᵛ⟨ l ⟩ f ∷ Π F ▹ G / [Γ] / [ΠFG]
      → Γ ⊩ᵛ⟨ l ⟩ g ∷ Π F ▹ G / [Γ] / [ΠFG]
      → Γ ∙ F ⊩ᵛ⟨ l ⟩ wk1 f ∘ var 0 ≡ wk1 g ∘ var 0 ∷ G
                     / [Γ] ∙″ [F] / [G]
      → Γ ⊩ᵛ⟨ l ⟩ f ≡ g ∷ Π F ▹ G / [Γ] / [ΠFG]
η-eqᵛ {f} {g} {F} {G} [Γ] [F] [G] [f] [g] [f0≡g0] {Δ} {σ} ⊢Δ [σ] =
  η-eqEqTerm {f} {g} {F} {G} [Γ] [F] [G] [f0≡g0] ⊢Δ [σ]
                (proj₁ ([f] ⊢Δ [σ])) (proj₁ ([g] ⊢Δ [σ]))

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Prelude.Variables where

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.List

variable
  ℓ ℓ₁ ℓ₂ ℓ₃ : Level
  A B C : Set ℓ
  F M : Set ℓ₁ → Set ℓ₂
  x y z : A
  xs ys zs : List A
  n m : Nat

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
-- Solver for functors

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

open import Categories.Category
open import Categories.Functor renaming (id to idF)

module Experiment.Categories.Solver.MultiFunctor {o ℓ e} where

import Categories.Morphism.Reasoning as MR

open import Level
open import Relation.Binary using (Rel)

infixr 9 _:∘_

data Expr : (𝒞 : Category o ℓ e) → Rel (Category.Obj 𝒞) (suc (o ⊔ ℓ ⊔ e)) where
  :id  : ∀ {𝒞 A} → Expr 𝒞 A A
  _:∘_ : ∀ {𝒞 A B C} → Expr 𝒞 B C → Expr 𝒞 A B → Expr 𝒞 A C
  :F₁  : ∀ {𝒞 𝒟} (F : Functor 𝒟 𝒞) {A B} →
         Expr 𝒟 A B → Expr 𝒞 (Functor.F₀ F A) (Functor.F₀ F B)
  ∥_∥  : ∀ {𝒞 A B} → 𝒞 [ A , B ] → Expr 𝒞 A B

-- Semantics
_⟦_⟧ : ∀ 𝒞 {A B} → Expr 𝒞 A B → 𝒞 [ A , B ]
𝒞 ⟦ :id ⟧      = Category.id 𝒞
𝒞 ⟦ e₁ :∘ e₂ ⟧ = 𝒞 [ 𝒞 ⟦ e₁ ⟧ ∘ 𝒞 ⟦ e₂ ⟧ ]
𝒞 ⟦ :F₁ F e ⟧  = Functor.F₁ F (_ ⟦ e ⟧)
𝒞 ⟦ ∥ f ∥ ⟧    = f

N∘ : ∀ (𝒞 𝒟 : Category o ℓ e) (F : Functor 𝒟 𝒞) {A B C} →
     Expr 𝒟 B C → 𝒞 [ A , Functor.F₀ F B ] → 𝒞 [ A , Functor.F₀ F C ]
N∘ 𝒞 𝒟 F :id                g = g
N∘ 𝒞 𝒟 F (e₁ :∘ e₂)         g = N∘ 𝒞 𝒟 F e₁ (N∘ 𝒞 𝒟 F e₂ g)
N∘ 𝒞 𝒟 F (:F₁ {𝒟 = ℰ} G e) g = N∘ 𝒞 ℰ (F ∘F G) e g
N∘ 𝒞 𝒟 F ∥ f ∥              g = 𝒞 [ Functor.F₁ F f ∘ g ]

_⟦_⟧N : ∀ 𝒞 {A B} → Expr 𝒞 A B → 𝒞 [ A , B ]
𝒞 ⟦ e ⟧N = N∘ 𝒞 𝒞 idF e (Category.id 𝒞)

N∘≈⟦⟧ : ∀ 𝒞 𝒟 (F : Functor 𝒟 𝒞) {A B C}
        (e : Expr 𝒟 B C) (g : 𝒞 [ A , Functor.F₀ F B ]) →
        𝒞 [ N∘ 𝒞 𝒟 F e g ≈ 𝒞 [ Functor.F₁ F (𝒟 ⟦ e ⟧) ∘ g ] ]
N∘≈⟦⟧ 𝒞 𝒟 F :id                g = begin
  g                       ≈˘⟨ identityˡ ⟩
  id ∘ g                  ≈˘⟨ identity ⟩∘⟨refl ⟩
  F₁ (Category.id 𝒟) ∘ g ∎
  where open Category 𝒞
        open Functor F
        open HomReasoning
N∘≈⟦⟧ 𝒞 𝒟 F (e₁ :∘ e₂)         g = begin
  N∘ 𝒞 𝒟 F e₁ (N∘ 𝒞 𝒟 F e₂ g)       ≈⟨ N∘≈⟦⟧ 𝒞 𝒟 F e₁ (N∘ 𝒞 𝒟 F e₂ g) ⟩
  F₁ (𝒟 ⟦ e₁ ⟧) ∘ N∘ 𝒞 𝒟 F e₂ g      ≈⟨ pushʳ (N∘≈⟦⟧ 𝒞 𝒟 F e₂ g) ⟩
  (F₁ (𝒟 ⟦ e₁ ⟧) ∘ F₁ (𝒟 ⟦ e₂ ⟧)) ∘ g ≈˘⟨ homomorphism ⟩∘⟨refl ⟩
  F₁ (𝒟 [ 𝒟 ⟦ e₁ ⟧ ∘ 𝒟 ⟦ e₂ ⟧ ]) ∘ g ∎
  where open Category 𝒞
        open HomReasoning
        open MR 𝒞
        open Functor F
N∘≈⟦⟧ 𝒞 𝒟 F (:F₁ {𝒟 = ℰ} G e) g = N∘≈⟦⟧ 𝒞 ℰ (F ∘F G) e g
N∘≈⟦⟧ 𝒞 𝒟 F ∥ f ∥              g = Category.Equiv.refl 𝒞

⟦e⟧N≈⟦e⟧ : ∀ 𝒞 {A B} (e : Expr 𝒞 A B) → 𝒞 [ 𝒞 ⟦ e ⟧N ≈ 𝒞 ⟦ e ⟧ ]
⟦e⟧N≈⟦e⟧ 𝒞 e = N∘≈⟦⟧ 𝒞 𝒞 idF e id ○ identityʳ
  where open Category 𝒞
        open HomReasoning

solve : ∀ {𝒞 A B} (e₁ e₂ : Expr 𝒞 A B) →
        𝒞 [ 𝒞 ⟦ e₁ ⟧N ≈ 𝒞 ⟦ e₂ ⟧N ] → 𝒞 [ 𝒞 ⟦ e₁ ⟧ ≈ 𝒞 ⟦ e₂ ⟧ ]
solve {𝒞 = 𝒞} e₁ e₂ eq = begin
  𝒞 ⟦ e₁ ⟧  ≈˘⟨ ⟦e⟧N≈⟦e⟧ 𝒞 e₁ ⟩
  𝒞 ⟦ e₁ ⟧N ≈⟨ eq ⟩
  𝒞 ⟦ e₂ ⟧N ≈⟨ ⟦e⟧N≈⟦e⟧ 𝒞 e₂ ⟩
  𝒞 ⟦ e₂ ⟧  ∎
  where open Category 𝒞
        open HomReasoning

∥-∥ : ∀ {𝒞 A B} {f : 𝒞 [ A , B ]} → Expr 𝒞 A B
∥-∥ {f = f} = ∥ f ∥


text:
-- Andreas, 2017-05-17, issue #2574 reported by G. Allais

open import Issue2574Import        -- The imported module should be clickable.
open import Issue2574ImportBlank   -- The imported module should be clickable.


text:
-- Currently this test case is broken. Once Issue 3451 has been fixed
-- it should be moved to test/Fail (and this comment should be
-- removed).

-- The option --guardedness turns off sized types.

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Size

record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream A j

open Stream

postulate
  destroy-guardedness : {A : Set} → A → A

repeat : ∀ {A i} → A → Stream A i
repeat x .head = x
repeat x .tail = destroy-guardedness (repeat x)

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
module Class.MonadTrans where

open import Class.Monad
open import Level

record MonadTrans {a} (T : (Set a -> Set a) -> Set a -> Set a) : Set (suc a) where
  field
    embed : {A : Set a} {M : Set a -> Set a} {{_ : Monad M}} -> M A -> T M A

open MonadTrans {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
module Numeral.Natural.Relation.Order where

import Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Relator.Equals
open import Relator.Equals.Proofs
open import Relator.Ordering

-- Inequalities/Comparisons

data _≤_ : ℕ → ℕ → Stmt{Lvl.𝟎} where
  min  : ∀{y} → (𝟎 ≤ y)
  succ : ∀{x y} → (x ≤ y) → (𝐒(x) ≤ 𝐒(y))

_<_ : ℕ → ℕ → Stmt
_<_ a b = (𝐒(a) ≤ b)

open From-[≤][<] (_≤_) (_<_) public

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Eq.ObsTheory where

open import Prelude
open import T
open import DynTheory
open import SubstTheory
open import Contexts
open import Eq.Defs
open import Eq.KleeneTheory

open ObservEq
---- Proofs about observational equivalence

-- observational equivalence being an equiv reln follows trivially from kleene equiv being one
obs-refl : ∀ {Γ} {A} → Reflexive (ObservEq Γ A)
obs-refl = obs (λ C → kleene-refl)
obs-sym : ∀ {Γ} {A} → Symmetric (ObservEq Γ A)
obs-sym eq = obs (λ C → kleene-sym (observe eq C))
obs-trans : ∀ {Γ} {A} → Transitive (ObservEq Γ A)
obs-trans eq1 eq2 = obs (λ C → kleene-trans (observe eq1 C) (observe eq2 C))

obs-is-equivalence : ∀{Γ} {A} → IsEquivalence (ObservEq Γ A)
obs-is-equivalence = record { refl_ = obs-refl
                            ; sym_ = obs-sym
                            ; trans_ = obs-trans }

obs-congruence : Congruence ObservEq
obs-congruence {e = e} {e' = e'} oeq C = obs help
  where help : (C₁ : TCtx _ _ _ _) → KleeneEq (C₁ < C < e > >) (C₁ < C < e' > >)
        help C' with observe oeq (C' << C >>)
        ... | keq = ID.coe2 KleeneEq (composing-commutes C' C e) (composing-commutes C' C e') keq

obs-consistent : Consistent ObservEq
obs-consistent oeq = observe oeq ∘

obs-is-con-congruence : IsConsistentCongruence ObservEq
obs-is-con-congruence = record { equiv = obs-is-equivalence
                               ; cong = obs-congruence
                               ; consistent = obs-consistent
                               }

-- Prove that observational equivalence is the coarsest consistent congruence.
-- That is, that it contains all other consistent congruences.
-- That is, if two terms are related by a consistent congruence, they are
-- observationally equivalence.
obs-is-coarsest : (R : TRel) → IsConsistentCongruence R →
                  {Γ : Ctx} {A : TTp} →
                  (R Γ A) ⊆ (ObservEq Γ A)
obs-is-coarsest R isCC eq = obs help
  where help : (C : TCtx _ _ _ _) → KleeneEq (C < _ >) (C < _ >)
        help C with (IsConsistentCongruence.cong isCC) eq C
        ... | eqC = (IsConsistentCongruence.consistent isCC) eqC

-- Produce a program context that is "equivalent" to a substitution.
-- Essentially the idea is, if we have a substitution
-- γ = e1/x1,...,en/xn, we produce the term
-- (λx1. ⋯ λxn. ∘) e1 ⋯ en
--
-- It took me a while of fiddling around before I came up with this
-- implementation based on composing contexts, but it works really nicely.
--
-- The earlier version that I got closest to making work placed the
-- terms we were substituting underneath other lambdas, which almost
-- works; since it requires weakening the terms, it means to prove
-- subst-ctx-respect-obs we would need to show that weakening preserves
-- observational equivalence. I don't know how to do this without using
-- that observational and logical equivalence coincide.
subst-ctx : ∀{Γ C} → (γ : TSubst Γ []) → (TCtx Γ C [] C)
subst-ctx {[]} γ = ∘
subst-ctx {A :: Γ} {C} γ with (subst-ctx {Γ} {A ⇒ C} (dropγ γ))
... | D = (D << Λ ∘ >>) $e (γ Z)

-- This would basically be the end of the world in call by value.
-- On paper, this proof goes:
--
-- Given some substitution γ[x -> e'], want to show that
-- (C << (λ x. ∘) >> e') < e > e'~>* γ[x -> e'](e), where C is the context constructed for γ.
-- We know that (C << (λ x. ∘) >> e') < e > = C << (λ x. e) >> e'.
-- By induction, we have that "C << (λ x. e) >> ~>* (λ x. γ(e))", and by compatability rules,
-- C << (λ x. e) >> e' ~>* (λ x. γ(e)) e'
-- Then, by beta, we have that (λ x. γ(e)) e' ~> γ([e'/x]e)).
subst-ctx-substs : ∀{Γ A} → (γ : TSubst Γ []) → (e : TExp Γ A) →
                   (subst-ctx γ) < e > ~>* ssubst γ e
subst-ctx-substs {[]} γ e = ID.coe1 (_~>*_ e) (symm (closed-subst γ e)) eval-refl
subst-ctx-substs {x :: Γ} γ e with subst-ctx-substs (dropγ γ) (Λ e)
... | recursive-eval with eval-compat (step-app-l {e₂ = γ Z}) recursive-eval
... | compat-eval with step-beta {e = ssubst (liftγ (dropγ γ)) e} {e' = γ Z}
... | step with eval-trans compat-eval (eval-step step)

... | eval with composing-commutes (subst-ctx (dropγ γ)) (Λ ∘) e
... | ctx-eq with (symm (subcomp (singγ (γ Z)) (liftγ (dropγ γ)) e) ≡≡ symm (subeq (drop-fix γ) e))
... | subst-eq = ID.coe2 (λ y z → (y $ γ Z) ~>* z) (symm ctx-eq) subst-eq eval

-- Straightforward extension of the above theorem to kleene equivalence at nat type.
subst-ctx-substs-eq : ∀{Γ} → (γ : TSubst Γ []) → (e : TExp Γ nat) →
                     (subst-ctx γ) < e > ≃ ssubst γ e
subst-ctx-substs-eq γ e with subst-ctx-substs γ e | kleene-refl {x = ssubst γ e}
... | eval | kleeneq n val E1 E2 = kleeneq n val (eval-trans eval E1) E2

-- Prove that observationally equivalent substitutions yield
-- contexts that are observationally equivalent when applied to a term.
subst-ctx-respect-obs : ∀{Γ} {A} (e : TExp Γ A) {γ γ' : TSubst Γ []} →
                         SubstRel (ObservEq []) Γ γ γ' →
                         [] ⊢ subst-ctx γ < e > ≅ subst-ctx γ' < e > :: A
subst-ctx-respect-obs {[]} e η = obs-refl
subst-ctx-respect-obs {B :: Γ} {A} e {γ} {γ'} η with
  subst-ctx-respect-obs (Λ e) {dropγ γ} {dropγ γ'} (λ x → η (S x))
... | D-D'-equiv with obs-congruence D-D'-equiv (∘ $e γ Z)
... | cong1 with obs-congruence (η Z) ((subst-ctx (dropγ γ') < Λ e >) e$ ∘)
... | cong2 with obs-trans cong1 cong2
... | equiv =
  ID.coe2 (ObservEq [] A)
  (symm (resp (λ x → x $ γ Z) (composing-commutes (subst-ctx (dropγ γ)) (Λ ∘) e)))
  (symm (resp (λ x → x $ γ' Z) (composing-commutes (subst-ctx (dropγ γ')) (Λ ∘) e)))
  equiv

-- Applying a substitution to two obs equivalent terms yields observational equivalent output.
-- Takes advantage of substitution contexts.
substs-respect-obs-1 : ∀{Γ} {A} {e e' : TExp Γ A} {γ : TSubst Γ []} →
                       Γ ⊢ e ≅ e' :: A →
                       [] ⊢ ssubst γ e ≅ ssubst γ e' :: A
substs-respect-obs-1 {Γ} {A} {e} {e'} {γ} (obs observe) = obs help
  where help : (C : TCtx [] A [] nat) → KleeneEq (C < ssubst γ e >) (C < ssubst γ e' >)
        help C with observe (subst-ctx γ << weaken-closed-tctx C >>)
        ... | D-equiv with ID.coe2 KleeneEq
                           (composing-commutes (subst-ctx γ) (weaken-closed-tctx C) e)
                           (composing-commutes (subst-ctx γ) (weaken-closed-tctx C) e')
                           D-equiv
        ... | D-equiv2 with subst-ctx-substs-eq γ ((weaken-closed-tctx C) < e >) |
                            subst-ctx-substs-eq γ ((weaken-closed-tctx C) < e' >)
        ... | sub-equiv1 | sub-equiv2 with
          kleene-trans (kleene-sym sub-equiv1) (kleene-trans D-equiv2 sub-equiv2)
        ... | equiv = ID.coe2 KleeneEq
              (symm (subst-commutes-w-closed-tctx γ C e))
                (symm (subst-commutes-w-closed-tctx γ C e')) equiv

-- Applying observationally equivalent substitutions a term
-- yields observational equivalent output.
-- Takes advantage of substitution contexts.
-- There is much in this proof that is similar to substs-respect-obs-1.
-- Maybe they could have been merged more?
substs-respect-obs-2 : ∀{Γ} {A} (e : TExp Γ A) {γ γ' : TSubst Γ []} →
                       SubstRel (ObservEq []) Γ γ γ' →
                       [] ⊢ ssubst γ e ≅ ssubst γ' e :: A
substs-respect-obs-2 {Γ} {A} e {γ} {γ'} η = obs help
  where help : (C : TCtx [] A [] nat) → KleeneEq (C < ssubst γ e >) (C < ssubst γ' e >)
        help C with subst-ctx-respect-obs (weaken-closed-tctx C < e >) η
        ... | oeq with obs-consistent oeq
        ... | keq with subst-ctx-substs-eq γ ((weaken-closed-tctx C) < e >) |
                       subst-ctx-substs-eq γ' ((weaken-closed-tctx C) < e >)
        ... | sub-equiv1 | sub-equiv2 with
          kleene-trans (kleene-sym sub-equiv1) (kleene-trans keq sub-equiv2)
        ... | equiv = ID.coe2 KleeneEq
              (symm (subst-commutes-w-closed-tctx γ C e))
              (symm (subst-commutes-w-closed-tctx γ' C e)) equiv

-- Combine the two previous theorems.
substs-respect-obs : ∀{Γ} {A} {e e' : TExp Γ A} {γ γ' : TSubst Γ []} →
                     Γ ⊢ e ≅ e' :: A →
                     SubstRel (ObservEq []) Γ γ γ' →
                     [] ⊢ ssubst γ e ≅ ssubst γ' e' :: A
substs-respect-obs {Γ} {A} {e} {e'} {γ} {γ'} oeq η =
  obs-trans (substs-respect-obs-2 e η) (substs-respect-obs-1 oeq)

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


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

module function.fibration where

open import level
open import sum
open import equality.core
open import function.core
open import function.isomorphism.core
open import function.isomorphism.coherent
open import function.isomorphism.lift
open import function.isomorphism.univalence
open import function.isomorphism.utils
open import function.extensionality.core
open import function.extensionality.proof
open import function.overloading
open import hott.level.core
open import hott.equivalence.core
open import hott.equivalence.alternative
open import hott.univalence
open import sets.unit

Fibration : ∀ {i} j → Set i → Set _
Fibration j X = Σ (Set j) λ Y → Y → X

fib : ∀ {i j}{X : Set i}(Y : X → Set j)
    → Σ X Y → X
fib Y = proj₁

fib-iso : ∀ {i j}{X : Set i}{Y : X → Set j}
        → (x : X)
        → fib Y ⁻¹ x ≅ Y x
fib-iso {X = X}{Y = Y} x = begin
    fib Y ⁻¹ x
  ≅⟨ refl≅ ⟩
    ( Σ (Σ X Y) λ { (x' , y)
    → x' ≡ x } )
  ≅⟨ Σ-assoc-iso ⟩
    ( Σ X λ x' → Y x' × x' ≡ x )
  ≅⟨ (Σ-ap-iso refl≅ λ x' → ×-comm) ⟩
    ( Σ X λ x' → x' ≡ x × Y x' )
  ≅⟨ sym≅ Σ-assoc-iso ⟩
    ( Σ (singleton' x) λ { (x' , _) → Y x' } )
  ≅⟨ Σ-ap-iso' (contr-⊤-iso (singl-contr' x)) (λ _ → refl≅) ⟩
    ( ⊤ × Y x )
  ≅⟨ ×-left-unit ⟩
    Y x
  ∎
  where open ≅-Reasoning

total-iso : ∀ {i j}{X : Set i}{Y : Set j}(p : Y → X)
          → (Σ X (_⁻¹_ p)) ≅ Y
total-iso {X = X}{Y = Y} p = begin
    ( Σ X λ x → (Σ Y λ y → p y ≡ x) )
  ≅⟨ Σ-comm-iso ⟩
    ( Σ Y λ y → (Σ X λ x → p y ≡ x) )
  ≅⟨ ( Σ-ap-iso refl≅ λ y → contr-⊤-iso (singl-contr (p y)) ) ⟩
    (Y × ⊤)
  ≅⟨ ×-right-unit ⟩
    Y
  ∎
  where open ≅-Reasoning

fib-eq-iso : ∀ {i j}{X : Set i}{Y₁ Y₂ : Set j}
           → (p₁ : Y₁ → X) (p₂ : Y₂ → X)
           → _≡_ {A = Fibration _ X} (Y₁ , p₁) (Y₂ , p₂)
           ≅ ( Σ (Y₁ ≅' Y₂) λ q → p₁ ≡ p₂ ∘ apply q )
fib-eq-iso {i}{j}{X}{Y₁}{Y₂} p₁ p₂ = begin
    _≡_ {A = Fibration _ X} (Y₁ , p₁) (Y₂ , p₂)
  ≅⟨ sym≅ Σ-split-iso ⟩
    ( Σ (Y₁ ≡ Y₂) λ q → subst (λ Y → Y → X) q p₁ ≡ p₂ )
  ≅⟨ ( Σ-ap-iso refl≅ λ q → lem q p₁ p₂ ) ⟩
    ( Σ (Y₁ ≡ Y₂) λ q → p₁ ≡ p₂ ∘ coerce q )
  ≅⟨ step ⟩
    ( Σ (Y₁ ≅' Y₂) λ q → p₁ ≡ p₂ ∘ apply q )
  ∎
  where
    open ≅-Reasoning
    abstract
      step : ( Σ (Y₁ ≡ Y₂) λ q → p₁ ≡ p₂ ∘ coerce q )
           ≅ ( Σ (Y₁ ≅' Y₂) λ q → p₁ ≡ p₂ ∘ apply q )
      step = Σ-ap-iso (uni-iso ·≅ ≈⇔≅') λ q → refl≅

    abstract
      lem : {Y₁ Y₂ : Set j}(q : Y₁ ≡ Y₂)(p₁ : Y₁ → X)(p₂ : Y₂ → X)
          → (subst (λ Y → Y → X) q p₁ ≡ p₂)
          ≅ (p₁ ≡ p₂ ∘ coerce q)
      lem refl p₁ p₂ = refl≅

fibration-iso : ∀ {i} j {X : Set i}
              → (Σ (Set (i ⊔ j)) λ Y → Y → X)
              ≅ (X → Set (i ⊔ j))
fibration-iso {i} j {X} = record
  { to = λ { (Y , p) x → p ⁻¹ x }
  ; from = λ P → (Σ X P , fib P)
  ; iso₁ = λ { (Y , p) → α Y p }
  ; iso₂ = λ P → funext λ x → ≅⇒≡ (fib-iso x) }
  where
    α : (Y : Set (i ⊔ j))(p : Y → X)
      → _≡_ {A = Σ (Set (i ⊔ j)) λ Y → Y → X}
        (Σ X (_⁻¹_ p) , proj₁)
        (Y , p)
    α Y p = invert (fib-eq-iso proj₁ p)
            ( ≅⇒≅' (total-iso p)
            , funext λ { (y , x , eq) → sym eq } )

family-eq-iso : ∀ {i j₁ j₂}{X : Set i}{Y₁ : X → Set j₁}{Y₂ : X → Set j₂}
              → (isom : Σ X Y₁ ≅ Σ X Y₂)
              → (∀ x y → proj₁ (apply≅ isom (x , y)) ≡ x)
              → (x : X) → Y₁ x ≅ Y₂ x
family-eq-iso {i}{j₁}{j₂}{X}{Y₁}{Y₂} isom comm x
  = lift-iso _ (Y₁ x)
  ·≅ ≡⇒≅ (funext-inv eq' x)
  ·≅ sym≅ (lift-iso _ (Y₂ x))
  where
    open _≅_ isom

    to-we : weak-equiv to
    to-we = proj₂ (≅⇒≈ isom)

    P₁ : X → Set (i ⊔ j₁ ⊔ j₂)
    P₁ x = ↑ (i ⊔ j₂) (Y₁ x)

    p₁ : Σ X P₁ → X
    p₁ = proj₁

    P₂ : X → Set (i ⊔ j₁ ⊔ j₂)
    P₂ x = ↑ (i ⊔ j₁) (Y₂ x)

    p₂ : Σ X P₂ → X
    p₂ = proj₁

    total : Σ X P₁ ≅ Σ X P₂
    total = (Σ-ap-iso refl≅ λ x → sym≅ (lift-iso _ _))
          ·≅ isom
          ·≅ (Σ-ap-iso refl≅ λ x → lift-iso _ _)

    comm' : (a : Σ X P₁) → p₁ a ≡ p₂ (apply total a)
    comm' (x , lift u) = sym (comm x u)

    eq' : P₁ ≡ P₂
    eq' = iso⇒inj (sym≅ (fibration-iso (i ⊔ j₁ ⊔ j₂)))
          (invert (fib-eq-iso p₁ p₂) (≅⇒≅' total , funext comm'))

fib-compose : ∀ {i j k}{X : Set i}{Y : Set j}{Z : Set k}
            → (f : X → Y)(g : Y → Z)(z : Z)
            → (g ∘' f) ⁻¹ z
            ≅ ( Σ (g ⁻¹ z) λ { (y , _) → f ⁻¹ y } )
fib-compose {X = X}{Y}{Z} f g z = begin
    (g ∘' f) ⁻¹ z
  ≅⟨ refl≅ ⟩
    ( Σ X λ x → g (f x) ≡ z )
  ≅⟨ Σ-ap-iso refl≅ (λ _ → sym≅ ×-left-unit) ⟩
    ( Σ X λ x → ⊤ × g (f x) ≡ z)
  ≅⟨ ( Σ-ap-iso refl≅ λ x
      → Σ-ap-iso (sym≅ (contr-⊤-iso (singl-contr (f x))) ) λ _
      → refl≅ ) ⟩
    ( Σ X λ x → singleton (f x) × g (f x) ≡ z )
  ≅⟨ ( Σ-ap-iso refl≅ λ x → Σ-assoc-iso ) ⟩
    ( Σ X λ x → Σ Y λ y → (f x ≡ y) × (g (f x) ≡ z) )
  ≅⟨ ( Σ-ap-iso refl≅ λ x
       → Σ-ap-iso refl≅ λ y
       → Σ-ap-iso refl≅ λ p
       → ≡⇒≅ (ap (λ u → g u ≡ z) p) ) ⟩
    ( Σ X λ x → Σ Y λ y → (f x ≡ y) × (g y ≡ z) )
  ≅⟨ Σ-comm-iso ⟩
    ( Σ Y λ y → Σ X λ x → (f x ≡ y) × (g y ≡ z) )
  ≅⟨ ( Σ-ap-iso refl≅ λ y → sym≅ Σ-assoc-iso ) ⟩
    ( Σ Y λ y → (f ⁻¹ y) × (g y ≡ z) )
  ≅⟨ ( Σ-ap-iso refl≅ λ y → ×-comm ) ⟩
    ( Σ Y λ y →  (g y ≡ z) × (f ⁻¹ y) )
  ≅⟨ sym≅ Σ-assoc-iso ⟩
    ( Σ (g ⁻¹ z) λ { (y , _) → f ⁻¹ y } )
  ∎
  where open ≅-Reasoning

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

open import HoTT

module Reflective where

  record ReflectiveSubuniverse {ℓ} : Type (lsucc ℓ) where
    field

      P : Type ℓ → Type ℓ
      R : Type ℓ → Type ℓ

      η : (A : Type ℓ) → A → R A

      -- replete : (A B : Type ℓ) → P A → A ≃ B → P B

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category

private
  variable
    ℓ ℓ' : Level

-- C needs to be explicit for these definitions as Agda can't infer it
module _ (C : Category ℓ ℓ') where
  open Category C

  private
    variable
      x y z w : ob

  isMonic : Hom[ x , y ] → Type (ℓ-max ℓ ℓ')
  isMonic {x} {y} f =
    ∀ {z} {a a' : Hom[ z , x ]} → f ∘ a ≡ f ∘ a' → a ≡ a'

  isEpic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')
  isEpic {x} {y} g =
    ∀ {z} {b b' : Hom[ y , z ]} → b ∘ g ≡ b' ∘ g → b ≡ b'

  -- A morphism is split monic if it has a *retraction*
  isSplitMon : (Hom[ x , y ]) → Type ℓ'
  isSplitMon {x} {y} f = ∃[ r ∈ Hom[ y , x ] ] r ∘ f ≡ id

  -- A morphism is split epic if it has a *section*
  isSplitEpi : (Hom[ x , y ]) → Type ℓ'
  isSplitEpi {x} {y} g = ∃[ s ∈ Hom[ y , x ] ] g ∘ s ≡ id

  record areInv (f : Hom[ x , y ]) (g : Hom[ y , x ]) : Type ℓ' where
    field
      sec : g ⋆ f ≡ id
      ret : f ⋆ g ≡ id

  record isIso (f : Hom[ x , y ]) : Type ℓ' where
    field
      inv : Hom[ y , x ]
      sec : inv ⋆ f ≡ id
      ret : f ⋆ inv ≡ id

-- C can be implicit here
module _ {C : Category ℓ ℓ'} where
  open Category C

  private
    variable
      x y z w : ob

  open areInv

  symAreInv : {f : Hom[ x , y ]} {g : Hom[ y , x ]} → areInv C f g → areInv C g f
  sec (symAreInv x) = ret x
  ret (symAreInv x) = sec x

  -- equational reasoning with inverses
  invMoveR : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ z , x ]} {k : Hom[ z , y ]}
           → areInv C f g
           → h ⋆ f ≡ k
           → h ≡ k ⋆ g
  invMoveR {f = f} {g} {h} {k} ai p
    = h
    ≡⟨ sym (⋆IdR _) ⟩
      (h ⋆ id)
    ≡⟨ cong (h ⋆_) (sym (ai .ret)) ⟩
      (h ⋆ (f ⋆ g))
    ≡⟨ sym (⋆Assoc _ _ _) ⟩
      ((h ⋆ f) ⋆ g)
    ≡⟨ cong (_⋆ g) p ⟩
      k ⋆ g
    ∎

  invMoveL : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ y , z ]} {k : Hom[ x , z ]}
          → areInv C f g
          → f ⋆ h ≡ k
          → h ≡ g ⋆ k
  invMoveL {f = f} {g} {h} {k} ai p
    = h
    ≡⟨ sym (⋆IdL _) ⟩
      id ⋆ h
    ≡⟨ cong (_⋆ h) (sym (ai .sec)) ⟩
      (g ⋆ f) ⋆ h
    ≡⟨ ⋆Assoc _ _ _ ⟩
      g ⋆ (f ⋆ h)
    ≡⟨ cong (g ⋆_) p ⟩
      (g ⋆ k)
    ∎

  open isIso

  isIso→areInv : ∀ {f : Hom[ x , y ]}
               → (isI : isIso C f)
               → areInv C f (isI .inv)
  sec (isIso→areInv isI) = sec isI
  ret (isIso→areInv isI) = ret isI

  open CatIso

  -- isIso agrees with CatIso
  isIso→CatIso : ∀ {f : C [ x , y ]}
               → isIso C f
               → CatIso C x y
  mor (isIso→CatIso {f = f} x) = f
  inv (isIso→CatIso x) = inv x
  sec (isIso→CatIso x) = sec x
  ret (isIso→CatIso x) = ret x

  CatIso→isIso : (cIso : CatIso C x y)
               → isIso C (cIso .mor)
  inv (CatIso→isIso f) = inv f
  sec (CatIso→isIso f) = sec f
  ret (CatIso→isIso f) = ret f

  CatIso→areInv : (cIso : CatIso C x y)
                → areInv C (cIso .mor) (cIso .inv)
  CatIso→areInv cIso = isIso→areInv (CatIso→isIso cIso)

  -- reverse of an iso is also an iso
  symCatIso : ∀ {x y}
             → CatIso C x y
             → CatIso C y x
  symCatIso (catiso mor inv sec ret) = catiso inv mor ret sec


text:
------------------------------------------------------------------------
-- Pi with partiality algebra families as codomains
------------------------------------------------------------------------

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

module Partiality-algebra.Pi where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (T)

open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA hiding (id; _∘_)

open Partiality-algebra-with
open Partiality-algebra

-- Applies an increasing sequence of functions to a value.

at-with :
  ∀ {a b p q} {A : Type a} {T : A → Type p} {B : A → Type b}
  (P : (x : A) → Partiality-algebra-with (T x) q (B x)) →
  let module P x = Partiality-algebra-with (P x) in
  (∃ λ (f : ℕ → (x : A) → T x) →
     ∀ n x → P._⊑_ x (f n x) (f (suc n) x)) →
  (x : A) → ∃ λ (f : ℕ → T x) →
                ∀ n → P._⊑_ x (f n) (f (suc n))
at-with _ s x = Σ-map (λ f n → f n x) (λ f n → f n x) s

-- Applies an increasing sequence of functions to a value.

at :
  ∀ {a b p q} {A : Type a} {B : A → Type b}
  (P : (x : A) → Partiality-algebra p q (B x)) →
  let module P x = Partiality-algebra (P x) in
  (∃ λ (f : ℕ → (x : A) → P.T x) →
     ∀ n x → P._⊑_ x (f n x) (f (suc n) x)) →
  (x : A) → ∃ λ (f : ℕ → P.T x) →
                ∀ n → P._⊑_ x (f n) (f (suc n))
at P = at-with (partiality-algebra-with ∘ P)

-- A kind of dependent function space from types to
-- Partiality-algebra-with families.

Π-with : ∀ {a b p q}
         (A : Type a) {T : A → Type p} {B : A → Type b} →
         ((x : A) → Partiality-algebra-with (T x) q (B x)) →
         Partiality-algebra-with
           ((x : A) → T x) (a ⊔ q) ((x : A) → B x)
_⊑_               (Π-with A P) = λ f g → ∀ x → _⊑_ (P x) (f x) (g x)
never             (Π-with A P) = λ x → never (P x)
now               (Π-with A P) = λ f x → now (P x) (f x)
⨆                 (Π-with A P) = λ s x → ⨆ (P x) (at-with P s x)
antisymmetry      (Π-with A P) = λ p q → ⟨ext⟩ λ x →
                                   antisymmetry (P x) (p x) (q x)
T-is-set-unused   (Π-with A P) = Π-closure ext 2 λ x →
                                   T-is-set-unused (P x)
⊑-refl            (Π-with A P) = λ f x → ⊑-refl (P x) (f x)
⊑-trans           (Π-with A P) = λ f g x → ⊑-trans (P x) (f x) (g x)
never⊑            (Π-with A P) = λ f x → never⊑ (P x) (f x)
upper-bound       (Π-with A P) = λ s n x →
                                   upper-bound (P x) (at-with P s x) n
least-upper-bound (Π-with A P) = λ s ub is-ub x →
                                   least-upper-bound
                                     (P x) (at-with P s x) (ub x)
                                     (λ n → is-ub n x)
⊑-propositional   (Π-with A P) = Π-closure ext 1 λ x →
                                   ⊑-propositional (P x)

-- A kind of dependent function space from types to partiality algebra
-- families.

Π : ∀ {a b p q} →
    (A : Type a) {B : A → Type b} →
    ((x : A) → Partiality-algebra p q (B x)) →
    Partiality-algebra (a ⊔ p) (a ⊔ q) ((x : A) → B x)
T                       (Π A P) = (x : A) → T (P x)
partiality-algebra-with (Π A P) = Π-with A (partiality-algebra-with ∘ P)

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
-- {-# OPTIONS -v tc.with.strip:40 #-}
module Issue824 where

record R : Set where

data D : Set → Set₁ where
  d : ∀ {A} → D A → D A

postulate
  d′ : D R

data P : R → D R → Set₁ where
  p : {x : R} {y : D R} → P x y → P x (d y)

Foo : P _ (d d′) → Set₁
Foo (p _) with Set
Foo (p _) | _ = Set

-- Bug.agda:18,1-19,20
-- Inaccessible (dotted) patterns from the parent clause must also be
-- inaccessible in the with clause, when checking the pattern
-- {.Bug.recCon-NOT-PRINTED},
-- when checking that the clause
-- Foo (p _) with unit
-- Foo (p _) | _ = Set
-- has type P (record {}) (d d′) → Set₁

-- See also issue 635 and issue 665.

-- Andreas, 2013-03-21: should work now.


text:
------------------------------------------------------------------------
-- Call-by-value (CBV) reduction in pure type systems (PTS)
------------------------------------------------------------------------

module Pts.Reduction.Cbv where

open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Star using (map; gmap)
import Relation.Binary.EquivalenceClosure as EqClos
import Relation.Binary.PropositionalEquality as PropEq
open import Relation.Binary.Reduction

open import Pts.Syntax
open import Pts.Reduction.Full as Full hiding (reduction)

-- All remaining submodules are parametrized by a given set of sorts.
module _ {Sort : Set} where

  open Syntax       Sort
  open Substitution Sort using (_[_])

  ----------------------------------------------------------------------
  -- Call-by-value (CBV) reduction and equivalence relations

  -- Untyped values with up to n free variables.
  data Val {n} : Term n → Set where
    sort : ∀ s   → Val (sort s)  -- sort
    Π    : ∀ a b → Val (Π a b)   -- dependent product
    ƛ    : ∀ a b → Val (ƛ a b)   -- abstraction

  infixl 9  _·₁_ _·₂_
  infix  5  _→v_

  -- One-step CBV reduction.
  data _→v_ {n} : Term n → Term n → Set where
    cont : ∀ a b {c} (v : Val c)              → (ƛ a b) · c →v b [ c ]
    _·₁_ : ∀ {a₁ a₂} → a₁ →v a₂ → ∀ b         →      a₁ · b →v a₂ · b
    _·₂_ : ∀ {a b₁ b₂} (v : Val a) → b₁ →v b₂ →      a · b₁ →v a · b₂

  reduction : Reduction Term
  reduction = record { _→1_ = _→v_ }

  -- CBV reduction and equivalence.
  open Reduction reduction public renaming (_→*_ to _→v*_; _↔_ to _≡v_)

  ----------------------------------------------------------------------
  -- Substitutions in CBV reductions/equivalence
  --
  -- The applications _/→v_, _/→v*_ and _/≡v_ below may be considered
  -- substitution lemmas, i.e. they establish the commutativity of the
  -- respective reductions/equivalence with substitutions.

  -- Application of generic substitutions to the
  -- reductions/equivalence.
  record CbvSubstApp {T} (l : Lift T Term) : Set where
    open Lift l
    open SubstApp Sort l
    open PropEq hiding ([_])

    -- Substitutions commute.
    field /-sub-↑ : ∀ {m n} a b (σ : Sub T m n) →
                    a [ b ] / σ ≡ (a / σ ↑) [ b / σ ]

    infixl 8 _/Val_ _/→v_

    -- Application of substitutions preserves values.
    _/Val_ : ∀ {m n a} → Val a → (σ : Sub T m n) → Val (a / σ)
    sort s /Val σ = sort s
    Π a b  /Val σ = Π (a / σ) (b / σ ↑)
    ƛ a b  /Val σ = ƛ (a / σ) (b / σ ↑)

    -- Substitution commutes with one-step reduction.
    _/→v_ : ∀ {m n a b} → a →v b → (σ : Sub T m n) → a / σ →v b / σ
    cont a b c /→v σ =
      subst (_→v_ _) (sym (/-sub-↑ b _ σ)) (cont (a / σ) (b / σ ↑) (c /Val σ))
    a₁→a₂ ·₁ b /→v σ = (a₁→a₂ /→v σ) ·₁ (b / σ)
    a ·₂ b₁→b₂ /→v σ = (a /Val σ) ·₂ (b₁→b₂ /→v σ)

    redSubstApp : RedSubstApp reduction (record { _/_ = _/_ })
    redSubstApp = record { _/→1_ = _/→v_ }

    open RedSubstApp redSubstApp public
      hiding (_/→1_) renaming (_/→*_ to _/→v*_; _/↔_ to _/≡v_)

  -- Term substitutions in reductions/equivalences.
  module CbvSubstitution where
    open Substitution Sort
      using (termSubst; weaken; sub-commutes; varLiftSubLemmas)

    -- Application of renamings to reductions/equivalences.
    varSubstApp : CbvSubstApp (TermSubst.varLift termSubst)
    varSubstApp = record { /-sub-↑ = /-sub-↑ }
      where open LiftSubLemmas varLiftSubLemmas
    private module V = CbvSubstApp varSubstApp

    -- Weakening of one-step CBV reductions.
    weaken-→v : ∀ {n} {a b : Term n} → a →v b → weaken a →v weaken b
    weaken-→v a→b = a→b V./→v VarSubst.wk

    -- Weakening of CBV reductions.
    weaken-→v* : ∀ {n} {a b : Term n} → a →v* b → weaken a →v* weaken b
    weaken-→v* = gmap weaken weaken-→v

    -- Weakening of equivalences.
    weaken-≡v : ∀ {n} {a b : Term n} → a ≡v b → weaken a ≡v weaken b
    weaken-≡v = EqClos.gmap weaken weaken-→v

    -- Application of term substitutions to reductions/equivalences.
    termSubstApp : CbvSubstApp (TermSubst.termLift termSubst)
    termSubstApp = record { /-sub-↑ = λ a _ _ → sub-commutes a }
    open CbvSubstApp termSubstApp public

  ----------------------------------------------------------------------
  -- Properties of the CBV reductions/equivalence

  -- Inclusions.
  →v⇒→v* = →1⇒→* reduction
  →v*⇒≡v = →*⇒↔  reduction
  →v⇒≡v  = →1⇒↔  reduction

  -- CBV reduction is a preorder.
  →v*-predorder = →*-predorder reduction

  -- Preorder reasoning for CBV reduction.
  module →v*-Reasoning = →*-Reasoning reduction

  -- Terms together with CBV equivalence form a setoid.
  ≡v-setoid = ↔-setoid reduction

  -- Equational reasoning for CBV equivalence.
  module ≡v-Reasoning = ↔-Reasoning reduction

  ----------------------------------------------------------------------
  -- Relationships between CBV reduction and full β-reduction

  -- One-step CBV reduction implies one-step β-reduction.
  →v⇒→β : ∀ {n} {a b : Term n} → a →v b → a →β b
  →v⇒→β (cont a b c) = cont a b _
  →v⇒→β (a₁→a₂ ·₁ b) = →v⇒→β a₁→a₂ ·₁ b
  →v⇒→β (a ·₂ b₁→b₂) = _ ·₂ →v⇒→β b₁→b₂

  -- CBV reduction implies parallel reduction.
  →v*⇒→β* : ∀ {n} {a b : Term n} → a →v* b → a →β* b
  →v*⇒→β* = map →v⇒→β

  -- CBV equivalence implies parallel equivalence.
  ≡v⇒≡p : ∀ {n} {a b : Term n} → a ≡v b → a ≡β b
  ≡v⇒≡p = EqClos.map →v⇒→β

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
module LocalVsImportedModuleClash where

X = TODO--This-shouldn't-happen-if-the-scope-checker-does-it's-job


text:
{-# OPTIONS --without-K --safe #-}
module Categories.NaturalTransformation.NaturalIsomorphism.Equivalence where

-- a certain notion of equivalence between Natural Isomorphisms.

open import Level
open import Data.Product using (_×_; _,_; map; zip)
open import Relation.Binary using (IsEquivalence)

open import Categories.Category
open import Categories.Functor using (Functor)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (_≃_)
open import Categories.NaturalTransformation.Equivalence
open NaturalIsomorphism

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    C D : Category o ℓ e

infix 4 _≅_
_≅_ : ∀ {F G : Functor C D} → (α β : NaturalIsomorphism F G) → Set _
α ≅ β = F⇒G α ≃ F⇒G β × F⇐G α ≃ F⇐G β

≅-isEquivalence : ∀ {F G : Functor C D} → IsEquivalence (_≅_ {F = F} {G = G})
≅-isEquivalence {D = D} {F = F} {G = G} = record
  { refl  = H.refl , H.refl
  ; sym   =  map (λ z → H.sym z) (λ z → H.sym z) -- eta expansion needed
  ; trans = zip (λ a b → H.trans a b) λ a b → H.trans a b -- ditto
  }
  where module H = Category.HomReasoning D

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.DiffInt where

open import Cubical.HITs.SetQuotients
open import Cubical.Foundations.Prelude
open import Cubical.Data.Int.MoreInts.DiffInt renaming (ℤ to ℤType ; _+_ to _+ℤ_ ; _-_ to _-ℤ_)
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Semigroup.Base
open import Cubical.Algebra.Monoid.Base

open GroupStr

ℤ-isGroup : IsGroup {G = ℤType} ([ 0 , 0 ]) (_+ℤ_) (-ℤ_)
IsSemigroup.is-set (IsMonoid.isSemigroup (IsGroup.isMonoid ℤ-isGroup)) = ℤ-isSet
IsSemigroup.assoc (IsMonoid.isSemigroup (IsGroup.isMonoid ℤ-isGroup)) = +ℤ-assoc
IsMonoid.identity (IsGroup.isMonoid ℤ-isGroup) = λ x → (zero-identityʳ 0 x  , zero-identityˡ 0 x)
IsGroup.inverse ℤ-isGroup = λ x → (-ℤ-invʳ x , -ℤ-invˡ x)

ℤ : Group₀
fst ℤ = ℤType
1g (snd ℤ) = [ 0 , 0 ]
_·_ (snd ℤ) = _+ℤ_
inv (snd ℤ) = -ℤ_
isGroup (snd ℤ) = ℤ-isGroup


text:
open import Common.Size

postulate
  A : Set
  f : Size → A

-- k' < k < j <= i + 2 =/=> ∃ l < i
test : ∀ i (j : Size< (↑ ↑ ↑ i)) (k : Size< j) (k' : Size< k) → Size → Set → (((l : Size< i) → A) → A) → A
test i j k k' _ _ ret = ret λ l → f l


text:
module RTP where
  open import RTN public

{-
  data Bool : Set where
    False : Bool
    True : Bool
-}

  postulate
    Int    : Set
    String : Set
    Float  : Set
    Char   : Set

  {-# BUILTIN FLOAT Float #-}
  {-# BUILTIN STRING String #-}
  {-# BUILTIN CHAR Char #-}

  -- postulate primShowBool : Bool -> String
  postulate primShowInt : Int -> String
  postulate primShowChar : Char -> String

  postulate primStringAppend : String -> String -> String
  postulate primStringReverse : String -> String

  -- postulate primStringToList : String -> List Char
  -- postulate primStringFromList

-- Int stuff
  postulate primIntZero : Int
  postulate primIntOne : Int
  postulate primIntSucc : Int -> Int
  postulate primNatToInt : Nat -> Int
  postulate primIntToNat : Int -> Nat
  postulate primIntAdd : Int -> Int -> Int
  postulate primIntSub : Int -> Int -> Int
  postulate primIntMul : Int -> Int -> Int
  postulate primIntDiv : Int -> Int -> Int
  postulate primIntMod : Int -> Int -> Int

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_; Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
open import Relation.Binary using (Setoid)

-- A formalization of raw syntax

module Syntax where

  -- Syntactic classes

  data ObjectClass : Set where
    Ty Tm : ObjectClass

  data Class : Set where
    obj : ObjectClass → Class
    EqTy EqTm : Class

  -- Variable context shape

  infixl 6 _⊕_

  data VShape : Set where
    𝟘 : VShape
    𝟙 : VShape
    _⊕_ : VShape → VShape → VShape

  data var : VShape → Set where
    var-here : var 𝟙
    var-left : ∀ {γ δ} → var γ → var (γ ⊕ δ)
    var-right : ∀ {γ δ} → var δ → var (γ ⊕ δ)

  -- Metavariable context shapes

  infixl 9 _⊕ᵐᵛ_

  data MShape : Set where
    𝟘ᵐᵛ : MShape
    𝟙ᵐᵛ : ∀ (cl : Class) (γ : VShape) → MShape
    _⊕ᵐᵛ_ : MShape → MShape → MShape

  infix 8 [_,_]∈_

  data [_,_]∈_ : Class → VShape → MShape → Set where
    mv-here : ∀ cl γ → [ cl , γ ]∈ 𝟙ᵐᵛ cl γ
    mv-left : ∀ {𝕂 𝕄} cl γ → [ cl , γ ]∈ 𝕂 → [ cl , γ ]∈ 𝕂 ⊕ᵐᵛ 𝕄
    mv-right : ∀ {𝕂 𝕄} cl γ → [ cl , γ ]∈ 𝕄 → [ cl , γ ]∈ 𝕂 ⊕ᵐᵛ 𝕄

  -- Symbol signature

  record Signature : Set₁ where
    field
      symb : ObjectClass → Set -- a set of symbol names, one for each class
      symb-arg : ∀ {cl} → symb cl → MShape

  -- Expressions

  module Expression (𝕊 : Signature) where
    open Signature 𝕊

    data Expr : Class → (𝕄 : MShape) → (γ : VShape) → Set

    Arg : ∀ (cl : Class) (𝕄 : MShape) (γ : VShape) (δ : VShape) → Set
    Arg cl 𝕄 γ δ = Expr cl 𝕄 (γ ⊕ δ)

    ExprObj : ∀ (cl : ObjectClass) (𝕄 : MShape) (γ : VShape) → Set
    ExprObj cl = Expr (obj cl)

    ExprTm = ExprObj Tm
    ExprTy = ExprObj Ty

    data Expr where
      expr-var : ∀ {𝕄} {γ} (x : var γ) → ExprTm 𝕄 γ
      expr-symb : ∀ {cl 𝕄 γ} (S : symb cl) →
                    (es : ∀ {clⁱ γⁱ} (i : [ clⁱ , γⁱ ]∈ symb-arg S) → Arg clⁱ 𝕄 γ γⁱ) →
                    ExprObj cl 𝕄 γ
      expr-meta : ∀ {cl 𝕄 γ} {γᴹ} (M : [ obj cl , γᴹ ]∈ 𝕄) → (ts : ∀ (i : var γᴹ) → ExprTm 𝕄 γ) → ExprObj cl 𝕄 γ
      expr-eqty : ∀ {γ} {𝕄} → Expr EqTy 𝕄 γ
      expr-eqtm : ∀ {γ} {𝕄} → Expr EqTm 𝕄 γ

    expr-meta-generic : ∀ {𝕄} {cl} {γ γᴹ} (M : [ cl , γᴹ ]∈ 𝕄) → Arg cl 𝕄 γ γᴹ
    expr-meta-generic {cl = obj _} M = expr-meta M (λ i → expr-var (var-right i))
    expr-meta-generic {cl = EqTy} M = expr-eqty
    expr-meta-generic {cl = EqTm} M = expr-eqtm

  -- Syntactic equality

  module Equality {𝕊 : Signature} where

    open Signature 𝕊
    open Expression 𝕊

    infix 4 _≈_

    data _≈_ : ∀ {cl 𝕄 γ} → Expr cl 𝕄 γ → Expr cl 𝕄 γ → Set where
      ≈-≡ : ∀ {cl 𝕄 γ} {t u : Expr cl 𝕄 γ} (ξ : t ≡ u) → t ≈ u
      ≈-symb : ∀ {cl 𝕄 γ} {S : symb cl} →
                {ds es : ∀ {cⁱ γⁱ} (i : [ cⁱ , γⁱ ]∈ symb-arg S) → Arg cⁱ 𝕄 γ γⁱ}
                (ξ : ∀ {cⁱ γⁱ} (i : [ cⁱ , γⁱ ]∈ symb-arg S) → ds i ≈ es i) → expr-symb S ds ≈ expr-symb S es
      ≈-meta : ∀ {cl 𝕄 γ} {γᴹ} {M : [ obj cl , γᴹ ]∈ 𝕄} → {ts us : ∀ (i : var γᴹ) → ExprTm 𝕄 γ}
                (ξ : ∀ i → ts i ≈ us i) → expr-meta M ts ≈ expr-meta M us

    ≈-refl : ∀ {cl 𝕄 γ} {t : Expr cl 𝕄 γ} → t ≈ t
    ≈-refl = ≈-≡ refl

    ≈-eqty : ∀ {𝕄 γ} {s t : Expr EqTy 𝕄  γ} → s ≈ t
    ≈-eqty {s = expr-eqty} {t = expr-eqty} = ≈-refl

    ≈-eqtm : ∀ {𝕄 γ} {s t : Expr EqTm 𝕄 γ} → s ≈ t
    ≈-eqtm {s = expr-eqtm} {t = expr-eqtm} = ≈-refl

    ≈-sym : ∀ {cl 𝕄 γ} {t u : Expr cl 𝕄 γ} → t ≈ u → u ≈ t
    ≈-sym (≈-≡ refl) = ≈-≡ refl
    ≈-sym (≈-symb ε) = ≈-symb (λ i → ≈-sym (ε i))
    ≈-sym (≈-meta ε) = ≈-meta (λ i → ≈-sym (ε i))

    ≈-trans : ∀ {cl 𝕄 γ} {t u v : Expr cl 𝕄 γ} → t ≈ u → u ≈ v → t ≈ v
    ≈-trans (≈-≡ refl) ξ = ξ
    ≈-trans (≈-symb ζ) (≈-≡ refl) = ≈-symb ζ
    ≈-trans (≈-symb ζ) (≈-symb ξ) = ≈-symb (λ i → ≈-trans (ζ i) (ξ i))
    ≈-trans (≈-meta ζ) (≈-≡ refl) = ≈-meta ζ
    ≈-trans (≈-meta ζ) (≈-meta ξ) = ≈-meta (λ i → ≈-trans (ζ i) (ξ i))

    -- the setoid of expressions

    Expr-setoid : ∀ (cl : Class) (𝕄 : MShape) (γ : VShape) →  Setoid lzero lzero
    Expr-setoid cl 𝕄 γ =
      record
        { Carrier =  Expr cl 𝕄 γ
        ; _≈_ = _≈_
        ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans }
        }

  infix 4 _%_≈_

  _%_≈_ : ∀ (𝕊 : Signature) {cl 𝕄 γ} → (t u : Expression.Expr 𝕊 cl 𝕄 γ) → Set
  _%_≈_ 𝕊 = Equality._≈_ {𝕊 = 𝕊}


text:
-- 2011-10-01 Andreas
module EtaContractIrrelevant where

import Common.Level

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

subst : ∀ {a b}{A : Set a}(P : A → Set b){x y : A} → x ≡ y → P x → P y
subst P refl x = x

postulate
  Val : Set

Pred = Val → Set

fam : Pred → Set1
fam A = {a : Val} → .(A a) → Pred

postulate
  π : (A : Pred)(F : fam A) → Pred

πCong : {A A' : Pred}(A≡A' : A ≡ A') →
  {F  : fam A }
  {F' : fam A'}
  (F≡F' : (λ {a} Aa → F {a = a} Aa)
        ≡ (λ {a} Aa → F' {a = a} (subst (λ A → A a) A≡A' Aa))) →
  π A F ≡ π A' F'
πCong refl refl = refl
-- needs eta-contraction for irrelevant functions F F'

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- Termination
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Delay-monad.Termination {a} {A : Type a} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Double-negation equality-with-J
open import Monad equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity hiding (_∎; step-≡ˡ)

-- Termination predicates.

Terminates : Size → Delay A ∞ → A → Type a
Terminates i x y = [ i ] now y ≈ x

infix 4 _⇓_

_⇓_ : Delay A ∞ → A → Type a
_⇓_ = Terminates ∞

-- Terminates i is pointwise isomorphic to Terminates ∞.
--
-- Note that Terminates carves out an "inductive fragment" of [_]_≈_:
-- the only "coinductive" constructor, later, does not target
-- Terminates.

Terminates↔⇓ : ∀ {i x y} → Terminates i x y ↔ x ⇓ y
Terminates↔⇓ = record
  { surjection = record
    { logical-equivalence = record
      { to   = to
      ; from = from _
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = from∘to
  }
  where
  to : ∀ {i x y} → Terminates i x y → x ⇓ y
  to now        = now
  to (laterʳ p) = laterʳ (to p)

  from : ∀ i {x y} → x ⇓ y → Terminates i x y
  from _ now        = now
  from _ (laterʳ p) = laterʳ (from _ p)

  to∘from : ∀ {i x y} (p : x ⇓ y) → to (from i p) ≡ p
  to∘from now        = refl
  to∘from (laterʳ p) = cong laterʳ (to∘from p)

  from∘to : ∀ {i x y} (p : Terminates i x y) → from i (to p) ≡ p
  from∘to now        = refl
  from∘to (laterʳ p) = cong laterʳ (from∘to p)

-- The termination relation respects weak bisimilarity.
--
-- This function cannot be made size-preserving in its second argument
-- (unless A is uninhabited), see Delay-monad.Bisimilarity.Negative.

⇓-respects-≈ : ∀ {i x y z} →
               Terminates i x z → x ≈ y → Terminates i y z
⇓-respects-≈ = transitive-≈-now

-- If a computation does not terminate, then it is weakly bisimilar
-- to never.

¬⇓→⇑ : ∀ {i} x → ¬ (∃ λ y → x ⇓ y) → [ i ] never ≈ x
¬⇓→⇑ (now   x) ¬⇓ = ⊥-elim (¬⇓ (_ , now))
¬⇓→⇑ (later x) ¬⇓ = later λ { .force → ¬⇓→⇑ _ (¬⇓ ∘ Σ-map id laterʳ) }

-- In the double-negation monad every computation is weakly
-- bisimilar to either never or now something.

¬¬[⇑⊎⇓] : ∀ x → ¬¬ (never ≈ x ⊎ ∃ λ y → x ⇓ y)
¬¬[⇑⊎⇓] x = [ inj₂ , inj₁ ∘ ¬⇓→⇑ _ ] ⟨$⟩ excluded-middle

-- If A is a set, then the termination predicate is propositional.

Terminates-propositional :
  Is-set A → ∀ {i x y} → Is-proposition (Terminates i x y)
Terminates-propositional A-set {i} = λ p q → irr p q refl
  where
  irr :
    ∀ {x y y′}
    (p : [ i ] now y  ≈ x)
    (q : [ i ] now y′ ≈ x)
    (y≡y′ : y ≡ y′) →
    subst (([ i ]_≈ x) ∘ now) y≡y′ p ≡ q
  irr         (laterʳ p) (laterʳ q) refl = cong laterʳ (irr p q refl)
  irr {y = y} now        now        y≡y  =
    subst (([ i ]_≈ now y) ∘ now) y≡y  now  ≡⟨ cong (λ eq → subst (([ i ]_≈ now y) ∘ now) eq _) (A-set y≡y refl) ⟩
    subst (([ i ]_≈ now y) ∘ now) refl now  ≡⟨⟩
    now                                     ∎

-- If x terminates with y and z, then y is equal to z.

termination-value-unique :
  ∀ {i x y z} → Terminates i x y → Terminates i x z → y ≡ z
termination-value-unique now        now        = refl
termination-value-unique (laterʳ p) (laterʳ q) =
  termination-value-unique p q

-- If A is a set, then ∃ λ y → x ⇓ y is propositional.

∃-Terminates-propositional :
  Is-set A → ∀ {i x} → Is-proposition (∃ (Terminates i x))
∃-Terminates-propositional A-set (y₁ , x⇓y₁) (y₂ , x⇓y₂) =
  Σ-≡,≡→≡
    (termination-value-unique x⇓y₁ x⇓y₂)
    (Terminates-propositional A-set _ _)

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
-- Module shadowing using generated modules for records and datatypes
module Issue260a where

module D where
data D : Set where


text:
interleaved mutual

  data Nat : Set
  record IsNat (n : Nat) : Set
  isNat : (n : Nat) → IsNat n

max_stars_repo_name: cruhland/agda


text:
module string-thms where

open import bool
open import eq
open import string

postulate
  =string-refl : (s : string) → s =string s ≡ tt
  =string-to-≡ : (a b : string) → a =string b ≡ tt → a ≡ b

≡string-to-= : (a b : string) → a ≡ b → a =string b ≡ tt
≡string-to-= a .a refl = =string-refl a

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --without-K #-}
module hott.truncation.core where

open import sum
open import equality
open import function.core
open import function.fibration
open import function.extensionality
open import function.isomorphism
open import sets.nat.core
open import hott.equivalence
open import hott.level.core
open import hott.level.closure

module _ {i j i' j'}{A : Set i}{A' : Set i'}
         {B : A → Set j}{B' : A' → Set j'}
         (f : A → A')
         (g : (a : A) → B a → B' (f a)) where
  private
    E E' : Set _
    E = Σ A B
    E' = Σ A' B'

    p : E → A
    p = proj₁

    p' : E' → A'
    p' = proj₁

    t : E → E'
    t (a , b) = (f a , g a b)

  module _ (f-equiv : weak-equiv f)
           (t-equiv : weak-equiv t) where

    private
      φ : A ≅ A'
      φ = ≈⇒≅ (f , f-equiv)

      τ : E ≅ E'
      τ = ≈⇒≅ (t , t-equiv)

      lem : (a : A)(e : E) → (p e ≡ a) ≅ (p' (t e) ≡ f a)
      lem a e = iso≡ φ

    fib-equiv : (a : A) → B a ≅ B' (f a)
    fib-equiv a = sym≅ (fib-iso a) ·≅ Σ-ap-iso τ (lem a) ·≅ fib-iso (f a)

postulate
  Trunc : ∀ {i} → ℕ → Set i → Set i
  Trunc-level : ∀ {i} n {X : Set i} → h n (Trunc n X)
  [_] : ∀ {i n} {X : Set i} → X → Trunc n X

Trunc-ext : ∀ {i j} n (X : Set i)(Y : Set j)
          → (Trunc n X → Y) → X → Y
Trunc-ext n X Y f x = f [ x ]

postulate
  Trunc-univ : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
             → weak-equiv (Trunc-ext n X Y)

Trunc-elim-iso : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
               → (Trunc n X → Y) ≅ (X → Y)
Trunc-elim-iso n X Y hY = ≈⇒≅ (Trunc-ext n X Y , Trunc-univ n X Y hY)

Trunc-elim : ∀ {i j} n (X : Set i)(Y : Set j) → h n Y
           → (X → Y) → (Trunc n X → Y)
Trunc-elim n X Y hY = invert (Trunc-elim-iso n X Y hY)

Trunc-elim-β : ∀ {i j} n (X : Set i)(Y : Set j)(hY : h n Y)
             → (f : X → Y)(x : X)
             → Trunc-elim n X Y hY f [ x ] ≡ f x
Trunc-elim-β n X Y hY f x = funext-inv (_≅_.iso₂ (Trunc-elim-iso n X Y hY) f) x

module _ {i j} n {X : Set i} (Y : Trunc n X → Set j)
         (hY : (x : Trunc n X) → h n (Y x)) where

  private
    Z : Set _
    Z = Σ (Trunc n X) Y

    hZ : h n Z
    hZ = Σ-level (Trunc-level n) hY

    Sec₂ : ∀ {k}{A : Set k} → (A → Trunc n X) → Set _
    Sec₂ {A = A} r = (x : A) → Y (r x)

    Sec : ∀ {k} → Set k → Set _
    Sec A = Σ (A → Trunc n X) Sec₂

    τ : Sec (Trunc n X) ≅ Sec X
    τ = sym≅ ΠΣ-swap-iso ·≅ Trunc-elim-iso n X Z hZ ·≅ ΠΣ-swap-iso

    ψ : (r : Trunc n X → Trunc n X)
      → (Sec₂ r) ≅ Sec₂ (r ∘ [_])
    ψ = fib-equiv {A = Trunc n X → Trunc n X}{A' = X → Trunc n X}{B = Sec₂} {B' = Sec₂}
        (Trunc-ext n X (Trunc n X)) (λ r g x → g [ x ])
        (Trunc-univ n X (Trunc n X) (Trunc-level n))
        (proj₂ (≅⇒≈ τ))

  Trunc-dep-iso : Sec₂ (λ x → x) ≅ Sec₂ [_]
  Trunc-dep-iso = ψ (λ x → x)

  Trunc-dep-elim : ((x : X) → Y [ x ]) → (x : Trunc n X) → Y x
  Trunc-dep-elim = invert Trunc-dep-iso

  Trunc-dep-elim-β : (d : ((x : X) → Y [ x ]))
                   → (x : X) → Trunc-dep-elim d [ x ] ≡ d x
  Trunc-dep-elim-β d = funext-inv (_≅_.iso₂ Trunc-dep-iso d)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module Human.Humanity where

-- Use agda-prelude instead of agda-stdlib?

open import Human.JS public
open import Human.Unit public
open import Human.Nat public
open import Human.List public
open import Human.Bool public
open import Human.String public
open import Human.IO public
open import Human.Float public
open import Human.Int public

Lazy : ∀ (A : Set) → Set
Lazy A = Unit → A

then:_ : ∀ {A : Set} → A → Lazy A
then: a = λ x → a

else:_ : ∀ {A : Set} → A → Lazy A
else: a = λ x → a

if : ∀ {A : Set} → Bool → Lazy A → Lazy A → A
if true  t f = t unit
if false t f = f unit

init-to : ∀ {A : Set} → Nat → A → (Nat → A → A) → A
init-to zero    x fn = x
init-to (suc i) x fn = init-to i (fn zero x) (λ i → fn (suc i))

{-# COMPILE JS init-to = A => n => x => fn => { for (var i = 0, l = n.toJSValue(); i < l; ++i) x = fn(agdaRTS.primIntegerFromString(String(i)))(x); return x; } #-}

syntax init-to m x (λ i → b) = init x for i to m do: b

init-from-to : ∀ {A : Set} → Nat → A → Nat → (Nat → A → A) → A
init-from-to n x m f = init-to (m - n) x (λ i x → f (n + i) x)

syntax init-from-to n x m (λ i → b) = init x for i from n to m do: b

for-to : Nat → (Nat → IO Unit) → IO Unit
for-to zero    act = return unit
for-to (suc n) act = act zero >> for-to n (λ i → act (suc i))

syntax for-from-to n m (λ i → b) = for i from n to m do: b

for-from-to : Nat → Nat → (Nat → IO Unit) → IO Unit
for-from-to n m f = for-to (m - n) (λ i → f (n + i))

syntax for-to m (λ i → b) = for i to m do: b

_++_ : String → String → String
_++_ = primStringAppend

show : Nat → String
show zero    = "Z"
show (suc n) = "S" ++ show n

Program : Set
Program = Lazy (IO Unit)

_f+_ : Float → Float → Float
_f+_ = primFloatPlus

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Interleavings of lists using setoid equality
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid)

module Data.List.Relation.Ternary.Interleaving.Setoid {c ℓ} (S : Setoid c ℓ) where

open import Level using (_⊔_)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Ternary.Interleaving.Properties
import Data.List.Relation.Ternary.Interleaving as General
open Setoid S renaming (Carrier to A)

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

Interleaving : List A → List A → List A → Set (c ⊔ ℓ)
Interleaving = General.Interleaving _≈_ _≈_

------------------------------------------------------------------------
-- Re-export the basic combinators

open General hiding (Interleaving) public


text:
-- Andreas, 2015-12-29

record ⊤ : Set where

data P : ⊤ → Set where
  c : P record{}

test : (x : ⊤) (p : P x) → Set
test _ c with ⊤
test _ y | z = ⊤

-- Expected error: with-clause pattern mismatch.
-- The error should be printed nicely, like:
--
-- With clause pattern x is not an instance of its parent pattern
-- record {}
-- when checking that the clause
-- test c with Set
-- test x y | z = ⊤
-- has type (x : ⊤) → P x → Set


text:
{-

Product of structures S and T: X ↦ S X × T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Product where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level

ProductStructure : (S₁ : Type ℓ → Type ℓ₁) (S₂ : Type ℓ → Type ℓ₂)
  → Type ℓ → Type (ℓ-max ℓ₁ ℓ₂)
ProductStructure S₁ S₂ X = S₁ X × S₂ X

ProductEquivStr :
  {S₁ : Type ℓ → Type ℓ₁} (ι₁ : StrEquiv S₁ ℓ₁')
  {S₂ : Type ℓ → Type ℓ₂} (ι₂ : StrEquiv S₂ ℓ₂')
  → StrEquiv (ProductStructure S₁ S₂) (ℓ-max ℓ₁' ℓ₂')
ProductEquivStr ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) f =
  (ι₁ (X , s₁) (Y , t₁) f) × (ι₂ (X , s₂) (Y , t₂) f)

productUnivalentStr :
  {S₁ : Type ℓ → Type ℓ₁} (ι₁ : StrEquiv S₁ ℓ₁') (θ₁ : UnivalentStr S₁ ι₁)
  {S₂ : Type ℓ → Type ℓ₂} (ι₂ : StrEquiv S₂ ℓ₂') (θ₂ : UnivalentStr S₂ ι₂)
  → UnivalentStr (ProductStructure S₁ S₂) (ProductEquivStr ι₁ ι₂)
productUnivalentStr {S₁ = S₁} ι₁ θ₁ {S₂} ι₂ θ₂ {X , s₁ , s₂} {Y , t₁ , t₂} e =
  compEquiv (Σ-cong-equiv (θ₁ e) (λ _ → θ₂ e)) ΣPath≃PathΣ

productEquivAction :
  {S₁ : Type ℓ → Type ℓ₁} (α₁ : EquivAction S₁)
  {S₂ : Type ℓ → Type ℓ₂} (α₂ : EquivAction S₂)
  → EquivAction (ProductStructure S₁ S₂)
productEquivAction α₁ α₂ e = Σ-cong-equiv (α₁ e) (λ _ → α₂ e)

productTransportStr :
  {S₁ : Type ℓ → Type ℓ₁} (α₁ : EquivAction S₁) (τ₁ : TransportStr α₁)
  {S₂ : Type ℓ → Type ℓ₂} (α₂ : EquivAction S₂) (τ₂ : TransportStr α₂)
  → TransportStr (productEquivAction α₁ α₂)
productTransportStr _ τ₁ _ τ₂ e (s₁ , s₂) = ΣPathP (τ₁ e s₁ , τ₂ e s₂)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical