text:
open import Prelude
open import Data.Nat using (_≤?_)
open import Data.Maybe using (Maybe; just; nothing; is-just)
open import Reflection using (_≟-Lit_; _≟-Name_)

open import RW.Language.RTerm
open import RW.Utils.Monads

module RW.Language.RTermUtils where

  open Monad {{...}}

  --   The complexity annotations might require
  --   a slight notational introduction.
  --
  --   If a variable name overlaps one in the corresponding type signature,
  --   this is intentional.
  --
  --   Sₜ is defined by (S t).
  --   #Fvₜ is defined by length (Fv t).
  --   Both measures are defined below.
  --

  --------------
  -- Measures --
  --------------

  -- The TERMINATING pragmas are required since Agda does not
  -- recognize a call to map as terminating.

  {-# TERMINATING #-}
  height : {A : Set} → RTerm A → ℕ
  height (ovar _)    = 0
  height (ivar _)    = 0
  height (rlit _)    = 0
  height (rlam t)    = 1 + height t
  height (rapp _ ts) = 1 + max* (map height ts)
    where
      max : ℕ → ℕ → ℕ
      max a b with a ≤? b
      ...| yes _ = b
      ...| no  _ = a

      max* : List ℕ → ℕ
      max* [] = 0
      max* (h ∷ t) = max h (max* t)

  {-# TERMINATING #-}
  S : {A : Set} → RTerm A → ℕ
  S (ovar _) = 1
  S (ivar _) = 1
  S (rlit _) = 1
  S (rlam t) = 1 + S t
  S (rapp n ts) = 1 + sum (map S ts)
    where open import Data.List using (sum)

  {-# TERMINATING #-}
  Fv : {A : Set} → RTerm A → List A
  Fv (ovar a) = a ∷ []
  Fv (ivar _) = []
  Fv (rlit _) = []
  Fv (rlam t) = Fv t
  Fv (rapp _ ts) = concatMap Fv ts
    where open import Data.List using (concatMap)

  -------------------------------------------------------
  -- Terms with Context
  --
  --   Holes will be represented by a nothing;
  pattern hole = ovar nothing

  isHole : ∀{a}{A : Set a} → RTerm (Maybe A) → Bool
  isHole (ovar nothing) = true
  isHole _              = false

  -- Term Intersection
  --
  -- Complexity analisys follows below.
  {-# TERMINATING #-}
  _∩_ : ∀{A} ⦃ eqA : Eq A ⦄
      → RTerm A → RTerm A → RTerm (Maybe A)
  _∩_ (rapp x ax) (rapp y ay) with x ≟-RTermName y
  ...| no  _ = ovar nothing
  ...| yes _ = rapp x (map (uncurry _∩_) (zip ax ay))
  _∩_ (ivar x) (ivar y) with x ≟-ℕ y
  ...| no  _ = ovar nothing
  ...| yes _ = ivar x
  _∩_ ⦃ eq _≟_ ⦄ (ovar x) (ovar y) with x ≟ y
  ...| no  _ = ovar nothing
  ...| yes _ = ovar (just x)
  _∩_ (rlit x) (rlit y) with x ≟-Lit y
  ...| no  _ = ovar nothing
  ...| yes _ = rlit x
  _∩_ (rlam x) (rlam y) = rlam (x ∩ y)
  _∩_ _ _ = ovar nothing

  -- The wors case for a intersection is, of course, both terms being
  -- equal. But in that case, (t ∩ t) is just a (fmap just), as we
  -- can see below.
  --
  -- Therefore, t ∩ t ∈ O(Sₜ)
  --
  -- In case we have two different terms, the smaller of
  -- them will make _∩_ halt. Therefore,
  --
  -- t ∩ u ∈ O(min(Sₜ , Sᵤ))
  --
  private
    mutual
      t∩t≡t : {A : Set}⦃ eqA : Eq A ⦄{t : RTerm A}
            → t ∩ t ≡ replace-A (ovar ∘ just) t
      t∩t≡t ⦃ eq _≟_ ⦄ {t = ovar x} with x ≟ x
      ...| yes x≡x = refl
      ...| no  x≢x = ⊥-elim (x≢x refl)
      t∩t≡t {t = ivar n} with n ≟-ℕ n
      ...| yes n≡n = refl
      ...| no  n≢n = ⊥-elim (n≢n refl)
      t∩t≡t {t = rlit l} with l ≟-Lit l
      ...| yes l≡l = refl
      ...| no  l≢l = ⊥-elim (l≢l refl)
      t∩t≡t {A} {t = rlam t}
        = trans (cong rlam (t∩t≡t {t = t}))
                (sym (lemma-replace-rlam {A = A} {f = ovar ∘ just} {t = t}))
      t∩t≡t {t = rapp n ts} with n ≟-RTermName n
      ...| no  n≢n = ⊥-elim (n≢n refl)
      ...| yes n≡n = cong (rapp n) t∩t≡t*

      t∩t≡t* : {A : Set}⦃ eqA : Eq A ⦄{ts : List (RTerm A)}
             → map (uncurry _∩_) (zip ts ts)
             ≡ map (replace-A (ovar ∘ just)) ts
      t∩t≡t* {ts = []} = refl
      t∩t≡t* {ts = t ∷ ts}
        rewrite sym (t∩t≡t {t = t}) = cong (_∷_ (t ∩ t)) (t∩t≡t* {ts = ts})

  -- Lifting holes.
  --
  --  Will translate every definition with only holes as arguments
  --  into a single hole.
  --
  --  The worst case for lifting holes is to find a term t
  --  with no holes. Therefore _↑ ∈ O(Sₜ).
  {-# TERMINATING #-}
  _↑ : ∀{a}{A : Set a} → RTerm (Maybe A) → RTerm (Maybe A)
  _↑ (rapp x []) = rapp x []
  _↑ (rapp x ax) with all isHole ax
  ...| true   = ovar nothing
  ...| false  = rapp x (map _↑ ax)
  _↑ (rlam x) = rlam (x ↑)
  _↑ t        = t

  -- It is commom to need only "linear" intersections;
  --
  -- _∩↑_ ∈ O(Sₜ + Sₜ) ≈ O(Sₜ)
  --
  _∩↑_ : ∀{A} ⦃ eqA : Eq A ⦄
       → RTerm A → RTerm A → RTerm (Maybe A)
  v ∩↑ u = (v ∩ u) ↑

  -- Casting
  ⊥2UnitCast : RTerm (Maybe ⊥) → RTerm Unit
  ⊥2UnitCast = replace-A (maybe ⊥-elim (ovar unit))

  -- Converting Holes to Abstractions
  --
  --  Will replace holes for "var 0",
  --  and increment every other non-captured variable.
  --
  {-# TERMINATING #-}
  holeElim : ℕ → RTerm Unit → RTerm ⊥
  holeElim d (ovar unit) = ivar zero
  holeElim d (ivar n) with suc n ≤? d
  ...| yes _ = ivar n
  ...| no  _ = ivar (suc n)
  holeElim d (rlit l) = rlit l
  holeElim d (rlam rt) = rlam (holeElim (suc d) rt)
  holeElim d (rapp n ts) = rapp n (map (holeElim d) ts)

  -- Specialized version for handling indexes.
  hole2Abs : RTerm Unit → RTerm ⊥
  hole2Abs = rlam ∘ holeElim 0

  hole2Absℕ : RTerm Unit → RTerm ℕ
  hole2Absℕ = replace-A ⊥-elim ∘ hole2Abs

  open import Data.String hiding (_++_)
  postulate
    err : ∀{a}{A : Set a} → String → A

  private
    joinInner : {A : Set} → List (Maybe (List A)) → Maybe (List A)
    joinInner [] = just []
    joinInner (nothing ∷ _) = nothing -- err "2"
    joinInner (just x ∷ xs) = maybe (λ l → just (x ++ l)) nothing (joinInner xs)

    lemma-joinInner : {A : Set}{x : List A}{l : List (Maybe (List A))}
                    → joinInner (just x ∷ l)
                    ≡ maybe (λ l → just (x ++ l)) nothing (joinInner l)
    lemma-joinInner = refl

  -- Term Subtraction
  --
  -- Compelxity analisys follows below.
  --
  {-# TERMINATING #-}
  _-_ : ∀{A} ⦃ eqA : Eq A ⦄ → RTerm (Maybe A) → RTerm A → Maybe (List (RTerm A))
  hole - t = return (t ∷ [])
  (rapp x ax) - (rapp y ay) with x ≟-RTermName y
  ...| no  _ = nothing -- err "1"
  ...| yes _ = joinInner (map (uncurry _-_) (zip ax ay))
  (rlam x) - (rlam y) = x - y
  x - y with x ≟-RTerm (replace-A (ovar ∘ just) y)
  ...| yes _ = just []
  ...| no  _ = nothing -- err "3"

  -- Similarly to _∩_, we will prove the worst case complexity
  -- based on lemma t-t≡Fvt.
  -- That is, looking at term subtraction, the wors possible case
  -- is that our roadmap (RTerm (Maybe A)) perfectly matches the
  -- term we are looking for, and has all occurences of ovars as holes.
  -- (a simple drawing might help to see this).
  --
  -- Well, when this is the case, our lemma tells us that
  -- subtraction is the same as getting the free variables
  -- and mapping ovar over them.
  --
  -- It is clear that we have some additional complexity on
  -- the function joinInner, but we will ignore this for
  -- the sake of simplicity, for now.
  -- If we consider that most of the lemmas do not have more than 10
  -- free variables, joinInner is of negligible run-time
  -- (TODO: dangerous afirmation!!)
  --
  -- We'll then say that _-_ ∈ O(#Fvₜ).
  --
  private
    fmap-nothing : {A : Set} → RTerm A → RTerm (Maybe A)
    fmap-nothing = replace-A (const $ ovar nothing)

    mutual
      t-t≡Fvt : {A : Set}⦃ eqA : Eq A ⦄(t : RTerm A)
              → (fmap-nothing t) - t
              ≡ just (map ovar (Fv t))
      t-t≡Fvt (ovar x) = refl
      t-t≡Fvt (ivar n) with n ≟-ℕ n
      ...| yes n≡n = refl
      ...| no  n≢n = ⊥-elim (n≢n refl)
      t-t≡Fvt (rlit l) with l ≟-Lit l
      ...| yes l≡l = refl
      ...| no  l≢l = ⊥-elim (l≢l refl)
      t-t≡Fvt (rlam t) = t-t≡Fvt t
      t-t≡Fvt (rapp n ts) with n ≟-RTermName n
      ...| yes n≡n = t-t≡Fvt* ts
      ...| no  n≢n = ⊥-elim (n≢n refl)

      t-t≡Fvt* : {A : Set}⦃ eqA : Eq A ⦄(ts : List (RTerm A))
               → joinInner (map (uncurry _-_) (zip (map fmap-nothing ts) ts))
               ≡ just (map ovar (concat (map Fv ts)))
      t-t≡Fvt* [] = refl
      t-t≡Fvt* (t ∷ ts)
        rewrite t-t≡Fvt t
        with joinInner (map (uncurry _-_) (zip (map fmap-nothing ts) ts))
           | t-t≡Fvt* ts
      t-t≡Fvt* (t ∷ ts) | nothing | ()
      t-t≡Fvt* (t ∷ ts) | just .(map ovar (foldr _++_ [] (map Fv ts)))
                        | refl
        = cong just (sym (map-++-commute ovar (Fv t) (concat (map Fv ts))))
        where open import Data.List.Properties using (map-++-commute)

  -- Term Subtraction, single result.
  --
  -- Disconsidering lazyness, (_-↓_ t) = fmap head ∘ (_-_ t)
  -- Therefore, _-↓_ ∈ O(#Fvₜ).
  --
  _-↓_ : ∀{A} ⦃ eqA : Eq A ⦄ → RTerm (Maybe A) → RTerm A → Maybe (RTerm A)
  t -↓ u with t - u
  ...| just []      = nothing
  ...| just (x ∷ _) = just x
  ...| nothing      = nothing

  -- Structural Manipulation

  {-# TERMINATING #-}
  map-ivar : {A : Set} → ℕ → (ℕ → RTerm A) → RTerm ⊥ → RTerm A
  map-ivar _ f (ovar ())
  map-ivar d f (ivar n) with d ≤? n
  ...| yes _ = f n
  ...| no  _ = ivar n
  map-ivar _ f (rlit l) = rlit l
  map-ivar d f (rlam t) = rlam (map-ivar (suc d) f t)
  map-ivar d f (rapp n ts) = rapp n (map (map-ivar d f) ts)

  -- Lift ivar's to ovar's
  lift-ivar : RTerm ⊥ → RTerm ℕ
  lift-ivar = map-ivar 0 ovar

  private
    last : {A : Set} → List A → Maybe A
    last [] = nothing
    last (x ∷ []) = just x
    last (_ ∷ xs) = last xs

    strip-last : {A : Set} → List A → List A
    strip-last [] = []
    strip-last (x ∷ []) = []
    strip-last (x ∷ xs) = x ∷ (strip-last xs)

    -- last argument
    larg : {B : Set} → RTerm B → Maybe (RTerm B)
    larg (rapp n []) = nothing
    larg (rapp n ts) = last ts
    larg _           = nothing

    dec : ℕ → ℕ
    dec zero = zero
    dec (suc x) = x

    strip-larg : {B : Set} → RTerm B → RTerm B
    strip-larg (rapp n ts) = rapp n (strip-last ts)
    strip-larg t           = t

    {-# TERMINATING #-}
    n-is-in : {B : Set} → ℕ → RTerm B → Bool
    n-is-in n (ivar k) = dec-elim (const true) (const false) (n ≟-ℕ k)
    n-is-in n (rapp _ ts) = foldr (λ h r → n-is-in n h or r) false ts
    n-is-in n (rlam t) = n-is-in (suc n) t
    n-is-in _ _ = false

  {-# TERMINATING #-}
  η : RTerm ⊥ → RTerm ⊥
  η (ovar x) = ovar x
  η (ivar n) = ivar n
  η (rlit l) = rlit l
  η (rlam t) with η t
  ...| t' with larg t'
  ...| just (ivar 0)
     = if n-is-in 0 (strip-larg t')
       then rlam t'
       else map-ivar 0 (ivar ∘ dec) (strip-larg t')
  ...| _             = rlam t'
  η (rapp n ts) = rapp n (map η ts)

  -- Models a binary application
  RBinApp : ∀{a} → Set a → Set _
  RBinApp A = RTermName × RTerm A × RTerm A

  -- Opens a term representing a binary application.
  forceBinary : ∀{a}{A : Set a}
              → RTerm A → Maybe (RBinApp A)
  forceBinary (rapp n (a₁ ∷ a₂ ∷ [])) = just (n , a₁ , a₂)
  forceBinary _                       = nothing

  -- Given a 'impl' chain, return it's result.
  typeResult : ∀{a}{A : Set a}
             → RTerm A → RTerm A
  typeResult (rapp impl (t1 ∷ t2 ∷ [])) = typeResult t2
  typeResult t = t

  -- Gives the length of a 'impl' chain.
  typeArity : ∀{a}{A : Set a} → RTerm A → ℕ
  typeArity (rapp impl (t1 ∷ t2 ∷ [])) = suc (typeArity t2)
  typeArity _                          = 0

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some defined operations (multiplication by natural number and
-- exponentiation)
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Operations.CommutativeMonoid
  {s₁ s₂} (CM : CommutativeMonoid s₁ s₂)
  where

open import Data.Nat.Base using (ℕ; zero; suc)
  renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.List as List using (List; []; _∷_; _++_)
open import Data.Fin using (Fin; zero)
open import Data.Product using (proj₁; proj₂)
open import Data.Table.Base as Table using (Table)
open import Function using (_∘_; _⟨_⟩_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open CommutativeMonoid CM
  renaming
  ( _∙_       to _+_
  ; ∙-cong    to +-cong
  ; identityˡ to +-identityˡ
  ; identityʳ to +-identityʳ
  ; assoc     to +-assoc
  ; comm      to +-comm
  ; ε         to 0#
  )
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Operations

-- Multiplication by natural number.

infixr 8 _×_ _×′_

_×_ : ℕ → Carrier → Carrier
0     × x = 0#
suc n × x = x + n × x

-- A variant that includes a "redundant" case which ensures that `1 × x`
-- is definitionally equal to `x`.

_×′_ : ℕ → Carrier → Carrier
0     ×′ x = 0#
1     ×′ x = x
suc n ×′ x = x + n ×′ x

-- Summation over lists/tables

sumₗ : List Carrier → Carrier
sumₗ = List.foldr _+_ 0#

sumₜ : ∀ {n} → Table Carrier n → Carrier
sumₜ = Table.foldr _+_ 0#

-- An alternative mathematical-style syntax for sumₜ

infixl 10 sumₜ-syntax

sumₜ-syntax : ∀ n → (Fin n → Carrier) → Carrier
sumₜ-syntax _ = sumₜ ∘ Table.tabulate

syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x

------------------------------------------------------------------------
-- Properties of _×_

×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
×-congʳ 0       x≈x′ = refl
×-congʳ (suc n) x≈x′ = x≈x′ ⟨ +-cong ⟩ ×-congʳ n x≈x′

×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×-cong {u} P.refl x≈x′ = ×-congʳ u x≈x′

-- _×_ is homomorphic with respect to _ℕ+_/_+_.

×-homo-+ : ∀ c m n → (m ℕ+ n) × c ≈ m × c + n × c
×-homo-+ c 0       n = sym (+-identityˡ (n × c))
×-homo-+ c (suc m) n = begin
  c + (m ℕ+ n) × c     ≈⟨ +-cong refl (×-homo-+ c m n) ⟩
  c + (m × c + n × c)  ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩
  c + m × c + n × c    ∎

------------------------------------------------------------------------
-- Properties of _×′_

1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
1+×′ 0       x = sym (+-identityʳ x)
1+×′ (suc n) x = refl

-- _×_ and _×′_ are extensionally equal (up to the setoid
-- equivalence).

×≈×′ : ∀ n x → n × x ≈ n ×′ x
×≈×′ 0       x = begin 0# ∎
×≈×′ (suc n) x = begin
  x + n × x   ≈⟨ +-cong refl (×≈×′ n x) ⟩
  x + n ×′ x  ≈⟨ sym (1+×′ n x) ⟩
  suc n ×′ x  ∎

-- _×′_ is homomorphic with respect to _ℕ+_/_+_.

×′-homo-+ : ∀ c m n → (m ℕ+ n) ×′ c ≈ m ×′ c + n ×′ c
×′-homo-+ c m n = begin
  (m ℕ+ n) ×′ c    ≈⟨ sym (×≈×′ (m ℕ+ n) c) ⟩
  (m ℕ+ n) ×  c    ≈⟨ ×-homo-+ c m n ⟩
  m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
  m ×′ c + n ×′ c  ∎

-- _×′_ preserves equality.

×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
×′-cong {n} {_} {x} {y} P.refl x≈y = begin
  n  ×′ x ≈⟨ sym (×≈×′ n x) ⟩
  n  ×  x ≈⟨ ×-congʳ n x≈y ⟩
  n  ×  y ≈⟨ ×≈×′ n y ⟩
  n  ×′ y ∎

ext: agda


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

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

ap : {A B : Set} (f : A → B) {x y : A}
  → x == y → f x == f y
ap f idp = idp

postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ (A : Set) (base* : A) (loop* : base* == base*) where
  postulate
    Circle-rec : Circle → A
    Circle-base-β : Circle-rec base == base*
  {-# REWRITE Circle-base-β #-}
  postulate
    Circle-loop-β : ap Circle-rec loop == loop*
  {-# REWRITE Circle-loop-β #-}

test : (x : Circle) → ap (Circle-rec (Circle → Circle) (λ y → y) idp x) loop == idp
test x = idp

{-
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:178
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --type-in-type --no-pattern-matching #-}
open import Spire.IDarkwingDuck.Primitive
module Spire.IDarkwingDuck.Derived where

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

ISet : Set → Set
ISet I = I → Set

Enum : Set
Enum = List String

Tag : Enum → Set
Tag xs = PointsTo String xs

proj₁ : ∀{A B} → Σ A B → A
proj₁ = elimPair _ (λ a b → a)

proj₂ : ∀{A B} (ab : Σ A B) → B (proj₁ ab)
proj₂ = elimPair _ (λ a b → b)

Branches : (E : List String) (P : Tag E → Set) → Set
Branches = elimList _
  (λ P → ⊤)
  (λ l E ih P → Σ (P here) (λ _ → ih (λ t → P (there t))))

case' : (E : List String) (t : Tag E) (P : Tag E → Set) (cs : Branches E P) → P t
case' = elimPointsTo _
  (λ l E P c,cs → proj₁ c,cs)
  (λ l E t ih P c,cs → ih (λ t → P (there t)) (proj₂ c,cs))

case : {E : List String} (P : Tag E → Set) (cs : Branches E P) (t : Tag E) → P t
case P cs t = case' _ t P cs

Elᵀ  : Tel → Set
Elᵀ = elimTel _ ⊤ (λ A B ih → Σ A ih) (λ A B ih → Σ A ih)

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

UncurriedBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
UncurriedBranches E P X = Branches E P → X

CurriedBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → Set
CurriedBranches = elimList _
  (λ P X → X)
  (λ l E ih P X → P here → ih (λ t → P (there t)) X)

curryBranches : (E : Enum) (P : Tag E → Set) (X : Set)
  → UncurriedBranches E P X → CurriedBranches E P X
curryBranches = elimList _
  (λ P X f → f tt)
  (λ l E ih P X f c → ih (λ t → P (there t)) X (λ cs → f (c , cs)))

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

UncurriedElᵀ : (T : Tel) (X : Elᵀ T → Set) → Set
UncurriedElᵀ T X = (xs : Elᵀ T) → X xs

CurriedElᵀ : (T : Tel) (X : Elᵀ T → Set) → Set
CurriedElᵀ = elimTel _
  (λ X → X tt)
  (λ A B ih X → (a : A) → ih a (λ b → X (a , b)))
  (λ A B ih X → {a : A} → ih a (λ b → X (a , b)))

curryElᵀ : (T : Tel) (X : Elᵀ T → Set)
  → UncurriedElᵀ T X → CurriedElᵀ T X
curryElᵀ = elimTel _
  (λ X f → f tt)
  (λ A B ih X f a → ih a (λ b → X (a , b)) (λ b → f (a , b)))
  (λ A B ih X f {a} → ih a (λ b → X (a , b)) (λ b → f (a , b)))

uncurryElᵀ : (T : Tel) (X : Elᵀ T → Set)
  → CurriedElᵀ T X → UncurriedElᵀ T X
uncurryElᵀ = elimTel _
  (λ X x → elimUnit X x)
  (λ A B ih X f → elimPair X (λ a b → ih a (λ b → X (a , b)) (f a) b))
  (λ A B ih X f → elimPair X (λ a b → ih a (λ b → X (a , b)) f b))

ICurriedElᵀ : (T : Tel) (X : Elᵀ T → Set) → Set
ICurriedElᵀ = elimTel _
  (λ X → X tt)
  (λ A B ih X → {a : A} → ih a (λ b → X (a , b)))
  (λ A B ih X → {a : A} → ih a (λ b → X (a , b)))

icurryElᵀ : (T : Tel) (X : Elᵀ T → Set)
  → UncurriedElᵀ T X → ICurriedElᵀ T X
icurryElᵀ = elimTel _
  (λ X f → f tt)
  (λ A B ih X f {a} → ih a (λ b → X (a , b)) (λ b → f (a , b)))
  (λ A B ih X f {a} → ih a (λ b → X (a , b)) (λ b → f (a , b)))

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

UncurriedElᴰ : {I : Set} (D : Desc I) (X : ISet I) → Set
UncurriedElᴰ D X = ∀{i} → Elᴰ D X i → X i

CurriedElᴰ : {I : Set} (D : Desc I) (X : ISet I) → Set
CurriedElᴰ = elimDesc _
  (λ i X → X i)
  (λ i D ih X → (x : X i) → ih X )
  (λ A B ih X → (a : A) → ih a X)
  (λ A B ih X → {a : A} → ih a X)

curryElᴰ : {I : Set} (D : Desc I) (X : ISet I)
  → UncurriedElᴰ D X → CurriedElᴰ D X
curryElᴰ = elimDesc _
  (λ i X cn → cn refl)
  (λ i D ih X cn x → ih X (λ xs → cn (x , xs)))
  (λ A B ih X cn a → ih a X (λ xs → cn (a , xs)))
  (λ A B ih X cn {a} → ih a X (λ xs → cn (a , xs)))

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

UncurriedHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedElᴰ D X)
  → Set
UncurriedHyps D X P cn =
  ∀ i (xs : Elᴰ D X i) (ihs : Hyps D X P i xs) → P i (cn xs)

CurriedHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedElᴰ D X)
  → Set
CurriedHyps = elimDesc _
  (λ i X P cn → P i (cn refl))
  (λ i D ih X P cn → (x : X i) → P i x → ih X P (λ xs → cn (x , xs)))
  (λ A B ih X P cn → (a : A) → ih a X P (λ xs → cn (a , xs)))
  (λ A B ih X P cn → {a : A} → ih a X P (λ xs → cn (a , xs)))

uncurryHyps : {I : Set} (D : Desc I) (X : ISet I)
  (P : (i : I) → X i → Set)
  (cn : UncurriedElᴰ D X)
  → CurriedHyps D X P cn
  → UncurriedHyps D X P cn
uncurryHyps = elimDesc _
  (λ j X P cn pf →
    elimEq _ (λ u → pf))
  (λ j D ih X P cn pf i →
    elimPair _ (λ x xs ih,ihs →
      ih X P (λ ys → cn (x , ys)) (pf x (proj₁ ih,ihs)) i xs (proj₂ ih,ihs)))
  (λ A B ih X P cn pf i →
    elimPair _ (λ a xs → ih a X P (λ ys → cn (a , ys)) (pf a) i xs))
  (λ A B ih X P cn pf i →
    elimPair _ (λ a xs → ih a X P (λ ys → cn (a , ys)) pf i xs))

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

record Data : Set where
  field
    P : Tel
    I : Elᵀ P → Tel
    E : Enum
    B : (A : Elᵀ P) → Branches E (λ _ → Desc (Elᵀ (I A)))

  C : (A : Elᵀ P) → Tag E → Desc (Elᵀ (I A))
  C A = case (λ _ → Desc (Elᵀ (I A))) (B A)

  D : (A : Elᵀ P) → Desc (Elᵀ (I A))
  D A = Arg (Tag E) (C A)

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

Decl :
  (P : Tel)
  (I : CurriedElᵀ P (λ _ → Tel))
  (E : Enum)
  (B : let I = uncurryElᵀ P (λ _ → Tel) I
      in CurriedElᵀ P λ A → Branches E (λ _ → Desc (Elᵀ (I A))))
  → Data
Decl P I E B = record
  { P = P
  ; I = uncurryElᵀ P _ I
  ; E = E
  ; B = uncurryElᵀ P _ B
  }

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

End[_] : (I : Tel)
  → CurriedElᵀ I (λ _ → Desc (Elᵀ I))
End[_] I = curryElᵀ I _ End

Rec[_] : (I : Tel)
  → CurriedElᵀ I (λ _ → Desc (Elᵀ I) → Desc (Elᵀ I))
Rec[_] I = curryElᵀ I _ Rec

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

FormUncurried : (R : Data)
  → UncurriedElᵀ (Data.P R) λ p
  → UncurriedElᵀ (Data.I R p) λ i
  → Set
FormUncurried R p i = μ (Data.D R p) i

Form : (R : Data)
  → CurriedElᵀ (Data.P R) λ p
  → CurriedElᵀ (Data.I R p) λ i
  → Set
Form R =
  curryElᵀ (Data.P R) (λ p → CurriedElᵀ (Data.I R p) λ i → Set) λ p →
  curryElᵀ (Data.I R p) (λ i → Set) λ i →
  FormUncurried R p i

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

injUncurried : (R : Data)
  → UncurriedElᵀ (Data.P R) λ p
  → let D = Data.D R p
  in CurriedElᴰ D (μ D)
injUncurried R p t = curryElᴰ (Data.C R p t)
  (μ (Data.D R p))
  (λ xs → init (t , xs))

inj : (R : Data)
  → ICurriedElᵀ (Data.P R) λ p
  → let D = Data.D R p
  in CurriedElᴰ D (μ D)
inj R = icurryElᵀ (Data.P R)
  (λ p → let D = Data.D R p in CurriedElᴰ D (μ D))
  (injUncurried R)

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

indCurried : {I : Set} (D : Desc I)
  (M : (i : I) → μ D i → Set)
  (f : CurriedHyps D (μ D) M init)
  (i : I)
  (x : μ D i)
  → M i x
indCurried D M f i x =
  ind D M (uncurryHyps D (μ D) M init f) i x

SumCurriedHyps : (R : Data)
  → UncurriedElᵀ (Data.P R) λ p
  → let D = Data.D R p in
  (M : CurriedElᵀ (Data.I R p) (λ i → μ D i → Set))
  → Tag (Data.E R) → Set
SumCurriedHyps R p M t =
  let unM = uncurryElᵀ (Data.I R p) (λ i → μ (Data.D R p) i → Set) M in
  CurriedHyps (Data.C R p t) (μ (Data.D R p)) unM (λ xs → init (t , xs))

elimUncurried : (R : Data)
  → UncurriedElᵀ (Data.P R) λ p
  → let D = Data.D R p in
  (M : CurriedElᵀ (Data.I R p) (λ i → μ D i → Set))
  → let unM = uncurryElᵀ (Data.I R p) (λ i → μ D i → Set) M
  in UncurriedBranches (Data.E R)
     (SumCurriedHyps R p M)
     (CurriedElᵀ (Data.I R p) (λ i → (x : μ D i) → unM i x))
elimUncurried R p M cs =
  let D = Data.D R p
      unM = uncurryElᵀ (Data.I R p) (λ i → μ D i → Set) M
  in
  curryElᵀ (Data.I R p) (λ i → (x : μ D i) → unM i x) λ i x →
  indCurried (Data.D R p) unM
    (case (SumCurriedHyps R p M) cs)
    i x

elim : (R : Data)
  → ICurriedElᵀ (Data.P R) λ p
  → let D = Data.D R p in
  (M : CurriedElᵀ (Data.I R p) (λ i → μ D i → Set))
  → let unM = uncurryElᵀ (Data.I R p) (λ i → μ D i → Set) M
  in CurriedBranches (Data.E R)
     (SumCurriedHyps R p M)
     (CurriedElᵀ (Data.I R p) (λ i → (x : μ D i) → unM i x))
elim R = icurryElᵀ (Data.P R)
  (λ p → let D = Data.D R p in
    (M : CurriedElᵀ (Data.I R p) (λ i → μ D i → Set))
    → let unM = uncurryElᵀ (Data.I R p) (λ i → μ D i → Set) M
    in CurriedBranches (Data.E R)
       (SumCurriedHyps R p M)
       (CurriedElᵀ (Data.I R p) (λ i → (x : μ D i) → unM i x)))
  (λ p M → curryBranches (Data.E R) _ _
    (elimUncurried R p M))

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

max_stars_repo_name: spire/spire

max_issues_repo_name: spire/spire

max_forks_repo_name: spire/spire


text:
module Relator.Equals.Proofs where

import      Lvl
open import Functional as Fn using (_→ᶠ_ ; _∘_)
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Propositional.Proofs.Structures
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv public
open import Structure.Function.Names
open import Structure.Relator.Properties
open import Structure.Setoid using (Equiv ; intro) renaming (_≡_ to _≡ₛ_)
open import Structure.Type.Identity
open import Syntax.Function
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ ℓₑ ℓₚ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x y : T

[≡]-coercion : (_≡_ {T = Type{ℓ}}) ⊆₂ (_→ᶠ_)
[≡]-coercion = [≡]-sub-of-reflexive

[≡]-unsubstitution : (∀{f : T → Stmt} → f(x) → f(y)) → (x ≡ y)
[≡]-unsubstitution {x = x} F = F {x ≡_} [≡]-intro

-- The statement that two functions are equal when all their values are equal are not provable.
-- Also called: Extensional equality, function extensionality.
-- [≡]-function : ∀{A B : Type}{f₁ f₂ : A → B) → (∀{x} → (f₁(x) ≡ f₂(x))) → (f₁ ≡ f₂)

[≡]-function-application : FunctionApplication A B
[≡]-function-application [≡]-intro = [≡]-intro

[≡]-with-specific : ∀{x y : A} → (f : (a : A) → ⦃ _ : (a ≡ x) ⦄ → ⦃ _ : (a ≡ y) ⦄ → B) → (p : (x ≡ y)) → (f(x) ⦃ [≡]-intro ⦄ ⦃ p ⦄ ≡ f(y) ⦃ symmetry(_≡_) p ⦄ ⦃ [≡]-intro ⦄)
[≡]-with-specific f [≡]-intro = [≡]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module T where

open import Prelude

module GÖDEL-T where

  -- Core syntax
  infixr 30 _⇒_
  infixl 30 _$_
  data TTp : Set where
    nat : TTp
    _⇒_ : (A B : TTp) → TTp

  Ctx = List TTp

  data TExp (Γ : Ctx) : TTp → Set where
    var : ∀{A} (x : A ∈ Γ) → TExp Γ A
    Λ : ∀{A B} (e : TExp (A :: Γ) B) → TExp Γ (A ⇒ B)
    _$_ : ∀{A B} (e₁ : TExp Γ (A ⇒ B)) (e₂ : TExp Γ A) → TExp Γ B
    zero : TExp Γ nat
    suc : (e : TExp Γ nat) → TExp Γ nat
    rec : ∀{A} → (e : TExp Γ nat) → (e₀ : TExp Γ A) → (es : TExp (A :: Γ) A) →
               TExp Γ A

  TCExp = TExp []
  TNat = TCExp nat

  ---- denotational semantics
  interp : TTp → Set
  interp nat = Nat
  interp (A ⇒ B) = interp A → interp B

  meaningη : (Γ : Ctx) → Set
  meaningη Γ = ∀{A} (x : A ∈ Γ) → interp A

  emptyη : meaningη []
  emptyη ()

  extendη : ∀{Γ A} → meaningη Γ → interp A → meaningη (A :: Γ)
  extendη η M Z = M
  extendη η M (S n) = η n

  meaning : ∀{A Γ} → TExp Γ A → meaningη Γ → interp A
  meaning (var x) η = η x
  meaning (Λ e) η = λ x → meaning e (extendη η x)
  meaning (e₁ $ e₂) η = meaning e₁ η (meaning e₂ η)
  meaning zero η = Z
  meaning (suc e) η = S (meaning e η)
  meaning (rec e e₀ es) η = NAT.fold (meaning e₀ η)
                                     (λ n x → meaning es (extendη η x))
                                     (meaning e η)

  cmeaning : ∀{A} → TCExp A → interp A
  cmeaning e = meaning e emptyη

  ---- Definition related to substitution.
  -- Renamings
  TRen : Ctx → Ctx → Set
  TRen Γ Γ' = ∀ {A} → A ∈ Γ → A ∈ Γ'

  renId : ∀{Γ} → TRen Γ Γ
  renId = \ x -> x

  renComp : ∀{B Γ Δ} → TRen Γ Δ → TRen B Γ → TRen B Δ
  renComp f g = f o g

  wk : ∀{Γ Γ' A} → TRen Γ Γ' → TRen (A :: Γ) (A :: Γ')
  wk f Z = Z
  wk f (S n) = S (f n)

  ren : ∀{Γ Γ'} → TRen Γ Γ' → ∀ {A} → TExp Γ A → TExp Γ' A
  ren γ (var x) = var (γ x)
  ren γ (Λ e) = Λ (ren (wk γ) e)
  ren γ (e₁ $ e₂) = (ren γ e₁) $ (ren γ e₂)
  ren γ zero = zero
  ren γ (suc e) = suc (ren γ e)
  ren γ (rec e e₀ es) = rec (ren γ e) (ren γ e₀) (ren (wk γ) es)

  -- Substitutions
  TSubst : Ctx → Ctx → Set
  TSubst Γ Γ' = ∀ {A} → A ∈ Γ → TExp Γ' A

  emptyγ : ∀{Γ} → TSubst Γ Γ
  emptyγ = λ x → var x

  liftγ : ∀{Γ Γ' A} → TSubst Γ Γ' → TSubst (A :: Γ) (A :: Γ')
  liftγ γ Z = var Z
  liftγ γ (S n) = ren S (γ n)

  singγ : ∀{Γ A} → TExp Γ A → TSubst (A :: Γ) Γ
  singγ e Z = e
  singγ e (S n) = var n

  dropγ : ∀{Γ A Γ'} → TSubst (A :: Γ) Γ' → TSubst Γ Γ'
  dropγ γ n = γ (S n)

  closed-wkγ : {Γ : Ctx} → TRen [] Γ
  closed-wkγ ()

  ssubst : ∀{Γ Γ' C} →
           (γ : TSubst Γ Γ') →
           (e : TExp Γ C) →
           TExp Γ' C
  ssubst γ (var x) = γ x
  ssubst γ (Λ e) = Λ (ssubst (liftγ γ) e)
  ssubst γ (e₁ $ e₂) = (ssubst γ e₁) $ (ssubst γ e₂)
  ssubst γ zero = zero
  ssubst γ (suc e) = suc (ssubst γ e)
  ssubst γ (rec e e₀ es) = rec (ssubst γ e) (ssubst γ e₀) (ssubst (liftγ γ) es)

  subComp : ∀{B Γ Γ'} → TSubst Γ Γ' → TSubst B Γ → TSubst B Γ'
  subComp f g = ssubst f o g

  extendγ : ∀{Γ Γ' A} → TSubst Γ Γ' → TExp Γ' A → TSubst (A :: Γ) Γ'
  extendγ γ e = subComp (singγ e) (liftγ γ)

  -- substituting one thing in a closed term
  subst : ∀{A C} → (e' : TCExp A) → (e : TExp (A :: []) C) → TCExp C
  subst e' e = ssubst (singγ e') e

  weaken-closed : ∀{Γ B} → TCExp B → TExp Γ B
  weaken-closed e = ren closed-wkγ e

  ---- dynamic semantics (and, implicitly, preservation)
  data TVal : ∀{Γ A} → TExp Γ A → Set where
    val-zero : ∀{Γ} → TVal {Γ} zero
    val-suc : ∀{Γ e} → TVal {Γ} e → TVal {Γ} (suc e)
    val-lam : ∀{A B} {e : TExp (A :: []) B} → TVal (Λ e)

  -- only worry about closed steps; embed preservation in the statement
  -- We are call-by-name for function application, but call-by-value for natural evaluation.
  -- This is so that any value of type nat is a numeral.
  data _~>_ : ∀{A} → TCExp A → TCExp A → Set where
    step-app-l : ∀{A B} {e₁ e₁' : TCExp (A ⇒ B)} {e₂ : TCExp A} →
                  e₁ ~> e₁' → (e₁ $ e₂) ~> (e₁' $ e₂)
    step-beta  : ∀{A B} {e : TExp (A :: []) B} {e' : TCExp A} →
                  ((Λ e) $ e') ~> (subst e' e)
    step-suc   : ∀{e e' : TCExp nat} →
                  e ~> e' → (suc e) ~> (suc e')
    step-rec   : ∀{A} {e e' : TCExp nat} {e₀ : TCExp A} {es : TExp (A :: []) A} →
                  e ~> e' → (rec e e₀ es) ~> (rec e' e₀ es)
    step-rec-z : ∀{A} {e₀ : TCExp A} {es : TExp (A :: []) A} →
                  (rec zero e₀ es) ~> e₀
    step-rec-s : ∀{A} {e : TCExp nat} {e₀ : TCExp A} {es : TExp (A :: []) A} →
                  TVal e → (rec (suc e) e₀ es) ~> subst (rec e e₀ es) es

  -- iterated stepping
  data _~>*_ : ∀{A} → TCExp A → TCExp A → Set where
    eval-refl : ∀{A} {e : TCExp A} → e ~>* e
    eval-cons : ∀{A} {e e' e'' : TCExp A} →
               e ~> e' → e' ~>* e'' → e ~>* e''

  eval-step : ∀{A} {e e' : TCExp A} → e ~> e' → e ~>* e'
  eval-step s = eval-cons s eval-refl

  -- Should I use a record, or the product thing, or something else?
  data THalts : ∀{A} → TCExp A → Set where
    halts : {A : TTp} {e e' : TCExp A} → (eval : (e ~>* e')) → (val : TVal e') → THalts e

open GÖDEL-T public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text: module Categories.Preorder where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------------
-- Totality properties respect to OrdList (flatten-OrdList-helper)
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.Totality.OrdList.FlattenATP where

open import FOTC.Base
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.Type
open import FOTC.Program.SortList.Properties.Totality.BoolATP
open import FOTC.Program.SortList.Properties.Totality.ListN-ATP
open import FOTC.Program.SortList.Properties.Totality.OrdTreeATP
open import FOTC.Program.SortList.Properties.MiscellaneousATP
open import FOTC.Program.SortList.SortList

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

flatten-OrdList-helper : ∀ {t₁ i t₂} → Tree t₁ → N i → Tree t₂ →
                         OrdTree (node t₁ i t₂) →
                         ≤-Lists (flatten t₁) (flatten t₂)

flatten-OrdList-helper {t₂ = t₂} tnil Ni Tt₂ OTt =
  subst (λ t → ≤-Lists t (flatten t₂))
        (sym (flatten-nil))
        (le-Lists-[] (flatten t₂))

flatten-OrdList-helper (ttip {i₁} Ni₁) Tt₁ tnil OTt = prf
  where postulate prf : ≤-Lists (flatten (tip i₁)) (flatten nil)
        {-# ATP prove prf #-}

flatten-OrdList-helper {i = i} (ttip {i₁} Ni₁) Ni (ttip {i₂} Ni₂) OTt = prf
  where
  postulate lemma : i₁ ≤ i₂
  {-# ATP prove lemma ≤-trans &&-list₄-t le-ItemTree-Bool le-TreeItem-Bool ordTree-Bool #-}

  postulate prf : ≤-Lists (flatten (tip i₁)) (flatten (tip i₂))
  {-# ATP prove prf lemma #-}

flatten-OrdList-helper {i = i} (ttip {i₁} Ni₁) Ni
                       (tnode {t₂₁} {i₂} {t₂₂} Tt₂₁ Ni₂ Tt₂₂) OTt = prf
  where
  -- Helper terms to get the conjuncts from OTt.
  helper₁ = ordTree-Bool (ttip Ni₁)
  helper₂ = ordTree-Bool (tnode Tt₂₁ Ni₂ Tt₂₂)
  helper₃ = le-TreeItem-Bool (ttip Ni₁) Ni
  helper₄ = le-ItemTree-Bool Ni (tnode Tt₂₁ Ni₂ Tt₂₂)
  helper₅ = trans (sym (ordTree-node (tip i₁) i (node t₂₁ i₂ t₂₂))) OTt

  -- Helper terms to get the conjuncts from the fourth conjunct of OTt
  helper₆ = le-ItemTree-Bool Ni Tt₂₁
  helper₇ = le-ItemTree-Bool Ni Tt₂₂
  helper₈ = trans (sym (le-ItemTree-node i t₂₁ i₂ t₂₂))
                  (&&-list₄-t₄ helper₁ helper₂ helper₃ helper₄ helper₅)

  -- Common terms for the lemma₁ and lemma₂.
  -- The ATPs could not figure out them.
  OrdTree-tip-i₁ : OrdTree (tip i₁)
  OrdTree-tip-i₁ = &&-list₄-t₁ helper₁ helper₂ helper₃ helper₄ helper₅

  ≤-TreeItem-tip-i₁-i : ≤-TreeItem (tip i₁) i
  ≤-TreeItem-tip-i₁-i = &&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅

  lemma₁ : ≤-Lists (flatten (tip i₁)) (flatten t₂₁)
  lemma₁ = flatten-OrdList-helper (ttip Ni₁) Ni Tt₂₁ OT
    where
    -- The ATPs could not figure these terms.
    OrdTree-t₂₁ : OrdTree t₂₁
    OrdTree-t₂₁ =
      leftSubTree-OrdTree Tt₂₁ Ni₂ Tt₂₂
                          (&&-list₄-t₂ helper₁ helper₂ helper₃ helper₄ helper₅)

    ≤-ItemTree-i-t₂₁ : ≤-ItemTree i t₂₁
    ≤-ItemTree-i-t₂₁ = &&-list₂-t₁ helper₆ helper₇ helper₈

    postulate OT : OrdTree (node (tip i₁) i t₂₁)
    {-# ATP prove OT ≤-TreeItem-tip-i₁-i ≤-ItemTree-i-t₂₁ OrdTree-tip-i₁ OrdTree-t₂₁ #-}

  lemma₂ : ≤-Lists (flatten (tip i₁)) (flatten t₂₂)
  lemma₂ = flatten-OrdList-helper (ttip Ni₁) Ni Tt₂₂ OT
    where
    -- The ATPs could not figure these terms.
    OrdTree-t₂₂ : OrdTree t₂₂
    OrdTree-t₂₂ =
      rightSubTree-OrdTree Tt₂₁ Ni₂ Tt₂₂
                           (&&-list₄-t₂ helper₁ helper₂ helper₃ helper₄ helper₅)

    ≤-ItemTree-i-t₂₂ : ≤-ItemTree i t₂₂
    ≤-ItemTree-i-t₂₂ = &&-list₂-t₂ helper₆ helper₇ helper₈

    postulate OT : OrdTree (node (tip i₁) i t₂₂)
    {-# ATP prove OT ≤-TreeItem-tip-i₁-i ≤-ItemTree-i-t₂₂ OrdTree-tip-i₁ OrdTree-t₂₂ #-}

  postulate prf : ≤-Lists (flatten (tip i₁)) (flatten (node t₂₁ i₂ t₂₂))
  {-# ATP prove prf xs≤ys→xs≤zs→xs≤ys++zs flatten-ListN lemma₁ lemma₂ #-}

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂)
                       Ni tnil OTt = prf
  where
  -- Helper terms to get the conjuncts from OTt.
  helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
  helper₂ = ordTree-Bool tnil
  helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
  helper₄ = le-ItemTree-Bool Ni tnil
  helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i nil)) OTt

  -- Helper terms to get the conjuncts from the third conjunct of OTt.
  helper₆ = le-TreeItem-Bool Tt₁₁ Ni
  helper₇ = le-TreeItem-Bool Tt₁₂ Ni
  helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                  (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

  lemma₁ : ≤-Lists (flatten t₁₁) (flatten nil)
  lemma₁ = flatten-OrdList-helper Tt₁₁ Ni tnil OT
    where
    postulate OT : OrdTree (node t₁₁ i nil)
    {-# ATP prove OT leftSubTree-OrdTree &&-list₂-t &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  lemma₂ : ≤-Lists (flatten t₁₂) (flatten nil)
  lemma₂ = flatten-OrdList-helper Tt₁₂ Ni tnil OT
    where
    postulate OT : OrdTree (node t₁₂ i nil)
    {-# ATP prove OT rightSubTree-OrdTree &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  postulate prf : ≤-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten nil)
  {-# ATP prove prf xs≤zs→ys≤zs→xs++ys≤zs flatten-ListN lemma₁ lemma₂ #-}

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂) Ni
                       (ttip {i₂} Ni₂) OTt = prf
  where
  -- Helper terms to get the conjuncts from OTt.
  helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
  helper₂ = ordTree-Bool (ttip Ni₂)
  helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
  helper₄ = le-ItemTree-Bool Ni (ttip Ni₂)
  helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i (tip i₂))) OTt

  -- Helper terms to get the conjuncts from the third conjunct of OTt.
  helper₆ = le-TreeItem-Bool Tt₁₁ Ni
  helper₇ = le-TreeItem-Bool Tt₁₂ Ni
  helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                  (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

  lemma₁ : ≤-Lists (flatten t₁₁) (flatten (tip i₂))
  lemma₁ = flatten-OrdList-helper Tt₁₁ Ni (ttip Ni₂) OT
    where
    postulate OT : OrdTree (node t₁₁ i (tip i₂))
    {-# ATP prove OT leftSubTree-OrdTree &&-list₂-t &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  lemma₂ : ≤-Lists (flatten t₁₂) (flatten (tip i₂))
  lemma₂ = flatten-OrdList-helper Tt₁₂ Ni (ttip Ni₂) OT
    where
    postulate OT : OrdTree (node t₁₂ i (tip i₂))
    {-# ATP prove OT rightSubTree-OrdTree &&-list₂-t &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  postulate prf : ≤-Lists (flatten (node t₁₁ i₁ t₁₂)) (flatten (tip i₂))
  {-# ATP prove prf xs≤zs→ys≤zs→xs++ys≤zs flatten-ListN lemma₁ lemma₂ #-}

flatten-OrdList-helper {i = i} (tnode {t₁₁} {i₁} {t₁₂} Tt₁₁ Ni₁ Tt₁₂) Ni
                       (tnode {t₂₁} {i₂} {t₂₂} Tt₂₁ Ni₂ Tt₂₂) OTt = prf
  where
  -- Helper terms to get the conjuncts from OTt.
  helper₁ = ordTree-Bool (tnode Tt₁₁ Ni₁ Tt₁₂)
  helper₂ = ordTree-Bool (tnode Tt₂₁ Ni₂ Tt₂₂)
  helper₃ = le-TreeItem-Bool (tnode Tt₁₁ Ni₁ Tt₁₂) Ni
  helper₄ = le-ItemTree-Bool Ni (tnode Tt₂₁ Ni₂ Tt₂₂)
  helper₅ = trans (sym (ordTree-node (node t₁₁ i₁ t₁₂) i (node t₂₁ i₂ t₂₂)))
                    OTt

  -- Helper terms to get the conjuncts from the third conjunct of OTt.
  helper₆ = le-TreeItem-Bool Tt₁₁ Ni
  helper₇ = le-TreeItem-Bool Tt₁₂ Ni
  helper₈ = trans (sym (le-TreeItem-node t₁₁ i₁ t₁₂ i))
                  (&&-list₄-t₃ helper₁ helper₂ helper₃ helper₄ helper₅)

  lemma₁ : ≤-Lists (flatten t₁₁) (flatten (node t₂₁ i₂ t₂₂))
  lemma₁ = flatten-OrdList-helper Tt₁₁ Ni (tnode Tt₂₁ Ni₂ Tt₂₂) OT
    where
    postulate OT : OrdTree (node t₁₁ i (node t₂₁ i₂ t₂₂))
    {-# ATP prove OT leftSubTree-OrdTree &&-list₂-t &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  lemma₂ : ≤-Lists (flatten t₁₂) (flatten (node t₂₁ i₂ t₂₂))
  lemma₂ = flatten-OrdList-helper Tt₁₂ Ni (tnode Tt₂₁ Ni₂ Tt₂₂) OT
    where
    postulate OT : OrdTree (node t₁₂ i (node t₂₁ i₂ t₂₂))
    {-# ATP prove OT rightSubTree-OrdTree &&-list₂-t &&-list₄-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ helper₇ helper₈ #-}

  postulate prf : ≤-Lists (flatten (node t₁₁ i₁ t₁₂))
                  (flatten (node t₂₁ i₂ t₂₂))
  {-# ATP prove prf xs≤zs→ys≤zs→xs++ys≤zs flatten-ListN lemma₁ lemma₂ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.HITs.Ints.QuoInt

open import Cubical.Data.Nat as ℕ hiding (_·_)
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Sigma

open import Cubical.Data.Nat.GCD
open import Cubical.Data.Nat.Coprime

-- ℚ as the set of coprime pairs in ℤ × ℕ₊₁

ℚ : Type₀
ℚ = Σ[ (a , b) ∈ ℤ × ℕ₊₁ ] areCoprime (abs a , ℕ₊₁→ℕ b)

isSetℚ : isSet ℚ
isSetℚ = isSetΣ (isSet× isSetℤ (subst isSet 1+Path isSetℕ)) (λ _ → isProp→isSet isPropIsGCD)

signedPair : Sign → ℕ × ℕ₊₁ → ℤ × ℕ₊₁
signedPair s (a , b) = (signed s a , b)

[_] : ℤ × ℕ₊₁ → ℚ
[ signed s a , b ] = signedPair s (toCoprime (a , b)) , toCoprimeAreCoprime (a , b)
[ posneg i   , b ] = (posneg i , 1) , toCoprimeAreCoprime (0 , b)

[]-cancelʳ : ∀ ((a , b) : ℤ × ℕ₊₁) k → [ a · pos (ℕ₊₁→ℕ k) , b ·₊₁ k ] ≡ [ a , b ]
[]-cancelʳ (signed s zero    , b) k =
  Σ≡Prop (λ _ → isPropIsGCD) (λ i → signed-zero spos s i , 1)
[]-cancelʳ (signed s (suc a) , b) k =
  Σ≡Prop (λ _ → isPropIsGCD) (λ i → signedPair (·S-comm s spos i)
                                               (toCoprime-cancelʳ (suc a , b) k i))
[]-cancelʳ (posneg i ,         b) k j =
  isSet→isSet' isSetℚ ([]-cancelʳ (pos zero , b) k) ([]-cancelʳ (neg zero , b) k)
                      (λ i → [ posneg i · pos (ℕ₊₁→ℕ k) , b ·₊₁ k ]) (λ i → [ posneg i , b ]) i j

-- Natural number and negative integer literals for ℚ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℚ : HasFromNat ℚ
  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → (pos n , 1) , oneGCD n }

instance
  fromNegℚ : HasFromNeg ℚ
  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → (neg n , 1) , oneGCD n }

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Equality of terms
module Syntax.Equality where

open import Syntax.Types
open import Syntax.Context
open import Syntax.Terms
open import Syntax.Substitution.Kits
open import Syntax.Substitution.Instances
open import Syntax.Substitution.Lemmas

open Kit 𝒯erm

-- Shorthands for de Bruijn indices
x₁ : ∀{Γ A} -> Γ , A now ⊢ A now
x₁ = var top

x₂ : ∀{Γ A B} -> Γ , A now , B ⊢ A now
x₂ = var (pop top)

x₃ : ∀{Γ A B C} -> Γ , A now , B , C ⊢ A now
x₃ = var (pop (pop top))

x₄ : ∀{Γ A B C D} -> Γ , A now , B , C , D ⊢ A now
x₄ = var (pop (pop (pop top)))

s₁ : ∀{Γ A} -> Γ , A always ⊢ A always
s₁ = var top

s₂ : ∀{Γ A B} -> Γ , A always , B ⊢ A always
s₂ = var (pop top)

s₃ : ∀{Γ A B C} -> Γ , A always , B , C ⊢ A always
s₃ = var (pop (pop top))

s₄ : ∀{Γ A B C D} -> Γ , A always , B , C , D ⊢ A always
s₄ = var (pop (pop (pop top)))

-- β-η equality of terms
data Eq (Γ : Context) : (A : Judgement) -> Γ ⊢ A -> Γ ⊢ A -> Set
data Eq′ (Γ : Context) : (A : Judgement) -> Γ ⊨ A -> Γ ⊨ A -> Set
syntax Eq Γ A M N = Γ ⊢ M ≡ N ∷ A
syntax Eq′ Γ A M N = Γ ⊨ M ≡ N ∷ A

data Eq Γ where
    -- | Equivalence relation
    -- Reflexivity
    refl  : ∀{A}            ->               (M : Γ ⊢ A)
                                           ---------------
                            ->              Γ ⊢ M ≡ M ∷ A

    -- Symmetry
    sym   : ∀{A}{M₁ M₂ : Γ ⊢ A}
                            ->              Γ ⊢ M₁ ≡ M₂ ∷ A
                                           -----------------
                            ->              Γ ⊢ M₂ ≡ M₁ ∷ A

    -- Transitivity
    trans : ∀{A}{M₁ M₂ M₃ : Γ ⊢ A}
                            ->   Γ ⊢ M₁ ≡ M₂ ∷ A   ->   Γ ⊢ M₂ ≡ M₃ ∷ A
                                -----------------------------------------
                            ->               Γ ⊢ M₁ ≡ M₃ ∷ A

    -- | β-equality
    -- β-reduction for function application
    β-lam : ∀{A B}          ->  (N : Γ , A now ⊢ B now)   (M : Γ ⊢ A now)
                               -------------------------------------------
                            ->      Γ ⊢ (lam N) $ M ≡ [ M /] N ∷ B now

    -- β-reduction for first projection

    β-fst : ∀{A B}          ->        (M : Γ ⊢ A now)   (N : Γ ⊢ B now)
                                     -----------------------------------
                            ->          Γ ⊢ fst [ M ,, N ] ≡ M ∷ A now

    -- β-reduction for second projection
    β-snd : ∀{A B}          ->        (M : Γ ⊢ A now)   (N : Γ ⊢ B now)
                                     -----------------------------------
                            ->          Γ ⊢ snd [ M ,, N ] ≡ N ∷ B now

    -- β-reduction for case split on first injection
    β-inl : ∀{A B C}        ->                    (M : Γ ⊢ A now)
                                 (N₁ : Γ , A now ⊢ C now) (N₂ : Γ , B now ⊢ C now)
                                ---------------------------------------------------
                            ->       Γ ⊢ case (inl M) inl↦ N₁
                                                    ||inr↦ N₂ ≡ [ M /] N₁ ∷ C now

    -- β-reduction for case split on first injection
    β-inr : ∀{A B C}        ->                    (M : Γ ⊢ B now)
                                 (N₁ : Γ , A now ⊢ C now) (N₂ : Γ , B now ⊢ C now)
                                ---------------------------------------------------
                            ->       Γ ⊢ case (inr M) inl↦ N₁
                                                    ||inr↦ N₂ ≡ [ M /] N₂ ∷ C now

    -- β-reduction for signal binding
    β-sig : ∀{A B}          ->  (N : Γ , A always ⊢ B now)   (M : Γ ⊢ A always)
                               --------------------------------------------------
                            ->     Γ ⊢ letSig (sig M) In N ≡ [ M /] N ∷ B now

    -- | η-equality
    -- η-expansion for functions
    η-lam : ∀{A B}          ->              (M : Γ ⊢ A => B now)
                                   --------------------------------------
                            ->      Γ ⊢ M ≡ lam (𝓌 M $ x₁) ∷ A => B now

    -- η-expansion for pairs
    η-pair : ∀{A B}         ->               (M : Γ ⊢ A & B now)
                                   ----------------------------------------
                            ->      Γ ⊢ M ≡ [ fst M ,, snd M ] ∷ A & B now

    -- η-expansion for unit
    η-unit :                                 (M : Γ ⊢ Unit now)
                                          -------------------------
                            ->             Γ ⊢ M ≡ unit ∷ Unit now

    -- η-expansion for sums
    η-sum : ∀{A B}          ->                (M : Γ ⊢ A + B now)
                                    ------------------------------------------
                            ->        Γ ⊢ M ≡ case M inl↦ inl x₁
                                                   ||inr↦ inr x₁ ∷ A + B now

    -- η-expansion for signals
    η-sig : ∀{A}            ->                (M : Γ ⊢ Signal A now)
                                    -------------------------------------------
                            ->       Γ ⊢ M ≡ letSig M In (sig s₁) ∷ Signal A now

    -- η-expansion for events in computational terms
    η-evt : ∀{A}           ->                  (M : Γ ⊢ Event A now)
                                  ----------------------------------------------------
                            ->     Γ ⊢ M ≡ event (letEvt M In pure x₁) ∷ Event A now

    -- | Congruence rules
    -- Congruence in pairs
    cong-pair : ∀{A B}{M₁ M₂ : Γ ⊢ A now}{N₁ N₂ : Γ ⊢ B now}
                            ->   Γ ⊢ M₁ ≡ M₂ ∷ A now  ->   Γ ⊢ N₁ ≡ N₂ ∷ B now
                                ------------------------------------------------
                            ->    Γ ⊢ [ M₁ ,, N₁ ] ≡ [ M₂ ,, N₂ ] ∷ A & B now

    -- Congruence in first projection
    cong-fst : ∀{A B}{M₁ M₂ : Γ ⊢ A & B now}
                            ->             Γ ⊢ M₁ ≡ M₂ ∷ A & B now
                                        ------------------------------
                            ->           Γ ⊢ fst M₁ ≡ fst M₂ ∷ A now

    -- Congruence in second projection
    cong-snd : ∀{A B}{M₁ M₂ : Γ ⊢ A & B now}
                            ->             Γ ⊢ M₁ ≡ M₂ ∷ A & B now
                                        ------------------------------
                            ->           Γ ⊢ snd M₁ ≡ snd M₂ ∷ B now

    -- Congruence in lambda body
    cong-lam : ∀{A B}{M₁ M₂ : Γ , A now ⊢ B now}
                            ->            Γ , A now ⊢ M₁ ≡ M₂ ∷ B now
                                       ----------------------------------
                            ->          Γ ⊢ lam M₁ ≡ lam M₂ ∷ A => B now

    -- Congruence in application
    cong-app : ∀{A B}{N₁ N₂ : Γ ⊢ A => B now}{M₁ M₂ : Γ ⊢ A now}
                            ->   Γ ⊢ N₁ ≡ N₂ ∷ A => B now  ->  Γ ⊢ M₁ ≡ M₂ ∷ A now
                                ---------------------------------------------------
                            ->            Γ ⊢ N₁ $ M₁ ≡ N₂ $ M₂ ∷ B now

    -- Congruence in case split
    cong-case : ∀{A B C}{M₁ M₂ : Γ ⊢ A + B now}
                            ->               Γ ⊢ M₁ ≡ M₂ ∷ A + B now
                            ->   (N₁ : Γ , A now ⊢ C now) (N₂ : Γ , B now ⊢ C now)
                                ---------------------------------------------------
                            ->          Γ ⊢ case M₁ inl↦ N₁ ||inr↦ N₂
                                          ≡ case M₂ inl↦ N₁ ||inr↦ N₂ ∷ C now

    -- Congruence in first injection
    cong-inl : ∀{A B}{M₁ M₂ : Γ ⊢ A now}
                            ->              Γ ⊢ M₁ ≡ M₂ ∷ A now
                                      ------------------------------------
                            ->         Γ ⊢ inl M₁ ≡ inl M₂ ∷ A + B now

    -- Congruence in second injection
    cong-inr : ∀{A B}{M₁ M₂ : Γ ⊢ B now}
                            ->              Γ ⊢ M₁ ≡ M₂ ∷ B now
                                      ------------------------------------
                            ->         Γ ⊢ inr M₁ ≡ inr M₂ ∷ A + B now

    -- Congruence in signal constructor
    cong-sig : ∀{A}{M₁ M₂ : Γ ⊢ A always}
                            ->              Γ ⊢ M₁ ≡ M₂ ∷ A always
                                      ------------------------------------
                            ->         Γ ⊢ sig M₁ ≡ sig M₂ ∷ Signal A now

    -- Congruence in signal binding
    cong-letSig : ∀{A B}{S₁ S₂ : Γ ⊢ Signal A now}
                            ->          Γ ⊢ S₁ ≡ S₂ ∷ Signal A now
                            ->          (N : Γ , A always ⊢ B now)
                                ---------------------------------------------
                            ->   Γ ⊢ letSig S₁ In N ≡ letSig S₂ In N ∷ B now

    -- Congruence in sampling
    cong-sample : ∀{A}{M₁ M₂ : Γ ⊢ A always}
                            ->              Γ ⊢ M₁ ≡ M₂ ∷ A always
                                      -------------------------------------
                            ->         Γ ⊢ sample M₁ ≡ sample M₂ ∷ A now

    -- Congruence in stabilisation
    cong-stable : ∀{A}{M₁ M₂ : Γ ˢ ⊢ A now}
                            ->                 Γ ˢ ⊢ M₁ ≡ M₂ ∷ A now
                                      -------------------------------------
                            ->         Γ ⊢ stable M₁ ≡ stable M₂ ∷ A always

    -- Congruence in events
    cong-event : ∀{A}{E₁ E₂ : Γ ⊨ A now}
                            ->                 Γ ⊨ E₁ ≡ E₂ ∷ A now
                                      -------------------------------------
                            ->         Γ ⊢ event E₁ ≡ event E₂ ∷ Event A now

data Eq′ (Γ : Context) where
    -- | Equivalence relation
    -- Reflexivity
    refl  : ∀{A}            ->                (M : Γ ⊨ A)
                                            ---------------
                            ->               Γ ⊨ M ≡ M ∷ A

    -- Symmetry
    sym   : ∀{A}{M₁ M₂ : Γ ⊨ A}
                            ->              Γ ⊨ M₁ ≡ M₂ ∷ A
                                           -----------------
                            ->              Γ ⊨ M₂ ≡ M₁ ∷ A

    -- Transitivity
    trans : ∀{A}{M₁ M₂ M₃ : Γ ⊨ A}
                            ->   Γ ⊨ M₁ ≡ M₂ ∷ A   ->   Γ ⊨ M₂ ≡ M₃ ∷ A
                                -----------------------------------------
                            ->               Γ ⊨ M₁ ≡ M₃ ∷ A

    -- | β-equality
    -- β-reduction for signal binding in computational terms
    β-sig′ : ∀{A B}         ->  (C : Γ , A always ⊨ B now)   (M : Γ ⊢ A always)
                               --------------------------------------------------
                            ->     Γ ⊨ letSig (sig M) InC C ≡ [ M /′] C ∷ B now

    -- β-reduction for event binding in computational terms
    β-evt′ : ∀{A B}         ->     (C : Γ ˢ , A now ⊨ B now)   (D : Γ ⊨ A now)
                                 ---------------------------------------------
                            ->    Γ ⊨ letEvt (event D) In C ≡ ⟨ D /⟩ C ∷ B now

    -- β-reduction for event binding in computational terms
    β-selectₚ : ∀{A B C}    ->      (C₁ : Γ ˢ , A now , Event B now ⊨ C now)
                                    (C₂ : Γ ˢ , Event A now , B now ⊨ C now)
                                       (C₃ : Γ ˢ , A now , B now ⊨ C now)
                                      (M₁ : Γ ⊢ A now)   (M₂ : Γ ⊢ B now)
                                 ---------------------------------------------
                            ->    Γ ⊨ select event (pure M₁) ↦ C₁
                                          || event (pure M₂) ↦ C₂
                                          ||both↦ C₃
                                    ≡ [ M₁ /′] ([ 𝓌 M₂ /′]
                                        (weakening′ (keep (keep (Γˢ⊆Γ Γ))) C₃)) ∷ C now

    -- | η-equality
    -- η-expansion for signals in computational terms
    η-sig′ : ∀{A}           ->                  (M : Γ ⊢ Signal A now)
                               --------------------------------------------------------
                            ->  Γ ⊨ pure M ≡ letSig M InC (pure (sig s₁)) ∷ Signal A now

    -- | Congruence rules
    -- Congruence in pure computational term
    cong-pure′ : ∀{A}{M₁ M₂ : Γ ⊢ A}
                            ->                Γ ⊢ M₁ ≡ M₂ ∷ A
                                         ---------------------------
                            ->            Γ ⊨ pure M₁ ≡ pure M₂ ∷ A

    -- Congruence in signal binding
    cong-letSig′ : ∀{A B}{S₁ S₂ : Γ ⊢ Signal A now}
                            ->            Γ ⊢ S₁ ≡ S₂ ∷ Signal A now
                            ->            (N : Γ , A always ⊨ B now)
                                -----------------------------------------------
                            ->   Γ ⊨ letSig S₁ InC N ≡ letSig S₂ InC N ∷ B now

    -- Congruence in event binding
    cong-letEvt′ : ∀{A B}{E₁ E₂ : Γ ⊢ Event A now}
                            ->            Γ ⊢ E₁ ≡ E₂ ∷ Event A now
                            ->            (D : Γ ˢ , A now ⊨ B now)
                                -----------------------------------------------
                            ->   Γ ⊨ letEvt E₁ In D ≡ letEvt E₂ In D ∷ B now

test : ∀{A} -> ∙ ⊢ (Signal A => A) now
test = lam (letSig x₁ In sample s₁)

tes : ∀{A} -> ∙ ⊢ (Signal A => Signal (Signal A)) now
tes = lam (letSig x₁ In sig (stable (sig s₁)))

te : ∀{A} -> ∙ ⊢ (A => Event A) now
te = lam (event (pure x₁))

t2 : ∀{A} -> ∙ ⊢ (Signal A) now -> ∙ ⊢ A always
t2 M = stable (letSig M In sample s₁)

t : ∀{A} -> ∙ ⊢ (Event (Event A) => Event A) now
t = lam (event (letEvt x₁ In (letEvt x₁ In pure x₁)))

t3 : ∀{A B} -> ∙ ⊢ (Event A => Signal (A => Event B) => Event B) now
t3 = lam (lam
        (letSig x₁ In (event
        (letEvt x₃ In
        (letEvt (sample s₂ $ x₁) In pure x₁)))))

-- t4 : ∀{A B C} -> ∙ ⊢ (Event A => Event B => Signal (A => Event C) => Signal (B => Event C) => Event C) now
-- t4 = lam (lam (lam (lam (
--         letSig x₂ In (
--         letSig x₂ In (event (
--             select (var (pop (pop (pop (pop (pop top)))))) ↦ letEvt sample s₄ $ x₁ In pure x₁
--                 || (var (pop (pop (pop (pop top))))) ↦ letEvt (sample s₃ $ x₁) In pure x₁
--                 ||both↦ {!   !})))))))

t5 : ∀{A B} -> ∙ , Signal A now , Event (A => B) now ⊨ B now
t5 = letSig (var (pop top)) InC (letEvt (var (pop top)) In pure (x₁ $ sample s₂))

t6 : ∀{A B} -> ∙ , Event (Signal A) now , Signal B now ⊢ Event (Signal (A & B)) now
t6 = event (letSig x₁ InC (letEvt x₃ In (pure (letSig x₁ In (sig (stable [ sample s₁ ,, sample s₂ ]))))))
-- t6 = event (letSig x₁ InC (letEvt x₃ In (letSig x₁ InC (pure [ sample s₁ ,, sample s₃ ]))))

too : ∀{A B} -> ∙ ⊢ Signal (A => B) => (Event A => Event B) now
too = lam (lam (letSig x₂ In event (letEvt x₂ In pure (sample s₂ $ x₁))))

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module All where

open import Basics
open import Ix

All : {X : Set} -> (X -> Set) -> (List X -> Set)
All P []        = One
All P (x ,- xs) = P x * All P xs

allPu : forall {X}{T : X -> Set} -> [ T ] -> [ All T ]
allPu t [] = <>
allPu t (x ,- xs) = t x , allPu t xs

allAp : forall {X}{S T : X -> Set} -> [ All (S -:> T) -:> All S -:> All T ]
allAp [] <> <> = <>
allAp (x ,- xs) (f , fs) (s , ss) = f s , allAp xs fs ss

all : {X : Set}{S T : X -> Set} ->
      [ S -:> T ] -> [ All S -:> All T ]
all f xs = allAp xs (allPu f xs)

allRe : forall {X Y}(f : X -> Y){P : Y -> Set}
        (xs : List X) -> All (\ x -> P (f x)) xs -> All P (list f xs)
allRe f [] <> = <>
allRe f (x ,- xs) (p , ps) = p , allRe f xs ps

collect : {I J : Set}(is : List I) -> All (\ i -> List J) is -> List J
collect [] <> = []
collect (i ,- is) (js , jss) = js +L collect is jss

max_stars_repo_name: pigworker/InteriorDesign

max_issues_repo_name: pigworker/InteriorDesign

max_forks_repo_name: pigworker/InteriorDesign


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

module Evaluator where

open import Agda.Prim
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

open import Paths

------------------------------------------------------------------------------
-- For the usual situation, we can only establish one direction of univalence

swap₊ : {ℓ : Level} {A B : Set ℓ} → A ⊎ B → B ⊎ A
swap₊ (inj₁ a) = inj₂ a
swap₊ (inj₂ b) = inj₁ b

assocl₊ : {ℓ : Level} {A B C : Set ℓ} → A ⊎ (B ⊎ C) → (A ⊎ B) ⊎ C
assocl₊ (inj₁ a) = inj₁ (inj₁ a)
assocl₊ (inj₂ (inj₁ b)) = inj₁ (inj₂ b)
assocl₊ (inj₂ (inj₂ c)) = inj₂ c

assocr₊ : {ℓ : Level} {A B C : Set ℓ} → (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
assocr₊ (inj₁ (inj₁ a)) = inj₁ a
assocr₊ (inj₁ (inj₂ b)) = inj₂ (inj₁ b)
assocr₊ (inj₂ c) = inj₂ (inj₂ c)

unite⋆ : {ℓ : Level} {A : Set ℓ} → ⊤ × A → A
unite⋆ (tt , a) = a

uniti⋆ : {ℓ : Level} {A : Set ℓ} → A → ⊤ × A
uniti⋆ a = (tt , a)

swap⋆ : {ℓ : Level} {A B : Set ℓ} → A × B → B × A
swap⋆ (a , b) = (b , a)

assocl⋆ : {ℓ : Level} {A B C : Set ℓ} → A × (B × C) → (A × B) × C
assocl⋆ (a , (b , c)) = ((a , b) , c)

assocr⋆ : {ℓ : Level} {A B C : Set ℓ} → (A × B) × C → A × (B × C)
assocr⋆ ((a , b) , c) = (a , (b , c))

dist : {ℓ : Level} {A B C : Set ℓ} → (A ⊎ B) × C → (A × C ⊎ B × C)
dist (inj₁ a , c) = inj₁ (a , c)
dist (inj₂ b , c) = inj₂ (b , c)

fact : {ℓ : Level} {A B C : Set ℓ} → (A × C ⊎ B × C) → (A ⊎ B) × C
fact (inj₁ (a , c)) = (inj₁ a , c)
fact (inj₂ (b , c)) = (inj₂ b , c)

eval : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} → Path a b → (A → B)
eval swap₁₊⇛              = swap₊
eval swap₂₊⇛              = swap₊
eval assocl₁₊⇛            = assocl₊
eval assocl₁₊⇛'           = assocl₊
{-- eval (assocl₂₁₊⇛ _)        = assocl₊
eval (assocl₂₂₊⇛ _)        = assocl₊
eval (assocr₁₁₊⇛ _)        = assocr₊
eval (assocr₁₂₊⇛ _)        = assocr₊
eval (assocr₂₊⇛ _)         = assocr₊
eval (unite⋆⇛ _)           = unite⋆
eval (uniti⋆⇛ _)           = uniti⋆
eval (swap⋆⇛ _ _)          = swap⋆
eval (assocl⋆⇛ _ _ _)      = assocl⋆
eval (assocr⋆⇛ _ _ _)      = assocr⋆
eval (dist₁⇛ _ _)          = dist
eval (dist₂⇛ _ _)          = dist
eval (factor₁⇛ _ _)        = fact
eval (factor₂⇛ _ _)        = fact
eval (id⇛ _)               = id
eval (trans⇛ c d)          = eval d ∘ eval c
eval (plus₁⇛ c d)          = Data.Sum.map (eval c) (eval d)
eval (plus₂⇛ c d)          = Data.Sum.map (eval c) (eval d)
eval (times⇛ c d)          = Data.Product.map (eval c) (eval d)
--}
-- Inverses

evalB : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} → Path a b → (B → A)
evalB swap₂₊⇛              = swap₊
evalB swap₁₊⇛          = swap₊
evalB assocl₁₊⇛        = assocr₊
evalB assocl₁₊⇛'        = assocr₊
{-- evalB (assocr₂₊⇛ _)        = assocl₊
evalB (assocr₁₂₊⇛ _)       = assocl₊
evalB (assocr₁₁₊⇛ _)       = assocl₊
evalB (assocl₂₂₊⇛ _)       = assocr₊
evalB (assocl₂₁₊⇛ _)       = assocr₊
evalB (uniti⋆⇛ _)          = unite⋆
evalB (unite⋆⇛ _)          = uniti⋆
evalB (swap⋆⇛ _ _)         = swap⋆
evalB (assocr⋆⇛ _ _ _)     = assocl⋆
evalB (assocl⋆⇛ _ _ _)     = assocr⋆
evalB (dist₁⇛ _ _)         = fact
evalB (dist₂⇛ _ _)         = fact
evalB (factor₁⇛ _ _)       = dist
evalB (factor₂⇛ _ _)       = dist
evalB (id⇛ _)              = id
evalB (trans⇛ c d)         = evalB c ∘ evalB d
evalB (plus₁⇛ c d)         = Data.Sum.map (evalB c) (evalB d)
evalB (plus₂⇛ c d)         = Data.Sum.map (evalB c) (evalB d)
evalB (times⇛ c d)         = Data.Product.map (evalB c) (evalB d)
--}

------------------------------------------------------------------------------
-- Proving univalence•

eval-resp-• : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} →
              (c : Path a b) → eval c a ≡ b
eval-resp-• swap₁₊⇛ = refl
eval-resp-• swap₂₊⇛ = refl
eval-resp-• assocl₁₊⇛ = refl
eval-resp-• assocl₁₊⇛' = refl
{-- eval-resp-• (assocl₂₁₊⇛ b) = refl
eval-resp-• (assocl₂₂₊⇛ c) = refl
eval-resp-• (assocr₁₁₊⇛ a) = refl
eval-resp-• (assocr₁₂₊⇛ b) = refl
eval-resp-• (assocr₂₊⇛ c) = refl
eval-resp-• {b = b} (unite⋆⇛ .b) = refl
eval-resp-• {a = a} (uniti⋆⇛ .a) = refl
eval-resp-• (swap⋆⇛ a b) = refl
eval-resp-• (assocl⋆⇛ a b c) = refl
eval-resp-• (assocr⋆⇛ a b c) = refl
eval-resp-• (dist₁⇛ a c) = refl
eval-resp-• (dist₂⇛ b c) = refl
eval-resp-• (factor₁⇛ a c) = refl
eval-resp-• (factor₂⇛ b c) = refl
eval-resp-• {a = a} (id⇛ .a) = refl
eval-resp-• {a = a} (trans⇛ c d) rewrite eval-resp-• c | eval-resp-• d = refl
eval-resp-• (plus₁⇛ c d) rewrite eval-resp-• c = refl
eval-resp-• (plus₂⇛ c d) rewrite eval-resp-• d = refl
eval-resp-• (times⇛ c d) rewrite eval-resp-• c | eval-resp-• d = refl
--}
evalB-resp-• : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} →
              (c : Path a b) → evalB c b ≡ a
evalB-resp-• swap₁₊⇛ = refl
evalB-resp-• swap₂₊⇛ = refl
evalB-resp-• assocl₁₊⇛ = refl
evalB-resp-• assocl₁₊⇛' = refl
{-- evalB-resp-• (assocl₂₁₊⇛ b) = refl
evalB-resp-• (assocl₂₂₊⇛ c) = refl
evalB-resp-• (assocr₁₁₊⇛ a) = refl
evalB-resp-• (assocr₁₂₊⇛ b) = refl
evalB-resp-• (assocr₂₊⇛ c) = refl
evalB-resp-• {b = b} (unite⋆⇛ .b) = refl
evalB-resp-• {a = a} (uniti⋆⇛ .a) = refl
evalB-resp-• (swap⋆⇛ a b) = refl
evalB-resp-• (assocl⋆⇛ a b c) = refl
evalB-resp-• (assocr⋆⇛ a b c) = refl
evalB-resp-• (dist₁⇛ a c) = refl
evalB-resp-• (dist₂⇛ b c) = refl
evalB-resp-• (factor₁⇛ a c) = refl
evalB-resp-• (factor₂⇛ b c) = refl
evalB-resp-• {a = a} (id⇛ .a) = refl
evalB-resp-• {a = a} (trans⇛ c d) rewrite evalB-resp-• d | evalB-resp-• c = refl
evalB-resp-• (plus₁⇛ c d) rewrite evalB-resp-• c = refl
evalB-resp-• (plus₂⇛ c d) rewrite evalB-resp-• d = refl
evalB-resp-• (times⇛ c d) rewrite evalB-resp-• c | evalB-resp-• d = refl
--}
-- the proof that eval ∙ evalB x ≡ x will be useful below
eval∘evalB≡id :  {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} →
  (c : Path a b) → evalB c (eval c a) ≡ a
eval∘evalB≡id c rewrite eval-resp-• c | evalB-resp-• c = refl

{--
-- if this is useful, move it elsewhere
-- but it might not be, as it appears to be 'level raising'
cong⇚ : {ℓ : Level} {A B : Set ℓ} {a₁ a₂ : A}
       (f : Path a₁ a₂ ) → (x : A) → Path (evalB f x) (evalB f x)
cong⇚ f x = id⇛ (evalB f x)
--}

{--
eval∘evalB :  {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} →
  (c : Path a b) → (x : A) → Path (evalB c (eval c x)) x
eval∘evalB (swap₁₊⇛ a) (inj₁ x) = id⇛ (inj₁ x)
eval∘evalB (swap₁₊⇛ a) (inj₂ y) = id⇛ (inj₂ y)
eval∘evalB (swap₂₊⇛ b) (inj₁ x) = id⇛ (inj₁ x)
eval∘evalB (swap₂₊⇛ b) (inj₂ y) = id⇛ (inj₂ y)
eval∘evalB (assocl₁₊⇛ a) (inj₁ x) = id⇛ (inj₁ x)
eval∘evalB (assocl₁₊⇛ a) (inj₂ (inj₁ x)) = id⇛ (inj₂ (inj₁ x))
eval∘evalB (assocl₁₊⇛ a) (inj₂ (inj₂ y)) = id⇛ (inj₂ (inj₂ y))
eval∘evalB (assocl₂₁₊⇛ b) (inj₁ x) = id⇛ (inj₁ x)
eval∘evalB (assocl₂₁₊⇛ b) (inj₂ (inj₁ x)) = id⇛ (inj₂ (inj₁ x))
eval∘evalB (assocl₂₁₊⇛ b) (inj₂ (inj₂ y)) = id⇛ (inj₂ (inj₂ y))
eval∘evalB (assocl₂₂₊⇛ c) (inj₁ x) = id⇛ (inj₁ x)
eval∘evalB (assocl₂₂₊⇛ c) (inj₂ (inj₁ x)) = id⇛ (inj₂ (inj₁ x))
eval∘evalB (assocl₂₂₊⇛ c) (inj₂ (inj₂ y)) = id⇛ (inj₂ (inj₂ y))
eval∘evalB (assocr₁₁₊⇛ a) (inj₁ (inj₁ x)) = id⇛ (inj₁ (inj₁ x))
eval∘evalB (assocr₁₁₊⇛ a) (inj₁ (inj₂ y)) = id⇛ (inj₁ (inj₂ y))
eval∘evalB (assocr₁₁₊⇛ a) (inj₂ y) = id⇛ (inj₂ y)
eval∘evalB (assocr₁₂₊⇛ b) (inj₁ (inj₁ x)) = id⇛ (inj₁ (inj₁ x))
eval∘evalB (assocr₁₂₊⇛ b) (inj₁ (inj₂ y)) = id⇛ (inj₁ (inj₂ y))
eval∘evalB (assocr₁₂₊⇛ b) (inj₂ y) = id⇛ (inj₂ y)
eval∘evalB (assocr₂₊⇛ c) (inj₁ (inj₁ x)) = id⇛ (inj₁ (inj₁ x))
eval∘evalB (assocr₂₊⇛ c) (inj₁ (inj₂ y)) = id⇛ (inj₁ (inj₂ y))
eval∘evalB (assocr₂₊⇛ c) (inj₂ y) = id⇛ (inj₂ y)
eval∘evalB {b = b} (unite⋆⇛ .b) (tt , x) = id⇛ (tt , x)
eval∘evalB {a = a} (uniti⋆⇛ .a) x = id⇛ x
eval∘evalB (swap⋆⇛ a b) (x , y) = id⇛ (x , y)
eval∘evalB (assocl⋆⇛ a b c) (x , y , z) = id⇛ (x , y , z)
eval∘evalB (assocr⋆⇛ a b c) ((x , y) , z) = id⇛ ((x , y) , z)
eval∘evalB (dist₁⇛ a c) (inj₁ x , y) = id⇛ (inj₁ x , y)
eval∘evalB (dist₁⇛ a c) (inj₂ y , z) = id⇛ (inj₂ y , z)
eval∘evalB (dist₂⇛ b c) (inj₁ x , z) = id⇛ (inj₁ x , z)
eval∘evalB (dist₂⇛ b c) (inj₂ y , z) = id⇛ (inj₂ y , z)
eval∘evalB (factor₁⇛ a c) (inj₁ (x , y)) = id⇛ (inj₁ (x , y))
eval∘evalB (factor₁⇛ a c) (inj₂ (x , y)) = id⇛ (inj₂ (x , y))
eval∘evalB (factor₂⇛ b c) (inj₁ (x , y)) = id⇛ (inj₁ (x , y))
eval∘evalB (factor₂⇛ b c) (inj₂ (x , y)) = id⇛ (inj₂ (x , y))
eval∘evalB {a = a} (id⇛ .a) x = id⇛ x
eval∘evalB (trans⇛ {A = A} {B} {C} {a} {b} {c} c₁ c₂) x = trans⇛ {!cong⇚ ? (id⇛ (eval c₁ x))!} (eval∘evalB c₁ x)
eval∘evalB (plus₁⇛ {b = b} c₁ c₂) (inj₁ x) = plus₁⇛ (eval∘evalB c₁ x) (id⇛ b)
eval∘evalB (plus₁⇛ {a = a} c₁ c₂) (inj₂ y) = plus₂⇛ (id⇛ a) (eval∘evalB c₂ y)
eval∘evalB (plus₂⇛ {b = b} c₁ c₂) (inj₁ x) = plus₁⇛ (eval∘evalB c₁ x) (id⇛ b)
eval∘evalB (plus₂⇛ {a = a} c₁ c₂) (inj₂ y) = plus₂⇛ (id⇛ a) (eval∘evalB c₂ y)
eval∘evalB (times⇛ c₁ c₂) (x , y) = times⇛ (eval∘evalB c₁ x) (eval∘evalB c₂ y)
--}

{--
eval-gives-id⇛ : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} →
  (c : Path a b) → Path (eval c a) b
eval-gives-id⇛ {b = b} c rewrite eval-resp-• c = id⇛ b
--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Prelude
open import core
open import contexts

module synth-unicity where
  -- synthesis only produces equal types. note that there is no need for an
  -- analagous theorem for analytic positions because we think of
  -- the type as an input
  synthunicity : {Γ : tctx} {e : hexp} {t t' : htyp} →
                  (Γ ⊢ e => t)
                → (Γ ⊢ e => t')
                → t == t'
  synthunicity (SAsc _) (SAsc _) = refl
  synthunicity {Γ = G} (SVar in1) (SVar in2) = ctxunicity {Γ = G} in1 in2
  synthunicity (SAp _  D1 MAHole _) (SAp _ D2 MAHole y) = refl
  synthunicity (SAp _ D1 MAHole _) (SAp _ D2 MAArr y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp _ D1 MAArr _) (SAp _ D2 MAHole y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp _ D1 MAArr _) (SAp _ D2 MAArr y) with synthunicity D1 D2
  ... | refl = refl
  synthunicity SEHole SEHole = refl
  synthunicity (SNEHole _ _) (SNEHole _ _) = refl
  synthunicity SConst SConst = refl
  synthunicity (SLam _ D1) (SLam _ D2) with synthunicity D1 D2
  synthunicity (SLam x₁ D1) (SLam x₂ D2) | refl = refl

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

module Cubical.HITs.MappingCones where

open import Cubical.HITs.MappingCones.Base public
open import Cubical.HITs.MappingCones.Properties public


text:
module Web.Semantic.DL.Signature where

infixr 4 _,_

data Signature : Set₁ where
  _,_ : (CN RN : Set) → Signature

CN : Signature → Set
CN (CN , RN) = CN

RN : Signature → Set
RN (CN , RN) = RN

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

open import HoTT
open import cohomology.Exactness
open import cohomology.FunctionOver
open import cohomology.ProductRepr
open import cohomology.Theory
open import cohomology.WedgeCofiber

{- For the cohomology group of a suspension ΣX, the group inverse has the
 - explicit form Cⁿ(flip-susp) : Cⁿ(ΣX) → Cⁿ(ΣX).
 -}

module cohomology.InverseInSusp {i} (CT : CohomologyTheory i)
  (n : ℤ) {X : Ptd i} where

open CohomologyTheory CT
open import cohomology.Functor CT
open import cohomology.BaseIndependence CT
open import cohomology.Wedge CT

private
  module CW = CWedge n (⊙Susp X) (⊙Susp X)

  module Subtract = SuspensionRec (fst X) {C = fst (⊙Susp X ⊙∨ ⊙Susp X)}
    (winl (south _))
    (winr (south _))
    (λ x → ap winl (! (merid _ x)) ∙ wglue ∙ ap winr (merid _ x))

  subtract = Subtract.f

  ⊙subtract : fst (⊙Susp X ⊙→ ⊙Susp X ⊙∨ ⊙Susp X)
  ⊙subtract = (subtract , ! (ap winl (merid _ (snd X))))

  projl-subtract : ∀ σ → projl _ _ (subtract σ) == flip-susp σ
  projl-subtract = Suspension-elim (fst X) idp idp $
    ↓-='-from-square ∘ vert-degen-square ∘ λ x →
      ap-∘ (projl _ _) subtract (merid _ x)
      ∙ ap (ap (projl _ _)) (Subtract.glue-β x)
      ∙ ap-∙ (projl _ _) (ap winl (! (merid _ x))) (wglue ∙ ap winr (merid _ x))
      ∙ ((∘-ap (projl _ _) winl (! (merid _ x))
          ∙ ap-idf _)
         ∙2 (ap-∙ (projl _ _) wglue (ap winr (merid _ x))
             ∙ (Projl.glue-β _ _
                ∙2 (∘-ap (projl _ _) winr (merid _ x) ∙ ap-cst _ _))))
      ∙ ∙-unit-r _
      ∙ ! (FlipSusp.glue-β x)

  projr-subtract : ∀ σ → projr _ _ (subtract σ) == σ
  projr-subtract = Suspension-elim (fst X) idp idp $
    ↓-∘=idf-in (projr _ _) subtract ∘ λ x →
      ap (ap (projr _ _)) (Subtract.glue-β x)
      ∙ ap-∙ (projr _ _) (ap winl (! (merid _ x))) (wglue ∙ ap winr (merid _ x))
      ∙ ((∘-ap (projr _ _) winl (! (merid _ x)) ∙ ap-cst _ _)
         ∙2 (ap-∙ (projr _ _) wglue (ap winr (merid _ x))
             ∙ (Projr.glue-β _ _
                ∙2 (∘-ap (projr _ _) winr (merid _ x) ∙ ap-idf _))))

  fold-subtract : ∀ σ → fold (subtract σ) == south _
  fold-subtract = Suspension-elim (fst X) idp idp $
    ↓-app=cst-in ∘ ! ∘ λ x →
      ∙-unit-r _
      ∙ ap-∘ fold subtract (merid _ x)
      ∙ ap (ap fold) (Subtract.glue-β x)
      ∙ ap-∙ fold (ap winl (! (merid _ x))) (wglue ∙ ap winr (merid _ x))
      ∙ ((∘-ap fold winl (! (merid _ x)) ∙ ap-idf _)
         ∙2 (ap-∙ fold wglue (ap winr (merid _ x))
             ∙ (Fold.glue-β
                ∙2 (∘-ap fold winr (merid _ x) ∙ ap-idf _))))
      ∙ !-inv-l (merid _ x)

  cancel :
    ×ᴳ-sum-hom (C-abelian n _) (CF-hom n (⊙flip-susp X)) (idhom _) ∘ᴳ ×ᴳ-diag
    == cst-hom
  cancel =
    ap2 (λ φ ψ → ×ᴳ-sum-hom (C-abelian n _) φ ψ ∘ᴳ ×ᴳ-diag)
        (! (CF-λ= n projl-subtract))
        (! (CF-ident n) ∙ ! (CF-λ= n projr-subtract))
    ∙ transport (λ {(G , φ , ψ) → φ ∘ᴳ ψ == cst-hom})
        (pair= (CW.path) $ ↓-×-in
          (CW.wedge-in-over ⊙subtract)
          (CW.⊙wedge-rec-over (⊙idf _) (⊙idf _)
           ▹ ap2 ×ᴳ-hom-in (CF-ident n) (CF-ident n)))
        (! (CF-comp n ⊙fold ⊙subtract)
         ∙ CF-λ= n (λ σ → fold-subtract σ ∙ ! (merid _ (snd X)))
         ∙ CF-cst n)

C-flip-susp-is-inv :
  CF-hom n (⊙flip-susp X) == inv-hom (C n (⊙Susp X)) (C-abelian _ _)
C-flip-susp-is-inv = hom= _ _ $ λ= $ λ g →
  ! (group-inv-unique-l (C n (⊙Susp X)) _ g (app= (ap GroupHom.f cancel) g))

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

pattern vArg x = arg (arg-info visible relevant) x
pattern hArg x = arg (arg-info hidden  relevant) x

idClause-ok : Clause
idClause-ok = clause
             (("A" , hArg (agda-sort (lit 0))) ∷ ("x" , vArg (var 0 [])) ∷ [])
             (hArg (var 1) ∷ vArg (var 0) ∷ [])
             (var 0 [])

id-ok : {A : Set} → A → A
unquoteDef id-ok = defineFun id-ok (idClause-ok ∷ [])

idClause-fail : Clause
idClause-fail = clause
             (("A" , hArg (agda-sort (lit 0))) ∷ ("x" , vArg (var 0 [])) ∷ [])
             ({-hArg (var 1) ∷-} vArg (var 0) ∷ [])
             (var 0 [])

id-fail : {A : Set} → A → A
unquoteDef id-fail = defineFun id-fail (idClause-fail ∷ [])
-- Panic: unbound variable A (id: 191@9559440724209987811)
-- when checking that the expression A has type _7

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
module L.Base.Empty.Properties where

-- There are no properties yet.

max_stars_repo_name: borszag/smallib

max_issues_repo_name: borszag/smallib

max_forks_repo_name: borszag/smallib


text:
------------------------------------------------------------------------------
-- Reasoning about a function without a termination proof
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Collatz.CollatzSL where

open import Data.Bool.Base
open import Data.Empty
open import Data.Nat renaming ( suc to succ )
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary

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

isEven : ℕ → Bool
isEven 0               = true
isEven 1               = false
isEven (succ (succ n)) = isEven n

{-# TERMINATING #-}
collatz : ℕ → ℕ
collatz zero        = 1
collatz (succ zero) = 1
{-# CATCHALL #-}
collatz n with isEven n
... | true  = collatz ⌊ n /2⌋
... | false = collatz (3 * n + 1)

-- 25 April 2014: Failed with Andreas' --without-K.
xy≡0→x≡0∨y≡0 : (m n : ℕ) → m * n ≡ zero → m ≡ zero ⊎ n ≡ zero
xy≡0→x≡0∨y≡0 zero     n        h = inj₁ refl
xy≡0→x≡0∨y≡0 (succ m) zero     h = inj₂ refl
xy≡0→x≡0∨y≡0 (succ m) (succ n) ()

+∸2 : ∀ {n} → n ≢ zero → n ≢ 1 → n ≡ succ (succ (n ∸ 2))
+∸2 {zero}          0≢0 _   = ⊥-elim (0≢0 refl)
+∸2 {succ zero}     _   1≢1 = ⊥-elim (1≢1 refl)
+∸2 {succ (succ n)} _   _   = refl

2^x≢0 : (n : ℕ) → 2 ^ n ≢ zero
2^x≢0 zero ()
2^x≢0 (succ n) h = [ (λ ())
                   , (λ 2^n≡0 → ⊥-elim (2^x≢0 n 2^n≡0))
                   ]′ (xy≡0→x≡0∨y≡0 2 (2 ^ n) h)

2^[x+1]/2≡2^x : ∀ n → ⌊ 2 ^ succ n /2⌋ ≡ 2 ^ n
2^[x+1]/2≡2^x zero            = refl
2^[x+1]/2≡2^x (succ zero)     = refl
2^[x+1]/2≡2^x (succ (succ n)) = {!!}

collatz-2^x : ∀ n → Σ ℕ (λ k → n ≡ 2 ^ k) → collatz n ≡ 1
collatz-2^x zero     h                = refl
collatz-2^x (succ n) (zero , proj₂)   = subst (λ t → collatz t ≡ 1) (sym proj₂) refl
collatz-2^x (succ n) (succ k , proj₂) = subst (λ t → collatz t ≡ 1) (sym proj₂) {!!}

succInjective : ∀ {m n} → succ m ≡ succ n → m ≡ n
succInjective refl = refl

Sx≡x→⊥ : ∀ n → succ n ≢ n
Sx≡x→⊥ zero ()
Sx≡x→⊥ (succ n) h = ⊥-elim (Sx≡x→⊥ n (succInjective h))

2^[x+1]≢1 : ∀ n → 2 ^ (succ n) ≢ 1
2^[x+1]≢1 n h = Sx≡x→⊥ 1 (i*j≡1⇒i≡1 2 (2 ^ n) h)


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

module Categories.Bicategory where

open import Level
open import Data.Product using (Σ; _,_)
open import Relation.Binary using (Rel)

open import Categories.Category
open import Categories.Category.Monoidal.Instance.Cats using (module Product)
open import Categories.Category.Instance.Cats
open import Categories.Enriched.Category renaming (Category to Enriched)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR

-- https://ncatlab.org/nlab/show/bicategory
-- notice that some axioms in nLab is inconsistent. they have been fixed in this definition.
record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where
  field
    enriched : Enriched (Product.Cats-Monoidal {o} {ℓ} {e}) t

  open Enriched enriched public
  module hom {A B} = Category (hom A B)

  open Functor

  module ⊚ {A B C}          = Functor (⊚ {A} {B} {C})
  module ⊚-assoc {A B C D}  = NaturalIsomorphism (⊚-assoc {A} {B} {C} {D})
  module unitˡ {A B}        = NaturalIsomorphism (unitˡ {A} {B})
  module unitʳ {A B}        = NaturalIsomorphism (unitʳ {A} {B})
  module id {A}             = Functor (id {A})

  infix 4 _⇒₁_ _⇒₂_ _≈_
  infixr 7 _∘ᵥ_ _∘ₕ_
  infixr 9 _▷_
  infixl 9 _◁_
  infixr 11 _⊚₀_ _⊚₁_

  _⇒₁_ : Obj → Obj → Set o
  A ⇒₁ B = Category.Obj (hom A B)

  _⇒₂_ : {A B : Obj} → A ⇒₁ B → A ⇒₁ B → Set ℓ
  _⇒₂_ = hom._⇒_

  _⊚₀_ : {A B C : Obj} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  f ⊚₀ g = ⊚.F₀ (f , g)

  _⊚₁_ : {A B C : Obj} {f h : B ⇒₁ C} {g i : A ⇒₁ B} → f ⇒₂ h → g ⇒₂ i → f ⊚₀ g ⇒₂ h ⊚₀ i
  α ⊚₁ β = ⊚.F₁ (α , β)

  _≈_ : {A B : Obj} {f g : A ⇒₁ B} → Rel (f ⇒₂ g) e
  _≈_ = hom._≈_

  id₁ : {A : Obj} → A ⇒₁ A
  id₁ {_} = id.F₀ _

  id₂ : {A B : Obj} {f : A ⇒₁ B} → f ⇒₂ f
  id₂ = hom.id

  -- horizontal composition
  _∘ₕ_ : {A B C : Obj} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  _∘ₕ_ = _⊚₀_

  -- vertical composition
  _∘ᵥ_ : {A B : Obj} {f g h : A ⇒₁ B} (α : g ⇒₂ h) (β : f ⇒₂ g) → f ⇒₂ h
  _∘ᵥ_ = hom._∘_

  _◁_ : {A B C : Obj} {g h : B ⇒₁ C} (α : g ⇒₂ h) (f : A ⇒₁ B) → g ∘ₕ f ⇒₂ h ∘ₕ f
  α ◁ f = α ⊚₁ id₂

  _▷_ : {A B C : Obj} {f g : A ⇒₁ B} (h : B ⇒₁ C) (α : f ⇒₂ g) → h ∘ₕ f ⇒₂ h ∘ₕ g
  h ▷ α = id₂ ⊚₁ α

  unitorˡ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (id₁ ∘ₕ f) f
  unitorˡ {_} {_} {f} = record
    { from = unitˡ.⇒.η (_ , f)
    ; to   = unitˡ.⇐.η (_ , f)
    ; iso  = unitˡ.iso (_ , f)
    }

  module unitorˡ {A B f} = Mor._≅_ (unitorˡ {A} {B} {f})

  unitorʳ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (f ∘ₕ id₁) f
  unitorʳ {_} {_} {f} = record
    { from = unitʳ.⇒.η (f , _)
    ; to   = unitʳ.⇐.η (f , _)
    ; iso  = unitʳ.iso (f , _)
    }

  module unitorʳ {A B f} = Mor._≅_ (unitorʳ {A} {B} {f})

  associator : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} →  Mor._≅_ (hom A B) ((f ∘ₕ g) ∘ₕ h) (f ∘ₕ g ∘ₕ h)
  associator {_} {_} {_} {_} {f} {g} {h} = record
    { from = ⊚-assoc.⇒.η ((f , g) , h)
    ; to   = ⊚-assoc.⇐.η ((f , g) , h)
    ; iso  = ⊚-assoc.iso ((f , g) , h)
    }

  module associator {A B C D} {f : C ⇒₁ B} {g : D ⇒₁ C} {h} = Mor._≅_ (associator {A = A} {B = B} {f = f} {g = g} {h = h})

  open hom.Commutation

  field
    triangle : {A B C : Obj} {f : A ⇒₁ B} {g : B ⇒₁ C} →
                 [ (g ∘ₕ id₁) ∘ₕ f ⇒ g ∘ₕ f ]⟨
                   associator.from          ⇒⟨ g ∘ₕ id₁ ∘ₕ f ⟩
                   g ▷ unitorˡ.from
                 ≈ unitorʳ.from ◁ f
                 ⟩
    pentagon : {A B C D E : Obj} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} →
                 [ ((i ∘ₕ h) ∘ₕ g) ∘ₕ f ⇒ i ∘ₕ h ∘ₕ g ∘ₕ f ]⟨
                   associator.from ◁ f                     ⇒⟨ (i ∘ₕ h ∘ₕ g) ∘ₕ f ⟩
                   associator.from                         ⇒⟨ i ∘ₕ (h ∘ₕ g) ∘ₕ f ⟩
                   i ▷ associator.from
                 ≈ associator.from                         ⇒⟨ (i ∘ₕ h) ∘ₕ g ∘ₕ f ⟩
                   associator.from
                 ⟩

  private
    variable
      A B C D : Obj
      f g h i : A ⇒₁ B
      α β γ : f ⇒₂ g

  -⊚_ : C ⇒₁ A → Functor (hom A B) (hom C B)
  -⊚_ = appʳ ⊚

  _⊚- : B ⇒₁ C → Functor (hom A B) (hom A C)
  _⊚- = appˡ ⊚

  identity₂ˡ : id₂ ∘ᵥ α ≈ α
  identity₂ˡ = hom.identityˡ

  identity₂ʳ : α ∘ᵥ id₂ ≈ α
  identity₂ʳ = hom.identityʳ

  assoc₂ : (α ∘ᵥ β) ∘ᵥ γ ≈ α ∘ᵥ β ∘ᵥ γ
  assoc₂ = hom.assoc

  id₂◁ : id₂ {f = g} ◁ f ≈ id₂
  id₂◁ = ⊚.identity

  ▷id₂ : f ▷ id₂ {f = g} ≈ id₂
  ▷id₂ = ⊚.identity

  open hom.HomReasoning
  private
    module MR′ {A} {B} where
      open MR (hom A B) public
      open Mor (hom A B) public
    open MR′

  ∘ᵥ-distr-◁ : (α ◁ f) ∘ᵥ (β ◁ f) ≈ (α ∘ᵥ β) ◁ f
  ∘ᵥ-distr-◁ {f = f} = ⟺ (Functor.homomorphism (-⊚ f))

  ∘ᵥ-distr-▷ : (f ▷ α) ∘ᵥ (f ▷ β) ≈ f ▷ (α ∘ᵥ β)
  ∘ᵥ-distr-▷ {f = f} = ⟺ (Functor.homomorphism (f ⊚-))

  ρ-∘ᵥ-▷ : unitorˡ.from ∘ᵥ (id₁ ▷ α) ≈ α ∘ᵥ unitorˡ.from
  ρ-∘ᵥ-▷ {α = α} = begin
    unitorˡ.from ∘ᵥ (id₁ ▷ α)    ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (id.identity , refl)) ⟩
    unitorˡ.from ∘ᵥ id.F₁ _ ⊚₁ α ≈⟨ unitˡ.⇒.commute (_ , α) ⟩
    α ∘ᵥ unitorˡ.from            ∎

  ▷-∘ᵥ-ρ⁻¹ : (id₁ ▷ α) ∘ᵥ unitorˡ.to ≈ unitorˡ.to ∘ᵥ α
  ▷-∘ᵥ-ρ⁻¹ = conjugate-to (≅.sym unitorˡ) (≅.sym unitorˡ) ρ-∘ᵥ-▷

  λ-∘ᵥ-◁ : unitorʳ.from ∘ᵥ (α ◁ id₁) ≈ α ∘ᵥ unitorʳ.from
  λ-∘ᵥ-◁ {α = α} = begin
    unitorʳ.from ∘ᵥ (α ◁ id₁)      ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (refl , id.identity)) ⟩
    unitorʳ.from ∘ᵥ (α ⊚₁ id.F₁ _) ≈⟨ unitʳ.⇒.commute (α , _) ⟩
    α ∘ᵥ unitorʳ.from              ∎

  ◁-∘ᵥ-λ⁻¹ : (α ◁ id₁) ∘ᵥ unitorʳ.to ≈ unitorʳ.to ∘ᵥ α
  ◁-∘ᵥ-λ⁻¹ = conjugate-to (≅.sym unitorʳ) (≅.sym unitorʳ) λ-∘ᵥ-◁

  assoc⁻¹-◁-∘ₕ : associator.to ∘ᵥ (α ◁ (g ∘ₕ f)) ≈ ((α ◁ g) ◁ f) ∘ᵥ associator.to
  assoc⁻¹-◁-∘ₕ {α = α} {g = g} {f = f} = begin
    associator.to ∘ᵥ (α ◁ (g ∘ₕ f))    ≈˘⟨ hom.∘-resp-≈ʳ (⊚.F-resp-≈ (refl , ⊚.identity)) ⟩
    associator.to ∘ᵥ (α ⊚₁ id₂ ⊚₁ id₂) ≈⟨ ⊚-assoc.⇐.commute ((α , id₂) , id₂) ⟩
    ((α ◁ g) ◁ f) ∘ᵥ associator.to     ∎

  assoc⁻¹-▷-◁ : associator.to ∘ᵥ (f ▷ (α ◁ g)) ≈ ((f ▷ α) ◁ g) ∘ᵥ associator.to
  assoc⁻¹-▷-◁ {f = f} {α = α} {g = g} = ⊚-assoc.⇐.commute ((id₂ , α) , id₂)

  assoc⁻¹-▷-∘ₕ : associator.to ∘ᵥ (g ▷ (f ▷ α)) ≈ ((g ∘ₕ f) ▷ α) ∘ᵥ associator.to
  assoc⁻¹-▷-∘ₕ {g = g} {f = f} {α = α} = begin
    associator.to ∘ᵥ (g ▷ (f ▷ α))       ≈⟨ ⊚-assoc.⇐.commute ((id₂ , id₂) , α) ⟩
    ((id₂ ⊚₁ id₂) ⊚₁ α) ∘ᵥ associator.to ≈⟨ hom.∘-resp-≈ˡ (⊚.F-resp-≈ (⊚.identity , refl)) ⟩
    ((g ∘ₕ f) ▷ α) ∘ᵥ associator.to      ∎

  ◁-▷-exchg : ∀ {α : f ⇒₂ g} {β : h ⇒₂ i} → (i ▷ α) ∘ᵥ (β ◁ f) ≈ (β ◁ g) ∘ᵥ (h ▷ α)
  ◁-▷-exchg = [ ⊚ ]-commute

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --cubical #-}
module Agda.Builtin.Cubical.Id where

  open import Agda.Primitive.Cubical
  open import Agda.Builtin.Cubical.Path

  postulate
    Id : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ

  {-# BUILTIN ID           Id       #-}
  {-# BUILTIN CONID        conid    #-}

  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

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module FixityOutOfScopeInRecord where

record R : Set where
  infixl 30 _+_

-- Should complain that _+_ is not in scope
-- in its fixity declaration.


text:
------------------------------------------------------------------------------
-- Non-intuitionistic logic theorems
------------------------------------------------------------------------------

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

module FOL.NonIntuitionistic.TheoremsI where

-- The theorems below are valid with an empty domain.
open import FOL.Base hiding ( D≢∅ )

------------------------------------------------------------------------------
-- The principle of indirect proof (proof by contradiction).
¬-elim : ∀ {A} → (¬ A → ⊥) → A
¬-elim h = case (λ a → a) (λ ¬a → ⊥-elim (h ¬a)) pem

-- Double negation elimination.
¬¬-elim : ∀ {A} → ¬ ¬ A → A
¬¬-elim {A} h = ¬-elim h

-- The reductio ab absurdum rule. (Some authors uses this name for the
-- principle of indirect proof).
raa : ∀ {A} → (¬ A → A) → A
raa h = case (λ a → a) h pem

-- ∃ in terms of ∀ and ¬.
¬∃¬→∀ : {A : D → Set} → ¬ (∃[ x ] ¬ A x) → ∀ {x} → A x
¬∃¬→∀ h {x} = ¬-elim (λ ah → h (x , ah))


text:
module GGT.Group.Definitions
  {a ℓ}
  where

open import Relation.Unary using (Pred)
open import Algebra.Bundles using (Group)
open import Level

IsOpInvClosed : {l : Level} → (G : Group a ℓ) → (Pred (Group.Carrier G) l) → Set (a ⊔ l)
IsOpInvClosed G P = ∀ {x y : Carrier} → P x → P y → P (x - y) where open Group G

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


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

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

{-# BUILTIN REWRITE _≡_ #-}

data _≐_ {ℓ} {A : Set ℓ} (x : A) : A → Prop ℓ where
  refl : x ≐ x

postulate
  subst : ∀ {ℓ ℓ′} {A : Set ℓ} (P : A → Set ℓ′)
        → (x y : A) → x ≐ y → P x → P y
  subst-rew : ∀ {ℓ ℓ′} {A : Set ℓ} (P : A → Set ℓ′)
            → {x : A} (e : x ≐ x) (p : P x) → subst P x x e p ≡ p
{-# REWRITE subst-rew #-}

data Box (A : Prop) : Set where
  box : A -> Box A

foo : (A : Prop)(x y : A)(P : Box A → Set)(p : P (box x)) → subst P (box x) (box y) refl p ≐ p
foo A x y P p = refl -- refl does not type check

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Polymorphic and iso-recursive lambda terms
------------------------------------------------------------------------

module SystemF.Term where

open import Data.Fin using (Fin; zero; suc; inject+)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Nat using (ℕ; suc; _+_; _∸_)
open import Data.Product using (Σ; _,_)
open import Data.Vec using (Vec; []; _∷_; lookup; map)
open import Function as Fun hiding (id)
open import Relation.Binary.PropositionalEquality as PropEq
  using (refl; _≡_; cong; cong₂; sym)
open PropEq.≡-Reasoning

open import SystemF.Type

------------------------------------------------------------------------
-- Untyped terms and values

infixl 9 _[_] _·_

-- Untyped terms with up to m free term variables and up to n free
-- type variables
data Term (m n : ℕ) : Set where
  var     : (x : Fin m)                   → Term m n  -- term variable
  Λ       : Term m (1 + n)                → Term m n  -- type abstraction
  λ'      : Type n       → Term (1 + m) n → Term m n  -- term abstraction
  μ       : Type n       → Term (1 + m) n → Term m n  -- recursive term
  _[_]    : Term m n     → Type n         → Term m n  -- type application
  _·_     : Term m n     → Term m n       → Term m n  -- term application
  fold    : Type (1 + n) → Term m n       → Term m n  -- fold recursive type
  unfold  : Type (1 + n) → Term m n       → Term m n  -- unfold recursive type

-- Untyped values with up to m free term variables and up to n free
-- type variables
data Val (m n : ℕ) : Set where
  Λ       : Term m (1 + n)                → Val m n   -- type abstraction
  λ'      : Type n       → Term (1 + m) n → Val m n   -- term abstraction
  fold    : Type (1 + n) → Val m n        → Val m n   -- fold recursive type

-- Conversion from values to terms
⌜_⌝  : ∀ {m n} → Val m n → Term m n
⌜ Λ x      ⌝ = Λ x
⌜ λ' a t   ⌝ = λ' a t
⌜ fold a t ⌝ = fold a ⌜ t ⌝

------------------------------------------------------------------------
-- Substitutions in terms

-- Type substitutions in terms
module TermTypeSubst where

  module TermTypeApp {T : ℕ → Set} (l : Lift T Type) where
    open Lift l hiding (var)
    open TypeSubst.TypeApp l renaming (_/_ to _/tp_)

    infixl 8 _/_

    -- Apply a type substitution to a term
    _/_ : ∀ {m n k} → Term m n → Sub T n k → Term m k
    var x      / σ = var x
    Λ t        / σ = Λ (t / σ ↑)
    λ' a t     / σ = λ' (a /tp σ) (t / σ)
    μ a t      / σ = μ (a /tp σ) (t / σ)
    t [ a ]    / σ = (t / σ) [ a /tp σ ]
    s · t      / σ = (s / σ) · (t / σ)
    fold a t   / σ = fold (a /tp σ ↑) (t / σ)
    unfold a t / σ = unfold (a /tp σ ↑) (t / σ)

  open TypeSubst using (varLift; termLift; sub)

  module Lifted {T} (lift : Lift T Type) {m} where
    application : Application (Term m) T
    application = record { _/_ = TermTypeApp._/_ lift {m = m} }

    open Application application public

  open Lifted termLift public

  -- Apply a type variable substitution (renaming) to a term
  _/Var_ : ∀ {m n k} → Term m n → Sub Fin n k → Term m k
  _/Var_ = TermTypeApp._/_ varLift

  -- Weaken a term with an additional type variable
  weaken : ∀ {m n} → Term m n → Term m (suc n)
  weaken t = t /Var VarSubst.wk

  infix 8 _[/_]

  -- Shorthand for single-variable type substitutions in terms
  _[/_] : ∀ {m n} → Term m (1 + n) → Type n → Term m n
  t [/ b ] = t / sub b

-- Lemmas about type substitutions in terms.
module TermTypeLemmas where
  open TermTypeSubst public

  private module T = TypeLemmas
  private module V = VarLemmas

  /-↑⋆ :
    ∀ {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} →
    let open T.Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/tp₁_)
        open   Lifted lift₁ using () renaming (_/_  to _/₁_)
        open T.Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/tp₂_)
        open   Lifted lift₂ using () renaming (_/_  to _/₂_)
    in
    ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
    (∀ i x → Type.var x /tp₁ ρ₁ ↑⋆₁ i ≡ Type.var x /tp₂ ρ₂ ↑⋆₂ i) →
     ∀ i {m} (t : Term m (i + n))  → t /₁ ρ₁ ↑⋆₁ i ≡ t /₂ ρ₂ ↑⋆₂ i
  /-↑⋆ ρ₁ ρ₂ hyp i (var x)      = refl
  /-↑⋆ ρ₁ ρ₂ hyp i (Λ t)        = cong Λ      (/-↑⋆ ρ₁ ρ₂ hyp (1 + i) t)
  /-↑⋆ ρ₁ ρ₂ hyp i (λ' a t)     =
    cong₂ λ'     (T./-↑⋆ ρ₁ ρ₂ hyp i a)       (/-↑⋆ ρ₁ ρ₂ hyp i t)
  /-↑⋆ ρ₁ ρ₂ hyp i (μ a t)      =
    cong₂ μ      (T./-↑⋆ ρ₁ ρ₂ hyp i a)       (/-↑⋆ ρ₁ ρ₂ hyp i t)
  /-↑⋆ ρ₁ ρ₂ hyp i (t [ b ])    =
    cong₂ _[_]     (/-↑⋆ ρ₁ ρ₂ hyp i t)     (T./-↑⋆ ρ₁ ρ₂ hyp i b)
  /-↑⋆ ρ₁ ρ₂ hyp i (s · t)      =
    cong₂ _·_      (/-↑⋆ ρ₁ ρ₂ hyp i s)       (/-↑⋆ ρ₁ ρ₂ hyp i t)
  /-↑⋆ ρ₁ ρ₂ hyp i (fold a t)   =
    cong₂ fold   (T./-↑⋆ ρ₁ ρ₂ hyp (1 + i) a) (/-↑⋆ ρ₁ ρ₂ hyp i t)
  /-↑⋆ ρ₁ ρ₂ hyp i (unfold a t) =
    cong₂ unfold (T./-↑⋆ ρ₁ ρ₂ hyp (1 + i) a) (/-↑⋆ ρ₁ ρ₂ hyp i t)

  /-wk : ∀ {m n} (t : Term m n) → t / TypeSubst.wk ≡ weaken t
  /-wk t = /-↑⋆ TypeSubst.wk VarSubst.wk (λ k x → begin
    tpVar x T./ T.wk T.↑⋆ k         ≡⟨ T.var-/-wk-↑⋆ k x ⟩
    tpVar (Data.Fin.lift k suc x)   ≡⟨ cong tpVar (sym (V.var-/-wk-↑⋆ k x)) ⟩
    tpVar (lookup (V.wk V.↑⋆ k) x)  ≡⟨ refl ⟩
    tpVar x T./Var V.wk V.↑⋆ k      ∎) 0 t
      where open Type using () renaming (var to tpVar)

-- Term substitutions in terms
module TermTermSubst where

  -- Substitutions of terms in terms
  --
  -- A TermSub T m n k is a substitution which, when applied to a term
  -- with at most m free term variables and n free type variables,
  -- yields a term with at most k free term variables and n free type
  -- variables.
  TermSub : (ℕ → ℕ → Set) → ℕ → ℕ → ℕ → Set
  TermSub T m n k = Sub (flip T n) m k

  record TermLift (T : ℕ → ℕ → Set) : Set where
    infix 10 _↑tm _↑tp
    field
      lift : ∀ {m n} → T m n → Term m n
      _↑tm : ∀ {m n k} → TermSub T m n k → TermSub T (suc m) n (suc k)
      _↑tp : ∀ {m n k} → TermSub T m n k → TermSub T m (suc n) k

  module TermTermApp {T} (l : TermLift T) where
    open TermLift l

    infixl 8 _/_

    -- Apply a term substitution to a term
    _/_ : ∀ {m n k} → Term m n → TermSub T m n k → Term k n
    var x      / ρ = lift (lookup ρ x)
    Λ t        / ρ = Λ (t / ρ ↑tp)
    λ' a t     / ρ = λ' a (t / ρ ↑tm)
    μ a t      / ρ = μ a (t / ρ ↑tm)
    t [ a ]    / ρ = (t / ρ) [ a ]
    s · t      / ρ = (s / ρ) · (t / ρ)
    fold a t   / ρ = fold a (t / ρ)
    unfold a t / ρ = unfold a (t / ρ)

  Fin′ : ℕ → ℕ → Set
  Fin′ m _ = Fin m

  varLift : TermLift Fin′
  varLift = record { lift = var; _↑tm = VarSubst._↑; _↑tp = Fun.id }

  infixl 8 _/Var_

  _/Var_ : ∀ {m n k} → Term m n → Sub Fin m k → Term k n
  _/Var_ = TermTermApp._/_ varLift

  Term′ : ℕ → ℕ → Set
  Term′ = flip Term

  private
    module ExpandSimple {n : ℕ} where
      simple : Simple (Term′ n)
      simple = record { var = var; weaken = λ t → t /Var VarSubst.wk }

      open Simple simple public

  open ExpandSimple  using (_↑; simple)
  open TermTypeSubst using () renaming (weaken to weakenTp)

  termLift : TermLift Term
  termLift = record
    { lift = Fun.id; _↑tm = _↑ ; _↑tp = λ ρ → map weakenTp ρ }

  private
    module ExpandSubst {n : ℕ} where
      app : Application (Term′ n) (Term′ n)
      app = record { _/_ = TermTermApp._/_ termLift {n = n} }

      subst : Subst (flip Term n)
      subst = record
        { simple      = simple
        ; application = app
        }

      open Subst subst public

  open ExpandSubst public hiding (var; simple)

  infix 8 _[/_]

  -- Shorthand for single-variable term substitutions in terms
  _[/_] : ∀ {m n} → Term (1 + m) n → Term m n → Term m n
  s [/ t ] = s / sub t

open TermTypeSubst renaming (weaken to weakenTmTp)
open TermTermSubst renaming (weaken to weakenTmTm) hiding (id)
open TypeSubst     renaming (weaken to weakenTp; weaken↑ to weakenTp↑)
                   hiding (id)

------------------------------------------------------------------------
-- Encoding of additional term operators
--
-- NOTE: These encoded operators require more type information than
-- their "classic" untyped counterparts.  The additional types are
-- required by the underlying (untyped) abstractions and type
-- applications.  Cf. TAPL sec. 24.3, pp. 377-379.
module TermOperators where

  open TypeOperators using (⊤; ⊥; _→ⁿ_)

  -- Polymorphic identity function
  id : {m n : ℕ} → Term m n
  id = Λ (λ' (var zero) (var zero))

  -- Bottom elimination/univeral property of the initial type
  ⊥-elim : ∀ {m n} → Type n → Term m n
  ⊥-elim a = λ' ⊥ ((var zero) [ a ])

  -- Unit value
  tt = id

  -- Top introduction/universal property of the terminal type
  ⊤-intro : ∀ {m n} → Type n → Term m n
  ⊤-intro a = λ' a id

  -- Packing existential types
  as-∃_pack_,_ : ∀ {m n} → Type (1 + n) → Type n → Term m n → Term m n
  as-∃ a pack b , t =
    Λ (λ' (∀' (weakenTp↑ a →' var (suc zero)))
          ((var zero [ weakenTp b ]) · weakenTmTm (weakenTmTp t)))

  -- Unpacking existential types
  unpack_in'_ : ∀ {m n} → Term m n → Term (1 + m) (1 + n) →
                {a : Type (1 + n)} {b : Type n} → Term m n
  unpack_in'_ s t {a} {b} = (s [ b ]) · (Λ (λ' a t))

  -- n-ary term abstraction
  λⁿ : ∀ {m n k} → Vec (Type n) k → Term (k + m) n → Term m n
  λⁿ []       t = t
  λⁿ (a ∷ as) t = λⁿ as (λ' a t)

  infixl 9 _·ⁿ_

  -- n-ary term application
  _·ⁿ_ : ∀ {m n k} → Term m n → Vec (Term m n) k → Term m n
  s ·ⁿ []       = s
  s ·ⁿ (t ∷ ts) = s ·ⁿ ts · t

  -- Record/tuple constructor
  new : ∀ {m n k} → Vec (Term m n) k → {as : Vec (Type n) k} → Term m n
  new []                = tt
  new (t ∷ ts) {a ∷ as} =
    Λ (λ' (map weakenTp (a ∷ as) →ⁿ var zero)
          (var zero ·ⁿ map weakenTmTm (map weakenTmTp (t ∷ ts))))

  -- Field access/projection
  π : ∀ {m n k} → Fin k → Term m n → {as : Vec (Type n) k} → Term m n
  π     () t {[]}
  π {m} x  t {a ∷ as} =
    (t [ lookup (a ∷ as) x ]) · (λⁿ (a ∷ as) (var (inject+ m x)))

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
module Codata where

codata D : Set where

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
-- 2010-10-15

module DoNotEtaExpandMVarsWhenComparingAgainstRecord where

open import Common.Irrelevance

data _==_ {A : Set1}(a : A) : A -> Set where
  refl : a == a

record IR : Set1 where
  constructor mkIR
  field
    .fromIR : Set

open IR

reflIR2 : (r : IR) -> _ == mkIR (fromIR r)
reflIR2 r = refl {a = _}
-- this would fail if
-- ? = mkIR (fromIR r)
-- would be solved by
-- mkIR ?1 = mkIR (fromIR r)
-- because then no constraint is generated for ?1 due to triviality