text:
module SystemF.BigStep.Extrinsic.Welltyped where

open import Prelude
open import SystemF.BigStep.Types
open import SystemF.BigStep.Extrinsic.Terms
open import Data.List
open import Extensions.List

-- welltyped terms
data _⊢_∶_ {n}(Γ : Ctx n) : Term → Type n → Set where

  unit : -------------------
         Γ ⊢ unit ∶ Unit

  ƛ : ∀ {b t} a →
      (a ∷ Γ) ⊢ t ∶ b →
      -------------------
      Γ ⊢ ƛ t ∶ (a ⇒ b)

  var : ∀ {a i} →
      Γ [ i ]= a →
      -------------
      Γ ⊢ var i ∶ a

  _·_ : ∀ {f e a b} →
      Γ ⊢ f ∶ (a ⇒ b) →
      Γ ⊢ e ∶ a →
      ---------------
      Γ ⊢ f · e ∶ b

  Λ : ∀ {a t} →
      (Γ ctx/ wk) ⊢ t ∶ a →
      ---------------------
      Γ ⊢ Λ t ∶ ∀' a

  _[_] : ∀ {f a} →
      Γ ⊢ f ∶ (∀' a) →
      (b : Type n) →
      ---------------------------
      Γ ⊢ f [-] ∶ (a / (sub b))


text:
module AocVec where
open import Data.Vec as Vec
open import Data.Nat

addToBack : {A : Set} → {N : ℕ} → A → Vec A N → Vec A (suc N)
addToBack v [] = v ∷ []
addToBack v (x ∷ vs) = x ∷ addToBack v vs

dupFrontToBack : {A : Set} → {N : ℕ} → Vec A (suc N) → Vec A (suc (suc N))
dupFrontToBack (x ∷ vs) = addToBack x (x ∷ vs)

dupFirstNToBack : {A : Set} → {M : ℕ} → (N : ℕ) → Vec A (suc M) → Vec A (N + (suc M))
dupFirstNToBack zero vs = vs
dupFirstNToBack (suc N) (x ∷ vs) = x ∷ dupFirstNToBack N (addToBack x vs)

ext: agda


text:
module _ where

open import Agda.Primitive
open import Agda.Builtin.Equality

data Wrap {a} (A : Set a) : Set a where
  wrap : A → Wrap A

data Unit (A : Set) : Set where
  unit : Unit A

record Functor {a b} (F : Set a → Set b) : Set (lsuc (a ⊔ b)) where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

open Functor ⦃ ... ⦄

instance
  FunWrap : ∀ {a} → Functor {a} Wrap
  FunWrap .fmap f (wrap x) = wrap (f x)

  FunUnit : Functor Unit
  FunUnit .fmap f unit = unit

_=$=_ : ∀ {a b} {A B : Set a} {F : Set a → Set b} {{_ : Functor F}} {x y : F A}
          (f : A → B) → x ≡ y → fmap f x ≡ fmap f y
f =$= refl = refl

postulate A : Set

wrap-refl : (x : A) → wrap x ≡ wrap x
wrap-refl x = refl

prf : (x : Wrap A) → wrap x ≡ wrap x
prf (wrap x) = wrap =$= wrap-refl x

-- Incomplete pattern matching when applying FunUnit
-- (Internal error at Reduce.Fast:1347)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ {A : Set} where

postulate B : Set

postulate
  H : {A : Set} → Set

test-H : Set
test-H = H {A = B}

record R {A : Set} : Set where
  constructor rc
  field f : A

test-R : Set
test-R = R {A = B}

test-f : ∀ B → R {A = B} → B
test-f B = R.f {A = B}

module N {A : Set} where

module test-N = N {A = B}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to Any
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Any.Properties where

open import Category.Monad
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Bool.Properties
open import Data.Empty using (⊥)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.List as List
open import Data.List.Categorical using (monad)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties.Core
  using (Any↔; find∘map; map∘find; lose∘find)
open import Data.List.Relation.Binary.Pointwise
  using (Pointwise; []; _∷_)
open import Data.Nat using (zero; suc; _<_; z≤n; s≤s)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.Any as MAny using (just)
open import Data.Product as Prod
  using (_×_; _,_; ∃; ∃₂; proj₁; proj₂; uncurry′)
open import Data.Product.Properties
open import Data.Product.Function.NonDependent.Propositional
  using (_×-cong_)
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
open import Function.Inverse as Inv using (_↔_; inverse; Inverse)
open import Function.Related as Related using (Related; SK-sym)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; inspect)
open import Relation.Unary
  using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
open import Relation.Nullary using (¬_)
open Related.EquationalReasoning

private
  open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})

------------------------------------------------------------------------
-- Equality properties

module _ {a p ℓ} {A : Set a} {P : A → Set p} {_≈_ : Rel A ℓ} where

  lift-resp : P Respects _≈_ → (Any P) Respects (Pointwise _≈_)
  lift-resp resp []            ()
  lift-resp resp (x≈y ∷ xs≈ys) (here px)   = here (resp x≈y px)
  lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
    there (lift-resp resp xs≈ys pxs)

module _ {a p} {A : Set a} {P : A → Set p} where

  here-injective : ∀ {x xs} {p q : P x} →
                   here {P = P} {xs = xs} p ≡ here q → p ≡ q
  here-injective refl = refl

  there-injective : ∀ {x xs} {p q : Any P xs} →
                    there {x = x} p ≡ there q → p ≡ q
  there-injective refl = refl

------------------------------------------------------------------------
-- Misc

module _ {a p} {A : Set a} {P : A → Set p} where

  ¬Any[] : ¬ Any P []
  ¬Any[] ()

------------------------------------------------------------------------
-- Any is a congruence

module _ {a k p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  Any-cong : ∀ {xs ys : List A} →
             (∀ x → Related k (P x) (Q x)) →
             Preorder._∼_ (Related.InducedPreorder₂ k {A = A} _∈_) xs ys →
             Related k (Any P xs) (Any Q ys)
  Any-cong {xs} {ys} P↔Q xs≈ys =
    Any P xs                ↔⟨ SK-sym Any↔ ⟩
    (∃ λ x → x ∈ xs × P x)  ∼⟨ Σ.cong Inv.id (xs≈ys ×-cong P↔Q _) ⟩
    (∃ λ x → x ∈ ys × Q x)  ↔⟨ Any↔ ⟩
    Any Q ys                ∎

------------------------------------------------------------------------
-- map

map-id : ∀ {a p} {A : Set a} {P : A → Set p} (f : P ⋐ P) {xs} →
         (∀ {x} (p : P x) → f p ≡ p) →
         (p : Any P xs) → Any.map f p ≡ p
map-id f hyp (here  p) = P.cong here (hyp p)
map-id f hyp (there p) = P.cong there $ map-id f hyp p

map-∘ : ∀ {a p q r}
          {A : Set a} {P : A → Set p} {Q : A → Set q} {R : A → Set r}
        (f : Q ⋐ R) (g : P ⋐ Q)
        {xs} (p : Any P xs) →
        Any.map (f ∘ g) p ≡ Any.map f (Any.map g p)
map-∘ f g (here  p) = refl
map-∘ f g (there p) = P.cong there $ map-∘ f g p

------------------------------------------------------------------------
-- Swapping

-- Nested occurrences of Any can sometimes be swapped. See also ×↔.

swap : ∀ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ} {xs ys} →
        Any (λ x → Any (P x) ys) xs → Any (λ y → Any (flip P y) xs) ys
swap (here  pys)  = Any.map here pys
swap (there pxys) = Any.map there (swap pxys)

swap-there : ∀ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ}
             {x xs ys} → (any : Any (λ x → Any (P x) ys) xs) →
             swap (Any.map (there {x = x}) any) ≡ there (swap any)
swap-there (here  pys)  = refl
swap-there (there pxys) = P.cong (Any.map there) (swap-there pxys)

swap-invol : ∀ {a b ℓ} {A : Set a} {B : Set b} {P : A → B → Set ℓ}
             {xs ys} → (any : Any (λ x → Any (P x) ys) xs) →
             swap (swap any) ≡ any
swap-invol (here (here px))   = refl
swap-invol (here (there pys)) =
  P.cong (Any.map there) (swap-invol (here pys))
swap-invol (there pxys)       =
  P.trans (swap-there (swap pxys)) (P.cong there (swap-invol pxys))

swap↔ : ∀ {ℓ} {A B : Set ℓ} {P : A → B → Set ℓ} {xs ys} →
       Any (λ x → Any (P x) ys) xs ↔ Any (λ y → Any (flip P y) xs) ys
swap↔ {P = P} = inverse swap swap swap-invol swap-invol

------------------------------------------------------------------------
-- Lemmas relating Any to ⊥

⊥↔Any⊥ : ∀ {a} {A : Set a} {xs : List A} → ⊥ ↔ Any (const ⊥) xs
⊥↔Any⊥ {A = A} = inverse (λ()) (λ p → from p) (λ()) (λ p → from p)
  where
  from : {xs : List A} → Any (const ⊥) xs → ∀ {b} {B : Set b} → B
  from (here ())
  from (there p) = from p

⊥↔Any[] : ∀ {a p} {A : Set a} {P : A → Set p} → ⊥ ↔ Any P []
⊥↔Any[] = inverse (λ()) (λ()) (λ()) (λ())

------------------------------------------------------------------------
-- Lemmas relating Any to ⊤

-- These introduction and elimination rules are not inverses, though.

module _ {a} {A : Set a} where

  any⁺ : ∀ (p : A → Bool) {xs} → Any (T ∘ p) xs → T (any p xs)
  any⁺ p (here  px)          = Equivalence.from T-∨ ⟨$⟩ inj₁ px
  any⁺ p (there {x = x} pxs) with p x
  ... | true  = _
  ... | false = any⁺ p pxs

  any⁻ : ∀ (p : A → Bool) xs → T (any p xs) → Any (T ∘ p) xs
  any⁻ p []       ()
  any⁻ p (x ∷ xs) px∷xs with p x | inspect p x
  any⁻ p (x ∷ xs) px∷xs | true  | P.[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq)
  any⁻ p (x ∷ xs) px∷xs | false | _       = there (any⁻ p xs px∷xs)

  any⇔ : ∀ {p : A → Bool} {xs} → Any (T ∘ p) xs ⇔ T (any p xs)
  any⇔ = equivalence (any⁺ _) (any⁻ _ _)

------------------------------------------------------------------------
-- Sums commute with Any

module _ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} where

  Any-⊎⁺ : ∀ {xs} → Any P xs ⊎ Any Q xs → Any (λ x → P x ⊎ Q x) xs
  Any-⊎⁺ = [ Any.map inj₁ , Any.map inj₂ ]′

  Any-⊎⁻ : ∀ {xs} → Any (λ x → P x ⊎ Q x) xs → Any P xs ⊎ Any Q xs
  Any-⊎⁻ (here (inj₁ p)) = inj₁ (here p)
  Any-⊎⁻ (here (inj₂ q)) = inj₂ (here q)
  Any-⊎⁻ (there p)       = Sum.map there there (Any-⊎⁻ p)

  ⊎↔ : ∀ {xs} → (Any P xs ⊎ Any Q xs) ↔ Any (λ x → P x ⊎ Q x) xs
  ⊎↔ = inverse Any-⊎⁺ Any-⊎⁻ from∘to to∘from
    where
    from∘to : ∀ {xs} (p : Any P xs ⊎ Any Q xs) → Any-⊎⁻ (Any-⊎⁺ p) ≡ p
    from∘to (inj₁ (here  p)) = refl
    from∘to (inj₁ (there p)) rewrite from∘to (inj₁ p) = refl
    from∘to (inj₂ (here  q)) = refl
    from∘to (inj₂ (there q)) rewrite from∘to (inj₂ q) = refl

    to∘from : ∀ {xs} (p : Any (λ x → P x ⊎ Q x) xs) →
              Any-⊎⁺ (Any-⊎⁻ p) ≡ p
    to∘from (here (inj₁ p)) = refl
    to∘from (here (inj₂ q)) = refl
    to∘from (there p) with Any-⊎⁻ p | to∘from p
    to∘from (there .(Any.map inj₁ p)) | inj₁ p | refl = refl
    to∘from (there .(Any.map inj₂ q)) | inj₂ q | refl = refl

------------------------------------------------------------------------
-- Products "commute" with Any.

module _ {a b p q} {A : Set a} {B : Set b}
         {P : Pred A p} {Q : Pred B q} where

  Any-×⁺ : ∀ {xs ys} → Any P xs × Any Q ys →
           Any (λ x → Any (λ y → P x × Q y) ys) xs
  Any-×⁺ (p , q) = Any.map (λ p → Any.map (λ q → (p , q)) q) p

  Any-×⁻ : ∀ {xs ys} → Any (λ x → Any (λ y → P x × Q y) ys) xs →
           Any P xs × Any Q ys
  Any-×⁻ pq with Prod.map id (Prod.map id find) (find pq)
  ... | (x , x∈xs , y , y∈ys , p , q) = (lose x∈xs p , lose y∈ys q)

  ×↔ : ∀ {xs ys} →
       (Any P xs × Any Q ys) ↔ Any (λ x → Any (λ y → P x × Q y) ys) xs
  ×↔ {xs} {ys} = inverse Any-×⁺ Any-×⁻ from∘to to∘from
    where
    from∘to : ∀ pq → Any-×⁻ (Any-×⁺ pq) ≡ pq
    from∘to (p , q) rewrite
        find∘map p (λ p → Any.map (λ q → (p , q)) q)
      | find∘map q (λ q → proj₂ (proj₂ (find p)) , q)
      | lose∘find p
      | lose∘find q
      = refl

    to∘from : ∀ pq → Any-×⁺ (Any-×⁻ pq) ≡ pq
    to∘from pq
      with find pq
        | (λ (f : (proj₁ (find pq) ≡_) ⋐ _) → map∘find pq {f})
    ... | (x , x∈xs , pq′) | lem₁
      with find pq′
        | (λ (f : (proj₁ (find pq′) ≡_) ⋐ _) → map∘find pq′ {f})
    ... | (y , y∈ys , p , q) | lem₂
      rewrite P.sym $ map-∘ {R = λ x → Any (λ y → P x × Q y) ys}
                            (λ p → Any.map (λ q → p , q) (lose y∈ys q))
                            (λ y → P.subst P y p)
                            x∈xs
              = lem₁ _ helper
      where
      helper : Any.map (λ q → p , q) (lose y∈ys q) ≡ pq′
      helper rewrite P.sym $ map-∘ (λ q → p , q)
                                   (λ y → P.subst Q y q)
                                   y∈ys
             = lem₂ _ refl

------------------------------------------------------------------------
-- Invertible introduction (⁺) and elimination (⁻) rules for various
-- list functions

------------------------------------------------------------------------
-- map

module _ {a p} {A : Set a} {P : Pred A p} where

  singleton⁺ : ∀ {x} → P x → Any P [ x ]
  singleton⁺ Px = here Px

  singleton⁻ : ∀ {x} → Any P [ x ] → P x
  singleton⁻ (here Px) = Px
  singleton⁻ (there ())

------------------------------------------------------------------------
-- map

module _ {a b} {A : Set a} {B : Set b} {f : A → B} where

  map⁺ : ∀ {p} {P : B → Set p}  {xs} →
         Any (P ∘ f) xs → Any P (List.map f xs)
  map⁺ (here p)  = here p
  map⁺ (there p) = there $ map⁺ p

  map⁻ : ∀ {p} {P : B → Set p} {xs} →
         Any P (List.map f xs) → Any (P ∘ f) xs
  map⁻ {xs = []}     ()
  map⁻ {xs = x ∷ xs} (here p)  = here p
  map⁻ {xs = x ∷ xs} (there p) = there $ map⁻ p

  map⁺∘map⁻ : ∀ {p} {P : B → Set p} {xs} →
              (p : Any P (List.map f xs)) → map⁺ (map⁻ p) ≡ p
  map⁺∘map⁻ {xs = []}     ()
  map⁺∘map⁻ {xs = x ∷ xs} (here  p) = refl
  map⁺∘map⁻ {xs = x ∷ xs} (there p) = P.cong there (map⁺∘map⁻ p)

  map⁻∘map⁺ : ∀ {p} (P : B → Set p) {xs} →
              (p : Any (P ∘ f) xs) → map⁻ {P = P} (map⁺ p) ≡ p
  map⁻∘map⁺ P (here  p) = refl
  map⁻∘map⁺ P (there p) = P.cong there (map⁻∘map⁺ P p)

  map↔ : ∀ {p} {P : B → Set p} {xs} →
         Any (P ∘ f) xs ↔ Any P (List.map f xs)
  map↔ = inverse map⁺ map⁻ (map⁻∘map⁺ _) map⁺∘map⁻

------------------------------------------------------------------------
-- mapMaybe

module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
         (f : A → Maybe B) where

  mapMaybe⁺ : ∀ xs → Any (MAny.Any P) (map f xs) →
              Any P (mapMaybe f xs)
  mapMaybe⁺ []       ()
  mapMaybe⁺ (x ∷ xs) ps with f x | ps
  ... | nothing | here  ()
  ... | nothing | there pxs      = mapMaybe⁺ xs pxs
  ... | just _  | here (just py) = here py
  ... | just _  | there pxs      = there (mapMaybe⁺ xs pxs)

------------------------------------------------------------------------
-- _++_

module _ {a p} {A : Set a} {P : A → Set p} where

  ++⁺ˡ : ∀ {xs ys} → Any P xs → Any P (xs ++ ys)
  ++⁺ˡ (here p)  = here p
  ++⁺ˡ (there p) = there (++⁺ˡ p)

  ++⁺ʳ : ∀ xs {ys} → Any P ys → Any P (xs ++ ys)
  ++⁺ʳ []       p = p
  ++⁺ʳ (x ∷ xs) p = there (++⁺ʳ xs p)

  ++⁻ : ∀ xs {ys} → Any P (xs ++ ys) → Any P xs ⊎ Any P ys
  ++⁻ []       p         = inj₂ p
  ++⁻ (x ∷ xs) (here p)  = inj₁ (here p)
  ++⁻ (x ∷ xs) (there p) = Sum.map there id (++⁻ xs p)

  ++⁺∘++⁻ : ∀ xs {ys} (p : Any P (xs ++ ys)) →
            [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs p) ≡ p
  ++⁺∘++⁻ []       p         = refl
  ++⁺∘++⁻ (x ∷ xs) (here  p) = refl
  ++⁺∘++⁻ (x ∷ xs) (there p) with ++⁻ xs p | ++⁺∘++⁻ xs p
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₁ p′ | ih = P.cong there ih
  ++⁺∘++⁻ (x ∷ xs) (there p) | inj₂ p′ | ih = P.cong there ih

  ++⁻∘++⁺ : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) →
            ++⁻ xs ([ ++⁺ˡ , ++⁺ʳ xs ]′ p) ≡ p
  ++⁻∘++⁺ []            (inj₁ ())
  ++⁻∘++⁺ []            (inj₂ p)         = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₁ (here  p)) = refl
  ++⁻∘++⁺ (x ∷ xs) {ys} (inj₁ (there p)) rewrite ++⁻∘++⁺ xs {ys} (inj₁ p) = refl
  ++⁻∘++⁺ (x ∷ xs)      (inj₂ p)         rewrite ++⁻∘++⁺ xs      (inj₂ p) = refl

  ++↔ : ∀ {xs ys} → (Any P xs ⊎ Any P ys) ↔ Any P (xs ++ ys)
  ++↔ {xs = xs} = inverse [ ++⁺ˡ , ++⁺ʳ xs ]′ (++⁻ xs) (++⁻∘++⁺ xs) (++⁺∘++⁻ xs)

  ++-comm : ∀ xs ys → Any P (xs ++ ys) → Any P (ys ++ xs)
  ++-comm xs ys = [ ++⁺ʳ ys , ++⁺ˡ ]′ ∘ ++⁻ xs

  ++-comm∘++-comm : ∀ xs {ys} (p : Any P (xs ++ ys)) →
                    ++-comm ys xs (++-comm xs ys p) ≡ p
  ++-comm∘++-comm [] {ys} p
    rewrite ++⁻∘++⁺ ys {ys = []} (inj₁ p) = refl
  ++-comm∘++-comm (x ∷ xs) {ys} (here p)
    rewrite ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₂ (here p)) = refl
  ++-comm∘++-comm (x ∷ xs)      (there p) with ++⁻ xs p | ++-comm∘++-comm xs p
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ʳ ys p))))
    | inj₁ p | refl
    rewrite ++⁻∘++⁺ ys (inj₂                 p)
            | ++⁻∘++⁺ ys (inj₂ $ there {x = x} p) = refl
  ++-comm∘++-comm (x ∷ xs) {ys} (there .([ ++⁺ʳ xs , ++⁺ˡ ]′ (++⁻ ys (++⁺ˡ p))))
    | inj₂ p | refl
    rewrite ++⁻∘++⁺ ys {ys =     xs} (inj₁ p)
            | ++⁻∘++⁺ ys {ys = x ∷ xs} (inj₁ p) = refl

  ++↔++ : ∀ xs ys → Any P (xs ++ ys) ↔ Any P (ys ++ xs)
  ++↔++ xs ys = inverse (++-comm xs ys) (++-comm ys xs)
                        (++-comm∘++-comm xs) (++-comm∘++-comm ys)

  ++-insert : ∀ xs {ys x} → P x → Any P (xs ++ [ x ] ++ ys)
  ++-insert xs Px = ++⁺ʳ xs (++⁺ˡ (singleton⁺ Px))

------------------------------------------------------------------------
-- concat

module _ {a p} {A : Set a} {P : A → Set p} where

  concat⁺ : ∀ {xss} → Any (Any P) xss → Any P (concat xss)
  concat⁺ (here p)           = ++⁺ˡ p
  concat⁺ (there {x = xs} p) = ++⁺ʳ xs (concat⁺ p)

  concat⁻ : ∀ xss → Any P (concat xss) → Any (Any P) xss
  concat⁻ []               ()
  concat⁻ ([]       ∷ xss) p         = there $ concat⁻ xss p
  concat⁻ ((x ∷ xs) ∷ xss) (here  p) = here (here p)
  concat⁻ ((x ∷ xs) ∷ xss) (there p) with concat⁻ (xs ∷ xss) p
  ... | here  p′ = here (there p′)
  ... | there p′ = there p′

  concat⁻∘++⁺ˡ : ∀ {xs} xss (p : Any P xs) →
                 concat⁻ (xs ∷ xss) (++⁺ˡ p) ≡ here p
  concat⁻∘++⁺ˡ xss (here  p) = refl
  concat⁻∘++⁺ˡ xss (there p) rewrite concat⁻∘++⁺ˡ xss p = refl

  concat⁻∘++⁺ʳ : ∀ xs xss (p : Any P (concat xss)) →
                   concat⁻ (xs ∷ xss) (++⁺ʳ xs p) ≡ there (concat⁻ xss p)
  concat⁻∘++⁺ʳ []       xss p = refl
  concat⁻∘++⁺ʳ (x ∷ xs) xss p rewrite concat⁻∘++⁺ʳ xs xss p = refl

  concat⁺∘concat⁻ : ∀ xss (p : Any P (concat xss)) →
                      concat⁺ (concat⁻ xss p) ≡ p
  concat⁺∘concat⁻ []               ()
  concat⁺∘concat⁻ ([]       ∷ xss) p         = concat⁺∘concat⁻ xss p
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (here p)  = refl
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there p)
                with concat⁻ (xs ∷ xss) p | concat⁺∘concat⁻ (xs ∷ xss) p
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there .(++⁺ˡ p′))              | here  p′ | refl = refl
  concat⁺∘concat⁻ ((x ∷ xs) ∷ xss) (there .(++⁺ʳ xs (concat⁺ p′))) | there p′ | refl = refl

  concat⁻∘concat⁺ : ∀ {xss} (p : Any (Any P) xss) → concat⁻ xss (concat⁺ p) ≡ p
  concat⁻∘concat⁺ (here                      p) = concat⁻∘++⁺ˡ _ p
  concat⁻∘concat⁺ (there {x = xs} {xs = xss} p)
    rewrite concat⁻∘++⁺ʳ xs xss (concat⁺ p) =
      P.cong there $ concat⁻∘concat⁺ p

  concat↔ : ∀ {xss} → Any (Any P) xss ↔ Any P (concat xss)
  concat↔ {xss} = inverse concat⁺ (concat⁻ xss) concat⁻∘concat⁺ (concat⁺∘concat⁻ xss)

------------------------------------------------------------------------
-- applyUpTo

module _ {a p} {A : Set a} {P : A → Set p} where

  applyUpTo⁺ : ∀ f {i n} → P (f i) → i < n → Any P (applyUpTo f n)
  applyUpTo⁺ _ p (s≤s z≤n)       = here p
  applyUpTo⁺ f p (s≤s (s≤s i<n)) =
    there (applyUpTo⁺ (f ∘ suc) p (s≤s i<n))

  applyUpTo⁻ : ∀ f {n} → Any P (applyUpTo f n) →
               ∃ λ i → i < n × P (f i)
  applyUpTo⁻ f {zero}  ()
  applyUpTo⁻ f {suc n} (here p)  = zero , s≤s z≤n , p
  applyUpTo⁻ f {suc n} (there p) with applyUpTo⁻ (f ∘ suc) p
  ... | i , i<n , q = suc i , s≤s i<n , q

------------------------------------------------------------------------
-- tabulate

module _ {a p} {A : Set a} {P : A → Set p} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} i → P (f i) → Any P (tabulate f)
  tabulate⁺ fzero    p = here p
  tabulate⁺ (fsuc i) p = there (tabulate⁺ i p)

  tabulate⁻ : ∀ {n} {f : Fin n → A} →
              Any P (tabulate f) → ∃ λ i → P (f i)
  tabulate⁻ {zero}  ()
  tabulate⁻ {suc n} (here p)   = fzero , p
  tabulate⁻ {suc n} (there p) = Prod.map fsuc id (tabulate⁻ p)

------------------------------------------------------------------------
-- map-with-∈.

module _ {a b p} {A : Set a} {B : Set b} {P : B → Set p} where

  map-with-∈⁺ : ∀ {xs : List A} (f : ∀ {x} → x ∈ xs → B) →
                (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
                Any P (map-with-∈ xs f)
  map-with-∈⁺ f (_ , here refl  , p) = here p
  map-with-∈⁺ f (_ , there x∈xs , p) =
    there $ map-with-∈⁺ (f ∘ there) (_ , x∈xs , p)

  map-with-∈⁻ : ∀ (xs : List A) (f : ∀ {x} → x ∈ xs → B) →
                Any P (map-with-∈ xs f) →
                ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)
  map-with-∈⁻ []       f ()
  map-with-∈⁻ (y ∷ xs) f (here  p) = (y , here refl , p)
  map-with-∈⁻ (y ∷ xs) f (there p) =
    Prod.map id (Prod.map there id) $ map-with-∈⁻ xs (f ∘ there) p

  map-with-∈↔ : ∀  {xs : List A} {f : ∀ {x} → x ∈ xs → B} →
    (∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) ↔ Any P (map-with-∈ xs f)
  map-with-∈↔ = inverse (map-with-∈⁺ _) (map-with-∈⁻ _ _) (from∘to _) (to∘from _ _)
    where
    from∘to : ∀ {xs : List A} (f : ∀ {x} → x ∈ xs → B)
              (p : ∃₂ λ x (x∈xs : x ∈ xs) → P (f x∈xs)) →
              map-with-∈⁻ xs f (map-with-∈⁺ f p) ≡ p
    from∘to f (_ , here refl  , p) = refl
    from∘to f (_ , there x∈xs , p)
      rewrite from∘to (f ∘ there) (_ , x∈xs , p) = refl

    to∘from : ∀ (xs : List A) (f : ∀ {x} → x ∈ xs → B)
              (p : Any P (map-with-∈ xs f)) →
              map-with-∈⁺ f (map-with-∈⁻ xs f p) ≡ p
    to∘from []       f ()
    to∘from (y ∷ xs) f (here  p) = refl
    to∘from (y ∷ xs) f (there p) =
      P.cong there $ to∘from xs (f ∘ there) p

------------------------------------------------------------------------
-- return

module _ {a p} {A : Set a} {P : A → Set p} where

  return⁺ : ∀ {x} → P x → Any P (return x)
  return⁺ = here

  return⁻ : ∀ {x} → Any P (return x) → P x
  return⁻ (here p)   = p
  return⁻ (there ())

  return⁺∘return⁻ : ∀ {x} (p : Any P (return x)) →
                    return⁺ (return⁻ p) ≡ p
  return⁺∘return⁻ (here p)   = refl
  return⁺∘return⁻ (there ())

  return⁻∘return⁺ : ∀ {x} (p : P x) → return⁻ (return⁺ p) ≡ p
  return⁻∘return⁺ p = refl

  return↔ : ∀ {x} → P x ↔ Any P (return x)
  return↔ = inverse return⁺ return⁻ return⁻∘return⁺ return⁺∘return⁻

------------------------------------------------------------------------
-- _∷_

module _ {a p} {A : Set a} where

  ∷↔ : ∀ (P : Pred A p) {x xs} → (P x ⊎ Any P xs) ↔ Any P (x ∷ xs)
  ∷↔ P {x} {xs} =
    (P x         ⊎ Any P xs)  ↔⟨ return↔ {P = P} ⊎-cong (Any P xs ∎) ⟩
    (Any P [ x ] ⊎ Any P xs)  ↔⟨ ++↔ {P = P} {xs = [ x ]} ⟩
    Any P (x ∷ xs)            ∎

------------------------------------------------------------------------
-- _>>=_

module _ {ℓ p} {A B : Set ℓ} {P : B → Set p} {f : A → List B} where

  >>=↔ : ∀ {xs} → Any (Any P ∘ f) xs ↔ Any P (xs >>= f)
  >>=↔ {xs} =
    Any (Any P ∘ f) xs           ↔⟨ map↔ ⟩
    Any (Any P) (List.map f xs)  ↔⟨ concat↔ ⟩
    Any P (xs >>= f)             ∎

------------------------------------------------------------------------
-- _⊛_

module _ {ℓ} {A B : Set ℓ} where

  ⊛↔ : ∀ {P : B → Set ℓ} {fs : List (A → B)} {xs : List A} →
       Any (λ f → Any (P ∘ f) xs) fs ↔ Any P (fs ⊛ xs)
  ⊛↔ {P = P} {fs} {xs} =
    Any (λ f → Any (P ∘ f) xs) fs               ↔⟨ Any-cong (λ _ → Any-cong (λ _ → return↔) (_ ∎)) (_ ∎) ⟩
    Any (λ f → Any (Any P ∘ return ∘ f) xs) fs  ↔⟨ Any-cong (λ _ → >>=↔ ) (_ ∎) ⟩
    Any (λ f → Any P (xs >>= return ∘ f)) fs    ↔⟨ >>=↔ ⟩
    Any P (fs ⊛ xs)                             ∎

-- An alternative introduction rule for _⊛_

  ⊛⁺′ : ∀ {P : A → Set ℓ} {Q : B → Set ℓ} {fs : List (A → B)} {xs} →
        Any (P ⟨→⟩ Q) fs → Any P xs → Any Q (fs ⊛ xs)
  ⊛⁺′ pq p =
    Inverse.to ⊛↔ ⟨$⟩
      Any.map (λ pq → Any.map (λ {x} → pq {x}) p) pq

------------------------------------------------------------------------
-- _⊗_

module _ {ℓ} {A B : Set ℓ} where

  ⊗↔ : {P : A × B → Set ℓ} {xs : List A} {ys : List B} →
       Any (λ x → Any (λ y → P (x , y)) ys) xs ↔ Any P (xs ⊗ ys)
  ⊗↔ {P} {xs} {ys} =
    Any (λ x → Any (λ y → P (x , y)) ys) xs                             ↔⟨ return↔ ⟩
    Any (λ _,_ → Any (λ x → Any (λ y → P (x , y)) ys) xs) (return _,_)  ↔⟨ ⊛↔ ⟩
    Any (λ x, → Any (P ∘ x,) ys) (_,_ <$> xs)                           ↔⟨ ⊛↔ ⟩
    Any P (xs ⊗ ys)                                                     ∎

  ⊗↔′ : {P : A → Set ℓ} {Q : B → Set ℓ} {xs : List A} {ys : List B} →
        (Any P xs × Any Q ys) ↔ Any (P ⟨×⟩ Q) (xs ⊗ ys)
  ⊗↔′ {P} {Q} {xs} {ys} =
    (Any P xs × Any Q ys)                    ↔⟨ ×↔ ⟩
    Any (λ x → Any (λ y → P x × Q y) ys) xs  ↔⟨ ⊗↔ ⟩
    Any (P ⟨×⟩ Q) (xs ⊗ ys)                  ∎


text:
{-# OPTIONS --cumulativity --postfix-projections #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  ℓ ℓ₁ ℓ₂ ℓ₃ : Level
  A B C : Set ℓ
  x y z : A
  k l m n : Nat

record Σ {ℓ} (A : Set ℓ) (B : A → Set ℓ) : Set ℓ where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

record Category ℓ : Set (lsuc ℓ) where
  field
    Carrier : Set ℓ
    _~>_    : Carrier → Carrier → Set ℓ
    id      : ∀ {X} → X ~> X
    _∘_     : ∀ {X Y Z} → X ~> Y → Y ~> Z → X ~> Z
open Category public

SetCat : ∀ ℓ → Category (lsuc ℓ)
SetCat ℓ .Carrier  = Set ℓ
SetCat ℓ ._~>_ A B = A → B
SetCat ℓ .id = λ x → x
SetCat ℓ ._∘_ f g = λ x → g (f x)

record Functor (c : Category ℓ₁) (c′ : Category ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  private
    module c  = Category c
    module c′ = Category c′

  field
    F    : c.Carrier → c′.Carrier
    fmap : {A B : c.Carrier} → A c.~> B → F A c′.~> F B
open Functor public

idFunctor : {c : Category ℓ} → Functor c c
idFunctor .F    X = X
idFunctor .fmap f = f

compFunctor : {c₁ : Category ℓ₁} {c₂ : Category ℓ₂} {c₃ : Category ℓ₃}
            → Functor c₁ c₂ → Functor c₂ c₃ → Functor c₁ c₃
compFunctor F₁ F₂ .F    X = F₂ .F (F₁ .F X)
compFunctor F₁ F₂ .fmap f = F₂ .fmap (F₁ .fmap f)

Cat : ∀ ℓ → Category (lsuc ℓ)
Cat ℓ .Carrier    = Category ℓ
Cat ℓ ._~>_ c₁ c₂ = Functor c₁ c₂
Cat ℓ .id  = idFunctor
Cat ℓ ._∘_ = compFunctor

NatTrans : {c₁ : Category ℓ₁} {c₂ : Category ℓ₂} → (F G : Functor c₁ c₂) → Set (ℓ₁ ⊔ ℓ₂)
NatTrans {c₁ = c₁} {c₂ = c₂} F G =
  let module c₁ = Category c₁
      module c₂ = Category c₂
      module F = Functor F
      module G = Functor G
  in ∀ X → F.F X c₂.~> G.F X

FunctorCat : (c₁ : Category ℓ₁) (c₂ : Category ℓ₂) → Category (ℓ₁ ⊔ ℓ₂)
FunctorCat c₁ c₂ .Carrier   = Functor c₁ c₂
FunctorCat c₁ c₂ ._~>_      = NatTrans
FunctorCat c₁ c₂ .id X      = c₂ .id
FunctorCat c₁ c₂ ._∘_ α β X =
  let module c₁ = Category c₁
      module c₂ = Category c₂
  in α X c₂.∘ β X

record Setoid ℓ : Set (lsuc ℓ) where
  field
    Carrier : Set ℓ
    _~_     : Carrier → Carrier → Set ℓ
    rfl     : ∀ {x} → x ~ x
    sym     : ∀ {x y} → x ~ y → y ~ x
    trans   : ∀ {x y z} → x ~ y → y ~ z → x ~ z
open Setoid public

DiscreteSetoid : Set ℓ → Setoid ℓ
DiscreteSetoid A .Carrier = A
DiscreteSetoid A ._~_     = _≡_
DiscreteSetoid A .rfl = refl
DiscreteSetoid A .sym refl = refl
DiscreteSetoid A .trans refl refl = refl

SetoidCat : ∀ ℓ → Category (lsuc ℓ)
SetoidCat ℓ .Carrier   = Setoid ℓ
SetoidCat ℓ ._~>_  A B =
  let module A = Setoid A
      module B = Setoid B
  in Σ {ℓ} (A.Carrier → B.Carrier)
     λ f → ∀ {x y} → x A.~ y → f x B.~ f y
SetoidCat ℓ .id  = (λ x → x) , λ x= → x=
SetoidCat ℓ ._∘_ (f , f=) (g , g=) = (λ x → g (f x)) , λ x= → g= (f= x=)

DiscreteSetoidFunctor : ∀ {ℓ} → Functor (SetCat ℓ) (SetoidCat ℓ)
DiscreteSetoidFunctor .F = DiscreteSetoid
DiscreteSetoidFunctor .fmap f .fst = f
DiscreteSetoidFunctor .fmap f .snd refl = refl

Op : Category ℓ → Category ℓ
Op c .Carrier  = c .Carrier
Op c ._~>_ A B = c ._~>_ B A
Op c .id = c .id
Op c ._∘_ = let module c = Category c in λ f g → g c.∘ f

Yoneda : {c : Category ℓ} (X : c .Carrier) → Functor c (Op (SetCat ℓ))
Yoneda {c = c} X .F Y =
  let module c = Category c
  in  Y c.~> X
Yoneda {c = c} X .fmap = c ._∘_

test : Functor (SetCat (lsuc lzero)) (Op (SetCat (lsuc (lsuc lzero))))
test = Yoneda {c = SetCat (lsuc lzero)} Set


text:
module Issue4435-2 where

record ⊤ : Set where

data Foo (a : Set) : Set where
Bar : {a : Set} → Foo a → Set

-- Here, the error message does NOT include
-- "Perhaps you meant to write 'data Foo a where'"
-- because Foo is defined above (rather than declared - note the "where"
-- compared to Issue4435-1.agda).
data Foo a : Set where
  c1 : Foo a
  c2 : (x : Foo a) (y : Bar x → Foo a) → Foo a

Bar c1 = ⊤
Bar (c2 a b) = (x : Bar a) → Bar (b x)

max_forks_repo_name: shlevy/agda


text:
module PushArgument where

open import Agda.Builtin.Nat

data List (A : Set) : Nat -> Set where
    nil : List A 0
    cons : {n : Nat} -> A -> List A n -> List A (suc n)

newFunc : {A : Set} -> {B : Set} -> (f : A -> B) -> (x : A) -> B

newFunc f x = f x

map : {n : Nat} -> {A : Set} -> {B : Set} -> (A -> B) -> List A n -> List B n

map f nil = nil

map f (cons x xs) = cons (newFunc f x) (map f xs)


text:
-- Andreas, 2016-07-28, issue #779

record R : Set1 where
  data Bla : Set where
  field F : Set

-- WAS:
-- Not a valid let-definition

-- Expected:
-- Success, or error outlawing pattern matching definition before last field.


text:
------------------------------------------------------------------------
-- Examples related to Univalence-axiom.Isomorphism-is-equality.More
------------------------------------------------------------------------

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

-- Note that this module uses ordinary propositional equality, with a
-- computing J rule.

-- This module has been developed in collaboration with Thierry
-- Coquand.

module Univalence-axiom.Isomorphism-is-equality.More.Examples where

open import Equality.Propositional renaming (equality-with-J to eq)

open import Equivalence eq hiding (id)
open import Function-universe eq hiding (id)
open import H-level.Closure eq
open import Prelude hiding (id)
open import Univalence-axiom.Isomorphism-is-equality.More

------------------------------------------------------------------------
-- Magmas

magma : Code
magma = ε ▻ A-type ▻ N-ary [0] 2

Magma : Type₁
Magma = ⟦ magma ⟧

private

  -- An unfolding of Magma.

  Magma-unfolded :
    Magma ≡ Σ (Σ (↑ _ ⊤) λ _ →
    Type                   ) λ { (_ , A) →
    ↑ _ A → ↑ _ A → ↑ _ A }
  Magma-unfolded = refl

  -- An unfolding of Isomorphic magma.

  Isomorphic-magma-unfolded :
    ∀ {ass A₁ f₁ A₂ f₂} →
    Isomorphic ass magma ((_ , A₁) , f₁) ((_ , A₂) , f₂) ≡
    Σ (Σ (↑ _ ⊤) λ _ →
      ↑ _ (A₁ ≃ A₂)                             ) λ { (_ , lift A₁≃A₂) →
      let open _≃_ (↑-cong A₁≃A₂) in
        ∀ x y → to (f₁ x y) ≡ f₂ (to x) (to y) }
  Isomorphic-magma-unfolded = refl

------------------------------------------------------------------------
-- Semigroups

-- Note that one axiom states that the underlying type is a set. This
-- assumption is used to prove that the other axiom is propositional.

semigroup : Code
semigroup =
  ε

  ▻ A-type

  ▻ Is-a-set [0]

  ▻ N-ary (1+ [0]) 2

  ▻ Proposition
      (λ { (_ , _∙_) →
           ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })
      assoc-prop

  where
  assoc-prop = λ { ass ((_ , A-set) , _) →
    let open Assumptions ass in
    Π-closure ext₁ 1 λ _ →
    Π-closure ext₁ 1 λ _ →
    Π-closure ext₁ 1 λ _ →
    A-set }

Semigroup : Type₁
Semigroup = ⟦ semigroup ⟧

private

  -- An unfolding of Semigroup.

  Semigroup-unfolded :
    Semigroup ≡ Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      Type                                     ) λ {  (_ , A) →
      Is-set (↑ _ A)                          }) λ { ((_ , A) , _) →
      ↑ _ A → ↑ _ A → ↑ _ A                   }) λ { (_ , _∙_) →
      ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }
  Semigroup-unfolded = refl

  -- An unfolding of Isomorphic semigroup.

  Isomorphic-semigroup-unfolded :
    ∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)} {_∙₁_ assoc₁}
          {A₂} {is₂ : Is-set (↑ _ A₂)} {_∙₂_ assoc₂} →
    Isomorphic ass semigroup ((((_ , A₁) , is₁) , _∙₁_) , assoc₁)
                             ((((_ , A₂) , is₂) , _∙₂_) , assoc₂) ≡
    Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      ↑ _ (A₁ ≃ A₂)                           ) λ { _ →
      ↑ _ ⊤                                  }) λ { ((_ , lift A₁≃A₂) , _) →
      let open _≃_ (↑-cong A₁≃A₂) in
        ∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y) }) λ { _ →
      ↑ _ ⊤                                  }
  Isomorphic-semigroup-unfolded = refl

------------------------------------------------------------------------
-- Sets with fixed-point operators

set-with-fixed-point-operator : Code
set-with-fixed-point-operator =
  ε

  ▻ A-type

  ▻ Is-a-set [0]

  ▻ Simple ((base (1+ [0]) ⟶ base (1+ [0])) ⟶ base (1+ [0]))

  ▻ Proposition
      (λ { (_ , fix) →
           ∀ f → fix f ≡ f (fix f) })
      fix-point-prop

  where
  fix-point-prop = λ { ass ((_ , A-set) , _) →
    let open Assumptions ass in
    Π-closure ext₁ 1 λ _ →
    A-set }

Set-with-fixed-point-operator : Type₁
Set-with-fixed-point-operator = ⟦ set-with-fixed-point-operator ⟧

private

  -- An unfolding of Set-with-fixed-point-operator.

  Set-with-fixed-point-operator-unfolded :
    Set-with-fixed-point-operator ≡ Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      Type                     ) λ {  (_ , A) →
      Is-set (↑ _ A)          }) λ { ((_ , A) , _) →
      (↑ _ A → ↑ _ A) → ↑ _ A }) λ { (_ , fix) →
      ∀ f → fix f ≡ f (fix f) }
  Set-with-fixed-point-operator-unfolded = refl

  -- An unfolding of Isomorphic set-with-fixed-point-operator.

  Isomorphic-set-with-fixed-point-operator-unfolded :
    ∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)} {fix₁ fixed-point₁}
          {A₂} {is₂ : Is-set (↑ _ A₂)} {fix₂ fixed-point₂} →
    Isomorphic ass set-with-fixed-point-operator
               ((((_ , A₁) , is₁) , fix₁) , fixed-point₁)
               ((((_ , A₂) , is₂) , fix₂) , fixed-point₂) ≡
    Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      ↑ _ (A₁ ≃ A₂)                             ) λ { _ →
      ↑ _ ⊤                                    }) λ { ((_ , lift A₁≃A₂) , _) →
      let open _≃_ (↑-cong A₁≃A₂) in
        ∀ f g →
        (∀ x y → to x ≡ y → to (f x) ≡ g y) →
        to (fix₁ f) ≡ fix₂ g                   }) λ { _ →
      ↑ _ ⊤                                    }
  Isomorphic-set-with-fixed-point-operator-unfolded = refl

------------------------------------------------------------------------
-- Abelian groups

abelian-group : Code
abelian-group =
  ε

  -- The underlying type.
  ▻ A-type

  -- The underlying type is a set.
  ▻ Is-a-set [0]

  -- The binary group operation.
  ▻ N-ary (1+ [0]) 2

  -- Commutativity.
  ▻ Comm

  -- Associativity.
  ▻ Assoc

  -- Identity.
  ▻ N-ary (1+ 1+ 1+ 1+ [0]) 0

  -- Left identity.
  ▻ Left-identity

  -- Right identity.
  ▻ Right-identity

  -- Inverse.
  ▻ N-ary (1+ 1+ 1+ 1+ 1+ 1+ 1+ [0]) 1

  -- Left inverse.
  ▻ Left-inverse

  -- Right inverse.
  ▻ Right-inverse

  where
  Comm = Proposition
    (λ { (_ , _∙_) →
       ∀ x y → (x ∙ y) ≡ (y ∙ x) })

    (λ { ass ((_ , A-set) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       Π-closure ext₁ 1 λ _ →
       A-set
     })

  Assoc = Proposition
    (λ { ((_ , _∙_) , _) →
         ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) })

    (λ { ass (((_ , A-set) , _) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       Π-closure ext₁ 1 λ _ →
       Π-closure ext₁ 1 λ _ →
       A-set
     })

  Left-identity = Proposition
    (λ { ((((_ , _∙_) , _) , _) , e) →
         ∀ x → (e ∙ x) ≡ x })

    (λ { ass (((((_ , A-set) , _) , _) , _) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       A-set
     })

  Right-identity = Proposition
    (λ { (((((_ , _∙_) , _) , _) , e) , _) →
         ∀ x → (x ∙ e) ≡ x })

    (λ { ass ((((((_ , A-set) , _) , _) , _) , _) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       A-set
     })

  Left-inverse = Proposition
    (λ { (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
         ∀ x → ((x ⁻¹) ∙ x) ≡ e })

    (λ { ass ((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       A-set
     })

  Right-inverse = Proposition
    (λ { ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
         ∀ x → (x ∙ (x ⁻¹)) ≡ e })

    (λ { ass (((((((((_ , A-set) , _) , _) , _) , _) , _) , _) , _) , _) →
       let open Assumptions ass in
       Π-closure ext₁ 1 λ _ →
       A-set
     })

Abelian-group : Type₁
Abelian-group = ⟦ abelian-group ⟧

private

  -- An unfolding of Abelian-group. Note that the inner structure is
  -- left-nested.

  Abelian-group-unfolded :
    Abelian-group ≡ Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      Type                                     ) λ {        (_ , A) →
      Is-set (↑ _ A)                          }) λ {       ((_ , A) , _) →
      ↑ _ A → ↑ _ A → ↑ _ A                   }) λ {                  (_ , _∙_) →
      ∀ x y → (x ∙ y) ≡ (y ∙ x)               }) λ {                 ((_ , _∙_) , _) →
      ∀ x y z → (x ∙ (y ∙ z)) ≡ ((x ∙ y) ∙ z) }) λ {    (((((_ , A) , _) , _  ) , _) , _) →
      ↑ _ A                                   }) λ {               ((((_ , _∙_) , _) , _) , e) →
      ∀ x → (e ∙ x) ≡ x                       }) λ {              (((((_ , _∙_) , _) , _) , e) , _) →
      ∀ x → (x ∙ e) ≡ x                       }) λ { ((((((((_ , A) , _) , _  ) , _) , _) , _) , _) , _) →
      ↑ _ A → ↑ _ A                           }) λ {            (((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) →
      ∀ x → ((x ⁻¹) ∙ x) ≡ e                  }) λ {           ((((((((_ , _∙_) , _) , _) , e) , _) , _) , _⁻¹) , _) →
      ∀ x → (x ∙ (x ⁻¹)) ≡ e                  }
  Abelian-group-unfolded = refl

  -- An unfolding of Isomorphic abelian-group.

  Isomorphic-abelian-group-unfolded :
    ∀ {ass A₁} {is₁ : Is-set (↑ _ A₁)}
      {_∙₁_ comm₁ assoc₁ e₁ lid₁ rid₁ _⁻¹₁ linv₁ rinv₁}
      {A₂} {is₂ : Is-set (↑ _ A₂)}
      {_∙₂_ comm₂ assoc₂ e₂ lid₂ rid₂ _⁻¹₂ linv₂ rinv₂} →
    Isomorphic ass abelian-group
      (((((((((((_ , A₁) , is₁) , _∙₁_) , comm₁) ,
       assoc₁) , e₁) , lid₁) , rid₁) , _⁻¹₁) , linv₁) , rinv₁)
      (((((((((((_ , A₂) , is₂) , _∙₂_) , comm₂) ,
       assoc₂) , e₂) , lid₂) , rid₂) , _⁻¹₂) , linv₂) , rinv₂) ≡
    Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (Σ (↑ _ ⊤) λ _ →
      ↑ _ (A₁ ≃ A₂)                           ) λ { _ →
      ↑ _ ⊤                                  }) λ {       ((_ , lift A₁≃A₂) , _) →
      let open _≃_ (↑-cong A₁≃A₂) in
        ∀ x y → to (x ∙₁ y) ≡ (to x ∙₂ to y) }) λ { _ →
      ↑ _ ⊤                                  }) λ { _ →
      ↑ _ ⊤                                  }) λ {    (((((_ , lift A₁≃A₂) , _) , _) , _) , _) →
      let open _≃_ (↑-cong A₁≃A₂) in
        to e₁ ≡ e₂                           }) λ { _ →
      ↑ _ ⊤                                  }) λ { _ →
      ↑ _ ⊤                                  }) λ { ((((((((_ , lift A₁≃A₂) , _) , _) , _) , _) , _) , _) , _) →
      let open _≃_ (↑-cong A₁≃A₂) in
        ∀ x → to (x ⁻¹₁) ≡ (to x ⁻¹₂)        }) λ { _ →
      ↑ _ ⊤                                  }) λ { _ →
      ↑ _ ⊤                                  }
  Isomorphic-abelian-group-unfolded = refl

------------------------------------------------------------------------
-- Church-encoded natural numbers for which we can do induction

-- Church-encoded natural numbers.

Nat : Type₁
Nat = (A : Type) → ↑ (# 1) A → (↑ (# 1) A → ↑ (# 1) A) → ↑ (# 1) A

-- Zero and successor.

Zero : Nat
Zero = λ A z s → z

Suc : Nat → Nat
Suc = λ n A z s → s (n A z s)

-- The code.

inductive-natural-numbers : Code
inductive-natural-numbers =
  ε

  ▻ Dep (Π set (Π (base ⟨0⟩)
                  (Π (Π (base (1+ ⟨0⟩)) (base (1+ 1+ ⟨0⟩)))
                     (base (1+ 1+ ⟨0⟩)))))

  ▻ Proposition
      (λ { (_ , n) →
           (P : Nat → Type) →
           Is-proposition (P n) →
           P Zero →
           (∀ m → P m → P (Suc m)) →
           P n })
      (λ ass _ →
           let open Assumptions ass in
           Π-closure ext₁ 1 λ _ →
           Π-closure (lower-extensionality (# 1) (# 0) ext₁) 1 λ Pn-prop →
           Π-closure (lower-extensionality (# 1) (# 0) ext₁) 1 λ _ →
           Π-closure (lower-extensionality (# 0) (# 1) ext₁) 1 λ _ →
           Pn-prop)

  where open Dependent

private

  -- The usual unfolding lemmas.

  ⟦inductive-natural-numbers⟧ :

    ⟦ inductive-natural-numbers ⟧
      ≡
    Σ (Σ (↑ _ ⊤) λ _ →
      Nat                        ) λ { (_ , n) →
      (P : Nat → Type) →
      Is-proposition (P n) →
      P Zero →
      (∀ m → P m → P (Suc m)) →
      P n                       }
  ⟦inductive-natural-numbers⟧ = refl

  Isomorphic-inductive-natural-numbers :
    ∀ {ass : Assumptions}
      {n₁ n₂ : Nat}
      {prop₁ : (P : Nat → Type) → Is-proposition (P n₁) →
               P Zero → (∀ m → P m → P (Suc m)) → P n₁}
      {prop₂ : (P : Nat → Type) → Is-proposition (P n₂) →
               P Zero → (∀ m → P m → P (Suc m)) → P n₂} →

    Isomorphic ass inductive-natural-numbers
                   ((_ , n₁) , prop₁) ((_ , n₂) , prop₂)
      ≡
    Σ (Σ (↑ (# 1) ⊤) λ _ →
    ((A₁ A₂ : Type) → (A₁≃A₂ : ↑ (# 1) (A₁ ≃ A₂)) →
     let cast = _≃_.from (↑-cong (lower A₁≃A₂)) in
     (z₁ : ↑ (# 1) A₁) (z₂ : ↑ (# 1) A₂) →
       z₁ ≡ cast z₂ →
     (s₁ : ↑ (# 1) A₁ → ↑ (# 1) A₁) (s₂ : ↑ (# 1) A₂ → ↑ (# 1) A₂) →
       (∀ n₁ n₂ → n₁ ≡ cast n₂ → s₁ n₁ ≡ cast (s₂ n₂)) →
     n₁ A₁ z₁ s₁ ≡ cast (n₂ A₂ z₂ s₂))) λ _ →
    ↑ (# 1) ⊤

  Isomorphic-inductive-natural-numbers = refl

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import common
open import syntx
open import derivability

{- Helper functions to compute the arity of a rule given the arity of the symbol. -}

SStoJS : SyntaxSort → JudgmentSort
SStoJS Ty = Ty
SStoJS Tm = Tm

TArityArgs : SyntaxArityArgs → JudgmentArityArgs
TArityArgs [] = []
TArityArgs (ar , (n , k)) = TArityArgs ar , (n , SStoJS k)

TArity : SyntaxArity → JudgmentArity
TArity ar = (TArityArgs (args ar) , SStoJS (sort ar))

SStoJS= : SyntaxSort → JudgmentSort
SStoJS= Ty = Ty=
SStoJS= Tm = Tm=

CArityArgs : SyntaxArityArgs → JudgmentArityArgs
CArityArgs [] = []
CArityArgs (ar , (n , k)) = CArityArgs ar , (n , SStoJS= k)

CArity : SyntaxArity → JudgmentArity
CArity ar = (CArityArgs (args ar) , SStoJS= (sort ar))

{-
[↑DerivationRule r] extends the derivation rule [r] to an extended signature.
This is easy because derivation rules were designed to be extendable.
-}
↑DerivationRule : {Σ : Signature} {sar : SyntaxArity} {jar : JudgmentArity}
                → DerivationRule Σ jar → DerivationRule (ExtSig Σ sar) jar
rule (↑DerivationRule r) ↑ Γ = rule r (Ext→ ↑) Γ

{- Record combining the typing and congruence rules for a new symbol. -}
record DerivationRules {Σ : Signature} (E : DerivabilityStructure Σ) (ar : SyntaxArity) : Set₁ where
  field
    typingdrule     : DerivationRule (ExtSig Σ ar) (TArity ar)
    congruencedrule : DerivationRule (ExtSig Σ ar) (CArity ar)
open DerivationRules public

{-
[extend E tc] extends the derivability structure [E] to an extended signature, where [tc] is the
typing/congruence rules of a new symbol. We also use a custom data type in order to add the two new
rules, in order to get something readable.
-}

data ExtT (A : JudgmentArity → Set) (sar : SyntaxArity) : JudgmentArity → Set where
  typingrule : ExtT A sar (TArity sar)
  prev : {jar : JudgmentArity} → A jar → ExtT A sar jar

data ExtC (A : JudgmentArity → Set) (sar : SyntaxArity) : JudgmentArity → Set where
  congruencerule : ExtC A sar (CArity sar)
  prev : {jar : JudgmentArity} → A jar → ExtC A sar jar

extend : {Σ : Signature} (E : DerivabilityStructure Σ)
         {ar : SyntaxArity}
         (tc : DerivationRules E ar)
         → DerivabilityStructure (ExtSig Σ ar)

Rules (extend E {ar} tc) S  = Rules E S
Rules (extend E {ar} tc) T  = ExtT (Rules E T) ar
Rules (extend E {ar} tc) C  = ExtC (Rules E C) ar
Rules (extend E {ar} tc) Eq = Rules E Eq
derivationRule (extend E tc) {t = S} r = ↑DerivationRule (derivationRule E r)
derivationRule (extend E tc) {t = T} (prev r) = ↑DerivationRule (derivationRule E r)
derivationRule (extend E tc) {t = T} typingrule = typingdrule tc
derivationRule (extend E tc) {t = C} (prev r) = ↑DerivationRule (derivationRule E r)
derivationRule (extend E tc) {t = C} congruencerule = congruencedrule tc
derivationRule (extend E tc) {t = Eq} r = ↑DerivationRule (derivationRule E r)

-- data Ext (A : Tag → JudgmentArity → Set) (sar : SyntaxArity) : Tag → JudgmentArity → Set where
--   typingrule : Ext A sar T (TArity sar)
--   congruencerule : Ext A sar C (CArity sar)
--   prev : {t : Tag} {jar : JudgmentArity} → A t jar → Ext A sar t jar

-- extend : {Σ : Signature} (E : DerivabilityStructure Σ)
--          {ar : SyntaxArity}
--          (tc : DerivationRules E ar 0)
--          → DerivabilityStructure (ExtSig Σ ar)
-- Rules (extend E {ar} tc) = Ext (Rules E) ar
-- derivationRule (extend E tc) typingrule = typingdrule tc
-- derivationRule (extend E tc) congruencerule = congruencedrule tc
-- derivationRule (extend E tc) (prev r) = ↑DerivationRule (derivationRule E r)

{- Typing rules for basic metavariables (simply a derivable type in the empty context) -}

record BMTypingRule {Σ : Signature} (E : DerivabilityStructure Σ) : Set where
  constructor _/_
  field
    type : TyExpr Σ 0
    der : Derivable E {Γ = ◇} (◇ ⊢ type)
open BMTypingRule public

{- The derivation rules corresponding to a basic metavariable (on the extended signature). -}

BMRules : {Σ : Signature} {E : DerivabilityStructure Σ}
          (t : BMTypingRule E)
          → DerivationRules E ([] , Tm)
rule (typingdrule     (BMRules t)) ↑ Γ [] = return (◇ ⊢ (↑ $ new) []
                                                      :> ↑Expr (Ext→ ↑) (weaken0 (type t)))
rule (congruencedrule (BMRules t)) ↑ Γ [] = return (◇ ⊢ (↑ $ new) [] == (↑ $ new) []
                                                      :> ↑Expr (Ext→ ↑) (weaken0 (type t)))

-- --------------    -----------------
--   Γ ⊢ s : A         Γ ⊢ s = s : A

{-
The premises of a typing rule for a metavariables form essentially a list of typing rules for basic
metavariables in increasingly extended signatures. There are two different ways to order the premises:
- either we have the first premise, and then the rest in an extended signature,
- or we have all but the last premises, and then the last one in a signature extended by all the
  previous ones.

The first option looks simpler, but we use the second option because we will need to talk about
multiple substitution later anyway, and also it allows us to keep typing rules in the empty context.

The type [MTypingRulePremises E n] represents a list of length [n] of such premises. It is defined
simultaneously with multiple substitution: [extend^BM E ts] represents the derivability structure
[E] extended by all the basic metavariables of [ts].
-}

data MTypingRulePremises : {Σ : Signature} (E : DerivabilityStructure Σ) (n : ℕ) → Set

extend^BM : {Σ : Signature} (E : DerivabilityStructure Σ) {n : ℕ} (ts : MTypingRulePremises E n)
          → DerivabilityStructure (ExtSig^ Σ (MArityArgs n))

data MTypingRulePremises where
  [] : ∀ {Σ} {E : DerivabilityStructure Σ} → MTypingRulePremises E 0
  _,_ : ∀ {Σ} {E : DerivabilityStructure Σ} {n : ℕ}
      → (ts : MTypingRulePremises E n)
      → (t : BMTypingRule (extend^BM E ts))
      → MTypingRulePremises E (suc n)

extend^BM E [] = E
extend^BM E (ts , t) = extend (extend^BM E ts) (BMRules t)

{-
[MTypingRule E n k] represents typing rules in derivability structure [E] for a metavariable of
arity (n , k).
There are two cases depending on [k]:
- if [k] is [Ty], then we simply need a list of premises,
- if [k] is [Tm], then we need a list of premises and a type for the conclusion, in the correctly
  extended derivability structure.
-}

data MTypingRule {Σ : Signature} (E : DerivabilityStructure Σ) (n : ℕ) : (k : SyntaxSort) → Set where
  Ty : MTypingRulePremises E n → MTypingRule E n Ty
  Tm : (ts : MTypingRulePremises E n) → BMTypingRule (extend^BM E ts) → MTypingRule E n Tm

{-
Γ, n : ℕ, y : P n ⊢ dS : P (n + 1)

◇ ⊢ _n : ℕ
◇ ⊢ _y : P _n
----------------------------
◇ ⊢ dS(_n , _y) : P (_n + 1)

Γ ⊢ n = m : ℕ
Γ ⊢ u = v : P n
-----------
Γ ⊢ dS(n , u) = dS(m , v) : P (n + 1)

Γ ⊢ 3 : ℕ
Γ ⊢ u : P 3
~~~>
Γ ⊢ dS(3 , u) : P (3 + 1)

(n : ℕ, y : P n)

-}

{-
The derivation rules associated to a typing rule for a metavariable.
-}

MTypingRule-TArgs : {Σ Σ' : Signature} (E : DerivabilityStructure Σ) {n m : ℕ} (↑ : (Σ →Sig Σ') m) {Γ : Ctx Σ' m}
                   (ts : MTypingRulePremises E n) (js : DerivationRulePremises Σ' Γ (TArityArgs (MArityArgs n)))
                   → Partial (Args Σ' m (MArityArgs n))
MTypingRule-TArgs E ↑ [] [] = return []
MTypingRule-TArgs E ↑ (ts , t) (js , ◇ ⊢ a :> A) = do
  as ← MTypingRule-TArgs E ↑ ts js
  assume (A ≡ ↑Expr (SubstM ↑ as) (weaken0 (type t)))
  return (as , a)

MTypingRule-TRule : {Σ : Signature} (E : DerivabilityStructure Σ) {n : ℕ} {k : SyntaxSort}
                    (t : MTypingRule E n k)
                    → DerivationRule (ExtSig Σ (MArity n k)) (TArity (MArity n k))
rule (MTypingRule-TRule E (Ty ts)) ↑ Γ js = do
  as ← MTypingRule-TArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as)
rule (MTypingRule-TRule E (Tm ts t)) ↑ Γ js = do
  as ← MTypingRule-TArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as :> ↑Expr (SubstM (Ext→ ↑) as) (weaken0 (type t)))

MTypingRule-CArgs : {Σ Σ' : Signature} (E : DerivabilityStructure Σ) {n m : ℕ} (↑ : (Σ →Sig Σ') m) {Γ : Ctx Σ' m}
                   (ts : MTypingRulePremises E n) (js : DerivationRulePremises Σ' Γ (CArityArgs (MArityArgs n)))
                   → Partial (Args Σ' m (MArityArgs n) × Args Σ' m (MArityArgs n))
MTypingRule-CArgs E ↑ [] [] = return ([] , [])
MTypingRule-CArgs E ↑ (ts , t) (js , ◇ ⊢ a == a' :> A) = do
  (as , as') ← MTypingRule-CArgs E ↑ ts js
  assume (A ≡ ↑Expr (SubstM ↑ as) (weaken0 (type t)))
  return ((as , a) , (as' , a'))

MTypingRule-CRule : {Σ : Signature} (E : DerivabilityStructure Σ) {n : ℕ} {k : SyntaxSort}
                    (t : MTypingRule E n k)
                    → DerivationRule (ExtSig Σ (MArity n k)) (CArity (MArity n k))
rule (MTypingRule-CRule E (Ty ts)) ↑ Γ js = do
  (as , as') ← MTypingRule-CArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as == (↑ $ new) as')
rule (MTypingRule-CRule E (Tm ts t)) ↑ Γ js = do
  (as , as') ← MTypingRule-CArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as == (↑ $ new) as' :> ↑Expr (SubstM (Ext→ ↑) as) (weaken0 (type t)))

MRules : {Σ : Signature} {E : DerivabilityStructure Σ} {n : ℕ} {k : SyntaxSort}
                    (t : MTypingRule E n k)
                    → DerivationRules E (MArity n k)
typingdrule (MRules t) = MTypingRule-TRule _ t
congruencedrule (MRules t) = MTypingRule-CRule _ t

{-
General typing rules are very similar to typing rules of metavariables, except that they are using
[MTypingRule] instead of [BMTypingRule] for the premises.
-}

data TypingRulePremises : {Σ : Signature} (E : DerivabilityStructure Σ) (args : SyntaxArityArgs) → Set

extend^M : {Σ : Signature} (E : DerivabilityStructure Σ) {args : SyntaxArityArgs} (ts : TypingRulePremises E args) → DerivabilityStructure (ExtSig^ Σ args)

data TypingRulePremises where
  [] : ∀ {Σ} {E : DerivabilityStructure Σ} → TypingRulePremises E []
  _,_ : ∀ {Σ} {E : DerivabilityStructure Σ} {args : SyntaxArityArgs} {m : ℕ} {k : SyntaxSort}
      → (ts : TypingRulePremises E args)
      → (t : MTypingRule (extend^M E ts) m k)
      → TypingRulePremises E (args , (m , k))

extend^M E [] = E
extend^M E (ts , t) = extend (extend^M E ts) (MRules t)

data TypingRule {Σ : Signature} (E : DerivabilityStructure Σ) (args : SyntaxArityArgs) : (k : SyntaxSort) → Set where
  Ty : TypingRulePremises E args → TypingRule E args Ty
  Tm : (ts : TypingRulePremises E args) → BMTypingRule (extend^M E ts) → TypingRule E args Tm

{- The derivation rules associated to a typing rule. -}

{- List of all the last [n] variables in scope [m + n] -}
Vars : {Σ : Signature} {n : ℕ} (m : ℕ) → Args Σ (m + n) (MArityArgs n)
Vars {n = zero} m = []
Vars {n = suc n} m = weakenA {{≤-+ {m + n} {1}}} last (Vars m) , var last

{-
[check-DepCtx ↑ as ts Δ] checks that the premises [ts] correspond to the dependent context [Δ],
where [as] corresponds to the interpretations of the metavariables.
-}
check-DepCtx : {Σ Σ' : Signature} {m n : ℕ} {args : SyntaxArityArgs}
               {E : DerivabilityStructure (ExtSig^ Σ args)}
               → (Σ →Sig Σ') m → Args Σ' m args
               → MTypingRulePremises E n → DepCtx Σ' m n → Prop
check-DepCtx ↑ as [] ◇ = ⊤
check-DepCtx {m = m} {n = suc n} ↑ as (ts , t) (Δ , A) =
  ΣP (check-DepCtx ↑ as ts Δ)
  (λ _ → A ≡ ↑Expr (SubstM (liftSig ↑) (weakenAL as)) (↑Expr (SubstM idSig (Vars m)) (weaken0 (type t))))

TypingRule-TArgs : {Σ Σ' : Signature} (E : DerivabilityStructure Σ) {args : SyntaxArityArgs} {m : ℕ} (↑ : (Σ →Sig Σ') m) {Γ : Ctx Σ' m}
                   (ts : TypingRulePremises E args) (js : DerivationRulePremises Σ' Γ (TArityArgs args))
                   → Partial (Args Σ' m args)
TypingRule-TArgs E ↑ [] [] = return []
TypingRule-TArgs E ↑ (ts , Ty t's) (js , Δ ⊢ A) = do
  as ← TypingRule-TArgs E ↑ ts js
  assume (check-DepCtx ↑ as t's Δ)
  return (as , A)
TypingRule-TArgs E {m = m} ↑ (ts , Tm t's t) (_,_ {m = m'} js (Δ ⊢ u :> A)) = do
  as ← TypingRule-TArgs E ↑ ts js
  assume (check-DepCtx ↑ as t's Δ)
  assume (A ≡ ↑Expr (SubstM (liftSig ↑) (weakenAL as)) (↑Expr (SubstM idSig (Vars m)) (weaken0 (type t))))
  return (as , u)

TypingRule-TRule : {Σ : Signature} (E : DerivabilityStructure Σ) {args : SyntaxArityArgs} {k : SyntaxSort}
                   (t : TypingRule E args k)
                   → DerivationRule (ExtSig Σ (args , k)) (TArity (args , k))
rule (TypingRule-TRule E (Ty ts)) ↑ Γ js = do
  as ← TypingRule-TArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as)
rule (TypingRule-TRule E (Tm ts t)) ↑ Γ js = do
  as ← TypingRule-TArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as :> ↑Expr (SubstM (Ext→ ↑) as) (weaken0 (type t)))

TypingRule-CArgs : {Σ Σ' : Signature} (E : DerivabilityStructure Σ) {args : SyntaxArityArgs} {m : ℕ} (↑ : (Σ →Sig Σ') m) {Γ : Ctx Σ' m}
                   (ts : TypingRulePremises E args) (js : DerivationRulePremises Σ' Γ (CArityArgs args))
                   → Partial (Args Σ' m args × Args Σ' m args)
TypingRule-CArgs E ↑ [] [] = return ([] , [])
TypingRule-CArgs E {args = args , (n , Ty)} {m} ↑ (ts , Ty t's) (js , Δ ⊢ A == A') = do
  (as , as') ← TypingRule-CArgs E ↑ ts js
  assume (check-DepCtx ↑ as t's Δ)
  return ((as , A) , (as' , A'))
TypingRule-CArgs E {args = args , (n , Tm)} {m} ↑ (ts , Tm t's t) (js , Δ ⊢ u == u' :> A) = do
  (as , as') ← TypingRule-CArgs E ↑ ts js
  assume (check-DepCtx ↑ as t's Δ)
  assume (A ≡ ↑Expr (SubstM (liftSig ↑) (weakenAL as)) (↑Expr (SubstM idSig (Vars m)) (weaken0 (type t))))
  return ((as , u) , (as' , u'))

TypingRule-CRule : {Σ : Signature} (E : DerivabilityStructure Σ) {args : SyntaxArityArgs} {k : SyntaxSort}
                   (t : TypingRule E args k)
                   → DerivationRule (ExtSig Σ (args , k)) (CArity (args , k))
rule (TypingRule-CRule E (Ty ts)) ↑ Γ js = do
  (as , as') ← TypingRule-CArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as == (↑ $ new) as')
rule (TypingRule-CRule E (Tm ts t)) {n = n} ↑ Γ js = do
  (as , as') ← TypingRule-CArgs E (Ext→ ↑) ts js
  return (◇ ⊢ (↑ $ new) as == (↑ $ new) as' :> ↑Expr (SubstM (Ext→ ↑) as) (weaken0 (type t)))

TRules : {Σ : Signature} {E : DerivabilityStructure Σ} {ar : SyntaxArity}
        (t : TypingRule E (args ar) (sort ar))
        → DerivationRules E ar
typingdrule (TRules t) = TypingRule-TRule _ t
congruencedrule (TRules t) = TypingRule-CRule _ t

{-
Γ ⊢ A == A'
Γ , x : A ⊢ B == B'
--------------------
Γ ⊢ Π A B == Π A' B'
-}

{- Equality rules -}

{-
[extendE E tc] extends the derivability structure with one single (equality) rule
-}

data ExtE (A : JudgmentArity → Set) (nar : JudgmentArity) : JudgmentArity → Set where
  equalityrule : ExtE A nar nar
  prev : {jar : JudgmentArity} → A jar → ExtE A nar jar

extendE : {Σ : Signature} (E : DerivabilityStructure Σ)
          {ar : JudgmentArity}
          (tc : DerivationRule Σ ar)
          → DerivabilityStructure Σ
Rules (extendE E {ar} tc) S = Rules E S
Rules (extendE E {ar} tc) T = Rules E T
Rules (extendE E {ar} tc) C = Rules E C
Rules (extendE E {ar} tc) Eq = ExtE (Rules E Eq) ar
derivationRule (extendE E tc) {S} r = derivationRule E r
derivationRule (extendE E tc) {T} r = derivationRule E r
derivationRule (extendE E tc) {C} r = derivationRule E r
derivationRule (extendE E tc) {Eq} (prev r) = derivationRule E r
derivationRule (extendE E tc) {Eq} equalityrule = tc

-- data ExtE (A : Tag → JudgmentArity → Set) (nar : JudgmentArity) : Tag → JudgmentArity → Set where
--   equalityrule : ExtE A nar Eq nar
--   prev : {t : Tag} {jar : JudgmentArity} → A t jar → ExtE A nar t jar

-- extendE : {Σ : Signature} (E : DerivabilityStructure Σ)
--           {ar : JudgmentArity}
--           (tc : {n : ℕ} → DerivationRule Σ ar n)
--           → DerivabilityStructure Σ
-- Rules (extendE E {ar} tc) = ExtE (Rules E) ar
-- derivationRule (extendE E tc) (prev r) = derivationRule E r
-- derivationRule (extendE E tc) equalityrule = tc

record TermEquality {Σ : Signature} (E : DerivabilityStructure Σ) : Set where
  constructor _<:_/_//_/_
  field
    type : TyExpr Σ 0
    term1 : TmExpr Σ 0
    der1 : Derivable E {Γ = ◇} (◇ ⊢ term1 :> type)
    term2 : TmExpr Σ 0
    der2 : Derivable E {Γ = ◇} (◇ ⊢ term2 :> type)
open BMTypingRule public

data EqualityRule {Σ : Signature} (E : DerivabilityStructure Σ) (args : SyntaxArityArgs) : (k : SyntaxSort) → Set where
  Ty= : (ts : TypingRulePremises E args) (A B : BMTypingRule (extend^M E ts)) → EqualityRule E args Ty
  Tm= : (ts : TypingRulePremises E args) (A : TermEquality (extend^M E ts)) → EqualityRule E args Tm

ERule : {Σ : Signature} {E : DerivabilityStructure Σ} {args : SyntaxArityArgs} {k : SyntaxSort}
        → EqualityRule E args k
        → DerivationRule Σ (TArityArgs args , SStoJS= k)
rule (ERule {E = E} (Ty= ts A B)) ↑ Γ js = do
  as ← TypingRule-TArgs E ↑ ts js
  return (◇ ⊢ (↑Expr (SubstM ↑ as) (weaken0 (A .type))) == (↑Expr (SubstM ↑ as) (weaken0 (B .type))))
rule (ERule {E = E} (Tm= ts (A <: u / _ // v / _))) ↑ Γ js = do
  as ← TypingRule-TArgs E ↑ ts js
  return (◇ ⊢ (↑Expr (SubstM ↑ as) (weaken0 u)) == (↑Expr (SubstM ↑ as) (weaken0 v)) :> ↑Expr (SubstM ↑ as) (weaken0 A))

max_stars_repo_name: guillaumebrunerie/general-type-theories

max_issues_repo_name: guillaumebrunerie/general-type-theories

max_forks_repo_name: guillaumebrunerie/general-type-theories


text:
compose : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
        → (B → C)
        → (A → B)
        → A → C
compose f g x = f (g x)

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
module Generic.Lib.Data.String where

open import Data.String.Base using (String) renaming (toList to toListˢ; _++_ to _++ˢ_) public

open import Generic.Lib.Decidable
import Data.String as String

instance
  StringEq : Eq String
  StringEq = viaBase String._≟_

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Setoids
open import Functions.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Setoids.Orders.Total.Definition where

open import Setoids.Orders.Partial.Definition

record SetoidTotalOrder {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (P : SetoidPartialOrder S _<_) : Set (a ⊔ b ⊔ c) where
  open Setoid S
  field
    totality : (a b : A) → ((a < b) || (b < a)) || (a ∼ b)
  partial : SetoidPartialOrder S _<_
  partial = P
  min : A → A → A
  min a b with totality a b
  min a b | inl (inl a<b) = a
  min a b | inl (inr b<a) = b
  min a b | inr a=b = a
  max : A → A → A
  max a b with totality a b
  max a b | inl (inl a<b) = b
  max a b | inl (inr b<a) = a
  max a b | inr a=b = b

totalOrderToSetoidTotalOrder : {a b : _} {A : Set a} (T : TotalOrder {a} A {b}) → SetoidTotalOrder (partialOrderToSetoidPartialOrder (TotalOrder.order T))
SetoidTotalOrder.totality (totalOrderToSetoidTotalOrder T) = TotalOrder.totality T


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  A : Set
  a : A

record R : Set where
  constructor c
  field f : A
open R

postulate
  r : R
  rew₁ : ∀ x → c x ≡ r

{-# REWRITE rew₁ #-}

postulate
  g : A → A
  rew₂ : g (f r) ≡ a

{-# REWRITE rew₂ #-}

postulate
  rew₃ : f r ≡ a

{-# REWRITE rew₃ #-}


text:
------------------------------------------------------------------------------
-- Theorems which require a non-empty domain
------------------------------------------------------------------------------

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

module FOL.NonEmptyDomain.TheoremsI where

-- The theorems below are valid on intuitionistic logic.
open import FOL.Base hiding ( pem )

------------------------------------------------------------------------------
-- We postulate some formulae and propositional functions.
postulate
  A  : Set
  A¹ : D → Set

∀→∃ : (∀ {x} → A¹ x) → ∃ A¹
∀→∃ h = D≢∅ , h

-- Let A be a formula. If x is not free in A then ⊢ (∃x)A ↔ A
-- (Mendelson 1997, proposition 2.18 (b), p. 70).
∃-erase-add₁ : (∃[ _ ] A) ↔ A
∃-erase-add₁ = l→r , r→l
  where
  l→r : (∃[ _ ] A) → A
  l→r (_ , a) = a

  r→l : A → (∃[ _ ] A)
  r→l A = D≢∅ , A

-- Quantification over a variable that does not occur can be erased or
-- added.
∀-erase-add : ((x : D) → A) ↔ A
∀-erase-add = l→r , r→l
  where
  l→r : ((x : D) → A) → A
  l→r h = h D≢∅

  r→l : A → (x : D) → A
  r→l a _ = a

∃-erase-add₂ : (∃[ x ] (A ∨ A¹ x)) ↔ A ∨ (∃[ x ] A¹ x)
∃-erase-add₂ = l→r , r→l
  where
  l→r : ∃[ x ] (A ∨ A¹ x) → A ∨ (∃[ x ] A¹ x)
  l→r (x , inj₁ a)   = inj₁ a
  l→r (x , inj₂ A¹x) = inj₂ (x , A¹x)

  r→l : A ∨ (∃[ x ] A¹ x) → ∃[ x ] (A ∨ A¹ x)
  r→l (inj₁ a)         = D≢∅ , inj₁ a
  r→l (inj₂ (x , A¹x)) = x , inj₂ A¹x

------------------------------------------------------------------------------
-- References
--
-- Mendelson, Elliott (1997). Introduction to Mathematical Logic. 4th
-- ed. Chapman & Hall.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Number.Prelude.Int where

open import Cubical.Data.Int public using
  ( Int
  ; fromNatInt
  ; fromNegInt
  ; sucInt
  ; predInt
  ; sucInt+
  ; predInt+
  ; _+pos_
  ; _+negsuc_
  ) renaming
  ( isSetInt to isSetℤ
  ; _-_      to infix 7 _-ᶻ_
  ; _+_      to infix 5 _+ᶻ_
  ; pos      to posᶻ
  ; negsuc   to negsucᶻ
  )
open import Number.Instances.Int public using
  ( +negsuc-identityˡ
  ; negsuc+negsuc≡+ⁿ
  ; sneg
  ; spos
  ) renaming
  ( _·_          to _·ᶻ_
  ; -_           to -ᶻ_
  ; _<_          to _<ᶻ_
  ; min          to minᶻ
  ; max          to maxᶻ
  ; is-min       to is-minᶻ
  ; is-max       to is-maxᶻ
  ; ·-reflects-< to ·ᶻ-reflects-<ᶻ
  ; is-LinearlyOrderedCommRing to is-LinearlyOrderedCommRingᶻ
  )

-- Int≅Builtin
-- Int≡Builtin
-- Sign
-- spos
-- sneg
-- _·ˢ_
-- sign
-- signed
-- -_
-- -involutive
-- _·_
-- _·'_
-- _·''_
-- ·''-nullifiesʳ
-- _<_
-- min
-- max
-- <-irrefl
-- <-trans
-- <-asym
-- <-cotrans
-- +-identityʳ
-- +-identityˡ
-- -1·≡-
-- negsuc≡-pos
-- negsuc-reflects-≡
-- pos-reflects-≡
-- possuc+negsuc≡0
-- sucInt[negsuc+pos]≡0
-- +-inverseʳ
-- +-inverseˡ
-- +-inverse
-- pos+pos≡+ⁿ
-- negsuc+negsuc≡+ⁿ
-- +negsuc-identityˡ
-- pos+negsuc≡⊎
-- negsuc+pos≡⊎
-- pos+negsuc≡negsuc+pos
-- predInt-
-- pos+negsuc-swap
-- negsuc+pos-swap
-- +negsuc-assoc
-- sucInt[negsuc+pos]≡pos
-- +pos-inverse
-- +pos-assoc
-- Trichotomy
-- _≟_
-- MinTrichtotomy
-- MaxTrichtotomy
-- min-trichotomy
-- max-trichotomy
-- is-min
-- is-max
-- sucInt-reflects-<
-- predInt-reflects-<
-- sucInt-preserves-<
-- predInt-preserves-<
-- +-preserves-<
-- +-reflects-<
-- +-reflects-<ˡ
-- +-<-ext
-- ·≡·'
-- ·'-nullifiesʳ
-- ·'-nullifiesˡ
-- -distrˡ
-- ·-comm
-- -distrʳ
-- ·'-assoc
-- ·'-assoc≡
-- ·-assoc
-- ·-nullifiesˡ
-- ·-nullifiesʳ
-- ·-identityˡ
-- ·-identityʳ
-- ·-preserves-<
-- ·-reflects-<
-- ·-sucInt
-- ·-sucIntˡ
-- ·-predInt
-- ·-predIntˡ
-- -distrib
-- ·-distribˡ
-- ·-distribʳ

-- ·-Semigroup .IsSemigroup.is-assoc
-- +-Monoid .IsMonoid.is-identity
-- ·-Monoid .IsMonoid.is-identity
-- is-Semiring .IsSemiring.is-dist
-- <-StrictLinearOrder .IsStrictLinearOrder.is-tricho

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------
-- A coinductive definition of weak similarity
------------------------------------------------------------------------

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

open import Labelled-transition-system

module Similarity.Weak {ℓ} (lts : LTS ℓ) where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Bisimilarity.Weak lts as WB using ([_]_≈_; [_]_≈′_)
open import Expansion lts as E using ([_]_≳_; [_]_≳′_)
open import Indexed-container hiding (⟨_⟩)
open import Relation
open import Similarity lts as S using ([_]_≤_; [_]_≤′_)
import Similarity.General

open LTS lts

private
  module General = Similarity.General lts _[_]⇒̂_ ⟶→⇒̂

open General public
  using (module StepC; ⟨_⟩; challenge; force;
         [_]_≡_; [_]_≡′_; []≡↔; Extensionality; extensionality)
  renaming ( reflexive-≤ to reflexive-≼
           ; reflexive-≤′ to reflexive-≼′
           ; ≡⇒≤ to ≡⇒≼
           ; ≤:_ to ≼:_
           ; ≤′:_ to ≼′:_
           )

-- StepC is given in the following way, rather than via open public,
-- to make hyperlinks to it more informative.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = General.StepC

-- The following definitions are given explicitly, in order to make
-- the code easier to follow.

Weak-similarity : Size → Rel₂ ℓ Proc
Weak-similarity = ν StepC

Weak-similarity′ : Size → Rel₂ ℓ Proc
Weak-similarity′ = ν′ StepC

infix 4 [_]_≼_ [_]_≼′_ _≼_ _≼′_

[_]_≼_ : Size → Proc → Proc → Type ℓ
[ i ] p ≼ q = ν StepC i (p , q)

[_]_≼′_ : Size → Proc → Proc → Type ℓ
[ i ] p ≼′ q = ν′ StepC i (p , q)

_≼_ : Proc → Proc → Type ℓ
_≼_ = [ ∞ ]_≼_

_≼′_ : Proc → Proc → Type ℓ
_≼′_ = [ ∞ ]_≼′_

private

  -- However, these definitions are definitionally equivalent to
  -- corresponding definitions in General.

  indirect-Weak-similarity : Weak-similarity ≡ General.Similarity
  indirect-Weak-similarity = refl

  indirect-Weak-similarity′ : Weak-similarity′ ≡ General.Similarity′
  indirect-Weak-similarity′ = refl

  indirect-[]≼ : [_]_≼_ ≡ General.[_]_≤_
  indirect-[]≼ = refl

  indirect-[]≼′ : [_]_≼′_ ≡ General.[_]_≤′_
  indirect-[]≼′ = refl

  indirect-≼ : _≼_ ≡ General._≤_
  indirect-≼ = refl

  indirect-≼′ : _≼′_ ≡ General._≤′_
  indirect-≼′ = refl

mutual

  -- Weak bisimilarity is contained in weak similarity.

  ≈⇒≼ : ∀ {i p q} → [ i ] p ≈ q → [ i ] p ≼ q
  ≈⇒≼ = λ p≈q →
    ⟨ (λ q⟶q′ →
         let p′ , p⇒̂p′ , p′≈′q′ = WB.left-to-right p≈q q⟶q′
         in p′ , p⇒̂p′ , ≈⇒≼′ p′≈′q′)
    ⟩

  ≈⇒≼′ : ∀ {i p q} → [ i ] p ≈′ q → [ i ] p ≼′ q
  force (≈⇒≼′ p≳′q) = ≈⇒≼ (S.force p≳′q)

mutual

  -- Similarity is contained in weak similarity.

  ≤⇒≼ : ∀ {i p q} → [ i ] p ≤ q → [ i ] p ≼ q
  ≤⇒≼ = λ p≤q →
    ⟨ (λ q⟶q′ →
         let p′ , p⟶p′ , p′≤′q′ = S.challenge p≤q q⟶q′
         in p′ , ⟶→⇒̂ p⟶p′ , ≤⇒≼′ p′≤′q′)
    ⟩

  ≤⇒≼′ : ∀ {i p q} → [ i ] p ≤′ q → [ i ] p ≼′ q
  force (≤⇒≼′ p≳′q) = ≤⇒≼ (S.force p≳′q)

-- Weak similarity is a weak simulation (of a certain kind).

weak-is-weak⇒̂ :
  ∀ {p p′ q μ} →
  p ≼ q → p [ μ ]⇒̂ p′ →
  ∃ λ q′ → q [ μ ]⇒̂ q′ × p′ ≼ q′
weak-is-weak⇒̂ = is-weak⇒̂ challenge (λ p≼′q → force p≼′q) ⇒̂→⇒ id

mutual

  -- Weak similarity is transitive.
  --
  -- Note that the size of the second argument is not preserved.
  --
  -- TODO: Can one prove that the size cannot be preserved?

  transitive-≼ : ∀ {i p q r} → [ i ] p ≼ q → q ≼ r → [ i ] p ≼ r
  transitive-≼ p≼q q≼r =
    ⟨ (λ p⟶p′ →
         let q′ , q⇒̂q′ , p′≼q′ = challenge p≼q p⟶p′
             r′ , r⇒̂r′ , q′≼r′ = weak-is-weak⇒̂ q≼r q⇒̂q′
         in r′ , r⇒̂r′ , transitive-≼′ p′≼q′ q′≼r′)
    ⟩

  transitive-≼′ :
    ∀ {i p q r} → [ i ] p ≼′ q → q ≼ r → [ i ] p ≼′ r
  force (transitive-≼′ p≼q q≼r) = transitive-≼ (force p≼q) q≼r

mutual

  -- A fully size-preserving transitivity-like lemma.
  --
  -- Note that expansion could be replaced by a kind of one-sided
  -- expansion.

  transitive-≳≼ : ∀ {i p q r} → [ i ] p ≳ q → [ i ] q ≼ r → [ i ] p ≼ r
  transitive-≳≼ p≳q q≼r =
    ⟨ (λ p⟶p′ → case E.left-to-right p≳q p⟶p′ of λ where
                  (_ , done s , p′≳q) →
                    _ , silent s done
                      , transitive-≳≼′
                          p′≳q (record { force = λ { {_} → q≼r } })

                  (q′ , step q⟶q′ , p′≳q′) →
                    let r′ , r⇒̂r′ , q′≼r′ = challenge q≼r q⟶q′
                    in r′ , r⇒̂r′ , transitive-≳≼′ p′≳q′ q′≼r′)
    ⟩

  transitive-≳≼′ :
    ∀ {i p q r} → [ i ] p ≳′ q → [ i ] q ≼′ r → [ i ] p ≼′ r
  force (transitive-≳≼′ p≼q q≼r) =
    transitive-≳≼ (force p≼q) (force q≼r)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Implicits.Everything where

-- common agda stdlib imports
open import Prelude

--
-- Oliveira's calculi in Agda
--

-- We give a well-scoped version of Oliveira's ambiguous and deterministic
-- resolution rules
open import Implicits.Resolution.Ambiguous.Resolution
open import Implicits.Resolution.Deterministic.Resolution

-- and prove soundness of det. resolution w.r.t the ambiguous one
open import Implicits.Resolution.Deterministic.Expressiveness

-- we show that Oliveira's deterministic rules are incomplete w.r.t.
-- the ambiguous resolution
open import Implicits.Resolution.Deterministic.Incomplete

-- and prove ambiguous resolution undecidable
open import Implicits.Resolution.Ambiguous.SystemFEquiv
open import Implicits.Resolution.Ambiguous.Undecidable

--
-- Partial resolution
--

-- We maintain the syntax-directedness of the rules and strenghten the hypothesis of r-simp
-- to circumvent the weakness of Oliveira's deterministic rules.
-- In order to maintain strict-positiveness of the rules, we drop determinacy.
-- We will regain determinacy in the algorithmic description of resolution.
open import Implicits.Resolution.Infinite.Resolution

-- We first show that the rules are isomorphic to EBNF System F expressions
-- and use it to prove that infinite resolution is complete w.r.t. ambiguous resolution.
open import Implicits.Resolution.Infinite.NormalFormEquiv
open import Implicits.Resolution.Infinite.Expressiveness

-- Furthermore we give a partial algorithm for infinite resolution.
-- We have soundness and develop partial completeness for this algorithm.
open import Implicits.Resolution.Infinite.Algorithm
open import Implicits.Resolution.Infinite.Algorithm.Soundness
-- open import Implicits.Resolution.Infinite.Algorithm.Completeness

-- We'd love to show that the existence of a finite resolution Δ ⊢ᵣ r guarantees
-- termination of the partial resolution algorithm on input r;
-- but this clearly isn't a theorem: it's easy to imagine an implicit context that both has
-- a diverging 'trap' for the deterministic algorithm but also allows a finite 'shortcut'
-- derivation (hiding behind the trap).
-- In fact, the fact that infinite resolution is complete w.r.t. Ambiguous resolution,
-- indirectly proves that it's undecidable.

-- Instead we define a version of infinite resolution with a generic termination condition
open import Implicits.Resolution.GenericFinite.TerminationCondition
open import Implicits.Resolution.GenericFinite.Resolution
open import Implicits.Resolution.GenericFinite.Expressiveness

-- We give a total algorithm and prove it sound
open import Implicits.Resolution.GenericFinite.Algorithm
open import Implicits.Resolution.GenericFinite.Algorithm.Soundness
-- and develop completeness; finished modulo 2 lemmas
-- open import Implicits.Resolution.GenericFinite.Algorithm.Completeness

-- We provide two examples of termination conditions
-- A simple "maximum depth" condition like Coq's auto tactic has:
open import Implicits.Resolution.GenericFinite.Examples.MaximumDepth
-- And basically a termination condition inspired by Haskell's conditions on
-- typeclasses, developed by Oliveira et al.
-- Importantly we prove that the resulting calculus is more expressive than
-- Oliveira's deterministic resolution
open import Implicits.Resolution.GenericFinite.Examples.Haskell

-- We define a denotation semantics for the entire calculus -- into System F.
-- To this end we develop System F:
open import SystemF.Syntax
open import SystemF.WellTyped
open import SystemF.SmallStep
open import SystemF.NormalForm

-- The actual semantics is implemented aa module that depends on
-- the semantics for your favorite flavor of resolution.
-- It includes a proof that the translation preserves the typing relation.
open import Implicits.Semantics.Preservation
open import Implicits.Semantics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

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

module Relation.Nullary where

open import Agda.Builtin.Equality

open import Data.Bool.Base
open import Data.Empty hiding (⊥-elim)
open import Data.Empty.Irrelevant
open import Level

------------------------------------------------------------------------
-- Negation.

infix 3 ¬_
infix 2 _because_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥

------------------------------------------------------------------------
-- `Reflects` idiom.

-- The truth value of P is reflected by a boolean value.

data Reflects {p} (P : Set p) : Bool → Set p where
  ofʸ : ( p :   P) → Reflects P true
  ofⁿ : (¬p : ¬ P) → Reflects P false

------------------------------------------------------------------------
-- Decidability.

-- Decidability proofs have two parts: the `does` term which contains
-- the boolean result and the `proof` term which contains a proof that
-- reflects the boolean result. This definition allows the boolean
-- part of the decision procedure to compute independently from the
-- proof. This leads to better computational behaviour when we only care
-- about the result and not the proof. See README.Decidability for
-- further details.

record Dec {p} (P : Set p) : Set p where
  constructor _because_
  field
    does  : Bool
    proof : Reflects P does

open Dec public

pattern yes p =  true because ofʸ  p
pattern no ¬p = false because ofⁿ ¬p

-- Given an irrelevant proof of a decidable type, a proof can
-- be recomputed and subsequently used in relevant contexts.
recompute : ∀ {a} {A : Set a} → Dec A → .A → A
recompute (yes x) _ = x
recompute (no ¬p) x = ⊥-elim (¬p x)

------------------------------------------------------------------------
-- Irrelevant types

Irrelevant : ∀ {p} → Set p → Set p
Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂


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

module DTLC.Base where

open import Cubical.Foundations.Prelude hiding (Σ; _,_)
open import Cubical.Foundations.Function

--------------------------------------------------------------------------
-- Adapted from: Type Theory in Type Theory using Quotient Inductive Types
--               by Thorsten Altenkirch and Ambrus Kaposi
-- See: http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf
--
-- Note: We have changed a number of names relative to this paper, in the
--  interest of clarity. In particular, Tms is now _~>_, with the
--  arguments reversed. Thus, _∘_ (which we call _∘*_) also is reversed
--  with respect to [AK16]. Furthermore, we renamed π₁ to tail*, π₂
--  to head*, and app to unlam to make their functions more clear.
--------------------------------------------------------------------------

infixl 6 _,_
infixl 6 _,*_
infixr 5 _∘*_

PathPSyntax = PathP
syntax PathPSyntax A x y = x ≡[ A ]≡ y
infix 2 PathPSyntax

-----------------
-- Declarations
-----------------

-- We will mutually inductively define:

-- The type of contexts
data Ctx : Type₀

-- The type of types
data Typ : Ctx -> Type₀

-- The type of judgements x : τ ⊣ Γ ("x has type τ in context Γ")
Term : (Γ : Ctx) -> Typ Γ -> Type₀
syntax Term Γ τ = τ ⊣ Γ

-- The type of transformations / generalized subsitutions between contexts
_~>_ : Ctx -> Ctx -> Type₀

-- ...in fact, we define terms and transformations together:

data TmQV : Type₀ where
  TmV : TmQV
  TrV : TmQV

TmQArg : TmQV -> Ctx -> Type₀
TmQArg TmV Γ = Typ Γ
TmQArg TrV _ = Ctx

data TmQ : (a : TmQV) -> (Γ : Ctx) -> TmQArg a Γ -> Type₀

Term = TmQ TmV
_~>_ = TmQ TrV

-- Some forward declarations:
id* : ∀ {Γ} -> Γ ~> Γ
_∘*_ : ∀ {Γ Δ Σ} -> (Δ ~> Σ) -> (Γ ~> Δ) -> Γ ~> Σ
_[_]T : ∀ {Γ Δ} (τ : Typ Γ) (f : Γ ~> Δ) -> Typ Δ
_[_] : ∀ {Γ Δ τ} (x : τ ⊣ Γ) (f : Γ ~> Δ) -> (τ [ f ]T) ⊣ Δ

----------------
-- Definitions
----------------

data Ctx where
  ∙ : Ctx
  _,_ : (Γ : Ctx) -> Typ Γ -> Ctx

-- Unlike Altenkirch-Kaposi, we have a universe of types U:
data Typ where
  U : ∀ {Γ} -> Typ Γ
  type : ∀ {Γ} (τ : U ⊣ Γ) -> Typ Γ

-- Subsitution on types is defined in terms of substition on terms!
U [ f ]T = U
(type τ) [ f ]T = type (τ [ f ])

-- Substitution on types is a functor -- definitions are below
[id]T : ∀ {Γ} (τ : Typ Γ) -> τ [ id* ]T ≡ τ
[][]T : ∀ {Γ Δ Σ} (g : Δ ~> Σ) (f : Γ ~> Δ) (τ : Typ Γ)
        -> τ [ f ]T [ g ]T ≡ τ [ g ∘* f ]T

-- Having these is quite useful for readibility:

coeTm : ∀ {Γ} {x y : Typ Γ} -> x ≡ y -> Term Γ x -> Term Γ y
coeTm p = transport (cong (Term _) p)

coeTmTy : ∀ {Γ} {τ σ : Term Γ U} -> τ ≡ σ -> Term Γ (type τ) -> Term Γ (type σ)
coeTmTy p = transport (cong (Term _ ∘ type) p)

-- We define terms and transformations together
data TmQ where

  -- Ctx and ~> form a category
  -- Note: these are the definitions of id* and ∘* -- see below
  id*C : ∀ {Γ} -> Γ ~> Γ
  _∘*C_ : ∀ {Γ Δ Σ} -> (Δ ~> Σ) -> (Γ ~> Δ) -> Γ ~> Σ

  id*-l : ∀ {Γ Δ} (f : Γ ~> Δ) -> id* ∘* f ≡ f
  id*-r : ∀ {Γ Δ} (f : Γ ~> Δ) -> f ∘* id* ≡ f
  assoc : ∀ {Γ Δ Σ P} (h : Σ ~> P) (g : Δ ~> Σ) (f : Γ ~> Δ)
          -> (h ∘* g) ∘* f ≡ h ∘* (g ∘* f)

  -- ~> has a list structure on its first argument
  ∙* : ∀ {Δ} -> ∙ ~> Δ
  _,*_ : ∀ {Γ Δ τ} (f : Γ ~> Δ) (x : Term Δ (τ [ f ]T)) -> (Γ , τ) ~> Δ

  tail* : ∀ {Γ Δ τ} (f : (Γ , τ) ~> Δ) -> Γ ~> Δ
  head* : ∀ {Γ Δ τ} (f : (Γ , τ) ~> Δ) -> (τ [ tail* f ]T) ⊣ Δ

  ,*-∘* : ∀ {Γ Δ Σ τ} (g : Δ ~> Σ) (f : Γ ~> Δ) (x : Term Δ (τ [ f ]T))
          -> g ∘* (f ,* x) ≡ (g ∘* f) ,* coeTm ([][]T g f τ) (x [ g ])

  -- Computation rules for tail* and head*
  tail*-β : ∀ {Γ Δ τ} (f : Γ ~> Δ) (x : Term Δ (τ [ f ]T)) -> tail* (f ,* x) ≡ f
  head*-β : ∀ {Γ Δ τ} (f : Γ ~> Δ) (x : Term Δ (τ [ f ]T))
            -> head* (f ,* x) ≡[ (λ i → (τ [ tail*-β f x i ]T) ⊣ Δ) ]≡ x

  -- Uniqueness rules for ~>
  ∙*-η : ∀ {Δ} (f : ∙ ~> Δ) -> f ≡ ∙*
  ,*-η : ∀ {Γ Δ τ} (f : (Γ , τ) ~> Δ) -> (tail* f ,* head* f) ≡ f

  -- A useful combinator, defined in terms of the above
  _↑_ : ∀ {Γ Δ} (f : Γ ~> Δ) (τ : Typ Γ) -> (Γ , τ) ~> (Δ , τ [ f ]T)
  ↑-β : ∀ {Γ Δ} (f : Γ ~> Δ) (τ : Typ Γ) -> (Γ , τ) ~> (Δ , τ [ f ]T)
        -> f ↑ τ ≡ (tail* id* ∘* f) ,* coeTm ([][]T (tail* id*) f τ) (head* id*)

  -- The definition of substitution on terms _[_]
  _[_]C : ∀ {Γ Δ τ} (x : τ ⊣ Γ) (f : Γ ~> Δ) -> (τ [ f ]T) ⊣ Δ

  -- Substitution on terms is a functor
  [id] : ∀ {Γ τ} (x : τ ⊣ Γ) -> x [ id* ] ≡[ (λ i → ([id]T τ i) ⊣ Γ) ]≡ x
  [][] : ∀ {Γ Δ Σ τ} (g : Δ ~> Σ) (f : Γ ~> Δ) (x : τ ⊣ Γ)
         -> x [ f ] [ g ] ≡[ (λ i → ([][]T g f τ i) ⊣ Σ) ]≡ x [ g ∘* f ]

  -- Pi types and their computation rule for substition
  Π : ∀ {Γ} (τ : Typ Γ) (σ : Typ (Γ , τ)) -> U ⊣ Γ
  Π[] : ∀ {Γ Δ} (τ : Typ Γ) (σ : Typ (Γ , τ)) (f : Γ ~> Δ)
        -> (Π τ σ) [ f ] ≡ Π (τ [ f ]T) (σ [ f ↑ τ ]T)

  -- lambdas and their computation rule for substitition
  lam : ∀ {Γ τ σ} (y : σ ⊣ (Γ , τ)) -> type (Π τ σ) ⊣ Γ
  lam[] : ∀ {Γ Δ τ σ} (y : σ ⊣ (Γ , τ)) (f : Γ ~> Δ)
          -> lam y [ f ] ≡[ (λ i → type (Π[] τ σ f i) ⊣ Δ) ]≡ lam (y [ f ↑ τ ])

  -- Pi type elim, whose computation rule for substition is derivable using Π-η
  -- (Note: application is defined in terms of this below)
  unlam : ∀ {Γ τ σ} (ℓ : type (Π τ σ) ⊣ Γ) -> σ ⊣ (Γ , τ)

  -- Computation and uniqueness for Pi types
  Π-β : ∀ {Γ τ σ} (y : σ ⊣ (Γ , τ))      -> unlam (lam y) ≡ y
  Π-η : ∀ {Γ τ σ} (ℓ : type (Π τ σ) ⊣ Γ) -> lam (unlam ℓ) ≡ ℓ

-- The missing substitution computation rule for unlam, derivable because we have definitional η!
unlam[] : ∀ {Γ Δ τ σ} (ℓ : type (Π τ σ) ⊣ Γ) (f : Γ ~> Δ)
          -> unlam ℓ [ f ↑ τ ] ≡ unlam (coeTmTy (Π[] τ σ f) (ℓ [ f ]))
unlam[] {Γ} {Δ} {τ} {σ} ℓ f =
              (unlam ℓ) [ f ↑ τ ]                     ≡[ i ]⟨ Π-β ((unlam ℓ) [ f ↑ τ ]) (~ i) ⟩
  unlam (lam ((unlam ℓ) [ f ↑ τ ]))                   ≡[ i ]⟨ unlam (fromPathP (lam[] (unlam ℓ) f) (~ i)) ⟩
  unlam (coeTmTy (Π[] τ σ f) ((lam (unlam ℓ)) [ f ])) ≡[ i ]⟨ unlam (coeTmTy (Π[] τ σ f) ((Π-η ℓ i) [ f ])) ⟩
  unlam (coeTmTy (Π[] τ σ f) (ℓ [ f ]))               ∎

-- Missing definitions from above
[id]T U = refl
[id]T (type τ) = cong type ([id] τ)
[][]T g f U = refl
[][]T g f (type τ) = cong type ([][] g f τ)
id* = id*C
_∘*_ = _∘*C_
_[_] = _[_]C

--------------------
-- Derived Notions
--------------------

-- Weakening on contexts
wkn : ∀ {Γ τ} -> Γ ~> (Γ , τ)
wkn = tail* id*

-- A single substition at the top of a context
<_> : ∀ {Γ τ} (x : τ ⊣ Γ) -> (Γ , τ) ~> Γ
< x > = id* ,* coeTm (sym ([id]T _)) x

-- Using substition, we can now write the usual definition of application
_$_ : ∀ {Γ τ σ} (ℓ : (type (Π τ σ)) ⊣ Γ) (x : τ ⊣ Γ) -> (σ [ < x > ]T) ⊣ Γ
ℓ $ x = unlam ℓ [ < x > ]
infixl 4 _$_

-- Variables (as de Bruijn indices) are also derived!

var₀ : ∀ {Γ τ} -> (τ [ wkn ]T) ⊣ (Γ , τ)
var₀ = head* id*

var₊ : ∀ {Γ τ σ} -> τ ⊣ Γ -> (τ [ wkn ]T) ⊣ (Γ , σ)
var₊ x = x [ wkn ]

var₁ : ∀ {Γ τ σ} -> (τ [ wkn ]T [ wkn ]T) ⊣ ((Γ , τ) , σ)
var₁ = var₊ var₀

var₂ : ∀ {Γ τ σ ρ} -> (τ [ wkn ]T [ wkn ]T [ wkn ]T) ⊣ (((Γ , τ) , σ) , ρ)
var₂ = var₊ var₁

-- The other classical operations on contexts:

ctr : ∀ {Γ τ} -> (Γ , τ , τ [ wkn ]T) ~> (Γ , τ)
ctr {Γ} {τ} = id* ,* coeTm (sym p) var₀
  where p : τ [ wkn ]T [ id* ]T ≡ τ [ tail* id* ]T
        p =
          τ [ wkn ]T [ id* ]T ≡⟨ [][]T id* wkn _ ⟩
          τ [ id* ∘* wkn ]T   ≡⟨ cong (τ [_]T) (id*-l wkn) ⟩
          τ [ tail* id* ]T ∎

-- exg : ∀ {Γ τ σ} -> (Γ , τ , σ [ wkn ]T) ~> (Γ , σ , τ [ wkn ]T)
-- exg {Γ} {τ} {σ} = wkn ∘* wkn ,*
--                   coeTm ([][]T wkn wkn τ) var₀ ,*
--                   coeTm (sym p) (coeTm ([][]T wkn wkn σ) var₁)
--   where p : σ [ wkn ]T [ (wkn ∘* wkn) ,* coeTm ([][]T wkn wkn τ) var₀ ]T ≡ σ [ wkn ∘* wkn ]T
--         p = begin
--           σ [ wkn ]T [ (wkn ∘* wkn) ,* coeTm ([][]T wkn wkn τ) var₀ ]T ≡⟨ [][]T _ _ σ ⟩
--           σ [ ((wkn ∘* wkn) ,* coeTm ([][]T wkn wkn τ) var₀) ∘* wkn ]T ≡⟨ cong (σ [_]T) {!!} ⟩
--           σ [ wkn ∘* wkn ]T ∎
--         -- p' : (wkn ∘* wkn) ,* coeTm ([][]T wkn wkn τ) var₁ ≡ wkn
--         -- p' = begin
--         --   (wkn ∘* wkn) ,* coeTm ([][]T wkn wkn τ) var₁ ≡⟨ sym (,*-∘* wkn wkn var₀) ⟩
--         --   wkn ∘* (wkn ,* var₀) ≡⟨ cong (wkn ∘*_) (,*-η id*) ⟩
--         --   wkn ∘* id*           ≡⟨ id*-r wkn ⟩
--         --   wkn ∎

--------------------------------------
-- Experimental: Encoding more types
--------------------------------------

_⇒_ : ∀ {Γ} (τ : U ⊣ Γ) (σ : U ⊣ (Γ , type τ)) -> U ⊣ Γ
x ⇒ y = Π (type x) (type y)
infixr 4 _⇒_

-- The natural number type

N : ∀ {Γ} -> U ⊣ Γ
N = Π U (type (var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂))

-- N[] : ∀ {Γ Δ} (f : Γ ~> Δ) -> type N [ f ]T ≡ type N
-- N[] f = cong type p
--   where p : Π U (type (var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂)) [ f ] ≡  Π U (type (var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂))
--         p = begin
--           Π U (type (var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂)) [ f ] ≡⟨ Π[] _ _ f ⟩
--           Π U (type ((var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂) [ f ↑ U ])) ≡⟨ {!!} ⟩
--           Π U (type (var₀ ⇒ (var₁ ⇒ var₂) ⇒ var₂)) ∎

z : ∀ {Γ} -> type N ⊣ Γ
z = lam (lam (lam var₁))

-- s : ∀ {Γ} (n : type N ⊣ Γ) -> type N ⊣ Γ
-- s {Γ} n = lam (lam (lam {!!})) -- var₀ $ (n' $ var₀ $ var₁ $ var₂)
--   where n' : type N ⊣ (((Γ , U) , type var₀) , type (var₁ ⇒ var₂))
--         n' = coe (cong (Term _) {!!}) (var₊ (var₊ (var₊ n)))

-- The dependent pair type

-- Σ : ∀ {Γ} (τ : Typ Γ) (σ : Typ (Γ , τ)) -> U ⊣ Γ
-- Σ τ σ = Π U (type ((Π (τ [ tail* id* ]T) (type (Π (σ [ tail* id* ↑ τ ]T) (type var₂)))) ⇒ var₀))

-- pair : ∀ {Γ τ σ} (x : τ ⊣ Γ) (y : σ ⊣ (Γ , τ)) -> (type (Σ τ σ)) ⊣ Γ
-- pair x y = lam (lam {!!})

  -- Σ : ∀ {Γ} (τ : Typ Γ) (σ : Typ (Γ , τ)) -> U ⊣ Γ
  -- Σ[] : ∀ {Γ Δ} (τ : Typ Γ) (σ : Typ (Γ , τ)) (f : Γ ~> Δ)
  --       -> (Σ τ σ) [ f ] ≡ Σ (τ [ f ]T) (σ [ f ↑ τ ]T)

  -- pair : ∀ {Γ τ σ} (x : τ ⊣ Γ) (y : σ ⊣ (Γ , τ)) -> (type (Σ τ σ)) ⊣ Γ
  -- pair[] : ∀ {Γ Δ τ σ} (x : τ ⊣ Γ) (y : σ ⊣ (Γ , τ)) (f : Γ ~> Δ)
  --          -> (pair x y) [ f ] ≡[ (λ i → type (Σ[] τ σ f i) ⊣ Δ) ]≡ pair (x [ f ]) (y [ f ↑ τ ])

  -- Σ-ind : ∀ {Γ τ σ} (ρ : Typ (Γ , type (Σ τ σ)))
  --                   (xy : (ρ [ {!!} ∘* ({!!} ↑ type (Σ τ σ)) ]T) ⊣ ((Γ , τ) , σ))
  --                   -> ρ ⊣ (Γ , type (Σ τ σ))

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Metalogic.Linear.Syntax {ℓₚ} (Proposition : Set(ℓₚ)) where

import Lvl

-- https://en.wikipedia.org/wiki/Linear_logic
-- https://plato.stanford.edu/entries/logic-linear/#ProSys

data Formula : Set(ℓₚ) where
  •_ : Proposition → Formula

  -- Top
  ⊤ : Formula

  -- Bottom
  ⊥ : Formula

  -- Classical conjunction
  _∧_ : Formula → Formula → Formula

  -- Classical disjunction
  _∨_ : Formula → Formula → Formula

  -- Additive and
  _&_ : Formula → Formula → Formula

  -- Additive or
  _⊕_ : Formula → Formula → Formula

  -- Multiplicative and
  _⊗_ : Formula → Formula → Formula

  -- Multiplicative or
  _⅋_ : Formula → Formula → Formula

  -- Linear implication
  _⊸_ : Formula → Formula → Formula

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 --erased-cubical --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.Cubical.Id where

  open import Agda.Primitive.Cubical
  open import Agda.Builtin.Cubical.Path
  open import Agda.Builtin.Cubical.Sub renaming (primSubOut to ouc; Sub to _[_↦_])

  {-# BUILTIN ID           Id       #-}
  {-# BUILTIN REFLID       reflId   #-}

  private
    module ConId where
      primitive
        primConId : ∀ {ℓ} {A : Set ℓ} {x y : A} → I → x ≡ y → Id x y

  open ConId public renaming (primConId to conid)

  -- Id x y is treated as a pair of I and x ≡ y, using "i" for the
  -- first component and "p" for the second.
  {-# COMPILE JS conid =
      _ => _ => _ => _ => i => p => { return { "i" : i, "p" : p } }
    #-}

  primitive
    primDepIMin : _
    primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I
    primIdPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → x ≡ y

  primitive
    primIdJ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ') →
                P x (conid i1 (λ i → x)) → ∀ {y} (p : Id x y) → P y p

  primitive
    primIdElim : ∀ {a c} {A : Set a} {x : A}
                   (C : (y : A) → Id x y → Set c) →
                   ((φ : I) (y : A [ φ ↦ (λ _ → x) ])
                    (w : (x ≡ ouc y) [ φ ↦ (λ { (φ = i1) → \ _ → x}) ]) →
                    C (ouc y) (conid φ (ouc w))) →
                   {y : A} (p : Id x y) → C y p