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

module Fragment.Extensions.Semigroup where

open import Fragment.Equational.Theory.Bundles

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Homomorphism Σ-magma
open import Fragment.Algebra.Free Σ-magma hiding (_~_)
open import Fragment.Algebra.Algebra Σ-magma
  using (Algebra; IsAlgebra; Interpretation; Congruence; algebra)

open import Fragment.Equational.FreeExtension Θ-semigroup
open import Fragment.Equational.Model Θ-semigroup

open import Fragment.Setoid.Morphism using (_↝_)

open import Level using (Level; _⊔_)

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; #_)
open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive using ([]; _∷_)

import Relation.Binary.Reasoning.Setoid as Reasoning
open import Relation.Binary using (Setoid; IsEquivalence)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

private
  variable
    a ℓ : Level

module _ (A : Model {a} {ℓ}) (n : ℕ) where

  private

    open module A = Setoid ∥ A ∥/≈

    _·_ : ∥ A ∥ → ∥ A ∥ → ∥ A ∥
    x · y = A ⟦ • ⟧ (x ∷ y ∷ [])

    ·-cong : ∀ {x y z w} → x ≈ y → z ≈ w → x · z ≈ y · w
    ·-cong x≈y z≈w = (A ⟦ • ⟧-cong) (x≈y ∷ z≈w ∷ [])

    ·-assoc : ∀ (x y z : ∥ A ∥) → (x · y) · z ≈ x · (y · z)
    ·-assoc x y z = ∥ A ∥ₐ-models assoc (env {A = ∥ A ∥ₐ} (x ∷ y ∷ z ∷ []))

    mutual

      data STree : Set a where
        leaf : ∥ A ∥ → STree
        cons : ∥ A ∥ → DTree → STree

      data DTree : Set a where
        leaf : Fin n → DTree
        cons : Fin n → Tree → DTree

      data Tree : Set a where
        sta : STree → Tree
        dyn : DTree → Tree

    mutual

      infix 6 _≋_ _≋⟨s⟩_ _≋⟨d⟩_

      data _≋⟨s⟩_ : STree → STree → Set (a ⊔ ℓ) where
        leaf : ∀ {x y} → x ≈ y → leaf x ≋⟨s⟩ leaf y
        cons : ∀ {x y xs ys} → x ≈ y → xs ≋⟨d⟩ ys
               → cons x xs ≋⟨s⟩ cons y ys

      data _≋⟨d⟩_ : DTree → DTree → Set (a ⊔ ℓ) where
        leaf : ∀ {x y} → x ≡ y → leaf x ≋⟨d⟩ leaf y
        cons : ∀ {x y xs ys} → x ≡ y → xs ≋ ys
               → cons x xs ≋⟨d⟩ cons y ys

      data _≋_ : Tree → Tree → Set (a ⊔ ℓ) where
        sta : ∀ {x y} → x ≋⟨s⟩ y → sta x ≋ sta y
        dyn : ∀ {x y} → x ≋⟨d⟩ y → dyn x ≋ dyn y

    mutual

      ≋⟨s⟩-refl : ∀ {x} → x ≋⟨s⟩ x
      ≋⟨s⟩-refl {leaf x}    = leaf A.refl
      ≋⟨s⟩-refl {cons x xs} = cons A.refl ≋⟨d⟩-refl

      ≋⟨d⟩-refl : ∀ {x} → x ≋⟨d⟩ x
      ≋⟨d⟩-refl {leaf x}    = leaf PE.refl
      ≋⟨d⟩-refl {cons x xs} = cons PE.refl ≋-refl

      ≋-refl : ∀ {x} → x ≋ x
      ≋-refl {sta x} = sta ≋⟨s⟩-refl
      ≋-refl {dyn x} = dyn ≋⟨d⟩-refl

    mutual

      ≋⟨s⟩-sym : ∀ {x y} → x ≋⟨s⟩ y → y ≋⟨s⟩ x
      ≋⟨s⟩-sym (leaf p)    = leaf (A.sym p)
      ≋⟨s⟩-sym (cons p ps) = cons (A.sym p) (≋⟨d⟩-sym ps)

      ≋⟨d⟩-sym : ∀ {x y} → x ≋⟨d⟩ y → y ≋⟨d⟩ x
      ≋⟨d⟩-sym (leaf p)    = leaf (PE.sym p)
      ≋⟨d⟩-sym (cons p ps) = cons (PE.sym p) (≋-sym ps)

      ≋-sym : ∀ {x y} → x ≋ y → y ≋ x
      ≋-sym (sta p) = sta (≋⟨s⟩-sym p)
      ≋-sym (dyn p) = dyn (≋⟨d⟩-sym p)

    mutual

      ≋⟨s⟩-trans : ∀ {x y z} → x ≋⟨s⟩ y → y ≋⟨s⟩ z → x ≋⟨s⟩ z
      ≋⟨s⟩-trans (leaf p)    (leaf q)    = leaf (A.trans p q)
      ≋⟨s⟩-trans (cons p ps) (cons q qs) = cons (A.trans p q) (≋⟨d⟩-trans ps qs)

      ≋⟨d⟩-trans : ∀ {x y z} → x ≋⟨d⟩ y → y ≋⟨d⟩ z → x ≋⟨d⟩ z
      ≋⟨d⟩-trans (leaf p)    (leaf q)    = leaf (PE.trans p q)
      ≋⟨d⟩-trans (cons p ps) (cons q qs) = cons (PE.trans p q) (≋-trans ps qs)

      ≋-trans : ∀ {x y z} → x ≋ y → y ≋ z → x ≋ z
      ≋-trans (sta p) (sta q) = sta (≋⟨s⟩-trans p q)
      ≋-trans (dyn p) (dyn q) = dyn (≋⟨d⟩-trans p q)

  ≋-isEquivalence : IsEquivalence _≋_
  ≋-isEquivalence = record { refl  = ≋-refl
                           ; sym   = ≋-sym
                           ; trans = ≋-trans
                           }

  Tree/≋ : Setoid _ _
  Tree/≋ = record { Carrier       = Tree
                  ; _≈_           = _≋_
                  ; isEquivalence = ≋-isEquivalence
                  }

  mutual

    _++⟨d⟩_ : DTree → Tree → DTree
    (leaf x)    ++⟨d⟩ y = cons x y
    (cons x xs) ++⟨d⟩ y = cons x (xs ++ y)

    _++_ : Tree → Tree → Tree
    sta (leaf x)    ++ sta (leaf y)    = sta (leaf (x · y))
    sta (leaf x)    ++ sta (cons y ys) = sta (cons (x · y) ys)
    sta (leaf x)    ++ dyn y           = sta (cons x y)
    sta (cons x xs) ++ y               = sta (cons x (xs ++⟨d⟩ y))
    dyn x           ++ y               = dyn (x ++⟨d⟩ y)

  mutual

    ++⟨d⟩-assoc : ∀ x y z → (x ++⟨d⟩ y) ++⟨d⟩ z ≋⟨d⟩ x ++⟨d⟩ (y ++ z)
    ++⟨d⟩-assoc (leaf x)    y z = ≋⟨d⟩-refl
    ++⟨d⟩-assoc (cons x xs) y z = cons PE.refl (++-assoc xs y z)

    ++-assoc : ∀ x y z → (x ++ y) ++ z ≋ x ++ (y ++ z)
    ++-assoc (sta (leaf x))    (sta (leaf y))    (sta (leaf z))    = sta (leaf (·-assoc x y z))
    ++-assoc (sta (leaf x))    (sta (leaf y))    (sta (cons z zs)) = sta (cons (·-assoc x y z) ≋⟨d⟩-refl)
    ++-assoc (sta (leaf x))    (sta (leaf y))    (dyn z)           = ≋-refl
    ++-assoc (sta (leaf x))    (sta (cons y ys)) z                 = ≋-refl
    ++-assoc (sta (leaf x))    (dyn y)           z                 = ≋-refl
    ++-assoc (sta (cons x xs)) y                 z                 = sta (cons A.refl (++⟨d⟩-assoc xs y z))
    ++-assoc (dyn x)           y                 z                 = dyn (++⟨d⟩-assoc x y z)

  mutual

    ++⟨d⟩-cong : ∀ {x y z w} → x ≋⟨d⟩ y → z ≋ w → x ++⟨d⟩ z ≋⟨d⟩ y ++⟨d⟩ w
    ++⟨d⟩-cong (leaf p)    q = cons p q
    ++⟨d⟩-cong (cons p ps) q = cons p (++-cong ps q)

    ++-cong : ∀ {x y z w} → x ≋ y → z ≋ w → x ++ z ≋ y ++ w
    ++-cong (sta (leaf p))    (sta (leaf q))    = sta (leaf (·-cong p q))
    ++-cong (sta (leaf p))    (sta (cons q qs)) = sta (cons (·-cong p q) qs)
    ++-cong (sta (leaf p))    (dyn q)           = sta (cons p q)
    ++-cong (sta (cons p ps)) q                 = sta (cons p (++⟨d⟩-cong ps q))
    ++-cong (dyn p)           q                 = dyn (++⟨d⟩-cong p q)

  Tree⟦_⟧ : Interpretation Tree/≋
  Tree⟦ • ⟧ (x ∷ y ∷ []) = x ++ y

  Tree⟦_⟧-cong : Congruence Tree/≋ Tree⟦_⟧
  Tree⟦ • ⟧-cong (p ∷ q ∷ []) = ++-cong p q

  Tree/≋-isAlgebra : IsAlgebra Tree/≋
  Tree/≋-isAlgebra = record { ⟦_⟧     = Tree⟦_⟧
                            ; ⟦⟧-cong = Tree⟦_⟧-cong
                            }

  Tree/≋-algebra : Algebra
  Tree/≋-algebra = record { ∥_∥/≈           = Tree/≋
                          ; ∥_∥/≈-isAlgebra = Tree/≋-isAlgebra
                          }

  Tree/≋-models : Models Tree/≋-algebra
  Tree/≋-models assoc θ = ++-assoc (θ (# 0)) (θ (# 1)) (θ (# 2))

  Tree/≋-isModel : IsModel Tree/≋
  Tree/≋-isModel = record { isAlgebra = Tree/≋-isAlgebra
                          ; models    = Tree/≋-models
                          }

  Frex : Model
  Frex = record { ∥_∥/≈   = Tree/≋
                ; isModel = Tree/≋-isModel
                }

  ∣inl∣ : ∥ A ∥ → ∥ Frex ∥
  ∣inl∣ x = sta (leaf x)

  ∣inl∣-cong : Congruent _≈_ _≋_ ∣inl∣
  ∣inl∣-cong p = sta (leaf p)

  ∣inl∣⃗ : ∥ A ∥/≈ ↝ ∥ Frex ∥/≈
  ∣inl∣⃗ = record { ∣_∣      = ∣inl∣
                  ; ∣_∣-cong = ∣inl∣-cong
                  }

  ∣inl∣-hom : Homomorphic ∥ A ∥ₐ ∥ Frex ∥ₐ ∣inl∣
  ∣inl∣-hom • (x ∷ y ∷ []) = ≋-refl

  inl : ∥ A ∥ₐ ⟿ ∥ Frex ∥ₐ
  inl = record { ∣_∣⃗    = ∣inl∣⃗
               ; ∣_∣-hom = ∣inl∣-hom
               }

  inr : ∥ J n ∥ₐ ⟿ ∥ Frex ∥ₐ
  inr = interp Frex (λ k → dyn (leaf k))

  module _ {b ℓ} (X : Model {b} {ℓ}) where

    private

      open module X = Setoid ∥ X ∥/≈ renaming (_≈_ to _~_)

      _⊕_ : ∥ X ∥ → ∥ X ∥ → ∥ X ∥
      x ⊕ y = X ⟦ • ⟧ (x ∷ y ∷ [])

      ⊕-cong : ∀ {x y z w} → x ~ y → z ~ w → x ⊕ z ~ y ⊕ w
      ⊕-cong p q = (X ⟦ • ⟧-cong) (p ∷ q ∷ [])

      ⊕-assoc : ∀ (x y z : ∥ X ∥) → (x ⊕ y) ⊕ z ~ x ⊕ (y ⊕ z)
      ⊕-assoc x y z = ∥ X ∥ₐ-models assoc (env {A = ∥ X ∥ₐ} (x ∷ y ∷ z ∷ []))

    module _
      (f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ)
      (g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ)
      where

      ∣resid∣ : ∥ Frex ∥ → ∥ X ∥
      ∣resid∣ (sta (leaf x))    = ∣ f ∣ x
      ∣resid∣ (sta (cons x xs)) = ∣ f ∣ x ⊕ ∣resid∣ (dyn xs)
      ∣resid∣ (dyn (leaf x))    = ∣ g ∣ (atom (dyn x))
      ∣resid∣ (dyn (cons x xs)) = ∣ g ∣ (atom (dyn x)) ⊕ ∣resid∣ xs

      ∣resid∣-cong : Congruent _≋_ _~_ ∣resid∣
      ∣resid∣-cong (sta (leaf p))    = ∣ f ∣-cong p
      ∣resid∣-cong (sta (cons p ps)) = ⊕-cong (∣ f ∣-cong p) (∣resid∣-cong (dyn ps))
      ∣resid∣-cong (dyn (leaf p))    = ∣ g ∣-cong (inherit (atom (dyn p)))
      ∣resid∣-cong (dyn (cons p ps)) =
        ⊕-cong (∣ g ∣-cong (inherit (atom (dyn p)))) (∣resid∣-cong ps)

      open Reasoning ∥ X ∥/≈

      ∣resid∣-hom : Homomorphic ∥ Frex ∥ₐ ∥ X ∥ₐ ∣resid∣
      ∣resid∣-hom • (sta (leaf x) ∷ sta (leaf y) ∷ [])    = ∣ f ∣-hom • (x ∷ y ∷ [])
      ∣resid∣-hom • (sta (leaf x) ∷ sta (cons y ys) ∷ []) = begin
          ∣ f ∣ x ⊕ (∣ f ∣ y ⊕ ∣resid∣ (dyn ys))
        ≈⟨ X.sym (⊕-assoc (∣ f ∣ x) (∣ f ∣ y) _) ⟩
          (∣ f ∣ x ⊕ ∣ f ∣ y) ⊕ ∣resid∣ (dyn ys)
        ≈⟨ ⊕-cong (∣ f ∣-hom • (x ∷ y ∷ [])) X.refl ⟩
          ∣ f ∣ (x · y) ⊕ ∣resid∣ (dyn ys)
        ∎
      ∣resid∣-hom • (sta (leaf x) ∷ dyn y ∷ [])           = X.refl
      ∣resid∣-hom • (sta (cons x xs) ∷ y ∷ [])            = begin
          (∣ f ∣ x ⊕ ∣resid∣ (dyn xs)) ⊕ ∣resid∣ y
        ≈⟨ ⊕-assoc (∣ f ∣ x) _ (∣resid∣ y) ⟩
          ∣ f ∣ x ⊕ (∣resid∣ (dyn xs) ⊕ ∣resid∣ y)
        ≈⟨ ⊕-cong X.refl (∣resid∣-hom • (dyn xs ∷ y ∷ [])) ⟩
          ∣ f ∣ x ⊕ ∣resid∣ (dyn xs ++ y)
        ∎
      ∣resid∣-hom • (dyn (leaf x) ∷ y ∷ [])               = X.refl
      ∣resid∣-hom • (dyn (cons x xs) ∷ y ∷ [])            = begin
          (∣ g ∣ (atom (dyn x)) ⊕ ∣resid∣ xs) ⊕ ∣resid∣ y
        ≈⟨ ⊕-assoc _ (∣resid∣ xs) (∣resid∣ y) ⟩
          ∣ g ∣ (atom (dyn x)) ⊕ (∣resid∣ xs ⊕ ∣resid∣ y)
        ≈⟨ ⊕-cong X.refl (∣resid∣-hom • (xs ∷ y ∷ [])) ⟩
          ∣ g ∣ (atom (dyn x)) ⊕ ∣resid∣ (xs ++ y)
        ∎

      ∣resid∣⃗ : ∥ Frex ∥/≈ ↝ ∥ X ∥/≈
      ∣resid∣⃗ = record { ∣_∣      = ∣resid∣
                        ; ∣_∣-cong = ∣resid∣-cong
                        }

      _[_,_] : ∥ Frex ∥ₐ ⟿ ∥ X ∥ₐ
      _[_,_] = record { ∣_∣⃗    = ∣resid∣⃗
                      ; ∣_∣-hom = ∣resid∣-hom
                      }

  module _ {b ℓ} {X : Model {b} {ℓ}} where

    private

      open module X = Setoid ∥ X ∥/≈ renaming (_≈_ to _~_)

      _⊕_ : ∥ X ∥ → ∥ X ∥ → ∥ X ∥
      x ⊕ y = X ⟦ • ⟧ (x ∷ y ∷ [])

      ⊕-cong : ∀ {x y z w} → x ~ y → z ~ w → x ⊕ z ~ y ⊕ w
      ⊕-cong p q = (X ⟦ • ⟧-cong) (p ∷ q ∷ [])

      ⊕-assoc : ∀ (x y z : ∥ X ∥) → (x ⊕ y) ⊕ z ~ x ⊕ (y ⊕ z)
      ⊕-assoc x y z = ∥ X ∥ₐ-models assoc (env {A = ∥ X ∥ₐ} (x ∷ y ∷ z ∷ []))

    module _
      {f : ∥ A ∥ₐ ⟿ ∥ X ∥ₐ}
      {g : ∥ J n ∥ₐ ⟿ ∥ X ∥ₐ}
      where

      commute₁ : X [ f , g ] ⊙ inl ≗ f
      commute₁ = X.refl

      open Reasoning ∥ X ∥/≈

      commute₂ : X [ f , g ] ⊙ inr ≗ g
      commute₂ {atom (dyn k)} =
        ∣ X [ f , g ] ∣-cong (≋-refl {x = dyn (leaf k)})
      commute₂ {t@(term • (x ∷ y ∷ []))} = begin
          ∣ X [ f , g ] ∣ (∣ inr ∣ t)
        ≈⟨ ∣ X [ f , g ] ∣-cong (∣ inr ∣-hom • (x ∷ y ∷ [])) ⟩
          ∣ X [ f , g ] ∣ (∣ inr ∣ x ++ ∣ inr ∣ y)
        ≈⟨ X.sym (∣ X [ f , g ] ∣-hom • (∣ inr ∣ x ∷ ∣ inr ∣ y ∷ [])) ⟩
          ∣ X [ f , g ] ∣ (∣ inr ∣ x) ⊕ ∣ X [ f , g ] ∣ (∣ inr ∣ y)
        ≈⟨ ⊕-cong commute₂ commute₂ ⟩
          ∣ g ∣ x ⊕ ∣ g ∣ y
        ≈⟨ ∣ g ∣-hom • (x ∷ y ∷ []) ⟩
          ∣ g ∣ t
        ∎

      module _ {h : ∥ Frex ∥ₐ ⟿ ∥ X ∥ₐ}
        (c₁ : h ⊙ inl ≗ f)
        (c₂ : h ⊙ inr ≗ g)
        where

        universal : X [ f , g ] ≗ h
        universal {sta (leaf x)}    = X.sym c₁
        universal {dyn (leaf x)}    = X.sym c₂
        universal {sta (cons x xs)} = begin
            ∣ f ∣ x ⊕ ∣ X [ f , g ] ∣ (dyn xs)
          ≈⟨ ⊕-cong (X.sym c₁) universal ⟩
            ∣ h ∣ (sta (leaf x)) ⊕ ∣ h ∣ (dyn xs)
          ≈⟨ ∣ h ∣-hom • (sta (leaf x) ∷ dyn xs ∷ []) ⟩
            ∣ h ∣ (sta (leaf x) ++ dyn xs)
          ∎
        universal {dyn (cons x xs)} = begin
            ∣ g ∣ (atom (dyn x)) ⊕ ∣ X [ f , g ] ∣ xs
          ≈⟨ ⊕-cong (X.sym c₂) universal ⟩
            ∣ h ∣ (dyn (leaf x)) ⊕ ∣ h ∣ xs
          ≈⟨ ∣ h ∣-hom • (dyn (leaf x) ∷ xs ∷ []) ⟩
            ∣ h ∣ (dyn (leaf x) ++ xs)
          ∎

SemigroupFrex : FreeExtension
SemigroupFrex = record { _[_]        = Frex
                       ; _[_]-isFrex = isFrex
                       }
  where isFrex : IsFreeExtension Frex
        isFrex A n =
          record { inl       = inl A n
                 ; inr       = inr A n
                 ; _[_,_]    = _[_,_] A n
                 ; commute₁  = λ {_ _ X f g} → commute₁ A n {X = X} {f} {g}
                 ; commute₂  = λ {_ _ X f g} → commute₂ A n {X = X} {f} {g}
                 ; universal = λ {_ _ X f g h} → universal A n {X = X} {f} {g} {h}
                 }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module _ where

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

module Vars (A : Set) where
  variable
    x : A

-- Was
--   Panic: Unbound name: Issue3121._.x [0,10,12]@8066984681118411118
--   when checking that the expression
--   {A : Set} (let open Vars A) → ;Issue3121.x ≡ ;Issue3121.x has type _2
-- Should be
--   scope error on x
r : {A : Set} (let open Vars A) → x ≡ x
r = refl

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Virtual machine instructions, state etc.
------------------------------------------------------------------------

open import Prelude

module Lambda.Virtual-machine.Instructions (Name : Type) where

open import Equality.Propositional

open import Lambda.Syntax Name

------------------------------------------------------------------------
-- Instruction set

mutual

  -- Instructions.

  data Instr (n : ℕ) : Type where
    var     : Fin n → Instr n
    clo     : Code (suc n) → Instr n
    app ret : Instr n
    cal tcl : Name → Instr n  -- Calls and tail calls.
    con     : Bool → Instr n
    bra     : Code n → Code n → Instr n

  -- Code.

  Code : ℕ → Type
  Code n = List (Instr n)

-- Environments and values.

open Closure Code

------------------------------------------------------------------------
-- Stacks and states

-- Stacks.

data Stack-element : Type where
  val : Value → Stack-element
  ret : ∀ {n} → Code n → Env n → Stack-element

Stack : Type
Stack = List Stack-element

-- States.

data State : Type where
  ⟨_,_,_⟩ : ∀ {n} → Code n → Stack → Env n → State

------------------------------------------------------------------------
-- Results

-- The result of running the VM one step.

data Result : Type where
  continue : State → Result
  done     : Value → Result
  crash    : Result

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


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

module Categories.Adjoint.Equivalence.Properties where

open import Level

open import Categories.Category
open import Categories.Adjoint.Equivalence
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism as ≃ using (_≃_; NaturalIsomorphism)

import Categories.Morphism.Reasoning as MR
import Categories.Category.Construction.Cones as Co
import Categories.Diagram.Limit as Lim

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

-- diagrams are preserved by adjoint equivalence
--
-- if categories C and D are adjoint equivalent, then a limit from one determines one from another
module _  (⊣equiv : ⊣Equivalence C D) (F : Functor C E) where
  private
    module LF where
      open Co F public
      open Lim F public
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module ⊣equiv = ⊣Equivalence ⊣equiv
    open ⊣equiv
    open E
    open MR E
    open HomReasoning
    open LF

    FR = F ∘F R

    module LFR where
      open Co FR public
      open Lim FR public

  module _ (Lm : Limit) where
    private
      module Lm = Lim.Limit Lm
      open Lm

      ⊤cone : LFR.Cone
      ⊤cone = record
        { N    = Lm.apex
        ; apex = record
          { ψ       = λ d → proj (R.₀ d)
          ; commute = λ f → limit-commute (R.₁ f)
          }
        }

      module _ {K : LFR.Cone} where
        private
          module K = LFR.Cone K

        K′ : Cone
        K′ = record
          { N    = K.N
          ; apex = record
            { ψ       = λ c → F.₁ (unit.⇐.η c) ∘ K.ψ (L.₀ c)
            ; commute = λ {X} {Y} f → begin
              F.₁ f ∘ F.₁ (unit.⇐.η X) ∘ K.ψ (L.₀ X)                         ≈˘⟨ pushˡ ([ F ]-resp-square (unit.⇐.commute f)) ⟩
              (F.₁ (unit.⇐.η Y) ∘ F.₁ (Functor.F₁ (R ∘F L) f)) ∘ K.ψ (L.₀ X) ≈⟨ pullʳ (K.commute (L.₁ f)) ⟩
              F.₁ (unit.⇐.η Y) ∘ K.ψ (L.₀ Y)                                 ∎
            }
          }

        !cone : LFR.Cones [ K , ⊤cone ]
        !cone = record
          { arr     = rep K′
          ; commute = λ {d} → begin
            proj (R.₀ d) ∘ rep K′                          ≈⟨ commute ⟩
            F.₁ (unit.⇐.η (R.₀ d)) ∘ K.ψ (L.₀ (R.₀ d))     ≈˘⟨ F.F-resp-≈ (MR.flip-fromʳ C unit.FX≅GX zag) ⟩∘⟨refl ⟩
            (F.₁ (R.₁ (counit.⇒.η d)) ∘ K.ψ (L.₀ (R.₀ d))) ≈⟨ K.commute (counit.⇒.η d) ⟩
            K.ψ d                                          ∎
          }

      module _ {K : LFR.Cone} (f : LFR.Cones [ K , ⊤cone ]) where
        private
          module K = LFR.Cone K
          module f = LFR.Cone⇒ f

        !cone-unique : LFR.Cones [ !cone ≈ f ]
        !cone-unique = begin
          rep (K′ {K}) ≈⟨ terminal.!-unique {K′ {K}} (record { arr = f.arr ; commute = eq }) ⟩
          f.arr        ∎
          where eq : ∀ {c} → proj c ∘ f.arr ≈ F.₁ (unit.⇐.η c) ∘ K.ψ (L.₀ c)
                eq {c} = begin
                  proj c ∘ f.arr                                ≈˘⟨ pullˡ (limit-commute (unit.⇐.η c)) ⟩
                  F.₁ (unit.⇐.η c) ∘ proj (R.₀ (L.₀ c)) ∘ f.arr ≈⟨ refl⟩∘⟨ f.commute ⟩
                  F.₁ (unit.⇐.η c) ∘ K.ψ (L.₀ c)                ∎

    ⊣equiv-preserves-diagram : Lim.Limit FR
    ⊣equiv-preserves-diagram = record
      { terminal = record
        { ⊤        = ⊤cone
        ; !        = !cone
        ; !-unique = !cone-unique
        }
      }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-
   Copyright (c) 2017 Diego Pedraza.

   This is Free/Libre Open Source Software, released under the MIT License.
   For the full copyright and license information, please view the LICENSE
   file that was distributed with this source code.
 -}

module R1 where

open import Data.List using (List; _∷_; _++_; [_]; [])
open import Data.Nat
open import Data.Bool

record Pair (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

{- ----------------------------------------------------------------
  Ejercicio 1. Definir, por recursión, la función
     longitud :: 'a list ⇒ nat
  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
     longitud [a,b,c] = 3
  ----------------------------------------------------------------- -}

longitud : ∀ {A : Set} → List A → ℕ
longitud [] = 0
longitud (x ∷ xs) = 1 + longitud xs

{- ---------------------------------------------------------------
  Ejercicio 2. Definir la función
     fun intercambia :: 'a × 'b ⇒ 'b × 'a
  tal que (intercambia p) es el par obtenido intercambiando las
  componentes del par p. Por ejemplo,
     intercambia (u,v) = (v,u)
  ---------------------------------------------------------------- -}

intercambia : ∀ {A} {B : Set} → Pair A B → Pair B A
intercambia (a , b) = (b , a)

{- ---------------------------------------------------------------
  Ejercicio 3. Definir, por recursión, la función
     inversa :: 'a list ⇒ 'a list
  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
  elementos de xs. Por ejemplo,
     inversa [a,d,c] = [c,d,a]
  ---------------------------------------------------------------- -}

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

{- ---------------------------------------------------------------
  Ejercicio 4. Definir la función
     repite :: nat ⇒ 'a ⇒ 'a list
  tal que (repite n x) es la lista formada por n copias del elemento
  x. Por ejemplo,
     repite 3 a = [a,a,a]
  ---------------------------------------------------------------- -}

repite : ∀ {A : Set} → ℕ → A → List A
repite 0 x = []
repite (suc n) x = x ∷ repite n x

{- ---------------------------------------------------------------
  Ejercicio 5. Definir la función
     conc :: 'a list ⇒ 'a list ⇒ 'a list
  tal que (conc xs ys) es la concatención de las listas xs e ys. Por
  ejemplo,
     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
  ---------------------------------------------------------------- -}

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

{- ---------------------------------------------------------------
  Ejercicio 6. Definir la función
     coge :: nat ⇒ 'a list ⇒ 'a list
  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
  ejemplo,
     coge 2 [a,c,d,b,e] = [a,c]
  ---------------------------------------------------------------- -}

coge : ∀ {A : Set} -> ℕ → List A → List A
coge 0 xs = []
coge n [] = []
coge (suc n) (x ∷ xs) = x ∷ coge n xs

{- ---------------------------------------------------------------
  Ejercicio 7. Definir la función
     elimina :: nat ⇒ 'a list ⇒ 'a list
  tal que (elimina n xs) es la lista obtenida eliminando los n primeros
  elementos de xs. Por ejemplo,
     elimina 2 [a,c,d,b,e] = [d,b,e]
  ---------------------------------------------------------------- -}

elimina : ∀ {A : Set} → ℕ → List A → List A
elimina 0 xs = xs
elimina n [] = []
elimina (suc n) (x ∷ xs) = elimina n xs

{- ---------------------------------------------------------------
  Ejercicio 8. Definir la función
     esVacia :: 'a list ⇒ bool
  tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
     esVacia [a] = False
  ---------------------------------------------------------------- -}

esVacia : ∀ {A : Set} → List A → Bool
esVacia [] = true
esVacia (x ∷ xs) = false

{- ---------------------------------------------------------------
  Ejercicio 9. Definir la función
     inversaAc :: 'a list ⇒ 'a list
  tal que (inversaAc xs) es a inversa de xs calculada usando
  acumuladores. Por ejemplo,
     inversaAc [a,c,b,e] = [e,b,c,a]
  ---------------------------------------------------------------- -}

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

inversaAc : ∀ {A : Set} → List A → List A
inversaAc xs = inversaAcAux xs []

{- ---------------------------------------------------------------
  Ejercicio 10. Definir la función
     sum :: nat list ⇒ nat
  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
     sum [3,2,5] = 10
  ---------------------------------------------------------------- -}

sum  : List ℕ → ℕ
sum [] = 0
sum (x ∷ xs) = x + sum xs

{- ---------------------------------------------------------------
  Ejercicio 11. Definir la función
     map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
  tal que (map f xs) es la lista obtenida aplicando la función f a los
  elementos de xs. Por ejemplo,
     map (λx. 2*x) [3,2,5] = [6,4,10]
  ---------------------------------------------------------------- -}

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

max_stars_repo_name: Zegeri/TFG-TeoriaCategorias

max_issues_repo_name: Zegeri/TFG-TeoriaCategorias

max_forks_repo_name: Zegeri/TFG-TeoriaCategorias


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

module Copatterns where

record Stream (A : Set) : Set where
  field
    head : A
    tail : Stream A
open Stream

repeat : {A : Set}(a : A) -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

map : {A B : Set}(f : A -> B)(as : Stream A) -> Stream B
head (map f as) = f (head as)
tail (map f as) = map f (tail as)

iterate : {A : Set}(f : A -> A)(a : A) -> Stream A
head (iterate f a) = a
tail (iterate f a) = iterate f (f a)

scanl : {A B : Set} -> (B -> A -> B) -> B -> Stream A -> Stream B
head (scanl f b as) = b
tail (scanl f b as) = scanl f (f b (head as)) (tail as)

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

nats : Stream Nat
nats = iterate suc zero

alternate : Stream Nat
(      head alternate ) = zero
(head (tail alternate)) = suc zero
(tail (tail alternate)) = alternate

record _×_ (A B : Set) : Set where
  field
    fst : A
    snd : B
open _×_

build : {A S : Set} → (S → A × S) -> S -> Stream A
head (build step s) = fst (step s)
tail (build step s) = build step (snd (step s))
-- build step s = mapSnd (build step) (step s)

build1 : {A S : Set} → (S → A × S) -> S -> Stream A
build1 step s = record
  { head = fst (step s)
  ; tail = build1 step (snd (step s))
  }

build2 : {A S : Set} → (S → A × S) -> S -> Stream A
build2 step s = record
  { head = fst p
  ; tail = build2 step (snd p)
  }
  where p = step s

mapSnd : {A B C : Set}(f : B → C) → A × B → A × C
fst (mapSnd f p) = fst p
snd (mapSnd f p) = f (snd p)

record Str (A : Set) : Set where
  field
    out : A × Str A
open Str

build' : {A S : Set} → (S → A × S) -> S -> Stream A
out (build' step s) = mapSnd (build' step) (step s)

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Numeral.Integer.Sign where

open import Numeral.Natural
  using (ℕ)
open import Numeral.Integer
open import Numeral.Sign as Sign
  using (+|− ; +|0|−)

sign : ℤ → (+|−)
sign(+ₙ _) = Sign.➕
sign(−𝐒ₙ _) = Sign.➖

sign0 : ℤ → (+|0|−)
sign0(𝟎) = Sign.𝟎
sign0(+𝐒ₙ _) = Sign.➕
sign0(−𝐒ₙ _) = Sign.➖

signum0 : ℤ → ℤ
signum0(𝟎) = 𝟎
signum0(+𝐒ₙ _) = +𝐒ₙ(ℕ.𝟎)
signum0(−𝐒ₙ _) = −𝐒ₙ(ℕ.𝟎)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- And
------------------------------------------------------------------------

module TotalParserCombinators.And where

open import Category.Monad
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.Membership.Propositional.Properties
import Data.List.Categorical
open import Data.Product
open import Data.Product.Function.NonDependent.Propositional
open import Function.Base
open import Function.Inverse using (_↔_)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Level

open RawMonadPlus {f = zero} Data.List.Categorical.monadPlus
  using (_⊗_)
open Related using (SK-sym)

open import TotalParserCombinators.Congruence using (_∼[_]P_; _≅P_)
open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Parser
import TotalParserCombinators.Pointwise as Pointwise
open import TotalParserCombinators.Semantics using (_∈_·_)

-- _&_ is defined as a pointwise lifting of _⊗_.

private
  module And {R₁ R₂ : Set} = Pointwise R₁ R₂ id _⊗_ ⊗-cong

-- p₁ & p₂ returns a result if both p₁ and p₂ do.

infixr 6 _&_ _&-cong_

_&_ : ∀ {Tok R₁ R₂ xs₁ xs₂} →
      Parser Tok R₁ xs₁ → Parser Tok R₂ xs₂ →
      Parser Tok (R₁ × R₂) (xs₁ ⊗ xs₂)
_&_ = And.lift

-- D distributes over _&_.

D-& : ∀ {Tok R₁ R₂ xs₁ xs₂ t}
      (p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂) →
      D t (p₁ & p₂) ≅P D t p₁ & D t p₂
D-& = And.D-lift

-- _&_ preserves equality.

_&-cong_ : ∀ {k Tok R xs₁ xs₁′ xs₂ xs₂′}
             {p₁  : Parser Tok R xs₁} {p₁′ : Parser Tok R xs₁′}
             {p₂  : Parser Tok R xs₂} {p₂′ : Parser Tok R xs₂′} →
           p₁ ∼[ k ]P p₁′ → p₂ ∼[ k ]P p₂′ → p₁ & p₂ ∼[ k ]P p₁′ & p₂′
_&-cong_ = And.lift-cong

-- _&_ is correct.

correct : ∀ {Tok R₁ R₂ xs₁ xs₂ x₁ x₂ s}
          (p₁ : Parser Tok R₁ xs₁) (p₂ : Parser Tok R₂ xs₂) →
          (x₁ , x₂) ∈ p₁ & p₂ · s ↔ (x₁ ∈ p₁ · s × x₂ ∈ p₂ · s)
correct {x₁ = x₁} {x₂} =
  And.lift-property
    (λ F G H → H (x₁ , x₂) ↔ (F x₁ × G x₂))
    (λ F↔F′ G↔G′ H↔H′ →
       Related-cong (H↔H′ (x₁ , x₂)) (F↔F′ x₁ ×-↔ G↔G′ x₂))
    (SK-sym ⊗-∈↔)
  where open Related.EquationalReasoning

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
test : Set
test = {! M !}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Eq.Theory where

open import Prelude
open import T
open import DynTheory
open import SubstTheory
open import Contexts
open import Eq.Defs
open import Eq.KleeneTheory
open import Eq.ObsTheory
open import Eq.LogicalTheory

-- Theory about the interactions between the relationships between the equivs

-- Now that we have shown that logical equivalence is a consistent congruence,
-- it follows that it is contained in observational equivalence.
obs-contains-logical : ∀{Γ} {A} → OLogicalEq Γ A ⊆ ObservEq Γ A
obs-contains-logical = obs-is-coarsest OLogicalEq log-is-con-congruence

obs-contains-clogical : ∀{A} → (LogicalEq A) ⊆ (ObservEq [] A)
obs-contains-clogical leq = obs-contains-logical (closed-logical-imp-open leq)

-- Show that observational equivalence implies logical for closed terms.
obs-implies-closed-logical : ∀{A} {e e' : TCExp A} →
                             [] ⊢ e ≅ e' :: A →
                             e ~ e' :: A
obs-implies-closed-logical {nat} oeq = ObservEq.observe oeq ∘
obs-implies-closed-logical {A ⇒ B} {e} {e'} oeq = body
  where body : (e₁ e₁' : TExp [] A) → LogicalEq A e₁ e₁' → LogicalEq B (e $ e₁) (e' $ e₁')
        body e₁ e₁' leq with obs-contains-clogical leq
        ... | oeq' with obs-trans (obs-congruence oeq' (e e$ ∘)) (obs-congruence oeq (∘ $e e₁'))
        ... | oeq'' = obs-implies-closed-logical oeq''

obs-contains-logical-subst : ∀{Γ} → SubstRel LogicalEq Γ ⊆ SubstRel (ObservEq []) Γ
obs-contains-logical-subst η x = obs-contains-clogical (η x)

-- Since observational implies logical for closed terms and
-- respects substitution of observational equivalent terms,
-- logical equivalence contains observational.
logical-contains-obs : ∀{Γ} {A} → ObservEq Γ A ⊆ OLogicalEq Γ A
logical-contains-obs {Γ} {A} {e} {e'} oeq {γ} {γ'} η
  with substs-respect-obs oeq (obs-contains-logical-subst η)
... | coeq = obs-implies-closed-logical coeq

-- This is sort of silly. We need these lemmas to prove that logical
-- equivalence contains definitional.
nat-val-weakening : ∀{Γ} {n : TNat} → TVal n →
                    Σ[ e :: TExp Γ nat ] (∀{γ : TSubst Γ []} → n ≡ ssubst γ e)
nat-val-weakening val-zero = zero , (λ {γ} → Refl)
nat-val-weakening {Γ} {suc n} (val-suc v) with nat-val-weakening {Γ} v
... | e , subst-thing = (suc e) , (λ {γ} → resp suc subst-thing)

nat-logical-equiv-val : ∀{Γ} (γ : TSubst Γ []) (e : TExp Γ nat) →
                        Σ[ n :: TExp Γ nat ] ((ssubst γ n ~ ssubst γ e :: nat) × TVal (ssubst γ n))
nat-logical-equiv-val {Γ} γ e with kleene-refl {ssubst γ e}
... | kleeneq n val E1 E2 with nat-val-weakening {Γ} val
... | n' , is-val = n' , ((kleeneq n val (ID.coe1 (λ x → x ~>* n) is-val eval-refl) E1) ,
                          ID.coe1 TVal is-val val)

-- Logical equivalence contains definitional equivalence.
logical-contains-def : ∀{Γ} {A} → DefEq Γ A ⊆ OLogicalEq Γ A
logical-contains-def {y = e} def-refl η = ological-refl e η
logical-contains-def {x = e} {y = e'} (def-sym defeq) η =
  ological-sym {_} {_} {e'} {e} (logical-contains-def defeq) η
logical-contains-def {x = e} {y = e''} (def-trans {e' = e'} defeq1 defeq2) η
  with logical-contains-def defeq1 | logical-contains-def defeq2
... | leq1 | leq2 = ological-trans {_} {_} {e} {e'} {e''} leq1 leq2 η
logical-contains-def (def-cong defeq C) η = ological-is-congruence (logical-contains-def defeq) C η
logical-contains-def {Γ} {A} (def-beta {e = e} {e' = e'}) {γ} {γ'} η
  with step-beta {e = (ssubst (liftγ γ) e)} {e' = ssubst γ e'}
... | step with ological-refl e (extendLogicalEQΓ η (ological-refl e' η))

... | leq with subeq (compose-subst-noob γ' e') e ≡≡ subcomp γ' (singγ e') e
... | subeq-r with subcomp (singγ (ssubst γ e')) (liftγ γ) e
... | subeq-l with ID.coe2 (LogicalEq A) subeq-l subeq-r leq
... | leq' = logical-converse-evaluation-1 leq' (eval-step step)

logical-contains-def {Γ} {A} (def-rec-z {e0 = e0} {es = es}) {γ} {γ'} η with ological-refl e0 η
... | leq = logical-converse-evaluation-1 leq (eval-step step-rec-z)

-- This is super nasty. It has some code duplication when handling the congruence stuff.
-- And it also needs to deal with a bunch of nasty substitution crap.
-- The main source of nonstupid complication is that the step rule requires
-- n to be a value, and definitional equivalence does not.
logical-contains-def {Γ} {A} (def-rec-s {e = en} {e0 = e0} {es = es}) {γ} {γ'} η
  with nat-logical-equiv-val γ en
... | n , num-leq , is-val with ological-refl (rec en e0 es) η

... | full-leq with ological-is-congruence {e = ssubst γ n} {e' = ssubst γ en}
                    (closed-logical-imp-open num-leq) (rec1 ∘ (ssubst γ e0) (ssubst (liftγ γ) es))
                    (emptyLogicalEqΓ {γ = emptyγ} {γ' = emptyγ})
... | eq-with-γn-and-nasty-subst with ID.coe2 (LogicalEq A) (subid _) (subid _) eq-with-γn-and-nasty-subst
... | eq-with-γn with logical-trans eq-with-γn full-leq

... | leq-subrec with ological-refl (rec (suc en) e0 es) (logicalγ-refl {x = γ})
... | full-leq-s with ological-is-congruence {e = ssubst γ n} {e' = ssubst γ en}
                    (closed-logical-imp-open num-leq) (rec1 (suc ∘) (ssubst γ e0) (ssubst (liftγ γ) es))
                    (emptyLogicalEqΓ {γ = emptyγ} {γ' = emptyγ})
... | eq-with-sγn-and-nasty-subst with ID.coe2 (LogicalEq A) (subid _) (subid _) eq-with-sγn-and-nasty-subst
... | eq-with-sγn with logical-trans eq-with-sγn full-leq-s
... | leq-subrec-2 with ological-refl es (extendLogicalEQΓ η leq-subrec)

... | leq-unrolled with subeq (compose-subst-noob γ' (rec en e0 es)) es ≡≡
                        subcomp γ' (singγ (rec en e0 es)) es
... | subeq-l with subcomp (singγ (ssubst γ (rec n e0 es))) (liftγ γ) es
... | subeq-r with ID.coe2 (LogicalEq A) subeq-r subeq-l leq-unrolled
... | leq with step-rec-s {e = ssubst γ n} {e₀ = ssubst γ e0} {es = ssubst (liftγ γ) es} is-val
... | step with logical-converse-evaluation-1 leq (eval-step step)
... | leq-stepped = logical-trans (logical-sym leq-subrec-2) leq-stepped

-- Obvious corollary that observational equivalence contains definitional.
obs-contains-def : ∀{Γ} {A} → DefEq Γ A ⊆ ObservEq Γ A
obs-contains-def = obs-contains-logical o logical-contains-def

-- Proving this mostly out of spite, because one formulation
-- of my theory needed this for observational equivalence,
-- and there wasn't a good way to prove it other than appealing
-- to observational equivalence coinciding with logical, which
-- was what we were trying to prove.
weakened-equiv-log : ∀{Γ} {A} {e e' : TCExp A} →
                     e ~ e' :: A →
                     Γ ⊢ weaken-closed e ~ weaken-closed e' :: A
weakened-equiv-log {Γ} {A} {e} {e'} leq {γ} {γ'} η with subren γ closed-wkγ e | subren γ' closed-wkγ e'
... | eq1 | eq2 with closed-subst (γ o closed-wkγ) e | closed-subst (γ' o closed-wkγ) e'
... | eq1' | eq2' = ID.coe2 (LogicalEq A) (symm eq1' ≡≡ symm eq1) (symm eq2' ≡≡ symm eq2) leq

weakened-equiv-obs : ∀{Γ} {A} {e e' : TCExp A} →
                     [] ⊢ e ≅ e' :: A →
                     Γ ⊢ weaken-closed e ≅ weaken-closed e' :: A
weakened-equiv-obs {Γ} {A} {e} {e'} oeq = obs-contains-logical (weakened-equiv-log {Γ} {A} {e} {e'} (obs-implies-closed-logical oeq))

-- Some more stuff about renaming.
wkren1 : ∀{Γ A} → TRen Γ (A :: Γ)
wkren1 = (λ x → S x)

weaken1 : ∀{Γ A B} → TExp Γ B → TExp (A :: Γ) B
weaken1 e = ren wkren1 e

weakening-ignores : ∀{Γ A} (e₁ : TCExp A) (γ : TSubst Γ []) →
                    Sub≡ (λ x₁ → ssubst (singγ e₁) (ren wkren1 (γ x₁))) γ
weakening-ignores e₁ γ x = subren (singγ e₁) wkren1 (γ x)  ≡≡ subid (γ x)

-- Functional extensionality
function-ext-log : ∀{Γ A B} {e e' : TExp Γ (A ⇒ B)} →
                   (A :: Γ) ⊢ weaken1 e $ var Z ~ weaken1 e' $ var Z :: B →
                   Γ ⊢ e ~ e' :: A ⇒ B
function-ext-log {Γ} {A} {B} {e} {e'} leq {γ} {γ'} η e₁ e₁' leq'
  with leq (extendLogicalEQΓ η leq')
... | leq'' with subren (subComp (singγ e₁) (liftγ γ)) wkren1 e |
                 subren (subComp (singγ e₁') (liftγ γ')) wkren1 e'
... | eq1' | eq2' with eq1' ≡≡ subeq (weakening-ignores e₁ γ) e |
                       eq2' ≡≡ subeq (weakening-ignores e₁' γ') e'
... | eq1 | eq2 = ID.coe2 (LogicalEq B) (resp (λ x → x $ e₁) eq1) (resp (λ x → x $ e₁') eq2)  leq''

function-ext-obs : ∀{Γ A B} {e e' : TExp Γ (A ⇒ B)} →
                   (A :: Γ) ⊢ weaken1 e $ var Z ≅ weaken1 e' $ var Z :: B →
                   Γ ⊢ e ≅ e' :: A ⇒ B
function-ext-obs {e = e} {e' = e'} oeq = obs-contains-logical
                                         (function-ext-log {e = e} {e' = e'} (logical-contains-obs oeq))

-- Eta, essentially
-- The important part of the proof is the def-beta and the function-ext-obs,
-- but most of the actual work is fucking around with substitutions.
function-eta-obs : ∀{Γ A B} (e : TExp Γ (A ⇒ B)) →
                   Γ ⊢ e ≅ (Λ (weaken1 e $ var Z)) :: A ⇒ B
function-eta-obs {Γ} {A} {B} e with
  obs-sym (obs-contains-def (def-beta {e = ren (wk wkren1) (ren wkren1 e) $ var Z} {e' = var Z}))

... | beta-eq with (subren (singγ (var Z)) (wk wkren1) (weaken1 e)) ≡≡
                   (subren (λ x → singγ (var Z) (wk wkren1 x)) wkren1 e) ≡≡
                   symm (subren emptyγ wkren1 e) ≡≡
                   subid (weaken1 e)
... | eq2 with resp (λ x → x $ var Z) eq2
... | eq with ID.coe2 (ObservEq (A :: Γ) B) eq refl beta-eq
... | oeq = function-ext-obs oeq

obs-equiv-nat-val : (e : TNat) → Σ[ n :: TNat ] (TVal n × ([] ⊢ e ≅ n :: nat))
obs-equiv-nat-val e with ological-equiv-nat-val e
obs-equiv-nat-val e | n , val , eq = n , val , obs-contains-logical eq

-- OK, maybe we are trying this with numerals again. Argh.

t-numeral : ∀{Γ} → Nat → TExp Γ nat
t-numeral Z = zero
t-numeral (S n) = suc (t-numeral n)

numeral-val : ∀{Γ} → (n : Nat) → TVal {Γ} (t-numeral n)
numeral-val Z = val-zero
numeral-val (S n) = val-suc (numeral-val n)

val-numeral : ∀{Γ} {e : TExp Γ nat} → TVal e → Σ[ n :: Nat ] (e ≡ t-numeral n)
val-numeral val-zero = Z , Refl
val-numeral (val-suc v) with val-numeral v
... | n , eq = (S n) , (resp suc eq)

numeral-subst-dontcare : ∀{Γ Γ'} (n : Nat) (γ : TSubst Γ Γ') → ssubst γ (t-numeral n) ≡ t-numeral n
numeral-subst-dontcare Z γ = Refl
numeral-subst-dontcare (S n) γ = resp suc (numeral-subst-dontcare n γ)

--
obs-equiv-numeral : (e : TNat) → Σ[ n :: Nat ] ([] ⊢ e ≅ t-numeral n :: nat)
obs-equiv-numeral e with obs-equiv-nat-val e
obs-equiv-numeral e | en , val , oeq with val-numeral val
... | n , eq = n , (ID.coe1 (ObservEq [] nat e) eq oeq)

dropSubstRel : ∀(R : CRel) {Γ A} {γ γ' : TSubst (A :: Γ) []} →
               SubstRel R (A :: Γ) γ γ' →
               SubstRel R Γ (dropγ γ) (dropγ γ')
dropSubstRel R η n = η (S n)
dropLogicalEqΓ = dropSubstRel LogicalEq

-- Allow induction over nats, essentially
function-induction-log : ∀{Γ A} {e e' : TExp (nat :: Γ) A} →
                         ((n : Nat) → Γ ⊢ ssubst (singγ (t-numeral n)) e ~
                                          ssubst (singγ (t-numeral n)) e' :: A) →
                         (nat :: Γ) ⊢ e ~ e' :: A
function-induction-log {Γ} {A} {e} {e'} f {γ} {γ'} η
  with η Z | obs-equiv-numeral (γ Z)
... | n-eq | n , oeq-n with f n (dropLogicalEqΓ η)
... | butt with subcomp (dropγ γ) (singγ (t-numeral n)) e | subcomp (dropγ γ') (singγ (t-numeral n)) e'
... | lol1 | lol2 with subeq (compose-subst-noob (dropγ γ) (t-numeral n)) e |
                       subeq (compose-subst-noob (dropγ γ') (t-numeral n)) e'
... | lol1' | lol2' with ID.coe2 (LogicalEq A) (symm lol1 ≡≡ symm lol1') (symm lol2 ≡≡ symm lol2') butt
... | wtf with ID.coe2
               (λ x y → LogicalEq A
                        (ssubst (extendγ (dropγ γ) x) e)
                        (ssubst (extendγ (dropγ γ') y) e'))
               (numeral-subst-dontcare n (dropγ γ)) (numeral-subst-dontcare n (dropγ γ')) wtf
... | wtf' with ological-refl e (extendLogicalEQΓ (dropLogicalEqΓ (logicalγ-refl {x = γ})) (obs-consistent oeq-n))
... | leq-e with ID.coe2 (LogicalEq A) (symm (subeq (drop-fix γ) e)) Refl leq-e
... | leq-e' with ological-refl e' (extendLogicalEQΓ (dropLogicalEqΓ (logicalγ-refl {x = γ'}))
                                    (kleene-trans (kleene-sym n-eq) (obs-consistent oeq-n)))
... | leq-e2 with ID.coe2 (LogicalEq A) (symm (subeq (drop-fix γ') e')) Refl leq-e2
... | leq-e2' = logical-trans leq-e' (logical-trans wtf' (logical-sym leq-e2'))

function-induction-obs : ∀{Γ A} {e e' : TExp (nat :: Γ) A} →
                         ((n : Nat) → Γ ⊢ ssubst (singγ (t-numeral n)) e ≅
                                          ssubst (singγ (t-numeral n)) e' :: A) →
                         (nat :: Γ) ⊢ e ≅ e' :: A
function-induction-obs {Γ} {A} {e} {e'} f =
                           obs-contains-logical
                            (function-induction-log {Γ} {A} {e} {e'}
                             (λ n → logical-contains-obs (f n)))

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


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

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

macro
  doQuote : ∀ {ℓ} {A : Set ℓ} → A → Term → TC _
  doQuote x hole = bindTC (quoteTC x) (λ qx → bindTC (quoteTC qx) (unify hole))

testQuote₁ : doQuote Prop ≡ agda-sort (propLit 0)
testQuote₁ = refl

testQuote₂ : ∀ {ℓ} → doQuote (Prop ℓ) ≡ agda-sort (prop (var 0 []))
testQuote₂ = refl

macro
  doUnquote : Term → Term → TC _
  doUnquote t hole = bindTC (unquoteTC t) (unify hole)

testUnquote₁ : doUnquote (agda-sort (propLit 0)) ≡ Prop
testUnquote₁ = refl

testUnquote₂ : ∀ {ℓ} → doUnquote (agda-sort (prop (var 0 []))) ≡ Prop ℓ
testUnquote₂ = refl


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary

module Cubical.Relation.Binary.Construct.StrictToNonStrict
  {a ℓ} {A : Type a}
  (_<_ : Rel A ℓ)
  where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Logic hiding (_⇒_) renaming (inl to inlₚ; inr to inrₚ)

open import Cubical.Data.Prod
open import Cubical.Data.Sum.Base renaming (rec to ⊎-rec)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) using (isProp⊥)
open import Cubical.Relation.Binary.Properties
open import Cubical.Relation.Nullary
open import Cubical.HITs.PropositionalTruncation as PT

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

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

_≤_ : Rel A _
x ≤ y = (x < y) ⊔ (x ≡ₚ y)

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

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = inlₚ

≤-fromEq : FromEq _≤_
≤-fromEq = inrₚ

≤-reflexive : Reflexive _≤_
≤-reflexive = fromeq→reflx _≤_ ≤-fromEq

≤-antisym : Transitive _<_ → Irreflexive _<_ → Antisymmetric _≤_
≤-antisym transitive irrefl = rec2 squash λ
  { (inl x) (inl y) → ⊥-elim (irrefl (transitive x y))
  ; (inl x) (inr y) → PT.map sym y
  ; (inr x) _ → x
  }

≤-transitive : Transitive _<_ → Transitive _≤_
≤-transitive <-trans = rec2 squash λ
  { (inl x) (inl y) → inlₚ (<-trans x y)
  ; (inl x) (inr y) → inlₚ (substₚ (λ k → _ < k) y x)
  ; (inr x) (inl y) → inlₚ (substₚ (λ i → i < _) (PT.map sym x) y)
  ; (inr x) (inr y) → inrₚ (PT.map2 _∙_ x y)
  }

<-≤-trans : Transitive _<_ → Trans _<_ _≤_ _<_
<-≤-trans transitive x<y = rec (isProp[ _<_ ] _ _) λ
  { (inl x) → transitive x<y x
  ; (inr x) → substₚ (λ k → _ < k) x x<y
  }

≤-<-trans : Transitive _<_ → Trans _≤_ _<_ _<_
≤-<-trans transitive = rec (isPropΠ λ _ → isProp[ _<_ ] _ _) λ
  { (inl x) y → transitive x y
  ; (inr x) y → substₚ (λ i → i < _) (PT.map sym x) y
  }

≤-total : Trichotomous _<_ → Total _≤_
≤-total <-tri x y with <-tri x y
... | tri< x<y x≢y x≯y = inlₚ (inlₚ x<y)
... | tri≡ x≮y x≡y x≯y = inlₚ (inrₚ ∣ x≡y ∣)
... | tri> x≮y x≢y x>y = inrₚ (inlₚ x>y)

≤-decidable : Discrete A → Decidable _<_ → Decidable _≤_
≤-decidable _≟_ _<?_ x y with x <? y
... | yes x<y = yes (inlₚ x<y)
... | no x≮y with x ≟ y
... |    yes x≡y = yes (inrₚ ∣ x≡y ∣)
... |    no x≢y = no (rec isProp⊥ λ
                    { (inl x<y) → x≮y x<y
                    ; (inr x≡y) → x≢y (rec (Discrete→isSet _≟_ _ _) id x≡y)
                    })

≤-decidable′ : Trichotomous _<_ → Decidable _≤_
≤-decidable′ compare x y with compare x y
... | tri< x<y x≢y x≯y = yes (inlₚ x<y)
... | tri≡ x≮y x≡y x≯y = yes (inrₚ ∣ x≡y ∣)
... | tri> x≮y x≢y x>y = no (rec isProp⊥ λ
                          { (inl x<y) → x≮y x<y
                          ; (inr x≡y) → x≢y (rec (Discrete→isSet (tri→dec≡ _<_ compare) _ _) id x≡y)
                          })

------------------------------------------------------------------------
-- Converting structures

isPreorder : Transitive _<_ → IsPreorder _≤_
isPreorder transitive = record
  { reflexive  = ≤-reflexive
  ; transitive = ≤-transitive transitive
  }

isPartialOrder : IsStrictPartialOrder _<_ → IsPartialOrder _≤_
isPartialOrder spo = record
  { isPreorder = isPreorder S.transitive
  ; antisym    = ≤-antisym S.transitive S.irrefl
  }
  where module S = IsStrictPartialOrder spo

isTotalOrder : IsStrictTotalOrder _<_ → IsTotalOrder _≤_
isTotalOrder sto = record
  { isPartialOrder = isPartialOrder S.isStrictPartialOrder
  ; total          = ≤-total S.compare
  }
  where module S = IsStrictTotalOrder sto

isDecTotalOrder : IsStrictTotalOrder _<_ → IsDecTotalOrder _≤_
isDecTotalOrder sto = record
  { isTotalOrder = isTotalOrder sto
  ; _≤?_         = ≤-decidable′ S.compare
  }
  where module S = IsStrictTotalOrder sto


text:
-- Andreas, 2010-09-24 deactivated this annoying test case in Makefile
module Impossible where

-- The only way to trigger an __IMPOSSIBLE__ that isn't a bug.
{-# IMPOSSIBLE #-}


text:
-- Andreas, 2019-08-17, issue #1346

-- Allow changing fixity in renaming statement

module Issue1346 where

data Bool : Set where true false : Bool

module Product where

  infixr 4 _,_

  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

module List where

  infixr 5 _∷_

  data List (A : Set) : Set where
    []  : List A
    _∷_ : A → List A → List A

open List public hiding (module List)
open Product public using () renaming
  ( _,_ to infixr 5 _∷_   -- change binding strength of _,_ when imported as _∷_
  ; _×_ to infixr 8 _×_   -- make _×_ right associatives
  )

-- Non-empty lists.

List⁺ : Set → Set
List⁺ A = A × List A

head : ∀{A} → List⁺ A → A
head (a ∷ as) = a

private
  test₁ : List⁺ Bool
  test₁ = true ∷ false ∷ []  -- mixing _∷_ of _×_ and List

open Product public using (_,_)  -- _,_ is still available with original fixity

private
  test₂ : ∀{A : Set} → A → List A × List⁺ A × List⁺ A
  test₂ a = [] , a ∷ [] , a ∷ a ∷ []  -- mixing _,_ and _∷_ of _×_


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

module lib.groups.Groups where

open import lib.groups.Homomorphisms public
open import lib.groups.Lift public
open import lib.groups.Unit public
open import lib.groups.PropSubgroup public
open import lib.groups.GroupProduct public
open import lib.groups.PullbackGroup public
open import lib.groups.TruncationGroup public
open import lib.groups.HomotopyGroup public
open import lib.groups.FormalSum public

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Exponential and compatible strengths
module SOAS.Abstract.ExpStrength {T : Set} where

open import SOAS.Families.Core {T}
open import SOAS.Context
open import SOAS.Variable
open import SOAS.ContextMaps.Combinators
open import SOAS.ContextMaps.CategoryOfRenamings

open import SOAS.Common
open import SOAS.Coalgebraic.Strength
import SOAS.Abstract.Coalgebra as →□
open →□.Sorted
open →□.Unsorted using (⊤ᵇ) renaming (Coalg to UCoalg ; Coalg⇒ to UCoalg⇒ ; □ᵇ to □ᵘᵇ)
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Families.BCCC using (⊤ₘ)

private
  variable
    X : Family
    𝒴 𝒵 : Familyₛ
    Γ Δ Θ : Ctx
    α : T

-- Mixed-sorted Cartesian and linear exponentials
_⇨_ : Family → Familyₛ → Familyₛ
(X ⇨ 𝒴) τ Γ =  X Γ → 𝒴 τ Γ

_➡_ : Family → Familyₛ → Familyₛ
X ➡ 𝒴 = □ (X ⇨ 𝒴)

_⊸_ : Family → Familyₛ → Familyₛ
(X ⊸ 𝒴) α Γ = {Δ : Ctx} → X Δ → 𝒴 α (Γ ∔ Δ)

[_⊸_] : Familyₛ → Familyₛ → Family
[ 𝒳 ⊸ 𝒴 ] Γ = {τ : T}{Δ : Ctx} → 𝒳 τ Δ → 𝒴 τ (Δ ∔ Γ)

-- Linear exponential [ 𝒳 ⊸ 𝒴 ] is an unsorted coalgebra if 𝒴 is sorted coalgebra
[_⊸_]ᵇ : (𝒳 {𝒴} : Familyₛ) → Coalg 𝒴 → UCoalg ([ 𝒳 ⊸ 𝒴 ])
[ 𝒳 ⊸ 𝒴ᵇ ]ᵇ = record
  { r = λ l ρ {_}{Δ} x → r (l x) (Δ ∔∣ ρ)
  ; counit = λ{ {Γ = Γ}{t = l} → iext (dext λ {Δ} ρ →  trans (r≈₂ (Concatʳ.identity Γ {Δ})) counit) }
  ; comult = λ{ {Γ = Γ}{Δ}{Θ}{ρ = ρ}{ϱ}{l} → iext (dext λ {Ξ} x → trans (r≈₂ (Functor.homomorphism (Ξ ∔F-))) comult) } }
  where
  open Coalg 𝒴ᵇ

-- Shorthands
⟅_⇨_⟆ : Familyₛ → Familyₛ → Familyₛ
⟅ 𝒳 ⇨ 𝒴 ⟆ = [ 𝒳 ⊸ 𝒴 ] ⇨ 𝒴
⟅_➡_⟆ : Familyₛ → Familyₛ → Familyₛ
⟅ 𝒳 ➡ 𝒴 ⟆ = [ 𝒳 ⊸ 𝒴 ] ➡ 𝒴
⟅_⊸_⟆ : Familyₛ → Familyₛ → Familyₛ
⟅ 𝒳 ⊸ 𝒴 ⟆ = [ 𝒳 ⊸ 𝒴 ] ⊸ 𝒴

-- Exponential strength of an endofunctor
record ExpStrength (Fᶠ : Functor 𝔽amiliesₛ 𝔽amiliesₛ) : Set₁ where
  open Functor Fᶠ

  field
    -- Strength transformation that lifts a 𝒫-substitution over an endofunctor F₀
    estr : {X : Family}(Xᵇ : UCoalg X)(𝒴 : Familyₛ)
         → F₀ (X ⇨ 𝒴) ⇾̣ (X ⇨ F₀ 𝒴)

    -- Naturality conditions for the two components
    estr-nat₁ : {X X′ : Family}{Xᵇ : UCoalg X}{X′ᵇ : UCoalg X′}{𝒴 : Familyₛ}
              → {f : X′ ⇾ X}(fᵇ⇒ : UCoalg⇒ X′ᵇ Xᵇ f)
              → (e : F₀ (X ⇨ 𝒴) α Γ) (x : X′ Γ)
      → estr Xᵇ 𝒴 e (f x)
      ≡ estr X′ᵇ 𝒴 (F₁ (λ e x → e (f x)) e) x

    estr-nat₂ : {X : Family}{Xᵇ : UCoalg X}{𝒴 𝒴′ : Familyₛ}
              → (g : 𝒴 ⇾̣ 𝒴′)(e : F₀ (X ⇨ 𝒴) α Γ)(x : X Γ)
      → estr Xᵇ 𝒴′ (F₁ (λ e x → g (e x)) e) x
      ≡ F₁ g (estr Xᵇ 𝒴 e x)

    estr-unit : {𝒴 : Familyₛ}{e : F₀ (⊤ₘ ⇨ 𝒴) α Γ}
              → estr ⊤ᵇ 𝒴 e tt ≡ F₁ (λ e′ → e′ tt) e

  -- Derived unit law
  estr-unit′ : {X : Family}{Xᵇ : UCoalg X}{𝒴 : Familyₛ}{e : F₀ (X ⇨ 𝒴) α Γ}
               {x : {Γ : Ctx} → X Γ}(fᵇ⇒ : UCoalg⇒ ⊤ᵇ Xᵇ (λ _ → x))
             → estr Xᵇ 𝒴 e x ≡ F₁ (λ e′ → e′ x) e
  estr-unit′ {X = X}{Xᵇ}{𝒴}{e}{x} fᵇ⇒ = begin
        estr Xᵇ 𝒴 e x                                  ≡⟨⟩
        estr Xᵇ 𝒴 e ((λ _ → x) tt)                     ≡⟨ estr-nat₁ fᵇ⇒ e tt ⟩
        estr ⊤ᵇ 𝒴 (F₁ (λ e′ _ → e′ x) e) tt            ≡⟨ estr-unit ⟩
        F₁ (λ e′ → e′ tt) (F₁ (λ e′ _ → e′ x) e)        ≡˘⟨ homomorphism ⟩
        F₁ (λ e′ → e′ x) e
    ∎ where open ≡-Reasoning

  -- Combination of coalgebraic and exponential strength over X ➡ 𝒴 = □ (X ⇨ 𝒴)
  module ➡-Strength (F:Str : Strength Fᶠ) where
    open Strength F:Str
    open ≡-Reasoning
    □estr : (Xᵇ : UCoalg X)(𝒴 : Familyₛ)
          → F₀ (X ➡ 𝒴) ⇾̣ (X ➡ F₀ 𝒴)
    □estr {X} Xᵇ 𝒴 e ρ x = estr Xᵇ 𝒴 (str ℐᴮ (X ⇨ 𝒴) e ρ) x

-- Compatible exponential and coalgebraic strengths
-- (for now no extra condition)
record CompatStrengths (Fᶠ : Functor 𝔽amiliesₛ 𝔽amiliesₛ) : Set₁ where
  open Functor Fᶠ
  field
    CoalgStr : Strength Fᶠ
    ExpStr : ExpStrength Fᶠ

  open Strength CoalgStr public
  open ExpStrength ExpStr public

  open ➡-Strength CoalgStr public


text:
module Structure.Operator.Monoid.Monoids.Function where

open import Functional
open import Function.Equals
open import Function.Equals.Proofs
import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Function
open import Structure.Operator.Monoid
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}

function-monoid : ⦃ equiv : Equiv{ℓₑ}(T)⦄ ⦃ function : ∀{f : T → T} → Function(f) ⦄ → Monoid(_∘_ {X = T}{Y = T}{Z = T})
Monoid.binary-operator    function-monoid = [⊜][∘]-binaryOperator
Monoid.associativity      function-monoid = intro(\{f g h} → [⊜]-associativity {x = f}{y = g}{z = h})
Monoid.identity-existence function-monoid = [∃]-intro id ⦃ [⊜]-identity ⦄


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

open import Agda.Builtin.Equality

postulate
  A : Set
  x0 : A
  f : A → A → A

{-# BUILTIN REWRITE _≡_ #-}

postulate
  fxx : (x : A) → (f x x) ≡ x

{-# REWRITE fxx #-}

meta : A
meta-reveal : meta ≡ x0
test : f x0 meta ≡ x0

meta = _
test = refl
meta-reveal = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Implementation of Gödel's System T as an example for
-- Σ-terms (Σ = {Z, S}; α(Z) = 0; α(S) = 1) with primitive recursion
module SystemT where

open import Data.Vec hiding (_++_)
open import Data.Nat
open import Data.List
open import Data.List.All

-- Not in use yet:
-- Σ is a vector of given length n of natural numbers denoting the arity of symbols
data Σ {n : ℕ} : Set where
  intr : Vec ℕ n → Σ

-- Successor has arity one, Zero has arity 0
Σ-Nat = intr (1 ∷ 0 ∷ [])

-- Types
data Type : Set where
  Nat  : Type
  Fun  : Type → Type → Type

-- Type environment
Env : Set
Env = List Type

-- Environment lookup
data _∈`_ : Type → Env → Set where
  here  : ∀ {φ A}    → A ∈` (A ∷ φ)
  there : ∀ {φ A A'} → A ∈` φ → A ∈` (A' ∷ φ)

-- Zero & Successor, Variables, prim. recursion on Σ-Nat, Abstraction, Application
data Expr : Env → Type → Set where
  Z      : ∀ {φ}     → Expr φ Nat
  S      : ∀ {φ}     → Expr φ Nat → Expr φ Nat
  Var    : ∀ {φ A}   → A ∈` φ → Expr φ A
  NatRec : ∀ {φ A}   → Expr φ A → Expr (A ∷ φ) A → Expr φ Nat → Expr φ A
  Abs    : ∀ {φ A B} → Expr (A ∷ φ) B → Expr φ (Fun A B)
  App    : ∀ {φ A B} → Expr φ (Fun A B) → Expr φ A → Expr φ B

----- Big step semantics using Agda semantics -----
Value : Type → Set
Value Nat        = ℕ
Value (Fun A B)  = Value A → Value B

-- Lookup in environment of values
access : ∀ {A φ} → A ∈` φ → All Value φ → Value A
access here      (px ∷ p) = px
access (there x) (px ∷ p) = access x p

-- Conversion of a natural number to an expression
natconv : ∀ {φ} → ℕ → Expr φ Nat
natconv zero    = Z
natconv (suc n) = S (natconv n)

natrec : ∀ {A : Set} → A → (A → A) → ℕ → A
natrec vz vs zero    = vz
natrec vz vs (suc n) = vs (natrec vz vs n)

-- Evaluation
eval : ∀ {φ A} → Expr φ A → All Value φ → Value A
eval Z ϱ                   = zero
eval (S x) ϱ               = suc (eval x ϱ)
eval (Var x) ϱ             = access x ϱ
eval (NatRec ez es enat) ϱ = natrec (eval ez ϱ) (λ v → eval es (v ∷ ϱ)) (eval enat ϱ)
eval (Abs e) ϱ             = λ x → eval e (x ∷ ϱ)
eval (App e e₁) ϱ          = (eval e ϱ) (eval e₁ ϱ)

----- Small step semantics -----
----- Substitution: Two methods.
-- a) Define simultaneous substitution with a map from variables to expression; see LDLC.agda and
--    the book "Programming Language Foundations in Agda"
-- b) Define singular substitution but "within" environments, i.e. for terms of the form (φ' ++ A ∷ φ)
--    This makes the Var case a tiny bit more tricky. See also type substitution in LDLC.agda
----- Method b is chosen since it is a bit shorter and (subjectively) easier to understand

-- Lemmas required for substitution, esp. Var case
-- 0) Insertion: Insert a variable and adjust DeBruijn indices
--  0.1) De Bruijn adjustement
insdebr : ∀ {φ φ'} {A B} → B ∈` (φ' ++ φ) → B ∈` (φ' ++ (A ∷ φ))
insdebr {φ' = []} here           = there here
insdebr {φ' = []} (there x)      = there (there x)
insdebr {φ' = y ∷ ys} here      = here
insdebr {φ' = y ∷ ys} (there x) = there (insdebr x)
--  0.2) Insertion
ins : ∀ {φ φ'} {A B} → Expr (φ' ++ φ) B → Expr (φ' ++ A ∷ φ) B
ins Z                                   = Z
ins (S x)                               = S (ins x)
ins (Var x)                             = Var (insdebr x)
ins {φ' = φ'} (NatRec{A = A'} ez es en) = NatRec (ins ez) (ins{φ' = A' ∷ φ'} es) (ins en)
ins {φ' = φ'} (Abs{A = A'} x)           = Abs (ins{φ' = A' ∷ φ'}  x)
ins (App x y)                           = App (ins x) (ins y)
-- 1) Variable substitution
varsub : ∀ {φ φ'} {A B} → A ∈` (φ' ++ B ∷ φ) → Expr φ B → Expr (φ' ++ φ) A
varsub {φ' = []} here M           = M
varsub {φ' = []} (there x) M      = Var x
varsub {φ' = z ∷ zs} here M      = Var here
varsub {φ' = z ∷ zs} (there x) M = ins{φ' = []} (varsub x M)

-- Substitution: Given an expression that binds topmost variable to B and has type A &
--               an expression of type B => we get an expression of type A by binding the topmost
--               variable to that expression
_[[_]] : ∀ {φ φ'} {A B : Type} → Expr (φ' ++ B ∷ φ) A → Expr φ B → Expr (φ' ++ φ) A
Z [[ M ]]               = Z
S N [[ M ]]             = S (N [[ M ]])
Var x [[ M ]]           = varsub x M
NatRec N N' N'' [[ M ]] = NatRec (N [[ M ]]) (N' [[ M ]]) (N'' [[ M ]])
Abs N [[ M ]]           = Abs (N [[ M ]])
App N N' [[ M ]]        = App (N [[ M ]]) (N' [[ M ]])

-- Values
data Value' {φ} : (t : Type) → Expr φ t → Set where
  VZero : Value' Nat Z
  VSuc  : ∀ {x} →  Value' Nat x → Value' Nat (S x)
  VFun  : ∀ {A B exp} → Value' (Fun A B) (Abs exp)

-- Semantics
data _↠_ {φ} : {A : Type} → Expr φ A → Expr φ A → Set where
  -- Basic call-by-value λ-calc. stuff
  -- Application: Elimination & Reduction
  ξ-App1 : ∀ {A B} {L L' : Expr φ (Fun B A)} {M}
           → L ↠ L'
           → App L M ↠ App L' M

  ξ-App2 : ∀ {A B} {M M' : Expr φ A} {L : Expr φ (Fun A B)}
           → Value' (Fun A B) L
           → M ↠ M'
           → App L M ↠ App L M'

  β-App : ∀ {A B M exp}
          → Value' B M
          → App{B = A} (Abs exp) M ↠ (exp [[ M ]])

  -- Elimination for successor
  ξ-Nat : ∀ {L L'}
          → L ↠ L'
          → S L ↠ S L'

  -- Interesting cases
  ξ-NatRec : ∀ {A} {Ez : Expr φ A} {Es En En'}
             → En ↠ En'
             → NatRec Ez Es En ↠ NatRec Ez Es En'

  β-NatRec-Z : ∀ {A} {Ez : Expr φ A} {Es}
               → NatRec Ez Es Z ↠ Ez

  β-NatRec-S : ∀ {A} {Ez : Expr φ A} {Es} {n}
               → Value' Nat n
               → NatRec Ez Es (S n) ↠ (Es [[ NatRec Ez Es n ]])

----- Reflexive & Transitive closure of ↠; defined for chain reasoning
infix 1 begin_
infix 2 _⇨_
infix 2 _⇨⟨_⟩_
infix 3 _∎

data _⇨_ : ∀ {φ} {A} → Expr φ A → Expr φ A → Set where
  -- Reflexivity / end of Reasoning
  _∎ : ∀ {φ} {A} (L : Expr φ A)
       → (L ⇨ L)

  -- Transitivity / chain Reasoning
  _⇨⟨_⟩_ : ∀ {φ A} {L' M : Expr φ A}
           → (L : Expr φ A)
           → L ↠ L'
           → L' ⇨ M
           → L ⇨ M

-- Highlight the start of a chain of reasoning
begin_ : ∀ {φ} {A} {M N : Expr φ A} → M ⇨ N → M ⇨ N
begin x = x

----- Progress Theorem; also used to generate evaluation sequence (since it defines how to evaluate)
-- Definition: ∀ M : (Value'(M) ∨ (∃ N : M ↠ N))
data Progress {A} (M : Expr [] A) : Set where
  step : ∀ {N : Expr [] A} → M ↠ N → Progress M
  done : Value' A M → Progress M

-- Proof
progress : ∀ {A} → (M : Expr [] A) → Progress M
progress Z                 = done VZero
progress (S L) with progress L
... | step L↠N            = step (ξ-Nat L↠N)
... | done y               = done (VSuc y)
progress (NatRec ez es en) with progress en
... | step en↠en'         = step (ξ-NatRec en↠en')
... | done (VZero)         = step (β-NatRec-Z)
... | done (VSuc x)        = step (β-NatRec-S x)
progress (Abs L)           = done VFun
progress (App L N) with progress L
... | step L↠L'           = step (ξ-App1 L↠L')
... | done VFun with progress N
...   | step N↠N'         = step (ξ-App2 VFun N↠N')
...   | done val           = step (β-App val)

----- Generation of evaluation sequence (idea & implementation from PLFA)
-- Used to limit number of steps taken
data Gas : Set where
  gas : ℕ → Gas

-- Either enough steps taken or Value' reached
data Finished {φ A} (N : Expr φ A) : Set where
  done : Value' A N → Finished N
  out-of-gas : Finished N

-- Encapsulates the steps taken
data Steps : ∀ {A} → Expr [] A → Set where
  steps : ∀ {A} {L N : Expr [] A}
          → L ⇨ N
          → Finished N
          → Steps L

-- Generation of evaluation
eval' : ∀ {A} → Gas → (L : Expr [] A) → Steps L
eval' (gas zero) L                    = steps (L ∎) out-of-gas
eval' (gas (suc m)) L with progress L
... | done VL                         = steps (L ∎) (done VL)
... | step {M} L↠M with eval' (gas m) M
...    | steps M⇨N fin               = steps (L ⇨⟨ L↠M ⟩ M⇨N) fin

----- Examples
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)

emptyenv : All Value []
emptyenv = []

-- Addition of two numbers defined as primitive recursion
_plus_ : ℕ → ℕ → Expr [] Nat
n plus m  = NatRec (natconv n) (S (Var here)) (natconv m)

-- _ : eval (3 plus 5) emptyenv ≡ 8
-- _ = refl

_ : eval' (gas 5) (1 plus 2) ≡ steps
  (NatRec (S Z) (S (Var here)) (S (S Z)) ⇨⟨ β-NatRec-S (VSuc VZero) ⟩
  (S (NatRec (S Z) (S (Var here)) (S Z)) ⇨⟨ ξ-Nat (β-NatRec-S VZero) ⟩
  (S (S (NatRec (S Z) (S (Var here)) Z)) ⇨⟨ ξ-Nat (ξ-Nat β-NatRec-Z) ⟩ S (S (S Z)) ∎)))
  (done (VSuc (VSuc (VSuc VZero)))) -- 3
_ = {!!}

-- Multiplication of two numbers defined as primitive recursion using addition
_times_ : ℕ → ℕ → Expr [] Nat
n times m = NatRec Z (NatRec (natconv n) (S (Var here)) (Var here)) (natconv m)

-- _ : eval (50 times 5) emptyenv ≡ 250
-- _ = refl

_ : eval' (gas 10) (2 times 2) ≡ steps
 (NatRec Z (NatRec (S (S Z)) (S (Var here)) (Var here)) (S (S Z)) ⇨⟨ β-NatRec-S (VSuc VZero) ⟩
 (NatRec (S (S Z)) (S (Var here))
  (NatRec Z (NatRec (S (S Z)) (S (Var here)) (Var here)) (S Z))  ⇨⟨ ξ-NatRec (β-NatRec-S VZero) ⟩
  (NatRec (S (S Z)) (S (Var here))
   (NatRec (S (S Z)) (S (Var here))
    (NatRec Z (NatRec (S (S Z)) (S (Var here)) (Var here)) Z)) ⇨⟨ ξ-NatRec (ξ-NatRec β-NatRec-Z) ⟩
   (NatRec (S (S Z)) (S (Var here))
    (NatRec (S (S Z)) (S (Var here)) Z) ⇨⟨ ξ-NatRec β-NatRec-Z ⟩
    (NatRec (S (S Z)) (S (Var here)) (S (S Z)) ⇨⟨ β-NatRec-S (VSuc VZero) ⟩
     (S (NatRec (S (S Z)) (S (Var here)) (S Z)) ⇨⟨ ξ-Nat (β-NatRec-S VZero) ⟩
      (S (S (NatRec (S (S Z)) (S (Var here)) Z)) ⇨⟨ ξ-Nat (ξ-Nat β-NatRec-Z) ⟩ S (S (S (S Z))) ∎)))))))
 (done (VSuc (VSuc (VSuc (VSuc VZero))))) -- 4
_ = {!!}

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
{- Box operator. -}
module TemporalOps.Box where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Sets
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.BCCCs
open import CategoryTheory.Functor
open import CategoryTheory.CartesianStrength
open import CategoryTheory.NatTrans
open import CategoryTheory.Adjunction
open import CategoryTheory.Comonad
open import TemporalOps.Common

-- The box operator can be derived as a comonad from an adjunction K ⊣ G

K : Functor 𝕊et ℝeactive
K = record
  { omap = λ A -> (λ n -> A)
  ; fmap = λ f -> (λ n -> λ x -> f x)
  ; fmap-id = refl
  ; fmap-∘ = refl
  ; fmap-cong = λ z → z
  }

G : Functor ℝeactive 𝕊et
G = record
  { omap = λ A -> (∀(n : ℕ) -> A n)
  ; fmap = λ f -> λ a -> (λ n -> f n (a n))
  ; fmap-id = refl
  ; fmap-∘ = refl
  ; fmap-cong = λ pf → ext (λ n → pf)
  }

K⊣G : K ⊣ G
K⊣G = record
    { η = record
        { at = λ A x n → x
        ; nat-cond = refl }
    ; ε = record
        { at = λ A n a → a n
        ; nat-cond = refl }
    ; tri1 = refl
    ; tri2 = refl
    }

-- | Box operator

-- Comonad instance from adjunction
W-□ : Comonad ℝeactive
W-□ = AdjComonad K⊣G

-- Endofunctor from comonad
F-□ : Endofunctor ℝeactive
F-□ = Comonad.W W-□

-- Operator from functor
□_ : τ -> τ
□_ = Functor.omap (Comonad.W W-□)
infixr 65 □_

-- Extensional equality for boxed values
□-≡ : ∀{A} n l {v : (□ A) n}{w : (□ A) l}
   -> v ≡ w
   -> ∀ m -> v m ≡ w m
□-≡ n l refl m = refl

-- □ is a Cartesian functor
F-cart-□ : CartesianFunctor F-□ ℝeactive-cart ℝeactive-cart
F-cart-□ = record
    { u = λ n a _ → a
    ; m = m-□
    ; m-nat₁ = λ f → refl
    ; m-nat₂ = λ f → refl
    ; associative = refl
    ; unital-right = refl
    ; unital-left = refl
    }
    where
    m-□ : ∀(A B : τ) -> □ A ⊗ □ B ⇴ □ (A ⊗ B)
    m-□ A B n (a , b) = λ k → a k , b k

open CartesianFunctor F-cart-□ public

-- □ is a Cartesian comonad
W-cart-□ : CartesianComonad W-□ ℝeactive-cart
W-cart-□ = record { cart-fun = F-cart-□ ; u-ε = refl ; u-δ = refl
                                        ; m-ε = refl ; m-δ = refl }

open CartesianComonad W-cart-□ public

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


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

open import LogicalFormulae
open import Lists.Lists
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations

module Setoids.Lists where

listEquality : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Rel {a} {b} (List A)
listEquality S [] [] = True'
listEquality S [] (x :: w2) = False'
listEquality S (x :: w1) [] = False'
listEquality S (x :: w1) (y :: w2) = (Setoid._∼_ S x y) && listEquality S w1 w2

listEqualityReflexive : {a b : _} {A : Set a} (S : Setoid {a} {b} A) (w : List A) → listEquality S w w
listEqualityReflexive S [] = record {}
listEqualityReflexive S (x :: w) = Equivalence.reflexive (Setoid.eq S) ,, listEqualityReflexive S w

listEqualitySymmetric : {a b : _} {A : Set a} (S : Setoid {a} {b} A) {w1 w2 : List A} → listEquality S w1 w2 → listEquality S w2 w1
listEqualitySymmetric S {w1 = []} {[]} pr = record {}
listEqualitySymmetric S {[]} {x :: xs} ()
listEqualitySymmetric S {x :: xs} {[]} ()
listEqualitySymmetric S {w1 = x :: w1} {y :: w2} (pr1 ,, pr2) = Equivalence.symmetric (Setoid.eq S) pr1 ,, listEqualitySymmetric S pr2

listEqualityTransitive : {a b : _} {A : Set a} (S : Setoid {a} {b} A) {w1 w2 w3 : List A} → listEquality S w1 w2 → listEquality S w2 w3 → listEquality S w1 w3
listEqualityTransitive S {w1 = []} {[]} {[]} w1=w2 w2=w3 = record {}
listEqualityTransitive S {w1 = []} {[]} {x :: xs} w1=w2 ()
listEqualityTransitive S {w1 = []} {x :: xs} {w3} () w2=w3
listEqualityTransitive S {w1 = x :: w1} {[]} {w3} () w2=w3
listEqualityTransitive S {w1 = x :: w1} {y :: ys} {[]} w1=w2 ()
listEqualityTransitive S {w1 = x :: w1} {y :: w2} {z :: w3} (pr1 ,, pr2) (pr3 ,, pr4) = Equivalence.transitive (Setoid.eq S) pr1 pr3 ,, listEqualityTransitive S pr2 pr4

listEqualityRespectsMap : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) (fWD : {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)) → {w1 w2 : List A} (w1=w2 : listEquality S w1 w2) → listEquality T (map f w1) (map f w2)
listEqualityRespectsMap S T f fWD {[]} {[]} w1=w2 = record {}
listEqualityRespectsMap S T f fWD {[]} {x :: w2} ()
listEqualityRespectsMap S T f fWD {x :: w1} {[]} ()
listEqualityRespectsMap S T f fWD {x :: w1} {y :: w2} (x=y ,, w1=w2) = fWD x=y ,, listEqualityRespectsMap S T f fWD {w1} {w2} w1=w2

listSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (List A)
Setoid._∼_ (listSetoid S) word1 word2 = listEquality S word1 word2
Equivalence.reflexive (Setoid.eq (listSetoid S)) {word} = listEqualityReflexive S word
Equivalence.symmetric (Setoid.eq (listSetoid S)) pr = listEqualitySymmetric S pr
Equivalence.transitive (Setoid.eq (listSetoid S)) pr1 pr2 = listEqualityTransitive S pr1 pr2

consWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (xs : List A) {x y : A} (x=y : Setoid._∼_ S x y) → Setoid._∼_ (listSetoid S) (x :: xs) (y :: xs)
consWellDefined {S = S} xs x=y = x=y ,, Equivalence.reflexive (Setoid.eq (listSetoid S))

appendWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {xs ys as bs : List A} (xs=as : Setoid._∼_ (listSetoid S) xs as) → (ys=bs : Setoid._∼_ (listSetoid S) ys bs) → Setoid._∼_ (listSetoid S) (xs ++ ys) (as ++ bs)
appendWellDefined {S = S} {[]} {[]} {[]} {[]} record {} record {} = record {}
appendWellDefined {S = S} {[]} {[]} {[]} {x :: bs} record {} ()
appendWellDefined {S = S} {[]} {x :: ys} {[]} {[]} record {} ys=bs = ys=bs
appendWellDefined {S = S} {[]} {x :: ys} {[]} {x₁ :: bs} record {} ys=bs = ys=bs
appendWellDefined {S = S} {[]} {ys} {x :: as} {bs} () ys=bs
appendWellDefined {S = S} {x :: xs} {ys} {[]} {bs} () ys=bs
appendWellDefined {S = S} {x :: xs} {[]} {x₁ :: as} {[]} xs=as record {} = _&&_.fst xs=as ,, identityOfIndiscernablesRight (listEquality S) (identityOfIndiscernablesLeft (listEquality S) (_&&_.snd xs=as) (equalityCommutative (appendEmptyList xs))) (equalityCommutative (appendEmptyList as))
appendWellDefined {S = S} {x :: xs} {[]} {x₁ :: as} {x₂ :: bs} xs=as ()
appendWellDefined {S = S} {x :: xs} {x₂ :: ys} {x₁ :: as} {[]} xs=as ()
appendWellDefined {S = S} {x :: xs} {x₂ :: ys} {x₁ :: as} {x₃ :: bs} (fst ,, snd) ys=bs = fst ,, appendWellDefined snd ys=bs


text:
open import Common.Reflection
open import Common.Prelude hiding (_<$>_)
open import Common.Equality

_<$>_ : ∀ {A B : Set} → (A → B) → Maybe A → Maybe B
f <$> just x  = just (f x)
f <$> nothing = nothing

_==_ = primQNameEquality

-- This is awkward!
awkwardUnquoteBool : Term → Maybe Bool
awkwardUnquoteBool (con c []) =
  if c == quote true then just true
  else if c == quote false then just false
  else nothing
awkwardUnquoteBool v = nothing

testAwkward : just false ≡ awkwardUnquoteBool (quoteTerm false)
testAwkward = refl

-- This is nicer!
pattern `false = con (quote false) []
pattern `true  = con (quote true) []

unquoteBool : Term → Maybe Bool
unquoteBool `false = just false
unquoteBool `true  = just true
unquoteBool _      = nothing

test : just true ≡ unquoteBool (quoteTerm true)
test = refl


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

module Number.Instances.QuoIntFromIntSIP where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything hiding (⋆) renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

-- open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
-- open import Cubical.Relation.Binary.Base
-- open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
-- open import Cubical.Data.Sigma
-- open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
-- open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
-- open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
-- open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation --.Properties
open import Cubical.Foundations.SIP

-- open import Utils using (!_; !!_)
-- open import MoreLogic.Reasoning
open import MoreLogic.Definitions
-- open import MoreLogic.Properties
-- open import MorePropAlgebra.Definitions hiding (_≤''_)
-- open import MorePropAlgebra.Structures
-- open import MorePropAlgebra.Bundles
-- open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

-- import Agda.Builtin.Int as Builtin
-- import Data.Integer.Base as BuiltinBase
-- import Data.Integer.Properties as BuiltinProps

-- open import Cubical.Data.Nat.Literals
-- open import Number.Prelude.Nat
-- open import Number.Prelude.Int
-- import Cubical.Data.Int as Int
-- import Number.Instances.Int

-- LinearlyOrderedCommRing ≡ LOCR

record LOCRStructure {ℓ ℓ'} (Carrier : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
  constructor locrstructure
  field
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
    is-LOCR : [ isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max ]

LOCRΣ : ∀{ℓ ℓ'} → Type (ℓ-suc (ℓ-max ℓ ℓ'))
LOCRΣ {ℓ} {ℓ'} = TypeWithStr {ℓ' = ℓ-max ℓ (ℓ-suc ℓ')} ℓ (LOCRStructure {ℓ} {ℓ'})

record LOCRΣEquiv {ℓ} {ℓ'} (Σ₁ Σ₂ : LOCRΣ {ℓ} {ℓ'}) (Carrier₁≃₂ : fst Σ₁ ≃ fst Σ₂) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where
  constructor locrΣequiv
  Carrier₁   = fst Σ₁
  Carrier₂   = fst Σ₂
  Structure₁ = snd Σ₁
  Structure₂ = snd Σ₂
  private
    module ₁ = LOCRStructure Structure₁
    module ₂ = LOCRStructure Structure₂
  〚_〛 = equivFun Carrier₁≃₂
  field
    pres0 : 〚 ₁.0f 〛 ≡ ₂.0f
    pres1 : 〚 ₁.1f 〛 ≡ ₂.1f
    isHom--   : ∀ y   → 〚         ₁.- y 〛 ≡             ₂.- 〚 y 〛
    isHom-+   : ∀ x y → 〚       x ₁.+ y 〛 ≡       〚 x 〛 ₂.+ 〚 y 〛
    isHom-·   : ∀ x y → 〚       x ₁.· y 〛 ≡       〚 x 〛 ₂.· 〚 y 〛
    isHom-min : ∀ x y → 〚 ₁.min x     y 〛 ≡ ₂.min 〚 x 〛     〚 y 〛
    isHom-max : ∀ x y → 〚 ₁.max x     y 〛 ≡ ₂.max 〚 x 〛     〚 y 〛
    isHom-<   : ∀ x y →         x ₁.< y   ≡       〚 x 〛 ₂.< 〚 y 〛

LOCREquivStr : ∀{ℓ ℓ'} → StrEquiv (LOCRStructure {ℓ} {ℓ'}) (ℓ-max ℓ (ℓ-suc ℓ'))
LOCREquivStr Σ₁@(Carrier₁ , Structure₁) Σ₂@(Carrier₂ , Structure₂) Carrier₁≃₂ = LOCRΣEquiv Σ₁ Σ₂ Carrier₁≃₂

LOCRUnivalentStructure : ∀{ℓ ℓ'} → UnivalentStr (LOCRStructure {ℓ} {ℓ'}) LOCREquivStr
LOCRUnivalentStructure {A = Σ₁@(Carrier₁ , Structure₁)} {B = Σ₂@(Carrier₂ , Structure₂)} Carrier₁≃₂ = f , φ where
  Carrier₁≡Carrier₂ : Carrier₁ ≡ Carrier₂
  Carrier₁≡Carrier₂ = ua Carrier₁≃₂
  module ₁ = LOCRStructure Structure₁
  module ₂ = LOCRStructure Structure₂
  〚_〛 = equivFun Carrier₁≃₂
  -- {-# DISPLAY equivFun Carrier₁≃₂ x = 〚 x 〛 #-} -- somehow omits its `x` ?

  -- I guess this is what we have "the machinery" for
  f : LOCREquivStr Σ₁ Σ₂ Carrier₁≃₂
    → PathP (λ i → LOCRStructure (Carrier₁≡Carrier₂ i)) Structure₁ Structure₂
  f (locrΣequiv pres0 pres1 isHom-- isHom-+ isHom-· isHom-min isHom-max isHom-<) = {!   !}
  φ : isEquiv f
  φ .equiv-proof Structure₁≡₂ = {!   !}

-- R ≃[ LOCREquivStr ] S ≡ Σ _ (LOCRΣEquiv R S)
-- LOCRΣPath : ∀{ℓ ℓ'} (R S : LOCRΣ {ℓ} {ℓ'}) → (R ≃[ LOCREquivStr ] S) ≃ (R ≡ S)
-- "an equivalence between the two carriers that fulfills the axioms in `LOCRΣEquiv` is equivalent to a path between the two structures"
LOCRΣPath* : ∀{ℓ ℓ'} (R S : LOCRΣ {ℓ} {ℓ'}) → Σ _ (LOCRΣEquiv R S) ≃ (R ≡ S)
LOCRΣPath* = SIP LOCRUnivalentStructure

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint -- congIso

module _ {ℓ ℓ'} where
  LOCRRawStructure'    = λ(X : Type ℓ) → X × X × (X → X) × (X → X → X) × (X → X → X) × (X → X → X) × (X → X → X) × (X → X → hProp ℓ')
  LOCRRawEquivStr'     = AutoEquivStr LOCRRawStructure'

  LOCRRawUnivalentStr' : UnivalentStr _ LOCRRawEquivStr'
  LOCRRawUnivalentStr' = autoUnivalentStr LOCRRawStructure'

  LOCRAxioms' : (X : Type ℓ) (Structure : LOCRRawStructure' X) → _
  LOCRAxioms' X (0f , 1f , -_ , _+_ , _·_ , min , max , _<_) = [ isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max ]

  LOCRStructure'          = AxiomsStructure LOCRRawStructure' LOCRAxioms'
  LOCRΣ'                  = TypeWithStr ℓ LOCRStructure'
  LOCREquivStr'           = AxiomsEquivStr LOCRRawEquivStr' LOCRAxioms'

  LOCRUnivalentStructure' : UnivalentStr LOCRStructure' LOCREquivStr'
  LOCRUnivalentStructure' = axiomsUnivalentStr _ γ LOCRRawUnivalentStr' where
    γ : (X : Type ℓ) (s : LOCRRawStructure' X) → isProp (LOCRAxioms' X s)
    γ X (0f , 1f , -_ , _+_ , _·_ , min , max , _<_) = isProp[] (isLinearlyOrderedCommRing 0f 1f _+_ _·_ -_ _<_ min max)

  LOCRΣPath' : (A B : LOCRΣ') → (A ≃[ LOCREquivStr' ] B) ≃ (A ≡ B)
  LOCRΣPath' = SIP LOCRUnivalentStructure'

  LOCRΣ→' : LOCRΣ {ℓ} {ℓ'} → LOCRΣ'
  LOCRΣ→' (X , s) = let open LOCRStructure s in X , (0f , 1f , -_ , _+_ , _·_ , min , max , _<_) , is-LOCR

  LOCRΣ←' : LOCRΣ' → LOCRΣ {ℓ} {ℓ'}
  LOCRΣ←' (X , (0f , 1f , -_ , _+_ , _·_ , min , max , _<_) , is-LOCR) = (X , γ) where
    γ : LOCRStructure {ℓ} {ℓ'} X
    γ  .LOCRStructure.0f      = 0f
    γ  .LOCRStructure.1f      = 1f
    γ  .LOCRStructure._+_     = _+_
    γ  .LOCRStructure.-_      = -_
    γ  .LOCRStructure._·_     = _·_
    γ  .LOCRStructure.min     = min
    γ  .LOCRStructure.max     = max
    γ  .LOCRStructure._<_     = _<_
    γ  .LOCRStructure.is-LOCR = is-LOCR

  LOCRΣIso : Iso LOCRΣ LOCRΣ'
  LOCRΣIso = iso LOCRΣ→' LOCRΣ←' (λ _ → refl) (λ _ → refl)

  LOCRΣEquiv' = λ(A B : LOCRΣ {ℓ} {ℓ'}) → LOCRΣ→' A ≃[ LOCREquivStr' ] LOCRΣ→' B

  LOCRΣEquivIso : {R S : LOCRΣ} → Iso (Σ _ (LOCRΣEquiv R S)) (LOCRΣEquiv' R S)
  LOCRΣEquivIso .Iso.fun (Carrier₁≃₂ , locrΣequiv pres0   pres1   isHom--   isHom-+   isHom-·   isHom-min   isHom-max   isHom-<) =
                         (Carrier₁≃₂ ,            pres0 , pres1 , isHom-- , isHom-+ , isHom-· , isHom-min , isHom-max , isHom-<)
  LOCRΣEquivIso .Iso.inv (Carrier₁≃₂ ,            pres0 , pres1 , isHom-- , isHom-+ , isHom-· , isHom-min , isHom-max , isHom-<) =
                         (Carrier₁≃₂ , locrΣequiv pres0   pres1   isHom--   isHom-+   isHom-·   isHom-min   isHom-max   isHom-<)
  LOCRΣEquivIso .Iso.rightInv _ = refl
  LOCRΣEquivIso .Iso.leftInv  _ = refl

  -- obtained by SIP-machinery:
  --   our previously defined LOCRΣEquiv-record is equivalent to a path
  LOCRΣPath : (R S : LOCRΣ {ℓ} {ℓ'}) → Σ _ (LOCRΣEquiv R S) ≃ (R ≡ S)
  LOCRΣPath R S =
    Σ _ (LOCRΣEquiv R S) ≃⟨ isoToEquiv LOCRΣEquivIso ⟩
    LOCRΣEquiv' R S ≃⟨ LOCRΣPath' _ _ ⟩
    LOCRΣ→' R ≡ LOCRΣ→' S ≃⟨ isoToEquiv (invIso (congIso LOCRΣIso)) ⟩
    R ≡ S ■

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
{-# OPTIONS --universe-polymorphism #-}
-- There was a bug with reducing levels which could leave
-- instantiated metas in the term.
module Issue469 where

open import Common.Level

postulate
  ∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
  E : ∀ {c d} → Set c → Set d → Set (c ⊔ d)

data K : Set where
  k₁ : K

P : ∀ {e f} → K → Set e → Set f → Set (e ⊔ f)
P k₁ A B = E A B

postulate
  lemma₁ : ∀ {g h} {A : Set g} {B : Set h} → E A B → E A B

  lemma₂ :
    ∀ {i j k l} {A : Set i} {B₁ : A → Set j} {B₂ : A → Set k} →
    (∀ x → P l (B₁ x) (B₂ x)) → P l (∃ B₁) (∃ B₂)

  lemma₃ : ∀ {m n} {A₁ A₂ : Set m} → E A₁ A₂ → P n A₁ A₂

Foo : ∀ o {A : Set} {B₁ B₂ : A → Set o} →
      (∀ x → E (B₁ x) (B₂ x)) → E (∃ B₁) (∃ B₂)
Foo o B₁↔B₂ = lemma₁ (lemma₂ (λ r → lemma₃ (B₁↔B₂ r)))

-- Unsolved constraints:
--
-- o = o
--
-- This constraint shouldn't be too hard to solve...
--
-- I haven't checked, but I suspect that this code type checks using
-- Agda 2.2.10.


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

open import Data.Product using (_×_)
open import Data.String
open import Level
open import Relation.Binary.PropositionalEquality.Core

Valence : Set
Valence = String

data Type : Set where
  Outgoing : Type
  Incoming : Type

infix 5 _,_⦂_
data Context : Set where
  ∅    : Context
  _,_⦂_ : Context → Valence → Type → Context

_+_ : Context → Context → Context
∅           + Γ₂ = Γ₂
(Γ₁ , x ⦂ A) + Γ₂ = (Γ₁ + Γ₂) , x ⦂ A

rename : Context → (Valence → Valence) → Context
rename ∅          ϕ = ∅
rename (Γ , x ⦂ A) ϕ = rename Γ ϕ , ϕ x ⦂ A

data Agent {ℓ} : Context → Set ℓ → Set (suc ℓ) where
  Nil  : ∀ {A : Set ℓ} → Agent ∅ A

  _∙_  : ∀ {Γ A}
       → (ion : Valence)
       → (com : Type)
       → (x : A)
       → Agent (Γ , ion ⦂ com) A

  _∣_  : ∀ {Γ₁ Γ₂} {A B : Set ℓ}
       → Agent Γ₁ A
       → Agent Γ₂ B
       → Agent (Γ₁ + Γ₂) (A × B)

  _/_  : ∀ {Γ A}
       → A
       → (ion : Valence)
       → Agent (Γ , ion ⦂ Outgoing) A

  _[_] : ∀ {Γ A}
       → (ϕ : Valence → Valence)
       → Agent Γ A
       → Agent (rename Γ ϕ) A

  fix_ : ∀ {Γ} {A B : Set ℓ}
       → (f : A → B)
       → Agent Γ A
       → Agent Γ B

infix 4 _∋_⦂_
data _∋_⦂_ : Context → Valence → Type → Set where
  Z : ∀ {Γ x A}
      -----------------
    → Γ , x ⦂ A ∋ x ⦂ A

  S : ∀ {Γ x y A B}
    → x ≢ y
    → Γ ∋ x ⦂ A
      -----------------
    → Γ , y ⦂ B ∋ x ⦂ A

data _⊢_⦂_ : Context → Valence → Type → Set where
  ⊢ : ∀ {Γ x A}
    → Γ ∋ x ⦂ A
      ----------
    → Γ ⊢ x ⦂ A


text:
module Cats.Category.Wedges where

open import Level using (_⊔_ ; suc)
open import Relation.Binary using (Rel ; IsEquivalence)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)
open import Cats.Profunctor
open import Cats.Util.Function using (_on_ ; on-isEquivalence)

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  (F : Profunctor C C D)
  where

  private
    module C = Category C
    module D = Category D
    module F = Profunctor F

  record Wedge : Set (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) where
    open D

    field
      Apex : Obj
      arr : ∀ x → Apex ⇒ pobj F x x
      commute : ∀ {a b} (f : a C.⇒ b)
        → pmap₂ F f ∘ arr a ≈ pmap₁ F f ∘ arr b

  Obj = Wedge

  record _⇒_ (A B : Obj) : Set (lo ⊔ la′ ⊔ l≈′) where
    open Wedge
    open D

    field
      θ : Apex A D.⇒ Apex B
      commute : ∀ x → arr B x ∘ θ ≈ arr A x

  _≈_ : ∀ {A B} → Rel (A ⇒ B) l≈′
  _≈_ = D._≈_ on _⇒_.θ

  equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  equiv = on-isEquivalence _⇒_.θ D.equiv

  id : ∀ {A} → A ⇒ A
  id = record
    { θ = D.id
    ; commute = λ x → D.id-r
    }

  _∘_ : ∀ {A B C} → B ⇒ C → A ⇒ B → A ⇒ C
  _∘_ {A} {B} {C} f g = record
    { θ = θ f ∘S θ g
    ; commute = λ j →
        begin
          arr C j ∘S θ f ∘S θ g
        ≈⟨ D.unassoc ⟩
          (arr C j ∘S θ f) ∘S θ g
        ≈⟨ D.∘-resp-l (commute f j) ⟩
          arr B j ∘S θ g
        ≈⟨ commute g j ⟩
          arr A j
        ∎
    }
    where
      open Wedge using (arr)
      open _⇒_
      open D using () renaming (_∘_ to _∘S_)
      open D.≈-Reasoning

  Wedges : Category (lo ⊔ la ⊔ lo′ ⊔ la′ ⊔ l≈′) (lo ⊔ la′ ⊔ l≈′) l≈′
  Wedges = record
    { Obj = Obj
    ; _⇒_ = _⇒_
    ; _≈_ = _≈_
    ; id = id
    ; _∘_ = _∘_
    ; equiv = equiv
    ; ∘-resp = D.∘-resp
    ; id-r = D.id-r
    ; id-l = D.id-l
    ; assoc = D.assoc
    }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Join.Base where

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

open import Cubical.HITs.S1
open import Cubical.HITs.S3

-- redtt version : https://github.com/RedPRL/redtt/blob/master/library/cool/s3-to-join.red

data join {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  inl : A → join A B
  inr : B → join A B
  push : ∀ a b → inl a ≡ inr b

facek01 : I → I → I → join S¹ S¹
facek01 i j k = hfill (λ l → λ { (j = i0) → push base base (~ l ∧ ~ k)
                               ; (j = i1) → push base base (~ l ∧ ~ k)
                               ; (k = i0) → push (loop j) base (~ l)
                               ; (k = i1) → inl base })
                      (inS (push base base (~ k))) i

border-contraction : I → I → I → I → join S¹ S¹
border-contraction i j k m =
  hfill (λ l → λ { (i = i0) → facek01 i1 j l
                 ; (i = i1) → push base (loop k) (~ l)
                 ; (j = i0) → push base (loop k) (i ∧ ~ l)
                 ; (j = i1) → push base (loop k) (i ∧ ~ l)
                 ; (k = i0) → facek01 (~ i) j l
                 ; (k = i1) → facek01 (~ i) j l })
        (inS (push (loop j) (loop k) i)) m

S³→joinS¹S¹ : S³ → join S¹ S¹
S³→joinS¹S¹ base = inl base
S³→joinS¹S¹ (surf j k i) = border-contraction i j k i1

joinS¹S¹→S³ : join S¹ S¹ → S³
joinS¹S¹→S³ (inl x) = base
joinS¹S¹→S³ (inr x) = base
joinS¹S¹→S³ (push base b i) = base
joinS¹S¹→S³ (push (loop x) base i) = base
joinS¹S¹→S³ (push (loop i) (loop j) k) = surf i j k

connection : I → I → I → I → S³
connection i j k l =
  hfill (λ m → λ { (k = i0) → joinS¹S¹→S³ (facek01 m i j)
                 ; (k = i1) → base
                 ; (j = i0) → base
                 ; (j = i1) → base
                 ; (i = i0) → base
                 ; (i = i1) → base })
        (inS base) l

S³→joinS¹S¹→S³ : ∀ x → joinS¹S¹→S³ (S³→joinS¹S¹ x) ≡ x
S³→joinS¹S¹→S³ base l = base
S³→joinS¹S¹→S³ (surf j k i) l =
  hcomp (λ m → λ { (l = i0) → joinS¹S¹→S³ (border-contraction i j k m)
                 ; (l = i1) → surf j k i
                 ; (i = i0) → connection j m l i1
                 ; (i = i1) → base
                 ; (j = i0) → base
                 ; (j = i1) → base
                 ; (k = i0) → connection j m l (~ i)
                 ; (k = i1) → connection j m l (~ i) })
                 (surf j k i)

joinS¹S¹→S³→joinS¹S¹ : ∀ x → S³→joinS¹S¹ (joinS¹S¹→S³ x) ≡ x
joinS¹S¹→S³→joinS¹S¹ (inl base) l = inl base
joinS¹S¹→S³→joinS¹S¹ (inl (loop i)) l = facek01 i1 i (~ l)
joinS¹S¹→S³→joinS¹S¹ (inr base) l = push base base l
joinS¹S¹→S³→joinS¹S¹ (inr (loop i)) l = push base (loop i) l
joinS¹S¹→S³→joinS¹S¹ (push base base i) l = push base base (i ∧ l)
joinS¹S¹→S³→joinS¹S¹ (push base (loop k) i) l = push base (loop k) (i ∧ l)
joinS¹S¹→S³→joinS¹S¹ (push (loop k) base i) l = facek01 (~ i) k (~ l)
joinS¹S¹→S³→joinS¹S¹ (push (loop j) (loop k) i) l = border-contraction i j k (~ l)

S³IsojoinS¹S¹ : Iso S³ (join S¹ S¹)
Iso.fun S³IsojoinS¹S¹ = S³→joinS¹S¹
Iso.inv S³IsojoinS¹S¹ = joinS¹S¹→S³
Iso.rightInv S³IsojoinS¹S¹ = joinS¹S¹→S³→joinS¹S¹
Iso.leftInv S³IsojoinS¹S¹ = S³→joinS¹S¹→S³

S³≡joinS¹S¹ : S³ ≡ join S¹ S¹
S³≡joinS¹S¹ = isoToPath S³IsojoinS¹S¹

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module _ where

open import Agda.Builtin.Nat

postulate
  F : Set → Set
  pure : ∀ {A} → A → F A
  _<*>_ : ∀ {A B} → F (A → B) → F A → F B

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

ok : ∀ n → F Nat → F (Vec Nat n) → F (Vec Nat (suc n))
ok n a as = (| a ∷ as |)

ok₂ : ∀ n → F Nat → F (Vec Nat n) → F (Vec Nat (suc n))
ok₂ n a as = (| (_∷_ {n = n}) a as |)

fail : ∀ n → F Nat → F (Vec Nat n) → F (Vec Nat (suc n))
fail n a as = (| _∷_ {n = n} a as |)


text:
-- Andreas, 2016-08-02 issue #2127 reported by petercommand

data Test : Set₁ where
  field
    A : Set
    B : Set  -- second field necessary to trigger internal error

-- WAS: internal error

-- Should give proper error


text:
-- Andreas, 2011-10-03
-- allow matching on irrelevant data as long as there is at most one
-- matching constructor
{-# OPTIONS --experimental-irrelevance #-}
module MatchIrrelevant where

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

data NAT : Nat -> Set where
  Zero : NAT zero
  Suc  : (n : Nat) -> NAT n -> NAT (suc n)

-- should succeed:
f : (n : Nat).(N : NAT n) -> Nat
f zero Zero = zero
f (suc n) (Suc .n N) = f n N

-- prove the equations to test reduction

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

fzero : f zero Zero ≡ zero
fzero = refl

fsuc : (n : Nat)(N : NAT n) -> f (suc n) (Suc n N) ≡ f n N
fsuc n N = refl

{- DOES NOT YET WORK and probably should never work
fzero' : (N : NAT zero) → f zero N ≡ zero
fzero' N = refl
-}

{-
-- should fail:
f' : (n : Nat).(N : NAT n) -> Nat
f' zero Zero = zero
f' (suc _) (Suc n N) = n
-}

{-
-- should fail:
g : {n : Nat}.(N : NAT n) -> Nat
g Zero = zero
g (Suc _ N) = g N
-}

{-
data Fin : Nat -> Set where
  zero : (n : Nat) -> Fin (suc n)
  suc  : (n : Nat) -> Fin n -> Fin (suc n)

-- should fail:
toNat : {n : Nat} → .(Fin n) -> Nat
toNat (zero n) = zero
toNat (suc n i) = suc (toNat i)
-}

{-
-- fails for other reasons
weak : {n : Nat} → .(Fin n) -> Fin (suc n)
weak (zero n) = zero (suc n)
weak (suc n i) = suc (suc n) (weak i)
-}


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

open import lib.Basics

module lib.types.Sigma where

-- Cartesian product
_×_ : ∀ {i j} (A : Type i) (B : Type j) → Type (lmax i j)
A × B = Σ A (λ _ → B)

module _ {i j} {A : Type i} {B : A → Type j} where

  pair : (a : A) (b : B a) → Σ A B
  pair a b = (a , b)

  -- pair= has already been defined

  fst= : {ab a'b' : Σ A B} (p : ab == a'b') → (fst ab == fst a'b')
  fst= = ap fst

  snd= : {ab a'b' : Σ A B} (p : ab == a'b')
    → (snd ab == snd a'b' [ B ↓ fst= p ])
  snd= {._} {_} idp = idp

  fst=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → fst= (pair= p q) == p
  fst=-β idp idp = idp

  snd=-β : {a a' : A} (p : a == a')
    {b : B a} {b' : B a'} (q : b == b' [ B ↓ p ])
    → snd= (pair= p q) == q [ (λ v → b == b' [ B ↓ v ]) ↓ fst=-β p q ]
  snd=-β idp idp = idp

  pair=-η : {ab a'b' : Σ A B} (p : ab == a'b')
    → p == pair= (fst= p) (snd= p)
  pair=-η {._} {_} idp = idp

  pair== : {a a' : A} {p p' : a == a'} (α : p == p')
           {b : B a} {b' : B a'} {q : b == b' [ B ↓ p ]} {q' : b == b' [ B ↓ p' ]}
           (β : q == q' [ (λ u → b == b' [ B ↓ u ]) ↓ α ])
    → pair= p q == pair= p' q'
  pair== idp idp = idp

module _ {i j} {A : Type i} {B : Type j} where

  fst×= : {ab a'b' : A × B} (p : ab == a'b') → (fst ab == fst a'b')
  fst×= = ap fst

  snd×= : {ab a'b' : A × B} (p : ab == a'b')
    → (snd ab == snd a'b')
  snd×= = ap snd

  fst×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → fst×= (pair×= p q) == p
  fst×=-β idp idp = idp

  snd×=-β : {a a' : A} (p : a == a')
    {b b' : B} (q : b == b')
    → snd×= (pair×= p q) == q
  snd×=-β idp idp = idp

module _ {i j} {A : Type i} {B : A → Type j} where

  =Σ : (x y : Σ A B) → Type (lmax i j)
  =Σ (a , b) (a' , b') = Σ (a == a') (λ p → b == b' [ B ↓ p ])

  =Σ-eqv : (x y : Σ A B) →  (=Σ x y) ≃ (x == y)
  =Σ-eqv x y =
    equiv (λ pq → pair= (fst pq) (snd pq)) (λ p → fst= p , snd= p)
          (λ p → ! (pair=-η p))
          (λ pq → pair= (fst=-β (fst pq) (snd pq)) (snd=-β (fst pq) (snd pq)))

  =Σ-path : (x y : Σ A B) → (=Σ x y) == (x == y)
  =Σ-path x y = ua (=Σ-eqv x y)

Σ= : ∀ {i j} {A A' : Type i} (p : A == A') {B : A → Type j} {B' : A' → Type j}
  (q : B == B' [ (λ X → (X → Type j)) ↓ p ]) → Σ A B == Σ A' B'
Σ= idp idp = idp

abstract

  Σ-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {P : A → Type j}
    → (has-level n A → ((x : A) → has-level n (P x))
      → has-level n (Σ A P))
  Σ-level {n = ⟨-2⟩} p q =
    ((fst p , (fst (q (fst p)))) ,
      (λ y → pair= (snd p _) (from-transp! _ _ (snd (q _) _))))
  Σ-level {n = S n} p q = λ x y → equiv-preserves-level (=Σ-eqv x y)
    (Σ-level (p _ _)
      (λ _ → equiv-preserves-level ((to-transp-equiv _ _)⁻¹) (q _ _ _)))

  ×-level : ∀ {i j} {n : ℕ₋₂} {A : Type i} {B : Type j}
    → (has-level n A → has-level n B → has-level n (A × B))
  ×-level pA pB = Σ-level pA (λ x → pB)

-- Equivalences in a Σ-type

equiv-Σ-fst : ∀ {i j k} {A : Type i} {B : Type j} (P : B → Type k) {h : A → B}
                  → is-equiv h → (Σ A (P ∘ h)) ≃ (Σ B P)
equiv-Σ-fst {A = A} {B = B} P {h = h} e = equiv f g f-g g-f
  where f : Σ A (P ∘ h) → Σ B P
        f (a , r) = (h a , r)

        g : Σ B P → Σ A (P ∘ h)
        g (b , s) = (is-equiv.g e b , transport P (! (is-equiv.f-g e b)) s)

        f-g : ∀ y → f (g y) == y
        f-g (b , s) = pair= (is-equiv.f-g e b) (trans-↓ P (is-equiv.f-g e b) s)

        g-f : ∀ x → g (f x) == x
        g-f (a , r) =
          pair= (is-equiv.g-f e a)
                (transport (λ q → transport P (! q) r == r [ P ∘ h ↓ is-equiv.g-f e a ])
                           (is-equiv.adj e a)
                           (trans-ap-↓ P h (is-equiv.g-f e a) r) )

equiv-Σ-snd : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  → (∀ x → B x ≃ C x) → Σ A B ≃ Σ A C
equiv-Σ-snd {A = A} {B = B} {C = C} k = equiv f g f-g g-f
  where f : Σ A B → Σ A C
        f (a , b) = (a , fst (k a) b)

        g : Σ A C → Σ A B
        g (a , c) = (a , is-equiv.g (snd (k a)) c)

        f-g : ∀ p → f (g p) == p
        f-g (a , c) = pair= idp (is-equiv.f-g (snd (k a)) c)

        g-f : ∀ p → g (f p) == p
        g-f (a , b) = pair= idp (is-equiv.g-f (snd (k a)) b)

-- Two ways of simultaneously applying equivalences in each component.
module _ {i₀ i₁ j₀ j₁} {A₀ : Type i₀} {A₁ : Type i₁}
         {B₀ : A₀ → Type j₀} {B₁ : A₁ → Type j₁} where
  equiv-Σ : (u : A₀ ≃ A₁) (v : ∀ a → B₀ (<– u a) ≃ B₁ a) → Σ A₀ B₀ ≃ Σ A₁ B₁
  equiv-Σ u v = Σ A₀ B₀           ≃⟨ equiv-Σ-fst _ (snd (u ⁻¹)) ⁻¹ ⟩
                Σ A₁ (B₀ ∘ <– u)  ≃⟨ equiv-Σ-snd v ⟩
                Σ A₁ B₁           ≃∎

  equiv-Σ' : (u : A₀ ≃ A₁) (v : ∀ a → B₀ a ≃ B₁ (–> u a)) → Σ A₀ B₀ ≃ Σ A₁ B₁
  equiv-Σ' u v = Σ A₀ B₀           ≃⟨ equiv-Σ-snd v ⟩
                 Σ A₀ (B₁ ∘ –> u)  ≃⟨ equiv-Σ-fst _ (snd u) ⟩
                 Σ A₁ B₁           ≃∎

-- Implementation of [_∙'_] on Σ
Σ-∙' : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙' pair= p' r) == pair= (p ∙' p') (q ∙'ᵈ r)
Σ-∙' {p = idp} {p' = idp} q idp = idp

-- Implementation of [_∙_] on Σ
Σ-∙ : ∀ {i j} {A : Type i} {B : A → Type j}
  {x y z : A} {p : x == y} {p' : y == z}
  {u : B x} {v : B y} {w : B z}
  (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
  → (pair= p q ∙ pair= p' r) == pair= (p ∙ p') (q ∙ᵈ r)
Σ-∙ {p = idp} {p' = idp} idp r = idp

-- Implementation of [_∙'_] on ×
×-∙' : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙' pair×= p' q') == pair×= (p ∙' p') (q ∙' q')
×-∙' idp idp q idp = idp

-- Implementation of [_∙_] on ×
×-∙ : ∀ {i j} {A : Type i} {B : Type j}
  {x y z : A} (p : x == y) (p' : y == z)
  {u v w : B} (q : u == v) (q' : v == w)
  → (pair×= p q ∙ pair×= p' q') == pair×= (p ∙ p') (q ∙ q')
×-∙ idp idp idp r = idp

-- Special case of [ap-,]
ap-cst,id : ∀ {i j} {A : Type i} (B : A → Type j)
  {a : A} {x y : B a} (p : x == y)
  → ap (λ x → _,_ {B = B} a x) p == pair= idp p
ap-cst,id B idp = idp

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda