text:
------------------------------------------------------------------------------
-- Testing Agsy arithmetic properties used by the McCarthy 91 function
------------------------------------------------------------------------------

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

-- Tested with the development version of the Agda standard library on
-- 02 February 2012.

module Agsy.McCarthy91.Arithmetic where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

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

91≡[100+11∸10]∸10 : (100 + 11 ∸ 10) ∸ 10 ≡ 91
91≡[100+11∸10]∸10 = refl

20>19 : 20 > 19  -- via Agsy
20>19 = s≤s
          (s≤s
           (s≤s
            (s≤s
             (s≤s
              (s≤s
               (s≤s
                (s≤s
                 (s≤s
                  (s≤s
                   (s≤s
                    (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))))))))))))))))))

50>49 : 50 > 49  -- via Agsy {-t 30}
50>49 = s≤s
          (s≤s
           (s≤s
            (s≤s
             (s≤s
              (s≤s
               (s≤s
                (s≤s
                 (s≤s
                  (s≤s
                   (s≤s
                    (s≤s
                     (s≤s
                      (s≤s
                       (s≤s
                        (s≤s
                         (s≤s
                          (s≤s
                           (s≤s
                            (s≤s
                             (s≤s
                              (s≤s
                               (s≤s
                                (s≤s
                                 (s≤s
                                  (s≤s
                                   (s≤s
                                    (s≤s
                                     (s≤s
                                      (s≤s
                                       (s≤s
                                        (s≤s
                                         (s≤s
                                          (s≤s
                                           (s≤s
                                            (s≤s
                                             (s≤s
                                              (s≤s
                                               (s≤s
                                                (s≤s
                                                 (s≤s
                                                  (s≤s
                                                   (s≤s
                                                    (s≤s
                                                     (s≤s
                                                      (s≤s
                                                       (s≤s
                                                        (s≤s
                                                         (s≤s
                                                          (s≤s
                                                           z≤n)))))))))))))))))))))))))))))))))))))))))))))))))

75>74 : 75 > 74  -- via Agsy {-t 180}
75>74 = s≤s
          (s≤s
           (s≤s
            (s≤s
             (s≤s
              (s≤s
               (s≤s
                (s≤s
                 (s≤s
                  (s≤s
                   (s≤s
                    (s≤s
                     (s≤s
                      (s≤s
                       (s≤s
                        (s≤s
                         (s≤s
                          (s≤s
                           (s≤s
                            (s≤s
                             (s≤s
                              (s≤s
                               (s≤s
                                (s≤s
                                 (s≤s
                                  (s≤s
                                   (s≤s
                                    (s≤s
                                     (s≤s
                                      (s≤s
                                       (s≤s
                                        (s≤s
                                         (s≤s
                                          (s≤s
                                           (s≤s
                                            (s≤s
                                             (s≤s
                                              (s≤s
                                               (s≤s
                                                (s≤s
                                                 (s≤s
                                                  (s≤s
                                                   (s≤s
                                                    (s≤s
                                                     (s≤s
                                                      (s≤s
                                                       (s≤s
                                                        (s≤s
                                                         (s≤s
                                                          (s≤s
                                                           (s≤s
                                                            (s≤s
                                                             (s≤s
                                                              (s≤s
                                                               (s≤s
                                                                (s≤s
                                                                 (s≤s
                                                                  (s≤s
                                                                   (s≤s
                                                                    (s≤s
                                                                     (s≤s
                                                                      (s≤s
                                                                       (s≤s
                                                                        (s≤s
                                                                         (s≤s
                                                                          (s≤s
                                                                           (s≤s
                                                                            (s≤s
                                                                             (s≤s
                                                                              (s≤s
                                                                               (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                z≤n))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

101>100 : 101 > 100  -- via Agsy {-t 600}
101>100 = s≤s
          (s≤s
           (s≤s
            (s≤s
             (s≤s
              (s≤s
               (s≤s
                (s≤s
                 (s≤s
                  (s≤s
                   (s≤s
                    (s≤s
                     (s≤s
                      (s≤s
                       (s≤s
                        (s≤s
                         (s≤s
                          (s≤s
                           (s≤s
                            (s≤s
                             (s≤s
                              (s≤s
                               (s≤s
                                (s≤s
                                 (s≤s
                                  (s≤s
                                   (s≤s
                                    (s≤s
                                     (s≤s
                                      (s≤s
                                       (s≤s
                                        (s≤s
                                         (s≤s
                                          (s≤s
                                           (s≤s
                                            (s≤s
                                             (s≤s
                                              (s≤s
                                               (s≤s
                                                (s≤s
                                                 (s≤s
                                                  (s≤s
                                                   (s≤s
                                                    (s≤s
                                                     (s≤s
                                                      (s≤s
                                                       (s≤s
                                                        (s≤s
                                                         (s≤s
                                                          (s≤s
                                                           (s≤s
                                                            (s≤s
                                                             (s≤s
                                                              (s≤s
                                                               (s≤s
                                                                (s≤s
                                                                 (s≤s
                                                                  (s≤s
                                                                   (s≤s
                                                                    (s≤s
                                                                     (s≤s
                                                                      (s≤s
                                                                       (s≤s
                                                                        (s≤s
                                                                         (s≤s
                                                                          (s≤s
                                                                           (s≤s
                                                                            (s≤s
                                                                             (s≤s
                                                                              (s≤s
                                                                               (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                (s≤s
                                                                                z≤n))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Integer Literals
------------------------------------------------------------------------

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

module Data.Integer.Literals where

open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Data.Unit
open import Data.Integer

number : Number ℤ
number = record
  { Constraint = λ _ → ⊤
  ; fromNat    = λ n → + n
  }

negative : Negative ℤ
negative = record
  { Constraint = λ _ → ⊤
  ; fromNeg    = λ n → - (+ n)
  }

ext: agda


text:
module TelescopingLet where

module Star where
  ★ : Set₁
  ★ = Set

  ★₁ : Set₂
  ★₁ = Set₁

module MEndo (open Star) (A : ★) where
  Endo : ★
  Endo = A → A

module Batch1 where
  f : (let ★ = Set) (A : ★) → A → A
  f A x = x

  g : (let ★ = Set
           Endo = λ A → A → A) (A : ★) → Endo A
  g = f

  h : (open Star) (A : ★) → A → A
  h = g

module N (open Star) (A : ★) (open MEndo A) (f : Endo) where
  B : ★
  B = A
  f' : Endo
  f' = f

-- module N can be desugared as follows:

module _ where
  open Star
  module _ (A : ★) where
    open MEndo A
    module N' (f : Endo) where
      B : ★
      B = A
      f' : Endo
      f' = f

-- Here are instantiations of N and its desugaring:

f'1 = f'
  where
    postulate A : Set
              f : A → A
    open N A f

f'2 = f'
  where
    postulate A : Set
              f : A → A
    open N' A f

data ⊥ : Set where

module Batch2 where
  f = λ (let ★ = Set) (A : ★) (x : A) → x

  g = λ (open Star) (A : ★) (x : A) → x

  h0 = let open Star in
       λ (A : ★) →
       let module MA = MEndo A in
       let open MA in
       λ (f : Endo) →
       f

  h1 = let open Star in
       λ (A : ★) →
       let open MEndo A in
       λ (f : Endo) →
       f

  h = λ (open Star) (A : ★) (open MEndo A) (f : Endo) → f

module Batch3 where
  e1 : (let ★ = Set) → ★
  e1 = ⊥

  e2 = λ (let ★ = Set) → ★

  e3 = λ (open Star) → ★

  -- "λ (open M es) → e" is an edge case which behaves like "let open M es in e"

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- The purpose of this universe construction is to get some definitional
-- equalities in the model. Specifically, if we define ⟦σ⟧ : ⟦Δ⟧ → ⟦Ω⟧
-- (a functor) for the "canonical" notion of subsitution, then we have
-- ⟦Wk⟧ (δ , m) ≡ δ propositionally, but *not* definitionally. This then
-- complicates proofs involving ⟦Wk⟧, and similar for the other substitutions.

{-# OPTIONS --without-K --safe #-}
module Source.Size.Substitution.Universe where

open import Relation.Binary using (IsEquivalence ; Setoid)

open import Source.Size
open import Source.Size.Substitution.Canonical as Can using (Sub⊢)
open import Util.Prelude

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

infix  4 _≈_
infixl 5 _>>_

data Sub : (Δ Ω : Ctx) → Set where
  Id : Sub Δ Δ
  _>>_ : (σ : Sub Δ Δ′) (τ : Sub Δ′ Ω) → Sub Δ Ω
  Wk : Sub (Δ ∙ n) Δ
  Lift : (σ : Sub Δ Ω) → Sub (Δ ∙ m) (Ω ∙ n)
  Sing : (n : Size Δ) → Sub Δ (Δ ∙ m)
  Skip : Sub (Δ ∙ n ∙ v0) (Δ ∙ n)

⟨_⟩ : Sub Δ Ω → Can.Sub Δ Ω
⟨ Id ⟩ = Can.Id
⟨ σ >> τ ⟩ = ⟨ σ ⟩ Can.>> ⟨ τ ⟩
⟨ Wk ⟩ = Can.Wk
⟨ Lift σ ⟩ = Can.Lift ⟨ σ ⟩
⟨ Sing n ⟩ = Can.Sing n
⟨ Skip ⟩ = Can.Skip

subV : (σ : Sub Δ Ω) (x : Var Ω) → Size Δ
subV σ = Can.subV ⟨ σ ⟩

sub : (σ : Sub Δ Ω) (n : Size Ω) → Size Δ
sub σ = Can.sub ⟨ σ ⟩

pattern Lift′ σ ⊢n = Lift σ ⊢n refl

variable σ τ ι : Sub Δ Ω

data Sub⊢ᵤ : ∀ Δ Ω → Sub Δ Ω → Set where
  Id : Sub⊢ᵤ Δ Δ Id
  comp : (⊢σ : Sub⊢ᵤ Δ Δ′ σ) (⊢τ : Sub⊢ᵤ Δ′ Δ″ τ) → Sub⊢ᵤ Δ Δ″ (σ >> τ)
  Wk : Sub⊢ᵤ (Δ ∙ n) Δ Wk
  Lift : (⊢σ : Sub⊢ᵤ Δ Ω σ) (m≡n[σ] : m ≡ sub σ n)
    → Sub⊢ᵤ (Δ ∙ m) (Ω ∙ n) (Lift σ)
  Sing : (n<m : n < m) → Sub⊢ᵤ Δ (Δ ∙ m) (Sing n)
  Skip : Sub⊢ᵤ (Δ ∙ n ∙ v0) (Δ ∙ n) Skip

syntax Sub⊢ᵤ Δ Ω σ = σ ∶ Δ ⇒ᵤ Ω

⟨⟩-resp-⊢ : σ ∶ Δ ⇒ᵤ Ω → ⟨ σ ⟩ ∶ Δ ⇒ Ω
⟨⟩-resp-⊢ Id = Can.Id⊢
⟨⟩-resp-⊢ (comp ⊢σ ⊢τ) = Can.>>⊢ (⟨⟩-resp-⊢ ⊢σ) (⟨⟩-resp-⊢ ⊢τ)
⟨⟩-resp-⊢ Wk = Can.Wk⊢
⟨⟩-resp-⊢ (Lift ⊢σ m≡n[σ]) = Can.Lift⊢ (⟨⟩-resp-⊢ ⊢σ) m≡n[σ]
⟨⟩-resp-⊢ (Sing n<m) = Can.Sing⊢ n<m
⟨⟩-resp-⊢ Skip = Can.Skip⊢

record _≈_ (σ τ : Sub Δ Ω) : Set where
  constructor ≈⁺
  field ≈⁻ : ⟨ σ ⟩ ≡ ⟨ τ ⟩

open _≈_ public

≈-refl : σ ≈ σ
≈-refl = ≈⁺ refl

≈-sym : σ ≈ τ → τ ≈ σ
≈-sym (≈⁺ p) = ≈⁺ (sym p)

≈-trans : σ ≈ τ → τ ≈ ι → σ ≈ ι
≈-trans (≈⁺ p) (≈⁺ q) = ≈⁺ (trans p q)

≈-isEquivalence : IsEquivalence (_≈_ {Δ} {Ω})
≈-isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans }

Sub-setoid : (Δ Ω : Ctx) → Setoid 0ℓ 0ℓ
Sub-setoid Δ Ω = record
  { Carrier = Sub Δ Ω
  ; _≈_ = _≈_
  ; isEquivalence = ≈-isEquivalence
  }

module ≈-Reasoning {Δ} {Ω} = SetoidReasoning (Sub-setoid Δ Ω)

abstract
  >>-resp-≈ : {σ σ′ : Sub Δ Δ′} {τ τ′ : Sub Δ′ Δ″}
    → σ ≈ σ′ → τ ≈ τ′ → σ >> τ ≈ σ′ >> τ′
  >>-resp-≈ (≈⁺ p) (≈⁺ q) = ≈⁺ (cong₂ Can._>>_ p q)

  Lift-resp-≈ : σ ≈ τ → Lift {m = m} {n} σ ≈ Lift τ
  Lift-resp-≈ (≈⁺ p) = ≈⁺ (cong Can.Lift p)

  sub-resp-< : σ ∶ Δ ⇒ᵤ Ω → n < m → sub σ n < sub σ m
  sub-resp-< ⊢σ = Can.sub-resp-< (⟨⟩-resp-⊢ ⊢σ)

mutual
  subV′ : Sub Δ Ω → Var Ω → Size Δ
  subV′ Id x = var x
  subV′ (σ >> τ) x = sub′ σ (subV′ τ x)
  subV′ Wk x = var (suc x)
  subV′ (Lift σ) zero = var zero
  subV′ (Lift σ) (suc x) = wk (subV′ σ x)
  subV′ (Sing n) zero = n
  subV′ (Sing n) (suc x) = var x
  subV′ Skip zero = var zero
  subV′ Skip (suc x) = var (suc (suc x))

  sub′ : Sub Δ Ω → Size Ω → Size Δ
  sub′ σ (var x) = subV′ σ x
  sub′ σ ∞ = ∞
  sub′ σ zero = zero
  sub′ σ (suc n) = suc (sub′ σ n)

  abstract
    subV′≡subV : ∀ (σ : Sub Δ Ω) x → subV′ σ x ≡ subV σ x
    subV′≡subV Id x = sym (Can.subV-Id x)
    subV′≡subV (σ >> τ) x
      = trans (sub′≡sub σ (subV′ τ x))
          (trans (cong (sub σ) (subV′≡subV τ x))
            (sym (Can.subV->> ⟨ σ ⟩ ⟨ τ ⟩ x)))
    subV′≡subV Wk x = sym (Can.sub-Wk (var x))
    subV′≡subV (Lift σ) zero = refl
    subV′≡subV (Lift σ) (suc x)
      = trans (cong wk (subV′≡subV σ x)) (sym (Can.subV-Weaken ⟨ σ ⟩ x))
    subV′≡subV (Sing n) zero = refl
    subV′≡subV (Sing n) (suc x) = sym (Can.subV-Id x)
    subV′≡subV Skip zero = refl
    subV′≡subV Skip (suc x) = sym
      (trans (Can.subV-Weaken (Can.Weaken Can.Id) x) (cong wk (Can.sub-Wk (var x))))

    sub′≡sub : ∀ (σ : Sub Δ Ω) n → sub′ σ n ≡ sub σ n
    sub′≡sub σ (var x) = subV′≡subV σ x
    sub′≡sub σ ∞ = refl
    sub′≡sub σ zero = refl
    sub′≡sub σ (suc n) = cong suc (sub′≡sub σ n)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DirectSum.DirectSumHIT.Properties where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

private variable
  ℓ ℓ' : Level

module AbGroupProperties
  (Idx : Type ℓ)
  (P : Idx → Type ℓ')
  (AGP : (r : Idx) → AbGroupStr (P r))
  where

  inv : ⊕HIT Idx P AGP → ⊕HIT Idx P AGP
  inv = DS-Rec-Set.f Idx P AGP (⊕HIT Idx P AGP) trunc
           -- elements
           neutral
           (λ r a → base r (AbGroupStr.-_ (AGP r) a))
           (λ xs ys → xs add ys)
           -- eq group
           (λ xs ys zs → addAssoc xs ys zs)
           (λ xs → addRid xs)
           (λ xs ys → addComm xs ys)
           -- eq base
           (λ r → let open AbGroupStr (AGP r) in
                   let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
                   (cong (base r) inv1g) ∙ (base-neutral r))
           (λ r a b → let open AbGroupStr (AGP r) in
                       let open GroupTheory (P r , AbGroupStr→GroupStr (AGP r)) in
                       ((base r (- a) add base r (- b))   ≡⟨ (base-add r (- a) (- b)) ⟩
                       base r ((- a) + (- b))             ≡⟨ (cong (base r) (sym (invDistr b a))) ⟩
                       base r (- (b + a))                 ≡⟨ cong (base r) (cong (-_) (+Comm b a)) ⟩
                       base r (- (a + b)) ∎))

  rinv : (z : ⊕HIT Idx P AGP) → z add (inv z) ≡ neutral
  rinv = DS-Ind-Prop.f Idx P AGP (λ z → z add (inv z) ≡ neutral) (λ _ → trunc _ _)
         -- elements
         (addRid neutral)
         (λ r a → let open AbGroupStr (AGP r) in
                        ((base r a add base r (- a)) ≡⟨ base-add r a (- a) ⟩
                        base r (a + - a)             ≡⟨ cong (base r) (+InvR a) ⟩
                        base r 0g                    ≡⟨ base-neutral r ⟩
                        neutral ∎))
         (λ {x} {y} p q →
                        (((x add y) add ((inv x) add (inv y)))   ≡⟨ cong (λ X → X add ((inv x) add (inv y))) (addComm x y) ⟩
                        ((y add x) add (inv x add inv y))        ≡⟨ sym (addAssoc y x (inv x add inv y)) ⟩
                        (y add (x add (inv x add inv y)))        ≡⟨ cong (λ X → y add X) (addAssoc x (inv x) (inv y)) ⟩
                        (y add ((x add inv x) add inv y))        ≡⟨ cong (λ X → y add (X add (inv y))) (p) ⟩
                        (y add (neutral add inv y))              ≡⟨ cong (λ X → y add X) (addComm neutral (inv y)) ⟩
                        (y add (inv y add neutral))              ≡⟨ cong (λ X → y add X) (addRid (inv y)) ⟩
                        (y add inv y)                            ≡⟨ q ⟩
                        neutral ∎))

module SubstLemma
  (Idx : Type ℓ)
  (G    : Idx → Type ℓ')
  (Gstr : (r : Idx) → AbGroupStr (G r))
  where

  open AbGroupStr

  subst0g : {l k : Idx} → (p : l ≡ k) → subst G p (0g (Gstr l)) ≡ 0g (Gstr k)
  subst0g {l} {k} p = J (λ k p → subst G p (0g (Gstr l)) ≡ 0g (Gstr k)) (transportRefl _) p

  subst+ : {l : Idx} → (a b : G l) → {k : Idx} →  (p : l ≡ k) →
           Gstr k ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr l ._+_ a b)
  subst+ {l} a b {k} p = J (λ k p → Gstr k ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr l ._+_ a b))
                         (cong₂ (Gstr l ._+_) (transportRefl _) (transportRefl _) ∙ sym (transportRefl _))
                         p

module DecIndec-BaseProperties
  (Idx  : Type ℓ)
  (decIdx : Discrete Idx)
  (G    : Idx → Type ℓ')
  (Gstr : (r : Idx) → AbGroupStr (G r))
  where

  open AbGroupStr
  open SubstLemma Idx G Gstr

  πₖ : (k : Idx) → ⊕HIT Idx G Gstr → G k
  πₖ k = DS-Rec-Set.f _ _ _ _ (is-set (Gstr k))
         (0g (Gstr k))
         base-trad
         (_+_ (Gstr k))
         (+Assoc (Gstr k))
         (+IdR (Gstr k))
         (+Comm (Gstr k))
         base-neutral-eq
         base-add-eq
     where
     base-trad : (l : Idx) → (a : G l) → G k
     base-trad l a with decIdx l k
     ... | yes p = subst G p a
     ... | no ¬p = 0g (Gstr k)

     base-neutral-eq : _
     base-neutral-eq l with decIdx l k
     ... | yes p = subst0g p
     ... | no ¬p = refl

     base-add-eq : _
     base-add-eq l a b with decIdx l k
     ... | yes p = subst+ a b p
     ... | no ¬p = +IdR (Gstr k) _

  πₖ-id : {k : Idx} → (a : G k) → πₖ k (base k a) ≡ a
  πₖ-id {k} a with decIdx k k
  ... | yes p = cong (λ X → subst G X a) (Discrete→isSet decIdx _ _ _ _) ∙ transportRefl _
  ... | no ¬p = rec (¬p refl)

  πₖ-0g : {k l : Idx} → (a : G l) → (p : k ≡ l → ⊥) → πₖ k (base l a) ≡ 0g (Gstr k)
  πₖ-0g {k} {l} a ¬q with decIdx l k
  ... | yes p = rec (¬q (sym p))
  ... | no ¬p = refl

  base-inj : {k : Idx} → {a b : G k} → base {AGP = Gstr} k a ≡ base k b → a ≡ b
  base-inj {k} {a} {b} p = sym (πₖ-id a) ∙ cong (πₖ k) p ∙ πₖ-id b

  base-≢ : {k : Idx} → {a : G k} → {l : Idx} → {b : G l} → (p : k ≡ l → ⊥) →
           base {AGP = Gstr} k a ≡ base {AGP = Gstr} l b → (a ≡ 0g (Gstr k)) × (b ≡ 0g (Gstr l))
  base-≢ {k} {a} {l} {b} ¬p q = helper1 , helper2
    where
    helper1 : a ≡ 0g (Gstr k)
    helper1 = sym (πₖ-id a) ∙ cong (πₖ k) q ∙ πₖ-0g b ¬p

    helper2 : b ≡ 0g (Gstr l)
    helper2 = sym (πₖ-id b) ∙ cong (πₖ l) (sym q) ∙ πₖ-0g a (λ x → ¬p (sym x))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Check that unquoted functions are termination checked.
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection

`⊥ : Type
`⊥ = def (quote ⊥) []

{-
Generate
  aux : ⊥
  aux = aux

  loop : ⊥
  loop = aux
-}
makeLoop : QName → TC ⊤
makeLoop loop =
  freshName "aux" >>= λ aux →
  declareDef (vArg aux) `⊥ >>= λ _ →
  defineFun aux (clause [] (def aux []) ∷ []) >>= λ _ →
  declareDef (vArg loop) `⊥ >>= λ _ →
  defineFun loop (clause [] (def aux []) ∷ [])

unquoteDecl loop = makeLoop loop

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions for types of functions that only require an equality
-- relation over the domain.
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

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

open import Relation.Binary

module Function.Definitions.Core1
  {a ℓ₁} {A : Set a} (_≈₁_ : Rel A ℓ₁)
  where

open import Level using (_⊔_)

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

-- (Note the name `RightInverse` is used for the bundle)
Inverseʳ : ∀ {b} {B : Set b} → (A → B) → (B → A) → Set (a ⊔ ℓ₁)
Inverseʳ f g = ∀ x → g (f x) ≈₁ x


text:
------------------------------------------------------------------------
-- Parsers containing non-terminals, and grammars using such parsers
------------------------------------------------------------------------

module StructurallyRecursiveDescentParsing.Grammar where

open import Data.Bool
open import Data.Empty
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Codata.Musical.Notation
open import Level

open import StructurallyRecursiveDescentParsing.Index
import StructurallyRecursiveDescentParsing.Simplified as Simplified
open Simplified hiding (Parser; module Parser; ⟦_⟧)

infixl 10 _!>>=_ _?>>=_
infixl  5 _∣_

-- The parsers are parameterised on a type of nonterminals.

data Parser (NT : NonTerminalType) (Tok : Set) : NonTerminalType where
  return : ∀ {R} (x : R) → Parser NT Tok (true ◇ ε) R

  fail   : ∀ {R} → Parser NT Tok (false ◇ ε) R

  token  : Parser NT Tok (false ◇ ε) Tok

  _∣_    : ∀ {e₁ e₂ c₁ c₂ R}
           (p₁ : Parser NT Tok (e₁      ◇ c₁     ) R)
           (p₂ : Parser NT Tok (     e₂ ◇      c₂) R) →
                 Parser NT Tok (e₁ ∨ e₂ ◇ c₁ ∪ c₂) R

  _?>>=_ : ∀ {e₂ c₁ c₂ R₁ R₂}
           (p₁ :      Parser NT Tok (true ◇ c₁     ) R₁)
           (p₂ : R₁ → Parser NT Tok (e₂   ◇      c₂) R₂) →
                      Parser NT Tok (e₂   ◇ c₁ ∪ c₂) R₂

  _!>>=_ : ∀ {c₁ R₁ R₂} {i₂ : R₁ → Index}
           (p₁ :               Parser NT Tok (false ◇ c₁) R₁)
           (p₂ : (x : R₁) → ∞ (Parser NT Tok (i₂ x)       R₂)) →
                               Parser NT Tok (false ◇ c₁) R₂

  !      : ∀ {e c R} (nt : NT (e ◇ c) R) → Parser NT Tok (e ◇ c ∪ ε) R

-- Grammars.

Grammar : NonTerminalType → Set → Set1
Grammar NT Tok = ∀ {i R} → NT i R → Parser NT Tok i R

-- An empty non-terminal type.

EmptyNT : NonTerminalType
EmptyNT _ _ = Lift _ ⊥

-- An empty grammar.

emptyGrammar : ∀ {Tok} → Grammar EmptyNT Tok
emptyGrammar (lift ())

-- The semantics of grammar-based parsers is defined in terms of their
-- translation into "plain" parsers. The translation instantiates all
-- non-terminals corecursively.

⟦_⟧ : ∀ {Tok NT e c R} →
      Parser NT Tok (e ◇ c) R → Grammar NT Tok →
      Simplified.Parser Tok e R
⟦ return x   ⟧ g = return x
⟦ fail       ⟧ g = fail
⟦ token      ⟧ g = token
⟦ p₁ ∣ p₂    ⟧ g = ⟦ p₁ ⟧ g ∣ ⟦ p₂ ⟧ g
⟦ p₁ ?>>= p₂ ⟧ g = ⟦ p₁ ⟧ g ?>>= λ x →   ⟦    p₂ x  ⟧ g
⟦ p₁ !>>= p₂ ⟧ g = ⟦ p₁ ⟧ g !>>= λ x → ♯ ⟦ ♭ (p₂ x) ⟧ g
⟦ ! nt       ⟧ g = ⟦ g nt ⟧ g

-- Note that some "plain" parsers cannot be directly rewritten using
-- the parser type in this module (although there may be /equivalent/
-- parsers):

private

  only-plain : Simplified.Parser Bool false Bool
  only-plain = return true ?>>= λ x →
               if x then token else token ∣ token

  -- The following code does not type-check.

  -- doesnt-work : Parser EmptyNT Bool (false ◇ _) Bool
  -- doesnt-work = return true ?>>= λ x →
  --               if x then token else token ∣ token

-- A map function which can be useful when combining grammars.

mapNT : ∀ {NT₁ NT₂ Tok i R} →
        (∀ {i R} → NT₁ i R → NT₂ i R) →
        Parser NT₁ Tok i R → Parser NT₂ Tok i R
mapNT f (return x)   = return x
mapNT f fail         = fail
mapNT f token        = token
mapNT f (p₁ ∣ p₂)    = mapNT f p₁ ∣ mapNT f p₂
mapNT f (p₁ ?>>= p₂) = mapNT f p₁ ?>>= λ x →   mapNT f    (p₂ x)
mapNT f (p₁ !>>= p₂) = mapNT f p₁ !>>= λ x → ♯ mapNT f (♭ (p₂ x))
mapNT f (! nt)       = ! (f nt)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


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

open import Level
open import Function renaming (id to idᶠ; _∘_ to _©_)

open import Categories.Support.PropositionalEquality

open import Categories.Category
import Categories.Morphisms as Mor

open import Relation.Binary hiding (_⇒_)

module GlueSquares {o ℓ e} (C : Category o ℓ e) where
  private module C = Category C
  open C
  open Mor C

  module Pulls {X Y Z} {a : Y ⇒ Z} {b : X ⇒ Y} {c : X ⇒ Z} (ab≡c : a ∘ b ≡ c) where
    .pullʳ : ∀ {W} {f : Z ⇒ W} → (f ∘ a) ∘ b ≡ f ∘ c
    pullʳ {f = f} =
      begin
        (f ∘ a) ∘ b
      ↓⟨ assoc ⟩
        f ∘ (a ∘ b)
      ↓⟨ ∘-resp-≡ʳ ab≡c ⟩
        f ∘ c
      ∎
      where open HomReasoning

    .pullˡ : ∀ {W} {f : W ⇒ X} → a ∘ (b ∘ f) ≡ c ∘ f
    pullˡ {f = f} =
      begin
        a ∘ (b ∘ f)
      ↑⟨ assoc ⟩
        (a ∘ b) ∘ f
      ↓⟨ ∘-resp-≡ˡ ab≡c ⟩
        c ∘ f
      ∎
      where open HomReasoning

  open Pulls public

  module Pushes {X Y Z} {a : Y ⇒ Z} {b : X ⇒ Y} {c : X ⇒ Z} (c≡ab : c ≡ a ∘ b) where
    .pushʳ : ∀ {W} {f : Z ⇒ W} → f ∘ c ≡ (f ∘ a) ∘ b
    pushʳ {f = f} =
      begin
        f ∘ c
      ↓⟨ ∘-resp-≡ʳ c≡ab ⟩
        f ∘ (a ∘ b)
      ↑⟨ assoc ⟩
        (f ∘ a) ∘ b
      ∎
      where open HomReasoning

    .pushˡ : ∀ {W} {f : W ⇒ X} → c ∘ f ≡ a ∘ (b ∘ f)
    pushˡ {f = f} =
      begin
        c ∘ f
      ↓⟨ ∘-resp-≡ˡ c≡ab ⟩
        (a ∘ b) ∘ f
      ↓⟨ assoc ⟩
        a ∘ (b ∘ f)
      ∎
      where open HomReasoning

  open Pushes public

  module IntroElim {X} {a : X ⇒ X} (a≡id : a ≡ id) where
    .elimʳ : ∀ {W} {f : X ⇒ W} → (f ∘ a) ≡ f
    elimʳ {f = f} =
      begin
        f ∘ a
      ↓⟨ ∘-resp-≡ʳ a≡id ⟩
        f ∘ id
      ↓⟨ identityʳ ⟩
        f
      ∎
      where
      open HomReasoning

    .introʳ : ∀ {W} {f : X ⇒ W} → f ≡ f ∘ a
    introʳ = Equiv.sym elimʳ

    .elimˡ : ∀ {W} {f : W ⇒ X} → (a ∘ f) ≡ f
    elimˡ {f = f} =
      begin
        a ∘ f
      ↓⟨ ∘-resp-≡ˡ a≡id ⟩
        id ∘ f
      ↓⟨ identityˡ ⟩
        f
      ∎
      where
      open HomReasoning

    .introˡ : ∀ {W} {f : W ⇒ X} → f ≡ a ∘ f
    introˡ = Equiv.sym elimˡ

  open IntroElim public

  module Extends {X Y Z W} {f : X ⇒ Y} {g : X ⇒ Z} {h : Y ⇒ W} {i : Z ⇒ W} (s : CommutativeSquare f g h i) where
    .extendˡ : ∀ {A} {a : W ⇒ A} → CommutativeSquare f g (a ∘ h) (a ∘ i)
    extendˡ {a = a} =
      begin
        (a ∘ h) ∘ f
      ↓⟨ pullʳ s ⟩
        a ∘ i ∘ g
      ↑⟨ assoc ⟩
        (a ∘ i) ∘ g
      ∎
      where
      open HomReasoning

    .extendʳ : ∀ {A} {a : A ⇒ X} → CommutativeSquare (f ∘ a) (g ∘ a) h i
    extendʳ {a = a} =
      begin
        h ∘ (f ∘ a)
      ↓⟨ pullˡ s ⟩
        (i ∘ g) ∘ a
      ↓⟨ assoc ⟩
        i ∘ (g ∘ a)
      ∎
      where
      open HomReasoning

    .extend² : ∀ {A B} {a : W ⇒ A} {b : B ⇒ X} → CommutativeSquare (f ∘ b) (g ∘ b) (a ∘ h) (a ∘ i)
    extend² {a = a} {b} =
      begin
        (a ∘ h) ∘ (f ∘ b)
      ↓⟨ pullʳ extendʳ ⟩
        a ∘ (i ∘ (g ∘ b))
      ↑⟨ assoc ⟩
        (a ∘ i) ∘ (g ∘ b)
      ∎
      where
      open HomReasoning

  open Extends public

  -- essentially composition in the arrow category
  .glue : {X Y Y′ Z Z′ W : Obj} {a : Z ⇒ W} {a′ : Y′ ⇒ Z′} {b : Y ⇒ Z} {b′ : X ⇒ Y′} {c : X ⇒ Y} {c′ : Y′ ⇒ Z} {c″ : Z′ ⇒ W} → CommutativeSquare c′ a′ a c″ → CommutativeSquare c b′ b c′ → CommutativeSquare c (a′ ∘ b′) (a ∘ b) c″
  glue {a = a} {a′} {b} {b′} {c} {c′} {c″} sq-a sq-b =
    begin
      (a ∘ b) ∘ c
    ↓⟨ pullʳ sq-b ⟩
      a ∘ (c′ ∘ b′)
    ↓⟨ pullˡ sq-a ⟩
      (c″ ∘ a′) ∘ b′
    ↓⟨ assoc ⟩
      c″ ∘ (a′ ∘ b′)
    ∎
    where
    open HomReasoning

  .glue◃◽ : {X Y Y′ Z W : Obj} {a : Z ⇒ W} {b : Y ⇒ Z} {b′ : X ⇒ Y′} {c : X ⇒ Y} {c′ : Y′ ⇒ Z} {c″ : Y′ ⇒ W} → a ∘ c′ ≡ c″ → CommutativeSquare c b′ b c′ → CommutativeSquare c b′ (a ∘ b) c″
  glue◃◽ {a = a} {b} {b′} {c} {c′} {c″} tri-a sq-b =
    begin
      (a ∘ b) ∘ c
    ↓⟨ pullʳ sq-b ⟩
      a ∘ (c′ ∘ b′)
    ↓⟨ pullˡ tri-a ⟩
      c″ ∘ b′
    ∎
    where
    open HomReasoning

  -- essentially composition in the over category
  .glueTrianglesʳ : ∀ {X X′ X″ Y} {a : X ⇒ Y} {b : X′ ⇒ X} {a′ : X′ ⇒ Y} {b′ : X″ ⇒ X′} {a″ : X″ ⇒ Y}
    → a ∘ b ≡ a′ → a′ ∘ b′ ≡ a″ → a ∘ (b ∘ b′) ≡ a″
  glueTrianglesʳ {a = a} {b} {a′} {b′} {a″} a∘b≡a′ a′∘b′≡a″ =
    begin
      a ∘ (b ∘ b′)
    ↓⟨ pullˡ a∘b≡a′ ⟩
      a′ ∘ b′
    ↓⟨ a′∘b′≡a″ ⟩
      a″
    ∎
    where open HomReasoning

  -- essentially composition in the under category
  .glueTrianglesˡ : ∀ {X Y Y′ Y″} {b : X ⇒ Y} {a : Y ⇒ Y′} {b′ : X ⇒ Y′} {a′ : Y′ ⇒ Y″} {b″ : X ⇒ Y″} → a′ ∘ b′ ≡ b″ → a ∘ b ≡ b′ → (a′ ∘ a) ∘ b ≡ b″
  glueTrianglesˡ {b = b} {a} {b′} {a′} {b″} a′∘b′≡b″ a∘b≡b′ =
    begin
      (a′ ∘ a) ∘ b
    ↓⟨ pullʳ a∘b≡b′ ⟩
      a′ ∘ b′
    ↓⟨ a′∘b′≡b″ ⟩
      b″
    ∎
    where open HomReasoning

  module Cancellers {Y Y′ : Obj} {h : Y′ ⇒ Y} {i : Y ⇒ Y′} (inv : h ∘ i ≡ id) where

    .cancelRight : ∀ {Z} {f : Y ⇒ Z} → (f ∘ h) ∘ i ≡ f
    cancelRight {f = f} =
      begin
        (f ∘ h) ∘ i
      ↓⟨ pullʳ inv ⟩
        f ∘ id
      ↓⟨ identityʳ ⟩
        f
      ∎
      where open HomReasoning

    .cancelLeft : ∀ {X} {f : X ⇒ Y} → h ∘ (i ∘ f) ≡ f
    cancelLeft {f = f} =
      begin
        h ∘ (i ∘ f)
      ↓⟨ pullˡ inv ⟩
        id ∘ f
      ↓⟨ identityˡ ⟩
        f
      ∎
      where open HomReasoning

    .cancelInner : ∀ {X Z} {f : Y ⇒ Z} {g : X ⇒ Y} → (f ∘ h) ∘ (i ∘ g) ≡ f ∘ g
    cancelInner {f = f} {g} =
      begin
        (f ∘ h) ∘ (i ∘ g)
      ↓⟨ pullˡ cancelRight ⟩
        f ∘ g
      ∎
      where open HomReasoning

  open Cancellers public

  module Switch {X Y} (i : X ≅ Y) where
    open _≅_ i

    .switch-fgˡ : ∀ {W} {h : W ⇒ X} {k : W ⇒ Y} → (f ∘ h ≡ k) → (h ≡ g ∘ k)
    switch-fgˡ {h = h} {k} pf =
      begin
        h
      ↑⟨ cancelLeft isoˡ ⟩
        g ∘ (f ∘ h)
      ↓⟨ ∘-resp-≡ʳ pf ⟩
        g ∘ k
      ∎
      where open HomReasoning

    .switch-gfˡ : ∀ {W} {h : W ⇒ Y} {k : W ⇒ X} → (g ∘ h ≡ k) → (h ≡ f ∘ k)
    switch-gfˡ {h = h} {k} pf =
      begin
        h
      ↑⟨ cancelLeft isoʳ ⟩
        f ∘ (g ∘ h)
      ↓⟨ ∘-resp-≡ʳ pf ⟩
        f ∘ k
      ∎
      where open HomReasoning

    .switch-fgʳ : ∀ {W} {h : Y ⇒ W} {k : X ⇒ W} → (h ∘ f ≡ k) → (h ≡ k ∘ g)
    switch-fgʳ {h = h} {k} pf =
      begin
        h
      ↑⟨ cancelRight isoʳ ⟩
        (h ∘ f) ∘ g
      ↓⟨ ∘-resp-≡ˡ pf ⟩
        k ∘ g
      ∎
      where open HomReasoning

    .switch-gfʳ : ∀ {W} {h : X ⇒ W} {k : Y ⇒ W} → (h ∘ g ≡ k) → (h ≡ k ∘ f)
    switch-gfʳ {h = h} {k} pf =
      begin
        h
      ↑⟨ cancelRight isoˡ ⟩
        (h ∘ g) ∘ f
      ↓⟨ ∘-resp-≡ˡ pf ⟩
        k ∘ f
      ∎
      where open HomReasoning

  open Switch public

module Yon-Eda {o ℓ e} (C : Category o ℓ e) where
  private module C = Category C
  open C
  open Equiv
  record Yon (X Y : Obj) : Set (o ⊔ ℓ ⊔ e) where
    field
      arr : X ⇒ Y
      fun : ∀ {W} (f : W ⇒ X) → (W ⇒ Y)
      .ok : ∀ {W} (f : W ⇒ X) → fun f ≡ arr ∘ f

    norm : X ⇒ Y
    norm = fun id

    .norm≡arr : norm ≡ arr
    norm≡arr = trans (ok id) identityʳ

  record _≡′_ {X Y : Obj} (f g : Yon X Y) : Set (o ⊔ ℓ ⊔ e) where
    constructor yeq
    field
      arr-≡ : Yon.arr f ≡ Yon.arr g

  open _≡′_ public using (arr-≡)

  module _ {X Y} where
    .Yon-refl : Reflexive (_≡′_ {X} {Y})
    Yon-refl = yeq refl
    .Yon-sym : Symmetric (_≡′_ {X} {Y})
    Yon-sym = yeq © sym © arr-≡
    .Yon-trans : Transitive (_≡′_ {X} {Y})
    Yon-trans eq eq′ = yeq (trans (arr-≡ eq) (arr-≡ eq′))

  Yon-id : ∀ {X} → Yon X X
  Yon-id = record
    { arr = id
    ; fun = idᶠ
    ; ok = λ _ → sym identityˡ
    }

  Yon-inject : ∀ {X Y} → (X ⇒ Y) → Yon X Y
  Yon-inject f = record { arr = f; fun = _∘_ f; ok = λ _ → refl }

  Yon-compose : ∀ {X Y Z} → (Yon Y Z) → (Yon X Y) → (Yon X Z)
  Yon-compose g f = record
    { arr = g.fun f.arr
    ; fun = g.fun © f.fun
    ; ok = λ h → trans (g.ok (f.fun h)) (trans (∘-resp-≡ʳ (f.ok h)) (trans (sym assoc) (sym (∘-resp-≡ˡ (g.ok f.arr)))))
    }
    where
    module g = Yon g
    module f = Yon f

  .Yon-assoc : ∀ {X Y Z W} (f : Yon Z W) (g : Yon Y Z) (h : Yon X Y) → Yon-compose f (Yon-compose g h) ≣ Yon-compose (Yon-compose f g) h
  Yon-assoc f g h = ≣-refl

  .Yon-identityˡ : ∀ {X Y} (f : Yon X Y) → Yon-compose Yon-id f ≣ f
  Yon-identityˡ f = ≣-refl

  .Yon-identityʳ : ∀ {X Y} (f : Yon X Y) → Yon-compose f Yon-id ≡′ f
  Yon-identityʳ f = yeq (Yon.norm≡arr f)

  .Yon-compose-resp-≡′ : ∀ {X Y Z} {f f′ : Yon Y Z} {g g′ : Yon X Y}
                         → f ≡′ f′ → g ≡′ g′
                         → Yon-compose f g ≡′ Yon-compose f′ g′
  Yon-compose-resp-≡′ {f = f} {f′} {g} {g′} f≡′f′ g≡′g′
    = yeq (trans (Yon.ok f (Yon.arr g))
           (trans (∘-resp-≡ (arr-≡ f≡′f′) (arr-≡ g≡′g′))
            (sym (Yon.ok f′ (Yon.arr g′)))))

  record Eda (X Y : Obj) : Set (o ⊔ ℓ ⊔ e) where
    field
      yon : Yon X Y
      fun : ∀ {Z} (f : Yon Y Z) → Yon X Z
      .ok : ∀ {Z} (f : Yon Y Z) → fun f ≡′ Yon-compose f yon

    norm : Yon X Y
    norm = fun Yon-id

    open Yon yon public using (arr)

  Eda-id : ∀ {X} → Eda X X
  Eda-id = record
    { yon = Yon-id
    ; fun = idᶠ
    ; ok = yeq © sym © arr-≡ © Yon-identityʳ
    }

  Eda-inject : ∀ {X Y} → Yon X Y → Eda X Y
  Eda-inject f = record { yon = f; fun = flip Yon-compose f; ok = λ _ → yeq refl }

  Eda-compose : ∀ {X Y Z} → (Eda Y Z) → (Eda X Y) → (Eda X Z)
  Eda-compose {X} {Y} {Z} g f = record
    { yon = f.fun g.yon
    ; fun = f.fun © g.fun
    ; ok = λ {W} h → Yon-trans {X} {W} {f.fun (g.fun h)} (f.ok (g.fun h))
                  (Yon-trans (Yon-compose-resp-≡′ (g.ok h) (Yon-refl {x = f.yon}))
                   (Yon-sym (Yon-compose-resp-≡′ (Yon-refl {x = h}) (f.ok g.yon))))
    }
    where
    module g = Eda g
    module f = Eda f

  .Eda-assoc : ∀ {X Y Z W} (f : Eda Z W) (g : Eda Y Z) (h : Eda X Y) → Eda-compose f (Eda-compose g h) ≣ Eda-compose (Eda-compose f g) h
  Eda-assoc f g h = ≣-refl

  -- .Eda-identityˡ : ∀ {X Y} (f : Eda X Y) → Eda-compose Eda-id f ≣ f
  -- Eda-identityˡ f = {!!}

  .Eda-identityʳ : ∀ {X Y} (f : Eda X Y) → Eda-compose f Eda-id ≣ f
  Eda-identityʳ f = ≣-refl

record NormReasoning {o ℓ e} (C : Category o ℓ e) (o′ ℓ′ : _) : Set (suc o′ ⊔ o ⊔ ℓ ⊔ e ⊔ suc ℓ′) where
  private module C = Category C
  field
    U : Set o′
    T : U -> C.Obj
    _#⇒_ : U -> U -> Set ℓ′
    eval : ∀ {A B} -> A #⇒ B -> T A C.⇒ T B
    norm : ∀ {A B} -> A #⇒ B -> T A C.⇒ T B
    .norm≡eval : ∀ {A B} (f : A #⇒ B) -> norm f C.≡ eval f

  open C.Equiv
  open C

  infix  4 _IsRelatedTo_
  infix  1 begin_
  infixr 2 _≈⟨_⟩_ _↓⟨_⟩_ _↑⟨_⟩_ _↓≡⟨_⟩_ _↑≡⟨_⟩_ _↕_
  infix  3 _∎

  data _IsRelatedTo_ {X Y} (f g : _#⇒_ X Y) : Set e where
    relTo : (f∼g : norm f ≡ norm g) → f IsRelatedTo g

  .begin_ : ∀ {X Y} {f g : _#⇒_ X Y} → f IsRelatedTo g → eval f ≡ eval g
  begin_ {f = f} {g} (relTo f∼g) = trans (sym (norm≡eval f)) (trans f∼g (norm≡eval g))

  ._↓⟨_⟩_ : ∀ {X Y} (f : _#⇒_ X Y) {g h} → (norm f ≡ norm g) → g IsRelatedTo h → f IsRelatedTo h
  _ ↓⟨ f∼g ⟩ relTo g∼h = relTo (trans f∼g g∼h)

  ._↑⟨_⟩_ : ∀ {X Y} (f : _#⇒_ X Y) {g h} → (norm g ≡ norm f) → g IsRelatedTo h → f IsRelatedTo h
  _ ↑⟨ g∼f ⟩ relTo g∼h = relTo (trans (sym g∼f) g∼h)

  -- the syntax of the ancients, for compatibility
  ._≈⟨_⟩_ : ∀ {X Y} (f : _#⇒_ X Y) {g h} → (norm f ≡ norm g) → g IsRelatedTo h → f IsRelatedTo h
  _ ≈⟨ f∼g ⟩ relTo g∼h = relTo (trans f∼g g∼h)

  ._↓≡⟨_⟩_ : ∀ {X Y} (f : _#⇒_ X Y) {g h} → eval f ≡ eval g → g IsRelatedTo h → f IsRelatedTo h
  _↓≡⟨_⟩_ f {g} f∼g (relTo g∼h) = relTo (trans (norm≡eval f) (trans f∼g (trans (sym (norm≡eval g)) g∼h)))

  ._↑≡⟨_⟩_ : ∀ {X Y} (f : _#⇒_ X Y) {g h} → eval g ≡ eval f → g IsRelatedTo h → f IsRelatedTo h
  _↑≡⟨_⟩_ f {g} g∼f (relTo g∼h) = relTo (trans (norm≡eval f) (trans (sym g∼f) (trans (sym (norm≡eval g)) g∼h)))

  ._↕_ : ∀ {X Y} (f : _#⇒_ X Y) {h} → f IsRelatedTo h → f IsRelatedTo h
  _ ↕ f∼h = f∼h

  ._∎ : ∀ {X Y} (f : _#⇒_ X Y) → f IsRelatedTo f
  _∎ _ = relTo refl

  .by_ : ∀ {X Y} {f g h : X ⇒ Y} -> ((h ≡ h) -> f ≡ g) -> f ≡ g
  by eq = eq refl

  .computation : ∀ {X Y} (f g : X #⇒ Y) -> norm f ≡ norm g → eval f ≡ eval g
  computation f g eq = begin f ↓⟨ eq ⟩ g ∎

module AUReasoning {o ℓ e} (C : Category o ℓ e) where
  private module C = Category C
  open C
  open Equiv
{-
  infix  4 _IsRelatedTo_
  infix  2 _∎
  infixr 2 _≈⟨_⟩_
  infixr 2 _↓⟨_⟩_
  infixr 2 _↑⟨_⟩_
  infixr 2 _↓≡⟨_⟩_
  infixr 2 _↑≡⟨_⟩_
  infixr 2 _↕_
  infix  1 begin_
-}
  infixr 8 _∙_

  open Yon-Eda C public

  data Climb : Rel Obj (o ⊔ ℓ) where
    ID : ∀ {X} → Climb X X
    leaf : ∀ {X Y} → (X ⇒ Y) → Climb X Y
    _branch_ : ∀ {X Y Z} (l : Climb Y Z) (r : Climb X Y) → Climb X Z

  interp : ∀ {p} (P : Rel Obj p)
           (f-id : ∀ {X} → P X X)
           (f-leaf : ∀ {X Y} → X ⇒ Y → P X Y)
           (f-branch : ∀ {X Y Z} → P Y Z → P X Y → P X Z)
         → ∀ {X Y} → Climb X Y → P X Y
  interp P f-id f-leaf f-branch ID = f-id
  interp P f-id f-leaf f-branch (leaf y) = f-leaf y
  interp P f-id f-leaf f-branch (l branch r) = f-branch
    (interp P f-id f-leaf f-branch l)
    (interp P f-id f-leaf f-branch r)

  eval : ∀ {X Y} → Climb X Y → X ⇒ Y
  eval = interp _⇒_ id idᶠ _∘_

  yeval : ∀ {X Y} → Climb X Y → Yon X Y
  yeval = interp Yon Yon-id Yon-inject Yon-compose

  .yarr : ∀ {X Y} → (t : Climb X Y) → Yon.arr (yeval t) ≡ eval t
  yarr ID = refl
  yarr (leaf y) = refl
  yarr (t branch t1) = trans (Yon.ok (yeval t) (Yon.arr (yeval t1))) (∘-resp-≡ (yarr t) (yarr t1))

  eeval : ∀ {X Y} → Climb X Y → Eda X Y
  eeval = interp Eda Eda-id (Eda-inject © Yon-inject) Eda-compose

  .eyon : ∀ {X Y} → (t : Climb X Y) → Eda.yon (eeval t) ≡′ yeval t
  eyon ID = Yon-refl
  eyon (leaf y) = Yon-refl
  eyon (t branch t1) = Yon-trans (Eda.ok (eeval t1) (Eda.yon (eeval t)))
                                 (Yon-compose-resp-≡′ (eyon t) (eyon t1))

  .earr : ∀ {X Y} → (t : Climb X Y) → Eda.arr (eeval t) ≡ eval t
  earr t = trans (arr-≡ (eyon t)) (yarr t)

  yyeval : ∀ {X Y} → (t : Climb X Y) → (X ⇒ Y)
  yyeval = Eda.arr © eeval

  record ClimbBuilder (X Y : Obj) {t} (T : Set t) : Set (o ⊔ ℓ ⊔ t) where
    field build : T → Climb X Y

  instance
    leafBuilder : ∀ {X Y} → ClimbBuilder X Y (X ⇒ Y)
    leafBuilder = record { build = leaf }

    idBuilder : ∀ {X Y} → ClimbBuilder X Y (Climb X Y)
    idBuilder = record { build = idᶠ }

  _∙_ : ∀ {X Y Z} {s} {S : Set s} {{Sb : ClimbBuilder Y Z S}} (f : S) {t} {T : Set t} {{Tb : ClimbBuilder X Y T}} (g : T) → Climb X Z
  _∙_ {{Sb}} f {{Tb}} g = ClimbBuilder.build Sb f branch ClimbBuilder.build Tb g

  aureasoning : NormReasoning C o (ℓ ⊔ o)
  aureasoning = record
                  { U = Obj
                  ; T = λ A → A
                  ; _#⇒_ = Climb
                  ; eval = eval
                  ; norm = yyeval
                  ; norm≡eval = earr
                  }

  open NormReasoning aureasoning public hiding (eval)

{-
  data _IsRelatedTo_ {X Y} (f g : Climb X Y) : Set e where
    relTo : (f∼g : yyeval f ≡ yyeval g) → f IsRelatedTo g

  .begin_ : ∀ {X Y} {f g : Climb X Y} → f IsRelatedTo g → eval f ≡ eval g
  begin_ {f = f} {g} (relTo f∼g) = trans (sym (earr f)) (trans f∼g (earr g))

  ._↓⟨_⟩_ : ∀ {X Y} (f : Climb X Y) {g h} → (yyeval f ≡ yyeval g) → g IsRelatedTo h → f IsRelatedTo h
  _ ↓⟨ f∼g ⟩ relTo g∼h = relTo (trans f∼g g∼h)

  ._↑⟨_⟩_ : ∀ {X Y} (f : Climb X Y) {g h} → (yyeval g ≡ yyeval f) → g IsRelatedTo h → f IsRelatedTo h
  _ ↑⟨ g∼f ⟩ relTo g∼h = relTo (trans (sym g∼f) g∼h)

  -- the syntax of the ancients, for compatibility
  ._≈⟨_⟩_ : ∀ {X Y} (f : Climb X Y) {g h} → (yyeval f ≡ yyeval g) → g IsRelatedTo h → f IsRelatedTo h
  _ ≈⟨ f∼g ⟩ relTo g∼h = relTo (trans f∼g g∼h)

  ._↓≡⟨_⟩_ : ∀ {X Y} (f : Climb X Y) {g h} → eval f ≡ eval g → g IsRelatedTo h → f IsRelatedTo h
  _↓≡⟨_⟩_ f {g} f∼g (relTo g∼h) = relTo (trans (earr f) (trans f∼g (trans (sym (earr g)) g∼h)))

  ._↑≡⟨_⟩_ : ∀ {X Y} (f : Climb X Y) {g h} → eval g ≡ eval f → g IsRelatedTo h → f IsRelatedTo h
  _↑≡⟨_⟩_ f {g} g∼f (relTo g∼h) = relTo (trans (earr f) (trans (sym g∼f) (trans (sym (earr g)) g∼h)))
{-
  -- XXX i want this to work whenever the Edas are equal -- but that probably
  -- requires Climb to be indexed by yyeval!  oh, for cheap ornamentation.
  ._↕_ : ∀ {X Y} (f : Climb X Y) {h} → f IsRelatedTo h → f IsRelatedTo h
  _ ↕ f∼h = f∼h
-}
  ._∎ : ∀ {X Y} (f : Climb X Y) → f IsRelatedTo f
  _∎ _ = relTo refl
-}

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2016-06-09 issue during refactoring for #1963
-- Shrunk this issue with projection-like functions from std-lib

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.proj.like:10 #-}

open import Common.Level
open import Common.Nat renaming ( Nat to ℕ )

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

postulate anything : ∀{A : Set} → A

data _≤_ : (m n : ℕ) → Set where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

≤-refl : ∀{n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀{k l m} → k ≤ l → l ≤ m → k ≤ m
≤-trans z≤n q = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

n≤m+n : ∀ m n → n ≤ (m + n)
n≤m+n zero zero = z≤n
n≤m+n zero (suc n) = s≤s (n≤m+n zero n)
n≤m+n (suc m) zero = z≤n
n≤m+n (suc m) (suc n) = s≤s anything

record Preord c ℓ₁ : Set (lsuc (c ⊔ ℓ₁)) where
  infix 4 _∼_
  field
    Carrier    : Set c
    _∼_        : (x y : Carrier) → Set ℓ₁  -- The relation.
    refl       : ∀{x} → x ∼ x
    trans      : ∀{x y z} → x ∼ y → y ∼ z → x ∼ z

Npreord : Preord _ _
Npreord = record { Carrier = ℕ ; _∼_ = _≤_ ; refl = ≤-refl; trans = ≤-trans }

module Pre {p₁ p₂} (P : Preord p₁ p₂) where

  open Preord P

  infix  4 _IsRelatedTo_
  infix  3 _∎
  infixr 2 _≤⟨_⟩_
  infix  1 begin_

  data _IsRelatedTo_ (x y : Carrier) : Set p₂ where
    relTo : (x≤y : x ∼ y) → x IsRelatedTo y

  begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
  begin relTo x≤y = x≤y

  _≤⟨_⟩_ : ∀ x {y z} → x ∼ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≤⟨ x≤y ⟩ relTo y≤z = relTo (trans x≤y y≤z)

  _∎ : ∀ x → x IsRelatedTo x
  _∎ _ = relTo refl

-- begin_  :  {p₁ p₂ : Level} (P : Preord p₁ p₂)
--            {x y : Preord.Carrier P} →
--            x IsRelatedTo y → (P Preord.∼ x) y
--  is projection like in argument 5 for type ProjectionLike1963.Pre._IsRelatedTo_

-- _∎  :  {p₁ p₂ : Level} (P : Preord p₁ p₂) (x : Preord.Carrier P) →
--        x IsRelatedTo x
--  is projection like in argument 2 for type ProjectionLike1963.Preord

open Pre Npreord

_+-mono_ : ∀{m₁ m₂ n₁ n₂} → m₁ ≤ m₂ → n₁ ≤ n₂ → (m₁ + n₁) ≤ (m₂ + n₂)
_+-mono_ {zero} {m₂} {n₁} {n₂} z≤n n₁≤n₂ = begin
  n₁      ≤⟨ n₁≤n₂ ⟩
  n₂      ≤⟨ n≤m+n m₂ n₂ ⟩
  m₂ + n₂ ∎
s≤s m₁≤m₂ +-mono n₁≤n₂ = s≤s (m₁≤m₂ +-mono n₁≤n₂)

ISS : ∀ {n m} (p : n ≤ m) → Set
ISS z≤n     = ⊥
ISS (s≤s p) = ⊤

test : ISS ((z≤n {0}) +-mono (s≤s (z≤n {0})))
test = tt

-- Goal display:
--     C-u C-c C-,  ISS (z≤n +-mono s≤s z≤n)
--         C-c C-,  ISS (begin 1 ≤⟨ s≤s z≤n ⟩ 1 ≤⟨ s≤s z≤n ⟩ 1 ∎)
-- C-u C-u C-c C-,  ISS (λ {y} → Pre.begin _)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Level using (_⊔_; suc; Lift; lift)
open import Function using (_$_; _∘_; _⤖_)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary using (Rel; Decidable; Setoid; DecSetoid; IsEquivalence; IsDecEquivalence)

open import Data.Empty using (⊥)
open import Data.Product using (∃-syntax; _,_)
open import Data.Sum using (_⊎_)

module AKS.Algebra.Structures {c ℓ} (C : Set c) (_≈_ : Rel C ℓ) where

open import Data.Unit using (⊤; tt)
open import Agda.Builtin.FromNat using (Number)
open import AKS.Nat using (ℕ; _<_; _≟_)
open import AKS.Fin using (Fin)

open import Algebra.Core using (Op₂; Op₁)
open import Algebra.Structures _≈_ using (IsCommutativeRing; IsAbelianGroup)

infix 4 _≉_
_≉_ : Rel C ℓ
x ≉ y = x ≈ y → ⊥

record IsNonZeroCommutativeRing (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) : Set (c ⊔ ℓ) where
  field
    isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
    0#≉1# : 0# ≉ 1#

  open IsCommutativeRing isCommutativeRing public
  open import Relation.Binary.Reasoning.Setoid setoid
  open import Algebra.Properties.Ring (record { isRing = isRing }) using (-‿distribˡ-*; -‿involutive)

  1#≉0# : 1# ≉ 0#
  1#≉0# = 0#≉1# ∘ sym

  0#≉-1# : 0# ≉ - 1#
  0#≉-1# 0#≈-1# = 0#≉1# $ begin
    0#              ≈⟨ sym (zeroʳ 0#) ⟩
    0# * 0#         ≈⟨ *-cong 0#≈-1# 0#≈-1# ⟩
    (- 1#) * (- 1#) ≈⟨ sym (-‿distribˡ-* 1# (- 1#)) ⟩
    - (1# * (- 1#)) ≈⟨ -‿cong (*-identityˡ (- 1#)) ⟩
    - (- 1#)        ≈⟨ -‿involutive 1# ⟩
    1#              ∎

  -1#≉0# : - 1# ≉ 0#
  -1#≉0# = 0#≉-1# ∘ sym

  C/0 : Set (c ⊔ ℓ)
  C/0 = ∃[ x ] (x ≉ 0#)

  1#-nonzero : C/0
  1#-nonzero = 1# , 1#≉0#

  -1#-nonzero : C/0
  -1#-nonzero = - 1# , -1#≉0#

  fromNat : ℕ → C
  fromNat ℕ.zero = 0#
  fromNat (ℕ.suc ℕ.zero) = 1#
  fromNat (ℕ.suc (ℕ.suc n)) = 1# + fromNat (ℕ.suc n)

  instance
    C-number : Number C
    C-number = record
      { Constraint = λ _ → Lift c ⊤
      ; fromNat = λ n → fromNat n
      }

record IsIntegralDomain (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) : Set (c ⊔ ℓ) where
  field
    isNonZeroCommutativeRing : IsNonZeroCommutativeRing _+_ _*_ -_ 0# 1#
    *-cancelˡ : ∀ x {y z} → x ≉ 0# → (x * y) ≈ (x * z) → y ≈ z

  open IsNonZeroCommutativeRing isNonZeroCommutativeRing public
  open import Relation.Binary.Reasoning.Setoid setoid

  *-cancelʳ : ∀ x {y z} → x ≉ 0# → (y * x) ≈ (z * x) → y ≈ z
  *-cancelʳ x {y} {z} x≉0 y*x≈z*x = *-cancelˡ x x≉0 $ begin
    (x * y) ≈⟨ *-comm x y ⟩
    (y * x) ≈⟨ y*x≈z*x ⟩
    (z * x) ≈⟨ *-comm z x ⟩
    (x * z) ∎

  *≉0 : ∀ {c₁ c₂} → c₁ ≉ 0# → c₂ ≉ 0# → c₁ * c₂ ≉ 0#
  *≉0 {c₁} {c₂} c₁≉0 c₂≉0 c₁*c₂≈0 = c₂≉0 $ *-cancelˡ c₁ c₁≉0 $ begin
     (c₁ * c₂) ≈⟨ c₁*c₂≈0 ⟩
     (0#)      ≈⟨ sym (zeroʳ c₁) ⟩
     (c₁ * 0#) ∎

  infixl 7 _*-nonzero_
  _*-nonzero_ : C/0 → C/0 → C/0
  (c₁ , c₁≉0) *-nonzero (c₂ , c₂≉0) = c₁ * c₂ , *≉0 c₁≉0 c₂≉0

module Divisibility (_*_ : Op₂ C) where
  infix 4 _∣_
  record _∣_ (d : C) (a : C) : Set (c ⊔ ℓ) where
    constructor divides
    field
      quotient : C
      equality : a ≈ (quotient * d)

  infix 4 _∤_
  _∤_ : C → C → Set (c ⊔ ℓ)
  d ∤ a = ¬ (d ∣ a)

  record IsGCD (gcd : Op₂ C) : Set (c ⊔ ℓ) where
    field
      gcd[a,b]∣a : ∀ a b → gcd a b ∣ a
      gcd[a,b]∣b : ∀ a b → gcd a b ∣ b
      gcd-greatest : ∀ {c a b} → c ∣ a → c ∣ b → c ∣ gcd a b

record IsGCDDomain (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) (gcd : Op₂ C) : Set (c ⊔ ℓ) where
  open Divisibility _*_ public
  field
    isIntegralDomain : IsIntegralDomain _+_ _*_ -_ 0# 1#
    gcd-isGCD : IsGCD gcd

  open IsIntegralDomain isIntegralDomain public

record IsUniqueFactorizationDomain (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) (gcd : Op₂ C) : Set (c ⊔ ℓ) where
  field
    isGCDDomain : IsGCDDomain _+_ _*_ -_ 0# 1# gcd
    -- TODO define factorization

  open IsGCDDomain isGCDDomain public

module Modulus
  (0# : C) (∣_∣ : ∀ n {n≉0 : n ≉ 0#} → ℕ) (_mod_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  where
  data Remainder (n : C) (m : C) {m≉0 : m ≉ 0#} : Set (c ⊔ ℓ) where
    0≈ : (r≈0 : (n mod m) {m≉0} ≈ 0#) → Remainder n m
    0≉ : (r≉0 : (n mod m) {m≉0} ≉ 0#) → ∣ n mod m ∣ {r≉0} < ∣ m ∣ {m≉0} → Remainder n m

module _
  (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) (∣_∣ : ∀ n {n≉0 : n ≉ 0#} → ℕ)
  (_div_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C) (_mod_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  (gcd : Op₂ C)
  where

  record IsEuclideanDomain : Set (c ⊔ ℓ) where
    open Modulus 0# ∣_∣ _mod_ public
    field
      isUniqueFactorizationDomain : IsUniqueFactorizationDomain _+_ _*_ -_ 0# 1# gcd
      division : ∀ n m {m≉0 : m ≉ 0#} → n ≈ ((m * (n div m) {m≉0}) + (n mod m) {m≉0})
      modulus : ∀ n m {m≉0 : m ≉ 0#} → Remainder n m {m≉0}
      div-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ div y₁) {y₁≉0} ≈ (x₂ div y₂) {y₂≉0}
      mod-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ mod y₁) {y₁≉0} ≈ (x₂ mod y₂) {y₂≉0}

    open IsUniqueFactorizationDomain isUniqueFactorizationDomain public

record IsField (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C) (_/_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C) (gcd : Op₂ C) : Set (c ⊔ ℓ) where
  field
    isEuclideanDomain : IsEuclideanDomain _+_ _*_ -_ 0# 1# (λ _ → 0) _/_ (λ _ _ → 0#) gcd

  open IsEuclideanDomain isEuclideanDomain public renaming (div-cong to /-cong)
  open import Relation.Binary.Reasoning.Setoid setoid

  m*[n/m]≈n : ∀ n m {m≉0 : m ≉ 0#} → (m * (n / m) {m≉0}) ≈ n
  m*[n/m]≈n n m {m≉0} = begin
    (m * (n / m) {m≉0}) ≈⟨ sym (+-identityʳ (m * (n / m) {m≉0})) ⟩
    ((m * (n / m) {m≉0}) + 0#) ≈⟨ sym (division n m) ⟩
    n ∎

  [n/m]*m≈n : ∀ n m {m≉0 : m ≉ 0#} → ((n / m) {m≉0} * m) ≈ n
  [n/m]*m≈n n m {m≉0} = begin
    ((n / m) * m) ≈⟨ *-comm (n / m) m ⟩
    (m * (n / m)) ≈⟨ m*[n/m]≈n n m ⟩
    n ∎

  /≉0 : ∀ {c₁ c₂} → c₁ ≉ 0# → (c₂≉0 : c₂ ≉ 0#) → (c₁ / c₂) {c₂≉0} ≉ 0#
  /≉0 {c₁} {c₂} c₁≉0 c₂≉0 c₁/c₂≈0 = 0#≉1# $ *-cancelˡ c₂ c₂≉0 $ begin
    c₂ * 0#                      ≈⟨ *-congˡ (sym (zeroˡ ((c₂ / c₁) {c₁≉0}))) ⟩
    c₂ * (0# * (c₂ / c₁))        ≈⟨ *-congˡ (*-congʳ (sym (c₁/c₂≈0))) ⟩
    c₂ * ((c₁ / c₂) * (c₂ / c₁)) ≈⟨ sym (*-assoc c₂  (c₁ / c₂) (c₂ / c₁)) ⟩
    (c₂ * (c₁ / c₂)) * (c₂ / c₁) ≈⟨ *-congʳ (m*[n/m]≈n c₁ c₂) ⟩
    c₁ * (c₂ / c₁)               ≈⟨ m*[n/m]≈n c₂ c₁ ⟩
    c₂                           ≈⟨ sym (*-identityʳ c₂) ⟩
    c₂ * 1#                      ∎

  infixl 7 _/-nonzero_
  _/-nonzero_ : C/0 → C/0 → C/0
  (c₁ , c₁≉0) /-nonzero (c₂ , c₂≉0) = (c₁ / c₂) {c₂≉0} , /≉0 c₁≉0 c₂≉0

  infix 8 _⁻¹
  _⁻¹ : ∀ x {x≉0 : x ≉ 0#} → C
  _⁻¹ x {x≉0} = (1# / x) {x≉0}

  ⁻¹-inverseʳ : ∀ x {x≉0 : x ≉ 0#} → (x * (x ⁻¹) {x≉0}) ≈ 1#
  ⁻¹-inverseʳ = m*[n/m]≈n 1#

  ⁻¹-inverseˡ : ∀ x {x≉0 : x ≉ 0#} → ((x ⁻¹) {x≉0} * x) ≈ 1#
  ⁻¹-inverseˡ = [n/m]*m≈n 1#

  x⁻¹≉0 : ∀ x {x≉0 : x ≉ 0#} → (x ⁻¹) {x≉0} ≉ 0#
  x⁻¹≉0 x {x≉0} = /≉0 1#≉0# x≉0
  -- 0#≉1# $ begin
  --   0# ≈⟨ sym (zeroʳ x) ⟩
  --   x * 0# ≈⟨ *-congˡ (sym x⁻¹≈0) ⟩
  --   x * (x ⁻¹) {x≉0} ≈⟨ ⁻¹-inverseʳ x ⟩
  --   1# ∎

  ⁻¹-cong : ∀ {x y} {x≉0 : x ≉ 0#} {y≉0 : y ≉ 0#} → x ≈ y → (x ⁻¹) {x≉0} ≈ (y ⁻¹) {y≉0}
  ⁻¹-cong {x} {y} {x≉0} {y≉0} x≈y = *-cancelˡ x x≉0 $ begin
    (x * (x ⁻¹)) ≈⟨ ⁻¹-inverseʳ x ⟩
    1#           ≈⟨ sym (⁻¹-inverseʳ y {y≉0}) ⟩
    (y * (y ⁻¹)) ≈⟨ *-congʳ (sym x≈y) ⟩
    (x * (y ⁻¹)) ∎

record IsDecField
  (_≈?_ : Decidable _≈_) (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C)
  (_/_  : ∀ (n m : C) {m≉0 : m ≉ 0#} → C) (gcd : Op₂ C) : Set (c ⊔ ℓ) where
  field
    isField : IsField _+_ _*_ -_ 0# 1# _/_ gcd

  open IsField isField public

  isDecEquivalence : IsDecEquivalence _≈_
  isDecEquivalence = record
    { isEquivalence = isEquivalence
    ; _≟_ = _≈?_
    }

record IsFiniteField
  (_≈?_ : Decidable _≈_) (_+_ _*_ : Op₂ C) (-_ : Op₁ C) (0# 1# : C)
  (_/_  : ∀ (n m : C) {m≉0 : m ≉ 0#} → C) (gcd : Op₂ C)
  (cardinality : ℕ) : Set (suc c ⊔ ℓ) where
  field
    isDecField : IsDecField _≈?_ _+_ _*_ -_ 0# 1# _/_ gcd
    C↦Fin[cardinality] : C ⤖ Fin cardinality

  open IsDecField isDecField public

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Eq (A : Set) : Set₁ where
  field
    _≈_ : A → A → Set

open Eq {{...}} public

record Setoid : Set₁ where
  field
    ∣_∣    : Set
    {{eq}} : Eq ∣_∣

open Setoid public

-- instance
--   EqNat : Eq Nat
--   _≈_ {{EqNat}} = _≡_

NatSetoid : Setoid
∣ NatSetoid ∣ = Nat
-- Should give: No instance of type Eq Nat


text:
open import Data.Bool

module GUIgeneric.GUIExample   where

open import GUIgeneric.Prelude renaming (inj₁ to secondBtn; inj₂ to firstBtn; WxColor to Color) hiding (addButton; _>>_)

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib renaming (addButton to addButton')

open import Data.Product

addButton : String → Frame → Frame
addButton str fr = addButton' str fr optimized

addTxtBox : String → Frame → Frame
addTxtBox str fr = addTxtBox' str fr optimized

oneBtnGUI : Frame
oneBtnGUI = addButton "OK" create-frame

twoBtnGUI : Frame
twoBtnGUI = addButton "Cancel" oneBtnGUI

-- Attributes
--
Cols = ℕ
Margin  = ℕ
HSpace  = ℕ
VSpace  = ℕ

oneColumnLayout : Cols × Margin × HSpace × VSpace
oneColumnLayout = (1 , 10 , 2 , 2)

black : Color
black = rgb 0 0 0

propOneBtn : properties oneBtnGUI
propOneBtn = black , oneColumnLayout

propTwoBtn : properties twoBtnGUI
propTwoBtn = black , black , oneColumnLayout

putStr' : {A : Set} → String → (f : IO GuiLev1Interface ∞ A) →
           IO GuiLev1Interface ∞ A
putStr' s f = do (putStrLn s) (λ _ → f)

syntax putStr' s f = putStrLn s >> f

keepGUI : {j : Size} → HandlerObject j twoBtnGUI →
            IO GuiLev1Interface ∞
      (Σ-syntax (returnType twoBtnGUI)
       (λ r →
          IOObjectˢ GuiLev1Interface handlerInterface j
          (nextStateFrame twoBtnGUI r)))
keepGUI = λ obj → return (noChange , obj)

changeGUI : ∀ {j} (g : CompEls frame) {g'} (prop : properties g) obj →
              IO GuiLev1Interface ∞ (Σ (returnType g') (\r -> IOObjectˢ GuiLev1Interface handlerInterface j (nextStateFrame g' r)))
changeGUI = λ g prop obj →  return (changedGUI g prop , obj)

mutual
 objTwoBtnGUI' : ∀ i → HandlerObject i twoBtnGUI
 objTwoBtnGUI' i .method {j} (secondBtn bt) =
   putStrLn "Cancel Fired! NO GUI Change." >>
   keepGUI (objTwoBtnGUI' j)

 objTwoBtnGUI' i .method {j} (firstBtn bt) =
   putStrLn "OK Fired! Redefining GUI." >>
   changeGUI oneBtnGUI propOneBtn (objOneBtnGUI' j)

 objOneBtnGUI' : ∀ i → HandlerObject i oneBtnGUI
 objOneBtnGUI' i .method {j} bt =
    putStrLn "OK Fired! Redefining GUI." >>
    changeGUI twoBtnGUI propTwoBtn (objTwoBtnGUI' j)

 obj2Btn : ∀ {i} → HandlerObject i twoBtnGUI
 obj2Btn .method (firstBtn bt) =
   putStrLn "OK fired! Redefining GUI." >>
   changeGUI oneBtnGUI propOneBtn obj1Btn
 obj2Btn .method (secondBtn bt) =
   putStrLn "Cancel fired! No GUI change." >>
   keepGUI obj2Btn

 obj1Btn : ∀ {i} → HandlerObject i oneBtnGUI
 obj1Btn .method bt =
    putStrLn "OK fired! Redefining GUI." >>
    changeGUI twoBtnGUI propTwoBtn obj2Btn

main : NativeIO Unit
main = compileProgram  twoBtnGUI propTwoBtn
                       (obj2Btn {∞})

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
-- {-# OPTIONS -v tc.conv.level:60 #-}
-- {-# OPTIONS -v tc.conv:30 #-}

{- Agda development version: Wed Oct 30 16:30:06 GMT 2013

   The last line of code triggers the following error,
   but replacing '_' with 'a' typechecks just fine.

   Bug.agda:32,8-11
   tt != a of type ⊤
   when checking that the expression s _ has type P tt → P a

   Changing 'Set (q a)' to 'Set' in line 26 suppresses the error.
-}

-- Andreas, 2013-10-31  Fixed by retrying sort comparison after
-- successful type comparison (which might have solve the missing level metas).

module Issue930 where

open import Common.Level

data ⊤ : Set where
  tt : ⊤

postulate
  q : ⊤ → Level
  P : (a : ⊤) → Set (q a)
  s : (a : ⊤) → P tt → P a
  a : ⊤
  g : (P tt → P a) → ⊤

v : ⊤
v = g (s _)

{-
coerce term      v  = s ?1
       from type t1 = P tt → P ?1
       to type   t2 = P tt → P a
equalSort
  Set (q tt ⊔ q ?1) == Set (q a ⊔ q tt)
compareAtom q tt == q a : Level
compareTerm tt == a : ⊤
sort comparison failed  -- THIS ERROR IS CAUGHT, BUT RETHROWN AT THE END
compareTerm P tt → P ?1 =< P tt → P a : Set (q tt ⊔ q ?1)
compare function types
  t1 = P tt → P ?1
  t2 = P tt → P a
equalSort
  Set (q ?1) == Set (q a)
compareTerm ?1 == a : ⊤
attempting shortcut ?1 := a
solving _13 := a

-}


text:
module x01-842Naturals where

-- This is a comment.

{-
  This is a multi-line comment
-}

-- Definition of datatype representing natural numbers. ♭

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- A couple of definitions using this datatype.

one : ℕ
one = suc zero

two : ℕ
two = suc (suc zero)

-- I could have also said two = suc one.

-- PLFA exercise: write out seven.

-- Pragma to use decimal notation as shorthand.

{-# BUILTIN NATURAL ℕ #-}

-- Some useful imports from the standard library:

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

-- Addition on naturals.

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc {!m + n!}

-- Agda normalization; proof of equality.

_ : 2 + 3 ≡ 5
_ = refl

-- Equational reasoning.

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- many steps condensed
    5
  ∎

-- PLFA shows longhand and shorthand are interchangeable.

-- PLFA exercise: write out the reduction for 3+4 equationally.

-- Multiplication.

_*_ : ℕ → ℕ → ℕ
m * n = {!!}

_ =
  begin
    2 * 3
  ≡⟨⟩    -- many steps condensed
    6
  ∎

-- PLFA exercise: write out 3*4.

-- 842 exercise: Exponentiation (1 point)
-- Define exponentiation (m raised to the power n).

_^_ : ℕ → ℕ → ℕ
m ^ n = {!!}

-- One test for exponentiation (you should write others).

_ : 2 ^ 3 ≡ 8
_ = refl

-- Monus (subtraction for naturals, bottoms out at zero).

_∸_ : ℕ → ℕ → ℕ
m ∸ n = {!!}

_ =
  begin
     3 ∸ 2
  ≡⟨⟩ -- many steps condensed
     1
  ∎

_ =
  begin
     2 ∸ 3
  ≡⟨⟩ -- many steps condensed
     0
  ∎

-- PLFA exercise: write out 5 ∸ 3 and 3 ∸ 5.

infixl 6  _+_  _∸_
infixl 7  _*_

-- These pragmas will register our operations, if we want,
-- so that they work with decimal notation.

-- {-# BUILTIN NATPLUS _+_ #-}
-- {-# BUILTIN NATTIMES _*_ #-}
-- {-# BUILTIN NATMINUS _∸_ #-}

-- Binary representation.
-- Modified from PLFA exercise (thanks to David Darais).

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

-- Our representation of zero is different from PLFA.
-- We use the empty sequence of bits (more consistent).

bin-zero : Bin-ℕ
bin-zero = bits

bin-one : Bin-ℕ
bin-one = bits x1     -- 1 in binary

bin-two : Bin-ℕ
bin-two = bits x1 x0  -- 10 in binary

-- 842 exercise: Increment (1 point)
-- Define increment (add one).

inc : Bin-ℕ → Bin-ℕ
inc m = {!!}

-- An example/test of increment (you should create others).

_ : inc (bits x1 x0 x1 x1) ≡ bits x1 x1 x0 x0
_ = refl

-- 842 exercise: To/From (2 points)
-- Define 'tob' and 'fromb' operations
-- to convert between unary (ℕ) and binary (Bin-ℕ) notation.
-- Hint: avoid addition and multiplication,
-- and instead use the provided dbl (double) function.
-- This will make later proofs easier.
-- I've put 'b' on the end of the operations to
-- avoid a name clash in a later file.
-- It also makes the direction clear when using them.

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc m) = suc (suc (dbl m))

tob : ℕ → Bin-ℕ
tob m = {!!}

fromb : Bin-ℕ → ℕ
fromb n = {!!}

-- A couple of examples/tests (you should create others).

_ : tob 6 ≡ bits x1 x1 x0
_ = refl

_ : fromb (bits x1 x1 x0) ≡ 6
_ = refl

-- 842 exercise: BinAdd (2 points)
-- Write the addition function for binary notation.
-- Do NOT use 'to' and 'from'. Work with Bin-ℕ as if ℕ did not exist.
-- Hint: use recursion on both m and n.

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
m bin-+ n = {!!}

-- Tests can use to/from, or write out binary constants as below.
-- Again: write more tests!

_ : (bits x1 x0) bin-+ (bits x1 x1) ≡ (bits x1 x0 x1)
_ = refl

-- That's it for now, but we will return to binary notation later.

-- Many definitions from above are also in the standard library.

-- open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_; _∸_)

-- Unicode used in this chapter:

{-
    ℕ  U+2115  DOUBLE-STRUCK CAPITAL N (\bN)
    →  U+2192  RIGHTWARDS ARROW (\to, \r, \->)
    ∸  U+2238  DOT MINUS (\.-)
    ≡  U+2261  IDENTICAL TO (\==)
    ⟨  U+27E8  MATHEMATICAL LEFT ANGLE BRACKET (\<)
    ⟩  U+27E9  MATHEMATICAL RIGHT ANGLE BRACKET (\>)
    ∎  U+220E  END OF PROOF (\qed)
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
-- Andreas, 2018-05-28, issue #3095, fail on attempt to make hidden parent variable visible

data Nat : Set where
  suc : {n : Nat} → Nat

data IsSuc : Nat → Set where
  isSuc : ∀{n} → IsSuc (suc {n})

test : ∀{m} → IsSuc m → Set
test p = aux p
  where
  aux : ∀{n} → IsSuc n → Set
  aux isSuc = {!.m!}  -- Split on .m here

-- Context:
-- p  : IsSuc .m
-- .m : Nat
-- .n : Nat

-- Expected error:
-- Cannot split on module parameter .m
-- when checking that the expression ? has type Set

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Categories.Minus2-Category.Properties where

-- All -2-Categories are equivalent to One

open import Level
open import Data.Product using (Σ; _,_; proj₁; proj₂)
open import Data.Unit using (⊤; tt)

open import Categories.Minus2-Category
open import Categories.Category
import Categories.Morphism as M
open import Categories.Category.Monoidal
open import Categories.Category.Instance.One
open import Categories.Category.Equivalence hiding (refl)
open import Categories.NaturalTransformation using (ntHelper)

private
  variable
    o ℓ e : Level

shrink-them-all : (X : -2-Category {o} {ℓ} {e}) → StrongEquivalence (-2-Category.cat X) (One {o} {ℓ} {e})
shrink-them-all X = record
  { F = record
    { F₀ = λ _ → lift tt
    ; F₁ = λ _ → lift tt
    }
  ; G = record
    { F₀ = λ _ → proj₁ Obj-Contr
    ; F₁ = λ _ → M._≅_.from (proj₂ Obj-Contr (proj₁ Obj-Contr))
    ; identity = Hom-Conn
    ; homomorphism = Hom-Conn
    ; F-resp-≈ = λ _ → Hom-Conn
    }
  ; weak-inverse = record
    { F∘G≈id = _
    ; G∘F≈id = record
      { F⇒G = ntHelper (record
        { η = λ y → M._≅_.from (proj₂ Obj-Contr y)
        ; commute = λ _ → Hom-Conn
        })
      ; F⇐G = ntHelper (record
        { η = λ y → M._≅_.to (proj₂ Obj-Contr y)
        ; commute = λ _ → Hom-Conn
        })
      ; iso = λ Z → record
        { isoˡ = M._≅_.isoˡ (proj₂ Obj-Contr Z)
        ; isoʳ = M._≅_.isoʳ (proj₂ Obj-Contr Z)
        }
      }
    }
  }
  where
    open -2-Category X
    open Category cat

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 gc where

open import lib

-- we will model addresses in memory as just natural numbers
Address : Set
Address = ℕ

-- a value of type (Bounded n) is an address a together with a proof that a is less than n
Bounded : Address → Set
Bounded n = Σ Address (λ a → a < n ≡ tt)

-- a (Cell a) models an addressable cell of memory
data Cell(bound : Address) : Set where
  Scalar : ℕ → Cell bound -- this represents a cell with no outgoing pointers, just a natural number value
  Pointers : ∀ (p1 p2 : Bounded bound) → Cell bound -- this cell has exactly two outgoing pointers

{- a (well-formed) memory is a vector of m cells, where all pointers in those cells are bounded by n.
   This is just a way of expressing that the memory does not have any pointers heading off to some
   illegal locations (outside the allocated memory). -}
Memory : Address → Set
Memory m = 𝕍 (Cell m) m

-- return a list of natural numbers from n-1 down to 0. [5 points]
nats : ∀(n : ℕ) → 𝕍 ℕ n
nats zero = []
nats (suc n) = n :: (nats n)

-- when the definition of nats is correct, the highlighting will disappear from refl below:
test-nats : nats 3 ≡ 2 :: 1 :: 0 :: []
test-nats = refl

{- (outgoingPointers m mem b) returns the list of outgoing pointers at the location
   given by b in the Memory m.  This is either empty (for Scalar) or a list of length
   two (for Pointers).

   Hint: there is already a function in vector.agda in the IAL that can find the Cell
   for you from mem and b.

   [10 points] -}
outgoingPointers : ∀ (m : Address) → Memory m → Bounded m → 𝕃 (Bounded m)
outgoingPointers n mem (j , k) with (nth𝕍 j k mem)
... | Scalar c = []
... | Pointers x y = x :: y :: []

{- (doMark u unmarked m b) is supposed to return (just v) if the address
   given by b is a member of unmarked, and v is the result of removing that
   address from unmarked.  If the address given by b is not in unmarked,
   then return none. This function simulates marking a cell by removing
   it (if it is there) from the vector of unmarked cells.  Because the
   length of the vector decreases, we can recurse in markh on the result
   if we need to.

   [17 points]
-}
doMark : ∀(u : ℕ)(unmarked : 𝕍 Address (suc u)) → (m : Address) → Bounded m → maybe (𝕍 Address u)
doMark u ( x :: unmarked ) m ( a , b ) with ( a =ℕ x )
... | tt = just unmarked
doMark 0 ( x :: [] ) m ( a , b ) | ff = nothing
doMark ( suc u ) ( x :: x1 :: unmarked ) m ( a , b ) | ff with ( doMark u ( x1 :: unmarked ) m ( a , b ) )
... | nothing = nothing
... | just unmarked1 = just ( x :: unmarked1 )

{- given a list of unmarked addresses and a Memory m, and a worklist of addresses,  return the
   list of all unmarked addresses that are not reachable in the memory from an address in the
   worklist.  So this is basically implementing mark and sweep gc, where addresses are considered
   marked if they do not appear in unmarked, and you use outgoingPointers to update the worklist
   when it is time to recurse.

   [18 points]
-}
markh : ∀(u : ℕ)(unmarked : 𝕍 Address u) → (m : Address) → Memory m → (worklist : 𝕃 (Bounded m)) → 𝕃 Address
markh u [] m x worklist = []
markh u unmarked m x [] = 𝕍-to-𝕃 unmarked
markh ( suc u ) unmarked m x ( x1 :: worklist ) with ( doMark u unmarked m x1 )
... | nothing = markh ( suc u ) unmarked m x worklist
... | just something = markh u something m x ( worklist ++ ( outgoingPointers m x x1 ) )

{- the final mark-and-sweep function, which just takes in a memory and list of roots, and
   returns the addresses not reachable in that memory from one of the roots. -}
mark : ∀(m : Address) → Memory m → (roots : 𝕃 (Bounded m)) → 𝕃 Address
mark m memory roots = markh m (nats m) m memory roots

----------------------------------------------------------------------
-- a test case:

test-memory : Memory 3
test-memory = Pointers (0 , refl) (2 , refl) :: Pointers (0 , refl) (2 , refl) :: Pointers (0 , refl) (0 , refl) :: []

test-roots : 𝕃 (Bounded 3)
test-roots = [ (0 , refl) ]

-- the addresses not reachable from address 0 by following pointers in test-memory
test-garbage : 𝕃 Address
test-garbage = mark 3 test-memory test-roots

-- if the implementation above is correct, highlighting on refl below will disappear
test-check : test-garbage ≡ 1 :: []
test-check = refl


text:
{-

In this file we apply the cubical machinery to Martin Hötzel-Escardó's
structure identity principle:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.SIP where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv')
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties renaming (cong≃ to _⋆_)
open import Cubical.Foundations.HAEquiv
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

open import Cubical.Foundations.Structure public

private
  variable
    ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level
    S : Type ℓ₁ → Type ℓ₂

  -- For technical reasons we reprove ua-pathToEquiv using the
  -- particular proof constructed by iso→HAEquiv. The reason is that we
  -- want to later be able to extract
  --
  --   eq : ua-au (ua e) ≡ cong ua (au-ua e)
  --
  uaHAEquiv : (A B : Type ℓ₁) → HAEquiv (A ≃ B) (A ≡ B)
  uaHAEquiv A B = iso→HAEquiv (iso ua pathToEquiv ua-pathToEquiv' pathToEquiv-ua)

  open isHAEquiv

  -- We now extract the particular proof constructed from iso→HAEquiv
  -- for reasons explained above.
  ua-pathToEquiv : {A B : Type ℓ₁} (e : A ≡ B) → ua (pathToEquiv e) ≡ e
  ua-pathToEquiv e = uaHAEquiv _ _ .snd .ret e

-- Note that for any equivalence (f , e) : X ≃ Y the type  ι (X , s) (Y , t) (f , e) need not to be
-- a proposition. Indeed this type should correspond to the ways s and t can be identified
-- as S-structures. This we call a standard notion of structure or SNS.
-- We will use a different definition, but the two definitions are interchangeable.
SNS-≡ : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
SNS-≡ {ℓ₁} S ι = ∀ {X : Type ℓ₁} (s t : S X) → ι (X , s) (X , t) (idEquiv X) ≃ (s ≡ t)

-- We introduce the notation for structure preserving equivalences a
-- bit differently, but this definition doesn't actually change from
-- Escardó's notes.
_≃[_]_ : (A : TypeWithStr ℓ₁ S) (ι : StrIso S ℓ₂) (B : TypeWithStr ℓ₁ S) → Type (ℓ-max ℓ₁ ℓ₂)
A ≃[ ι ] B = Σ[ e ∈ typ A ≃ typ B ] (ι A B e)

-- The following PathP version of SNS-≡ is a bit easier to work with
-- for the proof of the SIP
SNS-PathP : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
SNS-PathP {ℓ₁} S ι = {A B : TypeWithStr ℓ₁ S} (e : typ A ≃ typ B)
                  → ι A B e ≃ PathP (λ i → S (ua e i)) (str A) (str B)

-- A quick sanity-check that our definition is interchangeable with
-- Escardó's. The direction SNS-≡→SNS-PathP corresponds more or less
-- to a dependent EquivJ formulation of Escardó's homomorphism-lemma.
SNS-PathP→SNS-≡ : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) → SNS-PathP S ι → SNS-≡ S ι
SNS-PathP→SNS-≡ S ι θ {X = X} s t = ι (X , s) (X , t) (idEquiv X)           ≃⟨ θ (idEquiv X) ⟩
                                   PathP (λ i → S (ua (idEquiv X) i)) s t  ≃⟨ φ ⟩
                                   s ≡ t                                   ■
  where
   φ = transportEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = X} j i)) s t)

SNS-≡→SNS-PathP : (ι : StrIso S ℓ₃) → SNS-≡ S ι → SNS-PathP S ι
SNS-≡→SNS-PathP {S = S} ι θ {A = A} {B = B} e = EquivJ P C e (str A) (str B)
  where
   Y = typ B

   P : (X : Type _) → X ≃ Y → Type _
   P X e' = (s : S X) (t : S Y) → ι (X , s) (Y , t) e' ≃ PathP (λ i → S (ua e' i)) s t

   C : (s t : S Y) → ι (Y , s) (Y , t) (idEquiv Y) ≃ PathP (λ i → S (ua (idEquiv Y) i)) s t
   C s t = ι (Y , s) (Y , t) (idEquiv Y)           ≃⟨ θ s t ⟩
           s ≡ t                                   ≃⟨ ψ ⟩
           PathP (λ i → S (ua (idEquiv Y) i)) s t  ■
    where
     ψ = transportEquiv λ j → PathP (λ i → S (uaIdEquiv {A = Y} (~ j) i)) s t

-- We can now directly define an invertible function
--
--    sip : A ≃[ ι ] B → A ≡ B
--
sip : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) (θ : SNS-PathP S ι)
      (A B : TypeWithStr ℓ₁ S) → A ≃[ ι ] B → A ≡ B
sip S ι θ A B (e , p) i = ua e i , θ e .fst p i

-- The inverse to sip uses the following little lemma
private
  lem : (S : Type ℓ₁ → Type ℓ₂) (A B : TypeWithStr ℓ₁ S) (e : typ A ≡ typ B)
      → PathP (λ i → S (ua (pathToEquiv e) i)) (A .snd) (B .snd) ≡
        PathP (λ i → S (e i)) (A .snd) (B .snd)
  lem S A B e i = PathP (λ j → S (ua-pathToEquiv e i j)) (A .snd) (B .snd)

-- The inverse
sip⁻ : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) (θ : SNS-PathP S ι)
       (A B : TypeWithStr ℓ₁ S) → A ≡ B → A ≃[ ι ] B
sip⁻ S ι θ A B r = pathToEquiv p , invEq (θ (pathToEquiv p)) q
  where
  p : typ A ≡ typ B
  p = cong fst r
  q : PathP (λ i → S (ua (pathToEquiv p) i)) (A .snd) (B .snd)
  q = transport⁻ (lem S A B p) (cong snd r)

-- We can rather directly show that sip and sip⁻ are mutually inverse:
sip-sip⁻ : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) (θ : SNS-PathP S ι)
           (A B : TypeWithStr ℓ₁ S) (r : A ≡ B)
         → sip S ι θ A B (sip⁻ S ι θ A B r) ≡ r
sip-sip⁻ S ι θ A B r =
  let p : typ A ≡ typ B
      p = cong fst r
      q : PathP (λ i → S (p i)) (str A) (str B)
      q = cong snd r
  in sip S ι θ A B (sip⁻ S ι θ A B r)
   ≡⟨ refl ⟩
     (λ i → ( ua (pathToEquiv p) i)
            , θ (pathToEquiv p) .fst
                (invEq (θ (pathToEquiv p))
                       (transport⁻ (lem S A B p) q)) i)
   ≡⟨ (λ i j → ( ua (pathToEquiv p) j
               , retEq (θ (pathToEquiv p))
                       (transport⁻ (lem S A B p) q) i j)) ⟩
     (λ i → ( ua (pathToEquiv p) i
            , transport⁻ (lem S A B p) q i))
   ≡⟨ (λ i j → ( ua-pathToEquiv p i j
               , transp (λ k → PathP (λ j → S (ua-pathToEquiv p (i ∧ k) j)) (str A) (str B))
                        (~ i) (transport⁻ (lem S A B p) q) j)) ⟩
     (λ i → ( p i
            , transport (λ i → lem S A B p i) (transport⁻ (lem S A B p) q) i))
   ≡⟨ (λ i j → ( p j
               , transportTransport⁻ (lem S A B p) q i j)) ⟩
     r ∎

-- The trickier direction:
sip⁻-sip : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃) (θ : SNS-PathP S ι)
           (A B : TypeWithStr ℓ₁ S) (r : A ≃[ ι ] B)
         → sip⁻ S ι θ A B (sip S ι θ A B r) ≡ r
sip⁻-sip S ι θ A B (e , p) =
    sip⁻ S ι θ A B (sip S ι θ A B (e , p))
  ≡⟨ refl ⟩
    pathToEquiv (ua e) , invEq (θ (pathToEquiv (ua e))) (f⁺ p')
  ≡⟨ (λ i → pathToEquiv-ua e i , invEq (θ (pathToEquiv-ua e i)) (pth' i)) ⟩
    e , invEq (θ e) (f⁻ (f⁺ p'))
  ≡⟨ (λ i → e , invEq (θ e) (transportTransport⁻ (lem S A B (ua e)) p' i)) ⟩
    e , invEq (θ e) (θ e .fst p)
  ≡⟨ (λ i → e , (secEq (θ e) p i)) ⟩
    e , p ∎
  where
  p' : PathP (λ i → S (ua e i)) (str A) (str B)
  p' = θ e .fst p

  f⁺ : PathP (λ i → S (ua e i)) (str A) (str B)
     → PathP (λ i → S (ua (pathToEquiv (ua e)) i)) (str A) (str B)
  f⁺ = transport (λ i → PathP (λ j → S (ua-pathToEquiv (ua e) (~ i) j)) (str A) (str B))

  f⁻ : PathP (λ i → S (ua (pathToEquiv (ua e)) i)) (str A) (str B)
     → PathP (λ i → S (ua e i)) (str A) (str B)
  f⁻ = transport (λ i → PathP (λ j → S (ua-pathToEquiv (ua e) i j)) (str A) (str B))

  -- We can prove the following as in sip∘pis-id, but the type is not
  -- what we want as it should be "cong ua (pathToEquiv-ua e)"
  pth : PathP (λ j → PathP (λ k → S (ua-pathToEquiv (ua e) j k)) (str A) (str B))
              (f⁺ p') (f⁻ (f⁺ p'))
  pth i = transp (λ k → PathP (λ j → S (ua-pathToEquiv (ua e) (i ∧ k) j)) (str A) (str B))
                 (~ i) (f⁺ p')

  -- So we build an equality that we want to cast the types with
  casteq : PathP (λ j → PathP (λ k → S (ua-pathToEquiv (ua e) j k)) (str A) (str B))
                 (f⁺ p') (f⁻ (f⁺ p'))
         ≡ PathP (λ j → PathP (λ k → S (cong ua (pathToEquiv-ua e) j k)) (str A) (str B))
                 (f⁺ p') (f⁻ (f⁺ p'))
  casteq i = PathP (λ j → PathP (λ k → S (eq i j k)) (str A) (str B)) (f⁺ p') (f⁻ (f⁺ p'))
    where
    -- This is where we need the half-adjoint equivalence property
    eq : ua-pathToEquiv (ua e) ≡ cong ua (pathToEquiv-ua e)
    eq = sym (uaHAEquiv (typ A) (typ B) .snd .com e)

  -- We then get a term of the type we need
  pth' : PathP (λ j → PathP (λ k → S (cong ua (pathToEquiv-ua e) j k)) (str A) (str B))
               (f⁺ p') (f⁻ (f⁺ p'))
  pth' = transport (λ i → casteq i) pth

-- Finally package everything up to get the cubical SIP
SIP : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃)
      (θ : SNS-PathP S ι) (A B : TypeWithStr ℓ₁ S)
    → A ≃[ ι ] B ≃ (A ≡ B)
SIP S ι θ A B = isoToEquiv (iso (sip S ι θ A B) (sip⁻ S ι θ A B)
                               (sip-sip⁻ S ι θ A B) (sip⁻-sip S ι θ A B))

-- Now, we want to add axioms (i.e. propositions) to our Structure S that don't affect the ι.
-- We use a lemma due to Zesen Qian, which can now be found in Foundations.Prelude:
-- https://github.com/riaqn/cubical/blob/hgroup/Cubical/Data/Group/Properties.agda#L83

add-to-structure : (S : Type ℓ₁ → Type ℓ₂)
                   (axioms : (X : Type ℓ₁) → S X → Type ℓ₄)
                 → Type ℓ₁ → Type (ℓ-max ℓ₂ ℓ₄)
add-to-structure S axioms X = Σ[ s ∈ S X ] (axioms X s)

add-to-iso : (S : Type ℓ₁ → Type ℓ₂) (ι : StrIso S ℓ₃)
             (axioms : (X : Type ℓ₁) → S X → Type ℓ₄)
           → StrIso (add-to-structure S axioms) ℓ₃
add-to-iso S ι axioms (X , (s , a)) (Y , (t , b)) f = ι (X , s) (Y , t) f

add-ax-lemma : (S : Type ℓ₁ → Type ℓ₂)
               (axioms : (X : Type ℓ₁) → S X → Type ℓ₄)
               (axioms-are-Props : (X : Type ℓ₁) (s : S X) → isProp (axioms X s))
               {X Y : Type ℓ₁} {s : S X} {t : S Y} {a : axioms X s} {b : axioms Y t}
               (f : X ≃ Y)
             → PathP (λ i → S (ua f i)) s t ≃
               PathP (λ i → add-to-structure S axioms (ua f i)) (s , a) (t , b)
add-ax-lemma S axioms axioms-are-Props {s = s} {t = t} {a = a} {b = b} f = isoToEquiv (iso φ ψ η ε)
      where
       φ : PathP (λ i → S (ua f i)) s t → PathP (λ i → add-to-structure S axioms (ua f i)) (s , a) (t , b)
       φ p i = p i , isProp→PathP (λ i → axioms-are-Props (ua f i) (p i)) a b i

       ψ : PathP (λ i → add-to-structure S axioms (ua f i)) (s , a) (t , b) → PathP (λ i → S (ua f i)) s t
       ψ r i = r i .fst

       η : section φ ψ
       η r i j =  r j .fst , isProp→isSet-PathP (λ k → axioms-are-Props (ua f k) (r k .fst)) _ _
                                                (isProp→PathP (λ k → axioms-are-Props (ua f k) (r k .fst)) a b)
                                                (λ k → r k .snd) i j

       ε : retract φ ψ
       ε p = refl

add-axioms-SNS : (S : Type ℓ₁ → Type ℓ₂)
                 (ι : (A B : Σ[ X ∈ (Type ℓ₁) ] (S X)) → A .fst ≃ B .fst → Type ℓ₃)
                 (axioms : (X : Type ℓ₁) → S X → Type ℓ₄)
                 (axioms-are-Props : (X : Type ℓ₁) (s : S X) → isProp (axioms X s))
                 (θ : SNS-PathP S ι)
               → SNS-PathP (add-to-structure S axioms) (add-to-iso S ι axioms)
add-axioms-SNS S ι axioms axioms-are-Props θ {X , s , a} {Y , t , b} f =
  add-to-iso S ι axioms (X , s , a) (Y , t , b) f                      ≃⟨ θ f ⟩
  PathP (λ i → S (ua f i)) s t                                        ≃⟨ add-ax-lemma S axioms axioms-are-Props f ⟩
  PathP (λ i → (add-to-structure S axioms) (ua f i)) (s , a) (t , b)  ■

-- Now, we want to join two structures. Together with the adding of
-- axioms this will allow us to prove that a lot of mathematical
-- structures are a standard notion of structure

join-structure : (S₁ : Type ℓ₁ → Type ℓ₂) (S₂ : Type ℓ₁ → Type ℓ₄)
               → Type ℓ₁ → Type (ℓ-max ℓ₂ ℓ₄)
join-structure S₁ S₂ X = S₁ X × S₂ X

join-iso : {S₁ : Type ℓ₁ → Type ℓ₂} (ι₁ : StrIso S₁ ℓ₃)
           {S₂ : Type ℓ₁ → Type ℓ₄} (ι₂ : StrIso S₂ ℓ₅)
         → StrIso (join-structure S₁ S₂) (ℓ-max ℓ₃ ℓ₅)
join-iso ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) f = (ι₁ (X , s₁) (Y , t₁) f) × (ι₂ (X , s₂) (Y , t₂) f)

join-SNS : (S₁ : Type ℓ₁ → Type ℓ₂) (ι₁ : StrIso S₁ ℓ₃) (θ₁ : SNS-PathP S₁ ι₁)
           (S₂ : Type ℓ₁ → Type ℓ₄) (ι₂ : StrIso S₂ ℓ₅) (θ₂ : SNS-PathP S₂ ι₂)
         → SNS-PathP (join-structure S₁ S₂) (join-iso ι₁ ι₂)
join-SNS S₁ ι₁ θ₁ S₂ ι₂ θ₂ {X , s₁ , s₂} {Y , t₁ , t₂} e = isoToEquiv (iso φ ψ η ε)
   where
    φ : join-iso ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) e
      → PathP (λ i → join-structure S₁ S₂ (ua e i)) (s₁ , s₂) (t₁ , t₂)
    φ (p , q) i = (θ₁ e .fst p i) , (θ₂ e .fst q i)

    ψ : PathP (λ i → join-structure S₁ S₂ (ua e i)) (s₁ , s₂) (t₁ , t₂)
      → join-iso ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) e
    ψ p = invEq (θ₁ e) (λ i → p i .fst) , invEq (θ₂ e) (λ i → p i .snd)

    η : section φ ψ
    η p i j = retEq (θ₁ e) (λ k → p k .fst) i j , retEq (θ₂ e) (λ k → p k .snd) i j

    ε : retract φ ψ
    ε (p , q) i = secEq (θ₁ e) p i , secEq (θ₂ e) q i

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- Validity of canonical kinding in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Kinding.Canonical.Validity where

open import Data.Product using (∃; _,_; _×_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality

open import FOmegaInt.Syntax
open import FOmegaInt.Syntax.HereditarySubstitution
open import FOmegaInt.Syntax.Normalization
open import FOmegaInt.Kinding.Canonical
open import FOmegaInt.Kinding.Canonical.HereditarySubstitution

open Syntax
open ElimCtx
open Substitution hiding (subst)
open Kinding
open WfCtxOps
open ContextNarrowing

private module TK = TrackSimpleKindsSubst

------------------------------------------------------------------------
-- Validity of canonical kinding, subkinding and subtyping.

-- Validity of spine kinding: the kind of an elimination is
-- well-formed, provided that the spine is well-kinded and the kind of
-- the head is well-formed.
Sp⇉-valid : ∀ {n} {Γ : Ctx n} {as j k} → Γ ⊢ j kd → Γ ⊢ j ⇉∙ as ⇉ k → Γ ⊢ k kd
Sp⇉-valid j-kd ⇉-[] = j-kd
Sp⇉-valid (kd-Π j-kd k-kd) (⇉-∷ a⇇j _ k[a]⇉as⇉l) =
  Sp⇉-valid (TK.kd-/⟨⟩ k-kd (⇇-hsub a⇇j j-kd (⌊⌋-⌊⌋≡ _))) k[a]⇉as⇉l

-- Validity of kinding for neutral types: the kinds of neutral types
-- are well-formed.
Ne∈-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Ne a ∈ k → Γ ⊢ k kd
Ne∈-valid (∈-∙ x∈j j⇉as⇉k) = Sp⇉-valid (Var∈-valid x∈j) j⇉as⇉k

-- Validity of spine equality.
Sp≃-valid : ∀ {n} {Γ : Ctx n} {as bs j₁ j₂ k₂} →
            Γ ⊢ j₁ <∷ j₂ → Γ ⊢ j₂ ⇉∙ as ≃ bs ⇉ k₂ →
            ∃ λ k₁ → Γ ⊢ j₂ ⇉∙ as ⇉ k₂ × Γ ⊢ j₁ ⇉∙ bs ⇉ k₁ × Γ ⊢ k₁ <∷ k₂
Sp≃-valid k₁<∷k₂ ≃-[] = _ , ⇉-[] , ⇉-[] , k₁<∷k₂
Sp≃-valid (<∷-Π j₂<∷j₁ k₁<∷k₂ (kd-Π j₁-kd k₁-kd))
          (≃-∷ a≃b⇇j₂ k₂[a]⇉as≃bs⇉l₂) =
  let j₂-kd        = ≃-valid-kd a≃b⇇j₂
      a⇇j₂ , b⇇j₂  = ≃-valid a≃b⇇j₂
      b⇇j₁         = Nf⇇-⇑ b⇇j₂ j₂<∷j₁
      k₁[b]<∷k₂[a] = TK.<∷-/⟨⟩≃ k₁<∷k₂ (≃-hsub (≃-sym a≃b⇇j₂) (⌊⌋-⌊⌋≡ _))
      l₁ , k₂[a]⇉as⇉l₂ , k₁[b]⇉bs⇉l₁ , l₁<∷l₂ = Sp≃-valid k₁[b]<∷k₂[a]
                                                          k₂[a]⇉as≃bs⇉l₂
  in l₁ ,
     ⇉-∷ a⇇j₂ j₂-kd k₂[a]⇉as⇉l₂ ,
     ⇉-∷ b⇇j₁ j₁-kd (subst (λ k → _ ⊢ _ Kind[ _ ∈ k ] ⇉∙ _ ⇉ l₁)
                           (<∷-⌊⌋ j₂<∷j₁) k₁[b]⇉bs⇉l₁) ,
     l₁<∷l₂

-- Validity of subkinding and subtyping: well-formed subkinds
-- resp. well-kinded subtypes are also well-formed resp. well-kinded.

mutual

  <∷-valid : ∀ {n} {Γ : Ctx n} {j k} →
             Γ ⊢ j <∷ k → Γ ⊢ j kd × Γ ⊢ k kd
  <∷-valid (<∷-⋯ a₂<:a₁ b₁<:b₂) =
    let a₂⇉a₂⋯a₂ , a₁⇉a₁⋯a₁ = <:-valid a₂<:a₁
        b₁⇉b₁⋯b₁ , b₂⇉b₂⋯b₂ = <:-valid b₁<:b₂
    in kd-⋯ a₁⇉a₁⋯a₁ b₁⇉b₁⋯b₁ , kd-⋯ a₂⇉a₂⋯a₂ b₂⇉b₂⋯b₂
  <∷-valid (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd) =
    let j₂-kd , j₁-kd = <∷-valid j₂<∷j₁
        k₁-kd , k₂-kd = <∷-valid k₁<∷k₂
    in Πj₁k₁-kd , kd-Π j₂-kd k₂-kd

  <:-valid : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a <: b →
             Γ ⊢Nf a ⇉ a ⋯ a × Γ ⊢Nf b ⇉ b ⋯ b
  <:-valid (<:-trans a<:b b<:c) =
    proj₁ (<:-valid a<:b) , proj₂ (<:-valid b<:c)
  <:-valid (<:-⊥ a⇉a⋯a) = ⇉-⊥-f (Nf⇉-ctx a⇉a⋯a) , a⇉a⋯a
  <:-valid (<:-⊤ a⇉a⋯a) = a⇉a⋯a , ⇉-⊤-f (Nf⇉-ctx a⇉a⋯a)
  <:-valid (<:-∀ k₂<∷k₁ a₁<:a₂ Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁) =
    let k₂-kd   , k₁-kd   = <∷-valid  k₂<∷k₁
        a₁⇉a₁⋯a₁ , a₂⇉a₂⋯a₂ = <:-valid a₁<:a₂
    in Πk₁a₁⇉Πk₁a₁⋯Πk₁a₁ , ⇉-∀-f k₂-kd a₂⇉a₂⋯a₂
  <:-valid (<:-→ a₂<:a₁ b₁<:b₂) =
    let a₂⇉a₂⋯a₂ , a₁⇉a₁⋯a₁ = <:-valid a₂<:a₁
        b₁⇉b₁⋯b₁ , b₂⇉b₂⋯b₂ = <:-valid b₁<:b₂
    in ⇉-→-f a₁⇉a₁⋯a₁ b₁⇉b₁⋯b₁ , ⇉-→-f a₂⇉a₂⋯a₂ b₂⇉b₂⋯b₂
  <:-valid (<:-∙ x∈j j⇉as≃bs⇉c⋯d)
    with Sp≃-valid (<∷-refl (Var∈-valid x∈j)) j⇉as≃bs⇉c⋯d
  <:-valid (<:-∙ x∈j j⇉as≃bs⇉c₂⋯d₂)
    | _ , j⇉as⇉c₂⋯d₂ , j⇉bs⇉c₁⋯d₁ , <∷-⋯ c₂<:c₁ d₁<:d₂ =
      ⇉-s-i (∈-∙ x∈j j⇉as⇉c₂⋯d₂) , ⇉-s-i (∈-∙ x∈j j⇉bs⇉c₁⋯d₁)
  <:-valid (<:-⟨| a∈b⋯c) with Ne∈-valid a∈b⋯c
  <:-valid (<:-⟨| a∈b⋯c) | kd-⋯ b⇉b⋯b _ = b⇉b⋯b , ⇉-s-i a∈b⋯c
  <:-valid (<:-|⟩ a∈b⋯c) with Ne∈-valid a∈b⋯c
  <:-valid (<:-|⟩ a∈b⋯c) | kd-⋯ _ c⇉c⋯c = ⇉-s-i a∈b⋯c , c⇉c⋯c

-- Validity of kind checking: if a normal type checks against a kind,
-- then that kind is well-formed.
Nf⇇-valid : ∀ {n} {Γ : Ctx n} {a k} → Γ ⊢Nf a ⇇ k → Γ ⊢ k kd
Nf⇇-valid (⇇-⇑ a⇉j j<∷k) = proj₂ (<∷-valid j<∷k)

-- Some corollaries.

-- The checked kinds of subtypes are well-formed.
<:⇇-valid-kd : ∀ {n} {Γ : Ctx n} {a b k} → Γ ⊢ a <: b ⇇ k → Γ ⊢ k kd
<:⇇-valid-kd a<:b⇇k = Nf⇇-valid (proj₁ (<:⇇-valid a<:b⇇k))

-- Canonical kinding of applications is admissible.
Nf⇇-Π-e : ∀ {n} {Γ : Ctx n} {a b j k} →
          Γ ⊢Nf a ⇇ Π j k → Γ ⊢Nf b ⇇ j →
          Γ ⊢Nf a ⌜·⌝⟨ ⌊ Π j k ⌋ ⟩ b ⇇ k Kind[ b ∈ ⌊ j ⌋ ]
Nf⇇-Π-e a⇇Πjk b⇇j = TK.Nf⇇-Π-e a⇇Πjk b⇇j (Nf⇇-valid b⇇j) (⌊⌋-⌊⌋≡ _)

-- Canonical subtyping of applications is admissible.
<:-⌜·⌝ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ j k} →
         Γ ⊢ a₁ <: a₂ ⇇ Π j k → Γ ⊢ b₁ ≃ b₂ ⇇ j →
         Γ ⊢ a₁ ⌜·⌝⟨ ⌊ Π j k ⌋ ⟩ b₁ <: a₂ ⌜·⌝⟨ ⌊ Π j k ⌋ ⟩ b₂ ⇇
           k Kind[ b₁ ∈ ⌊ j ⌋ ]
<:-⌜·⌝ a₁<:a₂⇇Πjk b₁≃b₂⇇j with <:⇇-valid-kd a₁<:a₂⇇Πjk
<:-⌜·⌝ (<:-λ a₁<:a₂⇇k Λj₁a₁⇇Πjk Λj₂a₂⇇Πjk) b₁≃b₂⇇j | (kd-Π _ k-kd) =
  TK.<:⇇-/⟨⟩≃ a₁<:a₂⇇k k-kd (≃-hsub b₁≃b₂⇇j (⌊⌋-⌊⌋≡ _))

-- Subtyping of proper types checks against the kind of proper types.
<:-⋯-* : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢ a <: b → Γ ⊢ a <: b ⇇ ⌜*⌝
<:-⋯-* a<:b with <:-valid a<:b
<:-⋯-* a<:b | a⇉a⋯a , b⇉b⋯b = <:-⇇ (Nf⇉-⋯-* a⇉a⋯a) (Nf⇉-⋯-* b⇉b⋯b) a<:b

-- Some commonly used (hereditary) substitution lemmas.

kd-[] : ∀ {n} {Γ : Ctx n} {a j k} →
        kd k ∷ Γ ⊢ j kd → Γ ⊢Nf a ⇇ k → Γ ⊢ j Kind[ a ∈ ⌊ k ⌋ ] kd
kd-[] j-kd a⇇k = TK.kd-/⟨⟩ j-kd (⇇-hsub a⇇k (Nf⇇-valid a⇇k) (⌊⌋-⌊⌋≡ _))

Nf⇇-[] : ∀ {n} {Γ : Ctx n} {a b j k} →
         kd j ∷ Γ ⊢Nf a ⇇ k → Γ ⊢Nf b ⇇ j →
         Γ ⊢Nf a [ b ∈ ⌊ j ⌋ ] ⇇ k Kind[ b ∈ ⌊ j ⌋ ]
Nf⇇-[] a⇇k b⇇j = TK.Nf⇇-/⟨⟩ a⇇k (⇇-hsub b⇇j (Nf⇇-valid b⇇j) (⌊⌋-⌊⌋≡ _))

<∷-[≃] : ∀ {n} {Γ : Ctx n} {j k₁ k₂ a₁ a₂} →
         kd j ∷ Γ ⊢ k₁ <∷ k₂ → Γ ⊢ a₁ ≃ a₂ ⇇ j →
         Γ ⊢ k₁ Kind[ a₁ ∈ ⌊ j ⌋ ] <∷ k₂ Kind[ a₂ ∈ ⌊ j ⌋ ]
<∷-[≃] k₁<∷k₂ a₁≃a₂⇇j =
  TK.<∷-/⟨⟩≃ k₁<∷k₂ (≃-hsub a₁≃a₂⇇j (⌊⌋-⌊⌋≡ _))

<:-[≃] : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ j k} →
         kd j ∷ Γ ⊢ a₁ <: a₂ ⇇ k → Γ ⊢ b₁ ≃ b₂ ⇇ j →
         Γ ⊢ a₁ [ b₁ ∈ ⌊ j ⌋ ] <: a₂ [ b₂ ∈ ⌊ j ⌋ ] ⇇ k Kind[ b₁ ∈ ⌊ j ⌋ ]
<:-[≃] a₁<:a₂⇇k b₁≃b₂⇇j =
  TK.<:⇇-/⟨⟩≃ a₁<:a₂⇇k (<:⇇-valid-kd a₁<:a₂⇇k) (≃-hsub b₁≃b₂⇇j (⌊⌋-⌊⌋≡ _))

-- Another admissible kinding rule for applications.
Nf⇇-Π-e′ : ∀ {n} {Γ : Ctx n} {a b j k} →
           Γ ⊢Nf a ⇇ Π j k → Γ ⊢Nf b ⇇ j →
           Γ ⊢Nf a ↓⌜·⌝ b ⇇ k Kind[ b ∈ ⌊ j ⌋ ]
Nf⇇-Π-e′ {b = b} (⇇-⇑ (⇉-Π-i {_} {a₁} j₁-kd a⇉k₁) (<∷-Π j₂<∷j₁ k₁<∷k₂ Πj₁k₁-kd))
         b⇇j₂ =
  subst (_ ⊢Nf_⇇ _) (cong (a₁ [ b ∈_]) (<∷-⌊⌋ j₂<∷j₁))
        (Nf⇇-[] (⇇-⇑ (⇓-Nf⇉ (Nf⇇-valid b⇇j₂) j₂<∷j₁ a⇉k₁) k₁<∷k₂) b⇇j₂)

-- Another admissible subtyping rule for applications.
<:-↓⌜·⌝ : ∀ {n} {Γ : Ctx n} {a₁ a₂ b₁ b₂ j k} →
         Γ ⊢ a₁ <: a₂ ⇇ Π j k → Γ ⊢ b₁ ≃ b₂ ⇇ j →
         Γ ⊢ a₁ ↓⌜·⌝ b₁ <: a₂ ↓⌜·⌝ b₂ ⇇ k Kind[ b₁ ∈ ⌊ j ⌋ ]
<:-↓⌜·⌝ {b₁ = b₁} {b₂}
        (<:-λ a₁<:a₂⇇k (⇇-⇑ (⇉-Π-i {_} {a₁} _ _) (<∷-Π j₁<∷j _ _))
                       (⇇-⇑ (⇉-Π-i {_} {a₂} _ _) (<∷-Π j₂<∷j _ _))) b₁≃b₂⇇j =
  subst₂ (_ ⊢_<:_⇇ _)
         (cong (a₁ [ b₁ ∈_]) (<∷-⌊⌋ j₁<∷j)) (cong (a₂ [ b₂ ∈_]) (<∷-⌊⌋ j₂<∷j))
         (<:-[≃] a₁<:a₂⇇k b₁≃b₂⇇j)

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the extensional sublist relation over setoid equality.
------------------------------------------------------------------------

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

open import Relation.Binary hiding (Decidable)

module Data.List.Relation.Binary.Subset.Setoid.Properties where

open import Data.Bool using (Bool; true; false)
open import Data.List
open import Data.List.Relation.Unary.Any using (here; there)
import Data.List.Membership.Setoid as Membership
open import Data.List.Membership.Setoid.Properties
import Data.List.Relation.Binary.Subset.Setoid as Sublist
import Data.List.Relation.Binary.Equality.Setoid as Equality
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Unary using (Pred; Decidable)
import Relation.Binary.Reasoning.Preorder as PreorderReasoning

open Setoid using (Carrier)

------------------------------------------------------------------------
-- Relational properties

module _ {a ℓ} (S : Setoid a ℓ) where

  open Equality S
  open Sublist S
  open Membership S

  ⊆-reflexive : _≋_ ⇒ _⊆_
  ⊆-reflexive xs≋ys = ∈-resp-≋ S xs≋ys

  ⊆-refl : Reflexive _⊆_
  ⊆-refl x∈xs = x∈xs

  ⊆-trans : Transitive _⊆_
  ⊆-trans xs⊆ys ys⊆zs x∈xs = ys⊆zs (xs⊆ys x∈xs)

  ⊆-isPreorder : IsPreorder _≋_ _⊆_
  ⊆-isPreorder = record
    { isEquivalence = ≋-isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder
    }

  -- Reasoning over subsets
  module ⊆-Reasoning where
    open PreorderReasoning ⊆-preorder public
      renaming
      ( _∼⟨_⟩_  to _⊆⟨_⟩_
      ; _≈⟨_⟩_  to _≋⟨_⟩_
      ; _≈˘⟨_⟩_ to _≋˘⟨_⟩_
      ; _≈⟨⟩_   to _≋⟨⟩_
      )

    infix 1 _∈⟨_⟩_
    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

------------------------------------------------------------------------
-- filter

module _ {a p ℓ} (S : Setoid a ℓ)
         {P : Pred (Carrier S) p} (P? : Decidable P) where

  open Setoid S renaming (Carrier to A)
  open Sublist S

  filter⁺ : ∀ xs → filter P? xs ⊆ xs
  filter⁺ []       ()
  filter⁺ (x ∷ xs) y∈f[x∷xs] with P? x
  ... | no  _ = there (filter⁺ xs y∈f[x∷xs])
  ... | yes _ with y∈f[x∷xs]
  ...   | here  y≈x     = here y≈x
  ...   | there y∈f[xs] = there (filter⁺ xs y∈f[xs])


text:
-- Andreas, 2013-10-26
-- What if user tried to eliminate function type by copattern?

{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v tc.lhs.split:30 #-}

module CopatternsSplitErrorWithUnboundDBIndex where

import Common.Level

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_

-- pair defined by copatterns
test : {A B : Set} → A → A → A × A
fst test a = a
snd test a = a

-- Bad error WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Rules/LHS.hs:250

-- Correct error:
-- Cannot eliminate type A → A → A × A with projection pattern fst
-- when checking that the clause fst test a = a has type
-- {A : Set} → {Set} → A → A → A × A
--

-- pair defined by copatterns
pair : {A B : Set} → A → B → A × B
fst pair a b = a
snd pair a b = b

-- Bad error WAS: Unbound index in error message:
--
-- Cannot eliminate type @3 × A with pattern b (did you supply too many arguments?)
-- when checking that the clause fst pair a b = a has type
-- {A B : Set} → A → B → A × B


text:
-- This file is imported by other tests, can't just remove (Andreas, 2015-07-15).

module Nat where

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


text:
module Function.Domains.Id where

import      Lvl
open import Functional using (_∘_)
open import Type
open import Type.Dependent

private variable ℓₒ₁ ℓₒ₂ ℓₑ₁ ℓₑ₂ : Lvl.Level

module _ {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} where
  data Image (f : X → Y) : Y → Type{ℓₒ₁ Lvl.⊔ ℓₒ₂} where
    intro : (x : X) → Image f (f(x))

  -- The image/range of a function.
  -- Represents the "set" of values of a function.
  -- Note: An element of Y and a proof that this element is the value of the function f is included so that (⊶ f) does not become injective when f is not.
  -- Note: A construction of this implies that X is non-empty.
  ⊶ : (X → Y) → Type{ℓₒ₁ Lvl.⊔ ℓₒ₂}
  ⊶ = Σ(Y) ∘ Image

  -- Represents the "set" of objects pointing to the value y of the function f.
  -- ∃(Fiber f(y)) is also called "the fiber of the element y under the map f".
  -- Fiber(f) is similar to the inverse image or the preimage of f when their argument is a singleton set.
  data Fiber (f : X → Y) : Y → X → Type{ℓₒ₁ Lvl.⊔ ℓₒ₂} where
    intro : (x : X) → Fiber f (f(x)) x

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{- Example by Andrew Pitts, 2016-05-23 -}

{-# OPTIONS --rewriting --cubical-compatible #-}

open import Agda.Builtin.Equality public

infix 6 I─_
postulate
  𝕀     : Set
  O     : 𝕀
  I     : 𝕀
  I─_   : 𝕀 → 𝕀

{-# BUILTIN REWRITE _≡_ #-}

postulate
  I─O≡I   :           I─ O     ≡ I

{-# REWRITE I─O≡I   #-}

data Pth (A : Set) : A → A → Set where
  path : (f : 𝕀 → A) → Pth A (f O) (f I)

infix 6 _at_
_at_ : {A : Set}{x y : A} → Pth A x y → 𝕀 → A
path f at i = f i

record Path (A : Set)(x y : A) : Set where
  field
    pth : Pth A x y
    feq : pth at O ≡ x
    seq : pth at I ≡ y

open Path public

{-# REWRITE feq #-}
{-# REWRITE seq #-}

infix 6 _′_
_′_ : {A : Set}{x y : A} → Path A x y → 𝕀 → A
p ′ i = pth p at i

fun2path : {A : Set}(f : 𝕀 → A) → Path A (f O) (f I)
pth (fun2path f) = path f
feq (fun2path f) = refl
seq (fun2path f) = refl

inv : {A : Set}{x y : A} → Path A x y → Path A y x
inv p = fun2path (λ i → p ′ (I─ i))