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

module Pif2 where

{-- 2 paths --}

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

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; subst₂; cong; cong₂; setoid;
        inspect; [_]; proof-irrelevance; module ≡-Reasoning)
open import Relation.Binary.PropositionalEquality.TrustMe
  using (trustMe)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Data.Nat.Properties
  using (m≢1+m+n; i+j≡0⇒i≡0; i+j≡0⇒j≡0; n≤m+n)
open import Data.Nat.Properties.Simple
  using (+-right-identity; +-suc; +-assoc; +-comm;
        *-assoc; *-comm; *-right-zero; distribʳ-*-+)
open import Data.Nat.DivMod using (_mod_)
open import Relation.Binary using (Rel; Decidable; Setoid)
open import Relation.Binary.Core using (Transitive)

open import Data.String using (String)
  renaming (_++_ to _++S_)
open import Data.Nat.Show using (show)
open import Data.Bool using (Bool; false; true; T; _∧_; _∨_)
open import Data.Nat using (ℕ; suc; _+_; _∸_; _*_; _<_; _≮_; _≤_; _≰_;
  z≤n; s≤s; _≟_; _≤?_; module ≤-Reasoning)
open import Data.Fin
  using (Fin; zero; suc; toℕ; fromℕ; _ℕ-_; _≺_;
         raise; inject+; inject₁; inject≤; _≻toℕ_)
  renaming (_+_ to _F+_)
open import Data.Fin.Properties using (bounded; inject+-lemma)
open import Data.Vec.Properties
  using (lookup∘tabulate; tabulate∘lookup; lookup-allFin; tabulate-∘;
         tabulate-allFin; map-id; allFin-map)

open import Data.List
  using (List; []; _∷_; _∷ʳ_; foldl; replicate; reverse; downFrom;
         concatMap; gfilter; initLast; InitLast; _∷ʳ'_)
  renaming (_++_ to _++L_; map to mapL; concat to concatL; zip to zipL)
open import Data.List.NonEmpty
  using (List⁺; module List⁺; [_]; _∷⁺_; head; last; _⁺++_)
  renaming (toList to nonEmptyListtoList; _∷ʳ_ to _n∷ʳ_; tail to ntail)
open List⁺ public
open import Data.List.Any using (Any; here; there; any; module Membership)
open import Data.Maybe using (Maybe; nothing; just; maybe′)
open import Data.Vec
  using (Vec; tabulate; []; _∷_; tail; lookup; zip; zipWith; splitAt;
         _[_]≔_; allFin; toList)
  renaming (_++_ to _++V_; map to mapV; concat to concatV)
open import Function using (id; _∘_; _$_)

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)

open import Cauchy
open import Perm
open import Proofs
open import CauchyProofs
open import CauchyProofsT
open import CauchyProofsS
open import Groupoid
open import PiLevel0
open import Swaps
open import Pif

------------------------------------------------------------------------------
-- Picture so far:
--
--           path p
--   =====================
--  ||   ||             ||
--  ||   ||2path        ||
--  ||   ||             ||
--  ||   ||  path q     ||
--  t₁ =================t₂
--  ||   ...            ||
--   =====================
--
-- The types t₁, t₂, etc are discrete groupoids. The paths between
-- them correspond to permutations. Each syntactically different
-- permutation corresponds to a path but equivalent permutations are
-- connected by 2paths.  But now we want an alternative definition of
-- 2paths that is structural, i.e., that looks at the actual
-- construction of the path t₁ ⟷ t₂ in terms of combinators... The
-- theorem we want is that α ∼ β iff we can rewrite α to β using
-- various syntactic structural rules. We start with a collection of
-- simplication rules and then try to show they are complete.

-- Simplification rules

infix  30 _⇔_

data _⇔_ : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂) → Set where
  assoc◎l : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          (c₁ ◎ (c₂ ◎ c₃)) ⇔ ((c₁ ◎ c₂) ◎ c₃)
  assoc◎r : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₃ ⟷ t₄} →
          ((c₁ ◎ c₂) ◎ c₃) ⇔ (c₁ ◎ (c₂ ◎ c₃))
  assoc⊕l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (c₁ ⊕ (c₂ ⊕ c₃)) ⇔ (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊)
  assoc⊕r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (assocl₊ ◎ ((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊) ⇔ (c₁ ⊕ (c₂ ⊕ c₃))
  assoc⊗l : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (c₁ ⊗ (c₂ ⊗ c₃)) ⇔ (assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆)
  assoc⊗r : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (assocl⋆ ◎ ((c₁ ⊗ c₂) ⊗ c₃) ◎ assocr⋆) ⇔ (c₁ ⊗ (c₂ ⊗ c₃))
  dist⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          ((c₁ ⊕ c₂) ⊗ c₃) ⇔ (dist ◎ ((c₁ ⊗ c₃) ⊕ (c₂ ⊗ c₃)) ◎ factor)
  factor⇔ : {t₁ t₂ t₃ t₄ t₅ t₆ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
          (dist ◎ ((c₁ ⊗ c₃) ⊕ (c₂ ⊗ c₃)) ◎ factor) ⇔ ((c₁ ⊕ c₂) ⊗ c₃)
  idl◎l   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (id⟷ ◎ c) ⇔ c
  idl◎r   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ id⟷ ◎ c
  idr◎l   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (c ◎ id⟷) ⇔ c
  idr◎r   : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ (c ◎ id⟷)
  linv◎l  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (c ◎ ! c) ⇔ id⟷
  linv◎r  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → id⟷ ⇔ (c ◎ ! c)
  rinv◎l  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → (! c ◎ c) ⇔ id⟷
  rinv◎r  : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → id⟷ ⇔ (! c ◎ c)
  unitel₊⇔ : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (unite₊ ◎ c₂) ⇔ ((c₁ ⊕ c₂) ◎ unite₊)
  uniter₊⇔ : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          ((c₁ ⊕ c₂) ◎ unite₊) ⇔ (unite₊ ◎ c₂)
  unitil₊⇔ : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (uniti₊ ◎ (c₁ ⊕ c₂)) ⇔ (c₂ ◎ uniti₊)
  unitir₊⇔ : {t₁ t₂ : U} {c₁ : ZERO ⟷ ZERO} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti₊) ⇔ (uniti₊ ◎ (c₁ ⊕ c₂))
  unitial₊⇔ : {t₁ t₂ : U} → (uniti₊ {PLUS t₁ t₂} ◎ assocl₊) ⇔ (uniti₊ ⊕ id⟷)
  unitiar₊⇔ : {t₁ t₂ : U} → (uniti₊ {t₁} ⊕ id⟷ {t₂}) ⇔ (uniti₊ ◎ assocl₊)
  swapl₊⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          (swap₊ ◎ (c₁ ⊕ c₂)) ⇔ ((c₂ ⊕ c₁) ◎ swap₊)
  swapr₊⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          ((c₂ ⊕ c₁) ◎ swap₊) ⇔ (swap₊ ◎ (c₁ ⊕ c₂))
  unitel⋆⇔ : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (unite⋆ ◎ c₂) ⇔ ((c₁ ⊗ c₂) ◎ unite⋆)
  uniter⋆⇔ : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          ((c₁ ⊗ c₂) ◎ unite⋆) ⇔ (unite⋆ ◎ c₂)
  unitil⋆⇔ : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (uniti⋆ ◎ (c₁ ⊗ c₂)) ⇔ (c₂ ◎ uniti⋆)
  unitir⋆⇔ : {t₁ t₂ : U} {c₁ : ONE ⟷ ONE} {c₂ : t₁ ⟷ t₂} →
          (c₂ ◎ uniti⋆) ⇔ (uniti⋆ ◎ (c₁ ⊗ c₂))
  unitial⋆⇔ : {t₁ t₂ : U} → (uniti⋆ {TIMES t₁ t₂} ◎ assocl⋆) ⇔ (uniti⋆ ⊗ id⟷)
  unitiar⋆⇔ : {t₁ t₂ : U} → (uniti⋆ {t₁} ⊗ id⟷ {t₂}) ⇔ (uniti⋆ ◎ assocl⋆)
  swapl⋆⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          (swap⋆ ◎ (c₁ ⊗ c₂)) ⇔ ((c₂ ⊗ c₁) ◎ swap⋆)
  swapr⋆⇔ : {t₁ t₂ t₃ t₄ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} →
          ((c₂ ⊗ c₁) ◎ swap⋆) ⇔ (swap⋆ ◎ (c₁ ⊗ c₂))
  swapfl⋆⇔ : {t₁ t₂ t₃ : U} →
          (swap₊ {TIMES t₂ t₃} {TIMES t₁ t₃} ◎ factor) ⇔
          (factor ◎ (swap₊ {t₂} {t₁} ⊗ id⟷))
  swapfr⋆⇔ : {t₁ t₂ t₃ : U} →
          (factor ◎ (swap₊ {t₂} {t₁} ⊗ id⟷)) ⇔
          (swap₊ {TIMES t₂ t₃} {TIMES t₁ t₃} ◎ factor)
  id⇔     : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ c
  trans⇔  : {t₁ t₂ : U} {c₁ c₂ c₃ : t₁ ⟷ t₂} →
          (c₁ ⇔ c₂) → (c₂ ⇔ c₃) → (c₁ ⇔ c₃)
  resp◎⇔  : {t₁ t₂ t₃ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₂ ⟷ t₃} {c₃ : t₁ ⟷ t₂} {c₄ : t₂ ⟷ t₃} →
          (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ◎ c₂) ⇔ (c₃ ◎ c₄)
  resp⊕⇔  : {t₁ t₂ t₃ t₄ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₁ ⟷ t₂} {c₄ : t₃ ⟷ t₄} →
          (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ⊕ c₂) ⇔ (c₃ ⊕ c₄)
  resp⊗⇔  : {t₁ t₂ t₃ t₄ : U}
          {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₁ ⟷ t₂} {c₄ : t₃ ⟷ t₄} →
          (c₁ ⇔ c₃) → (c₂ ⇔ c₄) → (c₁ ⊗ c₂) ⇔ (c₃ ⊗ c₄)

-- better syntax for writing 2paths

infix  2  _▤
infixr 2  _⇔⟨_⟩_

_⇔⟨_⟩_ : {t₁ t₂ : U} (c₁ : t₁ ⟷ t₂) {c₂ : t₁ ⟷ t₂} {c₃ : t₁ ⟷ t₂} →
         (c₁ ⇔ c₂) → (c₂ ⇔ c₃) → (c₁ ⇔ c₃)
_ ⇔⟨ α ⟩ β = trans⇔ α β

_▤ : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → (c ⇔ c)
_▤ c = id⇔

-- Inverses for 2paths

2! : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ⇔ c₂) → (c₂ ⇔ c₁)
2! assoc◎l = assoc◎r
2! assoc◎r = assoc◎l
2! assoc⊕l = assoc⊕r
2! assoc⊕r = assoc⊕l
2! assoc⊗l = assoc⊗r
2! assoc⊗r = assoc⊗l
2! dist⇔ = factor⇔
2! factor⇔ = dist⇔
2! idl◎l = idl◎r
2! idl◎r = idl◎l
2! idr◎l = idr◎r
2! idr◎r = idr◎l
2! linv◎l = linv◎r
2! linv◎r = linv◎l
2! rinv◎l = rinv◎r
2! rinv◎r = rinv◎l
2! unitel₊⇔ = uniter₊⇔
2! uniter₊⇔ = unitel₊⇔
2! unitil₊⇔ = unitir₊⇔
2! unitir₊⇔ = unitil₊⇔
2! swapl₊⇔ = swapr₊⇔
2! swapr₊⇔ = swapl₊⇔
2! unitial₊⇔ = unitiar₊⇔
2! unitiar₊⇔ = unitial₊⇔
2! unitel⋆⇔ = uniter⋆⇔
2! uniter⋆⇔ = unitel⋆⇔
2! unitil⋆⇔ = unitir⋆⇔
2! unitir⋆⇔ = unitil⋆⇔
2! unitial⋆⇔ = unitiar⋆⇔
2! unitiar⋆⇔ = unitial⋆⇔
2! swapl⋆⇔ = swapr⋆⇔
2! swapr⋆⇔ = swapl⋆⇔
2! swapfl⋆⇔ = swapfr⋆⇔
2! swapfr⋆⇔ = swapfl⋆⇔
2! id⇔ = id⇔
2! (trans⇔ α β) = trans⇔ (2! β) (2! α)
2! (resp◎⇔ α β) = resp◎⇔ (2! α) (2! β)
2! (resp⊕⇔ α β) = resp⊕⇔ (2! α) (2! β)
2! (resp⊗⇔ α β) = resp⊗⇔ (2! α) (2! β)

-- a nice example of 2 paths

negEx : uniti⋆ ◎ (swap⋆ ◎ ((swap₊ {ONE} {ONE} ⊗ id⟷) ◎ (swap⋆ ◎ unite⋆)))
        ⇔ swap₊
negEx = uniti⋆ ◎ (swap⋆ ◎ ((swap₊ ⊗ id⟷) ◎ (swap⋆ ◎ unite⋆)))
          ⇔⟨ resp◎⇔ id⇔ assoc◎l ⟩
        uniti⋆ ◎ ((swap⋆ ◎ (swap₊ ⊗ id⟷)) ◎ (swap⋆ ◎ unite⋆))
          ⇔⟨ resp◎⇔ id⇔ (resp◎⇔ swapl⋆⇔ id⇔) ⟩
        uniti⋆ ◎ (((id⟷ ⊗ swap₊) ◎ swap⋆) ◎ (swap⋆ ◎ unite⋆))
          ⇔⟨ resp◎⇔ id⇔ assoc◎r ⟩
        uniti⋆ ◎ ((id⟷ ⊗ swap₊) ◎ (swap⋆ ◎ (swap⋆ ◎ unite⋆)))
          ⇔⟨ resp◎⇔ id⇔ (resp◎⇔ id⇔ assoc◎l) ⟩
        uniti⋆ ◎ ((id⟷ ⊗ swap₊) ◎ ((swap⋆ ◎ swap⋆) ◎ unite⋆))
          ⇔⟨ resp◎⇔ id⇔ (resp◎⇔ id⇔ (resp◎⇔ linv◎l id⇔)) ⟩
        uniti⋆ ◎ ((id⟷ ⊗ swap₊) ◎ (id⟷ ◎ unite⋆))
          ⇔⟨ resp◎⇔ id⇔ (resp◎⇔ id⇔ idl◎l) ⟩
        uniti⋆ ◎ ((id⟷ ⊗ swap₊) ◎ unite⋆)
          ⇔⟨ assoc◎l ⟩
        (uniti⋆ ◎ (id⟷ ⊗ swap₊)) ◎ unite⋆
          ⇔⟨ resp◎⇔ unitil⋆⇔ id⇔ ⟩
        (swap₊ ◎ uniti⋆) ◎ unite⋆
          ⇔⟨ assoc◎r ⟩
        swap₊ ◎ (uniti⋆ ◎ unite⋆)
          ⇔⟨ resp◎⇔ id⇔ linv◎l ⟩
        swap₊ ◎ id⟷
          ⇔⟨ idr◎l ⟩
        swap₊ ▤

-- The equivalence ⇔ of paths is rich enough to make U a 1groupoid:
-- the points are types (t : U); the 1paths are ⟷; and the 2paths
-- between them are based on the simplification rules ⇔

G' : 1Groupoid
G' = record
        { set = U
        ; _↝_ = _⟷_
        ; _≈_ = _⇔_
        ; id  = id⟷
        ; _∘_ = λ p q → q ◎ p
        ; _⁻¹ = !
        ; lneutr = λ _ → idr◎l
        ; rneutr = λ _ → idl◎l
        ; assoc  = λ _ _ _ → assoc◎l
        ; equiv = record {
            refl  = id⇔
          ; sym   = 2!
          ; trans = trans⇔
          }
        ; linv = λ {t₁} {t₂} α → linv◎l
        ; rinv = λ {t₁} {t₂} α → rinv◎l
        ; ∘-resp-≈ = λ p∼q r∼s → resp◎⇔ r∼s p∼q
        }

------------------------------------------------------------------------------
-- Soundness and completeness

-- The idea is to invert evaluation and use that to extract from each
-- extensional representation of a combinator, a canonical syntactic
-- representative

canonical : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂)
canonical c = perm2c (size≡ c , c2perm c)

-- Check canonical NOT = canonical NEG1 = canonical NEG2 = canonical NEG3
-- = canonical NEG4 = canonical NEG5

canonicalEx : Bool
canonicalEx =
  let x = canonical NOT in
  comb= x (canonical NEG1) ∧
  comb= x (canonical NEG2) ∧
  comb= x (canonical NEG3) ∧
  comb= x (canonical NEG4) ∧
  comb= x (canonical NEG5)

-- Proof of soundness and completeness: now we want to verify that ⇔
-- is sound and complete with respect to ∼. The statement to prove is
-- that for all c₁ and c₂, we have c₁ ∼ c₂ iff c₁ ⇔ c₂

assoc⊕∼ : {t₁ t₂ t₃ t₄ t₅ t₆ : U} {c₁ : t₁ ⟷ t₂} {c₂ : t₃ ⟷ t₄} {c₃ : t₅ ⟷ t₆} →
  subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅)) (c2cauchy ((c₁ ⊕ c₂) ⊕ c₃))
  ≡ c2cauchy (c₁ ⊕ (c₂ ⊕ c₃))
assoc⊕∼ {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃} =
  begin (subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
           (mapV
             (inject+ (size t₅))
             (mapV (inject+ (size t₃)) (c2cauchy c₁) ++V
              mapV (raise (size t₁)) (c2cauchy c₂))
            ++V mapV (raise (size t₁ + size t₃)) (c2cauchy c₃))
        ≡⟨ cong
             (λ x →
               subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
                 (x ++V mapV (raise (size t₁ + size t₃)) (c2cauchy c₃)))
             (map-++-commute
               (inject+ (size t₅))
               (mapV (inject+ (size t₃)) (c2cauchy c₁))) ⟩
         subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
           ((mapV (inject+ (size t₅)) (mapV (inject+ (size t₃)) (c2cauchy c₁)) ++V
             mapV (inject+ (size t₅)) (mapV (raise (size t₁)) (c2cauchy c₂)))
            ++V mapV (raise (size t₁ + size t₃)) (c2cauchy c₃))
        ≡⟨ cong
             (λ x →
               subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
                 (x ++V mapV (raise (size t₁ + size t₃)) (c2cauchy c₃)))
             (cong₂ _++V_
               (sym (map-∘ (inject+ (size t₅)) (inject+ (size t₃)) (c2cauchy c₁)))
               (sym (map-∘ (inject+ (size t₅)) (raise (size t₁)) (c2cauchy c₂)))) ⟩
         subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
           ((mapV (inject+ (size t₅) ∘ inject+ (size t₃)) (c2cauchy c₁) ++V
             mapV (inject+ (size t₅) ∘ raise (size t₁)) (c2cauchy c₂))
            ++V mapV (raise (size t₁ + size t₃)) (c2cauchy c₃))
        ≡⟨ {!!} ⟩
         (subst
           (λ x → Vec (Fin x) (size t₁))
           (+-assoc (size t₁) (size t₃) (size t₅))
           (mapV (inject+ (size t₅) ∘ inject+ (size t₃)) (c2cauchy c₁))) ++V
         ((subst
            (λ x → Vec (Fin x) (size t₃))
            (+-assoc (size t₁) (size t₃) (size t₅))
            (mapV (inject+ (size t₅) ∘ raise (size t₁)) (c2cauchy c₂))) ++V
          (subst
            (λ x → Vec (Fin x) (size t₅))
            (+-assoc (size t₁) (size t₃) (size t₅))
            (mapV (raise (size t₁ + size t₃)) (c2cauchy c₃))))
        ≡⟨ {!!} ⟩
         mapV (inject+ (size t₃ + size t₅)) (c2cauchy c₁) ++V
         (mapV (raise (size t₁) ∘ inject+ (size t₅)) (c2cauchy c₂) ++V
          mapV (raise (size t₁) ∘ raise (size t₃)) (c2cauchy c₃))
        ≡⟨ cong
             (λ x → mapV (inject+ (size t₃ + size t₅)) (c2cauchy c₁) ++V x)
             (cong₂ _++V_
               (map-∘ (raise (size t₁)) (inject+ (size t₅)) (c2cauchy c₂))
               (map-∘ (raise (size t₁)) (raise (size t₃)) (c2cauchy c₃))) ⟩
         mapV (inject+ (size t₃ + size t₅)) (c2cauchy c₁) ++V
         (mapV (raise (size t₁)) (mapV (inject+ (size t₅)) (c2cauchy c₂)) ++V
          mapV (raise (size t₁)) (mapV (raise (size t₃)) (c2cauchy c₃)))
        ≡⟨ cong
             (λ x → mapV (inject+ (size t₃ + size t₅)) (c2cauchy c₁) ++V x)
             (sym (map-++-commute
                    (raise (size t₁))
                    (mapV (inject+ (size t₅)) (c2cauchy c₂)))) ⟩
         mapV (inject+ (size t₃ + size t₅)) (c2cauchy c₁) ++V
         (mapV (raise (size t₁))
           (mapV (inject+ (size t₅)) (c2cauchy c₂) ++V
            mapV (raise (size t₃)) (c2cauchy c₃)))
        ≡⟨ refl ⟩
         pcompcauchy (c2cauchy c₁) (pcompcauchy (c2cauchy c₂) (c2cauchy c₃)) ∎)
  where open ≡-Reasoning

soundness : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ⇔ c₂) → (c₁ ∼ c₂)
soundness (assoc◎l {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃}) =
  assoc∼ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃}
soundness (assoc◎r {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃}) =
  sym (assoc∼ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃})
soundness (assoc⊕l {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) =
  begin (c2cauchy (c₁ ⊕ (c₂ ⊕ c₃))
       ≡⟨ sym (assoc⊕∼ {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) ⟩
         subst Cauchy (+-assoc (size t₁) (size t₃) (size t₅))
           (c2cauchy {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃))
       ≡⟨ sym (scomprid _) ⟩
       scompcauchy
         (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
           (c2cauchy {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃)))
         (idcauchy (size t₁ + (size t₃ + size t₅)))
       ≡⟨ cong
            (scompcauchy
              (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
                (c2cauchy
                  {PLUS (PLUS t₁ t₃) t₅}
                  {PLUS (PLUS t₂ t₄) t₆}
                  ((c₁ ⊕ c₂) ⊕ c₃))))
            (sym (congD! idcauchy (size≡! (assocl₊ {t₁} {t₃} {t₅})))) ⟩
       scompcauchy
         (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
           (c2cauchy {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃)))
         (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
           (idcauchy ((size t₁ + size t₃) + size t₅)))
       ≡⟨ cong
            (λ x →
             scompcauchy
              (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
                (c2cauchy
                  {PLUS (PLUS t₁ t₃) t₅}
                  {PLUS (PLUS t₂ t₄) t₆}
                  ((c₁ ⊕ c₂) ⊕ c₃)))
              (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅})) x))
            (sym (congD! idcauchy (size≡! ((c₁ ⊕ c₂) ⊕ c₃)))) ⟩
       scompcauchy
         (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
           (c2cauchy {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃)))
         (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
           (subst Cauchy (size≡! ((c₁ ⊕ c₂) ⊕ c₃))
             (idcauchy ((size t₂ + size t₄) + size t₆))))
       ≡⟨ sym (subst-dist scompcauchy (size≡! (assocl₊ {t₁} {t₃} {t₅})) _ _) ⟩
       subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
         (scompcauchy
           (c2cauchy {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃))
           (subst Cauchy (size≡! ((c₁ ⊕ c₂) ⊕ c₃))
             (idcauchy ((size t₂ + size t₄) + size t₆))))
       ≡⟨ sym (scomplid _) ⟩
         scompcauchy
           (idcauchy (size t₁ + (size t₃ + size t₅)))
           (subst Cauchy (size≡! (assocl₊ {t₁} {t₃} {t₅}))
             (scompcauchy
               (c2cauchy
                  {PLUS (PLUS t₁ t₃) t₅} {PLUS (PLUS t₂ t₄) t₆} ((c₁ ⊕ c₂) ⊕ c₃))
               (subst Cauchy (size≡! ((c₁ ⊕ c₂) ⊕ c₃))
                (idcauchy ((size t₂ + size t₄) + size t₆)))))
       ≡⟨ refl ⟩
         c2cauchy (assocl₊ ◎ (((c₁ ⊕ c₂) ⊕ c₃) ◎ assocr₊)) ∎)
  where open ≡-Reasoning
soundness (assoc⊕r {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) = {!!}
soundness (assoc⊗l {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) = {!!}
soundness (assoc⊗r {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) = {!!}
soundness (dist⇔ {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) = {!!}
soundness (factor⇔ {t₁} {t₂} {t₃} {t₄} {t₅} {t₆} {c₁} {c₂} {c₃}) = {!!}
soundness (idl◎l {t₁} {t₂} {c}) = id◎c∼c {t₁} {t₂} {c}
soundness (idl◎r {t₁} {t₂} {c}) = sym (id◎c∼c {t₁} {t₂} {c})
soundness (idr◎l {t₁} {t₂} {c}) = c◎id∼c {t₁} {t₂} {c}
soundness (idr◎r {t₁} {t₂} {c}) = sym (c◎id∼c {t₁} {t₂} {c})
soundness (linv◎l {t₁} {t₂} {c}) = linv∼ {t₁} {t₂} {c}
soundness (linv◎r {t₁} {t₂} {c}) = sym (linv∼ {t₁} {t₂} {c})
soundness (rinv◎l {t₁} {t₂} {c})  = rinv∼ {t₁} {t₂} {c}
soundness (rinv◎r {t₁} {t₂} {c})  = sym (rinv∼ {t₁} {t₂} {c})
soundness (unitel₊⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (uniter₊⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitil₊⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitir₊⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitial₊⇔ {t₁} {t₂}) = {!!}
soundness (unitiar₊⇔ {t₁} {t₂}) = {!!}
soundness (swapl₊⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂}) = {!!}
soundness (swapr₊⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂}) = {!!}
soundness (unitel⋆⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (uniter⋆⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitil⋆⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitir⋆⇔ {t₁} {t₂} {c₁} {c₂}) = {!!}
soundness (unitial⋆⇔ {t₁} {t₂}) = {!!}
soundness (unitiar⋆⇔ {t₁} {t₂}) = {!!}
soundness (swapl⋆⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂}) = {!!}
soundness (swapr⋆⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂}) = {!!}
soundness (swapfl⋆⇔ {t₁} {t₂} {t₃}) = {!!}
soundness (swapfr⋆⇔ {t₁} {t₂} {t₃}) = {!!}
soundness (id⇔ {t₁} {t₂} {c}) = refl∼ {t₁} {t₂} {c}
soundness (trans⇔ {t₁} {t₂} {c₁} {c₂} {c₃} α β) =
  trans∼ {t₁} {t₂} {c₁} {c₂} {c₃} (soundness α) (soundness β)
soundness (resp◎⇔ {t₁} {t₂} {t₃} {c₁} {c₃} {c₂} {c₄} α β) =
  resp∼ {t₁} {t₂} {t₃} {c₁} {c₂} {c₃} {c₄} (soundness α) (soundness β)
soundness (resp⊕⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃} {c₄} α β) = {!!}
soundness (resp⊗⇔ {t₁} {t₂} {t₃} {t₄} {c₁} {c₂} {c₃} {c₄} α β) = {!!}

-- If we can prove that every combinator is equal to its normal form
-- then we can prove completeness.

inversion : {t₁ t₂ : U} (c : t₁ ⟷ t₂) → canonical c ⇔ c
inversion (c₁ ◎ c₂) = {!!}
inversion {PLUS ZERO t} {.t} unite₊ = {!!}
inversion {t} {PLUS ZERO .t} uniti₊ = {!!}
inversion {PLUS t₁ t₂} {PLUS .t₂ .t₁} swap₊ = {!!}
inversion {PLUS t₁ (PLUS t₂ t₃)} {PLUS (PLUS .t₁ .t₂) .t₃} assocl₊ = {!!}
inversion {PLUS (PLUS t₁ t₂) t₃} {PLUS .t₁ (PLUS .t₂ .t₃)} assocr₊ = {!!}
inversion {TIMES ONE t} {.t} unite⋆ = {!!}
inversion {t} {TIMES ONE .t} uniti⋆ = {!!}
inversion {TIMES t₁ t₂} {TIMES .t₂ .t₁} swap⋆ = {!!}
inversion {TIMES t₁ (TIMES t₂ t₃)} {TIMES (TIMES .t₁ .t₂) .t₃} assocl⋆ = {!!}
inversion {TIMES (TIMES t₁ t₂) t₃} {TIMES .t₁ (TIMES .t₂ .t₃)} assocr⋆ = {!!}
inversion {TIMES .ZERO t} {ZERO} distz = {!!}
inversion {ZERO} {TIMES ZERO t} factorz = {!!}
inversion {TIMES (PLUS t₁ t₂) t₃} {PLUS (TIMES .t₁ .t₃) (TIMES .t₂ .t₃)} dist = {!!}
inversion {PLUS (TIMES t₁ t₃) (TIMES t₂ .t₃)} {TIMES (PLUS .t₁ .t₂) .t₃} factor = {!!}
inversion {t} {.t} id⟷ =
  canonical id⟷
    ⇔⟨ id⇔ ⟩
  normalizeC t ◎
  transposition*2c (size t) (size t) refl (cauchy→transposition* (idcauchy (size t))) ◎
  ! (normalizeC t)
    ⇔⟨ {!!} ⟩
  normalizeC t ◎ id⟷ ◎ ! (normalizeC t)
    ⇔⟨ resp◎⇔ id⇔ idl◎l ⟩
  normalizeC t ◎ ! (normalizeC t)
    ⇔⟨ linv◎l ⟩
  id⟷ ▤
inversion {PLUS t₁ t₂} {PLUS t₃ t₄} (c₁ ⊕ c₂) = {!!}
inversion {TIMES t₁ t₂} {TIMES t₃ t₄} (c₁ ⊗ c₂) = {!!}
inversion {PLUS ONE ONE} {BOOL} foldBool = {!!}
{--
canonical foldBool =
  ((uniti₊ ◎ swap₊ ⊕ uniti₊ ◎ swap₊) ◎ assocr₊ ◎ (id⟷ ⊕ unite₊)) ◎
  (id⟷ ◎ (id⟷ ⊕ id⟷) ◎ id⟷) ◎
  (((id⟷ ⊕ uniti₊) ◎ assocl₊) ◎ (swap₊ ◎ unite₊ ⊕ swap₊ ◎ unite₊)) ◎
  foldBool
--}
inversion {BOOL} {PLUS ONE ONE} unfoldBool = {!!}

resp≡⇔ : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ≡ c₂) → (c₁ ⇔ c₂)
resp≡⇔ {t₁} {t₂} {c₁} {c₂} p rewrite p = id⇔

completeness : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ∼ c₂) → (c₁ ⇔ c₂)
completeness {t₁} {t₂} {c₁} {c₂} c₁∼c₂ =
  c₁
    ⇔⟨ 2! (inversion c₁) ⟩
  canonical c₁
    ⇔⟨ resp≡⇔ {!!} ⟩
  canonical c₂
    ⇔⟨ inversion c₂ ⟩
  c₂ ▤

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.Word
open import lib.groups.GeneratedAbelianGroup
open import lib.groups.GeneratedGroup
open import lib.groups.GroupProduct
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.FreeAbelianGroup {i} where

module FreeAbelianGroup (A : Type i) where

  private
    module Gen = GeneratedAbelianGroup A empty-rel
  open Gen hiding (GenAbGroup; module HomomorphismEquiv) public

  CommutativityRel : Rel (Word A) i
  CommutativityRel = AbGroupRel

  FormalSumRel : Rel (Word A) i
  FormalSumRel = QuotWordRel

  FormalSum : Type i
  FormalSum = QuotWord

  FreeGroup : Group i
  FreeGroup = Gen.GenGroup

  FreeAbGroup : AbGroup i
  FreeAbGroup = Gen.GenAbGroup

  module FreeAbGroup = AbGroup FreeAbGroup

  {- Universal Property -}
  module Freeness {j} (G : AbGroup j) where

    private
      module G = AbGroup G

    extend-equiv : (A → G.El) ≃ (FreeAbGroup.grp →ᴳ G.grp)
    extend-equiv =
      Gen.HomomorphismEquiv.extend-equiv G ∘e every-function-respects-empty-rel-equiv A G.grp

    extend : (A → G.El) → (FreeAbGroup.grp →ᴳ G.grp)
    extend = –> extend-equiv

    extend-is-equiv : is-equiv extend
    extend-is-equiv = snd extend-equiv

    extend-hom : Πᴳ A (λ _ → G.grp) →ᴳ hom-group FreeAbGroup.grp G
    extend-hom = record {M} where
      module M where
        f : (A → G.El) → (FreeAbGroup.grp →ᴳ G.grp)
        f = extend
        abstract
          pres-comp : preserves-comp (Group.comp (Πᴳ A (λ _ → G.grp))) (Group.comp (hom-group FreeAbGroup.grp G)) f
          pres-comp = λ f₁ f₂ → group-hom= $ λ= $
            QuotWord-elim
              (Word-extendᴳ-comp G f₁ f₂)
              (λ _ → prop-has-all-paths-↓)

    extend-iso : Πᴳ A (λ _ → G.grp) ≃ᴳ hom-group FreeAbGroup.grp G
    extend-iso = extend-hom , snd extend-equiv

ext: agda

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

module Categories.Enriched.Over.One where

open import Level

open import Categories.Category.Monoidal.Instance.One
open import Categories.Enriched.Category

TruthValue : (o ℓ e t : Level) → Set (o ⊔ ℓ ⊔ e ⊔ suc t)
TruthValue o ℓ e t = Category (One-Monoidal {o} {ℓ} {e}) t

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K --safe #-}
module Util.HoTT.Equiv.Core where

open import Util.Prelude
open import Util.HoTT.HLevel.Core

infix 4 _≅_ _≃_

private
  variable
    α β γ : Level
    A B C : Set α

Injective : (f : A → B) → Set _
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

record IsIso {A : Set α} {B : Set β} (forth : A → B) : Set (α ⊔ℓ β)
  where
  field
    back : B → A
    back∘forth : ∀ x → back (forth x) ≡ x
    forth∘back : ∀ x → forth (back x) ≡ x

record _≅_ (A : Set α) (B : Set β) : Set (α ⊔ℓ β) where
  field
    forth : A → B
    isIso : IsIso forth

  open IsIso isIso public

open _≅_ public

IsEquiv : {A : Set α} {B : Set β} (forth : A → B)
  → Set (α ⊔ℓ β)
IsEquiv {A = A} {B} forth
  = ∀ b → IsContr (Σ[ a ∈ A ] forth a ≡ b)

record _≃_ (A : Set α) (B : Set β) : Set (α ⊔ℓ β) where
  field
    forth : A → B
    isEquiv : IsEquiv forth

open _≃_ public

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Nat where

data Nat : Set

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

plus : Nat -> Nat -> Nat
plus zero    n = n
plus (suc m) n = suc (plus m n)

elim : (P : (n : Nat) -> Set) ->
       (z : P (plus zero zero)) ->
       (s : (n : Nat) -> P (plus zero n) -> P (plus (suc zero) n)) ->
       (n : Nat) -> P n
elim P z s zero    = z
elim P z s (suc n) = s n (elim P z s n)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Oscar.Category where

open import Oscar.Level
open import Oscar.Function

record Setoid {𝔬} (𝔒 : Ø 𝔬) 𝔮 : Ø 𝔬 ∙̂ ↑̂ 𝔮 where
  infix 4 _≋_
  field
    _≋_ : 𝔒 → 𝔒 → Ø 𝔮
    ≋-reflexivity : ∀ {x} → x ≋ x
    ≋-symmetry : ∀ {x y} → x ≋ y → y ≋ x
    ≋-transitivity : ∀ {x y} → x ≋ y → ∀ {z} → y ≋ z → x ≋ z

record Semigroupoid
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} (𝔐 : 𝔒 → 𝔒 → Ø 𝔪)
  {𝔮} (𝔐-setoid : ∀ {x y} → Setoid (𝔐 x y) 𝔮)
  : Ø 𝔬 ∙̂ 𝔪 ∙̂ 𝔮 where
  instance _ = λ {x y} → 𝔐-setoid {x} {y}
  open Setoid ⦃ … ⦄ using (_≋_)
  infixr 9 _∙_
  field
    _∙_ : ∀ {y z} → 𝔐 y z → ∀ {x} → 𝔐 x y → 𝔐 x z
    ∙-extensionality : ∀ {x y} {f₁ f₂ : 𝔐 x y} → f₁ ≋ f₂ → ∀ {z} {g₁ g₂ : 𝔐 y z} → g₁ ≋ g₂ → g₁ ∙ f₁ ≋ g₂ ∙ f₂
    ∙-associativity : ∀ {w x} (f : 𝔐 w x) {y} (g : 𝔐 x y) {z} (h : 𝔐 y z) → (h ∙ g) ∙ f ≋ h ∙ (g ∙ f)

record Category
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔪} {𝔐 : 𝔒 → 𝔒 → Ø 𝔪}
  {𝔮} {𝔐-setoid : ∀ {x y} → Setoid (𝔐 x y) 𝔮}
  (semigroupoid : Semigroupoid 𝔐 𝔐-setoid)
  : Ø 𝔬 ∙̂ 𝔪 ∙̂ 𝔮 where
  instance _ = λ {x y} → 𝔐-setoid {x} {y}
  open Setoid ⦃ … ⦄ using (_≋_)
  open Semigroupoid semigroupoid using (_∙_)
  field
    ε : ∀ {x} → 𝔐 x x
    ε-left-identity : ∀ {x y} {f : 𝔐 x y} → ε ∙ f ≋ f
    ε-right-identity : ∀ {x y} {f : 𝔐 x y} → f ∙ ε ≋ f

record Semifunctor
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔪₁} {𝔐₁ : 𝔒₁ → 𝔒₁ → Ø 𝔪₁}
  {𝔮₁} {𝔐₁-setoid : ∀ {x y} → Setoid (𝔐₁ x y) 𝔮₁}
  (semigroupoid₁ : Semigroupoid 𝔐₁ 𝔐₁-setoid)
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔪₂} {𝔐₂ : 𝔒₂ → 𝔒₂ → Ø 𝔪₂}
  {𝔮₂} {𝔐₂-setoid : ∀ {x y} → Setoid (𝔐₂ x y) 𝔮₂}
  (semigroupoid₂ : Semigroupoid 𝔐₂ 𝔐₂-setoid)
  : Ø 𝔬₁ ∙̂ 𝔪₁ ∙̂ 𝔮₁ ∙̂ 𝔬₂ ∙̂ 𝔪₂ ∙̂ 𝔮₂
  where
  instance _ = λ {x y} → 𝔐₁-setoid {x} {y}
  instance _ = λ {x y} → 𝔐₂-setoid {x} {y}
  open Setoid ⦃ … ⦄ using (_≋_)
  module ⒈ = Semigroupoid semigroupoid₁
  module ⒉ = Semigroupoid semigroupoid₂
  field
    {μ} : 𝔒₁ → 𝔒₂
    𝔣 : ∀ {x y} → 𝔐₁ x y → 𝔐₂ (μ x) (μ y)
    𝔣-extensionality : ∀ {x y} → {f₁ f₂ : 𝔐₁ x y} → f₁ ≋ f₂ → 𝔣 f₁ ≋ 𝔣 f₂
    𝔣-commutativity : ∀ {x y} {f : 𝔐₁ x y} {z} {g : 𝔐₁ y z} → 𝔣 (g ⒈.∙ f) ≋ 𝔣 g ⒉.∙ 𝔣 f

record Functor
  {𝔬₁} {𝔒₁ : Ø 𝔬₁}
  {𝔪₁} {𝔐₁ : 𝔒₁ → 𝔒₁ → Ø 𝔪₁}
  {𝔮₁} {𝔐₁-setoid : ∀ {x y} → Setoid (𝔐₁ x y) 𝔮₁}
  {semigroupoid₁ : Semigroupoid 𝔐₁ 𝔐₁-setoid}
  {𝔬₂} {𝔒₂ : Ø 𝔬₂}
  {𝔪₂} {𝔐₂ : 𝔒₂ → 𝔒₂ → Ø 𝔪₂}
  {𝔮₂} {𝔐₂-setoid : ∀ {x y} → Setoid (𝔐₂ x y) 𝔮₂}
  {semigroupoid₂ : Semigroupoid 𝔐₂ 𝔐₂-setoid}
  (semifunctor : Semifunctor semigroupoid₁ semigroupoid₂)
  (category₁ : Category semigroupoid₁)
  (category₂ : Category semigroupoid₂)
  : Ø 𝔬₁ ∙̂ 𝔪₁ ∙̂ 𝔮₁ ∙̂ 𝔬₂ ∙̂ 𝔪₂ ∙̂ 𝔮₂
  where
  instance _ = λ {x y} → 𝔐₂-setoid {x} {y}
  open Setoid ⦃ … ⦄ using (_≋_)
  open Semifunctor semifunctor using (𝔣; μ)
  module ⒈ = Category category₁
  module ⒉ = Category category₂
  field
    𝔣-identity : ∀ {x : 𝔒₁} → 𝔣 (⒈.ε {x = x}) ≋ (⒉.ε {x = μ x})


text:
module consoleExamples.simpleLoop where

open import ConsoleLib
open import Data.Bool renaming (not to ¬)
open import Data.String hiding (_==_)
open import SizedIO.Base
open import Size

-- the following program asks the user for an input, which is a string.
-- It converts this string into a Boolean value (by mapping "true" to true and
--    "false" to false), applies Boolean negation to the result
-- and then converts the resulting Boolean value back to a string

boolStrInput2Bool : String → Bool
boolStrInput2Bool s = s ==str "true"

checkStrBoolInput : String → Bool
checkStrBoolInput s = (s ==str "true") ∨ (s ==str "false")

bool2Str : Bool → String
bool2Str true = "true"
bool2Str false = "false"

-- when writing a recursive program you need to write first the body
-- as an element of IOConsole
-- and apply an eliminator to it, followed by a a function which
--  results in an element of IOConsole'
-- otherwise the recursion would unfold and you get an infinite term
--
-- The functions WriteString+ and ReadLine+  which need the continuing program
--   as argument can be used to create elements of IOConsole'
--
-- Furthermore after applying a size argument (i which is of type Size)
--  the termination checker can figure out that your definition is productive
--  i.e. has at least one interaction before carrying out the recursion.

mainBody : ∀{i} → IOConsole i  Unit
force (mainBody) = WriteString+ "Enter true or false"
                   (GetLine >>= λ s →
                    if   (checkStrBoolInput s)
                    then (WriteString ("Result of negating your input is " ++
                                       bool2Str (¬ (boolStrInput2Bool s))) >>= λ _ →
                          mainBody)
                     else
                       (WriteString ("Please enter \"true\" or \"false\"") >>= λ _ →
                       mainBody))

main : ConsoleProg
main = run mainBody

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module DoBlock3 where

data Id
  (A : Set)
  : Set
  where

  id
    : A
    → Id A

_>>=_
  : {A B : Set}
  → Id A
  → (A → Id B)
  → Id B
id x >>= f
  = f x

_>>_
  : {A B : Set}
  → Id A
  → Id B
  → Id B
_ >> y
  = y

f
  : {A : Set}
  → A
  → Id A
f x
  = do
    id x
    id x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module Numeral.Natural.UnclosedOper where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Data.Option as Option using (Option)
open import Data.Option.Functions as Option
open import Logic.Propositional
open import Numeral.Finite as 𝕟
  using (𝕟)
import      Numeral.Finite.Bound as 𝕟bound
open import Numeral.Integer as ℤ
  using (ℤ)
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Decidable
open import Numeral.Natural.Relation.Order.Proofs
import      Numeral.Sign as Sign
open import Type.Properties.Decidable.Proofs

infix  10010 _−_

-- TODO _/_ : ℕ → ℕ → ℚ

-- Unclosed total subtraction from natural numbers to an optional natural number.
-- When the subtraction gives a negative number semantically, this operation gives Option.None.
_−?_ : ℕ → ℕ → Option(ℕ)
a    −? 𝟎    = Option.Some(a)
𝟎    −? 𝐒(b) = Option.None
𝐒(a) −? 𝐒(b) = a −? b

-- Unclosed total floored division
{-# TERMINATING #-}
_⌊/₀⌋_ : ℕ → ℕ → ℕ
𝐒(x) ⌊/₀⌋ 𝐒(y) with (𝐒(x) −? 𝐒(y))
... | Option.Some(𝐒x𝐒y) = 𝐒(𝐒x𝐒y ⌊/₀⌋ 𝐒(y))
... | Option.None       = 𝟎
{-# CATCHALL #-}
_    ⌊/₀⌋ _    = 𝟎

-- Unclosed total subtraction from natural numbers to an optional natural number.
-- When dividing by 0, this operation gives Option.None.
{-# TERMINATING #-}
_⌊/⌋?_ : ℕ → ℕ → Option(ℕ)
_    ⌊/⌋? 𝟎    = Option.None
𝟎    ⌊/⌋? 𝐒(_) = Option.Some(𝟎)
𝐒(x) ⌊/⌋? 𝐒(y) with (𝐒(x) −? 𝐒(y))
... | Option.Some(𝐒x𝐒y) = Option.map 𝐒(𝐒x𝐒y ⌊/⌋? 𝐒(y))
... | Option.None       = Option.Some(𝟎)

-- Unclosed total subtraction from natural numbers to an optional natural number.
-- When dividing by 0 or the division gives a rational number semantically, this operation gives Option.None.
{-# TERMINATING #-}
_/?_ : ℕ → ℕ → Option(ℕ)
_    /? 𝟎    = Option.None
𝟎    /? 𝐒(_) = Option.Some(𝟎)
𝐒(x) /? 𝐒(y) with (𝐒(x) −? 𝐒(y))
... | Option.Some(𝐒x𝐒y) = Option.map 𝐒(𝐒x𝐒y /? 𝐒(y))
... | Option.None       = Option.None

-- Unclosed total subtraction from natural numbers to finite natural numbers
_−₀fin_ : (x : ℕ) → ℕ → 𝕟(𝐒(x))
𝟎    −₀fin _    = 𝕟.𝟎
𝐒(x) −₀fin 𝟎    = 𝕟.𝐒(x −₀fin 𝟎)
𝐒(x) −₀fin 𝐒(y) = 𝕟bound.bound-𝐒 (x −₀fin y)

-- Unclosed total subtraction from a natural number and a finite natural number to a finite natural number
_−fin_ : (x : ℕ) → 𝕟(𝐒(x)) → 𝕟(𝐒(x))
𝟎    −fin 𝕟.𝟎    = 𝕟.𝟎
𝐒(x) −fin 𝕟.𝟎    = 𝕟.𝐒(x −fin 𝕟.𝟎)
𝐒(x) −fin 𝕟.𝐒(y) = 𝕟bound.bound-𝐒 (x −fin y)

-- Modulo operation to upper bounded natural numbers.
_modfin_ : ℕ → (b : ℕ) → ⦃ _ : IsTrue(b ≢? 𝟎) ⦄ → 𝕟(b)
a modfin 𝐒 b = 𝕟.ℕ-to-𝕟 (a mod 𝐒(b)) ⦃ [↔]-to-[→] decider-true (mod-maxᵣ{a}{𝐒 b}) ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import Type

module Structure.Operator.SetAlgebra {ℓ} (S : Type{ℓ}) where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Operator.Properties
open import Structure.Operator.Proofs
open import Structure.Relator.Properties
open import Syntax.Transitivity

record Fundamentals : Stmt{ℓ} where
  infixl 1001 _∩_
  infixl 1000 _∪_

  field
    _∪_ : S → S → S -- Union
    _∩_ : S → S → S -- Intersection
    ∅   : S         -- Empty set
    𝐔   : S         -- Universal set

  field -- TODO: This is two commutative monoids with distributivity over each other
    ⦃ [∪]-commutativity ⦄ : Commutativity(_∪_)
    ⦃ [∩]-commutativity ⦄ : Commutativity(_∩_)

    ⦃ [∪]-associativity ⦄ : Associativity(_∪_)
    ⦃ [∩]-associativity ⦄ : Associativity(_∩_)

    ⦃ [∪][∩]-distributivityₗ ⦄ : Distributivityₗ(_∪_)(_∩_)
    ⦃ [∩][∪]-distributivityₗ ⦄ : Distributivityₗ(_∩_)(_∪_)

    ⦃ [∪]-identityₗ ⦄ : Identityₗ(_∪_)(∅)
    ⦃ [∩]-identityₗ ⦄ : Identityₗ(_∩_)(𝐔)

  instance
    [∪][∩]-distributivityᵣ : Distributivityᵣ(_∪_)(_∩_)
    [∪][∩]-distributivityᵣ = [↔]-to-[→] OneTypeTwoOp.distributivity-equivalence-by-commutativity [∪][∩]-distributivityₗ

  instance
    [∩][∪]-distributivityᵣ : Distributivityᵣ(_∩_)(_∪_)
    [∩][∪]-distributivityᵣ = [↔]-to-[→] OneTypeTwoOp.distributivity-equivalence-by-commutativity [∩][∪]-distributivityₗ

  instance
    [∪]-identityᵣ : Identityᵣ(_∪_)(∅)
    [∪]-identityᵣ = [↔]-to-[→] One.identity-equivalence-by-commutativity [∪]-identityₗ

  instance
    [∩]-identityᵣ : Identityᵣ(_∩_)(𝐔)
    [∩]-identityᵣ = [↔]-to-[→] One.identity-equivalence-by-commutativity [∩]-identityₗ

record Complement : Stmt{ℓ} where
  infixl 1002 ∁_
  infixl 1000 _∖_

  field
    ∁_   : S → S -- Complement

  field
    ⦃ fundamentals ⦄ : Fundamentals
  open Fundamentals(fundamentals)

  field -- TODO: Not really inverses. These are using the absorbers
    [∪]-inverseᵣ : ∀{s : S} → (s ∪ ∁(s) ≡ 𝐔)
    [∩]-inverseᵣ : ∀{s : S} → (s ∩ ∁(s) ≡ ∅)

  _∖_ : S → S → S -- Difference
  _∖_ (s₁)(s₂) = s₁ ∩ ∁(s₂)

  [∪]-inverseₗ : ∀{s : S} → (∁(s) ∪ s ≡ 𝐔)
  [∪]-inverseₗ = transitivity(_≡_) (commutativity(_∪_)) [∪]-inverseᵣ

  [∩]-inverseₗ : ∀{s : S} → (∁(s) ∩ s ≡ ∅)
  [∩]-inverseₗ = transitivity(_≡_) (commutativity(_∩_)) [∩]-inverseᵣ

  [∁]-of-[∅] : (∁(∅) ≡ 𝐔)
  [∁]-of-[∅] =
    symmetry(_≡_) (identityₗ(_∪_)(∅))
    🝖 ([∪]-inverseᵣ)

  [∁]-of-[𝐔] : (∁(𝐔) ≡ ∅)
  [∁]-of-[𝐔] =
    symmetry(_≡_) (identityₗ(_∩_)(𝐔))
    🝖 ([∩]-inverseᵣ)

  [∪]-idempotence : ∀{s : S} → (s ∪ s) ≡ s
  [∪]-idempotence{s} =
    ([≡]-intro)
    🝖 (symmetry(_≡_) (identityᵣ(_∩_)(𝐔)))
    🝖 ([≡]-with(expr ↦ ((s ∪ s) ∩ expr)) (symmetry(_≡_) [∪]-inverseᵣ))
    🝖 (symmetry(_≡_) (distributivityₗ(_∪_)(_∩_)))
    🝖 ([≡]-with(expr ↦ (s ∪ expr)) [∩]-inverseᵣ)
    🝖 ((identityᵣ(_∪_)(∅)))

  [∩]-idempotence : ∀{s : S} → (s ∩ s) ≡ s
  [∩]-idempotence{s} =
    ([≡]-intro)
    🝖 (symmetry(_≡_) (identityᵣ(_∪_)(∅)))
    🝖 ([≡]-with(expr ↦ ((s ∩ s) ∪ expr)) (symmetry(_≡_) [∩]-inverseᵣ))
    🝖 (symmetry(_≡_) (distributivityₗ(_∩_)(_∪_)))
    🝖 ([≡]-with(expr ↦ (s ∩ expr)) [∪]-inverseᵣ)
    🝖 ((identityᵣ(_∩_)(𝐔)))

  [∪]-absorber : ∀{s : S} → (s ∪ 𝐔) ≡ 𝐔
  [∪]-absorber{s} =
    ([≡]-with(expr ↦ s ∪ expr) (symmetry(_≡_) [∪]-inverseᵣ))
    🝖 (symmetry(_≡_) (associativity(_∪_)))
    🝖 ([≡]-with(expr ↦ expr ∪ ∁(s)) [∪]-idempotence)
    🝖 ([∪]-inverseᵣ)
    -- s∪𝐔 = s∪(s ∪ ∁(s)) = (s∪s) ∪ ∁(s) = s ∪ ∁(s) = 𝐔

  [∩]-absorber : ∀{s : S} → (s ∩ ∅) ≡ ∅
  [∩]-absorber{s} =
    ([≡]-with(expr ↦ s ∩ expr) (symmetry(_≡_) [∩]-inverseᵣ))
    🝖 (symmetry(_≡_) (associativity(_∩_)))
    🝖 ([≡]-with(expr ↦ expr ∩ ∁(s)) [∩]-idempotence)
    🝖 ([∩]-inverseᵣ)
    -- s∩∅ = s∩(s ∩ ∁(s)) = (s∩s) ∩ ∁(s) = s ∩ ∁(s) = ∅

  -- postulate [∪]-absorptionₗ : ∀{s₁ s₂ : S} → (s₁ ∪ (s₁ ∩ s₂)) ≡ s₁
    -- s₁∪(s₁∩s₂)
    -- = (s₁∪s₁)∩(s₁∪s₂)
    -- = s₁∩(s₁∪s₂)
    -- = (s₁∩s₁) ∪ (s₁∩s₂)
    -- = s₁ ∪ (s₁∩s₂)
    -- = ?
  -- postulate [∩]-absorptionₗ : ∀{s₁ s₂ : S} → (s₁ ∩ (s₁ ∪ s₂)) ≡ s₁

  -- ∁(s₁) ∪ ∁(s₁ ∪ s₂) = ∁(s₁)
  -- ∁(s₁) ∩ ∁(s₁ ∪ s₂) = ∁(s₁ ∪ s₂)
  -- ∁(s₁) ∪ ∁(s₁ ∩ s₂) = ∁(s₁ ∩ s₂)
  -- ∁(s₁) ∩ ∁(s₁ ∩ s₂) = ∁(s₁)

--    postulate a : ∀{a} → a

  -- postulate [∁]-of-[∪] : ∀{s₁ s₂ : S} → ∁(s₁ ∪ s₂) ≡ ∁(s₁) ∩ ∁(s₂)
  -- [∁]-of-[∪] =
    -- ((∁(s₁) ∩ ∁(s₂)) ∪ (s₁ ∪ s₂)) = 𝐔 ?

    -- (s₁ ∪ s₂) ∪ ∁(s₁ ∪ s₂) = 𝐔
    -- ∁(s₂) ∩ ((s₁ ∪ s₂) ∪ ∁(s₁ ∪ s₂)) = ∁(s₁) ∩ 𝐔
    -- (∁(s₂) ∩ (s₁ ∪ s₂)) ∪ (∁(s₁) ∩ ∁(s₁ ∪ s₂)) = ∁(s₂) ∩ 𝐔
    -- (∁(s₂) ∩ (s₁ ∪ s₂)) ∪ (∁(s₁) ∩ ∁(s₁ ∪ s₂)) = ∁(s₂) ∩ 𝐔
    -- (∁(s₂) ∩ (s₁ ∪ s₂)) ∪ (∁(s₁) ∩ ∁(s₁ ∪ s₂)) = ∁(s₂)
    -- ∁(s₂) = (∁(s₂) ∩ (s₁ ∪ s₂)) ∪ (∁(s₁) ∩ ∁(s₁ ∪ s₂))
    -- ∁(s₂) = ((∁(s₂) ∩ s₁) ∪ (∁(s₂) ∩ s₂)) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₂) = ((∁(s₂) ∩ s₁) ∪ ∅) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₂) = (∁(s₂) ∩ s₁) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = ∁(s₁) ∩ ((∁(s₂) ∩ s₁) ∪ ∁(s₁ ∪ s₂))
    -- ∁(s₁) ∩ ∁(s₂) = (∁(s₁) ∩ (∁(s₂) ∩ s₁)) ∪ (∁(s₁) ∩ ∁(s₁ ∪ s₂))
    -- ∁(s₁) ∩ ∁(s₂) = (∁(s₁) ∩ (∁(s₂) ∩ s₁)) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = (∁(s₁) ∩ (s₁ ∩ ∁(s₂))) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = ((∁(s₁) ∩ s₁) ∩ ∁(s₂)) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = (∅ ∩ ∁(s₂)) ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = ∅ ∪ ∁(s₁ ∪ s₂)
    -- ∁(s₁) ∩ ∁(s₂) = ∁(s₁ ∪ s₂)

    -- postulate proof1 : ∀{a b c d} → (a ∩ b) ∩ (c ∪ d) ≡ (a ∩ (b ∩ d)) ∪ (b ∩ (a ∩ c))
      -- (a ∩ b) ∩ (c ∪ d)
      -- = ((a ∩ b) ∩ c) ∪ ((a ∩ b) ∩ d)
      -- = ((b ∩ a) ∩ c) ∪ ((a ∩ b) ∩ d)
      -- = (b ∩ (a ∩ c)) ∪ ((a ∩ b) ∩ d)
      -- = (b ∩ (a ∩ c)) ∪ (a ∩ (b ∩ d))
      -- = (a ∩ (b ∩ d)) ∪ (b ∩ (a ∩ c))

    -- postulate proof2 : ∀{a b} → (a ∩ b) ∩ (∁(a) ∪ ∁(b)) ≡ ∅
      -- (a ∩ b) ∩ (∁(a) ∪ ∁(b))
      -- = (a ∩ (b ∩ ∁(b))) ∪ (b ∩ (a ∩ ∁(a)))
      -- = (a ∩ ∅) ∪ (b ∩ (a ∩ ∁(a)))
      -- = ∅ ∪ (b ∩ (a ∩ ∁(a)))
      -- = b ∩ (a ∩ ∁(a))
      -- = b ∩ ∅
      -- = ∅

    -- ∁(s₁ ∪ s₂) ∪ (s₁ ∪ s₂) = 𝐔
    -- (∁(s₁ ∪ s₂) ∪ (s₁ ∪ s₂)) ∩ (∁(a) ∪ ∁(b)) = 𝐔 ∩ (∁(a) ∪ ∁(b))
    -- (∁(s₁ ∪ s₂) ∪ (s₁ ∪ s₂)) ∩ (∁(a) ∪ ∁(b)) = ∁(a) ∪ ∁(b)
    -- ∁(a) ∪ ∁(b) = (∁(s₁ ∪ s₂) ∪ (s₁ ∪ s₂)) ∩ (∁(a) ∪ ∁(b))
    -- ∁(a) ∪ ∁(b) = (∁(s₁ ∪ s₂) ∩ (∁(a) ∪ ∁(b))) ∪ ((s₁ ∪ s₂) ∩ (∁(a) ∪ ∁(b)))
    -- ∁(a) ∪ ∁(b) = (∁(s₁ ∪ s₂) ∩ (∁(a) ∪ ∁(b))) ∪ ∅
    -- ∁(a) ∪ ∁(b) = ∁(s₁ ∪ s₂) ∩ (∁(a) ∪ ∁(b))

  postulate [∁]-of-[∩] : ∀{s₁ s₂ : S} → ∁(s₁ ∩ s₂) ≡ ∁(s₁) ∪ ∁(s₂)

  [∁∁]-elim : ∀{s : S} → ∁(∁(s)) ≡ s
  [∁∁]-elim {s} = transitivity(_≡_) proof2 (symmetry(_≡_) proof1) where
    proof1 : s ≡ s ∪ ∁(∁(s))
    proof1 =
      [∩]-inverseᵣ {∁(s)}
      ⩺ [≡]-with(s ∪_)
      ⩺ (eq ↦ transitivity(_≡_) eq ((identityᵣ(_∪_)(∅)) {s}))
      ⩺ symmetry(_≡_)
      ⩺ (eq ↦ transitivity(_≡_) eq ((distributivityₗ(_∪_)(_∩_))))
      ⩺ (eq ↦ transitivity(_≡_) eq ([≡]-with(_∩ (s ∪ ∁(∁(s)))) ([∪]-inverseᵣ)))
      ⩺ (eq ↦ transitivity(_≡_) eq (identityₗ(_∩_)(𝐔)))
      -- ∁(s) ∩ ∁(∁(s)) ≡ ∅
      -- s ∪ (∁(s) ∩ ∁(∁(s))) ≡ s ∪ ∅
      -- s ∪ (∁(s) ∩ ∁(∁(s))) ≡ s
      -- s ≡ s ∪ (∁(s) ∩ ∁(∁(s)))
      -- s ≡ (s ∪ ∁(s)) ∩ (s ∪ ∁(∁(s)))
      -- s ≡ 𝐔 ∩ (s ∪ ∁(∁(s)))
      -- s ≡ s ∪ ∁(∁(s))

    proof2 : ∁(∁(s)) ≡ s ∪ ∁(∁(s))
    proof2 =
      [∩]-inverseᵣ {s}
      ⩺ [≡]-with(_∪ ∁(∁(s)))
      ⩺ (eq ↦ transitivity(_≡_) eq (identityₗ(_∪_)(∅)))
      ⩺ symmetry(_≡_)
      ⩺ (eq ↦ transitivity(_≡_) eq ((distributivityᵣ(_∪_)(_∩_))))
      ⩺ (eq ↦ transitivity(_≡_) eq ([≡]-with((s ∪ ∁(∁(s))) ∩_) ([∪]-inverseᵣ)))
      ⩺ (eq ↦ transitivity(_≡_) eq ((identityᵣ(_∩_)(𝐔))))
      -- (s ∩ ∁(s)) ∪ ∁(∁(s)) ≡ ∅ ∪ ∁(∁(s))
      -- (s ∩ ∁(s)) ∪ ∁(∁(s)) ≡ ∁(∁(s))
      -- ∁(∁(s)) ≡ (s ∩ ∁(s)) ∪ ∁(∁(s))
      -- ∁(∁(s)) ≡ (s ∪ ∁(∁(s))) ∩ (∁(s) ∪ ∁(∁(s)))
      -- ∁(∁(s)) ≡ (s ∪ ∁(∁(s))) ∩ 𝐔
      -- ∁(∁(s)) ≡ s ∪ ∁(∁(s))

  postulate [∁]-uniqueness : ∀{s₁ s₂ : S} → (s₁ ∪ s₂ ≡ 𝐔) → (s₁ ∩ s₂ ≡ ∅) → (s₁ ≡ ∁(s₂))

  postulate [∁]-of-[∖] : ∀{s₁ s₂ : S} → ∁(s₁ ∖ s₂) ≡ ∁(s₁) ∪ s₂
  postulate [∖]-of-[∁] : ∀{s₁ s₂ : S} → ∁(s₁) ∖ ∁(s₂) ≡ s₂ ∖ s₁

  postulate [∖]-of-[∪]ᵣ : ∀{s₁ s₂ s₃ : S} → (s₁ ∖ (s₂ ∪ s₃)) ≡ (s₁ ∖ s₂)∩(s₁ ∖ s₃)
  postulate [∖]-of-[∩]ᵣ : ∀{s₁ s₂ s₃ : S} → (s₁ ∖ (s₂ ∩ s₃)) ≡ (s₁ ∖ s₂)∪(s₁ ∖ s₃)

  postulate [∖]-of-[∖]ᵣ : ∀{s₁ s₂ s₃ : S} → (s₁ ∖ (s₂ ∖ s₃)) ≡ (s₁ ∩ s₃)∪(s₁ ∖ s₂)
  postulate [∩]-from-[∖] : ∀{s₁ s₂ : S} → (s₁ ∖ (s₁ ∖ s₂)) ≡ (s₁ ∩ s₂) -- TODO: from [∖]-of-[∖]ᵣ

  postulate [∖]-self : ∀{s : S} → s ∖ s ≡ ∅
  postulate [∖]-of-[∅]ₗ : ∀{s : S} → ∅ ∖ s ≡ ∅
  postulate [∖]-of-[∅]ᵣ : ∀{s : S} → s ∖ ∅ ≡ s
  postulate [∖]-of-[𝐔]ₗ : ∀{s : S} → 𝐔 ∖ s ≡ ∁(s)
  postulate [∖]-of-[𝐔]ᵣ : ∀{s : S} → s ∖ 𝐔 ≡ ∅

record Subset : Type{Lvl.𝐒(ℓ)} where
  field
    _⊆_ : S → S → Stmt{ℓ} -- Subset
    ⦃ fundamentals ⦄ : Fundamentals
  open Fundamentals(fundamentals)

  field
    ⦃ [⊆]-antisymmetry ⦄ : Antisymmetry(_⊆_)(_≡_)
    ⦃ [⊆]-transitivity ⦄ : Transitivity(_⊆_)
    ⦃ [⊆]-reflexivity  ⦄ : Reflexivity(_⊆_)

    [≡]-to-[⊆] : ∀{a b} → (a ≡ b) → (a ⊆ b)

    [⊆]ₗ-of-[∪] : ∀{a b c} → (a ⊆ c) → (b ⊆ c) → ((a ∪ b) ⊆ c)
    [⊆]ᵣ-of-[∪]ₗ : ∀{a b} → (a ⊆ (a ∪ b))

    [⊆]ₗ-of-[∩]ₗ : ∀{a b} → ((a ∩ b) ⊆ a)
    [⊆]ᵣ-of-[∩] : ∀{a b c} → (c ⊆ a) → (c ⊆ b) → (c ⊆ (a ∩ b))

  [⊆]ᵣ-of-[∪]ᵣ : ∀{a b} → (b ⊆ (a ∪ b))
  [⊆]ᵣ-of-[∪]ᵣ {a}{b} =
    [⊆]ᵣ-of-[∪]ₗ {b}{a}
    🝖 [≡]-to-[⊆] (commutativity(_∪_))

  [⊆]ₗ-of-[∩]ᵣ : ∀{a b} → ((a ∩ b) ⊆ b)
  [⊆]ₗ-of-[∩]ᵣ {a}{b} =
    [≡]-to-[⊆] (commutativity(_∩_))
    🝖 [⊆]ₗ-of-[∩]ₗ {b}{a}

  [⊆]-min : ∀{s} → (∅ ⊆ s)
  [⊆]-min {s} =
    [⊆]ᵣ-of-[∪]ₗ {∅}{s}
    🝖 [≡]-to-[⊆] (identityₗ(_∪_)(∅))

  [⊆]-max : ∀{s} → (s ⊆ 𝐔)
  [⊆]-max {s} =
    [≡]-to-[⊆] (symmetry(_≡_) (identityₗ(_∩_)(𝐔)))
    🝖 [⊆]ₗ-of-[∩]ₗ {𝐔}{s}

  [⊆][∩]-equiv : ∀{a b} → (a ⊆ b) ↔ (a ∩ b ≡ a)
  [⊆][∩]-equiv {a}{b} = [↔]-intro l r where
    l : (a ⊆ b) ← (a ∩ b ≡ a)
    l aba =
      [≡]-to-[⊆] (symmetry(_≡_) aba)
      🝖 [⊆]ₗ-of-[∩]ᵣ

    r : (a ⊆ b) → (a ∩ b ≡ a)
    r ab =
      (antisymmetry(_⊆_)(_≡_)
        ([⊆]ₗ-of-[∩]ₗ)
        ([⊆]ᵣ-of-[∩] {a}{b}{a} (reflexivity(_⊆_)) ab)
      )
{-
  [⊆][∪]-equiv : ∀{a b} → (a ⊆ b) ↔ (a ∪ b ≡ b)
  [⊆][∪]-equiv {a}{b} = [↔]-intro l r where
    l : (a ⊆ b) ← (a ∪ b ≡ b)
    l aba =
      [≡]-to-[⊆] (symmetry(_≡_) aba)
      🝖 [⊆]ᵣ-of-[∪]ᵣ

    r : (a ⊆ b) → (a ∪ b ≡ b)
    r ab =
      (antisymmetry
        ([⊆]ᵣ-of-[∪]ᵣ)
        ([⊆]ₗ-of-[∪] {a}{b}{a} reflexivity ab)
      )
-}
  -- [⊆][∖]-equiv : (a ⊆ b) ↔ (a ∖ b ≡ ∅)

  -- [⊆][∁]-equiv : (a ⊆ b) ↔ (∁(b) ⊆ ∁(a))

  -- [∩][∪]-sub : (a ∩ b) ⊆ (a ∪ b)


text:
module ImportTests.ExtractDependent where
open import Data.Bool
open import Data.Nat
open import ExtractDependent

f : ℕ -> Bool
f 0 = false
f _ = true

testApply : Bool
testApply = apply _ _ f 5

testApplyImp : Bool
testApplyImp = applyImp f 6

testApplyImpSameName : Bool
testApplyImpSameName = applyImpSameName {ℕ} Bool f 3


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Values for AVL trees
-- Values must respect the underlying equivalence on keys
-----------------------------------------------------------------------

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

open import Relation.Binary using (Setoid; _Respects_)

module Data.AVL.Value {a ℓ} (S : Setoid a ℓ) where

open import Level using (suc; _⊔_)
import Function as F
open Setoid S renaming (Carrier to Key)

record Value v : Set (a ⊔ ℓ ⊔ suc v) where
  constructor MkValue
  field
    family   : Key → Set v
    respects : family Respects _≈_

-- The function `const` is defined using copatterns to prevent eager
-- unfolding of the function in goal types.
const : ∀ {v} → Set v → Value v
Value.family   (const V) = F.const V
Value.respects (const V) = F.const F.id


text:
module Thesis.Subst where

--------------------------------------------------------------------------------
-- Prove substitution lemma. Unfortunately, this is done using a quite different
-- machinery from what we use elsewhere. The machinery for defining substitution
-- is taken from a formalization of hereditary substitution (Hereditary
-- Substitutions for Simple Types, Formalized, by Keller and Altenkirch), and
-- uses a different machinery for weakening.

-- I developed the lemmas relating substitution and this form of weakening from
-- scratch.
--------------------------------------------------------------------------------

open import Thesis.Lang hiding (_-_)

_-_ : ∀ {σ} Γ → Var Γ σ → Context
∅ - ()
(σ • Γ) - this = Γ
(τ • Γ) - that x = τ • (Γ - x)

import Relation.Binary.PropositionalEquality as P
open P hiding (subst)
open import Postulate.Extensionality

extend-env : ∀ {σ Γ} (x : Var Γ σ) (rho : ⟦ Γ - x ⟧Context) (v : ⟦ σ ⟧Type) → ⟦ Γ ⟧Context
extend-env this rho v = v • rho
extend-env (that x) (v1 • rho) v = v1 • extend-env x rho v

extend-env-sound : ∀ {σ Γ} (x : Var Γ σ) (rho : ⟦ Γ - x ⟧Context) (v : ⟦ σ ⟧Type) → v ≡ ⟦ x ⟧Var (extend-env x rho v)
extend-env-sound this rho v = refl
extend-env-sound (that x) (v1 • rho) v = extend-env-sound x rho v

wkv : ∀ {Γ σ τ} → (x : Var Γ σ) → Var (Γ - x) τ → Var Γ τ
wkv this y = that y
wkv (that x) this = this
wkv (that x) (that y) = that (wkv x y)

data EqV : ∀ {Γ σ τ} → Var Γ σ → Var Γ τ → Set where
  same : ∀ {Γ σ} → {x : Var Γ σ} → EqV x x
  diff : ∀ {Γ σ τ} → (x : Var Γ σ) → (z : Var (Γ - x) τ) → EqV x (wkv x z)
  -- If x and y do not represent the same variable, then
  -- ∃ z. y ≡ wkv x z, allowing us to construct a proof that diff x z : EqV x y

eq : ∀ {Γ σ τ} → (x : Var Γ σ) → (y : Var Γ τ) → EqV x y
eq this this = same
eq this (that y) = diff this y
eq (that x) this = diff (that x) this
eq (that x) (that y) with eq x y
eq (that y) (that .y) | same = same
eq (that x) (that .(wkv x z)) | diff .x z = diff (that x) (that z)

wkTerm : ∀ {Γ σ τ} → (x : Var Γ σ) → Term (Γ - x) τ → Term Γ τ
wkTerm x (var v) = var (wkv x v)
wkTerm x (app t₁ t₂) = (app (wkTerm x t₁) (wkTerm x t₂))
wkTerm x (abs t) = abs (wkTerm (that x) t)
wkTerm x (const c) = const c

wkv-sound : ∀ {Γ σ τ} → (x : Var Γ σ) → (y : Var (Γ - x) τ) →
  (ρ : ⟦ Γ - x ⟧Context) (v : ⟦ σ ⟧Type) →
  ⟦ wkv x y ⟧Var (extend-env x ρ v) ≡ ⟦ y ⟧Var ρ
wkv-sound this y ρ v = refl
wkv-sound (that x) this (v0 • ρ) v = refl
wkv-sound (that x) (that y) (v0 • ρ) v = wkv-sound x y ρ v

wkTerm-sound : ∀ {Γ σ τ} → (x : Var Γ σ) → (t : Term (Γ - x) τ) →
  (ρ : ⟦ Γ - x ⟧Context) (v : ⟦ σ ⟧Type) →
  ⟦ wkTerm x t ⟧Term (extend-env x ρ v) ≡ ⟦ t ⟧Term ρ
wkTerm-sound x (const c) ρ v = refl
wkTerm-sound x (var y) ρ v = wkv-sound x y ρ v
wkTerm-sound x (app t₁ t₂) ρ v
  rewrite wkTerm-sound x t₁ ρ v
  | wkTerm-sound x t₂ ρ v = refl
wkTerm-sound x (abs t) ρ v = ext (λ v₁ → wkTerm-sound (that x) t (v₁ • ρ) v)

substVar : ∀ {Γ σ τ} → Var Γ τ → (x : Var Γ σ) → Term (Γ - x) σ → Term (Γ - x) τ
substVar v x u with eq x v
substVar v .v u | same = u
substVar .(wkv x z) x u | diff .x z = var z

-- The above is the crucial rule. The dotted pattern makes producing the result
-- easy.

subst : ∀ {Γ σ τ} → Term Γ τ → (x : Var Γ σ) → Term (Γ - x) σ → Term (Γ - x) τ
subst (var v) x u = substVar v x u
subst (app t₁ t₂) x u = app (subst t₁ x u) (subst t₂ x u)
subst (abs t) x u = abs (subst t (that x) (wkTerm this u))
subst (const c) x u = const c

substVar-lemma : ∀ {σ τ Γ} (v : Var Γ τ) (x : Var Γ σ) s rho → ⟦ substVar v x s ⟧Term rho ≡ ⟦ v ⟧Var (extend-env x rho (⟦ s ⟧Term rho))
substVar-lemma v x s rho with eq x v
substVar-lemma .(wkv x z) x s rho | diff .x z = sym (wkv-sound x z rho (⟦ s ⟧Term rho))
substVar-lemma x .x s rho | same = extend-env-sound x rho (⟦ s ⟧Term rho)

subst-lemma : ∀ {σ τ Γ} (t : Term Γ τ) (x : Var Γ σ) s rho → ⟦ subst t x s ⟧Term rho ≡ ⟦ t ⟧Term (extend-env x rho (⟦ s ⟧Term rho))
subst-lemma (const c) x s rho = refl
subst-lemma (var y) x s rho = substVar-lemma y x s rho
subst-lemma (app t₁ t₂) x s rho rewrite subst-lemma t₁ x s rho | subst-lemma t₂ x s rho = refl
subst-lemma (abs t) x s rho = ext body
  where
    body : ∀ v → ⟦ subst t (that x) (wkTerm this s) ⟧Term (v • rho) ≡
           ⟦ t ⟧Term (v • extend-env x rho (⟦ s ⟧Term rho))
    body v rewrite subst-lemma t (that x) (wkTerm this s) (v • rho) |
      wkTerm-sound this s rho v = refl

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------------
-- Abelian group base
------------------------------------------------------------------------------

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

module GroupTheory.AbelianGroup.Base where

-- We use the group theory base
open import GroupTheory.Base public

------------------------------------------------------------------------------
-- Abelian group theory axioms

-- We only need to add the commutativity axiom.
postulate comm : ∀ a b → a · b ≡ b · a
{-# ATP axiom comm #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Agda Sample File
-- https://github.com/agda/agda/blob/master/examples/syntax/highlighting/Test.agda

-- This test file currently lacks module-related stuff.

{- Nested
   {- comment. -} -}

module Test where

infix  12 _!
infixl  7 _+_ _-_
infixr  2 -_

postulate x : Set

f : (Set -> Set -> Set) -> Set
f _*_ = x * x

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

_+_ : ℕ -> ℕ -> ℕ
zero  + n = n
suc m + n = suc (m + n)

postulate _-_ : ℕ -> ℕ -> ℕ

-_ : ℕ -> ℕ
- n = n

_! : ℕ -> ℕ
zero  ! = suc zero
suc n ! = n - n !

record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where
  field
    refl      : forall x       -> x ≈ x
    sym       : {x y : a}      -> x ≈ y -> y ≈ x
    _`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z

data _≡_ {a : Set} (x : a) : a -> Set where
  refl : x ≡ x

subst : forall {a x y} ->
  (P : a -> Set) -> x ≡ y -> P x -> P y
subst {x = x} .{y = x} _ refl p = p

Equiv-≡ : forall {a} -> Equiv {a} _≡_
Equiv-≡ {a} =
  record { refl      = \_ -> refl
         ; sym       = sym
         ; _`trans`_ = _`trans`_
         }
  where
  sym : {x y : a} -> x ≡ y -> y ≡ x
  sym refl = refl

  _`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
  refl `trans` refl = refl

postulate
  String : Set
  Char   : Set
  Float  : Set

data Int : Set where
  pos    : ℕ → Int
  negsuc : ℕ → Int

{-# BUILTIN STRING  String #-}
{-# BUILTIN CHAR    Char   #-}
{-# BUILTIN FLOAT   Float  #-}

{-# BUILTIN NATURAL ℕ      #-}

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

data [_] (a : Set) : Set where
  []  : [ a ]
  _∷_ : a -> [ a ] -> [ a ]

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

primitive
  primStringToList : String -> [ Char ]

string : [ Char ]
string = primStringToList "∃ apa"

char : Char
char = '∀'

anotherString : String
anotherString = "¬ be\
    \pa"

nat : ℕ
nat = 45

float : Float
float = 45.0e-37

-- Testing qualified names.

open import Test
Eq = Test.Equiv {Test.ℕ}

max_stars_repo_name: dawidsowa/syntax-highlighting

max_issues_repo_name: dawidsowa/syntax-highlighting

max_forks_repo_name: dawidsowa/syntax-highlighting


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

syntax CommRing | CR

type
  * : 0-ary

term
  zero : * | 𝟘
  add  : *  *  ->  * | _⊕_ l20
  one  : * | 𝟙
  mult : *  *  ->  * | _⊗_ l30
  neg  : *  ->  * | ⊖_ r50

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
  (⊗C) a b |> mult(a, b) = mult(b, a)
-}

module CommRing.Syntax where

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

open import SOAS.Metatheory.Syntax

open import CommRing.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

-- Inductive term declaration
module CR:Terms (𝔛 : Familyₛ) where

  data CR : Familyₛ where
    var  : ℐ ⇾̣ CR
    mvar : 𝔛 α Π → Sub CR Π Γ → CR α Γ

    𝟘   : CR * Γ
    _⊕_ : CR * Γ → CR * Γ → CR * Γ
    𝟙   : CR * Γ
    _⊗_ : CR * Γ → CR * Γ → CR * Γ
    ⊖_  : CR * Γ → CR * Γ

  infixl 20 _⊕_
  infixl 30 _⊗_
  infixr 50 ⊖_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  CRᵃ : MetaAlg CR
  CRᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (zeroₒ ⋮ _)     → 𝟘
      (addₒ  ⋮ a , b) → _⊕_ a b
      (oneₒ  ⋮ _)     → 𝟙
      (multₒ ⋮ a , b) → _⊗_ a b
      (negₒ  ⋮ a)     → ⊖_  a
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module CRᵃ = MetaAlg CRᵃ

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

    open MetaAlg 𝒜ᵃ

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

    𝕤𝕖𝕞  𝟘        = 𝑎𝑙𝑔 (zeroₒ ⋮ tt)
    𝕤𝕖𝕞 (_⊕_ a b) = 𝑎𝑙𝑔 (addₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  𝟙        = 𝑎𝑙𝑔 (oneₒ  ⋮ tt)
    𝕤𝕖𝕞 (_⊗_ a b) = 𝑎𝑙𝑔 (multₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (⊖_  a)   = 𝑎𝑙𝑔 (negₒ  ⋮ 𝕤𝕖𝕞 a)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ CRᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ CR α Γ) → 𝕤𝕖𝕞 (CRᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (zeroₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (addₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (oneₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (multₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (negₒ  ⋮ _) = refl

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

    module _ (g : CR ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ CRᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

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

      𝕤𝕖𝕞! 𝟘 = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊕_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! 𝟙 = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊗_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (⊖_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩

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

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

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Data.Either.Multi where

open import Data
open import Data.Either
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Data.Tuple.RaiseTypeᵣ
open import Data.Tuple.RaiseTypeᵣ.Functions
open import Data.Tuple using (_⨯_ ; _,_)
open import Function.Multi
open import Function.Multi.Functions
import      Lvl
import      Lvl.MultiFunctions as Lvl
open import Numeral.Finite
open import Numeral.Natural
open import Type

Alt : (n : ℕ) → ∀{ℓ𝓈} → TypesOfTypes{n}(ℓ𝓈) ⇉ Type{Lvl.⨆(ℓ𝓈)}
Alt(n) = binaryTypeRelator₊(n)(_‖_)(Empty)

pattern alt₀   x = _‖_.Left x
pattern alt₁   x = _‖_.Right(alt₀ x)
pattern alt₂   x = _‖_.Right(alt₁ x)
pattern alt₃   x = _‖_.Right(alt₂ x)
pattern alt₄   x = _‖_.Right(alt₃ x)
pattern alt₅   x = _‖_.Right(alt₄ x)
pattern alt₆   x = _‖_.Right(alt₅ x)
pattern alt₇   x = _‖_.Right(alt₆ x)
pattern alt₈   x = _‖_.Right(alt₇ x)
pattern alt₉   x = _‖_.Right(alt₈ x)
pattern alt₁,₂ x = _‖_.Right(x)
pattern alt₂,₃ x = _‖_.Right(alt₁,₂ x)
pattern alt₃,₄ x = _‖_.Right(alt₂,₃ x)
pattern alt₄,₅ x = _‖_.Right(alt₃,₄ x)
pattern alt₅,₆ x = _‖_.Right(alt₄,₅ x)
pattern alt₆,₇ x = _‖_.Right(alt₅,₆ x)
pattern alt₇,₈ x = _‖_.Right(alt₆,₇ x)
pattern alt₈,₉ x = _‖_.Right(alt₇,₈ x)

{-
-- TODO: Move or generalize uncurry
uncurryTypes : (n : ℕ) → ∀{ℓ𝓈}{ℓ}{B : Type{ℓ}} → (TypesOfTypes{𝐒(n)}(ℓ𝓈) ⇉ B) → (Types(ℓ𝓈) → B)
uncurryTypes(𝟎)    f          = f
uncurryTypes(𝐒(n)) f (x , xs) = uncurryTypes(n) (f(x)) xs

-- TODO: Problem with the type. Not normalizing correctly
alt : ∀{n}{ℓ𝓈}{As : Types(ℓ𝓈)} → (i : 𝕟(𝐒(n))) → (index i As) → uncurryTypes(n) (Alt(𝐒(n)){ℓ𝓈}) As
alt {0}       𝟎     x = x
alt {1}       𝟎     x = Left  x
alt {1}       (𝐒 𝟎) x = Right x
alt {𝐒(𝐒(n))} 𝟎     x = {!Left x!}
alt {𝐒(𝐒(n))} (𝐒 i) x = {!Right(alt {𝐒(n)} i x)!}
-}


text:
{-# OPTIONS --allow-unsolved-metas #-}
module FindTermNode where

open import TermNode
open import OscarPrelude

record FindTermNode (A : Set) : Set
 where
  field
    findTermNode : A → TermNode → Maybe TermNode

open FindTermNode ⦃ … ⦄ public

open import TermCode
open import Term
open import Element

instance
  FindTermNodeTermCode : FindTermNode TermCode
  FindTermNode.findTermNode FindTermNodeTermCode termCode record { children = [] ; number = number₁ } = nothing
  FindTermNode.findTermNode FindTermNodeTermCode termCode 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } = ifYes fst₁ ≟ termCode then just snd₁ else findTermNode termCode record 𝔫 { children = children₁ }

  FindTermNodeTermCodes : FindTermNode (List TermCode)
  FindTermNode.findTermNode FindTermNodeTermCodes [] node = just node
  FindTermNode.findTermNode FindTermNodeTermCodes (x ∷ termCodes) node = join $ findTermNode termCodes <$> findTermNode x node

  FindTermNodeTerm : FindTermNode Term
  FindTermNode.findTermNode FindTermNodeTerm term node = findTermNode (encodeTerm term) node

-- This is starting to get difficult. We need Agda to know that the Term is encoded in the TermNode. Then we can drop the Maybe
getInterpretationOfTerm : Term → TermNode → Maybe Element
getInterpretationOfTerm τ node = ⟨_⟩ ∘ number <$> findTermNode (encodeTerm τ) node

open import Membership

FindTermNodeTermCode-ok : ∀ {𝔠 𝔫} → 𝔠 child∈ 𝔫 → IsJust (findTermNode 𝔠 𝔫)
FindTermNodeTermCode-ok {𝔠} {record { children = [] ; number = number₁ }} ()
--FindTermNodeTermCode-ok {𝔠} {record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} x₁ = case (fst₁ ≟_) 𝔠 , graphAt {B = λ 𝑐 → Dec (fst₁ ≡ 𝑐)} (fst₁ ≟_) 𝔠 of λ { (yes x , snd₂) → {!!} ; (no x , snd₂) → {!!}} --λ { ((yes ===) , (inspect s1)) → {!!} ; ((no =n=) , inspect s2) → {!!} }
--FindTermNodeTermCode-ok {𝔠} {record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} x₁ = case fst₁ ≟ 𝔠 of λ { (yes refl) → {!!} ; (no x) → {!!}}
FindTermNodeTermCode-ok {𝔠} {record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} x₁ with fst₁ ≟ 𝔠
FindTermNodeTermCode-ok {𝔠} {record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} x₁ | yes eq2 = tt
FindTermNodeTermCode-ok {.fst₁} {record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} (zero) | no neq = ⊥-elim (neq refl)
FindTermNodeTermCode-ok {𝔠} {𝔫@record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }} (suc x₁) | no neq = FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }} x₁

Justified : ∀ {a} {A : Set a} → (m : Maybe A) → IsJust m → ∃ λ x → m ≡ just x
Justified nothing ()
Justified (just x) x₁ = _ , refl

open import FunctionName
open import Vector

storeTerm-ok : ∀ τ 𝔫 𝔑 → IsJust (findTermNode τ (snd (runIdentity (runStateT (runStateT (storeTerm τ) 𝔑) 𝔫))))
storeTerm-ok (variable 𝑥) 𝔫 𝔑 with variable 𝑥 child∈? 𝔫
storeTerm-ok (variable 𝑥) 𝔫 𝔑 | no x with TermCode.variable 𝑥 ≟ variable 𝑥
storeTerm-ok (variable 𝑥) 𝔫 𝔑 | no x | yes _ = tt
storeTerm-ok (variable 𝑥) 𝔫 𝔑 | no x | no variable𝑥≢variable𝑥 = ⊥-elim (variable𝑥≢variable𝑥 refl)
--storeTerm-ok (variable 𝑥) 𝔫 𝔑 | yes vx∈𝔫 rewrite setGet-ok 𝔫 vx∈𝔫 = {!𝔫!}
storeTerm-ok (variable 𝑥) record { children = [] ; number = number₁ } 𝔑 | yes ()
--storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 rewrite setGet-ok 𝔫 vx∈𝔫 = {!!}
storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 rewrite setGet-ok 𝔫 vx∈𝔫 with fst₁ ≟ variable 𝑥
storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 | yes eq = tt
--… | no neq = case vx∈𝔫 of λ { (here .(map fst children₁)) → ⊥-elim (neq refl)  ; (there .fst₁ asdf) → case graphAt FindTermNodeTermCode-ok asdf of λ { (ingraph sss) → {!!} } } -- storeTerm-ok x {!record 𝔫 { children = children₁ }!} 𝔑 -- x record 𝔫 { children = children₁ } 𝔑
--… | no neq = case vx∈𝔫 of λ { (here .(map fst children₁)) → ⊥-elim (neq refl)  ; (there .fst₁ asdf) → case inspect $ FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }} asdf of λ { (.(FindTermNodeTermCode-ok asdf) , ingraph refl) → {!!}} } -- storeTerm-ok x {!record 𝔫 { children = children₁ }!} 𝔑 -- x record 𝔫 { children = children₁ } 𝔑
storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 | no neq with vx∈𝔫
storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 | no neq | zero = ⊥-elim (neq refl)
--storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 | no neq | there dfdsf fdsdfs with FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }} fdsdfs | graphAt (FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }}) fdsdfs
--… | frfrrf | ingraph tttttt = transport _ (snd $ Justified (FindTermNode.findTermNode FindTermNodeTermCode (variable 𝑥) (record { children = children₁ ; number = number₁ })) (FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }} fdsdfs)) _
storeTerm-ok x@(variable 𝑥) 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } 𝔑 | yes vx∈𝔫 | no neq | suc fdsdfs rewrite (snd $ Justified (FindTermNode.findTermNode FindTermNodeTermCode (variable 𝑥) (record { children = children₁ ; number = number₁ })) (FindTermNodeTermCode-ok {𝔫 = record 𝔫 { children = children₁ }} fdsdfs)) = tt
storeTerm-ok (function 𝑥 𝑎) 𝔫 𝔑 with (function 𝑥 (arity 𝑎)) child∈? 𝔫
storeTerm-ok (function 𝑥 ⟨ ⟨ [] ⟩ ⟩) 𝔫 𝔑 | no x with Eq._==_ EqFunctionName ⟨ name 𝑥 ⟩ ⟨ name 𝑥 ⟩
storeTerm-ok (function 𝑥 ⟨ ⟨ [] ⟩ ⟩) 𝔫 𝔑 | no x | (yes refl) = tt
… | no neq = ⊥-elim (neq refl)
--storeTerm-ok τ₀@(function 𝑓 ⟨ τ₁ ∷ τ₂s ⟩) 𝔫 𝔑 | no 𝔠₁∉𝔫 = {!τ₁!}
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₁∉𝔫 with variable 𝑥 child∈? 𝔫
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₀∉𝔫 | (yes 𝔠₁∈𝔫) with 𝑓₀ ≟ 𝑓₀
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₀∉𝔫 | (yes 𝔠₁∈𝔫) | yes refl with TermCode.variable 𝑥 ≟ variable 𝑥
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₀∉𝔫 | (yes 𝔠₁∈𝔫) | yes refl | yes eq = tt
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₀∉𝔫 | (yes 𝔠₁∈𝔫) | yes refl | no neq = ⊥-elim (neq refl)
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥 ∷ []        ⟩ ⟩) 𝔫 𝔑        | no 𝔠₀∉𝔫 | (yes 𝔠₁∈𝔫) | no neq = ⊥-elim (neq refl)
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ []       ⟩ ⟩) 𝔫 𝔑       | no 𝔠₀∉𝔫 | (no 𝔠₁∉𝔫) with 𝑓₀ ≟ 𝑓₀
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ []       ⟩ ⟩) 𝔫 𝔑       | no 𝔠₀∉𝔫 | (no 𝔠₁∉𝔫) | yes refl with TermCode.variable 𝑥₁ ≟ variable 𝑥₁
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ []       ⟩ ⟩) 𝔫 𝔑       | no 𝔠₀∉𝔫 | (no 𝔠₁∉𝔫) | yes refl | yes 𝔠₁≡𝔠₁ = tt
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ []       ⟩ ⟩) 𝔫 𝔑       | no 𝔠₀∉𝔫 | (no 𝔠₁∉𝔫) | yes refl | no 𝔠₁≢𝔠₁ = ⊥-elim (𝔠₁≢𝔠₁ refl)
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ []       ⟩ ⟩) 𝔫 𝔑       | no 𝔠₀∉𝔫 | (no 𝔠₁∉𝔫) | no 𝑓₀≢𝑓₀ = ⊥-elim (𝑓₀≢𝑓₀ refl) -- rewrite setGet-ok 𝔫 𝔠₁∈𝔫
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ τ₂ ∷ τ₃s ⟩ ⟩) 𝔫 𝔑 | no 𝔠₀∉𝔫 with variable 𝑥₁ child∈? 𝔫
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ τ₂ ∷ τ₃s ⟩ ⟩) 𝔫 𝔑 | no 𝔠₀∉𝔫 | yes 𝔠₁∈𝔫 = {!!}
storeTerm-ok (function 𝑓₀ ⟨ ⟨ variable 𝑥₁ ∷ τ₂ ∷ τ₃s ⟩ ⟩) 𝔫 𝔑 | no 𝔠₀∉𝔫 | no 𝔠₁∉𝔫 = {!!}
storeTerm-ok τ₀@(function 𝑓₀ ⟨ ⟨ function 𝑓₁ τ₁s ∷ τ₂s ⟩ ⟩) 𝔫 𝔑 | no 𝔠₁∉𝔫 = {!!}
storeTerm-ok (function 𝑥 x₁) 𝔫 𝔑 | yes x = {!!}

mutual

  storeTermVerifiably' : (τ : Term) → StateT Nat (StateT (Σ TermNode λ n → IsJust (findTermNode τ n)) Identity) ⊤
  storeTermVerifiably' (variable x) = {!!}
  storeTermVerifiably' (function x x₁) = {!!}

  storeTermVerifiably : Term → StateT Nat (StateT TermNode Identity) ⊤
  storeTermVerifiably τ@(variable _) = storeTermCodes' (encodeTerm τ)
  storeTermVerifiably τ@(function _ τs) = storeTermCodes' (encodeTerm τ) ~| storeTermsVerifiably τs

  storeTermsVerifiably : Terms → StateT Nat (StateT TermNode Identity) ⊤
  storeTermsVerifiably ⟨ ⟨ [] ⟩ ⟩ = return tt
  storeTermsVerifiably ⟨ ⟨ τ ∷ τs ⟩ ⟩ = storeTermVerifiably τ ~| storeTermsVerifiably ⟨ ⟨ τs ⟩ ⟩ ~| return tt


text:
module Relator.Congruence.Proofs where

import      Lvl
open import Functional
open import Logic.Propositional
open import Logic.Predicate
-- TODO: open import Structure.Function.Domain
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Relator.Congruence
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Names
open import Syntax.Transitivity
open import Type

module _ {ℓ₁ ℓ₂} {X : Type{ℓ₁}}{Y : Type{ℓ₂}} {f : X → Y} where
  instance
    [≅]-reflexivity : Reflexivity (_≅_of f)
    Reflexivity.proof([≅]-reflexivity) = [≅]-intro [≡]-intro

  instance
    [≅]-symmetry : Symmetry (_≅_of f)
    Symmetry.proof([≅]-symmetry) = ([≅]-intro ∘ symmetry(_≡_) ∘ [≅]-elim)

  instance
    [≅]-transitivity : Transitivity (_≅_of f)
    Transitivity.proof([≅]-transitivity) (eq1) (eq2) = [≅]-intro(([≅]-elim eq1) 🝖 ([≅]-elim eq2))

  instance
    [≅]-equivalence : Equivalence (_≅_of f)
    [≅]-equivalence = record {
        reflexivity  = [≅]-reflexivity ;
        symmetry     = [≅]-symmetry    ;
        transitivity = [≅]-transitivity
      }

  [≅]-to-[≡] : Injective(f) ↔ (∀{x₁ x₂ : X} → (x₁ ≅ x₂ of f) → (x₁ ≡ x₂))
  [≅]-to-[≡] = [↔]-intro (_∘ [≅]-intro) (_∘ [≅]-elim)

module _ {ℓ₁ ℓ₂ ℓ₃} {X₁ : Type{ℓ₁}}{X₂ : Type{ℓ₂}}{Y : Type{ℓ₃}} where
  [≅]-composition : ∀{x₁ x₂ : X₁}{g : X₁ → X₂} → (x₁ ≅ x₂ of g) → ∀{f : X₂ → Y} → (g(x₁) ≅ g(x₂) of f)
  [≅]-composition ([≅]-intro (fx₁≡fx₂)) {f} = [≅]-intro ([≡]-with(f) (fx₁≡fx₂))
    -- x₁ ≅ x₂
    -- ⇔ g(x₁) = g(x₂)
    -- ⇒ f(g(x₁)) = f(g(x₂))


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Exponential Object

-- TODO: Where is the notation from? It is neither from Wikipedia nor the nLab.
module Categories.Object.Exponential {o ℓ e} (𝒞 : Category o ℓ e) where

open Category 𝒞

open import Level
open import Function using (_$_)

open import Categories.Morphism.Reasoning 𝒞
open import Categories.Object.Product 𝒞
  hiding (repack; repack≡id; repack∘; repack-cancel; up-to-iso; transport-by-iso)
open import Categories.Morphism 𝒞

open HomReasoning

private
  variable
    A B C D X Y : Obj

record Exponential (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
  field
    B^A : Obj
    product : Product B^A A

  module product = Product product

  B^A×A : Obj
  B^A×A = product.A×B

  field
    eval     : B^A×A ⇒ B
    λg       : ∀ (X×A : Product X A) → (Product.A×B X×A ⇒ B) → (X ⇒ B^A)
    β        : ∀ (X×A : Product X A) {g : Product.A×B X×A ⇒ B} →
                 (eval ∘ [ X×A ⇒ product ] λg X×A g ×id ≈ g)
    λ-unique : ∀ (X×A : Product X A) {g : Product.A×B X×A ⇒ B} {h : X ⇒ B^A} →
                 (eval ∘ [ X×A ⇒ product ] h ×id ≈ g) → (h ≈ λg X×A g)

  η : ∀ (X×A : Product X A) {f : X ⇒ B^A } → λg X×A (eval ∘ [ X×A ⇒ product ] f ×id) ≈ f
  η X×A {f} = sym (λ-unique X×A refl)

  λ-cong : ∀ {X : Obj} (X×A : Product X A) {f g} →
             f ≈ g → λg X×A f ≈ λg X×A g
  λ-cong X×A {f = f} {g = g} f≡g = λ-unique X×A (trans (β X×A) f≡g)

  subst : ∀ (p₂ : Product C A) (p₃ : Product D A) {f g} →
            λg p₃ f ∘ g ≈ λg p₂ (f ∘ [ p₂ ⇒ p₃ ] g ×id)
  subst p₂ p₃ {f} {g} = λ-unique p₂ (begin
    eval ∘ [ p₂ ⇒ product ] λg p₃ f ∘ g ×id
                           ≈˘⟨ refl⟩∘⟨ [ p₂ ⇒ p₃ ⇒ product ]×id∘×id ⟩
    eval ∘ [ p₃ ⇒ product ] λg p₃ f ×id ∘ [ p₂ ⇒ p₃ ] g ×id
                           ≈⟨ pullˡ (β p₃) ⟩
    f ∘ [ p₂ ⇒ p₃ ] g ×id ∎)

  η-id : λg product eval ≈ id
  η-id = begin
    λg product eval                                  ≈˘⟨ identityʳ ⟩
    λg product eval ∘ id                             ≈⟨ subst _ _ ⟩
    λg product (eval ∘ [ product ⇒ product ] id ×id) ≈⟨ η product ⟩
    id                                               ∎

  λ-unique′ : ∀ (X×A : Product X A) {h i : X ⇒ B^A} →
                eval ∘ [ X×A ⇒ product ] h ×id ≈ eval ∘ [ X×A ⇒ product ] i ×id → h ≈ i
  λ-unique′ p eq = trans (λ-unique p eq) (sym (λ-unique p refl))

-- some aliases to make proof signatures less ugly
[_]eval : ∀{A B}(e₁ : Exponential A B) → Exponential.B^A×A e₁ ⇒ B
[ e₁ ]eval = Exponential.eval e₁

[_]λ : ∀{A B}(e₁ : Exponential A B)
  → {X : Obj} → (X×A : Product X A) → (Product.A×B X×A ⇒ B) → (X ⇒ Exponential.B^A e₁)
[ e₁ ]λ = Exponential.λg e₁

{-
   D×C --id × f--> D×A --g--> B

   D --λ (g ∘ id × f)--> B^C
    \                   ^
     \                 /
     λ g       λ (e ∘ id × f)
       \        /
        v      /
          B^A
-}
λ-distrib : ∀ (e₁ : Exponential C B) (e₂ : Exponential A B)
              (p₃ : Product D C) (p₄ : Product D A) (p₅ : Product (Exponential.B^A e₂) C)
              {f} {g : Product.A×B p₄ ⇒ B} →
              [ e₁ ]λ p₃ (g ∘ [ p₃ ⇒ p₄ ]id× f)
              ≈ [ e₁ ]λ p₅ ([ e₂ ]eval ∘ [ p₅ ⇒ Exponential.product e₂ ]id× f) ∘ [ e₂ ]λ p₄ g
λ-distrib e₁ e₂ p₃ p₄ p₅ {f} {g} = sym $ e₁.λ-unique p₃ $ begin
  [ e₁ ]eval ∘ ([ p₃ ⇒ p₁ ] [ e₁ ]λ p₅ ([ e₂ ]eval ∘ [ p₅ ⇒ p₂ ]id× f) ∘ [ e₂ ]λ p₄ g ×id)
                       ≈˘⟨ refl⟩∘⟨ [ p₃ ⇒ p₅ ⇒ p₁ ]×id∘×id ⟩
  [ e₁ ]eval ∘ [ p₅ ⇒ p₁ ] [ e₁ ]λ p₅ ([ e₂ ]eval ∘ [ p₅ ⇒ p₂ ]id× f) ×id
             ∘ [ p₃ ⇒ p₅ ] [ e₂ ]λ p₄ g ×id
                       ≈⟨ pullˡ (e₁.β p₅) ⟩
  ([ e₂ ]eval ∘ [ p₅ ⇒ p₂ ]id× f)
              ∘ [ p₃ ⇒ p₅ ] [ e₂ ]λ p₄ g ×id
                       ≈⟨ assoc ⟩
  [ e₂ ]eval ∘ [ p₅ ⇒ p₂ ]id× f
             ∘ [ p₃ ⇒ p₅ ] [ e₂ ]λ p₄ g ×id
                       ≈˘⟨ refl⟩∘⟨ [ p₄ ⇒ p₂ , p₃ ⇒ p₅ ]first↔second ⟩
  [ e₂ ]eval ∘ [ p₄ ⇒ p₂ ] [ e₂ ]λ p₄ g ×id ∘ [ p₃ ⇒ p₄ ]id× f
                       ≈⟨ pullˡ (e₂.β p₄) ⟩
  g ∘ [ p₃ ⇒ p₄ ]id× f ∎
  where module e₁ = Exponential e₁
        module e₂ = Exponential e₂
        p₁        = e₁.product
        p₂        = e₂.product

repack : ∀{A B} (e₁ e₂ : Exponential A B) → Exponential.B^A e₁ ⇒ Exponential.B^A e₂
repack e₁ e₂ = e₂.λg e₁.product e₁.eval
  where
    module e₁ = Exponential e₁
    module e₂ = Exponential e₂

repack≡id : ∀{A B} (e : Exponential A B) → repack e e ≈ id
repack≡id = Exponential.η-id

repack∘ : ∀ (e₁ e₂ e₃ : Exponential A B) → repack e₂ e₃ ∘ repack e₁ e₂ ≈ repack e₁ e₃
repack∘ e₁ e₂ e₃ =
  let p₁ = product e₁ in
  let p₂ = product e₂ in
  begin
      [ e₃ ]λ p₂ [ e₂ ]eval
    ∘ [ e₂ ]λ p₁ [ e₁ ]eval
  ≈⟨ λ-cong e₃ p₂ (introʳ (second-id p₂)) ⟩∘⟨refl ⟩
      [ e₃ ]λ p₂ ([ e₂ ]eval ∘ [ p₂ ⇒ p₂ ]id× id)
    ∘ [ e₂ ]λ p₁ [ e₁ ]eval
  ≈˘⟨ λ-distrib e₃ e₂ p₁ p₁ p₂ ⟩
    [ e₃ ]λ p₁ ([ e₁ ]eval ∘ [ p₁ ⇒ p₁ ]id× id)
  ≈⟨ λ-cong e₃ p₁ (⟺ (introʳ (second-id (product e₁)))) ⟩
    [ e₃ ]λ p₁ [ e₁ ]eval
  ∎
  where open Exponential

repack-cancel : ∀{A B} (e₁ e₂ : Exponential A B) → repack e₁ e₂ ∘ repack e₂ e₁ ≈ id
repack-cancel e₁ e₂ = repack∘ e₂ e₁ e₂ ○ repack≡id e₂

up-to-iso : ∀{A B} (e₁ e₂ : Exponential A B) → Exponential.B^A e₁ ≅ Exponential.B^A e₂
up-to-iso e₁ e₂ = record
  { from = repack e₁ e₂
  ; to   = repack e₂ e₁
  ; iso  = record
    { isoˡ = repack-cancel e₂ e₁
    ; isoʳ = repack-cancel e₁ e₂
    }
  }

transport-by-iso : ∀ (e : Exponential A B) → Exponential.B^A e ≅ X → Exponential A B
transport-by-iso {X = X} e e≅X = record
  { B^A             = X
  ; product         = X×A
  ; eval            = e.eval
  ; λg              = λ Y×A Y×A⇒B → from ∘ (e.λg Y×A Y×A⇒B)
  ; β               = λ Y×A {h} → begin
    e.eval ∘ [ Y×A ⇒ X×A ] from ∘ e.λg Y×A h ×id ≈⟨ refl⟩∘⟨ e.product.⟨⟩-cong₂ (pullˡ (cancelˡ isoˡ))
                                                                               (elimˡ refl) ⟩
    e.eval ∘ [ Y×A ⇒ e.product ] e.λg Y×A h ×id  ≈⟨ e.β Y×A ⟩
    h                                            ∎
  ; λ-unique        = λ Y×A {h} {i} eq →
    switch-tofromˡ e≅X $ e.λ-unique Y×A $ begin
      e.eval ∘ [ Y×A ⇒ e.product ] to ∘ i ×id    ≈⟨ refl⟩∘⟨ e.product.⟨⟩-cong₂ assoc (introˡ refl) ⟩
      e.eval ∘ [ Y×A ⇒ X×A ] i ×id               ≈⟨ eq ⟩
      h                                          ∎
  }
  where module e = Exponential e
        X×A      = Mobile e.product e≅X ≅.refl
        open _≅_ e≅X

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Relation.Binary.Core

module Morphism.Structures where

open import Algebra
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
import Function.Definitions as FunctionDefinitions
open import Relation.Binary.Morphism.Structures
open import Algebra.Morphism.Structures

private
  variable
    a b ℓ₁ ℓ₂ : Level


text:
-- Andreas, 2015-05-02, issue reported by Gabe Dijkstra
open import Common.Prelude
open import Common.Equality

data T : Set where
  c0 : ⊥ → T
  c1 : ⊥ → T

-- The following should not pass, as c0 and c1 are not fully applied.
c0≠c1 : c0 ≡ c1 → ⊥
c0≠c1 ()

-- The latter conflicts with function extensionality.
postulate
  fun-ext : {A B : Set} → (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g

c0=c1 : c0 ≡ c1
c0=c1 = fun-ext c0 c1 (λ ())

wrong : ⊥
wrong = c0≠c1 c0=c1

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Categories.Morphism.Cartesian where

open import Level

open import Categories.Category
open import Categories.Functor

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

record Cartesian (F : Functor C D) {X Y} (f : C [ X , Y ]) : Set (levelOfTerm F) where
  private
    module C = Category C
    module D = Category D
    open Functor F
    open D

  field
    universal : ∀ {A} {u : F₀ A ⇒ F₀ X} (h : C [ A , Y ]) →
                  F₁ f ∘ u ≈ F₁ h →  C [ A , X ]
    commute   : ∀ {A} {u : F₀ A ⇒ F₀ X} {h : C [ A , Y ]}
                  (eq : F₁ f ∘ u ≈ F₁ h) →
                  C [ C [ f ∘ universal h eq ] ≈ h ]
    compat    : ∀ {A} {u : F₀ A ⇒ F₀ X} {h : C [ A , Y ]}
                  (eq : F₁ f ∘ u ≈ F₁ h) →
                  F₁ (universal h eq) ≈ u


text: module Issue1232.Nat where


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition for the permutation relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Permutation.Propositional
  {a} {A : Set a} where

open import Data.List.Base using (List; []; _∷_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.Reasoning.Setoid as EqReasoning

------------------------------------------------------------------------
-- An inductive definition of permutation

-- Note that one would expect that this would be defined in terms of
-- `Permutation.Setoid`. This is not currently the case as it involves
-- adding in a bunch of trivial `_≡_` proofs to the constructors which
-- a) adds noise and b) prevents easy access to the variables `x`, `y`.
-- This may be changed in future when a better solution is found.

infix 3 _↭_

data _↭_ : Rel (List A) a where
  refl  : ∀ {xs}        → xs ↭ xs
  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs

------------------------------------------------------------------------
-- _↭_ is an equivalence

↭-reflexive : _≡_ ⇒ _↭_
↭-reflexive refl = refl

↭-refl : Reflexive _↭_
↭-refl = refl

↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
↭-sym refl                = refl
↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)

-- A smart version of trans that avoids unnecessary `refl`s (see #1113).
↭-trans : Transitive _↭_
↭-trans refl ρ₂ = ρ₂
↭-trans ρ₁ refl = ρ₁
↭-trans ρ₁ ρ₂   = trans ρ₁ ρ₂

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

↭-setoid : Setoid _ _
↭-setoid = record
  { isEquivalence = ↭-isEquivalence
  }

------------------------------------------------------------------------
-- A reasoning API to chain permutation proofs and allow "zooming in"
-- to localised reasoning.

module PermutationReasoning where

  private
    module Base = EqReasoning ↭-setoid

  open EqReasoning ↭-setoid public
    hiding (step-≈; step-≈˘)

  infixr 2 step-↭  step-↭˘ step-swap step-prep

  step-↭  = Base.step-≈
  step-↭˘ = Base.step-≈˘

  -- Skip reasoning on the first element
  step-prep : ∀ x xs {ys zs : List A} → (x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ xs) IsRelatedTo zs
  step-prep x xs rel xs↭ys = relTo (trans (prep x xs↭ys) (begin rel))

  -- Skip reasoning about the first two elements
  step-swap : ∀ x y xs {ys zs : List A} → (y ∷ x ∷ ys) IsRelatedTo zs →
              xs ↭ ys → (x ∷ y ∷ xs) IsRelatedTo zs
  step-swap x y xs rel xs↭ys = relTo (trans (swap x y xs↭ys) (begin rel))

  syntax step-↭  x y↭z x↭y = x ↭⟨  x↭y ⟩ y↭z
  syntax step-↭˘ x y↭z y↭x = x ↭˘⟨  y↭x ⟩ y↭z
  syntax step-prep x xs y↭z x↭y = x ∷ xs <⟨ x↭y ⟩ y↭z
  syntax step-swap x y xs y↭z x↭y = x ∷ y ∷ xs <<⟨ x↭y ⟩ y↭z


text:
-- Andreas, 2017-11-19, issue #2854

-- Agda should not complain about "possibly empty type of sizes"
-- if the SIZELT builtin is not bound.

data Tree : Set₁ where
  node : {A : Set} (f : A → Tree) → Tree

const : Tree → Tree
const t = node λ x → t

-- WAS:
-- Failed to solve the following constraints:
--   Is not empty type of sizes: _A_6 t

-- Expected:
-- Unsolved meta.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module DSession where

open import Data.Bool
open import Data.Fin
open import Data.Empty
open import Data.List
open import Data.List.All
open import Data.Maybe hiding (All)
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Data.Unit
open import Function using (_$_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values

-- this is really just a Kleisli arrow
data Cont (G : SCtx) (φ : TCtx) (t : Type) : Type → Set where
  ident :
    (ina-G : Inactive G)
    → (unr-φ : All Unr φ)
    → Cont G φ t t

  bind : ∀ {φ₁ φ₂ G₁ G₂ t₂ t₃}
    → (ts : Split φ φ₁ φ₂)
    → (ss : SSplit G G₁ G₂)
    → (e₂ : Expr (t ∷ φ₁) t₂)
    → (ϱ₂ : VEnv G₁ φ₁)
    → (κ₂ : Cont G₂ φ₂ t₂ t₃)
    → Cont G φ t t₃

  subsume : ∀ {t₁ t₂}
    → (t≤t1 : SubT t t₁)
    → (κ : Cont G φ t₁ t₂)
    → Cont G φ t t₂

compose : ∀ {G G₁ G₂ φ φ₁ φ₂ t₁ t₂ t₃}
  → Split φ φ₁ φ₂
  → SSplit G G₁ G₂
  → Cont G₁ φ₁ t₁ t₂
  → Cont G₂ φ₂ t₂ t₃
  → Cont G φ t₁ t₃
compose ss ssp (ident ina-G unr-φ) (ident ina-G₁ unr-φ₁) =
  ident (ssplit-inactive ssp ina-G ina-G₁) (split-unr ss unr-φ unr-φ₁)
compose ss ssp (ident ina-G unr-φ) (bind ts ss₁ e₂ ϱ₂ κ₂) = bind {!!} {!!} e₂ ϱ₂ κ₂
compose ss ssp (ident ina-G unr-φ) (subsume t≤t1 κ₂)
  with inactive-left-ssplit ssp ina-G
... | refl
  = subsume t≤t1 {!!}
compose ss ssp (bind ts ss₁ e₂ ϱ₂ κ₁) (ident ina-G unr-φ) = {!!}
compose ss ssp (bind ts ss₁ e₂ ϱ₂ κ₁) (bind ts₁ ss₂ e₃ ϱ₃ κ₂) = {!!}
compose ss ssp (bind ts ss₁ e₂ ϱ₂ κ₁) (subsume t≤t1 κ₂) = {!!}
compose ss ssp (subsume t≤t1 κ₁) (ident ina-G unr-φ) = {!!}
compose ss ssp (subsume t≤t1 κ₁) (bind ts ss₁ e₂ ϱ₂ κ₂) = {!!}
compose ss ssp (subsume t≤t1 κ₁) (subsume t≤t2 κ₂) = {!!}

-- command is a monad
data Command (G : SCtx) (t : Type) : Set where

  Return : (v : Val G t)
    → Command G t

  Fork : ∀ {φ₁ φ₂ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (κ₁ : Cont G₁ φ₁ TUnit TUnit)
    → (κ₂ : Cont G₂ φ₂ TUnit t)
    → Command G t

  New : ∀ {φ}
    → (s : SType)
    → (κ : Cont G φ (TPair (TChan (SType.force s)) (TChan (SType.force (dual s)))) t)
    → Command G t

  Close : ∀ {φ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (v : Val G₁ (TChan send!))
    → (κ : Cont G₂ φ TUnit t)
    → Command G t

  Wait  : ∀ {φ G₁ G₂}
    → (ss : SSplit G G₁ G₂)
    → (v : Val G₁ (TChan send?))
    → (κ : Cont G₂ φ TUnit t)
    → Command G t

  Send : ∀ {φ G₁ G₂ G₁₁ G₁₂ tv s}
    → (ss : SSplit G G₁ G₂)
    → (ss-args : SSplit G₁ G₁₁ G₁₂)
    → (vch : Val G₁₁ (TChan (send tv s)))
    → (v : Val G₁₂ tv)
    → (κ : Cont G₂ φ (TChan (SType.force s)) t)
    → Command G t

  Recv : ∀ {φ G₁ G₂ tv s}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (recv tv s)))
    → (κ : Cont G₂ φ (TPair (TChan (SType.force s)) tv) t)
    → Command G t

  Select : ∀ {φ G₁ G₂ s₁ s₂}
    → (ss : SSplit G G₁ G₂)
    → (lab : Selector)
    → (vch : Val G₁ (TChan (sintern s₁ s₂)))
    → (κ : Cont G₂ φ (TChan (selection lab (SType.force s₁) (SType.force s₂))) t)
    → Command G t

  Branch : ∀ {φ G₁ G₂ s₁ s₂}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (sextern s₁ s₂)))
    → (dcont : (lab : Selector) → Cont G₂ φ (TChan (selection lab (SType.force s₁) (SType.force s₂))) t)
    → Command G t

  NSelect : ∀ {φ G₁ G₂ m alt}
    → (ss : SSplit G G₁ G₂)
    → (lab : Fin m)
    → (vch : Val G₁ (TChan (sintN m alt)))
    → (κ : Cont G₂ φ (TChan (SType.force (alt lab))) t)
    → Command G t

  NBranch : ∀ {φ G₁ G₂ m alt}
    → (ss : SSplit G G₁ G₂)
    → (vch : Val G₁ (TChan (sextN m alt)))
    → (dcont : (lab : Fin m) → Cont G₂ φ (TChan (SType.force (alt lab))) t)
    → Command G t

-- cont G = ∀ G' → G ≤ G' → SSplit G' Gval Gcont → Val Gval t →

data _≼_ G : SCtx → Set where
  ≼-rfl : G ≼ G
  ≼-ext : ∀ {G'} → G ≼ G' → G ≼ (nothing ∷ G')

{-
mbindf : ∀ {Gin G1in G2in G1out G2out t t'} → SSplit Gin G1in G2in
  → Command G1in G1out t
  → (∀ G2in' G1out' G2out' → G2in ≼ G2in' → G1out ≼ G1out' → G2out ≼ G2out'
    → Val G1out' t → Command G2in' G2out' t')
  → Command Gin G2out t'
mbindf = {!!}
-}

mbind : ∀ {G G₁ G₂ Φ t t'} → SSplit G G₁ G₂ → Command G₁ t → Cont G₂ Φ t t' → Command G t'
mbind ssp (Return v) (ident x x₁)
  with inactive-right-ssplit ssp x
... | refl
  = Return v
mbind ssp (Return v) (bind ts ss e₂ ϱ₂ cont) = {!!}
mbind ssp (Return v) (subsume t≤t1 cont) = {!!}
mbind ssp (Fork ss κ₁ κ₂) cont = Fork {!!} κ₁ {!!}
mbind ssp (New s κ) cont = {!!}
mbind ssp (Close ss v κ) cont = {!!}
mbind ssp (Wait ss v κ) cont = {!!}
mbind ssp (Send ss ss-args vch v κ) cont = {!!}
mbind ssp (Recv ss vch κ) cont = {!!}
mbind ssp (Select ss lab vch κ) cont = {!!}
mbind ssp (Branch ss vch dcont) cont = {!!}
mbind ssp (NSelect ss lab vch κ) cont = {!!}
mbind ssp (NBranch ss vch dcont) cont = {!!}

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
module Hwequivalence where

open import Relation.Binary.PropositionalEquality
open import Data.Bool

-- A 1-bit adder
bit-adder-spec : Bool → Bool → Bool → Bool
bit-adder-spec A B C = X ∧ Y
  where
  X : Bool
  X = (A ∧ not B ∧ not C)
      ∨
      (not A ∧ B ∧ not C)
      ∨
      (not A ∧ not B ∧ C)
      ∨
      (A ∧ B ∧ C)

  Y : Bool
  Y = (A ∧ B)
      ∨
      (A ∧ C)
      ∨
      (B ∧ C)

bit-adder-imp : Bool → Bool → Bool → Bool
bit-adder-imp A B C = X ∧ Y
  where
  u : Bool
  u = (A ∧ not B)
      ∨
      (not A ∧ B)
  v : Bool
  v = u ∧ C
  w : Bool
  w = A ∧ B
  X : Bool
  X = (u ∧ not C)
      ∨
      (not u ∧ C)
  Y : Bool
  Y = (w ∨ v)

data _≃_ {A : Set} (f : A → A) (g : A → A) : Set where
  f≃g : ((x y : A) → (x ≡ y) → (f x ≡ g y)) → f ≃ g

-- Prove equivalence of specification and implementation using
-- ≃ data type.
equivalence-spec-imp : ∀ (A B : Bool) → (bit-adder-spec A B) ≃ (bit-adder-imp A B)
equivalence-spec-imp A B = f≃g (λ x y x₁ → prove x y x₁)
  where
  pr1 : (x y : Bool) → (bit-adder-spec x y true) ≡ (bit-adder-imp x y true)
  pr1 true true = refl
  pr1 true false = refl
  pr1 false true = refl
  pr1 false false = refl

  pr2 : (x y : Bool) → (bit-adder-spec x y false) ≡ (bit-adder-imp x y false)
  pr2 true true = refl
  pr2 true false = refl
  pr2 false true = refl
  pr2 false false = refl

  prove : (x y : Bool) → (p : x ≡ y) → (bit-adder-spec A B x) ≡ (bit-adder-imp A B y)
  prove true .true refl = pr1 A B
  prove false .false refl = pr2 A B


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

module Definition.Typed.Properties where

open import Definition.Untyped
open import Definition.Typed

open import Tools.Empty using (⊥; ⊥-elim)
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Escape context extraction

wfTerm : ∀ {Γ A t} → Γ ⊢ t ∷ A → ⊢ Γ
wfTerm (ℕⱼ ⊢Γ) = ⊢Γ
wfTerm (Πⱼ F ▹ G) = wfTerm F
wfTerm (var ⊢Γ x₁) = ⊢Γ
wfTerm (lamⱼ F t) with wfTerm t
wfTerm (lamⱼ F t) | ⊢Γ ∙ F′ = ⊢Γ
wfTerm (g ∘ⱼ a) = wfTerm a
wfTerm (zeroⱼ ⊢Γ) = ⊢Γ
wfTerm (sucⱼ n) = wfTerm n
wfTerm (natrecⱼ F z s n) = wfTerm z
wfTerm (conv t A≡B) = wfTerm t

wf : ∀ {Γ A} → Γ ⊢ A → ⊢ Γ
wf (ℕⱼ ⊢Γ) = ⊢Γ
wf (Uⱼ ⊢Γ) = ⊢Γ
wf (Πⱼ F ▹ G) = wf F
wf (univ A) = wfTerm A

wfEqTerm : ∀ {Γ A t u} → Γ ⊢ t ≡ u ∷ A → ⊢ Γ
wfEqTerm (refl t) = wfTerm t
wfEqTerm (sym t≡u) = wfEqTerm t≡u
wfEqTerm (trans t≡u u≡r) = wfEqTerm t≡u
wfEqTerm (conv t≡u A≡B) = wfEqTerm t≡u
wfEqTerm (Π-cong F F≡H G≡E) = wfEqTerm F≡H
wfEqTerm (app-cong f≡g a≡b) = wfEqTerm f≡g
wfEqTerm (β-red F t a) = wfTerm a
wfEqTerm (η-eq F f g f0≡g0) = wfTerm f
wfEqTerm (suc-cong n) = wfEqTerm n
wfEqTerm (natrec-cong F≡F′ z≡z′ s≡s′ n≡n′) = wfEqTerm z≡z′
wfEqTerm (natrec-zero F z s) = wfTerm z
wfEqTerm (natrec-suc n F z s) = wfTerm n

wfEq : ∀ {Γ A B} → Γ ⊢ A ≡ B → ⊢ Γ
wfEq (univ A≡B) = wfEqTerm A≡B
wfEq (refl A) = wf A
wfEq (sym A≡B) = wfEq A≡B
wfEq (trans A≡B B≡C) = wfEq A≡B
wfEq (Π-cong F F≡H G≡E) = wfEq F≡H

-- Reduction is a subset of conversion

subsetTerm : ∀ {Γ A t u} → Γ ⊢ t ⇒ u ∷ A → Γ ⊢ t ≡ u ∷ A
subsetTerm (natrec-subst F z s n⇒n′) =
  natrec-cong (refl F) (refl z) (refl s) (subsetTerm n⇒n′)
subsetTerm (natrec-zero F z s) = natrec-zero F z s
subsetTerm (natrec-suc n F z s) = natrec-suc n F z s
subsetTerm (app-subst t⇒u a) = app-cong (subsetTerm t⇒u) (refl a)
subsetTerm (β-red A t a) = β-red A t a
subsetTerm (conv t⇒u A≡B) = conv (subsetTerm t⇒u) A≡B

subset : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A ≡ B
subset (univ A⇒B) = univ (subsetTerm A⇒B)

subset*Term : ∀ {Γ A t u} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ t ≡ u ∷ A
subset*Term (id t) = refl t
subset*Term (t⇒t′ ⇨ t⇒*u) = trans (subsetTerm t⇒t′) (subset*Term t⇒*u)

subset* : ∀ {Γ A B} → Γ ⊢ A ⇒* B → Γ ⊢ A ≡ B
subset* (id A) = refl A
subset* (A⇒A′ ⇨ A′⇒*B) = trans (subset A⇒A′) (subset* A′⇒*B)

-- Can extract left-part of a reduction

redFirstTerm : ∀ {Γ t u A} → Γ ⊢ t ⇒ u ∷ A → Γ ⊢ t ∷ A
redFirstTerm (conv t⇒u A≡B) = conv (redFirstTerm t⇒u) A≡B
redFirstTerm (app-subst t⇒u a) = (redFirstTerm t⇒u) ∘ⱼ a
redFirstTerm (β-red A t a) = (lamⱼ A t) ∘ⱼ a
redFirstTerm (natrec-subst F z s n⇒n′) = natrecⱼ F z s (redFirstTerm n⇒n′)
redFirstTerm (natrec-zero F z s) = natrecⱼ F z s (zeroⱼ (wfTerm z))
redFirstTerm (natrec-suc n F z s) = natrecⱼ F z s (sucⱼ n)

redFirst : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A
redFirst (univ A⇒B) = univ (redFirstTerm A⇒B)

redFirst*Term : ∀ {Γ t u A} → Γ ⊢ t ⇒* u ∷ A → Γ ⊢ t ∷ A
redFirst*Term (id t) = t
redFirst*Term (t⇒t′ ⇨ t′⇒*u) = redFirstTerm t⇒t′

redFirst* : ∀ {Γ A B} → Γ ⊢ A ⇒* B → Γ ⊢ A
redFirst* (id A) = A
redFirst* (A⇒A′ ⇨ A′⇒*B) = redFirst A⇒A′

-- No neutral terms are well-formed in an empty context

noNe : ∀ {t A} → ε ⊢ t ∷ A → Neutral t → ⊥
noNe (var x₁ ()) (var x)
noNe (conv ⊢t x) (var n) = noNe ⊢t (var n)
noNe (⊢t ∘ⱼ ⊢t₁) (∘ₙ neT) = noNe ⊢t neT
noNe (conv ⊢t x) (∘ₙ neT) = noNe ⊢t (∘ₙ neT)
noNe (natrecⱼ x ⊢t ⊢t₁ ⊢t₂) (natrecₙ neT) = noNe ⊢t₂ neT
noNe (conv ⊢t x) (natrecₙ neT) = noNe ⊢t (natrecₙ neT)

-- Neutrals do not weak head reduce

neRedTerm : ∀ {Γ t u A} (d : Γ ⊢ t ⇒ u ∷ A) (n : Neutral t) → ⊥
neRedTerm (conv d x) n = neRedTerm d n
neRedTerm (app-subst d x) (∘ₙ n) = neRedTerm d n
neRedTerm (β-red x x₁ x₂) (∘ₙ ())
neRedTerm (natrec-subst x x₁ x₂ d) (natrecₙ n₁) = neRedTerm d n₁
neRedTerm (natrec-zero x x₁ x₂) (natrecₙ ())
neRedTerm (natrec-suc x x₁ x₂ x₃) (natrecₙ ())

neRed : ∀ {Γ A B} (d : Γ ⊢ A ⇒ B) (N : Neutral A) → ⊥
neRed (univ x) N = neRedTerm x N

-- Whnfs do not weak head reduce

whnfRedTerm : ∀ {Γ t u A} (d : Γ ⊢ t ⇒ u ∷ A) (w : Whnf t) → ⊥
whnfRedTerm (conv d x) w = whnfRedTerm d w
whnfRedTerm (app-subst d x) (ne (∘ₙ x₁)) = neRedTerm d x₁
whnfRedTerm (β-red x x₁ x₂) (ne (∘ₙ ()))
whnfRedTerm (natrec-subst x x₁ x₂ d) (ne (natrecₙ x₃)) = neRedTerm d x₃
whnfRedTerm (natrec-zero x x₁ x₂) (ne (natrecₙ ()))
whnfRedTerm (natrec-suc x x₁ x₂ x₃) (ne (natrecₙ ()))

whnfRed : ∀ {Γ A B} (d : Γ ⊢ A ⇒ B) (w : Whnf A) → ⊥
whnfRed (univ x) w = whnfRedTerm x w

whnfRed*Term : ∀ {Γ t u A} (d : Γ ⊢ t ⇒* u ∷ A) (w : Whnf t) → t PE.≡ u
whnfRed*Term (id x) Uₙ = PE.refl
whnfRed*Term (id x) Πₙ = PE.refl
whnfRed*Term (id x) ℕₙ = PE.refl
whnfRed*Term (id x) lamₙ = PE.refl
whnfRed*Term (id x) zeroₙ = PE.refl
whnfRed*Term (id x) sucₙ = PE.refl
whnfRed*Term (id x) (ne x₁) = PE.refl
whnfRed*Term (conv x x₁ ⇨ d) w = ⊥-elim (whnfRedTerm x w)
whnfRed*Term (x ⇨ d) (ne x₁) = ⊥-elim (neRedTerm x x₁)

whnfRed* : ∀ {Γ A B} (d : Γ ⊢ A ⇒* B) (w : Whnf A) → A PE.≡ B
whnfRed* (id x) w = PE.refl
whnfRed* (x ⇨ d) w = ⊥-elim (whnfRed x w)

-- Whr is deterministic

whrDetTerm : ∀{Γ t u A u′ A′} (d : Γ ⊢ t ⇒ u ∷ A) (d′ : Γ ⊢ t ⇒ u′ ∷ A′) → u PE.≡ u′
whrDetTerm (conv d x) d′ = whrDetTerm d d′
whrDetTerm d (conv d′ x₁) = whrDetTerm d d′
whrDetTerm (app-subst d x) (app-subst d′ x₁) rewrite whrDetTerm d d′ = PE.refl
whrDetTerm (app-subst d x) (β-red x₁ x₂ x₃) = ⊥-elim (whnfRedTerm d lamₙ)
whrDetTerm (β-red x x₁ x₂) (app-subst d x₃) = ⊥-elim (whnfRedTerm d lamₙ)
whrDetTerm (β-red x x₁ x₂) (β-red x₃ x₄ x₅) = PE.refl
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-subst x₃ x₄ x₅ d′) rewrite whrDetTerm d d′ = PE.refl
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-zero x₃ x₄ x₅) = ⊥-elim (whnfRedTerm d zeroₙ)
whrDetTerm (natrec-subst x x₁ x₂ d) (natrec-suc x₃ x₄ x₅ x₆) = ⊥-elim (whnfRedTerm d sucₙ)
whrDetTerm (natrec-zero x x₁ x₂) (natrec-subst x₃ x₄ x₅ d′) = ⊥-elim (whnfRedTerm d′ zeroₙ)
whrDetTerm (natrec-zero x x₁ x₂) (natrec-zero x₃ x₄ x₅) = PE.refl
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-subst x₄ x₅ x₆ d′) = ⊥-elim (whnfRedTerm d′ sucₙ)
whrDetTerm (natrec-suc x x₁ x₂ x₃) (natrec-suc x₄ x₅ x₆ x₇) = PE.refl

whrDet : ∀{Γ A B B′} (d : Γ ⊢ A ⇒ B) (d′ : Γ ⊢ A ⇒ B′) → B PE.≡ B′
whrDet (univ x) (univ x₁) = whrDetTerm x x₁

whrDet↘Term : ∀{Γ t u A u′} (d : Γ ⊢ t ↘ u ∷ A) (d′ : Γ ⊢ t ⇒* u′ ∷ A) → Γ ⊢ u′ ⇒* u ∷ A
whrDet↘Term (proj₁ , proj₂) (id x) = proj₁
whrDet↘Term (id x , proj₂) (x₁ ⇨ d′) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet↘Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ d′) =
  whrDet↘Term (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _) (whrDetTerm x x₁) (proj₁ , proj₂)) d′

whrDet*Term : ∀{Γ t u A u′} (d : Γ ⊢ t ↘ u ∷ A) (d′ : Γ ⊢ t ↘ u′ ∷ A) → u PE.≡ u′
whrDet*Term (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet*Term (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRedTerm x₁ proj₂)
whrDet*Term (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRedTerm x proj₄)
whrDet*Term (x ⇨ proj₁ , proj₂) (x₁ ⇨ proj₃ , proj₄) =
  whrDet*Term (proj₁ , proj₂) (PE.subst (λ x₂ → _ ⊢ x₂ ↘ _ ∷ _)
                                    (whrDetTerm x₁ x) (proj₃ , proj₄))

whrDet* : ∀{Γ A B B′} (d : Γ ⊢ A ↘ B) (d′ : Γ ⊢ A ↘ B′) → B PE.≡ B′
whrDet* (id x , proj₂) (id x₁ , proj₄) = PE.refl
whrDet* (id x , proj₂) (x₁ ⇨ proj₃ , proj₄) = ⊥-elim (whnfRed x₁ proj₂)
whrDet* (x ⇨ proj₁ , proj₂) (id x₁ , proj₄) = ⊥-elim (whnfRed x proj₄)
whrDet* (A⇒A′ ⇨ A′⇒*B , whnfB) (A⇒A″ ⇨ A″⇒*B′ , whnfB′) =
  whrDet* (A′⇒*B , whnfB) (PE.subst (λ x → _ ⊢ x ↘ _)
                                     (whrDet A⇒A″ A⇒A′)
                                     (A″⇒*B′ , whnfB′))

-- Identity of syntactic reduction

idRed:*: : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A :⇒*: A
idRed:*: A = [ A , A , id A ]

idRedTerm:*: : ∀ {Γ A t} → Γ ⊢ t ∷ A → Γ ⊢ t :⇒*: t ∷ A
idRedTerm:*: t = [ t , t , id t ]

-- U cannot be a term

UnotInA : ∀ {A Γ} → Γ ⊢ U ∷ A → ⊥
UnotInA (conv U∷U x) = UnotInA U∷U

UnotInA[t] : ∀ {A B t a Γ}
         → t [ a ] PE.≡ U
         → Γ ⊢ a ∷ A
         → Γ ∙ A ⊢ t ∷ B
         → ⊥
UnotInA[t] () x₁ (ℕⱼ x₂)
UnotInA[t] () x₁ (Πⱼ x₂ ▹ x₃)
UnotInA[t] x₁ x₂ (var x₃ here) rewrite x₁ = UnotInA x₂
UnotInA[t] () x₂ (var x₃ (there x₄))
UnotInA[t] () x₁ (lamⱼ x₂ x₃)
UnotInA[t] () x₁ (x₂ ∘ⱼ x₃)
UnotInA[t] () x₁ (zeroⱼ x₂)
UnotInA[t] () x₁ (sucⱼ x₂)
UnotInA[t] () x₁ (natrecⱼ x₂ x₃ x₄ x₅)
UnotInA[t] x x₁ (conv x₂ x₃) = UnotInA[t] x x₁ x₂

redU*Term′ : ∀ {A B U′ Γ} → U′ PE.≡ U → Γ ⊢ A ⇒ U′ ∷ B → ⊥
redU*Term′ U′≡U (conv A⇒U x) = redU*Term′ U′≡U A⇒U
redU*Term′ () (app-subst A⇒U x)
redU*Term′ U′≡U (β-red x x₁ x₂) = UnotInA[t] U′≡U x₂ x₁
redU*Term′ () (natrec-subst x x₁ x₂ A⇒U)
redU*Term′ U′≡U (natrec-zero x x₁ x₂) rewrite U′≡U = UnotInA x₁
redU*Term′ () (natrec-suc x x₁ x₂ x₃)

redU*Term : ∀ {A B Γ} → Γ ⊢ A ⇒* U ∷ B → ⊥
redU*Term (id x) = UnotInA x
redU*Term (x ⇨ A⇒*U) = redU*Term A⇒*U

-- Nothing reduces to U

redU : ∀ {A Γ} → Γ ⊢ A ⇒ U → ⊥
redU (univ x) = redU*Term′ PE.refl x

redU* : ∀ {A Γ} → Γ ⊢ A ⇒* U → A PE.≡ U
redU* (id x) = PE.refl
redU* (x ⇨ A⇒*U) rewrite redU* A⇒*U = ⊥-elim (redU x)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.FOL using  ( Formula ; _∈₂_ ; _∈₂_⇒_ )
open import Web.Semantic.DL.FOL.Model using ( _⊨f_ )
open import Web.Semantic.DL.Role using ( Role ; ⟨_⟩ ; ⟨_⟩⁻¹ )
open import Web.Semantic.DL.Role.Model using ( _⟦_⟧₂ ; ⟦⟧₂-resp-≈ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( Interp ; ≈-sym )

module Web.Semantic.DL.Role.Skolemization {Σ : Signature} where

rskolem : ∀ {Δ} → Role Σ → Δ → Δ → Formula Σ Δ
rskolem ⟨ r ⟩   x y = (x , y) ∈₂ r
rskolem ⟨ r ⟩⁻¹ x y = (y , x) ∈₂ r

rskolem⇒ : ∀ {Δ} → Role Σ → Δ → Δ → Formula Σ Δ → Formula Σ Δ
rskolem⇒ ⟨ r ⟩   x y F = (x , y) ∈₂ r ⇒ F
rskolem⇒ ⟨ r ⟩⁻¹ x y F = (y , x) ∈₂ r ⇒ F

rskolem-sound : ∀ I R x y → (I ⊨f rskolem R x y) → ((x , y) ∈ I ⟦ R ⟧₂)
rskolem-sound I ⟨ r ⟩   x y xy∈⟦r⟧ = xy∈⟦r⟧
rskolem-sound I ⟨ r ⟩⁻¹ x y yx∈⟦r⟧ = yx∈⟦r⟧

rskolem⇒-sound : ∀ I R x y F → (I ⊨f rskolem⇒ R x y F) → ((x , y) ∈ I ⟦ R ⟧₂) → (I ⊨f F)
rskolem⇒-sound I ⟨ r ⟩   x y F xy∈r⇒F xy∈⟦r⟧ = xy∈r⇒F xy∈⟦r⟧
rskolem⇒-sound I ⟨ r ⟩⁻¹ x y F yx∈r⇒F yx∈⟦r⟧ = yx∈r⇒F yx∈⟦r⟧

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic