text:
open import Web.Semantic.DL.Role using ( Role )
open import Web.Semantic.DL.Signature using ( Signature ; CN ; RN )

module Web.Semantic.DL.Concept where

infixr 9 ∀[_]_
infixr 8 ∃⟨_⟩_
infixl 7 _⊓_
infixl 6 _⊔_

data Concept (Σ : Signature) : Set where
  ⟨_⟩ : (c : CN Σ) → Concept Σ
  ¬⟨_⟩ : (c : CN Σ) → Concept Σ
  ⊤ : Concept Σ
  ⊥ : Concept Σ
  _⊓_ : (C D : Concept Σ) → Concept Σ
  _⊔_ : (C D : Concept Σ) → Concept Σ
  ∀[_]_ : (R : Role Σ) (C : Concept Σ) → Concept Σ
  ∃⟨_⟩_ : (R : Role Σ) (C : Concept Σ) → Concept Σ
  ≤1 : (R : Role Σ) → Concept Σ
  >1 : (R : Role Σ) → Concept Σ

neg : ∀ {Σ} (C : Concept Σ) → Concept Σ
neg ⟨ c ⟩      = ¬⟨ c ⟩
neg ¬⟨ c ⟩     = ⟨ c ⟩
neg ⊤          = ⊥
neg ⊥          = ⊤
neg (C ⊓ D)    = neg C ⊔ neg D
neg (C ⊔ D)    = neg C ⊓ neg D
neg (∀[ R ] C) = ∃⟨ R ⟩ neg C
neg (∃⟨ R ⟩ C) = ∀[ R ] neg C
neg (≤1 R)     = >1 R
neg (>1 R)     = ≤1 R

ext: agda

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

module HoTT where

open import lib.Basics public
open import lib.types.Types public
open import lib.groups.Groups public
open import lib.cubical.Cubical public
open import lib.NType2 public
open import lib.Equivalences2 public
open import lib.NConnected public

{-
To use coinduction in the form of [∞], [♭] and [♯] you can do:

open import HoTT
open Coinduction

You can also use coinductive records and copatterns instead, that’s prettier
(see experimental/GlobularTypes.agda for an example)
-}
module Coinduction where
  open import lib.Coinduction public

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Intuitionistic propositional calculus.
-- Hilbert-style formalisation of syntax.
-- Sequences of terms.

module IPC.Syntax.HilbertSequential where

open import IPC.Syntax.Common public

-- Derivations.

infix 3 _⊦⊢_
data _⊦⊢_ (Γ : Cx Ty) : Cx Ty → Set where
  nil   : Γ ⊦⊢ ∅
  var   : ∀ {Ξ A}     → A ∈ Γ → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A
  mp    : ∀ {Ξ A B}   → A ▻ B ∈ Ξ → A ∈ Ξ → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , B
  ci    : ∀ {Ξ A}     → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ▻ A
  ck    : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ▻ B ▻ A
  cs    : ∀ {Ξ A B C} → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
  cpair : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ▻ B ▻ A ∧ B
  cfst  : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ∧ B ▻ A
  csnd  : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ∧ B ▻ B
  unit  : ∀ {Ξ}       → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , ⊤
  cboom : ∀ {Ξ C}     → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , ⊥ ▻ C
  cinl  : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ▻ A ∨ B
  cinr  : ∀ {Ξ A B}   → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , B ▻ A ∨ B
  ccase : ∀ {Ξ A B C} → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ , A ∨ B ▻ (A ▻ C) ▻ (B ▻ C) ▻ C

infix 3 _⊢_
_⊢_ : Cx Ty → Ty → Set
Γ ⊢ A = ∃ (λ Ξ → Γ ⊦⊢ Ξ , A)

-- Monotonicity with respect to context inclusion.

mono⊦⊢ : ∀ {Ξ Γ Γ′} → Γ ⊆ Γ′ → Γ ⊦⊢ Ξ → Γ′ ⊦⊢ Ξ
mono⊦⊢ η nil         = nil
mono⊦⊢ η (var i ts)  = var (mono∈ η i) (mono⊦⊢ η ts)
mono⊦⊢ η (mp i j ts) = mp i j (mono⊦⊢ η ts)
mono⊦⊢ η (ci ts)     = ci (mono⊦⊢ η ts)
mono⊦⊢ η (ck ts)     = ck (mono⊦⊢ η ts)
mono⊦⊢ η (cs ts)     = cs (mono⊦⊢ η ts)
mono⊦⊢ η (cpair ts)  = cpair (mono⊦⊢ η ts)
mono⊦⊢ η (cfst ts)   = cfst (mono⊦⊢ η ts)
mono⊦⊢ η (csnd ts)   = csnd (mono⊦⊢ η ts)
mono⊦⊢ η (unit ts)   = unit (mono⊦⊢ η ts)
mono⊦⊢ η (cboom ts)  = cboom (mono⊦⊢ η ts)
mono⊦⊢ η (cinl ts)   = cinl (mono⊦⊢ η ts)
mono⊦⊢ η (cinr ts)   = cinr (mono⊦⊢ η ts)
mono⊦⊢ η (ccase ts)  = ccase (mono⊦⊢ η ts)

mono⊢ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ A → Γ′ ⊢ A
mono⊢ η (Ξ , ts) = Ξ , mono⊦⊢ η ts

-- Concatenation of derivations.

_⧺⊦_ : ∀ {Γ Ξ Ξ′} → Γ ⊦⊢ Ξ → Γ ⊦⊢ Ξ′ → Γ ⊦⊢ Ξ ⧺ Ξ′
us ⧺⊦ nil       = us
us ⧺⊦ var i ts  = var i (us ⧺⊦ ts)
us ⧺⊦ mp i j ts = mp (mono∈ weak⊆⧺₂ i) (mono∈ weak⊆⧺₂ j) (us ⧺⊦ ts)
us ⧺⊦ ci ts     = ci (us ⧺⊦ ts)
us ⧺⊦ ck ts     = ck (us ⧺⊦ ts)
us ⧺⊦ cs ts     = cs (us ⧺⊦ ts)
us ⧺⊦ cpair ts  = cpair (us ⧺⊦ ts)
us ⧺⊦ cfst ts   = cfst (us ⧺⊦ ts)
us ⧺⊦ csnd ts   = csnd (us ⧺⊦ ts)
us ⧺⊦ unit ts   = unit (us ⧺⊦ ts)
us ⧺⊦ cboom ts  = cboom (us ⧺⊦ ts)
us ⧺⊦ cinl ts   = cinl (us ⧺⊦ ts)
us ⧺⊦ cinr ts   = cinr (us ⧺⊦ ts)
us ⧺⊦ ccase ts  = ccase (us ⧺⊦ ts)

-- Modus ponens in expanded form.

app : ∀ {A B Γ} → Γ ⊢ A ▻ B → Γ ⊢ A → Γ ⊢ B
app {A} {B} (Ξ , ts) (Ξ′ , us) = Ξ″ , vs
  where Ξ″ = (Ξ′ , A) ⧺ (Ξ , A ▻ B)
        vs = mp top (mono∈ (weak⊆⧺₁ (Ξ , A ▻ B)) top) (us ⧺⊦ ts)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
import      Lvl
open import Data.Boolean
open import Type

module Data.List.Sorting.Proofs {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

open import Data.Boolean.Proofs
open import Data.Boolean.Stmt
open import Data.Boolean.Stmt.Proofs
open import Data.List
import      Data.List.Functions as List
open import Data.List.Relation.Membership as Membership using (_∈_ ; use ; skip)
open import Data.List.Relation.Permutation
open import Data.List.Sorting(_≤?_)
open import Data.List.Sorting.Functions(_≤?_)
open import Functional hiding (swap)
open import Lang.Inspect
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Relator.Properties

-- If a list is sorted, then its tail is also sorted.
tail-sorted-proof : ∀{l} → Sorted(l) → Sorted(List.tail l)
tail-sorted-proof {.∅}           empty                = empty
tail-sorted-proof {_ ⊰ ∅}        single               = empty
tail-sorted-proof {a ⊰ b ⊰ l}    (step ⦃ ab ⦄ ⦃ sl ⦄) = sl

module _ (asym : ∀{x y} → (x ≤? y ≡ not(y ≤? x))) where
  -- Correctness of the sorted property of insert.
  insert-sorted-proof : ∀{x}{l} → Sorted(l) → Sorted(insert x l)
  insert-sorted-proof {x} {∅} sl = single
  insert-sorted-proof {x} {y ⊰ ∅} single with (x ≤? y) | inspect (x ≤?_) y
  ... | 𝑇 | intro p = step ⦃ [↔]-to-[←] IsTrue.is-𝑇 p ⦄
  ... | 𝐹 | intro p rewrite asym{x}{y} = step ⦃ [↔]-to-[←] IsFalse.is-𝐹 p ⦄ ⦃ single ⦄
  insert-sorted-proof {x} {y ⊰ z ⊰ l} (step ⦃ yz ⦄ ⦃ sl ⦄) with (x ≤? y) | inspect (x ≤?_) y
  ... | 𝑇 | intro p = step ⦃ [↔]-to-[←] IsTrue.is-𝑇 p ⦄ ⦃ step ⦃ yz ⦄ ⦃ sl ⦄ ⦄
  ... | 𝐹 | intro p rewrite asym{x}{y} = if-intro {x = x ⊰ z ⊰ l}{y = z ⊰ insert x l}{P = expr ↦ Sorted(y ⊰ expr)}{B = x ≤? z} (xzt ↦ step ⦃ IsFalse.[¬]-elim([↔]-to-[←] IsFalse.is-𝐹 p) ⦄ ⦃ step ⦃ [↔]-to-[←] IsTrue.is-𝑇 xzt ⦄ ⦃ sl ⦄ ⦄) (xzf ↦ step ⦃ yz ⦄ ⦃ if-elimᵣ {x = x ⊰ z ⊰ l}{y = z ⊰ insert x l}{P = Sorted} (insert-sorted-proof {x} {z ⊰ l} sl) xzf ⦄) where
    private variable ℓ₁ : Lvl.Level
    private variable A : Type{ℓ}
    if-elimᵣ : ∀{b : Bool}{x y : A}{P : A → Type{ℓ₁}} → P(if b then x else y) → (b ≡ 𝐹) → P(y)
    if-elimᵣ x [≡]-intro = x

  -- Correctness of the sorted property of merge.
  merge-sorted-proof : ∀{l₁ l₂} → Sorted(l₁) → Sorted(l₂) → Sorted(merge l₁ l₂)
  merge-sorted-proof {l₁} {∅}          s₁ s₂                   = s₁
  merge-sorted-proof {l₁} {x ⊰ ∅}      s₁ single               = insert-sorted-proof s₁
  merge-sorted-proof {l₁} {x ⊰ y ⊰ l₂} s₁ (step ⦃ xy ⦄ ⦃ s₂ ⦄) = insert-sorted-proof (merge-sorted-proof s₁ s₂)

  mergeAll-sorted-proof : ∀{ls} → (∀{l} → ⦃ _ : (l ∈ ls) ⦄ → Sorted(l)) → Sorted(mergeAll ls)
  mergeAll-sorted-proof {∅}      p = empty
  mergeAll-sorted-proof {l ⊰ ls} p = merge-sorted-proof (p ⦃ use (reflexivity(_≡_)) ⦄) (mergeAll-sorted-proof {ls} (\{l} ⦃ q ⦄ → p{l} ⦃ _∈_.skip q ⦄))

  {-
  split₂-sorted-proof : ∀{l} → Sorted(l) → let (a , b) = List.split₂(l) in (Sorted(a) ∧ Sorted(b))
  split₂-sorted-proof {∅}             empty                                 = (Sorted.empty , Sorted.empty)
  split₂-sorted-proof {x ⊰ ∅}         single                                = (single , Sorted.empty)
  split₂-sorted-proof {x ⊰ y ⊰ ∅}     (step ⦃ p ⦄ ⦃ single ⦄)               = (single , single)
  split₂-sorted-proof {x ⊰ y ⊰ z ⊰ l} (step ⦃ xy ⦄ ⦃ step ⦃ yz ⦄ ⦃ szl ⦄ ⦄) = ({!step ⦃ trans xy yz ⦄ ⦃ prevₗ ⦄!} , {!step ⦃ yz ⦄ ⦃ prevᵣ ⦄!}) where
    prev : let (a , b) = List.split₂(z ⊰ l) in (Sorted(a) ∧ Sorted(b))
    prev = split₂-sorted-proof {z ⊰ l} szl

    prevₗ : Sorted(Tuple.left(List.split₂(z ⊰ l)))
    prevₗ = Tuple.left prev

    prevᵣ : Sorted(Tuple.right(List.split₂(z ⊰ l)))
    prevᵣ = Tuple.right prev
  -}

open import Data using (Unit ; <>)
open import Data.Option
import      Data.Option.Functions as Option
open import Data.Tuple using (_⨯_ ; _,_)
extractMinimal-permutation : ∀{l} → Option.partialMap (∅ permutes l) (\{(x , xs) → (x ⊰ xs) permutes l}) (extractMinimal l)
extractMinimal-permutation {∅} = empty
extractMinimal-permutation {x ⊰ ∅} = prepend empty
extractMinimal-permutation {x ⊰ l@(_ ⊰ _)} with extractMinimal l | extractMinimal-permutation{l}
... | None           | p with () ← Proofs.permutes-empty-not-empty p
... | (Some(y , l₂)) | p with (x ≤? y)
... | 𝑇 = reflexivity(_permutes_)
... | 𝐹 = trans swap (prepend p)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
import cedille-options
open import general-util

module toplevel-state (options : cedille-options.options) {mF : Set → Set} {{_ : monad mF}} where

open import cedille-types
--open import classify options {mF}
open import ctxt
open import constants
open import conversion
open import rename
open import spans options {mF}
open import syntax-util
open import to-string options
open import string-format
open import subst
open import json

import cws-types

record include-elt : Set where
  field ast : maybe ex-file
        ast~ : maybe file
        cwst : maybe cws-types.start
        deps : 𝕃 string -- dependencies
        import-to-dep : trie filepath -- map import strings in the file to their full paths
        ss : spans ⊎ string -- spans in string form (read from disk)
        err : 𝔹 -- is ss reporting an error
        need-to-add-symbols-to-context : 𝔹
        do-type-check : 𝔹
        inv : do-type-check imp need-to-add-symbols-to-context ≡ tt
        last-parse-time : maybe UTC
        cede-up-to-date : 𝔹
        rkt-up-to-date : 𝔹
        source : string

blank-include-elt : include-elt
blank-include-elt = record { ast = nothing ; ast~ = nothing; cwst = nothing; deps = [] ;
                             import-to-dep = empty-trie ; ss = inj₂ "" ; err = ff ; need-to-add-symbols-to-context = tt ;
                             do-type-check = tt ; inv = refl ; last-parse-time = nothing; cede-up-to-date = ff ; rkt-up-to-date = ff ; source = "" }

-- the dependencies should pair import strings found in the file with the full paths to those imported files
new-include-elt : filepath → (dependencies : 𝕃 (string × string)) → (ast : ex-file) →
                  cws-types.start → maybe UTC → include-elt
new-include-elt filename deps x y time =
  record { ast = just x ; ast~ = nothing; cwst = just y ; deps = map snd deps ; import-to-dep = trie-fill empty-trie deps ; ss = inj₂ "" ; err = ff ;
           need-to-add-symbols-to-context = tt ;
           do-type-check = tt ; inv = refl ; last-parse-time = time ; cede-up-to-date = ff ; rkt-up-to-date = ff ; source = "" }

error-include-elt : string → include-elt
error-include-elt err = record blank-include-elt { ss = inj₂ (global-error-string err) ; err = tt }

error-span-include-elt : string → string → posinfo → include-elt
error-span-include-elt err errSpan pos = record blank-include-elt { ss = inj₁ (add-span (span.mk-span err pos (posinfo-plus pos 1) [] (just errSpan) ) empty-spans ) ; err = tt }

set-do-type-check-include-elt : include-elt → 𝔹 → include-elt
set-do-type-check-include-elt ie b =
 record ie { need-to-add-symbols-to-context = (b || include-elt.need-to-add-symbols-to-context ie) ;
             do-type-check = b ;
             inv = lem b }
 where lem : (b : 𝔹) → b imp (b || include-elt.need-to-add-symbols-to-context ie) ≡ tt
       lem tt = refl
       lem ff = refl

set-need-to-add-symbols-to-context-include-elt : include-elt → 𝔹 → include-elt
set-need-to-add-symbols-to-context-include-elt ie b =
 record ie { need-to-add-symbols-to-context = b ;
             do-type-check = b && include-elt.do-type-check ie ;
             inv = lem b }
 where lem : ∀(b : 𝔹){b' : 𝔹} → b && b' imp b ≡ tt
       lem tt {tt} = refl
       lem tt {ff} = refl
       lem ff {tt} = refl
       lem ff {ff} = refl

set-spans-include-elt : include-elt → spans → file → include-elt
set-spans-include-elt ie ss f =
 record ie { ss = inj₁ ss ;
             ast~ = just f ;
             err = spans-have-error ss  }

set-last-parse-time-include-elt : include-elt → UTC → include-elt
set-last-parse-time-include-elt ie time =
  record ie { last-parse-time = just time }

set-cede-file-up-to-date-include-elt : include-elt → 𝔹 → include-elt
set-cede-file-up-to-date-include-elt ie up-to-date = record ie { cede-up-to-date = up-to-date }
set-rkt-file-up-to-date-include-elt : include-elt → 𝔹 → include-elt
set-rkt-file-up-to-date-include-elt ie up-to-date = record ie { rkt-up-to-date = up-to-date }

set-spans-string-include-elt : include-elt → (err : 𝔹) → string → include-elt
set-spans-string-include-elt ie err ss = record ie { ss = inj₂ ss ; err = err  }

set-source-include-elt : include-elt → string → include-elt
set-source-include-elt ie source = record ie { source = source }

record toplevel-state : Set where
  constructor mk-toplevel-state
  field include-path : 𝕃 string × stringset
        files-with-updated-spans : 𝕃 string
        is : trie include-elt {- keeps track of files we have parsed and/or processed -}
        Γ : ctxt
        logFilePath : filepath

new-toplevel-state : (logFilePath : filepath) → (include-path : 𝕃 string × stringset) → toplevel-state
new-toplevel-state logFilePath ip =
  record { include-path = ip ;
           files-with-updated-spans = [] ;
           is = empty-trie ;
           Γ = new-ctxt "[nofile]" "[nomod]" ;
           logFilePath = logFilePath }

get-include-elt-if : toplevel-state → filepath → maybe include-elt
get-include-elt-if s filename = trie-lookup (toplevel-state.is s) filename

-- get an include-elt assuming it will be there
get-include-elt : toplevel-state → filepath → include-elt
get-include-elt s filename with get-include-elt-if s filename
get-include-elt s filename | nothing = blank-include-elt {- should not happen -}
get-include-elt s filename | just ie = ie

set-include-elt : toplevel-state → filepath → include-elt → toplevel-state
set-include-elt s f ie = record s { is = trie-insert (toplevel-state.is s) f ie }

set-include-path : toplevel-state → 𝕃 string × stringset → toplevel-state
set-include-path s ip = record s { include-path = ip }

get-do-type-check : toplevel-state → string → 𝔹
get-do-type-check s filename = include-elt.do-type-check (get-include-elt s filename)

include-elt-spans-to-json : include-elt → json
include-elt-spans-to-json ie with (include-elt.ss ie)
include-elt-spans-to-json ie | inj₁ ss = spans-to-json ss
include-elt-spans-to-json ie | inj₂ ss = json-raw [[ ss ]]

include-elt-to-archive : include-elt → json
include-elt-to-archive ie with (include-elt.ss ie) | (include-elt.source ie)
include-elt-to-archive ie | inj₁ ss | source = json-object $ ("source" , json-string source) :: spans-to-json' ss
include-elt-to-archive ie | inj₂ ss | source = json-object $ ("source" , json-string source) :: [ "spans" , json-raw [[ ss ]] ]

include-elt-to-string : include-elt → string
include-elt-to-string ie =
    " deps:  " ^ (𝕃-to-string (λ x → x) "," (include-elt.deps ie)) ^
    -- ast
    ", ast:  " ^ maybe-else "not parsed" (λ ast → "parsed") (include-elt.ast ie) ^ ", " ^
    " import-to-dep:  " ^ (trie-to-string "," (format "filename: %s") (include-elt.import-to-dep ie)) ^
    -- spans
    " err:  " ^ (𝔹-to-string (include-elt.err ie)) ^
    ", need-to-add-symbols-to-context:  " ^ (𝔹-to-string (include-elt.need-to-add-symbols-to-context ie)) ^
    ", do-type-check:  " ^ (𝔹-to-string (include-elt.do-type-check ie)) ^
    ", last-parse-time: " ^ (maybe-else "" utcToString (include-elt.last-parse-time ie))

params-to-string''' : params → string
params-to-string''' [] = ""
-- TODO print erased vs non-erased?
params-to-string''' (Param me v tk :: pms) = "{var: " ^ v ^ ", tk: " ^ rope-to-string (tpkd-to-string empty-ctxt tk) ^ "}" ^ ", " ^ (params-to-string''' pms)

defParams-to-string : defParams → string
defParams-to-string (just pms) = params-to-string''' pms
defParams-to-string nothing = ""

-- TODO also print modname?
syms-to-string : trie (string × 𝕃 string) → string
syms-to-string = trie-to-string ", " (λ l → "{" ^ (𝕃-to-string (λ s → s) ", " (snd l)) ^ "}")

ctxt-info-to-string : ctxt-info → string
ctxt-info-to-string (term-decl tp) = "term-decl: {type: " ^ rope-to-string (to-string empty-ctxt tp) ^ "}"
ctxt-info-to-string (term-def dp opac t tp) = "term-def: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", maybe term: " ^ maybe-else' t "nothing" (λ t → "just " ^ rope-to-string (to-string empty-ctxt t)) ^ ", type: " ^ rope-to-string (to-string empty-ctxt tp) ^ "}"
ctxt-info-to-string (term-udef dp opac t) = "term-udef: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", term: " ^ rope-to-string (to-string empty-ctxt t) ^ "}"
ctxt-info-to-string (type-decl k) = "type-decl: {kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (type-def dp opac tp k) = "type-def: {defParams: {" ^ (defParams-to-string dp) ^ "}, opacity: " ^ (opacity-to-string opac) ^ ", maybe type: " ^ maybe-else' tp "nothing" (λ tp → "just " ^ rope-to-string (to-string empty-ctxt tp)) ^ ", kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (kind-def pms k) = "kind-def: {pms: " ^ (params-to-string''' pms) ^ "kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"
ctxt-info-to-string (rename-def v) = "rename-def: {var: " ^ v ^ "}"
ctxt-info-to-string (var-decl) = "var-decl"
ctxt-info-to-string (ctr-def _ _ _ _ _) = "ctr-def"
--ctxt-info-to-string (mu-def x) = "mu-def: {var: " ^ x ^ "}"
--ctxt-info-to-string (datatype-def ps kᵢ k cs) = "datatype-def: {defParams: {" ^ defParams-to-string ps ^ "}, inductive hypothesis kind: " ^ rope-to-string (to-string empty-ctxt kᵢ) ^ ", kind: " ^ rope-to-string (to-string empty-ctxt k) ^ ", cs: " ^ "TODO" ^ "}"
--ctxt-info-to-string (mu-def ps x k) = "mu-def: {defParams: {" ^ defParams-to-string ps ^ "}, datatype var: " ^ x ^ ", kind: " ^ rope-to-string (to-string empty-ctxt k) ^ "}"

sym-info-to-string : sym-info → string
sym-info-to-string (ci , (fn , pi)) = "{ctxt-info: " ^ (ctxt-info-to-string ci) ^ ", location: {filename: " ^ fn ^ ", posinfo: " ^ pi ^ "}}"

sym-infos-to-string : trie sym-info → string
sym-infos-to-string = trie-to-string ", " sym-info-to-string

occ-to-string : var × posinfo × string → string
occ-to-string (v , pi , s) = "var: " ^ v ^ ", posinfo: " ^ pi ^ ", string: " ^ s

sym-occs-to-string : trie (𝕃 (var × posinfo × string)) → string
sym-occs-to-string = trie-to-string ", " (λ l → "{" ^ (𝕃-to-string occ-to-string ", " l) ^ "}")

qualif-to-string : qualif-info → string
qualif-to-string (x , as) = x ^ rope-to-string (doc-to-rope $ fst (args-to-string as {TERM} NIL 0 [] (new-ctxt "" "") nothing neither)) where open import pretty

mod-info-to-string : (string × string × params × qualif) → string
mod-info-to-string (fn , mn , pms , q) = "filename: " ^ fn ^ ", modname: " ^ mn ^ ", pms: {" ^ (params-to-string''' pms) ^ "}" ^ ", qualif: {" ^ (trie-to-string ", " qualif-to-string q) ^ "}"

ctxt-to-string : ctxt → string
ctxt-to-string (mk-ctxt fn mn ps qual syms mod-map _ _ _ is _ _ _ _ _ _) = "mod-info: {" ^ (mod-info-to-string (fn , mn , ps , qual)) ^ "}, syms: {" ^ (syms-to-string syms) ^ "}, i: {" ^ (sym-infos-to-string is) ^ "}"

toplevel-state-to-string : toplevel-state → string
toplevel-state-to-string (mk-toplevel-state include-path files is context logFilePath) =
    "\ninclude-path: {\n" ^ (𝕃-to-string (λ x → x) "\n" (fst include-path)) ^
    "\n}\nis: {" ^ (trie-to-string "\n" include-elt-to-string is) ^
    "\n}\nΓ: {" ^ (ctxt-to-string context) ^
    "\n}\nlogFilePath : {" ^ logFilePath ^ "\n}"

-- check if a variable is being redefined, and if so return the first given state; otherwise the second (in the monad)
check-redefined : ∀ {X} → posinfo → var → toplevel-state → X → spanM toplevel-state → spanM (toplevel-state × X)
check-redefined pi v s x c =
  let Γ = toplevel-state.Γ s in
  if ctxt-binds-var Γ v then
    ([- redefined-var-span Γ pi v -] return2 s x)
  else (c >>= λ s → return2 s x)

import-as-x : var → maybe var → var
import-as-x v nothing = v
import-as-x v (just pfx) = pfx # v

error-in-import-string = "There is an error in the imported file"

-- Traverse all imports, returning an error if we encounter the same file twice
{-# TERMINATING #-}
check-cyclic-imports : (original current : filepath) → stringset → (path : 𝕃 string) → toplevel-state → err-m
check-cyclic-imports fnₒ fn fs path s with stringset-contains fs fn
...| ff = foldr (λ fnᵢ x → x ||-maybe check-cyclic-imports fnₒ fnᵢ (stringset-insert fs fn) (fn :: path) s)
            nothing (include-elt.deps (get-include-elt s fn))
...| tt with fnₒ =string fn
...| tt = just (foldr (λ fnᵢ x → x ^ " → " ^ fnᵢ) ("Cyclic dependencies (" ^ fn) path ^ " → " ^ fn ^ ")")
...| ff = just error-in-import-string

scope-t : Set → Set
scope-t X = filepath → string → maybe var → params → args → X → toplevel-state → toplevel-state × err-m

infixl 0 _>>=scope_
_>>=scope_ : toplevel-state × err-m → (toplevel-state → toplevel-state × err-m) → toplevel-state × err-m
_>>=scope_ (ts , err) f with f ts
...| ts' , err' = ts' , err ||-maybe err'

{-# TERMINATING #-}
scope-file : toplevel-state → (original imported : filepath) → maybe var → args → toplevel-state × err-m
scope-file' : scope-t ⊤
scope-cmds : scope-t cmds
scope-cmd : scope-t cmd
scope-var : scope-t var
scope-ctrs : scope-t ctrs
scope-datatype-names : scope-t var
scope-enc-defs : scope-t encoding-defs

scope-file ts fnₒ fnᵢ oa as with check-cyclic-imports fnₒ fnᵢ (trie-single fnₒ triv) [] ts
...| just e = ts , just e
...| nothing = scope-file' fnₒ fnᵢ oa [] as triv ts

scope-file' fnₒ fn oa psₒ as triv s with get-include-elt s fn
...| ie with include-elt.err ie | include-elt.ast~ ie
...| e | nothing = s , when e error-in-import-string
...| e | just (Module mn ps cs) =
  (s , when e error-in-import-string) >>=scope
  scope-cmds fn mn oa ps as cs

scope-cmds fn mn oa ps as (c :: cs) s =
  scope-cmd fn mn oa ps as c s >>=scope scope-cmds fn mn oa ps as cs
scope-cmds fn mn oa ps as [] s = s , nothing

scope-cmd fn mn oa ps as (CmdImport (Import Private ifn mn' oa' as')) s = s , nothing
scope-cmd fn mn oa psₒ asₒ (CmdImport (Import Public ifn mn' oa' asᵢ')) s =
  scope-file' fn ifn oa psₒ asᵢ triv s
  -- ^ oa' should be NoOptAs, so we can use oa ^
  where

  merged : trie (maybe arg) → params → args → trie (maybe arg)
  merged σ (Param me x tk :: ps) (a :: as) =
    merged (trie-insert σ x $ just a) ps as
  merged σ (Param me x tk :: ps) [] =
    merged (trie-insert σ x nothing) ps []
  merged σ _ _ = σ

  arg-var : arg → maybe var
  arg-var (Arg (Var x)) = just x
  arg-var (ArgE (Ttm (Var x))) = just x
  arg-var (ArgE (Ttp (TpVar x))) = just x
  arg-var _ = nothing

  σ = merged empty-trie psₒ asₒ

  reorder : args → args
  reorder (a :: as) =
    maybe-else' (arg-var a >>= trie-lookup σ) (a :: reorder as) λ ma →
    maybe-else' ma [] λ a → a :: reorder as
  reorder [] = []

  asᵢ = reorder asᵢ'

scope-cmd fn mn oa ps as (CmdDefKind v _ _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (CmdDefTerm v   _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (CmdDefType v _ _) = scope-var fn mn oa ps as v
scope-cmd fn mn oa ps as (CmdDefData eds v _ _ cs) s =
  scope-var fn mn oa ps as v s >>=scope
  scope-ctrs fn mn oa ps as cs >>=scope
  scope-enc-defs fn mn oa ps as eds >>=scope
  scope-datatype-names fn mn oa ps as v

scope-ctrs fn mn oa ps as [] s = s , nothing
scope-ctrs fn mn oa ps as (Ctr x T :: ds) s =
  scope-var fn mn oa ps as x s >>=scope
  scope-ctrs fn mn oa ps as ds

scope-datatype-names fn mn oa ps as x s =
  scope-var fn mn oa ps as (data-Is/ x) s >>=scope
  scope-var fn mn oa ps as (data-is/ x) >>=scope
  scope-var fn mn oa ps as (data-to/ x)

scope-enc-defs fn mn oa ps as eds s =
  record s { Γ = record (toplevel-state.Γ s) { μᵤ = just eds } } , nothing

scope-var fn mn oa ps as ignored-var s = s , nothing
scope-var _ mn oa ps as v s with import-as-x v oa | s
...| v' | mk-toplevel-state ip fns is Γ logFilePath =
  mk-toplevel-state ip fns is
    (record Γ { qual = trie-insert (ctxt.qual Γ) v' (mn # v , as) }) logFilePath ,
  flip maybe-map (trie-lookup (ctxt.qual Γ) v') (uncurry λ v'' as' →
    "Multiple definitions of variable " ^ v' ^ " as " ^ v'' ^ " and " ^ (mn # v) ^
    (if (mn # v =string v'') then " (perhaps it was already imported?)" else ""))


text:
module Issue4408b where

open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Agda.Primitive

id : ∀ {a} {A : Set a} → A → A
id x = x

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

infix 0 _↔_

record _↔_ {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
  field
    to               : From → To
    from             : To → From
    right-inverse-of : ∀ x → to (from x) ≡ x
    left-inverse-of  : ∀ x → from (to x) ≡ x

infixr 1 _⊎_

data _⊎_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

[_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

Σ-map : ∀ {a b p q}
          {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
        (f : A → B) → (∀ {x} → P x → Q (f x)) →
        Σ A P → Σ B Q
Σ-map f g = λ p → (f (fst p) , g (snd p))

∃-⊎-distrib-right :
  ∀ {a b c} {A : Set a} {B : Set b} {C : A ⊎ B → Set c} →
  Σ (A ⊎ B) C ↔ Σ A (C ∘ inj₁) ⊎ Σ B (C ∘ inj₂)
∃-⊎-distrib-right {A = A} {B} {C} = record
  { to               = to
  ; from             = from
  ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
  ; left-inverse-of  = from∘to
  }
  where
  to : Σ (A ⊎ B) C → Σ A (C ∘ inj₁) ⊎ Σ B (C ∘ inj₂)
  to (inj₁ x , y) = inj₁ (x , y)
  to (inj₂ x , y) = inj₂ (x , y)

  from = [ Σ-map inj₁ id , Σ-map inj₂ id ]

  from∘to : ∀ p → from (to p) ≡ p
  from∘to (inj₁ x , y) = refl
  from∘to (inj₂ x , y) = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


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

open import HoTT.Base renaming (_+_ to _⊎_)
open import HoTT.Identity

private variable n m : ℕ

_+_ : ℕ → ℕ → ℕ
0 + m = m
succ n + m = succ (n + m)

+-comm : (n m : ℕ) → n + m == m + n
+-comm zero zero = refl
+-comm zero (succ m) = ap succ (+-comm zero m)
+-comm (succ n) zero = ap succ (+-comm n zero)
+-comm (succ n) (succ m) = ap succ $
  n + succ m   =⟨ +-comm n (succ m) ⟩
  succ m + n   =⟨ ap (succ) (+-comm m n) ⟩
  succ (n + m) =⟨ +-comm (succ n) m ⟩
  m + succ n   ∎
  where open =-Reasoning

_≤_ : ℕ → ℕ → 𝒰₀
n ≤ m = Σ ℕ λ k → n + k == m

≤succ : n ≤ m → n ≤ succ m
≤succ {n} (k , p) = succ k , +-comm n (succ k) ∙ ap succ (+-comm k n ∙ p)

_<_ : ℕ → ℕ → 𝒰₀
n < m = succ n ≤ m

_<=>_ : (n m : ℕ) → (n == m) ⊎ (n < m) ⊎ (m < n)
zero <=> zero = inl refl
zero <=> succ m = inr (inl (m , refl))
succ n <=> zero = inr (inr (n , refl))
succ n <=> succ m with n <=> m
... | inl p = inl (ap succ p)
... | inr (inl (k , p)) = inr (inl (k , ap succ p))
... | inr (inr (k , p)) = inr (inr (k , ap succ p))

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homomorphism proofs for addition over polynomials
------------------------------------------------------------------------

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

open import Tactic.RingSolver.Core.Polynomial.Parameters

module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
  {r₁ r₂ r₃ r₄}
  (homo : Homomorphism r₁ r₂ r₃ r₄)
  where

open import Data.Nat            as ℕ  using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
open import Data.Nat.Properties as ℕₚ using (≤′-trans)
open import Data.Product              using (_,_; _×_; proj₂)
open import Data.List                 using (_∷_; [])
open import Data.List.Kleene
open import Data.Vec                  using (Vec)
open import Function
open import Relation.Unary

import Relation.Binary.PropositionalEquality as ≡

open Homomorphism homo hiding (_^_)
open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
open import Tactic.RingSolver.Core.Polynomial.Base from
open import Tactic.RingSolver.Core.Polynomial.Reasoning to
open import Tactic.RingSolver.Core.Polynomial.Semantics homo
open import Algebra.Operations.Ring rawRing

mutual
  ⊞-hom : ∀ {n} (xs ys : Poly n) →
          ∀ ρ → ⟦ xs ⊞ ys ⟧ ρ ≈ ⟦ xs ⟧ ρ + ⟦ ys ⟧ ρ
  ⊞-hom (xs ⊐ i≤n) (ys ⊐ j≤n) = ⊞-match-hom (inj-compare i≤n j≤n) xs ys

  ⊞-match-hom : ∀ {i j n} {i≤n : i ≤′ n} {j≤n : j ≤′ n}
                (i-cmp-j : InjectionOrdering i≤n j≤n)
                (xs : FlatPoly i) (ys : FlatPoly j) →
                ∀ ρ → ⟦ ⊞-match i-cmp-j xs ys ⟧ ρ ≈ ⟦ xs ⊐ i≤n ⟧ ρ + ⟦ ys ⊐ j≤n ⟧ ρ
  ⊞-match-hom (inj-eq ij≤n) (Κ x) (Κ y) Ρ = +-homo x y
  ⊞-match-hom (inj-eq ij≤n) (⅀ (x Δ i & xs)) (⅀ (y Δ j & ys)) Ρ =
    begin
      ⟦ ⊞-zip (compare i j) x xs y ys ⊐↓ ij≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-zip (compare i j) x xs y ys) ij≤n Ρ ⟩
      ⅀?⟦ ⊞-zip (compare i j) x xs y ys ⟧ (drop-1 ij≤n Ρ)
    ≈⟨ ⊞-zip-hom (compare i j) x xs y ys (drop-1 ij≤n Ρ) ⟩
      ⅀⟦ x Δ i & xs ⟧ (drop-1 ij≤n Ρ) + ⅀⟦ y Δ j & ys ⟧ (drop-1 ij≤n Ρ)
    ∎
  ⊞-match-hom (inj-gt i≤n j≤i-1) (⅀ xs) ys Ρ =
    let (ρ , Ρ′) = drop-1 i≤n Ρ
    in
    begin
      ⟦ ⊞-inj j≤i-1 ys xs ⊐↓ i≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-inj j≤i-1 ys xs) i≤n Ρ ⟩
      ⅀?⟦ ⊞-inj j≤i-1 ys xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ ⊞-inj-hom j≤i-1 ys xs ρ Ρ′ ⟩
      ⟦ ys ⊐ j≤i-1 ⟧ (proj₂ (drop-1 i≤n Ρ)) + ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ ≪+ trans-join-hom j≤i-1 i≤n ys Ρ ⟩
      ⟦ ys ⊐ (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) ⟧ Ρ + ⅀⟦ xs ⟧ (drop-1 i≤n Ρ)
    ≈⟨ +-comm _ _ ⟩
      ⅀⟦ xs ⟧ (drop-1 i≤n Ρ) + ⟦ ys ⊐ (≤′-step j≤i-1 ⟨ ≤′-trans ⟩ i≤n) ⟧ Ρ
    ∎
  ⊞-match-hom (inj-lt i≤j-1 j≤n) xs (⅀ ys) Ρ =
    let (ρ , Ρ′) = drop-1 j≤n Ρ
    in
    begin
      ⟦ ⊞-inj i≤j-1 xs ys ⊐↓ j≤n ⟧ Ρ
    ≈⟨ ⊐↓-hom (⊞-inj i≤j-1 xs ys) j≤n Ρ ⟩
      ⅀?⟦ ⊞-inj i≤j-1 xs ys ⟧ (drop-1 j≤n Ρ)
    ≈⟨ ⊞-inj-hom i≤j-1 xs ys ρ Ρ′ ⟩
      ⟦ xs ⊐ i≤j-1 ⟧ (proj₂ (drop-1 j≤n Ρ)) + ⅀⟦ ys ⟧ (drop-1 j≤n Ρ)
    ≈⟨ ≪+ trans-join-hom i≤j-1 j≤n xs Ρ ⟩
      ⟦ xs ⊐ (≤′-step i≤j-1 ⟨ ≤′-trans ⟩ j≤n) ⟧ Ρ + ⅀⟦ ys ⟧ (drop-1 j≤n Ρ)
    ∎

  ⊞-inj-hom : ∀ {i k}
            → (i≤k : i ≤′ k)
            → (x : FlatPoly i)
            → (ys : Coeff k +)
            → (ρ : Carrier)
            → (Ρ : Vec Carrier k)
            → ⅀?⟦ ⊞-inj i≤k x ys ⟧ (ρ , Ρ) ≈ ⟦ x ⊐ i≤k ⟧ Ρ + ⅀⟦ ys ⟧ (ρ , Ρ)
  ⊞-inj-hom i≤k xs (y ⊐ j≤k ≠0 Δ 0 & []) ρ Ρ =
    begin
      ⅀?⟦ ⊞-match (inj-compare j≤k i≤k) y xs Δ 0 ∷↓ [] ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 ((⊞-match (inj-compare j≤k i≤k) y xs)) [] ρ Ρ ⟩
      ⟦ ⊞-match (inj-compare j≤k i≤k) y xs ⟧ Ρ
    ≈⟨ ⊞-match-hom (inj-compare j≤k i≤k) y xs Ρ ⟩
      (⟦ y ⊐ j≤k ⟧ Ρ + ⟦ xs ⊐ i≤k ⟧ Ρ)
    ≈⟨ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ( ⟦ y ⊐ j≤k ⟧ Ρ)
    ∎
  ⊞-inj-hom i≤k xs (y ⊐ j≤k ≠0 Δ 0 & (∹ ys )) ρ Ρ =
    begin
      ⅀?⟦ ⊞-match (inj-compare j≤k i≤k) y xs Δ 0 ∷↓ (∹ ys ) ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 ((⊞-match (inj-compare j≤k i≤k) y xs)) (∹ ys ) ρ Ρ ⟩
      ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ ⊞-match (inj-compare j≤k i≤k) y xs ⟧ Ρ
    ≈⟨ +≫ ⊞-match-hom (inj-compare j≤k i≤k) y xs Ρ ⟩
      ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + (⟦ y ⊐ j≤k ⟧ Ρ + ⟦ xs ⊐ i≤k ⟧ Ρ)
    ≈⟨ sym (+-assoc _ _ _) ⟨ trans ⟩ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + (ρ * ⅀⟦ ys ⟧ (ρ , Ρ) + ⟦ y ⊐ j≤k ⟧ Ρ)
    ∎
  ⊞-inj-hom i≤k xs (y Δ suc j & ys) ρ Ρ =
    begin
      ⅀?⟦ ⊞-inj i≤k xs (y Δ suc j & ys) ⟧ (ρ , Ρ)
    ≡⟨⟩
      ⅀?⟦ xs ⊐ i≤k Δ 0 ∷↓ (∹ y Δ j & ys ) ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom-0 (xs ⊐ i≤k) (∹ y Δ j & ys ) ρ Ρ ⟩
      ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ) + ⟦ xs ⊐ i≤k ⟧ Ρ
    ≈⟨ +-comm _ _ ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ)
    ≈⟨ +≫ (
        begin
          ρ * ⅀⟦ y Δ j & ys ⟧ (ρ , Ρ)
        ≡⟨⟩
          ρ * (((poly y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j)
        ≈⟨ *≫ pow-opt _ ρ j ⟩
          ρ * (ρ ^ j * ((poly y , ys) ⟦∷⟧ (ρ , Ρ)))
        ≈⟨ sym (*-assoc ρ _ _) ⟩
          ρ * ρ ^ j * ((poly y , ys) ⟦∷⟧ (ρ , Ρ))
        ≈⟨ ≪* sym (pow-suc ρ j) ⟩
          ⅀⟦ y Δ suc j & ys ⟧ (ρ , Ρ)
        ∎) ⟩
      ⟦ xs ⊐ i≤k ⟧ Ρ + ⅀⟦ y Δ suc j & ys ⟧ (ρ , Ρ)
    ∎

  ⊞-coeffs-hom : ∀ {n} (xs : Coeff n *) (ys : Coeff n *) →
                 ∀ ρ → ⅀?⟦ ⊞-coeffs xs ys ⟧ ρ ≈ ⅀?⟦ xs ⟧ ρ + ⅀?⟦ ys ⟧ ρ
  ⊞-coeffs-hom [] ys Ρ         = sym (+-identityˡ (⅀?⟦ ys ⟧ Ρ))
  ⊞-coeffs-hom (∹ x Δ i & xs ) = ⊞-zip-r-hom i x xs

  ⊞-zip-hom : ∀ {n i j}
           → (c : ℕ.Ordering i j)
           → (x : NonZero n)
           → (xs : Coeff n *)
           → (y : NonZero n)
           → (ys : Coeff n *)
           → ∀ ρ → ⅀?⟦ ⊞-zip c x xs y ys ⟧ ρ ≈ ⅀⟦ x Δ i & xs ⟧ ρ + ⅀⟦ y Δ j & ys ⟧ ρ
  ⊞-zip-hom (ℕ.equal i) (x ≠0) xs (y ≠0) ys (ρ , Ρ) =
    let x′  = ⟦ x ⟧ Ρ
        y′  = ⟦ y ⟧ Ρ
        xs′ = ⅀?⟦ xs ⟧ (ρ , Ρ)
        ys′ = ⅀?⟦ ys ⟧ (ρ , Ρ)
    in
    begin
      ⅀?⟦ x ⊞ y Δ i ∷↓ ⊞-coeffs xs ys ⟧ (ρ , Ρ)
    ≈⟨ ∷↓-hom (x ⊞ y) i (⊞-coeffs xs ys) ρ Ρ ⟩
      ρ ^ i * (((x ⊞ y) , (⊞-coeffs xs ys)) ⟦∷⟧ (ρ , Ρ))
    ≈⟨ *≫ ⟦∷⟧-hom (x ⊞ y) (⊞-coeffs xs ys) ρ Ρ ⟩
      ρ ^ i * (ρ * ⅀?⟦ ⊞-coeffs xs ys ⟧ (ρ , Ρ) + ⟦ x ⊞ y ⟧ Ρ)
    ≈⟨ *≫ begin
           ρ * ⅀?⟦ ⊞-coeffs xs ys ⟧ (ρ , Ρ) + ⟦ x ⊞ y ⟧ Ρ
          ≈⟨ (*≫ ⊞-coeffs-hom xs ys (ρ , Ρ)) ⟨ +-cong ⟩ ⊞-hom x y Ρ  ⟩
            ρ * (xs′ + ys′) + (x′ + y′)
          ≈⟨ ≪+ distribˡ ρ xs′ ys′ ⟩
            ρ * xs′ + ρ * ys′ + (x′ + y′)
          ≈⟨ +-assoc _ _ _ ⟨ trans ⟩ (+≫ (sym (+-assoc _ _ _) ⟨ trans ⟩ (≪+ +-comm _ _))) ⟩
            ρ * xs′ + (x′ + ρ * ys′ + y′)
          ≈⟨ (+≫ +-assoc _ _ _) ⟨ trans ⟩ sym (+-assoc _ _ _) ⟩
            (ρ * xs′ + x′) + (ρ * ys′ + y′)
          ∎ ⟩
     ρ ^ i * ((ρ * xs′ + x′) + (ρ * ys′ + y′))
    ≈⟨ distribˡ (ρ ^ i) _ _ ⟩
      ρ ^ i * (ρ * xs′ + x′) + ρ ^ i * (ρ * ys′ + y′)
    ≈⟨ sym (pow-opt _ ρ i ⟨ +-cong ⟩ pow-opt _ ρ i) ⟩
      (ρ * xs′ + x′) *⟨ ρ ⟩^ i + (ρ * ys′ + y′) *⟨ ρ ⟩^ i
    ≈⟨ pow-mul-cong (sym (⟦∷⟧-hom x xs ρ Ρ)) ρ i ⟨ +-cong ⟩ pow-mul-cong (sym (⟦∷⟧-hom y ys ρ Ρ)) ρ i ⟩
      ((x , xs) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ i + ((y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ i
    ∎
  ⊞-zip-hom (ℕ.less i k) x xs y ys (ρ , Ρ) = ⊞-zip-r-step-hom i k y ys x xs (ρ , Ρ) ⊙ +-comm _ _
  ⊞-zip-hom (ℕ.greater j k) = ⊞-zip-r-step-hom j k

  ⊞-zip-r-step-hom : ∀ {n} j k
                  → (x : NonZero n)
                  → (xs : Coeff n *)
                  → (y : NonZero n)
                  → (ys : Coeff n *)
                  → ∀ ρ → ⅀⟦ y Δ j & ⊞-zip-r x k xs ys ⟧ ρ ≈ ⅀⟦ x Δ suc (j ℕ.+ k) & xs ⟧ ρ + ⅀⟦ y Δ j & ys ⟧ ρ
  ⊞-zip-r-step-hom j k x xs y ys (ρ , Ρ) =
    let x′  = ⟦ NonZero.poly x ⟧ Ρ
        y′  = ⟦ NonZero.poly y ⟧ Ρ
        xs′ = ⅀?⟦ xs ⟧ (ρ , Ρ)
        ys′ = ⅀?⟦ ys ⟧ (ρ , Ρ)
    in
    begin
      ((poly y , ⊞-zip-r x k xs ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
    ≈⟨ pow-mul-cong (⟦∷⟧-hom (poly y) (⊞-zip-r x k xs ys) ρ Ρ) ρ j ⟩
      (ρ * ⅀?⟦ ⊞-zip-r x k xs ys ⟧ (ρ , Ρ) + y′) *⟨ ρ ⟩^ j
    ≈⟨ pow-opt _ ρ j ⟩
      ρ ^ j * (ρ * ⅀?⟦ ⊞-zip-r x k xs ys ⟧ (ρ , Ρ) + y′)
    ≈⟨ *≫ ≪+ *≫ (⊞-zip-r-hom k x xs ys (ρ , Ρ) ⟨ trans ⟩ (≪+ pow-mul-cong (⟦∷⟧-hom (poly x) xs ρ Ρ) ρ k)) ⟩
      ρ ^ j * (ρ * ((ρ * xs′ + x′) *⟨ ρ ⟩^ k + ys′) + y′)
    ≈⟨ *≫ ≪+ distribˡ ρ _ _ ⟩
      ρ ^ j * ((ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k + ρ * ys′) + y′)
    ≈⟨ *≫ +-assoc _ _ _ ⟩
      ρ ^ j * (ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k + (ρ * ys′ + y′))
    ≈⟨ distribˡ _ _ _ ⟩
      ρ ^ j * (ρ * (ρ * xs′ + x′) *⟨ ρ ⟩^ k) + ρ ^ j * (ρ * ys′ + y′)
    ≈⟨ sym (pow-opt _ ρ j) ⟨ flip +-cong ⟩
         (begin
            ρ ^ j * (ρ * ((ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ k))
          ≈⟨ (sym (*-assoc _ _ _) ⟨ trans ⟩ (≪* sym (pow-sucʳ ρ j))) ⟩
            ρ ^ suc j * ((ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ k)
          ≈⟨ pow-add _ _ k j ⟩
            (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ (k ℕ.+ suc j)
            ≡⟨ ≡.cong (λ i → (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ i) (ℕₚ.+-comm k (suc j)) ⟩
            (ρ * ⅀?⟦ xs ⟧ (ρ , Ρ) + ⟦ poly x ⟧ Ρ) *⟨ ρ ⟩^ (suc j ℕ.+ k)
          ∎)
    ⟩
      (ρ * xs′ + x′) *⟨ ρ ⟩^ suc (j ℕ.+ k) + (ρ * ys′ + y′) *⟨ ρ ⟩^ j
    ≈⟨ pow-mul-cong (sym (⟦∷⟧-hom (poly x) xs ρ Ρ)) ρ (suc (j ℕ.+ k)) ⟨ +-cong ⟩ pow-mul-cong (sym (⟦∷⟧-hom (poly y) ys ρ Ρ)) ρ j ⟩
      ((poly x , xs) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ suc (j ℕ.+ k) + ((poly y , ys) ⟦∷⟧ (ρ , Ρ)) *⟨ ρ ⟩^ j
    ∎

  ⊞-zip-r-hom : ∀ {n} i
             → (x : NonZero n)
             → (xs ys : Coeff n *)
             → (Ρ : Carrier × Vec Carrier n)
             → ⅀?⟦ ⊞-zip-r x i xs ys ⟧ (Ρ) ≈ ⅀⟦ x Δ i & xs ⟧ ( Ρ) + ⅀?⟦ ys ⟧ ( Ρ)
  ⊞-zip-r-hom i x xs []                (ρ , Ρ) = sym (+-identityʳ _)
  ⊞-zip-r-hom i x xs (∹ (y Δ j) & ys )         = ⊞-zip-hom (compare i j) x xs y ys


text:
module List.Properties (A : Set) where

open import Data.List
open import Relation.Binary.PropositionalEquality

++id : (xs : List A) → xs ++ [] ≡ xs
++id [] = refl
++id (x ∷ xs) = cong (_∷_ x) (++id xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Lift where

open import Level
open import Function using () renaming (_∘_ to _∙_)

open import Categories.Category using (Category; module Category)
open import Categories.Functor using (Functor; module Functor)
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)

private
  Lifted₂ : ∀ ℓ {a} {a′} {A : Set a} {b} → (A → A → Set b) → (Lift {a} a′ A) → (Lift {a} a′ A) → Set (b ⊔ ℓ)
  Lifted₂ ℓ f x y = Lift  ℓ  (f (lower x) (lower y))

  lifted₂ : ∀ {a a′ b b′} {A A′ : Set a} {B : Set b} → (A → A′ → B) → Lift  a′ A → Lift  a′ A′ → Lift  b′ B
  lifted₂ f x y = lift (f (lower x) (lower y))

LiftC : ∀ {o ℓ e} o′ ℓ′ e′ → Category o ℓ e → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
LiftC o′ ℓ′ e′ C =
  record
  { Obj = Lift  o′ Obj
  ; _⇒_ = Lifted₂ ℓ′ _⇒_
  ; _≡_ = Lifted₂ e′ _≡_
  ; id = lift id
  ; _∘_ = lifted₂ _∘_
  ; assoc = lift assoc
  ; identityˡ = lift identityˡ
  ; identityʳ = lift identityʳ
  ; equiv = record { refl = lift Equiv.refl
                   ; sym = lift ∙ Equiv.sym ∙ lower
                   ; trans = lifted₂ Equiv.trans
                   }
  ; ∘-resp-≡ = lifted₂ ∘-resp-≡
  }
  where open Category C

LiftF : ∀ {oC ℓC eC oD ℓD eD} oC′ ℓC′ eC′ oD′ ℓD′ eD′ {C : Category oC ℓC eC} {D : Category oD ℓD eD} → Functor C D → Functor (LiftC oC′ ℓC′ eC′ C) (LiftC oD′ ℓD′ eD′ D)
LiftF _ _ _ _ _ _ F =
  record
  { F₀ = lift ∙ F₀ ∙ lower
  ; F₁ = lift ∙ F₁ ∙ lower
  ; identity = lift identity
  ; homomorphism = lift homomorphism
  ; F-resp-≡ = lift ∙ F-resp-≡ ∙ lower
  }
  where open Functor F

LiftFˡ : ∀ {oC ℓC eC oD ℓD eD} {C : Category oC ℓC eC} {D : Category oD ℓD eD} → Functor C D → Functor (LiftC oD ℓD eD C) D
LiftFˡ F =
  record
  { F₀ = F₀ ∙ lower
  ; F₁ = F₁ ∙ lower
  ; identity = identity
  ; homomorphism = homomorphism
  ; F-resp-≡ = F-resp-≡ ∙ lower
  }
  where open Functor F

LiftFʳ : ∀ {oC ℓC eC oD ℓD eD} {C : Category oC ℓC eC} {D : Category oD ℓD eD} → Functor C D → Functor C (LiftC oC ℓC eC D)
LiftFʳ F =
  record
  { F₀ = lift ∙ F₀
  ; F₁ = lift ∙ F₁
  ; identity = lift identity
  ; homomorphism = lift homomorphism
  ; F-resp-≡ = lift ∙ F-resp-≡
  }
  where open Functor F

LiftNT : ∀ {oC ℓC eC oD ℓD eD oC′ ℓC′ eC′ oD′ ℓD′ eD′} {C : Category oC ℓC eC} {D : Category oD ℓD eD} {F G : Functor C D} → NaturalTransformation F G → NaturalTransformation (LiftF oC′ ℓC′ eC′ oD′ ℓD′ eD′ F) (LiftF oC′ ℓC′ eC′ oD′ ℓD′ eD′ G)
LiftNT α = record { η = lift ∙ η ∙ lower; commute = lift ∙ commute ∙ lower }
  where open NaturalTransformation α

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Example usage of solver

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

module Experiment.Categories.Solver.MultiFunctor.Example {o ℓ e} where

open import Categories.Category
open import Categories.Functor renaming (id to idF)
open import Experiment.Categories.Solver.MultiFunctor {o} {ℓ} {e}

module _ {𝒞 𝒟 ℰ : Category o ℓ e} (F : Functor 𝒞 𝒟) (G : Functor 𝒟 ℰ) where
  module F = Functor F
  module G = Functor G
  module 𝒞 = Category 𝒞
  module 𝒟 = Category 𝒟
  open Category ℰ
  open HomReasoning
  module _ {A B C D}
           (f : 𝒞 [ C , D ]) (g : 𝒞 [ B , C ]) (h : 𝒟 [ A , F.F₀ B ]) where
    _ : G.F₁ (F.F₁ f) ∘ G.F₁ 𝒟.id ∘ G.F₁ (F.F₁ g) ∘ G.F₁ h ≈
        G.F₁ (𝒟 [ F.F₁ (𝒞 [ f ∘ g ]) ∘ h ])
    _ = solve (:F₁ G (:F₁ F ∥-∥) :∘ :F₁ G :id :∘ :F₁ G (:F₁ F ∥-∥) :∘ :F₁ G ∥-∥)
              (:F₁ G (:F₁ F (∥-∥ :∘ ∥-∥) :∘ ∥-∥))
              refl


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

refl : ∀ {a}{A : Set a} {x : A} → x ≡ x
refl {x = x} = \ i → x

data Sphere : Set where
  base : Sphere
  surf : PathP (\ i → PathP (\ j → Sphere) base base) (\ _ → base) (\ _ → base)

elim : (D : Sphere → Set) → (b : D base) →
       (s : PathP (\ i → PathP (\ j → D (surf i j)) b b) refl refl) →
       -- the type for the refl is unified with D (surf i0 j), where j is not in scope.
       -- Agda should recognize that "j" is flexible since it goes away by endpoint reduction.
       (x : Sphere) → D x
elim D b s base = b
elim D b s (surf i j) = s i j

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------------
-- Test the consistency of FOTC.Program.McCarthy91.McCarthy91
------------------------------------------------------------------------------

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

-- In the module FOTC.Program.McCarthy91.McCarthy91 we declare Agda
-- postulates as first-order logic axioms. We test if it is possible
-- to prove an unprovable theorem from these axioms.

module FOTC.Program.McCarthy91.McCarthy91.Consistency.Axioms where

open import FOTC.Base
open import FOTC.Program.McCarthy91.McCarthy91

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

postulate impossible : ∀ d e → d ≡ e
{-# ATP prove impossible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe #-}
module Cubical.Foundations.Pointed.Base where

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

open import Cubical.Foundations.Structure
open import Cubical.Foundations.Structure using (typ) public
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function

private
  variable
    ℓ ℓ' : Level

Pointed : (ℓ : Level) → Type (ℓ-suc ℓ)
Pointed ℓ = TypeWithStr ℓ (λ x → x)

pt : ∀ {ℓ} (A∙ : Pointed ℓ) → typ A∙
pt = str

Pointed₀ = Pointed ℓ-zero

{- Pointed functions -}
_→∙_ : (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
(A , a) →∙ (B , b) = Σ[ f ∈ (A → B) ] f a ≡ b

_→∙_∙ : (A : Pointed ℓ) (B : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
(A →∙ B ∙) .fst = A →∙ B
(A →∙ B ∙) .snd .fst x = pt B
(A →∙ B ∙) .snd .snd = refl

idfun∙ : (A : Pointed ℓ) → A →∙ A
idfun∙ A .fst x = x
idfun∙ A .snd = refl

infix 3 _≃∙_
{-Pointed equivalences -}
_≃∙_ : (A : Pointed ℓ) (B : Pointed ℓ') → Type (ℓ-max ℓ ℓ')
A ≃∙ B = Σ[ e ∈ fst A ≃ fst B ] fst e (pt A) ≡ pt B

{- Underlying pointed map of an equivalence -}
≃∙map : {A : Pointed ℓ} {B : Pointed ℓ'} → A ≃∙ B → A →∙ B
fst (≃∙map e) = fst (fst e)
snd (≃∙map e) = snd e

invEquiv∙ : {A : Pointed ℓ} {B : Pointed ℓ'} → A ≃∙ B → B ≃∙ A
fst (invEquiv∙ x) = invEquiv (fst x)
snd (invEquiv∙ {A = A} x) =
  sym (cong (fst (invEquiv (fst x))) (snd x)) ∙ retEq (fst x) (pt A)

compEquiv∙ : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
  → A ≃∙ B → B ≃∙ C → A ≃∙ C
fst (compEquiv∙ e1 e2) = compEquiv (fst e1) (fst e2)
snd (compEquiv∙ e1 e2) = cong (fst (fst e2)) (snd e1) ∙ snd e2

Equiv∙J : {B : Pointed ℓ} (C : (A : Pointed ℓ) → A ≃∙ B → Type ℓ')
          → C B (idEquiv (fst B) , refl)
          → {A : _} (e : A ≃∙ B) → C A e
Equiv∙J {ℓ} {ℓ'} {B = B} C ind {A = A} =
  uncurry λ e p → help e (pt A) (pt B) p C ind
  where
  help : ∀ {A : Type ℓ} (e : A ≃ typ B) (a : A) (b : typ B)
       → (p : fst e a ≡ b)
       → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
       → C (fst B , b) (idEquiv (fst B) , refl)
       → C (A , a)  (e , p)
  help = EquivJ (λ A e → (a : A) (b : typ B)
       → (p : fst e a ≡ b)
       → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
       → C (fst B , b) (idEquiv (fst B) , refl)
       → C (A , a)  (e , p))
        λ a b → J (λ b p
          → (C : (A : Pointed ℓ) → A ≃∙ (fst B , b) → Type ℓ')
                → C (fst B , b)
      (idEquiv (fst B) , refl) →
      C (typ B , a) (idEquiv (typ B) , p))
         λ _ p → p

ua∙ : {A B : Pointed ℓ} (e : fst A ≃ fst B)
                  → fst e (snd A) ≡ snd B → A ≡ B
fst (ua∙ e p i) = ua e i
snd (ua∙ {A = A} e p i) = ua-gluePath e p i

{- J for pointed function types -}
→∙J : ∀ {ℓ ℓ' ℓ''} {A : Pointed ℓ} {B : Type ℓ'}
    → (P : (b₀ : B) (f : A →∙ (B , b₀)) → Type ℓ'')
    → ((f : fst A → B) → P (f (pt A)) (f , refl))
    → {b₀ : B} (f : A →∙ (B , b₀)) → P b₀ f
→∙J {A = A} P ind =
  uncurry λ f → J (λ b₀ y → P b₀ (f , y)) (ind f)

{- HIT allowing for pattern matching on pointed types -}
data Pointer {ℓ} (A : Pointed ℓ) : Type ℓ where
  pt₀ : Pointer A
  ⌊_⌋ : typ A → Pointer A
  id : ⌊ pt A ⌋ ≡ pt₀

IsoPointedPointer : {A : Pointed ℓ} → Iso (typ A) (Pointer A)
Iso.fun IsoPointedPointer = ⌊_⌋
Iso.inv (IsoPointedPointer {A = A}) pt₀ = pt A
Iso.inv IsoPointedPointer ⌊ x ⌋ = x
Iso.inv (IsoPointedPointer {A = A}) (id i) = pt A
Iso.rightInv IsoPointedPointer pt₀ = id
Iso.rightInv IsoPointedPointer ⌊ x ⌋ = refl
Iso.rightInv IsoPointedPointer (id i) j = id (i ∧ j)
Iso.leftInv IsoPointedPointer x = refl

Pointed≡Pointer : {A : Pointed ℓ} → typ A ≡ Pointer A
Pointed≡Pointer = isoToPath IsoPointedPointer

Pointer∙ : (A : Pointed ℓ) → Pointed ℓ
Pointer∙ A .fst = Pointer A
Pointer∙ A .snd = pt₀

Pointed≡∙Pointer : {A : Pointed ℓ} → A ≡ (Pointer A , pt₀)
Pointed≡∙Pointer {A = A} i = (Pointed≡Pointer {A = A} i) , helper i
  where
  helper : PathP (λ i → Pointed≡Pointer {A = A} i) (pt A) pt₀
  helper = ua-gluePath (isoToEquiv (IsoPointedPointer {A = A})) id

pointerFun : ∀ {ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
            → Pointer A → Pointer B
pointerFun f pt₀ = pt₀
pointerFun f ⌊ x ⌋ = ⌊ fst f x ⌋
pointerFun f (id i) = (cong ⌊_⌋ (snd f) ∙ id) i

pointerFun∙ : ∀ {ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B)
             → Pointer∙ A →∙ Pointer∙ B
pointerFun∙ f .fst = pointerFun f
pointerFun∙ f .snd = refl

-- pointed identity equivalence
idEquiv∙ : (A : Pointed ℓ) → (A ≃∙ A)
idEquiv∙ A = (isoToEquiv (iso (λ x → x) (λ x → x) (λ _ → refl) (λ _ → refl))) ,
             refl

{-
  Equational reasoning for pointed equivalences
-}

infix  3 _∎≃∙
infixr 2 _≃∙⟨_⟩_

_∎≃∙ : (A : Pointed ℓ) → A ≃∙ A
A ∎≃∙ = idEquiv∙ A

_≃∙⟨_⟩_ : {B C : Pointed ℓ} (A : Pointed ℓ) → A ≃∙ B → B ≃∙ C → A ≃∙ C
A ≃∙⟨ f ⟩ g = compEquiv∙ f g

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module hPropInvestigations where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Foundations.Prelude
open import Function.Base using (_∋_)
open import Cubical.Foundations.Logic
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Data.Empty renaming (elim to ⊥-elim) renaming (⊥ to ⊥⊥) -- `⊥` and `elim`

import Cubical.Data.Empty as Empty
open import Cubical.Data.Unit.Base

import Cubical.Structures.Axioms

-- NOTE:
--   we have both:
--   the "classic" bundle/unbundle record-based definition of a CommRing from `Cubical.Structures.CommRing`
--
--     record IsCommRing {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where
--       field
--         isRing : IsRing 0r 1r _+_ _·_ -_
--         ·-comm : (x y : R) → x · y ≡ y · x
--     record CommRing : Type (ℓ-suc ℓ) where
--       field
--         Carrier    : Type ℓ
--         0r         : Carrier
--         1r         : Carrier
--         _+_        : Carrier → Carrier → Carrier
--         _·_        : Carrier → Carrier → Carrier
--         -_         : Carrier → Carrier
--         isCommRing : IsCommRing 0r 1r _+_ _·_ -_
--
--   and a CommRingΣTheory
--
--     CommRingAxioms R (_+_ , 1r , _·_) = RingAxioms R (_+_ , 1r , _·_) × ((x y : R) → x · y ≡ y · x)
--     CommRingStructure = AxiomsStructure RawRingStructure CommRingAxioms
--     CommRingΣ         = TypeWithStr ℓ CommRingStructure
--     CommRingEquivStr  : StrEquiv CommRingStructure ℓ
--     CommRingEquivStr  = AxiomsEquivStr RawRingEquivStr CommRingAxioms
--
--   especially when we look at
--
--     CommRingEquivStr = AxiomsEquivStr RawRingEquivStr CommRingAxioms
--
--   here `AxiomsEquivStr` from `Cubical.Structures.Axioms`
--
--     AxiomsEquivStr : {S : Type ℓ → Type ℓ₁} (ι : StrEquiv S ℓ₁') (axioms : (X : Type ℓ) → S X → Type ℓ₂)
--                    → StrEquiv (AxiomsStructure S axioms) ℓ₁'
--     AxiomsEquivStr ι axioms (X , (s , a)) (Y , (t , b)) e = ι (X , s) (Y , t) e
--
--   takes the two arguments `RawRingEquivStr` and `CommRingAxioms`
--
--     RawRingEquivStr = AutoEquivStr RawRingStructure
--
--     CommRingAxioms : (R : Type ℓ) (s : RawRingStructure R) → Type ℓ
--     CommRingAxioms R (_+_ , 1r , _·_) = RingAxioms R (_+_ , 1r , _·_) × ((x y : R) → x · y ≡ y · x)
--
--   where `AutoEquivStr` is a macro from `Cubical.Structures.Auto`
--
--     -- (S : Type ℓ → Type ℓ₁) → StrEquiv (AutoStructure S) _
--     AutoEquivStr : R.Term → R.Term → R.TC Unit
--     AutoEquivStr t hole =
--       newMeta (tDesc R.unknown) >>= λ d →
--       R.unify hole (R.def (quote MacroEquivStr) [ varg d ]) >>
--       autoDesc' t d

import Cubical.Structures.CommRing
open import Cubical.Data.Sigma.Properties
import Cubical.Foundations.Transport
import Cubical.Foundations.Path

¬[P⊓¬P] : ∀(P : hProp ℓ) → [ ¬(P ⊓ ¬ P) ]
¬[P⊓¬P] _ (p , q) = q p

lemma-comm : ∀(P : hProp ℓ) → P ⊓ ¬ P ≡ ¬ P ⊓ P
lemma-comm P = ⊓-comm P (¬ P)

lemma-comm-elm-forward : ∀(P : hProp ℓ) → [ P ⊓ ¬ P ] → [ ¬ P ⊓ P ]
lemma-comm-elm-forward P (p , ¬p) = (¬p , p)

lemma-comm-elm-back : ∀(P : hProp ℓ) → [ ¬ P ⊓ P ] → [ P ⊓ ¬ P ]
lemma-comm-elm-back P (¬p , p) = (p , ¬p)

comm-elm-iso : ∀(P : hProp ℓ) → Iso [ P ⊓ ¬ P ] [ ¬ P ⊓ P ]
comm-elm-iso P = λ where
  .Iso.fun        → lemma-comm-elm-forward P
  .Iso.inv        → lemma-comm-elm-back P
  .Iso.rightInv _ → refl
  .Iso.leftInv  _ → refl

-- let A = fst P
-- [ P ⊓ ¬ P ] : A × (A → ⊥)
-- [ ¬ P ⊓ P ] : (A → ⊥) × A
-- we have `P ⊓ ¬ P ≡ ¬ P ⊓ P`
-- and we have ≡ for the witness-type `[ P ⊓ ¬ P ] ≡ [ ¬ P ⊓ P ]`
-- because `A × (A → ⊥) ≢ (A → ⊥) × A`

lemma-Σ-swap-≡ : ∀(A B : Type ℓ) → (A × B) ≡ (B × A)
lemma-Σ-swap-≡ A B = isoToPath (Σ-swap-Iso {A = A} {A' = B})

lemma-comm-elm' : ∀(P : hProp ℓ) → [ P ⊓ ¬ P ] ≡ [ ¬ P ⊓ P ]
lemma-comm-elm' P = lemma-Σ-swap-≡ _ _

lemma-comm-elm : ∀(P : hProp ℓ) → [ P ⊓ ¬ P ] ≡ [ ¬ P ⊓ P ]
lemma-comm-elm P = isoToPath (comm-elm-iso P)

-- see `2.8 Classical principles` in Booij's thesis
weak-LEM' : ∀(P : hProp ℓ) → [ (¬ ¬ P) ⊔ (¬ P) ]
weak-LEM' {ℓ = ℓ} P = {! (¬[P⊓¬P] P) ∘ pathTo⇒ (⊓-comm (¬ P) P) !} -- (⊓-comm P (¬ P)) ∘ (¬[P⊓¬P] P)
  where
    γ : P ⊓ ¬ P ≡ ¬ P ⊓ P
    -- γ : PathP (λ i → ?)
    γ = ⊓-comm P (¬ P)
    κ : [ P ⊓ ¬ P ⇒ ¬ P ⊓ P ]
 -- κ : [ P ⊓ ¬ P ] → [ ¬ P ⊓ P ] -- is the same !
    κ = pathTo⇒ γ
    η : [ P ⊓ ¬ P ] → [ ¬ P ⊓ P ]
    η p = κ p
    φ : [ ¬ (¬ P ⊓ P) ] -- and from here we would need deMorgan₁ to obtain the goal which is not provable without further assumptions
    φ = (¬[P⊓¬P] P) ∘ pathTo⇒ (⊓-comm (¬ P) P)
    -- (p , q) = Iso.inv ΣPathIsoPathΣ γ
    pq : Σ[ p ∈ fst (P ⊓ ¬ P) ≡ fst (¬ P ⊓ P) ] PathP (λ i → isProp (p i)) (snd (P ⊓ ¬ P)) (snd (¬ P ⊓ P))
    pq = Iso.inv ΣPathIsoPathΣ γ
    p : fst (P ⊓ ¬ P) ≡ fst (¬ P ⊓ P)
    p = fst pq
    q : PathP (λ i → isProp (fst pq i)) (snd (P ⊓ ¬ P)) (snd (¬ P ⊓ P))
    q = snd pq
    k = transport {ℓ = ℓ} {A = isProp (fst (P ⊓ ¬ P))} {B = isProp (fst (¬ P ⊓ P))} {! κ  !}
    l = {! Σ[ A ∈ Type ℓ ] isProp A!}
-- ⊓-comm P (¬ P) : P ⊓ ¬ P ≡ ¬ P ⊓ P
-- [ ¬ ¬ P ⊔ ¬ P ]
-- [ ¬ (¬ P ⊓ P) ]
-- hProp ℓ = Σ[ A ∈ Type ℓ ] (∀(x y : A) → x ≡ y)
--         = Σ[ A ∈ Type ℓ ] isProp A
-- HOTT: Definition 3.3.1. A type P is a mere proposition if for all x, y : P we have x = y.
-- NOTE: so `isMere P = isProp P`
-- _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
-- _≡_ {A = A} = PathP (λ i → A)
-- transport : {A B : Type ℓ} → A ≡ B → A → B
-- transport p a = transp (λ i → p i) i0 a
-- pathTo⇒ : P ≡ Q → [ P ⇒ Q ]
-- PathP is dependent path type (builtin)
-- Path is non-dependent path type
--   PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 →  Set ℓ
--   Path  : ∀ {ℓ} (A :    Type ℓ) → A    → A    → Type ℓ
--   Path A a b = PathP (λ _ → A) a b
-- Direct definitions of lower h-levels
--   isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)
--   isProp  A = (x y : A) → x ≡ y
--   isSet   A = (x y : A) → isProp (x ≡ y)
--
-- an element of   hProp   states what the proposition is    - the element is the proposition
-- an element of [ hProp ] states that the proposition holds - the element is the proof
-- pathes such as `P ⊓ ¬ P ≡ ¬ P ⊓ P` just state that the propositions are the same
-- we cannot use `transport` on `P ⊓ ¬ P ≡ ¬ P ⊓ P`
-- `⇔toPath` can be used to get equality of the propositions from forward and backward implication based on the witnesses
--   ⇔toPath : [ P ⇒ Q ] → [ Q ⇒ P ] → P ≡ Q
-- similar with `hProp≡`
--   hProp≡ : [ P ] ≡ [ Q ] → P ≡ Q
-- there is `pathTo⇒` and `pathTo⇐` to create witness-based implications
--   pathTo⇒ : P ≡ Q → [ P ⇒ Q ]
--   pathTo⇐ : P ≡ Q → [ Q ⇒ P ]
-- here, we have that `[ P ⇒ Q ]` is definitionally equivalent to `[ P ] → [ Q ]`
-- because `[ P ] → [ Q ]` is the first element of the tuple `P ⇒ Q` which gets projected out with `[_]`
--   A ⇒ B = ([ A ] → [ B ]) , isPropΠ λ _ → isProp[] B
-- we can use `isoToPath` to create a path `[ P ] ≡ [ Q ]` but only when we are able to formulate an isomorphism
-- so `[ P ] ≡ [ Q ]` is what we can transport the witnesses along
--   isoToPath  : Iso A B → A ≡ B
--   isoToEquiv : Iso A B → A ≃ B
-- with
--   A ≃ B = Σ[ f ∈ A → B ] isEquiv f
-- where `isEquiv` is basically
--   isEquiv = (f : A → B) → ∀(y : B) → isContr (fiber f y)
-- but it seems to be a very strong property of two ≡-equal propositions to have their elements being ≡-equal too
--   is it? Or can we always find an isomorphism `Iso [ P ] [ Q ]` for every path `P ≡ Q`? I guess not

-- ∥¬A∥≡¬∥A∥
_ = hProp≡
_ = transport
_ = ∥ {!!} ∥
_ = _≡_
_ = Path

-- Propositions
--
-- Definition 2.4.1. A proposition is a type P all whose elements are identical, which is expressed type-theoretically as
--
--   isHProp(P) := (Π p, q : P) (p =ₚ q).
--
-- We have the type
--
--   HProp := (Σ P : U) isHProp(P)
--
-- of all propositions, and we identify elements of HProp with their underlying type, that is, their first projection.
-- The letter ‘H’ stands for homotopy, which we briefly touch on in Section 2.5.4.
--
-- checkout p.31 ff of Booij's thesis
--
-- Definition 2.4.5. Univalent logic is defined by the following, where P, Q : HProp and R : X → HProp [91, Definition 3.7.1]:
--
--   ⊤              := 1
--   ⊥              := 0
--   P ∧ Q          := P × Q
--   P ⇒ Q          := P → Q
--   P ⇔ Q          := P = Q
--   ¬P             := P → 0
--   P ∨ Q          := ∥ P + Q ∥
--   (∀ x : X) R(x) :=  (Π x : X) R(x)
--   (∃ x : X) R(x) := ∥ (Σ x : X) R(x) ∥
--
-- NOTE: the important sentence is "we identify elements of HProp with ... their first projection"
--       therefore Agda's first projection `[_]` is not present in Booij's writing (it's implicit)

import Cubical.Functions.Embedding

-- Embeddings are generalizations of injections. The usual
-- definition of injection as:
--
--    f x ≡ f y → x ≡ y
--
-- is not well-behaved with higher h-levels, while embeddings
-- are.
--
--   isEmbedding : (A → B) → Type _
--   isEmbedding f = ∀ w x → isEquiv {A = w ≡ x} (cong f)

-- injEmbedding
--   : {f : A → B}
--   → isSet A → isSet B
--   → (∀{w x} → f w ≡ f x → w ≡ x)
--   → isEmbedding f

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import FRP.JS.Nat using ( ℕ ; zero ; suc )
open import FRP.JS.Bool using ( Bool ; true ; false ; _∧_ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )

module FRP.JS.List where

infixr 4 _∷_ _++_
infixr 2 _≟[_]_

data List {α} (A : Set α) : Set α where
  [] : List A
  _∷_ : (a : A) → (as : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

[_] : ∀ {α} {A : Set α} → A → List A
[ x ] = x ∷ []

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

map : ∀ {α β} {A : Set α} {B : Set β} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

foldr : ∀ {α β} {A : Set α} {B : Set β} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

foldl : ∀ {α β} {A : Set α} {B : Set β} → (A → B → A) → A → List B → A
foldl c n []       = n
foldl c n (x ∷ xs) = foldl c (c n x) xs

buildAppend : ∀ {α} {A : Set α} → List A → (ℕ → A) → ℕ → List A
buildAppend as f zero    = as
buildAppend as f (suc n) = buildAppend (f n ∷ as) f n

build : ∀ {α} {A : Set α} → (ℕ → A) → ℕ → List A
build = buildAppend []

length : ∀ {α} {A : Set α} → List A → ℕ
length = foldr (λ a n → suc n) zero

lookup : ∀ {α} {A : Set α} → List A → ℕ → Maybe A
lookup []       x       = nothing
lookup (a ∷ as) zero    = just a
lookup (a ∷ as) (suc n) = lookup as n

_≟[_]_ : ∀ {α β} {A : Set α} {B : Set β} → List A → (A → B → Bool) → List B → Bool
[]       ≟[ p ] []       = true
(a ∷ as) ≟[ p ] (b ∷ bs) = (p a b) ∧ (as ≟[ p ] bs)
_        ≟[ p ] _        = false

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Andreas, 2020-11-18, issue #5065, reported by nad
-- Termination checker regresssion in Agda 2.6.1

-- {-# OPTIONS -v term.reduce:80 #-}

open import Agda.Builtin.Bool

bad : Bool → Bool
bad b with bad b
… | true  = bad b
… | false = true

-- Termination checker loops in Agda 2.6.1.

-- Expected error (works in <= 2.6.0 and now again in 2.6.2):
--
-- Termination checking failed for the following functions:
--   bad
-- Problematic calls:
--   bad b


text:
module Structure.Relator.Ordering where

import      Lvl
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Logic.Propositional.Theorems
open import Structure.Relator.Properties
  hiding (antisymmetry ; asymmetry ; transitivity ; reflexivity ; irreflexivity ; trichotomy)
open import Type
open import Type.Properties.Empty

private variable ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Lvl.Level

-- A weak order formalizes both "less or equals"-relations and "greater or equals"-relations.
module Weak {T : Type{ℓ₁}} (_≤_ : T → T → Stmt{ℓ₂}) where
  record PartialOrder (_≡_ : T → T → Stmt{ℓ₃}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field
     ⦃ antisymmetry ⦄ : Antisymmetry(_≤_)(_≡_)
     ⦃ transitivity ⦄ : Transitivity(_≤_)
     ⦃ reflexivity ⦄  : Reflexivity (_≤_)

  -- A weak total order is a weak partial order where all objects are ordered.
  -- Also called: Weak Linear order
  record TotalOrder (_≡_ : T → T → Stmt{ℓ₃}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field
     ⦃ partialOrder ⦄ : PartialOrder(_≡_)
     ⦃ totality ⦄     : ConverseTotal(_≤_)

  module Properties where
    -- A left extremum is an object which is one of the left-most in the order of all objects.
    record Extremumₗ (e : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x : T} → (e ≤ x)

    -- A left extremum is an object which is one of the right-most in the order of all objects.
    record Extremumᵣ (e : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      constructor intro
      field proof : ∀{x : T} → (x ≤ e)

    Extremum : T → Stmt{ℓ₁ Lvl.⊔ ℓ₂}
    Extremum(e) = Extremumₗ(e) ∨ Extremumᵣ(e)

    module LE where
      Minimum = Extremumₗ
      Maximum = Extremumᵣ

      module Minimum = Extremumₗ
      module Maximum = Extremumᵣ

  extremeₗ : ⦃ _ : ∃(Properties.Extremumₗ) ⦄ → T
  extremeₗ ⦃ e ⦄ = [∃]-witness e

  extremeᵣ : ⦃ _ : ∃(Properties.Extremumᵣ) ⦄ → T
  extremeᵣ ⦃ e ⦄ = [∃]-witness e

  module LE where
    min = extremeₗ
    max = extremeᵣ

module Strict {T : Type{ℓ₁}} (_<_ : T → T → Stmt{ℓ₂}) where
  record PartialOrder : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
    constructor intro
    field
     ⦃ transitivity ⦄  : Transitivity  (_<_)
     ⦃ asymmetry ⦄     : Asymmetry     (_<_)
     ⦃ irreflexivity ⦄ : Irreflexivity (_<_)

  -- A strict total order is a strict partial order where all objects are ordered.
  -- Also called: Strict linear order
  record TotalOrder(_≡_ : T → T → Stmt{ℓ₃}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    constructor intro
    field
     ⦃ partialOrder ⦄ : PartialOrder
     ⦃ trichotomy ⦄   : ConverseTrichotomy(_<_)(_≡_)

  module Properties where
    -- An ordering of a type is dense when there is an object inbetween every pair of objects with respect to its order.
    record Dense : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      field
        between : T → T → T
        left    : ∀{x y : T} → ⦃ _ : (x < y) ⦄ → (x < between(x)(y))
        right   : ∀{x y : T} → ⦃ _ : (x < y) ⦄ → (between(x)(y) < y)

    -- An element is left accessible when there is a left-most object in the order when comparing to the element.
    -- It is defined as: An element is accessible when all objects to the left of the object in the order is accessible.
    -- Because this is an inductive definition, it must have a base case (the terminating case) where the proof is vacuously true (an element which is vacuously accessible). This element can be interpreted as the left-most object.
    -- Example using sets and a weak partial order:
    --   S   = ℤ ∪ {a,b,c}
    --   _≤_ = ℤ._≤_ ∪ {(a,b),(b,c₁),(b,c₂),(a,c₁),(a,c₂) , (a,a),(b,b),(c₁,c₁),(c₂,c₂)}
    --   a is accessible because there are no elements lesser than a (∀(x∊S). ¬(x ≤ a)).
    --   b is accessible because only a is lesser than b, and it is accessible.
    --   c₁ is accessible because all elements lesser than c₁ are a and b, and both of them are accessible.
    --   c₂ is accessible because all elements lesser than c₂ are a and b, and both of them are accessible.
    record Accessibleₗ (a : T) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
      inductive
      pattern
      constructor intro
      field ⦃ proof ⦄ : ∀{x : T} → ⦃ _ : (x < a) ⦄ → Accessibleₗ(x)

    accessible-induction : ∀{P : T → Type{ℓ₃}} → (∀{x} → (∀{prev} → ⦃ _ : (prev < x) ⦄ → P(prev)) → P(x)) → (∀{x} → ⦃ _ : Accessibleₗ(x) ⦄ → P(x))
    accessible-induction proof ⦃ intro ⦄ = proof(accessible-induction proof)

    accessible-recursion : ∀{U : T → Type{ℓ₃}} → ((x : T) → ((prev : T) → ⦃ _ : (prev < x) ⦄ → U(prev)) → U(x)) → ((x : T) → ⦃ _ : Accessibleₗ(x) ⦄ → U(x))
    accessible-recursion previous x ⦃ intro ⦄ = previous x (\x → accessible-recursion previous x)

    open import Relator.Equals
    accessible-recursion-intro : ∀{P : T → Type{ℓ₃}}{rec : ∀(x) → _ → P(x)}{φ : ∀{x} → P(x) → Type{ℓ₄}}
                               → (∀(y) ⦃ acc-y : Accessibleₗ(y)⦄
                                 → (∀{x} → ⦃ xy : x < y ⦄ → φ{x}(accessible-recursion rec x ⦃ Accessibleₗ.proof acc-y {x} ⦄))
                                 → (∀{x} → ⦃ xy : x < y ⦄ → (accessible-recursion rec y ≡ rec y (\x → accessible-recursion rec x ⦃ Accessibleₗ.proof acc-y {x} ⦄)))
                                 → φ{y}(accessible-recursion rec y)
                               )
                               → (∀{x} → ⦃ acc : Accessibleₗ(x) ⦄ → φ(accessible-recursion{U = P} rec x))
                               -- accessible-recursion rec x ⦃ Accessibleₗ.proof acc-y {x} ⦄
    accessible-recursion-intro{φ = φ} step {x} acc-x@⦃ intro ⦃ prev ⦄ ⦄ = step x ⦃ acc-x ⦄
      (\{y} ⦃ xy ⦄ → accessible-recursion-intro{φ = φ} step {y} ⦃ prev{y} ⦃ xy ⦄ ⦄)
      [≡]-intro

    -- TODO: When proving stuff about a function defined using accessible-recursion? accessible-recursion-all-proof : ∀{U}{x} → ⦃ _ : Accessibleₗ(x) ⦄ → P(accessible-recursion)

    -- An order is well-founded when all objects have a left-most element in the order relative to themselves.
    -- It is well-founded when all objects are left accessible.
    -- Note: Not equivalent to the classical definition of well-foundedness. This does not require a construction of the minimal element. (TODO: I think? At least not computable from the relation? So maybe this should be renamed to something else?)
    -- Note: In the context of rewriting, the a well-founded converse is called terminating.
    -- TODO: Maybe move this to ReductionSystems because it is formalized like this in those cases, but well-foundedness is usually defined using some other formula classically?
    WellFounded : Stmt{ℓ₁ Lvl.⊔ ℓ₂}
    WellFounded = ∀ₗ(Accessibleₗ)
    wellfounded = \{a} ⦃ acc ⦄ {x} ⦃ p ⦄ → inst-fn(Accessibleₗ.proof {a = a}) ⦃ acc ⦄ {x} ⦃ p ⦄

    wellfounded-induction : ⦃ WellFounded ⦄ → ∀{P : T → Type{ℓ₃}} → (∀{x} → (∀{prev} → ⦃ _ : (prev < x) ⦄ → P(prev)) → P(x)) → (∀{x} → P(x))
    wellfounded-induction proof = accessible-induction proof

    -- A helper function that helps defining a recursive function which is able to depend on all its preceding values without explicit recursion.
    -- Note: When non-dependent
    --   If the function to be defined is not a dependent function, then the type is:
    --   wellfounded-recursion : ∀{U : Type{ℓ₃}} → ((x : T) → ((prev : T) → ⦃ _ : (prev < x) ⦄ → U) → U) → (T → U)
    wellfounded-recursion : ⦃ WellFounded ⦄ → ∀{P : T → Type{ℓ₃}} → ((x : T) → ((prev : T) → ⦃ _ : (prev < x) ⦄ → P(prev)) → P(x)) → ((x : T) → P(x))
    wellfounded-recursion proof x = accessible-recursion proof x

    wellfounded-recursion-intro : ⦃ wf : WellFounded ⦄ → ∀{P : T → Type{ℓ₃}}{rec : ∀(x) → _ → P(x)}{φ : ∀{x} → P(x) → Type{ℓ₄}}
                                → (∀(y)
                                  → (∀{x} → ⦃ xy : x < y ⦄ → φ{x}(wellfounded-recursion rec x))
                                  → (∀{x} → ⦃ xy : x < y ⦄ → (accessible-recursion rec y ≡ rec y (\x → wellfounded-recursion rec x)))
                                  → φ{y}(accessible-recursion rec y)
                                )
                                → (∀{x} → φ(accessible-recursion{U = P} rec x))
    wellfounded-recursion-intro{φ = φ} step = accessible-recursion-intro{φ = φ} (\x → step x)

  -- A well-ordering is a well-founded strict total order
  record WellOrder(_≡_ : T → T → Stmt{ℓ₃}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓ₃} where
    instance constructor intro
    field
     ⦃ totalOrder ⦄  : TotalOrder(_≡_)
     ⦃ wellfounded ⦄ : Properties.WellFounded


text:
module _ (_ : Set) where

open import Agda.Builtin.Size

postulate
  I : Set

record ∃ (B : I → Set) : Set where
  constructor _,_
  field
    proj₁ : I
    proj₂ : B proj₁

module M (_ : Set₁) where

  mutual

    P : Size → I → I → Set
    P i x y = ∃ (Q i x)

    record Q (i : Size) (x y : I) : Set where
      coinductive
      field
        force : {j : Size< i} → P j x y

open M Set

postulate
  map   : (B : I → Set) → (∀ x → B x → B x) → ∃ B → ∃ B
  lemma : ∀ x y i → Q i x y → Q i x y

p  : ∀ x i → P i x x
q′ : ∀ x i → ∃ λ y → Q i x y
q  : ∀ x i → Q i x x

q′ x i              = x , q x i
p x i               = map _ (λ y → lemma x y _) (q′ x _)
Q.force (q x i) {j} = p _ _

max_forks_repo_name: Agda-zh/agda


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

open import HoTT
open import homotopy.PtdAdjoint
open import homotopy.SuspAdjointLoop
open import cohomology.WithCoefficients

module cohomology.SuspAdjointLoopIso where

module SuspAdjointLoopIso {i} where

  private
    hadj : HomAdjoint {i} {i} Σ⊣Ω.SuspFunctor Σ⊣Ω.LoopFunctor
    hadj = counit-unit-to-hom Σ⊣Ω.adj

    module A = HomAdjoint hadj

  module _ (X Y : Ptd i) where

    abstract
      pres-comp : (h₁ h₂ : fst (⊙Susp X ⊙→ ⊙Ω Y))
        → –> (A.eq X (⊙Ω Y)) (⊙conc ⊙∘ ⊙×-in h₁ h₂)
           == ⊙conc ⊙∘ ⊙×-in (–> (A.eq X (⊙Ω Y)) h₁) (–> (A.eq X (⊙Ω Y)) h₂)
      pres-comp h₁ h₂ =
        B.nat-cod h₁ h₂ ⊙conc
        ∙ ap (λ w → w ⊙∘ ⊙×-in (–> (A.eq X (⊙Ω Y)) h₁) (–> (A.eq X (⊙Ω Y)) h₂))
             arr2-lemma
        where
        module A× = RightAdjoint× hadj
        module B = RightAdjointBinary hadj

        ap2-lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
          (f : A × B → C) {r s : A × B} (p : r == s)
          → ap f p == ap2 (curry f) (ap fst p) (ap snd p)
        ap2-lemma f idp = idp

        ⊙ap2-lemma : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
          (f : fst (X ⊙× Y ⊙→ Z))
          → ⊙ap f == ⊙ap2 f ⊙∘ ⊙×-in (⊙ap ⊙fst) (⊙ap ⊙snd)
        ⊙ap2-lemma (f , idp) = ⊙λ= (ap2-lemma f) idp

        arr2-lemma : B.arr2 ⊙conc == ⊙conc
        arr2-lemma =
          ⊙ap ⊙conc ⊙∘ A×.⊙out _ _
            =⟨ ⊙ap2-lemma ⊙conc |in-ctx (λ w → w ⊙∘ A×.⊙out _ _) ⟩
          (⊙ap2 ⊙conc ⊙∘ A×.⊙into _ _) ⊙∘ A×.⊙out _ _
            =⟨ ⊙∘-assoc (⊙ap2 ⊙conc) (A×.⊙into _ _) (A×.⊙out _ _) ⟩
          ⊙ap2 ⊙conc ⊙∘ (A×.⊙into _ _ ⊙∘ A×.⊙out _ _)
            =⟨ A×.⊙into-out _ _ |in-ctx (λ w → ⊙ap2 ⊙conc ⊙∘ w) ⟩
          ⊙ap2 ⊙conc
            =⟨ ⊙ap2-conc-is-conc ⟩
          ⊙conc ∎

    iso : →Ω-group (⊙Susp X) Y ≃ᴳ →Ω-group X (⊙Ω Y)
    iso = Trunc-group-iso
      (–> (A.eq X (⊙Ω Y))) pres-comp (snd (A.eq X (⊙Ω Y)))

  abstract
    nat-dom : {X Y : Ptd i} (f : fst (X ⊙→ Y)) (Z : Ptd i)
      → fst (iso X Z) ∘ᴳ →Ω-group-dom-act (⊙susp-fmap f) Z
        == →Ω-group-dom-act f (⊙Ω Z) ∘ᴳ fst (iso Y Z)
    nat-dom f Z = hom= _ _ $ λ= $ Trunc-elim
      (λ _ → =-preserves-level _ Trunc-level)
      (λ g → ap [_] (! (A.nat-dom f (⊙Ω Z) g)))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text: {-# OPTIONS --profile=feta #-}


text:
module _ where

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality

[_==_] : ∀ {a} {A : Set a} (x y : A) → x ≡ y → A
[ x == _ ] _ = x

pattern ! = refl

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

data Vec {a} (A : Set a) : Nat → Set a where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

_++_ : ∀ {a n m} {A : Set a} → Vec A n → Vec A m → Vec A (n + m)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

toList : ∀ {a n} {A : Set a} → Vec A n → List A
toList []       = []
toList (x ∷ xs) = x ∷ toList xs

foo : ∀ {a n} {A : Set a} (xs ys : Vec A n) → Vec A (n + n)
foo [] [] = []
foo xs@(x ∷ xs₁) ys@(y ∷ ys₁) = [ xs == x ∷ xs₁ ] ! ++ [ ys == y ∷ ys₁ ] !

--- Record patterns ---

infixr 0 _,_
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ

rec : ∀ {a b} {A : Set a} {B : A → Set b} → Σ A B → Σ A B
rec p@record{ fst = x; snd = y } = p

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

insideRec : ∀ {a} {A : Set a} → Σ Nat (Vec A) → List A
insideRec p@record{ fst = zero     ; snd = xs  } = toList ([ snd p == xs ] !)
insideRec record { fst = n@(suc _) ; snd = xs@(x ∷ []) } =
  [ n == 1 ] ! |> toList ([ xs == x ∷ [] ] !)
insideRec record { fst = n@(suc _) ; snd = xs₀@(x ∷ xs₁@(x₁ ∷ xs)) } =
  toList ([ xs₀ == x ∷ xs₁ ] ! ++ [ xs₁ == x₁ ∷ xs ] !)

check : insideRec (_ , 1 ∷ 2 ∷ 3 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ 2 ∷ 3 ∷ []
check = refl

--- Copatterns ---

Nary : ∀ {a} → Nat → Set a → Set a
Nary zero    A = A
Nary (suc n) A = Nat → Nary n A

copat : ∀ {a} {A : Set a} → (Nat → A) → Σ Nat λ n → Nary n A
fst (copat f) = 1
snd (copat f) n@(suc m) = f ([ n == suc m ] !)
snd (copat f) n@zero    = f ([ n == 0 ] !)

--- Dot patterns ---

weird-but-legal : ∀ n → Vec Nat n → Nat
weird-but-legal n@.n [] = [ n == 0 ] !
weird-but-legal n@.n (_∷_ {m} x xs) = [ n == suc m ] !

--- Let pattern bindings ---

letpat : ∀ {a} {A : Set a} → Σ Nat (Vec A) → Nat
letpat p =
  let q@(n , xs) = p in [ fst ([ p == q ] !) == n ] !

letpat₁ : Σ Nat (λ _ → Σ Nat λ _ → Nat) → Nat
letpat₁ p =
  let (a , q@(b , c)) = p in [ snd q == c ] !


text:
module examplesPaperJFP.loadAllOOAgdaFilesAsInLibrary where

-- this file loads those files from the ooAgda paper
-- which occur in the library as well
-- the code as it occurred in the original paper after adapting to current Agda
--    including any code not found directly inthe library
--    can be found in loadAllOOAgdaPart1.agda
--    and             loadAllOOAgdaPart2.agda

-- Source of paper:
--  Andreas Abel, Stephan Adelsberger, Anton Setzer:
--    Interactive Programming in Agda - Objects and Graphical User Interfaces
--    Journal of Functional Programming, 27, 2017
--    doi: http://dx.doi.org/10.1145/2976022.2976032
--    authors copy: http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.pdf
--    bibtex: http://www.cs.swan.ac.uk/~csetzer/articles/ooAgda.bib

-- 1. Introdution
-- 2. Introduction to Agda
-- 3. Coalgebras in Agda
-- 3.1. Coalgebra by example: Colists
-- 3.2. Coalgebras in General
-- 4. Interactive Programs in Agda
-- 4.1. Interaction interfaces
-- 4.2. Interaction trees
-- 4.3. Running interactive programs
-- 5. Objects in Agda

-- code as in paper adapted to new Agda
-- open import examplesPaperJFP.Object
-- code as in library
open import SizedIO.Object

-- 6. Sized Coinductive Types
-- 7. Interface Extension and Delegation

-- code as in paper adapted to new Agda
-- open import examplesPaperJFP.CounterCell
-- code as in library
open import Sized.CounterCell

-- 8. State-Dependent Objects and IO
-- 8.1 State-Dependent Interfaces
-- 8.2 State-Dependent Objects
-- 8.2.1. Example of Use of Safe Stack
-- 8.3 Reasoning About Stateful Objects
-- 8.3.1. Bisimilarity
-- 8.3.2. Verifying stack laws}
-- 8.3.3. Bisimilarity of different stack implementations
-- 8.4. State-Dependent IO
-- 9. A Drawing Program in Agda

open import SizedIO.IOGraphicsLib

-- 10. A Graphical User Interface using an Object
-- 10.1. wxHaskell
-- 10.2. A Library for Object-Based GUIs in Agda

open import StateSizedIO.GUI.VariableList
open import StateSizedIO.GUI.WxGraphicsLib

-- 10.3 Example: A GUI controlling a Space Ship in Agda

open import StateSized.GUI.SpaceShipSimpleVar
open import StateSized.GUI.SpaceShipCell
open import StateSized.GUI.SpaceShipAdvanced

-- 11. Related Work
-- 12. Conclusion
-- Bibliography

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-
  General lemmas about morphisms (defined as loosely as possible)
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Functions.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function

open Iso
module ax {ℓ : Level} (A : Type ℓ) (_+A_ : A → A → A) (a₀ : A) where
  rUnit = (a : A) → a +A a₀ ≡ a
  lUnit = (a : A) → a₀ +A a ≡ a

  rCancel : (-A_ : A → A) → Type ℓ
  rCancel -A_ = (a : A) → a +A (-A a) ≡ a₀

  lCancel : (-A_ : A → A) → Type ℓ
  lCancel -A_ = (a : A) → (-A a) +A a ≡ a₀

  assoc = (x y z : A) → x +A (y +A z) ≡ ((x +A y) +A z)

  comm = (x y : A) → x +A y ≡ y +A x

module morphLemmas {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'}
         (_+A_ : A → A → A) (_+B_ : B → B → B)
         (f : A → B) (f-hom : (x y : A) → f (x +A y) ≡ f x +B f y)
         where

  0↦0 : (a₀ : A) (b₀ : B) (-A_ : A → A) (-B_ : B → B)
      → ax.rUnit A _+A_ a₀
      → ax.rUnit B _+B_ b₀
      → ax.rCancel B _+B_ b₀ -B_
      → ax.assoc B _+B_ b₀
      → f a₀ ≡ b₀
  0↦0 a₀ b₀ -A_ -B_ rUnitA rUnitB rCancelB assocB =
       sym (rUnitB (f a₀))
    ∙∙ cong (f a₀ +B_) (sym (rCancelB (f a₀)))
    ∙∙ assocB (f a₀) (f a₀) (-B f a₀)
    ∙∙ sym (cong (_+B (-B f a₀)) (cong f (sym (rUnitA a₀)) ∙ f-hom a₀ a₀))
    ∙∙ rCancelB (f a₀)

  distrMinus : (a₀ : A) (b₀ : B) (-A_ : A → A) (-B_ : B → B)
            → ax.lUnit B _+B_ b₀
            → ax.rUnit B _+B_ b₀
            → ax.lCancel A _+A_ a₀ -A_
            → ax.rCancel B _+B_ b₀ -B_
            → ax.assoc B _+B_ b₀
            → (0↦0 : f a₀ ≡ b₀)
            → (x : A) → f (-A x) ≡ -B (f x)
  distrMinus a₀ b₀ -A_ -B_ lUnitB rUnitB lCancelA rCancelB assocB 0↦0 x =
       sym (rUnitB _)
    ∙∙ cong (f (-A x) +B_) (sym (rCancelB (f x)))
    ∙∙ assocB _ _ _
    ∙∙ cong (_+B (-B (f x))) (sym (f-hom (-A x) x) ∙∙ cong f (lCancelA x) ∙∙ 0↦0)
    ∙∙ lUnitB _

  distrMinus' : (a₀ : A) (b₀ : B) (-A_ : A → A) (-B_ : B → B)
             → ax.lUnit B _+B_ b₀
             → ax.rUnit B _+B_ b₀
             → ax.rUnit A _+A_ a₀
             → ax.lCancel A _+A_ a₀ -A_
             → ax.rCancel B _+B_ b₀ -B_
             → ax.assoc A _+A_ a₀
             → ax.assoc B _+B_ b₀
             → f a₀ ≡ b₀ -- not really needed, but it can be useful to specify the proof yourself
             → (x y : A)
             → f (x +A (-A y)) ≡ (f x +B (-B (f y)))
  distrMinus' a₀ b₀ -A_ -B_ lUnitB rUnitB rUnitA lCancelA rCancelB assocA assocB 0↦0 x y =
       sym (rUnitB _)
    ∙∙ cong (f (x +A (-A y)) +B_) (sym (rCancelB (f y))) ∙ assocB _ _ _
    ∙∙ cong (_+B (-B f y)) (sym (f-hom (x +A (-A y)) y)
                          ∙ cong f (sym (assocA x (-A y) y)
                                 ∙∙ cong (x +A_) (lCancelA y)
                                 ∙∙ rUnitA x))

  isMorphInv :  (g : B → A) → section f g → retract f g
             → (x y : B)
             → (g (x +B y) ≡ (g x +A g y))
  isMorphInv g sect retr x y =
       cong g (cong₂ _+B_ (sym (sect x)) (sym (sect y)))
    ∙∙ cong g (sym (f-hom (g x) (g y)))
    ∙∙ retr (g x +A g y)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical