text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.AbGroup.TensorProduct where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function hiding (flip)
open import Cubical.Foundations.Isomorphism

open import Cubical.Relation.Binary

open import Cubical.Data.Sigma

open import Cubical.Data.List
open import Cubical.Data.Nat as ℕ
open import Cubical.Foundations.HLevels
open import Cubical.Data.Int
open import Cubical.Data.Sum hiding (map)

open import Cubical.HITs.PropositionalTruncation
  renaming (map to pMap ; rec to pRec ; elim to pElim ; elim2 to pElim2)

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

private
  variable
    ℓ ℓ' : Level

module _ (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  data _⨂₁_ : Type (ℓ-max ℓ ℓ') where
   _⊗_ : (a : A) → (b : B) → _⨂₁_
   _+⊗_ : (w : _⨂₁_) → (u : _⨂₁_) → _⨂₁_

   ⊗comm : (x y : _) → x +⊗ y ≡ y +⊗ x
   ⊗assoc : (x y z : _) → x +⊗ (y +⊗ z) ≡ (x +⊗ y) +⊗ z
   ⊗lUnit : (x : _) → (0A ⊗ 0B) +⊗ x ≡ x

   linl : (x y : A) (z : B) → (x +A y) ⊗ z ≡ ((x ⊗ z) +⊗ (y ⊗ z))
   linr : (x : A) (y z : B) → x ⊗ (y +B z) ≡ ((x ⊗ y) +⊗ (x ⊗ z))

   ⊗squash : isSet _⨂₁_

module _ {AGr : AbGroup ℓ} {BGr : AbGroup ℓ'} where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  A⊗B = AGr ⨂₁ BGr

  ⊗elimProp : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ}
           → ((x : _) → isProp (C x))
           → (f : (x : A) (b : B) → C (x ⊗ b))
           → (g : ((x y : _) → C x → C y → C (x +⊗ y)))
           → (x : _) → C x
  ⊗elimProp p f g (a ⊗ b) = f a b
  ⊗elimProp p f g (x +⊗ y) = g x y (⊗elimProp p f g x) (⊗elimProp p f g y)
  ⊗elimProp  {C = C} p f g (⊗comm x y j) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g x y (⊗elimProp p f g x) (⊗elimProp p f g y))
      (g y x (⊗elimProp p f g y) (⊗elimProp p f g x)) (⊗comm x y) j
  ⊗elimProp {C = C} p f g (⊗assoc x y z j) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g x (y +⊗ z) (⊗elimProp p f g x)
         (g y z (⊗elimProp p f g y) (⊗elimProp p f g z)))
         (g (x +⊗ y) z (g x y (⊗elimProp p f g x)
           (⊗elimProp p f g y)) (⊗elimProp p f g z)) (⊗assoc x y z) j
  ⊗elimProp {C = C} p f g (⊗lUnit x i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (g (0A ⊗ 0B) x (f 0A 0B) (⊗elimProp p f g x))
      (⊗elimProp p f g x)
      (⊗lUnit x) i
  ⊗elimProp {C = C} p f g (linl x y z i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (f (x +A y) z) (g (x ⊗ z) (y ⊗ z) (f x z) (f y z)) (linl x y z) i
  ⊗elimProp {C = C} p f g (linr x y z i) =
    isOfHLevel→isOfHLevelDep 1 {B = C} p
      (f x (y +B z)) (g (x ⊗ y) (x ⊗ z) (f x y) (f x z)) (linr x y z) i
  ⊗elimProp {C = C} p f g (⊗squash x y q r i j) =
    isOfHLevel→isOfHLevelDep 2 {B = C} (λ x → isProp→isSet (p x))
      _ _ (λ j → ⊗elimProp p f g (q j)) (λ j → ⊗elimProp p f g (r j))
          (⊗squash x y q r) i j

  -- Group structure
  0⊗ : AGr ⨂₁ BGr
  0⊗ = 0A ⊗ 0B

  -⊗ : AGr ⨂₁ BGr → AGr ⨂₁ BGr
  -⊗ (a ⊗ b) = (-A a) ⊗ b
  -⊗ (x +⊗ x₁) = -⊗ x +⊗ -⊗ x₁
  -⊗ (⊗comm x y i) = ⊗comm (-⊗ x) (-⊗ y) i
  -⊗ (⊗assoc x y z i) = ⊗assoc (-⊗ x) (-⊗ y) (-⊗ z) i
  -⊗ (⊗lUnit x i) =
    ((λ i → (GroupTheory.inv1g (AbGroup→Group AGr) i ⊗ 0B) +⊗ -⊗ x)
       ∙ ⊗lUnit (-⊗ x)) i
  -⊗ (linl x y z i) =
     ((λ i → (GroupTheory.invDistr (AbGroup→Group AGr) x y
             ∙ comm strA (-A y) (-A x)) i ⊗ z)
    ∙ linl (-A x) (-A y) z) i
  -⊗ (linr x y z i) = linr (-A x) y z i
  -⊗ (⊗squash x y p q i j) =
    ⊗squash _ _ (λ j → -⊗ (p j)) (λ j → -⊗ (q j)) i j

  ⊗rUnit : (x : A⊗B) → x +⊗ 0⊗ ≡ x
  ⊗rUnit x = ⊗comm x 0⊗ ∙ ⊗lUnit x

  -------------------------------------------------------------------------------
  -- Useful induction principle, which lets us view elements of A ⨂ B as lists
  -- over (A × B). Used for the right cancellation law
  unlist : List (A × B) → AGr ⨂₁ BGr
  unlist [] = 0A ⊗ 0B
  unlist (x ∷ x₁) = (fst x ⊗ snd x) +⊗ unlist x₁

  unlist++ : (x y : List (A × B))
            → unlist (x ++ y) ≡ (unlist x +⊗ unlist y)
  unlist++ [] y = sym (⊗lUnit (unlist y))
  unlist++ (x ∷ x₁) y =
       (λ i → (fst x ⊗ snd x) +⊗ (unlist++ x₁ y i))
     ∙ ⊗assoc (fst x ⊗ snd x) (unlist x₁) (unlist y)

  ∃List : (x : AGr ⨂₁ BGr) → ∃[ l ∈ List (A × B) ] (unlist l ≡ x)
  ∃List =
    ⊗elimProp (λ _ → squash₁)
      (λ a b → ∣ [ a , b ] , ⊗rUnit (a ⊗ b) ∣₁)
      λ x y → rec2 squash₁ λ {(l1 , p) (l2 , q)
                          → ∣ (l1 ++ l2) , unlist++ l1 l2 ∙ cong₂ _+⊗_ p q ∣₁}

  ⊗elimPropUnlist : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ}
           → ((x : _) → isProp (C x))
           → ((x : _) → C (unlist x))
           → (x : _) → C x
  ⊗elimPropUnlist {C = C} p f =
    ⊗elimProp p (λ x y → subst C (⊗rUnit (x ⊗ y)) (f [ x , y ]))
      λ x y → pRec (isPropΠ2 λ _ _ → p _)
                    (pRec (isPropΠ3 λ _ _ _ → p _)
                      (λ {(l1 , p) (l2 , q) ind1 ind2
                        → subst C (unlist++ l2 l1 ∙ cong₂ _+⊗_ q p) (f (l2 ++ l1))})
                      (∃List y))
                    (∃List x)
  -----------------------------------------------------------------------------------

  lCancelPrim : (x : B) → (0A ⊗ x) ≡ 0⊗
  lCancelPrim x =
    sym (⊗rUnit _)
    ∙∙ cong ((0A ⊗ x) +⊗_) (sym cancelLem)
    ∙∙ ⊗assoc (0A ⊗ x) (0A ⊗ x) (0A ⊗ (-B x))
    ∙∙ cong (_+⊗ (0A ⊗ (-B x))) inner
    ∙∙ cancelLem
    where
    cancelLem : (0A ⊗ x) +⊗ (0A ⊗ (-B x)) ≡ 0⊗
    cancelLem = sym (linr 0A x (-B x)) ∙ (λ i → 0A ⊗ invr strB x i)

    inner : (0A ⊗ x) +⊗ (0A ⊗ x) ≡ 0A ⊗ x
    inner = sym (linl 0A 0A x) ∙ (λ i → rid strA 0A i ⊗ x)

  rCancelPrim : (x : A) → (x ⊗ 0B) ≡ 0⊗
  rCancelPrim x =
    sym (⊗rUnit _)
    ∙∙ cong ((x ⊗ 0B) +⊗_) (sym cancelLem)
    ∙∙ ⊗assoc (x ⊗ 0B) (x ⊗ 0B) ((-A x) ⊗ 0B)
    ∙∙ cong (_+⊗ ((-A x) ⊗ 0B)) inner
    ∙∙ cancelLem
    where
    cancelLem : (x ⊗ 0B) +⊗ ((-A x) ⊗ 0B) ≡ 0⊗
    cancelLem = sym (linl x (-A x) 0B) ∙ (λ i → invr strA x i ⊗ 0B)

    inner : (x ⊗ 0B) +⊗ (x ⊗ 0B) ≡ x ⊗ 0B
    inner = sym (linr x 0B 0B) ∙ (λ i → x ⊗ rid strB 0B i)

  flip : (x : A) (b : B) → x ⊗ (-B b) ≡ ((-A x) ⊗ b)
  flip x b =
    sym (⊗rUnit _)
    ∙ cong ((x ⊗ (-B b)) +⊗_) (sym cancelLemA)
    ∙ ⊗assoc (x ⊗ (-B b)) (x ⊗ b) ((-A x) ⊗ b)
    ∙ cong (_+⊗ ((-A x) ⊗ b)) cancelLemB
    ∙ ⊗lUnit _
    where
    cancelLemA : (x ⊗ b) +⊗ ((-A x) ⊗ b) ≡ 0⊗
    cancelLemA = sym (linl x (-A x) b) ∙ (λ i → invr strA x i ⊗ b) ∙ lCancelPrim b

    cancelLemB : (x ⊗ (-B b)) +⊗ (x ⊗ b) ≡ 0⊗
    cancelLemB = sym (linr x (-B b) b) ∙ (λ i → x ⊗ invl strB b i) ∙ rCancelPrim x

  ⊗rCancel : (x : AGr ⨂₁ BGr) → (x +⊗ -⊗ x) ≡ 0⊗
  ⊗rCancel =
    ⊗elimPropUnlist (λ _ → ⊗squash _ _) h
    where
    h : (x : List (A × B)) → (unlist x +⊗ -⊗ (unlist x)) ≡ 0⊗
    h [] = sym (linl 0A (-A 0A) (0B))
         ∙ cong (λ x →  _⊗_ {AGr = AGr} {BGr = BGr} x 0B) (invr strA 0A)
    h (x ∷ x₁) =
      move4 (fst x ⊗ snd x) (unlist x₁) ((-A fst x) ⊗ snd x) (-⊗ (unlist x₁))
            _+⊗_ ⊗assoc ⊗comm
      ∙∙ cong₂ _+⊗_ (sym (linl (fst x) (-A (fst x)) (snd x))
                   ∙∙ (λ i → invr strA (fst x) i ⊗ (snd x))
                   ∙∙ lCancelPrim (snd x))
                    (h x₁)
      ∙∙ ⊗rUnit 0⊗

  ⊗lCancel : (x : AGr ⨂₁ BGr) → (-⊗ x +⊗ x) ≡ 0⊗
  ⊗lCancel x = ⊗comm _ _ ∙ ⊗rCancel x

module _ where
  open AbGroupStr
  open IsAbGroup
  open IsGroup
  open IsMonoid
  open IsSemigroup

  _⨂_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')
  fst (A ⨂ B) = A ⨂₁ B
  0g (snd (A ⨂ B)) = 0⊗
  AbGroupStr._+_ (snd (A ⨂ B)) = _+⊗_
  AbGroupStr.- snd (A ⨂ B) = -⊗
  is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (A ⨂ B)))))) = ⊗squash
  assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd (A ⨂ B)))))) = ⊗assoc
  fst (identity (isMonoid (isGroup (isAbGroup (snd (A ⨂ B))))) x) = ⊗rUnit x
  snd (identity (isMonoid (isGroup (isAbGroup (snd (A ⨂ B))))) x) = ⊗lUnit x
  fst (inverse (isGroup (isAbGroup (snd (A ⨂ B)))) x) = ⊗rCancel x
  snd (inverse (isGroup (isAbGroup (snd (A ⨂ B)))) x) = ⊗lCancel x
  comm (isAbGroup (snd (A ⨂ B))) = ⊗comm

-------------- Elimination principle into AbGroups --------------
module _ {ℓ ℓ' : Level} {A : AbGroup ℓ}  {B : AbGroup ℓ'} where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G)
    _+A_ = _+G_ (snd A)
    _+B_ = _+G_ (snd B)

    0A = 0g (snd A)
    0B = 0g (snd B)

  ⨂→AbGroup-elim : ∀ {ℓ} (C : AbGroup ℓ)
         → (f : (fst A × fst B) → fst C)
         → (f (0A , 0B) ≡ 0g (snd C))
         → (linL : (x y : fst A) (b : fst B)
                 → f (x +A y , b) ≡ _+G_ (snd C) (f (x , b)) (f (y , b)))
         → (linR : (a : fst A) (x y : fst B)
                 → f (a , x +B y) ≡ _+G_ (snd C) (f (a , x)) (f (a , y)))
         → A ⨂₁ B → fst C
  ⨂→AbGroup-elim C f p linL linR (a ⊗ b) = f (a , b)
  ⨂→AbGroup-elim C f p linL linR (x +⊗ x₁) =
    _+G_ (snd C) (⨂→AbGroup-elim C f p linL linR x)
                 (⨂→AbGroup-elim C f p linL linR x₁)
  ⨂→AbGroup-elim C f p linL linR (⊗comm x x₁ i) =
    comm (snd C) (⨂→AbGroup-elim C f p linL linR x)
                 (⨂→AbGroup-elim C f p linL linR x₁) i
  ⨂→AbGroup-elim C f p linL linR (⊗assoc x x₁ x₂ i) =
    assoc (snd C) (⨂→AbGroup-elim C f p linL linR x)
                  (⨂→AbGroup-elim C f p linL linR x₁)
                  (⨂→AbGroup-elim C f p linL linR x₂) i
  ⨂→AbGroup-elim C f p linL linR (⊗lUnit x i) =
    (cong (λ y → (snd C +G y) (⨂→AbGroup-elim C f p linL linR x)) p
                     ∙ (lid (snd C) (⨂→AbGroup-elim C f p linL linR x))) i
  ⨂→AbGroup-elim C f p linL linR (linl x y z i) = linL x y z i
  ⨂→AbGroup-elim C f p linL linR (linr x y z i) = linR x y z i
  ⨂→AbGroup-elim C f p linL linR (⊗squash x x₁ x₂ y i i₁) =
    is-set (snd C) _ _
           (λ i → ⨂→AbGroup-elim C f p linL linR (x₂ i))
           (λ i → ⨂→AbGroup-elim C f p linL linR (y i)) i i₁

  ⨂→AbGroup-elim-hom : ∀ {ℓ} (C : AbGroup ℓ)
        → (f : (fst A × fst B) → fst C) (linL : _) (linR : _) (p : _)
        → AbGroupHom (A ⨂ B) C
  fst (⨂→AbGroup-elim-hom C f linL linR p) = ⨂→AbGroup-elim C f p linL linR
  snd (⨂→AbGroup-elim-hom C f linL linR p) =
    makeIsGroupHom
      (λ x y → refl)

private
  _* = AbGroup→Group

----------- Definition of universal property ------------
tensorFun : (A : Group ℓ) (B : Group ℓ') (T C : AbGroup (ℓ-max ℓ ℓ'))
    (f : GroupHom A (HomGroup B T *))
  → GroupHom (T *) (C *)
  → GroupHom A (HomGroup B C *)
fst (fst (tensorFun A B T C (f , p) (g , q)) a) b = g (fst (f a) b)
snd (fst (tensorFun A B T C (f , p) (g , q)) a) =
    makeIsGroupHom λ x y
      → cong g (IsGroupHom.pres· (snd (f a)) x y)
       ∙ IsGroupHom.pres· q _ _
snd (tensorFun A B T C (f , p) (g , q)) =
     makeIsGroupHom λ x y
      → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
           (funExt λ b
             → cong g (funExt⁻ (cong fst (IsGroupHom.pres· p x y)) b)
              ∙ IsGroupHom.pres· q _ _)

isTensorProductOf_and_ : AbGroup ℓ → AbGroup ℓ' → AbGroup (ℓ-max ℓ ℓ')→ Type _
isTensorProductOf_and_ {ℓ} {ℓ'} A B T =
  Σ[ f ∈ GroupHom (A *) ((HomGroup (B *) T) *) ]
    ((C : AbGroup (ℓ-max ℓ ℓ'))
      → isEquiv {A = GroupHom (T *) (C *)}
                 {B = GroupHom (A *) ((HomGroup (B *) C) *)}
          (tensorFun (A *) (B *) T C f))

------ _⨂_ satisfies the universal property --------
module UP (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where
  private
    open AbGroupStr renaming (_+_ to _+G_ ; -_ to -G_)

    strA = snd AGr
    strB = snd BGr

    A = fst AGr
    B = fst BGr

    0A = 0g strA
    0B = 0g strB

    _+A_ = _+G_ strA
    _+B_ = _+G_ strB

    -A_ = -G_ strA
    -B_ = -G_ strB

  mainF : GroupHom (AGr *) (HomGroup (BGr *) (AGr ⨂ BGr) *)
  fst (fst mainF a) b = a ⊗ b
  snd (fst mainF a) =
    makeIsGroupHom (linr a)
  snd mainF =
    makeIsGroupHom λ x y → Σ≡Prop (λ _ → isPropIsGroupHom _ _)
      (funExt (linl x y))

  isTensorProduct⨂ : (isTensorProductOf AGr and BGr) (AGr ⨂ BGr)
  fst isTensorProduct⨂ = mainF
  snd isTensorProduct⨂ C = isoToIsEquiv mainIso
    where
    invF : GroupHom (AGr *) (HomGroup (BGr *) C *) → GroupHom ((AGr ⨂ BGr) *) (C *)
    fst (invF (f , p)) = F
      where
      lem : f (0g (snd AGr)) .fst (0g (snd BGr)) ≡ 0g (snd C)
      lem = funExt⁻ (cong fst (IsGroupHom.pres1 p)) (0g (snd BGr))
      F : ((AGr ⨂ BGr) *) .fst → (C *) .fst
      F (a ⊗ b) = f a .fst b
      F (x +⊗ x₁) = _+G_ (snd C) (F x) (F x₁)
      F (⊗comm x x₁ i) = comm (snd C) (F x) (F x₁) i
      F (⊗assoc x y z i) = assoc (snd C) (F x) (F y) (F z) i
      F (⊗lUnit x i) = (cong (λ y → _+G_ (snd C) y (F x)) lem ∙ lid (snd C) (F x)) i
      F (linl x y z i) = fst (IsGroupHom.pres· p x y i) z
      F (linr x y z i) = IsGroupHom.pres· (f x .snd) y z i
      F (⊗squash x x₁ x₂ y i i₁) =
        is-set (snd C) (F x) (F x₁)
          (λ i → F (x₂ i)) (λ i → F (y i)) i i₁
    snd (invF (f , p)) =
      makeIsGroupHom λ x y → refl

    mainIso : Iso (GroupHom ((AGr ⨂ BGr) *) (C *))
                  (GroupHom (AGr *) (HomGroup (BGr *) C *))
    Iso.fun mainIso = _
    Iso.inv mainIso = invF
    Iso.rightInv mainIso (f , p) =
      Σ≡Prop (λ _ → isPropIsGroupHom _ _)
             (funExt λ a → Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl)
    Iso.leftInv mainIso (f , p) =
      Σ≡Prop (λ _ → isPropIsGroupHom _ _)
             (funExt (⊗elimProp (λ _ → is-set (snd C) _ _)
               (λ _ _ → refl)
               λ x y ind1 ind2 → cong₂ (_+G_ (snd C)) ind1 ind2 ∙ sym (IsGroupHom.pres· p x y)))

-------------------- Commutativity ------------------------
commFun : ∀ {ℓ ℓ'} {A : AbGroup ℓ}  {B : AbGroup ℓ'} → A ⨂₁ B → B ⨂₁ A
commFun (a ⊗ b) = b ⊗ a
commFun (x +⊗ x₁) = commFun x +⊗ commFun x₁
commFun (⊗comm x x₁ i) = ⊗comm (commFun x) (commFun x₁) i
commFun (⊗assoc x x₁ x₂ i) = ⊗assoc (commFun x) (commFun x₁) (commFun x₂) i
commFun (⊗lUnit x i) = ⊗lUnit (commFun x) i
commFun (linl x y z i) = linr z x y i
commFun (linr x y z i) = linl y z x i
commFun (⊗squash x x₁ x₂ y i i₁) =
  ⊗squash (commFun x) (commFun x₁)
          (λ i → commFun (x₂ i)) (λ i → commFun (y i)) i i₁

commFun²≡id : ∀ {ℓ ℓ'} {A : AbGroup ℓ}  {B : AbGroup ℓ'} (x : A ⨂₁ B)
          → commFun (commFun x) ≡ x
commFun²≡id =
  ⊗elimProp (λ _ → ⊗squash _ _)
    (λ _ _ → refl)
    λ _ _ p q → cong₂ _+⊗_ p q

⨂-commIso : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'}
          → GroupIso ((A ⨂ B) *) ((B ⨂ A) *)
Iso.fun (fst ⨂-commIso) = commFun
Iso.inv (fst ⨂-commIso) = commFun
Iso.rightInv (fst ⨂-commIso) = commFun²≡id
Iso.leftInv (fst ⨂-commIso) = commFun²≡id
snd ⨂-commIso = makeIsGroupHom λ x y → refl

⨂-comm : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} → AbGroupEquiv (A ⨂ B) (B ⨂ A)
fst ⨂-comm = isoToEquiv (fst (⨂-commIso))
snd ⨂-comm = snd ⨂-commIso

open AbGroupStr

-------------------- Associativity ------------------------
module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where
  private
    f : (c : fst C) → AbGroupHom (A ⨂ B) (A ⨂ (B ⨂ C))
    f c = ⨂→AbGroup-elim-hom (A ⨂ (B ⨂ C)) ((λ ab → fst ab ⊗ (snd ab ⊗ c)))
                  (λ x y b → linl x y (b ⊗ c))
                  (λ x y b → (λ i → x ⊗ (linl y b c i)) ∙ linr x (y ⊗ c) (b ⊗ c))
                  (λ i → 0g (snd A) ⊗ (lCancelPrim c i))

  assocHom : AbGroupHom ((A ⨂ B) ⨂ C) (A ⨂ (B ⨂ C))
  assocHom =
    ⨂→AbGroup-elim-hom _ (λ x → f (snd x) .fst (fst x))
      (λ x y b → IsGroupHom.pres· (snd (f b)) x y)
      (⊗elimProp (λ _ → isPropΠ2 λ _ _ → ⊗squash _ _)
                 (λ a b x y → (λ i → a ⊗ (linr b x y i))
                            ∙∙ linr a (b ⊗ x) (b ⊗ y)
                            ∙∙ refl)
                 λ a b ind1 ind2 x y → cong₂ _+⊗_ (ind1 x y) (ind2 x y)
                       ∙∙ move4 (f x .fst a) (f y .fst a) (f x .fst b) (f y .fst b)
                                _+⊗_ ⊗assoc ⊗comm
                       ∙∙ cong₂ _+⊗_ (sym (IsGroupHom.pres· (snd (f x)) a b))
                                     (IsGroupHom.pres· (snd (f y)) a b))
      refl

module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGroup ℓ''} where
  private
    f' : (a : fst A) → AbGroupHom (B ⨂ C) ((A ⨂ B) ⨂ C)
    f' a =
      ⨂→AbGroup-elim-hom ((A ⨂ B) ⨂ C)
         (λ bc → (a ⊗ fst bc) ⊗ snd bc)
         (λ x y b → (λ i → (linr a x y i) ⊗ b) ∙ linl (a ⊗ x) (a ⊗ y) b)
         (λ x y b → linr (a ⊗ x) y b)
         λ i → rCancelPrim a i ⊗ (0g (snd C))

  assocHom⁻ : AbGroupHom (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C)
  assocHom⁻ =
    ⨂→AbGroup-elim-hom _ (λ abc → f' (fst abc) .fst (snd abc))
       (λ x y → ⊗elimProp (λ _ → ⊗squash _ _)
                   (λ b c → (λ i → linl x y b i ⊗ c) ∙ linl (x ⊗ b) (y ⊗ b) c)
                   λ a b ind1 ind2 → cong₂ _+⊗_ ind1 ind2
                                  ∙∙ move4 _ _ _ _ _+⊗_ ⊗assoc ⊗comm
                                  ∙∙ cong₂ _+⊗_ (IsGroupHom.pres· (snd (f' x)) a b)
                                                (IsGroupHom.pres· (snd (f' y)) a b))
       (λ a → IsGroupHom.pres· (snd (f' a)))
       refl

  ⨂assocIso : Iso (A ⨂₁ (B ⨂ C)) ((A ⨂ B) ⨂₁ C)
  Iso.fun ⨂assocIso = fst assocHom⁻
  Iso.inv ⨂assocIso = fst assocHom
  Iso.rightInv ⨂assocIso =
    ⊗elimProp (λ _ → ⊗squash _ _)
      (⊗elimProp (λ _ → isPropΠ (λ _ → ⊗squash _ _))
        (λ a b c → refl)
        λ a b ind1 ind2 c → cong₂ _+⊗_ (ind1 c) (ind2 c) ∙ sym (linl a b c))
      λ x y p q → cong (fst assocHom⁻) (IsGroupHom.pres· (snd assocHom) x y)
               ∙∙ IsGroupHom.pres· (snd assocHom⁻) (fst assocHom x) (fst assocHom y)
               ∙∙ cong₂ _+⊗_ p q
  Iso.leftInv ⨂assocIso =
    ⊗elimProp (λ _ → ⊗squash _ _)
      (λ a → ⊗elimProp (λ _ → ⊗squash _ _)
              (λ b c → refl)
              λ x y ind1 ind2 →
                   cong (fst assocHom ∘ fst assocHom⁻) (linr a x y)
                ∙∙ cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) (a ⊗ x) (a ⊗ y))
                ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ (a ⊗ x)) (fst assocHom⁻ (a ⊗ y))
                ∙∙ cong₂ _+⊗_ ind1 ind2
                ∙∙ sym (linr a x y))
      λ x y p q → cong (fst assocHom) (IsGroupHom.pres· (snd assocHom⁻) x y)
               ∙∙ IsGroupHom.pres· (snd assocHom) (fst assocHom⁻ x) (fst assocHom⁻ y)
               ∙∙ cong₂ _+⊗_ p q

  ⨂assoc : AbGroupEquiv (A ⨂ (B ⨂ C)) ((A ⨂ B) ⨂ C)
  fst ⨂assoc = isoToEquiv ⨂assocIso
  snd ⨂assoc = snd assocHom⁻

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
open import Preliminaries

module Preorder where

  record Preorder-str (A : Set) : Set1 where
    constructor preorder
    field
      ≤ : A → A → Set
      refl : ∀ x → ≤ x x
      trans : ∀ x y z → ≤ x y → ≤ y z → ≤ x z
      prop : ∀ x y → (p q : ≤ x y) → p == q

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

  -- Task 1: Show that the Natural numbers with ≤ form a preorder

  -- the ≤ relation on Natural numbers
  ≤nat : Nat → Nat → Set
  ≤nat Z Z = Unit
  ≤nat Z (S y) = Unit
  ≤nat (S x) Z = Void
  ≤nat (S x) (S y) = ≤nat x y

  -- proof that Nat is reflexive under ≤
  nat-refl : ∀ (x : Nat) → ≤nat x x
  nat-refl Z = <>
  nat-refl (S x) = nat-refl x

  -- proof that Nat is transitive under ≤
  nat-trans : ∀ (x y z : Nat) → ≤nat x y → ≤nat y z → ≤nat x z
  nat-trans Z Z Z p q = <>
  nat-trans Z Z (S z) p q = <>
  nat-trans Z (S y) Z p q = abort q
  nat-trans Z (S y) (S z) p q = <>
  nat-trans (S x) Z Z () q
  nat-trans (S x) Z (S z) () q
  nat-trans (S x) (S y) Z p ()
  nat-trans (S x) (S y) (S z) p q = nat-trans x y z p q

  nat-prop : ∀ (x y : Nat) → (p q : ≤nat x y) → p == q
  nat-prop Z Z <> <> = Refl
  nat-prop Z (S y) <> <> = Refl
  nat-prop (S x) Z () q
  nat-prop (S x) (S y) p q = nat-prop x y p q

  -- proof that Nat and ≤ (the ≤ relation defined on the natural numbers) form a preorder
  nat-p : Preorder-str Nat
  nat-p = preorder ≤nat nat-refl nat-trans nat-prop

  --discrete nat
  nat-eq : Nat → Nat → Set
  nat-eq Z Z = Unit
  nat-eq Z (S n) = Void
  nat-eq (S m) Z = Void
  nat-eq (S m) (S n) = nat-eq m n

  ♭nat-refl : (x : Nat) → nat-eq x x
  ♭nat-refl Z = <>
  ♭nat-refl (S x) = ♭nat-refl x

  ♭nat-trans : (x y z : Nat) → nat-eq x y → nat-eq y z → nat-eq x z
  ♭nat-trans Z Z Z x x₁ = <>
  ♭nat-trans Z Z (S z) x ()
  ♭nat-trans Z (S y) z () x₁
  ♭nat-trans (S x) Z z () x₂
  ♭nat-trans (S x) (S y) Z x₁ x₂ = x₂
  ♭nat-trans (S x) (S y) (S z) x₁ x₂ = ♭nat-trans x y z x₁ x₂

  ♭nat-prop : ∀ (x y : Nat) → (p q : nat-eq x y) → p == q
  ♭nat-prop Z Z <> <> = Refl
  ♭nat-prop Z (S y) () q
  ♭nat-prop (S x) Z () q
  ♭nat-prop (S x) (S y) p q = ♭nat-prop x y p q

  ♭nat-p : Preorder-str Nat
  ♭nat-p = preorder nat-eq ♭nat-refl ♭nat-trans ♭nat-prop

  --bools
  ≤b : Bool → Bool → Set
  ≤b True True = Unit
  ≤b True False = Void
  ≤b False True = Void
  ≤b False False = Unit

  b-refl : (x : Bool) → ≤b x x
  b-refl True = <>
  b-refl False = <>

  b-trans : (x y z : Bool) → ≤b x y → ≤b y z → ≤b x z
  b-trans True True True x x₁ = <>
  b-trans True True False x ()
  b-trans True False z () x₁
  b-trans False True z () x₁
  b-trans False False True x ()
  b-trans False False False x x₁ = <>

  b-prop : ∀ (x y : Bool) → (p q : ≤b x y) → p == q
  b-prop True True <> <> = Refl
  b-prop True False () q
  b-prop False True () q
  b-prop False False <> <> = Refl

  bool-p : Preorder-str Bool
  bool-p = preorder ≤b b-refl b-trans b-prop

  --list
  ≤list : ∀ {A : Set} → Preorder-str A → List A → List A → Set
  ≤list PA [] [] = Unit
  ≤list PA [] (x :: l2) = Void
  ≤list PA (x :: l1) [] = Void
  ≤list PA (x :: l1) (x₁ :: l2) = Preorder-str.≤ PA x x₁ × ≤list PA l1 l2

  l-refl : ∀ {A : Set} → (PA : Preorder-str A) → (l : List A) → ≤list PA l l
  l-refl PA [] = <>
  l-refl PA (x :: l) = (Preorder-str.refl PA x) , (l-refl PA l)

  l-trans : ∀ {A : Set} → (PA : Preorder-str A) → (l1 l2 l3 : List A) → ≤list PA l1 l2 → ≤list PA l2 l3 → ≤list PA l1 l3
  l-trans PA [] [] [] p q = <>
  l-trans PA [] [] (x :: l3) p ()
  l-trans PA [] (x :: l2) l3 () q
  l-trans PA (x :: l1) [] l3 () q
  l-trans PA (x :: l1) (x₁ :: l2) [] p ()
  l-trans PA (x :: l1) (x₁ :: l2) (x₂ :: l3) p q = (Preorder-str.trans PA x x₁ x₂ (fst p) (fst q)) , (l-trans PA l1 l2 l3 (snd p) (snd q))

  l-prop : ∀ {A : Set} → (PA : Preorder-str A) → (x y : List A) → (p q : ≤list PA x y) → p == q
  l-prop PA [] [] <> <> = Refl
  l-prop PA [] (x :: y) () q
  l-prop PA (x :: x₁) [] () q
  l-prop PA (x :: x₁) (x₂ :: y) (p1 , p2) (q1 , q2) = ap2 (λ x₃ x₄ → x₃ , x₄) (Preorder-str.prop PA x x₂ p1 q1) (l-prop PA x₁ y p2 q2)

  list-p : ∀ {A : Set} (PA : Preorder-str A) → Preorder-str (List A)
  list-p PA = preorder (≤list PA) (l-refl PA) (l-trans PA) (l-prop PA)

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

  -- Task 2: Show that the product of two preorders is a preorder

  {- defining the relation: when is one cartesian product 'less than' another?
     if A and B are preorders and we have cartesian products (a1,b1) and (a2,b2)
     such that a1,a2 ∈ A and b1,b2 ∈ B,
     then (a1,b1)≤(a2,b2) iff a1≤a2 and b1≤b2
  -}
  ≤axb : ∀ {A B : Set} → Preorder-str A → Preorder-str B → (A × B) → (A × B) → Set
  ≤axb PA PB (a1 , b1) (a2 , b2) = Preorder-str.≤ PA a1 a2 × Preorder-str.≤ PB b1 b2

  {-  a cartesian product (a,b) is 'less than' itself
     if each component of the product is reflexive, i.e.
     just show that a is reflexive and b is reflexive
  -}
  axb-refl : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x : (A × B)) →  ≤axb PA PB x x
  axb-refl PA PB (a , b) = Preorder-str.refl PA a , Preorder-str.refl PB b

  -- same idea for transitivity...
  axb-trans : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y z : (A × B)) → ≤axb PA PB x y → ≤axb PA PB y z → ≤axb PA PB x z
  axb-trans PA PB (a1 , b1) (a2 , b2) (a3 , b3) (a1<a2 , b1<b2) (a2<a3 , b2<b3) =
                          Preorder-str.trans PA a1 a2 a3 a1<a2 a2<a3 , Preorder-str.trans PB b1 b2 b3 b1<b2 b2<b3

  axb-prop : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y : (A × B)) → (p q : ≤axb PA PB x y) → p == q
  axb-prop PA PB (x1 , x2) (y1 , y2) (p1 , p2) (q1 , q2) = ap2 (λ x x₁ → x , x₁) (Preorder-str.prop PA x1 y1 p1 q1) (Preorder-str.prop PB x2 y2 p2 q2)

  -- proof that AxB is a preorder
  axb-p : ∀ (A B : Set) → Preorder-str A → Preorder-str B → Preorder-str (A × B)
  axb-p A B pre-a pre-b = record { ≤ = ≤axb pre-a pre-b; refl = axb-refl pre-a pre-b; trans = axb-trans pre-a pre-b; prop = axb-prop pre-a pre-b}

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

  -- Task 4: Show that given a Preorder A and Preorder B, Preorder (Monotone A B)

  -- the type of monotone functions from A to B
  -- i.e. functions which give you bigger outputs when you give them bigger inputs
  record Monotone (A : Set) (B : Set) (PA : Preorder-str A) (PB : Preorder-str B) : Set where
    constructor monotone
    field
      f : A → B
      is-monotone : ∀ (x y : A) → Preorder-str.≤ PA x y → Preorder-str.≤ PB (f x) (f y)

  -- the order on monotone functions is just the
  -- pointwise order on the underlying functions
  ≤mono : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (Monotone A B PA PB) → (Monotone A B PA PB) → Set
  ≤mono {A} PA PB f g = (x : A) → Preorder-str.≤ PB (Monotone.f f x) (Monotone.f g x)

  mono-refl : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x : (Monotone A B PA PB)) → ≤mono PA PB x x
  mono-refl PA PB f = λ x → Preorder-str.refl PB (Monotone.f f x)

  mono-trans : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y z : (Monotone A B PA PB)) → ≤mono PA PB x y → ≤mono PA PB y z → ≤mono PA PB x z
  mono-trans PA PB f g h p q = λ x → Preorder-str.trans PB (Monotone.f f x) (Monotone.f g x) (Monotone.f h x) (p x) (q x)

  mono-prop : ∀ {A B : Set} → (PA : Preorder-str A) → (PB : Preorder-str B) → (x y : (Monotone A B PA PB)) → (p q : ≤mono PA PB x y) → p == q
  mono-prop PA PB x y p q = λ= (λ x₁ → Preorder-str.prop PB (Monotone.f x x₁) (Monotone.f y x₁) (p x₁) (q x₁))

  mono-p : ∀ (A B : Set) → (PA : Preorder-str A) → (PB : Preorder-str B) → Preorder-str (Monotone A B PA PB)
  mono-p A B PA PB = preorder (≤mono PA PB) (mono-refl PA PB) (mono-trans PA PB) (mono-prop PA PB)

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

-- New stuff: Interpreting types as preorders

  -- repackaging preorder as a type together with a Preorder structure on that type
  PREORDER = Σ (λ (A : Set) → Preorder-str A)

  MONOTONE : (PΓ PA : PREORDER) → Set
  MONOTONE (Γ , PΓ) (A , PA) = Monotone Γ A PΓ PA

  PN : PREORDER
  PN = Nat , nat-p

  PL : PREORDER → PREORDER
  PL (A , PA) = (List A) , list-p PA

  -- some operations
  _×p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ×p (B , PB) = A × B , axb-p A B PA PB

  _->p_ : PREORDER → PREORDER → PREORDER
  (A , PA) ->p (B , PB) = Monotone A B PA PB , mono-p A B PA PB

  -- Unit is a preorder
  unit-p : PREORDER
  unit-p = Unit , preorder (λ x x₁ → Unit) (λ x → <>) (λ x y z _ _ → <>) (λ x y p q → Refl)

  -- identity preserves monotonicity
  id : ∀ {Γ} → MONOTONE Γ Γ
  id = λ {Γ} → monotone (λ x → x) (λ x y x₁ → x₁)

  -- composition preserves monotonicity
  comp : ∀ {PA PB PC} → MONOTONE PA PB → MONOTONE PB PC → MONOTONE PA PC
  comp (monotone f f-ismono) (monotone g g-ismono) = monotone (λ x → g (f x)) (λ x y x₁ → g-ismono (f x) (f y) (f-ismono x y x₁))

  -- proofs that types like pairs etc. with preorders are monotone
  pair' : ∀ {PΓ PA PB} → MONOTONE PΓ PA → MONOTONE PΓ PB → MONOTONE PΓ (PA ×p PB)
  pair' (monotone f f-ismono) (monotone g g-ismono) = monotone (λ x → f x , g x) (λ x y z → f-ismono x y z , g-ismono x y z)

  fst' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PA
  fst' (monotone f f-ismono) = monotone (λ x → fst (f x)) (λ x y z → fst (f-ismono x y z))

  snd' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ×p PB) → MONOTONE PΓ PB
  snd' (monotone f f-ismono) = monotone (λ x → snd (f x)) (λ x y z → snd (f-ismono x y z))

  lam' : ∀ {PΓ PA PB} → MONOTONE (PΓ ×p PA) PB → MONOTONE PΓ (PA ->p PB)
  lam' {Γ , preorder ≤Γ reflΓ transΓ pΓ} {a , preorder ≤a refla transa pa} {b , _} (monotone f f-ismono) =
          monotone (λ x → monotone (λ p → f (x , p)) (λ a b c → f-ismono (x , a) (x , b) (reflΓ x , c))) (λ x y z w → f-ismono (x , w) (y , w) (z , refla w))

  app' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ->p PB) → MONOTONE PΓ PA → MONOTONE PΓ PB
  app' {Γ , preorder ≤Γ reflΓ transΓ pΓ} {a , preorder ≤a refla transa pa} {b , preorder ≤b reflb transb pb} (monotone f f-ismono) (monotone g g-ismono) =
          monotone (λ x → Monotone.f (f x) (g x))
            (λ x y z → transb
              (Monotone.f (f x) (g x))
              (Monotone.f (f y) (g x))
              (Monotone.f (f y) (g y))
                (f-ismono x y z (g x))
                (Monotone.is-monotone (f y) (g x) (g y) (g-ismono x y z)))

  unlam' : ∀ {PΓ PA PB} → MONOTONE PΓ (PA ->p PB) → MONOTONE (PΓ ×p PA) PB
  unlam' {Γ , preorder ≤Γ reflΓ transΓ pΓ} {a , preorder ≤a refla transa pa} {b , preorder ≤b reflb transb pb} (monotone f f-ismono) =
    monotone (λ x → Monotone.f (f (fst x)) (snd x))
      (λ x y x₁ → transb
        (Monotone.f (f (fst x)) (snd x))
        (Monotone.f (f (fst x)) (snd y))
        (Monotone.f (f (fst y)) (snd y))
          (Monotone.is-monotone (f (fst x)) (snd x) (snd y) (snd x₁))
          (f-ismono (fst x) (fst y) (fst x₁) (snd y)))

  z' : ∀ {PΓ} → MONOTONE PΓ PN
  z' = monotone (λ x → Z) (λ x y x₁ → <>)

  suc' : ∀ {PΓ} → MONOTONE PΓ PN → MONOTONE PΓ PN
  suc' {Γ , preorder ≤ refl trans pΓ} (monotone f f-is-monotone) = monotone (λ x → S (f x)) (λ x y x₁ → f-is-monotone x y x₁)

  nil' : ∀ {PΓ PA} → MONOTONE PΓ (PL PA)
  nil' = monotone (λ x → []) (λ x y x₁ → <>)

  cons' : ∀ {PΓ PA} → MONOTONE PΓ PA → MONOTONE PΓ (PL PA) → MONOTONE PΓ (PL PA)
  cons' (monotone f is-monotone) (monotone f₁ is-monotone₁) = monotone (λ x → f x :: f₁ x) (λ x y x₁ → (is-monotone x y x₁) , (is-monotone₁ x y x₁))

  lrec : ∀ {A C : Set} → (l : List A) → (nil : C) → (cons : A → List A → C → C) → C
  lrec [] nil cons = nil
  lrec (x :: l) nil cons = cons x l (lrec l nil cons)

  listrec-fix-args : ∀ {PΓ PA PC} → (enil : MONOTONE PΓ PC) → (econs : MONOTONE (((PΓ ×p PC) ×p PL PA) ×p PA) PC)
                   → (x y : fst (PΓ ×p PL PA)) → (Preorder-str.≤ (snd (PΓ ×p PL PA)) x y)
                   → Preorder-str.≤ (snd PC)
                       (lrec (snd x) (Monotone.f enil (fst x)) (λ x₁ x₂ x₃ → Monotone.f econs (((fst x , x₃) , x₂) , x₁)))
                       (lrec (snd y) (Monotone.f enil (fst x)) (λ x₁ x₂ x₃ → Monotone.f econs (((fst x , x₃) , x₂) , x₁)))
  listrec-fix-args {_} {_} {fst₂ , preorder ≤₂ refl₂ trans₂ p₂} enil _ (x , []) (y , []) p = refl₂ (Monotone.f enil x)
  listrec-fix-args _ _ (_ , []) (_ , x₁ :: ys) (_ , ())
  listrec-fix-args _ _ (_ , x₁ :: xs) (_ , []) (_ , ())
  listrec-fix-args {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} {fst₂ , preorder ≤₂ refl₂ trans₂ p3}
    enil (monotone f is-monotone) (x , x₁ :: xs) (y , x₂ :: ys) (x≤y , (hlt , tlt)) =
      is-monotone (((x , (lrec xs (Monotone.f enil x) (λ x₃ x₄ x₅ → f (((x , x₅) , x₄) , x₃)))) , xs) , x₁)
                  (((x , lrec ys (Monotone.f enil x) (λ x₃ x₄ x₅ → f (((x , x₅) , x₄) , x₃))) , ys) , x₂)
                    ((((refl x) , (listrec-fix-args enil (monotone f is-monotone) (x , xs) (y , ys) (x≤y , tlt))) , tlt) , hlt)

  listrec-fix-el : ∀ {PΓ PA PC} → (enil : MONOTONE PΓ PC) → (econs : MONOTONE (((PΓ ×p PC) ×p PL PA) ×p PA) PC)
                 → (x y : fst (PΓ ×p PL PA)) → (Preorder-str.≤ (snd (PΓ ×p PL PA)) x y)
                 → Preorder-str.≤ (snd PC)
                     (lrec (snd y) (Monotone.f enil (fst x)) (λ x₁ x₂ x₃ → Monotone.f econs (((fst x , x₃) , x₂) , x₁)))
                     (lrec (snd y) (Monotone.f enil (fst y)) (λ x₁ x₂ x₃ → Monotone.f econs (((fst y , x₃) , x₂) , x₁)))
  listrec-fix-el (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₃ , []) (fst₄ , []) (x≤y , <>) = is-monotone fst₃ fst₄ x≤y
  listrec-fix-el _ _ (_ , []) (_ , x₁ :: ys) (_ , ())
  listrec-fix-el _ _ (_ , x₁ :: xs) (_ , []) (_ , ())
  listrec-fix-el {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} {fst₂ , preorder ≤₂ refl₂ trans₂ p3}
    (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₃ , x :: xs) (fst₄ , y :: ys) (x≤y , hlt , tlt) =
      is-monotone₁ (((fst₃ , (lrec ys (f fst₃) (λ x₁ x₂ x₃ → f₁ (((fst₃ , x₃) , x₂) , x₁)))) , ys) , y)
                   (((fst₄ , (lrec ys (f fst₄) (λ x₁ x₂ x₃ → f₁ (((fst₄ , x₃) , x₂) , x₁)))) , ys) , y)
                     (((x≤y ,
                       listrec-fix-el {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} {fst₂ , preorder ≤₂ refl₂ trans₂ p3}
                                      (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₃ , xs) (fst₄ , ys) (x≤y , tlt)) ,
                       l-refl (preorder ≤₁ refl₁ trans₁ p2) ys) , (refl₁ y))

  lrec-cong : ∀ {PΓ PA PC} → (enil enil' : MONOTONE PΓ PC) → (econs econs' : MONOTONE (((PΓ ×p PC) ×p PL PA) ×p PA) PC)
            → (x : fst (PΓ ×p PL PA))
            → Preorder-str.≤ (snd (PΓ ->p PC)) enil enil'
            → Preorder-str.≤ (snd ((((PΓ ×p PC) ×p PL PA) ×p PA) ->p PC)) econs econs'
            → Preorder-str.≤ (snd PC)
                (lrec (snd x) (Monotone.f enil (fst x)) (λ x₁ x₂ x₃ → Monotone.f econs (((fst x , x₃) , x₂) , x₁)))
                (lrec (snd x) (Monotone.f enil' (fst x)) (λ x₁ x₂ x₃ → Monotone.f econs' (((fst x , x₃) , x₂) , x₁)))
  lrec-cong _ _ _ _ (x , []) p q = p x
  lrec-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} {fst₂ , preorder ≤₂ refl₂ trans₂ p3} en en' ec ec' (x , x₁ :: l) p q =
    trans₂
      (lrec (x₁ :: l) (Monotone.f en x) (λ x₂ x₃ x₄ → Monotone.f ec (((x , x₄) , x₃) , x₂)))
      (Monotone.f ec' (((x , lrec l (Monotone.f en x) (λ x₂ x₃ x₄ → Monotone.f ec (((x , x₄) , x₃) , x₂))) , l) , x₁))
      (lrec (x₁ :: l) (Monotone.f en' x) (λ x₂ x₃ x₄ → Monotone.f ec' (((x , x₄) , x₃) , x₂)))
        (q (((x , lrec l (Monotone.f en x) (λ x₂ x₃ x₄ → Monotone.f ec (((x , x₄) , x₃) , x₂))) , l) , x₁))
        (Monotone.is-monotone ec'
          (((x , lrec l (Monotone.f en x) (λ x₂ x₃ x₄ → Monotone.f ec (((x , x₄) , x₃) , x₂))) , l) , x₁)
          (((x , lrec l (Monotone.f en' x) (λ x₂ x₃ x₄ → Monotone.f ec' (((x , x₄) , x₃) , x₂))) , l) , x₁)
          ((((refl x) ,
          (lrec-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} {fst₂ , preorder ≤₂ refl₂ trans₂ p3} en en' ec ec' (x , l) p q)) ,
          (l-refl (preorder ≤₁ refl₁ trans₁ p2) l)) ,
          refl₁ x₁))

  lrec' : ∀ {PΓ PA PC} → (enil : MONOTONE PΓ PC) → (econs : MONOTONE (((PΓ ×p PC) ×p PL PA) ×p PA) PC) → MONOTONE (PΓ ×p PL PA) PC
  lrec' {Γ , preorder ≤Γ reflΓ transΓ pΓ} {A , preorder ≤A reflA transA pa} {C , preorder ≤C reflC transC pc} (monotone enil is-monotone) (monotone econs is-monotone₁) =
          monotone (λ x → lrec (snd x) (enil (fst x)) (λ x₁ x₂ x₃ → econs ((((fst x) , x₃) , x₂) , x₁)))
          (λ x y x₁ → transC
            (lrec (snd x) (enil (fst x)) (λ x₂ x₃ x₄ → econs (((fst x , x₄) , x₃) , x₂)))
            (lrec (snd y) (enil (fst x)) (λ x₂ x₃ x₄ → econs (((fst x , x₄) , x₃) , x₂)))
            (lrec (snd y) (enil (fst y)) (λ x₂ x₃ x₄ → econs (((fst y , x₄) , x₃) , x₂)))
              (listrec-fix-args {Γ , preorder ≤Γ reflΓ transΓ pΓ} {A , preorder ≤A reflA transA pa} {C , preorder ≤C reflC transC pc}
                (monotone enil is-monotone) (monotone econs is-monotone₁) x y x₁)
              (listrec-fix-el {Γ , preorder ≤Γ reflΓ transΓ pΓ} {A , preorder ≤A reflA transA pa} {C , preorder ≤C reflC transC pc}
                (monotone enil is-monotone) (monotone econs is-monotone₁) x y x₁))

  natrec : ∀{C : Set} → (base : C) → (step : Nat → C → C) → (n : Nat) → C
  natrec base step Z = base
  natrec base step (S n) = step n (natrec base step n)

  h-lem : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PN) ×p PC) PC) → (x y : fst (PΓ ×p PN))
         → (∀ x → Preorder-str.≤ (snd PC) (Monotone.f e0 x) (Monotone.f e1 ((x , 0) , Monotone.f e0 x)))
         → Preorder-str.≤ (snd PΓ) (fst x) (fst y)
         → Preorder-str.≤ (snd PC)
             (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , n) , x₂)) (snd x))
             (natrec (Monotone.f e0 (fst y)) (λ n x₂ → Monotone.f e1 ((fst y , n) , x₂)) (snd x))
  h-lem (monotone e0 e0-is-monotone) _ (x , Z) (y , m) p q = e0-is-monotone x y q
  h-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
         (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , S n) (y , m) p q =
           e1-is-monotone
             ((x , n) , natrec (e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) n)
             ((y , n) , natrec (e0 y) (λ n₁ x₂ → e1 ((y , n₁) , x₂)) n)
               ((q , (Preorder-str.refl nat-p n)) ,
                 (h-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , n) (y , m) p q))

  h-lem2-lem : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PN) ×p PC) PC) → (x : fst (PΓ ×p PN))
             → (∀ x → Preorder-str.≤ (snd PC) (Monotone.f e0 x) (Monotone.f e1 ((x , 0) , Monotone.f e0 x)))
             → Preorder-str.≤ (snd PC)
               (Monotone.f e0 (fst x))
               (Monotone.f e1 (((fst x) , (snd x)) , (natrec (Monotone.f e0 (fst x)) (λ x₁ x₂ → Monotone.f e1 (((fst x) , x₁) , x₂)) (snd x))))
  h-lem2-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
             (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , Z) p = p x
  h-lem2-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
             (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , S n) p =
               transc
                 (e0 x)
                 (e1 ((x , 0) , e0 x))
                 (e1 ((x , (S n)) , (natrec (e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) (S n))))
                   (p x)
                   (e1-is-monotone ((x , 0) , e0 x) ((x , (S n)) , (natrec (e0 x) (λ x₁ x₂ → e1 ((x , x₁) , x₂)) (S n)))
                     (((refl x) , <>) ,
                     h-lem2-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , n) p))

  h-lem2 : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PN) ×p PC) PC) → (x y : fst (PΓ ×p PN))
         → (∀ x → Preorder-str.≤ (snd PC) (Monotone.f e0 x) (Monotone.f e1 ((x , 0) , Monotone.f e0 x)))
         → Preorder-str.≤ (snd PN) (snd x) (snd y)
         → Preorder-str.≤ (snd PC)
             (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , n) , x₂)) (snd x))
             (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , n) , x₂)) (snd y))
  h-lem2 {_} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , Z) (y , Z) p q = reflc (e0 x)
  h-lem2 {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
         (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , Z) (y , S n) p q =
           h-lem2-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
             (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , n) (λ x₁ → p x₁)
  h-lem2 _ _ (x , S m) (y , Z) p ()
  h-lem2 {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
         (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , S m) (y , S n) p q =
           e1-is-monotone
             ((x , m) , (natrec (e0 x) (λ x₁ x₂ → e1 ((x , x₁) , x₂)) m))
             ((x , n) , natrec (e0 x) (λ x₁ x₂ → e1 ((x , x₁) , x₂)) n)
             (((refl x) , q) ,
               (h-lem2 {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
                 (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (x , m) (y , n) p q))

  h-cong : ∀ {PΓ PC} → (e0 e0' : MONOTONE PΓ PC) → (e1 e1' : MONOTONE ((PΓ ×p PN) ×p PC) PC) → (x : fst (PΓ ×p PN))
           → Preorder-str.≤ (snd (PΓ ->p PC)) e0 e0'
           → Preorder-str.≤ (snd (((PΓ ×p PN) ×p PC) ->p PC)) e1 e1'
           → Preorder-str.≤ (snd PC)
              (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , n) , x₂)) (snd x))
              (natrec (Monotone.f e0' (fst x)) (λ n x₂ → Monotone.f e1' ((fst x , n) , x₂)) (snd x))
  h-cong {_} {_} e0 e0' e1 e1' (x , Z) p q = p x
  h-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} e0 e0' (monotone e1 e1-is-monotone) (monotone e1' e1'-is-monotone) (x , S n) p q =
    trans₁
      (natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) (S n))
      (e1' ((x , n) , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) n))
      (natrec (Monotone.f e0' x) (λ n₁ x₂ → e1' ((x , n₁) , x₂)) (S n))
        (q ((x , n) , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) n))
        (e1'-is-monotone
          ((x , n) , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , n₁) , x₂)) n)
          ((x , n) , natrec (Monotone.f e0' x) (λ n₁ x₂ → e1' ((x , n₁) , x₂)) n)
          (((refl x) ,
          (nat-refl n)) ,
          h-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} e0 e0' (monotone e1 e1-is-monotone) (monotone e1' e1'-is-monotone) (x , n) p q))

  rec' : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PN) ×p PC) PC)
       → (∀ x → Preorder-str.≤ (snd PC) (Monotone.f e0 x) (Monotone.f e1 ((x , 0) , Monotone.f e0 x)))
       → MONOTONE (PΓ ×p PN) PC
  rec' {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) p =
          monotone (λ x → natrec (e0 (fst x)) (λ n x₂ → e1 ((fst x , n) , x₂)) (snd x))
            (λ x y x₁ →
              transc
                (natrec (e0 (fst x)) (λ n x₂ → e1 ((fst x , n) , x₂)) (snd x))
                (natrec (e0 (fst y)) (λ n x₂ → e1 ((fst y , n) , x₂)) (snd x))
                (natrec (e0 (fst y)) (λ n x₂ → e1 ((fst y , n) , x₂)) (snd y))
                  (h-lem {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
                    (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (fst x , snd x) (fst y , snd x) (λ x₂ → p x₂) (fst x₁))
                  (h-lem2 {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2}
                    (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) (fst y , snd x) (fst y , snd y) (λ x₂ → p x₂) (snd x₁)))

  h-cong2 : ∀ {PΓ PC} → (e0 e0' : MONOTONE PΓ PC) → (e1 e1' : MONOTONE ((PΓ ×p PN) ×p PC) PC)
          → Preorder-str.≤ (snd (PΓ ->p PC)) e0 e0'
          → Preorder-str.≤ (snd (((PΓ ×p PN) ×p PC) ->p PC)) e1 e1'
          → (x : ∀ x₁ → Preorder-str.≤ (snd PC) (Monotone.f e0 x₁) (Monotone.f e1 ((x₁ , 0) , Monotone.f e0 x₁)))
          → (y : ∀ x₁ → Preorder-str.≤ (snd PC) (Monotone.f e0' x₁) (Monotone.f e1' ((x₁ , 0) , Monotone.f e0' x₁)))
          → Preorder-str.≤ (snd ((PΓ ×p PN) ->p PC)) (rec' e0 e1 x) (rec' e0' e1' y)
  h-cong2 {_} {_} _ _ _ _ d1 d2 p q (el , Z) = d1 el
  h-cong2 {_} {_} e0 e0' e1 e1' d1 d2 p q (el , S n) = h-cong e0 e0' e1 e1' (el , (S n)) d1 d2

  ♭h-fix-args : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PC) ×p (Nat , ♭nat-p)) PC) → (x y : fst (PΓ ×p (Nat , ♭nat-p)))
              → nat-eq (snd x) (snd y)
              → Preorder-str.≤ (snd PC)
                (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , x₂) , n)) (snd x))
                (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , x₂) , n)) (snd y))
  ♭h-fix-args {_} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} (monotone f is-monotone) (monotone g is-monotone₁) (x , Z) (y , Z) p = refl₁ (f x)
  ♭h-fix-args (monotone f is-monotone) (monotone g is-monotone₁) (x , Z) (y , S n) ()
  ♭h-fix-args (monotone f is-monotone) (monotone g is-monotone₁) (x , S m) (y , Z) ()
  ♭h-fix-args {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} (monotone f is-monotone) (monotone g is-monotone₁) (x , S m) (y , S n) p =
    is-monotone₁ ((x , (natrec (f x) (λ n₁ x₂ → g ((x , x₂) , n₁)) m)) , m) ((x , (natrec (f x) (λ n₁ x₂ → g ((x , x₂) , n₁)) n)) , n)
      (((refl x) , (♭h-fix-args {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} (monotone f is-monotone) (monotone g is-monotone₁) (x , m) (y , n) p)) , p)

  ♭h-fix-el : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PC) ×p (Nat , ♭nat-p)) PC) → (x y : fst (PΓ ×p (Nat , ♭nat-p)))
           → Preorder-str.≤ (snd (PΓ ×p (Nat , ♭nat-p))) x y
           → Preorder-str.≤ (snd PC)
              (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , x₂) , n)) (snd y))
              (natrec (Monotone.f e0 (fst y)) (λ n x₂ → Monotone.f e1 ((fst y , x₂) , n)) (snd y))
  ♭h-fix-el {fst , preorder ≤ refl trans p≤} {_} (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₂ , Z) (fst₃ , Z) (p1 , p2) = is-monotone fst₂ fst₃ p1
  ♭h-fix-el (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₂ , Z) (fst₃ , S n) (fst₄ , ())
  ♭h-fix-el (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₂ , S m) (fst₃ , Z) (fst₄ , ())
  ♭h-fix-el {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₂ , S m) (fst₃ , S n) (fst₄ , snd) =
    is-monotone₁ ((fst₂ , (natrec (f fst₂) (λ n₁ x₂ → f₁ ((fst₂ , x₂) , n₁)) n)) , n) ((fst₃ , (natrec (f fst₃) (λ n₁ x₂ → f₁ ((fst₃ , x₂) , n₁)) n)) , n)
      ((fst₄ ,
      (♭h-fix-el {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2}
        (monotone f is-monotone) (monotone f₁ is-monotone₁) (fst₂ , m) (fst₃ , n) (fst₄ , snd))) ,
      (♭nat-refl n))

  ♭h-cong : ∀ {PΓ PC} → (e0 e0' : MONOTONE PΓ PC) → (e1 e1' : MONOTONE ((PΓ ×p PC) ×p (Nat , ♭nat-p)) PC) → (x : fst (PΓ ×p (Nat , ♭nat-p)))
           → Preorder-str.≤ (snd (PΓ ->p PC)) e0 e0'
           → Preorder-str.≤ (snd (((PΓ ×p PC) ×p (Nat , ♭nat-p)) ->p PC)) e1 e1'
           → Preorder-str.≤ (snd PC)
              (natrec (Monotone.f e0 (fst x)) (λ n x₂ → Monotone.f e1 ((fst x , x₂) , n)) (snd x))
              (natrec (Monotone.f e0' (fst x)) (λ n x₂ → Monotone.f e1' ((fst x , x₂) , n)) (snd x))
  ♭h-cong {_} {_} e0 e0' e1 e1' (x , Z) p q = p x
  ♭h-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} e0 e0' (monotone e1 e1-is-monotone) (monotone e1' e1'-is-monotone) (x , S n) p q =
    trans₁
      (natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , x₂) , n₁)) (S n))
      (e1' ((x , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , x₂) , n₁)) n) , n))
      (natrec (Monotone.f e0' x) (λ n₁ x₂ → e1' ((x , x₂) , n₁)) (S n))
        (q ((x , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , x₂) , n₁)) n) , n))
        (e1'-is-monotone
          ((x , natrec (Monotone.f e0 x) (λ n₁ x₂ → e1 ((x , x₂) , n₁)) n) , n)
          ((x , natrec (Monotone.f e0' x) (λ n₁ x₂ → e1' ((x , x₂) , n₁)) n) , n)
          (((refl x) ,
          ♭h-cong {fst , preorder ≤ refl trans p1} {fst₁ , preorder ≤₁ refl₁ trans₁ p2} e0 e0' (monotone e1 e1-is-monotone) (monotone e1' e1'-is-monotone) (x , n) p q) ,
          ♭nat-refl n))

  ♭rec' : ∀ {PΓ PC} → (e0 : MONOTONE PΓ PC) → (e1 : MONOTONE ((PΓ ×p PC) ×p (Nat , ♭nat-p)) PC) → MONOTONE (PΓ ×p (Nat , ♭nat-p)) PC
  ♭rec' {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) =
    monotone (λ x → natrec (e0 (fst x)) (λ n x₂ → e1 (((fst x) , x₂) , n)) (snd x))
      (λ x y x₁ → transc
        (natrec (e0 (fst x)) (λ n x₂ → e1 ((fst x , x₂) , n)) (snd x))
        (natrec (e0 (fst x)) (λ n x₂ → e1 ((fst x , x₂) , n)) (snd y))
        (natrec (e0 (fst y)) (λ n x₂ → e1 ((fst y , x₂) , n)) (snd y))
          (♭h-fix-args {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) x y (snd x₁))
          (♭h-fix-el {Γ , preorder ≤ refl trans p1} {C , preorder ≤c reflc transc p2} (monotone e0 e0-is-monotone) (monotone e1 e1-is-monotone) x y x₁))

--- extend Preorders so you can impose max on them if type has maximums

  record Preorder-max-str {A : Set} (PA : Preorder-str A) : Set where
    constructor preorder-max
    field
      max : A → A → A
      max-l : ∀ l r → Preorder-str.≤ PA l (max l r)
      max-r : ∀ l r → Preorder-str.≤ PA r (max l r)
      max-lub : ∀ k l r → Preorder-str.≤ PA l k → Preorder-str.≤ PA r k → Preorder-str.≤ PA (max l r) k

  nat-max : Nat → Nat → Nat
  nat-max Z n = n
  nat-max (S m) Z = S m
  nat-max (S m) (S n) = S (nat-max m n)

  nat-max-l : ∀ (l r : Nat) → ≤nat l (nat-max l r)
  nat-max-l Z Z = <>
  nat-max-l Z (S n) = <>
  nat-max-l (S m) Z = nat-refl m
  nat-max-l (S m) (S n) = nat-max-l m n

  nat-max-r : ∀ (l r : Nat) → ≤nat r (nat-max l r)
  nat-max-r Z Z = <>
  nat-max-r Z (S n) = nat-refl n
  nat-max-r (S m) Z = <>
  nat-max-r (S m) (S n) = nat-max-r m n

  nat-max-lub : ∀ (k l r : Nat) → ≤nat l k → ≤nat r k → ≤nat (nat-max l r) k
  nat-max-lub Z Z Z p q = <>
  nat-max-lub Z Z (S r) p ()
  nat-max-lub Z (S l) Z () q
  nat-max-lub Z (S l) (S r) () q
  nat-max-lub (S k) Z Z p q = <>
  nat-max-lub (S k) Z (S r) p q = q
  nat-max-lub (S k) (S l) Z p q = p
  nat-max-lub (S k) (S l) (S r) p q = nat-max-lub k l r p q

  nat-pM : Preorder-max-str nat-p
  nat-pM = preorder-max nat-max nat-max-l nat-max-r nat-max-lub

  unit-pM : Preorder-max-str (snd unit-p)
  unit-pM = preorder-max (λ x x₁ → <>) (λ l r → <>) (λ l r → <>) (λ k l r x x₁ → <>)

  axb-max : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
          → Preorder-max-str PA → Preorder-max-str PB → (A × B) → (A × B) → (A × B)
  axb-max PA PB (a1 , b1) (a2 , b2) = Preorder-max-str.max PA a1 a2 , Preorder-max-str.max PB b1 b2

  axb-max-l : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
            → (PMA : Preorder-max-str PA) → (PMB : Preorder-max-str PB) → (l r : (A × B)) → ≤axb PA PB l (axb-max PMA PMB l r)
  axb-max-l PMA PMB (a1 , b1) (a2 , b2) = Preorder-max-str.max-l PMA a1 a2 , Preorder-max-str.max-l PMB b1 b2

  axb-max-r : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
            → (PMA : Preorder-max-str PA) → (PMB : Preorder-max-str PB) → (l r : (A × B)) → ≤axb PA PB r (axb-max PMA PMB l r)
  axb-max-r PMA PMB (a1 , b1) (a2 , b2) = Preorder-max-str.max-r PMA a1 a2 , Preorder-max-str.max-r PMB b1 b2

  axb-max-lub : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
              → (PMA : Preorder-max-str PA) → (PMB : Preorder-max-str PB) → (k l r : (A × B))
              → ≤axb PA PB l k → ≤axb PA PB r k → ≤axb PA PB (axb-max PMA PMB l r) k
  axb-max-lub PMA PMB (k1 , k2) (l1 , l2) (r1 , r2) (l1<k1 , l2<k2) (r1<k1 , r2<k2) =
                 Preorder-max-str.max-lub PMA k1 l1 r1 l1<k1 r1<k1 , Preorder-max-str.max-lub PMB k2 l2 r2 l2<k2 r2<k2

  axb-pM : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
         → Preorder-max-str PA → Preorder-max-str PB → Preorder-max-str (axb-p A B PA PB)
  axb-pM PMA PMB = preorder-max (axb-max PMA PMB) (axb-max-l PMA PMB) (axb-max-r PMA PMB) (axb-max-lub PMA PMB)

  mono-max : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
           → Preorder-max-str PB
           → (Monotone A B PA PB) → (Monotone A B PA PB) → (Monotone A B PA PB)
  mono-max {A} {B} {PA} {PB} PMB (monotone f f-ismono) (monotone g g-ismono) =
           monotone (λ x → Preorder-max-str.max PMB (f x) (g x))
                    (λ x y x₁ → Preorder-max-str.max-lub PMB (Preorder-max-str.max PMB (f y) (g y)) (f x) (g x)
                    (Preorder-str.trans PB (f x) (f y)
                       (Preorder-max-str.max PMB (f y) (g y)) (f-ismono x y x₁)
                       (Preorder-max-str.max-l PMB (f y) (g y)))
                    (Preorder-str.trans PB (g x) (g y)
                       (Preorder-max-str.max PMB (f y) (g y)) (g-ismono x y x₁)
                       (Preorder-max-str.max-r PMB (f y) (g y))))

  mono-max-l : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
             → (PMB : Preorder-max-str PB) → (l r : Monotone A B PA PB) → ≤mono PA PB l (mono-max PMB l r)
  mono-max-l PMB f g = λ x → Preorder-max-str.max-l PMB (Monotone.f f x) (Monotone.f g x)

  mono-max-r : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
             → (PMB : Preorder-max-str PB) → (l r : Monotone A B PA PB) → ≤mono PA PB r (mono-max PMB l r)
  mono-max-r PMB f g = λ x → Preorder-max-str.max-r PMB (Monotone.f f x) (Monotone.f g x)

  mono-max-lub : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
               → (PMB : Preorder-max-str PB)
               → (k l r : Monotone A B PA PB)
               → ≤mono PA PB l k → ≤mono PA PB r k → ≤mono PA PB (mono-max PMB l r) k
  mono-max-lub PMB f g h p q = λ x → Preorder-max-str.max-lub PMB (Monotone.f f x) (Monotone.f g x) (Monotone.f h x) (p x) (q x)

  mono-pM : ∀ {A B : Set} {PA : Preorder-str A} {PB : Preorder-str B}
          → Preorder-max-str PB → Preorder-max-str (mono-p A B PA PB)
  mono-pM PMB = preorder-max (mono-max PMB) (mono-max-l PMB) (mono-max-r PMB) (mono-max-lub PMB)

  --???
  PREORDER-MAX = (Σ (λ (A : Set) → (PA : Preorder-str A) → Preorder-max-str PA))

  -- stuff I need for monotonicity of plus

  nat-lemma3 : ∀ (x : Nat) → ≤nat x (S x)
  nat-lemma3 Z = <>
  nat-lemma3 (S x) = nat-lemma3 x

  plus-lem' : ∀ (a b c : Nat) → ≤nat a b → ≤nat a (b + c)
  plus-lem' Z Z Z <> = <>
  plus-lem' Z Z (S c) <> = <>
  plus-lem' Z (S b) c x = <>
  plus-lem' (S a) Z c ()
  plus-lem' (S a) (S b) c x = plus-lem' a b c x

  plus-rh-S : (n m : Nat) → ≤nat (S (n + m)) (n + S m)
  plus-rh-S Z m = nat-refl m
  plus-rh-S (S n) m = plus-rh-S n m

  +-unit : ∀ (a : Nat) → ≤nat (a + 0) a
  +-unit Z = <>
  +-unit (S a) = +-unit a

  +-comm : ∀ (a b : Nat) → ≤nat (a + b) (b + a)
  +-comm Z b = plus-lem' b b Z (nat-refl b)
  +-comm (S a) b = nat-trans (S (a + b)) (S (b + a)) (b + S a) (+-comm a b) (plus-rh-S b a)

  plus-assoc : ∀ (a b c : Nat) → ≤nat (a + (b + c)) ((a + b) + c)
  plus-assoc Z b c = nat-refl (b + c)
  plus-assoc (S a) b c = plus-assoc a b c

  plus-assoc' : ∀ (a b c : Nat) → ≤nat ((a + b) + c) (a + (b + c))
  plus-assoc' Z b c = nat-refl (b + c)
  plus-assoc' (S a) b c = plus-assoc' a b c

  mutual
    plus-lem'' : ∀ (a b : Nat) → ≤nat a (b + a)
    plus-lem'' a Z = nat-refl a
    plus-lem'' Z (S b) = <>
    plus-lem'' (S a) (S b) = nat-trans a (b + a) (b + S a) (plus-lem'' a b) (plus-lem b a b (S a) (nat-refl b) (nat-lemma3 a))

    plus-lem : ∀ (a b c d : Nat) → ≤nat a c → ≤nat b d → ≤nat (a + b) (c + d)
    plus-lem Z b Z d p q = q
    plus-lem Z Z (S c) Z p q = <>
    plus-lem Z (S b) (S c) Z p ()
    plus-lem Z Z (S c) (S d) p q = <>
    plus-lem Z (S b) (S c) (S d) p q = nat-trans b d (c + S d) q (nat-trans d (S d) (c + S d) (nat-lemma3 d) (plus-lem'' (S d) c))
    plus-lem (S a) b Z d () q
    plus-lem (S a) b (S c) d p q = plus-lem a b c d p q

  el : PREORDER → Set
  el = fst

  PREORDER≤ : (PA : PREORDER) → el PA → el PA → Set
  PREORDER≤ PA = Preorder-str.≤ (snd PA)

ext: agda

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
module Common.Level where

open import Agda.Primitive public

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Binary.Core

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

open import Data.List hiding (drop)
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Compound {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Drop.Complete _≤_ tot≤
open import PLRTree.DropLast.Complete _≤_ tot≤
open import PLRTree.DropLast.Permutation _≤_ tot≤
open import PLRTree.Equality {A}
open import PLRTree.Order.Properties {A}
open import PLRTree.Push.Permutation _≤_ tot≤

lemma-drop-++ : {t : Tag}{x : A}{l r : PLRTree} → Complete (node t x l r) → flatten (drop (node t x l r)) ∼ (flatten l ++ flatten r)
lemma-drop-++ (perfect {leaf} {leaf} x leaf leaf ≃lf) = ∼[]
lemma-drop-++ (perfect {node perfect x' l' r'} {node perfect x'' l'' r''} x cl cr (≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'')) =
                 let _l = node perfect x' l' r' ;
                      _r = node perfect x'' l'' r'' ;
                      _l≃r = ≃nd x' x'' l'≃r' l''≃r'' l'≃l'' ;
                      cxlr = perfect x cl cr _l≃r ;
                      z = last (node perfect x _l _r) compound ;
                      t' = dropLast (node perfect x _l _r) ;
                      ct' = right x cl (lemma-dropLast-complete cr) (lemma-dropLast-≃ _l≃r compound)
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))) (lemma-dropLast-∼ cxlr)
lemma-drop-++ (left {l} {r} x cl cr l⋘r)
    with l | r | l⋘r | lemma-dropLast-⋘ l⋘r
... | leaf | _ | () | _
... | node perfect x' l' r' | _ | () | _
... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₁ ld⋘r
    with dropLast (node left x' l' r') | ld⋘r | lemma-dropLast-complete cl | lemma-dropLast-∼ (left x cl cr (l⋘ x' x'' l'⋘r' l''≃r'' r'≃l''))
... | leaf | () | _ | _
... | node perfect _ _ _ | () | _ | _
... | node left x''' l''' r''' | ld⋘r' | cld | fzt'∼flfr =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node left x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))) fzt'∼flfr
... | node right x''' l''' r''' | ld⋘r' | cld | fzt'∼flfr =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node right x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))) fzt'∼flfr
lemma-drop-++ (left x cl cr l⋘r) | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₂ ld≃r
    with dropLast (node left x' l' r') | ld≃r | lemma-dropLast-complete cl | lemma-dropLast-∼ (left x cl cr (l⋘ x' x'' l'⋘r' l''≃r'' r'≃l''))
... | leaf | () | _ | _
... | node perfect x''' l''' r''' | ld≃r' | cld | fzt'∼flfr =
                 let z = last (node left x (node left x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node perfect x (node perfect x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = perfect x cld cr ld≃r'
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t'))) fzt'∼flfr
... | node left _ _ _ | () | _ | _
... | node right _ _ _ | () | _ | _
lemma-drop-++ (left x cl cr l⋘r) | node right x' l' r' | leaf | () | _
lemma-drop-++ (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₁ ()
lemma-drop-++ (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₂ x'≃x''' =
                 let z = last (node left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) compound ;
                      t' = dropLast (node left x (node right x' (node perfect x'' leaf leaf) leaf) (node perfect x''' leaf leaf)) ;
                      ct' = perfect x (perfect x' leaf leaf ≃lf) cr x'≃x''' ;
                      fzt'∼flfr = lemma-dropLast-∼ (left x cl cr (x⋘ x' x'' x'''))
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
lemma-drop-++ (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₁ ld⋘r
    with dropLast (node right x' l' r') | ld⋘r | lemma-dropLast-complete cl | lemma-dropLast-∼ (left x cl cr (r⋘ x' x'' l⋙r l''≃r'' l'⋗l''))
... | leaf | () | _ | _
... | node perfect _ _ _ | () | _ | _
... | node left x''' l''' r''' | ld⋘r' | cld | fzt'∼flfr =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node left x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                  in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
... | node right x''' l''' r''' | ld⋘r' | cld | fzt'∼flfr =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node left x (node right x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = left x cld cr ld⋘r'
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
lemma-drop-++ (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₂ ld≃r
    with dropLast (node right x' l' r') | ld≃r | lemma-dropLast-complete cl | lemma-dropLast-∼ (left x cl cr (r⋘ x' x'' l⋙r l''≃r'' l'⋗l''))
... | leaf | () | _ | _
... | node perfect x''' l''' r''' | ld≃r' | cld | fzt'∼flfr =
                 let z = last (node left x (node right x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = node perfect x (node perfect x''' l''' r''') (node perfect x'' l'' r'') ;
                      ct' = perfect x cld cr ld≃r'
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
... | node left _ _ _ | () | _ | _
... | node right _ _ _ | () | _ | _
lemma-drop-++ (left x cl cr l⋘r) | node right x' l' r' | node left x'' l'' r'' | () | _
lemma-drop-++ (left x cl cr l⋘r) | node right x' l' r' | node right x'' l'' r'' | () | _
lemma-drop-++ (right {l} {r} x cl cr l⋙r)
    with l | r | l⋙r | lemma-dropLast-⋙ l⋙r
... | leaf | leaf | ⋙p () | _
... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') | _ = ∼x /head /head ∼[]
... | node perfect _ _ (node _ _ _ _) | leaf | ⋙p () | _
... | node perfect _ (node _ _ _ _) _ | leaf | ⋙p () | _
... | node left _ _ _ | leaf | ⋙p () | _
... | node right _ _ _ | leaf | ⋙p () | _
... | leaf | node perfect _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') | _ =
                 let z = last (node right x (node perfect x' l' r') (node perfect x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node perfect x'' l'' r'')) ;
                      ct' = left x (lemma-dropLast-complete cl) cr (lemma-dropLast-⋗ (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'') compound) ;
                      fzt'∼flfr = lemma-dropLast-∼ (right x cl cr (⋙p (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'')))
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
... | node left _ _ _ | node perfect _ _ _ | ⋙p () | _
... | node right _ _ _ | node perfect _ _ _ | ⋙p () | _
... | leaf | node left _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node left x'' l'' r'' | _l⋙r | inj₁ l⋙rd =
                 let z = last (node right x (node perfect x' l' r') (node left x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node left x'' l'' r'')) ;
                      ct' = right x cl (lemma-dropLast-complete cr) l⋙rd ;
                      fzt'∼flfr = lemma-dropLast-∼ (right x cl cr _l⋙r)
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
... | node perfect _ _ _ | node left _ _ _ | _  | inj₂ ()
... | node left _ _ _ | node left _ _ _ | ⋙p () | _
... | node right _ _ _ | node left _ _ _ | ⋙p () | _
... | leaf | node right _ _ _ | ⋙p () | _
... | node perfect x' l' r' | node right x'' l'' r'' | _l⋙r | inj₁ l⋙rd =
                 let z = last (node right x (node perfect x' l' r') (node right x'' l'' r'')) compound ;
                      t' = dropLast (node right x (node perfect x' l' r') (node right x'' l'' r'')) ;
                      ct' = right x cl (lemma-dropLast-complete cr) l⋙rd ;
                      fzt'∼flfr = lemma-dropLast-∼ (right x cl cr _l⋙r)
                 in trans∼ (lemma-push-∼ (lemma-setRoot-complete z ct') (≺-wf (setRoot z t')))  fzt'∼flfr
... | node perfect _ _ _ | node right _ _ _ | _ | inj₂ ()
... | node left _ _ _ | node right _ _ _ | ⋙p () | _
... | node right _ _ _ | node right _ _ _ | ⋙p () | _

lemma-drop-∼ : {t : Tag}{x : A}{l r : PLRTree} → Complete (node t x l r) → (x ∷ flatten (drop (node t x l r))) ∼ flatten (node t x l r)
lemma-drop-∼ (perfect x cl cr l≃r) = ∼x /head /head (lemma-drop-++ (perfect x cl cr l≃r))
lemma-drop-∼ (left x cl cr l⋘r) = ∼x /head /head (lemma-drop-++ (left x cl cr l⋘r))
lemma-drop-∼ (right x cl cr l⋙r) = ∼x /head /head (lemma-drop-++ (right x cl cr l⋙r))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Classical propositional logic, PHOAS approach, initial encoding

module Pi.Cp where

-- Types

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty : Set where
  UNIT  :             Ty
  _=>_  : Ty -> Ty -> Ty
  _&&_  : Ty -> Ty -> Ty
  _||_  : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth judgement

Cx : Set1
Cx = Ty -> Set

isTrue : Ty -> Cx -> Set
isTrue a tc = tc a

-- Terms

module Cp where
  infixl 1 _$_
  data Tm (tc : Cx) : Ty -> Set where
    var    : forall {a}     -> isTrue a tc               -> Tm tc a
    lam'   : forall {a b}   -> (isTrue a tc -> Tm tc b)  -> Tm tc (a => b)
    _$_    : forall {a b}   -> Tm tc (a => b) -> Tm tc a -> Tm tc b
    pair'  : forall {a b}   -> Tm tc a        -> Tm tc b -> Tm tc (a && b)
    fst    : forall {a b}   -> Tm tc (a && b)            -> Tm tc a
    snd    : forall {a b}   -> Tm tc (a && b)            -> Tm tc b
    left   : forall {a b}   -> Tm tc a                   -> Tm tc (a || b)
    right  : forall {a b}   -> Tm tc b                   -> Tm tc (a || b)
    case'  : forall {a b c} -> Tm tc (a || b) -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c
    abort' : forall {a}    -> (isTrue (NOT a) tc -> Tm tc FALSE) -> Tm tc a

  lam'' : forall {tc a b} -> (Tm tc a -> Tm tc b) -> Tm tc (a => b)
  lam'' f = lam' \x -> f (var x)

  case'' : forall {tc a b c} -> Tm tc (a || b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
  case'' xy f g = case' xy (\x -> f (var x)) (\y -> g (var y))

  abort'' : forall {tc a} -> (Tm tc (NOT a) -> Tm tc FALSE) -> Tm tc a
  abort'' f = abort' \na -> f (var na)

  syntax lam''   (\a -> b) = lam a => b
  syntax pair'   x y       = [ x , y ]
  syntax case''  xy (\x -> z1) (\y -> z2) = case xy of x => z1 or y => z2
  syntax abort'' (\x -> y) = abort x => y

  Thm : Ty -> Set1
  Thm a = forall {tc} -> Tm tc a
open Cp public

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Inductions where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
open import Data.Nat using (ℕ; _+_; _*_; _∸_) hiding (zero) renaming (suc to succ)

max_stars_repo_path: testData/parse/agda/open using.agda

max_stars_repo_name: dubinsky/intellij-dtlc

max_issues_repo_path: testData/parse/agda/open using.agda

max_issues_repo_name: dubinsky/intellij-dtlc

max_forks_repo_path: testData/parse/agda/open using.agda

max_forks_repo_name: dubinsky/intellij-dtlc


text:
------------------------------------------------------------------------
-- Properties satisfied by decidable total orders
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.Props.DecTotalOrder (dt : DecTotalOrder) where

open Relation.Binary.DecTotalOrder dt hiding (trans)
import Relation.Binary.NonStrictToStrict as Conv
open Conv _≈_ _≤_

strictTotalOrder : StrictTotalOrder
strictTotalOrder = record
  { isStrictTotalOrder = record
      { isEquivalence = isEquivalence
      ; trans         = trans isPartialOrder
      ; compare       = trichotomous Eq.sym _≟_ antisym total
      ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
      }
  }

open StrictTotalOrder strictTotalOrder public

max_issues_repo_name: larrytheliquid/Lemmachine


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Free.Evaluation (Σ : Signature) where

open import Fragment.Algebra.Free.Monad Σ
open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Free.Base Σ
open import Fragment.Algebra.Homomorphism Σ
open import Fragment.Setoid.Morphism as Morphism

open import Level using (Level)

open import Data.Empty using (⊥)
open import Data.Nat using (ℕ; suc)
open import Data.Fin using (Fin; zero; suc)
open import Data.Vec using (Vec; []; _∷_; map)
open import Data.Vec.Relation.Binary.Pointwise.Inductive
  using (Pointwise; []; _∷_)

open import Relation.Binary using (Setoid)
import Relation.Binary.PropositionalEquality as PE

private
  variable
    a b ℓ₁ ℓ₂ : Level

module _ (A : Algebra {a} {ℓ₁}) where

  private

    open Setoid ∥ A ∥/≈
    open import Relation.Binary.Reasoning.Setoid ∥ A ∥/≈

    mutual
      map-∣eval∣ : ∀ {n} → Vec (Term ∥ A ∥) n → Vec ∥ A ∥ n
      map-∣eval∣ []       = []
      map-∣eval∣ (x ∷ xs) = ∣eval∣ x ∷ map-∣eval∣ xs

      ∣eval∣ : Term ∥ A ∥ → ∥ A ∥
      ∣eval∣ (atom x)    = x
      ∣eval∣ (term f xs) = A ⟦ f ⟧ (map-∣eval∣ xs)

    mutual
      map-∣eval∣-cong : ∀ {n} {xs ys : Vec (Term ∥ A ∥) n}
                         → Pointwise (_~_ ∥ A ∥/≈) xs ys
                         → Pointwise ≈[ A ] (map-∣eval∣ xs)
                                          (map-∣eval∣ ys)
      map-∣eval∣-cong []       = []
      map-∣eval∣-cong (p ∷ ps) = ∣eval∣-cong p ∷ map-∣eval∣-cong ps

      ∣eval∣-cong : Congruent (_~_ ∥ A ∥/≈) ≈[ A ] ∣eval∣
      ∣eval∣-cong (atom p)                 = p
      ∣eval∣-cong {x = term op _} (term p) =
        (A ⟦ op ⟧-cong) (map-∣eval∣-cong p)

    ∣eval∣⃗ : Herbrand ∥ A ∥/≈ ↝ ∥ A ∥/≈
    ∣eval∣⃗ = record { ∣_∣      = ∣eval∣
                     ; ∣_∣-cong = ∣eval∣-cong
                     }

    ∣eval∣-args≡map : ∀ {n} {xs : Vec (Term ∥ A ∥) n}
                      → Pointwise _≈_ (map-∣eval∣ xs) (map ∣eval∣ xs)
    ∣eval∣-args≡map {xs = []}     = []
    ∣eval∣-args≡map {xs = x ∷ xs} = refl ∷ ∣eval∣-args≡map

    ∣eval∣-hom : Homomorphic (Free ∥ A ∥/≈) A ∣eval∣
    ∣eval∣-hom f []       = refl
    ∣eval∣-hom f (x ∷ xs) = sym ((A ⟦ f ⟧-cong) (∣eval∣-args≡map {xs = x ∷ xs}))

  eval : Free ∥ A ∥/≈ ⟿ A
  eval = record { ∣_∣⃗    = ∣eval∣⃗
                ; ∣_∣-hom = ∣eval∣-hom
                }

fold : ∀ {A : Setoid a ℓ₁} (B : Algebra {b} {ℓ₂})
       → (A ↝ ∥ B ∥/≈) → Free A ⟿ B
fold B f = (eval B) ⊙ bind (unit · f)

Env : (A : Algebra {a} {ℓ₁}) → ℕ → Set _
Env A n = Fin n → ∥ A ∥

env : ∀ {A : Algebra {a} {ℓ₁}} {n} → (Γ : Vec ∥ A ∥ n) → Env A n
env {A = _} {suc n} (x ∷ _)  zero    = x
env {A = A} {suc n} (_ ∷ xs) (suc i) = env {A = A} xs i

module _ {n}
  {S : Setoid a ℓ₁}
  (T : Setoid b ℓ₂)
  (f : S ↝ T)
  (g : Fin n → Setoid.Carrier T)
  where

  private

    open Setoid S renaming (Carrier to A) using ()
    open Setoid T renaming (Carrier to B)

    ∣sub∣ : BT A n → B
    ∣sub∣ (sta x) = Morphism.∣ f ∣ x
    ∣sub∣ (dyn x) = g x

    ∣sub∣-cong : Congruent (_≍_ S n) _≈_ ∣sub∣
    ∣sub∣-cong (sta p) = Morphism.∣ f ∣-cong p
    ∣sub∣-cong (dyn q) = reflexive (PE.cong g q)

  sub : Atoms S n ↝ T
  sub = record { ∣_∣      = ∣sub∣
               ; ∣_∣-cong = ∣sub∣-cong
               }

module _ {n}
  {A : Setoid a ℓ₁}
  (B : Algebra {b} {ℓ₂})
  (f : A ↝ ∥ B ∥/≈)
  (g : Fin n → ∥ B ∥)
  where

  subst : Free (Atoms A n) ⟿ B
  subst = fold B (sub ∥ B ∥/≈ f g)

ignore : ∀ (A : Setoid a ℓ₁) → PE.setoid ⊥ ↝ A
ignore _ = record { ∣_∣      = λ ()
                  ; ∣_∣-cong = λ {}
                  }

inst : ∀ {n} (A : Algebra {a} {ℓ₁})
       → Env A n → F n ⟿ A
inst {n = n} A θ = subst A (ignore ∥ A ∥/≈) θ

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


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

module Definition.Typed.EqualityRelation where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening using (_∷_⊆_)

-- Generic equality relation used with the logical relation

record EqRelSet : Set₁ where
  constructor eqRel
  field
    ---------------
    -- Relations --
    ---------------

    -- Equality of types
    _⊢_≅_^_   : Con Term → (A B : Term) → TypeInfo → Set

    -- Equality of terms
    _⊢_≅_∷_^_ : Con Term → (t u A : Term) → TypeInfo → Set

    -- Equality of neutral terms
    _⊢_~_∷_^_ : Con Term → (t u A : Term) → TypeInfo → Set

    ----------------
    -- Properties --
    ----------------

    -- Generic equality compatibility
    ~-to-≅ₜ : ∀ {k l A r Γ}
            → Γ ⊢ k ~ l ∷ A ^ r
            → Γ ⊢ k ≅ l ∷ A ^ r

    -- Judgmental conversion compatibility
    ≅-eq  : ∀ {A B r Γ}
          → Γ ⊢ A ≅ B ^ r
          → Γ ⊢ A ≡ B ^ r
    ≅ₜ-eq : ∀ {t u A r Γ}
          → Γ ⊢ t ≅ u ∷ A ^ r
          → Γ ⊢ t ≡ u ∷ A ^ r

    -- Universe
    ≅-univ : ∀ {A B r l Γ}
           → Γ ⊢ A ≅ B ∷ (Univ r l) ^ [ ! , next l ]
           → Γ ⊢ A ≅ B ^ [ r , ι l ]

    ≅-un-univ : ∀ {A B r l Γ}
           → Γ ⊢ A ≅ B ^ [ r , ι l ]
           → Γ ⊢ A ≅ B ∷ (Univ r l) ^ [ ! , next l ]

    -- Symmetry
    ≅-sym  : ∀ {A B Γ r} → Γ ⊢ A ≅ B ^ r → Γ ⊢ B ≅ A ^ r
    ≅ₜ-sym : ∀ {t u A r Γ} → Γ ⊢ t ≅ u ∷ A ^ r → Γ ⊢ u ≅ t ∷ A ^ r
    ~-sym  : ∀ {k l A Γ r} → Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ l ~ k ∷ A ^ r

    -- Transitivity
    ≅-trans  : ∀ {A B C r Γ} → Γ ⊢ A ≅ B ^ r → Γ ⊢ B ≅ C ^ r → Γ ⊢ A ≅ C ^ r
    ≅ₜ-trans : ∀ {t u v A r Γ} → Γ ⊢ t ≅ u ∷ A ^ r → Γ ⊢ u ≅ v ∷ A ^ r → Γ ⊢ t ≅ v ∷ A ^ r
    ~-trans  : ∀ {k l m A r Γ} → Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ l ~ m ∷ A ^ r → Γ ⊢ k ~ m ∷ A ^ r

    -- Conversion
    ≅-conv : ∀ {t u A B r Γ} → Γ ⊢ t ≅ u ∷ A ^ r → Γ ⊢ A ≡ B ^ r → Γ ⊢ t ≅ u ∷ B ^ r
    ~-conv : ∀ {k l A B r Γ} → Γ ⊢ k ~ l ∷ A ^ r → Γ ⊢ A ≡ B ^ r → Γ ⊢ k ~ l ∷ B ^ r

    -- Weakening
    ≅-wk  : ∀ {A B r ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ A ≅ B ^ r
          → Δ ⊢ wk ρ A ≅ wk ρ B ^ r
    ≅ₜ-wk : ∀ {t u A r ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ t ≅ u ∷ A ^ r
          → Δ ⊢ wk ρ t ≅ wk ρ u ∷ wk ρ A ^ r
    ~-wk  : ∀ {k l A r ρ Γ Δ}
          → ρ ∷ Δ ⊆ Γ
          → ⊢ Δ
          → Γ ⊢ k ~ l ∷ A ^ r
          → Δ ⊢ wk ρ k ~ wk ρ l ∷ wk ρ A ^ r

    -- Weak head expansion
    ≅-red : ∀ {A A′ B B′ r Γ}
          → Γ ⊢ A ⇒* A′ ^ r
          → Γ ⊢ B ⇒* B′ ^ r
          → Whnf A′
          → Whnf B′
          → Γ ⊢ A′ ≅ B′ ^ r
          → Γ ⊢ A  ≅ B ^ r

    ≅ₜ-red : ∀ {a a′ b b′ A B l Γ}
           → Γ ⊢ A ⇒* B ^ [ ! , l ]
           → Γ ⊢ a ⇒* a′ ∷ B ^ l
           → Γ ⊢ b ⇒* b′ ∷ B ^ l
           → Whnf B
           → Whnf a′
           → Whnf b′
           → Γ ⊢ a′ ≅ b′ ∷ B ^ [ ! , l ]
           → Γ ⊢ a  ≅ b  ∷ A ^ [ ! , l ]

    -- Large universe type reflexivity
    ≅-U¹refl   : ∀ {r Γ} → ⊢ Γ → Γ ⊢ (Univ r ¹) ≅ (Univ r ¹) ^ [ ! , ∞ ]

    -- Small universe type reflexivity
    ≅-U⁰refl   : ∀ {r Γ} → ⊢ Γ → Γ ⊢ (Univ r ⁰) ≅ (Univ r ⁰) ∷ U ¹ ^ [ ! , ∞ ]

    -- Natural number type reflexivity
    ≅ₜ-ℕrefl  : ∀ {Γ} → ⊢ Γ → Γ ⊢ ℕ ≅ ℕ ∷ U ⁰ ^ [ ! , next ⁰ ]

    -- Empty type reflexivity
    ≅ₜ-Emptyrefl  : ∀ {Γ l} → ⊢ Γ → Γ ⊢ Empty l ≅ Empty l ∷ SProp l ^ [ ! , next l ]

    -- Π-congruence
    ≅ₜ-Π-cong : ∀ {F G H E rF lF r lG l Γ}
              → lF ≤ l
              → lG ≤ l
              → Γ ⊢ F ^ [ rF , ι lF ]
              → Γ ⊢ F ≅ H ∷ (Univ rF lF) ^ [ ! , next lF ]
              → Γ ∙ F ^ [ rF , ι lF ] ⊢ G ≅ E ∷ (Univ r lG) ^ [ ! , next lG ]
              → Γ ⊢ Π F ^ rF ° lF ▹ G ° lG ° l ≅ Π H ^ rF ° lF ▹ E ° lG ° l ∷ (Univ r l) ^ [ ! , next l ]

    -- ∃-congruence
    -- Since ∃ types are always small, no need for a type-level rule
    ≅ₜ-∃-cong : ∀ {F G H E l Γ}
              → Γ ⊢ F ^ [ % , ι l ]
              → Γ ⊢ F ≅ H ∷ SProp l ^ [ ! , next l ]
              → Γ ∙ F ^ [ % , ι l ] ⊢ G ≅ E ∷ SProp l ^ [ ! , next l ]
              → Γ ⊢ ∃ F ▹ G ≅ ∃ H ▹ E ∷ SProp l ^ [ ! , next l ]

    -- Zero reflexivity
    ≅ₜ-zerorefl : ∀ {Γ} → ⊢ Γ → Γ ⊢ zero ≅ zero ∷ ℕ ^ [ ! , ι ⁰ ]

    -- Successor congruence
    ≅-suc-cong : ∀ {m n Γ} → Γ ⊢ m ≅ n ∷ ℕ ^ [ ! , ι ⁰ ] → Γ ⊢ suc m ≅ suc n ∷ ℕ ^ [ ! , ι ⁰ ]

    -- η-equality
    ≅-η-eq : ∀ {f g F G rF lF lG l Γ}
              → lF ≤ l
              → lG ≤ l
              → Γ ⊢ F ^ [ rF , ι lF ]
              → Γ ⊢ f ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
              → Γ ⊢ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
              → Function f
              → Function g
              → Γ ∙ F ^ [ rF , ι lF ] ⊢ wk1 f ∘ var 0 ^ l ≅ wk1 g ∘ var 0 ^ l ∷ G ^ [ ! , ι lG ]
              → Γ ⊢ f ≅ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]

    -- Variable reflexivity
    ~-var : ∀ {x A Γ r} → Γ ⊢ var x ∷ A ^ r → Γ ⊢ var x ~ var x ∷ A ^ r

    -- Application congurence
    ~-app : ∀ {a b f g F G rF lF lG l Γ}
          → Γ ⊢ f ~ g ∷ Π F ^ rF ° lF ▹ G ° lG ° l ^ [ ! , ι l ]
          → Γ ⊢ a ≅ b ∷ F ^ [ rF , ι lF ]
          → Γ ⊢ f ∘ a ^ l ~ g ∘ b ^ l ∷ G [ a ] ^ [ ! , ι lG ]

    -- Natural recursion congurence
    ~-natrec : ∀ {z z′ s s′ n n′ F F′ l Γ}
             → Γ ∙ ℕ ^ [ ! , ι ⁰ ] ⊢ F ≅ F′ ^ [ ! , ι l ]
             → Γ     ⊢ z ≅ z′ ∷ F [ zero ] ^ [ ! , ι l ]
             → Γ     ⊢ s ≅ s′ ∷ Π ℕ ^ ! ° ⁰ ▹ (F ^ ! ° l ▹▹ F [ suc (var 0) ]↑ ° l ° l ) ° l ° l ^ [ ! , ι l ]
             → Γ     ⊢ n ~ n′ ∷ ℕ ^ [ ! , ι ⁰ ]
             → Γ     ⊢ natrec l F z s n ~ natrec l F′ z′ s′ n′ ∷ F [ n ] ^ [ ! , ι l ]

    -- Empty recursion congurence
    ~-Emptyrec : ∀ {e e′ F F′ l lEmpty Γ}
             → Γ ⊢ F ≅ F′ ^ [ ! , ι l ]
             → Γ ⊢ e ∷ Empty lEmpty ^ [ % , ι lEmpty ]
             → Γ ⊢ e′ ∷ Empty lEmpty ^ [ % , ι lEmpty ]
             → Γ     ⊢ Emptyrec l lEmpty F e ~ Emptyrec l lEmpty F′ e′ ∷ F ^ [ ! , ι l ]

    -- Id congruences
    ~-Id  : ∀ {A A' l t t' u u' Γ}
          → Γ ⊢ A ~ A' ∷ Univ ! l ^ [ ! , next l ]
          → Γ ⊢ t ≅ t' ∷ A ^ [ ! , ι l ]
          → Γ ⊢ u ≅ u' ∷ A ^ [ ! , ι l ]
          → Γ ⊢ Id A t u ~ Id A' t' u' ∷ SProp l ^ [ ! , next l ]

    ~-Idℕ : ∀ {t t' u u' Γ}
          → ⊢ Γ
          → Γ ⊢ t ~ t' ∷ ℕ ^ [ ! , ι ⁰ ]
          → Γ ⊢ u ≅ u' ∷ ℕ ^ [ ! , ι ⁰ ]
          → Γ ⊢ Id ℕ t u ~ Id ℕ t' u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]

    ~-Idℕ0 : ∀ {u u' Γ}
           → ⊢ Γ
           → Γ ⊢ u ~ u' ∷ ℕ ^ [ ! , ι ⁰ ]
           → Γ ⊢ Id ℕ zero u ~ Id ℕ zero u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]

    ~-IdℕS : ∀ {t t' u u' Γ}
           → ⊢ Γ
           → Γ ⊢ t ≅ t' ∷ ℕ ^ [ ! , ι ⁰ ]
           → Γ ⊢ u ~ u' ∷ ℕ ^ [ ! , ι ⁰ ]
           → Γ ⊢ Id ℕ (suc t) u ~ Id ℕ (suc t') u' ∷ SProp ⁰ ^ [ ! , next ⁰ ]

    ~-IdU : ∀ {t t' u u' Γ} →
          let l = ⁰ in
          let l' = ¹ in
            ⊢ Γ
          → Γ ⊢ t ~ t' ∷ U l ^ [ ! , next l ]
          → Γ ⊢ u ≅ u' ∷ U l ^ [ ! , next l ]
          → Γ ⊢ Id (U l) t u ~ Id (U l) t' u' ∷ SProp l' ^ [ ! , next l' ]

    ~-IdUℕ : ∀ {u u' Γ}
           → ⊢ Γ
           → Γ ⊢ u ~ u' ∷ U ⁰ ^ [ ! , next ⁰ ]
           → Γ ⊢ Id (U ⁰) ℕ u ~ Id (U ⁰) ℕ u' ∷ SProp ¹ ^ [ ! , next ¹ ]

    ~-IdUΠ : ∀ {A rA B A' B' u u' Γ} →
          let l = ⁰ in
          let l' = ¹ in
           Γ ⊢ Π A ^ rA ° ⁰ ▹ B ° ⁰ ° ⁰ ≅ Π A' ^ rA ° ⁰ ▹ B' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
           → Γ ⊢ u ~ u' ∷ U l ^ [ ! , next l ]
           → Γ ⊢ Id (U l)  (Π A ^ rA ° l ▹ B ° l ° ⁰ ) u ~ Id (U l) (Π A' ^ rA ° l ▹ B' ° l ° ⁰) u' ∷ SProp l' ^ [ ! , next l' ]

    -- cast congruences

    ~-cast : ∀ {A A' B B' e e' t t' Γ} →
           let l = ⁰ in
             Γ ⊢ A ~ A' ∷ U l ^ [ ! , next l ]
           → Γ ⊢ B ≅ B' ∷ U l ^ [ ! , next l ]
           → Γ ⊢ t ≅ t' ∷ A ^ [ ! , ι l ]
           → Γ ⊢ e ∷ (Id (U ⁰) A B) ^ [ % , next ⁰ ]
           → Γ ⊢ e' ∷ (Id (U ⁰) A' B') ^ [ % , next ⁰ ]
           → Γ ⊢ cast l A B e t ~ cast l A' B' e' t' ∷ B ^ [ ! , ι l ]

    ~-castℕ : ∀ {B B' e e' t t' Γ}
            → ⊢ Γ
            → Γ ⊢ B ~ B' ∷ U ⁰ ^ [ ! , next ⁰ ]
            → Γ ⊢ t ≅ t' ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ e ∷ (Id (U ⁰) ℕ B) ^ [ % , next ⁰ ]
            → Γ ⊢ e' ∷ (Id (U ⁰) ℕ B') ^ [ % , next ⁰ ]
            → Γ ⊢ cast ⁰ ℕ B e t ~ cast ⁰ ℕ B' e' t' ∷ B ^ [ ! , ι ⁰ ]

    ~-castℕℕ : ∀ {e e' t t' Γ}
             → ⊢ Γ
             → Γ ⊢ t ~ t' ∷ ℕ ^ [ ! , ι ⁰ ]
            → Γ ⊢ e ∷ (Id (U ⁰) ℕ ℕ) ^ [ % , next ⁰ ]
            → Γ ⊢ e' ∷ (Id (U ⁰) ℕ ℕ) ^ [ % , next ⁰ ]
             → Γ ⊢ cast ⁰ ℕ ℕ e t ~ cast ⁰ ℕ ℕ e' t' ∷ ℕ ^ [ ! , ι ⁰ ]

    ~-castΠ : ∀ {A A' rA P P' B B' e e' t t' Γ} →
           let l = ⁰ in
           Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ≅ Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
           → Γ ⊢ B ~ B' ∷ U l ^ [ ! , next l ]
           → Γ ⊢ t ≅ t' ∷ Π A ^ rA ° l ▹ P ° l ° l ^ [ ! , ι l ]
           → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ rA ° l ▹ P ° l ° l) B) ^ [ % , next ⁰ ]
           → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ rA ° l ▹ P' ° l ° l) B') ^ [ % , next ⁰ ]
           → Γ ⊢ cast l (Π A ^ rA ° l ▹ P ° l ° l) B e t ~ cast l (Π A' ^ rA ° l ▹ P' ° l ° l) B' e' t' ∷ B ^ [ ! , ι l ]

    ~-castℕΠ : ∀ {A A' rA P P' e e' t t' Γ}
             → Γ ⊢ A ∷ Univ rA ⁰ ^ [ ! , next ⁰ ]
             → Γ ∙ A ^ [ rA , ι ⁰ ] ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ≅ Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ t ≅ t' ∷ ℕ ^ [ ! , ι ⁰ ]
             → Γ ⊢ e ∷ (Id (U ⁰) ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ e' ∷ (Id (U ⁰) ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ cast ⁰ ℕ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) e t ~ cast ⁰ ℕ (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) e' t' ∷ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ^ [ ! , ι ⁰ ]

    ~-castΠℕ : ∀ {A A' rA P P' e e' t t' Γ} →
             let l = ⁰ in
               Γ ⊢ A ∷ Univ rA l ^ [ ! , next l ]
             → Γ ∙ A ^ [ rA , ι l ] ⊢ P ∷ U l ^ [ ! , next l ]
             → Γ ⊢ Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰ ≅ Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ t ≅ t' ∷ (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ^ [ ! , ι l ]
             → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ rA ° l ▹ P ° l ° ⁰) ℕ) ^ [ % , next ⁰ ]
             → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ rA ° l ▹ P' ° l  ° ⁰) ℕ) ^ [ % , next ⁰ ]
             → Γ ⊢ cast l (Π A ^ rA ° ⁰ ▹ P ° ⁰ ° ⁰) ℕ e t ~ cast l (Π A' ^ rA ° ⁰ ▹ P' ° ⁰ ° ⁰) ℕ e' t' ∷ ℕ ^ [ ! , ι ⁰ ]

    ~-castΠΠ%! : ∀ {A A' P P' B B' Q Q' e e' t t' Γ}
             → Γ ⊢ A ∷ Univ % ⁰ ^ [ ! , next ⁰ ]
             → Γ ∙ A ^ [ % , ι ⁰ ] ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ Π A ^ % ° ⁰ ▹ P ° ⁰  ° ⁰ ≅ Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ B ∷ Univ ! ⁰ ^ [ ! , next ⁰ ]
             → Γ ∙ B ^ [ ! , ι ⁰ ] ⊢ Q ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ ≅ Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ t ≅ t' ∷ Π A ^ % ° ⁰ ▹ P ° ⁰  ° ⁰ ^ [ ! , ι ⁰ ]
             → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ cast ⁰ (Π A ^ % ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~ cast ⁰ (Π A' ^ % ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ ! ° ⁰ ▹ Q' ° ⁰ ° ⁰) e' t' ∷ Π B ^ ! ° ⁰ ▹ Q ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]

    ~-castΠΠ!% : ∀ {A A' P P' B B' Q Q' e e' t t' Γ}
             → Γ ⊢ A ∷ Univ ! ⁰ ^ [ ! , next ⁰ ]
             → Γ ∙ A ^ [ ! , ι ⁰ ] ⊢ P ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ ≅ Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ B ∷ Univ % ⁰ ^ [ ! , next ⁰ ]
             → Γ ∙ B ^ [ % , ι ⁰ ] ⊢ Q ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰ ≅ Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰ ∷ U ⁰ ^ [ ! , next ⁰ ]
             → Γ ⊢ t ≅ t' ∷ Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰ ^ [ ! , ι ⁰ ]
             → Γ ⊢ e ∷ (Id (U ⁰) (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ e' ∷ (Id (U ⁰) (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰)) ^ [ % , next ⁰ ]
             → Γ ⊢ cast ⁰ (Π A ^ ! ° ⁰ ▹ P ° ⁰ ° ⁰) (Π B ^ % ° ⁰ ▹ Q ° ⁰ ° ⁰) e t ~ cast ⁰ (Π A' ^ ! ° ⁰ ▹ P' ° ⁰ ° ⁰) (Π B' ^ % ° ⁰ ▹ Q' ° ⁰ ° ⁰) e' t' ∷ Π B ^ % ° ⁰ ▹ Q ° ⁰  ° ⁰ ^ [ ! , ι ⁰ ]

    ~-irrelevance : ∀ {n n′ A l Γ} → Γ ⊢ n ∷ A ^ [ % , l ] → Γ ⊢ n′ ∷ A ^ [ % , l ]
                  → Γ ⊢ n ~ n′ ∷ A ^ [ % , l ]

  -- Composition of universe and generic equality compatibility
  ~-to-≅ : ∀ {t u r l Γ} → Γ ⊢ t ~ u ∷ (Univ r l) ^ [ ! , next l ] → Γ ⊢ t ≅ u ^ [ r , ι l ]
  ~-to-≅ t~u = ≅-univ (~-to-≅ₜ t~u)

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


text:
{-# OPTIONS --without-K #-}
open import container.core

module container.m.coalgebra {li la lb}
  (c : Container li la lb) where

open import level
open import sum
open import function as F hiding (_∘_ ; module _≅_ ; _≅_ ; iso ; ≅⇒≡)
open import equality
open import hott
------------------------------------------------------------------------------
open Container c

-- Definition 3 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
Coalg : ∀ ℓ → Set _
Coalg ℓ = Σ (I → Set ℓ) λ X → X →ⁱ F X

carrier : ∀ {ℓ} → Coalg ℓ → I → Set ℓ
carrier (X , _) = X

IsMor : ∀ {ℓ₁ ℓ₂}(𝓧 : Coalg ℓ₁)(𝓨 : Coalg ℓ₂)
      → (carrier 𝓧 →ⁱ carrier 𝓨) → Set _
IsMor (X , θ) (Y , ψ) f = ψ ∘ⁱ f ≡ imap f ∘ⁱ θ

_⇒_ : ∀ {ℓ₁ ℓ₂} → Coalg ℓ₁ → Coalg ℓ₂ → Set _
𝓧 ⇒ 𝓨 = Σ (carrier 𝓧 →ⁱ carrier 𝓨) (IsMor 𝓧 𝓨)

idf : ∀ {ℓ} → (𝓧 : Coalg ℓ) → 𝓧 ⇒ 𝓧
idf 𝓧 = (λ i x → x) , refl

_∘_ : ∀ {ℓ} → ⦃ 𝓧 𝓨 𝓩 : Coalg ℓ ⦄ → 𝓨 ⇒ 𝓩 → 𝓧 ⇒ 𝓨 → 𝓧 ⇒ 𝓩
(g , coh₁) ∘ (f , coh₂) = g ∘ⁱ f , funextⁱ (λ i x → funext-invⁱ coh₁ i (f i x)
                                   · ap (imap g i) (funext-invⁱ coh₂ i x))

private
  subst-coerce : ∀ {a b} {A : Set a} {B : A → Set b}
                 {x y : A} (p : x ≡ y) {u : B x}
    → subst B p u ≡ coerce (ap B p) u
  subst-coerce refl = refl

  app= : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → f ≡ g
    →(x : A) → f x ≡ g x
  app= p x = ap (λ u → u x) p

  app=-β : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x}
           (p : ∀ x → f x ≡ g x) (x : A)
    → app= (funext p) x ≡ p x
  app=-β {B = B} p x = helper (funext p) x
                         · app= (F._≅_.iso₁ strong-funext-iso p) x
    where helper : ∀ {f g : ∀ x → B x} (p : f ≡ g) x → app= p x ≡ funext-inv p x
          helper refl x = refl

  abstract
    ua : ∀ {i}{X Y : Set i} → X F.≅ Y → X ≡ Y
    ua = F.≅⇒≡

    coerce-β : ∀ {a} {X Y : Set a} → (e : X F.≅ Y)
      → ∀ x → coerce (ua e) x ≡ apply e x
    coerce-β e x = app= (uni-coherence (≅⇒≈ e)) x

  substⁱ-lemma : ∀ {ℓ} {X Y : I → Set ℓ} {f : X →ⁱ F X} {g : Y →ⁱ F Y}
                → (p : X ≡ Y)
                → (∀ i x → subst (λ Z → F Z i) p (f i x)
                              ≡ g i (subst (λ Z → Z i) p x))
    → subst (λ Z → Z →ⁱ F Z) p f ≡ g
  substⁱ-lemma refl = funextⁱ

  imap-subst : ∀ {ℓ} {X Y : I → Set ℓ} (p : X ≡ Y)
    → imap (λ i → subst (λ Z → Z i) p) ≡ (λ i → subst (λ Z → F Z i) p)
  imap-subst refl = refl

record _≅_ {ℓ} (𝓧 𝓨 : Coalg ℓ) : Set (lsuc $ ℓ ⊔ li ⊔ la ⊔ lb) where
  constructor iso
  field
    f : 𝓧 ⇒ 𝓨
    g : 𝓨 ⇒ 𝓧
    f-g : f ∘ g ≡ idf 𝓨
    g-f : g ∘ f ≡ idf 𝓧

≅⇒≡ : ∀ {ℓ} {𝓧 𝓨 : Coalg ℓ} → 𝓧 ≅ 𝓨 → 𝓧 ≡ 𝓨
≅⇒≡ {𝓧 = X , θ} {𝓨 = Y , ψ} 𝓧≅𝓨 = unapΣ (π₁≡ , π₂≡)
  where open _≅_ 𝓧≅𝓨
        X≅Y : ∀ i → X i F.≅ Y i
        X≅Y i = F.iso (proj₁ f i) (proj₁ g i)
                      (funext-invⁱ (ap proj₁ g-f) i)
                      (funext-invⁱ (ap proj₁ f-g) i)
        π₁≡ : X ≡ Y
        π₁≡ = funext λ i → ua (X≅Y i)
        π₂≡ : subst (λ Z → Z →ⁱ F Z) π₁≡ θ ≡ ψ
        π₂≡ = substⁱ-lemma π₁≡ λ i x →
                app= (lemma₂ i) _
              · sym (funext-invⁱ (proj₂ f) i x)
              · ap (ψ i) (sym (lemma₁ i x))
          where lemma₁ : ∀ i x → subst (λ Z → Z i) π₁≡ x ≡ proj₁ f i x
                lemma₁ i x = subst-coerce π₁≡
                           · ap (λ u → coerce u x) (app=-β _ i)
                           · coerce-β (X≅Y i) _
                lemma₂ : ∀ i → subst (λ Z → F Z i) π₁≡ ≡ imap (proj₁ f) i
                lemma₂ i = sym $ funext (hmap (λ i x → sym (lemma₁ i x)) i)
                                   · app= (imap-subst π₁≡) i

IsFinal : ∀ {ℓ} → Coalg ℓ → Set _
IsFinal {ℓ} 𝓧 = ∀ (𝓨 : Coalg ℓ) → contr (𝓨 ⇒ 𝓧)

Final : ∀ ℓ → Set _
Final ℓ = Σ (Coalg ℓ) IsFinal

prop-IsFinal : ∀ {ℓ} (𝓧 : Coalg ℓ) → prop (IsFinal 𝓧)
prop-IsFinal 𝓧 = h1⇒prop (Π-level (λ 𝓨 → contr-h1 _))

-- Lemma 5 in Ahrens, Capriotti and Spadotti (arXiv:1504.02949v1 [cs.LO])
Final-prop : ∀ {ℓ} → prop (Final ℓ)
Final-prop (𝓧 , IsFinal-𝓧) (𝓨 , IsFinal-𝓨) =
    unapΣ (𝓧≡𝓨 , prop-IsFinal 𝓨 _ _)
  where 𝓧≡𝓨 : 𝓧 ≡ 𝓨
        𝓧≡𝓨 = ≅⇒≡ $ iso (proj₁ (IsFinal-𝓨 𝓧)) (proj₁ (IsFinal-𝓧 𝓨))
                        (contr⇒prop (IsFinal-𝓨 𝓨) _ _)
                        (contr⇒prop (IsFinal-𝓧 𝓧) _ _)

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


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

-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/DepRep/DepRep.pdf

module Experiment.Outrageous.#01 where

open import Data.Unit using (⊤)
open import Data.Product using (_×_) renaming (_,_ to _,,_)
open import Data.Nat using (ℕ)

infixl 30 _,_
infixr 40 _:→_

-- Star
data St : Set where
  :ℕ : St
  _:→_ : St → St → St

data Cx : Set where
  ε   : Cx
  _,_ : Cx → St → Cx

data _∈_ : St → Cx → Set where
  top : ∀ {Γ τ} → τ ∈ Γ , τ
  pop : ∀ {Γ σ τ} → τ ∈ Γ → τ ∈ Γ , σ

data _⊢_ : Cx → St → Set where
  var : ∀ {Γ τ} → τ ∈ Γ → Γ ⊢ τ
  lam : ∀ {Γ σ τ} → Γ , σ ⊢ τ → Γ ⊢ σ :→ τ
  app : ∀ {Γ σ τ} → Γ ⊢ σ :→ τ → Γ ⊢ σ → Γ ⊢ τ

⟦_⟧St : St → Set
⟦ :ℕ ⟧St     = ℕ
⟦ σ :→ τ ⟧St = ⟦ σ ⟧St → ⟦ τ ⟧St

⟦_⟧Cx : Cx → Set
⟦ ε ⟧Cx     = ⊤
⟦ Γ , σ ⟧Cx = ⟦ Γ ⟧Cx × ⟦ σ ⟧St

⟦_⟧∈ : ∀ {Γ τ} → τ ∈ Γ → ⟦ Γ ⟧Cx → ⟦ τ ⟧St
⟦ top ⟧∈   (γ ,, t) = t
⟦ pop i ⟧∈ (γ ,, s) = ⟦ i ⟧∈ γ

⟦_⟧⊢ : ∀ {Γ τ} → Γ ⊢ τ → ⟦ Γ ⟧Cx → ⟦ τ ⟧St
⟦ var i ⟧⊢   γ = ⟦ i ⟧∈ γ
⟦ lam t ⟧⊢   γ = λ s → ⟦ t ⟧⊢ (γ ,, s)
⟦ app f a ⟧⊢ γ = ⟦ f ⟧⊢ γ (⟦ a ⟧⊢ γ)