text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Equivalence.Strong where

open import Level
open import Relation.Binary using (IsEquivalence)
open import Relation.Nullary using (¬_)
open import Data.Product using (Σ; ∃; _,_; proj₁; proj₂)
open import Function using () renaming (_∘_ to _∙_)

open import Categories.Category
open import Categories.Functor hiding (equiv)
open import Categories.Functor.Properties
import Categories.Morphisms as Morphisms

record StrongEquivalence {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    .full : Full F
    .faithful : Faithful F
    eso : EssentiallySurjective F

record StronglyEquivalent {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    C⇒D : Functor C D
    strong-equivalence : StrongEquivalence C⇒D
  open StrongEquivalence strong-equivalence public

refl : ∀ {o ℓ e} {C : Category o ℓ e} → StronglyEquivalent C C
refl {C = C} = record
  { C⇒D = id
  ; strong-equivalence = record
    { full = λ {X Y} → my-full X Y
    ; faithful = λ _ _ eq → eq
    ; eso = λ d → d , (record { f = C.id; g = C.id; iso = record { isoˡ = C.identityˡ; isoʳ = C.identityˡ } })
    }
  }
  where
  module C = Category C
  open C hiding (id)
  .my-full : ∀ X Y → ¬ Σ (X ⇒ Y) (λ f → ¬ ∃ (λ g → C [ g ≡ f ]))
  my-full X Y (f , elim) = elim (f , Equiv.refl)

sym : ∀ {o ℓ e o′ ℓ′ e′} → {C : Category o ℓ e} {D : Category o′ ℓ′ e′} → StronglyEquivalent C D → StronglyEquivalent D C
sym {C = C} {D = D} Op = record
  { C⇒D = record
    { F₀ = λ d → proj₁ (Op.eso d)
    ; F₁ = λ f → {!rev (proj₂ (Op.eso _)) ∘ f ∘ ?!}
    ; identity = {!!}
    ; homomorphism = {!!}
    ; F-resp-≡ = {!!}
    }
  ; strong-equivalence = record
    { full = {!!}
    ; faithful = {!!}
    ; eso = {!!}
    }
  }
  where
  module Op = StronglyEquivalent Op
  open Op using () renaming (C⇒D to F)
  open Functor F
  open Morphisms._≅_ C renaming (f to fwd; g to rev)

trans : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃} → StronglyEquivalent C₁ C₂ → StronglyEquivalent C₂ C₃ → StronglyEquivalent C₁ C₃
trans {C₁ = C₁} {C₂} {C₃} C₁⇒C₂ C₂⇒C₃ = record
  { C⇒D = G ∘ F
  ; strong-equivalence = record
    { full = λ {X Y} → my-full X Y
    ; faithful = λ f g → C₁⇒C₂.faithful _ _ ∙ C₂⇒C₃.faithful _ _
    ; eso = my-eso }
  }
  where
  module C₁⇒C₂ = StronglyEquivalent C₁⇒C₂
  module C₂⇒C₃ = StronglyEquivalent C₂⇒C₃
  open C₁⇒C₂ using () renaming (C⇒D to F)
  open C₂⇒C₃ using () renaming (C⇒D to G)
  module F = Functor F
  open F using (F₀; F₁)
  module G = Functor G
  open G using () renaming (F₀ to G₀; F₁ to G₁)
  module E = Category.Equiv C₃
  open Morphisms C₃
  .my-full : ∀ X Y → ¬ ∃ (λ f → ¬ ∃ (λ (g : C₁ [ X , Y ]) → C₃ [ G₁ (F₁ g) ≡ f ]))
  my-full X Y (f , elim) = C₂⇒C₃.full (f , lemma)
    where
    lemma : ¬ ∃ (λ h → C₃ [ G₁ h ≡ f ])
    lemma (h , G₁h≡f) = C₁⇒C₂.full (h , lemma₂)
      where
      lemma₂ : ¬ ∃ (λ g → C₂ [ F₁ g ≡ h ])
      lemma₂ (g , F₁g≡h) = elim (g , E.trans (G.F-resp-≡ F₁g≡h) G₁h≡f)
  my-eso : ∀ c₃ → ∃ (λ c₁ → G₀ (F₀ c₁) ≅ c₃)
  my-eso c₃ with C₂⇒C₃.eso c₃
  my-eso c₃ | c₂ , ff₃ with C₁⇒C₂.eso c₂
  my-eso c₃ | c₂ , ff₃ | c₁ , ff₂ = c₁ , (ff₃ ⓘ resp-≅ ff₂)
    where open FunctorsAlways G

equiv : ∀ {o ℓ e} → IsEquivalence (StronglyEquivalent {o} {ℓ} {e})
equiv = record
  { refl = refl
  ; sym = sym
  ; trans = trans
  }


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

open import Cubical.Data.Int hiding (_+_)
open import Cubical.Data.Bool
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.HITs.S1 hiding (inv)
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.Susp
open import Cubical.Data.Unit
open import Cubical.HITs.Join
open import Cubical.HITs.Pushout
open import Cubical.HITs.SmashProduct
open import Cubical.HITs.PropositionalTruncation

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

--- Some silly lemmas on S1 ---

S¹≡S1 : S₊ 1 ≡ S¹
S¹≡S1 = cong Susp (sym (ua Bool≃Susp⊥)) ∙ sym S¹≡SuspBool

isOfHLevelS1 : isOfHLevel 3 (S₊ 1)
isOfHLevelS1 = transport (λ i → isOfHLevel 3 (S¹≡S1 (~ i)))
                          λ x y → J (λ y p → (q : x ≡ y) → isProp (p ≡ q))
                                     (transport (λ i → isSet (basedΩS¹≡Int x (~ i))) isSetInt refl)

isGroupoidS1 : isGroupoid (S₊ 1)
isGroupoidS1 = transport (λ i → isGroupoid (S¹≡S1 (~ i))) isGroupoidS¹

isConnectedS1 : (x : S₊ 1) → ∥ north ≡ x ∥
isConnectedS1 x = rec propTruncIsProp
                       (λ p → ∣ cong (transport (sym (S¹≡S1))) p ∙ transport⁻Transport (S¹≡S1) x ∣)
                       (isConnectedS¹ (transport S¹≡S1 x))

SuspBool→S1 : Susp Bool → S₊ 1
SuspBool→S1 north           = north
SuspBool→S1 south           = south
SuspBool→S1 (merid false i) = merid south i
SuspBool→S1 (merid true i)  = merid north i

S1→SuspBool : S₊ 1 → Susp Bool
S1→SuspBool north           = north
S1→SuspBool south           = south
S1→SuspBool (merid north i) = merid true i
S1→SuspBool (merid south i) = merid false i

SuspBool→S1-sect : section SuspBool→S1 S1→SuspBool
SuspBool→S1-sect north = refl
SuspBool→S1-sect south = refl
SuspBool→S1-sect (merid north i) = refl
SuspBool→S1-sect (merid south i) = refl

SuspBool→S1-retr : retract SuspBool→S1 S1→SuspBool
SuspBool→S1-retr north = refl
SuspBool→S1-retr south = refl
SuspBool→S1-retr (merid false i) = refl
SuspBool→S1-retr (merid true i) = refl

S1→S¹ : S₊ 1 → S¹
S1→S¹ x = SuspBool→S¹ (S1→SuspBool x)

S¹→S1 : S¹ → S₊ 1
S¹→S1 x = SuspBool→S1 (S¹→SuspBool x)

S1→S¹-sect : section S1→S¹ S¹→S1
S1→S¹-sect x =
    cong SuspBool→S¹ (SuspBool→S1-retr (S¹→SuspBool x))
  ∙ S¹→SuspBool→S¹ x

S1→S¹-retr : retract S1→S¹ S¹→S1
S1→S¹-retr x =
    cong SuspBool→S1 (SuspBool→S¹→SuspBool (S1→SuspBool x))
  ∙ SuspBool→S1-sect x

SuspBoolIsoS1 : Iso (Susp Bool) (S₊ 1)
fun SuspBoolIsoS1                      = SuspBool→S1
inv SuspBoolIsoS1                      = S1→SuspBool
rightInv SuspBoolIsoS1 north           = refl
rightInv SuspBoolIsoS1 south           = refl
rightInv SuspBoolIsoS1 (merid north i) = refl
rightInv SuspBoolIsoS1 (merid south i) = refl
leftInv SuspBoolIsoS1 north            = refl
leftInv SuspBoolIsoS1 south            = refl
leftInv SuspBoolIsoS1 (merid false i)  = refl
leftInv SuspBoolIsoS1 (merid true i)   = refl

SuspBool≃S1 : Susp Bool ≃ S₊ 1
SuspBool≃S1 = isoToEquiv SuspBoolIsoS1

-- map between S¹ ∧ A and Susp A.
private
  f' : {a : A} → A → S₊ 1 → Susp A
  f' {a = pt} A north = north
  f' {a = pt} A south = north
  f' {a = pt} a (merid p i) = ((merid a) ∙ sym (merid pt)) i

  proj' : {A : Pointed ℓ} {B : Pointed ℓ'} → typ A → typ B → A ⋀ B
  proj' a b = inr (a , b)

module smashS1→susp {(A , pt) : Pointed ℓ} where
  f : (S₊ 1 , north) ⋀ (A , pt) → (Susp A)
  f (inl tt)                    = north
  f (inr (x , x₁))              = f' {a = pt} x₁ x
  f  (push (inl north) i)       = north
  f (push (inl south) i)        = north
  f (push (inl (merid a i₁)) i) = rCancel (merid pt) (~ i) i₁
  f (push (inr x) i)            = north
  f (push (push tt i₁) i)       = north

  f⁻ : Susp A → (S₊ 1 , north) ⋀ (A , pt)
  f⁻ north = inl tt
  f⁻ south = inl tt
  f⁻ (merid a i) =
    (push (inr a) ∙∙ cong (λ x → proj' {A = S₊ 1 , north} {B = A , pt} x a) (merid south ∙ sym (merid north)) ∙∙ sym (push (inr a))) i

  {- TODO : Prove that they cancel out -}

{- Map used in definition of cup product. Maybe mover there later -}
sphereSmashMap : (n m : ℕ) → (S₊ (suc n) , north) ⋀ (S₊ (suc m) , north) → S₊ (2 + n + m)
sphereSmashMap zero m = smashS1→susp.f
sphereSmashMap (suc n) m =
  smashS1→susp.f ∘
  (idfun∙ _ ⋀→ (sphereSmashMap n m , refl)) ∘
  ⋀-associate ∘
  ((smashS1→susp.f⁻ , refl) ⋀→ idfun∙ _)

ext: agda

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
record SemiRing : Set1 where
  field
    R    : Set
    _+_  : R -> R -> R
    zero : R
    _*_  : R -> R -> R
    one  : R

module Vectors (S : SemiRing) where

  open SemiRing S
  open import Data.Nat renaming (ℕ to Nat; zero to z; _*_ to times; _+_ to plus)
  open import Data.Fin renaming (zero to z) hiding (_+_)
  open import RMonads
  open import Functors.Fin
  open import Data.Bool
  open import Function
  open import Relation.Binary.HeterogeneousEquality

  Vec : Nat -> Set
  Vec n = Fin n -> R

  Matrix : Nat -> Nat -> Set
  Matrix m n = Fin m -> Vec n

  -- unit
  delta : forall {n} -> Matrix n n
  delta i j = if feq i j then one else zero

  transpose : forall {m n} -> Matrix m n -> Matrix n m
  transpose A = λ j i -> A i j

  dot : forall {n} -> Vec n -> Vec n -> R
  dot {z}     x y = zero
  dot {suc n} x y = (x z * y z) + dot (x ∘ suc) (y ∘ suc)

  mult : forall {m n} -> Matrix m n -> Vec m -> Vec n
  mult A x = λ j -> dot (transpose A j) x

  VecRMon : RMonad FinF
  VecRMon = rmonad
    Vec
    delta
    mult
    {!!}
    {!!}
    {!!}

    where
{-
    lem : forall {n}(x : Vec n)(j : Fin n) -> dot (λ i → if feq i j then one else zero) x ≅ x j
    lem {z} x ()
    lem {suc n} x z = {!lem {n} (x ∘ suc) !}
    lem {suc n} x (suc j) = {!!}

 -}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module BBHeap.DropLast {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import BBHeap.Compound _≤_
open import BBHeap.Properties _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.Empty
open import Data.Sum renaming (_⊎_ to _∨_)

mutual
  dropLast : {b : Bound} → BBHeap b → BBHeap b
  dropLast leaf = leaf
  dropLast (left b≤x l⋘r)
      with l⋘r | lemma-dropLast⋘ l⋘r
  ... | lf⋘ | _ = leaf
  ... | ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | inj₁ (≃nd .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ _ l₁≃l₂) =
               let l≃r = ≃nd x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂
               in right b≤x (lemma-dropLast≃ l≃r (cl x≤y₁ l₁⋘r₁))
  ... | lr⋘ _ _ _ _ _ _ | inj₁ ()
  ... | _ | inj₂ dl⋘r = left b≤x dl⋘r
  dropLast (right b≤x l⋙r)
      with lemma-dropLast⋙ l⋙r
  ... | inj₁ l⋗r = left b≤x (lemma-dropLast⋗ l⋗r)
  ... | inj₂ l⋙dr = right b≤x l⋙dr

  lemma-dropLast-⊥ : {b : Bound}{l r : BBHeap b} → l ≃ r → dropLast l ⋘ r → Compound l → ⊥
  lemma-dropLast-⊥ () _ (cr _ _)
  lemma-dropLast-⊥ (≃nd b≤x b≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') dxlr⋘x'l'r' (cl .b≤x .l⋘r)
      with l⋘r | l≃r | l≃l' | l'⋘r' | lemma-dropLast⋘ l⋘r | dxlr⋘x'l'r'
  ... | lf⋘ | ≃lf | _ | _ | _ |  ()
  ... | lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₁≃r₁ l₁⋗l₂ | () | _ | _ | _ | _
  ... | ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _ | ≃nd .x≤y₁ x'≤y'₁ .l₁⋘r₁ l'₁⋘r'₁ _ l'₁≃r'₁ l₁≃r'₁ | ll⋘ .x'≤y'₁ x'≤y'₂ .l'₁⋘r'₁ l'₂⋘r'₂ l'₂≃r'₂ r'₁≃l'₂ | inj₁ (≃nd .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ _ l₁≃l₂) | _dxlr⋘x'l'r'
      with lemma-dropLast≃ (≃nd x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) (cl x≤y₁ l₁⋘r₁) | _dxlr⋘x'l'r'
  ... | l⋙dr | lr⋘ .b≤x .b≤x' .l⋙dr .(ll⋘ x'≤y'₁ x'≤y'₂ l'₁⋘r'₁ l'₂⋘r'₂ l'₂≃r'₂ r'₁≃l'₂) _ l⋗l'
      with lemma-≃-⊥ (≃nd x≤y₁ x'≤y'₁ l₁⋘r₁ l'₁⋘r'₁ l₁≃r₁ l'₁≃r'₁ l₁≃r'₁) l⋗l'
  ... | ()
  lemma-dropLast-⊥ (≃nd b≤x b≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') dxlr⋘x'l'r' (cl .b≤x .l⋘r) | ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | ≃nd .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ _ l₁≃l₂ | _ | _ | inj₂ dl⋘r | _
      with lemma-dropLast-⊥ (≃nd x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) dl⋘r (cl x≤y₁ l₁⋘r₁)
  ... | ()

  lemma-dropLast≃ : {b : Bound}{l r : BBHeap b} → l ≃ r → Compound l → l ⋙ dropLast r
  lemma-dropLast≃ () (cr _ _)
  lemma-dropLast≃ (≃nd b≤x b≤x' l⋘r l'⋘r' l≃r l'≃r' l≃l') (cl .b≤x .l⋘r)
      with l'≃r' | l≃l' | l≃r | l⋘r | l'⋘r' | lemma-dropLast⋘ l'⋘r'
  ... | ≃lf | ≃lf | ≃lf | lf⋘ | lf⋘ | _ = ⋙lf b≤x
  ... | ≃nd x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ _ _ _ | _ | _l≃r | _l⋘r | ll⋘ .x'≤y₁ .x'≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₂≃r₂ _ | inj₁ (≃nd .x'≤y₁ .x'≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ _ l₁≃l₂) =
                 let l'≃r' = ≃nd x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ ;
                      l'⋙dr' = lemma-dropLast≃ l'≃r' (cl x'≤y₁ l₁⋘r₁)
                 in ⋙rr b≤x b≤x' _l⋘r _l≃r l'⋙dr' l≃l'
  ... | ≃nd x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ | _l≃l' | _l≃r | _l⋘r | ll⋘ .x'≤y₁ .x'≤y₂ .l₁⋘r₁ .l₂⋘r₂ _ _ | inj₂ dl'⋘r'
      with lemma-dropLast-⊥ (≃nd x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) dl'⋘r' (cl x'≤y₁ l₁⋘r₁)
  ... | ()

  lemma-dropLast⋗ : {b : Bound}{l r : BBHeap b} → l ⋗ r → dropLast l ⋘ r
  lemma-dropLast⋗ (⋗lf b≤x) = lf⋘
  lemma-dropLast⋗ (⋗nd b≤x b≤x' l⋘r l'⋘r' l≃r l'≃r' l⋗l')
      with l⋘r | l≃r | l⋗l' | lemma-dropLast⋘ l⋘r
  ... | lf⋘ | _ | () | _
  ... | lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₁≃r₁ l₁⋗l₂ | _ | _ | inj₁ ()
  ... | lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₁≃r₁ l₁⋗l₂ | () | _ | inj₂ _
  ... | ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _ | _ | inj₁ (≃nd .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ _ l₁≃l₂) =
                let _l≃r = ≃nd x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ ;
                     l⋙dr = lemma-dropLast≃ _l≃r (cl x≤y₁ l₁⋘r₁)
                in lr⋘ b≤x b≤x' l⋙dr l'⋘r' l'≃r' l⋗l'
  ... | ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ _ r₁≃l₂ | ≃nd .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂ | _ | inj₂ dl⋘r
      with lemma-dropLast-⊥ (≃nd x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) dl⋘r (cl x≤y₁ l₁⋘r₁)
  ... | ()

  lemma-dropLast⋘ : {b : Bound}{l r : BBHeap b} → l ⋘ r → l ≃ r ∨ dropLast l ⋘ r
  lemma-dropLast⋘ lf⋘ = inj₁ ≃lf
  lemma-dropLast⋘ (ll⋘ b≤x b≤x' l⋘r l'⋘r' l'≃r' r≃l')
      with l⋘r | l'⋘r' | r≃l' | lemma-dropLast⋘ l⋘r
  ... | lf⋘ | lf⋘ | ≃lf | _ = inj₁ (≃nd b≤x b≤x' lf⋘ lf⋘ ≃lf ≃lf ≃lf)
  ... | ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _l'⋘r' | _r≃l' | inj₁ l≃r =
               let l≃l' = trans≃ l≃r _r≃l' ;
                    _l⋘r = ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂
               in inj₁ (≃nd b≤x b≤x' _l⋘r _l'⋘r' l≃r l'≃r' l≃l')
  ... | ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _l'⋘r' | _r≃l' | inj₂ dl⋘r = inj₂ (ll⋘ b≤x b≤x' dl⋘r _l'⋘r' l'≃r' _r≃l')
  ... | lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | _l'⋘r' | _r≃l' | inj₁ l≃r =
               let l≃l' = trans≃ l≃r _r≃l' ;
                    _l⋘r = lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂
               in inj₁ (≃nd b≤x b≤x' _l⋘r _l'⋘r' l≃r l'≃r' l≃l')
  ... | lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | _l'⋘r' | _r≃l' | inj₂ dl⋘r = inj₂ (ll⋘ b≤x b≤x' dl⋘r _l'⋘r' l'≃r' _r≃l')
  lemma-dropLast⋘ (lr⋘ b≤x b≤x' l⋙r l'⋘r' l'≃r' l⋗l')
      with lemma-dropLast⋙ l⋙r
  ... | inj₁ l⋗r =
               let dl⋘r = lemma-dropLast⋗ l⋗r ;
                    r≃l' = lemma⋗⋗' l⋗r l⋗l'
               in inj₂ (ll⋘ b≤x b≤x' dl⋘r l'⋘r' l'≃r' r≃l')
  ... | inj₂ l⋙dr = inj₂ (lr⋘ b≤x b≤x' l⋙dr l'⋘r' l'≃r' l⋗l')

  lemma-dropLast⋙ : {b : Bound}{l r : BBHeap b} → l ⋙ r → l ⋗ r ∨ l ⋙ dropLast r
  lemma-dropLast⋙ (⋙lf b≤x) = inj₁ (⋗lf b≤x)
  lemma-dropLast⋙ (⋙rl b≤x b≤x' l⋘r l≃r l'⋘r' l⋗r')
      with l'⋘r' | l≃r | l⋗r' | lemma-dropLast⋘ l'⋘r'
  ... | lf⋘ | ≃nd x≤y _ lf⋘ lf⋘ ≃lf ≃lf ≃lf | ⋗lf .x≤y | _ = inj₁ (⋗nd b≤x b≤x' l⋘r lf⋘ l≃r ≃lf (⋗lf x≤y))
  ... | ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _l≃r | _l⋗r' | inj₁ l'≃r' =
             let l⋗l' = lemma⋗≃ _l⋗r' (sym≃ l'≃r') ;
                  _l'⋘r' = ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂
             in inj₁ (⋗nd b≤x b≤x' l⋘r _l'⋘r' _l≃r l'≃r' l⋗l')
  ... | ll⋘ x'≤y₁ x'≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂ | _l≃r | _l⋗r' | inj₂ dl'⋘r' = inj₂ (⋙rl b≤x b≤x' l⋘r _l≃r dl'⋘r' _l⋗r')
  ... | lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | _l≃r | _l⋗r' | inj₁ l'≃r' =
             let l⋗l' = lemma⋗≃ _l⋗r' (sym≃ l'≃r') ;
                  _l'⋘r' = lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂
             in inj₁ (⋗nd b≤x b≤x' l⋘r _l'⋘r' _l≃r l'≃r' l⋗l')
  ... | lr⋘ x'≤y₁ x'≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | _l≃r | _l⋗r' | inj₂ dl'⋘r' = inj₂ (⋙rl b≤x b≤x' l⋘r _l≃r dl'⋘r' _l⋗r')
  lemma-dropLast⋙ (⋙rr b≤x b≤x' l⋘r l≃r l'⋙r' l≃l')
      with lemma-dropLast⋙ l'⋙r'
  ... | inj₁ l'⋗r' =
               let dl'⋘r' = lemma-dropLast⋗ l'⋗r' ;
                    l⋗r' = lemma≃⋗ l≃l' l'⋗r'
               in inj₂ (⋙rl b≤x b≤x' l⋘r l≃r dl'⋘r' l⋗r')
  ... | inj₂ l'⋙dr' = inj₂ (⋙rr b≤x b≤x' l⋘r l≃r l'⋙dr' l≃l')

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Data.Bin.Props where

  open import Data.Bin
  import Data.Nat
  import Data.Nat.Properties
  open Data.Nat using (ℕ)
  open import Data.List
  open import Relation.Binary.PropositionalEquality
  open import Function using (_⟨_⟩_)
  open import Algebra.Structures using (IsCommutativeMonoid; module IsCommutativeMonoid; module IsCommutativeSemiring)

  import Data.Bin.Addition

  bin-+-is-comm-monoid = Data.Bin.Addition.is-commutativeMonoid

  open import Data.Bin.Bijection using (fromℕ-bijection)

  import Algebra.Lifting
  module Lifting = Algebra.Lifting _ _ fromℕ-bijection

  open import Data.Bin.Multiplication

  bin-*-is-comm-monoid : IsCommutativeMonoid _≡_ _*_ ([] 1#)
  bin-*-is-comm-monoid = lift-isCommutativeMonoid 1 *-isCommutativeMonoid
   where
     open IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using(*-isCommutativeMonoid)
     open Lifting.WithOp₂ Data.Nat._*_ _*_ *-is-multiplication

  open IsCommutativeMonoid bin-*-is-comm-monoid using () renaming (comm to *-comm)

  *2-is-2* : ∀ x → x *2 ≡ (fromℕ 2) * x
  *2-is-2* 0# = refl
  *2-is-2* (bs 1#) = refl

  *-distrib : ∀ {a b c} → (a + b) * c ≡ a * c + b * c
  *-distrib {a} {b} {c} = Data.Bin.Multiplication.*-distribʳ a b c

  *2-distrib : ∀ a b → (a + b) *2 ≡ a *2 + b *2
  *2-distrib a b = *2-is-*2-bin (a + b) ⟨ trans ⟩ *-distrib {a} {b} {fromℕ 2} ⟨ trans ⟩ cong₂ _+_ (sym (*2-is-*2-bin a)) (sym (*2-is-*2-bin b))
   where
    *2-is-*2-bin : ∀ a → a *2 ≡ a * fromℕ 2
    *2-is-*2-bin a = *2-is-2* a ⟨ trans ⟩ *-comm (fromℕ 2) a

  open import Function
  open import Data.Empty
  1+≢0 : ∀ l → toℕ (l 1#) ≢ 0
  1+≢0 l eq = case Data.Bin.Bijection.toℕ-inj {l 1#} {0#} eq of (λ ())

  z<nzℕ : ∀ {n} → n ≢ 0 → Data.Nat._<_ 0 n
  z<nzℕ {Data.Bin.0b} neq = ⊥-elim (neq refl)
  z<nzℕ {Data.Bin.Bijection.1+ n} neq = Data.Nat.s≤s Data.Nat.z≤n

  z<nz : ∀ l → 0# < l 1#
  z<nz l = Data.Bin.less (z<nzℕ (1+≢0 l))

max_stars_repo_name: Rotsor/BinDivMod

max_issues_repo_name: Rotsor/BinDivMod

max_forks_repo_name: Rotsor/BinDivMod