text:
module Ints.Add.Assoc where

open import Ints
open import Nats renaming (suc to nsuc; _+_ to _:+:_)

open import Nats.Add.Assoc
open import Nats.Add.Comm

open import Ints.Add.Comm

open import Equality
open import Function

------------------------------------------------------------------------
-- internal stuffs

private

  0+a=a : ∀ a → + 0 + a ≡ a
  0+a=a (+    n  ) = refl
  0+a=a (-[1+ n ]) = refl

  a+0=a : ∀ a → a + + 0 ≡ a
  a+0=a a rewrite int-add-comm a (+ 0) | 0+a=a a = refl

  z+/b+c/=/z+b/+c : ∀ b c → + 0 + (b + c) ≡ (+ 0 + b) + c
  z+/b+c/=/z+b/+c (+    a  ) (+    b  ) = refl
  z+/b+c/=/z+b/+c (-[1+ a ]) (-[1+ b ]) = refl
  z+/b+c/=/z+b/+c (+    a  ) (-[1+ b ])
    rewrite 0+a=a (a ⊖ nsuc b) = refl
  z+/b+c/=/z+b/+c (-[1+ a ]) (+    b  )
    rewrite 0+a=a (b ⊖ nsuc a) = refl

  a+b=a--b : ∀ a b → a + b ≡ a - (- b)
  a+b=a--b a (+ zero  ) = refl
  a+b=a--b a (+ nsuc n)
    rewrite a+b=a--b a (+ n) = refl
  a+b=a--b a (-[1+ n ]) = refl

  a-b+c=a+c-b : ∀ a b c → a ⊖ b + + c ≡ a :+: c ⊖ b
  a-b+c=a+c-b zero  zero    _ = refl
  a-b+c=a+c-b zero (nsuc _) _ = refl
  a-b+c=a+c-b (nsuc _) zero _ = refl
  a-b+c=a+c-b (nsuc a) (nsuc b) c = a-b+c=a+c-b a b c

  a+/b-c/=a+b-c : ∀ a b c → + a + (b ⊖ c) ≡ a :+: b ⊖ c
  a+/b-c/=a+b-c a b c
    rewrite int-add-comm (+ a) $ b ⊖ c
          | a-b+c=a+c-b b c a
          | nat-add-comm a b
            = refl

  b-c-a=b-/c+a/ : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (nsuc c :+: a)
  b-c-a=b-/c+a/ _ zero    zero    = refl
  b-c-a=b-/c+a/ _ zero    (nsuc _) = refl
  b-c-a=b-/c+a/ _ (nsuc _) zero    = refl
  b-c-a=b-/c+a/ a (nsuc b) (nsuc c) = b-c-a=b-/c+a/ a b c

  -a+/b-c/=b-/a+c/ : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (nsuc a :+: c)
  -a+/b-c/=b-/a+c/ a b c
    rewrite int-add-comm -[1+ a ] $ b ⊖ c
          | b-c-a=b-/c+a/ a b c
          | nat-add-comm a c
            = refl

  a+/b+c/=/a+b/+c : ∀ a b c → a + (b + c) ≡ a + b + c
  a+/b+c/=/a+b/+c (+ zero) b c rewrite 0+a=a (b + c) | 0+a=a b = refl
  a+/b+c/=/a+b/+c a (+ zero) c rewrite 0+a=a c | a+0=a a = refl
  a+/b+c/=/a+b/+c a b (+ zero) rewrite a+0=a b | a+0=a (a + b) = refl
  a+/b+c/=/a+b/+c (+ a) (+ b) (+ c)
    rewrite nat-add-assoc a b c = refl
  a+/b+c/=/a+b/+c -[1+ a ] -[1+ b ] (+ nsuc c)
    rewrite -a+/b-c/=b-/a+c/ a c b = refl
  a+/b+c/=/a+b/+c -[1+ a ] (+ nsuc b) -[1+ c ]
    rewrite -a+/b-c/=b-/a+c/ a b c
          | b-c-a=b-/c+a/ c b a
            = refl
  a+/b+c/=/a+b/+c (+ nsuc a) -[1+ b ] -[1+ c ]
    rewrite b-c-a=b-/c+a/ c a b = refl
  a+/b+c/=/a+b/+c (+ nsuc a) -[1+ b ] (+ nsuc c)
    rewrite a-b+c=a+c-b a b $ nsuc c
          | a+/b-c/=a+b-c (nsuc a) c b
          | sym $ nat-add-assoc a 1 c
          | nat-add-comm a 1
            = refl
  a+/b+c/=/a+b/+c -[1+ a ] (+ nsuc b) (+ nsuc c)
    rewrite a-b+c=a+c-b b a (nsuc c) = refl
  a+/b+c/=/a+b/+c -[1+ a ] -[1+ b ] -[1+ c ]
    rewrite nat-add-comm a $ nsuc $ b :+: c
          | nat-add-comm (b :+: c) a
          | nat-add-assoc a b c
            = refl
  a+/b+c/=/a+b/+c (+ nsuc a) (+ nsuc b) -[1+ c ]
    rewrite a+/b-c/=a+b-c (nsuc a) b c
          | sym $ nat-add-assoc a 1 b
          | nat-add-comm a 1
            = refl

------------------------------------------------------------------------
-- public aliases

int-add-assoc : ∀ a b c → a + (b + c) ≡ a + b + c
int-add-assoc = a+/b+c/=/a+b/+c


text:
mutual
  data D : Set where
    c : R → D

  record R : Set where
    inductive
    field
      out : D
open R

f : D → {A : Set} → A
f (c x) = f (out x)
-- should termination check

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-

  Functions building DUARels on constant families

-}
{-# OPTIONS --safe #-}
module Cubical.Displayed.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Displayed.Base
open import Cubical.Displayed.Subst

private
  variable
    ℓ ℓA ℓA' ℓP ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓ≅B' ℓC ℓ≅C : Level

-- constant DUARel

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A)
  {B : Type ℓB} (𝒮-B : UARel B ℓ≅B)  where

  open UARel 𝒮-B
  open DUARel

  𝒮ᴰ-const : DUARel 𝒮-A (λ _ → B) ℓ≅B
  𝒮ᴰ-const ._≅ᴰ⟨_⟩_ b _ b' = b ≅ b'
  𝒮ᴰ-const .uaᴰ b p b' = ua b b'

-- SubstRel for an arbitrary constant family

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : Type ℓB) where

  open SubstRel

  𝒮ˢ-const : SubstRel 𝒮-A (λ _ → B)
  𝒮ˢ-const .SubstRel.act _ = idEquiv B
  𝒮ˢ-const .SubstRel.uaˢ p b = transportRefl b

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{-# OPTIONS --without-K #-}
module sets.finite where

open import sets.finite.core public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- A Typed version of a subset of Landin's ISWIM from "The Next 700 Programming
-- Languages"

module ISWIM where

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

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}
{-# BUILTIN NATPLUS _+_  #-}

data Bool : Set where
  true  : Bool
  false : Bool

module Syntax where

  infixl 100 _∙_
  infixl 80 _WHERE_ _PP_
  infixr 60 _─→_
  infixl 40 _,_

  data Type : Set where
    nat  : Type
    bool : Type
    _─→_ : Type -> Type -> Type

  data Context : Set where
    ε   : Context
    _,_ : Context -> Type -> Context

  data Var : Context -> Type -> Set where
    vz : {Γ : Context}{τ : Type}            -> Var (Γ , τ) τ
    vs : {Γ : Context}{σ τ : Type} -> Var Γ τ -> Var (Γ , σ) τ

  data Expr (Γ : Context) : Type -> Set where
    var   : {τ : Type} -> Var Γ τ -> Expr Γ τ
    litNat  : Nat -> Expr Γ nat
    litBool : Bool -> Expr Γ bool
    plus    : Expr Γ (nat ─→ nat ─→ nat)
    if      : {τ : Type} -> Expr Γ (bool ─→ τ ─→ τ ─→ τ)
    _∙_           : {σ τ : Type} -> Expr Γ (σ ─→ τ) -> Expr Γ σ -> Expr Γ τ
    _WHERE_ : {σ τ ρ : Type} -> Expr (Γ , σ ─→ τ) ρ -> Expr (Γ , σ) τ -> Expr Γ ρ
    _PP_    : {σ τ ρ : Type} -> Expr (Γ , σ ─→ τ) ρ -> Expr (Γ , σ) ρ -> Expr Γ ρ

  -- ƛ x. e = f where f x = e
  ƛ : {Γ : Context}{σ τ : Type} -> Expr (Γ , σ) τ -> Expr Γ (σ ─→ τ)
  ƛ e = var vz WHERE e

module Cont (R : Set) where

  C : Set -> Set
  C a = (a -> R) -> R

  callcc : {a : Set} -> (({b : Set} -> a -> C b) -> C a) -> C a
  callcc {a} g = \k -> g (\x _ -> k x) k

  return : {a : Set} -> a -> C a
  return x = \k -> k x

  infixr 10 _>>=_

  _>>=_ : {a b : Set} -> C a -> (a -> C b) -> C b
  (m >>= k) ret = m \x -> k x ret

module Semantics (R : Set) where

  open module C = Cont R
  open Syntax

  infix 60 _!_
  infixl 40 _||_

  ⟦_⟧type : Type -> Set

  ⟦_⟧type' : Type -> Set
  ⟦ nat    ⟧type' = Nat
  ⟦ bool   ⟧type' = Bool
  ⟦ σ ─→ τ ⟧type' = ⟦ σ ⟧type' -> ⟦ τ ⟧type

  ⟦ τ ⟧type = C ⟦ τ ⟧type'

  data ⟦_⟧ctx : Context -> Set where
    ★    : ⟦ ε ⟧ctx
    _||_ : {Γ : Context}{τ : Type} -> ⟦ Γ ⟧ctx -> ⟦ τ ⟧type' -> ⟦ Γ , τ ⟧ctx

  _!_ : {Γ : Context}{τ : Type} -> ⟦ Γ ⟧ctx -> Var Γ τ -> ⟦ τ ⟧type'
  ★      ! ()
  (ρ || v) ! vz   = v
  (ρ || v) ! vs x = ρ ! x

  ⟦_⟧ : {Γ : Context}{τ : Type} -> Expr Γ τ -> ⟦ Γ ⟧ctx -> ⟦ τ ⟧type
  ⟦ var x   ⟧ ρ = return (ρ ! x)
  ⟦ litNat n        ⟧ ρ = return n
  ⟦ litBool b       ⟧ ρ = return b
  ⟦ plus    ⟧ ρ = return \n -> return \m -> return (n + m)
  ⟦ f ∙ e ⟧ ρ = ⟦ e ⟧ ρ >>= \v ->
                    ⟦ f ⟧ ρ >>= \w ->
                    w v
  ⟦ e WHERE f ⟧ ρ = ⟦ e ⟧ (ρ || (\x -> ⟦ f ⟧ (ρ || x)))
  ⟦ e PP f  ⟧ ρ = callcc \k ->
                    let throw = \x -> ⟦ f ⟧ (ρ || x) >>= k
                    in  ⟦ e ⟧ (ρ || throw)
  ⟦ if        ⟧ ρ = return \x -> return \y -> return \z -> return (iff x y z)
    where
      iff : {A : Set} -> Bool -> A -> A -> A
      iff true  x y = x
      iff false x y = y

module Test where

  open Syntax
  open module C = Cont Nat
  open module S = Semantics Nat

  run : Expr ε nat -> Nat
  run e = ⟦ e ⟧ ★ \x -> x

  -- 1 + 1
  two : Expr ε nat
  two = plus ∙ litNat 1 ∙ litNat 1

  -- f 1 + f 2 where f x = x
  three : Expr ε nat
  three = plus ∙ (var vz ∙ litNat 1) ∙ (var vz ∙ litNat 2) WHERE var vz

  -- 1 + f 1 where pp f x = x
  one : Expr ε nat
  one = plus ∙ litNat 1 ∙ (var vz ∙ litNat 1) PP var vz

open Test

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

twoOK : run two == 2
twoOK = refl

threeOK : run three == 3
threeOK = refl

oneOK : run one == 1
oneOK = refl

open Cont
open Syntax
open Semantics

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
postulate
  P : {A : Set} → A → A → Set
  p : {A : Set} {x : A} → P x x
  q : {A : Set} (x : A) {y : A} → P x y → P x y
  A : Set

record R (F : Set → Set) : Set₁ where
  field
    f₁ : (A → A) → F A → F A
    f₂ : P (f₁ (λ x → x)) (λ (x : F A) → x)

open R ⦃ … ⦄ public

instance

  r : R (λ O → O → O)
  r = record
    { f₁ = λ f g x → f (g x)
    ; f₂ = p
    }

postulate
  F : Set → Set

  instance
    rF : R F

Foo : P (f₁ (λ x → x)) (λ (x : F A) → x)
Foo = q (f₁ (λ x → x)) f₂

-- An internal error has occurred. Please report this as a bug.
-- Location of the error:
-- src/full/Agda/TypeChecking/InstanceArguments.hs:224


text:
{-

  Reflection-based tools for converting between iterated record types, particularly between
  record types and iterated Σ-types.

  See end of file for examples.

-}
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Reflection.RecordEquiv where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.List as List
open import Cubical.Data.Nat
open import Cubical.Data.Maybe as Maybe
open import Cubical.Data.Sigma

open import Agda.Builtin.String
import Agda.Builtin.Reflection as R
open import Cubical.Reflection.Base

Projections = Maybe (List R.Name)

-- Describes a correspondence between two iterated record types
RecordAssoc = List (Projections × Projections)

-- Describes a correspondence between a record type and an iterated Σ-types;
-- more convenient than RecordAssoc for this special case
data ΣFormat : Type where
  leaf : R.Name → ΣFormat
  _,_ : ΣFormat → ΣFormat → ΣFormat
  unit : ΣFormat

infixr 4 _,_

flipRecordAssoc : RecordAssoc → RecordAssoc
flipRecordAssoc = List.map λ {p .fst → p .snd; p .snd → p .fst}

fstIdRecordAssoc : RecordAssoc → RecordAssoc
fstIdRecordAssoc = List.map λ {p .fst → p .fst; p .snd → p .fst}

List→ΣFormat : List R.Name → ΣFormat
List→ΣFormat [] = unit
List→ΣFormat (x ∷ []) = leaf x
List→ΣFormat (x ∷ y ∷ xs) = leaf x , List→ΣFormat (y ∷ xs)

ΣFormat→RecordAssoc : ΣFormat → RecordAssoc
ΣFormat→RecordAssoc = go []
  where
  go : List R.Name → ΣFormat → RecordAssoc
  go prefix unit = [ just prefix , nothing ]
  go prefix (leaf fieldName) = [ just prefix , just [ fieldName ] ]
  go prefix (sig₁ , sig₂) =
    go (quote fst ∷ prefix) sig₁ ++ go (quote snd ∷ prefix) sig₂

-- Derive the shape of the compound Σ-type
ΣFormat→Ty : ΣFormat → R.Type
ΣFormat→Ty unit = R.def (quote Unit) []
ΣFormat→Ty (leaf _) = R.unknown
ΣFormat→Ty (sig₁ , sig₂) =
  R.def (quote Σ) (ΣFormat→Ty sig₁ v∷ R.lam R.visible (R.abs "_" (ΣFormat→Ty sig₂)) v∷ [])

recordName→isoTy : R.Name → R.Term → R.TC R.Term
recordName→isoTy name σShape =
  R.inferType (R.def name []) >>= R.normalise >>= go []
  where
  go : List R.ArgInfo → R.Type → R.TC R.Term
  go acc (R.pi (R.arg i argTy) (R.abs s ty)) =
    liftTC (λ t → R.pi (R.arg i' argTy) (R.abs s t)) (go (i ∷ acc) ty)
    where
    i' = R.arg-info R.hidden (R.modality R.relevant R.quantity-ω)
  go acc (R.agda-sort _) =
    R.returnTC (R.def (quote Iso) (R.def name (makeArgs 0 [] acc) v∷ σShape v∷ []))
    where
    makeArgs : ℕ → List (R.Arg R.Term) → List R.ArgInfo → List (R.Arg R.Term)
    makeArgs n acc [] = acc
    makeArgs n acc (i ∷ infos) = makeArgs (suc n) (R.arg i (v n) ∷ acc) infos
  go _ _ = R.typeError (R.strErr "Not a record type name: " ∷ R.nameErr name ∷ [])

projNames→Patterns : List R.Name → List (R.Arg R.Pattern)
projNames→Patterns = go []
  where
  go : List (R.Arg R.Pattern) → List R.Name → List (R.Arg R.Pattern)
  go acc [] = acc
  go acc (π ∷ projs) = go (varg (R.proj π) ∷ acc) projs

projNames→Term : R.Term → List R.Name → R.Term
projNames→Term term [] = term
projNames→Term term (π ∷ projs) = R.def π [ varg (projNames→Term term projs) ]

convertClauses : RecordAssoc → R.Term → List R.Clause
convertClauses al term = fixIfEmpty (List.filterMap makeClause al)
  where
  makeClause : Projections × Projections → Maybe R.Clause
  makeClause (projl , just projr) =
    just (R.clause [] (goPat [] projr) (Maybe.rec R.unknown goTm projl))
    where
    goPat : List (R.Arg R.Pattern) → List R.Name → List (R.Arg R.Pattern)
    goPat acc [] = acc
    goPat acc (π ∷ projs) = goPat (varg (R.proj π) ∷ acc) projs

    goTm : List R.Name → R.Term
    goTm [] = term
    goTm (π ∷ projs) = R.def π [ varg (goTm projs) ]
  makeClause (_ , nothing) = nothing

  fixIfEmpty : List R.Clause → List R.Clause
  fixIfEmpty [] = [ R.clause [] [] R.unknown ]
  fixIfEmpty (c ∷ cs) = c ∷ cs

mapClause :
  (List (String × R.Arg R.Type) → List (String × R.Arg R.Type))
  → (List (R.Arg R.Pattern) → List (R.Arg R.Pattern))
  → (R.Clause → R.Clause)
mapClause f g (R.clause tel ps t) = R.clause (f tel) (g ps) t
mapClause f g (R.absurd-clause tel ps) = R.absurd-clause (f tel) (g ps)

recordIsoΣClauses : ΣFormat → List R.Clause
recordIsoΣClauses σ =
  funClauses (quote Iso.fun) Σ↔R ++
  funClauses (quote Iso.inv) R↔Σ ++
  pathClauses (quote Iso.rightInv) R↔Σ ++
  pathClauses (quote Iso.leftInv) Σ↔R
  where
  R↔Σ = ΣFormat→RecordAssoc σ
  Σ↔R = flipRecordAssoc R↔Σ

  funClauses : R.Name → RecordAssoc → List R.Clause
  funClauses name al =
    List.map
      (mapClause
        (("_" , varg R.unknown) ∷_)
        (λ ps → R.proj name v∷ R.var 0 v∷ ps))
      (convertClauses al (v 0))

  pathClauses : R.Name → RecordAssoc → List R.Clause
  pathClauses name al =
    List.map
      (mapClause
        (λ vs → ("_" , varg R.unknown) ∷ ("_" , varg R.unknown) ∷ vs)
        (λ ps → R.proj name v∷ R.var 1 v∷ R.var 0 v∷ ps))
      (convertClauses (fstIdRecordAssoc al) (v 1))

recordIsoΣTerm : ΣFormat → R.Term
recordIsoΣTerm σ = R.pat-lam (recordIsoΣClauses σ) []

-- with a provided ΣFormat for the record
declareRecordIsoΣ' : R.Name → ΣFormat → R.Name → R.TC Unit
declareRecordIsoΣ' idName σ recordName =
  let σTy = ΣFormat→Ty σ in
  recordName→isoTy recordName σTy >>= λ isoTy →
  R.declareDef (varg idName) isoTy >>
  R.defineFun idName (recordIsoΣClauses σ)

-- using the right-associated Σ given by the record fields
declareRecordIsoΣ : R.Name → R.Name → R.TC Unit
declareRecordIsoΣ idName recordName =
  R.getDefinition recordName >>= λ where
  (R.record-type _ fs) →
    let σ = List→ΣFormat (List.map (λ {(R.arg _ n) → n}) fs) in
    declareRecordIsoΣ' idName σ recordName
  _ →
    R.typeError (R.strErr "Not a record type name:" ∷ R.nameErr recordName ∷ [])

private
  module Example where
    variable
      ℓ ℓ' : Level
      A : Type ℓ
      B : A → Type ℓ'

    record Example0 {A : Type ℓ} (B : A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
      no-eta-equality -- works with or without eta equality
      field
        cool : A
        fun : A
        wow : B cool

    -- Declares a function `Example0IsoΣ` that gives an isomorphism between the record type and a
    -- right-associated nested Σ-type (with the parameters to Example0 as implict arguments).
    unquoteDecl Example0IsoΣ = declareRecordIsoΣ Example0IsoΣ (quote Example0)

    -- `Example0IsoΣ` has the type we expect
    test0 : Iso (Example0 B) (Σ[ a ∈ A ] (Σ[ _ ∈ A ] B a))
    test0 = Example0IsoΣ

    -- A record with no fields is isomorphic to Unit

    record Example1 : Type where

    unquoteDecl Example1IsoΣ = declareRecordIsoΣ Example1IsoΣ (quote Example1)

    test1 : Iso Example1 Unit
    test1 = Example1IsoΣ


text:
module Oscar.Builtin.Nat where

open import Agda.Builtin.Nat public
  using ()
  renaming (Nat to ℕ; zero to ∅; suc to ↑_)


text:
--
-- Created by Dependently-Typed Lambda Calculus on 2020-10-07
-- Isomorphism
-- Author: dplaindoux
--

{-# OPTIONS --without-K --no-sized-types --no-guardedness bbbbb#-}

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

module Isomorphism where

_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f) = λ x → g (f x)

-- Extensionality and function equivalence

_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m n rewrite +-comm m n = helper m n
  where
  helper : ∀ (m n : ℕ) → m +′ n ≡ n + m
  helper m zero    = refl
  helper m (suc n) = cong suc (helper m n)

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

postulate
  ∀-extensionality : ∀ {A : Set} {B : A → Set} {f g : ∀(x : A) → B x}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

same : _+′_ ≡ _+_
same = ∀-extensionality (λ m → ∀-extensionality (λ n → same-app m n))

-- Isomorphism definition

infix 0 _≃_

record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y

open _≃_

≃-refl : ∀ {A : Set}
    -----
  → A ≃ A
≃-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    ; to∘from = λ{y → refl}
    }

≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A
≃-sym A≃B =
  record
    { to      = from A≃B
    ; from    = to   A≃B
    ; from∘to = to∘from A≃B
    ; to∘from = from∘to A≃B
    }

≃-trans : ∀ {A B C : Set}
  → A ≃ B
  → B ≃ C
    -----
  → A ≃ C
≃-trans A≃B B≃C =
  record
    { to       = to   B≃C ∘ to   A≃B
    ; from     = from A≃B ∘ from B≃C
    ; from∘to  = λ{x →
        begin
          ((from A≃B ∘ from B≃C) ∘ (to B≃C ∘ to A≃B)) x
        ≡⟨⟩
          (from A≃B ∘ from B≃C) ((to B≃C ∘ to A≃B) x)
        ≡⟨⟩
          from A≃B (from B≃C (to B≃C (to A≃B x)))
        ≡⟨ cong (from A≃B) (from∘to B≃C (to A≃B x)) ⟩
          from A≃B (to A≃B x)
        ≡⟨ from∘to A≃B x ⟩
          x
        ∎}
    ; to∘from = λ{y →
        begin
          ((to B≃C ∘ to A≃B) ∘ (from A≃B ∘ from B≃C)) y
        ≡⟨⟩
          (to B≃C ∘ to A≃B) ((from A≃B ∘ from B≃C) y)
        ≡⟨⟩
          to B≃C (to A≃B (from A≃B (from B≃C y)))
        ≡⟨ cong (to B≃C) (to∘from A≃B (from B≃C y)) ⟩
          to B≃C (from B≃C y)
        ≡⟨ to∘from B≃C y ⟩
          y
        ∎}
     }

module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    → B ≃ C
      -----
    → A ≃ C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

infix 0 _≲_

record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x

open _≲_

≲-refl : ∀ {A : Set}
    -----
  → A ≲ A
≲-refl =
  record
    { to      = λ{x → x}
    ; from    = λ{y → y}
    ; from∘to = λ{x → refl}
    }

≲-trans : ∀ {A B C : Set}
  → A ≲ B
  → B ≲ C
    -----
  → A ≲ C
≲-trans A≲B B≲C =
  record
    { to      = λ{x → to   B≲C (to   A≲B x)}
    ; from    = λ{y → from A≲B (from B≲C y)}
    ; from∘to = λ{x →
        begin
          ((from A≲B ∘ from B≲C) ∘ (to B≲C ∘ to A≲B)) x
        ≡⟨⟩
          (from A≲B ∘ from B≲C) ((to B≲C ∘ to A≲B) x)
        ≡⟨⟩
          from A≲B (from B≲C (to B≲C (to A≲B x)))
        ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B x)) ⟩
          from A≲B (to A≲B x)
        ≡⟨ from∘to A≲B x ⟩
          x
        ∎}
     }

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to A≲B ≡ from B≲A)
  → (from A≲B ≡ to B≲A)
    -------------------
  → A ≃ B
≲-antisym A≲B B≲A to≡from from≡to =
  record
    { to      = to A≲B
    ; from    = from A≲B
    ; from∘to = from∘to A≲B
    ; to∘from = λ{y →
        begin
          (to A≲B ∘ from A≲B) y
        ≡⟨⟩
          to A≲B (from A≲B y)
        ≡⟨ cong (to A≲B) (cong-app from≡to y) ⟩
          to A≲B (to B≲A y)
        ≡⟨ cong-app to≡from (to B≲A y) ⟩
          from B≲A (to B≲A y)
        ≡⟨ from∘to B≲A y ⟩
          y
        ∎}
    }

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
------------------------------------------------------------------------------
-- Logical Theory of Constructions for PCF (LTC-PCF)
------------------------------------------------------------------------------

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

-- Code accompanying the paper "Embedding a Logical Theory of
-- Constructions in Agda" by Ana Bove, Peter Dybjer and Andrés
-- Sicard-Ramírez (PLPV'09).

-- The code presented here does not match the paper exactly.

module LTC-PCF.README where

------------------------------------------------------------------------------
-- Description

-- Formalization of (a version of) Azcel's Logical Theory of
-- Constructions for PCF.

------------------------------------------------------------------------------
-- The axioms
open import LTC-PCF.Base

-- Properties
open import LTC-PCF.Base.Properties

------------------------------------------------------------------------------
-- Booleans

-- The inductive predicate
open import LTC-PCF.Data.Bool.Type

-- Properties
open import LTC-PCF.Data.Bool.Properties

------------------------------------------------------------------------------
-- Natural numberes

-- The arithmetical functions
open import LTC-PCF.Data.Nat

-- The inductive predicate
open import LTC-PCF.Data.Nat.Type

-- Properties
open import LTC-PCF.Data.Nat.Properties

-- Divisibility relation
open import LTC-PCF.Data.Nat.Divisibility.NotBy0.Properties

-- Induction
open import LTC-PCF.Data.Nat.Induction.NonAcc.Lexicographic
open import LTC-PCF.Data.Nat.Induction.NonAcc.WF

-- Inequalites
open import LTC-PCF.Data.Nat.Inequalities.EliminationProperties
open import LTC-PCF.Data.Nat.Inequalities.Properties

-- The recursive operator
open import LTC-PCF.Data.Nat.Rec.ConversionRules

------------------------------------------------------------------------------
-- A looping combinator
open import LTC-PCF.Loop

------------------------------------------------------------------------------
-- Verification of programs

-- The division algorithm: A non-structurally recursive algorithm
open import LTC-PCF.Program.Division.CorrectnessProof

-- The GCD algorithm: A non-structurally recursive algorithm
open import LTC-PCF.Program.GCD.Partial.CorrectnessProof
open import LTC-PCF.Program.GCD.Total.CorrectnessProof

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Categories.Category
open import Categories.Functor.Bifunctor

module Categories.Diagram.Coend {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  variable
    A B : Obj
    f g : A ⇒ B

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

open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural
open import Categories.Morphism.Reasoning D

open Functor F

record Cowedge : Set (levelOfTerm F) where
  field
    E         : Obj
    dinatural : DinaturalTransformation F (const E)

  module dinatural = DinaturalTransformation dinatural

Cowedge-∘ : (W : Cowedge) → Cowedge.E W ⇒ A → Cowedge
Cowedge-∘ {A = A} W f = record
  { E         = A
  ; dinatural = extranaturalˡ (λ X → f ∘ dinatural.α X)
                              (assoc ○ ∘-resp-≈ʳ (extranatural-commˡ dinatural) ○ ⟺ assoc)
  }
  where open Cowedge W

record Coend : Set (levelOfTerm F) where
  field
    cowedge : Cowedge

  module cowedge = Cowedge cowedge
  open cowedge public
  open Cowedge

  field
    factor    : (W : Cowedge) → cowedge.E ⇒ E W
    universal : ∀ {W : Cowedge} {A} → factor W ∘ cowedge.dinatural.α A ≈ dinatural.α W A
    unique    : ∀ {W : Cowedge} {g : cowedge.E ⇒ E W} → (∀ {A} → g ∘ cowedge.dinatural.α A ≈ dinatural.α W A) → factor W ≈ g

  η-id : factor cowedge ≈ D.id
  η-id = unique identityˡ

  unique′ :(∀ {A} → f ∘ cowedge.dinatural.α A ≈ g ∘ cowedge.dinatural.α A) → f ≈ g
  unique′ {f = f} {g = g} eq = ⟺ (unique {W = Cowedge-∘ cowedge f} refl) ○ unique (⟺ eq)

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module Plus where

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

infixr 40 _+_
infix  10 _==_

_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

data _==_ (x, y : Nat) : Set where
  -- ...

postulate
  refl : {n : Nat} -> n == n
  cong : (f : Nat -> Nat){n, m : Nat} -> n == m -> f n == f m

plusZero : {n : Nat} -> n + zero == n
plusZero {zero}  = refl
plusZero {suc n} = cong suc plusZero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Common.Prelude renaming (return to foo)

main : IO Unit
main = foo unit


text:
-- There's something very strange going on with mutual and parameterised
-- modules.  Can't reproduce the bug... :(
module Mutual where

data True : Set where
  tt : True

data False : Set where

data _\/_ (A B : Set) : Set where
  inl : A -> A \/ B
  inr : B -> A \/ B

swap : {A B : Set} -> A \/ B -> B \/ A
swap (inl a) = inr a
swap (inr b) = inl b

module Foo (A : Set)(P : A -> Set) where

  Q : A -> A -> Set
  Q x y = P x \/ P y

mutual

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

  Even : Nat -> Set
  Even zero = True
  Even (suc zero) = False
  Even (suc (suc n)) = Even n

  f : Nat -> Set
  f zero    = True
  f (suc n) = Q n (suc n)
    where
      open module F = Foo Nat Even

  g : (n : Nat) -> f n
  g zero = tt
  g (suc zero) = inl tt
  g (suc (suc n)) = swap (g (suc n))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Agda.Builtin.Bool

F : Bool → Set
F true = Bool
F _    = Bool


text:
open import Relation.Binary.Core

module BHeap.Height {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_) where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import BHeap _≤_
open import BHeap.Properties _≤_
open import Data.Nat renaming (_≤_ to _≤ₙ_)
open import Data.Nat.Properties
open import Data.Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding (trans)

open DecTotalOrder decTotalOrder hiding (refl)

theorem-height-merge : {b : Bound}{x : A}(b≤x : LeB b (val x))(l r : BHeap (val x)) → height (merge tot≤ l r) ≤ₙ height (nd b≤x l r)
theorem-height-merge _ lf r = ≤-step (reflexive refl)
theorem-height-merge _ l lf rewrite lemma-merge-lf tot≤ l
    with total (height l) zero
... | inj₁ hl≤0 rewrite antisym hl≤0 z≤n = ≤-step (reflexive refl)
... | inj₂ 0≤hl = ≤-step (reflexive refl)
theorem-height-merge b≤x (nd {x = y} x≤y l r) (nd {x = y'} x≤y' l' r')
    with tot≤ y y' | total (height (nd x≤y l r)) (height (nd x≤y' l' r'))
... | inj₁ y≤y' | inj₁ hylr≤hy'l'r'
    with total (height (merge tot≤ l r)) (height (nd (lexy y≤y') l' r'))
... | inj₁ hmlr≤hy'l'r' = reflexive refl
... | inj₂ hy'l'r'≤hmlr rewrite antisym (trans (theorem-height-merge x≤y l r) hylr≤hy'l'r') hy'l'r'≤hmlr = reflexive refl
theorem-height-merge b≤x (nd {x = y} x≤y l r) (nd {x = y'} x≤y' l' r') | inj₁ y≤y' | inj₂ hy'l'r'≤hylr
    with total (height (merge tot≤ l r)) (height (nd (lexy y≤y') l' r'))
... | inj₁ hmlr≤hy'l'r' = s≤s hy'l'r'≤hylr
... | inj₂ hy'l'r'≤hmlr = s≤s (theorem-height-merge x≤y l r)
theorem-height-merge b≤x (nd {x = y} x≤y l r) (nd {x = y'} x≤y' l' r') | inj₂ y'≤y | inj₁ hylr≤hy'l'r'
    with total (height (nd (lexy y'≤y) l r)) (height (merge tot≤ l' r'))
... | inj₁ hylr≤hml'r' = s≤s (theorem-height-merge x≤y' l' r')
... | inj₂ hml'r'≤hylr = s≤s hylr≤hy'l'r'
theorem-height-merge b≤x (nd {x = y} x≤y l r) (nd {x = y'} x≤y' l' r') | inj₂ y'≤y | inj₂ hy'l'r'≤hylr
    with total (height (nd (lexy y'≤y) l r)) (height (merge tot≤ l' r'))
... | inj₁ hylr≤hml'r' rewrite antisym (trans (theorem-height-merge x≤y' l' r') hy'l'r'≤hylr) hylr≤hml'r' = reflexive refl
... | inj₂ hml'r'≤hylr = reflexive refl

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Cats.Category.Constructions.Iso where

open import Relation.Binary using (IsEquivalence ; Setoid)
open import Level

open import Cats.Category.Base
open import Cats.Util.Conv

import Relation.Binary.EqReasoning as EqReasoning

import Cats.Category.Constructions.Epi as Epi
import Cats.Category.Constructions.Mono as Mono

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

  private open module Cat = Category Cat
  open Cat.≈-Reasoning
  open Epi.Build Cat
  open Mono.Build Cat

  record _≅_ (A B : Obj) : Set (lo ⊔ la ⊔ l≈) where
    field
      forth : A ⇒ B
      back : B ⇒ A
      back-forth : back ∘ forth ≈ id
      forth-back : forth ∘ back ≈ id

  open _≅_

  instance
    HasArrow-≅ : ∀ {A B} → HasArrow (A ≅ B) lo la l≈
    HasArrow-≅ = record { Cat = Cat ; _⃗ = forth }

  ≅-equiv : IsEquivalence _≅_
  ≅-equiv = record { refl = refl ; sym = sym ; trans = trans }
    where
      refl : ∀ {A} → A ≅ A
      refl {A} = record
          { forth = id
          ; back = id
          ; back-forth = id-l
          ; forth-back = id-l
          }

      sym : ∀ {A B} → A ≅ B → B ≅ A
      sym iso = record
          { forth = back iso
          ; back = forth iso
          ; back-forth = forth-back iso
          ; forth-back = back-forth iso
          }

      trans : ∀ {A B C : Obj} → A ≅ B → B ≅ C → A ≅ C
      trans {A} {B} {C} A≅B B≅C = record
          { forth = forth B≅C ∘ forth A≅B
          ; back = back A≅B ∘ back B≅C
          ; back-forth
              = begin
                  (back A≅B ∘ back B≅C) ∘ forth B≅C ∘ forth A≅B
                ≈⟨ assoc ⟩
                  back A≅B ∘ back B≅C ∘ forth B≅C ∘ forth A≅B
                ≈⟨ ∘-resp-r (≈.trans unassoc (∘-resp-l (back-forth B≅C))) ⟩
                  back A≅B ∘ id ∘ forth A≅B
                ≈⟨ ∘-resp-r id-l ⟩
                  back A≅B ∘ forth A≅B
                ≈⟨ back-forth A≅B ⟩
                  id
                ∎
          ; forth-back
              = begin
                  (forth B≅C ∘ forth A≅B) ∘ back A≅B ∘ back B≅C
                ≈⟨ assoc ⟩
                  forth B≅C ∘ forth A≅B ∘ back A≅B ∘ back B≅C
                ≈⟨ ∘-resp-r (≈.trans unassoc (∘-resp-l (forth-back A≅B))) ⟩
                  forth B≅C ∘ id ∘ back B≅C
                ≈⟨ ∘-resp-r id-l ⟩
                  forth B≅C ∘ back B≅C
                ≈⟨ forth-back B≅C ⟩
                  id
                ∎
          }

  ≅-Setoid : Setoid lo (lo ⊔ la ⊔ l≈)
  ≅-Setoid = record
      { Carrier = Obj
      ; _≈_ = _≅_
      ; isEquivalence = ≅-equiv
      }

  module ≅ = IsEquivalence ≅-equiv
  module ≅-Reasoning = EqReasoning ≅-Setoid

  iso-mono : ∀ {A B} (iso : A ≅ B) → IsMono (forth iso)
  iso-mono iso {g = g} {h} iso∘g≈iso∘h
      = begin
          g
        ≈⟨ ≈.sym id-l ⟩
          id ∘ g
        ≈⟨ ∘-resp-l (≈.sym (back-forth iso)) ⟩
          (back iso ∘ forth iso) ∘ g
        ≈⟨ assoc ⟩
          back iso ∘ forth iso ∘ g
        ≈⟨ ∘-resp-r iso∘g≈iso∘h ⟩
          back iso ∘ forth iso ∘ h
        ≈⟨ unassoc ⟩
          (back iso ∘ forth iso) ∘ h
        ≈⟨ ∘-resp-l (back-forth iso) ⟩
          id ∘ h
        ≈⟨ id-l ⟩
          h
        ∎

  iso-epi : ∀ {A B} (iso : A ≅ B) → IsEpi (forth iso)
  iso-epi iso {g = g} {h} g∘iso≈h∘iso
      = begin
          g
        ≈⟨ ≈.sym id-r ⟩
          g ∘ id
        ≈⟨ ∘-resp-r (≈.sym (forth-back iso)) ⟩
          g ∘ forth iso ∘ back iso
        ≈⟨ unassoc ⟩
          (g ∘ forth iso) ∘ back iso
        ≈⟨ ∘-resp-l g∘iso≈h∘iso ⟩
          (h ∘ forth iso) ∘ back iso
        ≈⟨ assoc ⟩
          h ∘ forth iso ∘ back iso
        ≈⟨ ∘-resp-r (forth-back iso) ⟩
          h ∘ id
        ≈⟨ id-r ⟩
          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:
{-# OPTIONS --type-in-type #-}

module Fusion where

open import Data.Product renaming  (proj₁ to ₁; proj₂ to ₂) hiding (map; zip)
open import Relation.Binary.PropositionalEquality
open import Data.Sum hiding (map)
open import Data.Bool
open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Function
open import Data.Maybe hiding (map; zip; zipWith)
open import Data.List hiding (map; zip; _++_; filter; foldr; foldl; zipWith; drop; take)

module Stream1 where

  data Step (S A : Set) : Set where
    stop  : Step S A
    yield : A → S → Step S A
    skip  : S → Step S A

  mapStep : ∀ {A A' S S'} → (A → A') → (S → S') → Step S A → Step S' A'
  mapStep f g stop        = stop
  mapStep f g (yield a s) = yield (f a) (g s)
  mapStep f g (skip s)    = skip (g s)

  record Stream (A : Set) : Set where
    constructor stream
    field
      S    : Set
      seed : S
      step : S → Step S A
  open Stream public

  infixr 4 _++_
  _++_ : ∀ {A} → Stream A → Stream A → Stream A
  S    (xs ++ ys)           = S xs ⊎ S ys
  seed (xs ++ ys)           = inj₁ (seed xs)
  step (xs ++ ys) (inj₁ s ) with step xs s
  ... | stop       = skip (inj₂ (seed ys))
  ... | yield a s' = yield a (inj₁ s')
  ... | skip s'    = skip (inj₁ s')
  step (xs ++ ys) (inj₂ s) = mapStep id inj₂ (step ys s)

  filter : ∀ {A} → (A → Bool) → Stream A → Stream A
  S    (filter f as) = S as
  seed (filter f as) = seed as
  step (filter f as) s with step as s
  ... | stop       = stop
  ... | yield a s' = if f a then yield a s' else skip s'
  ... | skip s'    = skip s'

  map : ∀ {A B} → (A → B) → Stream A → Stream B
  S    (map f as) = S as
  seed (map f as) = seed as
  step (map f as) = mapStep f id ∘ step as

  empty : ∀ {A} → Stream A
  S    empty = ⊤
  seed empty = tt
  step empty = λ _ → stop

  pure : ∀ {A} → A → Stream A
  S    (pure a)       = Bool
  seed (pure a)       = true
  step (pure a) false = stop
  step (pure a) true  = yield a false

  bind : ∀ {A B} → Stream A → (A → Stream B) → Stream B
  S    (bind as f) = S as ⊎ (S as × ∃ (S ∘ f))
  seed (bind as f) = inj₁ (seed as)
  step (bind as f) (inj₁ s) with step as s
  ... | stop       = stop
  ... | yield a s' = skip (inj₂ (s' , a , seed (f a)))
  ... | skip s'    = skip (inj₁ s')
  step (bind as f) (inj₂ (s , a , s')) with step (f a) s'
  ... | stop        = skip (inj₁ s)
  ... | yield b s'' = yield b (inj₂ (s , a , s''))
  ... | skip s''    = skip (inj₂ (s , a , s''))

  zip : ∀ {A B} → Stream A → Stream B → Stream (A × B)
  S    (zip {A} as bs)                     = S as × S bs × Maybe A
  seed (zip {A} as bs)                     = seed as , seed bs , nothing
  step (zip {A} as bs) (sa , sb , nothing) with step as sa
  ... | stop        = stop
  ... | yield a sa' = skip (sa' , sb , just a)
  ... | skip sa'    = skip (sa' , sb , nothing)
  step (zip {A} as bs) (sa , sb , just a) with step bs sb
  ... | stop        = stop
  ... | yield b sb' = yield (a , b) (sa , sb' , nothing)
  ... | skip sb'    = skip (sa , sb' , just a)

  {-# NON_TERMINATING #-}
  foldr : ∀ {A B : Set} → (A → B → B) → B → Stream A → B
  foldr f b (stream S s step) with step s
  ... | stop       = b
  ... | yield a s' = f a (foldr f b (stream S s' step))
  ... | skip s'    = foldr f b (stream S s' step)

  {-# NON_TERMINATING #-}
  foldl : ∀ {A B : Set} → (B → A → B) → B → Stream A → B
  foldl f b (stream S s step) with step s
  ... | stop       = b
  ... | yield a s' = foldl f (f b a) (stream S s' step)
  ... | skip s'    = foldl f b (stream S s' step)

module Stream2 where

  data Step (S A : Set) : Set where
    stop  : Step S A
    yield : A → S → Step S A
    skip  : S → Step S A

  mapStep : ∀ {A A' S S'} → (A → A') → (S → S') → Step S A → Step S' A'
  mapStep f g stop        = stop
  mapStep f g (yield a s) = yield (f a) (g s)
  mapStep f g (skip s)    = skip (g s)

  record Prod (A : Set) : Set where
    constructor stream
    field
      S    : Set
      seed : S
      step : S → Step S A
  open Prod public

  infixr 4 _++_
  data Stream (A : Set) : Set where
    prod    : Prod A → Stream A
    _++_    : Stream A → Stream A → Stream A
    bind    : ∀ {B} → Stream B → (B → Stream A) → Stream A
    zipWith : ∀ {B C} → (B → C → A) → Stream B → Stream C → Stream A

  filter : ∀ {A} → (A → Bool) → Stream A → Stream A
  filter f (prod x) = {!!}
  filter f (str ++ str₁) = filter f str ++ filter f str₁
  filter f (bind str g) = bind str λ b → filter f (g b)
  filter f (zipWith x str str₁) = {!!} -- issue

  map : ∀ {A B} → (A → B) → Stream A → Stream B
  map f (prod as) = {!!}
  map f (as ++ as') = map f as ++ map f as'
  map f (bind bs g) = bind bs λ b → map f (g b)
      -- no bind fusion! (i.e. monad laws)
  map f (zipWith g bc cs) = {!!} -- can convert to prod, but better to freely add map...
                                 -- but then we don't have map fusion unless we just add it
                                 -- perhaps first-order syntax is OK, if we hand-write
                                 -- enough fusion?

  {-# NON_TERMINATING #-}
  foldr : ∀ {A B : Set} → (A → B → B) → B → Stream A → B
  foldr f b (prod x) = {!!}
  foldr f b (as ++ as') = foldr f (foldr f b as') as
  foldr {A} {B} f b (bind {C} cs g) = foldr (λ c b → foldr f b (g c)) b cs
  foldr {A} {B} f b (zipWith {C} {D} g cs ds) = {!!}
    -- first I have to convert cs/ds to producers to fold them!
    -- this means that optimization from first-order rep is blocked at the first zip!
    -- general solution: robust producer-to-state-machine compilation

module Stream3 where

  Step : Set → Set → Set
  Step S A = (Step : Set) → Step → (A → S → Step) → Step

  record Pull (A : Set) : Set where
    constructor pull
    field
      S    : Set
      seed : S
      step : S → Step S A
  open Pull public

  zip : ∀ {A B} → Pull A → Pull B → Pull (A × B)
  S    (zip as bs) = S as × S bs
  seed (zip as bs) = seed as , seed bs
  step (zip as bs) (sa , sb) _ stop yield =
    step as sa _
      stop
      λ a sa' → step bs sb _
        stop
        λ b sb' → yield (a , b) (sa , sb')

  map : ∀ {A B} → (A → B) → Pull A → Pull B
  S    (map f as) = S as
  seed (map f as) = seed as
  step (map f as) s _ stop yield = step as s _
    stop
    λ a s → yield (f a) s

  {-# NON_TERMINATING #-}
  find : ∀ {A S} → (A → Bool) → (S → Step S A) → S → Step S A
  find f step s _ stop yield = step s _
    stop
    λ a s → if f a then yield a s
                   else find f step s _ stop yield

  -- fusing filter without Skip!

  -- we can inline continuations in tail-recursive functions, and skipping to the next
  -- yield is such a loop
  filter : ∀ {A} → (A → Bool) → Pull A → Pull A
  S    (filter f as) = S as
  seed (filter f as) = seed as
  step (filter f as) = find f (step as)

  {-# NON_TERMINATING #-}
  drop' : ∀ {A S} → ℕ → (S → Step S A) → S → S
  drop' zero    step s = s
  drop' (suc n) step s = step s _ s λ a s → drop' n step s

  drop : ∀ {A} → ℕ → Pull A → Pull A
  S    (drop n as) = S as
  seed (drop n as) = drop' n (step as) (seed as)
  step (drop n as) = step as

  take : ∀ {A} → ℕ → Pull A → Pull A
  S    (take n as) = S as × ℕ
  seed (take n as) = seed as , n
  step (take n as) (s , zero)  _ stop yield = stop
  step (take n as) (s , suc x) _ stop yield = step as s _ stop λ a s → yield a (s , x)

  infixr 4 _++_
  _++_ : ∀ {A} → Pull A → Pull A → Pull A
  S    (xs ++ ys) = S xs ⊎ S ys
  seed (xs ++ ys) = inj₁ (seed xs)
  step (xs ++ ys) (inj₁ s) _ stop yield =
    step xs s _
      (step ys (seed ys) _
        stop
        λ a s → yield a (inj₂ s))
      λ a s → yield a (inj₁ s)
  step (xs ++ ys) (inj₂ s) _ stop yield =
    step ys s _
      stop
      λ a s → yield a (inj₂ s)

  {-# NON_TERMINATING #-}
  bind' : ∀ {A B : Set} (as : Pull A) (f : A → Pull B)
          → S as × Maybe (∃ (S ∘ f)) → Step (S as × Maybe (∃ (S ∘ f))) B
  bind' as f (sa , nothing)       _ stop yield =
    step as sa _
      stop
      λ a sa → step (f a) (seed (f a)) _
        (bind' as f (sa , nothing) _ stop yield)
        λ b sb → yield b (sa , (just (a , sb)))
  bind' as f (sa , just (a , sb)) _ stop yield =
    step (f a) sb _
      (bind' as f (sa , nothing) _ stop yield)
      λ b sb → yield b (sa , just (a , sb))

  {-# NON_TERMINATING #-}
  bindNothing' : ∀ {A B : Set} (as : Pull A) (f : A → Pull B)
          → S as → Step (S as × Maybe (∃ (S ∘ f))) B
  bindJust' : ∀ {A B : Set} (as : Pull A) (f : A → Pull B)
          → S as × ∃ (S ∘ f) → Step (S as × Maybe (∃ (S ∘ f))) B
  bindNothing' as f sa _ stop yield =
    step as sa _
      stop
      λ a sa → bindJust' as f (sa , a , seed (f a)) _ stop yield
  bindJust' as f (sa , a , sb) _ stop yield =
    step (f a) sb _
      (bindNothing' as f sa _ stop yield)
      λ b sb → yield b (sa , just (a , sb))

  bind : ∀ {A B} → Pull A → (A → Pull B) → Pull B
  S    (bind as f) = S as × Maybe (∃ (S ∘ f))
  seed (bind as f) = seed as , nothing
  step (bind as f) (sa , nothing) _ stop yield = bindNothing' as f sa _ stop yield
  step (bind as f) (sa , just x)  _ stop yield = bindJust' as f (sa , x) _ stop yield

max_stars_repo_name: AndrasKovacs/staged

max_issues_repo_name: AndrasKovacs/staged

max_forks_repo_name: AndrasKovacs/staged


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Results concerning uniqueness of identity proofs, with axiom K
------------------------------------------------------------------------

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

module Axiom.UniquenessOfIdentityProofs.WithK where

open import Axiom.UniquenessOfIdentityProofs
open import Relation.Binary.PropositionalEquality.Core

-- Axiom K implies UIP.

uip : ∀ {a A} → UIP {a} A
uip refl refl = refl


text:
-- examples for termination checking mutual recursion

module Mutual where

data Odd : Set

data Even : Set where
  zeroE : Even
  succE : Odd -> Even

data Odd where
  succO : Even -> Odd

addEO : Even -> Odd -> Odd

addOO : Odd -> Odd -> Even
addOO (succO x) y = succE (addEO x y)

addEO zeroE y = y
addEO (succE x) y = succO (addOO x y)


text:
--{-# OPTIONS -v tc.pos:100 #-}

open import Agda.Builtin.Equality

data ⊥ : Set where

postulate
  A : Set
  R : A → Set

magic : ⊥ → A
magic ()

test : (a : ⊥) → magic a ≡ magic _
test a = refl


text:
module Main where
{-# IMPORT System.IO #-}
{-# IMPORT System.Environment #-}

open import Base
open import IO
open import IO.File

postulate
  getArgs : IO (List String)
{-# COMPILED getArgs getArgs #-}

_`bindIO`_ : {A B : Set} -> IO A -> (A -> IO B) -> IO B
_`bindIO`_ = bindIO

main : IO Unit
main = getArgs `bindIO` mainWithArgs
  where
    mainWithArgs : List String -> IO Unit
    mainWithArgs [] = putStrLn "Give a file name silly"
    mainWithArgs (file :: []) =
      runFileIO (
        openFile file readMode >>= \h ->
        -- hGetLine h hd          >>= \s ->
        -- hClose h hd            >>= \_ ->
        hGetContents h hd         >>= \s ->
        return s
      ) `bindIO` \s -> putStrLn s
    mainWithArgs (_ :: _ :: _) =
      putStrLn "Just one file will do, thank you very much."


text:
-- A term model à la Beth

open import Library hiding (_∈_)

module TermModel (Base : Set) where

import Formulas   ; open module Form = Formulas    Base
import Derivations; open module Der  = Derivations Base

-- Beth model

data Cover (Δ : Cxt) : Set where
  idc  : Cover Δ
  bot  : (t : Δ ⊢ False) → Cover Δ
  node : ∀{A B} (t : Δ ⊢ A ∨ B) (C : Cover (Δ ∙ A)) (D : Cover (Δ ∙ B)) → Cover Δ

data _∈_ Γ : ({Δ} : Cxt) (C : Cover Δ) → Set where
  here  : Γ ∈ idc {Γ}
  left  : ∀{Δ A B C D}{t : Δ ⊢ A ∨ B} (e : Γ ∈ C) → Γ ∈ node t C D
  right : ∀{Δ A B C D}{t : Δ ⊢ A ∨ B} (e : Γ ∈ D) → Γ ∈ node t C D

coverWk : ∀{Γ Δ} {C : Cover Δ} (e : Γ ∈ C) → Γ ≤ Δ
coverWk here      = id≤
coverWk (left  e) = coverWk e • weak id≤
coverWk (right e) = coverWk e • weak id≤

transC : ∀{Γ} (C : Cover Γ) (f : ∀{Δ} → Δ ∈ C → Cover Δ) → Cover Γ
transC idc f = f here
transC (bot t) f = bot t
transC (node t C D) f = node t (transC C (f ∘ left)) (transC D (f ∘ right))

-- UNUSED:
trans∈ : ∀{Γ} (C : Cover Γ) (f : ∀{Δ} → Δ ∈ C → Cover Δ) →
  ∀ {Φ} {Δ} (e : Δ ∈ C) → Φ ∈ f e → Φ ∈ transC C f
trans∈ idc f here = id
trans∈ (bot t) f ()
trans∈ (node t C D) f (left  e) = left  ∘ trans∈ C (f ∘ left ) e
trans∈ (node t C D) f (right e) = right ∘ trans∈ D (f ∘ right) e

split∈ : ∀{Γ} (C : Cover Γ) (f : ∀{Δ} → Δ ∈ C → Cover Δ) {Φ} (e : Φ ∈ transC C f)
  → ∃ λ Δ → ∃ λ (e : Δ ∈ C) → Φ ∈ f e
split∈ idc f e = _ , _ , e
split∈ (bot t) f ()
split∈ (node t C D) f (left e) with split∈ C (f ∘ left) e
... | Δ , e₁ , e₂ = Δ , left e₁ , e₂
split∈ (node t C D) f (right e) with split∈ D (f ∘ right) e
... | Δ , e₁ , e₂ = Δ , right e₁ , e₂

-- Empty cover

EmptyCover : (Γ : Cxt) → Set
EmptyCover Γ = Σ (Cover Γ) λ C → ∀{Δ} → Δ ∈ C → ⊥

-- Empty cover is isomorphic to a witness of inconsistency

toEmptyCover : ∀{Γ} (t : Γ ⊢ False) → EmptyCover Γ
toEmptyCover t = bot t , λ()

fromEmptyCover : ∀{Γ} (ec : EmptyCover Γ) → Γ ⊢ False
fromEmptyCover (C , f) = reifyF C f
  where
  reifyF : ∀ {Γ} (C : Cover Γ) (f : ∀ {Δ} → Δ ∈ C → ⊥) → Γ ⊢ False
  reifyF idc          f = ⊥-elim (f here)
  reifyF (bot t)      f = t
  reifyF (node t C D) f = orE t (reifyF C (f ∘ left)) (reifyF D (f ∘ right))

transE : ∀{Γ} (C : Cover Γ) (f : ∀{Δ} → Δ ∈ C → EmptyCover Δ) → EmptyCover Γ
transE C f = transC C (proj₁ ∘ f) , λ e → let _ , e₁ , e₂ = split∈ C (proj₁ ∘ f) e in f e₁ .proj₂ e₂

-- Paste (from Thorsten)

paste' : ∀{A Γ} (C : Cover Γ) (f : ∀{Δ} (e : Δ ∈ C) → Δ ⊢ A) → Γ ⊢ A
paste' idc          f = f here
paste' (bot t)      f = falseE t
paste' (node t C D) f = orE t (paste' C (f ∘ left)) (paste' D (f ∘ right))

-- Weakening Covers

monC : ∀{Γ Δ} (τ : Δ ≤ Γ) (C : Cover Γ) → Cover Δ
monC τ idc = idc
monC τ (bot t) = bot (monD τ t)
monC τ (node t C D) = node (monD τ t) (monC (lift τ) C) (monC (lift τ) D)

mon∈ : ∀{Γ Δ Φ} (C : Cover Γ) (τ : Δ ≤ Γ) (e : Φ ∈ monC τ C) → ∃ λ Ψ → Ψ ∈ C × Φ ≤ Ψ
mon∈ {Γ} {Δ} {.Δ} idc τ here = _ , here , τ
mon∈ {Γ} {Δ} {Φ} (bot t) τ ()
mon∈ {Γ} {Δ} {Φ} (node t C D) τ (left e) with mon∈ C (lift τ) e
... | Ψ , e' , σ = Ψ , left e' , σ
mon∈ {Γ} {Δ} {Φ} (node t C D) τ (right e) with mon∈ D (lift τ) e
... | Ψ , e' , σ = Ψ , right e' , σ

-- The syntactic Beth model

T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
T⟦ Atom P ⟧ Γ = Γ ⊢ Atom P
T⟦ True ⟧ Γ = ⊤
T⟦ False ⟧ Γ = EmptyCover Γ
T⟦ A ∨ B ⟧ Γ = ∃ λ (C : Cover Γ) → ∀{Δ} → Δ ∈ C → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ
T⟦ A ∧ B ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
T⟦ A ⇒ B ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ B ⟧ Δ

monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ
monT (Atom P) τ t = monD τ t
monT True τ _ = _
monT False τ (C , f) = monC τ C , λ {Φ} e → f (proj₁ (proj₂ (mon∈ C τ e)))
monT (A ∨ B) {Γ} {Δ} τ (C , f) = monC τ C ,  λ {Φ} e →
  let Ψ , e' , σ = mon∈ C τ e
  in  map-⊎ (monT A σ) (monT B σ) (f {Ψ} e')
monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
monT (A ⇒ B) τ f σ = f (σ • τ)

-- Reflection / reification

mutual

  reflect : ∀{Γ} A (t : Γ ⊢ A) → T⟦ A ⟧ Γ
  reflect (Atom P) t = t
  reflect True t = _
  reflect False = toEmptyCover
  reflect (A ∨ B) t = node t idc idc , aux
    where
    aux : ∀{Δ} → Δ ∈ node t idc idc → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ
    aux (left  here) = inj₁ (reflect A (hyp top))
    aux (right here) = inj₂ (reflect B (hyp top))

  reflect (A ∧ B) t = reflect A (andE₁ t) , reflect B (andE₂ t)
  reflect (A ⇒ B) t τ a = reflect B (impE (monD τ t) (reify A a))

  reify : ∀{Γ} A (⟦f⟧ :  T⟦ A ⟧ Γ) → Γ ⊢ A
  reify (Atom P) t      = t
  reify True _          = trueI
  reify False           = fromEmptyCover
  reify (A ∨ B) (C , f) = paste' C ([ orI₁ ∘ reify A , orI₂ ∘ reify B ] ∘ f)
  reify (A ∧ B) (a , b) = andI (reify A a) (reify B b)
  reify (A ⇒ B) ⟦f⟧     = impI (reify B (⟦f⟧ (weak id≤) (reflect A (hyp top))))

-- In the absurd world, every proposition holds.

absurd : ∀{Γ A} (t : Γ ⊢ False) → T⟦ A ⟧ Γ
absurd t = reflect _ (falseE t)

-- We can paste in the model thanks to reflection and reification.
-- (However, this does not look nice, since it goes through terms.)

-- paste : ∀ {A Γ} (C : Cover Γ) (f : ∀{Δ} (e : Δ ∈ C) → T⟦ A ⟧ Δ) → T⟦ A ⟧ Γ
-- paste C f = reflect _ (paste' C (reify _ ∘ f))

-- Semantic paste:

paste : ∀ A {Γ} (C : Cover Γ) (f : ∀{Δ} (e : Δ ∈ C) → T⟦ A ⟧ Δ) → T⟦ A ⟧ Γ
paste (Atom P) = paste'
paste True C f = _
paste False C f = transE C f
paste (A ∨ B) C f = transC C (proj₁ ∘ f) , λ e → let _ , e₁ , e₂ = split∈ C (proj₁ ∘ f) e in f e₁ .proj₂ e₂
paste (A ∧ B) C f = paste A C (proj₁ ∘ f) , paste B C (proj₂ ∘ f)
paste (A ⇒ B) C f τ a = paste B (monC τ C) λ {Δ} e → let Ψ , e' , σ  = mon∈ C τ e in f e' σ (monT A (coverWk e) a)

-- Fundamental theorem

-- Extension of T⟦_⟧ to contexts

G⟦_⟧ : ∀ (Γ Δ : Cxt) → Set
G⟦ ε     ⟧ Δ = ⊤
G⟦ Γ ∙ A ⟧ Δ = G⟦ Γ ⟧ Δ × T⟦ A ⟧ Δ

monG : ∀{Γ Δ Φ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ → G⟦ Γ ⟧ Φ
monG {ε} τ _ = _
monG {Γ ∙ A} τ (γ , a) = monG τ γ , monT A τ a

-- Variable case

fundH : ∀{Γ Δ A} (x : Hyp A Γ) (γ : G⟦ Γ ⟧ Δ) → T⟦ A ⟧ Δ
fundH top     = proj₂
fundH (pop x) = fundH x ∘ proj₁

-- A lemma for the orElim case.

orElim : ∀ {Γ A B X} (C : Cover Γ) (f : {Δ : Cxt} → Δ ∈ C → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ) →
         (∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ X ⟧ Δ) →
         (∀{Δ} (τ : Δ ≤ Γ) → T⟦ B ⟧ Δ → T⟦ X ⟧ Δ) →
         T⟦ X ⟧ Γ
orElim C f g h = paste _ C λ e → [ g (coverWk e) , h (coverWk e) ] (f e)

-- falseElim :
falseElim : ∀{Γ A} (C : Cover Γ) (f : ∀{Δ} → Δ ∈ C → ⊥) → T⟦ A ⟧ Γ
falseElim C f = paste _ C (⊥-elim ∘ f)

-- The fundamental theorem

fund :  ∀{Γ A} (t : Γ ⊢ A) {Δ} (γ : G⟦ Γ ⟧ Δ) → T⟦ A ⟧ Δ
fund (hyp x) = fundH x
fund (impI t) γ τ a = fund t (monG τ γ , a)
fund (impE t u) γ = fund t γ id≤ (fund u γ)
fund (andI t u) γ = fund t γ , fund u γ
fund (andE₁ t) = proj₁ ∘ fund t
fund (andE₂ t) = proj₂ ∘ fund t
fund (orI₁ t) γ = idc , inj₁ ∘ λ{ here → fund t γ }
fund (orI₂ t) γ = idc , inj₂ ∘ λ{ here → fund t γ }
fund (orE t u v) γ = uncurry orElim (fund t γ)
  (λ τ a → fund u (monG τ γ , a))
  (λ τ b → fund v (monG τ γ , b))
fund (falseE t) γ = uncurry falseElim (fund t γ)
fund trueI γ = _

-- -}
-- -}

-- Example:

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
------------------------------------------------------------------------
-- Decoding types and subtypes into SK terms and equality
------------------------------------------------------------------------

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

module FOmegaInt.Undecidable.Decoding where

open import Data.List using ([]; _∷_)
open import Data.Product using (_,_; proj₁; proj₂; _×_)
open import Data.Fin using (zero; suc)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.ExtraLemmas
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import FOmegaInt.Syntax
open import FOmegaInt.Kinding.Canonical as Canonical
open import FOmegaInt.Kinding.Canonical.Reduced as Reduced
open import FOmegaInt.Undecidable.SK
open import FOmegaInt.Undecidable.Encoding

open Syntax
open ElimCtx
open Substitution hiding (subst)
open Canonical.Kinding using (_⊢_<:_; _⊢_<:_⇇_; <:-⇇)
open Reduced.Kinding
open Encoding
open ≡-Reasoning
module V   = VarSubst
module EL  = TermLikeLemmas Substitution.termLikeLemmasElim
module ELV = LiftAppLemmas EL.varLiftAppLemmas

------------------------------------------------------------------------
-- Decoding of types into SK? terms

decode : Elim |Γ| → SK?Term
decode (var x₀ ∙ (a ∷ b ∷ _))     = K · (decode a) · (decode b)
decode (var x₁ ∙ (a ∷ b ∷ c ∷ _)) = S · (decode a) · (decode b) · (decode c)
decode (var x₂ ∙ (a ∷ b ∷ _))     = K · (decode a) · (decode b)
decode (var x₃ ∙ (a ∷ b ∷ c ∷ _)) = S · (decode a) · (decode b) · (decode c)
decode (var x₄ ∙ (a ∷ b ∷ _))     = decode a · decode b
decode (var x₅ ∙ _)               = K
decode (var x₆ ∙ _)               = S
decode (⊥ ∙ _)                    = ⊥
decode (⊤ ∙ _)                    = ⊤
{-# CATCHALL #-}
decode _ = ⊤

-- Decoding is the left-inverse of encoding.
--
-- NOTE. We encode SK terms but decode to SK? terms, so decoding is
-- strictly speaking only left-inverse when restricted to (pure) SK
-- terms.  Hence the use of `inject' here.

decode-encode : ∀ t → decode (encode t) ≡ inject t
decode-encode S       = refl
decode-encode K       = refl
decode-encode (s · t) = cong₂ _·_ (decode-encode s) (decode-encode t)

-- Decoding subsumes squashing

decode-squash : ∀ (a : Elim |Γ|) → decode (squashElim a) ≡ decode a
decode-squash (var x₀ ∙ [])              = refl   -- degenerate case
decode-squash (var x₀ ∙ (_ ∷ []))        = refl   -- degenerate case
decode-squash (var x₀ ∙ (a ∷ b ∷ _))     =
  cong₂ (λ a b → K · a · b) (decode-squash a) (decode-squash b)
decode-squash (var x₁ ∙ [])              = refl   -- degenerate case
decode-squash (var x₁ ∙ (_ ∷ []))        = refl   -- degenerate case
decode-squash (var x₁ ∙ (_ ∷ _ ∷ []))    = refl   -- degenerate case
decode-squash (var x₁ ∙ (a ∷ b ∷ c ∷ _)) =
  trans (cong (S · _ · _ ·_) (decode-squash c))
        (cong₂ (λ a b → S · a · b · _) (decode-squash a) (decode-squash b))
decode-squash (var x₂ ∙ [])              = refl   -- degenerate case
decode-squash (var x₂ ∙ (_ ∷ []))        = refl   -- degenerate case
decode-squash (var x₂ ∙ (a ∷ b ∷ _))     =
  cong₂ (λ a b → K · a · b) (decode-squash a) (decode-squash b)
decode-squash (var x₃ ∙ [])              = refl   -- degenerate case
decode-squash (var x₃ ∙ (_ ∷ []))        = refl   -- degenerate case
decode-squash (var x₃ ∙ (_ ∷ _ ∷ []))    = refl   -- degenerate case
decode-squash (var x₃ ∙ (a ∷ b ∷ c ∷ _)) =
  trans (cong (S · _ · _ ·_) (decode-squash c))
        (cong₂ (λ a b → S · a · b · _) (decode-squash a) (decode-squash b))
decode-squash (var x₄ ∙ [])              = refl   -- degenerate case
decode-squash (var x₄ ∙ (_ ∷ []))        = refl   -- degenerate case
decode-squash (var x₄ ∙ (a ∷ b ∷ _))     =
  cong₂ _·_ (decode-squash a) (decode-squash b)
decode-squash (var x₅ ∙ as) = refl
decode-squash (var x₆ ∙ as) = refl
decode-squash (⊥ ∙ as)      = refl
decode-squash (⊤ ∙ as)      = refl
-- squashed cases
decode-squash (Π k a   ∙ as) = refl
decode-squash ((a ⇒ b) ∙ as) = refl
decode-squash (Λ k a   ∙ as) = refl
decode-squash (ƛ a b   ∙ as) = refl
decode-squash (a ⊡ b   ∙ as) = refl

-- Helper lemmas to be used when decoding kinding derivations.

⌜⌝-⌞⌟-∙∙ : ∀ {n} (a : Elim n) → ⌜ ⌞ a ⌟ ⌝ ∙∙ [] ≡ a
⌜⌝-⌞⌟-∙∙ a = begin
  ⌜ ⌞ a ⌟ ⌝ ∙∙ []  ≡⟨ ∙∙-[] ⌜ ⌞ a ⌟ ⌝ ⟩
  ⌜ ⌞ a ⌟ ⌝        ≡⟨ ⌜⌝∘⌞⌟-id a ⟩
  a                ∎

⌜⌝-⌞⌟-weaken-sub₁ : ∀ {n} (a b : Elim n) →
                    (⌜ weaken ⌞ a ⌟ ⌝ ∙∙ []) Elim[ ⌞ b ⌟ ] ≡ a
⌜⌝-⌞⌟-weaken-sub₁ a b = begin
    (⌜ weaken ⌞ a ⌟ ⌝ ∙∙ []) Elim[ ⌞ b ⌟ ]
  ≡˘⟨ cong (λ a → (⌜ a ⌝ ∙∙ []) Elim[ ⌞ b ⌟ ]) (⌞⌟-/Var a) ⟩
    (⌜ ⌞ weakenElim a ⌟ ⌝ ∙∙ []) Elim[ ⌞ b ⌟ ]
  ≡⟨ cong (_Elim[ ⌞ b ⌟ ]) (⌜⌝-⌞⌟-∙∙ (weakenElim a)) ⟩
    weakenElim a Elim[ ⌞ b ⌟ ]
  ≡⟨ EL.weaken-sub a ⟩
    a
  ∎

⌜⌝-⌞⌟-weaken-sub₂ : ∀ {n} (a b c : Elim n) →
  ((⌜ weaken (weaken ⌞ a ⌟) ⌝ ∙∙ []) Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ] ≡ a
⌜⌝-⌞⌟-weaken-sub₂ a b c = begin
    ((⌜ weaken (weaken ⌞ a ⌟) ⌝ ∙∙ []) Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ]
  ≡˘⟨ cong (λ a → ((⌜ a ⌝ ∙∙ []) Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ])
           (trans (⌞⌟-/Var (weakenElim a)) (cong weaken (⌞⌟-/Var a))) ⟩
    ((⌜ ⌞ weakenElim (weakenElim a) ⌟ ⌝ ∙∙ []) Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ]
  ≡⟨ cong (λ a → (a Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ])
          (⌜⌝-⌞⌟-∙∙ (weakenElim (weakenElim a))) ⟩
    (weakenElim (weakenElim a) Elim/ sub ⌞ b ⌟ ↑) Elim[ ⌞ c ⌟ ]
  ≡⟨ cong (_Elim[ ⌞ c ⌟ ]) (sym (EL.weaken-/ (weakenElim a))) ⟩
    weakenElim (weakenElim a Elim/ sub ⌞ b ⌟) Elim[ ⌞ c ⌟ ]
  ≡⟨ cong ((_Elim[ ⌞ c ⌟ ]) ∘ weakenElim) (EL.weaken-sub a) ⟩
    weakenElim a Elim[ ⌞ c ⌟ ]
  ≡⟨ EL.weaken-sub a ⟩
    a
  ∎

-- Decoding of (reduced) canonical type order into the SK? term order.

mutual

  decode-∼ : ∀ {a b} → Γ-SK? ⊢ a ∼ b → decode a ≤SK? decode b
  decode-∼ (∼-trans a∼b b∼c) = ≤?-trans (decode-∼ a∼b) (decode-∼ b∼c)
  decode-∼ (∼-⊥ b⇉b⋯b)       = ≤?-⊥
  decode-∼ (∼-⊤ a⇉a⋯a)       = ≤?-⊤
  decode-∼ (∼-∙ (⇉-var x₀ _ refl) (∼-∷ _ _ a₁∼b₁ (∼-∷ _ _ a₂∼b₂ ∼-[]))) =
    ≤?-· (≤?-· ≤?-refl (decode-∼ a₁∼b₁)) (decode-∼ a₂∼b₂)
  decode-∼ (∼-∙ (⇉-var x₁ _ refl)
           (∼-∷ _ _ a₁∼b₁ (∼-∷ _ _ a₂∼b₂ (∼-∷ _ _ a₃∼b₃ ∼-[])))) =
    ≤?-· (≤?-· (≤?-· ≤?-refl (decode-∼ a₁∼b₁)) (decode-∼ a₂∼b₂))
         (decode-∼ a₃∼b₃)
  decode-∼ (∼-∙ (⇉-var x₂ _ refl) (∼-∷ _ _ a₁∼b₁ (∼-∷ _ _ a₂∼b₂ ∼-[]))) =
    ≤?-· (≤?-· ≤?-refl (decode-∼ a₁∼b₁)) (decode-∼ a₂∼b₂)
  decode-∼ (∼-∙ (⇉-var x₃ _ refl)
           (∼-∷ _ _ a₁∼b₁ (∼-∷ _ _ a₂∼b₂ (∼-∷ _ _ a₃∼b₃ ∼-[])))) =
    ≤?-· (≤?-· (≤?-· ≤?-refl (decode-∼ a₁∼b₁)) (decode-∼ a₂∼b₂))
         (decode-∼ a₃∼b₃)
  decode-∼ (∼-∙ (⇉-var x₄ _ refl) (∼-∷ _ _ a₁∼b₁ (∼-∷ _ _ a₂∼b₂ ∼-[]))) =
    ≤?-· (decode-∼ a₁∼b₁) (decode-∼ a₂∼b₂)
  decode-∼ (∼-∙ (⇉-var x₅ _ refl) ∼-[]) = ≤?-refl
  decode-∼ (∼-∙ (⇉-var x₆ _ refl) ∼-[]) = ≤?-refl
  decode-∼ (∼-⟨| a⇉b⋯c) = proj₁ (decode-Ne⇉ a⇉b⋯c)
  decode-∼ (∼-|⟩ a⇉b⋯c) = proj₂ (decode-Ne⇉ a⇉b⋯c)

  decode-Ne⇉ : ∀ {a b c} → Γ-SK? ⊢Ne a ⇉ b ⋯ c →
               decode b ≤SK? decode a × decode a ≤SK? decode c
  decode-Ne⇉ (⇉-∙ (⇉-var x₀ _ refl) (⇉-∷ {a} a∈* (⇉-∷ {b} b∈* ⇉-[]))) =
    subst (λ a′ → decode a′ ≤SK? K · (decode a) · (decode b))
          (sym (⌜⌝-⌞⌟-weaken-sub₁ a b)) ≤?-Kexp ,
    subst₂ (λ a′ b′ → K · decode a  · decode b ≤SK?
                      K · decode a′ · decode b′)
           (sym (⌜⌝-⌞⌟-weaken-sub₁ a b)) (sym (⌜⌝-⌞⌟-∙∙ b)) ≤?-refl
  decode-Ne⇉ (⇉-∙ (⇉-var x₁ _ refl)
                  (⇉-∷ {a} a∈* (⇉-∷ {b} b∈* (⇉-∷ {c} c∈* ⇉-[])))) =
    subst₂ (λ a′ b′ → decode a′ · decode c′ · (decode b′ · decode c′) ≤SK?
                      S · decode a · decode b · decode c)
      (sym (⌜⌝-⌞⌟-weaken-sub₂ a b c)) (sym (⌜⌝-⌞⌟-weaken-sub₁ b c))
      (subst (λ c′ → decode a · decode c′ · (decode b · decode c′) ≤SK?
                     S · decode a · decode b · decode c)
        (sym (⌜⌝-⌞⌟-∙∙ c)) ≤?-Sexp) ,
    subst₂ (λ a′ b′ → S · decode a  · decode b  · decode c ≤SK?
                      S · decode a′ · decode b′ · decode c′)
      (sym (⌜⌝-⌞⌟-weaken-sub₂ a b c)) (sym (⌜⌝-⌞⌟-weaken-sub₁ b c))
      (subst (λ c′ → S · decode a · decode b · decode c ≤SK?
                     S · decode a · decode b · decode c′)
        (sym (⌜⌝-⌞⌟-∙∙ c)) ≤?-refl)
    where c′ = ⌜ ⌞ c ⌟ ⌝ ∙∙ []
  decode-Ne⇉ (⇉-∙ (⇉-var x₂ _ refl) (⇉-∷ {a} a∈* (⇉-∷ {b} b∈* ⇉-[]))) =
    subst₂ (λ a′ b′ → K · decode a′ · decode b′ ≤SK?
                      K · decode a  · decode b)
           (sym (⌜⌝-⌞⌟-weaken-sub₁ a b)) (sym (⌜⌝-⌞⌟-∙∙ b)) ≤?-refl ,
    subst (λ a′ → K · decode a · decode b ≤SK? decode a′)
          (sym (⌜⌝-⌞⌟-weaken-sub₁ a b)) ≤?-Kred
  decode-Ne⇉ (⇉-∙ (⇉-var x₃ _ refl)
             (⇉-∷ {a} a∈* (⇉-∷ {b} b∈* (⇉-∷ {c} c∈* ⇉-[])))) =
    subst₂ (λ a′ b′ → S · decode a′ · decode b′ · decode c′ ≤SK?
                      S · decode a  · decode b  · decode c)
      (sym (⌜⌝-⌞⌟-weaken-sub₂ a b c)) (sym (⌜⌝-⌞⌟-weaken-sub₁ b c))
      (subst (λ c′ → S · decode a · decode b · decode c′ ≤SK?
                     S · decode a · decode b · decode c)
        (sym (⌜⌝-⌞⌟-∙∙ c)) ≤?-refl) ,
    subst₂ (λ a′ b′ → S · decode a · decode b · decode c ≤SK?
                      decode a′ · decode c′ · (decode b′ · decode c′))
      (sym (⌜⌝-⌞⌟-weaken-sub₂ a b c)) (sym (⌜⌝-⌞⌟-weaken-sub₁ b c))
      (subst (λ c′ → S · decode a · decode b · decode c ≤SK?
                     decode a · decode c′ · (decode b · decode c′))
        (sym (⌜⌝-⌞⌟-∙∙ c)) ≤?-Sred)
    where c′ = ⌜ ⌞ c ⌟ ⌝ ∙∙ []
  decode-Ne⇉ (⇉-∙ (⇉-var x₄ _ refl) (⇉-∷ a∈* (⇉-∷ b∈* ⇉-[]))) = ≤?-⊥ , ≤?-⊤
  decode-Ne⇉ (⇉-∙ (⇉-var x₅ _ refl) ⇉-[]) = ≤?-⊥ , ≤?-⊤
  decode-Ne⇉ (⇉-∙ (⇉-var x₆ _ refl) ⇉-[]) = ≤?-⊥ , ≤?-⊤

-- The SK? signature is a first-order context.

kdS-fo : FOKind (kdS {0})
kdS-fo = fo-⋯

kdK-fo : FOKind (kdK {0})
kdK-fo = fo-⋯

kdApp-fo : FOKind (kdApp {0})
kdApp-fo = fo-Π (fo-Π fo-⋯)

kdSRed-fo : FOKind (kdSRed {0})
kdSRed-fo = fo-Π (fo-Π (fo-Π fo-⋯))

kdKRed-fo : FOKind (kdKRed {0})
kdKRed-fo = fo-Π (fo-Π fo-⋯)

kdSExp-fo : FOKind (kdSExp {0})
kdSExp-fo = fo-Π (fo-Π (fo-Π fo-⋯))

kdKExp-fo : FOKind (kdKExp {0})
kdKExp-fo = fo-Π (fo-Π fo-⋯)

Γ-SK?-fo : FOCtx Γ-SK?
Γ-SK?-fo =
  fo-∷ (fo-kd kdKExp-fo)
       (fo-∷ (fo-kd kdSExp-fo)
             (fo-∷ (fo-kd kdKRed-fo)
                   (fo-∷ (fo-kd kdSRed-fo)
                         (fo-∷ (fo-kd kdApp-fo)
                               (fo-∷ (fo-kd kdK-fo)
                                     (fo-∷ (fo-kd kdS-fo) fo-[]))))))

-- Decoding of canonical subtyping into the SK? term order.

decode-<: : ∀ {a b} → Γ-SK? ⊢ a <: b → decode a ≤SK? decode b
decode-<: {a} {b} a<:b =
  subst₂ (_≤SK?_) (decode-squash a) (decode-squash b)
         (decode-∼ (reduce-<: Γ-SK?-fo a<:b))

decode-<:⇇ : ∀ {a b} → Γ-SK? ⊢ a <: b ⇇ ⌜*⌝ → decode a ≤SK? decode b
decode-<:⇇ {a} {b} (<:-⇇ _ _ a<:b) = decode-<: a<:b

-- Full decoding to SK term equality.

decode-<:⇇-encode : ∀ {s t} → Γ-SK? ⊢ encode s <: encode t ⇇ ⌜*⌝ → s ≡SK t
decode-<:⇇-encode {s} {t} es<:et⇇* =
  inject-≤SK?-≡SK (subst₂ (_≤SK?_) (decode-encode s) (decode-encode t)
                          (decode-<:⇇ es<:et⇇*))

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.WedgeOfSpheres where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Connected

open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.Foundations.Prelude
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Truncation renaming (elim to trElim)
open import Cubical.Algebra.Group

S¹⋁S¹ : Type₀
S¹⋁S¹ = S₊∙ 1 ⋁ S₊∙ 1

S²⋁S¹⋁S¹ : Type₀
S²⋁S¹⋁S¹ = S₊∙ 2 ⋁ (S¹⋁S¹ , inl base)

------------- H⁰(S¹⋁S¹) ------------
H⁰-S¹⋁S¹ : GroupIso (coHomGr 0 S¹⋁S¹) intGroup
H⁰-S¹⋁S¹ = H⁰-connected (inl base) (wedgeConnected _ _ (Sn-connected 0) (Sn-connected 0))

------------- H¹(S¹⋁S¹) ------------
H¹-S¹⋁S¹ : GroupIso (coHomGr 1 S¹⋁S¹) (dirProd intGroup intGroup)
H¹-S¹⋁S¹ =  (Hⁿ-⋁ _ _ 0) □ dirProdGroupIso coHom1S1≃ℤ coHom1S1≃ℤ

------------- H⁰(S²⋁S¹⋁S¹) ---------
H⁰-S²⋁S¹⋁S¹ : GroupIso (coHomGr 0 S²⋁S¹⋁S¹) intGroup
H⁰-S²⋁S¹⋁S¹ = H⁰-connected (inl north)
                  (wedgeConnected _ _
                    (Sn-connected 1)
                    (wedgeConnected _ _
                      (Sn-connected 0)
                      (Sn-connected 0)))

------------- H¹(S²⋁S¹⋁S¹) ---------
H¹-S²⋁S¹⋁S¹ : GroupIso (coHomGr 1 S²⋁S¹⋁S¹) (dirProd intGroup intGroup)
H¹-S²⋁S¹⋁S¹ =
    Hⁿ-⋁ (S₊∙ 2) (S¹⋁S¹ , inl base) 0
  □ dirProdGroupIso (H¹-Sⁿ≅0 0) H¹-S¹⋁S¹
  □ lUnitGroupIso

------------- H²(S²⋁S¹⋁S¹) ---------
H²-S²⋁S¹⋁S¹ : GroupIso (coHomGr 2 S²⋁S¹⋁S¹) intGroup
H²-S²⋁S¹⋁S¹ =
  compGroupIso
  (Hⁿ-⋁ _ _ 1)
  (dirProdGroupIso {B = trivialGroup}
    (invGroupIso (Hⁿ-Sⁿ≅ℤ 1))
    ((Hⁿ-⋁ _ _ 1)  □ dirProdGroupIso (Hⁿ-S¹≅0 0) (Hⁿ-S¹≅0 0) □ rUnitGroupIso)
  □ rUnitGroupIso)

private
  open import Cubical.Data.Int
  open import Cubical.Foundations.Equiv
  open import Cubical.Data.Sigma
  to₂ : coHom 2 S²⋁S¹⋁S¹ → Int
  to₂ = GroupHom.fun (GroupIso.map H²-S²⋁S¹⋁S¹)
  from₂ : Int → coHom 2 S²⋁S¹⋁S¹
  from₂ = GroupIso.inv H²-S²⋁S¹⋁S¹

  to₁ : coHom 1 S²⋁S¹⋁S¹ → Int × Int
  to₁ = GroupHom.fun (GroupIso.map H¹-S²⋁S¹⋁S¹)
  from₁ : Int × Int → coHom 1 S²⋁S¹⋁S¹
  from₁ = GroupIso.inv H¹-S²⋁S¹⋁S¹

  to₀ : coHom 0 S²⋁S¹⋁S¹ → Int
  to₀ = GroupHom.fun (GroupIso.map H⁰-S²⋁S¹⋁S¹)
  from₀ : Int → coHom 0 S²⋁S¹⋁S¹
  from₀ = GroupIso.inv H⁰-S²⋁S¹⋁S¹

{-
-- Computes (a lot slower than for the torus)
test : to₁ (from₁ (1 , 0) +ₕ from₁ (0 , 1)) ≡ (1 , 1)
test = refl

-- Does not compute:
test2 : to₂ (from₂ 0) ≡ 0
test2 = refl
-}

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
open import Agda.Builtin.Size

mutual

  data Unit (i : Size) : Set where
    c : Unit′ i → Unit i

  record Unit′ (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → Unit j

open Unit′ public

tail : Unit ∞ → Unit ∞
tail (c x) = force x

u : (∀ {i} → Unit′ i → Unit i) →
    ∀ {i} → Unit i
u cons = tail (cons λ { .force → u cons })

bad : Unit ∞
bad = u c


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

open import HoTT

-- custom pushout for Blakers-Massey

module homotopy.blakersmassey.Pushout {i j k}
  {A : Type i} {B : Type j} (Q : A → B → Type k) where

bmspan : Span {i} {j} {lmax i (lmax j k)}
bmspan = span A B (Σ A λ a → Σ B λ b → Q a b) fst (fst ∘ snd)

BMPushout : Type (lmax i (lmax j k))
BMPushout = Pushout bmspan

bmleft : A → BMPushout
bmleft = left

bmright : B → BMPushout
bmright = right

bmglue : ∀ {a b} → Q a b → bmleft a == bmright b
bmglue {a} {b} q = glue (a , b , q)

module BMPushoutElim {l} {P : BMPushout → Type l}
  (bmleft* : (a : A) → P (bmleft a)) (bmright* : (b : B) → P (bmright b))
  (bmglue* : ∀ {a b} (q : Q a b) → bmleft* a == bmright* b [ P ↓ bmglue q ]) where

  private
    module P = PushoutElim {d = bmspan} {P = P}
      bmleft* bmright* (λ c → bmglue* (snd (snd c)))

  f = P.f

  glue-β : ∀ {a b} (q : Q a b) → apd f (bmglue q) == bmglue* q
  glue-β q = P.glue-β (_ , _ , q)

BMPushout-elim = BMPushoutElim.f

module BMPushoutRec {l} {D : Type l}
  (bmleft* : A → D) (bmright* : B → D)
  (bmglue* : ∀ {a b} (q : Q a b) → bmleft* a == bmright* b) where

  private
    module P = PushoutRec {d = bmspan} {D = D}
      bmleft* bmright* (λ c → bmglue* (snd (snd c)))

  f = P.f

  glue-β : ∀ {a b} (q : Q a b) → ap f (bmglue q) == bmglue* q
  glue-β q = P.glue-β (_ , _ , q)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

-- The category build from ObjectRestriction can be done so Functorially

module Categories.Functor.Construction.ObjectRestriction where

open import Level
open import Data.Product using (proj₁)
open import Relation.Unary using (Pred)
open import Function using () renaming (id to id→)

open import Categories.Category.Core
open import Categories.Category.Construction.ObjectRestriction
open import Categories.Functor.Core
open import Categories.Functor.Properties using (Faithful; Full)

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

RestrictionFunctor : {ℓ′ : Level} → (C : Category o ℓ e) → (E : Pred (Category.Obj C) ℓ′) → Functor (ObjectRestriction C E) C
RestrictionFunctor C E = record
  { F₀ = proj₁
  ; F₁ = id→
  ; identity = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈ = id→
  }
  where
  open Category C

RF-Faithful : {E : Pred (Category.Obj C) ℓ′} → Faithful (RestrictionFunctor C E)
RF-Faithful _ _ = id→

RF-Full : {E : Pred (Category.Obj C) ℓ′} → Full (RestrictionFunctor C E)
RF-Full {C = C} = record
  { from = record
    { _⟨$⟩_ = id→
    ; cong = id→
    }
  ; right-inverse-of = λ _ → Category.Equiv.refl C
  }

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:
open import Data.Nat using (_+_; _*_; zero; suc; ℕ)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; _≢_; refl; cong)
import Data.Nat.Properties
open Data.Nat.Properties.SemiringSolver
  using (solve; _:=_; con; var; _:+_; _:*_; :-_; _:-_)
open PropEq.≡-Reasoning

lem1 : (4 + 6 ≡ 10)
lem1 = refl

lem3 : (x : ℕ) → (2 * (x + 4) ≡ 8 + 2 * x)
lem3 = solve 1 (λ x' → con 2 :* (x' :+ con 4) := con 8 :+ con 2 :* x') refl

sum : ℕ → ℕ
sum zero    = 0
sum (suc n) = 1 + 2 * n + sum n

theorem : (n : ℕ) → (sum n ≡ n * n)
theorem 0       = refl
theorem (suc p) =
  begin
    sum (suc p)
  ≡⟨ refl ⟩
    1 + 2 * p + sum p
  ≡⟨ cong (λ x → 1 + 2 * p + x)  (theorem p)⟩
    1 + 2 * p + p * p
  ≡⟨ solve 1 (λ p → con 1 :+ con 2 :* p :+ p :* p := (con 1 :+ p) :* (con 1 :+ p)) refl p ⟩
    (1 + p) * (1 + p)
  ≡⟨ refl ⟩
    (suc p) * (suc p)
  ∎


text:
-- test for pattern matching on Strings
module StringPattern where

open import Common.IO
open import Common.Unit
open import Common.String

f : String → String
f "bla" = "found-bla"
f x = x

-- expected:
-- no-bla
-- found-bla
main : IO Unit
main =
  putStrLn (f "no-bla") ,,
  putStrLn (f "bla")

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Issue183 where

postulate A : Set

T : Set
T = A → A

data L (A : Set) : Set where

data E (x : T) : T → Set where
  e : E x x

foo : (f : A → A) → L (E f (λ x → f x))
foo = λ _ → e

-- Previously:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Translation/AbstractToConcrete.hs:705
-- Should now give a proper error message.

-- E (_8 f) (_8 f) !=< L (E f f) of type Set
-- when checking that the expression e has type L (E f f)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Type.Proofs where

open import Logic
import      Lvl
open import Type

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 --rewriting #-}

module Sharp where
  open import Basics
  open import Flat

  open import lib.NType2
  open import lib.Equivalence2
  open import lib.types.Modality

  -- --------------------------------------------------------------------------------------
  -- Postulating the ♯ Modality
  -- --------------------------------------------------------------------------------------
  postulate
    -- Here, I've tried to implement the rules for ♯ as in Shulman as closely as possible
    -- to the sequents in Figure 3 of Section 3.

    -- I'm pretty convinced now that this approach will work
    -- However, as currently (02/18/19) rewrite rules do not see the ♭ modality,
    -- it is not fully operational (and, clearly, has not been cleaned up).

    -- The litmus is proving the lexness of ♯ along the lines of Shulman 3.7

    {-
      We implement the ♯ typing operations in two ways.

      First, naively, as follows:
    -}

    -- Rule 1/5: Given a type A, we may form ♯ A
    ♯ : {i : ULevel} → Type i → Type i

    -- Rule 2/5: Given an a : A, we may form a^♯ : ♯ A
    _^♯ : {i : ULevel} {A : Type i} → A → ♯ A

    -- Rule 3/5: Given a crisp a :: ♯ A, we may form a ↓♯ : A
    _↓♯ : {@♭ i : ULevel} {@♭ A : Type i} → ♯ A ::→ A

    {-
      Rule 4/5
      Given a :: A, we have that (a ^♯) ↓♯ ≡ a.

      Δ | ∙ ⊢ a : A
      -------------------------
      Δ | Γ ⊢ (a ^♯) ↓♯ ≡ a : A

      A and a are crisp, but we can have any other context Γ appear
      which is fine, we just don't mention it.
    -}
    ^↓♯ : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : A)
          → ((a ^♯) ↓♯) ↦ a
    {-# REWRITE ^↓♯ #-}

    {-
      Rule 5/5
      Given a : ♯ A in any context, we have (a ↓♯) ^♯ ≡ a

      Δ | Γ ⊢ a : ♯ A
      ---------------
      Δ | Γ ⊢ (a ↓♯) ^♯ ≡ a : ♯ A

      Here we can do this in any context, but for agda that might mean
      "factoring through" the ptwise operations first...

      [WARNING] This implementation needs A to be crisp, and so doesn't
                express the above sequent (I think...)
    -}
    ↓^♯ : {@♭ i : ULevel} {@♭ A : Type i} (@♭ a : ♯ A)
          → ((a ↓♯) ^♯) ↦ a
    {-# REWRITE ↓^♯ #-}

    {-
      Now, we will postulate "pointwise" versions of the above operations which
      take in an additional crisp "context" Γ or Δ. The name Γ or Δ is chosen to match
      the role of the explicit "context" with its analogy in Shulman.

      In each of these, the context either becomes cohesive or not, according to the
      rules from Shulman (which are reproduced here for comparison).
    -}

    {-
      Rule 1/5, pointwise version
      If one has a crisp context Γ and a type A which depends crisply on Γ,
      Then one may form ♯ A which depends cohesively on Γ.

      Or, read backwards, to construct ♯ A in the context Γ, it suffices to assume
      That every variable x : Γ appearing in A is crisp.

      Δ, Γ | ∙ ⊢ A : Type
      -------------------
      Δ | Γ  ⊢ ♯ A : Type
    -}
    -- compare to ♯ : {i : ULevel} → Type i → Type i
    ♯-ptwise : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
               (A : Γ ::→ Type j)
               → (Γ → Type j)

    {-
      We relate the pointwise # with the naive one in the obvious way.

      That is, if we apply a pointwise operation to a crisp variable of the "context",
      this is the same as applying the naive operation pointwise to that variable.

      We take this sameness to be a judgemental equality, implemented as a rewrite rule.
    -}

    ♯-law : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
             (A : Γ ::→ Type j) (@♭ x : Γ)
             → (♯-ptwise A) x ↦ ♯ (A x)
    {-# REWRITE ♯-law #-}

    {-
      Rule 2/5, pointwise version
      If one has a : A in a crisp context Γ,
      one may form a ^♯ : ♯ A in the cohesive context Γ.

      Δ, Γ | ∙ ⊢ a : A
      -------------------
      Δ | Γ ⊢ a ^♯ : ♯ A
    -}
    ^♯-ptwise : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
                {A : Γ ::→ Type j} (a : (@♭ x : Γ) → A x)
                → (x : Γ) → (♯-ptwise A) x

    {-
      Relate the pointwise ^# with the naive one
    -}
    -- ^♯-law : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
    --           {A : Γ ::→ Type j} (a : (@♭ x : Γ) → A x)
    --           (@♭ x : Γ) → (^♯-ptwise a) x ↦ ((a x) ^♯)
    -- {-# REWRITE ^♯-law #-}

    {-
      Rule 3/5, pointwise version
      If one has a :: ♯ A in a crisp context Γ,
      one may form a ↓♯ : A, also in a crisp context Γ

      Δ | ∙ ⊢ a : ♯ A
      ---------------
      Δ | Γ ⊢ a ↓♯ : A

      It seems to me that to have a crisp variable of ♯ A requires A to be crisp...
      But this pointwise definition one doesn't. It just requires that the context
      is crisp.
    -}
    ↓♯-ptwise : {@♭ i : ULevel} {@♭ Δ : Type i} {j : ULevel} {A : Δ ::→ Type j}
                (a : (@♭ x : Δ) → (♯-ptwise A) x)
                → (@♭ x : Δ) → A x

    {-
      Rule 4/5, pointwise version
    -}
    ^↓♯-ptwise : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
                {A : Γ ::→ Type j} (a : (@♭ x : Γ) → A x) (@♭ x : Γ)
                → (((^♯-ptwise a) x) ↓♯) ↦ a x

    {-
      Rule 5/5, pointwise version
      I'm having a difficulty implementing the ptwise version of ↓^♯ that will fire
      whether or not A and a are crisp.
      I think this is because if they are, it is a special case of the ↓^♯ rule,
      But it is not strictly more general, since it keeps track of the "explicit context" Δ

      Or, if I take everything in ↓♯-ptwise to be crisp, then it doesn't typecheck at this
      generality.
    -}
    ↓^♯-ptwise : {@♭ i : ULevel} {j : ULevel} {@♭ Δ : Type i} {A : Δ ::→ Type j}
                 (a : (@♭ x : Δ) → (♯-ptwise A) x) (@♭ x : Δ)
                 → (((↓♯-ptwise a) x) ^♯) ↦ a x
    --                                      ^^^ : (♯-ptwise A) x
    --                ^^^^^^^^^^^               : (@♭ x : Δ) → A x
    --              ^^^^^^^^^^^^^^^^            : A x
    --             ^^^^^^^^^^^^^^^^^^^^^        : # (A x)
    {-# REWRITE ↓^♯-ptwise #-}

    -- [WARNING] When normalizing λ A x → (^♯-ptwise a) x, the rewrite ^♯-law will fire
    -- turning it into ((a x) ^♯), which is ill typed on cohesive x : Γ (and the typechecker
    -- complains)

    ↓♯-law : {@♭ i : ULevel} {@♭ Δ : Type i} {@♭ j : ULevel} {@♭ A : Δ ::→ Type j}
              (@♭ a : (@♭ x : Δ) → (♯-ptwise A) x)
              (@♭ x : Δ) → (↓♯-ptwise a) x ↦ ((a x) ↓♯)
    {-# REWRITE ↓♯-law #-}

    {-
      Finally, we define some convenient notation for the ptwise operations.

      To see how these work in practice, see below.
    -}
  syntax ♯-ptwise (λ γ → A) ctx = let♯ γ ::= ctx in♯-♯ A

  syntax ^♯-ptwise (λ γ → a) ctx = let♯ γ ::= ctx in♯ a ^^♯

  ^♯-ptwise-explicit : {@♭ i : ULevel} {@♭ Γ : Type i} {j : ULevel}
                       (A : Γ ::→ Type j) (a : (@♭ x : Γ) → A x)
                       → (x : Γ) → (♯-ptwise A) x
  ^♯-ptwise-explicit A = ^♯-ptwise {A = A}
  syntax ^♯-ptwise-explicit A (λ γ → t) ctx = let♯ γ ::= ctx in♯ t ^^♯-in-family A

  syntax ↓♯-ptwise (λ γ → a) ctx = let♯ γ ::= ctx in♯ a ↓↓♯

  -- ----------------------------------------------------------------------------------------------
  -- End of Postulates
  -- ----------------------------------------------------------------------------------------------

  -- We have to leave the universe levels out and assume they are crisp,
  -- otherwise the "context record" becomes large.
  -- It shouldn't matter tho, since ULevel is discrete.
  module _ {@♭ i j : ULevel} where
    private
      record Γ : Type (lsucc (lmax i j)) where
        constructor ctx
        field
          ᶜA   : Type i
          ᶜB   : Type j
          ᶜf   : ᶜA → ᶜB
          ᶜa   : ♯ ᶜA
      open Γ

    -- Functoriality of ♯
    ♯→ : {A : Type i} {B : Type j}
       (f : A → B) → (♯ A) → (♯ B)
    ♯→ {A} {B} f a =
      let♯ γ ::= (ctx A B f a) in♯
        (ᶜf γ (ᶜa γ ↓♯)) ^^♯ -- (f (a ↓♯)) ^♯

    -- The naturality square of the unit (judgemental!)
    ♯→-nat : {A : Type i} {B : Type j} (f : A → B)
             (a : A) → ((f a) ^♯) == ((♯→ f) (a ^♯))
    ♯→-nat {A} {B} f a = refl

  -- ♯-elmination (Shulman Theorem 3.4)
  {-
    The general form of these definitions is:
    Take the context (or the part of the context) you want to make crisp,
    and make a private record Γ with fields ᶜx for every variable x in the context.
    Then use the let♯ notation to crispify in the context.
  -}
  module _ {@♭ i j : ULevel} where
    private
      record Γ : Type (lsucc (lmax i j)) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜB : (♯ ᶜA) → Type j
          ᶜf : (a : ᶜA) → ♯ (ᶜB (a ^♯))
          ᶜa : ♯ ᶜA
      open Γ

    ♯-elim : {A : Type i} (B : ♯ A → Type j)
             (f : (a : A) → ♯ (B (a ^♯)))
             → ((a : ♯ A) → ♯ (B a))
    ♯-elim {A} B f a =
      let♯ γ ::= (ctx A B f a) in♯
        (ᶜf γ (ᶜa γ ↓♯)) ↓♯ ^^♯
    syntax ♯-elim B (λ x → t) a = let♯ x ^♯:= a in♯ t in-family B

    -- Elimination with implicit family,
    ♯-elim' : {A : Type i} {B : ♯ A → Type j}
              (f : (a : A) → ♯ (B (a ^♯)))
              → ((a : ♯ A) → ♯ (B a))
    ♯-elim' {A} {B} f a = ♯-elim {A} B f a
    syntax ♯-elim' (λ x → t) a = let♯ x ^♯:= a in♯ t

    -- Crisp eliminators
    ♯-elim-crisp : {@♭ A : Type i} (@♭ B : ♯ A → Type j)
                   (f : (@♭ a : A) → ♯ (B (a ^♯)))
                   → (@♭ a : ♯ A) → ♯ (B a)
    ♯-elim-crisp B f a =
      let♯ ᶜf ::= f in♯ ((ᶜf (a ↓♯)) ↓♯) ^^♯
    syntax ♯-elim-crisp B (λ x → t) a = let♯ x ^♯::= a in♯ t in-family B

    -- β holds judgementally :)
    ♯-elim-β : {A : Type i} {B : ♯ A → Type j}
               (f : (a : A) → ♯ (B (a ^♯))) (a : A)
               → (♯-elim B f (a ^♯)) == (f a)
    ♯-elim-β f a = refl

    -- ♯-elim is inverse to precomposition by _^♯
    -- This proves that ♯ is a uniquely eliminating modality
    ♯-universal : {A : Type i} (B : ♯ A → Type j)
                  → ((a : ♯ A) → ♯ (B a)) ≃ ((a : A) → ♯ (B (a ^♯)))
    ♯-universal {A} B = equiv to fro to-fro fro-to
      where
        to : (f : (a : ♯ A) → ♯ (B a))
             → (a : A) → ♯ (B (a ^♯))
        to f = f ∘ _^♯

        fro : ((a : A) → ♯ (B (a ^♯))) → ((a : ♯ A) → ♯ (B a))
        fro = ♯-elim B

        to-fro : (f : (a : A) → ♯ (B (a ^♯))) → to (fro f) == f
        to-fro f = refl

        fro-to : (f : (a : ♯ A) → ♯ (B a)) → fro (to f) == f
        fro-to f = refl

  -- A type is codiscrete if the inclusion a ↦ a ^♯ is an equivalence.
  _is-codiscrete : {i : ULevel} (A : Type i) → Type i
  A is-codiscrete = (_^♯ {A = A}) is-an-equiv

  codisc-eq : {i : ULevel} {A : Type i} (p : A is-codiscrete) → A ≃ (♯ A)
  codisc-eq = _^♯ ,_

  un♯ : {i : ULevel} {A : Type i} (p : A is-codiscrete) → ♯ A → A
  un♯ p = <– (codisc-eq p)

  _is-codisc-is-a-prop : {i : ULevel} (A : Type i) → (A is-codiscrete) is-a-prop
  A is-codisc-is-a-prop = is-equiv-is-prop

  -- Shulman Theorem 3.5
  -- ♯ A is codiscrete.
  module _ {@♭ i : ULevel} where
    private
      record Γ : Type (lsucc i) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜa : ♯ (♯ ᶜA)
      open Γ

    ♯-is-codiscrete : (A : Type i) → (♯ A) is-codiscrete
    ♯-is-codiscrete = λ A →
      (_^♯ {A = ♯ A}) is-an-equivalence-because fro is-inverse-by to-fro and fro-to
      where
        fro : {A : Type i} → ♯ (♯ A) → ♯ A
        fro {A} a = let♯ γ ::= (ctx A a) in♯ ((ᶜa γ ↓♯) ↓♯) ^^♯

        to-fro : {A : Type i} → (a : ♯ (♯ A)) → ((fro a) ^♯) == a
        to-fro a = refl

        fro-to : {A : Type i} → (a : ♯ A) → fro (a ^♯) == a
        fro-to a = refl

  {-
  module _ {@♭ i j : ULevel} {@♭ i j : Type i} where
    private
      record Γ : Type (lsucc (lmax i j)) where
        constructor ctx
        field
          ᶜA : Δ ::→ Type j
          ᶜx : Δ
      open Γ
    ♯-ptwise-is-codiscrete : (A : Δ ::→ Type j) (x : Δ)
                             → ((♯-ptwise A) x) is-codiscrete
    ♯-ptwise-is-codiscrete = λ A x →
      {!(_^\# {A = (♯-ptwise A) x}) is-an-equivalence-because fro is-inverse-by to-fro and fro-to!}
      where
        module _ {A : Δ ::→ Type j} {x : Δ} where
          fro : ♯ ((♯-ptwise A) x) → (♯-ptwise A) x
          fro = {!!}

          -- to-fro : (a : ♯ ((♯-ptwise A) x)) → ((fro a) ^♯) == a
         -- to-fro = {!!}

         -- fro-to : ∀ a → fro (a ^♯) == a
         -- fro-to = {!!}
    -}

  module _ {@♭ i j : ULevel} where
    record CTX-uncrisp {@♭ A : Type i} : Type (lsucc (lmax i j)) where
      constructor ctx
      field
        ᶜB : A → Type j
        ᶜf : (@♭ a : A) → ♯ (ᶜB a)
        ᶜa : A

    uncrisp : {@♭ A : Type i} (B : A → Type j)
              → ((@♭ a : A) → ♯ (B a))
              → ((a : A) → ♯ (B a))
    uncrisp B f a =
      let♯ γ ::= (ctx B f a) in♯
        (((ᶜf γ) (ᶜa γ)) ↓♯) ^^♯
      where open CTX-uncrisp

  Π-codisc : {@♭ i j : ULevel} {A : Type i} (B : A → Type j)
                 → ((a : A) → ♯ (B a)) is-codiscrete
  Π-codisc {A = A} B =
    _^♯ is-an-equivalence-because
      (λ f a → let♯ g ^♯:= f in♯ (g a)) is-inverse-by
        (λ _ → refl) and (λ _ → refl)

  -- The map ♯ (x == y) → (x == y) for x y : ♯ A, following RSS Lemma 1.25
  module _ {@♭ i : ULevel} {A : Type i} {x y : ♯ A} where
    private
      constx : ♯ (x == y) → ♯ A
      constx _ = x

      consty : ♯ (x == y) → ♯ A
      consty _ = y

      lemma₀ : (constx ∘ _^♯) == (consty ∘ _^♯)
      lemma₀ = λ= (λ p → p)

      lemma₁ : constx == consty
      lemma₁ = -- constx == consty because they are equalized by _^♯, via the universal prop of ♯
        –>-is-inj (♯-universal (λ (_ : ♯ (x == y)) → A)) constx consty lemma₀

    ♯-=-retract : ♯ (x == y) → x == y
    ♯-=-retract p = app= lemma₁ p

  -- To prove a type is an equivalence, it suffices to give a retract of _^♯
  _is-codiscrete-because_is-retract-by_ : {@♭ i : ULevel} (A : Type i)
                                          (r : ♯ A → A) (p : (a : A) → r (a ^♯)  == a)
                                          → A is-codiscrete
  A is-codiscrete-because r is-retract-by p =
    (_^♯ {A = A}) is-an-equivalence-because r is-inverse-by
        (λ a → -- Given an a : ♯ A, we will show ♯ ((r a)^♯ == a)
             (let♯ b ^♯:= a in♯ -- We suppose a is b ^♯
                   ((ap _^♯ (p b)) ^♯) -- apply p to b to get r (b ^♯) == b,
                                      -- then apply _^♯ to get (r b^♯)^♯ == b^♯
                                      -- then hit it with _^♯ to get ♯ ((r b^♯)^♯ == b^♯)
              in-family (λ (a : ♯ A) → ((r a) ^♯) == a) -- which is ♯ ((r a)^♯ == a) by our hypothesis,
             )  -- and we can strip the ♯ becacuse equality types in ♯ are codiscrete.
          |> (♯-=-retract {x = (r a) ^♯} {a})
        )
      and p

  -- We follow RSS Lemma 1.25
  =-is-codiscrete : {@♭ i : ULevel} {A : Type i} (x y : ♯ A)
                    → (x == y) is-codiscrete
  =-is-codiscrete {A = A} x y =
   (x == y) is-codiscrete-because ♯-=-retract is-retract-by proof
    where
      abstract -- UNFINISHED
        proof : (p : x == y) → (♯-=-retract (p ^♯)) == p
        proof = trust-me
          where postulate trust-me : (p : x == y) → (♯-=-retract (p ^♯)) == p

  ♯-modality : {@♭ i : ULevel} → Modality i
  ♯-modality {i} = record
                 { is-local = _is-codiscrete
                 ; is-local-is-prop = λ {A} → A is-codisc-is-a-prop
                 ; ◯ = ♯
                 ; ◯-is-local = λ {A} → ♯-is-codiscrete A
                 ; η = _^♯
                 ; ◯-elim = λ {A} {B} p f a → un♯ (p a) (♯-elim B (λ a → (f a) ^♯) a)
                 ; ◯-elim-β = λ {A} {B} p f a → <–-inv-l (codisc-eq (p (a ^♯))) (f a)
                 ; ◯-=-is-local = =-is-codiscrete
                 }

  _is-infinitesimal : {@♭ i : ULevel} → Type i → Type i
  _is-infinitesimal = Modality.is-◯-connected ♯-modality

  ♯→e : {@♭ i : ULevel} {A B : Type i} → A ≃ B → (♯ A) ≃ (♯ B)
  ♯→e = Modality.◯-emap ♯-modality

  ♯-Σ : ∀ {@♭ i} {A : Type i} (B : A → Type i)
        → A is-codiscrete → ((a : A) → (B a) is-codiscrete)
        → (Σ A B) is-codiscrete
  ♯-Σ {i} = (Modality.Σ-is-local {i}) ♯-modality

  ♯-Π : ∀ {@♭ i} {A : Type i} {B : A → Type i} (w : (a : A) → (B a) is-codiscrete)
        → (Π A B) is-codiscrete
  ♯-Π {i} = (Modality.Π-is-local {i}) ♯-modality

  -- Theorem 6.22 of Shulman
  -- Points of ♯ A are the points of A, and ♯ of the points of A is ♯ A.
  ♭♯-eq : {@♭ i : ULevel} {@♭ A : Type i} → ♭ (♯ A) ≃ ♭ A
  ♭♯-eq {A = A} = equiv to fro to-fro fro-to
    where
      to : ♭ (♯ A) → ♭ A
      to (a ^♭) = (a ↓♯) ^♭

      fro : ♭ A → ♭ (♯ A)
      fro (a ^♭) = (a ^♯) ^♭

      to-fro : (a : ♭ A) → to (fro a) == a
      to-fro (a ^♭) = refl

      fro-to : (a : ♭ (♯ A)) → fro (to a) == a
      fro-to (a ^♭) = ♭-ap _^♭ refl

  ♯♭-eq : {@♭ i : ULevel} {@♭ A : Type i} → ♯ (♭ A) ≃ ♯ A
  ♯♭-eq {A = A} = equiv to fro to-fro fro-to
    where
      to : ♯ (♭ A) → ♯ A
      to a =
        let♯ u ^♯:= a in♯
          let♭ v ^♭:= u in♭ (v ^♯)

      fro : ♯ A → ♯ (♭ A)
      fro a =
        let♯ u ^♯:= a in♯
          let♯ v ::= u in♯ (v ^♭) ^^♯

      abstract
        to-fro : (a : ♯ A) → to (fro a) == a
        to-fro a = -- It suffices to show ♯ (to fro a == a),
          (let♯ u ^♯:= a in♯ -- which lets us assume a = u^♯
            refl ^♯ -- so that the equality follows judgementally.
          in-family (λ a → to (fro a) == a))
          |> ♯-=-retract

        fro-to : (a : ♯ (♭ A)) → fro (to a) == a
        fro-to a = -- It suffices to show ♯ (fro to a == a),
          (let♯ u ^♯:= a in♯ -- which lets us assume a = u^♯ with u : ♭ A,
            (let♭ v ^♭:= u in♭ -- so we can assume u = v^♭,
                  refl ^♯ -- so that the equality follows judgementally.
             in-family (λ u → ♯ (fro (to (u ^♯)) == (u ^♯))))
           in-family (λ a → fro (to a) == a))
          |> ♯-=-retract

  -- Theorem 6.27 of Shulman
  -- The adjunction between ♭ and ♯
  ♭♯-adjoint : {@♭ i j : ULevel} {@♭ A : Type i} {@♭ B : A → Type j}
               → ♭ ((a : ♭ A) → B (a ↓♭)) ≃ ♭ ((a : A) → ♯ (B a))
  ♭♯-adjoint {A = A} {B = B} = equiv to fro to-fro fro-to
    where
      to :  ♭ ((a : ♭ A) → B (a ↓♭)) →  ♭ ((a : A) → ♯ (B a))
      to (f ^♭) = (λ a → let♯ u ::= a in♯ f (u ^♭) ^^♯) ^♭

      fro :  ♭ ((a : A) → ♯ (B a)) →  ♭ ((a : ♭ A) → B (a ↓♭))
      fro (f ^♭) = (λ a → let♭ u ^♭:= a in♭ ((f u) ↓♯) in-family (λ a → B (a ↓♭))) ^♭

      to-fro : ∀ f → to (fro f) == f
      to-fro (f ^♭) = refl

      fro-to : ∀ f → fro (to f) == f
      fro-to (f ^♭) =
        ♭-ap _^♭ -- We can strip ^♭ from both sides,
          ( λ= (λ a →  let♭ u ^♭:= a in♭ -- then, working at a crisp argument u,
                  refl -- we find both sides are judgementally the same.
               in-family (λ a → ♭-elim (λ a₁ → B (a₁ ↓♭)) (λ (@♭ u : _) → f (u ^♭)) a == f a)  )
            ) -- The "in family" gibberish just reminds agda what we are trying to prove.

  -- Shulman Theorem 3.7
  -- ♯ is left exact, in that x^♯ == y^♯ is ♯ (x == y)
  module _ {@♭ i : ULevel} where
    private
      record CTX-code : Type (lsucc i) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜx : ♯ ᶜA
          ᶜy : ♯ ᶜA

    code : {A : Type i} → ♯ A → ♯ A → Type i
    code {A} x y =
      let♯ γ ::= (ctx A x y) in♯-♯ (((ᶜx γ) ↓♯) == ((ᶜy γ) ↓♯))
      where open CTX-code

    private
      record CTX-r : Type (lsucc i) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜx : ♯ ᶜA

    r : {A : Type i} (x : ♯ A) → code x x
    r {A} x =
      let♯ γ ::= (ctx A x) in♯ (idp {a = (ᶜx γ) ↓♯}) ^^♯
      where open CTX-r
       -- for some reason, I can't use refl here, I need idp???

    encode : {A : Type i} {a b : ♯ A} → (a == b) → code a b
    encode {A} {a} {b} p = transport (λ y → code a y) p (r a)

    decode : {A : Type i} {a b : ♯ A} → code a b → (a == b)
    decode {A} {a} {b} = -- It suffices to give ♯ (code a b → a == b) by lemma.
      lemma a b (decode' a b)
      where
        lemma : {A : Type i} (a b : ♯ A)
                → ♯ (code a b → (a == b))
                → code a b → (a == b)
        lemma a b p e =
          ♯-=-retract $ -- it suffices to show ♯ (a == b)
            let♯ q ^♯:= p in♯ ((q e) ^♯) -- so we can assume p is of the form q ^♯.

        decode' : {A : Type i} (a b : ♯ A) → ♯ (code a b → (a == b))
        decode' {A} a b =
          let♯ u ^♯:= a in♯ -- By ♯-elim, we can assume a and b are of the form
            let♯ v ^♯:= b in♯ -- u ^♯ and v ^♯, and we'll give
                                 -- code (u ^♯) (v ^♯) → (u ^♯) == (v ^♯).
                   (λ p → ♯-=-retract -- Assuming a code p, it suffices to give
                                                    -- ♯ (u ^♯ == v ^♯).
                   (let♯ q ^♯:= p in♯ ((ap _^♯ q)^♯)) )^♯ -- So, we let p be q^♯
                                                          -- with q : u == v, and then
                                                          -- push this through the unit.
            in-family (λ b' → code (u ^♯) b' → (u ^♯) == b')
          in-family (λ a' → code a' b → a' == b)

    private -- context for encode-decode'
      record CTX-encode-decode : Type (lsucc i) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜa : ♯ ᶜA
          ᶜb : ♯ ᶜA
          -- ᶜp : code ᶜa ᶜb
      open CTX-encode-decode
    {-
    encode-decode' : {A : Type i} {a b : ♯ A} → ♯ ((encode {a = a}{b = b})∘ decode == (idf (code a b)))
    encode-decode' {A} {a} {b} =
      let♯ γ ::= (ctx A a b) in♯
        {!let♯ u ^♯:= (ᶜa γ) in♯
           ?
         in-family (λ a' → (encode {a = a'}{b = ᶜb γ})∘ decode == (idf (code a' (ᶜb γ))))!}
      ^^♯-in-family (λ γ' → (encode {a = ᶜa γ'}{b = ᶜb γ'})∘ decode == (idf (code (ᶜa γ') (ᶜb γ'))))

    -- [WARNING] I get an error here complaining about A in (a ↓♯) == (b ↓♯) if doing this at
    -- p : code a b (I believe this to be because rewrite rules do not see the ♭ modality)
    encode-decode : {A : Type i} {a b : ♯ A} → (encode {a = a}{b = b})∘ decode == (idf (code a b))
    encode-decode {A} {a} {b} =
      λ= (λ p → {!!})

    -}

  -- For now, we'll just postulate it
  ♯-=-compare : {@♭ i : ULevel} {A : Type i} {x y : A}
                → ♯ (x == y) → (x ^♯) == (y ^♯)
  ♯-=-compare {x = x} {y = y} p =
    ♯-=-retract  $ -- it suffices to give ♯ (x ^♯ == y ^♯)
      let♯ q ^♯:= p in♯ -- in which case we may assume p = q ^♯ with q : x == y
        ((ap _^♯ q) ^♯) -- and so we can push this through.
  module _ {@♭ i : ULevel} where
    private
      record CTX-♯-lex : Type (lsucc i) where
        constructor ctx
        field
          ᶜA : Type i
          ᶜx : ᶜA
          ᶜy : ᶜA
    postulate
      ♯-lex : {A : Type i} {x y : A}
              → (♯-=-compare {x = x} {y = y}) is-an-equiv

    ♯-lex-eq : {A : Type i} {x y : A}
               → (♯ (x == y)) ≃ ((x ^♯) == (y ^♯))
    ♯-lex-eq {A}{x}{y} = ♯-=-compare , ♯-lex

    test : {A : Type i} {x y : ♯ A}
           → ♯ ((x ^♯) == (y ^♯) → ♯ (x == y))
    test {A} {x} {y} =
      let♯ γ ::= (ctx (♯ A) x y) in♯
        (λ p → let♯ q ::= p in♯
                  (♭-ap _↓♯ q)
                ^^♯-in-family (λ _ → (ᶜx γ == ᶜy γ)))
      ^^♯-in-family (λ γ → ((ᶜx γ) ^♯) == ((ᶜy γ) ^♯) → ♯ ((ᶜx γ) == (ᶜy γ)))
      where open CTX-♯-lex

  ♯-has-level-is-codisc : {@♭ i : ULevel} {A : Type i}
                          {n : ℕ₋₂} → (has-level n (♯ A)) is-codiscrete
  ♯-has-level-is-codisc {i} {A} {n} = replete helper (has-level-def-eq ⁻¹)
    where
      replete = (Modality.local-is-replete {i}) ♯-modality

      helper : {A : Type i}
               {n : ℕ₋₂} → (has-level-aux n (♯ A)) is-codiscrete
      helper {A} {⟨-2⟩} =
        ♯-Σ (λ x → (y : ♯ A) → x == y) (♯-is-codiscrete A) $
          λ x → ♯-Π (λ y → =-is-codiscrete x y)

      helper {A} {n = S n} =
        ♯-Π (λ x →
          ♯-Π (λ y →
            replete (replete (helper {A = (x == y)} {n}) (has-level-def-eq ⁻¹))
              (≃-preserves-level-eq ((codisc-eq $ =-is-codiscrete x y) ⁻¹))))

  ♯-preserves-level : {@♭ i : ULevel} {A : Type i}
                      {n : ℕ₋₂} (p : has-level n A)
                      → has-level n (♯ A)
  ♯-preserves-level {i} {A} {⟨-2⟩} p =
    has-level-in ( ((contr-center p)^♯) ,
      (λ y → ♯-=-retract $ -- It suffices to prove ♯ (center == y)
              let♯ u ^♯:= y in♯ -- so we can assume y is u ^♯
                ap _^♯ (contr-path p u) ^♯ -- and then apply _^♯ to the contractibility of A.
              in-family (λ y → ((contr-center p) ^♯) == y))
      )
  ♯-preserves-level {i} {A} {S n} p =
    has-level-in
      (λ x y → -- Given x y : ♯ A, we need to show that x == y has level n.
           ≃-preserves-level ((codisc-eq (=-is-codiscrete x y))⁻¹) lemma
      ) -- since x == y is ♯ (x == y), it will suffice to show that has level n.
    where
      lemma : {x y : ♯ A} →  has-level n (♯ (x == y))
      lemma {x} {y} = -- Since has-level is codiscrete on codiscretes,
        un♯ ♯-has-level-is-codisc $ -- we can let x and y be u^♯ and v^♯.
          let♯ u ^♯:= x in♯ -- Then, we use the lex-ness of ♯ and a bit of jiggling
             let♯ v ^♯:= y in♯ -- to show that we might as well prove the result of
                (≃-preserves-level (e u v) -- ♯ (u == v), which we can do by recursing.
                  (♯-preserves-level (has-level-apply p u v)))^♯
              in-family (λ y → has-level n (♯ ((u ^♯) == y)))
           in-family (λ x → has-level n (♯ (x == y)))
        where
          e : (u v : A) → ♯ (u == v) ≃ ♯ ((u ^♯) == (v ^♯))
          e u v = ♯ (u == v)
                ≃⟨ codisc-eq (♯-is-codiscrete (u == v)) ⟩
                  ♯ (♯ (u == v))
                ≃⟨ ♯→e ♯-lex-eq ⟩
                  ♯ ((u ^♯) == (v ^♯))
                ≃∎

  ♯ₙ : {@♭ i : ULevel} {n : ℕ₋₂}
       → (A : n -Type i) → (n -Type i)
  ♯ₙ A = (♯ (fst A)) , ♯-preserves-level (snd A)

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
------------------------------------------------------------------------------
-- Example of a nested recursive function using the Bove-Capretta
-- method
------------------------------------------------------------------------------

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

-- From: Bove, A. and Capretta, V. (2001). Nested General Recursion
-- and Partiality in Type Theory. In: Theorem Proving in Higher Order
-- Logics (TPHOLs 2001). Ed. by Boulton, R. J. and Jackson,
-- P. B. Vol. 2152. LNCS. Springer, pp. 121–135.

module FOT.FOTC.Program.Nest.NestBC-SL where

open import Data.Nat renaming ( suc to succ )
open import Data.Nat.Properties

open import Induction
open import Induction.Nat

open import Relation.Binary

------------------------------------------------------------------------------
-- The original non-terminating function.

{-# TERMINATING #-}
nestI : ℕ → ℕ
nestI 0        = 0
nestI (succ n) = nestI (nestI n)

-- ≤′-trans : Transitive _≤′_
-- ≤′-trans i≤′j j≤′k = ≤⇒≤′ (NDTO.trans (≤′⇒≤ i≤′j) (≤′⇒≤ j≤′k))

mutual
  -- The domain predicate of the nest function.
  data NestDom : ℕ → Set where
    nestDom0 : NestDom 0
    nestDomS : ∀ {n} → (h₁ : NestDom n) →
               (h₂ : NestDom (nestD n h₁)) →
               NestDom (succ n)

  -- The nest function by structural recursion on the domain predicate.
  nestD : ∀ n → NestDom n → ℕ
  nestD .0        nestDom0             = 0
  nestD .(succ n) (nestDomS {n} h₁ h₂) = nestD (nestD n h₁) h₂

nestD-≤′ : ∀ n → (h : NestDom n) → nestD n h ≤′ n
nestD-≤′ .0        nestDom0             = ≤′-refl
nestD-≤′ .(succ n) (nestDomS {n} h₁ h₂) =
  ≤′-trans (≤′-trans (nestD-≤′ (nestD n h₁) h₂) (nestD-≤′ n h₁))
           (≤′-step ≤′-refl)

-- The nest function is total.
allNestDom : ∀ n → NestDom n
allNestDom = build <′-recBuilder P ih
  where
  P : ℕ → Set
  P = NestDom

  ih : ∀ y → <′-Rec P y → P y
  ih zero     rec = nestDom0
  ih (succ y) rec = nestDomS nd-y (rec (nestD y nd-y) (s≤′s (nestD-≤′ y nd-y)))
    where
    helper : ∀ x → x <′ y → P x
    helper x Sx≤′y = rec x (≤′-step Sx≤′y)

    nd-y : NestDom y
    nd-y = ih y helper

-- The nest function.
nest : ℕ → ℕ
nest n = nestD n (allNestDom n)