text:
{-# OPTIONS --safe #-}
module STLC.Denotational where

open import STLC.Syntax
open import STLC.Typing
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Unit using (⊤; tt)

private
  variable
    n : ℕ
    Γ : Ctx n
    A : Type

⟦_⟧ : Type → Set
⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧
⟦ unit ⟧ = ⊤
⟦ A ×' B ⟧ = ⟦ A ⟧ × ⟦ B ⟧

data Env : Ctx n → Set where
  ∅ : Env ●
  ⟨_,_⟩ : Env Γ → ⟦ A ⟧ → Env (Γ ,- A)

lookup : Env {n} Γ → (v : Fin n) → ⟦ find Γ v ⟧
lookup ⟨ ρ , term ⟩ fzero = term
lookup ⟨ ρ , term ⟩ (fsuc n) = lookup ρ n

⟦_⟧⟨_⟩ : ∀ {term : Term n} {type : Type} → (Γ ⊢ term ∈ type) → Env Γ → ⟦ type ⟧
⟦ ty-abs body ⟧⟨ ρ ⟩ = λ x → ⟦ body ⟧⟨ ⟨ ρ , x ⟩ ⟩
⟦ ty-app f x ⟧⟨ ρ ⟩ = ⟦ f ⟧⟨ ρ ⟩ ⟦ x ⟧⟨ ρ ⟩
⟦ ty-var v ⟧⟨ ρ ⟩ = lookup ρ v
⟦ ty-⋆ ⟧⟨ _ ⟩ = tt
⟦ ty-pair l r ⟧⟨ ρ ⟩ = ⟦ l ⟧⟨ ρ ⟩ , ⟦ r ⟧⟨ ρ ⟩
⟦ ty-projₗ p ⟧⟨ ρ ⟩ = proj₁ ⟦ p ⟧⟨ ρ ⟩
⟦ ty-projᵣ p ⟧⟨ ρ ⟩ = proj₂ ⟦ p ⟧⟨ ρ ⟩

max_stars_repo_name: TypesLogicsCats/STLC

max_issues_repo_name: TrulyNonstrict/STLC

max_forks_repo_name: TrulyNonstrict/STLC


text:
module Types.Tail1 where

open import Data.Fin
open import Data.Nat
open import Function using (_∘_)

open import Types.Direction
import Types.IND1 as IND

private
  variable
    n : ℕ

-- session types restricted to tail recursion
-- can be recognized by type of TChan constructor

data Type : Set
data SType (n : ℕ) : Set
data GType (n : ℕ) : Set

data Type where
  TUnit TInt : Type
  TPair : (t₁ t₂ : Type) → Type
  TChan : (s : IND.SType 0) → Type

data SType n where
  gdd : (g : GType n) → SType n
  rec : (g : GType (suc n)) → SType n
  var : (x : Fin n) → SType n

data GType n where
  transmit : (d : Dir) (t : Type) (s : SType n) → GType n
  choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
  end : GType n

-- naive definition of duality for tail recursive session types
-- message types are ignored as they are closed

dualS : SType n → SType n
dualG : GType n → GType n

dualS (gdd g) = gdd (dualG g)
dualS (rec g) = rec (dualG g)
dualS (var x) = var x

dualG (transmit d t s) = transmit (dual-dir d) t (dualS s)
dualG (choice d m alt) = choice (dual-dir d) m (dualS ∘ alt)
dualG end = end

ext: agda

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
-- A Beth model of normal forms

open import Library hiding (_∈_; All)

module NfModel (Base : Set) where

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

-- Beth model

-- A cover for Γ is the skeleton of a case tree that can be formed in Γ.
-- It contains the (neutral) scrutinees we case over and the markers (hole)
-- for the leaves that have to be filled by the branches of the case statement.

data Cover (Γ : Cxt) : Set where
  hole   : Cover Γ
  falseC : (t : Ne Γ False) → Cover Γ
  orC    : ∀{A B} (t : Ne Γ (A ∨ B)) (c : Cover (Γ ∙ A)) (d : Cover (Γ ∙ B)) → Cover Γ

-- Choice of names.
-- hole  : has the same role as the hole-evaluation context (identity).
-- falseC: basically falseE.
-- orC   : basically orE.

-- Given c : Cover Γ, a path p : Δ ∈ c leads us from the root to one of the leaves (hole)
-- of the case tree.  Δ is the context at the leaf.

data _∈_ Δ : ({Γ} : Cxt) (c : Cover Γ) → Set where
  here  : Δ ∈ hole {Δ}
  left  : ∀{Γ A B c d} {t : Ne Γ (A ∨ B)} (e : Δ ∈ c) → Δ ∈ orC t c d
  right : ∀{Γ A B c d} {t : Ne Γ (A ∨ B)} (e : Δ ∈ d) → Δ ∈ orC t c d

-- Given a case tree c : Cover Γ and a context-indexed set P,
-- f : All c P  is an assignment of things in  P Δ  to holes
-- of type Δ reached by pathes e : Δ ∈ c.

All : ∀{Γ} (c : Cover Γ) (P : (Δ : Cxt) → Set) → Set
All c P = ∀{Δ} (e : Δ ∈ c) → P Δ

-- We can also use All c P with a property P on context,
-- to express that all holes of c satify P.

-- We might want to depend on the path e : Δ ∈ c also:

All' : ∀{Γ} (c : Cover Γ) (P : ∀ {Δ} (e : Δ ∈ c) → Set) → Set
All' c P = ∀{Δ} (e : Δ ∈ c) → P e

-- If  c : Cover Γ  and  e : Δ ∈ C,  then Δ must be an extension of Γ.
-- Here, we only prove that it is a thinning.

coverWk : ∀{Γ} {c : Cover Γ} → All c (_≤ Γ)
coverWk here      = id≤
coverWk (left  e) = coverWk e • weak id≤
coverWk (right e) = coverWk e • weak id≤

-- We can substitute leaves in the case tree by case trees in turn.
-- The following is a ``parallel substitution'' operations for covers.

-- If c : Cover Γ and f is a mapping from the leaves of c to case trees
-- we can graft f onto c to get a new case tree  transC c f.

-- Here, the case tree substitution is given as a function from pathes
-- p : Δ ∈ c  to covers.

transC : ∀{Γ} (c : Cover Γ) (f : All c Cover) → Cover Γ
transC hole        f = f here
transC (falseC t)  f = falseC t
transC (orC t c d) f = orC t (transC c (f ∘ left)) (transC d (f ∘ right))

-- Composition of pathes.

-- Assume a c : Cover Γ and a substitution f : Δ ∈ c → ∁over Δ and a path e : Δ ∈ c.
-- Then any path p : Φ ∈ f e can be extended to a path q : Φ ∈ transC c f
-- by essentially concatenating e and p.

-- Note that we maintain f only for the sake of typing.

-- trans∈ : ∀{Γ} (c : Cover Γ) (f : All c Cover) →
--   ∀ {Δ} (e : Δ ∈ c) {Φ} → Φ ∈ f e → Φ ∈ transC c f

trans∈ : ∀{Γ} (c : Cover Γ) (f : All c Cover) →
  All' c λ {Δ} (e : Δ ∈ c) → All (f e) (_∈ transC c f)
trans∈ hole        f here      = id
trans∈ (falseC t)  f ()
trans∈ (orC t c d) f (left  e) = left  ∘ trans∈ c (f ∘ left ) e
trans∈ (orC t c d) f (right e) = right ∘ trans∈ d (f ∘ right) e

-- Splitting of pathes.

-- In a situation similar to the previous lemma:
-- If we have a path q : Φ ∈ transC c f we can split it into some
-- e : Δ ∈ c and p : Φ ∈ f e.

split∈ : ∀{Γ} (c : Cover Γ) (f : All c Cover) {Φ} (q : Φ ∈ transC c f)
  → ∃ λ Δ → ∃ λ (e : Δ ∈ c) → Φ ∈ f e
split∈ hole        f q = _ , _ , q
split∈ (falseC t)  f ()
split∈ (orC t c d) f (left q) with split∈ c (f ∘ left) q
... | Δ , e₁ , e₂ = Δ , left e₁ , e₂
split∈ (orC t c d) f (right q) with split∈ d (f ∘ right) q
... | Δ , e₁ , e₂ = Δ , right e₁ , e₂

-- Syntactic paste (from Thorsten).

-- If for each leave e : Δ ∈ c of a case tree c : Cover Γ we have a normal form
-- f e : Nf Δ A  of type A, grafting these nfs onto c gives us a  Nf Γ A.

pasteNf : ∀{A Γ} (c : Cover Γ) (f : All c λ Δ → Nf Δ A) → Nf Γ A
pasteNf hole        f = f here
pasteNf (falseC t)  f = falseE t
pasteNf (orC t c d) f = orE t (pasteNf c (f ∘ left)) (pasteNf d (f ∘ right))

-- Weakening covers:  A case tree in Γ can be transported to a thinning Δ
-- by weakening all the scrutinees.

-- monC : ∀{Γ Δ} (τ : Δ ≤ Γ) (c : Cover Γ) → Cover Δ
monC : Mon Cover
monC τ hole        = hole
monC τ (falseC t)  = falseC (monNe τ t)
monC τ (orC t c d) = orC (monNe τ t) (monC (lift τ) c) (monC (lift τ) d)

-- Undoing a weakening on a path.
--
-- If we have a path  e : Φ ∈ monC τ c  in a case tree  c : Cover Γ  transported
-- to Δ via thinning  τ : Δ ≤ Γ, we also get a path  e' : Ψ ∈ c  in the original
-- case tree c such that Ψ is a strenthening of Φ  (Φ ≤ Ψ).

mon∈ : ∀{Γ Δ Φ} (c : Cover Γ) (τ : Δ ≤ Γ) (e : Φ ∈ monC τ c) → ∃ λ Ψ → Ψ ∈ c × Φ ≤ Ψ
mon∈  hole τ here = _ , here , τ
mon∈ (falseC t)  τ ()
mon∈ (orC t c d) τ (left e)  with mon∈ c (lift τ) e
... | Ψ , e' , σ = Ψ , left e' , σ
mon∈ (orC t c d) τ (right e) with mon∈ d (lift τ) e
... | Ψ , e' , σ = Ψ , right e' , σ

-- Packaging a case tree with its valuation.

CovExt : (Γ : Cxt) (P : Cxt → Set) → Set
CovExt Γ P = Σ (Cover Γ) λ c → All c P

transCE : ∀ {P Γ} (c : Cover Γ) (f : All c λ Δ → CovExt Δ P) → CovExt Γ P
transCE c f = transC c (proj₁ ∘ f) , λ e →
  let _ , e₁ , e₂ = split∈ c (proj₁ ∘ f) e
  in  f e₁ .proj₂ e₂

monCE : ∀{P} → Mon P → Mon λ Γ → CovExt Γ P
monCE monP τ (c , f) = monC τ c ,  λ {Φ} e →
  let Ψ , e' , σ = mon∈ c τ e
  in  monP σ (f {Ψ} e')

-- The syntactic Beth model.

-- We interpret base propositions  Atom P  by their normal deriviations.
-- ("Normal" is important; "neutral is not sufficient since we need case trees here.)

-- The negative connectives True, ∧, and ⇒ are explained as usual by η-expansion
-- and the meta-level connective.

-- The positive connectives False and ∨ are inhabited by case trees.
-- In case False, the tree has no leaves.
-- In case A ∨ B, each leaf must be in the semantics of either A or B.

T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
T⟦ Atom P ⟧ Γ = Nf Γ (Atom P)
T⟦ True   ⟧ Γ = ⊤
T⟦ False  ⟧ Γ = CovExt Γ λ Δ → ⊥
T⟦ A ∨ B  ⟧ Γ = CovExt Γ λ Δ → T⟦ A ⟧ Δ ⊎ T⟦ B ⟧ Δ
T⟦ A ∧ B  ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
T⟦ A ⇒ B  ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ B ⟧ Δ

-- Monotonicity of the model is proven by induction on the proposition,
-- using monotonicity of covers and the built-in monotonicity at implication.

-- monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ

monT : ∀ A → Mon T⟦ A ⟧
monT (Atom P) = monNf
monT True     = _
monT False    = monCE λ τ ()
monT (A ∨ B)  = monCE λ τ → map-⊎ (monT A τ) (monT B τ)
monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
monT (A ⇒ B) τ f σ = f (σ • τ)

-- Reflection / reification, proven simultaneously by induction on the proposition.

-- Reflection is η-expansion (and recursively reflection);
-- at positive connections we build a case tree with a single scrutinee: the neutral
-- we are reflecting.

-- At implication, we need reification, which produces introductions
-- and reifies the stored case trees.

mutual

  reflect : ∀{Γ} A (t : Ne Γ A) → T⟦ A ⟧ Γ
  reflect (Atom P) t = ne t
  reflect True     t = _
  reflect False    t = falseC t , λ()
  reflect (A ∨ B)  t = orC t hole hole , λ where
    (left  here) → inj₁ (reflect A (hyp top))
    (right here) → inj₂ (reflect B (hyp top))
  reflect (A ∧ B)  t = reflect A (andE₁ t) , reflect B (andE₂ t)
  reflect (A ⇒ B)  t τ a = reflect B (impE (monNe τ t) (reify A a))

  reify : ∀{Γ} A (⟦f⟧ : T⟦ A ⟧ Γ) → Nf Γ A
  reify (Atom P) t      = t
  reify True _          = trueI
  reify False   (c , f) = pasteNf c (⊥-elim ∘ f)
  reify (A ∨ B) (c , f) = pasteNf c ([ orI₁ ∘ reify A , orI₂ ∘ reify B ] ∘ f)
  reify (A ∧ B) (a , b) = andI (reify A a) (reify B b)
  reify (A ⇒ B) ⟦f⟧     = impI (reify B (⟦f⟧ (weak id≤) (reflect A (hyp top))))

-- Semantic paste.

-- This grafts semantic values f onto a case tree c : Cover Γ.
-- For atomic propositions, this is grafting of normal forms (defined before).

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

-- Fundamental theorem
-- Extension of T⟦_⟧ to contexts

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

-- monG : ∀{Γ Δ Φ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ → G⟦ Γ ⟧ Φ

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

-- Variable case.

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

-- A lemma for the orE case.

orElim : ∀ {Γ A B E} → T⟦ A ∨ B ⟧ Γ →
         (∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → T⟦ E ⟧ Δ) →
         (∀{Δ} (τ : Δ ≤ Γ) → T⟦ B ⟧ Δ → T⟦ E ⟧ Δ) →
         T⟦ E ⟧ Γ
orElim (c , f) g h = paste _ c λ e → case f e of [ g (coverWk e) , h (coverWk e) ]

-- A lemma for the falseE case.

-- Casts an empty cover into any semantic value (by contradiction).

falseElim : ∀{Γ A} → T⟦ False ⟧ Γ → T⟦ A ⟧ Γ
falseElim (c , f) = paste _ c (⊥-elim ∘ f)

-- The fundamental theorem

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

-- Identity environment

ide : ∀ Γ → G⟦ Γ ⟧ Γ
ide ε = _
ide (Γ ∙ A) = monG (weak id≤) (ide Γ) , reflect A (hyp top)

-- Normalization

norm : ∀{Γ A} (t : Γ ⊢ A) → Nf Γ A
norm t = reify _ (fund t (ide _))

-- Q.E.D. -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module Computability.Enumeration.Diagonal where

open import Computability.Prelude
open import Computability.Function
open import Computability.Data.Fin.Opposite
open import Computability.Data.Nat.Iteration
open import Computability.Enumeration.Base
open import Data.Nat using (_∸_; pred; ⌊_/2⌋; _≤_; _<_; s≤s; z≤n)
open import Data.Nat.Properties using (+-suc; +-assoc; +-comm; +-identityʳ)
open import Data.Nat.Properties using (*-suc; *-assoc; *-comm; *-zeroʳ)
open import Data.Nat.Properties using (≤-step)
open import Data.Fin using (Fin; zero; suc; inject₁; fromℕ; fromℕ<; toℕ; opposite)
open import Data.Fin.Properties using (toℕ<n; toℕ-fromℕ; toℕ-inject₁; fromℕ<-toℕ)
open import Relation.Binary.PropositionalEquality using (_≢_; cong; sym)
open Relation.Binary.PropositionalEquality.≡-Reasoning

Diagonal : Set
Diagonal = Σ[ k ∈ ℕ ] Fin (suc k)

step-Diag : Diagonal → Diagonal
step-Diag (k , zero) = suc k , fromℕ (suc k)
step-Diag (k , suc i) = k , inject₁ i

triangle : ℕ → ℕ
triangle k = ⌊ suc k * k /2⌋

enum-Diag : ℕ → Diagonal
enum-Diag n = iterate step-Diag n (zero , zero)

code-Diag : Diagonal → ℕ
code-Diag (k , i) = toℕ (opposite i) + triangle k

module TriangleProperties where
  elim-⌊/2⌋ : ∀ k i → ⌊ i * 2 + k /2⌋ ≡ i + ⌊ k /2⌋
  elim-⌊/2⌋ k zero = refl
  elim-⌊/2⌋ k (suc i) rewrite elim-⌊/2⌋ k i = refl

  rewrite-triangle : (k : ℕ) → suc (k + suc (k + k * suc k)) ≡ suc k * 2 + (k + k * k)
  rewrite-triangle k
    rewrite *-comm k (suc k)
          | +-suc k (k + (k + k * k))
          | *-comm k 2
          | +-identityʳ k
          | +-assoc k k (k + k * k) = refl

  triangle-relation : ∀ k → triangle (suc k) ≡ suc k + triangle k
  triangle-relation k =
    begin
      ⌊ suc (suc k) * suc k /2⌋
    ≡⟨ cong ⌊_/2⌋ (rewrite-triangle k) ⟩
      ⌊ suc k * 2 + suc k * k /2⌋
    ≡⟨ elim-⌊/2⌋ (suc k * k) (suc k) ⟩
      suc k + ⌊ suc k * k /2⌋
    ∎

open TriangleProperties

step-Diag-suc : ∀ d → code-Diag (step-Diag d) ≡ suc (code-Diag d)
step-Diag-suc (k , zero)
  rewrite opposite-fromℕ k
        | toℕ-fromℕ k
        | triangle-relation k = refl
step-Diag-suc (k , suc i)
  rewrite opposite-inject₁-suc i
        | toℕ-inject₁ (opposite i) = refl

code-Diag-LInv : ∀ n → code-Diag (enum-Diag n) ≡ n
code-Diag-LInv zero = refl
code-Diag-LInv (suc n) =
  begin
    code-Diag (step-Diag (enum-Diag n))
  ≡⟨ step-Diag-suc (enum-Diag n) ⟩
    suc (code-Diag (enum-Diag n))
  ≡⟨ cong suc (code-Diag-LInv n) ⟩
    suc n
  ∎

enum-Diag-Fin-Order : ∀ k i → (lt : i < suc k) → iterate step-Diag i (k , fromℕ k) ≡ (k , opposite (fromℕ< lt))
enum-Diag-Fin-Order k zero lt = refl
enum-Diag-Fin-Order k (suc i) (s≤s lt)
  rewrite enum-Diag-Fin-Order k i (≤-step lt)
        | opposite-fromℕ< i k lt = refl

enum-Diag-Fin : ∀ k (i : Fin (suc k)) → iterate step-Diag (toℕ i) (k , fromℕ k) ≡ (k , opposite i)
enum-Diag-Fin k i =
  begin
    iterate step-Diag (toℕ i) (k , fromℕ k)
  ≡⟨ enum-Diag-Fin-Order k (toℕ i) (toℕ<n i)⟩
    (k , opposite (fromℕ< (toℕ<n i)))
  ≡⟨ cong (λ e → k , opposite e) (fromℕ<-toℕ i (toℕ<n i)) ⟩
    (k , opposite i)
  ∎

enum-Diag-triangle : ∀ k → enum-Diag (triangle k) ≡ (k , fromℕ k)
enum-Diag-triangle zero = refl
enum-Diag-triangle (suc k) =
  begin
    enum-Diag (triangle (suc k))
  ≡⟨ cong enum-Diag (triangle-relation k) ⟩
    enum-Diag (suc k + triangle k)
  ≡⟨ split-iterate step-Diag (zero , zero) (suc k) (triangle k) ⟩
    iterate step-Diag (suc k) (enum-Diag (triangle k))
  ≡⟨ cong (iterate step-Diag (suc k)) (enum-Diag-triangle k) ⟩
    iterate step-Diag (suc k) (k , fromℕ k)
  ≡⟨ sym (cong (λ e → iterate step-Diag (suc e) (k , fromℕ k)) (toℕ-fromℕ k)) ⟩
    iterate step-Diag (suc (toℕ (fromℕ k))) (k , fromℕ k)
  ≡⟨ cong step-Diag (enum-Diag-Fin k (fromℕ k)) ⟩
    step-Diag (k , opposite (fromℕ k))
  ≡⟨ cong (λ e → step-Diag (k , e)) (opposite-fromℕ k) ⟩
    step-Diag (k , zero)
  ∎

code-Diag-RInv : ∀ d → enum-Diag (code-Diag d) ≡ d
code-Diag-RInv (k , i) =
  begin
    enum-Diag (toℕ (opposite i) + triangle k)
  ≡⟨ split-iterate step-Diag (zero , zero) (toℕ (opposite i)) (triangle k) ⟩
    iterate step-Diag (toℕ (opposite i)) (enum-Diag (triangle k))
  ≡⟨ cong (iterate step-Diag (toℕ (opposite i))) (enum-Diag-triangle k) ⟩
    iterate step-Diag (toℕ (opposite i)) (k , fromℕ k)
  ≡⟨ enum-Diag-Fin k (opposite i) ⟩
    k , opposite (opposite i)
  ≡⟨ cong (λ e → k , e) (opposite-opposite i) ⟩
    k , i
  ∎

open Enumerable

Diag-Enumerable : Enumerable Diagonal
enum Diag-Enumerable = enum-Diag
proj₁ (bijective Diag-Enumerable) {x = n₀} {y = n₁} eq =
  begin
    n₀
  ≡⟨ sym (code-Diag-LInv n₀) ⟩
    code-Diag (enum-Diag n₀)
  ≡⟨ cong code-Diag eq ⟩
    code-Diag (enum-Diag n₁)
  ≡⟨ code-Diag-LInv n₁ ⟩
    n₁
  ∎
proj₁ (proj₂ (bijective Diag-Enumerable) d) = code-Diag d
proj₂ (proj₂ (bijective Diag-Enumerable) d) = code-Diag-RInv d

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
module Issue4869 where

open import Agda.Builtin.Nat

infix 4 _≤_

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

foo : 2 ≤ 1 → Nat
foo (s≤s ()) = 123

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module RecursiveInstanceSearch where

open import Common.Prelude
open import Common.Product

_&&_ : Bool → Bool → Bool
true && b = b
false && _ = false

record Eq (A : Set) : Set where
  constructor eq
  field
    _==_ : A → A → Bool
open Eq {{...}} public

instance
  eq-Bool : Eq Bool
  eq-Bool = eq aux  where

    aux : Bool → Bool → Bool
    aux true true = true
    aux false false = true
    aux _ _ = false

  eq-Nat : Eq Nat
  eq-Nat = eq aux  where

    aux : Nat → Nat → Bool
    aux zero zero = true
    aux (suc n) (suc m) = aux n m
    aux _ _ = false

  eq-Maybe : {A : Set} {{_ : Eq A}} → Eq (Maybe A)
  eq-Maybe {A} = eq aux  where

    aux : Maybe A → Maybe A → Bool
    aux nothing nothing = true
    aux (just y) (just z) = (y == z)
    aux _ _ = false

  eq-List : {A : Set} {{_ : Eq A}} → Eq (List A)
  eq-List {A} = eq aux  where

    aux : List A → List A → Bool
    aux [] [] = true
    aux (x ∷ l) (y ∷ l') = (x == y) && (aux l l')
    aux _ _ = false

  eq-× : {A B : Set} {{_ : Eq A}} {{_ : Eq B}} → Eq (A × B)
  eq-× {A} {B} = eq (λ x y → (proj₁ x == proj₁ y) && (proj₂ x == proj₂ y))

test₂ : Bool
test₂ = (3 == 4)

test₃ : Bool
test₃ = ((just 9) == nothing)

test₃' : Bool
test₃' = (nothing == just 6)

test₄ : Bool
test₄ = (true ∷ []) == (false ∷ [])

test₅ : Bool
test₅ = (just ((true ,′ (1 ,′ just 0)) ∷ []) == just ((true , (1 , just 0)) ∷ []))

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Nullary relations (some core definitions)
------------------------------------------------------------------------

-- The definitions in this file are reexported by Relation.Nullary.

module Relation.Nullary.Core where

open import Data.Empty
open import Level

-- Negation.

infix 3 ¬_

¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬ P = P → ⊥

-- Decidable relations.

data Dec {p} (P : Set p) : Set p where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P


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

open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Setoids
open import Functions.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Groups.Orders.Partial.Definition {n m : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} (G : Group S _+_) where

open Group G
open Setoid S

record PartiallyOrderedGroup {p : _} {_<_ : Rel {_} {p} A} (pOrder : SetoidPartialOrder S _<_) : Set (lsuc n ⊔ m ⊔ p) where
  field
    orderRespectsAddition : {a b : A} → (a < b) → (c : A) → (a + c) < (b + c)


text:
-- This test case is aimed at checking that one can give RTS options
-- (as well as other options) using the Emacs mode. It does not test
-- backend options.


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

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Data.Sigma
open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
open import Cubical.Data.Nat
open import Cubical.Algebra.Group
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3)

open GroupHom

module MV {ℓ ℓ' ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') (f : C → A) (g : C → B) where
  -- Proof from Brunerie 2016.
  -- We first define the three morphisms involved: i, Δ and d.

  private
    i* : (n : ℕ) → coHom n (Pushout f g) → coHom n A × coHom n B
    i* n = sRec (isSet× setTruncIsSet setTruncIsSet) λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂

  iIsHom : (n : ℕ) → isGroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B) (i* n)
  iIsHom n = sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _) λ _ _ → refl

  i : (n : ℕ) → GroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B)
  GroupHom.fun (i n) = i* n
  GroupHom.isHom (i n) = iIsHom n

  private
    distrLem : (n : ℕ) (x y z w : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ (z +[ n ]ₖ w) ≡ (x -[ n ]ₖ z) +[ n ]ₖ (y -[ n ]ₖ w)
    distrLem n x y z w = cong (λ z → (x +[ n ]ₖ y) +[ n ]ₖ z) (-distrₖ n z w)
                     ∙∙ sym (assocₖ n x y ((-[ n ]ₖ z) +[ n ]ₖ (-[ n ]ₖ w)))
                     ∙∙ cong (λ y → x +[ n ]ₖ y) (commₖ n y ((-[ n ]ₖ z) +[ n ]ₖ (-[ n ]ₖ w)) ∙ sym (assocₖ n _ _ _))
                     ∙∙ assocₖ n _ _ _
                     ∙∙ cong (λ y → (x -[ n ]ₖ z) +[ n ]ₖ y) (commₖ n (-[ n ]ₖ w) y)

    Δ' : (n : ℕ) → coHom n A × coHom n B → coHom n C
    Δ' n (α , β) = coHomFun n f α -[ n ]ₕ coHomFun n g β

    Δ'-isMorph : (n : ℕ) → isGroupHom (×coHomGr n A B) (coHomGr n C) (Δ' n)
    Δ'-isMorph n =
      prodElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _ )
        λ f' x1 g' x2 i → ∣ (λ x → distrLem n (f' (f x)) (g' (f x)) (x1 (g x)) (x2 (g x)) i) ∣₂

  Δ : (n : ℕ) → GroupHom (×coHomGr n A B) (coHomGr n C)
  GroupHom.fun (Δ n) = Δ' n
  GroupHom.isHom (Δ n) = Δ'-isMorph n

  d-pre : (n : ℕ) → (C → coHomK n) → Pushout f g → coHomK (suc n)
  d-pre n γ (inl x) = 0ₖ (suc n)
  d-pre n γ (inr x) = 0ₖ (suc n)
  d-pre n γ (push a i) = Kn→ΩKn+1 n (γ a) i

  dHomHelper : (n : ℕ) (h l : C → coHomK n) (x : Pushout f g)
             → d-pre n (λ x → h x +[ n ]ₖ l x) x ≡ d-pre n h x +[ suc n ]ₖ d-pre n l x
  dHomHelper n h l (inl x) = sym (rUnitₖ (suc n) (0ₖ (suc n)))
  dHomHelper n h l (inr x) = sym (lUnitₖ (suc n) (0ₖ (suc n)))
  dHomHelper n h l (push a i) j =
    hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
                    ; (i = i1) → lUnitₖ (suc n) (0ₖ (suc n)) (~ j)
                    ; (j = i0) → Kn→ΩKn+1-hom n (h a) (l a) (~ k) i
                    ; (j = i1) → cong₂Funct (λ x y → x +[ (suc n) ]ₖ y) (Kn→ΩKn+1 n (h a)) (Kn→ΩKn+1 n (l a)) (~ k) i })
          (hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
                           ; (i = i1) → lUnitₖ (suc n) (Kn→ΩKn+1 n (l a) k) (~ j)})
                 (hcomp (λ k → λ { (i = i0) → rUnitₖ (suc n) (0ₖ (suc n)) (~ j)
                                  ; (i = i1) → lUnitₖ≡rUnitₖ (suc n) (~ k) (~ j)
                                  ; (j = i0) → Kn→ΩKn+1 n (h a) i
                                  ; (j = i1) → (Kn→ΩKn+1 n (h a) i) +[ (suc n) ]ₖ coHom-pt (suc n)})
                        (rUnitₖ (suc n) (Kn→ΩKn+1 n (h a) i) (~ j))))

  dIsHom : (n : ℕ) → isGroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (sRec setTruncIsSet λ a → ∣ d-pre n a ∣₂)
  dIsHom n = sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                     λ f g i → ∣ funExt (λ x → dHomHelper n f g x) i ∣₂

  d : (n : ℕ) → GroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g))
  GroupHom.fun (d n) = sRec setTruncIsSet λ a → ∣ d-pre n a ∣₂
  GroupHom.isHom (d n) = dIsHom n

  -- The long exact sequence
  Im-d⊂Ker-i : (n : ℕ) (x : ⟨ (coHomGr (suc n) (Pushout f g)) ⟩)
            → isInIm (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) x
            → isInKer (coHomGr (suc n) (Pushout f g)) (×coHomGr (suc n) A B) (i (suc n)) x
  Im-d⊂Ker-i n = sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
                       λ a → pRec (isOfHLevelPath' 1 (isSet× setTruncIsSet setTruncIsSet) _ _)
                               (sigmaElim (λ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
                                λ δ b i → sRec (isSet× setTruncIsSet setTruncIsSet)
                                               (λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂ ) (b (~ i)))

  Ker-i⊂Im-d : (n : ℕ) (x : ⟨ coHomGr (suc n) (Pushout f g) ⟩)
             → isInKer (coHomGr (suc n) (Pushout f g)) (×coHomGr (suc n) A B) (i (suc n)) x
             → isInIm (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) x
  Ker-i⊂Im-d n =
     sElim (λ _ → isSetΠ λ _ → isProp→isSet propTruncIsProp)
           λ a p → pRec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ (suc n)}
                        (isProp→ propTruncIsProp)
                        (λ p1 → pRec propTruncIsProp λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn n (sym (cong (λ F → F (f c)) p1)
                                                                                ∙∙ cong a (push c)
                                                                                ∙∙ cong (λ F → F (g c)) p2)) ∣₂
                                                                             , cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁)
                                       (Iso.fun PathIdTrunc₀Iso (cong fst p))
                                       (Iso.fun PathIdTrunc₀Iso (cong snd p))

      where
      helper : (F : (Pushout f g) → coHomK (suc n))
               (p1 : Path (_ → coHomK (suc n)) (λ a₁ → F (inl a₁)) (λ _ → coHom-pt (suc n)))
               (p2 : Path (_ → coHomK (suc n)) (λ a₁ → F (inr a₁)) (λ _ → coHom-pt (suc n)))
             → (δ : Pushout f g)
             → d-pre n (λ c → ΩKn+1→Kn n ((λ i₁ → p1 (~ i₁) (f c))
                                                     ∙∙ cong F (push c)
                                                     ∙∙ cong (λ F → F (g c)) p2)) δ
              ≡ F δ
      helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1)
      helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2)
      helper F p1 p2 (push a i) j =
        hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a)
                       ; (i = i1) → p2 (~ j) (g a)
                       ; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 n) ((λ i₁ → p1 (~ i₁) (f a))
                                                                       ∙∙ cong F (push a)
                                                                       ∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i
                        ; (j = i1) → F (push a i)})
              (doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i)

  open GroupHom

  Im-i⊂Ker-Δ : (n : ℕ) (x : ⟨ ×coHomGr n A B ⟩)
            → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) x
            → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) x
  Im-i⊂Ker-Δ n (Fa , Fb) =
    sElim {B = λ Fa → (Fb : _) → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) (Fa , Fb)
                               → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) (Fa , Fb)}
          (λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          (λ Fa → sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                        λ Fb → pRec (setTruncIsSet _ _)
                                     (sigmaElim (λ x → isProp→isSet (setTruncIsSet _ _))
                                                λ Fd p → helper n Fa Fb Fd p))
          Fa
          Fb
    where
    helper : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n) (Fd : (Pushout f g) → coHomK n)
          → (fun (i n) ∣ Fd ∣₂ ≡ (∣ Fa ∣₂ , ∣ Fb ∣₂))
          → (fun (Δ n)) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
    helper n Fa Fb Fd p = cong (fun (Δ n)) (sym p)
                           ∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ n ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂ )
                           ∙∙ rCancelₕ n ∣ (λ x → Fd (inl (f x))) ∣₂

  Ker-Δ⊂Im-i : (n : ℕ) (a : ⟨ ×coHomGr n A B ⟩)
            → isInKer (×coHomGr n A B) (coHomGr n C) (Δ n) a
            → isInIm (coHomGr n (Pushout f g)) (×coHomGr n A B) (i n) a
  Ker-Δ⊂Im-i n = prodElim (λ _ → isSetΠ (λ _ → isProp→isSet propTruncIsProp))
                          (λ Fa Fb p → pRec propTruncIsProp
                                            (λ q → ∣ ∣ helpFun Fa Fb q ∣₂ , refl ∣₁)
                                            (helper Fa Fb p))
    where
    helper : (Fa : A → coHomK n) (Fb : B → coHomK n)
           → fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n
           → ∥ Path (_ → _) (λ c → Fa (f c)) (λ c → Fb (g c)) ∥₁
    helper Fa Fb p = Iso.fun PathIdTrunc₀Iso
                               (sym (cong ∣_∣₂ (funExt (λ x → sym (assocₖ n _ _ _)
                               ∙∙ cong (λ y → Fa (f x) +[ n ]ₖ y) (lCancelₖ n (Fb (g x)))
                               ∙∙ rUnitₖ n (Fa (f x)))))
                               ∙∙ cong (λ x → x +[ n ]ₕ ∣ (λ c → Fb (g c)) ∣₂) p
                               ∙∙ lUnitₕ n _)

    helpFun : (Fa : A → coHomK n) (Fb : B → coHomK n)
            → ((λ c → Fa (f c)) ≡ (λ c → Fb (g c)))
            → Pushout f g → coHomK n
    helpFun Fa Fb p (inl x) = Fa x
    helpFun Fa Fb p (inr x) = Fb x
    helpFun Fa Fb p (push a i) = p i a

  private
    distrHelper : (n : ℕ) (p q : _)
                → ΩKn+1→Kn n p +[ n ]ₖ (-[ n ]ₖ ΩKn+1→Kn n q) ≡ ΩKn+1→Kn n (p ∙ sym q)
    distrHelper n p q = cong (λ x → ΩKn+1→Kn n p +[ n ]ₖ x) helper ∙ sym (ΩKn+1→Kn-hom n _ _)
      where
      helper : -[ n ]ₖ ΩKn+1→Kn n q ≡ ΩKn+1→Kn n (sym q)
      helper =
           sym (rUnitₖ n _)
        ∙∙ cong (λ x → (-[ n ]ₖ (ΩKn+1→Kn n q)) +[ n ]ₖ x) (sym helper2)
        ∙∙ (assocₖ n _ _ _ ∙∙ cong (λ x → x +[ n ]ₖ (ΩKn+1→Kn n (sym q))) (lCancelₖ n _) ∙∙ lUnitₖ n _)
        where
        helper2 : ΩKn+1→Kn n q +[ n ]ₖ (ΩKn+1→Kn n (sym q)) ≡ coHom-pt n
        helper2 = sym (ΩKn+1→Kn-hom n q (sym q)) ∙∙ cong (ΩKn+1→Kn n) (rCancel q) ∙∙ ΩKn+1→Kn-refl n

  Ker-d⊂Im-Δ : (n : ℕ) (a : coHom n C)
             → isInKer (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) a
             → isInIm (×coHomGr n A B) (coHomGr n C) (Δ n) a
  Ker-d⊂Im-Δ n =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
          λ Fc p → pRec propTruncIsProp (λ p → ∣ (∣ (λ a → ΩKn+1→Kn n (cong (λ f → f (inl a)) p)) ∣₂ ,
                                                     ∣ (λ b → ΩKn+1→Kn n (cong (λ f → f (inr b)) p)) ∣₂) ,
                                                  Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁)
                                         (Iso.fun (PathIdTrunc₀Iso) p)

    where

    helper2 : (Fc : C → coHomK n)
              (p : d-pre n Fc ≡ (λ _ → coHom-pt (suc n))) (c : C)
            → ΩKn+1→Kn n (λ i₁ → p i₁ (inl (f c))) -[ n ]ₖ (ΩKn+1→Kn n (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c
    helper2 Fc p c = distrHelper n _ _ ∙∙ cong (ΩKn+1→Kn n) helper3 ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) (Fc c)
      where
      helper3 : (λ i₁ → p i₁ (inl (f c))) ∙ sym (λ i₁ → p i₁ (inr (g c))) ≡ Kn→ΩKn+1 n (Fc c)
      helper3 = cong ((λ i₁ → p i₁ (inl (f c))) ∙_) (lUnit _) ∙ sym (PathP→compPathR (cong (λ f → cong f (push c)) p))

  Im-Δ⊂Ker-d : (n : ℕ) (a : coHom n C)
             → isInIm (×coHomGr n A B) (coHomGr n C) (Δ n) a
             → isInKer (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (d n) a
  Im-Δ⊂Ker-d n =
    sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          λ Fc → pRec (isOfHLevelPath' 1 setTruncIsSet _ _)
                       (sigmaProdElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                      λ Fa Fb p → pRec (isOfHLevelPath' 1 setTruncIsSet _ _)
                                                        (λ q → ((λ i → fun (d n) ∣ (q (~ i)) ∣₂) ∙ dΔ-Id n Fa Fb))
                                                        (Iso.fun (PathIdTrunc₀Iso) p))

    where
    d-preLeftId : (n : ℕ) (Fa : A → coHomK n)(d : (Pushout f g))
                → d-pre n (Fa ∘ f) d ≡ 0ₖ (suc n)
    d-preLeftId n Fa (inl x) = Kn→ΩKn+1 n (Fa x)
    d-preLeftId n Fa (inr x) = refl
    d-preLeftId n Fa (push a i) j = Kn→ΩKn+1 n (Fa (f a)) (j ∨ i)

    d-preRightId : (n : ℕ) (Fb : B → coHomK n) (d : (Pushout f g))
                → d-pre n (Fb ∘ g) d ≡ 0ₖ (suc n)
    d-preRightId n Fb (inl x) = refl
    d-preRightId n Fb (inr x) = sym (Kn→ΩKn+1 n (Fb x))
    d-preRightId n Fb (push a i) j = Kn→ΩKn+1 n (Fb (g a)) (~ j ∧ i)

    dΔ-Id : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n)
            → fun (d n) (fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂)) ≡ 0ₕ (suc n)
    dΔ-Id n Fa Fb = -distrLemma n (suc n) (d n) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂
                    ∙∙ (λ i → ∣ (λ x → d-preLeftId n Fa x i) ∣₂ -[ (suc n) ]ₕ ∣ (λ x → d-preRightId n Fb x i) ∣₂)
                    ∙∙ rCancelₕ (suc n) (0ₕ (suc n))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Lib where
open import Data.List
open import Relation.Binary.PropositionalEquality

data _∧_ (A : Set) (B : Set) : Set where
  ∧-intro : A → B → (A ∧ B)

--------------------------------
-- Extension with Pairs and Sums
--------------------------------

--------------------------------
-- Basic Set-up
--------------------------------
record Sg  (S : Set) (T : S → Set) : Set where
  constructor _,_
  field
    ffst : S
    ssnd : T ffst
open Sg public

--pair type on the agda level
_*_ : Set → Set → Set
S * T = Sg S \ _ → T
--proj functions on the agda level
fst : {A B : Set} → A * B → A
fst (a , b) =  a

snd : {A B : Set} → A * B → B
snd (a , b) =  b

--sum type on the agda level
data _⨄_ (A : Set) (B : Set) : Set where
  tl : (a : A) → A ⨄ B
  tr : (b : B) → A ⨄ B

--typeofSum : ∀ {A B : Set} (sum : A ⨄ B) → Set
--typeofSum {A = A} (tl _) = A
--typeofSum {B = B} (tr _) = B

-- Pointer into a list. It is similar to list membership as defined in
-- Data.List.AnyMembership, rather than going through propositional
-- equality, it asserts the existence of the referenced element
-- directly.
module ListReference where
  infix 4 _∈_
  data _∈_ {A : Set} : A → List A → Set where
    hd : ∀ {x xs} → x ∈ (x ∷ xs)
    tl : ∀ {x y xs} → x ∈ xs → x ∈ (y ∷ xs)
open ListReference public

mapIdx : {A B : Set} → (f : A → B) →
         {x : A} {xs : List A} → x ∈ xs → f x ∈ map f xs
mapIdx f hd = hd
mapIdx f (tl x₁) = tl (mapIdx f x₁)

-- Extension of lists at the front and, as a generalization, extension
-- of lists somewhere in the middle.
module ListExtension where
  open import Relation.Binary.PropositionalEquality

  -- Extension of a list by consing elements at the front.
  data _↝_ {A : Set} : List A → List A → Set where
    ↝-refl   : ∀ {Γ}      → Γ ↝ Γ
    ↝-extend : ∀ {Γ Γ' τ} → Γ ↝ Γ' → Γ ↝ (τ ∷ Γ')

  -- Combining two transitive extensions.
  ↝-trans : ∀ {A : Set}{Γ Γ' Γ'' : List A} → Γ ↝ Γ' → Γ' ↝ Γ'' → Γ ↝ Γ''
  ↝-trans Γ↝Γ' ↝-refl = Γ↝Γ'
  ↝-trans Γ↝Γ' (↝-extend Γ'↝Γ'') = ↝-extend (↝-trans Γ↝Γ' Γ'↝Γ'')

  -- Of course, ↝-refl is the identity for combining two extensions.
  lem-↝-refl-id : ∀ {A : Set} {Γ Γ' : List A} →
                    (Γ↝Γ' : Γ ↝ Γ') →
                    Γ↝Γ' ≡ (↝-trans ↝-refl Γ↝Γ')
  lem-↝-refl-id ↝-refl = refl
  lem-↝-refl-id (↝-extend Γ↝Γ') = cong ↝-extend (lem-↝-refl-id Γ↝Γ')

  -- Extending a list in the middle:
  data _↝_↝_ {A : Set} : List A → List A → List A → Set where
    -- First prepend the extension list to the common suffix
    ↝↝-base   : ∀ {Γ Γ''} → Γ ↝ Γ'' → Γ ↝ [] ↝ Γ''
    -- ... and then add the common prefix
    ↝↝-extend : ∀ {Γ Γ' Γ'' τ} →
                 Γ ↝ Γ' ↝ Γ'' → (τ ∷ Γ) ↝ (τ ∷ Γ') ↝ (τ ∷ Γ'')
open ListExtension public

    ---------------------------------
    -- helper functions for rewriting
    ---------------------------------
→tl : ∀ {A B x' y'} (x y : A ⨄ B)→ x ≡ y →  x ≡ tl x' → y ≡ tl y' → x' ≡ y'
→tl {x' = x'} px py a b c rewrite b | c with py | a
... | H | refl = refl
-- →tl {α} {α'} {.y'} {y'} px py a b c | refl | ._ | refl | ._ | refl = ? -- rewrite b | c = {!!}

→tr : ∀ {A B x' y'} (x y : A ⨄ B)→ x ≡ y →  x ≡ tr x' → y ≡ tr y' → x' ≡ y'
→tr px py a b c rewrite c | b with px | a
... | H | refl = refl
    ---------------------------------

max_stars_repo_name: luminousfennell/polybta

max_issues_repo_name: luminousfennell/polybta

max_forks_repo_name: luminousfennell/polybta


text:
module Base where

module Classes where

  record LeastUpperBound {ℓ} (A : Set ℓ) : Set ℓ where
    infixl 6 _⊔_
    field
      _⊔_ : A → A → A

  open LeastUpperBound ⦃ … ⦄ public

  record Successor {ℓ} (A : Set ℓ) : Set ℓ where
    field
      ↑ : A → A

  open Successor ⦃ … ⦄ public

module Primitive where
  import Agda.Primitive as P

  open Classes

  instance LeastUpperBoundLevel : LeastUpperBound P.Level
  LeastUpperBound._⊔_ LeastUpperBoundLevel = P._⊔_

  instance SuccessorLevel : Successor P.Level
  Successor.↑ SuccessorLevel = P.lsuc

open Primitive
open Classes

infix -65536 ℞_
℞_ : ∀ ℓ → Set _
℞_ ℓ = Set ℓ

record IsIndexedReflexive {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) {ℓ} (ėq : ∀ {𝑥} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ) : ℞ 𝔵 ⊔ 𝔞 ⊔ ℓ where
  private
    infix 4 _≈̇_
    _≈̇_ = ėq
  field
    ṙeflexivity : ∀ {𝑥} (a : 𝔄 𝑥) → a ≈̇ a

open IsIndexedReflexive ⦃ … ⦄ public

record IsIndexedSymmetric {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) {ℓ} (ėq : ∀ {𝑥} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ) : ℞ 𝔵 ⊔ 𝔞 ⊔ ℓ where
  private
    infix 4 _≈̇_
    _≈̇_ = ėq
  field
    ṡymmetry : ∀ {𝑥} (a b : 𝔄 𝑥) → a ≈̇ b → b ≈̇ a

open IsIndexedSymmetric ⦃ … ⦄ public

record IsIndexedTransitive {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) {ℓ} (ėq : ∀ {𝑥} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ) : ℞ 𝔵 ⊔ 𝔞 ⊔ ℓ where
  private
    infix 4 _≈̇_
    _≈̇_ = ėq
  field
    ṫransitivity : ∀ {𝑥} (a b c : 𝔄 𝑥) → a ≈̇ b → b ≈̇ c → a ≈̇ c

open IsIndexedTransitive ⦃ … ⦄ public

record IsIndexedEquivalence {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) {ℓ} (ėq : ∀ {𝑥 : 𝔛} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ) : ℞ 𝔵 ⊔ 𝔞 ⊔ ℓ where
  field
    ⦃ isReflexive ⦄ : IsIndexedReflexive 𝔄 ėq
    ⦃ isSymmetric ⦄ : IsIndexedSymmetric 𝔄 ėq
    ⦃ isTransitive ⦄ : IsIndexedTransitive 𝔄 ėq

open IsIndexedEquivalence ⦃ … ⦄ public

record IndexedEquivalence {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) ℓ : ℞ 𝔵 ⊔ 𝔞 ⊔ ↑ ℓ where
  infix 4 _≈̇_
  field
    _≈̇_ : ∀ {𝑥 : 𝔛} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ
    ⦃ isIndexedEquivalence ⦄ : IsIndexedEquivalence 𝔄 _≈̇_

open import Prelude.Nat
open import Prelude.Fin
open import Prelude.Equality
open import Prelude.Function

postulate
  eFin : ∀ {n} → Fin n → Fin n → Set

eqFin : ∀ {n} → Fin n → Fin n → Set
eqFin = _≡_

module IndexedEquivalence₁ = IndexedEquivalence
open IndexedEquivalence₁ ⦃ … ⦄ renaming (_≈̇_ to _≈̇₁_)

module IndexedEquivalence₂ = IndexedEquivalence
open IndexedEquivalence₂ ⦃ … ⦄ renaming (_≈̇_ to _≈̇₂_)

postulate
  instance IndexedEquivalenceFinProp : IndexedEquivalence Fin _

-- instance IsIndexedReflexiveEqFin : IsIndexedReflexive Fin _≡_
-- IsIndexedReflexive.ṙeflexivity IsIndexedReflexiveEqFin a = it

-- {-
-- instance IndexedEquivalenceProp : ∀ {𝔵} {𝔛 : Set 𝔵} {𝔞} {𝔄 : 𝔛 → Set 𝔞} → IndexedEquivalence 𝔄 𝔞
-- IndexedEquivalence._≈̇_ IndexedEquivalenceProp = _≡_
-- IsIndexedEquivalence.isReflexive (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceProp) = {!!}
-- IsIndexedEquivalence.isSymmetric (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceProp) = {!!}
-- IsIndexedEquivalence.isTransitive (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceProp) = {!!}
-- -}

-- instance IndexedEquivalenceFinProp : IndexedEquivalence Fin _
-- IndexedEquivalence._≈̇_ IndexedEquivalenceFinProp = _≡_
-- IsIndexedEquivalence.isReflexive (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceFinProp) = it
-- IsIndexedEquivalence.isSymmetric (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceFinProp) = {!!}
-- IsIndexedEquivalence.isTransitive (IndexedEquivalence.isIndexedEquivalence IndexedEquivalenceFinProp) = {!!}

-- someFin : Fin 5
-- someFin = suc (suc zero)

-- eqFinLemma : someFin ≈̇ someFin
-- eqFinLemma = ṙeflexivity someFin

-- record IsReflexive {𝔞} {𝔄 : Set 𝔞} {ℓ} (eq : 𝔄 → 𝔄 → Set ℓ) : ℞ 𝔞 ⊔ ℓ where
--   private
--     infix 4 _≈_
--     _≈_ = eq
--   field
--     reflexivity : ∀ a → a ≈ a

-- open IsReflexive ⦃ … ⦄

-- record IsSymmetric {𝔞} {𝔄 : Set 𝔞} {ℓ} (eq : 𝔄 → 𝔄 → Set ℓ) : ℞ 𝔞 ⊔ ℓ where
--   private
--     infix 4 _≈_
--     _≈_ = eq
--   field
--     symmetry : ∀ a b → a ≈ b → b ≈ a

-- open IsReflexive ⦃ … ⦄

-- record IsTransitive {𝔞} {𝔄 : Set 𝔞} {ℓ} (eq : 𝔄 → 𝔄 → Set ℓ) : ℞ 𝔞 ⊔ ℓ where
--   private
--     infix 4 _≈_
--     _≈_ = eq
--   field
--     transitivity : ∀ a b c → a ≈ b → b ≈ c → a ≈ c

-- open IsTransitive ⦃ … ⦄

-- record IsEquivalence {𝔞} {𝔄 : Set 𝔞} {ℓ} (eq : 𝔄 → 𝔄 → Set ℓ) : ℞ 𝔞 ⊔ ℓ where
--   field
--     ⦃ isReflexive ⦄ : IsReflexive eq
--     ⦃ isSymmetric ⦄ : IsSymmetric eq
--     ⦃ isTransitive ⦄ : IsTransitive eq

-- open IsEquivalence ⦃ … ⦄

-- record Equivalence {𝔞} {𝔄 : Set 𝔞} ℓ : ℞ 𝔞 ⊔ ↑ ℓ where
--   infix 4 _≈_
--   field
--     _≈_ : 𝔄 → 𝔄 → Set ℓ
--     ⦃ isEquivalence ⦄ : IsEquivalence _≈_

-- open Equivalence ⦃ … ⦄

-- data IndexedTree {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) : ℞ 𝔵 ⊔ 𝔞 where
--   leaf : IndexedTree 𝔄
--   _fork_ : IndexedTree 𝔄 → IndexedTree 𝔄 → IndexedTree 𝔄
--   variable : ∀ {𝑥} → 𝔄 𝑥 → IndexedTree 𝔄

-- infix 4 _≈ᵗ_
-- data _≈ᵗ_ {𝔵} {𝔛 : Set 𝔵} {𝔞} {𝔄 : 𝔛 → Set 𝔞} ⦃ _ : IndexedEquivalence 𝔄 𝔞 ⦄ : IndexedTree 𝔄 → IndexedTree 𝔄 → ℞ 𝔵 ⊔ 𝔞 where
--   leaf : leaf ≈ᵗ leaf
--   _fork_ : ∀ {left-t₁ left-t₂ right-t₁ right-t₂} →
--              left-t₁ ≈ᵗ left-t₂ →
--              right-t₁ ≈ᵗ right-t₂ →
--              left-t₁ fork right-t₁ ≈ᵗ left-t₂ fork right-t₂
--   variable : ∀ {a} → {left-x right-x : 𝔄 a} → left-x ≈̇ right-x → variable left-x ≈ᵗ variable right-x

-- -- reflexivityIndexedTreeEquality : ∀ {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) ⦃ _ : IndexedEquivalence 𝔄 𝔞 ⦄ (a : IndexedTree 𝔄) → a ≈ᵗ a
-- -- reflexivityIndexedTreeEquality 𝔄 leaf = leaf
-- -- reflexivityIndexedTreeEquality 𝔄 (a fork a₁) = (reflexivityIndexedTreeEquality 𝔄 _≈_ a) fork (reflexivityIndexedTreeEquality 𝔄 _≈_ a₁)
-- -- reflexivityIndexedTreeEquality 𝔄 (variable x₁) = variable (ṙeflexivity _)

-- -- -- instance IsEquivalenceIndexedTreeEquality : ∀ {𝔵} {𝔛 : Set 𝔵} {𝔞} (𝔄 : 𝔛 → Set 𝔞) {ℓ} (_≈_ : ∀ {𝑥} → 𝔄 𝑥 → 𝔄 𝑥 → Set ℓ) ⦃ _ : IsIndexedEquivalence 𝔄 _≈_ ⦄ → IsEquivalence ((IndexedTreeEquality 𝔄 _≈_))
-- -- -- IsReflexive.reflexivity (IsEquivalence.isReflexive (IsEquivalenceIndexedTreeEquality 𝔄 _≈_)) a = reflexivityIndexedTreeEquality 𝔄 _≈_ a
-- -- -- IsEquivalence.isSymmetric (IsEquivalenceIndexedTreeEquality 𝔄 _≈_) = {!!}
-- -- -- IsEquivalence.isTransitive (IsEquivalenceIndexedTreeEquality 𝔄 _≈_) = {!!}

-- -- -- data Tree {𝔞} (𝔄 : Set 𝔞) : ℞ 𝔞 where
-- -- --   leaf : Tree 𝔄
-- -- --   _fork_ : Tree 𝔄 → Tree 𝔄 → Tree 𝔄
-- -- --   variable : 𝔄 → Tree 𝔄


text:
-- exercises-01-monday.agda

open import Data.Nat

variable
  A B C : Set

-- Exercise 1

add3 : ℕ → ℕ
add3 x = x + 3

tw : (A → A) → A → A
tw f n = f (f n) -- tw = λ f n → f (f n)

-- evaluate: "tw tw add3 1"; derive the result (in a comment) step by step
{-
    tw tw add3 1 =
  = tw (tw add3) 1 =
  = (tw add3) (tw add3 1) =
  = (tw add3) (add3 (add3 1))
  = tw add3 7 =
  = add3 (add3 7) =
  = 13
-}

-- Exercise 2

-- derive lambda terms with the following types

f₀ : (A → B) → (B → C) → (A → C)
f₀ f g a = g (f a)

f₁ : (A → B) → ((A → C) → C) → ((B → C) → C)
f₁ f g h = g λ a -> h (f a)

f₂ : (A → B → C) → B → A → C
f₂ f b a = f a b

-- Exercise 3

-- derive a function tw-c which behaves the same as tw using only S, K (and I
-- which is defined using S and K below).

K : A → B → A
K = λ a b → a

S : (A → B → C) → (A → B) → A → C
S = λ f g x → f x (g x)

-- I = λ x → x
I : A → A
I {A} = S K (K {B = A})

{-
    λ f n → f (f n) =
  = λ f → λ n → f (f n) =
  = λ f → S (λ n → f) (λ n → f n) =
  = λ f → S (K f) f =
  = S (λ f → S (K f) (λ f → f) =
  = S (S (λ f → S) (λ f → (K f)) I =
  = S (S (K S) K) I =
-}

tw-c : (A → A) → A → A
tw-c = S (S (K S) K) I

max_stars_repo_path: Type Theory/exercises-01-monday.agda

max_issues_repo_path: Type Theory/exercises-01-monday.agda

max_forks_repo_path: Type Theory/exercises-01-monday.agda


text:
module Issue840a where

------------------------------------------------------------------------
-- Prelude

record ⊤ : Set where

data ⊥ : Set where

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

data Bool : Set where
  true false : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

postulate String : Set

{-# BUILTIN STRING String #-}

primitive primStringEquality : String → String → Bool

infixr 4 _,_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

------------------------------------------------------------------------
-- Other stuff

mutual

  infixl 5 _,_∶_

  data Signature : Set₁ where
    ∅     : Signature
    _,_∶_ : (Sig : Signature)
            (ℓ : String)
            (A : Record Sig → Set) →
            Signature

  record Record (Sig : Signature) : Set where
    constructor rec
    field fun : Record-fun Sig

  Record-fun : Signature → Set
  Record-fun ∅             = ⊤
  Record-fun (Sig , ℓ ∶ A) = Σ (Record Sig) A

_∈_ : String → Signature → Set
ℓ ∈ ∅              = ⊥
ℓ ∈ (Sig , ℓ′ ∶ A) with primStringEquality ℓ ℓ′
... | true  = ⊤
... | false = ℓ ∈ Sig

Restrict : (Sig : Signature) (ℓ : String) → ℓ ∈ Sig → Signature
Restrict ∅              ℓ ()
Restrict (Sig , ℓ′ ∶ A) ℓ ℓ∈ with primStringEquality ℓ ℓ′
... | true  = Sig
... | false = Restrict Sig ℓ ℓ∈

Proj : (Sig : Signature) (ℓ : String) {ℓ∈ : ℓ ∈ Sig} →
       Record (Restrict Sig ℓ ℓ∈) → Set
Proj ∅              ℓ {}
Proj (Sig , ℓ′ ∶ A) ℓ {ℓ∈} with primStringEquality ℓ ℓ′
... | true  = A
... | false = Proj Sig ℓ {ℓ∈}

_∣_ : {Sig : Signature} → Record Sig →
      (ℓ : String) {ℓ∈ : ℓ ∈ Sig} → Record (Restrict Sig ℓ ℓ∈)
_∣_ {Sig = ∅}            r       ℓ {}
_∣_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with primStringEquality ℓ ℓ′
... | true  = Σ.proj₁ r
... | false = _∣_ (Σ.proj₁ r) ℓ {ℓ∈}

infixl 5 _·_

_·_ : {Sig : Signature} (r : Record Sig)
      (ℓ : String) {ℓ∈ : ℓ ∈ Sig} →
      Proj Sig ℓ {ℓ∈} (r ∣ ℓ)
_·_ {Sig = ∅}            r       ℓ {}
_·_ {Sig = Sig , ℓ′ ∶ A} (rec r) ℓ {ℓ∈} with primStringEquality ℓ ℓ′
... | true  = Σ.proj₂ r
... | false = _·_ (Σ.proj₁ r) ℓ {ℓ∈}

R : Set → Signature
R A = ∅ , "f"     ∶ (λ _ → A → A)
        , "x"     ∶ (λ _ → A)
        , "lemma" ∶ (λ r → ∀ y → (r · "f") y ≡ y)

record GS (A B : Set) : Set where
  field
    get     : A → B
    set     : A → B → A
    get-set : ∀ a b → get (set a b) ≡ b
    set-get : ∀ a → set a (get a) ≡ a

f : {A : Set} →
    GS (Record (R A))
       (Record (∅ , "f"     ∶ (λ _ → A → A)
                  , "lemma" ∶ (λ r → ∀ x → (r · "f") x ≡ x)))
f = record
  { set     = λ r f-lemma → rec (rec (rec (rec _
                , f-lemma · "f")
                , r · "x")
                , f-lemma · "lemma")
  ; get-set = λ { (rec (rec (rec (_ , _) , _) , _))
                  (rec (rec (_ , _) , _)) → refl }
  ; set-get = λ { (rec (rec (rec (rec _ , _) , _) , _)) → refl }
  }

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Relation.Binary.Core

module PLRTree.Insert.Heap {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)
                     (trans≤ : Transitive _≤_) where

open import Data.Sum
open import Order.Total _≤_ tot≤
open import PLRTree {A}
open import PLRTree.Compound {A}
open import PLRTree.Insert _≤_ tot≤
open import PLRTree.Insert.Properties _≤_ tot≤
open import PLRTree.Heap _≤_
open import PLRTree.Heap.Properties _≤_ trans≤

lemma-insert-≤* : {x y : A}{t : PLRTree} → x ≤ y → x ≤* t → x ≤* insert y t
lemma-insert-≤* {y = y} x≤y (lf≤* x) = nd≤* x≤y (lf≤* x) (lf≤* x)
lemma-insert-≤* {y = y} x≤y (nd≤* {perfect} {x} {z} {l} {r} x≤z x≤*l x≤*r)
    with tot≤ y z | l | r
... | inj₁ y≤z | leaf | leaf = nd≤* x≤y (nd≤* x≤z x≤*r x≤*r) x≤*r
... | inj₁ y≤z | node _ _ _ _ | leaf = nd≤* x≤y (lemma-insert-≤* x≤z x≤*l) x≤*r
... | inj₁ y≤z | leaf | node _ _ _ _ = nd≤* x≤y (nd≤* x≤z x≤*l x≤*l) x≤*r
... | inj₁ y≤z | node _ _ _ _ | node _ _ _ _ = nd≤* x≤y (lemma-insert-≤* x≤z x≤*l) x≤*r
... | inj₂ z≤y | leaf | leaf = nd≤* x≤z (nd≤* x≤y x≤*r x≤*r) x≤*r
... | inj₂ z≤y | node _ _ _ _ | leaf = nd≤* x≤z (lemma-insert-≤* x≤y x≤*l) x≤*r
... | inj₂ z≤y | leaf | node _ _ _ _ = nd≤* x≤z (nd≤* x≤y x≤*l x≤*l) x≤*r
... | inj₂ z≤y | node _ _ _ _ | node _ _ _ _ = nd≤* x≤z (lemma-insert-≤* x≤y x≤*l) x≤*r
lemma-insert-≤* {y = y} x≤y (nd≤* {left} {x} {z} {l} {r} x≤z x≤*l x≤*r)
    with tot≤ y z
... | inj₁ y≤z
    with insert z l | lemma-insert-≤* (trans≤ x≤y y≤z) x≤*l | lemma-insert-compound z l
... | node perfect z' l' r' | x≤*lᵢ | compound = nd≤* x≤y x≤*lᵢ x≤*r
... | node right z' l' r' | x≤*lᵢ | compound = nd≤* x≤y x≤*lᵢ x≤*r
... | node left z' l' r' | x≤*lᵢ | compound = nd≤* x≤y x≤*lᵢ x≤*r
lemma-insert-≤* {y = y} x≤y (nd≤* {left} {x} {z} {l} {r} x≤z x≤*l x≤*r) | inj₂ z≤y
    with insert y l  | lemma-insert-≤* x≤y x≤*l | lemma-insert-compound y l
... | node perfect y' l' r' | x≤*lᵢ | compound = nd≤* x≤z x≤*lᵢ x≤*r
... | node right y' l' r' | x≤*lᵢ | compound = nd≤* x≤z x≤*lᵢ x≤*r
... | node left y' l' r' | x≤*lᵢ | compound = nd≤* x≤z x≤*lᵢ x≤*r
lemma-insert-≤* {y = y} x≤y (nd≤* {right} {x} {z} {l} {r} x≤z x≤*l x≤*r)
    with tot≤ y z
... | inj₁ y≤z
    with insert z r | lemma-insert-≤* (trans≤ x≤y y≤z) x≤*r | lemma-insert-compound z r
... | node perfect z' l' r' | x≤*rᵢ | compound = nd≤* x≤y x≤*l x≤*rᵢ
... | node right z' l' r' | x≤*rᵢ | compound = nd≤* x≤y x≤*l x≤*rᵢ
... | node left z' l' r' | x≤*rᵢ | compound = nd≤* x≤y x≤*l x≤*rᵢ
lemma-insert-≤* {y = y} x≤y (nd≤* {right} {x} {z} {l} {r} x≤z x≤*l x≤*r) | inj₂ z≤y
    with insert y r  | lemma-insert-≤* x≤y x≤*r | lemma-insert-compound y r
... | node perfect y' l' r' | x≤*rᵢ | compound = nd≤* x≤z x≤*l x≤*rᵢ
... | node right y' l' r' | x≤*rᵢ | compound = nd≤* x≤z x≤*l x≤*rᵢ
... | node left y' l' r' | x≤*rᵢ | compound = nd≤* x≤z x≤*l x≤*rᵢ

lemma-insert-≤*' : {x y : A}{t : PLRTree} → x ≤ y → y ≤* t → x ≤* insert y t
lemma-insert-≤*' x≤y y≤*t = lemma-≤-≤* x≤y (lemma-insert-≤* refl≤ y≤*t)

lemma-insert-heap : {t : PLRTree}(x : A) → Heap t → Heap (insert x t)
lemma-insert-heap x leaf = node (lf≤* x) (lf≤* x) leaf leaf
lemma-insert-heap x (node {perfect} {y} {l} {r} y≤*l y≤*r hl hr)
    with tot≤ x y | l | r
... | inj₁ x≤y | leaf | leaf = node (nd≤* x≤y (lf≤* x) (lf≤* x)) (lf≤* x) (node (lf≤* y) (lf≤* y) leaf leaf) leaf
... | inj₁ x≤y | node _ _ _ _ | leaf = node (lemma-insert-≤*' x≤y y≤*l) (lf≤* x) (lemma-insert-heap y hl) hr
... | inj₁ x≤y | leaf | node _ _ _ _ = node (nd≤* x≤y (lf≤* x) (lf≤* x)) (lemma-≤-≤* x≤y y≤*r) (node y≤*l y≤*l hl hl) hr
... | inj₁ x≤y | node _ _ _ _ | node _ _ _ _ = node (lemma-insert-≤*' x≤y y≤*l) (lemma-≤-≤* x≤y y≤*r) (lemma-insert-heap y hl) hr
... | inj₂ y≤x | leaf | leaf = node (nd≤* y≤x (lf≤* y) (lf≤* y)) (lf≤* y) (node (lf≤* x) (lf≤* x) leaf leaf) leaf
... | inj₂ y≤x | node _ _ _ _ | leaf = node (lemma-insert-≤* y≤x y≤*l) y≤*r (lemma-insert-heap x hl) hr
... | inj₂ y≤x | leaf | node _ _ _ _ = node (nd≤* y≤x y≤*l y≤*l) y≤*r (lemma-insert-heap x hl) hr
... | inj₂ y≤x | node _ _ _ _ | node _ _ _ _ = node (lemma-insert-≤* y≤x y≤*l) y≤*r (lemma-insert-heap x hl) hr
lemma-insert-heap x (node {left} {y} {l} {r} y≤*l y≤*r hl hr)
    with tot≤ x y
... | inj₁ x≤y
    with insert y l | lemma-insert-heap y hl | lemma-insert-≤*' x≤y y≤*l | lemma-insert-compound y l
... | node perfect y' l' r' | hlᵢ | x≤*lᵢ | compound = node x≤*lᵢ (lemma-≤-≤* x≤y y≤*r) hlᵢ hr
... | node right y' l' r' | hlᵢ | x≤*lᵢ | compound = node x≤*lᵢ (lemma-≤-≤* x≤y y≤*r) hlᵢ hr
... | node left y' l' r' | hlᵢ | x≤*lᵢ | compound = node x≤*lᵢ (lemma-≤-≤* x≤y y≤*r) hlᵢ hr
lemma-insert-heap x (node {left} {y} {l} {r} y≤*l y≤*r hl hr) | inj₂ y≤x
    with insert x l  | lemma-insert-heap x hl | lemma-insert-≤* y≤x y≤*l | lemma-insert-compound x l
... | node perfect y' l' r' | hlᵢ | y≤*lᵢ | compound = node y≤*lᵢ y≤*r hlᵢ hr
... | node right y' l' r' | hlᵢ | y≤*lᵢ | compound = node y≤*lᵢ y≤*r hlᵢ hr
... | node left y' l' r' | hlᵢ | y≤*lᵢ | compound = node y≤*lᵢ y≤*r hlᵢ hr
lemma-insert-heap x (node {right} {y} {l} {r} y≤*l y≤*r hl hr)
    with tot≤ x y
... | inj₁ x≤y
    with insert y r | lemma-insert-heap y hr | lemma-insert-≤*' x≤y y≤*r | lemma-insert-compound y r
... | node perfect y' l' r' | hrᵢ | x≤*rᵢ | compound = node (lemma-≤-≤* x≤y y≤*l) x≤*rᵢ hl hrᵢ
... | node right y' l' r' | hrᵢ | x≤*rᵢ | compound = node (lemma-≤-≤* x≤y y≤*l) x≤*rᵢ hl hrᵢ
... | node left y' l' r' | hrᵢ | x≤*rᵢ | compound = node (lemma-≤-≤* x≤y y≤*l) x≤*rᵢ hl hrᵢ
lemma-insert-heap x (node {right} {y} {l} {r} y≤*l y≤*r hl hr) | inj₂ y≤x
    with insert x r | lemma-insert-heap x hr | lemma-insert-≤* y≤x y≤*r | lemma-insert-compound x r
... | node perfect y' l' r' | hrᵢ | y≤*rᵢ | compound = node y≤*l y≤*rᵢ hl hrᵢ
... | node right y' l' r' | hrᵢ | y≤*rᵢ | compound = node y≤*l y≤*rᵢ hl hrᵢ
... | node left y' l' r' | hrᵢ | y≤*rᵢ | compound = node y≤*l y≤*rᵢ hl hrᵢ

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

module Cubical.Categories.Yoneda where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence using (ua)
open import Cubical.Foundations.Function renaming (_∘_ to _◍_)
open import Cubical.Data.Sigma
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Functor
open import Cubical.Categories.Presheaf

private
  variable
    ℓ ℓ' ℓ'' : Level

-- THE YONEDA LEMMA

open NatTrans
open NatTransP
open Functor
open Iso

module _ (A B : Type ℓ) (f : A → B) where

  isInj = ∀ (x y : A) → (f x ≡ f y) → x ≡ y
  isSurj = ∀ (b : B) → Σ[ a ∈ A ] f a ≡ b

  bijectionToIso : isInj × isSurj
                 → isIso f
  bijectionToIso (i , s) = (λ b → fst (s b)) , (λ b → snd (s b)) , λ a → i (fst (s (f a))) a (snd (s (f a)))

module _ {C : Precategory ℓ ℓ'} ⦃ isCatC : isCategory C ⦄ where
  open Precategory
  yoneda : (F : Functor C (SET ℓ'))
         → (c : C .ob)
         → Iso ((FUNCTOR C (SET ℓ')) [ C [ c ,-] , F ]) (fst (F ⟅ c ⟆))
  yoneda F c = theIso
    where
      natType = (FUNCTOR C (SET ℓ')) [ C [ c ,-] , F ]
      setType = fst (F ⟅ c ⟆)

      -- takes a natural transformation to what it does on id
      ϕ : natType → setType
      ϕ α = (α ⟦ _ ⟧) (C .id c)

      -- takes an element x of F c and sends it to the (only) natural transformation
      -- which takes the identity to x
      Ψ : setType → natType
      Ψ x .N-ob c = λ f → (F ⟪ f ⟫) x
      Ψ x .N-hom g
        = funExt (λ f → (F ⟪ f ⋆⟨ C ⟩ g ⟫) x
                      ≡[ i ]⟨ (F .F-seq f g) i x ⟩
                        (F ⟪ g ⟫) ((F ⟪ f ⟫) x)
                      ∎)

      theIso : Iso natType setType
      theIso .fun = ϕ
      theIso .inv = Ψ
      theIso .rightInv x i = F .F-id i x
      theIso .leftInv α@(natTrans αo αh) = NatTrans-≡-intro (sym αo≡βo) (symP αh≡βh)
        where
          β = Ψ (ϕ α)
          βo = β .N-ob
          βh = β .N-hom

          -- equivalence of action on objects follows
          -- from simple equational reasoning using naturality
          αo≡βo : αo ≡ βo
          αo≡βo = funExt λ x → funExt λ f
                → αo x f
                ≡[ i ]⟨ αo x (C .⋆IdL f (~ i)) ⟩ -- expand into the bottom left of the naturality diagram
                  αo x (C .id c ⋆⟨ C ⟩ f)
                ≡[ i ]⟨ αh f i (C .id c) ⟩ -- apply naturality
                  (F ⟪ f ⟫) ((αo _) (C .id c))
                ∎

          -- type aliases for natural transformation
          NOType = N-ob-Type (C [ c ,-]) F
          NHType = N-hom-Type (C [ c ,-]) F

          -- equivalence of commutative squares follows from SET being a Category
          αh≡βh : PathP (λ i → NHType (αo≡βo i)) αh βh -- αh βh
          αh≡βh = isPropHomP αh βh αo≡βo
            where
              isProp-hom : ⦃ isCatSET : isCategory (SET ℓ') ⦄ → (ϕ : NOType) → isProp (NHType ϕ)
              isProp-hom ⦃ isCatSET ⦄ γ = isPropImplicitΠ λ x
                                        → isPropImplicitΠ λ y
                                        → isPropΠ λ f
                                        → isCatSET .isSetHom {x = (C [ c , x ]) , (isCatC .isSetHom)} {F ⟅ y ⟆} _ _

              isPropHomP : isOfHLevelDep 1 (λ ηo → NHType ηo)
              isPropHomP = isOfHLevel→isOfHLevelDep 1 λ a → isProp-hom a

  -- Naturality of the bijection

  -- in the functor
  -- it's equivalent to apply ϕ to α then do β ⟦ c ⟧
  -- or apply ϕ the the composite nat trans α ◍ β
  -- where ϕ takes a natural transformation to its representing element
  yonedaIsNaturalInFunctor : ∀ {F G : Functor C (SET ℓ')} (c : C .ob)
                     → (β : F ⇒ G)
                     → (fun (yoneda G c) ◍ compTrans β) ≡ (β ⟦ c ⟧ ◍ fun (yoneda F c))
  yonedaIsNaturalInFunctor {F = F} {G} c β = funExt λ α → refl

  -- in the object
  -- it's equivalent to apply ϕ and then F ⟪ f ⟫
  -- or to apply ϕ to the natural transformation obtained by precomposing with f
  yonedaIsNaturalInOb : ∀ {F : Functor C (SET ℓ')}
                      → (c c' : C .ob)
                      → (f : C [ c , c' ])
                      → yoneda F c' .fun ◍ preComp f ≡ F ⟪ f ⟫ ◍ yoneda F c .fun
  yonedaIsNaturalInOb {F = F} c c' f = funExt (λ α
                             → (yoneda F c' .fun ◍ preComp f) α
                             ≡⟨ refl ⟩
                               (α ⟦ c' ⟧) (f ⋆⟨ C ⟩ C .id c')
                             ≡[ i ]⟨ (α ⟦ c' ⟧) (C .⋆IdR f i) ⟩
                               (α ⟦ c' ⟧) f
                             ≡[ i ]⟨ (α ⟦ c' ⟧) (C .⋆IdL f (~ i)) ⟩
                               (α ⟦ c' ⟧) (C .id c ⋆⟨ C ⟩ f)
                             ≡[ i ]⟨ (α .N-hom f i) (C .id c) ⟩
                               (F ⟪ f ⟫) ((α ⟦ c ⟧) (C .id c))
                             ≡⟨ refl ⟩
                               ((F ⟪ f ⟫) ◍ yoneda F c .fun) α
                             ∎)

-- Yoneda embedding
-- TODO: probably want to rename/refactor
module _ {C : Precategory ℓ ℓ} ⦃ C-cat : isCategory C ⦄ where
  open Functor
  open NatTrans
  open Precategory C

  yo : ob → Functor (C ^op) (SET ℓ)
  yo x .F-ob y .fst = C [ y , x ]
  yo x .F-ob y .snd = C-cat .isSetHom
  yo x .F-hom f g = f ⋆⟨ C ⟩ g
  yo x .F-id i f = ⋆IdL f i
  yo x .F-seq f g i h = ⋆Assoc g f h i

  YO : Functor C (PreShv C ℓ)
  YO .F-ob = yo
  YO .F-hom f .N-ob z g = g ⋆⟨ C ⟩ f
  YO .F-hom f .N-hom g i h = ⋆Assoc g h f i
  YO .F-id = makeNatTransPath λ i _ → λ f → ⋆IdR f i
  YO .F-seq f g = makeNatTransPath λ i _ → λ h → ⋆Assoc h f g (~ i)

  module _ {x} (F : Functor (C ^op) (SET ℓ)) where
    yo-yo-yo : NatTrans (yo x) F → F .F-ob x .fst
    yo-yo-yo α = α .N-ob _ (id _)

    no-no-no : F .F-ob x .fst → NatTrans (yo x) F
    no-no-no a .N-ob y f = F .F-hom f a
    no-no-no a .N-hom f = funExt λ g i → F .F-seq g f i a

    yoIso : Iso (NatTrans (yo x) F) (F .F-ob x .fst)
    yoIso .Iso.fun = yo-yo-yo
    yoIso .Iso.inv = no-no-no
    yoIso .Iso.rightInv b i = F .F-id i b
    yoIso .Iso.leftInv a = makeNatTransPath (funExt λ _ → funExt rem)
      where
        rem : ∀ {z} (x₁ : C [ z , x ]) → F .F-hom x₁ (yo-yo-yo a) ≡ (a .N-ob z) x₁
        rem g =
          F .F-hom g (yo-yo-yo a)
            ≡[ i ]⟨ a .N-hom g (~ i) (id x) ⟩
          a .N-hom g i0 (id x)
            ≡[ i ]⟨ a .N-ob _ (⋆IdR g i) ⟩
          (a .N-ob _) g
            ∎

    yoEquiv : NatTrans (yo x) F ≃ F .F-ob x .fst
    yoEquiv = isoToEquiv yoIso

  isFullYO : isFull YO
  isFullYO x y F[f] = ∣ yo-yo-yo _ F[f] , yoIso {x} (yo y) .Iso.leftInv F[f] ∣

  isFaithfulYO : isFaithful YO
  isFaithfulYO x y f g p i =
    hcomp
      (λ j → λ{ (i = i0) → ⋆IdL f j; (i = i1) → ⋆IdL g j})
      (yo-yo-yo _ (p i))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical