text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Properties where

{-
This module contains:
1. direct proofs of connectedness of Kn and ΩKn
2. Induction principles for cohomology groups of pointed types
3. Equivalence between cohomology of A and reduced cohomology of (A + 1)
4. Equivalence between cohomology and reduced cohomology for dimension ≥ 1
5. Encode-decode proof of Kₙ ≃ ΩKₙ₊₁ and proofs that this equivalence
   and its inverse are morphisms
6. A proof of coHomGr ≅ coHomGrΩ
7. A locked (non-reducing) version of Kₙ ≃ ΩKₙ₊₁
-}

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure

open import Cubical.HITs.S1 hiding (encode ; decode)
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws renaming (assoc to assoc∙)
open import Cubical.Foundations.Univalence
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2 ; setTruncIsSet to §)
open import Cubical.Data.Int renaming (_+_ to _ℤ+_) hiding (-_)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; map2 to trMap2; rec to trRec ; elim3 to trElim3)
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.Algebra.Group hiding (Unit ; Int)
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Data.Sum.Base hiding (map)
open import Cubical.Functions.Morphism
open import Cubical.Data.Sigma

open Iso renaming (inv to inv')

private
  variable
    ℓ ℓ' : Level

------------------- Connectedness ---------------------
is2ConnectedKn : (n : ℕ) → isConnected 2 (coHomK (suc n))
is2ConnectedKn zero = ∣ ∣ base ∣ ∣
                    , trElim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
                        (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelSuc 2 (isOfHLevelTrunc 2)) _ _)
                          (toPropElim (λ _ → isOfHLevelTrunc 2 _ _) refl))
is2ConnectedKn (suc n) = ∣ ∣ north ∣ ∣
                       , trElim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
                           (trElim (λ _ → isProp→isOfHLevelSuc (3 + n) (isOfHLevelTrunc 2 _ _))
                             (suspToPropElim (ptSn (suc n)) (λ _ → isOfHLevelTrunc 2 _ _) refl))

isConnectedKn : (n : ℕ) → isConnected (2 + n) (coHomK (suc n))
isConnectedKn n = isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (2 + n) 1)) (sphereConnected (suc n))

-- direct proof of connectedness of ΩKₙ₊₁ not relying on the equivalence ∥ a ≡ b ∥ₙ ≃ (∣ a ∣ₙ₊₁ ≡ ∣ b ∣ₙ₊₁)
isConnectedPathKn : (n : ℕ) (x y : (coHomK (suc n))) → isConnected (suc n) (x ≡ y)
isConnectedPathKn n =
  trElim (λ _ → isProp→isOfHLevelSuc (2 + n) (isPropΠ λ _ → isPropIsContr))
    (sphereElim _ (λ _ → isProp→isOfHLevelSuc n (isPropΠ λ _ → isPropIsContr))
      λ y → isContrRetractOfConstFun
               {B = (hLevelTrunc (suc n) (ptSn (suc n) ≡ ptSn (suc n)))} ∣ refl ∣
                 (fun⁻ n y
                , trElim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
                         (J (λ y p → fun⁻ n y _ ≡ _) (funExt⁻ (fun⁻Id n) ∣ refl ∣))))
  where
  fun⁻ : (n : ℕ) → (y : coHomK (suc n)) →
         hLevelTrunc (suc n) (ptSn (suc n) ≡ ptSn (suc n))
      → hLevelTrunc (suc n) (∣ ptSn (suc n) ∣ ≡ y)
  fun⁻ n =
    trElim (λ _ → isOfHLevelΠ (3 + n) λ _ → isOfHLevelSuc (2 + n) (isOfHLevelSuc (suc n) (isOfHLevelTrunc (suc n))))
      (sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelTrunc (suc n)) λ _ → ∣ refl ∣)

  fun⁻Id : (n : ℕ) → fun⁻ n ∣ ptSn (suc n) ∣ ≡ λ _ → ∣ refl ∣
  fun⁻Id zero = refl
  fun⁻Id (suc n) = refl

-------------------
-- Induction principles for cohomology groups (n ≥ 1)
-- If we want to show a proposition about some x : Hⁿ(A), it suffices to show it under the
-- assumption that x = ∣ f ∣₂ for some f : A → Kₙ and that f is pointed

coHomPointedElim : {A : Type ℓ} (n : ℕ) (a : A) {B : coHom (suc n) A → Type ℓ'}
                 → ((x : coHom (suc n) A) → isProp (B x))
                 → ((f : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → B ∣ f ∣₂)
                 → (x : coHom (suc n) A) → B x
coHomPointedElim {ℓ' = ℓ'} {A = A} n a isprop indp =
  sElim (λ _ → isOfHLevelSuc 1 (isprop _))
         λ f → helper n isprop indp f (f a) refl
  where
  helper :  (n : ℕ) {B : coHom (suc n) A → Type ℓ'}
         → ((x : coHom (suc n) A) → isProp (B x))
         → ((f : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → B ∣ f ∣₂)
         → (f : A → coHomK (suc n))
         → (x : coHomK (suc n))
         → f a ≡ x → B ∣ f ∣₂
  -- pattern matching a bit extra to avoid isOfHLevelPlus'
  helper zero isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 2 (isPropΠ λ _ → isprop _))
           (toPropElim (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc zero) isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 3 (isPropΠ λ _ → isprop _))
           (suspToPropElim base (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc (suc zero)) isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 4 (isPropΠ λ _ → isprop _))
           (suspToPropElim north (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc (suc (suc n))) isprop ind f =
    trElim (λ _ → isOfHLevelPlus' {n = 5 + n} 1 (isPropΠ λ _ → isprop _))
           (suspToPropElim north (λ _ → isPropΠ λ _ → isprop _) (ind f))

coHomPointedElim2 : {A : Type ℓ} (n : ℕ) (a : A) {B : coHom (suc n) A → coHom (suc n) A → Type ℓ'}
                 → ((x y : coHom (suc n) A) → isProp (B x y))
                 → ((f g : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → g a ≡ coHom-pt (suc n) → B ∣ f ∣₂ ∣ g ∣₂)
                 → (x y : coHom (suc n) A) → B x y
coHomPointedElim2 {ℓ' = ℓ'} {A = A} n a isprop indp = sElim2 (λ _ _ → isOfHLevelSuc 1 (isprop _ _))
                                                   λ f g → helper n a isprop indp f g (f a) (g a) refl refl
  where
  helper : (n : ℕ) (a : A) {B : coHom (suc n) A → coHom (suc n) A → Type ℓ'}
                 → ((x y : coHom (suc n) A) → isProp (B x y))
                 → ((f g : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → g a ≡ coHom-pt (suc n) → B ∣ f ∣₂ ∣ g ∣₂)
                 → (f g : A → coHomK (suc n))
                 → (x y : coHomK (suc n))
                 → f a ≡ x → g a ≡ y
                 → B ∣ f ∣₂ ∣ g ∣₂
  helper zero a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 2 (isPropΠ2 λ _ _ → isprop _ _))
          (toPropElim2 (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc zero) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 3 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 base (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc (suc zero)) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 4 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 north (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc (suc (suc n))) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus' {n = 5 + n} 1 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 north (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))

coHomK-elim : ∀ {ℓ} (n : ℕ) {B : coHomK (suc n) → Type ℓ}
           → ((x : _) → isOfHLevel (suc n) (B x))
           → B (0ₖ (suc n))
           → (x : _) → B x
coHomK-elim n {B = B } hlev b =
  trElim (λ _ → isOfHLevelPlus {n = (suc n)} 2 (hlev _))
    (sphereElim _ (hlev ∘ ∣_∣) b)

{- Equivalence between cohomology of A and reduced cohomology of (A + 1) -}
coHomRed+1Equiv : (n : ℕ) →
                  (A : Type ℓ) →
                  (coHom n A) ≡ (coHomRed n ((A ⊎ Unit , inr (tt))))
coHomRed+1Equiv zero A i = ∥ helpLemma {C = (Int , pos 0)} i ∥₂
  module coHomRed+1 where
  helpLemma : {C : Pointed ℓ} → ( (A → (typ C)) ≡  ((((A ⊎ Unit) , inr (tt)) →∙ C)))
  helpLemma {C = C} = isoToPath (iso map1
                                     map2
                                     (λ b → linvPf b)
                                     (λ _  → refl))
    where
    map1 : (A → typ C) → ((((A ⊎ Unit) , inr (tt)) →∙ C))
    map1 f = map1' , refl
      module helpmap where
      map1' : A ⊎ Unit → fst C
      map1' (inl x) = f x
      map1' (inr x) = pt C

    map2 : ((((A ⊎ Unit) , inr (tt)) →∙ C)) → (A → typ C)
    map2 (g , pf) x = g (inl x)

    linvPf : (b :((((A ⊎ Unit) , inr (tt)) →∙ C))) →  map1 (map2 b) ≡ b
    linvPf (f , snd) i = (λ x → helper x i)  , λ j → snd ((~ i) ∨ j)
      where
      helper : (x : A ⊎ Unit) → ((helpmap.map1') (map2 (f , snd)) x) ≡ f x
      helper (inl x) = refl
      helper (inr tt) = sym snd
coHomRed+1Equiv (suc zero) A i = ∥ coHomRed+1.helpLemma A i {C = (coHomK 1 , ∣ base ∣)} i ∥₂
coHomRed+1Equiv (suc (suc n)) A i = ∥ coHomRed+1.helpLemma A i {C = (coHomK (2 + n) , ∣ north ∣)} i ∥₂

Iso-coHom-coHomRed : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → Iso (coHomRed (suc n) A) (coHom (suc n) (typ A))
fun (Iso-coHom-coHomRed {A = A , a} n) = map fst
inv' (Iso-coHom-coHomRed {A = A , a} n) = map λ f → (λ x → f x -ₖ f a) , rCancelₖ _ _
rightInv (Iso-coHom-coHomRed {A = A , a} n) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
         λ f → trRec (isProp→isOfHLevelSuc _ (§ _ _))
                      (λ p → cong ∣_∣₂ (funExt λ x → cong (λ y → f x +ₖ y) (cong -ₖ_ p ∙ -0ₖ) ∙ rUnitₖ _ (f x)))
                      (Iso.fun (PathIdTruncIso (suc n)) (isContr→isProp (isConnectedKn n) ∣ f a ∣ ∣ 0ₖ _ ∣))
leftInv (Iso-coHom-coHomRed {A = A , a} n) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ {(f , p) → cong ∣_∣₂ (ΣPathP (((funExt λ x → (cong (λ y → f x -ₖ y) p
                                                    ∙∙ cong (λ y → f x +ₖ y) -0ₖ
                                                    ∙∙ rUnitₖ _ (f x)) ∙ refl))
                              , helper n (f a) (sym p)))}
    where
    path : (n : ℕ) (x : coHomK (suc n)) (p : 0ₖ _ ≡ x) → _
    path n x p = (cong (λ y → x -ₖ y) (sym p) ∙∙ cong (λ y → x +ₖ y) -0ₖ ∙∙ rUnitₖ _ x) ∙ refl

    helper :  (n : ℕ) (x : coHomK (suc n)) (p : 0ₖ _ ≡ x)
            → PathP (λ i → path n x p i ≡ 0ₖ _) (rCancelₖ _ x) (sym p)
    helper zero x =
      J (λ x p → PathP (λ i → path 0 x p i ≡ 0ₖ _)
                        (rCancelₖ _ x) (sym p))
        λ i j → rUnit (rUnit (λ _ → 0ₖ 1) (~ j)) (~ j) i
    helper (suc n) x =
      J (λ x p → PathP (λ i → path (suc n) x p i ≡ 0ₖ _) (rCancelₖ _ x) (sym p))
        λ i j → rCancelₖ (suc (suc n)) (0ₖ (suc (suc n))) (~ i ∧ ~ j)

+∙≡+ : (n : ℕ) {A : Pointed ℓ} (x y : coHomRed (suc n) A)
     → Iso.fun (Iso-coHom-coHomRed n) (x +ₕ∙ y)
      ≡ Iso.fun (Iso-coHom-coHomRed n) x +ₕ Iso.fun (Iso-coHom-coHomRed n) y

+∙≡+ zero = sElim2 (λ _ _ → isOfHLevelPath 2 § _ _) λ _ _ → refl
+∙≡+ (suc n) = sElim2 (λ _ _ → isOfHLevelPath 2 § _ _) λ _ _ → refl

private
  homhelp : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) (x y : coHom (suc n) (typ A))
          → Iso.inv (Iso-coHom-coHomRed {A = A} n) (x +ₕ y)
           ≡ Iso.inv (Iso-coHom-coHomRed n) x +ₕ∙ Iso.inv (Iso-coHom-coHomRed n) y
  homhelp n A = morphLemmas.isMorphInv _+ₕ∙_ _+ₕ_
                (Iso.fun (Iso-coHom-coHomRed n)) (+∙≡+ n) _
                (Iso.rightInv (Iso-coHom-coHomRed n)) (Iso.leftInv (Iso-coHom-coHomRed n))

coHomGr≅coHomRedGr : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ)
                  → GroupEquiv (coHomRedGrDir (suc n) A) (coHomGr (suc n) (typ A))
fst (coHomGr≅coHomRedGr n A) = isoToEquiv (Iso-coHom-coHomRed n)
snd (coHomGr≅coHomRedGr n A) = makeIsGroupHom (+∙≡+ n)

coHomRedGroup : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) → AbGroup ℓ
coHomRedGroup zero A = coHomRedGroupDir zero A
coHomRedGroup (suc n) A =
  InducedAbGroup (coHomGroup (suc n) (typ A))
                 _+ₕ∙_
                 (isoToEquiv (invIso (Iso-coHom-coHomRed n)))
                 (homhelp n A)

abstract
  coHomGroup≡coHomRedGroup : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ)
                          → coHomGroup (suc n) (typ A) ≡ coHomRedGroup (suc n) A
  coHomGroup≡coHomRedGroup n A =
    InducedAbGroupPath (coHomGroup (suc n) (typ A))
              _+ₕ∙_
              (isoToEquiv (invIso (Iso-coHom-coHomRed n)))
              (homhelp n A)

------------------- Kₙ ≃ ΩKₙ₊₁ ---------------------
-- This proof uses the encode-decode method rather than Freudenthal

-- We define the map σ : Kₙ → ΩKₙ₊₁ and prove that it is a morphism
private
  module _ (n : ℕ) where
  σ : {n : ℕ} → coHomK (suc n) → Path (coHomK (2 + n)) ∣ north ∣ ∣ north ∣
  σ {n = n} = trRec (isOfHLevelTrunc (4 + n) _ _)
                    λ a → cong ∣_∣ (merid a ∙ sym (merid (ptSn (suc n))))

  σ-hom-helper : ∀ {ℓ} {A : Type ℓ} {a : A} (p : a ≡ a) (r : refl ≡ p)
                   → lUnit p ∙ cong (_∙ p) r ≡ rUnit p ∙ cong (p ∙_) r
  σ-hom-helper p = J (λ p r → lUnit p ∙ cong (_∙ p) r ≡ rUnit p ∙ cong (p ∙_) r) refl

  σ-hom : {n : ℕ} (x y : coHomK (suc n)) → σ (x +ₖ y) ≡ σ x ∙ σ y
  σ-hom {n = zero} =
    elim2 (λ _ _ → isOfHLevelPath 3 (isOfHLevelTrunc 4 _ _) _ _)
          (wedgeconFun _ _
            (λ _ _ → isOfHLevelTrunc 4 _ _ _ _)
            (λ x → lUnit _
                  ∙ cong (_∙ σ ∣ x ∣) (cong (cong ∣_∣) (sym (rCancel (merid base)))))
            (λ y → cong σ (rUnitₖ 1 ∣ y ∣)
                 ∙∙ rUnit _
                 ∙∙ cong (σ ∣ y ∣ ∙_) (cong (cong ∣_∣) (sym (rCancel (merid base)))))
            (sym (σ-hom-helper (σ ∣ base ∣) (cong (cong ∣_∣) (sym (rCancel (merid base)))))))
  σ-hom {n = suc n} =
    elim2 (λ _ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (5 + n) _ _) _ _)
          (wedgeconFun _ _ (λ _ _ → isOfHLevelPath ((2 + n) + (2 + n)) (wedgeConHLev' n) _ _)
           (λ x → lUnit _
                 ∙ cong (_∙ σ ∣ x ∣) (cong (cong ∣_∣) (sym (rCancel (merid north)))))
           (λ y → cong σ (rUnitₖ (2 + n) ∣ y ∣)
                ∙∙ rUnit _
                ∙∙ cong (σ ∣ y ∣ ∙_) (cong (cong ∣_∣) (sym (rCancel (merid north)))))
           (sym (σ-hom-helper (σ ∣ north ∣) (cong (cong ∣_∣) (sym (rCancel (merid north)))))))

  -- We will need to following lemma
  σ-minusDistr : {n : ℕ} (x y : coHomK (suc n)) → σ (x -ₖ y) ≡ σ x ∙ sym (σ y)
  σ-minusDistr {n = n} =
    morphLemmas.distrMinus'
      _+ₖ_ _∙_
      σ σ-hom ∣ (ptSn (suc n)) ∣ refl
      -ₖ_ sym
      (λ x → sym (lUnit x)) (λ x → sym (rUnit x))
      (rUnitₖ (suc n))
      (lCancelₖ (suc n)) rCancel
      (assocₖ (suc n)) assoc∙
       (cong (cong ∣_∣) (rCancel (merid (ptSn (suc n)))))

  -- we define the code using addIso
  Code : (n : ℕ) →  coHomK (2 + n) → Type₀
  Code n x = (trRec {B = TypeOfHLevel ℓ-zero (3 + n)} (isOfHLevelTypeOfHLevel (3 + n))
                     λ a → Code' a , hLevCode' a) x .fst
    where
    Code' : (S₊ (2 + n)) → Type₀
    Code' north = coHomK (suc n)
    Code' south = coHomK (suc n)
    Code' (merid a i) = isoToPath (addIso (suc n) ∣ a ∣) i

    hLevCode' : (x : S₊ (2 + n)) → isOfHLevel (3 + n) (Code' x)
    hLevCode' = suspToPropElim (ptSn (suc n)) (λ _ → isPropIsOfHLevel (3 + n)) (isOfHLevelTrunc (3 + n))

  symMeridLem : (n : ℕ) → (x : S₊ (suc n)) (y : coHomK (suc n))
                        → subst (Code n) (cong ∣_∣ (sym (merid x))) y ≡ y -ₖ ∣ x ∣
  symMeridLem n x = trElim (λ _ → isOfHLevelPath (3 + n) (isOfHLevelTrunc (3 + n)) _ _)
                            (λ y → cong (_-ₖ ∣ x ∣) (transportRefl ∣ y ∣))

  decode : {n : ℕ} (x : coHomK (2 + n)) → Code n x → ∣ north ∣ ≡ x
  decode {n = n} = trElim (λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelPath (4 + n) (isOfHLevelTrunc (4 + n)) _ _)
                          decode-elim
    where
    north≡merid : (a : S₊ (suc n))
                → Path (coHomK (2 + n)) ∣ north ∣ ∣ north ∣
                ≡ (Path (coHomK (2 + n)) ∣ north ∣ ∣ south ∣)
    north≡merid a i = Path (coHomK (2 + n)) ∣ north ∣ ∣ merid a i ∣

    decode-elim : (a : S₊ (2 + n)) → Code n ∣ a ∣ → Path (coHomK (2 + n)) ∣ north ∣ ∣ a ∣
    decode-elim north = σ
    decode-elim south = trRec (isOfHLevelTrunc (4 + n) _ _)
                              λ a → cong ∣_∣ (merid a)
    decode-elim (merid a i) =
      hcomp (λ k → λ { (i = i0) → σ
                      ; (i = i1) → mainPath a k})
            (funTypeTransp (Code n) (λ x → ∣ north ∣ ≡ x) (cong ∣_∣ (merid a)) σ i)
      where
      mainPath : (a : (S₊ (suc n))) →
             transport (north≡merid a) ∘ σ ∘ transport (λ i → Code n ∣ merid a (~ i) ∣)
           ≡ trRec (isOfHLevelTrunc (4 + n) _ _) λ a → cong ∣_∣ (merid a)
      mainPath a = funExt (trElim (λ _ → isOfHLevelPath (3 + n) (isOfHLevelTrunc (4 + n) _ _) _ _)
                                  (λ x → (λ i → transport (north≡merid a) (σ (symMeridLem n a ∣ x ∣ i)))
                                       ∙∙ cong (transport (north≡merid a)) (-distrHelp x)
                                       ∙∙ (substAbove x)))
        where
        -distrHelp : (x : S₊ (suc n)) → σ (∣ x ∣ -ₖ ∣ a ∣) ≡ cong ∣_∣ (merid x) ∙ cong ∣_∣ (sym (merid a))
        -distrHelp x =
             σ-minusDistr ∣ x ∣ ∣ a ∣
           ∙ (λ i → (cong ∣_∣ (compPath-filler (merid x) (λ j → merid (ptSn (suc n)) (~ j ∨ i)) (~ i)))
                   ∙ (cong ∣_∣ (sym (compPath-filler (merid a) (λ j → merid (ptSn (suc n)) (~ j ∨ i)) (~ i)))))

        substAbove : (x : S₊ (suc n)) → transport (north≡merid a) (cong ∣_∣ (merid x) ∙ cong ∣_∣ (sym (merid a)))
                   ≡ cong ∣_∣ (merid x)
        substAbove x i = transp (λ j → north≡merid a (i ∨ j)) i
                                (compPath-filler (cong ∣_∣ (merid x)) (λ j → ∣ merid a (~ j ∨ i) ∣) (~ i))

  encode : {n : ℕ} {x : coHomK (2 + n)} → Path (coHomK (2 + n)) ∣ north ∣ x → Code n x
  encode {n = n} p = transport (cong (Code n) p) ∣ (ptSn (suc n)) ∣

  decode-encode : {n : ℕ} {x : coHomK (2 + n)} (p : Path (coHomK (2 + n)) ∣ north ∣ x)
               → decode _ (encode p) ≡ p
  decode-encode {n = n} =
    J (λ y p → decode _ (encode p) ≡ p)
        (cong (decode ∣ north ∣) (transportRefl ∣ ptSn (suc n) ∣)
       ∙ cong (cong ∣_∣) (rCancel (merid (ptSn (suc n)))))

-- We define an addition operation on Code which we can use in order to show that encode is a
-- morphism (in a very loose sense)
  hLevCode : {n : ℕ} (x : coHomK (2 + n)) → isOfHLevel (3 + n) (Code n x)
  hLevCode {n = n} =
    trElim (λ _ → isProp→isOfHLevelSuc (3 + n) (isPropIsOfHLevel (3 + n)))
      (sphereToPropElim _
        (λ _ → (isPropIsOfHLevel (3 + n))) (isOfHLevelTrunc (3 + n)))

  Code-add' : {n : ℕ} (x : _) → Code n ∣ north ∣ → Code n ∣ x ∣ → Code n ∣ x ∣
  Code-add' {n = n} north = _+ₖ_
  Code-add' {n = n} south = _+ₖ_
  Code-add' {n = n} (merid a i) = helper n a i
    where
    help : (n : ℕ) → (x y a : S₊ (suc n))
        → transport (λ i → Code n ∣ north ∣ → Code n ∣ merid a i ∣ → Code n ∣ merid a i ∣)
                     (_+ₖ_) ∣ x ∣ ∣ y ∣
         ≡ ∣ x ∣ +ₖ ∣ y ∣
    help n x y a =
         (λ i → transportRefl ((∣ transportRefl x i ∣  +ₖ (∣ transportRefl y i ∣ -ₖ ∣ a ∣)) +ₖ ∣ a ∣) i)
      ∙∙ cong (_+ₖ ∣ a ∣) (assocₖ _ ∣ x ∣ ∣ y ∣ (-ₖ ∣ a ∣))
      ∙∙ sym (assocₖ _ (∣ x ∣ +ₖ ∣ y ∣) (-ₖ ∣ a ∣) ∣ a ∣)
      ∙∙ cong ((∣ x ∣ +ₖ ∣ y ∣) +ₖ_) (lCancelₖ _ ∣ a ∣)
      ∙∙ rUnitₖ _ _

    helper : (n : ℕ) (a : S₊ (suc n))
           → PathP (λ i → Code n ∣ north ∣ → Code n ∣ merid a i ∣ → Code n ∣ merid a i ∣) _+ₖ_ _+ₖ_
    helper n a =
      toPathP (funExt
                (trElim (λ _ → isOfHLevelPath (3 + n) (isOfHLevelΠ (3 + n) (λ _ → isOfHLevelTrunc (3 + n))) _ _)
                  λ x → funExt
                           (trElim (λ _ → isOfHLevelPath (3 + n) (isOfHLevelTrunc (3 + n)) _ _)
                                   λ y → help n x y a)))

  Code-add : {n : ℕ} (x : _) → Code n ∣ north ∣ → Code n x → Code n x
  Code-add {n = n} =
    trElim (λ x → isOfHLevelΠ (4 + n) λ _ → isOfHLevelΠ (4 + n) λ _ → isOfHLevelSuc (3 + n) (hLevCode {n = n} x))
           Code-add'

  encode-hom : {n : ℕ} {x : _} (q : 0ₖ _ ≡ 0ₖ _) (p : 0ₖ _ ≡ x)
             → encode (q ∙ p) ≡ Code-add {n = n} x (encode q) (encode p)
  encode-hom {n = n} q = J (λ x p → encode (q ∙ p) ≡ Code-add {n = n} x (encode q) (encode p))
                           (cong encode (sym (rUnit q))
                         ∙∙ sym (rUnitₖ _ (encode q))
                         ∙∙ cong (encode q +ₖ_) (cong ∣_∣ (sym (transportRefl _))))

stabSpheres : (n : ℕ) → Iso (coHomK (suc n)) (typ (Ω (coHomK-ptd (2 + n))))
fun (stabSpheres n) = decode _
inv' (stabSpheres n) = encode
rightInv (stabSpheres n) p = decode-encode p
leftInv (stabSpheres n) =
  trElim (λ _ → isOfHLevelPath (3 + n) (isOfHLevelTrunc (3 + n)) _ _)
    λ a → cong encode (congFunct ∣_∣ (merid a) (sym (merid (ptSn (suc n)))))
        ∙∙ (λ i → transport (congFunct (Code n) (cong ∣_∣ (merid a))
                             (cong ∣_∣ (sym (merid (ptSn (suc n))))) i) ∣ ptSn (suc n) ∣)
        ∙∙ (substComposite (λ x → x)
                           (cong (Code n) (cong ∣_∣ (merid a)))
                           (cong (Code n) (cong ∣_∣ (sym (merid (ptSn (suc n)))))) ∣ ptSn (suc n) ∣
        ∙∙ cong (transport (λ i → Code n ∣ merid (ptSn (suc n)) (~ i) ∣))
                (transportRefl (∣ (ptSn (suc n)) ∣ +ₖ ∣ a ∣) ∙ lUnitₖ (suc n) ∣ a ∣)
        ∙∙ symMeridLem n (ptSn (suc n)) ∣ a ∣
        ∙∙ cong (∣ a ∣ +ₖ_) -0ₖ
        ∙∙ rUnitₖ (suc n) ∣ a ∣)

Iso-Kn-ΩKn+1 : (n : HLevel) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso-Kn-ΩKn+1 zero = invIso (compIso (congIso (truncIdempotentIso _ isGroupoidS¹)) ΩS¹IsoInt)
Iso-Kn-ΩKn+1 (suc n) = stabSpheres n

Kn≃ΩKn+1 : {n : ℕ} → coHomK n ≃ typ (Ω (coHomK-ptd (suc n)))
Kn≃ΩKn+1 {n = n} = isoToEquiv (Iso-Kn-ΩKn+1 n)

-- Some properties of the Iso
Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
Kn→ΩKn+1 n = Iso.fun (Iso-Kn-ΩKn+1 n)

ΩKn+1→Kn : (n : ℕ) → typ (Ω (coHomK-ptd (suc n))) → coHomK n
ΩKn+1→Kn n = Iso.inv (Iso-Kn-ΩKn+1 n)

Kn→ΩKn+10ₖ : (n : ℕ) → Kn→ΩKn+1 n (0ₖ n) ≡ refl
Kn→ΩKn+10ₖ zero = sym (rUnit refl)
Kn→ΩKn+10ₖ (suc n) i j = ∣ (rCancel (merid (ptSn (suc n))) i j) ∣

ΩKn+1→Kn-refl : (n : ℕ) → ΩKn+1→Kn n refl ≡ 0ₖ n
ΩKn+1→Kn-refl zero = refl
ΩKn+1→Kn-refl (suc zero) = refl
ΩKn+1→Kn-refl (suc (suc n)) = refl

Kn→ΩKn+1-hom : (n : ℕ) (x y : coHomK n) → Kn→ΩKn+1 n (x +[ n ]ₖ y) ≡ Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y
Kn→ΩKn+1-hom zero x y = (λ j i → hfill (doubleComp-faces (λ i₁ → ∣ base ∣) (λ _ → ∣ base ∣) i)
                                         (inS (∣ intLoop (x ℤ+ y) i ∣)) (~ j))
                      ∙∙ (λ j i → ∣ intLoop-hom x y (~ j) i ∣)
                      ∙∙ (congFunct ∣_∣ (intLoop x) (intLoop y)
                        ∙ cong₂ _∙_ (λ j i → hfill (doubleComp-faces (λ i₁ → ∣ base ∣) (λ _ → ∣ base ∣) i)
                                                    (inS (∣ intLoop x i ∣)) j)
                                     λ j i → hfill (doubleComp-faces (λ i₁ → ∣ base ∣) (λ _ → ∣ base ∣) i)
                                                    (inS (∣ intLoop y i ∣)) j)
Kn→ΩKn+1-hom (suc n) = σ-hom

ΩKn+1→Kn-hom : (n : ℕ) (x y : Path (coHomK (suc n)) (0ₖ _) (0ₖ _))
             → ΩKn+1→Kn n (x ∙ y) ≡ ΩKn+1→Kn n x +[ n ]ₖ ΩKn+1→Kn n y
ΩKn+1→Kn-hom zero p q =
     cong winding (congFunct (trRec isGroupoidS¹ (λ x → x)) p q)
   ∙ winding-hom (cong (trRec isGroupoidS¹ (λ x → x)) p) (cong (trRec isGroupoidS¹ (λ x → x)) q)
ΩKn+1→Kn-hom (suc n) = encode-hom

isHomogeneousKn : (n : HLevel) → isHomogeneous (coHomK-ptd n)
isHomogeneousKn n =
  subst isHomogeneous
    (sym (ΣPathP (ua Kn≃ΩKn+1 , ua-gluePath _ (Kn→ΩKn+10ₖ n))))
    (isHomogeneousPath _ _)

-- With the equivalence Kn≃ΩKn+1, we get that the two definitions of cohomology groups agree
open IsGroupHom

coHom≅coHomΩ : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → GroupIso (coHomGr n A) (coHomGrΩ n A)
fun (fst (coHom≅coHomΩ n A)) = map λ f a → Kn→ΩKn+1 n (f a)
inv' (fst (coHom≅coHomΩ n A)) = map λ f a → ΩKn+1→Kn n (f a)
rightInv (fst (coHom≅coHomΩ n A)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ f → cong ∣_∣₂ (funExt λ x → rightInv (Iso-Kn-ΩKn+1 n) (f x))
leftInv (fst (coHom≅coHomΩ n A)) =
  sElim (λ _ → isOfHLevelPath 2 § _ _)
        λ f → cong ∣_∣₂ (funExt λ x → leftInv (Iso-Kn-ΩKn+1 n) (f x))
snd (coHom≅coHomΩ n A) =
  makeIsGroupHom
    (sElim2 (λ _ _ → isOfHLevelPath 2 § _ _)
            λ f g → cong ∣_∣₂ (funExt λ x → Kn→ΩKn+1-hom n (f x) (g x)))

module lockedKnIso (key : Unit') where
  Kn→ΩKn+1' : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
  Kn→ΩKn+1' n = lock key (Iso.fun (Iso-Kn-ΩKn+1 n))

  ΩKn+1→Kn' : (n : ℕ) → typ (Ω (coHomK-ptd (suc n))) → coHomK n
  ΩKn+1→Kn' n = lock key (Iso.inv (Iso-Kn-ΩKn+1 n))

  ΩKn+1→Kn→ΩKn+1 : (n : ℕ) → (x : typ (Ω (coHomK-ptd (suc n)))) → Kn→ΩKn+1' n (ΩKn+1→Kn' n x) ≡ x
  ΩKn+1→Kn→ΩKn+1 n x = pm key
    where
    pm : (key : Unit') → lock key (Iso.fun (Iso-Kn-ΩKn+1 n)) (lock key (Iso.inv (Iso-Kn-ΩKn+1 n)) x) ≡ x
    pm unlock = Iso.rightInv (Iso-Kn-ΩKn+1 n) x

  Kn→ΩKn+1→Kn : (n : ℕ) → (x : coHomK n) → ΩKn+1→Kn' n (Kn→ΩKn+1' n x) ≡ x
  Kn→ΩKn+1→Kn n x = pm key
    where
    pm : (key : Unit') → lock key (Iso.inv (Iso-Kn-ΩKn+1 n)) (lock key (Iso.fun (Iso-Kn-ΩKn+1 n)) x) ≡ x
    pm unlock = Iso.leftInv (Iso-Kn-ΩKn+1 n) x

-distrLemma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : ℕ) (f : GroupHom (coHomGr n A) (coHomGr m B))
              (x y : coHom n A)
            → fst f (x -[ n ]ₕ y) ≡ fst f x -[ m ]ₕ fst f y
-distrLemma n m f' x y = sym (-cancelRₕ m (f y) (f (x -[ n ]ₕ y)))
                     ∙∙ cong (λ x → x -[ m ]ₕ f y) (sym (f' .snd .pres· (x -[ n ]ₕ y) y))
                     ∙∙ cong (λ x → x -[ m ]ₕ f y) ( cong f (-+cancelₕ n _ _))
  where
  f = fst f'

max_stars_repo_name: maxdore/cubical

max_issues_repo_name: maxdore/cubical

max_forks_repo_name: maxdore/cubical


text:
module PatternSynonymImports where

open import PatternSynonyms renaming (z to zzz)

pattern myzero = zzz
two = ss zzz

list : List ℕ
list = 1 ∷ []

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --cubical #-}

module Issue2799 where

open import Agda.Primitive.Cubical

postulate
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATHP        PathP     #-}

_≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
_≡_ {A = A} = PathP (λ _ → A)

record Stream (A : Set) : Set where
  coinductive
  constructor _,_
  field
    head : A
    tail : Stream A

open Stream

mapS : ∀ {A B} → (A → B) → Stream A → Stream B
head (mapS f xs) = f (head xs)
tail (mapS f xs) = mapS f (tail xs)

mapS-id : ∀ {A} {xs : Stream A} → mapS (λ x → x) xs ≡ xs
head (mapS-id {xs = xs} i) = head xs
tail (mapS-id {xs = xs} i) = mapS-id {xs = tail xs} i

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
postulate A : Set

record Overlap : Set where
  constructor mk
  field overlap {{a}} : A

record NoOverlap : Set where
  constructor mk
  field {{a}} : A

ok : A → NoOverlap
ok a = mk {{a}}

bad : A → Overlap
bad a = mk {{a}}
-- Function does not accept argument {{a}}
-- when checking that {{a}} is a valid argument to a function of type
-- {{a = a₁ : A}} → Overlap

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Categories.Category

module Categories.Morphism.IsoEquiv {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Function using (flip; _on_)
open import Relation.Binary hiding (_⇒_)
import Relation.Binary.Construct.On as On

open import Categories.Morphism 𝒞

open Category 𝒞

private
  variable
    A B C : Obj

-- Two lemmas to set things up: if they exist, inverses are unique.

to-unique : ∀ {f₁ f₂ : A ⇒ B} {g₁ g₂} →
            Iso f₁ g₁ → Iso f₂ g₂ → f₁ ≈ f₂ → g₁ ≈ g₂
to-unique {_} {_} {f₁} {f₂} {g₁} {g₂} iso₁ iso₂ hyp = begin
                 g₁   ≈˘⟨ identityˡ ⟩
     id        ∘ g₁   ≈˘⟨ ∘-resp-≈ˡ Iso₂.isoˡ ⟩
    (g₂ ∘  f₂) ∘ g₁   ≈˘⟨ ∘-resp-≈ˡ (∘-resp-≈ʳ hyp) ⟩
    (g₂ ∘  f₁) ∘ g₁   ≈⟨ assoc ⟩
     g₂ ∘ (f₁  ∘ g₁)  ≈⟨ ∘-resp-≈ʳ Iso₁.isoʳ ⟩
     g₂ ∘  id         ≈⟨ identityʳ ⟩
     g₂               ∎
  where
    open HomReasoning
    module Iso₁ = Iso iso₁
    module Iso₂ = Iso iso₂

from-unique : ∀ {f₁ f₂ : A ⇒ B} {g₁ g₂} →
              Iso f₁ g₁ → Iso f₂ g₂ → g₁ ≈ g₂ → f₁ ≈ f₂
from-unique iso₁ iso₂ hyp = to-unique iso₁⁻¹ iso₂⁻¹ hyp
  where
    iso₁⁻¹ = record { isoˡ = Iso.isoʳ iso₁  ; isoʳ = Iso.isoˡ iso₁ }
    iso₂⁻¹ = record { isoˡ = Iso.isoʳ iso₂  ; isoʳ = Iso.isoˡ iso₂ }

-- Equality of isomorphisms is just equality of the underlying morphism(s).
--
-- Only one equation needs to be given; the equation in the other
-- direction holds automatically (by the above lemmas).
--
-- The reason for wrapping the underlying equality in a record at all
-- is that this helps unification.  Concretely, it allows Agda to
-- infer the isos |i| and |j| being related in function applications
-- where only the equation |i ≃ j| is passed as an explicit argument.

infix 4 _≃_
record _≃_ (i j : A ≅ B) : Set e where
  constructor ⌞_⌟
  open _≅_
  field from-≈ : from i ≈ from j

  to-≈ : to i ≈ to j
  to-≈ = to-unique (iso i) (iso j) from-≈

open _≃_

≃-isEquivalence : IsEquivalence (_≃_ {A} {B})
≃-isEquivalence = record
  { refl  = ⌞ refl ⌟
  ; sym   = λ where ⌞ eq ⌟          → ⌞ sym eq ⌟
  ; trans = λ where ⌞ eq₁ ⌟ ⌞ eq₂ ⌟ → ⌞ trans eq₁ eq₂ ⌟
  }
  where open Equiv

≃-setoid : ∀ {A B : Obj} → Setoid _ _
≃-setoid {A} {B} = record
  { Carrier       = A ≅ B
  ; _≈_           = _≃_
  ; isEquivalence = ≃-isEquivalence
  }

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

-- An alternative, more direct notion of equality on isomorphisms that
-- involves no wrapping/unwrapping.

infix 4 _≃′_
_≃′_ : Rel (A ≅ B) e
_≃′_ = _≈_ on _≅_.from

≃′-isEquivalence : IsEquivalence (_≃′_ {A} {B})
≃′-isEquivalence = On.isEquivalence _≅_.from equiv

≃′-setoid : ∀ {A B : Obj} → Setoid _ _
≃′-setoid {A} {B} = record
  { Carrier       = A ≅ B
  ; _≈_           = _≃′_
  ; isEquivalence = ≃′-isEquivalence
  }

-- The two notions of equality are equivalent

≃⇒≃′ : ∀ {i j : A ≅ B} → i ≃ j → i ≃′ j
≃⇒≃′ eq = from-≈ eq

≃′⇒≃ : ∀ {i j : A ≅ B} → i ≃′ j → i ≃ j
≃′⇒≃ {_} {_} {i} {j} eq = ⌞ eq ⌟

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Expressions(x : X) where
  import OutsideIn.TypeSchema as TS
  open TS(x)
  open X(x)

  {- SYNTAX -}
  data Name (n : Set) : NameType → Set where
    N : n → Name n Regular
    DC : ∀ {x} → dc x → Name n (Datacon x)

  mutual
    data Alternative (ev tv : Set) : Shape → Set where
      _→′_ : ∀ {n : ℕ}{r : Shape}→ Name ev (Datacon n) → Expression (ev ⨁ n) tv r
           → Alternative ev tv (Unary r)

    infixr 5 _∣_

    data Alternatives (ev tv : Set) : Shape → Set where
      esac : Alternatives ev tv Nullary
      _∣_  : ∀ {r₁ r₂} → Alternative ev tv r₁ → Alternatives ev tv r₂
           → Alternatives ev tv (Binary r₁ r₂)

    data Expression (ev tv : Set) : Shape → Set where
      Var : ∀ {x} → Name ev x → Expression ev tv Nullary
      λ′_ : ∀ {a} → Expression (Ⓢ ev) tv a → Expression ev tv (Unary a)
      _·_ : ∀ {a a′} → Expression ev tv a → Expression ev tv a′ → Expression ev tv (Binary a a′)
      let₁_in′_ : ∀ {a a′} → Expression ev tv a → Expression (Ⓢ ev) tv a′
                → Expression ev tv (Binary a a′)
      let₂_∷_in′_ : ∀ {a a′} → Expression ev tv a → Type tv → Expression (Ⓢ ev) tv a′
                  → Expression ev tv (Binary a a′)
      let₃_·_∷_⇒_in′_ : ∀ {a a′} → (n : ℕ) → Expression ev (tv ⨁ n) a
                                  → QConstraint (tv ⨁ n)
                                  → Type (tv ⨁ n)
                                  → Expression (Ⓢ ev) tv a′
                                  → Expression ev tv (Binary a a′)
      case_of_ : ∀ {r₁ r₂} → Expression ev tv r₁ → Alternatives ev tv r₂
               → Expression ev tv (Binary r₁ r₂)

  private
    module PlusN-f n        = Functor (Monad.is-functor (PlusN-is-monad {n}))
    module Ⓢ-f             = Functor Ⓢ-is-functor
    module Type-f           = Functor (type-is-functor)
    module TypeSchema-f {n} = Functor (type-schema-is-functor {n})
    module QC-f             = Functor (qconstraint-is-functor)

  private
    fmap-alt₁ : ∀ {a b tv}{r} → (a → b) → Alternative a tv r → Alternative b tv r
    fmap-exp₁ : ∀ {a b tv}{r} → (a → b) → Expression a tv r → Expression b tv r
    map-fmap-alt₁ : ∀ {a b tv}{r} → (a → b) → Alternatives a tv r → Alternatives b tv r
    fmap-alt₁ f (_→′_ {n} (DC c) expr) = DC c →′ fmap-exp₁ (pn.map f) expr
       where module pn = PlusN-f n
    fmap-exp₁ f (Var (DC c)) = Var (DC c)
    fmap-exp₁ f (Var (N x)) = Var (N (f x))
    fmap-exp₁ f (λ′ x) = λ′ (fmap-exp₁ (Ⓢ-f.map f) x)
    fmap-exp₁ f (x · y) = (fmap-exp₁ f x) · (fmap-exp₁ f y)
    fmap-exp₁ f (let₁ x in′ y) = let₁ (fmap-exp₁ f x) in′ (fmap-exp₁ (Ⓢ-f.map f) y)
    fmap-exp₁ f (let₂ x ∷ τ in′ y) = let₂ (fmap-exp₁ f x) ∷ τ in′ (fmap-exp₁ (Ⓢ-f.map f) y)
    fmap-exp₁ f (let₃ n · x ∷ Q ⇒ τ in′ y) = let₃  n · fmap-exp₁ f x ∷ Q ⇒ τ
                                              in′ fmap-exp₁ (Ⓢ-f.map f) y
    fmap-exp₁ f (case x of alts) = case (fmap-exp₁ f x) of map-fmap-alt₁ f alts
    map-fmap-alt₁ f esac = esac
    map-fmap-alt₁ f (x ∣ xs) = fmap-alt₁ f x ∣ map-fmap-alt₁ f xs

  private
    fmap-alt₂ : ∀ {a b ev}{r} → (a → b) → Alternative ev a r → Alternative ev b r
    fmap-exp₂ : ∀ {a b ev}{r} → (a → b) → Expression ev a r → Expression ev b r
    map-fmap-alt₂ : ∀ {a b ev}{r} → (a → b) → Alternatives ev a r → Alternatives ev b r
    fmap-alt₂ f (p →′ expr) = p →′ fmap-exp₂ f expr
    fmap-exp₂ f (Var x) = Var x
    fmap-exp₂ f (λ′ x) = λ′ (fmap-exp₂ f x)
    fmap-exp₂ f (x · y) = fmap-exp₂ f x · fmap-exp₂ f y
    fmap-exp₂ f (let₁ x in′ y) = let₁ fmap-exp₂ f x in′ fmap-exp₂ f y
    fmap-exp₂ f (let₂ x ∷ τ in′ y) = let₂ fmap-exp₂ f x ∷ Type-f.map f τ in′ fmap-exp₂ f y
    fmap-exp₂ f (let₃ n · x ∷ Q ⇒ τ in′ y) = let₃ n · fmap-exp₂ (pn.map f) x
                                                ∷ QC-f.map (pn.map f) Q ⇒ Type-f.map (pn.map f) τ
                                               in′ fmap-exp₂ f y
      where module pn = PlusN-f n
    fmap-exp₂ f (case x of alts) = case (fmap-exp₂ f x) of map-fmap-alt₂ f alts
    map-fmap-alt₂ f esac = esac
    map-fmap-alt₂ f (x ∣ xs) = fmap-alt₂ f x ∣ map-fmap-alt₂ f xs

  private
    fmap-alt-id₁ : {A tv : Set} {f : A → A}{r : Shape}
                 → isIdentity f → isIdentity (fmap-alt₁ {A}{A}{tv}{r} f)
    map-fmap-alt-id₁ : ∀ {a}{tv}{f : a → a}{r : Shape}
                     → isIdentity f → isIdentity (map-fmap-alt₁  {a}{a}{tv}{r} f)
    fmap-exp-id₁ : ∀{A tv : Set}{r : Shape} {f : A → A} → isIdentity f
                 → isIdentity (fmap-exp₁ {A}{A}{tv}{r} f)
    fmap-alt-id₁ {A}{f} f-is-id {_→′_ {n} (DC p) x} = cong (_→′_ (DC p)) (fmap-exp-id₁ (pn.identity f-is-id))
      where module pn = PlusN-f n
    map-fmap-alt-id₁ {r = Unary _} f-is-id {}
    map-fmap-alt-id₁ {r = Nullary} f-is-id {esac} = refl
    map-fmap-alt-id₁ {r = Binary r₁ r₂} f-is-id {x ∣ xs} = cong₂ _∣_ (fmap-alt-id₁ f-is-id)
                                                                     (map-fmap-alt-id₁ f-is-id)
    fmap-exp-id₁ {r = Nullary} f-is-id {Var (DC x)} = refl
    fmap-exp-id₁ {r = Nullary} f-is-id {Var (N x)} = cong Var (cong N f-is-id)
    fmap-exp-id₁ {r = Unary r′} f-is-id {λ′ x} = cong λ′_ (fmap-exp-id₁ (Ⓢ-f.identity f-is-id))
    fmap-exp-id₁ {r = Binary r₁ r₂} f-is-id {x · y} = cong₂ _·_ (fmap-exp-id₁ f-is-id)
                                                                (fmap-exp-id₁ f-is-id)
    fmap-exp-id₁ {r = Binary r₁ r₂} f-is-id {let₁ x in′ y}
      = cong₂ let₁_in′_ (fmap-exp-id₁ f-is-id) (fmap-exp-id₁ (Ⓢ-f.identity f-is-id))
    fmap-exp-id₁ {r = Binary r₁ r₂} f-is-id {let₂ x ∷ τ in′ y}
      = cong₂ (λ a b → let₂ a ∷ τ in′ b) (fmap-exp-id₁ f-is-id)
                                         (fmap-exp-id₁ (Ⓢ-f.identity f-is-id))
    fmap-exp-id₁ {r = Binary r₁ r₂} f-is-id {let₃ n · x ∷ Q ⇒ τ in′ y}
      = cong₂ (λ a b → let₃ n · a ∷ Q ⇒ τ in′ b) (fmap-exp-id₁ f-is-id)
                                                 (fmap-exp-id₁ (Ⓢ-f.identity f-is-id))
    fmap-exp-id₁ {r = Binary r₁ r₂} f-is-id {case x of alts}
      = cong₂ case_of_ (fmap-exp-id₁ f-is-id) (map-fmap-alt-id₁ f-is-id)

  private
    fmap-alt-id₂ : {A ev : Set}{r : Shape}{f : A → A}
                 → isIdentity f → isIdentity (fmap-alt₂ {A}{A}{ev}{r} f)
    map-fmap-alt-id₂ : ∀ {a}{ev}{r : Shape}{f : a → a}
                     → isIdentity f → isIdentity (map-fmap-alt₂  {a}{a}{ev}{r} f)
    fmap-exp-id₂ : ∀{A ev : Set}{r : Shape} {f : A → A}
                 → isIdentity f → isIdentity (fmap-exp₂ {A}{A}{ev}{r} f)
    fmap-alt-id₂ f-is-id {_→′_ {n} p x} = cong (_→′_ p) (fmap-exp-id₂ f-is-id)
    map-fmap-alt-id₂ f-is-id {esac} = refl
    map-fmap-alt-id₂ f-is-id {x ∣ xs} = cong₂ _∣_ (fmap-alt-id₂ f-is-id) (map-fmap-alt-id₂ f-is-id)
    fmap-exp-id₂ {r = Nullary}      f-is-id {Var x} = refl
    fmap-exp-id₂ {r = Unary r′}     f-is-id {λ′ x} = cong λ′_ (fmap-exp-id₂ f-is-id)
    fmap-exp-id₂ {r = Binary r₁ r₂} f-is-id {x · y} = cong₂ _·_ (fmap-exp-id₂ f-is-id)
                                                                (fmap-exp-id₂ f-is-id)
    fmap-exp-id₂ {r = Binary r₁ r₂} f-is-id {let₁ x in′ y} = cong₂ let₁_in′_ (fmap-exp-id₂ f-is-id)
                                                                             (fmap-exp-id₂ f-is-id)
    fmap-exp-id₂ {r = Binary r₁ r₂} f-is-id {let₂ x ∷ τ in′ y} = cong₃ let₂_∷_in′_
                                                                       (fmap-exp-id₂ f-is-id)
                                                                       (Type-f.identity f-is-id)
                                                                       (fmap-exp-id₂ f-is-id)
    fmap-exp-id₂ {r = Binary r₁ r₂} f-is-id {let₃ n · x ∷ Q ⇒ τ in′ y}
      = cong₄ (let₃_·_∷_⇒_in′_ n) (fmap-exp-id₂ (pn.identity f-is-id))
                                  (QC-f.identity (pn.identity f-is-id))
                                  (Type-f.identity (pn.identity f-is-id))
                                  (fmap-exp-id₂ f-is-id)
      where module pn = PlusN-f n
    fmap-exp-id₂ {r = Binary r₁ r₂} f-is-id {case x of alts}
      = cong₂ case_of_ (fmap-exp-id₂ f-is-id) (map-fmap-alt-id₂ f-is-id)

  private
    fmap-alt-comp₁ : {r : Shape} {A B C tv : Set} {f : A → B}{g : B → C} {x : Alternative A tv r}
                   → fmap-alt₁ (g ∘ f) x ≡ fmap-alt₁ g (fmap-alt₁ f x)
    fmap-exp-comp₁ : {r : Shape}{tv A B C : Set} {f : A → B} {g : B → C} {x : Expression A tv r}
                   → fmap-exp₁ (g ∘ f) x ≡ fmap-exp₁ g (fmap-exp₁ f x)
    map-fmap-alt-comp₁ : {r : Shape}{A B C tv : Set}{f : A → B}{g : B → C}{l : Alternatives A tv r}
                       → map-fmap-alt₁ (g ∘ f) l ≡ map-fmap-alt₁ g (map-fmap-alt₁ f l)
    fmap-alt-comp₁ {Nullary}   {x = ()}
    fmap-alt-comp₁ {Binary _ _}{x = ()}
    fmap-alt-comp₁ {Unary r}{f = f}{g}{x = _→′_ {n} (DC p) expr}
      = cong (_→′_ (DC p))
             (combine-composite′ ⦃ Monad.is-functor (PlusN-is-monad {n}) ⦄ {expr}
                                 fmap-exp₁
                                 (fmap-exp-comp₁ {f = pn.map f}{g = pn.map g}{expr}))
      where module pn = PlusN-f n
    map-fmap-alt-comp₁ {l = esac} = refl
    map-fmap-alt-comp₁ {Binary a b}{A}{B}{C}{tv}{l = x ∣ xs} = cong₂ _∣_ (fmap-alt-comp₁ {x = x}) (map-fmap-alt-comp₁)

    fmap-exp-comp₁ {x = Var (N x)} = cong Var (cong N (refl))
    fmap-exp-comp₁ {x = Var (DC x)} = refl
    fmap-exp-comp₁ {f = f}{g}{x = λ′ x }
      = cong λ′_ (combine-composite′ ⦃ Monad.is-functor (Ⓢ-is-monad) ⦄ {x}
                                     fmap-exp₁
                                     (fmap-exp-comp₁ {f = Ⓢ-f.map f}{g = Ⓢ-f.map g}{x}))
    fmap-exp-comp₁ {f = f}{g}{x = x · y } = cong₂ _·_ (fmap-exp-comp₁ {f = f}{g}{x})
                                                      (fmap-exp-comp₁ {f = f}{g}{y})
    fmap-exp-comp₁ {f = f}{g}{x = let₁ x in′ y }
      = cong₂ let₁_in′_ (fmap-exp-comp₁ {f = f}{g}{x})
                        (combine-composite′ ⦃ Monad.is-functor (Ⓢ-is-monad) ⦄ {y}
                                     fmap-exp₁
                                     (fmap-exp-comp₁ {f = Ⓢ-f.map f}{g = Ⓢ-f.map g}{y}))
    fmap-exp-comp₁ {f = f}{g}{x = let₂ x ∷ τ in′ y}
      = cong₂ (λ a b → let₂ a ∷ τ in′ b) (fmap-exp-comp₁ {f = f}{g}{x})
                                         (combine-composite′ ⦃ Monad.is-functor (Ⓢ-is-monad) ⦄ {y}
                                                             fmap-exp₁
                                                             (fmap-exp-comp₁ {f = Ⓢ-f.map f}
                                                                             {g = Ⓢ-f.map g}{y}))
    fmap-exp-comp₁ {f = f}{g}{x = let₃ n · x ∷ Q ⇒ τ in′ y}
      = cong₂ (λ a b → let₃ n · a ∷ Q ⇒ τ in′ b)
              (fmap-exp-comp₁ {f = f}{g}{x})
              (combine-composite′ ⦃ Monad.is-functor (Ⓢ-is-monad) ⦄ {y}
                                  fmap-exp₁
                                  (fmap-exp-comp₁ {f = Ⓢ-f.map f}{g = Ⓢ-f.map g}{y}))
    fmap-exp-comp₁ {f = f}{g}{x = case x of alts } = cong₂ case_of_
                                                           (fmap-exp-comp₁ {f = f}{g}{x})
                                                           map-fmap-alt-comp₁

  private
    fmap-alt-comp₂ : {A B C ev : Set}{r : Shape} {f : A → B} {g : B → C} {x : Alternative ev A r}
                   → fmap-alt₂ (g ∘ f) x ≡ fmap-alt₂ g (fmap-alt₂ f x)
    fmap-exp-comp₂ : {A B C ev : Set}{r : Shape} {f : A → B} {g : B → C} {x : Expression ev A r}
                   → fmap-exp₂ (g ∘ f) x ≡ fmap-exp₂ g (fmap-exp₂ f x)
    map-fmap-alt-comp₂ : ∀{r}{A B C ev : Set} {f : A → B} {g : B → C} {alts : Alternatives ev A r}
                       → map-fmap-alt₂ (g ∘ f) alts ≡ map-fmap-alt₂ g (map-fmap-alt₂ f alts)
    fmap-alt-comp₂ {x = _→′_ {n} p expr} = cong (_→′_ p) fmap-exp-comp₂
    map-fmap-alt-comp₂ {alts = esac} = refl
    map-fmap-alt-comp₂ {alts = x ∣ xs} = cong₂ _∣_ fmap-alt-comp₂ map-fmap-alt-comp₂

    fmap-exp-comp₂ {x = Var a} = refl
    fmap-exp-comp₂ {x = λ′ x } = cong λ′_ fmap-exp-comp₂
    fmap-exp-comp₂ {x = x · y } = cong₂ _·_ fmap-exp-comp₂ fmap-exp-comp₂
    fmap-exp-comp₂ {x = let₁ x in′ y } = cong₂ let₁_in′_ fmap-exp-comp₂ fmap-exp-comp₂
    fmap-exp-comp₂ {x = let₂ x ∷ τ in′ y } = cong₃ let₂_∷_in′_ fmap-exp-comp₂ Type-f.composite fmap-exp-comp₂
    fmap-exp-comp₂ {x = let₃ n · x ∷ Q ⇒ τ in′ y }
      = cong₄ (λ a b c d → let₃ n · a ∷ b ⇒ c in′ d)
              (combine-composite′ ⦃ pnf ⦄ fmap-exp₂ fmap-exp-comp₂)
              (combine-composite ⦃ qconstraint-is-functor ⦄ ⦃ pnf ⦄)
              (combine-composite ⦃ type-is-functor        ⦄ ⦃ pnf ⦄)
              fmap-exp-comp₂
      where pnf = Monad.is-functor (PlusN-is-monad {n})
    fmap-exp-comp₂ {x = case x of alts } = cong₂ case_of_ fmap-exp-comp₂ map-fmap-alt-comp₂

  alternatives-is-functor₁ : ∀{tv}{r} → Functor (λ x → Alternatives x tv r)
  alternatives-is-functor₁ = record { map = map-fmap-alt₁
                                    ; identity = map-fmap-alt-id₁
                                    ; composite = map-fmap-alt-comp₁
                                    }
  alternatives-is-functor₂ : ∀{ev}{r} → Functor (λ x → Alternatives ev x r)
  alternatives-is-functor₂ = record { map = map-fmap-alt₂
                                    ; identity = map-fmap-alt-id₂
                                    ; composite = map-fmap-alt-comp₂
                                    }
  alternative-is-functor₁ : ∀{tv}{r} → Functor (λ x → Alternative x tv r)
  alternative-is-functor₁ = record { map = fmap-alt₁
                                   ; identity = fmap-alt-id₁
                                   ; composite = λ { {x = x} → fmap-alt-comp₁ {x = x} }
                                   }
  alternative-is-functor₂ : ∀{ev}{r} → Functor (λ x → Alternative ev x r)
  alternative-is-functor₂ = record { map = fmap-alt₂
                                   ; identity = fmap-alt-id₂
                                   ; composite = fmap-alt-comp₂
                                   }
  expression-is-functor₁ : ∀{tv}{r} → Functor (λ x → Expression x tv r)
  expression-is-functor₁ {tv}{r} = record { map = fmap-exp₁
                                          ; identity = fmap-exp-id₁
                                          ; composite = λ {A}{B}{C}{f}{g}{x}
                                                        → fmap-exp-comp₁ {r}{tv}{A}{B}{C}{f}{g}{x}
                                          }
  expression-is-functor₂ : ∀{ev}{r} → Functor (λ x → Expression ev x r)
  expression-is-functor₂ = record { map = fmap-exp₂
                                  ; identity = fmap-exp-id₂
                                  ; composite = fmap-exp-comp₂
                                  }

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
{-# OPTIONS --cubical #-}

module Type.Cubical.Path.Equality where

open import Functional
open import Function.Axioms
import      Lvl
open import Type
open import Type.Cubical
open import Type.Cubical.Path
open import Type.Cubical.Path.Proofs as Path
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator
open import Structure.Setoid using (Equiv ; intro)
open import Structure.Type.Identity

private variable ℓ ℓ₁ ℓ₂ ℓₚ : Lvl.Level
private variable T A B C : Type{ℓ}
private variable f : A → B
private variable _▫_ : A → B → C
private variable P : T → Type{ℓ}
private variable x y : T

_≡_ : T → T → Type
_≡_ = Path

instance
  Path-reflexivity : Reflexivity{T = T}(Path)
  Path-reflexivity = intro Path.point

instance
  Path-symmetry : Symmetry{T = T}(Path)
  Path-symmetry = intro Path.reverse

instance
  Path-transitivity : Transitivity{T = T}(Path)
  Path-transitivity = intro Path.concat

instance
  Path-equivalence : Equivalence{T = T}(Path)
  Path-equivalence = intro

instance
  Path-equiv : Equiv(T)
  Path-equiv = intro(Path) ⦃ Path-equivalence ⦄

instance
  Path-congruence₁ : Function(f)
  Path-congruence₁ {f = f} = intro(Path.map f)

instance
  Path-congruence₂ : BinaryOperator(_▫_)
  Path-congruence₂ {_▫_ = _▫_} = intro(Path.map₂(_▫_))

instance
  Path-substitution₁ : UnaryRelator(P)
  Path-substitution₁ {P = P} = intro(Path.liftedSpaceMap P)

instance
  Path-substitution₂ : BinaryRelator(_▫_)
  Path-substitution₂ {_▫_ = _▫_} = intro(Path.liftedSpaceMap₂(_▫_))

instance
  Path-coercion : Path ⊆₂ (_→ᶠ_ {ℓ}{ℓ})
  Path-coercion = intro(Path.spaceMap)

Path-sub-of-reflexive : ⦃ refl : Reflexivity(_▫_) ⦄ → (Path ⊆₂ (_▫_))
Path-sub-of-reflexive {_▫_ = _▫_} = intro(\{a b} → ab ↦ sub₂(Path)(_→ᶠ_) ⦃ Path-coercion ⦄ (congruence₂ᵣ(_▫_)(a) ab) (reflexivity(_▫_) {a}))

instance
  Path-function-extensionality : FunctionExtensionality A B
  Path-function-extensionality = intro Path.mapping

instance
  Path-dependent-function-extensionality : ∀{A : Type{ℓ₁}}{B : (a : A) → Type{ℓ₂}} → DependentFunctionExtensionality A B
  Path-dependent-function-extensionality = intro Path.mapping

instance
  Path-function-application : FunctionApplication A B
  Path-function-application = intro Path.mappingPoint

Path-identity-eliminator : IdentityEliminator{ℓₚ = ℓₚ}(Path{P = T})
IdentityEliminator.elim Path-identity-eliminator P prefl eq  = sub₂(Path)(_→ᶠ_) ⦃ Path-coercion ⦄ (\i → P(\j → eq(Interval.min i j))) prefl

-- TODO: Organize and move everything below

open import Type.Properties.MereProposition
open import Type.Properties.Singleton

prop-is-prop-unit : ⦃ proof : MereProposition(A) ⦄ → IsUnit(MereProposition(A))
MereProposition.uniqueness (IsUnit.unit prop-is-prop-unit) {x} {y} = uniqueness _
MereProposition.uniqueness (IsUnit.uniqueness (prop-is-prop-unit {A = A}) {intro p} i) {x}{y} j = Interval.hComp d x where
  d : Interval → Interval.Partial (Interval.max (Interval.max (Interval.flip i) i) (Interval.max (Interval.flip j) j)) A
  d k (i = Interval.𝟎) = uniqueness(A) {x}{p{x}{y} j} k
  d k (i = Interval.𝟏) = uniqueness(A) {x}{uniqueness(A) {x}{y} j} k
  d k (j = Interval.𝟎) = uniqueness(A) {x}{x} k
  d k (j = Interval.𝟏) = uniqueness(A) {x}{y} k

{-
Path-isUnit : ∀{ℓ}{A : Type{ℓ}} → ⦃ _ : MereProposition(A) ⦄ → (∀{x y : A} → IsUnit(x ≡ y))
IsUnit.unit       (Path-isUnit {A = A}) = uniqueness(A)
IsUnit.uniqueness (Path-isUnit {A = A} ⦃ mere-A ⦄ {x = x} {y = y}) {p} i = Interval.hComp d p where
  d : Interval → Interval.Partial (Interval.max (Interval.flip i) i) (Path x y)
  d j (i = Interval.𝟎) = p
  d j (i = Interval.𝟏) = {!uniqueness(A) {x}{y}!}
-- congruence₁ (prop ↦ MereProposition.uniqueness prop {x}{y}) (IsUnit.uniqueness prop-is-prop-unit {intro (\{x y} → {!p!})})
-}

{-
open import Structure.Setoid.Uniqueness
open import Type.Dependent
-}

-- TODO
-- ∀{eu₁ eu₂ : ∃!{Obj = Obj}(Pred)} → () → (eu₁ ≡ eu₂)

{-
Unique-MereProposition-equivalence : ⦃ prop : ∀{x} → MereProposition(P(x)) ⦄ → (Unique(P) ↔ MereProposition(∃ P))
Unique-MereProposition-equivalence {P = P} = [↔]-intro l r where
  l : Unique(P) ← MereProposition(∃ P)
  l (intro p) {x} {y} px py = mapP([∃]-witness) (p{[∃]-intro x ⦃ px ⦄} {[∃]-intro y ⦃ py ⦄})
  r : Unique(P) → MereProposition(∃ P)
  MereProposition.uniqueness (r p) {[∃]-intro w₁ ⦃ p₁ ⦄} {[∃]-intro w₂ ⦃ p₂ ⦄} i = mapP (mapP (\w p → [∃]-intro w ⦃ p ⦄) (p p₁ p₂) i) {!!} i
  -- mapP [∃]-intro (p p₁ p₂) i ⦃ {!!} ⦄

Unique-prop : ⦃ prop : ∀{x} → MereProposition(P(x)) ⦄ → MereProposition(Unique(P))
MereProposition.uniqueness Unique-prop {u₁} {u₂} i {x} {y} px py j = Interval.hComp d x where
  d : Interval → Interval.Partial (Interval.max (Interval.max (Interval.flip i) i) (Interval.max (Interval.flip j) j)) A
  d k (i = Interval.𝟎) = {!!}
  d k (i = Interval.𝟏) = {!!}
  d k (j = Interval.𝟎) = {!!}
  d k (j = Interval.𝟏) = {!!}

[∃!trunc]-to-existence : ⦃ prop : ∀{x} → MereProposition(Pred(x)) ⦄ → HTrunc₁(∃!{Obj = Obj}(Pred)) → HomotopyLevel(0)(∃{Obj = Obj}(Pred))
[∃!trunc]-to-existence {Pred = Pred} (trunc ([∧]-intro e u)) = intro e (\{e₂} i → [∃]-intro (u ([∃]-proof e₂) ([∃]-proof e) i) ⦃ {!!} ⦄)
-- MereProposition.uniqueness test) {u _ _ _}
-- sub₂(_≡_)(_→ᶠ_) ⦃ [≡][→]-sub ⦄ (congruence₁(Pred) ?) ?
[∃!trunc]-to-existence (trunc-proof i) = {!!}
-}

{-
[∃!]-squashed-witness : HTrunc₁(∃!{Obj = Obj}(Pred)) → Obj
[∃!]-squashed-witness (trunc eu) = [∃]-witness([∧]-elimₗ eu)
[∃!]-squashed-witness (trunc-proof {trunc ([∧]-intro e₁ u₁)} {trunc ([∧]-intro e₂ u₂)} i) = u₁ ([∃]-proof e₁) ([∃]-proof e₂) i
[∃!]-squashed-witness (trunc-proof {trunc ([∧]-intro e₁ u₁)} {trunc-proof j} i) = {!!}
[∃!]-squashed-witness (trunc-proof {trunc-proof i₁} {trunc x} i) = {!!}
[∃!]-squashed-witness (trunc-proof {trunc-proof i₁} {trunc-proof i₂} i) = {!!}
-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module PureLambda where

data D : Set where
  lam : (D -> D) -> D

_·_ : D -> D -> D
lam f · x = f x

δ : D
δ = lam (\x -> x · x)

loop : D
loop = δ · δ

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- 2010-09-07 Andreas

module IrrelevantRecordMatching where

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

wrongElim : {A : Set} -> .(Prod A A) -> A
wrongElim (a , a') = a
-- needs to fail because a is irrelevant


text:
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection

pattern `Nat = def (quote Nat) []

unquoteDecl f =
  declareDef (vArg f) `Nat >>= λ _ →
  freshName "aux" >>= λ aux →
  declareDef (vArg aux) `Nat >>= λ _ →
  defineFun f (clause [] (def aux []) ∷ [])

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
module Structure.LinearAlgebra where

import      Lvl
open import Data
open import Data.Tuple
open import Functional hiding (id)
open import Function.Equals
open import Function.Proofs
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
-- open import Relator.Equals
-- open import Relator.Equals.Proofs
open import Structure.Setoid
open import Structure.Setoid.Uniqueness
open import Structure.Setoid.Uniqueness.Proofs
open import Structure.Function.Domain
import      Structure.Function.Linear as Linear
open import Structure.Operator.Field
open import Structure.Operator.Group
open import Structure.Operator.Properties hiding (commutativity)
open import Structure.Operator.Vector
open import Syntax.Number
open import Type

-- Finite dimensional linear algebra
-- TODO: Apparently, most of linear algebra will not work in constructive logic

module _
  {ℓᵥ ℓₛ : Lvl.Level}
  {V : Type{ℓᵥ}}
  ⦃ equiv-V : Equiv(V) ⦄
  {S : Type{ℓₛ}}
  ⦃ equiv-S : Equiv(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

  module _ where
    open VectorSpace(vectorSpace)

    -- A list of scalars
    Scalars : ℕ → Type
    Scalars(n) = Vec(n)(S) -- TODO: Prove that this type is a group if its underlying type (S) is a group. THen proceed to prove that injective-kernelᵣ holds with LinearCombination(_) being a homomorphism, which one can deduce that LinearlyIndependent is equivalent to Injective.

    -- A list of vectors
    Vectors : ℕ → Type
    Vectors(n) = Vec(n)(V)

    module _ where
      -- TODO: Make this a record instead, and then define an "eval"-function and prove LinearCombination-addition for this eval function (homomorphism)
      -- A specific linear combination of vectors (specific as specified by scalars).
      -- Linear combination of 0 scalars and vectors are the zero vector.
      -- Linear combination of 1 scalar and vector is just scalar on vector multiplication.
      -- Example: LinearCombination {4} sf vf = (sf[0] ⋅ₛᵥ vf[0]) +ᵥ (sf[1] ⋅ₛᵥ vf[1]) +ᵥ (sf[2] ⋅ₛᵥ vf[2]) +ᵥ (sf[3] ⋅ₛᵥ vf[3])
      LinearCombination : ∀{n} → Vectors(n) → Scalars(n) → V
      LinearCombination {0}       _ _ = 𝟎ᵥ
      LinearCombination {1}       vf sf = Vec.proj(sf)(0) ⋅ₛᵥ Vec.proj(vf)(0)
      LinearCombination {𝐒(𝐒(n))} vf sf = (Vec.proj(sf)(0) ⋅ₛᵥ Vec.proj(vf)(0)) +ᵥ (LinearCombination {𝐒(n)} (Vec.tail vf) (Vec.tail sf))

      postulate LinearCombination-addition    : ∀{n}{sf₁ sf₂}{vf} → (LinearCombination{n}(vf)(sf₁) +ᵥ LinearCombination{n}(vf)(sf₂) ≡ LinearCombination{n}(vf)(sf₁ ⦗ Vec.map₂ (_+ₛ_) ⦘ sf₂))
      postulate LinearCombination-subtraction : ∀{n}{sf₁ sf₂}{vf} → (LinearCombination{n}(vf)(sf₁) −ᵥ LinearCombination{n}(vf)(sf₂) ≡ LinearCombination{n}(vf)(sf₁ ⦗ Vec.map₂ (_−ₛ_) ⦘ sf₂))

      -- Spanning(vf) ⇔ (VSP = Span(vf))
      -- A set of vectors is spanning the vector space when every vector in the vector space can be represented as a linear combination of the set of vectors.
      Spanning : ∀{n} → Vectors(n) → Stmt
      Spanning(vf) = (∀{v} → ∃(sf ↦ LinearCombination(vf)(sf) ≡ v))

      -- Basis(vf) ⇔ (vf is a basis)
      -- A set of vectors is a basis when every vector in the vector space can be represented as a unique linear combination of the set of vectors.
      -- A set of vectors is a basis when they span the vector space and is linearly independent.
      Basis : ∀{n} → Vectors(n) → Stmt
      Basis(vf) = (∀{v} → ∃!(sf ↦ LinearCombination(vf)(sf) ≡ v)) -- TODO: Should be some kind of set equality. Could be impossible to prove the uniqueness otherwise because one can just permute for commutative scalars

      -- A set of vectors is linearly independent when there is no vector that can be represented as a linear combination by the others.
      LinearlyIndependent : ∀{n} → Vectors(n) → Stmt
      LinearlyIndependent{n}(vf) = ∀{sf} → (LinearCombination(vf)(sf) ≡ 𝟎ᵥ) → (∀{i} → Vec.proj(sf)(i) ≡ 𝟎ₛ) -- sf ⊜ fill(𝟎ₛ)

      postulate independent-injective : ∀{n}{vf} → LinearlyIndependent{n}(vf) ↔ (∀{sf₁ sf₂} → (LinearCombination(vf)(sf₁) ≡ LinearCombination(vf)(sf₂)) → (∀{i}→ Vec.proj(sf₁)(i) ≡ Vec.proj(sf₂)(i))) -- TODO: Vec.proj(sf₁) ⊜ Vec.proj(sf₂)
      -- TODO: Is there some axioms that make this happen? I remember this pattern from somewhere, that injectivity is equivalent to stuff being the identity of something. Maybe it is usually expressed using a kernel? See the note written above
      -- TODO: Express this as injectivity when `Injective` is general over setoids

      basis-span-independent : ∀{n}{vf : Vectors(n)} → Basis(vf) ↔ (Spanning(vf) ∧ LinearlyIndependent(vf))
      basis-span-independent{n}{vf} = [↔]-intro (uncurry l) (([↔]-to-[←] [→][∧]-distributivityₗ) ([∧]-intro r₁ r₂)) where
        l : Spanning(vf) → LinearlyIndependent(vf) → Basis(vf)
        l spanning indep {v} = [∃!]-intro existence uniqueness where
          existence : ∃(sf ↦ LinearCombination(vf)(sf) ≡ v)
          existence = spanning

          postulate uniqueness : Unique(sf ↦ LinearCombination(vf)(sf) ≡ v)
          -- uniqueness = ([↔]-elimₗ Uniqueness-Injectivity) (([↔]-elimᵣ independent-injective) indep)
          -- TODO: `Injective` over setoids is blocking this proof. It is at the moment proving something incorrect

        r₁ : Basis(vf) → Spanning(vf)
        r₁(proof) {v} = [∃!]-existence(proof{v})

        postulate r₂ : Basis(vf) → LinearlyIndependent(vf)
        -- TODO: `Injective` over setoids is blocking this proof. It is at the moment proving something incorrect

      -- Cardinality of a set of linearly independent vectors is always less than the cardinality of a set of spanning vectors
      postulate independent-less-than-spanning : ∀{n₁ n₂} → ∀{vf₁} → LinearlyIndependent{n₁}(vf₁) → ∀{vf₂} → Spanning{n₂}(vf₂) → (n₁ ≤ n₂)

      -- Existence of a subset of spanning vectors which is a basis
      -- TODO: postulate basis-from-spanning : ∀{n}{vf} → ⦃ _ : Spanning{n}(vf) ⦄ → ∃(m ↦ (m ≤ n) ∧ ∃(f ↦ Basis{n}(vf ∘ f) ∧ Injective(f)))

      -- Existence of a finite set of vectors which spans the vector space
      -- A "finite dimensional vector space" is sometimes defined as a vector space which satisfies this proposition.
      postulate span-existence : ∃(n ↦ ∃(vf ↦ Spanning{n}(vf)))
      -- TODO: Usually, this exists because one can take the whole set

      -- Existence of a basis
      postulate basis-existence : ∃(n ↦ ∃(vf ↦ Basis{n}(vf)))

      -- A set of linearly independent vectors is smaller than a set of basis vectors
      postulate independent-lesser-than-basis-number : ∀{m n} → {vfₘ : Vectors(m)} → LinearlyIndependent(vfₘ) → {vfₙ : Vectors(n)} → Basis(vfₙ) → (m ≤ n)

      -- Every set of basis vectors are equal in size
      postulate basis-equal-number : ∀{m n} → {vfₘ : Vectors(m)} → Basis(vfₘ) → {vfₙ : Vectors(n)} → Basis(vfₙ) → (m ≡ n)

      -- The dimension of the vector space
      dim :  ℕ
      dim = [∃]-witness(basis-existence)

      -- Existence of a superset of linearly independent vectors which is a basis
      -- TODO: basis-from-linearly-independent : ∀{n}{vf} → ⦃ _ : Spanning{n}(vf) ⦄ → ∃(m ↦ (m ≥ n) ∧ ∃(f ↦ Basis{n}(vf ∘ f) ∧ Injective(f)))

      postulate basis-from-dim-spanning : ∀{vf} → Spanning{dim}(vf) → Basis{dim}(vf)

      postulate basis-from-dim-independent : ∀{vf} → LinearlyIndependent{dim}(vf) → Basis{dim}(vf)

      -- TODO: Move to some algebraic structure?
      -- Nilpotent(f) = ∃(n ↦ ∀{v} → (f ^ n ≡ 𝟎ᵥ))

    module _ where
      private LinearMap = Linear.LinearMap(_+ᵥ_)(_⋅ₛᵥ_)(_+ᵥ_)(_⋅ₛᵥ_)

      postulate linear-map-id : LinearMap(Function.id)

      -- v is a eigenvector for the eigenvalue 𝜆 of the linear transformation f
      Eigenvector : (V → V) → S → V → Stmt
      Eigenvector(f)(𝜆)(v) = ((v ≢ 𝟎ᵥ) → (f(v) ≡ 𝜆 ⋅ₛᵥ v))

      -- 𝜆 is a eigenvalue of the linear transformation f
      -- Multiplication by an eigenvalue can replace a linear transformation for certain vectors.
      Eigenvalue : (V → V) → S → Stmt
      Eigenvalue(f)(𝜆) = (∀{v : V} → Eigenvector(f)(𝜆)(v))

      -- Two linear mappings are similiar when there is a basis in which they are equal.
      -- Similiar : (f : V → V) → ⦃ _ : LinearMap(f) ⦄ → (g : V → V) → ⦃ _ : LinearMap(g) ⦄ → Stmt
      -- Similiar(f)(g) = (∀{v} → ∃(b ↦ Bijective(b) ∧ (f(v) ≡ (b ∘ g ∘ (inv(b)))(v))))

    record DotProductSpace (_∙_ : V → V → S) (_≤_ : S → S → Stmt) : Stmt where
      field
        commutativity     : Commutativity(_∙_)
        linearmapₗ        : ∀{v₂} → Linear.LinearMap(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) (_∙ v₂)
        positive          : ∀{v} → (𝟎ₛ ≤ (v ∙ v))
        injective-zero    : ∀{v} → ((v ∙ v) ≡ 𝟎ₛ) → (v ≡ 𝟎ᵥ)

      postulate [⋅ₛᵥ]-commuting : ∀{s}{v₁ v₂} → ((s ⋅ₛᵥ v₁) ∙ v₂) ≡ (v₁ ∙ (s ⋅ₛᵥ v₂))
      postulate almost-injectivity-zeroₗ : ∀{v₁} → (∀{v₂} → ((v₁ ∙ v₂) ≡ 𝟎ₛ)) → (v₁ ≡ 𝟎ᵥ)
      postulate injectivityₗ : ∀{v₁ v₂} → (∀{v₃} → ((v₁ ∙ v₃) ≡ (v₂ ∙ v₃))) → (v₁ ≡ v₂)

      module Norm (√ : S → S) where
        -- The length of a vector
        norm : V → S
        norm(v) = √(v ∙ v)

        -- The positive part of a scalar
        abs : S → S
        abs(s) = √(s ⋅ₛ s)

        postulate homogeneity : ∀{s}{v} → norm(s ⋅ₛᵥ v) ≡ abs(s) ⋅ₛ norm(v)
        postulate triangle-inequality : ∀{v₁ v₂} → (norm(v₁ +ᵥ v₂) ≤ (norm(v₁) +ₛ norm(v₂)))
        postulate positivity : ∀{v} → (𝟎ₛ ≤ norm(v))
        postulate injectivity-zero : ∀{v} → (norm(v) ≡ 𝟎ₛ) → (v ≡ 𝟎ᵥ)
        postulate mult-inequality : ∀{v₁ v₂} → (abs(v₁ ∙ v₂) ≤ (norm(v₁) ⋅ₛ norm(v₂)))

        -- Two vectors are orthogonal when they are perpendicular.
        Orthogonal : V → V → Stmt
        Orthogonal(v₁)(v₂) = (v₁ ∙ v₂ ≡ 𝟎ₛ)

        {-
        OrthogonalAll : ∀{n} → Vectors(n) → Stmt
        OrthogonalAll{0}       (vf) = ⊤
        OrthogonalAll{1}       (vf) = Orthogonal(vf(0))(vf(1))
        OrthogonalAll{𝐒(𝐒(n))} (vf) = (OrthogonalAll{n} (vf)) ∧ Orthogonal(vf(n))(vf(𝐒(n)))
        -}

        postulate hypotenuse-length : ∀{v₁ v₂} → ⦃ _ : Orthogonal(v₁)(v₂) ⦄ → ((v₁ +ᵥ v₂) ∙ (v₁ +ᵥ v₂) ≡ (v₁ ∙ v₁) +ₛ (v₂ ∙ v₂))

        -- Transforms a vector to an unit vector in the same direction.
        normalize : (v : V) → ⦃ _ : v ≢ 𝟎ᵥ ⦄ → V
        normalize(v) ⦃ proof ⦄ = (⅟ₛ (norm(v)) ⦃ contrapositiveᵣ (injectivity-zero) (proof) ⦄) ⋅ₛᵥ v

        postulate norm-of-normalize : ∀{v} → ⦃ nonzero : (v ≢ 𝟎ᵥ) ⦄ → (norm(normalize(v) ⦃ nonzero ⦄) ≡ 𝟏ₛ)

--  -- TODO: Is it okay for VSP₂ to have a different scalar field compared to VSP? Some stuff will not be compatible (like addition for the same scalar type)?
--  module _ {V₂} ⦃ lang₂ ⦄ (VSP₂ : VectorSpace(V₂)(S) ⦃ lang₂ ⦄) where
--    open Language ⦃ ... ⦄
--    open VectorSpace ⦃ ... ⦄
--
--    private _+ᵥ₁_ = _+ᵥ_ ⦃ lang ⦄
--    private _⋅ₛᵥ₁_ = _⋅ₛᵥ_ ⦃ lang ⦄
--    private _+ᵥ₂_ = _+ᵥ_ ⦃ lang₂ ⦄
--    private _⋅ₛᵥ₂_ = _⋅ₛᵥ_ ⦃ lang₂ ⦄
--
--    private LinearMap₁₂ = Linear.LinearMap(_+ᵥ₁_)(_⋅ₛᵥ₁_)(_+ᵥ₂_)(_⋅ₛᵥ₂_)
--    private LinearMap₂₁ = Linear.LinearMap(_+ᵥ₂_)(_⋅ₛᵥ₂_)(_+ᵥ₁_)(_⋅ₛᵥ₁_)
--
--    module _ where
--      -- Kernel(f)(v) ⇔ (v ∈ Kernel(f))
--      Kernel : (f : V → V₂) → ⦃ _ : LinearMap₁₂(f) ⦄ → V → Stmt
--      Kernel(f)(v) = (f(v) ≡ 𝟎ᵥ ⦃ lang₂ ⦄ ⦃ VSP₂ ⦄)
--
--      -- TODO: Move away the module for two vector spaces from one so that dim is not bound to V
--      -- rank : (V → V₂) → ℕ
--      -- rank(_) = dim ⦃ VSP₂ ⦄
--
--    module _ where
--      postulate linear-map-const-zero : LinearMap₁₂(const(𝟎ᵥ ⦃ lang₂ ⦄ ⦃ VSP₂ ⦄))
--
--      -- The inverse of an invertible linear mapping is a linear mapping
--      postulate linear-inverse : ∀{f} → ⦃ _ : Bijective(f) ⦄ → LinearMap₁₂(f) → LinearMap₂₁(inv(f))
--
--      -- Injectivity for only the zero vector implies injectivity
--      postulate injective-zero : ∀{f} → ⦃ _ : LinearMap₁₂(f) ⦄ → (∀{v} → (f(v) ≡ 𝟎ᵥ ⦃ lang₂ ⦄ ⦃ VSP₂ ⦄) → (v ≡ 𝟎ᵥ ⦃ lang ⦄ ⦃ VSP ⦄)) → Injective(f)
--
--    -- module _ {_∙₁_ : V → V → S}{_≤₁_} {_∙₂_ : V₂ → V₂ → S}{_≤₂_} (DPSP₁ : DotProductSpace(_∙₁_)(_≤₁_)) (DPSP₂ : DotProductSpace(_∙₂_)(_≤₂_)) where
--    --   Adjoint : (f : V → V₂) → ⦃ _ : LinearMap₁₂(f) ⦄ → (g : V₂ → V) → ⦃ _ : LinearMap₂₁(g) ⦄ → Stmt
--    --   Adjoint(f)(g) = (∀{v₁ : V}{v₂ : V₂} → (f(v₁) ∙₂ v₂ ≡ v₁ ∙₁ g(v₂)))


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category

module Categories.Pullback {o ℓ e} (C : Category o ℓ e) where

open Category C

open import Level

record Pullback {X Y Z}(f : X ⇒ Z)(g : Y ⇒ Z) : Set (o ⊔ ℓ ⊔ e) where
  field
    P  : Obj
    p₁ : P ⇒ X
    p₂ : P ⇒ Y

  field
    .commutes : f ∘ p₁ ≡ g ∘ p₂

    universal : ∀ {Q}(q₁ : Q ⇒ X)(q₂ : Q ⇒ Y)
              → .(commutes : (f ∘ q₁ ≡ g ∘ q₂)) → (Q ⇒ P)

    .universal-unique : ∀ {Q} {q₁ : Q ⇒ X} {q₂ : Q ⇒ Y}
                        .{commutes : f ∘ q₁ ≡ g ∘ q₂}
                          (u : Q ⇒ P)
                          .(p₁∘u≡q₁ : p₁ ∘ u ≡ q₁)
                          .(p₂∘u≡q₂ : p₂ ∘ u ≡ q₂)
                      →   u ≡ universal q₁ q₂ commutes

    .p₁∘universal≡q₁  : ∀ {Q} {q₁ : Q ⇒ X} {q₂ : Q ⇒ Y}
                          .{commutes : f ∘ q₁ ≡ g ∘ q₂}
                      →   (p₁ ∘ universal q₁ q₂ commutes ≡ q₁)

    .p₂∘universal≡q₂  : ∀ {Q} {q₁ : Q ⇒ X} {q₂ : Q ⇒ Y}
                          .{commutes : f ∘ q₁ ≡ g ∘ q₂}
                      →   (p₂ ∘ universal q₁ q₂ commutes ≡ q₂)

glue : ∀ {W X Y Z : Obj} {f0 : W ⇒ X}{f : X ⇒ Z}{g : Y ⇒ Z}
         → (p : Pullback f g) → Pullback f0 (Pullback.p₁ p) → Pullback (f ∘ f0) g
glue {f0 = f0} {f} {g} R L = record {
                      P = L.P;
                      p₁ = L.p₁;
                      p₂ = R.p₂ ∘ L.p₂;
                      commutes = begin (f ∘ f0) ∘ L.p₁   ↓⟨ assoc ⟩
                                       f ∘ f0 ∘ L.p₁     ↓⟨ ∘-resp-≡ʳ L.commutes ⟩
                                       f ∘ R.p₁ ∘ L.p₂   ↑⟨ assoc ⟩
                                       (f ∘ R.p₁) ∘ L.p₂ ↓⟨ ∘-resp-≡ˡ R.commutes ⟩
                                       (g ∘ R.p₂) ∘ L.p₂ ↓⟨ assoc ⟩
                                       g ∘ R.p₂ ∘ L.p₂   ∎;
                      universal = λ q₁ q₂ commutes → L.universal q₁ (R.universal (f0 ∘ q₁) q₂ (Equiv.trans (Equiv.sym assoc) commutes))
                                                                    (Equiv.sym R.p₁∘universal≡q₁);
                      universal-unique = λ {Q} {q₁} u p₁∘u≡q₁ p₂∘u≡q₂ →
                            L.universal-unique u p₁∘u≡q₁
                                       (R.universal-unique (L.p₂ ∘ u) (begin
                                                                         R.p₁ ∘ L.p₂ ∘ u   ↑⟨ assoc ⟩
                                                                         (R.p₁ ∘ L.p₂) ∘ u ↑⟨ ∘-resp-≡ˡ L.commutes ⟩
                                                                         (f0 ∘ L.p₁) ∘ u   ↓⟨ assoc ⟩
                                                                         f0 ∘ L.p₁ ∘ u     ↓⟨ ∘-resp-≡ʳ p₁∘u≡q₁ ⟩
                                                                         f0 ∘ q₁           ∎)
                                                   (Equiv.trans (Equiv.sym assoc) p₂∘u≡q₂));
                      p₁∘universal≡q₁ = L.p₁∘universal≡q₁;
                      p₂∘universal≡q₂ = Equiv.trans assoc (Equiv.trans (∘-resp-≡ʳ L.p₂∘universal≡q₂) R.p₂∘universal≡q₂) }
   where
    module L = Pullback L
    module R = Pullback R
    open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Issue2641.Import where

open import Agda.Builtin.Nat

five : Nat
five = 5


text:
{-# OPTIONS --safe --warning=error #-}

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)
open import Setoids.Setoids
open import Groups.Definition
open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Groups.Lemmas
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas

module Groups.FreeProduct.UniversalProperty {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) {a b : _} {A : I → Set a} {S : (i : I) → Setoid {a} {b} (A i)} {_+_ : (i : I) → (A i) → (A i) → A i} (decidableGroups : (i : I) → (x y : A i) → ((Setoid._∼_ (S i) x y)) || ((Setoid._∼_ (S i) x y) → False)) (G : (i : I) → Group (S i) (_+_ i)) where

open import Groups.FreeProduct.Definition decidableIndex decidableGroups G
open import Groups.FreeProduct.Setoid decidableIndex decidableGroups G
open import Groups.FreeProduct.Addition decidableIndex decidableGroups G
open import Groups.FreeProduct.Group decidableIndex decidableGroups G

private
  universalPropertyFunction' : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → {i : I} → ReducedSequenceBeginningWith i → C
  universalPropertyFunction' {_+_ = _+_} H fs homs {i} (ofEmpty .i g nonZero) = fs i g
  universalPropertyFunction' {_+_ = _+_} H fs homs {i} (prependLetter .i g nonZero x x₁) = (fs i g) + universalPropertyFunction' H fs homs x

universalPropertyFunction : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → ReducedSequence → C
universalPropertyFunction H fs homs empty = Group.0G H
universalPropertyFunction H fs homs (nonempty i x) = universalPropertyFunction' H fs homs x

private
  upWellDefined' : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → {m n : I} → (x : ReducedSequenceBeginningWith m) (y : ReducedSequenceBeginningWith n) → (eq : =RP' x y) → Setoid._∼_ T (universalPropertyFunction H fs homs (nonempty m x)) (universalPropertyFunction H fs homs (nonempty n y))
  upWellDefined' H fs homs (ofEmpty m g nonZero) (ofEmpty n g₁ nonZero₁) eq with decidableIndex m n
  ... | inl refl = GroupHom.wellDefined (homs m) eq
  upWellDefined' H fs homs (prependLetter m g nonZero x x₁) (prependLetter n g₁ nonZero₁ y x₂) eq with decidableIndex m n
  ... | inl refl = Group.+WellDefined H (GroupHom.wellDefined (homs m) (_&&_.fst eq)) (upWellDefined' H fs homs x y (_&&_.snd eq))

  upWellDefined : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → (x : ReducedSequence) (y : ReducedSequence) → (eq : _=RP_ x y) → Setoid._∼_ T (universalPropertyFunction H fs homs x) (universalPropertyFunction H fs homs y)
  upWellDefined {T = T} H fs homs empty empty eq = Equivalence.reflexive (Setoid.eq T)
  upWellDefined H fs homs (nonempty i w1) (nonempty j w2) eq = upWellDefined' H fs homs w1 w2 eq

private
  upPrepend : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → {j : I} (y : ReducedSequence) → (g : A j) .(pr : _) → Setoid._∼_ T (universalPropertyFunction H fs homs (prepend j g pr y)) ((fs j g) + universalPropertyFunction H fs homs y)
  upPrepend {T = T} H fs homs empty g pr = Equivalence.symmetric (Setoid.eq T) (Group.identRight H)
  upPrepend {T = T} H fs homs {j} (nonempty i (ofEmpty .i h nonZero)) g pr with decidableIndex j i
  ... | inr j!=i = Equivalence.reflexive (Setoid.eq T)
  ... | inl refl with decidableGroups j ((j + g) h) (Group.0G (G j))
  ... | inl x = Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (imageOfIdentityIsIdentity (homs j))) (Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (GroupHom.wellDefined (homs j) x)) (GroupHom.groupHom (homs j)))
  ... | inr x = GroupHom.groupHom (homs j)
  upPrepend {T = T} H fs homs {j} (nonempty k (prependLetter .k h nonZero y _)) g pr with decidableIndex j k
  ... | inr j!=k = Equivalence.reflexive (Setoid.eq T)
  ... | inl refl with decidableGroups j ((j + g) h) (Group.0G (G j))
  ... | inl x = transitive (symmetric (Group.identLeft H)) (transitive (Group.+WellDefined H (transitive (symmetric (imageOfIdentityIsIdentity (homs k))) (transitive (GroupHom.wellDefined (homs k) (Equivalence.symmetric (Setoid.eq (S k)) x)) (GroupHom.groupHom (homs k)))) reflexive) (symmetric (Group.+Associative H)))
    where
      open Setoid T
      open Equivalence eq
  ... | inr x = transitive (Group.+WellDefined H (GroupHom.groupHom (homs k)) reflexive) (symmetric (Group.+Associative H))
    where
      open Setoid T
      open Equivalence eq

private
  upHom : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → {i : I} (x : ReducedSequenceBeginningWith i) (y : ReducedSequence) → Setoid._∼_ T (universalPropertyFunction H fs homs (plus' x y)) (universalPropertyFunction' H fs homs x + universalPropertyFunction H fs homs y)
  upHom {T = T} H fs homs (ofEmpty _ g nonZero) empty = Equivalence.symmetric (Setoid.eq T) (Group.identRight H)
  upHom {T = T} H fs homs (ofEmpty j g nonZero) (nonempty i (ofEmpty .i h nonZero1)) with decidableIndex j i
  ... | inr j!=i = Equivalence.reflexive (Setoid.eq T)
  ... | inl refl with decidableGroups j ((j + g) h) (Group.0G (G j))
  ... | inl x = Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (imageOfIdentityIsIdentity (homs j))) (Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (GroupHom.wellDefined (homs j) x)) (GroupHom.groupHom (homs j)))
  ... | inr x = GroupHom.groupHom (homs j)
  upHom {T = T} H fs homs (ofEmpty j g nonZero) (nonempty i (prependLetter .i h nonZero1 x x₁)) with decidableIndex j i
  ... | inr j!=i = Equivalence.reflexive (Setoid.eq T)
  ... | inl refl with decidableGroups j ((j + g) h) (Group.0G (G j))
  ... | inr _ = Equivalence.transitive (Setoid.eq T) (Group.+WellDefined H (GroupHom.groupHom (homs j)) (Equivalence.reflexive (Setoid.eq T))) (Equivalence.symmetric (Setoid.eq T) (Group.+Associative H))
  ... | inl eq1 = Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (Group.identLeft H)) (Equivalence.transitive (Setoid.eq T) (Group.+WellDefined H (Equivalence.transitive (Setoid.eq T) (Equivalence.symmetric (Setoid.eq T) (imageOfIdentityIsIdentity (homs j))) (Equivalence.transitive (Setoid.eq T) (GroupHom.wellDefined (homs j) (Equivalence.symmetric (Setoid.eq (S j)) eq1)) (GroupHom.groupHom (homs j)))) (Equivalence.reflexive (Setoid.eq T))) (Equivalence.symmetric (Setoid.eq T) (Group.+Associative H)))
  upHom {T = T} H fs homs (prependLetter j g nonZero {k} w k!=j) empty = Equivalence.transitive (Setoid.eq T) (Equivalence.transitive (Setoid.eq T) (upWellDefined H fs homs (plus' (prependLetter j g _ w k!=j) empty) (prepend j g _ (nonempty k w)) (prependWD' g nonZero (plus' w empty) (nonempty k w) (plusEmptyRight w))) (upPrepend H fs homs (nonempty k w) g nonZero)) (Equivalence.symmetric (Setoid.eq T) (Group.identRight H))
  upHom {T = T} H fs homs (prependLetter j g nonZero {k} m k!=j) (nonempty i x2) = transitive (upPrepend H fs homs (plus' m (nonempty i x2)) g nonZero) (transitive (Group.+WellDefined H reflexive (upHom H fs homs m (nonempty i x2))) (Group.+Associative H))
    where
      open Setoid T
      open Equivalence eq

universalPropertyHom : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → GroupHom FreeProductGroup H (universalPropertyFunction H fs homs)
GroupHom.wellDefined (universalPropertyHom {T = T} H fs homs) {x} {y} eq = upWellDefined H fs homs x y eq
GroupHom.groupHom (universalPropertyHom {T = T} H fs homs) {empty} {y} = Equivalence.symmetric (Setoid.eq T) (Group.identLeft H)
GroupHom.groupHom (universalPropertyHom {T = T} H fs homs) {nonempty i x} {empty} = transitive (upWellDefined H fs homs (nonempty i x +RP empty) (nonempty i x) (plusEmptyRight x)) (symmetric (Group.identRight H))
  where
    open Setoid T
    open Equivalence eq
GroupHom.groupHom (universalPropertyHom H fs homs) {nonempty i x} {nonempty j y} = upHom H fs homs x (nonempty j y)

universalPropertyFunctionHasProperty : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → {i : I} → (g : A i) → (nz : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → Setoid._∼_ T (fs i g) (universalPropertyFunction H fs homs (injection g nz))
universalPropertyFunctionHasProperty {T = T} H fs homs g nz = Equivalence.reflexive (Setoid.eq T)

private
  universalPropertyFunctionUniquelyHasPropertyLemma : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → (otherFunction : ReducedSequence → C) → (isHom : GroupHom FreeProductGroup H otherFunction) → ({i : I} → (g : A i) → .(nz : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → Setoid._∼_ T (fs i g) (otherFunction (injection g nz))) → {k l : I} (neq : (k ≡ l) → False) (r : ReducedSequenceBeginningWith l) (g : A k) .(nz : (Setoid._∼_ (S k) g (Group.0G (G k)) → False)) → Setoid._∼_ T (otherFunction (nonempty k (prependLetter k g nz r neq))) (fs k g + universalPropertyFunction' H fs homs r)
  universalPropertyFunctionUniquelyHasPropertyLemma {T = T} H fs homs otherFunction hom x {k} {l} neq (ofEmpty .l g2 nonZero) g nz = transitive (GroupHom.wellDefined hom {nonempty k (prependLetter k g nz (ofEmpty l g2 nonZero) neq)} {nonempty _ (ofEmpty k g nz) +RP nonempty _ (ofEmpty l g2 nonZero)} t) (transitive (GroupHom.groupHom hom {nonempty k (ofEmpty k g nz)} {nonempty _ (ofEmpty l g2 nonZero)}) (Group.+WellDefined H (symmetric (x g nz)) (symmetric (x g2 nonZero))))
    where
      open Setoid T
      open Equivalence eq
      t : Setoid._∼_ freeProductSetoid (nonempty k (prependLetter k g nz (ofEmpty l g2 nonZero) neq)) (prepend k g nz (nonempty l (ofEmpty l g2 nonZero)))
      t with decidableIndex k l
      ... | inl p = exFalso (neq p)
      ... | inr _ with decidableIndex k k
      ... | inr bad = exFalso (bad refl)
      ... | inl refl = Equivalence.reflexive (Setoid.eq (S k)) ,, =RP'reflex (ofEmpty l g2 _)
  universalPropertyFunctionUniquelyHasPropertyLemma {T = T} H fs homs otherFunction hom x {k} {l} neq (prependLetter .l h nonZero r pr) g nz = transitive (GroupHom.wellDefined hom {nonempty _ (prependLetter k g nz (prependLetter l h nonZero r pr) neq)} {(nonempty k (ofEmpty k g nz)) +RP (nonempty l (prependLetter l h nonZero r pr))} t) (transitive (GroupHom.groupHom hom {nonempty k (ofEmpty k g nz)} {nonempty l (prependLetter l h nonZero r pr)}) (Group.+WellDefined H (symmetric (x g nz)) (universalPropertyFunctionUniquelyHasPropertyLemma H fs homs otherFunction hom x pr r h nonZero)))
    where
      open Setoid T
      open Equivalence eq
      t : Setoid._∼_ freeProductSetoid (nonempty k (prependLetter k g nz (prependLetter l h nonZero r pr) neq)) (prepend k g nz (nonempty l (prependLetter l h nonZero r pr)))
      t with decidableIndex k l
      ... | inl bad = exFalso (neq bad)
      ... | inr k!=l with decidableIndex k k
      ... | inr bad = exFalso (bad refl)
      ... | inl refl with decidableIndex l l
      ... | inr bad = exFalso (bad refl)
      ... | inl refl = Equivalence.reflexive (Setoid.eq (S k)) ,, ((Equivalence.reflexive (Setoid.eq (S l))) ,, =RP'reflex r)

universalPropertyFunctionUniquelyHasProperty : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+_ : C → C → C} (H : Group T _+_) → (fs : (i : I) → (A i → C)) → (homs : (i : I) → GroupHom (G i) H (fs i)) → (otherFunction : ReducedSequence → C) → (isHom : GroupHom FreeProductGroup H otherFunction) → ({i : I} → (g : A i) → .(nz : (Setoid._∼_ (S i) g (Group.0G (G i))) → False) → Setoid._∼_ T (fs i g) (otherFunction (injection g nz))) → (r : ReducedSequence) → Setoid._∼_ T (otherFunction r) (universalPropertyFunction H fs homs r)
universalPropertyFunctionUniquelyHasProperty H fs homs otherFunction hom prop empty = imageOfIdentityIsIdentity hom
universalPropertyFunctionUniquelyHasProperty {T = T} H fs homs otherFunction hom prop (nonempty i (ofEmpty .i g nonZero)) = Equivalence.symmetric (Setoid.eq T) (prop g nonZero)
universalPropertyFunctionUniquelyHasProperty {T = T} H fs homs otherFunction hom prop (nonempty i (prependLetter .i g nonZero {k} (ofEmpty .k g1 nonZero1) x1)) = transitive (GroupHom.wellDefined hom {_} {(nonempty i (ofEmpty i g nonZero)) +RP (nonempty k (ofEmpty k g1 nonZero1))} t) (transitive (GroupHom.groupHom hom {nonempty i (ofEmpty i g nonZero)}) (Group.+WellDefined H (symmetric (prop g nonZero)) (symmetric (prop g1 nonZero1))))
  where
    open Setoid T
    open Equivalence eq
    t : Setoid._∼_ freeProductSetoid (nonempty i (prependLetter i g nonZero (ofEmpty k g1 nonZero1) x1)) (prepend i g nonZero (nonempty k (ofEmpty k g1 nonZero1)))
    t with decidableIndex i k
    ... | inl p = exFalso (x1 p)
    ... | inr _ with decidableIndex i i
    ... | inr bad = exFalso (bad refl)
    ... | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, =RP'reflex (ofEmpty k g1 nonZero1)
universalPropertyFunctionUniquelyHasProperty {T = T} H fs homs otherFunction hom prop (nonempty i (prependLetter .i g nonZero {k} (prependLetter .k g2 nonZero2 x x2) x1)) = transitive (GroupHom.wellDefined hom {nonempty i (prependLetter i g nonZero (prependLetter k g2 nonZero2 x x2) x1)} {(nonempty i (ofEmpty i g nonZero)) +RP (nonempty k (prependLetter k g2 nonZero2 x x2))} t) (transitive (GroupHom.groupHom hom {nonempty i (ofEmpty i g nonZero)} {nonempty k (prependLetter k g2 nonZero2 x x2)}) (Group.+WellDefined H (symmetric (prop g nonZero)) (universalPropertyFunctionUniquelyHasPropertyLemma H fs homs otherFunction hom prop x2 x g2 nonZero2)))
  where
    open Setoid T
    open Equivalence eq
    t : Setoid._∼_ freeProductSetoid (nonempty i (prependLetter i g nonZero (prependLetter k g2 nonZero2 x x2) x1)) (prepend i g nonZero (nonempty k (prependLetter k g2 nonZero2 x x2)))
    t with decidableIndex i k
    ... | inl x = exFalso (x1 x)
    ... | inr _ = =RP'reflex (prependLetter i g nonZero (prependLetter k g2 nonZero2 x x2) x1)


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

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data ⊥ : Set where

{-# NON_COVERING #-}

f : ∀ b → b ≡ true → ⊥
f false ()

bad : ⊥
bad = f true refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

-- Yoneda Lemma.  In total, provides:
-- * the Yoneda Embedding (called embed here) from any Category C into Presheaves C
--   Worth noticing that there is no 'locally small' condition here; however, if one looks at
--   the levels involved, there is indeed a raise from that of C to that of Presheaves C.
-- * The traditional Yoneda lemma (yoneda-inverse) which says that for any object a of C, and
--   any Presheaf F over C (where our presheaves are over Setoids), then
--   Hom[ Presheaves C] (Functor.F₀ embed a , F) ≅ Functor.F₀ F a
--   as Setoids. In addition, Yoneda (yoneda) also says that this isomorphism is natural in a and F.
open import Level
open import Function using (_$_; Inverse) -- else there's a conflict with the import below
open import Function.Equality using (Π; _⟨$⟩_; cong)
open import Relation.Binary using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Hom using (module Hom; Hom[_][-,_]; Hom[_][-,-])
open import Categories.Functor.Bifunctor
open import Categories.Functor.Presheaf
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

private
  variable
    o ℓ e : Level

module Yoneda (C : Category o ℓ e) where
  open Category C
  open HomReasoning
  open MR C
  open Functor
  open NaturalTransformation
  open NT-Hom C
  private
    module CE = Category.Equiv C
    module C = Category C

  -- The Yoneda embedding functor
  embed : Functor C (Presheaves C)
  embed = record
    { F₀           = Hom[ C ][-,_]
    ; F₁           = Hom[A,C]⇒Hom[B,C] -- A⇒B induces a NatTrans on the Homs.
    ; identity     = identityˡ ○_
    ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ʳ h₁≈h₂ ○ assoc
    ; F-resp-≈     = λ f≈g h≈i → ∘-resp-≈ f≈g h≈i
    }

  -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor
  yoneda-inverse : (a : Obj) (F : Presheaf C (Setoids ℓ e)) →
    Inverse (Category.hom-setoid (Presheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
  yoneda-inverse a F = record
    { f = λ nat → η nat a ⟨$⟩ id
    ; f⁻¹ = λ x → ntHelper record
        { η       = λ X → record
          { _⟨$⟩_ = λ X⇒a → F₁ F X⇒a ⟨$⟩ x
          ; cong  = λ i≈j → F-resp-≈ F i≈j SE.refl
          }
        ; commute = λ {X} {Y} Y⇒X {f} {g} f≈g →
          let module SFY = Setoid (F₀ F Y) in
          let module SR = SetoidR (F₀ F Y) in
          SR.begin
             F₁ F (id ∘ f ∘ Y⇒X) ⟨$⟩ x   SR.≈⟨ F-resp-≈ F (identityˡ ○ ∘-resp-≈ˡ f≈g) (SE.refl {x}) ⟩
             F₁ F (g ∘ Y⇒X) ⟨$⟩ x        SR.≈⟨ homomorphism F SE.refl ⟩
             F₁ F Y⇒X ⟨$⟩ (F₁ F g ⟨$⟩ x)
           SR.∎
        }
    ; cong₁ = λ i≈j → i≈j CE.refl
    ; cong₂ = λ i≈j y≈z → F-resp-≈ F y≈z i≈j
    ; inverse = (λ Fa → identity F SE.refl) , λ nat {x} {z} z≈y →
        let module S     = Setoid (F₀ F x) in
        S.trans (S.sym (commute nat z CE.refl))
                (cong (η nat x) (identityˡ ○ identityˡ ○ z≈y))
    }
    where module SE = Setoid (F₀ F a)

  private
    -- in this bifunctor, a presheaf from Presheaves C goes from C to Setoids ℓ e,
    -- but the over Setoids has higher level than the hom setoids.
    Nat[Hom[C][-,c],F] : Bifunctor (Presheaves C) (Category.op C) (Setoids _ _)
    Nat[Hom[C][-,c],F] = Hom[ Presheaves C ][-,-] ∘F (Functor.op embed ∘F πʳ ※ πˡ)

    -- in this bifunctor, it needs to go from Presheaves which maps C to Setoids ℓ e,
    -- so the universe level needs to be lifted.
    FC : Bifunctor (Presheaves C) (Category.op C) (Setoids _ _)
    FC = LiftSetoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ) ∘F eval {C = Category.op C} {D = Setoids ℓ e}

    module yoneda-inverse {a} {F} = Inverse (yoneda-inverse a F)

  -- the two bifunctors above are naturally isomorphic.
  -- it is easy to show yoneda-inverse first then to yoneda.
  yoneda : NaturalIsomorphism Nat[Hom[C][-,c],F] FC
  yoneda = record
    { F⇒G = ntHelper record
      { η       = λ where
        (F , A) → record
          { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α)
          ; cong  = λ i≈j → lift (i≈j CE.refl)
          }
      ; commute = λ where
        {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ)
      }
    ; F⇐G = ntHelper record
      { η       = λ where
        (F , A) → record
          { _⟨$⟩_ = λ where
            (lift x) → yoneda-inverse.f⁻¹ x
          ; cong  = λ where
            (lift i≈j) y≈z → F-resp-≈ F y≈z i≈j
          }
      ; commute = λ where
        (α , f) (lift eq) eq′ → helper′ α f eq eq′
      }
    ; iso = λ where
      (F , A) → record
        { isoˡ = λ {α β} i≈j {X} y≈z →
          let module S = Setoid (F₀ F X)
          in S.trans ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl)
        ; isoʳ = λ where
          (lift eq) →
            let module S = Setoid (F₀ F A)
            in lift (S.trans ( yoneda-inverse.inverseˡ {F = F} _) eq)
        }
    }
    where helper : ∀ {F : Functor (Category.op C) (Setoids ℓ e)}
                     {A B : Obj} (f : B ⇒ A)
                     (β γ : NaturalTransformation Hom[ C ][-, A ] F) →
                   Setoid._≈_ (F₀ Nat[Hom[C][-,c],F] (F , A)) β γ →
                   Setoid._≈_ (F₀ F B) (η β B ⟨$⟩ f ∘ id) (F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id))
          helper {F} {A} {B} f β γ β≈γ = S.begin
            η β B ⟨$⟩ f ∘ id          S.≈⟨ cong (η β B) (id-comm ○ (⟺ identityˡ)) ⟩
            η β B ⟨$⟩ id ∘ id ∘ f     S.≈⟨ commute β f CE.refl ⟩
            F₁ F f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F₁ F f) (β≈γ CE.refl) ⟩
            F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎
            where module S where
                    open Setoid (F₀ F B) public
                    open SetoidR (F₀ F B) public

          helper′ : ∀ {F G : Functor (Category.op C) (Setoids ℓ e)}
                      {A B Z : Obj}
                      {h i : Z ⇒ B}
                      {X Y : Setoid.Carrier (F₀ F A)}
                      (α : NaturalTransformation F G)
                      (f : B ⇒ A) →
                      Setoid._≈_ (F₀ F A) X Y →
                      h ≈ i →
                      Setoid._≈_ (F₀ G Z) (F₁ G h ⟨$⟩ (η α B ⟨$⟩ (F₁ F f ⟨$⟩ X)))
                                          (η α Z ⟨$⟩ (F₁ F (f ∘ i) ⟨$⟩ Y))
          helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin
            F₁ G h ⟨$⟩ (η α B ⟨$⟩ (F₁ F f ⟨$⟩ X)) S.≈˘⟨ commute α h (S′.sym (cong (F₁ F f) eq)) ⟩
            η α Z ⟨$⟩ (F₁ F h ⟨$⟩ (F₁ F f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) (F-resp-≈ F eq′ S′.refl) ⟩
            η α Z ⟨$⟩ (F₁ F i ⟨$⟩ (F₁ F f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) (homomorphism F (Setoid.refl (F₀ F A))) ⟩
            η α Z ⟨$⟩ (F₁ F (f ∘ i) ⟨$⟩ Y)        S.∎
            where module S where
                    open Setoid (F₀ G Z) public
                    open SetoidR (F₀ G Z) public
                  module S′ = Setoid (F₀ F B)

  module yoneda = NaturalIsomorphism yoneda