text:
open import Oscar.Prelude
open import Oscar.Class.IsPrecategory
open import Oscar.Class.IsCategory
open import Oscar.Class.Category
open import Oscar.Class.IsFunctor
open import Oscar.Class.Functor

open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity
open import Oscar.Class.Surjection
open import Oscar.Class.Smap
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.Surjidentity
open import Oscar.Class

module Oscar.Class.Kitten where

productCat : ∀ {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} → Category 𝔬₁ 𝔯₁ ℓ₁ → Category 𝔬₂ 𝔯₂ ℓ₂ → Category (𝔬₁ ∙̂ 𝔬₂) (𝔯₁ ∙̂ 𝔯₂) (ℓ₁ ∙̂ ℓ₂)
Category.𝔒 (productCat c₁ c₂) = Category.𝔒 c₁ × Category.𝔒 c₂
Category._∼_ (productCat c₁ c₂) (x₁ , x₂) (y₁ , y₂) = Category._∼_ c₁ x₁ y₁ × Category._∼_ c₂ x₂ y₂
Category._∼̇_ (productCat c₁ c₂) {x₁ , x₂} {y₁ , y₂} (f₁ , g₁) (f₂ , g₂) = Category._∼̇_ c₁ f₁ f₂ × Category._∼̇_ c₂ g₁ g₂
Category.category-ε (productCat c₁ c₂) = (Category.category-ε c₁) , (Category.category-ε c₂)
Category._↦_ (productCat c₁ c₂) (f₁ , f₂) (g₁ , g₂) = (Category._↦_ c₁ f₁ g₁) , (Category._↦_ c₂ f₂ g₂)
Category.`IsCategory (productCat c₁ c₂) .IsCategory.`IsPrecategory .IsPrecategory.`𝓣ransextensionality .⋆ (x₁ , y₁) (x₂ , y₂) = transextensionality x₁ x₂ , transextensionality y₁ y₂
Category.`IsCategory (productCat c₁ c₂) .IsCategory.`IsPrecategory .IsPrecategory.`𝓣ransassociativity .⋆ f g h = transassociativity (f .π₀) (g .π₀) (h .π₀) , transassociativity (f .π₁) (g .π₁) (h .π₁)
Category.`IsCategory (productCat c₁ c₂) .IsCategory.`𝓣ransleftidentity .⋆ = transleftidentity , transleftidentity
Category.`IsCategory (productCat c₁ c₂) .IsCategory.`𝓣ransrightidentity = ∁ (transrightidentity , transrightidentity)

record AFunctor {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂} (source : Category 𝔬₁ 𝔯₁ ℓ₁) (target : Category 𝔬₂ 𝔯₂ ℓ₂) : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
  constructor ∁
  private module S = Category source
  private module T = Category target
  field
    F₀ : S.𝔒 → T.𝔒
    F₁ : Smap.type S._∼_ T._∼_ F₀ F₀
    isFunctor : IsFunctor S._∼_ S._∼̇_ S.category-ε S._↦_ T._∼_ T._∼̇_ T.category-ε T._↦_ F₁

record MonoidalCategory 𝔬 𝔯 ℓ : Ø ↑̂ (𝔬 ∙̂ 𝔯 ∙̂ ℓ) where
  constructor ∁
  field
    thecat : Category 𝔬 𝔯 ℓ
    thefunc : AFunctor (productCat thecat thecat) thecat
  O : Ø 𝔬
  O = Category.𝔒 thecat
  field
    𝟏 : O
  _⟶_ : O → O → Ø 𝔯
  _⟶_ = Category._∼_ thecat
  _⊗_ : O → O → O
  _⊗_ = λ x y → AFunctor.F₀ thefunc (x , y)
  _⨂_ : ∀ {w x y z} → w ⟶ x → y ⟶ z → (w ⊗ y) ⟶ (x ⊗ z)
  _⨂_ f g = AFunctor.F₁ thefunc (f , g)
  _↦_ : ∀ {x y z} (f : x ⟶ y) (g : y ⟶ z) → x ⟶ z
  _↦_ = Category._↦_ thecat
  i : ∀ {x} → x ⟶ x
  i = Category.category-ε thecat
  _≈̇_ = Category._∼̇_ thecat
  -- infixr 9 _⊗_
  field
    associator : ∀ (x y z : O)
                 → Σ (((x ⊗ y) ⊗ z) ⟶ (x ⊗ (y ⊗ z))) λ f
                 → Σ ((x ⊗ (y ⊗ z)) ⟶ ((x ⊗ y) ⊗ z)) λ f⁻¹
                 → ((f ↦ f⁻¹) ≈̇ i) × ((f⁻¹ ↦ f) ≈̇ i)
    left-unitor : ∀ (x : O)
                  → Σ ((𝟏 ⊗ x) ⟶ x) λ f
                  → Σ (x ⟶ (𝟏 ⊗ x)) λ f⁻¹
                  → ((f ↦ f⁻¹) ≈̇ i) × ((f⁻¹ ↦ f) ≈̇ i)
    right-unitor : ∀ (x : O)
                   → Σ ((x ⊗ 𝟏) ⟶ x) λ f
                   → Σ (x ⟶ (x ⊗ 𝟏)) λ f⁻¹
                   → ((f ↦ f⁻¹) ≈̇ i) × ((f⁻¹ ↦ f) ≈̇ i)
  assoc : ∀ (x y z : O) → ((x ⊗ y) ⊗ z) ⟶ (x ⊗ (y ⊗ z))
  assoc x y z = π₀ (associator x y z)
  ru : ∀ x → (x ⊗ 𝟏) ⟶ x
  ru x = π₀ (right-unitor x)
  lu : ∀ x → (𝟏 ⊗ x) ⟶ x
  lu x = π₀ (left-unitor x)
  field
    triangle-identity : ∀ (x y : O)
                        → (ru x ⨂ i) ≈̇ (assoc x 𝟏 y ↦ (i ⨂ lu y))
    pentagon-identity : ∀ (w x y z : O)
      → (((assoc w x y ⨂ i) ↦ assoc w (x ⊗ y) z) ↦ (i ⨂ assoc x y z))
      ≈̇ (assoc (w ⊗ x) y z ↦ assoc w x (y ⊗ z))

module _
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
  (source : MonoidalCategory 𝔬₁ 𝔯₁ ℓ₁)
  (target : MonoidalCategory 𝔬₂ 𝔯₂ ℓ₂)
  where
  record LaxMonoidalFunctor : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
    module C = MonoidalCategory source
    module D = MonoidalCategory target
    field
      𝓕 : AFunctor C.thecat D.thecat
    open AFunctor 𝓕 public
    field
      e : D.𝟏 D.⟶ F₀ C.𝟏
      μ : ∀ x y → (F₀ x D.⊗ F₀ y) D.⟶ F₀ (x C.⊗ y) -- F A → F B → F (A × B)
      associativity : ∀ x y z
        → ((μ x y D.⨂ D.i) D.↦ (μ (x C.⊗ y) z D.↦ F₁ (C.assoc x y z)))
              D.≈̇
          (D.assoc (F₀ x) (F₀ y) (F₀ z) D.↦ ((D.i D.⨂ μ y z) D.↦ μ x (y C.⊗ z)))
      left-unitality : ∀ x → (D.lu (F₀ x)) D.≈̇ ((e D.⨂ D.i) D.↦ (μ C.𝟏 x D.↦ F₁ (C.lu x)))
      right-unitality : ∀ x → (D.ru (F₀ x)) D.≈̇ ((D.i D.⨂ e) D.↦ (μ x C.𝟏 D.↦ F₁ (C.ru x)))

module _
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
  (source : MonoidalCategory 𝔬₁ 𝔯₁ ℓ₁)
  (target : MonoidalCategory 𝔬₂ 𝔯₂ ℓ₂)
  (let module C = MonoidalCategory source)
  (let module D = MonoidalCategory target)
  (𝓕 : AFunctor C.thecat D.thecat)
  (open AFunctor 𝓕)
  (e : D.𝟏 D.⟶ F₀ C.𝟏)
  (μ : ∀ x y → (F₀ x D.⊗ F₀ y) D.⟶ F₀ (x C.⊗ y))
  where
  record IsLaxMonoidalFunctor : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
    field
      associativity : ∀ x y z
        → ((μ x y D.⨂ D.i) D.↦ (μ (x C.⊗ y) z D.↦ F₁ (C.assoc x y z)))
              D.≈̇
          (D.assoc (F₀ x) (F₀ y) (F₀ z) D.↦ ((D.i D.⨂ μ y z) D.↦ μ x (y C.⊗ z)))
      left-unitality : ∀ x → (D.lu (F₀ x)) D.≈̇ ((e D.⨂ D.i) D.↦ (μ C.𝟏 x D.↦ F₁ (C.lu x)))
      right-unitality : ∀ x → (D.ru (F₀ x)) D.≈̇ ((D.i D.⨂ e) D.↦ (μ x C.𝟏 D.↦ F₁ (C.ru x)))

record GenericApplicativeRaw
  {lc ld} {Oc : Ø lc} {Od : Ø ld}
  (F : Oc → Od)
  (1c : Oc) (1d : Od)
  (_⊗c_ : Oc → Oc → Oc) (_⊗d_ : Od → Od → Od)
  {ℓc} (_⟶c_ : Oc → Oc → Ø ℓc)
  {ℓd} (_⟶d_ : Od → Od → Ø ℓd)
  : Ø ℓd ∙̂ lc ∙̂ ℓc
  where
  field
    m : ∀ {x y} → x ⟶c y → F x ⟶d F y -- fmap
    e : 1d ⟶d F 1c -- pure
    μ : ∀ {x y} → (F x ⊗d F y) ⟶d F (x ⊗c y) -- apply

  -- _<*>_ : ∀ {x y : Oc} → ? → ? → {!!} --  F (x ⟶c y) → F x ⟶d F y
  -- _<*>_ f x = m ? (μ )

{-
  _<*>_ : ∀ {A B} → F (A → B) → F A → F B
  _<*>_ f x = sfmap (λ {(f , x) → f x}) (f <s> x)
-}

{-
record ContainedGenericApplicativeRaw
  {lc ld} {Oc : Ø lc} {Od : Ø ld}
  (F : Oc → Od)
  (1c : Oc) (1d : Od)
  (_⊗c_ : Oc → Oc → Oc) (_⊗d_ : Od → Od → Od)
  {ℓd} (_⟶d_ : Od → Od → Ø ℓd)
  : Ø ℓd ∙̂ lc
  where
  field
    e : 1d ⟶d F 1c
    μ : ∀ {x y} → (F x ⊗d F y) ⟶d F (x ⊗c y)
-}
open import Oscar.Data.𝟙
open import Oscar.Data.Proposequality

record Action {a b} {A : Set a} {B : Set b} {f g h} (F : A → B → Set f) (G : A → Set g) (H : B → Set h) : Ø a ∙̂ b ∙̂ f ∙̂ g ∙̂ h where
  field
    act : ∀ {x y} → F x y → G x → H y

record SetApplyM {a b} (F : Set a → Set b)
  -- (𝟏ᴬ : Set a) (𝟏ᴮ : Set b) (_⊕_ : Set p → Set p → Set p) (_⟶_ : A → A → Set ℓ)
  : Ø ↑̂ a ∙̂ b where
  field
    sfmap : ∀ {A B} → (A → B) → F A → F B
    sunit : Lift {_} {a} 𝟙 → F (Lift 𝟙)
    _<s>_ : ∀ {A B} → F A → F B → F (A × B)
  _<*>_ : ∀ {A B} → F (A → B) → F A → F B
  _<*>_ f x = sfmap (λ {(f , x) → f x}) (f <s> x)
  _⨂_ : ∀ {A B C D : Ø a} → (A → B) → (C → D) → A × C → B × D
  _⨂_ f g ac = let (a , c) = ac in f a , g c
  assoc : ∀ {A B C : Ø a} → A × (B × C) → (A × B) × C
  assoc abc = let (a , (b , c)) = abc in (a , b) , c
  field
    law-nat : ∀ {A B C D} (f : A → B) (g : C → D) u v → sfmap (f ⨂ g) (u <s> v) ≡ (sfmap f u <s> sfmap g v)
    leftid : ∀ {B} (v : F B) → sfmap π₁ (sunit _ <s> v) ≡ v
    righttid : ∀ {A} (u : F A) → sfmap π₀ (u <s> sunit _) ≡ u
    associativity : ∀ {A B C} u v w → sfmap (assoc {A} {B} {C}) (u <s> (v <s> w)) ≡ ((u <s> v) <s> w)

  source-cat : MonoidalCategory _ _ _
  source-cat .MonoidalCategory.thecat .Category.𝔒 = Ø a
  source-cat .MonoidalCategory.thecat .Category._∼_ = Function
  source-cat .MonoidalCategory.thecat .Category._∼̇_ = _≡̇_
  source-cat .MonoidalCategory.thecat .Category.category-ε = ¡
  source-cat .MonoidalCategory.thecat .Category._↦_ = flip _∘′_
  source-cat .MonoidalCategory.thecat .Category.`IsCategory = {!!}
  source-cat .MonoidalCategory.thefunc .AFunctor.F₀ (A , B) = A × B
  source-cat .MonoidalCategory.thefunc .AFunctor.F₁ = {!!}
  source-cat .MonoidalCategory.thefunc .AFunctor.isFunctor = {!!}
  source-cat .MonoidalCategory.𝟏 = Lift 𝟙
  source-cat .MonoidalCategory.associator = {!!}
  source-cat .MonoidalCategory.left-unitor = {!!}
  source-cat .MonoidalCategory.right-unitor = {!!}
  source-cat .MonoidalCategory.triangle-identity = {!!}
  source-cat .MonoidalCategory.pentagon-identity = {!!}

  target-cat : MonoidalCategory _ _ _
  target-cat .MonoidalCategory.thecat .Category.𝔒 = Ø b
  target-cat .MonoidalCategory.thecat .Category._∼_ = Function
  target-cat .MonoidalCategory.thecat .Category._∼̇_ = _≡̇_
  target-cat .MonoidalCategory.thecat .Category.category-ε = ¡
  target-cat .MonoidalCategory.thecat .Category._↦_ = flip _∘′_
  target-cat .MonoidalCategory.thecat .Category.`IsCategory = {!!}
  target-cat .MonoidalCategory.thefunc .AFunctor.F₀ (A , B) = A × B
  target-cat .MonoidalCategory.thefunc .AFunctor.F₁ = {!!}
  target-cat .MonoidalCategory.thefunc .AFunctor.isFunctor = {!!}
  target-cat .MonoidalCategory.𝟏 = Lift 𝟙
  target-cat .MonoidalCategory.associator = {!!}
  target-cat .MonoidalCategory.left-unitor = {!!}
  target-cat .MonoidalCategory.right-unitor = {!!}
  target-cat .MonoidalCategory.triangle-identity = {!!}
  target-cat .MonoidalCategory.pentagon-identity = {!!}

  module C = MonoidalCategory source-cat
  module D = MonoidalCategory target-cat

  the-functor : AFunctor C.thecat D.thecat
  the-functor .AFunctor.F₀ = F
  the-functor .AFunctor.F₁ = sfmap
  the-functor .AFunctor.isFunctor = {!!}

  open AFunctor the-functor

  the-e : D.𝟏 D.⟶ F₀ C.𝟏 -- F (Lift 𝟙)
  the-e = {!!}

  the-μ : ∀ x y → (F₀ x D.⊗ F₀ y) D.⟶ F₀ (x C.⊗ y) -- F A → F B → F (A × B)
  the-μ A B (FA , FB) = FA <s> FB

toSetApply : ∀ {a b} (F : Set a → Set b) (gar : GenericApplicativeRaw F (Lift 𝟙) (Lift 𝟙) (λ A B → A × B) (λ A B → A × B) Function Function) → SetApplyM F
toSetApply F gar .SetApplyM.sfmap = GenericApplicativeRaw.m gar
toSetApply F gar .SetApplyM.sunit _ = GenericApplicativeRaw.e gar !
toSetApply F gar .SetApplyM._<s>_ FA FB = GenericApplicativeRaw.μ gar (FA , FB)
toSetApply F gar .SetApplyM.law-nat = {!!}
toSetApply F gar .SetApplyM.leftid = {!!}
toSetApply F gar .SetApplyM.righttid = {!!}
toSetApply F gar .SetApplyM.associativity = {!!}

module _
  {𝔬₁ 𝔯₁ ℓ₁ 𝔬₂ 𝔯₂ ℓ₂}
  (C : MonoidalCategory 𝔬₁ 𝔯₁ ℓ₁)
  (D : MonoidalCategory 𝔬₂ 𝔯₂ ℓ₂)
  where
  record LaxMonoidalFunctorWithStrength : Ø 𝔬₁ ∙̂ 𝔯₁ ∙̂ ℓ₁ ∙̂ 𝔬₂ ∙̂ 𝔯₂ ∙̂ ℓ₂ where
    field
      laxMonoidalFunctor : LaxMonoidalFunctor C D
    open LaxMonoidalFunctor laxMonoidalFunctor
    {-
    field
      β : ∀ v w → (v D.⊗ F₀ w) D.⟶ F₀ (v C.⊗ w)
      commute-5 : ∀ u v w → (C.assoc u v (F₀ w) C.↦ ((C.i C.⨂ β v w) C.↦ β u (v C.⊗ w))) C.≈̇ (β (u C.⊗ v) w C.↦ F₁ (C.assoc u v w))
      commute-3 : ∀ v → C.lu (F₀ v) C.≈̇ (β C.𝟏 v C.↦ F₁ (C.lu v))
      -- strength : TensorialStrength C (LaxMonoidalFunctor.𝓕 laxMonoidalEndofunctor)
    -}

module _ {𝔬 𝔯 ℓ} (V : MonoidalCategory 𝔬 𝔯 ℓ) (let C = MonoidalCategory.thecat V) (F : AFunctor C C) where
  open MonoidalCategory V
  open AFunctor F
  record TensorialStrength : Ø 𝔬 ∙̂ 𝔯 ∙̂ ℓ where
    field
      β : ∀ v w → (v ⊗ F₀ w) ⟶ F₀ (v ⊗ w)
      commute-5 : ∀ u v w → (assoc u v (F₀ w) ↦ ((i ⨂ β v w) ↦ β u (v ⊗ w))) ≈̇ (β (u ⊗ v) w ↦ F₁ (assoc u v w))
      commute-3 : ∀ v → lu (F₀ v) ≈̇ (β 𝟏 v ↦ F₁ (lu v))

module _
  {𝔬 𝔯 ℓ}
  (C : MonoidalCategory 𝔬 𝔯 ℓ)
  where
  record LaxMonoidalEndofunctorWithStrength : Ø 𝔬 ∙̂ 𝔯 ∙̂ ℓ where
    field
      laxMonoidalEndofunctor : LaxMonoidalFunctor C C
      strength : TensorialStrength C (LaxMonoidalFunctor.𝓕 laxMonoidalEndofunctor)

{- want parameters :
  X : Set a
  Y : Set b
  X₀ : X
  F : X → Y
  _⨁_ : X → X → Set a

  LaxMonoidalFunctor.e = unit : F X₀
  LaxMonoidalFunctor.μ = apply : ∀ {A B : X} → F A → F B → F (A ⨁ B)
  LaxMonoidalFunctor.𝓕.F₀ = F : X → Y

-}

record GenericApplyM {a ℓ} {A : Set a} (F : A → A) (𝟏 : A) (_⊕_ : A → A → A) (_⟶_ : A → A → Set ℓ) : Ø a ∙̂ ℓ where
  field
    gunit : 𝟏 ⟶ F 𝟏
    gproduct : ∀ {x y : A} → (F x ⊕ F y) ⟶ F (x ⊕ y)

open import Oscar.Data.𝟙
-- open import Oscar.Class.Kitten
open import Oscar.Class.Category
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.IsCategory
open import Oscar.Class.IsPrecategory
open import Oscar.Property.Category.Function
open import Oscar.Class
open import Oscar.Class.Fmap
import Oscar.Class.Reflexivity.Function

module _
  {𝔬₁ 𝔬₂} (𝓕 : Ø 𝔬₁ → Ø 𝔬₂)
  (fmapper : Fmap 𝓕)
  (fpure : ∀ {𝔄} → 𝔄 → 𝓕 𝔄)
  (fapply : ∀ {𝔄 𝔅} → 𝓕 (𝔄 → 𝔅) → 𝓕 𝔄 → 𝓕 𝔅)
  where
  -- instance _ = fmapper
  fmap' = λ {A B} (f : A → B) → fapply (fpure f)
  mkProductMonoidalCategory : MonoidalCategory _ _ _
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category.𝔒 = Ø 𝔬₁
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category._∼_ = MFunction 𝓕
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category._∼̇_ = Proposextensequality
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category.category-ε = ε
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category._↦_ = (flip _∘′_)
  mkProductMonoidalCategory .MonoidalCategory.thecat .Category.`IsCategory = ?
  mkProductMonoidalCategory .MonoidalCategory.thefunc .AFunctor.F₀ (A , B) = A × B
  mkProductMonoidalCategory .MonoidalCategory.thefunc .AFunctor.F₁ (f , g) xy = fapply (fmap' _,_ (f (fmap' π₀ xy))) (g (fmap' π₁ xy))
  mkProductMonoidalCategory .MonoidalCategory.thefunc .AFunctor.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjtranscommutativity = {!!}
  mkProductMonoidalCategory .MonoidalCategory.thefunc .AFunctor.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjextensionality = {!!}
  mkProductMonoidalCategory .MonoidalCategory.thefunc .AFunctor.isFunctor .IsFunctor.`𝒮urjidentity = {!!}
  mkProductMonoidalCategory .MonoidalCategory.𝟏 = {!!}
  mkProductMonoidalCategory .MonoidalCategory.associator = {!!}
  mkProductMonoidalCategory .MonoidalCategory.left-unitor = {!!}
  mkProductMonoidalCategory .MonoidalCategory.right-unitor = {!!}
  mkProductMonoidalCategory .MonoidalCategory.triangle-identity = {!!}
  mkProductMonoidalCategory .MonoidalCategory.pentagon-identity = {!!}

record HApplicativeFunctor {𝔬₁ 𝔬₂} (𝓕 : Ø 𝔬₁ → Ø 𝔬₂) : Ø (↑̂ (↑̂ 𝔬₁ ∙̂ 𝔬₂)) where
  constructor ∁
  field
    fmapper : Fmap 𝓕
    fpure : ∀ {𝔄} → 𝔄 → 𝓕 𝔄
    fapply : ∀ {𝔄 𝔅} → 𝓕 (𝔄 → 𝔅) → 𝓕 𝔄 → 𝓕 𝔅

  field
    isStrongLaxMonoidalEndofunctor : LaxMonoidalEndofunctorWithStrength (mkProductMonoidalCategory 𝓕 fmapper fpure fapply)

  module LMF = LaxMonoidalFunctor (LaxMonoidalEndofunctorWithStrength.laxMonoidalEndofunctor isStrongLaxMonoidalEndofunctor)
  derive-fpure : ∀ {𝔄} → 𝔄 → 𝓕 𝔄
  derive-fpure = {!LMF!} where

  {-
    ⦃ isFunctor ⦄ : IsFunctor
                       {𝔒₁ = Ø 𝔬₁} (λ A B → A × 𝓕 B)
                         {!(λ { {A} {B} (x₁ , f₁) (x₂ , f₂) → {!(x₁ ≡ x₂) × !}})!} (λ {A} → {!!} , {!!}) {!!}
                       {𝔒₂ = Ø 𝔬₁} {!!}
                         {!!} {!!} {!!}
                       {!!}
  -}

record MonoidalFunctor {𝔬₁ 𝔬₂} (𝓕 : Ø 𝔬₁ → Ø 𝔬₂) : Ø (↑̂ (↑̂ 𝔬₁ ∙̂ 𝔬₂)) where
  constructor ∁
  field
    ⦃ isFmap ⦄ : Fmap 𝓕
    unit : 𝓕 (Lift 𝟙)
    mappend : ∀ {𝔄 𝔅} → 𝓕 𝔄 → 𝓕 𝔅 → 𝓕 (𝔄 × 𝔅)
    {-
    ⦃ isFunctor ⦄ : IsFunctor
                       Function⟦ 𝔬₁ ⟧
                         Proposextensequality ε (flip _∘′_)
                       (MFunction 𝓕)
                         Proposextensequality ε (flip _∘′_)
                       {!!}
    -}
  pure : ∀ {𝔄} → 𝔄 → 𝓕 𝔄
  pure x = fmap (x ∞) unit

  infixl 4 _<*>_
  _<*>_ : ∀ {𝔄 𝔅} → 𝓕 (𝔄 → 𝔅) → 𝓕 𝔄 → 𝓕 𝔅
  f <*> x = fmap (λ {(f , x) → f x}) (mappend f x)

  app-identity : ∀ {𝔄} (v : 𝓕 𝔄) → (pure ¡[ 𝔄 ] <*> v) ≡ v
  app-identity v = {!!}

open MonoidalFunctor ⦃ … ⦄ public using (unit; mappend)

-- record ApplicativeFunctor where
module Purity
  {𝔵₁ 𝔵₂ 𝔯} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂} (F : 𝔛₁ → 𝔛₂) (x₁ : 𝔛₁) (x₂ : 𝔛₂) (_⟶_ : 𝔛₂ → 𝔛₂ → Ø 𝔯)
  = ℭLASS (F , x₁ , x₂ , _⟶_) (x₂ ⟶ F x₁)

module Applicativity
  {𝔵₁ 𝔵₂ 𝔯} {𝔛₁ : Ø 𝔵₁} {𝔛₂ : Ø 𝔵₂} (F : 𝔛₁ → 𝔛₂) (_⊗₁_ : 𝔛₁ → 𝔛₁ → 𝔛₁) (_⊗₂_ : 𝔛₂ → 𝔛₂ → 𝔛₂) (_⟶_ : 𝔛₂ → 𝔛₂ → Ø 𝔯)
  = ℭLASS (F , _⊗₁_ , _⊗₂_ , _⟶_) (∀ x y → (F x ⊗₂ F y) ⟶ F (x ⊗₁ y))

-- FunctionalMonoidalCategory

AFunctorFunction²Function : ∀ {𝔬₁} → AFunctor (productCat (CategoryFunction {𝔬₁}) (CategoryFunction {𝔬₁})) (CategoryFunction {𝔬₁})
AFunctorFunction²Function .AFunctor.F₀ = uncurry _×_
AFunctorFunction²Function .AFunctor.F₁ (f₁ , f₂) (x₁ , x₂) = f₁ x₁ , f₂ x₂
AFunctorFunction²Function .AFunctor.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjtranscommutativity = {!!}
AFunctorFunction²Function .AFunctor.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjextensionality = {!!}
AFunctorFunction²Function .AFunctor.isFunctor .IsFunctor.`𝒮urjidentity = {!!}

record LMF {𝔬₁ 𝔬₂} (𝓕 : Ø 𝔬₁ → Ø 𝔬₂) ⦃ _ : Fmap 𝓕 ⦄ : Ø ↑̂ (↑̂ 𝔬₁ ∙̂ 𝔬₂) where
  constructor ∁
  field
    lmf-pure : Purity.type 𝓕 (Lift 𝟙) (Lift 𝟙) Function
    lmf-apply : Applicativity.type 𝓕 _×_ _×_ Function

  lmf-happly : ∀ {𝔄 𝔅} → 𝓕 (𝔄 → 𝔅) → 𝓕 𝔄 → 𝓕 𝔅
  lmf-happly f x = fmap (λ {(f , x) → f x}) (lmf-apply _ _ (f , x))

  field
    ⦃ islmf ⦄ : IsLaxMonoidalFunctor (∁ CategoryFunction (∁ (uncurry _×_) {!!} {!!}) (Lift 𝟙) {!!} {!!} {!!} {!!} {!!}) (∁ CategoryFunction (∁ (uncurry _×_) {!!} {!!}) ((Lift 𝟙)) {!!} {!!} {!!} {!!} {!!}) (record { F₀ = 𝓕 ; F₁ = fmap ; isFunctor = ∁ ⦃ {!!} ⦄ ⦃ ! ⦄ ⦃ ! ⦄ ⦃ {!!} ⦄  }) lmf-pure lmf-apply


text:
open import Common.Prelude renaming (Nat to ℕ)
open import Common.Reflect

module StrangeRecursiveUnquote where

`ℕ : Term
`ℕ = def (quote ℕ) []

-- the term f n is stuck and so we cannot unquote (as expected)
f : ℕ → Term
f zero    = `ℕ
f (suc n) = unquote (f n)

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record R : Set where
  field
    r1 r2 : Nat

test : (x : R) → R.r1 x ≡ 0 → Nat
test x refl = 0

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Syntax of pure type systems (PTS)
------------------------------------------------------------------------

module Pts.Syntax where

open import Data.Fin using (Fin)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Fin.Substitution.Typed
open import Data.Star using (Star; ε; _◅_)
open import Data.Nat using (ℕ; suc; _+_)
open import Data.Vec using (lookup)
open import Relation.Binary.PropositionalEquality as PropEq
open PropEq.≡-Reasoning

-- All submodules are parametrized by a given set of sorts.
module _ (Sort : Set) where

  ----------------------------------------------------------------------
  -- Abstract syntax of terms

  module Syntax where

    infixl 9 _·_

    -- Untyped terms with up to n free variables.
    data Term (n : ℕ) : Set where
      var  : (x : Fin n)                     → Term n  -- variable
      sort : (s : Sort)                      → Term n  -- sort
      Π    : (a : Term n) (b : Term (1 + n)) → Term n  -- dependent product
      ƛ    : (a : Term n) (b : Term (1 + n)) → Term n  -- abstraction
      _·_  : (a b : Term n)                  → Term n  -- application

  open Syntax

  ----------------------------------------------------------------------
  -- Substitutions in terms

  -- Application of generic substitutions to terms
  module SubstApp {T} (l : Lift T Term) where
    open Lift l

    infixl 8 _/_

    -- Apply a substitution to a term.
    _/_ : ∀ {m n} → Term m → Sub T m n → Term n
    var x  / σ = lift (lookup x σ)
    sort s / σ = sort s
    Π a b  / σ = Π (a / σ) (b / σ ↑)
    ƛ a b  / σ = ƛ (a / σ) (b / σ ↑)
    a · b  / σ = (a / σ) · (b / σ)

    -- Some helper lemmas about applying sequences of substitutions.
    -- To be used in PathSubstLemmas.

    open Application (record { _/_ = _/_ }) hiding (_/_)

    -- Sorts are invariant under substitution.
    sort-/✶-↑✶ : ∀ k {m n s} (σs : Subs T m n) → sort s /✶ σs ↑✶ k ≡ sort s
    sort-/✶-↑✶ k ε        = refl
    sort-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (sort-/✶-↑✶ k σs) refl

    -- Substitutions in dependent product types are compositional.
    Π-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
                  (Π a b) /✶ σs ↑✶ k ≡  Π (a /✶ σs ↑✶ k) (b /✶ σs ↑✶ suc k)
    Π-/✶-↑✶ k ε        = refl
    Π-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (Π-/✶-↑✶ k σs) refl

    -- Substitutions in abstractions are compositional.
    ƛ-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
                  (ƛ a b) /✶ σs ↑✶ k ≡  ƛ (a /✶ σs ↑✶ k) (b /✶ σs ↑✶ suc k)
    ƛ-/✶-↑✶ k ε        = refl
    ƛ-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (ƛ-/✶-↑✶ k σs) refl

    -- Substitutions in applications are compositional.
    ·-/✶-↑✶ : ∀ k {m n a b} (σs : Subs T m n) →
                  (a · b) /✶ σs ↑✶ k ≡ (a /✶ σs ↑✶ k) · (b /✶ σs ↑✶ k)
    ·-/✶-↑✶ k ε        = refl
    ·-/✶-↑✶ k (σ ◅ σs) = cong₂ _/_ (·-/✶-↑✶ k σs) refl

  -- Substitutions in terms and associated lemmas.
  module Substitution where

    -- Term substitutions.
    termSubst : TermSubst Term
    termSubst = record { var = var; app = SubstApp._/_ }

    -- Lemmas relating application of sequences of generic substitutions
    -- lifted to any number of additional variables.
    --
    -- Using these generic lemmas, we can instantiate the record
    -- Data.Fin.Substitution.Lemmas.TermLemmas below, which gives access
    -- to a number of useful (derived) lemmas about path substitutions.
    module Lemmas {T₁ T₂} {lift₁ : Lift T₁ Term} {lift₂ : Lift T₂ Term} where
      open SubstApp
      open Lift lift₁ using () renaming (_↑✶_ to _↑✶₁_)
      open Lift lift₂ using () renaming (_↑✶_ to _↑✶₂_)
      open Application (record { _/_ = SubstApp._/_ lift₁ }) using ()
        renaming (_/✶_ to _/✶₁_)
      open Application (record { _/_ = SubstApp._/_ lift₂ }) using ()
        renaming (_/✶_ to _/✶₂_)

      -- Sequences of (lifted) T₁ and T₂-substitutions are equivalent
      -- when applied to terms if they are equivalent when applied to
      -- variables.
      /✶-↑✶ : ∀ {m n} (σs₁ : Subs T₁ m n) (σs₂ : Subs T₂ m n) →
                (∀ k x → var x /✶₁ σs₁ ↑✶₁ k ≡ var x /✶₂ σs₂ ↑✶₂ k) →
                 ∀ k t → t     /✶₁ σs₁ ↑✶₁ k ≡ t     /✶₂ σs₂ ↑✶₂ k
      /✶-↑✶ σs₁ σs₂ hyp k (var x)  = hyp k x
      /✶-↑✶ σs₁ σs₂ hyp k (sort s) = begin
        sort s /✶₁ σs₁ ↑✶₁ k   ≡⟨ sort-/✶-↑✶ _ k σs₁ ⟩
        sort s                 ≡⟨ sym (sort-/✶-↑✶ _ k σs₂) ⟩
        sort s /✶₂ σs₂ ↑✶₂ k   ∎
      /✶-↑✶ σs₁ σs₂ hyp k (Π a b) = begin
          (Π a b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ Π-/✶-↑✶ _ k σs₁ ⟩
          Π (a /✶₁ σs₁ ↑✶₁ k) (b /✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ Π (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp (suc k) b) ⟩
          Π (a /✶₂ σs₂ ↑✶₂ k) (b /✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (Π-/✶-↑✶ _ k σs₂) ⟩
          (Π a b) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (ƛ a b) = begin
          (ƛ a b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ƛ-/✶-↑✶ _ k σs₁ ⟩
          ƛ (a /✶₁ σs₁ ↑✶₁ k) (b /✶₁ σs₁ ↑✶₁ suc k)
        ≡⟨ cong₂ ƛ (/✶-↑✶ σs₁ σs₂ hyp k a) (/✶-↑✶ σs₁ σs₂ hyp (suc k) b) ⟩
          ƛ (a /✶₂ σs₂ ↑✶₂ k) (b /✶₂ σs₂ ↑✶₂ suc k)
        ≡⟨ sym (ƛ-/✶-↑✶ _ k σs₂) ⟩
          (ƛ a b) /✶₂ σs₂ ↑✶₂ k
        ∎
      /✶-↑✶ σs₁ σs₂ hyp k (a · b) = begin
          (a · b) /✶₁ σs₁ ↑✶₁ k
        ≡⟨ ·-/✶-↑✶ _ 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 (·-/✶-↑✶ _ k σs₂) ⟩
          (a · b) /✶₂ σs₂ ↑✶₂ k
        ∎

    -- By instantiating TermLemmas, we get access to a number of useful
    -- (derived) lemmas about path substitutions.
    termLemmas : TermLemmas Term
    termLemmas = record
      { termSubst = termSubst
      ; app-var   = refl
      ; /✶-↑✶     = Lemmas./✶-↑✶
      }

    open TermLemmas termLemmas public hiding (var; termSubst)

    -- By instantiating TermLikeLemmas, we get access to a number of
    -- useful (derived) lemmas about variable substitutions (renamings).
    private
      termLikeLemmas : TermLikeLemmas Term Term
      termLikeLemmas = record
        { app        = SubstApp._/_
        ; termLemmas = termLemmas
        ; /✶-↑✶₁     = Lemmas./✶-↑✶
        ; /✶-↑✶₂     = Lemmas./✶-↑✶
        }

    open TermLikeLemmas termLikeLemmas public
      using (varLiftAppLemmas; varLiftSubLemmas; _/Var_)

    infix 10 _[_]

    -- Shorthand for single-variable term substitutions.
    _[_] : ∀ {n} → Term (1 + n) → Term n → Term n
    a [ b ] = a / sub b

  ----------------------------------------------------------------------
  -- Concrete typing contexts over terms.

  module Ctx where
    open Substitution using (weaken)
    open Context      Term public hiding (module Ctx)

    weakenOps : WeakenOps
    weakenOps = record { weaken = weaken }

    open WeakenOps weakenOps public hiding (weaken)

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
module Structure.Setoid.Uniqueness where

import      Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Type

private variable ℓₗ ℓₗ₁ ℓₗ₂ : Lvl.Level

module _ {ℓ₁}{ℓ₂} where
  -- Definition of uniqueness of a property.
  -- This means that there is at most one element that satisfies this property.
  -- This is similiar to "Injective" for functions.
  Unique : ∀{Obj : Type{ℓ₁}}{ℓₗ} → ⦃ equiv : Equiv{ℓₗ}(Obj) ⦄ → (Pred : Obj → Stmt{ℓ₂}) → Stmt
  Unique {Obj = Obj} Pred = ∀{x y : Obj} → Pred(x) → Pred(y) → (x ≡ y)

  -- Definition of existence of an unique element satisfying a property.
  -- This means that there is one and only one element that satisfies this property.
  ∃! : ∀{Obj : Type{ℓ₁}}{ℓₗ} → ⦃ equiv : Equiv{ℓₗ}(Obj) ⦄ → (Pred : Obj → Stmt{ℓ₂}) → Stmt
  ∃! {Obj} Pred = ∃(Pred) ∧ Unique(Pred)

  [∃!]-intro : ∀{T} → ⦃ _ : Equiv{ℓₗ}(T) ⦄ → ∀{property} → ∃(property) → Unique{T}(property) → ∃!(property)
  [∃!]-intro = [∧]-intro

  [∃!]-existence : ∀{Obj} → ⦃ _ : Equiv{ℓₗ}(Obj) ⦄ → ∀{Pred} → ∃!{Obj}(Pred) → ∃(Pred)
  [∃!]-existence  = [∧]-elimₗ

  [∃!]-uniqueness : ∀{Obj} → ⦃ _ : Equiv{ℓₗ}(Obj) ⦄ → ∀{Pred} → ∃!{Obj}(Pred) → Unique(Pred)
  [∃!]-uniqueness = [∧]-elimᵣ

  [∃!]-witness : ∀{Obj} → ⦃ _ : Equiv{ℓₗ}(Obj) ⦄ → ∀{Pred} → ∃!{Obj}(Pred) → Obj
  [∃!]-witness e = [∃]-witness ([∃!]-existence e)

  [∃!]-proof : ∀{Obj} → ⦃ _ : Equiv{ℓₗ}(Obj) ⦄ → ∀{Pred} → (e : ∃!{Obj}(Pred)) → Pred([∃!]-witness(e))
  [∃!]-proof e = [∃]-proof ([∃!]-existence e)

  [∃!]-existence-eq : ∀{T} → ⦃ _ : Equiv{ℓₗ}(T) ⦄ → ∀{P} → (e : ∃!(P)) → ∀{x} → P(x) → (x ≡ [∃!]-witness e)
  [∃!]-existence-eq e {x} px = [∃!]-uniqueness e {x} {[∃!]-witness e} px ([∃!]-proof e)

  [∃!]-existence-eq-any : ∀{T} → ⦃ _ : Equiv{ℓₗ}(T) ⦄ → ∀{P} → (e : ∃!(P)) → ∀{x} → P(x) → ([∃!]-witness e ≡ x)
  [∃!]-existence-eq-any e {x} px = [∃!]-uniqueness e {[∃!]-witness e} {x} ([∃!]-proof e) px

  -- TODO: [∃!]-equivalence {T} property = ∃(a ↦ ∃{property(a)}(pa ↦ pa ∧ Uniqueness{T}(property){a}(pa)))

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:
------------------------------------------------------------------------
-- Some χ program combinators
------------------------------------------------------------------------

module Combinators where

open import Equality.Propositional
open import Prelude hiding (id; if_then_else_; not; const)
open import Tactic.By.Propositional

open import Equality.Decision-procedures equality-with-J
import Nat equality-with-J as Nat

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Constants      χ-ℕ-atoms
open import Deterministic  χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms
open import Reasoning      χ-ℕ-atoms
open import Substitution   χ-ℕ-atoms
open import Termination    χ-ℕ-atoms
open import Values         χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

import Coding.Instances.Nat

------------------------------------------------------------------------
-- A non-terminating expression

loop : Exp
loop = rec v-x (var v-x)

loop-closed : Closed loop
loop-closed =
  Closed′-closed-under-rec $
  Closed′-closed-under-var (inj₁ refl)

¬loop⇓ : ¬ Terminates loop
¬loop⇓ (_ , p) = lemma p
  where
  lemma : ∀ {w} → ¬ loop ⇓ w
  lemma (rec p) with v-x V.≟ v-x
  ... | no  x≢x = x≢x refl
  ... | yes _   = lemma p

------------------------------------------------------------------------
-- The identity function

id : Exp
id = lambda v-x (var v-x)

id-closed : Closed id
id-closed = from-⊎ (closed? id)

id-correct : ∀ {e v} → e ⇓ v → apply id e ⇓ v
id-correct {e = e} {v = v} e⇓v =
  apply id e           ⟶⟨ apply lambda e⇓v ⟩
  var v-x [ v-x ← v ]  ≡⟨ var-step-≡ (refl {x = v-x}) ⟩⟶
  v                    ■⟨ ⇓-Value e⇓v ⟩

------------------------------------------------------------------------
-- Natural numbers

-- Equality of natural numbers.

private

  equal-ℕ′ : Exp
  equal-ℕ′ =
    rec v-equal (lambda v-m (lambda v-n (case (var v-m) branches)))
    module Equal-ℕ where
    zero-branches =
      branch c-zero [] (const c-true []) ∷
      branch c-suc (v-n ∷ []) (const c-false []) ∷
      []

    suc-branches =
      branch c-zero [] (const c-false []) ∷
      branch c-suc (v-n ∷ []) (
        apply (apply (var v-equal) (var v-m)) (var v-n)) ∷
      []

    branches =
      branch c-zero [] (case (var v-n) zero-branches) ∷
      branch c-suc (v-m ∷ []) (case (var v-n) suc-branches) ∷
      []

equal-ℕ : Exp → Exp → Exp
equal-ℕ e₁ e₂ = apply (apply equal-ℕ′ e₁) e₂

equal-ℕ-closed :
  ∀ {xs e₁ e₂} →
  Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (equal-ℕ e₁ e₂)
equal-ℕ-closed {xs} cl-e₁ cl-e₂ =
  Closed′-closed-under-apply
    (Closed′-closed-under-apply
       (from-⊎ (closed′? equal-ℕ′ xs))
       cl-e₁)
    cl-e₂

equal-ℕ-correct :
  ∀ m n →
  equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓
  ⌜ Prelude.if m Nat.≟ n then true else false ⌝
equal-ℕ-correct m n =
  equal-ℕ ⌜ m ⌝ ⌜ n ⌝                               ⟶⟨⟩

  apply (apply equal-ℕ′ ⌜ m ⌝) ⌜ n ⌝                ⟶⟨ apply (apply (rec lambda) (rep⇓rep m) lambda) (rep⇓rep n) ⟩

  case ⟨ ⌜ m ⌝ [ v-n ← ⌜ n ⌝ ] ⟩
    (branches [ v-equal ← equal-ℕ′ ]B⋆
              [ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆)  ≡⟨ ⟨by⟩ (subst-rep m) ⟩⟶

  case ⌜ m ⌝
    (branches [ v-equal ← equal-ℕ′ ]B⋆
              [ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆)  ⇓⟨ lemma m n ⟩■

  ⌜ Prelude.if m Nat.≟ n then true else false ⌝
  where
  open Equal-ℕ

  lemma :
    ∀ m n →
    case ⌜ m ⌝
      (branches [ v-equal ← equal-ℕ′ ]B⋆
                [ v-m ← ⌜ m ⌝ ]B⋆ [ v-n ← ⌜ n ⌝ ]B⋆)
      ⇓
    ⌜ Prelude.if m Nat.≟ n then true else false ⌝
  lemma zero zero =
    case ⌜ zero ⌝
      (branches [ v-equal ← equal-ℕ′ ]B⋆
                [ v-m ← ⌜ zero ⌝ ]B⋆ [ v-n ← ⌜ zero ⌝ ]B⋆)  ⟶⟨ _⇓_.case (rep⇓rep zero) here [] ⟩

    case ⌜ zero ⌝ zero-branches                             ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (true ⦂ Bool)) ⟩■

    ⌜ true ⦂ Bool ⌝

  lemma zero (suc n) =
    case ⌜ zero ⌝
      (branches [ v-equal ← equal-ℕ′ ]B⋆
                [ v-m ← ⌜ zero ⌝ ]B⋆ [ v-n ← ⌜ suc n ⌝ ]B⋆)  ⟶⟨ case (rep⇓rep zero) here [] ⟩

    case ⌜ suc n ⌝ zero-branches                             ⇓⟨ case (rep⇓rep (suc n)) (there (λ ()) here) (∷ [])
                                                                     (rep⇓rep (false ⦂ Bool)) ⟩■
    ⌜ false ⦂ Bool ⌝

  lemma (suc m) zero =
    case ⌜ suc m ⌝
      (branches [ v-equal ← equal-ℕ′ ]B⋆
                [ v-m ← ⌜ suc m ⌝ ]B⋆ [ v-n ← ⌜ zero ⌝ ]B⋆)     ⟶⟨ case (rep⇓rep (suc m)) (there (λ ()) here) (∷ []) ⟩

    case ⌜ zero ⌝
      (suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
                    [ v-n ← ⌜ zero ⌝ ]B⋆)                       ⇓⟨ case (rep⇓rep zero) here [] (rep⇓rep (false ⦂ Bool)) ⟩■

    ⌜ false ⦂ Bool ⌝

  lemma (suc m) (suc n) =
    case ⌜ suc m ⌝
      (branches [ v-equal ← equal-ℕ′ ]B⋆
                [ v-m ← ⌜ suc m ⌝ ]B⋆ [ v-n ← ⌜ suc n ⌝ ]B⋆)    ⟶⟨ case (rep⇓rep (suc m)) (there (λ ()) here) (∷ []) ⟩

    case ⟨ ⌜ suc n ⌝ [ v-m ← ⌜ m ⌝ ] ⟩
      (suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
                    [ v-n ← ⌜ suc n ⌝ ]B⋆)                      ≡⟨ ⟨by⟩ (subst-rep (suc n)) ⟩⟶

    case ⌜ suc n ⌝
      (suc-branches [ v-equal ← equal-ℕ′ ]B⋆ [ v-m ← ⌜ m ⌝ ]B⋆
                    [ v-n ← ⌜ suc n ⌝ ]B⋆)                      ⟶⟨ case (rep⇓rep (suc n)) (there (λ ()) here) (∷ []) ⟩

    apply (apply equal-ℕ′ ⟨ ⌜ m ⌝ [ v-n ← ⌜ n ⌝ ] ⟩) ⌜ n ⌝      ≡⟨ ⟨by⟩ (subst-rep m) ⟩⟶

    apply (apply equal-ℕ′ ⌜ m ⌝) ⌜ n ⌝                          ⟶⟨⟩

    equal-ℕ ⌜ m ⌝ ⌜ n ⌝                                         ⇓⟨ equal-ℕ-correct m n ⟩

    ⌜ Prelude.if m Nat.≟ n then true else false ⌝               ≡⟨ by lem ⟩⟶

    ⌜ Prelude.if suc m Nat.≟ suc n then true else false ⌝       ■⟨ rep-value (Prelude.if suc m Nat.≟ suc n then true else false) ⟩
    where
    lem : Prelude.if m Nat.≟ n then true else false ≡
          Prelude.if suc m Nat.≟ suc n then true else false
    lem with m Nat.≟ n
    ... | yes _ = refl
    ... | no  _ = refl

private

  equal-ℕ-correct′ :
    ∀ m n {v} →
    equal-ℕ ⌜ m ⌝ ⌜ n ⌝ ⇓ v →
    v ≡ ⌜ Prelude.if m Nat.≟ n then true else false ⌝
  equal-ℕ-correct′ m n p =
    ⇓-deterministic p (equal-ℕ-correct m n)

-- Membership of a list of natural numbers.

private

  member′ : Exp
  member′ =
    lambda v-x body
    module Member where
    cons-branches =
      branch c-true [] (const c-true []) ∷
      branch c-false [] (apply (var v-member) (var v-xs)) ∷
      []

    branches =
      branch c-nil [] (const c-false []) ∷
      branch c-cons (v-y ∷ v-xs ∷ []) (
        case (equal-ℕ (var v-x) (var v-y))
          cons-branches) ∷
      []

    body = rec v-member (lambda v-xs (case (var v-xs) branches))

    body-closed : ∀ {xs} → Closed′ (v-x ∷ xs) body
    body-closed {xs} = from-⊎ (closed′? body (v-x ∷ xs))

member : Exp → Exp → Exp
member m ns = apply (apply member′ m) ns

member-closed :
  ∀ {xs m ns} →
  Closed′ xs m → Closed′ xs ns → Closed′ xs (member m ns)
member-closed cl-m cl-ns =
  Closed′-closed-under-apply
    (Closed′-closed-under-apply
       (Closed′-closed-under-lambda Member.body-closed)
       cl-m)
    cl-ns

member-correct :
  ∀ m ns →
  member ⌜ m ⌝ ⌜ ns ⌝ ⇓
  ⌜ Prelude.if V.member m ns then true else false ⌝
member-correct m ns =
  member ⌜ m ⌝ ⌜ ns ⌝                                                   ⟶⟨⟩

  apply (apply member′ ⌜ m ⌝) ⌜ ns ⌝                                    ⟶⟨ apply (apply lambda (rep⇓rep m) (rec lambda)) (rep⇓rep ns) ⟩

  case ⌜ ns ⌝
    (branches [ v-x ← ⌜ m ⌝ ]B⋆ [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)  ⇓⟨ lemma ns ⟩■

  ⌜ Prelude.if V.member m ns then true else false ⌝
  where
  open Member

  lemma :
    ∀ ns →
    case ⌜ ns ⌝ (branches [ v-x ← ⌜ m ⌝ ]B⋆
                             [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)
      ⇓
    ⌜ Prelude.if V.member m ns then true else false ⌝
  lemma [] =
    case ⌜ [] ⦂ List ℕ ⌝
      (branches [ v-x ← ⌜ m ⌝ ]B⋆
                [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)         ⇓⟨ case (rep⇓rep ([] ⦂ List ℕ)) here [] (const []) ⟩■

    ⌜ false ⦂ Bool ⌝

  lemma (n ∷ ns) =
    case ⌜ n List.∷ ns ⌝
      (branches [ v-x ← ⌜ m ⌝ ]B⋆
                [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)         ⟶⟨ case (rep⇓rep (n List.∷ ns)) (there (λ ()) here) (∷ ∷ []) ⟩

    case (equal-ℕ ⟨ ⌜ m ⌝ [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]
                          [ v-xs ← ⌜ ns ⌝ ] [ v-y ← ⌜ n ⌝ ] ⟩
                  ⌜ n ⌝)
      (cons-branches [ v-x ← ⌜ m ⌝ ]B⋆
                     [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                     [ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆)    ≡⟨ ⟨by⟩ (substs-rep m ((v-y , ⌜ n ⌝) ∷ (v-xs , ⌜ ns ⌝) ∷
                                                                                (v-member , body [ v-x ← ⌜ m ⌝ ]) ∷ [])) ⟩⟶
    case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
      (⟨ cons-branches [ v-x ← ⌜ m ⌝ ]B⋆ ⟩
                       [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                       [ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆)  ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _ ⌜ m ⌝ (from-⊎ (v-x ∈?-B⋆ cons-branches))) ⟩⟶

    case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
      ⟨ cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                      [ v-xs ← ⌜ ns ⌝ ]B⋆ [ v-y ← ⌜ n ⌝ ]B⋆ ⟩  ≡⟨ ⟨by⟩ (subst-∉-B⋆ _ _ _
                                                                          λ { (._ , ._ , ._ , inj₁ refl        , const _ ()        , _)
                                                                            ; (._ , ._ , ._ , inj₂ (inj₁ refl) , y∈FV[body[x←m]ns] , _) →
                                                                              Closed′-closed-under-apply
                                                                                (Closed′-closed-under-subst body-closed (rep-closed m))
                                                                                (rep-closed ns)
                                                                                v-y (λ ()) y∈FV[body[x←m]ns]
                                                                            ; (_ , _ , _ , (inj₂ (inj₂ ())) , _) }) ⟩⟶
    case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
      (cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                     [ v-xs ← ⌜ ns ⌝ ]B⋆)                      ⇓⟨ lemma′ (m Nat.≟ n) (equal-ℕ-correct m n) ⟩■

    ⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝
    where
    lemma′ :
      (m≟n : Dec (m ≡ n)) →
      equal-ℕ ⌜ m ⌝ ⌜ n ⌝
        ⇓
      ⌜ Prelude.if m≟n then true else false ⌝ →
      case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
        (cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                       [ v-xs ← ⌜ ns ⌝ ]B⋆)
        ⇓
      ⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝
    lemma′ (yes m≡n) hyp =
      case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
        (cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                       [ v-xs ← ⌜ ns ⌝ ]B⋆)                    ⟶⟨ case hyp here [] ⟩

      ⌜ true ⦂ Bool ⌝                                          ≡⟨ cong ⌜_⌝ lem ⟩⟶

      ⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝  ■⟨ rep-value (Prelude.if V.member m (n ∷ ns) then true else false) ⟩
      where
      lem : true ≡ Prelude.if V.member m (n ∷ ns) then true else false
      lem with m Nat.≟ n
      ... | yes _   = refl
      ... | no  m≢n = ⊥-elim (m≢n m≡n)

    lemma′ (no m≢n) hyp =
      case (equal-ℕ ⌜ m ⌝ ⌜ n ⌝)
        (cons-branches [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆
                       [ v-xs ← ⌜ ns ⌝ ]B⋆)                    ⟶⟨ case hyp (there (λ ()) here) [] ⟩

      apply ⟨ body [ v-x ← ⌜ m ⌝ ] [ v-xs ← ⌜ ns ⌝ ] ⟩ ⌜ ns ⌝  ≡⟨ ⟨by⟩ (subst-closed v-xs ⌜ ns ⌝
                                                                          (Closed′-closed-under-subst body-closed (rep-closed m))) ⟩⟶

      apply (body [ v-x ← ⌜ m ⌝ ]) ⌜ ns ⌝                      ⟶⟨ apply (rec lambda) (rep⇓rep ns) ⟩

      case ⌜ ns ⌝
        (branches [ v-x ← ⌜ m ⌝ ]B⋆
                  [ v-member ← body [ v-x ← ⌜ m ⌝ ] ]B⋆)       ⇓⟨ lemma ns ⟩

      ⌜ Prelude.if V.member m      ns  then true else false ⌝  ≡⟨ cong ⌜_⌝ lem ⟩⟶

      ⌜ Prelude.if V.member m (n ∷ ns) then true else false ⌝  ■⟨ rep-value (Prelude.if V.member m (n ∷ ns) then true else false) ⟩
      where
      lem : Prelude.if V.member m      ns  then true else false ≡
            Prelude.if V.member m (n ∷ ns) then true else false
      lem with m Nat.≟ n
      ... | yes m≡n = ⊥-elim (m≢n m≡n)
      ... | no  _   with V.member m ns
      ...   | yes _ = refl
      ...   | no  _ = refl

------------------------------------------------------------------------
-- Booleans

-- If-then-else.

infix 5 if_then_else_

if_then_else_ : Exp → Exp → Exp → Exp
if c then t else f =
  case c (branch c-true  [] t ∷
          branch c-false [] f ∷
          [])

if-then-else-closed :
  ∀ {xs c t f} →
  Closed′ xs c → Closed′ xs t → Closed′ xs f →
  Closed′ xs (if c then t else f)
if-then-else-closed c-cl t-cl f-cl =
  Closed′-closed-under-case
    c-cl
    λ where
      (inj₁ refl)        → t-cl
      (inj₂ (inj₁ refl)) → f-cl
      (inj₂ (inj₂ ()))

if-then-else-correct :
  ∀ {A : Type} ⦃ cA : Rep A Consts ⦄ {e₁ e₂ e₃}
  (b₁ : Bool) (v₂ v₃ : A) →
  e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ v₂ ⌝ → e₃ ⇓ ⌜ v₃ ⌝ →
  if e₁ then e₂ else e₃ ⇓ ⌜ Prelude.if b₁ then v₂ else v₃ ⌝
if-then-else-correct true  _ _ e₁⇓ e₂⇓ e₃⇓ = case e₁⇓ here [] e₂⇓
if-then-else-correct false _ _ e₁⇓ e₂⇓ e₃⇓ =
  case e₁⇓ (there (λ ()) here) [] e₃⇓

-- Negation of booleans.

not : Exp → Exp
not e = if e then ⌜ false ⦂ Bool ⌝ else ⌜ true ⦂ Bool ⌝

not-closed : ∀ {xs e} → Closed′ xs e → Closed′ xs (not e)
not-closed cl-e =
  if-then-else-closed
    cl-e
    (Closed→Closed′ (from-⊎ (closed? ⌜ false ⦂ Bool ⌝)))
    (Closed→Closed′ (from-⊎ (closed? ⌜ true  ⦂ Bool ⌝)))

not-correct : ∀ {e} (b : Bool) → e ⇓ ⌜ b ⌝ → not e ⇓ ⌜ Prelude.not b ⌝
not-correct true  e⇓ = case e⇓ here [] (rep⇓rep (false ⦂ Bool))
not-correct false e⇓ =
  case e⇓ (there (λ ()) here) [] (rep⇓rep (true ⦂ Bool))

-- Conjunction.

and : Exp → Exp → Exp
and e₁ e₂ = if e₁ then e₂ else ⌜ false ⦂ Bool ⌝

and-closed :
  ∀ {xs e₁ e₂} → Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (and e₁ e₂)
and-closed cl-e₁ cl-e₂ =
  if-then-else-closed
    cl-e₁
    cl-e₂
    (Closed→Closed′ (from-⊎ (closed? ⌜ false ⦂ Bool ⌝)))

and-correct :
  ∀ {e₁ e₂} b₁ b₂ →
  e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
  and e₁ e₂ ⇓ ⌜ b₁ ∧ b₂ ⌝
and-correct b₁ b₂ e₁⇓ e₂⇓ =
  if-then-else-correct b₁ b₂ false e₁⇓ e₂⇓ (rep⇓rep (false ⦂ Bool))

-- Disjunction.

or : Exp → Exp → Exp
or e₁ e₂ = if e₁ then ⌜ true ⦂ Bool ⌝ else e₂

or-closed :
  ∀ {xs e₁ e₂} → Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (or e₁ e₂)
or-closed cl-e₁ cl-e₂ =
  if-then-else-closed
    cl-e₁
    (Closed→Closed′ (from-⊎ (closed? ⌜ true ⦂ Bool ⌝)))
    cl-e₂

or-correct :
  ∀ {e₁ e₂} b₁ b₂ →
  e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
  or e₁ e₂ ⇓ ⌜ b₁ ∨ b₂ ⌝
or-correct b₁ b₂ e₁⇓ e₂⇓ =
  if-then-else-correct b₁ true b₂ e₁⇓ (rep⇓rep (true ⦂ Bool)) e₂⇓

-- Equality of booleans.

equal-Bool : Exp → Exp → Exp
equal-Bool e₁ e₂ =
  if e₁ then e₂ else not e₂

equal-Bool-closed :
  ∀ {xs e₁ e₂} →
  Closed′ xs e₁ → Closed′ xs e₂ → Closed′ xs (equal-Bool e₁ e₂)
equal-Bool-closed cl-e₁ cl-e₂ =
  if-then-else-closed cl-e₁ cl-e₂ (not-closed cl-e₂)

equal-Bool-correct :
  ∀ {e₁ e₂} b₁ b₂ →
  e₁ ⇓ ⌜ b₁ ⌝ → e₂ ⇓ ⌜ b₂ ⌝ →
  equal-Bool e₁ e₂ ⇓ ⌜ Prelude.if b₁ Bool.≟ b₂ then true else false ⌝
equal-Bool-correct {e₁} {e₂} b₁ b₂ e₁⇓ e₂⇓ =
  equal-Bool e₁ e₂                                  ⇓⟨ if-then-else-correct b₁ b₂ (Prelude.not b₂) e₁⇓ e₂⇓ (not-correct b₂ e₂⇓) ⟩
  ⌜ Prelude.if b₁ then b₂ else Prelude.not b₂ ⌝     ≡⟨ cong ⌜_⌝ (lemma b₁ b₂) ⟩⟶
  ⌜ Prelude.if b₁ Bool.≟ b₂ then true else false ⌝  ■⟨ rep-value (Prelude.if b₁ Bool.≟ b₂ then true else false) ⟩
  where
  lemma :
    ∀ b₁ b₂ →
    Prelude.if b₁ then b₂ else Prelude.not b₂ ≡
    Prelude.if b₁ Bool.≟ b₂ then true else false
  lemma true  true  = refl
  lemma true  false = refl
  lemma false true  = refl
  lemma false false = refl

-- An internal decoding function for booleans.

decode-Bool : Exp → Exp
decode-Bool e =
  case e
    (branch c-const (v-c ∷ v-es ∷ [])
       (equal-ℕ (var v-c) ⌜ c-true ⌝) ∷ [])

decode-Bool-closed :
  ∀ {xs e} → Closed′ xs e → Closed′ xs (decode-Bool e)
decode-Bool-closed cl-e =
  Closed′-closed-under-case
    cl-e
    λ where
      (inj₁ refl) → equal-ℕ-closed
                      (Closed′-closed-under-var
                         (from-⊎ (V.member v-c (v-c ∷ v-es ∷ _))))
                      (Closed→Closed′ (rep-closed c-true))
      (inj₂ ())

decode-Bool-correct :
  ∀ {e} (b : Bool) →
  e ⇓ ⌜ ⌜ b ⌝ ⦂ Exp ⌝ → decode-Bool e ⇓ ⌜ b ⌝
decode-Bool-correct true e⇓ =
  case e⇓ here (∷ ∷ []) (equal-ℕ-correct c-true c-true)
decode-Bool-correct false e⇓ =
  case e⇓ here (∷ ∷ []) (equal-ℕ-correct c-false c-true)

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
-- Various operations and proofs on morphisms between products
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

module Categories.Object.Product.Morphisms {o ℓ e} (C : Category o ℓ e) where

import Categories.Object.Product
open Categories.Object.Product C

open Category C
open Equiv
open HomReasoning

open import Function using (flip)
open import Level

infix 10 [_]⟨_,_⟩ [_⇒_]_⁂_

[[_]] : ∀{A B} → Product A B → Obj
[[ p ]] = Product.A×B p

[_]⟨_,_⟩ : ∀ {A B C}
  → (p : Product B C) → A ⇒ B → A ⇒ C → A ⇒ [[ p ]]
[ p ]⟨ f , g ⟩ = Product.⟨_,_⟩ p f g

[_]π₁ : ∀ {A B}
  → (p : Product A B) → [[ p ]] ⇒ A
[_]π₁ = Product.π₁

[_]π₂ : ∀ {A B}
  → (p : Product A B) → [[ p ]] ⇒ B
[_]π₂ = Product.π₂

[_⇒_]_⁂_ : ∀ {A B C D}
    → (p₁ : Product A C)
    → (p₂ : Product B D)
    → (A ⇒ B) → (C ⇒ D) → ([[ p₁ ]] ⇒ [[ p₂ ]])
[ p₁ ⇒ p₂ ] f ⁂ g = [ p₂ ]⟨ f ∘ p₁.π₁ , g ∘ p₁.π₂ ⟩
    where
        module p₁ = Product p₁
        module p₂ = Product p₂

.id⁂id : ∀ {A B}(p : Product A B) → [ p ⇒ p ] id ⁂ id ≡ id
id⁂id p =
  begin
    ⟨ id ∘ π₁ , id ∘ π₂ ⟩
  ↓⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
    ⟨ π₁ , π₂ ⟩
  ↓⟨ η ⟩
    id
  ∎
  where
  open Product p

.repack≡id⁂id : ∀{X Y}(p₁ p₂ : Product X Y) → repack p₁ p₂ ≡ [ p₁ ⇒ p₂ ] id ⁂ id
repack≡id⁂id p₁ p₂ = sym (Product.⟨⟩-cong₂ p₂ identityˡ identityˡ)
    where open Equiv

.[_⇒_]π₁∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D}
  → (p₁ : Product A C)
  → (p₂ : Product B D)
  → Product.π₁ p₂ ∘ [ p₁ ⇒ p₂ ] f ⁂ g ≡ f ∘ Product.π₁ p₁
[_⇒_]π₁∘⁂ {f = f} {g} p₁ p₂ = Product.commute₁ p₂

.[_⇒_]π₂∘⁂ : ∀ {A B C D} → {f : A ⇒ B} → {g : C ⇒ D}
  → (p₁ : Product A C)
  → (p₂ : Product B D)
  → Product.π₂ p₂ ∘ [ p₁ ⇒ p₂ ] f ⁂ g ≡ g ∘ Product.π₂ p₁
[_⇒_]π₂∘⁂ {f = f} {g} p₁ p₂ = Product.commute₂ p₂

.[_⇒_]⁂-cong₂ : ∀ {A B C D}{f g h i}
    → (p₁ : Product A B)
    → (p₂ : Product C D)
    → f ≡ g
    → h ≡ i
    → [ p₁ ⇒ p₂ ] f ⁂ h ≡ [ p₁ ⇒ p₂ ] g ⁂ i
[_⇒_]⁂-cong₂ {A}{B}{C}{D}{f}{g}{h}{i} p₁ p₂ f≡g h≡i =
    Product.⟨⟩-cong₂ p₂ (∘-resp-≡ f≡g refl) (∘-resp-≡ h≡i refl)

.[_⇒_]⁂∘⟨⟩ : ∀{A B C D X}
  → {f  : A ⇒ C} {f′ : X ⇒ A}
  → {g  : B ⇒ D} {g′ : X ⇒ B}
  → (p₁ : Product A B)
  → (p₂ : Product C D)
  → ([ p₁ ⇒ p₂ ] f ⁂ g) ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≡ [ p₂ ]⟨ f ∘ f′ , g ∘ g′ ⟩
[_⇒_]⁂∘⟨⟩ {A}{B}{C}{D}{X}{f}{f′}{g}{g′} p₁ p₂ =
  begin
    [ p₂ ]⟨ f ∘ p₁.π₁ , g ∘ p₁.π₂ ⟩ ∘ [ p₁ ]⟨ f′ , g′ ⟩
  ↓⟨ p₂.⟨⟩∘ ⟩
    [ p₂ ]⟨ (f ∘ p₁.π₁) ∘ p₁.⟨_,_⟩ f′ g′
          , (g ∘ p₁.π₂) ∘ p₁.⟨_,_⟩ f′ g′ ⟩
  ↓⟨ p₂.⟨⟩-cong₂ assoc assoc ⟩
    [ p₂ ]⟨ f ∘ p₁.π₁ ∘ p₁.⟨_,_⟩ f′ g′
          , g ∘ p₁.π₂ ∘ p₁.⟨_,_⟩ f′ g′ ⟩
  ↓⟨ p₂.⟨⟩-cong₂ (∘-resp-≡ refl p₁.commute₁) (∘-resp-≡ refl p₁.commute₂) ⟩
    [ p₂ ]⟨ f ∘ f′ , g ∘ g′ ⟩
  ∎
  where
  module p₁ = Product p₁
  module p₂ = Product p₂

.[_⇒_⇒_]⁂∘⁂ : ∀ {A B C D E F}{f g h i}
    → (p₁ : Product A B)
    → (p₂ : Product C D)
    → (p₃ : Product E F)
    → ([ p₂ ⇒ p₃ ] g ⁂ i) ∘ ([ p₁ ⇒ p₂ ] f ⁂ h) ≡ [ p₁ ⇒ p₃ ] (g ∘ f) ⁂ (i ∘ h)
[_⇒_⇒_]⁂∘⁂ {A}{B}{C}{D}{E}{F}{f}{g}{h}{i} p₁ p₂ p₃ =
    begin
        [ p₃ ]⟨ g ∘ p₂.π₁ , i ∘ p₂.π₂ ⟩ ∘ [ p₂ ]⟨ f ∘ p₁.π₁ , h ∘ p₁.π₂ ⟩
    ↓⟨ [ p₂ ⇒ p₃ ]⁂∘⟨⟩ ⟩
        [ p₃ ]⟨ g ∘ f ∘ p₁.π₁ , i ∘ h ∘ p₁.π₂ ⟩
    ↑⟨ p₃.⟨⟩-cong₂ assoc assoc ⟩
        [ p₃ ]⟨ (g ∘ f) ∘ p₁.π₁ , (i ∘ h) ∘ p₁.π₂ ⟩
    ∎
    where
    module p₁ = Product p₁
    module p₂ = Product p₂
    module p₃ = Product p₃

.[_⇒_⇒_]repack∘⁂ : ∀ {A B C D}{f g}
    → (p₁ : Product A B)
    → (p₂ : Product C D)
    → (p₃ : Product C D)
    → repack p₂ p₃ ∘ [ p₁ ⇒ p₂ ] f ⁂ g ≡ [ p₁ ⇒ p₃ ] f ⁂ g
[_⇒_⇒_]repack∘⁂ {A}{B}{C}{D}{f}{g} p₁ p₂ p₃ =
  begin
    repack p₂ p₃ ∘ [ p₁ ⇒ p₂ ] f ⁂ g
  ↓⟨ repack≡id⁂id p₂ p₃ ⟩∘⟨ refl ⟩
    ([ p₂ ⇒ p₃ ] id ⁂ id) ∘ ([ p₁ ⇒ p₂ ] f ⁂ g)
  ↓⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]⁂∘⁂ ⟩
    [ p₁ ⇒ p₃ ] (id ∘ f) ⁂ (id ∘ g)
  ↓⟨ [ p₁ ⇒ p₃ ]⁂-cong₂ identityˡ identityˡ ⟩
    [ p₁ ⇒ p₃ ] f ⁂ g
  ∎

.[_⇒_⇒_]repack∘repack : ∀{A B}
  → (p₁ p₂ p₃ : Product A B)
  → repack p₂ p₃ ∘ repack p₁ p₂ ≡ repack p₁ p₃
[_⇒_⇒_]repack∘repack = repack∘
{-
  begin
    repack p₂ p₃ ∘ repack p₁ p₂
  ↓⟨ repack≡id⁂id p₂ p₃ ⟩∘⟨ repack≡id⁂id p₁ p₂ ⟩
    ([ p₂ ⇒ p₃ ] id ⁂ id) ∘ ([ p₁ ⇒ p₂ ] id ⁂ id)
  ↓⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]⁂∘⁂ ⟩
    [ p₁ ⇒ p₃ ] (id ∘ id) ⁂ (id ∘ id)
  ↓⟨ [ p₁ ⇒ p₃ ]⁂-cong₂ identityˡ identityˡ ⟩
    [ p₁ ⇒ p₃ ] id ⁂ id
  ↑⟨ repack≡id⁂id p₁ p₃ ⟩
    repack p₁ p₃
  ∎
-}

[_⇒_]first
    : ∀ {A B C}
    → (p₁ : Product A C) → (p₂ : Product B C)
    → A ⇒ B → [[ p₁ ]] ⇒ [[ p₂ ]]
[ p₁ ⇒ p₂ ]first f = [ p₁ ⇒ p₂ ] f ⁂ id

[_⇒_]second
    : ∀ {A B C}
    → (p₁ : Product A B) → (p₂ : Product A C)
    → B ⇒ C → [[ p₁ ]] ⇒ [[ p₂ ]]
[ p₁ ⇒ p₂ ]second g = [ p₁ ⇒ p₂ ] id ⁂ g

.first-id : ∀ {A B}(p : Product A B) → [ p ⇒ p ]first id ≡ id
first-id = id⁂id

.second-id : ∀ {A B}(p : Product A B) → [ p ⇒ p ]second id ≡ id
second-id = id⁂id

.[_⇒_]first∘⟨⟩ : ∀ {A B C D}
  → {f : B ⇒ C} {f′ : A ⇒ B} {g′ : A ⇒ D}
  → (p₁ : Product B D) (p₂ : Product C D)
  → [ p₁ ⇒ p₂ ]first f ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≡ [ p₂ ]⟨ f ∘ f′ , g′ ⟩
[_⇒_]first∘⟨⟩ {A}{B}{C}{D}{f}{f′}{g′} p₁ p₂ =
  begin
    [ p₁ ⇒ p₂ ]first f ∘ [ p₁ ]⟨ f′ , g′ ⟩
  ↓⟨ [ p₁ ⇒ p₂ ]⁂∘⟨⟩ ⟩
    [ p₂ ]⟨ f ∘ f′ , id ∘ g′ ⟩
  ↓⟨ p₂.⟨⟩-cong₂ refl identityˡ ⟩
    [ p₂ ]⟨ f ∘ f′ , g′ ⟩
  ∎
  where
  module p₂ = Product p₂

.[_⇒_]second∘⟨⟩ : ∀ {A B D E}
  → {f′ : A ⇒ B} {g : D ⇒ E} {g′ : A ⇒ D}
  → (p₁ : Product B D) (p₂ : Product B E)
  → [ p₁ ⇒ p₂ ]second g ∘ [ p₁ ]⟨ f′ , g′ ⟩ ≡ [ p₂ ]⟨ f′ , g ∘ g′ ⟩
[_⇒_]second∘⟨⟩ {A}{B}{D}{E}{f′}{g}{g′} p₁ p₂ =
  begin
    [ p₁ ⇒ p₂ ]second g ∘ [ p₁ ]⟨ f′ , g′ ⟩
  ↓⟨ [ p₁ ⇒ p₂ ]⁂∘⟨⟩ ⟩
    [ p₂ ]⟨ id ∘ f′ , g ∘ g′ ⟩
  ↓⟨ p₂.⟨⟩-cong₂ identityˡ refl ⟩
    [ p₂ ]⟨ f′ , g ∘ g′ ⟩
  ∎
  where
  module p₂ = Product p₂

.[_⇒_⇒_]first∘first : ∀ {A B C D}{f : B ⇒ C} {g : A ⇒ B}
  → (p₁ : Product A D)
  → (p₂ : Product B D)
  → (p₃ : Product C D)
  → [ p₂ ⇒ p₃ ]first f ∘ [ p₁ ⇒ p₂ ]first g ≡ [ p₁ ⇒ p₃ ]first(f ∘ g)
[_⇒_⇒_]first∘first {A}{B}{C}{D}{f}{g} p₁ p₂ p₃ =
  begin
    [ p₂ ⇒ p₃ ]first f ∘ [ p₁ ⇒ p₂ ]first g
  ↓⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]⁂∘⁂ ⟩
    [ p₁ ⇒ p₃ ] (f ∘ g) ⁂ (id ∘ id)
  ↓⟨ [ p₁ ⇒ p₃ ]⁂-cong₂ refl identityˡ ⟩
    [ p₁ ⇒ p₃ ]first (f ∘ g)
  ∎

.[_⇒_⇒_]second∘second : ∀ {A B C D}{f : C ⇒ D} {g : B ⇒ C}
  → (p₁ : Product A B)
  → (p₂ : Product A C)
  → (p₃ : Product A D)
  → [ p₂ ⇒ p₃ ]second f ∘ [ p₁ ⇒ p₂ ]second g ≡ [ p₁ ⇒ p₃ ]second(f ∘ g)
[_⇒_⇒_]second∘second {A}{B}{C}{D}{f}{g} p₁ p₂ p₃ =
  begin
    [ p₂ ⇒ p₃ ]second f ∘ [ p₁ ⇒ p₂ ]second g
  ↓⟨ [ p₁ ⇒ p₂ ⇒ p₃ ]⁂∘⁂ ⟩
    [ p₁ ⇒ p₃ ] (id ∘ id) ⁂ (f ∘ g)
  ↓⟨ [ p₁ ⇒ p₃ ]⁂-cong₂ identityˡ refl ⟩
    [ p₁ ⇒ p₃ ]second (f ∘ g)
  ∎

.[_⇒_,_⇒_]first↔second : ∀ {A B C D}{f : A ⇒ B}{g : C ⇒ D}
  → (p₁ : Product A D)
  → (p₂ : Product B D)
  → (p₃ : Product A C)
  → (p₄ : Product B C)
  → [ p₁ ⇒ p₂ ]first f ∘ [ p₃ ⇒ p₁ ]second g ≡ [ p₄ ⇒ p₂ ]second g ∘ [ p₃ ⇒ p₄ ]first f
[_⇒_,_⇒_]first↔second {A}{B}{C}{D}{f}{g} p₁ p₂ p₃ p₄ =
  begin
    [ p₁ ⇒ p₂ ]first f ∘ [ p₃ ⇒ p₁ ]second g
  ↓⟨ [ p₃ ⇒ p₁ ⇒ p₂ ]⁂∘⁂ ⟩
    [ p₃ ⇒ p₂ ] (f ∘ id) ⁂ (id ∘ g)
  ↓⟨ [ p₃ ⇒ p₂ ]⁂-cong₂ identityʳ identityˡ ⟩
    [ p₃ ⇒ p₂ ] f ⁂ g
  ↑⟨ [ p₃ ⇒ p₂ ]⁂-cong₂ identityˡ identityʳ ⟩
    [ p₃ ⇒ p₂ ] (id ∘ f) ⁂ (g ∘ id)
  ↑⟨ [ p₃ ⇒ p₄ ⇒ p₂ ]⁂∘⁂ ⟩
    [ p₄ ⇒ p₂ ]second g ∘ [ p₃ ⇒ p₄ ]first f
  ∎

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Prelude

module Implicits.Substitutions.Lemmas where

open import Implicits.Syntax.Type
open import Implicits.Syntax.Term hiding (var)
open import Implicits.Syntax.Context
open import Implicits.WellTyped
open import Implicits.Substitutions
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Extensions.Substitution
import Category.Applicative.Indexed as Applicative
open Applicative.Morphism using (op-<$>)

module TypeLemmas where
  open import Implicits.Substitutions.Lemmas.Type public

open import Implicits.Substitutions.Lemmas.MetaType public

{-
module SubstLemmas (_⊢ᵣ_ : ∀ {ν} → ICtx ν → Type ν → Set) where

  open TypingRules _⊢ᵣ_

  private
    ⊢subst : ∀ {m n} {Γ₁ Γ₂ : Ktx 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} {Γ₁ Γ₂ : Ktx n m} {t : Term n m} {a : Type n} →
      Γ₁ ≡ Γ₂ → Γ₁ ⊢ t ∈ a → Γ₂ ⊢ t ∈ a
    ⊢substCtx refl hyp = hyp

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

  module WtTermLemmas where
    weaken : ∀ {ν n} {K : Ktx ν n} {t : Term ν n} {a b : Type ν} →
                       K ⊢ t ∈ a → b ∷Γ K ⊢ tmtm-weaken t ∈ a
    -- weaken {Γ = Γ} {b = b} ⊢t = Var.wk /Var ⊢substCtx (C.wkVar-/Var-∷ Γ b) ⊢t

  module TermTypeLemmas where
    open TermTypeSubst

    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+ n) m)  → t /₁ ρ₁ ↑⋆₁ i ≡ t /₂ ρ₂ ↑⋆₂ i
    /-↑⋆ ρ₁ ρ₂ hyp i (new x)      = refl
    /-↑⋆ ρ₁ ρ₂ hyp i (var x)      = refl
    /-↑⋆ ρ₁ ρ₂ hyp i (Λ t)        = cong Λ      (/-↑⋆ ρ₁ ρ₂ hyp (1 N+ 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)
    /-↑⋆ ρ₁ ρ₂ hyp i (x)      = {!!}

    /-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 (finlift 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 KtxLemmas where
    open KtxSubst hiding (ktx-map)

    private module Tp  = TypeLemmas
    private module Var = VarSubst

    ktx-map-cong : ∀ {ν μ n} {f g : Type ν → Type μ} →
                   f ≗ g → _≗_ {A = Ktx ν n} (ktx-map f) (ktx-map g)
    ktx-map-cong K = ?

    -- Term variable substitution (renaming) commutes with type
    -- substitution.
    {-
    /Var-/ : ∀ {m ν n l} (ρ : Sub Fin m n) (Γ : Ktx ν 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} {Γ : Ktx ν n} {a} → (ktx-weaken Γ) / (Tp.sub a) ≡ Γ
    ctx-weaken-sub-vanishes {Γ = Γ} {a} = begin
      (Γ / Tp.wk) / (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 Γ ⟩
      Γ ∎
    -}

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

    infixl 8 _/_

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

    -- Weakening of terms with additional type variables lifted to
    -- well-typed terms.
    weaken : ∀ {m n} {Γ : Ktx n m} {t : Term n m} {a : Type n} →
             Γ ⊢ t ∈ a → ktx-weaken Γ ⊢ tm-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} {Γ : Ktx n m} {ts : Vec (Term n m) k}
                  {as : Vec (Type n) k} → Γ ⊢ⁿ ts ∈ as →
                  ktx-weaken Γ ⊢ⁿ map tm-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} {Γ : Ktx (1 N+ n) m} {t a} →
            Γ ⊢ t ∈ a → (b : Type n) → Γ ktx/ sub b ⊢ t tm/tp 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   = KtxLemmas
      TmSub = TmTm.TermSub Term

    infix 4 _⇒_⊢_

    -- Well-typed term substitutions are collections of well-typed terms.
    _⇒_⊢_ : ∀ {ν m k} → Ktx ν m → Ktx ν k → TmSub ν m k → Set
    Γ ⇒ Δ ⊢ s = Δ ⊢ⁿ s ∈ (proj₁ Γ)

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

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

    -- Weakening of terms with additional term variables lifted to
    -- well-typed terms.
    weaken : ∀ {ν n} {K : Ktx ν n} {t : Term ν n} {a b : Type ν} →
             K ⊢ t ∈ a → b ∷Γ K ⊢ TmTm.weaken t ∈ a
    weaken {K = K} {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 : ∀ {ν n k} {K : Ktx ν n} {ts : Vec (Term ν n) k}
                  {as : Vec (Type ν) k} {b : Type ν} →
                K ⊢ⁿ ts ∈ as → (b ∷Γ K) ⊢ⁿ map TmTm.weaken ts ∈ as
    weakenAll {ts = []}    {[]}    []         = []
    weakenAll {ts = _ ∷ _} {_ ∷ _} (⊢t ∷ ⊢ts) = weaken ⊢t ∷ weakenAll ⊢ts

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

    -- The well-typed identity substitution.
    id : ∀ {ν n} {K : Ktx ν n} → K ⇒ K ⊢ TmTm.id
    id {K = K} = ?
    -- id {zero}  {._} {K = [] , _}    = []
    -- id {suc _} {._} {K = a ∷ Γ , _} = id ↑

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

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

    -- Application of term substitutions lifted to well-typed terms
    _/_ : ∀ {ν n} {K : Ktx ν n} {Δ : Ktx ν n} {t a s} →
          K ⊢ t ∈ a → K ⇒ Δ ⊢ s → Δ ⊢ t TmTm./ s ∈ a
    new c       / ⊢ρ = new c
    var x       / ⊢ρ = lookup-⊢ x ⊢ρ
    _/_ {K = K} {Δ = Δ} {s = s} (Λ ⊢t) ⊢ρ = Λ (⊢t / weaken-⊢p)
      where
        weaken-⊢p : ktx-weaken K ⇒ ktx-weaken Δ ⊢ map tm-weaken s
        weaken-⊢p = (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 BasicIS4.Metatheory.DyadicGentzen-BasicKripkeBozicDosen where

open import BasicIS4.Syntax.DyadicGentzen public
open import BasicIS4.Semantics.BasicKripkeBozicDosen public hiding (_⊨_) -- TODO

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊨ A
eval (var i)           γ δ = lookup i γ
eval (lam t)           γ δ = λ ξ a → eval t (mono⊩⋆ ξ γ , a) (λ ζ →
                               let _ , (ζ′ , ξ′) = ≤⨾R→R⨾≤ (_ , (ξ , ζ))
                               in  mono⊩⋆ ξ′ (δ ζ′))
eval (app {A} {B} t u) γ δ = _⟪$⟫_ {A} {B} (eval t γ δ) (eval u γ δ)
eval (mvar i)          γ δ = lookup i (δ reflR)
eval (box t)           γ δ = λ ζ → eval t ∙ (λ ζ′ → δ (transR ζ ζ′))
eval (unbox t u)       γ δ = eval u γ (λ ζ → δ ζ , (eval t γ δ) ζ)
eval (pair t u)        γ δ = eval t γ δ , eval u γ δ
eval (fst t)           γ δ = π₁ (eval t γ δ)
eval (snd t)           γ δ = π₂ (eval t γ δ)
eval unit              γ δ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Coirc.Network.Primitive where
{-# IMPORT Coirc.Network.FFI #-}
{-# IMPORT System.IO #-}
open import Data.String
open import IO.Primitive
open import Foreign.Haskell

postulate Handle : Set
{-# COMPILED_TYPE Handle System.IO.Handle #-}

postulate hConnect : String → IO Handle
{-# COMPILED hConnect Coirc.Network.FFI.hConnect #-}

postulate hPutStr : Handle → String → IO Unit
{-# COMPILED hPutStr System.IO.hPutStr #-}

postulate hGetLine : Handle → IO String
{-# COMPILED hGetLine System.IO.hGetLine #-}

max_stars_repo_name: larrytheliquid/coirc

max_issues_repo_name: larrytheliquid/coirc

max_forks_repo_name: larrytheliquid/coirc


text:
module Algebra.Dioid.Bool.Theorems where

open import Algebra.Dioid
open import Algebra.Dioid.Bool

or-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b or d) ≡ (c or d)
or-left-congruence {b} {.b} {d} reflexivity = reflexivity
or-left-congruence {b} {c} {d} (symmetry eq) = symmetry (or-left-congruence eq)
or-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-left-congruence eq) (or-left-congruence eq₁)

or-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b or c) ≡ (b or d)
or-right-congruence {b} {c} {.c} reflexivity = reflexivity
or-right-congruence {b} {c} {d} (symmetry eq) = symmetry (or-right-congruence eq)
or-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (or-right-congruence eq) (or-right-congruence eq₁)

and-left-congruence : ∀ {b c d : Bool} -> b ≡ c -> (b and d) ≡ (c and d)
and-left-congruence {b} {.b} {d} reflexivity = reflexivity
and-left-congruence {b} {c} {d} (symmetry eq) = symmetry (and-left-congruence eq)
and-left-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-left-congruence eq) (and-left-congruence eq₁)

and-right-congruence : ∀ {b c d : Bool} -> c ≡ d -> (b and c) ≡ (b and d)
and-right-congruence {b} {c} {.c} reflexivity = reflexivity
and-right-congruence {b} {c} {d} (symmetry eq) = symmetry (and-right-congruence eq)
and-right-congruence {b} {c} {d} (transitivity eq eq₁) = transitivity (and-right-congruence eq) (and-right-congruence eq₁)

or-idempotence : ∀ {b : Bool} -> (b or b) ≡ b
or-idempotence {true} = reflexivity
or-idempotence {false} = reflexivity

or-commutativity : ∀ {b c : Bool} -> (b or c) ≡ (c or b)
or-commutativity {true} {true} = reflexivity
or-commutativity {true} {false} = reflexivity
or-commutativity {false} {true} = reflexivity
or-commutativity {false} {false} = reflexivity

or-associativity : ∀ {b c d : Bool} -> (b or (c or d)) ≡ ((b or c) or d)
or-associativity {true} {c} {d} = reflexivity
or-associativity {false} {true} {d} = reflexivity
or-associativity {false} {false} {true} = reflexivity
or-associativity {false} {false} {false} = reflexivity

or-false-identity : ∀ {b : Bool} -> (b or false) ≡ b
or-false-identity {true} = reflexivity
or-false-identity {false} = reflexivity

and-associativity : ∀ {b c d : Bool} -> (b and (c and d)) ≡ ((b and c) and d)
and-associativity {true} {true} {true} = reflexivity
and-associativity {true} {true} {false} = reflexivity
and-associativity {true} {false} {d} = reflexivity
and-associativity {false} {c} {d} = reflexivity

and-left-false : ∀ {b : Bool} -> (false and b) ≡ false
and-left-false {b} = reflexivity

and-right-false : ∀ {b : Bool} -> (b and false) ≡ false
and-right-false {true} = reflexivity
and-right-false {false} = reflexivity

and-left-true : ∀ {b : Bool} -> (true and b) ≡ b
and-left-true {true} = reflexivity
and-left-true {false} = reflexivity

and-right-true : ∀ {b : Bool} -> (b and true) ≡ b
and-right-true {true} = reflexivity
and-right-true {false} = reflexivity

left-distributivity : ∀ {b c d : Bool} -> (b and (c or d)) ≡ ((b and c) or (b and d))
left-distributivity {true} {true} {d} = reflexivity
left-distributivity {true} {false} {true} = reflexivity
left-distributivity {true} {false} {false} = reflexivity
left-distributivity {false} {c} {d} = reflexivity

right-distributivity : ∀ {b c d : Bool} -> ((b or c) and d) ≡ ((b and d) or (c and d))
right-distributivity {true} {true} {true} = reflexivity
right-distributivity {true} {true} {false} = reflexivity
right-distributivity {true} {false} {true} = reflexivity
right-distributivity {true} {false} {false} = reflexivity
right-distributivity {false} {true} {true} = reflexivity
right-distributivity {false} {true} {false} = reflexivity
right-distributivity {false} {false} {d} = reflexivity

bool-dioid : Dioid Bool _≡_
bool-dioid = record
  { zero = false
  ; one  = true
  ; _+_  = _or_
  ; _*_  = _and_
  ; reflexivity  = reflexivity
  ; symmetry     = symmetry
  ; transitivity = transitivity

  ; +left-congruence  = or-left-congruence
  ; *left-congruence  = and-left-congruence
  ; *right-congruence = and-right-congruence

  ; +idempotence   = or-idempotence
  ; +commutativity = or-commutativity
  ; +associativity = or-associativity
  ; +zero-identity = or-false-identity

  ; *associativity  = and-associativity
  ; *left-zero      = λ {r} → reflexivity
  ; *right-zero     = and-right-false
  ; *left-identity  = and-left-true
  ; *right-identity = and-right-true

  ; left-distributivity  = left-distributivity
  ; right-distributivity = right-distributivity
  }

max_stars_repo_name: snowleopard/alga-proofs

max_issues_repo_name: snowleopard/alga-proofs

max_forks_repo_name: snowleopard/alga-proofs