text:
module Data.List.Equiv.Id where

import Lvl
open import Functional
open import Function.Names as Names using (_⊜_)
import      Function.Equals as Fn
open import Data.Boolean
open import Data.Option
open import Data.Option.Equiv.Id
open import Data.Option.Proofs using ()
open import Data.List
open import Data.List.Equiv
open import Data.List.Functions
open import Logic
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Relator.Equals
open import Structure.Function
open import Structure.Function.Domain
import      Structure.Function.Names as Names
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid using (Equiv) renaming (_≡_ to _≡ₛ_)
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ ℓₑₗ ℓₑₒ ℓₑ₁ ℓₑ₂ ℓₑₗ₁ ℓₑₗ₂ : Lvl.Level
private variable T A B : Type{ℓ}
private variable n : ℕ

open import Relator.Equals
open import Relator.Equals.Proofs

private variable l l₁ l₂ : List(T)
private variable a b x : T
private variable f : A → B
private variable P : List(T) → Stmt{ℓ}

[⊰]-general-cancellation : ((a ⊰ l₁) ≡ (b ⊰ l₂)) → (a ≡ b) ∧ (l₁ ≡ l₂)
[⊰]-general-cancellation p = [∧]-intro (L p) (R p) where
  R : ((a ⊰ l₁) ≡ (b ⊰ l₂)) → (l₁ ≡ l₂)
  R p = congruence₁(tail) p

  L : ((a ⊰ l₁) ≡ (b ⊰ l₂)) → (a ≡ b)
  L {l₁ = ∅}     {l₂ = ∅}      [≡]-intro = [≡]-intro
  L {l₁ = ∅}     {l₂ = _ ⊰ _} p with () ← R p
  L {l₁ = _ ⊰ _} {l₂ = _ ⊰ _} p = injective(Some) (congruence₁(first) p)

instance
  List-Id-extensionality : Extensionality([≡]-equiv {T = List(T)})
  Extensionality.generalized-cancellationᵣ List-Id-extensionality = [∧]-elimₗ ∘ [⊰]-general-cancellation
  Extensionality.generalized-cancellationₗ List-Id-extensionality = [∧]-elimᵣ ∘ [⊰]-general-cancellation
  Extensionality.case-unequality           List-Id-extensionality ()

open import Data.List.Proofs

initial-0-length : (initial(0)(l) ≡ ∅)
initial-0-length {l = ∅}     = reflexivity(_≡_)
initial-0-length {l = x ⊰ l} = reflexivity(_≡_)
{-# REWRITE initial-0-length #-}

multiply-singleton-repeat : (singleton(l) ++^ n ≡ repeat(l)(n))
multiply-singleton-repeat {l = l} {n = 𝟎}   = reflexivity(_≡_)
multiply-singleton-repeat {l = l} {n = 𝐒 n} = congruence₁(l ⊰_) (multiply-singleton-repeat {l = l} {n = n})

module _ {f g : A → B} where
  map-function-raw : (f ⊜ g) → (map f ⊜ map g)
  map-function-raw p {∅} = reflexivity(_≡_)
  map-function-raw p {x ⊰ l} rewrite p{x} = congruence₁(g(x) ⊰_) (map-function-raw p {l})

module _ {f g : A → List(B)} where
  concatMap-function-raw : (f ⊜ g) → (concatMap f ⊜ concatMap g)
  concatMap-function-raw p {∅}                  = reflexivity(_≡_)
  concatMap-function-raw p {x ⊰ l} rewrite p{x} = congruence₁(g(x) ++_) (concatMap-function-raw p {l})

module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : Type{ℓ₃}} {f : B → C}{g : A → B} where
  map-preserves-[∘] : (map(f ∘ g) ⊜ (map f ∘ map g))
  map-preserves-[∘] {x = ∅}     = reflexivity(_≡_)
  map-preserves-[∘] {x = x ⊰ l} = congruence₁(f(g(x)) ⊰_) (map-preserves-[∘] {x = l})

map-preserves-id : (map id ⊜ id{T = List(T)})
map-preserves-id {x = ∅} = reflexivity(_≡_)
map-preserves-id {x = x ⊰ l} = congruence₁(x ⊰_) (map-preserves-id {x = l})
{-# REWRITE map-preserves-id #-}

concatMap-[++] : (concatMap f (l₁ ++ l₂) ≡ (concatMap f l₁ ++ concatMap f l₂))
concatMap-[++] {f = f} {∅}      {l₂} = reflexivity(_≡_)
concatMap-[++] {f = f} {x ⊰ l₁} {l₂} =
  (f(x) ++ concatMap f (l₁ ++ l₂))             🝖-[ congruence₁(f(x) ++_) (concatMap-[++] {f = f} {l₁} {l₂}) ]
  (f(x) ++ (concatMap f l₁ ++ concatMap f l₂)) 🝖-[ associativity(_++_) {x = f(x)}{y = concatMap f l₁}{z = concatMap f l₂} ]-sym
  (f(x) ++ concatMap f l₁ ++ concatMap f l₂)   🝖-end

module _ {ℓ₁ ℓ₂ ℓ₃} {A : Type{ℓ₁}} {B : Type{ℓ₂}} {C : Type{ℓ₃}} {f : B → List(C)}{g : A → List(B)} where
  concatMap-[∘] : (concatMap(concatMap f ∘ g)) ⊜ (concatMap f ∘ concatMap g)
  concatMap-[∘] {∅}     = reflexivity(_≡_)
  concatMap-[∘] {x ⊰ l} =
    (concatMap(concatMap f ∘ g)) (x ⊰ l)                  🝖[ _≡_ ]-[]
    (concatMap f ∘ g) x ++ concatMap(concatMap f ∘ g) l   🝖-[ congruence₁((concatMap f ∘ g) x ++_) (concatMap-[∘] {l}) ]
    (concatMap f ∘ g) x ++ (concatMap f ∘ concatMap g) l  🝖[ _≡_ ]-[]
    (concatMap f (g(x))) ++ (concatMap f (concatMap g l)) 🝖-[ concatMap-[++] {f = f}{l₁ = g(x)}{l₂ = concatMap g l} ]-sym
    concatMap f (g(x) ++ concatMap g l)                   🝖[ _≡_ ]-[]
    concatMap f (concatMap g (x ⊰ l))                     🝖[ _≡_ ]-[]
    (concatMap f ∘ concatMap g) (x ⊰ l)                   🝖-end

concatMap-singleton : (concatMap{A = T} singleton) ⊜ id
concatMap-singleton {x = ∅} = reflexivity(_≡_)
concatMap-singleton {x = x ⊰ l} = congruence₁(x ⊰_) (concatMap-singleton {x = l})

concatMap-concat-map : (concatMap f l ≡ concat(map f l))
concatMap-concat-map        {l = ∅} = reflexivity(_≡_)
concatMap-concat-map {f = f}{l = x ⊰ l} =
  concatMap f (x ⊰ l)     🝖[ _≡_ ]-[]
  f(x) ++ concatMap f l   🝖[ _≡_ ]-[ congruence₂ᵣ(_++_)(f(x)) (concatMap-concat-map {l = l}) ]
  f(x) ++ concat(map f l) 🝖[ _≡_ ]-[]
  concat(f(x) ⊰ map f l)  🝖[ _≡_ ]-[]
  concat(map f (x ⊰ l))   🝖-end

foldₗ-lastElem-equivalence : (last{T = T} ⊜ foldₗ (const Option.Some) Option.None)
foldₗ-lastElem-equivalence {x = ∅}         = reflexivity(_≡_)
foldₗ-lastElem-equivalence {x = x ⊰ ∅}     = reflexivity(_≡_)
foldₗ-lastElem-equivalence {x = x ⊰ y ⊰ l} = foldₗ-lastElem-equivalence {x = y ⊰ l}

{-
foldₗ-reverse-equivalence : (reverse{T = T} ⊜ foldₗ (Functional.swap(_⊰_)) ∅)
foldₗ-reverse-equivalence {x = ∅} = reflexivity(_≡_)
foldₗ-reverse-equivalence {x = x ⊰ l} =
  reverse (x ⊰ l)                                           🝖[ _≡_ ]-[]
  (postpend x ∘ reverse) l                                  🝖[ _≡_ ]-[ congruence₁(postpend x) (foldₗ-reverse-equivalence {x = l}) ]
  (postpend x ∘ foldₗ (Functional.swap(_⊰_)) ∅) l           🝖[ _≡_ ]-[ {!!} ]
  foldₗ (Functional.swap(_⊰_)) (Functional.swap(_⊰_) ∅ x) l 🝖[ _≡_ ]-[]
  foldₗ (Functional.swap(_⊰_)) (singleton(x)) l             🝖[ _≡_ ]-[]
  foldₗ (Functional.swap(_⊰_)) ∅ (x ⊰ l)                    🝖-end
-}

foldᵣ-function : ⦃ equiv : Equiv{ℓₑ}(B) ⦄ → ∀{_▫_ : A → B → B} ⦃ oper : BinaryOperator(_▫_) ⦄ → Function ⦃ equiv-B = equiv ⦄ (foldᵣ(_▫_) a)
foldᵣ-function {a = a} ⦃ equiv ⦄ {_▫_ = _▫_} ⦃ oper ⦄ = intro p where
  p : Names.Congruence₁ ⦃ equiv-B = equiv ⦄ (foldᵣ(_▫_) a)
  p {∅}       {∅}       xy = reflexivity(Equiv._≡_ equiv)
  p {x₁ ⊰ l₁} {x₂ ⊰ l₂} xy =
    foldᵣ(_▫_) a (x₁ ⊰ l₁) 🝖[ Equiv._≡_ equiv ]-[]
    x₁ ▫ (foldᵣ(_▫_) a l₁) 🝖[ Equiv._≡_ equiv ]-[ congruence₂(_▫_) ⦃ oper ⦄ ([∧]-elimₗ([⊰]-general-cancellation xy)) (p {l₁} {l₂} ([∧]-elimᵣ([⊰]-general-cancellation xy))) ]
    x₂ ▫ (foldᵣ(_▫_) a l₂) 🝖[ Equiv._≡_ equiv ]-[]
    foldᵣ(_▫_) a (x₂ ⊰ l₂) 🝖-end

foldᵣ-function₊-raw : ∀{l₁ l₂ : List(A)} ⦃ equiv : Equiv{ℓₑ}(B) ⦄ {_▫₁_ _▫₂_ : A → B → B} ⦃ oper₁ : BinaryOperator(_▫₁_) ⦄ ⦃ oper₂ : BinaryOperator ⦃ [≡]-equiv ⦄ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₂_) ⦄ {a₁ a₂ : B} → (∀{x y} → (_≡ₛ_ ⦃ equiv ⦄ (x ▫₁ y) (x ▫₂ y))) → (_≡ₛ_ ⦃ equiv ⦄ a₁ a₂) → (l₁ ≡ l₂) → (foldᵣ(_▫₁_) a₁ l₁ ≡ₛ foldᵣ(_▫₂_) a₂ l₂)
foldᵣ-function₊-raw {l₁ = ∅} {∅} ⦃ equiv ⦄ {_▫₁_} {_▫₂_} ⦃ oper₁ ⦄ ⦃ oper₂ ⦄ {a₁} {a₂} opeq aeq leq = aeq
foldᵣ-function₊-raw {l₁ = x₁ ⊰ l₁} {x₂ ⊰ l₂} ⦃ equiv ⦄ {_▫₁_} {_▫₂_} ⦃ oper₁ ⦄ ⦃ oper₂ ⦄ {a₁} {a₂} opeq aeq leq =
  foldᵣ(_▫₁_) a₁ (x₁ ⊰ l₁)  🝖[ Equiv._≡_ equiv ]-[]
  x₁ ▫₁ (foldᵣ(_▫₁_) a₁ l₁) 🝖[ Equiv._≡_ equiv ]-[ congruence₂(_▫₁_) ⦃ oper₁ ⦄ ([∧]-elimₗ([⊰]-general-cancellation leq)) (foldᵣ-function₊-raw {l₁ = l₁} {l₂} ⦃ equiv ⦄ {_▫₁_}{_▫₂_} ⦃ oper₁ ⦄ ⦃ oper₂ ⦄ {a₁}{a₂} opeq aeq ([∧]-elimᵣ([⊰]-general-cancellation leq))) ]
  x₂ ▫₁ (foldᵣ(_▫₂_) a₂ l₂) 🝖[ Equiv._≡_ equiv ]-[ opeq{x₂}{foldᵣ(_▫₂_) a₂ l₂} ]
  x₂ ▫₂ (foldᵣ(_▫₂_) a₂ l₂) 🝖[ Equiv._≡_ equiv ]-[]
  foldᵣ(_▫₂_) a₂ (x₂ ⊰ l₂)  🝖[ Equiv._≡_ equiv ]-end

map-binaryOperator : BinaryOperator {A₁ = A → B} ⦃ equiv-A₁ = Fn.[⊜]-equiv ⦃ [≡]-equiv ⦄ ⦄ ⦃ equiv-A₂ = [≡]-equiv ⦄ (map)
map-binaryOperator = intro p where
  p : Names.Congruence₂(map)
  p {f} {g} {∅}       {∅}       fg xy = reflexivity(_≡_)
  p {f} {g} {x₁ ⊰ l₁} {x₂ ⊰ l₂} fg xy = congruence₂(_⊰_) ba rec where
    ba : f(x₁) ≡ g(x₂)
    ba =
      f(x₁) 🝖[ _≡_ ]-[ Fn._⊜_.proof fg {x₁} ]
      g(x₁) 🝖[ _≡_ ]-[ congruence₁(g) ([∧]-elimₗ([⊰]-general-cancellation xy)) ]
      g(x₂) 🝖-end
    rec : map f(l₁) ≡ map g(l₂)
    rec =
      map f(l₁) 🝖[ _≡_ ]-[ p fg ([∧]-elimᵣ([⊰]-general-cancellation xy)) ]
      map g(l₂) 🝖-end

count-of-[++] : ∀{P} → (count P (l₁ ++ l₂) ≡ count P l₁ + count P l₂)
count-of-[++] {l₁ = ∅}       {l₂ = l₂} {P = P} = reflexivity(_≡_)
count-of-[++] {l₁ = x₁ ⊰ l₁} {l₂ = l₂} {P = P} with P(x₁) | count-of-[++] {l₁ = l₁} {l₂ = l₂} {P = P}
... | 𝑇 | p = congruence₁ 𝐒(p)
... | 𝐹 | p = p

-- TODO Is this true?: count-single-equality-equivalence : (∀{P} → count P l₁ ≡ count P l₂) ↔ (∀{x} → (count (x ≡?_) l₁ ≡ count (x ≡?_) l₂))

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:
{-# OPTIONS --rewriting #-}

-- {-# OPTIONS -v rewriting:30 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality renaming (_≡_ to _≡≡_)

record Eq (t : Set) : Set₁ where
  field
    _≡_ : t → t → Set

open Eq {{...}}

{-# BUILTIN REWRITE _≡_ #-}

instance
  eqN : Eq Nat
  eqN = record { _≡_ = _≡≡_ }

postulate
  plus0p :  ∀{x} → (x + zero) ≡ x

{-# REWRITE plus0p #-}

-- Error:
-- plus0p  does not target rewrite relation
-- when checking the pragma REWRITE plus0p

-- The type of the postulate ends in _≡≡_ (after reduction)
-- but the rewrite relation is _≡_

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module MLib.Algebra.PropertyCode.RawStruct where

open import MLib.Prelude
open import MLib.Fin.Parts
open import MLib.Finite

open import Relation.Binary as B using (Setoid)

open import Data.List.Any using (Any; here; there)
open import Data.List.Membership.Propositional using (_∈_)

open import Data.Vec.N-ary

open import Data.Product.Relation.SigmaPropositional as OverΣ using (OverΣ)

open import Data.Bool using (T)

open import Category.Applicative

module _ {c ℓ} {A : Set c} (_≈_ : Rel A ℓ) where
  open Algebra.FunctionProperties _≈_

  Congruentₙ : ∀ {n} → (Vec A n → A) → Set (c ⊔ˡ ℓ)
  Congruentₙ f = ∀ {xs ys} → Vec.Pointwise _≈_ xs ys → f xs ≈ f ys

  fromRefl : Reflexive _≈_ → (f : Vec A 0 → A) → Congruentₙ f
  fromRefl refl f [] = refl

  fromCongruent₂ : (f : Vec A 2 → A) → Congruent₂ (curryⁿ f) → Congruentₙ f
  fromCongruent₂ f cong₂ (x≈u ∷ y≈v ∷ []) = cong₂ x≈u y≈v

PointwiseFunc : ∀ {n} {a b ℓ r} {A : Set a} {B : Set b} (_∼_ : A → B → Set ℓ) (xs : Vec A n) (ys : Vec B n) (R : Set r) → Set (N-ary-level ℓ r n)
PointwiseFunc _∼_ [] [] R = R
PointwiseFunc _∼_ (x ∷ xs) (y ∷ ys) R = x ∼ y → PointwiseFunc _∼_ xs ys R

appPW : ∀ {n} {a b ℓ r} {A : Set a} {B : Set b} {_∼_ : A → B → Set ℓ} {xs : Vec A n} {ys : Vec B n} {R : Set r} → PointwiseFunc _∼_ xs ys R → Vec.Pointwise _∼_ xs ys → R
appPW f [] = f
appPW f (x∼y ∷ pw) = appPW (f x∼y) pw

curryPW : ∀ {n} {a b ℓ r} {A : Set a} {B : Set b} {_∼_ : A → B → Set ℓ} {xs : Vec A n} {ys : Vec B n} {R : Set r} → (Vec.Pointwise _∼_ xs ys → R) → PointwiseFunc _∼_ xs ys R
curryPW {xs = []} {[]} f = f []
curryPW {xs = x ∷ xs} {y ∷ ys} f x∼y = curryPW {xs = xs} {ys} λ pw → f (x∼y ∷ pw)

--------------------------------------------------------------------------------
--  Raw structures implementing a set of operators, i.e. interpretations of the
--  operators which are each congruent under an equivalence, but do not
--  necessarily have any other properties.
--------------------------------------------------------------------------------

record IsRawStruct {c ℓ} {A : Set c} (_≈_ : Rel A ℓ) {k} {K : ℕ → Set k} (appOp : ∀ {n} → K n → Vec A n → A) : Set (c ⊔ˡ ℓ ⊔ˡ k) where
  open Algebra.FunctionProperties _≈_
  field
    isEquivalence : IsEquivalence _≈_
    congⁿ : ∀ {n} (κ : K n) → Congruentₙ _≈_ (appOp κ)

  cong : ∀ {n} (κ : K n) {xs ys} → PointwiseFunc _≈_ xs ys (appOp κ xs ≈ appOp κ ys)
  cong κ {xs} = curryPW {xs = xs} (congⁿ κ)

  setoid : Setoid _ _
  setoid = record { isEquivalence = isEquivalence }

  ⟦_⟧ : ∀ {n} → K n → N-ary n A A
  ⟦ κ ⟧ = curryⁿ (appOp κ)

  _⟨_⟩_ : A → K 2 → A → A
  x ⟨ κ ⟩ y = ⟦ κ ⟧ x y

  open IsEquivalence isEquivalence public

record RawStruct {k} (K : ℕ → Set k) c ℓ : Set (sucˡ (c ⊔ˡ ℓ ⊔ˡ k)) where
  infix 4 _≈_

  field
    Carrier : Set c
    _≈_ : Rel Carrier ℓ
    appOp : ∀ {n} → K n → Vec Carrier n → Carrier
    isRawStruct : IsRawStruct _≈_ appOp

  open IsRawStruct isRawStruct public

  -- Form a structure over a new kind of operator by injecting from it.
  subRawStruct : ∀ {k′} {K′ : ℕ → Set k′} → (∀ {n} → K′ n → K n) → RawStruct K′ c ℓ
  subRawStruct liftK = record
    { Carrier = Carrier
    ; _≈_ = _≈_
    ; appOp = appOp ∘ liftK
    ; isRawStruct = record
      { isEquivalence = isEquivalence
      ; congⁿ = congⁿ ∘ liftK
      }
    }


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue293a where

open import Agda.Primitive
  using (Level; _⊔_) renaming (lzero to zero; lsuc to suc)

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

record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Carrier → Carrier → Set ℓ
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

module M (rm : RawMonoid zero zero) where

  open RawMonoid rm

  thm : ∀ x → x ∙ ε ≈ x
  thm = {!!}

  -- Previous agda2-goal-and-context:

  -- rm : RawMonoid zero zero
  -- ------------------------
  -- Goal: (x : RawMonoid.Carrier rm) →
  --       RawMonoid._≈_ rm (RawMonoid._∙_ rm x (RawMonoid.ε rm)) x

  -- Current agda2-goal-and-context:

  -- rm : RawMonoid zero zero
  -- ------------------------
  -- Goal: (x : Carrier) → x ∙ ε ≈ x

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

record RawMonoid′ : Set₁ where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set
    _≈_     : Carrier → Carrier → Set
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

module M′ (rm : RawMonoid′) where

  open RawMonoid′ rm

  thm′ : ∀ x → x ∙ ε ≈ x
  thm′ = {!!}

  -- Previous and current agda2-goal-and-context:

  -- rm : RawMonoid′
  -- ---------------
  -- Goal: (x : Carrier) → x ∙ ε ≈ x

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

-- UP isn't relevant.

record RawMonoid″ (Carrier : Set) : Set₁ where
  infixl 7 _∙_
  infix  4 _≈_
  field
    _≈_     : Carrier → Carrier → Set
    _∙_     : Carrier → Carrier → Carrier
    ε       : Carrier

data Bool : Set where
  true false : Bool

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

module M″ (rm : RawMonoid″ (List Bool)) where

  open RawMonoid″ rm

  thm″ : ∀ x → x ∙ ε ≈ x
  thm″ = {!!}

  -- Previous agda2-goal-and-context:

  -- rm : RawMonoid″ (List Bool)
  -- ---------------------------
  -- Goal: (x : List Bool) →
  --       RawMonoid″._≈_ rm (RawMonoid″._∙_ rm x (RawMonoid″.ε rm)) x

  -- Current agda2-goal-and-context:

  -- rm : RawMonoid″ (List Bool)
  -- ---------------------------
  -- Goal: (x : List Bool) → x ∙ ε ≈ x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Weight biased leftist heap that proves to maintain priority      --
-- invariant and uses a single-pass merging algorithm.              --
----------------------------------------------------------------------

{-# OPTIONS --sized-types #-}
module SinglePassMerge.PriorityProof where

open import Basics.Nat renaming (_≥_ to _≥ℕ_)
open import Basics
open import Sized

data Heap : {i : Size} → Priority → Set where
  empty : {i : Size} {n : Priority} → Heap {↑ i} n
  node  : {i : Size} {n : Priority} → (p : Priority) → Rank → p ≥ n →
          Heap {i} p → Heap {i} p → Heap {↑ i} n

rank : {b : Priority} → Heap b → Rank
rank empty            = zero
rank (node _ r _ _ _) = r

-- This implementation is derived in the same way as merge in
-- SinglePassMerge.NoProofs: depending on the size of new children we
-- swap parameters passed to node. Nothing really interesting.
merge : {i j : Size} {p : Nat} → Heap {i} p → Heap {j} p → Heap p
merge empty h2 = h2
merge h1 empty = h1
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  with order p1 p2
  | rank l1 ≥ℕ rank r1 + r-rank
  | rank l2 ≥ℕ rank r2 + l-rank
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | le p1≤p2 | true | _
  = node p1 (l-rank + r-rank) p1≥p l1 (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2))
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | le p1≤p2 | false | _
  = node p1 (l-rank + r-rank) p1≥p (merge {i} {↑ j} r1 (node p2 r-rank p1≤p2 l2 r2)) l1
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | ge p2≤p1 | _ | true
  = node p2 ((l-rank + r-rank)) p2≥p l2 (merge {↑ i} {j} (node p1 l-rank p2≤p1 l1 r1) r2)
merge .{↑ i} .{↑ j}
  (node {i} p1 l-rank p1≥p l1 r1)
  (node {j} p2 r-rank p2≥p l2 r2)
  | ge p2≤p1 | _ | false
  = node p2 ((l-rank + r-rank)) p2≥p (merge {↑ i} {j} (node p1 l-rank p2≤p1 l1 r1) r2) l2

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


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

open import lib.Base
open import lib.PathGroupoid

module lib.PathFunctor where

{- Nondependent stuff -}
module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  !-ap : {x y : A} (p : x == y)
    → ! (ap f p) == ap f (! p)
  !-ap idp = idp

  ap-! : {x y : A} (p : x == y)
    → ap f (! p) == ! (ap f p)
  ap-! idp = idp

  ∙-ap : {x y z : A} (p : x == y) (q : y == z)
    → ap f p ∙ ap f q == ap f (p ∙ q)
  ∙-ap idp q = idp

  ap-∙ : {x y z : A} (p : x == y) (q : y == z)
    → ap f (p ∙ q) == ap f p ∙ ap f q
  ap-∙ idp q = idp

  !ap-∙=∙-ap : {x y z : A} (p : x == y) (q : y == z)
    → ! (ap-∙ p q) == ∙-ap p q
  !ap-∙=∙-ap idp q = idp

  ∙∙-ap : {x y z w : A} (p : x == y) (q : y == z) (r : z == w)
    → ap f p ∙ ap f q ∙ ap f r == ap f (p ∙ q ∙ r)
  ∙∙-ap idp idp r = idp

  ap-∙∙ : {x y z w : A} (p : x == y) (q : y == z) (r : z == w)
    → ap f (p ∙ q ∙ r) == ap f p ∙ ap f q ∙ ap f r
  ap-∙∙ idp idp r = idp

  ap-∙∙∙ : {x y z w t : A} (p : x == y) (q : y == z) (r : z == w) (s : w == t)
    → ap f (p ∙ q ∙ r ∙ s) == ap f p ∙ ap f q ∙ ap f r ∙ ap f s
  ap-∙∙∙ idp idp idp s = idp

  ∙'-ap : {x y z : A} (p : x == y) (q : y == z)
    → ap f p ∙' ap f q == ap f (p ∙' q)
  ∙'-ap p idp = idp

  -- note: ap-∙' is defined in PathGroupoid

{- Dependent stuff -}
module _ {i j} {A : Type i} {B : A → Type j} (f : Π A B) where

  apd-∙ : {x y z : A} (p : x == y) (q : y == z)
    → apd f (p ∙ q) == apd f p ∙ᵈ apd f q
  apd-∙ idp idp = idp

  apd-∙' : {x y z : A} (p : x == y) (q : y == z)
    → apd f (p ∙' q) == apd f p ∙'ᵈ apd f q
  apd-∙' idp idp = idp

  apd-! : {x y : A} (p : x == y)
    → apd f (! p) == !ᵈ (apd f p)
  apd-! idp = idp

{- Over stuff -}
module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (f : {a : A} → B a → C a) where

  ap↓-◃ : {x y z : A} {u : B x} {v : B y} {w : B z}
    {p : x == y} {p' : y == z} (q : u == v [ B ↓ p ]) (r : v == w [ B ↓ p' ])
    → ap↓ f (q ◃ r) == ap↓ f q ◃ ap↓ f r
  ap↓-◃ {p = idp} {p' = idp} idp idp = idp

  ap↓-▹! : {x y z : A} {u : B x} {v : B y} {w : B z}
    {p : x == y} {p' : z == y} (q : u == v [ B ↓ p ]) (r : w == v [ B ↓ p' ])
    → ap↓ f (q ▹! r) == ap↓ f q ▹! ap↓ f r
  ap↓-▹! {p = idp} {p' = idp} idp idp = idp

{- Fuse and unfuse -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B) where
  ∘-ap : {x y : A} (p : x == y) → ap g (ap f p) == ap (g ∘ f) p
  ∘-ap idp = idp

  ap-∘ : {x y : A} (p : x == y) → ap (g ∘ f) p == ap g (ap f p)
  ap-∘ idp = idp

  !ap-∘=∘-ap : {x y : A} (p : x == y) → ! (ap-∘ p) == ∘-ap p
  !ap-∘=∘-ap idp = idp

ap-idf : ∀ {i} {A : Type i} {u v : A} (p : u == v) → ap (idf A) p == p
ap-idf idp = idp

{- Functoriality of [coe] -}
coe-∙ : ∀ {i} {A B C : Type i} (p : A == B) (q : B == C) (a : A)
  → coe (p ∙ q) a == coe q (coe p a)
coe-∙ idp q a = idp

coe-! : ∀ {i} {A B : Type i} (p : A == B) (b : B) → coe (! p) b == coe! p b
coe-! idp b = idp

coe!-inv-r : ∀ {i} {A B : Type i} (p : A == B) (b : B)
  → coe p (coe! p b) == b
coe!-inv-r idp b = idp

coe!-inv-l : ∀ {i} {A B : Type i} (p : A == B) (a : A)
  → coe! p (coe p a) == a
coe!-inv-l idp a = idp

coe-inv-adj : ∀ {i} {A B : Type i} (p : A == B) (a : A) →
  ap (coe p) (coe!-inv-l p a) == coe!-inv-r p (coe p a)
coe-inv-adj idp a = idp

coe!-inv-adj : ∀ {i} {A B : Type i} (p : A == B) (b : B) →
  ap (coe! p) (coe!-inv-r p b) == coe!-inv-l p (coe! p b)
coe!-inv-adj idp b = idp

coe-ap-! : ∀ {i j} {A : Type i} (P : A → Type j) {a b : A} (p : a == b)
  (x : P b)
  → coe (ap P (! p)) x == coe! (ap P p) x
coe-ap-! P idp x = idp

{- Functoriality of transport -}
transp-∙ : ∀ {i j} {A : Type i} {B : A → Type j} {x y z : A}
  (p : x == y) (q : y == z) (b : B x)
  → transport B (p ∙ q) b == transport B q (transport B p b)
transp-∙ idp _ _ = idp

transp-∙' : ∀ {i j} {A : Type i} {B : A → Type j} {x y z : A}
  (p : x == y) (q : y == z) (b : B x)
  → transport B (p ∙' q) b == transport B q (transport B p b)
transp-∙' _ idp _ = idp

{- Naturality of transport -}
transp-naturality : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
  (u : {a : A} → B a → C a)
  {a₀ a₁ : A} (p : a₀ == a₁)
  → u ∘ transport B p == transport C p ∘ u
transp-naturality f idp = idp

transp-idp : ∀ {i j} {A : Type i} {B : Type j}
  (f : A → B) {x y : A} (p : x == y)
  → transport (λ a → f a == f a) p idp == idp
transp-idp f idp = idp

module _ {i j} {A : Type i} {B : Type j} where

  ap-transp : (f g : A → B) {a₀ a₁ : A} (p : a₀ == a₁) (h : f a₀ == g a₀)
    → h ∙ ap g p == ap f p ∙ transport (λ a → f a == g a) p h
  ap-transp f g p@idp h = ∙-unit-r h

  ap-transp-idp : (f : A → B)
    {a₀ a₁ : A} (p : a₀ == a₁)
    → ap-transp f f p idp ◃∙
      ap (ap f p ∙_) (transp-idp f p) ◃∙
      ∙-unit-r (ap f p) ◃∎
      =ₛ
      []
  ap-transp-idp f p@idp = =ₛ-in idp

{- for functions with two arguments -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B → C) where

  ap2 : {x y : A} {w z : B}
    → (x == y) → (w == z) → f x w == f y z
  ap2 idp idp = idp

  ap2-out : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 p q ◃∎ =ₛ ap (λ u → f u w) p ◃∙ ap (λ v → f y v) q ◃∎
  ap2-out idp idp = =ₛ-in idp

  ap2-out' : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 p q ◃∎ =ₛ ap (λ u → f x u) q ◃∙ ap (λ v → f v z) p ◃∎
  ap2-out' idp idp = =ₛ-in idp

  ap2-idp-l : {x : A} {w z : B} (q : w == z)
    → ap2 (idp {a = x}) q == ap (f x) q
  ap2-idp-l idp = idp

  ap2-idp-r : {x y : A} {w : B} (p : x == y)
    → ap2 p (idp {a = w}) == ap (λ z → f z w) p
  ap2-idp-r idp = idp

  ap2-! : {a a' : A} {b b' : B} (p : a == a') (q : b == b')
    → ap2 (! p) (! q) == ! (ap2 p q)
  ap2-! idp idp = idp

  !-ap2 : {a a' : A} {b b' : B} (p : a == a') (q : b == b')
    → ! (ap2 p q) == ap2 (! p) (! q)
  !-ap2 idp idp = idp

  ap2-∙ : {a a' a'' : A} {b b' b'' : B}
    (p : a == a') (p' : a' == a'')
    (q : b == b') (q' : b' == b'')
    → ap2 (p ∙ p') (q ∙ q') == ap2 p q ∙ ap2 p' q'
  ap2-∙ idp p' idp q' = idp

  ∙-ap2 : {a a' a'' : A} {b b' b'' : B}
    (p : a == a') (p' : a' == a'')
    (q : b == b') (q' : b' == b'')
    → ap2 p q ∙ ap2 p' q' == ap2 (p ∙ p') (q ∙ q')
  ∙-ap2 idp p' idp q' = idp

{- ap2 lemmas -}
module _ {i j} {A : Type i} {B : Type j} where

  ap2-fst : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 (curry fst) p q == p
  ap2-fst idp idp = idp

  ap2-snd : {x y : A} {w z : B} (p : x == y) (q : w == z)
    → ap2 (curry snd) p q == q
  ap2-snd idp idp = idp

  ap-ap2 : ∀ {k l} {C : Type k} {D : Type l}
    (g : C → D) (f : A → B → C) {x y : A} {w z : B}
    (p : x == y) (q : w == z)
    → ap g (ap2 f p q) == ap2 (λ a b → g (f a b)) p q
  ap-ap2 g f idp idp = idp

  ap2-ap-l : ∀ {k l} {C : Type k} {D : Type l}
    (g : B → C → D) (f : A → B) {x y : A} {w z : C}
    (p : x == y) (q : w == z)
    → ap2 g (ap f p) q == ap2 (λ a c → g (f a) c) p q
  ap2-ap-l g f idp idp = idp

  ap2-ap-r : ∀ {k l} {C : Type k} {D : Type l}
    (g : A → C → D) (f : B → C) {x y : A} {w z : B}
    (p : x == y) (q : w == z)
    → ap2 g p (ap f q) == ap2 (λ a b → g a (f b)) p q
  ap2-ap-r g f idp idp = idp

  ap2-ap-lr : ∀ {k l m} {C : Type k} {D : Type l} {E : Type m}
    (g : C → D → E) (f : A → C) (h : B → D)
    {x y : A} {w z : B}
    (p : x == y) (q : w == z)
    → ap2 g (ap f p) (ap h q) == ap2 (λ a b → g (f a) (h b)) p q
  ap2-ap-lr g f h idp idp = idp

  ap2-diag : (f : A → A → B)
    {x y : A} (p : x == y)
    → ap2 f p p == ap (λ x → f x x) p
  ap2-diag f idp = idp

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B) where

  module _ {a a' a'' : A} (p : a == a') (p' : a' == a'') where
    ap-∘-∙-coh-seq₁ :
      ap (g ∘ f) (p ∙ p') =-= ap g (ap f p) ∙ ap g (ap f p')
    ap-∘-∙-coh-seq₁ =
      ap (g ∘ f) (p ∙ p')
        =⟪ ap-∙ (g ∘ f) p p' ⟫
      ap (g ∘ f) p ∙ ap (g ∘ f) p'
        =⟪ ap2 _∙_ (ap-∘ g f p) (ap-∘ g f p') ⟫
      ap g (ap f p) ∙ ap g (ap f p') ∎∎

    ap-∘-∙-coh-seq₂ :
      ap (g ∘ f) (p ∙ p') =-= ap g (ap f p) ∙ ap g (ap f p')
    ap-∘-∙-coh-seq₂ =
      ap (g ∘ f) (p ∙ p')
        =⟪ ap-∘ g f (p ∙ p') ⟫
      ap g (ap f (p ∙ p'))
        =⟪ ap (ap g) (ap-∙ f p p') ⟫
      ap g (ap f p ∙ ap f p')
        =⟪ ap-∙ g (ap f p) (ap f p') ⟫
      ap g (ap f p) ∙ ap g (ap f p') ∎∎

  ap-∘-∙-coh :  {a a' a'' : A} (p : a == a') (p' : a' == a'')
    → ap-∘-∙-coh-seq₁ p p' =ₛ ap-∘-∙-coh-seq₂ p p'
  ap-∘-∙-coh idp idp = =ₛ-in idp

module _ {i} {A : Type i} where

  ap-null-homotopic : ∀ {k} {B : Type k} (f : A → B) {b : B}
    (h : (x : A) → f x == b) {x y : A} (p : x == y)
    → ap f p == h x ∙ ! (h y)
  ap-null-homotopic f h {x} p@idp = ! (!-inv-r (h x))

module _ {i j} {A : Type i} {B : Type j} (b : B) where

  ap-cst : {x y : A} (p : x == y)
    → ap (cst b) p == idp
  ap-cst = ap-null-homotopic (cst b) (cst idp)

  ap-cst-coh : {x y z : A} (p : x == y) (q : y == z)
    → ap-cst (p ∙ q) ◃∎
      =ₛ
      ap-∙ (cst b) p q ◃∙
      ap2 _∙_ (ap-cst p) (ap-cst q) ◃∎
  ap-cst-coh idp idp = =ₛ-in idp

ap-∘-cst-coh : ∀ {i} {j} {k} {A : Type i} {B : Type j} {C : Type k}
  (g : B → C) (b : B)
  {x y : A} (p : x == y)
  → ∘-ap g (λ _ → b) p ◃∙
    ap-cst (g b) p ◃∎
    =ₛ
    ap (ap g) (ap-cst b p) ◃∎
ap-∘-cst-coh g b p@idp = =ₛ-in idp

{- Naturality of homotopies -}

module _ {i} {A : Type i} where

  homotopy-naturality : ∀ {k} {B : Type k} (f g : A → B)
    (h : (x : A) → f x == g x) {x y : A} (p : x == y)
    → ap f p ◃∙ h y ◃∎ =ₛ h x ◃∙ ap g p ◃∎
  homotopy-naturality f g h {x} idp =
    =ₛ-in (! (∙-unit-r (h x)))

  homotopy-naturality-to-idf : (f : A → A)
    (h : (x : A) → f x == x) {x y : A} (p : x == y)
    → ap f p ◃∙ h y ◃∎ =ₛ h x ◃∙ p ◃∎
  homotopy-naturality-to-idf f h {x} p = =ₛ-in $
    =ₛ-out (homotopy-naturality f (λ a → a) h p) ∙ ap (λ w → h x ∙ w) (ap-idf p)

  homotopy-naturality-from-idf : (g : A → A)
    (h : (x : A) → x == g x) {x y : A} (p : x == y)
    → p ◃∙ h y ◃∎ =ₛ h x ◃∙ ap g p ◃∎
  homotopy-naturality-from-idf g h {y = y} p = =ₛ-in $
    ap (λ w → w ∙ h y) (! (ap-idf p)) ∙ =ₛ-out (homotopy-naturality (λ a → a) g h p)

  homotopy-naturality-to-cst : ∀ {k} {B : Type k} (f : A → B) (b : B)
    (h : (x : A) → f x == b) {x y : A} (p : x == y)
    → ap f p ◃∙ h y ◃∎ =ₛ h x ◃∎
  homotopy-naturality-to-cst f b h p@idp = =ₛ-in idp

  ap-null-homotopic-cst : ∀ {k} {B : Type k}
    (b₀ b₁ : B) (h : A → b₀ == b₁) {x y : A} (p : x == y)
    → ap-null-homotopic (cst b₀) h p ◃∙
      ap (λ v → h v ∙ ! (h y)) p ◃∙
      !-inv-r (h y) ◃∎
      =ₛ
      ap-cst b₀ p ◃∎
  ap-null-homotopic-cst b₀ b₁ h {x} p@idp =
    =ₛ-in (!-inv-l (!-inv-r (h x)))

module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         (f g : A → B → C) (h : ∀ a b → f a b == g a b) where
  homotopy-naturality2 : {a₀ a₁ : A} {b₀ b₁ : B} (p : a₀ == a₁) (q : b₀ == b₁)
    → ap2 f p q ◃∙ h a₁ b₁ ◃∎ =ₛ h a₀ b₀ ◃∙ ap2 g p q ◃∎
  homotopy-naturality2 {a₀ = a} {b₀ = b} idp idp =
    =ₛ-in (! (∙-unit-r (h a b)))

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B → C) where

  ap-comm : {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    → ap (λ a → f a b₀) p ∙ ap (λ z → f a₁ z) q ==
      ap (λ z → f a₀ z) q ∙ ap (λ a → f a b₁) p
  ap-comm p q = ! (=ₛ-out (ap2-out f p q)) ∙ =ₛ-out (ap2-out' f p q)

  ap-comm-=ₛ : {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    → ap (λ a → f a b₀) p ◃∙ ap (λ z → f a₁ z) q ◃∎ =ₛ
      ap (λ z → f a₀ z) q ◃∙ ap (λ a → f a b₁) p ◃∎
  ap-comm-=ₛ p q = =ₛ-in (ap-comm p q)

  ap-comm' : {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    → ap (λ a → f a b₀) p ∙' ap (λ z → f a₁ z) q ==
      ap (λ z → f a₀ z) q ∙ ap (λ a → f a b₁) p
  ap-comm' p idp = idp

  ap-comm-cst-seq : {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    (c : C) (h₀ : ∀ b → f a₀ b == c)
    → ap (λ a → f a b₀) p ∙ ap (λ b → f a₁ b) q =-=
      ap (λ z → f a₀ z) q ∙ ap (λ a → f a b₁) p
  ap-comm-cst-seq {a₀} {a₁} p {b₀} {b₁} q c h₀ =
    ap (λ a → f a b₀) p ∙ ap (λ b → f a₁ b) q
      =⟪ ap (ap (λ a → f a b₀) p ∙_) $
        ap-null-homotopic (λ b → f a₁ b) h₁ q ⟫
    ap (λ a → f a b₀) p ∙ h₁ b₀ ∙ ! (h₁ b₁)
      =⟪ ap (ap (λ a → f a b₀) p ∙_) $ ap (λ k → k h₀) $
        transp-naturality {B = λ a → ∀ b → f a b == c} (λ h → h b₀ ∙ ! (h b₁)) p ⟫
    ap (λ a → f a b₀) p ∙ transport (λ a → f a b₀ == f a b₁) p (h₀ b₀ ∙ ! (h₀ b₁))
      =⟪ ! (ap-transp (λ a → f a b₀) (λ a → f a b₁) p (h₀ b₀ ∙ ! (h₀ b₁))) ⟫
    (h₀ b₀ ∙ ! (h₀ b₁)) ∙ ap (λ a → f a b₁) p
      =⟪ ! (ap (_∙ ap (λ a → f a b₁) p) $
              (ap-null-homotopic (λ b → f a₀ b) h₀ q)) ⟫
    ap (λ z → f a₀ z) q ∙ ap (λ a → f a b₁) p ∎∎
    where
      h₁ : ∀ b → f a₁ b == c
      h₁ = transport (λ a → ∀ b → f a b == c) p h₀

  ap-comm-cst-coh : {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    (c : C) (h₀ : ∀ b → f a₀ b == c)
    → ap-comm p q ◃∎ =ₛ
      ap-comm-cst-seq p q c h₀
  ap-comm-cst-coh p@idp {b₀} q@idp c h₀ = =ₛ-in $ ! $
    ap (idp ∙_) (! (!-inv-r (h₀ b₀))) ∙
    ! (∙-unit-r (h₀ b₀ ∙ ! (h₀ b₀))) ∙
    ! (ap (_∙ idp) (! (!-inv-r (h₀ b₀))))
      =⟨ ap (_∙ ! (∙-unit-r (h₀ b₀ ∙ ! (h₀ b₀))) ∙ ! (ap (_∙ idp) (! (!-inv-r (h₀ b₀)))))
            (ap-idf (! (!-inv-r (h₀ b₀)))) ⟩
    ! (!-inv-r (h₀ b₀)) ∙
    ! (∙-unit-r (h₀ b₀ ∙ ! (h₀ b₀))) ∙
    ! (ap (_∙ idp) (! (!-inv-r (h₀ b₀))))
      =⟨ ap (λ v → ! (!-inv-r (h₀ b₀)) ∙ ! (∙-unit-r (h₀ b₀ ∙ ! (h₀ b₀))) ∙ v)
            (!-ap (_∙ idp) (! (!-inv-r (h₀ b₀)))) ⟩
    ! (!-inv-r (h₀ b₀)) ∙
    ! (∙-unit-r (h₀ b₀ ∙ ! (h₀ b₀))) ∙
    ap (_∙ idp) (! (! (!-inv-r (h₀ b₀))))
      =⟨ ap (! (!-inv-r (h₀ b₀)) ∙_) $ ! $ =ₛ-out $
         homotopy-naturality-from-idf (_∙ idp)
                                      (λ p → ! (∙-unit-r p))
                                      (! (! (!-inv-r (h₀ b₀)))) ⟩
    ! (!-inv-r (h₀ b₀)) ∙ ! (! (!-inv-r (h₀ b₀))) ∙ idp
      =⟨ ap (! (!-inv-r (h₀ b₀)) ∙_) (∙-unit-r (! (! (!-inv-r (h₀ b₀))))) ⟩
    ! (!-inv-r (h₀ b₀)) ∙ ! (! (!-inv-r (h₀ b₀)))
      =⟨ !-inv-r (! (!-inv-r (h₀ b₀))) ⟩
    idp =∎

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} where

  ap-comm-comm : (f : A → B → C) {a₀ a₁ : A} (p : a₀ == a₁) {b₀ b₁ : B} (q : b₀ == b₁)
    → ap-comm f p q == ! (ap-comm (λ x y → f y x) q p)
  ap-comm-comm f p@idp q@idp = idp

module _ {i} {A : Type i} where

  -- unsure where this belongs
  transp-cst=idf : {a x y : A} (p : x == y) (q : a == x)
    → transport (λ x → a == x) p q == q ∙ p
  transp-cst=idf idp q = ! (∙-unit-r q)

  transp-cst=idf-pentagon : {a x y z : A}
    (p : x == y) (q : y == z) (r : a == x)
    → transp-cst=idf (p ∙ q) r ◃∎ =ₛ
      transp-∙ p q r ◃∙
      ap (transport (λ x → a == x) q) (transp-cst=idf p r) ◃∙
      transp-cst=idf q (r ∙ p) ◃∙
      ∙-assoc r p q ◃∎
  transp-cst=idf-pentagon idp q idp =
    =ₛ-in (! (∙-unit-r (transp-cst=idf q idp)))

{- for functions with more arguments -}
module _ {i₀ i₁ i₂ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂}
  {B : Type j} (f : A₀ → A₁ → A₂ → B) where

  ap3 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → f x₀ x₁ x₂ == f y₀ y₁ y₂
  ap3 idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → B) where

  ap4 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → f x₀ x₁ x₂ x₃ == f y₀ y₁ y₂ y₃
  ap4 idp idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ i₄ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {A₄ : Type i₄} {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → A₄ → B) where

  ap5 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃} {x₄ y₄ : A₄}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → (x₄ == y₄)
    → f x₀ x₁ x₂ x₃ x₄ == f y₀ y₁ y₂ y₃ y₄
  ap5 idp idp idp idp idp = idp

module _ {i₀ i₁ i₂ i₃ i₄ i₅ j} {A₀ : Type i₀} {A₁ : Type i₁} {A₂ : Type i₂} {A₃ : Type i₃}
  {A₄ : Type i₄} {A₅ : Type i₅} {B : Type j} (f : A₀ → A₁ → A₂ → A₃ → A₄ → A₅ → B) where

  ap6 : {x₀ y₀ : A₀} {x₁ y₁ : A₁} {x₂ y₂ : A₂} {x₃ y₃ : A₃} {x₄ y₄ : A₄} {x₅ y₅ : A₅}
    → (x₀ == y₀) → (x₁ == y₁) → (x₂ == y₂) → (x₃ == y₃) → (x₄ == y₄) → (x₅ == y₅)
    → f x₀ x₁ x₂ x₃ x₄ x₅ == f y₀ y₁ y₂ y₃ y₄ y₅
  ap6 idp idp idp idp idp idp = idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.constr.findInScope:10 #-} -- -v tc.conv.elim:25 #-}
-- Andreas, 2012-07-01
module Issue670a where

import Common.Level
open import Common.Equality

findRefl : {A : Set}(a : A){{p : a ≡ a}} → a ≡ a
findRefl a {{p}} = p

uip : {A : Set}{a : A} → findRefl a ≡ refl
uip = refl
-- this should work.  Used to throw an internal error in Conversion,
-- because the solution for p was refl applied to parameters, instead of just refl.


text:
module BasicIO where

open import Agda.Builtin.IO public
open import Data.Char
open import Data.List

{-# FOREIGN GHC import Control.Exception #-}
{-# FOREIGN GHC import System.Environment #-}

-- This is easier than using the IO functions in the standard library,
-- but it's technically not as type-safe. And it bypasses the
-- termination checker.
postulate
  return : {A : Set} → A → IO A
  _>>_ : {A B : Set} → IO A → IO B → IO B
  _>>=_ : {A B : Set} → IO A → (A → IO B) → IO B
  fail : {A : Set} → List Char → IO A
  bracket : {A B C : Set} → IO A → (A → IO B) → (A → IO C) → IO C
  getArgs : IO (List (List Char))

{-# COMPILE GHC return = \_ -> return #-}
{-# COMPILE GHC _>>_ = \_ _ -> (>>) #-}
{-# COMPILE GHC _>>=_ = \_ _ -> (>>=) #-}
{-# COMPILE GHC fail = \_ -> fail #-}
{-# COMPILE GHC bracket = \ _ _ _ -> bracket #-}
{-# COMPILE GHC getArgs = getArgs #-}

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


text:
-- Andreas, 2016-12-20, issue #2350
-- Agda ignores a wrong instance parameter to a constructor

data D {{a}} (A : Set a) : Set a where
  c : A → D A

test : ∀ ℓ {ℓ'} (A : Set ℓ') {B : Set ℓ} (a : A) → D A
test ℓ A a = c {{ℓ}} a

-- Expected Error:
-- .ℓ' != ℓ of type .Agda.Primitive.Level
-- when checking that the expression a has type A

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.Free where

open import Categories.Category
open import Categories.Free.Core
open import Categories.Free.Functor
open import Categories.Graphs.Underlying
open import Categories.Functor
  using (Functor)
open import Graphs.Graph
open import Graphs.GraphMorphism
  using (GraphMorphism; module GraphMorphism)
open import Data.Star

-- Exports from other modules:
--    Free₀, Free₁ and Free
open Categories.Free.Core public
  using (Free₀)
open Categories.Free.Functor public
  using (Free)

-- TODO:
--  Prove Free⊣Underlying : Adjunction Free Underlying
--  Define Adjunction.left and Adjunction.right as conveniences
--    (or whatever other names make sense for the hom-set maps
--    C [ F _ , _ ] → D [ _ , G _ ] and inverse, respectively)
--  Let Cata = Adjunction.left Free⊣Underlying
Cata : ∀{o₁ ℓ₁ e₁}{G : Graph    o₁ ℓ₁ e₁}
        {o₂ ℓ₂ e₂}{C : Category o₂ ℓ₂ e₂}
  → (F : GraphMorphism G (Underlying₀ C))
  → Functor (Free₀ G) C
Cata {G = G} {C = C} F = record
  { F₀            = F₀
  ; F₁            = F₁*
  ; identity      = refl
  ; homomorphism  = λ{X}{Y}{Z}{f}{g} → homomorphism {X}{Y}{Z}{f}{g}
  ; F-resp-≡      = F₁*-resp-≡
  }
  where
    open Category C
    open GraphMorphism F
    open Equiv
    open HomReasoning
    open PathEquality using (ε-cong; _◅-cong_)

    F₁* : ∀ {A B} → Free₀ G [ A , B ] → C [ F₀ A , F₀ B ]
    F₁* ε = id
    F₁* (f ◅ fs) = F₁* fs ∘ F₁ f

    .homomorphism : ∀ {X Y Z} {f : Free₀ G [ X , Y ]} {g : Free₀ G [ Y , Z ]}
                  → C [ F₁* (Free₀ G [ g ∘ f ]) ≡ C [ F₁* g ∘ F₁* f ] ]
    homomorphism {f = ε} = sym identityʳ
    homomorphism {f = f ◅ fs}{gs} =
      begin
        F₁* (fs ◅◅ gs) ∘ F₁ f
      ↓⟨ homomorphism {f = fs}{gs} ⟩∘⟨ refl ⟩
        (F₁* gs ∘ F₁* fs) ∘ F₁ f
      ↓⟨ assoc ⟩
        F₁* gs ∘ F₁* fs ∘ F₁ f
      ∎

    .F₁*-resp-≡ : ∀ {A B} {f g : Free₀ G [ A , B ]} → Free₀ G [ f ≡ g ] → C [ F₁* f ≡ F₁* g ]
    F₁*-resp-≡ {f = ε}{.ε} ε-cong = refl
    F₁*-resp-≡ {f = f ◅ fs}{g ◅ gs} (f≈g ◅-cong fs≈gs) =
      begin
        F₁* fs ∘ F₁ f
      ↓⟨ F₁*-resp-≡ fs≈gs ⟩∘⟨ F-resp-≈ f≈g ⟩
        F₁* gs ∘ F₁ g
      ∎
    F₁*-resp-≡ {f = f ◅ fs}{ε} ()

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

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

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

open import Function

open import Types.Direction

open import Auxiliary.Extensionality

open import Max hiding (n)

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

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

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

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

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

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

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

open import Agda.Builtin.Equality.Rewrite

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

module Alternative-Substitution where

  -- analogous to https://plfa.github.io/DeBruijn/

  -- extending a map by an identity segment

  extV : (Fin m → Fin n) → (Fin (suc m) → Fin (suc n))
  extV ρ zero = zero
  extV ρ (suc i) = suc (ρ i)

  -- renaming / can be used for weakening one binding as @rename suc@

  renameT : (Fin m → Fin n) → TType m → TType n
  renameS : (Fin m → Fin n) → SType m → SType n

  renameT ρ TInt = TInt
  renameT ρ (TChn S) = TChn (renameS ρ S)

  renameS ρ (xmt d T S) = xmt d (renameT ρ T) (renameS ρ S)
  renameS ρ end = end
  renameS ρ (rec S) = rec (renameS (extV ρ) S)
  renameS ρ (var x) = var (ρ x)

  -- extending a map from variables to terms

  extS : (Fin m → SType n) → (Fin (suc m) → SType (suc n))
  extS σ zero = var zero
  extS σ (suc i) = renameS suc (σ i)

  -- simultaneous substitution

  substT : (Fin m → SType n) → TType m → TType n
  substS : (Fin m → SType n) → SType m → SType n

  substT σ TInt = TInt
  substT σ (TChn S) = TChn (substS σ S)

  substS σ (xmt d T S) = xmt d (substT σ T) (substS σ S)
  substS σ end = end
  substS σ (rec S) = rec (substS (extS σ) S)
  substS σ (var x) = σ x

  -- single substitution

  mk-σ : SType n → Fin (suc n) → SType n
  mk-σ S' zero = S'
  mk-σ S' (suc x) = var x

  substT1 : SType n → TType (suc n) → TType n
  substT1 S' T = substT (mk-σ S') T

  substS1 : SType n → SType (suc n) → SType n
  substS1 S' S = substS (mk-σ S') S

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

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

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

increaseS m (xmt d t s) = xmt d (increaseT m t) (increaseS m s)
increaseS m (rec s) = rec (increaseS m s)
increaseS m (var x) = var (inject+ m x) -- should say increase here
increaseS m end = end

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

-- weaken m is used to push a (closed) term under m new binders
weakenS : ∀ m → SType n → SType (n +ℕ m)
weakenT : ∀ m → TType n → TType (n +ℕ m)

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

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

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

-- this one behaves correctly
weaken'S : ∀ m → Fin (suc n) → SType n → SType (n +ℕ m)
weaken'T : ∀ m → Fin (suc n) → TType n → TType (n +ℕ m)

weaken'S m i (xmt d T S) = xmt d (weaken'T m i T) (weaken'S m i S)
weaken'S m i end = end
weaken'S m i (rec S) = rec (weaken'S m (suc i) S)
weaken'S {suc n} m zero (var x) = var (increase m x)
weaken'S {suc n} m (suc i) (var x)
  with compare i x
weaken'S {suc n} m (suc .(inject least)) (var x) | less .x least = var (increase m x)
weaken'S {suc n} m (suc i) (var .i) | equal .i = var (inject+ m i)
weaken'S {suc n} m (suc i) (var .(inject least)) | greater .i least = var (inject+ m (inject least))

weaken'T m i TInt = TInt
weaken'T m i (TChn S) = TChn (weaken'S m i S)

weaken'S0 : ∀ m → SType n → SType (n +ℕ m)
weaken'S0 m S = weaken'S m (fromℕ _) S

----------------------------------------------------------------------
-- examples

module Examples-Weakening where

  sv0 sv1 : SType 1
  sv0 = rec (var zero)
  sv1 = rec (var (suc zero))

  sv0-w : SType 2
  sv0-w = weaken'S 1 zero sv0

  step0 : weaken'S{2} 1 zero (var zero) ≡ var (suc zero)
        × weaken'S{2} 1 zero (var (suc zero)) ≡ var (suc (suc zero))
  step0 = refl , refl

  step1 : weaken'S{2} 1 (suc zero) (var zero) ≡ var zero
        × weaken'S{2} 1 (suc zero) (var (suc zero)) ≡ var (suc (suc zero))
  step1 = refl , refl

  stepr1 : weaken'S 1 zero sv0 ≡ rec (var zero)
         × weaken'S 1 zero sv1 ≡ rec (var (suc (suc zero)))
  stepr1 = refl , refl

  stepr2 : weaken'S{3} 1 zero (rec (rec (var zero))) ≡ rec (rec (var zero))
         × weaken'S{3} 1 zero (rec (rec (var (suc zero)))) ≡ rec (rec (var (suc zero)))
         × weaken'S{3} 1 zero (rec (rec (var (suc (suc zero))))) ≡ rec (rec (var (suc (suc (suc zero)))))
  stepr2 = refl , refl , refl

  sx1 : SType 0
  sx1 = rec (xmt SND TInt (var zero))

  sx1-w : SType 1
  sx1-w = rec (xmt SND TInt (var zero))

  sx1=sx1-w : sx1-w ≡ weaken'S 1 zero sx1
  sx1=sx1-w = refl

  sx2 : SType 1
  sx2 = xmt SND TInt (var zero)

  sx2-w1 : SType 2
  sx2-w1 = xmt SND TInt (var (suc zero))

  sx2-w0 : SType 2
  sx2-w0 = xmt SND TInt (var zero)

  sx2=w : sx2-w1 ≡ weaken'S 1 zero sx2
        × sx2-w0 ≡ weaken'S 1 (suc zero) sx2
  sx2=w = refl , refl

  open Alternative-Substitution

  step0-r : renameS suc sv0 ≡ rec (var zero)
          × renameS suc sv1 ≡ rec (var (suc (suc zero)))
  step0-r = refl , refl

  step1-r : renameS{1} suc (rec (rec (var zero))) ≡ (rec (rec (var zero)))
          × renameS{1} suc (rec (rec (var (suc zero)))) ≡ (rec (rec (var (suc zero))))
          × renameS{1} suc (rec (rec (var (suc (suc zero))))) ≡ (rec (rec (var (suc (suc (suc zero))))))
  step1-r = refl , refl , refl

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

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

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

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

  cn1 : ¬ Contractive {2} (suc zero) (var zero)
  cn1 (con-var ())

  cp1 : Contractive {2} zero (var (suc zero))
  cp1 = con-var z≤n

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

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

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

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

  sp2 : SType 0
  sp2 = s3

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

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

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

module Alternative-Unfolding where
  open Alternative-Substitution

  -- one top-level unfolding if possible

  unfold₁ : SType n → SType n
  unfold₁ (rec S) = substS1 (rec S) S
  unfold₁ S@(xmt d T x) = S
  unfold₁ S@end = S
  unfold₁ S@(var x) = S

  -- unfold all the way

  unfold : (S : SType n) (σ : SType n → SType m) → SType m
  unfold S@(xmt d T S') σ = σ S
  unfold end σ = end
  unfold (rec S) σ = unfold S (σ ∘ substS1 (rec S))
  unfold S@(var x) σ = σ S

  unfold₀ : SType n → SType n
  unfold₀ S = unfold S id

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  infer-p2 : infer-contractive sp2 zero ≡ yes cp2
  infer-p2 = refl

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

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

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

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

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

ct-weaken+ : {T : TType n} → ContractiveT T → ContractiveT (weaken'T 1 zero T)
c-weaken+ : {S : SType n} → Contractive i S → Contractive (suc i) (weaken'S 1 zero S)

ct-weaken+ con-int = con-int
ct-weaken+ (con-chn x) = con-chn (c-weakenS! (c-weaken+ x))

c-weaken+ (con-xmt x cis) = con-xmt (ct-weaken+ x) (c-weakenS! (c-weaken+ cis))
c-weaken+ con-end = con-end
c-weaken+ (con-rec cis) = con-rec {!!} -- gives a problem: (c-weaken+ {!cis!})
c-weaken+ {suc n} {i} {var j} (con-var i≤j) = con-var (s≤s i≤j)

module Alternative-Multiple-Substitution-Preserves where

  open Alternative-Substitution

  subst-contr-T :
    {T : TType m}
    (σ : Fin m → SType n)
    (γ : (j : Fin m) → Contractive i (σ j))
    (ct : ContractiveT T)
    → ContractiveT (substT σ T)

  subst-contr-S : ∀ {k} →
    (σ : Fin m → SType n)
    (γ : (j : Fin m) → Contractive k (σ j))
    (c : Contractive zero S)
    → Contractive k (substS σ S)

  subst-contr-T σ γ con-int = con-int
  subst-contr-T σ γ (con-chn cs) = con-chn (subst-contr-S σ (c-weakenS! ∘ γ) cs)

  subst-contr-S σ γ (con-xmt ct cs) =
    con-xmt (subst-contr-T σ γ ct) (subst-contr-S σ (c-weakenS! ∘ γ) cs)
  subst-contr-S σ γ con-end = con-end
  subst-contr-S σ γ (con-rec cs) = con-rec (subst-contr-S (extS σ) {!extS!} (c-weakenS₁ cs))
  subst-contr-S σ γ (con-var{j} x) = γ j

module Alternative-Substitution-Preserves where

  open Alternative-Substitution

  subst-contr-T :
    {S' : SType n} (c' : Contractive i S')
    {T : TType (suc n)} (c : ContractiveT T)
      → ContractiveT (substT1 S' T)
  subst-contr-S :
    {S' : SType n} (c' : Contractive i S')
    {S : SType (suc n)} (c : Contractive (inject₁ i) S)
      → Contractive i (substS1 S' S)

  subst-contr-T c' con-int = con-int
  subst-contr-T c' (con-chn x) = con-chn (subst-contr-S (c-weakenS! c') x)

  subst-contr-S c' (con-xmt ct cs) =
    con-xmt (subst-contr-T c' ct) (subst-contr-S (c-weakenS! c') cs)
  subst-contr-S c' con-end = con-end
  subst-contr-S c' (con-rec c) = con-rec {!!} -- (subst-contr-S {!!} {!c!})
  subst-contr-S c' (con-var x) = {!!}

module Alternative-SingleSubstitution where
  ----------------------------------------------------------------------
  -- single substitution of j ↦ Sj

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

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

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

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

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

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

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

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

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

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

unfoldmS : (S : SType n) → SType n
unfoldmS (xmt d T S) = xmt d T S
unfoldmS end = end
unfoldmS (rec S) = subst-maxS (rec S) S
unfoldmS {suc n} (var x) = var x

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

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

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

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

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

-- one step unfolding preserves contractivity

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

-- multiple unfolding
-- terminates even for non-contractive types because it delays the substitution

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

-- unclear how this could be completed
-- unfold!-contr : Contractive i S → Contractive i (unfold! S id)
-- unfold!-contr (con-xmt x cs) = con-xmt x cs
-- unfold!-contr con-end = con-end
-- unfold!-contr (con-rec cs) = {!!}

-- multiple unfolding preserves contractivity

TCType : (n : ℕ) → Set
TCType n = Σ (TType n) ContractiveT

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

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

{-# TERMINATING #-}
unfold!!! : ∀ {m n : ℕ} → SCType (n +ℕ m) zero → (SCType (n +ℕ m) zero → SCType m zero) → SCType m zero
unfold!!! SC@(xmt d T S , con-xmt x cs) σ = σ SC
unfold!!! (end , con-end) σ = end , con-end
unfold!!! (rec S , con-rec cs) σ =
  unfold!!! (S , c-weakenS₁ cs) (σ ∘ λ SC → (subst-maxS (rec S) (proj₁ SC)) , (subst-contr-mS (proj₂ SC) (con-rec cs)))
unfold!!! SC@(var x , con-var x₁) σ = σ SC

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

variable
  T₁ T₂ : TCType n
  S₁ S₂ : SCType n i

data EquivT (R : SCType n zero → SCType n zero → Set) : TCType n → TCType n → Set where
  eq-int : EquivT R (TInt , con-int) (TInt , con-int)
  eq-chn : R S₁ S₂ →
    EquivT R (TChn (proj₁ S₁) , con-chn (proj₂ S₁))
             (TChn (proj₁ S₂) , con-chn (proj₂ S₂))

data EquivS (R : SCType n zero → SCType n zero → Set) :
     (S₁ S₂ : SCType n zero) → Set where
  eq-end :
    EquivS R (end , con-end) (end , con-end)
  eq-xmt : (d : Dir) →
    EquivT R T₁ T₂ →
    R S₁ S₂ →
    EquivS R (xmt d (proj₁ T₁) (proj₁ S₁) , con-xmt (proj₂ T₁) (proj₂ S₁))
             (xmt d (proj₁ T₂) (proj₁ S₂) , con-xmt (proj₂ T₂) (proj₂ S₂))
  eq-rec-l :
    let S = proj₁ S₁ in
    let cs = proj₂ S₁ in
    EquivS R (subst-maxS (rec S) S , subst-contr-mS (c-weakenS₁ cs) (con-rec cs)) S₂ →
    EquivS R (rec S , con-rec cs) S₂
  eq-rec-r :
    let S = proj₁ S₂ in
    let cs = proj₂ S₂ in
    EquivS R S₁ (subst-maxS (rec S) S , subst-contr-mS (c-weakenS₁ cs) (con-rec cs)) →
    EquivS R S₁ (rec S , con-rec cs)

record Equiv (S₁ S₂ : SCType 0 zero) : Set where
  coinductive
  field force : EquivS Equiv (unfold!! S₁ id) (unfold!! S₂ id)

record Equiv' (S₁ S₂ : SCType n zero) : Set where
  coinductive
  field force : EquivS Equiv' (unfold!!!{n = 0} S₁ id) (unfold!!!{n = 0} S₂ id)

{-# TERMINATING #-}
equivt-refl : ∀ T → EquivT Equiv T T
equivs-refl : ∀ S → EquivS Equiv S S
equiv-refl : ∀ S → Equiv S S

equivt-refl (TInt , con-int) = eq-int
equivt-refl (TChn S , con-chn x) = eq-chn (equiv-refl (S , x))

equivs-refl (xmt d t s , con-xmt ct cs) = eq-xmt d (equivt-refl (t , ct)) (equiv-refl (s , cs))
equivs-refl (end , con-end) = eq-end
equivs-refl (rec s , con-rec cs) = eq-rec-l (eq-rec-r (equivs-refl ((subst-maxS (rec s) s) , (subst-contr-mS (c-weakenS₁ cs) (con-rec cs)))))

Equiv.force (equiv-refl S) = equivs-refl (unfold!! S id)

----------------------------------------------------------------------
-- prove equivalence of one-level unrolling
-- μX S ≈ S [μX S / X]

module μ-unrolling where

  unfold-≡ : ∀ S cs →
    unfold!! (S , cs) (λ { (S' , c') → (subst-maxS (rec S) S') , (subst-contr-mS (c-weakenS₁ c') (con-rec cs)) })
    ≡
      (unfold!!
       (subst-maxS (rec S) S ,
        subst-contr-mS (c-weakenS₁ cs) (con-rec cs))
       id)

  unfold-≡ (xmt d T S) (con-xmt x cs) = refl
  unfold-≡ end con-end = refl
  unfold-≡ (rec S) (con-rec cs) = {!!}
  unfold-≡ (var x) (con-var x₁)
    with max? x
  unfold-≡ (var x) (con-var x₁) | yes p = {!!}
  unfold-≡ (var x) (con-var x₁) | no ¬p = refl

  unroll : SCType n i → SCType n i
  unroll SC@(xmt d T S , con-xmt x cs) = SC
  unroll SC@(end , con-end) = SC
  unroll (rec S , cs@(con-rec cs')) = (subst-maxS (rec S) S) , (subst-contr-mS (c-weakenS₁ cs') cs)
  unroll SC@(var x , con-var x₁) = SC

  unroll-equiv : (SC : SCType 0 zero) → Equiv SC (unroll SC)
  Equiv.force (unroll-equiv SC@(xmt d T S , con-xmt x cs))
    with unroll SC
  ... | SC' = equivs-refl SC'
  Equiv.force (unroll-equiv (end , con-end)) = eq-end
  Equiv.force (unroll-equiv (rec S , con-rec cs))
    rewrite unfold-≡ S cs =
    let S₁ = unfold!! (S , cs) (λ { (S' , c') → (subst-maxS (rec S) S') , (subst-contr-mS (c-weakenS₁ c') (con-rec cs)) }) in
    let eqx = equivs-refl S₁ in
    {!S₁!}

----------------------------------------------------------------------
-- prove the folk theorem
-- μX μY S = μY [Y/X]S

module μ-examples where

  r1 : SType 0
  r1 = rec (rec (xmt SND (TChn (var zero)) (var (suc zero))))

  r2 : SType n
  r2 = rec (xmt SND (TChn (var zero)) (var zero))

  r2a : SType 0
  r2a = rec r2

  r2b : SType n
  r2b = rec (rec (xmt SND (TChn (var zero)) (var (suc zero))))

  r2-unfolded : SType 0
  r2-unfolded = xmt SND (TChn r2) r2

  r2-unf : SType 0
  r2-unf = rec (xmt SND (TChn (var zero)) r2b)

  rc2-unf : SCType 0 zero
  rc2-unf = r2-unf , (con-rec (con-xmt (con-chn (con-var z≤n)) (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n))))))

  rc1 : SCType 0 zero
  rc1 = r1 , (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n))))

  rc2 : SCType n zero
  rc2 = r2 , (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))

  rc2a : SCType 0 zero
  rc2a = r2a , con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))

  rc2b : SCType n zero
  rc2b = r2b , con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))

  rc2-unfolded : SCType 0 zero
  rc2-unfolded = r2-unfolded , (con-xmt (con-chn (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))) (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n))))

  rc2=rc2 : Equiv rc2 rc2
  Equiv.force rc2=rc2 = eq-xmt SND (eq-chn rc2=rc2) rc2=rc2

  rc2=rc2-unfolded : Equiv rc2 rc2-unfolded
  Equiv.force rc2=rc2-unfolded = eq-xmt SND (eq-chn rc2=rc2) rc2=rc2

  weak-r2 : SType 0
  weak-r2 = rec (weaken'S 1 zero r2)

  weak-rc2 : SCType 0 zero
  weak-rc2 = weak-r2 , (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n))))

  r2-weak : SType n
  r2-weak = rec (xmt SND ((TChn (weaken'S 1 zero (rec (rec (xmt SND (TChn (var (suc zero))) (var (suc zero)))))))) ((weaken'S 1 zero (rec (rec (xmt SND (TChn (var (suc zero))) (var (suc zero))))))))

  rc2-weak : SCType 0 zero
  rc2-weak = r2-weak , con-rec (con-xmt (con-chn (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n))))) (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))))

  rc2=rc2a : Equiv rc2 rc2a
  Equiv.force rc2=rc2a = eq-xmt SND (eq-chn rc2=rc2a) rc2=rc2a

  rc2=xxxrc2b : Equiv' rc2 rc2-unf
  rc2=rc2b : Equiv' rc2 rc2b

  Equiv'.force rc2=xxxrc2b = eq-xmt SND (eq-chn rc2=xxxrc2b) rc2=rc2b
  Equiv'.force rc2=rc2b = eq-xmt SND (eq-chn rc2=rc2b) rc2=xxxrc2b

  rc2=rc2-weak : Equiv' rc2 rc2-weak
  Equiv'.force rc2=rc2-weak = eq-xmt SND (eq-chn {!rc2=rc2b!}) {!!}

  rc2=weak-rc2 : Equiv rc2 weak-rc2
  Equiv.force rc2=weak-rc2 = eq-xmt SND (eq-chn rc2=rc2a) rc2=rc2a

  r3 : SType 0
  r3 = rec (xmt SND (TChn (var zero)) (weaken'S 1 zero r1))

  rc3 : SCType 0 zero
  rc3 = r3 , con-rec (con-xmt (con-chn (con-var z≤n)) (con-rec (con-rec (con-xmt (con-chn (con-var z≤n)) (con-var z≤n)))))

  rc1=rc2 : Equiv rc1 rc2
  rc3=rc2 : Equiv rc3 rc2

  Equiv.force rc1=rc2 = eq-xmt SND (eq-chn rc1=rc2) rc3=rc2
  Equiv.force rc3=rc2 = eq-xmt SND (eq-chn rc3=rc2) rc1=rc2

-- end examples
----------------------------------------------------------------------

recrec : SType 2 → SType 0 × SType 0
recrec S = rec (rec S) , rec (subst-maxS (var zero) S)

recrec2 : SType 2 → SType 1
recrec2 S = rec S

conrr1 : {S : SType 2} → Contractive (suc (suc zero)) S → Contractive zero (rec (rec S))
conrr1 cs = con-rec (con-rec cs)

conrr2 : {S : SType 2} → Contractive (suc (suc zero)) S → Contractive (suc zero) (subst-maxS (var zero) S)
conrr2 cs = subst-contr-mS {!subst-contr-mS!} (con-var (s≤s z≤n))

sc-rec : SCType (suc n) (suc i) → SCType n i
sc-rec (S , cs) = (rec S , con-rec cs)

¬fromN≤x : (x : Fin n) → ¬ (fromℕ n ≤ inject₁ x)
¬fromN≤x {suc n} zero ()
¬fromN≤x {suc n} (suc x) (s≤s n≤x) = ¬fromN≤x x n≤x

μμ-lem-gen : {n : ℕ}
  → (S : SType (suc (suc n)))
  → Contractive (suc (suc (fromℕ n))) S
  → Contractive (suc (fromℕ n)) (subst-maxS (var (fromℕ n)) S)
μμ-lem-gen (xmt d T S) (con-xmt x cs) = con-xmt (subst-contr-mT x (con-var z≤n)) (subst-contr-mS cs (con-var z≤n))
μμ-lem-gen end con-end = con-end
μμ-lem-gen (rec S) (con-rec cs) = con-rec (μμ-lem-gen S cs)
μμ-lem-gen (var zero) (con-var ())
μμ-lem-gen (var (suc zero)) (con-var (s≤s ()))
μμ-lem-gen (var (suc (suc x))) (con-var (s≤s (s≤s x₁)))
  with ¬fromN≤x x x₁
μμ-lem-gen (var (suc (suc x))) (con-var (s≤s (s≤s x₁))) | ()

μμ-lemma : (S : SType 2) → Contractive (suc (suc zero)) S → Contractive (suc zero) (subst-maxS (var zero) S)
μμ-lemma S cs = μμ-lem-gen S cs

μμ-gen : (S : SType (suc (suc n))) (cs : Contractive (suc (suc (fromℕ n))) S) →
  Equiv' (sc-rec (sc-rec (S , {!!})))
         (sc-rec ((subst-maxS (var zero) S) , {!!}))
μμ-gen S cs = {!!}

μμ1 : (S : SType 2) (cs : Contractive (suc (suc zero)) S) →
  Equiv (sc-rec (sc-rec (S , cs)))
        (sc-rec ((subst-maxS (var zero) S) , μμ-lemma S cs))
Equiv.force (μμ1 (xmt d T S) (con-xmt x cs)) = {!!}
Equiv.force (μμ1 end con-end) = eq-end
Equiv.force (μμ1 (rec S) (con-rec cs)) = {!!}
Equiv.force (μμ1 (var x) (con-var x₁)) = {!!}

-- or μX μY S = μX [X/Y]S

μμ2 : (S : SType 2) (cs : Contractive (suc (suc zero)) S) →
  Equiv (sc-rec (sc-rec (S , cs)))
        let xxx = subst-maxS {!sc-rec!} (rec S) in (sc-rec ((subst-maxS (var zero) S) , (subst-contr-mS (c-weakenS₁ cs) (con-var {!!}))))
μμ2 S cs = {!!}

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
{-

In this file we apply the cubical machinery to Martin Hötzel-Escardó's
structure identity principle:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#sns

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.SIP where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv')
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma

open import Cubical.Foundations.Structure public

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ : Level
    S : Type ℓ₁ → Type ℓ₂

-- Note that for any equivalence (f , e) : X ≃ Y the type  ι (X , s) (Y , t) (f , e) need not to be
-- a proposition. Indeed this type should correspond to the ways s and t can be identified
-- as S-structures. This we call a standard notion of structure or SNS.
-- We will use a different definition, but the two definitions are interchangeable.
SNS : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
SNS {ℓ₁} S ι = ∀ {X : Type ℓ₁} (s t : S X) → ι (X , s) (X , t) (idEquiv X) ≃ (s ≡ t)

-- We introduce the notation for structure preserving equivalences a
-- bit differently, but this definition doesn't actually change from
-- Escardó's notes.
_≃[_]_ : (A : TypeWithStr ℓ₁ S) (ι : StrEquiv S ℓ₂) (B : TypeWithStr ℓ₁ S) → Type (ℓ-max ℓ₁ ℓ₂)
A ≃[ ι ] B = Σ[ e ∈ typ A ≃ typ B ] (ι A B e)

-- The following PathP version of SNS is a bit easier to work with
-- for the proof of the SIP
UnivalentStr : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃) → Type (ℓ-max (ℓ-max (ℓ-suc ℓ₁) ℓ₂) ℓ₃)
UnivalentStr {ℓ₁} S ι =
  {A B : TypeWithStr ℓ₁ S} (e : typ A ≃ typ B)
  → ι A B e ≃ PathP (λ i → S (ua e i)) (str A) (str B)

-- A quick sanity-check that our definition is interchangeable with
-- Escardó's. The direction SNS→UnivalentStr corresponds more or less
-- to a dependent EquivJ formulation of Escardó's homomorphism-lemma.
UnivalentStr→SNS : (S : Type ℓ₁ → Type ℓ₂) (ι : StrEquiv S ℓ₃)
  → UnivalentStr S ι → SNS S ι
UnivalentStr→SNS S ι θ {X = X} s t =
  ι (X , s) (X , t) (idEquiv X)
    ≃⟨ θ (idEquiv X) ⟩
  PathP (λ i → S (ua (idEquiv X) i)) s t
    ≃⟨ transportEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = X} j i)) s t) ⟩
  s ≡ t
  ■

SNS→UnivalentStr : (ι : StrEquiv S ℓ₃) → SNS S ι → UnivalentStr S ι
SNS→UnivalentStr {S = S} ι θ {A = A} {B = B} e = EquivJ P C e (str A) (str B)
  where
  Y = typ B

  P : (X : Type _) → X ≃ Y → Type _
  P X e' = (s : S X) (t : S Y) → ι (X , s) (Y , t) e' ≃ PathP (λ i → S (ua e' i)) s t

  C : (s t : S Y) → ι (Y , s) (Y , t) (idEquiv Y) ≃ PathP (λ i → S (ua (idEquiv Y) i)) s t
  C s t =
    ι (Y , s) (Y , t) (idEquiv Y)
      ≃⟨ θ s t ⟩
    s ≡ t
      ≃⟨ transportEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = Y} (~ j) i)) s t) ⟩
    PathP (λ i → S (ua (idEquiv Y) i)) s t
    ■

TransportStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S) → Type (ℓ-max (ℓ-suc ℓ) ℓ₁)
TransportStr {ℓ} {S = S} α =
  {X Y : Type ℓ} (e : X ≃ Y) (s : S X) → equivFun (α e) s ≡ subst S (ua e) s

TransportStr→UnivalentStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S)
  → TransportStr α → UnivalentStr S (EquivAction→StrEquiv α)
TransportStr→UnivalentStr {S = S} α τ {X , s} {Y , t} e =
  equivFun (α e) s ≡ t
    ≃⟨ pathToEquiv (cong (_≡ t) (τ e s)) ⟩
  subst S (ua e) s ≡ t
    ≃⟨ invEquiv (PathP≃Path _ _ _) ⟩
  PathP (λ i → S (ua e i)) s t
  ■

UnivalentStr→TransportStr : {S : Type ℓ → Type ℓ₁} (α : EquivAction S)
  → UnivalentStr S (EquivAction→StrEquiv α) → TransportStr α
UnivalentStr→TransportStr {S = S} α θ e s =
  invEq (θ e) (transport-filler (cong S (ua e)) s)

invTransportStr : {S : Type ℓ → Type ℓ₂} (α : EquivAction S) (τ : TransportStr α)
  {X Y : Type ℓ} (e : X ≃ Y) (t : S Y) → invEq (α e) t ≡ subst⁻ S (ua e) t
invTransportStr {S = S} α τ e t =
  sym (transport⁻Transport (cong S (ua e)) (invEq (α e) t))
  ∙∙ sym (cong (subst⁻ S (ua e)) (τ e (invEq (α e) t)))
  ∙∙ cong (subst⁻ S (ua e)) (retEq (α e) t)

--- We can now define an invertible function
---
---    sip : A ≃[ ι ] B → A ≡ B

module _ {S : Type ℓ₁ → Type ℓ₂} {ι : StrEquiv S ℓ₃}
  (θ : UnivalentStr S ι) (A B : TypeWithStr ℓ₁ S)
  where

  sip : A ≃[ ι ] B → A ≡ B
  sip (e , p) i = ua e i , θ e .fst p i

  SIP : A ≃[ ι ] B ≃ (A ≡ B)
  SIP =
    sip , isoToIsEquiv (compIso (Σ-cong-iso (invIso univalenceIso) (equivToIso ∘ θ)) ΣPathIsoPathΣ)

  sip⁻ : A ≡ B → A ≃[ ι ] B
  sip⁻ = invEq SIP

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:
-- Andreas, 2016-07-25, issue #2108
-- test case and report by Jesper

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.pos.occ:70 #-}

open import Agda.Primitive
open import Agda.Builtin.Equality

lone = lsuc lzero

record Level-zero-or-one : Set where
  field
    level : Level
    is-lower : (level ⊔ lone) ≡ lone

open Level-zero-or-one public

Coerce : ∀ {a} → a ≡ lone → Set₁
Coerce refl = Set

data Test : Set₁ where
  test : Coerce (is-lower _) → Test

-- WAS:
-- Meta variable here triggers internal error.

-- Should succeed with unsolved metas.


text:
module Base.Prelude where

open import Base.Prelude.Bool    public
open import Base.Prelude.Integer public
open import Base.Prelude.List    public
open import Base.Prelude.Pair    public
open import Base.Prelude.Unit    public

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
module Holes.Test.Limited where

open import Holes.Prelude hiding (_⊛_)
open import Holes.Util
open import Holes.Term
open import Holes.Cong.Limited

open import Agda.Builtin.Equality using (_≡_; refl)

module Contrived where
  infixl 5 _⊕_
  infixl 6 _⊛_
  infix 4 _≈_

  -- A type of expression trees for natural number calculations

  data Expr : Set where
    zero : Expr
    succ : Expr → Expr
    _⊕_ _⊛_ : Expr → Expr → Expr

  -- An unsophisticated 'equality' relation on the expression trees. Doesn't try
  -- to make the operations associative.

  data _≈_ : Expr → Expr → Set where
    zero-cong : zero ≈ zero
    succ-cong : ∀ {m n} → m ≈ n → succ m ≈ succ n
    ⊕-cong : ∀ {a a′ b b′} → a ≈ a′ → b ≈ b′ → a ⊕ b ≈ a′ ⊕ b′
    ⊛-cong : ∀ {a a′ b b′} → a ≈ a′ → b ≈ b′ → a ⊛ b ≈ a′ ⊛ b′

    ⊕-comm : ∀ a b → a ⊕ b ≈ b ⊕ a

  -- Some lemmas that are necessary to proceed

  ≈-refl : ∀ {n} → n ≈ n
  ≈-refl {zero} = zero-cong
  ≈-refl {succ n} = succ-cong ≈-refl
  ≈-refl {m ⊕ n} = ⊕-cong ≈-refl ≈-refl
  ≈-refl {m ⊛ n} = ⊛-cong ≈-refl ≈-refl

  {-
  Each congruence in the database must have a type with the same shape as the
  below, following these rules:

  - A congruence `c` is for a single _top-level_ function `f`
  - `c` may only be a congruence for _one_ of `f`'s arguments
  - Each explicit argument to `f` must be an explicit argument to `c`
  - The 'rewritten' version of the changing argument must follow as an implicit
    argument to `c`
  - The equation to do the local rewriting must be the next explicit argument
  -}

  open CongSplit _≈_ ≈-refl

  ⊕-cong₁ = two→one₁ ⊕-cong
  ⊕-cong₂ = two→one₂ ⊕-cong
  ⊛-cong₁ = two→one₁ ⊛-cong
  ⊛-cong₂ = two→one₂ ⊛-cong

  succ-cong′ : ∀ n {n′} → n ≈ n′ → succ n ≈ succ n′
  succ-cong′ _ = succ-cong

  {-
  Create the database of congruences.
  - This is a list of (Name × ArgPlace × Congruence) triples.
  - The `Name` is the (reflected) name of the function to which the congruence
    applies.
  - The `ArgPlace` is the index of the argument place that the congruence can
    rewrite at. Make sure you take into account implicit and instance arguments
    as well!
  - The `Congruence` is a reflected copy of the congruence function, of type `Term`
  -}

  database
    = (quote _⊕_ , 0 , quote ⊕-cong₁)
    ∷ (quote _⊕_ , 1 , quote ⊕-cong₂)
    ∷ (quote _⊛_ , 0 , quote ⊛-cong₁)
    ∷ (quote _⊛_ , 1 , quote ⊛-cong₂)
    ∷ (quote succ , 0 , quote succ-cong′)
    ∷ []

  open AutoCong database

  test1 : ∀ a b → succ ⌞ a ⊕ b ⌟ ≈ succ (b ⊕ a)
  test1 a b = cong! (⊕-comm a b)

  test2 : ∀ a b c → succ (⌞ a ⊕ b ⌟ ⊕ c) ≈ succ (b ⊕ a ⊕ c)
  test2 a b c = cong! (⊕-comm a b)

  test3 : ∀ a b c → succ (a ⊕ ⌞ b ⊕ c ⌟) ≈ succ (a ⊕ (c ⊕ b))
  test3 a b c = cong! (⊕-comm b c)

  -- We can use a proof obtained by pattern matching for `cong!`
  test5 : ∀ a b c → a ≈ b ⊕ c × b ≈ succ c → succ (⌞ b ⌟ ⊕ c ⊛ a) ≈ succ (succ c ⊕ c ⊛ a)
  test5 a b c (eq1 , eq2) = cong! eq2

  record ∃ {a p} {A : Set a} (P : A → Set p) : Set (a ⊔ p) where
    constructor _,_

    field
      evidence : A
      proof : P evidence

  -- We can use `cong!` to prove some part of the result even when it depends on
  -- other parts of the result
  test6 : ∀ a b c → b ⊕ c ≈ a × b ≈ succ c → ∃ λ x → succ (⌞ b ⊕ x ⌟ ⊕ a) ≈ succ (a ⊕ a)
  test6 a b c (eq1 , eq2) = c , cong! eq1

  -- Deep nesting
  test7 : ∀ a b c
    → succ (a ⊕ succ (b ⊕ succ (c ⊕ succ (succ ⌞ b ⊕ c ⌟ ⊕ (a ⊕ b)))))
    ≈ succ (a ⊕ succ (b ⊕ succ (c ⊕ succ (succ ⌞ c ⊕ b ⌟ ⊕ (a ⊕ b)))))
  test7 _ b c = cong! (⊕-comm b c)

module Propositional (+-comm : ∀ a b → a + b ≡ b + a) where
  +-cong₁ : ∀ a b {a′} → a ≡ a′ → a + b ≡ a′ + b
  +-cong₁ _ _ refl = refl

  +-cong₂ : ∀ a b {b′} → b ≡ b′ → a + b ≡ a + b′
  +-cong₂ _ _ refl = refl

  suc-cong : ∀ n {n′} → n ≡ n′ → suc n ≡ suc n′
  suc-cong _ refl = refl

  database
    = (quote _+_ , 0 , quote +-cong₁)
    ∷ (quote _+_ , 1 , quote +-cong₂)
    ∷ (quote suc , 0 , quote suc-cong)
    ∷ []

  open AutoCong database

  test1 : ∀ a b → suc ⌞ a + b ⌟ ≡ suc (b + a)
  test1 a b = cong! (+-comm a b)

  test2 : ∀ a b c → suc (⌞ a + b ⌟ + c) ≡ suc (b + a + c)
  test2 a b c = cong! (+-comm a b)

  test3 : ∀ a b c → suc (a + ⌞ b + c ⌟) ≡ suc (a + (c + b))
  test3 a b c = cong! (+-comm b c)

  test4 : ∀ a b c a′ → a ≡ a′ → suc (⌞ a ⌟ + b + c) ≡ suc (a′ + b + c)
  test4 _ _ _ _ eq = cong! eq


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Symmetry {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening hiding (wk)
open import Definition.Typed.Properties
open import Definition.Typed.EqualityRelation
open import Definition.LogicalRelation
open import Definition.LogicalRelation.ShapeView
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.Properties.Escape
open import Definition.LogicalRelation.Properties.Conversion

open import Tools.Product
open import Tools.Empty
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

mutual
  -- Helper function for symmetry of type equality using shape views.
  symEqT : ∀ {Γ A B r l l′} {[A] : Γ ⊩⟨ l ⟩ A ^ r} {[B] : Γ ⊩⟨ l′ ⟩ B ^ r}
         → ShapeView Γ l l′ A B r r [A] [B]
         → Γ ⊩⟨ l  ⟩ A ≡ B ^ r / [A]
         → Γ ⊩⟨ l′ ⟩ B ≡ A ^ r / [B]
  symEqT (ℕᵥ D D′) A≡B = red D
  symEqT (Emptyᵥ D D′) A≡B = red D
  symEqT (ne (ne K D neK K≡K) (ne K₁ D₁ neK₁ K≡K₁)) (ne₌ M D′ neM K≡M)
         rewrite whrDet* (red D′ , ne neM) (red D₁ , ne neK₁) =
    ne₌ _ D neK
        (~-sym K≡M)
  symEqT {Γ = Γ} {r = [ r , ι lΠ ] } (Πᵥ (Πᵣ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                     (Πᵣ rF₁ lF₁ lG₁ _ _ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
         (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let ΠF₁G₁≡ΠF′G′   = whrDet* (red D₁ , Πₙ) (D′ , Πₙ)
        F₁≡F′ , rF₁≡rF′ , lF₁≡lF′ , G₁≡G′ , lG₁≡lG′ , lΠ≡lΠ₁ = Π-PE-injectivity ΠF₁G₁≡ΠF′G′
        [F₁≡F] : ∀ {Δ} {ρ} [ρ] ⊢Δ → _
        [F₁≡F] {Δ} {ρ} [ρ] ⊢Δ =
          let ρF′≡ρF₁ ρ = PE.cong (wk ρ) (PE.sym F₁≡F′)
              [ρF′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → Δ ⊩⟨ _ ⟩ wk ρ x ^ _) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
          in  irrelevanceEq′ {Δ} (ρF′≡ρF₁ ρ) PE.refl PE.refl
                             ([ρF′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ)
                             (symEq′ (PE.sym rF₁≡rF′) (PE.cong ι (PE.sym lF₁≡lF′)) ([F] [ρ] ⊢Δ) ([ρF′] [ρ] ⊢Δ)
                                    ([F≡F′] [ρ] ⊢Δ))
    in  Π₌ _ _ (red (PE.subst₃ _ (PE.sym rF₁≡rF′) (PE.sym lF₁≡lF′) (PE.sym lG₁≡lG′) D))
           (PE.subst₃ _ (PE.sym rF₁≡rF′) (PE.sym lF₁≡lF′) (PE.sym lG₁≡lG′) (≅-sym (PE.subst (λ x → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° lΠ ≅ x ^ [ r , ι lΠ ]) (PE.sym ΠF₁G₁≡ΠF′G′) A≡B)))
           [F₁≡F]
           (λ {ρ} [ρ] ⊢Δ [a] →
               let ρG′a≡ρG₁′a = PE.cong (λ x → wk (lift ρ) x [ _ ]) (PE.sym G₁≡G′)
                   [ρG′a] = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk (lift ρ) x [ _ ] ^ _) G₁≡G′
                                     ([G]₁ [ρ] ⊢Δ [a])
                   [a]₁ = convTerm₁′ rF₁≡rF′ (PE.cong ι lF₁≡lF′) ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) ([F₁≡F] [ρ] ⊢Δ) [a]
               in  irrelevanceEq′ ρG′a≡ρG₁′a PE.refl PE.refl
                                  [ρG′a]
                                  ([G]₁ [ρ] ⊢Δ [a]) (symEq′ PE.refl (PE.sym (PE.cong ι lG₁≡lG′)) ([G] [ρ] ⊢Δ [a]₁) [ρG′a] ([G≡G′] [ρ] ⊢Δ [a]₁)))
  symEqT {Γ = Γ} {r = r} (∃ᵥ (∃ᵣ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                     (∃ᵣ F₁ G₁ D₁ ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁))
         (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
    let ∃F₁G₁≡∃F′G′   = whrDet* (red D₁ , ∃ₙ) (D′ , ∃ₙ)
        F₁≡F′ , G₁≡G′ = ∃-PE-injectivity ∃F₁G₁≡∃F′G′
        [F₁≡F] : ∀ {Δ} {ρ} [ρ] ⊢Δ → _
        [F₁≡F] {Δ} {ρ} [ρ] ⊢Δ =
          let ρF′≡ρF₁ ρ = PE.cong (wk ρ) (PE.sym F₁≡F′)
              [ρF′] {ρ} [ρ] ⊢Δ = PE.subst (λ x → Δ ⊩⟨ _ ⟩ wk ρ x ^ _) F₁≡F′ ([F]₁ [ρ] ⊢Δ)
          in  irrelevanceEq′ {Δ} (ρF′≡ρF₁ ρ) PE.refl PE.refl
                             ([ρF′] [ρ] ⊢Δ) ([F]₁ [ρ] ⊢Δ)
                             (symEq′ PE.refl PE.refl ([F] [ρ] ⊢Δ) ([ρF′] [ρ] ⊢Δ)
                                    ([F≡F′] [ρ] ⊢Δ))
    in  ∃₌ _ _ (red D) (≅-sym (PE.subst (λ x → Γ ⊢ ∃ F ▹ G ≅ x ^ r) (PE.sym ∃F₁G₁≡∃F′G′) A≡B))
          [F₁≡F]
          (λ {ρ} [ρ] ⊢Δ [a] →
               let ρG′a≡ρG₁′a = PE.cong (λ x → wk (lift ρ) x [ _ ]) (PE.sym G₁≡G′)
                   [ρG′a] = PE.subst (λ x → _ ⊩⟨ _ ⟩ wk (lift ρ) x [ _ ] ^ _) G₁≡G′
                                     ([G]₁ [ρ] ⊢Δ [a])
                   [a]₁ = convTerm₁′ PE.refl PE.refl ([F]₁ [ρ] ⊢Δ) ([F] [ρ] ⊢Δ) ([F₁≡F] [ρ] ⊢Δ) [a]
               in  irrelevanceEq′ ρG′a≡ρG₁′a PE.refl PE.refl
                                  [ρG′a]
                                  ([G]₁ [ρ] ⊢Δ [a])
                                  (symEq ([G] [ρ] ⊢Δ [a]₁) [ρG′a]
                                         ([G≡G′] [ρ] ⊢Δ [a]₁)))
  symEqT (Uᵥ (Uᵣ r l l< el d) (Uᵣ r' l' l<' PE.refl d')) A≡B =
    let U≡U   = whrDet* (A≡B , Uₙ) (red d' , Uₙ)
        r≡r , l≡l = Univ-PE-injectivity (PE.sym U≡U)
    in PE.subst _ (PE.sym l≡l) (PE.subst _ (PE.sym r≡r) (red d))
  symEqT (emb⁰¹ X) A≡B = symEqT X A≡B
  symEqT (emb¹⁰ X) A≡B = symEqT X A≡B
  symEqT (emb¹∞ X) A≡B = symEqT X A≡B
  symEqT (emb∞¹ X) A≡B = symEqT X A≡B

  -- Symmetry of type equality.
  symEq : ∀ {Γ A B r l l′} ([A] : Γ ⊩⟨ l ⟩ A ^ r) ([B] : Γ ⊩⟨ l′ ⟩ B ^ r)
        → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
        → Γ ⊩⟨ l′ ⟩ B ≡ A ^ r / [B]
  symEq [A] [B] A≡B = symEqT (goodCases [A] [B] A≡B) A≡B

  -- same but with PE
  symEq′ : ∀ {Γ A B r r' l l′ ll ll'} (eq : r PE.≡ r') (eq' : ll PE.≡ ll')
             ([A] : Γ ⊩⟨ l ⟩ A ^ [ r , ll ]) ([B] : Γ ⊩⟨ l′ ⟩ B ^ [ r' , ll' ])
        → Γ ⊩⟨ l ⟩ A ≡ B ^ [ r , ll ] / [A]
        → Γ ⊩⟨ l′ ⟩ B ≡ A ^ [ r' , ll' ] / [B]
  symEq′ PE.refl PE.refl [A] [B] A≡B = symEq [A] [B] A≡B

symNeutralTerm : ∀ {t u A r Γ}
               → Γ ⊩neNf t ≡ u ∷ A ^ r
               → Γ ⊩neNf u ≡ t ∷ A ^ r
symNeutralTerm {r = [ ! , ll ]} (neNfₜ₌ neK neM k≡m) = neNfₜ₌ neM neK (~-sym k≡m)
symNeutralTerm {r = [ % , ll ]} (neNfₜ₌ neK neM k≡m) = neNfₜ₌ neM neK (~-sym k≡m)

symNatural-prop : ∀ {Γ k k′}
                → [Natural]-prop Γ k k′
                → [Natural]-prop Γ k′ k
symNatural-prop (sucᵣ (ℕₜ₌ k k′ d d′ t≡u prop)) =
  sucᵣ (ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop))
symNatural-prop zeroᵣ = zeroᵣ
symNatural-prop (ne prop) = ne (symNeutralTerm prop)

symEmpty-prop : ∀ {Γ k k′ l}
                → [Empty]-prop Γ k k′ l
                → [Empty]-prop Γ k′ k l
symEmpty-prop (ne t u ) = ne u t

symEqTerm⁰ : ∀ {Γ A t u r} ([A] : Γ ⊩⟨ ι ⁰ ⟩ A ^ r)
          → Γ ⊩⟨ ι ⁰ ⟩ t ≡ u ∷ A ^ r / [A]
          → Γ ⊩⟨ ι ⁰ ⟩ u ≡ t ∷ A ^ r / [A]
symEqTerm⁰ (ℕᵣ D) (ℕₜ₌ k k′ d d′ t≡u prop) =
  ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop)
symEqTerm⁰ (Emptyᵣ D) (Emptyₜ₌ prop) = Emptyₜ₌ (symEmpty-prop prop)
symEqTerm⁰ {r = [ ! , ll ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ m k d′ d (symNeutralTerm nf)
symEqTerm⁰ {r = [ % , ll ]} (ne′ K D neK K≡K) (neₜ₌ d d′) = neₜ₌ d′ d
symEqTerm⁰ {r = [ ! , ll ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  Πₜ₌ g f d′ d funcG funcF (≅ₜ-sym f≡g) [g] [f]
      (λ ρ ⊢Δ [a] → symEqTerm⁰ ([G] ρ ⊢Δ [a]) ([f≡g] ρ ⊢Δ [a]))
symEqTerm⁰ {r = [ % , ll ]} (Πᵣ′ rF lF _ _ F lG G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d
symEqTerm⁰ {r = [ % , ll ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d

symEqTerm¹ : ∀ {Γ A t u r} ([A] : Γ ⊩⟨ ι ¹ ⟩ A ^ r)
          → Γ ⊩⟨ ι ¹ ⟩ t ≡ u ∷ A ^ r / [A]
          → Γ ⊩⟨ ι ¹ ⟩ u ≡ t ∷ A ^ r / [A]
symEqTerm¹ {Γ} {A} {t} {u} (Uᵣ (Uᵣ r ⁰ l< el D)) (Uₜ₌ [A] [B] A≡B [A≡B]) =
  let
    [B≡A] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      symEq (LogRel._⊩¹U_∷_^_/_.[t] [A] [ρ] ⊢Δ) (LogRel._⊩¹U_∷_^_/_.[t] [B] [ρ] ⊢Δ) ([A≡B] [ρ] ⊢Δ)
    u_to_t : ∀ {ρ Δ a} → ([ρ] : ρ ∷ Δ ⊆ Γ) → (⊢Δ : ⊢ Δ)
      → ([a] : Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ u ^ [ r , ι ⁰ ] / (LogRel._⊩¹U_∷_^_/_.[t] [B] [ρ] ⊢Δ))
      → Δ ⊩⟨ ι ⁰ ⟩ a ∷ wk ρ t ^ [ r , ι ⁰ ] / (LogRel._⊩¹U_∷_^_/_.[t] [A] [ρ] ⊢Δ)
    u_to_t = λ [ρ] ⊢Δ [a] → convTerm₂ (LogRel._⊩¹U_∷_^_/_.[t] [A] [ρ] ⊢Δ) (LogRel._⊩¹U_∷_^_/_.[t] [B] [ρ] ⊢Δ) ([A≡B] [ρ] ⊢Δ) [a]
  in
  Uₜ₌ [B] [A] (≅ₜ-sym A≡B) [B≡A]
symEqTerm¹ (ℕᵣ D) (ℕₜ₌ k k′ d d′ t≡u prop) =
  ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop)
symEqTerm¹ (Emptyᵣ D) (Emptyₜ₌ prop) = Emptyₜ₌ (symEmpty-prop prop)
symEqTerm¹ {r = [ ! , ll ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ m k d′ d (symNeutralTerm nf)
symEqTerm¹ {r = [ % , ll ]} (ne′ K D neK K≡K) (neₜ₌ d d′) = neₜ₌ d′ d
symEqTerm¹ {r = [ ! , ll ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  Πₜ₌ g f d′ d funcG funcF (≅ₜ-sym f≡g) [g] [f]
      (λ ρ ⊢Δ [a] → symEqTerm¹ ([G] ρ ⊢Δ [a]) ([f≡g] ρ ⊢Δ [a]))
symEqTerm¹ {r = [ % , ll ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d
symEqTerm¹ {r = [ % , ll ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d
symEqTerm¹ (emb <l x) t≡u = symEqTerm⁰ x t≡u

-- Symmetry of term equality.
symEqTerm∞ : ∀ {Γ A t u r} ([A] : Γ ⊩⟨ ∞ ⟩ A ^ r)
          → Γ ⊩⟨ ∞ ⟩ t ≡ u ∷ A ^ r / [A]
          → Γ ⊩⟨ ∞ ⟩ u ≡ t ∷ A ^ r / [A]
symEqTerm∞ {Γ} {A} {t} {u} (Uᵣ (Uᵣ r ⁰ l< el D)) (Uₜ₌ [A] [B] A≡B [A≡B]) =
  let
    [B≡A] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      symEq (LogRel._⊩¹U_∷_^_/_.[t] [A] [ρ] ⊢Δ) (LogRel._⊩¹U_∷_^_/_.[t] [B] [ρ] ⊢Δ) ([A≡B] [ρ] ⊢Δ)
  in
  Uₜ₌ [B] [A] (≅ₜ-sym A≡B) [B≡A]
symEqTerm∞ {Γ} {A} {t} {u} (Uᵣ (Uᵣ r ¹ l< el D)) (Uₜ₌ [A] [B] A≡B [A≡B]) =
  let
    [B≡A] = λ {ρ} {Δ} ([ρ] : ρ ∷ Δ ⊆ Γ) ⊢Δ →
      symEq (LogRel._⊩¹U_∷_^_/_.[t] [A] [ρ] ⊢Δ) (LogRel._⊩¹U_∷_^_/_.[t] [B] [ρ] ⊢Δ) ([A≡B] [ρ] ⊢Δ)
  in
  Uₜ₌ [B] [A] (≅ₜ-sym A≡B) [B≡A]
symEqTerm∞ (ℕᵣ D) (ℕₜ₌ k k′ d d′ t≡u prop) =
  ℕₜ₌ k′ k d′ d (≅ₜ-sym t≡u) (symNatural-prop prop)
symEqTerm∞ (Emptyᵣ D) (Emptyₜ₌ prop) = Emptyₜ₌ (symEmpty-prop prop)
symEqTerm∞ {r = [ ! , ll ]} (ne′ K D neK K≡K) (neₜ₌ k m d d′ nf) =
  neₜ₌ m k d′ d (symNeutralTerm nf)
symEqTerm∞ {r = [ % , ll ]} (ne′ K D neK K≡K) (neₜ₌ d d′) = neₜ₌ d′ d
symEqTerm∞ {r = [ ! , ll ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  Πₜ₌ g f d′ d funcG funcF (≅ₜ-sym f≡g) [g] [f]
      (λ ρ ⊢Δ [a] → symEqTerm∞ ([G] ρ ⊢Δ [a]) ([f≡g] ρ ⊢Δ [a]))
symEqTerm∞ {r = [ % , ll ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d
symEqTerm∞ {r = [ % , ll ]} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
          (d , d′) = d′ , d
symEqTerm∞ (emb <l x) t≡u = symEqTerm¹ x t≡u

symEqTerm : ∀ {l Γ A t u r} ([A] : Γ ⊩⟨ l ⟩ A ^ r)
          → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / [A]
          → Γ ⊩⟨ l ⟩ u ≡ t ∷ A ^ r / [A]
symEqTerm {l = ι ⁰} = symEqTerm⁰
symEqTerm {l = ι ¹} = symEqTerm¹
symEqTerm {l = ∞} = symEqTerm∞

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Categories.Functor.Bifunctor.Properties where

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

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Bifunctor
import Categories.Morphism.Reasoning as MR

private
  variable
    o ℓ e : Level
    C D E : Category o ℓ e

module _ (F : Bifunctor C D E) where
  private
    module C = Category C
    module D = Category D
    module E = Category E

    variable
      A B : C.Obj
      X Y : D.Obj
      f h j : A C.⇒ B
      g i k : X D.⇒ Y

  open E
  open HomReasoning
  open Functor F

  [_]-commute : F₁ (C.id , g) ∘ F₁ (f , D.id) ≈ F₁ (f , D.id) ∘ F₁ (C.id , g)
  [_]-commute {g = g} {f = f} = begin
    F₁ (C.id , g) ∘ F₁ (f , D.id) ≈˘⟨ homomorphism ⟩
    F₁ (C.id C.∘ f , g D.∘ D.id)  ≈⟨ F-resp-≈ (MR.id-comm-sym C , MR.id-comm D) ⟩
    F₁ (f C.∘ C.id , D.id D.∘ g)  ≈⟨ homomorphism ⟩
    F₁ (f , D.id) ∘ F₁ (C.id , g) ∎

  [_]-decompose₁ : F₁ (f , g) ≈ F₁ (f , D.id) ∘ F₁ (C.id , g)
  [_]-decompose₁ {f = f} {g = g} = begin
    F₁ (f , g)                    ≈˘⟨ F-resp-≈ (C.identityʳ , D.identityˡ) ⟩
    F₁ (f C.∘ C.id , D.id D.∘ g)  ≈⟨ homomorphism ⟩
    F₁ (f , D.id) ∘ F₁ (C.id , g) ∎

  [_]-decompose₂ : F₁ (f , g) ≈ F₁ (C.id , g) ∘ F₁ (f , D.id)
  [_]-decompose₂ {f = f} {g = g} = begin
    F₁ (f , g)                    ≈˘⟨ F-resp-≈ (C.identityˡ , D.identityʳ) ⟩
    F₁ (C.id C.∘ f , g D.∘ D.id)  ≈⟨ homomorphism ⟩
    F₁ (C.id , g) ∘ F₁ (f , D.id) ∎

  [_]-merge : f C.∘ h C.≈ j → g D.∘ i D.≈ k →  F₁ (f , g) ∘ F₁ (h , i) ≈ F₁ (j , k)
  [_]-merge {f = f} {h = h} {j = j} {g = g} {i = i} {k = k} eq eq′ = begin
    F₁ (f , g) ∘ F₁ (h , i) ≈˘⟨ homomorphism ⟩
    F₁ (f C.∘ h , g D.∘ i)  ≈⟨ F-resp-≈ (eq , eq′) ⟩
    F₁ (j , k)              ∎

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Categories.Category
open import Categories.Monad

module Categories.Adjoint.Construction.Kleisli {o ℓ e} {C : Category o ℓ e} (M : Monad C) where

open import Categories.Category.Construction.Kleisli
open import Categories.Adjoint
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Monad M
  open M.F
  open C
  open HomReasoning

Forgetful : Functor (Kleisli M) C
Forgetful = record
  { F₀           = λ X → F₀ X
  ; F₁           = λ f → M.μ.η _ ∘ F₁ f
  ; identity     = M.identityˡ
  ; homomorphism = λ {X Y Z} {f g} → begin
    M.μ.η Z ∘ F₁ ((M.μ.η Z ∘ F₁ g) ∘ f)         ≈⟨ refl⟩∘⟨ homomorphism ⟩
    M.μ.η Z ∘ F₁ (M.μ.η Z ∘ F₁ g) ∘ F₁ f        ≈⟨ refl⟩∘⟨ homomorphism ⟩∘⟨refl ⟩
    M.μ.η Z ∘ (F₁ (M.μ.η Z) ∘ F₁ (F₁ g)) ∘ F₁ f ≈⟨ pull-first M.assoc ⟩
    (M.μ.η Z ∘ M.μ.η (F₀ Z)) ∘ F₁ (F₁ g) ∘ F₁ f ≈⟨ center (M.μ.commute g) ⟩
    M.μ.η Z ∘ (F₁ g ∘ M.μ.η Y) ∘ F₁ f           ≈⟨ pull-first refl ⟩
    (M.μ.η Z ∘ F₁ g) ∘ M.μ.η Y ∘ F₁ f           ∎
  ; F-resp-≈     = λ eq → ∘-resp-≈ʳ (F-resp-≈ eq)
  }

Free : Functor C (Kleisli M)
Free = record
  { F₀           = λ X → X
  ; F₁           = λ f → M.η.η _ ∘ f
  ; identity     = identityʳ
  ; homomorphism = λ {X Y Z} {f g} → begin
    M.η.η Z ∘ g ∘ f                                 ≈⟨ sym-assoc ○ ⟺ identityˡ ⟩
    C.id ∘ (M.η.η Z ∘ g) ∘ f                        ≈˘⟨ pull-first M.identityˡ ⟩
    M.μ.η Z ∘ (F₁ (M.η.η Z) ∘ M.η.η Z ∘ g) ∘ f      ≈⟨ refl⟩∘⟨ pushʳ (M.η.commute g) ⟩∘⟨refl ⟩
    M.μ.η Z ∘ ((F₁ (M.η.η Z) ∘ F₁ g) ∘ M.η.η Y) ∘ f ≈˘⟨ center (∘-resp-≈ˡ homomorphism) ⟩
    (M.μ.η Z ∘ F₁ (M.η.η Z ∘ g)) ∘ M.η.η Y ∘ f      ∎
  ; F-resp-≈     = ∘-resp-≈ʳ
  }

FF≃F : Forgetful ∘F Free ≃ M.F
FF≃F = record
  { F⇒G = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      F₁ C.id ∘ M.μ.η Y ∘ F₁ (M.η.η Y ∘ f)      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ homomorphism ⟩
      F₁ C.id ∘ M.μ.η Y ∘ F₁ (M.η.η Y) ∘ F₁ f   ≈⟨ refl⟩∘⟨ cancelˡ M.identityˡ ⟩
      F₁ C.id ∘ F₁ f                            ≈⟨ [ M.F ]-resp-square id-comm-sym ⟩
      F₁ f ∘ F₁ C.id                            ∎
    }
  ; F⇐G = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      F₁ C.id ∘ F₁ f                            ≈⟨ [ M.F ]-resp-square id-comm-sym ⟩
      F₁ f ∘ F₁ C.id                            ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
      (M.μ.η Y ∘ F₁ (M.η.η Y) ∘ F₁ f) ∘ F₁ C.id ≈˘⟨ ∘-resp-≈ʳ homomorphism ⟩∘⟨refl ⟩
      (M.μ.η Y ∘ F₁ (M.η.η Y ∘ f)) ∘ F₁ C.id    ∎
    }
  ; iso = λ X → record
    { isoˡ = elimˡ identity ○ identity
    ; isoʳ = elimˡ identity ○ identity
    }
  }

Free⊣Forgetful : Free ⊣ Forgetful
Free⊣Forgetful = record
  { unit   = ntHelper record
    { η       = M.η.η
    ; commute = λ {X Y} f → begin
      M.η.η Y ∘ f                               ≈⟨ M.η.commute f ⟩
      F₁ f ∘ M.η.η X                            ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
      (M.μ.η Y ∘ F₁ (M.η.η Y) ∘ F₁ f) ∘ M.η.η X ≈˘⟨ ∘-resp-≈ʳ homomorphism ⟩∘⟨refl ⟩
      (M.μ.η Y ∘ F₁ (M.η.η Y ∘ f)) ∘ M.η.η X    ∎
    }
  ; counit = ntHelper record
    { η       = λ X → F₁ C.id
    ; commute = λ {X Y} f → begin
      (M.μ.η Y ∘ F₁ (F₁ C.id)) ∘ M.η.η (F₀ Y) ∘ M.μ.η Y ∘ F₁ f
        ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
      M.μ.η Y ∘ M.η.η (F₀ Y) ∘ M.μ.η Y ∘ F₁ f
        ≈⟨ cancelˡ M.identityʳ ⟩
      M.μ.η Y ∘ F₁ f
        ≈⟨ introʳ identity ⟩
      (M.μ.η Y ∘ F₁ f) ∘ F₁ C.id
        ∎
    }
  ; zig    = λ {A} → begin
    (M.μ.η A ∘ F₁ (F₁ C.id)) ∘ M.η.η (F₀ A) ∘ M.η.η A ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
    M.μ.η A ∘ M.η.η (F₀ A) ∘ M.η.η A                  ≈⟨ cancelˡ M.identityʳ ⟩
    M.η.η A                                           ∎
  ; zag    = λ {B} → begin
    (M.μ.η B ∘ F₁ (F₁ C.id)) ∘ M.η.η (F₀ B)           ≈⟨ elimʳ (F-resp-≈ identity ○ identity) ⟩∘⟨refl ⟩
    M.μ.η B ∘ M.η.η (F₀ B)                            ≈⟨ M.identityʳ ⟩
    C.id                                              ∎
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories