text:
--{-# OPTIONS --rewriting #-}
--{-# OPTIONS --exact-split #-}
--{-# OPTIONS --show-implicit #-}
--{-# OPTIONS --allow-unsolved-metas #-}

module NaturalDeduction where

open import OscarPrelude
open import Delay
open import Successor
open import Membership
open import DecidableMembership renaming (DecidableMembership to RDecidableMembership)
open import VariableName
open import FunctionName
open import PredicateName
open import Arity
open import Vector
open import 𝕃ist
open import TermByFunctionNames
open import Term
--open import TermUnification
open import MGU-revised
open import HasNegation
open import Formula
open import IsFormula
open import 𝓕ormula
open import HasNeitherNor
open import IsLiteralFormula
open import LiteralFormula
open import IsPropositionalFormula
open import 𝓐ssertion
open import 𝓢equent
open import Sequent
open import 𝑱udgement
open import IsLiteralSequent
open import LiteralSequent
open import Problem
open import IsLiteralProblem
open import LiteralProblem
open import Element
open import Elements
open import TruthValue
open import Interpretation
open import HasSatisfaction
open import InterpretationEqualityExceptAtVariableName
open import HasDecidableSatisfaction
open import Validation
open import HasDecidableValidation
open import HasSubstantiveDischarge
open import HasDecidableSubstantiveDischarge
open import HasVacuousDischarge
open import HasSalvation
open import SubstantiveDischargeIsConsistent
open import SubstantiveDischargeIsReflexive
open import HasDecidableVacuousDischarge
open import HasDecidableSalvation
open import TermCode
open import TermNode
open import FindTermNode
open import Theorem1

-- infixr 1 ,_
-- pattern  ,_ p = _ , p

-- pattern ◁pattern c₁∈xs c₁≽s c₂∈xs c₂≽~s = , (((, (c₁∈xs , c₁≽s)) , (, (c₂∈xs , c₂≽~s))))

-- negationEliminationRule : (I : Interpretation) (φ : Formula) → I ⊨ ~ (~ φ) → I ⊨ φ
-- negationEliminationRule I φ (¬[I⊭φ×I⊭φ] , _) with I ⊨? φ
-- … | yes I⊨φ = I⊨φ
-- … | no I⊭φ = ⊥-elim $ ¬[I⊭φ×I⊭φ] $ I⊭φ , I⊭φ

-- -- justifieds simplification and ... more?
-- simplificationRule₁ : (I : Interpretation) (φ₁ φ₂ : Formula) → I ⊨ Formula.logical φ₁ φ₂ → I ⊨ Formula.logical φ₁ φ₁
-- simplificationRule₁ I φ₁ φ₂ x = (fst x) , (fst x)

-- simplificationRule₂ : (I : Interpretation) (φ₁ φ₂ : Formula) → I ⊨ Formula.logical φ₁ φ₂ → I ⊨ Formula.logical φ₂ φ₂
-- simplificationRule₂ I φ₁ φ₂ x = snd x , snd x

-- -- logical (logical (logical p p) q) (logical (logical p p) q)
-- {-
-- conditionalizationRule : (I : Interpretation) (p q : Formula) → I ⊨ q → I ⊨ (p ⊃ q ╱ (p ∷ []) )
-- conditionalizationRule I p q ⊨q (_ , _) = let prf = λ { (_ , ⊭q) → ⊭q ⊨q} in prf , prf
-- --let ⊨p = {!-⊨p p (here [])!} in (λ { (x , ~q) → ~q ⊨q}) , (λ { (x , y) → y ⊨q})
-- -}

-- modusPonens : (I : Interpretation) (p q : Formula) → I ⊨ p → I ⊨ (p ⊃ q) → I ⊨ q
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) with I ⊨? q
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) | yes x = x
-- modusPonens I p q P (~[~p&~p&~q] , ~[~p&~p&~q]²) | no x = ⊥-elim (~[~p&~p&~q] ((λ { (x₁ , y) → y P}) , (λ x₁ → x x₁)))

-- -- -- -- -- -- data SkolemFormula {ι : Size} (α : Alphabet) : Set where
-- -- -- -- -- --   atomic : Predication α → SkolemFormula α
-- -- -- -- -- --   logical : {ι¹ : Size< ι} → SkolemFormula {ι¹} α → {ι² : Size< ι} → SkolemFormula {ι²} α → SkolemFormula {ι} α

-- -- -- -- -- -- record Alphabet₊ᵥ (α : Alphabet) : Set where
-- -- -- -- -- --   constructor α₊ᵥ⟨_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     alphabet : Alphabet
-- -- -- -- -- --     .one-variable-is-added : (number ∘ variables $ alphabet) ≡ suc (number ∘ variables $ α)
-- -- -- -- -- --     .there-are-no-functions-of-maximal-arity : number (functions alphabet) zero ≡ zero
-- -- -- -- -- --     .shifted-function-matches : ∀ {ytira₀ ytira₁} → finToNat ytira₁ ≡ finToNat ytira₀ → number (functions alphabet) (suc ytira₁) ≡ number (functions α) ytira₀
-- -- -- -- -- -- open Alphabet₊ᵥ

-- -- -- -- -- -- record Alphabet₊ₛ (α : Alphabet) : Set where
-- -- -- -- -- --   constructor α₊ₛ⟨_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     alphabet : Alphabet
-- -- -- -- -- -- open Alphabet₊ₛ

-- -- -- -- -- -- {-
-- -- -- -- -- --   toSkolemFormula
-- -- -- -- -- --   ∀x(F x v₀ v₁) ⟿ F v₀ v₁ v₂
-- -- -- -- -- --   ∃x(F x v₀ v₁) ⟿ F (s₀͍₂ v₀ v₁) v₀ v₁
-- -- -- -- -- --   ∀x(F x (s₀͍₂ v₀ v₁) v₁) ⟿ F v₀ (s₀͍₂ v₁ v₂) v₂
-- -- -- -- -- --   ∃x(F x (s₀͍₂ v₀ v₁) v₁) ⟿ F (s₀͍₂ v₀ v₁) (s₁͍₂ v₁ v₂) v₂
-- -- -- -- -- --   F v₀ ⊗ G v₀ ⟿ F v₀ ⊗ G v₀
-- -- -- -- -- --   ∀x(F x v₀ v₁) ⊗ ∀x(G x (s₀͍₂ x v₁) v₁) ⟿ F v₀ v₂ v₃ ⊗ G v₁ (s₀͍₂ v₀ v₃) v₃

-- -- -- -- -- --   ∀x(F x v₀ v₁) ⊗ ∃x(G x (s₀͍₂ x v₁) v₁) ⟿ F v₀ v₁ v₂ ⊗ G (s₀͍₁ v₂) (s₁͍₂ (s₀͍₂ v₂) v₂) v₂

-- -- -- -- -- --   Φ₀ = ∃x(G x (s₀͍₂ x v₁) v₁) has alphabet of 2 variables, skolem functions: 0, 0, 1
-- -- -- -- -- --   this is existential {α₊ₛ} Φ₁, where
-- -- -- -- -- --     Φ₁ = G (s₀͍₂ v₀ v₁) (s₁͍₂ (s₀͍₂ v₀ v₁)) v₁
-- -- -- -- -- --     α₊ₛ = ⟨ 2 , 0 ∷ 0 ∷ 2 ∷ [] ⟩

-- -- -- -- -- --   maybe Φ₋₁ = ∀y∃x(G x (s₀͍₂ x v₀) v₀)
-- -- -- -- -- --    and  Φ₋₂ = ∀z∀y∃x(G x (s₀͍₂ x z) z), finally having no free variables, but nevertheless having skolem functions! these are user-defined functions, so this notion of Alphabet is somehow wrong. we have also left out constants (i.e. user-defined skolem-functions of arity 0)

-- -- -- -- -- --   Instead, take the alphabet as defining
-- -- -- -- -- --     a stack of free variables
-- -- -- -- -- --     a matrix (triangle?) of skolem functions

-- -- -- -- -- --   Let's try to reverse Φ₁ from a Skolem to a 1st-order formula. Is there a unique way to do it?
-- -- -- -- -- --   Φ₀' = ∀x(G (s₀͍₂ x v₀) (s₁͍₂ (s₀͍₂ x v₀)) v₀

-- -- -- -- -- --   Nope!

-- -- -- -- -- --   toSkolemFormula of

-- -- -- -- -- -- -}

-- -- -- -- -- -- -- toSkolemFormula (logical Φ₁ Φ₂) ⟿
-- -- -- -- -- -- --   let α' , φ₁ = toSkolemFormula Φ₁
-- -- -- -- -- -- --       Φ₂' = transcodeToAugmentedAlphabet Φ₂ α'
-- -- -- -- -- -- --       α'' , φ₂' = toSkolemFormula Φ₂'
-- -- -- -- -- -- --       φ₁' = transcodeToAugmentedAlphabet φ₁ α''

-- -- -- -- -- -- {-
-- -- -- -- -- -- given Δv = #varibles α' - #variables α
-- -- -- -- -- -- for every variable v in α, v in Φ, v stays the same in Φ'
-- -- -- -- -- -- for the added variable v⁺ in α₊ - α, v⁺ in Φ, v⁺ ⟿ v⁺ + Δv in transcode (universal {α₊} Φ)
-- -- -- -- -- -- α'₊ = α' + 1 variable
-- -- -- -- -- -- -}

-- -- -- -- -- -- -- record AddVariable (A : Alphabet → Set) : Set where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     addVariableToAlphabet : {α : Alphabet} → A α → {α₊ : Alphabet} → Alphabet₊ᵥ α₊ → A α₊

-- -- -- -- -- -- -- instance
-- -- -- -- -- -- --   AddVariableFirstOrderFormula : AddVariable FirstOrderFormula
-- -- -- -- -- -- --   AddVariableFirstOrderFormula = {!!}

-- -- -- -- -- -- -- #variables = number ∘ variables

-- -- -- -- -- -- -- #functions_ofArity_ : Alphabet → Nat → Nat
-- -- -- -- -- -- -- #functions α⟨ V⟨ #variables ⟩ , S⟨ #functions ⟩ ⟩ ofArity arity = if′ lessNat arity (suc #variables) then #functions (natToFin arity) else 0

-- -- -- -- -- -- -- record _⊇_ (α' α : Alphabet) : Set where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     at-least-as-many-variables : #variables α' ≥ #variables α
-- -- -- -- -- -- --     at-least-as-many-functions : ∀ {arity} → arity < #variables α → #functions α' ofArity arity ≥ #functions α ofArity arity

-- -- -- -- -- -- -- record AddAlphabet (α-top α-bottom : Alphabet) : Set where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     alphabet : Alphabet

-- -- -- -- -- -- -- record Transcodeable (A : Alphabet → Set) : Set where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     transcode : {α' α : Alphabet} → ⦃ _ : α' ⊇ α ⦄ → A α → A α'

-- -- -- -- -- -- -- open Transcodeable ⦃ … ⦄

-- -- -- -- -- -- -- record TransferAlphabet {α' α : Alphabet} (α'⊇α : α' ⊇ α) (α₊ : Alphabet₊ᵥ α) (Φ : FirstOrderFormula (alphabet α₊)) : Set where
-- -- -- -- -- -- --   field
-- -- -- -- -- -- --     alphabet : Alphabet
-- -- -- -- -- -- --     firstOrderFormula : FirstOrderFormula alphabet

-- -- -- -- -- -- -- instance
-- -- -- -- -- -- --   TranscodeablePredication : Transcodeable Predication
-- -- -- -- -- -- --   TranscodeablePredication = {!!}

-- -- -- -- -- -- --   TranscodeableAlphabet+Variable : Transcodeable Alphabet₊ᵥ
-- -- -- -- -- -- --   TranscodeableAlphabet+Variable = {!!}

-- -- -- -- -- -- --   TranscodeableSkolemFormula : Transcodeable SkolemFormula
-- -- -- -- -- -- --   TranscodeableSkolemFormula = {!!}

-- -- -- -- -- -- --   TranscodeableFirstOrderFormula : Transcodeable FirstOrderFormula
-- -- -- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (atomic p) = atomic (transcode p)
-- -- -- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (logical Φ₁ Φ₂) = logical (transcode Φ₁) (transcode Φ₂)
-- -- -- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula {α'} {α} ⦃ α'⊇α ⦄ (universal {α₊} Φ) = {!!} -- universal {_} {_} {transcode α₊} (transcode Φ)

-- -- -- -- -- -- --   Transcodeable.transcode TranscodeableFirstOrderFormula (existential Φ) = {!!}

-- -- -- -- -- -- -- --(α' α : Alphabet) (α'⊇α : α' ⊇ α) (α₊ : Alphabet+Variable α) (Φ : FirstOrderFormula (alphabet α₊)) → Σ _ λ (α''' : Alphabet) → FirstOrderFormula α'''

-- -- -- -- -- -- -- --FirstOrderFormula (alphabet α₊)
-- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- --transcodeIntoAugmentedAlphabet :

-- -- -- -- -- -- -- -- --toSkolemFormula : {α : Alphabet} → FirstOrderFormula α → Σ _ λ (α¹ : AugmentedAlphabet α) → SkolemFormula (alphabet α¹)

-- -- -- -- -- -- -- -- --record IsEquivalentFormulas {α₀ : Alphabet} (φ₀ : SkolemFormula α₀) {α₁ : Alphabet} (Φ₁ : FirstOrderFormula α₁) : Set where
-- -- -- -- -- -- -- -- --  field
-- -- -- -- -- -- -- -- --    .atomicCase : {p : Predication α₀} → φ₀ ≡ atomic p → Φ₁ ≡ atomic p

-- -- -- -- -- -- -- -- -- --
-- -- -- -- -- -- -- -- -- -- record Alphabet+Alphabet (α₀ α₁ α₂ : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- --     alphabet :

-- -- -- -- -- -- -- -- -- -- ∀xφ₁(x) ⊗ φ₂ ⟿ ∀x(φ₁ ⊗ φ₂)

-- -- -- -- -- -- -- -- -- -- hasQuantifiers : FirstOrderFormula α → Bool

-- -- -- -- -- -- -- -- -- --record Skolemization {α : Alphabet} (φ : FirstOrderFormula α) : Set where
-- -- -- -- -- -- -- -- -- --  field
-- -- -- -- -- -- -- -- -- --    alphabet : Alphabet
-- -- -- -- -- -- -- -- -- --    skolemization : SkolemFormula alphabet

-- -- -- -- -- -- -- -- -- record _IsAugmentationOf_ (α₁ α₀ : Alphabet) : Set where

-- -- -- -- -- -- -- -- -- record AugmentedAlphabet (α : Alphabet) : Set where
-- -- -- -- -- -- -- -- --   constructor ⟨_⟩
-- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- --     alphabet : Alphabet
-- -- -- -- -- -- -- -- --     ..laws : alphabet ≡ α
-- -- -- -- -- -- -- -- -- open AugmentedAlphabet

-- -- -- -- -- -- -- -- -- trivialAugmentation : (α : Alphabet) → AugmentedAlphabet α
-- -- -- -- -- -- -- -- -- trivialAugmentation = {!!}

-- -- -- -- -- -- -- -- -- record DisjointRelativeUnion {α : Alphabet} (α¹ α² : AugmentedAlphabet α) : Set where
-- -- -- -- -- -- -- -- --   constructor ⟨_⟩
-- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- --     augmentation : AugmentedAlphabet α
-- -- -- -- -- -- -- -- --     .laws : {!!}
-- -- -- -- -- -- -- -- -- open DisjointRelativeUnion

-- -- -- -- -- -- -- -- -- disjointRelativeUnion : {α : Alphabet} → (α¹ α² : AugmentedAlphabet α) → DisjointRelativeUnion α¹ α²
-- -- -- -- -- -- -- -- -- disjointRelativeUnion = {!!}

-- -- -- -- -- -- -- -- -- -- inAugmentedAlphabet : {α : Alphabet} → (α¹ : AugmentedAlphabet α) → SkolemFormula α → SkolemFormula (alphabet α¹)
-- -- -- -- -- -- -- -- -- -- inAugmentedAlphabet = {!!}

-- -- -- -- -- -- -- -- -- -- toSkolemFormula : {α : Alphabet} → FirstOrderFormula α → Σ _ λ (α¹ : AugmentedAlphabet α) → SkolemFormula (alphabet α¹)
-- -- -- -- -- -- -- -- -- -- toSkolemFormula {α₀} (atomic 𝑃) = trivialAugmentation α₀ , atomic 𝑃
-- -- -- -- -- -- -- -- -- -- toSkolemFormula {α₀} (logical φ₁ φ₂) with toSkolemFormula φ₁ | toSkolemFormula φ₂
-- -- -- -- -- -- -- -- -- -- toSkolemFormula {α₀} (logical φ₁ φ₂) | α¹ , Φ₁ | α² , Φ₂ = augmentation (disjointRelativeUnion α¹ α²) , logical {!inAugmentedAlphabet (augmentation (disjointRelativeUnion α¹ α²)) Φ₁!} {!Φ₂!}
-- -- -- -- -- -- -- -- -- -- toSkolemFormula {α₀} (universal x) = {!!}
-- -- -- -- -- -- -- -- -- -- toSkolemFormula {α₀} (existential x) = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula : ∀ {alphabet₀} → QFormula alphabet₀ → Σ _ λ alphabet₁ → NQFormula alphabet₁
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (atomic name terms) = alphabet₀ , atomic name terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (logical formula₁ formula₂) with toNQFormula formula₁ | toNQFormula formula₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- … | alphabet₁ , nqFormula₁ | alphabet₂ , nqFormula₂ = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (universal formula) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (existential formula) = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- --VariableName = Fin ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- -- -- --FunctionArity = Fin ∘ suc ∘ size
-- -- -- -- -- -- -- -- -- -- -- -- -- --FunctionName = λ alphabet ytira → Fin (|f| alphabet ytira)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- record Alphabet : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- --     |v| : Nat -- number of variables
-- -- -- -- -- -- -- -- -- -- -- -- -- --     |f| : Fin (suc |v|) → Nat -- number of functions of each arity, |v| through 0

-- -- -- -- -- -- -- -- -- -- -- -- -- -- open Alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- VariableName = Fin ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- FunctionArity = Fin ∘ suc ∘ |v|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- FunctionName = λ alphabet ytira → Fin (|f| alphabet ytira)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Term {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   variable : VariableName alphabet → Term alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   function : ∀ {arity : FunctionArity alphabet} →
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --              FunctionName alphabet (natToFin (|v| alphabet) - arity) →
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --              ∀ {j : Size< i} → Vec (Term {j} alphabet) (finToNat arity) →
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --              Term {i} alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- PredicateArity = Nat
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- PredicateName = Nat

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a zeroth-order formula? (i.e. no quantifiers)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data NQFormula {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   atomic : PredicateName → ∀ {arity} → Vec (Term alphabet) arity → NQFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   logical : {j : Size< i} → NQFormula {j} alphabet → {k : Size< i} → NQFormula {k} alphabet → NQFormula {i} alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentedByVariable (alphabet₀ alphabet₁ : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     one-variable-is-added : |v| alphabet₁ ≡ suc (|v| alphabet₀)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     function-domain-is-zero-at-new-variable : |f| alphabet₁ zero ≡ 0
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     shifted-function-matches : ∀ {ytira₀ ytira₁} → finToNat ytira₁ ≡ finToNat ytira₀ → |f| alphabet₁ (suc ytira₁) ≡ |f| alphabet₀ ytira₀

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentVariables (alphabet₀ : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     alphabet₁ : Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     augmentation : AugmentedByVariable alphabet₀ alphabet₁

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- open AugmentVariables

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables : (alphabet : Alphabet) → AugmentVariables alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables ⟨ |v| , |f| ⟩ =
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   record
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   { alphabet₁ = ⟨ suc |v| , (λ { zero → zero ; (suc ytira) → |f| ytira}) ⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   ; augmentation =
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     record
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     { one-variable-is-added = refl
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     ; function-domain-is-zero-at-new-variable = refl
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     ; shifted-function-matches = cong |f| ∘ finToNat-inj } }

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- |f|₀ = |f|₀ + 1
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions : Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions ⟨ |v| , |f| ⟩ = ⟨ |v| , (λ { zero → suc (|f| zero) ; (suc ytira) → |f| (suc ytira) }) ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data QFormula {i : Size} (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   atomic : PredicateName → ∀ {arity} → Vec (Term alphabet) arity → QFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   logical : {j : Size< i} → QFormula {j} alphabet → {k : Size< i} → QFormula {k} alphabet → QFormula {i} alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   universal : QFormula (alphabet₁ (augmentVariables alphabet)) → QFormula alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   existential : QFormula (augmentFunctions alphabet) → QFormula alphabet

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Assignment (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     μ : VariableName alphabet → Domain
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑓 : ∀ {arity} → FunctionName alphabet arity → Vec Domain (finToNat arity) → Domain

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm : ∀ {i alphabet} → Assignment alphabet → Term {i} alphabet → Domain
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm ⟨ μ , _ ⟩ (variable x) = μ x
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateTerm 𝑎@(⟨ μ , 𝑓 ⟩) (function f x) = 𝑓 f (evaluateTerm 𝑎 <$> x)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Interpretation (alphabet : Alphabet) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   constructor ⟨_,_⟩
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   open Assignment
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑎 : Assignment alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     𝑃 : PredicateName → ∀ {arity} → Vec Domain arity → Bool

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula : ∀ {i alphabet} → Interpretation alphabet → NQFormula {i} alphabet → Bool
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula ⟨ 𝑎 , 𝑃 ⟩ (atomic name terms) = 𝑃 name $ evaluateTerm 𝑎 <$> terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- evaluateNQFormula I (logical formula₁ formula₂) = not (evaluateNQFormula I formula₁) && not (evaluateNQFormula I formula₂)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula : ∀ {alphabet₀} → QFormula alphabet₀ → Σ _ λ alphabet₁ → NQFormula alphabet₁
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (atomic name terms) = alphabet₀ , atomic name terms
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (logical formula₁ formula₂) with toNQFormula formula₁ | toNQFormula formula₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- … | alphabet₁ , nqFormula₁ | alphabet₂ , nqFormula₂ = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (universal formula) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- toNQFormula {alphabet₀} (existential formula) = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record IsADisjointUnionOfNQFormulas
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --        {alphabet₁ alphabet₂ alphabet₁₊₂ : Alphabet}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₁ : NQFormula alphabet₁)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₂ : NQFormula alphabet₂)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --        (formula₁₊₂ : NQFormula alphabet₁₊₂)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --        : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     alphabet-size : |v| alphabet₁₊₂ ≡ |v| alphabet₁ + |v| alphabet₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     --|f| alphabet₁₊₂ ytira

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ----record AlphabetSummed  (alphabet₀ alphabet₁ : Alphabet)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --addAlphabets : Alphabet → Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --addAlphabets ⟨ |v|₁ , |f|₁ ⟩ ⟨ |v|₂ , |f|₂ ⟩ = ⟨ (|v|₁ + |v|₂) , (λ x → if′ finToNat x ≤? |v|₁ && finToNat x ≤? |v|₂ then {!!} else {!!}) ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- sup : ∀ {alphabet₁} → Formula alphabet₁ → ∀ {alphabet₂} → Formula alphabet₂ → Σ _ λ alphabet₁₊₂ → Formula alphabet₁₊₂ × Formula alphabet₁₊₂
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- sup {⟨ |v|₁ , |a|₁ , |f|₁ ⟩} φ₁ {⟨ |v|₂ , |a|₂ , |f|₂ ⟩} φ₂ = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- pnf : ∀ {alphabet} → Formula alphabet → Σ _ λ alphabet+ → Formula₀ alphabet+
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- pnf = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --universal (P 0) = ∀ x → P x
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- (∀ x ∃ y (P x y)) ∨ (∀ x ∃ y (P x y))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- P x₀ (s₀͍₁ x₀) ∨ P x₁ (s₁͍₁ x₁)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   extended|f| : (arity : Arity) → Vec ℕ (suc |a|) → Vec ℕ (++arity (max arity |a|))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   extended|f| = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- add a variable to the alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables : Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentVariables = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- increaseTabulationAtN : ∀ {n} → Fin n → (Fin n → Nat) → Fin n → Nat
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- increaseTabulationAtN = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record AugmentedFunctions {|a| : Arity} (arity : Arity) (|f| : Vec ℕ (++arity |a|)) : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     maxA : ℕ
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     maxA-law : max arity |a| ≡ maxA
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     ++|f| : Vec ℕ maxA
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     f-law : increaseTabulationAt arity (indexVec |f|)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- {-

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- define
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ⊗ b ≡ False a and False b

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- now, we can define
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ¬a = a ⊗ a ≡ False a and False a
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ∨ b = ¬(a ⊗ b) ≡ False (False a and False b) and False (False a and False b)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a ∧ b = ¬(¬a ∨ ¬b) = ¬(¬(¬a ⊗ ¬b)) = ¬a ⊗ ¬b = False (False a and False a) and False (False b and False b)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- a → b = ¬a ∨ b = (a ⊗ a) ∨ b = ¬((a ⊗ a) ⊗ b) = ((a ⊗ a) ⊗ b) ⊗ ((a ⊗ a) ⊗ b)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- conversion to prenex
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ∀xF ⊗ G ⟿ ∃x(F ⊗ wk(G))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ∃xF ⊗ G ⟿ ∀x(F ⊗ wk(G))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- F ⊗ ∀xG ⟿ ∃x(wk(F) ⊗ G)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- F ⊗ ∃xG ⟿ ∀x(wk(F) ⊗ G)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- ========================
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- (a ⊗ ∀xB) ⊗ c ⟿ ∃x(wk(a) ⊗ B) ⊗ c ⟿ ∀x((wk(a) ⊗ B) ⊗ wk(c))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF : (arity : Arity) → ∀ {|a| : Arity} → Vec ℕ (++arity |a|) → Vec ℕ (++arity (max arity |a|))
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --  with decBool (lessNat |a| arity)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | yes x with compare arity |a|
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.(suc (k + arity))} |f| | yes x | less (diff k refl) = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.arity} |f| | yes x | equal refl with lessNat arity arity
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {.arity} |f| | yes x | equal refl | false = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF zero {.zero} |f| | yes true | equal refl | true = {!!} ∷ []
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF (suc arity) {.(suc arity)} |f| | yes true | equal refl | true = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | yes x | greater gt = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x with decBool (lessNat arity |a|)
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x₁ | yes x = {!!}
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentF arity {|a|} |f| | no x₁ | no x = {!!}

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- = case arity <? |a| of λ { false → {!!} ; true → {!!} }

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- add a function of a given arity to the alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions : Arity → Alphabet → Alphabet
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- augmentFunctions arity ⟨ |v| , |a| , |f| ⟩ = ⟨ |v| , max arity |a| , augmentF arity |f| ⟩

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Alphabet : Set where

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data DomainSignifier : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   free : Nat → DomainSignifier

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data PartiallyAppliedFunction : Nat → Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   constant : PartiallyAppliedFunction 0
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   function : ∀ {n} → PartiallyAppliedFunction 0 → PartiallyAppliedFunction (suc n)

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Term = PartiallyAppliedFunction 0

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data PartialyAppliedPredicate : Nat → Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   statement : PartialyAppliedPredicate 0
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   partial : ∀

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Language : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Name = String

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- record Function : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   field
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     name : Name
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --     number-of-arguments : Nat

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- Vec

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Function : Set where

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Term : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   function : Function →

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- data Sentence : Set where
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --   predication : Name →

-- -- -- -- -- -- {-

-- -- -- -- -- -- record Variables : Set where
-- -- -- -- -- --   constructor V⟨_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     number : Nat
-- -- -- -- -- -- open Variables

-- -- -- -- -- -- record Functions (υ : Variables) : Set where
-- -- -- -- -- --   constructor S⟨_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     number : Fin (suc (number υ)) → Nat
-- -- -- -- -- -- open Functions

-- -- -- -- -- -- record Alphabet : Set where
-- -- -- -- -- --   constructor α⟨_,_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     variables : Variables
-- -- -- -- -- --     functions : Functions variables
-- -- -- -- -- -- open Alphabet

-- -- -- -- -- -- record Variable (α : Alphabet) : Set where
-- -- -- -- -- --   constructor v⟨_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     name : Fin (number (variables α))
-- -- -- -- -- -- open Variable

-- -- -- -- -- -- record Function (α : Alphabet) : Set where
-- -- -- -- -- --   constructor s⟨_,_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     arity : Fin ∘ suc ∘ number ∘ variables $ α
-- -- -- -- -- --     name : Fin $ number (functions α) arity
-- -- -- -- -- -- open Function

-- -- -- -- -- -- data Term (𝑽 : Nat) : Set where
-- -- -- -- -- --   variable : Fin 𝑽 → Term 𝑽
-- -- -- -- -- --   function : (𝑓 : Function α) → {ι₋₁ : Size< ι₀} → Vec (Term {ι₋₁} α) (finToNat (arity 𝑓)) →
-- -- -- -- -- --              Term {ι₀} α

-- -- -- -- -- -- record Predication (alphabet : Alphabet) : Set where
-- -- -- -- -- --   constructor P⟨_,_,_⟩
-- -- -- -- -- --   field
-- -- -- -- -- --     name : Nat
-- -- -- -- -- --     arity : Nat
-- -- -- -- -- --     terms : Vec (Term alphabet) arity
-- -- -- -- -- -- open Predication
-- -- -- -- -- -- -}

-- -- module NotUsed where

-- --   -- thought it might be easier to use this
-- --   module UsingContainerList where

-- --     record TermNode : Set
-- --      where
-- --       inductive
-- --       field
-- --         children : List (TermCode × TermNode)
-- --         number : Nat

-- --     open TermNode

-- --     _child∈_ : TermCode → TermNode → Set
-- --     _child∈_ 𝔠 𝔫 = Any ((𝔠 ≡_) ∘ fst) (children 𝔫)

-- --   -- this still has a lambda problem, albeit weirder
-- --   module RememberChildren where

-- --     record TermNode : Set
-- --      where
-- --       inductive
-- --       field
-- --         tests : List TermCode
-- --         children : ∀ {𝔠} → 𝔠 ∈ tests → TermNode
-- --         number : Nat
-- --     open TermNode

-- --     addChild : {𝔠 : TermCode} (𝔫 : TermNode) → 𝔠 ∉ tests 𝔫 → TermNode → TermNode
-- --     addChild {𝔠} 𝔫 𝔠∉tests𝔫 𝔫' =
-- --       record 𝔫
-- --       { tests = 𝔠 ∷ tests 𝔫
-- --       ; children = λ
-- --         { (here _) → 𝔫'
-- --         ; (there _ 𝔠'∈tests) → children 𝔫 𝔠'∈tests }}

-- --     setChild : {𝔠 : TermCode} (𝔫 : TermNode) → 𝔠 ∈ tests 𝔫 → TermNode → TermNode
-- --     setChild {𝔠} 𝔫 𝔠∈tests𝔫 𝔫' =
-- --       record 𝔫
-- --       { children = λ {𝔠'} 𝔠'∈tests𝔫' → ifYes 𝔠' ≟ 𝔠 then 𝔫' else children 𝔫 𝔠'∈tests𝔫' }

-- --     storeTermCodes : List TermCode → Nat → StateT TermNode Identity Nat
-- --     storeTermCodes [] 𝔑 = return 𝔑
-- --     storeTermCodes (𝔠 ∷ 𝔠s) 𝔑 =
-- --       𝔫 ← get -|
-- --       case 𝔠 ∈? tests 𝔫 of λ
-- --       { (no 𝔠∉tests) →
-- --         let 𝔑' , 𝔫' = runIdentity $
-- --                       runStateT
-- --                         (storeTermCodes 𝔠s $ suc 𝔑)
-- --                         (record
-- --                           { tests = []
-- --                           ; children = λ ()
-- --                           ; number = suc 𝔑 }) in
-- --         put (addChild 𝔫 𝔠∉tests 𝔫') ~|
-- --         return 𝔑'
-- --       ; (yes 𝔠∈tests) →
-- --         let 𝔑' , 𝔫' = runIdentity $
-- --                       runStateT
-- --                         (storeTermCodes 𝔠s $ suc 𝔑)
-- --                         (children 𝔫 𝔠∈tests) in
-- --         put (setChild 𝔫 𝔠∈tests 𝔫') ~|
-- --         return 𝔑' }

-- --     topNode : TermNode
-- --     topNode = record { tests = [] ; children = λ () ; number = 0 }

-- --     example-store : TermNode
-- --     example-store = snd ∘ runIdentity $ runStateT (storeTermCodes example-TermCodes 0) topNode

-- --     foo : TermNode × TermNode
-- --     foo =
-- --       {!example-store!} ,
-- --       {!snd ∘ runIdentity $ runStateT (storeTermCodes example-TermCodes 10) example-store!}

-- --   -- using a lambda for the children results in extra unnecessary structure when adding to an existing node; perhaps using an explicit mapping? or use another field to state what codes are present in the mapping?
-- --   module NoParents where

-- --     mutual

-- --       record TermNode : Set
-- --        where
-- --         inductive
-- --         field
-- --           children : TermCode → Maybe TermNode -- Map TermCode TermNode
-- --           self : TermCode
-- --           number : Nat

-- --       record TopTermNode : Set
-- --        where
-- --         inductive
-- --         field
-- --           children : TermCode → Maybe TermNode

-- --     open TermNode
-- --     open TopTermNode

-- --     storeTermCodes : List TermCode → Nat → StateT TermNode Identity ⊤
-- --     storeTermCodes [] _ = return tt
-- --     storeTermCodes (𝔠 ∷ 𝔠s) 𝔑 =
-- --       𝔫 ← get -|
-- --       case children 𝔫 𝔠 of λ
-- --       { nothing →
-- --         put
-- --           (record 𝔫
-- --             { children =
-- --               λ 𝔠' →
-- --               ifYes 𝔠' ≟ 𝔠 then
-- --                 just ∘ snd ∘ runIdentity $
-- --                 (runStateT
-- --                   (storeTermCodes 𝔠s (suc 𝔑))
-- --                     (record
-- --                       { self = 𝔠
-- --                       ; children = const nothing
-- --                       ; number = suc 𝔑 }))
-- --               else
-- --                 children 𝔫 𝔠' } ) ~|
-- --         return tt
-- --       ; (just 𝔫') →
-- --         put (record 𝔫
-- --               { children =
-- --                 λ 𝔠' →
-- --                 ifYes 𝔠' ≟ 𝔠 then
-- --                   just ∘ snd ∘ runIdentity $
-- --                   runStateT (storeTermCodes 𝔠s 𝔑) 𝔫'
-- --                 else
-- --                   children 𝔫 𝔠' }) ~|
-- --         return tt }

-- --     storeTermCodesAtTop : List TermCode → Nat → StateT TopTermNode Identity ⊤
-- --     storeTermCodesAtTop [] _ = return tt
-- --     storeTermCodesAtTop (𝔠 ∷ 𝔠s) 𝔑 =
-- --       𝔫 ← get -|
-- --       case children 𝔫 𝔠 of λ
-- --       { nothing →
-- --         put
-- --           (record 𝔫
-- --             { children =
-- --               λ 𝔠' →
-- --               ifYes 𝔠' ≟ 𝔠 then
-- --                 just ∘ snd ∘ runIdentity $
-- --                 (runStateT
-- --                   (storeTermCodes 𝔠s (suc 𝔑))
-- --                     (record
-- --                       { self = 𝔠
-- --                       ; children = const nothing
-- --                       ; number = suc 𝔑 }))
-- --               else
-- --                 children 𝔫 𝔠' } ) ~|
-- --         return tt
-- --       ; (just 𝔫') →
-- --         put (record 𝔫
-- --               { children =
-- --                 λ 𝔠' →
-- --                 ifYes 𝔠' ≟ 𝔠 then
-- --                   just ∘ snd ∘ runIdentity $
-- --                   runStateT (storeTermCodes 𝔠s 𝔑) 𝔫'
-- --                 else
-- --                   children 𝔫 𝔠' }) ~|
-- --         return tt }

-- --     initialTopNode : TopTermNode
-- --     initialTopNode = record { children = const nothing }

-- --     example-store : TopTermNode
-- --     example-store = snd ∘ runIdentity $ runStateT (storeTermCodesAtTop example-TermCodes 0) initialTopNode

-- --     foo : TopTermNode × TopTermNode
-- --     foo =
-- --       {!example-store!} ,
-- --       {!snd ∘ runIdentity $ runStateT (storeTermCodesAtTop example-TermCodes 10) example-store!}

-- --   -- it's tricky to keep the parents up to date when the children change (viz adolescence)
-- --   module FirstTryWithParent where
-- --     mutual

-- --       record TermNode : Set
-- --        where
-- --         inductive
-- --         field
-- --           parent : TopTermNode ⊎ TermNode
-- --           self : TermCode
-- --           children : TermCode → Maybe TermNode -- Map TermCode TermNode
-- --           number : Nat

-- --       record TopTermNode : Set
-- --        where
-- --         inductive
-- --         field
-- --           children : TermCode → Maybe TermNode

-- --     open TermNode
-- --     open TopTermNode

-- --     storeTermCodes : List TermCode → Nat → StateT TermNode Identity ⊤
-- --     storeTermCodes [] _ = return tt
-- --     storeTermCodes (𝔠 ∷ 𝔠s) 𝔑 =
-- --       𝔫 ← get -|
-- --       case children 𝔫 𝔠 of λ
-- --       { nothing →
-- --         put
-- --           (record 𝔫
-- --             { children =
-- --               λ 𝔠' →
-- --               ifYes 𝔠' ≟ 𝔠 then
-- --                 just ∘ snd ∘ runIdentity $
-- --                 (runStateT
-- --                   (storeTermCodes 𝔠s (suc 𝔑))
-- --                     (record
-- --                       { parent = right 𝔫
-- --                       ; self = 𝔠
-- --                       ; children = const nothing
-- --                       ; number = suc 𝔑 }))
-- --               else
-- --                 children 𝔫 𝔠' } ) ~|
-- --         return tt
-- --       ; (just 𝔫') →
-- --         put (record 𝔫
-- --               { children =
-- --                 λ 𝔠' →
-- --                 ifYes 𝔠' ≟ 𝔠 then
-- --                   just ∘ snd ∘ runIdentity $
-- --                   runStateT (storeTermCodes 𝔠s 𝔑) 𝔫'
-- --                 else
-- --                   children 𝔫 𝔠' }) ~|
-- --         return tt }

-- --     storeTermCodesAtTop : List TermCode → Nat → StateT TopTermNode Identity ⊤
-- --     storeTermCodesAtTop [] _ = return tt
-- --     storeTermCodesAtTop (𝔠 ∷ 𝔠s) 𝔑 =
-- --       𝔫 ← get -|
-- --       case children 𝔫 𝔠 of λ
-- --       { nothing →
-- --         put
-- --           (record 𝔫
-- --             { children =
-- --               λ 𝔠' →
-- --               ifYes 𝔠' ≟ 𝔠 then
-- --                 just ∘ snd ∘ runIdentity $
-- --                 (runStateT
-- --                   (storeTermCodes 𝔠s (suc 𝔑))
-- --                     (record
-- --                       { parent = left 𝔫
-- --                       ; self = 𝔠
-- --                       ; children = const nothing
-- --                       ; number = suc 𝔑 }))
-- --               else
-- --                 children 𝔫 𝔠' } ) ~|
-- --         return tt
-- --       ; (just 𝔫') →
-- --         put (record 𝔫
-- --               { children =
-- --                 λ 𝔠' →
-- --                 ifYes 𝔠' ≟ 𝔠 then
-- --                   just ∘ snd ∘ runIdentity $
-- --                   runStateT (storeTermCodes 𝔠s 𝔑) 𝔫'
-- --                 else
-- --                   children 𝔫 𝔠' }) ~|
-- --         return tt }

-- --     initialTopNode : TopTermNode
-- --     initialTopNode = record { children = const nothing }

-- --     example-store : TopTermNode
-- --     example-store = snd ∘ runIdentity $ runStateT (storeTermCodesAtTop example-TermCodes 0) initialTopNode

-- --     foo : TopTermNode
-- --     foo = {!example-store!}
-- --
-- --
-- -- _⟪_⟫_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
-- --         A → (A → B → C) → B → C
-- -- x ⟪ f ⟫ y = f x y
-- --
-- -- {-
-- -- infixr 9 _∘₂′_
-- -- _∘₂′_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
-- --          (C → D) → (A → B → C) → (A → B → D)
-- -- _∘₂′_ = _∘′_ ∘ _∘′_
-- -- {-# INLINE _∘₂′_ #-}
-- --
-- -- infixr 9 _∘₂′_
-- -- _∘₂′_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
-- --          (C → D) → (A → B → C) → (A → B → D)
-- -- _∘₂′_ = _∘′_ ∘ _∘′_
-- -- {-# INLINE _∘₂′_ #-}
-- -- -}
-- -- {-
-- -- infixr 9 _∘₂_
-- -- _∘₂_ : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : ∀ x → B x → Set c} {D : ∀ x → B x → C x
-- --          (f : ∀ {x} (y : B x) → C x y) (g : ∀ x → B x) →
-- --          ∀ x → C x (g x)
-- -- _∘₂_ = _∘′_ ∘ _∘′_
-- -- {-# INLINE _∘₂′_ #-}
-- -- -}


text:
open import Level using (Level; _⊔_)
open import Function using (id; case_of_)
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin; suc; zero)
open import Data.Vec as Vec using (Vec) renaming (_∷_ to _,_; [] to ∅)
open import Data.List using (_∷_; [])
open import Data.List as List using (List; _++_) renaming (_∷_ to _,_; [] to ∅)
open import Data.Product as Product using (∃; _×_; _,_)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; sym; cong)

module IntuitionisticLogic (U : Set) (⟦_⟧ᵁ : U → Set) where

infix  30 _⊗_
infixr 20 _⇒_

data Type : Set where
  el    : (A : U) → Type
  _⊗_   : Type → Type → Type
  _⇒_  : Type → Type → Type

module Implicit where

  infix  4  _⊢_

  data _⊢_ : ∀ {k} (Γ : Vec Type k) (A : Type) → Set where
    var   : ∀ {k} {Γ : Vec Type k} (x : Fin k) → Γ ⊢ Vec.lookup x Γ
    abs   : ∀ {A B} {k} {Γ : Vec Type k} → A , Γ ⊢ B → Γ ⊢ A ⇒ B
    app   : ∀ {A B} {k} {Γ : Vec Type k} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
    pair  : ∀ {A B} {k} {Γ : Vec Type k} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ⊗ B
    case  : ∀ {A B C} {k} {Γ : Vec Type k} → Γ ⊢ A ⊗ B → A , B , Γ ⊢ C → Γ ⊢ C

  swap : ∀ {A B} {k} {Γ : Vec Type k} → Γ ⊢ A ⊗ B ⇒ B ⊗ A
  swap = abs (case (var zero) (pair (var (suc zero)) (var zero)))

  Vec-exch : ∀ {k} (i : Fin k) → Vec Type (suc k) → Vec Type (suc k)
  Vec-exch  zero    (A , B , Γ)  = B , A , Γ
  Vec-exch (suc i)  (A , Γ)      = A , (Vec-exch i Γ)

  lemma-var : ∀ {k} {Γ : Vec Type (suc k)} → ∀ i x → ∃ λ y → Vec.lookup x Γ ≡ Vec.lookup y (Vec-exch i Γ)
  lemma-var {Γ = A , B , Γ} zero     zero           = suc zero , refl
  lemma-var {Γ = A , B , Γ} zero     (suc zero)     = zero , refl
  lemma-var {Γ = A , B , Γ} zero     (suc (suc x))  = suc (suc x) , refl
  lemma-var {Γ = A , Γ} (suc i)  zero           = zero , refl
  lemma-var {Γ = A , Γ} (suc i)  (suc x)        = Product.map suc id (lemma-var {Γ = Γ} i x)

  exch : ∀ {k} {Γ : Vec Type (suc k)} {A} → ∀ i → Γ ⊢ A → Vec-exch i Γ ⊢ A
  exch {Γ = Γ} i (var x) with lemma-var {Γ = Γ} i x
  exch {Γ = Γ} i (var x) | y , p rewrite p  = var y
  exch i (abs t)     = abs (exch (suc i) t)
  exch i (app s t)   = app (exch i s) (exch i t)
  exch i (pair s t)  = pair (exch i s) (exch i t)
  exch i (case s t)  = case (exch i s) (exch (suc (suc i)) t)

module Explicit where

  infix  4  _⊢_

  data _⊢_ : ∀ (X : List Type) (A : Type) → Set where
    var   : ∀ {A} → A , ∅ ⊢ A
    abs   : ∀ {X A B} → A , X ⊢ B → X ⊢ A ⇒ B
    app   : ∀ {X Y A B} → X ⊢ A ⇒ B → Y ⊢ A → X ++ Y ⊢ B
    pair  : ∀ {X Y A B} → X ⊢ A → Y ⊢ B → X ++ Y ⊢ A ⊗ B
    case  : ∀ {X Y A B C} → X ⊢ A ⊗ B → A , B , Y ⊢ C → X ++ Y ⊢ C
    weak  : ∀ {X Y A} → X ⊢ A → X ++ Y ⊢ A
    cont  : ∀ {X A B} → A , A , X ⊢ B → A , X ⊢ B
    exch  : ∀ {X Y Z W A} →  (X ++ Z) ++ (Y ++ W) ⊢ A
          →  (X ++ Y) ++ (Z ++ W) ⊢ A

  exch₀ : ∀ {X A B C} → B , A , X ⊢ C → A , B , X ⊢ C
  exch₀ {X} {A} {B} = exch {∅} {A , ∅} {B , ∅} {X}

  swap : ∀ {X A B} → X ⊢ A ⊗ B ⇒ B ⊗ A
  swap {X} {A} {B} = abs (case var (exch₀ (pair var (weak {A , ∅} {X} var))))

  record Reify {a b : Level} (A : Set a) (B : Set b) : Set (a ⊔ b) where
    field
      ⟦_⟧ : A → B

  instance
    ReifyType : Reify Type Set
    ReifyType = record { ⟦_⟧ = ⟦_⟧ }
      where

      ⟦_⟧ : Type → Set
      ⟦ el A    ⟧ = ⟦ A ⟧ᵁ
      ⟦ A ⊗ B   ⟧ = ⟦ A ⟧ × ⟦ B ⟧
      ⟦ A ⇒ B  ⟧ = ⟦ A ⟧ → ⟦ B ⟧

  data Ctxt : ∀ (X : List Set) → Set₁ where
    ∅ : Ctxt ∅
    _,_ : ∀ {A X} → A → Ctxt X → Ctxt (A , X)

  open Reify {{...}} using (⟦_⟧)

  instance
    ReifyCtxt : Reify (List Type) (List Set)
    ReifyCtxt = record { ⟦_⟧ = List.map ⟦_⟧ }

  Ctxt-insert : {A : Type} {X Y : List Type} → ⟦ A ⟧ → Ctxt ⟦ X ++ Y ⟧ → Ctxt ⟦ X ++ (A , Y) ⟧
  Ctxt-insert {A} {∅} {Y} A′ E = A′ , E
  Ctxt-insert {A} {B , X} {Y} A′ (B′ , E) = B′ , Ctxt-insert {A} {X} {Y} A′ E

  Ctxt-exch : {X Y Z W : List Type} → Ctxt ⟦ (X ++ Y) ++ (Z ++ W) ⟧ → Ctxt ⟦ (X ++ Z) ++ (Y ++ W) ⟧
  Ctxt-exch {X = ∅} {Y = ∅} {Z} {W} E = E
  Ctxt-exch {X = ∅} {Y = A , Y} {Z} {W} (A′ , E) = Ctxt-insert {A} {Z} {Y ++ W} A′ (Ctxt-exch {∅} {Y} {Z} {W} E)
  Ctxt-exch {X = A , X} {Y} {Z} {W} (A′ , E) = A′ , Ctxt-exch {X} {Y} {Z} {W} E

  Ctxt-split : {X Y : List Type} → Ctxt ⟦ X ++ Y ⟧ → Ctxt ⟦ X ⟧ × Ctxt ⟦ Y ⟧
  Ctxt-split {∅} {Y} E = ∅ , E
  Ctxt-split {A , X} {Y} (A′ , E) with Ctxt-split {X} {Y} E
  ... | Eˣ , Eʸ = ((A′ , Eˣ) , Eʸ)

  reify : {A : Type} {X : List Type} → X ⊢ A → (Ctxt ⟦ X ⟧ → ⟦ A ⟧)
  reify var         (x , ∅)   = x
  reify (abs t)     E         = λ x → reify t (x , E)
  reify (app s t)   E         with Ctxt-split E
  ... | Eˢ , Eᵗ               = (reify s Eˢ) (reify t Eᵗ)
  reify (pair s t)  E         with Ctxt-split E
  ... | Eˢ , Eᵗ               = (reify s Eˢ , reify t Eᵗ)
  reify (case s t)  E         with Ctxt-split E
  ... | Eˢ , Eᵗ               = case reify s Eˢ of λ{ (x , y) → reify t (x , y , Eᵗ)}
  reify (weak {X} s)    E         with Ctxt-split {X} E
  ... | Eˢ , Eᵗ               = reify s Eˢ
  reify (cont t)    (x , E)   = reify t (x , x , E)
  reify (exch {X} {Y} {Z} {W} t)    E         = reify t (Ctxt-exch {X} {Y} {Z} {W} E)

  [_] : {A : Type} {X : List Type} → X ⊢ A → (Ctxt ⟦ X ⟧ → ⟦ A ⟧)
  [_] = reify

  swap′ : ∀ {A B} → ⟦ A ⟧ × ⟦ B ⟧ → ⟦ B ⟧ × ⟦ A ⟧
  swap′ {A} {B} = [ swap {∅} {A} {B} ] ∅

ext: agda


text:
{-# OPTIONS --copatterns #-}
{-# OPTIONS -v tc.constr.findInScope:15 #-}

-- One-place functors (decorations) on Set

module Control.Bug-Loop where

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

open import Control.Functor

open IsFunctor {{...}}

record IsDecoration (D : Set → Set) : Set₁ where
  field
    traverse    : ∀ {F} {{ functor : IsFunctor F }} {A B} →

        (A → F B) → D A → F (D B)

    traverse-id : ∀ {A} →

        traverse {F = λ A → A} {A = A} id ≡ id

    traverse-∘  :
      ∀ {F G} {{ funcF : IsFunctor F}} {{ funcG : IsFunctor G}} →
      ∀ {A B C} {f : A → F B} {g : B → G C} →

        traverse ((map g) ∘ f) ≡ map {{funcF}} (traverse g) ∘ traverse f

  isFunctor : IsFunctor D
  isFunctor = record
    { ops   = record { map    = traverse }
    ; laws  = record { map-id = traverse-id
                     ; map-∘  = traverse-∘
                     }
    }

open IsDecoration

idIsDecoration : IsDecoration (λ A → A)
traverse    idIsDecoration f = f
traverse-id idIsDecoration = refl
traverse-∘  idIsDecoration = refl

compIsDecoration : ∀ {D E} → IsDecoration D → IsDecoration E → IsDecoration (λ A → D (E A))
traverse    (compIsDecoration d e) f = traverse d (traverse e f)
traverse-id (compIsDecoration d e) = begin
    traverse d (traverse e id)
  ≡⟨ cong (traverse d) (traverse-id e) ⟩
    traverse d id
  ≡⟨ traverse-id d ⟩
    id
  ∎
traverse-∘ (compIsDecoration d e) {{funcF = funcF}} {{funcG = funcG}} {f = f} {g = g} = begin
    traverse (compIsDecoration d e) (map g ∘ f)
  ≡⟨⟩
    traverse d (traverse e (map g ∘ f))
  ≡⟨ cong (traverse d) (traverse-∘ e) ⟩
    traverse d (map (traverse e g) ∘ traverse e f)
  ≡⟨ traverse-∘ d ⟩
    map (traverse d (traverse e g)) ∘ traverse d (traverse e f)
  ≡⟨⟩
    map (traverse (compIsDecoration d e) g) ∘ traverse (compIsDecoration d e) f
  ∎

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


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

open import lib.Basics

module lib.types.Empty where

Empty-rec : ∀ {i} {A : Type i} → (Empty → A)
Empty-rec = Empty-elim

⊥-rec : ∀ {i} {A : Type i} → (⊥ → A)
⊥-rec = Empty-rec

Empty-is-prop : is-prop Empty
Empty-is-prop = has-level-in Empty-elim

instance
  Empty-level : {n : ℕ₋₂} → has-level (S n) Empty
  Empty-level = prop-has-level-S Empty-is-prop

Empty-is-set : is-set Empty
Empty-is-set = raise-level -1 Empty-is-prop

⊥-is-prop = Empty-is-prop
⊥-is-set = Empty-is-set
⊥-level = Empty-level

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

postulate
  A : Set
  a : A

record Eq (a : A) : Set where
  constructor mkEq
  field
    v : A
    p : a ≡ v
open Eq

record S : Set1 where
  constructor mkS
  field
    u : A
    e : Eq u
  open Eq e public
open S

test : ∀ (b : A) → S
u (test b) = b
v (e (test b)) = a
p (e (test b)) = refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Jesper, 2018-11-29: Instances with explicit arguments will never be
-- used, so declaring them should give a warning.

postulate
  X : Set
  instance _ : Set → X -- this should give a warning

it : {{_ : X}} → X
it {{x}} = x

-- OTOH, this is fine as the instance can be used inside the module
module _ (A : Set) where
  postulate instance instX : X

  test : X
  test = it

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
-- {-# OPTIONS -v tc.cover.split.con:20 #-}

open import Common.Prelude renaming (Nat to ℕ)
open import Common.Equality

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

-- Decidable relations.

data Dec (P : Set) : Set where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

_≟_ : (m n : ℕ) → Dec (m ≡ n)
zero  ≟ zero   = yes refl
zero  ≟ suc n  = no λ()
suc m ≟ zero   = no λ()
suc m ≟ suc n  with m ≟ n
suc m ≟ suc .m | yes refl = yes refl
suc m ≟ suc n  | no prf   = no (λ x → prf (cong pred x))

data Ty : Set where

data Cxt : Set where
  ε   : Cxt
  _,_ : (Γ : Cxt) (a : Ty) → Cxt

len : Cxt → ℕ
len ε       = 0
len (Γ , _) = suc (len Γ)

-- De Bruijn index

mutual
  Var : Cxt → Ty → Set
  Var Γ a = Var' a Γ

  data Var' (a : Ty) : (Γ : Cxt) → Set where
    zero : ∀ {Γ}                 → Var (Γ , a) a
    suc  : ∀ {Γ b} (x : Var Γ a) → Var (Γ , b) a

-- De Bruijn Level

Lev = ℕ

-- Valid de Bruijn levels.

data LookupLev : (x : Lev) (Γ : Cxt) (a : Ty) (i : Var Γ a) → Set where
  lookupZero : ∀ {Γ a} →
    LookupLev (len Γ) (Γ , a) a zero

  lookupSuc : ∀ {Γ a b x i} →
    LookupLev x Γ a i →
    LookupLev x (Γ , b) a (suc i)

record ValidLev (x : Lev) (Γ : Cxt) : Set where
  constructor validLev
  field
    {type } : Ty
    {index} : Var Γ type
    valid   : LookupLev x Γ type index

weakLev : ∀ {x Γ a} → ValidLev x Γ → ValidLev x (Γ , a)
weakLev (validLev d) = validLev (lookupSuc d)

-- Looking up a de Bruijn level.

lookupLev : ∀ (x : Lev) (Γ : Cxt) → Dec (ValidLev x Γ)
lookupLev x ε = no λ { (validLev ()) }
lookupLev x (Γ , a) with x ≟ len Γ
lookupLev ._ (Γ , a) | yes refl = yes (validLev lookupZero)
lookupLev x (Γ , a) | no _ with lookupLev x Γ
lookupLev x (Γ , a) | no ¬p | yes d = yes (weakLev d)
lookupLev x (Γ , a) | no ¬p | no ¬d = no contra
  where
    contra : ¬ ValidLev x (Γ , a)
    contra (validLev (lookupSuc valid)) = ?

{- Unbound indices showing up in error message:

I'm not sure if there should be a case for the constructor
lookupZero, because I get stuck when trying to solve the following
unification problems (inferred index ≟ expected index):
  len Γ ≟ @8
  Γ , a ≟ @7 , @4
  a ≟ type
  zero ≟ index
when checking the definition of contra -}

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

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

open import Cubical.Data.Bool
open import Cubical.HITs.Join
open import Cubical.HITs.Susp.Base

open Iso

Susp-iso-joinBool : ∀ {ℓ} {A : Type ℓ} → Iso (Susp A) (join A Bool)
fun Susp-iso-joinBool north = inr true
fun Susp-iso-joinBool south = inr false
fun Susp-iso-joinBool (merid a i) = (sym (push a true) ∙ push a false) i
inv Susp-iso-joinBool (inr true ) = north
inv Susp-iso-joinBool (inr false) = south
inv Susp-iso-joinBool (inl _) = north
inv Susp-iso-joinBool (push a true  i) = north
inv Susp-iso-joinBool (push a false i) = merid a i
rightInv Susp-iso-joinBool (inr true ) = refl
rightInv Susp-iso-joinBool (inr false) = refl
rightInv Susp-iso-joinBool (inl a) = sym (push a true)
rightInv Susp-iso-joinBool (push a true  i) j = push a true (i ∨ ~ j)
rightInv Susp-iso-joinBool (push a false i) j
  = hcomp (λ k → λ { (i = i0) → push a true (~ j)
                   ; (i = i1) → push a false k
                   ; (j = i1) → push a false (i ∧ k) })
          (push a true (~ i ∧ ~ j))
leftInv Susp-iso-joinBool north = refl
leftInv Susp-iso-joinBool south = refl
leftInv (Susp-iso-joinBool {A = A}) (merid a i) j
  = hcomp (λ k → λ { (i = i0) → transp (λ _ → Susp A) (k ∨ j) north
                   ; (i = i1) → transp (λ _ → Susp A) (k ∨ j) (merid a k)
                   ; (j = i1) → merid a (i ∧ k) })
          (transp (λ _ → Susp A) j north)

Susp≃joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≃ join A Bool
Susp≃joinBool = isoToEquiv Susp-iso-joinBool

Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool
Susp≡joinBool = isoToPath Susp-iso-joinBool

congSuspEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≃ B → Susp A ≃ Susp B
congSuspEquiv {ℓ} {A} {B} h = isoToEquiv isom
  where isom : Iso (Susp A) (Susp B)
        Iso.fun isom north = north
        Iso.fun isom south = south
        Iso.fun isom (merid a i) = merid (fst h a) i
        Iso.inv isom north = north
        Iso.inv isom south = south
        Iso.inv isom (merid a i) = merid (invEq h a) i
        Iso.rightInv isom north = refl
        Iso.rightInv isom south = refl
        Iso.rightInv isom (merid a i) j = merid (retEq h a j) i
        Iso.leftInv isom north = refl
        Iso.leftInv isom south = refl
        Iso.leftInv isom (merid a i) j = merid (secEq h a j) i

suspToPropElim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Type ℓ'} (a : A)
                 → ((x : Susp A) → isProp (B x))
                 → B north
                 → (x : Susp A) → B x
suspToPropElim a isProp Bnorth north = Bnorth
suspToPropElim {B = B} a isProp Bnorth south = subst B (merid a) Bnorth
suspToPropElim {B = B} a isProp Bnorth (merid a₁ i) =
  isOfHLevel→isOfHLevelDep 1 isProp Bnorth (subst B (merid a) Bnorth) (merid a₁) i

suspToPropElim2 : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Susp A → Susp A → Type ℓ'} (a : A)
                 → ((x y : Susp A) → isProp (B x y))
                 → B north north
                 → (x y : Susp A) → B x y
suspToPropElim2 _ _ Bnorth north north = Bnorth
suspToPropElim2 {B = B} a _ Bnorth north south = subst (B north) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth north (merid x i) =
  isProp→PathP (λ i → isprop north (merid x i))
               Bnorth (subst (B north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a _ Bnorth south north = subst (λ x → B x north) (merid a) Bnorth
suspToPropElim2 {B = B} a _ Bnorth south south = subst (λ x → B x x) (merid a) Bnorth
suspToPropElim2 {B = B} a isprop Bnorth south (merid x i) =
  isProp→PathP (λ i → isprop south (merid x i))
               (subst (λ x → B x north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) north =
  isProp→PathP (λ i → isprop (merid x i) north)
               Bnorth (subst (λ x → B x north) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) south =
  isProp→PathP (λ i → isprop (merid x i) south)
               (subst (B north) (merid a) Bnorth)
               (subst (λ x → B x x) (merid a) Bnorth) i
suspToPropElim2 {B = B} a isprop Bnorth (merid x i) (merid y j) =
  isSet→SquareP (λ i j → isOfHLevelSuc 1 (isprop _ _))
     (isProp→PathP (λ i₁ → isprop north (merid y i₁)) Bnorth
                   (subst (B north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop south (merid y i₁))
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) north) Bnorth
                   (subst (λ x₁ → B x₁ north) (merid a) Bnorth))
     (isProp→PathP (λ i₁ → isprop (merid x i₁) south)
                   (subst (B north) (merid a) Bnorth)
                   (subst (λ x₁ → B x₁ x₁) (merid a) Bnorth)) i j
{- Clever proof:
suspToPropElim2 a isProp Bnorth =
  suspToPropElim a (λ x → isOfHLevelΠ 1 λ y → isProp x y)
                   (suspToPropElim a (λ x → isProp north x) Bnorth)
-}

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fancy display functions for List-based tables
------------------------------------------------------------------------

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

module Text.Tabular.List where

open import Data.String using (String)
open import Data.List.Base
import Data.Nat.Properties as ℕₚ
open import Data.Product using (-,_; proj₂)
open import Data.Vec.Base as Vec using (Vec)
open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤)
open import Function.Base

open import Text.Tabular.Base
import Text.Tabular.Vec as Show

display : TabularConfig → List Alignment → List (List String) → List String
display c a rows = Show.display c alignment rectangle where

  alignment : Vec Alignment _
  alignment = Vec≤.padRight Left
            $ Vec≤.≤-cast (ℕₚ.m⊓n≤m _ _)
            $ Vec≤.take _ (Vec≤.fromList a)

  rectangle : Vec (Vec String _) _
  rectangle = Vec.fromList
            $ map (Vec≤.padRight "")
            $ proj₂
            $ Vec≤.rectangle
            $ map (λ row → -, Vec≤.fromList row) rows


text:
-- Andreas, Ulf, 2015-06-03
-- Issue 473 was not fixed for records without constructor
record _×_ A B : Set where
  constructor _,_
  field
    fst : A
    snd : B

open _×_

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data Zero : Nat → Set where
  zero : Zero zero

data Zero₂ : Nat → Nat → Set where
  zero : Zero₂ zero zero

f₁ : (p : Nat × Nat) → Zero₂ (fst p) (snd p) → Set
f₁ (.zero , .zero) zero = Nat    -- works
-- f₁ .(zero , zero) zero = Nat  -- fails

f₂ : (p : Nat × Nat) → Zero (fst p) → Set
f₂ (.zero , y) zero = Nat  -- works
-- foo .?? zero             -- fails (nothing to write in place of ??)

f₃ : {p : Nat × Nat} → Zero (fst p) → Set
f₃ zero = Nat

f₄ : {p : Nat × (Nat × Nat)} → Zero (fst (snd p)) → Set
f₄ zero = Nat

f₅ : {p : Nat × Nat} → Zero₂ (fst p) (snd p) → Set
f₅ zero = Nat

data I : Set where
  i : I

record Box (A B : Set) : Set where
  -- no constructor [_]
  field contents : A

[_] : ∀{A B} → A → Box A B
[ a ] = record { contents = a }

data D : Set → Set₁ where
  d₁ : (R : Set) → D R
  d₂ : (i : I) (R : I → Set) → D (R i) → D (Box I (R i))

data S : (R : Set) → R → D R → Set₁ where
  s : (j : I) (R : I → Set) (p : D (R j)) →
      S (Box I (R j)) [ j ] (d₂ j R p)

postulate
  P : I → Set

Fails : {e : Box I (P i)} → S (Box I (P i)) e (d₂ i P (d₁ (P i))) → Set₁
Fails (s .i .P .(d₁ (P i))) = Set

-- Refuse to solve heterogeneous constraint p : D (P (Box.contents e))
-- =?= d₁ (P i) : D (P i)
-- when checking that the pattern s .i .P .(d₁ (P i)) has type
-- S (Box I (P i)) e (d₂ i P (d₁ (P i)))


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Monoid.Morphism

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Pointed

open import Cubical.Algebra.Semigroup.Properties using (isPropIsSemigroup)

open import Cubical.Relation.Binary.Reasoning.Equality

open Iso

private
  variable
    ℓ ℓ′ ℓ′′ : Level
    L : Monoid ℓ
    M : Monoid ℓ′
    N : Monoid ℓ′′

isPropIsMonoidHom : ∀ (M : Monoid ℓ) (N : Monoid ℓ′) f → isProp (IsMonoidHom M N f)
isPropIsMonoidHom M N f (ismonoidhom aOp aId) (ismonoidhom bOp bId) =
  cong₂ ismonoidhom
    (isPropHomomorphic₂ (Monoid.is-set N) f (Monoid._•_ M) (Monoid._•_ N) aOp bOp)
    (isPropHomomorphic₀ (Monoid.is-set N) f (Monoid.ε   M) (Monoid.ε   N) aId bId)

isSetMonoidHom : isSet (M ⟶ᴴ N)
isSetMonoidHom {M = M} {N = N} = isOfHLevelRespectEquiv 2 equiv
                                  (isSetΣ (isSetΠ λ _ → is-set N)
                                          (λ f → isProp→isSet (isPropIsMonoidHom M N f)))
  where
    open Monoid
    equiv : (Σ[ g ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsMonoidHom M N g) ≃ MonoidHom M N
    equiv = isoToEquiv (iso (λ (g , m) → monoidhom g m) (λ (monoidhom g m) → g , m) (λ _ → refl) λ _ → refl)

isMonoidHomComp : {f : ⟨ L ⟩ → ⟨ M ⟩} {g : ⟨ M ⟩ → ⟨ N ⟩}
                  → IsMonoidHom L M f → IsMonoidHom M N g → IsMonoidHom L N (g ∘ f)
isMonoidHomComp {g = g} (ismonoidhom fOp fId) (ismonoidhom gOp gId) =
  ismonoidhom (λ _ _ → cong g (fOp _ _) ∙ gOp _ _) (cong g fId ∙ gId)

private
  isMonoidHomComp′ : (f : L ⟶ᴴ M) (g : M ⟶ᴴ N)
                      → IsMonoidHom L N (MonoidHom.fun g ∘ MonoidHom.fun f)
  isMonoidHomComp′ (monoidhom f (ismonoidhom fOp fId)) (monoidhom g (ismonoidhom gOp gId)) =
    ismonoidhom (λ _ _ → cong g (fOp _ _) ∙ gOp _ _) (cong g fId ∙ gId)

compMonoidHom : (L ⟶ᴴ M) → (M ⟶ᴴ N) → (L ⟶ᴴ N)
compMonoidHom f g = monoidhom _ (isMonoidHomComp′ f g)

compMonoidEquiv : L ≃ᴴ M → M ≃ᴴ N → L ≃ᴴ N
compMonoidEquiv f g = monoidequiv (compEquiv f.eq g.eq) (isMonoidHomComp′ f.hom g.hom)
  where
    module f = MonoidEquiv f
    module g = MonoidEquiv g

isMonoidHomId : (M : Monoid ℓ) → IsMonoidHom M M id
isMonoidHomId M = record
  { preservesOp = λ _ _ → refl
  ; preservesId = refl
  }

idMonoidHom : (M : Monoid ℓ) → (M ⟶ᴴ M)
idMonoidHom M = record
  { fun   = id
  ; isHom = isMonoidHomId M
  }

idMonoidEquiv : (M : Monoid ℓ) → M ≃ᴴ M
idMonoidEquiv M = record
  { eq    = idEquiv ⟨ M ⟩
  ; isHom = isMonoidHomId M
  }

-- Isomorphism inversion
isMonoidHomInv : (eqv : M ≃ᴴ N) → IsMonoidHom N M (invEq (MonoidEquiv.eq eqv))
isMonoidHomInv {M = M} {N = N} (monoidequiv eq (ismonoidhom hOp hId)) = ismonoidhom
  (λ x y → isInj-f (
    f (f⁻¹ (x N.• y))       ≡⟨ retEq eq _ ⟩
    x N.• y                 ≡˘⟨ cong₂ N._•_ (retEq eq x) (retEq eq y) ⟩
    f (f⁻¹ x) N.• f (f⁻¹ y) ≡˘⟨ hOp (f⁻¹ x) (f⁻¹ y) ⟩
    f (f⁻¹ x M.• f⁻¹ y)     ∎))
  (isInj-f (
    f (f⁻¹ N.ε) ≡⟨ retEq eq _ ⟩
    N.ε         ≡˘⟨ hId ⟩
    f M.ε       ∎))
    where
      module M = Monoid M
      module N = Monoid N
      f = equivFun eq
      f⁻¹ = invEq eq
      isInj-f : {x y : ⟨ M ⟩} → f x ≡ f y → x ≡ y
      isInj-f {x} {y} = invEq (_ , isEquiv→isEmbedding (eq .snd) x y)

invMonoidHom : M ≃ᴴ N → (N ⟶ᴴ M)
invMonoidHom eq = record { isHom = isMonoidHomInv eq }

invMonoidEquiv : M ≃ᴴ N → N ≃ᴴ M
invMonoidEquiv eq = record
  { eq    = invEquiv (MonoidEquiv.eq eq)
  ; isHom = isMonoidHomInv eq
  }

monoidHomEq : {f g : M ⟶ᴴ N} → MonoidHom.fun f ≡ MonoidHom.fun g → f ≡ g
monoidHomEq {M = M} {N = N} {monoidhom f fm} {monoidhom g gm} p i =
  monoidhom (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsMonoidHom M N (p i)) fm gm
    p-hom = toPathP (isPropIsMonoidHom M N _ _ _)

monoidEquivEq : {f g : M ≃ᴴ N} → MonoidEquiv.eq f ≡ MonoidEquiv.eq g → f ≡ g
monoidEquivEq {M = M} {N = N} {monoidequiv f fm} {monoidequiv g gm} p i =
  monoidequiv (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsMonoidHom M N (p i .fst)) fm gm
    p-hom = toPathP (isPropIsMonoidHom M N _ _ _)

module MonoidΣTheory {ℓ} where

  RawMonoidStructure : Type ℓ → Type ℓ
  RawMonoidStructure X = (X → X → X) × X

  RawMonoidEquivStr = AutoEquivStr RawMonoidStructure

  rawMonoidUnivalentStr : UnivalentStr _ RawMonoidEquivStr
  rawMonoidUnivalentStr = autoUnivalentStr RawMonoidStructure

  MonoidAxioms : (M : Type ℓ) → RawMonoidStructure M → Type ℓ
  MonoidAxioms M (_•_ , ε) = IsSemigroup M _•_ × Identity ε _•_

  MonoidStructure : Type ℓ → Type ℓ
  MonoidStructure = AxiomsStructure RawMonoidStructure MonoidAxioms

  MonoidΣ : Type (ℓ-suc ℓ)
  MonoidΣ = TypeWithStr ℓ MonoidStructure

  isPropMonoidAxioms : (M : Type ℓ) (s : RawMonoidStructure M) → isProp (MonoidAxioms M s)
  isPropMonoidAxioms M (_•_ , ε) = isPropΣ isPropIsSemigroup
                                    λ isSemiM → isPropIdentity (IsSemigroup.is-set isSemiM) _•_ ε

  MonoidEquivStr : StrEquiv MonoidStructure ℓ
  MonoidEquivStr = AxiomsEquivStr RawMonoidEquivStr MonoidAxioms

  MonoidAxiomsIsoIsMonoid : {M : Type ℓ} (s : RawMonoidStructure M) →
                            Iso (MonoidAxioms M s) (IsMonoid M (s .fst) (s .snd))
  fun (MonoidAxiomsIsoIsMonoid s) (x , y)        = ismonoid x y
  inv (MonoidAxiomsIsoIsMonoid s) (ismonoid x y) = (x , y)
  rightInv (MonoidAxiomsIsoIsMonoid s) _         = refl
  leftInv (MonoidAxiomsIsoIsMonoid s) _          = refl

  MonoidAxioms≡IsMonoid : {M : Type ℓ} (s : RawMonoidStructure M) →
                          MonoidAxioms M s ≡ IsMonoid M (s .fst) (s .snd)
  MonoidAxioms≡IsMonoid s = isoToPath (MonoidAxiomsIsoIsMonoid s)

  Monoid→MonoidΣ : Monoid ℓ → MonoidΣ
  Monoid→MonoidΣ (mkmonoid M _•_ ε isMonoidM) =
    M , (_•_ , ε) , MonoidAxiomsIsoIsMonoid (_•_ , ε) .inv isMonoidM

  MonoidΣ→Monoid : MonoidΣ → Monoid ℓ
  MonoidΣ→Monoid (M , (_•_ , ε) , isMonoidM) =
    mkmonoid M _•_ ε (MonoidAxiomsIsoIsMonoid (_•_ , ε) .fun isMonoidM)

  MonoidIsoMonoidΣ : Iso (Monoid ℓ) MonoidΣ
  MonoidIsoMonoidΣ =
    iso Monoid→MonoidΣ MonoidΣ→Monoid (λ _ → refl) (λ _ → refl)

  monoidUnivalentStr : UnivalentStr MonoidStructure MonoidEquivStr
  monoidUnivalentStr = axiomsUnivalentStr _ isPropMonoidAxioms rawMonoidUnivalentStr

  MonoidΣPath : (M N : MonoidΣ) → (M ≃[ MonoidEquivStr ] N) ≃ (M ≡ N)
  MonoidΣPath = SIP monoidUnivalentStr

  MonoidEquivΣ : (M N : Monoid ℓ) → Type ℓ
  MonoidEquivΣ M N = Monoid→MonoidΣ M ≃[ MonoidEquivStr ] Monoid→MonoidΣ N

  MonoidIsoΣPath : {M N : Monoid ℓ} → Iso (MonoidEquiv M N) (MonoidEquivΣ M N)
  fun MonoidIsoΣPath (monoidequiv eq (ismonoidhom hOp hId)) = (eq , hOp , hId)
  inv MonoidIsoΣPath (eq , hOp , hId)                       = monoidequiv eq (ismonoidhom hOp hId)
  rightInv MonoidIsoΣPath _                                 = refl
  leftInv MonoidIsoΣPath _                                  = refl

  MonoidPath : (M N : Monoid ℓ) → (MonoidEquiv M N) ≃ (M ≡ N)
  MonoidPath M N =
    MonoidEquiv M N                       ≃⟨ isoToEquiv MonoidIsoΣPath ⟩
    MonoidEquivΣ M N                      ≃⟨ MonoidΣPath _ _ ⟩
    Monoid→MonoidΣ M ≡ Monoid→MonoidΣ N   ≃⟨ isoToEquiv (invIso (congIso MonoidIsoMonoidΣ)) ⟩
    M ≡ N                                 ■

  RawMonoidΣ : Type (ℓ-suc ℓ)
  RawMonoidΣ = TypeWithStr ℓ RawMonoidStructure

  Monoid→RawMonoidΣ : Monoid ℓ → RawMonoidΣ
  Monoid→RawMonoidΣ (mkmonoid A _•_ ε _) = A , _•_ , ε

  InducedMonoid : (M : Monoid ℓ) (N : RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst) →
                  RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e → Monoid ℓ
  InducedMonoid M N e r =
    MonoidΣ→Monoid (inducedStructure rawMonoidUnivalentStr (Monoid→MonoidΣ M) N (e , r))

  InducedMonoidPath : (M : Monoid ℓ) (N : RawMonoidΣ) (e : M .Monoid.Carrier ≃ N .fst)
                      (E : RawMonoidEquivStr (Monoid→RawMonoidΣ M) N e) →
                      M ≡ InducedMonoid M N e E
  InducedMonoidPath M N e E =
    MonoidPath M (InducedMonoid M N e E) .fst (monoidequiv e (ismonoidhom (E .fst) (E .snd)))

-- We now extract the important results from the above module

open MonoidΣTheory public using (InducedMonoid; InducedMonoidPath)

isPropIsMonoid : {M : Type ℓ} {_•_ : Op₂ M} {ε : M} → isProp (IsMonoid M _•_ ε)
isPropIsMonoid {_•_ = _•_} {ε} =
  subst isProp (MonoidΣTheory.MonoidAxioms≡IsMonoid (_•_ , ε))
        (MonoidΣTheory.isPropMonoidAxioms _ (_•_ , ε))

MonoidPath : (M ≃ᴴ N) ≃ (M ≡ N)
MonoidPath {M = M} {N} = MonoidΣTheory.MonoidPath M N

open Monoid

uaMonoid : M ≃ᴴ N → M ≡ N
uaMonoid = equivFun MonoidPath

carac-uaMonoid : {M N : Monoid ℓ} (f : M ≃ᴴ N) → cong Carrier (uaMonoid f) ≡ ua (MonoidEquiv.eq f)
carac-uaMonoid (monoidequiv f m) =
  (refl ∙∙ ua f ∙∙ refl)  ≡˘⟨ rUnit (ua f) ⟩
  ua f                    ∎

Monoid≡ : (M N : Monoid ℓ) → (
  Σ[ p ∈ ⟨ M ⟩ ≡ ⟨ N ⟩ ]
  Σ[ q ∈ PathP (λ i → p i → p i → p i) (_•_ M) (_•_ N) ]
  Σ[ r ∈ PathP (λ i → p i) (ε M) (ε N) ]
  PathP (λ i → IsMonoid (p i) (q i) (r i)) (isMonoid M) (isMonoid N))
  ≃ (M ≡ N)
Monoid≡ M N = isoToEquiv (iso
  (λ (p , q , r , s) i → mkmonoid (p i) (q i) (r i) (s i))
  (λ p → cong Carrier p , cong _•_ p , cong ε p , cong isMonoid p)
  (λ _ → refl) (λ _ → refl))

caracMonoid≡ : {M N : Monoid ℓ} (p q : M ≡ N) → cong Carrier p ≡ cong Carrier q → p ≡ q
caracMonoid≡ {M = M} {N} p q t = cong (fst (Monoid≡ M N)) (Σ≡Prop (λ _ →
    isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set N) _ _) λ _ → isPropΣ
    (isOfHLevelPathP' 1 (is-set N) _ _) λ _ →
    isOfHLevelPathP 1 isPropIsMonoid _ _)
  t)

uaMonoidId : (M : Monoid ℓ) → uaMonoid (idMonoidEquiv M) ≡ refl
uaMonoidId M = caracMonoid≡ _ _ (carac-uaMonoid (idMonoidEquiv M) ∙ uaIdEquiv)

uaCompMonoidEquiv : {L M N : Monoid ℓ} (f : L ≃ᴴ M) (g : M ≃ᴴ N)
                    → uaMonoid (compMonoidEquiv f g) ≡ uaMonoid f ∙ uaMonoid g
uaCompMonoidEquiv f g = caracMonoid≡ _ _ (
  cong Carrier (uaMonoid (compMonoidEquiv f g))
    ≡⟨ carac-uaMonoid (compMonoidEquiv f g) ⟩
  ua (eq (compMonoidEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡˘⟨ cong (_∙ ua (eq g)) (carac-uaMonoid f) ⟩
  cong Carrier (uaMonoid f) ∙ ua (eq g)
    ≡˘⟨ cong (cong Carrier (uaMonoid f) ∙_) (carac-uaMonoid g) ⟩
  cong Carrier (uaMonoid f) ∙ cong Carrier (uaMonoid g)
    ≡˘⟨ cong-∙ Carrier (uaMonoid f) (uaMonoid g) ⟩
  cong Carrier (uaMonoid f ∙ uaMonoid g) ∎)
  where open MonoidEquiv


text:
module json where

open import lib
open import general-util

data json : Set where
  json-null : json
  json-raw : rope → json
  json-string : string → json
  json-nat : nat → json
  json-array : 𝕃 json → json
  json-object : trie json → json

json-escape-string : string → string
json-escape-string str = 𝕃char-to-string $ rec $ string-to-𝕃char str where
  rec : 𝕃 char → 𝕃 char
  rec [] = []
  rec ('\b' :: chars) = '\\' :: 'b' :: rec chars
  rec ('\f' :: chars) = '\\' :: 'f' :: rec chars
  rec ('\n' :: chars) = '\\' :: 'n' :: rec chars
  rec ('\r' :: chars) = '\\' :: 'r' :: rec chars
  rec ('\t' :: chars) = '\\' :: 't' :: rec chars
  rec ('"'  :: chars) = '\\' :: '"' :: rec chars
  rec ('\\' :: chars) = '\\' :: '\\' :: rec chars
  rec (char :: chars) = char :: rec chars

{-# TERMINATING #-}
json-to-rope : json → rope
json-to-rope json-null = [[ "null" ]]
json-to-rope (json-raw rope) = rope
json-to-rope (json-string string) = [[ "\"" ]] ⊹⊹ [[ json-escape-string string ]] ⊹⊹ [[ "\"" ]]
json-to-rope (json-nat nat) = [[ ℕ-to-string nat ]]
json-to-rope (json-array array) = [[ "[" ]] ⊹⊹ 𝕃-to-rope json-to-rope "," array ⊹⊹ [[ "]" ]]
json-to-rope (json-object t) = [[ "{" ]] ⊹⊹ 𝕃-to-rope key-to-rope "," (trie-strings t) ⊹⊹ [[ "}" ]] where
  key-to-rope : string → rope
  key-to-rope key with trie-lookup t key
  ...| just value = [[ "\"" ]] ⊹⊹ [[ json-escape-string key ]] ⊹⊹ [[ "\":" ]] ⊹⊹ json-to-rope value
  ...| nothing = [[ "\"" ]] ⊹⊹ [[ json-escape-string key ]] ⊹⊹ [[ "\":null" ]] -- shouldn't happen

json-new : 𝕃 (string × json) → json
json-new pairs = json-object $ foldr insert empty-trie pairs where
  insert : string × json → trie json → trie json
  insert (key , value) trie = trie-insert trie key value

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
-- Andreas, 2017-07-05, issue #2626 raised by cartazio
-- shrunk by gallais

-- There was an assignTerm inspite of
-- dontAssignMetas (issued by checking inequations involving ⊔ˢ)

-- {-# OPTIONS -v tc:45 #-}

{-# OPTIONS --allow-unsolved-metas #-}

module Issue2626 where

open import Agda.Builtin.Equality
open import Agda.Builtin.Size

data D : (sz : Size) → Set where
  c : (q s : Size) → D (q ⊔ˢ s)

postulate
  foo : c _ _ ≡ c _ _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
module Example where

import Level
open import Signature
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Fin
open import Data.Product as Prod renaming (Σ to ⨿)
open import Data.Sum as Sum
open import Relation.Nullary
open import Relation.Unary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

postulate
  ext : Extensionality Level.zero Level.zero

------
-- Examples
-----

module NatProg where
  Σ : Sig
  ∥ Σ ∥ = Fin 3
  ar Σ zero                         = Fin 0 -- 0
  ar Σ (suc zero)                   = Fin 1 -- succ
  ar Σ (suc (suc _))                = Fin 1 -- nat

  open import Terms Σ
  V = ℕ
  Z S N : ∥ Σ ∥
  Z     = # 0
  S     = # 1
  N     = # 2

  z : T V
  z = μ (ι (Z , (λ ())))

  s nat : T V → T V
  s   t = μ (ι (S , (λ _ → t)))
  nat t = μ (ι (N , (λ _ → t)))

  z∞ : T∞ V
  z∞ = χ z

  s∞ nat∞ : ∀{X} → T∞ X → T∞ X
  s∞   t = μ∞ (ι∞ (S , (λ _ → t)))
  nat∞ t = μ∞ (ι∞ (N , (λ _ → t)))

  inf : T∞ ⊥
  inf = corec (λ x → inj₁ (S , (λ _ → tt))) tt

  inf-nat : T∞ ⊥
  inf-nat = nat∞ inf

  open import Program Σ V

  -- | Program consisting of
  -- ⇒ nat(0)
  -- nat(n) ⇒ nat(s n)
  P : Program
  P = ((0 , (λ ())) , ( , clauses))
    where
      clauses : Fin 2 → Clause
      clauses zero             = (0 , (λ ())) ⊢ nat z
      clauses (suc _)          = (1 , b)      ⊢ nat (s n)
        where
          n = η 0

          b : Fin 1 → T V
          b _ = nat n

  open import Herbrand Σ V P

  lem : ¬ (∃ λ σ → (inf ~ app∞ σ (χ (geth-ν P (# 0)))))
  lem (σ , p) with out~ p
  lem (σ , p) | () , _

  bad-ν : inf-nat ∈ Herbrand-ν
  bw-closed bad-ν = inj₁ p
    where
      p : (i : dom-ν P) {σ : V → T∞ ⊥} →
          inf-nat ~ (app∞ σ (χ (geth-ν P i))) →
          (j : dom (getb-ν P i)) →
          app∞ σ (χ (get (getb-ν P i) j)) ∈ Herbrand-ν

{-
      p i {σ} p j with out inf-nat | out (σ 0) | out~ p
      p i p j | inj₁ (zero , α) | v | r = {!!}
      p i p j | inj₁ (suc zero , α) | v | r = {!!}
      p i p j | inj₁ (suc (suc _) , α) | v | r = {!!}
      p i p j | inj₂ () | v | r
-}
      p i {σ} p j with out (σ 0) | out~ p
      p zero p () | u | refl , r
      p (suc i) p zero | inj₁ (zero , _) | refl , r = {!!}
      p (suc i) p zero | inj₁ (suc zero , _) | refl , r = {!!}
      p (suc i) p zero | inj₁ (suc (suc _) , proj₂) | refl , r = {!!}
      p (suc i) p zero | inj₂ () | refl , r
      p (suc _) p (suc ()) | u | refl , r

    {-
      f : ?
      f i {σ} p j with out~ p
      ... | u = ?
-}
  bad : inf-nat ∈ Herbrand-μ
  bad = coind-μ bad-ν

{-

module BitList where
  Σ : Sig
  ∥ Σ ∥ = Fin 6
  ar Σ zero                            = Fin 0 -- 0
  ar Σ (suc zero)                      = Fin 0 -- 1
  ar Σ (suc (suc zero))                = Fin 1 -- bit(x)
  ar Σ (suc (suc (suc zero)))          = Fin 1 -- blist(x)
  ar Σ (suc (suc (suc (suc zero))))    = Fin 0 -- nil
  ar Σ (suc (suc (suc (suc (suc f))))) = Fin 2 -- cons(x,y)

  open import Terms Σ
  V = ℕ

  Z O Bit BList Nil Cons : ∥ Σ ∥
  Z     = # 0
  O     = # 1
  Bit   = # 2
  BList = # 3
  Nil   = # 4
  Cons  = # 5

  z o nil : T V
  z   = μ (ι (Z , (λ ())))
  o   = μ (ι (O , (λ ())))
  nil = μ (ι (Nil , (λ ())))

  bit blist : T V → T V
  bit   t = μ (ι (Bit , (λ _ → t)))
  blist t = μ (ι (BList , (λ _ → t)))

  bin-branch : {X : Set} → X → X → Fin 2 → X
  bin-branch x y zero    = x
  bin-branch x y (suc _) = y

  cons-br-distr : ∀{X Y} (t s : X) (f : X → Y) →
                  f ∘ bin-branch t s ≡ bin-branch (f t) (f s)
  cons-br-distr t s f = ext p
    where
      p : (i : Fin 2) → f (bin-branch t s i) ≡ bin-branch (f t) (f s) i
      p zero    = refl
      p (suc _) = refl

  cons : T V → T V → T V
  cons t s = μ (ι (Cons , bin-branch t s))

  bit0 bit1 : T V
  bit0 = bit z
  bit1 = bit o

  open import Program Σ V

  -- | Program consisting of
  -- ⇒ bit(0)
  -- ⇒ bit(1)
  -- ⇒ blist(nil)
  -- bit(x), blist(y) ⇒ blist(cons(x,y))
  P : Program
  P = , clauses
    where
      clauses : Fin 4 → Clause
      clauses zero                = (0 , (λ ())) ⊢ bit0
      clauses (suc zero)          = (0 , (λ ())) ⊢ bit1
      clauses (suc (suc zero))    = (0 , (λ ())) ⊢ nil
      clauses (suc (suc (suc c))) = (2 , b)      ⊢ blist (cons (η 0) (η 1))
        where
          b : Fin 2 → T V
          b zero = bit (η 0)
          b (suc i) = blist (η 1)

  open import Rewrite Σ V P

  X S bitX : T V
  X = η 0
  S = blist (cons X (cons X nil))
  bitX = bit X

  bitX-val : Val bitX
  bitX-val zero                ()      x
  bitX-val (suc zero)          ()      x
  bitX-val (suc (suc zero))    ()      x
  bitX-val (suc (suc (suc _))) zero    ()
  bitX-val (suc (suc (suc _))) (suc _) ()

  step1 : S ⟿ bitX
  step1 = rew-step (# 3) (# 0) {σ} σ-match
    where
      σ : Subst V V
      σ zero = X
      σ (suc zero) = cons X nil
      σ (suc (suc n)) = η (suc (suc n))

      σ-match : matches (geth P (# 3)) S σ
      σ-match =
        begin
          app σ (blist (cons X (η 1)))
        ≡⟨ refl ⟩
          μ (T₁ σ (blist (cons X (η 1))))
        ≡⟨ refl ⟩
          μ (T₁ σ (μ (ι (BList , (λ _ → (cons X (η 1)))))))
        ≡⟨ refl ⟩
          μ (μ (ι (BList , (λ _ → T₁ σ (cons X (η 1))))))
        ≡⟨ refl ⟩
          μ (μ (ι (BList , (λ _ → T₁ σ (μ (ι (Cons , bin-branch X (η 1))))))))
        ≡⟨ refl ⟩
          μ (μ (ι (BList , (λ _ → μ (ι (Cons , T₁ σ ∘ (bin-branch X (η 1))))))))
        ≡⟨ cong (λ u → μ (μ (ι (BList , (λ _ → μ (ι (Cons , u)))))))
                (cons-br-distr X (η 1) (T₁ σ)) ⟩
          μ (μ (ι (BList , (λ _ →
               μ (ι (Cons , (bin-branch (T₁ σ X) (T₁ σ (η 1)))))))))
        ≡⟨ refl ⟩
          μ (μ (ι (BList , (λ _ →
               μ (ι (Cons , (bin-branch (η (σ 0)) (η (σ 1)))))))))
        ≡⟨ cong (λ u → μ (μ (ι (BList , (λ _ → μ (ι (Cons , u)))))))
                (sym (cons-br-distr (σ 0) (σ 1) η)) ⟩
          μ (μ (ι (BList , (λ _ →
               μ (ι (Cons , (η ∘ (bin-branch (σ 0) (σ 1)))))))))
        ≡⟨ refl ⟩
          blist (cons (σ 0) (σ 1))
        ≡⟨ refl ⟩
          blist (cons X (cons X nil))
        ≡⟨ refl ⟩
          S
        ∎

  term1 : S ↓ bitX
  term1 = step bitX bitX (val bitX-val) step1

  -- Problem: The substitution needs to match _all_ leaves!!!
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
open import Prelude
open import Nat
open import core

module binders-disjoint-checks where
  -- these are fairly mechanical lemmas that show that the
  -- judgementally-defined binders-disjoint is really a type-directed
  -- function
  mutual
    lem-bdσ-lam : ∀{σ x τ d} → binders-disjoint-σ σ (·λ_[_]_ x τ d) → binders-disjoint-σ σ d
    lem-bdσ-lam BDσId = BDσId
    lem-bdσ-lam (BDσSubst x₁ bd) = BDσSubst (lem-bd-lam x₁) (lem-bdσ-lam bd)

    lem-bd-lam :  ∀{ d1 x τ1 d} → binders-disjoint d1 (·λ_[_]_ x  τ1 d) → binders-disjoint d1 d
    lem-bd-lam BDConst = BDConst
    lem-bd-lam BDVar = BDVar
    lem-bd-lam (BDLam bd (UBLam2 x₂ x₃)) = BDLam (lem-bd-lam bd) x₃
    lem-bd-lam (BDHole x₁) = BDHole (lem-bdσ-lam x₁)
    lem-bd-lam (BDNEHole x₁ bd) = BDNEHole (lem-bdσ-lam x₁) (lem-bd-lam bd)
    lem-bd-lam (BDAp bd bd₁) = BDAp (lem-bd-lam bd) (lem-bd-lam bd₁)
    lem-bd-lam (BDCast bd) = BDCast (lem-bd-lam bd)
    lem-bd-lam (BDFailedCast bd) = BDFailedCast (lem-bd-lam bd)

  mutual
    lem-bdσ-hole : ∀{d u σ σ'} → binders-disjoint-σ σ ⦇⌜ d ⌟⦈⟨ u , σ' ⟩ → binders-disjoint-σ σ d
    lem-bdσ-hole BDσId = BDσId
    lem-bdσ-hole (BDσSubst x bd) = BDσSubst (lem-bd-hole x) (lem-bdσ-hole bd)

    lem-bd-hole : ∀{d1 d u σ} → binders-disjoint d1 ⦇⌜ d ⌟⦈⟨ u , σ ⟩ → binders-disjoint d1 d
    lem-bd-hole BDConst = BDConst
    lem-bd-hole BDVar = BDVar
    lem-bd-hole (BDLam bd (UBNEHole x₁ x₂)) = BDLam (lem-bd-hole bd) x₂
    lem-bd-hole (BDHole x) = BDHole (lem-bdσ-hole x)
    lem-bd-hole (BDNEHole x bd) = BDNEHole (lem-bdσ-hole x) (lem-bd-hole bd)
    lem-bd-hole (BDAp bd bd₁) = BDAp (lem-bd-hole bd) (lem-bd-hole bd₁)
    lem-bd-hole (BDCast bd) = BDCast (lem-bd-hole bd)
    lem-bd-hole (BDFailedCast bd) = BDFailedCast (lem-bd-hole bd)

  mutual
    lem-bdσ-cast : ∀{σ d τ1 τ2} → binders-disjoint-σ σ (d ⟨ τ1 ⇒ τ2 ⟩) → binders-disjoint-σ σ d
    lem-bdσ-cast BDσId = BDσId
    lem-bdσ-cast (BDσSubst x bd) = BDσSubst (lem-bd-cast x) (lem-bdσ-cast bd)

    lem-bd-cast : ∀{d1 d τ1 τ2} → binders-disjoint d1 (d ⟨ τ1 ⇒ τ2 ⟩) → binders-disjoint d1 d
    lem-bd-cast BDConst = BDConst
    lem-bd-cast BDVar = BDVar
    lem-bd-cast (BDLam bd (UBCast x₁)) = BDLam (lem-bd-cast bd) x₁
    lem-bd-cast (BDHole x) = BDHole (lem-bdσ-cast x)
    lem-bd-cast (BDNEHole x bd) = BDNEHole (lem-bdσ-cast x) (lem-bd-cast bd)
    lem-bd-cast (BDAp bd bd₁) = BDAp (lem-bd-cast bd) (lem-bd-cast bd₁)
    lem-bd-cast (BDCast bd) = BDCast (lem-bd-cast bd)
    lem-bd-cast (BDFailedCast bd) = BDFailedCast (lem-bd-cast bd)

  mutual
    lem-bdσ-failedcast : ∀{σ d τ1 τ2} → binders-disjoint-σ σ (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) → binders-disjoint-σ σ d
    lem-bdσ-failedcast BDσId = BDσId
    lem-bdσ-failedcast (BDσSubst x bd) = BDσSubst (lem-bd-failedcast x) (lem-bdσ-failedcast bd)

    lem-bd-failedcast : ∀{d1 d τ1 τ2} → binders-disjoint d1 (d ⟨ τ1 ⇒⦇-⦈⇏ τ2 ⟩) → binders-disjoint d1 d
    lem-bd-failedcast BDConst = BDConst
    lem-bd-failedcast BDVar = BDVar
    lem-bd-failedcast (BDLam bd (UBFailedCast x₁)) = BDLam (lem-bd-failedcast bd) x₁
    lem-bd-failedcast (BDHole x) = BDHole (lem-bdσ-failedcast x)
    lem-bd-failedcast (BDNEHole x bd) = BDNEHole (lem-bdσ-failedcast x) (lem-bd-failedcast bd)
    lem-bd-failedcast (BDAp bd bd₁) = BDAp (lem-bd-failedcast bd) (lem-bd-failedcast bd₁)
    lem-bd-failedcast (BDCast bd) = BDCast (lem-bd-failedcast bd)
    lem-bd-failedcast (BDFailedCast bd) = BDFailedCast (lem-bd-failedcast bd)

  mutual
    lem-bdσ-into-cast : ∀{σ d τ1 τ2} → binders-disjoint-σ σ d → binders-disjoint-σ σ (d ⟨ τ1 ⇒ τ2 ⟩)
    lem-bdσ-into-cast BDσId = BDσId
    lem-bdσ-into-cast (BDσSubst x bd) = BDσSubst (lem-bd-into-cast x) (lem-bdσ-into-cast bd)

    lem-bd-into-cast : ∀{d1 d2 τ1 τ2} → binders-disjoint d1 d2 → binders-disjoint d1 (d2 ⟨ τ1 ⇒ τ2 ⟩)
    lem-bd-into-cast BDConst = BDConst
    lem-bd-into-cast BDVar = BDVar
    lem-bd-into-cast (BDLam bd x₁) = BDLam (lem-bd-into-cast bd) (UBCast x₁)
    lem-bd-into-cast (BDHole x) = BDHole (lem-bdσ-into-cast x)
    lem-bd-into-cast (BDNEHole x bd) = BDNEHole (lem-bdσ-into-cast x) (lem-bd-into-cast bd)
    lem-bd-into-cast (BDAp bd bd₁) = BDAp (lem-bd-into-cast bd) (lem-bd-into-cast bd₁)
    lem-bd-into-cast (BDCast bd) = BDCast (lem-bd-into-cast bd)
    lem-bd-into-cast (BDFailedCast bd) = BDFailedCast (lem-bd-into-cast bd)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Left inverses
------------------------------------------------------------------------

module Function.LeftInverse where

open import Data.Product
open import Level
import Relation.Binary.EqReasoning as EqReasoning
open import Relation.Binary
open import Function.Equality as Eq
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
open import Function.Equivalence using (Equivalence)
open import Function.Injection using (Injective; Injection)
import Relation.Binary.PropositionalEquality as P

-- Left and right inverses.

_LeftInverseOf_ :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  To ⟶ From → From ⟶ To → Set _
_LeftInverseOf_ {From = From} f g = ∀ x → f ⟨$⟩ (g ⟨$⟩ x) ≈ x
  where open Setoid From

_RightInverseOf_ :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  To ⟶ From → From ⟶ To → Set _
f RightInverseOf g = g LeftInverseOf f

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

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

  private
    open module F = Setoid From
    open module T = Setoid To
  open EqReasoning From

  injective : Injective to
  injective {x} {y} eq = begin
    x                    ≈⟨ F.sym (left-inverse-of x) ⟩
    from ⟨$⟩ (to ⟨$⟩ x)  ≈⟨ Eq.cong from eq ⟩
    from ⟨$⟩ (to ⟨$⟩ y)  ≈⟨ left-inverse-of y ⟩
    y                    ∎

  injection : Injection From To
  injection = record { to = to; injective = injective }

  equivalence : Equivalence From To
  equivalence = record
    { to   = to
    ; from = from
    }

  to-from : ∀ {x y} → to ⟨$⟩ x T.≈ y → from ⟨$⟩ y F.≈ x
  to-from {x} {y} to-x≈y = begin
    from ⟨$⟩ y           ≈⟨ Eq.cong from (T.sym to-x≈y) ⟩
    from ⟨$⟩ (to ⟨$⟩ x)  ≈⟨ left-inverse-of x ⟩
    x                    ∎

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

RightInverse : ∀ {f₁ f₂ t₁ t₂}
               (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) → Set _
RightInverse From To = LeftInverse To From

-- The set of all left inverses from one set to another. (Read A ↞ B
-- as "surjection from B to A".)

infix 3 _↞_

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

-- Identity and composition.

id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → LeftInverse S S
id {S = S} = record
  { to              = Eq.id
  ; from            = Eq.id
  ; left-inverse-of = λ _ → Setoid.refl S
  }

infixr 9 _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
      LeftInverse M T → LeftInverse F M → LeftInverse F T
_∘_ {F = F} f g = record
  { to              = to   f ⟪∘⟫ to   g
  ; from            = from g ⟪∘⟫ from f
  ; left-inverse-of = λ x → begin
      from g ⟨$⟩ (from f ⟨$⟩ (to f ⟨$⟩ (to g ⟨$⟩ x)))  ≈⟨ Eq.cong (from g) (left-inverse-of f (to g ⟨$⟩ x)) ⟩
      from g ⟨$⟩ (to g ⟨$⟩ x)                          ≈⟨ left-inverse-of g x ⟩
      x                                                ∎
  }
  where
  open LeftInverse
  open EqReasoning F


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Canonical model equipment for Kripke-style semantics.

module BasicIS4.Equipment.KripkeDyadicCanonical where

open import BasicIS4.Syntax.Common public

module Syntax
    (_⊢_    : Cx² Ty Ty → Ty → Set)
    (mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A)
    (up      : ∀ {A Π} → Π ⊢ (□ A) → Π ⊢ (□ □ A))
    (down    : ∀ {A Π} → Π ⊢ (□ A) → Π ⊢ A)
    (lift    : ∀ {A Γ Δ} → (Γ ⁏ Δ) ⊢ A → (□⋆ Γ ⁏ Δ) ⊢ (□ A))
  where

  -- Worlds.

  Worldᶜ : Set
  Worldᶜ = Cx² Ty Ty

  -- Intuitionistic accessibility.

  infix 3 _≤ᶜ_
  _≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤ᶜ_ = _⊆²_

  refl≤ᶜ : ∀ {w} → w ≤ᶜ w
  refl≤ᶜ = refl⊆²

  trans≤ᶜ : ∀ {w w′ w″} → w ≤ᶜ w′ → w′ ≤ᶜ w″ → w ≤ᶜ w″
  trans≤ᶜ = trans⊆²

  bot≤ᶜ : ∀ {w} → ∅² ≤ᶜ w
  bot≤ᶜ = bot⊆²

  -- The canonical modal accessibility, based on the T axiom.

  infix 3 _Rᶜ_
  _Rᶜ_ : Worldᶜ → Worldᶜ → Set
  w Rᶜ w′ = ∀ {A} → w ⊢ (□ A) → w′ ⊢ A

  reflRᶜ : ∀ {w} → w Rᶜ w
  reflRᶜ = down

  transRᶜ : ∀ {w w′ w″} → w Rᶜ w′ → w′ Rᶜ w″ → w Rᶜ w″
  transRᶜ ζ ζ′ = ζ′ ∘ ζ ∘ up

  botRᶜ : ∀ {w} → ∅² Rᶜ w
  botRᶜ = mono²⊢ bot≤ᶜ ∘ down

  liftRᶜ : ∀ {Γ Δ} → Γ ⁏ Δ Rᶜ □⋆ Γ ⁏ Δ
  liftRᶜ = down ∘ lift ∘ down

  -- Composition of accessibility.

  infix 3 _≤⨾Rᶜ_
  _≤⨾Rᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⨾Rᶜ_ = _≤ᶜ_ ⨾ _Rᶜ_

  infix 3 _R⨾≤ᶜ_
  _R⨾≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _R⨾≤ᶜ_ = _Rᶜ_ ⨾ _≤ᶜ_

  refl≤⨾Rᶜ : ∀ {w} → w ≤⨾Rᶜ w
  refl≤⨾Rᶜ {w} = w , (refl≤ᶜ , reflRᶜ)

  reflR⨾≤ᶜ : ∀ {w} → w R⨾≤ᶜ w
  reflR⨾≤ᶜ {w} = w , (reflRᶜ , refl≤ᶜ)

  -- Persistence condition, after Iemhoff; included by Ono.
  --
  --   w′      v′  →           v′
  --   ◌───R───●   →           ●
  --   │           →         ╱
  --   ≤  ξ,ζ      →       R
  --   │           →     ╱
  --   ●           →   ●
  --   w           →   w

  ≤⨾R→Rᶜ : ∀ {v′ w} → w ≤⨾Rᶜ v′ → w Rᶜ v′
  ≤⨾R→Rᶜ (w′ , (ξ , ζ)) = ζ ∘ mono²⊢ ξ

  -- Brilliance condition, after Iemhoff.
  --
  --           v′  →           v′
  --           ●   →           ●
  --           │   →         ╱
  --      ζ,ξ  ≤   →       R
  --           │   →     ╱
  --   ●───R───◌   →   ●
  --   w       v   →   w

  R⨾≤→Rᶜ : ∀ {w v′} → w R⨾≤ᶜ v′ → w Rᶜ v′
  R⨾≤→Rᶜ (v , (ζ , ξ)) = mono²⊢ ξ ∘ ζ

  -- Minor persistence condition, included by Božić and Došen.
  --
  --   w′      v′  →           v′
  --   ◌───R───●   →           ●
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ●           →   ●───R───◌
  --   w           →   w       v
  --
  --                   w″  →                   w″
  --                   ●   →                   ●
  --                   │   →                   │
  --             ξ′,ζ′ ≤   →                   │
  --                   │   →                   │
  --           ●───R───◌   →                   ≤
  --           │       v′  →                   │
  --      ξ,ζ  ≤           →                   │
  --           │           →                   │
  --   ●───R───◌           →   ●───────R───────◌
  --   w       v           →   w               v″

  ≤⨾R→R⨾≤ᶜ : ∀ {v′ w} → w ≤⨾Rᶜ v′ → w R⨾≤ᶜ v′
  ≤⨾R→R⨾≤ᶜ {v′} ξ,ζ = v′ , (≤⨾R→Rᶜ ξ,ζ , refl≤ᶜ)

  transR⨾≤ᶜ : ∀ {w′ w w″} → w R⨾≤ᶜ w′ → w′ R⨾≤ᶜ w″ → w R⨾≤ᶜ w″
  transR⨾≤ᶜ {w′} (v , (ζ , ξ)) (v′ , (ζ′ , ξ′)) = let v″ , (ζ″ , ξ″) = ≤⨾R→R⨾≤ᶜ (w′ , (ξ , ζ′))
                                                  in  v″ , (transRᶜ ζ ζ″ , trans≤ᶜ ξ″ ξ′)

  ≤→Rᶜ : ∀ {v′ w} → w ≤ᶜ v′ → w Rᶜ v′
  ≤→Rᶜ {v′} ξ = ≤⨾R→Rᶜ (v′ , (ξ , reflRᶜ))

  -- Minor brilliance condition, included by Ewald and Alechina et al.
  --
  --           v′  →   w′      v′
  --           ●   →   ◌───R───●
  --           │   →   │
  --      ζ,ξ  ≤   →   ≤
  --           │   →   │
  --   ●───R───◌   →   ●
  --   w       v   →   w
  --
  --           v′      w″  →   v″              w″
  --           ◌───R───●   →   ◌───────R───────●
  --           │           →   │
  --           ≤  ξ′,ζ′    →   │
  --   v       │           →   │
  --   ◌───R───●           →   ≤
  --   │       w′          →   │
  --   ≤  ξ,ζ              →   │
  --   │                   →   │
  --   ●                   →   ●
  --   w                   →   w

  R⨾≤→≤⨾Rᶜ : ∀ {w v′} → w R⨾≤ᶜ v′ → w ≤⨾Rᶜ v′
  R⨾≤→≤⨾Rᶜ {w} ζ,ξ = w , (refl≤ᶜ , R⨾≤→Rᶜ ζ,ξ)

  trans≤⨾Rᶜ : ∀ {w′ w w″} → w ≤⨾Rᶜ w′ → w′ ≤⨾Rᶜ w″ → w ≤⨾Rᶜ w″
  trans≤⨾Rᶜ {w′} (v , (ξ , ζ)) (v′ , (ξ′ , ζ′)) = let v″ , (ξ″ , ζ″) = R⨾≤→≤⨾Rᶜ (w′ , (ζ , ξ′))
                                                  in  v″ , (trans≤ᶜ ξ ξ″ , transRᶜ ζ″ ζ′)

  ≤→Rᶜ′ : ∀ {w v′} → w ≤ᶜ v′ → w Rᶜ v′
  ≤→Rᶜ′ {w} ξ = R⨾≤→Rᶜ (w , (reflRᶜ , ξ))

  -- Infimum (greatest lower bound) of accessibility.
  --
  --   w′
  --   ●
  --   │
  --   ≤  ξ,ζ
  --   │
  --   ◌───R───●
  --   w       v

  infix 3 _≤⊓Rᶜ_
  _≤⊓Rᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⊓Rᶜ_ = _≤ᶜ_ ⊓ _Rᶜ_

  infix 3 _R⊓≤ᶜ_
  _R⊓≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _R⊓≤ᶜ_ = _Rᶜ_ ⊓ _≤ᶜ_

  ≤⊓R→R⊓≤ᶜ : ∀ {w′ v} → w′ ≤⊓Rᶜ v → v R⊓≤ᶜ w′
  ≤⊓R→R⊓≤ᶜ (w , (ξ , ζ)) = w , (ζ , ξ)

  R⊓≤→≤⊓Rᶜ : ∀ {w′ v} → v R⊓≤ᶜ w′ → w′ ≤⊓Rᶜ v
  R⊓≤→≤⊓Rᶜ (w , (ζ , ξ)) = w , (ξ , ζ)

  -- Supremum (least upper bound) of accessibility.
  --
  --   w′      v′
  --   ●───R───◌
  --           │
  --      ξ,ζ  ≤
  --           │
  --           ●
  --           v

  infix 3 _≤⊔Rᶜ_
  _≤⊔Rᶜ_ : Worldᶜ → Worldᶜ → Set
  _≤⊔Rᶜ_ = _≤ᶜ_ ⊔ _Rᶜ_

  infix 3 _R⊔≤ᶜ_
  _R⊔≤ᶜ_ : Worldᶜ → Worldᶜ → Set
  _R⊔≤ᶜ_ = _Rᶜ_ ⊔ _≤ᶜ_

  ≤⊔R→R⊔≤ᶜ : ∀ {w′ v} → w′ ≤⊔Rᶜ v → v R⊔≤ᶜ w′
  ≤⊔R→R⊔≤ᶜ (v′ , (ξ , ζ)) = v′ , (ζ , ξ)

  R⊔≤→≤⊔Rᶜ : ∀ {w′ v} → v R⊔≤ᶜ w′ → w′ ≤⊔Rᶜ v
  R⊔≤→≤⊔Rᶜ (v′ , (ζ , ξ)) = v′ , (ξ , ζ)

  -- Infimum-to-supremum condition, included by Ewald.
  --
  --   w′          →   w′      v′
  --   ●           →   ●───R───◌
  --   │           →           │
  --   ≤  ξ,ζ      →           ≤
  --   │           →           │
  --   ◌───R───●   →           ●
  --   w       v   →           v

  -- NOTE: This could be more precise.
  ≤⊓R→≤⊔Rᶜ : ∀ {v w′} → w′ ≤⊓Rᶜ v → v ≤⊔Rᶜ w′
  ≤⊓R→≤⊔Rᶜ {v} {w′} (w , (ξ , ζ)) =
    (w′ ⧺² v) , (weak⊆²⧺₂ , mono²⊢ (weak⊆²⧺₁ v) ∘ down)

  -- Supremum-to-infimum condition.
  --
  --   w′      v′  →   w′
  --   ●───R───◌   →   ●
  --           │   →   │
  --      ξ,ζ  ≤   →   ≤
  --           │   →   │
  --           ●   →   ◌───R───●
  --           v   →   w       v

  -- NOTE: This could be more precise.
  ≤⊔R→≤⊓Rᶜ : ∀ {w′ v} → v ≤⊔Rᶜ w′ → w′ ≤⊓Rᶜ v
  ≤⊔R→≤⊓Rᶜ (v′ , (ξ , ζ)) = ∅² , (bot≤ᶜ , botRᶜ)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-

Definition of the Klein bottle as a HIT

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.KleinBottle.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Cubical.Data.Int public renaming (_+_ to _+Int_ ; +-assoc to +Int-assoc; +-comm to +Int-comm)
open import Cubical.Data.Prod
open import Cubical.Data.Sigma
open import Cubical.HITs.S1
open import Cubical.HITs.PropositionalTruncation

open import Cubical.HITs.KleinBottle.Base

loop1 : S¹ → KleinBottle
loop1 base = point
loop1 (loop i) = line1 i

invS¹Loop : S¹ → Set
invS¹Loop base = S¹
invS¹Loop (loop i) = invS¹Path i

loop1Inv : (s : S¹) → loop1 (inv s) ≡ loop1 s
loop1Inv base = line2
loop1Inv (loop i) = square i

twist : (s : S¹) → PathP (λ i → invS¹Path i) s (inv s)
twist s i = glue (λ {(i = i0) → s; (i = i1) → inv s}) (inv s)

twistBaseLoop : (s : S¹) → invS¹Loop s
twistBaseLoop base = base
twistBaseLoop (loop i) = twist base i

kleinBottle≃Σ : KleinBottle ≃ Σ S¹ invS¹Loop
kleinBottle≃Σ = isoToEquiv (iso fro to froTo toFro)
  where
  fro : KleinBottle → Σ S¹ invS¹Loop
  fro point = (base , base)
  fro (line1 i) = (base , loop i)
  fro (line2 j) = (loop (~ j) , twist base (~ j))
  fro (square i j) = (loop (~ j) , twist (loop i) (~ j))

  toLoopFiller : (j : I) → ua invS¹Equiv j → I → KleinBottle
  toLoopFiller j g l =
    hfill
      (λ l → λ
        { (j = i0) → loop1Inv g l
        ; (j = i1) → loop1 g
        })
      (inS (loop1 (unglue (j ∨ ~ j) g)))
      l

  to : Σ S¹ invS¹Loop → KleinBottle
  to (base , s) = loop1 s
  to (loop j , g) = toLoopFiller j g i1

  toFro : (a : KleinBottle) → to (fro a) ≡ a
  toFro point = refl
  toFro (line1 i) = refl
  toFro (line2 j) k = lUnit line2 (~ k) j
  toFro (square i j) k = lUnit (square i) (~ k) j

  froLoop1 : (s : S¹) → fro (loop1 s) ≡ (base , s)
  froLoop1 base = refl
  froLoop1 (loop i) = refl

  froLoop1Inv :
    PathP (λ k → (s : S¹) → froLoop1 (inv s) k ≡ froLoop1 s k)
      (λ s l → fro (loop1Inv s l))
      (λ s l → loop (~ l) , twist s (~ l))
  froLoop1Inv k base l = loop (~ l) , twist base (~ l)
  froLoop1Inv k (loop i) l = loop (~ l) , twist (loop i) (~ l)

  froTo : (a : Σ S¹ invS¹Loop) → fro (to a) ≡ a
  froTo (base , s) = froLoop1 s
  froTo (loop j , g) k =
    hcomp
      (λ l → λ
        { (j = i0) → froLoop1Inv k g l
        ; (j = i1) → froLoop1 g k
        ; (k = i0) → fro (toLoopFiller j g l)
        ; (k = i1) →
          ( loop (j ∨ ~ l)
          , glue
             (λ
               { (j = i0) (l = i1) → g
               ; (j = i1) → g
               ; (l = i0) → unglue (j ∨ ~ j) g
               })
             (unglue (j ∨ ~ j) g)
          )
        })
      (froLoop1 (unglue (j ∨ ~ j) g) k)

isGroupoidKleinBottle : isGroupoid KleinBottle
isGroupoidKleinBottle =
  transport (λ i → isGroupoid (ua kleinBottle≃Σ (~ i)))
    (isOfHLevelΣ 3 isGroupoidS¹
      (λ s →
        recPropTrunc
          (isPropIsOfHLevel 3 (invS¹Loop s))
          (λ p → subst (λ s → isGroupoid (invS¹Loop s)) p isGroupoidS¹)
          (isConnectedS¹ s)))

-- Transport across the following is too slow :(

ΩKlein≡Int² : Path KleinBottle point point ≡ Int × Int
ΩKlein≡Int² =
  Path KleinBottle point point
    ≡⟨ (λ i → basePath i ≡ basePath i) ⟩
  Path (Σ S¹ invS¹Loop) (base , base) (base , base)
    ≡⟨ sym (ua Σ≡) ⟩
  Σ ΩS¹ (λ p → PathP (λ j → invS¹Loop (p j)) base base)
    ≡⟨ (λ i → Σ ΩS¹ (λ p → PathP (λ j → invS¹Loop (p (j ∨ i))) (twistBaseLoop (p i)) base)) ⟩
  Σ ΩS¹ (λ _ → ΩS¹)
    ≡⟨ sym A×B≡A×ΣB ⟩
  ΩS¹ × ΩS¹
    ≡⟨ (λ i → ΩS¹≡Int i × ΩS¹≡Int i) ⟩
  Int × Int ∎
  where
  basePath : PathP (λ i → ua kleinBottle≃Σ i) point (base , base)
  basePath i = glue (λ {(i = i0) → point; (i = i1) → base , base}) (base , base)

-- We can at least define the winding function directly and get results on small examples

windingKlein : Path KleinBottle point point → Int × Int
windingKlein p = (z₀ , z₁)
  where
  step₀ : Path (Σ S¹ invS¹Loop) (base , base) (base , base)
  step₀ = (λ i → kleinBottle≃Σ .fst (p i))

  z₀ : Int
  z₀ = winding (λ i → kleinBottle≃Σ .fst (p i) .fst)

  z₁ : Int
  z₁ = winding
    (transport
      (λ i → PathP (λ j → invS¹Loop (step₀ (j ∨ i) .fst)) (twistBaseLoop (step₀ i .fst)) base)
      (cong snd step₀))

_ : windingKlein line1 ≡ (pos 0 , pos 1)
_ = refl

_ : windingKlein line2 ≡ (negsuc 0 , pos 0)
_ = refl

_ : windingKlein (line1 ∙ line2) ≡ (negsuc 0 , negsuc 0)
_ = refl

_ : windingKlein (line1 ∙ line2 ∙ line1) ≡ (negsuc 0 , pos 0)
_ = refl

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- An ATP hint must be used with functions.

-- This error is detected by TypeChecking.Rules.Decl.

module ATPBadHint2 where

data Bool : Set where
  false true : Bool

{-# ATP hint Bool #-}

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda