text:
module cedille-find where

open import lib

open import cedille-types

occurrence-tuple = var × posinfo × string
occurrences-table = trie (𝕃 occurrence-tuple)

--------------------------
-- helper functions
--------------------------

occurrence-tuple-to-JSON : occurrence-tuple → string
occurrence-tuple-to-JSON (str , pos-info , filename) = "{\"defn\":\"" ^ str ^ "\",\"pos-info\":" ^ pos-info ^ ",\"filename\":\"" ^ filename ^ "\"}"

find-symbols-to-JSON-h : 𝕃 occurrence-tuple → string
find-symbols-to-JSON-h [] = ""
find-symbols-to-JSON-h (x :: []) = (occurrence-tuple-to-JSON x)
find-symbols-to-JSON-h (x :: xs) = (occurrence-tuple-to-JSON x) ^ "," ^ find-symbols-to-JSON-h xs

find-symbols-to-JSON : var → 𝕃 occurrence-tuple → string
find-symbols-to-JSON symb l = "{\"find\":{\"symbol\":\"" ^ symb ^ "\",\"occurrences\":[" ^ (find-symbols-to-JSON-h l) ^ "]}}"

-- updates the value list in the symbol map provided that the key symbol is not being shadowed
trie-append-or-create : occurrences-table → stringset → var → var → string → posinfo → occurrences-table
trie-append-or-create symb-map shadow key defn pos-info filename with (stringset-contains shadow key)
...                                                    | tt = symb-map
...                                                    | ff with (trie-lookup symb-map key)
...                                                         | nothing = trie-insert symb-map key ((defn , pos-info , filename) :: [])
...                                                         | just list = trie-insert symb-map key ((defn , pos-info , filename) :: list)

--------------------------
-- find declarations
--------------------------
find-symbols-cmd : cmd → string → occurrences-table → stringset → occurrences-table

find-symbols-t : Set → Set
find-symbols-t X = X → var → string → occurrences-table → stringset → occurrences-table

find-symbols-checkKind : find-symbols-t checkKind
find-symbols-kind : find-symbols-t kind
find-symbols-liftingType : find-symbols-t liftingType
find-symbols-lterms : find-symbols-t lterms
find-symbols-maybeCheckType : find-symbols-t maybeCheckType
find-symbols-optType : find-symbols-t optType
find-symbols-term : find-symbols-t term
find-symbols-optTerm : find-symbols-t optTerm
find-symbols-tk : find-symbols-t tk
find-symbols-type : find-symbols-t type

--------------------------
-- definitions
--------------------------
find-symbols-checkKind (Kind k) defn filename symb-map shadow = find-symbols-kind k defn filename symb-map shadow

find-symbols-cmd (DefKind _ kvar _ k _) filename symb-map shadow = find-symbols-kind k kvar filename symb-map shadow
find-symbols-cmd (DefTerm _ var mcT t _ _) filename symb-map shadow = find-symbols-maybeCheckType mcT var filename (find-symbols-term t var filename symb-map shadow) shadow
find-symbols-cmd (DefType _ var cK T _ _) filename symb-map shadow = find-symbols-checkKind cK var filename (find-symbols-type T var filename symb-map shadow) shadow
find-symbols-cmd _ _ symb-map _ = symb-map

find-symbols-kind (KndArrow k1 k2) defn filename symb-map shadow = find-symbols-kind k1 defn filename (find-symbols-kind k2 defn filename symb-map shadow) shadow
find-symbols-kind (KndParens _ k _) defn filename symb-map shadow = find-symbols-kind k defn filename symb-map shadow
find-symbols-kind (KndPi _ _ var tk k) defn filename symb-map shadow = find-symbols-tk tk defn filename (find-symbols-kind k defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-kind (KndTpArrow T k) defn filename symb-map shadow = find-symbols-type T defn filename (find-symbols-kind k defn filename symb-map shadow) shadow
find-symbols-kind (KndVar pos-info kvar) defn filename symb-map shadow = trie-append-or-create symb-map shadow kvar defn pos-info filename
find-symbols-kind _ _ _ symb-map _ = symb-map

find-symbols-liftingType (LiftArrow lT1 lT2) defn filename symb-map shadow = find-symbols-liftingType lT1 defn filename (find-symbols-liftingType lT2 defn filename symb-map shadow) shadow
find-symbols-liftingType (LiftParens _ lT _) defn filename symb-map shadow = find-symbols-liftingType lT defn filename symb-map shadow
find-symbols-liftingType (LiftPi _ var T lT) defn filename symb-map shadow = find-symbols-type T defn filename (find-symbols-liftingType lT defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-liftingType (LiftTpArrow T lT) defn filename symb-map shadow = find-symbols-type T defn filename (find-symbols-liftingType lT defn filename symb-map shadow) shadow
find-symbols-liftingType _ _ _ symb-map _ = symb-map

find-symbols-lterms (LtermsCons _ t lt) defn filename symb-map shadow = find-symbols-term t defn filename (find-symbols-lterms lt defn filename symb-map shadow) shadow
find-symbols-lterms _ _ _ symb-map _ = symb-map

find-symbols-maybeCheckType (Type T) defn filename symb-map shadow = find-symbols-type T defn filename symb-map shadow
find-symbols-maybeCheckType _ _ _ symb-map _ = symb-map

find-symbols-optType (SomeType T) defn filename symb-map shadow = find-symbols-type T defn filename symb-map shadow
find-symbols-optType _ _ _ symb-map _ = symb-map

find-symbols-optTerm (SomeTerm t _) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-optTerm _ _ _ symb-map _ = symb-map

find-symbols-term (App t1 _ t2) defn filename symb-map shadow = find-symbols-term t1 defn filename (find-symbols-term t2 defn filename symb-map shadow) shadow
find-symbols-term (AppTp t T) defn filename symb-map shadow = find-symbols-term t defn filename (find-symbols-type T defn filename symb-map shadow) shadow
find-symbols-term (Chi _ _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Delta _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Epsilon _ _ _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
--find-symbols-term (Fold _ _ T t) defn filename symb-map shadow = find-symbols-type T defn filename (find-symbols-term t defn filename symb-map shadow) shadow
-- treated as a new top global def
find-symbols-term (InlineDef _ _ var t _) defn filename symb-map shadow = find-symbols-term t var filename symb-map shadow
find-symbols-term (IotaPair _ t1 t2 ot _) defn filename symb-map shadow = find-symbols-term t1 defn filename (find-symbols-term t2 defn filename (find-symbols-optTerm ot defn filename symb-map shadow) shadow) shadow
find-symbols-term (IotaProj t _ _) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Lam _ _ _ var _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map (stringset-insert shadow var)
find-symbols-term (Parens _ t _) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (PiInj _ _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Rho _ _ t1 t2) defn filename symb-map shadow = find-symbols-term t1 defn filename (find-symbols-term t2 defn filename symb-map shadow) shadow
find-symbols-term (Sigma _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Theta _ _ t lt) defn filename symb-map shadow = find-symbols-term t defn filename (find-symbols-lterms lt defn filename symb-map shadow) shadow
find-symbols-term (Unfold _ t) defn filename symb-map shadow = find-symbols-term t defn filename symb-map shadow
find-symbols-term (Var pos-info var) defn filename symb-map shadow = trie-append-or-create symb-map shadow var defn pos-info filename
find-symbols-term _ _ _ symb-map _ = symb-map

find-symbols-tk (Tkk k) defn filename symb-map shadow = find-symbols-kind k defn filename symb-map shadow
find-symbols-tk (Tkt T) defn filename symb-map shadow = find-symbols-type T defn filename symb-map shadow

find-symbols-type (Abs _ _ _ var tk T) defn filename symb-map shadow = find-symbols-tk tk defn filename (find-symbols-type T defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-type (Iota _ _ var oT T) defn filename symb-map shadow = find-symbols-optType oT defn filename (find-symbols-type T defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-type (Lft _ _ var t lT) defn filename symb-map shadow = find-symbols-term t defn filename (find-symbols-liftingType lT defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-type (Mu _ _ var k T) defn filename symb-map shadow = find-symbols-kind k defn filename (find-symbols-type T defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-type (NoSpans T _) defn filename symb-map shadow = find-symbols-type T defn filename symb-map shadow
find-symbols-type (TpApp T1 T2) defn filename symb-map shadow = find-symbols-type T1 defn filename (find-symbols-type T2 defn filename symb-map shadow) shadow
find-symbols-type (TpAppt T t) defn filename symb-map shadow = find-symbols-type T defn filename (find-symbols-term t defn filename symb-map shadow) shadow
find-symbols-type (TpArrow T1 _ T2) defn filename symb-map shadow = find-symbols-type T1 defn filename (find-symbols-type T2 defn filename symb-map shadow) shadow
find-symbols-type (TpEq t1 t2) defn filename symb-map shadow = find-symbols-term t1 defn filename (find-symbols-term t2 defn filename symb-map shadow) shadow
find-symbols-type (TpLambda _ _ var tk T) defn filename symb-map shadow = find-symbols-tk tk defn filename (find-symbols-type T defn filename symb-map (stringset-insert shadow var)) shadow
find-symbols-type (TpParens _ T _) defn filename symb-map shadow = find-symbols-type T defn filename symb-map shadow
find-symbols-type (TpVar pos-info var) defn filename symb-map shadow = trie-append-or-create symb-map shadow var defn pos-info filename
find-symbols-type (TpHole pos-info) defn filename symb-map shadow = trie-append-or-create symb-map shadow "hole" defn pos-info filename
--ACG: Not sure this works

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
module list-thms2 where

open import bool
open import bool-thms
open import bool-thms2
open import functions
open import list
open import list-thms
open import nat
open import nat-thms
open import product-thms
open import logic

list-and-++ : ∀(l1 l2 : 𝕃 𝔹) → list-and (l1 ++ l2) ≡ (list-and l1) && (list-and l2)
list-and-++ [] l2 = refl
list-and-++ (x :: l1) l2 rewrite (list-and-++ l1 l2) | (&&-assoc x (list-and l1) (list-and l2))= refl

list-or-++ : ∀(l1 l2 : 𝕃 𝔹) → list-or (l1 ++ l2) ≡ (list-or l1) || (list-or l2)
list-or-++ [] l2 = refl
list-or-++ (x :: l1) l2 rewrite (list-or-++ l1 l2) | (||-assoc x (list-or l1) (list-or l2))  = refl

++-singleton : ∀{ℓ}{A : Set ℓ}(a : A)(l1 l2 : 𝕃 A) → (l1 ++ [ a ]) ++ l2 ≡ l1 ++ (a :: l2)
++-singleton a l1 [] rewrite ++[] (l1 ++ a :: []) = refl
++-singleton a l1 l2  rewrite (++-assoc l1 [ a ] l2) = refl

list-member-++ : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l1 l2 : 𝕃 A) →
                 list-member eq a (l1 ++ l2) ≡ (list-member eq a l1) || (list-member eq a l2)
list-member-++ eq a [] l2 = refl
list-member-++ eq a (x :: l1) l2 with eq a x
list-member-++ eq a (x :: l1) l2 | tt = refl
list-member-++ eq a (x :: l1) l2 | ff rewrite (list-member-++ eq a l1 l2) = refl

list-member-++2 : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l1 l2 : 𝕃 A) →
                   list-member eq a l1 ≡ tt →
                   list-member eq a (l1 ++ l2) ≡ tt
list-member-++2 eq a [] l2 ()
list-member-++2 eq a (x :: l1) l2 p with eq a x
list-member-++2 eq a (x :: l1) l2 p | tt = refl
list-member-++2 eq a (x :: l1) l2 p | ff rewrite (list-member-++2 eq a l1 l2 p) = refl

list-member-++3 : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l1 l2 : 𝕃 A) →
                   list-member eq a l2 ≡ tt →
                   list-member eq a (l1 ++ l2) ≡ tt
list-member-++3 eq a [] l2 p = p
list-member-++3 eq a (x :: l1) l2 p with eq a x
list-member-++3 eq a (x :: l1) l2 p | tt = refl
list-member-++3 eq a (x :: l1) l2 p | ff rewrite (list-member-++3 eq a l1 l2 p) = refl

filter-ff-repeat : ∀{ℓ}{A : Set ℓ}{p : A → 𝔹}{a : A}(n : ℕ) →
                     p a ≡ ff →
                     filter p (repeat n a) ≡ []
filter-ff-repeat zero p1 = refl
filter-ff-repeat{ℓ}{A}{p0}{a} (suc n) p1 with keep (p0 a)
filter-ff-repeat{ℓ}{A}{p0}{a} (suc n) p1 | tt , y rewrite y = 𝔹-contra (sym p1)
filter-ff-repeat{ℓ}{A}{p0}{a} (suc n) p1 | ff , y rewrite y = filter-ff-repeat {ℓ} {A} {p0} {a} n y

is-empty-distr : ∀{ℓ}{A : Set ℓ} (l1 l2 : 𝕃 A) → is-empty (l1 ++ l2) ≡ (is-empty l1) && (is-empty l2)
is-empty-distr [] l2 = refl
is-empty-distr (x :: l1) l2 = refl

is-empty-reverse : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → is-empty l ≡ is-empty (reverse l)
is-empty-reverse [] = refl
is-empty-reverse (x :: xs) rewrite (reverse-++h (x :: []) xs) | (is-empty-distr (reverse-helper [] xs) (x :: []))
                                 | (&&-comm (is-empty (reverse-helper [] xs)) ff) = refl

reverse-length : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → length (reverse l) ≡ length l
reverse-length l = length-reverse-helper [] l

last-distr : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A)(x : A)(p : is-empty l ≡ ff) → last (x :: l) refl ≡ last l p
last-distr [] x ()
last-distr (x :: l) x2 refl = refl

is-empty-[] : ∀{ℓ}{A : Set ℓ} (l : 𝕃 A)(p : is-empty l ≡ tt) → l ≡ []
is-empty-[] [] p = refl
is-empty-[] (x :: l) ()

rev-help-empty : ∀ {ℓ}{A : Set ℓ} (l1 l2 : 𝕃 A) → (p1 : is-empty l2 ≡ ff) →
                      is-empty (reverse-helper l1 l2) ≡ ff
rev-help-empty l1 [] ()
rev-help-empty l1 (x :: l2) p rewrite reverse-++h (x :: l1) l2 | is-empty-distr (reverse-helper [] l2) (x :: l1)
                                    | (&&-comm (is-empty (reverse-helper [] l2)) ff) = refl

is-empty-revh : ∀{ℓ}{A : Set ℓ}(h l : 𝕃 A) → is-empty l ≡ ff → is-empty (reverse-helper h l) ≡ ff
is-empty-revh h l p = rev-help-empty h l p

head-last-reverse-lem : ∀{ℓ}{A : Set ℓ}(h l : 𝕃 A)(p : is-empty l ≡ ff) → last l p ≡ head (reverse-helper h l) (is-empty-revh h l p)
head-last-reverse-lem h [] ()
head-last-reverse-lem h (x :: []) p = refl
head-last-reverse-lem h (x :: y :: l) p = head-last-reverse-lem (x :: h) (y :: l) refl

head-last-reverse : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A)(p : is-empty l ≡ ff) → last l p ≡ head (reverse l) (rev-help-empty [] l p)
head-last-reverse [] ()
head-last-reverse (x :: l) p with keep (is-empty l)
head-last-reverse (x :: l) refl | tt , b rewrite is-empty-[] l b = refl
head-last-reverse (x :: l) refl | ff , b rewrite (last-distr l x b)  = head-last-reverse-lem (x :: []) l b

reverse-reverse : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → reverse (reverse l) ≡ l
reverse-reverse [] = refl
reverse-reverse (x :: l) rewrite (reverse-++h (x :: []) l) | (reverse-++ (reverse-helper [] l) (x  :: [])) | reverse-reverse l = refl

empty++elem : ∀ {ℓ}{A : Set ℓ} (a : A) (l : 𝕃 A) → is-empty ( l ++ [ a ]) ≡ ff
empty++elem a [] = refl
empty++elem a (x :: l) = refl

last-++ : ∀{ℓ}{A : Set ℓ} (a : A) (l : 𝕃 A) → last (l ++ [ a ]) (empty++elem a l) ≡ a
last-++ a [] = refl
last-++ a (x :: l) rewrite last-distr (l ++ [ a ]) x (empty++elem a l) | last-++ a l = refl

ext: agda

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Semantics.Bind where

open import Syntax.Types
open import Syntax.Context renaming (_,_ to _,,_)
open import Syntax.Terms
open import Syntax.Substitution.Kits
open import Syntax.Substitution.Instances
open import Syntax.Substitution.Lemmas

open import Semantics.Types
open import Semantics.Terms
open import Semantics.Context
open import Semantics.Substitution.Kits
open import Semantics.Substitution.Traversal
open import Semantics.Substitution.Instances

open import CategoryTheory.Categories using (Category ; ext)
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import CategoryTheory.Comonad
open import CategoryTheory.CartesianStrength
open import CategoryTheory.Instances.Reactive renaming (top to ⊤)
open import TemporalOps.Diamond
open import TemporalOps.Delay
open import TemporalOps.Box
open import TemporalOps.OtherOps
open import TemporalOps.StrongMonad

open import Data.Sum
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl ; sym ; trans ; cong ; cong₂ ; subst)

open ≡.≡-Reasoning
open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

open Comonad W-□
open Monad M-◇
private module F-◇ = Functor F-◇
private module F-□ = Functor F-□
open Functor F-□ renaming (fmap to □-f)
open Functor F-◇ renaming (fmap to ◇-f)
private module ▹ᵏ-C k = CartesianFunctor (F-cart-delay k)
private module ▹ᵏ-F k = Functor (F-delay k)
private module □-▹ᵏ k = _⟹_ (□-to-▹ᵏ k)

bind-to->>= : ∀ Γ {⟦A⟧ ⟦B⟧} -> (⟦E⟧ : ⟦ Γ ⟧ₓ ⇴ ◇ ⟦A⟧) (⟦C⟧ : ⟦ Γ ˢ ⟧ₓ ⊗ ⟦A⟧ ⇴ ◇ ⟦B⟧)
        -> (n : ℕ) (⟦Γ⟧ : ⟦ Γ ⟧ₓ n)
        -> bindEvent Γ ⟦E⟧ ⟦C⟧ n ⟦Γ⟧
        ≡ (⟦E⟧ n ⟦Γ⟧ >>= λ l ⟦A⟧ → ⟦C⟧ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧))
bind-to->>= Γ {⟦A⟧} {⟦B⟧} ⟦E⟧ ⟦C⟧ n ⟦Γ⟧ =
    begin
        bindEvent Γ ⟦E⟧ ⟦C⟧ n ⟦Γ⟧
    ≡⟨⟩
        μ.at ⟦B⟧ n (F-◇.fmap (⟦C⟧ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n (st ⟦ Γ ˢ ⟧ₓ ⟦A⟧ n (⟦ Γ ˢ⟧□ n ⟦Γ⟧ , ⟦E⟧ n ⟦Γ⟧)))
    ≡⟨ cong (μ.at ⟦B⟧ n) (lemma (⟦E⟧ n ⟦Γ⟧)) ⟩
        μ.at ⟦B⟧ n (F-◇.fmap (⟦C⟧ ∘ ⟨ (λ l _ → ⟦ Γ ˢ⟧□ n ⟦Γ⟧ l) , id ⟩) n (⟦E⟧ n ⟦Γ⟧))
    ≡⟨⟩
        (⟦E⟧ n ⟦Γ⟧ >>= (λ l ⟦A⟧ → ⟦C⟧ l (⟦ Γ ˢ⟧□ n ⟦Γ⟧ l , ⟦A⟧)))
    ∎
    where
    lemma : ∀ ◇⟦A⟧
         -> F-◇.fmap (⟦C⟧ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n (st ⟦ Γ ˢ ⟧ₓ ⟦A⟧ n (⟦ Γ ˢ⟧□ n ⟦Γ⟧ , ◇⟦A⟧))
          ≡ F-◇.fmap (⟦C⟧ ∘ ⟨ (λ l _ → ⟦ Γ ˢ⟧□ n ⟦Γ⟧ l) , id ⟩) n ◇⟦A⟧
    lemma (k , a) =
        begin
            F-◇.fmap (⟦C⟧ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n (st ⟦ Γ ˢ ⟧ₓ ⟦A⟧ n (⟦ Γ ˢ⟧□ n ⟦Γ⟧ , (k , a)))
        ≡⟨⟩
            k , ▹ᵏ-F.fmap k (⟦C⟧ ∘ ε.at ⟦ Γ ˢ ⟧ₓ * id) n
                (▹ᵏ-C.m k (□ ⟦ Γ ˢ ⟧ₓ) ⟦A⟧ n (□-▹ᵏ.at k (□ ⟦ Γ ˢ ⟧ₓ) n (δ.at ⟦ Γ ˢ ⟧ₓ k (⟦ Γ ˢ⟧□ n ⟦Γ⟧)) , a))
        ≡⟨ {!   !} ⟩
            k , ▹ᵏ-F.fmap k (⟦C⟧ ∘ ⟨ (λ l _ → ⟦ Γ ˢ⟧□ n ⟦Γ⟧ l) , id ⟩) n a
        ≡⟨⟩
            F-◇.fmap (⟦C⟧ ∘ ⟨ (λ l _ → ⟦ Γ ˢ⟧□ n ⟦Γ⟧ l) , id ⟩) n (k , a)
        ∎

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Prelude where

infix 20 _≡_ _≤_ _∈_
infixl 60 _,_ _++_ _+_ _◄_ _◄²_

_∘_ : {A B : Set}{C : B -> Set}(f : (x : B) -> C x)(g : A -> B)(x : A) -> C (g x)
(f ∘ g) x = f (g x)

data _≡_ {A : Set}(x : A) : {B : Set} -> B -> Set where
  refl : x ≡ x

cong : {A : Set}{B : A -> Set}(f : (z : A) -> B z){x y : A} ->
       x ≡ y -> f x ≡ f y
cong f refl = refl

subst : {A : Set}(P : A -> Set){x y : A} -> x ≡ y -> P y -> P x
subst P refl px = px

sym : {A : Set}{x y : A} -> x ≡ y -> y ≡ x
sym refl = refl

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

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN NATPLUS _+_  #-}

data _≤_ : Nat -> Nat -> Set where
  leqZ : {m : Nat}   -> zero ≤ m
  leqS : {n m : Nat} -> n ≤ m -> suc n ≤ suc m

refl-≤ : {n : Nat} -> n ≤ n
refl-≤ {zero } = leqZ
refl-≤ {suc n} = leqS refl-≤

refl-≤' : {n m : Nat} -> n ≡ m -> n ≤ m
refl-≤' refl = refl-≤

trans-≤ : {x y z : Nat} -> x ≤ y -> y ≤ z -> x ≤ z
trans-≤ leqZ      yz        = leqZ
trans-≤ (leqS xy) (leqS yz) = leqS (trans-≤ xy yz)

lem-≤suc : {x : Nat} -> x ≤ suc x
lem-≤suc {zero } = leqZ
lem-≤suc {suc x} = leqS lem-≤suc

lem-≤+L : (x : Nat){y : Nat} -> y ≤ x + y
lem-≤+L zero    = refl-≤
lem-≤+L (suc x) = trans-≤ (lem-≤+L x) lem-≤suc

lem-≤+R : {x y : Nat} -> x ≤ x + y
lem-≤+R {zero } = leqZ
lem-≤+R {suc x} = leqS lem-≤+R

data List (A : Set) : Set where
  ε   : List A
  _,_ : List A -> A -> List A

_++_ : {A : Set} -> List A -> List A -> List A
xs ++ ε        = xs
xs ++ (ys , y) = (xs ++ ys) , y

data All {A : Set}(P : A -> Set) : List A -> Set where
  ∅   : All P ε
  _◄_ : forall {xs x} -> All P xs -> P x -> All P (xs , x)

{-
data Some {A : Set}(P : A -> Set) : List A -> Set where
  hd : forall {x xs} -> P x -> Some P (xs , x)
  tl : forall {x xs} -> Some P xs -> Some P (xs , x)
-}

data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ xs , x
  tl : forall {y xs} -> x ∈ xs -> x ∈ xs , y

_!_ : {A : Set}{P : A -> Set}{xs : List A} ->
      All P xs -> {x : A} -> x ∈ xs -> P x
∅        ! ()
(xs ◄ x) ! hd   = x
(xs ◄ x) ! tl i = xs ! i

tabulate : {A : Set}{P : A -> Set}{xs : List A} ->
           ({x : A} -> x ∈ xs -> P x) -> All P xs
tabulate {xs = ε}      f = ∅
tabulate {xs = xs , x} f = tabulate (f ∘ tl) ◄ f hd

data All² {I : Set}{A : I -> Set}(P : {i : I} -> A i -> Set) :
          {is : List I} -> All A is -> Set where
  ∅²   : All² P ∅
  _◄²_ : forall {i is}{x : A i}{xs : All A is} ->
         All² P xs -> P x -> All² P (xs ◄ x)

data _∈²_ {I : Set}{A : I -> Set}{i : I}(x : A i) :
          {is : List I} -> All A is -> Set where
  hd² : forall {is}{xs : All A is} -> x ∈² xs ◄ x
  tl² : forall {j is}{y : A j}{xs : All A is} ->
        x ∈² xs -> x ∈² xs ◄ y

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Patterns for Fin
------------------------------------------------------------------------

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

module Data.Fin.Patterns where

open import Data.Fin.Base

------------------------------------------------------------------------
-- Constants

pattern 0F = zero
pattern 1F = suc 0F
pattern 2F = suc 1F
pattern 3F = suc 2F
pattern 4F = suc 3F
pattern 5F = suc 4F
pattern 6F = suc 5F
pattern 7F = suc 6F
pattern 8F = suc 7F
pattern 9F = suc 8F


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Text.Pretty.Core where

import Level

open import Data.Bool.Base using (Bool)
open import Data.Erased    as Erased using (Erased) hiding (module Erased)
open import Data.List.Base as List   using (List; []; _∷_)
open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
open import Data.Nat.Properties
open import Data.Product as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
import Data.Product.Relation.Unary.All as Allᴾ

open import Data.Tree.Binary as Tree using (Tree; leaf; node)
open import Data.Tree.Binary.Relation.Unary.All as Allᵀ using (leaf; node)
import Data.Tree.Binary.Relation.Unary.All.Properties as Allᵀₚ
import Data.Tree.Binary.Properties as Treeₚ

open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
open import Data.Maybe.Relation.Unary.All as Allᴹ using (nothing; just)

open import Data.String.Base as String
open import Data.String.Unsafe as Stringₚ
open import Function.Base
open import Relation.Nullary using (Dec)
open import Relation.Unary using (IUniversal; _⇒_)
open import Relation.Binary.PropositionalEquality

open import Data.Refinement hiding (map)
import Data.Refinement.Relation.Unary.All as Allᴿ

------------------------------------------------------------------------
-- Block of text

-- Content is a representation of the first line and the middle of the block.
-- We use a tree rather than a list for the middle of the block so that we can
-- extend it with lines on the left and on the line for free. We will ultimately
-- render the block by traversing the tree left to right in a depth-first manner.

Content : Set
Content = Maybe (String × Tree String)

size : Content → ℕ
size = maybe′ (suc ∘ Tree.size ∘ proj₂) 0

All : ∀ {p} (P : String → Set p) → (Content → Set p)
All P = Allᴹ.All (Allᴾ.All P (Allᵀ.All P))

All≤ : ℕ → Content → Set
All≤ n = All (λ s → length s ≤ n)

record Block : Set where
  field
    height    : ℕ
    block     : [ xs ∈ Content ∣ size xs ≡ height ]
  -- last line
    lastWidth : ℕ
    last      : [ s ∈ String ∣ length s ≡ lastWidth ]
  -- max of all the widths
    maxWidth  : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n (block .value) ]

------------------------------------------------------------------------
-- Raw string

text : String → Block
text s = record
  { height    = 0
  ; block     = nothing , ⦇ refl ⦈
  ; lastWidth = width
  ; last      = s , ⦇ refl ⦈
  ; maxWidth  = width , ⦇ (≤-refl , nothing) ⦈
  } where width = length s; open Erased

------------------------------------------------------------------------
-- Empty

empty : Block
empty = text ""

------------------------------------------------------------------------
-- Helper functions

node? : Content → String → Tree String → Content
node? (just (x , xs)) y ys = just (x , node xs y ys)
node? nothing         y ys = just (y , ys)

∣node?∣ : ∀ b y ys → size (node? b y ys)
                   ≡ size b + suc (Tree.size ys)
∣node?∣ (just (x , xs)) y ys = refl
∣node?∣ nothing         y ys = refl

≤-Content : ∀ {m n} {b : Content} → m ≤ n → All≤ m b → All≤ n b
≤-Content {m} {n} m≤n = Allᴹ.map (Prod.map step (Allᵀ.map step))

  where

  step : ∀ {p} → p ≤ m → p ≤ n
  step = flip ≤-trans m≤n

All≤-node? : ∀ {l m r n} →
             All≤ n l → length m ≤ n → Allᵀ.All (λ s → length s ≤ n) r →
             All≤ n (node? l m r)
All≤-node? nothing           py pys = just (py , pys)
All≤-node? (just (px , pxs)) py pys = just (px , node pxs py pys)

------------------------------------------------------------------------
-- Appending two documents

private
  module append (x y : Block) where

    module x = Block x
    module y = Block y

    blockx = x.block .value
    blocky = y.block .value

    widthx = x.maxWidth .value
    widthy = y.maxWidth .value

    lastx = x.last .value
    lasty = y.last .value

    height : ℕ
    height = (_+_ on Block.height) x y

    lastWidth : ℕ
    lastWidth = (_+_ on Block.lastWidth) x y

    pad : Maybe String
    pad with x.lastWidth
    ... | 0 = nothing
    ... | l = just (replicate l ' ')

    size-pad : maybe′ length 0 pad ≡ x.lastWidth
    size-pad with x.lastWidth
    ... | 0         = refl
    ... | l@(suc _) = length-replicate l

    indent : Maybe String → String → String
    indent = maybe′ _++_ id

    size-indent : ∀ ma str → length (indent ma str)
                ≡ maybe′ length 0 ma + length str
    size-indent nothing    str = refl
    size-indent (just pad) str = length-++ pad str

    indents : Maybe String → Tree String → Tree String
    indents = maybe′ (Tree.map ∘ _++_) id

    size-indents : ∀ ma t → Tree.size (indents ma t) ≡ Tree.size t
    size-indents nothing    t = refl
    size-indents (just pad) t = Treeₚ.size-map (pad ++_) t

    unfold-indents : ∀ ma t → indents ma t ≡ Tree.map (indent ma) t
    unfold-indents nothing    t = sym (Treeₚ.map-id t)
    unfold-indents (just pad) t = refl

    vContent : Content × String
    vContent with blocky
    ... | nothing        = blockx
                         , lastx ++ lasty
    ... | just (hd , tl) = node?
      {-,--------------,-}
      {-|-} blockx   {-|-}
      {-|-}          {-'---,-}    {-,------------------,-}
      {-|-} (lastx       {-|-} ++ {-|-}  hd)         {-|-}
      {-'------------------'-}    {-|-}              {-|-}
      (indents pad                {-|-}  tl)    {-,----'-}
      , indent pad                {-|-} lasty   {-|-}
                                  {-'-------------'-}

    vBlock = proj₁ vContent
    vLast  = proj₂ vContent

    isBlock : size blockx ≡ x.height → size blocky ≡ y.height →
              size vBlock ≡ height
    isBlock ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      size blockx         ≡⟨ ∣x∣ ⟩
      x.height            ≡˘⟨ +-identityʳ x.height ⟩
      x.height + 0        ≡⟨ cong (_ +_) ∣y∣ ⟩
      x.height + y.height ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      ∣node∣                          ≡⟨ ∣node?∣ blockx middle rest ⟩
      ∣blockx∣ + suc (Tree.size rest) ≡⟨ cong ((size blockx +_) ∘′ suc) ∣rest∣ ⟩
      ∣blockx∣ + suc (Tree.size tl)   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.height + y.height             ∎ where

      open ≡-Reasoning
      ∣blockx∣ = size blockx
      middle   = lastx ++ hd
      rest     = indents pad tl
      ∣rest∣   = size-indents pad tl
      ∣node∣   = size (node? blockx middle rest)

    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vBlock
    block .proof = ⦇ isBlock (Block.block x .proof) (Block.block y .proof) ⦈
      where open Erased

    isLastLine : length lastx ≡ x.lastWidth →
                 length lasty ≡ y.lastWidth →
                 length vLast ≡ lastWidth
    isLastLine ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      length (lastx ++ lasty)       ≡⟨ length-++ lastx lasty ⟩
      length lastx + length lasty   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.lastWidth + y.lastWidth     ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      length (indent pad lasty)          ≡⟨ size-indent pad lasty ⟩
      maybe′ length 0 pad + length lasty ≡⟨ cong₂ _+_ size-pad ∣y∣ ⟩
      x.lastWidth + y.lastWidth          ∎ where open ≡-Reasoning

    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last .value = vLast
    last .proof = ⦇ isLastLine (Block.last x .proof) (Block.last y .proof) ⦈
      where open Erased

    vMaxWidth : ℕ
    vMaxWidth = widthx ⊔ (x.lastWidth + widthy)

    isMaxWidth₁ : y.lastWidth ≤ widthy → lastWidth ≤ vMaxWidth
    isMaxWidth₁ p = begin
      lastWidth            ≤⟨ +-monoʳ-≤ x.lastWidth p ⟩
      x.lastWidth + widthy ≤⟨ n≤m⊔n _ _ ⟩
      vMaxWidth            ∎ where open ≤-Reasoning

    isMaxWidth₂ : length lastx ≡ x.lastWidth →
                  x.lastWidth ≤ widthx →
                  All≤ widthx blockx →
                  All≤ widthy blocky →
                  All≤ vMaxWidth vBlock
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ ∣ys∣ with blocky
    ... | nothing        = ≤-Content (m≤m⊔n _ _) ∣xs∣
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ (just (∣hd∣ , ∣tl∣))
        | just (hd , tl) =
      All≤-node? (≤-Content (m≤m⊔n _ _) ∣xs∣)
                 middle
                 (subst (Allᵀ.All _) (sym $ unfold-indents pad tl)
                 $ Allᵀₚ.map⁺ (indent pad) (Allᵀ.map (indented _) ∣tl∣))
      where

      middle : length (lastx ++ hd) ≤ vMaxWidth
      middle = begin
        length (lastx ++ hd)     ≡⟨ length-++ lastx hd ⟩
        length lastx + length hd ≡⟨ cong (_+ _) ∣x∣≡ ⟩
        x.lastWidth + length hd  ≤⟨ +-monoʳ-≤ x.lastWidth ∣hd∣ ⟩
        x.lastWidth + widthy     ≤⟨ n≤m⊔n _ _ ⟩
        vMaxWidth                ∎ where open ≤-Reasoning

      indented : ∀ s → length s ≤ widthy →
                 length (indent pad s) ≤ vMaxWidth
      indented s ∣s∣ = begin
        length (indent pad s)          ≡⟨ size-indent pad s ⟩
        maybe′ length 0 pad + length s ≡⟨ cong (_+ _) size-pad ⟩
        x.lastWidth + length s         ≤⟨ +-monoʳ-≤ x.lastWidth ∣s∣ ⟩
        x.lastWidth + widthy           ≤⟨ n≤m⊔n (widthx) _ ⟩
        vMaxWidth                      ∎ where open ≤-Reasoning

    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vBlock ]
    maxWidth .value = vMaxWidth
    maxWidth .proof =
      ⦇ _,_ ⦇ isMaxWidth₁ (map proj₁ (Block.maxWidth y .proof)) ⦈
            ⦇ isMaxWidth₂ (Block.last x .proof)
                          (map proj₁ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth y .proof))
            ⦈
      ⦈ where open Erased

infixl 4 _<>_
_<>_ : Block → Block → Block
x <> y = record { append x y }

------------------------------------------------------------------------
-- Flush (introduces a new line)

private
  module flush (x : Block) where

    module x = Block x
    blockx  = x.block .value
    lastx   = x.last .value
    widthx  = x.maxWidth .value
    heightx = x.height

    height    = suc heightx
    lastWidth = 0
    vMaxWidth = widthx

    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last = "" , ⦇ refl ⦈ where open Erased

    vContent = node? blockx lastx leaf

    isBlock : size blockx ≡ heightx → size vContent ≡  height
    isBlock ∣x∣ = begin
      size vContent   ≡⟨ ∣node?∣ blockx lastx leaf ⟩
      size blockx + 1 ≡⟨ cong (_+ 1) ∣x∣ ⟩
      heightx + 1     ≡⟨ +-comm heightx 1 ⟩
      height          ∎ where open ≡-Reasoning

    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vContent
    block .proof = Erased.map isBlock $ Block.block x .proof

    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vContent ]
    maxWidth .value = widthx
    maxWidth .proof = map (z≤n ,_)
      ⦇ All≤-node? ⦇ proj₂ (Block.maxWidth x .proof) ⦈
                   ⦇ middle (Block.last x .proof) ⦇ proj₁ (Block.maxWidth x .proof) ⦈ ⦈
                   (pure leaf)
      ⦈ where

      open Erased

      middle : length lastx ≡ x.lastWidth → x.lastWidth ≤ vMaxWidth →
               length lastx ≤ vMaxWidth
      middle p q = begin
        length lastx ≡⟨ p ⟩
        x.lastWidth  ≤⟨ q ⟩
        vMaxWidth    ∎ where open ≤-Reasoning

flush : Block → Block
flush x = record { flush x }

------------------------------------------------------------------------
-- Other functions

render : Block → String
render x = unlines
  $ maybe′ (uncurry (λ hd tl → hd ∷ Tree.Infix.toList tl)) []
  $ node? (Block.block x .value) (Block.last x .value) leaf

valid : (width : ℕ) (b : Block) → Dec (Block.maxWidth b .value ≤ width)
valid width b = Block.maxWidth b .value ≤? width


text:
module CoinductiveBuiltinList where

open import Common.Coinduction

data List (A : Set) : Set where
  []  : List A
  _∷_ : (x : A) (xs : ∞ (List A)) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- This module introduces operators.

module Introduction.Operators where

-- Agda has a very flexible mechanism for defining operators, supporting infix,
-- prefix, postfix and mixfix operators.

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

-- Any name containing underscores (_) can be used as an operator by writing
-- the arguments where the underscores are. For instance, the function _+_ is
-- the infix addition function. This function can be used either as a normal
-- function: '_+_ zero zero', or as an operator: 'zero + zero'.

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

-- A fixity declaration specifies precedence level (50 in this case) and
-- associativity (left associative here) of an operator. Only infix operators
-- (whose names start and end with _) have associativity.
infixl 50 _+_

-- The only restriction on where _ can appear in a name is that there cannot be
-- two underscores in sequence. For instance, we can define an if-then-else
-- operator:

data Bool : Set where
  false : Bool
  true  : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

-- if_then_else_ is treated as a prefix operator (ends, but doesn't begin with
-- an _), so the declared precedence determines how something in an else branch
-- should be parsed. For instance, with the given precedences
--   if x then y else a + b
-- is parsed as
--   if x then y else (a + b)
-- and not
--   (if x then y else a) + b

infix 10 if_then_else_

-- In Agda there is no restriction on what characters are allowed to appear in
-- an operator (as opposed to a function symbol). For instance, it is allowed
-- (but not recommended) to define 'f' to be an infix operator and '+' to be a
-- function symbol.

module BadIdea where

  _f_ : Nat -> Nat -> Nat
  zero  f zero  = zero
  zero  f suc n = suc n
  suc n f zero  = suc n
  suc n f suc m = suc (n f m)

  + : Nat -> Nat
  + n = suc n


text:
module Issue1232.All where

import Issue1232.Fin
import Issue1232.List

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Level
open import Categories.Category

module Categories.Functor.Power.Functorial {o ℓ e : Level} (C : Category o ℓ e) where

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

open import Categories.Functor renaming (id to idF)
open import Categories.Category.Discrete
open import Categories.Category.Equivalence
open import Categories.Category.Construction.Functors
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism as NI
  using (module NaturalIsomorphism; _≃_; refl)
import Categories.Morphism.Reasoning as MR
open MR C

import Categories.Functor.Power as Power
open Power C

open Category using (Obj)
open Category C using (_⇒_; _∘_; module Equiv)
module C = Category C
module CE = Equiv

private
  variable
    i : Level
    I : Set i

exp→functor₀ : Obj (Exp I) → Functor (Discrete I) C
exp→functor₀ X = record
  { F₀ = X
  ; F₁ = λ { refl → C.id }
  ; identity = CE.refl
  ; homomorphism = λ { {_} {_} {_} {refl} {refl} → CE.sym C.identityˡ}
  ; F-resp-≈ = λ { {_} {_} {refl} {refl} refl → CE.refl}
  }

exp→functor₁ : {X Y : I → C.Obj} → Exp I [ X , Y ] → NaturalTransformation (exp→functor₀ X) (exp→functor₀ Y)
exp→functor₁ F = record { η = F ; commute = λ { refl → id-comm } ; sym-commute = λ { refl → id-comm-sym } }

exp→functor : Functor (Exp I) (Functors (Discrete I) C)
exp→functor = record
  { F₀ = exp→functor₀
  ; F₁ = exp→functor₁
  ; identity = CE.refl
  ; homomorphism = CE.refl
  ; F-resp-≈ = λ eqs {x} → eqs x
  }

functor→exp : Functor (Functors (Discrete I) C) (Exp I)
functor→exp = record
  { F₀ = Functor.F₀
  ; F₁ = NaturalTransformation.η
  ; identity = λ _ → CE.refl
  ; homomorphism = λ _ → CE.refl
  ; F-resp-≈ = λ eqs i → eqs {i}
  }

exp≋functor : StrongEquivalence (Exp I) (Functors (Discrete I) C)
exp≋functor = record
  { F = exp→functor
  ; G = functor→exp
  ; weak-inverse = record
    { F∘G≈id = record
      { F⇒G = ntHelper record
        { η       = λ DI → record
          { η           = λ _ → C.id
          ; commute     = λ { refl → C.∘-resp-≈ˡ (CE.sym (Functor.identity DI))}
          ; sym-commute = λ { refl → C.∘-resp-≈ˡ (Functor.identity DI)}
          }
        ; commute = λ _ → id-comm-sym
        }
      ; F⇐G = ntHelper record
        { η = λ DI → ntHelper record { η = λ _ → C.id ; commute = λ { refl → C.∘-resp-≈ʳ (Functor.identity DI)} }
        ; commute = λ _ → id-comm-sym
        }
      ; iso = λ X → record { isoˡ = C.identity²; isoʳ = C.identity² }
      }
    ; G∘F≈id = record
      { F⇒G = record { η = λ _ _ → C.id ; commute = λ _ _ → id-comm-sym ; sym-commute = λ _ _ → id-comm }
      ; F⇐G = record { η = λ _ _ → C.id ; commute = λ _ _ → id-comm-sym ; sym-commute = λ _ _ → id-comm }
      ; iso = λ X → record { isoˡ = λ _ → C.identity² ; isoʳ = λ _ → C.identity² }
      }
    }
  }
  where
    open C.HomReasoning

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light where

open import Light.Library public
module Implementation where open import Light.Implementation public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import Cubical.Data.NatMinusOne.Base public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import HoTT
open import homotopy.Bouquet
open import cohomology.Theory

module cohomology.Bouquet {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cohomology.Sphere OT

C-Bouquet-diag : ∀ n (I : Type i) → has-choice 0 I i
  → C (ℕ-to-ℤ n) (⊙Bouquet I n) ≃ᴳ Πᴳ I (λ _ → C2 0)
C-Bouquet-diag n I I-choice =
  C (ℕ-to-ℤ n) (⊙Bouquet I n)
    ≃ᴳ⟨ C-emap (ℕ-to-ℤ n) (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)) ⟩
  C (ℕ-to-ℤ n) (⊙BouquetLift I n)
    ≃ᴳ⟨ C-additive-iso (ℕ-to-ℤ n) (BouquetLift-family I n) I-choice ⟩
  Πᴳ I (λ _ → C (ℕ-to-ℤ n) (⊙Lift (⊙Sphere n)))
    ≃ᴳ⟨ Πᴳ-emap-r I (λ _ → C-Sphere-diag n) ⟩
  Πᴳ I (λ _ → C2 0)
    ≃ᴳ∎

abstract
  C-Bouquet-≠-is-trivial : ∀ (n : ℤ) (I : Type i) (m : ℕ)
    → (n ≠ ℕ-to-ℤ m) → has-choice 0 I i
    → is-trivialᴳ (C n (⊙Bouquet I m))
  C-Bouquet-≠-is-trivial n I m n≠m I-choice = iso-preserves'-trivial
    (C n (⊙Bouquet I m)
      ≃ᴳ⟨ C-emap n (⊙BigWedge-emap-r (λ _ → ⊙lower-equiv)) ⟩
    C n (⊙BouquetLift I m)
      ≃ᴳ⟨ C-additive-iso n (BouquetLift-family I m) I-choice ⟩
    Πᴳ I (λ _ → C n (⊙Lift (⊙Sphere m)))
      ≃ᴳ∎)
    (Πᴳ-is-trivial I (λ _ → C n (⊙Lift (⊙Sphere m))) (λ _ → C-Sphere-≠-is-trivial n m n≠m))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Issue756b where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data T : (Nat → Nat) → Set where
  idId : T (λ { zero → zero; (suc n) → suc n })

bad : ∀ f → T f → Nat
bad .(λ { zero → zero ; (suc n) → suc n }) idId = zero

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.Disks
open import CaTT.Ps-contexts
open import CaTT.Uniqueness-Derivations-Ps
open import Sets ℕ eqdecℕ

module CaTT.Fullness where

  data Ty : Set₁
  data Tm : Set₁
  data Sub : Set₁

  data _is-full-in_ : Ty → ps-ctx → Set₁

  data Ty where
    ∗ : Ty
    ⇒ : Ty → Tm → Tm → Ty
  data Tm where
    v : ℕ → Tm
    coh : (Γ : ps-ctx) → (A : Ty) → A is-full-in Γ → Sub  → Tm
  data Sub where
    <> : Sub
    <_,_↦_> : Sub → ℕ → Tm → Sub

  =⇒Ty : ∀ {A A' : Ty} {t t' u u' : Tm} → _==_ {A = Ty} (⇒ A t u) (⇒ A' t' u') → ((A == A' × t == t') × u == u')
  =⇒Ty idp = (idp , idp) , idp

  coh= : ∀ {Γ Γ' A A' Afull A'full γ γ'} → coh Γ A Afull γ == coh Γ' A' A'full γ' → ((Γ == Γ' × A == A') × γ == γ')
  coh= idp = (idp , idp) , idp

  <>= : ∀ {γ γ' x x' t t'} → < γ , x ↦ t > == < γ' , x' ↦ t' > → ((γ == γ' × x == x') × t == t')
  <>= idp = (idp , idp) , idp

  {- Set of variables -}
  varC : Pre-Ctx → set
  varC nil = Ø
  varC (Γ :: (x , _)) = (varC Γ) ∪-set (singleton x)

  varT : Ty → set
  vart : Tm → set
  varS : Sub → set

  varT ∗ = Ø
  varT (⇒ A t u) = (varT A) ∪-set ((vart t) ∪-set (vart u))
  vart (v x) = singleton x
  vart (coh Γ A Afull γ) = varS γ
  varS <> = Ø
  varS < γ , x ↦ t > = (varS γ) ∪-set (vart t)

  {- fullness condition -}
  data _is-full-in_ where
    side-cond₁ : ∀ Γ A t u → (src-var Γ) ≗ ((varT A) ∪-set (vart t)) → (tgt-var Γ) ≗ ((varT A) ∪-set (vart u)) → (⇒ A t u) is-full-in Γ
    side-cond₂ : ∀ Γ A →  (varC (fst Γ)) ≗ (varT A) → A is-full-in Γ

  ∈-drop : ∀ {A : Set} {a : A} {l : list A} → a ∈-list drop l → a ∈-list l
  ∈-drop {A} {a} {l :: a₁} x = inl x

  l∉∂⁻ : ∀ {Γ i x A y} → (Γ⊢ps : Γ ⊢ps x # A) → length Γ ≤ y → ¬ (y ∈-list (srcᵢ-var i Γ⊢ps))
  l∉∂⁻ {i = i} pss lΓ≤y y∈ with eqdecℕ i O
  ... | inl _ = y∈
  l∉∂⁻ {i = i} pss lΓ≤y (inr idp) | inr _ = Sn≰n _ lΓ≤y
  l∉∂⁻ (psd Γ⊢ps) lΓ≤y y∈ = l∉∂⁻ Γ⊢ps lΓ≤y y∈
  l∉∂⁻ {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) SSl≤y y∈ with dec-≤ i (S (dim A))
  ... | inl _ = l∉∂⁻ Γ⊢ps (Sn≤m→n≤m (Sn≤m→n≤m SSl≤y)) y∈
  l∉∂⁻ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inl (inl y∈)) | inr _ = l∉∂⁻ Γ⊢ps (Sn≤m→n≤m (Sn≤m→n≤m SSl≤y)) y∈
  l∉∂⁻ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inl (inr idp)) | inr _ = Sn≰n _ (n≤m→n≤Sm SSl≤y)
  l∉∂⁻ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inr idp) | inr _ = Sn≰n _ SSl≤y

  l∉∂⁺ : ∀ {Γ i x A y} → (Γ⊢ps : Γ ⊢ps x # A) → length Γ ≤ y → ¬ (y ∈-list (tgtᵢ-var i Γ⊢ps))
  l∉∂⁺ {i = i} pss lΓ≤y y∈ with eqdecℕ i O
  ... | inl _ = y∈
  l∉∂⁺ {i = i} pss lΓ≤y (inr idp) | inr _ = Sn≰n _ lΓ≤y
  l∉∂⁺ (psd Γ⊢ps) lΓ≤y y∈ = l∉∂⁺ Γ⊢ps lΓ≤y y∈
  l∉∂⁺ {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) SSl≤y y∈ with dec-≤ i (S (dim A))
  l∉∂⁺ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inl (inl y∈)) | inr _ = l∉∂⁺ Γ⊢ps (Sn≤m→n≤m (Sn≤m→n≤m SSl≤y)) y∈
  l∉∂⁺ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inl (inr idp)) | inr _ = Sn≰n _ (n≤m→n≤Sm SSl≤y)
  l∉∂⁺ {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inr idp) | inr x = Sn≰n _ SSl≤y
  ... | inl _ with eqdecℕ i (S (dim A))
  l∉∂⁺ {i = .(S (dim _))} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inl y∈drop) | inl _ | inl idp = l∉∂⁺ Γ⊢ps (Sn≤m→n≤m (Sn≤m→n≤m SSl≤y)) (∈-drop y∈drop)
  l∉∂⁺ {i = .(S (dim _))} (pse {A = _} Γ⊢ps idp idp idp idp idp) SSl≤y (inr idp) | inl _ | inl idp = Sn≰n _ (n≤m→n≤Sm SSl≤y)
  ... | inr _ = l∉∂⁺ Γ⊢ps (Sn≤m→n≤m (Sn≤m→n≤m SSl≤y)) y∈

  ∂⁻ᵢ-var : ∀ {Γ x A y B i} → (Γ⊢ps : Γ ⊢ps x # A)  → Γ ⊢t (Var y) # B → i ≤ dim B → ¬ (y ∈-list (srcᵢ-var i Γ⊢ps))
  ∂⁻ᵢ-var pss (var x (inr (idp , idp))) (0≤ .0) ()
  ∂⁻ᵢ-var (psd Γ⊢ps) Γ⊢y i≤B y∈∂⁻ = ∂⁻ᵢ-var Γ⊢ps Γ⊢y i≤B y∈∂⁻
  ∂⁻ᵢ-var {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B y∈∂⁻ with dec-≤ i (S (dim A))
  ... | inl _ = ∂⁻ᵢ-var Γ⊢ps (var (psv Γ⊢ps) y∈Γ) i≤B y∈∂⁻
  ∂⁻ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inl (inl y∈∂⁻)) | inr _ = ∂⁻ᵢ-var Γ⊢ps (var (psv Γ⊢ps) y∈Γ) i≤B y∈∂⁻
  ∂⁻ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inl (inr idp)) | inr _ = x∉ (psv Γ⊢ps) (n≤n _) (var (psv Γ⊢ps) y∈Γ)
  ∂⁻ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inr idp) | inr _ = x∉ (psv Γ⊢ps) (n≤Sn _) (var (psv Γ⊢ps) y∈Γ)
  ∂⁻ᵢ-var {i = i} (pse {A = B} Γ⊢ps idp idp idp idp idp) (var _ (inl (inr (idp , idp)))) i≤B y∈∂⁻ with dec-≤ i (S (dim B))
  ... | inl _ = l∉∂⁻ Γ⊢ps (n≤n _) y∈∂⁻
  ... | inr i≰SB = i≰SB (n≤m→n≤Sm i≤B)
  ∂⁻ᵢ-var {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) (var _ (inr (idp , idp))) i≤SA y∈∂⁻ with dec-≤ i (S (dim A))
  ... | inl _ = l∉∂⁻ Γ⊢ps (n≤Sn _) y∈∂⁻
  ... | inr i≰SA = i≰SA i≤SA

  ∂⁺ᵢ-var : ∀ {Γ x A y B i} → (Γ⊢ps : Γ ⊢ps x # A)  → Γ ⊢t (Var y) # B → i ≤ dim B → ¬ (y ∈-list (tgtᵢ-var i Γ⊢ps))
  ∂⁺ᵢ-var pss (var x (inr (idp , idp))) (0≤ .0) ()
  ∂⁺ᵢ-var (psd Γ⊢ps) Γ⊢y i≤B y∈∂⁺ = ∂⁺ᵢ-var Γ⊢ps Γ⊢y i≤B y∈∂⁺
  ∂⁺ᵢ-var {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B y∈∂⁺ with dec-≤ i (S (dim A))
  ... | inl i≤SdimA with eqdecℕ i (S (dim A))
  ... | inr _ = ∂⁺ᵢ-var Γ⊢ps (var (psv Γ⊢ps) y∈Γ) i≤B y∈∂⁺
  ∂⁺ᵢ-var {i = .(S (dim _))} (pse {A = A}  Γ⊢ps idp idp idp idp idp) (var {x = y} _ (inl (inl y∈Γ))) i≤B (inl y∈drop) | inl i≤SdimA | inl idp = ∂⁺ᵢ-var Γ⊢ps (var (psv Γ⊢ps) y∈Γ) i≤B (∈-drop y∈drop)
  ∂⁺ᵢ-var {i = .(S (dim _))} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inr idp) | inl i≤SdimA | inl idp = lΓ∉Γ (psv Γ⊢ps) y∈Γ
  ∂⁺ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inl (inl y∈∂⁻)) | inr _ = ∂⁺ᵢ-var Γ⊢ps (var (psv Γ⊢ps) y∈Γ) i≤B y∈∂⁻
  ∂⁺ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inl (inr idp)) | inr _ = x∉ (psv Γ⊢ps) (n≤n _) (var (psv Γ⊢ps) y∈Γ)
  ∂⁺ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inl (inl y∈Γ))) i≤B (inr idp) | inr _ = x∉ (psv Γ⊢ps) (n≤Sn _) (var (psv Γ⊢ps) y∈Γ)
  ∂⁺ᵢ-var {i = i} (pse {A = B} Γ⊢ps idp idp idp idp idp) (var _ (inl (inr (idp , idp)))) i≤B y∈∂⁺ with dec-≤ i (S (dim B))
  ... | inr i≰SB = i≰SB (n≤m→n≤Sm i≤B)
  ... | inl _  with eqdecℕ i (S (dim B))
  ... | inr _ = l∉∂⁺ Γ⊢ps (n≤n _) y∈∂⁺
  ∂⁺ᵢ-var (pse Γ⊢ps idp idp idp idp idp) (var _ (inl (inr (idp , idp)))) i≤B (inl l∈drop) | inl _ | inl _ = l∉∂⁺ Γ⊢ps (n≤n _) (∈-drop l∈drop)
  ∂⁺ᵢ-var (pse Γ⊢ps idp idp idp idp idp) (var _ (inl (inr (idp , idp)))) i≤B (inr p) | inl _ | inl idp = Sn≰n _ i≤B
  ∂⁺ᵢ-var {i = i} (pse {A = A} Γ⊢ps idp idp idp idp idp) (var _ (inr (idp , idp))) i≤SA y∈∂⁺ with dec-≤ i (S (dim A))
  ... | inr i≰SA = i≰SA i≤SA
  ... | inl _ with eqdecℕ i (S (dim A))
  ... | inr _ = l∉∂⁺ Γ⊢ps (n≤Sn _) y∈∂⁺
  ∂⁺ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inr (idp , idp))) i≤SA (inl Sl∈drop) | inl _ | inl _ = l∉∂⁺ Γ⊢ps (n≤Sn _) (∈-drop Sl∈drop)
  ∂⁺ᵢ-var {i = i} (pse {A = _} Γ⊢ps idp idp idp idp idp) (var _ (inr (idp , idp))) i≤SA (inr Sl=l) | inl _ | inl _ = Sn≠n _ Sl=l

  ∈-varC : ∀ {Γ x A} →  x # A ∈ Γ → x ∈-set (varC Γ)
  ∈-varC {Γ :: (y , B)} {x} {A} (inl x∈Γ) = ∈-∪₁ {A = varC Γ} {B = singleton y} (∈-varC x∈Γ)
  ∈-varC {Γ :: (y , B)} {x} {A} (inr (idp , _)) = ∈-∪₂ {A = varC Γ} {B = singleton y} (∈-singleton y)

  max-var-def : Pre-Ctx → ℕ × Pre-Ty
  max-var-def nil = 0 , ∗
  max-var-def (Γ :: (y , B)) with dec-≤ (dimC Γ) (dim B)
  ... | inr _ = max-var-def Γ
  ... | inl _ = y , B

  max-var-is-max : ∀ {Γ} → Γ ≠ nil → Γ ⊢C → let (x , A) = max-var-def Γ in ((x # A ∈ Γ) × (dimC Γ == dim A))
  max-var-is-max {nil} Γ≠nil _ = ⊥-elim (Γ≠nil idp)
  max-var-is-max {Γ :: (y , B)} _ Γ⊢ with dec-≤ (dimC Γ) (dim B)
  ... | inl _ = inr (idp , idp) , idp
  ... | inr _ with Γ
  max-var-is-max {Γ :: (y , B)} _ (cc Γ⊢ Γ⊢B idp) | inr _ | Δ :: (x , A) = let (x∈ , dimA) = max-var-is-max (λ{()}) Γ⊢ in inl x∈ , dimA
  max-var-is-max {Γ :: (.0 , .∗)} _ (cc Γ⊢ (ob _) idp) | inr _ | nil = inr (idp , idp) , idp
  max-var-is-max {Γ :: (.0 , _)} _ (cc Γ⊢ (ar _ _) idp) | inr dΓ≤dB | nil = ⊥-elim (dΓ≤dB (0≤ _))

  psx-nonul : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ≠ nil
  psx-nonul (psd x) idp = psx-nonul x idp

  ps-nonul : ∀ {Γ} → Γ ⊢ps → Γ ≠ nil
  ps-nonul (ps Γ⊢ps) = psx-nonul Γ⊢ps

  max-var : ∀ {Γ} → Γ ⊢ps → Σ (ℕ × Pre-Ty) λ {(x , A) → (x # A ∈ Γ) × (dimC Γ == dim A)}
  max-var {Γ} Γ⊢ps@(ps Γ⊢psx) = max-var-def Γ , max-var-is-max (ps-nonul Γ⊢ps) (psv Γ⊢psx)

  ∂Γ-not-full : ∀ Γ → ¬ (varC (fst Γ) ⊂ ((src-var Γ) ∪-set (tgt-var Γ)))
  ∂Γ-not-full (Γ , Γ⊢ps@(ps Γ⊢psx)) vΓ⊂∂ = let ((x , A) , (x∈Γ , dimA)) = max-var Γ⊢ps in
    ∉-∪ {set-of-list (srcᵢ-var (dimC Γ) Γ⊢psx)} {set-of-list (tgtᵢ-var (dimC Γ) Γ⊢psx)} {x}
    (λ x∈∂⁻ → ∂⁻ᵢ-var Γ⊢psx (var (psv Γ⊢psx) x∈Γ) (≤-= (n≤n _) dimA) (∈-set-∈-list _ _ x∈∂⁻))
    (λ x∈∂⁺ → ∂⁺ᵢ-var Γ⊢psx (var (psv Γ⊢psx) x∈Γ) (≤-= (n≤n _) dimA) (∈-set-∈-list _ _ x∈∂⁺))
    (vΓ⊂∂ x (∈-varC x∈Γ))

  disjoint-cond : ∀ Γ A t u → (src-var Γ) ≗ ((varT A) ∪-set (vart t)) → (tgt-var Γ) ≗ ((varT A) ∪-set (vart u)) → ¬ (varC (fst Γ) ≗ varT (⇒ A t u))
  disjoint-cond Γ A t u (_ , A⊂∂⁻) (_ , A⊂∂⁺) (Γ⊂A , _) =
    let vA = varT A in let vt = vart t in let vu = vart u in
    let sr = src-var Γ in let tg = tgt-var Γ in
    ∂Γ-not-full Γ
      (⊂-trans {varC (fst Γ)} {vA ∪-set (vt ∪-set vu)} {sr ∪-set tg} Γ⊂A
      (≗-⊂ {vA ∪-set (vt ∪-set vu)} {(vA ∪-set vt) ∪-set (vA ∪-set vu)} {sr ∪-set tg} (∪-factor (varT A) (vart t) (vart u))
      (⊂-∪ {vA ∪-set vt} {sr} {vA ∪-set vu} {tg} A⊂∂⁻ A⊂∂⁺)))

  side-cond₁= : ∀ Γ A t u ∂⁻-full₁ ∂⁻-full₂ ∂⁺-full₁ ∂⁺-full₂ → ∂⁻-full₁ == ∂⁻-full₂ → ∂⁺-full₁ == ∂⁺-full₂ → side-cond₁ Γ A t u ∂⁻-full₁ ∂⁺-full₁ == side-cond₁ Γ A t u ∂⁻-full₂ ∂⁺-full₂
  side-cond₁= Γ A t u ∂⁻-full₁ .∂⁻-full₁ ∂⁺-full₁ .∂⁺-full₁ idp idp = idp

  has-all-paths-is-full : ∀ Γ A → has-all-paths (A is-full-in Γ)
  has-all-paths-is-full Γ .(⇒ A t u) (side-cond₁ .Γ A t u x x₁) (side-cond₁ .Γ .A .t .u x₂ x₃) = ap² (λ ∂⁻ → λ ∂⁺ → side-cond₁ Γ A t u ∂⁻ ∂⁺) (is-prop-has-all-paths (is-prop-≗ (src-var Γ) (varT A ∪-set vart t)) x x₂) (is-prop-has-all-paths (is-prop-≗ (tgt-var Γ) (varT A ∪-set vart u)) x₁ x₃)
  has-all-paths-is-full Γ .(⇒ A t u) (side-cond₁ .Γ A t u ∂⁻ ∂⁺) (side-cond₂ .Γ .(⇒ A t u) full) = ⊥-elim (disjoint-cond Γ A t u ∂⁻ ∂⁺ full)
  has-all-paths-is-full Γ .(⇒ A t u) (side-cond₂ .Γ .(⇒ A t u) full) (side-cond₁ .Γ A t u ∂⁻ ∂⁺) = ⊥-elim (disjoint-cond Γ A t u ∂⁻ ∂⁺ full)
  has-all-paths-is-full Γ A (side-cond₂ .Γ .A x) (side-cond₂ .Γ .A x₁) = ap (side-cond₂ Γ A) (is-prop-has-all-paths (is-prop-≗ (varC (fst Γ)) (varT A)) x x₁)

  is-prop-full : ∀ Γ A → is-prop (A is-full-in Γ)
  is-prop-full Γ A = has-all-paths-is-prop (has-all-paths-is-full Γ A)

  eqdec-Ty : eqdec Ty
  eqdec-Tm : eqdec Tm
  eqdec-Sub : eqdec Sub

  eqdec-Ty ∗ ∗ = inl idp
  eqdec-Ty ∗ (⇒ _ _ _) = inr λ{()}
  eqdec-Ty (⇒ _ _ _) ∗ = inr λ{()}
  eqdec-Ty (⇒ A t u) (⇒ A' t' u') with eqdec-Ty A A' | eqdec-Tm t t' | eqdec-Tm u u'
  ...                                        | inl idp | inl idp | inl idp = inl idp
  ...                                        | inr A≠A' | _ | _ = inr λ {idp → A≠A' idp}
  ...                                        | inl idp | inr t≠t' | _ = inr λ p → t≠t' (snd (fst (=⇒Ty p)))
  ...                                        | inl idp | inl idp | inr u≠u' = inr λ p → u≠u' (snd (=⇒Ty p))
  eqdec-Tm (v x) (v y) with eqdecℕ x y
  ...                   | inl idp = inl idp
  ...                   | inr x≠y = inr λ{idp → x≠y idp}
  eqdec-Tm (v _) (coh _ _ _ _) = inr λ{()}
  eqdec-Tm (coh _ _ _ _) (v _) = inr λ{()}
  eqdec-Tm (coh Γ A Afull γ) (coh Γ' A' A'full γ') with eqdec-ps Γ Γ' | eqdec-Ty A A' | eqdec-Sub γ γ'
  ...                                               | inl idp | inl idp | inl idp = inl (ap (λ X → coh Γ A X γ) (is-prop-has-all-paths (is-prop-full Γ A) Afull A'full))
  ...                                               | inr Γ≠Γ' | _ | _ = inr λ {idp → Γ≠Γ' idp}
  ...                                               | inl idp | inr A≠A' | _ = inr λ p → A≠A' (snd (fst (coh= p)))
  ...                                               | inl idp | inl idp | inr γ≠γ' = inr λ p → γ≠γ' (snd (coh= p))
  eqdec-Sub <> <> = inl idp
  eqdec-Sub <> < _ , _ ↦ _ > = inr λ{()}
  eqdec-Sub < _ , _ ↦ _ > <> = inr λ{()}
  eqdec-Sub < γ , x ↦ t > < γ' , x' ↦ t' > with eqdec-Sub γ γ' | eqdecℕ x x' | eqdec-Tm t t'
  ...                                        | inl idp | inl idp | inl idp = inl idp
  ...                                        | inr γ≠γ' | _ | _ = inr λ {idp → γ≠γ' idp}
  ...                                        | inl idp | inr x≠x' | _ = inr λ p → x≠x' (snd (fst (<>= p)))
  ...                                        | inl idp | inl idp | inr t≠t' = inr λ p → t≠t' (snd (<>= p))

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
------------------------------------------------------------------------
-- A sound, inductive approximation of stream equality
------------------------------------------------------------------------

-- The point of this module is to give a short (not entirely faithful)
-- illustration of the technique used to establish soundness of
-- RecursiveTypes.Subtyping.Axiomatic.Inductive._⊢_≤_ with respect to
-- RecursiveTypes.Subtyping.Axiomatic.Coinductive._≤_.

module InductiveStreamEquality {A : Set} where

open import Codata.Musical.Notation
open import Codata.Musical.Stream hiding (_∈_; lookup)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

infixr 5 _∷_
infix  4 _⊢_≈_ _≈P_ _≈W_

------------------------------------------------------------------------
-- An approximation of stream equality

-- Streams do not need to be regular, so _⊢_≈_ is not complete with
-- respect to _≈_.

data _⊢_≈_ (H : List (Stream A × Stream A)) :
           Stream A → Stream A → Set where
  _∷_   : ∀ x {xs ys} →
          (x ∷ xs , x ∷ ys) ∷ H ⊢ ♭ xs ≈ ♭ ys →
          H ⊢ x ∷ xs ≈ x ∷ ys
  hyp   : ∀ {xs ys} → (xs , ys) ∈ H → H ⊢ xs ≈ ys
  trans : ∀ {xs ys zs} → H ⊢ xs ≈ ys → H ⊢ ys ≈ zs → H ⊢ xs ≈ zs

-- Example.

repeat-refl : (x : A) → [] ⊢ repeat x ≈ repeat x
repeat-refl x = x ∷ hyp (here refl)

------------------------------------------------------------------------
-- Soundness

Valid : (Stream A → Stream A → Set) → Stream A × Stream A → Set
Valid _R_ (xs , ys) = xs R ys

-- Programs and WHNFs.

mutual

  data _≈P_ : Stream A → Stream A → Set where
    sound : ∀ {A xs ys} → All (Valid _≈W_) A → A ⊢ xs ≈ ys → xs ≈P ys
    trans : ∀ {xs ys zs} → xs ≈P ys → ys ≈P zs → xs ≈P zs

  data _≈W_ : Stream A → Stream A → Set where
    _∷_ : ∀ x {xs ys} → ∞ (♭ xs ≈P ♭ ys) → x ∷ xs ≈W x ∷ ys

transW : ∀ {xs ys zs} → xs ≈W ys → ys ≈W zs → xs ≈W zs
transW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ ♯ trans (♭ xs≈ys) (♭ ys≈zs)

soundW : ∀ {A xs ys} → All (Valid _≈W_) A → A ⊢ xs ≈ ys → xs ≈W ys
soundW valid (hyp h)             = All.lookup valid h
soundW valid (trans xs≈ys ys≈zs) = transW (soundW valid xs≈ys)
                                          (soundW valid ys≈zs)
soundW valid (x ∷ xs≈ys)         = proof
  where
  proof : _ ≈W _
  proof = x ∷ ♯ sound (proof ∷ valid) xs≈ys

whnf : ∀ {xs ys} → xs ≈P ys → xs ≈W ys
whnf (sound valid xs≈ys) = soundW valid xs≈ys
whnf (trans xs≈ys ys≈zs) = transW (whnf xs≈ys) (whnf ys≈zs)

-- The programs and WHNFs are sound with respect to _≈_.

mutual

  ⟦_⟧W : ∀ {xs ys} → xs ≈W ys → xs ≈ ys
  ⟦ x ∷ xs≈ys ⟧W = refl ∷ ♯ ⟦ ♭ xs≈ys ⟧P

  ⟦_⟧P : ∀ {xs ys} → xs ≈P ys → xs ≈ ys
  ⟦ xs≈ys ⟧P = ⟦ whnf xs≈ys ⟧W

-- The programs and WHNFs are also complete with respect to _≈_.

mutual

  completeP : ∀ {xs ys} → xs ≈ ys → xs ≈P ys
  completeP xs≈ys = sound (completeW xs≈ys ∷ []) (hyp (here refl))

  completeW : ∀ {xs ys} → xs ≈ ys → xs ≈W ys
  completeW (refl ∷ xs≈ys) = _ ∷ ♯ completeP (♭ xs≈ys)

-- Finally we get the intended soundness result for _⊢_≈_.

reallySound : ∀ {A xs ys} → All (Valid _≈_) A → A ⊢ xs ≈ ys → xs ≈ ys
reallySound valid xs≈ys =
  ⟦ sound (All.map (λ {p} → done p) valid) xs≈ys ⟧P
  where
  done : ∀ p → Valid _≈_ p → Valid _≈W_ p
  done (xs , ys) = completeW

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Support.StarEquality where

open import Categories.Support.Equivalence
open import Data.Star
import Data.Star.Properties as Props
open import Level
open import Relation.Binary
  using ( Rel
        ; Reflexive; Symmetric; Transitive
        ; IsEquivalence
        ; _=[_]⇒_)
open import Relation.Binary.PropositionalEquality
  using (_≡_)
  renaming (refl to ≡-refl)

module StarEquality {o ℓ e} {Obj : Set o} (S : Obj → Obj → Setoid ℓ e) where
  private
    open module S i j = Setoid (S i j)
      using () renaming (Carrier to T)
    _≊_ : ∀ {i j} → Rel (T i j) e
    _≊_ {i}{j} = S._≈_ i j

  infix 4 _≈_

  data _≈_ : {i₁ i₂ : Obj} → Rel (Star T i₁ i₂) (o ⊔ ℓ ⊔ e) where
    ε-cong : ∀ {i} → ε {x = i} ≈ ε {x = i}
    _◅-cong_ : {i j k : Obj}{x₁ x₂ : T i j} {xs₁ xs₂ : Star T j k}
      → x₁ ≊ x₂
      → xs₁ ≈ xs₂
      → (x₁ ◅ xs₁) ≈ (x₂ ◅ xs₂)

  _◅◅-cong_ : {i j k : Obj}{xs₁ xs₂ : Star T i j} {ys₁ ys₂ : Star T j k}
      → xs₁ ≈ xs₂
      → ys₁ ≈ ys₂
      → (xs₁ ◅◅ ys₁) ≈ (xs₂ ◅◅ ys₂)
  ε-cong         ◅◅-cong p   = p
  (p ◅-cong ps₁) ◅◅-cong ps₂ = p ◅-cong (ps₁ ◅◅-cong ps₂)

  _▻▻-cong_ : {i j k : Obj}{xs₁ xs₂ : Star T j k} {ys₁ ys₂ : Star T i j}
      → xs₁ ≈ xs₂
      → ys₁ ≈ ys₂
      → (xs₁ ▻▻ ys₁) ≈ (xs₂ ▻▻ ys₂)
  x ▻▻-cong y = y ◅◅-cong x

  private
    .refl : ∀ {i j} → Reflexive (_≈_ {i}{j})
    refl {x = ε} = ε-cong
    refl {x = x ◅ xs} = S.refl _ _ ◅-cong refl

    .sym : ∀ {i j} → Symmetric (_≈_ {i}{j})
    sym ε-cong = ε-cong
    sym (px ◅-cong pxs) = S.sym _ _ px ◅-cong sym pxs

    .trans : ∀ {i j} → Transitive (_≈_ {i}{j})
    trans ε-cong ε-cong = ε-cong
    trans (px₁ ◅-cong pxs₁) (px₂ ◅-cong pxs₂)
      = S.trans _ _ px₁ px₂ ◅-cong trans pxs₁ pxs₂

  .isEquivalence : ∀ {i j} → IsEquivalence (_≈_ {i}{j})
  isEquivalence = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }

  private
    .reflexive : ∀ {i j} {x y : Star T i j} → x ≡ y → x ≈ y
    reflexive ≡-refl = refl

  StarSetoid : ∀ i j → Setoid (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
  StarSetoid i j = record
    { Carrier       = Star T i j
    ; _≈_           = _≈_
    ; isEquivalence = isEquivalence
    }

  .◅◅-assoc : {A B C D : Obj} (f : Star T A B) (g : Star T B C) (h : Star T C D)
    → ((f ◅◅ g) ◅◅ h) ≈ (f ◅◅ (g ◅◅ h))
  ◅◅-assoc f g h = reflexive (Props.◅◅-assoc f g h)

  .▻▻-assoc : {A B C D : Obj} (f : Star T A B) (g : Star T B C) (h : Star T C D)
    → ((h ▻▻ g) ▻▻ f) ≈ (h ▻▻ (g ▻▻ f))
  ▻▻-assoc f g h = sym (◅◅-assoc f g h)

open StarEquality public using (StarSetoid)

-- congruences involving Star lists of 2 relations
module StarCong₂ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
  {I : Set o₁} (T-setoid : I → I → Setoid ℓ₁ e₁)
  {J : Set o₂} (U-setoid : J → J → Setoid ℓ₂ e₂)

  where
    private
      module T i j = Setoid (T-setoid i j)
      T : Rel I ℓ₁
      T = T.Carrier
      _≊₁_ : ∀ {i j} → Rel (T i j) e₁
      _≊₁_ {i}{j} = T._≈_ i j
      module T* i j = Setoid (StarSetoid T-setoid i j)
      _≈₁_ : ∀ {i j} → Rel (Star T i j) (o₁ ⊔ ℓ₁ ⊔ e₁)
      _≈₁_ {i}{j} = T*._≈_ i j
      open StarEquality T-setoid
        using ()
        renaming (ε-cong to ε-cong₁; _◅-cong_ to _◅-cong₁_)

      module U i j = Setoid (U-setoid i j)
      U : Rel J ℓ₂
      U = U.Carrier
      _≊₂_ : ∀ {i j} → Rel (U i j) e₂
      _≊₂_ {i}{j} = U._≈_ i j
      module U* i j = Setoid (StarSetoid U-setoid i j)
      _≈₂_ : ∀ {i j} → Rel (Star U i j) (o₂ ⊔ ℓ₂ ⊔ e₂)
      _≈₂_ {i}{j} = U*._≈_ i j
      open StarEquality U-setoid
        using ()
        renaming (ε-cong to ε-cong₂; _◅-cong_ to _◅-cong₂_)

    gmap-cong : (f : I → J) (g : T =[ f ]⇒ U) (g′ : T =[ f ]⇒ U)
              → (∀ {i j} (x y : T i j) → x ≊₁ y → g x ≊₂ g′ y)
              → ∀ {i j} (xs ys : Star T i j)
              → xs ≈₁ ys
              → gmap {U = U} f g xs ≈₂ gmap f g′ ys
    gmap-cong f g g′ eq ε .ε ε-cong₁ = ε-cong₂
    gmap-cong f g g′ eq (x ◅ xs) (y ◅ ys) (x≊y ◅-cong₁ xs≈ys)
      = (eq x y x≊y) ◅-cong₂ (gmap-cong f g g′ eq xs ys xs≈ys)
    gmap-cong f g g′ eq (x ◅ xs) ε ()

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module LC.Confluence where

open import LC.Base
open import LC.Subst
open import LC.Reduction

open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

β→confluent : ∀ {M N O : Term} → (M β→ N) → (M β→ O) → ∃ (λ P → (N β→* P) × (O β→* P))
β→confluent (β-ƛ-∙ {M} {N}) β-ƛ-∙ = M [ N ] , ε , ε
β→confluent (β-ƛ-∙ {M} {N}) (β-∙-l {N = _} (β-ƛ {N = O} M→O)) = (O [ N ]) , cong-[]-l M→O , return β-ƛ-∙
β→confluent (β-ƛ-∙ {M} {N}) (β-∙-r {N = O} N→O) = M [ O ] , cong-[]-r M N→O , return β-ƛ-∙
β→confluent (β-ƛ M→N) (β-ƛ M→O) with β→confluent M→N M→O
... | P , N→P , O→P = ƛ P , cong-ƛ N→P , cong-ƛ O→P
β→confluent (β-∙-l {L} (β-ƛ {N = N} M→N)) β-ƛ-∙ = N [ L ] , return β-ƛ-∙ , cong-[]-l M→N
β→confluent (β-∙-l {L} M→N) (β-∙-l  M→O) with β→confluent M→N M→O
... | P , N→P , O→P = P ∙ L , cong-∙-l N→P , cong-∙-l O→P
β→confluent (β-∙-l {N = N} M→N) (β-∙-r {N = O} L→O) = N ∙ O , cong-∙-r (return L→O) , cong-∙-l (return M→N)
β→confluent (β-∙-r {N = N} M→N) (β-ƛ-∙ {O}) = O [ N ] , return β-ƛ-∙ , cong-[]-r O M→N
β→confluent (β-∙-r {N = N} M→N) (β-∙-l {N = O} L→O) = O ∙ N , cong-∙-l (return L→O) , cong-∙-r (return M→N)
β→confluent (β-∙-r {L} {M} {N} M→N) (β-∙-r {N = O} M→O) with β→confluent M→N M→O
... | P , N→P , O→P = L ∙ P , cong-∙-r N→P , cong-∙-r O→P

-- β→*-confluent : ∀ {M N O} → (M β→* N) → (M β→* O) → ∃ (λ P → (N β→* P) × (O β→* P))
-- β→*-confluent {O = O} ε M→O = O , M→O , ε
-- β→*-confluent {N = N} M→N ε = N , ε , M→N
-- β→*-confluent {M} {N} {O} (_◅_ {j = L} M→L L→N) (_◅_ {j = K} M→K K→O) with β→confluent M→L M→K
-- ... | M' , L→M'  , K→M' = {!   !}

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
-- This module closely follows a section of Martín Escardó's HoTT lecture notes:
-- https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#funextfromua
{-# OPTIONS --without-K #-}
module Util.HoTT.FunctionalExtensionality where

open import Axiom.Extensionality.Propositional using
  (ExtensionalityImplicit ; implicit-extensionality)

open import Util.Data.Product using (map₂)
open import Util.HoTT.Equiv
open import Util.HoTT.Equiv.Induction
open import Util.HoTT.HLevel.Core
open import Util.HoTT.Homotopy
open import Util.HoTT.Section
open import Util.HoTT.Singleton
open import Util.HoTT.Univalence
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using (Σ-≡⁻)

private
  variable
    α β γ : Level
    A B C : Set α

FunextNondep : ∀ α β → Set (lsuc (α ⊔ℓ β))
FunextNondep α β
  = {A : Set α} {B : Set β} {f g : A → B} → (∀ a → f a ≡ g a) → f ≡ g

IsContr-∀-Closure : ∀ α β → Set (lsuc (α ⊔ℓ β))
IsContr-∀-Closure α β
  = {A : Set α} {B : A → Set β} → (∀ a → IsContr (B a)) → IsContr (∀ a → B a)

FunextHapply : ∀ α β → Set (lsuc (α ⊔ℓ β))
FunextHapply α β
  = {A : Set α} {B : A → Set β} (f g : ∀ a → B a) → IsEquiv (≡→~ {f = f} {g})

Funext : ∀ α β → Set (lsuc (α ⊔ℓ β))
Funext α β
  = {A : Set α} {B : A → Set β} {f g : ∀ a → B a} → (∀ a → f a ≡ g a) → f ≡ g

abstract
  precomp-IsEquiv : {A B : Set α} (f : A → B)
    → IsEquiv f
    → {C : Set α}
    → IsEquiv (λ (g : B → C) → g ∘ f)
  precomp-IsEquiv f f-equiv {C}
    = J-IsEquiv (λ A B f → IsEquiv (λ (g : B → C) → g ∘ f)) (λ A → id-IsEquiv) f
        f-equiv

  funext-nondep : FunextNondep α β
  funext-nondep {α} {β} {A} {B} {f} {g} f~g
    = cong (λ π x → π (f x , g x , f~g x)) π₀≡π₁
    where
      Δ : Set β
      Δ = Σ[ b ∈ B ] Σ[ b′ ∈ B ] (b ≡ b′)

      δ : B → Δ
      δ b = b , b , refl

      π₀ π₁ : Δ → B
      π₀ (b , b′ , p) = b
      π₁ (b , b′ , p) = b′

      δ-IsEquiv : IsEquiv δ
      δ-IsEquiv = IsIso→IsEquiv record
        { back = π₀
        ; back∘forth = λ _ → refl
        ; forth∘back = λ { (b , b′ , refl) → refl }
        }

      φ : (Δ → B) → (B → B)
      φ = _∘ δ

      φ-IsEquiv : IsEquiv φ
      φ-IsEquiv = precomp-IsEquiv δ δ-IsEquiv

      φπ₀≡φπ₁ : φ π₀ ≡ φ π₁
      φπ₀≡φπ₁ = refl

      π₀≡π₁ : π₀ ≡ π₁
      π₀≡π₁ = IsEquiv→Injective φ-IsEquiv φπ₀≡φπ₁

  postcomp-IsIso : {A : Set α} {B : Set β} (f : B → C)
    → IsIso f
    → IsIso (λ (g : A → B) → f ∘ g)
  postcomp-IsIso {A = A} {B} f i = record
    { back = λ g a → i .IsIso.back (g a)
    ; back∘forth = λ g → funext-nondep λ a → i .IsIso.back∘forth (g a)
    ; forth∘back = λ g → funext-nondep λ a → i .IsIso.forth∘back (g a)
    }

  postcomp-IsEquiv : {A : Set α} {B : Set β} (f : B → C)
    → IsEquiv f
    → IsEquiv (λ (g : A → B) → f ∘ g)
  postcomp-IsEquiv f f-equiv
    = IsIso→IsEquiv (postcomp-IsIso f (IsEquiv→IsIso f-equiv))

  ∀-IsContr : IsContr-∀-Closure α β
  ∀-IsContr {A = A} {B} B-contr = ◁-pres-IsContr ΠB◁g-fiber g-fiber-IsContr
    where
      f : Σ A B → A
      f = proj₁

      f-IsEquiv : IsEquiv f
      f-IsEquiv = proj₁-IsEquiv B-contr

      g : (A → Σ A B) → (A → A)
      g = f ∘_

      g-IsEquiv : IsEquiv g
      g-IsEquiv = postcomp-IsEquiv f f-IsEquiv

      g-fiber-IsContr : IsContr (Σ[ h ∈ (A → Σ A B) ] (f ∘ h ≡ id))
      g-fiber-IsContr = g-IsEquiv id

      ΠB◁g-fiber : (∀ a → B a) ◁ (Σ[ h ∈ (A → Σ A B) ] (f ∘ h ≡ id))
      ΠB◁g-fiber = record
        { retraction = λ { (h , p) a → subst B (≡→~ p a) (proj₂ (h a)) }
        ; hasSection = record
          { section = λ h → (λ a → a , h a) , refl
          ; isSection = λ _ → refl
          }
        }

  ≡→~-IsEquiv : FunextHapply α β
  ≡→~-IsEquiv {A = A} {B} f = goal
    where
      i : ∀ a → IsContr (Σ[ b ∈ B a ] (f a ≡ b))
      i a = IsContr-Singleton′

      ii : IsContr (∀ a → Σ[ b ∈ B a ] (f a ≡ b))
      ii = ∀-IsContr i

      iii : (∃[ g ] (f ~ g)) ◁ (∀ a → Σ[ b ∈ B a ] (f a ≡ b))
      iii = ≅→▷ (Π-distr-Σ-≅ _ _ _)

      iv : IsContr (∃[ g ] (f ~ g))
      iv = ◁-pres-IsContr iii ii

      e : (∃[ g ] (f ≡ g)) → (∃[ g ] (f ~ g))
      e = map₂ (λ _ → ≡→~)

      e-IsEquiv : IsEquiv e
      e-IsEquiv = IsContr→IsEquiv IsContr-Singleton′ iv e

      goal : ∀ g → IsEquiv (≡→~ {f = f} {g})
      goal = IsEquiv-map₂-f→IsEquiv-f (λ _ → ≡→~) e-IsEquiv

funext : Funext α β
funext {f = f} {g} eq = ≡→~-IsEquiv f g eq .proj₁ .proj₁

funext∙ : ExtensionalityImplicit α β
funext∙ = implicit-extensionality funext

module _ {α β} {A : Set α} {B : A → Set β} {f g : ∀ a → B a} where

  ≡→~∘funext : (eq : ∀ a → f a ≡ g a)
    → ≡→~ (funext eq) ≡ eq
  ≡→~∘funext eq = ≡→~-IsEquiv f g eq .proj₁ .proj₂

  funext-unique′ : ∀ eq
    → (y : Σ-syntax (f ≡ g) (λ p → ≡→~ p ≡ eq))
    → (funext eq , ≡→~∘funext eq) ≡ y
  funext-unique′ eq = ≡→~-IsEquiv f g eq .proj₂

  funext-unique : ∀ eq (p : f ≡ g)
    → ≡→~ p ≡ eq
    → funext eq ≡ p
  funext-unique eq p q = proj₁ (Σ-≡⁻ (funext-unique′ eq (p , q)))

  funext∘≡→~ : ∀ (eq : f ≡ g)
    → funext (≡→~ eq) ≡ eq
  funext∘≡→~ eq = funext-unique (≡→~ eq) eq refl

subst-funext : ∀ {α β γ} {A : Set α} {B : A → Set β} {f g : ∀ a → B a}
  → (P : ∀ a → B a → Set γ)
  → (f≡g : ∀ x → f x ≡ g x)
  → ∀ {a} (Pf : P a (f a))
  → subst (λ f → P a (f a)) (funext f≡g) Pf ≡ subst (P a) (f≡g a) Pf
subst-funext P f≡g {a} Pf = sym
  (trans
    (cong (λ p → subst (P a) (p a) Pf) (sym (≡→~∘funext f≡g)))
    go)
  where
    go : subst (P a) (≡→~ (funext f≡g) a) Pf
        ≡ subst (λ f → P a (f a)) (funext f≡g) Pf
    go with funext f≡g
    ... | refl = refl

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
open import Prelude

module Nat where
  data Nat : Set where
    Z : Nat
    1+ : Nat → Nat

  {-# BUILTIN NATURAL Nat #-}

  -- the succ operation is injective
  1+inj : (x y : Nat) → (1+ x == 1+ y) → x == y
  1+inj Z .0 refl = refl
  1+inj (1+ x) .(1+ x) refl = refl

  -- equality of naturals is decidable. we represent this as computing a
  -- choice of units, with inl <> meaning that the naturals are indeed the
  -- same and inr <> that they are not.
  natEQ : (x y : Nat) → ((x == y) + ((x == y) → ⊥))
  natEQ Z Z = Inl refl
  natEQ Z (1+ y) = Inr (λ ())
  natEQ (1+ x) Z = Inr (λ ())
  natEQ (1+ x) (1+ y) with natEQ x y
  natEQ (1+ x) (1+ .x) | Inl refl = Inl refl
  ... | Inr b = Inr (λ x₁ → b (1+inj x y x₁))

  -- nat equality as a predicate. this saves some very repetetive casing.
  natEQp : (x y : Nat) → Set
  natEQp x y with natEQ x y
  natEQp x .x | Inl refl = ⊥
  natEQp x y | Inr x₁ = ⊤

  _nat+_ : Nat → Nat → Nat
  Z nat+ y = y
  1+ x nat+ y = 1+ (x nat+ y)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

open import HoTT

module homotopy.PathSetIsInitalCover {i} (X : Ptd i)
    -- and an arbitrary covering
    {k} (⊙cov : ⊙Cover X k) where

  open Cover

  private
    univ-cover = path-set-cover X
    module ⊙cov = ⊙Cover ⊙cov

  -- Weak initiality by transport.
  quotient-cover : CoverHom univ-cover ⊙cov.cov
  quotient-cover _ p = cover-trace ⊙cov.cov ⊙cov.pt p

  -- Strong initiality by path induction.
  module Uniqueness
    (cover-hom : CoverHom univ-cover ⊙cov.cov)
    (pres-pt : cover-hom (pt X) idp₀ == ⊙cov.pt)
    where

    private
      lemma₁ : ∀ a p → cover-hom a [ p ] == quotient-cover a [ p ]
      lemma₁ ._ idp = pres-pt

      lemma₂ : ∀ a p → cover-hom a p == quotient-cover a p
      lemma₂ a = Trunc-elim
        (λ p → =-preserves-set (⊙cov.Fiber-level a))
        (lemma₁ a)

    theorem : cover-hom == quotient-cover
    theorem = λ= λ a → λ= $ lemma₂ a

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.FiniteDimensional.Proofs
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Data.Tuple as Tuple using (_,_)
open import Functional using (id ; _∘_ ; _∘₂_ ; _$_ ; swap ; _on₂_)
open import Function.Equals
open import Logic
open import Logic.Classical
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.CoordinateVector.Proofs
open import Numeral.Finite
open import Numeral.Finite.Proofs
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
import      Relator.Equals as Eq
open import Relator.Equals.Proofs.Equivalence
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Operator.Proofs
open import Structure.Operator
open import Structure.Operator.Vector.FiniteDimensional        ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Operator.Vector.LinearCombination        ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Operator.Vector.LinearCombination.Proofs
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Number
open import Syntax.Transitivity

private variable ℓ ℓ₁ ℓ₂ ℓₗ : Lvl.Level
private variable n n₁ n₂ : ℕ

private variable vf vf₁ vf₂ : Vec(n)(V)
private variable sf sf₁ sf₂ : Vec(n)(S)
private variable i j : 𝕟(n)

-- A basis could essentially be defined as being linearly independent and spanning the vector space.
linearIndependence-spanning-basis-equivalence : (LinearlyIndependent(vf) ∧ Spanning(vf)) ↔ Basis(vf)
linearIndependence-spanning-basis-equivalence = injective-surjective-bijective-equivalence _

-- Linearly independent sequence of vectors are vectors such that a linear combination of them never maps to zero.
-- Note that this is the usual definition of linear independence.
linearIndependence-equivalence : LinearlyIndependent(vf) ↔ (∀{sf} → (linearCombination(vf)(sf) ≡ 𝟎ᵥ) → (sf ⊜ Vec.fill(𝟎ₛ)))
linearIndependence-equivalence =
  Two.injective-kernel
    {_▫₁_ = Vec.map₂(_+ₛ_)}
    ⦃ func = BinaryOperator.right linearCombination-binaryOperator ⦄
    ⦃ cancₗ₂ = One.cancellationₗ-by-associativity-inverse ⦄
    {inv₁ = Vec.map(−ₛ_)}

-- postulate linearCombination-when-zero : (linearCombination(vf)(sf) ≡ 𝟎ᵥ) → (∀{i} → (vf(i) ≡ 𝟎ᵥ) ∨ (sf(i) ≡ 𝟎ₛ))

-- A sequence of vectors with a zero vector in it are not linearly independent, and a linearly independent sequence of vectors do not contain zero vectors.
linearIndependence-no-zero-vectors : LinearlyIndependent(vf) → ∀{i} → (vf(i) ≡ 𝟎ᵥ) → ⊥
linearIndependence-no-zero-vectors {𝐒(n)}{vf} li {i} vfzero = distinct-identitiesₛ $
  𝟎ₛ                         🝖[ _≡_ ]-[]
  Vec.fill 𝟎ₛ i              🝖[ _≡_ ]-[ _⊜_.proof ([↔]-to-[→] linearIndependence-equivalence li p) ]-sym
  Vec.indexProject i 𝟏ₛ 𝟎ₛ i 🝖[ _≡_ ]-[ [↔]-to-[→] (indexProject-true{i = i}{false = 𝟎ₛ}) ([∨]-introₗ(reflexivity(Eq._≡_))) ]
  𝟏ₛ                         🝖-end
  where
    p =
      linearCombination vf (Vec.indexProject i 𝟏ₛ 𝟎ₛ) 🝖[ _≡_ ]-[ linearCombination-of-indexProject{vf = vf} ]
      vf(i)                                           🝖[ _≡_ ]-[ vfzero ]
      𝟎ᵥ                                              🝖-end

--∀{i} → (vf(i) ≡ 𝟎ᵥ) → Spanning{𝐒(n)}(vf) → Spanning{n}(Vec.without i vf)

-- There are no duplicates in a sequence of linearly independent vectors.
linearIndependence-to-distinct : LinearlyIndependent(vf) → Vec.Distinct(vf)
Injective.proof (linearIndependence-to-distinct {vf = vf} (intro inj)) {x} {y} vfxy = [¬¬]-elim ⦃ [≡][𝕟]-classical ⦄ $ nxy ↦
  let
    p : linearCombination vf (Vec.indexProject x 𝟏ₛ 𝟎ₛ) ≡ linearCombination vf (Vec.indexProject y 𝟏ₛ 𝟎ₛ)
    p =
      linearCombination vf (Vec.indexProject x 𝟏ₛ 𝟎ₛ) 🝖[ _≡_ ]-[ linearCombination-of-indexProject{vf = vf} ]
      vf(x)                                           🝖[ _≡_ ]-[ vfxy ]
      vf(y)                                           🝖[ _≡_ ]-[ linearCombination-of-indexProject{vf = vf} ]-sym
      linearCombination vf (Vec.indexProject y 𝟏ₛ 𝟎ₛ) 🝖-end

    q : 𝟎ₛ ≡ 𝟏ₛ
    q =
      𝟎ₛ                                      🝖[ _≡_ ]-[ [↔]-to-[→] (indexProject-false{true = 𝟏ₛ}) ([∨]-introₗ nxy) ]-sym
      Vec.proj(Vec.indexProject(x) 𝟏ₛ 𝟎ₛ) (y) 🝖[ _≡_ ]-[ _⊜_.proof(inj p) {y} ]
      Vec.proj(Vec.indexProject(y) 𝟏ₛ 𝟎ₛ) (y) 🝖[ _≡_ ]-[ [↔]-to-[→] (indexProject-true{false = 𝟎ₛ}) ([∨]-introₗ(reflexivity(Eq._≡_) {x = y})) ]
      𝟏ₛ                                      🝖-end
  in distinct-identitiesₛ q

-- A subsequence of a linearly independent sequence of vectors are linearly independent.
postulate independent-subsequence-is-independent : ∀{N : 𝕟(n₁) → 𝕟(n₂)} ⦃ inj : Injective ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (N) ⦄ → LinearlyIndependent{n₂}(vf) → LinearlyIndependent{n₁}(vf ∘ N)

postulate linear-independent-sequence-set-equivalence : ∀{N : 𝕟(n₁) → 𝕟(n₂)} ⦃ bij : Bijective ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (N)⦄ → LinearlyIndependent{n₂}(vf) ↔ LinearlyIndependent{n₁}(vf ∘ N)

postulate spanning-supersequence-is-spanning : ∀{N : 𝕟(n₁) → 𝕟(n₂)} ⦃ surj : Surjective ⦃ [≡]-equiv ⦄ (N) ⦄ → Spanning{n₂}(vf) → Spanning{n₁}(vf ∘ N)

postulate spanning-sequence-set-equivalence : ∀{N : 𝕟(n₁) → 𝕟(n₂)} ⦃ bij : Bijective ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (N) ⦄ → Spanning{n₂}(vf) ↔ Spanning{n₁}(vf ∘ N)

-- The number of linearly independent vectors is always less than the cardinality of a set of spanning vectors.
-- TODO: It is important to prove this if possible
postulate independent-less-than-spanning : ∀{n₁}{vf₁} → LinearlyIndependent{n₁}(vf₁) → ∀{n₂}{vf₂} → Spanning{n₂}(vf₂) → (n₁ ≤ n₂)
{- TODO: Here is an idea of a proof, but it probably requires more development in the theory of cardinalities. Or maybe just some stuff on linearCombination
  LinearlyIndependent{n₁}(vf₁)
  Injective(linearCombination{n = n₁}(vf₁)) (essentially: Vec(n₁)(S) ≤ V)

  Spanning{n₂}(vf₂)
  Surjective(linearCombination{n = n₂}(vf₂)) (essentially: Vec(n₂)(S) ≥ V)
  Injective(linearCombination{n = n₂}(vf₂) ∘ inv) (Is this really true then? Essentially: V ≤ Vec(n₂)(S))

  Injective(linearCombination{n = n₂}(vf₂) ∘ inv ∘ linearCombination{n = n₁}(vf₁)) (essentially: Vec(n₁)(S) ≤ Vec(n₂)(S))
  n₁ ≤ n₂ (Note: This is not true in general. Only if the morphism is the "natural one" (the 𝟎 ↦ 𝟎 and n-tuples only maps to n-tuples and so on)), but is it really obtained by the proofs above?
-}

-- Two bases in a vector space are always of the same length.
basis-equal-length : Basis{n₁}(vf₁) → Basis{n₂}(vf₂) → (n₁ Eq.≡ n₂)
basis-equal-length b₁ b₂
  with (li₁ , sp₁) ← [↔]-to-[←] linearIndependence-spanning-basis-equivalence b₁
  |    (li₂ , sp₂) ← [↔]-to-[←] linearIndependence-spanning-basis-equivalence b₂
  = antisymmetry(_≤_)(Eq._≡_) (independent-less-than-spanning li₁ sp₂) (independent-less-than-spanning li₂ sp₁)

-- A finite basis can always be constructed by a subsequence of a finite spanning sequence of vectors.
-- TODO: One way of proving this is by assuming that the relation LinearlyIndependent is decidable (it is because of the isomorphism from matrices (all vector spaces of the same dimension are isomorphic) and then matrix operations can tell whether a set of finite vectors are decidable), and then remove vectors one by one from the spanning sequence until it is linearly independent (which it will be at the end. In extreme cases, a sequence of zero vectors are linearly independent). This algorithm will always terminate because all vectors are finite, but how will this be shown?
postulate basis-subsequence-from-spanning : Spanning{n₂}(vf) → ∃(n₁ ↦ ∃{Obj = 𝕟(n₁) → 𝕟(n₂)}(N ↦ Injective ⦃ [≡]-equiv ⦄ ⦃ [≡]-equiv ⦄ (N) ∧ Basis{n₁}(vf ∘ N)))

module _ ⦃ fin-dim@([∃]-intro(spanSize) ⦃ [∃]-intro span ⦃ span-spanning ⦄ ⦄) : FiniteDimensional ⦄ where
  -- A basis always exists for finite dimensional vector spaces.
  basis-existence : ∃(n ↦ ∃(vf ↦ Basis{n}(vf)))
  basis-existence
    with [∃]-intro(n) ⦃ [∃]-intro N ⦃ [∧]-intro inj basis ⦄ ⦄ ← basis-subsequence-from-spanning span-spanning
    = [∃]-intro(n) ⦃ [∃]-intro (span ∘ N) ⦃ basis ⦄ ⦄

  -- The dimension of the vector space is the length of a basis, which are the same for every vector space.
  dim : ℕ
  dim = [∃]-witness basis-existence

  postulate basis-supersequence-from-linear-independence : LinearlyIndependent{n₂}(vf) → ∃(n₁ ↦ ∃{Obj = 𝕟(n₁) → 𝕟(n₂)}(N ↦ Surjective ⦃ [≡]-equiv ⦄ (N) ∧ Basis{n₁}(vf ∘ N)))
  -- TODO: One idea is to start with vf. Then try to add the basis vectors one by one from basis-existence while maintaining the linear independence

  postulate independence-spanning-equivalence-for-dimension : LinearlyIndependent{dim}(vf) ↔ Spanning{dim}(vf)

-- TODO: For this to be formulated, reorganize some stuff
-- finite-subspace-set-equality : ∀{Vₛ₁ Vₛ₂} → Subspace(Vₛ₁) → Subspace(Vₛ₂) → (dim(Vₛ₁) ≡ dim(Vₛ₂)) → (Vₛ₁ ≡ Vₛ₂) -- as in set equality

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:
{-# OPTIONS --without-K --safe #-}

open import Categories.Category

module Categories.Diagram.Pushout {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level

private
  variable
    A B X Y Z : Obj
    h h₁ h₂ j : A ⇒ B

record Pushout (f : X ⇒ Y) (g : X ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
  field
    {Q} : Obj
    i₁  : Y ⇒ Q
    i₂  : Z ⇒ Q

  field
    commute   : i₁ ∘ f ≈ i₂ ∘ g
    universal : h₁ ∘ f ≈ h₂ ∘ g → Q ⇒ cod h₁
    unique    : ∀ {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                  j ∘ i₁ ≈ h₁ → j ∘ i₂ ≈ h₂ →
                  j ≈ universal eq

    universal∘i₁≈h₁  : ∀ {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₁ ≈ h₁
    universal∘i₂≈h₂  : ∀ {eq : h₁ ∘ f ≈ h₂ ∘ g} →
                         universal eq ∘ i₂ ≈ h₂

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module L.Base where

-- Reexport definitions
open import L.Base.Sigma public
open import L.Base.Coproduct public renaming (_+_ to _⊎_)
open import L.Base.Empty public
open import L.Base.Unit public
open import L.Base.Nat public
open import L.Base.Id public

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
open import Level
open import Relation.Binary.PropositionalEquality
open import Relation.Binary using (Setoid)
import Function.Equality
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category
import Categories.Functor
import Categories.Category.Instance.Setoids

import Categories.Category.Cocartesian

import SecondOrder.Arity
import SecondOrder.Signature
import SecondOrder.Metavariable
import SecondOrder.Term

module SecondOrder.VRenaming
  {ℓ}
  {𝔸 : SecondOrder.Arity.Arity}
  (Σ : SecondOrder.Signature.Signature ℓ 𝔸)
  where

  open SecondOrder.Signature.Signature Σ
  open SecondOrder.Metavariable Σ
  open SecondOrder.Term Σ

  -- a renaming maps variables between contexts in a type-preserving way
  _⇒ᵛ_ : ∀ (Γ Δ : VContext) → Set ℓ
  Γ ⇒ᵛ Δ = ∀ {A} → A ∈ Γ → A ∈ Δ

  infix 4 _⇒ᵛ_

  -- equality of renamings

  _≡ᵛ_ : ∀ {Γ Δ} (σ τ : Γ ⇒ᵛ Δ) → Set ℓ
  _≡ᵛ_ {Γ} σ τ = ∀ {A} (x : A ∈ Γ) → σ x ≡ τ x

  infixl 3 _≡ᵛ_

  ≡ᵛ-refl : ∀ {Γ Δ} {ρ : Γ ⇒ᵛ Δ} → ρ ≡ᵛ ρ
  ≡ᵛ-refl = λ x → refl

  ≡ᵛ-sym : ∀ {Γ Δ} {ρ ν : Γ ⇒ᵛ Δ}
          → ρ ≡ᵛ ν
          → ν ≡ᵛ ρ
  ≡ᵛ-sym eq x = sym (eq x)

  ≡ᵛ-trans : ∀ {Γ Δ} {ρ ν γ : Γ ⇒ᵛ Δ}
           → ρ ≡ᵛ ν
           → ν ≡ᵛ γ
           → ρ ≡ᵛ γ
  ≡ᵛ-trans eq1 eq2 x = trans (eq1 x) (eq2 x)

  -- renamings form a setoid

  renaming-setoid : ∀ (Γ Δ : VContext) → Setoid ℓ ℓ
  renaming-setoid Γ Δ =
    record
      { Carrier = Γ ⇒ᵛ Δ
      ;  _≈_ = λ ρ ν → ρ ≡ᵛ ν
      ; isEquivalence =
                      record
                        { refl = λ {ρ} x → ≡ᵛ-refl {Γ} {Δ} {ρ} x
                        ; sym = ≡ᵛ-sym
                        ; trans = ≡ᵛ-trans
                        }
      }

  -- renaming preserves equality of variables
  ρ-resp-≡ : ∀ {Γ Δ A} {x y : A ∈ Γ} {ρ : Γ ⇒ᵛ Δ} → x ≡ y → ρ x ≡ ρ y
  ρ-resp-≡ refl = refl

  -- the identity renaming

  idᵛ : ∀ {Γ : VContext} → Γ ⇒ᵛ Γ
  idᵛ x = x

  -- composition of renamings
  _∘ᵛ_ : ∀ {Γ Δ Ξ} → Δ ⇒ᵛ Ξ → Γ ⇒ᵛ Δ → Γ ⇒ᵛ Ξ
  (σ ∘ᵛ ρ) x = σ (ρ x)

  infix 7 _∘ᵛ_

  -- composition respects equality
  ∘ᵛ-resp-≡ᵛ : ∀ {Γ Δ Ξ} {τ₁ τ₂ : Δ ⇒ᵛ Ξ} {σ₁ σ₂ : Γ ⇒ᵛ Δ} →
                 τ₁ ≡ᵛ τ₂ → σ₁ ≡ᵛ σ₂ → τ₁ ∘ᵛ σ₁ ≡ᵛ τ₂ ∘ᵛ σ₂
  ∘ᵛ-resp-≡ᵛ {τ₁ = τ₁} {σ₂ = σ₂} ζ ξ x = trans (cong τ₁ (ξ x)) (ζ (σ₂ x))

  -- the identity is the unit

  identity-leftᵛ : ∀ {Γ Δ} {ρ : Γ ⇒ᵛ Δ} → idᵛ ∘ᵛ ρ ≡ᵛ ρ
  identity-leftᵛ ρ = refl

  identity-rightᵛ : ∀ {Γ Δ} {ρ : Γ ⇒ᵛ Δ} → ρ ∘ᵛ idᵛ ≡ᵛ ρ
  identity-rightᵛ ρ = refl

  -- composition is associative

  assocᵛ : ∀ {Γ Δ Ξ Ψ} {τ : Γ ⇒ᵛ Δ} {ρ : Δ ⇒ᵛ Ξ} {σ : Ξ ⇒ᵛ Ψ} →
             (σ ∘ᵛ ρ) ∘ᵛ τ ≡ᵛ σ ∘ᵛ (ρ ∘ᵛ τ)
  assocᵛ x = refl

  sym-assocᵛ : ∀ {Γ Δ Ξ Ψ} {τ : Γ ⇒ᵛ Δ} {ρ : Δ ⇒ᵛ Ξ} {σ : Ξ ⇒ᵛ Ψ} →
             σ ∘ᵛ (ρ ∘ᵛ τ) ≡ᵛ (σ ∘ᵛ ρ) ∘ᵛ τ
  sym-assocᵛ x = refl

  -- contexts and renamings form a category
  module _ where
    open Categories.Category

    VContexts : Category ℓ ℓ ℓ
    VContexts =
      record
        { Obj = VContext
        ; _⇒_ = _⇒ᵛ_
        ; _≈_ = _≡ᵛ_
        ; id = idᵛ
        ; _∘_ = _∘ᵛ_
        ; assoc = λ {_} {_} {_} {_} {f} {g} {h} {_} → assocᵛ {τ = f} {ρ = g} {σ = h}
        ; sym-assoc = λ {_} {_} {_} {_} {f} {g} {h} {_} → sym-assocᵛ {τ = f} {ρ = g} {σ = h}
        ; identityˡ = λ x → refl
        ; identityʳ = λ x → refl
        ; identity² = λ x → refl
        ; equiv = record { refl = λ {ρ} {_} → ≡ᵛ-refl {ρ = ρ} ; sym = ≡ᵛ-sym ; trans = ≡ᵛ-trans }
        ; ∘-resp-≈ = ∘ᵛ-resp-≡ᵛ
        }

  -- the coproduct structure of the category
  module _ where

    infixl 7 [_,_]ᵛ

    [_,_]ᵛ : ∀ {Γ Δ Ξ} → Γ ⇒ᵛ Ξ → Δ ⇒ᵛ Ξ → Γ ,, Δ ⇒ᵛ Ξ
    [ σ , τ ]ᵛ (var-inl x) = σ x
    [ σ , τ ]ᵛ (var-inr y) = τ y

    [,]ᵛ-resp-≡ᵛ : ∀ {Γ Δ Ξ} {ρ₁ ρ₂ : Γ ⇒ᵛ Ξ} {τ₁ τ₂ : Δ ⇒ᵛ Ξ} → ρ₁ ≡ᵛ ρ₂ → τ₁ ≡ᵛ τ₂ → [ ρ₁ , τ₁ ]ᵛ ≡ᵛ [ ρ₂ , τ₂ ]ᵛ
    [,]ᵛ-resp-≡ᵛ pρ pτ (var-inl x) = pρ x
    [,]ᵛ-resp-≡ᵛ pρ pτ (var-inr x) = pτ x

    inlᵛ : ∀ {Γ Δ} → Γ ⇒ᵛ Γ ,, Δ
    inlᵛ = var-inl

    inrᵛ : ∀ {Γ Δ} → Δ ⇒ᵛ Γ ,, Δ
    inrᵛ = var-inr

    uniqueᵛ : ∀ {Γ Δ Ξ} {τ : Γ ,, Δ ⇒ᵛ Ξ} {ρ : Γ ⇒ᵛ Ξ} {σ : Δ ⇒ᵛ Ξ}
              → τ ∘ᵛ inlᵛ ≡ᵛ ρ
              → τ ∘ᵛ inrᵛ ≡ᵛ σ
              → [ ρ , σ ]ᵛ ≡ᵛ τ
    uniqueᵛ ξ ζ (var-inl x) = sym (ξ x)
    uniqueᵛ ξ ζ (var-inr y) = sym (ζ y)

    uniqueᵛ² : ∀ {Γ Δ Ξ} {τ σ : Γ ,, Δ ⇒ᵛ Ξ}
              → τ ∘ᵛ inlᵛ ≡ᵛ σ ∘ᵛ inlᵛ
              → τ ∘ᵛ inrᵛ ≡ᵛ σ ∘ᵛ inrᵛ
              → τ ≡ᵛ σ
    uniqueᵛ² ξ ζ (var-inl x) = ξ x
    uniqueᵛ² ξ ζ (var-inr y) = ζ y

    Context-+ : Categories.Category.Cocartesian.BinaryCoproducts VContexts
    Context-+ =
      record {
        coproduct =
          λ {Γ Δ} →
          record
            { A+B = Γ ,, Δ
            ; i₁ = inlᵛ
            ; i₂ = inrᵛ
            ; [_,_] = [_,_]ᵛ
            ; inject₁ = λ x → refl
            ; inject₂ = λ x → refl
            ; unique = uniqueᵛ
            }
      }

  open Categories.Category.Cocartesian.BinaryCoproducts Context-+

  -- the renaming from the empty context

  inᵛ : ∀ {Γ} → ctx-empty ⇒ᵛ Γ
  inᵛ ()

  -- extension of a renaming is summing with identity
  ⇑ᵛ : ∀ {Γ Δ Ξ} → Γ ⇒ᵛ Δ → Γ ,, Ξ ⇒ᵛ Δ ,, Ξ
  ⇑ᵛ ρ = ρ +₁ idᵛ

  -- a renaming can also be extended on the right
  ʳ⇑ᵛ : ∀ {Γ Δ} → Γ ⇒ᵛ Δ → ∀ {Ξ} → Ξ ,, Γ ⇒ᵛ Ξ ,, Δ
  ʳ⇑ᵛ ρ = idᵛ +₁ ρ

  -- right extension of renamings commutes with right injection
  ʳ⇑ᵛ-comm-inrᵛ : ∀ {Γ Δ Ξ} (ρ : Γ ⇒ᵛ Δ)
    → (ʳ⇑ᵛ ρ {Ξ = Ξ}) ∘ᵛ (inrᵛ {Δ = Γ}) ≡ᵛ inrᵛ ∘ᵛ ρ
  ʳ⇑ᵛ-comm-inrᵛ ρ var-slot = refl
  ʳ⇑ᵛ-comm-inrᵛ ρ (var-inl x) = refl
  ʳ⇑ᵛ-comm-inrᵛ ρ (var-inr x) = refl

  -- left extension of renamings commutes with left injection
  ⇑ᵛ-comm-inlᵛ : ∀ {Γ Δ Ξ} (ρ : Γ ⇒ᵛ Δ) → (⇑ᵛ {Ξ = Ξ} ρ) ∘ᵛ (inlᵛ {Δ = Ξ}) ≡ᵛ inlᵛ ∘ᵛ ρ
  ⇑ᵛ-comm-inlᵛ ρ var-slot = refl
  ⇑ᵛ-comm-inlᵛ ρ (var-inl x) = refl
  ⇑ᵛ-comm-inlᵛ ρ (var-inr x) = refl

  -- the action of a renaming on terms
  module _ {Θ : MContext} where

    infix 6 [_]ᵛ_

    [_]ᵛ_ : ∀ {Γ Δ A} → Γ ⇒ᵛ Δ → Term Θ Γ A → Term Θ Δ A
    [ ρ ]ᵛ (tm-var x) = tm-var (ρ x)
    [ ρ ]ᵛ (tm-meta M ts) = tm-meta M (λ i → [ ρ ]ᵛ (ts i))
    [ ρ ]ᵛ (tm-oper f es) = tm-oper f (λ i → [ ⇑ᵛ ρ ]ᵛ (es i))

  -- The sum of identities is an identity
  idᵛ+idᵛ : ∀ {Γ Δ} → idᵛ {Γ = Γ} +₁ idᵛ {Γ = Δ} ≡ᵛ idᵛ {Γ = Γ ,, Δ}
  idᵛ+idᵛ (var-inl x) = refl
  idᵛ+idᵛ (var-inr y) = refl

  -- The action of a renaming respects equality of terms
  []ᵛ-resp-≈ : ∀ {Θ Γ Δ A} {s t : Term Θ Γ A} {ρ : Γ ⇒ᵛ Δ} → s ≈ t → [ ρ ]ᵛ s ≈ [ ρ ]ᵛ t
  []ᵛ-resp-≈ (≈-≡ refl) = ≈-≡ refl
  []ᵛ-resp-≈ (≈-meta ξ) = ≈-meta (λ i → []ᵛ-resp-≈ (ξ i))
  []ᵛ-resp-≈ (≈-oper ξ) = ≈-oper (λ i → []ᵛ-resp-≈ (ξ i))

  -- The action of a renaming respects equality of renamings
  []ᵛ-resp-≡ᵛ : ∀ {Θ Γ Δ A} {ρ τ : Γ ⇒ᵛ Δ} {t : Term Θ Γ A} → ρ ≡ᵛ τ → [ ρ ]ᵛ t ≈ [ τ ]ᵛ t
  []ᵛ-resp-≡ᵛ {t = tm-var x} ξ = ≈-≡ (cong tm-var (ξ x))
  []ᵛ-resp-≡ᵛ {t = tm-meta M ts} ξ = ≈-meta (λ i → []ᵛ-resp-≡ᵛ ξ)
  []ᵛ-resp-≡ᵛ {t = tm-oper f es} ξ = ≈-oper (λ i → []ᵛ-resp-≡ᵛ (+₁-cong₂ ξ ≡ᵛ-refl))

  -- The action of the identity is trival
  [idᵛ] : ∀ {Θ Γ A} {t : Term Θ Γ A} → [ idᵛ ]ᵛ t ≈ t
  [idᵛ] {t = tm-var x} = ≈-refl
  [idᵛ] {t = tm-meta M ts} = ≈-meta λ i → [idᵛ]
  [idᵛ] {t = tm-oper f es} = ≈-oper λ i → ≈-trans ([]ᵛ-resp-≡ᵛ idᵛ+idᵛ) [idᵛ]

  -- Extension respects composition
  ⇑ᵛ-resp-∘ᵛ : ∀ {Γ Δ Ξ Ψ} {ρ : Γ ⇒ᵛ Δ} {τ : Δ ⇒ᵛ Ξ} → ⇑ᵛ {Ξ = Ψ} (τ ∘ᵛ ρ) ≡ᵛ (⇑ᵛ τ) ∘ᵛ (⇑ᵛ ρ)
  ⇑ᵛ-resp-∘ᵛ (var-inl x) = refl
  ⇑ᵛ-resp-∘ᵛ (var-inr y) = refl

  -- Right extension respects composition
  ʳ⇑ᵛ-resp-∘ᵛ : ∀ {Γ Δ Ξ Ψ} {ρ : Γ ⇒ᵛ Δ} {τ : Δ ⇒ᵛ Ξ} → ʳ⇑ᵛ (τ ∘ᵛ ρ) {Ξ = Ψ} ≡ᵛ (ʳ⇑ᵛ τ) ∘ᵛ (ʳ⇑ᵛ ρ)
  ʳ⇑ᵛ-resp-∘ᵛ (var-inl x) = refl
  ʳ⇑ᵛ-resp-∘ᵛ (var-inr y) = refl

  -- The action of a renaming is functorial
  [∘ᵛ] : ∀ {Θ Γ Δ Ξ} {ρ : Γ ⇒ᵛ Δ} {τ : Δ ⇒ᵛ Ξ} {A} {t : Term Θ Γ A}
    → [ τ ∘ᵛ ρ ]ᵛ t ≈ [ τ ]ᵛ ([ ρ ]ᵛ t)
  [∘ᵛ] {t = tm-var x} = ≈-refl
  [∘ᵛ] {t = tm-meta M ts} = ≈-meta (λ i → [∘ᵛ])
  [∘ᵛ] {t = tm-oper f es} = ≈-oper (λ i → ≈-trans ([]ᵛ-resp-≡ᵛ ⇑ᵛ-resp-∘ᵛ) [∘ᵛ])

  ∘ᵛ-resp-ʳ⇑ᵛ : ∀ {Γ Δ Ξ Λ} {ρ : Γ ⇒ᵛ Δ} {τ : Δ ⇒ᵛ Ξ}
    → ʳ⇑ᵛ (τ ∘ᵛ ρ) {Ξ = Λ} ≡ᵛ ʳ⇑ᵛ τ ∘ᵛ ʳ⇑ᵛ ρ
  ∘ᵛ-resp-ʳ⇑ᵛ (var-inl x) = refl
  ∘ᵛ-resp-ʳ⇑ᵛ (var-inr y) = refl

  ∘ᵛ-resp-ʳ⇑ᵛ-term : ∀ {Θ Γ Δ Ξ Λ A} {ρ : Γ ⇒ᵛ Δ} {τ : Δ ⇒ᵛ Ξ} {t : Term Θ (Λ ,, Γ) A}
    → [ ʳ⇑ᵛ (τ ∘ᵛ ρ) {Ξ = Λ} ]ᵛ t ≈ [ ʳ⇑ᵛ τ ]ᵛ ([ ʳ⇑ᵛ ρ ]ᵛ t)
  ∘ᵛ-resp-ʳ⇑ᵛ-term {Θ} {Γ} {Δ} {Ξ} {Λ} {A} {ρ} {τ} {t = t} =
    let open SetoidR (Term-setoid Θ (Λ ,, Ξ) A) in
    begin
    [ ʳ⇑ᵛ (τ ∘ᵛ ρ) {Ξ = Λ} ]ᵛ t ≈⟨ []ᵛ-resp-≡ᵛ ∘ᵛ-resp-ʳ⇑ᵛ ⟩
    [ ʳ⇑ᵛ τ ∘ᵛ ʳ⇑ᵛ ρ ]ᵛ t ≈⟨ [∘ᵛ] ⟩
    [ ʳ⇑ᵛ τ ]ᵛ ([ ʳ⇑ᵛ ρ ]ᵛ t)
    ∎

  ʳ⇑ᵛ-comm-inrᵛ-term : ∀ {Θ Γ Δ Ξ A} {ρ : Γ ⇒ᵛ Δ} {t : Term Θ Γ A}
    → ([ ʳ⇑ᵛ ρ {Ξ = Ξ} ]ᵛ ([ inrᵛ {Δ = Γ} ]ᵛ t)) ≈ ([ inrᵛ ]ᵛ ([ ρ ]ᵛ t))
  ʳ⇑ᵛ-comm-inrᵛ-term {Θ} {Γ} {Δ} {Ξ} {A} {ρ} {t = t} =
    let open SetoidR (Term-setoid Θ (Ξ ,, Δ) A) in
    begin
    [ ʳ⇑ᵛ ρ ]ᵛ ([ inrᵛ ]ᵛ t) ≈⟨ ≈-sym [∘ᵛ] ⟩
    [ ʳ⇑ᵛ ρ ∘ᵛ var-inr ]ᵛ t ≈⟨ []ᵛ-resp-≡ᵛ (ʳ⇑ᵛ-comm-inrᵛ ρ) ⟩
    [ inrᵛ ∘ᵛ ρ ]ᵛ t ≈⟨ [∘ᵛ] ⟩
    [ inrᵛ ]ᵛ ([ ρ ]ᵛ t)
    ∎

  -- Forming terms over a given metacontext and sort is functorial in the context
  module _ {Θ : MContext} {A : sort} where
    open Categories.Functor
    open Categories.Category.Instance.Setoids

    Term-Functor : Functor VContexts (Setoids ℓ ℓ)
    Term-Functor =
      record
        { F₀ = λ Γ → Term-setoid Θ Γ A
        ; F₁ = λ ρ → record { _⟨$⟩_ = [ ρ ]ᵛ_ ; cong = []ᵛ-resp-≈ }
        ; identity = ≈-trans [idᵛ]
        ; homomorphism = λ ξ → ≈-trans ([]ᵛ-resp-≈ ξ) [∘ᵛ]
        ; F-resp-≈ = λ ζ ξ → ≈-trans ([]ᵛ-resp-≡ᵛ ζ) ([]ᵛ-resp-≈ ξ)
        }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
-- Andreas, 2017-12-13, issue #2867
-- Parentheses needed when giving module argument

module _ where

module M (A : Set) where
  id : A → A
  id x = x

test : (F : Set → Set) (A : Set) (x : F A) → F A
test F A = λ x → x
  where open M {!F A!}  -- Give this

-- Expected: M (F A)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda