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

open import Categories.Bicategory using (Bicategory)

-- The 1-cell dual (op) and 2-cell dual (co) of a given bicategory.

module Categories.Bicategory.Opposite where

open import Data.Product using (_,_)

import Categories.Bicategory.Extras as BicategoryExtras
open import Categories.Category using (Category)
import Categories.Category.Cartesian as Cartesian
import Categories.Morphism as Morphism
import Categories.Morphism.Reasoning as MorphismReasoning
open import Categories.Category.Product using (Swap)
open import Categories.Functor using (Functor; _∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; niHelper)

-- There several ways to dualize a bicategory:
--
--  * flip the 1-cells (op C), or
--  * flip the 2-cells (co C).
--  * flip both (coop C).
--
-- We implement all three.

module _ {o ℓ e t} (C : Bicategory o ℓ e t) where

  open BicategoryExtras C
  open Shorthands
  private
    module MR {A} {B} where
      open Morphism          (hom A B) public using (module ≅)
      open MorphismReasoning (hom A B) public using (switch-tofromʳ)
  open MR

  -- The 1-cell dual of C.
  --
  -- NOTE.  The definition here is specialized to the particular choice
  -- of tensor product (cartesian) and braiding (swap) used in the
  -- definition of Bicategories.  We could instead have defined the
  -- `enriched' field using the generic `op' operation defined in
  -- Categories.Enriched.Category.Opposite, but that would have resulted
  -- in much more complicated proofs of the triangle and pentagon
  -- identities.  That's because the definition of associativity and the
  -- unit laws in the generic opposite enriched category has to work for
  -- any choice of braiding and is therefore more involved.  When these
  -- laws become natural isomorphism in the definition of Bicategories,
  -- they turn into long chains consisting of mostly identity morphisms
  -- that make the types of the triangle and pentagon identities
  -- enormous.  We can avoid this by specializing the definitions of the
  -- associators and unitors below.
  --
  -- Note also that this version of `op' is almost a (definitional)
  -- involution.  The problematic fields are the triangle and pentagon
  -- identities which are not involutive on the nose.  This could be
  -- fixed by adding additional fields (in the style of `sym-assoc' in
  -- Category).  To also support `co` and `coop` would require two more
  -- variants of each equation, so there would be quite a lot of
  -- redundancy in the end.

  op : Bicategory o ℓ e t
  op = record
    { enriched = record
      { Obj = Obj
      ; hom = λ A B → hom B A
      ; id  = id
      ; ⊚   = ⊚ ∘F Swap
      ; ⊚-assoc = niHelper (record
        { η       = λ{ ((f , g) , h) → ⊚-assoc.⇐.η ((h , g) , f) }
        ; η⁻¹     = λ{ ((f , g) , h) → ⊚-assoc.⇒.η ((h , g) , f) }
        ; commute = λ{ ((α , β) , γ) → ⊚-assoc.⇐.commute ((γ , β) , α) }
        ; iso     = λ _ → record
          { isoˡ = ⊚-assoc.iso.isoʳ _ ; isoʳ = ⊚-assoc.iso.isoˡ _ }
        })
      ; unitˡ = niHelper (record
        { η       = λ{ (_ , g) → unitʳ.⇒.η (g , _) }
        ; η⁻¹     = λ{ (_ , g) → unitʳ.⇐.η (g , _) }
        ; commute = λ{ (_ , β) → unitʳ.⇒.commute (β , _) }
        ; iso     = λ{ (_ , g) → record
          { isoˡ = unitʳ.iso.isoˡ (g , _) ; isoʳ = unitʳ.iso.isoʳ (g , _) } }
        })
      ; unitʳ = niHelper (record
        { η       = λ{ (f , _) → unitˡ.⇒.η (_ , f) }
        ; η⁻¹     = λ{ (f , _) → unitˡ.⇐.η (_ , f) }
        ; commute = λ{ (α , _) → unitˡ.⇒.commute (_ , α) }
        ; iso     = λ{ (f , _) → record
          { isoˡ = unitˡ.iso.isoˡ (_ , f) ; isoʳ = unitˡ.iso.isoʳ (_ , f) } }
        })
      }
    ; triangle = λ {_ _ _ f g} → begin
        ρ⇒ ◁ g ∘ᵥ α⇐   ≈˘⟨ switch-tofromʳ (≅.sym associator) triangle ⟩
        f ▷ λ⇒         ∎
    ; pentagon = λ {_ _ _ _ _ f g h i} → begin
        α⇐ ◁ i ∘ᵥ α⇐ ∘ᵥ f ▷ α⇐     ≈˘⟨ hom.assoc ⟩
        (α⇐ ◁ i ∘ᵥ α⇐) ∘ᵥ f ▷ α⇐   ≈⟨ pentagon-inv ⟩
        α⇐ ∘ᵥ α⇐                   ∎
    }
    where open hom.HomReasoning

  -- The 2-cell dual of C.

  co : Bicategory o ℓ e t
  co = record
    { enriched = record
      { Obj     = Obj
      ; hom     = λ A B → Category.op (hom A B)
      ; id      = Functor.op id
      ; ⊚       = Functor.op ⊚
      ; ⊚-assoc = NaturalIsomorphism.op′ ⊚-assoc
      ; unitˡ   = NaturalIsomorphism.op′ unitˡ
      ; unitʳ   = NaturalIsomorphism.op′ unitʳ
      }
    ; triangle  = triangle-inv
    ; pentagon  = pentagon-inv
    }

-- The combined 1- and 2-cell dual of C.

coop : ∀ {o ℓ e t} → Bicategory o ℓ e t → Bicategory o ℓ e t
coop C = co (op C)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import LogicalFormulae
open import Setoids.Setoids
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Setoids.Functions.Extension

module Groups.SymmetricGroups.Definition where

data SymmetryGroupElements {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
  sym : {f : A → A} → SetoidBijection S S f → SymmetryGroupElements S

symmetricSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (SymmetryGroupElements S)
Setoid._∼_ (symmetricSetoid S) (sym {f} bijF) (sym {g} bijG) = ExtensionallyEqual {S = S} {S} (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG)
Equivalence.reflexive (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} = extensionallyEqualReflexive S S f (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijF)
Equivalence.symmetric (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} {sym {g} bijG} f~g = extensionallyEqualSymmetric S S f g (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) f~g
Equivalence.transitive (Setoid.eq (symmetricSetoid S)) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} f~g g~h = extensionallyEqualTransitive S S f g h (SetoidBijection.wellDefined bijF) (SetoidBijection.wellDefined bijG) (SetoidBijection.wellDefined bijH) f~g g~h

symmetricGroupOp : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (f g : SymmetryGroupElements S) → SymmetryGroupElements S
symmetricGroupOp (sym {f} bijF) (sym {g} bijG) = sym (setoidBijComp bijG bijF)

symmetricGroupInv : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → SymmetryGroupElements S → SymmetryGroupElements S
symmetricGroupInv S (sym {f} bijF) with setoidBijectiveImpliesInvertible bijF
... | record { inverse = inverse ; inverseWellDefined = iwd ; isLeft = isLeft ; isRight = isRight } = sym (setoidInvertibleImpliesBijective (record { fWellDefined = iwd ; inverse = f ; inverseWellDefined = SetoidInjection.wellDefined (SetoidBijection.inj bijF) ; isLeft = λ b → isRight b ; isRight = λ b → isLeft b }))

symmetricGroupInvIsLeft : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp (symmetricGroupInv S x) x) (sym setoidIdIsBijective)
symmetricGroupInvIsLeft {A = A} S {sym {f = f} fBij} = ans
  where
    ans : {x : A} → Setoid._∼_ S (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) (f x)) x
    ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {f x}
    ans {x} | a , b = SetoidInjection.injective (SetoidBijection.inj fBij) b

symmetricGroupInvIsRight : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → {x : SymmetryGroupElements S} → Setoid._∼_ (symmetricSetoid S) (symmetricGroupOp x (symmetricGroupInv S x)) (sym setoidIdIsBijective)
symmetricGroupInvIsRight {A = A} S {sym {f = f} fBij} = ans
  where
    ans : {x : A} → Setoid._∼_ S (f (SetoidInvertible.inverse (setoidBijectiveImpliesInvertible fBij) x)) x
    ans {x} with SetoidSurjection.surjective (SetoidBijection.surj fBij) {x}
    ans {x} | a , b = b

symmetricGroup : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Group (symmetricSetoid S) (symmetricGroupOp {A = A})
Group.+WellDefined (symmetricGroup A) {sym {m} bijM} {sym {n} bijN} {sym {x} bijX} {sym {y} bijY} m~x n~y = transitive m~x (SetoidBijection.wellDefined bijX n~y)
  where
    open Equivalence (Setoid.eq A)
Group.0G (symmetricGroup A) = sym setoidIdIsBijective
Group.inverse (symmetricGroup S) = symmetricGroupInv S
Group.+Associative (symmetricGroup A) {sym {f} bijF} {sym {g} bijG} {sym {h} bijH} = Equivalence.reflexive (Setoid.eq A)
Group.identRight (symmetricGroup A) {sym {f} bijF} = Equivalence.reflexive (Setoid.eq A)
Group.identLeft (symmetricGroup A) {sym {f} bijF} = Equivalence.reflexive (Setoid.eq A)
Group.invLeft (symmetricGroup S) {x} = symmetricGroupInvIsLeft S {x}
Group.invRight (symmetricGroup S) {x} = symmetricGroupInvIsRight S {x}

ext: agda


text:
import Relation.Unary.Monotone as Mono
open import Relation.Binary using (Preorder)
open import Relation.Binary.PropositionalEquality
open import Level

module Category.Monad.Monotone.Heap
  -- preordered heap types
  {ℓ}(pre : Preorder ℓ ℓ ℓ)
  -- types
  (T : Set ℓ)
  -- weakenable values
  (V : T → Preorder.Carrier pre → Set ℓ) ⦃ wkV : ∀ {a} → Mono.Monotone pre (V a) ⦄
  -- heaps indexed by the heap type
  (H : Preorder.Carrier pre → Set ℓ)
  -- weakenable heap type membership
  (_∈_ : T → Preorder.Carrier pre → Set ℓ) ⦃ wk∈ : ∀ {a} → Mono.Monotone pre (_∈_ a) ⦄ where

open Preorder pre renaming (Carrier to I; _∼_ to _≤_; refl to ≤-refl; trans to ≤-trans)

open import Data.Unit using (⊤; tt)
open import Relation.Unary hiding (_∈_)
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Unary.Monotone pre
open import Data.Product
open import Category.Monad
open import Category.Monad.Monotone pre
open import Category.Monad.Identity

open import Category.Monad.Monotone.State pre H

record HeapMonad (M : Pt I ℓ) : Set (suc ℓ) where
  field
    ⦃ super ⦄ : StateMonad M

  open StateMonad super public

  field
    store  : ∀ {a} → V a ⊆ M (λ W → a ∈ W)
    modify : ∀ {a} → _∈_ a ⊆ V a ⇒ M (λ W' → Lift ⊤)
    deref  : ∀ {a} → _∈_ a ⊆ M (V a)

  module _ ⦃ m : RawMPMonad M ⦄ where
    open RawMPMonad m
    open import Data.List.All as All

    storeₙ  : ∀ {W as} → All (λ a → V a W) as → M (λ W' → All (λ a → a ∈ W') as) W
    storeₙ vs = sequenceM (All.map (λ v {x} ext → store (wk ext v)) vs)


text:
module BasicT.Metatheory.Gentzen-BasicTarski where

open import BasicT.Syntax.Gentzen public
open import BasicT.Semantics.BasicTarski public

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

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)     γ = lookup i γ
eval (lam t)     γ = λ a → eval t (γ , a)
eval (app t u)   γ = eval t γ $ eval u γ
eval (pair t u)  γ = eval t γ , eval u γ
eval (fst t)     γ = π₁ (eval t γ)
eval (snd t)     γ = π₂ (eval t γ)
eval unit        γ = ∙
eval true        γ = true
eval false       γ = false
eval (if t u v)  γ = ifᴮ (eval t γ) (eval u γ) (eval v γ)
eval zero        γ = zero
eval (suc t)     γ = suc (eval t γ)
eval (it t u v)  γ = itᴺ (eval t γ) (eval u γ) (eval v γ)
eval (rec t u v) γ = recᴺ (eval t γ) (eval u γ) (eval v γ)

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

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

module Pifextensional where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
open ≡-Reasoning

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

open import Groupoid

------------------------------------------------------------------------------
-- Level 0:

-- ZERO is a type with no elements
-- ONE is a type with one element 'tt'
-- PLUS ONE ONE is a type with elements 'false' and 'true'
-- and so on for all finite types built from ZERO, ONE, PLUS, and TIMES
--
-- We also have that U is a type with elements ZERO, ONE, PLUS ONE ONE,
--   TIMES BOOL BOOL, etc.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

-- Abbreviations for examples

BOOL BOOL² : U
BOOL  = PLUS ONE ONE
BOOL² = TIMES BOOL BOOL

false⟷ true⟷ : ⟦ BOOL ⟧
false⟷ = inj₁ tt
true⟷  = inj₂ tt

-- For any finite type (t : U) there is no non-trivial path structure
-- between the elements of t. All such finite types are discrete
-- groupoids
--
-- For U, there are non-trivial paths between its points. In the
-- conventional HoTT presentation, a path between t₁ and t₂ is
-- postulated by univalence for each equivalence between t₁ and t₂. In
-- the context of finite types, an equivalence corresponds to a
-- permutation as each permutation has a unique inverse
-- permutation. Thus instead of the detour using univalence, we can
-- give an inductive definition of all possible permutations between
-- finite types which naturally induces paths between the points. More
-- precisely, two types t₁ and t₂ have a path between them if there is
-- a permutation (c : t₁ ⟷ t₂). The fact that c is a permutation
-- guarantees, by construction, that (c ◎ ! c ∼ id⟷) and (! c ◎ c ∼
-- id⟷). A complete set of generators for all possible permutations
-- between finite types is given by the following definition. Note
-- that these permutations do not reach inside the types and hence do
-- not generate paths between the points within the types. The paths
-- are just between the types themselves.

infix  30 _⟷_
infixr 50 _◎_

data _⟷_ : U → U → Set where
  unite₊  : {t : U} → PLUS ZERO t ⟷ t
  uniti₊  : {t : U} → t ⟷ PLUS ZERO t
  swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
  assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
  assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
  unite⋆  : {t : U} → TIMES ONE t ⟷ t
  uniti⋆  : {t : U} → t ⟷ TIMES ONE t
  swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
  assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
  assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
  distz   : {t : U} → TIMES ZERO t ⟷ ZERO
  factorz : {t : U} → ZERO ⟷ TIMES ZERO t
  dist    : {t₁ t₂ t₃ : U} →
            TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
  factor  : {t₁ t₂ t₃ : U} →
            PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
  id⟷    : {t : U} → t ⟷ t
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)

-- Nicer syntax that shows intermediate values instead of the above
-- point-free notation of permutations

infixr 2  _⟷⟨_⟩_
infix  2  _□

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

_□ : (t : U) → {t : U} → (t ⟷ t)
_□ t = id⟷

-- Many ways of negating a BOOL. Again, it is absolutely critical that there
-- is NO path between false⟷ and true⟷. These permutations instead are based
-- on paths between x and neg (neg x) which are the trivial paths on each of
-- the two points in BOOL.

neg₁ neg₂ neg₃ neg₄ neg₅ : BOOL ⟷ BOOL
neg₁ = swap₊
neg₂ = id⟷ ◎ swap₊
neg₃ = swap₊ ◎ swap₊ ◎ swap₊
neg₄ = swap₊ ◎ id⟷
neg₅ = uniti⋆ ◎ swap⋆ ◎ (swap₊ ⊗ id⟷) ◎ swap⋆ ◎ unite⋆

-- CNOT

CNOT : BOOL² ⟷ BOOL²
CNOT = TIMES (PLUS x y) BOOL
         ⟷⟨ dist ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ id⟷ ⊕ (id⟷ ⊗ swap₊) ⟩
       PLUS (TIMES x BOOL) (TIMES y BOOL)
         ⟷⟨ factor ⟩
       TIMES (PLUS x y) BOOL □
  where x = ONE; y = ONE

-- TOFFOLI

TOFFOLI : TIMES BOOL BOOL² ⟷ TIMES BOOL BOOL²
TOFFOLI = TIMES (PLUS x y) BOOL²
            ⟷⟨ dist ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ id⟷ ⊕ (id⟷ ⊗ CNOT) ⟩
          PLUS (TIMES x BOOL²) (TIMES y BOOL²)
            ⟷⟨ factor ⟩
          TIMES (PLUS x y) BOOL² □
  where x = ONE; y = ONE

-- Every permutation has an inverse. There are actually many syntactically
-- different inverses but they are all equivalent.

! : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊    = uniti₊
! uniti₊    = unite₊
! swap₊     = swap₊
! assocl₊   = assocr₊
! assocr₊   = assocl₊
! unite⋆    = uniti⋆
! uniti⋆    = unite⋆
! swap⋆     = swap⋆
! assocl⋆   = assocr⋆
! assocr⋆   = assocl⋆
! distz     = factorz
! factorz   = distz
! dist      = factor
! factor    = dist
! id⟷      = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)

!! : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → ! (! c) ≡ c
!! {c = unite₊}  = refl
!! {c = uniti₊}  = refl
!! {c = swap₊}   = refl
!! {c = assocl₊} = refl
!! {c = assocr₊} = refl
!! {c = unite⋆}  = refl
!! {c = uniti⋆}  = refl
!! {c = swap⋆}   = refl
!! {c = assocl⋆} = refl
!! {c = assocr⋆} = refl
!! {c = distz}   = refl
!! {c = factorz} = refl
!! {c = dist}    = refl
!! {c = factor}  = refl
!! {c = id⟷}    = refl
!! {c = c₁ ◎ c₂} =
  begin (! (! (c₁ ◎ c₂))
           ≡⟨ refl ⟩
         ! (! c₂ ◎ ! c₁)
           ≡⟨ refl ⟩
         ! (! c₁) ◎ ! (! c₂)
           ≡⟨ cong₂ _◎_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ◎ c₂ ∎)
!! {c = c₁ ⊕ c₂} =
  begin (! (! (c₁ ⊕ c₂))
           ≡⟨ refl ⟩
         ! (! c₁) ⊕ ! (! c₂)
           ≡⟨ cong₂ _⊕_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ⊕ c₂ ∎)
!! {c = c₁ ⊗ c₂} =
  begin (! (! (c₁ ⊗ c₂))
           ≡⟨ refl ⟩
         ! (! c₁) ⊗ ! (! c₂)
           ≡⟨ cong₂ _⊗_ (!! {c = c₁}) (!! {c = c₂}) ⟩
         c₁ ⊗ c₂ ∎)

------------------------------------------------------------------------------
-- Extensional view of 2paths.
--
-- There is a 2path between two permutations p and q if for each x, the
-- result of p(x) and q(x) are identical.

-- First we define the extensional view of a permutation as a function.

ap : {t₁ t₂ : U} → (t₁ ⟷ t₂) → ⟦ t₁ ⟧ → ⟦ t₂ ⟧
ap unite₊ (inj₁ ())         -- absurd
ap unite₊ (inj₂ v)          = v
ap uniti₊ v                 = inj₂ v
ap swap₊ (inj₁ v)           = inj₂ v
ap swap₊ (inj₂ v)           = inj₁ v
ap assocl₊ (inj₁ v)         = inj₁ (inj₁ v)
ap assocl₊ (inj₂ (inj₁ v))  = inj₁ (inj₂ v)
ap assocl₊ (inj₂ (inj₂ v))  = inj₂ v
ap assocr₊ (inj₁ (inj₁ v))  = inj₁ v
ap assocr₊ (inj₁ (inj₂ v))  = inj₂ (inj₁ v)
ap assocr₊ (inj₂ v)         = inj₂ (inj₂ v)
ap unite⋆ (tt , v)          = v
ap uniti⋆ v                 = (tt , v)
ap swap⋆ (v₁ , v₂)          = (v₂ , v₁)
ap assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
ap assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
ap distz (() , _)           -- absurd
ap factorz ()               -- absurd
ap dist (inj₁ v₁ , v₃)      = inj₁ (v₁ , v₃)
ap dist (inj₂ v₂ , v₃)      = inj₂ (v₂ , v₃)
ap factor (inj₁ (v₁ , v₃))  = (inj₁ v₁ , v₃)
ap factor (inj₂ (v₂ , v₃))  = (inj₂ v₂ , v₃)
ap id⟷ v                   = v
ap (c₁ ◎ c₂) v              = ap c₂ (ap c₁ v)
ap (c₁ ⊕ c₂) (inj₁ v)       = inj₁ (ap c₁ v)
ap (c₁ ⊕ c₂) (inj₂ v)       = inj₂ (ap c₂ v)
ap (c₁ ⊗ c₂) (v₁ , v₂)      = (ap c₁ v₁ , ap c₂ v₂)

α◎!α : {t₁ t₂ : U} {α : t₁ ⟷ t₂} {v : ⟦ t₁ ⟧} → ap (α ◎ ! α) v ≡ v
α◎!α {α = unite₊} {inj₁ ()}
α◎!α {α = unite₊} {inj₂ v} = refl
α◎!α {α = uniti₊} {v} = refl
α◎!α {α = swap₊} {inj₁ v} = refl
α◎!α {α = swap₊} {inj₂ v} = refl
α◎!α {α = assocl₊} {inj₁ v} = refl
α◎!α {α = assocl₊} {inj₂ (inj₁ v)} = refl
α◎!α {α = assocl₊} {inj₂ (inj₂ v)} = refl
α◎!α {α = assocr₊} {inj₁ (inj₁ v)} = refl
α◎!α {α = assocr₊} {inj₁ (inj₂ v)} = refl
α◎!α {α = assocr₊} {inj₂ v} = refl
α◎!α {α = unite⋆} {v} = refl
α◎!α {α = uniti⋆} {v} = refl
α◎!α {α = swap⋆} {v} = refl
α◎!α {α = assocl⋆} {v} = refl
α◎!α {α = assocr⋆} {v} = refl
α◎!α {α = distz} {(() , _)}
α◎!α {α = factorz} {()}
α◎!α {α = dist} {(inj₁ v₁ , v₂)} = refl
α◎!α {α = dist} {(inj₂ v₁ , v₂)} = refl
α◎!α {α = factor} {inj₁ v} = refl
α◎!α {α = factor} {inj₂ v} = refl
α◎!α {α = id⟷} {v} = refl
α◎!α {α = α₁ ◎ α₂} {v} =
  begin
    ap ((α₁ ◎ α₂) ◎ ! (α₁ ◎ α₂)) v
      ≡⟨ refl ⟩
    ap (! α₁) (ap (α₂ ◎ ! α₂) (ap α₁ v))
      ≡⟨ cong (λ v' → ap (! α₁) v') (α◎!α {α = α₂} {v = ap α₁ v}) ⟩
    ap (! α₁) (ap α₁ v)
      ≡⟨ α◎!α {α = α₁} {v = v} ⟩
    v ∎
α◎!α {α = α₁ ⊕ α₂} {inj₁ v} =
  begin
    ap ((α₁ ⊕ α₂) ◎ ! (α₁ ⊕ α₂)) (inj₁ v)
      ≡⟨ refl ⟩
    inj₁ (ap (! α₁) (ap α₁ v))
      ≡⟨ cong inj₁ (α◎!α {α = α₁} {v}) ⟩
    inj₁ v ∎
α◎!α {α = α₁ ⊕ α₂} {inj₂ v} =
  begin
    ap ((α₁ ⊕ α₂) ◎ ! (α₁ ⊕ α₂)) (inj₂ v)
      ≡⟨ refl ⟩
    inj₂ (ap (! α₂) (ap α₂ v))
      ≡⟨ cong inj₂ (α◎!α {α = α₂} {v}) ⟩
    inj₂ v ∎
α◎!α {α = α₁ ⊗ α₂} {(v₁ , v₂)} =
  begin
    ap ((α₁ ⊗ α₂) ◎ ! (α₁ ⊗ α₂)) (v₁ , v₂)
      ≡⟨ refl ⟩
    (ap (! α₁) (ap α₁ v₁) , ap (! α₂) (ap α₂ v₂))
      ≡⟨ cong₂ (_,_) (α◎!α {α = α₁} {v = v₁}) (α◎!α {α = α₂} {v = v₂}) ⟩
    (v₁ , v₂) ∎

!α◎α : {t₁ t₂ : U} {α : t₁ ⟷ t₂} {v : ⟦ t₂ ⟧} → ap (! α ◎ α) v ≡ v
!α◎α {α = unite₊} {v} = refl
!α◎α {α = uniti₊} {inj₁ ()}
!α◎α {α = uniti₊} {inj₂ v} = refl
!α◎α {α = swap₊} {inj₁ v} = refl
!α◎α {α = swap₊} {inj₂ v} = refl
!α◎α {α = assocl₊} {inj₁ (inj₁ v)} = refl
!α◎α {α = assocl₊} {inj₁ (inj₂ v)} = refl
!α◎α {α = assocl₊} {inj₂ v} = refl
!α◎α {α = assocr₊} {inj₁ v} = refl
!α◎α {α = assocr₊} {inj₂ (inj₁ v)} = refl
!α◎α {α = assocr₊} {inj₂ (inj₂ v)} = refl
!α◎α {α = unite⋆} {v} = refl
!α◎α {α = uniti⋆} {v} = refl
!α◎α {α = swap⋆} {v} = refl
!α◎α {α = assocl⋆} {v} = refl
!α◎α {α = assocr⋆} {v} = refl
!α◎α {α = distz} {()}
!α◎α {α = factorz} {(() , _)}
!α◎α {α = dist} {inj₁ v} = refl
!α◎α {α = dist} {inj₂ v} = refl
!α◎α {α = factor} {(inj₁ v₁ , v₂)} = refl
!α◎α {α = factor} {(inj₂ v₁ , v₂)} = refl
!α◎α {α = id⟷} {v} = refl
!α◎α {α = α₁ ◎ α₂} {v} =
  begin
    ap (! (α₁ ◎ α₂) ◎ (α₁ ◎ α₂)) v
      ≡⟨ refl ⟩
    ap α₂ (ap (! α₁ ◎ α₁) (ap (! α₂) v))
      ≡⟨ cong (λ v' → ap α₂ v') (!α◎α {α = α₁} {v = ap (! α₂) v}) ⟩
    ap α₂ (ap (! α₂) v)
      ≡⟨ !α◎α {α = α₂} {v = v} ⟩
    v ∎
!α◎α {α = α₁ ⊕ α₂} {inj₁ v} =
  begin
    ap (! (α₁ ⊕ α₂) ◎ (α₁ ⊕ α₂)) (inj₁ v)
      ≡⟨ refl ⟩
    inj₁ (ap α₁ (ap (! α₁) v))
      ≡⟨ cong inj₁ (!α◎α {α = α₁} {v}) ⟩
    inj₁ v ∎
!α◎α {α = α₁ ⊕ α₂} {inj₂ v} =
  begin
    ap (! (α₁ ⊕ α₂) ◎ (α₁ ⊕ α₂)) (inj₂ v)
      ≡⟨ refl ⟩
    inj₂ (ap α₂ (ap (! α₂) v))
      ≡⟨ cong inj₂ (!α◎α {α = α₂} {v}) ⟩
    inj₂ v ∎
!α◎α {α = α₁ ⊗ α₂} {(v₁ , v₂)} =
  begin
    ap (! (α₁ ⊗ α₂) ◎ (α₁ ⊗ α₂)) (v₁ , v₂)
      ≡⟨ refl ⟩
    (ap α₁ (ap (! α₁) v₁) , ap α₂ (ap (! α₂) v₂))
      ≡⟨ cong₂ (_,_) (!α◎α {α = α₁} {v = v₁}) (!α◎α {α = α₂} {v = v₂}) ⟩
    (v₁ , v₂) ∎

-- Two permutations, viewed extensionally, are equivalent if they map
-- each value x to the same value. Generally we would only require
-- that the resulting values y and z have a path between them, but
-- because the internals of each type are discrete groupoids, this
-- reduces to saying that y and z are identical.

infix  10  _∼_

_∼_ : ∀ {t₁ t₂} → (p q : t₁ ⟷ t₂) → Set
_∼_ {t₁} {t₂} p q = (x : ⟦ t₁ ⟧) → ap p x ≡ ap q x

α◎!α∼id⟷ : {t₁ t₂ : U} {α : t₁ ⟷ t₂} → α ◎ ! α ∼ id⟷
α◎!α∼id⟷ {α = α} v = α◎!α {α = α} {v}

!α◎α∼id⟷ : {t₁ t₂ : U} {α : t₁ ⟷ t₂} → ! α ◎ α ∼ id⟷
!α◎α∼id⟷ {t₁} {t₂} {α} v = !α◎α {α = α} {v}

resp◎ : {t₁ t₂ t₃ : U} {p q : t₁ ⟷ t₂} {r s : t₂ ⟷ t₃} →
        (α : p ∼ q) → (β : r ∼ s) → (p ◎ r) ∼ (q ◎ s)
resp◎ {t₁} {t₂} {t₃} {p} {q} {r} {s} α β v =
  begin
    ap (p ◎ r) v
      ≡⟨ refl ⟩
    ap r (ap p v)
      ≡⟨ cong (λ v → ap r v) (α v) ⟩
    ap r (ap q v)
      ≡⟨ β (ap q v) ⟩
    ap (q ◎ s) v ∎

-- Because we representing combinators semantically as functions (not as
-- permutations), we have to use function extensionality to compare the
-- semantic representation. This need to be changed by making use of a proper
-- representation of permutations instead of plain functions.

postulate
  funExtP : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) → (f ≡ g)

-- Two extensionally equivalent combinators are semantically
-- equivalent. Again, if we had a proper representation of permutations, this
-- would reduce to comparing the two representations without involving
-- function extensionality.

ext2id : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ∼ c₂) → ap c₁ ≡ ap c₂
ext2id {t₁} {t₂} {c₁} {c₂} c₁∼c₂ =
  funExtP {⟦ t₁ ⟧} {⟦ t₂ ⟧} {ap c₁} {ap c₂} c₁∼c₂

-- The equivalence ∼ of paths makes U a 1groupoid: the points are
-- types (t : U); the 1paths are ⟷; and the 2paths between them are
-- based on extensional equivalence ∼

G : 1Groupoid
G = record
        { set = U
        ; _↝_ = _⟷_
        ; _≈_ = _∼_
        ; id  = id⟷
        ; _∘_ = λ p q → q ◎ p
        ; _⁻¹ = !
        ; lneutr = λ _ _ → refl
        ; rneutr = λ _ _ → refl
        ; assoc  = λ _ _ _ _ → refl
        ; equiv = record {
            refl  = λ _ → refl
          ; sym   = λ α x → sym (α x)
          ; trans = λ α β x → trans (α x) (β x)
          }
        ; linv = λ {t₁} {t₂} α → α◎!α∼id⟷ {t₁} {t₂} {α}
        ; rinv = λ {t₁} {t₂} α → !α◎α∼id⟷ {t₁} {t₂} {α}
        ; ∘-resp-≈ = λ {t₁} {t₂} {t₃} {p} {q} {r} {s} p∼q r∼s →
                    resp◎ {t₁} {t₂} {t₃} {r} {s} {p} {q} r∼s p∼q
        }

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

-- Simplification rules

infix  30 _⇔_

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

-- better syntax for writing 2paths

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

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

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

-- Inverses for 2paths

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

-- a nice example of 2 paths

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

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

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

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

postulate -- to do eventually but should be fairly easy
  soundnessP : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ⇔ c₂) → (c₁ ∼ c₂)

-- postulate -- proved below
--  completenessP : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} → (c₁ ∼ c₂) → (c₁ ⇔ c₂)

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

postulate
  invertP : {t₁ t₂ : U} → (⟦ t₁ ⟧ → ⟦ t₂ ⟧) → (t₁ ⟷ t₂)

canonical : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂)
canonical c = invertP (ap c)

-- Note that if c₁ ⇔ c₂, then by soundness c₁ ∼ c₂ and hence their
-- canonical representatives are identical.

canonicalWellDefined : {t₁ t₂ : U} {c₁ c₂ : t₁ ⟷ t₂} →
  (c₁ ⇔ c₂) → (canonical c₁ ≡ canonical c₂)
canonicalWellDefined {t₁} {t₂} {c₁} {c₂} α =
  cong invertP (ext2id {t₁} {t₂} {c₁} {c₂} (soundnessP α))

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

postulate
  inversionP : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ canonical c

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

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

-- To summarize, completeness can be proved if we can define the following
-- two functions:
--
-- * a function that extracts a canonical combinator out of the
--   semantic representation of a permutation:
--     invertP : {t₁ t₂ : U} → (⟦ t₁ ⟧ → ⟦ t₂ ⟧) → (t₁ ⟷ t₂)
-- * a function that proves that every combinator can be rewritten to this
--   canonical form:
--    inversionP : {t₁ t₂ : U} {c : t₁ ⟷ t₂} → c ⇔ canonical c
--
-- This all uses function extensionality. It is possible to get rid of
-- that if we use an accurate representation of permutations.

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import Prelude hiding (_<_)

module Implicits.Resolution.GenericFinite.Resolution where

open import Coinduction
open import Data.List
open import Data.List.Any
open Membership-≡
open import Data.Fin.Substitution
open import Relation.Binary using (Rel)

open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas.MetaType
open import Implicits.Resolution.Termination
open import Implicits.Resolution.GenericFinite.TerminationCondition

private
  module M = MetaTypeMetaSubst

module ResolutionRules (cond : TerminationCondition) where
  open TerminationCondition cond

  mutual
    data _,_⊢_↓_ {ν} (Δ : ICtx ν) : (Φ : TCtx) → Type ν → SimpleType ν → Set where
      i-simp : ∀ {Φ} a → Δ , Φ ⊢ simpl a ↓ a
      i-iabs : ∀ {Φ ρ₁ ρ₂ a} → let Φ' = (step Φ Δ ρ₁ ρ₂ a) in
               Φ' < Φ → Δ , Φ' ⊢ᵣ ρ₁ → Δ , Φ ⊢ ρ₂ ↓ a → Δ , Φ ⊢ ρ₁ ⇒ ρ₂ ↓ a
      i-tabs : ∀ {Φ ρ a} b → Δ , Φ ⊢ ρ tp[/tp b ] ↓ a → Δ , Φ ⊢ ∀' ρ ↓ a

    data _,_⊢ᵣ_ {ν} (Δ : ICtx ν) : TCtx → Type ν → Set where
      r-simp : ∀ {Φ r τ} → r ∈ Δ → Δ , Φ ⊢ r ↓ τ → Δ , Φ ⊢ᵣ simpl τ
      r-iabs : ∀ {Φ} ρ₁ {ρ₂} → ((ρ₁ ∷ Δ) , Φ ⊢ᵣ ρ₂) → Δ , Φ ⊢ᵣ (ρ₁ ⇒ ρ₂)
      r-tabs : ∀ {Φ ρ} → ictx-weaken Δ , Φ ⊢ᵣ ρ → Δ , Φ ⊢ᵣ ∀' ρ


text:
module Haskell.Prim.Bounded where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Char
open import Agda.Builtin.Equality
open import Agda.Builtin.List

open import Haskell.Prim
open import Haskell.Prim.Eq
open import Haskell.Prim.Int
open import Haskell.Prim.Maybe
open import Haskell.Prim.Ord
open import Haskell.Prim.Tuple
open import Haskell.Prim.Word

--------------------------------------------------
-- Bounded

record BoundedBelow (a : Set) : Set where
  field
    minBound : a

record BoundedAbove (a : Set) : Set where
  field
    maxBound : a

record Bounded (a : Set) : Set where
  field
    overlap ⦃ below ⦄ : BoundedBelow a
    overlap ⦃ above ⦄ : BoundedAbove a

open BoundedBelow ⦃ ... ⦄ public
open BoundedAbove ⦃ ... ⦄ public

instance
  iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a
  iBounded .Bounded.below = it
  iBounded .Bounded.above = it

instance
  iBoundedBelowNatural : BoundedBelow Nat
  iBoundedBelowNatural .minBound = 0

  iBoundedBelowWord : BoundedBelow Word
  iBoundedBelowWord .minBound = 0
  iBoundedAboveWord : BoundedAbove Word
  iBoundedAboveWord .maxBound = 18446744073709551615

  iBoundedBelowInt : BoundedBelow Int
  iBoundedBelowInt .minBound = -9223372036854775808
  iBoundedAboveInt : BoundedAbove Int
  iBoundedAboveInt .maxBound = 9223372036854775807

  iBoundedBelowBool : BoundedBelow Bool
  iBoundedBelowBool .minBound = false
  iBoundedAboveBool : BoundedAbove Bool
  iBoundedAboveBool .maxBound = true

  iBoundedBelowChar : BoundedBelow Char
  iBoundedBelowChar .minBound = '\0'
  iBoundedAboveChar : BoundedAbove Char
  iBoundedAboveChar .maxBound = '\1114111'

  iBoundedBelowTuple₀ : BoundedBelow (Tuple [])
  iBoundedBelowTuple₀ .minBound = []
  iBoundedAboveTuple₀ : BoundedAbove (Tuple [])
  iBoundedAboveTuple₀ .maxBound = []

  iBoundedBelowTuple : ∀ {as} → ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow (Tuple as) ⦄ → BoundedBelow (Tuple (a ∷ as))
  iBoundedBelowTuple .minBound = minBound ∷ minBound
  iBoundedAboveTuple : ∀ {as} → ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove (Tuple as) ⦄ → BoundedAbove (Tuple (a ∷ as))
  iBoundedAboveTuple .maxBound = maxBound ∷ maxBound

  iBoundedBelowOrdering : BoundedBelow Ordering
  iBoundedBelowOrdering .minBound = LT
  iBoundedAboveOrdering : BoundedAbove Ordering
  iBoundedAboveOrdering .maxBound = GT

-- Sanity checks

private
  _ : addWord maxBound 1 ≡ minBound
  _ = refl

  _ : addInt maxBound 1 ≡ minBound
  _ = refl


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

open import lib.Basics

module C1 {@♭ i₁ j₁ : ULevel}
          (@♭ I : Type i₁)
          (@♭ R : I → Type j₁)
          (@♭ r₀ : (index : I) → R index) where
  -- We assume the family R satisfies Axiom C0
  open import Axiom.C0 {i₁} {j₁} I R

  open import Basics
  open import Flat
  open import Sharp
  open import lib.types.Bool
  open import Bool

  open import lib.Equivalence2
  open import lib.types.Coproduct

  _is-discrete-C0 : {i : ULevel} (A : Type i) → Type _
  _is-discrete-C0 {i} A = (index : I) → (is-equiv {i = i} (λ (a : A) → (λ (r : R index) → a)))

  discrete-C0-eq : {i : ULevel} {A : Type i} (p : A is-discrete-C0) (index : I)
                   → A ≃ ((R index) → A)
  discrete-C0-eq p index = _ , (p index)

  prop-is-discrete-C0 : {i : ULevel} (P : PropT i) → (P holds) is-discrete-C0
  prop-is-discrete-C0 P =
    (λ index →
      is-eq to
            fro
            (λ f → λ= (λ r → prop-path (P holds-is-a-prop) (f (r₀ index)) (f r)))
            (λ p → prop-path (P holds-is-a-prop) (fro {index} (to p)) p))
      where
        to : {index : I} → P holds → (r : R index) → P holds
        to = λ p _ → p

        fro : {index : I} → ((r : R index) → P holds) → P holds
        fro {index} = λ f → f (r₀ index)

  crisp-prop-is-discrete : {@♭ i : ULevel} (@♭ P : PropT i) → (P holds) is-discrete
  crisp-prop-is-discrete P = C0 (P holds) (prop-is-discrete-C0 P)

  ⊥-is-discrete : ⊥ is-discrete
  ⊥-is-discrete = crisp-prop-is-discrete False

  -- Mapping into a C0 discrete gives a C0 discrete space.
  -- The argument is by swapping the order of application.
  Π-♭-C0 : {i j : ULevel} {A : Type i}
           {B : A → Type j} (p : (a : A) → (B a) is-discrete-C0)
           → ((a : A) → B a) is-discrete-C0
  Π-♭-C0 {A = A} {B = B} p =
    λ index → _ is-an-equivalence-because
      (fro index) is-inverse-by
        to-fro index and fro-to index
    where
      fro : (index : I) → ((R index) → (a : A) → B a) → (a : A) → B a
      fro index f a = (<– (discrete-C0-eq (p a) index)) (λ r → f r a)

      abstract
        to-fro : ∀ index f → (λ _ → fro index f) == f
        to-fro index f = -- We swap the order of r and a and use the discreteness of B a
          λ= $ λ r →
            λ= $ λ a →
              app= (lemma a) r
          where
            lemma : ∀ a → (λ _ → fro index f a) == (λ r → f r a)
            lemma a = <–-inv-r (discrete-C0-eq (p a) index) $ λ r → f r a

        fro-to : ∀ index f → (fro index (λ _ → f)) == f
        fro-to index f =
          λ= $ λ a →
            <–-inv-l (discrete-C0-eq (p a) index) $ f a

  -- Crisp propositions are codiscrete
  crisp-prop-is-codiscrete : {@♭ i : ULevel} (@♭ P : PropT i) → (P holds) is-codiscrete
  crisp-prop-is-codiscrete P =
    (P holds) is-codiscrete-because -- We give the map going the other way:
      ♯ (P holds) –⟨ map₁ ⟩→ ♭ (♯ (P holds)) –⟨ map₂ ⟩→ ♭ (P holds) –⟨ _↓♭ ⟩→ P holds →∎
        is-retract-by (λ _ → prop-path (snd P) _ _)
    where
      map₁ : ♯ (P holds) → ♭ (♯ (P holds))
      map₁ = <– (discrete-eq (crisp-prop-is-discrete (♯ₙ P)))

      map₂ : ♭ (♯ (P holds)) → ♭ (P holds)
      map₂ = –> ♭♯-eq

  ¬-is-codiscrete : ∀ {i} (A : Type i) → (¬ A) is-codiscrete
  ¬-is-codiscrete {i} A = -- mapping into a codiscrete is codiscrete.
    replete (Π-codisc {A = A} (λ _ → ⊥)) (lemma₁ ⁻¹)
    where
      lemma₁ : (A → ⊥) ≃ (A → ♯ ⊥)-- ⊥ is codiscrete b/c it is crisp.
      lemma₁ = post∘-equiv (codisc-eq (crisp-prop-is-codiscrete False))

      open import lib.types.Modality
      replete = (Modality.local-is-replete {i}) ♯-modality

  ♭-commutes-with-¬ : {@♭ i : ULevel} {@♭ A : Type i} → ♭ (¬ A) ≃ ¬ (♭ A)
  ♭-commutes-with-¬ {i = i} {A = A} =
                    ♭ (¬ A)
                  ≃⟨ ♭→e {A = ¬ A} {B = A → ♯ ⊥} lemma₁ ⟩
                    ♭ (A → ♯ ⊥)
                  ≃⟨ ♭♯-adjoint ⁻¹ ⟩
                     ♭ (¬ (♭ A))
                  ≃⟨ discrete-eq (crisp-prop-is-discrete (¬ (♭ A) , proof)) ⟩
                     ¬ (♭ A)
                  ≃∎
    where
      lemma₁ : (A → ⊥) ≃ (A → ♯ ⊥)-- ⊥ is codiscrete b/c it is crisp.
      lemma₁ = post∘-equiv (codisc-eq (crisp-prop-is-codiscrete False))

      proof : ¬ (♭ A) is-a-prop
      proof = mapping-into-prop-is-a-prop (λ _ → False holds-is-a-prop)

  -- Hereafter, we use LEM
  open import LEM
  open import NotNot

  module _ {@♭ i : ULevel} where
    record Γ : Type (lsucc i) where
      constructor ctx
      field
        ᶜP : PropT i
        ᶜnnp : ¬¬ (ᶜP holds) holds
    open Γ

    ♯-prop-is-¬¬ : (P : PropT i) → ((♯ₙ P) holds) ≃ ((¬¬ (P holds)) holds)
    ♯-prop-is-¬¬ P =
      iff-to-≃ {P = ♯ₙ P} {Q = ¬¬ (P holds)}
        -- ⇒
        (♯ₙ P holds
          –⟨ (λ a → let♯ u ^♯:= a in♯ ((continue u) ^♯)) ⟩→
        ♯ₙ (¬¬ (P holds)) holds
          –⟨ un♯ (¬-is-codiscrete (¬ (P holds))) ⟩→
        ¬¬ (P holds) holds
          →∎)
      -- ⇐
        (λ nnp → {!let♯ γ ::= (ctx P nnp) in♯ (helper (ᶜP γ) (ᶜnnp γ)) ^^♯-in-family (λ (@♭ γ : Γ) → (ᶜP γ) holds) !})
      where
        helper : (@♭ P : PropT i) → ((¬¬ (P holds)) holds) ::→ (P holds)
        helper P nnp = (un¬¬-crisp {P = P} nnp)

max_stars_repo_name: glangmead/formalization

max_issues_repo_name: glangmead/formalization

max_forks_repo_name: glangmead/formalization


text:
-- this is so this can be imported even though it has unresolved holes
{-# OPTIONS --allow-unsolved-metas #-}

module v01-01-basics where

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

data day : Set where
 mon : day
 tue : day
 wed : day
 thu : day
 fri : day
 sat : day
 sun : day

next-weekday : day → day
next-weekday mon = tue
next-weekday tue = wed
next-weekday wed = thu
next-weekday thu = fri
next-weekday fri = mon
next-weekday sat = mon
next-weekday sun = mon

_ : next-weekday fri ≡ mon
_ = refl

_ : next-weekday (next-weekday sat) ≡ tue
_ = refl

data bool : Set where
  true  : bool
  false : bool

negb : bool → bool
negb true  = false
negb false = true

andb : bool → bool → bool
andb  true b2 = b2
andb false  _ = false

orb : bool → bool → bool
orb  true  _ = true
orb false b2 = b2

_ : orb false false ≡ false
_ = refl
_ : orb false  true ≡ true
_ = refl
_ : orb  true false ≡ true
_ = refl
_ : orb  true  true ≡ true
_ = refl

nandb : bool → bool → bool
nandb true true = false
nandb    _    _ = true

_ : nandb false false ≡ true
_ = refl
_ : nandb false  true ≡ true
_ = refl
_ : nandb  true false ≡ true
_ = refl
_ : nandb  true  true ≡ false
_ = refl

andb3 : bool → bool → bool → bool
andb3 true true true = true
andb3    _    _    _ = false

_ : andb3  true  true  true ≡ true
_ = refl
_ : andb3 false  true  true ≡ false
_ = refl
_ : andb3  true false  true ≡ false
_ = refl
_ : andb3  true  true false ≡ false
_ = refl

data rgb : Set where
  red   : rgb
  green : rgb
  blue  : rgb

data color : Set where
  black   : color
  white   : color
  primary : rgb → color

monochrome : color → bool
monochrome black = true
monochrome white = true
monochrome (primary _) = false

isred : color → bool
isred (primary red) = true
isred            _  = false

data bit : Set where
  B0 : bit
  B1 : bit

data nybble : Set where
  bits : (b0 b1 b2 b3 : bit) → nybble

all-zero : nybble → bool
all-zero (bits B0 B0 B0 B0) = true
all-zero                 _  = false

_ : all-zero (bits B1 B0 B1 B0) ≡ false
_ = refl
_ : all-zero (bits B0 B0 B0 B0) ≡ true
_ = refl

data nat : Set where
  O : nat
  S : nat → nat

pred : nat → nat
pred    O  = O
pred (S n) = n

{-# BUILTIN NATURAL nat #-}

_ : S (S (S (S O))) ≡ 4
_ = refl

minustwo : nat → nat
minustwo       O   = O
minustwo    (S O)  = O
minustwo (S (S n)) = n

_ : minustwo 4 ≡ 2
_ = refl

evenb : nat → bool
evenb       O   = true
evenb    (S O)  = false
evenb (S (S n)) = evenb n

oddb : nat → bool
oddb n = negb (evenb n)

_ : oddb 1 ≡ true
_ = refl
_ : oddb 4 ≡ false
_ = refl

plus : nat → nat → nat
plus    O  m = m
plus (S n) m = S (plus n m)

_ : plus 3 2 ≡ 5
_ = refl

mult : nat → nat → nat
mult    O  m = 0
mult (S n) m = plus m (mult n m)

_ : mult 3 3 ≡ 9
_ = refl

minus : nat → nat → nat
minus    O     _  = O
minus    x     O  = x
minus (S n) (S m) = minus n m

exp : (base power : nat) → nat
exp _    O  = S O
exp b (S p) = mult b (exp b p)

_ : exp 2 0 ≡ 1
_ = refl
_ : exp 2 1 ≡ 2
_ = refl
_ : exp 2 2 ≡ 4
_ = refl
_ : exp 2 3 ≡ 8
_ = refl

factorial : nat → nat
factorial    O  = 1
factorial (S n) = mult (S n) (factorial n)

_ : factorial 3 ≡ 6
_ = refl
_ : factorial 5 ≡ mult 10 12
_ = refl

_+_ : nat → nat → nat
_+_ = plus

_-_ : nat → nat → nat
_-_ = minus

_*_ : nat → nat → nat
_*_ = mult

infixl 6  _+_  _-_
infixl 7  _*_
{-# BUILTIN NATPLUS  _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _-_ #-}

eqb : (n m : nat) → bool
eqb    O     O  = true
eqb    O  (S _) = false
eqb (S _)    O  = false
eqb (S l) (S r) = eqb l r

leb : (n m : nat) → bool
leb    O     _  = true
leb (S n)    O  = false
leb (S n) (S m) = leb n m

_ : leb 2 2 ≡ true
_ = refl
_ : leb 2 4 ≡ true
_ = refl
_ : leb 4 2 ≡ false
_ = refl

_=?_ : (n m : nat) → bool
_=?_ = eqb

_<=?_ : (n m : nat) → bool
_<=?_ = leb

infix 4 _=?_
infix 4 _<=?_

_ : (4 <=? 2) ≡ false
_ = refl

ltb : (n m : nat) → bool
ltb    O     O  = false
ltb    O  (S m) = true
ltb (S n)    O  = false
ltb (S n) (S m) = ltb n m

_<?_ : (n m : nat) → bool
_<?_ = ltb
infix 4 _<?_

_ : ltb 2 2 ≡ false
_ = refl
_ : ltb 2 4 ≡ true
_ = refl
_ : ltb 4 2 ≡ false
_ = refl

-- proof by simplification

plus-O-n : ∀ {n : nat} → 0 + n ≡ n
plus-O-n = refl

plus-1-l : ∀ {n : nat} → 1 + n ≡ S n
plus-1-l = refl

mult-O-l : ∀ {n : nat} → 0 * n ≡ 0
mult-O-l = refl

-- proof by rewriting

plus-id-example : ∀ {n m : nat}
  →     n ≡ m
  → n + n ≡ m + m
plus-id-example n≡m rewrite n≡m = refl

plus_id_exercise : ∀ {n m o : nat}
  → n     ≡ m
  →     m ≡     o
  → n + m ≡ m + o
plus_id_exercise n≡m m≡o rewrite n≡m | m≡o = refl

*0 : ∀ (m : nat) → m * 0 ≡ 0
*0    0  = refl
*0 (S m) = *0 m

mult-n-O : ∀ (n : nat) → 0 ≡ n * 0
mult-n-O n rewrite *0 n = refl

*1 : ∀ (n : nat) → n * 1 ≡ n
*1    0 = refl
*1 (S n) rewrite *1 n = refl

1* : ∀ (n : nat) → 1 * n ≡ n
1*    0 = refl
1* (S n) rewrite 1* n = refl

mult-n-Sm : ∀ (n m : nat) → n * m + n ≡ n * S m
mult-n-Sm    O     m  = refl
mult-n-Sm    n     O  rewrite *0 n | plus-O-n {n} | *1 n = refl
mult-n-Sm (S n) (S m) = {!!} -- TODO

mult-n-0-m-0 : ∀ (p q : nat)
  → (p * 0) + (q * 0) ≡ 0
mult-n-0-m-0 p q rewrite *0 p | *0 q = refl

mult-n-1 : ∀ (p : nat) → p * 1 ≡ p
mult-n-1 = *1

-- proof by case analysis

plus-1-neq-0 : ∀ (n : nat) → ((n + 1) =? 0) ≡ false
plus-1-neq-0    O  = refl
plus-1-neq-0 (S n) rewrite plus-1-neq-0 n = refl

negb-involutive : ∀ (b : bool) → negb (negb b) ≡ b
negb-involutive true  = refl
negb-involutive false = refl

andb-commutative : ∀ (b c : bool) → andb b c ≡ andb c b
andb-commutative false false = refl
andb-commutative false  true = refl
andb-commutative  true false = refl
andb-commutative  true  true = refl

andb3-exchange : ∀ (b c d : bool) → andb (andb b c) d ≡ andb (andb b d) c
andb3-exchange  true  true  true = refl
andb3-exchange  true  true false = refl
andb3-exchange  true false  true = refl
andb3-exchange  true false false = refl
andb3-exchange false  true  true = refl
andb3-exchange false  true false = refl
andb3-exchange false false  true = refl
andb3-exchange false false false = refl

andb-true-elim2 : ∀ (b c : bool)
  → andb b c ≡ true
  →        c ≡ true
andb-true-elim2 false      _ ()
andb-true-elim2  true  false ()
andb-true-elim2  true   true _ = refl

zero-nbeq-plus-1 : ∀ (n : nat) → (0 =? (n + 1)) ≡ false
zero-nbeq-plus-1    O  = refl
zero-nbeq-plus-1 (S n) rewrite  zero-nbeq-plus-1 n = refl

identity-fn-applied-twice : ∀ {f : bool → bool} (b : bool)
  →    f b  ≡ b
  → f (f b) ≡ b
identity-fn-applied-twice b p rewrite p | p = refl

negation-fn-applied-twice : ∀ {f : bool → bool} {b : bool} -- TODO
  →    f b  ≡ negb b
  → f (f b) ≡ b
negation-fn-applied-twice {f} {false} p = {!!} -- TODO
negation-fn-applied-twice {f}  {true} p = {!!} -- TODO

andb-eq-orb : ∀ (b c : bool)
  → andb b c ≡ orb b c
  →      b   ≡       c
andb-eq-orb  true c p rewrite p = refl
andb-eq-orb false c p rewrite p = refl

-- NOTE: lowest order bit is on LEFT
data bin : Set where
  Z  : bin
  B₀ : bin → bin
  B₁ : bin → bin

incr : bin → bin
incr     Z  = B₁ Z
incr (B₀ x) = B₁ x
incr (B₁ x) = B₀ (incr x)

bin-to-nat : bin → nat
bin-to-nat     Z  = 0
bin-to-nat (B₀ x) =     2 * (bin-to-nat x)
bin-to-nat (B₁ x) = 1 + 2 * (bin-to-nat x)

_ :     (incr (B₁ Z))  ≡     B₀ (B₁ Z)
_ = refl
_ : (incr (B₀ (B₁ Z))) ≡     B₁ (B₁ Z)
_ = refl
_ : (incr (B₁ (B₁ Z))) ≡ B₀ (B₀ (B₁ Z))
_ = refl

_ : bin-to-nat         (B₀ (B₁ Z))  ≡ 2
_ = refl
_ : bin-to-nat       (incr (B₁ Z))  ≡ 1 + bin-to-nat (B₁ Z)
_ = refl
_ : bin-to-nat (incr (incr (B₁ Z))) ≡ 2 + bin-to-nat (B₁ Z)
_ = refl

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

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

macro
  tac : Term → TC ⊤
  tac hole = unify hole (def (quote id) (arg (arg-info visible relevant) (var 0 []) ∷ []))

test : {A : Set} → A → A
test x = {!tac!}

max_stars_repo_name: msuperdock/agda

max_issues_repo_name: msuperdock/agda

max_forks_repo_name: msuperdock/agda


text:
module bijection where

open import Level renaming ( zero to Zero ; suc to Suc )
open import Data.Nat
open import Data.Maybe
open import Data.List hiding ([_] ; sum )
open import Data.Nat.Properties
open import Relation.Nullary
open import Data.Empty
open import Data.Unit hiding ( _≤_ )
open import  Relation.Binary.Core hiding (_⇔_)
open import  Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality

open import logic
open import nat

-- record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m)  where
--    field
--        fun←  :  S → R
--        fun→  :  R → S
--        fiso← : (x : R)  → fun← ( fun→ x )  ≡ x
--        fiso→ : (x : S ) → fun→ ( fun← x )  ≡ x
--
-- injection :  {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
-- injection R S f = (x y : R) → f x ≡ f y → x ≡ y

open Bijection

bi-trans : {n m l : Level} (R : Set n) (S : Set m) (T : Set l)  → Bijection R S → Bijection S T → Bijection R T
bi-trans R S T rs st = record { fun← = λ x → fun← rs ( fun← st x ) ; fun→ = λ x → fun→ st ( fun→ rs x )
    ; fiso← = λ x →  trans (cong (λ k → fun← rs k) (fiso← st (fun→ rs x))) ( fiso← rs x)
    ; fiso→ = λ x →  trans (cong (λ k → fun→ st k) (fiso→ rs (fun← st x))) ( fiso→ st x) }

bid : {n : Level} (R : Set n)  → Bijection R R
bid {n} R = record {  fun← = λ x → x ; fun→  = λ x → x ; fiso← = λ _ → refl ;  fiso→ = λ _ → refl }

bi-sym : {n m : Level} (R : Set n) (S : Set m) → Bijection R S →  Bijection S R
bi-sym R S eq = record {  fun← =  fun→ eq ; fun→  = fun← eq  ; fiso← =  fiso→ eq ;  fiso→ =  fiso← eq }

open import Relation.Binary.Structures

bijIsEquivalence : {n : Level } → IsEquivalence  (Bijection {n} {n})
bijIsEquivalence = record { refl = λ {R} → bid R ; sym = λ {R} {S} → bi-sym R S ; trans = λ {R} {S} {T} → bi-trans R S T }

--  ¬ A = A → ⊥
--
-- famous diagnostic function
--

diag : {S : Set }  (b : Bijection  ( S → Bool ) S) → S → Bool
diag b n = not (fun← b n n)

diagonal : { S : Set } → ¬ Bijection  ( S → Bool ) S
diagonal {S} b = diagn1 (fun→ b (λ n → diag b n) ) refl where
    diagn1 : (n : S ) → ¬ (fun→ b (λ n → diag b n) ≡ n )
    diagn1 n dn = ¬t=f (diag b n ) ( begin
           not (diag b n)
        ≡⟨⟩
           not (not fun← b n n)
        ≡⟨ cong (λ k → not (k  n) ) (sym (fiso← b _)) ⟩
           not (fun← b (fun→ b (diag b))  n)
        ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
           not (fun← b n n)
        ≡⟨⟩
           diag b n
        ∎ ) where open ≡-Reasoning

b1 : (b : Bijection  ( ℕ → Bool ) ℕ) → ℕ
b1 b = fun→ b (diag b)

b-iso : (b : Bijection  ( ℕ → Bool ) ℕ) → fun← b (b1 b) ≡ (diag b)
b-iso b = fiso← b _

--
-- ℕ <=> ℕ + 1
--
to1 : {n : Level} {R : Set n} → Bijection ℕ R → Bijection ℕ (⊤ ∨ R )
to1 {n} {R} b = record {
       fun←  = to11
     ; fun→  = to12
     ; fiso← = to13
     ; fiso→ = to14
   } where
       to11 : ⊤ ∨ R → ℕ
       to11 (case1 tt) = 0
       to11 (case2 x) = suc ( fun← b x )
       to12 : ℕ → ⊤ ∨ R
       to12 zero = case1 tt
       to12 (suc n) = case2 ( fun→ b n)
       to13 : (x : ℕ) → to11 (to12 x) ≡ x
       to13 zero = refl
       to13 (suc x) = cong suc (fiso← b x)
       to14 : (x : ⊤ ∨ R) → to12 (to11 x) ≡ x
       to14 (case1 x) = refl
       to14 (case2 x) = cong case2 (fiso→ b x)

open _∧_

record NN ( i  : ℕ) (nxn→n :  ℕ →  ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where
  field
     j k sum stage : ℕ
     nn : j + k ≡ sum
     ni : i ≡ j + stage   -- not used
     k1 : nxn→n j k ≡ i
     k0 : n→nxn i ≡ ⟪ j , k ⟫
     nn-unique : {j0 k0 : ℕ } →  nxn→n j0 k0 ≡ i  → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫

i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
i≤0→i≡0 {0} z≤n = refl

nxn : Bijection ℕ (ℕ ∧ ℕ)
nxn = record {
     fun← = λ p → nxn→n (proj1 p) (proj2 p)
   ; fun→ =  n→nxn
   ; fiso← = n-id
   ; fiso→ = λ x → nn-id (proj1 x) (proj2 x)
  } where
     nxn→n :  ℕ →  ℕ → ℕ
     nxn→n zero zero = zero
     nxn→n zero (suc j) = j + suc (nxn→n zero j)
     nxn→n (suc i) zero = suc i + suc (nxn→n i zero)
     nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j))
     n→nxn : ℕ → ℕ ∧ ℕ
     n→nxn zero = ⟪ 0 , 0 ⟫
     n→nxn (suc i) with n→nxn i
     ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
     ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫

     nxn→n0 : { j k : ℕ } →  nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 )
     nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫
     nxn→n0 {zero} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (subst (λ k → 0 < k) (+-comm _ k) (s≤s z≤n)))
     nxn→n0 {(suc j)} {zero} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )
     nxn→n0 {(suc j)} {(suc k)} eq = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) )

     nid20 : (i : ℕ) →  i +  (nxn→n 0 i) ≡ nxn→n i 0
     nid20 zero = refl -- suc (i + (i + suc (nxn→n 0 i))) ≡ suc (i + suc (nxn→n i 0))
     nid20 (suc i) = begin
         suc (i + (i + suc (nxn→n 0 i)))  ≡⟨ cong (λ k → suc (i + k)) (sym (+-assoc i 1 (nxn→n 0 i))) ⟩
         suc (i + ((i + 1) + nxn→n 0 i))  ≡⟨ cong (λ k →  suc (i + (k + nxn→n 0 i))) (+-comm i 1)  ⟩
         suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i)  ⟩
         suc (i + suc (nxn→n i 0)) ∎  where open ≡-Reasoning

     nid4 : {i j : ℕ} →  i + 1 + j ≡ i + suc j
     nid4 {zero} {j} = refl
     nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
     nid5 : {i j k : ℕ} →  i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
     nid5 {zero} {j} {k} = begin
          suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
          1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
          (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
          suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
          suc j + suc (suc k) ∎ where open ≡-Reasoning
     nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )

     -- increment in ths same stage
     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
     nid2 zero zero = refl
     nid2 zero (suc j) = refl
     nid2 (suc i) zero = begin
          suc (nxn→n (suc i) 1)  ≡⟨ refl ⟩
          suc (suc (i + 1 + suc (nxn→n i 1)))  ≡⟨ cong (λ k → suc (suc k)) nid4  ⟩
          suc (suc (i + suc (suc (nxn→n i 1))))  ≡⟨ cong (λ k →  suc (suc (i + suc (suc k)))) (nid3 i) ⟩
          suc (suc (i + suc (suc (i + suc (nxn→n i 0)))))  ≡⟨ refl ⟩
          nxn→n (suc (suc i)) zero ∎ where
             open ≡-Reasoning
             nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
             nid3 zero = refl
             nid3 (suc i) = begin
                 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
                 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
                 suc (i + suc (suc (i + suc (nxn→n i 0)))) ∎
     nid2 (suc i) (suc j) = begin
          suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
          suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
          suc (suc (i + suc (suc j) + suc      (i + suc j + suc (nxn→n i (suc j)))))  ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
          suc (suc (i + suc j       + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
          nxn→n (suc (suc i)) (suc j) ∎ where
             open ≡-Reasoning

     -- increment ths stage
     nid00 : (i : ℕ) → suc (nxn→n i 0) ≡ nxn→n 0 (suc i)
     nid00 zero = refl
     nid00 (suc i) = begin
        suc (suc (i + suc (nxn→n i 0))) ≡⟨ cong (λ k → suc (suc (i + k ))) (nid00 i) ⟩
        suc (suc (i + (nxn→n 0 (suc i)))) ≡⟨ refl ⟩
        suc (suc (i + (i + suc (nxn→n 0 i))))  ≡⟨ cong suc (sym ( +-assoc 1 i (i + suc (nxn→n 0 i)))) ⟩
        suc ((1 + i) + (i + suc (nxn→n 0 i))) ≡⟨ cong (λ k → suc (k + (i + suc (nxn→n 0 i)))) (+-comm 1 i) ⟩
        suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩
        suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning

     -----
     --
     -- create the invariant NN for all n
     --
     nn : ( i  : ℕ) → NN i nxn→n n→nxn
     nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
        ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
     nn (suc i) with NN.k (nn i)  | inspect  NN.k (nn i)
     ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc  (NN.sum (nn i)) ; stage = suc  (NN.sum (nn i)) + (NN.stage (nn i))
         ; nn = refl
         ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ;  nn-unique = nn04 } where
            ---
            --- increment the stage
            ---
            sum = NN.sum (nn i)
            stage = NN.stage (nn i)
            j = NN.j (nn i)
            nn01 : suc i ≡ 0 + (suc sum + stage )
            nn01 = begin
               suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩
               suc ((NN.j  (nn i) ) + stage )  ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩
               suc ((NN.j  (nn i) + 0 ) + stage )  ≡⟨ cong (λ k → suc ((NN.j  (nn i) + k) + stage )) (sym eq) ⟩
               suc ((NN.j (nn i) + NN.k  (nn i)) + stage )  ≡⟨ cong (λ k → suc ( k + stage )) (NN.nn (nn i)) ⟩
               0 +   (suc sum + stage ) ∎  where open ≡-Reasoning
            nn02 :  nxn→n 0 (suc sum)  ≡ suc i
            nn02 = begin
               sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩
               (sum + 1) + nxn→n 0 sum  ≡⟨ cong (λ k → k + nxn→n 0 sum )  (+-comm sum 1 )⟩
               suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩
               suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NN.nn (nn i))) ⟩
               suc (nxn→n (NN.j (nn i) + (NN.k (nn i))  ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq)  ⟩
               suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩
               suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩
               suc i ∎  where open ≡-Reasoning
            nn03 :  n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫   -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫
            nn03 with n→nxn i | inspect  n→nxn i
            ... | ⟪ x , zero  ⟫ | record { eq = eq1 } = begin
                ⟪ zero , suc x ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩
                ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i)))  ⟩
                ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨  cong (λ k →  ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩
                ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨  cong (λ k →  ⟪ zero , suc (NN.j (nn i) + k)  ⟫ ) (sym eq)  ⟩
                ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k →  ⟪ zero , suc k ⟫ ) (NN.nn (nn i))  ⟩
                ⟪ 0 , suc sum  ⟫  ∎  where open ≡-Reasoning
            ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin
               suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩
               suc 0 ≤⟨ s≤s z≤n  ⟩
               suc y ≡⟨ sym (cong proj2 eq1) ⟩
               proj2 (n→nxn i)  ∎ ))  where open ≤-Reasoning
            --  nid2  : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j
            nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫
            nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i --
               nn07 : nxn→n k0 0 ≡ i
               nn07 = cong pred ( begin
                  suc ( nxn→n k0 0 ) ≡⟨ nid00 k0 ⟩
                  nxn→n 0 (suc k0 )  ≡⟨ eq1 ⟩
                  suc i  ∎ )  where open ≡-Reasoning
               nn08 : k0 ≡ sum
               nn08 = begin
                  k0  ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩
                  NN.j (nn i)  ≡⟨ +-comm 0 _ ⟩
                  NN.j (nn i) + 0  ≡⟨ cong (λ k →  NN.j (nn i) + k) (sym eq) ⟩
                  NN.j (nn i) + NN.k (nn i)  ≡⟨ NN.nn (nn i) ⟩
                  sum   ∎   where open ≡-Reasoning
            nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where
               nn05 : nxn→n j0 (suc k0) ≡ i
               nn05 = begin
                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin
                    suc (nxn→n j0 (suc k0))  ≡⟨ nid2 j0 k0 ⟩
                    nxn→n (suc j0) k0  ≡⟨ eq1 ⟩
                    suc i ∎ ) ⟩
                  i ∎   where open ≡-Reasoning
               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
               nn06 = NN.nn-unique (nn i)
     ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = nn10
         ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ;  nn-unique = nn13 } where
            ---
            --- increment in a stage
            ---
            nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i)
            nn10 = begin
                suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _)  ⟩
                (NN.j (nn i) + 1) + k ≡⟨  +-assoc (NN.j (nn i)) 1 k ⟩
                NN.j (nn i) + suc k  ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩
                NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩
                NN.sum (nn i)  ∎   where open ≡-Reasoning
            nn11 :  nxn→n (suc (NN.j (nn i))) k ≡ suc i --  nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i
            nn11 = begin
                nxn→n (suc (NN.j (nn i))) k   ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩
                suc (nxn→n (NN.j (nn i)) (suc k)) ≡⟨ cong (λ k →   suc (nxn→n (NN.j (nn i)) k)) (sym eq) ⟩
                suc (nxn→n ( NN.j (nn i)) (NN.k (nn i)))  ≡⟨ cong suc (NN.k1 (nn i)) ⟩
                suc i  ∎   where open ≡-Reasoning
            nn18 :  zero < NN.k (nn i)
            nn18 = subst (λ k → 0 < k ) ( begin
                    suc k ≡⟨ sym eq ⟩
                    NN.k (nn i)  ∎  ) (s≤s z≤n )  where open ≡-Reasoning
            nn12 :   n→nxn (suc i) ≡ ⟪ suc (NN.j (nn i)) , k ⟫  --  n→nxn i ≡ ⟪ NN.j (nn i) ,  NN.k (nn i)  ⟫
            nn12 with  n→nxn i | inspect  n→nxn i
            ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1))
                (subst (λ k → 0 < k ) ( begin
                    suc k ≡⟨ sym eq ⟩
                    NN.k (nn i) ≡⟨ cong proj2 (sym (NN.k0 (nn i)) ) ⟩
                    proj2 (n→nxn i) ∎  ) (s≤s z≤n )) ) where open ≡-Reasoning  --  eq1 n→nxn i ≡ ⟪ x , zero ⟫
            ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫
                ⟪ suc x , y ⟫ ≡⟨ refl ⟩
                ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
                   ⟪ x , suc y ⟫  ≡⟨ sym eq1 ⟩
                   n→nxn i ≡⟨ NN.k0 (nn i) ⟩
                   ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ )  ⟩
                ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k →  ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩
                ⟪ suc (NN.j (nn i)) , k ⟫ ∎   where open ≡-Reasoning
            nn13 :  {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ suc (NN.j (nn i)) , k ⟫ ≡ ⟪ j0 , k0 ⟫
            nn13 {zero} {suc k0} eq1 = ⊥-elim ( nat-≡< (sym (cong proj2 nn17)) nn18 ) where  -- (nxn→n zero (suc k0)) ≡ suc i
                nn16 : nxn→n k0 zero ≡ i
                nn16 =  cong pred ( subst (λ k → k ≡ suc i) (sym ( nid00 k0 )) eq1 )
                nn17 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ k0 , zero ⟫
                nn17 = NN.nn-unique (nn i) nn16
            nn13 {suc j0} {k0} eq1 = begin
               ⟪ suc (NN.j (nn i)) , pred (suc k) ⟫ ≡⟨ cong (λ k →  ⟪ suc (NN.j (nn i)) , pred k ⟫ ) (sym eq) ⟩
               ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin
                 ⟪ NN.j (nn i) , NN.k (nn i) ⟫  ≡⟨ nn15 ⟩
                 ⟪ j0 , suc k0 ⟫ ∎ ) ⟩
               ⟪ suc j0 , k0 ⟫ ∎  where -- nxn→n (suc j0) k0 ≡ suc i
                open ≡-Reasoning
                nn14 : nxn→n j0 (suc k0) ≡ i
                nn14 = cong pred ( subst (λ k → k ≡ suc i) (sym ( nid2 j0 k0 )) eq1 )
                nn15 : ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫
                nn15 = NN.nn-unique (nn i) nn14

     n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
     n-id i = subst (λ k →  nxn→n (proj1 k) (proj2 k)  ≡ i ) (sym (NN.k0 (nn i))) (NN.k1 (nn i))

     nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫
     nn-id j k = begin
          n→nxn (nxn→n j k)  ≡⟨ NN.k0 (nn (nxn→n j k))   ⟩
          ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩
          ⟪ j , k ⟫ ∎  where open ≡-Reasoning

--   []     0
--   0    → 1
--   1    → 2
--   01   → 3
--   11   → 4
--   ...

--
-- binary invariant
--
record LB (n : ℕ) (lton : List Bool → ℕ ) : Set where
  field
     nlist : List Bool
     isBin : lton nlist ≡ n
     isUnique :  (x : List Bool) → lton x ≡ n → nlist  ≡ x -- we don't need this

lb+1 : List Bool → List Bool
lb+1 [] =  false ∷ []
lb+1 (false ∷ t) = true ∷ t
lb+1 (true ∷ t) =  false ∷ lb+1 t

lb-1 : List Bool → List Bool
lb-1 [] =  []
lb-1 (true ∷ t) = false ∷ t
lb-1 (false ∷ t) with lb-1 t
... | [] = true ∷ []
... | x ∷ t1 = true ∷ x ∷ t1

LBℕ : Bijection ℕ ( List Bool )
LBℕ = record {
       fun←  = λ x → lton x
     ; fun→  = λ n → LB.nlist (lb n)
     ; fiso← = λ n → LB.isBin (lb n)
     ; fiso→ = λ x → LB.isUnique (lb (lton x)) x refl
   } where
     lton1 : List Bool → ℕ
     lton1 [] = 1
     lton1 (true ∷ t) = suc (lton1 t + lton1 t)
     lton1 (false ∷ t) = lton1 t + lton1 t
     lton : List Bool → ℕ
     lton x  = pred (lton1 x)

     lton1>0 : (x : List Bool ) → 0 < lton1 x
     lton1>0 [] = a<sa
     lton1>0 (true ∷ x₁) = 0<s
     lton1>0 (false ∷ t) = ≤-trans (lton1>0 t) x≤x+y

     2lton1>0 : (t : List Bool ) →  0 < lton1 t + lton1 t
     2lton1>0 t = ≤-trans (lton1>0 t) x≤x+y

     lb=3 : {x y : ℕ} → 0 < x → 0 < y → 1 ≤ pred (x + y)
     lb=3 {suc x} {suc y} (s≤s 0<x) (s≤s 0<y) = subst (λ k → 1 ≤ k ) (+-comm (suc y) _ ) (s≤s z≤n)

     lton-cons>0 : {x : Bool} {y : List Bool } → 0 < lton (x ∷ y)
     lton-cons>0 {true} {[]} = refl-≤s
     lton-cons>0 {true} {x ∷ y} = ≤-trans ( lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))) px≤x
     lton-cons>0 {false} {[]} = refl-≤
     lton-cons>0 {false} {x ∷ y} = lb=3 (lton1>0 (x ∷ y)) (lton1>0 (x ∷ y))

     lb=0 : {x y : ℕ } → pred x  < pred y → suc (x + x ∸ 1) < suc (y + y ∸ 1)
     lb=0 {0} {suc y} lt = s≤s (subst (λ k → 0 < k ) (+-comm (suc y) y ) 0<s)
     lb=0 {suc x} {suc y} lt = begin
            suc (suc ((suc x + suc x) ∸ 1)) ≡⟨ refl  ⟩
            suc (suc x) + suc x ≡⟨ refl ⟩
            suc (suc x + suc x) ≤⟨ <-plus (s≤s lt) ⟩
            suc y + suc x <⟨ <-plus-0 {suc x} {suc y} {suc y} (s≤s lt) ⟩
            suc y + suc y ≡⟨ refl ⟩
            suc ((suc y + suc y) ∸ 1) ∎  where open ≤-Reasoning
     lb=2 : {x y : ℕ } → pred x  < pred y → suc (x + x ) < suc (y + y )
     lb=2 {zero} {suc y} lt = s≤s 0<s
     lb=2 {suc x} {suc y} lt = s≤s (lb=0 {suc x} {suc y} lt)
     lb=1 : {x y : List Bool} {z : Bool} → lton (z ∷ x) ≡ lton (z ∷ y) → lton x ≡ lton y
     lb=1 {x} {y} {true} eq with <-cmp (lton x) (lton y)
     ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=2 {lton1 x} {lton1 y} a))
     ... | tri≈ ¬a b ¬c = b
     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=2 {lton1 y} {lton1 x} c))
     lb=1 {x} {y} {false} eq with <-cmp (lton x) (lton y)
     ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< (cong suc eq) (lb=0 {lton1 x} {lton1 y} a))
     ... | tri≈ ¬a b ¬c = b
     ... | tri> ¬a ¬b c = ⊥-elim (nat-≡< (cong suc (sym eq)) (lb=0 {lton1 y} {lton1 x} c))

     ---
     --- lton is unique in a head
     ---
     lb-tf : {x y : List Bool } → ¬ (lton (true ∷ x) ≡ lton (false ∷ y))
     lb-tf {x} {y} eq with <-cmp (lton1 x) (lton1 y)
     ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (lb=01 a)) where
        lb=01 : {x y : ℕ } → x  < y → x + x  < (y + y ∸ 1)
        lb=01 {x} {y} x<y = begin
            suc (x + x) ≡⟨ refl  ⟩
            suc x + x ≤⟨ ≤-plus x<y ⟩
            y + x ≡⟨ refl ⟩
            pred (suc y + x) ≡⟨ cong (λ k → pred ( k + x)) (+-comm 1 y) ⟩
            pred ((y + 1) + x ) ≡⟨ cong pred (+-assoc y 1 x)  ⟩
            pred (y + suc x) ≤⟨ px≤py (≤-plus-0 {suc x} {y} {y} x<y) ⟩
            (y + y) ∸ 1  ∎  where open ≤-Reasoning
     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (lb=02 c) ) where
        lb=02 : {x y : ℕ } → x  < y → x + x ∸ 1 < y + y
        lb=02 {0} {y} lt = ≤-trans lt x≤x+y
        lb=02 {suc x} {y} lt = begin
            suc ( suc x + suc x ∸ 1 ) ≡⟨ refl ⟩
            suc x + suc x  ≤⟨ ≤-plus {suc x} (<to≤ lt) ⟩
            y + suc x  ≤⟨ ≤-plus-0 (<to≤ lt) ⟩
            y + y  ∎  where open ≤-Reasoning
     ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< (sym eq) ( begin
            suc (lton1 y + lton1 y ∸ 1) ≡⟨ sucprd ( 2lton1>0 y) ⟩
            lton1 y + lton1 y  ≡⟨  cong (λ k → k + k ) (sym b)  ⟩
            lton1 x + lton1 x ∎  )) where open ≤-Reasoning

     ---
     --- lton uniqueness
     ---
     lb=b : (x y : List Bool) → lton x ≡ lton y → x ≡ y
     lb=b [] [] eq = refl
     lb=b [] (x ∷ y) eq = ⊥-elim ( nat-≡< eq (lton-cons>0 {x} {y} ))
     lb=b (x ∷ y) [] eq = ⊥-elim ( nat-≡< (sym eq) (lton-cons>0 {x} {y} ))
     lb=b (true ∷ x) (false ∷ y) eq = ⊥-elim ( lb-tf {x} {y} eq )
     lb=b (false ∷ x) (true ∷ y) eq = ⊥-elim ( lb-tf {y} {x} (sym eq) )
     lb=b (true ∷ x)  (true ∷ y)  eq = cong (λ k → true ∷ k  ) (lb=b x y (lb=1 {x} {y} {true}  eq))
     lb=b (false ∷ x) (false ∷ y) eq = cong (λ k → false ∷ k ) (lb=b x y (lb=1 {x} {y} {false} eq))

     lb : (n : ℕ) → LB n lton
     lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where
         lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x
         lb05 x eq = lb=b [] x (sym eq)
     lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n)
     ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where
         open ≡-Reasoning
         lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n
         lb10 = begin
           lton (false ∷ []) ≡⟨ refl ⟩
           suc 0  ≡⟨ refl ⟩
           suc (lton [])   ≡⟨ cong (λ k → suc (lton k)) (sym eq) ⟩
           suc (lton (LB.nlist (lb n)))  ≡⟨ cong suc (LB.isBin (lb n) ) ⟩
           suc n ∎
         lb06 :  (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x
         lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x
     ... | false ∷ t | record { eq = eq } =  record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where
        lb01 : lton (true ∷ t) ≡ suc n
        lb01 = begin
           lton (true ∷ t)  ≡⟨ refl ⟩
           lton1 t + lton1 t   ≡⟨ sym ( sucprd (2lton1>0 t) ) ⟩
           suc (pred (lton1 t + lton1 t ))  ≡⟨ refl ⟩
           suc (lton (false ∷ t))   ≡⟨ cong (λ k → suc (lton k )) (sym eq) ⟩
           suc (lton (LB.nlist (lb n))) ≡⟨  cong suc (LB.isBin (lb n)) ⟩
           suc n ∎  where open ≡-Reasoning
        lb09 :  (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x
        lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) --  lton (true ∷ t) ≡ lton x
     ... | true ∷ t | record { eq = eq } = record { nlist =  lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where
        lb03 : lton (true ∷ t) ≡ n
        lb03 = begin
           lton (true ∷ t)   ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩
           lton (LB.nlist (lb n)) ≡⟨ LB.isBin (lb n) ⟩
           n ∎  where open ≡-Reasoning

        add11 : (x1 : ℕ ) → suc x1 + suc x1 ≡ suc (suc  (x1 + x1))
        add11 zero = refl
        add11 (suc x) = cong (λ k → suc (suc k)) (trans (+-comm x _) (cong suc (+-comm _ x)))

        lb04 : (t : List Bool) →  suc (lton1 t) ≡ lton1 (lb+1 t)
        lb04 [] = refl
        lb04 (false ∷ t) = refl
        lb04 (true ∷ []) = refl
        lb04 (true ∷ t0 )  = begin
           suc (suc (lton1 t0 + lton1 t0)) ≡⟨ sym (add11 (lton1 t0)) ⟩
           suc (lton1 t0) + suc (lton1 t0) ≡⟨ cong (λ k → k + k ) (lb04 t0  ) ⟩
           lton1 (lb+1 t0) + lton1 (lb+1 t0) ∎  where
              open ≡-Reasoning

        lb02 : (t : List Bool) → lton t ≡ n → lton (lb+1 t) ≡ suc n
        lb02 [] refl = refl
        lb02 t eq1 = begin
            lton (lb+1 t) ≡⟨ refl ⟩
            pred (lton1 (lb+1 t)) ≡⟨ cong pred (sym (lb04 t)) ⟩
            pred (suc (lton1 t))  ≡⟨ sym (sucprd (lton1>0 t)) ⟩
            suc (pred (lton1 t)) ≡⟨ refl ⟩
            suc (lton t) ≡⟨ cong suc eq1  ⟩
            suc n ∎  where open ≡-Reasoning

        lb07 : (x : List Bool) → pred (lton1 x ) ≡ suc n → lb+1 (true ∷ t) ≡ x
        lb07 x eq1 = lb=b (lb+1 (true ∷ t)) x (trans ( lb02 (true ∷ t) lb03 ) (sym eq1))

max_stars_repo_name: shinji-kono/HyperReal-in-agda

max_issues_repo_name: shinji-kono/HyperReal-in-agda

max_forks_repo_name: shinji-kono/HyperReal-in-agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.TLevel

module experimental.Category where

record CategoryStructure {i j} (Obj : Type i)
  (Mor : Obj → Obj → Type j) : Type (lmax i j) where
  constructor category-structure
  field
    comp : {o₁ o₂ o₃ : Obj} → Mor o₁ o₂ → Mor o₂ o₃ → Mor o₁ o₃
    idm : {o : Obj} → Mor o o
    unit-r : ∀ {o₁ o₂} (m : Mor o₁ o₂) → comp m idm == m
    unit-l : ∀ {o₁ o₂} (m : Mor o₁ o₂) → comp idm m == m

record Category i j : Type (lsucc (lmax i j)) where
  constructor category
  field
    Obj : Type i
    Mor : Obj → Obj → Type j
    Mor-level : ∀ {o₁ o₂} → is-set (Mor o₁ o₂)
    cat-struct : CategoryStructure Obj Mor
  open CategoryStructure cat-struct public

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Definition.Typed.EqualityRelation

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

open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution
open import Definition.Untyped using (Con ; Term)

open import Tools.Nat
open import Tools.Product

private
  variable
    n : Nat
    Γ : Con Term n

-- Any level can be embedded into the highest level (validity variant).
maybeEmbᵛ : ∀ {l A}
            ([Γ] : ⊩ᵛ Γ)
          → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
          → Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]
maybeEmbᵛ {l = ⁰} [Γ] [A] ⊢Δ [σ] =
  let [σA]  = proj₁ ([A] ⊢Δ [σ])
      [σA]′ = maybeEmb (proj₁ ([A] ⊢Δ [σ]))
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] → irrelevanceEq [σA] [σA]′ (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]))
maybeEmbᵛ {l = ¹} [Γ] [A] = [A]

-- The lowest level can be embedded in any level (validity variant).
maybeEmbₛ′ : ∀ {l A}
             ([Γ] : ⊩ᵛ Γ)
           → Γ ⊩ᵛ⟨ ⁰ ⟩ A / [Γ]
           → Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
maybeEmbₛ′ {l = ⁰} [Γ] [A] = [A]
maybeEmbₛ′ {l = ¹} [Γ] [A] ⊢Δ [σ] =
  let [σA]  = proj₁ ([A] ⊢Δ [σ])
      [σA]′ = maybeEmb′ (proj₁ ([A] ⊢Δ [σ]))
  in  [σA]′
  ,   (λ [σ′] [σ≡σ′] → irrelevanceEq [σA] [σA]′ (proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]))

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt