text:
------------------------------------------------------------------------------
-- Properties of the alter list
------------------------------------------------------------------------------

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

module FOT.FOTC.UnguardedCorecursion.Alter.PropertiesATP where

open import FOT.FOTC.UnguardedCorecursion.Alter.Alter

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- TODO (23 December 2013).
-- alter-Stream : Stream alter
-- alter-Stream = Stream-coind A h refl
--   where
--   A : D → Set
--   A xs = xs ≡ xs
--   {-# ATP definition A #-}

--   postulate h : A alter → ∃[ x' ] ∃[ xs' ] alter ≡ x' ∷ xs' ∧ A xs'
--   {-# ATP prove h #-}

-- TODO (23 December 2013).
-- alter'-Stream : Stream alter'
-- alter'-Stream = Stream-coind A h refl
--   where
--   A : D → Set
--   A xs = xs ≡ xs
--   {-# ATP definition A #-}

--   postulate h : A alter' → ∃[ x' ] ∃[ xs' ] alter' ≡ x' ∷ xs' ∧ A xs'
--   {-# ATP prove h #-}

-- TODO (23 December 2013).
-- alter≈alter' : alter ≈ alter'
-- alter≈alter' = ≈-coind B h₁ h₂
--   where
--   B : D → D → Set
--   B xs ys = xs ≡ xs
--   {-# ATP definition B #-}

--   postulate h₁ : B alter alter' → ∃[ x' ] ∃[ xs' ] ∃[ ys' ]
--                    alter ≡ x' ∷ xs' ∧ alter' ≡ x' ∷ ys' ∧ B xs' ys'
--   {-# ATP prove h₁ #-}

--   postulate h₂ : B alter alter'
--   {-# ATP prove h₂ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --without-K #-}
module sets.nat.ordering.properties where

open import function.isomorphism
open import sets.nat.core
open import sets.nat.ordering.lt
open import sets.nat.ordering.leq
open import hott.level.core

<-≤-iso : ∀ {n m} → (n < m) ≅ (suc n ≤ m)
<-≤-iso = record
  { to = f
  ; from = g
  ; iso₁ = λ _ → h1⇒prop <-level _ _
  ; iso₂ = λ _ → h1⇒prop ≤-level _ _ }
  where
    f : ∀ {n m} → n < m → suc n ≤ m
    f suc< = refl-≤
    f (n<s p) = s≤s (trans-≤ suc≤ (f p))

    g : ∀ {n m} → suc n ≤ m → n < m
    g {zero} (s≤s p) = z<n
    g {suc n} (s≤s p) = ap<-suc (g p)

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
open import Prelude hiding (lift; Fin′; subst; id)

module Implicits.Substitutions.LNMetaType where

open import Implicits.Syntax.LNMetaType
open import Data.Fin.Substitution
open import Data.Star as Star hiding (map)
open import Data.Star.Properties

module MetaTypeApp {T} (l : Lift T MetaType) where
  open Lift l hiding (var)

  infixl 8 _/_

  mutual
    _simple/_ : ∀ {m n} → MetaSType m → Sub T m n → MetaType n
    tc c simple/ σ = simpl (tc c)
    tvar x simple/ σ = simpl (tvar x)
    mvar x simple/ σ = lift $ lookup x σ
    (a →' b) simple/ σ = simpl ((a / σ) →' (b / σ))

    _/_ : ∀ {m n} → MetaType m → Sub T m n → MetaType n
    (simpl c) / σ = (c simple/ σ)
    (a ⇒ b)  / σ = (a / σ) ⇒ (b / σ)
    (∀' a)   / σ = ∀' (a / σ)

  open Application (record { _/_ = _/_ }) using (_/✶_)

  →'-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
             (simpl (a →' b)) /✶ ρs ↑✶ k ≡ simpl ((a /✶ ρs ↑✶ k) →' (b /✶ ρs ↑✶ k))
  →'-/✶-↑✶ k ε        = refl
  →'-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (→'-/✶-↑✶ k ρs) refl

  ⇒-/✶-↑✶ : ∀ k {m n a b} (ρs : Subs T m n) →
             (a ⇒ b) /✶ ρs ↑✶ k ≡ (a /✶ ρs ↑✶ k) ⇒ (b /✶ ρs ↑✶ k)
  ⇒-/✶-↑✶ k ε        = refl
  ⇒-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

  tc-/✶-↑✶ : ∀ k {c m n} (ρs : Subs T m n) →
             (simpl (tc c)) /✶ ρs ↑✶ k ≡ simpl (tc c)
  tc-/✶-↑✶ k ε        = refl
  tc-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tc-/✶-↑✶ k ρs) refl

  tvar-/✶-↑✶ : ∀ k {c m n} (ρs : Subs T m n) →
             (simpl (tvar c)) /✶ ρs ↑✶ k ≡ simpl (tvar c)
  tvar-/✶-↑✶ k ε        = refl
  tvar-/✶-↑✶ k (r ◅ ρs) = cong₂ _/_ (tvar-/✶-↑✶ k ρs) refl

  ∀'-/✶-↑✶ : ∀ k {m n a} (ρs : Subs T m n) →
             (∀' a) /✶ ρs ↑✶ k ≡ ∀' (a /✶ ρs ↑✶ k)
  ∀'-/✶-↑✶ k ε = refl
  ∀'-/✶-↑✶ k (x ◅ ρs) = cong₂ _/_ (∀'-/✶-↑✶ k ρs) refl

typeSubst : TermSubst MetaType
typeSubst = record { var = (λ n → simpl (mvar n)); app = MetaTypeApp._/_ }

open TermSubst typeSubst public hiding (var)
open MetaTypeApp termLift public using (_simple/_)
open MetaTypeApp varLift public using () renaming (_simple/_ to _simple/Var_)

infix 8 _[/_]

-- Shorthand for single-variable type substitutions
_[/_] : ∀ {n} → MetaType (suc n) → MetaType n → MetaType n
a [/ b ] = a / sub b

_◁m₁ : ∀ {m} (r : MetaType m) → ℕ
_◁m₁ (a ⇒ b) = b ◁m₁
_◁m₁ (∀' r) = 1 N+ r ◁m₁
_◁m₁ (simpl x) = zero

-- heads of metatypes
_◁m : ∀ {m} (r : MetaType m) → (MetaType ((r ◁m₁) N+ m))
(a ⇒ b) ◁m = b ◁m
∀' r ◁m = open-meta zero (r ◁m)
simpl x ◁m = simpl x


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.MultivariatePoly-notationZ where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat
open import Cubical.Data.FinData

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.CommRing.Instances.Int

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient

-- Notations for ℤ polynomial rings

ℤ[X] : CommRing ℓ-zero
ℤ[X] = PolyCommRing ℤCommRing 1

ℤ[x] : Type ℓ-zero
ℤ[x] = fst ℤ[X]

ℤ[X,Y] : CommRing ℓ-zero
ℤ[X,Y] = PolyCommRing ℤCommRing 2

ℤ[x,y] : Type ℓ-zero
ℤ[x,y] = fst ℤ[X,Y]

ℤ[X,Y,Z] : CommRing ℓ-zero
ℤ[X,Y,Z] = PolyCommRing ℤCommRing 3

ℤ[x,y,z] : Type ℓ-zero
ℤ[x,y,z] = fst ℤ[X,Y,Z]

ℤ[X1,···,Xn] : (n : ℕ) → CommRing ℓ-zero
ℤ[X1,···,Xn] n = A[X1,···,Xn] ℤCommRing n

ℤ[x1,···,xn] : (n : ℕ) → Type ℓ-zero
ℤ[x1,···,xn] n = fst (ℤ[X1,···,Xn] n)

-- Notation for quotiented ℤ polynomial ring

<X> : FinVec ℤ[x] 1
<X> = <Xkʲ> ℤCommRing 1 0 1

<X²> : FinVec ℤ[x] 1
<X²> = <Xkʲ> ℤCommRing 1 0 2

<X³> : FinVec ℤ[x] 1
<X³> = <Xkʲ> ℤCommRing 1 0 3

<Xᵏ> : (k  : ℕ) → FinVec ℤ[x] 1
<Xᵏ> k = <Xkʲ> ℤCommRing 1 0 k

ℤ[X]/X : CommRing ℓ-zero
ℤ[X]/X = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 1

ℤ[x]/x : Type ℓ-zero
ℤ[x]/x = fst ℤ[X]/X

ℤ[X]/X² : CommRing ℓ-zero
ℤ[X]/X² = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 2

ℤ[x]/x² : Type ℓ-zero
ℤ[x]/x² = fst ℤ[X]/X²

ℤ[X]/X³ : CommRing ℓ-zero
ℤ[X]/X³ = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 3

ℤ[x]/x³ : Type ℓ-zero
ℤ[x]/x³ = fst ℤ[X]/X³

ℤ[X1,···,Xn]/<X1,···,Xn> : (n : ℕ) → CommRing ℓ-zero
ℤ[X1,···,Xn]/<X1,···,Xn> n = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing n

ℤ[x1,···,xn]/<x1,···,xn> : (n : ℕ) → Type ℓ-zero
ℤ[x1,···,xn]/<x1,···,xn> n = fst (ℤ[X1,···,Xn]/<X1,···,Xn> n)

-- Warning there is two possible definitions of ℤ[X]
-- they only holds up to a path

ℤ'[X]/X : CommRing ℓ-zero
ℤ'[X]/X = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing 1

equivℤ[X] : ℤ'[X]/X ≡ ℤ[X]/X
equivℤ[X] = cong (λ X → (A[X1,···,Xn] ℤCommRing 1) / (genIdeal ((A[X1,···,Xn] ℤCommRing 1)) X))
                   (funExt (λ {zero → refl }))

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
-- Andreas, 2015-03-12
-- Sizes should be irrelevant in terms, while they are relevant in types!

{-# OPTIONS --experimental-irrelevance #-}

open import Common.Size
open import Common.Equality

module IrrelevantSizes where

  -- Nat i is shape-irrelevant in i.

  data Nat ..(i : Size) : Set where
    zero : .(j : Size< i) → Nat i
    suc  : .(j : Size< i) → Nat j → Nat i

  add : .(i : Size) → Nat i → Nat ∞ → Nat ∞
  add i (zero j) y = y
  add i (suc j x) y = suc ∞ (add j x y)

  -- Proving this lemma is much easier with irrelevant sizes
  -- in constructors zero and suc

  plus0 : .(i : Size) (x : Nat i) → add ∞ x (zero ∞) ≡ x
  plus0 i (zero j) = refl                       -- Goal: zero ∞ = zero j
  plus0 i (suc j x) = cong (suc ∞) (plus0 j x)  -- Goal: suc ∞ (add j x (zero ∞)) ≡ suc j x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Cardinality.Finite.ManifestBishop.Isomorphism where

open import Prelude
open import Data.Fin
open import Data.Fin.Properties

open import Container.List.Isomorphism

import Cardinality.Finite.ManifestBishop.Inductive as 𝕃
import Cardinality.Finite.ManifestBishop.Container as ℒ

open import Cardinality.Finite.SplitEnumerable.Isomorphism

open import Data.Nat.Properties

∈!ℒ⇒∈!𝕃 : ∀ (x : A) l (xs : Fin l → A) → x ℒ.∈! (l , xs) → x 𝕃.∈! ℒ→𝕃 (l , xs)
∈!ℒ⇒∈!𝕃 x (suc l) xs ((f0   , p) , u) = (f0 , p) , lemma
  where
  lemma : (y : x 𝕃.∈ ℒ→𝕃 (suc l , xs)) → (f0 , p) ≡ y
  lemma (f0   , q) = cong (∈ℒ⇒∈𝕃 x (suc l , xs)) (u (f0 , q))
  lemma (fs m , q) =
    let o , r = subst (x ℒ.∈_) (ℒ→𝕃→ℒ l (xs ∘ fs)) (m , q)
    in ⊥-elim (znots (cong (FinToℕ ∘ fst) (u (fs o , r))))
∈!ℒ⇒∈!𝕃 x (suc l) xs ((fs n , p) , u) = 𝕃.push! xs0≢x (∈!ℒ⇒∈!𝕃 x l (xs ∘ fs) ((n , p) , uxss))
  where
  xs0≢x : xs f0 ≢ x
  xs0≢x xs0≡x = snotz (cong (FinToℕ ∘ fst) (u (f0 , xs0≡x)))

  uxss : (y : x ℒ.∈ (l , xs ∘ fs)) → (n , p) ≡ y
  uxss (m , q) = cong (λ { (f0 , q) → ⊥-elim (xs0≢x q) ; (fs m , q) → m , q}) (u (fs m , q))

𝕃⇔ℒ⟨ℬ⟩ : 𝕃.ℬ A ⇔ ℒ.ℬ A
𝕃⇔ℒ⟨ℬ⟩ .fun (sup , cov) = 𝕃→ℒ sup , cov
𝕃⇔ℒ⟨ℬ⟩ .inv ((l , xs) , cov) = ℒ→𝕃 (l , xs) , λ x → ∈!ℒ⇒∈!𝕃 x l xs (cov x)
𝕃⇔ℒ⟨ℬ⟩ .rightInv (sup , cov) i .fst = 𝕃⇔ℒ .rightInv sup i
𝕃⇔ℒ⟨ℬ⟩ .rightInv ((l , xs) , cov) i .snd x =
  J
    (λ ys ys≡ → (zs : x ℒ.∈! ys) → PathP (λ i → x ℒ.∈! sym ys≡ i) zs (cov x))
    (λ _ → isPropIsContr _ _)
    (sym (ℒ→𝕃→ℒ l xs))
    (∈!ℒ⇒∈!𝕃 x l xs (cov x))
    i
𝕃⇔ℒ⟨ℬ⟩ .leftInv  (sup , cov) i .fst = 𝕃⇔ℒ .leftInv sup i
𝕃⇔ℒ⟨ℬ⟩ .leftInv  (sup , cov) i .snd x =
  J
    (λ ys ys≡ → (zs : x 𝕃.∈! ys) → PathP (λ i → x 𝕃.∈! sym ys≡ i) zs (cov x))
    (λ zs → isPropIsContr _ _)
    (sym (𝕃→ℒ→𝕃 sup))
    (∈!ℒ⇒∈!𝕃 x (𝕃.length sup) (sup 𝕃.!_) (cov x))
    i

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2013-02-26
module Issue799a where

data D (A : Set1) : Set where
  d : D A

x : D Set
x = d {A = _} -- correct parameter name

y : D Set
y = d {B = _} -- wrong parameter name, should give error

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Acc where

data Acc ( A : Set ) ( Lt : A -> A -> Set) : A -> Set where
  acc :    (   b : A )
        -> ( ( a : A ) -> Lt a b  ->  Acc A Lt a )
        -> ( Acc A Lt b )

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

data Lt : Nat -> Nat -> Set where
  ltzero : ( x : Nat ) -> Lt zero (succ x)
  ltsucc : ( x : Nat ) -> (y : Nat) -> Lt x y -> Lt (succ x) (succ y)

ltcase : ( x : Nat ) -> ( y : Nat ) -> Lt x (succ y) ->
         ( P : Nat -> Set ) -> ( (x' : Nat ) -> Lt x' y -> P x') -> P y -> P x
ltcase zero zero      _ P hx' hy = hy
ltcase zero (succ y') _ P hx' hy = hx' zero (ltzero y')
ltcase (succ x') zero (ltsucc .x' .zero ()) _ _ _
ltcase (succ x') (succ y') (ltsucc ._ ._ p) P hx' hy =
  ltcase x' y' p (\ n -> P (succ n))
    (\ x'' p' -> hx' (succ x'') (ltsucc _ _ p')) hy

accSucc : (x : Nat) -> Acc Nat Lt x -> Acc Nat Lt (succ x)
accSucc x a@(acc .x h) = acc (succ x) (\ y p -> ltcase y x p (Acc Nat Lt) h a)

max_stars_repo_name: andreasabel/miniagda

max_issues_repo_name: andreasabel/miniagda

max_forks_repo_name: andreasabel/miniagda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Symmetry {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
import Definition.Typed.Weakening as Wk
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Conversion

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Helper function for symmetry of type equality using shape views.
  symEqT : ∀ {Γ A B l l′} {[A] : Γ ⊩⟨ l ⟩ A} {[B] : Γ ⊩⟨ l′ ⟩ B}
         → ShapeView Γ l l′ A B [A] [B]
         → Γ ⊩⟨ l  ⟩ A ≡ B / [A]
         → Γ ⊩⟨ l′ ⟩ B ≡ A / [B]
  symEqT (ℕᵥ D D′) A≡B = red D
  symEqT (Emptyᵥ D D′) A≡B = red D
  symEqT (Unitᵥ D D′) A≡B = red D
  symEqT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
         rewrite whrDet* (red D′ , ne neM) (red D₁ , ne neK₁) =
    ne₌ _ D neK
        (~-sym K≡M)
  symEqT {Γ = Γ} (Bᵥ W (Bᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                       (Bᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
         (B₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , ⟦ W ⟧ₙ) (D′ , ⟦ W ⟧ₙ)
        F₁≡F′ , G₁≡G′ = B-PE-injectivity W ΠF₁G₁≡ΠF′G′
        [F₁≡F] : ∀ {Δ} {ρ} [ρ] ⊢Δ → _
        [F₁≡F] {Δ} {ρ} [ρ] ⊢Δ =
          let ρF′≡ρF₁ ρ = PE.cong (wk ρ) (PE.sym F₁≡F′)
              [ρF′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → Δ ⊩⟨ _ ⟩ wk ρ x) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
          in  irrelevanceEq′ {Δ} (ρF′≡ρF₁ ρ)
                             ([ρF′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ)
                             (symEq ([F] [ρ] ⊢Δ) ([ρF′] [ρ] ⊢Δ)
                                    ([F≡F′] [ρ] ⊢Δ))
    in  B₌ _ _ (red D) (≅-sym (PE.subst (λ x → Γ ⊢ ⟦ W ⟧ F ▹ G ≅ x) (PE.sym ΠF₁G₁≡ΠF′G′) A≡B))
          [F₁≡F]
          (λ {ρ} [ρ] ⊢Δ [a] →
               let ρG′a≡ρG₁′a = PE.cong (λ x → wk (lift ρ) x [ _ ]) (PE.sym G₁≡G′)
                   [ρG′a] = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk (lift ρ) x [ _ ]) G₁≡G′
                                     ([G]₁ [ρ] ⊢Δ [a])
                   [a]₁ = convTerm₁ ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) ([F₁≡F] [ρ] ⊢Δ) [a]
               in  irrelevanceEq′ ρG′a≡ρG₁′a
                                  [ρG′a]
                                  ([G]₁ [ρ] ⊢Δ [a])
                                  (symEq ([G] [ρ] ⊢Δ [a]₁) [ρG′a]
                                         ([G≡G′] [ρ] ⊢Δ [a]₁)))
  symEqT (Uᵥ (Uᵣ _ _ _) (Uᵣ _ _ _)) A≡B = PE.refl
  symEqT (emb⁰¹ x) A≡B = symEqT x A≡B
  symEqT (emb¹⁰ x) A≡B = symEqT x A≡B

  -- Symmetry of type equality.
  symEq : ∀ {Γ A B l l′} ([A] : Γ ⊩⟨ l ⟩ A) ([B] : Γ ⊩⟨ l′ ⟩ B)
        → Γ ⊩⟨ l ⟩ A ≡ B / [A]
        → Γ ⊩⟨ l′ ⟩ B ≡ A / [B]
  symEq [A] [B] A≡B = symEqT (goodCases [A] [B] A≡B) A≡B

symNeutralTerm : ∀ {t u A Γ}
               → Γ ⊩neNf t ≡ u ∷ A
               → Γ ⊩neNf u ≡ t ∷ A
symNeutralTerm (neNfₜ₌ neK neM k≡m) = neNfₜ₌ neM neK (~-sym k≡m)

symNatural-prop : ∀ {Γ k k′}
                → [Natural]-prop Γ k k′
                → [Natural]-prop Γ k′ k
symNatural-prop (sucᵣ (ℕₜ₌ k k′ d d′ t≡u prop)) =
  sucᵣ (ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop))
symNatural-prop zeroᵣ = zeroᵣ
symNatural-prop (ne prop) = ne (symNeutralTerm prop)

symEmpty-prop : ∀ {Γ k k′}
              → [Empty]-prop Γ k k′
              → [Empty]-prop Γ k′ k
symEmpty-prop (ne prop) = ne (symNeutralTerm prop)

-- Symmetry of term equality.
symEqTerm : ∀ {l Γ A t u} ([A] : Γ ⊩⟨ l ⟩ A)
          → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
          → Γ ⊩⟨ l ⟩ u ≡ t ∷ A / [A]
symEqTerm (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [A] [B] [A≡B]) =
  Uₜ₌ B A d′ d typeB typeA (≅ₜ-sym A≡B) [B] [A] (symEq [A] [B] [A≡B])
symEqTerm (ℕᵣ D) (ℕₜ₌ k k′ d d′ t≡u prop) =
  ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop)
symEqTerm (Emptyᵣ D) (Emptyₜ₌ k k′ d d′ t≡u prop) =
  Emptyₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symEmpty-prop prop)
symEqTerm (Unitᵣ D) (Unitₜ₌ ⊢t ⊢u) =
  Unitₜ₌ ⊢u ⊢t
symEqTerm (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ m k d′ d (symNeutralTerm nf)
symEqTerm (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  Πₜ₌ g f d′ d funcG funcF (≅ₜ-sym f≡g) [g] [f]
      (λ ρ ⊢Δ [a] → symEqTerm ([G] ρ ⊢Δ [a]) ([f≡g] ρ ⊢Δ [a]))
symEqTerm (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Σₜ₌ p r d d′ pProd rProd p≅r [t] [u] [fstp] [fstr] [fst≡] [snd≡]) =
  let ⊢Γ = wf ⊢F
      [Gfstp≡Gfstr] = G-ext Wk.id ⊢Γ [fstp] [fstr] [fst≡]
  in  Σₜ₌ r p d′ d rProd pProd (≅ₜ-sym p≅r) [u] [t] [fstr] [fstp]
          (symEqTerm ([F] Wk.id ⊢Γ) [fst≡])
          (convEqTerm₁
            ([G] Wk.id ⊢Γ [fstp]) ([G] Wk.id ⊢Γ [fstr])
            [Gfstp≡Gfstr]
            (symEqTerm ([G] Wk.id ⊢Γ [fstp]) [snd≡]))
symEqTerm (emb 0<1 x) t≡u = symEqTerm x t≡u


text:
module Lib where

open import Data.Nat public hiding (_<_)
open import Function public using (_∘_)
open import Data.List public
open import Data.Product public using (_×_ ; _,_ ; proj₁ ; proj₂ ; Σ ; ∃)
open import Data.Sum public using (_⊎_ ; [_,_]′ ; inj₁ ; inj₂)
open import Relation.Nullary public
open import Relation.Binary.PropositionalEquality public hiding ([_])

open import Category.Functor public

-- Pointer into a list. It is similar to list membership as defined in
-- Data.List.AnyMembership, rather than going through propositional
-- equality, it asserts the existence of the referenced element
-- directly.
infix 4 _∈_
data _∈_ {A : Set} : A → List A → Set where
  hd : ∀ {x xs} → x ∈ (x ∷ xs)
  tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)

mapIdx : {A B : Set} → (f : A → B) →
         {x : A} {xs : List A} → x ∈ xs → f x ∈ map f xs
mapIdx f hd = hd
mapIdx f (tl x₁) = tl (mapIdx f x₁)

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
module Debug where
open import Data.String using (String) public
open import Level public

{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified Debug.Trace as Trace #-}

{-# FOREIGN GHC
debug' :: Data.Text.Text -> c -> c
debug' txt c = Trace.trace (Data.Text.unpack txt) c
#-}

postulate debug : {a : Level} {A : Set a} → String → A → A
{-# COMPILE GHC debug = (\x -> (\y -> debug')) #-}

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


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

syntax Lens | L

type
  S : 0-ary
  A : 0-ary

term
  get : S  ->  A
  put : S  A  ->  S

theory
  (PG) s : S  a : A   |> get (put (s, a))   = a
  (GP) s : S          |> put (s, get(s))    = s
  (PP) s : S  a b : A |> put (put(s, a), b) = put (s, a)
-}

module Lens.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import Lens.Signature

private
  variable
    Γ Δ Π : Ctx
    α : LT
    𝔛 : Familyₛ

-- Inductive term declaration
module L:Terms (𝔛 : Familyₛ) where

  data L : Familyₛ where
    var  : ℐ ⇾̣ L
    mvar : 𝔛 α Π → Sub L Π Γ → L α Γ

    get : L S Γ → L A Γ
    put : L S Γ → L A Γ → L S Γ

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  Lᵃ : MetaAlg L
  Lᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (getₒ ⋮ a)     → get a
      (putₒ ⋮ a , b) → put a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module Lᵃ = MetaAlg Lᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : L ⇾̣ 𝒜
    𝕊 : Sub L Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞 (get a)   = 𝑎𝑙𝑔 (getₒ ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (put a b) = 𝑎𝑙𝑔 (putₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ Lᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ L α Γ) → 𝕤𝕖𝕞 (Lᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (getₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (putₒ ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ L ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : L ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ Lᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : L α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub L Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! (get a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (put a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
L:Syn : Syntax
L:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = L:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open L:Terms 𝔛 in record
    { ⊥ = L ⋉ Lᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax L:Syn public
open L:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands Lᵃ public
open import SOAS.Metatheory L:Syn public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
open import Oscar.Prelude
open import Oscar.Class.IsCategory
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.Reflexivity
open import Oscar.Class.Smap
open import Oscar.Class.Surjection
open import Oscar.Class.Surjidentity
open import Oscar.Class.Transitivity

module Oscar.Class.IsFunctor where

module _
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔯₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø 𝔯₁)
  {ℓ₁} (_∼̇₁_ : ∀ {x y} → x ∼₁ y → x ∼₁ y → Ø ℓ₁)
  (ε₁ : Reflexivity.type _∼₁_)
  (_↦₁_ : Transitivity.type _∼₁_)
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔯₂} (_∼₂_ : 𝔒₂ → 𝔒₂ → Ø 𝔯₂)
  {ℓ₂} (_∼̇₂_ : ∀ {x y} → x ∼₂ y → x ∼₂ y → Ø ℓ₂)
  (ε₂ : Reflexivity.type _∼₂_)
  (_↦₂_ : Transitivity.type _∼₂_)
  {surjection : Surjection.type 𝔒₁ 𝔒₂}
  (smap : Smap.type _∼₁_ _∼₂_ surjection surjection)
  where
  record IsFunctor : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
    constructor ∁
    field
      ⦃ `IsPrefunctor ⦄ : IsPrefunctor _∼₁_ _∼̇₁_ _↦₁_ _∼₂_ _∼̇₂_ _↦₂_ smap
      overlap ⦃ `IsCategory₁ ⦄ : IsCategory _∼₁_ _∼̇₁_ ε₁ _↦₁_
      overlap ⦃ `IsCategory₂ ⦄ : IsCategory _∼₂_ _∼̇₂_ ε₂ _↦₂_
      overlap ⦃ `𝒮urjidentity ⦄ : Surjidentity.class _∼₁_ _∼₂_ _∼̇₂_ smap ε₁ ε₂