text:
{-# OPTIONS --without-K #-}
module Model.Type.Core where

open import Cats.Category
open import Relation.Binary using (IsEquivalence)

open import Model.RGraph as RG using (RGraph)
open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.HoTT.Homotopy
open import Util.HoTT.Univalence
open import Util.Prelude hiding (id) renaming (_∘_ to _∘F_)
open import Util.Relation.Binary.LogicalEquivalence using
  ( _↔_ ; forth ; back ; ↔-reflexive )
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; Σ-≡⁻ ; cast ; subst-subst ; subst-sym-subst ; subst-subst-sym )

open Category._≅_ public
open RG._⇒_

infixr 0 _⇒_
infix  4 _≈_ _≈⟦Type⟧_
infixr 9 _∘_

private
  variable Δ Γ Ψ : RGraph

-- This is an RGraph-indexed family of RGraphs.
record ⟦Type⟧ (Δ : RGraph) : Set₁ where
  no-eta-equality
  field
    ObjHSet : Δ .RG.Obj → HSet 0ℓ

  private
    module M₀ δ = HLevel (ObjHSet δ)
    module M₁ {δ} = HLevel (ObjHSet δ)

  open M₀ public using () renaming
    ( type to Obj )
  open M₁ public using () renaming
    ( level to Obj-IsSet )

  field
    eqHProp : ∀ {δ δ′} → Δ .RG.eq δ δ′ → Obj δ → Obj δ′ → HProp 0ℓ

  private
    module M₂ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) x y   = HLevel (eqHProp δ≈δ′ x y)
    module M₃ {δ δ′} {δ≈δ′ : Δ .RG.eq δ δ′} {x y} = HLevel (eqHProp δ≈δ′ x y)

  open M₂ public using () renaming
    ( type to eq )
  open M₃ public using () renaming
    ( level to eq-IsProp )

  field
    eq-refl : ∀ {δ} (x : Obj δ) → eq (Δ .RG.eq-refl δ) x x

open ⟦Type⟧ public

private
  variable T U V W : ⟦Type⟧ Δ

open RGraph

transportEq : ∀ (T : ⟦Type⟧ Δ) {δ γ} {δ≈γ₀ δ≈γ₁ : Δ .eq δ γ} {x y}
  → T .eq δ≈γ₀ x y → T .eq δ≈γ₁ x y
transportEq {Δ} T = subst (λ p → T .eq p _ _) (Δ .eq-IsProp _ _)

transportObj : ∀ (T : ⟦Type⟧ Δ) {δ γ}
  → δ ≡ γ
  → T .Obj δ
  → T .Obj γ
transportObj T = subst (T .Obj)

abstract
  transportObj-resp : ∀ (T : ⟦Type⟧ Δ) {δ γ}
    → (δ≡γ₀ δ≡γ₁ : δ ≡ γ)
    → ∀ {x y}
    → x ≡ y
    → transportObj T δ≡γ₀ x ≡ transportObj T δ≡γ₁ y
  transportObj-resp {Δ} T refl δ≡γ₁ x≡y
    rewrite Δ .Obj-IsSet δ≡γ₁ refl = x≡y

transportObj-resp-eq : ∀ (T : ⟦Type⟧ Δ) {δ₀ γ₀ δ₁ γ₁}
  → (δ₀≡γ₀ : δ₀ ≡ γ₀) (δ₁≡γ₁ : δ₁ ≡ γ₁)
  → ∀ {x y} {δ₀≈δ₁ : Δ .eq δ₀ δ₁} {γ₀≈γ₁ : Δ .eq γ₀ γ₁}
  → T .eq δ₀≈δ₁ x y
  → T .eq γ₀≈γ₁ (transportObj T δ₀≡γ₀ x) (transportObj T δ₁≡γ₁ y)
transportObj-resp-eq {Δ} T refl refl {δ₀≈δ₁ = δ₀≈δ₁} {γ₀≈γ₁} x≈y
  = transportEq T x≈y

abstract
  transportObj∘transportObj : ∀ (T : ⟦Type⟧ Δ) {δ δ′ δ″}
    → (p : δ ≡ δ′) (q : δ′ ≡ δ″) {x : T .Obj δ}
    → transportObj T q (transportObj T p x) ≡ transportObj T (trans p q) x
  transportObj∘transportObj T p q = subst-subst p

  transportObj-refl : ∀ (T : ⟦Type⟧ Δ) {δ}
    → (p : δ ≡ δ) {x : T .Obj δ}
    → transportObj T p x ≡ x
  transportObj-refl {Δ} T p rewrite Δ .Obj-IsSet p refl = refl

record _⇒_ (T U : ⟦Type⟧ Δ) : Set where
  no-eta-equality
  field
    fobj : ∀ {δ} → Obj T δ → Obj U δ
    feq : ∀ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) {x y}
      → eq T δ≈δ′ x y
      → eq U δ≈δ′ (fobj x) (fobj y)

open _⇒_ public

record _≈_ (f g : T ⇒ U) : Set where
  no-eta-equality
  constructor ≈⁺
  field
    ≈⁻ : ∀ δ (x : Obj T δ) → f .fobj x ≡ g .fobj x

open _≈_ public

≈-isEquivalence : (T U : ⟦Type⟧ Δ) → IsEquivalence (_≈_ {T = T} {U})
≈-isEquivalence T U = record
  { refl = ≈⁺ λ γ x → refl
  ; sym = λ f≈g → ≈⁺ λ γ x → sym (f≈g .≈⁻ γ x)
  ; trans = λ f≈g g≈h → ≈⁺ λ γ x → trans (f≈g .≈⁻ γ x) (g≈h .≈⁻ γ x)
  }

⇒Canon : (T U : ⟦Type⟧ Δ) → Set
⇒Canon {Δ} T U
  = Σ[ fobj ∈ (∀ {δ} → T .Obj δ → U .Obj δ) ]
      (∀ {δ δ′} (δ≈δ′ : Δ .RG.eq δ δ′) {x y}
        → T .eq δ≈δ′ x y → U .eq δ≈δ′ (fobj x) (fobj y))

⇒≅⇒Canon : (T ⇒ U) ≅ ⇒Canon T U
⇒≅⇒Canon = record
  { forth = λ f → f .fobj , f .feq
  ; isIso = record
    { back = λ f → record { fobj = f .proj₁ ; feq = f .proj₂ }
    ; back∘forth = λ where
        record { fobj = fo ; feq = fe } → refl
    ; forth∘back = λ x → refl
    }
  }

⇒Canon-IsSet : (T U : ⟦Type⟧ Δ) → IsSet (⇒Canon T U)
⇒Canon-IsSet T U = Σ-IsSet
  (∀∙-IsSet λ δ → →-IsSet (U .Obj-IsSet))
  (λ _ → ∀∙-IsSet λ δ → ∀∙-IsSet λ δ′ → ∀-IsSet λ δ≈δ′ → ∀∙-IsSet λ x
    → ∀∙-IsSet λ y → →-IsSet (IsProp→IsSet (U .eq-IsProp)))

⇒-IsSet : IsSet (T ⇒ U)
⇒-IsSet {T = T} {U} = ≅-pres-IsOfHLevel 2 (≅-sym ⇒≅⇒Canon) (⇒Canon-IsSet T U)

≈→≡Canon : {f g : T ⇒ U}
  → f ≈ g → ⇒≅⇒Canon .forth f ≡ ⇒≅⇒Canon .forth g
≈→≡Canon {U = U} f≈g = Σ-≡⁺
  ( (funext∙ (funext (λ x → f≈g .≈⁻ _ x)))
  , funext∙ (funext∙ (funext λ a → funext∙ (funext∙
      (funext λ eq → U .eq-IsProp _ _)))) )

≈→≡ : {f g : T ⇒ U} → f ≈ g → f ≡ g
≈→≡ f≈g = ≅-Injective ⇒≅⇒Canon (≈→≡Canon f≈g)

private
  open module M₀ {Δ} {T U : ⟦Type⟧ Δ}
    = IsEquivalence (≈-isEquivalence T U)
    public using () renaming
    ( refl to ≈-refl
    ; sym to ≈-sym
    ; trans to ≈-trans
    ; reflexive to ≈-reflexive )

id : {T : ⟦Type⟧ Δ} → T ⇒ T
id = record
  { fobj = λ x → x
  ; feq = λ γ≈γ′ x → x
  }

_∘_ : {T U V : ⟦Type⟧ Δ} → U ⇒ V → T ⇒ U → T ⇒ V
_∘_ {Γ} f g = record
  { fobj = f .fobj ∘F g .fobj
  ; feq = λ γ≈γ′ → f .feq γ≈γ′ ∘F g .feq γ≈γ′
  }

⟦Types⟧ : RGraph → Category (lsuc 0ℓ) 0ℓ 0ℓ
⟦Types⟧ Δ = record
  { Obj = ⟦Type⟧ Δ
  ; _⇒_ = _⇒_
  ; _≈_ = _≈_
  ; id = id
  ; _∘_ = _∘_
  ; equiv = ≈-isEquivalence _ _
  ; ∘-resp = λ {Δ Γ Ψ f g h i} f≈g h≈i
    → ≈⁺ λ γ x → trans (f≈g .≈⁻ γ (h .fobj x)) (cong (g .fobj) (h≈i .≈⁻ γ x))
  ; id-r = ≈⁺ λ γ x → refl
  ; id-l = ≈⁺ λ γ x → refl
  ; assoc = ≈⁺ λ γ x → refl
  }

module ⟦Types⟧ {Γ} = Category (⟦Types⟧ Γ)

_≈⟦Type⟧_ : (T U : ⟦Type⟧ Δ) → Set₁
_≈⟦Type⟧_ = ⟦Types⟧._≅_

private
  open module M₁ {Δ} = ⟦Types⟧.≅ {Δ} public using () renaming
    ( refl to ≈⟦Type⟧-refl
    ; sym to ≈⟦Type⟧-sym
    ; trans to ≈⟦Type⟧-trans
    ; reflexive to ≈⟦Type⟧-reflexive )

module ≅-Reasoning = ⟦Types⟧.≅-Reasoning
module ≈-Reasoning = ⟦Types⟧.≈-Reasoning

⟦Type⟧Canon : RGraph → Set₁
⟦Type⟧Canon Δ
  = Σ[ ObjHSet ∈ (Δ .Obj → HSet 0ℓ) ]
    Σ[ eq ∈ (∀ {δ δ′} (δ≈δ′ : Δ .eq δ δ′)
        → (x : ObjHSet δ .type) (y : ObjHSet δ′ .type) → HProp 0ℓ) ]
    (∀ {δ} (x : ObjHSet δ .type) → eq (Δ .eq-refl δ) x x .type)

⟦Type⟧≅⟦Type⟧Canon : ∀ {Δ} → ⟦Type⟧ Δ ≅ ⟦Type⟧Canon Δ
⟦Type⟧≅⟦Type⟧Canon {Δ} = record
  { forth = λ T → T .ObjHSet , T .eqHProp , T .eq-refl
  ; isIso = record
    { back = λ T → record
      { ObjHSet = T .proj₁
      ; eqHProp = T .proj₂ .proj₁
      ; eq-refl = T .proj₂ .proj₂
      }
    ; back∘forth = λ where
        record { ObjHSet = x ; eqHProp = y ; eq-refl = z } → refl
    ; forth∘back = λ x → refl
    }
  }

proj₁∘subst : ∀ {α β γ} {A : Set α} (B : A → Set β) (C : ∀ a → B a → Set γ)
  → ∀ {a a′} (p : a ≡ a′) (x : Σ (B a) (C a))
  → proj₁ (subst (λ a → Σ (B a) (C a)) p x) ≡ subst B p (proj₁ x)
proj₁∘subst B C refl x = refl

≈⟦Type⟧→≡Canon
  : T ≈⟦Type⟧ U
  → ⟦Type⟧≅⟦Type⟧Canon .forth T ≡ ⟦Type⟧≅⟦Type⟧Canon .forth U
≈⟦Type⟧→≡Canon {Δ} {T} {U} T≈U
  = Σ-≡⁺ (T≡U , Σ-≡⁺ (T≈≡U≈ , funext∙ (funext (λ x → U .eq-IsProp _ _))))
  where
    T≅U : ∀ δ → T .Obj δ ≅ U .Obj δ
    T≅U δ = record
      { forth = T≈U .forth .fobj
      ; isIso = record
        { back = T≈U .back .fobj
        ; back∘forth = λ x → T≈U .back-forth .≈⁻ _ _
        ; forth∘back = λ x → T≈U .forth-back .≈⁻ _ _
        }
      }

    T≡U : T .ObjHSet ≡ U .ObjHSet
    T≡U = funext λ δ → HLevel-≡⁺ _ _ (≅→≡ (T≅U δ))

    -- "HoTT makes everything so much nicer", they said. "It's all automatic",
    -- they said.
    abstract
      subst-type : ∀ {α n} (A B : HLevel n α)
        → (p : A .type ≡ B .type)
        → (x : A .type)
        → subst type (HLevel-≡⁺ A B p) x ≡ cast p x
      subst-type A B refl x with IsOfHLevel-IsProp _ (A .level) (B .level)
      ... | refl = refl

      -- I believe this equation would be definitional in Cubical TT.
      subst-T≡U : ∀ {δ} x
        → subst (λ T → T δ .type) T≡U x ≡ T≈U .forth .fobj x
      subst-T≡U {δ} x
        = trans (subst-funext (λ δ T → T .type) _ x)
          (trans (subst-type (T .ObjHSet δ) (U .ObjHSet δ) (≅→≡ (T≅U δ)) x)
            (cast-≅→≡ (T≅U δ)))

      go : (Δ : Set) (T U : Δ → HSet 0ℓ) (eqΔ : Δ → Δ → Set)
        → (eqT : ∀ δ δ′ → eqΔ δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
        → (eqU : ∀ δ δ′ → eqΔ δ δ′ → U δ .type → U δ′ .type → HProp 0ℓ)
        → (T≡U : T ≡ U)
        → (∀ δ δ′ (δ≈δ′ : eqΔ δ δ′) (x : T δ .type) (y : T δ′ .type)
            → eqT _ _ δ≈δ′ x y .type
            ↔ eqU _ _ δ≈δ′
                (subst (λ T → T δ .type) T≡U x)
                (subst (λ T → T δ′ .type) T≡U y)
                .type)
        → _≡_ {A = ∀ {δ δ′} → eqΔ δ δ′ → U δ .type → U δ′ .type → HProp 0ℓ}
            (subst (λ T → ∀ {δ δ′} → eqΔ δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
              T≡U (λ {δ δ′} → eqT δ δ′))
            (λ {δ δ′} → eqU δ δ′)
      go Δ T U eqΔ eqT eqU refl eq = funext∙ λ {δ} → funext∙ λ {δ′}
        → funext λ δ≈δ′ → funext λ x → funext λ y
        → HProp-≡⁺ _ _ (eq δ δ′ δ≈δ′ x y)

      T≈≡U≈ : _
      T≈≡U≈
        = trans
            (proj₁∘subst
              (λ T → ∀ {δ δ′} → Δ .eq δ δ′ → T δ .type → T δ′ .type → HProp 0ℓ)
              (λ T eq → ∀ {δ} (x : T δ .type) → eq (Δ .eq-refl δ) x x .type)
              T≡U
              ((λ {δ δ′} → T .eqHProp {δ} {δ′}), (λ {δ} x → T .eq-refl {δ} x)))
            (go (Δ .Obj) (T .ObjHSet) (U .ObjHSet) (Δ .eq)
              (λ δ δ′ → T .eqHProp {δ} {δ′})
              (λ δ δ′ → U .eqHProp {δ} {δ′})
              T≡U
              λ δ δ′ δ≈δ′ x y → record
                { forth = λ x≈y
                    → subst₂ (λ x y → U .eq δ≈δ′ x y) (sym (subst-T≡U x))
                        (sym (subst-T≡U y)) (T≈U .forth .feq δ≈δ′ x≈y)
                ; back = λ x≈y
                    → subst₂ (λ x y → T .eq δ≈δ′ x y)
                        (trans (cong (T≈U .back .fobj) (subst-T≡U x))
                          (T≈U .back-forth .≈⁻ δ x))
                        (trans (cong (T≈U .back .fobj) (subst-T≡U y))
                          (T≈U .back-forth .≈⁻ δ′ y))
                        (T≈U .back .feq δ≈δ′ x≈y)
                })

≈⟦Type⟧→≡ : T ≈⟦Type⟧ U → T ≡ U
≈⟦Type⟧→≡ T≈U = ≅-Injective ⟦Type⟧≅⟦Type⟧Canon (≈⟦Type⟧→≡Canon T≈U)

subT : ∀ {Δ Ω} → Δ RG.⇒ Ω → ⟦Type⟧ Ω → ⟦Type⟧ Δ
subT {Γ} {Ω} f T = record
  { ObjHSet = T .ObjHSet ∘F f .fobj
  ; eqHProp = T .eqHProp ∘F f .feq
  ; eq-refl = λ x
      → subst (λ p → T .eq p x x) (Ω .eq-IsProp _ _) (T .eq-refl x)
  }

subt : ∀ {Δ Ω} (f : Δ RG.⇒ Ω) {T U : ⟦Type⟧ Ω}
  → T ⇒ U
  → subT f T ⇒ subT f U
subt f g = record
  { fobj = g .fobj
  ; feq = λ γ≈γ′ → g .feq (f .feq γ≈γ′)
  }

subt-∘ : ∀ {Δ Ω} (f : Δ RG.⇒ Ω) {T U V : ⟦Type⟧ Ω}
  → (g : U ⇒ V) (h : T ⇒ U)
  → subt f (g ∘ h) ≈ subt f g ∘ subt f h
subt-∘ f g h = ≈⁺ λ δ γ → refl

subT∘subT : ∀ {Δ Γ Ψ}
  → {f : Δ RG.⇒ Ψ} {g : Γ RG.⇒ Δ} {T : ⟦Type⟧ Ψ}
  → subT g (subT f T) ≈⟦Type⟧ subT (f RG.∘ g) T
subT∘subT = record
  { forth = record { fobj = λ x → x ; feq = λ _ x → x }
  ; back = record { fobj = λ x → x ; feq = λ _ x → x }
  ; back-forth = ≈⁺ λ γ x → refl
  ; forth-back = ≈⁺ λ γ x → refl
  }

castObj : {T U : ⟦Type⟧ Δ} → T ≡ U → ∀ {δ} → Obj T δ → Obj U δ
castObj p {δ} = subst (λ T → Obj T δ) p

≡→≈⟦Type⟧ : {T U : ⟦Type⟧ Δ} → T ≡ U → T ≈⟦Type⟧ U
≡→≈⟦Type⟧ {Δ} {T} {U} T≡U = record
  { forth = record
    { fobj = λ {δ} → castObj T≡U
    ; feq = λ δ≈δ′ x≈y → go T≡U x≈y
    }
  ; back = record
    { fobj = λ {δ} → castObj (sym T≡U)
    ; feq = λ δ≈δ′ x≈y → go (sym T≡U) x≈y
    }
  ; back-forth = ≈⁺ λ δ x → subst-sym-subst T≡U
  ; forth-back = ≈⁺ λ δ x → subst-subst-sym T≡U
  }
  where
    go : {T U : ⟦Type⟧ Δ} (p : T ≡ U) → ∀ {δ δ′} {δ≈δ′ : Δ .eq δ δ′} {x y}
      → eq T δ≈δ′ x y
      → eq U δ≈δ′ (castObj p x) (castObj p y)
    go refl x≈y = x≈y

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Structure.Relator.Function.Proofs where

import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Functional
open import Structure.Relator.Function
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Relator.Properties
open import Structure.Relator
open import Type

private variable ℓ₁ ℓ₂ ℓ₃ ℓₗ ℓₒ ℓₒ₁ ℓₒ₂ ℓₒ₃ ℓₒ₄ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ : Lvl.Level

module _ {A : Type{ℓₒ₁}}{B : Type{ℓₒ₁ Lvl.⊔ ℓₒ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ (φ : A → B → Stmt{ℓₗ}) ⦃ totality : Total(φ)⦄ ⦃ func : Function(φ)⦄ ⦃ _ : ∀{x} → UnaryRelator(φ(x)) ⦄ where
  -- There is a function for a binary relation that is total and function-like.
  relation-function-existence : ∃(f ↦ ∀{x}{y} → (f(x) ≡ y) ↔ φ(x)(y))
  relation-function-existence = [∃]-intro(f) ⦃ \{x y} → proof{x}{y} ⦄ where
    -- The function
    f : A → B
    f(x) = [∃]-witness(total(φ){x})

    -- Proof that the function returns the value that the binary relation defines the element from Y that an element from X is associated with.
    proof : ∀{x}{y} → (f(x) ≡ y) ↔ φ(x)(y)
    proof{x}{y} = [↔]-intro l r where
      r : (f(x) ≡ y) → φ(x)(y)
      r(fxy) = substitute₁(φ(x)) fxy ([∃]-proof(total(φ){x}))

      l : (f(x) ≡ y) ← φ(x)(y)
      l(φxy) = [∃!]-existence-eq-any(totalFunction(φ)) φxy

  -- Constructing a total function from a a binary operation with conditions.
  relation-function : A → B
  relation-function = [∃]-witness(relation-function-existence)

module _ {A : Type{ℓₒ₁}} {B : Type{ℓₒ₂}} ⦃ _ : Equiv{ℓₑ₂}(B) ⦄ {f : A → B} where
  -- A function is total
  -- ∀{x} → ∃(y ↦ f(x) ≡ y)
  Function-totality : Total(x ↦ y ↦ f(x) ≡ y)
  Total.proof(Function-totality) {x} = [∃]-intro(f(x)) ⦃ reflexivity(_≡_) ⦄

module _ {X : Type{ℓₒ₁}} {Y : X → Type{ℓₒ₂}} {φ : (x : X) → Y(x) → Stmt{ℓₗ}} where
  -- Every binary predicate that have its first argument defined for all values
  -- have at least one choice function that can determine the second argument from the first.
  -- Proposition: ∀(X: Type)∀(Y: Type)∀(φ: X → Y → Stmt). (∀(x: X)∃(y: Y). φ(x)(y)) → (∃(choice: X → Y)∀(x: X). φ(x)(choice(x)))
  --   ∀(x: X)∃(y: Y). φ(x)(y) means that the predicate φ holds for every x and some y (which may depend on x). In other words: it associates every element in X with a subset of Y, a function (X → ℘(Y)).
  --   ∃(choice: X → Y)∀(x: X). φ(x)(choice(x)) means that there is a function that picks out a particular y.
  -- Note: This proposition can be recognised as one equivalent variant of "Axiom of Choice" from set theory when formulated in classical logic.
  -- Note: This is similar to what one does in the process of "Skolemization" for an existentially quantified formula in logic.
  dependent-function-predicate-choice : (∀{x : X} → ∃{Obj = Y(x)}(y ↦ φ(x)(y))) → ∃{Obj = (x : X) → Y(x)}(choice ↦ ∀{x : X} → φ(x)(choice(x)))
  dependent-function-predicate-choice(function) = [∃]-intro(x ↦ [∃]-witness(function{x})) ⦃ \{x} → [∃]-proof(function{x}) ⦄

module _ {X : Type{ℓₒ₁}} {Y : Type{ℓₒ₂}} {φ : X → Y → Stmt{ℓₗ}} where
  function-predicate-choice : (∀{x} → ∃(y ↦ φ(x)(y))) → ∃{Obj = X → Y}(choice ↦ ∀{x} → φ(x)(choice(x)))
  function-predicate-choice = dependent-function-predicate-choice

{-
module _ {ℓₗ₁ ℓₗ₂ ℓₒ} {X : Type{ℓₒ}} {P : (X → Stmt{ℓₗ₁}) → Stmt{ℓₗ₂}} where
  standard-choice : (∀{Q : X → Stmt{ℓₗ₁}} → P(Q) → (∃ P)) → ∃{Obj = (X → Stmt{ℓₗ₁}) → X}(f ↦ ∀{Q : X → Stmt{ℓₗ₁}} → P(Q) → Q(f(Q)))
  standard-choice ep = [∃]-intro (choice) ⦃ \{x} → proof{x} ⦄ where
    choice : (X → Stmt{ℓₗ₁}) → X
    choice(R) = [∃]-witness(ep{R} (pr))

    proof : ∀{Q : X → Stmt{ℓₗ₁}} → P(Q) → Q(choice(Q))
    proof{Q} pq = [∃]-proof(surjective{x})
-}

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module List.Order.Bounded.Properties {A : Set}
                   (_≤_ : A → A → Set)
                   (trans≤ : {x y z : A} → x ≤ y → y ≤ z → x ≤ z)  where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Bound.Total.Order.Properties _≤_ trans≤
open import Data.List
open import List.Order.Bounded _≤_
open import List.Sorted _≤_

lemma-sorted++ : {x : A}{xs ys : List A} → xs ≤* (val x) → (val x) *≤ ys → Sorted xs → Sorted ys → Sorted (xs ++ (x ∷ ys))
lemma-sorted++ {x = x} lenx genx _ _ = singls x
lemma-sorted++ lenx (gecx u≤y _) _ sys = conss (lemma-LeB≤ u≤y) sys
lemma-sorted++ (lecx x≤u xs≤*u) u*≤ys (singls x) sys = conss (lemma-LeB≤ x≤u) (lemma-sorted++ xs≤*u u*≤ys nils sys)
lemma-sorted++ (lecx x≤u xs≤*u) u*≤ys (conss x≤z sxs) sys = conss x≤z (lemma-sorted++ xs≤*u u*≤ys sxs sys)

lemma-++≤* : {t : Bound}{x : A}{xs ys : List A} → LeB (val x) t → xs ≤* (val x) → ys ≤* t → (xs ++ (x ∷ ys)) ≤* t
lemma-++≤* u≤t lenx ys≤*t = lecx u≤t ys≤*t
lemma-++≤* u≤t (lecx x≤u xs≤*u) ys≤*u = lecx (transLeB x≤u u≤t) (lemma-++≤* u≤t xs≤*u ys≤*u)

lemma-*≤ : {b : Bound}{x : A}{xs : List A} → LeB b (val x) → (val x) *≤ xs → b *≤ xs
lemma-*≤ _ genx = genx
lemma-*≤ b≤u (gecx u≤x u*≤xs) = gecx (transLeB b≤u u≤x) (lemma-*≤ b≤u u*≤xs)

lemma-++*≤ : {b : Bound}{x : A}{xs ys : List A} → LeB b (val x) → b *≤ xs → (val x) *≤ ys → b *≤ (xs ++ (x ∷ ys))
lemma-++*≤ b≤u genx u*≤ys = gecx b≤u (lemma-*≤ b≤u u*≤ys)
lemma-++*≤ b≤u (gecx b≤x b*≤xs) u*≤ys = gecx b≤x (lemma-++*≤ b≤u b*≤xs u*≤ys)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Support.PropositionalEquality where

open import Function using (flip; id)
open import Relation.Binary.PropositionalEquality public using () renaming (_≡_ to _≣_; refl to ≣-refl; trans to ≣-trans; sym to ≣-sym; cong to ≣-cong; cong₂ to ≣-cong₂; subst to ≣-subst; subst₂ to ≣-subst₂; isEquivalence to ≣-isEquivalence; setoid to ≣-setoid)

module ≣-reasoning = Relation.Binary.PropositionalEquality.≡-Reasoning renaming (_≡⟨_⟩_ to _≣⟨_⟩_)

≣-app : ∀ {a} {A : Set a} {b} {B : A → Set b} {f g : (x : A) → B x} → f ≣ g → (x : A) → f x ≣ g x
≣-app {f = f} {g} = flip (λ x → ≣-cong (flip id x))

≣-appʰ : ∀ {a} {A : Set a} {b} {B : A → Set b} {f g : ∀ {x} → B x} → (λ {x} → f) ≣ g → ∀ {x} → f {x} ≣ g {x}
≣-appʰ {f = f} {g} = λ pf {x} → ≣-cong (λ h → h {x}) pf

≣-subst₂-breakdown-lr : ∀ {a} {A : Set a} {b} {B : Set b} {ℓ} (f : A → B → Set ℓ) {a₁ a₂ : A} (a₁≣a₂ : a₁ ≣ a₂) {b₁ b₂ : B} (b₁≣b₂ : b₁ ≣ b₂) (x : f a₁ b₁) → ≣-subst₂ f a₁≣a₂ b₁≣b₂ x ≣ ≣-subst (f a₂) b₁≣b₂ (≣-subst (λ y → f y b₁) a₁≣a₂ x)
≣-subst₂-breakdown-lr f ≣-refl ≣-refl x = ≣-refl

≣-subst₂-breakdown-rl : ∀ {a} {A : Set a} {b} {B : Set b} {ℓ} (f : A → B → Set ℓ) {a₁ a₂ : A} (a₁≣a₂ : a₁ ≣ a₂) {b₁ b₂ : B} (b₁≣b₂ : b₁ ≣ b₂) (x : f a₁ b₁) → ≣-subst₂ f a₁≣a₂ b₁≣b₂ x ≣ ≣-subst (λ y → f y b₂) a₁≣a₂ (≣-subst (f a₁) b₁≣b₂ x)
≣-subst₂-breakdown-rl f ≣-refl ≣-refl x = ≣-refl

≣-subst-trans : ∀ {a} {A : Set a} {ℓ} (f : A → Set ℓ) {a₁ a₂ a₃ : A} (a₁≣a₂ : a₁ ≣ a₂) (a₂≣a₃ : a₂ ≣ a₃) (x : f a₁) → ≣-subst f (≣-trans a₁≣a₂ a₂≣a₃) x ≣ ≣-subst f a₂≣a₃ (≣-subst f a₁≣a₂ x)
≣-subst-trans f ≣-refl ≣-refl x = ≣-refl

≣-cong₂₊ : ∀ {a b c r} {A : Set a} {B : Set b} {C : A → B → Set c} {R : Set r} (f : (x : A) → (u : B) → .(z : C x u) → R) {x y : A} {u v : B} .(z : C x u) → (x≣y : x ≣ y) (u≣v : u ≣ v) → f x u z ≣ f y v (≣-subst₂ C x≣y u≣v z)
≣-cong₂₊ f z ≣-refl ≣-refl = ≣-refl

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module StronglyRigidOccurrence where

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

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

test : let X : Nat; X = _ in X ≡ suc X
test = refl
-- this gives an error in the occurs checker

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
module Open2 where

data ⊤
  : Set
  where

  tt
    : ⊤

data ⊤'
  (x : ⊤)
  : Set
  where

  tt
    : ⊤' x

record R
  : Set
  where

  field

    x
      : ⊤

    y
      : ⊤

record S
  : Set₁
  where

  field

    x
      : R

  open R x public
    renaming (x to y; y to z)

postulate

  s
    : S

open S s
  using (y)

postulate

  p
    : ⊤' y

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

open import HoTT
open import homotopy.Cogroup
open import cohomology.Theory

-- H^n is a group homomorphism when the domain is (Susp X -> Y).
module cohomology.Cogroup {i} (CT : CohomologyTheory i) (n : ℤ)
  {X : Ptd i} (cogroup-struct : CogroupStructure X) (Y : Ptd i) where

  open CohomologyTheory CT
  open import cohomology.Wedge CT
  open CogroupStructure cogroup-struct
  open import cohomology.CoHSpace CT n co-h-struct

  private
    module dom = GroupStructure (cogroup⊙→-group-structure cogroup-struct Y)
    module codom = Group (hom-group (C n Y) (C-abgroup n X))

  C-fmap-preserves-comp : preserves-comp dom.comp codom.comp (C-fmap n)
  C-fmap-preserves-comp f g = group-hom= $ λ= λ y →
    CEl-fmap n (dom.comp f g) y
      =⟨ C-fmap-∘ n (⊙Wedge-rec f g) ⊙coμ y ⟩
    CEl-fmap n ⊙coμ (CEl-fmap n (⊙Wedge-rec f g) y)
      =⟨ C-fmap-coμ (CEl-fmap n (⊙Wedge-rec f g) y) ⟩
    Group.comp (C n X)
      (CEl-fmap n ⊙winl (CEl-fmap n (⊙Wedge-rec f g) y))
      (CEl-fmap n ⊙winr (CEl-fmap n (⊙Wedge-rec f g) y))
      =⟨ ap2 (Group.comp (C n X))
           ( ∘-CEl-fmap n ⊙winl (⊙Wedge-rec f g) y
           ∙ ap (λ f → CEl-fmap n f y) (⊙WedgeRec.⊙winl-β f g))
           ( ∘-CEl-fmap n ⊙winr (⊙Wedge-rec f g) y
           ∙ ap (λ f → CEl-fmap n f y) (⊙WedgeRec.⊙winr-β f g)) ⟩
    Group.comp (C n X) (CEl-fmap n f y) (CEl-fmap n g y)
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Definition of mutual inductive predicates
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --without-K                #-}
{-# OPTIONS --no-universe-polymorphism #-}

module FOTC.MutualInductivePredicates where

open import FOTC.Base

------------------------------------------------------------------------------
-- Using mutual inductive predicates

data Even : D → Set
data Odd  : D → Set

data Even where
  ezero : Even zero
  esucc : ∀ {n} → Odd n → Even (succ₁ n)

data Odd where
  osucc : ∀ {n} → Even n → Odd (succ₁ n)

-- Non-mutual induction principles

Even-ind : (A : D → Set) →
           A zero →
           (∀ {n} → Odd n → A (succ₁ n)) →
           ∀ {n} → Even n → A n
Even-ind A A0 h ezero      = A0
Even-ind A A0 h (esucc On) = h On

Odd-ind : (A : D → Set) →
          (∀ {n} → Even n → A (succ₁ n)) →
          ∀ {n} → Odd n → A n
Odd-ind A h (osucc En) = h En

-- Mutual induction principles (from Coq)
Even-mutual-ind :
  (A B : D → Set) →
  A zero →
  (∀ {n} → Odd n → B n → A (succ₁ n)) →
  (∀ {n} → Even n → A n → B (succ₁ n)) →
  ∀ {n} → Even n → A n

Odd-mutual-ind :
  (A B : D → Set) →
  A zero →
  (∀ {n} → Odd n → B n → A (succ₁ n)) →
  (∀ {n} → Even n → A n → B (succ₁ n)) →
  ∀ {n} → Odd n → B n

Even-mutual-ind A B A0 h₁ h₂ ezero      = A0
Even-mutual-ind A B A0 h₁ h₂ (esucc On) = h₁ On (Odd-mutual-ind A B A0 h₁ h₂ On)

Odd-mutual-ind A B A0 h₁ h₂ (osucc En) = h₂ En (Even-mutual-ind A B A0 h₁ h₂ En)

module DisjointSum where
  -- Using a single inductive predicate on D × D (see
  -- Blanchette (2013)).

  _+_ : Set → Set → Set
  _+_ = _∨_

  data EvenOdd : D + D → Set where
    eozero :                            EvenOdd (inj₁ zero)
    eoodd  : {n : D} → EvenOdd (inj₁ n) → EvenOdd (inj₂ (succ₁ n))
    eoeven : {n : D} → EvenOdd (inj₂ n) → EvenOdd (inj₁ (succ₁ n))

  -- Induction principle
  EvenOdd-ind : (A : D + D → Set) →
                A (inj₁ zero) →
                ({n : D} → A (inj₁ n) → A (inj₂ (succ₁ n))) →
                ({n : D} → A (inj₂ n) → A (inj₁ (succ₁ n))) →
                {n : D + D} → EvenOdd n → A n
  EvenOdd-ind A A0 h₁ h₂ eozero       = A0
  EvenOdd-ind A A0 h₁ h₂ (eoodd EOn)  = h₁ (EvenOdd-ind A A0 h₁ h₂ EOn)
  EvenOdd-ind A A0 h₁ h₂ (eoeven EOn) = h₂ (EvenOdd-ind A A0 h₁ h₂ EOn)

  -------------------------------------------------------------------------
  -- From the single inductive predicate to the mutual inductive predicates

  -- Even and Odd from EvenOdd.
  Even' : D → Set
  Even' n = EvenOdd (inj₁ n)

  Odd' : D → Set
  Odd' n = EvenOdd (inj₂ n)

  -- From Even/Odd to Even'/Odd'
  Even→Even' : ∀ {n} → Even n → Even' n
  Odd→Odd'   : ∀ {n} → Odd n → Odd' n

  Even→Even' ezero = eozero
  Even→Even' (esucc On) = eoeven (Odd→Odd' On)

  Odd→Odd' (osucc En) = eoodd (Even→Even' En)

  -- From Even'/Odd' to Even/Odd
  Even'→Even : ∀ {n} → Even' n → Even n
  Odd'→Odd : ∀ {n} → Odd' n → Odd n

  -- Requires K.
  Even'→Even eozero     = ezero
  Even'→Even (eoeven h) = esucc (Odd'→Odd h)

  Odd'→Odd (eoodd h) = osucc (Even'→Even h)

  -- TODO (03 December 2012). From EvenOdd-ind to Even-mutual-ind and
  -- Odd-mutual-ind.

module FunctionSpace where
-- Using a single inductive predicate on D → D

  data EvenOdd : D → D → Set where
    eozero :                         EvenOdd zero (succ₁ zero)
    eoodd  : ∀ {m n} → EvenOdd m n → EvenOdd m (succ₁ m)
    eoeven : ∀ {m n} → EvenOdd m n → EvenOdd (succ₁ n) n

  -- Even and Odd from EvenOdd.
  -- Even' : D → Set
  -- Even' n = EvenOdd zero (succ₁ zero) ∨ EvenOdd (succ₁ n) n

  -- Odd' : D → Set
  -- Odd' n = EvenOdd n (succ₁ n)

  -- -- From Even/Odd to Even'/Odd'
  -- Even→Even' : ∀ {n} → Even n → Even' n
  -- Odd→Odd'   : ∀ {n} → Odd n → Odd' n

  -- Even→Even' ezero      = inj₁ eozero
  -- Even→Even' (esucc On) = inj₂ (eoeven (Odd→Odd' On))

  -- Odd→Odd' (osucc En) = eoodd {!!}

  -- -- From Even'/Odd' to Even/Odd
  -- Even'→Even : ∀ {n} → Even' n → Even n
  -- Odd'→Odd : ∀ {n} → Odd' n → Odd n

  -- Even'→Even (inj₁ x) = {!!}
  -- Even'→Even (inj₂ x) = {!!}

  -- Odd'→Odd h = {!!}

------------------------------------------------------------------------------
-- References
--
-- Blanchette, Jasmin Christian (2013). Relational analysis of
-- (co)inductive predicates, (co)algebraic datatypes, and
-- (co)recursive functions. Software Quality Journal 21.1,
-- pp. 101–126.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module RewritingNat where

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero + n = n
(suc m) + n = suc (m + n)

plus0T : Set
plus0T = ∀{x} → (x + zero) ≡ x

plusSucT : Set
plusSucT = ∀{x y} → (x + (suc y)) ≡ suc (x + y)

postulate
  plus0p : plus0T
  {-# REWRITE plus0p #-}

  plusSucp : plusSucT

{-# REWRITE plusSucp #-}

plus0 : plus0T
plus0 = refl

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

reverseAcc : ∀{A n m} → Vec A n → Vec A m → Vec A (n + m)
reverseAcc [] acc = acc
reverseAcc (x ∷ xs) acc = reverseAcc xs (x ∷ acc)


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation

open import Tools.Nat

private
  variable
    n : Nat
    Γ : Con Term n

-- Any level can be embedded into the highest level.
maybeEmb : ∀ {l A}
         → Γ ⊩⟨ l ⟩ A
         → Γ ⊩⟨ ¹ ⟩ A
maybeEmb {l = ⁰} [A] = emb 0<1 [A]
maybeEmb {l = ¹} [A] = [A]

-- The lowest level can be embedded in any level.
maybeEmb′ : ∀ {l A}
          → Γ ⊩⟨ ⁰ ⟩ A
          → Γ ⊩⟨ l ⟩ A
maybeEmb′ {l = ⁰} [A] = [A]
maybeEmb′ {l = ¹} [A] = emb 0<1 [A]

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
module Prelude.Product where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

open _×_ public

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.Categories.Sets where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Categories.Category

open Precategory

module _ ℓ where
  SET : Precategory (ℓ-suc ℓ) ℓ
  SET .ob = Σ (Type ℓ) isSet
  SET .Hom[_,_] (A , _) (B , _) = A → B
  SET .id _  = λ x → x
  SET ._⋆_ f g = λ x → g (f x)
  SET .⋆IdL f = refl
  SET .⋆IdR f = refl
  SET .⋆Assoc f g h = refl

module _ {ℓ} where
  isSetExpIdeal : {A B : Type ℓ} → isSet B → isSet (A → B)
  isSetExpIdeal B/set = isSetΠ λ _ → B/set

  isSetLift : {A : Type ℓ} → isSet A → isSet (Lift {ℓ} {ℓ-suc ℓ} A)
  isSetLift = isOfHLevelLift 2

  instance
    SET-category : isCategory (SET ℓ)
    SET-category .isSetHom {_} {B , B/set} = isSetExpIdeal B/set


text:
-- 2014-03-06 Andreas, Reported by Fabien Renaud

-- This is a larger example for the termination checker, to test performance.
-- In 2014-02-X, it exhausted the heap.

-- 2013-03-17
-- The termination checker now rejects this code instead of crashing.
-- I do not know whether it is supposed to terminate.

-- {-# OPTIONS -v term.matrices:40 #-}

module Issue1075 where

open import Common.Prelude renaming (Nat to ℕ) hiding (map; length)
open import Common.Product
open import Common.Sum
open import Common.Equality

[_] : {A : Set} → A → List A
[ x ] = x ∷ []

map : {A B : Set} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr c n []       = n
foldr c n (x ∷ xs) = c x (foldr c n xs)

length : ∀ {A} → List A → ℕ
length = foldr (λ _ → suc) 0

postulate
  _∈_ : {A : Set} → A → List A → Set
  _⊆_ : {A : Set} → List A → List A → Set

data All {A : Set}
         (P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

_⋐_ : ∀{A} (P Q : A → Set) → Set
P ⋐ Q = ∀{x} → P x → Q x

map-all : ∀ {A : Set} {P : A → Set} {Q : A → Set} →
      P ⋐ Q → All P ⋐ All Q
map-all g []         = []
map-all g (px ∷ pxs) = g px ∷ map-all g pxs

-- Propositions and polarity

data Polarity : Set where
  ⁺ : Polarity
  ⁻ : Polarity

data Type : Polarity → Set where
  a : (Q : String) (⁼ : Polarity) → Type ⁼
  --
  ↓ : (A : Type ⁻) → Type ⁺
  ⊥⁺ : Type ⁺
  _∨_ : (A B : Type ⁺) → Type ⁺
  ⊤⁺ : Type ⁺
  _∧⁺_ : (A B : Type ⁺) → Type ⁺
  --
  ↑ : (A : Type ⁺) → Type ⁻
  _⊃_ : (A : Type ⁺) (B : Type ⁻) → Type ⁻
  ⊤⁻ : Type ⁻
  _∧⁻_ : (A B : Type ⁻) → Type ⁻

-- Judgmental infrastructure

data Conc : Set where
  Inv  : (A : Type ⁻) → Conc
  True : (A : Type ⁺) → Conc
  Susp : (A : Type ⁻) → Conc

stable : Conc → Set
stable (Inv A) = ⊥
stable (True A) = ⊤
stable (Susp A) = ⊤

suspnormal : Conc → Set
suspnormal (Inv A) = ⊤
suspnormal (True A) = ⊤
suspnormal (Susp (a Q .⁻)) = ⊤
suspnormal (Susp (↑ A)) = ⊥
suspnormal (Susp (A ⊃ A₁)) = ⊥
suspnormal (Susp ⊤⁻) = ⊥
suspnormal (Susp (A ∧⁻ A₁)) = ⊥

suspstable : Conc -> Set
suspstable U = stable U × suspnormal U

data Hyp : Set where
  HSusp : (A : Type ⁺) → Hyp
  Pers : (A : Type ⁻) → Hyp

Ctx = List Hyp

hsusp-inj : ∀{x y} → HSusp x ≡ HSusp y → x ≡ y
hsusp-inj refl = refl

{- Suspension normality: all suspended propositions are atomic -}
suspnormalΓ : Ctx → Set
suspnormalΓ Γ = ∀{A} → HSusp A {-Membership-≡.-}∈ Γ → ∃ λ Q → A ≡ (a Q ⁺)

postulate
  conssusp   : ∀{Γ Q} → suspnormalΓ Γ → suspnormalΓ ((HSusp (a Q ⁺)) ∷ Γ)
  conspers   : ∀{Γ A} → suspnormalΓ Γ → suspnormalΓ ((Pers A) ∷ Γ)
  fromctx    : ∀{A B Γ} (Γ' : Ctx) → B ∈ (Γ' ++ A ∷ Γ) → (A ≡ B) ⊎ (B ∈ (Γ' ++ Γ))
  fromctxGen : ∀{A} {Γ : Ctx} → (Γ' : Ctx) → (L : Ctx) → A ∈ (Γ' ++ L ++ Γ) → (A ∈ L) ⊎ (A ∈ (Γ' ++ Γ))

-- Sequent calculus

data SeqForm : Set where
  Rfoc : (A : Type ⁺) → SeqForm
  Left : (L : List (Type ⁺) ⊎ Type ⁻) (U : Conc) → SeqForm

suspnormalF : SeqForm → Set
suspnormalF (Rfoc A) = ⊤
suspnormalF (Left L U) = suspnormal U

data Exp (Γ : Ctx) : SeqForm → Set

Value : (Γ : Ctx) → Type ⁺ → Set
Value Γ A = Exp Γ (Rfoc A)

Term : (Γ : Ctx) → List (Type ⁺) → Conc → Set
Term Γ Ω U = Exp Γ (Left (inj₁ Ω) U)

Spine : (Γ : Ctx) (A : Type ⁻) (U : Conc) → Set
Spine Γ A U = Exp Γ (Left (inj₂ A) U)

data Exp Γ where

  -- Values
  id⁺ : ∀{A}
    (v : HSusp A ∈ Γ)
    → Value Γ A
  ↓R : ∀{A}
    (N : Term Γ [] (Inv A))
    → Value Γ (↓ A)
  ∨R₁ : ∀{A B}
    (V : Value Γ A)
    → Value Γ (A ∨ B)
  ∨R₂ : ∀{A B}
    (V : Value Γ B)
    → Value Γ (A ∨ B)
  ⊤⁺R : Value Γ ⊤⁺
  ∧⁺R : ∀{A B}
    (V₁ : Value Γ A)
    (V₂ : Value Γ B)
    → Value Γ (A ∧⁺ B)

  -- Terms
  focR : ∀{A}
    (V : Value Γ A)
    → Term Γ [] (True A)
  focL : ∀{A U}
    (pf : stable U)
    (x : Pers A ∈ Γ)
    (Sp : Spine Γ A U)
    → Term Γ [] U
  η⁺ : ∀{Q Ω U}
    (N : Term (HSusp (a Q ⁺) ∷ Γ) Ω U)
    → Term Γ (a Q ⁺ ∷ Ω) U
  ↓L : ∀{A Ω U}
    (N : Term (Pers A ∷ Γ) Ω U)
    → Term Γ (↓ A ∷ Ω) U
  ⊥L : ∀{U Ω}
    → Term Γ (⊥⁺ ∷ Ω) U
  ∨L : ∀{A B Ω U}
    (N₁ : Term Γ (A ∷ Ω) U)
    (N₂ : Term Γ (B ∷ Ω) U)
    → Term Γ ((A ∨ B) ∷ Ω) U
  ⊤⁺L : ∀{U Ω}
    (N : Term Γ Ω U)
    → Term Γ (⊤⁺ ∷ Ω) U
  ∧⁺L : ∀{U Ω A B}
    (N : Term Γ (A ∷ B ∷ Ω) U)
    → Term Γ ((A ∧⁺ B) ∷ Ω) U
  η⁻ : ∀{Q}
    (N : Term Γ [] (Susp (a Q ⁻)))
    → Term Γ [] (Inv (a Q ⁻))
  ↑R : ∀{A}
    (N : Term Γ [] (True A))
    → Term Γ [] (Inv (↑ A))
  ⊃R : ∀{A B}
    (N : Term Γ [ A ] (Inv B))
    → Term Γ [] (Inv (A ⊃ B))
  ⊤⁻R : Term Γ [] (Inv ⊤⁻)
  ∧⁻R : ∀{A B}
    (N₁ : Term Γ [] (Inv A))
    (N₂ : Term Γ [] (Inv B))
    → Term Γ [] (Inv (A ∧⁻ B))

  -- Spines
  id⁻ : ∀{A}
    → Spine Γ A (Susp A)
  ↑L : ∀{A U}
    (N : Term Γ [ A ] U)
    → Spine Γ (↑ A) U
  ⊃L : ∀{A B U}
    (V : Value Γ A)
    (Sp : Spine Γ B U)
    → Spine Γ (A ⊃ B) U
  ∧⁻L₁ : ∀{A B U}
    (Sp : Spine Γ A U)
    → Spine Γ (A ∧⁻ B) U
  ∧⁻L₂ : ∀{A B U}
    (Sp : Spine Γ B U)
    → Spine Γ (A ∧⁻ B) U

-- Weakening
postulate
  sub-cons-congr : ∀{A : Set} {x : A} {xs ys : List A}
      → xs ⊆ ys
      → (x ∷ xs) ⊆ (x ∷ ys)

  sub-wkex : ∀{A : Set} {x y : A} {xs ys : List A}
    → (x ∷ xs) ⊆ (x ∷ y ∷ xs)

  sub-cntr : ∀{A : Set} {x : A}
       → (xs : List A)
       → x ∈ xs
       → (x ∷ xs) ⊆ xs

  wk : ∀{Γ Γ' Form} → Γ ⊆ Γ' → Exp Γ Form → Exp Γ' Form
  wken : ∀{Γ A Form} → Exp Γ Form → Exp (A ∷ Γ) Form

wken-all-rfoc : ∀{Γ' Γ xs B}
  → All (λ A → Exp (Γ' ++ Γ) (Rfoc A)) xs
  → All (λ A → Exp (B ∷ (Γ' ++ Γ)) (Rfoc A)) xs
wken-all-rfoc [] = []
wken-all-rfoc (px ∷ All) = map-all (\x → wken x) (px ∷ All)

wken-all-inv : ∀{Γ' Γ Ω xs B}
  → All (λ A → Exp (Γ' ++ Γ) (Left (inj₁ Ω) (Inv A))) xs
  → All (λ A → Exp (B ∷ (Γ' ++ Γ)) (Left (inj₁ Ω) (Inv A))) xs
wken-all-inv [] = []
wken-all-inv (px ∷ All) = map-all (\x → wken x) (px ∷ All)

postulate
  wkex : ∀{Γ A B Form} → Exp (A ∷ Γ) Form → Exp (A ∷ B ∷ Γ) Form
  wkex2 : ∀{Γ A B C Form} → Exp (A ∷ B ∷ Γ) Form → Exp (A ∷ B ∷ C ∷ Γ) Form

cntr : ∀{A Form} → (Γ : Ctx) → A ∈ Γ → Exp (A ∷ Γ) Form → Exp Γ Form
cntr Γ In Exp = wk (sub-cntr Γ In) Exp

postulate

  exch-cons : ∀{Γ Γ' LA C x} → Term (x ∷ Γ ++ Γ') LA C → Term (Γ ++ x ∷ Γ') LA C

  subst⁺ :
    ∀{Γ Form}
    → (Γ' : Ctx)
    → (LAi : List (Type ⁺))
    → All (\x → Value (Γ' ++ Γ) x) LAi
    → Exp (Γ' ++ map (\x → HSusp x) (LAi) ++ Γ) Form
    → Exp (Γ' ++ Γ) Form

  subst⁻ : ∀{Γ A L U}
    → stable U
    → Exp Γ (Left L (Susp A))
    → Spine Γ A U
    → Exp Γ (Left L U)

cut⁺ : ∀{U Γ Ω}
  → suspnormalΓ Γ
  → suspnormal U
  → (LAi : List (Type ⁺))
  → All (\x → Value Γ x) LAi
  → Term Γ (LAi ++ Ω) U
  → Term Γ Ω U

cut⁻ : ∀{U Γ N}
  → suspnormalΓ Γ
  → suspstable U
  → (LA : List (Type ⁻))
  → (length LA ≡ suc N)
  → All (\x → Term Γ [] (Inv x)) LA
  → All (\x → Spine Γ x U) LA
  → Term Γ [] U

rsubst+  : ∀{Ω Γ Form} (Γ' : Ctx)
  → suspnormalΓ (Γ' ++ Γ)
  → suspnormal Form
  → (LA+ : List (Type ⁺))
  → (LA- : List (Type ⁻))
  → All (\x →  Term (Γ' ++ Γ) [] (Inv x)) LA-
  → All (\x → Value Γ x) LA+
  → Term (Γ' ++ (map (\x → Pers x) LA-) ++ Γ) (LA+ ++ Ω) Form
  → Term (Γ' ++ Γ) Ω  Form

postulate rsubst-v : ∀{Γ Form} (Γ' : Ctx)   → suspnormalΓ (Γ' ++ Γ)  → suspnormalF Form  → (LA- : List (Type ⁻))  → All (\x →  Term (Γ' ++ Γ) [] (Inv x)) LA-  → Exp (Γ' ++ (map (\x → Pers x) LA-) ++ Γ) Form  → Exp (Γ' ++ Γ) Form

-- {-# NO_TERMINATION_CHECK #-}
--rsubst : ∀{Γ Form A} (Γ' : Ctx)
--  → suspnormalΓ (Γ' ++ Γ)
--  → suspnormalF Form
--  → Term (Γ' ++ Γ) [] (Inv A)
--  → Exp (Γ' ++ (Pers A) ∷ Γ) Form
--  → Exp (Γ' ++ Γ) Form

lsubst : ∀{Γ U L A}
  → suspnormalΓ Γ
  → suspstable U
  → Exp Γ (Left L (True A))
  → Term Γ [ A ] U
  → Exp Γ (Left L U)

-- -- Positive principal substitution

cut⁺ pfΓ pf [] Values T = T

cut⁺ pfΓ pf (z ∷ LA) ((id⁺ v) ∷ Values) N with (pfΓ v)
cut⁺ pfΓ pf (.(a A ⁺) ∷ LA) (id⁺ v ∷ Values) (η⁺ N) | A , refl =
  subst⁺ [] (a A ⁺ ∷ []) (id⁺ v ∷ []) (cut⁺ (conssusp pfΓ) pf LA (wken-all-rfoc {[]} Values) N)
cut⁺ {U} {Γ} {Ω} pfΓ pf (.(↓ A) ∷ LA) (↓R N ∷ Values) (↓L {A} N') =
  rsubst+ [] pfΓ pf LA (A ∷ []) (N ∷ []) Values N'
  -- rsubst+ [] pfΓ pf N (cut⁺ (conspers pfΓ) pf LA (wken-all-rfoc {[]} Values) N₁)
cut⁺ pfΓ pf (.(A ∨ B) ∷ LA) (∨R₁ V ∷ Values) (∨L {A} {B} N₁ N₂) = cut⁺ pfΓ pf (A ∷ LA) (V ∷ Values) N₁
cut⁺ pfΓ pf (.(A ∨ B) ∷ LA) (∨R₂ V ∷ Values) (∨L {A} {B} N₁ N₂) =  cut⁺ pfΓ pf (B ∷ LA) (V ∷ Values) N₂
cut⁺ pfΓ pf (.⊤⁺ ∷ LA) (px ∷ Values) (⊤⁺L N) = cut⁺ pfΓ pf LA Values N
cut⁺ pfΓ pf ((A ∧⁺ B) ∷ LA) (∧⁺R V₁ V₂ ∷ Values) (∧⁺L N) = cut⁺ pfΓ pf (B ∷ LA) (V₂ ∷ Values) (cut⁺ pfΓ pf ((A ∷ [])) (V₁ ∷ [])  N)

-- -- Negative principle substitution

cut⁻ pfΓ pf [] () LExp LExp'
cut⁻ pfΓ pf (_ ∷ LA) LL (focL () x Sp ∷ LExp) (px₁ ∷ LExp')

cut⁻ pfΓ pf (a Q .⁻ ∷ LA) LL (η⁻ N₁ ∷ LExp) (id⁻ ∷ LExp') = N₁

cut⁻ pfΓ (proj₁ , ()) (⊤⁻ ∷ LA) LL (⊤⁻R ∷ LExp) (id⁻ ∷ LExp')
cut⁻ pfΓ (proj₁ , ()) (↑ x ∷ LA) LL (↑R N₁ ∷ LExp) (id⁻ ∷ LExp')
cut⁻ pfΓ (proj₁ , ()) ((x ⊃ x₁) ∷ LA) LL (⊃R N₁ ∷ LExp) (id⁻ ∷ LExp')
cut⁻ pfΓ (proj₁ , ()) ((x ∧⁻ x₁) ∷ LA) LL (∧⁻R N₁ N₂ ∷ LExp) (id⁻ ∷ LExp')

cut⁻ pfΓ pf (↑ x ∷ LA) LL (↑R N₁ ∷ LExp) (↑L N₂ ∷ LExp') = lsubst pfΓ pf N₁ N₂

cut⁻ pfΓ pf ((x ⊃ x₁) ∷ LA) refl (⊃R N₁ ∷ LExp) (⊃L V Sp ∷ LExp') =
  cut⁻ pfΓ pf (x₁ ∷ LA) refl ((cut⁺ pfΓ _ (x ∷ []) (V ∷ []) N₁) ∷ LExp) (Sp ∷ LExp')

cut⁻ pfΓ pf ((x ∧⁻ x₁) ∷ LA) refl (∧⁻R N₁ N₂ ∷ LExp) (∧⁻L₁ Sp ∷ LExp') =
  cut⁻ pfΓ pf (x ∷ LA) refl (N₁ ∷ LExp) (Sp ∷ LExp')

cut⁻ pfΓ pf ((x ∧⁻ x₁) ∷ LA) LL (∧⁻R N₁ N₂ ∷ LExp) (∧⁻L₂ Sp ∷ LExp') =
  cut⁻ pfΓ pf (x₁ ∷ LA) refl (N₂ ∷ LExp) (Sp ∷ LExp')

-- helper : ∀{Γ LA- A} →
--   All (λ x₂ → Exp (Γ) (Left (inj₁ []) (Inv x₂))) LA-
--   → Any (_≡_ (Pers A)) (map Pers LA-)
--   → All (λ x₂ → Exp (Γ) (Left (inj₁ []) (Inv x₂))) (A ∷ [])
-- helper [] ()
-- helper (px ∷ L) (here refl) = px ∷ []
-- helper (px ∷ L) (there In) = helper L In

rsubst+ Γ' pfΓ pf [] LA- LT [] (focR V) = focR (rsubst-v Γ' pfΓ _ LA- LT V )
rsubst+ Γ' pfΓ pf [] LA- LT [] (focL pf₁ x Sp) with fromctxGen Γ' (map Pers LA-) x
rsubst+ Γ' pfΓ pf [] LA- LT [] (focL {A} pf₁ x Sp) | inj₁ x₁ =
  cut⁻ pfΓ (pf₁ , pf) (A ∷ []) refl {!(helper LT x₁)!} ((rsubst-v Γ' pfΓ pf LA- LT Sp) ∷ [])
rsubst+ Γ' pfΓ pf [] LA- LT [] (focL pf₁ x Sp) | inj₂ y =
  focL pf₁ y (rsubst-v Γ' pfΓ pf LA- LT Sp )
rsubst+ Γ' pfΓ pf [] LA- LT [] (η⁺ N) =
  η⁺ (rsubst-v (_ ∷ Γ' ) (conssusp pfΓ) pf LA- (wken-all-inv {[]} LT) N )
rsubst+ Γ' pfΓ pf [] LA- LT [] (↓L N) =
  ↓L (rsubst-v (_ ∷ Γ' ) (conspers pfΓ) pf LA- (wken-all-inv {[]} LT) N )
rsubst+ Γ' pfΓ pf [] LA- LT [] ⊥L = ⊥L
rsubst+ Γ' pfΓ pf [] LA- LT [] (∨L N₁ N₂) =
  ∨L (rsubst+ Γ' pfΓ pf [] LA- LT [] N₁) (rsubst+ Γ' pfΓ pf [] LA- LT [] N₂)
rsubst+ Γ' pfΓ pf [] LA- LT [] (⊤⁺L N) = ⊤⁺L (rsubst+ Γ' pfΓ pf [] LA- LT [] N )
rsubst+ Γ' pfΓ pf [] LA- LT [] (∧⁺L N) = ∧⁺L (rsubst+  Γ' pfΓ pf [] LA- LT [] N)
rsubst+ Γ' pfΓ pf [] LA- LT [] (η⁻ N) = η⁻ (rsubst+  Γ' pfΓ pf [] LA- LT [] N)
rsubst+ Γ' pfΓ pf [] LA- LT [] (↑R N) = ↑R (rsubst+  Γ' pfΓ pf [] LA- LT [] N)
rsubst+ Γ' pfΓ pf [] LA- LT [] (⊃R N) = ⊃R (rsubst+  Γ' pfΓ pf [] LA- LT [] N)
rsubst+ Γ' pfΓ pf [] LA- LT [] ⊤⁻R = ⊤⁻R
rsubst+ Γ' pfΓ pf [] LA- LT [] (∧⁻R N₁ N₂) =
  ∧⁻R (rsubst+  Γ' pfΓ pf [] LA- LT [] N₁) (rsubst+  Γ' pfΓ pf [] LA- LT [] N₂)

-- rsubst+ Γ' pfΓ pf (↓ x ∷ LA+) LA- LT (id⁺ v ∷ Values) (↓L N) with (pfΓ (++ʳ Γ' v))
-- ... | proj₁ , ()

-- ------------
-- -- Part which requires a list for negative types
-- rsubst+ {Ω} {Γ} Γ' pfΓ pf (a Q .⁺ ∷ LA+) LA- LT (id⁺ v ∷ Values) (η⁺ N) =
--   rsubst+ Γ' pfΓ pf LA+ LA- (LT ) Values
--           (cntr (Γ' ++ map Pers LA- ++ Γ) (++ʳ Γ' (++ʳ (map Pers LA-) v) ) N)

-- rsubst+ {Ω} {Γ} Γ' pfΓ pf (↓ x ∷ LA+) LA- LT (↓R N ∷ Values) (↓L N₁) =
--   rsubst+ Γ' pfΓ pf LA+ (x ∷ LA-) ((wk (λ x₂ → ++ʳ Γ' x₂) N) ∷ LT)  Values (exch-cons {Γ'} {map Pers LA- ++ Γ} N₁)
--------------
-- rsubst+ Γ' pfΓ pf (⊥⁺ ∷ LA+) LA- LT (id⁺ v ∷ Values) ⊥L with (pfΓ (++ʳ Γ' v))
-- ... | proj₁ , ()
-- rsubst+ Γ' pfΓ pf (x ∨ x₁ ∷ LA+) LA- LT (id⁺ v ∷ Values) (∨L N₁ N₂)  with (pfΓ (++ʳ Γ' v))
-- ... | proj₁ , ()
rsubst+ Γ' pfΓ pf ((x ∨ x₁) ∷ LA+) LA- LT (∨R₁ V ∷ Values) (∨L N₁ N₂) = rsubst+ Γ' pfΓ pf (x ∷ LA+) LA- LT (V ∷ Values) N₁
rsubst+ Γ' pfΓ pf ((x ∨ x₁) ∷ LA+) LA- LT (∨R₂ V ∷ Values) (∨L N₁ N₂) = rsubst+ Γ' pfΓ pf (x₁ ∷ LA+) LA- LT (V ∷ Values) N₂
rsubst+ Γ' pfΓ pf (⊤⁺ ∷ LA+) LA- LT (_ ∷ Values) (⊤⁺L N) =  rsubst+ Γ' pfΓ pf LA+ LA- LT Values N
-- rsubst+ Γ' pfΓ pf (x ∧⁺ x₁ ∷ LA+) LA- LT (id⁺ v ∷ Values) (∧⁺L N) with (pfΓ (++ʳ Γ' v))
-- ... | proj₁ , ()
rsubst+ Γ' pfΓ pf ((x ∧⁺ x₁) ∷ LA+) LA- LT (∧⁺R V₁ V₂ ∷ Values) (∧⁺L N) =
  rsubst+ Γ' pfΓ pf (x ∷ x₁ ∷ LA+) LA- LT (V₁ ∷ V₂ ∷ Values) N
rsubst+ {_} {_} {_} _ _ _ _ _ _ _ _ = ?

-- -- -- Substitution out of terms
lsubst pfΓ pf (focR {A} V) N = cut⁺ pfΓ (proj₂ pf) (A ∷ []) (V ∷ []) N
lsubst pfΓ pf (focL pf' x Sp) N = focL (proj₁ pf) x (lsubst pfΓ pf Sp N)
lsubst pfΓ pf (η⁺ M) N = η⁺ (lsubst (conssusp pfΓ) pf M (wken N))
lsubst pfΓ pf (↓L M) N = ↓L (lsubst (conspers pfΓ) pf M (wken N))
lsubst pfΓ pf ⊥L M = ⊥L
lsubst pfΓ pf (∨L M₁ M₂) N = ∨L (lsubst pfΓ pf M₁ N) (lsubst pfΓ pf M₂ N)
lsubst pfΓ pf (⊤⁺L M) N = ⊤⁺L (lsubst pfΓ pf M N)
lsubst pfΓ pf (∧⁺L M) N = ∧⁺L (lsubst pfΓ pf M N)

-- Substitution of of spines
lsubst pfΓ pf (↑L M) N = ↑L (lsubst pfΓ pf M N)
lsubst pfΓ pf (⊃L V Sp) N = ⊃L V (lsubst pfΓ pf Sp N)
lsubst pfΓ pf (∧⁻L₁ Sp) N = ∧⁻L₁ (lsubst pfΓ pf Sp N)
lsubst pfΓ pf (∧⁻L₂ Sp) N = ∧⁻L₂ (lsubst pfΓ pf Sp N)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Category.Choice where
open import Data.Sum using (_⊎_)
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Category.Profunctor

record ChoiceImp {a b : Level} (p : Set a → Set a → Set b) : Set (lsuc (a ⊔ b)) where
  field
    isProfunctor : ProfunctorImp p
    left' : ∀ {x y z : Set a} → p x y → p (x ⊎ z) (y ⊎ z)
    right' : ∀ {x y z : Set a} → p x y → p (z ⊎ x) (z ⊎ y)

module Choice {a b : Level} {p : Set a → Set a → Set b} (isChoice : ChoiceImp p) where
  left : ∀ {x y z : Set a} → p x y → p (x ⊎ z) (y ⊎ z)
  left = ChoiceImp.left' isChoice
  right : ∀ {x y z : Set a} → p x y → p (z ⊎ x) (z ⊎ y)
  right = ChoiceImp.right' isChoice
  open Profunctor (ChoiceImp.isProfunctor isChoice)

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
open import Common.Prelude
open import Common.Equality
open import Common.Product

test : (p : Bool × Bool) → proj₁ p ≡ true → Set
test _ e = {!e!}

-- WAS:
-- Splitting on e gives
-- test r refl = ?
-- proj₁ r != true of type Bool
-- when checking that the pattern refl has type proj₁ r ≡ true


text:
module Category.Strong where
open import Data.Product using (_×_)
open import Agda.Primitive using (Level; _⊔_; lsuc)
open import Category.Profunctor

record StrongImp {a b : Level} (p : Set a → Set a → Set b) : Set (lsuc (a ⊔ b)) where
  field
    isProfunctor : ProfunctorImp p
    first' : ∀ {x y z : Set a} → p x y → p (x × z) (y × z)
    second' : ∀ {x y z : Set a} → p x y → p (z × x) (z × y)

module Strong {a b : Level} {p : Set a → Set a → Set b} (isStrong : StrongImp p) where
  first : ∀ {x y z : Set a} → p x y → p (x × z) (y × z)
  first = StrongImp.first' isStrong
  second : ∀ {x y z : Set a} → p x y → p (z × x) (z × y)
  second = StrongImp.second' isStrong
  open Profunctor (StrongImp.isProfunctor isStrong)


text:
module Bee2.Crypto.Bign where

open import Data.ByteString
open import Data.ByteVec
open import Data.Bool using (Bool)
open import Data.Nat using (ℕ)
open import Data.Product using (_,_)
open import Agda.Builtin.TrustMe using (primTrustMe)

import Bee2.Crypto.Defs
open Bee2.Crypto.Defs
open Bee2.Crypto.Defs using (Hash) public

{-# FOREIGN GHC import qualified Bee2.Crypto.Bign    #-}
{-# FOREIGN GHC import qualified Data.ByteString    #-}

postulate
  -- bignstd128-pri [32] → belt-hash [32] → bign-sig [48]
  primBignSign2 : ByteString Strict → ByteString Strict → ByteString Strict
  -- bignstd128-pri [32] → bignstd128-pub [64]
  primBignCalcPubkey : ByteString Strict → ByteString Strict
  -- bignstd128-pub [64] → belt-hash [32] → bign-sig [48] → Bool
  primBignVerify : ByteString Strict → ByteString Strict → ByteString Strict → Bool

{-# COMPILE GHC primBignSign2 =
    ( \pri hash -> Bee2.Crypto.Bign.bignSign2'bs 128 pri Bee2.Crypto.Belt.hbelt_oid hash ) #-}
{-# COMPILE GHC primBignCalcPubkey =
    ( \pri -> Bee2.Crypto.Bign.bignCalcPubkey'bs 128 pri ) #-}
{-# COMPILE GHC primBignVerify =
    ( \pub hash sig -> Bee2.Crypto.Bign.bignVerify'bs 128 pub Bee2.Crypto.Belt.hbelt_oid hash sig ) #-}

Pri = ByteVec {Strict} 32
Pub = ByteVec {Strict} 64 -- TODO: add IsValid
Sig = ByteVec {Strict} 48

bignSign2 : Pri → Hash → Sig
bignSign2 (pri , _) (hash , _) = primBignSign2 pri hash , primTrustMe

bignCalcPubkey : Pri → Pub
bignCalcPubkey (pri , _) = primBignCalcPubkey pri , primTrustMe

bignVerify : Pub → Hash → Sig → Bool
bignVerify (pub , _) (hash , _) (sig , _) = primBignVerify pub hash sig


text:
------------------------------------------------------------------------
-- A partial order
------------------------------------------------------------------------

{-# OPTIONS --cubical --sized-types #-}

open import Prelude hiding (⊥; module W)

module Partiality-monad.Coinductive.Partial-order {a} {A : Type a} where

open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms.Univalence equality-with-paths
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional equality-with-paths
  as Trunc
open import Quotient equality-with-paths as Quotient
open import Univalence-axiom equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity as B using (_≈_)
import Delay-monad.Partial-order as PO

open import Partiality-monad.Coinductive

-- An ordering relation.

LE : A ⊥ → A ⊥ → Proposition a
LE x y = Quotient.rec
  (λ where
     .[]ʳ x                 → LE″ x y
     .[]-respects-relationʳ → left-lemma″-∥∥ y
     .is-setʳ               → is-set)
  x
  where
  LE′ : Delay A ∞ → Delay A ∞ → Proposition a
  LE′ x y = ∥ x PO.⊑ y ∥ , truncation-is-proposition

  abstract

    is-set : Is-set (∃ λ (A : Type a) → Is-proposition A)
    is-set = Is-set-∃-Is-proposition ext prop-ext

    right-lemma : ∀ {x y z} → x ≈ y → LE′ z x ≡ LE′ z y
    right-lemma x≈y =
      _↔_.to (⇔↔≡″ ext prop-ext)
             (record { to   = ∥∥-map (flip PO.transitive-⊑≈ x≈y)
                     ; from = ∥∥-map (flip PO.transitive-⊑≈
                                        (B.symmetric x≈y))
                     })

    right-lemma-∥∥ : ∀ {x y z} → ∥ x ≈ y ∥ → LE′ z x ≡ LE′ z y
    right-lemma-∥∥ = Trunc.rec is-set right-lemma

  LE″ : Delay A ∞ → A ⊥ → Proposition a
  LE″ x y = Quotient.rec
    (λ where
       .[]ʳ                   → LE′ x
       .[]-respects-relationʳ → right-lemma-∥∥
       .is-setʳ               → is-set)
    y

  abstract

    left-lemma : ∀ {x y z} → x ≈ y → LE′ x z ≡ LE′ y z
    left-lemma x≈y =
      _↔_.to (⇔↔≡″ ext prop-ext)
             (record { to   = ∥∥-map (PO.transitive-≈⊑
                                        (B.symmetric x≈y))
                     ; from = ∥∥-map (PO.transitive-≈⊑ x≈y)
                     })

    left-lemma″ : ∀ {x y} z → x ≈ y → LE″ x z ≡ LE″ y z
    left-lemma″ {x} {y} z x≈y = Quotient.elim-prop
      {P = λ z → LE″ x z ≡ LE″ y z}
      (λ where
         .[]ʳ _             → left-lemma x≈y
         .is-propositionʳ _ →
           Is-set-∃-Is-proposition ext prop-ext)
      z

    left-lemma″-∥∥ : ∀ {x y} z → ∥ x ≈ y ∥ → LE″ x z ≡ LE″ y z
    left-lemma″-∥∥ z = Trunc.rec
     is-set
     (left-lemma″ z)

infix 4 _⊑_

_⊑_ : A ⊥ → A ⊥ → Type a
x ⊑ y = proj₁ (LE x y)

-- _⊑_ is propositional.

⊑-propositional : ∀ x y → Is-proposition (x ⊑ y)
⊑-propositional x y = proj₂ (LE x y)

-- _⊑_ is reflexive.

reflexive : ∀ x → x ⊑ x
reflexive = Quotient.elim-prop λ where
  .[]ʳ x             → ∣ PO.reflexive x ∣
  .is-propositionʳ x → ⊑-propositional [ x ] [ x ]

-- _⊑_ is antisymmetric.

antisymmetric : ∀ x y → x ⊑ y → y ⊑ x → x ≡ y
antisymmetric = Quotient.elim-prop λ where
  .[]ʳ x → Quotient.elim-prop (λ where
    .[]ʳ y ∥x⊑y∥ ∥y⊑x∥ →
      []-respects-relation $
      Trunc.rec truncation-is-proposition
        (λ x⊑y → ∥∥-map (PO.antisymmetric x⊑y) ∥y⊑x∥)
        ∥x⊑y∥
    .is-propositionʳ _ →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      ⊥-is-set)
  .is-propositionʳ _ →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    ⊥-is-set

-- _⊑_ is transitive.

transitive : ∀ x y z → x ⊑ y → y ⊑ z → x ⊑ z
transitive = Quotient.elim-prop λ where
  .[]ʳ x → Quotient.elim-prop λ where
    .[]ʳ y → Quotient.elim-prop λ where
      .[]ʳ z ∥x⊑y∥ →
        Trunc.rec truncation-is-proposition
          (λ y⊑z → ∥∥-map (λ x⊑y → PO.transitive x⊑y y⊑z) ∥x⊑y∥)
      .is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        Π-closure ext 1 λ _ →
        ⊑-propositional [ _ ] [ _ ]
    .is-propositionʳ _ →
      Π-closure ext 1 λ z →
      Π-closure ext 1 λ _ →
      Π-closure ext 1 λ _ →
      ⊑-propositional [ _ ] z
  .is-propositionʳ _ →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ z →
    Π-closure ext 1 λ _ →
    Π-closure ext 1 λ _ →
    ⊑-propositional [ _ ] z

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module SystemF.Substitutions.Lemmas where

open import Prelude hiding (module Fin; id)

open import SystemF.WellTyped
open import SystemF.Substitutions

open import Data.Fin as Fin using ()
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec hiding ([_])

open import Extensions.Substitution
open import Extensions.Vec
open import Data.Vec.Properties

import Category.Applicative.Indexed as Applicative
open Applicative.Morphism using (op-<$>)

module TypeLemmas where
  open TypeSubst using (module Lifted; module TypeApp)
  open import Data.Fin.Substitution.Lemmas
  open import Data.Fin.Substitution.Lemmas public using (module VarLemmas)
  open import Data.Star using (Star; ε; _◅_)

  typeLemmas : TermLemmas Type
  typeLemmas = record { termSubst = TypeSubst.typeSubst; app-var = refl ; /✶-↑✶ = Lemma./✶-↑✶ }
    where
      module Lemma {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} where

        open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
        open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

        /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                          (∀ k x → tvar x /✶₁ σs₁ ↑✶₁ k ≡ tvar x /✶₂ σs₂ ↑✶₂ k) →
                          ∀ k t → t /✶₁ σs₁ ↑✶₁ k ≡ t /✶₂ σs₂ ↑✶₂ k
        /✶-↑✶ ρs₁ ρs₂ hyp k (tvar x) = hyp k x
        /✶-↑✶ ρs₁ ρs₂ hyp k (tc c) = begin
            (tc c) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.tc-/✶-↑✶ _ k ρs₁ ⟩
            (tc c)
          ≡⟨ sym $ TypeApp.tc-/✶-↑✶ _ k ρs₂ ⟩
            (tc c) /✶₂ ρs₂ ↑✶₂ k ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (a ⟶ b) = begin
            (a ⟶  b) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.⟶-/✶-↑✶ _ k ρs₁ ⟩
            (a /✶₁ ρs₁ ↑✶₁ k) ⟶ (b /✶₁ ρs₁ ↑✶₁ k)
          ≡⟨ cong₂ _⟶_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
            (a /✶₂ ρs₂ ↑✶₂ k) ⟶ (b /✶₂ ρs₂ ↑✶₂ k)
          ≡⟨ sym (TypeApp.⟶-/✶-↑✶ _ k ρs₂) ⟩
            (a ⟶ b) /✶₂ ρs₂ ↑✶₂ k
          ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (a →' b) = begin
            (a →' b) /✶₁ ρs₁ ↑✶₁ k
          ≡⟨ TypeApp.→'-/✶-↑✶ _ k ρs₁ ⟩
            (a /✶₁ ρs₁ ↑✶₁ k) →' (b /✶₁ ρs₁ ↑✶₁ k)
          ≡⟨ cong₂ _→'_ (/✶-↑✶ ρs₁ ρs₂ hyp k a) (/✶-↑✶ ρs₁ ρs₂ hyp k b) ⟩
            (a /✶₂ ρs₂ ↑✶₂ k) →' (b /✶₂ ρs₂ ↑✶₂ k)
          ≡⟨ sym (TypeApp.→'-/✶-↑✶ _ k ρs₂) ⟩
            (a →' b) /✶₂ ρs₂ ↑✶₂ k
          ∎
        /✶-↑✶ ρs₁ ρs₂ hyp k (∀' a) = begin
          (∀' a) /✶₁ ρs₁ ↑✶₁ k        ≡⟨ TypeApp.∀'-/✶-↑✶ _ k ρs₁ ⟩
          ∀' (a /✶₁ ρs₁ ↑✶₁ (1 + k))  ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (1 + k) a) ⟩
          ∀' (a /✶₂ ρs₂ ↑✶₂ (1 + k))  ≡⟨ sym (TypeApp.∀'-/✶-↑✶ _ k ρs₂) ⟩
          (∀' a) /✶₂ ρs₂ ↑✶₂ k        ∎

  module tpl = TermLemmas typeLemmas

  -- The above lemma /✶-↑✶ specialized to single substitutions
  /-↑⋆ : ∀ {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} →
         let open Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/₁_)
             open Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/₂_)
         in
         ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
         (∀ i x → tvar x /₁ ρ₁ ↑⋆₁ i ≡ tvar x /₂ ρ₂ ↑⋆₂ i) →
          ∀ i a → a /₁ ρ₁ ↑⋆₁ i ≡ a /₂ ρ₂ ↑⋆₂ i
  /-↑⋆ ρ₁ ρ₂ hyp i a = tpl./✶-↑✶ (ρ₁ ◅ ε) (ρ₂ ◅ ε) hyp i a

  open AdditionalLemmas typeLemmas public
  open tpl public

  /Var-/ : ∀ {ν μ} (t : Type ν) (s : Sub Fin ν μ) → t /Var s ≡ t / (map tvar s)
  /Var-/ (tc c) s = refl
  /Var-/ (tvar n) s = lookup⋆map s tvar n
  /Var-/ (a →' b) s = cong₂ _→'_ (/Var-/ a s) (/Var-/ b s)
  /Var-/ (a ⟶ b) s = cong₂ _⟶_ (/Var-/ a s) (/Var-/ b s)
  /Var-/ (∀' t) s = begin
    ∀' (t /Var (s Var.↑))
      ≡⟨ cong ∀' $ /Var-/ t (s Var.↑) ⟩
    ∀' (t / (map tvar $ s Var.↑))
      ≡⟨ cong (λ u → ∀' (t / u)) (map-var-↑ refl) ⟩
    ∀' t / (map tvar s) ∎

  a-/Var-varwk↑-/-sub0≡a : ∀ {n} (a : Type (suc n)) → (a /Var Var.wk Var.↑) / sub (tvar zero) ≡ a
  a-/Var-varwk↑-/-sub0≡a a = begin
    (a /Var Var.wk Var.↑) / (sub $ tvar zero)
      ≡⟨ cong (λ u → u / (sub $ tvar zero)) (/Var-/ a $ Var.wk Var.↑) ⟩
    (a / (map tvar $ Var.wk Var.↑)) / sub (tvar zero)
      ≡⟨ cong (λ u → (a / u) / (sub $ tvar zero)) (map-var-↑ map-var-varwk≡wk) ⟩
    (a / wk ↑) / (sub $ tvar zero)
      ≡⟨ a/wk↑/sub0≡a a ⟩
    a ∎

-- Lemmas about type substitutions in terms.
module TermTypeLemmas where
  open TermTypeSubst public

  private module T = TypeLemmas
  private module TS = TypeSubst
  private module V = VarLemmas

  /-↑⋆ :
    ∀ {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} →
    let open TS.Lifted lift₁ using () renaming (_↑⋆_ to _↑⋆₁_; _/_ to _/tp₁_)
        open   Lifted lift₁ using () renaming (_/_  to _/₁_)
        open TS.Lifted lift₂ using () renaming (_↑⋆_ to _↑⋆₂_; _/_ to _/tp₂_)
        open   Lifted lift₂ using () renaming (_/_  to _/₂_)
    in
    ∀ {n k} (ρ₁ : Sub T₁ n k) (ρ₂ : Sub T₂ n k) →
    (∀ i x → tvar x /tp₁ ρ₁ ↑⋆₁ i ≡ tvar x /tp₂ ρ₂ ↑⋆₂ i) →
     ∀ i {m} (t : Term (i + n) m)  → t /₁ ρ₁ ↑⋆₁ i ≡ t /₂ ρ₂ ↑⋆₂ i
  /-↑⋆ ρ₁ ρ₂ hyp i (var x)      = refl
  /-↑⋆ ρ₁ ρ₂ hyp i (Λ t)        = cong Λ      (/-↑⋆ ρ₁ ρ₂ hyp (1 + i) t)
  /-↑⋆ ρ₁ ρ₂ hyp i (λ' a t)     =
    cong₂ λ'     (T./-↑⋆ ρ₁ ρ₂ hyp i a)       (/-↑⋆ ρ₁ ρ₂ hyp i t)
  /-↑⋆ ρ₁ ρ₂ hyp i (t [ b ])    =
    cong₂ _[_]     (/-↑⋆ ρ₁ ρ₂ hyp i t)     (T./-↑⋆ ρ₁ ρ₂ hyp i b)
  /-↑⋆ ρ₁ ρ₂ hyp i (s · t)      =
    cong₂ _·_      (/-↑⋆ ρ₁ ρ₂ hyp i s)       (/-↑⋆ ρ₁ ρ₂ hyp i t)

  /-wk : ∀ {m n} (t : Term m n) → t / TypeSubst.wk ≡ weaken t
  /-wk t = /-↑⋆ TypeSubst.wk VarSubst.wk (λ k x → begin
    tvar x T./ T.wk T.↑⋆ k ≡⟨ T.var-/-wk-↑⋆ k x ⟩
    tvar (Fin.lift k suc x) ≡⟨ cong tvar (sym (V.var-/-wk-↑⋆ k x)) ⟩
    tvar (lookup x (V.wk V.↑⋆ k)) ≡⟨ refl ⟩
    tvar x TS./Var V.wk V.↑⋆ k ∎) 0 t

module CtxLemmas where
  open CtxSubst public

  private module Tp  = TypeLemmas
  private module Var = VarSubst

  -- Term variable substitution (renaming) commutes with type
  -- substitution.
  /Var-/ : ∀ {m ν n l} (ρ : Sub Fin m n) (Γ : Ctx ν n) (σ : Sub Type ν l) →
           (ρ /Var Γ) / σ ≡ ρ /Var (Γ / σ)
  /Var-/ ρ Γ σ = begin
      (ρ /Var Γ) / σ
    ≡⟨ sym (map-∘ _ _ ρ) ⟩
      map (λ x → (lookup x Γ) Tp./ σ) ρ
    ≡⟨ map-cong (λ x → sym (Tp.lookup-⊙ x)) ρ ⟩
      map (λ x → lookup x (Γ / σ)) ρ
    ∎

  -- Term variable substitution (renaming) commutes with weakening of
  -- typing contexts with an additional type variable.
  /Var-weaken : ∀ {m n k} (ρ : Sub Fin m k) (Γ : Ctx n k) →
                weaken (ρ /Var Γ) ≡ ρ /Var (weaken Γ)
  /Var-weaken ρ Γ = begin
    (ρ /Var Γ) / Tp.wk   ≡⟨ /Var-/ ρ Γ Tp.wk ⟩
    ρ /Var (weaken Γ)    ∎

  -- Term variable substitution (renaming) commutes with term variable
  -- lookup in typing context.
  /Var-lookup : ∀ {m n k} (x : Fin m) (ρ : Sub Fin m k) (Γ : Ctx n k) →
                lookup x (ρ /Var Γ) ≡ lookup (lookup x ρ) Γ
  /Var-lookup x ρ Γ = op-<$> (lookup-morphism x) _ _

  -- Term variable substitution (renaming) commutes with weakening of
  -- typing contexts with an additional term variable.
  /Var-∷ : ∀ {m n k} (a : Type n) (ρ : Sub Fin m k) (Γ : Ctx n k) →
           a ∷ (ρ /Var Γ) ≡ (ρ Var.↑) /Var (a ∷ Γ)
  /Var-∷ a []      Γ = refl
  /Var-∷ a (x ∷ ρ) Γ = cong (_∷_ a) (cong (_∷_ (lookup x Γ)) (begin
    map (λ x → lookup x Γ) ρ                   ≡⟨ refl ⟩
    map (λ x → lookup (suc x) (a ∷ Γ)) ρ       ≡⟨ map-∘ _ _ ρ ⟩
    map (λ x → lookup x (a ∷ Γ)) (map suc ρ)   ∎))

  -- Invariants of term variable substitution (renaming)
  idVar-/Var   : ∀ {m n} (Γ : Ctx n m) → Γ ≡ (Var.id /Var Γ)
  wkVar-/Var-∷ : ∀ {m n} (Γ : Ctx n m) (a : Type n) → Γ ≡ (Var.wk /Var (a ∷ Γ))

  idVar-/Var []      = refl
  idVar-/Var (a ∷ Γ) = cong (_∷_ a) (wkVar-/Var-∷ Γ a)

  wkVar-/Var-∷ Γ a = begin
    Γ ≡⟨ idVar-/Var Γ ⟩
    Var.id /Var Γ ≡⟨ map-∘ _ _ VarSubst.id ⟩
    Var.wk /Var (a ∷ Γ) ∎

  ctx-weaken-sub-vanishes : ∀ {ν n} {Γ : Ctx ν n} {a} → (ctx-weaken Γ) ctx/ (Tp.sub a) ≡ Γ
  ctx-weaken-sub-vanishes {Γ = Γ} {a} = begin
    (Γ ctx/ Tp.wk) ctx/ (Tp.sub a)
      ≡⟨ sym $ map-∘ (λ s → s tp/tp Tp.sub a) (λ s → s tp/tp Tp.wk) Γ ⟩
    (map (λ s → s tp/tp Tp.wk tp/tp (Tp.sub a)) Γ)
      ≡⟨ map-cong (TypeLemmas.wk-sub-vanishes) Γ ⟩
    (map (λ s → s) Γ) ≡⟨ map-id Γ ⟩
    Γ ∎

private
  ⊢subst : ∀ {m n} {Γ₁ Γ₂ : Ctx n m} {t₁ t₂ : Term n m} {a₁ a₂ : Type n} →
    Γ₁ ≡ Γ₂ → t₁ ≡ t₂ → a₁ ≡ a₂ → Γ₁ ⊢ t₁ ∈ a₁ → Γ₂ ⊢ t₂ ∈ a₂
  ⊢subst refl refl refl hyp = hyp

  ⊢substCtx : ∀ {m n} {Γ₁ Γ₂ : Ctx n m} {t : Term n m} {a : Type n} →
    Γ₁ ≡ Γ₂ → Γ₁ ⊢ t ∈ a → Γ₂ ⊢ t ∈ a
  ⊢substCtx refl hyp = hyp

  ⊢substTp : ∀ {m n} {Γ : Ctx n m} {t : Term n m} {a₁ a₂ : Type n} →
    a₁ ≡ a₂ → Γ ⊢ t ∈ a₁ → Γ ⊢ t ∈ a₂
  ⊢substTp refl hyp = hyp

module WtTypeLemmas where
  open TypeLemmas hiding (_/_; var; weaken)
  private
    module Tp = TypeLemmas
    module TmTp = TermTypeLemmas
    module C  = CtxLemmas

  infixl 8 _/_

  -- Type substitutions lifted to well-typed terms
  _/_ : ∀ {m n k} {Γ : Ctx n m} {t : Term n m} {a : Type n} →
        Γ ⊢ t ∈ a → (σ : Sub Type n k) → Γ C./ σ ⊢ t TmTp./ σ ∈ a Tp./ σ
  var x             / σ = ⊢substTp (lookup-⊙ x) (var x)
  _/_ {Γ = Γ} (Λ ⊢t)  σ = Λ (⊢substCtx eq (⊢t / σ ↑))
    where
      eq : (ctx-weaken Γ) C./ (σ Tp.↑) ≡ ctx-weaken (Γ C./ σ)
      eq = begin
        (map (λ s → s tp/tp Tp.wk) Γ) C./ (σ Tp.↑)
          ≡⟨ cong (λ a → a C./ (σ Tp.↑)) (map-cong (λ a → Tp./-wk {t = a}) Γ) ⟩
        (map Tp.weaken Γ) ⊙ (σ Tp.↑)
          ≡⟨ sym $ map-weaken-⊙ Γ σ ⟩
        map Tp.weaken (Γ ⊙ σ)
          ≡⟨ (map-cong (λ a → sym $ Tp./-wk {t = a}) (Γ ⊙ σ)) ⟩
        ctx-weaken (Γ C./ σ) ∎
  λ' a ⊢t           / σ = λ' (a Tp./ σ) (⊢t / σ)
  _[_] {a = a} ⊢t b / σ = ⊢substTp (sym (sub-commutes a)) ((⊢t / σ) [ b Tp./ σ ])
  ⊢s · ⊢t           / σ = (⊢s / σ) · (⊢t / σ)

  -- Weakening of terms with additional type variables lifted to
  -- well-typed terms.
  weaken : ∀ {m n} {Γ : Ctx n m} {t : Term n m} {a : Type n} →
           Γ ⊢ t ∈ a → ctx-weaken Γ ⊢ TmTp.weaken t ∈ Tp.weaken a
  weaken {t = t} {a = a} ⊢t = ⊢subst refl (TmTp./-wk t) (/-wk {t = a}) (⊢t / wk)

  -- Weakening of terms with additional type variables lifted to
  -- collections of well-typed terms.
  weakenAll : ∀ {m n k} {Γ : Ctx n m} {ts : Vec (Term n m) k}
                {as : Vec (Type n) k} → Γ ⊢ⁿ ts ∈ as →
                ctx-weaken Γ ⊢ⁿ map TmTp.weaken ts ∈ map Tp.weaken as
  weakenAll {ts = []}    {[]}    []         = []
  weakenAll {ts = _ ∷ _} {_ ∷ _} (⊢t ∷ ⊢ts) = weaken ⊢t ∷ weakenAll ⊢ts

  -- Shorthand for single-variable type substitutions in well-typed
  -- terms.
  _[/_] : ∀ {m n} {Γ : Ctx (1 + n) m} {t a} →
          Γ ⊢ t ∈ a → (b : Type n) → Γ C./ sub b ⊢ t TmTp./ sub b ∈ a Tp./ sub b
  ⊢t [/ b ] = ⊢t / sub b

  tm[/tp]-preserves : ∀ {ν n} {Γ : Ctx ν n} {t τ} → Γ ⊢ Λ t ∈ ∀' τ → ∀ a → Γ ⊢ (t tm[/tp a ]) ∈ τ tp[/tp a ]
  tm[/tp]-preserves {Γ = Γ} {t} {τ} (Λ p) a = ctx-subst C.ctx-weaken-sub-vanishes (p / (Tp.sub a))
    where
      ctx-subst = Prelude.subst (λ c → c ⊢ t tm[/tp a ] ∈ τ tp[/tp a ])

module WtTermLemmas where
  private
    module Tp  = TypeLemmas
    module TmTp  = TermTypeLemmas
    module TmTm  = TermTermSubst
    module Var = VarSubst
    module C   = CtxLemmas
    TmSub = TmTm.TermSub Term

  infix 4 _⇒_⊢_

  -- Well-typed term substitutions are collections of well-typed terms.
  _⇒_⊢_ : ∀ {ν m k} → Ctx ν m → Ctx ν k → TmSub ν m k → Set
  Γ ⇒ Δ ⊢ ρ = Δ ⊢ⁿ ρ ∈ Γ

  infixl 8  _/_ _/Var_
  infix  10 _↑

  -- Application of term variable substitutions (renaming) lifted to
  -- well-typed terms.
  _/Var_ : ∀ {m n k} {Γ : Ctx n k} {t : Term n m} {a : Type n}
             (ρ : Sub Fin m k) → ρ C./Var Γ ⊢ t ∈ a → Γ ⊢ t TmTm./Var ρ ∈ a
  _/Var_ {Γ = Γ} ρ (var x)   =
    ⊢substTp (sym (C./Var-lookup x ρ Γ)) (var (lookup x ρ))
  _/Var_ {Γ = Γ} ρ (Λ ⊢t)    =
    Λ    (ρ      /Var ⊢substCtx (C./Var-weaken ρ Γ) ⊢t)
  _/Var_ {Γ = Γ} ρ (λ' a ⊢t) =
    λ' a (ρ Var.↑ /Var ⊢substCtx (C./Var-∷ a ρ Γ) ⊢t)
  ρ /Var (⊢t [ b ])          = (ρ /Var ⊢t) [ b ]
  ρ /Var (⊢s · ⊢t)           = (ρ /Var ⊢s) · (ρ /Var ⊢t)

  -- Weakening of terms with additional term variables lifted to
  -- well-typed terms.
  weaken : ∀ {m n} {Γ : Ctx n m} {t : Term n m} {a b : Type n} →
           Γ ⊢ t ∈ a → b ∷ Γ ⊢ TmTm.weaken t ∈ a
  weaken {Γ = Γ} {b = b} ⊢t =
    Var.wk /Var ⊢substCtx (C.wkVar-/Var-∷ Γ b) ⊢t

  -- Weakening of terms with additional term variables lifted to
  -- collections of well-typed terms.
  weakenAll : ∀ {m n k} {Γ : Ctx n m} {ts : Vec (Term n m) k}
                {as : Vec (Type n) k} {b : Type n} →
              Γ ⊢ⁿ ts ∈ as → (b ∷ Γ) ⊢ⁿ map TmTm.weaken ts ∈ as
  weakenAll {ts = []}    {[]}    []         = []
  weakenAll {ts = _ ∷ _} {_ ∷ _} (⊢t ∷ ⊢ts) = weaken ⊢t ∷ weakenAll ⊢ts

  -- Lifting of well-typed term substitutions.
  _↑ : ∀ {m n k} {Γ : Ctx n m} {Δ : Ctx n k} {ρ b} →
       Γ ⇒ Δ ⊢ ρ → b ∷ Γ ⇒ b ∷ Δ ⊢ ρ TmTm.↑
  ⊢ρ ↑ = var zero ∷ weakenAll ⊢ρ

  -- The well-typed identity substitution.
  id : ∀ {m n} {Γ : Ctx n m} → Γ ⇒ Γ ⊢ TmTm.id
  id {zero}  {Γ = []}    = []
  id {suc m} {Γ = a ∷ Γ} = id ↑

  -- Well-typed weakening (as a substitution).
  wk : ∀ {m n} {Γ : Ctx n m} {a} → Γ ⇒ a ∷ Γ ⊢ TmTm.wk
  wk = weakenAll id

  -- A well-typed substitution which only replaces the first variable.
  sub : ∀ {m n} {Γ : Ctx n m} {t a} → Γ ⊢ t ∈ a → a ∷ Γ ⇒ Γ ⊢ TmTm.sub t
  sub ⊢t = ⊢t ∷ id

  -- Application of term substitutions lifted to well-typed terms
  _/_ : ∀ {m n k} {Γ : Ctx n m} {Δ : Ctx n k} {t a ρ} →
        Γ ⊢ t ∈ a → Γ ⇒ Δ ⊢ ρ → Δ ⊢ t TmTm./ ρ ∈ a
  var x       / ⊢ρ = lookup-⊢ x ⊢ρ
  _/_ {Γ = Γ} {Δ = Δ} {ρ = ρ} (Λ ⊢t) ⊢ρ = Λ (⊢t / weaken-⊢p)
    where
      weaken-⊢p : ctx-weaken Γ ⇒ ctx-weaken Δ ⊢ map TmTp.weaken ρ
      weaken-⊢p = (Prelude.subst
        (λ G → G ⇒ ctx-weaken Δ ⊢ map TmTp.weaken ρ) Tp.map-weaken (WtTypeLemmas.weakenAll ⊢ρ))
  λ' a ⊢t     / ⊢ρ = λ' a (⊢t / ⊢ρ ↑)
  (⊢t [ a ])  / ⊢ρ = (⊢t / ⊢ρ) [ a ]
  (⊢s · ⊢t)   / ⊢ρ = (⊢s / ⊢ρ) · (⊢t / ⊢ρ)

  -- Shorthand for well-typed single-variable term substitutions.
  _[/_] : ∀ {m n} {Γ : Ctx n m} {s t a b} →
          b ∷ Γ ⊢ s ∈ a → Γ ⊢ t ∈ b → Γ ⊢ s TmTm./ TmTm.sub t ∈ a
  ⊢s [/ ⊢t ] = ⊢s / sub ⊢t

  tm[/tm]-preserves : ∀ {ν n} {Γ : Ctx ν n} {t u a b} →
                      b ∷ Γ ⊢ t ∈ a → Γ ⊢ u ∈ b → Γ ⊢ (t tm[/tm u ]) ∈ a
  tm[/tm]-preserves ⊢s ⊢t = ⊢s / sub ⊢t

open WtTypeLemmas public using ()
  renaming (weaken to ⊢tp-weaken)
open WtTermLemmas public using ()
  renaming (_/_ to _⊢/tp_; _[/_] to _⊢[/_]; weaken to ⊢weaken)


text:
module Issue802b where

data I : Set where
  i : I

f : I → I
f i = i

mutual

  data P : I → Set where
    p : (x : I) → Q x x → P (f x)

  Q : I → I → Set
  Q i = P

g : (x y : I) → Q x y → P y
g i _ q = q

data R : (x : I) → P x → Set where
  r : (x : I) (q : Q x x) → R _ (g x _ q) → R (f x) (p x q)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Adjoint where

-- Adjoints

open import Level

open import Data.Product using (_,_; _×_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality using (Π; _⟶_)
import Function.Inverse as FI
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

-- be explicit in imports to 'see' where the information comes from
open import Categories.Category using (Category)
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Category.Instance.Setoids
open import Categories.Morphism
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Hom using (Hom[_][-,-])
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ₕ_; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
  renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; unitorˡ; unitorʳ; associator; _≃_)
import Categories.Morphism.Reasoning as MR

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

record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R

  field
    unit   : NaturalTransformation idF (R ∘F L)
    counit : NaturalTransformation (L ∘F R) idF

  module unit = NaturalTransformation unit
  module counit = NaturalTransformation counit

  field
    zig : ∀ {A : C.Obj} → counit.η (L.F₀ A) D.∘ L.F₁ (unit.η A) D.≈ D.id
    zag : ∀ {B : D.Obj} → R.F₁ (counit.η B) C.∘ unit.η (R.F₀ B) C.≈ C.id

  private
    variable
      A : C.Obj
      B : D.Obj

  Ladjunct : L.F₀ A D.⇒ B → A C.⇒ R.F₀ B
  Ladjunct f = R.F₁ f C.∘ unit.η _

  Radjunct : A C.⇒ R.F₀ B → L.F₀ A D.⇒ B
  Radjunct f = counit.η _ D.∘ L.F₁ f

  RLadjunct≈id : ∀ {f : L.F₀ A D.⇒ B} → Radjunct (Ladjunct f) D.≈ f
  RLadjunct≈id {f = f} = begin
    Radjunct (Ladjunct f)                            ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
    counit.η _ D.∘ L.F₁ (R.F₁ f) D.∘ L.F₁ (unit.η _) ≈⟨ pullˡ (counit.commute f) ⟩
    (f D.∘ counit.η _) D.∘ L.F₁ (unit.η _)           ≈⟨ pullʳ zig ⟩
    f D.∘ D.id                                       ≈⟨ D.identityʳ ⟩
    f                                                ∎
    where open D.HomReasoning
          open MR D

  LRadjunct≈id : ∀ {f : A C.⇒ R.F₀ B} → Ladjunct (Radjunct f) C.≈ f
  LRadjunct≈id {f = f} = begin
    Ladjunct (Radjunct f)                              ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
    (R.F₁ (counit.η _) C.∘ R.F₁ (L.F₁ f)) C.∘ unit.η _ ≈˘⟨ pushʳ (unit.commute f) ⟩
    R.F₁ (counit.η _) C.∘ unit.η _ C.∘ f               ≈⟨ pullˡ zag ⟩
    C.id C.∘ f                                         ≈⟨ C.identityˡ ⟩
    f                                                  ∎
    where open C.HomReasoning
          open MR C

  Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
  Hom[L-,-] = Hom[ D ][-,-] ∘F (L.op ⁂ idF)

  Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
  Hom[-,R-] = Hom[ C ][-,-] ∘F (idF ⁂ R)

  module Hom[L-,-] = Functor Hom[L-,-]
  module Hom[-,R-] = Functor Hom[-,R-]

  -- Inverse is more 'categorical' than bijection defined via injection/surjection
  Hom-inverse : ∀ A B → FI.Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
  Hom-inverse A B = record
    { to = record
      { _⟨$⟩_ = Ladjunct {A} {B}
      ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
      }
    ; from = record
      { _⟨$⟩_ = Radjunct {A} {B}
      ; cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
      }
    ; inverse-of = record
      { left-inverse-of = λ _ → RLadjunct≈id
      ; right-inverse-of = λ _ → LRadjunct≈id
      }
    }

  module Hom-inverse {A} {B} = FI.Inverse (Hom-inverse A B)

  op : Adjoint R.op L.op
  op = record
    { unit   = counit.op
    ; counit = unit.op
    ; zig    = zag
    ; zag    = zig
    }

  -- naturality condition on the two hom functors.
  -- these conditions are separated out because a complication due to the
  -- universe level in Agda.
  module _ where
    open C
    open HomReasoning
    open MR C

    Ladjunct-comm : ∀ {X Y A B} {h i : L.F₀ X D.⇒ Y} {f : A ⇒ X} {g : Y D.⇒ B} →
                      h D.≈ i →
                      R.F₁ (g D.∘ h D.∘ L.F₁ f) ∘ unit.η A ≈ R.F₁ g ∘ (R.F₁ i ∘ unit.η X) ∘ f
    Ladjunct-comm {X} {Y} {A} {B} {h} {i} {f} {g} eq = begin
      R.F₁ (g D.∘ h D.∘ L.F₁ f) ∘ unit.η A         ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
      (R.F₁ g ∘ R.F₁ (h D.∘ L.F₁ f)) ∘ unit.η A    ≈⟨ (refl⟩∘⟨ R.homomorphism) ⟩∘⟨refl ⟩
      (R.F₁ g ∘ R.F₁ h ∘ R.F₁ (L.F₁ f)) ∘ unit.η A ≈⟨ pullʳ assoc ⟩
      R.F₁ g ∘ R.F₁ h ∘ R.F₁ (L.F₁ f) ∘ unit.η A   ≈˘⟨ refl⟩∘⟨ ⟺ (R.F-resp-≈ eq) ⟩∘⟨ unit.commute f ⟩
      R.F₁ g ∘ R.F₁ i ∘ unit.η X ∘ f               ≈˘⟨ refl⟩∘⟨ assoc ⟩
      R.F₁ g ∘ (R.F₁ i ∘ unit.η X) ∘ f             ∎

    Ladjunct-comm′ : ∀ {X A B} {f : A ⇒ X} {g : L.F₀ X D.⇒ B} →
                      Ladjunct (g D.∘ L.F₁ f) ≈ Ladjunct g ∘ f
    Ladjunct-comm′ = ∘-resp-≈ˡ R.homomorphism ○ (pullʳ (⟺ (unit.commute _))) ○ ⟺ assoc

    Ladjunct-resp-≈ : ∀ {A B} {f g : L.F₀ A D.⇒ B} → f D.≈ g → Ladjunct f ≈ Ladjunct g
    Ladjunct-resp-≈ eq = ∘-resp-≈ˡ (R.F-resp-≈ eq)

  module _ where
    open D
    open HomReasoning
    open MR D

    Radjunct-comm : ∀ {X Y A B} {h i : X C.⇒ R.F₀ Y} {f : A C.⇒ X} {g : Y ⇒ B} →
                      h C.≈ i →
                      counit.η B ∘ L.F₁ (R.F₁ g C.∘ h C.∘ f) ≈ g ∘ (counit.η Y ∘ L.F₁ i) ∘ L.F₁ f
    Radjunct-comm {X} {Y} {A} {B} {h} {i} {f} {g} eq = begin
      counit.η B ∘ L.F₁ (R.F₁ g C.∘ h C.∘ f)       ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
      counit.η B ∘ L.F₁ (R.F₁ g) ∘ L.F₁ (h C.∘ f)  ≈⟨ pullˡ (counit.commute g) ⟩
      (g ∘ counit.η Y) ∘ L.F₁ (h C.∘ f)            ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
      (g ∘ counit.η Y) ∘ L.F₁ h ∘ L.F₁ f           ≈⟨ refl ⟩∘⟨ L.F-resp-≈ eq ⟩∘⟨ refl ⟩
      (g ∘ counit.η Y) ∘ L.F₁ i ∘ L.F₁ f           ≈⟨ pullʳ (⟺ assoc) ⟩
      g ∘ (counit.η Y ∘ L.F₁ i) ∘ L.F₁ f           ∎

    Radjunct-comm′ : ∀ {Y A B} {f : A C.⇒ R.F₀ Y} {g : Y ⇒ B} →
                      Radjunct (R.F₁ g C.∘ f) ≈ g ∘ Radjunct f
    Radjunct-comm′ = ∘-resp-≈ʳ L.homomorphism ○ pullˡ (counit.commute _) ○ assoc

    Radjunct-resp-≈ : ∀ {A B} {f g : A C.⇒ R.F₀ B} → f C.≈ g → Radjunct f ≈ Radjunct g
    Radjunct-resp-≈ eq = ∘-resp-≈ʳ (L.F-resp-≈ eq)

  -- a complication: the two hom functors do not live in the same Setoids,
  -- so they need to be mapped to the same Setoids first before establishing
  -- natural isomorphism!
  module _ where
    private
      levelℓ : Category o ℓ e → Level
      levelℓ {ℓ = ℓ} _ = ℓ

      levele : Category o ℓ e → Level
      levele {e = e} _ = e

    Hom[L-,-]′ : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-]′ = LiftSetoids (levelℓ C) (levele C) ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-]′ : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-]′ = LiftSetoids (levelℓ D) (levele D) ∘F Hom[ C ][-,-] ∘F (idF ⁂ R)

    Hom-NI : NaturalIsomorphism Hom[L-,-]′ Hom[-,R-]′
    Hom-NI = record
      { F⇒G = ntHelper record
        { η       = λ _ → record
          { _⟨$⟩_ = λ f → lift (Ladjunct (lower f))
          ; cong  = λ eq → lift (Ladjunct-resp-≈ (lower eq))
          }
        ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq)
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → record
          { _⟨$⟩_ = λ f → lift (Radjunct (lower f))
          ; cong  = λ eq → lift (Radjunct-resp-≈ (lower eq))
          }
        ; commute = λ _ eq → lift $ Radjunct-comm (lower eq)
        }
      ; iso = λ X → record
        { isoˡ = λ eq → let open D.HomReasoning in lift (RLadjunct≈id ○ lower eq)
        ; isoʳ = λ eq → let open C.HomReasoning in lift (LRadjunct≈id ○ lower eq)
        }
      }

  module Hom-NI = NaturalIsomorphism Hom-NI

infix 5 _⊣_
_⊣_ = Adjoint

-- a special case of the natural isomorphism in which homsets in C and D have the same
-- universe level. therefore there is no need to lift Setoids to the saem level.
-- this is helpful when combining with Yoneda lemma.
module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R : Functor D C} where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R

  module _ (adjoint : L ⊣ R) where
    open Adjoint adjoint

    -- in this case, the hom functors are naturally isomorphism directly
    Hom-NI′ : NaturalIsomorphism Hom[L-,-] Hom[-,R-]
    Hom-NI′ = record
      { F⇒G = ntHelper record
        { η       = λ _ → Hom-inverse.to
        ; commute = λ _ eq → Ladjunct-comm eq
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → Hom-inverse.from
        ; commute = λ _ eq → Radjunct-comm eq
        }
      ; iso = λ _ → record
        { isoˡ = λ eq → let open D.HomReasoning in RLadjunct≈id ○ eq
        ; isoʳ = λ eq → let open C.HomReasoning in LRadjunct≈id ○ eq
        }
      }

  -- now goes from natural isomorphism back to adjoint.
  -- for simplicity, just construct the case in which homsetoids of C and D
  -- are compatible.

  private
    Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-] = Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-] = Hom[ C ][-,-] ∘F (idF ⁂ R)

  module _ (Hni : NaturalIsomorphism Hom[L-,-] Hom[-,R-]) where
    open NaturalIsomorphism Hni
    open NaturalTransformation
    open Functor
    open Π

    private
      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
      unitη X = ⇒.η (X , L.F₀ X)

      unit : NaturalTransformation idF (R ∘F L)
      unit = ntHelper record
        { η       = λ X → unitη X ⟨$⟩ D.id
        ; commute = λ {X} {Y} f → begin
          (unitη Y ⟨$⟩ D.id) ∘ f                             ≈⟨ introˡ R.identity ⟩
          R.F₁ D.id ∘ (unitη Y  ⟨$⟩ D.id) ∘ f                ≈˘⟨ ⇒.commute (f , D.id) D.Equiv.refl ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ (D.id D.∘ D.id D.∘ L.F₁ f)    ≈⟨ cong (⇒.η (X , L.F₀ Y)) (D.Equiv.trans D.identityˡ D.identityˡ) ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ L.F₁ f                        ≈⟨ cong (⇒.η (X , L.F₀ Y)) (MR.introʳ D (MR.elimʳ D L.identity)) ⟩
          ⇒.η (X , L.F₀ Y) ⟨$⟩ (L.F₁ f D.∘ D.id D.∘ L.F₁ id) ≈⟨ ⇒.commute (C.id , L.F₁ f) D.Equiv.refl ⟩
          R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id) ∘ id            ≈⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (L.F₁ f) ∘ (unitη X ⟨$⟩ D.id)                 ∎
        }
        where open C
              open HomReasoning
              open MR C

      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
      counitη X = ⇐.η (R.F₀ X , X)

      counit : NaturalTransformation (L ∘F R) idF
      counit = ntHelper record
        { η       = λ X → counitη X ⟨$⟩ C.id
        ; commute = λ {X} {Y} f → begin
          (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)               ≈˘⟨ identityˡ ⟩
          id ∘ (counitη Y ⟨$⟩ C.id) ∘ L.F₁ (R.F₁ f)          ≈˘⟨ ⇐.commute (R.F₁ f , D.id) C.Equiv.refl ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ R.F₁ f) ≈⟨ cong (⇐.η (R.F₀ X , Y)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ R.F₁ f                        ≈⟨ cong (⇐.η (R.F₀ X , Y)) (MR.introʳ C C.identityˡ) ⟩
          ⇐.η (R.F₀ X , Y) ⟨$⟩ (R.F₁ f C.∘ C.id C.∘ C.id)    ≈⟨ ⇐.commute (C.id , f) C.Equiv.refl ⟩
          f ∘ (counitη X ⟨$⟩ C.id) ∘ L.F₁ C.id               ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
          f ∘ (counitη X ⟨$⟩ C.id)                           ∎
        }
        where open D
              open HomReasoning
              open MR D

    Hom-NI⇒Adjoint : L ⊣ R
    Hom-NI⇒Adjoint = record
      { unit   = unit
      ; counit = counit
      ; zig    = λ {A} →
        let open D
            open HomReasoning
            open MR D
        in begin
          η counit (L.F₀ A) ∘ L.F₁ (η unit A)      ≈˘⟨ identityˡ ⟩
          id ∘ η counit (L.F₀ A) ∘ L.F₁ (η unit A) ≈˘⟨ ⇐.commute (η unit A , id) C.Equiv.refl ⟩
          ⇐.η (A , L.F₀ A) ⟨$⟩ (R.F₁ id C.∘ C.id C.∘ η unit A)
                                                   ≈⟨ cong (⇐.η (A , L.F₀ A)) (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ) ⟩
          ⇐.η (A , L.F₀ A) ⟨$⟩ η unit A            ≈⟨ isoˡ refl ⟩
          id
                                                   ∎
      ; zag    = λ {B} →
        let open C
            open HomReasoning
            open MR C
        in begin
          R.F₁ (η counit B) ∘ η unit (R.F₀ B)      ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (η counit B) ∘ η unit (R.F₀ B) ∘ id ≈˘⟨ ⇒.commute (id , η counit B) D.Equiv.refl ⟩
          ⇒.η (R.F₀ B , B) ⟨$⟩ (η counit B D.∘ D.id D.∘ L.F₁ id)
                                                   ≈⟨ cong (⇒.η (R.F₀ B , B)) (MR.elimʳ D (MR.elimʳ D L.identity)) ⟩
          ⇒.η (R.F₀ B , B) ⟨$⟩ η counit B          ≈⟨ isoʳ refl ⟩
          id                                       ∎
      }
      where module i {X} = Iso (iso X)
            open i

-- the general case from isomorphic Hom setoids to adjoint functors
module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D} {R : Functor D C} where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R
    open Functor
    open Π

    Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-] = LiftSetoids ℓ e ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-] = LiftSetoids ℓ′ e′ ∘F Hom[ C ][-,-] ∘F (idF ⁂ R)

  module _ (Hni : Hom[L-,-] ≃ Hom[-,R-]) where
    open NaturalIsomorphism Hni
    private
      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
      unitη X = ⇒.η (X , L.F₀ X)

      unit : NaturalTransformation idF (R ∘F L)
      unit = ntHelper record
        { η       = λ X → lower (unitη X ⟨$⟩ lift D.id)
        ; commute = λ {X Y} f → begin
          lower (unitη Y ⟨$⟩ lift D.id) ∘ f
            ≈⟨ introˡ R.identity ⟩
          R.F₁ D.id ∘ lower (unitη Y ⟨$⟩ lift D.id) ∘ f
            ≈˘⟨ lower (⇒.commute (f , D.id) (lift D.Equiv.refl)) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (D.id D.∘ D.id D.∘ L.F₁ f))
            ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (D.Equiv.trans D.identityˡ D.identityˡ))) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f))
            ≈⟨ lower (cong (⇒.η (X , L.F₀ Y)) (lift (MR.introʳ D (MR.elimʳ D L.identity)))) ⟩
          lower (⇒.η (X , L.F₀ Y) ⟨$⟩ lift (L.F₁ f D.∘ D.id D.∘ L.F₁ id))
            ≈⟨ lower (⇒.commute (C.id , L.F₁ f) (lift D.Equiv.refl)) ⟩
          R.F₁ (L.F₁ f) ∘ lower (⇒.η (X , L.F₀ X) ⟨$⟩ lift D.id) ∘ id
            ≈⟨ refl⟩∘⟨ identityʳ ⟩
          F₁ (R ∘F L) f ∘ lower (unitη X ⟨$⟩ lift D.id)                ∎
        }
        where open C
              open HomReasoning
              open MR C

      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
      counitη X = ⇐.η (R.F₀ X , X)

      counit : NaturalTransformation (L ∘F R) idF
      counit = ntHelper record
        { η       = λ X → lower (counitη X ⟨$⟩ lift C.id)
        ; commute = λ {X} {Y} f → begin
          lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
            ≈˘⟨ identityˡ ⟩
          id ∘ lower (⇐.η (R.F₀ Y , Y) ⟨$⟩ lift C.id) ∘ L.F₁ (R.F₁ f)
            ≈˘⟨ lower (⇐.commute (R.F₁ f , D.id) (lift C.Equiv.refl)) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ R.F₁ f))
            ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f))
            ≈⟨ lower (cong (⇐.η (R.F₀ X , Y)) (lift (MR.introʳ C C.identityˡ))) ⟩
          lower (⇐.η (R.F₀ X , Y) ⟨$⟩ lift (R.F₁ f C.∘ C.id C.∘ C.id))
            ≈⟨ lower (⇐.commute (C.id , f) (lift C.Equiv.refl)) ⟩
          f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id) ∘ L.F₁ C.id
            ≈⟨ refl⟩∘⟨ elimʳ L.identity ⟩
          f ∘ lower (⇐.η (R.F₀ X , X) ⟨$⟩ lift C.id)
            ∎
        }
        where open D
              open HomReasoning
              open MR D

    Hom-NI′⇒Adjoint : L ⊣ R
    Hom-NI′⇒Adjoint = record
      { unit   = unit
      ; counit = counit
      ; zig    = λ {A} →
        let open D
            open HomReasoning
            open MR D
        in begin
          lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
            ≈˘⟨ identityˡ ⟩
          id ∘ lower (counitη (L.F₀ A) ⟨$⟩ lift C.id) ∘ L.F₁ (η unit A)
            ≈˘⟨ lower (⇐.commute (η unit A , id) (lift C.Equiv.refl)) ⟩
          lower (⇐.η (A , L.F₀ A) ⟨$⟩ lift (R.F₁ id C.∘ C.id C.∘ lower (⇒.η (A , L.F₀ A) ⟨$⟩ lift id)))
            ≈⟨ lower (cong (⇐.η (A , L.F₀ A)) (lift (C.Equiv.trans (MR.elimˡ C R.identity) C.identityˡ))) ⟩
          lower (⇐.η (A , L.F₀ A) ⟨$⟩ (⇒.η (A , L.F₀ A) ⟨$⟩ lift id))
            ≈⟨ lower (isoˡ (lift refl)) ⟩
          id ∎
      ; zag    = λ {B} →
        let open C
            open HomReasoning
            open MR C
        in begin
          R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id)
            ≈˘⟨ refl⟩∘⟨ identityʳ ⟩
          R.F₁ (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)) ∘ lower (⇒.η (R.F₀ B , L.F₀ (R.F₀ B)) ⟨$⟩ lift D.id) ∘ id
            ≈˘⟨ lower (⇒.commute (id , η counit B) (lift D.Equiv.refl)) ⟩
          lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id) D.∘ D.id D.∘ L.F₁ id))
            ≈⟨ lower (cong (⇒.η (R.F₀ B , B)) (lift (MR.elimʳ D (MR.elimʳ D L.identity)))) ⟩
          lower (⇒.η (R.F₀ B , B) ⟨$⟩ lift (lower (⇐.η (R.F₀ B , B) ⟨$⟩ lift id)))
            ≈⟨ lower (isoʳ (lift refl)) ⟩
          id ∎
      }
      where open NaturalTransformation
            module _ {X} where
              open Iso (iso X) public

⊣-id : idF {C = C} ⊣ idF {C = C}
⊣-id {C = C} = record
  { unit   = F⇐G unitorˡ
  ; counit = F⇒G unitorʳ
  ; zig    = identityˡ
  ; zag    = identityʳ
  }
  where open Category C
        open NaturalIsomorphism

-- Adjoints compose; we can't be sloppy, so associators and unitors must be inserted.
-- Use single letters in pairs, so L & M on the left, and R & S on the right
_∘⊣_ : {L : Functor C D} {R : Functor D C} {M : Functor D E} {S : Functor E D} →
  L ⊣ R → M ⊣ S → (M ∘F L) ⊣ (R ∘F S)
_∘⊣_ {C = C} {D = D} {E = E} {L = L} {R} {M} {S} LR MS = record
  { unit =  ((F⇐G (associator _ S R) ∘ᵥ R ∘ˡ (F⇒G (associator L M S))) ∘ᵥ
            (R ∘ˡ (MSη′ ∘ʳ L)) ∘ᵥ (R ∘ˡ (F⇐G unitorˡ))) ∘ᵥ LRη′
  ; counit = MSε′ ∘ᵥ (((F⇒G (unitorʳ {F = M}) ∘ʳ S) ∘ᵥ ((M ∘ˡ LRε′) ∘ʳ S)) ∘ᵥ
             (F⇒G (associator R L M) ∘ʳ S) ) ∘ᵥ F⇐G (associator S R (M ∘F L) )
  ; zig = λ {A} → zig′ {A}
  ; zag = λ {B} → zag′ {B}
  }
  where
    open Functor
    open NaturalTransformation
    open NaturalIsomorphism
    module LR = Adjoint LR renaming (unit to LRη′; counit to LRε′)
    module MS = Adjoint MS renaming (unit to MSη′; counit to MSε′)
    module LRη = NaturalTransformation (Adjoint.unit LR) renaming (η to ηLR)
    module MSη = NaturalTransformation (Adjoint.unit MS) renaming (η to ηMS)
    module LRε = NaturalTransformation (Adjoint.counit LR) renaming (η to εLR)
    module MSε = NaturalTransformation (Adjoint.counit MS) renaming (η to εMS)
    module C = Category C
    module D = Category D
    module E = Category E
    module L = Functor L renaming (F₀ to L₀; F₁ to L₁)
    module M = Functor M renaming (F₀ to M₀; F₁ to M₁)
    module R = Functor R renaming (F₀ to R₀; F₁ to R₁)
    module S = Functor S renaming (F₀ to S₀; F₁ to S₁)
    open LR; open MS; open LRη; open LRε; open MSε; open MSη; open L; open M; open R; open S

    zig′ : {A : C.Obj} → (εMS (M₀ (L₀ A)) E.∘
       ((E.id E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))))) E.∘ E.id) E.∘ E.id)
      E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      E.≈ E.id
    -- use "inverted" format here, where rules are out-dented
    zig′ {A} = begin
        (εMS (M₀ (L₀ A)) E.∘ ((E.id E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))))) E.∘ E.id) E.∘ E.id)
        E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      ≈⟨  ( refl⟩∘⟨ (E.identityʳ ○ E.identityʳ ○ E.identityˡ)) ⟩∘⟨refl ⟩  -- get rid of those pesky E.id
        (εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A)))))
        E.∘ M₁ (L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
      ≈⟨ E.assoc ○ E.∘-resp-≈ʳ (⟺ M.homomorphism) ⟩
        εMS (M₀ (L₀ A)) E.∘
        M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ A)) C.∘ R₁ D.id) C.∘ ηLR A))
         -- below: get rid of lots of pesky id. Nasty bit of nested equational reasoning, but nothing deep
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ʳ (L.F-resp-≈
             (C.∘-resp-≈ˡ (C.∘-resp-≈ C.identityˡ (C.∘-resp-≈ʳ R.identity) C.HomReasoning.○
                let _⊚_ = C.HomReasoning._○_ in C.∘-resp-≈ R.identity C.identityʳ ⊚ C.identityˡ)))) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ ((R₁ (ηMS (L₀ A))) C.∘ ηLR A))
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ʳ L.homomorphism) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (R₁ (ηMS (L₀ A))) D.∘ L₁ (ηLR A))
      ≈˘⟨  refl⟩∘⟨ M.F-resp-≈ D.assoc ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ ((εLR (S₀ (M₀ (L₀ A))) D.∘ L₁ (R₁ (ηMS (L₀ A)))) D.∘ L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ M.F-resp-≈ (D.∘-resp-≈ˡ (LRε.commute _)) ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ ( (_ D.∘ εLR _) D.∘ L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ M.homomorphism ⟩
        εMS (M₀ (L₀ A)) E.∘ M₁ (_ D.∘ εLR _) E.∘ M₁ (L₁ (ηLR A))
      ≈⟨  refl⟩∘⟨ ( M.homomorphism ⟩∘⟨refl ) ⟩
        εMS (M₀ (L₀ A)) E.∘ (M₁ (ηMS (L₀ A)) E.∘ M₁ (εLR _)) E.∘ M₁ (L₁ (ηLR A))
      ≈˘⟨ E.assoc ○ E.∘-resp-≈ʳ (⟺ E.assoc) ⟩
        (εMS (M₀ (L₀ A)) E.∘ M₁ (ηMS (L₀ A))) E.∘ (M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A)))
      ≈⟨ MS.zig ⟩∘⟨refl ⟩
        E.id E.∘ (M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A)))
      ≈⟨ E.identityˡ ⟩
        M₁ (εLR _) E.∘ M₁ (L₁ (ηLR A))
      ≈˘⟨ M.homomorphism ⟩
        M₁ (εLR _ D.∘ L₁ (ηLR A))
      ≈⟨ M.F-resp-≈ LR.zig ○ M.identity ⟩
        E.id ∎
      where open E.HomReasoning

    zag′ : {B : E.Obj} → R₁ (S₁ (εMS B E.∘ ((E.id E.∘ M₁ (εLR (S₀ B))) E.∘ E.id) E.∘ E.id))
      C.∘ ((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ R₁ D.id) C.∘
      ηLR (R₀ (S₀ B)) C.≈ C.id
    zag′ {B} =
      let _⊚_ = E.HomReasoning._○_ in
      begin
         R₁ (S₁ (εMS B E.∘ ((E.id E.∘ M₁ (εLR (S₀ B))) E.∘ E.id) E.∘ E.id))
          C.∘ ((C.id C.∘ R₁ D.id) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ R₁ D.id) C.∘
          ηLR (R₀ (S₀ B)) -- get rid of all those id
      ≈⟨ R.F-resp-≈ (S.F-resp-≈ (E.∘-resp-≈ʳ (E.identityʳ ⊚ (E.identityʳ ⊚ E.identityˡ)))) ⟩∘⟨
         C.∘-resp-≈ˡ (C.∘-resp-≈ C.identityˡ (C.∘-resp-≈ʳ R.identity) ○
          C.∘-resp-≈ R.identity C.identityʳ ○ C.identityˡ) ⟩
         R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B)))) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈˘⟨ C.assoc ⟩
         (R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B)))) C.∘ R₁ (ηMS (L₀ (R₀ (S₀ B))))) C.∘ ηLR (R₀ (S₀ B))
      ≈˘⟨  R.homomorphism ⟩∘⟨refl ⟩
         R₁ (S₁ (εMS B E.∘ M₁ (εLR (S₀ B))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ˡ S.homomorphism) ⟩∘⟨refl ⟩
        R₁ ((S₁ (εMS B) D.∘ (S₁ (M₁ (εLR (S₀ B))))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ D.assoc ⟩∘⟨refl ⟩
        R₁ (S₁ (εMS B) D.∘ S₁ (M₁ (εLR (S₀ B))) D.∘ ηMS (L₀ (R₀ (S₀ B)))) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ʳ (D.HomReasoning.⟺ (MSη.commute (εLR (S₀ B))))) ⟩∘⟨refl ⟩
         R₁ (S₁ (εMS B) D.∘ ηMS (S₀ B) D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈˘⟨ R.F-resp-≈ D.assoc ⟩∘⟨refl ⟩
         R₁ ((S₁ (εMS B) D.∘ ηMS (S₀ B)) D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ R.F-resp-≈ (D.∘-resp-≈ˡ MS.zag) ⟩∘⟨refl ⟩
         R₁ (D.id D.∘ εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ C.∘-resp-≈ˡ (R.F-resp-≈ D.identityˡ) ⟩
         R₁ (εLR (S₀ B)) C.∘ ηLR (R₀ (S₀ B))
      ≈⟨ LR.zag ⟩
         C.id ∎
      where open C.HomReasoning

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories