text:
------------------------------------------------------------------------------
-- Conversion rules for the division
------------------------------------------------------------------------------

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

module LTC-PCF.Program.Division.ConversionRules where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Program.Division.Division

------------------------------------------------------------------------------
-- Division properties

private
    -- Before to prove some properties for div it is convenient
    -- to have a proof for each possible execution step.

    -- Initially, we define the possible states (div-s₁, div-s₂,
    -- ...) and after that, we write down the proof for the execution
    -- step from the state p to the state q, e.g.
    --
    -- proof₂₋₃ : ∀ i j → div-s₂ i j ≡ div-s₃ i j.

    -- Initially, the conversion rule fix-eq is applied.
    div-s₁ : D → D → D
    div-s₁ i j = divh (fix divh) · i · j

    -- First argument application.
    div-s₂ : D → D → D
    div-s₂ i j = fun · j
      where
      fun : D
      fun = lam (λ j → if (lt i j)
                         then zero
                         else succ₁ (fix divh · (i ∸ j) · j))

    -- Second argument application.
    div-s₃ : D → D → D
    div-s₃ i j = if (lt i j) then zero else succ₁ (fix divh · (i ∸ j) · j)

    -- lt i j ≡ true.
    div-s₄ : D → D → D
    div-s₄ i j = if true then zero else succ₁ (fix divh · (i ∸ j) · j)

    -- lt i j ≡ false.
    div-s₅ : D → D → D
    div-s₅ i j = if false then zero else succ₁ (fix divh · (i ∸ j) · j)

    -- The conditional is true.
    div-s₆ : D
    div-s₆ = zero

    -- The conditional is false.
    div-s₇ : D → D → D
    div-s₇ i j = succ₁ (fix divh · (i ∸ j) · j)

    {-

    To prove the execution steps, e.g.

    proof₃₋₄ : ∀ i j → div-s₃ i j → divh_s₄ i j,

    we usually need to prove that

                             ... m ... ≡ ... n ...    (1)

    given that
                                  m ≡ n,              (2)

    where (2) is a conversion rule usually.

    We prove (1) using

    subst : ∀ {x y} (A : D → Set) → x ≡ y → A x → A y

    where
      • P is given by \m → ... m ... ≡ ... n ...,
      • x ≡ y is given n ≡ m (actually, we use ≡-sym (m ≡ n)) and
      • P x is given by ... n ... ≡ ... n ... (i.e. ≡-refl)
    -}

    -- From div · i · j to div-s₁ using the conversion rule fix-eq.
    proof₀₋₁ : ∀ i j → fix divh · i · j ≡ div-s₁ i j
    proof₀₋₁ i j = subst (λ t → t · i · j ≡ divh (fix divh) · i · j)
                         (sym (fix-eq divh))
                         refl

    -- From div-s₁ to div-s₂ using the conversion rule beta.
    proof₁₋₂ : ∀ i j → div-s₁ i j ≡ div-s₂ i j
    proof₁₋₂ i j =
      subst (λ t → t · j ≡ fun i · j)
            (sym (beta fun i))
            refl
         where
         -- The function fun is the same that the fun part of div-s₂,
         -- except that we need a fresh variable y to avoid the
         -- clashing of the variable i in the application of the beta
         -- rule.
         fun : D → D
         fun y = lam (λ j → if (lt y j)
                              then zero
                              else succ₁ (fix divh · (y ∸ j) · j))

    -- From div-s₂ to div-s₃ using the conversion rule beta.
    proof₂₋₃ : ∀ i j → div-s₂ i j ≡ div-s₃ i j
    proof₂₋₃ i j  = beta fun j
      where
      -- The function fun is the same that div-s₃, except that we
      -- need a fresh variable y to avoid the clashing of the
      -- variable j in the application of the beta rule.
      fun : D → D
      fun y = if (lt i y) then zero else succ₁ ((fix divh) · (i ∸ y) · y)

    -- From div-s₃ to div-s₄ using the proof i<j.
    proof₃_₄ : ∀ i j → i < j → div-s₃ i j ≡ div-s₄ i j
    proof₃_₄ i j i<j =
      subst (λ t → (if t then zero else succ₁ ((fix divh) · (i ∸ j) · j)) ≡
                   (if true then zero else succ₁ ((fix divh) · (i ∸ j) · j)))
            (sym i<j)
            refl

    -- From div-s₃ to div-s₅ using the proof i≮j.
    proof₃₋₅ : ∀ i j → i ≮ j → div-s₃ i j ≡ div-s₅ i j
    proof₃₋₅ i j i≮j =
      subst (λ t → (if t then zero else succ₁ ((fix divh) · (i ∸ j) · j)) ≡
                   (if false then zero else succ₁ ((fix divh) · (i ∸ j) · j)))
            (sym i≮j)
            refl

    -- From div-s₄ to div-s₆ using the conversion rule if-true.
    proof₄₋₆ : ∀ i j → div-s₄ i j ≡ div-s₆
    proof₄₋₆ i j = if-true zero

    -- From div-s₅ to div-s₇ using the conversion rule if-false.
    proof₅₋₇ : ∀ i j → div-s₅ i j ≡ div-s₇ i j
    proof₅₋₇ i j = if-false (succ₁ (fix divh · (i ∸ j) · j))

----------------------------------------------------------------------
-- The division result when the dividend is minor than the
-- the divisor.
div-x<y : ∀ {i j} → i < j → div i j ≡ zero
div-x<y {i} {j} i<j =
  div i j    ≡⟨ proof₀₋₁ i j ⟩
  div-s₁ i j ≡⟨ proof₁₋₂ i j ⟩
  div-s₂ i j ≡⟨ proof₂₋₃ i j ⟩
  div-s₃ i j ≡⟨ proof₃_₄ i j i<j ⟩
  div-s₄ i j ≡⟨ proof₄₋₆ i j ⟩
  div-s₆     ∎

----------------------------------------------------------------------
-- The division result when the dividend is greater or equal than the
-- the divisor.
div-x≮y : ∀ {i j} → i ≮ j → div i j ≡ succ₁ (div (i ∸ j) j)
div-x≮y {i} {j} i≮j =
  div i j    ≡⟨ proof₀₋₁ i j ⟩
  div-s₁ i j ≡⟨ proof₁₋₂ i j ⟩
  div-s₂ i j ≡⟨ proof₂₋₃ i j ⟩
  div-s₃ i j ≡⟨ proof₃₋₅ i j i≮j ⟩
  div-s₅ i j ≡⟨ proof₅₋₇ i j ⟩
  div-s₇ i j ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Issue314 where

postulate A : Set

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

postulate lemma : (x y : A) → x ≡ y

Foo : A → Set₁
Foo x with lemma x _
Foo x | refl = Set

-- Bug.agda:12,9-13
-- Failed to solve the following constraints:
--   x == _23 x : A
-- when checking that the pattern refl has type x ≡ _23 x

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Agda.Builtin.List
open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Data.Empty
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Unit
open import Cubical.Relation.Nullary

open import Cubical.Data.List.Base

module _ {ℓ} {A : Type ℓ} where

  ++-unit-r : (xs : List A) → xs ++ [] ≡ xs
  ++-unit-r [] = refl
  ++-unit-r (x ∷ xs) = cong (_∷_ x) (++-unit-r xs)

  ++-assoc : (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ ys ++ zs
  ++-assoc [] ys zs = refl
  ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

  rev-++ : (xs ys : List A) → rev (xs ++ ys) ≡ rev ys ++ rev xs
  rev-++ [] ys = sym (++-unit-r (rev ys))
  rev-++ (x ∷ xs) ys =
    cong (λ zs → zs ++ [ x ]) (rev-++ xs ys)
    ∙ ++-assoc (rev ys) (rev xs) [ x ]

  rev-rev : (xs : List A) → rev (rev xs) ≡ xs
  rev-rev [] = refl
  rev-rev (x ∷ xs) = rev-++ (rev xs) [ x ] ∙ cong (_∷_ x) (rev-rev xs)

-- Path space of list type
module ListPath {ℓ} {A : Type ℓ} where

  Cover : List A → List A → Type ℓ
  Cover [] [] = Lift Unit
  Cover [] (_ ∷ _) = Lift ⊥
  Cover (_ ∷ _) [] = Lift ⊥
  Cover (x ∷ xs) (y ∷ ys) = (x ≡ y) × Cover xs ys

  reflCode : ∀ xs → Cover xs xs
  reflCode [] = lift tt
  reflCode (_ ∷ xs) = refl , reflCode xs

  encode : ∀ xs ys → (p : xs ≡ ys) → Cover xs ys
  encode xs _ = J (λ ys _ → Cover xs ys) (reflCode xs)

  encodeRefl : ∀ xs → encode xs xs refl ≡ reflCode xs
  encodeRefl xs = JRefl (λ ys _ → Cover xs ys) (reflCode xs)

  decode : ∀ xs ys → Cover xs ys → xs ≡ ys
  decode [] [] _ = refl
  decode [] (_ ∷ _) (lift ())
  decode (x ∷ xs) [] (lift ())
  decode (x ∷ xs) (y ∷ ys) (p , c) = cong₂ _∷_ p (decode xs ys c)

  decodeRefl : ∀ xs → decode xs xs (reflCode xs) ≡ refl
  decodeRefl [] = refl
  decodeRefl (x ∷ xs) = cong (cong₂ _∷_ refl) (decodeRefl xs)

  decodeEncode : ∀ xs ys → (p : xs ≡ ys) → decode xs ys (encode xs ys p) ≡ p
  decodeEncode xs _ =
    J (λ ys p → decode xs ys (encode xs ys p) ≡ p)
      (cong (decode xs xs) (encodeRefl xs) ∙ decodeRefl xs)

  isOfHLevelCover : (n : ℕ) (p : isOfHLevel (suc (suc n)) A)
    (xs ys : List A) → isOfHLevel (suc n) (Cover xs ys)
  isOfHLevelCover n p [] [] =
    isOfHLevelLift (suc n)
      (subst (λ m → isOfHLevel m Unit) (+-comm n 1)
        (hLevelLift n isPropUnit))
  isOfHLevelCover n p [] (y ∷ ys) =
    isOfHLevelLift (suc n)
      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
        (hLevelLift n isProp⊥))
  isOfHLevelCover n p (x ∷ xs) [] =
    isOfHLevelLift (suc n)
      (subst (λ m → isOfHLevel m ⊥) (+-comm n 1)
        (hLevelLift n isProp⊥))
  isOfHLevelCover n p (x ∷ xs) (y ∷ ys) =
    hLevelProd (suc n) (p x y) (isOfHLevelCover n p xs ys)

isOfHLevelList : ∀ {ℓ} (n : ℕ) {A : Type ℓ}
  → isOfHLevel (suc (suc n)) A → isOfHLevel (suc (suc n)) (List A)
isOfHLevelList n ofLevel xs ys =
  retractIsOfHLevel (suc n)
    (ListPath.encode xs ys)
    (ListPath.decode xs ys)
    (ListPath.decodeEncode xs ys)
    (ListPath.isOfHLevelCover n ofLevel xs ys)

private
  variable
    ℓ : Level
    A : Type ℓ

  caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B
  caseList n _ []      = n
  caseList _ c (_ ∷ _) = c

  safe-head : A → List A → A
  safe-head x []      = x
  safe-head _ (x ∷ _) = x

  safe-tail : List A → List A
  safe-tail []       = []
  safe-tail (_ ∷ xs) = xs

cons-inj₁ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y
cons-inj₁ {x = x} p = cong (safe-head x) p

cons-inj₂ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
cons-inj₂ = cong safe-tail

¬cons≡nil : ∀ {x : A} {xs} → ¬ (x ∷ xs ≡ [])
¬cons≡nil {A = A} p = lower (subst (caseList (Lift ⊥) (List A)) p [])

¬nil≡cons : ∀ {x : A} {xs} → ¬ ([] ≡ x ∷ xs)
¬nil≡cons {A = A} p = lower (subst (caseList (List A) (Lift ⊥)) p [])

¬snoc≡nil : ∀ {x : A} {xs} → ¬ (xs ∷ʳ x ≡ [])
¬snoc≡nil {xs = []} contra = ¬cons≡nil contra
¬snoc≡nil {xs = x ∷ xs} contra = ¬cons≡nil contra

¬nil≡snoc : ∀ {x : A} {xs} → ¬ ([] ≡ xs ∷ʳ x)
¬nil≡snoc contra = ¬snoc≡nil (sym contra)

cons≡rev-snoc : (x : A) → (xs : List A) → x ∷ rev xs ≡ rev (xs ∷ʳ x)
cons≡rev-snoc _ [] = refl
cons≡rev-snoc x (y ∷ ys) = λ i → cons≡rev-snoc x ys i ++ y ∷ []

nil≡nil-isContr : isContr (Path (List A) [] [])
nil≡nil-isContr = refl , ListPath.decodeEncode [] []

list≡nil-isProp : {xs : List A} → isProp (xs ≡ [])
list≡nil-isProp {xs = []} = hLevelSuc 0 _ nil≡nil-isContr
list≡nil-isProp {xs = x ∷ xs} = λ p _ → ⊥-elim (¬cons≡nil p)

discreteList : Discrete A → Discrete (List A)
discreteList eqA []       []       = yes refl
discreteList eqA []       (y ∷ ys) = no ¬nil≡cons
discreteList eqA (x ∷ xs) []       = no ¬cons≡nil
discreteList eqA (x ∷ xs) (y ∷ ys) with eqA x y | discreteList eqA xs ys
... | yes p | yes q = yes (λ i → p i ∷ q i)
... | yes _ | no ¬q = no (λ p → ¬q (cons-inj₂ p))
... | no ¬p | _     = no (λ q → ¬p (cons-inj₁ q))

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


text:
module UnequalHiding where

data One : Set where one : One

f : ({A : Set} -> A -> A) -> One
f = \(id : (A : Set) -> A -> A) -> id One one


text:
data _≡_ {X : Set} : X → X → Set where
  refl : {x : X} → x ≡ x

ap : {X Y : Set} (f : X → Y) {x x' : X} → x ≡ x' → f x ≡ f x'
ap f refl = refl

_∙_ : {X : Set} {x y z : X} → x ≡ y → y ≡ z → x ≡ z
p ∙ refl = p

f : {X : Set} {x : X} {A : X → Set} (η θ : (y : X) → x ≡ y → A y)
  → η x refl ≡ θ x refl → ∀ y p → η y p ≡ θ y p
f η θ q y refl = ap (λ a → a) q

succeeds : (X : Set) (z t : X) (r : z ≡ t)
         → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
         ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
succeeds X z = f -- {A = λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - }
                (λ z r x y p q → (p ∙ q) ∙ r)
                (λ z r x y p q → p ∙ (q ∙ r))
                refl

fails : (X : Set) (z t : X) (r : z ≡ t)
      → (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → (p ∙ q) ∙ r)
      ≡ (λ (x y : X) (p : x ≡ y) (q : y ≡ z) → p ∙ (q ∙ r))
fails X z t = f -- {A = λ - → (x y : X) (p : x ≡ y) (q : y ≡ z) → x ≡ - }
               (λ z r x y p q → (p ∙ q) ∙ r)
               (λ z r x y p q → p ∙ (q ∙ r))
               refl
               t

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Oscar.Data.Step {𝔣} (FunctionName : Set 𝔣) where

open import Data.Nat using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂; cong; sym; trans)
open import Function using (_∘_; flip)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Product using (∃; _,_; _×_)
open import Data.Empty using (⊥-elim)
open import Data.Vec using (Vec; []; _∷_)

open import Oscar.Data.Fin
open import Data.Nat hiding (_≤_)
open import Relation.Binary.PropositionalEquality renaming ([_] to [[_]])
open import Function using (_∘_; id; case_of_; _$_; flip)
open import Relation.Nullary
open import Data.Product renaming (map to _***_)
open import Data.Empty
open import Data.Maybe
open import Category.Functor
open import Category.Monad
import Level
open RawMonad (Data.Maybe.monad {Level.zero})
open import Data.Sum
open import Data.Maybe using (maybe; maybe′; nothing; just; monad; Maybe)
open import Data.List renaming (_++_ to _++L_)
open ≡-Reasoning
open import Data.Vec using (Vec; []; _∷_) renaming (_++_ to _++V_; map to mapV)

open import Oscar.Data.Term FunctionName

data Step (n : ℕ) : Set 𝔣 where
  left : Term n -> Step n
  right : Term n -> Step n
  function : FunctionName → ∀ {L} → Vec (Term n) L → ∀ {R} → Vec (Term n) R → Step n

fmapS : ∀ {n m} (f : Term n -> Term m) (s : Step n) -> Step m
fmapS f (left x) = left (f x)
fmapS f (right x) = right (f x)
fmapS f (function fn ls rs) = function fn (mapV f ls) (mapV f rs)

_⊹_ : ∀ {n} (ps : List (Step n)) (t : Term n) -> Term n
[] ⊹ t             = t
(left r ∷ ps) ⊹ t  = (ps ⊹ t) fork r
(right l ∷ ps) ⊹ t = l fork (ps ⊹ t)
(function fn ls rs ∷ ps) ⊹ t = function fn (ls ++V (ps ⊹ t) ∷ rs)

fork++ : ∀ {m} {s t : Term m} ps ->
              (ps ⊹ (s fork t) ≡ (ps ++L [ left t ]) ⊹ s)
              × (ps ⊹ (s fork t) ≡ (ps ++L [ right s ]) ⊹ t)
fork++ [] = refl , refl
fork++ (left y' ∷ xs') = (cong (λ a -> a fork y') *** cong (λ a -> a fork y')) (fork++ xs')
fork++ (right y' ∷ xs') = (cong (λ a -> y' fork a) *** cong (λ a -> y' fork a)) (fork++ xs')
fork++ {s = s} {t} (function fn ls rs ∷ xs') =
  (cong (λ a → function fn (ls ++V a ∷ rs)) *** cong (λ a → function fn (ls ++V a ∷ rs))) (fork++ xs')

function++ : ∀ {m} {fn} {t : Term m} {L} {ls : Vec (Term m) L} {R} {rs : Vec (Term m) R} ps →
               ps ⊹ (function fn (ls ++V t ∷ rs)) ≡ (ps ++L [ function fn ls rs ]) ⊹ t
function++ [] = refl
function++ (left x ∷ ps) = cong (_fork x) (function++ ps)
function++ (right x ∷ ps) = cong (x fork_) (function++ ps)
function++ (function fn ls rs ∷ ps) = cong (λ a → function fn (ls ++V a ∷ rs)) (function++ ps)

-- _◃S_ : ∀ {n m} (f : n ⊸ m) -> List (Step n) -> List (Step m)
-- _◃S_ f = Data.List.map (fmapS (f ◃_))

-- map-[] : ∀ {n m} (f : n ⊸ m) ps -> f ◃S ps ≡ [] -> ps ≡ []
-- map-[] f [] _ = refl
-- map-[] f (x ∷ xs) ()

-- module StepM where

--   lemma1 : ∀ {n} (x : Step n) xs t -> [ x ] ⊹ ( xs ⊹ t ) ≡ (x ∷ xs) ⊹ t
--   lemma1 (left y) xs t = refl
--   lemma1 (right y) xs t = refl
--   lemma1 (function fn ls rs) xs t = refl

--   lemma2 : ∀ {n} {r} {t} {xs} (x : Step n) -> xs ⊹ t ≡ r -> ((x ∷ xs) ⊹ t ) ≡ [ x ] ⊹ r
--   lemma2 (left y) eq = cong (λ t -> t fork y) eq
--   lemma2 (right y) eq = cong (λ t -> y fork t) eq
--   lemma2 (function fn ls rs) eq = cong (λ t → function fn (ls ++V t ∷ rs)) eq

--   fact1 : ∀ {n} ps qs (t : Term n) -> (ps ++L qs) ⊹ t ≡ ps ⊹ (qs ⊹ t)
--   fact1 [] qs t = refl
--   fact1 (p ∷ ps) qs t = begin (p ∷ (ps ++L qs)) ⊹ t ≡⟨ lemma2 p (fact1 ps qs t) ⟩
--                               [ p ] ⊹ (ps ⊹ (qs ⊹ t)) ≡⟨ lemma1 p ps (qs ⊹ t)  ⟩
--                               (p ∷ ps) ⊹ (qs ⊹ t) ∎

--   ◃-fact1 : ∀ {m n} (f : m ⊸ n) {N} (rs : Vec (Term m) N) → f ◃s rs ≡ mapV (f ◃_) rs
--   ◃-fact1 f [] = refl
--   ◃-fact1 f (x ∷ rs) rewrite ◃-fact1 f rs = refl

--   ◃-fact2 : ∀ {m n} (f : m ⊸ n) {L} (ls : Vec (Term m) L) {R} (rs : Vec (Term m) R) → f ◃s (ls ++V rs) ≡ (f ◃s ls) ++V (f ◃s rs)
--   ◃-fact2 f [] rs = refl
--   ◃-fact2 f (l ∷ ls) rs = cong ((f ◃ l) ∷_) (◃-fact2 f ls rs)

--   fact2 : ∀ {m n} (f : m ⊸ n) t ps ->
--                f ◃ (ps ⊹ t) ≡ (f ◃S ps) ⊹ (f ◃ t)
--   fact2 f t [] = refl
--   fact2 f t (left y ∷ xs) = cong (λ t -> t fork (f ◃ y)) (fact2 f t xs)
--   fact2 f t (right y ∷ xs) = cong (λ t -> (f ◃ y) fork t) (fact2 f t xs)
--   fact2 f t (function fn ls rs ∷ xs) rewrite sym (◃-fact1 f ls) | sym (◃-fact1 f rs) = cong (function fn) (trans (◃-fact2 f ls ((xs ⊹ t) ∷ rs)) (cong ((f ◃s ls) ++V_) (cong (_∷ (f ◃s rs)) (fact2 f t xs))))

-- mutual

--   check-props : ∀ {m} (x : Fin (suc m)) {N} (ts : Vec (Term (suc m)) N) fn ->
--                  (∃ λ (ts' : Vec (Term m) N) -> ts ≡ ▹ (thin x) ◃s ts' × check x ts ≡ just ts')
--                  ⊎ (∃ λ ps -> function fn ts ≡ (ps ⊹ i x) × check x ts ≡ nothing)
--   check-props x [] fn = inj₁ ([] , refl , refl)
--   check-props x (t ∷ ts) fn with check-prop x t
--   … | inj₂ (ps , t=ps+ix , checkxt=no) rewrite t=ps+ix | checkxt=no = inj₂ (function fn [] ts ∷ ps , refl , refl)
--   … | inj₁ (t' , t=thinxt' , checkxt=t') rewrite checkxt=t' with check-props x ts fn
--   … | inj₁ (ts' , ts=thinxts' , checkxts=ts') rewrite t=thinxt' | ts=thinxts' | checkxts=ts' = inj₁ (_ , refl , refl)
--   … | inj₂ ([] , () , checkxts=no)
--   … | inj₂ (left _ ∷ ps , () , checkxts=no)
--   … | inj₂ (right _ ∷ ps , () , checkxts=no)
--   … | inj₂ (function fn' ls rs ∷ ps , ts=ps+ix , checkxts=no) with Term-function-inj-VecSize ts=ps+ix
--   … | refl with Term-function-inj-Vector ts=ps+ix
--   … | refl rewrite checkxts=no = inj₂ (function fn (t ∷ ls) rs ∷ ps , refl , refl)

--   check-prop : ∀ {m} (x : Fin (suc m)) t ->
--                 (∃ λ t' -> t ≡ ▹ (thin x) ◃ t' × check x t ≡ just t')
--                 ⊎ (∃ λ ps -> t ≡ (ps ⊹ i x) × check x t ≡ nothing)
--   check-prop x (i x') with checkfact1 x x' (check x x') refl
--   check-prop x (i .x) | inj₁ (refl , e) = inj₂ ([] , refl , cong (_<$>_ i) e)
--   ... | inj₂ (y , thinxy≡x' , thickxx'≡justy')
--       = inj₁ (i y
--              , cong i (sym (thinxy≡x'))
--              , cong (_<$>_ i) thickxx'≡justy' )
--   check-prop x leaf = inj₁ (leaf , (refl , refl))
--   check-prop x (s fork t)
--    with check-prop x s                     | check-prop x t
--   ... | inj₁ (s' , s≡thinxs' , checkxs≡s') | inj₁ (t' , t≡thinxt' , checkxt≡t')
--       = inj₁ (s' fork t' , cong₂ _fork_ s≡thinxs' t≡thinxt'
--              , cong₂ (λ a b -> _fork_ <$> a ⊛ b) checkxs≡s' checkxt≡t' )
--   ... | inj₂ (ps , s≡ps+ix , checkxs≡no )  | _
--       = inj₂ (left t ∷ ps , cong (λ s -> s fork t) s≡ps+ix
--              , cong (λ a -> _fork_ <$> a ⊛ check x t) checkxs≡no )
--   ... | _                                  | inj₂ (ps , s≡ps+ix , checkxs≡no )
--       = inj₂ (right s ∷ ps , cong (λ t -> s fork t) s≡ps+ix
--              , trans (cong (λ a -> _fork_ <$> check x s ⊛ a) checkxs≡no) (lemma (_fork_ <$> check x s)))
--     where
--       lemma : ∀ {a b : Set} {y : b} (x : Maybe a) -> maybe (λ _ → y) y x ≡ y
--       lemma (just x') = refl
--       lemma nothing = refl
--   check-prop x (function fn ts) with check-props x ts fn
--   … | inj₁ (t' , t=thinxt' , checkxt=t') rewrite checkxt=t' = inj₁ (function fn t' , cong (function fn) t=thinxt' , refl)
--   … | inj₂ (ps , t=ps+ix , checkxt=no) rewrite checkxt=no = inj₂ (ps , t=ps+ix , refl)

-- -- data SizedTerm (n : ℕ) : ℕ → Set where
-- --   i : (x : Fin n) -> SizedTerm n (suc zero)
-- --   leaf : SizedTerm n (suc zero)
-- --   _fork_ : (s : ∃ (SizedTerm n)) (t : ∃ (SizedTerm n)) -> SizedTerm n (suc (proj₁ s + proj₁ t))
-- --   function : FunctionName → ∀ {f} → (ts : Vec (∃ (SizedTerm n)) f) → SizedTerm n (suc (Data.Vec.sum (Data.Vec.map proj₁ ts)))

-- -- data SizedStep (n : ℕ) : Set where
-- --   left : ∃ (SizedTerm n) -> SizedStep n
-- --   right : ∃ (SizedTerm n) -> SizedStep n
-- --   function : FunctionName → ∀ {L} → Vec (∃ (SizedTerm n)) L → ∀ {R} → Vec (∃ (SizedTerm n)) R → SizedStep n

-- -- mutual

-- --   toSizedTerm : ∀ {n} → Term n → ∃ (SizedTerm n)
-- --   toSizedTerm (i x) = suc zero , i x
-- --   toSizedTerm leaf = suc zero , leaf
-- --   toSizedTerm (l fork r) with toSizedTerm l | toSizedTerm r
-- --   … | L , sl | R , sr = (suc (L + R)) , ((L , sl) fork (R , sr))
-- --   toSizedTerm (function fn ts) with toSizedTerms ts
-- --   … | sts = suc (Data.Vec.sum (Data.Vec.map proj₁ sts)) , SizedTerm.function fn sts

-- --   fromSizedTerm : ∀ {n} → ∃ (SizedTerm n) → Term n
-- --   fromSizedTerm (_ , i x) = i x
-- --   fromSizedTerm (_ , leaf) = leaf
-- --   fromSizedTerm (_ , (_fork_ t₁ t₂)) = (fromSizedTerm t₁ fork fromSizedTerm t₂)
-- --   fromSizedTerm (_ , function fn ts) = function fn (fromSizedTerms ts)

-- --   toSizedTerms : ∀ {n N} → Vec (Term n) N → Vec (∃ (SizedTerm n)) N
-- --   toSizedTerms [] = []
-- --   toSizedTerms (t ∷ ts) = toSizedTerm t ∷ toSizedTerms ts

-- --   fromSizedTerms : ∀ {n N} → Vec (∃ (SizedTerm n)) N → Vec (Term n) N
-- --   fromSizedTerms [] = []
-- --   fromSizedTerms (t ∷ ts) = fromSizedTerm t ∷ fromSizedTerms ts

-- -- mutual

-- --   isoSizedTerm : ∀ {n} → (st : ∃ (SizedTerm n)) → st ≡ toSizedTerm (fromSizedTerm st)
-- --   isoSizedTerm (._ , i x) = refl
-- --   isoSizedTerm (._ , leaf) = refl
-- --   isoSizedTerm (.(suc (proj₁ s + proj₁ t)) , (s fork t)) rewrite sym (isoSizedTerm s) | sym (isoSizedTerm t) = refl
-- --   isoSizedTerm (._ , function x ts) rewrite sym (isoSizedTerms ts) = refl

-- --   isoSizedTerms : ∀ {n N} → (st : Vec (∃ (SizedTerm n)) N) → st ≡ toSizedTerms (fromSizedTerms st)
-- --   isoSizedTerms [] = refl
-- --   isoSizedTerms (t ∷ ts) rewrite sym (isoSizedTerm t) | sym (isoSizedTerms ts) = refl

-- -- mutual

-- --   isoTerm : ∀ {n} → (t : Term n) → t ≡ fromSizedTerm (toSizedTerm t)
-- --   isoTerm (i x) = refl
-- --   isoTerm leaf = refl
-- --   isoTerm (s fork t) rewrite sym (isoTerm s) | sym (isoTerm t) = refl
-- --   isoTerm (function fn ts) rewrite sym (isoTerms ts) = refl

-- --   isoTerms : ∀ {n N} → (t : Vec (Term n) N) → t ≡ fromSizedTerms (toSizedTerms t)
-- --   isoTerms [] = refl
-- --   isoTerms (t ∷ ts) rewrite sym (isoTerm t) | sym (isoTerms ts) = refl

-- -- toSizedStep : ∀ {n} → Step n → SizedStep n
-- -- toSizedStep (left r) = left (toSizedTerm r)
-- -- toSizedStep (right l) = right (toSizedTerm l)
-- -- toSizedStep (function fn ls rs) = function fn (toSizedTerms ls) (toSizedTerms rs)

-- -- fromSizedStep : ∀ {n} → SizedStep n → Step n
-- -- fromSizedStep (left r) = left (fromSizedTerm r)
-- -- fromSizedStep (right l) = right (fromSizedTerm l)
-- -- fromSizedStep (function fn ls rs) = function fn (fromSizedTerms ls) (fromSizedTerms rs)

-- -- isoSizedStep : ∀ {n} → (ss : SizedStep n) → ss ≡ toSizedStep (fromSizedStep ss)
-- -- isoSizedStep (left r) rewrite sym (isoSizedTerm r) = refl
-- -- isoSizedStep (right l) rewrite sym (isoSizedTerm l) = refl
-- -- isoSizedStep (function fn ls rs) rewrite sym (isoSizedTerms ls) | sym (isoSizedTerms rs) = refl

-- -- isoStep : ∀ {n} → (s : Step n) → s ≡ fromSizedStep (toSizedStep s)
-- -- isoStep (left r) rewrite sym (isoTerm r) = refl
-- -- isoStep (right l) rewrite sym (isoTerm l) = refl
-- -- isoStep (function fn ls rs) rewrite sym (isoTerms ls) | sym (isoTerms rs) = refl

-- -- toSizedSteps : ∀ {n} → List (Step n) → List (SizedStep n)
-- -- toSizedSteps [] = []
-- -- toSizedSteps (s ∷ ss) = toSizedStep s ∷ toSizedSteps ss

-- -- fromSizedSteps : ∀ {n} → List (SizedStep n) → List (Step n)
-- -- fromSizedSteps [] = []
-- -- fromSizedSteps (s ∷ ss) = fromSizedStep s ∷ fromSizedSteps ss

-- -- isoSizedSteps : ∀ {n} → (ss : List (SizedStep n)) → ss ≡ toSizedSteps (fromSizedSteps ss)
-- -- isoSizedSteps [] = refl
-- -- isoSizedSteps (s ∷ ss) rewrite sym (isoSizedStep s) | sym (isoSizedSteps ss) = refl

-- -- isoSteps : ∀ {n} → (s : List (Step n)) → s ≡ fromSizedSteps (toSizedSteps s)
-- -- isoSteps [] = refl
-- -- isoSteps (s ∷ ss) rewrite sym (isoStep s) | sym (isoSteps ss) = refl

-- -- _Sized⊹_ : ∀ {n} (ps : List (SizedStep n)) (t : ∃ (SizedTerm n)) -> ∃ (SizedTerm n)
-- -- [] Sized⊹ t = t
-- -- (left r ∷ ps) Sized⊹ t = _ , (ps Sized⊹ t) SizedTerm.fork r
-- -- (right l ∷ ps) Sized⊹ t = _ , l SizedTerm.fork (ps Sized⊹ t)
-- -- (function fn ls rs ∷ ps) Sized⊹ t = _ , function fn (ls ++V (ps Sized⊹ t) ∷ rs)

-- -- fromSizedTerms-commute : ∀ {n} {L R} → (ls : Vec (∃ (SizedTerm n)) L) (rs : Vec (∃ (SizedTerm n)) R) → fromSizedTerms (ls ++V rs) ≡ fromSizedTerms ls ++V fromSizedTerms rs
-- -- fromSizedTerms-commute [] rs = refl
-- -- fromSizedTerms-commute (l ∷ ls) rs rewrite fromSizedTerms-commute ls rs = refl

-- -- toSizedTerms-commute : ∀ {n} {L R} → (ls : Vec (Term n) L) (rs : Vec (Term n) R) → toSizedTerms (ls ++V rs) ≡ toSizedTerms ls ++V toSizedTerms rs
-- -- toSizedTerms-commute [] rs = refl
-- -- toSizedTerms-commute (l ∷ ls) rs rewrite toSizedTerms-commute ls rs = refl

-- -- isoSized⊹ : ∀ {n} (ps : List (SizedStep n)) (t : ∃ (SizedTerm n)) → fromSizedTerm (ps Sized⊹ t) ≡ fromSizedSteps ps ⊹ fromSizedTerm t
-- -- isoSized⊹ [] t = refl
-- -- isoSized⊹ (left r ∷ ps) t rewrite isoSized⊹ ps t = refl
-- -- isoSized⊹ (right l ∷ ps) t rewrite isoSized⊹ ps t = refl
-- -- isoSized⊹ (function fn ls rs ∷ ps) t rewrite sym (isoSized⊹ ps t) | fromSizedTerms-commute ls ((ps Sized⊹ t) ∷ rs) = refl

-- -- iso⊹ : ∀ {n} (ps : List (Step n)) (t : Term n) → toSizedTerm (ps ⊹ t) ≡ toSizedSteps ps Sized⊹ toSizedTerm t
-- -- iso⊹ [] t = refl
-- -- iso⊹ (left r ∷ ps) t rewrite iso⊹ ps t = refl
-- -- iso⊹ (right l ∷ ps) t rewrite iso⊹ ps t = refl
-- -- iso⊹ (function fn ls rs ∷ ps) t rewrite sym (iso⊹ ps t) | toSizedTerms-commute ls ((ps ⊹ t) ∷ rs) = refl

-- -- import Data.Vec.Properties
-- -- import Relation.Binary.PropositionalEquality as PE
-- -- open Data.Vec.Properties.UsingVectorEquality (PE.setoid ℕ)
-- -- import Data.Vec.Equality
-- -- open Data.Vec.Equality.PropositionalEquality using (to-≡)

-- -- -- some equivalences needed to adapt Tactic.Nat to the standard library
-- -- module EquivalenceOf≤ where
-- --   open import Agda.Builtin.Equality
-- --   open import Agda.Builtin.Nat

-- --   open import Data.Nat using (less-than-or-equal) renaming (_≤_ to _≤s_)
-- --   open import Data.Nat.Properties using (≤⇒≤″; ≤″⇒≤)
-- --   open import Prelude using (diff; id) renaming (_≤_ to _≤p_)

-- --   open import Tactic.Nat.Generic (quote _≤p_) (quote Function.id) (quote Function.id) using (by)

-- --   ≤p→≤s : ∀ {a b} → a ≤p b → a ≤s b
-- --   ≤p→≤s (diff k b₊₁≡k₊₁+a) = ≤″⇒≤ (less-than-or-equal {k = k} (by b₊₁≡k₊₁+a))

-- --   ≤s→≤p : ∀ {a b} → a ≤s b → a ≤p b
-- --   ≤s→≤p a≤sb with ≤⇒≤″ a≤sb
-- --   ≤s→≤p _ | less-than-or-equal {k = k} a+k≡b = diff k (by a+k≡b)

-- -- module _ where
-- --   open EquivalenceOf≤
-- --   open import Data.Nat
-- --   open import Tactic.Nat.Generic (quote Data.Nat._≤_) (quote ≤s→≤p) (quote ≤p→≤s) public

-- -- growingSize : ∀ {m} (st : ∃ (SizedTerm m)) → (sp : SizedStep m) (sps : List (SizedStep m)) → proj₁ ((sp ∷ sps) Sized⊹ st) > proj₁ st
-- -- growingSize st (left r) [] = auto
-- -- growingSize st (right l) [] = auto
-- -- growingSize {m} st (function fn ls rs) [] rewrite to-≡ (map-++-commute proj₁ ls {ys = st ∷ rs}) | Data.Vec.Properties.sum-++-commute (mapV proj₁ ls) {ys = mapV proj₁ (st ∷ rs)} = auto
-- -- growingSize st (left x) (p₂ ∷ ps) = by (growingSize st p₂ ps)
-- -- growingSize st (right x) (p₂ ∷ ps) = by (growingSize st p₂ ps)
-- -- growingSize st (function fn ls rs) (p₂ ∷ ps) rewrite to-≡ (map-++-commute proj₁ ls {ys = ((p₂ ∷ ps) Sized⊹ st) ∷ rs}) | Data.Vec.Properties.sum-++-commute (mapV proj₁ ls) {ys = mapV proj₁ (((p₂ ∷ ps) Sized⊹ st) ∷ rs)} = by (growingSize st p₂ ps)

-- -- No-Cycle : ∀{m} (t : Term m) ps -> (eq : t ≡ ps ⊹ t) → ps ≡ []
-- -- No-Cycle t [] eq = refl
-- -- No-Cycle t (p ∷ ps) eq = refute (subst (λ v → v > proj₁ (toSizedTerm t)) (sym (trans same iso)) growth) where
-- --   same : proj₁ (toSizedTerm t) ≡ proj₁ (toSizedTerm ((p ∷ ps) ⊹ t))
-- --   growth : proj₁ ((toSizedStep p ∷ toSizedSteps ps) Sized⊹ toSizedTerm t) > proj₁ (toSizedTerm t)
-- --   iso : proj₁ (toSizedTerm ((p ∷ ps) ⊹ t)) ≡ proj₁ ((toSizedStep p ∷ toSizedSteps ps) Sized⊹ toSizedTerm t)
-- --   growth = growingSize (toSizedTerm t) (toSizedStep p) (toSizedSteps ps)
-- --   same = cong (proj₁ ∘ toSizedTerm) eq
-- --   iso = cong proj₁ (iso⊹ (p ∷ ps) t)

-- -- module Step2 where
-- --   fact : ∀{m} (x : Fin m) p ps -> Nothing (Unifies (i x) ((p ∷ ps) ⊹ i x))
-- --   fact x p ps f r with No-Cycle (f x) (f ◃S (p ∷ ps)) (trans r (StepM.fact2 f (i x) (p ∷ ps)))
-- --   ... | ()

-- -- NothingStep : ∀ {l} (x : Fin (suc l)) (t : Term (suc l)) →
-- --               i x ≢ t →
-- --               (ps : List (Step (suc l))) →
-- --               t ≡ (ps ⊹ i x) →
-- --               ∀ {n} (f : Fin (suc l) → Term n) → f x ≢ (f ◃ t)
-- -- NothingStep {l} x t ix≢t ps r = No-Unifier
-- --   where
-- --     No-Unifier : {n : ℕ} (f : Fin (suc l) → Term n) → f x ≢ f ◃ t
-- --     No-Unifier f fx≡f◃t = ix≢t (sym (trans r (cong (λ ps -> ps ⊹ i x) ps≡[])))
-- --           where
-- --             ps≡[] : ps ≡ []
-- --             ps≡[] = map-[] f ps (No-Cycle (f x) (f ◃S ps)
-- --                   (begin f x             ≡⟨ fx≡f◃t ⟩
-- --                          f ◃ t           ≡⟨ cong (f ◃_) r ⟩
-- --                          f ◃ (ps ⊹ i x)  ≡⟨ StepM.fact2 f (i x) ps ⟩
-- --                          (f ◃S ps) ⊹ f x ∎))


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

module Data.List.Permute where

open import Prelude
open import Data.Nat
open import Data.Nat.Properties using (_≤ᴮ_)

infixr 5 _∹_∷_
data Premuted {a} (A : Type a) : Type a where
 [] : Premuted A
 _∹_∷_ : ℕ → A → Premuted A → Premuted A

mutual
  merge : Premuted A → Premuted A → Premuted A
  merge [] = id
  merge (n ∹ x ∷ xs) = mergeˡ n x (merge xs)

  mergeˡ : ℕ → A → (Premuted A → Premuted A) → Premuted A → Premuted A
  mergeˡ i x xs [] = i ∹ x ∷ xs []
  mergeˡ i x xs (j ∹ y ∷ ys) = merge⁺ i x xs j y ys (i ≤ᴮ j)

  merge⁺ : ℕ → A → (Premuted A → Premuted A) → ℕ → A → Premuted A → Bool → Premuted A
  merge⁺ i x xs j y ys true  = i ∹ x ∷ xs ((j ∸ i) ∹ y ∷ ys)
  merge⁺ i x xs j y ys false = j ∹ y ∷ mergeˡ ((i ∸ j) ∸ 1) x xs ys

merge-idʳ : (xs : Premuted A) → merge xs [] ≡ xs
merge-idʳ [] = refl
merge-idʳ (i ∹ x ∷ xs) = cong (i ∹ x ∷_) (merge-idʳ xs)

open import Algebra

≤≡-trans : ∀ x y z → (x ≤ᴮ y) ≡ true → (y ≤ᴮ z) ≡ true → (x ≤ᴮ z) ≡ true
≤≡-trans zero y z p₁ p₂ = refl
≤≡-trans (suc x) zero z p₁ p₂ = ⊥-elim (subst (bool ⊤ ⊥) p₁ tt)
≤≡-trans (suc x) (suc y) zero p₁ p₂ = ⊥-elim (subst (bool ⊤ ⊥) p₂ tt)
≤≡-trans (suc x) (suc y) (suc z) p₁ p₂ = ≤≡-trans x y z p₁ p₂

<≡-trans : ∀ x y z → (x ≤ᴮ y) ≡ false → (y ≤ᴮ z) ≡ false → (x ≤ᴮ z) ≡ false
<≡-trans zero y z p₁ p₂ = ⊥-elim (subst (bool ⊥ ⊤) p₁ tt)
<≡-trans (suc x) zero z p₁ p₂ = ⊥-elim (subst (bool ⊥ ⊤) p₂ tt)
<≡-trans (suc x) (suc y) zero p₁ p₂ = p₂
<≡-trans (suc x) (suc y) (suc z) p₁ p₂ = <≡-trans x y z p₁ p₂

≤≡-sub : ∀ i j k → (j ≤ᴮ k) ≡ true → (j ∸ i ≤ᴮ k ∸ i) ≡ true
≤≡-sub zero j k p = p
≤≡-sub (suc i) zero k p = refl
≤≡-sub (suc i) (suc j) zero p = ⊥-elim (subst (bool ⊤ ⊥) p tt)
≤≡-sub (suc i) (suc j) (suc k) p = ≤≡-sub i j k p

≥≡-sub : ∀ i j k → (j ≤ᴮ k) ≡ false → (i ≤ᴮ k) ≡ true → (j ∸ i ≤ᴮ k ∸ i) ≡ false
≥≡-sub i zero k p _ = ⊥-elim (subst (bool ⊥ ⊤) p tt)
≥≡-sub zero (suc j) k p _ = p
≥≡-sub (suc i) (suc j) zero p p₂ = ⊥-elim (subst (bool ⊤ ⊥) p₂ tt)
≥≡-sub (suc i) (suc j) (suc k) p p₂ = ≥≡-sub i j k p p₂

<≡-sub : ∀ i j k → (i ≤ᴮ j) ≡ false → (j ≤ᴮ k) ≡ false → (i ∸ k ∸ 1 ≤ᴮ j ∸ k ∸ 1) ≡ false
<≡-sub zero j k p _ = ⊥-elim (subst (bool ⊥ ⊤) p tt)
<≡-sub (suc i) zero k p p₂ = ⊥-elim (subst (bool ⊥ ⊤) p₂ tt)
<≡-sub (suc i) (suc j) zero p p₂ = p
<≡-sub (suc i) (suc j) (suc k) p p₂ = <≡-sub i j k p p₂

>≡-sub : ∀ i j k → (i ≤ᴮ j) ≡ true → (j ≤ᴮ k) ≡ false → (i ≤ᴮ k) ≡ false → (i ∸ k ∸ 1 ≤ᴮ j ∸ k ∸ 1) ≡ true
>≡-sub i zero    k p₁ p₂ p₃ = ⊥-elim (subst (bool ⊥ ⊤) p₂ tt)
>≡-sub zero (suc j) k p₁ p₂ p₃ = ⊥-elim (subst (bool ⊥ ⊤) p₃ tt)
>≡-sub (suc i) (suc j) zero p₁ p₂ p₃ = p₁
>≡-sub (suc i) (suc j) (suc k) p₁ p₂ p₃ = >≡-sub i j k p₁ p₂ p₃

zero-sub : ∀ n → zero ∸ n ≡ zero
zero-sub zero = refl
zero-sub (suc n) = refl

≤-sub-id : ∀ i j k → (i ≤ᴮ j) ≡ true → k ∸ i ∸ (j ∸ i) ≡ k ∸ j
≤-sub-id zero j k p = refl
≤-sub-id (suc i) zero k p = ⊥-elim (subst (bool ⊤ ⊥) p tt)
≤-sub-id (suc i) (suc j) zero p = zero-sub (j ∸ i)
≤-sub-id (suc i) (suc j) (suc k) p = ≤-sub-id i j k p

lemma₁ : ∀ i j k → (j ≤ᴮ k) ≡ false → i ∸ k ∸ 1 ∸ (j ∸ k ∸ 1) ∸ 1 ≡ i ∸ j ∸ 1
lemma₁ zero j k _ = cong (λ zk → zk ∸ 1 ∸ (j ∸ k ∸ 1) ∸ 1) (zero-sub k) ; cong (_∸ 1) (zero-sub (j ∸ k ∸ 1)) ; sym (cong (_∸ 1) (zero-sub j))
lemma₁ (suc i) zero k p₂ = ⊥-elim (subst (bool ⊥ ⊤) p₂ tt)
lemma₁ (suc i) (suc j) zero p₂ = refl
lemma₁ (suc i) (suc j) (suc k) p₂ = lemma₁ i j k p₂

lemma₂ : ∀ i j k → (i ≤ᴮ j) ≡ true → (j ≤ᴮ k) ≡ false → (i ≤ᴮ k) ≡ false → j ∸ i ≡ j ∸ k ∸ 1 ∸ (i ∸ k ∸ 1)
lemma₂ i zero    k p₁ p₂ p₃ = ⊥-elim (subst (bool ⊥ ⊤) p₂ tt)
lemma₂ zero (suc j) k p₁ p₂ p₃ = ⊥-elim (subst (bool ⊥ ⊤) p₃ tt)
lemma₂ (suc i) (suc j) zero p₁ p₂ p₃ = refl
lemma₂ (suc i) (suc j) (suc k) p₁ p₂ p₃ = lemma₂ i j k p₁ p₂ p₃

{-# TERMINATING #-}
merge-assoc : Associative (merge {A = A})
merge-assoc [] ys zs = refl
merge-assoc (i ∹ x ∷ xs) [] zs = cong (flip merge zs) (merge-idʳ (i ∹ x ∷ xs))
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) [] = merge-idʳ (merge (i ∹ x ∷ xs) (j ∹ y ∷ ys)) ; sym (cong (merge (i ∹ x ∷ xs)) (merge-idʳ (j ∹ y ∷ ys)))
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) with merge-assoc xs (j ∸ i ∹ y ∷ ys) (k ∸ i ∹ z ∷ zs) | merge-assoc (i ∸ k ∸ 1 ∹ x ∷ xs) (j ∸ k ∸ 1 ∹ y ∷ ys) zs | (merge-assoc (i ∸ j ∸ 1 ∹ x ∷ xs) ys (k ∸ j ∹ z ∷ zs)) | i ≤ᴮ j | inspect (i ≤ᴮ_) j | j ≤ᴮ k | inspect (j ≤ᴮ_) k
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | r | _ | _ | true  | 〖 ij 〗 | true  | 〖 jk 〗 = cong (merge⁺ i x (merge (merge xs (j ∸ i ∹ y ∷ ys))) k z zs) (≤≡-trans i j k ij jk) ;
                                                                                cong (i ∹ x ∷_) (r ;
                                                                                cong (merge xs) (cong (merge⁺ (j ∸ i) y (merge ys) (k ∸ i) z zs) (≤≡-sub i j k jk) ; cong (λ kij → j ∸ i ∹ y ∷ merge ys (kij ∹ z ∷ zs)) (≤-sub-id i j k ij))) ;
                                                                                cong (merge⁺ i x (merge xs) j y (merge ys (k ∸ j ∹ z ∷ zs))) (sym ij)
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | _ | r | _ | false | 〖 ij 〗 | false | 〖 jk 〗 = cong (merge⁺ j y (merge (mergeˡ (i ∸ j ∸ 1) x (merge xs) ys)) k z zs ) jk ;
                                                                                cong (k ∹ z ∷_) (cong (λ s → mergeˡ (j ∸ k ∸ 1) y (merge (mergeˡ s x (merge xs) ys)) zs) (sym (lemma₁ i j k jk)) ;
                                                                                cong (λ s → merge (merge⁺ (i ∸ k ∸ 1) x (merge xs) (j ∸ k ∸ 1) y ys s) zs) (sym (<≡-sub i j k ij jk)) ;
                                                                                r) ;
                                                                                cong (merge⁺ i x (merge xs) k z (mergeˡ (j ∸ k ∸ 1) y (merge ys) zs)) (sym (<≡-trans i j k ij jk))
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | _ | _ | r | false | 〖 ij 〗 | true  | 〖 jk 〗 = cong (merge⁺ j y (merge (mergeˡ (i ∸ j ∸ 1) x (merge xs) ys)) k z zs) jk ;
                                                                                cong (j ∹ y ∷_) r ;
                                                                                cong (merge⁺ i x (merge xs) j y (merge ys (k ∸ j ∹ z ∷ zs))) (sym ij)
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | _ | _ | _ | true  | ij | false | jk with i ≤ᴮ k | inspect (i ≤ᴮ_) k
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | _ | r | _ | true | 〖 ij 〗 | false | 〖 jk 〗 | false | 〖 ik 〗 = cong (k ∹ z ∷_) ((cong (λ s → mergeˡ (i ∸ k ∸ 1) x (merge (merge xs (s ∹ y ∷ ys))) zs) (lemma₂ i j k ij jk ik) ;
                                                                                cong (λ c → merge (merge⁺ (i ∸ k ∸ 1) x (merge xs) (j ∸ k ∸ 1) y ys c) zs) (sym (>≡-sub i j k ij jk ik ))) ;
                                                                                r )
merge-assoc (i ∹ x ∷ xs) (j ∹ y ∷ ys) (k ∹ z ∷ zs) | r | _ | _ | true | 〖 ij 〗 | false | 〖 jk 〗 | true  | 〖 ik 〗 = cong (i ∹ x ∷_) (r ;
                                                                                cong (merge xs) (cong (merge⁺ (j ∸ i) y (merge ys) (k ∸ i) z zs) (≥≡-sub i j k jk ik) ;
                                                                                cong (λ s → k ∸ i ∹ z ∷ mergeˡ s y (merge ys) zs) (cong (_∸ 1) (≤-sub-id i k j ik)) ))

open import Data.List

index : List ℕ → List A → List (Premuted A)
index _  []       = []
index [] (x ∷ xs) = (0 ∹ x ∷ []) ∷ index [] xs
index (i ∷ is) (x ∷ xs) = (i ∹ x ∷ []) ∷ index is xs

unindex : Premuted A → List A
unindex [] = []
unindex (_ ∹ x ∷ xs) = x ∷ unindex xs

open import TreeFold

shuffle : List ℕ → List A → List A
shuffle is = unindex ∘ treeFold merge [] ∘ index is

open import Data.List.Syntax

e : List ℕ
e = shuffle [ 0 , 1 , 0 ] [ 1 , 2 , 3 ]

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text: module Categories.Monoidal.Closed where

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue755 where

open import Common.Prelude renaming (Nat to ℕ)
open import Common.Equality

abstract
  foo : ℕ → ℕ
  foo x = zero

bar : foo zero ≡ foo (suc zero) → foo zero ≡ foo (suc zero)
bar refl = refl
-- 0 != 1 of type ℕ
-- when checking that the pattern refl has type
-- foo zero ≡ foo (suc zero)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Empty
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Group
open import lib.types.Nat
open import lib.types.List
open import lib.types.Word
open import lib.types.SetQuotient
open import lib.groups.Homomorphism

module lib.groups.FreeGroup {i} where

-- [qwr-sym] is not needed, but it seems more principled to
-- make [QuotWordRel] an equivalence relation.
data QuotWordRel {A : Type i} : Word A → Word A → Type i where
  qwr-refl : ∀ {l₁ l₂} → l₁ == l₂ → QuotWordRel l₁ l₂
  qwr-trans : ∀ {l₁ l₂ l₃} → QuotWordRel l₁ l₂ → QuotWordRel l₂ l₃ → QuotWordRel l₁ l₃
  qwr-sym : ∀ {l₁ l₂} → QuotWordRel l₁ l₂ → QuotWordRel l₂ l₁
  qwr-cons : ∀ x {l₁ l₂} → QuotWordRel l₁ l₂ → QuotWordRel (x :: l₁) (x :: l₂)
  qwr-flip : ∀ x₁ l → QuotWordRel (x₁ :: flip x₁ :: l) l

-- The quotient
QuotWord : Type i → Type i
QuotWord A = SetQuot (QuotWordRel {A})

module _ {A : Type i} where

  qw[_] : Word A → QuotWord A
  qw[_] = q[_]

  module QuotWordElim {k} {P : QuotWord A → Type k}
    {{_ : {x : QuotWord A} → is-set (P x)}} (incl* : (a : Word A) → P qw[ a ])
    (rel* : ∀ {a₁ a₂} (r : QuotWordRel a₁ a₂) → incl* a₁ == incl* a₂ [ P ↓ quot-rel r ])
    = SetQuotElim incl* rel*
  open QuotWordElim public renaming (f to QuotWord-elim) hiding (quot-rel-β)

  module QuotWordRec {k} {B : Type k} {{_ : is-set B}} (incl* : Word A → B)
    (rel* : ∀ {a₁ a₂} (r : QuotWordRel a₁ a₂) → incl* a₁ == incl* a₂)
    = SetQuotRec incl* rel*
  open QuotWordRec public renaming (f to QuotWord-rec)

module _ (A : Type i) where
  private
    abstract
      QuotWordRel-cong-++-l :
        ∀ {l₁ l₁'} → QuotWordRel {A} l₁ l₁'
        → (l₂ : Word A)
        → QuotWordRel (l₁ ++ l₂) (l₁' ++ l₂)
      QuotWordRel-cong-++-l (qwr-refl idp) l₂ = qwr-refl idp
      QuotWordRel-cong-++-l (qwr-trans qwr₁ qwr₂) l₂ = qwr-trans (QuotWordRel-cong-++-l qwr₁ l₂) (QuotWordRel-cong-++-l qwr₂ l₂)
      QuotWordRel-cong-++-l (qwr-sym qwr) l₂ = qwr-sym (QuotWordRel-cong-++-l qwr l₂)
      QuotWordRel-cong-++-l (qwr-cons x qwr₁) l₂ = qwr-cons x (QuotWordRel-cong-++-l qwr₁ l₂)
      QuotWordRel-cong-++-l (qwr-flip x₁ l₁) l₂ = qwr-flip x₁ (l₁ ++ l₂)

      QuotWordRel-cong-++-r :
        ∀ (l₁ : Word A)
        → ∀ {l₂ l₂'} → QuotWordRel l₂ l₂'
        → QuotWordRel (l₁ ++ l₂) (l₁ ++ l₂')
      QuotWordRel-cong-++-r nil qwr₂ = qwr₂
      QuotWordRel-cong-++-r (x :: l₁) qwr₂ = qwr-cons x (QuotWordRel-cong-++-r l₁ qwr₂)

    infixl 80 _⊞_
    _⊞_ : QuotWord A → QuotWord A → QuotWord A
    _⊞_ = QuotWord-rec
      (λ l₁ → QuotWord-rec (λ l₂ → qw[ l₁ ++ l₂ ])
        (λ r → quot-rel $ QuotWordRel-cong-++-r l₁ r))
      (λ {l₁} {l₁'} r → λ= $ QuotWord-elim
        (λ l₂ → quot-rel $ QuotWordRel-cong-++-l r l₂)
        (λ _ → prop-has-all-paths-↓))

    abstract
      QuotWordRel-cong-flip : ∀ {l₁ l₂}
        → QuotWordRel {A} l₁ l₂ → QuotWordRel (Word-flip l₁) (Word-flip l₂)
      QuotWordRel-cong-flip (qwr-refl idp) = qwr-refl idp
      QuotWordRel-cong-flip (qwr-trans qwr₁ qwr₂) = qwr-trans (QuotWordRel-cong-flip qwr₁) (QuotWordRel-cong-flip qwr₂)
      QuotWordRel-cong-flip (qwr-sym qwr) = qwr-sym (QuotWordRel-cong-flip qwr)
      QuotWordRel-cong-flip (qwr-cons x qwr₁) = qwr-cons (flip x) (QuotWordRel-cong-flip qwr₁)
      QuotWordRel-cong-flip (qwr-flip (inl x) l) = qwr-flip (inr x) (Word-flip l)
      QuotWordRel-cong-flip (qwr-flip (inr x) l) = qwr-flip (inl x) (Word-flip l)

      QuotWordRel-cong-reverse : ∀ {l₁ l₂}
        → QuotWordRel {A} l₁ l₂ → QuotWordRel (reverse l₁) (reverse l₂)
      QuotWordRel-cong-reverse (qwr-refl x) = qwr-refl (ap reverse x)
      QuotWordRel-cong-reverse (qwr-trans qwr qwr₁) = qwr-trans (QuotWordRel-cong-reverse qwr) (QuotWordRel-cong-reverse qwr₁)
      QuotWordRel-cong-reverse (qwr-sym qwr) = qwr-sym (QuotWordRel-cong-reverse qwr)
      QuotWordRel-cong-reverse (qwr-cons x qwr) = QuotWordRel-cong-++-l (QuotWordRel-cong-reverse qwr) (x :: nil)
      QuotWordRel-cong-reverse (qwr-flip (inl x) l) =
        qwr-trans (qwr-refl (++-assoc (reverse l) (inr x :: nil) (inl x :: nil))) $
        qwr-trans (QuotWordRel-cong-++-r (reverse l) (qwr-flip (inr x) nil)) $
        qwr-refl (++-unit-r (reverse l))
      QuotWordRel-cong-reverse (qwr-flip (inr x) l) =
        qwr-trans (qwr-refl (++-assoc (reverse l) (inl x :: nil) (inr x :: nil))) $
        qwr-trans (QuotWordRel-cong-++-r (reverse l) (qwr-flip (inl x) nil)) $
        qwr-refl (++-unit-r (reverse l))

    ⊟ : QuotWord A → QuotWord A
    ⊟ = QuotWord-rec (qw[_] ∘ reverse ∘ Word-flip)
      (λ r → quot-rel $ QuotWordRel-cong-reverse $ QuotWordRel-cong-flip r)

    ⊞-unit : QuotWord A
    ⊞-unit = qw[ nil ]

    abstract
      ⊞-unit-l : ∀ g → ⊞-unit ⊞ g == g
      ⊞-unit-l = QuotWord-elim
        (λ _ → idp)
        (λ _ → prop-has-all-paths-↓)

      ⊞-assoc : ∀ g₁ g₂ g₃ → (g₁ ⊞ g₂) ⊞ g₃ == g₁ ⊞ (g₂ ⊞ g₃)
      ⊞-assoc = QuotWord-elim
        (λ l₁ → QuotWord-elim
          (λ l₂ → QuotWord-elim
            (λ l₃ → ap qw[_] $ ++-assoc l₁ l₂ l₃)
            (λ _ → prop-has-all-paths-↓))
          (λ _ → prop-has-all-paths-↓))
        (λ _ → prop-has-all-paths-↓)

      Word-inv-l : ∀ l → QuotWordRel {A} (reverse (Word-flip l) ++ l) nil
      Word-inv-l nil = qwr-refl idp
      Word-inv-l (inl x :: l) =
        qwr-trans (qwr-refl (++-assoc (reverse (Word-flip l)) (inr x :: nil) (inl x :: l))) $
        qwr-trans (QuotWordRel-cong-++-r (reverse (Word-flip l)) (qwr-flip (inr x) l)) $
        Word-inv-l l
      Word-inv-l (inr x :: l) =
        qwr-trans (qwr-refl (++-assoc (reverse (Word-flip l)) (inl x :: nil) (inr x :: l))) $
        qwr-trans (QuotWordRel-cong-++-r (reverse (Word-flip l)) (qwr-flip (inl x) l)) $
        Word-inv-l l

      ⊟-inv-l : ∀ g → (⊟ g) ⊞ g == ⊞-unit
      ⊟-inv-l = QuotWord-elim
        (λ l → quot-rel (Word-inv-l l))
        (λ _ → prop-has-all-paths-↓)

  QuotWord-group-structure : GroupStructure (QuotWord A)
  QuotWord-group-structure = record
    { ident = ⊞-unit
    ; inv = ⊟
    ; comp = _⊞_
    ; unit-l = ⊞-unit-l
    ; assoc = ⊞-assoc
    ; inv-l = ⊟-inv-l
    }

  FreeGroup : Group i
  FreeGroup = group _ QuotWord-group-structure

  module FreeGroup = Group FreeGroup

-- freeness
module _ {A : Type i} {j} (G : Group j) where

  private
    module G = Group G

    abstract
      Word-extendᴳ-emap : ∀ f {l₁ l₂}
        → QuotWordRel {A} l₁ l₂
        → Word-extendᴳ G f l₁ == Word-extendᴳ G f l₂
      Word-extendᴳ-emap f (qwr-refl idp) = idp
      Word-extendᴳ-emap f (qwr-trans qwr qwr₁) = (Word-extendᴳ-emap f qwr) ∙ (Word-extendᴳ-emap f qwr₁)
      Word-extendᴳ-emap f (qwr-sym qwr) = ! (Word-extendᴳ-emap f qwr)
      Word-extendᴳ-emap f (qwr-cons x qwr) = ap (G.comp (PlusMinus-extendᴳ G f x)) (Word-extendᴳ-emap f qwr)
      Word-extendᴳ-emap f (qwr-flip (inl x) l) =
          ! (G.assoc (f x) (G.inv (f x)) (Word-extendᴳ G f l))
        ∙ ap (λ g → G.comp g (Word-extendᴳ G f l)) (G.inv-r (f x)) ∙ G.unit-l _
      Word-extendᴳ-emap f (qwr-flip (inr x) l) =
          ! (G.assoc (G.inv (f x)) (f x) (Word-extendᴳ G f l))
        ∙ ap (λ g → G.comp g (Word-extendᴳ G f l)) (G.inv-l (f x)) ∙ G.unit-l _

  FreeGroup-extend : (A → G.El) → (FreeGroup A →ᴳ G)
  FreeGroup-extend f' = record {M} where
    module M where
      f : QuotWord A → G.El
      f = QuotWord-rec (Word-extendᴳ G f')
          (λ r → Word-extendᴳ-emap f' r)
      abstract
        pres-comp : preserves-comp (FreeGroup.comp A) G.comp f
        pres-comp =
          QuotWord-elim
            (λ l₁ → QuotWord-elim
              (λ l₂ → Word-extendᴳ-++ G f' l₁ l₂)
              (λ _ → prop-has-all-paths-↓))
            (λ _ → prop-has-all-paths-↓)

  private
    module Lemma (hom : FreeGroup A →ᴳ G) where
      open GroupHom hom
      f* : A → G.El
      f* a = f qw[ inl a :: nil ]

      abstract
        PlusMinus-extendᴳ-hom : ∀ x → PlusMinus-extendᴳ G f* x == f qw[ x :: nil ]
        PlusMinus-extendᴳ-hom (inl x) = idp
        PlusMinus-extendᴳ-hom (inr x) = ! $ pres-inv qw[ inl x :: nil ]

        Word-extendᴳ-hom : ∀ l → Word-extendᴳ G f* l == f qw[ l ]
        Word-extendᴳ-hom nil = ! pres-ident
        Word-extendᴳ-hom (x :: l) = ap2 G.comp (PlusMinus-extendᴳ-hom x) (Word-extendᴳ-hom l) ∙ ! (pres-comp _ _)
    open Lemma

  FreeGroup-extend-is-equiv : is-equiv FreeGroup-extend
  FreeGroup-extend-is-equiv = is-eq _ from to-from from-to where
    to = FreeGroup-extend
    from = f*

    abstract
      to-from : ∀ h → to (from h) == h
      to-from h = group-hom= $ λ= $ QuotWord-elim
        (λ l → Word-extendᴳ-hom h l)
        (λ _ → prop-has-all-paths-↓)

      from-to : ∀ f → from (to f) == f
      from-to f = λ= λ a → G.unit-r (f a)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Data.Nat     using (ℕ; _+_) renaming (_≤?_ to _≤?ₙ_)
open import Data.Bool    using (Bool; not; _∧_)
open import Data.String  using (String; _≟_)
open import Relation.Nullary           using (yes; no)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)

vname = String
val = ℕ
bool = Bool
state = vname → val

data aexp : Set where
  N : ℕ → aexp
  V : vname → aexp
  Plus : aexp → aexp → aexp

_[_/_] : aexp → aexp → vname → aexp
N c [ a′ / X ] = N c
V Y [ a′ / X ] with Y ≟ X
... | yes _ = a′
... | no  _ = V Y
Plus a b [ a′ / X ] = Plus (a [ a′ / X ]) (b [ a′ / X ])

_[_::=_] : state → vname → val → state
(s [ X ::= n ]) Y with Y ≟ X
... | yes _ = n
... | no  _ = s Y

aval : aexp → state → val
aval (N c) s = c
aval (V v) s = s v
aval (Plus a b) s = aval a s + aval b s

substitution : ∀ a {X a′ s}
  → aval (a [ a′ / X ]) s ≡ aval a (s [ X ::= aval a′ s ])
substitution (N x) = refl
substitution (V Y) {X} with Y ≟ X
... | yes _ = refl
... | no  _ = refl
substitution (Plus a b) {X}{a′}{s}
  rewrite substitution a {X}{a′}{s}
        | substitution b {X}{a′}{s} = refl

substitution-equiv : ∀{a a₁ a₂ X s}
  → aval a₁ s             ≡ aval a₂ s
  → aval (a [ a₁ / X ]) s ≡ aval (a [ a₂ / X ]) s
substitution-equiv {a}{a₁}{a₂}{X}{s} hyp
  rewrite substitution a {X}{a₁}{s}
        | hyp
        | sym (substitution a {X}{a₂}{s}) = refl

data bexp : Set where
  Bc   : Bool → bexp
  Not  : bexp → bexp
  And  : bexp → bexp → bexp
  Less : aexp → aexp → bexp

_≤?_ : ℕ → ℕ → Bool
a ≤? b = ⌊ a ≤?ₙ b ⌋

bval : bexp → state → bool
bval (Bc x) s = x
bval (Not b) s = not (bval b s)
bval (And a b) s = bval a s ∧ bval b s
bval (Less a b) s = aval a s ≤? aval b s

data com : Set where
  SKIP  : com
  _::=_ : String → aexp → com
  _::_  : com → com → com
  IF_THEN_ELSE_ : bexp → com → com → com
  WHILE_DO_     : bexp → com → com

max_stars_repo_name: iwilare/imp-semantics

max_issues_repo_name: iwilare/imp-semantics

max_forks_repo_name: iwilare/imp-semantics


text:
{-
  There was a bug when partially instantiating a module containing
  record projections.
-}
module Issue438 where

module M (A : Set) where

  record R (a : A) : Set₁ where
    field
      S : Set

postulate
  X : Set
  x : X
  r : M.R X x

module MX = M X

postulate
  T : MX.R.S r → Set
  y : M.R.S X r
  t : T y

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

module Ctt where

open import Cubical.Core.Everything
open import Agda.Primitive.Cubical
  using ( primComp )

-- Identity function.
id : ∀ {ℓ} {A : Set ℓ} (x : A) → A
id x = x

-- Funciton composition.
_∘_ : ∀ {ℓ} {A B C : Type ℓ} (g : B → C) (f : A → B) → A → C
g ∘ f = λ a → g (f a)

-- Equivalence is the path to `x` itself.
refl : ∀ {ℓ} {A : Type ℓ} {x : A} → Path A x x
refl {x = x} = λ i → x

-- A square in `A` is built out of 4 points and 4 lines.
square : ∀ {ℓ} {A : Type ℓ} {x0 x1 y0 y1 : A}
  → x0 ≡ x1 → y0 ≡ y1 → x0 ≡ y0 → x1 ≡ y1
  → Type ℓ
square p q r s = PathP (λ i → p i ≡ q i) r s

-- Symmetry.
sym : ∀ {ℓ} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
sym p i = p (~ i)
-- sym p i = λ i → p (~ i)

-- Congruence.
cong : ∀ {ℓ} {A : Type ℓ} {x y : A} {B : A → Type ℓ}
  (f : (a : A) → B a) (p : x ≡ y)
  → PathP (λ i → B (p i)) (f x) (f y)
cong f p i = f (p i)

-- Symmetry inverse.
symInv : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
symInv p = refl

-- Congruence with identity function.
congId : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → cong id p ≡ p
congId p = refl

-- Congruence with composition.
congComp : ∀ {ℓ} {A B C : Type ℓ}
  (f : A → B) (g : B → C)
  {x y : A} (p : x ≡ y)
  → cong (g ∘ f) p ≡ cong g (cong f p)
congComp f g p = refl

-- Function extensionality.
funExt : ∀ {ℓ} {A : Type ℓ} {B : A → Type ℓ} {f g : (x : A) → B x}
  → ((x : A) → f x ≡ g x) → f ≡ g
funExt p i x = p x i
-- `p` matches the 1st parameter,
-- `i` matches the dimension of the 1st parameter,
-- `x` matches `(x : A)`,
-- `funExt p i x = {!!}` the goal matches `B x`,
-- `(p x) i` is obvious.

-- Transitivity.
trans : ∀ {ℓ} {A : Type ℓ} {x y z : A}
  → x ≡ y → y ≡ z → x ≡ z
trans {y = y} p q i = primComp {!!} {!!} {!!}

-- Transport with composition.
transportComp : ∀ {ℓ} {A B C : Type ℓ}
  → A ≡ B → B ≡ C → A → C
transportComp p q a = {!!}

max_stars_repo_name: anqurvanillapy/fpl

max_issues_repo_name: anqurvanillapy/fpl

max_forks_repo_name: anqurvanillapy/fpl


text:
module Monads.Identity where

open import Class.Functor
open import Class.Monad
open import Class.MonadTrans
open import Level

private
  variable
    a : Level

Id : Set a -> Set a
Id A = A

IdentityT : (Set a -> Set a) -> Set a -> Set a
IdentityT M A = M A

instance
  Id-Monad : Monad (Id {a})
  Id-Monad = record { _>>=_ = λ a f -> f a ; return = λ a -> a }

module _ (M : Set a -> Set a) {{_ : Monad M}} where
  IdentityT-Monad : Monad (IdentityT M)
  IdentityT-Monad = record { _>>=_ = _>>=_ ; return = return }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------
-- Untyped hereditary substitution in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Syntax.SingleVariableSubstitution where

open import Data.Fin using (Fin; zero; suc; raise; lift)
open import Data.Fin.Substitution using (Sub; Subs; Lift; Application)
open import Data.Fin.Substitution.Lemmas using (AppLemmas)
  renaming (module VarLemmas to V)
open import Data.Fin.Substitution.ExtraLemmas
  using (TermLikeLemmas; LiftAppLemmas)
open import Data.Nat using (ℕ; zero; suc; _+_)
import Data.Vec as Vec
open import Data.Vec.Properties using (lookup-map)
open import Relation.Binary.Construct.Closure.ReflexiveTransitive using (ε; _◅_)
open import Relation.Binary.PropositionalEquality as P hiding ([_])

open import FOmegaInt.Syntax renaming (module Substitution to Sub)

----------------------------------------------------------------------
-- Untyped single-variable substitution.

open Syntax
open Sub using (weaken; weakenElim; weakenElim⋆; _Elim/Var_)

-- Suspended single-variable substitions.
--
-- Traditionally, a single-variable substitution [t/x] consists of two
-- data: the name x of the variable to be substituted and the
-- substitute t for the variable.
--
-- The following inductive definition is an alternative representation
-- of this data.  Instead of specifying the variable name (i.e. the de
-- Bruijn index) to be substituted, we use two constructors: one for
-- substituting the zero-th variable (sub) and one for lifting the
-- substitution over an a new free variable (_↑).  The advantage of
-- this representation is that it corresponds more closely to the
-- explicit substitution calculus and the inductive structure of both
-- de Bruijn indices and dependent contexts.  Among other things, this
-- avoids green slime in the definition.
--
-- Since we are working with intrinsically well-scoped syntax, the
-- datatype is parametrized by the number of free variables in the
-- source and target context: a substitution |σ : SVSub m n|, when
-- applied to a term with at most m variables, yields a term with at
-- most n variables.

data SVSub : ℕ → ℕ → Set where
  sub : ∀ {n}   (a : Elim n)    → SVSub (suc n) n
  _↑  : ∀ {m n} (σ : SVSub m n) → SVSub (suc m) (suc n)

-- Repeated lifting.

_↑⋆_ : ∀ {m n} (σ : SVSub m n) k → SVSub (k + m) (k + n)
σ ↑⋆ zero  = σ
σ ↑⋆ suc k = (σ ↑⋆ k) ↑

-- Turn a single-variable substitution into a multi-variable
-- substitution.

toSub : ∀ {m n} → SVSub m n → Sub Term m n
toSub (sub a) = Sub.sub ⌞ a ⌟
toSub (σ ↑)   = (toSub σ) Sub.↑

-- The result of looking up a single-variable substitution.

data SVRes : ℕ → Set where
  hit  : ∀ {n} (a : Elim n) → SVRes n  -- hit: looked up t at x in [t/x]
  miss : ∀ {n} (y : Fin n)  → SVRes n  -- miss: looked up y ≠ x in [t/x]

toElim : ∀ {n} → SVRes n → Elim n
toElim (hit a)  = a
toElim (miss y) = var∙ y

-- Renamings in single-variable substitutions and results.

infixl 8 _?/Var_

_?/Var_ : ∀ {m n} → SVRes m → Sub Fin m n → SVRes n
hit a  ?/Var ρ = hit (a Elim/Var ρ)
miss y ?/Var ρ = miss (Vec.lookup ρ y)

-- Weakening of SV results.

weakenSVRes : ∀ {n} → SVRes n → SVRes (suc n)
weakenSVRes r = r ?/Var V.wk

-- Look up a variable in a single-variable substitution.

lookupSV : ∀ {m n} → SVSub m n → Fin m → SVRes n
lookupSV (sub a) zero    = hit a
lookupSV (sub a) (suc x) = miss x
lookupSV (σ ↑)   zero    = miss zero
lookupSV (σ ↑)   (suc x) = weakenSVRes (lookupSV σ x)

----------------------------------------------------------------------
-- Properties of single-variable substitution and results.

open P.≡-Reasoning

-- Lifting commutes with conversion of substitutions.

↑⋆-toSub : ∀ {m n} {σ : SVSub m n} k → toSub (σ ↑⋆ k) ≡ (toSub σ) Sub.↑⋆ k
↑⋆-toSub zero    = refl
↑⋆-toSub (suc k) = cong Sub._↑ (↑⋆-toSub k)

-- Application of renamings commutes with conversion to terms.

toElim-/Var : ∀ {m n} r {ρ : Sub Fin m n} →
              toElim (r ?/Var ρ) ≡ toElim r Elim/Var ρ
toElim-/Var (hit a)  = refl
toElim-/Var (miss y) = refl

-- Lookup commutes with conversion of substitutions.

lookup-toSub : ∀ {m n} (σ : SVSub m n) (x : Fin m) →
               Vec.lookup (toSub σ) x ≡ ⌞ toElim (lookupSV σ x) ⌟
lookup-toSub (sub a) zero    = refl
lookup-toSub (sub a) (suc x) = Sub.lookup-id x
lookup-toSub (σ ↑)   zero    = refl
lookup-toSub (σ ↑)   (suc x) = begin
  Vec.lookup ((toSub σ) Sub.↑) (suc x)      ≡⟨⟩
  Vec.lookup (Vec.map weaken (toSub σ)) x   ≡⟨ lookup-map x weaken (toSub σ) ⟩
  weaken (Vec.lookup (toSub σ) x)           ≡⟨ cong weaken (lookup-toSub σ x) ⟩
  weaken ⌞ toElim σ[x] ⌟                    ≡˘⟨ Sub.⌞⌟-/Var (toElim σ[x]) ⟩
  ⌞ weakenElim (toElim σ[x]) ⌟              ≡˘⟨ cong ⌞_⌟ (toElim-/Var σ[x]) ⟩
  ⌞ toElim (weakenSVRes σ[x]) ⌟             ≡⟨⟩
  ⌞ toElim (lookupSV (σ ↑) (suc x)) ⌟       ∎
  where
    open P.≡-Reasoning
    σ[x] = lookupSV σ x

-- Lemmas about applications of renamings to SV results

open TermLikeLemmas Sub.termLikeLemmasElim using (varLiftAppLemmas)
open LiftAppLemmas varLiftAppLemmas using (id-vanishes; /-⊙; wk-commutes)

?/Var-id : ∀ {n} (r : SVRes n) → r ?/Var V.id ≡ r
?/Var-id (hit a)  = cong hit (id-vanishes a)
?/Var-id (miss y) = cong miss (V.id-vanishes y)

?/Var-⊙ : ∀ {m n k} {ρ₁ : Sub Fin m n} {ρ₂ : Sub Fin n k} r →
          r ?/Var ρ₁ V.⊙ ρ₂ ≡ r ?/Var ρ₁ ?/Var ρ₂
?/Var-⊙                (hit a)  = cong hit (/-⊙ a)
?/Var-⊙ {ρ₁ = ρ₁} {ρ₂} (miss y) = cong miss (V./-⊙ {ρ₁ = ρ₁} {ρ₂} y)

resAppLemmas : AppLemmas SVRes Fin
resAppLemmas = record
  { application = record { _/_ = _?/Var_ }
  ; lemmas₄     = V.lemmas₄
  ; id-vanishes = ?/Var-id
  ; /-⊙         = ?/Var-⊙
  }

module SVResAppLemmas = AppLemmas resAppLemmas

-- Lookup in a single-variable substitution commutes with renaming

lookup-sub-/Var-↑⋆ : ∀ {m n} a i x {ρ : Sub Fin m n} →
                     lookupSV (sub a ↑⋆ i) x ?/Var ρ V.↑⋆ i  ≡
                     lookupSV (sub (a Elim/Var ρ) ↑⋆ i) (x V./ (ρ V.↑) V.↑⋆ i)
lookup-sub-/Var-↑⋆ a zero zero        = refl
lookup-sub-/Var-↑⋆ a zero (suc x) {ρ} = begin
    miss (Vec.lookup ρ x)
  ≡⟨⟩
    lookupSV (sub (a Elim/Var ρ)) (suc (Vec.lookup ρ x))
  ≡˘⟨ cong (lookupSV (sub (a Elim/Var ρ))) (lookup-map x suc ρ) ⟩
    lookupSV (sub (a Elim/Var ρ)) (Vec.lookup (Vec.map suc ρ) x)
  ≡⟨⟩
    lookupSV (sub (a Elim/Var ρ)) (suc x V./ ρ V.↑)
  ∎
lookup-sub-/Var-↑⋆ a (suc i) zero        = refl
lookup-sub-/Var-↑⋆ a (suc i) (suc x) {ρ} = begin
    weakenSVRes (lookupSV (sub a ↑⋆ i) x) ?/Var (ρ V.↑⋆ i) V.↑
  ≡⟨⟩
    lookupSV (sub a ↑⋆ i) x ?/Var V.wk ?/Var (ρ V.↑⋆ i) V.↑
  ≡˘⟨ SVResAppLemmas.wk-commutes (lookupSV (sub a ↑⋆ i) x) ⟩
    lookupSV (sub a ↑⋆ i) x ?/Var (ρ V.↑⋆ i) ?/Var V.wk
  ≡⟨ cong (_?/Var V.wk) (lookup-sub-/Var-↑⋆ a i x) ⟩
    lookupSV (sub (a Elim/Var ρ) ↑⋆ i) (x V./ ((ρ V.↑) V.↑⋆ i)) ?/Var V.wk
  ≡⟨⟩
    lookupSV ((sub (a Elim/Var ρ) ↑⋆ i) ↑) (suc (x V./ (ρ V.↑) V.↑⋆ i))
  ≡˘⟨ cong (lookupSV ((sub (a Elim/Var ρ) ↑⋆ i) ↑))
           (lookup-map x suc ((ρ V.↑) V.↑⋆ i)) ⟩
    lookupSV ((sub (a Elim/Var ρ) ↑⋆ i) ↑)
             (Vec.lookup (Vec.map suc ((ρ V.↑) V.↑⋆ i)) x)
  ≡⟨⟩
    lookupSV ((sub (a Elim/Var ρ) ↑⋆ i) ↑) (suc x V./ ((ρ V.↑) V.↑⋆ i) V.↑)
  ∎

-- Lookup commutes with weakening

lookup-/Var-wk-↑⋆ : ∀ {m n} i x {σ : SVSub m n} →
                    lookupSV (σ ↑⋆ i) x ?/Var V.wk V.↑⋆ i ≡
                    lookupSV ((σ ↑) ↑⋆ i) (x V./ V.wk V.↑⋆ i)
lookup-/Var-wk-↑⋆ zero x {σ} = begin
    lookupSV σ x ?/Var V.wk
  ≡⟨⟩
    lookupSV (σ ↑) (suc x)
  ≡˘⟨ cong (lookupSV (σ ↑)) V./-wk ⟩
    lookupSV (σ ↑) (x V./ V.wk)
  ∎
lookup-/Var-wk-↑⋆ (suc i) zero        = refl
lookup-/Var-wk-↑⋆ (suc i) (suc x) {σ} = begin
    lookupSV (σ ↑⋆ i) x ?/Var V.wk ?/Var (V.wk V.↑⋆ i) V.↑
  ≡˘⟨ SVResAppLemmas.wk-commutes (lookupSV (σ ↑⋆ i) x) ⟩
    lookupSV (σ ↑⋆ i) x ?/Var V.wk V.↑⋆ i ?/Var V.wk
  ≡⟨ cong weakenSVRes (lookup-/Var-wk-↑⋆ i x) ⟩
    lookupSV (((σ ↑) ↑⋆ i) ↑) (suc (Vec.lookup (V.wk V.↑⋆ i) x))
  ≡˘⟨ cong (lookupSV (((σ ↑) ↑⋆ i) ↑)) (lookup-map x suc (V.wk V.↑⋆ i)) ⟩
    lookupSV (((σ ↑) ↑⋆ i) ↑) (Vec.lookup (Vec.map suc (V.wk V.↑⋆ i)) x)
  ≡⟨⟩
    lookupSV (((σ ↑) ↑⋆ i) ↑) (suc x V./ V.wk V.↑⋆ suc i)
  ∎

----------------------------------------------------------------------
-- Predicates relating SV substitutions to variables.

data Hit : ∀ {m n} → SVSub m n → Fin m → Elim n → Set where
  here : ∀ {n} {a : Elim n} → Hit (sub a) zero a
  _↑   : ∀ {m n} {σ : SVSub m n} {x a} →
         Hit σ x a → Hit (σ ↑) (suc x) (weakenElim a)

data Miss : ∀ {m n} → SVSub m n → Fin m → Fin n → Set where
  over  : ∀ {n} {a : Elim n} {y : Fin n} → Miss (sub a) (suc y) y
  under : ∀ {m n} {σ : SVSub m n} → Miss (σ ↑) zero zero
  _↑    : ∀ {m n} {σ : SVSub m n} {x y} →
          Miss σ x y → Miss (σ ↑) (suc x) (suc y)

data Hit? {m n} (σ : SVSub m n) (x : Fin m) : Set where
  hit  : ∀ a → Hit  σ x a → Hit? σ x
  miss : ∀ y → Miss σ x y → Hit? σ x

toRes : ∀ {m n} {σ : SVSub m n} {x : Fin m} → Hit? σ x → SVRes n
toRes (hit a _)  = hit a
toRes (miss y _) = miss y

-- A version of `lookupSV' that produces a more a more informative
-- result.

hit? : ∀ {m n} (σ : SVSub m n) (x : Fin m) → Hit? σ x
hit? (sub a) zero    = hit a here
hit? (sub a) (suc x) = miss x over
hit? (σ ↑)   zero    = miss zero under
hit? (σ ↑)   (suc x) with hit? σ x
... | hit a hitP   = hit (weakenElim a) (hitP ↑)
... | miss y missP = miss (suc y) (missP ↑)

-- The two versions of lookup agree.

lookup-Hit : ∀ {m n} {σ : SVSub m n} {x : Fin m} {a : Elim n} →
             Hit σ x a → lookupSV σ x ≡ hit a
lookup-Hit here  = refl
lookup-Hit (hitP ↑) = cong weakenSVRes (lookup-Hit hitP)

lookup-Miss : ∀ {m n} {σ : SVSub m n} {x : Fin m} {y : Fin n} →
              Miss σ x y → lookupSV σ x ≡ miss y
lookup-Miss                           over      = refl
lookup-Miss                           under     = refl
lookup-Miss {σ = σ ↑} {suc x} {suc y} (missP ↑) = begin
  weakenSVRes (lookupSV σ x)  ≡⟨ cong weakenSVRes (lookup-Miss missP) ⟩
  miss (y V./ V.wk)           ≡⟨ cong miss V./-wk ⟩
  miss (suc y)                ∎

hit?-lookup : ∀ {m n} (σ : SVSub m n) (x : Fin m) →
              lookupSV σ x ≡ toRes (hit? σ x)
hit?-lookup σ x with hit? σ x
... | (hit a hitP)   = lookup-Hit hitP
... | (miss y missP) = lookup-Miss missP

-- The Hit predicate is functional.

Hit-functional₁ : ∀ {m n} {σ : SVSub m n} {x y : Fin m} {a b : Elim n} →
                  Hit σ x a → Hit σ y b → x ≡ y
Hit-functional₁ here      here      = refl
Hit-functional₁ (hitP₁ ↑) (hitP₂ ↑) = cong suc (Hit-functional₁ hitP₁ hitP₂)

Hit-functional₂ : ∀ {m n} {σ : SVSub m n} {x y : Fin m} {a b : Elim n} →
                  Hit σ x a → Hit σ y b → a ≡ b
Hit-functional₂ here      here      = refl
Hit-functional₂ (hitP₁ ↑) (hitP₂ ↑) =
  cong weakenElim (Hit-functional₂ hitP₁ hitP₂)

-- For a fixed σ, the Miss predicate is injective.

Miss-injective : ∀ {m n} {σ : SVSub m n} {x y : Fin m} {z : Fin n} →
                 Miss σ x z → Miss σ y z → x ≡ y
Miss-injective over      over      = refl
Miss-injective under     under     = refl
Miss-injective (hitP₁ ↑) (hitP₂ ↑) = cong suc (Miss-injective hitP₁ hitP₂)

-- Lifting preserves the predicates

Hit-↑⋆ : ∀ {m n} {σ : SVSub m n} {x : Fin m} {a : Elim n} i →
         Hit σ x a → Hit (σ ↑⋆ i) (raise i x) (weakenElim⋆ i a)
Hit-↑⋆ zero    hyp = hyp
Hit-↑⋆ (suc i) hyp = (Hit-↑⋆ i hyp) ↑

Miss-↑⋆ : ∀ {m n} {σ : SVSub m n} {x : Fin m} {y : Fin n} i →
          Miss σ x y → Miss (σ ↑⋆ i) (raise i x) (raise i y)
Miss-↑⋆ zero    hyp = hyp
Miss-↑⋆ (suc i) hyp = (Miss-↑⋆ i hyp) ↑

Hit-↑-↑⋆ : ∀ {m n} {σ : SVSub m n} i {x a} → Hit (σ ↑⋆ i) x a →
           Hit ((σ ↑) ↑⋆ i) (lift i suc x) (a Elim/Var V.wk V.↑⋆ i)
Hit-↑-↑⋆ zero    hyp               = hyp ↑
Hit-↑-↑⋆ (suc i) (_↑ {a = a} hyp ) =
  subst (Hit _ _) (wk-commutes a) (Hit-↑-↑⋆ i hyp ↑)

Miss-↑-↑⋆ : ∀ {m n} {σ : SVSub m n} i {x y} → Miss (σ ↑⋆ i) x y →
            Miss ((σ ↑) ↑⋆ i) (lift i suc x) (lift i suc y)
Miss-↑-↑⋆ zero    hyp     = hyp ↑
Miss-↑-↑⋆ (suc i) under   = under
Miss-↑-↑⋆ (suc i) (hyp ↑) = (Miss-↑-↑⋆ i hyp) ↑

-- Yet another way to characterize hits/misses of single-variable
-- substitutions.

Hit-sub-↑⋆ : ∀ {n} {a : Elim n} i →
             Hit (sub a ↑⋆ i) (raise i zero) (weakenElim⋆ i a)
Hit-sub-↑⋆ i = Hit-↑⋆ i here

Hit-sub-↑⋆₁ : ∀ {n} {a : Elim n} i {x b} →
              Hit (sub a ↑⋆ i) x b → x ≡ raise i zero
Hit-sub-↑⋆₁ i hyp = Hit-functional₁ hyp (Hit-sub-↑⋆ i)

Hit-sub-↑⋆₂ : ∀ {n} {a : Elim n} i {x b} →
              Hit (sub a ↑⋆ i) x b → b ≡ weakenElim⋆ i a
Hit-sub-↑⋆₂ i hyp = Hit-functional₂ hyp (Hit-sub-↑⋆ i)

Miss-sub-↑⋆ : ∀ {n} {a : Elim n} i x → Miss (sub a ↑⋆ i) (lift i suc x) x
Miss-sub-↑⋆ zero    x       = over
Miss-sub-↑⋆ (suc i) zero    = under
Miss-sub-↑⋆ (suc i) (suc x) = Miss-sub-↑⋆ i x ↑

Miss-sub-↑⋆′ : ∀ {n} {a : Elim n} i {x} y →
               Miss (sub a ↑⋆ i) x y → x ≡ lift i suc y
Miss-sub-↑⋆′ i y hyp = Miss-injective hyp (Miss-sub-↑⋆ i y)

-- Looking up a sufficiently weakened variable will always miss.

lookup-sub-wk-↑⋆ : ∀ {n} i x {a : Elim n} →
                   lookupSV (sub a ↑⋆ i) (x V./ V.wk V.↑⋆ i) ≡ miss x
lookup-sub-wk-↑⋆ i x {a} = begin
    lookupSV (sub a ↑⋆ i) (x V./ V.wk V.↑⋆ i)
  ≡⟨ cong (lookupSV (sub a ↑⋆ i)) (V.lookup-wk-↑⋆ i x) ⟩
    lookupSV (sub a ↑⋆ i) (lift i suc x)
  ≡⟨ lookup-Miss (Miss-sub-↑⋆ i x) ⟩
    miss x
  ∎

-- A predicate for comparing variable names to naturals.
--
-- Instances of |Eq? n x| are proofs that a natural number |n| is or
-- is not "equal" to a variable name |x|.  Given two natural numbers
-- m, n and a "name" x in the interval { 0, ..., (n + 1 + m) }, "yes"
-- instances of the |Eq? n x| prove that "n = x", while "no" instances
-- prove that x is any one of the other names in the interval.
--
-- The predicate is useful for deciding whether a lookup of |x| in
-- some single-variable substitutions will lead to a hit or miss,
-- independently of the actual substitution.
--
-- NOTE. This predicate is only used in the proof of one lemma, namely
-- FOmegaInt.Kinding.Simple.EtaExpansion.Nf∈-[]-η-var.  Maybe the
-- proof of the lemma could be rewritten so as to avoid the
-- introduction of this extra predicate, but this might reduce
-- clarity.

data Eq? {m : ℕ} (n : ℕ) (x : Fin (n + suc m)) : Set where
  yes : raise n zero ≡ x       → Eq? n x
  no  : ∀ y → lift n suc y ≡ x → Eq? n x

-- Eq? is stable w.r.t. increments.

suc-Eq? : ∀ {m n} {x : Fin (n + suc m)} → Eq? n x → Eq? (suc n) (suc x)
suc-Eq? (yes refl)  = yes refl
suc-Eq? (no y refl) = no (suc y) refl

-- A decision procedure for Eq?.

compare : ∀ {m} n (x : Fin (n + suc m)) → Eq? n x
compare zero    zero    = yes refl
compare zero    (suc x) = no x refl
compare (suc n) zero    = no zero refl
compare (suc n) (suc x) = suc-Eq? (compare n x)

-- Turn Eq? instances into Hit? instances for a given substitution.

toHit? : ∀ {m n} {a : Elim m} {x} → Eq? n x → Hit? (sub a ↑⋆ n) x
toHit? {_} {n} (yes refl)  = hit _ (Hit-sub-↑⋆ n)
toHit? {_} {n} (no y refl) = miss y (Miss-sub-↑⋆ n y)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc; _+_)
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any as LA using (Any; here; there)
open import Data.Product using (_,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import Data.Environment
open import nodcap.Base

module nodcap.Typing where

-- Typing Rules.

infix 1 ⊢_

data ⊢_ : Environment → Set where

  ax   : {A : Type} →

       --------------
       ⊢ A ∷ A ^ ∷ []

  cut  : {Γ Δ : Environment} {A : Type} →

       ⊢ A ∷ Γ → ⊢ A ^ ∷ Δ →
       ---------------------
       ⊢ Γ ++ Δ

  send : {Γ Δ : Environment} {A B : Type} →

       ⊢ A ∷ Γ → ⊢ B ∷ Δ →
       -------------------
       ⊢ A ⊗ B ∷ Γ ++ Δ

  recv : {Γ : Environment} {A B : Type} →

       ⊢ A ∷ B ∷ Γ →
       -------------
       ⊢ A ⅋ B ∷ Γ

  sel₁ : {Γ : Environment} {A B : Type} →

       ⊢ A ∷ Γ →
       -----------
       ⊢ A ⊕ B ∷ Γ

  sel₂ : {Γ : Environment} {A B : Type} →

       ⊢ B ∷ Γ →
       -----------
       ⊢ A ⊕ B ∷ Γ

  case : {Γ : Environment} {A B : Type} →

       ⊢ A ∷ Γ → ⊢ B ∷ Γ →
       -------------------
       ⊢ A & B ∷ Γ

  halt :

       --------
       ⊢ 𝟏 ∷ []

  wait : {Γ : Environment} →

       ⊢ Γ →
       -------
       ⊢ ⊥ ∷ Γ

  loop : {Γ : Environment} →

       -------
       ⊢ ⊤ ∷ Γ

  mk?₁ : {Γ : Environment} {A : Type} →

       ⊢ A ∷ Γ →
       --------------
       ⊢ ?[ 1 ] A ∷ Γ

  mk!₁ : {Γ : Environment} {A : Type} →

       ⊢ A ∷ Γ →
       --------------
       ⊢ ![ 1 ] A ∷ Γ

  cont : {Γ : Environment} {A : Type} {m n : ℕ⁺} →

       ⊢ ?[ m ] A ∷ ?[ n ] A ∷ Γ →
       ------------------------------
       ⊢ ?[ m + n ] A ∷ Γ

  pool : {Γ Δ : Environment} {A : Type} {m n : ℕ⁺} →

       ⊢ ![ m ] A ∷ Γ → ⊢ ![ n ] A ∷ Δ →
       -------------------------------------
       ⊢ ![ m + n ] A ∷ Γ ++ Δ

  exch : {Γ Δ : Environment} →

       Γ ∼[ bag ] Δ → ⊢ Γ →
       --------------------
       ⊢ Δ

cutIn : {Γ Δ : Environment} {A : Type} (i : A ∈ Γ) (j : A ^ ∈ Δ) →

  ⊢ Γ → ⊢ Δ →
  ----------------
  ⊢ Γ - i ++ Δ - j

cutIn {Γ} {Δ} {A} i j P Q with ∈→++ i | ∈→++ j
... | (Γ₁ , Γ₂ , P.refl , p) | (Δ₁ , Δ₂ , P.refl , q) rewrite p | q
    = cut (exch (fwd [] Γ₁) P) (exch (fwd [] Δ₁) Q)

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


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

module Cardinality.Finite.ManifestBishop.Inductive where

open import Data.List public
open import Data.List.Membership public
open import Prelude

ℬ : Type a → Type a
ℬ A = Σ[ xs ⦂ List A ] Π[ x ⦂ A ] x ∈! xs

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Families with compatible monoid and coal
module SOAS.Coalgebraic.Monoid {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Variable
open import SOAS.Families.Core {T}
import SOAS.Families.Delta {T} as δ; open δ.Sorted
open import SOAS.Abstract.Hom {T}
import SOAS.Abstract.Box {T} as □ ; open □.Sorted
open import SOAS.Abstract.Monoid {T}
import SOAS.Abstract.Coalgebra {T} as →□ ; open →□.Sorted

open import SOAS.Coalgebraic.Map
open import SOAS.Coalgebraic.Strength
open import SOAS.Coalgebraic.Lift

private
  variable
    Γ Δ : Ctx
    α β : T

-- Coalgebraic monoid: family with compatible coalgebra and monoid structure
record CoalgMon (𝒳 : Familyₛ) : Set where
  field
    ᴮ : Coalgₚ 𝒳
    ᵐ : Mon 𝒳

  open Coalgₚ ᴮ public renaming (η to ηᴮ)
  open Mon ᵐ public hiding (ᵇ ; ᴮ ; r ; r∘η ; μᶜ) renaming (η to ηᵐ)

  field
    η-compat : {v : ℐ α Γ} → ηᴮ v ≡ ηᵐ v
    μ-compat : {ρ : Γ ↝ Δ}{t : 𝒳 α Γ} → r t ρ ≡ μ t (ηᵐ ∘ ρ)

  open Coalgₚ ᴮ using (r∘η) public

  -- Multiplication of coalgebraic monoids is a pointed coalgebraic map
  μᶜ : Coalgebraic ᴮ ᴮ ᴮ μ
  μᶜ = record
    { r∘f = λ{ {σ = σ}{ϱ}{t} → begin
             r (μ t σ) ϱ                  ≡⟨ μ-compat ⟩
             μ (μ t σ) (ηᵐ ∘ ϱ)            ≡⟨ assoc ⟩
             μ t (λ v → μ (σ v) (ηᵐ ∘ ϱ))  ≡˘⟨ cong (μ t) (dext (λ _ → μ-compat)) ⟩
             μ t (λ v → r (σ v) ϱ)        ∎ }
    ; f∘r = λ{ {ρ = ρ}{ς}{t} → begin
             μ (r t ρ) ς                ≡⟨ cong (λ - → μ - ς) μ-compat ⟩
             μ (μ t (ηᵐ ∘ ρ)) ς          ≡⟨ assoc ⟩
             μ t (λ v → μ (ηᵐ (ρ v)) ς)  ≡⟨ cong (μ t) (dext (λ _ → lunit)) ⟩
             μ t (ς ∘ ρ)                ∎ }
    ; f∘η = trans (μ≈₂ η-compat) runit
    } where open ≡-Reasoning

  str-eq : (𝒴 : Familyₛ){F : Functor 𝔽amiliesₛ 𝔽amiliesₛ}(F:Str : Strength F)
           (open Functor F)(open Strength F:Str)
           (h : F₀ 〖 𝒳 , 𝒴 〗 α Γ)(σ : Γ ~[ 𝒳 ]↝ Δ)
         → str ᴮ 𝒴 h σ ≡ str (Mon.ᴮ ᵐ) 𝒴 h σ
  str-eq 𝒴 {F} F:Str h σ = begin
        str ᴮ 𝒴 h σ
    ≡⟨ str-nat₁ {f = id} (record { ᵇ⇒ = record { ⟨r⟩ = sym μ-compat }
                                               ; ⟨η⟩ = sym η-compat }) h σ ⟩
        str (Mon.ᴮ ᵐ) 𝒴 (F₁ id h) σ
    ≡⟨ congr identity (λ - → str (Mon.ᴮ ᵐ) 𝒴 - σ) ⟩
        str (Mon.ᴮ ᵐ) 𝒴 h σ
    ∎
    where
    open Functor F
    open Strength F:Str
    open ≡-Reasoning

  lift-eq : {Ξ : Ctx}(t : 𝒳 β (Ξ ∔ Γ))(σ : Γ ~[ 𝒳 ]↝ Δ) →
            μ t (lift ᴮ Ξ σ) ≡ μ t (lift (Mon.ᴮ ᵐ) Ξ σ)
  lift-eq {Ξ = Ξ} t σ = str-eq 𝒳 (δ:Strength Ξ) (μ t) σ

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import HoTT
open import homotopy.Bouquet
open import homotopy.SphereEndomorphism
open import groups.SphereEndomorphism
open import groups.CoefficientExtensionality
open import cw.CW
open import cw.WedgeOfCells

module cw.DegreeByProjection {i} where

  module DegreeAboveOne {n : ℕ} (skel : Skeleton {i} (S (S n)))
    (dec : has-cells-with-dec-eq skel)
    -- the cells at the upper and lower dimensions
    (upper : cells-last skel)
    (lower : cells-last (cw-init skel))
    where

    private
      lower-skel = cw-init skel
      lower-cells = cells-nth lteS skel
      lower-dec = cells-nth-has-dec-eq lteS skel dec

    degree-map : Sphere (S n) → Sphere (S n)
    degree-map = bwproj lower-dec lower
               ∘ <– (Bouquet-equiv-Xₙ/Xₙ₋₁ lower-skel)
               ∘ cfcod
               ∘ attaching-last skel upper

    degree : ℤ
    degree = Trunc-⊙SphereS-endo-degree n (Trunc-⊙SphereS-endo-in n [ degree-map ])

  module DegreeAtOne (skel : Skeleton {i} 1)
    (dec : has-cells-with-dec-eq skel)
    -- the cells at the upper and lower dimensions
    (line : cells-last skel)
    (point : cells-last (cw-init skel)) where

    private
      points-dec-eq = cells-nth-has-dec-eq (inr ltS) skel dec
      endpoint = attaching-last skel

    -- When [true] matches, [true] will be sent to [false],
    -- which is bad.
    degree-true : ℤ
    degree-true with points-dec-eq point (endpoint line true)
    degree-true | inl _ = -1
    degree-true | inr _ = 0

    -- When [false] matches, [false] will be sent to [false],
    -- which is good.
    degree-false : ℤ
    degree-false with points-dec-eq point (endpoint line false)
    degree-false | inl _ = 1
    degree-false | inr _ = 0

    degree : ℤ
    degree = degree-true ℤ+ degree-false

  degree-last : ∀ {n} (skel : Skeleton {i} (S n))
    → has-cells-with-dec-eq skel
    → cells-last skel → cells-last (cw-init skel) → ℤ
  degree-last {n = O} = DegreeAtOne.degree
  degree-last {n = S _} = DegreeAboveOne.degree

  degree-nth : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n)
    → has-cells-with-dec-eq skel
    → cells-nth Sm≤n skel → cells-last (cw-init (cw-take Sm≤n skel)) → ℤ
  degree-nth Sm≤n skel dec = degree-last (cw-take Sm≤n skel) (take-has-cells-with-dec-eq Sm≤n skel dec)

  has-degrees-with-finite-support : ∀ {n} (skel : Skeleton {i} n)
    → has-cells-with-dec-eq skel → Type i
  has-degrees-with-finite-support {n = O} _ _ = Lift ⊤
  has-degrees-with-finite-support {n = S n} skel dec =
    has-degrees-with-finite-support (cw-init skel) (init-has-cells-with-dec-eq skel dec) ×
    ∀ upper → has-finite-support (cells-nth-has-dec-eq (inr ltS) skel dec) (degree-last skel dec upper)

  init-has-degrees-with-finite-support : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → has-degrees-with-finite-support (cw-init skel) (init-has-cells-with-dec-eq skel dec)
  init-has-degrees-with-finite-support skel dec fin-sup = fst fin-sup

  take-has-degrees-with-finite-support : ∀ {m n} (m≤n : m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → has-degrees-with-finite-support (cw-take m≤n skel) (take-has-cells-with-dec-eq m≤n skel dec)
  take-has-degrees-with-finite-support (inl idp) skel dec fin-sup = fin-sup
  take-has-degrees-with-finite-support (inr ltS) skel dec fin-sup =
    init-has-degrees-with-finite-support skel dec fin-sup
  take-has-degrees-with-finite-support (inr (ltSR lt)) skel dec fin-sup =
    take-has-degrees-with-finite-support (inr lt) (cw-init skel)
      (init-has-cells-with-dec-eq skel dec)
      (init-has-degrees-with-finite-support skel dec fin-sup)

  degree-last-has-finite-support : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → ∀ upper → has-finite-support
        (cells-last-has-dec-eq (cw-init skel) (init-has-cells-with-dec-eq skel dec))
        (degree-last skel dec upper)
  degree-last-has-finite-support skel dec fin-sup = snd fin-sup

  degree-nth-has-finite-support : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → ∀ upper → has-finite-support
        (cells-last-has-dec-eq
          (cw-init (cw-take Sm≤n skel))
          (init-has-cells-with-dec-eq (cw-take Sm≤n skel) (take-has-cells-with-dec-eq Sm≤n skel dec)))
        (degree-nth Sm≤n skel dec upper)
  degree-nth-has-finite-support Sm≤n skel dec fin-sup =
    degree-last-has-finite-support (cw-take Sm≤n skel)
      (take-has-cells-with-dec-eq Sm≤n skel dec)
      (take-has-degrees-with-finite-support Sm≤n skel dec fin-sup)

  -- the following are named [boundary'] because it is not extended to the free groups

  boundary'-last : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → cells-last skel → FreeAbGroup.El (cells-last (cw-init skel))
  boundary'-last skel dec fin-sup upper = fst ((snd fin-sup) upper)

  boundary-last : ∀ {n} (skel : Skeleton {i} (S n)) dec
    → has-degrees-with-finite-support skel dec
    → FreeAbGroup.grp (cells-last skel) →ᴳ FreeAbGroup.grp (cells-last (cw-init skel))
  boundary-last skel dec fin-sup =
    FreeAbGroup-extend (FreeAbGroup (cells-last (cw-init skel))) (boundary'-last skel dec fin-sup)

  boundary'-nth : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    → cells-nth Sm≤n skel → FreeAbGroup.El (cells-last (cw-init (cw-take Sm≤n skel)))
  boundary'-nth Sm≤n skel dec fin-sup =
    boundary'-last (cw-take Sm≤n skel)
      (take-has-cells-with-dec-eq Sm≤n skel dec)
      (take-has-degrees-with-finite-support Sm≤n skel dec fin-sup)

  boundary-nth : ∀ {m n} (Sm≤n : S m ≤ n) (skel : Skeleton {i} n) dec
    → has-degrees-with-finite-support skel dec
    →  FreeAbGroup.grp (cells-nth Sm≤n skel)
    →ᴳ FreeAbGroup.grp (cells-last (cw-init (cw-take Sm≤n skel)))
  boundary-nth Sm≤n skel dec fin-sup =
    FreeAbGroup-extend
      (FreeAbGroup (cells-last (cw-init (cw-take Sm≤n skel))))
      (boundary'-nth Sm≤n skel dec fin-sup)


text:
module tests.Forcing where

open import Prelude.IO
open import Prelude.Unit
open import Prelude.Vec
open import Prelude.Nat

len : {A : Set}{n : Nat} -> Vec A n -> Nat
len {A} .{Z}   []              = Z
len {A} .{S n} (_::_ {n} x xs) = S n

len2 : {A : Set}{n : Nat} -> Vec A n -> Nat
len2 [] = 0
len2 (_::_ {n} x xs) = S (len2 {n = n} xs)

len3 : {A : Set}{n : Nat} -> Vec A n -> Nat
len3 {n = Z}   []               = Z
len3 {n = S n} (_::_ .{n} x xs) = S n

len4 : {A : Set}{n : Nat} -> Vec A n -> Nat
len4 []               = Z
len4 (_::_ {Z} x xs) = S Z
len4 (_::_ {S n} x xs) = S (S n)

main : IO Unit
main =
    printNat (len  l1) ,,
    printNat (len  l2) ,,
    printNat (len  l3) ,,

    printNat (len2 l1) ,,
    printNat (len2 l2) ,,
    printNat (len2 l3) ,,

    printNat (len3 l1) ,,
    printNat (len3 l2) ,,
    printNat (len3 l3) ,,

    printNat (len4 l1) ,,
    printNat (len4 l2) ,,
    printNat (len4 l3) ,,

    return unit
  where l1 = "a" :: "b" :: "c" :: []
        l2 = 1   :: 2   :: 3   :: 4 :: 5 :: []
        l3 : Vec Nat Z
        l3 = []

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text: {-# COMPILE GHC myNat = 0 #-}


text:
-- Free category over a directed graph/quiver
{-# OPTIONS --safe #-}

module Cubical.Categories.Constructions.Free where

open import Cubical.Categories.Category.Base
open import Cubical.Data.Graph.Base
open import Cubical.Data.Graph.Path
open import Cubical.Foundations.Prelude hiding (Path)

module _ {ℓv ℓe : Level} where

  module _ (G : Graph ℓv ℓe)
          (isSetNode : isSet (Node G))
          (isSetEdge : ∀ v w → isSet (Edge G v w)) where
    open Category

    FreeCategory : Category ℓv (ℓ-max ℓv ℓe)
    FreeCategory .ob = Node G
    FreeCategory .Hom[_,_] = Path G
    FreeCategory .id = pnil
    FreeCategory ._⋆_ = ccat G
    FreeCategory .⋆IdL = pnil++ G
    FreeCategory .⋆IdR P = refl
    FreeCategory .⋆Assoc = ++assoc G
    FreeCategory .isSetHom = isSetPath G isSetNode isSetEdge _ _

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An All predicate for the partiality monad
------------------------------------------------------------------------

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

module Category.Monad.Partiality.All where

open import Category.Monad
open import Category.Monad.Partiality as Partiality using (_⊥; ⇒≈)
open import Codata.Musical.Notation
open import Function
open import Level
open import Relation.Binary using (_Respects_; IsEquivalence)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open Partiality._⊥
open Partiality.Equality using (Rel)
open Partiality.Equality.Rel
private
  open module E {a} {A : Set a} = Partiality.Equality (_≡_ {A = A})
    using (_≅_; _≳_)
  open module M {f} = RawMonad (Partiality.monad {f = f})
    using (_>>=_)

------------------------------------------------------------------------
-- All, along with some lemmas

-- All P x means that if x terminates with the value v, then P v
-- holds.

data All {a p} {A : Set a} (P : A → Set p) : A ⊥ → Set (a ⊔ p) where
  now   : ∀ {v} (p : P v)             → All P (now v)
  later : ∀ {x} (p : ∞ (All P (♭ x))) → All P (later x)

-- Bind preserves All in the following way:

_>>=-cong_ : ∀ {ℓ p q} {A B : Set ℓ} {P : A → Set p} {Q : B → Set q}
               {x : A ⊥} {f : A → B ⊥} →
             All P x → (∀ {x} → P x → All Q (f x)) →
             All Q (x >>= f)
now p   >>=-cong f = f p
later p >>=-cong f = later (♯ (♭ p >>=-cong f))

-- All respects all the relations, given that the predicate respects
-- the underlying relation.

respects :
  ∀ {k a p ℓ} {A : Set a} {P : A → Set p} {_∼_ : A → A → Set ℓ} →
  P Respects _∼_ → All P Respects Rel _∼_ k
respects resp (now    x∼y) (now   p) = now (resp x∼y p)
respects resp (later  x∼y) (later p) = later (♯ respects resp (♭ x∼y) (♭ p))
respects resp (laterˡ x∼y) (later p) =          respects resp    x∼y  (♭ p)
respects resp (laterʳ x≈y) p         = later (♯ respects resp    x≈y     p)

respects-flip :
  ∀ {k a p ℓ} {A : Set a} {P : A → Set p} {_∼_ : A → A → Set ℓ} →
  P Respects flip _∼_ → All P Respects flip (Rel _∼_ k)
respects-flip resp (now    x∼y) (now   p) = now (resp x∼y p)
respects-flip resp (later  x∼y) (later p) = later (♯ respects-flip resp (♭ x∼y) (♭ p))
respects-flip resp (laterˡ x∼y) p         = later (♯ respects-flip resp    x∼y     p)
respects-flip resp (laterʳ x≈y) (later p) =          respects-flip resp    x≈y  (♭ p)

-- "Equational" reasoning.

module Reasoning {a p ℓ}
                 {A : Set a} {P : A → Set p}
                 {_∼_ : A → A → Set ℓ}
                 (resp : P Respects flip _∼_) where

  infix  3 finally
  infixr 2 _≡⟨_⟩_ _∼⟨_⟩_

  _≡⟨_⟩_ : ∀ x {y} → x ≡ y → All P y → All P x
  _ ≡⟨ P.refl ⟩ p = p

  _∼⟨_⟩_ : ∀ {k} x {y} → Rel _∼_ k x y → All P y → All P x
  _ ∼⟨ x∼y ⟩ p = respects-flip resp (⇒≈ x∼y) p

  -- A cosmetic combinator.

  finally : (x : A ⊥) → All P x → All P x
  finally _ p = p

  syntax finally x p = x ⟨ p ⟩

-- "Equational" reasoning with _∼_ instantiated to propositional
-- equality.

module Reasoning-≡ {a p} {A : Set a} {P : A → Set p}
  = Reasoning {P = P} {_∼_ = _≡_} (P.subst P ∘ P.sym)

------------------------------------------------------------------------
-- An alternative, but equivalent, formulation of All

module Alternative {a p : Level} where

  infix  3 _⟨_⟩P
  infixr 2 _≅⟨_⟩P_ _≳⟨_⟩P_

  -- All "programs".

  data AllP {A : Set a} (P : A → Set p) : A ⊥ → Set (suc (a ⊔ p)) where
    now         : ∀ {x} (p : P x) → AllP P (now x)
    later       : ∀ {x} (p : ∞ (AllP P (♭ x))) → AllP P (later x)
    _>>=-congP_ : ∀ {B : Set a} {Q : B → Set p} {x f}
                  (p-x : AllP Q x) (p-f : ∀ {v} → Q v → AllP P (f v)) →
                  AllP P (x >>= f)
    _≅⟨_⟩P_     : ∀ x {y} (x≅y : x ≅ y) (p : AllP P y) → AllP P x
    _≳⟨_⟩P_     : ∀ x {y} (x≳y : x ≳ y) (p : AllP P y) → AllP P x
    _⟨_⟩P       : ∀ x (p : AllP P x) → AllP P x

  private

    -- WHNFs.

    data AllW {A} (P : A → Set p) : A ⊥ → Set (suc (a ⊔ p)) where
      now   : ∀ {x} (p : P x) → AllW P (now x)
      later : ∀ {x} (p : AllP P (♭ x)) → AllW P (later x)

    -- A function which turns WHNFs into programs.

    program : ∀ {A} {P : A → Set p} {x} → AllW P x → AllP P x
    program (now   p) = now      p
    program (later p) = later (♯ p)

    -- Functions which turn programs into WHNFs.

    trans-≅ : ∀ {A} {P : A → Set p} {x y : A ⊥} →
              x ≅ y → AllW P y → AllW P x
    trans-≅ (now P.refl) (now   p) = now p
    trans-≅ (later  x≅y) (later p) = later (_ ≅⟨ ♭ x≅y ⟩P p)

    trans-≳ : ∀ {A} {P : A → Set p} {x y : A ⊥} →
              x ≳ y → AllW P y → AllW P x
    trans-≳ (now P.refl) (now   p) = now p
    trans-≳ (later  x≳y) (later p) = later (_ ≳⟨ ♭ x≳y ⟩P p)
    trans-≳ (laterˡ x≳y)        p  = later (_ ≳⟨   x≳y ⟩P program p)

    mutual

      _>>=-congW_ : ∀ {A B} {P : A → Set p} {Q : B → Set p} {x f} →
                    AllW P x → (∀ {v} → P v → AllP Q (f v)) →
                    AllW Q (x >>= f)
      now   p >>=-congW p-f = whnf (p-f p)
      later p >>=-congW p-f = later (p >>=-congP p-f)

      whnf : ∀ {A} {P : A → Set p} {x} → AllP P x → AllW P x
      whnf (now   p)           = now p
      whnf (later p)           = later (♭ p)
      whnf (p-x >>=-congP p-f) = whnf p-x >>=-congW p-f
      whnf (_ ≅⟨ x≅y ⟩P p)     = trans-≅ x≅y (whnf p)
      whnf (_ ≳⟨ x≳y ⟩P p)     = trans-≳ x≳y (whnf p)
      whnf (_ ⟨ p ⟩P)          = whnf p

  -- AllP P is sound and complete with respect to All P.

  sound : ∀ {A} {P : A → Set p} {x} → AllP P x → All P x
  sound = λ p → soundW (whnf p)
    where
    soundW : ∀ {A} {P : A → Set p} {x} → AllW P x → All P x
    soundW (now   p) = now p
    soundW (later p) = later (♯ sound p)

  complete : ∀ {A} {P : A → Set p} {x} → All P x → AllP P x
  complete (now   p) = now p
  complete (later p) = later (♯ complete (♭ p))


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

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

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:
open import Data.Nat using ( zero ; suc ) renaming ( ℕ to ♭ℕ ; _+_ to add )
open import Function using () renaming ( _∘′_ to _∘_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans ; cong ; cong₂ )

open import AssocFree.Util using ( ≡-relevant )

module AssocFree.DNat where

open Relation.Binary.PropositionalEquality.≡-Reasoning using ( begin_ ; _≡⟨_⟩_ ; _∎ )

infixr 5 _,_
infixr 5 _+_

_+♭_ = add

add-unit : ∀ n → (add n 0) ≡ n
add-unit zero    = refl
add-unit (suc n) = cong suc (add-unit n)

add-assoc : ∀ m n → (add (add m n) ≡ ((add m) ∘ (add n)))
add-assoc zero    n = refl
add-assoc (suc m) n = cong (_∘_ suc) (add-assoc m n)

-- "Difference nats" are isomorphic to ℕ but have _+_ associative up
-- to beta-reduction, not just up to _≡_.

record ℕ : Set where
  constructor _,_
  field
    fun : ♭ℕ → ♭ℕ
    .fun✓ : fun ≡ add (fun 0)

open ℕ public

-- Convert ℕ to ♭ℕ and back

♯ : ♭ℕ → ℕ
♯ n = (add n , cong add (sym (add-unit n)))

♭ : ℕ → ♭ℕ
♭ (f , f✓) = f 0

-- Constants

♯0 = ♯ 0
♯1 = ♯ 1

-- Addition

_+_ : ℕ → ℕ → ℕ
(f , f✓) + (g , g✓) = ((f ∘ g) , f∘g✓) where
  .f∘g✓ : (f ∘ g) ≡ add (f (g 0))
  f∘g✓ = begin
      f ∘ g
    ≡⟨ cong₂ _∘_ f✓ g✓ ⟩
      add (f 0) ∘ add (g 0)
    ≡⟨ sym (add-assoc (f 0) (g 0)) ⟩
      add (add (f 0) (g 0))
    ≡⟨ cong (λ X → add (X (g 0))) (sym f✓) ⟩
      add (f (g 0))
    ∎

--Isomorphism which respects +

inject : ∀ m n → (fun m ≡ fun n) → (m ≡ n)
inject (f , f✓) (.f , g✓) refl = refl

iso : ∀ n → ♯ (♭ n) ≡ n
iso n = inject (♯ (♭ n)) n (sym (≡-relevant (fun✓ n)))

iso⁻¹ : ∀ n → ♭ (♯ n) ≡ n
iso⁻¹ = add-unit

iso-resp-+ : ∀ m n → ♭ (m + n) ≡ (♭ m +♭ ♭ n)
iso-resp-+ (f , f✓) (g , g✓) = cong (λ X → X (g 0)) (≡-relevant f✓)

-- Addition forms a monoid on the nose

+-assoc : ∀ l m n → (((l + m) + n) ≡ (l + (m + n)))
+-assoc l m n = refl

+-unit₁ : ∀ n → ((♯0 + n) ≡ n)
+-unit₁ n = refl

+-unit₂ : ∀ n → ((n + ♯0) ≡ n)
+-unit₂ n = refl

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


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

open import Categories.Category

-- a zero object is both terminal and initial.
module Categories.Object.Zero {o ℓ e} (C : Category o ℓ e) where

open import Level

open import Categories.Object.Terminal C
open import Categories.Object.Initial C

open import Categories.Morphism C
open import Categories.Morphism.Reasoning C

open Category C
open HomReasoning

record IsZero (Z : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    isInitial : IsInitial Z
    isTerminal : IsTerminal Z

  open IsInitial isInitial public
    renaming
    ( ! to ¡
    ; !-unique to ¡-unique
    ; !-unique₂ to ¡-unique₂
    )
  open IsTerminal isTerminal public

  zero⇒ : ∀ {A B : Obj} → A ⇒ B
  zero⇒ = ¡ ∘ !

  zero-∘ˡ : ∀ {X Y Z} → (f : Y ⇒ Z) → f ∘ zero⇒ {X} ≈ zero⇒
  zero-∘ˡ f = pullˡ (⟺ (¡-unique (f ∘ ¡)))

  zero-∘ʳ : ∀ {X Y Z} → (f : X ⇒ Y) → zero⇒ {Y} {Z} ∘ f ≈ zero⇒
  zero-∘ʳ f = pullʳ (⟺ (!-unique (! ∘ f)))

record Zero : Set (o ⊔ ℓ ⊔ e) where
  field
    𝟘 : Obj
    isZero : IsZero 𝟘

  open IsZero isZero public

  terminal : Terminal
  terminal = record { ⊤-is-terminal = isTerminal }

  initial : Initial
  initial = record { ⊥-is-initial = isInitial }

open Zero

¡-Mono : ∀ {A} {z : Zero} → Mono (¡ z {A})
¡-Mono {z = z} = from-⊤-is-Mono {t = terminal z} (¡ z)

!-Epi : ∀ {A} {z : Zero} → Epi (! z {A})
!-Epi {z = z} = to-⊥-is-Epi {i = initial z} (! z)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Issue279-2 where

data ⊥ : Set where

data ⊤ : Set where
  tt : ⊤

module M (A : Set) where

  data P : ⊤ → Set where
    tt : A → P tt

module X = M ⊥ using (tt)
open X

good : ⊥ → M.P ⊥ tt
good = tt

bad : M.P ⊤ tt
bad = tt tt

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
abstract

  data D : Set where
    d : D

  data P : D → Set where
    p : P d

  d′ : D
  d′ = d

  d₂ : D
  d₂ = d

private
  abstract
    p′ : P d
    p′ = p

A : P d′
A = p′

-- A : Set₁ -- P d′
-- A = Set -- p′
--   where

--   abstract

--     p′ : P d
--     p′ = p

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda