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

open import Categories.Category
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Closed

module Categories.Category.Monoidal.Closed.IsClosed.Diagonal
  {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (Cl : Closed M) where

open import Data.Product using (Σ; _,_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality as Π using (Π)

open import Categories.Category.Product
open import Categories.Category.Monoidal.Properties M
open import Categories.Morphism C
open import Categories.Morphism.Properties C
open import Categories.Morphism.Reasoning C
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Bifunctor.Properties
open import Categories.NaturalTransformation hiding (id)
open import Categories.NaturalTransformation.Dinatural hiding (_∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as NI hiding (refl)
import Categories.Category.Closed as Cls

open Closed Cl

private
  open Category C
  module ℱ = Functor
  module ⊗ = Functor ⊗
  α⇒ = associator.from
  α⇐ = associator.to
  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to
  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to

open HomReasoning
open Π.Π
open adjoint renaming (unit to η; counit to ε; Ladjunct to 𝕃; Ladjunct-comm′ to 𝕃-comm′;
 Ladjunct-resp-≈ to 𝕃-resp-≈)

open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl  -- defines diagonal
open import Categories.Category.Monoidal.Closed.IsClosed.L Cl

Lj≈j : ∀ {X Y} → L X Y Y ∘ diagonal.α Y ≈ diagonal.α [ X , Y ]₀
Lj≈j {X} {Y} = begin
  L X Y Y ∘ 𝕃 λ⇒                                            ≈˘⟨ 𝕃-comm′ ⟩
  𝕃 (𝕃 (ε.η Y ∘ id ⊗₁ ε.η Y ∘ α⇒) ∘ 𝕃 λ⇒ ⊗₁ id)            ≈˘⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ (ε.η Y ∘ id ⊗₁ ε.η Y ∘ α⇒) ∘ (𝕃 λ⇒ ⊗₁ id) ⊗₁ id) ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ $ absorb-λ⇒ ⟩
  𝕃 (𝕃 (Radjunct λ⇒))                                       ≈⟨ 𝕃-resp-≈ LRadjunct≈id ⟩
  diagonal.α [ X , Y ]₀                                     ∎
  where
  absorb-λ⇒ : (ε.η Y ∘ id ⊗₁ ε.η {X} Y ∘ α⇒) ∘ (𝕃 λ⇒ ⊗₁ id) ⊗₁ id ≈ Radjunct λ⇒
  absorb-λ⇒ = begin
    (ε.η Y ∘ id ⊗₁ ε.η Y ∘ α⇒) ∘ (𝕃 λ⇒ ⊗₁ id) ⊗₁ id ≈⟨ pull-last assoc-commute-from ⟩
    ε.η Y ∘ id ⊗₁ ε.η Y ∘ 𝕃 λ⇒ ⊗₁ id ⊗₁ id ∘ α⇒     ≈˘⟨ assoc ⟩
    (ε.η Y ∘ id ⊗₁ ε.η Y) ∘ 𝕃 λ⇒ ⊗₁ id ⊗₁ id ∘ α⇒   ≈⟨ refl⟩∘⟨ ⊗.F-resp-≈ (refl , ⊗.identity) ⟩∘⟨refl ⟩
    (ε.η Y ∘ id ⊗₁ ε.η Y) ∘ 𝕃 λ⇒ ⊗₁ id ∘ α⇒         ≈⟨ center [ ⊗ ]-commute ⟩
    ε.η Y ∘ (𝕃 λ⇒ ⊗₁ id ∘ id ⊗₁ ε.η Y) ∘ α⇒         ≈⟨ pull-first RLadjunct≈id ⟩
    λ⇒ ∘ id ⊗₁ ε.η Y ∘ α⇒                           ≈⟨ pullˡ unitorˡ-commute-from ⟩
    (ε.η Y ∘ λ⇒) ∘ α⇒                                ≈⟨ pullʳ coherence₁ ⟩
    Radjunct λ⇒ ∎

jL≈i : {X Y : Obj} → [ diagonal.α X , id ]₁ ∘ L X X Y ≈ identity.⇒.η [ X , Y ]₀
jL≈i {X} {Y} = begin
  [ Δ X , id ]₁ ∘ L X X Y                             ≈˘⟨ pushˡ [ [-,-] ]-commute ⟩
  ([ id , 𝕃 inner ]₁ ∘ [ Δ X , id ]₁) ∘ η.η XY        ≈˘⟨ pushʳ (mate.commute₁ (diagonal.α X)) ⟩
  [ id , 𝕃 inner ]₁ ∘ [ id , id ⊗₁ Δ X ]₁ ∘ η.η XY    ≈˘⟨ pushˡ (ℱ.homomorphism [ unit ,-]) ⟩
  𝕃 (𝕃 inner ∘ id ⊗₁ Δ X)                             ≈˘⟨ 𝕃-resp-≈ $ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ inner ∘ (id ⊗₁ Δ X) ⊗₁ id)                  ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ inner∘diag⇒ℝρ ⟩
  𝕃 (𝕃 $ Radjunct ρ⇒)                                 ≈⟨ 𝕃-resp-≈ $ LRadjunct≈id ⟩
  𝕃 ρ⇒                                                ≈˘⟨ identityˡ ⟩
  id ∘ 𝕃 ρ⇒    ∎
  where
  XY = [ X , Y ]₀
  inner = ε.η Y ∘ id ⊗₁ ε.η X ∘ α⇒
  Δ = diagonal.α
  inner∘diag⇒ℝρ : inner ∘ (id ⊗₁ Δ X) ⊗₁ id ≈ Radjunct ρ⇒
  inner∘diag⇒ℝρ = begin
    inner ∘ (id ⊗₁ Δ X) ⊗₁ id                      ≈⟨ pull-last assoc-commute-from ○ ⟺ assoc ⟩
    (ε.η Y ∘ id ⊗₁ ε.η X) ∘ id ⊗₁ Δ X ⊗₁ id ∘ α⇒   ≈⟨ center (⟺ (ℱ.homomorphism (XY ⊗-))) ⟩
    ε.η Y ∘ id ⊗₁ (ε.η X ∘ 𝕃 λ⇒ ⊗₁ id) ∘ α⇒        ≈⟨ refl⟩∘⟨ ℱ.F-resp-≈ (XY ⊗-) RLadjunct≈id ⟩∘⟨refl ⟩
    ε.η Y ∘ id ⊗₁ λ⇒ ∘ α⇒                          ≈⟨ refl⟩∘⟨ triangle ⟩
    Radjunct ρ⇒ ∎

private
  i-η = identity.⇒.η

-- Not about diagonal, but it feels like a waste to start another file just for this
iL≈i : {Y Z : Obj} → [ i-η Y , id ]₁ ∘ L unit Y Z ≈ [ id , i-η Z ]₁
iL≈i {Y} {Z} = begin
  [ i-η Y , id ]₁ ∘ L unit Y Z                       ≈˘⟨ pushˡ [ [-,-] ]-commute ⟩
  ([ id , 𝕃 inner ]₁ ∘ [ i-η Y , id ]₁) ∘ η.η YZ     ≈⟨ ( refl⟩∘⟨ (ℱ.F-resp-≈ [-, YZ ⊗₀ [ unit , Y ]₀ ] identityˡ)) ⟩∘⟨refl ⟩
  ([ id , 𝕃 inner ]₁ ∘ [ 𝕃 ρ⇒ , id ]₁) ∘ η.η YZ      ≈˘⟨ pushʳ (mate.commute₁ (𝕃 ρ⇒)) ⟩
  [ id , 𝕃 inner ]₁ ∘ [ id , id ⊗₁ 𝕃 ρ⇒ ]₁ ∘ η.η YZ  ≈˘⟨ pushˡ (ℱ.homomorphism [ Y ,-]) ⟩
  𝕃 (𝕃 inner ∘ id ⊗₁ 𝕃 ρ⇒)                           ≈˘⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ inner ∘ (id ⊗₁ 𝕃 ρ⇒) ⊗₁ id)                ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ absorb ⟩
  𝕃 (𝕃 $ ε.η Z ∘ ρ⇒)                                ≈⟨ 𝕃-resp-≈ $ ∘-resp-≈ˡ (ℱ.homomorphism [ unit ,-])
                                                                  ○ (assoc ○ ∘-resp-≈ʳ (⟺ identityˡ)) ⟩
  𝕃 ([ id , ε.η Z ]₁ ∘ i-η (YZ ⊗₀ Y))               ≈˘⟨ 𝕃-resp-≈ $ identity.⇒.commute (ε.η Z) ⟩
  𝕃 (i-η Z ∘ ε.η Z)                                  ≈˘⟨ 𝕃-resp-≈ $ ε.commute (i-η Z) ⟩
  𝕃 (Radjunct [ id , i-η Z ]₁)                       ≈⟨ LRadjunct≈id ⟩
  [ id , i-η Z ]₁   ∎
  where
  YZ = [ Y , Z ]₀
  inner = ε.η Z ∘ id ⊗₁ ε.η Y ∘ α⇒
  absorb : inner ∘ (id ⊗₁ 𝕃 ρ⇒) ⊗₁ id ≈ ε.η Z ∘ ρ⇒
  absorb = begin
    inner ∘ (id ⊗₁ 𝕃 ρ⇒) ⊗₁ id                      ≈⟨ pull-last assoc-commute-from ○ ⟺ assoc ⟩
    (ε.η Z ∘ id ⊗₁ ε.η Y) ∘ id ⊗₁ 𝕃 ρ⇒ ⊗₁ id ∘ α⇒   ≈⟨ center (⟺ (ℱ.homomorphism (YZ ⊗-))) ⟩
    ε.η Z ∘ id ⊗₁ (ε.η Y ∘ 𝕃 ρ⇒ ⊗₁ id) ∘ α⇒         ≈⟨ refl⟩∘⟨ ℱ.F-resp-≈ (YZ ⊗-) RLadjunct≈id ⟩∘⟨refl ⟩
    ε.η Z ∘ id ⊗₁ ρ⇒ ∘ α⇒                           ≈⟨ refl⟩∘⟨ coherence₂ ⟩
    ε.η Z ∘ ρ⇒  ∎

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
{- Type class for monads. -}
module CategoryTheory.Monad where

open import CategoryTheory.Categories
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans

-- A monad on a category
record Monad {n} (ℂ : Category n) : Set (lsuc n) where
    open Category ℂ
    field
        -- Underlying endofunctor
        T : Endofunctor ℂ
    open Functor T

    field
        -- || Definitions
        -- Unit / return
        η : I ⟹ T
        -- Multiplication / join
        μ : (T ²) ⟹ T

    module η = _⟹_ η
    module μ = _⟹_ μ
    field
        -- || Laws
        -- Unit on both sides is cancelled by multiplication (unit)
        η-unit1 : ∀ {A : obj} -> (μ.at A) ∘ (η.at (omap A)) ≈ id
        η-unit2 : ∀ {A : obj} -> (μ.at A) ∘ (fmap (η.at A)) ≈ id

        -- Multiplication can be performed on both sides (associativity)
        μ-assoc : ∀ {A : obj} -> (μ.at A) ∘ (μ.at (omap A))
                               ≈ (μ.at A) ∘ (fmap (μ.at A))

ext: agda

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
-- Andreas, 2015-03-16
-- Andreas, 2020-10-26 removed loop during injectivity check

open import Agda.Builtin.Size

-- Note: the assumption of pred is absurd,
-- but still should not make Agda loop.

module _ (pred : ∀ i → Size< i) where

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  wrap : (j : Size< i) → SizeLt i

loop : (d : ∀ i → SizeLt i) → ∀ i → SizeLt i → ⊥
loop d i (wrap j) = loop d j (d j)

-- -- Loops during injectivity check:
-- loop : ∀ i → SizeLt i → ⊥
-- loop i (wrap j) = loop j (wrap (pred j))

d : ∀ i → SizeLt i
d i = wrap (pred i)

absurd : ⊥
absurd = loop d ∞ (d ∞)

_ = FIXME

-- Testcase temporarily mutilated, original error:
--
-- -Issue1428a.agda:..
-- -Functions may not return sizes, thus, function type
-- -(i : Size) → Size< i is illegal
-- -when checking that the expression ∀ i → Size< i is a type
--
-- +Issue1428a.agda:...
-- +Not in scope:
-- +  FIXME at Issue1428a.agda:...
-- +when scope checking FIXME

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
--
-- open import Relation.Binary using (Rel; Setoid; IsEquivalence)
-- open import Level as Lvl using ()

module Structures
  {G F : Set}
  (_≈G_ : G → G → Set)
  (_≈F_ : F → F → Set)
  where

-- import M as M’
open import Algebra.Structures _≈G_
  using (IsAbelianGroup)

open import Algebra.Structures _≈F_
  using (IsCommutativeRing)

open import Relation.Nullary

open import Algebra.FunctionProperties _≈F_ using (Inverse)

record IsField (+ * : F → F → F) (𝟘 𝟙 : F) (- : F → F) (⁻¹ : (a : F) → ¬ (a ≈F 𝟘) → F) : Set where
  field
    isCommutativeRing : IsCommutativeRing + * - 𝟘 𝟙
    *-inverse : Inverse {!   !} {!  ⁻¹  !} {!   !}

record IsVectorSpace

  (+ᵍ : G → G → G)
  (𝟘ᵍ : G)
  (-ᵍ : G → G)

  : Set where

  -- module G =
  field
    G-isAbelianGroup : IsAbelianGroup +ᵍ 𝟘ᵍ -ᵍ
    F-isField : {! Rel  !}
      -- IsAbelianGroup {! +G  !} {!   !} {!   !} {!   !}

max_stars_repo_name: banacorn/linear-algebra

max_issues_repo_name: banacorn/linear-algebra

max_forks_repo_name: banacorn/linear-algebra


text:
module OlderBasicILP.Direct.Gentzen where

open import Common.Context public

-- Propositions of intuitionistic logic of proofs, without ∨, ⊥, or +.

mutual
  infixr 10 _⦂_
  infixl 9 _∧_
  infixr 7 _▻_
  data Ty : Set where
    α_  : Atom → Ty
    _▻_ : Ty → Ty → Ty
    _⦂_ : Box → Ty → Ty
    _∧_ : Ty → Ty → Ty
    ⊤  : Ty

  record Box : Set where
    inductive
    constructor [_]
    field
      {/A} : Ty
      t    : ∅ ⊢ /A

  _⦂⋆_ : ∀ {n} → VCx Box n → VCx Ty n → Cx Ty
  ∅        ⦂⋆ ∅       = ∅
  (ts , t) ⦂⋆ (Ξ , A) = (ts ⦂⋆ Ξ) , (t ⦂ A)

  -- Derivations, as Gentzen-style natural deduction trees.

  infix 3 _⊢_
  data _⊢_ (Γ : Cx Ty) : Ty → Set where
    var      : ∀ {A}              → A ∈ Γ → Γ ⊢ A
    lam      : ∀ {A B}            → Γ , A ⊢ B → Γ ⊢ A ▻ B
    app      : ∀ {A B}            → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
--    multibox : ∀ {n A} {[ss] : VCx Box n} {Ξ : VCx Ty n}
--               → Γ ⊢⋆ [ss] ⦂⋆ Ξ → (u : [ss] ⦂⋆ Ξ ⊢ A)
--               → Γ ⊢ [ u ] ⦂ A
    down     : ∀ {A} {t : ∅ ⊢ A} → Γ ⊢ [ t ] ⦂ A → Γ ⊢ A
    pair     : ∀ {A B}            → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
    fst      : ∀ {A B}            → Γ ⊢ A ∧ B → Γ ⊢ A
    snd      : ∀ {A B}            → Γ ⊢ A ∧ B → Γ ⊢ B
    unit     : Γ ⊢ ⊤

  infix 3 _⊢⋆_
  _⊢⋆_ : Cx Ty → Cx Ty → Set
  Γ ⊢⋆ ∅     = 𝟙
  Γ ⊢⋆ Ξ , A = Γ ⊢⋆ Ξ × Γ ⊢ A

infix 7 _▻◅_
_▻◅_ : Ty → Ty → Ty
A ▻◅ B = (A ▻ B) ∧ (B ▻ A)

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
  mono⊢ η (var i)         = var (mono∈ η i)
  mono⊢ η (lam t)         = lam (mono⊢ (keep η) t)
  mono⊢ η (app t u)       = app (mono⊢ η t) (mono⊢ η u)
--  mono⊢ η (multibox ts u) = multibox (mono⊢⋆ η ts) u
  mono⊢ η (down t)        = down (mono⊢ η t)
  mono⊢ η (pair t u)      = pair (mono⊢ η t) (mono⊢ η u)
  mono⊢ η (fst t)         = fst (mono⊢ η t)
  mono⊢ η (snd t)         = snd (mono⊢ η t)
  mono⊢ η unit            = unit

  mono⊢⋆ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
  mono⊢⋆ {∅}     η ∙        = ∙
  mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Shorthand for variables.

v₀ : ∀ {A Γ} → Γ , A ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ} → (Γ , A) , B ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ} → ((Γ , A) , B) , C ⊢ A
v₂ = var i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ} → Γ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

-- Deduction theorem is built-in.

-- Detachment theorem.

det : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ , A ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

-- Cut and multicut.

cut : ∀ {A B Γ} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut t u = app (lam u) t

multicut : ∀ {Ξ A Γ} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

-- Transitivity.

trans⊢⋆ : ∀ {Γ″ Γ′ Γ} → Γ ⊢⋆ Γ′ → Γ′ ⊢⋆ Γ″ → Γ ⊢⋆ Γ″
trans⊢⋆ {∅}      ts ∙        = ∙
trans⊢⋆ {Γ″ , A} ts (us , u) = trans⊢⋆ ts us , multicut ts u

-- Contraction.

ccont : ∀ {A B Γ} → Γ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ} → Γ , A , A ⊢ B → Γ , A ⊢ B
cont t = det (app ccont (lam (lam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ} → Γ , A , B ⊢ C → Γ , B , A ⊢ C
exch t = det (det (app cexch (lam (lam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ} → Γ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ} → Γ , B ⊢ C → Γ , A ⊢ B → Γ , A ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

-- Useful theorems in functional form.

-- dist : ∀ {A B Ψ Γ} {t : Ψ ⊢ A ▻ B} {u : Ψ ⊢ A}
--        → Γ ⊢ [ t ] ⦂ (A ▻ B) → Γ ⊢ [ u ] ⦂ A
--        → Γ ⊢ [ app (down v₁) (down v₀) ] ⦂ B
-- dist t u = multibox ((∙ , t) , u) (app (down v₁) (down v₀))
--
-- up : ∀ {A Ψ Γ} {t : Ψ ⊢ A}
--      → Γ ⊢ [ t ] ⦂ A
--      → Γ ⊢ [ v₀ ] ⦂ [ t ] ⦂ A
-- up t = multibox (∙ , t) v₀
--
-- distup : ∀ {A B Ψ Γ} {u : Ψ ⊢ A} {t : ∅ , [ u ] ⦂ A ⊢ [ u ] ⦂ A ▻ B}
--          → Γ ⊢ [ t ] ⦂ ([ u ] ⦂ A ▻ B) → Γ ⊢ [ u ] ⦂ A
--          → Γ ⊢ [ app (down v₁) (down v₀) ] ⦂ B
-- distup t u = dist t (up u)
--
-- box : ∀ {A Γ}
--       → (t : ∅ ⊢ A)
--       → Γ ⊢ [ t ] ⦂ A
-- box t = multibox ∙ t

unbox : ∀ {A C Γ} {t : ∅ ⊢ A} {u : ∅ ⊢ C}
        → Γ ⊢ [ t ] ⦂ A → Γ , [ t ] ⦂ A ⊢ [ u ] ⦂ C
        → Γ ⊢ [ u ] ⦂ C
unbox t u = app (lam u) t

-- Useful theorems in combinatory form.

ci : ∀ {A Γ} → Γ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ} → Γ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

-- cdist : ∀ {A B Ψ Γ} {t : Ψ ⊢ A ▻ B} {u : Ψ ⊢ A}
--         → Γ ⊢ [ t ] ⦂ (A ▻ B) ▻ [ u ] ⦂ A ▻ [ app (down v₁) (down v₀) ] ⦂ B
-- cdist = lam (lam (dist v₁ v₀))
--
-- cup : ∀ {A Ψ Γ} {t : Ψ ⊢ A} → Γ ⊢ [ t ] ⦂ A ▻ [ v₀ ] ⦂ [ t ] ⦂ A
-- cup = lam (up v₀)

cdown : ∀ {A Γ} {t : ∅ ⊢ A} → Γ ⊢ [ t ] ⦂ A ▻ A
cdown = lam (down v₀)

-- cdistup : ∀ {A B Ψ Γ} {u : Ψ ⊢ A} {t : ∅ , [ u ] ⦂ A ⊢ [ u ] ⦂ A ▻ B}
--           → Γ ⊢ [ t ] ⦂ ([ u ] ⦂ A ▻ B) ▻ [ u ] ⦂ A ▻ [ app (down v₁) (down v₀) ] ⦂ B
-- cdistup = lam (lam (dist v₁ (up v₀)))

cunbox : ∀ {A C Γ} {t : ∅ ⊢ A} {u : ∅ ⊢ C}
         → Γ ⊢ [ t ] ⦂ A ▻ ([ t ] ⦂ A ▻ C) ▻ C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ} → Γ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ} → Γ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ → Γ , A ⊢ B → Γ′ ⊢ A → Γ ⧺ Γ′ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

-- Substitution.

mutual
  [_≔_]_ : ∀ {A B Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢ B → Γ ∖ i ⊢ B
  [ i ≔ s ] var j         with i ≟∈ j
  [ i ≔ s ] var .i        | same   = s
  [ i ≔ s ] var ._        | diff j = var j
  [ i ≔ s ] lam t         = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
  [ i ≔ s ] app t u       = app ([ i ≔ s ] t) ([ i ≔ s ] u)
--  [ i ≔ s ] multibox ts u = multibox ([ i ≔ s ]⋆ ts) u
  [ i ≔ s ] down t        = down ([ i ≔ s ] t)
  [ i ≔ s ] pair t u      = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
  [ i ≔ s ] fst t         = fst ([ i ≔ s ] t)
  [ i ≔ s ] snd t         = snd ([ i ≔ s ] t)
  [ i ≔ s ] unit          = unit

  [_≔_]⋆_ : ∀ {Ξ A Γ} → (i : A ∈ Γ) → Γ ∖ i ⊢ A → Γ ⊢⋆ Ξ → Γ ∖ i ⊢⋆ Ξ
  [_≔_]⋆_ {∅}     i s ∙        = ∙
  [_≔_]⋆_ {Ξ , B} i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- "Equational" reasoning combinator setup
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Expansion.Equational-reasoning-instances {ℓ} {lts : LTS ℓ} where

open import Prelude

open import Bisimilarity lts
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Expansion lts

instance

  reflexive≳ : ∀ {i} → Reflexive [ i ]_≳_
  reflexive≳ = is-reflexive reflexive-≳

  reflexive≳′ : ∀ {i} → Reflexive [ i ]_≳′_
  reflexive≳′ = is-reflexive reflexive-≳′

  convert≳≳ : ∀ {i} → Convertible [ i ]_≳_ [ i ]_≳_
  convert≳≳ = is-convertible id

  convert≳′≳ : ∀ {i} → Convertible _≳′_ [ i ]_≳_
  convert≳′≳ = is-convertible λ p≳′q → force p≳′q

  convert≳≳′ : ∀ {i} → Convertible [ i ]_≳_ [ i ]_≳′_
  convert≳≳′ = is-convertible lemma
    where
    lemma : ∀ {i p q} → [ i ] p ≳ q → [ i ] p ≳′ q
    force (lemma p≳q) = p≳q

  convert≳′≳′ : ∀ {i} → Convertible [ i ]_≳′_ [ i ]_≳′_
  convert≳′≳′ = is-convertible id

  convert∼≳ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≳_
  convert∼≳ = is-convertible ∼⇒≳

  convert∼′≳ : ∀ {i} → Convertible _∼′_ [ i ]_≳_
  convert∼′≳ = is-convertible (convert ∘ ∼⇒≳′)

  convert∼≳′ : ∀ {i} → Convertible [ i ]_∼_ [ i ]_≳′_
  convert∼≳′ {i} = is-convertible lemma
    where
    lemma : ∀ {p q} → [ i ] p ∼ q → [ i ] p ≳′ q
    force (lemma p∼q) = ∼⇒≳ p∼q

  convert∼′≳′ : ∀ {i} → Convertible [ i ]_∼′_ [ i ]_≳′_
  convert∼′≳′ = is-convertible ∼⇒≳′

  trans≳≳ : ∀ {i} → Transitive _≳_ [ i ]_≳_
  trans≳≳ = is-transitive transitive-≳

  trans≳′≳ : ∀ {i} → Transitive _≳′_ [ i ]_≳_
  trans≳′≳ = is-transitive λ p≳′q → transitive (force p≳′q)

  trans≳′≳′ : ∀ {i} → Transitive _≳′_ [ i ]_≳′_
  trans≳′≳′ = is-transitive transitive-≳′

  trans≳≳′ : ∀ {i} → Transitive _≳_ [ i ]_≳′_
  trans≳≳′ = is-transitive lemma
    where
    lemma : ∀ {i p q r} → p ≳ q → [ i ] q ≳′ r → [ i ] p ≳′ r
    force (lemma p≳q q≳′r) = transitive-≳ p≳q (force q≳′r)

  trans∼≳ : ∀ {i} → Transitive _∼_ [ i ]_≳_
  trans∼≳ = is-transitive transitive-∼≳

  -- The occurrences of {a = ℓ} below can perhaps be removed if
  -- Issue #2780 on the Agda bug tracker is fixed.

  trans∼′≳ : ∀ {i} → Transitive _∼′_ [ i ]_≳_
  trans∼′≳ = is-transitive (transitive-∼≳ ∘ convert {a = ℓ})

  trans∼′≳′ : ∀ {i} → Transitive _∼′_ [ i ]_≳′_
  trans∼′≳′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ∼′ q → [ i ] q ≳′ r → [ i ] p ≳′ r
    force (lemma p∼′q q≳′r) =
      transitive-∼≳ (convert {a = ℓ} p∼′q) (force q≳′r)

  trans∼≳′ : ∀ {i} → Transitive _∼_ [ i ]_≳′_
  trans∼≳′ {i} = is-transitive lemma
    where
    lemma : ∀ {p q r} → p ∼ q → [ i ] q ≳′ r → [ i ] p ≳′ r
    force (lemma p∼q q≳′r) = transitive-∼≳ p∼q (force q≳′r)

  trans≳∼ : ∀ {i} → Transitive′ [ i ]_≳_ _∼_
  trans≳∼ = is-transitive transitive-≳∼

  trans≳∼′ : ∀ {i} → Transitive′ [ i ]_≳_ _∼′_
  trans≳∼′ = is-transitive (λ p≳q q∼′r →
    transitive-≳∼ p≳q (convert {a = ℓ} q∼′r))

  trans≳′∼′ : ∀ {i} → Transitive′ [ i ]_≳′_ _∼′_
  trans≳′∼′ = is-transitive transitive-≳∼′

  trans≳′∼ : ∀ {i} → Transitive′ [ i ]_≳′_ _∼_
  trans≳′∼ = is-transitive λ p≳′q q∼r →
    transitive-≳∼′ p≳′q (convert {a = ℓ} q∼r)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Structure.Numeral.Integer where

import      Lvl
open import Structure.Setoid
open import Structure.Operator.Properties
open import Structure.Operator.Ring
open import Structure.OrderedField
open import Structure.Relator
open import Type

private variable ℓₒ ℓₗ ℓₑ ℓₗ₁ ℓₗ₂ : Lvl.Level
private variable Z : Type{ℓₒ}

record Integer ⦃ equiv : Equiv{ℓₑ}(Z) ⦄ (_+_ : Z → Z → Z) (_⋅_ : Z → Z → Z) (_≤_ : Z → Z → Type{ℓₗ}) : Typeω where
  constructor intro
  field
    ⦃ ring ⦄              : Ring(_+_)(_⋅_)
    ⦃ ordered ⦄           : Ordered(_+_)(_⋅_)(_≤_)
  open Ring(ring) public
  open Ordered(ordered) public

  𝐒 : Z → Z
  𝐒 = _+ 𝟏

  𝐏 : Z → Z
  𝐏 = _− 𝟏

  field
    ⦃ distinct-identities ⦄ : DistinctIdentities
    positive-induction : ∀{ℓ}{P : Z → Type{ℓ}} ⦃ rel-p : UnaryRelator(P) ⦄ → P(𝟎) → (∀{n} → (𝟎 ≤ n) → P(n) → P(𝐒(n))) → (∀{n} → (𝟎 ≤ n) → P(n))

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:
-- Datatype modules weren't added as sections properly.
module Issue263b where

module M (A : Set) where
  data D : Set where

postulate A : Set

open M.D A

-- The module M.D is not parameterized, but is being applied to
-- arguments
-- when checking the module application module _ = M.D A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Control.Monad.Weighted.Functor.TypeDef where

open import Level

data 𝔚-F {r w a p} (R : Type r) (W : Type w) (A : Type a) (P : W → Type p) : Type (r ℓ⊔ a ℓ⊔ p ℓ⊔ w) where
  [] : 𝔚-F R W A P
  _◃_∷_⟨_⟩ : ∀ (w : R) (x : A) (xs : W) (P⟨xs⟩ : P xs) → 𝔚-F R W A P

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module examplesPaperJFP.Equality where

infix 4 _≡_

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

-- obsolete, now in Agda.Builtin.Equality: {-# BUILTIN EQUALITY _≡_ #-}
--  No longer exists in Agda: {-# BUILTIN REFL refl #-}

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- {-# OPTIONS -v tc.inj:100 -v tc.reduce:100 #-}
module Issue801 where

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

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

cong : ∀ {A : Set} {B : Set}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

lem : (n : ℕ) → n ≡ n
lem zero    = refl
lem (suc n) = cong (λ x → x) (lem (suc n))
-- Andreas: this made the injectivity checker loop.
-- Now it should just report a termination error.


text:
------------------------------------------------------------------------
-- Partial functions, computability
------------------------------------------------------------------------

open import Atom

module Computability (atoms : χ-atoms) where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (_∘_; Decidable)
open import Tactic.By.Propositional

open import Bool equality-with-J
open import Bijection equality-with-J using (_↔_)
open import Double-negation equality-with-J
open import Equality.Decision-procedures equality-with-J
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Injection equality-with-J using (Injective)
open import Monad equality-with-J

open import Chi            atoms
open import Coding         atoms
import Coding.Instances    atoms as Dummy
open import Deterministic  atoms
open import Free-variables atoms
open import Propositional  atoms
open import Reasoning      atoms
open import Values         atoms

-- Partial functions for which the relation defining the partial
-- function must be propositional.

record _⇀_ {a b} (A : Type a) (B : Type b) : Type (lsuc (a ⊔ b)) where
  infix 4 _[_]=_
  field
    -- The relation defining the partial function.
    _[_]=_ : A → B → Type (a ⊔ b)

    -- The relation must be deterministic and propositional.
    deterministic : ∀ {a b₁ b₂} → _[_]=_ a b₁ → _[_]=_ a b₂ → b₁ ≡ b₂
    propositional : ∀ {a b} → Is-proposition (_[_]=_ a b)

  -- A simple lemma.

  ∃[]=-propositional :
    ∀ {a} →
    Is-proposition (∃ (_[_]=_ a))
  ∃[]=-propositional (b₁ , [a]=b₁) (b₂ , [a]=b₂) =
    Σ-≡,≡→≡ (deterministic [a]=b₁ [a]=b₂)
            (propositional _ _)

open _⇀_ public using (_[_]=_)

-- Totality. The definition is parametrised by something which could
-- be a modality.

Total : ∀ {a b} {A : Type a} {B : Type b} →
        (Type (a ⊔ b) → Type (a ⊔ b)) →
        A ⇀ B → Type (a ⊔ b)
Total P f = ∀ a → P (∃ λ b → f [ a ]= b)

-- Totality with ∥_∥ as the modality implies totality with the
-- identity function as the modality.

total-with-∥∥→total :
  ∀ {a b} {A : Type a} {B : Type b} (f : A ⇀ B) →
  Total ∥_∥ f →
  Total id f
total-with-∥∥→total f total a =
  Trunc.rec
    (_⇀_.∃[]=-propositional f)
    id
    (total a)

-- If the codomain of a function is a set, then the function can be
-- turned into a partial function.

as-partial : ∀ {a b} {A : Type a} {B : Type b} →
             Is-set B → (A → B) → A ⇀ B
as-partial {ℓa} B-set f = record
  { _[_]=_        = λ a b → ↑ ℓa (f a ≡ b)
  ; deterministic = λ {a b₁ b₂} fa≡b₁ fa≡b₂ →
                      b₁   ≡⟨ sym (lower fa≡b₁) ⟩
                      f a  ≡⟨ lower fa≡b₂ ⟩∎
                      b₂   ∎
  ; propositional = ↑-closure 1 (+⇒≡ {n = 1} B-set)
  }

-- Composition of partial functions.

infixr 9 _∘_

_∘_ : ∀ {ℓ c} {A B : Type ℓ} {C : Type c} →
      B ⇀ C → A ⇀ B → A ⇀ C
f ∘ g = record
  { _[_]=_        = λ a c → ∃ λ b → g [ a ]= b × f [ b ]= c
  ; deterministic = λ where
      (b₁ , g[a]=b₁ , f[b₁]=c₁) (b₂ , g[a]=b₂ , f[b₂]=c₂) →
        _⇀_.deterministic f
          (subst (f [_]= _) (_⇀_.deterministic g g[a]=b₁ g[a]=b₂) f[b₁]=c₁)
          f[b₂]=c₂
  ; propositional = λ {a c} →                                           $⟨ Σ-closure 1 (_⇀_.∃[]=-propositional g) (λ _ → _⇀_.propositional f) ⟩
      Is-proposition (∃ λ (p : ∃ λ b → g [ a ]= b) → f [ proj₁ p ]= c)  ↝⟨ H-level.respects-surjection (_↔_.surjection $ inverse Σ-assoc) 1 ⟩□
      Is-proposition (∃ λ b → g [ a ]= b × f [ b ]= c)                  □
  }

-- If f is a partial function, g a function whose domain is a set, and
-- f (g a) = c, then (f ∘ g) a = c.

pre-apply : ∀ {ℓ c} {A B : Type ℓ} {C : Type c}
            (f : B ⇀ C) {g : A → B} {a c}
            (B-set : Is-set B) →
            f [ g a ]= c → f ∘ as-partial B-set g [ a ]= c
pre-apply _ _ f[ga]=b = _ , lift refl , f[ga]=b

-- If f is a function whose domain is a set, g a partial function, and
-- g a = b, then (f ∘ g) a = f b.

post-apply : ∀ {ℓ c} {A B : Type ℓ} {C : Type c}
               {f : B → C} (g : A ⇀ B) {a b}
             (C-set : Is-set C) →
             g [ a ]= b → as-partial C-set f ∘ g [ a ]= f b
post-apply _ _ g[a]=b = _ , g[a]=b , lift refl

-- Implements P p f means that p is an implementation of f. The
-- definition is parametrised by P, which could be a modality.

Implements :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  (Type (a ⊔ b) → Type (a ⊔ b)) →
  Exp → A ⇀ B → Type (a ⊔ b)
Implements P p f =
  Closed p
    ×
  (∀ x y → f [ x ]= y → apply p ⌜ x ⌝ ⇓ ⌜ y ⌝)
    ×
  (∀ x y → apply p ⌜ x ⌝ ⇓ y →
     P (∃ λ y′ → f [ x ]= y′ × y ≡ ⌜ y′ ⌝))

-- If P maps propositions to propositions, then Implements P p f is a
-- proposition.

Implements-propositional :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
    {P : Type (a ⊔ b) → Type (a ⊔ b)} {p : Exp}
  (f : A ⇀ B) →
  (∀ {A} → Is-proposition A → Is-proposition (P A)) →
  Is-proposition (Implements P p f)
Implements-propositional f pres =
  ×-closure 1 Closed-propositional $
  ×-closure 1 (Π-closure ext 1 λ _ →
               Π-closure ext 1 λ _ →
               Π-closure ext 1 λ _ →
               ⇓-propositional)
              (Π-closure ext 1 λ x →
               Π-closure ext 1 λ y →
               Π-closure ext 1 λ _ →
               pres $
               H-level.respects-surjection
                 (_↔_.surjection $ inverse Σ-assoc) 1
                 (Σ-closure 1 (_⇀_.∃[]=-propositional f) λ _ →
                              Exp-set))

-- Computability. The definition is parametrised by something which
-- could be a modality.

Computable′ :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  (Type (a ⊔ b) → Type (a ⊔ b)) →
  A ⇀ B → Type (a ⊔ b)
Computable′ P f = ∃ λ p → Implements P p f

-- Computability.

Computable :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  A ⇀ B → Type (a ⊔ b)
Computable = Computable′ id

-- If the partial function is total, then one part of the proof of
-- computability can be omitted.

total→almost-computable→computable :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄
  (P : Type (a ⊔ b) → Type (a ⊔ b)) →
  (∀ {X Y} → (X → Y) → P X → P Y) →
  (f : A ⇀ B) →
  Total P f →
  (∃ λ p →
     Closed p
       ×
     (∀ x y → f [ x ]= y → apply p ⌜ x ⌝ ⇓ ⌜ y ⌝)) →
  Computable′ P f
total→almost-computable→computable P map f total (p , cl-p , hyp) =
    p
  , cl-p
  , hyp
  , λ x y px⇓y →
      flip map (total x) λ where
        (y′ , f[x]=y′) →
          y′ , f[x]=y′ , ⇓-deterministic px⇓y (hyp x y′ f[x]=y′)

-- The semantics of χ as a partial function.

semantics : Closed-exp ⇀ Closed-exp
semantics = record
  { _[_]=_        = _⇓_ on proj₁
  ; deterministic = λ e⇓v₁ e⇓v₂ →
      closed-equal-if-expressions-equal (⇓-deterministic e⇓v₁ e⇓v₂)
  ; propositional = ⇓-propositional
  }

-- Another definition of computability.

Computable″ :
  ∀ {ℓ} {A B : Type ℓ}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  A ⇀ B → Type ℓ
Computable″ f =
  ∃ λ (p : Closed-exp) → ∀ a →
    ∀ q → semantics [ apply-cl p ⌜ a ⌝ ]= q
            ⇔
          as-partial Closed-exp-set ⌜_⌝ ∘ f [ a ]= q

-- The two definitions of computability are logically equivalent.

Computable⇔Computable″ :
  ∀ {ℓ} {A B : Type ℓ} ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  (f : A ⇀ B) →
  Computable f ⇔ Computable″ f
Computable⇔Computable″ f = record { to = to; from = from }
  where
  to : Computable f → Computable″ f
  to (p , cl , hyp₁ , hyp₂) =
    (p , cl) , λ { a (q , cl-q) → record
      { to   = Σ-map id (Σ-map id (lift P.∘
                                   closed-equal-if-expressions-equal P.∘
                                   sym))
                 P.∘
               hyp₂ a q
      ; from = λ { (b , f[a]=b , ⌜b⌝≡q) →
                   apply p ⌜ a ⌝  ⇓⟨ hyp₁ a b f[a]=b ⟩
                   ⌜ b ⌝          ≡⟨ cong proj₁ (lower ⌜b⌝≡q) ⟩⟶
                   q              ■⟨ subst Value (cong proj₁ (lower ⌜b⌝≡q)) (rep-value b) ⟩ }
      } }

  from : Computable″ f → Computable f
  from ((p , cl) , hyp) =
    p , cl ,
    (λ a b f[a]=b →
       apply p ⌜ a ⌝  ⇓⟨ _⇔_.from (hyp a ⌜ b ⌝) (post-apply f Closed-exp-set f[a]=b) ⟩■
       ⌜ b ⌝) ,
    λ a q p⌜a⌝⇓q →
      let cl-q : Closed q
          cl-q = closed⇓closed p⌜a⌝⇓q
                   (Closed′-closed-under-apply
                      (Closed→Closed′ cl)
                      (Closed→Closed′ (rep-closed a)))
      in
      Σ-map id (Σ-map id (cong proj₁ P.∘ sym P.∘ lower))
        (_⇔_.to (hyp a (q , cl-q)) p⌜a⌝⇓q)

-- Yet another definition of computability.

Computable‴ :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  A ⇀ B → Type (a ⊔ b)
Computable‴ f =
  ∃ λ (p : Closed-exp) →
    ∀ a →
      ∃ λ b →
        apply (proj₁ p) ⌜ a ⌝ ⇓ ⌜ b ⌝
          ×
        f [ a ]= b

-- If a partial function is computable by the last definition of
-- computability above, then it is also computable by the first one.

Computable‴→Computable :
  ∀ {a b} {A : Type a} {B : Type b}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  (f : A ⇀ B) →
  Computable‴ f → Computable f
Computable‴→Computable f ((p , cl-p) , hyp) =
    p
  , cl-p
  , (λ a b f[a]=b → case hyp a of λ where
       (b′ , p⌜a⌝⇓⌜b′⌝ , f[a]=b′) →
         apply p ⌜ a ⌝  ⇓⟨ p⌜a⌝⇓⌜b′⌝ ⟩
         ⌜ b′ ⌝         ≡⟨ by (_⇀_.deterministic f f[a]=b f[a]=b′) ⟩⟶
         ⌜ b ⌝          ■⟨ rep-value b ⟩)
  , (λ a v p⌜a⌝⇓v → case hyp a of λ where
       (b , p⌜a⌝⇓⌜b⌝ , f[a]=b) →
           b
         , f[a]=b
         , ⇓-deterministic p⌜a⌝⇓v p⌜a⌝⇓⌜b⌝)

module _  {a b c d} {A : Type a} {B : Type b} {C : Type c} {D : Type d}
          ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄
          ⦃ rC : Rep C Consts ⦄ ⦃ rD : Rep D Consts ⦄ where

  -- Reductions.

  Reduction : A ⇀ B → C ⇀ D → Type (a ⊔ b ⊔ c ⊔ d)
  Reduction f g = Computable g → Computable f

  -- If f can be reduced to g, and f is not computable, then g is not
  -- computable.

  Reduction→¬Computable→¬Computable :
    (f : A ⇀ B) (g : C ⇀ D) →
    Reduction f g → ¬ Computable f → ¬ Computable g
  Reduction→¬Computable→¬Computable _ _ red ¬f g = ¬f (red g)

-- Total partial functions to the booleans. Note that totality is
-- defined using the double-negation modality.

_→Bool : ∀ {ℓ} → Type ℓ → Type (lsuc ℓ)
A →Bool = ∃ λ (f : A ⇀ Bool) → Total (λ A → ¬¬ A) f

-- One way to view a predicate as a total partial function to the
-- booleans.

as-function-to-Bool₁ : ∀ {a} {A : Type a} → (A → Type a) → A →Bool
as-function-to-Bool₁ P =
    (record
       { _[_]=_        = λ a b →
                           (P a → b ≡ true)
                             ×
                           (¬ P a → b ≡ false)
       ; deterministic = λ where
           {b₁ = true}  {b₂ = true}  _  _  → refl
           {b₁ = false} {b₂ = false} _  _  → refl
           {b₁ = true}  {b₂ = false} f₁ f₂ →
             proj₂ f₁ (Bool.true≢false P.∘ sym P.∘ proj₁ f₂)
           {b₁ = false} {b₂ = true}  f₁ f₂ →
             sym (proj₂ f₂ (Bool.true≢false P.∘ sym P.∘ proj₁ f₁))
       ; propositional = ×-closure 1
                           (Π-closure ext 1 λ _ →
                            Bool-set)
                           (Π-closure ext 1 λ _ →
                            Bool-set)
       })
  , λ a →
      [ (λ p  → true  , (λ _ → refl)  , ⊥-elim P.∘ (_$ p))
      , (λ ¬p → false , ⊥-elim P.∘ ¬p , (λ _ → refl))
      ] ⟨$⟩ excluded-middle

-- Another way to view a predicate as a total partial function to the
-- booleans.

as-function-to-Bool₂ :
  ∀ {a} {A : Type a} →
  (P : A → Type a) →
  (∀ {a} → Is-proposition (P a)) →
  A →Bool
as-function-to-Bool₂ P P-prop =
    (record
       { _[_]=_        = λ a b →
                           P a × b ≡ true
                             ⊎
                           ¬ P a × b ≡ false
       ; deterministic = λ where
           (inj₁ (_ , refl)) (inj₁ (_ , refl)) → refl
           (inj₁ (p , _))    (inj₂ (¬p , _))   → ⊥-elim (¬p p)
           (inj₂ (¬p , _))   (inj₁ (p , _))    → ⊥-elim (¬p p)
           (inj₂ (_ , refl)) (inj₂ (_ , refl)) → refl
       ; propositional = λ {_ b} →
           ⊎-closure-propositional
             (λ { (_ , b≡true) (_ , b≡false) →
                  Bool.true≢false (
                    true   ≡⟨ sym b≡true ⟩
                    b      ≡⟨ b≡false ⟩∎
                    false  ∎) })
             (×-closure 1 P-prop Bool-set)
             (×-closure 1 (¬-propositional ext) Bool-set)
       })
  , λ a →
      [ (λ p  → true  , inj₁ (p , refl))
      , (λ ¬p → false , inj₂ (¬p , refl))
      ] ⟨$⟩ excluded-middle

-- If a is mapped to b by as-function-to-Bool₂ P P-prop, then a is
-- also mapped to b by as-function-to-Bool₁ P.

to-Bool₂→to-Bool₁ :
  ∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
  (P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
  proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b →
  proj₁ (as-function-to-Bool₁ P) [ a ]= b
to-Bool₂→to-Bool₁ _ _ = λ where
  (inj₁ (Pa  , refl)) → (λ _ → refl) , ⊥-elim P.∘ (_$ Pa)
  (inj₂ (¬Pa , refl)) → ⊥-elim P.∘ ¬Pa , λ _ → refl

-- If a is mapped to b by as-function-to-Bool₁ P, then a is not not
-- mapped to b by as-function-to-Bool₂ P P-prop.

to-Bool₁→to-Bool₂ :
  ∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
  (P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) {a b} →
  proj₁ (as-function-to-Bool₁ P) [ a ]= b →
  ¬¬ proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b
to-Bool₁→to-Bool₂ _ _ (Pa→b≡true , ¬Pa→b≡false) =
  ⊎-map (λ Pa → Pa , Pa→b≡true Pa) (λ ¬Pa → ¬Pa , ¬Pa→b≡false ¬Pa) ⟨$⟩
    excluded-middle

-- If as-function-to-Bool₁ P is ¬¬-computable, then
-- as-function-to-Bool₂ P P-prop is also ¬¬-computable.

to-Bool₁-computable→to-Bool₂-computable :
  ∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄
  (P : A → Type a) (P-prop : ∀ {a} → Is-proposition (P a)) →
  Computable′ (λ A → ¬¬ A) (proj₁ (as-function-to-Bool₁ P)) →
  Computable′ (λ A → ¬¬ A) (proj₁ (as-function-to-Bool₂ P P-prop))
to-Bool₁-computable→to-Bool₂-computable
  P P-prop (p , cl-p , hyp₁ , hyp₂) =
    p
  , cl-p
  , (λ a b →
       proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b  ↝⟨ to-Bool₂→to-Bool₁ P P-prop ⟩
       proj₁ (as-function-to-Bool₁ P)        [ a ]= b  ↝⟨ hyp₁ a b ⟩□
       apply p ⌜ a ⌝ ⇓ ⌜ b ⌝                           □)
  , λ a e →
      apply p ⌜ a ⌝ ⇓ e                                             ↝⟨ hyp₂ a e ⟩

      ¬¬ (∃ λ b → proj₁ (as-function-to-Bool₁ P) [ a ]= b ×
                  e ≡ ⌜ b ⌝)                                        ↝⟨ _>>= (λ { (b , =b , ≡⌜b⌝) →
                                                                                to-Bool₁→to-Bool₂ P P-prop =b >>= λ =b →
                                                                                return (b , =b , ≡⌜b⌝) }) ⟩□
      ¬¬ (∃ λ b → proj₁ (as-function-to-Bool₂ P P-prop) [ a ]= b ×
                  e ≡ ⌜ b ⌝)                                        □

-- A lemma related to as-function-to-Bool₂.

×≡true⊎¬×≡false⇔⇔T :
  ∀ {a} {A : Type a} (P : A → Type a) →
  ∀ {a b} → P a × b ≡ true ⊎ ¬ P a × b ≡ false ⇔ (P a ⇔ T b)
×≡true⊎¬×≡false⇔⇔T P {a} {b} = record
  { to = λ where
      (inj₁ (p  , refl)) → record { from = λ _ → p }
      (inj₂ (¬p , refl)) → record { to = ¬p; from = ⊥-elim }
  ; from = helper b
  }
  where
  helper : ∀ b → P a ⇔ T b → P a × b ≡ true ⊎ ¬ P a × b ≡ false
  helper true  hyp = inj₁ (_⇔_.from hyp _ , refl)
  helper false hyp = inj₂ (_⇔_.to hyp , refl)

-- One way to view a predicate as a partial function to the booleans.

as-partial-function-to-Bool₁ :
  ∀ {a} {A : Type a} → (A → Type a) → A ⇀ Bool
as-partial-function-to-Bool₁ P = record
  { _[_]=_        = λ a b →
                      (P a → b ≡ true)
                        ×
                      ¬ ¬ P a
  ; deterministic = λ where
      {b₁ = true}  {b₂ = true}  _ _ → refl
      {b₁ = false} {b₂ = false} _ _ → refl
      {b₁ = true}  {b₂ = false} _ f →
        ⊥-elim $ proj₂ f (Bool.true≢false P.∘ sym P.∘ proj₁ f)
      {b₁ = false} {b₂ = true}  f _ →
        ⊥-elim $ proj₂ f (Bool.true≢false P.∘ sym P.∘ proj₁ f)
  ; propositional = ×-closure 1
                      (Π-closure ext 1 λ _ →
                       Bool-set)
                      (¬-propositional ext)
  }

-- Another way to view a predicate as a partial function to the
-- booleans.

as-partial-function-to-Bool₂ :
  ∀ {a} {A : Type a} →
  (P : A → Type a) →
  (∀ {a} → Is-proposition (P a)) →
  A ⇀ Bool
as-partial-function-to-Bool₂ P P-prop = record
  { _[_]=_        = λ a b → P a × b ≡ true
  ; deterministic = λ { (_ , refl) (_ , refl) → refl }
  ; propositional = ×-closure 1 P-prop Bool-set
  }

-- One definition of what it means for a total partial function to the
-- booleans to be decidable.

Decidable :
  ∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
  A →Bool → Type a
Decidable = Computable P.∘ proj₁

-- Another definition of what it means for a total partial function to
-- the booleans to be decidable.

Decidable′ :
  ∀ {a} {A : Type a} ⦃ rA : Rep A Consts ⦄ →
  A →Bool → Type a
Decidable′ = Computable‴ P.∘ proj₁

-- Computable functions from a type to a set.

record Computable-function
         {a b} (A : Type a) (B : Type b) (B-set : Is-set B)
         ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ :
         Type (a ⊔ b) where
  field
    function   : A → B
    computable : Computable (as-partial B-set function)

open Computable-function

-- An unfolding lemma for Computable-function.

Computable-function↔ :
  ∀ {a b} {A : Type a} {B : Type b} {B-set : Is-set B}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
  Computable-function A B B-set ↔
  ∃ λ (f : A → B) → Computable (as-partial B-set f)
Computable-function↔ = record
  { surjection = record
    { logical-equivalence = record
      { to = λ f → function f , computable f
      }
    ; right-inverse-of = λ _ → refl
    }
  ; left-inverse-of = λ _ → refl
  }

-- If two computable functions have equal implementations, then they
-- are equal.

equal-implementations→equal :
  ∀ {a b} {A : Type a} {B : Type b} {B-set : Is-set B}
    ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄
  (f g : Computable-function A B B-set) →
  proj₁ (computable f) ≡ proj₁ (computable g) →
  function f ≡ function g
equal-implementations→equal f g hyp = ⟨ext⟩ λ x →          $⟨ proj₁ (proj₂ (proj₂ (computable f))) x (function f x) (lift refl)
                                                            , proj₁ (proj₂ (proj₂ (computable g))) x (function g x) (lift refl) ⟩
  apply (proj₁ (computable f)) ⌜ x ⌝ ⇓ ⌜ function f x ⌝ ×
  apply (proj₁ (computable g)) ⌜ x ⌝ ⇓ ⌜ function g x ⌝    ↝⟨ Σ-map id (subst (λ e → apply e _ ⇓ _) (sym hyp)) ⟩

  apply (proj₁ (computable f)) ⌜ x ⌝ ⇓ ⌜ function f x ⌝ ×
  apply (proj₁ (computable f)) ⌜ x ⌝ ⇓ ⌜ function g x ⌝    ↝⟨ uncurry ⇓-deterministic ⟩

  ⌜ function f x ⌝ ≡ ⌜ function g x ⌝                      ↝⟨ rep-injective ⟩□

  function f x ≡ function g x                              □

instance

  -- Representation functions for computable functions.

  rep-Computable-function :
    ∀ {a b} {A : Type a} {B : Type b} {B-set : Is-set B}
      ⦃ rA : Rep A Consts ⦄ ⦃ rB : Rep B Consts ⦄ →
    Rep (Computable-function A B B-set) Consts
  rep-Computable-function {A = A} {B = B} {B-set = B-set} = record
    { ⌜_⌝           = ⌜_⌝ P.∘ proj₁ P.∘ computable
    ; rep-injective = injective
    }
    where
    abstract
      injective :
        Injective {A = Computable-function A B B-set} {B = Consts}
          (⌜_⌝ P.∘ proj₁ P.∘ computable)
      injective {f} {g} =
        ⌜ proj₁ (computable f) ⌝ ≡ ⌜ proj₁ (computable g) ⌝             ↝⟨ rep-injective ⟩

        proj₁ (computable f) ≡ proj₁ (computable g)                     ↝⟨ (λ hyp → cong₂ _,_ (equal-implementations→equal f g hyp) hyp) ⟩

        (function f , proj₁ (computable f)) ≡
        (function g , proj₁ (computable g))                             ↔⟨ ignore-propositional-component $
                                                                           Implements-propositional (as-partial B-set (function g)) id ⟩
        ((function f , proj₁ (computable f)) , proj₂ (computable f)) ≡
        ((function g , proj₁ (computable g)) , proj₂ (computable g))    ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Σ-assoc) ⟩

        (function f , computable f) ≡ (function g , computable g)       ↔⟨ Eq.≃-≡ (Eq.↔⇒≃ Computable-function↔) ⟩□

        f ≡ g                                                           □

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Symmetry

module Oscar.Class.Symmetry.ToSym where

private

  test-class :
    ⦃ _ : ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class _∼_ ⦄
    → ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class _∼_
  test-class = !

  test-class' :
    ∀ {𝔬} {𝔒 : Ø 𝔬} {x : 𝔒} {𝔯} {F : (𝔒 → 𝔒 → Ø 𝔯) → 𝔒 → 𝔒 → Ø 𝔯}
    ⦃ _ : ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F (S x)) ⦄
    → ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F (S x))
  test-class' ⦃ ⌶ ⦄ {S} = ⌶ {S} -- FIXME _S _x ≟ _S' _x

  test-class'' :
    ∀ {𝔬} {𝔒 : Ø 𝔬} {x : 𝔒} {𝔯} {F : (𝔒 → 𝔒 → 𝔒 → Ø 𝔯) → 𝔒 → 𝔒 → 𝔒 → Ø 𝔯}
    ⦃ _ : ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F S x) ⦄
    → ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F S x)
  test-class'' = !

  test-class''' :
    ∀ {𝔬} {𝔒 : Ø 𝔬} {𝔯} {F : (𝔒 → 𝔒 → 𝔒 → Ø 𝔯) → 𝔒 → 𝔒 → Ø 𝔯}
    ⦃ _ : ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F S) ⦄
    → ∀ {S : 𝔒 → 𝔒 → 𝔒 → Ø 𝔯} → Symmetry.class (F S)
  test-class''' = !

  test-method-sym : ∀
    {𝔬} {𝔒 : Ø 𝔬}
    {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
    ⦃ _ : Symmetry.class _∼_ ⦄
    → _
  test-method-sym {_∼_ = _∼_} = λ {x} {y} → Symmetry.method _∼_ {x} {y}

  test-method-symmetry : ∀
    {𝔬} {𝔒 : Ø 𝔬}
    {𝔯} {_∼_ : 𝔒 → 𝔒 → Ø 𝔯}
    ⦃ _ : Symmetry.class _∼_ ⦄
    → _
  test-method-symmetry {_∼_ = _∼_} = λ {x} {y} → symmetry[ _∼_ ] {x} {y}


text:
{-# OPTIONS --universe-polymorphism #-}

module RawFunctor where

open import Common.Level

postulate RawFunctor : ∀ {ℓ} (F : Set ℓ → Set ℓ) → Set (lsuc ℓ)

-- Broken occurs check for levels made this not infer properly
postulate
  sequence⁻¹ : ∀ {F}{A} {P : A → Set} → RawFunctor F →
                 F (∀ i → P i) → ∀ i → F (P i)

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module ImportWarningsB where

-- all of the following files have warnings, which should be displayed
-- when loading this file

import Issue1988
import Issue2243
import Issue708quote
import OldCompilerPragmas
import RewritingEmptyPragma
import Unreachable

-- this warning will be ignored
{-# REWRITE #-}

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of fresh lists and functions acting on them
------------------------------------------------------------------------

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

module Data.List.Fresh.Properties where

open import Level using (Level; _⊔_; Lift)
open import Data.Product using (_,_)
open import Relation.Nullary
open import Relation.Unary as U using (Pred)
open import Relation.Binary as B using (Rel)

open import Data.List.Fresh

private
  variable
    a b e p r : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Fresh congruence

module _ {R : Rel A r} {_≈_ : Rel A e} (R≈ : R B.Respectsˡ _≈_) where

  fresh-respectsˡ : ∀ {x y} {xs : List# A R} → x ≈ y → x # xs → y # xs
  fresh-respectsˡ {xs = []}      x≈y x#xs       = _
  fresh-respectsˡ {xs = x ∷# xs} x≈y (r , x#xs) =
    R≈ x≈y r , fresh-respectsˡ x≈y x#xs

------------------------------------------------------------------------
-- Empty and NotEmpty

Empty⇒¬NonEmpty : {R : Rel A r} {xs : List# A R} → Empty xs → ¬ (NonEmpty xs)
Empty⇒¬NonEmpty [] ()

NonEmpty⇒¬Empty : {R : Rel A r} {xs : List# A R} → NonEmpty xs → ¬ (Empty xs)
NonEmpty⇒¬Empty () []

empty? : {R : Rel A r} (xs : List# A R) → Dec (Empty xs)
empty? []       = yes []
empty? (_ ∷# _) = no (λ ())

nonEmpty? : {R : Rel A r} (xs : List# A R) → Dec (NonEmpty xs)
nonEmpty? []             = no (λ ())
nonEmpty? (cons x xs pr) = yes (cons x xs pr)


text:
{-

Definition of a homogeneous pointed type, and proofs that pi, product, path, and discrete types are homogeneous

Portions of this file adapted from Nicolai Kraus' code here:
  https://bitbucket.org/nicolaikraus/agda/src/e30d70c72c6af8e62b72eefabcc57623dd921f04/trunc-inverse.lagda

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Data.Prod
open import Cubical.Data.Empty
open import Cubical.Relation.Nullary

open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties

isHomogeneous : ∀ {ℓ} → Pointed ℓ → Type (ℓ-suc ℓ)
isHomogeneous {ℓ} (A , x) = ∀ y → Path (Pointed ℓ) (A , x) (A , y)

isHomogeneousPi : ∀ {ℓ ℓ'} {A : Type ℓ} {B∙ : A → Pointed ℓ'}
                 → (∀ a → isHomogeneous (B∙ a)) → isHomogeneous (Π∙ A B∙)
isHomogeneousPi h f i = (∀ a → typ (h a (f a) i)) , (λ a → pt (h a (f a) i))

isHomogeneousProd : ∀ {ℓ ℓ'} {A∙ : Pointed ℓ} {B∙ : Pointed ℓ'}
                   → isHomogeneous A∙ → isHomogeneous B∙ → isHomogeneous (A∙ ×∙ B∙)
isHomogeneousProd hA hB (a , b) i = (typ (hA a i)) × (typ (hB b i)) , (pt (hA a i) , pt (hB b i))

isHomogeneousPath : ∀ {ℓ} (A : Type ℓ) {x y : A} (p : x ≡ y) → isHomogeneous ((x ≡ y) , p)
isHomogeneousPath A {x} {y} p q i
  = ua eqv i , ua-gluePath eqv (compPathr-cancel p q) i
  where eqv : (x ≡ y) ≃ (x ≡ y)
        eqv = ((q ∙ sym p) ∙_) , compPathl-isEquiv (q ∙ sym p)

module HomogeneousDiscrete {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) (y : typ A∙) where

  -- switches pt A∙ with y
  switch : typ A∙ → typ A∙
  switch x with dA x (pt A∙)
  ...         | yes _ = y
  ...         | no _ with dA x y
  ...                | yes _  = pt A∙
  ...                | no  _  = x

  switch-ptA∙ : switch (pt A∙) ≡ y
  switch-ptA∙ with dA (pt A∙) (pt A∙)
  ...         | yes _ = refl
  ...         | no ¬p = ⊥-elim (¬p refl)

  switch-idp : ∀ x → switch (switch x) ≡ x
  switch-idp x with dA x (pt A∙)
  switch-idp x | yes p with dA y (pt A∙)
  switch-idp x | yes p | yes q = q ∙ sym p
  switch-idp x | yes p | no  _ with dA y y
  switch-idp x | yes p | no  _ | yes _ = sym p
  switch-idp x | yes p | no  _ | no ¬p = ⊥-elim (¬p refl)
  switch-idp x | no ¬p with dA x y
  switch-idp x | no ¬p | yes p with dA y (pt A∙)
  switch-idp x | no ¬p | yes p | yes q = ⊥-elim (¬p (p ∙ q))
  switch-idp x | no ¬p | yes p | no  _ with dA (pt A∙) (pt A∙)
  switch-idp x | no ¬p | yes p | no  _ | yes _ = sym p
  switch-idp x | no ¬p | yes p | no  _ | no ¬q = ⊥-elim (¬q refl)
  switch-idp x | no ¬p | no ¬q with dA x (pt A∙)
  switch-idp x | no ¬p | no ¬q | yes p = ⊥-elim (¬p p)
  switch-idp x | no ¬p | no ¬q | no  _ with dA x y
  switch-idp x | no ¬p | no ¬q | no  _ | yes q = ⊥-elim (¬q q)
  switch-idp x | no ¬p | no ¬q | no  _ | no  _ = refl

  switch-eqv : typ A∙ ≃ typ A∙
  switch-eqv = isoToEquiv (iso switch switch switch-idp switch-idp)

isHomogeneousDiscrete : ∀ {ℓ} {A∙ : Pointed ℓ} (dA : Discrete (typ A∙)) → isHomogeneous A∙
isHomogeneousDiscrete {ℓ} {A∙} dA y i
  = ua switch-eqv i , ua-gluePath switch-eqv switch-ptA∙ i
  where open HomogeneousDiscrete {ℓ} {A∙} dA y

max_stars_repo_name: oisdk/cubical

max_issues_repo_name: oisdk/cubical

max_forks_repo_name: oisdk/cubical


text:
module Data.Bin.Bijection where

  open import Relation.Binary.PropositionalEquality as PropEq hiding (inspect)
  open import Function.Inverse renaming (_∘_ to _∙_)
  import Function.Surjection
  open Function.Surjection using (module Surjection; module Surjective)
  open import Function.Equality using (_⟶_)
  open import Data.Nat using (ℕ; _*_; _+_)
  open import Data.Bin using (toℕ; Bin; fromBits; 2+_; 0b; 1b)
  open import Data.Product
  open import Data.Digit using (Bit; toDigits; fromDigits)

  ℕ-setoid = PropEq.setoid ℕ
  Bin-setoid = PropEq.setoid Bin

  import Data.Fin
  pattern 1+ x = Data.Nat.suc x

  fromℕ : ℕ → Bin
  fromℕ x = fromBits (proj₁ (toDigits 2 x))

-- hard to prove now
--  fromℕeq' : {n : ℕ} → fromℕ n ≡ fromℕ' n
--  fromℕeq' {x} with toDigits 2 x
--  fromℕeq' .{fromDigits d} | d , refl = {!!}

  fromℕ⟶ : ℕ-setoid ⟶ Bin-setoid
  fromℕ⟶ = record
    { _⟨$⟩_ = fromℕ
    ; cong = PropEq.cong fromℕ
    }

  toℕ⟶ : Bin-setoid ⟶ ℕ-setoid
  toℕ⟶ = record
    { _⟨$⟩_ = toℕ
    ; cong = PropEq.cong toℕ
    }

  open import Data.Digit using(Bit)
  open import Data.Bin using (fromBits; toBits; _1#; 0#; 0b; 1b)
  open import Data.List using (_∷_; []; _++_)
  open import Data.Fin using (suc; zero) renaming (toℕ to bitToℕ)

  open import Data.Bin.BitListBijection
    using (_≈_; All-zero; module All-zero; All-zero-respects-equivalence)
    renaming (setoid to bits-setoid; bijection-to-ℕ to Bits-bijection-ℕ)

  open _≈_
  open All-zero
  open import Relation.Binary using (module Setoid)
  module Bits = Setoid bits-setoid

  open import Data.Product using (_,_; proj₂; proj₁)
  open import Function using (_∘_)

  open Data.List using(List)

  fromBits-zero : ∀ {l} → All-zero l → fromBits l ≡ 0#
  fromBits-zero [] = PropEq.refl
  fromBits-zero (All-zero.cons {t} z) with fromBits t | fromBits-zero z
  fromBits-zero (All-zero.cons z) | .0# | refl = PropEq.refl

  fromBitsCong : ∀ {i j} → i ≈ j → fromBits i ≡ fromBits j
  fromBitsCong (both-zero a-zero b-zero) =
     PropEq.trans (fromBits-zero a-zero)
      (PropEq.sym (fromBits-zero b-zero))
  fromBitsCong (heads-match h at bt eq) with fromBits at | fromBits bt | fromBitsCong eq
  fromBitsCong (heads-match Data.Bin.0b at bt eq) | 0# | .0# | refl = PropEq.refl
  fromBitsCong (heads-match Data.Bin.1b at bt eq) | 0# | .0# | refl = PropEq.refl
  fromBitsCong (heads-match (Data.Bin.2+ ()) at bt eq) | 0# | .0# | refl
  fromBitsCong (heads-match h at bt eq) | bs 1# | .(bs 1#) | refl = PropEq.refl

  fromBits⟶ : bits-setoid ⟶ Bin-setoid
  fromBits⟶ = record
    { _⟨$⟩_ = fromBits
    ; cong = fromBitsCong
    }

  toBits⟶ : Bin-setoid ⟶ bits-setoid
  toBits⟶ = record
    { _⟨$⟩_ = toBits
    ; cong = λ { {i} .{_} PropEq.refl → Bits.refl }
    }

  open import Data.Product using (_×_)

  #1-inj : ∀ {a b} → a 1# ≡ b 1# → a ≡ b
  #1-inj refl = refl

  fromToBits-inverse : ∀ a → fromBits (toBits a) ≡ a
  fromToBits-inverse 0# = refl
  fromToBits-inverse ([] 1#) = refl
  fromToBits-inverse ((h ∷ t) 1#) with fromBits (toBits (t 1#)) | fromToBits-inverse (t 1#)
  ... | 0# | ()
  ... | l 1# | eq = PropEq.cong (λ x → (h ∷ x) 1#) (#1-inj eq)

  qqq : ∀ {xs} → (0b ∷ []) ≈ xs → [] ≈ xs
  qqq (both-zero a-zero b-zero) = both-zero [] b-zero
  qqq (heads-match .0b .[] bt x) = both-zero [] (cons (All-zero-respects-equivalence x []))

  toFromBits-inverse : ∀ a → (toBits (fromBits a)) ≈ a
  toFromBits-inverse [] = both-zero (cons []) []
  toFromBits-inverse (x ∷ xs) with fromBits xs | toFromBits-inverse xs
  toFromBits-inverse (0b ∷ xs) | 0# | w =
    heads-match 0b [] xs (qqq w)
  toFromBits-inverse (1b ∷ xs) | 0# | w =
    heads-match 1b [] xs (qqq w)
  toFromBits-inverse ((2+ ()) ∷ xs) | 0# | w
  toFromBits-inverse (x ∷ xs) | bs 1# | w =
    heads-match x (bs ++ suc 0b ∷ []) xs w

  fromBits-inj : ∀ {x y} → fromBits x ≡ fromBits y → x ≈ y
  fromBits-inj eq =
    Bits.trans (Bits.sym (toFromBits-inverse _))
    (Bits.trans (Setoid.reflexive bits-setoid (cong toBits eq)) (toFromBits-inverse _))

  open import Function.Inverse using (Inverse; _InverseOf_)

  inverseFB : toBits⟶ InverseOf fromBits⟶
  inverseFB = record
    {
      left-inverse-of = toFromBits-inverse;
      right-inverse-of = fromToBits-inverse
    }

  Bits-inverse-Bin : Inverse bits-setoid Bin-setoid
  Bits-inverse-Bin = record
    { inverse-of = inverseFB
    }

  fromℕ-inverse : Inverse ℕ-setoid Bin-setoid
  fromℕ-inverse =
    Bits-inverse-Bin
    ∙ Function.Inverse.sym (Function.Inverse.fromBijection Bits-bijection-ℕ)

  bijection-is-reasonable1 :
    Function.Equality._⟨$⟩_ (Inverse.to fromℕ-inverse) ≡ fromℕ
  bijection-is-reasonable1 = PropEq.refl

  bijection-is-reasonable2 :
    Function.Equality._⟨$⟩_ (Inverse.from fromℕ-inverse) ≡ toℕ
  bijection-is-reasonable2 = PropEq.refl

  toℕ-inverse = Function.Inverse.sym fromℕ-inverse
  toℕ-bijection = Inverse.bijection toℕ-inverse
  fromℕ-bijection = Inverse.bijection fromℕ-inverse

  toℕ-inj = Inverse.injective toℕ-inverse
  fromℕ-inj = Inverse.injective fromℕ-inverse
  fromToℕ-inverse = Inverse.left-inverse-of toℕ-inverse
  toFromℕ-inverse = Inverse.right-inverse-of toℕ-inverse

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod


text:
module Issue690a where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

-- A negative type.
data T : Set → Set where
  c : T (T ℕ)

-- From Andreas (2012-09-07) message on Agda mailing list "Forget
-- Hurken's paradox ..."
--
-- Trying to make sense of T in terms of inductive types, explaining
-- indices via equalities, one arrives at
--
--  data T (X : Set) : Set where
--    c : (X ≡ T ℕ) → T X
--
-- which has a non-positive occurrence of T in (X ≡ T ℕ).
--
-- An argument for the existence of T would have to argue for the
-- existence this least fixed point:
--
--  lfp \lambda T X → (X ≡ T ℕ)

-- ASR (14 August 2014): In Coq'Art, § 14.1.2.1, the type T is
-- rejected due to the head type constrains.


text:
open import Common.IO

header = putStrLn "foo"

main : IO _
main = putStrLn "42"

max_forks_repo_name: Agda-zh/agda