text:
------------------------------------------------------------------------
-- A wrapper that turns a representation of natural numbers (with a
-- unique representative for every number) into a representation that
-- computes roughly like the unary natural numbers (at least for some
-- operations)
------------------------------------------------------------------------

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

import Bijection
open import Equality
import Erased.Without-box-cong
open import Prelude hiding (zero; suc; _+_; _*_; _^_)

module Nat.Wrapper
  {c⁺}
  (eq : ∀ {a p} → Equality-with-J a p c⁺)

  -- The underlying representation of natural numbers.
  (Nat′ : Type)
  -- A bijection between this representation and the unary natural
  -- numbers.
  (open Bijection eq using (_↔_))
  (Nat′↔ℕ : Nat′ ↔ ℕ)
  where

open Derived-definitions-and-properties eq

open import Dec
import Erased.Level-1 eq as E₁
import Erased.Stability eq as ES
open import Logical-equivalence using (_⇔_)

open import Erased.Without-box-cong eq
open import Function-universe eq as F hiding (_∘_)
open import H-level eq
open import H-level.Closure eq
open import List eq
open import List.All.Recursive eq
open import Vec eq as Vec

private

  module N where
    open import Nat eq public
    open Prelude public using (zero; suc; _+_; _*_; _^_)

  variable
    A               : Type
    f f′ m n n′ hyp : A

------------------------------------------------------------------------
-- The wrapper

private

  -- Converts from the underlying representation to unary natural
  -- numbers.

  to-ℕ : Nat′ → ℕ
  to-ℕ = _↔_.to Nat′↔ℕ

-- Natural numbers built on top of Nat′, indexed by corresponding
-- unary natural numbers.

Nat-[_] : @0 ℕ → Type
Nat-[ m ] = ∃ λ (n : Nat′) → Erased (to-ℕ n ≡ m)

-- A non-indexed variant of Nat-[_].

Nat : Type
Nat = ∃ λ (n : Erased ℕ) → Nat-[ erased n ]

-- Returns the (erased) index.

@0 ⌊_⌋ : Nat → ℕ
⌊ [ n ] , _ ⌋ = n

------------------------------------------------------------------------
-- Some conversion functions

-- Nat-[ n ] is isomorphic to the type of natural numbers equal
-- (with erased equality proofs) to n.

Nat-[]↔Σℕ : {@0 n : ℕ} → Nat-[ n ] ↔ ∃ λ m → Erased (m ≡ n)
Nat-[]↔Σℕ {n = n} =
  (∃ λ (m : Nat′) → Erased (to-ℕ m ≡ n))  ↝⟨ (Σ-cong Nat′↔ℕ λ _ → F.id) ⟩□
  (∃ λ m → Erased (m ≡ n))                □

-- Nat is logically equivalent to the type of unary natural numbers.

Nat⇔ℕ : Nat ⇔ ℕ
Nat⇔ℕ =
  Nat                                                   ↔⟨⟩
  (∃ λ (n : Erased ℕ) → Nat-[ erased n ])               ↔⟨ (∃-cong λ _ → Nat-[]↔Σℕ) ⟩
  (∃ λ (n : Erased ℕ) → ∃ λ m → Erased (m ≡ erased n))  ↝⟨ Σ-Erased-Erased-singleton⇔ ⟩□
  ℕ                                                     □

-- Converts from Nat to ℕ.

Nat→ℕ : Nat → ℕ
Nat→ℕ (_ , n′ , _) = to-ℕ n′

-- Nat→ℕ is definitionally equal to the forward direction of Nat⇔ℕ.

_ : Nat→ℕ ≡ _⇔_.to Nat⇔ℕ
_ = refl _

-- Converts from ℕ to Nat.

⌈_⌉ : ℕ → Nat
⌈_⌉ = _⇔_.from Nat⇔ℕ

-- The index matches the result of Nat→ℕ.

@0 ≡⌊⌋ : ∀ n → Nat→ℕ n ≡ ⌊ n ⌋
≡⌊⌋ ([ m ] , n , eq) =
  Nat→ℕ ([ m ] , n , eq)  ≡⟨⟩
  to-ℕ n                  ≡⟨ erased eq ⟩∎
  m                       ∎

------------------------------------------------------------------------
-- Some operations for Nat-[_]

-- A helper function that can be used to define constants.

nullary-[] :
  {@0 n : ℕ}
  (n′ : Nat′) →
  @0 to-ℕ n′ ≡ n →
  Nat-[ n ]
nullary-[] n′ hyp = n′ , [ hyp ]

-- A helper function that can be used to define unary operators.

unary-[] :
  {@0 n : ℕ} {@0 f : ℕ → ℕ}
  (f′ : Nat′ → Nat′) →
  @0 (∀ n → to-ℕ (f′ n) ≡ f (to-ℕ n)) →
  Nat-[ n ] → Nat-[ f n ]
unary-[] {n = n} {f = f} f′ hyp (n′ , p) =
    f′ n′
  , [ to-ℕ (f′ n′)  ≡⟨ hyp _ ⟩
      f (to-ℕ n′)   ≡⟨ cong f (erased p) ⟩∎
      f n           ∎
    ]

-- A helper function that can be used to define n-ary operators.

n-ary-[] :
  (n : ℕ)
  {@0 ms : Vec (Erased ℕ) n}
  (@0 f : Vec ℕ n → ℕ)
  (f′ : Vec Nat′ n → Nat′) →
  @0 (∀ ms → to-ℕ (f′ ms) ≡ f (Vec.map to-ℕ ms)) →
  All (λ m → Nat-[ erased m ]) (Vec.to-list ms) →
  Nat-[ f (Vec.map erased ms) ]
n-ary-[] N.zero _ f′ hyp _ =
  nullary-[] (f′ _) (hyp _)
n-ary-[] (N.suc n) {ms = ms} f f′ hyp ((m′ , p) , ms′) =
  n-ary-[]
    n
    (f ∘ (erased (Vec.head ms) ,_))
    (λ ms′ → f′ (m′ , ms′))
    (λ ms′ →
       to-ℕ (f′ (m′ , ms′))                         ≡⟨ hyp (m′ , ms′) ⟩
       f (to-ℕ m′              , Vec.map to-ℕ ms′)  ≡⟨ cong (λ x → f (x , _)) (erased p) ⟩∎
       f (erased (Vec.head ms) , Vec.map to-ℕ ms′)  ∎)
    ms′

-- The function n-ary-[] should be normalised by the compiler.

{-# STATIC n-ary-[] #-}

-- A helper function that can be used to define binary
-- operators.

binary-[] :
  {@0 m n : ℕ} {@0 f : ℕ → ℕ → ℕ}
  (f′ : Nat′ → Nat′ → Nat′) →
  @0 (∀ m n → to-ℕ (f′ m n) ≡ f (to-ℕ m) (to-ℕ n)) →
  Nat-[ m ] → Nat-[ n ] → Nat-[ f m n ]
binary-[] f′ hyp m n =
  n-ary-[]
    2
    _
    (λ (m , n , _) → f′ m n)
    (λ (m , n , _) → hyp m n)
    (m , n , _)

-- The code below is parametrised by implementations of (and
-- correctness properties for) certain operations for Nat′.

record Operations : Type where
  infixl 8 _*2^_
  infixr 8 _^_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≟_

  field
    zero      : Nat′
    to-ℕ-zero : to-ℕ zero ≡ N.zero

    suc       : Nat′ → Nat′
    to-ℕ-suc  : ∀ n → to-ℕ (suc n) ≡ N.suc (to-ℕ n)

    _+_       : Nat′ → Nat′ → Nat′
    to-ℕ-+    : ∀ m n → to-ℕ (m + n) ≡ to-ℕ m N.+ to-ℕ n

    _*_       : Nat′ → Nat′ → Nat′
    to-ℕ-*    : ∀ m n → to-ℕ (m * n) ≡ to-ℕ m N.* to-ℕ n

    _^_       : Nat′ → Nat′ → Nat′
    to-ℕ-^    : ∀ m n → to-ℕ (m ^ n) ≡ to-ℕ m N.^ to-ℕ n

    ⌊_/2⌋     : Nat′ → Nat′
    to-ℕ-⌊/2⌋ : ∀ n → to-ℕ ⌊ n /2⌋ ≡ N.⌊ to-ℕ n /2⌋

    ⌈_/2⌉     : Nat′ → Nat′
    to-ℕ-⌈/2⌉ : ∀ n → to-ℕ ⌈ n /2⌉ ≡ N.⌈ to-ℕ n /2⌉

    _*2^_     : Nat′ → ℕ → Nat′
    to-ℕ-*2^  : ∀ m n → to-ℕ (m *2^ n) ≡ to-ℕ m N.* 2 N.^ n

    _≟_       : ∀ m n → Dec (Erased (to-ℕ m ≡ to-ℕ n))

    from-bits      : List Bool → Nat′
    to-ℕ-from-bits :
      ∀ bs →
      to-ℕ (from-bits bs) ≡
      foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0 bs

    to-bits                : Nat′ → List Bool
    to-ℕ-from-bits-to-bits :
      ∀ n → to-ℕ (from-bits (to-bits n)) ≡ to-ℕ n

-- If certain operations are defined for Nat′, then they can be
-- defined for Nat-[_] as well.

module Operations-for-Nat-[] (o : Operations) where

  private

    module O = Operations o

  -- Zero.

  zero : Nat-[ N.zero ]
  zero = nullary-[] O.zero O.to-ℕ-zero

  -- The number's successor.

  suc : {@0 n : ℕ} → Nat-[ n ] → Nat-[ N.suc n ]
  suc = unary-[] O.suc O.to-ℕ-suc

  -- Addition.

  infixl 6 _+_

  _+_ : {@0 m n : ℕ} → Nat-[ m ] → Nat-[ n ] → Nat-[ m N.+ n ]
  _+_ = binary-[] O._+_ O.to-ℕ-+

  -- Multiplication.

  infixl 7 _*_

  _*_ : {@0 m n : ℕ} → Nat-[ m ] → Nat-[ n ] → Nat-[ m N.* n ]
  _*_ = binary-[] O._*_ O.to-ℕ-*

  -- Exponentiation.

  infixr 8 _^_

  _^_ : {@0 m n : ℕ} → Nat-[ m ] → Nat-[ n ] → Nat-[ m N.^ n ]
  _^_ = binary-[] O._^_ O.to-ℕ-^

  -- Division by two, rounded downwards.

  ⌊_/2⌋ : {@0 n : ℕ} → Nat-[ n ] → Nat-[ N.⌊ n /2⌋ ]
  ⌊_/2⌋ = unary-[] O.⌊_/2⌋ O.to-ℕ-⌊/2⌋

  -- Division by two, rounded upwards.

  ⌈_/2⌉ : {@0 n : ℕ} → Nat-[ n ] → Nat-[ N.⌈ n /2⌉ ]
  ⌈_/2⌉ = unary-[] O.⌈_/2⌉ O.to-ℕ-⌈/2⌉

  -- Left shift.

  infixl 8 _*2^_

  _*2^_ : {@0 m : ℕ} → Nat-[ m ] → ∀ n → Nat-[ m N.* 2 N.^ n ]
  m *2^ n = unary-[] (O._*2^ n) (flip O.to-ℕ-*2^ n) m

  -- Equality is decidable (in a certain sense).

  infix 4 _≟_

  _≟_ :
    {@0 m n : ℕ} →
    Nat-[ m ] → Nat-[ n ] →
    Dec (Erased (m ≡ n))
  _≟_ {m = m} {n = n} (m′ , [ m≡m′ ]) (n′ , [ n≡n′ ]) =
    Dec-map
      (Erased-cong-⇔ (
         to-ℕ m′ ≡ to-ℕ n′  ↝⟨ ≡⇒↝ _ (cong₂ _≡_ m≡m′ n≡n′) ⟩□
         m ≡ n              □))
      (m′ O.≟ n′)

  -- Conversion from bits. (The most significant bit comes first.)

  from-bits :
    (bs : List Bool) →
    Nat-[ foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0 bs ]
  from-bits bs = nullary-[] (O.from-bits bs) (O.to-ℕ-from-bits bs)

  -- Conversion to bits. (The most significant bit comes first.)

  to-bits :
    {@0 n : ℕ} →
    Nat-[ n ] →
    ∃ λ (bs : List Bool) →
      Erased (foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0 bs ≡ n)
  to-bits {n = n} (n′ , [ n′≡n ]) =
      O.to-bits n′
    , [ foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0
          (O.to-bits n′)                                    ≡⟨ sym $ O.to-ℕ-from-bits _ ⟩

        to-ℕ (O.from-bits (O.to-bits n′))                   ≡⟨ O.to-ℕ-from-bits-to-bits _ ⟩

        to-ℕ n′                                             ≡⟨ n′≡n ⟩∎

        n                                                   ∎
      ]

------------------------------------------------------------------------
-- Operations for Nat

private

  -- Equality is stable for the natural numbers.

  Stable-≡-ℕ : Stable-≡ ℕ
  Stable-≡-ℕ m n = Dec→Stable (m N.≟ n)

-- A helper function that can be used to define constants.

nullary :
  (@0 n : ℕ) (n′ : Nat′) →
  @0 to-ℕ n′ ≡ n →
  Nat
nullary n n′ hyp = [ n ] , nullary-[] n′ hyp

-- A first correctness result for nullary.
--
-- Note that this result holds by definition.

private

  @0 nullary-correct′ : ⌊ nullary n n′ hyp ⌋ ≡ n
  nullary-correct′ = refl _

-- A second correctness result for nullary.

nullary-correct :
  (@0 hyp : to-ℕ n′ ≡ n) →
  Nat→ℕ (nullary n n′ hyp) ≡ n
nullary-correct {n′ = n′} {n = n} hyp =
  Stable-≡-ℕ _ _
     [ Nat→ℕ (nullary n n′ hyp)  ≡⟨ ≡⌊⌋ (nullary n n′ hyp) ⟩
       ⌊ nullary n n′ hyp ⌋      ≡⟨⟩
       n                         ∎
     ]

-- A helper function that can be used to define unary operators.

unary :
  (@0 f : ℕ → ℕ) (f′ : Nat′ → Nat′) →
  @0 (∀ n → to-ℕ (f′ n) ≡ f (to-ℕ n)) →
  Nat → Nat
unary f f′ hyp ([ n ] , n′) = ([ f n ] , unary-[] f′ hyp n′)

-- A first correctness result for unary.
--
-- Note that this result holds by definition.

private

  @0 unary-correct′ : ⌊ unary f f′ hyp n ⌋ ≡ f ⌊ n ⌋
  unary-correct′ = refl _

-- A second correctness result for unary.

unary-correct :
  (f : ℕ → ℕ) (@0 hyp : ∀ n → to-ℕ (f′ n) ≡ f (to-ℕ n)) →
  ∀ n → Nat→ℕ (unary f f′ hyp n) ≡ f (Nat→ℕ n)
unary-correct {f′ = f′} f hyp n =
  Stable-≡-ℕ _ _
    [ Nat→ℕ (unary f f′ hyp n)  ≡⟨ ≡⌊⌋ (unary f f′ hyp n) ⟩
      ⌊ unary f f′ hyp n ⌋      ≡⟨⟩
      f ⌊ n ⌋                   ≡⟨ sym $ cong f $ ≡⌊⌋ n ⟩∎
      f (Nat→ℕ n)               ∎
    ]

-- A helper function that can be used to define n-ary operators.

n-ary :
  (n : ℕ)
  (@0 f : Vec ℕ n → ℕ)
  (f′ : Vec Nat′ n → Nat′) →
  @0 (∀ ms → to-ℕ (f′ ms) ≡ f (Vec.map to-ℕ ms)) →
  Vec Nat n → Nat
n-ary n f f′ hyp ms =
    [ f (Vec.map erased (proj₁ (_↔_.to Vec-Σ ms))) ]
  , n-ary-[] n f f′ hyp (proj₂ (_↔_.to Vec-Σ ms))

-- The function n-ary should be normalised by the compiler.

{-# STATIC n-ary #-}

-- The function n-ary is correct.

n-ary-correct :
  ∀ (n : ℕ) f {f′}
  (@0 hyp : ∀ ms → to-ℕ (f′ ms) ≡ f (Vec.map to-ℕ ms)) →
  ∀ ms →
  Nat→ℕ (n-ary n f f′ hyp ms) ≡ f (Vec.map (Nat→ℕ) ms)
n-ary-correct n f {f′ = f′} hyp ms =
  Stable-≡-ℕ _ _
    [ Nat→ℕ (n-ary n f f′ hyp ms)                   ≡⟨ ≡⌊⌋ (n-ary n f f′ hyp ms) ⟩
      ⌊ n-ary n f f′ hyp ms ⌋                       ≡⟨⟩
      f (Vec.map erased (proj₁ (_↔_.to Vec-Σ ms)))  ≡⟨ cong (f ∘ Vec.map _) proj₁-Vec-Σ ⟩
      f (Vec.map erased (Vec.map proj₁ ms))         ≡⟨ cong f $ sym Vec.map-∘ ⟩
      f (Vec.map ⌊_⌋ ms)                            ≡⟨ cong f $ sym $ Vec.map-cong ≡⌊⌋ ⟩∎
      f (Vec.map (Nat→ℕ) ms)                        ∎
    ]

-- A helper function that can be used to define binary operators

binary :
  (@0 f : ℕ → ℕ → ℕ) (f′ : Nat′ → Nat′ → Nat′) →
  @0 (∀ m n → to-ℕ (f′ m n) ≡ f (to-ℕ m) (to-ℕ n)) →
  Nat → Nat → Nat
binary f g hyp m n =
  n-ary
    2
    (λ (m , n , _) → f m n)
    (λ (m , n , _) → g m n)
    (λ (m , n , _) → hyp m n)
    (m , n , _)

-- A first correctness result for binary.
--
-- Note that this result holds by definition.

private

  @0 binary-correct′ : ⌊ binary f f′ hyp m n ⌋ ≡ f ⌊ m ⌋ ⌊ n ⌋
  binary-correct′ = refl _

-- A second correctness result for binary.

binary-correct :
  (f : ℕ → ℕ → ℕ)
  (@0 hyp : ∀ m n → to-ℕ (f′ m n) ≡ f (to-ℕ m) (to-ℕ n)) →
  ∀ m n →
  Nat→ℕ (binary f f′ hyp m n) ≡ f (Nat→ℕ m) (Nat→ℕ n)
binary-correct f hyp m n =
  n-ary-correct
    2
    (λ (m , n , _) → f m n)
    (λ (m , n , _) → hyp m n)
    (m , n , _)

-- If certain operations are defined for Nat′, then they can be
-- defined for Nat-[_] as well.

module Operations-for-Nat (o : Operations) where

  private

    module O    = Operations o
    module O-[] = Operations-for-Nat-[] o

  -- Zero.

  zero : Nat
  zero = nullary N.zero O.zero O.to-ℕ-zero

  to-ℕ-zero : Nat→ℕ zero ≡ N.zero
  to-ℕ-zero = nullary-correct O.to-ℕ-zero

  -- The number's successor.

  suc : Nat → Nat
  suc = unary N.suc O.suc O.to-ℕ-suc

  to-ℕ-suc : ∀ n → Nat→ℕ (suc n) ≡ N.suc (Nat→ℕ n)
  to-ℕ-suc = unary-correct N.suc O.to-ℕ-suc

  -- Addition.

  infixl 6 _+_

  _+_ : Nat → Nat → Nat
  _+_ = binary N._+_ O._+_ O.to-ℕ-+

  to-ℕ-+ : ∀ m n → Nat→ℕ (m + n) ≡ Nat→ℕ m N.+ Nat→ℕ n
  to-ℕ-+ = binary-correct N._+_ O.to-ℕ-+

  -- Multiplication.

  infixl 7 _*_

  _*_ : Nat → Nat → Nat
  _*_ = binary N._*_ O._*_ O.to-ℕ-*

  to-ℕ-* : ∀ m n → Nat→ℕ (m * n) ≡ Nat→ℕ m N.* Nat→ℕ n
  to-ℕ-* = binary-correct N._*_ O.to-ℕ-*

  -- Multiplication.

  infixr 8 _^_

  _^_ : Nat → Nat → Nat
  _^_ = binary N._^_ O._^_ O.to-ℕ-^

  to-ℕ-^ : ∀ m n → Nat→ℕ (m ^ n) ≡ Nat→ℕ m N.^ Nat→ℕ n
  to-ℕ-^ = binary-correct N._^_ O.to-ℕ-^

  -- Division by two, rounded downwards.

  ⌊_/2⌋ : Nat → Nat
  ⌊_/2⌋ = unary N.⌊_/2⌋ O.⌊_/2⌋ O.to-ℕ-⌊/2⌋

  to-ℕ-⌊/2⌋ : ∀ n → Nat→ℕ ⌊ n /2⌋ ≡ N.⌊ Nat→ℕ n /2⌋
  to-ℕ-⌊/2⌋ = unary-correct N.⌊_/2⌋ O.to-ℕ-⌊/2⌋

  -- Division by two, rounded upwards.

  ⌈_/2⌉ : Nat → Nat
  ⌈_/2⌉ = unary N.⌈_/2⌉ O.⌈_/2⌉ O.to-ℕ-⌈/2⌉

  to-ℕ-⌈/2⌉ : ∀ n → Nat→ℕ ⌈ n /2⌉ ≡ N.⌈ Nat→ℕ n /2⌉
  to-ℕ-⌈/2⌉ = unary-correct N.⌈_/2⌉ O.to-ℕ-⌈/2⌉

  -- Left shift.

  infixl 8 _*2^_

  _*2^_ : Nat → ℕ → Nat
  m *2^ n =
    unary (λ m → m N.* 2 N.^ n) (O._*2^ n) (flip O.to-ℕ-*2^ n) m

  to-ℕ-*2^ : ∀ m n → Nat→ℕ (m *2^ n) ≡ Nat→ℕ m N.* 2 N.^ n
  to-ℕ-*2^ m n =
    unary-correct (λ m → m N.* 2 N.^ n) (flip O.to-ℕ-*2^ n) m

  -- Equality is decidable (in a certain sense).

  infix 4 _≟_

  _≟_ : (m n : Nat) → Dec (Erased (⌊ m ⌋ ≡ ⌊ n ⌋))
  (_ , m′) ≟ (_ , n′) = m′ O-[].≟ n′

  -- Conversion from bits. (The most significant bit comes first.)

  from-bits : List Bool → Nat
  from-bits bs =
    nullary
      (foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0 bs)
      (O.from-bits bs)
      (O.to-ℕ-from-bits bs)

  to-ℕ-from-bits :
    ∀ bs →
    Nat→ℕ (from-bits bs) ≡
    foldl (λ n b → (if b then 1 else 0) N.+ 2 N.* n) 0 bs
  to-ℕ-from-bits bs = nullary-correct (O.to-ℕ-from-bits bs)

  -- Conversion to bits. (The most significant bit comes first.)

  to-bits : Nat → List Bool
  to-bits (_ , n′) = proj₁ (O-[].to-bits n′)

------------------------------------------------------------------------
-- Results that make use of an instantiation of the []-cong axioms

module []-cong (ax : []-cong-axiomatisation lzero) where

  open E₁.[]-cong₁ ax
  open E₁.Erased-cong ax ax
  open ES.[]-cong₁ ax
  open ES.[]-cong₂ ax ax

  ----------------------------------------------------------------------
  -- Some lemmas

  private

    -- Equality is very stable for the natural numbers.

    Very-stable-≡-ℕ : Very-stable-≡ ℕ
    Very-stable-≡-ℕ = Decidable-equality→Very-stable-≡ N._≟_

  -- Nat-[ n ] is a proposition.

  Nat-[]-propositional : {@0 n : ℕ} → Is-proposition Nat-[ n ]
  Nat-[]-propositional {n = n} =                                      $⟨ Very-stable-≡-ℕ ⟩
    Very-stable-≡ ℕ                                                   ↝⟨ Very-stable-congⁿ _ 1 (inverse Nat′↔ℕ) ⟩
    Very-stable-≡ Nat′                                                ↝⟨ Very-stable→Very-stableᴱ 1 ⟩
    Very-stableᴱ-≡ Nat′                                               ↝⟨ erased-singleton-with-erased-center-propositional ⟩
    Is-proposition (∃ λ (m : Nat′) → Erased (m ≡ _↔_.from Nat′↔ℕ n))  ↝⟨ (H-level-cong _ 1 $ ∃-cong λ _ → Erased-cong-↔ (inverse $
                                                                          from≡↔≡to (from-isomorphism $ inverse Nat′↔ℕ))) ⟩□
    Is-proposition (∃ λ (m : Nat′) → Erased (to-ℕ m ≡ n))             □

  -- There is a bijection between equality of two values of type Nat
  -- and erased equality of the corresponding unary natural number
  -- indices.

  ≡-for-indices↔≡ :
    {m n : Nat} →
    Erased (⌊ m ⌋ ≡ ⌊ n ⌋) ↔ m ≡ n
  ≡-for-indices↔≡ {m = m} {n = n} =
    Erased (⌊ m ⌋ ≡ ⌊ n ⌋)  ↝⟨ Erased-≡↔[]≡[] ⟩
    proj₁ m ≡ proj₁ n       ↝⟨ ignore-propositional-component Nat-[]-propositional ⟩□
    m ≡ n                   □

  ----------------------------------------------------------------------
  -- Another conversion function

  -- Nat is isomorphic to the type of unary natural numbers.

  Nat↔ℕ : Nat ↔ ℕ
  Nat↔ℕ =
    Nat                                                   ↔⟨⟩
    (∃ λ (n : Erased ℕ) → Nat-[ erased n ])               ↝⟨ (∃-cong λ _ → Nat-[]↔Σℕ) ⟩
    (∃ λ (n : Erased ℕ) → ∃ λ m → Erased (m ≡ erased n))  ↝⟨ Σ-Erased-Erased-singleton↔ ⟩□
    ℕ                                                     □

  -- The logical equivalence underlying Nat↔ℕ is definitionally equal
  -- to Nat⇔ℕ.

  _ : _↔_.logical-equivalence Nat↔ℕ ≡ Nat⇔ℕ
  _ = refl _

  ----------------------------------------------------------------------
  -- A correctness result related to the module Operations-for-Nat

  module Operations-for-Nat-correct (o : Operations) where

    private

      module O-[] = Operations-for-Nat-[] o

    open Operations-for-Nat o

    to-ℕ-from-bits-to-bits :
      ∀ n → Nat→ℕ (from-bits (to-bits n)) ≡ Nat→ℕ n
    to-ℕ-from-bits-to-bits n@(_ , n′) =
      cong Nat→ℕ $
        _↔_.to (≡-for-indices↔≡ {m = from-bits (to-bits n)} {n = n})
          [ ⌊ from-bits (to-bits n) ⌋  ≡⟨ erased (proj₂ (O-[].to-bits n′)) ⟩∎
            ⌊ n ⌋                      ∎
          ]

  ----------------------------------------------------------------------
  -- Some examples

  private

    module Nat-[]-examples (o : Operations) where

      open Operations-for-Nat-[] o

      -- Converts unary natural numbers to binary natural numbers.

      from-ℕ : ∀ n → Nat-[ n ]
      from-ℕ = proj₂ ∘ _↔_.from Nat↔ℕ

      -- Nat n is a proposition, so it is easy to prove that two
      -- values of this type are equal.

      example₁ : from-ℕ 4 + ⌊ from-ℕ 12 /2⌋ ≡ from-ℕ 10
      example₁ = Nat-[]-propositional _ _

      -- However, stating that two values of type Nat m and Nat n are
      -- equal, for equal natural numbers m and n, can be awkward.

      @0 example₂ :
        {@0 m n : ℕ} →
        (b : Nat-[ m ]) (c : Nat-[ n ]) →
        subst (λ n → Nat-[ n ]) (N.+-comm m) (b + c) ≡ c + b
      example₂ _ _ = Nat-[]-propositional _ _

    module Nat-examples (o : Operations) where

      open Operations-for-Nat o

      -- If Nat is used instead of Nat-[_], then it can be easier to
      -- state that two values are equal.

      example₁ : ⌈ 4 ⌉ + ⌊ ⌈ 12 ⌉ /2⌋ ≡ ⌈ 10 ⌉
      example₁ = _↔_.to ≡-for-indices↔≡ [ refl _ ]

      example₂ : ∀ m n → m + n ≡ n + m
      example₂ m n = _↔_.to ≡-for-indices↔≡
        [ ⌊ m ⌋ N.+ ⌊ n ⌋  ≡⟨ N.+-comm ⌊ m ⌋ ⟩∎
          ⌊ n ⌋ N.+ ⌊ m ⌋  ∎
        ]

      -- One can construct a proof showing that ⌈ 5 ⌉ is either equal
      -- or not equal to ⌈ 2 ⌉ + ⌈ 3 ⌉, but the proof does not compute
      -- to "inj₁ something" at compile-time.

      example₃ : Dec (⌈ 5 ⌉ ≡ ⌈ 2 ⌉ + ⌈ 3 ⌉)
      example₃ =
        Dec-map (_↔_.logical-equivalence ≡-for-indices↔≡)
          (⌈ 5 ⌉ ≟ ⌈ 2 ⌉ + ⌈ 3 ⌉)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Import where

import Agda.Builtin.Bool
  as _
open import Agda.Builtin.Nat
  as _
import Agda.Builtin.Unit
  using (⊤; tt)

A
  : Set
A
  = Agda.Builtin.Unit.⊤

ext: agda

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
{-# OPTIONS --safe -W ignore #-}

module Map where

open import Data.String
open import Data.String.Properties using (_==_)
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Unit
open import Data.Empty
open import Relation.Nullary using (¬_)
import Relation.Nullary.Decidable.Core
import Data.List.Relation.Binary.Pointwise
import Data.List.Relation.Binary.Pointwise.Properties
import Agda.Builtin.Char.Properties
import Agda.Builtin.Char
import Data.Nat.Properties

-- The empty map
K : {A : Set} → (v : A) → (String → A)
K v = (λ _ → v)

-- Storing in map "m" with value "v" into key "k"
Store : {A : Set} → (m : (String → A)) → (k : String)
        → (v : A) → (String → A)
Store m k v = λ k' → if (k' == k) then v else m k'

-- Unit tests
open import Data.Nat

-- Example of initialising the variable stack
S : (String → ℕ)
S = K 0

-- Example of adding values to a stack
S1 : (String → ℕ)
S1 = Store S "a" 10

-- Adding the second variable
S2 : (String → ℕ)
S2 = Store S1 "b" 11

-- Getting the value of a from stack S2
A : ℕ
A = S2 "a"

-- Getting the value of b from stack S2
B : ℕ
B = S2 "b"

-- Try to get a string that is not in stack, gives the default value
C : ℕ
C = S2 "c"

-- Important properties

-- Lemma needed to prove the side condition between stacks after
-- function call
lemma-stack-eq : {A : Set} → ∀ (stm stf : (String → A)) → (X Y : String)
                 → (Store stm Y (stf X)) Y ≡ (stf X)
lemma-stack-eq stm stf X Y with (Y Data.String.≟ Y)
... | .true Relation.Nullary.because Relation.Nullary.ofʸ p = refl
... | .false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p = ⊥-elim (¬p refl)

-- Now a very important property for proving the constancy rule
t-update-neq : {A : Set} → ∀ (st : (String → A)) → (x1 x2 : String)
               → (v : A) → ((x2 ≡ x1) → ⊥) → (Store st x1 v) x2 ≡ (st x2)
t-update-neq st x1 x2 v p with (Relation.Nullary.Decidable.Core.map′
        (λ x →
           Data.String.Properties.toList-injective x2 x1
           (Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡ x))
        (λ x →
           Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡ (cong toList x))
        (Data.List.Relation.Binary.Pointwise.Properties.decidable
         (λ x y →
            Relation.Nullary.Decidable.Core.map′
            (Agda.Builtin.Char.Properties.primCharToNatInjective x y)
            (cong Agda.Builtin.Char.primCharToNat)
            (Relation.Nullary.Decidable.Core.map′
             (Data.Nat.Properties.≡ᵇ⇒≡ (Agda.Builtin.Char.primCharToNat x)
              (Agda.Builtin.Char.primCharToNat y))
             (Data.Nat.Properties.≡⇒≡ᵇ (Agda.Builtin.Char.primCharToNat x)
              (Agda.Builtin.Char.primCharToNat y))
             (T?
              (Agda.Builtin.Char.primCharToNat x ≡ᵇ
               Agda.Builtin.Char.primCharToNat y))))
         (toList x2) (toList x1)))
... | false Relation.Nullary.because Relation.Nullary.ofⁿ ¬p = refl
... | true Relation.Nullary.because Relation.Nullary.ofʸ refl = ⊥-elim (p refl)

-- Testing lookup with nested stores
test : {A : Set} →  ∀ (x1 x2 y : String) → (st st' : (String → A))
       → (v1 v2 : A) → (y ≡ x1 → ⊥) → (y ≡ x2 → ⊥)
       → (st' ≡ (Store (Store st x1 v1) x2 v2))
       → st' y ≡ st y
test x1 x2 y st st' v1 v2 p1 p2 q rewrite q
  | t-update-neq (Store st x1 v1) x2 y v2 p2
  | t-update-neq st x1 y v1 p1 = refl

-- Partial map
open import Data.Maybe

KP : {A : Set} → (String → Maybe A)
KP = (λ _ → nothing)

StoreP : {A : Set} → (st : (String → Maybe A))
         → (x : String) → (v : A)
         → (String → Maybe A)
StoreP st x v = λ x' → if x == x' then just v else st x'


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

module 2DTypes where

-- open import Level renaming (zero to lzero)
open import Relation.Binary.PropositionalEquality
open import Data.Unit
open import Data.Sum
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Product
open import Function using (_∘_)
open import Relation.Binary using (Setoid)
open import Data.Nat using (ℕ) renaming (suc to ℕsuc; _+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; lookup; _∷_; []; zipWith)
open import Data.Integer hiding (suc)

open import VectorLemmas using (_!!_)
open import PiU
open import PiLevel0 hiding (!!)
open import PiEquiv
open import PiLevel1
open import Equiv
open import EquivEquiv using (_≋_; module _≋_)

open import Categories.Category
open import Categories.Groupoid
open import Categories.Equivalence.Strong

-- This exists somewhere, but I can't find it
⊎-inj : ∀ {ℓ} {A B : Set ℓ} {a : A} {b : B} → inj₁ a ≡ inj₂ b → ⊥
⊎-inj ()

-- should probably make this level-polymorphic
record Typ : Set where
  constructor typ
  field
    carr : U
    len : ℕ -- number of non-trivial automorphisms
    auto : Vec (carr ⟷ carr) (ℕsuc len) -- the real magic goes here

    -- normally the stuff below is "global", but here
    -- we attach it to a type.
    id : id⟷ ⇔ (auto !! zero)
    _⊙_ : Fin (ℕsuc len) → Fin (ℕsuc len) → Fin (ℕsuc len)
    coh : ∀ (i j : Fin (ℕsuc len)) → -- note the flip !!!
        ((auto !! i) ◎ (auto !! j) ⇔ (auto !! (j ⊙ i)))
    -- to get groupoid, we need inverse knowledge, do later

open Typ

-- The above 'induces' a groupoid structure, which
-- we need to show in detail.
-- First, a useful container for the info we need:
record Hm (t : Typ) (a b : ⟦ carr t ⟧) : Set where
  constructor hm
  field
    eq : carr t ⟷ carr t
    good : Σ (Fin (ℕsuc (len t))) (λ n → eq ⇔ (auto t !! n))
    fwd : proj₁ (c2equiv eq) a ≡ b
    bwd : isqinv.g (proj₂ (c2equiv eq)) b ≡ a

-- note how (auto t) is not actually used!
-- also: not sure e₁ and e₂ always used coherently, as types are not enough
--  to decide which one to use...
induceCat : Typ → Category _ _ _
induceCat t = record
  { Obj =  ⟦ carr t ⟧
  ; _⇒_ = Hm t
  ; _≡_ = λ { (hm e₁ g₁ _ _) → λ { (hm e₂ g₂ _ _) → e₁ ⇔ e₂} }
  ; id = hm id⟷ (zero , id t) refl refl
  ; _∘_ = λ { {A} {B} {C} (hm e₁ (n₁ , p₁) fwd₁ bwd₁) (hm e₂ (n₂ , p₂) fwd₂ bwd₂) →
   let pf₁ = (begin (
        proj₁ (c2equiv e₁ ● c2equiv e₂) A
          ≡⟨ β₁ A ⟩
        (proj₁ (c2equiv e₁) ∘ (proj₁ (c2equiv e₂))) A
          ≡⟨ cong (proj₁ (c2equiv e₁)) fwd₂ ⟩
        proj₁ (c2equiv e₁) B
          ≡⟨ fwd₁ ⟩
        C ∎ ))
       -- same as above (in opposite direction), just compressed
       pf₂ = trans (β₂ C)
            (trans (cong (isqinv.g (proj₂ (c2equiv e₂))) bwd₁)
                   bwd₂)
       n₃ = _⊙_ t n₁ n₂
       compos = n₃ , trans⇔ (p₂ ⊡ p₁) (coh t n₂ n₁)
   in
        hm (e₂ ◎ e₁) compos pf₁ pf₂ }
  ; assoc = assoc◎l
  ; identityˡ = idr◎l
  ; identityʳ = idl◎l
  ; equiv = record { refl = id⇔ ; sym = 2! ; trans = trans⇔ }
  ; ∘-resp-≡ = λ f g → g ⊡ f
  }
  where open Typ
        open ≡-Reasoning

{-
 -- to get the Groupoid structure, there is stuff in the type that is
 -- missing; see the hole.
induceG : (t : Typ)  → Groupoid (induceCat t)
induceG t = record
  { _⁻¹ = λ { {A} {B} (hm e g fw bw) →
    hm (! e) {!!} (trans (f≡ (!≡sym≃ e) B) bw) (trans (g≡ (!≡sym≃ e) A) fw) }
  ; iso = record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }
  where open _≋_
-}

-- some useful functions for defining the type 1T
private
  mult : Fin 1 → Fin 1 → Fin 1
  mult zero zero = zero
  mult _ (suc ())
  mult (suc ()) _

  triv : Vec (ONE ⟷ ONE) 1
  triv = id⟷ ∷ []

  mult-coh : ∀ (i j : Fin 1) →
        ((triv !! i) ◎ (triv !! j) ⇔ (triv !! (mult j i)))
  mult-coh zero zero = idl◎l -- note how this is non-trivial!
  mult-coh _ (suc ())
  mult-coh (suc ()) _

1T : Typ
1T = record
  { carr = ONE
  ; len = 0
  ; auto = triv
  ; id = id⇔
  ; _⊙_ = mult
  ; coh = mult-coh
  }

BOOL : U
BOOL = PLUS ONE ONE

-- some useful functions for defining the type 1T′
private
  mult′ : Fin 2 → Fin 2 → Fin 2
  mult′ zero zero = zero
  mult′ zero (suc zero) = suc zero
  mult′ _ (suc (suc ()))
  mult′ (suc zero) zero = suc zero
  mult′ (suc zero) (suc zero) = zero
  mult′ (suc (suc ())) _

  sw : Vec (BOOL ⟷ BOOL) 2
  sw = id⟷ ∷ swap₊ ∷ []

  sw-coh :  ∀ (i j : Fin 2) →
        ((sw !! i) ◎ (sw !! j) ⇔ (sw !! (mult′ j i)))
  sw-coh zero zero = idl◎l
  sw-coh zero (suc zero) = idl◎l
  sw-coh _ (suc (suc ()))
  sw-coh (suc zero) zero = idr◎l
  sw-coh (suc zero) (suc zero) = linv◎l
  sw-coh (suc (suc ())) _

1T′ : Typ
1T′ = record
  { carr = BOOL
  ; len = 1
  ; auto = sw
  ; id = id⇔
  ; _⊙_ = mult′
  ; coh = sw-coh
  }

-- useful utilities
private
  collapse : ⊤ ⊎ ⊤ → ⊤
  collapse (inj₁ a) = a
  collapse (inj₂ b) = b

  collapse-coh : ∀ {A B : ⊤ ⊎ ⊤} → collapse A ≡ collapse B
  collapse-coh {inj₁ tt} {inj₁ tt} = refl
  collapse-coh {inj₁ tt} {inj₂ tt} = refl
  collapse-coh {inj₂ tt} {inj₁ tt} = refl
  collapse-coh {inj₂ tt} {inj₂ tt} = refl

-- let's do it on categories only.
-- The important thing here is that we only have
-- access to id⟷ and (auto 1T′) as things of type
-- (carr 1T′ ⟷ carr 1T′).
1T≃1T′ : StrongEquivalence (induceCat 1T) (induceCat 1T′)
1T≃1T′ =
  record
  -- from 1T to 1T′, we really do want to map down to id⟷ onto inj₁
  { F = record
    { F₀ = inj₁
    ; F₁ = λ { {tt} {tt} (hm e g fwd bwd) → hm id⟷ (zero , id⇔) refl refl}
    ; identity = id⇔
    ; homomorphism = idl◎r
    ; F-resp-≡ = λ _ → id⇔
    }
  -- and here, everything should be collapsed
  ; G = record
    { F₀ = collapse
    ; F₁ = λ { {A} {B} (hm e g fwd bwd) →
        hm id⟷ (zero , id⇔) (collapse-coh {A} {B}) (collapse-coh {B} {A})}
    ; identity = id⇔
    ; homomorphism = idl◎r
    ; F-resp-≡ = λ _ → id⇔
    }
  -- and here is where (auto 1T′) is needed, else this is false!!
  ; weak-inverse = record
    { F∘G≅id = record
      { F⇒G = record
        { η = λ { (inj₁ a) → hm id⟷ (zero , id⇔) refl refl;
                  (inj₂ b) → hm swap₊ (suc zero , id⇔) refl refl }
        ; commute =
          λ { {inj₁ tt} {inj₁ tt} (hm c (zero , x) _ _) →  trans⇔ idl◎l (trans⇔ (2! x) idl◎r) ;
              {inj₁ tt} {inj₁ tt} (hm c (suc zero , x) a b) →
                  ⊥-elim (⊎-inj (
                    trans (sym a) (
                    trans (sym (lemma0 c (inj₁ tt)))
                          (≋⇒≡ x (inj₁ tt))))) ;
              {inj₁ tt} {inj₁ tt} (hm c (suc (suc ()), _) _ _);
              {inj₁ tt} {inj₂ tt} (hm c (zero , x) a b) →
                ⊥-elim (⊎-inj (
                  trans (sym (≋⇒≡ x (inj₁ tt))) (
                  trans (lemma0 c (inj₁ tt))
                         a ) ) );
              {inj₁ tt} {inj₂ tt} (hm c (suc zero , x) _ _) →
                trans⇔ idl◎l (trans⇔ (2! x) idl◎r) ;
              {inj₁ tt} {inj₂ tt} (hm c (suc (suc ()), _) _ _);
              {inj₂ tt} {inj₁ tt} (hm c (zero , x) a b) →
                ⊥-elim (⊎-inj (
                  trans (sym a) (
                  trans (sym (lemma0 c (inj₂ tt)))
                        (≋⇒≡ x (inj₂ tt)) ) ) );
              {inj₂ tt} {inj₁ tt} (hm c (suc (suc ()), _) _ _);
              {inj₂ tt} {inj₂ tt} (hm c (zero , x) _ _) →
                trans⇔ idl◎l (trans⇔ idr◎r (id⇔ ⊡ (2! x)));
              {inj₂ tt} {inj₁ tt} (hm c (suc zero , x) _ _) →
                trans⇔ idl◎l (trans⇔ linv◎r (id⇔ ⊡ (2! x)));
              {inj₂ tt} {inj₂ tt} (hm c (suc zero , x) a b) →
                ⊥-elim (⊎-inj (
                  trans (sym (≋⇒≡ x (inj₂ tt))) (
                   trans (lemma0 c (inj₂ tt)) a) ) ) ;
              {inj₂ tt} {inj₂ tt} (hm c (suc (suc ()), _) _ _)
            }
          }
      ; F⇐G = record
        { η = λ { (inj₁ a) → hm id⟷ (zero , id⇔) refl refl;
                  (inj₂ b) → hm swap₊ ((suc zero , id⇔)) refl refl }
        ; commute = λ
          { {inj₁ tt} {inj₁ tt} (hm a (zero , e) c d) → e ⊡ id⇔
          ; {inj₁ tt} {inj₂ tt} (hm a (zero , e) c d) → {!!}
          ; {inj₂ tt} {inj₁ tt} (hm a (zero , e) c d) → {!!}
          ; {inj₂ tt} {inj₂ tt} (hm a (zero , e) c d) → trans⇔ (e ⊡ id⇔) (trans⇔ idl◎l idr◎r)
          ; {inj₁ tt} {inj₁ tt} (hm a (suc zero , e) c d) → {!!}
          ; {inj₁ tt} {inj₂ tt} (hm a (suc zero , e) c d) → {!!}
          ; {inj₂ tt} {inj₁ tt} (hm a (suc zero , e) c d) → {!!}
          ; {inj₂ tt} {inj₂ tt} (hm a (suc zero , e) c d) → {!!}
          ; (hm a (suc (suc ()) , _) _ _) }
        }
      ; iso = λ { (inj₁ tt) → record { isoˡ = idl◎l ; isoʳ = idl◎l };
                  (inj₂ tt) → record { isoˡ = linv◎l ; isoʳ = linv◎l } }
      }
    ; G∘F≅id = record
      { F⇒G = record
        { η = λ {tt → hm id⟷ (zero , id⇔) refl refl}
        ; commute =
          λ { {tt} {tt} (hm eq (zero , e) _ _) → id⇔ ⊡ (2! e)
            ; {tt} {tt} (hm eq (suc () , _) _ _) }
        }
      ; F⇐G = record
        { η = λ {tt → hm id⟷ (zero , id⇔) refl refl}
        ; commute =
          λ { {tt} {tt} (hm c (zero , e) _ _) → e ⊡ id⇔
            ; {tt} {tt} (hm c (suc () , _) _ _) }
        }
      ; iso = λ {tt → record { isoˡ = linv◎l ; isoʳ = linv◎l } }
      }
    }
  }

-- And so 1T′ is equivalent to 1T.  This can be interpreted to mean
-- that swap₊ (perhaps more precisely, id⟷ ∷ swap₊ ∷ [] ) is the
-- representation of a 'negative type'.

---------------
-- Cardinality function
card : Typ → ℤ
card (typ carr len _ _ _ _) = (+ size carr) - (+ len)

-- check
card-1T : card 1T ≡ + 1
card-1T = refl

card-1T′ : card 1T′ ≡ + 1
card-1T′ = refl

--------------
-- Conjecture...

-- to make this work, we're going to postulate another loop
-- and that it is idempotent:
postulate
  loop : ZERO ⟷ ZERO
  idemp : loop ◎ loop ⇔ loop

private
  cc : Fin 2 → Fin 2 → Fin 2
  cc zero zero = zero
  cc zero (suc zero) = suc zero
  cc (suc zero) zero = suc zero
  cc (suc zero) (suc zero) = suc zero
  cc (suc (suc ())) _
  cc _ (suc (suc ()))

  two-loops : Vec (ZERO ⟷ ZERO) 2
  two-loops = id⟷ ∷ loop ∷ []

  tl-coh :   ∀ (i j : Fin 2) →
        ((two-loops !! i) ◎ (two-loops !! j) ⇔ (two-loops !! (cc j i)))
  tl-coh zero zero = idl◎l
  tl-coh zero (suc zero) = idl◎l
  tl-coh (suc zero) zero = idr◎l
  tl-coh (suc zero) (suc zero) = {!idemp!}
  tl-coh (suc (suc ())) _
  tl-coh _ (suc (suc ()))

-1T : Typ
-1T = typ ZERO 1 two-loops id⇔ cc tl-coh

card--1T : card -1T ≡ -[1+ 0 ] -- indeed -1 ...
card--1T = refl

{--
Here is my current thinking:

* A type is a package of:
 - a carrier (that comes with the trivial automorphism)
 - a collection of non-trivial automorphisms that have a groupoid structure
 Let’s denote this package by ‘R A (Auto A)'

* The collection of non-trivial automorphisms could very well be
  missing (i.e., empty) and we then recover plain sets like Bool etc.

* Now here is the interesting bit: the carrier itself could be
  missing, i.e., a parameter. In that case we get something like:

 A -> R A (Auto A)

 That thing could be treated as outside the universe of types but we
 are proposing to enlarge the universe of type to also include it as a
 fractional type. Of course we need a way to combine such a fractional
 type with a carrier to get a regular type so we need another
 operation _[_] to do the instantiation.

* So to revise, a type is:

 T ::= R A (Auto A)    |    /\ A . T    |     T[A]

To make sure this behaves like fractional types, we want /\ A. T and
T[A] to behave like a product. It is a product of course but a
dependent one.
--}

-- Parameterized type
-- Frac supposed to 1/t
-- instantiate Frac with u to get u/t
-- make sure t/t is 1
-- define eta and epsilon and check axioms

{-- Syntax of types --}

Auto : (u : U) → Set
Auto u = Σ[ n ∈ ℕ ] (Vec (u ⟷ u) n)

trivA : (u : U) → Auto u
trivA u = (1 , id⟷ ∷ [])

data T : (u₁ : U) → {u₂ : U} → Auto u₂ → Set where
  UT : (u : U) → T u (trivA u) -- regular sets
  FT : (u₁ u₂ : U) → (auto₂ : Auto u₂) → T u₁ auto₂

-- Regular sets

ZT : T ZERO (trivA ZERO)
ZT = UT ZERO

OT : T ONE (trivA ONE)
OT = UT ONE

-- one third

2U : U
2U = PLUS ONE ONE

3U : U
3U = PLUS ONE (PLUS ONE ONE)

3T : T 3U (trivA 3U)
3T = UT 3U

-- could add the remaining two but these are sufficient I think
all3A : Auto 3U
all3A = (4 , id⟷ ∷
             (id⟷ ⊕ swap₊) ∷
             (assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊) ∷
             ((id⟷ ⊕ swap₊) ◎ (assocl₊ ◎ (swap₊ ⊕ id⟷) ◎ assocr₊) ◎ (id⟷ ⊕ swap₊)) ∷
             [])

1/3T : T ONE all3A
1/3T = FT ONE 3U all3A

-- notice that a/b + c/b = (a+c) / b
-- So 1/3T + 1/3T is

2/3T : T 2U all3A
2/3T = FT 2U 3U all3A

-- one more

3/3T : T 3U all3A
3/3T = FT 3U 3U all3A

-- Now eta applied to 3/3T should match the carrier with the autos and produce the plain OT

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Categories.Category

-- Defines the following properties of a Category:
-- 1. BinaryProducts -- for when a Category has all Binary Products
-- 2. Cartesian -- a Cartesian category is a category with all products

module Categories.Category.Cartesian {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Data.Product using (Σ; _,_; uncurry)

open Category 𝒞
open HomReasoning

open import Categories.Object.Terminal 𝒞
open import Categories.Object.Product 𝒞
open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
open import Categories.Category.Monoidal
import Categories.Category.Monoidal.Symmetric as Sym

open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation using (ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl; sym; trans)

private
  variable
    A B C D X Y Z : Obj
    f f′ g g′ h i : A ⇒ B

record BinaryProducts : Set (levelOfTerm 𝒞) where

  infixr 7 _×_
  infixr 8 _⁂_
  infix 11 ⟨_,_⟩

  field
    product : ∀ {A B} → Product A B

  module product {A} {B} = Product (product {A} {B})

  _×_ : Obj → Obj → Obj
  A × B = Product.A×B (product {A} {B})

  ×-comm : A × B ≅ B × A
  ×-comm = Commutative product product

  ×-assoc : X × Y × Z ≅ (X × Y) × Z
  ×-assoc = Associative product product product product

  open product hiding (⟨_,_⟩; ∘-distribʳ-⟨⟩) public

  -- define it like this instead of reexporting to redefine fixity
  ⟨_,_⟩ : X ⇒ A → X ⇒ B → X ⇒ A × B
  ⟨_,_⟩ = Product.⟨_,_⟩ product

  _⁂_ : A ⇒ B → C ⇒ D → A × C ⇒ B × D
  f ⁂ g = [ product ⇒ product ] f × g

  assocˡ : (A × B) × C ⇒ A × B × C
  assocˡ = _≅_.to ×-assoc

  assocʳ : A × B × C ⇒ (A × B) × C
  assocʳ = _≅_.from ×-assoc

  assocʳ∘assocˡ : assocʳ {A}{B}{C} ∘ assocˡ {A}{B}{C} ≈ id
  assocʳ∘assocˡ = Iso.isoʳ (_≅_.iso ×-assoc)

  assocˡ∘assocʳ : assocˡ {A}{B}{C} ∘ assocʳ {A}{B}{C} ≈ id
  assocˡ∘assocʳ = Iso.isoˡ (_≅_.iso ×-assoc)

  ⟨⟩-congʳ : f ≈ f′ → ⟨ f , g ⟩ ≈ ⟨ f′ , g ⟩
  ⟨⟩-congʳ pf = ⟨⟩-cong₂ pf refl

  ⟨⟩-congˡ : g ≈ g′ → ⟨ f , g ⟩ ≈ ⟨ f , g′ ⟩
  ⟨⟩-congˡ pf = ⟨⟩-cong₂ refl pf

  swap : A × B ⇒ B × A
  swap = ⟨ π₂ , π₁ ⟩

  -- TODO: this is probably harder to use than necessary because of this definition. Maybe make a version
  -- that doesn't have an explicit id in it, too?
  first : A ⇒ B → A × C ⇒ B × C
  first f = f ⁂ id

  second : C ⇒ D → A × C ⇒ A × D
  second g = id ⁂ g

  -- Just to make this more obvious
  π₁∘⁂ : π₁ ∘ (f ⁂ g) ≈ f ∘ π₁
  π₁∘⁂ {f = f} {g} = project₁

  π₂∘⁂ : π₂ ∘ (f ⁂ g) ≈ g ∘ π₂
  π₂∘⁂ {f = f} {g} = project₂

  ⁂-cong₂ : f ≈ g → h ≈ i → f ⁂ h ≈ g ⁂ i
  ⁂-cong₂ = [ product ⇒ product ]×-cong₂

  ⁂∘⟨⟩ : (f ⁂ g) ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g ∘ g′ ⟩
  ⁂∘⟨⟩ = [ product ⇒ product ]×∘⟨⟩

  first∘⟨⟩ : first f ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f ∘ f′ , g′ ⟩
  first∘⟨⟩ = [ product ⇒ product ]×id∘⟨⟩

  second∘⟨⟩ : second g ∘ ⟨ f′ , g′ ⟩ ≈ ⟨ f′ , g ∘ g′ ⟩
  second∘⟨⟩ = [ product ⇒ product ]id×∘⟨⟩

  ⁂∘⁂ : (f ⁂ g) ∘ (f′ ⁂ g′) ≈ (f ∘ f′) ⁂ (g ∘ g′)
  ⁂∘⁂ = [ product ⇒ product ⇒ product ]×∘×

  ⟨⟩∘ : ⟨ f , g ⟩ ∘ h ≈ ⟨ f ∘ h , g ∘ h ⟩
  ⟨⟩∘ = [ product ]⟨⟩∘

  first∘first : ∀ {C} → first {C = C} f ∘ first g ≈ first (f ∘ g)
  first∘first = [ product ⇒ product ⇒ product ]×id∘×id

  second∘second : ∀ {A} → second {A = A} f ∘ second g ≈ second (f ∘ g)
  second∘second = [ product ⇒ product ⇒ product ]id×∘id×

  first↔second : first f ∘ second g ≈ second g ∘ first f
  first↔second = [ product ⇒ product , product ⇒ product ]first↔second

  firstid : ∀ {f : A ⇒ A} (g : A ⇒ C) → first {C = C} f ≈ id → f ≈ id
  firstid {f = f} g eq = begin
    f                    ≈˘⟨ elimʳ project₁ ⟩
    f ∘ π₁ ∘ ⟨ id , g ⟩  ≈⟨ pullˡ fπ₁≈π₁ ⟩
    π₁ ∘ ⟨ id , g ⟩      ≈⟨ project₁ ⟩
    id                   ∎
    where fπ₁≈π₁ = begin
            f ∘ π₁       ≈˘⟨ project₁ ⟩
            π₁ ∘ first f ≈⟨ refl⟩∘⟨ eq ⟩
            π₁ ∘ id      ≈⟨ identityʳ ⟩
            π₁           ∎

  swap∘⟨⟩ : swap ∘ ⟨ f , g ⟩ ≈ ⟨ g , f ⟩
  swap∘⟨⟩ {f = f} {g = g} = begin
    ⟨ π₂ , π₁ ⟩ ∘ ⟨ f , g ⟩             ≈⟨ ⟨⟩∘ ⟩
    ⟨ π₂ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ f , g ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ project₂ project₁ ⟩
    ⟨ g , f ⟩                           ∎

  swap∘⁂ : swap ∘ (f ⁂ g) ≈ (g ⁂ f) ∘ swap
  swap∘⁂ {f = f} {g = g} = begin
    swap ∘ (f ⁂ g)      ≈⟨ swap∘⟨⟩ ⟩
    ⟨ g ∘ π₂ , f ∘ π₁ ⟩ ≈⟨ sym ⁂∘⟨⟩ ⟩
    (g ⁂ f) ∘ swap      ∎

  swap∘swap : (swap {A}{B}) ∘ (swap {B}{A}) ≈ id
  swap∘swap = trans swap∘⟨⟩ η

  assocʳ∘⟨⟩ : assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈ ⟨ ⟨ f , g ⟩ , h ⟩
  assocʳ∘⟨⟩ {f = f} {g = g} {h = h} = begin
    assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩
    ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    , (π₂ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
    ⟩                          ≈⟨ ⟨⟩-cong₂ ⟨⟩∘ (pullʳ project₂) ⟩
    ⟨ ⟨ π₁        ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      , (π₁ ∘ π₂) ∘ ⟨ f , ⟨ g , h ⟩ ⟩
      ⟩
    , π₂ ∘ ⟨ g , h ⟩
    ⟩                          ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁
                                                     (trans (pullʳ project₂) project₁))
                                           project₂ ⟩
    ⟨ ⟨ f , g ⟩ , h ⟩          ∎

  assocˡ∘⟨⟩ : assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩ ≈ ⟨ f , ⟨ g , h ⟩ ⟩
  assocˡ∘⟨⟩ {f = f} {g = g} {h = h} = begin
    assocˡ ∘ ⟨ ⟨ f , g ⟩ , h ⟩          ≈⟨ sym (refl ⟩∘⟨ assocʳ∘⟨⟩) ⟩
    assocˡ ∘ assocʳ ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≈⟨ cancelˡ assocˡ∘assocʳ ⟩
    ⟨ f , ⟨ g , h ⟩ ⟩                   ∎

  assocʳ∘⁂ : assocʳ ∘ (f ⁂ (g ⁂ h)) ≈ ((f ⁂ g) ⁂ h) ∘ assocʳ
  assocʳ∘⁂ {f = f} {g = g} {h = h} =
    begin
      assocʳ ∘ (f ⁂ (g ⁂ h))
    ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
      assocʳ ∘ ⟨ f ∘ π₁ , ⟨ (g ∘ π₁) ∘ π₂ , (h ∘ π₂) ∘ π₂ ⟩ ⟩
    ≈⟨ assocʳ∘⟨⟩ ⟩
      ⟨ ⟨ f ∘ π₁ , (g ∘ π₁) ∘ π₂ ⟩ , (h ∘ π₂) ∘ π₂ ⟩
    ≈⟨ ⟨⟩-cong₂ (⟨⟩-congˡ assoc) assoc ⟩
      ⟨ ⟨ f ∘ π₁ , g ∘ π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ≈˘⟨ ⟨⟩-congʳ ⁂∘⟨⟩ ⟩
      ⟨ (f ⁂ g) ∘ ⟨ π₁ , π₁ ∘ π₂ ⟩ , h ∘ π₂ ∘ π₂ ⟩
    ≈˘⟨ ⁂∘⟨⟩ ⟩
      ((f ⁂ g) ⁂ h) ∘ assocʳ
    ∎

  assocˡ∘⁂ : assocˡ ∘ ((f ⁂ g) ⁂ h) ≈ (f ⁂ (g ⁂ h)) ∘ assocˡ
  assocˡ∘⁂ {f = f} {g = g} {h = h} =
    begin
      assocˡ ∘ ((f ⁂ g) ⁂ h)
    ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
      assocˡ ∘ ⟨ ⟨ (f ∘ π₁) ∘ π₁ , (g ∘ π₂) ∘ π₁ ⟩ , h ∘ π₂ ⟩
    ≈⟨ assocˡ∘⟨⟩ ⟩
      ⟨ (f ∘ π₁) ∘ π₁ , ⟨ (g ∘ π₂) ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ≈⟨ ⟨⟩-cong₂ assoc (⟨⟩-congʳ assoc) ⟩
      ⟨ f ∘ π₁ ∘ π₁ , ⟨ g ∘ π₂ ∘ π₁ , h ∘ π₂ ⟩ ⟩
    ≈˘⟨ ⟨⟩-congˡ ⁂∘⟨⟩ ⟩
      ⟨ f ∘ π₁ ∘ π₁ , (g ⁂ h) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
    ≈˘⟨ ⁂∘⟨⟩ ⟩
      (f ⁂ (g ⁂ h)) ∘ assocˡ
    ∎

  -×- : Bifunctor 𝒞 𝒞 𝒞
  -×- = record
    { F₀           = uncurry _×_
    ; F₁           = uncurry _⁂_
    ; identity     = id×id product
    ; homomorphism = sym ⁂∘⁂
    ; F-resp-≈     = uncurry [ product ⇒ product ]×-cong₂
    }

  -×_ : Obj → Functor 𝒞 𝒞
  -×_ = appʳ -×-

  _×- : Obj → Functor 𝒞 𝒞
  _×- = appˡ -×-

-- Cartesian monoidal category
record Cartesian : Set (levelOfTerm 𝒞) where
  field
    terminal : Terminal
    products : BinaryProducts

  module terminal = Terminal terminal
  module products = BinaryProducts products
  open terminal public
  open products public

  ⊤×A≅A : ⊤ × A ≅ A
  ⊤×A≅A = record
    { from = π₂
    ; to   = ⟨ ! , id ⟩
    ; iso  = record
      { isoˡ = begin
        ⟨ ! , id ⟩ ∘ π₂ ≈˘⟨ unique !-unique₂ (cancelˡ project₂) ⟩
        ⟨ π₁ , π₂ ⟩     ≈⟨ η ⟩
        id              ∎
      ; isoʳ = project₂
      }
    }

  A×⊤≅A : A × ⊤ ≅ A
  A×⊤≅A = record
    { from = π₁
    ; to   = ⟨ id , ! ⟩
    ; iso  = record
      { isoˡ = begin
        ⟨ id , ! ⟩ ∘ π₁ ≈˘⟨ unique (cancelˡ project₁) !-unique₂ ⟩
        ⟨ π₁ , π₂ ⟩     ≈⟨ η ⟩
        id              ∎
      ; isoʳ = project₁
      }
    }

  ⊤×--id : NaturalIsomorphism (⊤ ×-) idF
  ⊤×--id = record
    { F⇒G = ntHelper record
      { η       = λ _ → π₂
      ; commute = λ _ → project₂
      }
    ; F⇐G = ntHelper record
      { η       = λ _ → ⟨ ! , id ⟩
      ; commute = λ f → begin
        ⟨ ! , id ⟩ ∘ f                                     ≈⟨ ⟨⟩∘ ⟩
        ⟨ ! ∘ f , id  ∘ f ⟩                                ≈⟨ ⟨⟩-cong₂ (sym (!-unique _)) identityˡ ⟩
        ⟨ ! , f ⟩                                          ≈˘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
        ⟨ id ∘ ! , f ∘ id ⟩                                ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ project₂) ⟩
        ⟨ (id ∘ π₁) ∘ ⟨ ! , id ⟩ , (f ∘ π₂) ∘ ⟨ ! , id ⟩ ⟩ ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ id ∘ π₁ , f ∘ π₂ ⟩ ∘ ⟨ ! , id ⟩                  ∎
      }
    ; iso = λ _ → _≅_.iso ⊤×A≅A
    }

  -×⊤-id : NaturalIsomorphism (-× ⊤) idF
  -×⊤-id = record
    { F⇒G = ntHelper record
      { η       = λ _ → π₁
      ; commute = λ _ → project₁
      }
    ; F⇐G = ntHelper record
      { η       = λ _ → ⟨ id , ! ⟩
      ; commute = λ f → begin
        ⟨ id , ! ⟩ ∘ f                                     ≈⟨ ⟨⟩∘ ⟩
        ⟨ id ∘ f , ! ∘ f ⟩                                 ≈⟨ ⟨⟩-cong₂ identityˡ (sym (!-unique _)) ⟩
        ⟨ f , ! ⟩                                          ≈˘⟨ ⟨⟩-cong₂ identityʳ identityˡ ⟩
        ⟨ f ∘ id , id ∘ ! ⟩                                ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ project₂) ⟩
        ⟨ (f ∘ π₁) ∘ ⟨ id , ! ⟩ , (id ∘ π₂) ∘ ⟨ id , ! ⟩ ⟩ ≈˘⟨ ⟨⟩∘ ⟩
        ⟨ f ∘ π₁ , id ∘ π₂ ⟩ ∘ ⟨ id , ! ⟩                  ∎
      }
    ; iso = λ _ → _≅_.iso A×⊤≅A
    }

  monoidal : Monoidal 𝒞
  monoidal = record
    { ⊗                    = -×-
    ; unit                 = ⊤
    ; unitorˡ              = ⊤×A≅A
    ; unitorʳ              = A×⊤≅A
    ; associator           = ≅.sym ×-assoc
    ; unitorˡ-commute-from = project₂
    ; unitorˡ-commute-to   = let open NaturalIsomorphism ⊤×--id in ⇐.commute _
    ; unitorʳ-commute-from = project₁
    ; unitorʳ-commute-to   = let open NaturalIsomorphism -×⊤-id in ⇐.commute _
    ; assoc-commute-from   = assocˡ∘⁂
    ; assoc-commute-to     = assocʳ∘⁂
    ; triangle             = begin
      (id ⁂ π₂) ∘ assocˡ                       ≈⟨ ⁂∘⟨⟩ ⟩
      ⟨ id ∘ π₁ ∘ π₁ , π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ identityˡ) (project₂ ○ (⟺ identityˡ)) ⟩
      π₁ ⁂ id                                  ∎
    ; pentagon             = begin
      (id ⁂ assocˡ) ∘ assocˡ ∘ (assocˡ ⁂ id)
        ≈⟨ pullˡ [ product ⇒ product ]id×∘⟨⟩ ⟩
      ⟨ π₁ ∘ π₁ , assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (assocˡ ⁂ id)
        ≈⟨ ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ (assocˡ ⁂ id) , (assocˡ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (assocˡ ⁂ id) ⟩
        ≈⟨ ⟨⟩-cong₂ (pullʳ project₁) (pullʳ ⟨⟩∘) ⟩
      ⟨ π₁ ∘ assocˡ ∘ π₁ , assocˡ ∘ ⟨ (π₂ ∘ π₁) ∘ (assocˡ ⁂ id) , π₂ ∘ (assocˡ ⁂ id) ⟩ ⟩
        ≈⟨ ⟨⟩-cong₂ (pullˡ project₁) (∘-resp-≈ʳ (⟨⟩-cong₂ (pullʳ project₁) project₂)) ⟩
      ⟨ (π₁ ∘ π₁) ∘ π₁ , assocˡ ∘ ⟨ π₂ ∘ assocˡ ∘ π₁ , id ∘ π₂ ⟩ ⟩
        ≈⟨ ⟨⟩-cong₂ assoc (∘-resp-≈ʳ (⟨⟩-cong₂ (pullˡ project₂) identityˡ)) ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩
        ≈⟨ ⟨⟩-congˡ ⟨⟩∘ ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ (π₁ ∘ π₁) ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩ ⟩
        ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘) ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ , π₂ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩ ⟩ ⟩
        ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (pullˡ project₁) (⟨⟩-cong₂ (pullʳ project₁) project₂)) ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ π₁ , ⟨ π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ π₁ , π₂ ⟩ ⟩ ⟩
        ≈⟨ ⟨⟩-congˡ (⟨⟩-cong₂ assoc (⟨⟩-congʳ (pullˡ project₂))) ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ⟩
        ≈˘⟨ ⟨⟩-congˡ (⟨⟩-cong₂ (pullʳ project₁) project₂) ⟩
      ⟨ π₁ ∘ π₁ ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ assocˡ , π₂ ∘ assocˡ ⟩ ⟩
        ≈˘⟨ ⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘ ⟩
      ⟨ (π₁ ∘ π₁) ∘ assocˡ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ assocˡ ⟩
        ≈˘⟨ ⟨⟩∘ ⟩
      assocˡ ∘ assocˡ
        ∎
    }

  module monoidal = Monoidal monoidal
  open monoidal using (_⊗₁_)

  open Sym monoidal

  symmetric : Symmetric
  symmetric = symmetricHelper record
    { braiding    = record
      { F⇒G = ntHelper record
        { η       = λ _ → swap
        ; commute = λ _ → swap∘⁂
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → swap
        ; commute = λ _ → swap∘⁂
        }
      ; iso = λ _ → record
        { isoˡ = swap∘swap
        ; isoʳ = swap∘swap
        }
      }
    ; commutative = swap∘swap
    ; hexagon     = begin
        id ⊗₁ swap ∘ assocˡ ∘ swap ⊗₁ id                          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congʳ ⟨⟩∘ ⟩
        id ⊗₁ swap ∘ assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₁ ∘ π₁ ⟩ , id ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
        id ⊗₁ swap ∘ ⟨ π₂ ∘ π₁ , ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩          ≈⟨ ⁂∘⟨⟩ ⟩
        ⟨ id ∘ π₂ ∘ π₁ , swap ∘ ⟨ π₁ ∘ π₁ , id ∘ π₂ ⟩ ⟩           ≈⟨ ⟨⟩-cong₂ identityˡ swap∘⟨⟩ ⟩
        ⟨ π₂ ∘ π₁ , ⟨ id ∘ π₂ , π₁ ∘ π₁ ⟩ ⟩                       ≈⟨ ⟨⟩-congˡ (⟨⟩-congʳ identityˡ) ⟩
        ⟨ π₂ ∘ π₁ , ⟨ π₂ , π₁ ∘ π₁ ⟩ ⟩                            ≈˘⟨ assocˡ∘⟨⟩ ⟩
        assocˡ ∘ ⟨ ⟨ π₂ ∘ π₁ , π₂ ⟩ , π₁ ∘ π₁ ⟩                   ≈˘⟨ refl ⟩∘⟨ swap∘⟨⟩ ⟩
        assocˡ ∘ swap ∘ assocˡ                                    ∎
    }

  module symmetric = Symmetric symmetric
  open symmetric public

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
open import Agda.Builtin.List
open import Agda.Builtin.Char

foo : Char → List Char
foo c = c ∷ []

case-split-test : List Char → List Char
case-split-test ('-' ∷ ls) with (foo '+')
... | foo-ls = {!foo-ls!}
case-split-test ls = ls

-- WAS: case splitting on foo-ls produces:
--   case-split-test (.'-' ∷ ls) | [] = ?
--   case-split-test (.'-' ∷ ls) | x ∷ foo-ls = ?
-- SHOULD: not put dots in front of literal patterns:
--   case-split-test ('-' ∷ ls) | [] = {!!}
--   case-split-test ('-' ∷ ls) | x ∷ foo-ls = {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
-- Jesper, Andreas, 2018-10-29, issue #3332
--
-- WAS: With-inlining failed in termination checker
-- due to a DontCare protecting the clause bodies
-- (introduced by Prop).

{-# OPTIONS --prop #-}

data _≡_ {A : Set} (a : A) : A → Prop where
  refl : a ≡ a
{-# BUILTIN EQUALITY _≡_ #-}

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

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

test : {A : Set} (l : List A) → (l ++ []) ≡ l
test [] = refl
test (x ∷ xs) rewrite test xs = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module UniDB.Morph.Sum where

open import UniDB.Spec

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

data Sum (Ξ Ζ : MOR) (γ₁ γ₂ : Dom) : Set where
  inl : Ξ γ₁ γ₂ → Sum Ξ Ζ γ₁ γ₂
  inr : Ζ γ₁ γ₂ → Sum Ξ Ζ γ₁ γ₂

instance
  iUpSum : {Ξ Ζ : MOR} {{upΞ : Up Ξ}} {{upΖ : Up Ζ}} → Up (Sum Ξ Ζ)
  _↑₁ {{iUpSum}} (inl ξ) = inl (ξ ↑₁)
  _↑₁ {{iUpSum}} (inr ζ) = inr (ζ ↑₁)
  _↑_ {{iUpSum}} ξ 0 = ξ
  _↑_ {{iUpSum}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpSum}} ξ = refl
  ↑-suc {{iUpSum}} ξ δ⁺ = refl

  iLkSum :
    {T : STX}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} →
    Lk T (Sum Ξ Ζ)
  lk {{iLkSum {T} {Ξ} {Ζ}}} (inl ξ) i = lk {T} {Ξ} ξ i
  lk {{iLkSum {T} {Ξ} {Ζ}}} (inr ζ) i = lk {T} {Ζ} ζ i

  iLkUpSum :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{upΞ : Up Ξ}} {{lkUpTΞ : LkUp T Ξ}}
    {Ζ : MOR} {{lkTΖ : Lk T Ζ}} {{upΖ : Up Ζ}} {{lkUpTΖ : LkUp T Ζ}} →
    LkUp T (Sum Ξ Ζ)
  lk-↑₁-zero {{iLkUpSum {T} {Ξ} {Ζ}}} (inl ξ) = lk-↑₁-zero {T} {Ξ} ξ
  lk-↑₁-zero {{iLkUpSum {T} {Ξ} {Ζ}}} (inr ζ) = lk-↑₁-zero {T} {Ζ} ζ
  lk-↑₁-suc {{iLkUpSum {T} {Ξ} {Ζ}}} (inl ξ) = lk-↑₁-suc {T} {Ξ} ξ
  lk-↑₁-suc {{iLkUpSum {T} {Ξ} {Ζ}}} (inr ζ) = lk-↑₁-suc {T} {Ζ} ζ

module _
  (Ξ Ζ : MOR) {{upΞ : Up Ξ}} {{upΖ : Up Ζ}}
  where

  inl-↑ : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (δ : Dom) →
    inl {Ξ} {Ζ} ξ ↑ δ ≡ inl (ξ ↑ δ)
  inl-↑ ξ zero    rewrite ↑-zero ξ              = refl
  inl-↑ ξ (suc δ) rewrite inl-↑ ξ δ | ↑-suc ξ δ = refl

  inr-↑ : {γ₁ γ₂ : Dom} (ζ : Ζ γ₁ γ₂) (δ : Dom) →
    inr {Ξ} {Ζ} ζ ↑ δ ≡ inr (ζ ↑ δ)
  inr-↑ ζ zero    rewrite ↑-zero ζ              = refl
  inr-↑ ζ (suc δ) rewrite inr-↑ ζ δ | ↑-suc ζ δ = refl

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how Algebra.CommutativeMonoidSolver can be used
------------------------------------------------------------------------

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

module Algebra.Solver.CommutativeMonoid.Example where

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

open import Data.Bool.Base using (_∨_)
open import Data.Bool.Properties using (∨-commutativeMonoid)

open import Data.Fin using (zero; suc)
open import Data.Vec using ([]; _∷_)

open import Algebra.Solver.CommutativeMonoid ∨-commutativeMonoid

test : ∀ x y z → (x ∨ y) ∨ (x ∨ z) ≡ (z ∨ y) ∨ (x ∨ x)
test a b c = let _∨_ = _⊕_ in
  prove 3 ((x ∨ y) ∨ (x ∨ z)) ((z ∨ y) ∨ (x ∨ x)) (a ∷ b ∷ c ∷ [])
  where
  x = var zero
  y = var (suc zero)
  z = var (suc (suc zero))


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Nat.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat.Base
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq

private
  variable
    l m n : ℕ

min : ℕ → ℕ → ℕ
min zero m = zero
min (suc n) zero = zero
min (suc n) (suc m) = suc (min n m)

minComm : (n m : ℕ) → min n m ≡ min m n
minComm zero zero = refl
minComm zero (suc m) = refl
minComm (suc n) zero = refl
minComm (suc n) (suc m) = cong suc (minComm n m)

max : ℕ → ℕ → ℕ
max zero m = m
max (suc n) zero = suc n
max (suc n) (suc m) = suc (max n m)

maxComm : (n m : ℕ) → max n m ≡ max m n
maxComm zero zero = refl
maxComm zero (suc m) = refl
maxComm (suc n) zero = refl
maxComm (suc n) (suc m) = cong suc (maxComm n m)

znots : ¬ (0 ≡ suc n)
znots eq = subst (caseNat ℕ ⊥) eq 0

snotz : ¬ (suc n ≡ 0)
snotz eq = subst (caseNat ⊥ ℕ) eq 0

injSuc : suc m ≡ suc n → m ≡ n
injSuc p = cong predℕ p

discreteℕ : Discrete ℕ
discreteℕ zero zero = yes refl
discreteℕ zero (suc n) = no znots
discreteℕ (suc m) zero = no snotz
discreteℕ (suc m) (suc n) with discreteℕ m n
... | yes p = yes (cong suc p)
... | no p = no (λ x → p (injSuc x))

isSetℕ : isSet ℕ
isSetℕ = Discrete→isSet discreteℕ

-- Arithmetic facts about predℕ

suc-predℕ : ∀ n → ¬ n ≡ 0 → n ≡ suc (predℕ n)
suc-predℕ zero p = ⊥.rec (p refl)
suc-predℕ (suc n) p = refl

-- Arithmetic facts about +

+-zero : ∀ m → m + 0 ≡ m
+-zero zero = refl
+-zero (suc m) = cong suc (+-zero m)

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm m zero = +-zero m
+-comm m (suc n) = (+-suc m n) ∙ (cong suc (+-comm m n))

-- Addition is associative
+-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
+-assoc zero _ _    = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

inj-m+ : m + l ≡ m + n → l ≡ n
inj-m+ {zero} p = p
inj-m+ {suc m} p = inj-m+ (injSuc p)

inj-+m : l + m ≡ n + m → l ≡ n
inj-+m {l} {m} {n} p = inj-m+ ((+-comm m l) ∙ (p ∙ (+-comm n m)))

m+n≡n→m≡0 : m + n ≡ n → m ≡ 0
m+n≡n→m≡0 {n = zero} = λ p → (sym (+-zero _)) ∙ p
m+n≡n→m≡0 {n = suc n} p = m+n≡n→m≡0 (injSuc ((sym (+-suc _ n)) ∙ p))

m+n≡0→m≡0×n≡0 : m + n ≡ 0 → (m ≡ 0) × (n ≡ 0)
m+n≡0→m≡0×n≡0 {zero} = refl ,_
m+n≡0→m≡0×n≡0 {suc m} p = ⊥.rec (snotz p)

-- Arithmetic facts about ·

0≡m·0 : ∀ m → 0 ≡ m · 0
0≡m·0 zero = refl
0≡m·0 (suc m) = 0≡m·0 m

·-suc : ∀ m n → m · suc n ≡ m + m · n
·-suc zero n = refl
·-suc (suc m) n
  = cong suc
  ( n + m · suc n ≡⟨ cong (n +_) (·-suc m n) ⟩
    n + (m + m · n) ≡⟨ +-assoc n m (m · n) ⟩
    (n + m) + m · n ≡⟨ cong (_+ m · n) (+-comm n m) ⟩
    (m + n) + m · n ≡⟨ sym (+-assoc m n (m · n)) ⟩
    m + (n + m · n) ∎
  )

·-comm : ∀ m n → m · n ≡ n · m
·-comm zero n = 0≡m·0 n
·-comm (suc m) n = cong (n +_) (·-comm m n) ∙ sym (·-suc n m)

·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
·-distribʳ zero _ _ = refl
·-distribʳ (suc m) n o = sym (+-assoc o (m · o) (n · o)) ∙ cong (o +_) (·-distribʳ m n o)

·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
·-distribˡ o m n = (λ i → ·-comm o m i + ·-comm o n i) ∙ ·-distribʳ m n o ∙ ·-comm (m + n) o

·-assoc : ∀ m n o → m · (n · o) ≡ (m · n) · o
·-assoc zero _ _ = refl
·-assoc (suc m) n o = cong (n · o +_) (·-assoc m n o) ∙ ·-distribʳ n (m · n) o

·-identityˡ : ∀ m → 1 · m ≡ m
·-identityˡ m = +-zero m

·-identityʳ : ∀ m → m · 1 ≡ m
·-identityʳ zero = refl
·-identityʳ (suc m) = cong suc (·-identityʳ m)

0≡n·sm→0≡n : 0 ≡ n · suc m → 0 ≡ n
0≡n·sm→0≡n {n = zero} p = refl
0≡n·sm→0≡n {n = suc n} p = ⊥.rec (znots p)

inj-·sm : l · suc m ≡ n · suc m → l ≡ n
inj-·sm {zero} {m} {n} p = 0≡n·sm→0≡n p
inj-·sm {l} {m} {zero} p = sym (0≡n·sm→0≡n (sym p))
inj-·sm {suc l} {m} {suc n} p = cong suc (inj-·sm (inj-m+ {m = suc m} p))

inj-sm· : suc m · l ≡ suc m · n → l ≡ n
inj-sm· {m} {l} {n} p = inj-·sm (·-comm l (suc m) ∙ p ∙ ·-comm (suc m) n)

-- Arithmetic facts about ∸

zero∸ : ∀ n → zero ∸ n ≡ zero
zero∸ zero = refl
zero∸ (suc _) = refl

∸-cancelˡ : ∀ k m n → (k + m) ∸ (k + n) ≡ m ∸ n
∸-cancelˡ zero    = λ _ _ → refl
∸-cancelˡ (suc k) = ∸-cancelˡ k

∸-cancelʳ : ∀ m n k → (m + k) ∸ (n + k) ≡ m ∸ n
∸-cancelʳ m n k = (λ i → +-comm m k i ∸ +-comm n k i) ∙ ∸-cancelˡ k m n

∸-distribʳ : ∀ m n k → (m ∸ n) · k ≡ m · k ∸ n · k
∸-distribʳ m       zero    k = refl
∸-distribʳ zero    (suc n) k = sym (zero∸ (k + n · k))
∸-distribʳ (suc m) (suc n) k = ∸-distribʳ m n k ∙ sym (∸-cancelˡ k (m · k) (n · k))

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


text:
-- TODO: Move some of the proofs from Function.Iteration.Proofs to here so that (_^_) on functions, natural numbers and integers can be generalised.

-- TODO: Maybe something like this
record Iteration(f)(id)(repeat : I → Y) where
  field
    𝟎 : I
    repeat-𝟎 : repeat 𝟎 ≡ id

  record Successor(𝐒 : I → I) where
    field proof : repeat(𝐒(i)) ≡ f(repeat(i))

  record Predecessor(𝐏 : I → I) where
    field proof : f(repeat(𝐏(i))) ≡ repeat(i)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module #7 where

{-
Exercise 1.7. Give an alternative derivation of ind′=A from ind=A which avoids the use of universes.
(This is easiest using concepts from later chapters.)
-}

open import Relation.Binary.PropositionalEquality

ind'₌A : ∀{a}{A : Set a} → (C : (x y : A) → (x ≡ y) → Set) → ((x : A) → C x x refl) → (x y : A) → (p : x ≡ y) → C x y p
ind'₌A = {!!}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module SemiLattice where

open import Prelude
open import PartialOrder as PO
import Chain

private
 module IsSemiLat
   {A : Set}(po : PartialOrder A)(_⊓_ : A -> A -> A) where
  private open module PO = PartialOrder po

  record IsSemiLattice : Set where
    field
      ⊓-lbL : forall {x y}   -> (x ⊓ y) ≤ x
      ⊓-lbR : forall {x y}   -> (x ⊓ y) ≤ y
      ⊓-glb : forall {x y z} -> z ≤ x -> z ≤ y -> z ≤ (x ⊓ y)

open IsSemiLat public

record SemiLattice (A : Set) : Set1 where
  field
    po  : PartialOrder A
    _⊓_ : A -> A -> A
    prf : IsSemiLattice po _⊓_

module SemiLat {A : Set}(L : SemiLattice A) where

  private module SL   = SemiLattice L
  private module SLPO = POrder SL.po
  private module IsSL = IsSemiLattice SL.po SL._⊓_ SL.prf

  open SLPO public
  open SL   public hiding (prf)
  open IsSL public

  private open module C≤ = Chain _≤_ (\x -> ≤-refl) (\x y z -> ≤-trans)
                      renaming (_===_ to _-≤-_; chain>_ to trans>_)

  ⊓-commute : forall {x y} -> (x ⊓ y) == (y ⊓ x)
  ⊓-commute = ≤-antisym lem lem
    where
      lem : forall {x y} -> (x ⊓ y) ≤ (y ⊓ x)
      lem = ⊓-glb ⊓-lbR ⊓-lbL

  ⊓-assoc : forall {x y z} -> (x ⊓ (y ⊓ z)) == ((x ⊓ y) ⊓ z)
  ⊓-assoc = ≤-antisym lem₁ lem₂
    where
      lem₁ : forall {x y z} -> (x ⊓ (y ⊓ z)) ≤ ((x ⊓ y) ⊓ z)
      lem₁ = ⊓-glb (⊓-glb ⊓-lbL (≤-trans ⊓-lbR ⊓-lbL))
                   (≤-trans ⊓-lbR ⊓-lbR)

      lem₂ : forall {x y z} ->  ((x ⊓ y) ⊓ z) ≤ (x ⊓ (y ⊓ z))
      lem₂ = ⊓-glb (≤-trans ⊓-lbL ⊓-lbL)
                   (⊓-glb (≤-trans ⊓-lbL ⊓-lbR) ⊓-lbR)

  ⊓-idem : forall {x} -> (x ⊓ x) == x
  ⊓-idem = ≤-antisym ⊓-lbL (⊓-glb ≤-refl ≤-refl)

  ≤⊓-L : forall {x y} -> (x ≤ y) ⇐⇒ ((x ⊓ y) == x)
  ≤⊓-L = (fwd , bwd)
    where
      fwd = \x≤y -> ≤-antisym ⊓-lbL (⊓-glb ≤-refl x≤y)
      bwd = \x⊓y=x -> ≤-trans (==≤-R x⊓y=x) ⊓-lbR

  ≤⊓-R : forall {x y} -> (y ≤ x) ⇐⇒ ((x ⊓ y) == y)
  ≤⊓-R {x}{y} = (fwd , bwd)
    where
      lem : (y ≤ x) ⇐⇒ ((y ⊓ x) == y)
      lem = ≤⊓-L

      fwd = \y≤x -> ==-trans ⊓-commute (fst lem y≤x)
      bwd = \x⊓y=y -> snd lem (==-trans ⊓-commute x⊓y=y)

  ⊓-monotone-R : forall {a} -> Monotone (\x -> a ⊓ x)
  ⊓-monotone-R x≤y = ⊓-glb ⊓-lbL (≤-trans ⊓-lbR x≤y)

  ⊓-monotone-L : forall {a} -> Monotone (\x -> x ⊓ a)
  ⊓-monotone-L {a}{x}{y} x≤y =
    trans> x ⊓ a
       -≤- a ⊓ x  by ==≤-L ⊓-commute
       -≤- a ⊓ y  by ⊓-monotone-R x≤y
       -≤- y ⊓ a  by ==≤-L ⊓-commute

  ≤⊓-compat : forall {w x y z} -> w ≤ y -> x ≤ z -> (w ⊓ x) ≤ (y ⊓ z)
  ≤⊓-compat {w}{x}{y}{z} w≤y x≤z =
    trans> w ⊓ x
       -≤- w ⊓ z  by ⊓-monotone-R x≤z
       -≤- y ⊓ z  by ⊓-monotone-L w≤y

  ⊓-cong : forall {w x y z} -> w == y -> x == z -> (w ⊓ x) == (y ⊓ z)
  ⊓-cong wy xz = ≤-antisym (≤⊓-compat (==≤-L wy) (==≤-L xz))
                           (≤⊓-compat (==≤-R wy) (==≤-R xz))

  ⊓-cong-L : forall {x y z} -> x == y -> (x ⊓ z) == (y ⊓ z)
  ⊓-cong-L xy = ⊓-cong xy ==-refl

  ⊓-cong-R : forall {x y z} -> x == y -> (z ⊓ x) == (z ⊓ y)
  ⊓-cong-R xy = ⊓-cong ==-refl xy

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.Kernel where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.CommRing.Ideal using (IdealsIn; Ideal→CommIdeal)
open import Cubical.Algebra.Ring.Kernel using () renaming (kernelIdeal to ringKernelIdeal)

private
  variable
    ℓ : Level

-- If R and S were implicit, their ·Comm component could (almost?) never be inferred.
kernelIdeal : (R S : CommRing ℓ) (f : CommRingHom R S) → IdealsIn R
kernelIdeal _ _ f = Ideal→CommIdeal (ringKernelIdeal f)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --rewriting #-}
module DualContractive where

open import Data.Fin
open import Data.Maybe
open import Data.Nat hiding (_≤_ ; compare) renaming (_+_ to _+ℕ_)
open import Data.Nat.Properties
open import Data.Sum hiding (map)
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding (Extensionality)

open import Function

open import Direction

open import Extensionality

open import Max hiding (n)

----------------------------------------------------------------------
-- see also https://github.com/zmthy/recursive-types/tree/ftfjp16
-- for encoding of recursive types

variable
  m n : ℕ
  i i' j : Fin n

----------------------------------------------------------------------
-- lemmas for rewriting

n+1=suc-n : n +ℕ 1 ≡ suc n
n+1=suc-n {zero} = refl
n+1=suc-n {suc n} = cong suc (n+1=suc-n {n})

n+0=n : n +ℕ 0 ≡ n
n+0=n {zero} = refl
n+0=n {suc n} = cong suc (n+0=n {n})

n+sucm=sucn+m : ∀ n m → n +ℕ suc m ≡ suc (n +ℕ m)
n+sucm=sucn+m 0F m = refl
n+sucm=sucn+m (suc n) m = cong suc (n+sucm=sucn+m n m)

{-# REWRITE n+sucm=sucn+m #-}

open import Agda.Builtin.Equality.Rewrite

----------------------------------------------------------------------
-- auxiliaries for automatic rewriting

{- REWRITE n+1=suc-n #-}

{-# REWRITE n+0=n #-}

-- inject+0-x=x : {x : Fin m} → inject+ 0 x ≡ x
-- inject+0-x=x {x = zero} = refl
-- inject+0-x=x {x = suc x} = cong suc inject+0-x=x

{- REWRITE inject+0-x=x #-}

----------------------------------------------------------------------
-- types and session types

data TType (n : ℕ) : Set
data SType (n : ℕ) : Set

data TType n where
  TInt : TType n
  TChn : (S : SType n) → TType n

data SType n where
  xmt : (d : Dir) (T : TType n) (S : SType n) → SType n
  end : SType n
  rec : (S : SType (suc n)) → SType n
  var : (x : Fin n) → SType n

variable
  t T : TType n
  s s₀ S S₀ : SType n

----------------------------------------------------------------------
module Examples-Types where
  sint : SType n → SType n
  sint = xmt SND TInt

  -- μ X. !Int. X
  s1 : SType 0
  s1 = rec (sint (var 0F))

  -- μ X. μ Y. !Int. Y
  s2 : SType 0
  s2 = rec (rec (sint (var 0F)))

  -- μ X. μ Y. !Int. X
  s2a : SType 0
  s2a = rec (rec (sint (var 1F)))

  -- μ X. !Int. μ Y. X
  s3 : SType 0
  s3 = rec (sint (rec (var 1F)))

----------------------------------------------------------------------
-- weakening

increase : ∀ m → (x : Fin n) → Fin (n +ℕ m)
increase 0F x = x
increase (suc m) x = suc (increase m x)

increaseS : ∀ m → SType n → SType (n +ℕ m)
increaseT : ∀ m → TType n → TType (n +ℕ m)

increaseS m (xmt d t s) = xmt d (increaseT m t) (increaseS m s)
increaseS m (rec s) = rec (increaseS m s)
increaseS m (var x) = var (inject+ m x)
increaseS m end = end

increaseT m TInt = TInt
increaseT m (TChn s) = TChn (increaseS m s)

weakenS : ∀ m → SType n → SType (n +ℕ m)
weakenT : ∀ m → TType n → TType (n +ℕ m)

weakenS m (xmt d t s) = xmt d (weakenT m t) (weakenS m s)
weakenS m (rec s) = rec (weakenS m s)
weakenS m (var x) = var (increase m x)
weakenS m end = end

weakenT m TInt = TInt
weakenT m (TChn s) = TChn (weakenS m s)

weaken1S : SType n → SType (suc n)
weaken1S s = weakenS 1 s

----------------------------------------------------------------------
-- substitution

ssubst : SType (suc n) → Fin (suc n) → SType 0 → SType n
tsubst : TType (suc n) → Fin (suc n) → SType 0 → TType n

ssubst (xmt d t s) i s0 = xmt d (tsubst t i s0) (ssubst s i s0)
ssubst (rec s) i s0 = rec (ssubst s (suc i) s0)
ssubst {n} (var 0F) 0F s0 = increaseS n s0
ssubst {suc n} (var 0F) (suc i) s0 = var 0F
ssubst (var (suc x)) 0F s0 = var x
ssubst {suc n} (var (suc x)) (suc i) s0 = increaseS 1 (ssubst (var x) i s0)
ssubst end i s0 = end

tsubst TInt i s₀ = TInt
tsubst (TChn s) i s₀ = TChn (ssubst s i s₀)

----------------------------------------------------------------------
-- contractivity

mutual
  data ContractiveT : TType n → Set where
    con-int : ContractiveT{n} TInt
    con-chn : Contractive 0F S → ContractiveT (TChn S)

  data Contractive (i : Fin (suc n)) : SType n → Set where
    con-xmt : ContractiveT t → Contractive 0F s → Contractive i (xmt d t s)
    con-end : Contractive i end
    con-rec : Contractive (suc i) S → Contractive i (rec S)
    con-var : i ≤ inject₁ j → Contractive i (var j)

----------------------------------------------------------------------
module Examples-Contractivity where
  open Examples-Types

  cn1 : ¬ Contractive {2} 1F (var 0F)
  cn1 (con-var ())

  cp1 : Contractive {2} 0F (var 1F)
  cp1 = con-var z≤n

  cp0 : Contractive {2} 0F (var 0F)
  cp0 = con-var z≤n

  cs1 : Contractive 0F s1
  cs1 = con-rec (con-xmt con-int (con-var z≤n))

  cs2 : Contractive 0F s2
  cs2 = con-rec (con-rec (con-xmt con-int (con-var z≤n)))

  cs2a : Contractive 0F s2a
  cs2a = con-rec (con-rec (con-xmt con-int (con-var z≤n)))

  sp2 : SType 0
  sp2 = s3

  cp2 : Contractive 0F sp2
  cp2 = con-rec (con-xmt con-int (con-rec (con-var (s≤s z≤n))))

  sn2 : SType 0
  sn2 = (rec (xmt SND TInt (rec (var 0F))))

  cn2 : ¬ Contractive 0F sn2
  cn2 (con-rec (con-xmt con-int (con-rec (con-var ()))))

----------------------------------------------------------------------
-- unfolding to first non-rec constructor

unfold : (s : SType n) (c : Contractive i s) (σ : SType n → SType 0) → SType 0
unfold (xmt d t s) (con-xmt ct c) σ = σ (xmt d t s)
unfold end con-end σ = end
unfold (rec s) (con-rec c) σ = unfold s c (σ ∘ λ sn' → ssubst sn' 0F (σ (rec s)))
unfold {i = 0F} (var x) (con-var z≤n) σ = σ (var x)
unfold {i = suc i} (var 0F) (con-var ()) σ
unfold {i = suc i} (var (suc x)) (con-var (s≤s x₁)) σ = unfold (var x) (con-var x₁) (σ ∘ increaseS 1)

unfold₀ : (S : SType 0) (c : Contractive 0F S) → SType 0
unfold₀ S c = unfold S c id

----------------------------------------------------------------------
module Examples-Unfold where
  open Examples-Types

  c1 : Contractive 0F s1
  c1 = con-rec (con-xmt con-int (con-var z≤n))
  s11 : SType 0
  s11 = xmt SND TInt s1

  u-s1=s11 : unfold s1 c1 id ≡ s11
  u-s1=s11 = refl

  c2 : Contractive 0F s2
  c2 = con-rec (con-rec (con-xmt con-int (con-var z≤n)))
  u-s2=s11 : unfold s2 c2 id ≡ s11
  u-s2=s11 = cong (xmt SND TInt) (cong rec (cong (xmt SND TInt) refl))
----------------------------------------------------------------------
-- contractivity is decidable

infer-contractiveT : (t : TType n) → Dec (ContractiveT t)
infer-contractive : (s : SType n) (i : Fin (suc n)) → Dec (Contractive i s)

infer-contractiveT TInt = yes con-int
infer-contractiveT (TChn s)
  with infer-contractive s 0F
infer-contractiveT (TChn s) | yes p = yes (con-chn p)
infer-contractiveT (TChn s) | no ¬p = no (λ { (con-chn cs) → ¬p cs })

infer-contractive (xmt d t s) i
  with infer-contractiveT t | infer-contractive s 0F
infer-contractive (xmt d t s) i | yes p | yes p₁ = yes (con-xmt p p₁)
infer-contractive (xmt d t s) i | yes p | no ¬p = no (λ { (con-xmt ct cs) → ¬p cs })
infer-contractive (xmt d t s) i | no ¬p | yes p = no (λ { (con-xmt ct cs) → ¬p ct })
infer-contractive (xmt d t s) i | no ¬p | no ¬p₁ = no (λ { (con-xmt ct cs) → ¬p₁ cs})
infer-contractive end i = yes con-end
infer-contractive (rec s) i
  with infer-contractive s (suc i)
infer-contractive (rec s) i | yes p = yes (con-rec p)
infer-contractive (rec s) i | no ¬p = no (λ { (con-rec c) → ¬p c })
infer-contractive (var x) 0F = yes (con-var z≤n)
infer-contractive (var 0F) (suc i) = no (λ { (con-var ()) })
infer-contractive (var (suc x)) (suc i)
  with infer-contractive (var x) i
infer-contractive (var (suc x)) (suc i) | yes (con-var x₁) = yes (con-var (s≤s x₁))
infer-contractive (var (suc x)) (suc i) | no ¬p = no (λ { (con-var (s≤s y)) → ¬p (con-var y) })

----------------------------------------------------------------------
module Examples-Inference where
  open Examples-Contractivity

  infer-p2 : infer-contractive sp2 0F ≡ yes cp2
  infer-p2 = refl

  infer-n2 : infer-contractive sn2 0F ≡ no cn2
  infer-n2 = cong no (ext (λ { (con-rec (con-xmt con-int (con-rec (con-var ())))) }))

----------------------------------------------------------------------
-- RT: if a type is contractive at level i, then it is also contractive at any smaller level

c-weakenS : {S : SType n} (i' : Fin′ i) → Contractive i S → Contractive (inject i') S
c-weakenS i' (con-rec cis) = con-rec (c-weakenS (suc i') cis)
c-weakenS i' (con-xmt x cis) = con-xmt x cis
c-weakenS i' con-end = con-end
c-weakenS {i = suc i} i' (con-var {0F} ())
c-weakenS {i = suc i} 0F (con-var {suc n} (s≤s x)) = con-var z≤n
c-weakenS {i = suc i} (suc i') (con-var {suc n} (s≤s x)) = con-var (s≤s (trans-< x))

c-weakenS₁ : {S : SType n} → Contractive (suc i) S → Contractive (inject₁ i) S
c-weakenS₁ (con-rec cis) = con-rec (c-weakenS₁ cis)
c-weakenS₁ (con-xmt x cis) = con-xmt x cis
c-weakenS₁ con-end = con-end
c-weakenS₁ {0F} {()} (con-var x)
c-weakenS₁ {suc n} {0F} (con-var x) = con-var z≤n
c-weakenS₁ {suc n} {suc i} (con-var x) = con-var (pred-≤ x)

c-weakenS! : {S : SType n} → Contractive i S → Contractive 0F S
c-weakenS! {i = 0F} (con-rec cis) = con-rec cis
c-weakenS! {i = suc i} (con-rec cis) = con-rec (c-weakenS 1F cis)
c-weakenS! {n} {i} (con-xmt x cis) = con-xmt x cis
c-weakenS! {n} {i} con-end = con-end
c-weakenS! {n} {i} (con-var x) = con-var z≤n

----------------------------------------------------------------------
-- single substitution of j ↦ Sj

subst1T : (T : TType (suc n)) (j : Fin (suc n)) (Sj : SType n) → TType n
subst1S : (S : SType (suc n)) (j : Fin (suc n)) (Sj : SType n) → SType n

subst1T TInt j Sj = TInt
subst1T (TChn S) j Sj = TChn (subst1S S j Sj)

subst1S (xmt d T S) j Sj = xmt d (subst1T T j Sj) (subst1S S j Sj)
subst1S end j Sj = end
subst1S (rec S) j Sj = rec (subst1S S (suc j) (weaken1S Sj))
subst1S (var x) j Sj
  with compare x j
subst1S (var .(inject least)) j Sj | less .j least = var (inject! least)
subst1S (var x) .x Sj | equal .x = Sj
subst1S (var (suc x)) .(inject least) Sj | greater .(suc x) least = var x

{- the termination checker doesnt like this:
subst1S (var 0F) 0F Sj = Sj
subst1S {suc n} (var 0F) (suc j) Sj = var 0F
subst1S (var (suc x)) 0F Sj = var x
subst1S (var (suc x)) (suc j) Sj = subst1S (var (inject₁ x)) (inject₁ j) Sj
-}

unfold1S : (S : SType 0) → SType 0
unfold1S (xmt d T S) = xmt d T S
unfold1S end = end
unfold1S (rec S) = subst1S S 0F (rec S)

unfoldSS : (S : SType n) → SType n
unfoldSS (xmt d T S) = xmt d T S
unfoldSS end = end
unfoldSS (rec S)
  with unfoldSS S
... | ih = subst1S ih 0F (rec ih)
unfoldSS (var x) = var x

----------------------------------------------------------------------
-- max index substitution

subst-maxT : (Sm : SType n) (T : TType (suc n)) → TType n
subst-maxS : (Sm : SType n) (S : SType (suc n)) → SType n

subst-maxT Sm TInt = TInt
subst-maxT Sm (TChn S) = TChn (subst-maxS Sm S)

subst-maxS Sm (xmt d T S) = xmt d (subst-maxT Sm T) (subst-maxS Sm S)
subst-maxS Sm end = end
subst-maxS Sm (rec S) = rec (subst-maxS (weaken1S Sm) S)
subst-maxS Sm (var x)
  with max? x
subst-maxS Sm (var x) | yes p = Sm
subst-maxS Sm (var x) | no ¬p = var (reduce ¬p)

unfoldmS : (S : SType 0) → SType 0
unfoldmS (xmt d T S) = xmt d T S
unfoldmS end = end
unfoldmS (rec S) = subst-maxS (rec S) S

----------------------------------------------------------------------
-- max substitution preserves contractivity

contr-weakenT : ContractiveT T → ContractiveT (weakenT 1 T)
contr-weakenS : Contractive i S → Contractive (suc i) (weaken1S S)

contr-weakenT con-int = con-int
contr-weakenT (con-chn x) = con-chn (c-weakenS! (contr-weakenS x))

contr-weakenS (con-xmt x cs) = con-xmt (contr-weakenT x) (c-weakenS! (contr-weakenS cs))
contr-weakenS con-end = con-end
contr-weakenS (con-rec cs) = con-rec (contr-weakenS cs)
contr-weakenS {n}{i} {S = var j} (con-var x) = con-var (s≤s x)

subst-contr-mT :
  {T : TType (suc n)} (c : ContractiveT T)
  {S' : SType n} (c' : Contractive i S')
    → ContractiveT (subst-maxT S' T)

subst-contr-mS :
  -- {i : Fin (suc (suc n))}
  {S : SType (suc n)} (c : Contractive (inject₁ i) S)
  {S' : SType n} (c' : Contractive i S')
    → Contractive i (subst-maxS S' S)

subst-contr-mT con-int csm = con-int
subst-contr-mT (con-chn x) csm = con-chn (c-weakenS! (subst-contr-mS x (c-weakenS! csm)))

subst-contr-mS (con-xmt x cs) csm = con-xmt (subst-contr-mT x csm) (subst-contr-mS cs (c-weakenS! csm))
subst-contr-mS con-end csm = con-end
subst-contr-mS (con-rec cs) csm = con-rec (subst-contr-mS cs (contr-weakenS csm))
subst-contr-mS {S = var j} (con-var x) csm
  with max? j
subst-contr-mS {i = _} {var j} (con-var x) csm | yes p = csm
subst-contr-mS {i = _} {var j} (con-var x) csm | no ¬p = con-var (lemma-reduce x ¬p)

-- one step unfolding preserves contractivity

unfold-contr : Contractive i S → Contractive i (unfoldmS S)
unfold-contr (con-xmt x c) = con-xmt x c
unfold-contr con-end = con-end
unfold-contr (con-rec c) = subst-contr-mS (c-weakenS₁ c) (con-rec c)

-- multiple unfolding

unfold! : (S : SType n) (σ : SType n → SType 0) → SType 0
unfold! (xmt d T S) σ = σ (xmt d T S)
unfold! end σ = end
unfold! (rec S) σ = unfold! S (σ ∘ subst-maxS (rec S))
unfold! (var x) σ = σ (var x)

unfold!-contr : Contractive i S → Contractive i (unfold! S id)
unfold!-contr (con-xmt x cs) = con-xmt x cs
unfold!-contr con-end = con-end
unfold!-contr (con-rec cs) = {!!}

-- multiple unfolding preserves contractivity

SCType : (n : ℕ) → Fin (suc n) → Set
SCType n i = Σ (SType n) (Contractive i)

unfold!! : (SC : SCType n i) → (SCType n i → SCType 0 0F) → SCType 0 0F
unfold!! SC@(xmt d T S , con-xmt x cs) σ = σ SC
unfold!! (end , con-end) σ = end , con-end
unfold!! (rec S , con-rec cs) σ =
  unfold!! (S , cs) (σ ∘ λ{ (S' , c') → (subst-maxS (rec S) S') , (subst-contr-mS (c-weakenS₁ c') (con-rec cs)) })
unfold!! SC@(var x , con-var x₁) σ = σ SC

----------------------------------------------------------------------
-- equivalence requires multiple unfolding

variable
  t₁ t₂ t₁' t₂' : TType n
  s₁ s₂ : SType n

-- type equivalence
data EquivT (R : SType n → SType n → Set) : TType n → TType n → Set where
  eq-int  : EquivT R TInt TInt
  eq-chan : R s₁ s₂ → EquivT R (TChn s₁) (TChn s₂)

-- session type equivalence
data EquivS (R : SType n → SType n → Set) : SType n → SType n → Set where
  eq-xmt : (d : Dir) → EquivT R t₁ t₂ → R s₁ s₂ → EquivS R (xmt d t₁ s₁) (xmt d t₂ s₂)
  eq-end : EquivS R end end

-- record Equiv (s₁ s₂ : SType 0) : Set where
--   coinductive
--   field force : EquivS Equiv (unfold s₁) (unfold s₂)

-- open Equiv

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
module _ where

open import Common.Prelude renaming (_+_ to _+N_)
open import Common.Integer

diff : Nat → Nat → Integer
diff  a       zero   = pos a
diff  zero   (suc b) = negsuc b
diff (suc a) (suc b) = diff a b

_+_ : Integer → Integer → Integer
pos    a + pos    b = pos (a +N b)
pos    a + negsuc b = diff a (suc b)
negsuc a + pos    b = diff b (suc a)
negsuc a + negsuc b = negsuc (suc a +N b)

printInt : Integer → IO Unit
printInt n = putStrLn (intToString n)

main : IO Unit
main = printInt (pos 42 + pos 58)     ,,
       printInt (pos 42 + negsuc 141) ,,
       printInt (pos 42 + negsuc 31)  ,,
       printInt (negsuc 42 + pos 143) ,,
       printInt (negsuc 42 + pos 33)  ,,
       printInt (negsuc 42 + negsuc 56)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT renaming (pt to pt⊙)
open import cw.CW

module cw.FinCW where

record AttachedFinSkeleton n (Skel : Type₀) (Real : Skel → Skeleton n) : Type₀ where
  constructor attached-fin-skeleton
  field
    skel : Skel
    numCells : ℕ
    attaching : Attaching ⟦ Real skel ⟧ (Fin numCells) (Sphere n)

FinSkeleton : ℕ → Type₀
FinSkeleton-realize : {n : ℕ} → FinSkeleton n → Skeleton n

FinSkeleton O = ℕ
FinSkeleton (S n) = AttachedFinSkeleton n (FinSkeleton n) FinSkeleton-realize

FinSkeleton-realize {n = O} n = Fin n , Fin-is-set
FinSkeleton-realize {n = S n} (attached-fin-skeleton _ s α) =
  attached-skeleton _ (Fin s , Fin-is-set) α

⦉_⦊ = FinSkeleton-realize

-- Pointedness

-- this function is needed for pointedness
fcw-head : ∀ {n : ℕ} → FinSkeleton n → Type₀
fcw-head = cw-head ∘ FinSkeleton-realize

fcw-head-has-dec-eq : ∀ {n : ℕ} (fin-skel : FinSkeleton n)
  → has-dec-eq (fcw-head fin-skel)
fcw-head-has-dec-eq {n = 0} _ = Fin-has-dec-eq
fcw-head-has-dec-eq {n = S n} (attached-fin-skeleton skel _ _) =
  fcw-head-has-dec-eq skel

-- this function is needed for pointedness
fcw-incl^ : ∀ {n : ℕ} (skel : FinSkeleton n)
  → fcw-head skel → ⟦ ⦉ skel ⦊ ⟧
fcw-incl^ fin-skel = incl^ (FinSkeleton-realize fin-skel)

-- disjointly pointed skeletons
record ⊙FinSkeleton (n : ℕ) : Type₁ where
  constructor ⊙fin-skeleton
  field
    skel : FinSkeleton n
    pt : fcw-head skel

⊙FinSkeleton-realize : {n : ℕ} → ⊙FinSkeleton n → ⊙Skeleton {i = lzero} n
⊙FinSkeleton-realize (⊙fin-skeleton skel pt) =
  ⊙skeleton (FinSkeleton-realize skel) pt (fcw-head-has-dec-eq skel pt)

⊙⦉_⦊ : {n : ℕ} → ⊙FinSkeleton n → ⊙Skeleton {i = lzero} n
⊙⦉_⦊ = ⊙FinSkeleton-realize

-- Take a prefix of a skeleton

fcw-init : ∀ {n} → FinSkeleton (S n) → FinSkeleton n
fcw-init (attached-fin-skeleton skel _ _) = skel

⊙fcw-init : ∀ {n} → ⊙FinSkeleton (S n) → ⊙FinSkeleton n
⊙fcw-init (⊙fin-skeleton skel pt) = ⊙fin-skeleton (fcw-init skel) pt

-- Extra conditions on CW complexes

-- 1. decidable equalities

FinSkeleton-has-cells-with-dec-eq : ∀ {n} (fin-skel : FinSkeleton n)
  → has-cells-with-dec-eq (FinSkeleton-realize fin-skel)
FinSkeleton-has-cells-with-dec-eq {n = O} fin-skel = Fin-has-dec-eq
FinSkeleton-has-cells-with-dec-eq {n = S n} fin-skel =
  FinSkeleton-has-cells-with-dec-eq (fcw-init fin-skel) , Fin-has-dec-eq

⊙FinSkeleton-has-cells-with-dec-eq : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
  → ⊙has-cells-with-dec-eq (⊙FinSkeleton-realize ⊙fin-skel)
⊙FinSkeleton-has-cells-with-dec-eq ⊙fin-skel = FinSkeleton-has-cells-with-dec-eq _

-- 2. choice

FinSkeleton-has-cells-with-choice : ∀ t {n} (fin-skel : FinSkeleton n) j
  → has-cells-with-choice t (FinSkeleton-realize fin-skel) j
FinSkeleton-has-cells-with-choice t {n = O} fin-skel j = Fin-has-choice t j
FinSkeleton-has-cells-with-choice t {n = S n} fin-skel j =
  FinSkeleton-has-cells-with-choice t (fcw-init fin-skel) j , Fin-has-choice t j

⊙FinSkeleton-has-cells-with-choice : ∀ t {n} (fin-skel : ⊙FinSkeleton n) j
  → ⊙has-cells-with-choice t (⊙FinSkeleton-realize fin-skel) j
⊙FinSkeleton-has-cells-with-choice t fin-skel j = FinSkeleton-has-cells-with-choice t _ j

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- binary search trees (not balanced)

open import bool
open import bool-thms2
open import eq
open import maybe
open import product
open import product-thms
open import bool-relations using (transitive ; total)

module bst (A : Set) (_≤A_ : A → A → 𝔹)
           (≤A-trans : transitive _≤A_)
           (≤A-total : total _≤A_) where

open import bool-relations _≤A_ hiding (transitive ; total)
open import minmax _≤A_ ≤A-trans ≤A-total

data bst : A → A → Set where
  bst-leaf : ∀ {l u : A} → l ≤A u ≡ tt → bst l u
  bst-node : ∀ {l l' u' u : A}(d : A) →
               bst l' d → bst d u' →
               l ≤A l' ≡ tt → u' ≤A u ≡ tt →
               bst l u

-- find a node which is isomorphic (_=A_) to d and return it; or else return nothing
bst-search : ∀{l u : A}(d : A) → bst l u → maybe (Σ A (λ d' → d iso𝔹 d' ≡ tt))
bst-search d (bst-leaf _) = nothing
bst-search d (bst-node d' L R _ _) with keep (d ≤A d')
bst-search d (bst-node d' L R _ _) | tt , p1 with keep (d' ≤A d)
bst-search d (bst-node d' L R _ _) | tt , p1 | tt , p2 = just (d' , iso𝔹-intro p1 p2)
bst-search d (bst-node d' L R _ _) | tt , p1 | ff , p2 = bst-search d L
bst-search d (bst-node d' L R _ _) | ff , p1 = bst-search d R

bst-dec-lb : ∀ {l l' u' : A} → bst l' u' → l ≤A l' ≡ tt → bst l u'
bst-dec-lb (bst-leaf p) q = bst-leaf (≤A-trans q p)
bst-dec-lb (bst-node d L R p1 p2) q = bst-node d L R (≤A-trans q p1) p2

bst-inc-ub : ∀ {l' u' u : A} → bst l' u' → u' ≤A u ≡ tt → bst l' u
bst-inc-ub (bst-leaf p) q = bst-leaf (≤A-trans p q)
bst-inc-ub (bst-node d L R p1 p2) q = bst-node d L R p1 (≤A-trans p2 q)

bst-insert : ∀{l u : A}(d : A) → bst l u → bst (min d l) (max d u)
bst-insert d (bst-leaf p) = bst-node d (bst-leaf ≤A-refl) (bst-leaf ≤A-refl) min-≤1 max-≤1
bst-insert d (bst-node d' L R p1 p2) with keep (d ≤A d')
bst-insert d (bst-node d' L R p1 p2) | tt , p with bst-insert d L
bst-insert d (bst-node d' L R p1 p2) | tt , p | L' rewrite p =
  bst-node d' L' (bst-inc-ub R (≤A-trans p2 max-≤2)) (min2-mono p1) ≤A-refl
bst-insert d (bst-node d' L R p1 p2) | ff , p with bst-insert d R
bst-insert d (bst-node d' L R p1 p2) | ff , p | R' rewrite p =
  bst-node d' (bst-dec-lb L p1) R' min-≤2 (max2-mono p2)

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL