text:
{-# OPTIONS --without-K --allow-unsolved-metas #-}

module subuniverses where

import 14-univalence
open 14-univalence public

{-
is-local :
  {l1 l2 l3 l4 : Level}
  {I : UU l1} {A : I → UU l2} {B : I → UU l3} (f : (i : I) → A i → B i)
  (X : UU l4) → UU (l1 ⊔ (l2 ⊔ (l3 ⊔ l4)))
is-local {I = I} {B = B} f X =
  (i : I) → is-equiv (λ (h : B i → X) → h ∘ (f i))

is-subuniverse-is-local :
  {l1 l2 l3 l4 : Level}
  {I : UU l1} {A : I → UU l2} {B : I → UU l3} (f : (i : I) → A i → B i) →
  is-subuniverse (is-local {l4 = l4} f)
is-subuniverse-is-local f X = is-prop-Π (λ i → is-subtype-is-equiv _)
-}

universal-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2)
  (X : UU l1) (Y : total-subuniverse P) (l : X → pr1 Y) →
  UU ((lsuc l1) ⊔ l2)
universal-property-localization {l1} (pair P H) X (pair Y p) l =
  (Z : UU l1) (q : P Z) → is-equiv (λ (h : Y → Z) → h ∘ l)

universal-property-localization' :
  (l : Level) (α : Level → Level) (P : (l : Level) → subuniverse l (α l))
  (g : (l1 l2 : Level) → is-global-subuniverse α P l1 l2)
  {l1 l2 : Level} (X : UU l1) (Y : total-subuniverse (P l2)) (f : X → pr1 Y) →
  UU ((lsuc l) ⊔ ((α l) ⊔ (l1 ⊔ l2)))
universal-property-localization' l α P g X Y f =
  (Z : total-subuniverse (P l)) → is-equiv (λ (h : (pr1 Y) → (pr1 Z)) → h ∘ f)

is-prop-universal-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1)
  (Y : total-subuniverse P) (l : X → pr1 Y) →
  is-prop (universal-property-localization P X Y l)
is-prop-universal-property-localization (pair P H) X (pair Y p) l =
  is-prop-Π (λ Z → is-prop-Π (λ q → is-subtype-is-equiv _))

has-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  UU ((lsuc l1) ⊔ l2)
has-localization {l1} P X =
  Σ ( total-subuniverse P)
    ( λ Y → Σ (X → pr1 Y) (universal-property-localization P X Y))

Eq-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( s t : has-localization P X) → UU l1
Eq-localizations (pair P H) X
  (pair (pair Y p) (pair l up)) t =
  let Y' = pr1 (pr1 t)
      p' = pr1 (pr1 t)
      l' = pr1 (pr2 t)
      up' = pr2 (pr2 t)
  in
  Σ ( Y ≃ Y')
    ( λ e → ((map-equiv e) ∘ l) ~ l' )

reflexive-Eq-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (s : has-localization P X) → Eq-localizations P X s s
reflexive-Eq-localizations (pair P H) X (pair (pair Y p) (pair l up)) =
  pair (equiv-id Y) (htpy-refl l)

Eq-localizations-eq :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( s t : has-localization P X) → Id s t → Eq-localizations P X s t
Eq-localizations-eq P X s s refl = reflexive-Eq-localizations P X s

is-contr-total-Eq-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1)
  (s : has-localization P X) →
  is-contr (Σ (has-localization P X) (Eq-localizations P X s))
is-contr-total-Eq-localizations
  (pair P H) X (pair (pair Y p) (pair l up)) =
  is-contr-total-Eq-structure
    ( λ Y' l' e → ((map-equiv e) ∘ l) ~ (pr1 l'))
    ( is-contr-total-Eq-total-subuniverse (pair P H) (pair Y p))
    ( pair (pair Y p) (equiv-id Y))
    ( is-contr-total-Eq-substructure
      ( is-contr-total-htpy l)
      ( is-prop-universal-property-localization (pair P H) X (pair Y p))
      ( l)
      ( htpy-refl _)
      ( up))

is-equiv-Eq-localizations-eq :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( s t : has-localization P X) → is-equiv (Eq-localizations-eq P X s t)
is-equiv-Eq-localizations-eq P X s =
  fundamental-theorem-id s
  ( reflexive-Eq-localizations P X s)
  ( is-contr-total-Eq-localizations P X s)
  ( Eq-localizations-eq P X s)

eq-Eq-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1)
  ( s t : has-localization P X) → (Eq-localizations P X s t) → Id s t
eq-Eq-localizations P X s t =
  inv-is-equiv (is-equiv-Eq-localizations-eq P X s t)

uniqueness-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( s t : has-localization P X) → Eq-localizations P X s t
uniqueness-localizations (pair P H) X
  (pair (pair Y p) (pair l up)) (pair (pair Y' p') (pair l' up')) =
  pair
    ( pair
      ( inv-is-equiv (up Y' p') l')
      ( is-equiv-has-inverse
        ( pair
          ( inv-is-equiv (up' Y p) l)
          ( pair
            ( htpy-eq
              ( ap
                ( pr1 {B = λ h → Id (h ∘ l') l'})
                ( center
                  ( is-prop-is-contr
                    ( is-contr-map-is-equiv (up' Y' p') l')
                    ( pair
                      ( ( inv-is-equiv (up Y' p') l') ∘
                        ( inv-is-equiv (up' Y p) l))
                      ( ( ap
                          ( λ t → (inv-is-equiv (up Y' p') l') ∘ t)
                          ( issec-inv-is-equiv (up' Y p) l)) ∙
                        ( issec-inv-is-equiv (up Y' p') l')))
                    ( pair id refl)))))
            ( htpy-eq
              ( ap
                ( pr1 {B = λ h → Id (h ∘ l) l})
                ( center
                  ( is-prop-is-contr
                    ( is-contr-map-is-equiv (up Y p) l)
                    ( pair
                      ( ( inv-is-equiv (up' Y p) l) ∘
                        ( inv-is-equiv (up Y' p') l'))
                      ( ( ap
                          ( λ t → (inv-is-equiv (up' Y p) l) ∘ t)
                          ( issec-inv-is-equiv (up Y' p') l')) ∙
                         issec-inv-is-equiv (up' Y p) l))
                    ( pair id refl)))))))))
    ( htpy-eq (issec-inv-is-equiv (up Y' p') l'))

is-prop-localizations :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  is-prop (has-localization P X)
is-prop-localizations P X =
  is-prop-is-prop'
    ( λ Y Y' → eq-Eq-localizations P X Y Y'
      ( uniqueness-localizations P X Y Y'))

universal-property-localization-equiv-is-local :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : UU l1) (p : (pr1 P) Y) (l : X → Y) →
  is-equiv l → universal-property-localization P X (pair Y p) l
universal-property-localization-equiv-is-local
  (pair P H) X Y p l is-equiv-l Z q =
  is-equiv-precomp-is-equiv l is-equiv-l Z

universal-property-localization-id-is-local :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) (q : (pr1 P) X) →
  universal-property-localization P X (pair X q) id
universal-property-localization-id-is-local P X q =
  universal-property-localization-equiv-is-local P X X q id (is-equiv-id X)

is-equiv-localization-is-local :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( Y : has-localization P X) → (pr1 P) X → is-equiv (pr1 (pr2 Y))
is-equiv-localization-is-local
  (pair P H) X (pair (pair Y p) (pair l up)) q =
  is-equiv-right-factor
    ( id)
    ( inv-is-equiv (up X q) id)
    ( l)
    ( htpy-eq (inv (issec-inv-is-equiv (up X q) id)))
    ( pr2
      ( pr1
        ( uniqueness-localizations (pair P H) X
          ( pair (pair Y p) (pair l up))
          ( pair
            ( pair X q)
            ( pair id
              ( universal-property-localization-id-is-local
                (pair P H) X q))))))
    ( is-equiv-id X)

is-local-is-equiv-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  ( Y : has-localization P X) → is-equiv (pr1 (pr2 Y)) → (pr1 P) X
is-local-is-equiv-localization
  (pair P H) X (pair (pair Y p) (pair l up)) is-equiv-l =
  in-subuniverse-equiv' P (pair l is-equiv-l) p

strong-retraction-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : total-subuniverse P) (l : X → pr1 Y) → UU l1
strong-retraction-property-localization (pair P H) X (pair Y p) l =
  is-equiv (λ (h : Y → X) → h ∘ l)

retraction-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : total-subuniverse P) (l : X → pr1 Y) → UU l1
retraction-property-localization (pair P H) X (pair Y p) l =
  retr l

strong-retraction-property-localization-is-equiv-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : total-subuniverse P) (l : X → pr1 Y) →
  is-equiv l → strong-retraction-property-localization P X Y l
strong-retraction-property-localization-is-equiv-localization
  (pair P H) X (pair Y p) l is-equiv-l =
  is-equiv-precomp-is-equiv l is-equiv-l X

retraction-property-localization-strong-retraction-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : total-subuniverse P) (l : X → pr1 Y) →
  strong-retraction-property-localization P X Y l →
  retraction-property-localization P X Y l
retraction-property-localization-strong-retraction-property-localization
  (pair P H) X (pair Y p) l s =
  tot (λ h → htpy-eq) (center (is-contr-map-is-equiv s id))

is-equiv-localization-retraction-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : has-localization P X) →
  retraction-property-localization P X (pr1 Y) (pr1 (pr2 Y)) →
  is-equiv (pr1 (pr2 Y))
is-equiv-localization-retraction-property-localization
  (pair P H) X (pair (pair Y p) (pair l up)) (pair g isretr-g) =
  is-equiv-has-inverse
    ( pair g
      ( pair
        ( htpy-eq
          ( ap
            ( pr1 {B = λ (h : Y → Y) → Id (h ∘ l) l})
            ( center
              ( is-prop-is-contr
                ( is-contr-map-is-equiv (up Y p) l)
                ( pair (l ∘ g) (ap (λ t → l ∘ t) (eq-htpy isretr-g)))
                ( pair id refl)))))
        ( isretr-g)))

is-local-retraction-property-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (Y : has-localization P X) →
  retraction-property-localization P X (pr1 Y) (pr1 (pr2 Y)) →
  (pr1 P) X
is-local-retraction-property-localization P X Y r =
  is-local-is-equiv-localization P X Y
    ( is-equiv-localization-retraction-property-localization P X Y r)

is-local-has-localization-is-contr :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  is-contr X → has-localization P X → (pr1 P) X
is-local-has-localization-is-contr
  (pair P H) X is-contr-X (pair (pair Y p) (pair l up)) =
  is-local-retraction-property-localization (pair P H) X
    ( pair (pair Y p) (pair l up))
    ( pair
      ( λ _ → center is-contr-X)
      ( contraction is-contr-X))

has-localization-is-local-is-contr :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  is-contr X → (pr1 P) X → has-localization P X
has-localization-is-local-is-contr (pair P H) X is-contr-X p =
  pair
    ( pair X p)
    ( pair id (universal-property-localization-id-is-local (pair P H) X p))

is-contr-raise-unit :
  (l : Level) → is-contr (raise l unit)
is-contr-raise-unit l =
  is-contr-is-equiv' unit
    ( map-raise l unit)
    ( is-equiv-map-raise l unit)
    ( is-contr-unit)

is-local-unit-localization-unit :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (Y : has-localization P (raise l1 unit)) →
  (pr1 P) (raise l1 unit)
is-local-unit-localization-unit P Y =
  is-local-has-localization-is-contr P (raise _ unit) (is-contr-raise-unit _) Y

toto-dependent-elimination-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (has-loc-X : has-localization P X) →
  let Y = pr1 (pr1 has-loc-X)
      l = pr1 (pr2 has-loc-X)
  in
  (Z : Y → UU l1) →
  Σ (Y → Y) (λ h → (y : Y) → Z (h y)) →
  Σ (X → Y) (λ h → (x : X) → Z (h x))
toto-dependent-elimination-localization (pair P H) X
  (pair (pair Y p) (pair l up)) Z =
  toto
    ( λ (h : X → Y) → (x : X) → Z (h x))
    ( λ h → h ∘ l)
    ( λ h h' x → h' (l x))

square-dependent-elimination-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (has-loc-X : has-localization P X) →
  let Y = pr1 (pr1 has-loc-X)
      l = pr1 (pr2 has-loc-X)
  in
  (Z : Y → UU l1) (q : (pr1 P) (Σ _ Z)) →
  ( ( λ (h : Y → Σ Y Z) → h ∘ l) ∘
    ( inv-choice-∞)) ~
  ( ( inv-choice-∞) ∘
    ( toto-dependent-elimination-localization P X has-loc-X Z))
square-dependent-elimination-localization
  (pair P H) X (pair (pair Y p) (pair l up)) Z q =
  htpy-refl

is-equiv-toto-dependent-elimination-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) →
  (has-loc-X : has-localization P X)
  (Z : pr1 (pr1 has-loc-X) → UU l1) (q : (pr1 P) (Σ _ Z)) →
  is-equiv (toto-dependent-elimination-localization P X has-loc-X Z)
is-equiv-toto-dependent-elimination-localization
  (pair P H) X (pair (pair Y p) (pair l up)) Z q =
  is-equiv-top-is-equiv-bottom-square
    ( inv-choice-∞)
    ( inv-choice-∞)
    ( toto-dependent-elimination-localization
      (pair P H) X (pair (pair Y p) (pair l up)) Z)
    ( λ h → h ∘ l)
    ( square-dependent-elimination-localization
      (pair P H) X (pair (pair Y p) (pair l up)) Z q)
    ( is-equiv-inv-choice-∞)
    ( is-equiv-inv-choice-∞)
    ( up (Σ Y Z) q)

dependent-elimination-localization :
  {l1 l2 : Level} (P : subuniverse l1 l2) →
  (X : UU l1) (Y : has-localization P X) →
  (Z : (pr1 (pr1 Y)) → UU l1) (q : (pr1 P) (Σ _ Z)) →
  is-equiv (λ (h : (y : (pr1 (pr1 Y))) → (Z y)) → λ x → h (pr1 (pr2 Y) x))
dependent-elimination-localization (pair P H) X (pair (pair Y p) (pair l up)) Z q =
  is-fiberwise-equiv-is-equiv-toto-is-equiv-base-map
    ( λ (h : X → Y) → (x : X) → Z (h x))
    ( λ (h : Y → Y) → h ∘ l)
    ( λ (h : Y → Y) (h' : (y : Y) → Z (h y)) (x : X) → h' (l x))
    ( up Y p)
    ( is-equiv-toto-dependent-elimination-localization
      (pair P H) X (pair (pair Y p) (pair l up)) Z q)
    ( id)

is-reflective-subuniverse :
  {l1 l2 : Level} (P : subuniverse l1 l2) → UU ((lsuc l1) ⊔ l2)
is-reflective-subuniverse {l1} P = (X : UU l1) → has-localization P X

reflective-subuniverse :
  (l1 l2 : Level) → UU ((lsuc l1) ⊔ (lsuc l2))
reflective-subuniverse l1 l2 = Σ (subuniverse l1 l2) is-reflective-subuniverse

is-local :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) →
  UU l1 → UU l2
is-local L = pr1 (pr1 L)

is-prop-is-local :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) →
  (X : UU l1) → is-prop (is-local L X)
is-prop-is-local L = pr2 (pr1 L)

total-reflective-subuniverse :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) → UU ((lsuc l1) ⊔ l2)
total-reflective-subuniverse L = total-subuniverse (pr1 L)

local-type-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2)
  (X : UU l1) → total-reflective-subuniverse L
local-type-localization L X = pr1 ((pr2 L) X)

type-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) →
  UU l1 → UU l1
type-localization L X = pr1 (local-type-localization L X)

is-local-type-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2)
  (X : UU l1) → is-local L (type-localization L X)
is-local-type-localization L X = pr2 (local-type-localization L X)

universal-map-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) (X : UU l1) →
  Σ ( X → type-localization L X)
    ( universal-property-localization (pr1 L) X (local-type-localization L X))
universal-map-localization L X = pr2 ((pr2 L) X)

unit-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2)
  (X : UU l1) → X → type-localization L X
unit-localization L X = pr1 (universal-map-localization L X)

universal-property-map-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) (X : UU l1) →
  universal-property-localization (pr1 L) X
    ( local-type-localization L X)
    ( unit-localization L X)
universal-property-map-localization L X = pr2 (universal-map-localization L X)

dependent-elimination-reflective-subuniverse :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) (X : UU l1) →
  (Y : type-localization L X → UU l1)
  (is-loc-total-Y : is-local L (Σ _ Y)) →
  is-equiv
    ( λ (h : (x' : type-localization L X) → Y x') x → h (unit-localization L X x))
dependent-elimination-reflective-subuniverse L X =
  dependent-elimination-localization (pr1 L) X ((pr2 L) X)

is-contr-square-localization :
  {l1 l2 : Level} (L : reflective-subuniverse l1 l2) {X Y : UU l1} (f : X → Y) →
  is-contr
    ( Σ (type-localization L X → type-localization L Y)
      ( λ Lf → coherence-square (unit-localization L X) f Lf (unit-localization L Y)))
is-contr-square-localization L f = {!!}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
open import Relation.Binary.Core

module PLRTree.Push.Permutation {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.List
open import Data.Sum
open import Induction.WellFounded
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Equality {A}
open import PLRTree.Order {A}
open import PLRTree.Order.Properties {A}

lemma-push-∼-≃ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ≃ r → (acc : Acc _≺_ (node perfect x l r)) → flatten (push (node perfect x l r) acc) ∼ flatten (node right x l r)
lemma-push-∼-≃ {l} {r} x cl cr l≃r (acc rs)
    with l | r | l≃r | cl | cr
... | leaf | leaf | ≃lf | _ | _ = ∼x /head /head ∼[]
... | node perfect x' l' r' | node perfect x'' l'' r'' | ≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'' | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr

lemma-push-∼-⋗ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋗ r → (acc : Acc _≺_ (node right x l r)) → flatten (push (node right x l r) acc) ∼ flatten (node right x l r)
lemma-push-∼-⋗ {l} {r} x cl cr l⋗r (acc rs)
    with l | r | l⋗r | cl | cr
... | leaf | _ | () | _ | _
... | node perfect x' leaf leaf | leaf | ⋗lf .x' | perfect .x' leaf leaf ≃lf | leaf
    with tot≤ x x'
... | inj₁ x≤x' = ∼x /head /head (∼x /head /head ∼[])
... | inj₂ x'≤x = ∼x (/tail /head) /head (∼x /head /head ∼[])
lemma-push-∼-⋗ x cl cr l⋗r (acc rs) | node perfect x' l' r' | node perfect x'' l'' r'' | ⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'' | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _
    with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr

mutual
  lemma-push-∼-⋙ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋙ r → (acc : Acc _≺_ (node right x l r)) → flatten (push (node right x l r) acc) ∼ flatten (node right x l r)
  lemma-push-∼-⋙ {l} {r} x cl cr l⋙r (acc rs)
      with l | r | l⋙r | cl | cr
  ... | leaf | _ | ⋙p () | _ | _
  ... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') | perfect .x' leaf leaf ≃lf | leaf = lemma-push-∼-⋗ x (perfect x' leaf leaf ≃lf) leaf (⋗lf x') (acc rs)
  ... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') | perfect .x' cl' cr' _ | perfect .x'' cl'' cr'' _ =
             lemma-push-∼-⋗ x (perfect x' cl' cr' l'≃r') (perfect x'' cl'' cr'' l''≃r'') (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'') (acc rs)
  ... | node perfect x' leaf leaf | node left _ _ _ | ⋙p () | _ | _
  ... | node perfect x' leaf leaf | node right _ _ _ | ⋙p () | _ | _
  ... | node perfect x' l' r' | node left x'' l'' r'' | ⋙l .x' .x'' l'≃r' l''⋘r'' l'⋗r'' | perfect .x' cl' cr' _ | left .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height left x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node left x l'' r'') (lemma-≺-right perfect x _l (node left x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-⋘ x cl'' cr'' l''⋘r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node left x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node left x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height left x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node left x l'' r'') (lemma-≺-right perfect x _l (node left x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-⋘ x cl'' cr'' l''⋘r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  lemma-push-∼-⋙ x cl cr l⋙r (acc rs)| node perfect x' l' r' | node right x'' l'' r'' | ⋙r .x' .x'' l'≃r' l''⋙r'' l'≃l'' | perfect .x' cl' cr' _ | right .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height right x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node right x l'' r'') (lemma-≺-right perfect x _l (node right x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-⋙ x cl'' cr'' l''⋙r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node right x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height perfect x x' l' r' =
             let _r = node right x'' l'' r'' ;
                  acc-xl'r' = rs (node perfect x l' r') (lemma-≺-left perfect x (node perfect x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-≃ x cl' cr' l'≃r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height right x x'' l'' r'' =
             let _l = node perfect x' l' r' ;
                  acc-xl''r'' = rs (node right x l'' r'') (lemma-≺-right perfect x _l (node right x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-⋙ x cl'' cr'' l''⋙r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  lemma-push-∼-⋙ x cl cr l⋙r (acc rs) | node left _ _ _ | _ | ⋙p () | _ | _
  lemma-push-∼-⋙ x cl cr l⋙r (acc rs) | node right _ _ _ | _ | ⋙p () | _ | _

  lemma-push-∼-⋘ : {l r : PLRTree}(x : A) → Complete l → Complete r → l ⋘ r → (acc : Acc _≺_ (node left x l r)) → flatten (push (node left x l r) acc) ∼ flatten (node left x l r)
  lemma-push-∼-⋘ {l} {r} x cl cr l⋘r (acc rs)
      with l | r | l⋘r | cl | cr
  ... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | left .x' cl' cr' _ | perfect .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node left x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height left x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node left x l' r') (lemma-≺-left perfect x (node left x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-⋘ x cl' cr' l'⋘r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height left x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node left x l' r') (lemma-≺-left perfect x (node left x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-⋘ x cl' cr' l'⋘r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node left x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  lemma-push-∼-⋘ x cl cr l⋘r (acc rs) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | right .x' (perfect .x'' leaf leaf ≃lf) leaf (⋙p (⋗lf .x'')) | perfect .x''' leaf leaf ≃lf
      with tot≤ x x' | tot≤ x x''' | tot≤ x' x'''
  ... | inj₁ x≤x' | inj₁ x≤x''' | _ = refl∼
  ... | inj₁ x≤x' | inj₂ x'''≤x | _ =
             let _l = node perfect x' (node perfect x'' leaf leaf) leaf ;
                  acc-x = rs (node perfect x leaf leaf) (lemma-≺-right perfect x _l (node perfect x''' leaf leaf)) ;
                  x'''flfpx∼x'''flx = lemma++∼l {x''' ∷ flatten _l} (lemma-push-∼-≃ x leaf leaf ≃lf acc-x) ;
                  flxfr/x'''⟶flx = lemma++/l {x'''} {flatten _l} (/tail /head) ;
                  x'''flx∼flxfr = ∼x /head flxfr/x'''⟶flx refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x'''flx∼xflfr = trans∼ x'''flx∼flxfr flxfr∼xflfr
             in trans∼ x'''flfpx∼x'''flx x'''flx∼xflfr
  ... | inj₂ x'≤x | inj₁ x≤x''' | _ =
             let _r = node perfect x''' leaf leaf ;
                  acc-xx'' = rs (node right x (node perfect x'' leaf leaf) leaf) (lemma-≺-left perfect x (node right x' (node perfect x'' leaf leaf) leaf) _r) ;
                  fpxx''x'''∼xx''x''' = lemma++∼r (lemma-push-∼-⋗ x (perfect x'' leaf leaf ≃lf) leaf (⋗lf x'') acc-xx'') ;
                  x'fpxx''x'''∼x'xx''x''' = ∼x /head /head fpxx''x'''∼xx''x''' ;
                  x'xx''x'''∼xx'x''x''' = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxx''x'''∼x'xx''x''' x'xx''x'''∼xx'x''x'''
  ... | inj₂ x'≤x | inj₂ x'''≤x | inj₁ x'≤x''' =
             let _r = node perfect x''' leaf leaf ;
                  acc-xx'' = rs (node right x (node perfect x'' leaf leaf) leaf) (lemma-≺-left perfect x (node right x' (node perfect x'' leaf leaf) leaf) _r) ;
                  fpxx''x'''∼xx''x''' = lemma++∼r (lemma-push-∼-⋗ x (perfect x'' leaf leaf ≃lf) leaf (⋗lf x'') acc-xx'') ;
                  x'fpxx''x'''∼x'xx''x''' = ∼x /head /head fpxx''x'''∼xx''x''' ;
                  x'xx''x'''∼xx'x''x''' = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxx''x'''∼x'xx''x''' x'xx''x'''∼xx'x''x'''
  ... | inj₂ x'≤x | inj₂ x'''≤x | inj₂ x'''≤x' =
             let _l = node perfect x' (node perfect x'' leaf leaf) leaf ;
                  acc-x = rs (node perfect x leaf leaf) (lemma-≺-right perfect x _l (node perfect x''' leaf leaf)) ;
                  x'''flfpx∼x'''flx = lemma++∼l {x''' ∷ flatten _l} (lemma-push-∼-≃ x leaf leaf ≃lf acc-x) ;
                  flxfr/x'''⟶flx = lemma++/l {x'''} {flatten _l} (/tail /head) ;
                  x'''flx∼flxfr = ∼x /head flxfr/x'''⟶flx refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x'''flx∼xflfr = trans∼ x'''flx∼flxfr flxfr∼xflfr
             in trans∼ x'''flfpx∼x'''flx x'''flx∼xflfr
  lemma-push-∼-⋘ x cl cr l⋘r (acc rs) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l'⋙r' l''≃r'' l'⋗l'' | right .x' cl' cr' _ | perfect .x'' cl'' cr'' _
      with tot≤ x x' | tot≤ x x'' | tot≤ x' x''
  ... | inj₁ x≤x' | inj₁ x≤x'' | _ = refl∼
  ... | inj₁ x≤x' | inj₂ x''≤x | _ rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node right x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr
  ... | inj₂ x'≤x | inj₁ x≤x'' | _ rewrite lemma-≡-height right x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node right x l' r') (lemma-≺-left perfect x (node right x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-⋙ x cl' cr' l'⋙r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₁ x'≤x'' rewrite lemma-≡-height right x x' l' r' =
             let _r = node perfect x'' l'' r'' ;
                  acc-xl'r' = rs (node right x l' r') (lemma-≺-left perfect x (node right x' l' r') _r) ;
                  fpxl'r'fr∼xfl'fr'fr = lemma++∼r (lemma-push-∼-⋙ x cl' cr' l'⋙r' acc-xl'r') ;
                  x'fpxl'r'fr∼x'xfl'fr'fr = ∼x /head /head fpxl'r'fr∼xfl'fr'fr ;
                  x'xfl'fr'fr∼xflfr = ∼x /head (/tail /head) refl∼
             in trans∼ x'fpxl'r'fr∼x'xfl'fr'fr x'xfl'fr'fr∼xflfr
  ... | inj₂ x'≤x | inj₂ x''≤x | inj₂ x''≤x' rewrite lemma-≡-height perfect x x'' l'' r'' =
             let _l = node right x' l' r' ;
                  acc-xl''r'' = rs (node perfect x l'' r'') (lemma-≺-right perfect x _l (node perfect x'' l'' r'')) ;
                  x''flfpxl''r''∼x''flxfl''fr'' = lemma++∼l {x'' ∷ flatten _l} (lemma-push-∼-≃ x cl'' cr'' l''≃r'' acc-xl''r'') ;
                  flxfr/x''⟶flxfl''fr'' = lemma++/l {x''} {flatten _l} (/tail /head) ;
                  x''flxfl''fr''∼flxfr = ∼x /head flxfr/x''⟶flxfl''fr'' refl∼ ;
                  flxfr/x⟶flfr = lemma++/ {x} {flatten _l} ;
                  flxfr∼xflfr = ∼x flxfr/x⟶flfr /head refl∼ ;
                  x''flxfl''fr''∼xflfr = trans∼ x''flxfl''fr''∼flxfr flxfr∼xflfr
             in trans∼ x''flfpxl''r''∼x''flxfl''fr'' x''flxfl''fr''∼xflfr

lemma-push-∼ : {t : PLRTree} → Complete t → (acc : Acc _≺_ t) → flatten (push t acc) ∼ flatten t
lemma-push-∼ leaf _ = ∼[]
lemma-push-∼ (perfect {l} {r}x cl cr l≃r) (acc rs) = lemma-push-∼-≃ x cl cr l≃r (acc rs)
lemma-push-∼ (left {l} {r}x cl cr l⋘r) (acc rs) = lemma-push-∼-⋘ x cl cr l⋘r (acc rs)
lemma-push-∼ (right {l} {r}x cl cr l⋙r) (acc rs) = lemma-push-∼-⋙ x cl cr l⋙r (acc rs)

ext: agda

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --rewriting --prop --confluence-check #-}

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Data.Vec.Base
open import Data.Bool
open import Data.Sum

variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

record Top ℓ : Set ℓ where
  constructor ⟨⟩

{-
 Axiomatisation of ExTT
-}

postulate raise : (A : Set ℓ) → A

-- we now state rewrite rules for raise

postulate raise-Pi : (A : Set ℓ) (B : A → Set ℓ₁) →
                     raise ((a : A) → B a) ≡ λ a → raise (B a)

{-# REWRITE raise-Pi #-}

postulate raise-Sigma : (A : Set ℓ) (B : A → Set ℓ₁) →
                     raise (Σ A B) ≡ (raise A , raise (B (raise A)))

{-# REWRITE raise-Sigma #-}

nat-rec : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) → (n : Nat) → P n
nat-rec P P0 PS zero = P0
nat-rec P P0 PS (suc n) = PS n (nat-rec P P0 PS n)

postulate raise-nat-rec : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          nat-rec P P0 PS (raise Nat) ≡ raise (P (raise Nat))

{-# REWRITE raise-nat-rec #-}

postulate catch-nat : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                      (Praise : P (raise Nat)) → (n : Nat) → P n

postulate catch-nat-zero : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                           (Praise : P (raise Nat)) → catch-nat P P0 PS Praise 0 ≡ P0

postulate catch-nat-suc : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          (Praise : P (raise Nat)) → (n : Nat) →
                          catch-nat P P0 PS Praise (suc n) ≡ PS n (catch-nat P P0 PS Praise n)

postulate catch-nat-raise : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                            (Praise : P (raise Nat)) → catch-nat P P0 PS Praise (raise Nat) ≡ Praise

{-# REWRITE catch-nat-zero #-}
{-# REWRITE catch-nat-suc #-}
{-# REWRITE catch-nat-raise #-}

postulate raise-Top : raise (Top ℓ) ≡ ⟨⟩

{-# REWRITE raise-Top #-}

postulate raise-Set : raise (Set ℓ) ≡ Top ℓ

{-# REWRITE raise-Set #-}

{-
 Axiomatisation of unk
-}

postulate unk : (A : Set ℓ) → A

-- we now state rewrite rules for unk

postulate unk-Pi : (A : Set ℓ) (B : A → Set ℓ₁) →
                     unk ((a : A) → B a) ≡ λ a → unk (B a)

{-# REWRITE unk-Pi #-}

postulate unk-Sigma : (A : Set ℓ) (B : A → Set ℓ₁) →
                     unk (Σ A B) ≡ (unk A , unk (B (unk A)))

{-# REWRITE unk-Sigma #-}

postulate unk-nat-rec : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          nat-rec P P0 PS (unk Nat) ≡ unk (P (unk Nat))

{-# REWRITE unk-nat-rec #-}

postulate catch-unk-nat : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                      (Punk : P (unk Nat)) → (n : Nat) → P n

postulate catch-unk-nat-zero : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                           (Punk : P (unk Nat)) → catch-unk-nat P P0 PS Punk 0 ≡ P0

postulate catch-unk-nat-suc : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          (Punk : P (unk Nat)) → (n : Nat) →
                          catch-unk-nat P P0 PS Punk (suc n) ≡ PS n (catch-unk-nat P P0 PS Punk n)

postulate catch-unk-nat-unk : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                            (Punk : P (unk Nat)) → catch-unk-nat P P0 PS Punk (unk Nat) ≡ Punk

{-# REWRITE catch-unk-nat-zero #-}
{-# REWRITE catch-unk-nat-suc #-}
{-# REWRITE catch-unk-nat-unk #-}

postulate unk-Top : unk (Top ℓ) ≡ ⟨⟩

{-# REWRITE unk-Top #-}

Unk : ∀ ℓ → Set ℓ
Unk ℓ = unk (Set ℓ)

-- postulate Unk : ∀ ℓ → Set (lsuc ℓ)
-- -- record Unk ℓ : Set (lsuc ℓ) where
-- --   constructor box
-- --   field
-- --     type : Set ℓ
-- --     elem : type

-- postulate raise-Unk :  ∀ ℓ → raise (Unk ℓ) ≡ box (raise (Set ℓ)) (raise _)

-- {-# REWRITE raise-Unk #-}

max_stars_repo_name: CoqHott/exceptional-tt

max_issues_repo_name: CoqHott/exceptional-tt

max_forks_repo_name: CoqHott/exceptional-tt


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

open import Algebra.Solver.Ring.AlmostCommutativeRing

-- Some specialised tools for equaltional reasoning.
module Polynomial.Reasoning
  {a ℓ}
  (ring : AlmostCommutativeRing a ℓ)
  where

open AlmostCommutativeRing ring
open import Relation.Binary.Reasoning.Inference setoid public

infixr 1 ≪+_ +≫_ ≪*_ *≫_
≪+_ : ∀ {x₁ x₂ y} → x₁ ≈ x₂ → x₁ + y ≈ x₂ + y
≪+ prf = +-cong prf refl

+≫_ : ∀ {x y₁ y₂} → y₁ ≈ y₂ → x + y₁ ≈ x + y₂
+≫_ = +-cong refl

≪*_ : ∀ {x₁ x₂ y} → x₁ ≈ x₂ → x₁ * y ≈ x₂ * y
≪* prf = *-cong prf refl

*≫_ : ∀ {x y₁ y₂} → y₁ ≈ y₂ → x * y₁ ≈ x * y₂
*≫_ = *-cong refl
{-# INLINE ≪*_ #-}
{-# INLINE ≪+_ #-}
{-# INLINE *≫_ #-}
{-# INLINE +≫_ #-}

-- transitivity as an operator
infixr 0 _⊙_
_⊙_ : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z
_⊙_ = trans
{-# INLINE _⊙_ #-}

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module Logic.Propositional where

open import Data
open import Data.Either as Either using (_‖_)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic
import      Lvl
open import Type

infixl 1010 ¬_ ¬¬_
infixl 1005 _∧_
infixl 1004 _∨_
infixl 1000 _↔_

------------------------------------------
-- Conjunction (AND)

_∧_ : ∀{ℓ₁ ℓ₂} → Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
_∧_ = _⨯_

pattern [∧]-intro p q = p , q

[∧]-elimₗ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ∧ Q) → P
[∧]-elimₗ = Tuple.left

[∧]-elimᵣ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ∧ Q) → Q
[∧]-elimᵣ = Tuple.right

[∧]-map = Tuple.map

------------------------------------------
-- Implication

[→]-elim : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → P → (P → Q) → Q
[→]-elim p f = f(p)

[→]-intro : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P → Q) → (P → Q)
[→]-intro f(p) = f(p)

------------------------------------------
-- Reverse implication

open Functional using (_←_) public

[←]-intro : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P → Q) → (Q ← P)
[←]-intro = [→]-intro

[←]-elim : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → P → (Q ← P) → Q
[←]-elim = [→]-elim

------------------------------------------
-- Equivalence

_↔_ : ∀{ℓ₁ ℓ₂} → Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
P ↔ Q = ((P ← Q) ⨯ (P → Q))

pattern [↔]-intro l r = l , r

[↔]-elimₗ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → Q → (P ↔ Q) → P
[↔]-elimₗ = swap Tuple.left

[↔]-elimᵣ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → P → (P ↔ Q) → Q
[↔]-elimᵣ = swap Tuple.right

[↔]-to-[←] : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ↔ Q) → (Q → P)
[↔]-to-[←] = Tuple.left

[↔]-to-[→] : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ↔ Q) → (P → Q)
[↔]-to-[→] = Tuple.right

------------------------------------------
-- Disjunction (OR)

_∨_ : ∀{ℓ₁ ℓ₂} → Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
_∨_ = _‖_

pattern [∨]-introₗ l = Either.Left l
pattern [∨]-introᵣ r = Either.Right r

[∨]-elim : ∀{ℓ₁ ℓ₂ ℓ₃}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}}{R : Stmt{ℓ₃}} → (P → R) → (Q → R) → (P ∨ Q) → R
[∨]-elim = Either.map1

[∨]-elim2 = Either.map

------------------------------------------
-- Bottom (false, absurdity, empty, contradiction)

⊥ : Stmt{Lvl.𝟎}
⊥ = Empty

[⊥]-intro : ∀{ℓ}{P : Stmt{ℓ}} → P → (P → ⊥) → ⊥
[⊥]-intro = apply

[⊥]-elim : ∀{ℓ}{P : Stmt{ℓ}} → ⊥ → P
[⊥]-elim = empty

------------------------------------------
-- Top (true, truth, unit, validity)

⊤ : Stmt{Lvl.𝟎}
⊤ = Unit

pattern [⊤]-intro = <>

------------------------------------------
-- Negation

¬_ : ∀{ℓ} → Stmt{ℓ} → Stmt
¬_ {ℓ} T = (T → ⊥)

[¬]-intro : ∀{ℓ}{P : Stmt{ℓ}} → (P → ⊥) → (¬ P)
[¬]-intro = id

[¬]-elim : ∀{ℓ}{P : Stmt{ℓ}} → (¬ P) → (P → ⊥) -- written like (P → (¬ P) → ⊥) looks like a [⊥]-intro
[¬]-elim = id

¬¬_ : ∀{ℓ} → Stmt{ℓ} → Stmt
¬¬ p = ¬(¬ p)

------------------------------------------
-- Exclusive disjunction (XOR)

data _⊕_ {ℓ₁ ℓ₂} (P : Stmt{ℓ₁}) (Q : Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  [⊕]-introₗ : P → (¬ Q) → (P ⊕ Q)
  [⊕]-introᵣ : Q → (¬ P) → (P ⊕ Q)

------------------------------------------
-- Negative disjunction (NOR)

_⊽_ : ∀{ℓ₁ ℓ₂} → Stmt{ℓ₁} → Stmt{ℓ₂} → Stmt
p ⊽ q = (¬ p) ∧ (¬ q)

[⊽]-intro : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (¬ P) → (¬ Q) → (P ⊽ Q)
[⊽]-intro = [∧]-intro

[⊽]-elimₗ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ⊽ Q) → ¬ P
[⊽]-elimₗ = [∧]-elimₗ

[⊽]-elimᵣ : ∀{ℓ₁ ℓ₂}{P : Stmt{ℓ₁}}{Q : Stmt{ℓ₂}} → (P ⊽ Q) → ¬ Q
[⊽]-elimᵣ = [∧]-elimᵣ

------------------------------------------
-- Negative conjunction (NAND)

-- data _⊼_ {P : Stmt} {Q : Stmt} : Stmt where
--   [⊼]-intro ¬(P ∧ Q) → (P ⊼ Q)
--
-- [⊼]-elim : {P Q : Stmt} → (P ⨯ Q ⨯ (P ⊼ Q)) → ⊥
-- [⊼]-elim(p , q , nand)

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:
{- Basic theory about transport:

- transport is invertible
- transport is an equivalence ([transportEquiv])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Transport where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

-- Direct definition of transport filler, note that we have to
-- explicitly tell Agda that the type is constant (like in CHM)
transpFill : ∀ {ℓ} {A : Type ℓ}
             (φ : I)
             (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ])
             (u0 : outS (A i0))
           → --------------------------------------
             PathP (λ i → outS (A i)) u0 (transp (λ i → outS (A i)) φ u0)
transpFill φ A u0 i = transp (λ j → outS (A (i ∧ j))) (~ i ∨ φ) u0

transport⁻ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A
transport⁻ p = transport (λ i → p (~ i))

transport⁻Transport : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (a : A) →
                          transport⁻ p (transport p a) ≡ a
transport⁻Transport p a j =
  transp (λ i → p (~ i ∧ ~ j)) j (transp (λ i → p (i ∧ ~ j)) j a)

transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) →
                        transport p (transport⁻ p b) ≡ b
transportTransport⁻ p b j =
  transp (λ i → p (i ∨ j)) j (transp (λ i → p (~ i ∨ j)) j b)

-- Transport is an equivalence
isEquivTransport : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p)
isEquivTransport {A = A} {B = B} p =
  transport (λ i → isEquiv (λ x → transp (λ j → p (i ∧ j)) (~ i) x)) (idIsEquiv A)

transportEquiv : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B
transportEquiv p = (transport p , isEquivTransport p)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- Injections
------------------------------------------------------------------------

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

open import Equality

module Injection
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

------------------------------------------------------------------------
-- Injections

-- The property of being injective.

Injective : ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Injective f = ∀ {x y} → f x ≡ f y → x ≡ y

infix 0 _↣_

-- Injections.

record _↣_ {f t} (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    to        : From → To
    injective : Injective to

------------------------------------------------------------------------
-- Preorder

-- _↣_ is a preorder.

id : ∀ {a} {A : Type a} → A ↣ A
id = record
  { to        = P.id
  ; injective = P.id
  }

infixr 9 _∘_

_∘_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
      B ↣ C → A ↣ B → A ↣ C
f ∘ g = record
  { to        = to′
  ; injective = injective′
  }
  where
  open _↣_

  to′ = to f ⊚ to g

  injective′ : Injective to′
  injective′ = injective g ⊚ injective f

-- "Equational" reasoning combinators.

infix  -1 finally-↣
infixr -2 step-↣

-- For an explanation of why step-↣ is defined in this way, see
-- Equality.step-≡.

step-↣ : ∀ {a b c} (A : Type a) {B : Type b} {C : Type c} →
         B ↣ C → A ↣ B → A ↣ C
step-↣ _ = _∘_

syntax step-↣ A B↣C A↣B = A ↣⟨ A↣B ⟩ B↣C

finally-↣ : ∀ {a b} (A : Type a) (B : Type b) → A ↣ B → A ↣ B
finally-↣ _ _ A↣B = A↣B

syntax finally-↣ A B A↣B = A ↣⟨ A↣B ⟩□ B □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Negation where

-- Imports

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_)
-- open import plfa.part1.Isomorphism using (_≃_; extensionality)

-- 同型 (isomorphism)
infix 0 _≃_
record _≃_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

postulate
  -- 外延性の公理
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

-- Negation (否定)

infix 3 ¬_
¬_ : Set → Set
¬ A = A → ⊥

¬-elim : ∀ {A : Set}
  → ¬ A
  → A
    ---
  → ⊥
¬-elim ¬x x = ¬x x

-- 二重否定の導入則
¬¬-intro : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
¬¬-intro x  =  λ{¬x → ¬x x}

-- 二重否定の導入則
¬¬-intro′ : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
¬¬-intro′ x ¬x = ¬x x

-- 三重否定の除去則
¬¬¬-elim : ∀ {A : Set}
  → ¬ ¬ ¬ A
    -------
  → ¬ A
¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)

-- 対偶 (contraposition)
contraposition : ∀ {A B : Set}
  → (A → B)
    -----------
  → (¬ B → ¬ A)
contraposition f ¬y x = ¬y (f x)

-- 不等号(inequality)
_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y  =  ¬ (x ≡ y)

_ : 1 ≢ 2
_ = λ()

peano : ∀ {m : ℕ} → zero ≢ suc m
peano = λ()

id : ⊥ → ⊥
id x = x

id′ : ⊥ → ⊥
id′ ()

id≡id′ : id ≡ id′
id≡id′ = extensionality (λ())

-- 同化
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
assimilation ¬x ¬x′ = extensionality (λ x → ⊥-elim (¬x x))

-- Excluded middle is irrefutable

-- 排中律 (excluded middle)
postulate
  em : ∀ {A : Set} → A ⊎ ¬ A

-- 排中律は反駁できない
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-# OPTIONS --copatterns #-}

module Control.Functor.NaturalTransformation where

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

open import Control.Functor using (Functor; module Functor; Const)
open import Control.Category using (Category; module Category)

-- Natural transformations.

IsNatTrans : (F! G! : Functor) →
  let open Functor F! using () renaming (F to F; map to mapF)
      open Functor G! using () renaming (F to G; map to mapG)
  in
      (n : ∀ {A} → F A → G A) → Set₁

IsNatTrans F! G! eta = ∀ {A B} (f : A → B) →
  let open Functor F! using () renaming (F to F; map to mapF)
      open Functor G! using () renaming (F to G; map to mapG)
  in
      eta ∘ mapF f ≡ mapG f ∘ eta

-- Constant-Constant natural transformation.

KKNat : ∀ {A B} (η : A → B) → IsNatTrans (Const A) (Const B) η
KKNat η = λ f → refl

-- Natural transformations (packaged).

record NatTrans (F! G! : Functor) : Set₁ where

  open Functor F! using () renaming (F to F; map to mapF)
  open Functor G! using () renaming (F to G; map to mapG)
  field

    eta        : ∀ {A} → F A → G A

    naturality : ∀ {A B} (f : A → B) →

        eta ∘ mapF f ≡ mapG f ∘ eta

  -- To use naturality in applications:
  postulate
    app-naturality : ∀ {A : Set} {B C : A → Set}
     (f : (x : A) → B x → C x)
     (g : (x : A) → F (B x))
     (x : A) →

        eta (mapF (f x) (g x)) ≡ mapG (f x) (eta (g x))

  -- app-naturality g f x = {!!}

open NatTrans

-- The identity natural transformation.

Id : ∀ {F! : Functor} → NatTrans F! F!
Id {F! = F!} = record { eta = λ x → x ; naturality = λ f → refl }

-- Natural transformations compose.

Comp : ∀ {F! G! H! : Functor} → NatTrans F! G! → NatTrans G! H! → NatTrans F! H!
Comp {F! = F!}{G! = G!}{H! = H!} n m = record { eta = nm ; naturality = snm }
  where
    open Functor F! using () renaming (F to F; map to mapF)
    open Functor G! using () renaming (F to G; map to mapG)
    open Functor H! using () renaming (F to H; map to mapH)

    nm : ∀ {A} → F A → H A
    nm = λ x → eta m (eta n x)

    snm :  ∀ {A B} (f : A → B) →

        nm ∘ mapF f ≡ mapH f ∘ nm

    snm f = begin
        nm ∘ mapF f             ≡⟨⟩
        eta m ∘ eta n ∘ mapF f  ≡⟨ cong (λ z → eta m ∘ z) (naturality n f) ⟩
        eta m ∘ mapG f ∘ eta n  ≡⟨ cong (λ z → z ∘ eta n) (naturality m f) ⟩
        mapH f ∘ eta m ∘ eta n  ≡⟨⟩
        mapH f ∘ nm
      ∎

-- Natural transformation between constant functors.

ConstNat : ∀ {A B} (η : A → B) → NatTrans (Const A) (Const B)
ConstNat η = record
  { eta        = η
  ; naturality = λ f → refl
  }

-- Functor category.

FunctorHom : ∀ (F G : Functor) → Setoid _ _
FunctorHom F G = record
  { Carrier       = NatTrans F G
  ; _≈_           = λ n m → ∀ {A} → eta n {A} ≡ eta m {A}
  ; isEquivalence = record
    { refl  = refl
    ; sym   = λ p → sym p
    ; trans = λ p q → trans p q
    }
  }

FUNCTOR : Category _ _ _
FUNCTOR = record
  { Hom = FunctorHom
  ; isCategory = record
    { ops = record
      { id = Id
      ; _⟫_ = Comp
    }
    ; laws = record
      { id-first = refl
      ; id-last  = refl
      ; ∘-assoc  = λ f → refl
      ; ∘-cong   = λ n≡n' m≡m' → cong₂ (λ m n x → m (n x)) m≡m' n≡n' }
    }
  }

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
module Test2 where

open import Test

-- Testing the inter-file goto facility.

test : ℕ
test = 12 + 34 + 56

-- Testing qualified names.

Eq = Test.Equiv {Test.ℕ}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text: module Sort (A : Set)(_<_ : A → A → Set) where

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
module Everything where

open import Relation.Binary.Core

postulate A : Set
postulate _≤_ : A → A → Set
postulate tot≤ : Total _≤_
postulate trans≤ : Transitive _≤_

open import BBHeap.Everything _≤_ tot≤ trans≤

open import BHeap.Everything _≤_ tot≤

open import BTree.Complete.Alternative.Correctness {A}

open import BubbleSort.Everything _≤_ tot≤ trans≤

open import Heapsort.Everything _≤_ tot≤ trans≤

open import InsertSort.Everything _≤_ tot≤

open import List.Permutation.Base.Bag A

open import Mergesort.Everything _≤_ tot≤

open import PLRTree.Everything _≤_ tot≤ trans≤

open import Quicksort.Everything _≤_ tot≤ trans≤

open import SelectSort.Everything _≤_ tot≤ trans≤

open import TreeSort.Everything _≤_ tot≤ trans≤


text:
-----------------------------------------------------------------------
-- This file defines DC₂(Sets) and its SMC structure.              --
-----------------------------------------------------------------------
module DC2Sets where

open import prelude

-- The objects:
Obj : Set₁
Obj = Σ[ U ∈ Set ] (Σ[ X ∈ Set ] (U → X → Set))

-- The morphisms:
Hom : Obj → Obj → Set
Hom (U , X , α) (V , Y , β) =
  Σ[ f ∈ (U → V) ]
    (Σ[ F ∈ (U → Y → X) ] (∀{u : U}{y : Y} → α u (F u y) → β (f u) y))

-- Composition:
comp : {A B C : Obj} → Hom A B → Hom B C → Hom A C
comp {(U , X , α)} {(V , Y , β)} {(W , Z , γ)} (f , F , p₁) (g , G , p₂) =
  (g ∘ f , (λ u z → F u (G (f u) z)), (λ {u} {y} p₃ → p₂ (p₁ p₃)))

infixl 5 _○_

_○_ = comp

-- The contravariant hom-functor:
Homₐ :  {A' A B B' : Obj} → Hom A' A → Hom B B' → Hom A B → Hom A' B'
Homₐ f h g = comp f (comp g h)

-- The identity function:
id : {A : Obj} → Hom A A
id {(U , V , α)} = (id-set , curry snd , id-set)

-- In this formalization we will only worry about proving that the
-- data of morphisms are equivalent, and not worry about the morphism
-- conditions.  This will make proofs shorter and faster.
--
-- If we have parallel morphisms (f,F) and (g,G) in which we know that
-- f = g and F = G, then the condition for (f,F) will imply the
-- condition of (g,G) and vice versa.  Thus, we can safely ignore it.
infix 4 _≡h_

_≡h_ : {A B : Obj} → (f g : Hom A B) → Set
_≡h_ {(U , X , α)}{(V , Y , β)} (f , F , p₁) (g , G , p₂) = f ≡ g × F ≡ G

≡h-refl : {A B : Obj}{f : Hom A B} → f ≡h f
≡h-refl {U , X , α}{V , Y , β}{f , F , _} = refl , refl

≡h-trans : ∀{A B}{f g h : Hom A B} → f ≡h g → g ≡h h → f ≡h h
≡h-trans {U , X , α}{V , Y , β}{f , F , _}{g , G , _}{h , H , _} (p₁ , p₂) (p₃ , p₄) rewrite p₁ | p₂ | p₃ | p₄ = refl , refl

≡h-sym : ∀{A B}{f g : Hom A B} → f ≡h g → g ≡h f
≡h-sym {U , X , α}{V , Y , β}{f , F , _}{g , G , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

≡h-subst-○ : ∀{A B C}{f₁ f₂ : Hom A B}{g₁ g₂ : Hom B C}{j : Hom A C}
  → f₁ ≡h f₂
  → g₁ ≡h g₂
  → f₂ ○ g₂ ≡h j
  → f₁ ○ g₁ ≡h j
≡h-subst-○ {U , X , α}
         {V , Y , β}
         {W , Z , γ}
         {f₁ , F₁ , _}
         {f₂ , F₂ , _}
         {g₁ , G₁ , _}
         {g₂ , G₂ , _}
         {j , J , _}
         (p₅ , p₆) (p₇ , p₈) (p₉ , p₁₀) rewrite p₅ | p₆ | p₇ | p₈ | p₉ | p₁₀ = refl , refl

○-assoc : ∀{A B C D}{f : Hom A B}{g : Hom B C}{h : Hom C D}
  → f ○ (g ○ h) ≡h (f ○ g) ○ h
○-assoc {U , X , α}{V , Y , β}{W , Z , γ}{S , T , ι}
        {f , F , _}{g , G , _}{h , H , _} = refl , refl

○-idl : ∀{A B}{f : Hom A B} → id ○ f ≡h f
○-idl {U , X , _}{V , Y , _}{f , F , _} = refl , refl

○-idr : ∀{A B}{f : Hom A B} → f ○ id ≡h f
○-idr {U , X , _}{V , Y , _}{f , F , _} = refl , refl

-----------------------------------------------------------------------
-- DC₂(Sets) is a SMC                                              --
-----------------------------------------------------------------------

-- The tensor functor: ⊗
_⊗ᵣ_ : ∀{U X V Y : Set} → (U → X → Set) → (V → Y → Set) → ((U × V) → (X × Y) → Set)
_⊗ᵣ_ α β (u , v) (x , y) = (α u x) × (β v y)

_⊗ₒ_ : (A B : Obj) → Obj
(U , X , α) ⊗ₒ (V , Y , β) = ((U × V) , (X × Y) , α ⊗ᵣ β)

F⊗ : ∀{Z T V X U Y : Set}{F : U → Z → X}{G : V → T → Y} → (U × V) → (Z × T) → (X × Y)
F⊗ {F = F}{G} (u , v) (z , t) = F u z , G v t

_⊗ₐ_ : {A B C D : Obj} → Hom A C → Hom B D → Hom (A ⊗ₒ B) (C ⊗ₒ D)
_⊗ₐ_ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)}{(S , T , δ)} (f , F , p₁) (g , G , p₂) = ⟨ f , g ⟩ , F⊗ {F = F}{G} , p⊗
 where
  p⊗ : {u : Σ U (λ x → V)} {y : Σ Z (λ x → T)} → (α ⊗ᵣ β) u (F⊗ {F = F}{G} u y) → (γ ⊗ᵣ δ) (⟨ f , g ⟩ u) y
  p⊗ {u , v}{z , t} (p₃ , p₄) = p₁  p₃ , p₂ p₄

-- The unit for tensor:
ι : ⊤ → ⊤ → Set
ι triv triv = ⊤

I : Obj
I = (⊤ , ⊤ , ι)

J : Obj
J = (⊤ , ⊤ , (λ x y → ⊥))

-- The left-unitor:
λ⊗-p : ∀{U X α}{u : Σ ⊤ (λ x → U)} {y : X} → (ι ⊗ᵣ α) u (triv , y) → α (snd u) y
λ⊗-p {U}{X}{α}{(triv , u)}{x} = snd

λ⊗ : ∀{A : Obj} → Hom (I ⊗ₒ A) A
λ⊗ {(U , X , α)} = snd , (λ _ x → triv , x) , λ⊗-p

λ⊗-inv : ∀{A : Obj} → Hom A (I ⊗ₒ A)
λ⊗-inv {(U , X , α)} = (λ u → triv , u) , (λ _ r → snd r) , λ⊗-inv-p
 where
  λ⊗-inv-p : ∀{U X α}{u : U} {y : Σ ⊤ (λ x → X)} → α u (snd y) → (ι ⊗ᵣ α) (triv , u) y
  λ⊗-inv-p {U}{X}{α}{u}{triv , x} p = triv , p

-- The right-unitor:
ρ⊗ : ∀{A : Obj} → Hom (A ⊗ₒ I) A
ρ⊗ {(U , X , α)} = fst , (λ r x → x , triv) , ρ⊗-p
 where
  ρ⊗-p : ∀{U X α}{u : Σ U (λ x → ⊤)} {y : X} → (α ⊗ᵣ ι) u (y , triv) → α (fst u) y
  ρ⊗-p {U}{X}{α}{(u , _)}{x} (p , _) = p

ρ⊗-inv : ∀{A : Obj} → Hom A (A ⊗ₒ I)
ρ⊗-inv {(U , X , α)} = (λ u → u , triv) , (λ u r → fst r) , ρ⊗-p-inv
 where
  ρ⊗-p-inv : ∀{U X α}{u : U} {y : Σ X (λ x → ⊤)} → α u (fst y) → (α ⊗ᵣ ι) (u , triv) y
  ρ⊗-p-inv {U}{X}{α}{u}{x , triv} p = p , triv

-- Symmetry:
β⊗ : ∀{A B : Obj} → Hom (A ⊗ₒ B) (B ⊗ₒ A)
β⊗ {(U , X , α)}{(V , Y , β)} = twist-× , (λ r₁ r₂ → twist-× r₂) , β⊗-p
 where
   β⊗-p : ∀{U V Y X α β}{u : Σ U (λ x → V)} {y : Σ Y (λ x → X)} → (α ⊗ᵣ β) u (twist-× y) → (β ⊗ᵣ α) (twist-× u) y
   β⊗-p {U}{V}{Y}{X}{α}{β}{u , v}{y , x} = twist-×

-- The associator:
Fα-inv : ∀{ℓ}{U V W X Y Z : Set ℓ} → (U × (V × W)) → ((X × Y) × Z) → (X × (Y × Z))
Fα-inv (u , (v , w)) ((x , y) , z) = x , y , z

α⊗-inv : ∀{A B C : Obj} → Hom (A ⊗ₒ (B ⊗ₒ C)) ((A ⊗ₒ B) ⊗ₒ C)
α⊗-inv {(U , X , α)}{(V , Y , β)}{(W , Z , γ)} = rl-assoc-× , Fα-inv , α-inv-cond
 where
   α-inv-cond : {u : Σ U (λ x → Σ V (λ x₁ → W))}{y : Σ (Σ X (λ x → Y)) (λ x → Z)}
     → (α ⊗ᵣ (β ⊗ᵣ γ)) u (Fα-inv u y)
     → ((α ⊗ᵣ β) ⊗ᵣ γ) (rl-assoc-× u) y
   α-inv-cond {u , (v , w)}{(x , y) , z} (p₁ , (p₂ , p₃)) = (p₁ , p₂) , p₃

Fα : ∀{V W X Y U Z : Set} → ((U × V) × W) → (X × (Y × Z)) → ((X × Y) × Z)
Fα {V}{W}{X}{Y}{U}{Z} ((u , v) , w) (x , (y , z)) = (x , y) , z

α⊗ : ∀{A B C : Obj} → Hom ((A ⊗ₒ B) ⊗ₒ C) (A ⊗ₒ (B ⊗ₒ C))
α⊗ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)} = (lr-assoc-× , Fα , α-cond)
 where
  α-cond : {u : Σ (Σ U (λ x → V)) (λ x → W)}
      {y : Σ X (λ x → Σ Y (λ x₁ → Z))} →
      ((α ⊗ᵣ β) ⊗ᵣ γ) u (Fα u y) → (α ⊗ᵣ (β ⊗ᵣ γ)) (lr-assoc-× u) y
  α-cond {(u , v) , w}{x , (y , z)} ((p₁ , p₂) , p₃) = p₁ , p₂ , p₃

α⊗-id₁ : ∀{A B C} → (α⊗ {A}{B}{C}) ○ α⊗-inv ≡h id
α⊗-id₁ {U , X , α}{V , Y , β}{W , Z , γ} = ext-set aux , ext-set aux'
 where
   aux : {a : Σ (Σ U (λ x → V)) (λ x → W)} → rl-assoc-× (lr-assoc-× a) ≡ a
   aux {(u , v) , w} = refl

   aux' : {a : Σ (Σ U (λ x → V)) (λ x → W)} → (λ z → Fα {V}{W}{X}{Y}{U}{Z} a (Fα-inv (lr-assoc-× a) z)) ≡ (λ y → y)
   aux' {(u , v), w} = ext-set aux''
    where
      aux'' : {a : Σ (Σ X (λ x → Y)) (λ x → Z)} → Fα ((u , v) , w) (Fα-inv (u , v , w) a) ≡ a
      aux'' {(x , y) , z} = refl

α⊗-id₂ : ∀{A B C} → (α⊗-inv {A}{B}{C}) ○ α⊗ ≡h id
α⊗-id₂ {U , X , α}{V , Y , β}{W , Z , γ} = ext-set aux , ext-set aux'
 where
   aux : {a : Σ U (λ x → Σ V (λ x₁ → W))} → lr-assoc-× (rl-assoc-× a) ≡ a
   aux {u , (v , w)} = refl
   aux' : {a : Σ U (λ x → Σ V (λ x₁ → W))} → (λ z → Fα-inv {_}{U}{V}{W}{X}{Y}{Z} a (Fα (rl-assoc-× a) z)) ≡ (λ y → y)
   aux' {u , (v , w)} = ext-set aux''
    where
      aux'' : {a : Σ X (λ x → Σ Y (λ x₁ → Z))} → Fα-inv (u , v , w) (Fα ((u , v) , w) a) ≡ a
      aux'' {x , (y , z)} = refl

-- Internal hom:
⊸-cond : ∀{U V X Y : Set}{α : U → X → Set}{β : V → Y → Set}
  → Σ (U → V) (λ x → U → Y → X)
  → Σ U (λ x → Y)
  → Set
⊸-cond {α = α}{β} (f , F) (u , y) = α u (F u y) → β (f u) y

_⊸ₒ_ : Obj → Obj → Obj
(U , X , α) ⊸ₒ (V , Y , β) = ((U → V) × (U → Y → X)) , ((U × Y) , ⊸-cond {α = α}{β})

_⊸ₐ_ : {A B C D : Obj} → Hom C A → Hom B D → Hom (A ⊸ₒ B) (C ⊸ₒ D)
_⊸ₐ_ {(U , X , α)}{(V , Y , β)}{(W , Z , γ)}{(S , T , δ)} (f , F , p₁) (g , G , p₂) =
  h , H , cond
 where
  h : Σ (U → V) (λ x → U → Y → X) → Σ (W → S) (λ x → W → T → Z)
  h (i , I) = (λ w → g (i (f w))) , (λ w t → F w (I (f w) (G (i (f w)) t)))
  H : Σ (U → V) (λ x → U → Y → X) → Σ W (λ x → T) → Σ U (λ x → Y)
  H (i , I) (w , t) = f w , G (i (f w)) t
  cond : {u : Σ (U → V) (λ x → U → Y → X)} {y : Σ W (λ x → T)} → ⊸-cond {α = α}{β} u (H u y) → ⊸-cond {α = γ}{δ} (h u) y
  cond {i , I}{w , y} p₃ p₄ = p₂ (p₃ (p₁ p₄))

cur : {A B C : Obj}
  → Hom (A ⊗ₒ B) C
  → Hom A (B ⊸ₒ C)
cur {U , X , α}{V , Y , β}{W , Z , γ} (f , F , p₁)
  = (λ u → (λ v → f (u , v)) , (λ v z → snd (F (u , v) z))) , (λ u r → fst (F (u , (fst r)) (snd r))) , cond
 where
   cond : {u : U} {y : Σ V (λ x → Z)}
     → α u (fst (F (u , fst y) (snd y)))
     → ⊸-cond {α = β}{γ} ((λ v → f (u , v)) , (λ v z → snd (F (u , v) z))) y
   cond {u}{v , z} p₂ p₃ with (p₁ {u , v}{z})
   ... | p₄ with F (u , v) z
   ... | (x , y) = p₄ (p₂ , p₃)

cur-≡h : ∀{A B C}{f₁ f₂ : Hom (A ⊗ₒ B) C}
  → f₁ ≡h f₂
  → cur f₁ ≡h cur f₂
cur-≡h {U , X , α}{V , Y , β}{W , Z , γ}
       {f₁ , F₁ , p₁}{f₂ , F₂ , p₂} (p₃ , p₄)
       rewrite p₃ | p₄ = refl , refl

cur-cong : ∀{A B C}{f₁ f₂ : Hom (A ⊗ₒ B) C} → f₁ ≡h f₂ → cur f₁ ≡h cur f₂
cur-cong {(U , X , α)} {(V , Y , β)} {(W , Z , γ)}{f₁ , F₁ , _}{f₂ , F₂ , _} (p₁ , p₂) rewrite p₁ | p₂ = refl , refl

uncur : {A B C : Obj}
  → Hom A (B ⊸ₒ C)
  → Hom (A ⊗ₒ B) C
uncur {U , X , α}{V , Y , β}{W , Z , γ} (f , F , p₁)
  = let h = λ r → fst (f (fst r)) (snd r)
        H = λ r z → F (fst r) (snd r , z) , snd (f (fst r)) (snd r) z
     in h , (H , cond)
 where
  cond : {u : Σ U (λ x → V)} {y : Z} →
      (α ⊗ᵣ β) u (F (fst u) (snd u , y) , snd (f (fst u)) (snd u) y) →
      γ (fst (f (fst u)) (snd u)) y
  cond {u , v}{z} (p₂ , p₃) with p₁ {u} {v , z}
  ... | p₄ with f u
  ... | i , I = p₄ p₂ p₃

cur-uncur-bij₁ : ∀{A B C}{f : Hom (A ⊗ₒ B) C}
  → uncur (cur f) ≡h f
cur-uncur-bij₁ {U , X , α}{V , Y , β}{W , Z , γ}{f , F , p₁} = ext-set aux₁ , ext-set aux₂
 where
   aux₁ : {a : Σ U (λ x → V)} → f (fst a , snd a) ≡ f a
   aux₁ {u , v} = refl
   aux₂ : {a : Σ U (λ x → V)} → (λ z → fst (F (fst a , snd a) z) , snd (F (fst a , snd a) z)) ≡ F a
   aux₂ {u , v} = ext-set aux₃
    where
      aux₃ : {a : Z} → (fst (F (u , v) a) , snd (F (u , v) a)) ≡ F (u , v) a
      aux₃ {z} with F (u , v) z
      ... | x , y = refl

cur-uncur-bij₂ : ∀{A B C}{g : Hom A (B ⊸ₒ C)}
  → cur (uncur g) ≡h g
cur-uncur-bij₂ {U , X , α}{V , Y , β}{W , Z , γ}{g , G , p₁} = (ext-set aux) , ext-set (ext-set aux')
 where
  aux : {a : U} → ((λ v → fst (g a) v) , (λ v z → snd (g a) v z)) ≡ g a
  aux {u} with g u
  ... | i , I = refl
  aux' : {u : U}{r : Σ V (λ x → Z)} → G u (fst r , snd r) ≡ G u r
  aux' {u}{v , z} = refl

-- The of-course exponential:
!ₒ-cond : ∀{U X : Set} → (α : U → X → Set) → U → 𝕃 X → Set
!ₒ-cond {U}{X} α u [] = ⊤
!ₒ-cond {U}{X} α u (x :: xs) = (α u x) × (!ₒ-cond α u xs)

!ₒ-cond-++ : ∀{U X : Set}{α : U → X → Set}{u : U}{l₁ l₂ : 𝕃 X}
  → !ₒ-cond α u (l₁ ++ l₂) ≡ ((!ₒ-cond α u l₁) × (!ₒ-cond α u l₂))
!ₒ-cond-++ {U}{X}{α}{u}{[]}{l₂} = ∧-unit
!ₒ-cond-++ {U}{X}{α}{u}{x :: xs}{l₂} rewrite !ₒ-cond-++ {U}{X}{α}{u}{xs}{l₂} = ∧-assoc

!ₒ : Obj → Obj
!ₒ (U , X , α) = U ,  X * , !ₒ-cond α

!ₐ-s : ∀{U Y X : Set}
  → (U → Y → X)
  → (U → Y * → X *)
!ₐ-s f u l = map (f u) l

!ₐ : {A B : Obj} → Hom A B → Hom (!ₒ A) (!ₒ B)
!ₐ {U , X , α}{V , Y , β} (f , F , p) = f , (!ₐ-s F , aux)
 where
   aux : {u : U} {y : 𝕃 Y} → !ₒ-cond α u (!ₐ-s F u y) → !ₒ-cond β (f u) y
   aux {u}{[]} p₁ = triv
   aux {u}{y :: ys} (p₁ , p₂) = p p₁ , aux p₂

-- Of-course is a comonad:
ε : ∀{A} → Hom (!ₒ A) A
ε {U , X , α} = id-set , (λ u x → [ x ]) , fst

δ-s : {U X : Set} → U → 𝕃 (𝕃 X) → 𝕃 X
δ-s u xs = foldr _++_ [] xs

δ : ∀{A} → Hom (!ₒ A) (!ₒ (!ₒ A))
δ {U , X , α} = id-set , δ-s , cond
 where
   cond : {u : U} {y : 𝕃 (𝕃 X)} → !ₒ-cond α u (foldr _++_ [] y) → !ₒ-cond (!ₒ-cond α) u y
   cond {u}{[]} p = triv
   cond {u}{l :: ls} p with !ₒ-cond-++ {U}{X}{α}{u}{l}{foldr _++_ [] ls}
   ... | p' rewrite p' with p
   ... | p₂ , p₃ = p₂ , cond {u}{ls} p₃

comonand-diag₁ : ∀{A}
  → (δ {A}) ○ (!ₐ (δ {A})) ≡h (δ {A}) ○ (δ { !ₒ A})
comonand-diag₁ {U , X , α} = refl , ext-set (λ {x} → ext-set (λ {l} → aux {x} {l}))
 where
  aux : ∀{x : U}{l : 𝕃 (𝕃 (𝕃 X))}
    → foldr _++_ [] (!ₐ-s (λ u xs
    → foldr _++_ [] xs) x l) ≡ foldr _++_ [] (foldr _++_ [] l)
  aux {u}{[]} = refl
  aux {u}{x :: xs} rewrite aux {u}{xs} = foldr-append {_}{_}{X}{X}{x}{foldr _++_ [] xs}

comonand-diag₂ : ∀{A}
  → (δ {A}) ○ (ε { !ₒ A}) ≡h (δ {A}) ○ (!ₐ (ε {A}))
comonand-diag₂ {U , X , α} =
  refl , ext-set (λ {u} → ext-set (λ {l} → aux {l}))
  where
    aux : ∀{a : 𝕃 X} → a ++ [] ≡ foldr _++_ [] (map (λ x → x :: []) a)
    aux {[]} = refl
    aux {x :: xs} rewrite (++[] xs) | sym (foldr-map {_}{X}{xs}) = refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL