text:
--
-- Inspired by a blog post written by Arnaud Bailly
-- https://abailly.github.io/posts/dependently-typed-date.html
--

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

module Date where

open import Data.Nat using (ℕ; zero; suc; _≡ᵇ_; _<_; _≤_; z≤n; s≤s; _≤?_; _<?_)
open import Data.Nat.DivMod using (_%_)
open import Data.Bool using (Bool; true; false; _∧_; _∨_; not)
open import Data.Maybe using (Maybe; just; nothing)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)

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

module Day where
    data t : Set where
        Day : (n : ℕ) → {True (1 ≤? n)} → t   -- Capture a day which should not be zero

    make : (n : ℕ) → {True (1 ≤? n)} → t
    make = Day

    value : t → ℕ
    value (Day n) = n

module Year where
    t : Set
    t = ℕ

    isLeap : t → Bool
    isLeap y = (check4 ∧ not check100) ∨ check400
        where check4   = y % 4   ≡ᵇ 0
              check100 = y % 100 ≡ᵇ 0
              check400 = y % 400 ≡ᵇ 0

module Month where
    data t : Set where
        January    : t
        February   : t
        March      : t
        April      : t
        May        : t
        June       : t
        July       : t
        August     : t
        September  : t
        October    : t
        November   : t
        December   : t

    toNat : t → ℕ
    toNat January    = 1
    toNat February   = 2
    toNat March      = 3
    toNat April      = 4
    toNat May        = 5
    toNat June       = 6
    toNat July       = 7
    toNat August     = 8
    toNat September  = 9
    toNat October    = 10
    toNat November   = 11
    toNat December   = 12

    next : t → t
    next January   = February
    next February  = March
    next March     = April
    next April     = May
    next May       = June
    next June      = July
    next July      = August
    next August    = September
    next September = October
    next October   = November
    next November  = December
    next December  = January

    duration : t → Year.t → Day.t
    duration January _   = Day.make 31
    duration February year with Year.isLeap year
    ... | true           = Day.make 29
    ... | false          = Day.make 28
    duration March _     = Day.make 31
    duration April _     = Day.make 30
    duration May _       = Day.make 31
    duration June _      = Day.make 30
    duration July _      = Day.make 31
    duration August _    = Day.make 31
    duration September _ = Day.make 30
    duration October _   = Day.make 31
    duration November _  = Day.make 30
    duration December _  = Day.make 31

{-
module Date where
    data t : Set where
       Valid   : (year : Year.t) → (month : Month.t) → (day : ℕ)
               → {≤max : True (day ≤? Day.value (Month.duration month year))}
               → {min≤ : True (1 ≤? day)}
                --------------------------------------------------------------
               → t

    make = Valid

    changeMonth : (year : Year.t) → (month : Month.t) -> t
    changeMonth year Month.December = make (suc year) Month.January 1
    changeMonth year month          = make year (Month.next month) 1

    addOneDay : t → t
    addOneDay (Valid year month day) with (suc day) ≤? Day.value (Month.duration month year)
    ... | yes proof = Valid year month (suc day) {proof} {s≤s z≤n}
    ... | no  _     = changeMonth year month
    addOneDay d     = d
-}

module Date where
    data t : Set where
       Valid   : (year : Year.t) → (month : Month.t) → (day : ℕ)
               → {≤max : day ≤ Day.value (Month.duration month year)}
               → {min≤ : 1 ≤ day}
                --------------------------------------------------------------
               → t
       Invalid : t

    1≤month : ∀ {month year} -> 1 ≤ Day.value (Month.duration month year)
    1≤month {Month.January} {year} =
        begin
           1 ≤ Day.value (Month.duration month year)

{-
    make : (year : Year.t) → (month : Month.t) → (day : ℕ) → t
    make year month day with day ≤? Day.value (Month.duration month year) | 1 ≤? day
    ... | yes p1 | yes p2 = Valid year month day {p1} {p2}
    ... | _      | _      = Invalid

    changeMonth : (year : Year.t) → (month : Month.t) -> t
    changeMonth year Month.December = Valid (suc year) Month.January 1 {1≤month} {s≤s z≤n}
    changeMonth year month          = Valid year (Month.next month) 1 {1≤month} {s≤s z≤n}

    addOneDay : t → t
    addOneDay (Valid year month day) with (suc day) ≤? Day.value (Month.duration month year)
    ... | yes proof = Valid year month (suc day) {proof} {s≤s z≤n}
    ... | no  _     = changeMonth year month
    addOneDay d     = d

    -- addDays : t → ℕ → t
-}

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


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

module Cubical.Data.InfNat.Base where

open import Cubical.Data.Nat as ℕ using (ℕ)
open import Cubical.Core.Primitives

data ℕ+∞ : Type₀ where
  ∞ : ℕ+∞
  fin : ℕ → ℕ+∞

suc : ℕ+∞ → ℕ+∞
suc ∞ = ∞
suc (fin n) = fin (ℕ.suc n)

zero : ℕ+∞
zero = fin ℕ.zero

caseInfNat : ∀ {ℓ} → {A : Type ℓ} → (aF aI : A) → ℕ+∞ → A
caseInfNat aF aI (fin n) = aF
caseInfNat aF aI ∞       = aI

infixl 6 _+_
_+_ : ℕ+∞ → ℕ+∞ → ℕ+∞
∞     + m     = ∞
fin n + ∞     = ∞
fin n + fin m = fin (n ℕ.+ m)

infixl 7 _·_
_·_ : ℕ+∞ → ℕ+∞ → ℕ+∞
fin m         · fin n         = fin (m ℕ.· n)
∞             · fin ℕ.zero    = zero
fin ℕ.zero    · ∞             = zero
∞             · ∞             = ∞
∞             · fin (ℕ.suc _) = ∞
fin (ℕ.suc _) · ∞             = ∞

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module MissingTypeSignatureInMutual where

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

mutual
  pred zero    = zero
  pred (suc n) = n

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- "Basic" infinite grammars
------------------------------------------------------------------------

-- For a larger and possibly more convenient, but equivalent, grammar
-- interface, see Grammar.Infinite.

{-# OPTIONS --guardedness #-}

module Grammar.Infinite.Basic where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.Bool hiding (_≤_)
open import Data.Char hiding (_≤_)
open import Data.Empty
open import Data.List as List
import Data.List.Categorical
open import Data.List.Membership.Propositional
import Data.List.Membership.Propositional.Properties as ∈
open import Data.List.Properties
import Data.List.Relation.Unary.Any as Any
open import Data.List.Relation.Unary.Any.Properties
open import Data.Nat
open import Data.Nat.Properties as NatP
open import Data.Product as Prod
import Data.Product.Function.Dependent.Propositional as Σ
open import Data.Product.Function.NonDependent.Propositional
open import Data.Sum
open import Data.Unit using (tt)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
import Relation.Binary.PropositionalEquality.WithK as P
open import Relation.Nullary

private
  module LMi {A : Set} = Monoid (++-monoid A)
  module LMa = RawMonad (Data.List.Categorical.monad {ℓ = Level.zero})
open Any.Any

------------------------------------------------------------------------
-- Simple, potentially infinite grammars

-- These grammars are very general: they can represent every
-- recursively enumerable language (see Grammars.Infinite.expressive).
-- In practice one may want to restrict attention to languages that
-- can be parsed. I use general grammars to illustrate that this
-- approach to pretty-printing is not restricted to a small class of
-- languages.

infixl 15 _>>=_
infixl 10 _∣_

data Grammar : Set → Set₁ where

  -- The empty string.

  return : ∀ {A} → A → Grammar A

  -- A single, arbitrary token.

  token  : Grammar Char

  -- Monadic sequencing.

  _>>=_  : ∀ {A B} → ∞ (Grammar A) → (A → ∞ (Grammar B)) → Grammar B

  -- Symmetric choice.

  _∣_    : ∀ {A} → ∞ (Grammar A) → ∞ (Grammar A) → Grammar A

-- Semantics of grammars (parse trees). Here x ∈ g · s means that the
-- value x and string s are generated by the grammar g.

infix 4 _∈_·_

data _∈_·_ : ∀ {A} → A → Grammar A → List Char → Set₁ where
  return-sem : ∀ {A} {x : A} → x ∈ return x · []
  token-sem  : ∀ {t} → t ∈ token · [ t ]
  >>=-sem    : ∀ {A B x y s₁ s₂} {g₁ : ∞ (Grammar A)}
                 {g₂ : A → ∞ (Grammar B)} →
               x ∈ ♭ g₁ · s₁ → y ∈ ♭ (g₂ x) · s₂ →
               y ∈ g₁ >>= g₂ · s₁ ++ s₂
  left-sem   : ∀ {A} {g₁ g₂ : ∞ (Grammar A)} {x s} →
               x ∈ ♭ g₁ · s → x ∈ g₁ ∣ g₂ · s
  right-sem  : ∀ {A} {g₁ g₂ : ∞ (Grammar A)} {x s} →
               x ∈ ♭ g₂ · s → x ∈ g₁ ∣ g₂ · s

----------------------------------------------------------------------
-- Some grammar combinators

-- Failure.

fail : ∀ {A} → Grammar A
fail = ♯ fail ∣ ♯ fail

-- Map.

infixl 20 _<$>_ _<$_

_<$>_ : ∀ {A B} → (A → B) → Grammar A → Grammar B
f <$> g = ♯ g >>= λ x → ♯ return (f x)

_<$_ : ∀ {A B} → A → Grammar B → Grammar A
x <$ g = const x <$> g

-- The empty string if the argument is true, otherwise failure.

if-true : (b : Bool) → Grammar (T b)
if-true true  = return tt
if-true false = fail

-- A token satisfying a given predicate.

sat : (p : Char → Bool) → Grammar (∃ λ t → T (p t))
sat p = ♯ token >>= λ t → ♯ (_,_ t <$> if-true (p t))

-- A specific token.

tok : Char → Grammar Char
tok t = t <$ sat (λ t′ → t == t′)

------------------------------------------------------------------------
-- Some semantics combinators

-- Cast lemma.

cast : ∀ {A} {g : Grammar A} {x s₁ s₂} →
       s₁ ≡ s₂ → x ∈ g · s₁ → x ∈ g · s₂
cast refl = id

fail-sem⁻¹ : ∀ {A} {x : A} {s} → ¬ (x ∈ fail · s)
fail-sem⁻¹ (left-sem  ∈fail) = fail-sem⁻¹ ∈fail
fail-sem⁻¹ (right-sem ∈fail) = fail-sem⁻¹ ∈fail

<$>-sem : ∀ {A B} {f : A → B} {g : Grammar A} {y s} →
          y ∈ f <$> g · s ↔ ∃ λ x → x ∈ g · s × y ≡ f x
<$>-sem {A} {B} {f} {g} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }
  where
  lemma : ∀ s → s ++ [] ≡ s
  lemma s = proj₂ LMi.identity s

  to : ∀ {s g y} → y ∈ f <$> g · s → ∃ λ x → x ∈ g · s × y ≡ f x
  to (>>=-sem x∈ return-sem) =
    _ , cast (P.sym $ lemma _) x∈ , refl

  from : ∀ {s y g} → (∃ λ x → x ∈ g · s × y ≡ f x) → y ∈ f <$> g · s
  from (x , x∈ , refl) = cast (lemma _) (>>=-sem x∈ return-sem)

  >>=-cast : ∀ {x y s₁ s₂ s}
               {g₁ : ∞ (Grammar A)} {g₂ : A → ∞ (Grammar B)}
             (eq : s₁ ≡ s₂)
             (x∈ : x ∈ ♭ g₁ · s₁) (y∈ : y ∈ ♭ (g₂ x) · s) →
             >>=-sem {g₁ = g₁} {g₂ = g₂} (cast eq x∈) y∈ ≡
             cast (P.cong (λ s′ → s′ ++ s) eq) (>>=-sem x∈ y∈)
  >>=-cast refl _ _ = refl

  cast-cast : ∀ {A g s₁ s₂} {z : A} {z∈ : z ∈ g · s₂}
              (eq₁ : s₁ ≡ s₂) (eq₂ : s₂ ≡ s₁) →
              cast eq₁ (cast eq₂ z∈) ≡ z∈
  cast-cast refl refl = refl

  from∘to : ∀ {s g y} (y∈ : y ∈ f <$> g · s) → from (to y∈) ≡ y∈
  from∘to (>>=-sem {s₁ = s} x∈ return-sem) = begin
    cast (lemma (s ++ []))
         (>>=-sem (cast (P.sym $ lemma s) x∈) return-sem)  ≡⟨ P.cong (cast (lemma (s ++ []))) $
                                                                     >>=-cast (P.sym (lemma s)) x∈ return-sem ⟩
    cast (lemma (s ++ []))
         (cast (P.cong (λ s → s ++ []) (P.sym $ lemma s))
               (>>=-sem x∈ return-sem))                    ≡⟨ cast-cast (lemma (s ++ []))
                                                                        (P.cong (λ s → s ++ []) (P.sym $ lemma s)) ⟩
    >>=-sem x∈ return-sem                                  ∎
    where open P.≡-Reasoning

  to-cast : ∀ {s₁ s₂ y g} (eq : s₁ ≡ s₂) (y∈ : y ∈ f <$> g · s₁) →
            to (cast eq y∈) ≡
            P.subst (λ s → ∃ λ x → x ∈ g · s × y ≡ f x) eq (to y∈)
  to-cast refl y∈ = refl

  to∘from : ∀ {s y g}
            (x∈ : ∃ λ x → x ∈ g · s × y ≡ f x) → to (from x∈) ≡ x∈
  to∘from {s} (x , x∈ , refl)
    rewrite to-cast (lemma s) (>>=-sem x∈ return-sem)
          | lemma s
    = refl

if-true-sem : ∀ {b} x {s} → x ∈ if-true b · s ↔ s ≡ []
if-true-sem x = record
  { to         = P.→-to-⟶ (to _)
  ; from       = P.→-to-⟶ (from _ _)
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = to∘from _ x
    }
  }
  where
  to : ∀ b {x s} → x ∈ if-true b · s → s ≡ []
  to true  return-sem = refl
  to false ∈fail      = ⊥-elim $ fail-sem⁻¹ ∈fail

  from : ∀ b x {s} → s ≡ [] → x ∈ if-true b · s
  from true  _  refl = return-sem
  from false () refl

  from∘to : ∀ b {x s} (x∈ : x ∈ if-true b · s) → from b x (to b x∈) ≡ x∈
  from∘to true  return-sem = refl
  from∘to false ∈fail      = ⊥-elim $ fail-sem⁻¹ ∈fail

  to∘from : ∀ b x {s} (eq : s ≡ []) → to b (from b x eq) ≡ eq
  to∘from true  _  refl = refl
  to∘from false () refl

sat-sem : ∀ {p : Char → Bool} {t pt s} →
          (t , pt) ∈ sat p · s ↔ s ≡ [ t ]
sat-sem {p} {t} {pt} = record
  { to         = P.→-to-⟶ to
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }
  where
  to : ∀ {s} → (t , pt) ∈ sat p · s → s ≡ [ t ]
  to (>>=-sem token-sem (>>=-sem tt∈ return-sem)) =
    P.cong (λ s → t ∷ s ++ []) (Inverse.to (if-true-sem pt) ⟨$⟩ tt∈)

  from : ∀ {s} → s ≡ [ t ] → (t , pt) ∈ sat p · s
  from refl =
    >>=-sem token-sem
            (>>=-sem (Inverse.from (if-true-sem pt) ⟨$⟩ refl)
                     return-sem)

  from∘to : ∀ {s} (t∈ : (t , pt) ∈ sat p · s) → from (to t∈) ≡ t∈
  from∘to (>>=-sem token-sem (>>=-sem tt∈ return-sem))
    with Inverse.to (if-true-sem pt) ⟨$⟩ tt∈
       | Inverse.left-inverse-of (if-true-sem pt) tt∈
  from∘to (>>=-sem token-sem
             (>>=-sem .(Inverse.from (if-true-sem pt) ⟨$⟩ refl)
                      return-sem))
    | refl | refl = refl

  to∘from : ∀ {s} (eq : s ≡ [ t ]) → to (from eq) ≡ eq
  to∘from refl
    rewrite Inverse.right-inverse-of (if-true-sem pt) refl
    = refl

abstract

  -- Grammar.Infinite requires a lot more memory to type-check if this
  -- definition is made concrete (at the time of writing).

  tok-sem : ∀ {t′ t s} → t′ ∈ tok t · s ↔ (t ≡ t′ × s ≡ [ t ])
  tok-sem {t′} {t} {s} =
    t′ ∈ tok t · s                                   ↔⟨ <$>-sem ⟩
    (∃ λ p → p ∈ sat (λ t′ → t == t′) · s × t′ ≡ t)  ↔⟨ Σ.cong Inv.id (sat-sem ×-cong Inv.id) ⟩
    (∃ λ p → s ≡ [ proj₁ p ] × t′ ≡ t)               ↔⟨ Σ-assoc ⟩
    (∃ λ t″ → T (t == t″) × s ≡ [ t″ ] × t′ ≡ t)     ↔⟨ Σ.cong Inv.id (True↔ _ P.≡-irrelevant ×-cong Inv.id) ⟩
    (∃ λ t″ → t ≡ t″ × s ≡ [ t″ ] × t′ ≡ t)          ↔⟨ lemma ⟩
    (t ≡ t′ × s ≡ [ t ])                             ∎
    where
    open Related.EquationalReasoning

    lemma : (∃ λ t″ → t ≡ t″ × s ≡ [ t″ ] × t′ ≡ t) ↔
            (t ≡ t′ × s ≡ [ t ])
    lemma = record
      { to         = P.→-to-⟶ to
      ; from       = P.→-to-⟶ from
      ; inverse-of = record
        { left-inverse-of  = from∘to
        ; right-inverse-of = to∘from
        }
      }
      where
      to : ∀ {t′ t : Char} {s} →
           (∃ λ t″ → t ≡ t″ × s ≡ [ t″ ] × t′ ≡ t) → t ≡ t′ × s ≡ [ t ]
      to (_ , refl , refl , refl) = (refl , refl)

      from : ∀ {t′ t : Char} {s} →
             t ≡ t′ × s ≡ [ t ] → ∃ λ t″ → t ≡ t″ × s ≡ [ t″ ] × t′ ≡ t
      from (refl , refl) = (_ , refl , refl , refl)

      from∘to : ∀ {t′ t : Char} {s}
                (eqs : ∃ λ t″ → t ≡ t″ × s ≡ [ t″ ] × t′ ≡ t) →
                from (to eqs) ≡ eqs
      from∘to (_ , refl , refl , refl) = refl

      to∘from : ∀ {t′ t : Char} {s} (eqs : t ≡ t′ × s ≡ [ t ]) →
                to (from eqs) ≡ eqs
      to∘from (refl , refl) = refl

------------------------------------------------------------------------
-- An aside: An inductive version of the grammar type above wouldn't
-- be very useful (assuming that Char is finite)

module Aside (finite-number-of-tokens :
                ∃ λ (ts : List Char) → ∀ t → t ∈ ts) where

  open ≤-Reasoning

  infixl 15 _>>=_
  infixl 10 _∣_

  data GrammarI : Set → Set₁ where
    return : ∀ {A} → A → GrammarI A
    token  : GrammarI Char
    _>>=_  : ∀ {A B} → GrammarI A → (A → GrammarI B) → GrammarI B
    _∣_    : ∀ {A} → GrammarI A → GrammarI A → GrammarI A

  infix 4 _∈I_·_

  data _∈I_·_ : ∀ {A} → A → GrammarI A → List Char → Set₁ where
    return-sem : ∀ {A} {x : A} → x ∈I return x · []
    token-sem  : ∀ {t} → t ∈I token · [ t ]
    >>=-sem    : ∀ {A B x y s₁ s₂} {g₁ : GrammarI A}
                   {g₂ : A → GrammarI B} →
                 x ∈I g₁ · s₁ → y ∈I g₂ x · s₂ →
                 y ∈I g₁ >>= g₂ · s₁ ++ s₂
    left-sem   : ∀ {A} {g₁ g₂ : GrammarI A} {x s} →
                 x ∈I g₁ · s → x ∈I g₁ ∣ g₂ · s
    right-sem  : ∀ {A} {g₁ g₂ : GrammarI A} {x s} →
                 x ∈I g₂ · s → x ∈I g₁ ∣ g₂ · s

  -- A kind of parser for the inductive grammars, used to prove
  -- finite-number-of-results. Note that the "parser" is not quite
  -- correct when seen as a parser: it sometimes returns too many
  -- results. (The derivative of return x should be a failing
  -- grammar.)

  initial-bag : ∀ {A} (g : GrammarI A) →
                ∃ λ xs → ∀ {x} → x ∈I g · [] → x ∈ xs

  derivative : ∀ {A} (g : GrammarI A) t →
               ∃ λ g′ → ∀ {x s} → x ∈I g · t ∷ s → x ∈I g′ · s

  parse : ∀ {A} (g : GrammarI A) s →
          ∃ λ xs → ∀ {x} → x ∈I g · s → x ∈ xs
  parse g []      = initial-bag g
  parse g (t ∷ s) with derivative g t
  ... | g′ , ok₁ with parse g′ s
  ...   | xs , ok₂ = xs , ok₂ ∘ ok₁

  initial-bag (return x) = [ x ] , λ { .{x = x} return-sem → here refl }
  initial-bag token      = []    , λ ()
  initial-bag (g₁ ∣ g₂)  =
    Prod.zip
      _++_
      (λ {xs} i₁ i₂ →
       λ { (left-sem  ∈g₁) → Inverse.to ++↔             ⟨$⟩ inj₁ (i₁ ∈g₁)
         ; (right-sem ∈g₂) → Inverse.to (++↔ {xs = xs}) ⟨$⟩ inj₂ (i₂ ∈g₂)
         })
      (initial-bag g₁)
      (initial-bag g₂)
  initial-bag (_>>=_ {A = A} {B = B} g₁ g₂) with initial-bag g₁
  ... | xs , xs-ok = ys xs , λ ∈g₁>>=g₂ → lemma₁ ∈g₁>>=g₂ refl
    where
    ys : List A → List B
    ys xs = xs LMa.>>= λ x → proj₁ (initial-bag (g₂ x))

    lemma₂ : ∀ {x y} xs → x ∈ xs → y ∈I g₂ x · [] → y ∈ ys xs
    lemma₂ (x ∷ xs) (here refl) ∈g₂ =
      Inverse.to ++↔ ⟨$⟩ inj₁ (proj₂ (initial-bag (g₂ x)) ∈g₂)
    lemma₂ (z ∷ xs) (there x∈) ∈g₂ =
      Inverse.to (++↔ {xs = proj₁ (initial-bag (g₂ z))}) ⟨$⟩
        inj₂ (lemma₂ xs x∈ ∈g₂)

    lemma₁ : ∀ {x s} → x ∈I g₁ >>= g₂ · s → s ≡ [] → x ∈ ys xs
    lemma₁ (>>=-sem {s₁ = []}    ∈g₁ ∈g₂) refl = lemma₂ xs (xs-ok ∈g₁) ∈g₂
    lemma₁ (>>=-sem {s₁ = _ ∷ _} ∈g₁ ∈g₂) ()

  derivative (return x) t = return x , λ ()
  derivative token      t = return t , λ { .{s = []} token-sem → return-sem }
  derivative (g₁ ∣ g₂)  t =
    Prod.zip _∣_
             (λ {g₁′ g₂′} ok₁ ok₂ →
              λ { (left-sem  ∈g₁) → left-sem  (ok₁ ∈g₁)
                ; (right-sem ∈g₂) → right-sem (ok₂ ∈g₂)
                })
             (derivative g₁ t)
             (derivative g₂ t)
  derivative (_>>=_ {A = A} {B = B} g₁ g₂) t
    with derivative g₁ t | initial-bag g₁
  ... | g₁′ , g₁′-ok | xs , xs-ok =
    g′ xs , λ ∈g₁>>=g₂ → lemma₁ ∈g₁>>=g₂ refl
    where
    g′ : List A → GrammarI B
    g′ []       = g₁′ >>= g₂
    g′ (x ∷ xs) = return x >>= (λ x → proj₁ (derivative (g₂ x) t))
                ∣ g′ xs

    lemma₂ : ∀ {x y s} xs →
             x ∈ xs → y ∈I g₂ x · t ∷ s → y ∈I g′ xs · s
    lemma₂ (x ∷ xs) (here refl) ∈g₂ = left-sem (>>=-sem return-sem
                                        (proj₂ (derivative (g₂ x) t) ∈g₂))
    lemma₂ (z ∷ xs) (there x∈)  ∈g₂ = right-sem (lemma₂ xs x∈ ∈g₂)

    lemma₃ : ∀ {x y s₁ s₂} xs →
             x ∈I g₁′ · s₁ → y ∈I g₂ x · s₂ → y ∈I g′ xs · s₁ ++ s₂
    lemma₃ []       ∈g₁′ ∈g₂ = >>=-sem ∈g₁′ ∈g₂
    lemma₃ (x ∷ xs) ∈g₁′ ∈g₂ = right-sem (lemma₃ xs ∈g₁′ ∈g₂)

    lemma₁ : ∀ {y s s′} →
             y ∈I g₁ >>= g₂ · s → s ≡ t ∷ s′ → y ∈I g′ xs · s′
    lemma₁ (>>=-sem {s₁ = []}     ∈g₁ ∈g₂) refl = lemma₂ xs (xs-ok  ∈g₁) ∈g₂
    lemma₁ (>>=-sem {s₁ = .t ∷ _} ∈g₁ ∈g₂) refl = lemma₃ xs (g₁′-ok ∈g₁) ∈g₂

  -- If strings are restricted to have a given maximum length, then an
  -- inductive grammar generates a finite number of distinct results.

  finite-number-of-results :
    ∀ {A} (g : GrammarI A) n →
    ∃ λ xs → ∀ {x s} → length s ≤ n → x ∈I g · s → x ∈ xs
  finite-number-of-results g n =
    (all-strings n LMa.>>= proj₁ ∘ parse g) ,
    λ {_} {s} ≤n ∈g →
      Inverse.to ∈.>>=-∈↔ ⟨$⟩
        (_ , all-strings-ok s n ≤n , proj₂ (parse g s) ∈g)
    where
    all-strings : ℕ → List (List Char)
    all-strings 0       = [ [] ]
    all-strings (suc n) = all-strings n ++
                          (proj₁ finite-number-of-tokens LMa.>>= λ t →
                           List.map (_∷_ t) (all-strings n))

    all-strings-ok : ∀ s n → length s ≤ n → s ∈ all-strings n
    all-strings-ok []      zero    z≤n      = here refl
    all-strings-ok []      (suc n) z≤n      = Inverse.to ++↔ ⟨$⟩
                                                inj₁ (all-strings-ok [] n z≤n)
    all-strings-ok (t ∷ s) (suc n) (s≤s ≤n) =
      Inverse.to (++↔ {xs = all-strings n}) ⟨$⟩
        inj₂ (Inverse.to ∈.>>=-∈↔ ⟨$⟩
                (_ , proj₂ finite-number-of-tokens t
                   , Inverse.to (∈.map-∈↔ _) ⟨$⟩
                       (_ , all-strings-ok s n ≤n , refl)))

  -- No inductive grammar can generate strings of unbounded length.

  bounded-length :
    ∀ {A} (g : GrammarI A) →
    ∃ λ n → ∀ {x s} → x ∈I g · s → length s ≤ n
  bounded-length (return x) = 0 , λ { .{s = []}    return-sem → z≤n }
  bounded-length token      = 1 , λ { .{s = [ _ ]} token-sem  → s≤s z≤n }
  bounded-length (g₁ ∣ g₂)  =
    Prod.zip _+_
             (λ {n₁ n₂} b₁ b₂ →
              λ { {s = s} (left-sem ∈g₁) → begin
                  length s  ≤⟨ b₁ ∈g₁ ⟩
                  n₁        ≤⟨ m≤m+n _ _ ⟩
                  n₁ + n₂   ∎
                ; {s = s} (right-sem ∈g₂) → begin
                  length s  ≤⟨ b₂ ∈g₂ ⟩
                  n₂        ≤⟨ m≤n+m _ n₁ ⟩
                  n₁ + n₂   ∎
                })
             (bounded-length g₁)
             (bounded-length g₂)
  bounded-length (_>>=_ {A = A} g₁ g₂) with bounded-length g₁
  ... | n₁ , b₁ with finite-number-of-results g₁ n₁
  ...   | xs , xs-ok =
    n₁ + n₂ xs ,
    λ { .{s = _} (>>=-sem {s₁ = s₁} {s₂ = s₂} ∈g₁ ∈g₂) → begin
        length (s₁ ++ s₂)      ≡⟨ length-++ s₁ ⟩
        length s₁ + length s₂  ≤⟨ +-mono-≤ (b₁ ∈g₁) (lemma xs (xs-ok (b₁ ∈g₁) ∈g₁) ∈g₂) ⟩
        n₁        + n₂ xs      ∎ }
    where
    n₂ : List A → ℕ
    n₂ = foldr _⊔_ 0 ∘ List.map (λ x → proj₁ (bounded-length (g₂ x)))

    lemma : ∀ {x y s} xs → x ∈ xs → y ∈I g₂ x · s → length s ≤ n₂ xs
    lemma {s = s} (x ∷ xs) (here refl) y∈ = begin
      length s                               ≤⟨ proj₂ (bounded-length (g₂ x)) y∈ ⟩
      proj₁ (bounded-length (g₂ x))          ≤⟨ m≤m⊔n _ _ ⟩
      proj₁ (bounded-length (g₂ x)) ⊔ n₂ xs  ∎
    lemma {s = s} (z ∷ xs) (there x∈) y∈ = begin
      length s                               ≤⟨ lemma xs x∈ y∈ ⟩
      n₂ xs                                  ≤⟨ m≤m⊔n _ _ ⟩
      n₂ xs ⊔ proj₁ (bounded-length (g₂ z))  ≡⟨ ∧-comm (n₂ xs) _ ⟩
      proj₁ (bounded-length (g₂ z)) ⊔ n₂ xs  ∎
      where open DistributiveLattice NatP.⊓-⊔-distributiveLattice

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
open import Mockingbird.Forest using (Forest)

-- The Forest Without a Name
module Mockingbird.Problems.Chapter16 {b ℓ} (forest : Forest {b} {ℓ}) where

open import Data.Product using (_×_; _,_; ∃-syntax)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; _⇔_; Equivalence)
open import Relation.Binary using (_Respects_)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)

open Forest forest
import Mockingbird.Problems.Chapter14 forest as Chapter₁₄
open import Mockingbird.Problems.Chapter15 forest using (⇔-¬)

module _ {s} (Sings : Pred Bird s)
         (respects : Sings Respects _≈_)
         (LEM : ∀ x → Sings x ⊎ ¬ Sings x)
         (e : Bird)
         (law₁ : ∀ {x y} → Sings (e ∙ x ∙ y) → Sings y)
         (law₂ : ∀ {x y} → Sings (e ∙ x ∙ y) ⇔ (¬ Sings x))
         (law₃ : ∀ {x y} → Sings (e ∙ x ∙ y) ⇔ (¬ Sings x × Sings y))
         (law₄ : ∀ x → ∃[ y ] Sings y ⇔ Sings (e ∙ y ∙ x)) where

  IsSilent : Pred Bird s
  IsSilent x = ¬ Sings x

  private
    respects′ : IsSilent Respects _≈_
    respects′ x≈y ¬x-sings y-sings = ¬x-sings $ respects (sym x≈y) y-sings

    LEM′ : ∀ x → IsSilent x ⊎ ¬ IsSilent x
    LEM′ x with LEM x
    ... | inj₁ x-sings = inj₂ λ ¬x-sings → ¬x-sings x-sings
    ... | inj₂ ¬x-sings = inj₁ ¬x-sings

    law₁′ : ∀ {x y} → IsSilent y → IsSilent (e ∙ x ∙ y)
    law₁′ ¬y-sings exy-sings = ¬y-sings $ law₁ exy-sings

    law₂′ : ∀ {x y} → ¬ IsSilent x → IsSilent (e ∙ x ∙ y)
    law₂′ = Equivalence.g $ ⇔-¬ law₂

    law₃′ : ∀ {x y} → IsSilent x → IsSilent (e ∙ x ∙ y) → IsSilent y
    law₃′ {x} {y} ¬x-sings ¬exy-sings y-sings = Equivalence.f (⇔-¬ law₃) ¬exy-sings (¬x-sings , y-sings)

    law₄′ : ∀ x → ∃[ y ] IsSilent y ⇔ IsSilent (e ∙ y ∙ x)
    law₄′ x =
      let (y , y-sings⇔eyx-sings) = law₄ x
      in (y , ⇔-¬ y-sings⇔eyx-sings)

  problem : ∀ x → ¬ Sings x
  problem = Chapter₁₄.problem₁ IsSilent respects′ LEM′ e law₁′ law₂′ law₃′ law₄′

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
module Effect where

open import Data.List
open import Data.List.All
open import Data.List.Any
open import Level
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Function
open import Category.Monad
open import Data.Product
open import EffectUtil
open import Membership-equality hiding (_⊆_; set)

Effect : ∀ f → Set (suc f)
Effect f = (result : Set f) (i : Set f) (o : result → Set f) → Set f

record EFFECT (f : Level) : Set (suc f) where
  constructor mkEff
  field S : Set f
        E : Effect f

updateResTy : ∀ {f A E i o} → (val : A) →
              (es : List (EFFECT f)) →
              (prf : (mkEff i E) ∈ es) →
              (eff : E A i o) →
              List (EFFECT f)
updateResTy {o = o} val (mkEff i e ∷ es) (here px) eff = mkEff (o val) e ∷ es
updateResTy val (e ∷ es) (there prf) eff = e ∷ updateResTy val es prf eff

updateWith : ∀ {f ys} (ys' : List (EFFECT f)) → (xs : List (EFFECT f)) →
             (ys ⊆ xs) → List (EFFECT f)
updateWith [] xs inc = xs
updateWith (y' ∷ ys') xs [] = xs
updateWith (y' ∷ ys') (_ ∷ xs) (keep inc) = y' ∷ updateWith ys' xs inc
updateWith (y' ∷ ys') (x ∷ xs) (skip inc) = x ∷ updateWith (y' ∷ ys') xs inc

Handler : ∀ {f} → (Set f → Set f) → Effect f → Set (suc f)
Handler M e = ∀ {A a o res} → (r : res) → (eff : e A res o) →
              (k : ((x : A) → o x → M a)) → M a

-- @ A  The return type of the result
-- @ es The list of allowed side-effects
-- @ ce The function to compute a new list of allowed side-effects
data EffM {f : Level} (m : Set f → Set f) : (A : Set f) →
             (es : List (EFFECT f)) →
             (ce : A → List (EFFECT f)) → Set (suc f) where
  return : ∀ {A ce} (val : A) → EffM m A (ce val) ce
  _>>=_  : ∀ {A B es ce₁ ce₂} → EffM m A es ce₁ → (∀ x → EffM m B (ce₁ x) ce₂) → EffM m B es ce₂
  effect : ∀ {A E i es o} (prf : (mkEff i E) ∈ es) →
             (eff : E A i o) →
             EffM m A es (λ v → updateResTy v es prf eff)
  -- use to invoke sub-programs that use some or all of the available effects
  lift   : ∀ {A ys ys' xs} → (inc : ys ⊆ xs) →
           EffM m A ys ys' →
           EffM m A xs (λ v → updateWith (ys' v) xs inc)
  new : ∀ {A es} →
    (e : EFFECT f) →
    (val : EFFECT.S e) →
    Handler m (EFFECT.E e) →
    EffM {f} m A (e ∷ es) (λ v → e ∷ es) →
    EffM m A es (λ v → es)

pure : ∀ {l m A es} → A → EffM {l} m A es (λ v → es)
pure = return

_<*>_ : ∀ {l m A B es} → EffM {l} m (A → B) es (λ v → es) →
                    EffM {l} m A es (λ v → es) →
                    EffM {l} m B es (λ v → es)
_<*>_ prog v = prog >>= λ fn →
               v >>= λ arg →
               pure (fn arg)

_<$>_ : ∀ {l m A B es} → (f : A → B) → EffM {l} m A es (λ v → es) → EffM {l} m B es (λ v → es)
_<$>_ f m = pure f <*> m

data Env {f : Level} : (m : Set f → Set f) → List (EFFECT f) → Set (suc f) where
  [] : ∀ {m} → Env m []
  _∷_ : ∀ {m eff es a} → (el : Handler m eff × a) → Env m es → Env m (mkEff a eff ∷ es)

execEff : ∀ {f m A es E i} {o : A → Set f} {B} →
  Env {f} m es →
  (prf : (mkEff i E) ∈ es) →
  (eff : E A i o) →
  ((v : A) → Env {f} m (updateResTy v es prf eff) → m B) → m B
execEff {m = m} {A = A} {o = o} {B = B} ((handle , val) ∷ env) (here refl) eff k = handle val eff cont
  where
    cont : (v : A) → o v → m B
    cont v res = k v ((handle , res) ∷ env)
execEff (e ∷ env) (there prf) eff k = execEff env prf eff λ v → λ env' → k v (e ∷ env')

dropEnv : ∀ {f m ys xs} → Env {f} m ys → xs ⊆ ys → Env m xs
dropEnv [] [] = []
dropEnv (el ∷ env) [] = []
dropEnv (el ∷ env) (keep sub) = el ∷ (dropEnv env sub)
dropEnv (el ∷ env) (skip sub) = dropEnv env sub

rebuildEnv : ∀ {f m ys' ys xs} → Env {f} m ys' → (prf : ys ⊆ xs) →
             Env m xs → Env m (updateWith ys' xs prf)
rebuildEnv [] [] env = env
rebuildEnv (_ ∷ _) [] env = env
rebuildEnv [] (keep prf) env = env
rebuildEnv (el ∷ els) (keep prf) (_ ∷ env) = el ∷ rebuildEnv els prf env
rebuildEnv [] (skip prf) env = env
rebuildEnv (el ∷ els) (skip prf) (en ∷ env) = en ∷ rebuildEnv (el ∷ els) prf env

eff : ∀ {f m es A B ce} → Env {f} m es → EffM m A es ce → ((v : A) → Env m (ce v) → m B) → m B
eff env (return val) k = k val env
eff env (effM >>= c) k = eff env effM λ p' → λ env' → eff env' ((c p')) k
eff env (effect prf effP) k = execEff env prf effP k
eff env (lift inc effM) k = eff env' effM λ p' → λ envk → k p' (rebuildEnv envk inc env)
  where
    env' = dropEnv env inc
eff {f} {m} {es} {A} {B} env (new e val handler effM) k = eff ((handler , val) ∷ env) effM cont
  where
    cont : (v : A) → Env {f} m (e ∷ es) → m B
    cont v (val ∷ envk) = k v envk

run : ∀ {f a xs xs'} → ∀ m → (mon : RawMonad m) → (prog : EffM {f} m a xs xs') → Env m xs → m a
run m mon prog env = eff env prog λ r → λ env' → RawMonad.return mon r

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
-- Andreas, 2021-05-07, issue #5358 reported by ecavallo
-- Do not expand clauses with tactics attached to the target type!

open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

defaultTo : {A : Set} (x : A) → Term → TC ⊤
defaultTo x goal = do
  `x ← quoteTC x
  unify goal `x

record Class : Set where
  constructor con
  field
    x : Bool → Bool
    @(tactic defaultTo x) {y} : Bool → Bool
open Class

{- Correctly succeeds -}
testA : Class
testA = con (λ b → b)

{-
  WAS: Incorrectly fails with:
  Bool → Bool !=< Bool
  when checking that the inferred type of an application
    Bool → Bool
  matches the expected type
    Bool

What is happening here?

  - The coverage checker detects a missing clause
    testB .y : @(tactic defaultTo x) {Bool → Bool}.

  - It expands this to testB .y b : @(tactic defaultTo x) {Bool},
    eliminating the function type.

  - It then runs the tactic at the wrong type.

A fix is to not expand the clause if there is a tactic attached to the projections.
-}

testB : Class
testB .x = λ b → b

-- Should succeed


text:
-- Errors should precede warnings in info buffer
-- Reported by nad 2018-11-27
module Issue3416 where

A : Set
A = A

B : Set
B = Set


text:
module ModuleMacro where

record ⊤
  : Set
  where

module M where

module N where

  postulate

    A
      : Set

    B
      : Set

module O
  = M

module P
  = M

module Q
  = P

module R
  (x : ⊤)
  = N
  using (A)

module S
  = N
  renaming
  ( A
    to A'
  ; B
    to B'
  )

y
  : ⊤
y
  = record {O}

C
  : ⊤
  → Set
C
  = R.A

D
  : Set
D
  = S.B'

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on the Colist type
------------------------------------------------------------------------

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

module Codata.Colist.Properties where

open import Level using (Level)
open import Size
open import Codata.Thunk as Thunk using (Thunk; force)
open import Codata.Colist
open import Codata.Colist.Bisimilarity
open import Codata.Conat
open import Codata.Conat.Bisimilarity as coℕᵇ using (zero; suc)
import Codata.Conat.Properties as coℕₚ
open import Codata.Cowriter as Cowriter using ([_]; _∷_)
open import Codata.Cowriter.Bisimilarity as coWriterᵇ using ([_]; _∷_)
open import Codata.Stream as Stream using (Stream; _∷_)
open import Data.Vec.Bounded as Vec≤ using (Vec≤)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_)
open import Data.List.Relation.Binary.Equality.Propositional using (≋-refl)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just)
import Data.Maybe.Properties as Maybeₚ
open import Data.Maybe.Relation.Unary.All using (All; nothing; just)
open import Data.Nat.Base as ℕ using (zero; suc; z≤n; s≤s)
open import Data.Product as Prod using (_×_; _,_; uncurry)
open import Data.These.Base as These using (These; this; that; these)
open import Data.Vec.Base as Vec using (Vec; []; _∷_)
open import Function.Base
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; [_])

private
  variable
    a b c d : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    i : Size

------------------------------------------------------------------------
-- Functor laws

map-identity : ∀ (as : Colist A ∞) → i ⊢ map id as ≈ as
map-identity []       = []
map-identity (a ∷ as) = Eq.refl ∷ λ where .force → map-identity (as .force)

map-map-fusion : ∀ (f : A → B) (g : B → C) as {i} →
                 i ⊢ map g (map f as) ≈ map (g ∘ f) as
map-map-fusion f g []       = []
map-map-fusion f g (a ∷ as) =
  Eq.refl ∷ λ where .force → map-map-fusion f g (as .force)

------------------------------------------------------------------------
-- Relation to Cowriter

fromCowriter∘toCowriter≗id : ∀ (as : Colist A ∞) →
  i ⊢ fromCowriter (toCowriter as) ≈ as
fromCowriter∘toCowriter≗id []       = []
fromCowriter∘toCowriter≗id (a ∷ as) =
  Eq.refl ∷ λ where .force → fromCowriter∘toCowriter≗id (as .force)

------------------------------------------------------------------------
-- Properties of length

length-∷ : ∀ (a : A) as → i coℕᵇ.⊢ length (a ∷ as) ≈ 1 ℕ+ length (as .force)
length-∷ a as = suc (λ where .force → coℕᵇ.refl)

length-replicate : ∀ n (a : A) → i coℕᵇ.⊢ length (replicate n a) ≈ n
length-replicate zero    a = zero
length-replicate (suc n) a = suc λ where .force → length-replicate (n .force) a

length-++ : (as bs : Colist A ∞) →
            i coℕᵇ.⊢ length (as ++ bs) ≈ length as + length bs
length-++ []       bs = coℕᵇ.refl
length-++ (a ∷ as) bs = suc λ where .force → length-++ (as .force) bs

length-map : ∀ (f : A → B) as → i coℕᵇ.⊢ length (map f as) ≈ length as
length-map f []       = zero
length-map f (a ∷ as) = suc λ where .force → length-map f (as .force)

------------------------------------------------------------------------
-- Properties of replicate

replicate-+ : ∀ m n (a : A) →
              i ⊢ replicate (m + n) a ≈ replicate m a ++ replicate n a
replicate-+ zero    n a = refl
replicate-+ (suc m) n a = Eq.refl ∷ λ where .force → replicate-+ (m .force) n a

map-replicate : ∀ (f : A → B) n a →
                i ⊢ map f (replicate n a) ≈ replicate n (f a)
map-replicate f zero    a = []
map-replicate f (suc n) a =
  Eq.refl ∷ λ where .force → map-replicate f (n .force) a

lookup-replicate : ∀ k n (a : A) → All (a ≡_) (lookup k (replicate n a))
lookup-replicate k zero          a = nothing
lookup-replicate zero    (suc n) a = just Eq.refl
lookup-replicate (suc k) (suc n) a = lookup-replicate k (n .force) a

------------------------------------------------------------------------
-- Properties of unfold

map-unfold : ∀ (f : B → C) (alg : A → Maybe (A × B)) a →
             i ⊢ map f (unfold alg a) ≈ unfold (Maybe.map (Prod.map₂ f) ∘ alg) a
map-unfold f alg a with alg a
... | nothing       = []
... | just (a′ , b) = Eq.refl ∷ λ where .force → map-unfold f alg a′

module _ {alg : A → Maybe (A × B)} {a} where

  unfold-nothing : alg a ≡ nothing → unfold alg a ≡ []
  unfold-nothing eq with alg a
  ... | nothing = Eq.refl

  unfold-just : ∀ {a′ b} → alg a ≡ just (a′ , b) →
                i ⊢ unfold alg a ≈ b ∷ λ where .force → unfold alg a′
  unfold-just eq with alg a
  unfold-just Eq.refl | just (a′ , b) = Eq.refl ∷ λ where .force → refl

------------------------------------------------------------------------
-- Properties of scanl

length-scanl : ∀ (c : B → A → B) n as →
               i coℕᵇ.⊢ length (scanl c n as) ≈ 1 ℕ+ length as
length-scanl c n []       = suc λ where .force → zero
length-scanl c n (a ∷ as) = suc λ { .force → begin
  length (scanl c (c n a) (as .force))
    ≈⟨ length-scanl c (c n a) (as .force) ⟩
  1 ℕ+ length (as .force)
    ≈˘⟨ length-∷ a as ⟩
  length (a ∷ as) ∎ } where open coℕᵇ.≈-Reasoning

module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where

  private
    alg′ : (A × C) → Maybe ((A × C) × C)
    alg′ (a , c) = Maybe.map (uncurry step) (alg a) where
      step = λ a′ b → let b′ = cons c b in (a′ , b′) , b′

  scanl-unfold : ∀ nil a → i ⊢ scanl cons nil (unfold alg a)
                             ≈ nil ∷ (λ where .force → unfold alg′ (a , nil))
  scanl-unfold nil a with alg a | Eq.inspect alg a
  ... | nothing       | [ eq ] = Eq.refl ∷ λ { .force →
    sym (fromEq (unfold-nothing (Maybeₚ.map-nothing eq))) }
  ... | just (a′ , b) | [ eq ] = Eq.refl ∷ λ { .force → begin
    scanl cons (cons nil b) (unfold alg a′)
     ≈⟨ scanl-unfold (cons nil b) a′ ⟩
    (cons nil b ∷ _)
     ≈⟨ Eq.refl ∷ (λ where .force → refl) ⟩
    (cons nil b ∷ _)
     ≈˘⟨ unfold-just (Maybeₚ.map-just eq) ⟩
    unfold alg′ (a , nil) ∎ } where open ≈-Reasoning

------------------------------------------------------------------------
-- Properties of alignwith

map-alignWith : ∀ (f : C → D) (al : These A B → C) as bs →
                i ⊢ map f (alignWith al as bs) ≈ alignWith (f ∘ al) as bs
map-alignWith f al []         bs       = map-map-fusion (al ∘′ that) f bs
map-alignWith f al as@(_ ∷ _) []       = map-map-fusion (al ∘′ this) f as
map-alignWith f al (a ∷ as)   (b ∷ bs) =
  Eq.refl ∷ λ where .force → map-alignWith f al (as .force) (bs .force)

length-alignWith : ∀ (al : These A B → C) as bs →
                   i coℕᵇ.⊢ length (alignWith al as bs) ≈ length as ⊔ length bs
length-alignWith al []         bs       = length-map (al ∘ that) bs
length-alignWith al as@(_ ∷ _) []       = length-map (al ∘ this) as
length-alignWith al (a ∷ as)   (b ∷ bs) =
  suc λ where .force → length-alignWith al (as .force) (bs .force)

------------------------------------------------------------------------
-- Properties of zipwith

map-zipWith : ∀ (f : C → D) (zp : A → B → C) as bs →
              i ⊢ map f (zipWith zp as bs) ≈ zipWith (λ a → f ∘ zp a) as bs
map-zipWith f zp []       _        = []
map-zipWith f zp (_ ∷ _)  []       = []
map-zipWith f zp (a ∷ as) (b ∷ bs) =
  Eq.refl ∷ λ where .force → map-zipWith f zp (as .force) (bs .force)

length-zipWith : ∀ (zp : A → B → C) as bs →
                 i coℕᵇ.⊢ length (zipWith zp as bs) ≈ length as ⊓ length bs
length-zipWith zp []         bs       = zero
length-zipWith zp as@(_ ∷ _) []       = zero
length-zipWith zp (a ∷ as)   (b ∷ bs) =
  suc λ where .force → length-zipWith zp (as .force) (bs .force)

------------------------------------------------------------------------
-- Properties of drop

drop-nil : ∀ m → i ⊢ drop {A = A} m [] ≈ []
drop-nil zero    = []
drop-nil (suc m) = []

drop-drop-fusion : ∀ m n (as : Colist A ∞) →
                   i ⊢ drop n (drop m as) ≈ drop (m ℕ.+ n) as
drop-drop-fusion zero    n as       = refl
drop-drop-fusion (suc m) n []       = drop-nil n
drop-drop-fusion (suc m) n (a ∷ as) = drop-drop-fusion m n (as .force)

map-drop : ∀ (f : A → B) m as → i ⊢ map f (drop m as) ≈ drop m (map f as)
map-drop f zero    as       = refl
map-drop f (suc m) []       = []
map-drop f (suc m) (a ∷ as) = map-drop f m (as .force)

length-drop : ∀ m (as : Colist A ∞) → i coℕᵇ.⊢ length (drop m as) ≈ length as ∸ m
length-drop zero    as       = coℕᵇ.refl
length-drop (suc m) []       = coℕᵇ.sym (coℕₚ.0∸m≈0 m)
length-drop (suc m) (a ∷ as) = length-drop m (as .force)

drop-fromList-++-identity : ∀ (as : List A) bs →
                            drop (List.length as) (fromList as ++ bs) ≡ bs
drop-fromList-++-identity []       bs = Eq.refl
drop-fromList-++-identity (a ∷ as) bs = drop-fromList-++-identity as bs

drop-fromList-++-≤ : ∀ (as : List A) bs {m} → m ℕ.≤ List.length as →
                     drop m (fromList as ++ bs) ≡ fromList (List.drop m as) ++ bs
drop-fromList-++-≤ []       bs z≤n     = Eq.refl
drop-fromList-++-≤ (a ∷ as) bs z≤n     = Eq.refl
drop-fromList-++-≤ (a ∷ as) bs (s≤s p) = drop-fromList-++-≤ as bs p

drop-fromList-++-≥ : ∀ (as : List A) bs {m} → m ℕ.≥ List.length as →
                     drop m (fromList as ++ bs) ≡ drop (m ℕ.∸ List.length as) bs
drop-fromList-++-≥ []       bs z≤n     = Eq.refl
drop-fromList-++-≥ (a ∷ as) bs (s≤s p) = drop-fromList-++-≥ as bs p

drop-⁺++-identity : ∀ (as : List⁺ A) bs →
                    drop (List⁺.length as) (as ⁺++ bs) ≡ bs .force
drop-⁺++-identity (a ∷ as) bs = drop-fromList-++-identity as (bs .force)

------------------------------------------------------------------------
-- Properties of cotake

length-cotake : ∀ n (as : Stream A ∞) → i coℕᵇ.⊢ length (cotake n as) ≈ n
length-cotake zero    as       = zero
length-cotake (suc n) (a ∷ as) =
  suc λ where .force → length-cotake (n .force) (as .force)

map-cotake : ∀ (f : A → B) n as →
             i ⊢ map f (cotake n as) ≈ cotake n (Stream.map f as)
map-cotake f zero    as       = []
map-cotake f (suc n) (a ∷ as) =
  Eq.refl ∷ λ where .force → map-cotake f (n .force) (as .force)

------------------------------------------------------------------------
-- Properties of chunksOf

module Map-ChunksOf (f : A → B) n where

  open ChunksOf n using (chunksOfAcc)

  map-chunksOf : ∀ as →
    i coWriterᵇ.⊢ Cowriter.map (Vec.map f) (Vec≤.map f) (chunksOf n as)
                ≈ chunksOf n (map f as)
  map-chunksOfAcc : ∀ m as {k≤ k≡ k≤′ k≡′} →
                    (∀ vs → Vec≤.map f (k≤ vs) ≡ k≤′ (Vec≤.map f vs)) →
                    (∀ vs → Vec.map f (k≡ vs) ≡ k≡′ (Vec.map f vs)) →
                    i coWriterᵇ.⊢ Cowriter.map (Vec.map f) (Vec≤.map f)
                                        (chunksOfAcc m k≤ k≡ as)
                                ≈ chunksOfAcc m k≤′ k≡′ (map f as)

  map-chunksOf as = map-chunksOfAcc n as (λ vs → Eq.refl) (λ vs → Eq.refl)

  map-chunksOfAcc zero    as       eq-≤ eq-≡ =
      eq-≡ [] ∷ λ where .force → map-chunksOf as
  map-chunksOfAcc (suc m) []       eq-≤ eq-≡ = coWriterᵇ.[ eq-≤ Vec≤.[] ]
  map-chunksOfAcc (suc m) (a ∷ as) eq-≤ eq-≡ =
    map-chunksOfAcc m (as .force) (eq-≤ ∘ (a Vec≤.∷_)) (eq-≡ ∘ (a Vec.∷_))

open Map-ChunksOf using (map-chunksOf) public

------------------------------------------------------------------------
-- Properties of fromList

fromList-++ : (as bs : List A) →
              i ⊢ fromList (as List.++ bs) ≈ fromList as ++ fromList bs
fromList-++ []       bs = refl
fromList-++ (a ∷ as) bs = Eq.refl ∷ λ where .force → fromList-++ as bs

fromList-scanl : ∀ (c : B → A → B) n as →
                 i ⊢ fromList (List.scanl c n as) ≈ scanl c n (fromList as)
fromList-scanl c n []       = Eq.refl ∷ λ where .force → refl
fromList-scanl c n (a ∷ as) =
  Eq.refl ∷ λ where .force → fromList-scanl c (c n a) as

map-fromList : ∀ (f : A → B) as →
               i ⊢ map f (fromList as) ≈ fromList (List.map f as)
map-fromList f []       = []
map-fromList f (a ∷ as) = Eq.refl ∷ λ where .force → map-fromList f as

length-fromList : (as : List A) →
                  i coℕᵇ.⊢ length (fromList as) ≈ fromℕ (List.length as)
length-fromList []       = zero
length-fromList (a ∷ as) = suc (λ where .force → length-fromList as)

------------------------------------------------------------------------
-- Properties of fromStream

fromStream-++ : ∀ (as : List A) bs →
                i ⊢ fromStream (as Stream.++ bs) ≈ fromList as ++ fromStream bs
fromStream-++ []       bs = refl
fromStream-++ (a ∷ as) bs = Eq.refl ∷ λ where .force → fromStream-++ as bs

fromStream-⁺++ : ∀ (as : List⁺ A) bs →
                 i ⊢ fromStream (as Stream.⁺++ bs)
                   ≈ fromList⁺ as ++ fromStream (bs .force)
fromStream-⁺++ (a ∷ as) bs =
  Eq.refl ∷ λ where .force → fromStream-++ as (bs .force)

fromStream-concat : (ass : Stream (List⁺ A) ∞) →
                    i ⊢ concat (fromStream ass) ≈ fromStream (Stream.concat ass)
fromStream-concat (as@(a ∷ _) ∷ ass) = begin
  concat (fromStream (as ∷ ass))
    ≈⟨ Eq.refl ∷ (λ { .force → ++⁺ ≋-refl (fromStream-concat (ass .force))}) ⟩
  a ∷ _
    ≈⟨ sym (fromStream-⁺++ as _) ⟩
  fromStream (Stream.concat (as ∷ ass)) ∎ where open ≈-Reasoning

fromStream-scanl : ∀ (c : B → A → B) n as →
                   i ⊢ scanl c n (fromStream as)
                     ≈ fromStream (Stream.scanl c n as)
fromStream-scanl c n (a ∷ as) =
  Eq.refl ∷ λ where .force → fromStream-scanl c (c n a) (as .force)

map-fromStream : ∀ (f : A → B) as →
                 i ⊢ map f (fromStream as) ≈ fromStream (Stream.map f as)
map-fromStream f (a ∷ as) =
  Eq.refl ∷ λ where .force → map-fromStream f (as .force)


text:
module Cats.Category.Constructions.Epi where

open import Level

open import Cats.Category.Base

module Build {lo la l≈} (Cat : Category lo la l≈) where

  private open module Cat = Category Cat
  open Cat.≈-Reasoning

  IsEpi : ∀ {A B} → A ⇒ B → Set (lo ⊔ la ⊔ l≈)
  IsEpi {A} {B} f = ∀ {C} {g h : B ⇒ C} → g ∘ f ≈ h ∘ f → g ≈ h

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
------------------------------------------------------------------------
-- A library for working with dependently typed syntax
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- This library is leaning heavily on two of Conor McBride's papers:
--
-- * Type-Preserving Renaming and Substitution.
--
-- * Outrageous but Meaningful Coincidences: Dependent type-safe
--   syntax and evaluation.

-- This module gives a brief overview of the modules in the library.

module README where

------------------------------------------------------------------------
-- The library

-- Contexts, variables, context morphisms, context extensions, etc.

import deBruijn.Context

-- Parallel substitutions (defined using an inductive family).

import deBruijn.Substitution.Data.Basics

-- A map function for the substitutions.

import deBruijn.Substitution.Data.Map

-- Some simple substitution combinators. (Given a term type which
-- supports weakening and transformation of variables to terms various
-- substitutions are defined and various lemmas proved.)

import deBruijn.Substitution.Data.Simple

-- Given an operation which applies a substitution to a term,
-- satisfying some properties, more operations and lemmas are
-- defined/proved.
--
-- (This module reexports various other modules.)

import deBruijn.Substitution.Data.Application

-- A module which repackages (and reexports) the development under
-- deBruijn.Substitution.Data.

import deBruijn.Substitution.Data

-- Some modules mirroring the development under
-- deBruijn.Substitution.Data, but using substitutions defined as
-- functions rather than data.
--
-- The functional version of substitutions is in some respects easier
-- to work with than the one based on data, but in other respects more
-- awkward. I maintain both developments so that they can be compared.

import deBruijn.Substitution.Function.Basics
import deBruijn.Substitution.Function.Map
import deBruijn.Substitution.Function.Simple

-- The two definitions of substitutions are isomorphic (assuming
-- extensionality).

import deBruijn.Substitution.Isomorphic

------------------------------------------------------------------------
-- An example showing how the library can be used

-- A well-typed representation of a dependently typed language.

import README.DependentlyTyped.Term

-- Normal and neutral terms.

import README.DependentlyTyped.NormalForm

-- Instantiation of deBruijn.Substitution.Data for terms.

import README.DependentlyTyped.Term.Substitution

-- Instantiation of deBruijn.Substitution.Data for normal and neutral
-- terms.

import README.DependentlyTyped.NormalForm.Substitution

-- Normalisation by evaluation.

import README.DependentlyTyped.NBE

-- Various equality checkers (some complete, all sound).

import README.DependentlyTyped.Equality-checker

-- Raw terms.

import README.DependentlyTyped.Raw-term

-- A type-checker (sound).

import README.DependentlyTyped.Type-checker

-- A definability result: A "closed value" is the semantics of a
-- closed term if and only if it satisfies all "Kripke predicates".

import README.DependentlyTyped.Definability

-- An observation: There is a term without a corresponding syntactic
-- type (given some assumptions).

import README.DependentlyTyped.Term-without-type

-- Another observation: If the "Outrageous but Meaningful
-- Coincidences" approach is used to formalise a language, then you
-- can end up with an extensional type theory (with equality
-- reflection).

import README.DependentlyTyped.Extensional-type-theory

-- Inductively defined beta-eta-equality.

import README.DependentlyTyped.Beta-Eta

-- TODO: Add an untyped example.

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties that are related to pointwise lifting of binary
-- relations to sigma types and make use of heterogeneous equality
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Product.Relation.Binary.Pointwise.Dependent.WithK where

open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.Dependent
open import Function
open import Function.Inverse using (Inverse)
open import Relation.Binary using (_⇒_)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- The propositional equality setoid over sigma types can be
-- decomposed using Pointwise

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

  Pointwise-≡⇒≡ : Pointwise B _≡_ (λ x y → x ≅ y) ⇒ _≡_
  Pointwise-≡⇒≡ (P.refl , H.refl) = P.refl

  ≡⇒Pointwise-≡ : _≡_ ⇒ Pointwise B _≡_ (λ x y → x ≅ y)
  ≡⇒Pointwise-≡ P.refl = (P.refl , H.refl)

  Pointwise-≡↔≡ : Inverse (setoid (P.setoid A) (H.indexedSetoid B))
                  (P.setoid (Σ A B))
  Pointwise-≡↔≡ = record
    { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
    ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
    ; inverse-of = record
      { left-inverse-of  = uncurry (λ _ _ → (P.refl , H.refl))
      ; right-inverse-of = λ _ → P.refl
      }
    }


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

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

variable A : Set

postulate
  f : (A → A) → Bool
  f-id    :           f {A} (λ x → x) ≡ true
  f-const : (c : A) → f     (λ x → c) ≡ false

{-# REWRITE f-id    #-}
{-# REWRITE f-const #-}


text:
module ShouldBePi where

data One : Set where
  one : One

err1 : One
err1 = \x -> x

err2 : One
err2 = one one

err3 : One
err3 x = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Numeral.Natural.Oper.Modulo.Proofs.Algorithm where

import Lvl
open import Logic
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Order
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity
open import Type

-- The many steps variant of: `[ r , b ] 𝐒(a') mod' 𝐒(b') = [ 𝐒(r) , b ] a' mod' b'` from the definition.
mod'-ind-step : ∀{r b' a b c} → [ r , b' ] (a + c) mod' (b + c) ≡ [ (r + c) , b' ] a mod' b
mod'-ind-step {_}{_} {_}{_}{𝟎}   = [≡]-intro
mod'-ind-step {r}{b'}{a}{b}{𝐒 c} = mod'-ind-step {𝐒 r}{b'}{a}{b}{c = c}

-- The many steps variant of: `[ r , b ] 𝐒(a') mod' 𝐒(b') = [ 𝐒(r) , b ] a' mod' b'` from the definition when the dividend is greater than the modulus.
mod'-ind-step-modulo : ∀{r m' a m} → [ r , m' ] (a + m) mod' m ≡ [ (r + m) , m' ] a mod' 𝟎
mod'-ind-step-modulo {r}{m'}{a}{𝟎} =
  [ r       , m' ] (a + 𝟎) mod' 𝟎 🝖[ _≡_ ]-[]
  [ (r + 𝟎) , m' ] a       mod' 𝟎 🝖-end
mod'-ind-step-modulo {r}{m'}{a}{𝐒 m} =
  [ r          , m' ] (a + 𝐒(m)) mod' 𝐒(m) 🝖[ _≡_ ]-[]
  [ r          , m' ] 𝐒(a + m)   mod' 𝐒(m) 🝖[ _≡_ ]-[]
  [ 𝐒(r)       , m' ] (a + m)    mod' m    🝖[ _≡_ ]-[ mod'-ind-step-modulo {𝐒 r}{m'}{a}{m} ]
  [ 𝐒(r + m)   , m' ] a          mod' 𝟎    🝖[ _≡_ ]-[]
  [ (r + 𝐒(m)) , m' ] a          mod' 𝟎    🝖-end

-- When states and modulus is zero, the result is zero.
mod'-zero-all-except-dividend : ∀{a} → ([ 0 , 0 ] a mod' 0 ≡ 0)
mod'-zero-all-except-dividend {𝟎}    = [≡]-intro
mod'-zero-all-except-dividend {𝐒(a)} = mod'-zero-all-except-dividend {a}

mod'-greater-dividend : ∀{r b' a b} → (a > b) → ([ r , b' ] a mod' b ≡ [ 𝟎 , b' ] (a −₀ 𝐒(b)) mod' b')
mod'-greater-dividend {r} {b'} {.(𝐒 _)} {𝟎}   (succ ab) = [≡]-intro
mod'-greater-dividend {r} {b'} {.(𝐒 _)} {𝐒 b} (succ ab) = mod'-greater-dividend ab

mod'-zero-modulo-greater-dividend : ∀{r a b} → (a > b) → ([ r , 𝟎 ] a mod' b ≡ 𝟎)
mod'-zero-modulo-greater-dividend {r} {.𝟏}         {𝟎}   (succ {y = 𝟎}   ab) = [≡]-intro
mod'-zero-modulo-greater-dividend {r} {.(𝐒 (𝐒 a))} {𝟎}   (succ {y = 𝐒 a} ab) = mod'-zero-all-except-dividend {a}
mod'-zero-modulo-greater-dividend {r} {.(𝐒 _)}     {𝐒 b} (succ           ab) = mod'-zero-modulo-greater-dividend ab

mod'-lesser-dividend : ∀{r b' a b} → (a ≤ b) → ([ r , b' ] a mod' b ≡ r + a)
mod'-lesser-dividend {r} {b'} min = [≡]-intro
mod'-lesser-dividend {r} {b'} (succ ab) = mod'-lesser-dividend {𝐒 r} {b'} ab

-- When the number is the temporary modulus, the result is zero.
mod'-equal-dividend : ∀{r b' b} → ([ r , b' ] 𝐒(b) mod' b) ≡ 𝟎
mod'-equal-dividend {r}{b'}{b} = mod'-greater-dividend {r}{b'} (reflexivity(_≤_) {𝐒 b})

mod'-sumᵣ-modulo : ∀{r b' a b} → ([ r , b' ] (a + 𝐒(b)) mod' b) ≡ ([ 𝟎 , b' ] a mod' b')
mod'-sumᵣ-modulo {r}{b'}{a}{b} = mod'-greater-dividend {r}{b'}{a + 𝐒(b)}{b} (succ([≤]-of-[+]ᵣ {a}{b})) 🝖 congruence₁(a ↦ [ 𝟎 , b' ] a mod' b') (inverseOperᵣ(_+_)(_−₀_) {a}{b})

-- When the
mod'-sumₗ-modulo : ∀{r b' a b} → ([ r , b' ] (𝐒(b) + a) mod' b) ≡ ([ 𝟎 , b' ] a mod' b')
mod'-sumₗ-modulo {r}{b'}{a}{b} = congruence₁(a ↦ [ r , b' ] a mod' b) (commutativity(_+_) {𝐒(b)}{a}) 🝖 mod'-sumᵣ-modulo {r}{b'}{a}{b}

mod'-maxᵣ : ∀{r b a b'} → ⦃ _ : (b' ≤ b) ⦄ → (([ r , r + b ] a mod' b') ≤ r + b)
mod'-maxᵣ {r} {b} {𝟎} {b'} ⦃ b'b ⦄ = [≤]-of-[+]ₗ
mod'-maxᵣ {r} {𝟎} {𝐒 a} {.0} ⦃ min ⦄ = mod'-maxᵣ {𝟎} {r} {a} {r} ⦃ reflexivity(_≤_) ⦄
mod'-maxᵣ {r} {𝐒 b} {𝐒 a} {.0} ⦃ min ⦄ = mod'-maxᵣ {𝟎} {𝐒(r + b)} {a} {𝐒(r + b)} ⦃ reflexivity(_≤_) ⦄
mod'-maxᵣ {r} {𝐒 b} {𝐒 a} {𝐒 b'} ⦃ succ {b'} p ⦄ = mod'-maxᵣ {𝐒 r} {b} {a} {b'} ⦃ p ⦄

mod'-maxₗ : ∀{r b a b'} → (([ r , b ] a mod' b') ≤ r + a)
mod'-maxₗ {𝟎}  {_}  {𝟎}  {_}    = min
mod'-maxₗ {𝐒 r}{b}  {𝟎}  {𝐒 b'} = mod'-maxₗ {𝐒 r}{𝟎}{𝟎}{b'}
mod'-maxₗ {𝐒 r}{𝐒 b}{𝟎}  {b'}   = mod'-maxₗ {𝐒 r}{b}{𝟎}{b'}
mod'-maxₗ {𝐒 r}{b}  {𝐒 a}{𝟎}    = mod'-maxₗ {𝟎} {b} {a} {b} 🝖 [≤]-successor ([≤]-successor ([≤]-of-[+]ᵣ {r}))
mod'-maxₗ {r}  {b}  {𝐒 a}{𝐒 b'} = mod'-maxₗ {𝐒 r} {b} {a} {b'}
mod'-maxₗ {𝟎}  {𝟎}  {𝐒 a}{𝟎}    = [≤]-successor(mod'-maxₗ {𝟎} {𝟎} {a} {𝟎})
mod'-maxₗ {𝟎}  {𝐒 b}{𝐒 a}{𝟎}    = [≤]-successor(mod'-maxₗ {0} {𝐒 b} {a} {𝐒 b})
mod'-maxₗ {𝐒 r}{𝟎}  {𝟎}  {𝟎}    = succ(mod'-maxₗ {r}{𝟎}{𝟎}{𝟎})

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Adjoint.Relative where

-- Relative Adjoints, in their biased, level-restricted version
--   In other words, this uses the Hom-Setoid equivalent variant
--   of the adjoint formulation because relative adjoints don't
--   have a natural unit/counit formulation.

-- We use the Altenkirch-Chapman-Uustalu formulation, which means
-- that what is adjoint is a Functor and a Category.

open import Level

open import Data.Product using (_,_; _×_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality using (Π; _⟶_; _⟨$⟩_)
open import Relation.Binary using (Setoid)

-- be explicit in imports to 'see' where the information comes from
open import Categories.Adjoint
open import Categories.Category.Core using (Category)
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Category.Instance.Setoids
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Hom using (Hom[_][-,-])
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism)
import Categories.Morphism.Reasoning as MR
open import Categories.Monad.Relative renaming (Monad to RMonad)

private
  variable
    o o′ ℓ ℓ′ e e′ : Level
    E : Category o ℓ e

record RelativeAdjoint {C : Category o ℓ e} (D : Category o ℓ e) (J : Functor E C)  : Set (levelOfTerm D ⊔ levelOfTerm J) where
  field
    L : Functor E D
    R : Functor D C

  private
    module C = Category C
    module D = Category D
    module E = Category E
    module L = Functor L
    module R = Functor R
    module J = Functor J

  Hom[L-,-] : Bifunctor E.op D (Setoids _ _)
  Hom[L-,-] = Hom[ D ][-,-] ∘F (L.op ⁂ idF)

  Hom[J-,R-] : Bifunctor E.op D (Setoids _ _)
  Hom[J-,R-] = Hom[ C ][-,-] ∘F (J.op ⁂ R)

  module Hom[L-,-] = Functor Hom[L-,-]
  module Hom[J-,R-] = Functor Hom[J-,R-]

  field
    Hom-NI : NaturalIsomorphism Hom[J-,R-] Hom[L-,-]

RA⇒RMonad : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} {J : Functor E C} → RelativeAdjoint D J → RMonad J
RA⇒RMonad {C = C} {D} {E} {J} RA = record
  { F₀ = F₀ (R ∘F L)
  ; unit = λ {c} → ⇐.η (c , F₀ L c) ⟨$⟩ D.id {F₀ L c}
  ; extend = λ {X} {Y} k → F₁ R (⇒.η (X , F₀ L Y) ⟨$⟩ k)
  ; identityʳ = idʳ
  ; identityˡ = R.F-resp-≈ (iso.isoʳ _ D.Equiv.refl) ○ R.identity
  ; assoc = a
  ; extend-≈ = λ k≈h → F-resp-≈ R (Π.cong (⇒.η _) k≈h)
  }
  where
  open RelativeAdjoint RA
  open Functor
  open NaturalIsomorphism Hom-NI
  module D = Category D
  module E = Category E
  module J = Functor J
  module L = Functor L
  module R = Functor R
  open Category C
  open HomReasoning
  open MR C
  idʳ : {x y : E.Obj} {k : J.₀ x ⇒ F₀ (R ∘F L) y} → R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ≈ k
  idʳ {x} {y} {k} = begin
    R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id)               ≈⟨ introʳ J.identity ⟩
    (R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id)) ∘ J.₁ E.id  ≈⟨ assoc ⟩
    R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k) ∘ (⇐.η (x , L.₀ x) ⟨$⟩ D.id) ∘ J.₁ E.id    ≈⟨ ⇐.sym-commute (E.id , ⇒.η (x , L.₀ y) ⟨$⟩ k) (D.Equiv.refl) ⟩
    ⇐.η (x , L.₀ y) ⟨$⟩ ((⇒.η (x , L.₀ y) ⟨$⟩ k) D.∘ D.id D.∘ L.F₁ E.id)   ≈⟨ Π.cong (⇐.η _) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
    ⇐.η (x , L.₀ y) ⟨$⟩ (⇒.η (x , L.₀ y) ⟨$⟩ k)                            ≈⟨ iso.isoˡ (x , _) Equiv.refl ⟩
    k            ∎
  a : {x y z : E.Obj} {k : J.₀ x ⇒ R.₀ (L.₀ y)} {l : J.₀ y ⇒ R.₀ (L.₀ z)} →
      R.₁ (⇒.η (x , L.₀ z) ⟨$⟩ R.₁ (⇒.η (y , L.₀ z) ⟨$⟩ l) ∘ k) ≈
      R.₁ (⇒.η (y , L.₀ z) ⟨$⟩ l) ∘ R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k)
  a {x} {y} {z} {k} {l} = begin
    R.₁ (⇒.η (x , L.₀ z) ⟨$⟩ (R.₁ (⇒.η (y , L.₀ z) ⟨$⟩ l) ∘ k)) ≈⟨ R.F-resp-≈ lemma ⟩
    R.₁ ((⇒.η (y , L.₀ z) ⟨$⟩ l) D.∘ (⇒.η (x , L.₀ y) ⟨$⟩ k))   ≈⟨ R.homomorphism ⟩
    R.₁ (⇒.η (y , L.₀ z) ⟨$⟩ l) ∘ R.₁ (⇒.η (x , L.₀ y) ⟨$⟩ k)   ∎
    where
    xz = (x , L.₀ z)
    yz = (y , L.₀ z)
    xy = (x , L.₀ y)
    module DR = D.HomReasoning
    lemma : ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k D.≈ (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k)
    lemma = DR.begin
      ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ k                DR.≈⟨ Π.cong (⇒.η xz) (refl⟩∘⟨ introʳ J.identity ) ⟩
      ⇒.η xz ⟨$⟩ R.₁ (⇒.η yz ⟨$⟩ l) ∘ (k ∘ J.₁ E.id)   DR.≈⟨ ⇒.commute (E.id , ⇒.η yz ⟨$⟩ l) Equiv.refl ⟩
      (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) D.∘ L.₁ E.id   DR.≈⟨ D.sym-assoc  ⟩
      ((⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k)) D.∘ L.₁ E.id DR.≈⟨ MR.elimʳ D L.identity ⟩
      (⇒.η yz ⟨$⟩ l) D.∘ (⇒.η xy ⟨$⟩ k) DR.∎

⊣⇒RAdjoint : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} (L : Functor C D) (R : Functor D C) (J : Functor E C) → L ⊣ R → RelativeAdjoint D J
⊣⇒RAdjoint {C = C} {D} L R J A = record
  { L = L ∘F J
  ; R = R
  ; Hom-NI = record
    { F⇒G = ntHelper record
      { η = λ _ → record { _⟨$⟩_ = Radjunct ; cong = ∘-resp-≈ʳ ∙ L.F-resp-≈ }
      ; commute = λ _ x≈y → Radjunct-comm x≈y
      }
    ; F⇐G = ntHelper record
      { η = λ _ → record { _⟨$⟩_ = Ladjunct ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈ }
      ; commute = λ _ x≈y → Ladjunct-comm x≈y
      }
    ; iso = λ X → record
      { isoˡ = λ eq → LRadjunct≈id ○ eq
      ; isoʳ = Equiv.trans RLadjunct≈id
      }
    }
  }
  where
  open Adjoint A
  open Category D
  module C = Category C
  module L = Functor L
  module R = Functor R
  module J = Functor J
  open C.HomReasoning

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:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition

module Rings.Divisible.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Setoid S
open Equivalence eq
open Ring R

_∣_ : Rel A
a ∣ b = Sg A (λ c → (a * c) ∼ b)

divisibleWellDefined : {x y a b : A} → (x ∼ y) → (a ∼ b) → x ∣ a → y ∣ b
divisibleWellDefined x=y a=b (c , xc=a) = c , transitive (*WellDefined (symmetric x=y) reflexive) (transitive xc=a a=b)


text:
module Scratch.Subset where
open import Level renaming (zero to lzero; suc to lsuc)

open import Relation.Unary using (Pred; Satisfiable) renaming (Decidable to Dec₁)
open import Relation.Binary renaming (Decidable to Dec₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_ ; _≢_; refl; cong; sym; trans; subst₂)
open Eq.≡-Reasoning
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base as ℕ using (ℕ;_+_;_∸_;suc;zero; _<_)
open import Data.Bool using (not; Bool)
open import Data.Bool.Properties hiding (_≟_)
open import Data.Product
open import Data.Sum renaming ([_,_] to _⊞_)
open import Data.Vec hiding (allFin)
open import Data.Vec.Properties
open import Data.Fin.Properties using (∃-toSum)
open import Data.Fin hiding (fold; _+_; _<_)
  renaming (zero to fzero ; suc to fsuc)
  hiding (_≟_)

open import Relation.Nullary.Negation using (contradiction)

open import Data.Fin.Properties using (suc-injective)
open import Data.Fin.Subset
open import Data.Fin.Subset.Properties
open import Data.Maybe
open import Data.List.Base renaming (tabulate to tab ;
                                     foldr to fold;
                                     [] to <>;
                                     [_] to <_>;
                                     map to lmap;
                                     lookup to llookup)
                           hiding (tail; any)
open import Data.List.Properties
open import Data.List.Membership.Propositional
  renaming (_∈_ to _∈ℓ_)
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any as Any hiding (tail)
open import Data.List.Relation.Unary.Any.Properties
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.AllPairs as AllPairs
open import Data.List.Relation.Unary.AllPairs.Properties

open import Function.Base

open import Relation.Nullary

open import Data.Nat.Properties
  using (_≟_; m+n∸m≡n; +-∸-assoc; +-∸-comm; +-comm; +-identityʳ; 0∸n≡0; n≤0⇒n≡0; n≢0⇒n>0; +-0-commutativeMonoid)

open import Algebra.Core
import Algebra.Properties.BooleanAlgebra

_\\_ : ∀ {n} → Op₂ (Subset n)
S \\ T = S ∩ (∁ T)

s\\⊥≡s : ∀ {n : ℕ} → (S : Subset n) → (S \\ ⊥) ≡ S
s\\⊥≡s {n} S = begin
              S ∩ (∁ ⊥) ≡⟨ cong (S ∩_) ⊥≉⊤  ⟩
              S ∩ ⊤ ≡⟨ ∩-identityʳ _ ⟩
              S ∎ where open Algebra.Properties.BooleanAlgebra (∪-∩-booleanAlgebra n)

Disj : ∀ {n} → Subset n → Subset n → Set
Disj S T = S ∩ T ≡ ⊥

Disj-sym : ∀ {n} → Symmetric (Disj {n = n})
Disj-sym {n} {S} {T} S∩T≡⊥ = begin T ∩ S ≡⟨ ∩-comm T S ⟩ S ∩ T ≡⟨ S∩T≡⊥ ⟩ ⊥ ∎

∩-⊆-stable : ∀ {n} → ∀ {p q} → (r : Subset n) → p ⊆ q → (p ∩ r) ⊆ (q ∩ r)
∩-⊆-stable {_} {p} {q} r p⊆q x∈p∩r = let
                                     x∈p = proj₁ (x∈p∩q⁻ p r x∈p∩r)
                                     x∈r = proj₂ (x∈p∩q⁻ p r x∈p∩r)
                                     in x∈p∩q⁺ ( p⊆q x∈p , x∈r )

idʳ⇒⊆ : ∀ {n} → (S T : Subset n) → (S ∪ T) ≡ T → S ⊆ T
idʳ⇒⊆ {n} S T sut≡t = subst₂ _⊆_ refl sut≡t (p⊆p∪q T)

p∩∁p≡⊥ : ∀ {n} → (p : Subset n) → p ∩ ∁ p ≡ ⊥
p∩∁p≡⊥ [] = refl
p∩∁p≡⊥ (outside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)
p∩∁p≡⊥ (inside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)

p⊆q⇒p∩∁q≡⊥ : ∀ {n} → {S T : Subset n} → S ⊆ T → S ∩ (∁ T) ≡ ⊥
p⊆q⇒p∩∁q≡⊥ {_} {S} {T} s⊆t = let
                               a = p∩∁p≡⊥ _
                               b : S ∩ (∁ T) ⊆ T ∩ (∁ T)
                               b = ∩-⊆-stable (∁ T) s⊆t
                               c = subst₂ _⊆_ refl a b
                               in ⊆-antisym c (⊆-min _)

p⊆q⇒p∩q≡p : ∀ {n} → (S T : Subset n) → S ⊆ T → S ∩ T ≡ S
p⊆q⇒p∩q≡p S T s⊆t = sym (begin
                  S ≡˘⟨ ∩-identityʳ _ ⟩
                  S ∩ ⊤ ≡˘⟨ cong (_ ∩_) (p∪∁p≡⊤ _) ⟩
                  S ∩ (T ∪ (∁ T)) ≡⟨ ∩-distribˡ-∪ _ _ _ ⟩
                  (S ∩ T) ∪ (S ∩ (∁ T)) ≡⟨ cong ((S ∩ T) ∪_) (p⊆q⇒p∩∁q≡⊥ s⊆t)  ⟩
                  (S ∩ T) ∪ ⊥ ≡⟨ ∪-identityʳ _ ⟩
                  S ∩ T ∎)

disj⇒⊆∁ : ∀ {n} → {S T : Subset n} → Disj S T → S ⊆ (∁ T)
disj⇒⊆∁ {n} {S} {T} dst = let ct≡suct = begin
                                  ∁ T ≡˘⟨ ∪-identityˡ _ ⟩
                                  ⊥ ∪ (∁ T) ≡˘⟨ cong (_∪ (∁ T)) dst ⟩
                                  (S ∩ T) ∪ (∁ T) ≡⟨ ∪-distribʳ-∩ _ _ _ ⟩
                                  (S ∪ (∁ T)) ∩ (T ∪ (∁ T)) ≡⟨ cong ((S ∪ (∁ T)) ∩_) (p∪∁p≡⊤ T) ⟩
                                  (S ∪ (∁ T)) ∩ ⊤ ≡⟨ ∩-identityʳ _ ⟩
                                  S ∪ (∁ T) ∎
                  in idʳ⇒⊆ S (∁ T) (sym ct≡suct)

⊆∁⇒disj : ∀ {n} → {S T : Subset n} → S ⊆ (∁ T) → Disj S T
⊆∁⇒disj {n} {S} {T} s⊆∁t = begin
                         S ∩ T ≡˘⟨ cong (S ∩_) (¬-involutive T ) ⟩
                         S ∩ (∁ (∁ T)) ≡⟨ p⊆q⇒p∩∁q≡⊥ s⊆∁t ⟩
                         ⊥ ∎ where open Algebra.Properties.BooleanAlgebra (∪-∩-booleanAlgebra n)

p⊆r×q⊆r⇒p∪q⊆r : ∀ {n} → { p q r : Subset n} → (p ⊆ r) × (q ⊆ r) → (p ∪ q) ⊆ r
p⊆r×q⊆r⇒p∪q⊆r {n} {p} {q} {r} (p⊆r , q⊆r) x∈p∪q = let
                                                    y = x∈p∪q⁻ {n} p q x∈p∪q
                                                    in (p⊆r ⊞ q⊆r) y

pᵢ⊆q⇒⋃pᵢ⊆q : ∀ {n m} → (S : Subset n) → (ϕ : Fin m → Subset n) →
             (∀ i → (ϕ i) ⊆ S) → (⋃ (tab ϕ) ⊆ S)

pᵢ⊆q⇒⋃pᵢ⊆q {_} {zero} S _ _ = ⊆-min S
pᵢ⊆q⇒⋃pᵢ⊆q {n} {suc m} S ϕ Δ = let
                        y : ((ϕ fzero) ∪ (⋃(tab (ϕ ∘ fsuc)))) ⊆ S
                        y = p⊆r×q⊆r⇒p∪q⊆r ( Δ fzero , pᵢ⊆q⇒⋃pᵢ⊆q S (λ z → ϕ (fsuc z)) (λ i → Δ (fsuc i)) )
                        in subst₂ _⊆_ refl refl y

pᵢ⊆q⇒⋃pᵢ⊆q-list : ∀ {n} → ∀ S → ∀ (L : List (Subset n)) →
                  All (_⊆ S) L → (⋃ L) ⊆ S
pᵢ⊆q⇒⋃pᵢ⊆q-list S <> _ = ⊆-min S
pᵢ⊆q⇒⋃pᵢ⊆q-list S (x ∷ xs) (h ∷ t) = subst₂ _⊆_ refl refl (p⊆r×q⊆r⇒p∪q⊆r ( h , pᵢ⊆q⇒⋃pᵢ⊆q-list S xs t ))

-- obvious but exposes S for computation later
drop-outside : ∀ {n} → (S : Subset n) → ∣ outside ∷ S ∣ ≡ ∣ S ∣
drop-outside S = refl

drop-disj : ∀ {n} → {x y : Side} → {p q : Subset n} → Disj (x ∷ p) (y ∷ q) → Disj p q
drop-disj {zero} {_} {_} {[]} {[]} _ = refl
drop-disj d = cong Data.Vec.tail d

∣p⊍q∣≡∣p∣+∣q∣ : ∀ {n} → ∀ (p q : Subset n) → Disj p q → ∣ p ∪ q ∣ ≡ ∣ p ∣ + ∣ q ∣
∣p⊍q∣≡∣p∣+∣q∣ {zero} [] [] d = refl
∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (outside ∷ q) d = begin
                                                        -- ∣ (outside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨⟩
                                                        ∣ p ∪ q ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {outside} d) ⟩
                                                        -- ∣ p ∣ + ∣ q ∣ ≡⟨⟩
                                                        ∣ (outside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎

∣p⊍q∣≡∣p∣+∣q∣ {suc n} (inside ∷ p) (outside ∷ q) d = begin -- {!   !} -- begin
                                                        ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ refl ⟩ -- cong suc refl ⟩
                                                        -- suc ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ cong suc {!   !} ⟩ -- cong suc refl ⟩
                                                        suc ∣ p ∪ q ∣ ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {inside} {outside} d)) ⟩
                                                        suc (∣ p ∣ + ∣ q ∣) ≡⟨⟩
                                                        (suc ∣ p ∣) + ∣ q ∣ ≡⟨⟩
                                                        ∣ (inside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎
∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (inside ∷ q) d = begin
                                                        ∣ (outside ∷ p) ∪ (inside ∷ q) ∣ ≡⟨ refl ⟩
                                                        suc ∣ p ∪ q ∣ ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {inside} d)) ⟩
                                                        suc (∣ p ∣ + ∣ q ∣) ≡⟨ cong suc (+-comm ∣ p ∣ ∣ q ∣) ⟩
                                                        suc (∣ q ∣ + ∣ p ∣) ≡⟨ refl ⟩
                                                        (suc ∣ q ∣) + ∣ p ∣ ≡⟨⟩
                                                        ∣ (inside ∷ q) ∣ + ∣ (outside ∷ p) ∣ ≡⟨ +-comm ∣ (inside ∷ q) ∣ ∣ (outside ∷ p) ∣ ⟩
                                                        ∣ (outside ∷ p) ∣ + ∣ (inside ∷ q) ∣ ∎

-- why can't we use fold fusion here?
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ : ∀ {n m} → (ϕ : Fin m → Subset n) →
                (∀ i j → (i ≢ j) → Disj (ϕ i) (ϕ j)) →
                ∣ ⋃ (tab ϕ) ∣ ≡ fold _+_ 0 (tab (∣_∣ ∘ ϕ))
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} {zero} ϕ _ = begin
                                 ∣ ⋃ {n} <> ∣ ≡⟨⟩
                                 -- ∣ fold (_∪_ {n}) ⊥ <> ∣ ≡⟨⟩
                                 ∣ ⊥ {n} ∣ ≡⟨ ∣⊥∣≡0 n ⟩
                                 0 ≡⟨⟩
                                 fold _+_ 0 <> ∎
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} {suc m} ϕ Δ = begin
                                  ∣ ⋃ (tab ϕ) ∣ ≡⟨⟩
                                  ∣ (ϕ fzero) ∪ (⋃ (tab (ϕ ∘ fsuc))) ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ (ϕ fzero) (⋃ (tab (ϕ ∘ fsuc))) d ⟩
                                  ∣ (ϕ fzero) ∣ + ∣ ⋃ (tab (ϕ ∘ fsuc)) ∣ ≡⟨ cong (∣ (ϕ fzero) ∣ +_) (∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {_} {m} (ϕ ∘ fsuc) λ i j i≢j → Δ (fsuc i) (fsuc j) (i≢j ∘ suc-injective) ) ⟩
                                  ∣ (ϕ fzero) ∣ + (fold _+_ 0 (tab (∣_∣ ∘ (ϕ ∘ fsuc)))) ≡⟨⟩
                                  fold _+_ 0 (tab (∣_∣ ∘ ϕ)) ∎
                                  where
                                  a : ∀ (i : Fin m) → Disj (ϕ (fsuc i)) (ϕ fzero)
                                  a = λ i → Δ (fsuc i) fzero (λ ())
                                  b : ∀ (i : Fin m) → (ϕ (fsuc i) ⊆ ∁ (ϕ fzero))
                                  b = disj⇒⊆∁ ∘ a
                                  c : ⋃ (tab (ϕ ∘ fsuc)) ⊆ ∁ (ϕ fzero)
                                  c = pᵢ⊆q⇒⋃pᵢ⊆q (∁ (ϕ fzero)) (ϕ ∘ fsuc) b

                                  e : Disj (⋃ (tab (ϕ ∘ fsuc))) (ϕ fzero)
                                  e = ⊆∁⇒disj c

                                  d : Disj (ϕ fzero) (⋃ (tab (ϕ ∘ fsuc)))
                                  d = begin
                                        (ϕ fzero) ∩ (⋃ (tab (ϕ ∘ fsuc))) ≡⟨ ∩-comm _ _ ⟩
                                        (⋃ (tab (ϕ ∘ fsuc))) ∩ (ϕ fzero) ≡⟨ e ⟩
                                        ⊥ ∎

∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣-list : ∀ {n} (C : List (Subset n)) →
                     AllPairs Disj C →
                     ∣ ⋃ C ∣ ≡ fold _+_ 0 (lmap ∣_∣ C)
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣-list {n} <> Δℓ = begin
                             ∣ ⋃ {n} <> ∣ ≡⟨⟩
                             -- ∣ fold (_∪_ {n}) ⊥ <> ∣ ≡⟨⟩
                             ∣ ⊥ {n} ∣ ≡⟨ ∣⊥∣≡0 n ⟩
                             0 ≡⟨⟩
                             fold _+_ 0 <> ∎
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣-list {n} (s ∷ C) (h ∷ t) = begin
                                  ∣ ⋃ (s ∷ C) ∣ ≡⟨⟩
                                  ∣ s ∪ (⋃ C) ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ s (⋃ C) DisjsUC ⟩
                                  ∣ s ∣ + ∣ ⋃ C ∣ ≡⟨ cong (∣ s ∣ +_) (∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣-list {n} C t ) ⟩
                                  ∣ s ∣ + (fold _+_ 0 (lmap ∣_∣ C)) ≡⟨⟩
                                  fold _+_ 0 (lmap ∣_∣ (s ∷ C)) ∎
                                  where
                                  a : All (λ x → x ⊆ ∁ s) C
                                  a = All.map (disj⇒⊆∁ ∘ Disj-sym) h
                                  c : ⋃ C ⊆ ∁ s
                                  c = pᵢ⊆q⇒⋃pᵢ⊆q-list (∁ s) C a
                                  e : Disj (⋃ C) s
                                  e = ⊆∁⇒disj c
                                  DisjsUC : Disj s (⋃ C)
                                  DisjsUC = Disj-sym e

⋃-remove : ∀ {n} {L : List (Subset n)} →
           ∀ s → (s∈L : s ∈ℓ L) →
           (⋃ L) ≡ s ∪ ⋃ (L Any.─ s∈L)
⋃-remove {n} {<>} _ = λ ()
⋃-remove {n} {x ∷ xs} s (here px) = begin
                                      ⋃ (x ∷ xs) ≡⟨ refl ⟩
                                      x ∪ (⋃ xs) ≡˘⟨ cong (_∪ _) px ⟩
                                      s ∪ (⋃ xs) ≡⟨ cong (_ ∪_) refl ⟩
                                      s ∪ ⋃ ((x ∷ xs) Data.List.Base.─ fzero ) ≡⟨ cong (_ ∪_) refl ⟩
                                      s ∪ ⋃ ((x ∷ xs) Any.─ (here {P = P} px)) ∎
                                      where
                                      P : Pred (Subset n) lzero
                                      P = s ≡_

⋃-remove {n} {x ∷ xs} s (there s∈L) = begin
                                        x ∪ (⋃ xs) ≡⟨ cong (x ∪_) (⋃-remove {L = xs} s s∈L) ⟩
                                        x ∪ (s ∪ ⋃ (xs Any.─ s∈L)) ≡˘⟨ ∪-assoc _ _ _ ⟩ -- TODO: -- use solver
                                        (x ∪ s) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ cong (_∪ _) (∪-comm x s) ⟩
                                        (s ∪ x) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ ∪-assoc _ _ _ ⟩
                                        s ∪ (x ∪ ⋃ (xs Any.─ s∈L)) ≡⟨ refl ⟩
                                        s ∪ ⋃ ((x ∷ xs) Any.─ (there s∈L)) ∎

cover-⊤ : ∀ {n} → (L : List (Subset n)) →
          (∀ (x : Fin n) → Any (x ∈_) L ) →
          ⊤ {n} ≡ ⋃ L

cover-⊤ {n} L ∃lx∈l = ⊆-antisym ⊤⊆⋃L (⊆-max (⋃ L)) where
  ⊤⊆⋃L : ⊤ ⊆ (⋃ L)
  ⊤⊆⋃L {x} _ = let
                  (l , l∈ℓL , x∈l) = find {P = x ∈_} (∃lx∈l x)
                  l⊆l∪* = p⊆p∪q {p = l} (⋃ (L Any.─ l∈ℓL))
                  x∈l∪* = l⊆l∪* {x} x∈l
                in subst₂ _∈_ refl (sym (⋃-remove l l∈ℓL)) x∈l∪*

-- 👇 not essential

|s\\t| : ∀ {n : ℕ} → ∀ {S T : Subset n} → T ⊆ S → ∣ S \\ T ∣ ≡ ∣ S ∣ ∸ ∣ T ∣
|s\\t| {.0} {[]} {T} t⊆s = begin
                              ∣ [] \\ T ∣ ≡⟨ n≤0⇒n≡0 (∣p∩q∣≤∣p∣ [] (∁ T)) ⟩
                              0 ≡˘⟨ 0∸n≡0 ∣ T ∣ ⟩
                              ∣ [] ∣ ∸ ∣ T ∣
                              ∎
|s\\t| {.(suc _)} {inside ∷ S} {inside ∷ T} t⊆s = |s\\t| {_} {S} {T} (drop-∷-⊆ t⊆s)
|s\\t| {.(suc _)} {outside ∷ S} {outside ∷ T} t⊆s = |s\\t| {_} {S} {T} (drop-∷-⊆ t⊆s)
|s\\t| {.(suc _)} {outside ∷ S} {inside ∷ T} t⊆s = let z = (t⊆s here)
                                                       y = []=⇒lookup z
                                                       w = not-¬ y
                                                     in ⊥-elim (w refl)
|s\\t| {(suc n)} {inside ∷ S} {outside ∷ T} t⊆s = sym (begin
                                                        ∣ inside ∷ S ∣ ∸ ∣ outside ∷ T ∣ ≡⟨ refl ⟩
                                                        (suc ∣ S ∣) ∸ ∣ outside ∷ T ∣ ≡⟨ cong ((suc ∣ S ∣) ∸_) (drop-outside T) ⟩
                                                        (1 + ∣ S ∣) ∸ ∣ T ∣ ≡⟨ cong (_∸ ∣ T ∣) (Data.Nat.Properties.+-comm _ ∣ S ∣)⟩
                                                        (∣ S ∣ + 1) ∸ ∣ T ∣ ≡⟨ +-∸-comm  1 (p⊆q⇒∣p∣≤∣q∣ (drop-∷-⊆ {n} {_} {_} {T} {S} t⊆s)) ⟩
                                                        (∣ S ∣ ∸ ∣ T ∣) + 1 ≡⟨ Data.Nat.Properties.+-comm (∣ S ∣ ∸ ∣ T ∣) _ ⟩
                                                        (suc (∣ S ∣ ∸ ∣ T ∣)) ≡˘⟨ cong suc  (|s\\t| {n} {S} {T} (drop-∷-⊆ {n} t⊆s))⟩
                                                        (suc ∣ S \\ T ∣) ≡⟨ refl ⟩
                                                        ∣ (inside ∷ S) \\ (outside ∷ T) ∣ ∎)

fst : ∀ {n} → (s : Subset n) → Nonempty s → Fin n
fst {suc n} (x ∷ rest) ne with (∃-toSum ne)
... | inj₁ _ = fzero
... | inj₂ b = let w = drop-there (proj₂ b)
                   z = (proj₁ b , w)
               in fsuc (fst rest z)

record Partition (n : ℕ) : Set where
  field
    Carrier : Subset n
    size : ℕ
    -- try parts as Data.Vec.Functional
    -- or try parts as List (Subset n) for ease of updates
    parts : Fin size → Subset n
    -- nne : 0 ℕ.< m
    nnd : ∀ i → Nonempty (parts i)
    all-⊆ : ∀ i → (parts i) ⊆ Carrier
    disj : ∀ i j → i ≢ j → Disj (parts i) (parts j)
    cover : Carrier ≡ ⋃ (tab parts)

  traversal : Vec (Fin n) size
  traversal = Data.Vec.tabulate λ i → fst (parts i) (nnd i)

  _P∈ : (j : Fin n) → Dec ( j ∈ Carrier )
  j P∈ = (j ∈? Carrier)

  -- open import Data.Vec.Relation.Unary.Any {0ℓ} {Fin n}
  -- anyRel : {_≈_ : Rel (Fin n) 0ℓ } → Dec₂ _≈_ → (j : Fin n) → Dec (Any (j ≈_) traversal)
  -- anyRel _≈?_ j = any (j ≈?_) traversal

  -- do I need this for counting arguments?
  respects : Rel (Fin n) 0ℓ → Set _
  respects _≈_ = ∀ x y → x ≈ y → ∃ λ i → (x ∈ parts i) × (y ∈ parts i)

  -- proj i = index (proof anyRel ≈ j)
  -- ∀ i → tabulate (i ≈?_) ≡ proj i

⊥P : ∀ {n} → Partition n
⊥P {n} = record { Carrier = ⊥ {n} ;
                  size = 0 ;
                  parts = λ () ;
                  all-⊆ = λ () ;
                  nnd = λ () ;
                  disj = λ i () ;
                  cover = refl }

------ has holes
-- add : ∀ {n} {≈ : Rel (Fin n) 0ℓ } → Partition n → (Dec₂ ≈) → Fin n → Partition n
-- add P ≈ j with (j P∈) where open Partition P
-- ... | yes _ = P
-- ... | no j∉P with (anyRel ≈ j) where open Partition P
-- ... | yes p = {!   !}
-- ... | no ¬p = record { Carrier = Carrier ∪ ⁅ j ⁆ ;
--                        size = suc size ;
--                        parts = λ { fzero → ⁅ j ⁆ ;
--                                    (fsuc k) → parts k } ;
--                        nnd = {!   !} ;
--                        all-⊆ = {!   !} ;
--                        disj = {!   !} ;
--                        cover = {!   !}
--                        } where open Partition P

----junk👇--------------------------------------------------------
-- ↓ : ∀ {n m : ℕ} → ∀ {S : Subset n} → ( 0 < m ) →
--      (P : Partition S (suc m)) → Partition (S \\ Partition.p P fzero) m
-- ↓ {_} {m} {S} 0<m P = record { p = p∘fsuc;
--                                nne = 0<m ;
--                                nnd = λ i → Partition.nnd P (fsuc i) ;
--                                all-⊆ = all-⊆' ;
--                                disj = disj' ;
--                                cover = c } where
--                              open Partition P
--                              p∘fsuc : _
--                              p∘fsuc = p ∘ fsuc
--
--                              all-⊆' : ∀ (i : Fin m) → (p (fsuc i)) ⊆ (S \\ (p fzero))
--                              all-⊆' i x∈pfsuci = let
--                                           x : _
--                                           x = all-⊆ (fsuc i)
--                                           y : Disj (p (fsuc i)) (p fzero)
--                                           y = disj (fsuc i) fzero λ ()
--                                           -- x ∈ (S \\ p fzero)
--                                           r : _
--                                           r = disj⇒⊆∁ {_} {p (fsuc i)} {p fzero} y
--                                           s : _
--                                           s = Partition.all-⊆ P (fsuc i) x∈pfsuci
--                                           t : _
--                                           t = r x∈pfsuci
--                                          in x∈p∩q⁺ ( s , t )
--
--                              disj' : _
--                              disj' i j i≢j = disj (fsuc i) (fsuc j) (i≢j ∘ suc-injective)
--
--                              c : _
--                              c = let
--                                     a : _
--                                     a = cover
--                                     b : _
--                                     b = S ≡ (p fzero) ∪ (⋃ (tab p∘fsuc))
--                                     S₀ = (p fzero)
--                                     d = begin
--                                           S \\ S₀ ≡⟨ cong (_\\ S₀) (Partition.cover P) ⟩
--                                           (⋃ (S₀ ∷ (tab p∘fsuc))) \\ S₀ ≡⟨ cong (_\\ S₀) refl ⟩
--                                           (S₀ ∪ (⋃ (tab p∘fsuc))) \\ S₀    ≡⟨ refl ⟩
--                                           (S₀ ∪ (⋃ (tab p∘fsuc))) ∩ (∁ S₀) ≡⟨ ∩-distribʳ-∪ _ _ _ ⟩
--                                           (S₀ ∩ (∁ S₀)) ∪ ((⋃ (tab p∘fsuc)) ∩ (∁ S₀)) ≡⟨ cong (_∪ ((⋃ (tab p∘fsuc)) ∩ (∁ S₀))) (p∩∁p≡⊥ _) ⟩
--                                           ⊥ ∪ ((⋃ (tab p∘fsuc)) ∩ (∁ S₀)) ≡⟨ ∪-identityˡ _ ⟩
--                                           (⋃ (tab p∘fsuc)) ∩ (∁ S₀) ≡⟨ {!   !} ⟩
--                                           (⋃ (tab p∘fsuc)) -- ≡⟨ ? ⟩
--                                           ∎
--                                     t = {!   !}
--                                  in t
--
-- this seems pretty obvious but helps rule out case with a single set below
-- tab0 : ∀ {m : ℕ} → ∀ {B : Set} → {ϕ : Fin (suc m) → B} → (m ≡ ℕ.zero) → (tab ϕ) ≡ < ϕ fzero >
-- tab0 {zero} m≡0 = refl
--
-- would follow trivially from a kind of guarded (dependent)
-- fold fusion with h = ∣_∣ f = _∪_ and g = _+c_
-- cc : ∀ {n m : ℕ} → {S : Subset n} →
--      ∀ (P : Partition S m) → (card P) ≡ ∣ S ∣
-- cc {n} {m = suc m'} {S} P with m' ≟ 0
-- ... | yes m'≡0 = begin
--                   (card P) ≡⟨ refl ⟩
--                   fold _+c_ 0 (tab p) ≡⟨ cong (fold _+c_ 0) (tab0 {m'} {Subset n} {p} m'≡0) ⟩
--                   fold _+c_ 0 < p fzero > ≡⟨ refl ⟩
--                   (p fzero) +c 0  ≡⟨ refl ⟩
--                   -- (p fzero) +c (fold _+c_ 0 <>) ≡⟨ refl ⟩
--                   -- fold _+c_ 0 ((p fzero) ∷ <>) ≡⟨ refl ⟩
--                   ∣ (p fzero) ∣ + 0 ≡⟨ +-identityʳ _ ⟩
--                   ∣ (p fzero) ∣ ≡˘⟨ cong ∣_∣ (∪-identityʳ (p fzero)) ⟩
--                   ∣ (p fzero) ∪ ⊥ ∣ ≡˘⟨ refl ⟩
--                   ∣ ⋃ < (p fzero) > ∣ ≡˘⟨ cong ∣_∣ (cong ⋃ (tab0 {m'} {Subset n} {p} m'≡0)) ⟩
--                   ∣ ⋃ (tab p) ∣ ≡˘⟨ cong ∣_∣ cover ⟩
--                   ∣ S ∣ ∎ where
--                   open Partition P
--
-- ... | no ¬m'≡0 = begin
--               (card P) ≡⟨⟩
--               fold _+c_ 0 ((p fzero) ∷ tab (p ∘ fsuc))  ≡⟨⟩
--               (p fzero) +c (fold _+c_ 0 (tab (p ∘ fsuc))) ≡⟨⟩
--               ∣ (p fzero) ∣ + (fold _+c_ 0 (tab (p ∘ fsuc))) ≡˘⟨ cong (∣ (p fzero) ∣ +_) refl ⟩
--               ∣ (p fzero) ∣ + card (↓ r P) ≡⟨ cong (_ +_) (cc (↓ r P)) ⟩
--               ∣ (p fzero) ∣ + ∣ S \\ (p fzero) ∣ ≡⟨ cong (_ +_) (|s\\t| (all-⊆ fzero)) ⟩
--               ∣ (p fzero) ∣ + ( ∣ S ∣ ∸ ∣ (p fzero) ∣ ) ≡˘⟨ +-∸-assoc ∣ (p fzero) ∣ (p⊆q⇒∣p∣≤∣q∣ (all-⊆ fzero)) ⟩
--               (∣ (p fzero) ∣ + ∣ S ∣) ∸ ∣ (p fzero) ∣ ≡⟨ m+n∸m≡n ∣ (p fzero) ∣ ∣ S ∣ ⟩
--               ∣ S ∣ ∎ where
--              open Partition P
--              r = (n≢0⇒n>0 ¬m'≡0)

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


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

module Definition.Typed.Consequences.Inversion where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties

open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product

-- Inversion of natural number type.
inversion-ℕ : ∀ {Γ C} → Γ ⊢ ℕ ∷ C → Γ ⊢ C ≡ U
inversion-ℕ (ℕⱼ x) = refl (Uⱼ x)
inversion-ℕ (conv x x₁) = trans (sym x₁) (inversion-ℕ x)

-- Inversion of Π-types.
inversion-Π : ∀ {F G Γ C}
            → Γ ⊢ Π F ▹ G ∷ C → Γ ⊢ F ∷ U × Γ ∙ F ⊢ G ∷ U × Γ ⊢ C ≡ U
inversion-Π (Πⱼ x ▹ x₁) = x , x₁ , refl (Uⱼ (wfTerm x))
inversion-Π (conv x x₁) = let a , b , c = inversion-Π x
                          in  a , b , trans (sym x₁) c

-- Inversion of zero.
inversion-zero : ∀ {Γ C} → Γ ⊢ zero ∷ C → Γ ⊢ C ≡ ℕ
inversion-zero (zeroⱼ x) = refl (ℕⱼ x)
inversion-zero (conv x x₁) = trans (sym x₁) (inversion-zero x)

-- Inversion of successor.
inversion-suc : ∀ {Γ t C} → Γ ⊢ suc t ∷ C → Γ ⊢ t ∷ ℕ × Γ ⊢ C ≡ ℕ
inversion-suc (sucⱼ x) = x , refl (ℕⱼ (wfTerm x))
inversion-suc (conv x x₁) =
  let a , b = inversion-suc x
  in  a , trans (sym x₁) b

-- Inversion of natural recursion.
inversion-natrec : ∀ {Γ c g n A C} → Γ ⊢ natrec C c g n ∷ A
  → (Γ ∙ ℕ ⊢ C)
  × Γ ⊢ c ∷ C [ zero ]
  × Γ ⊢ g ∷ Π ℕ ▹ (C ▹▹ C [ suc (var 0) ]↑)
  × Γ ⊢ n ∷ ℕ
  × Γ ⊢ A ≡ C [ n ]
inversion-natrec (natrecⱼ x d d₁ n) = x , d , d₁ , n , refl (substType x n)
inversion-natrec (conv d x) = let a , b , c , d , e = inversion-natrec d
                              in  a , b , c , d , trans (sym x) e

-- Inversion of application.
inversion-app :  ∀ {Γ f a A} → Γ ⊢ (f ∘ a) ∷ A →
  ∃₂ λ F G → Γ ⊢ f ∷ Π F ▹ G × Γ ⊢ a ∷ F × Γ ⊢ A ≡ G [ a ]
inversion-app (d ∘ⱼ d₁) = _ , _ , d , d₁ , refl (substTypeΠ (syntacticTerm d) d₁)
inversion-app (conv d x) = let a , b , c , d , e = inversion-app d
                           in  a , b , c , d , trans (sym x) e

-- Inversion of lambda.
inversion-lam : ∀ {t A Γ} → Γ ⊢ lam t ∷ A →
  ∃₂ λ F G → Γ ⊢ F × (Γ ∙ F ⊢ t ∷ G × Γ ⊢ A ≡ Π F ▹ G)
inversion-lam (lamⱼ x x₁) = _ , _ , x , x₁ , refl (Πⱼ x ▹ (syntacticTerm x₁))
inversion-lam (conv x x₁) = let a , b , c , d , e = inversion-lam x
                            in  a , b , c , d , trans (sym x₁) e

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
------------------------------------------------------------------------------
-- Totality properties for Tree
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Tree.TotalityATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Forest.TotalityATP
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Type

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

mirror-Tree : ∀ {t} → Tree t → Tree (mirror · t)
mirror-Tree = Tree-mutual-ind {A} {B} hA B[] hB
  where
  A : D → Set
  A t = Tree (mirror · t)
  {-# ATP definition A #-}

  B : D → Set
  B ts = Forest (map mirror ts)
  {-# ATP definition B #-}

  postulate
    hA  : ∀ d {ts} → Forest ts → B ts → A (node d ts)
    B[] : B []
    hB  : ∀ {t ts} → Tree t → A t → Forest ts → B ts → B (t ∷ ts)
  {-# ATP prove hA reverse-Forest #-}
  {-# ATP prove B[] #-}
  {-# ATP prove hB #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- A universe for stream programs
------------------------------------------------------------------------

module Stream.Programs where

open import Codata.Musical.Notation renaming (∞ to ∞_)
import Stream as S
open S using (Stream; _≈_; _≺_; head; tail)
open import Relation.Binary.PropositionalEquality
open import Data.Vec using (Vec; []; _∷_)

------------------------------------------------------------------------
-- Stream programs

infix  8 _∞
infixr 7 _·_
infix  6 _⟨_⟩_
infixr 5 _≺_ _⋎_ _≺≺_

data Prog (A : Set) : Set1 where
  _≺_     : (x : A) (xs : ∞ (Prog A)) → Prog A
  _∞      : (x : A) → Prog A
  _·_     : ∀ {B} (f : B → A) (xs : Prog B) → Prog A
  _⟨_⟩_   : ∀ {B C} (xs : Prog B) (_∙_ : B → C → A) (ys : Prog C) →
            Prog A
  _⋎_     : (xs ys : Prog A) → Prog A
  iterate : (f : A → A) (x : A) → Prog A
  _≺≺_    : ∀ {n} (xs : Vec A n) (ys : Prog A) → Prog A

data WHNF A : Set1 where
  _≺_ : (x : A) (xs : Prog A) → WHNF A

------------------------------------------------------------------------
-- Conversion

whnf : ∀ {A} → Prog A → WHNF A
whnf (x ≺ xs)         = x ≺ ♭ xs
whnf (x ∞)            = x ≺ x ∞
whnf (f · xs)         with whnf xs
whnf (f · xs)         | x ≺ xs′ = f x ≺ f · xs′
whnf (xs ⟨ _∙_ ⟩ ys)  with whnf xs | whnf ys
whnf (xs ⟨ _∙_ ⟩ ys)  | x ≺ xs′ | y ≺ ys′ = (x ∙ y) ≺ xs′ ⟨ _∙_ ⟩ ys′
whnf (xs ⋎ ys)        with whnf xs
whnf (xs ⋎ ys)        | x ≺ xs′ = x ≺ ys ⋎ xs′
whnf (iterate f x)    = x ≺ iterate f (f x)
whnf ([]       ≺≺ ys) = whnf ys
whnf ((x ∷ xs) ≺≺ ys) = x ≺ xs ≺≺ ys

mutual

  value : ∀ {A} → WHNF A → Stream A
  value (x ≺ xs) = x ≺ ♯ ⟦ xs ⟧

  ⟦_⟧ : ∀ {A} → Prog A → Stream A
  ⟦ xs ⟧ = value (whnf xs)

fromStream : ∀ {A} → Stream A → Prog A
fromStream (x ≺ xs) = x ≺ ♯ fromStream (♭ xs)

lift : ∀ {A} → (Prog A → Prog A) → Stream A → Stream A
lift f xs = ⟦ f (fromStream xs) ⟧

------------------------------------------------------------------------
-- Some abbreviations

infixr 5 _≺♯_

_≺♯_ : ∀ {A} → A → Prog A → Prog A
x ≺♯ xs = x ≺ ♯ xs

headP : ∀ {A} → Prog A → A
headP xs = head ⟦ xs ⟧

tailP : ∀ {A} → Prog A → Prog A
tailP xs with whnf xs
tailP xs | x ≺ xs′ = xs′

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{- Examples by Twan van Laarhoven -}

{-# OPTIONS --rewriting #-}
module _ where

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x _ = x

_∘_ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c}
    → (f : ∀ {x} (y : B x) → C y) (g : (x : A) → B x)
    → (x : A) → C (g x)
(f ∘ g) x = f (g x)

postulate M : Set → Set
postulate pure : ∀ {A} → A → M A
postulate _>>=_ : ∀ {A B} → M A → (A → M B) → M B
postulate bind-assoc : ∀ {A B C mx} {my : A → M B} {mz : B → M C} → (mx >>= my) >>= mz  ≡  mx >>= \x → my x >>= mz
{-# REWRITE bind-assoc #-}

_<*>_ : ∀ {A B} → M (A → B) → M A → M B
mf <*> mx = mf >>= \f → mx >>= (pure ∘ f)

-- Agda was comparing inferred relevances here, causing the rewrite rule
-- to fail.
shouldWork : ∀ {A B} (mx : M A) (my : M B)
  → (mx >>= (pure ∘ const)) <*> my
  ≡ (mx >>= (pure ∘ const)) >>= (\f → my >>= (pure ∘ f))
shouldWork mx my = refl

shouldAlsoWork  : ∀ {A B} (mx : M A) (my : M B)
  → (mx >>= (pure ∘ const)) <*> my
  ≡ (mx >>= (pure ∘ \x _ → x)) >>= (\f → my >>= (pure ∘ f))
shouldAlsoWork mx my = refl

shouldAlsoWork2  : ∀ {A B} (mx : M A) (my : M B)
  → (mx >>= (pure ∘ const)) >>= (\f → my >>= (pure ∘ f))
  ≡ (mx >>= (pure ∘ \x _ → x)) >>= (\f → my >>= (pure ∘ f))
shouldAlsoWork2 mx my = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

open import HoTT
open import homotopy.PtdAdjoint

module homotopy.SuspAdjointLoopLadder where

  import homotopy.SuspAdjointLoop as A

  step : ∀ {i} {X Y Z : Ptd i} (f : Y ⊙→ Z)
    → CommSquareEquiv
        ((f ⊙∘_) :> ((⊙Susp X ⊙→ Y) → (⊙Susp X ⊙→ Z)))
        (⊙Ω-fmap f ⊙∘_)
        (–> (A.eq X Y))
        (–> (A.eq X Z))
  step f = comm-sqr (! ∘ A.nat-cod _ f) ,
    snd (A.eq _ _) , snd (A.eq _ _)

  rail : ∀ {i} {X Y : Ptd i} n
    → (⊙Susp^ n X ⊙→ Y) → (X ⊙→ ⊙Ω^' n Y)
  rail O = idf _
  rail (S n) = rail n ∘ –> (A.eq _ _)

  ladder : ∀ {i} {X Y Z : Ptd i} n (f : Y ⊙→ Z)
    → CommSquareEquiv
        ((f ⊙∘_) :> ((⊙Susp^ n X ⊙→ Y) → (⊙Susp^ n X ⊙→ Z)))
        (⊙Ω^'-fmap n f ⊙∘_)
        (rail n)
        (rail n)
  ladder O _ = (comm-sqr λ _ → idp) , idf-is-equiv _ , idf-is-equiv _
  ladder (S n) f = CommSquareEquiv-∘v (ladder n (⊙Ω-fmap f)) (step f)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Agda.Primitive
open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.CwF-structure
open import GSeTT.Uniqueness-Derivations

{- Typed syntax for type theory for globular sets -}
module GSeTT.Typed-Syntax where
  Ctx : Set₁
  Ctx = Σ Pre-Ctx (λ Γ → Γ ⊢C)

  Ty : Ctx → Set₁
  Ty (Γ , _) = Σ Pre-Ty (λ A → Γ ⊢T A)

  Tm : ∀ (Γ : Ctx) → Ty Γ → Set₁
  Tm (Γ , _) (A , _) = Σ Pre-Tm (λ t → Γ ⊢t t # A)

  Sub : ∀ (Δ : Ctx) (Γ : Ctx) → Set₁
  Sub (Δ , _) (Γ , _) = Σ Pre-Sub (λ γ → Δ ⊢S γ > Γ)

  eqC : ∀ (Γ Δ : Ctx) → fst Γ == fst Δ → Γ == Δ
  eqC (Γ , Γ⊢) (.Γ , Γ⊢') idp = Σ= idp (has-all-paths-⊢C _ _)

  eqT : ∀ {Γ} (A B : Ty Γ) → fst A == fst B → A == B
  eqT (A , Γ⊢A) (.A , Γ⊢'A) idp = Σ= idp (has-all-paths-⊢T _ _)

  eqt : ∀ {Γ A} (t u : Tm Γ A) → fst t == fst u → t == u
  eqt (t , Γ⊢t:A) (.t , Γ⊢':A) idp = Σ= idp (has-all-paths-⊢t _ _)

  eqS : ∀ {Γ Δ} (γ δ : Sub Γ Δ) → fst γ == fst δ → γ == δ
  eqS (γ , Γ⊢γ:Δ) (.γ , Γ⊢'γ:Δ) idp = Σ= idp (has-all-paths-⊢S _ _)

  trS : ∀ {Γ Δ Θ : Ctx} → (p : Δ == Θ) → {γ : Sub Γ Δ} → {δ : Sub Γ Θ} → fst γ == fst δ → transport p γ == δ
  trS {Γ} {Δ} {Θ} idp {γ} {δ} x = eqS {Γ} {Θ} γ δ x

  eqdec-Ty : ∀ Γ → eqdec (Ty Γ)
  eqdec-Ty Γ (A , Γ⊢A) (B , Γ⊢B) with eqdec-PreTy A B
  ... | inl idp = inl (eqT {Γ} (A , Γ⊢A) (B , Γ⊢B) idp)
  ... | inr A≠B = inr λ p → A≠B (fst-is-inj p)

  is-set-Ty : ∀ Γ → is-set (Ty Γ)
  is-set-Ty Γ = eqdec-is-set (eqdec-Ty Γ)

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


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

module Issue15 where

infix  7 _≡_
infixr 5 _∧_
infix  5 ∃
infixr 4 _∨_

data _∨_ (A B : Set) : Set where
  inj₁ : A → A ∨ B
  inj₂ : B → A ∨ B

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

postulate
  D    : Set
  _·_  : D → D → D
  succ : D → D
  zero : D

data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

syntax ∃ (λ x → e) = ∃[ x ] e

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

postulate Conat : D → Set

postulate
  Conat-out : ∀ {n} → Conat n → n ≡ zero ∨ (∃[ n' ] n ≡ succ n' ∧ Conat n')
{-# ATP axiom Conat-out #-}

postulate
  Conat-coind :
    (A : D → Set) →
    -- A is post-fixed point of NatF.
    (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ n' ∧ A n')) →
    -- Conat is greater than A.
    ∀ {n} → A n → Conat n

-- See Issue #81.
A : D → Set
A n = n ≡ zero ∨ (∃[ n' ] n ≡ succ n' ∧ Conat n')
{-# ATP definition A #-}

Conat-in : ∀ {n} →
           n ≡ zero ∨ (∃[ n' ] n ≡ succ n' ∧ Conat n') →
           Conat n
Conat-in h = Conat-coind A h' h
  where
  postulate h' : ∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ n' ∧ A n')
  {-# ATP prove h' #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia