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

open import Algebra.Structures.Bundles.Field

module Algebra.Linear.Construct.Matrix
  {k ℓ} (K : Field k ℓ)
  where

open import Level using (_⊔_)
open import Data.Product hiding (map)
open import Data.Fin using (Fin; toℕ; fromℕ; _≤_)
open import Data.Fin.Properties using (¬Fin0)
open import Data.Nat hiding (_⊔_; _≤_) renaming (_+_ to _+ℕ_; _*_ to _*ℕ_)
open import Data.Nat.Properties using (1+n≢0)

open import Relation.Binary
import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
open import Algebra.Linear.Core

import Data.Vec.Properties as VP

open import Algebra.Structures.Field.Utils K

import Algebra.Linear.Construct.Vector K as V
open V
  using (Vec; zipWith; replicate)
  renaming
    ( _+_ to _+v_
    ; _∙_ to _∙v_
    ; -_  to -v_
    )

open import Relation.Binary.PropositionalEquality as P
  using (_≡_; subst; subst-subst-sym; _≗_)
  renaming
  ( refl  to ≡-refl
  ; sym   to ≡-sym
  ; trans to ≡-trans
  )

import Algebra.Linear.Structures.VectorSpace as VS

open VS.VectorSpaceField K

open import Data.Nat.Properties
  using
    ( ≤-refl
    ; ≤-reflexive
    ; ≤-antisym
    ; n∸n≡0
    ; m+[n∸m]≡n
    ; m≤m+n
    ; suc-injective
    )
  renaming
    ( +-identityˡ to +ℕ-identityˡ
    ; +-identityʳ to +ℕ-identityʳ
    )

Matrix : ℕ -> ℕ -> Set k
Matrix n p = Vec (Vec K' p) n

private
  M : ℕ -> ℕ -> Set k
  M = Matrix

_≈ʰ_ : ∀ {n p n' p'} (A : M n p) (B : M n' p') → Set (k ⊔ ℓ)
_≈ʰ_ = PW.Pointwise V._≈ʰ_

module _ {n p} where
  setoid : Setoid k (k ⊔ ℓ)
  setoid = record
    { Carrier       = M n p
    ; _≈_           = _≈ʰ_ {n} {p}
    ; isEquivalence = PW.isEquivalence (V.≈-isEquiv {p}) n
    }

  open Setoid setoid public
    renaming
      ( refl  to ≈-refl
      ; sym   to ≈-sym
      ; trans to ≈-trans
      ; reflexive to ≈-reflexive
      ; isEquivalence to ≈-isEquiv
      )

import Algebra.FunctionProperties as FP

tabulate : ∀ {n p} -> (Fin n -> Fin p -> K') -> M n p
tabulate f = V.tabulate λ i -> V.tabulate λ j -> f i j

tabulate⁺ : ∀ {n p} {f g : Fin n -> Fin p -> K'}
         -> (∀ i j -> f i j ≈ᵏ g i j)
         -> tabulate f ≈ tabulate g
tabulate⁺ {0} r = PW.[]
tabulate⁺ {suc n} {p} {f} {g} r =
  (PW.tabulate⁺ (r Fin.zero)) PW.∷ tabulate⁺ {n} {p} λ i j → r (Fin.suc i) j

fromVec : ∀ {n p} -> V.Vec K' (n *ℕ p) -> M n p
fromVec {0} V.[] = V.[]
fromVec {suc n} {p} xs =
  let (vp , vnp , _) = V.splitAt p xs
  in vp V.∷ fromVec {n} vnp

toVec : ∀ {n p} -> M n p -> V.Vec K' (n *ℕ p)
toVec {n} {p} = V.concat {m = p} {n = n}

concat∘fromVec : ∀ {n p} (v : V.Vec K' (n *ℕ p)) -> toVec {n} {p} (fromVec v) V.≈ v
concat∘fromVec {0} V.[] = PW.[]
concat∘fromVec {suc n} {p} v =
  let (vn , vnp , r) = V.splitAt p v
  in begin
    toVec {suc n} {p} (fromVec v)
  ≡⟨⟩
    vn V.++ toVec {n} {p} (fromVec vnp)
  ≈⟨ V.++-cong {p} {n *ℕ p} V.≈-refl (concat∘fromVec {n} {p} vnp) ⟩
    vn V.++ vnp
  ≈⟨ V.≈-sym (V.≈-reflexive r) ⟩
    v
  ∎
  where open import Relation.Binary.EqReasoning (V.setoid (suc n *ℕ p))

_++_ : ∀ {n p q} -> M n p -> M n q -> M n (p +ℕ q)
_++_ = zipWith V._++_

_‡_ : ∀ {n m p} -> M n p -> M m p -> M (n +ℕ m) p
_‡_ = V._++_

lookup : ∀ {n p} -> M n p -> Fin n -> Fin p -> K'
lookup A i j = V.lookup (V.lookup A i) j

_⟪_,_⟫ : ∀ {n p} -> M n p -> Fin n -> Fin p -> K'
_⟪_,_⟫ = lookup

lookup-cong : ∀ {n p} {A B : M n p} (i : Fin n) (j : Fin p) -> A ≈ B -> (A ⟪ i , j ⟫) ≈ᵏ (B ⟪ i , j ⟫)
lookup-cong i j rs = PW.lookup (PW.lookup rs i) j

tabulate∘lookup : ∀ {n p} (A : M n p) → tabulate (lookup A) ≡ A
tabulate∘lookup A =
  begin
    tabulate (lookup A)
  ≡⟨⟩
    V.tabulate (λ i -> V.tabulate λ j -> V.lookup (V.lookup A i) j)
  ≡⟨ VP.tabulate-cong (λ i → VP.tabulate∘lookup (V.lookup A i)) ⟩
    V.tabulate (λ i -> V.lookup A i)
  ≡⟨ VP.tabulate∘lookup A ⟩
    A
  ∎
  where open import Relation.Binary.PropositionalEquality as Eq
        open Eq.≡-Reasoning

lookup∘tabulate : ∀ {n p} (f : Fin n -> Fin p -> K') (i : Fin n) (j : Fin p)
                -> lookup (tabulate f) i j ≡ f i j
lookup∘tabulate {suc n} f i j =
  begin
    lookup (tabulate f) i j
  ≡⟨⟩
    V.lookup (V.lookup (V.tabulate λ i′ -> V.tabulate λ j′ -> f i′ j′) i) j
  ≡⟨ cong (λ u → V.lookup u j) (VP.lookup∘tabulate (λ i′ -> V.tabulate λ j′ -> f i′ j′) i) ⟩
    V.lookup (V.tabulate λ j′ -> f i j′) j
  ≡⟨ VP.lookup∘tabulate (λ j′ -> f i j′) j ⟩
    f i j
  ∎
  where open import Relation.Binary.PropositionalEquality as Eq
        open Eq.≡-Reasoning

tabulate-cong-≡ : ∀ {n p} {f g : Fin n -> Fin p -> K'} -> (∀ i j -> f i j ≡ g i j) -> tabulate f ≡ tabulate g
tabulate-cong-≡ {f = f} {g = g} r = VP.tabulate-cong (λ i → VP.tabulate-cong (λ j → r i j))

tabulate-cong : ∀ {n p} {f g : Fin n -> Fin p -> K'} -> (∀ i j -> f i j ≈ᵏ g i j) -> tabulate f ≈ tabulate g
tabulate-cong {f = f} {g = g} r = PW.tabulate⁺ (λ i → V.tabulate-cong (λ j → r i j))

transpose : ∀ {n p} -> M n p -> M p n
transpose A = tabulate λ i j -> A ⟪ j , i ⟫

_ᵀ : ∀ {n p} -> M n p -> M p n
_ᵀ = transpose

transpose-involutive : ∀ {n p} (A : M n p) -> ((A ᵀ) ᵀ) ≡ A
transpose-involutive A =
  begin
    ((A ᵀ)ᵀ)
  ≡⟨⟩
    (tabulate λ i j -> (tabulate λ i′ j′ -> A ⟪ j′ , i′ ⟫) ⟪ j , i ⟫)
  ≡⟨ tabulate-cong-≡ (λ i j → lookup∘tabulate (λ i′ j′ -> A ⟪ j′ , i′ ⟫) j i) ⟩
    (tabulate λ i j -> A ⟪ i , j ⟫)
  ≡⟨ tabulate∘lookup A ⟩
    A
  ∎
  where open import Relation.Binary.PropositionalEquality as Eq
        open Eq.≡-Reasoning

map : ∀ {n p} -> (K' -> K') -> M n p -> M n p
map f = V.map (V.map f)

mapRows : ∀ {n p q} -> (V.Vec K' p -> V.Vec K' q) -> M n p -> M n q
mapRows = V.map

mapCols : ∀ {n m p} -> (V.Vec K' n -> V.Vec K' m) -> M n p -> M m p
mapCols f A = (V.map f (A ᵀ)) ᵀ

map-cong : ∀ {n p} {f g : K' -> K'} -> f ≗ g -> map {n} {p} f ≗ map g
map-cong r = VP.map-cong (VP.map-cong r)

mapRows-cong : ∀ {n p q} {f g : V.Vec K' p -> V.Vec K' q}
             -> f ≗ g -> mapRows {n} f ≗ mapRows g
mapRows-cong = VP.map-cong

mapCols-cong : ∀ {n m p} {f g : V.Vec K' n -> V.Vec K' m}
             -> f ≗ g -> mapCols {n} {m} {p} f ≗ mapCols g
mapCols-cong r A = P.cong transpose (VP.map-cong r (transpose A))

open import Data.Nat.DivMod

_+_ : ∀ {n p} -> FP.Op₂ (M n p)
_+_ = zipWith V._+_

_∙_ : ∀ {n p} -> ScalarMultiplication K' (M n p)
_∙_ k = V.map (k V.∙_)

-_ : ∀ {n p} -> FP.Op₁ (M n p)
-_ = V.map V.-_

0# : ∀ {n p} -> M n p
0# = replicate V.0#

+-cong : ∀ {n p} {A B C D : M n p} -> A ≈ B -> C ≈ D -> (A + C) ≈ (B + D)
+-cong PW.[] PW.[] = PW.[]
+-cong (r₁ PW.∷ rs₁) (r₂ PW.∷ rs₂) = V.+-cong r₁ r₂ PW.∷ +-cong rs₁ rs₂

+-assoc : ∀ {n p} (A B C : M n p) -> ((A + B) + C) ≈ (A + (B + C))
+-assoc V.[] V.[] V.[] = PW.[]
+-assoc (u V.∷ us) (v V.∷ vs) (w V.∷ ws) =
  V.+-assoc u v w PW.∷ +-assoc us vs ws

+-identityˡ : ∀ {n p} (A : M n p) -> (0# + A) ≈ A
+-identityˡ V.[] = PW.[]
+-identityˡ (u V.∷ us) = V.+-identityˡ u PW.∷ +-identityˡ us

+-identityʳ : ∀ {n p} (A : M n p) -> (A + 0#) ≈ A
+-identityʳ V.[] = PW.[]
+-identityʳ (u V.∷ us) = V.+-identityʳ u PW.∷ +-identityʳ us

+-identity : ∀ {n p} -> ((∀ (A : M n p) -> ((0# + A) ≈ A)) × (∀ (A : M n p) -> ((A + 0#) ≈ A)))
+-identity = +-identityˡ , +-identityʳ

+-comm : ∀ {n p} (A B : M n p) -> (A + B) ≈ (B + A)
+-comm V.[] V.[] = PW.[]
+-comm (u V.∷ us) (v V.∷ vs) = (V.+-comm u v) PW.∷ (+-comm us vs)

*ᵏ-∙-compat : ∀ {n p} (a b : K') (A : M n p) -> ((a *ᵏ b) ∙ A) ≈ (a ∙ (b ∙ A))
*ᵏ-∙-compat a b V.[] = PW.[]
*ᵏ-∙-compat a b (u V.∷ us) = (V.*ᵏ-∙-compat a b u) PW.∷ (*ᵏ-∙-compat a b us)

∙-+-distrib : ∀ {n p} (a : K') (A B : M n p) -> (a ∙ (A + B)) ≈ ((a ∙ A) + (a ∙ B))
∙-+-distrib a V.[] V.[] = PW.[]
∙-+-distrib a (u V.∷ us) (v V.∷ vs) = (V.∙-+-distrib a u v) PW.∷ (∙-+-distrib a us vs)

∙-+ᵏ-distrib : ∀ {n p} (a b : K') (A : M n p) -> ((a +ᵏ b) ∙ A) ≈ ((a ∙ A) + (b ∙ A))
∙-+ᵏ-distrib a b V.[] = PW.[]
∙-+ᵏ-distrib a b (u V.∷ us) = (V.∙-+ᵏ-distrib a b u) PW.∷ (∙-+ᵏ-distrib a b us)

∙-cong : ∀ {n p} {a b : K'} {A B : M n p} → a ≈ᵏ b -> A ≈ B -> (a ∙ A) ≈ (b ∙ B)
∙-cong rᵏ PW.[] = PW.[]
∙-cong rᵏ (r PW.∷ rs) = (V.∙-cong rᵏ r) PW.∷ (∙-cong rᵏ rs)

∙-identity : ∀ {n p} (A : M n p) → (1ᵏ ∙ A) ≈ A
∙-identity V.[] = PW.[]
∙-identity (u V.∷ us) = (V.∙-identity u) PW.∷ (∙-identity us)

∙-absorbˡ : ∀ {n p} (A : M n p) → (0ᵏ ∙ A) ≈ 0#
∙-absorbˡ V.[] = PW.[]
∙-absorbˡ (u V.∷ us) = (V.∙-absorbˡ u) PW.∷ (∙-absorbˡ us)

-‿inverseˡ : ∀ {n p} (A : M n p) -> ((- A) + A) ≈ 0#
-‿inverseˡ V.[] = PW.[]
-‿inverseˡ (u V.∷ us) = (V.-‿inverseˡ u) PW.∷ (-‿inverseˡ us)

-‿inverseʳ : ∀ {n p} (A : M n p) -> (A + (- A)) ≈ 0#
-‿inverseʳ V.[] = PW.[]
-‿inverseʳ (u V.∷ us) = (V.-‿inverseʳ u) PW.∷ (-‿inverseʳ us)

-‿inverse : ∀ {n p} → (∀ (A : M n p) -> ((- A) + A) ≈ 0#) × (∀ (A : M n p) -> (A + (- A)) ≈ 0#)
-‿inverse = -‿inverseˡ , -‿inverseʳ

-‿cong : ∀ {n p} {A B : M n p} -> A ≈ B -> (- A) ≈ (- B)
-‿cong PW.[] = PW.[]
-‿cong (r PW.∷ rs) = (V.-‿cong r) PW.∷ (-‿cong rs)

concat-+ : ∀ {n p} (A B : M n p) -> V.concat (V.zipWith V._+_ A B) V.≈ (V.concat A) +v (V.concat B)
concat-+ {0} {p} V.[] V.[] =
  V.≈-trans (PW.concat⁺ {m = p} {p = 0} PW.[]) (V.≈-sym (V.+-identityˡ V.[]))
concat-+ {suc n} {p} (u V.∷ us) (v V.∷ vs) =
  begin
    V.concat (V.zipWith V._+_ (u V.∷ us) (v V.∷ vs))
  ≡⟨⟩
    (u V.+ v) V.++ V.concat (V.zipWith V._+_ us vs)
  ≈⟨ V.++-cong V.≈-refl (concat-+ {n} {p} us vs) ⟩
    (u V.+ v) V.++ (V.concat us V.+ V.concat vs)
  ≈⟨ V.≈-sym (V.+-++-distrib u (V.concat us) v (V.concat vs)) ⟩
    (V.concat (u V.∷ us)) V.+ (V.concat (v V.∷ vs))
  ∎
  where open import Relation.Binary.EqReasoning (V.setoid (p +ℕ n *ℕ p))

concat-0# : ∀ {n p} -> V.concat (0# {n} {p}) V.≈ (V.0# {n *ℕ p})
concat-0# {0} = PW.[]
concat-0# {suc n} {p} =
  begin
    V.concat (0# {suc n} {p})
  ≡⟨⟩
    V.0# {p} V.++ V.concat (0# {n} {p})
  ≈⟨ PW.++⁺ V.≈-refl (concat-0# {n} {p}) ⟩
    V.0# {p} V.++ V.0# {n *ℕ p}
  ≈⟨ V.0++0≈0 {p} {n *ℕ p} ⟩
    V.0# {p +ℕ n *ℕ p}
  ∎
  where open import Relation.Binary.EqReasoning (V.setoid (p +ℕ n *ℕ p))

concat-∙ : ∀ {n p} (c : K') (A : M n p) -> V.concat (c ∙ A) V.≈ (c V.∙ V.concat A)
concat-∙ {0} c V.[] = PW.[]
concat-∙ {suc n} {p} c (u V.∷ us) =
  begin
    V.concat ((c V.∙ u) V.∷ (c ∙ us))
  ≡⟨⟩
    (c V.∙ u) V.++ (V.concat (c ∙ us))
  ≈⟨ V.++-cong V.≈-refl (concat-∙ {n} {p} c us) ⟩
    (c V.∙ u) V.++ (c V.∙ V.concat us)
  ≈⟨ V.≈-sym (V.∙-++-distrib c u (V.concat us)) ⟩
    c V.∙ V.concat (u V.∷ us)
  ∎
  where open import Relation.Binary.EqReasoning (V.setoid (p +ℕ n *ℕ p))

I : ∀ {n p} -> M n p
I = tabulate δ

_*_ : ∀ {n p q} -> M n p -> M p q -> M n q
A * B = tabulate λ i j -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ (B ⟪ k , j ⟫)

*-cong : ∀ {n p q} {A B : M n p} {C D : M p q}
       -> A ≈ B -> C ≈ D -> (A * C) ≈ (B * D)
*-cong {n} {q = q} {A} {B} {C} {D} r₁ r₂ =
  begin
    A * C
  ≡⟨⟩
    tabulate (λ i j -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ (C ⟪ k , j ⟫))
  ≈⟨ tabulate⁺ (λ i j -> V.sum-tab-cong λ k → *ᵏ-cong (lookup-cong i k r₁) (lookup-cong k j r₂)) ⟩
    B * D
  ∎
  where open import Relation.Binary.EqReasoning (setoid {n} {q})

*-assoc : ∀ {n p q r} (A : M n p) (B : M p q) (C : M q r)
        -> ((A * B) * C) ≈ (A * (B * C))
*-assoc {n} {r = r} A B C = tabulate⁺ λ i j ->
  begin
    V.sum-tab (λ k′ -> ((A * B) ⟪ i , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫))
  ≈⟨ V.sum-tab-cong (λ k′ -> *ᵏ-cong (≈ᵏ-reflexive (lookup∘tabulate
                   (λ i′ j′ -> V.sum-tab λ k -> (A ⟪ i′ , k ⟫) *ᵏ (B ⟪ k , j′ ⟫)) i k′)) ≈ᵏ-refl) ⟩
    V.sum-tab (λ k′ -> (V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ (B ⟪ k , k′ ⟫)) *ᵏ (C ⟪ k′ , j ⟫))
  ≈⟨ V.sum-tab-cong (λ k′ -> V.*ᵏ-sum-tab-distribʳ (C ⟪ k′ , j ⟫) λ k -> (A ⟪ i , k ⟫) *ᵏ (B ⟪ k , k′ ⟫)) ⟩
    V.sum-tab (λ k′ -> V.sum-tab λ k -> ((A ⟪ i , k ⟫) *ᵏ (B ⟪ k , k′ ⟫)) *ᵏ (C ⟪ k′ , j ⟫))
  ≈⟨ V.sum-tab-cong (λ k′ -> V.sum-tab-cong λ k -> *ᵏ-assoc (A ⟪ i , k ⟫) (B ⟪ k , k′ ⟫) (C ⟪ k′ , j ⟫)) ⟩
    V.sum-tab (λ k′ -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ ((B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)))
  ≈⟨ V.sum-tab-cong (λ k′ -> V.sum-tab-cong λ k -> *ᵏ-comm (A ⟪ i , k ⟫) ((B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫))) ⟩
    V.sum-tab (λ k′ -> V.sum-tab λ k -> ((B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)) *ᵏ (A ⟪ i , k ⟫))
  ≈⟨ V.sum-tab-swap (λ k k′ -> (B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)) (λ k -> A ⟪ i , k ⟫) ⟩
    V.sum-tab (λ k -> V.sum-tab λ k′ -> ((B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)) *ᵏ (A ⟪ i , k ⟫))
  ≈⟨ V.sum-tab-cong (λ k -> ≈ᵏ-trans
                       (≈ᵏ-sym (V.*ᵏ-sum-tab-distribʳ (A ⟪ i , k ⟫) λ k′ -> (B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)))
                       (*ᵏ-comm (V.sum-tab λ k′ -> (B ⟪ k , k′ ⟫) *ᵏ (C ⟪ k′ , j ⟫)) (A ⟪ i , k ⟫))) ⟩
    V.sum-tab (λ k -> (A ⟪ i , k ⟫) *ᵏ V.sum-tab (λ k′ -> (B ⟪ k , k′ ⟫) *ᵏ  (C ⟪ k′ , j ⟫)))
  ≈⟨ V.sum-tab-cong (λ k -> *ᵏ-cong ≈ᵏ-refl
                   (≈ᵏ-sym (≈ᵏ-reflexive (lookup∘tabulate
                     (λ i′ j′ -> V.sum-tab λ k′ -> (B ⟪ i′ , k′ ⟫) *ᵏ (C ⟪ k′ , j′ ⟫)) k j)))) ⟩
    V.sum-tab (λ k -> (A ⟪ i , k ⟫) *ᵏ ((B * C) ⟪ k , j ⟫))
  ∎
  where open import Relation.Binary.EqReasoning (Field.setoid K)

*-identityˡ : ∀ {n p} (A : M n p) -> I * A ≈ A
*-identityˡ {n} {p} A =
  begin
    I * A
  ≡⟨⟩
    tabulate (λ i j -> V.sum-tab λ k -> (I ⟪ i , k ⟫) *ᵏ (A ⟪ k , j ⟫))
  ≈⟨ tabulate-cong (λ i j -> V.sum-tab-cong {n} λ k -> *ᵏ-cong (≈ᵏ-reflexive (lookup∘tabulate δ i k)) ≈ᵏ-refl) ⟩
    tabulate (λ i j -> V.sum-tab λ k -> δ i k *ᵏ (A ⟪ k , j ⟫))
  ≈⟨ tabulate-cong (λ i j -> V.sum-tab-δ (λ k -> A ⟪ k , j ⟫) i) ⟩
    tabulate (λ i j -> A ⟪ i , j ⟫)
  ≡⟨ tabulate∘lookup A ⟩
    A
  ∎
  where open import Relation.Binary.EqReasoning (setoid {n} {p})

*-identityʳ : ∀ {n p} (A : M n p) -> A * I ≈ A
*-identityʳ {n} {p} A =
  begin
    A * I
  ≡⟨⟩
    tabulate (λ i j -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ (I ⟪ k , j ⟫))
  ≈⟨ tabulate-cong (λ i j -> V.sum-tab-cong {p} λ k -> *ᵏ-cong ≈ᵏ-refl (≈ᵏ-reflexive (lookup∘tabulate δ k j))) ⟩
    tabulate (λ i j -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ δ k j)
  ≈⟨ tabulate-cong (λ i j -> V.sum-tab-cong {p} λ k -> *ᵏ-cong ≈ᵏ-refl (δ-comm k j)) ⟩
    tabulate (λ i j -> V.sum-tab λ k -> (A ⟪ i , k ⟫) *ᵏ δ j k)
  ≈⟨ tabulate-cong (λ i j -> ≈ᵏ-trans (V.sum-tab-cong {p} (λ k -> *ᵏ-comm ((A ⟪ i , k ⟫)) (δ j k)))
                                      (V.sum-tab-δ (λ k -> A ⟪ i , k ⟫) j)) ⟩
    tabulate (λ i j -> A ⟪ i , j ⟫)
  ≡⟨ tabulate∘lookup A ⟩
    A
  ∎
  where open import Relation.Binary.EqReasoning (setoid {n} {p})

module _ {n p} where
  open IsEquivalence (≈-isEquiv {n} {p}) public
    using ()
    renaming
      ( refl  to ≈-refl
      ; sym   to ≈-sym
      ; trans to ≈-trans
      )

  open FP (_≈_ {n} {p})

  open import Algebra.Structures (_≈_ {n} {p})
  open import Algebra.Linear.Structures.Bundles

  isMagma : IsMagma _+_
  isMagma = record
    { isEquivalence = ≈-isEquiv
    ; ∙-cong        = +-cong
    }

  isSemigroup : IsSemigroup _+_
  isSemigroup = record
    { isMagma = isMagma
    ; assoc   = +-assoc
    }

  isMonoid : IsMonoid _+_ 0#
  isMonoid = record
    { isSemigroup = isSemigroup
    ; identity    = +-identity
    }

  isGroup : IsGroup _+_ 0# -_
  isGroup = record
    { isMonoid = isMonoid
    ; inverse  = -‿inverse
    ; ⁻¹-cong   = -‿cong
    }

  isAbelianGroup : IsAbelianGroup _+_ 0# -_
  isAbelianGroup = record
    { isGroup = isGroup
    ; comm    = +-comm
    }

  open VS K

  isVectorSpace : VS.IsVectorSpace K (_≈_ {n}) _+_ _∙_ -_ 0#
  isVectorSpace = record
    { isAbelianGroup  = isAbelianGroup
    ; *ᵏ-∙-compat     = *ᵏ-∙-compat
    ; ∙-+-distrib     = ∙-+-distrib
    ; ∙-+ᵏ-distrib    = ∙-+ᵏ-distrib
    ; ∙-cong          = ∙-cong
    ; ∙-identity      = ∙-identity
    ; ∙-absorbˡ        = ∙-absorbˡ
    }

  vectorSpace : VectorSpace K k (k ⊔ ℓ)
  vectorSpace = record { isVectorSpace = isVectorSpace }

  open import Algebra.Linear.Structures.FiniteDimensional K
  open import Algebra.Linear.Morphism.VectorSpace K
  open import Algebra.Linear.Morphism.Bundles K

  open import Algebra.Morphism.Definitions (M n p) (Vec K' (n *ℕ p)) V._≈_
  open import Algebra.Linear.Morphism.Definitions K (M n p) (Vec K' (n *ℕ p)) V._≈_
  import Relation.Binary.Morphism.Definitions (M n p) (Vec K' (n *ℕ p)) as R
  open import Function
  open import Relation.Binary.EqReasoning (V.setoid (n *ℕ p))

  ⟦_⟧ : M n p -> Vec K' (n *ℕ p)
  ⟦_⟧ = V.concat

  ⟦⟧-cong : R.Homomorphic₂ _≈_ (V._≈_ {n *ℕ p}) ⟦_⟧
  ⟦⟧-cong = PW.concat⁺

  +-homo : Homomorphic₂ ⟦_⟧ _+_ _+v_
  +-homo = concat-+

  0#-homo : Homomorphic₀ ⟦_⟧ 0# V.0#
  0#-homo = concat-0# {n} {p}

  ∙-homo : ScalarHomomorphism ⟦_⟧ _∙_ _∙v_
  ∙-homo = concat-∙

  ⟦⟧-injective : Injective (_≈_ {n} {p}) (V._≈_ {n *ℕ p}) ⟦_⟧
  ⟦⟧-injective {A} {B} r = PW.concat⁻ A B r

  ⟦⟧-surjective : Surjective (_≈_ {n} {p}) (V._≈_ {n *ℕ p}) ⟦_⟧
  ⟦⟧-surjective v = fromVec {n} {p} v , concat∘fromVec {n} {p} v

  embed : LinearIsomorphism vectorSpace (V.vectorSpace {n *ℕ p})
  embed = record
    { ⟦_⟧ = ⟦_⟧
    ; isLinearIsomorphism = record
      { isLinearMonomorphism = record
        { isLinearMap = record
          { isAbelianGroupMorphism = record
            { gp-homo = record
              { mn-homo = record
                { sm-homo = record
                  { ⟦⟧-cong = ⟦⟧-cong
                  ; ∙-homo = +-homo
                  }
                ; ε-homo = 0#-homo
                }
              }
            }
          ; ∙-homo = ∙-homo
          }
        ; injective = ⟦⟧-injective
        }
      ; surjective = ⟦⟧-surjective
      }
    }

  isFiniteDimensional : IsFiniteDimensional _≈_ _+_ _∙_ -_ 0# (n *ℕ p)
  isFiniteDimensional = record
    { isVectorSpace = isVectorSpace
    ; embed         = embed
    }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


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

open import Setoids.Setoids
open import Groups.Definition
open import Groups.Subgroups.Definition
open import Groups.Actions.Definition
open import Sets.EquivalenceRelations
open import Groups.Actions.Definition

module Groups.Actions.Stabiliser {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (act : GroupAction G T) where

open GroupAction act
open Setoid T

stabiliserPred : (x : B) → (g : A) → Set d
stabiliserPred x g = (action g x) ∼ x

stabiliserWellDefined : (x : B) → {g h : A} → Setoid._∼_ S g h → (stabiliserPred x g) → stabiliserPred x h
stabiliserWellDefined x {g} {h} g=h gx=x = transitive (actionWellDefined1 (Equivalence.symmetric (Setoid.eq S) g=h)) gx=x
  where
    open Equivalence eq

open Setoid T
open Equivalence (Setoid.eq T)

stabiliserSubgroup : (x : B) → Subgroup G (stabiliserPred x)
Subgroup.isSubset (stabiliserSubgroup x) = stabiliserWellDefined x
Subgroup.closedUnderPlus (stabiliserSubgroup x) gx=x hx=x = transitive associativeAction (transitive (actionWellDefined2 hx=x) gx=x)
Subgroup.containsIdentity (stabiliserSubgroup x) = identityAction
Subgroup.closedUnderInverse (stabiliserSubgroup x) {g} gx=x = transitive (transitive (transitive (actionWellDefined2 (symmetric gx=x)) (symmetric associativeAction)) (actionWellDefined1 (invLeft {g}))) identityAction
  where
    open Group G

ext: agda


text:
module TelescopingLet3 where

module Star where
  ★ : Set₁
  ★ = Set

  ★₁ : Set₂
  ★₁ = Set₁

module MEndo (open Star) (A : ★) where
  Endo = A → A

-- at this point, ★ should no longer be in scope

data D3 (open Star using (★₁)) : ★₁ where
  c : (A : ★) → D3
-- ★₁ is in scope
-- ★ is not in scope since it was not brought in scope
-- (not included in the using ())

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
variable {A} : Set _

id : A → A
id a = a

test : Set₁
test = id {A = Set₁} Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

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

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

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

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

open Closed Cl

private
  open Category C
  α⇒ = associator.from
  α⇐ = associator.to
  module ℱ = Functor
  module ⊗ = Functor ⊗

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

open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl
open import Categories.Category.Monoidal.Closed.IsClosed.L Cl

private
  id² : {S T : Obj} → [ S , T ]₀ ⇒ [ S , T ]₀
  id² = [ id , id ]₁

L-dinatural-comm :  ∀ {X′ Y Z X f} → [ [ f , id ]₁ , id² ]₁ ∘ L X′ Y Z ≈ [ id² , [ f , id ]₁ ]₁ ∘ L X Y Z
L-dinatural-comm {X′} {Y} {Z} {X} {f} = begin
  [ fˡ , id² ]₁ ∘ L X′ Y Z                              ≈⟨ [-,-].F-resp-≈ (refl , [-,-].identity) ⟩∘⟨refl ⟩
  [ fˡ , id ]₁ ∘ L X′ Y Z                               ≈˘⟨ pushˡ [ [-,-] ]-commute ⟩
  ([ id , 𝕃 L-inner ]₁ ∘ [ fˡ , id ]₁) ∘ η.η YZ         ≈˘⟨ pushʳ (mate.commute₁ [ f , id ]₁) ⟩
  [ id , 𝕃 L-inner ]₁ ∘ 𝕃 (id ⊗₁ fˡ)                    ≈˘⟨ pushˡ (ℱ.homomorphism [ XY ,-]) ⟩
  𝕃 (𝕃 L-inner ∘ id ⊗₁ fˡ)                              ≈˘⟨ 𝕃-resp-≈ 𝕃-comm′ ⟩
  𝕃 (𝕃 $ L-inner ∘ (id ⊗₁ fˡ) ⊗₁ id)                   ≈⟨ 𝕃-resp-≈ $ 𝕃-resp-≈ push-f-right ⟩
  𝕃 (𝕃 $ L-inner ∘ (id ⊗₁ id) ⊗₁ f)                    ≈⟨ 𝕃-resp-≈ $ pushˡ (ℱ.homomorphism [ X′ ,-]) ⟩
  𝕃 ([ id , L-inner {X} ]₁ ∘ 𝕃 ((id ⊗₁ id) ⊗₁ f))       ≈⟨ 𝕃-resp-≈ $ ∘-resp-≈ʳ (∘-resp-≈ˡ (X′-resp-≈ (⊗.F-resp-≈ (⊗.identity , refl))) ○ mate.commute₁ f) ⟩
  𝕃 ([ id , L-inner {X} ]₁ ∘ fˡ ∘ η.η (YZ ⊗₀ XY))        ≈⟨ 𝕃-resp-≈ $ pullˡ [ [-,-] ]-commute ○ assoc ⟩
  𝕃 (fˡ ∘ 𝕃 L-inner)                                     ≈⟨ ∘-resp-≈ˡ (ℱ.homomorphism [ XY ,-]) ○ assoc ⟩
  [ id , fˡ ]₁ ∘ L X Y Z                                 ≈˘⟨ [-,-].F-resp-≈ ([-,-].identity , refl) ⟩∘⟨refl ⟩
  [ id² , fˡ ]₁ ∘ L X Y Z                                ∎
  where
  fˡ        : ∀ {W} → [ X , W ]₀ ⇒ [ X′ , W ]₀
  fˡ        = [ f , id ]₁
  XY        = [ X , Y ]₀
  YZ        = [ Y , Z ]₀
  X′-resp-≈ = ℱ.F-resp-≈ [ X′ ,-]
  L-inner     : ∀ {W} → ([ Y , Z ]₀ ⊗₀ [ W , Y ]₀) ⊗₀ W ⇒ Z
  L-inner {W} = ε.η Z ∘ (id ⊗₁ ε.η {W} Y) ∘ α⇒
  push-f-right : (ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ α⇒) ∘ (id ⊗₁ fˡ) ⊗₁ id ≈ (ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ α⇒) ∘ (id ⊗₁ id) ⊗₁ f
  push-f-right = begin
    (ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ α⇒) ∘ (id ⊗₁ fˡ) ⊗₁ id     ≈⟨ pull-last assoc-commute-from ⟩
    ε.η Z ∘ (id ⊗₁ ε.η Y) ∘ id ⊗₁ fˡ ⊗₁ id ∘ α⇒         ≈˘⟨ refl⟩∘⟨ pushˡ (ℱ.homomorphism (YZ ⊗-)) ⟩
    ε.η Z ∘ id ⊗₁ (ε.η Y ∘ fˡ ⊗₁ id) ∘ α⇒               ≈⟨ refl⟩∘⟨ ℱ.F-resp-≈ (YZ ⊗-) (mate.commute₂ f) ⟩∘⟨refl ⟩
    ε.η Z ∘ id ⊗₁ (ε.η Y ∘ id ⊗₁ f) ∘ α⇒                ≈⟨ refl⟩∘⟨ ℱ.homomorphism (YZ ⊗-) ⟩∘⟨refl ⟩
    ε.η Z ∘ (id ⊗₁ ε.η Y ∘ id ⊗₁ id ⊗₁ f) ∘ α⇒          ≈⟨ center⁻¹ refl (⟺ assoc-commute-from) ○ pullˡ assoc ⟩
    (ε.η Z ∘ id ⊗₁ ε.η Y ∘ α⇒) ∘ (id ⊗₁ id) ⊗₁ f        ∎

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
-- Andreas, 2016-10-11, AIM XXIV
-- COMPILED pragma accidentially also accepted for abstract definitions

open import Common.String

data Unit : Set where
  unit : Unit

{-# COMPILED_DATA Unit () () #-}

postulate
  IO : Set → Set
  doNothing : IO Unit

{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}
{-# COMPILED doNothing (return ()) #-}

{-# IMPORT Data.Text.IO #-}

abstract
  putStrLn : String → IO Unit
  putStrLn _ = doNothing

{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}

main = putStrLn "Hello, world!"

-- WAS: compiler produced ill-formed Haskell-code
-- NOW: Error on COMPILED pragma

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
postulate
  A : Set

data D : Set → Set₁ where
  d : (A : Set) → D A

f : Set → (D A → Set) → Set
f A f = f (d A)

-- Expected error:
-- A != A of type Set
-- (because one is a variable and one a defined identifier)
-- when checking that the pattern d A has type D A

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Numeral.Natural.Relation.Order.Existence.Proofs where

import Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Induction
open import Numeral.Natural.Relation.Order.Existence
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Structure.Operator
open import Structure.Operator.Properties
import      Structure.Relator.Names as Names
open import Structure.Relator.Ordering
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

[≡]-to-[≤] : ∀{x y : ℕ} → (x ≡ y) → (x ≤ y)
[≡]-to-[≤] x≡y = [∃]-intro 0 ⦃ x≡y ⦄

[≤]-minimum : ∀{x : ℕ} → (0 ≤ x)
[≤]-minimum {x} = [∃]-intro x ⦃ identityₗ(_+_)(𝟎) ⦄

[≤][0]ᵣ : ∀{x : ℕ} → (x ≤ 0) ↔ (x ≡ 0)
[≤][0]ᵣ {𝟎}    = [↔]-intro [≡]-to-[≤] (const [≡]-intro)
[≤][0]ᵣ {𝐒(n)} = [↔]-intro (\()) (\{([∃]-intro _ ⦃ ⦄ )})

[≤][0]ᵣ-negation : ∀{x : ℕ} → ¬(𝐒(x) ≤ 0)
[≤][0]ᵣ-negation {x} (Sx≤0) = [𝐒]-not-0([↔]-to-[→] ([≤][0]ᵣ {𝐒(x)}) (Sx≤0))

[≤]-successor : ∀{a b : ℕ} → (a ≤ b) → (a ≤ 𝐒(b))
[≤]-successor ([∃]-intro(n) ⦃ proof ⦄) = [∃]-intro (𝐒(n)) ⦃ [≡]-with(𝐒) (proof) ⦄

[≤]-predecessor : ∀{a b : ℕ} → (𝐒(a) ≤ b) → (a ≤ b)
[≤]-predecessor ([∃]-intro n) = [∃]-intro(𝐒(n))

[≤]-without-[𝐒] : ∀{a b : ℕ} → (a ≤ b) ← (𝐒(a) ≤ 𝐒(b))
[≤]-without-[𝐒] {𝟎}   {b}    (_)                      = [≤]-minimum
[≤]-without-[𝐒] {𝐒(a)}{𝟎}    ()
[≤]-without-[𝐒] {𝐒(a)}{𝐒(b)} ([∃]-intro(n) ⦃ proof ⦄) = [≤]-with-[𝐒] {a}{b} ([≤]-without-[𝐒] {a}{b} ([∃]-intro(n) ⦃ injective(𝐒) proof ⦄))

[≤][𝐒]ₗ : ∀{x : ℕ} → ¬(𝐒(x) ≤ x)
[≤][𝐒]ₗ {𝟎}    (1≤0)    = [≤][0]ᵣ-negation{0}(1≤0)
[≤][𝐒]ₗ {𝐒(n)} (SSn≤Sn) = [≤][𝐒]ₗ {n} ([≤]-without-[𝐒] {𝐒(n)}{n} (SSn≤Sn))

instance
  [≤]-transitivity : Transitivity (_≤_)
  Transitivity.proof [≤]-transitivity {a}{b}{c} ([∃]-intro n₁ ⦃ an₁b ⦄) ([∃]-intro n₂ ⦃ bn₂c ⦄) = [∃]-intro (n₁ + n₂) ⦃ p ⦄ where
    p =
      a + (n₁ + n₂) 🝖[ _≡_ ]-[ associativity(_+_) {a}{n₁}{n₂} ]-sym
      (a + n₁) + n₂ 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(n₂) an₁b ]
      b + n₂        🝖[ _≡_ ]-[ bn₂c ]
      c             🝖-end

instance
  [≤]-reflexivity : Reflexivity (_≤_)
  Reflexivity.proof [≤]-reflexivity = [≡]-to-[≤] [≡]-intro

instance
  [≤]-antisymmetry : Antisymmetry (_≤_) (_≡_)
  Antisymmetry.proof [≤]-antisymmetry {a} {b} ([∃]-intro(n₁) ⦃ an₁b ⦄) ([∃]-intro(n₂) ⦃ bn₂a ⦄) =
    a      🝖[ _≡_ ]-[]
    a + 𝟎  🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(a) n₁0 ]-sym
    a + n₁ 🝖[ _≡_ ]-[ an₁b ]
    b      🝖-end
    where
      n₁n₂0 : (n₁ + n₂ ≡ 0)
      n₁n₂0 = cancellationₗ(_+_) $
        a + (n₁ + n₂) 🝖[ _≡_ ]-[ associativity(_+_) {a}{n₁}{n₂} ]-sym
        (a + n₁) + n₂ 🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(n₂) an₁b ]
        b + n₂        🝖[ _≡_ ]-[ bn₂a ]
        a             🝖[ _≡_ ]-[]
        a + 0         🝖-end

      n₁0 : (n₁ ≡ 0)
      n₁0 = [∧]-elimₗ ([+]-sum-is-0 {n₁} {n₂} n₁n₂0)

instance
  [≤]-weakPartialOrder : Weak.PartialOrder (_≤_) (_≡_)
  [≤]-weakPartialOrder = record{}

[<]-minimum : ∀{x : ℕ} → (0 < 𝐒(x))
[<]-minimum = [≤]-with-[𝐒] {0} [≤]-minimum

[≥]-is-[≮] : ∀{a b : ℕ} → ¬(a < b) ← (a ≥ b)
[≥]-is-[≮] {a}{b} b≤a Sa≤b = [≤][𝐒]ₗ (transitivity(_≤_) {x = 𝐒(a)}{y = b}{z = a} Sa≤b b≤a)

-- [≤]-is-[≯] : ∀{a b : ℕ} → ¬(a > b) ← (a ≤ b)
-- [≤]-is-[≯] {a}{b} = [≥]-is-[≮] {b}{a}

-- [>]-is-[≰] : ∀{a b : ℕ} → ¬(a ≤ b) ← (a > b)
-- [>]-is-[≰] {a}{b} (Sb≤a) (a≤b) = [≤]-is-[≯] {a}{b} (a≤b) (Sb≤a)

-- [<]-is-[≱] : ∀{a b : ℕ} → ¬(a ≥ b) ← (a < b)
-- [<]-is-[≱] {a}{b} = [>]-is-[≰] {b}{a}

instance
  [≤]-totality : ConverseTotal(_≤_)
  [≤]-totality = intro p where
    p : Names.ConverseTotal(_≤_)
    p {𝟎}   {𝟎}    = [∨]-introₗ ([≡]-to-[≤] [≡]-intro)
    p {𝐒(a)}{𝟎}    = [∨]-introᵣ ([≤]-minimum)
    p {𝟎}   {𝐒(b)} = [∨]-introₗ ([≤]-minimum)
    p {𝐒(a)}{𝐒(b)} = [∨]-elim ([∨]-introₗ ∘ ([≤]-with-[𝐒] {a}{b})) ([∨]-introᵣ ∘ ([≤]-with-[𝐒] {b}{a})) (p {a}{b})

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:
------------------------------------------------------------------------
-- Propositional (intensional) equality
------------------------------------------------------------------------

module Relation.Binary.PropositionalEquality where

open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.FunctionSetoid
open import Data.Function
open import Data.Product

-- Some of the definitions can be found in the following modules:

open import Relation.Binary.Core public using (_≡_; refl; _≢_)
open import Relation.Binary.PropositionalEquality.Core public

------------------------------------------------------------------------
-- Some properties

subst₂ : ∀ {A B} (P : A → B → Set) →
         ∀ {x₁ x₂ y₁ y₂} → x₁ ≡ x₂ → y₁ ≡ y₂ → P x₁ y₁ → P x₂ y₂
subst₂ P refl refl p = p

subst₁ : ∀ {a} (P : a → Set₁) → ∀ {x y} → x ≡ y → P x → P y
subst₁ P refl p = p

cong : Congruential _≡_
cong = subst⟶cong refl subst

cong₂ : Congruential₂ _≡_
cong₂ = cong+trans⟶cong₂ cong trans

setoid : Set → Setoid
setoid a = record
  { carrier       = a
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence
  }

decSetoid : ∀ {a} → Decidable (_≡_ {a}) → DecSetoid
decSetoid dec = record
  { _≈_              = _≡_
  ; isDecEquivalence = record
      { isEquivalence = isEquivalence
      ; _≟_           = dec
      }
  }

isPreorder : ∀ {a} → IsPreorder {a} _≡_ _≡_
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  ; ∼-resp-≈      = resp₂ _≡_
  }

preorder : Set → Preorder
preorder a = record
  { carrier    = a
  ; _≈_        = _≡_
  ; _∼_        = _≡_
  ; isPreorder = isPreorder
  }

------------------------------------------------------------------------
-- Pointwise equality

infix 4 _≗_

_→-setoid_ : (A B : Set) → Setoid
A →-setoid B = A ≡⇨ λ _ → setoid B

_≗_ : ∀ {a b} (f g : a → b) → Set
_≗_ {a} {b} = Setoid._≈_ (a →-setoid b)

→-to-⟶ : ∀ {A B} → (A → B) → setoid A ⟶ setoid B
→-to-⟶ f = record { _⟨$⟩_ = f; pres = cong f }

------------------------------------------------------------------------
-- The inspect idiom

-- The inspect idiom can be used when you want to pattern match on the
-- result r of some expression e, and you also need to "remember" that
-- r ≡ e.

data Inspect {a : Set} (x : a) : Set where
  _with-≡_ : (y : a) (eq : y ≡ x) → Inspect x

inspect : ∀ {a} (x : a) → Inspect x
inspect x = x with-≡ refl

-- Example usage:

-- f x y with inspect (g x)
-- f x y | c z with-≡ eq = ...

------------------------------------------------------------------------
-- Convenient syntax for equational reasoning

import Relation.Binary.EqReasoning as EqR

-- Relation.Binary.EqReasoning is more convenient to use with _≡_ if
-- the combinators take the type argument (a) as a hidden argument,
-- instead of being locked to a fixed type at module instantiation
-- time.

module ≡-Reasoning where
  private
    module Dummy {a : Set} where
      open EqR (setoid a) public
        hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _≡⟨_⟩_)
  open Dummy public

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module _ where

open import Agda.Primitive

module _ (a ℓ ℓ' : Level) where

  mutual
    X : Level
    X = _  -- Agda 2.5.1.1 solves this level meta

    hyp : Set₁
    hyp with (lsuc ℓ')
    ... | _ = Set
      where
        X<=a : Set (X ⊔ a) → Set a
        X<=a A = A

    test : Set₁
    test with (lsuc ℓ)
    ... | _ = Set
      where
        a<=X : Set (X ⊔ a) → Set X
        a<=X A = A


text:
{-A
Polynomials over commutative rings
==================================
-}
{-# OPTIONS --safe #-}

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

module Cubical.Algebra.Polynomials.Univariate.Properties where

open import Cubical.HITs.PropositionalTruncation
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _Nat·_) hiding (·-comm)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty.Base renaming (rec to ⊥rec )
open import Cubical.Data.Bool

open import Cubical.Algebra.Group hiding (Bool)
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base

private
  variable
    ℓ ℓ' : Level

module PolyModTheory (R' : CommRing ℓ) where
  private
    R = fst R'

  open PolyMod R'
  open CommRingTheory R'
  open RingTheory (CommRing→Ring R')
  open GroupTheory (Ring→Group (CommRing→Ring R'))

  pattern [_] x = x ∷ []

---------------------------------------
-- Definition
-- Identity for addition of polynomials
---------------------------------------
  0P : Poly
  0P = []

  --ReplicatePoly(n,p) returns 0 ∷ 0 ∷ ... ∷ [] (n zeros)
  ReplicatePoly0 : (n : ℕ)  → Poly
  ReplicatePoly0 zero  = 0P
  ReplicatePoly0 (suc n) = 0r ∷ ReplicatePoly0 n

  --The empty polynomial has multiple equal representations on the form 0 + 0x + 0 x² + ...
  replicatePoly0Is0P : ∀ (n : ℕ) → ReplicatePoly0 n ≡ 0P
  replicatePoly0Is0P zero = refl
  replicatePoly0Is0P (suc n) = (cong (0r ∷_) (replicatePoly0Is0P n)) ∙ drop0

-----------------------------
-- Definition
-- subtraction of polynomials
-----------------------------
  Poly- : Poly → Poly
  Poly- [] = []
  Poly- (a ∷ p) = (- a) ∷ (Poly- p)
  Poly- (drop0 i) = (cong (_∷ []) (inv1g) ∙ drop0) i

  -- Double negation (of subtraction of polynomials) is the identity mapping
  Poly-Poly- : (p : Poly) → Poly- (Poly- p) ≡ p
  Poly-Poly- = ElimProp.f (λ x → Poly- (Poly- x) ≡ x)
                          refl
                          (λ a p e → cong (_∷ (Poly- (Poly- p)))
                                          (-Idempotent a) ∙ cong (a ∷_ ) (e))
                          (isSetPoly _ _)

---------------------------
-- Definition
-- addition for polynomials
---------------------------
  _Poly+_ : Poly → Poly → Poly
  p Poly+ [] = p
  [] Poly+ (drop0 i) = drop0 i
  [] Poly+ (b ∷ q) = b ∷ q
  (a ∷ p) Poly+ (b ∷ q) = (a + b) ∷ (p Poly+ q)
  (a ∷ p) Poly+ (drop0 i) = +Rid a i ∷ p
  (drop0 i) Poly+ (a ∷ q) = lem q i  where
                                 lem : ∀ q → (0r + a) ∷ ([] Poly+ q) ≡ a ∷ q
                                 lem = ElimProp.f (λ q → (0r + a) ∷ ([] Poly+ q) ≡ a ∷ q)
                                                  (λ i → (+Lid a i ∷ []))
                                                  (λ r p _ → λ i → +Lid a i ∷ r ∷ p )
                                                  (isSetPoly _ _)
  (drop0 i) Poly+ (drop0 j) =  isSet→isSet' isSetPoly  (cong ([_] ) (+Rid 0r)) drop0
                                                       (cong ([_] ) (+Lid 0r)) drop0 i j

  -- [] is the left identity for Poly+
  Poly+Lid : ∀ p → ([] Poly+ p ≡ p)
  Poly+Lid =  ElimProp.f (λ p → ([] Poly+ p ≡ p) )
                         refl
                         (λ r p prf → refl)
                         (λ x y → isSetPoly _ _ x y)

  -- [] is the right identity for Poly+
  Poly+Rid : ∀ p → (p Poly+ [] ≡ p)
  Poly+Rid p = refl

  --Poly+ is Associative
  Poly+Assoc : ∀ p q r → p Poly+ (q Poly+ r) ≡ (p Poly+ q) Poly+ r
  Poly+Assoc =
    ElimProp.f (λ p → (∀ q r → p Poly+ (q Poly+ r) ≡ (p Poly+ q) Poly+ r))
               (λ q r → Poly+Lid (q Poly+ r) ∙ cong (_Poly+ r)  (sym (Poly+Lid q)))
               (λ a p prf → ElimProp.f ((λ q → ∀ r → ((a ∷ p) Poly+ (q Poly+ r)) ≡
                                                   (((a ∷ p) Poly+ q) Poly+ r)))
                                       (λ r → cong ((a ∷ p) Poly+_) (Poly+Lid r))
                                       (λ b q prf2 →
                                       ElimProp.f
                                         (λ r → ((a ∷ p) Poly+ ((b ∷ q) Poly+ r)) ≡
                                                 ((a + b ∷ (p Poly+ q)) Poly+ r))
                                         refl
                                         (λ c r prfp → cong ((a + (b + c))∷_)
                                                            (prf q r) ∙
                                                            (cong (_∷ ((p Poly+ q) Poly+ r))
                                                                  (+Assoc a b c)))
                                         (isSetPoly _ _))
                                       λ x y i r → isSetPoly (x r i0) (y r i1) (x r) (y r) i)
                λ x y i q r  → isSetPoly _ _ (x q r) (y q r) i

  -- for any polynomial, p, the additive inverse is given by Poly- p
  Poly+Inverses : ∀ p → p Poly+ (Poly- p) ≡ []
  Poly+Inverses = ElimProp.f ( λ p → p Poly+ (Poly- p) ≡ [])
                             refl --(Poly+Lid (Poly- []))
                             (λ r p prf → cong (r + - r ∷_) prf ∙
                                          (cong (_∷ [])  (+Rinv r) ∙ drop0))
                             (isSetPoly _ _)

  --Poly+ is commutative
  Poly+Comm : ∀ p q → p Poly+ q ≡ q Poly+ p
  Poly+Comm = ElimProp.f (λ p → (∀ q → p Poly+ q ≡ q Poly+ p))
                         (λ q → Poly+Lid q)
                         (λ a p prf → ElimProp.f (λ q → ((a ∷ p) Poly+ q) ≡ (q Poly+ (a ∷ p)))
                                                 refl
                                                 (λ b q prf2 → cong (_∷ (p Poly+ q)) (+Comm a b) ∙
                                                               cong ((b + a) ∷_) (prf q))
                                                 (isSetPoly _ _)
                         )
                         (λ {p} → isPropΠ (λ q → isSetPoly (p Poly+ q) (q Poly+ p)))

--------------------------------------------------------------
-- Definition
-- multiplication of a polynomial by a (constant) ring element
--------------------------------------------------------------
  _PolyConst*_ : (R) → Poly → Poly
  r PolyConst* [] = []
  r PolyConst* (a ∷ p) = (r · a) ∷ (r PolyConst* p)
  r PolyConst* (drop0 i) = lem r i where
                                 lem : ∀ r → [ r · 0r ] ≡ []
                                 lem =  λ r → [ r · 0r ] ≡⟨ cong (_∷ []) (0RightAnnihilates r) ⟩
                                        [ 0r ] ≡⟨ drop0 ⟩
                                        [] ∎

  -- For any polynomial p we have: 0 _PolyConst*_ p = []
  0rLeftAnnihilatesPoly : ∀ q → 0r PolyConst* q ≡ [ 0r ]
  0rLeftAnnihilatesPoly = ElimProp.f (λ q → 0r PolyConst* q ≡ [ 0r ])
                                         (sym drop0)
                                         (λ r p prf → cong ((0r · r) ∷_) prf ∙
                                                      cong (_∷ [ 0r ]) (0LeftAnnihilates r) ∙
                                                      cong (0r ∷_) drop0 )
                                         λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: 1 _PolyConst*_ p = p
  PolyConst*Lid : ∀ q → 1r PolyConst* q ≡ q
  PolyConst*Lid = ElimProp.f (λ q → 1r PolyConst* q ≡ q ) refl
                             (λ a p prf → cong (_∷ (1r PolyConst* p)) (·Lid a) ∙
                                          cong (a ∷_) (prf) )
                             λ x y → isSetPoly _ _ x y

--------------------------------
-- Definition
-- Multiplication of polynomials
--------------------------------
  _Poly*_ : Poly → Poly → Poly
  [] Poly* q = []
  (a ∷ p) Poly* q = (a PolyConst* q) Poly+ (0r ∷ (p Poly* q))
  (drop0 i) Poly* q = lem q i where
                               lem : ∀ q → (0r PolyConst* q) Poly+ [ 0r ] ≡ []
                               lem = λ q → ((0r PolyConst* q) Poly+ [ 0r ]) ≡⟨ cong ( _Poly+ [ 0r ] ) (0rLeftAnnihilatesPoly q)⟩
                                           ([ 0r ] Poly+ [ 0r ]) ≡⟨ cong (_∷ []) 0Idempotent  ∙ drop0 ⟩
                                           [] ∎

--------------------
--Definition
--Identity for Poly*
--------------------
  1P : Poly
  1P = [ 1r ]

  -- For any polynomial p we have: p Poly* [] = []
  0PRightAnnihilates : ∀ q → 0P Poly* q ≡ 0P
  0PRightAnnihilates = ElimProp.f (λ q → 0P Poly* q ≡ 0P)
                                  refl
                                  (λ r p prf → prf)
                                  λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: [] Poly* p = []
  0PLeftAnnihilates : ∀ p → p Poly* 0P ≡ 0P
  0PLeftAnnihilates = ElimProp.f (λ p → p Poly* 0P ≡ 0P )
                                 refl
                                 (λ r p prf → cong (0r ∷_) prf ∙ drop0)
                                 λ x y → isSetPoly _ _ x y

  -- For any polynomial p we have: p Poly* [ 1r ] = p
  Poly*Lid : ∀ q → 1P Poly* q ≡ q
  Poly*Lid =
    ElimProp.f (λ q → 1P Poly* q ≡ q)
               drop0
               (λ r p prf → lemma r p)
               (λ x y → isSetPoly _ _ x y)
                 where
                 lemma : ∀ r p → 1r · r + 0r ∷ (1r PolyConst* p) ≡ r ∷ p
                 lemma =
                   λ r p → 1r · r + 0r ∷ (1r PolyConst* p) ≡⟨ cong (_∷ (1r PolyConst* p) )
                                                                   (+Rid (1r · r)) ⟩
                           1r · r ∷ (1r PolyConst* p) ≡⟨ cong (_∷ 1r PolyConst* p) (·Lid r) ⟩
                           r ∷ (1r PolyConst* p) ≡⟨ cong (r ∷_) (PolyConst*Lid p) ⟩
                           r ∷ p ∎

  -- Distribution of indeterminate: (p + q)x = px + qx
  XLDistrPoly+ : ∀ p q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q))
  XLDistrPoly+ =
    ElimProp.f (λ p → ∀ q → (0r ∷ (p Poly+ q)) ≡ ((0r ∷ p) Poly+ (0r ∷ q)) )
               (λ q → (cong (0r ∷_) (Poly+Lid q)) ∙
                      cong (0r ∷_) (sym (Poly+Lid q)) ∙
                      sym (cong (_∷ [] Poly+ q) (+Lid 0r)))
               (λ a p prf → ElimProp.f (λ q → 0r ∷ ((a ∷ p) Poly+ q) ≡
                                         ((0r ∷ a ∷ p) Poly+ (0r ∷ q)))
                                       (cong (_∷ a ∷ p ) (sym (+Lid 0r)))
                                       (λ b q prf2 → cong (_∷ a + b ∷ (p Poly+ q)) (sym (+Lid 0r)))
                                       (λ x y i → isSetPoly (x i0) (x i1) x y i))
               (λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- Distribution of a constant ring element over added polynomials p, q: a (p + q) = ap + aq
  PolyConst*LDistrPoly+ : ∀ a p q → a PolyConst* (p Poly+ q) ≡
                                    (a PolyConst* p) Poly+ (a PolyConst* q)
  PolyConst*LDistrPoly+ =
    λ a → ElimProp.f (λ p → ∀ q → a PolyConst* (p Poly+ q) ≡
                                  (a PolyConst* p) Poly+ (a PolyConst* q))
                     (λ q → cong (a PolyConst*_) (Poly+Lid q) ∙
                            (sym (Poly+Lid (a PolyConst* q))))
                     (λ b p prf → ElimProp.f (λ q → (a PolyConst* ((b ∷ p) Poly+ q)) ≡
                                                    (a PolyConst* (b ∷ p)) Poly+ (a PolyConst* q))
                                             refl
                                             (λ c q prf2  → cong (_∷ (a PolyConst* (p Poly+ q)))
                                                                 (·Rdist+ a b c) ∙
                                                            cong (a · b + a · c ∷_) (prf q))
                                             (isSetPoly _ _))
                     (λ x y i q  → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  --Poly* left distributes over Poly+
  Poly*LDistrPoly+ : ∀ p q r → p Poly* (q Poly+ r) ≡ (p Poly* q) Poly+ (p Poly* r)
  Poly*LDistrPoly+ =
    ElimProp.f
      (λ p → ∀ q r → p Poly* (q Poly+ r) ≡ (p Poly* q) Poly+ (p Poly* r))
      (λ _ _ → refl)
      (λ a p prf q r → ((a PolyConst* (q Poly+ r)) Poly+
                        (0r ∷(p Poly*(q Poly+ r)))) ≡⟨
                                                      cong (_Poly+ (0r ∷ (p Poly* (q Poly+ r))))
                                                           (PolyConst*LDistrPoly+ a q r)
                                                     ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ (p Poly* (q Poly+ r)))) ≡⟨
                                        cong (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+_)
                                             (cong (0r ∷_) (prf q r))
                                       ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ ((p Poly* q) Poly+ (p Poly* r)))) ≡⟨
                                                  cong (((a PolyConst* q) Poly+
                                                         (a PolyConst* r)) Poly+_)
                                                  (XLDistrPoly+ (p Poly* q) (p Poly* r))
                                                 ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        ((0r ∷ (p Poly* q)) Poly+ (0r ∷ (p Poly* r)))) ≡⟨
                                                         Poly+Assoc ((a PolyConst* q) Poly+
                                                                      (a PolyConst* r))
                                                                    (0r ∷ (p Poly* q))
                                                                    (0r ∷ (p Poly* r))
                                                        ⟩
      (((a PolyConst* q) Poly+ (a PolyConst* r)) Poly+
        (0r ∷ (p Poly* q))) Poly+ (0r ∷ (p Poly* r)) ≡⟨ cong (_Poly+ (0r ∷ (p Poly* r)))
                                                             (sym (Poly+Assoc (a PolyConst* q)
                                                                              (a PolyConst* r)
                                                                              (0r ∷ (p Poly* q))))
                                                    ⟩
      (((a PolyConst* q) Poly+ ((a PolyConst* r) Poly+
        (0r ∷ (p Poly* q)))) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                         cong (_Poly+ (0r ∷ (p Poly* r)))
                                                              (cong ((a PolyConst* q) Poly+_)
                                                                    (Poly+Comm (a PolyConst* r)
                                                                               (0r ∷ (p Poly* q))))
                                                         ⟩
      (((a PolyConst* q) Poly+ ((0r ∷ (p Poly* q)) Poly+
        (a PolyConst* r))) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                       cong (_Poly+ (0r ∷ (p Poly* r)))
                                                            (Poly+Assoc (a PolyConst* q)
                                                                        (0r ∷ (p Poly* q))
                                                                        (a PolyConst* r))
                                                            ⟩
      ((((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) Poly+
        (a PolyConst* r)) Poly+ (0r ∷ (p Poly* r))) ≡⟨
                                                      sym (Poly+Assoc ((a PolyConst* q) Poly+
                                                                         (0r ∷ (p Poly* q)))
                                                                      ((a PolyConst* r))
                                                                      ((0r ∷ (p Poly* r))))
                                                     ⟩
      ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) Poly+
        ((a PolyConst* r) Poly+ (0r ∷ (p Poly* r))) ∎)
      (λ x y i q r → isSetPoly _ _ (x q r) (y q r) i)

  -- The constant multiplication of a ring element, a, with a polynomial, p, can be
  -- expressed by polynomial multiplication with the singleton polynomial [ a ]
  PolyConst*r=Poly*[r] : ∀ a p → a PolyConst* p ≡ p Poly* [ a ]
  PolyConst*r=Poly*[r] =
    λ a → ElimProp.f (λ p → a PolyConst* p ≡ p Poly* [ a ])
                     refl
                     ( λ r p prf →  a · r ∷ (a PolyConst* p) ≡⟨
                                                              cong (a · r ∷_) prf
                                                             ⟩
                       a · r ∷ (p Poly* [ a ]) ≡⟨
                                                 cong (a · r ∷_)
                                                      (sym (Poly+Lid (p Poly* [ a ])))
                                                ⟩
                       a · r ∷ ([] Poly+ (p Poly* [ a ])) ≡⟨
                                                            cong (_∷ ([] Poly+ (p Poly* [ a ])))
                                                                 (·Comm a r )
                                                           ⟩
                       r · a ∷ ([] Poly+ (p Poly* [ a ])) ≡⟨
                                                            cong (_∷ ([] Poly+ (p Poly* [ a ])))
                                                                 (sym (+Rid (r · a)))
                                                           ⟩
                       r · a + 0r ∷ ([] Poly+ (p Poly* [ a ])) ∎)
                     ( λ x y i → isSetPoly (x i0) (x i1) x y i)

  -- Connection between the constant multiplication and the multiplication in the ring
  PolyConst*Nested· : ∀ a b p → a PolyConst* (b PolyConst* p) ≡ (a · b) PolyConst* p
  PolyConst*Nested· =
    λ a b → ElimProp.f (λ p → a PolyConst* (b PolyConst* p) ≡ (a · b) PolyConst* p)
                       refl
                       (λ c p prf → cong ((a · (b · c)) ∷_) prf ∙
                                    cong (_∷ ((a · b) PolyConst* p)) (·Assoc a b c))
                       (isSetPoly _ _)

  -- We can move the indeterminate from left to outside: px * q = (p * q)x
  0r∷LeftAssoc : ∀ p q → (0r ∷ p) Poly* q ≡ 0r ∷ (p Poly* q)
  0r∷LeftAssoc =
    ElimProp.f (λ p → ∀ q → (0r ∷ p) Poly* q ≡ 0r ∷ (p Poly* q))
               (λ q → cong (_Poly+ [ 0r ])((cong (_Poly+ []) (0rLeftAnnihilatesPoly q))) ∙
                      cong (_∷ []) (+Lid 0r))
               (λ r p b q → cong (_Poly+ (0r ∷ ((r PolyConst* q) Poly+ (0r ∷ (p Poly* q)))))
                                 ((0rLeftAnnihilatesPoly q) ∙ drop0))
               (λ x y i q → isSetPoly _ _ (x q) (y q) i)

  --Associativity of constant multiplication in relation to polynomial multiplication
  PolyConst*AssocPoly* : ∀ a p q → a PolyConst* (p Poly* q) ≡ (a PolyConst* p) Poly* q
  PolyConst*AssocPoly* =
    λ a → ElimProp.f (λ p → ∀ q → a PolyConst* (p Poly* q) ≡ (a PolyConst* p) Poly* q)
                     (λ q → refl)
                     (λ b p prf q → a PolyConst* ((b PolyConst* q) Poly+
                                    (0r ∷ (p Poly* q))) ≡⟨
                                                          PolyConst*LDistrPoly+ a
                                                                                (b PolyConst* q)
                                                                                (0r ∷ (p Poly* q))
                                                         ⟩
                     (a PolyConst* (b PolyConst* q)) Poly+
                      (a PolyConst* (0r ∷ (p Poly* q))) ≡⟨
                                             cong (_Poly+ (a · 0r ∷ (a PolyConst* (p Poly* q))))
                                                  (PolyConst*Nested· a b q)
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (a PolyConst* (0r ∷ (p Poly* q))) ≡⟨
                                                    cong (((a · b) PolyConst* q) Poly+_)
                                                         (cong (a · 0r  ∷_)
                                                               (PolyConst*r=Poly*[r] a
                                                                                (p Poly* q)))
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (a · 0r ∷ ((p Poly* q) Poly* [ a ])) ≡⟨
                                                         cong (((a · b) PolyConst* q) Poly+_)
                                                              (cong (_∷ ((p Poly* q) Poly* [ a ]))
                                                                    (0RightAnnihilates a))  ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ ((p Poly* q) Poly* [ a ])) ≡⟨
                                            cong (((a · b) PolyConst* q) Poly+_)
                                                 (cong (0r ∷_)
                                                       (sym (PolyConst*r=Poly*[r] a (p Poly* q))))
                                                        ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ (a PolyConst* (p Poly* q))) ≡⟨
                                                         cong (((a · b) PolyConst* q) Poly+_)
                                                              (cong (0r ∷_) (prf q))
                                                         ⟩
                     ((a · b) PolyConst* q) Poly+
                      (0r ∷ ((a PolyConst* p) Poly* q)) ∎)
                     (λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- We can move the indeterminate from left to outside: p * qx = (p * q)x
  0r∷RightAssoc : ∀ p q → p Poly* (0r ∷  q) ≡ 0r ∷ (p Poly* q)
  0r∷RightAssoc =
    ElimProp.f (λ p → ∀ q → p Poly* (0r ∷  q) ≡ 0r ∷ (p Poly* q))
               (λ q → sym drop0)
               (λ a p prf q → ((a ∷ p) Poly* (0r ∷ q)) ≡⟨
                                                        cong ( a · 0r + 0r ∷_)
                                                             (cong ((a PolyConst* q) Poly+_ )
                                                                   (prf q))
                                                        ⟩
               a · 0r + 0r ∷ ((a PolyConst* q) Poly+
                 (0r ∷ (p Poly* q))) ≡⟨
                                       cong (_∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))))
                                            ((+Rid (a · 0r)))
                                      ⟩
               a · 0r ∷ ((a PolyConst* q) Poly+
                 (0r ∷ (p Poly* q))) ≡⟨
                                      cong (_∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))))
                                           (0RightAnnihilates a) ⟩
               0r ∷ ((a PolyConst* q) Poly+ (0r ∷ (p Poly* q))) ∎)
               (λ x y i q  → isSetPoly (x q i0) (x q i1) (x q) (y q) i)

  -- We can move the indeterminate around: px * q = p * qx
  0r∷Comm : ∀ p q → (0r ∷ p) Poly* q ≡ p Poly* (0r ∷ q)
  0r∷Comm = ElimProp.f (λ p → ∀ q → (0r ∷ p) Poly* q ≡ p Poly* (0r ∷ q))
                         (λ q → (cong ((0r PolyConst* q) Poly+_) drop0) ∙
                                                0rLeftAnnihilatesPoly q ∙
                                                                 drop0  )
                         (λ a p prf q → ((0r ∷ a ∷ p) Poly* q) ≡⟨ 0r∷LeftAssoc (a ∷ p) q ⟩
                                        0r ∷ ((a ∷ p) Poly* q) ≡⟨ sym (0r∷RightAssoc (a ∷ p) q) ⟩
                                      ((a ∷ p) Poly* (0r ∷ q)) ∎
                       )
                       λ x y i q → isSetPoly (x q i0) (x q i1) (x q) (y q) i

  --Poly* is commutative
  Poly*Commutative : ∀ p q → p Poly* q ≡ q Poly* p
  Poly*Commutative =
    ElimProp.f (λ p → ∀ q → p Poly* q ≡ q Poly* p)
               (λ q → sym (0PLeftAnnihilates q))
               (λ a p prf q → (a PolyConst* q) Poly+ (0r ∷ (p Poly* q)) ≡⟨
                                       cong ((a PolyConst* q) Poly+_)
                                            (cong (0r ∷_) (prf q)) ⟩
               ((a PolyConst* q) Poly+ (0r ∷ (q Poly* p))) ≡⟨
                                                            cong ((a PolyConst* q) Poly+_)
                                                            (sym (0r∷LeftAssoc q p))
                                                            ⟩
               ((a PolyConst* q) Poly+ ((0r ∷ q) Poly* p)) ≡⟨
                                      cong (_Poly+ ((0r PolyConst* p) Poly+ (0r ∷ (q Poly* p))))
                                           (PolyConst*r=Poly*[r] a q) ⟩
               ((q Poly* [ a ]) Poly+ ((0r ∷ q) Poly* p)) ≡⟨
                                                           cong ((q Poly* [ a ]) Poly+_)
                                                                (0r∷Comm q p)
                                                           ⟩
               ((q Poly* [ a ]) Poly+ (q Poly* (0r ∷ p))) ≡⟨
                                                           sym (Poly*LDistrPoly+ q [ a ] (0r ∷ p))
                                                           ⟩
               (((q Poly* ([ a ] Poly+ (0r ∷ p))))) ≡⟨
                                                     cong (q Poly*_)
                                                          (Poly+Comm [ a ] (0r ∷ p))
                                                     ⟩
               ((q Poly* ((0r ∷ p) Poly+ [ a ]))) ≡⟨
                                                   refl
                                                   ⟩
               (q Poly* ((0r + a) ∷ p)) ≡⟨ cong (q Poly*_)
                                                (cong (_∷ p) (+Lid a))
                                         ⟩
               (q Poly* (a ∷ p)) ∎)
               (λ x y i q → isSetPoly _ _ (x q ) (y q) i)

  --1P is the right identity of Poly*.
  Poly*Rid : ∀ p → p Poly* 1P ≡ p
  Poly*Rid = λ p → (Poly*Commutative p 1P ∙ Poly*Lid p)

  --Polynomial multiplication right distributes over polynomial addition.
  Poly*RDistrPoly+ : ∀ p q r → (p Poly+ q) Poly* r ≡ (p Poly* r) Poly+ (q Poly* r)
  Poly*RDistrPoly+ = λ p q r → sym (Poly*Commutative r (p Poly+ q)) ∙
                                       Poly*LDistrPoly+ r p q ∙
                                       cong (_Poly+ (r Poly* q)) (Poly*Commutative r p) ∙
                                       cong ((p Poly* r) Poly+_) (Poly*Commutative r q)

  --Polynomial multiplication is associative
  Poly*Associative : ∀ p q r → p Poly* (q Poly* r) ≡  (p Poly* q) Poly* r
  Poly*Associative =
    ElimProp.f (λ p → ∀ q r → p Poly* (q Poly* r) ≡  (p Poly* q) Poly* r )
               (λ _ _ → refl)
               (λ a p prf q r  →
                 ((a ∷ p) Poly* (q Poly* r)) ≡⟨
                                               cong (_Poly+ (0r ∷ (p Poly* (q Poly* r))))
                                                    (PolyConst*AssocPoly* a q r)
                                              ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r ∷ (p Poly* (q Poly* r)))) ≡⟨
                                                 sym (cong (((a PolyConst* q) Poly* r) Poly+_)
                                                           (cong (_∷ (p Poly* (q Poly* r)))
                                                                 (+Lid 0r)))
                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ (p Poly* (q Poly* r)))) ≡⟨
                                                 cong (((a PolyConst* q) Poly* r) Poly+_)
                                                      (cong (0r + 0r ∷_)
                                                            (sym (Poly+Lid (p Poly* (q Poly* r)))))
                                                      ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ ([] Poly+ (p Poly* (q Poly* r))))) ≡⟨
                                                         cong (((a PolyConst* q) Poly* r) Poly+_)
                                                              (cong (0r + 0r ∷_)
                                                                    (cong ([] Poly+_)
                                                                          (prf q r)))
                                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  (0r + 0r ∷ ([] Poly+ ((p Poly* q) Poly* r)))) ≡⟨
                                                  cong (((a PolyConst* q) Poly* r) Poly+_)
                                                       (cong (_Poly+ (0r ∷ ((p Poly* q) Poly* r)))
                                                             (sym (0rLeftAnnihilatesPoly r)))
                                                                 ⟩
                 (((a PolyConst* q) Poly* r) Poly+
                  ((0r PolyConst* r) Poly+ (0r ∷ ((p Poly* q) Poly* r)))) ≡⟨
                                                     sym (Poly*RDistrPoly+ (a PolyConst* q)
                                                                           (0r ∷ (p Poly* q)) r)
                                                                           ⟩
                 ((((a ∷ p) Poly* q) Poly* r)) ∎)
               (λ x y i q r  → isSetPoly _ _ (x q r) (y q r) i)

-----------------------------------------------------------------------------
-- Product by Xn and operationsproperties on it

  prod-Xn : (n : ℕ) → Poly → Poly
  prod-Xn zero x = x
  prod-Xn (suc n) x = 0r ∷ (prod-Xn n x)

  prod-Xn-0P : (n : ℕ) → prod-Xn n 0P ≡ 0P
  prod-Xn-0P zero = refl
  prod-Xn-0P (suc n) = cong (λ X → 0r ∷ X) (prod-Xn-0P n) ∙ drop0

  prod-Xn-sum : (n : ℕ) → (x y : Poly) → (prod-Xn n x) Poly+ (prod-Xn n y) ≡ prod-Xn n (x Poly+ y)
  prod-Xn-sum zero x y = refl
  prod-Xn-sum (suc n) x y = cong₂ _∷_ (+Rid 0r) (prod-Xn-sum n x y)

  prod-Xn-comp : (n m : ℕ) → (x : Poly) → prod-Xn n (prod-Xn m x) ≡ prod-Xn (n +n m) x
  prod-Xn-comp zero m x = refl
  prod-Xn-comp (suc n) m x = cong (λ X → 0r ∷ X) (prod-Xn-comp n m x)

  prod-Xn-∷ : (n : ℕ) → (r : R) → (x : Poly) → (prod-Xn n (r ∷ [])) Poly+ (0r ∷ prod-Xn n x) ≡ prod-Xn n (r ∷ x)
  prod-Xn-∷ zero r x = cong₂ _∷_ (+Rid r) (Poly+Lid x)
  prod-Xn-∷ (suc n) r x = cong₂ _∷_ (+Lid 0r) (prod-Xn-∷ n r x)

  prod-Xn-prod-0 : (m : ℕ) → (x y : Poly) → x Poly* (prod-Xn m y) ≡ prod-Xn m (x Poly* y)
  prod-Xn-prod-0 zero x y = refl
  prod-Xn-prod-0 (suc m) x y = ((x Poly* (0r ∷ prod-Xn m y)))
                                   ≡⟨ Poly*Commutative x (prod-Xn (suc m) y) ⟩
                               ((0r PolyConst* x) Poly+ (0r ∷ (prod-Xn m y Poly* x)))
                                  ≡⟨ cong (λ X → X Poly+ (0r ∷ ((prod-Xn m y) Poly* x))) ((0rLeftAnnihilatesPoly x) ∙ drop0) ⟩
                               ((0r ∷ (prod-Xn m y Poly* x)))
                                  ≡⟨ cong (λ X → 0r ∷ X) (Poly*Commutative (prod-Xn m y) x) ⟩
                               (0r ∷ (x Poly* prod-Xn m y))
                                  ≡⟨ cong (λ X → 0r ∷ X) (prod-Xn-prod-0 m x y) ⟩
                               (0r ∷ prod-Xn m (x Poly* y))  ∎

  prod-Xn-prod : (n m : ℕ) → (x y : Poly) → (prod-Xn n x) Poly* (prod-Xn m y) ≡ prod-Xn (n +n m) (x Poly* y)
  prod-Xn-prod zero m x y = prod-Xn-prod-0 m x y
  prod-Xn-prod (suc n) m x y = cong₂ _Poly+_ ((0rLeftAnnihilatesPoly (prod-Xn m y)) ∙ drop0) (cong (λ X → 0r ∷ X) (prod-Xn-prod n m x y))

----------------------------------------------------------------------------------------------
-- An instantiation of Polynomials as a commutative ring can be found in CommRing/Instances --
----------------------------------------------------------------------------------------------

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------
-- Conversion of ≤ to <, along with a number of properties
------------------------------------------------------------------------

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

open import Relation.Binary

module Relation.Binary.NonStrictToStrict
         {a : Set} (_≈_ _≤_ : Rel a)
         where

open import Relation.Nullary
open import Relation.Binary.Consequences
open import Data.Function
open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- Conversion

-- _≤_ can be turned into _<_ as follows:

_<_ : Rel a
x < y = (x ≤ y) × ¬ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

irrefl : Irreflexive _≈_ _<_
irrefl x≈y x<y = proj₂ x<y x≈y

trans : IsPartialOrder _≈_ _≤_ → Transitive _<_
trans po = λ x<y y<z →
  ( PO.trans (proj₁ x<y) (proj₁ y<z)
  , λ x≈z → proj₂ x<y $ lemma (proj₁ x<y) (proj₁ y<z) x≈z
  )
  where
  module PO = IsPartialOrder po

  lemma : ∀ {x y z} → x ≤ y → y ≤ z → x ≈ z → x ≈ y
  lemma x≤y y≤z x≈z =
    PO.antisym x≤y $ PO.trans y≤z (PO.reflexive $ PO.Eq.sym x≈z)

<-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
<-resp-≈ eq ≤-resp-≈ =
  (λ {x y' y} y'≈y x<y' →
    ( proj₁ ≤-resp-≈ y'≈y (proj₁ x<y')
    , λ x≈y → proj₂ x<y' (Eq.trans x≈y (Eq.sym y'≈y))
    )
  ) ,
  (λ {y x' x} x'≈x x'<y →
    ( proj₂ ≤-resp-≈ x'≈x (proj₁ x'<y)
    , λ x≈y → proj₂ x'<y (Eq.trans x'≈x x≈y)
    ))
  where module Eq = IsEquivalence eq

trichotomous : Symmetric _≈_ → Decidable _≈_ →
               Antisymmetric _≈_ _≤_ → Total _≤_ →
               Trichotomous _≈_ _<_
trichotomous ≈-sym ≈-dec antisym total x y with ≈-dec x y
... | yes x≈y = tri≈ (irrefl x≈y) x≈y (irrefl (≈-sym x≈y))
... | no  x≉y with total x y
...   | inj₁ x≤y = tri< (x≤y , x≉y) x≉y
                        (x≉y ∘ antisym x≤y ∘ proj₁)
...   | inj₂ x≥y = tri> (x≉y ∘ flip antisym x≥y ∘ proj₁) x≉y
                        (x≥y , x≉y ∘ ≈-sym)

decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_
decidable ≈-dec ≤-dec x y with ≈-dec x y | ≤-dec x y
... | yes x≈y | _       = no (flip proj₂ x≈y)
... | no  x≉y | yes x≤y = yes (x≤y , x≉y)
... | no  x≉y | no  x≰y = no (x≰y ∘ proj₁)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.List.Relation.Unary.All
-- directly.
------------------------------------------------------------------------

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

module Data.List.All where

open import Data.List.Relation.Unary.All public

{-# WARNING_ON_IMPORT
"Data.List.All was deprecated in v1.0.
Use Data.List.Relation.Unary.All instead."
#-}


text:
{-# OPTIONS -v impossible:100 #-}
module Issue882a where

open import Common.Level
open import Common.Equality

private
 primitive
   primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

-- trustMe {x = x} {y = y} evaluates to refl if x and y are
-- definitionally equal.
--
-- For an example of the use of trustMe, see Data.String._≟_.

trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
trustMe = primTrustMe

postulate
  S : Set
  B : Set
  b : B

M : Set
M = B -> S

out : M -> M
out m = o
  where

   s : S
   s = m b

   postulate
     mko : (mm : S) -> s ≡ mm -> M

   o : M
   o n = mko (m b) trustMe n

postulate
  unfold : (M -> M) -> M

inn : M
inn = unfold out

postulate
  n : B

iso1 : inn ≡ inn
iso1 rewrite refl {x = n} = {!!}
-- iso1 rewrite (refl {a = lzero}{A = B}{x = n}) = {!!}

{- Error

OLD:
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Conversion.hs:636

NEW:
Some vomit about Setω not equal to Level when checking well-formedness
of with type.

NEWER (2013-11-30):
Cannot instantiate the metavariable _48 to solution m b since it
contains the variable m which is not in scope of the metavariable
or irrelevant in the metavariable but relevant in the solution
when checking that the type
B →
(w : _x_48 ≡ _x_48) →
unfold (λ m → _.mko m (m b) w) ≡ unfold (λ m → _.mko m (m b) w)
of the generated with function is well-formed

NOW (2014-05-17):
Rewriting with refl is a no-op, so no error is triggered any more.
Just an unresolved meta now.
-}

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --cubical --guardedness --postfix-projections #-}

module Data.Graph where

open import Prelude
open import Data.List
open import Data.Nat

-- record Thunk (A : Type a) : Type a where
--   coinductive
--   constructor ⟪_⟫
--   field force : A
-- open Thunk

-- infixr 5 _◃_
-- record Stream (A : Type a) : Type a where
--   constructor _◃_
--   coinductive
--   field
--     head : A
--     tail : (Stream A)

-- open Stream

Graph : Type a → Type a
Graph A = A → List A

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

pure : A → Stream A
pure x _ = x

smap : (A → B) → Stream A → Stream B
smap f xs n = f (xs n)

bfs : Graph A → A → Stream (List A)
bfs g r zero    = r ∷ []
bfs g r (suc n) = concatMap g (bfs g r n)

-- module _ {A : Type a} (g : Graph A) where
--   mutual
--     bfs-foldr : List A → Stream (List A) → Stream (List A)
--     bfs-foldr []       qs = qs
--     bfs-foldr (x ∷ xs) qs .head = x ∷ bfs-foldr xs qs .head
--     bfs-foldr (x ∷ xs) qs .tail .force = bfs-foldr (g x) (bfs-foldr xs qs .tail .force)

--     -- bfs-cons : A → Stream (List A) → Stream (List A)
--     -- bfs-cons x (q ◃ qs) = (x ∷ q) ◃ bfs-foldr (g x) qs

--   -- bfs : A → Stream (List A)
--   -- bfs r = bfs-cons r (pure [])

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

record D (A : Set) : Set where
  constructor mkD
  field d : A
open D {{...}}

module test where

  instance

    _ : D Bool
    _ = mkD true

    a : D Nat
    a = mkD 0

  _ : d ≡ true
  _ = refl

  _ : d ≡ zero
  _ = refl

-- no instance in scope
-- _ : d ≡ true
-- _ = ?

_ : d ≡ zero
_ = refl


text:
open import Agda.Builtin.List
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.String
  renaming (primShowNat to show)
open import Agda.Builtin.Reflection
  renaming (bindTC to _>>=_; returnTC to return)

pattern vArg t = arg (arg-info visible relevant) t
pattern var₀ x = var x []

infixr 10 _++_
_++_ = primStringAppend

postulate
  whatever : ∀ {a} {A : Set a} → A

macro
  test1 : Nat → Term → TC _
  test1 n _ =
    extendContext (vArg (quoteTerm Nat)) do
      var₀ i ← quoteTC n where _ → whatever
      m ← unquoteTC {A = Nat} (var₀ 0)
      var₀ j ← quoteTC m where _ → whatever
      extendContext (vArg (quoteTerm Nat)) do
        var₀ k ← quoteTC n where _ → whatever
        var₀ l ← quoteTC m where _ → whatever
        typeError (strErr (show i ++ show k ++ show j ++ show l) ∷ [])

  test2 : Term → TC _
  test2 hole = do
    st ← quoteTC Set
    t ← extendContext (vArg st) do
      v ← unquoteTC {A = Set} (var₀ zero)
      extendContext (vArg (var₀ zero)) do
        _ ← unquoteTC {A = v} (var₀ zero)
        return tt
    u ← quoteTC t
    unify hole u

  test3 : Nat → Term → TC _
  test3 n _ = do
    m      ← extendContext (vArg (quoteTerm Nat)) (return n)
    var₀ i ← quoteTC m where _ → whatever
    typeError (strErr (show i) ∷ [])

  localvar : Term → TC _
  localvar _ = do
    m ← extendContext (vArg (quoteTerm Nat)) (unquoteTC {A = Nat} (var₀ 0))
    typeError (strErr (show m) ∷ [])


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

open import HoTT

module homotopy.HSpace where

record HSpaceStructure {i} (A : Type i) : Type i where
  constructor hSpaceStructure
  field
    e : A
    μ : A → A → A
    μe- : (a : A) → μ e a == a
    μ-e : (a : A) → μ a e == a

module ConnectedHSpace {i} (A : Type i) (c : is-connected ⟨0⟩ A)
  (hA : HSpaceStructure A) where

  open HSpaceStructure hA

  {-
  Given that [A] is 0-connected, to prove that each [μ a] is an equivalence we
  only need to prove that one of them is. But for [a] = [e], [μ a] is the
  identity so we’re done.
  -}

  μ-is-equiv : (a : A) → is-equiv (μ a)
  μ-is-equiv = prop-over-connected {a = e} c
    (λ a → (is-equiv (μ a) , is-equiv-is-prop (μ a)))
    (transport! is-equiv (λ= μe-) (idf-is-equiv A))

  μ'-is-equiv : (a : A) → is-equiv (λ a' → μ a' a)
  μ'-is-equiv = prop-over-connected {a = e} c
    (λ a → (is-equiv (λ a' → μ a' a) , is-equiv-is-prop (λ a' → μ a' a)))
    (transport! is-equiv (λ= μ-e) (idf-is-equiv A))

  μ-equiv : A → A ≃ A
  μ-equiv a = (μ a , μ-is-equiv a)

  μ'-equiv : A → A ≃ A
  μ'-equiv a = ((λ a' → μ a' a) , μ'-is-equiv a)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.Bool as 𝔹 using (Bool; true; false; if_then_else_)
open import Data.Fin as Fin using (Fin; #_)
open import Data.List
open import Relation.Nullary
open import Relation.Nullary.Decidable

module simple-if-temp-output where

postulate f : Tensor ℚ (1 ∷ []) → Tensor ℚ (1 ∷ [])

abstract
  prop1 : ∀ (x : ℚ) → if ⌊ x ℚ.>? ℤ.+ 0 ℚ./ 1 ⌋ then f (x ∷ []) (# 0) ℚ.> ℤ.+ 0 ℚ./ 1 else f (x ∷ []) (# 0) ℚ.≤ ℤ.+ 0 ℚ./ 1
  prop1 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

abstract
  prop3 : ∃ λ (x : ℚ) → if ⌊ f (x ∷ []) (# 0) ℚ.>? ℤ.+ 0 ℚ./ 1 ⌋ then x ℚ.≥ ℤ.+ 0 ℚ./ 1 else x ℚ.< ℤ.+ 0 ℚ./ 1
  prop3 = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
module Imports.ATP-A where

postulate
  D    : Set
  _≡_  : D → D → Set
  a b  : D

postulate p : a ≡ b

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


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

-- {-# OPTIONS -v tc.lhs.unify:15 #-}

open import Common.Equality
open import Common.Prelude

data Fin : (n : Nat) → Set where
  zero : {n : Nat} → Fin (suc n)
  suc  : {n : Nat} (i : Fin n) → Fin (suc n)

data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set1 where
  refl : a ≅ a

OffDiag : ∀ {n m} → Fin n → Fin m → Set
OffDiag zero    zero    = ⊥
OffDiag (suc _) (suc _) = ⊥
OffDiag _       _       = ⊤

inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → OffDiag i j → ⊥
inj-Fin-≅ {i = zero}  {zero} eq ()
inj-Fin-≅ {i = zero}  {suc j} ()
inj-Fin-≅ {i = suc i} {zero} ()
inj-Fin-≅ {i = suc i} {suc j} p ()


text:
module Cxt (K : Set) where

open import Basics
open import Pr
open import Nom

mutual
  data Cxt : Set where
    EC : Cxt
    _[_-_] : (G : Cxt)(x : Nom) -> K -> {p : [| G Hasn't x |]} -> Cxt

  HAS : Cxt -> Nom -> Bool
  HAS EC x = false
  HAS (G [ y - S ]) x with nomEq y x
  HAS (G [ y - S ]) .y   | yes refl = true
  ...                    | no n = HAS G x

  _Has_ : Cxt -> Nom -> Pr
  G Has x = So (HAS G x)

  _Hasn't_ : Cxt -> Nom -> Pr
  G Hasn't x = So (not (HAS G x))

GooN : (G : Cxt)(T : K) -> Nom -> Pr
GooN EC T y = ff
GooN (G [ x - S ]) T y with nomEq x y
GooN (G [ x - S ]) T .x   | yes refl   = S eq T
GooN (G [ x - S ]) T y    | no n       = GooN G T y

_?-_ : (G : Cxt)(x : Nom){p : [| G Has x |]} -> K :- \ T -> GooN G T x
(EC ?- y) {}
((G [ x - S ]) ?- y) {_} with nomEq x y
((G [ x - S ]) ?- .x) {_}   | yes refl  = [ S / refl ]
((G [ x - S ]) ?- y) {p}    | no n      = (G ?- y) {p}

topGooN : (G : Cxt)(x : Nom){p : [| G Hasn't x |]}(S : K) ->
          [| GooN ((G [ x - S ]) {p}) S x |]
topGooN G x S with nomEq x x
topGooN G x S | yes refl  = refl
topGooN G x S | no n      = magic (n refl)

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --sized-types #-}
module SOList.Lower.Properties {A : Set}(_≤_ : A → A → Set)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Size
open import List.Sorted _≤_
open import SOList.Lower _≤_

lemma-solist-sorted : {ι : Size}{b : Bound} → (xs : SOList {ι} b) →  Sorted (forget xs)
lemma-solist-sorted onil = nils
lemma-solist-sorted (:< {x = x} _ onil) = singls x
lemma-solist-sorted (:< b≤x (:< (lexy x≤y) ys)) = conss x≤y  (lemma-solist-sorted (:< (lexy x≤y) ys))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Float where

import      Lvl
open import Type

postulate Float : Type{Lvl.𝟎}
{-# BUILTIN FLOAT Float #-}


text:
{-# OPTIONS --copatterns #-}

open import Common.Equality
open import Common.Product

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

record Functor (F : Set → Set) : Set₁ where
  field
    map : ∀ {A B} → (A → B) → F A → F B
    map-id : ∀ {A}{x : F A} → map id x ≡ x
open Functor

test : {C : Set} → Functor (_×_ C)
map    test f (c , a) = c , f a
map-id test           = refl -- : map test id x ≡ x
  -- needs to match against record constructor
  -- x/(c,a) = proj₁ x / c, proj₂ x / a


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

module 02-pi where

import 00-preamble
open 00-preamble public

-- Section 2.3 The identity function, composition, and their laws

-- Definition 2.3.1
id : {i : Level} {A : UU i} → A → A
id a = a

-- Definition 2.3.2
_∘_ :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} →
  (B → C) → ((A → B) → (A → C))
(g ∘ f) a = g (f a)

-- Exercises

-- Exercise 2.3
const : {i j : Level} (A : UU i) (B : UU j) (b : B) → A → B
const A B b x = b

-- Exercise 2.4
_∘'_ :
  {i j k : Level} {A : UU i} {B : A → UU j} {C : (x : A) → B x → UU k} →
  (g : (x : A) → (y : B x) → C x y) (f : (x : A) → B x) → (x : A) → C x (f x)
(g ∘' f) x = g x (f x)

-- Exercise 2.5
Π-swap : {i j k : Level} {A : UU i} {B : UU j} {C : A → (B → UU k)} →
  ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
Π-swap f y x = f x y

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
------------------------------------------------------------------------
-- Some parsers which require a decidable token equality
------------------------------------------------------------------------

open import Relation.Binary

module RecursiveDescent.Inductive.Token (D : DecSetoid) where

open DecSetoid D using (_≟_) renaming (carrier to tok)

open import RecursiveDescent.Inductive
open import RecursiveDescent.Inductive.SimpleLib

open import Data.Maybe
open import Relation.Nullary
open import Data.Vec
open import Data.Vec1

-- Parsing a given token (or, really, a given equivalence class of
-- tokens).

sym : forall {nt} -> tok -> Parser tok nt _ tok
sym c = sat p
  where
  p : tok -> Maybe tok
  p x with c ≟ x
  ... | yes _ = just x
  ... | no  _ = nothing

-- Parsing a sequence of tokens.

string : forall {nt n} -> Vec tok n -> Parser tok nt _ (Vec tok n)
string cs = sequence (map₀₁ sym cs)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Propositional (intensional) equality
------------------------------------------------------------------------

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

module Relation.Binary.PropositionalEquality where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
import Axiom.Extensionality.Propositional as Ext
open import Axiom.UniquenessOfIdentityProofs
open import Function.Base
open import Function.Equality using (Π; _⟶_; ≡-setoid)
open import Level using (Level; _⊔_)
open import Data.Product using (∃)

open import Relation.Nullary using (yes ; no)
open import Relation.Nullary.Decidable.Core
open import Relation.Unary using (Pred)
open import Relation.Binary
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid)
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  as Trivial

private
  variable
    a b c ℓ p : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Re-export contents of core module

open import Relation.Binary.PropositionalEquality.Core public

------------------------------------------------------------------------
-- Some properties

subst₂ : ∀ (_∼_ : REL A B ℓ) {x y u v} → x ≡ y → u ≡ v → x ∼ u → y ∼ v
subst₂ _ refl refl p = p

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

cong₂ : ∀ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl

------------------------------------------------------------------------
-- Structure of equality as a binary relation

isEquivalence : IsEquivalence {A = A} _≡_
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

isDecEquivalence : Decidable _≡_ → IsDecEquivalence {A = A} _≡_
isDecEquivalence _≟_ = record
  { isEquivalence = isEquivalence
  ; _≟_           = _≟_
  }

isPreorder : IsPreorder {A = A} _≡_ _≡_
isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = id
  ; trans         = trans
  }

------------------------------------------------------------------------
-- Bundles for equality as a binary relation

setoid : Set a → Setoid _ _
setoid A = record
  { Carrier       = A
  ; _≈_           = _≡_
  ; isEquivalence = isEquivalence
  }

decSetoid : Decidable {A = A} _≡_ → DecSetoid _ _
decSetoid _≟_ = record
  { _≈_              = _≡_
  ; isDecEquivalence = isDecEquivalence _≟_
  }

preorder : Set a → Preorder _ _ _
preorder A = record
  { Carrier    = A
  ; _≈_        = _≡_
  ; _∼_        = _≡_
  ; isPreorder = isPreorder
  }

------------------------------------------------------------------------
-- Pointwise equality

infix 4 _≗_

_→-setoid_ : ∀ (A : Set a) (B : Set b) → Setoid _ _
A →-setoid B = ≡-setoid A (Trivial.indexedSetoid (setoid B))

_≗_ : (f g : A → B) → Set _
_≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B)

:→-to-Π : ∀ {A : Set a} {B : IndexedSetoid A b ℓ} →
          ((x : A) → IndexedSetoid.Carrier B x) → Π (setoid A) B
:→-to-Π {B = B} f = record
  { _⟨$⟩_ = f
  ; cong  = λ { refl → IndexedSetoid.refl B }
  }
  where open IndexedSetoid B using (_≈_)

→-to-⟶ : ∀ {A : Set a} {B : Setoid b ℓ} →
         (A → Setoid.Carrier B) → setoid A ⟶ B
→-to-⟶ = :→-to-Π

------------------------------------------------------------------------
-- Inspect

-- Inspect can be used when you want to pattern match on the result r
-- of some expression e, and you also need to "remember" that r ≡ e.

-- See README.Inspect for an explanation of how/why to use this.

record Reveal_·_is_ {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (a ⊔ b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

------------------------------------------------------------------------
-- Propositionality

isPropositional : Set a → Set a
isPropositional A = (a b : A) → a ≡ b

------------------------------------------------------------------------
-- Various equality rearrangement lemmas

trans-injectiveˡ : ∀ {x y z : A} {p₁ p₂ : x ≡ y} (q : y ≡ z) →
                   trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
trans-injectiveˡ refl = subst₂ _≡_ (trans-reflʳ _) (trans-reflʳ _)

trans-injectiveʳ : ∀ {x y z : A} (p : x ≡ y) {q₁ q₂ : y ≡ z} →
                   trans p q₁ ≡ trans p q₂ → q₁ ≡ q₂
trans-injectiveʳ refl eq = eq

cong-id : ∀ {x y : A} (p : x ≡ y) → cong id p ≡ p
cong-id refl = refl

cong-∘ : ∀ {x y : A} {f : B → C} {g : A → B} (p : x ≡ y) →
         cong (f ∘ g) p ≡ cong f (cong g p)
cong-∘ refl = refl

module _ {P : Pred A p} {x y : A} where

  subst-injective : ∀ (x≡y : x ≡ y) {p q : P x} →
                    subst P x≡y p ≡ subst P x≡y q → p ≡ q
  subst-injective refl p≡q = p≡q

  subst-subst : ∀ {z} (x≡y : x ≡ y) {y≡z : y ≡ z} {p : P x} →
                subst P y≡z (subst P x≡y p) ≡ subst P (trans x≡y y≡z) p
  subst-subst refl = refl

  subst-subst-sym : (x≡y : x ≡ y) {p : P y} →
                    subst P x≡y (subst P (sym x≡y) p) ≡ p
  subst-subst-sym refl = refl

  subst-sym-subst : (x≡y : x ≡ y) {p : P x} →
                    subst P (sym x≡y) (subst P x≡y p) ≡ p
  subst-sym-subst refl = refl

subst-∘ : ∀ {x y : A} {P : Pred B p} {f : A → B}
          (x≡y : x ≡ y) {p : P (f x)} →
          subst (P ∘ f) x≡y p ≡ subst P (cong f x≡y) p
subst-∘ refl = refl

subst-application : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                    (B₁ : A₁ → Set b₁) {B₂ : A₂ → Set b₂}
                    {f : A₂ → A₁} {x₁ x₂ : A₂} {y : B₁ (f x₁)}
                    (g : ∀ x → B₁ (f x) → B₂ x) (eq : x₁ ≡ x₂) →
                    subst B₂ eq (g x₁ y) ≡ g x₂ (subst B₁ (cong f eq) y)
subst-application _ _ refl = refl

-- A lemma that is very similar to Lemma 2.4.3 from the HoTT book.

naturality : ∀ {x y} {x≡y : x ≡ y} {f g : A → B}
             (f≡g : ∀ x → f x ≡ g x) →
             trans (cong f x≡y) (f≡g y) ≡ trans (f≡g x) (cong g x≡y)
naturality {x = x} {x≡y = refl} f≡g =
  f≡g x               ≡⟨ sym (trans-reflʳ _) ⟩
  trans (f≡g x) refl  ∎
  where open ≡-Reasoning

-- A lemma that is very similar to Corollary 2.4.4 from the HoTT book.

cong-≡id : ∀ {f : A → A} {x : A} (f≡id : ∀ x → f x ≡ x) →
           cong f (f≡id x) ≡ f≡id (f x)
cong-≡id {f = f} {x} f≡id =
  cong f fx≡x                                    ≡⟨ sym (trans-reflʳ _) ⟩
  trans (cong f fx≡x) refl                       ≡⟨ cong (trans _) (sym (trans-symʳ fx≡x)) ⟩
  trans (cong f fx≡x) (trans fx≡x (sym fx≡x))    ≡⟨ sym (trans-assoc (cong f fx≡x)) ⟩
  trans (trans (cong f fx≡x) fx≡x) (sym fx≡x)    ≡⟨ cong (λ p → trans p (sym _)) (naturality f≡id) ⟩
  trans (trans f²x≡x (cong id fx≡x)) (sym fx≡x)  ≡⟨ cong (λ p → trans (trans f²x≡x p) (sym fx≡x)) (cong-id _) ⟩
  trans (trans f²x≡x fx≡x) (sym fx≡x)            ≡⟨ trans-assoc f²x≡x ⟩
  trans f²x≡x (trans fx≡x (sym fx≡x))            ≡⟨ cong (trans _) (trans-symʳ fx≡x) ⟩
  trans f²x≡x refl                               ≡⟨ trans-reflʳ _ ⟩
  f≡id (f x)                                     ∎
  where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x)

module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where

  ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq
  ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq

  ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
  ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq

------------------------------------------------------------------------
-- Any operation forms a magma over _≡_

isMagma : (_∙_ : Op₂ A) → IsMagma _≡_ _∙_
isMagma _∙_ = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _∙_
  }

magma : (_∙_ : Op₂ A) → Magma _ _
magma _∙_ = record
  { isMagma = isMagma _∙_
  }

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

Extensionality = Ext.Extensionality
{-# WARNING_ON_USAGE Extensionality
"Warning: Extensionality was deprecated in v1.0.
Please use Extensionality from `Axiom.Extensionality.Propositional` instead."
#-}
extensionality-for-lower-levels = Ext.lower-extensionality
{-# WARNING_ON_USAGE extensionality-for-lower-levels
"Warning: extensionality-for-lower-levels was deprecated in v1.0.
Please use lower-extensionality from `Axiom.Extensionality.Propositional` instead."
#-}
∀-extensionality = Ext.∀-extensionality
{-# WARNING_ON_USAGE ∀-extensionality
"Warning: ∀-extensionality was deprecated in v1.0.
Please use ∀-extensionality from `Axiom.Extensionality.Propositional` instead."
#-}


text:
{-# TERMINATING         #-}
{-# NO_POSITIVITY_CHECK #-}
mutual
  data D₁ : Set where
    lam : (D₁ → D₁) → D₁

  Foo₁ : Set
  Foo₁ = Foo₁

{-# NON_TERMINATING     #-}
{-# NO_POSITIVITY_CHECK #-}
mutual
  data D₂ : Set where
    lam : (D₂ → D₂) → D₂

  Foo₂ : Set
  Foo₂ = Foo₂


text:
record R0 : Set₁ where
  constructor c0
  field f0 : Set

record R1 : Set₁ where
  constructor c1
  field f1 : R0

test : R1 → Set₁
test x@(c1 x) = Set

max_issues_repo_name: cruhland/agda


text:
-- forcePi should be allowed to generate constraints

module Lambda where

data Bool : Set where
  true : Bool
  false : Bool

T : Bool -> Set
T true  = Bool -> Bool
T false = Bool

id : {x : Bool} -> T x -> T x
id y = y

f : Bool -> Bool
f = id (\x -> x)


text:
-- Andreas, 2013-03-20 Problem was that CompiledClause.Match.unfoldCoinduction
-- did not instantiate metas
-- {-# OPTIONS -v tc.meta.assign:10 -v tc.reduce:100 -v tc.with.abstract:50 #-}
{-# OPTIONS --allow-unsolved-metas #-}
module Issue826 where

open import Common.Coinduction

postulate
  A : Set
  x : A
  P : A → Set
  p : P x

data Q : ∞ A → Set where

♯x = ♯ x

Foo : Q ♯x
Foo = goal
  where
  x′ : _
  x′ = _ -- problem went away if we wrote ♯x here

  goal : Q x′ -- ensures that x′ = ♯ x (instantiates meta)
  goal = {!♭ x′!} -- normalization of this expression should be x, but was not

  -- Note that ♭ x′ is definitionally equal to x:

  ok : P (♭ x′)
  ok = p

  good : P x
  good with (♭ x′) | p
  good | y | p′ = p′

{- This still does not work because the underscore is solved too late,
   only after with-abstraction is taking place.

  bad : P (♭ x′)
  bad with x | p
  bad | y | p′ = p′

-}

max_issues_repo_name: shlevy/agda


text:
module SetInf where

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


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

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate
  A : Set
  f g : A → A
  f≡g : ∀ a → f a ≡ g a

{-# REWRITE f≡g  #-}

-- Adding the same rule again would make Agda loop
postulate
  f≡g' : ∀ a → f a ≡ g a
{-# REWRITE f≡g' #-}

goal : ∀ {a} → f a ≡ g a
goal = refl


text:
module Oscar.Class where

open import Oscar.Data.Equality
open import Oscar.Function
open import Oscar.Relation
open import Oscar.Level
open import Oscar.Function
open import Oscar.Relation

-- instance EquivalenceProp : ∀ {a} {A : Set a} → Equivalence (_≡_ {a} {A})
-- EquivalenceProp = {!!}

-- instance EquivalenceProp1 : ∀ {a} {A : Set a} {b} {B : A → Set b} → Equivalence (_≡̇_ {a} {A} {b} {B})
-- Equivalence.reflexivity EquivalenceProp1 x x₁ = refl

-- import Oscar.Data.Term.internal.SubstituteAndSubstitution FunctionName as ⋆

-- instance SemigroupFinTerm : Semigroup _⊸_ _≡̇_
-- Semigroup.equivalence SemigroupFinTerm = it
-- Semigroup._◇_ SemigroupFinTerm = ⋆._◇_ -- (Semifunctor._◃ SemifunctorFinTerm g) ∘ f --
-- Semigroup.◇-associativity SemigroupFinTerm = {!!}

-- instance Semigroup⋆ : ∀ {a} {A : Set a} {x} {X : A → Set x} → Semigroup (_⟨ X ⟩→_) _≡̇_
-- Semigroup.equivalence Semigroup⋆ = it
-- Semigroup._◇_ Semigroup⋆ g f = g ∘ f
-- Semigroup.◇-associativity Semigroup⋆ = {!!}

-- instance SemifunctorFinTerm : Semifunctor _⊸_ _≡̇_ (_⟨ Term ⟩→_) _≡̇_ id
-- Semifunctor.domain SemifunctorFinTerm = it
-- Semifunctor.codomain SemifunctorFinTerm = it
-- SemifunctorFinTerm Semifunctor.◃ = ⋆._◃_
-- Semifunctor.◃-extensionality SemifunctorFinTerm = ⋆.◃-extensionality
-- Semifunctor.◃-associativity SemifunctorFinTerm = ⋆.◃-associativity

-- -- sufficient for all my substitutions (Term, Formula, etc.)
-- _◂_ : ∀ {m n a} {A : Nat → Set a} ⦃ _ : Semifunctor _⊸_ _≡̇_ (_⟨ A ⟩→_) _≡̇_ id ⦄ → m ⊸ n → m ⟨ A ⟩→ n
-- _◂_ ⦃ semifunctor ⦄ f x = Semifunctor._◃ semifunctor f x

-- -- even more general, handling all pointwise (semi)functors
-- _◂'_ : ∀ {a} {A : Set a} {m n : A} {b} {B : A → Set b} {c} {C : A → Set c} {d} {D : A → Set d}
--          ⦃ _ : Semifunctor (λ m n → B m → C n) _≡̇_ _⟨ D ⟩→_ _≡̇_ id ⦄ → (B m → C n) → m ⟨ D ⟩→ n
-- _◂'_ ⦃ semifunctor ⦄ f x = Semifunctor._◃ semifunctor f x

-- record UsableSemifunctor {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) {d} (D : A → Set d) : Set (a ⊔ b ⊔ c ⊔ d) where
--   field
--     ⦃ semifunctor ⦄ : Semifunctor (λ m n → B m → C n) _≡̇_ _⟨ D ⟩→_ _≡̇_ id

--   _◄_ : ∀ {m n} → (B m → C n) → m ⟨ D ⟩→ n
--   _◄_ f x = Semifunctor._◃ semifunctor f x

-- open UsableSemifunctor ⦃ … ⦄

-- instance UsableSemifunctor⋆ : ∀ {a} {A : Set a} {b} {B : A → Set b} {c} {C : A → Set c} {d} {D : A → Set d}
--                               -- { _≋₁_ : ∀ {m n} → (B m → C n) → (B m → C n) → Set (b ⊔ c) }
--                               -- ⦃ _ : ∀ {m n} → Equivalence (_≋₁_ {m} {n}) ⦄
--                               -- ⦃ _ : Semifunctor (λ m n → B m → C n) _≋₁_ _⟨ D ⟩→_ _≡̇_ id ⦄ → UsableSemifunctor B C D
--                               ⦃ _ : Semifunctor (λ m n → B m → C n) _≡̇_ _⟨ D ⟩→_ _≡̇_ id ⦄
--                               → UsableSemifunctor B C D
-- UsableSemifunctor.semifunctor (UsableSemifunctor⋆ ⦃ semi ⦄) = semi

-- {-
-- instance UsableSemifunctorFinTermTerm : UsableSemifunctor Fin Term Term
-- UsableSemifunctor.semifunctor UsableSemifunctorFinTermTerm = it
-- -}

-- -- obviously won't work unless we supply _≋₁_
-- _◂''_ : ∀ {a} {A : Set a} {m n : A} {b} {B : A → Set b} {c} {C : A → Set c} {d} {D : A → Set d}
--         ( _≋₁_ : ∀ {m n} → (B m → C n) → (B m → C n) → Set (b ⊔ c) )
--         ⦃ _ : ∀ {m n} → Equivalence (_≋₁_ {m} {n}) ⦄
--         ⦃ _ : Semifunctor (λ m n → B m → C n) _≋₁_ _⟨ D ⟩→_ _≡̇_ id ⦄ → (B m → C n) → m ⟨ D ⟩→ n
-- _◂''_ _ ⦃ _ ⦄ ⦃ semifunctor ⦄ f x = Semifunctor._◃ semifunctor f x

-- foo : ∀ {m n} → m ⊸ n → Term m → Term n
-- foo {m} {n} f x = f ◄ x

-- --foo f x = f ◂ x
-- --foo f x = _◂''_ _≡̇_ f x

-- -- record Ṁonoid {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- --   field
-- --     ε̇ : ∀ {m} → B m → C m
-- --     _◇̇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
-- --     ◇̇-left-identity : ∀ {m n} → (f : B m → C n) → ε̇ ◇̇ f ≡̇ f
-- --     ◇̇-right-identity : ∀ {m n} → (f : B m → C n) → f ◇̇ ε̇ ≡̇ f
-- --     ◇̇-associativity : ∀ {k l m n} (f : B k → C l) (g : B l → C m) (h : B m → C n) → h ◇̇ (g ◇̇ f) ≡̇ (h ◇̇ g) ◇̇ f

-- -- record Monoid {a} {A : Set a} {b} (_↠_ : A → A → Set b) : Set (a ⊔ b) where
-- --   field
-- --     ε : ∀ {m} → m ↠ m
-- --     _◇_ : ∀ {l m n} → m ↠ n → l ↠ m → l ↠ n
-- --     ◇-left-identity : ∀ {m n} → (f : m ↠ n) → ε ◇ f ≡ f
-- --     ◇-right-identity : ∀ {m n} → (f : m ↠ n) → f ◇ ε ≡ f
-- --     ◇-associativity : ∀ {k l m n} (f : k ↠ l) (g : l ↠ m) (h : m ↠ n) → h ◇ (g ◇ f) ≡ (h ◇ g) ◇ f

-- -- record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- --   field
-- --     ε : ∀ {m} → B m → C m
-- --     _◇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
-- --     ◇-left-identity : ∀ {m n} → (f : B m → C n) → ε ◇ f ≡̇ f
-- --     ◇-right-identity : ∀ {m n} → (f : B m → C n) → f ◇ ε ≡̇ f
-- --     ◇-associativity : ∀ {k l m n} (f : B k → C l) (g : B l → C m) (h : B m → C n) → h ◇ (g ◇ f) ≡̇ (h ◇ g) ◇ f

-- -- record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- --   field
-- --     ε : ∀ {m} → B m → C m
-- --     _◇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
-- --     ◇-left-identity : ∀ {m n} → (f : B m → C n) → ε ◇ f ≡̇ f
-- --     ◇-right-identity : ∀ {m n} → (f : B m → C n) → f ◇ ε ≡̇ f
-- --     ◇-associativity : ∀ {k l m n} (f : B k → C l) (g : B l → C m) (h : B m → C n) → h ◇ (g ◇ f) ≡̇ (h ◇ g) ◇ f

-- -- record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- --   field
-- --     ε : ∀ {m} → B m → C m
-- --     _◇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
-- --     ◇-left-identity : ∀ {m n} → (f : B m → C n) → ε ◇ f ≡̇ f
-- --     ◇-right-identity : ∀ {m n} → (f : B m → C n) → f ◇ ε ≡̇ f
-- --     ◇-associativity : ∀ {k l m n} (f : B k → C l) (g : B l → C m) (h : B m → C n) → h ◇ (g ◇ f) ≡̇ (h ◇ g) ◇ f