text:
module PiQ.Properties where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Data.Maybe.Properties
open import Data.Nat hiding (_≟_)
open import Data.Nat.Induction
open import Data.Nat.Properties hiding (_≟_)
open import Function using (_∘_)
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import PiQ.Syntax
open import PiQ.Opsem
open import PiQ.AuxLemmas
open import PiQ.NoRepeat
open import PiQ.Invariants
open import PiQ.Eval
open import PiQ.Interp

-- Change the direction of the given state
flip : (st : State) → st ≢ ⊠ → State
flip ⟨ c ∣ v ∣ κ ⟩▷ _ = ⟨ c ∣ v ∣ κ ⟩◁
flip ［ c ∣ v ∣ κ ］▷ _ = ［ c ∣ v ∣ κ ］◁
flip ⟨ c ∣ v ∣ κ ⟩◁ _ = ⟨ c ∣ v ∣ κ ⟩▷
flip ［ c ∣ v ∣ κ ］◁ _ = ［ c ∣ v ∣ κ ］▷
flip ⊠ st≢⊠ = ⊥-elim (st≢⊠ refl)

Rev : ∀ {st st'} → st ↦ st' → (nf : st ≢ ⊠) (nf' : st' ≢ ⊠)
    → flip st' nf' ↦ flip st nf
Rev ↦⃗₁ _ _ = ↦⃖₁
Rev ↦⃗₂ _ _ = ↦⃖₂
Rev ↦⃗₃ _ _ = ↦⃖₃
Rev ↦⃗₄ _ _ = ↦⃖₄
Rev ↦⃗₅ _ _ = ↦⃖₅
Rev ↦⃗₆ _ _ = ↦⃖₆
Rev ↦⃗₇ _ _ = ↦⃖₇
Rev ↦⃗₈ _ _ = ↦⃖₈
Rev ↦⃗₉ _ _ = ↦⃖₉
Rev ↦⃗₁₀ _ _ = ↦⃖₁₀
Rev ↦⃗₁₁ _ _ = ↦⃖₁₁
Rev ↦⃗₁₂ _ _ = ↦⃖₁₂
Rev ↦⃖₁ _ _ = ↦⃗₁
Rev ↦⃖₂ _ _ = ↦⃗₂
Rev ↦⃖₃ _ _ = ↦⃗₃
Rev ↦⃖₄ _ _ = ↦⃗₄
Rev ↦⃖₅ _ _ = ↦⃗₅
Rev ↦⃖₆ _ _ = ↦⃗₆
Rev ↦⃖₇ _ _ = ↦⃗₇
Rev ↦⃖₈ _ _ = ↦⃗₈
Rev ↦⃖₉ _ _ = ↦⃗₉
Rev ↦⃖₁₀ _ _ = ↦⃗₁₀
Rev ↦⃖₁₁ _ _ = ↦⃗₁₁
Rev ↦⃖₁₂ _ _ = ↦⃗₁₂
Rev ↦η₊₁ _ _ = ↦η₊₂
Rev ↦η₊₂ _ _ = ↦η₊₁
Rev ↦ε₊₁ _ _ = ↦ε₊₂
Rev ↦ε₊₂ _ _ = ↦ε₊₁
Rev ↦⃗ηₓ _ _ = ↦⃖ηₓ₁ {eq = refl}
Rev (↦⃖ηₓ₁ {eq = refl}) _ _ = ↦⃗ηₓ
Rev ↦⃖ηₓ₂ _ nf' = ⊥-elim (nf' refl)
Rev (↦⃗εₓ₁ {eq = refl}) _ _ = ↦⃖εₓ
Rev ↦⃗εₓ₂ _ nf' = ⊥-elim (nf' refl)
Rev ↦⃖εₓ _ _ = ↦⃗εₓ₁ {eq = refl}

Rev* : ∀ {st st'} → st ↦* st' → (nf : st ≢ ⊠) → (nf' : st' ≢ ⊠) → flip st' nf' ↦* flip st nf
Rev* {⟨ _ ∣ _ ∣ _ ⟩▷} ◾ _ _ = ◾
Rev* {［ _ ∣ _ ∣ _ ］▷} ◾ _ _ = ◾
Rev* {⟨ _ ∣ _ ∣ _ ⟩◁} ◾ _ _ = ◾
Rev* {［ _ ∣ _ ∣ _ ］◁} ◾ _ _ = ◾
Rev* {⊠} ◾ nf _ = ⊥-elim (nf refl)
Rev* (r ∷ ◾) nf nf' = Rev r nf nf' ∷ ◾
Rev* (r ∷ (r' ∷ rs)) nf nf' = Rev* (r' ∷ rs) nf'' nf' ++↦ (Rev r nf nf'' ∷ ◾)
  where
  nf'' = λ eq → ⊠-is-stuck eq (_ , r')

-- Helper functions
inspect⊎ : ∀ {ℓ ℓ₁ ℓ₂ ℓ₃} {P : Set ℓ} {Q : Set ℓ₁} {R : Set ℓ₂} {S : Set ℓ₃}
         → (f : P → Q ⊎ R ⊎ S) → (p : P) → (∃[ q ] (inj₁ q ≡ f p)) ⊎ (∃[ r ] (inj₂ (inj₁ r) ≡ f p)) ⊎ (∃[ s ] (inj₂ (inj₂ s) ≡ f p))
inspect⊎ f p with f p
... | inj₁ q = inj₁ (q , refl)
... | inj₂ (inj₁ r) = inj₂ (inj₁ (r , refl))
... | inj₂ (inj₂ r) = inj₂ (inj₂ (r , refl))

Val≢ : ∀ {A B v₁ v₂} → _⃗ {A} {B} v₁ ≢ v₂ ⃖
Val≢ ()

Maybe≢ : ∀ {ℓ} {A : Set ℓ} {a : A} → just a ≢ nothing
Maybe≢ ()

toState : ∀ {A B} → (A ↔ B) → Maybe (Val B A) → State
toState c (just (b ⃗)) = ［ c ∣ b ∣ ☐ ］▷
toState c (just (a ⃖)) = ⟨ c ∣ a ∣ ☐ ⟩◁
toState c nothing = ⊠

is-stuck-toState : ∀ {A B} → (c : A ↔ B) → (v : Maybe (Val B A)) → is-stuck (toState c v)
is-stuck-toState c (just (b ⃗)) = λ ()
is-stuck-toState c (just (a ⃖)) = λ ()
is-stuck-toState c nothing = λ ()

toStateEq₁ : ∀ {A B b} → (c : A ↔ B) → (x : Maybe (Val B A)) → ［ c ∣ b ∣ ☐ ］▷ ≡ toState c x → just (b ⃗) ≡ x
toStateEq₁ c (just (x ⃗)) refl = refl

toStateEq₂ : ∀ {A B a} → (c : A ↔ B) → (x : Maybe (Val B A)) → ⟨ c ∣ a ∣ ☐ ⟩◁ ≡ toState c x → just (a ⃖) ≡ x
toStateEq₂ c (just (x ⃖)) refl = refl

toStateEq₃ : ∀ {A B} → (c : A ↔ B) → (x : Maybe (Val B A)) → ⊠ ≡ toState c x → nothing ≡ x
toStateEq₃ c nothing refl = refl
toStateEq₃ c (just (x ⃗)) ()
toStateEq₃ c (just (x ⃖)) ()

toState≡₁ : ∀ {A B b x} {c : A ↔ B} → toState c x ≡ ［ c ∣ b ∣ ☐ ］▷ → x ≡ just (b ⃗)
toState≡₁ {x = just (x ⃗)} refl = refl

toState≡₂ : ∀ {A B a x} {c : A ↔ B} → toState c x ≡ ⟨ c ∣ a ∣ ☐ ⟩◁ → x ≡ just (a ⃖)
toState≡₂ {x = just (x ⃖)} refl = refl

toState≡₃ : ∀ {A B x} {c : A ↔ B} → toState c x ≡ ⊠ → x ≡ nothing
toState≡₃ {x = nothing} refl = refl
toState≡₃ {x = just (x ⃗)} ()
toState≡₃ {x = just (x ⃖)} ()

eval-toState₁ : ∀ {A B a x} {c : A ↔ B} → ⟨ c ∣ a ∣ ☐ ⟩▷ ↦* (toState c x) → eval c (a ⃗) ≡ x
eval-toState₁ {a = a} {just (b ⃗)} {c} rs with inspect⊎ (run ⟨ c ∣ a ∣ ☐ ⟩▷) (λ ())
eval-toState₁ {a = a} {just (b ⃗)} {c} rs | inj₁ ((a' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {just (b ⃗)} {c} rs | inj₂ (inj₁ ((b' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (b ⃗)) eq refl
eval-toState₁ {a = a} {just (b ⃗)} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {just (a' ⃖)} {c} rs with inspect⊎ (run ⟨ c ∣ a ∣ ☐ ⟩▷) (λ ())
eval-toState₁ {a = a} {just (a' ⃖)} {c} rs | inj₁ ((a'' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (a' ⃖)) eq refl
eval-toState₁ {a = a} {just (a' ⃖)} {c} rs | inj₂ (inj₁ ((b' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {just (a' ⃖)} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {nothing} {c} rs with inspect⊎ (run ⟨ c ∣ a ∣ ☐ ⟩▷) (λ ())
eval-toState₁ {a = a} {nothing} {c} rs | inj₁ ((a' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {nothing} {c} rs | inj₂ (inj₁ ((b' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₁ {a = a} {nothing} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ nothing) eq refl

eval-toState₂ : ∀ {A B b x} {c : A ↔ B} → ［ c ∣ b ∣ ☐ ］◁ ↦* (toState c x) → eval c (b ⃖) ≡ x
eval-toState₂ {b = b} {just (b' ⃗)} {c} rs with inspect⊎ (run ［ c ∣ b ∣ ☐ ］◁) (λ ())
eval-toState₂ {b = b} {just (b' ⃗)} {c} rs | inj₁ ((a' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {just (b' ⃗)} {c} rs | inj₂ (inj₁ ((b'' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (b' ⃗)) eq refl
eval-toState₂ {b = b} {just (b' ⃗)} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {just (a ⃖)} {c} rs with inspect⊎ (run ［ c ∣ b ∣ ☐ ］◁) (λ ())
eval-toState₂ {b = b} {just (a ⃖)} {c} rs | inj₁ ((a'' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (a ⃖)) eq refl
eval-toState₂ {b = b} {just (a ⃖)} {c} rs | inj₂ (inj₁ ((b' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {just (a ⃖)} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {nothing} {c} rs with inspect⊎ (run ［ c ∣ b ∣ ☐ ］◁) (λ ())
eval-toState₂ {b = b} {nothing} {c} rs | inj₁ ((a' , rs') , eq) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {nothing} {c} rs | inj₂ (inj₁ ((b' , rs') , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | ()
eval-toState₂ {b = b} {nothing} {c} rs | inj₂ (inj₂ (rs' , eq)) with deterministic* rs rs' (λ ()) (λ ())
... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ nothing) eq refl

getₜᵣ⃗ : ∀ {A B} → (c : A ↔ B) → {v : ⟦ A ⟧} {v' : Maybe (Val B A)} → eval c (v ⃗) ≡ v'
       → ⟨ c ∣ v ∣ ☐ ⟩▷ ↦* toState c v'
getₜᵣ⃗ c {v} {v'} eq with inspect⊎ (run ⟨ c ∣ v ∣ ☐ ⟩▷) (λ ())
getₜᵣ⃗ c {v} {nothing} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃗ c {v} {just (x ⃗)} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃗ c {v} {just (x ⃖)} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃗ c {v} {nothing} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃗ c {v} {just (x ⃗)} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃗ c {v} {just (x ⃖)} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃗ c {v} {nothing} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃗ c {v} {just (x ⃗)} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃗ c {v} {just (x ⃖)} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()

getₜᵣ⃖ : ∀ {A B} → (c : A ↔ B) → {v : ⟦ B ⟧} {v' : Maybe (Val B A)} → eval c (v ⃖) ≡ v'
       → ［ c ∣ v ∣ ☐ ］◁ ↦* toState c v'
getₜᵣ⃖ c {v} {v'} eq with inspect⊎ (run ［ c ∣ v ∣ ☐ ］◁) (λ ())
getₜᵣ⃖ c {v} {nothing} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃖ c {v} {just (x ⃗)} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃖ c {v} {just (x ⃖)} eq | inj₁ ((x₁ , rs₁) , eq₁) with trans (subst (λ x → just (x₁ ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃖ c {v} {nothing} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃖ c {v} {just (x ⃗)} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃖ c {v} {just (x ⃖)} eq | inj₂ (inj₁ ((x₁ , rs₁) , eq₁)) with trans (subst (λ x → just (x₁ ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃖ c {v} {nothing} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | refl = rs₁
getₜᵣ⃖ c {v} {just (x ⃗)} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()
getₜᵣ⃖ c {v} {just (x ⃖)} eq | inj₂ (inj₂ (rs₁ , eq₁)) with trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq₁ refl) eq
... | ()

-- Forward evaluator is reversible
evalIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : Val A B) (v₂ : Val B A)
          → eval c v₁ ≡ (just v₂) → evalᵣₑᵥ c v₂ ≡ (just v₁)
evalIsRev c (v₁ ⃗) (v₂ ⃗) eq with inspect⊎ (run ⟨ c ∣ v₁ ∣ ☐ ⟩▷) (λ ())
evalIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₁ ((u , rs) , eq') = ⊥-elim (Val≢ (sym (just-injective contr)))
  where
  contr : just (u ⃖) ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₂ (inj₁ ((u , rs) , eq')) = subst (λ x → evalᵣₑᵥ c x ≡ just (v₁ ⃗)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃗) ≡ (v₂ ⃗)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : evalᵣₑᵥ c (u ⃗) ≡ just (v₁ ⃗)
  rsinv with u≡v₂ | inspect⊎ (run ［ c ∣ v₂ ∣ ☐ ］◁) (λ ())
  rsinv | refl | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃗)) eq'' refl
  rsinv | refl | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | refl | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₂ (inj₂ (rs , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃗) (v₂ ⃖) eq with inspect⊎ (run ⟨ c ∣ v₁ ∣ ☐ ⟩▷) (λ ())
evalIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₁ ((u , rs) , eq') = subst (λ x → evalᵣₑᵥ c x ≡ just (v₁ ⃗)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃖) ≡ (v₂ ⃖)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : evalᵣₑᵥ c (u ⃖) ≡ just (v₁ ⃗)
  rsinv with u≡v₂ | inspect⊎ (run ⟨ c ∣ u ∣ ☐ ⟩▷) (λ ())
  rsinv | refl | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃗)) eq'' refl
  rsinv | refl | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | refl | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₂ (inj₁ ((u , rs) , eq')) = ⊥-elim (Val≢ (just-injective contr))
  where
  contr : just (u ⃗) ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₂ (inj₂ (rs , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃖) (v₂ ⃗) eq with inspect⊎ (run ［ c ∣ v₁ ∣ ☐ ］◁) (λ ())
evalIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₁ ((u , rs) , eq') = ⊥-elim (Val≢ (just-injective (sym contr)))
  where
  contr : just (u ⃖) ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₂ (inj₁ ((u , rs) , eq')) = subst (λ x → evalᵣₑᵥ c x ≡ just (v₁ ⃖)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃗) ≡ (v₂ ⃗)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : evalᵣₑᵥ c (u ⃗) ≡ just (v₁ ⃖)
  rsinv with u≡v₂ | inspect⊎ (run ［ c ∣ u ∣ ☐ ］◁) (λ ())
  rsinv | refl | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | refl | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃖)) eq'' refl
  rsinv | refl | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₂ (inj₂ (rs , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃖) (v₂ ⃖) eq with inspect⊎ (run ［ c ∣ v₁ ∣ ☐ ］◁) (λ ())
evalIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₁ ((u , rs) , eq') = subst (λ x → evalᵣₑᵥ c x ≡ just (v₁ ⃖)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃖) ≡ (v₂ ⃖)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : evalᵣₑᵥ c (u ⃖) ≡ just (v₁ ⃖)
  rsinv with u≡v₂ | inspect⊎ (run ⟨ c ∣ u ∣ ☐ ⟩▷) (λ ())
  rsinv | refl | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | refl | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃖)) eq'' refl
  rsinv | refl | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₂ (inj₁ ((u , rs) , eq')) = ⊥-elim (Val≢ (just-injective contr))
  where
  contr : just (u ⃗) ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₂ (inj₂ (rs , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq

-- Backward evaluator is reversible
evalᵣₑᵥIsRev : ∀ {A B} → (c : A ↔ B) (v₁ : Val B A) (v₂ : Val A B)
             → evalᵣₑᵥ c v₁ ≡ (just v₂) → eval c v₂ ≡ (just v₁)
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃗) eq with inspect⊎ (run ［ c ∣ v₁ ∣ ☐ ］◁) (λ ())
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₁ ((u , rs) , eq') = subst (λ x → eval c x ≡ just (v₁ ⃗)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃗) ≡ (v₂ ⃗)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : eval c (u ⃗) ≡ just (v₁ ⃗)
  rsinv with inspect⊎ (run ⟨ c ∣ u ∣ ☐ ⟩▷) (λ ())
  rsinv | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃗)) eq'' refl
  rsinv | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₂ (inj₁ ((u , rs) , eq')) = ⊥-elim (Val≢ (sym (just-injective contr)))
  where
  contr : just (u ⃖) ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃗) eq | inj₂ (inj₂ (rs' , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃖) eq with inspect⊎ (run ［ c ∣ v₁ ∣ ☐ ］◁) (λ ())
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₁ ((u , rs) , eq') = ⊥-elim (Val≢ (just-injective contr))
  where
  contr : just (u ⃗) ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₂ (inj₁ ((u , rs) , eq')) = subst (λ x → eval c x ≡ just (v₁ ⃗)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃖) ≡ (v₂ ⃖)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : eval c (u ⃖) ≡ just (v₁ ⃗)
  rsinv with inspect⊎ (run ［ c ∣ u ∣ ☐ ］◁) (λ ())
  rsinv | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃗)) eq'' refl
  rsinv | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalᵣₑᵥIsRev c (v₁ ⃗) (v₂ ⃖) eq | inj₂ (inj₂ (rs' , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃗) eq with inspect⊎ (run ⟨ c ∣ v₁ ∣ ☐ ⟩▷) (λ ())
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₁ ((u , rs) , eq') = subst (λ x → eval c x ≡ just (v₁ ⃖)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃗) ≡ (v₂ ⃗)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : eval c (u ⃗) ≡ just (v₁ ⃖)
  rsinv with inspect⊎ (run ⟨ c ∣ u ∣ ☐ ⟩▷) (λ ())
  rsinv | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃖)) eq'' refl
  rsinv | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₂ (inj₁ ((u , rs) , eq')) = ⊥-elim (Val≢ (sym (just-injective contr)))
  where
  contr : just (u ⃖) ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃗) eq | inj₂ (inj₂ (rs' , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃗)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃖) eq with inspect⊎ (run ⟨ c ∣ v₁ ∣ ☐ ⟩▷) (λ ())
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₁ ((u , rs) , eq') = ⊥-elim (Val≢ (just-injective contr))
  where
  contr : just (u ⃗) ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → just (u ⃗) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₂ (inj₁ ((u , rs) , eq')) = subst (λ x → eval c x ≡ just (v₁ ⃖)) u≡v₂ rsinv
  where
  u≡v₂ : (u ⃖) ≡ (v₂ ⃖)
  u≡v₂ = just-injective (trans (subst (λ x → just (u ⃖) ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq)

  rsinv : eval c (u ⃖) ≡ just (v₁ ⃖)
  rsinv with inspect⊎ (run ［ c ∣ u ∣ ☐ ］◁) (λ ())
  rsinv | inj₁ ((w , rs') , eq'') with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | refl = subst (λ x → [ just ∘ _⃖ ∘ proj₁ , [ just ∘ _⃗ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x ≡ just (v₁ ⃖)) eq'' refl
  rsinv | inj₂ (inj₁ ((w , rs') , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
  rsinv | inj₂ (inj₂ (rs' , eq'')) with deterministic* rs' (Rev* rs (λ ()) (λ ())) (λ ()) (λ ())
  ... | ()
evalᵣₑᵥIsRev c (v₁ ⃖) (v₂ ⃖) eq | inj₂ (inj₂ (rs' , eq')) = ⊥-elim (Maybe≢ (sym contr))
  where
  contr : nothing ≡ just (v₂ ⃖)
  contr = trans (subst (λ x → nothing ≡ [ just ∘ _⃗ ∘ proj₁ , [ just ∘ _⃖ ∘ proj₁ , (λ _ → nothing) ]′ ]′ x) eq' refl) eq

-- The abstract machine semantics is equivalent to the big-step semantics
mutual
  eval≡interp : ∀ {A B} → (c : A ↔ B) → (v : Val A B) → eval c v ≡ interp c v
  eval≡interp unite₊l (inj₂ v ⃗) = refl
  eval≡interp unite₊l (v ⃖) = refl
  eval≡interp uniti₊l (v ⃗) = refl
  eval≡interp uniti₊l (inj₂ v ⃖) = refl
  eval≡interp swap₊ (inj₁ x ⃗) = refl
  eval≡interp swap₊ (inj₂ y ⃗) = refl
  eval≡interp swap₊ (inj₁ x ⃖) = refl
  eval≡interp swap₊ (inj₂ y ⃖) = refl
  eval≡interp assocl₊ (inj₁ x ⃗) = refl
  eval≡interp assocl₊ (inj₂ (inj₁ y) ⃗) = refl
  eval≡interp assocl₊ (inj₂ (inj₂ z) ⃗) = refl
  eval≡interp assocl₊ (inj₁ (inj₁ x) ⃖) = refl
  eval≡interp assocl₊ (inj₁ (inj₂ y) ⃖) = refl
  eval≡interp assocl₊ (inj₂ z ⃖) = refl
  eval≡interp assocr₊ (inj₁ (inj₁ x) ⃗) = refl
  eval≡interp assocr₊ (inj₁ (inj₂ y) ⃗) = refl
  eval≡interp assocr₊ (inj₂ z ⃗) = refl
  eval≡interp assocr₊ (inj₁ x ⃖) = refl
  eval≡interp assocr₊ (inj₂ (inj₁ y) ⃖) = refl
  eval≡interp assocr₊ (inj₂ (inj₂ z) ⃖) = refl
  eval≡interp unite⋆l ((tt , v) ⃗) = refl
  eval≡interp unite⋆l (v ⃖) = refl
  eval≡interp uniti⋆l (v ⃗) = refl
  eval≡interp uniti⋆l ((tt , v) ⃖) = refl
  eval≡interp swap⋆ ((x , y) ⃗) = refl
  eval≡interp swap⋆ ((y , x) ⃖) = refl
  eval≡interp assocl⋆ ((x , (y , z)) ⃗) = refl
  eval≡interp assocl⋆ (((x , y) , z) ⃖) = refl
  eval≡interp assocr⋆ (((x , y) , z) ⃗) = refl
  eval≡interp assocr⋆ ((x , (y , z)) ⃖) = refl
  eval≡interp absorbr (() ⃗)
  eval≡interp absorbr (() ⃖)
  eval≡interp factorzl (() ⃗)
  eval≡interp factorzl (() ⃖)
  eval≡interp dist ((inj₁ x , z) ⃗) = refl
  eval≡interp dist ((inj₂ y , z) ⃗) = refl
  eval≡interp dist (inj₁ (x , z) ⃖) = refl
  eval≡interp dist (inj₂ (y , z) ⃖) = refl
  eval≡interp factor (inj₁ (x , z) ⃗) = refl
  eval≡interp factor (inj₂ (y , z) ⃗) = refl
  eval≡interp factor ((inj₁ x , z) ⃖) = refl
  eval≡interp factor ((inj₂ y , z) ⃖) = refl
  eval≡interp id↔ (v ⃗) = refl
  eval≡interp id↔ (v ⃖) = refl
  eval≡interp η₊ (inj₁ x ⃖) = refl
  eval≡interp η₊ (inj₂ (- x) ⃖) = refl
  eval≡interp ε₊ (inj₁ x ⃗) = refl
  eval≡interp ε₊ (inj₂ (- x) ⃗) = refl
  eval≡interp (ηₓ v) (tt ⃗) = refl
  eval≡interp (ηₓ v) ((v' , ↻) ⃖) with v ≟ v'
  ... | yes refl = refl
  ... | no  neq  = refl
  eval≡interp (εₓ v) ((v' , ↻) ⃗) with v ≟ v'
  ... | yes refl = refl
  ... | no  neq  = refl
  eval≡interp (εₓ v) (tt ⃖) = refl
  eval≡interp (c₁ ⨾ c₂) (a ⃗) with interp c₁ (a ⃗) | inspect (interp c₁) (a ⃗)
  eval≡interp (c₁ ⨾ c₂) (a ⃗) | just (b ⃗)  | [ eq₁ ] = lem
    where
    rs : ⟨ c₁ ⨾ c₂ ∣ a ∣ ☐ ⟩▷ ↦* ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷
    rs = ↦⃗₃ ∷ appendκ↦* ((getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (a ⃗)) eq₁))) (λ ()) (λ ()) refl (☐⨾ c₂ • ☐)

    rs' : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* (toState (c₁ ⨾ c₂) (eval (c₁ ⨾ c₂) (a ⃗)))
    rs' = proj₁ (deterministic*' rs (getₜᵣ⃗ (c₁ ⨾ c₂) refl) (is-stuck-toState _ _))

    lem : eval (c₁ ⨾ c₂) (a ⃗) ≡ (c₁ ⨾[ b ⃗]⨾ c₂)
    lem = proj₁ (loop (len↦ rs') b) rs' refl
  eval≡interp (c₁ ⨾ c₂) (a ⃗) | just (a₁ ⃖) | [ eq₁ ] = lem
    where
    rs : ⟨ c₁ ⨾ c₂ ∣ a ∣ ☐ ⟩▷ ↦* ⟨ c₁ ⨾ c₂ ∣ a₁ ∣ ☐ ⟩◁
    rs = ↦⃗₃ ∷ appendκ↦* ((getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (a ⃗)) eq₁))) (λ ()) (λ ()) refl (☐⨾ c₂ • ☐) ++↦ ↦⃖₃ ∷ ◾

    lem : eval (c₁ ⨾ c₂) (a ⃗) ≡ just (a₁ ⃖)
    lem = eval-toState₁ rs
  eval≡interp (c₁ ⨾ c₂) (a ⃗) | nothing     | [ eq₁ ] = lem
    where
    rs' : ⟨ c₁ ⨾ c₂ ∣ a ∣ ☐ ⟩▷ ↦* ⊠
    rs' = ↦⃗₃ ∷ appendκ↦*⊠ ((getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (a ⃗)) eq₁))) (λ ()) (☐⨾ c₂ • ☐)

    lem : eval (c₁ ⨾ c₂) (a ⃗) ≡ nothing
    lem = eval-toState₁ rs'
  eval≡interp (c₁ ⨾ c₂) (c ⃖) with interp c₂ (c ⃖) | inspect (interp c₂) (c ⃖)
  eval≡interp (c₁ ⨾ c₂) (c ⃖) | just (c' ⃗) | [ eq' ] = lem
    where
    rs' : ［ c₁ ⨾ c₂ ∣ c ∣ ☐ ］◁ ↦* ［ c₁ ⨾ c₂ ∣ c' ∣ ☐ ］▷
    rs' = ↦⃖₁₀ ∷ appendκ↦* ((getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (c ⃖)) eq'))) (λ ()) (λ ()) refl (c₁ ⨾☐• ☐) ++↦ ↦⃗₁₀ ∷ ◾

    lem : eval (c₁ ⨾ c₂) (c ⃖) ≡ just (c' ⃗)
    lem = eval-toState₂ rs'
  eval≡interp (c₁ ⨾ c₂) (c ⃖) | just (b ⃖)  | [ eq' ] = lem
    where
    rs : ［ c₁ ⨾ c₂ ∣ c ∣ ☐ ］◁ ↦* ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁
    rs = ↦⃖₁₀ ∷ appendκ↦* ((getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (c ⃖)) eq'))) (λ ()) (λ ()) refl (c₁ ⨾☐• ☐)

    rs' : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* (toState (c₁ ⨾ c₂) (eval (c₁ ⨾ c₂) (c ⃖)))
    rs' = proj₁ (deterministic*' rs (getₜᵣ⃖ (c₁ ⨾ c₂) refl) (is-stuck-toState _ _))

    lem : eval (c₁ ⨾ c₂) (c ⃖) ≡ (c₁ ⨾[ b ⃖]⨾ c₂)
    lem = proj₂ (loop (len↦ rs') b) rs' refl
  eval≡interp (c₁ ⨾ c₂) (c ⃖) | nothing     | [ eq' ] = lem
    where
    rs' : ［ c₁ ⨾ c₂ ∣ c ∣ ☐ ］◁ ↦* ⊠
    rs' = ↦⃖₁₀ ∷ appendκ↦*⊠ ((getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (c ⃖)) eq'))) (λ ()) (c₁ ⨾☐• ☐)

    lem : eval (c₁ ⨾ c₂) (c ⃖) ≡ nothing
    lem = eval-toState₂ rs'
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃗) with interp c₁ (x ⃗) | inspect (interp c₁) (x ⃗)
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃗) | just (x₁ ⃗) | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ⟩▷ ↦* ［ c₁ ⊕ c₂ ∣ inj₁ x₁ ∣ ☐ ］▷
    rs' = ↦⃗₄ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ ↦⃗₁₁ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃗) | just (x₁ ⃖) | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ⟩▷ ↦* ⟨ c₁ ⊕ c₂ ∣ inj₁ x₁ ∣ ☐ ⟩◁
    rs' = ↦⃗₄ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ ↦⃖₄ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃗) | nothing      | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ⟩▷ ↦* ⊠
    rs' = ↦⃗₄ ∷ appendκ↦*⊠ (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (☐⊕ c₂ • ☐)
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃗) with interp c₂ (y ⃗) | inspect (interp c₂) (y ⃗)
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃗) | just (y₁ ⃗) | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ⟩▷ ↦* ［ c₁ ⊕ c₂ ∣ inj₂ y₁ ∣ ☐ ］▷
    rs' = ↦⃗₅ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₁)) (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ ↦⃗₁₂ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃗) | just (y₁ ⃖) | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ⟩▷ ↦* ⟨ c₁ ⊕ c₂ ∣ inj₂ y₁ ∣ ☐ ⟩◁
    rs' = ↦⃗₅ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₁)) (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ ↦⃖₅ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃗) | nothing      | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ⟩▷ ↦* ⊠
    rs' = ↦⃗₅ ∷ appendκ↦*⊠ (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₁)) (λ ()) (c₁ ⊕☐• ☐)
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃖) with interp c₁ (x ⃖) | inspect (interp c₁) (x ⃖)
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃖) | just (x₁ ⃗) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ］◁ ↦* ［ c₁ ⊕ c₂ ∣ inj₁ x₁ ∣ ☐ ］▷
    rs' = ↦⃖₁₁ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ ↦⃗₁₁ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃖) | just (x₁ ⃖) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ］◁ ↦* ⟨ c₁ ⊕ c₂ ∣ inj₁ x₁ ∣ ☐ ⟩◁
    rs' = ↦⃖₁₁ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (λ ()) refl (☐⊕ c₂ • ☐) ++↦ ↦⃖₄ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₁ x ⃖) | nothing     | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ ☐ ］◁ ↦* ⊠
    rs' = ↦⃖₁₁ ∷ appendκ↦*⊠ (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (☐⊕ c₂ • ☐)
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃖) with interp c₂ (y ⃖) | inspect (interp c₂) (y ⃖)
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃖) | just (y₁ ⃗) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ］◁ ↦* ［ c₁ ⊕ c₂ ∣ inj₂ y₁ ∣ ☐ ］▷
    rs' = ↦⃖₁₂ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₁)) (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ ↦⃗₁₂ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃖) | just (y₁ ⃖) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ］◁ ↦* ⟨ c₁ ⊕ c₂ ∣ inj₂ y₁ ∣ ☐ ⟩◁
    rs' = ↦⃖₁₂ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₁)) (λ ()) (λ ()) refl (c₁ ⊕☐• ☐) ++↦ ↦⃖₅ ∷ ◾
  eval≡interp (c₁ ⊕ c₂) (inj₂ y ⃖) | nothing     | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ ☐ ］◁ ↦* ⊠
    rs' = ↦⃖₁₂ ∷ appendκ↦*⊠ (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₁)) (λ ()) (c₁ ⊕☐• ☐)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) with interp c₁ (x ⃗) | inspect (interp c₁) (x ⃗)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | just (x₁ ⃗) | [ eq₁ ] with interp c₂ (y ⃗) | inspect (interp c₂) (y ⃗)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | just (x₁ ⃗) | [ eq₁ ] | just (y₁ ⃗) | [ eq₂ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ⟩▷ ↦* ［ c₁ ⊗ c₂ ∣ (x₁ , y₁) ∣ ☐ ］▷
    rs' = ↦⃗₆ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐) ++↦
          ↦⃗₈ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x₁ ]⊗☐• ☐) ++↦ ↦⃗₉ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | just (x₁ ⃗) | [ eq₁ ] | just (y₁ ⃖) | [ eq₂ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ⟩▷ ↦* ⟨ c₁ ⊗ c₂ ∣ (x , y₁) ∣ ☐ ⟩◁
    rs' = ↦⃗₆ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐) ++↦
          ↦⃗₈ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x₁ ]⊗☐• ☐) ++↦
          ↦⃖₈ ∷ Rev* (appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y₁ ]• ☐)) (λ ()) (λ ()) ++↦ ↦⃖₆ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | just (x₁ ⃗) | [ eq₁ ] | nothing     | [ eq₂ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ⟩▷ ↦* ⊠
    rs' = ↦⃗₆ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐) ++↦
          ↦⃗₈ ∷ appendκ↦*⊠ (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (y ⃗)) eq₂)) (λ ()) ([ c₁ , x₁ ]⊗☐• ☐)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | just (x₁ ⃖) | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ⟩▷ ↦* ⟨ c₁ ⊗ c₂ ∣ (x₁ , y) ∣ ☐ ⟩◁
    rs' = ↦⃗₆ ∷ appendκ↦* (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y ]• ☐) ++↦ ↦⃖₆ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃗) | nothing     | [ eq₁ ] = eval-toState₁ rs'
    where
    rs' : ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ⟩▷ ↦* ⊠
    rs' = ↦⃗₆ ∷ appendκ↦*⊠ (getₜᵣ⃗ c₁ (trans (eval≡interp c₁ (x ⃗)) eq₁)) (λ ()) (☐⊗[ c₂ , y ]• ☐)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) with interp c₂ (y ⃖) | inspect (interp c₂) (y ⃖)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | just (y₁ ⃗) | [ eq₂ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ］◁ ↦* ［ c₁ ⊗ c₂ ∣ (x , y₁) ∣ ☐ ］▷
    rs' = ↦⃖₉ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x ]⊗☐• ☐) ++↦ ↦⃗₉ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | just (y₁ ⃖) | [ eq₂ ] with interp c₁ (x ⃖) | inspect (interp c₁) (x ⃖)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | just (y₁ ⃖) | [ eq₂ ] | just (x₁ ⃗) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ］◁ ↦* ［ c₁ ⊗ c₂ ∣ (x₁ , y) ∣ ☐ ］▷
    rs' = ↦⃖₉ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x ]⊗☐• ☐) ++↦
          ↦⃖₈ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y₁ ]• ☐) ++↦
          ↦⃗₈ ∷ Rev* (appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x₁ ]⊗☐• ☐)) (λ ()) (λ ()) ++↦ ↦⃗₉ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | just (y₁ ⃖) | [ eq₂ ] | just (x₁ ⃖) | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ］◁ ↦* ⟨ c₁ ⊗ c₂ ∣ (x₁ , y₁) ∣ ☐ ⟩◁
    rs' = ↦⃖₉ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x ]⊗☐• ☐) ++↦
          ↦⃖₈ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (λ ()) refl (☐⊗[ c₂ , y₁ ]• ☐) ++↦ ↦⃖₆ ∷ ◾
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | just (y₁ ⃖) | [ eq₂ ] | nothing     | [ eq₁ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ］◁ ↦* ⊠
    rs' = ↦⃖₉ ∷ appendκ↦* (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) (λ ()) refl ([ c₁ , x ]⊗☐• ☐) ++↦
          ↦⃖₈ ∷ appendκ↦*⊠ (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (x ⃖)) eq₁)) (λ ()) (☐⊗[ c₂ , y₁ ]• ☐)
  eval≡interp (c₁ ⊗ c₂) ((x , y) ⃖) | nothing     | [ eq₂ ] = eval-toState₂ rs'
    where
    rs' : ［ c₁ ⊗ c₂ ∣ (x , y) ∣ ☐ ］◁ ↦* ⊠
    rs' = ↦⃖₉ ∷ appendκ↦*⊠ (getₜᵣ⃖ c₂ (trans (eval≡interp c₂ (y ⃖)) eq₂)) (λ ()) ([ c₁ , x ]⊗☐• ☐)

  private
    loop : ∀ {A B C x} {c₁ : A ↔ B} {c₂ : B ↔ C} (n : ℕ)
         → ∀ b → ((rs : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* toState (c₁ ⨾ c₂) x) → len↦ rs ≡ n → x ≡ c₁ ⨾[ b ⃗]⨾ c₂)
               × ((rs : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* toState (c₁ ⨾ c₂) x) → len↦ rs ≡ n → x ≡ c₁ ⨾[ b ⃖]⨾ c₂)
    loop {A} {B} {C} {x} {c₁} {c₂} = <′-rec (λ n → _) loop-rec
      where
      loop-rec : (n : ℕ) → (∀ m → m <′ n → _) → _
      loop-rec n R b = loop₁ , loop₂
        where
        loop₁ : (rs : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* toState (c₁ ⨾ c₂) x) → len↦ rs ≡ n → x ≡ c₁ ⨾[ b ⃗]⨾ c₂
        loop₁ rs refl with interp c₂ (b ⃗) | inspect (interp c₂) (b ⃗)
        loop₁ rs refl | just (c ⃗)  | [ eq ] = toState≡₁ (deterministic* rs rs' (is-stuck-toState _ _) (λ ()))
          where
          rs' : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* ［ c₁ ⨾ c₂ ∣ c ∣ ☐ ］▷
          rs' = ↦⃗₇ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (b ⃗)) eq)) (λ ()) (λ ()) refl (c₁ ⨾☐• ☐) ++↦ ↦⃗₁₀ ∷ ◾
        loop₁ rs refl | just (b' ⃖) | [ eq ] = proj₂ (R (len↦ rs'') le b') rs'' refl
          where
          rs' : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* ⟨ c₂ ∣ b' ∣ c₁ ⨾☐• ☐ ⟩◁
          rs' = ↦⃗₇ ∷ appendκ↦* (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (b ⃗)) eq)) (λ ()) (λ ()) refl (c₁ ⨾☐• ☐)

          rs'' : ⟨ c₂ ∣ b' ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* toState (c₁ ⨾ c₂) x
          rs'' = proj₁ (deterministic*' rs' rs (is-stuck-toState _ _))

          req : len↦ rs ≡ len↦ rs' + len↦ rs''
          req = proj₂ (deterministic*' rs' rs (is-stuck-toState _ _))

          le : len↦ rs'' <′ len↦ rs
          le rewrite req = s≤′s (n≤′m+n _ _)
        loop₁ rs refl | nothing     | [ eq ] = toState≡₃ (deterministic* rs rs' (is-stuck-toState _ _) (λ ()))
          where
          rs' : ［ c₁ ∣ b ∣ ☐⨾ c₂ • ☐ ］▷ ↦* ⊠
          rs' = ↦⃗₇ ∷ appendκ↦*⊠ (getₜᵣ⃗ c₂ (trans (eval≡interp c₂ (b ⃗)) eq)) (λ ()) (c₁ ⨾☐• ☐)
        loop₂ : (rs : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* toState (c₁ ⨾ c₂) x) → len↦ rs ≡ n → x ≡ c₁ ⨾[ b ⃖]⨾ c₂
        loop₂ rs refl with interp c₁ (b ⃖) | inspect (interp c₁) (b ⃖)
        loop₂ rs refl | just (b' ⃗) | [ eq ] = proj₁ (R (len↦ rs'') le b') rs'' refl
          where
          rs' : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* ［ c₁ ∣ b' ∣ ☐⨾ c₂ • ☐ ］▷
          rs' = ↦⃖₇ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (b ⃖)) eq)) (λ ()) (λ ()) refl (☐⨾ c₂ • ☐)

          rs'' : ［ c₁ ∣ b' ∣ ☐⨾ c₂ • ☐ ］▷ ↦* toState (c₁ ⨾ c₂) x
          rs'' = proj₁ (deterministic*' rs' rs (is-stuck-toState _ _))

          req : len↦ rs ≡ len↦ rs' + len↦ rs''
          req = proj₂ (deterministic*' rs' rs (is-stuck-toState _ _))

          le : len↦ rs'' <′ len↦ rs
          le rewrite req = s≤′s (n≤′m+n _ _)
        loop₂ rs refl | just (a ⃖)  | [ eq ] = toState≡₂ (deterministic* rs rs' (is-stuck-toState _ _) (λ ()))
          where
          rs' : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* ⟨ c₁ ⨾ c₂ ∣ a ∣ ☐ ⟩◁
          rs' = ↦⃖₇ ∷ appendκ↦* (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (b ⃖)) eq)) (λ ()) (λ ()) refl (☐⨾ c₂ • ☐) ++↦ ↦⃖₃ ∷ ◾
        loop₂ rs refl | nothing     | [ eq ] = toState≡₃ (deterministic* rs rs' (is-stuck-toState _ _) (λ ()))
          where
          rs' : ⟨ c₂ ∣ b ∣ c₁ ⨾☐• ☐ ⟩◁ ↦* ⊠
          rs' = ↦⃖₇ ∷ appendκ↦*⊠ (getₜᵣ⃖ c₁ (trans (eval≡interp c₁ (b ⃖)) eq)) (λ ()) (☐⨾ c₂ • ☐)


text:
-- Proof irrelevance is nice when you want to work with subsets.
module Subset where

data True : Prop where
  tt : True

data False : Prop where

data (|) (A:Set)(P:A -> Prop) : Set where
  sub : (x:A) -> P x -> A | P

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

mutual
  IsEven : Nat -> Prop
  IsEven  zero   = True
  IsEven (suc n) = IsOdd n

  IsOdd : Nat -> Prop
  IsOdd  zero   = False
  IsOdd (suc n) = IsEven n

Even : Set
Even = Nat | IsEven

Odd : Set
Odd = Nat | IsOdd

(+) : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Document renderers
------------------------------------------------------------------------

{-# OPTIONS --guardedness #-}

module Renderer where

open import Algebra
open import Data.Bool
open import Data.Char using (Char)
open import Data.Empty
open import Data.Integer using (ℤ; +_; -[1+_]; _-_; _⊖_)
open import Data.List as List hiding ([_])
open import Data.List.NonEmpty using (_∷⁺_)
open import Data.List.Properties
open import Data.Nat
open import Data.Product
open import Data.String as String using (String)
open import Data.Unit
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (module Inverse)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
open import Tactic.MonoidSolver

private
  module LM {A : Set} = Monoid (++-monoid A)

open import Grammar.Infinite as G hiding (_⊛_; _<⊛_; _⊛>_)
open import Pretty using (Doc; Docs; Pretty-printer)
open Pretty.Doc
open Pretty.Docs
open import Utilities

------------------------------------------------------------------------
-- Renderers

record Renderer : Set₁ where
  field
    -- The function that renders.

    render : ∀ {A} {g : Grammar A} {x : A} → Doc g x → List Char

    -- The rendered string must be parsable.

    parsable : ∀ {A} {g : Grammar A} {x : A}
               (d : Doc g x) → x ∈ g · render d

  ----------------------------------------------------------------------
  -- Some derived definitions and properties

  -- Pretty-printers are correct by definition, for any renderer,
  -- assuming that the underlying grammar is unambiguous.

  correct :
    ∀ {A} {g : Grammar A} (pretty : Pretty-printer g) →
    ∀ x → x ∈ g · render (pretty x)
  correct pretty x = parsable (pretty x)

  correct-if-locally-unambiguous :
    ∀ {A} {g : Grammar A} →
    (parse : Parser g) (pretty : Pretty-printer g) →
    ∀ x →
    Locally-unambiguous g (render (pretty x)) →
    ∃ λ p → parse (render (pretty x)) ≡ yes (x , p)
  correct-if-locally-unambiguous parse pretty x unambiguous = c
    where
    c : ∃ λ p → parse (render (pretty x)) ≡ yes (x , p)
    c with parse (render (pretty x))
    c | no  no-parse   = ⊥-elim (no-parse (x , correct pretty x))
    c | yes (y  , y∈g) with unambiguous y∈g (correct pretty x)
    c | yes (.x , x∈g) | P.refl = (x∈g , P.refl)

  correct-if-unambiguous :
    ∀ {A} {g : Grammar A} →
    Unambiguous g → (parse : Parser g) (pretty : Pretty-printer g) →
    ∀ x → ∃ λ p → parse (render (pretty x)) ≡ yes (x , p)
  correct-if-unambiguous unambiguous parse pretty x =
    correct-if-locally-unambiguous parse pretty x unambiguous

  -- If there is only one grammatically correct string, then the
  -- renderer returns this string.

  render-unique-string : ∀ {A} {g : Grammar A} {x s} →
                         (∀ {s′} → x ∈ g · s′ → s′ ≡ s) →
                         (d : Doc g x) → render d ≡ s
  render-unique-string unique d = unique (parsable d)

  -- Thus, in particular, documents for the grammar "string s" are
  -- always rendered in the same way.

  render-string : ∀ {s s′} (d : Doc (string s) s′) → render d ≡ s
  render-string = render-unique-string λ s′∈ →
    P.sym $ proj₂ (Inverse.to string-sem′ ⟨$⟩ s′∈)

  -- The property of ignoring (top-level) emb constructors.

  Ignores-emb : Set₁
  Ignores-emb =
    ∀ {A B x y} {g₁ : Grammar A} {g₂ : Grammar B}
      {f : ∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s} {d : Doc g₁ x} →
    render (emb f d) ≡ render d

  -- If the renderer ignores emb constructors then, for every valid
  -- string, there is a document that renders as that string. (The
  -- renderers below ignore emb.)

  every-string-possible :
    Ignores-emb →
    ∀ {A} {g : Grammar A} {x s} →
    x ∈ g · s → ∃ λ (d : Doc g x) → render d ≡ s
  every-string-possible ignores-emb {g = g} {x} {s} x∈ =
    (Pretty.embed lemma₁ text , lemma₂)
    where
    open P.≡-Reasoning

    lemma₁ : ∀ {s′} → s ∈ string s · s′ → x ∈ g · s′
    lemma₁ s∈ = cast (proj₂ (Inverse.to string-sem′ ⟨$⟩ s∈)) x∈

    lemma₂ = begin
      render (Pretty.embed lemma₁ text)  ≡⟨ ignores-emb ⟩
      render text                        ≡⟨ render-string _ ⟩
      s                                  ∎

------------------------------------------------------------------------
-- An example renderer

-- This renderer renders every occurrence of "line" as a single space
-- character.

ugly-renderer : Renderer
ugly-renderer = record
  { render   = render
  ; parsable = parsable
  }
  where

  mutual

    render : ∀ {A} {g : Grammar A} {x} → Doc g x → List Char
    render (d₁ ◇ d₂)      = render d₁ ++ render d₂
    render (text {s = s}) = s
    render line           = String.toList " "
    render (group d)      = render d
    render (nest _ d)     = render d
    render (emb _ d)      = render d
    render (fill ds)      = render-fills ds

    render-fills : ∀ {A} {g : Grammar A} {x} → Docs g x → List Char
    render-fills [ d ]    = render d
    render-fills (d ∷ ds) = render d ++ ' ' ∷ render-fills ds

  mutual

    parsable : ∀ {A x} {g : Grammar A}
               (d : Doc g x) → x ∈ g · render d
    parsable (d₁ ◇ d₂)  = >>=-sem (parsable d₁) (parsable d₂)
    parsable text       = string-sem
    parsable line       = <$-sem single-space-sem
    parsable (group d)  = parsable d
    parsable (nest _ d) = parsable d
    parsable (emb f d)  = f (parsable d)
    parsable (fill ds)  = parsable-fills ds

    parsable-fills : ∀ {A xs} {g : Grammar A} (ds : Docs g xs) →
                     xs ∈ g sep-by whitespace + · render-fills ds
    parsable-fills [ d ]    = sep-by-sem-singleton (parsable d)
    parsable-fills (d ∷ ds) =
      sep-by-sem-∷ (parsable d) single-space-sem (parsable-fills ds)

-- The "ugly renderer" ignores emb constructors.

ugly-renderer-ignores-emb : Renderer.Ignores-emb ugly-renderer
ugly-renderer-ignores-emb = P.refl

------------------------------------------------------------------------
-- A general document property, proved using ugly-renderer

-- For every document of type Doc g x there is a string that witnesses
-- that the value x is generated by the grammar g.

string-exists : ∀ {A} {g : Grammar A} {x} →
                Doc g x → ∃ λ s → x ∈ g · s
string-exists d = (render d , parsable d)
  where open Renderer ugly-renderer

------------------------------------------------------------------------
-- An example renderer, based on the one in Wadler's "A prettier
-- printer"

module Wadler's-renderer where

  -- Layouts (representations of certain strings).

  data Layout-element : Set where
    text : List Char → Layout-element
    line : ℕ         → Layout-element

  Layout : Set
  Layout = List Layout-element

  -- Conversion of layouts into strings.

  show-element : Layout-element → List Char
  show-element (text s) = s
  show-element (line i) = '\n' ∷ replicate i ' '

  show : Layout → List Char
  show = concat ∘ List.map show-element

  -- Documents with unions instead of groups, and no fills. An extra
  -- index—the nesting level—is also included, and the line
  -- combinator's type is more precise (it can't be used for single
  -- spaces, only for newline-plus-indentation).

  infixr 20 _◇_

  data DocN : ∀ {A} → ℕ → Grammar A → A → Set₁ where
    _◇_   : ∀ {i c₁ c₂ A B x y}
              {g₁ : ∞Grammar c₁ A} {g₂ : A → ∞Grammar c₂ B} →
            DocN i (♭? g₁) x → DocN i (♭? (g₂ x)) y →
            DocN i (g₁ >>= g₂) y
    text  : ∀ {i} (s : List Char) → DocN i (string s) s
    line  : (i : ℕ) →
            let s = show-element (line i) in
            DocN i (string s) s
    union : ∀ {i A} {g : Grammar A} {x} →
            DocN i g x → DocN i g x → DocN i g x
    nest  : ∀ {i A} {g : Grammar A} {x}
            (j : ℕ) → DocN (j + i) g x → DocN i g x
    emb   : ∀ {i A B} {g₁ : Grammar A} {g₂ : Grammar B} {x y} →
            (∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) →
            DocN i g₁ x → DocN i g₂ y

  -- Some derived combinators.

  infix  21 <$>_
  infixl 20 _⊛_ _⊛>_

  embed : ∀ {i A B} {g₁ : Grammar A} {g₂ : Grammar B} {x y} →
          (∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) → DocN i g₁ x → DocN i g₂ y
  embed f (emb g d) = emb (f ∘ g) d
  embed f d         = emb f d

  nil : ∀ {i A} {x : A} → DocN i (return x) x
  nil = embed lemma (text [])
    where
    lemma : ∀ {x s} → [] ∈ string [] · s → x ∈ return x · s
    lemma return-sem = return-sem

  <$>_ : ∀ {i c A B} {f : A → B} {x} {g : ∞Grammar c A} →
         DocN i (♭? g) x → DocN i (f <$> g) (f x)
  <$> d = embed <$>-sem d

  _⊛_ : ∀ {i c₁ c₂ A B f x} {g₁ : ∞Grammar c₁ (A → B)}
          {g₂ : ∞Grammar c₂ A} →
        DocN i (♭? g₁) f → DocN i (♭? g₂) x → DocN i (g₁ G.⊛ g₂) (f x)
  _⊛_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ <$> d₂)
    where
    lemma : ∀ {x s} →
            x ∈ (g₁ >>= λ f → f <$> g₂) · s → x ∈ g₁ G.⊛ g₂ · s
    lemma (>>=-sem f∈ (<$>-sem x∈)) = ⊛-sem f∈ x∈

  _⊛>_ : ∀ {i c₁ c₂ A B x y} {g₁ : ∞Grammar c₁ A}
           {g₂ : ∞Grammar c₂ B} →
         DocN i (♭? g₁) x → DocN i (♭? g₂) y → DocN i (g₁ G.⊛> g₂) y
  _⊛>_ {g₁ = g₁} {g₂} d₁ d₂ =
    embed lemma (nil ⊛ d₁ ⊛ d₂)
    where
    lemma : ∀ {y s} →
            y ∈ return (λ _ x → x) G.⊛ g₁ G.⊛ g₂ · s →
            y ∈ g₁ G.⊛> g₂ · s
    lemma (⊛-sem (⊛-sem return-sem x∈) y∈) = ⊛>-sem x∈ y∈

  cons : ∀ {i A B} {g : Grammar A} {sep : Grammar B} {x xs} →
         DocN i g x → DocN i (tt <$ sep) tt → DocN i (g sep-by sep) xs →
         DocN i (g sep-by sep) (x ∷⁺ xs)
  cons {g = g} {sep} d₁ d₂ d₃ =
    embed lemma (<$> d₁ ⊛ (d₂ ⊛> d₃))
    where
    lemma : ∀ {ys s} →
            ys ∈ _∷⁺_ <$> g G.⊛ ((tt <$ sep) G.⊛> (g sep-by sep)) · s →
            ys ∈ g sep-by sep · s
    lemma (⊛-sem (<$>-sem x∈) (⊛>-sem (<$-sem y∈) xs∈)) =
      sep-by-sem-∷ x∈ y∈ xs∈

  -- A single space character.

  imprecise-space : ∀ {i} → DocN i (tt <$ whitespace +) tt
  imprecise-space = embed lemma (text (String.toList " "))
    where
    lemma : ∀ {s} →
            String.toList " " ∈ string′ " " · s →
            tt ∈ tt <$ whitespace + · s
    lemma s∈ =
      cast (proj₂ (Inverse.to string-sem′ ⟨$⟩ s∈))
           (<$-sem single-space-sem)

  -- A variant of line that has the same type as Pretty.line (except
  -- for the indentation index).

  imprecise-line : (i : ℕ) → DocN i (tt <$ whitespace +) tt
  imprecise-line i = embed lemma (line i)
    where
    replicate-lemma :
      ∀ i → replicate i ' ' ∈ whitespace ⋆ · replicate i ' '
    replicate-lemma zero    = ⋆-[]-sem
    replicate-lemma (suc i) =
      ⋆-∷-sem (left-sem tok-sem) (replicate-lemma i)

    lemma : ∀ {i s′} →
            let s = show-element (line i) in
            s ∈ string s · s′ → tt ∈ tt <$ whitespace + · s′
    lemma s∈ =
      cast (proj₂ (Inverse.to string-sem′ ⟨$⟩ s∈))
           (<$-sem (+-sem (right-sem tok-sem) (replicate-lemma _)))

  mutual

    -- Replaces line constructors with single spaces, removes groups.

    flatten : ∀ {i A} {g : Grammar A} {x} → Doc g x → DocN i g x
    flatten (d₁ ◇ d₂)  = flatten d₁ ◇ flatten d₂
    flatten text       = text _
    flatten line       = imprecise-space
    flatten (group d)  = flatten d
    flatten (nest _ d) = flatten d
    flatten (emb f d)  = embed f (flatten d)
    flatten (fill ds)  = flatten-fills ds

    flatten-fills : ∀ {i A} {g : Grammar A} {xs} →
                    Docs g xs → DocN i (g sep-by whitespace +) xs
    flatten-fills [ d ]    = embed sep-by-sem-singleton (flatten d)
    flatten-fills (d ∷ ds) =
      cons (flatten d) imprecise-space (flatten-fills ds)

  mutual

    -- Converts ("expands") groups to unions.

    expand : ∀ {i A} {g : Grammar A} {x} → Doc g x → DocN i g x
    expand (d₁ ◇ d₂)  = expand d₁ ◇ expand d₂
    expand text       = text _
    expand line       = imprecise-line _
    expand (group d)  = union (flatten d) (expand d)
    expand (nest j d) = nest j (expand d)
    expand (emb f d)  = embed f (expand d)
    expand (fill ds)  = expand-fills false ds

    expand-fills : Bool → -- Unconditionally flatten the first document?
                   ∀ {i A} {g : Grammar A} {xs} →
                   Docs g xs → DocN i (g sep-by whitespace +) xs
    expand-fills fl [ d ] =
      embed sep-by-sem-singleton (flatten/expand fl d)
    expand-fills fl (d ∷ ds) =
      union (cons (flatten d)           imprecise-space    (expand-fills true  ds))
            (cons (flatten/expand fl d) (imprecise-line _) (expand-fills false ds))

    flatten/expand : Bool → -- Flatten?
                     ∀ {i A} {g : Grammar A} {x} → Doc g x → DocN i g x
    flatten/expand true  d = flatten d
    flatten/expand false d = expand d

  -- Does the first line of the layout fit on a line with the given
  -- number of characters?

  fits : ℤ → Layout → Bool
  fits -[1+ w ] _            = false
  fits w        []           = true
  fits w        (text s ∷ x) = fits (w - + length s) x
  fits w        (line i ∷ x) = true

  module _ (width : ℕ) where

    -- Chooses the first layout if it fits, otherwise the second. The
    -- natural number is the current column number.

    better : ℕ → Layout → Layout → Layout
    better c x y = if fits (width ⊖ c) x then x else y

    -- If, for any starting column c, κ c is the layout for some text,
    -- then best i d κ c is the layout for the document d followed by
    -- this text, given the current indentation i and the current column
    -- number c.

    best : ∀ {i A} {g : Grammar A} {x} →
           DocN i g x → (ℕ → Layout) → (ℕ → Layout)
    best (d₁ ◇ d₂)     = best d₁ ∘ best d₂
    best (text [])     = id
    best (text s)      = λ κ c → text s ∷ κ (length s + c)
    best (line i)      = λ κ _ → line i ∷ κ i
    best (union d₁ d₂) = λ κ c → better c (best d₁ κ c)
                                          (best d₂ κ c)
    best (nest _ d)    = best d
    best (emb _ d)     = best d

    -- Renders a document.

    renderN : ∀ {A i} {g : Grammar A} {x} → DocN i g x → List Char
    renderN d = show (best d (λ _ → []) 0)

    -- Renders a document.

    render : ∀ {A} {g : Grammar A} {x} → Doc g x → List Char
    render d = renderN (expand {i = 0} d)

    -- A simple lemma.

    if-lemma :
      ∀ {A} {g : Grammar A} {x l₁ l₂} s b →
      x ∈ g · s ++ show l₁ →
      x ∈ g · s ++ show l₂ →
      x ∈ g · s ++ show (if b then l₁ else l₂)
    if-lemma _ true  ∈l₁ ∈l₂ = ∈l₁
    if-lemma _ false ∈l₁ ∈l₂ = ∈l₂

    -- The main correctness property for best.

    best-lemma :
      ∀ {c A B i} {g : Grammar A} {g′ : Grammar B} {x y κ}
        s (d : DocN i g x) →
      (∀ {s′ c′} → x ∈ g · s′ → y ∈ g′ · s ++ s′ ++ show (κ c′)) →
      y ∈ g′ · s ++ show (best d κ c)
    best-lemma     s (text [])      hyp = hyp return-sem
    best-lemma     s (text (_ ∷ _)) hyp = hyp string-sem
    best-lemma     s (line i)       hyp = hyp string-sem
    best-lemma {c} s (union d₁ d₂)  hyp = if-lemma s
                                            (fits (width ⊖ c) _)
                                            (best-lemma s d₁ hyp)
                                            (best-lemma s d₂ hyp)
    best-lemma     s (nest _ d)     hyp = best-lemma s d hyp
    best-lemma     s (emb f d)      hyp = best-lemma s d (hyp ∘ f)
    best-lemma     s (d₁ ◇ d₂)      hyp =
      best-lemma s d₁ λ {s′} f∈ →
        cast (LM.assoc s _ _)
          (best-lemma (s ++ s′) d₂ λ x∈ →
             cast lemma
               (hyp (>>=-sem f∈ x∈)))
      where
      lemma :
        ∀ {s′ s″ s‴} →
        s ++ (s′ ++ s″) ++ s‴ ≡ (s ++ s′) ++ s″ ++ s‴
      lemma = solve (++-monoid Char)

    -- A corollary.

    best-lemma′ :
      ∀ {A i} {g : Grammar A} {x}
      (d : DocN i g x) → x ∈ g · renderN d
    best-lemma′ d = best-lemma [] d (cast (P.sym $ proj₂ LM.identity _))

    -- The renderer is correct.

    parsable : ∀ {A} {g : Grammar A} {x}
               (d : Doc g x) → x ∈ g · render d
    parsable d = best-lemma′ (expand d)

    -- The renderer.

    wadler's-renderer : Renderer
    wadler's-renderer = record
      { render   = render
      ; parsable = parsable
      }

  -- The renderer ignores emb constructors.

  ignores-emb :
    ∀ {w} → Renderer.Ignores-emb (wadler's-renderer w)
  ignores-emb {d = d} with expand {i = 0} d
  ... | _ ◇ _     = P.refl
  ... | text _    = P.refl
  ... | line ._   = P.refl
  ... | union _ _ = P.refl
  ... | nest _ _  = P.refl
  ... | emb _ _   = P.refl

  -- A (heterogeneous) notion of document equivalence.

  infix 4 _≈_

  _≈_ : ∀ {A₁ i₁ g₁} {x₁ : A₁}
          {A₂ i₂ g₂} {x₂ : A₂} →
        DocN i₁ g₁ x₁ → DocN i₂ g₂ x₂ → Set
  d₁ ≈ d₂ = ∀ width → renderN width d₁ ≡ renderN width d₂

  -- Some laws satisfied by the DocN combinators.

  text-++ : ∀ {i₁ i₂} s₁ s₂ →
        text {i = i₁} (s₁ ++ s₂) ≈
        _⊛>_ {c₁ = false} {c₂ = false} (text {i = i₂} s₁) (text s₂)
  text-++ []        []        _ = P.refl
  text-++ []        (t₂ ∷ s₂) _ = P.refl
  text-++ (t₁ ∷ s₁) []        _ = lemma
    where
    lemma : ∀ {s₁} → (s₁ ++ []) ++ [] ≡ s₁ ++ []
    lemma = solve (++-monoid Char)
  text-++ (t₁ ∷ s₁) (t₂ ∷ s₂) _ = lemma (_ ∷ s₁)
    where
    lemma : ∀ s₁ {s₂} → (s₁ ++ s₂) ++ [] ≡ s₁ ++ s₂ ++ []
    lemma _ = solve (++-monoid Char)

  nest-union : ∀ {A i j g} {x : A} {d₁ d₂ : DocN (j + i) g x} →
               nest j (union d₁ d₂) ≈ union (nest j d₁) (nest j d₂)
  nest-union _ = P.refl

  union-◇ : ∀ {A B i x y c₁ c₂}
              {g₁ : ∞Grammar c₁ A} {g₂ : A → ∞Grammar c₂ B}
              {d₁ d₂ : DocN i (♭? g₁) x} {d₃ : DocN i (♭? (g₂ x)) y} →
            _◇_ {g₁ = g₁} {g₂ = g₂} (union d₁ d₂) d₃ ≈
            union (d₁ ◇ d₃) (_◇_ {g₁ = g₁} {g₂ = g₂} d₂ d₃)
  union-◇ _ = P.refl

  -- A law that is /not/ satisfied by the DocN combinators.

  ¬-◇-union :
    ¬ (∀ {A B i x y} c₁ c₂
         {g₁ : ∞Grammar c₁ A} {g₂ : A → ∞Grammar c₂ B}
       (d₁ : DocN i (♭? g₁) x) (d₂ d₃ : DocN i (♭? (g₂ x)) y) →
       _◇_ {g₁ = g₁} {g₂ = g₂} d₁ (union d₂ d₃) ≈
       union (d₁ ◇ d₂) (_◇_ {g₁ = g₁} {g₂ = g₂} d₁ d₃))
  ¬-◇-union hyp with hyp false false d₁ d₂ d₁ 0
    where
    d₁ = imprecise-line 0
    d₂ = imprecise-space

    -- The following four definitions are not part of the proof.

    left : DocN 0 _ _
    left = _◇_ {c₁ = false} {c₂ = false} d₁ (union d₂ d₁)

    right : DocN 0 _ _
    right = union (d₁ ◇ d₂) (_◇_ {c₁ = false} {c₂ = false} d₁ d₁)

    -- Note that left and right are not rendered in the same way.

    left-hand-string : renderN 0 left ≡ String.toList "\n\n"
    left-hand-string = P.refl

    right-hand-string : renderN 0 right ≡ String.toList "\n "
    right-hand-string = P.refl

  ... | ()

-- Uses Wadler's-renderer.render to render a document using the
-- given line width.

render : ∀ {A} {g : Grammar A} {x} → ℕ → Doc g x → String
render w d = String.fromList (Wadler's-renderer.render w d)

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
module Optics where
open import Agda.Primitive using (_⊔_; lsuc)
open import Data.Maybe using (Maybe; just)
open import Data.Sum using (_⊎_; inj₁)
open import Function using (const; id)
open import Category.Functor.Arr
open import Category.Functor.Const
open import Category.Functor.Either
open import Category.Profunctor.Joker
open import Category.Profunctor.Star

Optic : ∀ {l p} (c : (Set l → Set l → Set l) → Set p) (s t a b : Set l) → Set (lsuc l ⊔ p)
Optic {l} c s t a b = ∀ {p : Set l → Set l → Set l} (isClass : c p) → p a b → p s t

setOptic : ∀ {l p} (S T A B : Set l) {c : (Set l → Set l → Set l) → Set p} (isClass : c (Star (Arr B))) → Optic c S T A B → S → B → T
setOptic _ _ _ _ isClass l = l isClass (const id)

putOptic : ∀ {l p} (S T A B : Set l) {c : (Set l → Set l → Set l) → Set p} (isClass : c (Joker (Arr B))) → Optic c S T A B → B → T
putOptic _ _ _ _ isClass l = l isClass id

getOptic : ∀ {l p} (S T A B : Set l) {c : (Set l → Set l → Set l) → Set p} (isClass : c (Star (Const A))) → Optic c S T A B → S → A
getOptic _ _ _ _ isClass l = l isClass id

matchingOptic : ∀ {l p} (S T A B : Set l) {c : (Set l → Set l → Set l) → Set p} (isClass : c (Star (Either A))) → Optic c S T A B → S → A ⊎ T
matchingOptic _ _ _ _ isClass l = l isClass inj₁

previewOptic : ∀ {l p} (S T A B : Set l) {c : (Set l → Set l → Set l) → Set p} (isClass : c (Star (Const (Maybe A)))) → Optic c S T A B → S → Maybe A
previewOptic _ _ _ _ isClass l = l isClass just

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
{-# OPTIONS --safe #-}
module Cubical.Experiments.ZCohomologyExperiments where
open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.WedgeOfSpheres
open import Cubical.Foundations.Prelude

open import Cubical.HITs.Truncation
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.Data.Int
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma
open import Cubical.Foundations.Isomorphism
open import Cubical.Algebra.Group hiding (Int)

private

  ⋁-to : coHom 2 S²⋁S¹⋁S¹ → Int
  ⋁-to = Iso.fun (GroupIso.isom H²-S²⋁S¹⋁S¹)
  ⋁-from : Int → coHom 2 S²⋁S¹⋁S¹
  ⋁-from = Iso.inv (GroupIso.isom H²-S²⋁S¹⋁S¹)

  g : S²⋁S¹⋁S¹ → ∥ S₊ 2 ∥ 4
  g (inl x) = ∣ x ∣
  g (inr x) = 0ₖ 2
  g (push a i) = 0ₖ 2

  G = ∣ g ∣₂

{-
This computes:
⋁-to (⋁-from 1 +ₕ ⋁-from 1) ≡ 2
⋁-to = refl

We have ⋁-from 1 ≡ G and G is much simpler

But this does not compute:
test₀ : ⋁-to (G +ₕ G) ≡ 2
test₀ = refl

With the strange addition it does:
test₁ : ⋁-to (G +'ₕ G) ≡ 2
test₁ = refl
-}

-- Similar stuff happens with Sⁿ.
private
  S²-to : coHom 2 (S₊ 2) → Int
  S²-to = Iso.fun (GroupIso.isom (Hⁿ-Sⁿ≅ℤ 1))

  S²-from : Int → coHom 2 (S₊ 2)
  S²-from = Iso.inv (GroupIso.isom (Hⁿ-Sⁿ≅ℤ 1))

  one : coHom 2 (S₊ 2)
  one = ∣ ∣_∣ ∣₂

{-
Does not compute
test₂ : S²-to (S²-from 1 +ₕ S²-from 1) ≡ 2
test₂ = refl

But this does
test₂ : S²-to (S²-from 1 +'ₕ S²-from 1) ≡ 2
test₂ = refl

This doesn't
test₃ : S²-to (one +ₕ one) ≡ 2
test₃ = refl

But this does
test₃ : S²-to (one +'ₕ one) ≡ 2
test₃ = refl
-}

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflexive closures
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.Reflexive module directly.
------------------------------------------------------------------------

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

module Data.ReflexiveClosure where

open import Relation.Binary.Construct.Closure.Reflexive public


text:
open import Relation.Binary.Core

module BBHeap.Drop.Properties {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_
open import BBHeap.Compound _≤_
open import BBHeap.Drop _≤_ tot≤ trans≤
open import BBHeap.Equality _≤_
open import BBHeap.Equality.Properties _≤_
open import BBHeap.Push _≤_ tot≤ trans≤
open import BBHeap.Push.Properties _≤_ tot≤ trans≤
open import BBHeap.Subtyping _≤_ trans≤
open import BBHeap.Subtyping.Properties _≤_ trans≤
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.Nat
open import Data.List hiding (drop)
open import Data.Sum
open import Data.Product
open import Nat.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import Order.Total _≤_ tot≤

mutual
  lemma-drop⋘# : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋘r : l ⋘ r) → # (drop⋘ b≤x l⋘r) ≡ # l + # r
  lemma-drop⋘# b≤x lf⋘ = refl
  lemma-drop⋘# b≤x (ll⋘ {x = y₁} {x' = y₂} {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , l⋙dr)
      with # (drop⋘ x≤y₂ l₂⋘r₂) | lemma-drop⋘# x≤y₂ l₂⋘r₂ | # (push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁) | lemma-push# (lexy y₁≤y₂) (left (lexy refl≤) l₁⋘r₁) | # (subtyping (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂)) | lemma-subtyping# (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂) | # l₁ + # r₁ + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl | ._ | refl | ._ | refl = refl
  lemma-drop⋘# b≤x (ll⋘ {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) | inj₁ y₁≤y₂ | inj₂ dl⋘r
      with # (drop⋘ x≤y₁ l₁⋘r₁) | lemma-drop⋘# x≤y₁ l₁⋘r₁
  ... | ._ | refl = refl
  lemma-drop⋘# b≤x (ll⋘ {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) | inj₂ y₂≤y₁ | inj₁ (_ , l⋙dr)
      with # (drop⋘ x≤y₂ l₂⋘r₂) | lemma-drop⋘# x≤y₂ l₂⋘r₂ | (# l₁ + # r₁) + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl = refl
  lemma-drop⋘# b≤x (ll⋘ {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂) | inj₂ y₂≤y₁ | inj₂ dl⋘r
      with # (drop⋘ x≤y₁ l₁⋘r₁) | lemma-drop⋘# x≤y₁ l₁⋘r₁ | # (push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂) | lemma-push# (lexy y₂≤y₁) (left (lexy refl≤) l₂⋘r₂) | # (subtyping (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁)) | lemma-subtyping# (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁)
  ... | ._ | refl | ._ | refl | ._ | refl = refl
  lemma-drop⋘# b≤x (lr⋘ {x = y₁} {x' = y₂} {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cr x≤y₁ l₁⋙r₁) (cl x≤y₂ l₂⋘r₂) (lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ dl⋘r
      with # (drop⋙ x≤y₁ l₁⋙r₁) | lemma-drop⋙# x≤y₁ l₁⋙r₁
  ... | ._ | refl = refl
  lemma-drop⋘# b≤x (lr⋘ {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂) | inj₂ y₂≤y₁ | inj₂ dl⋘r
      with # (drop⋙ x≤y₁ l₁⋙r₁) | lemma-drop⋙# x≤y₁ l₁⋙r₁ | # (push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂) | lemma-push# (lexy y₂≤y₁) (left (lexy refl≤) l₂⋘r₂) | # (subtyping (lexy y₂≤y₁) (drop⋙ x≤y₁ l₁⋙r₁)) | lemma-subtyping# (lexy y₂≤y₁) (drop⋙ x≤y₁ l₁⋙r₁)
  ... | ._ | refl | ._ | refl | ._ | refl = refl

  lemma-drop⋙# : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋙r : l ⋙ r) → # (drop⋙ b≤x l⋙r) ≡ # l + # r
  lemma-drop⋙# b≤x (⋙lf x≤y) = refl
  lemma-drop⋙# b≤x (⋙rl {x = y₁} {x' = y₂} {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (⋙rl x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , dl⋘r)
      with # (drop⋘ x≤y₁ l₁⋘r₁) | lemma-drop⋘# x≤y₁ l₁⋘r₁
  ... | ._ | refl = refl
  lemma-drop⋙# b≤x (⋙rl {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) | inj₁ y₁≤y₂ | inj₂ l⋙dr
      with # (drop⋘ x≤y₂ l₂⋘r₂) | lemma-drop⋘# x≤y₂ l₂⋘r₂ | # (push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁) | lemma-push# (lexy y₁≤y₂) (left (lexy refl≤) l₁⋘r₁) | # (subtyping (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂)) | lemma-subtyping# (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂) | # l₁ + # r₁ + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl | ._ | refl | ._ | refl = refl
  lemma-drop⋙# b≤x (⋙rl x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) | inj₂ y₂≤y₁ | inj₁ (_ , dl⋘r)
        with # (drop⋘ x≤y₁ l₁⋘r₁) | lemma-drop⋘# x≤y₁ l₁⋘r₁ | # (push⋘ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂) | lemma-push# (lexy y₂≤y₁) (left (lexy refl≤) l₂⋘r₂) | # (subtyping (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁)) | lemma-subtyping# (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁)
  ... | ._ | refl | ._ | refl | ._ | refl = refl
  lemma-drop⋙# b≤x (⋙rl {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) | inj₂ y₂≤y₁ | inj₂ l⋙dr
      with # (drop⋘ x≤y₂ l₂⋘r₂) | lemma-drop⋘# x≤y₂ l₂⋘r₂ | (# l₁ + # r₁) + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl = refl
  lemma-drop⋙# b≤x (⋙rr {x = y₁} {x' = y₂} {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cr x≤y₂ l₂⋙r₂) (⋙rr x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ l⋙dr
      with # (drop⋙ x≤y₂ l₂⋙r₂) | lemma-drop⋙# x≤y₂ l₂⋙r₂ | # (push⋘ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁) | lemma-push# (lexy y₁≤y₂) (left (lexy refl≤) l₁⋘r₁) | # (subtyping (lexy y₁≤y₂) (drop⋙ x≤y₂ l₂⋙r₂)) | lemma-subtyping# (lexy y₁≤y₂) (drop⋙ x≤y₂ l₂⋙r₂) | # l₁ + # r₁ + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl | ._ | refl | ._ | refl = refl
  lemma-drop⋙# b≤x (⋙rr {l = l₁} {r = r₁} {l' = l₂} {r' = r₂} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂) | inj₂ y₂≤y₁ | inj₂ l⋙dr
      with # (drop⋙ x≤y₂ l₂⋙r₂) | lemma-drop⋙# x≤y₂ l₂⋙r₂ | (# l₁ + # r₁) + suc (# l₂ + # r₂) | +assoc (# l₁ + # r₁) (# l₂ + # r₂)
  ... | ._ | refl | ._ | refl = refl

lemma-drop# : {b : Bound}{h : BBHeap b}(cₕ : Compound h)  → suc (# (drop cₕ)) ≡ # h
lemma-drop# (cl b≤x l⋘r)
    with # (drop (cl b≤x l⋘r)) | lemma-drop⋘# b≤x l⋘r
... | ._ | refl = refl
lemma-drop# (cr b≤x l⋙r)
    with # (drop (cr b≤x l⋙r)) | lemma-drop⋙# b≤x l⋙r
... | ._ | refl = refl

lemma-drop≤′ : {b : Bound}{h : BBHeap b}(cₕ : Compound h) → suc (# (drop cₕ)) ≤′ # h
lemma-drop≤′ cₕ
    with suc (# (drop cₕ)) | lemma-drop# cₕ
... | ._ | refl = ≤′-refl

mutual
  lemma-drop⋘∼ : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋘r : l ⋘ r) → flatten (drop⋘ b≤x l⋘r) ∼ (flatten l ++ flatten r)
  lemma-drop⋘∼ b≤x lf⋘ = ∼[]
  lemma-drop⋘∼ b≤x (ll⋘ {x = y₁} {x' = y₂} {l = l₁} {r = r₁} x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (ll⋘ x≤y₁ x≤y₂ l₁⋘r₁ l₂⋘r₂ l₂≃r₂ r₁≃l₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , l⋙dr) =
                     let fdr∼fl₂fr₂ = lemma-drop⋘∼ x≤y₂ l₂⋘r₂ ;
                          fdr'∼fdr = lemma-subtyping∼ (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂) ;
                          fdr'∼fl₂fr₂ = trans∼ fdr'∼fdr fdr∼fl₂fr₂ ;
                          fpl'∼y₂fl₁fr₁ = lemma-push⋘∼ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                          fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ = lemma++∼ fpl'∼y₂fl₁fr₁ fdr'∼fl₂fr₂ ;
                          fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ = lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                          y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr = ∼x /head fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ refl∼ ;
                          fpl'fdr'∼fl₁fr₁fr = trans∼ fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr
                     in ∼x /head /head fpl'fdr'∼fl₁fr₁fr
  ... | inj₁ y₁≤y₂ | inj₂ dl⋘r =
                     let fdl∼fl₁fr₁ = lemma-drop⋘∼ x≤y₁ l₁⋘r₁ ;
                          fdlfr∼fl₁fr₁fr = lemma++∼r fdl∼fl₁fr₁
                     in ∼x /head /head fdlfr∼fl₁fr₁fr
  ... | inj₂ y₂≤y₁ | inj₁ (_ , l⋙dr) =
                     let fdr∼fl₂fr₂ = lemma-drop⋘∼ x≤y₂ l₂⋘r₂ ;
                          fl = y₁ ∷ (flatten l₁ ++ flatten r₁) ;
                          flfdr∼flfl₂fr₂ = lemma++∼l {xs = fl} fdr∼fl₂fr₂ ;
                          flfr/y₂⟶flfl₂fr₂ =  lemma++/ {xs = fl}
                     in ∼x {x = y₂} /head flfr/y₂⟶flfl₂fr₂ flfdr∼flfl₂fr₂
  ... | inj₂ y₂≤y₁ | inj₂ dl⋘r =
                     let fdl∼fl₁fr₁ = lemma-drop⋘∼ x≤y₁ l₁⋘r₁ ;
                          fdl'∼fdl = lemma-subtyping∼ (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁) ;
                          fdl'∼fl₁fr₁ = trans∼ fdl'∼fdl fdl∼fl₁fr₁ ;
                          fpr'∼y₁fl₂fr₂ = lemma-push⋘∼ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                          fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ = lemma++∼ fdl'∼fl₁fr₁ fpr'∼y₁fl₂fr₂ ;
                          flfr/y₂⟶flfl₂fr₂ = lemma++/ {xs = y₁ ∷ (flatten l₁ ++ flatten r₁)} ;
                          fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ =  lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                          fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂ = ∼x fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ /head refl∼ ;
                          fdl'fpr'∼flfl₂fr₂ = trans∼ fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂
                     in ∼x /head flfr/y₂⟶flfl₂fr₂ fdl'fpr'∼flfl₂fr₂
  lemma-drop⋘∼ b≤x (lr⋘ {x = y₁} {x' = y₂} {l = l₁} {r = r₁} x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
      with tot≤ y₁ y₂ | lemma-drop⋘ (cr x≤y₁ l₁⋙r₁) (cl x≤y₂ l₂⋘r₂) (lr⋘ x≤y₁ x≤y₂ l₁⋙r₁ l₂⋘r₂ l₂≃r₂ l₁⋗l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ dl⋘r =
                     let fdl∼fl₁fr₁ = lemma-drop⋙∼ x≤y₁ l₁⋙r₁ ;
                          fdlfr∼fl₁fr₁fr = lemma++∼r fdl∼fl₁fr₁
                     in ∼x /head /head fdlfr∼fl₁fr₁fr
  ... | inj₂ y₂≤y₁ | inj₂ dl⋘r =
                     let fdl∼fl₁fr₁ = lemma-drop⋙∼ x≤y₁ l₁⋙r₁ ;
                          fdl'∼fdl = lemma-subtyping∼ (lexy y₂≤y₁) (drop⋙ x≤y₁ l₁⋙r₁) ;
                          fdl'∼fl₁fr₁ = trans∼ fdl'∼fdl fdl∼fl₁fr₁ ;
                          fpr'∼y₁fl₂fr₂ = lemma-push⋘∼ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                          fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ = lemma++∼ fdl'∼fl₁fr₁ fpr'∼y₁fl₂fr₂ ;
                          flfr/y₂⟶flfl₂fr₂ = lemma++/ {xs = y₁ ∷ (flatten l₁ ++ flatten r₁)} ;
                          fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ =  lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                          fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂ = ∼x fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ /head refl∼ ;
                          fdl'fpr'∼flfl₂fr₂ = trans∼ fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂
                     in ∼x /head flfr/y₂⟶flfl₂fr₂ fdl'fpr'∼flfl₂fr₂

  lemma-drop⋙∼ : {b : Bound}{x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋙r : l ⋙ r) → flatten (drop⋙ b≤x l⋙r) ∼ (flatten l ++ flatten r)
  lemma-drop⋙∼ b≤x (⋙lf x≤y) = ∼x /head /head ∼[]
  lemma-drop⋙∼ b≤x (⋙rl {x = y₁} {x' = y₂} {l = l₁} {r = r₁} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cl x≤y₂ l₂⋘r₂) (⋙rl x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₁ y₁≤y₂ | inj₁ (_ , dl⋘r) =
                       let fdl∼fl₁fr₁ = lemma-drop⋘∼ x≤y₁ l₁⋘r₁ ;
                            fdlfr∼fl₁fr₁fr = lemma++∼r fdl∼fl₁fr₁
                       in ∼x /head /head fdlfr∼fl₁fr₁fr
  ... | inj₁ y₁≤y₂ | inj₂ l⋙dr =
                       let fdr∼fl₂fr₂ = lemma-drop⋘∼ (lexy refl≤) l₂⋘r₂ ;
                            fdr'∼fdr = lemma-subtyping∼ (lexy y₁≤y₂) (drop⋘ x≤y₂ l₂⋘r₂) ;
                            fdr'∼fl₂fr₂ = trans∼ fdr'∼fdr fdr∼fl₂fr₂ ;
                            fpl'∼y₂fl₁fr₁ = lemma-push⋘∼ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                            fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ = lemma++∼ fpl'∼y₂fl₁fr₁ fdr'∼fl₂fr₂ ;
                            fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ = lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                            y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr = ∼x /head fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ refl∼ ;
                            fpl'fdr'∼fl₁fr₁fr = trans∼ fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr
                       in ∼x /head /head fpl'fdr'∼fl₁fr₁fr
  ... | inj₂ y₂≤y₁ | inj₁ (_ , dl⋘r) =
                       let fdl∼fl₁fr₁ = lemma-drop⋘∼ x≤y₁ l₁⋘r₁ ;
                            fdl'∼fdl = lemma-subtyping∼ (lexy y₂≤y₁) (drop⋘ x≤y₁ l₁⋘r₁) ;
                            fdl'∼fl₁fr₁ = trans∼ fdl'∼fdl fdl∼fl₁fr₁ ;
                            fpr'∼y₁fl₂fr₂ = lemma-push⋘∼ (lexy y₂≤y₁) (lexy refl≤) l₂⋘r₂ ;
                            fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ = lemma++∼ fdl'∼fl₁fr₁ fpr'∼y₁fl₂fr₂ ;
                            flfr/y₂⟶flfl₂fr₂ = lemma++/ {xs = y₁ ∷ (flatten l₁ ++ flatten r₁)} ;
                            fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ =  lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                            fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂ = ∼x fl₁fr₁y₁fl₂fr₂/y₁⟶fl₁fr₁fl₂fr₂ /head refl∼ ;
                            fdl'fpr'∼flfl₂fr₂ = trans∼ fdl'fpr'∼fl₁fr₁y₁fl₂fr₂ fl₁fr₁y₁fl₂fr₂∼flfl₂fr₂
                       in ∼x /head flfr/y₂⟶flfl₂fr₂ fdl'fpr'∼flfl₂fr₂
  ... | inj₂ y₂≤y₁ | inj₂ l⋙dr =
                       let fdr∼fl₂fr₂ = lemma-drop⋘∼ x≤y₂ l₂⋘r₂ ;
                            fl = y₁ ∷ (flatten l₁ ++ flatten r₁) ;
                            flfdr∼flfl₂fr₂ = lemma++∼l {xs = fl} fdr∼fl₂fr₂ ;
                            flfr/y₂⟶flfl₂fr₂ =  lemma++/ {xs = fl}
                       in ∼x {x = y₂} /head flfr/y₂⟶flfl₂fr₂ flfdr∼flfl₂fr₂
  lemma-drop⋙∼ b≤x (⋙rr {x = y₁} {x' = y₂} {l = l₁} {r = r₁} x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
      with tot≤ y₁ y₂ | lemma-drop⋙ (cl x≤y₁ l₁⋘r₁) (cr x≤y₂ l₂⋙r₂) (⋙rr x≤y₁ x≤y₂ l₁⋘r₁ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | _ | inj₁ (() , _)
  ... | inj₁ y₁≤y₂ | inj₂ l⋙dr =
                       let fdr∼fl₂fr₂ = lemma-drop⋙∼ (lexy refl≤) l₂⋙r₂ ;
                            fdr'∼fdr = lemma-subtyping∼ (lexy y₁≤y₂) (drop⋙ x≤y₂ l₂⋙r₂) ;
                            fdr'∼fl₂fr₂ = trans∼ fdr'∼fdr fdr∼fl₂fr₂ ;
                            fpl'∼y₂fl₁fr₁ = lemma-push⋘∼ (lexy y₁≤y₂) (lexy refl≤) l₁⋘r₁ ;
                            fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ = lemma++∼ fpl'∼y₂fl₁fr₁ fdr'∼fl₂fr₂ ;
                            fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ = lemma++/ {xs = flatten l₁ ++ flatten r₁} ;
                            y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr = ∼x /head fl₁fr₁fr/y₂⟶fl₁fr₁fl₂fr₂ refl∼ ;
                            fpl'fdr'∼fl₁fr₁fr = trans∼ fpl'fdr'∼y₂fl₁fr₁fl₂fr₂ y₂fl₁fr₁fl₂fr₂∼fl₁fr₁fr
                       in ∼x /head /head fpl'fdr'∼fl₁fr₁fr
  ... | inj₂ y₂≤y₁ | inj₂ l⋙dr =
                       let fdr∼fl₂fr₂ = lemma-drop⋙∼ x≤y₂ l₂⋙r₂ ;
                            fl = y₁ ∷ (flatten l₁ ++ flatten r₁) ;
                            flfdr∼flfl₂fr₂ = lemma++∼l {xs = fl} fdr∼fl₂fr₂ ;
                            flfr/y₂⟶flfl₂fr₂ =  lemma++/ {xs = fl}
                       in ∼x {x = y₂} /head flfr/y₂⟶flfl₂fr₂ flfdr∼flfl₂fr₂

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Inductive.Examples.Product where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product hiding (_×_; <_,_>)
open import Data.List
open import Data.Vec

_×_ : Set → Set → Set
A × B = Inductive (((A ∷ (B ∷ [])) , []) ∷ [])

<_,_> : {A B : Set} → A → B → A × B
< a , b > = construct zero (a ∷ (b ∷ [])) []

fst : {A B : Set} → A × B → A
fst = rec ((λ a b → a) ∷ [])

snd : {A B : Set} → A × B → B
snd = rec ((λ a b → b) ∷ [])

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.NatPlusOne where

open import Cubical.Data.NatPlusOne.Base public

open import Cubical.Data.NatPlusOne.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS -v tc.conv.fun:20 #-}

-- Andreas, 2019-11-06, issue #4175, reported and test case by nad.
-- Check quantity for function type subtyping.

postulate
  F : Set → Set
  G : (@0 Set → Set) → Set

-- If an erased function is expected, we cannot pass one
-- that might actually use its arguments.

ShouldFail : Set
ShouldFail = G F

-- Note the eta-expanded version already failed:
-- Fails = G λ x → F x


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

open import HoTT
open import groups.Cokernel
open import cw.WedgeOfCells
open import cohomology.Theory

open import cw.CW

module cw.cohomology.reconstructed.HigherCoboundary {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S (S n))) where

open OrdinaryTheory OT
open import cw.cohomology.grid.LongExactSequence cohomology-theory
  (ℕ-to-ℤ (S n)) (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)
open import cw.cohomology.WedgeOfCells OT

cw-co∂-last : CXₙ/Xₙ₋₁ (⊙cw-init ⊙skel) (ℕ-to-ℤ (S n)) →ᴳ CXₙ/Xₙ₋₁ ⊙skel (ℕ-to-ℤ (S (S n)))
cw-co∂-last = grid-co∂

cw-∂-before-Susp : Xₙ/Xₙ₋₁ (⊙Skeleton.skel ⊙skel) → Susp (Xₙ/Xₙ₋₁ (cw-init (⊙Skeleton.skel ⊙skel)))
cw-∂-before-Susp = grid-∂-before-Susp

⊙cw-∂-before-Susp : ⊙Xₙ/Xₙ₋₁ (⊙Skeleton.skel ⊙skel) ⊙→ ⊙Susp (⊙Xₙ/Xₙ₋₁ (cw-init (⊙Skeleton.skel ⊙skel)))
⊙cw-∂-before-Susp = ⊙grid-∂-before-Susp

cw-∂-before-Susp-glue-β = grid-∂-before-Susp-glue-β
cw-co∂-last-β = grid-co∂-β

module CokerCo∂ where
  grp = Coker cw-co∂-last (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (S (S n))))
  open Group grp public

CokerCo∂ = CokerCo∂.grp

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Structure.Sets where

open import Functional
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Sets.Relator
open import Type

private variable ℓ ℓₑ ℓₗ : Lvl.Level
private variable S E : Type{ℓ}

module _ ⦃ equiv-S : let _ = E ; _ = S ; _ = ℓₗ in Equiv{ℓₑ}(S) ⦄ where
  module _ (_∈_ : E → S → Stmt{ℓₗ}) where
    SetExtensionality = SetEqualityRelation(_∈_)(_∈_) (Equiv._≡_ equiv-S)
    module SetExtensionality = SetEqualityRelation{_∈ₗ_ = _∈_}{_∈ᵣ_ = _∈_}{_≡_ = Equiv._≡_ equiv-S}
    set-extensionality = inst-fn SetExtensionality.membership

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:
-- The SIP applied to groups
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.GroupPath where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

private
  variable
    ℓ ℓ' ℓ'' : Level

open Iso
open GroupStr
open IsGroupHom

𝒮ᴰ-Group : DUARel (𝒮-Univ ℓ) GroupStr ℓ
𝒮ᴰ-Group =
  𝒮ᴰ-Record (𝒮-Univ _) IsGroupEquiv
    (fields:
      data[ _·_ ∣ autoDUARel _ _ ∣ pres· ]
      data[ 1g ∣ autoDUARel _ _ ∣ pres1 ]
      data[ inv ∣ autoDUARel _ _ ∣ presinv ]
      prop[ isGroup ∣ (λ _ _ → isPropIsGroup _ _ _) ])
  where
  open GroupStr
  open IsGroupHom

GroupPath : (M N : Group ℓ) → GroupEquiv M N ≃ (M ≡ N)
GroupPath = ∫ 𝒮ᴰ-Group .UARel.ua

-- TODO: Induced structure results are temporarily inconvenient while we transition between algebra
-- representations
module _ (G : Group ℓ) {A : Type ℓ} (m : A → A → A)
  (e : ⟨ G ⟩ ≃ A)
  (p· : ∀ x y → e .fst (G .snd ._·_ x y) ≡ m (e .fst x) (e .fst y))
  where

  private
    module G = GroupStr (G .snd)

    FamilyΣ : Σ[ B ∈ Type ℓ ] (B → B → B) → Type ℓ
    FamilyΣ (B , n) =
      Σ[ e ∈ B ]
      Σ[ i ∈ (B → B) ]
      IsGroup e n i

    inducedΣ : FamilyΣ (A , m)
    inducedΣ =
      subst FamilyΣ
        (UARel.≅→≡ (autoUARel (Σ[ B ∈ Type ℓ ] (B → B → B))) (e , p·))
        (G.1g , G.inv , G.isGroup)

  InducedGroup : Group ℓ
  InducedGroup .fst = A
  InducedGroup .snd ._·_ = m
  InducedGroup .snd .1g = inducedΣ .fst
  InducedGroup .snd .inv = inducedΣ .snd .fst
  InducedGroup .snd .isGroup = inducedΣ .snd .snd

  InducedGroupEquiv : GroupEquiv G InducedGroup
  fst InducedGroupEquiv = e
  snd InducedGroupEquiv = makeIsGroupHom p·

  InducedGroupPath : G ≡ InducedGroup
  InducedGroupPath = GroupPath _ _ .fst InducedGroupEquiv

uaGroup : {G H : Group ℓ} → GroupEquiv G H → G ≡ H
uaGroup {G = G} {H = H} = equivFun (GroupPath G H)

-- Group-ua functoriality
Group≡ : (G H : Group ℓ) → (
  Σ[ p ∈ ⟨ G ⟩ ≡ ⟨ H ⟩ ]
  Σ[ q ∈ PathP (λ i → p i) (1g (snd G)) (1g (snd H)) ]
  Σ[ r ∈ PathP (λ i → p i → p i → p i) (_·_ (snd G)) (_·_ (snd H)) ]
  Σ[ s ∈ PathP (λ i → p i → p i) (inv (snd G)) (inv (snd H)) ]
  PathP (λ i → IsGroup (q i) (r i) (s i)) (isGroup (snd G)) (isGroup (snd H)))
  ≃ (G ≡ H)
Group≡ G H = isoToEquiv theIso
  where
  theIso : Iso _ _
  fun theIso (p , q , r , s , t) i = p i , groupstr (q i) (r i) (s i) (t i)
  inv theIso x = cong ⟨_⟩ x , cong (1g ∘ snd) x , cong (_·_ ∘ snd) x , cong (inv ∘ snd) x , cong (isGroup ∘ snd) x
  rightInv theIso _ = refl
  leftInv theIso _ = refl

caracGroup≡ : {G H : Group ℓ} (p q : G ≡ H) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
caracGroup≡ {G = G} {H = H} p q P =
  sym (transportTransport⁻ (ua (Group≡ G H)) p)
                                   ∙∙ cong (transport (ua (Group≡ G H))) helper
                                   ∙∙ transportTransport⁻ (ua (Group≡ G H)) q
    where
    helper : transport (sym (ua (Group≡ G H))) p ≡ transport (sym (ua (Group≡ G H))) q
    helper = Σ≡Prop
               (λ _ → isPropΣ
                         (isOfHLevelPathP' 1 (is-set (snd H)) _ _)
                         λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd H)) _ _)
                         λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd H)) _ _)
                         λ _ → isOfHLevelPathP 1 (isPropIsGroup _ _ _) _ _)
               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))

uaGroupId : (G : Group ℓ) → uaGroup (idGroupEquiv {G = G}) ≡ refl
uaGroupId G = caracGroup≡ _ _ uaIdEquiv

uaCompGroupEquiv : {F G H : Group ℓ} (f : GroupEquiv F G) (g : GroupEquiv G H)
                 → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g
uaCompGroupEquiv f g = caracGroup≡ _ _ (
  cong ⟨_⟩ (uaGroup (compGroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  cong ⟨_⟩ (uaGroup f) ∙ cong ⟨_⟩ (uaGroup g)
    ≡⟨ sym (cong-∙ ⟨_⟩ (uaGroup f) (uaGroup g)) ⟩
  cong ⟨_⟩ (uaGroup f ∙ uaGroup g) ∎)

-- J-rule for GroupEquivs
GroupEquivJ : {G : Group ℓ} (P : (H : Group ℓ) → GroupEquiv G H → Type ℓ')
            → P G idGroupEquiv
            → ∀ {H} e → P H e
GroupEquivJ {G = G} P p {H} e =
  transport (λ i → P (GroupPath G H .fst e i)
    (transp (λ j → GroupEquiv G (GroupPath G H .fst e (i ∨ ~ j))) i e))
      (subst (P G) (sym lem) p)
  where
  lem : transport (λ j → GroupEquiv G (GroupPath G H .fst e (~ j))) e
       ≡ idGroupEquiv
  lem = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
       (Σ≡Prop (λ _ → isPropIsEquiv _)
         (funExt λ x → (λ i → fst (fst (fst e .snd .equiv-proof
                          (transportRefl (fst (fst e) (transportRefl x i)) i))))
                         ∙ retEq (fst e) x))

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Char where

open import Agda.Builtin.Char public
open import Common.Bool

charEq : Char -> Char -> Bool
charEq = primCharEquality


text:
module Array where

open import Array.Base public
open import Array.Properties public

max_stars_repo_name: ashinkarov/agda-array

max_issues_repo_name: ashinkarov/agda-array

max_forks_repo_name: ashinkarov/agda-array


text:
module Data.Tuple.Category where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equivalence
import      Functional as Fn
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.Functor.Functors
open import Structure.Categorical.Properties
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₒ ℓₘ ℓₑ ℓₒ₁ ℓₘ₁ ℓₑ₁ ℓₒ₂ ℓₘ₂ ℓₑ₂ : Lvl.Level
private variable Obj Obj₁ Obj₂ Obj₁ₗ Obj₁ᵣ Obj₂ₗ Obj₂ᵣ : Type{ℓ}
private variable Morphism Morphism₁ Morphism₂ Morphism₁ₗ Morphism₂ₗ Morphism₁ᵣ Morphism₂ᵣ : Obj → Obj → Type{ℓ}
private variable ⦃ morphism-equiv morphism-equiv₁ morphism-equiv₂ morphism-equiv₁ₗ morphism-equiv₂ₗ morphism-equiv₁ᵣ morphism-equiv₂ᵣ ⦄ : ∀{x y : Obj} → Equiv{ℓₑ}(Morphism x y)
private variable F F₁ F₂ : Obj₁ → Obj₂
private variable C Cₗ Cᵣ C₁ₗ C₁ᵣ C₂ₗ C₂ᵣ C₁ C₂ C₃ : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ}

module _
  (cat₁ : Category{Obj = Obj₁} (Morphism₁) ⦃ \{x y} → morphism-equiv₁{x}{y} ⦄)
  (cat₂ : Category{Obj = Obj₂} (Morphism₂) ⦃ \{x y} → morphism-equiv₂{x}{y} ⦄)
  where

  open Category ⦃ … ⦄

  private instance _ = cat₁
  private instance _ = cat₂

  productCategory : Category{Obj = Obj₁ ⨯ Obj₂} (\{(x₁ , x₂) (y₁ , y₂) → (Morphism₁ x₁ y₁) ⨯ (Morphism₂ x₂ y₂)})
  Category._∘_ productCategory (f₁ , f₂) (g₁ , g₂) = ((f₁ ∘ g₁) , (f₂ ∘ g₂))
  Category.id  productCategory                     = (id , id)
  _⨯_.left  (BinaryOperator.congruence (Category.binaryOperator productCategory) (p₁l , p₁r) (p₂l , p₂r)) = congruence₂(_∘_) p₁l p₂l
  _⨯_.right (BinaryOperator.congruence (Category.binaryOperator productCategory) (p₁l , p₁r) (p₂l , p₂r)) = congruence₂(_∘_) p₁r p₂r
  _⨯_.left  (Morphism.Associativity.proof (Category.associativity productCategory)) = Morphism.associativity(_∘_)
  _⨯_.right (Morphism.Associativity.proof (Category.associativity productCategory)) = Morphism.associativity(_∘_)
  _⨯_.left  (Morphism.Identityₗ.proof (_⨯_.left  (Category.identity productCategory))) = Morphism.identityₗ(_∘_)(id)
  _⨯_.right (Morphism.Identityₗ.proof (_⨯_.left  (Category.identity productCategory))) = Morphism.identityₗ(_∘_)(id)
  _⨯_.left  (Morphism.Identityᵣ.proof (_⨯_.right (Category.identity productCategory))) = Morphism.identityᵣ(_∘_)(id)
  _⨯_.right (Morphism.Identityᵣ.proof (_⨯_.right (Category.identity productCategory))) = Morphism.identityᵣ(_∘_)(id)

_⨯ᶜᵃᵗ_ : CategoryObject{ℓₒ₁}{ℓₘ₁}{ℓₑ₁} → CategoryObject{ℓₒ₂}{ℓₘ₂}{ℓₑ₂} → CategoryObject
(intro C₁) ⨯ᶜᵃᵗ (intro C₂) = intro (productCategory C₁ C₂)

module Tupleᶜᵃᵗ where
  open CategoryObject ⦃ … ⦄
  open Functor ⦃ … ⦄ renaming (map to fmap)
  private open module CategoryObjectEquiv {ℓₒ ℓₘ ℓₑ} ⦃ C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ} ⦄ {x}{y} = Equivalence (Equiv-equivalence ⦃ CategoryObject.morphism-equiv(C){x}{y} ⦄) using ()
  private open module CategoryObjectCategory {ℓₒ ℓₘ ℓₑ} ⦃ C : CategoryObject{ℓₒ}{ℓₘ}{ℓₑ} ⦄ = Category(category ⦃ C ⦄)

  open Structure.Category.Functor.Functors.Wrapped

  map : (C₁ₗ →ᶠᵘⁿᶜᵗᵒʳ C₁ᵣ) → (C₂ₗ →ᶠᵘⁿᶜᵗᵒʳ C₂ᵣ) → ((C₁ₗ ⨯ᶜᵃᵗ C₂ₗ) →ᶠᵘⁿᶜᵗᵒʳ (C₁ᵣ ⨯ᶜᵃᵗ C₂ᵣ))
  map {C₁ₗ = C₁ₗ} {C₁ᵣ = C₁ᵣ} {C₂ₗ = C₂ₗ} {C₂ᵣ = C₂ᵣ} ([∃]-intro F₁ ⦃ functor₁ ⦄) ([∃]-intro F₂ ⦃ functor₂ ⦄) = [∃]-intro _ ⦃ productMapFunctor ⦄ where
    instance _ = C₁ₗ ; instance _ = C₁ᵣ ; instance _ = C₂ₗ ; instance _ = C₂ᵣ
    instance _ = C₁ₗ ⨯ᶜᵃᵗ C₂ₗ ; instance _ = C₁ᵣ ⨯ᶜᵃᵗ C₂ᵣ
    productMapFunctor : Functor(productCategory (category ⦃ C₁ₗ ⦄) (category ⦃ C₂ₗ ⦄))(productCategory (category ⦃ C₁ᵣ ⦄) (category ⦃ C₂ᵣ ⦄)) (Tuple.map F₁ F₂)
    Functor.map productMapFunctor = Tuple.map fmap fmap
    Tuple.left  (Functor.op-preserving productMapFunctor) = op-preserving
    Tuple.right (Functor.op-preserving productMapFunctor) = op-preserving
    Tuple.left  (Functor.id-preserving productMapFunctor) = id-preserving
    Tuple.right (Functor.id-preserving productMapFunctor) = id-preserving

  mapLeft : (C₁ₗ →ᶠᵘⁿᶜᵗᵒʳ C₁ᵣ) → ((C₁ₗ ⨯ᶜᵃᵗ C₂) →ᶠᵘⁿᶜᵗᵒʳ (C₁ᵣ ⨯ᶜᵃᵗ C₂))
  mapLeft F = map F idᶠᵘⁿᶜᵗᵒʳ

  mapRight : (C₂ₗ →ᶠᵘⁿᶜᵗᵒʳ C₂ᵣ) → ((C₁ ⨯ᶜᵃᵗ C₂ₗ) →ᶠᵘⁿᶜᵗᵒʳ (C₁ ⨯ᶜᵃᵗ C₂ᵣ))
  mapRight F = map idᶠᵘⁿᶜᵗᵒʳ F

  left : ((Cₗ ⨯ᶜᵃᵗ Cᵣ) →ᶠᵘⁿᶜᵗᵒʳ Cₗ)
  ∃.witness left = Tuple.left
  Functor.map (∃.proof left) = Tuple.left
  Functor.op-preserving (∃.proof (left {Cₗ = Cₗ} {Cᵣ = Cᵣ})) {f = (fₗ , fᵣ)} {g = (gₗ , gᵣ)} =
    Tuple.left ((fₗ , fᵣ) ∘ (gₗ , gᵣ))        🝖[ _≡_ ]-[]
    Tuple.left ((fₗ ∘ gₗ) , (fᵣ ∘ gᵣ))        🝖[ _≡_ ]-[]
    fₗ ∘ gₗ                                   🝖[ _≡_ ]-[]
    Tuple.left(fₗ , fᵣ) ∘ Tuple.left(gₗ , gᵣ) 🝖-end
    where instance _ = Cₗ ; instance _ = Cᵣ ; instance _ = Cₗ ⨯ᶜᵃᵗ Cᵣ
  Functor.id-preserving (∃.proof (left {Cₗ = Cₗ} {Cᵣ = Cᵣ})) {x , y} =
    Tuple.left (id ⦃ Cₗ ⨯ᶜᵃᵗ Cᵣ ⦄ {x , y})      🝖[ _≡_ ]-[]
    Tuple.left (id ⦃ Cₗ ⦄ {x} , id ⦃ Cᵣ ⦄ {y})  🝖[ _≡_ ]-[]
    id ⦃ Cₗ ⦄ {x}                               🝖-end
    where instance _ = Cₗ ; instance _ = Cᵣ ; instance _ = Cₗ ⨯ᶜᵃᵗ Cᵣ

  right : ((Cₗ ⨯ᶜᵃᵗ Cᵣ) →ᶠᵘⁿᶜᵗᵒʳ Cᵣ)
  ∃.witness right = Tuple.right
  Functor.map (∃.proof right) = Tuple.right
  Functor.op-preserving (∃.proof (right {Cₗ = Cₗ} {Cᵣ = Cᵣ})) {f = (fₗ , fᵣ)} {g = (gₗ , gᵣ)} =
    Tuple.right ((fₗ , fᵣ) ∘ (gₗ , gᵣ))        🝖[ _≡_ ]-[]
    Tuple.right ((fₗ ∘ gₗ) , (fᵣ ∘ gᵣ))        🝖[ _≡_ ]-[]
    fᵣ ∘ gᵣ                                    🝖[ _≡_ ]-[]
    Tuple.right(fₗ , fᵣ) ∘ Tuple.right(gₗ , gᵣ) 🝖-end
    where instance _ = Cₗ ; instance _ = Cᵣ ; instance _ = Cₗ ⨯ᶜᵃᵗ Cᵣ
  Functor.id-preserving (∃.proof (right {Cₗ = Cₗ} {Cᵣ = Cᵣ})) {x , y} =
    Tuple.right (id ⦃ Cₗ ⨯ᶜᵃᵗ Cᵣ ⦄ {x , y})      🝖[ _≡_ ]-[]
    Tuple.right (id ⦃ Cₗ ⦄ {x} , id ⦃ Cᵣ ⦄ {y})  🝖[ _≡_ ]-[]
    id ⦃ Cᵣ ⦄ {y}                                🝖-end
    where instance _ = Cₗ ; instance _ = Cᵣ ; instance _ = Cₗ ⨯ᶜᵃᵗ Cᵣ

  repeat : (C →ᶠᵘⁿᶜᵗᵒʳ (C ⨯ᶜᵃᵗ C))
  ∃.witness repeat = Tuple.repeat
  Functor.map (∃.proof repeat) = Tuple.repeat
  Functor.op-preserving (∃.proof (repeat {C = C})) {f = f} {g = g} =
    Tuple.repeat(f ∘ g)               🝖[ _≡_ ]-[]
    Tuple.repeat(f) ∘ Tuple.repeat(g) 🝖-end
    where instance _ = C ; instance _ = C ⨯ᶜᵃᵗ C
  (Functor.id-preserving (∃.proof (repeat {C = C})) {x}) =
    Tuple.repeat(id{x = x})  🝖[ _≡_ ]-[]
    id{x = (x , x)}          🝖-end
    where instance _ = C ; instance _ = C ⨯ᶜᵃᵗ C

  constₗ : CategoryObject.Object(Cₗ) → (Cᵣ →ᶠᵘⁿᶜᵗᵒʳ (Cₗ ⨯ᶜᵃᵗ Cᵣ))
  constₗ c = mapLeft (constᶠᵘⁿᶜᵗᵒʳ c) ∘ᶠᵘⁿᶜᵗᵒʳ repeat

  constᵣ : CategoryObject.Object(Cᵣ) → (Cₗ →ᶠᵘⁿᶜᵗᵒʳ (Cₗ ⨯ᶜᵃᵗ Cᵣ))
  constᵣ c = mapRight (constᶠᵘⁿᶜᵗᵒʳ c) ∘ᶠᵘⁿᶜᵗᵒʳ repeat

  associateLeft : (C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃)) →ᶠᵘⁿᶜᵗᵒʳ ((C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃)
  ∃.witness associateLeft = Tuple.associateLeft
  Functor.map (∃.proof associateLeft) = Tuple.associateLeft
  Functor.op-preserving (∃.proof (associateLeft {C₁ = C₁}{C₂ = C₂}{C₃ = C₃})) {f = f}{g = g} =
    Tuple.associateLeft(f ∘ g)                    🝖[ _≡_ ]-[]
    Tuple.associateLeft f ∘ Tuple.associateLeft g 🝖-end
    where
      instance _ = C₁ ; instance _ = C₂ ; instance _ = C₃
      instance _ = C₁ ⨯ᶜᵃᵗ C₂ ; instance _ = C₂ ⨯ᶜᵃᵗ C₃
      instance _ = C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃) ; instance _ = (C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃
  Functor.id-preserving (∃.proof (associateLeft {C₁ = C₁}{C₂ = C₂}{C₃ = C₃})) =
    Tuple.associateLeft(id) 🝖[ _≡_ ]-[]
    id                      🝖-end
    where
      instance _ = C₁ ; instance _ = C₂ ; instance _ = C₃
      instance _ = C₁ ⨯ᶜᵃᵗ C₂ ; instance _ = C₂ ⨯ᶜᵃᵗ C₃
      instance _ = C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃) ; instance _ = (C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃

  associateRight : ((C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃) →ᶠᵘⁿᶜᵗᵒʳ (C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃))
  ∃.witness associateRight = Tuple.associateRight
  Functor.map (∃.proof associateRight) = Tuple.associateRight
  Functor.op-preserving (∃.proof (associateRight {C₁ = C₁}{C₂ = C₂}{C₃ = C₃})) {f = f}{g = g} =
    Tuple.associateRight(f ∘ g)                    🝖[ _≡_ ]-[]
    Tuple.associateRight f ∘ Tuple.associateRight g 🝖-end
    where
      instance _ = C₁ ; instance _ = C₂ ; instance _ = C₃
      instance _ = C₁ ⨯ᶜᵃᵗ C₂ ; instance _ = C₂ ⨯ᶜᵃᵗ C₃
      instance _ = C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃) ; instance _ = (C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃
  Functor.id-preserving (∃.proof (associateRight {C₁ = C₁}{C₂ = C₂}{C₃ = C₃})) =
    Tuple.associateRight(id) 🝖[ _≡_ ]-[]
    id                       🝖-end
    where
      instance _ = C₁ ; instance _ = C₂ ; instance _ = C₃
      instance _ = C₁ ⨯ᶜᵃᵗ C₂ ; instance _ = C₂ ⨯ᶜᵃᵗ C₃
      instance _ = C₁ ⨯ᶜᵃᵗ (C₂ ⨯ᶜᵃᵗ C₃) ; instance _ = (C₁ ⨯ᶜᵃᵗ C₂) ⨯ᶜᵃᵗ C₃


text:
module Haskell.Prim.Integer where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Char
open import Agda.Builtin.Unit

import Agda.Builtin.Int
open Agda.Builtin.Int public using () renaming (Int to Integer)
open Agda.Builtin.Int renaming (Int to Integer)

open import Haskell.Prim
open import Haskell.Prim.Bool

--------------------------------------------------
-- Literals

private
  negNat : Nat → Integer
  negNat 0       = pos 0
  negNat (suc n) = negsuc n

instance
  iNumberInteger : Number Integer
  iNumberInteger .Number.Constraint _ = ⊤
  iNumberInteger .fromNat n = pos n

  iNegativeInteger : Negative Integer
  iNegativeInteger .Negative.Constraint _ = ⊤
  iNegativeInteger .fromNeg n = negNat n

--------------------------------------------------
-- Arithmetic

private
  subNat : Nat → Nat → Integer
  subNat n m = if n < m then negsuc (m - suc n) else pos (n - m)

negateInteger : Integer → Integer
negateInteger (pos 0)       = pos 0
negateInteger (pos (suc n)) = negsuc n
negateInteger (negsuc n)    = pos (suc n)

addInteger : Integer → Integer → Integer
addInteger (pos    n) (pos    m) = pos (n + m)
addInteger (pos    n) (negsuc m) = subNat n (suc m)
addInteger (negsuc n) (pos    m) = subNat m (suc n)
addInteger (negsuc n) (negsuc m) = negsuc (n + m + 1)

subInteger : Integer → Integer → Integer
subInteger n m = addInteger n (negateInteger m)

mulInteger : Integer → Integer → Integer
mulInteger (pos    n) (pos    m) = pos (n * m)
mulInteger (pos    n) (negsuc m) = negNat (n * suc m)
mulInteger (negsuc n) (pos    m) = negNat (suc n * m)
mulInteger (negsuc n) (negsuc m) = pos (suc n * suc m)

absInteger : Integer → Integer
absInteger (pos    n) = pos n
absInteger (negsuc n) = pos (suc n)

signInteger : Integer → Integer
signInteger (pos 0)       = 0
signInteger (pos (suc _)) = 1
signInteger (negsuc _)    = -1

--------------------------------------------------
-- Comparisons

eqInteger : Integer → Integer → Bool
eqInteger (pos n)    (pos m)    = n == m
eqInteger (negsuc n) (negsuc m) = n == m
eqInteger _          _          = false

ltInteger : Integer → Integer → Bool
ltInteger (pos    n) (pos    m) = n < m
ltInteger (pos    n) (negsuc _) = false
ltInteger (negsuc n) (pos    _) = true
ltInteger (negsuc n) (negsuc m) = m < n

--------------------------------------------------
-- Show

showInteger : Integer → List Char
showInteger n = primStringToList (primShowInteger n)

--------------------------------------------------
-- Constraints

isNegativeInteger : Integer → Bool
isNegativeInteger (pos _)    = false
isNegativeInteger (negsuc _) = true

IsNonNegativeInteger : Integer → Set
IsNonNegativeInteger (pos _)      = ⊤
IsNonNegativeInteger n@(negsuc _) =
  TypeError (primStringAppend (primShowInteger n) (" is negative"))