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

open import lib.Basics
open import lib.NType2
open import lib.Equivalence2
open import lib.NConnected
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.types.Group
open import lib.groups.LoopSpace
open import lib.groups.Homomorphism

module lib.types.EilenbergMacLane1 {i} where

module _ (G : Group i) where

  postulate  -- HIT
    EM₁ : Type i
    embase' : EM₁
    emloop' : Group.El G → embase' == embase'
    emloop-comp' : ∀ g₁ g₂ → emloop' (Group.comp G g₁ g₂) == emloop' g₁ ∙ emloop' g₂
    EM₁-level' : has-level ⟨ 1 ⟩ EM₁

  ⊙EM₁ : Ptd i
  ⊙EM₁ = ⊙[ EM₁ , embase' ]

module _ {G : Group i} where
  private
    module G = Group G

  embase = embase' G
  emloop = emloop' G
  emloop-comp = emloop-comp' G

  instance
    EM₁-level : {n : ℕ₋₂} → has-level (S (S (S n))) (EM₁ G)
    EM₁-level {⟨-2⟩} = EM₁-level' G
    EM₁-level {S n} = raise-level _ EM₁-level

  abstract
    -- This was in the original paper, but is actually derivable.
    emloop-ident : emloop G.ident == idp
    emloop-ident = ! $ anti-whisker-right (emloop G.ident) $
      ap emloop (! $ G.unit-r G.ident) ∙ emloop-comp G.ident G.ident

  module EM₁Elim {j} {P : EM₁ G → Type j}
    {{_ : (x : EM₁ G) → has-level ⟨ 1 ⟩ (P x)}}
    (embase* : P embase)
    (emloop* : (g : G.El) → embase* == embase* [ P ↓ emloop g ])
    (emloop-comp* : (g₁ g₂ : G.El) →
       emloop* (G.comp g₁ g₂) == emloop* g₁ ∙ᵈ emloop* g₂
       [ (λ p → embase* == embase* [ P ↓ p ]) ↓ emloop-comp g₁ g₂ ])
    where

    postulate  -- HIT
      f : Π (EM₁ G) P
      embase-β : f embase ↦ embase*
    {-# REWRITE embase-β #-}

    postulate  -- HIT
      emloop-β : (g : G.El) → apd f (emloop g) == emloop* g

  open EM₁Elim public using () renaming (f to EM₁-elim)

  module EM₁Rec {j} {C : Type j}
    {{_ : has-level ⟨ 1 ⟩ C}} (embase* : C)
    (hom* : G →ᴳ (Ω^S-group 0 ⊙[ C , embase* ])) where

    private
      module M = EM₁Elim {P = λ _ → C}
        embase* (λ g → ↓-cst-in (GroupHom.f hom* g))
        (λ g₁ g₂ → ↓-cst-in2 (GroupHom.pres-comp hom* g₁ g₂)
                 ∙'ᵈ ↓-cst-in-∙ (emloop g₁) (emloop g₂)
                      (GroupHom.f hom* g₁) (GroupHom.f hom* g₂))

    f = M.f

    emloop-β : (g : G.El) → ap f (emloop g) == GroupHom.f hom* g
    emloop-β g = apd=cst-in {f = f} (M.emloop-β g)

  open EM₁Rec public using () renaming (f to EM₁-rec)

-- basic lemmas about [EM₁]

module _ {G : Group i} where
  private
    module G = Group G

  abstract
    emloop-inv : ∀ g → emloop' G (G.inv g) == ! (emloop g)
    emloop-inv g = cancels-inverse _ _ lemma
      where
        cancels-inverse : ∀ {i} {A : Type i} {x y : A}
          (p : x == y) (q : y == x) → p ∙ q == idp → p == ! q
        cancels-inverse p idp r = ! (∙-unit-r p) ∙ r

        lemma : emloop' G (G.inv g) ∙ emloop g  == idp
        lemma = ! (emloop-comp (G.inv g) g) ∙ ap emloop (G.inv-l g) ∙ emloop-ident

    {- EM₁ is 0-connected -}
    instance
      EM₁-conn : is-connected 0 (EM₁ G)
      EM₁-conn = has-level-in ([ embase ] , Trunc-elim
        (EM₁-elim
          {P = λ x → [ embase ] == [ x ]}
          {{λ _ → raise-level _ (=-preserves-level Trunc-level)}}
          idp
          (λ _ → prop-has-all-paths-↓)
          (λ _ _ → set-↓-has-all-paths-↓)))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --prop --show-irrelevant #-}

open import Agda.Builtin.Equality

postulate
  A : Set
  P : Prop
  f : P → A
  g : A → P

{-# TERMINATING #-}
loop : A → A
loop y = loop y

mutual
  X : A
  X = _

  test : ∀ y → X ≡ f (g (loop y))
  test y = refl

-- The occurs check should not try to normalize the argument `loop y`
-- because it only appears in an irrelevant context.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Type

module Relator.Congruence {ℓ₁}{ℓ₂} {X : Type{ℓ₁}}{Y : Type{ℓ₂}} where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Relator.Equals

-- The congruence relation with respect to a relation
infixl 15 _≅_of_
data _≅_of_ (x₁ : X) (x₂ : X) (f : X → Y) : Stmt{ℓ₂} where
  [≅]-intro : (f(x₁) ≡ f(x₂)) → (x₁ ≅ x₂ of f)

[≅]-elim : ∀{x₁ x₂ : X}{f : X → Y} → (x₁ ≅ x₂ of f) → (f(x₁) ≡ f(x₂))
[≅]-elim ([≅]-intro eq) = eq

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module PointedPi where

open import Level using (_⊔_) renaming (zero to l0; suc to lsuc)
open import Universe using (Universe)

open import Categories.Category using (Category)
open import Categories.Groupoid using (Groupoid)
open import Categories.Functor using (Functor)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum hiding ([_,_])
open import Data.Product
open import Relation.Binary.PropositionalEquality as P
open import Function using (flip)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Properties.Simple using (+-right-identity)
open import Data.Integer using (ℤ;+_;-[1+_]) renaming (suc to ℤsuc; -_ to ℤ-; _+_ to _ℤ+_)

open import Data.List using (List; foldr; replicate; _++_) renaming (map to Lmap; [] to nil; _∷_ to _∷:_)
open import Data.List.Any using (module Membership-≡; here; there)
open Membership-≡
open import Data.List.Properties using ()

open import Categories.Groupoid.Sum using () renaming (Sum to GSum)
open import Categories.Groupoid.Product using () renaming (Product to GProduct)

open import PiU using (U; ZERO; ONE; PLUS; TIMES; toℕ)
open import PiLevel0
open import PiLevel1
open import PiEquiv renaming (eval to ap; evalB to apB)
open import Equiv

open import PiIter

data Pointed (t : U) : Set where
  ∙ : ⟦ t ⟧ → Pointed t

-- yes, re-use name eval on purpose here
eval : {t₁ t₂ : U} → (t₁ ⟷ t₂) → Pointed t₁ → Pointed t₂
eval c (∙ x) = ∙ (ap c x)

-- all our values will be 'subtypes' of this:
record V (t : U) : Set where
  constructor v
  field
    pt : ⟦ t ⟧
    auto : t ⟷ t

evalV : {t₁ t₂ : U} → (t₁ ⟷ t₂) → V t₁ → V t₂
evalV c (v pt auto) = v (ap c pt) (! c ◎ auto ◎ c)

-- V equivalence
record _≈_ {t : U} (a : V t) (b : V t) : Set where
  constructor veq
  field
    pt-eq : V.pt a P.≡ V.pt b
    auto-eq : V.auto a ⇔ V.auto b

-- and in general, all our morphisms will be 'subtypes' of
record H {s t : U} (a : V s) (b : V t) : Set where
  constructor mor
  field
    transp : s ⟷ t
    t-eq : evalV transp a ≈ b

--- Generating sets: lists of combinators over a type
GenSet : U → Set
GenSet t = List (t ⟷ t)

-- We will need to use a choice between 3 things.  Don't want
-- to abuse ⊎.  The 3 things can be understood as
-- Forward, Backward and Neutral.  So we name it ⇕.
infix 30 _⇕_

data _⇕_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  Fwd : (x : A) → A ⇕ B
  Bwd : (y : B) → A ⇕ B
  Neu :           A ⇕ B

-- note that this uses ≡ (inside ∈), not ⇔.  On purpose.
inGS : {t : U} → GenSet t → Set
inGS {t} S = Σ (t ⟷ t) (λ p → (p ∈ S) ⇕ (p ∈ S))

-- flip a ⇕
flip⇕ : ∀ {a b} {A : Set a} {B : Set b} → A ⇕ B → B ⇕ A
flip⇕ (Fwd x) = Bwd x
flip⇕ (Bwd y) = Fwd y
flip⇕ Neu = Neu

-- type of sequences of applications from GenSet
CombS : {t : U} → GenSet t → Set
CombS {t} S = List ( inGS S )

extract : {t : U} {S : GenSet t} → inGS S → (t ⟷ t)
extract (p , Fwd x) = p
extract (p , Bwd y) = ! p
extract (p , Neu  ) = id⟷

interp : {t : U} {S : GenSet t} → CombS S → (t ⟷ t)
interp l = foldr _◎_ id⟷ (Lmap extract l)

-- the combinator (CombS S) acts as a sort of reference point
data U↑ : Set where
  ↑ : U → U↑
  # : {τ : U} → (S : GenSet τ) → CombS S → U↑
  1/ : {τ : U} → (S : GenSet τ) → CombS S → U↑
  _⊞_ : U↑ → U↑ → U↑
  _⊠_ : U↑ → U↑ → U↑

infix 40 _⇿_

data _⇿_ : U↑ → U↑ → Set where
  ↑ : {t₁ t₂ : U} → t₁ ⟷ t₂  → ↑ t₁ ⇿ ↑ t₂
  ev : {t₁ : U} {S : GenSet t₁} → (q : CombS S) → ((# S q) ⊠ (1/ S q)) ⇿ ↑ ONE
  coev : {t₁ : U} {S : GenSet t₁} → (q : CombS S) → ↑ ONE ⇿ ((# S q) ⊠ (1/ S q))
  id⇿ : {t₁ : U↑} → t₁ ⇿ t₁ -- needed for coev of ⊠

UG : Universe l0 (lsuc l0)
UG = record {
    U = U↑
 ;  El = λ T → Σ[ ℂ ∈ Category l0 l0 l0 ] (Groupoid ℂ)
 }

-- for convenience, create some types which are embedable into V
D : U → Set
D t = ⟦ t ⟧

embedD : {t : U} → D t → V t
embedD w = v w id⟷

-- and D equality lifts to ≈
embedDeq : {τ : U} → (s t : D τ) → s ≡ t → embedD s ≈ embedD t
embedDeq s .s P.refl = veq P.refl id⇔

-- even more to the point, it lifts to describing Hom sets
-- note how we can't use embedDeq directly!
embedDHom : {τ : U} → (s t : D τ) → s ≡ t → H (embedD s) (embedD t)
embedDHom s .s P.refl = mor id⟷ (veq P.refl (trans⇔ idl◎l idl◎l))

-- this is the same as in 2DTypes/groupoid
discreteC : U → Category _ _ _
discreteC t = record {
     Obj = D t
    ; _⇒_ = λ s₁ s₂ → s₁ P.≡ s₂ -- see embedDHom
    ; _≡_ = λ _ _ → ⊤ -- hard-code proof-irrelevance
    ; id = P.refl
    ; _∘_ = flip P.trans
    ; assoc = tt
    ; identityˡ = tt
    ; identityʳ = tt
    ; equiv = record { refl = tt ; sym = λ _ → tt ; trans = λ _ _ → tt }
    ; ∘-resp-≡ = λ _ _ → tt
    }
-- ditto
discreteG : (t : U) → Groupoid (discreteC t)
discreteG S = record
  { _⁻¹ = λ { {A} {.A} refl → P.refl }
  ; iso = record { isoˡ = tt; isoʳ = tt }
  }

-----------

--- Structure theorems for ⇕
extract-GS[]≡id⟷ : ∀ {t : U} → (gs : GenSet t) → gs ≡ nil →
  (∀ (y : inGS gs) → extract y ≡ id⟷)
extract-GS[]≡id⟷ .nil refl (p , Fwd ())
extract-GS[]≡id⟷ .nil refl (p , Bwd ())
extract-GS[]≡id⟷ .nil refl (p , Neu) = refl

private
  Iter→CombS :  ∀ {τ : U} (c : τ ⟷ τ) → Iter c → CombS (c ∷: nil)
  Iter→CombS p (iter (+_ n) _ _) = replicate n (p , Fwd (here refl))
  Iter→CombS p (iter (-[1+_] n) _ _) = replicate (suc n) (p , Bwd (here refl))

  CombS→Iter : ∀ {τ : U} (c : τ ⟷ τ) → CombS (c ∷: nil) → Iter c
  CombS→Iter p nil = iter (+ 0) id⟷ id⇔
  CombS→Iter p (x ∷: xs) with CombS→Iter p xs
  CombS→Iter p ((.p , Fwd (here refl)) ∷: xs) | iter i q pf =
      iter (ℤsuc i) (p ◎ q) (trans⇔ (id⇔ ⊡ pf)
        (trans⇔ (idr◎r ⊡ id⇔) (2! (lower (+ 1) i))))
  CombS→Iter p ((p' , Fwd (there ())) ∷: xs) | iter i q pf
  CombS→Iter p ((.p , Bwd (here refl)) ∷: xs) | iter i q pf =
     iter (i ℤ+ -[1+ 0 ]) (q ◎ (! p))
       (trans⇔ (pf ⊡ id⇔) (2! (lower i -[1+ 0 ])))
  CombS→Iter p ((p' , Bwd (there ())) ∷: xs) | iter i q pf
  CombS→Iter p ((p' , Neu) ∷: xs) | iter i q pf = iter i q pf

  -- split Fwd case from Bwd
  preserve-iter : ∀ {τ : U} (c : τ ⟷ τ) → (n : ℕ) →
    let p = CombS→Iter c (replicate n (c , Fwd (here refl))) in
    Iter.i p ≡ + n
  preserve-iter c zero = refl
  preserve-iter c (suc n) = cong ℤsuc (preserve-iter c n)

  preserve-iterB : ∀ {τ : U} (c : τ ⟷ τ) → (n : ℕ) →
    let p = CombS→Iter c (replicate (suc n) (c , Bwd (here refl))) in
    Iter.i p ≡ -[1+ n ]
  preserve-iterB c zero = refl
  preserve-iterB c (suc i) = P.trans
    (cong (λ z → z ℤ+ -[1+ 0 ]) (preserve-iterB c i))
    (cong (λ z → -[1+ (suc z) ]) (+-right-identity i))

  P2C2P : ∀ {τ : U} (c : τ ⟷ τ) → (p : Iter c) → (CombS→Iter c (Iter→CombS c p)) ≡c p
  P2C2P c (iter (+_ zero) p' p'⇔p^i) = eqc refl (2! p'⇔p^i)
  P2C2P c (iter (+_ (suc n)) p' p'⇔p^i) with CombS→Iter c (replicate n (c , Fwd (here refl))) | P.inspect (λ nn → CombS→Iter c (replicate nn (c , Fwd (here refl)))) n
  ... | iter i q pf | [ eq ] =
    let i=n = (P.trans (cong Iter.i (P.sym eq)) (preserve-iter c n)) in
    eqc (cong ℤsuc i=n) (trans⇔ (id⇔ {c = c} ⊡ pf)
        (trans⇔ (id⇔ ⊡ P.subst (λ j → c ^ i ⇔ c ^ j) i=n (id⇔ {c = c ^ i})) (2! p'⇔p^i)))
  P2C2P c (iter (-[1+_] n) p' p'⇔p^i) with CombS→Iter c (replicate (suc n) (c , Bwd (here refl))) | P.inspect (λ nn → CombS→Iter c (replicate (suc nn) (c , Bwd (here refl)))) n
  ... | iter i q pf | [ eq ] =
    let i=n = P.trans (cong Iter.i (P.sym eq)) (preserve-iterB c n) in
    eqc i=n (trans⇔ (P.subst (λ j → q ⇔ c ^ j) i=n pf) (2! p'⇔p^i))

  C2P2C :  ∀ {τ : U} (c : τ ⟷ τ) → (q : CombS (c ∷: nil)) →
    interp (Iter→CombS c (CombS→Iter c q)) ⇔ interp q
  C2P2C c nil = id⇔
  C2P2C c (x ∷: q) with CombS→Iter c q | (C2P2C c) q
  C2P2C c ((.c , Fwd (here refl)) ∷: q) | iter (+_ n) p' pf | pf2 = id⇔ ⊡ pf2
  C2P2C c ((.c , Fwd (here refl)) ∷: q) | iter (-[1+_] zero) p' pf | pf2 =
    trans⇔ (linv◎r {c = c}) (id⇔ ⊡ trans⇔ idr◎r pf2)
  C2P2C c ((.c , Fwd (here refl)) ∷: q) | iter (-[1+_] (suc n)) p' pf | pf2 =
    trans⇔ (trans⇔ idl◎r (linv◎r ⊡ id⇔)) (trans⇔ assoc◎r (id⇔ ⊡ pf2))
  C2P2C c ((comb , Fwd (there ())) ∷: q) | iter i p' pf | pf2
  C2P2C c ((.c , Bwd (here refl)) ∷: q) | iter (+_ zero) p' pf | pf2 = id⇔ ⊡ pf2
  C2P2C c ((.c , Bwd (here refl)) ∷: q) | iter (+_ (suc n)) p' pf | pf2 =
    trans⇔ (trans⇔ idl◎r (rinv◎r ⊡ id⇔)) (trans⇔ assoc◎r (id⇔ ⊡ pf2))
  C2P2C c ((.c , Bwd (here refl)) ∷: q) | iter (-[1+_] n) p' pf | pf2 =
    id⇔ {c = ! c} ⊡ (P.subst (λ j → ! c ◎ foldr _◎_ id⟷ (Lmap extract (replicate j (c , Bwd (here refl)))) ⇔ foldr _◎_ id⟷ (Lmap extract q)) (P.sym (+-right-identity n)) pf2)
  C2P2C c ((comb , Bwd (there ())) ∷: q) | iter i p' pf | pf2
  C2P2C c ((comb , Neu) ∷: q) | iter i p' pf | pf2 = trans⇔ pf2 idl◎r

-- we would like to say:
--    Iter[p]≃CombS[p] : ∀ {τ : U} (p : τ ⟷ τ) → Iter p ≃ CombS (p ∷: nil)
-- but the homotopies have the wrong type (≡ rather than ≡c and ⇔).

-----------
-- Generalization of # p to # S.

orderC : {τ : U} → (S : GenSet τ) → Category _ _ _
orderC {τ} S = record {
     Obj = CombS S
   ; _⇒_ = λ q₁ q₂ → interp q₁ ⇔ interp q₂
   ; _≡_ = λ _ _ → ⊤
   ; id = id⇔
   ; _∘_ = flip trans⇔
   ; assoc = tt
   ; identityˡ = tt
   ; identityʳ = tt
   ; equiv = record { refl = tt; sym = λ _ → tt; trans = λ _ _ → tt }
   ; ∘-resp-≡ = λ _ _ → tt
   }

orderG : {τ : U} → (S : GenSet τ) → Groupoid (orderC S)
orderG {τ} S = record {
    _⁻¹ = 2!
  ; iso = record {
        isoˡ = tt
      ; isoʳ = tt
      }
  }

commute-interp-++ : ∀ {τ : U} {S : GenSet τ} (f g : CombS S) →
  interp (f ++ g) ⇔ interp f ◎ interp g
commute-interp-++ nil g = idl◎r
commute-interp-++ (x ∷: f) g = trans⇔ (id⇔ ⊡ commute-interp-++ f g) assoc◎l

1/orderC : {τ : U} → (S : GenSet τ) → Category _ _ _
1/orderC S = record {
    Obj = ⊤
  ; _⇒_ = λ _ _ → CombS S
  ; _≡_ = λ p q → interp p ⇔ interp q
  ; id = nil
  ; _∘_ = _++_
  ; assoc = λ { {f = f} {g} {h} → trans⇔ (commute-interp-++ (h ++ g) f) (
      trans⇔ (commute-interp-++ h g ⊡ id⇔) (
      trans⇔ assoc◎r (
      trans⇔ (id⇔ ⊡ (2! (commute-interp-++ g f))) (
              2! (commute-interp-++ h (g ++ f)))))) }
  ; identityˡ = id⇔ -- could also use idl◎l like below
  ; identityʳ = λ { {f = f} → trans⇔ (commute-interp-++ f nil) idr◎l }
  ; equiv = record { refl = id⇔ ; sym = 2! ; trans = trans⇔ }
  ; ∘-resp-≡ = λ { {f = f} {h} {g} {i} f⇔h g⇔i →
      trans⇔ (commute-interp-++ f g) (trans⇔ (f⇔h ⊡ g⇔i) (2! (commute-interp-++ h i))) }
  }

flipGS : {τ : U} {S : GenSet τ} → inGS S → inGS S
flipGS (c , pf) = c , flip⇕ pf

invert-CombS : {τ : U} {S : GenSet τ} → CombS S → CombS S
invert-CombS pl = Data.List.map flipGS (Data.List.reverse pl)

-- sometimes we need to do some list manipulations under interp
lift-≡ : {t₁ t₂ : U} {p q : t₁ ⟷ t₂} → p ≡ q → p ⇔ q
lift-≡ refl = id⇔

interp-invert : {τ : U} {S : GenSet τ} → (x : inGS S) → (f : CombS S) →
  interp (invert-CombS (x ∷: f)) ⇔ interp (invert-CombS f) ◎ extract (flipGS x)
interp-invert (c , Fwd x) f = {!!}
interp-invert (c , Bwd y) f = {!!}
interp-invert (c , Neu) f = {!!}

extract-flipGS : {τ : U} {S : GenSet τ} → (x : inGS S) → extract (flipGS x) ⇔ ! (extract x)
extract-flipGS (proj₁ , Fwd x) = id⇔
extract-flipGS (proj₁ , Bwd y) = 2! !!⇔id
extract-flipGS (proj₁ , Neu) = id⇔

private
  left-invCS : {τ : U} {S : GenSet τ} (f : CombS S) → interp (invert-CombS f ++ f) ⇔ id⟷
  left-invCS nil = id⇔
  left-invCS (x ∷: f) = trans⇔
    (commute-interp-++ (invert-CombS (x ∷: f)) (x ∷: f)) (trans⇔
    (interp-invert x f ⊡ id⇔) (trans⇔
    assoc◎r (trans⇔
    (id⇔ ⊡ assoc◎l) (trans⇔
    (id⇔ ⊡ trans⇔ (trans⇔ (extract-flipGS x ⊡ id⇔) rinv◎l ⊡ id⇔) idl◎l) (trans⇔
    (2! (commute-interp-++ (invert-CombS f) f)) (left-invCS f))))))

  right-invCS : {τ : U} {S : GenSet τ} (f : CombS S) → interp (f ++ invert-CombS f) ⇔ id⟷
  right-invCS l = {!!}

1/orderG : {τ : U} → (S : GenSet τ) → Groupoid (1/orderC S)
1/orderG s = record {
    _⁻¹ = invert-CombS
  ; iso = λ {_} {_} {f} → record {
      isoˡ = left-invCS f
    ; isoʳ = right-invCS f
    }
  }

-----------
--- Our semantics into groupoids
⟦_⟧↑ : (T : U↑) → Universe.El UG T
⟦ ↑ S ⟧↑ = , discreteG S
⟦ # S q ⟧↑ = , orderG S -- the base point doesn't matter here?
⟦ 1/ S q ⟧↑ = , 1/orderG S -- ditto?
⟦ x ⊞ y ⟧↑ with ⟦ x ⟧↑ | ⟦ y ⟧↑
... | (_ , G₁) | (_ , G₂) = , GSum G₁ G₂
⟦ x ⊠ y ⟧↑ with ⟦ x ⟧↑ | ⟦ y ⟧↑
... | (_ , G₁) | (_ , G₂) = , GProduct G₁ G₂

record W (t : U↑) : Set where
  constructor w
  field
    pt : Category.Obj (proj₁ ⟦ t ⟧↑)
    auto : Category._⇒_ (proj₁ ⟦ t ⟧↑) pt pt

evalW : {s t : U↑} → s ⇿ t → W s → W t
evalW (↑ x) (w pt auto) = w (ap x pt) refl
evalW (ev q) (w (cc , tt) (cc⇔cc-pf , cc')) = w tt refl -- this is cheating, cc <=> cc' ??
evalW (coev q) (w tt refl) = w (q , tt) (id⇔ , q) -- but this isn't.
evalW id⇿ (w pt auto) = w pt auto

-- This should actually be Hom-set inhabitation, aka categorical equivalence
-- (as we are in a groupoid setting).
ObjEq : (t : U↑) → Category.Obj (proj₁ ⟦ t ⟧↑) → Category.Obj (proj₁ ⟦ t ⟧↑) → Set
ObjEq (↑ x) a b = a P.≡ b
ObjEq (# S x) a b = interp a ⇔ interp b
ObjEq (1/ S x) a b = ⊤
ObjEq (s ⊞ t) (inj₁ x) (inj₁ y) = ObjEq s x y
ObjEq (s ⊞ t) (inj₁ x) (inj₂ y) = ⊥
ObjEq (s ⊞ t) (inj₂ y) (inj₁ x) = ⊥
ObjEq (s ⊞ t) (inj₂ x) (inj₂ y) = ObjEq t x y
ObjEq (s ⊠ t) (a , b) (c , d) = ObjEq s a c × ObjEq t b d

HomEq : (t : U↑) → (a b : Category.Obj (proj₁ ⟦ t ⟧↑)) →
  Category._⇒_ (proj₁ ⟦ t ⟧↑) a b → Category._⇒_ (proj₁ ⟦ t ⟧↑) a b → Set
HomEq (↑ x) a b h1 h2 = ⊤ -- this is basically proof-irrelevance h1 h2
HomEq (# S x) a b h1 h2 = ⊤ -- because h1 and h2 are the exact same ⇔
HomEq (1/ S x) tt tt h1 h2 = interp h1 ⇔ interp h2 -- here!
HomEq (s ⊞ t) (inj₁ x) (inj₁ x₁) h1 h2 = HomEq s x x₁ h1 h2
HomEq (s ⊞ t) (inj₁ x) (inj₂ y) (Level.lift ()) h2
HomEq (s ⊞ t) (inj₂ y) (inj₁ x) (Level.lift ()) h2
HomEq (s ⊞ t) (inj₂ y) (inj₂ y₁) h1 h2 = HomEq t y y₁ h1 h2
HomEq (s ⊠ t) (a , b) (c , d) (a⇒c , b⇒d) (a⇒c' , b⇒d') =
  HomEq s a c a⇒c a⇒c' × HomEq t b d b⇒d b⇒d'

-- W equivalence; note that transp is restricted to be the Homs of cat
--   we might want to restrict that more.
record _≈W_ {t : U↑} (a : W t) (b : W t) : Set where
  constructor weq
  cat = proj₁ ⟦ t ⟧↑
  gpd = proj₂ ⟦ t ⟧↑
  _∘_ = Category._∘_ cat
  field
    pt-eq : ObjEq t (W.pt a) (W.pt b)
    transp : Category._⇒_ cat (W.pt a) (W.pt b)
    auto-eq : HomEq t (W.pt a) (W.pt b) (W.auto b ∘ (transp ∘ (W.auto a))) transp

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module AssocList where

open import Cubical.Core.Everything using (Type)

open import Data.Bool       using (Bool; false; true; _∨_; _∧_)
open import Data.List       using (List; []; _∷_; foldr)
open import Data.Product    using (_×_; _,_; proj₂)

open import Function        using (_∘_)

AList : (A B : Type) → Type
AList A B = List (A × List B)

-- Does not deduplicate in list of B.
insert : {A B : Type} → (A → A → Bool) → A × B → AList A B → AList A B
insert eq (a , b) []       = (a , b ∷ []) ∷ []
insert eq (a , b) ((a' , bs) ∷ xs) with eq a a'
... | false = (a' , bs)     ∷ insert eq (a , b) xs
... | true  = (a' , b ∷ bs) ∷ xs

lookup : {A B : Type} → (A → A → Bool) → A → AList A B → List B
lookup eq _ []               = []
lookup eq a ((a' , bs) ∷ xs) with eq a a'
... | false = lookup eq a xs
... | true  = bs

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
-- Empty, unit and equality.

⊥ = (X : Set) → X
⊤ = (X : Set) → X → X

data _≡_ {l}{A : Set l}(x : A) : A → Set l where
  <> : x ≡ x

-- The fixpoint of the identity functor as a data definition.

module Data where

  data μId : Set where
    In : μId → μId

-- μId can be proved empty. Here are both a direct proof and one that
-- relies on the eliminator for μId.

  ¬μId : μId → ⊥
  ¬μId (In x) = ¬μId x

  μId-elim : ∀ {l}(P : μId → Set l) → (∀ x → P x → P (In x)) → ∀ x → P x
  μId-elim P m (In x) = m x (μId-elim P m x)

  ¬Id' : μId → ⊥
  ¬Id' = μId-elim (λ _ → ⊥) (λ _ p → p)

-- To prove ∀ x → ¬ (x ≡ In x) it is enough to call ¬μId (or ¬μId'): the
-- equality proof is not inspected.

  ¬id≡In-empty : ∀ {x} → x ≡ In x → ⊥
  ¬id≡In-empty {x} _ = ¬μId x -- or ¬Id' x

-- Alternatively, one could use an absurd pattern which relies on the
-- presence of a cycle.

  ¬id≡In-pm : ∀ {x} → x ≡ In x → ⊥
  ¬id≡In-pm ()

-- The case of inductive records is a bit different. Here is the fixpoint
-- of the identity functor as an inductive record definition.

module Record where

  record μId : Set where
    inductive
    constructor In
    field       Out : μId
  open μId

-- It does not seem possible to prove Record.μId empty, as Agda does not
-- consider the following definitions as terminating.

  {-# NON_TERMINATING #-}
  ¬μId : μId → ⊥
  ¬μId (In x) = ¬μId x

  {-# NON_TERMINATING #-}
  μId-elim : ∀ {l}(P : μId → Set l) → (∀ x → P x → P (In x)) → ∀ x → P x
  μId-elim P m (In x) = m x (μId-elim P m x)

  ¬Id' : μId → ⊥
  ¬Id' = μId-elim (λ _ → ⊥) (λ _ p → p)

  ¬id≡In-empty : ∀ {x} → x ≡ In x → ⊥
  ¬id≡In-empty {x} _ = ¬μId x -- or ¬Id' x

-- However, we can still use an absurd pattern as in Data.¬id≡In-pm.

  ¬id≡In-pm : ∀ {x} → x ≡ In x → ⊥
  ¬id≡In-pm ()

-- This should not be possible.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- Vectors, defined using an inductive family
------------------------------------------------------------------------

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

open import Equality

module Vec.Data
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Function-universe eq hiding (_∘_)
open import List eq using (length)
open import Surjection eq using (_↠_; ↠-≡)

------------------------------------------------------------------------
-- The type

-- Vectors.

infixr 5 _∷_

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

------------------------------------------------------------------------
-- Some simple functions

-- Finds the element at the given position.

index : ∀ {n} {a} {A : Type a} → Vec A n → Fin n → A
index (x ∷ _)  fzero    = x
index (_ ∷ xs) (fsuc i) = index xs i

-- Updates the element at the given position.

infix 3 _[_≔_]

_[_≔_] : ∀ {n} {a} {A : Type a} → Vec A n → Fin n → A → Vec A n
_[_≔_] []       ()       _
_[_≔_] (x ∷ xs) fzero    y = y ∷ xs
_[_≔_] (x ∷ xs) (fsuc i) y = x ∷ (xs [ i ≔ y ])

-- Applies the function to every element in the vector.

map : ∀ {n a b} {A : Type a} {B : Type b} → (A → B) → Vec A n → Vec B n
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

-- Constructs a vector containing a certain number of copies of the
-- given element.

replicate : ∀ {n a} {A : Type a} → A → Vec A n
replicate {zero}  _ = []
replicate {suc _} x = x ∷ replicate x

-- The head of the vector.

head : ∀ {n a} {A : Type a} → Vec A (suc n) → A
head (x ∷ _) = x

-- The tail of the vector.

tail : ∀ {n a} {A : Type a} → Vec A (suc n) → Vec A n
tail (_ ∷ xs) = xs

------------------------------------------------------------------------
-- Conversions to and from lists

-- Vectors can be converted to lists.

to-list : ∀ {n} {a} {A : Type a} → Vec A n → List A
to-list  []        = []
to-list (x ∷ xs) = x ∷ to-list xs

-- Lists can be converted to vectors.

from-list : ∀ {a} {A : Type a} (xs : List A) → Vec A (length xs)
from-list []       = []
from-list (x ∷ xs) = x ∷ from-list xs

-- ∃ (Vec A) is isomorphic to List A.

∃Vec↔List : ∀ {a} {A : Type a} → ∃ (Vec A) ↔ List A
∃Vec↔List {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = to-list ∘ proj₂
      ; from = λ xs → length xs , from-list xs
      }
    ; right-inverse-of = to∘from
    }
  ; left-inverse-of = uncurry from∘to
  }
  where
  to∘from : (xs : List A) → to-list (from-list xs) ≡ xs
  to∘from []       = refl _
  to∘from (x ∷ xs) = cong (x ∷_) (to∘from xs)

  tail′ : A → ∃ (Vec A) ↠ ∃ (Vec A)
  tail′ y = record
    { logical-equivalence = record
      { to   = λ where
                 (suc n , _ ∷ xs) → n , xs
                 xs@(zero , _)    → xs
      ; from = Σ-map suc (y ∷_)
      }
    ; right-inverse-of = refl
    }

  from∘to :
    ∀ n (xs : Vec A n) →
    (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs)
  from∘to zero    []       = refl _
  from∘to (suc n) (x ∷ xs) =                                    $⟨ from∘to n xs ⟩
    (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs)   ↝⟨ _↠_.from $ ↠-≡ (tail′ x) ⟩□

    (length (to-list (x ∷ xs)) , from-list (to-list (x ∷ xs)))
      ≡
    (suc n , x ∷ xs)                                            □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import Categories.Category
open import Categories.Object.Zero

-- Kernels of morphisms.
-- https://ncatlab.org/nlab/show/kernel
module Categories.Object.Kernel {o ℓ e} {𝒞 : Category o ℓ e} (zero : Zero 𝒞) where

open import Level using (_⊔_)

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
  hiding (glue)

open Category 𝒞
open Zero zero

open HomReasoning

private
  variable
    A B X : Obj
    f h i j k : A ⇒ B

-- Note: We could define Kernels directly as equalizers or as pullbacks, but it seems somewhat
-- cleaner to just define them "as is" to avoid mucking about with extra morphisms that can
-- get in the way. For example, if we defined them as 'Pullback f !' then our 'p₂' projection
-- would _always_ be trivially equal to '¡ : K ⇒ zero'.

record IsKernel {A B K} (k : K ⇒ A) (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    commute : f ∘ k ≈ zero⇒
    universal : ∀ {X} {h : X ⇒ A} → f ∘ h ≈ zero⇒ → X ⇒ K
    factors : ∀ {eq : f ∘ h ≈ zero⇒} → h ≈ k ∘ universal eq
    unique : ∀ {eq : f ∘ h ≈ zero⇒} → h ≈ k ∘ i → i ≈ universal eq

  universal-resp-≈ : ∀ {eq : f ∘ h ≈ zero⇒} {eq′ : f ∘ i ≈ zero⇒} →
    h ≈ i → universal eq ≈ universal eq′
  universal-resp-≈ h≈i = unique (⟺ h≈i ○ factors)

  universal-∘ : f ∘ k ∘ h ≈ zero⇒
  universal-∘ {h = h} = begin
    f ∘ k ∘ h ≈⟨ pullˡ commute ⟩
    zero⇒ ∘ h ≈⟨ pullʳ (⟺ (¡-unique (¡ ∘ h))) ⟩
    zero⇒ ∎

record Kernel {A B} (f : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
     {kernel} : Obj
     kernel⇒ : kernel ⇒ A
     isKernel : IsKernel kernel⇒ f

  open IsKernel isKernel public

IsKernel⇒Kernel : IsKernel k f → Kernel f
IsKernel⇒Kernel {k = k} isKernel = record
  { kernel⇒ = k
  ; isKernel = isKernel
  }

max_stars_repo_name: FintanH/agda-categories

max_issues_repo_name: FintanH/agda-categories

max_forks_repo_name: FintanH/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise table equality
------------------------------------------------------------------------

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

module Data.Table.Relation.Binary.Equality where

open import Relation.Binary using (Setoid)
open import Data.Table.Base
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
  as P using (_≡_; _→-setoid_)

setoid : ∀ {c p} → Setoid c p → ℕ → Setoid _ _
setoid S n = record
  { Carrier = Table Carrier n
  ; _≈_ = λ t t′ → ∀ i → lookup t i ≈ lookup t′ i
  ; isEquivalence = record
    { refl  = λ i → refl
    ; sym   = λ p → sym ∘ p
    ; trans = λ p q i → trans (p i) (q i)
    }
  }
  where open Setoid S

≡-setoid : ∀ {a} → Set a → ℕ → Setoid _ _
≡-setoid A = setoid (P.setoid A)

module _ {a} {A : Set a} {n} where
  open Setoid (≡-setoid A n) public
    using () renaming (_≈_ to _≗_)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the ring solver with two copies of the same ring with
-- decidable equality
------------------------------------------------------------------------

open import Algebra.RingSolver.AlmostCommutativeRing
open import Relation.Binary

module Algebra.RingSolver.Simple
         {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
         (_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
         where

open AlmostCommutativeRing R
import Algebra.RingSolver as RS
open RS rawRing R (-raw-almostCommutative⟶ R) _≟_ public


text:
module Extensions.All where

open import Data.List.All


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

open import Agda.Primitive.Cubical

postulate
  A : Set
  B : Set
  b : B

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

infix 4 _≡_
_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = PathP (λ _ → A)

f : (\ {a : A} (x : B) → b) ≡ (\ _ → b)
f i x = b


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

open import lib.Base

module test.fail.Test2 where

module _ where

  private
    data #I : Type₀ where
      #zero : #I
      #one : #I

  I : Type₀
  I = #I

  zero : I
  zero = #zero

  one : I
  one = #one

  postulate
    seg : zero == one

  I-elim : ∀ {i} {P : I → Type i} (zero* : P zero) (one* : P one)
           (seg* : zero* == one* [ P ↓ seg ]) → Π I P
  I-elim {i} {P} zero* one* seg* = I-elim-aux phantom  where

    I-elim-aux : Phantom seg* → Π I P
    I-elim-aux phantom #zero = zero*
    I-elim-aux phantom #one = one*

postulate
  P : I → Type₀
  z : P zero
  o : P one
  s s' : z == o [ P ↓ seg ]

absurd : I-elim z o s == I-elim z o s'
absurd = idp

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on containers
------------------------------------------------------------------------

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

module Data.Container.Properties where

import Function as F
open import Relation.Binary

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

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

  map-identity : ∀ {x e} (X : Setoid x e) xs →
                 Eq X C (map F.id xs) xs
  map-identity X xs = refl X C

  map-compose : ∀ {x y z e} {X : Set x} {Y : Set y} (Z : Setoid z e) g (f : X → Y) xs →
                Eq Z C (map g (map f xs)) (map (g F.∘′ f) xs)
  map-compose Z g f xs = refl Z C


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRingSolver.HornerForms where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Int hiding (_+_ ; _·_ ; -_)
open import Cubical.Data.FinData
open import Cubical.Data.Vec
open import Cubical.Data.Bool

open import Cubical.Relation.Nullary.Base using (yes; no)

open import Cubical.Algebra.CommRingSolver.Utility

open import Cubical.Algebra.CommRingSolver.RawRing
open import Cubical.Algebra.CommRingSolver.IntAsRawRing
open import Cubical.Algebra.CommRingSolver.RawAlgebra renaming (⟨_⟩ to ⟨_⟩ₐ)
open import Cubical.Algebra.CommRingSolver.AlgebraExpression public

private
  variable
    ℓ ℓ' : Level

{-
  This defines the type of multivariate Polynomials over the RawRing R.
  The construction is based on the algebraic fact

    R[X₀][X₁]⋯[Xₙ] ≅ R[X₀,⋯,Xₙ]

  BUT: Contrary to algebraic convetions, we will give 'Xₙ' the lowest index
  in the definition of 'Variable' below. So if 'Variable n R k' is identified
  with 'Xₖ', then the RawRing we construct should rather be denoted with

    R[Xₙ][Xₙ₋₁]⋯[X₀]

  or, to be precise about the evaluation order:

    (⋯((R[Xₙ])[Xₙ₋₁])⋯)[X₀]

-}

data IteratedHornerForms (A : RawAlgebra ℤAsRawRing ℓ) : ℕ → Type ℓ where
  const : ℤ → IteratedHornerForms A ℕ.zero
  0H : {n : ℕ} → IteratedHornerForms A (ℕ.suc n)
  _·X+_ : {n : ℕ} → IteratedHornerForms A (ℕ.suc n) → IteratedHornerForms A n
                  → IteratedHornerForms A (ℕ.suc n)

{-
  The following function returns true, if there is some
  obvious reason that the Horner-Expression should be zero.
  Since Equality is undecidable in a general RawAlgebra, we cannot
  have a function that fully lives up to the name 'isZero'.
-}
module _ (A : RawAlgebra ℤAsRawRing ℓ) where
  open RawRing ℤAsRawRing
  isZero : {n : ℕ} → IteratedHornerForms A n
                   → Bool
  isZero (const (pos ℕ.zero)) = true
  isZero (const (pos (ℕ.suc _))) = false
  isZero (const (negsuc _)) = false
  isZero 0H = true
  isZero (P ·X+ Q) = (isZero P) and (isZero Q)

  leftIsZero : {n : ℕ}
               (P : IteratedHornerForms A (ℕ.suc n))
               (Q : IteratedHornerForms A n)
               → isZero (P ·X+ Q) ≡ true
               → isZero P ≡ true
  leftIsZero P Q isZeroSum with isZero P
  ... | true = refl
  ... | false = byBoolAbsurdity (fst (extractFromAnd _ _ isZeroSum))

  rightIsZero : {n : ℕ}
               (P : IteratedHornerForms A (ℕ.suc n))
               (Q : IteratedHornerForms A n)
               → isZero (P ·X+ Q) ≡ true
               → isZero Q ≡ true
  rightIsZero P Q isZeroSum with isZero Q
  ... | true = refl
  ... | false = byBoolAbsurdity (snd (extractFromAnd _ _ isZeroSum))

module IteratedHornerOperations (A : RawAlgebra ℤAsRawRing ℓ) where
  open RawRing ℤAsRawRing

  private
    1H' : (n : ℕ) → IteratedHornerForms A n
    1H' ℕ.zero = const 1r
    1H' (ℕ.suc n) = 0H ·X+ 1H' n

    0H' : (n : ℕ) → IteratedHornerForms A n
    0H' ℕ.zero = const 0r
    0H' (ℕ.suc n) = 0H

  1ₕ : {n : ℕ} → IteratedHornerForms A n
  1ₕ {n = n} = 1H' n

  0ₕ : {n : ℕ} → IteratedHornerForms A n
  0ₕ {n = n} = 0H' n

  X : (n : ℕ) (k : Fin n) → IteratedHornerForms A n
  X (ℕ.suc m) zero = 1ₕ ·X+ 0ₕ
  X (ℕ.suc m) (suc k) = 0ₕ ·X+ X m k

  _+ₕ_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
               → IteratedHornerForms A n
  (const r) +ₕ (const s) = const (r + s)
  0H +ₕ Q = Q
  (P ·X+ r) +ₕ 0H = P ·X+ r
  (P ·X+ r) +ₕ (Q ·X+ s) =
    let left = (P +ₕ Q)
        right = (r +ₕ s)
    in if ((isZero A left) and (isZero A right))
       then 0ₕ
       else left ·X+ right

  -ₕ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
  -ₕ (const x) = const (- x)
  -ₕ 0H = 0H
  -ₕ (P ·X+ Q) = (-ₕ P) ·X+ (-ₕ Q)

  _⋆_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A (ℕ.suc n)
                → IteratedHornerForms A (ℕ.suc n)
  _·ₕ_ : {n : ℕ} → IteratedHornerForms A n → IteratedHornerForms A n
                → IteratedHornerForms A n
  r ⋆ 0H = 0H
  r ⋆ (P ·X+ Q) =
    if (isZero A r)
    then 0ₕ
    else (r ⋆ P) ·X+ (r ·ₕ Q)

  const x ·ₕ const y = const (x · y)
  0H ·ₕ Q = 0H
  (P ·X+ Q) ·ₕ S =
     let
        z = (P ·ₕ S)
     in if (isZero A z)
        then (Q ⋆ S)
        else (z ·X+ 0ₕ) +ₕ (Q ⋆ S)

  isZeroPresLeft⋆ :
    {n : ℕ}
    (r : IteratedHornerForms A n)
    (P : IteratedHornerForms A (ℕ.suc n))
    → isZero A r ≡ true
    → isZero A (r ⋆ P) ≡ true
  isZeroPresLeft⋆ r 0H isZero-r = refl
  isZeroPresLeft⋆ r (P ·X+ Q) isZero-r with isZero A r
  ...  | true = refl
  ...  | false = byBoolAbsurdity isZero-r

  isZeroPresLeft·ₕ :
    {n : ℕ} (P Q : IteratedHornerForms A n)
    → isZero A P ≡ true
    → isZero A (P ·ₕ Q) ≡ true
  isZeroPresLeft·ₕ (const (pos ℕ.zero)) (const _) isZeroP = refl
  isZeroPresLeft·ₕ (const (pos (ℕ.suc n))) (const _) isZeroP = byBoolAbsurdity isZeroP
  isZeroPresLeft·ₕ (const (negsuc n)) (const _) isZeroP = byBoolAbsurdity isZeroP
  isZeroPresLeft·ₕ 0H Q isZeroP = refl
  isZeroPresLeft·ₕ (P ·X+ Q) S isZeroSum with isZero A (P ·ₕ S) ≟ true
  ... | no p = byBoolAbsurdity (sym notZeroProd ∙ isZeroProd)
               where notZeroProd = ¬true→false _ p
                     isZeroP = extractFromAndLeft isZeroSum
                     isZeroProd = isZeroPresLeft·ₕ P S isZeroP
  ... | yes p with isZero A (P ·ₕ S)
  ...        | true = isZeroPresLeft⋆ Q S isZeroQ
                      where isZeroQ = extractFromAndRight isZeroSum
  ...        | false = byBoolAbsurdity p

  asRawRing : (n : ℕ) → RawRing ℓ
  RawRing.Carrier (asRawRing n) = IteratedHornerForms A n
  RawRing.0r (asRawRing n) = 0ₕ
  RawRing.1r (asRawRing n) = 1ₕ
  RawRing._+_ (asRawRing n) = _+ₕ_
  RawRing._·_ (asRawRing n) = _·ₕ_
  RawRing.- (asRawRing n) =  -ₕ

Variable : (n : ℕ) (R : RawAlgebra ℤAsRawRing ℓ') (k : Fin n) → IteratedHornerForms R n
Variable n R k = IteratedHornerOperations.X R n k

Constant : (n : ℕ) (R : RawAlgebra ℤAsRawRing ℓ') (r : ℤ) → IteratedHornerForms R n
Constant ℕ.zero R r = const r
Constant (ℕ.suc n) R r = IteratedHornerOperations.0ₕ R ·X+ Constant n R r

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ; _+_)
open import Data.Vec using (Vec; []; _∷_; _++_)
open import Dipsy.Polarity

module Dipsy.Base
  (FOp : {n : ℕ} (as : Vec Polarity n) (b : Polarity) → Set)
  (SOp : {n : ℕ} (as : Vec Polarity n) (b : Polarity) → Set)
  where

open import Dipsy.Form FOp public
open import Dipsy.Struct FOp SOp public

Res : Set
Res = {n₁ n₂ : ℕ}
    → {as₁ : Vec Polarity n₁}
    → {as₂ : Vec Polarity n₂}
    → {b : Polarity}
    → SOp (as₁ ++ flip b ∷ as₂) b
    → Context (flip b) b

-- we need contexts with n holes if we want to encode structuralisation properly..
-- those are functions...

max_stars_repo_name: wenkokke/Dipsy

max_issues_repo_name: wenkokke/dipsy

max_forks_repo_name: wenkokke/dipsy


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Right-biased universe-sensitive functor and monad instances for the
-- Product type.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
-- done.
------------------------------------------------------------------------

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

open import Algebra
open import Level

module Data.Product.Categorical.Right
  (a : Level) {b e} (B : RawMonoid b e) where

open import Data.Product
import Data.Product.Categorical.Right.Base as Base
open import Category.Applicative using (RawApplicative)
open import Category.Monad using (RawMonad; RawMonadT)
open import Function using (id; flip; _∘_; _∘′_)
import Function.Identity.Categorical as Id

open RawMonoid B

------------------------------------------------------------------------
-- Re-export the base contents publically

open Base Carrier a public

------------------------------------------------------------------------
-- Basic records

applicative : RawApplicative Productᵣ
applicative = record
  { pure = _, ε
  ; _⊛_  = zip id _∙_
  }

monadT : RawMonadT (_∘′ Productᵣ)
monadT M = record
  { return = pure ∘′ (_, ε)
  ; _>>=_  = λ ma f → ma >>= uncurry λ x b → map₂ (b ∙_) <$> f x
  } where open RawMonad M

monad : RawMonad Productᵣ
monad = monadT Id.monad

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {F} (App : RawApplicative {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Productᵣ (F A) → F (Productᵣ A)
  sequenceA (fa , y) = (_, y) <$> fa

  mapA : ∀ {A B} → (A → F B) → Productᵣ A → F (Productᵣ B)
  mapA f = sequenceA ∘ map₁ f

  forA : ∀ {A B} → Productᵣ A → (A → F B) → F (Productᵣ B)
  forA = flip mapA

module _ {M} (Mon : RawMonad {a ⊔ b} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {A} → Productᵣ (M A) → M (Productᵣ A)
  sequenceM = sequenceA App

  mapM : ∀ {A B} → (A → M B) → Productᵣ A → M (Productᵣ B)
  mapM = mapA App

  forM : ∀ {A B} → Productᵣ A → (A → M B) → M (Productᵣ B)
  forM = forA App


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

module Rings.IntegralDomains.Examples where


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

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

module Algebra.FunctionProperties.Consequences.Propositional
  {a} {A : Set a} where

{-# WARNING_ON_IMPORT
"Algebra.FunctionProperties.Consequences.Propositional was deprecated in v1.3.
Use Algebra.Consequences.Propositional instead."
#-}

open import Algebra.Consequences.Propositional {A = A} public


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Basic implementation of weight-biased leftist heap. No proofs    --
-- and no dependent types. Uses a two-pass merging algorithm.       --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module TwoPassMerge.NoProofs where

open import Basics.Nat
open import Basics hiding (_≥_)
open import Sized

-- Weight biased leftist heap is implemented using a binary tree. I
-- will interchangeably refer to children of a node as "subtrees" or
-- "subheaps".
--
-- A Heap usually stores elements of some type (Set) A with an
-- assigned priority. However to keep code easier to read each node
-- will only store Priority (a natural number). This will not affect
-- in any way proofs that we are conducting.

-- We begin with a simple implementation that uses no dependent
-- types. Note the we explicitly store rank in node constructor
-- (recall that rank is defined as number of elements in a
-- tree). Theoretically this information is redundant - we could
-- compute the size of a tree whenever we need it. The reason I choose
-- to store it in a node is that later, when we come to proving the
-- rank invariant, it will be instructive to show how information
-- stored inside a constructor is turned into an inductive family
-- index.

-- One more thing to note is that we will define most of our Heaps to
-- be sized types, ie. to use an implict index that defines how a
-- constructor affects the inductive size of the data structure. This
-- information is used to guide the termination checker in the
-- definitions of merge.
data Heap : {i : Size} → Set where
  empty : {i : Size} → Heap {↑ i}
  node  : {i : Size} → Priority → Rank → Heap {i} → Heap {i} → Heap {↑ i}

-- Returns rank of node.
rank : Heap → Nat
rank empty          = zero
rank (node _ r _ _) = r

-- Creates heap containing a single element with a given Priority
singleton : Priority → Heap
singleton p = node p one empty empty

-- Note [Two-pass merging algorithm]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We use a two-pass implementation of merging algorithm. One pass,
-- implemented by merge, performs merging in a top-down manner. Second
-- one, implemented by makeT, ensures that rank invariant of weight
-- biased leftist tree is not violated after merging.
--
-- Notation:
--
--  h1, h2 - heaps being merged
--  p1, p2 - priority of root element in h1 and h2
--  l1     - left  subtree in the first  heap
--  r1     - right subtree in the first  heap
--  l2     - left  subtree in the second heap
--  r2     - right subtree in the second heap
--
-- Merge function analyzes four cases. Two of them are base cases:
--
--    a) h1 is empty - return h2
--
--    b) h2 is empty - return h1
--
-- The other two form the inductive definition of merge:
--
--    c) priority p1 is higher than p2 - p1 becomes new root, l1
--       becomes its one child and result of merging r1 with h2
--       becomes the other child:
--
--               p1
--              /  \
--             /    \
--            l1  r1+h2 -- here "+" denotes merging
--
--    d) priority p2 is higher than p2 - p2 becomes new root, l2
--       becomes its one child and result of merging r2 with h1
--       becomes the other child.
--
--               p2
--              /  \
--             /    \
--            l2  r2+h1
--
-- Note that there is no guarantee that rank of r1+h2 (or r2+h1) will
-- be smaller than rank of l1 (or l2). To ensure that merged heap
-- maintains the rank invariant we pass both childred - ie. either l1
-- and r1+h2 or l2 and r2+h1 - to makeT, which creates a new node by
-- inspecting sizes of children and swapping them if necessary.

-- makeT takes an element (priority) and two heaps (trees). It
-- constructs a new heap with element at the root and two heaps as
-- children. makeT ensures that WBL heap rank invariant is maintained
-- in the newly created tree by reversing left and right subtrees when
-- necessary (note the inversed r and l in the last case of makeT).
makeT : Priority → Heap → Heap → Heap
makeT p l r with rank l ≥ rank r
makeT p l r | true  = node p (suc (rank l + rank r)) l r
makeT p l r | false = node p (suc (rank l + rank r)) r l

-- merge combines two heaps into one. There are two base cases and two
-- recursive cases - see [Two-pass Merging algorithm]. Recursive cases
-- call makeT to ensure that rank invariant is maintained after
-- merging.
merge : {i j : Size} → Heap {i} → Heap {j} → Heap
merge empty h2 = h2
merge h1 empty = h1
merge (node p1 h1-r l1 r1) (node p2 h2-r l2 r2)
  with p1 < p2
merge (node p1 h1-r l1 r1) (node p2 h2-r l2 r2)
  | true  = makeT p1 l1 (merge r1 (node p2 h2-r l2 r2))
merge (node p1 h1-r l1 r1) (node p2 h2-r l2 r2)
  | false = makeT p2 l2 (merge (node p1 h1-r l1 r1) r2)

-- Inserting into a heap is performed by merging that heap with newly
-- created singleton heap.
insert : Priority → Heap → Heap
insert p h = merge (singleton p) h

-- findMin returns element with highest priority, ie. root
-- element. Here we encounter first serious problem: we can't return
-- anything for empty node. If this was Haskell we could throw an
-- error, but Agda is a total language. This means that every program
-- written in Agda eventually terminates and produces a
-- result. Throwing errors is not allowed.
findMin : Heap → Priority
findMin empty          = {!!}  -- does it make sense to assume default
                               -- priority for empty heap?
findMin (node p _ _ _) = p

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

findMinM : Heap → Maybe Priority
findMinM empty          = nothing
findMinM (node p _ _ _) = just p

-- deleteMin removes the element with the highest priority by merging
-- subtrees of a root element. Again the case of empty heap is
-- problematic. We could give it semantics by returning empty, but
-- this just doesn't feel right. Why should we be able to remove
-- elements from the empty heap?
deleteMin : Heap → Heap
deleteMin empty          = {!!} -- should we insert empty?
deleteMin (node _ _ l r) = merge l r

-- As a quick sanity check let's construct some examples. Here's a
-- heap constructed by inserting following priorities into an empty
-- heap: 3, 0, 1, 2.
heap : Heap
heap = insert (suc (suc zero))
      (insert (suc zero)
      (insert zero
      (insert (suc (suc (suc zero))) empty)))

-- Example usage of findMin
findMinInHeap : Priority
findMinInHeap = findMin heap

-- Example usage of deleteMin
deleteMinFromHeap : Heap
deleteMinFromHeap = deleteMin heap

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
module Syntax where

import Level
open import Data.Unit as Unit renaming (tt to ∗)
open import Data.List as List
open import Data.Product
open import Categories.Category using (Category)
open import Function

open import Relation.Binary.PropositionalEquality as PE hiding ([_]; subst)
open import Relation.Binary using (module IsEquivalence; Setoid; module Setoid)
open ≡-Reasoning

open import Common.Context as Context

Univ = ⊤

data FP : Set where
  μ : FP
  ν : FP

mutual
  TypeCtx : Set
  TypeCtx = Ctx (TermCtx × Univ)

  data Type : TypeCtx → TermCtx → TermCtx → Univ → Set

  data TermCtx : Set where
    Ø : TermCtx
    _∷'_ : {i : Univ} → (Γ : TermCtx) → Type [] Γ Ø i → TermCtx

  data Term (Γ Γ' : TermCtx) {i : Univ} :
            Type [] Γ Γ' i → Type [] Γ Γ' i → Set

  TypeVar : TypeCtx → TermCtx → Univ → Set
  TypeVar Δ Γ i = Var Δ (Γ , i)

  data CtxMor (Γ : TermCtx) : TermCtx → Set where
    ⟨⟩ : CtxMor Γ Ø
    _⋉_ : {i : Univ} {Γ' : TermCtx} {A : Type [] Γ' Ø i}
          (f : CtxMor Γ Γ') → Term Γ (subst A f) → CtxMor Γ (Γ ∷' A)

  reidx : {Δ : TypeCtx} {Γ Γ' : TermCtx} {i : Univ} →
          CtxMor Γ' Γ → Type Δ Γ Ø i → Type Δ Γ' Ø i
  reidx = ?

  data Term (Γ Γ' : TermCtx) {i : Univ} :
            Type [] Γ Γ' i → Type [] Γ Γ' i → Set where
       in₁ : {i : Univ} {X : TypeVar [(Γ , i)] Γ i}
             {Γ₁ : TermCtx} (A₁ : Type [(Γ , i)] Γ₁ Ø i) (f₁ : Γ₁ ▹ Γ) →
             Term Γ Γ' i (tySubst (fp A₁ f₁ μ) A₁ X) (reidx f₁ (fp A₁ f₁ μ))

  {-
  _++'_ : TermCtx → TermCtx → TermCtx
  Γ₁ ++' Ø         = Γ₁
  Γ₁ ++' (Γ₂ ∷' A) =
-}
  data Type : TypeCtx → TermCtx → TermCtx → Univ → Set where
    tyVar : (Δ : TypeCtx) → (Γ : TermCtx) → (i : Univ) → Type Δ Ø Γ i
--    app :
    fp : {Δ : TypeCtx} {Γ : TermCtx} {i : Univ} {X : TypeVar Δ Γ i}
         {Γ₁ : TermCtx} (A₁ : Type Δ Γ₁ Ø i)
         (f₁ : Γ₁ ▹ Γ)
         (ρ : FP) →
         Type Δ Ø Γ i
{-    fp : {Δ : TypeCtx} {X : TypeVar} {Γ Γ' Γ₁ : TermCtx} {i : Univ}
         (A₁ : Type Δ (Γ' ++' Γ₁)
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
------------------------------------------------------------------------
-- Functional semantics for an untyped λ-calculus with constants
------------------------------------------------------------------------

module Lambda.Closure.Functional where

open import Category.Monad
open import Category.Monad.Partiality as Partiality
  using (_⊥; never; OtherKind; other; steps)
open import Codata.Musical.Notation
open import Data.Empty using (⊥-elim)
open import Data.List hiding (lookup)
open import Data.Maybe hiding (_>>=_)
import Data.Maybe.Categorical as Maybe
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Vec using (Vec; []; _∷_; lookup)
open import Function
import Level
open import Relation.Binary using (module Preorder)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Negation

open Partiality._⊥
private
  open module E {A : Set} = Partiality.Equality (_≡_ {A = A})
  open module R {A : Set} =
    Partiality.Reasoning (P.isEquivalence {A = A})

open import Lambda.Syntax
open Closure Tm
open import Lambda.VirtualMachine
open Functional
private
  module VM = Closure Code

------------------------------------------------------------------------
-- A monad with partiality and failure

PF : RawMonad {f = Level.zero} (_⊥ ∘ Maybe)
PF = Maybe.monadT Partiality.monad

module PF where
  open RawMonad PF public

  fail : {A : Set} → Maybe A ⊥
  fail = now nothing

  _>>=-cong_ :
    ∀ {k} {A B : Set} {x₁ x₂ : Maybe A ⊥} {f₁ f₂ : A → Maybe B ⊥} →
    Rel k x₁ x₂ → (∀ x → Rel k (f₁ x) (f₂ x)) →
    Rel k (x₁ >>= f₁) (x₂ >>= f₂)
  _>>=-cong_ {k} {f₁ = f₁} {f₂} x₁≈x₂ f₁≈f₂ =
    Partiality._>>=-cong_ x₁≈x₂ helper
    where
    helper : ∀ {x y} → x ≡ y →
             Rel k (maybe f₁ fail x) (maybe f₂ fail y)
    helper {x = nothing} P.refl = fail ∎
    helper {x = just x}  P.refl = f₁≈f₂ x

  associative :
    {A B C : Set}
    (x : Maybe A ⊥) (f : A → Maybe B ⊥) (g : B → Maybe C ⊥) →
    (x >>= f >>= g) ≅ (x >>= λ y → f y >>= g)
  associative x f g =
    (x >>= f >>= g)                      ≅⟨ Partiality.associative P.refl x _ _ ⟩
    (x >>=′ λ y → maybe f fail y >>= g)  ≅⟨ Partiality._>>=-cong_ (x ∎) helper ⟩
    (x >>= λ y → f y >>= g)              ∎
    where
    open RawMonad Partiality.monad renaming (_>>=_ to _>>=′_)

    helper : ∀ {y₁ y₂} → y₁ ≡ y₂ →
             (maybe f fail y₁ >>= g) ≅ maybe (λ z → f z >>= g) fail y₂
    helper {y₁ = nothing} P.refl = fail ∎
    helper {y₁ = just y}  P.refl = (f y >>= g) ∎

  >>=-inversion-⇓ :
    ∀ {k} {A B : Set} x {f : A → Maybe B ⊥} {y} →
    (x>>=f⇓ : (x >>= f) ⇓[ k ] just y) →
    ∃ λ z → ∃₂ λ (x⇓ : x ⇓[ k ] just z)
                 (fz⇓ : f z ⇓[ k ] just y) →
                 steps x⇓ + steps fz⇓ ≡ steps x>>=f⇓
  >>=-inversion-⇓ x {f} x>>=f⇓
    with Partiality.>>=-inversion-⇓ {_∼A_ = _≡_} P.refl x x>>=f⇓
  ... | (nothing , x↯ , now ()  , _)
  ... | (just z  , x⇓ , fz⇓     , eq) = (z , x⇓ , fz⇓ , eq)

  >>=-inversion-⇑ :
    ∀ {k} {A B : Set} x {f : A → Maybe B ⊥} →
    (x >>= f) ⇑[ other k ] →
    ¬ ¬ (x ⇑[ other k ] ⊎
         ∃ λ y → x ⇓[ other k ] just y × f y ⇑[ other k ])
  >>=-inversion-⇑ {k} x {f} x>>=f⇑ =
    helper ⟨$⟩ Partiality.>>=-inversion-⇑ P.isEquivalence x x>>=f⇑
    where
    open RawMonad ¬¬-Monad renaming (_<$>_ to _⟨$⟩_)

    helper : (_ ⊎ ∃ λ (y : Maybe _) → _) → _
    helper (inj₁ x⇑                      ) = inj₁ x⇑
    helper (inj₂ (just y  , x⇓,fy⇑)      ) = inj₂ (y , x⇓,fy⇑)
    helper (inj₂ (nothing , x↯,now∼never)) =
      ⊥-elim (Partiality.now≉never (proj₂ x↯,now∼never))

------------------------------------------------------------------------
-- A workaround for the limitations of guardedness

module Workaround where

  data Maybe_⊥P : Set → Set₁ where
    fail   : ∀ {A} → Maybe A ⊥P
    return : ∀ {A} (x : A) → Maybe A ⊥P
    later  : ∀ {A} (x : ∞ (Maybe A ⊥P)) → Maybe A ⊥P
    _>>=_  : ∀ {A B} (x : Maybe A ⊥P) (f : A → Maybe B ⊥P) → Maybe B ⊥P

  private

    data Maybe_⊥W : Set → Set₁ where
      fail   : ∀ {A} → Maybe A ⊥W
      return : ∀ {A} (x : A) → Maybe A ⊥W
      later  : ∀ {A} (x : Maybe A ⊥P) → Maybe A ⊥W

    mutual

      _>>=W_ : ∀ {A B} → Maybe A ⊥W → (A → Maybe B ⊥P) → Maybe B ⊥W
      fail     >>=W f = fail
      return x >>=W f = whnf (f x)
      later x  >>=W f = later (x >>= f)

      whnf : ∀ {A} → Maybe A ⊥P → Maybe A ⊥W
      whnf fail       = fail
      whnf (return x) = return x
      whnf (later x)  = later (♭ x)
      whnf (x >>= f)  = whnf x >>=W f

  mutual

    private

      ⟪_⟫W : ∀ {A} → Maybe A ⊥W → Maybe A ⊥
      ⟪ fail     ⟫W = PF.fail
      ⟪ return x ⟫W = PF.return x
      ⟪ later x  ⟫W = later (♯ ⟪ x ⟫P)

    ⟪_⟫P : ∀ {A} → Maybe A ⊥P → Maybe A ⊥
    ⟪ p ⟫P = ⟪ whnf p ⟫W

  -- The definitions above make sense. ⟪_⟫P is homomorphic with respect
  -- to fail, return, later and _>>=_.

  fail-hom : ∀ {A} → ⟪ fail {A = A} ⟫P ≅ PF.fail
  fail-hom = PF.fail ∎

  return-hom : ∀ {A} (x : A) → ⟪ return x ⟫P ≅ PF.return x
  return-hom x = PF.return x ∎

  later-hom : ∀ {A} (x : ∞ Maybe A ⊥P) →
              ⟪ later x ⟫P ≅ later (♯ ⟪ ♭ x ⟫P)
  later-hom x = later (♯ (⟪ ♭ x ⟫P ∎))

  mutual

    private

      >>=-homW : ∀ {A B} (x : Maybe A ⊥W) (f : A → Maybe B ⊥P) →
                 ⟪ x >>=W f ⟫W ≅ PF._>>=_ ⟪ x ⟫W (λ y → ⟪ f y ⟫P)
      >>=-homW fail       f = PF.fail ∎
      >>=-homW (return x) f = ⟪ f x ⟫P ∎
      >>=-homW (later x)  f = later (♯ >>=-hom x f)

    >>=-hom : ∀ {A B} (x : Maybe A ⊥P) (f : A → Maybe B ⊥P) →
              ⟪ x >>= f ⟫P ≅ PF._>>=_ ⟪ x ⟫P (λ y → ⟪ f y ⟫P)
    >>=-hom x f = >>=-homW (whnf x) f

open Workaround hiding (_>>=_)

------------------------------------------------------------------------
-- Semantics

infix 5 _∙_

-- Note that this definition gives us determinism "for free".

mutual

  ⟦_⟧′ : ∀ {n} → Tm n → Env n → Maybe Value ⊥P
  ⟦ con i ⟧′   ρ = return (con i)
  ⟦ var x ⟧′   ρ = return (lookup ρ x)
  ⟦ ƛ t ⟧′     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧′ ρ = ⟦ t₁ ⟧′ ρ >>= λ v₁ →
                   ⟦ t₂ ⟧′ ρ >>= λ v₂ →
                   v₁ ∙ v₂
    where open Workaround

  _∙_ : Value → Value → Maybe Value ⊥P
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = later (♯ (⟦ t₁ ⟧′ (v₂ ∷ ρ)))

⟦_⟧ : ∀ {n} → Tm n → Env n → Maybe Value ⊥
⟦ t ⟧ ρ = ⟪ ⟦ t ⟧′ ρ ⟫P

------------------------------------------------------------------------
-- Example

Ω-loops : ⟦ Ω ⟧ [] ≈ never
Ω-loops = later (♯ Ω-loops)

------------------------------------------------------------------------
-- Some lemmas

open PF hiding (_>>=_)

-- An abbreviation.

infix 5 _⟦·⟧_

_⟦·⟧_ : Maybe Value ⊥ → Maybe Value ⊥ → Maybe Value ⊥
v₁ ⟦·⟧ v₂ = v₁ >>= λ v₁ → v₂ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P
  where open PF

-- _⟦·⟧_ preserves equality.

_⟦·⟧-cong_ : ∀ {k v₁₁ v₁₂ v₂₁ v₂₂} →
             Rel k v₁₁ v₂₁ → Rel k v₁₂ v₂₂ →
             Rel k (v₁₁ ⟦·⟧ v₁₂) (v₂₁ ⟦·⟧ v₂₂)
v₁₁≈v₂₁ ⟦·⟧-cong v₁₂≈v₂₂ =
  v₁₁≈v₂₁ >>=-cong λ v₁ →
  v₁₂≈v₂₂ >>=-cong λ v₂ →
  ⟪ v₁ ∙ v₂ ⟫P ∎

-- The semantics of application is compositional (with respect to the
-- syntactic equality which is used).

·-comp : ∀ {n} (t₁ t₂ : Tm n) {ρ} →
         ⟦ t₁ · t₂ ⟧ ρ ≅ ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ
·-comp t₁ t₂ {ρ} =
  ⟦ t₁ · t₂ ⟧ ρ                                    ≅⟨ >>=-hom (⟦ t₁ ⟧′ ρ) _ ⟩

  PF._>>=_ (⟦ t₁ ⟧ ρ) (λ v₁ →
           ⟪ Workaround._>>=_ (⟦ t₂ ⟧′ ρ) (λ v₂ →
             v₁ ∙ v₂) ⟫P)                          ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ →
                                                       >>=-hom (⟦ t₂ ⟧′ ρ) _) ⟩
  ⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ                            ∎

open PF

------------------------------------------------------------------------
-- Compiler correctness

module Correctness {k : OtherKind} where

  infix  4 _≈P_ _≈W_
  infixr 2 _≡⟨_⟩W_ _≈⟨_⟩P_ _≈⟨_⟩W_

  mutual

    data _≈P_ : Maybe VM.Value ⊥ → Maybe VM.Value ⊥ → Set where
      _≈⟨_⟩P_ : ∀ x {y z} (x≈y : x ≈P y) (y≅z : y ≅ z) → x ≈P z
      correct :
        ∀ {n} t {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
        (hyp : ∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩
                       ≈W k v) →
        exec ⟨ comp t c , s , comp-env ρ ⟩ ≈P (⟦ t ⟧ ρ >>= k)

    data _≈W_ : Maybe VM.Value ⊥ → Maybe VM.Value ⊥ → Set where
      ⌈_⌉    : ∀ {x y} (x≈y : Rel (other k) x y) → x ≈W y
      later  : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y
      laterˡ : ∀ {x y} (x≈y : ♭ x ≈W   y) → later x ≈W       y

  _≡⟨_⟩W_ : ∀ x {y z} → x ≡ y → y ≈W z → x ≈W z
  _ ≡⟨ P.refl ⟩W y≈z = y≈z

  _≈⟨_⟩W_ : ∀ x {y z} → x ≈W y → y ≅ z → x ≈W z
  ._ ≈⟨ later  x≈y ⟩W later y≅z = later  (_ ≈⟨ x≈y ⟩P ♭ y≅z)
  ._ ≈⟨ laterˡ x≈y ⟩W       y≅z = laterˡ (_ ≈⟨ x≈y ⟩W   y≅z)
  _  ≈⟨ ⌈ x≈y ⌉    ⟩W       y≅z = ⌈ trans x≈y (Partiality.≅⇒ y≅z) ⌉
    where trans = Preorder.trans (Partiality.preorder P.isPreorder _)

  -- The relation _≈_ does not admit unrestricted use of transitivity
  -- in corecursive proofs, so I have formulated the correctness proof
  -- using a continuation. Note that the proof would perhaps be easier
  -- if the semantics was also formulated in continuation-passing
  -- style.

  mutual

    correctW :
      ∀ {n} t {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈W k v) →
      exec ⟨ comp t c , s , comp-env ρ ⟩ ≈W (⟦ t ⟧ ρ >>= k)
    correctW (con i) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (Lambda.Syntax.Closure.con i) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (con i) ⟩W
      k (con i)                                                        ∎)
    correctW (var x) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (lookup (comp-env ρ) x) ∷ s , comp-env ρ ⟩  ≡⟨ P.cong (λ v → exec ⟨ c , val v ∷ s , comp-env ρ ⟩) $ lookup-hom x ρ ⟩W
      exec ⟨ c , val (comp-val (lookup ρ x)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (lookup ρ x) ⟩W
      k (lookup ρ x)                                             ∎)
    correctW (ƛ t) {ρ} {c} {s} {k} hyp = laterˡ (
      exec ⟨ c , val (comp-val (ƛ t ρ)) ∷ s , comp-env ρ ⟩  ≈⟨ hyp (ƛ t ρ) ⟩W
      k (ƛ t ρ)                                             ∎)
    correctW (t₁ · t₂) {ρ} {c} {s} {k} hyp =
      exec ⟨ comp t₁ (comp t₂ (app ∷ c)) , s , comp-env ρ ⟩           ≈⟨ correctW t₁ (λ v₁ → correctW t₂ (λ v₂ → ∙-correctW v₁ v₂ hyp)) ⟩W
      (⟦ t₁ ⟧ ρ >>= λ v₁ →  ⟦ t₂ ⟧ ρ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P  >>= k)  ≅⟨ ((⟦ t₁ ⟧ ρ ∎) >>=-cong λ _ → sym $ associative (⟦ t₂ ⟧ ρ) _ _) ⟩
      (⟦ t₁ ⟧ ρ >>= λ v₁ → (⟦ t₂ ⟧ ρ >>= λ v₂ → ⟪ v₁ ∙ v₂ ⟫P) >>= k)  ≅⟨ sym $ associative (⟦ t₁ ⟧ ρ) _ _ ⟩
      (⟦ t₁ ⟧ ρ ⟦·⟧ ⟦ t₂ ⟧ ρ >>= k)                                   ≅⟨ sym (·-comp t₁ t₂ >>=-cong λ v → k v ∎) ⟩
      (⟦ t₁ · t₂ ⟧ ρ >>= k)                                           ∎

    ∙-correctW :
      ∀ {n} v₁ v₂ {ρ : Env n} {c s} {k : Value → Maybe VM.Value ⊥} →
      (∀ v → exec ⟨ c , val (comp-val v) ∷ s , comp-env ρ ⟩ ≈W k v) →
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val v₁) ∷ s , comp-env ρ ⟩ ≈W
      (⟪ v₁ ∙ v₂ ⟫P >>= k)
    ∙-correctW (con i)   v₂                 _   = ⌈ PF.fail ∎ ⌉
    ∙-correctW (ƛ t₁ ρ₁) v₂ {ρ} {c} {s} {k} hyp =
      exec ⟨ app ∷ c , val (comp-val v₂) ∷ val (comp-val (ƛ t₁ ρ₁)) ∷ s , comp-env ρ ⟩  ≈⟨ later (

        exec ⟨ comp t₁ [ ret ] , ret c (comp-env ρ) ∷ s , comp-env (v₂ ∷ ρ₁) ⟩               ≈⟨ correct t₁ (λ v → laterˡ (hyp v)) ⟩P
        (⟦ t₁ ⟧ (v₂ ∷ ρ₁) >>= k)                                                             ∎) ⟩W

      (⟪ ƛ t₁ ρ₁ ∙ v₂ ⟫P >>= k)                                                         ∎

  whnf : ∀ {x y} → x ≈P y → x ≈W y
  whnf (x ≈⟨ x≈y ⟩P y≅z) = x ≈⟨ whnf x≈y ⟩W y≅z
  whnf (correct t hyp)   = correctW t hyp

  mutual

    soundW : ∀ {x y} → x ≈W y → Rel (other k) x y
    soundW ⌈ x≈y ⌉      = x≈y
    soundW (later  x≈y) = later (♯ soundP x≈y)
    soundW (laterˡ x≈y) = laterˡ (soundW x≈y)

    soundP : ∀ {x y} → x ≈P y → Rel (other k) x y
    soundP x≈y = soundW (whnf x≈y)

-- Note that the equality that is used here is syntactic.

correct : ∀ t →
          exec ⟨ comp t [] , [] , [] ⟩ ≈
          (⟦ t ⟧ [] >>= λ v → PF.return (comp-val v))
correct t =
  soundP $ Correctness.correct t (λ v → ⌈ PF.return (comp-val v) ∎ ⌉)
  where open Correctness

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------------
-- Example using distributive laws on a binary operation via Agsy
------------------------------------------------------------------------------

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

-- Tested with the development version of the Agda standard library on
-- 02 February 2012.

module Agsy.DistributiveLaws.TaskB where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

infixl 7 _·_

------------------------------------------------------------------------------
-- Distributive laws axioms

postulate
  D   : Set        -- The universe
  _·_ : D → D → D  -- The binary operation.

  leftDistributive  : ∀ x y z → x · (y · z) ≡ (x · y) · (x · z)
  rightDistributive : ∀ x y z → (x · y) · z ≡ (x · z) · (y · z)

-- Properties

taskB : ∀ u x y z →
        (x · y · (z · u)) · ((x · y · ( z · u)) · (x · z · (y · u))) ≡
          x · z · (y · u)
taskB u x y z = {!-t 20 -m!}  -- Agsy fails

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Syntax.Type where

open import Type

-- Assures that a value has a certain type
type-ascript : ∀{ℓ} → (T : Type{ℓ}) → T → T
type-ascript T x = x
{-# INLINE type-ascript #-}

_:-[_] = type-ascript
infixr 0.98 _:-[_]
{-# INLINE _:-[_] #-}

infixl 10 type-ascript
syntax type-ascript T x = x :of: T


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Inverses
------------------------------------------------------------------------

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

module Function.Inverse where

open import Level
open import Function using (flip)
open import Function.Bijection hiding (id; _∘_; bijection)
open import Function.Equality as F
  using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
open import Function.LeftInverse as Left hiding (id; _∘_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_)
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Inverses

record _InverseOf_ {f₁ f₂ t₁ t₂}
                   {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
                   (from : To ⟶ From) (to : From ⟶ To) :
                   Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    left-inverse-of  : from LeftInverseOf  to
    right-inverse-of : from RightInverseOf to

------------------------------------------------------------------------
-- The set of all inverses between two setoids

record Inverse {f₁ f₂ t₁ t₂}
               (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
               Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to         : From ⟶ To
    from       : To ⟶ From
    inverse-of : from InverseOf to

  open _InverseOf_ inverse-of public

  left-inverse : LeftInverse From To
  left-inverse = record
    { to              = to
    ; from            = from
    ; left-inverse-of = left-inverse-of
    }

  open LeftInverse left-inverse public
    using (injective; injection)

  bijection : Bijection From To
  bijection = record
    { to        = to
    ; bijective = record
      { injective  = injective
      ; surjective = record
        { from             = from
        ; right-inverse-of = right-inverse-of
        }
      }
    }

  open Bijection bijection public
    using (equivalence; surjective; surjection; right-inverse;
           to-from; from-to)

------------------------------------------------------------------------
-- The set of all inverses between two sets (i.e. inverses with
-- propositional equality)

infix 3 _↔_ _↔̇_

_↔_ : ∀ {f t} → Set f → Set t → Set _
From ↔ To = Inverse (P.setoid From) (P.setoid To)

_↔̇_ : ∀ {i f t} {I : Set i} → Pred I f → Pred I t → Set _
From ↔̇ To = ∀ {i} → From i ↔ To i

inverse : ∀ {f t} {From : Set f} {To : Set t} →
          (to : From → To) (from : To → From) →
          (∀ x → from (to x) ≡ x) →
          (∀ x → to (from x) ≡ x) →
          From ↔ To
inverse to from from∘to to∘from = record
  { to   = P.→-to-⟶ to
  ; from = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to
    ; right-inverse-of = to∘from
    }
  }

------------------------------------------------------------------------
-- If two setoids are in bijective correspondence, then there is an
-- inverse between them

fromBijection :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  Bijection From To → Inverse From To
fromBijection b = record
  { to         = Bijection.to b
  ; from       = Bijection.from b
  ; inverse-of = record
    { left-inverse-of  = Bijection.left-inverse-of b
    ; right-inverse-of = Bijection.right-inverse-of b
    }
  }

------------------------------------------------------------------------
-- Inverse is an equivalence relation

-- Reflexivity

id : ∀ {s₁ s₂} → Reflexive (Inverse {s₁} {s₂})
id {x = S} = record
  { to         = F.id
  ; from       = F.id
  ; inverse-of = record
    { left-inverse-of  = LeftInverse.left-inverse-of id′
    ; right-inverse-of = LeftInverse.left-inverse-of id′
    }
  } where id′ = Left.id {S = S}

-- Transitivity

infixr 9 _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
      TransFlip (Inverse {f₁} {f₂} {m₁} {m₂})
                (Inverse {m₁} {m₂} {t₁} {t₂})
                (Inverse {f₁} {f₂} {t₁} {t₂})
f ∘ g = record
  { to         = to   f ⟪∘⟫ to   g
  ; from       = from g ⟪∘⟫ from f
  ; inverse-of = record
    { left-inverse-of  = LeftInverse.left-inverse-of (Left._∘_ (left-inverse  f) (left-inverse  g))
    ; right-inverse-of = LeftInverse.left-inverse-of (Left._∘_ (right-inverse g) (right-inverse f))
    }
  } where open Inverse

-- Symmetry.

sym : ∀ {f₁ f₂ t₁ t₂} →
      Sym (Inverse {f₁} {f₂} {t₁} {t₂}) (Inverse {t₁} {t₂} {f₁} {f₂})
sym inv = record
  { from       = to
  ; to         = from
  ; inverse-of = record
    { left-inverse-of  = right-inverse-of
    ; right-inverse-of = left-inverse-of
    }
  } where open Inverse inv

------------------------------------------------------------------------
-- Transformations

map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
        {f₁′ f₂′ t₁′ t₂′}
        {From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} →
      (t : (From ⟶ To) → (From′ ⟶ To′)) →
      (f : (To ⟶ From) → (To′ ⟶ From′)) →
      (∀ {to from} → from InverseOf to → f from InverseOf t to) →
      Inverse From To → Inverse From′ To′
map t f pres eq = record
  { to         = t to
  ; from       = f from
  ; inverse-of = pres inverse-of
  } where open Inverse eq

zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁}
        {From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁}
        {f₁₂ f₂₂ t₁₂ t₂₂}
        {From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂}
        {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
      (t : (From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) →
      (f : (To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) →
      (∀ {to₁ from₁ to₂ from₂} →
         from₁ InverseOf to₁ → from₂ InverseOf to₂ →
         f from₁ from₂ InverseOf t to₁ to₂) →
      Inverse From₁ To₁ → Inverse From₂ To₂ → Inverse From To
zip t f pres eq₁ eq₂ = record
  { to         = t (to   eq₁) (to   eq₂)
  ; from       = f (from eq₁) (from eq₂)
  ; inverse-of = pres (inverse-of eq₁) (inverse-of eq₂)
  } where open Inverse


text:
-- Non-indexed (plain) monads in form of Kleisli triple, presented in point-free style.

module Control.Comonad where

open import Function using (id) renaming (_∘′_ to _∘_)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Axiom.FunctionExtensionality
open import Control.Functor

record IsComonad (W : Set → Set) : Set₁ where

  -- Methods.

  field
    extract : ∀ {A  } → W A → A
    extend  : ∀ {A B} → (W A → B) → W A → W B

  -- Laws.

  field

    extend-β : ∀ {A B} {k : W A → B} →

      extract ∘ extend k ≡ k

    extend-η : ∀ {A} →

      extend {A = A} extract ≡ id

    extend-∘ : ∀ {A B C} {k : W A → B} {l : W B → C} →

      extend (l ∘ extend k) ≡ extend l ∘ extend k

  -- Comonadic composition.

  comComp : ∀ {A B C : Set} (l : W B → C) (k : W A → B) → (W A → C)
  comComp l k = l ∘ extend k

  -- Functoriality.

  isFunctor : IsFunctor W
  isFunctor = record
    { ops  = record { map = map  }
    ; laws = record { map-id = extend-η ; map-∘ = λ {A B C f g} → sym (map-∘-sym f g) }
    }
    where
      map : ∀ {A B} → (A → B) → W A → W B
      map f = extend (f ∘ extract)

      map-∘-sym : ∀ {A B C} (f : A → B) (g : B → C) → map g ∘ map f ≡ map (g ∘ f)
      map-∘-sym f g = begin
        map g ∘ map f                                ≡⟨⟩
        extend (g ∘ extract) ∘ extend (f ∘ extract)  ≡⟨ sym extend-∘ ⟩
        extend (g ∘ extract ∘ extend (f ∘ extract))  ≡⟨ cong (λ z → extend (g ∘ z)) extend-β ⟩
        extend (g ∘ f ∘ extract)                     ≡⟨⟩
        map (g ∘ f)                                  ∎

  open IsFunctor isFunctor public

-- Monads in Kleisli Triple presentation.

record Comonad : Set₁ where
  constructor comonad
  field
    W  : Set → Set
    W! : IsComonad W

  open IsComonad W! public

-- Casting a Comonad to a Functor

FunctorOfComonad : Comonad → Functor
FunctorOfComonad WW = functor W isFunctor
  where open Comonad WW

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
-- Andreas, 2016-01-21, issue 1791
-- With-clause stripping for copatterns with "polymorphic" field.

-- {-# OPTIONS -v tc.with.strip:60 #-}

postulate anything : ∀{A : Set} → A

record Wrap (A : Set) : Set where
  field unwrap : A

record Pointed (M : Set → Set) : Set₁ where
  field point : ∀{A} → M A  -- field type starts with hidden quantifier!

test : Pointed Wrap
Wrap.unwrap (Pointed.point test) with Set₂
... | _ = anything

-- should succeed


text:
module Generic.Property.Eq where

open import Generic.Core

SemEq : ∀ {i β} {I : Set i} -> Desc I β -> Set
SemEq (var i)   = ⊤
SemEq (π i q C) = ⊥
SemEq (D ⊛ E)   = SemEq D × SemEq E

mutual
  ExtendEq : ∀ {i β} {I : Set i} -> Desc I β -> Set β
  ExtendEq (var i)   = ⊤
  ExtendEq (π i q C) = ExtendEqᵇ i C q
  ExtendEq (D ⊛ E)   = SemEq D × ExtendEq E

  ExtendEqᵇ : ∀ {ι α β γ q} {I : Set ι} i -> Binder α β γ i q I -> α ≤ℓ β -> Set β
  ExtendEqᵇ (arg-info v r) (coerce (A , D)) q = Coerce′ q $ RelEq r A × ∀ {x} -> ExtendEq (D x)

instance
  {-# TERMINATING #-} -- Why?
  DataEq : ∀ {i β} {I : Set i} {D : Data (Desc I β)} {j}
             {{eqD : All ExtendEq (consTypes D)}} -> Eq (μ D j)
  DataEq {ι} {β} {I} {D₀} = record { _≟_ = decMu } where
    mutual
      decSem : ∀ D {{eqD : SemEq D}} -> IsSet (⟦ D ⟧ (μ D₀))
      decSem (var i)                 d₁ d₂ = decMu d₁ d₂
      decSem (π i q C) {{()}}
      decSem (D ⊛ E)   {{eqD , eqE}} p₁ p₂ =
        decProd (decSem D {{eqD}}) (decSem E {{eqE}}) p₁ p₂

      decExtend : ∀ {j} D {{eqD : ExtendEq D}} -> IsSet (Extend D (μ D₀) j)
      decExtend (var i)                 lrefl lrefl = yes refl
      decExtend (π i q C)               p₁    p₂    = decExtendᵇ i C q p₁ p₂
      decExtend (D ⊛ E)   {{eqD , eqE}} p₁    p₂    =
        decProd (decSem D {{eqD}}) (decExtend E {{eqE}}) p₁ p₂

      decExtendᵇ : ∀ {α γ q j} i (C : Binder α β γ i q I) q {{eqC : ExtendEqᵇ i C q}}
                 -> IsSet (Extendᵇ i C q (μ D₀) j)
      decExtendᵇ (arg-info v r) (coerce (A , D)) q {{eqC}} p₁ p₂ =
        split q eqC λ eqA eqD ->
          decCoerce′ q (decProd (_≟_ {{EqRelValue {{eqA}}}}) (decExtend (D _) {{eqD}})) p₁ p₂

      decAny : ∀ {j} (Ds : List (Desc I β)) {{eqD : All ExtendEq Ds}}
             -> ∀ d a b ns -> IsSet (Node D₀ (packData d a b Ds ns) j)
      decAny  []                         d a b  tt      () ()
      decAny (D ∷ [])     {{eqD , _}}    d a b (_ , ns) e₁ e₂ = decExtend D {{eqD}} e₁ e₂
      decAny (D ∷ E ∷ Ds) {{eqD , eqDs}} d a b (_ , ns) s₁ s₂ =
        decSum (decExtend D {{eqD}}) (decAny (E ∷ Ds) {{eqDs}} d a b ns) s₁ s₂

      decMu : ∀ {j} -> IsSet (μ D₀ j)
      decMu (node e₁) (node e₂) = dcong node node-inj $ decAny (consTypes D₀)
                                                               (dataName  D₀)
                                                               (parsTele  D₀)
                                                               (indsTele  D₀)
                                                               (consNames D₀)
                                                                e₁
                                                                e₂

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
module prelude where

Subset : Set → Set₁
Subset(X) = X → Set

_∈_ : ∀ {X} → X → Subset(X) → Set
(x ∈ A) = A(x)

_⊆_ : ∀ {X} → Subset(X) → Subset(X) → Set
(A ⊆ B) = ∀ x → (x ∈ A) → (x ∈ B)

record Inhabited {X} (S : Subset(X)) : Set where
  constructor _,_
  field witness : X
  field witness-in : (witness ∈ S)

Rel : Set → Set₁
Rel(X) = X → X → Set

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

data ℤ : Set where
  succ : ℕ → ℤ
  -ve : ℕ → ℤ

+ve : ℕ → ℤ
+ve zero = -ve zero
+ve (succ n) = (succ n)

sucz : ℤ → ℤ
sucz (succ x) = succ (succ x)
sucz (-ve zero) = succ zero
sucz (-ve (succ x)) = -ve x

pred : ℤ → ℤ
pred (succ zero) = -ve zero
pred (succ (succ x)) = succ x
pred (-ve x) = -ve (succ x)

_+_ : ℤ → ℤ → ℤ
succ zero + y = sucz y
succ (succ x) + y = sucz (succ x + y)
-ve zero + y = y
-ve (succ x) + y = pred (-ve x + y)

data _^_ (X : Set) : ℕ → Set where
  nil : (X ^ zero)
  _∷_ : ∀ {n} → X → (X ^ n) → (X ^ succ(n))

data _≡_ {D : Set} (d : D) : D → Set where
  refl : (d ≡ d)

sym : ∀ {D} {d e : D} → (d ≡ e) → (e ≡ d)
sym refl = refl

trans : ∀ {D} {d e f : D} → (d ≡ e) → (e ≡ f) → (d ≡ f)
trans refl refl = refl

subst : ∀ {X L R} (P : X → Set) → (L ≡ R) → (P R) → (P L)
subst P refl p = p

data _≣_ {X : Set₁} (x : X) : X → Set₁ where
  REFL : (x ≣ x)

SYM : ∀ {D} {d e : D} → (d ≣ e) → (e ≣ d)
SYM REFL = REFL

TRANS : ∀ {D} {d e f : D} → (d ≣ e) → (e ≣ f) → (d ≣ f)
TRANS REFL REFL = REFL

SUBST : ∀ {X L R} (P : X → Set) →
  (L ≣ R) →
  (P R) →
  (P L)
SUBST P REFL p = p

succ-dist-+ : ∀ m n → ((succ m + n) ≡ sucz (+ve m + n))
succ-dist-+ zero     n = refl
succ-dist-+ (succ m) n = refl

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

¬ : Set → Set
¬(X) = (X → ⊥)

contradiction : ∀ {X : Set} → ⊥ → X
contradiction ()

data _∨_ (X Y : Set) : Set where
  in₁ : X → (X ∨ Y)
  in₂ : Y → (X ∨ Y)

_∪_ : ∀ {X} → Subset(X) → Subset(X) → Subset(X)
(A ∪ B) x = (x ∈ A) ∨ (x ∈ B)

record _∧_ (X Y : Set) : Set where
  constructor _,_
  field proj₁ : X
  field proj₂ : Y

_∩_ : ∀ {X} → Subset(X) → Subset(X) → Subset(X)
(A ∩ B) x = (x ∈ A) ∧ (x ∈ B)

All : ∀ {X n} → Subset(X) → Subset(X ^ n)
All(S) nil = ⊤
All(S) (x ∷ xs) = (x ∈ S) ∧ (xs ∈ All(S))

All-resp-⊆ : ∀ {X} {A B : Subset(X)} {n} → (A ⊆ B) → (All {n = n} (A) ⊆ All(B))
All-resp-⊆ A⊆B nil tt = tt
All-resp-⊆ A⊆B (x ∷ xs) (x∈A , xs∈A) = (A⊆B x x∈A , All-resp-⊆ A⊆B xs xs∈A)

All-resp-∩ : ∀ {X} {A B : Subset(X)} {n} → ((All {n = n} (A) ∩ All(B)) ⊆ All(A ∩ B))
All-resp-∩ nil (tt , tt) = tt
All-resp-∩ (d ∷ ds) ((d∈A , ds∈A) , (d∈B , ds∈B)) = ((d∈A , d∈B) , (All-resp-∩ ds (ds∈A , ds∈B)))

record DirectedGraph(D : Set) : Set₁ where

  field _⇒_ : Rel(D)

  data _⇒+_ (d e : D) : Set where
    ⇒-impl-⇒+ : (d ⇒ e) → (d ⇒+ e)
    ⇒⇒+-impl-⇒+ : ∀ {f} → (d ⇒ f) → (f ⇒+ e) → (d ⇒+ e)

record Forest(D : Set) : Set₁ where

  field DG : DirectedGraph(D)
  open DirectedGraph DG public

  field ⇒-parent-uniq : ∀ {d e f} → (d ⇒ f) → (e ⇒ f) → (d ≡ e)
  field ⇒-acyclic : ∀ {d} → (d ⇒+ d) → ⊥

record PartialOrder(D : Set) : Set₁ where

  field _≤_ : Rel(D)
  field ≤-refl : ∀ {d} → (d ≤ d)
  field ≤-trans : ∀ {d e f} → (d ≤ e) → (e ≤ f) → (d ≤ f)
  field ≤-asym : ∀ {d e} → (d ≤ e) → (e ≤ d) → (d ≡ e)

  field _≤?_ : ∀ d e → ((d ≤ e) ∨ ¬(d ≤ e))

  _<_ : Rel(D)
  d < e = (d ≤ e) ∧ ¬(d ≡ e)

  ≡-impl-≤ : ∀ {d e} → (d ≡ e) → (d ≤ e)
  ≡-impl-≤ refl = ≤-refl

  <-trans-≤ : ∀ {d e f} → (d < e) → (e ≤ f) → (d < f)
  <-trans-≤ (d≤e , d≠e) e≤f = (≤-trans d≤e e≤f , (λ d≡f → d≠e (trans d≡f (≤-asym (≤-trans (≡-impl-≤ (sym d≡f)) d≤e) e≤f))))

  ≤-trans-< : ∀ {d e f} → (d ≤ e) → (e < f) → (d < f)
  ≤-trans-< d≤e (e≤f , e≠f) = (≤-trans d≤e e≤f , (λ d≡f → e≠f (trans (≤-asym (≤-trans e≤f (≡-impl-≤ (sym d≡f))) d≤e) d≡f)))

  <-trans : ∀ {d e f} → (d < e) → (e < f) → (d < f)
  <-trans d<e (e≤f , e≠f) = <-trans-≤ d<e e≤f

  <-impl-≤ : ∀ {d e} → (d < e) → (d ≤ e)
  <-impl-≤ (d≤e , d≠e) = d≤e

  <-impl-≱ : ∀ {d e} → (d < e) → ¬(e ≤ d)
  <-impl-≱ (d≤e , d≠e) e≤d = d≠e (≤-asym d≤e e≤d)

  Past : D → Subset(D)
  Past(d) e = (e < d)

  Future : D → Subset(D)
  Future(d) e = (d < e)

  Decreasing : ∀ {n} → Subset(D ^ n)
  Decreasing nil = ⊤
  Decreasing (d ∷ ds) = (ds ∈ (All(Past(d)) ∩  Decreasing))

  Increasing : ∀ {n} → Subset(D ^ n)
  Increasing nil = ⊤
  Increasing (d ∷ ds) = (ds ∈ (All(Future(d)) ∩  Increasing))

  _≤*_ : ∀ {n} → Rel(D ^ n)
  nil ≤* nil = ⊤
  (d ∷ ds) ≤* (e ∷ es) = (d ≤ e) ∧ (ds ≤* es)

  Min : Subset(D) → Subset(D)
  Min(S) d = (d ∈ S) ∧ (∀ e → (e ∈ S) → (d ≤ e))

  Max : Subset(D) → Subset(D)
  Max(S) d = (d ∈ S) ∧ (∀ e → (e ∈ S) → (e ≤ d))

  Min* : ∀ {n} → Subset(D ^ n) → Subset(D ^ n)
  Min*(S) ds = (ds ∈ S) ∧ (∀ es → (es ∈ S) → (ds ≤* es))

  Max* : ∀ {n} → Subset(D ^ n) → Subset(D ^ n)
  Max*(S) ds = (ds ∈ S) ∧ (∀ es → (es ∈ S) → (es ≤* ds))

record FiniteTotalOrder(D : Set) : Set₁ where

  field PO : PartialOrder(D)
  open PartialOrder PO public

  field min_∵_ : ∀ (S : Subset(D)) → Inhabited(S) → Inhabited(Min(S))
  field max_∵_ : ∀ (S : Subset(D)) → Inhabited(S) → Inhabited(Max(S))

  ≤-total : ∀ d e → (d ≤ e) ∨ (e < d)
  ≤-total d e with d ≤? e
  ≤-total d e | in₁ d≤e = in₁ d≤e
  ≤-total d e | in₂ d≰e with max (λ f → (d ≡ f) ∨ (e ≡ f)) ∵ (d , in₁ refl)
  ≤-total d e | in₂ d≰e | .d , (in₁ refl , d-max) = in₂ (e≤d , e≠d) where

    e≤d = d-max e (in₂ refl)
    e≠d = λ e=d → d≰e (≡-impl-≤ (sym e=d))

  ≤-total d e | in₂ d≰e | .e , (in₂ refl , e-max) = contradiction (d≰e (e-max d (in₁ refl)))

  Max-hd : ∀ S {n} d (ds : D ^ n) →
    ((d ∷ ds) ∈ Max*(Decreasing ∩ All(S))) →
    (d ∈ Max(S))
  Max-hd S d ds (((d>ds , ds↓) , (d∈S , ds∈S)) , d∷ds-max) = (d∈S , d-max) where

    d-max : ∀ e → (e ∈ S) → (e ≤ d)
    d-max e e∈S with ≤-total e d
    d-max e e∈S | in₁ e≤d = e≤d
    d-max e e∈S | in₂ d<e with d∷ds-max (e ∷ ds) ((All-resp-⊆ (λ f d<f → <-trans d<f d<e) ds d>ds , ds↓) , (e∈S , ds∈S))
    d-max e e∈S | in₂ d<e | (e≤d , ds≤ds) = e≤d

  Max-tl : ∀ S {n} d (ds : D ^ n) →
    ((d ∷ ds) ∈ Max*(Decreasing ∩ All(S))) →
    (ds ∈ Max*(All(Past(d)) ∩ (Decreasing ∩ All(S))))
  Max-tl S d ds (((d>ds , ds↓) , (d∈S , ds∈S)) , d∷ds-max) = ((d>ds , (ds↓ , ds∈S)) , ds-max) where

    ds-max : ∀ es → (es ∈ (All(Past(d)) ∩ (Decreasing ∩ All(S)))) → (es ≤* ds)
    ds-max es (d>es , (es↓ , es∈S)) with d∷ds-max (d ∷ es) ((d>es , es↓) , (d∈S , es∈S))
    ds-max es (d>es , (es↓ , es∈S)) | (d≤d , es≤ds) = es≤ds

record Equivalence(D : Set) : Set₁ where

  field _~_ : Rel(D)
  field ~-refl : ∀ {d} → (d ~ d)
  field ~-trans : ∀ {d e f} → (d ~ e) → (e ~ f) → (d ~ f)
  field ~-sym : ∀ {d e} → (d ~ e) → (e ~ d)

  field _~?_ : ∀ d e → ((d ~ e) ∨ ¬(d ~ e))

  ≡-impl-~ : ∀ {d e} → (d ≡ e) → (d ~ e)
  ≡-impl-~ refl = ~-refl

max_stars_repo_name: cbrewster/ServoNavigation

max_issues_repo_name: cbrewster/ServoNavigation

max_forks_repo_name: cbrewster/ServoNavigation


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

module Codata.Stream where

open import Prelude
open import Data.List using (List; _∷_; [])
open import Data.List.Kleene
import Data.List.Kleene.Membership as Kleene
open import Data.Fin

Stream : Type a → Type a
Stream A = ℕ → A

infixr 5 _∈_
_∈_ : A → Stream A → Type _
x ∈ xs = fiber xs x

toList : ℕ → Stream A → List A
toList zero xs = []
toList (suc n) xs = xs zero ∷ toList n (xs ∘ suc)

mutual
  concat⋆ : A ⋆ → Stream (A ⁺) → Stream A
  concat⋆ []    xs = concat⁺ (xs zero) (xs ∘ suc)
  concat⋆ (∹ x) xs = concat⁺ x xs

  concat⁺ : A ⁺ → Stream (A ⁺) → Stream A
  concat⁺ x xs zero    = x .head
  concat⁺ x xs (suc n) = concat⋆ (x .tail) xs n

concat : Stream (A ⁺) → Stream A
concat xs = concat⁺ (xs zero) (xs ∘ suc)

infixr 5 _∈²_
_∈²_ : A → Stream (A ⁺) → Type _
x ∈² xs = ∃[ n ] x Kleene.∈⁺ xs n

mutual
  ◇++⋆ : ∀ (x : A) y ys → x Kleene.∈⋆ y → x ∈ concat⋆ y ys
  ◇++⋆ x (∹ y) ys x∈y = ◇++⁺ x y ys x∈y

  ◇++⁺ : ∀ (x : A) y ys → x Kleene.∈⁺ y → x ∈ concat⁺ y ys
  ◇++⁺ x y ys (f0 , x∈y) = zero , x∈y
  ◇++⁺ x y ys (fs n , x∈y) = let m , p = ◇++⋆ x (y .tail) ys (n , x∈y) in suc m , p

mutual
  ++◇⋆ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⋆ y ys
  ++◇⋆ x [] ys x∈ys = x∈ys
  ++◇⋆ x (∹ y) ys x∈ys = ++◇⁺ x y ys x∈ys

  ++◇⁺ : ∀ (x : A) y ys → x ∈ concat ys → x ∈ concat⁺ y ys
  ++◇⁺ x y ys x∈ys = let n , p = ++◇⋆ x (y .tail) ys x∈ys in suc n , p

concat-∈ : ∀ (x : A) xs → x ∈² xs → x ∈ concat xs
concat-∈ x xs (zero  , x∈xs) = ◇++⁺ x (xs zero) (xs ∘ suc) x∈xs
concat-∈ x xs (suc n , x∈xs) = ++◇⁺ x (xs zero) (xs ∘ suc) (concat-∈ x (xs ∘ suc) (n , x∈xs))

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Issue472 where

postulate
 I : Set
 P : I → Set

record ∃ (P : I → Set) : Set where
 constructor _,_
 field
   fst : I
   snd : P fst

open ∃

data S : ∃ P → Set where
 s : (i : I) (x : P i) → S (i , x)

Foo : (p : ∃ P) → S p → Set
Foo p (s .(fst p) .(snd p)) = I

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

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda