text:
module Issue778M (Param : Set) where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

pred : Nat → Nat
pred = λ { zero → zero; (suc n) → n }
  where aux = zero

max_stars_repo_name: np/agda-git-experiment


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Syntax Experiment definitions.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.SyntaxExperiment ( n : ℕ ) where

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

open import Data.Bool using (false; true)

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Views n
open import Data.PropFormula.Dec n
open import Data.PropFormula.Properties n

open import Data.List public

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_)

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

data _⊢∧_ : Ctxt → List PropFormula → Set where

  empty-intro : ∀ {Γ} → Γ ⊢∧ []

  ∷-intro     : ∀ {Γ} {φ} {L}
              → Γ ⊢ φ
              → Γ ⊢∧ L
              → Γ ⊢∧ (φ ∷ L)

∷-proj₁
  : ∀ {Γ} {φ} {L}
  → Γ ⊢∧ (φ ∷ L)
  → Γ ⊢ φ
∷-proj₁ (∷-intro Γ⊢φ _) = Γ⊢φ

∷-proj₂
  : ∀ {Γ} {φ} {L}
  → Γ ⊢∧ (φ ∷ L)
  → Γ ⊢∧ L
∷-proj₂ (∷-intro _ Γ⊢∧L) = Γ⊢∧L

intro-thm
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢∧ [ φ ]
intro-thm {Γ} {φ} Γ⊢φ = ∷-intro Γ⊢φ empty-intro

++-intro  : ∀ {Γ} {L₁ L₂}
          → Γ ⊢∧ L₁ → Γ ⊢∧ L₂
          → Γ ⊢∧ (L₁ ++ L₂)
++-intro empty-intro th2 = th2
++-intro (∷-intro x th1) th2 = ∷-intro x (++-intro th1 th2)

toList : PropFormula → List PropFormula
toList φ with conj-view φ
toList .(φ₁ ∧ φ₂) | conj φ₁ φ₂ = toList φ₁ ++ toList φ₂
toList φ          | other .φ   = [ φ ]

⊢-to-⊢∧
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢∧ toList φ

⊢-to-⊢∧ {_} {φ} Γ⊢φ with conj-view φ
... | conj φ₁ φ₂ = ++-intro (⊢-to-⊢∧ (∧-proj₁ Γ⊢φ)) (⊢-to-⊢∧ (∧-proj₂ Γ⊢φ))
... | other .φ   = ∷-intro Γ⊢φ empty-intro

toProp : List PropFormula → PropFormula
toProp []       = ⊤
toProp (φ ∷ []) = φ
toProp (φ ∷ L)  = φ ∧ toProp L

⊢∧-to-⊢
  : ∀ {Γ} {L}
  → Γ ⊢∧ L
  → Γ ⊢ toProp L
⊢∧-to-⊢ {_} {[]}         _                 = ⊤-intro
⊢∧-to-⊢ {_} {_ ∷ []}     Γ⊢∧L              = ∷-proj₁ Γ⊢∧L
⊢∧-to-⊢ {_} {x ∷ _ ∷ _} (∷-intro Γ⊢φ Γ⊢∧L) = ∧-intro Γ⊢φ (⊢∧-to-⊢ Γ⊢∧L)

right-assoc-∧ : PropFormula → PropFormula
right-assoc-∧  = toProp ∘ toList

right-assoc-∧-lem
  : ∀ {Γ} {φ}
  → Γ ⊢ φ
  → Γ ⊢ right-assoc-∧ φ
right-assoc-∧-lem = ⊢∧-to-⊢ ∘ ⊢-to-⊢∧

find-conjunct : List PropFormula → PropFormula → PropFormula
find-conjunct [] x        = ⊤
find-conjunct (x ∷ xs) y with ⌊ eq x y ⌋
... | false = find-conjunct xs y
... | true  = x

find-conjunct-thm
  : ∀ {Γ} {L}
  → (ψ : PropFormula)
  → Γ ⊢∧ L
  → Γ ⊢ find-conjunct L ψ

find-conjunct-thm {_} {[]} ψ Γ⊢∧L    = ⊤-intro
find-conjunct-thm {_} {x ∷ L} ψ Γ⊢∧L with ⌊ eq x ψ ⌋
find-conjunct-thm {_} {x ∷ L} ψ Γ⊢∧L   | false with Γ⊢∧L
find-conjunct-thm {_} {x ∷ L} ψ Γ⊢∧L   | false | ∷-intro x₁ w = find-conjunct-thm ψ w
find-conjunct-thm {_} {x ∷ L} ψ Γ⊢∧L   | true  = ∷-proj₁ Γ⊢∧L

conjunct-thm
  : ∀ {Γ} {φ}
  → (ψ : PropFormula)
  → Γ ⊢ φ
  → Γ ⊢ find-conjunct (toList φ) ψ
conjunct-thm {_} ψ Γ⊢φ = find-conjunct-thm ψ (⊢-to-⊢∧ Γ⊢φ)

{-
toWeak : (Γ : List PropFormula) (ψ : PropFormula) → List PropFormula
toWeak t f = t , f , f

strip : ∀ {Γ} {φ} → (ψ : PropFormula) → Γ ⊢ φ → (toWeak Γ ψ) ⊢ φ
strip ψ Γ⊢φ = (weaken ψ (weaken ψ Γ⊢φ))

-- Bag Equivalance

-- open import Data.Fin using (Fin; suc; zero; #_)
-- open import Data.List using (length)

-- infixl 3 _↔_
-- record _↔_(A B : Set) : Set where
--   field
--     to      : A → B
--     from    : B → A
--     from-to : ∀ x → from (to x) ≡ x
--     to-from : ∀ x → to (from x) ≡ x

-- lookup : (xs : List PropFormula) → Fin (length xs) → PropFormula
-- lookup [] ()
-- lookup (x ∷ xs) zero    = x
-- lookup (x ∷ xs) (suc n) = lookup xs n

-- record _≈Bag_(xs ys : List PropFormula) : Set where
--   field
--     bijection : Fin (length xs) ↔ Fin (length ys)
--     related   : ∀ i → lookup xs i ≡ lookup ys (_↔_.to bijection i)

-- data _+_ (A B : Set) : Set where
--   left  : A → A + B
--   right : B → A + B

-- Any : (Prop → Set) → List PropFormula → Set
-- Any P []       = ⊥₂
-- Any P (x ∷ xs) = P x + Any P xs

-- infix 4 _∈₂_
-- _∈₂_ : PropFormula → List PropFormula → Set
-- x ∈₂ xs = Any (λ y → x ≡ y) xs

-- _≈Bag₂_ : List PropFormula → List PropFormula → Set
-- xs ≈Bag₂ ys = ∀ x → x ∈₂ xs ↔ x ∈₂ ys
-}

ext: agda

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples of printing list and vec-based tables
------------------------------------------------------------------------

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

module README.Text.Tabular where

open import Function.Base
open import Relation.Binary.PropositionalEquality

open import Data.List.Base
open import Data.String.Base
open import Data.Vec.Base

open import Text.Tabular.Base
import Text.Tabular.List as Tabularˡ
import Text.Tabular.Vec  as Tabularᵛ

------------------------------------------------------------------------
-- VEC
--
-- If you have a matrix of strings, you simply need to:
--   * pick a configuration (see below)
--   * pick an alignment for each column
--   * pass the matrix
--
-- The display function will then pad each string on the left, right,
-- or both to respect the alignment constraints.
-- It will return a list of strings corresponding to each line in the
-- table. You may then:
---  * use Data.String.Base's unlines to produce a String
--   * use Text.Pretty's text and vcat to produce a Doc (i.e. indentable!)
------------------------------------------------------------------------

_ : unlines (Tabularᵛ.display unicode
            (Right ∷ Left ∷ Center ∷ [])
          ( ("foo" ∷ "bar" ∷ "baz" ∷ [])
          ∷ ("1"   ∷ "2"   ∷ "3" ∷ [])
          ∷ ("6"   ∷ "5"   ∷ "4" ∷ [])
          ∷ []))
  ≡ "┌───┬───┬───┐
\   \│foo│bar│baz│
\   \├───┼───┼───┤
\   \│  1│2  │ 3 │
\   \├───┼───┼───┤
\   \│  6│5  │ 4 │
\   \└───┴───┴───┘"
_ = refl

------------------------------------------------------------------------
-- CONFIG
--
-- Configurations allow you to change the way the table is displayed.
------------------------------------------------------------------------

-- We will use the same example throughout

foobar : Vec (Vec String 2) 3
foobar = ("foo" ∷ "bar" ∷ [])
       ∷ ("1"   ∷ "2"   ∷ [])
       ∷ ("4"   ∷ "3"   ∷ [])
       ∷ []

------------------------------------------------------------------------
-- Basic configurations: unicode, ascii, whitespace

-- unicode

_ : unlines (Tabularᵛ.display unicode
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "┌───┬───┐
\   \│foo│bar│
\   \├───┼───┤
\   \│  1│2  │
\   \├───┼───┤
\   \│  4│3  │
\   \└───┴───┘"
_ = refl

-- ascii

_ : unlines (Tabularᵛ.display ascii
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "+-------+
\   \|foo|bar|
\   \|---+---|
\   \|  1|2  |
\   \|---+---|
\   \|  4|3  |
\   \+-------+"
_ = refl

-- whitespace

_ : unlines (Tabularᵛ.display whitespace
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "foo bar
\   \  1 2
\   \  4 3  "
_ = refl

------------------------------------------------------------------------
-- Modifiers: altering existing configurations

-- In these examples we will be using unicode as the base configuration.
-- However these modifiers apply to all configurations (and can even be
-- combined)

-- compact: drop the horizontal line between each row

_ : unlines (Tabularᵛ.display (compact unicode)
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "┌───┬───┐
\   \│foo│bar│
\   \│  1│2  │
\   \│  4│3  │
\   \└───┴───┘"
_ = refl

-- noBorder: drop the outside borders

_ : unlines (Tabularᵛ.display (noBorder unicode)
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "foo│bar
\   \───┼───
\   \  1│2
\   \───┼───
\   \  4│3  "
_ = refl

-- addSpace : add whitespace space inside cells

_ : unlines (Tabularᵛ.display (addSpace unicode)
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "┌─────┬─────┐
\   \│ foo │ bar │
\   \├─────┼─────┤
\   \│   1 │ 2   │
\   \├─────┼─────┤
\   \│   4 │ 3   │
\   \└─────┴─────┘"
_ = refl

-- compact together with addSpace

_ : unlines (Tabularᵛ.display (compact (addSpace unicode))
            (Right ∷ Left ∷ [])
            foobar)
  ≡ "┌─────┬─────┐
\   \│ foo │ bar │
\   \│   1 │ 2   │
\   \│   4 │ 3   │
\   \└─────┴─────┘"
_ = refl

------------------------------------------------------------------------
-- LIST
--
-- Same thing as for vectors except that if the list of lists is not
-- rectangular, it is padded with empty strings to make it so. If there
-- are not enough alignment directives, we arbitrarily pick Left.
------------------------------------------------------------------------

_ : unlines (Tabularˡ.display unicode
          (Center ∷ Right ∷ [])
          ( ("foo" ∷ "bar" ∷ [])
          ∷ ("partial" ∷ "rows" ∷ "are" ∷ "ok" ∷ [])
          ∷ ("3" ∷ "2" ∷ "1" ∷ "..." ∷ "surprise!" ∷ [])
          ∷ []))
  ≡ "┌───────┬────┬───┬───┬─────────┐
\   \│  foo  │ bar│   │   │         │
\   \├───────┼────┼───┼───┼─────────┤
\   \│partial│rows│are│ok │         │
\   \├───────┼────┼───┼───┼─────────┤
\   \│   3   │   2│1  │...│surprise!│
\   \└───────┴────┴───┴───┴─────────┘"
_ = refl

------------------------------------------------------------------------
-- LIST (UNSAFE)
--
-- If you know *for sure* that your data is already perfectly rectangular
-- i.e. all the rows of the list of lists have the same length
--      in each column, all the strings have the same width
-- then you can use the unsafeDisplay function defined Text.Tabular.Base.
--
-- This is what gets used internally by `Text.Tabular.Vec` and
-- `Text.Tabular.List` once the potentially unsafe data has been
-- processed.
------------------------------------------------------------------------

_ : unlines (unsafeDisplay (compact unicode)
          ( ("foo" ∷ "bar" ∷ [])
          ∷ ("  1" ∷ "  2" ∷ [])
          ∷ ("  4" ∷ "  3" ∷ [])
          ∷ []))
  ≡ "┌───┬───┐
\   \│foo│bar│
\   \│  1│  2│
\   \│  4│  3│
\   \└───┴───┘"
_ = refl


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

module Data.Vec.Iterated where

open import Data.Unit.UniversePolymorphic
open import Level
open import Data.Nat.Base
open import Function

private
  variable
    n m : ℕ

mutual
  Vec :  Type a → ℕ → Type a
  Vec A zero     = Vec⁰
  Vec A (suc n)  = Vec⁺ A n

  record Vec⁰ {a} : Type a where
    eta-equality
    constructor []

  infixr 5 _∷_
  record Vec⁺ {a} (A : Type a) (n : ℕ) : Type a where
    eta-equality
    inductive
    constructor _∷_
    field
      head : A
      tail : Vec A n

open Vec⁺ public

foldr : ∀ {p} (P : ℕ → Type p) →
          (∀ {n} → A → P n → P (suc n)) →
          P zero →
          Vec A n → P n
foldr {n = zero} P f b _         = b
foldr {n = suc n} P f b (x ∷ xs) = f x (foldr P f b xs)

foldl : ∀ {p} (P : ℕ → Type p) →
          (∀ {n} → A → P n → P (suc n)) →
          P zero →
          Vec A n → P n
foldl {n = zero } P f b _ = b
foldl {n = suc n} P f b (x ∷ xs) = foldl (P ∘ suc) f (f x b) xs

foldlN : ∀ {p} (P : ℕ → Type p) →
          (∀ {n} → A → P (suc n) → P n) →
          P n →
          Vec A n → P zero
foldlN P f b xs = foldr (λ n → P n → P zero) (λ x k xs → k (f x xs)) id xs b

module _ (f : A → B → B) (e : B) where
  foldr′ : Vec A n → B
  foldr′ {n = zero } xs = e
  foldr′ {n = suc n} (x ∷ xs) = f x (foldr′ xs)

foldl′ : (A → B → B) → B → Vec A n → B
foldl′ {n = zero}  f b xs = b
foldl′ {n = suc n} f b (x ∷ xs) = foldl′ f (f x b) xs

-- vecFromList : (xs : List A) → Vec A (length xs)
-- vecFromList List.[] = []
-- vecFromList (x List.∷ xs) = x ∷ vecFromList xs

-- vecToList : Vec A n → List A
-- vecToList = foldr′ List._∷_ List.[]

open import Data.Fin.Indexed

infixl 4 lookup
lookup : Fin n → Vec A n → A
lookup f0     = head
lookup (fs i) xs = lookup i (tail xs)

syntax lookup i xs = xs [ i ]

infixl 4 replace
replace : Fin n → A → Vec A n → Vec A n
replace f0     x xs .head = x
replace f0     x xs .tail = xs .tail
replace (fs i) x xs .head = xs .head
replace (fs i) x xs .tail = replace i x (xs .tail)

syntax replace i x xs = xs [ i ]≔ x

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Dependent product combinators for propositional equality
-- preserving functions
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Product.Function.Dependent.Propositional.WithK where

open import Data.Product
open import Data.Product.Function.Dependent.Setoid
open import Data.Product.Relation.Binary.Pointwise.Dependent
open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
open import Function.Equality using (_⟨$⟩_)
open import Function.Injection as Inj using (_↣_; module Injection)
open import Function.Inverse as Inv using (_↔_; module Inverse)
import Relation.Binary.HeterogeneousEquality as H

------------------------------------------------------------------------
-- Combinator for Injection

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {b₁ b₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
         where

  ↣ : ∀ (A₁↣A₂ : A₁ ↣ A₂) →
      (∀ {x} → B₁ x ↣ B₂ (Injection.to A₁↣A₂ ⟨$⟩ x)) →
      Σ A₁ B₁ ↣ Σ A₂ B₂
  ↣ A₁↣A₂ B₁↣B₂ =
    Inverse.injection Pointwise-≡↔≡ ⟨∘⟩
    injection (H.indexedSetoid B₂) A₁↣A₂
      (Inverse.injection (H.≡↔≅ B₂) ⟨∘⟩
       B₁↣B₂ ⟨∘⟩
       Inverse.injection (Inv.sym (H.≡↔≅ B₁))) ⟨∘⟩
    Inverse.injection (Inv.sym Pointwise-≡↔≡)
    where open Inj using () renaming (_∘_ to _⟨∘⟩_)


text:
open import Data.List
open import Data.Unit

open import Relation.Unary hiding (_∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Construct.Market
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Morphisms

module Relation.Ternary.Separation.Monad.State.Heap
  {ℓ}

  -- value types
  {T : Set ℓ}

  -- stored values
  (V : T → Pred (List T) ℓ)
  where

open import Level hiding (Lift)
open import Function using (_∘_; case_of_)
import Relation.Binary.HeterogeneousEquality as HEq
open import Relation.Unary.PredicateTransformer hiding (_⊔_; [_])
open import Relation.Binary.PropositionalEquality using (refl; _≡_)
open import Relation.Ternary.Separation.Construct.Product
open import Relation.Ternary.Separation.Construct.List T
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Allstar

open import Data.Product
open import Data.List.Relation.Ternary.Interleaving.Propositional as I

module HeapOps
  -- inner monad
  (M : Pt (Market (List T)) ℓ)
  {{monad : Monads.Monad ⊤ ℓ (λ _ _ → M) }}
  where
  Cells : Pred (List T × List T) ℓ
  Cells (Σ , Φ) = Allstar V Σ Φ

  open import Relation.Ternary.Separation.Monad.State
  open StateTransformer M public
  open Monads using (str)
  open Monads.Monad {{...}}

  -- Creating a reference to a new cell, filled with a given value.
  -- Note that in the market monoid this is pure!
  -- Because we get a reference that consumes the freshly created resource.
  newref : ∀ {a} → ∀[ V a ⇒ StateT M Cells (Just a) ]
  app (newref v) (lift st σ₁) (offerᵣ σ₂) =
    let _ , τ₁ , τ₂ = ⊎-assoc (⊎-comm σ₂) σ₁
    in return (
      inj refl
        ×⟨ offerᵣ ⊎-∙ ⟩
      lift (cons (v ×⟨ τ₂ ⟩ st)) (⊎-∙ₗ τ₁))

  -- A linear read on a store: you lose the reference.
  -- This is pure, because with the reference being lost, the cell is destroyed: no resources leak.
  read : ∀ {a} → ∀[ Just a ⇒ StateT M Cells (V a) ]
  app (read refl) (lift st σ₁) (offerᵣ σ₂) with ⊎-assoc σ₂ σ₁
  ... | _ , σ₃ , σ₄ with repartition σ₃ st
  ... | cons (v ×⟨ σ₅ ⟩ nil) ×⟨ σ₆ ⟩ st' with ⊎-id⁻ʳ σ₅ | ⊎-assoc (⊎-comm σ₆) (⊎-comm σ₄)
  ... | refl | _ , τ₁ , τ₂ = return (inj v ×⟨ offerᵣ τ₂ ⟩ lift st' (⊎-comm τ₁))

  -- Writing into a cell, returning the current contents
  write : ∀ {a b} → ∀[ Just b ✴ (V a) ⇒ StateT M Cells (Just a ✴ V b) ]
  app (write (refl ×⟨ σ₁ ⟩ v)) (lift st σ₂) (offerᵣ σ₃) with ⊎-assoc (⊎-comm σ₁) σ₃
  -- first we reassociate the arguments in the order that we want to piece it back together
  ... | _ , τ₁ , τ₂ with ⊎-assoc (⊎-comm τ₁) σ₂
  ... | _ , τ₃ , τ₄ with ⊎-assoc τ₂ τ₃
  ... | _ , τ₅ , τ₆
  -- then we reorganize the store internally to take out the unit value
    with repartition τ₅ st
  ... | cons (vb ×⟨ σ₅ ⟩ nil) ×⟨ σ₆ ⟩ st' rewrite ⊎-id⁻ʳ σ₅ =
    let
      _ , κ₁ , κ₂ = ⊎-unassoc τ₄ (⊎-comm σ₆)
      _ , κ₃ , κ₄ = ⊎-assoc κ₂ (⊎-comm τ₆)
    in return (
      inj (refl ×⟨ consˡ ⊎-idˡ ⟩ vb)
        ×⟨ offerᵣ (consˡ κ₄) ⟩
      lift (cons (v ×⟨ κ₁ ⟩ st')) (⊎-∙ₗ (⊎-comm κ₃)))

  -- A linear (strong) update on the store
  update! : ∀ {a b} → ∀[ Just a ⇒ (V a ─✴ StateT M Cells (V b)) ─✴ StateT M Cells (Just b) ]
  app (update! ptr) f σ = do
    a ×⟨ σ₁ ⟩ f ← read ptr &⟨ σ ⟩ f
    b           ← app f a (⊎-comm σ₁)
    newref b


text:
module STLC.Type.Context where

open import STLC.Type as Type using (Type)
open Type.Substitution using () renaming (_⊙_ to _⊙τ_; _/_ to _/τ_; wk to wk-τ)

open import Data.Nat using (ℕ; _+_)

open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Substitution

open import Data.Vec using (Vec; []; _∷_; map; lookup)
open import Data.Vec.Properties
  using (map-∘; map-cong; lookup-map)

open import Relation.Binary.PropositionalEquality as Eq
  using (refl; _≡_; sym; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

-- --------------------------------------------------------------------
-- Typing Contexts
-- --------------------------------------------------------------------
-- A typing context Γ is the mapping from free term variables to
-- types. A context Γ m n maps m term variables to tyhpes containing
-- n type variables.

Ctxt : ℕ -> ℕ -> Set
Ctxt m n = Vec (Type n) m

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

module Substitution where

  infixl 8 _/_ _/Var_

  -- Type substitutions lifted to typing contexts
  _/_ : ∀ { m n p } -> Ctxt m n -> Sub Type n p -> Ctxt m p
  Γ / ρ = Γ ⊙τ ρ

  -- Weakening of typing contexts
  weaken : ∀ { m n } -> Ctxt m n -> Ctxt m (1 + n)
  weaken Γ = map Type.Substitution.weaken Γ

  -- Term variable substitution
  _/Var_ : ∀  { m n p } -> Sub Fin m n -> Ctxt n p -> Ctxt m p
  θ /Var Γ = map (lookup Γ) θ

module Lemmas where
  open Substitution

  private module Lemmas-τ = Type.Lemmas

  -- /Var and / commute
  /Var-/-comm : ∀ { m n p q } (Γ : Ctxt p n) (θ : Sub Fin m p) (ρ : Sub Type n q)
    -> (θ /Var Γ) / ρ ≡ θ /Var (Γ / ρ)
  /Var-/-comm Γ θ ρ =
    begin
      (θ /Var Γ) / ρ
    ≡⟨ sym (map-∘ _ _ θ) ⟩
      map (λ x -> (lookup Γ x) /τ ρ) θ
    ≡⟨ map-cong (λ x → sym (Lemmas-τ.lookup-⊙ x {ρ₁ = Γ})) θ  ⟩
      map (λ x -> lookup (Γ / ρ) x) θ
    ∎

  -- /Var and weaken commute
  /Var-weaken-comm : ∀  { m n p } (θ : Sub Fin m p) (Γ : Ctxt p n)
    -> weaken (θ /Var Γ) ≡ θ /Var (weaken Γ)
  /Var-weaken-comm θ Γ =
    begin
      weaken (θ /Var Γ)
    ≡⟨ Lemmas-τ.map-weaken ⟩
      (θ /Var Γ) / wk-τ
    ≡⟨ /Var-/-comm Γ θ wk-τ ⟩
      θ /Var (Γ / wk-τ)
    ≡⟨ sym (cong (λ Γ -> θ /Var Γ) (Lemmas-τ.map-weaken {ρ = Γ})) ⟩
      θ /Var (weaken Γ)
    ∎

  -- /Var and lookup commute
  /Var-lookup-comm : ∀  { m n p } (x : Fin m) (θ : Sub Fin m p) (Γ : Ctxt p n)
    -> lookup (θ /Var Γ) x ≡ lookup Γ (lookup θ x)
  /Var-lookup-comm x θ Γ =
    begin
      lookup (θ /Var Γ) x
    ≡⟨⟩
      lookup (map (lookup Γ) θ) x
    ≡⟨ lookup-map x (lookup Γ) θ ⟩
      lookup Γ (lookup θ x)
    ∎

  /Var-∷-comm : ∀ { m n p } (τ : Type n) (θ : Sub Fin m p) (Γ : Ctxt p n)
    -> τ ∷ (θ /Var Γ) ≡ (θ VarSubst.↑) /Var (τ ∷ Γ)
  /Var-∷-comm τ [] Γ = refl
  /Var-∷-comm τ (x ∷ θ) Γ =
    begin
      τ ∷ ((x ∷ θ) /Var Γ)
    ≡⟨⟩
      τ ∷ (lookup Γ x) ∷ (θ /Var Γ)
    ≡⟨ cong (λ Γ' -> τ ∷ (lookup Γ x) ∷ Γ') lemma ⟩
      τ ∷ (lookup Γ x) ∷ map (lookup (τ ∷ Γ)) (map suc θ)
    ≡⟨⟩
      map (lookup (τ ∷ Γ)) (zero ∷ suc x ∷ map suc θ)
    ≡⟨⟩
      ((x ∷ θ) VarSubst.↑) /Var (τ ∷ Γ)
    ∎
    where
      lemma =
        begin
          θ /Var Γ
        ≡⟨⟩
          map (lookup Γ) θ
        ≡⟨⟩
          map (λ x -> lookup (τ ∷ Γ) (suc x)) θ
        ≡⟨ map-∘ _ _ θ ⟩
          map (lookup (τ ∷ Γ)) (map suc θ)
        ∎

  -- invariant on renaming of id
  /Var-id-inv : ∀ { m n } (Γ : Ctxt m n) -> Γ ≡ (VarSubst.id /Var Γ)

  /Var-id-inv [] = refl
  /Var-id-inv (τ ∷ Γ) =
    begin
      τ ∷ Γ
    ≡⟨ cong (λ Γ -> τ ∷ Γ) (/Var-id-inv Γ) ⟩
      τ ∷ (VarSubst.id /Var Γ)
    ≡⟨ /Var-∷-comm τ VarSubst.id Γ ⟩
      (VarSubst.id VarSubst.↑) /Var (τ ∷ Γ)
    ≡⟨⟩
      VarSubst.id /Var (τ ∷ Γ)
    ∎

  -- invariant on adding additional types, also known as the weakening lemma
  /Var-wk-inv : ∀ { m n } (Γ : Ctxt m n) -> (τ : Type n) -> Γ ≡ (VarSubst.wk /Var (τ ∷ Γ))
  /Var-wk-inv Γ τ =
    begin
      Γ
    ≡⟨ /Var-id-inv Γ ⟩
      VarSubst.id /Var Γ
    ≡⟨ map-∘ _ _ VarSubst.id ⟩
      VarSubst.wk /Var (τ ∷ Γ)
    ∎

max_stars_repo_name: johnyob/agda-types

max_issues_repo_name: johnyob/agda-types

max_forks_repo_name: johnyob/agda-types


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X] where

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

open import Cubical.Data.Nat using (ℕ) renaming (_+_ to _+n_)
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat
open import Cubical.Data.Sigma

open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly

private variable
  ℓ ℓ' : Level

module Comp-Poly-nm
  (Acr@(A , Astr) : CommRing ℓ)
  (n m : ℕ)
  where

  private
    PAm   = PolyCommRing Acr m
    PAn+m = PolyCommRing Acr (n +n m)
    PAmn  = PolyCommRing (PolyCommRing Acr m) n

  open CommRingStr

-----------------------------------------------------------------------------
-- direct sens

  PAmn→PAn+m-base : (v : Vec ℕ n) → Poly Acr m → Poly Acr (n +n m)
  PAmn→PAn+m-base v = DS-Rec-Set.f _ _ _ _ trunc
                       (0r (snd PAn+m))
                       (λ v' a → base (v ++ v') a)
                       (_+_ (snd PAn+m))
                       (+Assoc (snd PAn+m))
                       (+IdR (snd PAn+m))
                       (+Comm (snd PAn+m))
                       (λ v' → base-neutral (v ++ v'))
                       (λ v' a b → base-add (v ++ v') a b)

  PAmn→PAn+m : Poly (PolyCommRing Acr m) n → Poly Acr (n +n m)
  PAmn→PAn+m = DS-Rec-Set.f _ _ _ _ trunc
                (0r (snd PAn+m))
                PAmn→PAn+m-base
                (_+_ (snd PAn+m))
                (+Assoc (snd PAn+m))
                (+IdR (snd PAn+m))
                (+Comm (snd PAn+m))
                (λ _ → refl)
                λ _ _ _ → refl

-----------------------------------------------------------------------------
-- Converse sens

  PAn+m→PAmn : Poly Acr (n +n m) → Poly (PolyCommRing Acr m) n
  PAn+m→PAmn = DS-Rec-Set.f _ _ _ _ trunc
                (0r (snd PAmn))
                (λ v a → base (fst (sep-vec n m v)) (base (snd (sep-vec n m v)) a))
                (_+_ (snd PAmn))
                (+Assoc (snd PAmn))
                (+IdR (snd PAmn))
                (+Comm (snd PAmn))
                (λ v → (cong (base (fst (sep-vec n m v))) (base-neutral _)) ∙ (base-neutral _))
                 λ v a b → base-add _ _ _ ∙ cong (base (fst (sep-vec n m v))) (base-add _ _ _)

-----------------------------------------------------------------------------
-- Section

  e-sect : (P : Poly Acr (n +n m)) → PAmn→PAn+m (PAn+m→PAmn P) ≡ P
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
           refl
           (λ v a → cong (λ X → base X a) (sep-vec-id n m v))
           (λ {U V} ind-U ind-V → cong₂ (_+_ (snd PAn+m)) ind-U ind-V)

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (P : Poly (PolyCommRing Acr m) n) → PAn+m→PAmn (PAmn→PAn+m P) ≡ P
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc  _ _)
           refl
           (λ v → DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                   (sym (base-neutral _))
                   (λ v' a → cong₂ base (sep-vec-fst n m v v')
                                          (cong (λ X → base X a) (sep-vec-snd n m v v')))
                   λ {U V} ind-U ind-V → (cong₂ (_+_ (snd PAmn)) ind-U ind-V) ∙ (base-add _ _ _))
           (λ {U V} ind-U ind-V → cong₂ (_+_ (snd PAmn)) ind-U ind-V)

-----------------------------------------------------------------------------
-- Morphism of ring

  PAmn→PAn+m-pres1 : PAmn→PAn+m (1r (snd PAmn)) ≡ 1r (snd PAn+m)
  PAmn→PAn+m-pres1 = cong (λ X → base X (1r Astr)) (rep-concat n m 0 )

  PAmn→PAn+m-pres+ : (P Q : Poly (PolyCommRing Acr m) n) →
                      PAmn→PAn+m (snd PAmn ._+_ P Q) ≡ snd PAn+m ._+_ (PAmn→PAn+m P) (PAmn→PAn+m Q)
  PAmn→PAn+m-pres+ = λ _ _ → refl

  PAmn→PAn+m-pres· : (P Q : Poly (PolyCommRing Acr m) n) →
                      PAmn→PAn+m ( snd PAmn ._·_ P Q) ≡ snd PAn+m ._·_ (PAmn→PAn+m P) (PAmn→PAn+m Q)
  PAmn→PAn+m-pres· =
    DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ (λ _ → trunc _ _))
    (λ Q → refl)
    (λ v → DS-Ind-Prop.f _ _ _ _ (λ _ → isPropΠ (λ _ → trunc _ _))
            (λ Q → cong (λ X → PAmn→PAn+m (snd PAmn ._·_ X Q)) (base-neutral v))
            (λ v' a → DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                       refl
                       (λ w → DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                               refl
                               (λ w' b → cong (λ X → base X (Astr ._·_ a b)) (+n-vec-concat _ _ _ _ _ _))
                               λ {U V} ind-U ind-V → cong (λ X → PAmn→PAn+m (snd PAmn ._·_ (base v (base v' a)) X))
                                                           (sym (base-add _ _ _))
                                                      ∙ cong₂ (snd PAn+m ._+_) ind-U ind-V
                                                      ∙ sym (cong (λ X → snd PAn+m ._·_ (PAmn→PAn+m (base v (base v' a)))
                                                                  (PAmn→PAn+m X)) (base-add _ _ _)))
                       λ {U V} ind-U ind-V → cong₂ (snd PAn+m ._+_) ind-U ind-V)
            λ {U V} ind-U ind-V Q → cong (λ X → PAmn→PAn+m (snd PAmn ._·_ X Q)) (sym (base-add _ _ _))
                                     ∙ cong₂ (snd PAn+m ._+_) (ind-U Q) (ind-V Q)
                                     ∙ sym (cong (λ X → snd PAn+m ._·_ (PAmn→PAn+m X) (PAmn→PAn+m Q)) (base-add _ _ _)))
    λ {U V} ind-U ind-V Q → cong₂ (_+_ (snd PAn+m)) (ind-U Q) (ind-V Q)

-----------------------------------------------------------------------------
-- Ring Equivalence

module _ (A' : CommRing ℓ) (n m : ℕ) where

  open Comp-Poly-nm A' n m

  CRE-PolyN∘M-PolyN+M : CommRingEquiv (PolyCommRing (PolyCommRing A' m) n) (PolyCommRing A' (n +n m))
  fst CRE-PolyN∘M-PolyN+M = isoToEquiv is
    where
    is : Iso _ _
    Iso.fun is = PAmn→PAn+m
    Iso.inv is = PAn+m→PAmn
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr

  snd CRE-PolyN∘M-PolyN+M = makeIsRingHom PAmn→PAn+m-pres1 PAmn→PAn+m-pres+ PAmn→PAn+m-pres·

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module Foundation where

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

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

Op₀ : ∀ {ℓ} → ℞ ℓ → ℞ ℓ
Op₀ = id

Op₁ : ∀ {a} → ℞ a → ℞ a
Op₁ A = A → Op₀ A

Op₂ : ∀ {a} (A : ℞ a) → ℞ a
Op₂ A = A → Op₁ A

record ♩Op₀ {a} (A : ℞ a) : ℞ a where field 𝟘 : Op₀ A

record ♩Op₁ {a} (A : ℞ a) : ℞ a where
  infixr 65536 ¡_
  field ¡_ : Op₁ A

record ♩Op₂ {a} (A : ℞ a) : ℞ a where
  infixl 0 _∙_
  field _∙_ : Op₂ A

open ♩Op₀ ⦃ … ⦄ public
open ♩Op₁ ⦃ … ⦄ public
open ♩Op₂ ⦃ … ⦄ public

instance Set₀♩Op₀=Level : ♩Op₀ Set₀
Set₀♩Op₀=Level = record { 𝟘 = Level } where open import Agda.Primitive

instance Set₀♩Op₀=Nat : ♩Op₀ _
♩Op₀.𝟘 Set₀♩Op₀=Nat = Nat where open import Agda.Builtin.Nat

instance Nat♩Op₁=successor : ♩Op₁ 𝟘
♩Op₁.¡_ Nat♩Op₁=successor = suc where open import Agda.Builtin.Nat

instance zero♩Op₀Nat : ♩Op₀ 𝟘
♩Op₀.𝟘 zero♩Op₀Nat = zero where open import Agda.Builtin.Nat

instance Level♩Op₀ : ♩Op₀ 𝟘
♩Op₀.𝟘 Level♩Op₀ = lzero where open import Agda.Primitive

instance Level♩Op₁ : ♩Op₁ _
♩Op₁.¡_ Level♩Op₁ = lsuc where open import Agda.Primitive

instance Level♩Op₂ : ♩Op₂ 𝟘
♩Op₂._∙_ Level♩Op₂ = _⊔_ where open import Agda.Primitive

_℞_ : ∀ {a} (A : ℞ a) → ∀ ℓ → ℞ _
_℞_ A ℓ = A → ℞ ℓ

_₂℞_ : ∀ {a} (A : ℞ a) → ∀ ℓ → ℞ _
_₂℞_ A ℓ = A → A ℞ ℓ

record IsReflexive {a} {A : ℞ a} {ℓ} (_∼_ : A ₂℞ ℓ) : ℞ a ∙ ℓ where
  field
    reflexive : ∀ {x} → x ∼ x

open IsReflexive ⦃ … ⦄

record IsSymmetric {a} {A : ℞ a} {ℓ} (_∼_ : A ₂℞ ℓ) : ℞ a ∙ ℓ where
  field
    symmetric : ∀ {x} {y} → x ∼ y → y ∼ x

open IsSymmetric ⦃ … ⦄

record IsTransitive {a} {A : ℞ a} {ℓ} (_∼_ : A ₂℞ ℓ) : ℞ a ∙ ℓ where
  field
    transitive : ∀ {x} {y} {z} → x ∼ y → y ∼ z → x ∼ z

open IsTransitive ⦃ … ⦄

record IsEquivalence {a} {A : ℞ a} {ℓ} (_≈_ : A ₂℞ ℓ) : ℞ a ∙ ℓ where
  field
    overlap ⦃ reflexive ⦄ : IsReflexive _≈_
    overlap ⦃ symmetric ⦄ : IsSymmetric _≈_
    overlap ⦃ transitive ⦄ : IsTransitive _≈_

open IsEquivalence ⦃ … ⦄
open import Agda.Primitive

record Equivalence {a} (A : ℞ a) ℓ : ℞ (a ∙ ¡ ℓ) where
  infix 4 _≈_
  field
    _≈_ : A ₂℞ ℓ
    isEquivalence : IsEquivalence _≈_

open Equivalence ⦃ … ⦄

record IsAssociative {a} {A : ℞ a} (_∘_ : Op₂ A) {ℓ} (_≈_ : A ₂℞ ℓ) : ℞ a ∙ ¡ ℓ where
  field
    associative : ∀ x y z → (x ∘ (y ∘ z)) ≈ ((x ∘ y) ∘ z)

open IsAssociative ⦃ … ⦄

import Relation.Binary.Core as R

record ⟦_Preserves₂_⟶_⟶_⟧
       {a b c ℓ₁ ℓ₂ ℓ₃} {A : ℞ a} {B : ℞ b} {C : ℞ c}
       (_+_ : A → B → C) (P : R.Rel A ℓ₁) (Q : R.Rel B ℓ₂) (R : R.Rel C ℓ₃)
       : ℞ a ∙ b ∙ ℓ₁ ∙ ℓ₂ ∙ ℓ₃ where
  field
    _⟶_ : ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)

open ⟦_Preserves₂_⟶_⟶_⟧ ⦃ … ⦄

record Cong₂
       a b c
       (P : ∀ {x} {X : Set x} → X → X → Set (a ∙ x))
       : ℞ ¡ a ∙ ¡ b ∙ ¡ c where
  field
    cong₂ : {A : ℞ a} {B : ℞ b} {C : ℞ c} (_+_ : A → B → C) → ∀ {x y u v} → P x y → P u v → P (x + u) (y + v)

open Cong₂ ⦃ … ⦄

open import Prelude.Function using (_∘_; _∘′_)
open import Level

--instance Cong₂≡ : ∀ {a b c} → Cong₂ a b c (λ x₁ x₂ → Lift (x₁ R.≡ x₂)) -- R._≡_
--Cong₂≡ = {!!}
--Cong₂.cong₂ Cong₂≡ _+_ R.refl R.refl = R.refl

record Semigroup {a} (A : ℞ a) ℓ : ℞ a ∙ ¡ ℓ where
  field
    _⁀_ : Op₂ A
    overlap ⦃ equivalence ⦄ : Equivalence A ℓ
    ⦃ isAssociative ⦄ : IsAssociative _⁀_ _≈_
    ⦃ ∙-cong ⦄ : ⟦ _⁀_ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ ⟧

open Semigroup ⦃ … ⦄

record IdentityElement {a} (A : ℞ a) : ℞ a where
  field
    ε : A

open IdentityElement ⦃ … ⦄

record IsLeftIdentity {a} {A : ℞ a} ℓ (ε : A) (_∘_ : Op₂ A) : ℞ ¡ ℓ ∙ a where
  field
    overlap ⦃ equivalence ⦄ : Equivalence A ℓ
    left-identity : ∀ x → ε ∘ x ≈ x

open IsLeftIdentity ⦃ … ⦄

record IsRightIdentity {a} {A : ℞ a} ℓ (ε : A) (_∘_ : Op₂ A) : ℞ ¡ ℓ ∙ a where
  field
    overlap ⦃ equivalence ⦄ : Equivalence A ℓ
    right-identity : ∀ x → x ∘ ε ≈ x

open IsRightIdentity ⦃ … ⦄

record IsIdentity {a} {A : ℞ a} ℓ (ε : A) (_∘_ : Op₂ A) : ℞ ¡ ℓ ∙ a where
  field
    ⦃ isLeftIdentity ⦄ : IsLeftIdentity ℓ ε _∘_
    ⦃ isRightIdentity ⦄ : IsRightIdentity ℓ ε _∘_

open IsIdentity ⦃ … ⦄

record IsMonoid {a} (A : ℞ a) (ε : A) ℓ
  : ℞ a ∙ ¡ ℓ where
  field
    ⦃ semigroup ⦄ : Semigroup A ℓ
    ⦃ isIdentity ⦄ : IsIdentity ℓ ε _⁀_

open IsMonoid ⦃ … ⦄

record Monoid {a} (A : ℞ a) ℓ : ℞ a ∙ ¡ ℓ where
  field
    ⦃ identityElement ⦄ : IdentityElement A
    ⦃ isMonoid ⦄ : IsMonoid A ε ℓ

open Monoid ⦃ … ⦄

foo : (A : Set) ⦃ _ : Monoid A Level.zero ⦄ → (x : A) → (x ⁀ ε) ≈ x
foo A ⦃ m ⦄ x₁ = right-identity {zero} {{!!}}  {{!!}}  {{!!}} {{!!}} ⦃ isRightIdentity {{!!}} {{!!}} {{!!}} {{!!}} {{!!}} ⦄ x₁


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

module Dodo.Nullary.Unique where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open import Level using (Level)

-- # Definitions

Unique : ∀ {a : Level} (A : Set a) → Set _
Unique A = ∀ (x y : A) → x ≡ y

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
{-
This second-order term syntax was created from the following second-order syntax description:

$sig_string
-}

module ${syn_name}.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import ${syn_name}.Signature

private
  variable
    Γ Δ Π : Ctx
    $ty_vars : $type
    𝔛 : Familyₛ

-- Inductive term declaration
module ${sig}:Terms (𝔛 : Familyₛ) where

  data ${sig} : Familyₛ where
    var  : ℐ ⇾̣ ${sig}
    mvar : 𝔛 $fst_ty_var Π → Sub ${sig} Π Γ → ${sig} $fst_ty_var Γ

    $syn_constructors

  $op_fixity

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  ${sig}ᵃ : MetaAlg ${sig}
  ${sig}ᵃ = record
    { 𝑎𝑙𝑔 = λ where
      $alg_patterns
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module ${sig}ᵃ = MetaAlg ${sig}ᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : ${sig} ⇾̣ 𝒜
    𝕊 : Sub ${sig} Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    $sem_patterns

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ ${sig}ᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ ${sig} $fst_ty_var Γ) → 𝕤𝕖𝕞 (${sig}ᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      $alg_hom_patterns

      𝕊-tab : (mε : Π ~[ ${sig} ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : ${sig} ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ ${sig}ᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : ${sig} $fst_ty_var Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub ${sig} Π Γ)(v : ℐ $fst_ty_var Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      $alg_unique_patterns

-- Syntax instance for the signature
${sig}:Syn : Syntax
${sig}:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = ${sig}:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open ${sig}:Terms 𝔛 in record
    { ⊥ = ${sig} ⋉ ${sig}ᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax ${sig}:Syn public
open ${sig}:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands ${sig}ᵃ public
open import SOAS.Metatheory ${sig}:Syn public

$derived_tm_ops

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Prod {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening as T hiding (wk; wkTerm; wkEqTerm)
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Weakening
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Application
open import Definition.LogicalRelation.Substitution
open import Definition.LogicalRelation.Substitution.Properties
open import Definition.LogicalRelation.Substitution.Reflexivity
open import Definition.LogicalRelation.Substitution.Introductions.Pi
open import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

open import Tools.Product
import Tools.PropositionalEquality as PE

prod′ : ∀ {F G t u Γ l l′ l″}
       ([F] : Γ ⊩⟨ l ⟩ F)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ F / [F])
       ([Gt] : Γ ⊩⟨ l″ ⟩ G [ t ])
       ([u] : Γ ⊩⟨ l″ ⟩ u ∷ G [ t ] / [Gt])
       ([ΣFG] : Γ ⊩⟨ l′ ⟩B⟨ BΣ ⟩ Σ F ▹ G)
     → Γ ⊩⟨ l′ ⟩ prod t u ∷ Σ F ▹ G / B-intr BΣ [ΣFG]
prod′ {F} {G} {t} {u} {Γ} {l} {l′} {l″} [F] [t] [Gt] [u]
      [ΣFG]@(noemb (Bᵣ F₁ G₁ D ⊢F ⊢G A≡A [F]₁ [G]₁ G-ext)) with
        B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let ⊢t = escapeTerm [F] [t]
      ⊢u = escapeTerm [Gt] [u]
      ⊢Γ = wf ⊢F

      fst⇒t : Γ ⊢ fst (prod t u) ⇒ t ∷ F
      fst⇒t = Σ-β₁ ⊢F ⊢G ⊢t ⊢u
      [fstprod] , [fstprod≡t] = redSubstTerm fst⇒t [F] [t]
      [fstprod]′ = (irrelevanceTerm′ (PE.sym (wk-id F))
                                     [F] ([F]₁ id ⊢Γ)
                                     [fstprod])

      wkLiftIdEq = PE.cong (λ x → x [ fst (prod t u ) ]) (wk-lift-id G)
      [Gfst] = [G]₁ id ⊢Γ [fstprod]′
      [Gfst]′ = irrelevance′ wkLiftIdEq [Gfst]

      [t]′ = irrelevanceTerm′ (PE.sym (wk-id F))
                              [F] ([F]₁ id ⊢Γ)
                              [t]
      [fstprod≡t]′ = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                        [F] ([F]₁ id ⊢Γ)
                                        [fstprod≡t]

      [Gfst≡Gt] = irrelevanceEq″ wkLiftIdEq (PE.cong (λ x → x [ t ]) (wk-lift-id G))
                                 [Gfst] [Gfst]′
                                 (G-ext id ⊢Γ [fstprod]′ [t]′ [fstprod≡t]′)
      [u]′ = convTerm₂ [Gfst]′ [Gt] [Gfst≡Gt] [u]

      snd⇒u : Γ ⊢ snd (prod t u) ⇒ u ∷ G [ fst (prod t u) ]
      snd⇒u = Σ-β₂ ⊢F ⊢G ⊢t ⊢u
      [sndprod] , [sndprod≡u] = redSubstTerm snd⇒u [Gfst]′ [u]′

      ⊢prod = prodⱼ ⊢F ⊢G ⊢t ⊢u

      [fstRefl] = transEqTerm [F] [fstprod≡t] (symEqTerm [F] [fstprod≡t])
      [sndRefl] = transEqTerm [Gfst]′ [sndprod≡u] (symEqTerm [Gfst]′ [sndprod≡u])
  in  Σₜ (prod t u)
         (idRedTerm:*: ⊢prod)
         prodₙ
         (≅-Σ-η ⊢F ⊢G ⊢prod ⊢prod prodₙ prodₙ
                (escapeTermEq [F] [fstRefl])
                (escapeTermEq [Gfst]′ [sndRefl]))
         [fstprod]′
         (irrelevanceTerm′ (PE.sym wkLiftIdEq)
                       [Gfst]′ [Gfst]
                       [sndprod])
prod′ {F} {G} {t} {u} {Γ} {l} {l′} [F] [t] [Gt] [u]
      [ΣFG]@(emb 0<1 x) = prod′ [F] [t] [Gt] [u] x

prod″ : ∀ {F G t u Γ l l′}
       ([F] : Γ ⊩⟨ l ⟩ F)
       ([t] : Γ ⊩⟨ l ⟩ t ∷ F / [F])
       ([Gt] : Γ ⊩⟨ l ⟩ G [ t ])
       ([u] : Γ ⊩⟨ l ⟩ u ∷ G [ t ] / [Gt])
       ([ΣFG] : Γ ⊩⟨ l′ ⟩ Σ F ▹ G)
     → Γ ⊩⟨ l′ ⟩ prod t u ∷ Σ F ▹ G / [ΣFG]
prod″ [F] [t] [Gt] [u] [ΣFG] =
      let [prod] = prod′ [F] [t] [Gt] [u] (B-elim BΣ [ΣFG])
      in  irrelevanceTerm (B-intr BΣ (B-elim BΣ [ΣFG])) [ΣFG] [prod]

prod-cong′ : ∀ {F G t t′ u u′ Γ l l′}
             ([F] : Γ ⊩⟨ l ⟩ F)
             ([t] : Γ ⊩⟨ l ⟩ t ∷ F / [F])
             ([t′] : Γ ⊩⟨ l ⟩ t′ ∷ F / [F])
             ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ F / [F])
             ([Gt] : Γ ⊩⟨ l ⟩ G [ t ])
             ([u] : Γ ⊩⟨ l ⟩ u ∷ G [ t ] / [Gt])
             ([u′] : Γ ⊩⟨ l ⟩ u′ ∷ G [ t ] / [Gt])
             ([u≡u′] : Γ ⊩⟨ l ⟩ u ≡ u′ ∷ G [ t ] / [Gt])
             ([ΣFG] : Γ ⊩⟨ l′ ⟩B⟨ BΣ ⟩ Σ F ▹ G)
             → Γ ⊩⟨ l′ ⟩ prod t u ≡ prod t′ u′ ∷ Σ F ▹ G / B-intr BΣ [ΣFG]
prod-cong′ {F} {G} {t} {t′} {u} {u′} {Γ} {l} {l′}
           [F] [t] [t′] [t≡t′] [Gt] [u] [u′] [u≡u′]
           [ΣFG]@(noemb (Bᵣ F₁ G₁ D ⊢F ⊢G A≡A [F]₁ [G]₁ G-ext)) with
             B-PE-injectivity BΣ (whnfRed* (red D) Σₙ)
... | PE.refl , PE.refl =
  let [prod] = prod′ [F] [t] [Gt] [u] [ΣFG]

      ⊢Γ = wf ⊢F
      wk[F] = [F]₁ id ⊢Γ
      wk[t] = irrelevanceTerm′ (PE.sym (wk-id F)) [F] wk[F] [t]
      wk[t′] = irrelevanceTerm′ (PE.sym (wk-id F)) [F] wk[F] [t′]
      wk[t≡t′] = irrelevanceEqTerm′ (PE.sym (wk-id F)) [F] wk[F] [t≡t′]
      wk[Gt] = [G]₁ id ⊢Γ wk[t]
      wk[Gt′] = [G]₁ id ⊢Γ wk[t′]
      wk[Gt≡Gt′] = G-ext id ⊢Γ wk[t] wk[t′] wk[t≡t′]

      [Gt′] = irrelevance′ (PE.cong (λ x → x [ t′ ]) (wk-lift-id G)) wk[Gt′]
      [Gt≡Gt′] = irrelevanceEq″ (PE.cong (λ x → x [ t ]) (wk-lift-id G))
                                (PE.cong (λ x → x [ t′ ]) (wk-lift-id G))
                                wk[Gt] [Gt]
                                wk[Gt≡Gt′]

      [u′]Gt′ = convTerm₁ [Gt] [Gt′] [Gt≡Gt′] [u′]

      [prod′] = prod′ [F] [t′] [Gt′] [u′]Gt′ [ΣFG]

      ⊢t = escapeTerm [F] [t]
      ⊢t′ = escapeTerm [F] [t′]
      ⊢u = escapeTerm [Gt] [u]
      ⊢u′ = escapeTerm [Gt′] [u′]Gt′

      fst⇒t = Σ-β₁ ⊢F ⊢G ⊢t ⊢u
      [fst] , [fst≡t] = redSubstTerm fst⇒t [F] [t]
      fst⇒t′ = Σ-β₁ ⊢F ⊢G ⊢t′ ⊢u′
      [fst′] , [fst≡t′] = redSubstTerm fst⇒t′ [F] [t′]

      wk[fst≡t] = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                      [F] wk[F]
                                      [fst≡t]
      wk[fst≡t′] = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                      [F] wk[F]
                                      [fst≡t′]

      wk[fst] = irrelevanceTerm′ (PE.sym (wk-id F))
                                 [F] wk[F]
                                 [fst]
      wk[fst′] = irrelevanceTerm′ (PE.sym (wk-id F))
                                 [F] wk[F]
                                 [fst′]

      -- fst t ≡ fst t′ ∷ F
      [fst≡fst′] = transEqTerm [F] [fst≡t] (transEqTerm [F] [t≡t′] (symEqTerm [F] [fst≡t′]))
      wk[fst≡fst′] = irrelevanceEqTerm′ (PE.sym (wk-id F))
                                        [F] wk[F]
                                        [fst≡fst′]

      -- snd (prod t u) ≡ u ∷ G [ fst (prod t u) ]
      wkLiftIdEq = PE.cong (λ x → x [ fst (prod t u ) ]) (wk-lift-id G)
      wk[Gfst] = [G]₁ id ⊢Γ wk[fst]
      [Gfst] = irrelevance′ wkLiftIdEq wk[Gfst]
      [Gfst≡Gt] = irrelevanceEq″ wkLiftIdEq (PE.cong (λ x → x [ t ])
                                                     (wk-lift-id G))
                                 wk[Gfst] [Gfst]
                                 (G-ext id ⊢Γ wk[fst] wk[t] wk[fst≡t])

      [u]fst = convTerm₂ [Gfst] [Gt] [Gfst≡Gt] [u]
      snd⇒u = Σ-β₂ ⊢F ⊢G ⊢t ⊢u
      [snd] , [snd≡u] = redSubstTerm snd⇒u [Gfst] [u]fst

      -- u ≡ u′ ∷ G [ fst (prod t u) ]
      [u≡u′]Gfst = convEqTerm₂ [Gfst] [Gt] [Gfst≡Gt] [u≡u′]

      -- u′ ≡ snd (prod t′ u′) ∷ G [ fst (prod t u) ]
      wkLiftIdEq′ = PE.cong (λ x → x [ fst (prod t′ u′) ]) (wk-lift-id G)
      wk[Gfst′] = [G]₁ id ⊢Γ wk[fst′]
      [Gfst′] = irrelevance′ wkLiftIdEq′ wk[Gfst′]
      [Gfst′≡Gt′] = irrelevanceEq″ wkLiftIdEq′ (PE.cong (λ x → x [ t′ ])
                                                        (wk-lift-id G))
                                   wk[Gfst′] [Gfst′]
                                   (G-ext id ⊢Γ wk[fst′] wk[t′] wk[fst≡t′])

      snd⇒u′ = Σ-β₂ ⊢F ⊢G ⊢t′ ⊢u′

      [u′]Gfst′ = convTerm₂ [Gfst′] [Gt′] [Gfst′≡Gt′] [u′]Gt′
      [snd≡u′]Gfst′ = proj₂ (redSubstTerm snd⇒u′ [Gfst′] [u′]Gfst′)

      [Gfst≡Gfst′] = irrelevanceEq″ wkLiftIdEq wkLiftIdEq′
                                    wk[Gfst] [Gfst]
                                    (G-ext id ⊢Γ wk[fst] wk[fst′] wk[fst≡fst′])

      [snd≡u′]Gfst = convEqTerm₂ [Gfst] [Gfst′] [Gfst≡Gfst′] [snd≡u′]Gfst′

      [snd≡snd′] = transEqTerm [Gfst] [snd≡u]
                               (transEqTerm [Gfst] [u≡u′]Gfst
                                            (symEqTerm [Gfst] [snd≡u′]Gfst))
      wk[snd≡snd′] = irrelevanceEqTerm′ (PE.cong (λ x → x [ fst (prod t u) ])
                                                 (PE.sym (wk-lift-id G)))
                                        [Gfst] wk[Gfst]
                                        [snd≡snd′]

      ⊢prod = escapeTerm (B-intr BΣ [ΣFG]) [prod]
      ⊢prod′ = escapeTerm (B-intr BΣ [ΣFG]) [prod′]
  in Σₜ₌ (prod t u)
         (prod t′ u′)
         (idRedTerm:*: ⊢prod)
         (idRedTerm:*: ⊢prod′)
         prodₙ prodₙ
         (≅-Σ-η ⊢F ⊢G ⊢prod ⊢prod′ prodₙ prodₙ
                (escapeTermEq [F] [fst≡fst′])
                (escapeTermEq [Gfst] [snd≡snd′]))
         [prod] [prod′]
         wk[fst] wk[fst′]
         wk[fst≡fst′]
         wk[snd≡snd′]
prod-cong′ [F] [t] [t′] [t≡t′] [Gt] [u] [u′] [u≡u′] (emb 0<1 x) =
  prod-cong′ [F] [t] [t′] [t≡t′] [Gt] [u] [u′] [u≡u′] x

prod-cong″ : ∀ {F G t t′ u u′ Γ l l′}
             ([F] : Γ ⊩⟨ l ⟩ F)
             ([t] : Γ ⊩⟨ l ⟩ t ∷ F / [F])
             ([t′] : Γ ⊩⟨ l ⟩ t′ ∷ F / [F])
             ([t≡t′] : Γ ⊩⟨ l ⟩ t ≡ t′ ∷ F / [F])
             ([Gt] : Γ ⊩⟨ l ⟩ G [ t ])
             ([u] : Γ ⊩⟨ l ⟩ u ∷ G [ t ] / [Gt])
             ([u′] : Γ ⊩⟨ l ⟩ u′ ∷ G [ t ] / [Gt])
             ([u≡u′] : Γ ⊩⟨ l ⟩ u ≡ u′ ∷ G [ t ] / [Gt])
             ([ΣFG] : Γ ⊩⟨ l′ ⟩ Σ F ▹ G)
             → Γ ⊩⟨ l′ ⟩ prod t u ≡ prod t′ u′ ∷ Σ F ▹ G / [ΣFG]
prod-cong″ [F] [t] [t′] [t≡t′] [Gt] [u] [u′] [u≡u′] [ΣFG] =
  let [prod≡] = prod-cong′ [F] [t] [t′] [t≡t′] [Gt] [u] [u′] [u≡u′] (B-elim BΣ [ΣFG])
  in  irrelevanceEqTerm (B-intr BΣ (B-elim BΣ [ΣFG])) [ΣFG] [prod≡]

prod-congᵛ : ∀ {F G t t′ u u′ Γ l}
             ([Γ] : ⊩ᵛ Γ)
             ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
             ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
             ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
             ([t′] : Γ ⊩ᵛ⟨ l ⟩ t′ ∷ F / [Γ] / [F])
             ([t≡t′] : Γ ⊩ᵛ⟨ l ⟩ t ≡ t′ ∷ F / [Γ] / [F])
             ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ G [ t ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t])
             ([u′] : Γ ⊩ᵛ⟨ l ⟩ u′ ∷ G [ t′ ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t′])
             ([u≡u′] : Γ ⊩ᵛ⟨ l ⟩ u ≡ u′ ∷ G [ t ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t])
             → Γ ⊩ᵛ⟨ l ⟩ prod t u ≡ prod t′ u′ ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G]
prod-congᵛ {F} {G} {t} {t′} {u} {u′} {Γ} [Γ] [F] [G] [t] [t′] [t≡t′] [u] [u′] [u≡u′] {Δ} {σ} ⊢Δ [σ] =
  let ⊩σF = proj₁ ([F] ⊢Δ [σ])
      ⊩σt = proj₁ ([t] ⊢Δ [σ])
      ⊩σt′ = proj₁ ([t′] ⊢Δ [σ])
      σt≡σt′ = [t≡t′] ⊢Δ [σ]

      [Gt] = substS {F} {G} [Γ] [F] [G] [t]
      ⊩σGt₁ = proj₁ ([Gt] ⊢Δ [σ])
      ⊩σGt = irrelevance′ (singleSubstLift G t) ⊩σGt₁

      ⊩σu = irrelevanceTerm′ (singleSubstLift G t)
                             ⊩σGt₁ ⊩σGt
                             (proj₁ ([u] ⊢Δ [σ]))

      [Gt≡Gt′] = substSEq {F = F} {F′ = F} {G = G} {G′ = G} {t = t} {t′ = t′} [Γ]
                          [F] [F] (reflᵛ {A = F} [Γ] [F])
                          [G] [G] (reflᵛ {A = G} {Γ = Γ ∙ F} ([Γ] ∙ [F]) [G])
                          [t] [t′] [t≡t′]
      σGt≡σGt′ = [Gt≡Gt′] ⊢Δ [σ]

      ⊩σGt′ = proj₁ (substS {F} {G} [Γ] [F] [G] [t′] ⊢Δ [σ])
      ⊩σu′₂ = proj₁ ([u′] ⊢Δ [σ])
      ⊩σu′₁ = convTerm₂ ⊩σGt₁ ⊩σGt′ σGt≡σGt′ ⊩σu′₂
      ⊩σu′ = irrelevanceTerm′ (singleSubstLift G t) ⊩σGt₁ ⊩σGt ⊩σu′₁

      σu≡σu′ = irrelevanceEqTerm′ (singleSubstLift G t)
                                  ⊩σGt₁ ⊩σGt
                                  ([u≡u′] ⊢Δ [σ])

      ⊩σΣFG = proj₁ (Σᵛ {F} {G} [Γ] [F] [G] ⊢Δ [σ])
  in prod-cong″ ⊩σF ⊩σt ⊩σt′ σt≡σt′ ⊩σGt ⊩σu ⊩σu′ σu≡σu′ ⊩σΣFG

prodᵛ : ∀ {F G t u Γ l}
       ([Γ] : ⊩ᵛ Γ)
       ([F] : Γ ⊩ᵛ⟨ l ⟩ F / [Γ])
       ([G] : Γ ∙ F ⊩ᵛ⟨ l ⟩ G / [Γ] ∙ [F])
       ([t] : Γ ⊩ᵛ⟨ l ⟩ t ∷ F / [Γ] / [F])
       ([u] : Γ ⊩ᵛ⟨ l ⟩ u ∷ G [ t ] / [Γ] / substS {F} {G} [Γ] [F] [G] [t])
     → Γ ⊩ᵛ⟨ l ⟩ prod t u ∷ Σ F ▹ G / [Γ] / Σᵛ {F} {G} [Γ] [F] [G]
prodᵛ {F} {G} {t} {u} {Γ} {l} [Γ] [F] [G] [t] [u] {Δ = Δ} {σ = σ} ⊢Δ [σ] =
  let [Gt] = substS {F} {G} [Γ] [F] [G] [t]
      [ΣFG] = Σᵛ {F} {G} [Γ] [F] [G]

      ⊩σF = proj₁ ([F] ⊢Δ [σ])
      ⊢σF = escape ⊩σF
      ⊩σt = proj₁ ([t] ⊢Δ [σ])
      ⊩σGt′ : Δ ⊩⟨ l ⟩ subst σ (G [ t ])
      ⊩σGt′ = proj₁ ([Gt] ⊢Δ [σ])
      ⊩σGt : Δ ⊩⟨ l ⟩ subst (liftSubst σ) G [ subst σ t ]
      ⊩σGt = irrelevance′ (singleSubstLift G t) ⊩σGt′
      ⊩σu′ = proj₁ ([u] ⊢Δ [σ])
      ⊩σu : Δ ⊩⟨ l ⟩ subst σ u ∷ subst (liftSubst σ) G [ subst σ t ] / ⊩σGt
      ⊩σu = irrelevanceTerm′ (singleSubstLift G t) ⊩σGt′ ⊩σGt ⊩σu′
      ⊩σΣFG = proj₁ ([ΣFG] ⊢Δ [σ])

  in  prod″ ⊩σF ⊩σt ⊩σGt ⊩σu ⊩σΣFG ,
      (λ {σ′} [σ′] [σ≡σ′] →
        let ⊩σ′F = proj₁ ([F] ⊢Δ [σ′])
            σF≡σ′F = proj₂ ([F] ⊢Δ [σ]) [σ′] [σ≡σ′]

            ⊩σ′t = proj₁ ([t] ⊢Δ [σ′])
            ⊩σ′t = convTerm₂ ⊩σF ⊩σ′F σF≡σ′F ⊩σ′t
            σt≡σ′t = proj₂ ([t] ⊢Δ [σ]) [σ′] [σ≡σ′]

            ⊩σ′Gt′ = proj₁ ([Gt] ⊢Δ [σ′])
            ⊩σ′Gt = irrelevance′ (singleSubstLift G t) ⊩σ′Gt′

            σGt≡σ′Gt = proj₂ ([Gt] ⊢Δ [σ]) [σ′] [σ≡σ′]

            ⊩σ′u″ = proj₁ ([u] ⊢Δ [σ′])
            ⊩σ′u′ = convTerm₂ ⊩σGt′ ⊩σ′Gt′ σGt≡σ′Gt ⊩σ′u″
            ⊩σ′u = irrelevanceTerm′ (singleSubstLift G t) ⊩σGt′ ⊩σGt ⊩σ′u′

            σu≡σ′u : Δ ⊩⟨ l ⟩ subst σ u ≡ subst σ′ u ∷ subst (liftSubst σ) G [ subst σ t ] / ⊩σGt
            σu≡σ′u = irrelevanceEqTerm′ (singleSubstLift G t) ⊩σGt′ ⊩σGt (proj₂ ([u] ⊢Δ [σ]) [σ′] [σ≡σ′])
        in  prod-cong″ ⊩σF ⊩σt ⊩σ′t σt≡σ′t ⊩σGt ⊩σu ⊩σ′u σu≡σ′u ⊩σΣFG)


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

module Issue3517.S where

open import Agda.Builtin.Size public

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Data.Nat using (_+_)
open import Function using (flip)

open import Categories.Category
import Categories.Functor

open import Categories.Bifunctor hiding (identityˡ; identityʳ; assoc) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₀_; _∘₁_; _∘ˡ_; _∘ʳ_; NaturalTransformation) renaming (_≡_ to _≡ⁿ_; id to idⁿ)

module MonoidalHelperFunctors {o ℓ e} (C : Category o ℓ e) (—⊗— : Bifunctor C C C) (id : Category.Obj C) where
  private module C = Category C
  open C hiding (id; identityˡ; identityʳ)

  import Categories.Power.NaturalTransformation
  private module PowNat = Categories.Power.NaturalTransformation C
  open PowNat

  private module ⊗ = Functor —⊗— renaming (F₀ to ⊗₀; F₁ to ⊗₁; F-resp-≡ to ⊗-resp-≡)
  open ⊗

  infix 2 _⊗_
  _⊗_ : ∀ {n m} (F : Powerendo n) (G : Powerendo m) → Powerendo (n + m)
  _⊗_ = reduce —⊗—

  _⊗₂_ : ∀ {m} (F G : Powerendo m) → Powerendo m
  _⊗₂_ = overlaps {C} —⊗— -- reduce (flip-bifunctor {C = C} {C} —⊗—)

  id↑ : Powerendo 0
  id↑ = nullary id

  x : Powerendo 1
  x = unary (idF {C = C})

  id⊗x : Powerendo 1
  id⊗x = id↑ ⊗ x

  x⊗id : Powerendo 1
  x⊗id = x ⊗ id↑

  x⊗y : Powerendo 2
  x⊗y = binary —⊗—

  y⊗x : Powerendo 2
  y⊗x = binary (flip-bifunctor {C = C} {C} —⊗—)

  [x⊗y]⊗z : Powerendo 3
  [x⊗y]⊗z = x⊗y ⊗ x

  x⊗[y⊗z] : Powerendo 3
  x⊗[y⊗z] = x ⊗ x⊗y

  [y⊗z]⊗x : Powerendo 3
  [y⊗z]⊗x = (select 1 ⊗₂ select 2) ⊗₂ select 0

  [y⊗x]⊗z : Powerendo 3
  [y⊗x]⊗z = (select 1 ⊗₂ select 0) ⊗₂ select 2

  y⊗[x⊗z] : Powerendo 3
  y⊗[x⊗z] = select 1 ⊗₂ (select 0 ⊗₂ select 2)

  y⊗[z⊗x] : Powerendo 3
  y⊗[z⊗x] = select 1 ⊗₂ (select 2 ⊗₂ select 0)

  z⊗[x⊗y] : Powerendo 3
  z⊗[x⊗y] = select 2 ⊗₂ (select 0 ⊗₂ select 1)

  x⊗[z⊗y] : Powerendo 3
  x⊗[z⊗y] = select 0 ⊗₂ (select 2 ⊗₂ select 1)

  [x⊗z]⊗y : Powerendo 3
  [x⊗z]⊗y = (select 0 ⊗₂ select 2) ⊗₂ select 1

  [z⊗x]⊗y : Powerendo 3
  [z⊗x]⊗y = (select 2 ⊗₂ select 0) ⊗₂ select 1

  [x⊗id]⊗y : Powerendo 2
  [x⊗id]⊗y = x⊗id ⊗ x

  x⊗[id⊗y] : Powerendo 2
  x⊗[id⊗y] = x ⊗ id⊗x

  [[x⊗y]⊗z]⊗w : Powerendo 4
  [[x⊗y]⊗z]⊗w = [x⊗y]⊗z ⊗ x

  [x⊗y]⊗[z⊗w] : Powerendo 4
  [x⊗y]⊗[z⊗w] = x⊗y ⊗ x⊗y

  x⊗[y⊗[z⊗w]] : Powerendo 4
  x⊗[y⊗[z⊗w]] = x ⊗ x⊗[y⊗z]

  x⊗[[y⊗z]⊗w] : Powerendo 4
  x⊗[[y⊗z]⊗w] = x ⊗ [x⊗y]⊗z

  [x⊗[y⊗z]]⊗w : Powerendo 4
  [x⊗[y⊗z]]⊗w = x⊗[y⊗z] ⊗ x

  infix 2 _⊗ⁿ_
  _⊗ⁿ_ : ∀ {n} {F F′ : Powerendo n} (φ : NaturalTransformation F F′) {m} {G G′ : Powerendo m} (γ : NaturalTransformation G G′) → NaturalTransformation (F ⊗ G) (F′ ⊗ G′)
  _⊗ⁿ_ = reduceN —⊗—

  infix 2 _⊗ⁿ′_
  _⊗ⁿ′_ : ∀ {n} {F F′ : Powerendo n} (φ : NaturalTransformation F F′) {G G′ : Powerendo n} (γ : NaturalTransformation G G′) → NaturalTransformation (F ⊗₂ G) (F′ ⊗₂ G′)
  _⊗ⁿ′_ = overlapN —⊗—

  id₂ : NaturalTransformation x x
  id₂ = idⁿ

  id3 : {F : Powerendo 3} → NaturalTransformation F F
  id3 = idⁿ

  module Coherence (identityˡ : NaturalIsomorphism id⊗x x)
                   (identityʳ : NaturalIsomorphism x⊗id x)
                   (assoc : NaturalIsomorphism [x⊗y]⊗z x⊗[y⊗z]) where
    open NaturalIsomorphism identityˡ using () renaming (F⇒G to υˡ)
    open NaturalIsomorphism identityʳ using () renaming (F⇒G to υʳ)
    open NaturalIsomorphism assoc using () renaming (F⇒G to α)

    α-over : ∀ {n₁ n₂ n₃} (F₁ : Powerendo n₁) (F₂ : Powerendo n₂) (F₃ : Powerendo n₃) → NaturalTransformation ((F₁ ⊗ F₂) ⊗ F₃) (reduce2ʳ —⊗— F₁ F₂ F₃)
    α-over F₁ F₂ F₃ = α ∘ʳ ((hyp F₁ ∥ hyp F₂) ∥ hyp F₃)

    TriangleLeftSide : NaturalTransformation [x⊗id]⊗y x⊗y
    TriangleLeftSide = υʳ ⊗ⁿ id₂

    TriangleTopSide : NaturalTransformation [x⊗id]⊗y x⊗[id⊗y]
    TriangleTopSide = α-over x id↑ x

    TriangleRightSide : NaturalTransformation x⊗[id⊗y] x⊗y
    TriangleRightSide = id₂ ⊗ⁿ υˡ

    PentagonNWSide : NaturalTransformation [[x⊗y]⊗z]⊗w [x⊗y]⊗[z⊗w]
    PentagonNWSide = α-over x⊗y x x

    PentagonNESide : NaturalTransformation [x⊗y]⊗[z⊗w] x⊗[y⊗[z⊗w]]
    PentagonNESide = α-over x x x⊗y

    PentagonSWSide : NaturalTransformation [[x⊗y]⊗z]⊗w [x⊗[y⊗z]]⊗w
    PentagonSWSide = α ⊗ⁿ id₂

    PentagonSSide : NaturalTransformation [x⊗[y⊗z]]⊗w x⊗[[y⊗z]⊗w]
    PentagonSSide = α-over x x⊗y x

    PentagonSESide : NaturalTransformation x⊗[[y⊗z]⊗w] x⊗[y⊗[z⊗w]]
    PentagonSESide = id₂ ⊗ⁿ α

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --prop --allow-unsolved-metas #-}

postulate
  A : Set
  P : A → Prop
  a : A
  c : P a
  Q : Prop

x : Q
x = _ where
  b : A
  b = a

  d : P b
  d = c


text:
module WellScopedTermsModel where

open import Library
open import WellScopedTerms
open import RMonads
open import RMonads.REM
open import Categories.Sets

_<<_ : ∀{n}{X : Set} → (Fin n → X) → X → Fin (suc n) → X
(f << x) zero     = x
(f << x) (suc i) = f i

record LambdaModel : Set₁ where
  field S      : Set
  Env = λ n → Fin n → S
  field eval   : ∀{n} → Env n → Tm n → S
        ap     : S → S → S
        lawvar : ∀{n}{i : Fin n}{γ : Env n} →
                 eval γ (var i) ≅ γ i
        lawapp : ∀{n}{t u : Tm n}{γ : Env n} →
                 eval γ (app t u) ≅ ap (eval γ t) (eval γ u)
        lawlam : ∀{n}{t : Tm (suc n)}{γ : Env n}{s : S} →
                 ap (eval γ (lam t)) s ≅ eval (γ << s) t
        lawext : ∀{f g : S} → ((a : S) → ap f a ≅ ap g a) → f ≅ g

module Model (l : LambdaModel) where
  open LambdaModel l

  wk<< : ∀{m n}(α  : Ren m n)(β : Env n)
            (v : S) → (y : Fin (suc m)) →
            ((β ∘ α) << v) y ≅ (β << v) (wk α y)
  wk<< α β v zero    = refl
  wk<< α β v (suc i) = refl

  reneval : ∀{m n}(α : Ren m n)(β : Env n)
            (t : Tm m) → eval (β ∘ α) t ≅ (eval β ∘ ren α) t
  reneval α β (var i) =
    proof
    eval (β ∘ α) (var i)
    ≅⟨ lawvar ⟩
    β (α i)
    ≅⟨ sym lawvar ⟩
    eval β (var (α i)) ∎
  reneval α β (lam t) = lawext λ a →
    proof
    ap (eval (β ∘ α) (lam t)) a
    ≅⟨ lawlam ⟩
    eval ((β ∘ α) << a) t
    ≅⟨ cong (λ (f : Env _) → eval f t) (ext (wk<< α β a)) ⟩
    eval ((β << a) ∘ wk α) t
    ≅⟨ reneval (wk α) (β << a) t ⟩
    eval (β << a) (ren (wk α) t)
    ≅⟨ sym lawlam ⟩
    ap (eval β (lam (ren (wk α) t))) a
    ∎
  reneval α β (app t u) =
    proof
    eval (β ∘ α) (app t u)
    ≅⟨ lawapp ⟩
    ap (eval (β ∘ α) t) (eval (β ∘ α) u)
    ≅⟨ cong₂ ap (reneval α β t) (reneval α β u) ⟩
    ap (eval β (ren α t)) (eval β (ren α u))
    ≅⟨ sym lawapp ⟩
    eval β (app (ren α t) (ren α u))
    ∎

  lift<< : ∀{m n}(γ  : Sub m n)(α : Env n)
           (a  : S)(i : Fin (suc m)) →
           ((eval α ∘ γ ) << a) i ≅ (eval (α << a) ∘ lift γ) i
  lift<< γ α a zero =
    proof
    a
    ≅⟨ sym lawvar ⟩
    eval (α << a) (var zero)
    ∎
  lift<< γ α a (suc i) =
    proof
    eval α (γ i)
    ≡⟨⟩
    eval ((α << a) ∘ suc) (γ i)
    ≅⟨ reneval suc (α << a) (γ i) ⟩
    eval (α << a) (ren suc (γ i))
    ∎

  subeval : ∀{m n}(t : Tm m)(γ : Sub m n)(α : Env n) →
            eval (eval α ∘ γ) t  ≅ (eval α ∘ sub γ) t
  subeval (var i)   γ α =
    proof
    eval (eval α ∘ γ) (var i)
    ≅⟨ lawvar ⟩
    eval α (γ i)
    ∎
  subeval (lam t)   γ α = lawext λ a →
    proof
    ap (eval (eval α ∘ γ) (lam t)) a
    ≅⟨ lawlam ⟩
    eval ((eval α ∘ γ) << a) t
    ≅⟨ cong (λ (f : Env _) → eval f t) (ext (lift<< γ α a)) ⟩
    eval (eval (α << a) ∘ lift γ) t
    ≅⟨ subeval t (lift γ) (α << a) ⟩
    eval (α << a) (sub (lift γ) t)
    ≅⟨ sym lawlam ⟩
    ap (eval α (lam (sub (lift γ) t))) a
    ∎
  subeval (app t u) γ α =
    proof
    eval (eval α ∘ γ) (app t u)
    ≅⟨ lawapp ⟩
    ap (eval (eval α ∘ γ) t) (eval (eval α ∘ γ) u)
    ≅⟨ cong₂ ap (subeval t γ α) (subeval u γ α) ⟩
    ap (eval α (sub γ t)) (eval α (sub γ u))
    ≅⟨ sym lawapp ⟩
    eval α (app (sub γ t) (sub γ u))
    ∎

  TmRAlg : RAlg TmRMonad
  TmRAlg = record{
    acar  = S;
    astr  = eval;
    alaw1 = ext λ _ → sym lawvar;
    alaw2 =  ext λ t → subeval t _ _}

module VEnv where
  open import Delay
  open import Size

  mutual
    Env : ℕ → Set
    Env n = Fin n → Val

    data Val : Set where
      clo : ∀{n} → Env n → Tm (suc n) → Val

  -- the RAlg is expecting a env containing 'values' here the values
  -- evaluator takes an env of undelayed values and makes a delayed
  -- values.
  mutual
    ev : ∀{i n} → Env n → Tm n → Delay Val i
    ev γ (var x) = now (γ x)
    ev γ (lam t) = now (clo γ t)
    ev γ (app t u) = ev γ t >>= λ f → ev γ u >>= λ v → f $$ v

    _∞$$_ : ∀{i} → Val → Val → ∞Delay Val i
    force (clo γ t ∞$$ v) = ev (γ << v) t

    _$$_ : ∀{i} → Val → Val → Delay Val i
    f $$ v = later (f ∞$$ v)

module FusedVals where
  open import Size
  mutual
    data Env (i : Size) : (n : ℕ) → Set where
      ε   : Env i zero
      _,_ : ∀ {n} (ρ : Env i n) (v : Val i) → Env i (suc n)

    data Val (i : Size) : Set where
      lam   : forall {n} (t : Tm (suc n)) (ρ : Env i n)  → Val i
      later : (v∞ : ∞Val i)                   → Val i

    record ∞Val (i : Size) : Set where
      coinductive
      constructor ∞val
      field
        vforce : {j : Size< i} → Val j

  open ∞Val

  lookup : ∀{i n} -> Env i n -> Fin n -> Val i
  lookup (ρ , v) zero    = v
  lookup (ρ , v) (suc i) = lookup ρ i

  tabulate : ∀{i n} -> (Fin n -> Val i) -> Env i n
  tabulate {n = zero}  f = ε
  tabulate {n = suc n} f = (tabulate {n = n} (f ∘ suc)) , f zero

  mutual
    ev : ∀{i n} -> Env i n -> Tm n -> Val i
    ev ρ (var x)   = lookup ρ x
    ev ρ (lam t)   = lam t ρ
    ev ρ (app t u) = ev ρ t $$ ev ρ u

    _$$_ : ∀{i} → Val i → Val i → Val i
    f $$ v = later (f ∞$$ v)

    _∞$$_ : ∀{i} → Val i → Val i → ∞Val i
    vforce (lam t ρ ∞$$ v) = ev (ρ , v) t
    vforce (later p ∞$$ v) = later (vforce p ∞$$ v)

{-
    FRAlg : ∀ {i} -> RAlg TmRMonad
    FRAlg {i} = ralg
      (Val i)
      (ev ∘ tabulate)
      {!!}
      {!!}
-}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
open import Signature

-- | In this module, we construct the free monad and the free completely
-- iterative monad over a signature Σ (see Aczel, Adamek, Milius and Velebil).
-- The first assigns to a set V of variables the set TV of finite terms over Σ
-- (that is, finite trees labelled with symbols in f ∈ ∥Σ∥ and ar(f) branching).
-- The second extends this to also allow for infinite trees, the set of those
-- is then denoted by T∞(V).
-- Categorically, T(V) is the initial (Σ + V)-algebra, whereas T∞(V) is the
-- final (Σ + V)-coalgebra.
module Terms (Σ : Sig) where

open import Function
open import Data.Empty
open import Data.Unit hiding (_≤_)
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Nat as Nat
open import Data.Sum as Sum
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning
open import Relation.Binary hiding (_⇒_)
open import Relation.Unary hiding (_⇒_)
import Streams as Str
open import Streams hiding (corec)

-- | Natural transformations
Nat : (Set → Set) → (Set → Set) → Set₁
Nat F G = ∀{X} → F X → G X

Id : Set → Set
Id = id

least : {X : Set} (_⊑_ : Rel X _) (P : X → Set) → X → Set
least _⊑_ P x = (P x) × (∀ {y} → P y → x ⊑ y)

least-unique : {X : Set} {_⊑_ : Rel X _} → (IsTotalOrder _≡_ _⊑_) →
               {P : X → Set} → (x y : X) → least _⊑_ P x → least _⊑_ P y → x ≡ y
least-unique isTO x y (p , l₁) (q , l₂) with IsTotalOrder.total isTO x y
least-unique isTO x y (p , l₁) (q , l₂) | inj₁ x⊑y =
  IsTotalOrder.antisym isTO x⊑y (l₂ p)
least-unique isTO x y (p , l₁) (q , l₂) | inj₂ y⊑x =
  IsTotalOrder.antisym isTO (l₁ q) y⊑x

infixr 1 _⇒_
_⇒_ = Nat

data T (V : Set) : Set where
  sup : ⟪ Σ ⟫ (T V) ⊎ V → T V

rec : ∀{V X} → (f : ⟪ Σ ⟫ X ⊎ V → X) → T V → X
rec f (sup (inj₁ (s , α))) = f (inj₁ (s , λ i → rec f (α i)))
rec f (sup (inj₂ y))       = f (inj₂ y)

rec-hom : ∀{V X} → (f : ⟪ Σ ⟫ X ⊎ V → X) (u : ⟪ Σ ⟫ (T V) ⊎ V) →
          rec f (sup u) ≡ f (Sum.map (⟪ Σ ⟫₁ (rec f)) id u)
rec-hom f (inj₁ (s , α)) = cong (λ u → f (inj₁ (s , u))) refl
rec-hom f (inj₂ v) = refl

-- | Functor T, on morphisms
T₁ : ∀ {V W} → (V → W) → T V → T W
T₁ f = rec (sup ∘ Sum.map id f)

η : Id ⇒ T
η = sup ∘ inj₂

μ : T ∘ T ⇒ T
μ {V} = rec f
  where
    f : ⟪ Σ ⟫ (T V) ⊎ T V → T V
    f = [ sup ∘ inj₁ , id ]

-- | First monad law
postulate unitᵣ : ∀{V} {t : T V} → μ (T₁ η t) ≡ t
{-
unitᵣ {V} {t} =
  begin
    μ (T₁ η t)
  ≡⟨ {!!} ⟩
    t
  ∎
-}

-- | T is free over Σ with inclusion
ι : ⟪ Σ ⟫ ⇒ T
ι = sup ∘ inj₁ ∘ ⟪ Σ ⟫₁ η

postulate T₁-top-sym : ∀{V W} (f : V → W) (s : ∥ Σ ∥) (α : ar Σ s → T V) →
             T₁ f (μ (ι (s , α))) ≡ μ (ι (s , T₁ f ∘ α))
-- T₁-top-sym = {!!}

-- | Kleisli morphsims for T∞ V
Subst : Set → Set → Set
Subst V W = V → T W

infixr 9 _•_

-- | Kleisli composition
_•_ : ∀ {U V W} → Subst V W → Subst U V → Subst U W
τ • σ = μ ∘ T₁ τ ∘ σ

-- | Application of substitutions to infinite terms
app : ∀ {V W} → Subst V W → T V → T W
app σ = μ ∘ T₁ σ

infixl 1 _≡ₛ_

_≡ₛ_ : ∀{V W} → Rel (Subst V W) _
σ ≡ₛ τ = ∀ {v} → σ v ≡ τ v

-- | Order on subsitutions
_⊑_ : ∀{V W} → Rel (Subst V W) _
σ₁ ⊑ σ₂ = ∃ λ σ → σ • σ₁ ≡ₛ σ₂

matches : ∀{V W} → T V → T W → Subst V W → Set
matches t s σ = app σ t ≡ s

-- | Most general matcher
mgm : ∀{V W} → T V → T W → Subst V W → Set
mgm t s = least _⊑_ (matches t s)

η-mgm : ∀{V} (t : T V) → mgm t t η
η-mgm {V} t = m , min t
  where
    m : matches t t η
    m =
      begin
        app η t
      ≡⟨ refl ⟩
        μ (T₁ η t)
      ≡⟨ unitᵣ ⟩
        t
      ∎

    min : {σ : Subst V V} (t : T V) → matches t t σ → η ⊑ σ
    min {σ} t m with app σ t
    min {σ} (sup (inj₁ y)) refl | sup (inj₁ .y) = σ , refl
    min (sup (inj₁ x)) () | sup (inj₂ w)
    min (sup (inj₂ v)) () | sup (inj₁ y)
    min {σ} (sup (inj₂ v)) refl | sup (inj₂ .v) = σ , refl

unifies : ∀{V W} → T V → T V → Subst V W → Set
unifies t s σ = app σ t ≡ app σ s

-- | Most general unifier
mgu : ∀{V W} → T V → T V → Subst V W → Set
mgu t s = least _⊑_ (unifies t s)

-- | Free variables
fv : ∀{V} → T V → Pred V _
fv (sup (inj₁ (s , α))) v = ⨿ (Sig.ar Σ s) λ i → (fv (α i) v)
fv (sup (inj₂ v₁))      v = v₁ ≡ v

isCons : ∀{V} → Pred (T V) _
isCons (sup (inj₁ x)) = ⊤
isCons (sup (inj₂ y)) = ⊥

isVar : ∀{V} → Pred (T V) _
isVar (sup (inj₁ x)) = ⊥
isVar (sup (inj₂ y)) = ⊤

record T∞ (V : Set) : Set where
  coinductive
  field out : ⟪ Σ ⟫ (T∞ V) ⊎ V
open T∞ public

sum-lift : {A B : Set} (R₁ : A → A → Set) (R₂ : B → B → Set) (x y : A ⊎ B) → Set
sum-lift R₁ R₂ (inj₁ x) (inj₁ y) = R₁ x y
sum-lift R₁ R₂ (inj₁ x) (inj₂ y) = ⊥
sum-lift R₁ R₂ (inj₂ x) (inj₁ y) = ⊥
sum-lift R₁ R₂ (inj₂ x) (inj₂ y) = R₂ x y

~-data : ∀{V} (R : T∞ V → T∞ V → Set) (u w : ⟪ Σ ⟫ (T∞ V) ⊎ V) → Set
~-data R = sum-lift (sig-lift R) _≡_

record _~_ {V : Set} (t s : T∞ V) : Set where
  coinductive
  field out~ : ~-data _~_ (out t) (out s)
open _~_ public

corec : ∀{V X} → (f : X → ⟪ Σ ⟫ X ⊎ V) → X → T∞ V
out (corec f x) with f x
... | inj₁ (s , α) = inj₁ (s , (λ i → corec f (α i)))
... | inj₂ v       = inj₂ v

prim-corec : ∀{V X} → (f : X → ⟪ Σ ⟫ X ⊎ V ⊎ T∞ V) → X → T∞ V
out (prim-corec {V} {X} f x) with f x
... | inj₁ (s , α)  = inj₁ (s , (λ i → prim-corec f (α i)))
... | inj₂ (inj₁ v) = inj₂ v
... | inj₂ (inj₂ t) = out t

sup∞ : ∀{V} → ⟪ Σ ⟫ (T∞ V) ⊎ V → T∞ V
out (sup∞ (inj₁ u)) = inj₁ u
out (sup∞ (inj₂ v)) = inj₂ v

-- | Functor T∞, on morphisms
T∞₁ : ∀ {V W} → (V → W) → T∞ V → T∞ W
T∞₁ f = corec (Sum.map id f ∘ out)

η∞ : Id ⇒ T∞
η∞ = sup∞ ∘ inj₂

μ∞ : T∞ ∘ T∞ ⇒ T∞
μ∞ {V} = corec f
  where
    g : T∞ V → ⟪ Σ ⟫ (T∞ (T∞ V)) ⊎ V
    g = Sum.map (⟪ Σ ⟫₁ η∞) id ∘ out

    f : T∞ (T∞ V) → ⟪ Σ ⟫ (T∞ (T∞ V)) ⊎ V
    f = [ inj₁ , g ] ∘ out

ι∞ : ⟪ Σ ⟫ ⇒ T∞
ι∞ {V} = g ∘ inj₁
  where
    g : ⟪ Σ ⟫ V ⊎ T∞ V → T∞ V
    g = prim-corec [ inj₁ ∘ ⟪ Σ ⟫₁ (inj₂ ∘ η∞) , inj₂ ∘ inj₂ ]

-- | T is a submonad of T∞
χ : T ⇒ T∞
χ = rec sup∞

-- | Kleisli morphsims for T∞ V
Subst∞ : Set → Set → Set
Subst∞ V W = V → T∞ W

infixl 1 _≡ₛ∞_

_≡ₛ∞_ : ∀{V W} → Rel (Subst∞ V W) _
σ ≡ₛ∞ τ = ∀ {v} → σ v ~ τ v

infixr 9 _•∞_

-- | Kleisli composition
_•∞_ : ∀ {U V W} → Subst∞ V W → Subst∞ U V → Subst∞ U W
τ •∞ σ = μ∞ ∘ T∞₁ τ ∘ σ

-- | Application of substitutions to infinite terms
app∞ : ∀ {V W} → Subst∞ V W → T∞ V → T∞ W
app∞ σ = μ∞ ∘ T∞₁ σ

isVar∞ : ∀{V} → Pred (T∞ V) _
isVar∞ t with out t
isVar∞ t | inj₁ x = ⊥
isVar∞ t | inj₂ v = ⊤

varNowOrLater : ∀{V} → (T∞ V → Pred V _) → T∞ V → Pred V _
varNowOrLater R t v with out t
... | inj₁ (f , α) = ∃ (λ i → R (α i) v)
... | inj₂ v₁      = v ≡ v₁

record fv∞ {V : Set} (t : T∞ V) (v : V) : Set where
  coinductive
  field isFv∞ : varNowOrLater fv∞ t v

root-matches : ∀{V} → T V → ∥ Σ ∥ → Set
root-matches (sup (inj₁ (g , _))) f = g ≡ f
root-matches (sup (inj₂ y))       f = ⊥

record RootsMatch {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) : Set where
  coinductive
  field
    hd-match : root-matches (hd s) f
    tl-match : RootsMatch (tl s) f
open RootsMatch

-- | Nasty hack: assume that RootsMatch is propositional
postulate
  RootsMatch-unique : ∀{V} {s : Stream (T V)} {f : ∥ Σ ∥}
                      (p q : RootsMatch s f) → p ≡ q

split : {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) → RootsMatch s f →
        ar Σ f → Stream (T V)
hd (split s f p i) with hd s | hd-match p
hd (split s f p i) | sup (inj₁ (.f , α)) | refl = α i
hd (split s f p i) | sup (inj₂ y) | ()
tl (split s f p i) = split (tl s) f (tl-match p) i

root-matches∞ : ∀{V} → T∞ V → ∥ Σ ∥ → Set
root-matches∞ t f with out t
root-matches∞ t f | inj₁ (g , _) = f ≡ g
root-matches∞ t f | inj₂ v       = ⊥

split∞ : {V : Set} → (t : T∞ V) (f : ∥ Σ ∥) → root-matches∞ t f →
        ar Σ f → T∞ V
split∞ t f p i with out t
split∞ t f refl i | inj₁ (.f , α) = α i
split∞ t f ()   i | inj₂ y

data AnyRootMatch {V : Set} (s : Stream (T V)) (f : ∥ Σ ∥) : Stream (T V) → Set where
  match-hd : root-matches (hd s) f → AnyRootMatch s f s
  match-tl : AnyRootMatch (tl s) f (tl s) → AnyRootMatch s f (tl s)

first-root-match : ∀{V} → Stream (T V) → ∥ Σ ∥ → ℕ → Set
first-root-match s f = least _≤_ (λ k → root-matches (s at k) f)

conv-branch : {V : Set} (R : Stream (T V) → T∞ V → Set) →
               Stream (T V) → T∞ V → T V → ⟪ Σ ⟫ (T∞ V) ⊎ V → Set
conv-branch R s t (sup (inj₁ (f , α))) (inj₁ (g , β)) =
  ⨿ (f ≡ g) λ p →
  ⨿ (RootsMatch (tl s) f) λ q →
  ∀ i → R (split (tl s) f q i) (β (subst (ar Σ) p i))
conv-branch R s t (sup (inj₁ (f , α))) (inj₂ v) = ⊥
conv-branch R s t (sup (inj₂ v)) (inj₁ (f , α)) =
  ∃ λ s' → AnyRootMatch s f s' × R s' t
conv-branch R s t (sup (inj₂ v)) (inj₂ w) = v ≡ w × R (tl s) t

-- | A sequence s of finite terms converges to a possibly infinite term,
-- if for all i, sᵢ₊₁ = sᵢ[σ] for some substitution σ : V → T V and t = sᵢ[τ]
-- for some τ : V → T∞ V.
-- Note that this coincides with convergence in the prefix metric.
record _→∞_ {V : Set} (s : Stream (T V)) (t : T∞ V) : Set where
  coinductive
  field
    conv-out : conv-branch _→∞_ s t (hd s) (out t)
open _→∞_ public

{-
unique-conv : ∀{V} (s : Stream (T V)) (t₁ t₂ : T∞ V) →
              s →∞ t₁ → s →∞ t₂ → t₁ ~ t₂
-}

ProperlyRefining : ∀{V} → T V → Pred (Subst V V) _
ProperlyRefining t σ = ∀ v → v ∈ fv t → isCons (σ v)

record ProperlyRefiningSeq {V : Set} (t : T V) : Set where
  coinductive
  field
    hd-ref : Subst V V
    hd-is-ref : hd-ref ∈ ProperlyRefining t
    tl-ref : ProperlyRefiningSeq (app hd-ref t)
open ProperlyRefiningSeq public

{-

refining-on-subterms : ∀{V f α} (t : T V) → t ≡ sup (inj₁ (f , α)) →
                       ProperlyRefiningSeq t →
                       (i : ar Σ f) → ProperlyRefiningSeq (α i)
hd-ref    (refining-on-subterms ._ refl p i) = hd-ref p
hd-is-ref (refining-on-subterms ._ refl p i) = {!!}
tl-ref    (refining-on-subterms ._ refl p i) = {!!} -- refining-on-subterms {!!} {!!} {!!} {!!}

-- | A non-trivial substitution is a substitution σ, such that, for all v ∈ V
-- we have that either σ(v) is a non-trivial term or if it is a variable w, then
-- w = v.
-- This allows us to stop substituting the first time we hit a variable.
NonTrivSubst : Set → Set
NonTrivSubst V = ⨿ (Subst V V) λ σ → (∀ v → isVar (σ v) → σ v ≡ η v)

term-seq-from-subst-seq : ∀{V} (t : T V) → ProperlyRefiningSeq t → Stream (T V)
hd (term-seq-from-subst-seq t Δ) = t
tl (term-seq-from-subst-seq t Δ) =
  term-seq-from-subst-seq (app (hd-ref Δ) t) (tl-ref Δ)

var-app-lem : ∀{V} → (σ : Subst V V) → ∀ v → app σ (η v) ≡ σ v
var-app-lem = {!!}

∞term-from-subst-seq : ∀{V} (t : T V) → ProperlyRefiningSeq t → T∞ V
out (∞term-from-subst-seq {V} (sup (inj₁ (f , α))) Δ) = inj₁ (f , β)
  where
    β : ar Σ f → T∞ V
    β i = ∞term-from-subst-seq
          (α i)
          (refining-on-subterms (sup (inj₁ (f , α))) refl Δ i)
out (∞term-from-subst-seq {V} (sup (inj₂ v)) Δ) = {!!}
--  with fv (sup (inj₂ v)) v | hd-ref Δ v | hd-is-ref Δ v refl
  where
    g : ∀{σ} → σ ∈ ProperlyRefining (sup (inj₂ v)) → ⟪ Σ ⟫ (T∞ V)
    g {σ} p with σ v | p v refl
    g p | sup (inj₁ (f , α)) | tt = f , β
      where
        β : ar Σ f → T∞ V
        β i = ∞term-from-subst-seq
              (α i)
              (refining-on-subterms (sup (inj₁ (f , α)))
                                    refl
                                    {!!}
                                    i)
    g p | sup (inj₂ w) | ()

-}

{-

out (∞term-from-subst-seq {V} (sup (inj₂ v)) Δ) | p | sup (inj₁ (f , α)) | tt =
  inj₁ (f , β {!refl!})
  where
    foo : hd-ref Δ v ≡ sup (inj₁ (f , α)) → app (hd-ref Δ) (sup (inj₂ v)) ≡ sup (inj₁ (f , α))
    foo p =
      begin
        app (hd-ref Δ) (sup (inj₂ v))
      ≡⟨ {!!} ⟩
        hd-ref Δ v
      ≡⟨ {!refl!} ⟩
        sup (inj₁ (f , α))
      ∎

    β : hd-ref Δ v ≡ sup (inj₁ (f , α)) → ar Σ f → T∞ V
    β p i = ∞term-from-subst-seq
            (α i)
            (refining-on-subterms (sup (inj₁ (f , α)))
                                  refl
                                  (subst ProperlyRefiningSeq {!!} (tl-ref Δ))
                                  i)
          -- (app (hd-ref Δ) (η v)) (var-app-lem {!!} v)
out (∞term-from-subst-seq (sup (inj₂ v)) Δ) | p | sup (inj₂ y) | ()
-}

{-
∞term-from-subst-seq : ∀{V} → Stream (NonTrivSubst V) → T V → T∞ V
out (∞term-from-subst-seq Δ (sup (inj₁ (s , α)))) =
  inj₁ (s , (λ i → ∞term-from-subst-seq Δ (α i)))
out (∞term-from-subst-seq Δ (sup (inj₂ v))) with proj₁ (hd Δ) v | proj₂ (hd Δ) v
... | sup (inj₁ (s , α)) | f =
  inj₁ (s , (λ i → ∞term-from-subst-seq (tl Δ) (α i)))
... | sup (inj₂ v₁)      | f with f tt
out (∞term-from-subst-seq Δ (sup (inj₂ v))) | sup (inj₂ .v) | f | refl =
  inj₂ v
-}

{-
∞term-from-subst-seq-converges :
  ∀{V} → (Δ : Stream (NonTrivSubst V)) → (t : T V) →
  term-seq-from-subst-seq Δ t →∞ ∞term-from-subst-seq Δ t
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
open import Prelude
open import Data.Maybe using (Maybe; just; nothing)
open import Data.String renaming (_++_ to _++s_)

open import RW.Language.RTerm
open import RW.Language.RTermUtils
open import RW.Language.FinTerm
open import RW.Language.Instantiation

-- Strategy Module.
--
--  Here we'll provide a modular approach to implementing both
--  unification and  abstraction-guessing strategies based
--  on the head of both terms.
module RW.Strategy where

  --   The complexity annotations might require
  --   a slight notational introduction.
  --
  --   If a variable name overlaps one in the corresponding type signature,
  --   this is intentional.
  --
  --   Sₜ is defined by (S t).
  --   #Fvₜ is defined by length (Fv t).
  --   Both measures are defined at RW.Language.RTermUtils.
  --

  open import RW.Utils.Monads using (module Monad)
  open import RW.Utils.Error
  open Monad {{...}}
  open IsError {{...}}

  -------------------------
  -- Error Layer
  -------------------------

  -- Strategy related errors
  data StratErr : Set where
    Nothing       : StratErr
    NoUnification : StratErr
    NoUStrat      : StratErr
    NoTStrat      : RTermName → RTermName → StratErr
    Custom        : String → StratErr

  instance
    IsError-StratErr : IsError StratErr
    IsError-StratErr = record { showError = showErr }
      where
        showErr : StratErr → String
        showErr Nothing        = "Nothing; Internal msg passing flag."
        showErr NoUnification  = "No unification could be performed."
        showErr NoUStrat       = "No suitable unification strategy found."
        showErr (NoTStrat g a) = "No suitable term stragety found.\n"
                              ++s showRTermName g ++s ", " ++s showRTermName a
        showErr (Custom msg)   = "[!] " Data.String.++ msg

  -------------------------
  -- Strategy Pipeline
  --
  --  Whenever we want to perform a rewrite, we'll have a goal and an action to perform on a "subgoal"
  --  This subgoal has to figured out by us, which we denote by g□.
  --  Afterwards, we need to somehow apply our action.

  -- Let's encapsulate everything we need in a record
  record RWData : Set where
    constructor rw-data
    field
      goal   : RBinApp ⊥
      actℕ   : ℕ
      act    : RBinApp (Fin actℕ)
      ctx    : List (RTerm ⊥)

    goal-name : RTermName
    goal-name = p1 goal

    goal-1 : RTerm ⊥
    goal-1 = p1 (p2 goal)
    goal-2 : RTerm ⊥
    goal-2 = p2 (p2 goal)

    act-name : RTermName
    act-name = p1 act

  open RWData

  -- We might need a few transformations here and there.
  data Trs : Set where
    Symmetry : Trs

  -- Unification data
  record UData : Set where
    constructor u-data
    field
      -- We should have an abstraction available,
      □ : RTerm Unit

      -- A substitution
      σ : RSubst

      -- Our action and a few transformations that might need to be applied.
      trs : List Trs

  -------------------------
  -- Unification Strategy Layer
  -------------------------

  private
    μ : ∀{a}{A : Set a} → Maybe (Maybe A) → Maybe A
    μ (just x) = x
    μ nothing  = nothing

  -- Alternatives
  infixr 4 _<|>_
  _<|>_ : ∀{a b}{A : Set a}{B E : Set b} ⦃ isErr : IsError E ⦄
        → (A → Err E B) → (A → Err E B)
        → A → Err E B
  (f <|> g) a with f a
  ...| i1 _ = g a
  ...| i2b  = i2b

  try-all : ∀{a b}{A : Set a}{B E : Set b} ⦃ isErr : IsError E ⦄
          → (A → Err E B) → E → List A → Err E B
  try-all f e [] = i1 e
  try-all f e (a ∷ as) with f a
  ...| i1 _ = try-all f e as
  ...| i2 r = return r

  -- Basic unification strategy
  --
  --  g□ ← g₁ ∩↑ g₂    ∈ O(min(Sg₁, Sg₂))
  --  t1 ← g□ -↓ g₁    ∈ O(# Fv g□)
  --  u1 ← inst ty1 t1 ∈ O(ty1n² + (Sty1 + 1) × ty1n + Sty1)
  --  t2 ← g□ -↓ g₂    ∈ O(# Fv g□)
  --  u2 ← inst ty2 t2 ∈ O(ty2n² + (Sty2 + 1) × ty2n + Sty2)
  --
  --  Summing everything up and symplifying a bit, we get:
  --  (Note that S ty = S t₁ + S t₂ + 1)
  --
  --  min(Sg₁, Sg₂) + 2 #(Fv g□) + t₁² + t₂² + Sty₁ ty₁ + Sty2 ty₂
  --                                                    + t₁ + t₂ + ST - 1
  --
  --  Yet, g□, ideally is our context, with one hole, since
  --  we are doing one rewrite at a time. Therefore #Fv g□ = 1.
  --  Prunning out this constant we get:
  --
  --  min(Sg₁, Sg₂) + t₁² + t₂² + Sty₁ ty₁ + Sty2 ty₂ + t₁ + t₂ + ST
  --
  --  wlog, let us assume that t₁ ≥ t₂ and Sty1 ≥ Sty2.
  --  So,
  --      2t₁² + 2S₁t₁ + 2t₁ + 2S₁
  --         ≥ t₁² + t₂² + Sty₁ ty₁ + Sty2 ty₂ + t₁ + t₂ + ST
  --
  --  Also ignoring min(Sg₁, Sg₂), since it can be seen as a constant,
  --  Our basic unification strategy is somewhere around:
  --
  --  basic ∈ O(2t(t + S + 1) + 2S), for t = max(t₁ , t₂)
  --                                 and S = max(St₁ , St₂)
  --
  --  Which was expected! Our RTermUtils functions are linear in some of
  --  the parameters that appeared here, and instantiation was the
  --  only quadratic one, on the number of free variables to instantiate.
  --
  basic : RWData → Err StratErr UData
  basic (rw-data (hdₓ , g1 , g2) zero (hdₐ , ty1 , ty2) _ )
    = let g□ = g1 ∩↑ g2
      in i2 (u-data (⊥2UnitCast g□) [] [])
  basic (rw-data (hdₓ , g1 , g2) tn (hdₐ , ty1 , ty2)  _ )
    = let g□ = g1 ∩↑ g2
          u1 = (g□ -↓ g1) >>= (inst ty1)
          u2 = (g□ -↓ g2) >>= (inst ty2)
          σ  = μ ((_++ₓ_ <$> u1) <*> u2)
    in maybe (λ s → i2 (u-data (⊥2UnitCast g□) s [])) (i1 NoUnification) (σ >>= X2RSubst)

  -- Unification over the symmetric action type.
  basic-sym : RWData → Err StratErr UData
  basic-sym (rw-data (hdₓ , g1 , g2) tn (hdₐ , ty1 , ty2) _ )
    = let g□ = g1 ∩↑ g2
          u1 = (g□ -↓ g1) >>= (inst ty2)
          u2 = (g□ -↓ g2) >>= (inst ty1)
          σ  = μ ((_++ₓ_ <$> u1) <*> u2)
    in maybe (λ s → i2 (u-data (⊥2UnitCast g□) s (Symmetry ∷ []))) (i1 NoUnification) (σ >>= X2RSubst)

  -- Runs the unification strategies we know about
  -- in the given target terms.
  runUStrats : RWData → Err StratErr UData
  runUStrats = basic <|> basic-sym

  -------------------------
  -- Term Strategy Layer
  -------------------------

  -- The Term Guessing Strategy should be plugged right after
  -- a unification has been succesfuly performed.
  --
  -- Given the head of both our goal and action we
  -- should be able to guess a term that 'bridges' them.
  --
  record TStrat : Set where
    field
      when : RTermName → RTermName → Bool

      how  : Name → UData → Err StratErr (RTerm ⊥)

  -- For now, we'll use a naive list to implement a TStrat
  -- database.
  TStratDB : Set
  TStratDB = List TStrat

  -- Utility to run a list of TStrat's.
  -- Not only returns the resulting term, but also the selected TStrat.
  runTStrats : TStratDB → RWData → Name → UData → Err StratErr (RTerm ⊥)
  runTStrats [] rw = λ _ _ → i1 (NoTStrat (goal-name rw) (act-name rw))
  runTStrats (s ∷ ss) rw with TStrat.when s (goal-name rw) (act-name rw)
  ...| false = runTStrats ss rw
  ...| true  = TStrat.how s

  -- From a name and a substitution create an application.
  makeApp : Name → RSubst → RTerm ⊥
  makeApp act σ = rapp (rdef act) (map p2 σ)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
------------------------------------------------------------------------------
-- Foo module
------------------------------------------------------------------------------

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

module Foo where

postulate foo : Set

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- Sizes for Agda's sized types
------------------------------------------------------------------------

module Size where

postulate
  Size : Set
  ↑_   : Size → Size
  ∞    : Size

{-# BUILTIN SIZE    Size #-}
{-# BUILTIN SIZESUC ↑_   #-}
{-# BUILTIN SIZEINF ∞    #-}

max_issues_repo_name: larrytheliquid/Lemmachine


text:
open import IO

main = run (putStr "Hello, World!")

max_stars_repo_name: Andaraz/hello-world

max_issues_repo_name: Andaraz/hello-world

max_forks_repo_name: Andaraz/hello-world


text:
{-# OPTIONS --safe #-}
module Mod where

open import Data.Fin
open import Data.Nat as ℕ
  using (ℕ; zero; suc; z≤n; s≤s)
open import Relation.Binary.PropositionalEquality
open import Function

private variable k : ℕ

last : Fin (suc k)
last {k = zero} = zero
last {k = suc _} = suc last

negate : Fin k -> Fin k
negate zero = zero
negate (suc zero) = last
negate (suc (suc n)) = inject₁ (negate (suc n))

subt : Fin k -> Fin k -> Fin k
subt n zero = n
subt zero (suc m) = negate (suc m)
subt (suc n) (suc m) with (compare n m)
...| less _ _ = suc (subt n m)
...| _ = inject₁ (subt n m)

add : Fin k -> Fin k -> Fin k
add n m = subt n (negate m)

multAux : ∀{n} → ℕ → (Fin n → Fin n) → Fin n → Fin n
multAux zero _ x = x
multAux (suc n) f x = multAux n f (f x)

mult : Fin k -> Fin k -> Fin k
mult zero m = zero
mult (suc n) m = multAux (toℕ n) (add m) zero

zer : Fin 5
zer = zero
one : Fin 5
one = suc zero
two : Fin 5
two = suc (suc zero)
three : Fin 5
three = suc (suc (suc zero))
four : Fin 5
four = suc (suc (suc (suc zero)))

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
module BasicIS4.Metatheory.Hilbert-BasicKripkeOno where

open import BasicIS4.Syntax.Hilbert public
open import BasicIS4.Semantics.BasicKripkeOno public

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)           γ = lookup i γ
eval (app {A} {B} t u) γ = _⟪$⟫_ {A} {B} (eval t γ) (eval u γ)
eval ci                γ = K I
eval (ck {A} {B})      γ = K (⟪K⟫ {A} {B})
eval (cs {A} {B} {C})  γ = K (⟪S⟫′ {A} {B} {C})
eval (box t)           γ = λ ζ → eval t ∙
eval (cdist {A} {B})   γ = K (_⟪D⟫′_ {A} {B})
eval (cup {A})         γ = K (⟪↑⟫ {A})
eval (cdown {A})       γ = K (⟪↓⟫ {A})
eval (cpair {A} {B})   γ = K (_⟪,⟫′_ {A} {B})
eval cfst              γ = K π₁
eval csnd              γ = K π₂
eval unit              γ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- Andreas, 2017-10-09, issue #2576
-- Duplicate definition should be reported as such,
-- not as "Missing type signature."

data ⊥ : Set where
data ⊥ where

-- Error was: Missing type signature for ⊥

-- Expected error: Duplicate definition

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Number.Prettyprint where

open import Cubical.Data.Sigma.Base
open import Number.Postulates
open import Number.Base

[ℕ]   = Number (isNat     , anyPositivityᵒʳ)
[ℕ⁺⁻] = Number (isNat     , isNonzeroᵒʳ    )
[ℕ₀⁺] = Number (isNat     , isNonnegativeᵒʳ)
[ℕ⁺]  = Number (isNat     , isPositiveᵒʳ   )
[ℕ₀⁻] = Number (isNat     , isNonpositiveᵒʳ)
[ℤ]   = Number (isInt     , anyPositivityᵒʳ)
[ℤ⁺⁻] = Number (isInt     , isNonzeroᵒʳ    )
[ℤ₀⁺] = Number (isInt     , isNonnegativeᵒʳ)
[ℤ⁺]  = Number (isInt     , isPositiveᵒʳ   )
[ℤ⁻]  = Number (isInt     , isNegativeᵒʳ   )
[ℤ₀⁻] = Number (isInt     , isNonpositiveᵒʳ)
[ℚ]   = Number (isRat     , anyPositivityᵒʳ)
[ℚ⁺⁻] = Number (isRat     , isNonzeroᵒʳ    )
[ℚ₀⁺] = Number (isRat     , isNonnegativeᵒʳ)
[ℚ⁺]  = Number (isRat     , isPositiveᵒʳ   )
[ℚ⁻]  = Number (isRat     , isNegativeᵒʳ   )
[ℚ₀⁻] = Number (isRat     , isNonpositiveᵒʳ)
[ℝ]   = Number (isReal    , anyPositivityᵒʳ)
[ℝ⁺⁻] = Number (isReal    , isNonzeroᵒʳ    )
[ℝ₀⁺] = Number (isReal    , isNonnegativeᵒʳ)
[ℝ⁺]  = Number (isReal    , isPositiveᵒʳ   )
[ℝ⁻]  = Number (isReal    , isNegativeᵒʳ   )
[ℝ₀⁻] = Number (isReal    , isNonpositiveᵒʳ)
[ℂ]   = Number (isComplex , anyPositivityᶠ )
[ℂ⁺⁻] = Number (isComplex , isNonzeroᶠ     )

{-# DISPLAY Number (isNat     , anyPositivityᵒʳ) = [ℕ]   #-}
{-# DISPLAY Number (isNat     , isNonzeroᵒʳ    ) = [ℕ⁺⁻] #-}
{-# DISPLAY Number (isNat     , isNonnegativeᵒʳ) = [ℕ₀⁺] #-}
{-# DISPLAY Number (isNat     , isPositiveᵒʳ   ) = [ℕ⁺]  #-}
{-# DISPLAY Number (isNat     , isNonpositiveᵒʳ) = [ℕ₀⁻] #-}
{-# DISPLAY Number (isInt     , anyPositivityᵒʳ) = [ℤ]   #-}
{-# DISPLAY Number (isInt     , isNonzeroᵒʳ    ) = [ℤ⁺⁻] #-}
{-# DISPLAY Number (isInt     , isNonnegativeᵒʳ) = [ℤ₀⁺] #-}
{-# DISPLAY Number (isInt     , isPositiveᵒʳ   ) = [ℤ⁺]  #-}
{-# DISPLAY Number (isInt     , isNegativeᵒʳ   ) = [ℤ⁻]  #-}
{-# DISPLAY Number (isInt     , isNonpositiveᵒʳ) = [ℤ₀⁻] #-}
{-# DISPLAY Number (isRat     , anyPositivityᵒʳ) = [ℚ]   #-}
{-# DISPLAY Number (isRat     , isNonzeroᵒʳ    ) = [ℚ⁺⁻] #-}
{-# DISPLAY Number (isRat     , isNonnegativeᵒʳ) = [ℚ₀⁺] #-}
{-# DISPLAY Number (isRat     , isPositiveᵒʳ   ) = [ℚ⁺]  #-}
{-# DISPLAY Number (isRat     , isNegativeᵒʳ   ) = [ℚ⁻]  #-}
{-# DISPLAY Number (isRat     , isNonpositiveᵒʳ) = [ℚ₀⁻] #-}
{-# DISPLAY Number (isReal    , anyPositivityᵒʳ) = [ℝ]   #-}
{-# DISPLAY Number (isReal    , isNonzeroᵒʳ    ) = [ℝ⁺⁻] #-}
{-# DISPLAY Number (isReal    , isNonnegativeᵒʳ) = [ℝ₀⁺] #-}
{-# DISPLAY Number (isReal    , isPositiveᵒʳ   ) = [ℝ⁺]  #-}
{-# DISPLAY Number (isReal    , isNegativeᵒʳ   ) = [ℝ⁻]  #-}
{-# DISPLAY Number (isReal    , isNonpositiveᵒʳ) = [ℝ₀⁻] #-}
{-# DISPLAY Number (isComplex , anyPositivityᶠ ) = [ℂ]   #-}
{-# DISPLAY Number (isComplex , isNonzeroᶠ     ) = [ℂ⁺⁻] #-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text: module Categories.Functor.Coalgebra where

max_stars_repo_name: copumpkin/categories


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

open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas

module Sets.Cardinality.Finite.Lemmas where

finsetInjectIntoℕ : {n : ℕ} → Injection (toNat {n})
finsetInjectIntoℕ {zero} {()}
finsetInjectIntoℕ {succ n} = ans
  where
    ans : {n : ℕ} → {x y : FinSet (succ n)} → (toNat x ≡ toNat y) → x ≡ y
    ans {zero} {fzero} {fzero} _ = refl
    ans {zero} {fzero} {fsucc ()}
    ans {zero} {fsucc ()} {y}
    ans {succ n} {fzero} {fzero} pr = refl
    ans {succ n} {fzero} {fsucc y} ()
    ans {succ n} {fsucc x} {fzero} ()
    ans {succ n} {fsucc x} {fsucc y} pr with succInjective pr
    ... | pr' = applyEquality fsucc (ans {n} {x} {y} pr')


text:
open import Prelude
open import Data.List.Properties
open import Data.List.Any hiding (map)
open import Data.List.All as All hiding (map; lookup)
open import Data.Vec
open import Extensions.Vec

module Implicits.Resolution.Deterministic.Semantics where

open import Implicits.Syntax
open import Implicits.Resolution.Deterministic.Resolution
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Semantics
open import Implicits.Semantics.Lemmas
open import Extensions.ListFirst

open import SystemF.Everything as F using ()

module DerivationSemantics where

  ⟦_,_⟧r : ∀ {ν n} {K : Ktx ν n} {a} → (proj₂ K) ⊢ᵣ a → K# K →
           ∃ λ t → ⟦ proj₁ K ⟧ctx→ F.⊢ t ∈ ⟦ a ⟧tp→
  ⟦_,_⟧r {K = K} (r-simp {ρ = r} r∈Δ r↓τ) m with ∈⟶index (All.lookup m (proj₁ $ first⟶∈ r∈Δ))
  ⟦_,_⟧r {K = K} (r-simp {ρ = r} r∈Δ r↓τ) m | i , lookup-i≡r =
    ⟦ subst (λ u → _ F.⊢ F.var i ∈ u) eq (F.var i) , r↓τ , m ⟧r↓
    where
      eq = begin
        lookup i ⟦ proj₁ K ⟧ctx→
          ≡⟨ sym $ lookup-⟦⟧ctx→ (proj₁ K) i ⟩
        ⟦ lookup i (proj₁ K) ⟧tp→
            ≡⟨ cong ⟦_⟧tp→ lookup-i≡r ⟩
        ⟦ r ⟧tp→ ∎

      ⟦_,_,_⟧r↓ : ∀ {ν n} {K : Ktx ν n} {a ta τ} →
                ⟦ proj₁ K ⟧ctx→ F.⊢ ta ∈ ⟦ a ⟧tp→ → (proj₂ K) ⊢ a ↓ τ → K# K →
                ∃ λ tτ → ⟦ proj₁ K ⟧ctx→ F.⊢ tτ ∈ ⟦ simpl τ ⟧tp→
      ⟦ ⊢ta , i-simp τ , m ⟧r↓ = , ⊢ta
      ⟦ ⊢ta , i-iabs {ρ₁ = a} ⊢ᵣa b↓τ , m ⟧r↓ =
        , (proj₂ ⟦ ⊢ta F.· (proj₂ ⟦ ⊢ᵣa , m ⟧r) , b↓τ , m ⟧r↓)
      ⟦ ⊢ta , i-tabs {ρ = a} b p , m ⟧r↓ =
        ⟦ subst (λ u → _ F.⊢ _ ∈ u) (sym $ ⟦a/sub⟧tp→ a b) (⊢ta F.[ ⟦ b ⟧tp→ ]) , p , m ⟧r↓

  ⟦ r-iabs a {ρ₂ = b} ⊢b , m ⟧r = , F.λ' ⟦ a ⟧tp→ (proj₂ ⟦ ⊢b , #ivar a m ⟧r)

  ⟦_,_⟧r {K = K} (r-tabs {ρ = r} p) m with ⟦ p , #tvar m ⟧r
  ⟦_,_⟧r {K = K} (r-tabs {ρ = r} p) m | _ , x =
    , F.Λ (subst (λ u → u F.⊢ _ ∈ ⟦ r ⟧tp→) (⟦weaken⟧ctx→ (proj₁ K)) x)

open Semantics _⊢ᵣ_ DerivationSemantics.⟦_,_⟧r public


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Reflexivity {{eqrel : EqRelSet}} where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Reflexivity of reducible types.
reflEq : ∀ {l Γ A} ([A] : Γ ⊩⟨ l ⟩ A) → Γ ⊩⟨ l ⟩ A ≡ A / [A]
reflEq (Uᵣ′ l′ l< ⊢Γ) = PE.refl
reflEq (ℕᵣ D) = red D
reflEq (Emptyᵣ D) = red D
reflEq (Unitᵣ D) = red D
reflEq (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) =
  ne₌ _ [ ⊢A , ⊢B , D ] neK K≡K
reflEq (Bᵣ′ W F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) =
   B₌ _ _ D A≡A
      (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
      (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a]))
reflEq (emb 0<1 [A]) = reflEq [A]

reflNatural-prop : ∀ {Γ n}
                 → Natural-prop Γ n
                 → [Natural]-prop Γ n n
reflNatural-prop (sucᵣ (ℕₜ n d t≡t prop)) =
  sucᵣ (ℕₜ₌ n n d d t≡t
            (reflNatural-prop prop))
reflNatural-prop zeroᵣ = zeroᵣ
reflNatural-prop (ne (neNfₜ neK ⊢k k≡k)) = ne (neNfₜ₌ neK neK k≡k)

reflEmpty-prop : ∀ {Γ n}
                 → Empty-prop Γ n
                 → [Empty]-prop Γ n n
reflEmpty-prop (ne (neNfₜ neK ⊢k k≡k)) = ne (neNfₜ₌ neK neK k≡k)

-- Reflexivity of reducible terms.
reflEqTerm : ∀ {l Γ A t} ([A] : Γ ⊩⟨ l ⟩ A)
           → Γ ⊩⟨ l ⟩ t ∷ A / [A]
           → Γ ⊩⟨ l ⟩ t ≡ t ∷ A / [A]
reflEqTerm (Uᵣ′ ⁰ 0<1 ⊢Γ) (Uₜ A d typeA A≡A [A]) =
  Uₜ₌ A A d d typeA typeA A≡A [A] [A] (reflEq [A])
reflEqTerm (ℕᵣ D) (ℕₜ n [ ⊢t , ⊢u , d ] t≡t prop) =
  ℕₜ₌ n n [ ⊢t , ⊢u , d ] [ ⊢t , ⊢u , d ] t≡t
      (reflNatural-prop prop)
reflEqTerm (Emptyᵣ D) (Emptyₜ n [ ⊢t , ⊢u , d ] t≡t prop) =
  Emptyₜ₌ n n [ ⊢t , ⊢u , d ] [ ⊢t , ⊢u , d ] t≡t
    (reflEmpty-prop prop)
reflEqTerm (Unitᵣ D) (Unitₜ n [ ⊢t , ⊢u , d ] prop) =
  Unitₜ₌ ⊢t ⊢t
reflEqTerm (ne′ K D neK K≡K) (neₜ k d (neNfₜ neK₁ ⊢k k≡k)) =
  neₜ₌ k k d d (neNfₜ₌ neK₁ neK₁ k≡k)
reflEqTerm (Bᵣ′ BΠ F G D ⊢F ⊢G A≡A [F] [G] G-ext) [t]@(Πₜ f d funcF f≡f [f] [f]₁) =
  Πₜ₌ f f d d funcF funcF f≡f [t] [t]
      (λ ρ ⊢Δ [a] → [f] ρ ⊢Δ [a] [a] (reflEqTerm ([F] ρ ⊢Δ) [a]))
reflEqTerm (Bᵣ′ BΣ F G D ⊢F ⊢G A≡A [F] [G] G-ext) [t]@(Σₜ p d pProd p≅p [fst] [snd]) =
  Σₜ₌ p p d d pProd pProd p≅p [t] [t] [fst] [fst]
    (reflEqTerm ([F] id (wf ⊢F)) [fst])
    (reflEqTerm ([G] id (wf ⊢F) [fst]) [snd])
reflEqTerm (emb 0<1 [A]) t = reflEqTerm [A] t


text:
open import Agda.Primitive using (_⊔_)

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian
import SingleSorted.Interpretation as Interpretation

open import SingleSorted.AlgebraicTheory
open import SingleSorted.Substitution
import SingleSorted.Power as Power

module SingleSorted.Model {o ℓ e ℓt}
          {Σ : Signature}
          (T : Theory ℓt Σ)
          {𝒞 : Category.Category o ℓ e}
          (cartesian-𝒞 : Cartesian.Cartesian 𝒞) where

  -- Model of a theory

  record Model (I : Interpretation.Interpretation Σ cartesian-𝒞) : Set (ℓt ⊔ o ⊔ ℓ ⊔ e) where

    open Theory T
    open Category.Category 𝒞
    open Interpretation.Interpretation I
    open HomReasoning

    field
      model-eq : ∀ (ε : ax) → interp-term (ax-lhs ε) ≈ interp-term (ax-rhs ε)

    -- Soundness of semantics
    module _ where
      open Power.Powered interp-pow

      -- first we show that substitution preserves validity
      model-resp-[]s : ∀ {Γ Δ} {u v : Term Γ} {σ : Δ ⇒s Γ} →
                       interp-term u ≈ interp-term v → interp-term (u [ σ ]s) ≈ interp-term (v [ σ ]s)
      model-resp-[]s {u = u} {v = v} {σ = σ} ξ =
        begin
          interp-term (u [ σ ]s) ≈⟨  interp-[]s {t = u} ⟩
          (interp-term u ∘ interp-subst σ)  ≈⟨ ξ ⟩∘⟨refl ⟩
          (interp-term v ∘ interp-subst σ) ≈˘⟨ interp-[]s {t = v} ⟩
          interp-term (v [ σ ]s) ∎

      -- the soundness statement
      model-⊢-≈ : ∀ {Γ} {s t : Term Γ} → Γ ⊢ s ≈ t → interp-term s ≈ interp-term t
      model-⊢-≈ eq-refl =  Equiv.refl
      model-⊢-≈ (eq-symm ξ) = ⟺ (model-⊢-≈ ξ)
      model-⊢-≈ (eq-tran ξ θ) = (model-⊢-≈ ξ) ○ (model-⊢-≈ θ)
      model-⊢-≈ (eq-congr ξ) = ∘-resp-≈ʳ (unique (λ i → project ○ model-⊢-≈ (eq-symm (ξ i))))
      model-⊢-≈ (eq-axiom ε σ) = model-resp-[]s {u = ax-lhs ε} {v = ax-rhs ε} (model-eq ε)

  -- Every theory has the trivial model, whose carrier is the terminal object
  Trivial : Model (Interpretation.Trivial Σ cartesian-𝒞)
  Trivial =
    let open Cartesian.Cartesian cartesian-𝒞 in
    record { model-eq = λ ε → !-unique₂ }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module exampleEquivalenceLambdaNotations2 where

postulate A : Set

g : A -> A
g = \x -> x

g' : A -> A
g' a = a

postulate P : (A -> A) -> Set

f : P g -> P g'
f x = x

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Graph where

open import Cubical.Data.Graph.Base public
open import Cubical.Data.Graph.Examples public
open import Cubical.Data.Graph.Path public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical


text:
module Human.Int where

open import Human.Nat
open import Human.String

infix 8 pos

data Int : Set where
  pos    : (n : Nat) → Int
  negsuc : (n : Nat) → Int

{-# BUILTIN INTEGER       Int    #-}
{-# BUILTIN INTEGERPOS    pos    #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}

primitive primShowInteger : Int → String

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Data.Product.Instance where

open import Class.Equality
open import Class.Monoid
open import Class.Show
open import Data.Product
open import Data.Product.Properties
open import Data.String.Instance
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

instance
  Product-Eq : ∀ {A B} {{_ : Eq A}} {{_ : Eq B}} -> Eq (A × B)
  Product-Eq {A} {B} = record { _≟_ = ≡-dec _≟_ _≟_ }

  Product-Monoid : ∀ {a} {A B : Set a} -> {{_ : Monoid A}} -> {{_ : Monoid B}} -> Monoid (A × B)
  Product-Monoid = record
    { mzero = mzero , mzero
    ; _+_ = λ { (x1 , x2) (y1 , y2) -> (x1 + y1) , (x2 + y2) } }

  Product-Show : ∀ {a} {A B : Set a} {{_ : Show A}} {{_ : Show B}} -> Show (A × B)
  Product-Show = record { show = λ { (a , b) -> "(" + show a + ", " + show b + ")" } }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

module polynomial-rings where

import rings
open rings public

{- We state the universal property of the polynomial ring R[x]. -}

precomp-universal-property-polynomial-Ring :
  {l1 l2 l3 : Level} (R : Ring l1) (S : Ring l2) (T : Ring l3)
  (f : hom-Ring R S) (s : type-Ring S) →
  hom-Ring S T → (hom-Ring R T) × (type-Ring T)
precomp-universal-property-polynomial-Ring R S T f s g =
  pair (comp-hom-Ring R S T g f) (map-hom-Ring S T g s)

universal-property-polynomial-Ring :
  (l : Level) {l1 l2 : Level} (R : Ring l1) (S : Ring l2)
  (f : hom-Ring R S) (s : type-Ring S) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-polynomial-Ring l R S f s =
  (T : Ring l) →
  is-equiv (precomp-universal-property-polynomial-Ring R S T f s)

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Ring.Kernel where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset

open import Cubical.Algebra.Ring.Base
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.Ideal

private
  variable
    ℓ : Level

module _ {{R S : Ring {ℓ}}} (f′ : RingHom R S) where
  open RingHom f′
  open HomTheory f′
  open RingStr ⦃...⦄
  open isIdeal
  open Theory
  private
    instance
      _ = R
      _ = S
      _ = snd R
      _ = snd S

  kernel : ⟨ R ⟩ → hProp ℓ
  kernel x = (f x ≡ 0r) , isSetRing S _ _

  kernelIsIdeal : isIdeal R kernel
  +-closed kernelIsIdeal =
    λ fx≡0 fy≡0 → f (_ + _)  ≡⟨ isHom+ _ _ ⟩
                  f _ + f _  ≡⟨ cong (λ u → u + f _) fx≡0 ⟩
                  0r + f _   ≡⟨ cong (λ u → 0r + u) fy≡0 ⟩
                  0r + 0r    ≡⟨ 0-idempotent S ⟩
                  0r ∎
  -closed kernelIsIdeal =
    λ fx≡0 → f (- _)  ≡⟨ -commutesWithHom _ ⟩
             - f _    ≡⟨ cong -_ fx≡0 ⟩
             - 0r     ≡⟨ 0-selfinverse S ⟩
             0r       ∎
  0r-closed kernelIsIdeal = f 0r ≡⟨ homPres0 ⟩ 0r ∎
  ·-closedLeft kernelIsIdeal = λ r fx≡0 →
    f (r · _)    ≡⟨ isHom· _ _ ⟩
    f r · f (_)  ≡⟨ cong (λ u → f r · u) fx≡0 ⟩
    f r · 0r     ≡⟨ 0-rightNullifies S _ ⟩
    0r ∎
  ·-closedRight kernelIsIdeal = λ r fx≡0 →
    f (_ · r)    ≡⟨ isHom· _ _ ⟩
    f _ · f r     ≡⟨ cong (λ u → u · f r) fx≡0 ⟩
    0r · f r      ≡⟨ 0-leftNullifies S _ ⟩
    0r ∎

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical