text:
import      Lvl
open import Logic
open import Type

module Data.List.Relation.Pairwise {ℓ₁ ℓ₂} {T : Type{ℓ₁}} where

open import Data.List
import      Data.List.Functions as List
open import Data.List.Relation.Quantification
open import Functional
open import Logic.Propositional

-- Whether a list's elements pairwise satisfy a binary relation with their adjacent elements in the list.
-- Example:
--   AdjacentlyPairwise(_▫_) [a,b,c,d,e]
--   ↔ (∧){
--     • (a ▫ b)
--     • (b ▫ c)
--     • (c ▫ d)
--     • (d ▫ e)
--   }
-- Note: Equivalent to OrderedPairwise(_▫_) when (_▫_) is transitive.
data AdjacentlyPairwise(_▫_ : T → T → Stmt{ℓ₂}) : List(T) → Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  instance
    empty  : AdjacentlyPairwise(_▫_)(∅)
    single : ∀{a} → AdjacentlyPairwise(_▫_)(List.singleton(a))
    step   : ∀{a b}{l} → ⦃ _ : (a ▫ b) ⦄ → ⦃ _ : AdjacentlyPairwise(_▫_)(b ⊰ l) ⦄ → AdjacentlyPairwise(_▫_)(a ⊰ b ⊰ l)

-- Whether a list's elements pairwise satisfy a binary relation with all the successive elements in the list.
-- Example:
--   OrderedPairwise(_▫_) [a,b,c,d,e]
--   ↔ (∧){
--     • (a ▫ b)
--     • (a ▫ c)
--     • (a ▫ d)
--     • (a ▫ e)
--     • (b ▫ c)
--     • (b ▫ d)
--     • (b ▫ e)
--     • (c ▫ d)
--     • (c ▫ e)
--     • (d ▫ e)
--   }
-- Note: Equivalent to Pairwise(_▫_) when (_▫_) is symmetric.
data OrderedPairwise(_▫_ : T → T → Stmt{ℓ₂}) : List(T) → Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  empty  : OrderedPairwise(_▫_)(∅)
  step   : ∀{a}{l} → AllElements(a ▫_)(l) → OrderedPairwise(_▫_)(l) → OrderedPairwise(_▫_)(a ⊰ l)

-- TODO: Is this correct? Using (_∧_)?
Pairwise : (T → T → Stmt{ℓ₂}) → List(T) → Stmt
Pairwise(_▫_) = OrderedPairwise(x ↦ y ↦ (y ▫ x) ∧ (x ▫ y))


text:
open import Agda.Builtin.Nat

-- split on m

-- WAS: m = zero or m = suc m
-- WANT: m = suc m because 2nd clause already covers m = zero

f : Nat -> Nat -> Nat
f m zero = {!!}
f zero zero = zero
f _ _ = zero

-- However for g, we still get m = zero or m = suc m
-- because the other splits are orthogonal / catchalls

g : Nat -> Nat -> Nat
g m zero = {!!}
g zero n = zero
g _ _ = zero

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

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

pattern `Nat = def (quote Nat) []

unquoteDecl f =
  declareDef (vArg f) `Nat


text:
module _ where

postulate D : Set

module A where

  infixr 5 _∷_

  postulate
    _∷_ : Set₁ → D → D

module B where

  infix 5 _∷_

  postulate
    _∷_ : Set₁ → Set₁ → D

open A
open B

foo : D
foo = Set ∷ Set

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
module Cats.Category.Setoids where

open import Cats.Util.SetoidMorphism public using
  (_⇒_ ; _≈_ ; ≈-intro ; ≈-elim ; ≈-elim′ ; equiv ; _∘_ ; id ; ∘-resp ; assoc ; id-l
  ; id-r)

open import Level using (_⊔_ ; suc)
open import Relation.Binary using (Setoid)

open import Cats.Category.Base
open import Cats.Category.Sets using (Sets)
open import Cats.Util.Conv

instance
  HasArrow-⇒ : ∀ {l l≈} {A B : Setoid l l≈}
    → HasArrow (A ⇒ B) (suc l) l l
  HasArrow-⇒ {l} = record { Cat = Sets l ; _⃗ = _⇒_.arr }

Setoids : ∀ l l≈ → Category (suc (l ⊔ l≈)) (l ⊔ l≈) (l ⊔ l≈)
Setoids l l≈ = record
    { Obj = Setoid l l≈
    ; _⇒_ = λ A B → A ⇒ B
    ; _≈_ = _≈_
    ; id = id
    ; _∘_ = _∘_
    ; equiv = equiv
    ; ∘-resp = λ {A} {B} {C} {f} {g} {h} {i} → ∘-resp {f = f} {g} {h} {i}
    ; id-r = λ {A} {B} {f} → id-r {f = f}
    ; id-l = λ {A} {B} {f} → id-l {f = f}
    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} → assoc {f = f} {g} {h}
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --sized-types #-}

module Ex where

open import Size
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Fin
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

• : Set
• = ⊤

-- | Container for defining signatures
record Cont : Set₁ where
  constructor cont
  field
    Pos : Set
    Sh : Pos → Set
open Cont

-- | Extension of a container
⟪_⟫ : Cont → Set → Set
⟪ cont P S ⟫ X = Σ P (λ p → S p → X)

-- | Finite and infinite trees over a signature
record T∞ {i : Size} (C : Cont) : Set where
  coinductive
  field
    out : ∀ {j : Size< i} → • ⊎ ⟪ C ⟫ (T∞ {j} C)
open T∞

------
-- Example due to Fu Peng
-----

-- In the following, we give two interpretations to the logic program
-- ⇒ P(c)
-- P(x), P(f(f x)) ⇒ P(f x).
-- The first is an inductive interpretation, the second is coinductive.
-- In both cases we are able to prove that there is a tree x : Tree sig₁,
-- such that P x holds.

-- | Signature has two symbols, a nullary and a unary symbol.
sig₁ : Cont
sig₁ = cont (⊤ ⊎ ⊤) S
  where
    S : ⊤ ⊎ ⊤ → Set
    S (inj₁ tt) = Fin 0
    S (inj₂ tt) = Fin 1

-- | Symbol names
c' f' : Pos sig₁
c' = inj₁ tt
f' = inj₂ tt

-- | Symbol constructor for c
c : T∞ sig₁
out c = inj₂ (c' , (λ ()))

-- | Constructor for symbol f
f : T∞ sig₁ → T∞ sig₁
out (f x) = inj₂ (f' , (λ _ → x))

-- | c and f a distinct constructors
c≢f : (x : T∞ sig₁) → c ≡ f x → ⊥
c≢f x p = lem x (cong (λ t → out t {∞}) p)
  where
    lem : (y : T∞ sig₁) → out c ≡ out (f y) → ⊥
    lem y ()

-- | Inductive interpretation of LP
data P-ind : T∞ sig₁ → Set where
  c-P : P-ind c
  f-P : (x : T∞ sig₁) → P-ind x → P-ind (f (f x)) → P-ind (f x)

-- | P c holds immediately.
p-ind₀ : ∃ λ x → P-ind x
p-ind₀ = (c , c-P)

unprvbl-lem : (x : T∞ sig₁) → P-ind (f x) → ⊥
unprvbl-lem x q = m x (f x) q refl
  where
    m : (x y : T∞ sig₁) → P-ind y → y ≡ f x → ⊥
    m x .c c-P p = (c≢f x p)
    m x .(f x₁) (f-P x₁ p q₁) e = m (f x₁) (f (f x₁)) q₁ refl

-- | We can show that there is no tree x, s.t. P-ind (f x) holds.
unprvbl : ¬ (∃ λ x → P-ind (f x))
unprvbl (x , q) = unprvbl-lem x q

-------
-- Coinductive interpretation of LP

F : (T∞ sig₁ → Set) → T∞ sig₁ → Set
F G x = m (out x)
  where
    m : ⊤ ⊎ ⟪ sig₁ ⟫ (T∞ sig₁) → Set
    m (inj₁ tt) = ⊥            -- case for •
    m (inj₂ (inj₁ tt , _)) = ⊤ -- case for c, k₀
    m (inj₂ (inj₂ tt , α)) =   -- case for f x, k₁
      let x = α zero
      in G x × G (f (f x))

record P-coind' (x : T∞ sig₁) : Set where
  coinductive
  field
    p-out' : F P-coind' x
open P-coind'

record P-coind {i : Size} (x : T∞ sig₁) : Set where
  coinductive
  field
    p-out : ∀ {j : Size< i} → F (P-coind {j}) x
open P-coind

-- | Trivial proof
k₀ : P-coind c
p-out k₀ = tt

-- | Non-trivial proof
p-coind : ∃ λ x → P-coind (f x)
p-coind = (_ , k _ k₀)
  where
    k : ∀{i} → (x : T∞ sig₁) → P-coind {i} x → P-coind {i} (f x)
    p-out (k x q) = (q , k (f x) (k x q))

-------------------------------------------
------- From example
-------------------------------------------

-- | The signature has two symbols: S of arity 1 and cons of arity 2.
sig₂ : Cont
sig₂ = cont (⊤ ⊎ ⊤) ar₂
  where
    ar₂ : ⊤ ⊎ ⊤ → Set
    ar₂ (inj₁ tt) = Fin 1
    ar₂ (inj₂ tt) = Fin 2

-- | Easier to read symbol names
S' cons' : Pos sig₂
S'    = inj₁ tt
cons' = inj₂ tt

-- | Tree constructors for S
S : ∀{i} → T∞ {i} sig₂ → T∞ {i} sig₂
out (S x) = inj₂ (S' , (λ _ → x))

-- | Tree constructors for cons
cons : T∞ sig₂ → T∞ sig₂ → T∞ sig₂
out (cons x y) = inj₂ (cons' , α)
  where
    α : Sh sig₂ cons' → T∞ sig₂
    α zero    = x
    α (suc _) = y

-- | Coinductive conlusion for the rule
-- from(S x, y) ⇒ from(x, cons (x, y)).
-- Note that we need to encode this as
-- from(S x, y) ∧ x ≡ x' ⇒ from(x, cons (x', y)).
From-Enc : (T∞ sig₂ → T∞ sig₂ → Set) → T∞ sig₂ → T∞ sig₂ → Set
From-Enc G x y with (out y)
... | inj₁ tt            = ⊥ -- no clause for from(x, •)
... | inj₂ (inj₁ tt , _) = ⊥ -- neither for from(x, S y)
... | inj₂ (inj₂ tt , α) =   -- from(S x, y) ∧ x ≡ x' ⇒ from(x, cons (x', y))
  let x' = α zero
      y  = α (suc zero)
  in x ≡ x' × G (S x) y

-- | Define From as coinductive relation.
record From (x y : T∞ sig₂) : Set where
  coinductive
  field
    out-From : From-Enc From x y
open From

----- Below, we construct for each x : T∞ sig₂ a term tₓ that is related to x
----- via From, and prove that this is indeed the case.

-- | t x = cons x (cons (s x) ...
t : T∞ sig₂ → T∞ sig₂
out (t x) = inj₂ (cons' , α)
  where
    α : Sh sig₂ cons' → T∞ sig₂
    α zero    = x
    α (suc _) = t (S x)

-- | Prove that x and tₓ are related via From.
lem : (x : T∞ sig₂) → From x (t x)
out-From (lem x) = (refl , lem (S x))

-- | From is inhabitated if T∞ sig₂ is.
thm : (x : T∞ sig₂) → ∃ λ y → From x y
thm x = , (lem x)

----------------------------------------
-- Different approach to show that From is inhabited:
-- The separate definition of T∞ and From makes it impossible, or at least
-- extremly difficult, to construct y and From x y at the same time.
-- The predicate ∃-From x thus simultaneously defines a special existential
-- quantifier for T∞ sig₂ that ensures that the given witness y fulfills
-- From x y.
-- Note that elements of ∃-From contain a lot of junk, as we always just use
-- the root of a tree. This make the first projection rather complicated, see
-- p₁. I guess, this could be made more economical.

∃-From-Enc : ∀{i} → (T∞ {i} sig₂ → Set) → T∞ {i} sig₂ → Set
∃-From-Enc {i} G x = Σ (⟪ sig₂ ⟫ (T∞ sig₂)) m
  where
    m : ⟪ sig₂ ⟫ (T∞ {i} sig₂) → Set
    m (inj₁ tt , _) = ⊥
    m (inj₂ tt , α) =
      let x' = α zero
          y  = α (suc zero)
      in x ≡ x' × G (S x)

record ∃-From {i : Size} (x : T∞ {i} sig₂) : Set where
  coinductive
  field
    out-∃-From : {j : Size< i} → ∃-From-Enc (∃-From {j}) x
open ∃-From

postulate
  T∞-ext : ∀{C} → (x y : T∞ C) → out x ≡ out y → x ≡ y

-- | Project out the witness.
p₁ : ∀ {i x} → ∃-From {i} x → T∞ {i} sig₂
out (p₁ u) {j} with out-∃-From u
... | (inj₁ tt , _) , ()
... | (inj₂ tt , α) , q , u' = inj₂ (cons' , α')
  where
    t' = p₁ u'
    α' : Fin 2 → T∞ {j} sig₂
    α' zero    = α zero
    α' (suc _) = t'

p₂ : ∀ {x} → (u : ∃-From x) → From x (p₁ u)
out-From (p₂ {x} u) = {!!}
  where
    m : (v : ∃-From-Enc ∃-From x) → v ≡ out-∃-From u → From-Enc From x (p₁ u)
    m v p with v
    ... | ((inj₁ tt , _) , ())
    ... | ((inj₂ tt , α) , q , u') = {!!} -- subst (From-Enc From x) s m'
      where
        v' : From (S x) (p₁ u')
        v' = p₂ u'

        α' : Fin 2 → T∞ sig₂
        α' zero    = α zero
        α' (suc _) = p₁ u'

        s : ∀ {α q u'} → ((inj₂ tt , α) , q , u') ≡ out-∃-From u →
            record { out = inj₂ (cons' , α') } ≡ p₁ u
        s p with out-∃-From u
        s p | r = {!!}

{-
        s p with out-∃-From u
        s p | (inj₁ tt , _) , ()
        s p | ((inj₂ tt , α₁) , q₁ , u'₁) = ?
        --  T∞-ext (record { out = inj₂ (cons' , α') }) (p₁ u) {!!}
-}

        m' : From-Enc From x (record { out = inj₂ (cons' , α') })
        m' = (q , v')

thm₂ : ∀{i} → (x : T∞ {i} sig₂) → ∃-From {i} x
out-∃-From (thm₂ {i} x) {j} = ((cons' , α) , refl , u)
  where
    u = thm₂ {j} (S x)

    α : Sh sig₂ cons' → T∞ {j} sig₂
    α zero    = x
    α (suc _) = p₁ u

---------------------
-- Some other tries
--------------------
{-
F : (ℕ → Set) → ℕ → Set
F G 0       = ⊤
F G (suc n) = G n

record NatLp (n : ℕ) : Set where
  coinductive
  field
    out : F NatLp n
open NatLp

lem : (n : ℕ) → NatLp n
out (lem zero)    = tt
out (lem (suc n)) = lem n

record bad (A : Set) (a : A) : Set where
  coinductive
  field
    bad-out : bad A a
open bad

bad-lem : (n : ℕ) → bad ℕ n
bad-out (bad-lem n) = bad-lem n

-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Sets.EquivalenceRelations
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Functions.Definition

module Fields.Orders.LeastUpperBounds.Examples {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {_} {c} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {pOrderedRing : PartiallyOrderedRing R pOrder} (orderedRing : TotallyOrderedRing pOrderedRing) (F : Field R) (isNontrivial : Setoid._∼_ S (Ring.0R R) (Ring.1R R) → False) where

open PartiallyOrderedRing pOrderedRing
open Setoid S
open Equivalence eq
open SetoidTotalOrder (TotallyOrderedRing.total orderedRing)
open Field F
open Ring R
open SetoidPartialOrder pOrder
open Group additiveGroup
open import Rings.Orders.Partial.Lemmas pOrderedRing
open import Rings.Orders.Total.Lemmas orderedRing
open import Fields.Orders.LeastUpperBounds.Definition pOrder

charNot2 : Setoid._∼_ S (Ring.1R R + Ring.1R R) (Ring.0R R) → False
charNot2 = orderedImpliesCharNot2 nontrivial

openIntervalPred : (a : A) → (b : A) → a < b → A → Set _
openIntervalPred a b a<b x = (a < x) && (x < b)

openInterval : (a : A) → (b : A) → (a<b : a < b) → subset S (openIntervalPred a b a<b)
openInterval a b a<b x=y (a<x ,, x<b) = SetoidPartialOrder.<WellDefined pOrder reflexive x=y a<x ,, SetoidPartialOrder.<WellDefined pOrder x=y reflexive x<b

1/2 : A
1/2 with allInvertible (1R + 1R) charNot2
... | n , _ = n

1/2Is1/2 : 1/2 * (1R + 1R) ∼ 1R
1/2Is1/2 with allInvertible (1R + 1R) charNot2
... | n , pr = pr

1/2Is1/2' : (1/2 + 1/2) ∼ 1R
1/2Is1/2' = transitive (+WellDefined (symmetric identIsIdent) (symmetric identIsIdent)) (transitive (transitive (symmetric *DistributesOver+') *Commutative) 1/2Is1/2)

halfHalves : (a : A) → ((a + a) * 1/2) ∼ a
halfHalves a = transitive *DistributesOver+' (transitive (transitive (transitive (symmetric *DistributesOver+) (*WellDefined reflexive 1/2Is1/2')) *Commutative) identIsIdent)

0<1/2 : 0R < 1/2
0<1/2 = halvePositive 1/2 (<WellDefined reflexive (symmetric (transitive (symmetric (transitive *DistributesOver+ (+WellDefined (transitive *Commutative identIsIdent) (transitive *Commutative identIsIdent)))) 1/2Is1/2)) (0<1 nontrivial))

min<mean : (a b : A) → a < b → a < ((a + b) * 1/2)
min<mean a b a<b = <WellDefined (transitive *DistributesOver+' (transitive (+WellDefined *Commutative *Commutative) (transitive (symmetric *DistributesOver+') (transitive (*WellDefined 1/2Is1/2' reflexive) identIsIdent)))) reflexive a+a<a+b
  where
    a+a<a+b : ((a + a) * 1/2) < ((a + b) * 1/2)
    a+a<a+b = ringCanMultiplyByPositive 0<1/2 (<WellDefined reflexive groupIsAbelian (orderRespectsAddition a<b a))

mean<max : (a b : A) → a < b → ((a + b) * 1/2) < b
mean<max a b a<b = <WellDefined reflexive (halfHalves b) a+b<b+b
  where
    a+b<b+b : ((a + b) * 1/2) < ((b + b) * 1/2)
    a+b<b+b = ringCanMultiplyByPositive 0<1/2 (orderRespectsAddition a<b b)

example1 : (a b : A) (a<b : a < b) → LeastUpperBound (openInterval a b a<b) b
LeastUpperBound.upperBound (example1 a b a<b) y (a<y ,, y<b) = inl y<b
LeastUpperBound.leastUpperBound (example1 a b a<b) y isUpperBound with totality b y
LeastUpperBound.leastUpperBound (example1 a b a<b) y isUpperBound | inl (inl x) = inl x
LeastUpperBound.leastUpperBound (example1 a b a<b) y isUpperBound | inl (inr y<b) = exFalso false
  where
    betterBound : A
    betterBound = (y + b) * 1/2
    p1 : ((y + b) * 1/2) < ((b + b) * 1/2)
    p1 = ringCanMultiplyByPositive 0<1/2 (orderRespectsAddition y<b b)
    p2 : betterBound < b
    p2 = <WellDefined reflexive (transitive (*WellDefined (transitive (symmetric (+WellDefined identIsIdent identIsIdent)) (transitive (+WellDefined *Commutative *Commutative) (symmetric *DistributesOver+))) reflexive) (transitive (symmetric *Associative) (transitive (transitive (*WellDefined reflexive (transitive *Commutative 1/2Is1/2)) *Commutative) identIsIdent))) p1
    a<y : a < y
    a<y with isUpperBound ((a + b) * 1/2) (min<mean a b a<b ,, mean<max a b a<b)
    a<y | inl a+b/2<y = <Transitive (min<mean a b a<b) a+b/2<y
    a<y | inr a+b/2=y = <WellDefined reflexive a+b/2=y (min<mean a b a<b)
    p3 : ((a + a) * 1/2) < ((y + b) * 1/2)
    p3 = ringCanMultiplyByPositive 0<1/2 (ringAddInequalities a<y a<b)
    a<betterBound : a < betterBound
    a<betterBound = <WellDefined (halfHalves a) reflexive p3
    bad : (betterBound < y) || (betterBound ∼ y)
    bad = isUpperBound betterBound (a<betterBound ,, p2)
    false : False
    false with bad
    false | inl mean<y with min<mean y b y<b
    ... | y<mean = irreflexive (<Transitive y<mean mean<y)
    false | inr x = irreflexive (<WellDefined (symmetric x) reflexive (min<mean y b y<b))
LeastUpperBound.leastUpperBound (example1 a b a<b) y isUpperBound | inr x = inr x


text:
-- Andreas, 2020-04-15, issue #4586
-- Better error message when `let` contains an absurd pattern.

test : Set₁
test = let f ()
       in  Set

-- WAS:
-- Not a valid let-declaration
-- when scope checking let f () in Set

-- EXPECTED:
-- Missing right hand side in let binding
-- when scope checking let f () in Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2014-05-02
-- As of now, we have no negative integer literals, and these parse as identifiers.

module _ where

open import Common.Prelude

n : Nat
n = -1

-- Should give error "not in scope: -1"


text:
module UnSizedIO.ConsoleObject where

open import UnSizedIO.Console
open import UnSizedIO.Object
open import UnSizedIO.IOObject

-- A console object is an IO object for the IO interface  of console
ConsoleObject : (iface : Interface) → Set
ConsoleObject iface = IOObject ConsoleInterface iface

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propertiers of any for containers
------------------------------------------------------------------------

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

module Data.Container.Morphism.Properties where

open import Level using (_⊔_; suc)
open import Function as F using (_$_)
open import Data.Product using (∃; proj₁; proj₂; _,_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)

open import Data.Container.Core
open import Data.Container.Morphism
open import Data.Container.Relation.Binary.Equality.Setoid

-- Identity

module _ {s p} (C : Container s p) where

  id-correct : ∀ {x} {X : Set x} → ⟪ id C ⟫ {X = X} ≗ F.id
  id-correct x = P.refl

-- Composition.

module _ {s₁ s₂ s₃ p₁ p₂ p₃}
         {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} {C₃ : Container s₃ p₃}
         where

  ∘-correct : (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) → ∀ {x} {X : Set x} →
              ⟪ f ∘ g ⟫ {X = X} ≗ (⟪ f ⟫ F.∘ ⟪ g ⟫)
  ∘-correct f g xs = P.refl

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where

  -- Naturality.

  Natural : ∀ x e → (∀ {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) →
            Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂ ⊔ suc (x ⊔ e))
  Natural x e m =
    ∀ {X : Set x} (Y : Setoid x e) → let module Y = Setoid Y in
    (f : X → Y.Carrier) (xs : ⟦ C₁ ⟧ X) →
    Eq Y C₂ (m $ map f xs) (map f $ m xs)

  -- Container morphisms are natural.

  natural : ∀ (m : C₁ ⇒ C₂) x e → Natural x e ⟪ m ⟫
  natural m x e Y f xs = refl Y C₂

module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where

  -- Natural transformations.

  NT : ∀ x e → Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂ ⊔ suc (x ⊔ e))
  NT x e = ∃ λ (m : ∀ {X : Set x} → ⟦ C₁ ⟧ X → ⟦ C₂ ⟧ X) → Natural x e m

module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where

  -- All natural functions of the right type are container morphisms.

  complete : ∀ {e} → (nt : NT C₁ C₂ p₁ e) →
      ∃ λ m → (X : Setoid p₁ e) → let module X = Setoid X in
      ∀ xs → Eq X C₂ (proj₁ nt xs) (⟪ m ⟫ xs)
  complete (nt , nat) =
    (m , λ X xs → nat X (proj₂ xs) (proj₁ xs , F.id)) where

    m : C₁ ⇒ C₂
    m .shape    = λ s → proj₁ (nt (s , F.id))
    m .position = proj₂ (nt (_ , F.id))


text:
module Issue488 where

open import Data.Product using (∃-syntax; -,_; _×_; _,_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)

module CounterExample where

  data Term : Set where
    A B C D : Term

  data _—→_ : (M N : Term) → Set where
    B—→C : B —→ C
    C—→B : C —→ B
    B—→A : B —→ A
    C—→D : C —→ D

  infix  2 _—↠_
  infix  1 begin_
  infixr 2 _—→⟨_⟩_
  infix  3 _∎

  data _—↠_ : Term → Term → Set where
    _∎ : ∀ M
      ---------
      → M —↠ M

    _—→⟨_⟩_ : ∀ L {M N}
      → L —→ M
      → M —↠ N
        ---------
      → L —↠ N

  begin_ : ∀ {M N}
    → M —↠ N
      ------
    → M —↠ N
  begin M—↠N = M—↠N

  diamond : ∀ {L M N}
    → ((L —→ M) × (L —→ N))
      -----------------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P))
  diamond (B—→A , B—→A) = -, ((A ∎) , (A ∎))
  diamond (C—→B , C—→B) = -, ((B ∎) , (B ∎))
  diamond (B—→C , B—→C) = -, ((C ∎) , (C ∎))
  diamond (C—→D , C—→D) = -, ((D ∎) , (D ∎))
  diamond (B—→C , B—→A) = -, ((begin C —→⟨ C—→B ⟩ B —→⟨ B—→A ⟩ A ∎) , (A ∎))
  diamond (C—→B , C—→D) = -, ((begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎) , (D ∎))
  diamond (B—→A , B—→C) = -, ((A ∎) , (begin C —→⟨ C—→B ⟩ B —→⟨ B—→A ⟩ A ∎))
  diamond (C—→D , C—→B) = -, ((D ∎) , (begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎))

  A—↠A : ∀ {P} → A —↠ P → P ≡ A
  A—↠A (.A ∎) = refl

  D—↠D : ∀ {P} → D —↠ P → P ≡ D
  D—↠D (.D ∎) = refl

  ¬confluence : ¬ (∀ {L M N}
    → ((L —↠ M) × (L —↠ N))
      -----------------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P)))
  ¬confluence confluence
    with confluence ( (begin B —→⟨ B—→A ⟩ A ∎)
                    , (begin B —→⟨ B—→C ⟩ C —→⟨ C—→D ⟩ D ∎) )
  ... | (P , (A—↠P , D—↠P))
    with trans (sym (A—↠A A—↠P)) (D—↠D D—↠P)
  ... | ()

module DeterministicImpliesDiamondPropertyAndConfluence where

  infix  2 _—↠_
  infix  1 begin_
  infixr 2 _—→⟨_⟩_
  infix  3 _∎

  postulate
    Term : Set
    _—→_ : Term → Term → Set

  postulate
    deterministic : ∀ {L M N}
      → L —→ M
      → L —→ N
      ------
      → M ≡ N

  data _—↠_ : Term → Term → Set where
    _∎ : ∀ M
      ---------
      → M —↠ M

    _—→⟨_⟩_ : ∀ L {M N}
      → L —→ M
      → M —↠ N
        -------
      → L —↠ N

  begin_ : ∀ {M N}
    → M —↠ N
      ------
    → M —↠ N
  begin M—↠N = M—↠N

  diamond : ∀ {L M N}
    → ((L —→ M) × (L —→ N))
      --------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P))
  diamond (L—→M , L—→N)
    rewrite deterministic L—→M L—→N = -, ((_ ∎) , (_ ∎))

  confluence : ∀ {L M N}
    → (L —↠ M)
    → (L —↠ N)
      --------------------
    → ∃[ P ] ((M —↠ P) × (N —↠ P))
  confluence {L} {.L} { N} (.L ∎) L—↠N = -, (L—↠N , (N ∎))
  confluence {L} { M} {.L} L—↠M (.L ∎) = -, ((M ∎) , L—↠M)
  confluence {L} { M} { N} (.L —→⟨ L—→M′ ⟩ M′—↠M) (.L —→⟨ L—→N′ ⟩ N′—↠N)
    rewrite deterministic L—→M′ L—→N′ = confluence M′—↠M N′—↠N


text:
module SizedPolyIO.Console where

open import Level using () renaming (zero to lzero)
open import Size

open import NativePolyIO
open import SizedPolyIO.Base

data ConsoleCommand : Set where
  putStrLn : String → ConsoleCommand
  getLine  : ConsoleCommand

ConsoleResponse : ConsoleCommand → Set
ConsoleResponse (putStrLn s) = Unit
ConsoleResponse  getLine     = String

consoleI : IOInterface lzero lzero
Command  consoleI  = ConsoleCommand
Response consoleI  = ConsoleResponse

IOConsole : Size → Set → Set
IOConsole i = IO consoleI i

IOConsole+ : Size → Set → Set
IOConsole+ i = IO+ consoleI i

translateIOConsoleLocal : (c : ConsoleCommand) → NativeIO (ConsoleResponse c)
translateIOConsoleLocal (putStrLn s) = nativePutStrLn s
translateIOConsoleLocal getLine      = nativeGetLine

translateIOConsole : {A : Set} → IOConsole ∞ A → NativeIO A
translateIOConsole = translateIO translateIOConsoleLocal

main : NativeIO (Unit {lzero})
main = nativePutStrLn "Console"


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Lists.Lists
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Decidable.Sets
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Semiring

module Computability.LambdaCalculus.Definition where

open import UnorderedSet.Definition (ℕDecideEquality)

data Term : Set where
  var : (v : ℕ) → Term
  lam : (x : ℕ) → Term → Term
  apply : Term → Term → Term


text:
module StateSizedIO.Base where

open import Size
open import SizedIO.Base

open import Data.Product

record IOInterfaceˢ  : Set₁ where
  field
    IOStateˢ   : Set
    Commandˢ   : IOStateˢ → Set
    Responseˢ  : (s : IOStateˢ) → (m : Commandˢ s) → Set
    IOnextˢ      : (s : IOStateˢ) → (m : Commandˢ s) → (Responseˢ s m) → IOStateˢ
open IOInterfaceˢ public

record Interfaceˢ : Set₁ where
  field
    Stateˢ     : Set
    Methodˢ   : Stateˢ → Set
    Resultˢ  : (s : Stateˢ) → (m : Methodˢ s) → Set
    nextˢ      : (s : Stateˢ) → (m : Methodˢ s) → (Resultˢ s m) → Stateˢ
open Interfaceˢ public

module _  (ioi  : IOInterface)  (let C  = Command ioi)  (let R   = Response ioi)
          (oi   : Interfaceˢ)   (let S = Stateˢ oi) (let M  = Methodˢ oi)    (let Rt  = Resultˢ oi)
                                (let n = nextˢ oi)
  where

  record IOObjectˢ (i : Size) (s : Stateˢ) : Set where
    coinductive
    field
      method : ∀{j : Size< i} (m : M s) → IO ioi ∞ ( Σ[ r ∈ Rt s m ] IOObjectˢ j (n s m r))

open IOObjectˢ public

module _ (I : IOInterfaceˢ )
         (let S = IOStateˢ I) (let C = Commandˢ I)
         (let R = Responseˢ I) (let n = nextˢ I)
           where

  mutual
    record IOˢ (i : Size)  (A : S → Set) (s : S) : Set where
      coinductive
      constructor delay
      field
        forceˢ : {j : Size< i} → IOˢ' j A s

    data IOˢ' (i : Size)  (A : S → Set) (s : S) : Set where
      doˢ'      : (c : C s) (f : (r : R s c) → IOˢ i A (n s c r)) → IOˢ' i A s
      returnˢ' : (a : A s) → IOˢ' i A s

    data IOˢ+ (i : Size)  (A : S → Set) (s : S) : Set where
      do' : (c : C s)  (f : (r : R s c) → IOˢ i A (n s c r)) → IOˢ+ i A s

open IOˢ public

module _  {I : IOInterfaceˢ }
          (let S = Stateˢ I) (let C = Commandˢ I)
          (let R = Responseˢ I) (let n = nextˢ I)
           where
  returnˢ : ∀{i}{A : S → Set} (s : S) (a : A s) → IOˢ I i A s
  forceˢ (returnˢ s a) = returnˢ' a

  doˢ : ∀{i}{A : S → Set} (s : S) (c : C s)
           (f : (r : R s c) → IOˢ I i A (n s c r))
           → IOˢ I i A s
  forceˢ (doˢ s c f) = doˢ' c f


text:
open import Categories
open import Functors
import RMonads

module RMonads.RKleisli
  {a b c d}
  {C : Cat {a}{b}}
  {D : Cat {c}{d}}
  {J : Fun C D}
  (M : RMonads.RMonad J) where

open import Library
open RMonads.RMonad M
open Cat
open Fun

Kl : Cat
Kl = record{
  Obj  = Obj C;
  Hom  = λ X Y → Hom D (OMap J X) (T Y);
  iden = η;
  comp = λ f g → comp D (bind f) g;
  idl  = λ{X}{Y}{f} →
    proof
    comp D (bind η) f
    ≅⟨ cong (λ g → comp D g f) law1 ⟩
    comp D (iden D) f
    ≅⟨ idl D ⟩
    f
    ∎;
  idr  = law2;
  ass  =  λ{_ _ _ _ f g h} →
    proof
    comp D (bind (comp D (bind f) g)) h
    ≅⟨ cong (λ f → comp D f h) law3 ⟩
    comp D (comp D (bind f) (bind g)) h
    ≅⟨ ass D ⟩
    comp D (bind f) (comp D (bind g) h)
    ∎}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
----------------------------------------------------------------------
--                                                                  --
-- Author  : Jan Stolarek <jan.stolarek@p.lodz.pl>                  --
-- License : Public Domain                                          --
--                                                                  --
-- This module contains Agda implementation of code presented in    --
-- "Why Dependent Types Matter" by Thorsten Altenkirch, Conor       --
-- McBride and James McKinna. Original code in the paper was        --
-- written in Epigram but with its official web page offline        --
-- Epigram seems to be dead. Original paper elides details of some  --
-- proofs. I supplied the missing parts so that this module is      --
-- complete and self-contained. I avoided using the standard        --
-- library to show how the proofs are constructed from              --
-- scratch. This means I have to reinvent some of basic things like --
-- natural numbers, lists or vector. Some of the code below is not  --
-- mine, in which case I refer to the original source. If you're    --
-- reading "Why Dependent Types Matter" I encourage you to try and  --
-- implement all the code by yourself. I assure you that this will  --
-- be very rewarding.                                               --
--                                                                  --
-- This code was written and tested in Agda 2.3.2.1. YMMV           --
--                                                                  --
----------------------------------------------------------------------

module WhyDependentTypesMatter where

-- Reinventing the wheel: we will need a type of pairs to implement
-- deal function that splits list into a pair of lists. Sg is in fact
-- type of dependent pairs. This code is taken from Conor McBride:
-- https://github.com/pigworker/MetaprogAgda/blob/master/Basics.agda
record Sg (S : Set)(T : S → Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg public
_×_ : Set → Set → Set
S × T = Sg S λ _ → T
infixr 4 _,_ _×_

-- Section 1 : Introduction
-- ~~~~~~~~~~~~~~~~~~~~~~~~
-- Standard implementation of merge sort with no dependent types. This
-- implements code shown in the paper in Figure 1.

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Order : Set where
  le ge : Order

data List (X : Set) : Set where
  nil  : List X
  _::_ : X → List X → List X

order : Nat → Nat → Order
order zero    y       = le
order (suc x) zero    = ge
order (suc x) (suc y) = order x y

-- deal splits a list into a pair of lists. If the input list has even length
-- then the output lists have the same length. If input has odd length then
-- first output list is longer by one.
deal : {X : Set} → List X → List X × List X
deal nil        = nil , nil
deal (x :: nil) = x :: nil , nil
deal (y :: (z :: xs)) with deal xs
deal (y :: (z :: xs)) | ys , zs = y :: ys , z :: zs

-- We have a small problem with merge and sort functions - Agda's termination
-- checker complains about merge and sort. The problem is that it doesn't see
-- that parameteres to merge are actually getting smaller in the recursive
-- calls. This results from the usage of "with" pattern, which is desugared to
-- an auxiliary function (say, "go"). Here's an explanation from Andreas Abel:
--
-- the termination checker refutes this call pattern.
--
--    merge (x :: xs) (y :: ys)
--       --> go x xs y ys ...
--       --> merge xs (y :: ys)
--
-- The termination checker sees that in merge-->go, the arguments all become
-- smaller, but in go--->merge, one argument becomes bigger. Since it has
-- simplistic, it cannot remember where y and ys came from and that taken
-- together, they are actually the same as we started out.
--
-- See Andreas' full explanation on Agda mailing list here:
-- https://lists.chalmers.se/pipermail/agda/2013/005948.html
--
-- I could rewrite the code to avoid this problem, but I'm leaving it as-is
-- because IMO it teaches something important about Agda's termination checker.
merge : List Nat → List Nat → List Nat
merge nil       ys             = ys
merge xs        nil            = xs
merge (x :: xs) (y :: ys) with order x y
merge (x :: xs) (y :: ys) | le = x :: merge xs (y :: ys)
merge (x :: xs) (y :: ys) | ge = y :: merge (x :: xs) ys

-- After I posted the original code I realized that it is not obvious that this
-- function is total. We know that (deal xs) is smaller than xs, but I think
-- that this isn't obvious.
sort : List Nat → List Nat
sort xs with deal xs
sort xs | ys , nil = ys
sort xs | ys , zs  = merge (sort ys) (sort zs)

-- Section 3.1 : Totality is Good for more than the Soul
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Here we reinvent another wheel - refl

data _≡_ {S : Set} (s : S) : S → Set where
  refl : s ≡ s

infixl 1 _≡_

-- Section 3.2 : Defusing General Recursion
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- Merge sort with explicit structure of recursion.

data Parity : Set where
  p0 p1 : Parity

data DealT (X : Set) : Set where
  empT  : DealT X
  leafT : X → DealT X
  nodeT : Parity → DealT X → DealT X → DealT X

insertT : {X : Set} → X → DealT X → DealT X
insertT x empT = leafT x
insertT x (leafT y) = nodeT p0 (leafT y) (leafT x)
insertT x (nodeT p0 l r) = nodeT p1 (insertT x l) r
insertT x (nodeT p1 l r) = nodeT p0 l (insertT x r)

dealT : {X : Set} → List X → DealT X
dealT nil = empT
dealT (x :: xs) = insertT x (dealT xs)

mergeT : DealT Nat → List Nat
mergeT empT = nil
mergeT (leafT x) = x :: nil
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)

-- In the paper this function is called sort. Here and in other places I rename
-- functions to avoid name clashes.
sortT : List Nat → List Nat
sortT xs = mergeT (dealT xs)

-- Section 4 : Maintaining Invariants by Static Indexing
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-- Note that I'm using (suc n) instead of (1 + n). Why?
-- becuase I'm not using Agda's BUILTIN pragmas, so I'd
-- have to write (suc zero) instead of 1. This doesn't
-- change much in the proofs we'll be doing.
data Vec (X : Set) : Nat → Set where
  vnil  : Vec X zero
  vcons : {n : Nat} → X → Vec X n → Vec X (suc n)

vtail : {X : Set} {n : Nat} → Vec X (suc n) → Vec X n
vtail (vcons x xs) = xs

-- @ is a reserved sign in Agda, so I'm using vapp to denote
-- vectorized application.
vapp : {A B : Set} {n : Nat} → Vec (A → B) n → Vec A n → Vec B n
vapp vnil         vnil         = vnil
vapp (vcons f fs) (vcons s ss) = vcons (f s) (vapp fs ss)

_+_ : Nat → Nat → Nat
zero  + n = n
suc m + n = suc (m + n)

infixl 4 _+_

_++_ : {X : Set} {n m : Nat} → Vec X n → Vec X m → Vec X (n + m)
vnil       ++ ys = ys
vcons x xs ++ ys = vcons x (xs ++ ys)

vec : {X : Set} {n : Nat} → X → Vec X n
vec {X} {zero}  x = vnil
vec {X} {suc n} x = vcons x (vec x)

xpose : {X : Set} {n m : Nat} → Vec (Vec X n) m → Vec (Vec X m) n
xpose vnil            = vec vnil
xpose (vcons xj xi'j) = vapp (vapp (vec vcons) xj) (xpose xi'j)

-- Section 4.1 : Static Indexing and Proofs
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- This section is the one that is missing some of the proofs.

vrevacc : {X : Set} {n m : Nat} → Vec X n → Vec X m → Vec X (n + m)
vrevacc vnil         ys = ys
vrevacc (vcons x xs) ys = {!!} -- vrevacc xs (vcons x ys)
-- We can't fill in the correct code, because Agda doesn't know that m + (1 + n)
-- eqauls 1 + (m + n). We will have to prove it.

-- To conduct a proof we will need three properties:
-- a) symmetry: if a equals b then b equals a
sym : {A : Set} → {a b : A} → a ≡ b → b ≡ a
sym refl = refl

-- b) congruence: if a equals b, then (f a) equals (f b)
cong : {A B : Set} (f : A → B) → ∀ {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

-- c) substitution: if we have a proposition that is true for a
-- and a equals b, then proposition is also true for b
subst : {A : Set}(P : A → Set) → {a b : A} → a ≡ b → P a → P b
subst prp refl p = p

-- These three properties were taken from Thorsten Altenkirch's course
-- on Computer Aided Formal Reasoning: http://www.cs.nott.ac.uk/~txa/g53cfr/
-- If you don't know how they work and why do we need them now is a good moment
-- to stop reading "Why Dependent Types Matter" and go through lectures 1-9
-- of Thorsten's course.

plusSuc : (m n : Nat) → suc (m + n) ≡ m + (suc n)
plusSuc zero n = refl
plusSuc (suc m) n = cong suc (plusSuc m n)

vrevacc2 : {X : Set} {n m : Nat} → Vec X n → Vec X m → Vec X (n + m)
vrevacc2                 vnil         ys = ys
vrevacc2 {X} {suc n} {m} (vcons x xs) ys =
  subst (Vec X) (sym (plusSuc n m)) (vrevacc2 xs (vcons x ys))

-- Last line corresponds to
--
--    {[plusSuc m' n⟩} vrevacc2 xs (vcons x ys)
--
-- in the paper. Call to vrevacc2 produces Vec with index n + (suc m). The
-- problem is we need index suc (n + m). We need to prove their equality.  we
-- already proved with plusSuc that suc (n + m) equals n + (suc m). Since now
-- we're proving something opposite we make use of symmetry: we apply sym to
-- plusSuc. Having a proof is not enough - we must apply it to convert from the
-- result produced by vrevacc2 to the result expected by the typechecker. To do
-- this we use subst function. Our proposition is (Vec X). Look at the type
-- signature of subst - the proposition is something that will take an element
-- of Set (in this case Nat) and produce an element of Set. Vec X will return an
-- element of Set (ie a type) when we pass it an index of type Nat. subst
-- replaces (substitutes) index n + (suc m) produced by vrevacc2 with
-- suc (n + m).

plusZero : (n : Nat) → n + zero ≡ n
plusZero zero    = refl
plusZero (suc n) = cong suc (plusZero n)

vrev : {X : Set} {n : Nat} → Vec X n → Vec X n
vrev {X} {n} xs = subst (Vec X) (plusZero n) (vrevacc2 xs vnil)

-- Section 4.2 : Sized Merge-Sort
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-- note that mergeS is a renamed merge from the paper
mergeS : {n m : Nat} → Vec Nat n → Vec Nat m → Vec Nat (n + m)
mergeS {zero } {_    } vnil         ys   = ys
mergeS {suc n} {zero } (vcons x xs) vnil =
  subst (Vec Nat) (sym (plusZero (suc n))) (vcons x xs)
mergeS {suc n} {suc m} (vcons x xs) (vcons y ys) with order x y
mergeS {suc n} {suc m} (vcons x xs) (vcons y ys) | le =
  vcons x (mergeS xs (vcons y ys))
mergeS {suc n} {suc m} (vcons x xs) (vcons y ys) | ge =
  subst (Vec Nat) (plusSuc (suc n) m) (vcons y (mergeS (vcons x xs) ys))

p2n : Parity → Nat
p2n p0 = zero
p2n p1 = suc zero

-- Data types and functions below have S (mnemonic for Sized) appended to their
-- name to avoid name clash.
data DealTS (X : Set) : Nat → Set where
  empT  : DealTS X zero
  leafT : X → DealTS X (suc zero)
  nodeT : {n : Nat} → (p : Parity) → DealTS X (p2n p + n) → DealTS X n
        → DealTS X ((p2n p + n) + n)

mergeTS : {n : Nat} → DealTS Nat n → Vec Nat n
mergeTS empT          = vnil
mergeTS (leafT x)     = vcons x vnil
mergeTS (nodeT p l r) = mergeS (mergeTS l) (mergeTS r)

insertTS : {n : Nat} {X : Set} → X → DealTS X n → DealTS X (suc n)
insertTS x empT               = leafT x
insertTS x (leafT y         ) = nodeT p0 (leafT y) (leafT x)
insertTS x (nodeT     p0 l r) = nodeT p1 (insertTS x l) r
insertTS {.(p2n p1 + n + n)} {X} x (nodeT {n} p1 l r) =
  subst (DealTS X) (sym (cong suc (plusSuc n n))) (nodeT p0 l (insertTS x r))
--                  |    |         |
--                  |    |         +---- suc (n + n) ≡ n + suc n
--                  |    +-------------- suc (suc (n + n)) ≡ suc (n + suc n))
--                  +------------------- suc (n + suc n))  ≡ suc (suc (n + n))
--
-- It took me a while to figure out this proof (though in retrospect it is
-- simple). The expected size of the resulting vector is:
--
--   suc (suc (n + n))
--
-- First suc comes from the type signature of insertTS, second suc comes from
-- p2n p1 (which is suc zero), and n + n comes from nodeT definition. The actual
-- size produced by recursive call to nodeT is:
--
--   suc (n + suc n))
--
-- Outer suc comes from type signature, n is size of l, suc n is size of new r
-- (ie. r with x inserted into it).

dealTS : {X : Set} {n : Nat} → Vec X n → DealTS X n
dealTS vnil = empT
dealTS (vcons x xs) = insertTS x (dealTS xs)

sortTS : {n : Nat} → Vec Nat n → Vec Nat n
sortTS xs = mergeTS (dealTS xs)

-- Section 5.1 : Evidence of Ordering
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data _≤_ : Nat → Nat → Set where
  le0 : {y : Nat} → zero ≤ y
  leS : {x : Nat} {y : Nat} → x ≤ y → suc x ≤ suc y

data OrderD : Nat → Nat → Set where
  le : {x : Nat} {y : Nat} → x ≤ y → OrderD x y
  ge : {x : Nat} {y : Nat} → y ≤ x → OrderD x y

orderD : (x : Nat) → (y : Nat) → OrderD x y
orderD zero    y       = le le0
orderD (suc x) zero    = ge le0
orderD (suc x) (suc y) with orderD x y
orderD (suc x) (suc y) | le xley = le (leS xley)
orderD (suc x) (suc y) | ge ylex = ge (leS ylex)

leRefl : {x : Nat} → x ≤ x
leRefl {zero}  = le0
leRefl {suc x} = leS leRefl

leTrans : {x y z : Nat} → x ≤ y → y ≤ z → x ≤ z
leTrans le0      yz       = le0
leTrans (leS xy) (leS yz) = leS (leTrans xy yz)

leASym : {x y : Nat} → x ≤ y → y ≤ x → x ≡ x
leASym le0      le0      = refl
leASym (leS xy) (leS yx) = refl

-- Second equation for leASym is surprisingly simple. I admit I don't fully
-- understand why I could simply use refl here, without doing inductive proof.

-- Section 5.2 : Locally Sorted Lists
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-- LNat = Nat lifted with infinity
data LNat : Set where
  zero : LNat
  suc  : LNat → LNat
  inf  : LNat

lift : Nat → LNat
lift zero    = zero
lift (suc x) = suc (lift x)

-- In the paper ≤ is used for comparisons on lifted Nats. I'm using ≤' to avoid
-- name clash.
data _≤'_ : LNat → LNat → Set where
  le0 : {y : LNat} → zero ≤' y
  leS : {x : LNat} {y : LNat} → x ≤' y → suc x ≤' suc y
  leI : {x : LNat} → x ≤' inf

data CList : LNat → Set where
  cnil  : CList inf
  ccons : {y : LNat} → (x : Nat) → (lift x) ≤' y → CList y → CList (lift x)
--                                          |
--              +---------------------------+
--              +--> Paper compares lifted and unlifted Nat using ≤.
--                   This seems incorrect or at least unprecise.

-- The problem with CList is that we can't create it if we don't know the least
-- element. That's why the paper says sort is bound by min.
clist : CList zero
clist = ccons zero le0 (
        ccons (suc (suc zero)) (leS (leS le0)) (
        ccons (suc (suc zero))  leI cnil))

data OList : Nat → Set where
  onil  : {b : Nat} → OList b
  ocons : {b : Nat} → (x : Nat) → b ≤ x → OList x → OList b

-- With OList we can just create the list by saying it is bound by zero.
olist : OList zero
olist = ocons (suc zero) le0 onil

olist2 : OList zero
olist2 = ocons (suc zero) le0 (ocons (suc (suc zero)) (leS le0) onil)

-- mergeO (ie. merge for open-bounds lists) has the same problem that we've seen
-- earlier with merge and sort - termination checker complains because we use
-- "with" pattern.
mergeO : {b : Nat} → OList b → OList b → OList b
mergeO onil ys = ys
mergeO (ocons x blex xs) onil = ocons x blex xs
mergeO (ocons x blex xs) (ocons y bley ys) with orderD x y
mergeO (ocons x blex xs) (ocons y bley ys) | le xley =
  ocons x blex (mergeO xs (ocons y xley ys))
mergeO (ocons x blex xs) (ocons y bley ys) | ge ylex =
  ocons y bley (mergeO (ocons x ylex xs) ys)

-- The important thing here is that both lists passed to mergeO must share their
-- lower bound. That's why we have to replace old evidence of ordering (bley in
-- the first case) with the new one (xley).

mergeTO : DealT Nat → OList zero
mergeTO empT          = onil
mergeTO (leafT x)     = ocons x le0 onil
mergeTO (nodeT p l r) = mergeO (mergeTO l) (mergeTO r)

sortO : List Nat → OList zero
sortO xs = mergeTO (dealT xs)

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
-- Andreas, 2019-04-10, issue #3687, name mayhem when printing module contents (C-c C-o)

-- {-# OPTIONS -v interaction.contents.record:20 #-}

record Cat : Set₁ where
  field
    Obj   : Set
    Hom   : (A B : Obj) → Set
    Eq    : ∀{A B} (f g : Hom A B) → Set
    id    : (A : Obj) → Hom A A
    comp  : ∀{A B C} (f : Hom B C) (g : Hom A B) → Hom A C

record Functor (C1 C2 : Cat) : Set where

record FunEq {C D : Cat} (F G : Functor C D) : Set₁ where
  field
    eqMap : ∀{c d} (f g : Cat.Hom C c d) (eq : Cat.Eq C f g) → Set

test : ∀ C D (F G : Functor C D) → FunEq F G
FunEq.eqMap (test C D F G) f g f=g = {!D!}  -- C-c C-o

-- In the output, the names are completely garbled:

-- Names
--   Obj  : Set
--   Hom  : f=g → f=g → Set
--   Eq   : {A B : g} → f=g A B → f=g A B → Set
--   id   : (A : f) → g A A
--   comp : {A B : d} {C = C₁ : d} → f B C₁ → f A B → f A C₁

-- test/interaction$ make AGDA_BIN=agda-2.5.1.1 Issue3687.cmp

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Data.Nat.Base where

open import Cubical.Core.Primitives

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

predℕ : ℕ → ℕ
predℕ zero    = 0
predℕ (suc n) = n

caseNat : ∀ {ℓ} → {A : Type ℓ} → (a0 aS : A) → ℕ → A
caseNat a0 aS 0       = a0
caseNat a0 aS (suc n) = aS

doubleℕ : ℕ → ℕ
doubleℕ 0 = 0
doubleℕ (suc x) = suc (suc (doubleℕ x))

-- doublesℕ n m = 2^n * m
doublesℕ : ℕ → ℕ → ℕ
doublesℕ 0 m = m
doublesℕ (suc n) m = doublesℕ n (doubleℕ m)

-- iterate
iter : ∀ {ℓ} {A : Type ℓ} → ℕ → (A → A) → A → A
iter zero f z    = z
iter (suc n) f z = f (iter n f z)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Universe {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance

open import Tools.Embedding

-- Helper function for reducible terms of type U for specific type derivations.
univEq′ : ∀ {l Γ A} ([U] : Γ ⊩⟨ l ⟩U) → Γ ⊩⟨ l ⟩ A ∷ U / U-intr [U] → Γ ⊩⟨ ⁰ ⟩ A
univEq′ (noemb (Uᵣ .⁰ 0<1 ⊢Γ)) (Uₜ A₁ d typeA A≡A [A]) = [A]
univEq′ (emb 0<1 x) (ιx [A]) = univEq′ x [A]

-- Reducible terms of type U are reducible types.
univEq : ∀ {l Γ A} ([U] : Γ ⊩⟨ l ⟩ U) → Γ ⊩⟨ l ⟩ A ∷ U / [U] → Γ ⊩⟨ ⁰ ⟩ A
univEq [U] [A] = univEq′ (U-elim [U])
                         (irrelevanceTerm [U] (U-intr (U-elim [U])) [A])

-- Helper function for reducible term equality of type U for specific type derivations.
univEqEq′ : ∀ {l l′ Γ A B} ([U] : Γ ⊩⟨ l ⟩U) ([A] : Γ ⊩⟨ l′ ⟩ A)
         → Γ ⊩⟨ l ⟩ A ≡ B ∷ U / U-intr [U]
         → Γ ⊩⟨ l′ ⟩ A ≡ B / [A]
univEqEq′ (noemb (Uᵣ .⁰ 0<1 ⊢Γ)) [A]
          (Uₜ₌ A₁ B₁ d d′ typeA typeB A≡B [t] [u] [t≡u]) =
  irrelevanceEq [t] [A] [t≡u]
univEqEq′ (emb 0<1 x) [A] (ιx [A≡B]) = univEqEq′ x [A] [A≡B]

-- Reducible term equality of type U is reducible type equality.
univEqEq : ∀ {l l′ Γ A B} ([U] : Γ ⊩⟨ l ⟩ U) ([A] : Γ ⊩⟨ l′ ⟩ A)
         → Γ ⊩⟨ l ⟩ A ≡ B ∷ U / [U]
         → Γ ⊩⟨ l′ ⟩ A ≡ B / [A]
univEqEq [U] [A] [A≡B] =
  let [A≡B]′ = irrelevanceEqTerm [U] (U-intr (U-elim [U])) [A≡B]
  in  univEqEq′ (U-elim [U]) [A] [A≡B]′

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module ExtInterface.Data.Product where

-- TODO: Write to Agda team about the lack of compilability of Sigma.
-- I assumed that the builtin flag would allow to compile Σ into (,)
-- but it doesn't. That's why this microfile exists

infixr 4 ⟨_,_⟩
infixr 2 _×_

data _×_ (A B : Set) : Set where
  ⟨_,_⟩ : A → B → A × B

{-# COMPILE GHC _×_ = data (,) ((,)) #-} -- Yeah, kinda abstract

proj₁ : ∀ {A B : Set} → A × B → A
proj₁ ⟨ x , y ⟩ = x

proj₂ : ∀ {A B : Set} → A × B → B
proj₂ ⟨ x , y ⟩ = y

map : ∀ {A B C D : Set}
    → (A → C) → (B → D) → A × B → C × D
map f g ⟨ x , y ⟩ = ⟨ f x , g y ⟩

map₁ : ∀ {A B C : Set}
     → (A → C) → A × B → C × B
map₁ f = map f (λ x → x)

map₂ : ∀ {A B D : Set}
     → (B → D) → A × B → A × D
map₂ g = map (λ x → x) g

max_stars_repo_name: RPI-WCL/safety-envelopes-sentinels

max_issues_repo_name: RPI-WCL/safety-envelopes-sentinels

max_forks_repo_name: RPI-WCL/safety-envelopes-sentinels


text:
module #16 where

{-
  Show that addition of natural numbers is commutative: ∏(i,j:N)(i + j = j + i).
-}

open import Data.Nat
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

l-commut₀ : (n : ℕ) → n + 0 ≡ n
l-commut₀ zero = refl
l-commut₀ (suc n) = cong suc (l-commut₀ n)

suc-in-the-middle-with-you : ∀ m n → m + suc n ≡ suc (m + n)
suc-in-the-middle-with-you zero n = refl
suc-in-the-middle-with-you (suc m) n = cong suc (suc-in-the-middle-with-you m n)

+-commutative : (m n : ℕ) → m + n ≡ n + m
+-commutative zero n = sym (l-commut₀ n)
+-commutative (suc m) n =
  begin
    (suc m) + n
      ≡⟨ refl ⟩
    suc (m + n)
      ≡⟨ cong suc (+-commutative m n) ⟩
    suc (n + m)
      ≡⟨ sym (suc-in-the-middle-with-you n m) ⟩
    n + (suc m)
  ∎

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-# OPTIONS --without-K #-}
module function.isomorphism where

open import function.isomorphism.core public
open import function.isomorphism.properties public
open import function.isomorphism.coherent public
open import function.isomorphism.lift public
open import function.isomorphism.utils public
open import function.isomorphism.univalence public
open import function.isomorphism.remove public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Action where

open import Light.Level using (Level ; Setω)
open import Light.Library.Data.Unit as Unit using (Unit)
open import Light.Library.Data.Natural as Natural using (ℕ)
open import Light.Variable.Sets
open import Light.Variable.Levels
open import Light.Package using (Package)

record Dependencies : Setω where
      field ⦃ unit‐package ⦄ : Package record { Unit }
      field ⦃ natural‐package ⦄ : Package record { Natural }

record Library (dependencies : Dependencies) : Setω where
      field
            main‐ℓ : Level
            Action : Set aℓ → Set aℓ
            pure : 𝕒 → Action 𝕒
            _>>=_ : Action 𝕒 → (𝕒 → Action 𝕓) → Action 𝕓
            _>>_ : Action 𝕒 → Action 𝕓 → Action 𝕓
            log : 𝕒 → Action Unit
            Main : Set main‐ℓ
            run : Action Unit → Main
            prompt : Action ℕ
            alert : 𝕒 → Action Unit
open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Issue858 where

module _ (A B : Set) (recompute : .B → .{{A}} → B) where

  _$_ : .(A → B) → .A → B
  f $ x with .{f} | .(f x) | .{{x}}
  ... | y = recompute y

module _ (A B : Set) (recompute : ..B → ..{{A}} → B) where

  _$'_ : ..(A → B) → ..A → B
  f $' x with ..{f} | ..(f x) | ..{{x}}
  ... | y = recompute y

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module AutoMisc where

-- prelude

postulate
  Level : Set
  lzero : Level
  lsuc  : (i : Level) → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}

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

trans : ∀ {a} {A : Set a} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : ∀ {a} {A : Set a} → {x y : A} → x ≡ y → y ≡ x
sym refl = refl

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

data _IsRelatedTo_ {a : Level} {Carrier : Set a} (x y : Carrier) : Set a where
  relTo : (x∼y : x ≡ y) → x IsRelatedTo y

begin_ : {a : Level} {Carrier : Set a} → {x y : Carrier} → x IsRelatedTo y → x ≡ y
begin relTo x∼y = x∼y

_∎ : {a : Level} {Carrier : Set a} → (x : Carrier) → x IsRelatedTo x
_∎ _ = relTo refl

_≡⟨_⟩_ : {a : Level} {Carrier : Set a} → (x : Carrier) {y z : Carrier} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_ ≡⟨ x∼y ⟩ relTo y∼z = relTo (trans x∼y y∼z)

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

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

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

data Π (A : Set) (F : A → Set) : Set where
  fun : ((a : A) → F a) → Π A F

data Σ (A : Set) (F : A → Set) : Set where
  ΣI : (a : A) → (F a) → Σ A F

data Fin : ℕ → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

data List (X : Set) : Set where
  []  : List X
  _∷_ : X → List X → List X

_++_ : {X : Set} → List X → List X → List X
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Vec (X : Set) : ℕ → Set where
  []  : Vec X zero
  _∷_ : ∀ {n} → X → Vec X n → Vec X (suc n)

module AdditionCommutative where

 lemma : ∀ n m → (n + suc m) ≡ suc (n + m)
 lemma n m = {!!}

 lemma' : ∀ n m → (n + suc m) ≡ suc (n + m)
 lemma' zero m = refl
 lemma' (suc n) m = cong suc (lemma' n m)

 addcommut : ∀ n m → (n + m) ≡ (m + n)
 addcommut n m = {!!}

module Drink where

 postulate RAA : (A : Set) → (¬ A → ⊥) → A

 drink : (A : Set) → (a : A)
            → (Drink : A → Set) → Σ A (λ x → (Drink x) → Π A Drink)
 drink A a Drink = {!!}

module VecMap where

 map : {X Y : Set} → {n : ℕ} → (X → Y) → Vec X n → Vec Y n
 map f xs = {!!}

module Disproving where

 p : {X : Set} → (xs ys : List X) → (xs ++ ys) ≡ (ys ++ xs)
 p = {!!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module UnSized.SelfRef where

open import Data.Unit.Base
open import Data.Product
open import Data.String.Base
open import Data.Sum using (_⊎_) renaming (inj₁ to inl; inj₂ to inr)

open import Size
--open import SimpleCell
open import SizedIO.Object
open import SizedIO.IOObject
open import SizedIO.ConsoleObject
-- open import PrimTypeHelpersSmall

open import UnSizedIO.Base hiding (main)
open import UnSizedIO.Console hiding (main)

open import NativeIO
--open import SimpleCell

-- Object Alpha

data AlphaMethod A : Set where
    print : AlphaMethod A
    set : A → AlphaMethod A
    m1 : AlphaMethod A
    m2 : AlphaMethod A

AlphaResponses : {A : Set} (c : AlphaMethod A) → Set
AlphaResponses _  = ⊤

alphaI : (A : Set) → Interface
Method   (alphaI A)   = AlphaMethod A
Result  (alphaI A) m = AlphaResponses m

alphaC : (i : Size) → Set
alphaC i = ConsoleObject i (alphaI String)

--
--  Self Referential: method 'm1' calls method 'm2'
--
{-
-- {-# NON_TERMINATING #-}
alphaO :  ∀{i} (s : String) → alphaC i
method (alphaO s) print =
  exec (putStrLn s) >>
  return (_ , alphaO s)

method (alphaO s) (set x) =
  return (_ , alphaO x)

-- force (method (alphaO s) m1) = exec (putStrLn s) λ _ →
--   method (alphaO s) m2  >>= λ{ (_ , c₀) →
--   return (_ , c₀) }
method (alphaO s) m1 =
  exec1 (putStrLn s) >>
  method (alphaO s) m2  >>= λ{ (_ , c₀) →
  return (_ , c₀) }
method (alphaO s) m2 =
  return (_ , alphaO (s ++ "->m2"))

program : String → IOConsole ∞ Unit
program arg =
  let c₀ = alphaO ("start̄\n====\n\n") in
  method c₀ m1  >>= λ{ (_ , c₁) →   --- ===> m1 called, but m2 prints out text
  method c₁ print  >>= λ{ (_ , c₂) →
  exec1 (putStrLn "\n\n====\nend")        }}

main : NativeIO Unit
main = translateIOConsole (program "")
-}


text:
{-# OPTIONS --without-K #-}
module HoTT.Identity.Coproduct where

open import HoTT.Base
open import HoTT.Equivalence

open variables
private variable x y : A + B

_=+_ : {A : 𝒰 i} {B : 𝒰 j} (x y : A + B) → 𝒰 (i ⊔ j)
_=+_ {j = j} (inl a₁) (inl a₂) = Lift {j} (a₁ == a₂)
_=+_ (inl _) (inr _) = 𝟎
_=+_ (inr _) (inl _) = 𝟎
_=+_ {i} (inr b₁) (inr b₂) = Lift {i} (b₁ == b₂)

=+-equiv : (x == y) ≃ x =+ y
=+-equiv = f , qinv→isequiv (g , η , ε)
  where
  f : x == y → x =+ y
  f {x = inl a} refl = lift refl
  f {x = inr a} refl = lift refl

  g : x =+ y → x == y
  g {x = inl _} {inl _} (lift refl) = refl
  g {x = inl _} {inr _} ()
  g {x = inr _} {inl _} ()
  g {x = inr _} {inr _} (lift refl) = refl

  η : {x y : A + B} → g {x = x} {y} ∘ f ~ id
  η {y = inl _} refl = refl
  η {y = inr _} refl = refl

  ε : f {x = x} {y} ∘ g ~ id
  ε {x = inl _} {inl _} (lift refl) = refl
  ε {x = inl _} {inr _} ()
  ε {x = inr _} {inl _} ()
  ε {x = inr _} {inr _} (lift refl) = refl

=+-elim : x == y → x =+ y
=+-elim = pr₁ =+-equiv

=+-intro : x =+ y → x == y
=+-intro = Iso.g (eqv→iso =+-equiv)

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.SequentialColimit.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat

private
  variable
    ℓ : Level

record Sequence (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    space : ℕ → Type ℓ
    map : {n : ℕ} → space n → space (1 + n)

open Sequence

data Lim→ (X : Sequence ℓ) : Type ℓ where
  inl : {n : ℕ} → X .space n → Lim→ X
  push : {n : ℕ}(x : X .space n) → inl x ≡ inl (X .map x)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Oscar.Prelude
open import Oscar.Class.IsPrecategory
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.Transitivity

module Oscar.Class.IsCategory where

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ) (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
  (ε : Reflexivity.type _∼_)
  (_↦_ : Transitivity.type _∼_)
  where
  record IsCategory : Ø 𝔬 ∙̂ 𝔯 ∙̂ ℓ where
    constructor ∁
    field
      ⦃ `IsPrecategory ⦄ : IsPrecategory _∼_ _∼̇_ _↦_
      ⦃ `𝓣ransleftidentity ⦄ : Transleftidentity.class _∼_ _∼̇_ ε _↦_
      ⦃ `𝓣ransrightidentity ⦄ : Transrightidentity.class _∼_ _∼̇_ ε _↦_


text:
module logic where

open import Level
open import Relation.Nullary
open import Relation.Binary hiding (_⇔_ )
open import Data.Empty

data One {n : Level } : Set n where
  OneObj : One

data Two : Set where
   i0 : Two
   i1 : Two

data Bool : Set where
   true : Bool
   false : Bool

record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   constructor ⟪_,_⟫
   field
      proj1 : A
      proj2 : B

data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
   case1 : A → A ∨ B
   case2 : B → A ∨ B

_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
_⇔_ A B =  ( A → B ) ∧ ( B → A )

contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )

double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
double-neg A notnot = notnot A

double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
double-neg2 notnot A = notnot ( double-neg A )

de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))

dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
dont-or {A} {B} (case2 b) ¬A = b

dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
dont-orb {A} {B} (case1 a) ¬B = a

infixr  130 _∧_
infixr  140 _∨_
infixr  150 _⇔_

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Relations
------------------------------------------------------------------------

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

module Relation.Nary where

------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------

open import Level using (Level; _⊔_; Lift)
open import Data.Unit.Base
open import Data.Bool.Base using (true; false)
open import Data.Empty
open import Data.Nat.Base using (zero; suc)
open import Data.Product as Prod using (_×_; _,_)
open import Data.Product.Nary.NonDependent
open import Data.Sum.Base using (_⊎_)
open import Function using (_$_; _∘′_)
open import Function.Nary.NonDependent
open import Relation.Nullary using (¬_; Dec; yes; no; _because_)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
import Relation.Unary as Unary
open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)

private
  variable
    r : Level
    R : Set r

------------------------------------------------------------------------
-- Generic type constructors

-- `Relation.Unary` provides users with a wealth of combinators to work
-- with indexed sets. We can generalise these to n-ary relations.

-- The crucial thing to notice here is that because we are explicitly
-- considering that the input function should be a `Set`-ended `Arrows`,
-- all the other parameters are inferrable. This allows us to make the
-- number arguments (`n`) implicit.
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Quantifiers

-- If we already know how to quantify over one variable, we can easily
-- describe how to quantify over `n` variables by induction over said `n`.

quantₙ : (∀ {i l} {I : Set i} → (I → Set l) → Set (i ⊔ l)) →
         ∀ n {ls} {as : Sets n ls} →
         Arrows n as (Set r) → Set (r ⊔ (⨆ n ls))
quantₙ Q zero     f = f
quantₙ Q (suc n)  f = Q (λ x → quantₙ Q n (f x))

infix 5 ∃⟨_⟩ Π[_] ∀[_]

-- existential quantifier

∃⟨_⟩ : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
∃⟨_⟩ = quantₙ Unary.Satisfiable _

-- explicit universal quantifiers

Π[_] : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
Π[_] = quantₙ Unary.Universal _

-- implicit universal quantifiers

∀[_] : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ (⨆ n ls))
∀[_] = quantₙ Unary.IUniversal _

-- ≟-mapₙ : ∀ n. (con : A₁ → ⋯ → Aₙ → R) →
--               Injectiveₙ n con →
--               ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--               Dec (a₁₁ ≡ a₁₂) → ⋯ → Dec (aₙ₁ ≡ aₙ₂) →
--               Dec (con a₁₁ ⋯ aₙ₁ ≡ con a₁₂ ⋯ aₙ₂)

≟-mapₙ : ∀ n {ls} {as : Sets n ls} (con : Arrows n as R) → Injectiveₙ n con →
         ∀ {l r} → Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l ≡ uncurryₙ n con r))
≟-mapₙ n con con-inj =
  curryₙ n λ a?s → let as? = Product-dec n a?s in
  Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as?

------------------------------------------------------------------------
-- Substitution

module _ {n r ls} {as : Sets n ls} (P : as ⇉ Set r) where

-- Substitutionₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--                      a₁₁ ≡ a₁₂ → ⋯ → aₙ₁ ≡ aₙ₂ →
--                      P a₁₁ ⋯ aₙ₁ → P a₁₂ ⋯ aₙ₂

  Substitutionₙ : Set (r ⊔ (⨆ n ls))
  Substitutionₙ = ∀ {l r} → Equalₙ n l r ⇉ (uncurryₙ n P l → uncurryₙ n P r)

  substₙ : Substitutionₙ
  substₙ = curryₙ n (subst (uncurryₙ n P) ∘′ fromEqualₙ n)

------------------------------------------------------------------------
-- Pointwise liftings of k-ary operators

-- Rather than having multiple ad-hoc lifting functions for various arities
-- we have a fully generic liftₙ functional which lifts a k-ary operator
-- to work with k n-ary functions whose respective codomains match the domains
-- of the operator.
-- The type of liftₙ is fairly unreadable. Here it is written with ellipsis:

-- liftₙ : ∀ k n. (B₁ → ⋯ → Bₖ → R) →
--                (A₁ → ⋯ → Aₙ → B₁) →
--                       ⋮
--                (A₁ → ⋯ → Aₙ → B₁) →
--                (A₁ → ⋯ → Aₙ → R)

liftₙ : ∀ k n {ls rs} {as : Sets n ls} {bs : Sets k rs} →
        Arrows k bs R → Arrows k (smap _ (Arrows n as) k bs) (Arrows n as R)
liftₙ k n op = curry⊤ₙ k λ fs →
               curry⊤ₙ n λ vs →
               uncurry⊤ₙ k op $
               palg _ _ k (λ f → uncurry⊤ₙ n f vs) fs where

  -- The bulk of the work happens in this auxiliary definition:
  palg : ∀ f (F : ∀ {l} → Set l → Set (f l)) n {ls} {as : Sets n ls} →
         (∀ {l} {r : Set l} → F r → r) → Product⊤ n (smap f F n as) → Product⊤ n as
  palg f F zero    alg ps       = _
  palg f F (suc n) alg (p , ps) = alg p , palg f F n alg ps

-- implication

infixr 6 _⇒_
_⇒_ : ∀ {n} {ls r s} {as : Sets n ls} →
      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
_⇒_ = liftₙ 2 _ (λ A B → A → B)

-- conjunction

infixr 7 _∩_
_∩_ : ∀ {n} {ls r s} {as : Sets n ls} →
      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
_∩_ = liftₙ 2 _ _×_

-- disjunction

infixr 8 _∪_
_∪_ : ∀ {n} {ls r s} {as : Sets n ls} →
      as ⇉ Set r → as ⇉ Set s → as ⇉ Set (r ⊔ s)
_∪_ = liftₙ 2 _ _⊎_

-- negation

∁ : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → as ⇉ Set r
∁ = liftₙ 1 _ ¬_

apply⊤ₙ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} →
          Π[ R ] → (vs : Product⊤ n as) → uncurry⊤ₙ n R vs
apply⊤ₙ {zero}  prf vs       = prf
apply⊤ₙ {suc n} prf (v , vs) = apply⊤ₙ (prf v) vs

applyₙ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} →
         Π[ R ] → (vs : Product n as) → uncurry⊤ₙ n R (toProduct⊤ n vs)
applyₙ {n} prf vs = apply⊤ₙ prf (toProduct⊤ n vs)

iapply⊤ₙ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} →
           ∀[ R ] → {vs : Product⊤ n as} → uncurry⊤ₙ n R vs
iapply⊤ₙ {zero}  prf = prf
iapply⊤ₙ {suc n} prf = iapply⊤ₙ {n} prf

iapplyₙ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} →
          ∀[ R ] → {vs : Product n as} → uncurry⊤ₙ n R (toProduct⊤ n vs)
iapplyₙ {n} prf = iapply⊤ₙ {n} prf

------------------------------------------------------------------------
-- Properties of N-ary relations

-- Decidability

Decidable : ∀ {n ls r} {as : Sets n ls} → as ⇉ Set r → Set (r ⊔ ⨆ n ls)
Decidable R = Π[ mapₙ _ Dec R ]

-- erasure

⌊_⌋ : ∀ {n ls r} {as : Sets n ls} {R : as ⇉ Set r} → Decidable R → as ⇉ Set r
⌊_⌋ {zero}  R? = Lift _ (Dec.True R?)
⌊_⌋ {suc n} R? a = ⌊ R? a ⌋

-- equivalence between R and its erasure

fromWitness : ∀ {n ls r} {as : Sets n ls} (R : as ⇉ Set r) (R? : Decidable R) →
              ∀[ ⌊ R? ⌋ ⇒ R ]
fromWitness {zero} R R? with R?
... | yes           r = λ _ → r
... | false because _ = λ ()
fromWitness {suc n} R R? = fromWitness (R _) (R? _)

toWitness : ∀ {n ls r} {as : Sets n ls} (R : as ⇉ Set r) (R? : Decidable R) →
              ∀[ R ⇒ ⌊ R? ⌋ ]
toWitness {zero} R R? with R?
... | true because _ = _
... | no          ¬r = ⊥-elim ∘′ ¬r
toWitness {suc n} R R? = toWitness (R _) (R? _)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Nullary.DecidableEq where

open import Cubical.Relation.Nullary.Properties
  using (Dec→Stable; Discrete→isSet) public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Util where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; I; i0; i1)
--open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract; isoToEquiv)

open import Agda.Primitive       using (Level)
open import Data.Fin             using (Fin; #_; toℕ; inject; fromℕ; fromℕ<; inject₁) renaming (zero to fz; suc to fsuc)
open import Data.Bool            using (Bool; true; false; if_then_else_)
open import Data.Integer         using (ℤ; +_; -[1+_]; _-_; ∣_∣; -_)
open import Data.List            using (List; concat; replicate; []; _∷_; _∷ʳ_; map; _++_; reverse)
open import Data.Maybe           using (Maybe; just; nothing)
open import Data.Nat             using (ℕ; zero; suc; _+_; _*_; _<ᵇ_; _≤ᵇ_; _≡ᵇ_; _<?_; _≟_; _∸_; _<_; s≤s; z≤n; _⊓_)
open import Data.Nat.DivMod      using (_mod_)
open import Data.Nat.Properties  using (≤-step; ≤-trans; ≤-refl)
open import Data.Product         using (_×_; _,_)
open import Data.Vec             using (Vec; _∷_; []; zip; last) renaming (concat to cat; replicate to rep; map to vmap; _∷ʳ_ to _v∷ʳ_)
open import Relation.Nullary     using (yes; no; ¬_)
open import Relation.Nullary.Decidable using (False)
open import Relation.Unary       using (Pred; Decidable)

infixr 9 _∘_

_∘_ : {ℓ : Level}{A : Type ℓ}{B : A → Type ℓ}{C : (a : A) → B a → Type ℓ}
  (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → C a (f a)
g ∘ f = λ x → g (f x)
{-# INLINE _∘_ #-}

repeat : {ℓ : Level} {A : Type ℓ} → (n : ℕ) → List A → List A
repeat n = concat ∘ replicate n

repeatV : {ℓ : Level} {A : Type ℓ} {k : ℕ} → (n : ℕ) → Vec A k → Vec A (n * k)
repeatV n = cat ∘ rep {n = n}

-- return index of first element that satisfies predicate or last element if none do
findIndex : {a ℓ : Level} {A : Type a} {n : ℕ} {P : Pred A ℓ} → Decidable P → Vec A (suc n) → Fin (suc n)
findIndex _ (x ∷ [])     = # 0
findIndex P (x ∷ y ∷ ys) with P x
... | yes _ = # 0
... | no  _ = fsuc (findIndex P (y ∷ ys))

-- Returns a list of all adjacent pairs in the original list.
pairs : {ℓ : Level} {A : Type ℓ} → List A → List (A × A)
pairs []           = []
pairs (x ∷ [])     = []
pairs (x ∷ y ∷ xs) = (x , y) ∷ pairs (y ∷ xs)

-- Returns a list of all pairs in the original list.
allPairs : {ℓ : Level} {A : Type ℓ} → List A → List (A × A)
allPairs [] = []
allPairs (x ∷ xs) = map (x ,_) xs ++ allPairs xs

-- Returns a singleton list of the pair of the first and last element if the list has at least 2 elements,
-- or the empty list otherwise.
firstLast : {ℓ : Level} {A : Type ℓ} → List A → List (A × A)
firstLast []       = []
firstLast (x ∷ xs) with reverse xs
... | []     = []
... | y ∷ ys = (x , y) ∷ []

-- Returns a list of all adjacent pairs in the original list, prepended by the pair of the first and last elements.
◯pairs : {ℓ : Level} {A : Type ℓ} → List A → List (A × A)
◯pairs xs = firstLast xs ++ pairs xs

-- Returns a list of the first element paired with all later elements, in order.
firstPairs : {ℓ : Level} {A : Type ℓ} → List A → List (A × A)
firstPairs []       = []
firstPairs (x ∷ xs) = map (x ,_) xs

-- Basic Boolean Filter and Elem
filter : {ℓ : Level} {A : Type ℓ} → (A → Bool) → List A → List A
filter f []       = []
filter f (x ∷ xs) = if f x then x ∷ filter f xs else filter f xs

infix 4 _∈_via_
_∈_via_ : {ℓ : Level} {A : Type ℓ} → A → List A → (A → A → Bool) → Bool
x ∈ []     via f = false
x ∈ y ∷ ys via f = if f x y then true else x ∈ ys via f

concatMaybe : {ℓ : Level} {A : Type ℓ} → List (Maybe A) → List A
concatMaybe []             = []
concatMaybe (nothing ∷ xs) = concatMaybe xs
concatMaybe (just x  ∷ xs) = x ∷ concatMaybe xs

listMin : {ℓ : Level} {A : Type ℓ} → (A → ℕ) → List A → Maybe A
listMin f [] = nothing
listMin f (x ∷ xs) with listMin f xs
... | nothing = just x
... | just y  = if f x <ᵇ f y then just x else just y

fins : (k : ℕ) → Vec (Fin k) k
fins zero    = []
fins (suc k) = fz ∷ vmap fsuc (fins k)

fins' : (n : ℕ) → (k : Fin n) → Vec (Fin n) (toℕ k)
fins' n k = vmap inject (fins (toℕ k))

finSuc : {n : ℕ} → Fin (suc n) → Fin (suc n)
finSuc {n} m with suc (toℕ m) <? suc n
... | yes x = fromℕ< x
... | no  _  = fz

_+N_ : {n : ℕ} → Fin (suc n) → ℕ → Fin (suc n)
a +N zero  = a
a +N suc b = finSuc a +N b

∣-∣helper : (n : ℕ) → ℕ → ℕ → ℕ
∣-∣helper n a b with a ≤ᵇ b
... | true  = (b ∸ a) ⊓ ((n + a) ∸ b)
... | false = (a ∸ b) ⊓ ((n + b) ∸ a)

⟨_⟩∣_-_∣ : (n : ℕ) → Fin n → Fin n → ℕ
⟨_⟩∣_-_∣ n a b = ∣-∣helper n (toℕ a) (toℕ b)

n∸k<n : (n k : ℕ) → (suc n) ∸ (suc k) < suc n
n∸k<n zero    zero    = s≤s z≤n
n∸k<n (suc n) zero    = s≤s (n∸k<n n zero)
n∸k<n zero    (suc k) = s≤s z≤n
n∸k<n (suc n) (suc k) = ≤-trans (n∸k<n n k) (≤-step ≤-refl)

opposite' : ∀ {n} → Fin n → Fin n
opposite' {suc n} fz       = fz
opposite' {suc n} (fsuc k) = fromℕ< (n∸k<n n (toℕ k))

-- opposite "i" = "n - i" (i.e. the additive inverse).
opposite : ∀ {n} → Fin n → Fin n
opposite {suc n} fz              = fz
opposite {suc n} (fsuc fz)       = fromℕ n
opposite {suc n} (fsuc (fsuc i)) = inject₁ (opposite (fsuc i))

_modℕ_ : (dividend : ℤ) (divisor : ℕ) {≢0 : False (divisor ≟ 0)} → Fin divisor
((+ n)    modℕ d) {d≠0} = (n mod d) {d≠0}
(-[1+ n ] modℕ d) {d≠0} = opposite ((suc n mod d) {d≠0})

zipWithIndex : {ℓ : Level} {A : Type ℓ} {k : ℕ} → Vec A k → Vec (Fin k × A) k
zipWithIndex {k = k} = zip (fins k)

iter : {ℓ : Level} {A : Type ℓ} → (A → A) → ℕ → A → List A
iter f zero    x = x ∷ []
iter f (suc n) x = x ∷ iter f n (f x)

rotateLeft : {ℓ : Level} {A : Type ℓ} → List A → List A
rotateLeft []       = []
rotateLeft (x ∷ xs) = xs ∷ʳ x

rotateRight : {ℓ : Level} {A : Type ℓ} → List A → List A
rotateRight = reverse ∘ rotateLeft ∘ reverse

vrotateLeft : {ℓ : Level} {A : Type ℓ} {k : ℕ} → Vec A k → Vec A k
vrotateLeft {k = zero}  []       = []
vrotateLeft {k = suc k} (x ∷ xs) = xs v∷ʳ x

vrotateRight : {ℓ : Level} {A : Type ℓ} {k : ℕ} → Vec A k → Vec A k
vrotateRight {k = zero}  []          = []
vrotateRight {k = suc k} xs@(_ ∷ ys) = last xs ∷ ys

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Bool
open import Cubical.HITs.Join
open import Cubical.HITs.Susp.Base

open Iso

Susp-iso-joinBool : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (join A Bool)
fun Susp-iso-joinBool north = inr true
fun Susp-iso-joinBool south = inr false
fun Susp-iso-joinBool (merid a i) = (sym (push a true) ∙ push a false) i
inv Susp-iso-joinBool (inr true ) = north
inv Susp-iso-joinBool (inr false) = south
inv Susp-iso-joinBool (inl _) = north
inv Susp-iso-joinBool (push a true  i) = north
inv Susp-iso-joinBool (push a false i) = merid a i
rightInv Susp-iso-joinBool (inr true ) = refl
rightInv Susp-iso-joinBool (inr false) = refl
rightInv Susp-iso-joinBool (inl a) = sym (push a true)
rightInv Susp-iso-joinBool (push a true  i) j = push a true (i ∨ ~ j)
rightInv Susp-iso-joinBool (push a false i) j
  = hcomp (λ k → λ { (i = i0) → push a true (~ j)
                   ; (i = i1) → push a false k
                   ; (j = i1) → push a false (i ∧ k) })
          (push a true (~ i ∧ ~ j))
leftInv Susp-iso-joinBool north = refl
leftInv Susp-iso-joinBool south = refl
leftInv (Susp-iso-joinBool {A = A}) (merid a i) j
  = hcomp (λ k → λ { (i = i0) → transp (λ _ → Susp A) (k ∨ j) north
                   ; (i = i1) → transp (λ _ → Susp A) (k ∨ j) (merid a k)
                   ; (j = i1) → merid a (i ∧ k) })
          (transp (λ _ → Susp A) j north)

Susp≃joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≃ join A Bool
Susp≃joinBool = isoToEquiv Susp-iso-joinBool

Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
Susp≡joinBool = isoToPath Susp-iso-joinBool

congSuspEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≃ B → Susp A ≃ Susp B
congSuspEquiv {ℓ} {A} {B} h = isoToEquiv isom
  where isom : Iso (Susp A) (Susp B)
        Iso.fun isom north = north
        Iso.fun isom south = south
        Iso.fun isom (merid a i) = merid (fst h a) i
        Iso.inv isom north = north
        Iso.inv isom south = south
        Iso.inv isom (merid a i) = merid (invEq h a) i
        Iso.rightInv isom north = refl
        Iso.rightInv isom south = refl
        Iso.rightInv isom (merid a i) j = merid (retEq h a j) i
        Iso.leftInv isom north = refl
        Iso.leftInv isom south = refl
        Iso.leftInv isom (merid a i) j = merid (secEq h a j) i

suspToPropRec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Type ℓ'} (a : A)
                 → ((x : Susp A) → isProp (B x))
                 → B north
                 → (x : Susp A) → B x
suspToPropRec a isProp Bnorth north = Bnorth
suspToPropRec {B = B} a isProp Bnorth south = subst B (merid a) Bnorth
suspToPropRec {B = B} a isProp Bnorth (merid a₁ i) =
  isOfHLevel→isOfHLevelDep 1 isProp Bnorth (subst B (merid a) Bnorth) (merid a₁) i

suspToPropRec2 : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Susp A → Type ℓ'} (a : A)
                 → ((x y : Susp A) → isProp (B x y))
                 → B north north
                 → (x y : Susp A) → B x y
suspToPropRec2 a isProp Bnorth =
  suspToPropRec a (λ x → isOfHLevelΠ 1 λ y → isProp x y)
                      (suspToPropRec a (λ x → isProp north x) Bnorth)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
{-# OPTIONS --without-K #-}
module container.m.from-nat.bisimulation where

open import level
open import sum
open import equality
open import function
open import container.core
open import container.m.coalgebra as MC hiding (IsMor ; _⇒_)
open import container.m.from-nat.coalgebra hiding (X)
open import hott.level

module Def {la lb lc} {C : Container la lb lc} (𝓧 : Coalg C (lb ⊔ lc)) where

  open Container C
  open Σ 𝓧 renaming (proj₁ to X ; proj₂ to γ)
  open MC C using (IsMor ; _⇒_)

  -- Σ-closure of an indexed binary relation
  Σ₂[_] : (∀ {i} → X i → X i → Set (lb ⊔ lc)) → I → Set _
  Σ₂[ _∼_ ] i = Σ (X i) λ x → Σ (X i) λ x′ → x ∼ x′

  -- projections
  module _ {_∼_ : ∀ {i} → X i → X i → Set _} (i : I) where

    Σ₂-proj₁ : Σ₂[ _∼_ ] i → X i
    Σ₂-proj₁ = proj₁

    Σ₂-proj₂ : Σ₂[ _∼_ ] i → X i
    Σ₂-proj₂ = proj₁ ∘' proj₂

    Σ₂-proj₃ : (r : Σ₂[ _∼_ ] i) → _∼_ (Σ₂-proj₁ r) (Σ₂-proj₂ r)
    Σ₂-proj₃ = proj₂ ∘' proj₂

  -- Definition 16 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  -- bisimulation definition
  record Bisim (_∼_ : ∀ {i} → X i → X i → Set _): Set(lb ⊔ lc ⊔ lsuc la) where
    field
      α : Σ₂[ _∼_ ] →ⁱ F Σ₂[ _∼_ ]
      π₁-Mor : IsMor (_ , α) 𝓧 Σ₂-proj₁
      π₂-Mor : IsMor (_ , α) 𝓧 Σ₂-proj₂

    𝓑 : Coalg C _
    𝓑 = _ , α

    π₁ : 𝓑 ⇒ 𝓧
    π₁ = _ , π₁-Mor

    π₂ : 𝓑 ⇒ 𝓧
    π₂ = _ , π₂-Mor

  -- Lemma 17 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
  Δ : Bisim (λ {i} → _≡_)
  Δ = record { α = α ; π₁-Mor = π₁-Mor ; π₂-Mor = π₂-Mor }
    where α : Σ₂[ _≡_ ] →ⁱ F Σ₂[ _≡_ ]
          α i (x , ._ , refl) = proj₁ (γ _ x)
                                  , λ b → (proj₂ (γ _ x) b) , (_ , refl)
          π₁-Mor : IsMor (_ , α) 𝓧 _
          π₁-Mor = funextⁱ helper
            where helper : (i : I) → (p : Σ₂[ _≡_ ] i) → _
                  helper i (m , ._ , refl) = refl
          π₂-Mor : IsMor (_ , α) 𝓧 _
          π₂-Mor = funextⁱ helper
            where helper : (i : I) → (p : Σ₂[ _≡_ ] i) → _
                  helper i (m , ._ , refl) = refl

--------------------------------------------------------------------------------
-- coinduction proof principle

module _ {la lb lc} {C : Container la lb lc} where

  open Container C
  open MC C using (IsMor ; _⇒_)

  private
    𝓜 : Coalg C (lb ⊔ lc)
    𝓜 = 𝓛 C
    unfold : ∀ (𝓧 : Coalg C (lb ⊔ lc)) → 𝓧 ⇒ 𝓜
    unfold 𝓧 = proj₁ $ lim-terminal C 𝓧
    unfold-universal = λ {ℓ} (𝓧 : Coalg C ℓ) → proj₂ (lim-terminal C 𝓧)

  open Σ 𝓜 renaming (proj₁ to M ; proj₂ to out) ; open Def 𝓜

  module _ {_∼_ : ∀ {i} → M i → M i → Set (lb ⊔ lc)} (B : Bisim _∼_) where

    -- Theorem 18 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
    -- coinduction proof principle
    cpp : ∀ {i} {m m′ : M i} → m ∼ m′ → m ≡ m′
    cpp {i} p = funext-invⁱ (proj₁ $ apΣ π₁=π₂) i (_ , _ , p)
      where open Bisim B
            abstract
              π₁=π₂ : π₁ ≡ π₂
              π₁=π₂ = (sym $ unfold-universal 𝓑 π₁) · unfold-universal 𝓑 π₂

    -- In particular, provided that the bisimulation _∼_ is reflexive, we have:
    module _ (∼-refl : ∀ {i} {m : M i} → m ∼ m) where

      cpp′ : ∀ {i} {m m′ : M i} → m ∼ m′ → m ≡ m′
      cpp′ {i} p = cpp p · sym (cpp ∼-refl)

      cpp′-inv : ∀ {i} {m m′ : M i} → m ≡ m′ → m ∼ m′
      cpp′-inv refl = ∼-refl

      cpp′-id : ∀ {i} {m : M i} → cpp′ ∼-refl ≡ refl {x = m}
      cpp′-id = left-inverse $ cpp ∼-refl

      cpp′-retraction : ∀ {i} {m m′ : M i} (p : m ≡ m′) → cpp′ (cpp′-inv p) ≡ p
      cpp′-retraction refl = left-inverse $ cpp ∼-refl


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

module M-types.Base.Core where
    open import Agda.Primitive public using (Level) renaming
        (
            lzero to ℓ-zero ;
            lsuc to ℓ-suc ;
            _⊔_ to ℓ-max
        )

    variable
        ℓ ℓ₀ ℓ₁ ℓ₂ : Level

    Ty : (ℓ : Level) → Set (ℓ-suc ℓ)
    Ty ℓ = Set ℓ

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module _ where

-- Ulf's example of why removing abstract may
-- cause a proof that used to work to now fail

-- Agda mailing list, 16 May 2018

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

module WithAbstract where

  abstract
    f : Nat → Nat
    f zero    = zero
    f (suc n) = suc (f n)

    lem : ∀ n → f n ≡ n
    lem zero    = refl
    lem (suc n) rewrite lem n = refl

  thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm m n rewrite lem (suc m) = refl
  -- Works.

  thm′ : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm′ m n = {!!}

{- Hole 0
Goal: f (suc m) + n ≡ suc (m + n)
————————————————————————————————————————————————————————————
n : Nat
m : Nat
-}

module WithoutAbstract where

  f : Nat → Nat
  f zero    = zero
  f (suc n) = suc (f n)

  lem : ∀ n → f n ≡ n
  lem zero    = refl
  lem (suc n) rewrite lem n = refl

  thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm m n rewrite lem (suc m) = {! refl!}
  -- Fails since rewrite doesn't trigger:
  --   lem (suc m)  : suc (f m)     ≡ suc m
  --   goal         : suc (f m + n) ≡ suc (m + n)

  -- NB: The problem is with the expansion of `f`,
  -- not with the expansion of the lemma

  thm′ : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm′ m n = {!!}

{- Holes 1 and 2
Goal: suc (f m + n) ≡ suc (m + n)
————————————————————————————————————————————————————————————
n : Nat
m : Nat
-}


text:
postulate
  A : Set

module _ where

  {-# POLARITY A #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module UniDB.Subst where

open import UniDB.Subst.Core public
open import UniDB.Subst.Pair public
open import UniDB.Subst.Inst public

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
{-# OPTIONS --without-K --rewriting --allow-unsolved-metas #-}

open import HoTT renaming (pt to pt⊙)
open import homotopy.DisjointlyPointedSet
open import lib.types.Nat
open import lib.types.Vec

module simplicial.Base where

-- HELPERS
combinations : ℕ → List ℕ -> List (List ℕ)
combinations 0 _ = nil :: nil
combinations _ nil = nil
combinations (S n) (x :: xs) = (map (λ ys → x :: ys) (combinations (n) xs)) ++ (combinations (S n) xs)

standardSimplex : ℕ → List ℕ
standardSimplex O = nil
standardSimplex (S x) = (S x) :: (standardSimplex x)

-- UGLY HELPER FUNCTIONS -- TO BE REPLACED WITH STANDARD FUNCTIONS LATER ON
bfilter : {A : Type₀} → ((a : A) → Bool) → List A → List A
bfilter f nil = nil
bfilter f (a :: l) with f a
... | inl _ = a :: (bfilter f l)
... | inr _ = bfilter f l

ℕin : ℕ → List ℕ → Bool
ℕin x nil = inr unit
ℕin x (y :: ys) with ℕ-has-dec-eq x y
... | inl x₁ = inl unit
... | inr x₁ = inr unit

_lsubset_ : List ℕ → List ℕ → Bool
nil lsubset ys = inl unit
(x :: xs) lsubset ys with ℕin x ys
... | inl _ = xs lsubset ys
... | inr _ = inr unit

-- TYPES FOR SIMPLICES
-- 'Simplices' saves a collection of simplices, grouped by their dimension.
-- Note that we do not specify the dimensions of individual simplices, since
-- otherwise we could not simply save all simplices in a single vector
Simplex = List ℕ
Simplices : ℕ → Type₀
Simplices dim = (Vec (List Simplex) dim)

is-closed : {dim : ℕ} → (Simplices dim) → Type₀

record SC (dim : ℕ) : Type₀ where
  constructor complex
  field
    simplices : Simplices dim
    closed : is-closed simplices

simplices : {dim : ℕ} → SC dim → Simplices dim
simplices (complex simplices _) = simplices

faces : Simplex → List Simplex
faces s = concat (map (λ l → combinations l s) (standardSimplex (ℕ-pred (length s))))

-- removes grouping of simplices by dimension and puts all simplices in single list
compress : {dim : ℕ} → Simplices dim → List Simplex
compress {dim} []         = nil
compress {dim} (xs ∷ xss) = xs ++ compress xss

bodies : {dim : ℕ} → (SC dim) → Simplex → List Simplex
bodies (complex ss _) s = bfilter (λ o → (s lsubset o)) (compress ss)

-- inverse of compress function
unfold : {dim : ℕ}  → List Simplex → Simplices dim
unfold {dim} ss = unfold' {dim} ss (emptyss dim)
  where
  emptyss : (dim : ℕ) → Simplices dim
  emptyss 0 = []
  emptyss (S n) = nil ∷ (emptyss n)
  unfold' : {dim : ℕ}  → List Simplex → Simplices dim → Simplices dim
  unfold' {dim} nil sc = sc
  unfold' {dim} (x :: ss) sc = insert (faces x) sc
      where
      insert : {dim : ℕ} → List Simplex → Simplices dim → Simplices dim
      insert nil sc = sc
      insert (s :: ss) sc = insertS s sc
          where
          insertS : {dim : ℕ} → Simplex → Simplices dim → Simplices dim
          insertS s sc = updateAt ((length s) , {!!}) (λ l → s :: l) sc

is-closed {dim} ss = All (λ s → All (λ f → f ∈ ssc) (faces s)) ssc
  where ssc = compress ss

-- takes facet description of SC and generates their face closure
SCgenerator : (dim : ℕ) → List Simplex → SC dim
SC.simplices (SCgenerator dim ss) = unfold $ concat(concat (map(λ simplex → map (λ l → combinations l simplex) (standardSimplex (length simplex))) ss))
SC.closed (SCgenerator dim ss) = {!!}

-- EXAMPLES

sc-unit : SC 2
SC.simplices sc-unit = ((1 :: nil) :: (2 :: nil) :: nil) ∷ ((1 :: 2 :: nil) :: nil) ∷ []
SC.closed sc-unit = nil :: (nil :: (((here idp) :: ((there (here idp)) :: nil)) :: nil))

sc-circle : SC 2
SC.simplices sc-circle =
  ((1 :: nil) :: (2 :: nil) :: (3 :: nil) :: nil) ∷
  ((1 :: 2 :: nil) :: (1 :: 3 :: nil) :: (2 :: 3 :: nil) :: nil) ∷ []
SC.closed sc-circle = nil :: (nil :: (nil :: (((here idp) :: ((there (here idp)) :: nil)) :: (((here idp) :: ((there (there (here idp))) :: nil)) :: ((there (here idp) :: (there (there (here idp)) :: nil)) :: nil)))))

-- sc-circle-equiv-cw-circle : CWSphere 1 ≃ CWSphere 1
-- sc-circle-equiv-cw-circle = {!!}

sc-sphere : SC 3
sc-sphere = SCgenerator 3 ((1 :: 2 :: 3 :: nil) :: (1 :: 3 :: 4 :: nil) :: (2 :: 3 :: 4 :: nil) :: (1 :: 3 :: 4 :: nil) :: nil)

sc-unit-gen : SC 2
sc-unit-gen = SCgenerator 2 ((1 :: 2 :: nil) :: nil)

-- sc-unit≃sc-unit-gen : sc-unit ≃ sc-unit-gen
-- sc-unit≃sc-unit-gen = ?

max_stars_repo_name: maxdore/hott-morse

max_issues_repo_name: maxdore/hott-morse

max_forks_repo_name: maxdore/hott-morse


text:
-- If we try to naively extend the Kripke structure used for NbE of STLC,
-- we find that it is sound, but not complete.
--
-- The definition of semantic objects, which represent terms in normal form,
-- is not big enough to represent neutral terms of the coproduct types.
-- The problem is visible in the definition of `reflect`.

module STLC2.Kovacs.Normalisation.SoundNotComplete where

open import STLC2.Kovacs.NormalForm public

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

-- (Tyᴺ)
infix 3 _⊩_
_⊩_ : 𝒞 → 𝒯 → Set

Γ ⊩ ⎵      = Γ ⊢ⁿᶠ ⎵

Γ ⊩ A ⇒ B = ∀ {Γ′} → (η : Γ′ ⊇ Γ) (a : Γ′ ⊩ A)
                     → Γ′ ⊩ B

Γ ⊩ A ⩕ B  = Γ ⊩ A × Γ ⊩ B

Γ ⊩ ⫪     = ⊤

Γ ⊩ ⫫     = ⊥

Γ ⊩ A ⩖ B  = Γ ⊩ A ⊎ Γ ⊩ B

-- (Conᴺ ; ∙ ; _,_)
infix 3 _⊩⋆_
data _⊩⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ⊩⋆ ∅

    _,_ : ∀ {Γ Ξ A} → (ρ : Γ ⊩⋆ Ξ) (a : Γ ⊩ A)
                    → Γ ⊩⋆ Ξ , A

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

-- (Tyᴺₑ)
acc : ∀ {A Γ Γ′} → Γ′ ⊇ Γ → Γ ⊩ A → Γ′ ⊩ A
acc {⎵}      η M = renⁿᶠ η M
acc {A ⇒ B} η f = λ η′ a → f (η ○ η′) a
acc {A ⩕ B}  η s = acc η (proj₁ s) , acc η (proj₂ s)
acc {⫪}     η s = tt
acc {⫫}     η s = elim⊥ s
acc {A ⩖ B}  η s = elim⊎ s (λ a → inj₁ (acc η a))
                           (λ b → inj₂ (acc η b))

-- (Conᴺₑ)
-- NOTE: _⬖_ = acc⋆
_⬖_ : ∀ {Γ Γ′ Ξ} → Γ ⊩⋆ Ξ → Γ′ ⊇ Γ → Γ′ ⊩⋆ Ξ
∅       ⬖ η = ∅
(ρ , a) ⬖ η = ρ ⬖ η , acc η a

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

-- (∈ᴺ)
getᵥ : ∀ {Γ Ξ A} → Γ ⊩⋆ Ξ → Ξ ∋ A → Γ ⊩ A
getᵥ (ρ , a) zero    = a
getᵥ (ρ , a) (suc i) = getᵥ ρ i

-- (Tmᴺ)
eval : ∀ {Γ Ξ A} → Γ ⊩⋆ Ξ → Ξ ⊢ A → Γ ⊩ A
eval ρ (𝓋 i)         = getᵥ ρ i
eval ρ (ƛ M)         = λ η a → eval (ρ ⬖ η , a) M
eval ρ (M ∙ N)       = eval ρ M idₑ (eval ρ N)
eval ρ (M , N)       = eval ρ M , eval ρ N
eval ρ (π₁ M)        = proj₁ (eval ρ M)
eval ρ (π₂ M)        = proj₂ (eval ρ M)
eval ρ τ             = tt
eval ρ (φ M)         = elim⊥ (eval ρ M)
eval ρ (ι₁ M)        = inj₁ (eval ρ M)
eval ρ (ι₂ M)        = inj₂ (eval ρ M)
eval ρ (M ⁇ N₁ ∥ N₂) = elim⊎ (eval ρ M) (λ M₁ → eval (ρ , M₁) N₁)
                                        (λ M₂ → eval (ρ , M₂) N₂)

-- mutual
--   -- (qᴺ)
--   reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ⁿᶠ A
--   reify {⎵}      M = M
--   reify {A ⇒ B} f = ƛ (reify (f (wkₑ idₑ) (reflect 0)))
--   reify {A ⩕ B}  s = reify (proj₁ s) , reify (proj₂ s)
--   reify {⫪}     s = τ
--   reify {⫫}     s = elim⊥ s
--   reify {A ⩖ B}  s = elim⊎ s (λ a → ι₁ (reify a))
--                              (λ b → ι₂ (reify b))

--   -- (uᴺ)
--   reflect : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊩ A
--   reflect {⎵}      M = ne M
--   reflect {A ⇒ B} M = λ η a → reflect (renⁿᵉ η M ∙ reify a)
--   reflect {A ⩕ B}  M = reflect (π₁ M) , reflect (π₂ M)
--   reflect {⫪}     M = tt
--   reflect {⫫}     M = {!!}
--   reflect {A ⩖ B}  M = {!!}

-- -- (uᶜᴺ)
-- idᵥ : ∀ {Γ} → Γ ⊩⋆ Γ
-- idᵥ {∅}     = ∅
-- idᵥ {Γ , A} = idᵥ ⬖ wkₑ idₑ , reflect 0

-- -- (nf)
-- nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ⁿᶠ A
-- nf M = reify (eval idᵥ M)

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


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

module Base where

{-
With the HoTT-Agda library, the following import can be used instead:

open import HoTT using
  (Type; lmax; lsucc;
   _==_; idp; !;
   ap; apd;
   Square; ids; vid-square; hid-square; SquareOver; ↓-ap-in; apd-square;
   app=; λ=; app=-β;
   transport;
   ℕ; O; S; ℕ-reader;
   _×_; _,_; fst; snd;
   _∘_; ap-∘; ap-!;
   PathOver; ↓-cst-in; apd=cst-in; ap-idf; ap-cst; square-symmetry; uncurry; ap-square;
   Cube; idc; ap-cube;
   is-contr) public
-}

open import Agda.Primitive public using (lzero)
  renaming (Level to ULevel; lsuc to lsucc; _⊔_ to lmax)

Type : (i : ULevel) → Set (lsucc i)
Type i = Set i

Type₀ : Set (lsucc lzero)
Type₀ = Type lzero

infix 30 _==_
data _==_ {i} {A : Type i} (a : A) : A → Type i where
  idp : a == a

PathOver : ∀ {i j} {A : Type i} (B : A → Type j)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Type j
PathOver B idp u v = (u == v)

infix 30 PathOver
syntax PathOver B p u v =
  u == v [ B ↓ p ]

ap : ∀ {i j} {A : Type i} {B : Type j} (f : A → B) {x y : A}
  → (x == y → f x == f y)
ap f idp = idp

apd : ∀ {i j} {A : Type i} {B : A → Type j} (f : (a : A) → B a) {x y : A}
  → (p : x == y) → f x == f y [ B ↓ p ]
apd f idp = idp

transport : ∀ {i j} {A : Type i} (B : A → Type j) {x y : A} (p : x == y)
  → (B x → B y)
transport B idp u = u

infixr 60 _,_

record Σ {i j} (A : Type i) (B : A → Type j) : Type (lmax i j) where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

_×_ : ∀ {i j} (A : Type i) (B : Type j) → Type (lmax i j)
A × B = Σ A (λ _ → B)

data ℕ : Type lzero where
  O : ℕ
  S : (n : ℕ) → ℕ

Nat = ℕ

{-# BUILTIN NATURAL ℕ #-}

infixr 80 _∘_

_∘_ : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (a : A) → (B a → Type k)}
  → (g : {a : A} → (x : B a) → (C a x)) → (f : (x : A) → B x) → (x : A) → C x (f x)
g ∘ f = λ x → g (f x)

uncurry : ∀ {i j k} {A : Type i} {B : A → Type j} {C : (x : A) → B x → Type k}
  → (∀ x y → C x y) → (∀ s → C (fst s) (snd s))
uncurry f (x , y) = f x y

record FromNat {i} (A : Type i) : Type (lsucc i) where
  field
    in-range : ℕ → Type i
    read : ∀ n → ⦃ _ : in-range n ⦄ → A

open FromNat ⦃...⦄ public using () renaming (read to from-nat)

{-# BUILTIN FROMNAT from-nat #-}

record ⊤ : Type lzero where
  instance constructor unit

Unit = ⊤

instance
  ℕ-reader : FromNat ℕ
  FromNat.in-range ℕ-reader _ = ⊤
  FromNat.read ℕ-reader n = n

! : ∀ {i} {A : Type i} {x y : A} → x == y → y == x
! idp = idp

data Square {i} {A : Type i} {a₀₀ : A} : {a₀₁ a₁₀ a₁₁ : A}
  → a₀₀ == a₀₁ → a₀₀ == a₁₀ → a₀₁ == a₁₁ → a₁₀ == a₁₁ → Type i
  where
  ids : Square idp idp idp idp

hid-square : ∀ {i} {A : Type i} {a₀₀ a₀₁ : A} {p : a₀₀ == a₀₁}
  → Square p idp idp p
hid-square {p = idp} = ids

vid-square : ∀ {i} {A : Type i} {a₀₀ a₁₀ : A} {p : a₀₀ == a₁₀}
  → Square idp p p idp
vid-square {p = idp} = ids

ap-square : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square (ap f p₀₋) (ap f p₋₀) (ap f p₋₁) (ap f p₁₋)
ap-square f ids = ids

SquareOver : ∀ {i j} {A : Type i} (B : A → Type j) {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  {b₀₀ : B a₀₀} {b₀₁ : B a₀₁} {b₁₀ : B a₁₀} {b₁₁ : B a₁₁}
  (q₀₋ : b₀₀ == b₀₁ [ B ↓ p₀₋ ]) (q₋₀ : b₀₀ == b₁₀ [ B ↓ p₋₀ ])
  (q₋₁ : b₀₁ == b₁₁ [ B ↓ p₋₁ ]) (q₁₋ : b₁₀ == b₁₁ [ B ↓ p₁₋ ])
  → Type j
SquareOver B ids = Square

apd-square : ∀ {i j} {A : Type i} {B : A → Type j} (f : (x : A) → B x)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → SquareOver B sq (apd f p₀₋) (apd f p₋₀) (apd f p₋₁) (apd f p₁₋)
apd-square f ids = ids

square-symmetry : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₋₀ p₀₋ p₁₋ p₋₁
square-symmetry ids = ids

module _ {i j k} {A : Type i} {B : Type j} (C : B → Type k) (f : A → B) where

  ↓-ap-in : {x y : A} {p : x == y} {u : C (f x)} {v : C (f y)}
    → u == v [ C ∘ f ↓ p ]
    → u == v [ C ↓ ap f p ]
  ↓-ap-in {p = idp} idp = idp

-- We postulate function extensionality

module _ {i j} {A : Type i} {P : A → Type j} {f g : (x : A) → P x} where

  app= : (p : f == g) (x : A) → f x == g x
  app= p x = ap (λ u → u x) p

  postulate
    λ= : (h : (x : A) → f x == g x) → f == g
    app=-β : (h : (x : A) → f x == g x) (x : A) → app= (λ= h) x == h x

ap-∘ : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
  {x y : A} (p : x == y) → ap (g ∘ f) p == ap g (ap f p)
ap-∘ f g idp = idp

ap-cst : ∀ {i j} {A : Type i} {B : Type j} (b : B) {x y : A} (p : x == y)
  → ap (λ _ → b) p == idp
ap-cst b idp = idp

ap-idf : ∀ {i} {A : Type i} {u v : A} (p : u == v) → ap (λ x → x) p == p
ap-idf idp = idp

module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  ap-! : {x y : A} (p : x == y)
    → ap f (! p) == ! (ap f p)
  ap-! idp = idp

module _ {i j} {A : Type i} {B : Type j} where

  ↓-cst-in : {x y : A} {p : x == y} {u v : B}
    → u == v
    → u == v [ (λ _ → B) ↓ p ]
  ↓-cst-in {p = idp} q = q

{- Used for defining the recursor from the eliminator for 1-HIT -}
apd=cst-in : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a a' : A} {p : a == a'} {q : f a == f a'}
  → apd f p == ↓-cst-in q → ap f p == q
apd=cst-in {p = idp} x = x

data Cube {i} {A : Type i} {a₀₀₀ : A} :
  {a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  (sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀) -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  (sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁) -- back
  (sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁) -- top
  (sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁) -- bottom
  (sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) -- front
  → Type i

  where
  idc : Cube ids ids ids ids ids ids

ap-cube : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube (ap-square f sq₋₋₀) (ap-square f sq₋₋₁) (ap-square f sq₀₋₋)
         (ap-square f sq₋₀₋) (ap-square f sq₋₁₋) (ap-square f sq₁₋₋)
ap-cube f idc = idc

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
module Type.Category.IntensionalFunctionsCategory.HomFunctor where

import      Functional as Fn
open import Function.Proofs
open import Logic.Predicate
import      Lvl
open import Relator.Equals
open import Relator.Equals.Proofs
import      Relator.Equals.Proofs.Equiv
open import Structure.Category
open import Structure.Category.Dual
open import Structure.Category.Functor
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity
open import Type.Category.IntensionalFunctionsCategory
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ : Lvl.Level

module _
  {Obj : Type{ℓₒ}}
  {_⟶_ : Obj → Obj → Type{ℓₘ}}
  (C : Category(_⟶_))
  where

  open Category(C)

  covariantHomFunctor : Obj → (intro(C) →ᶠᵘⁿᶜᵗᵒʳ typeIntensionalFnCategoryObject{ℓₘ})
  ∃.witness (covariantHomFunctor x) y = (x ⟶ y)
  Functor.map (∃.proof (covariantHomFunctor _)) = (_∘_)
  Function.congruence (Functor.map-function (∃.proof (covariantHomFunctor _))) = congruence₁(_∘_)
  Functor.op-preserving (∃.proof (covariantHomFunctor x)) {f = f} {g = g} =
    (h ↦ (f ∘ g) ∘ h)  🝖[ _≡_ ]-[ {!!} ] -- TODO: Requires func. ext?
    (h ↦ f ∘ (g ∘ h))  🝖[ _≡_ ]-[]
    (f ∘_) Fn.∘ (g ∘_) 🝖-end
  Functor.id-preserving (∃.proof (covariantHomFunctor x)) = {!!}
{-
  contravariantHomFunctor : Object → (dual(C) →ᶠᵘⁿᶜᵗᵒʳ typeIntensionalFnCategoryObject{ℓₘ})
  ∃.witness (contravariantHomFunctor x) y = (y ⟶ x)
  Functor.map (∃.proof (contravariantHomFunctor _)) = Fn.swap(_∘_)
  Function.congruence (Functor.map-function (∃.proof (contravariantHomFunctor x))) x₁ = {!!}
  _⊜_.proof (Functor.op-preserving (∃.proof (contravariantHomFunctor x))) {x₁} = {!!}
  _⊜_.proof (Functor.id-preserving (∃.proof (contravariantHomFunctor x))) {x₁} = {!!}
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda