text:
{-

The sheaf property of a presheaf on a distributive lattice or a basis thereof
can be expressed as preservation of limits over diagrams defined in this file.

-}
{-# OPTIONS --safe #-}

module Cubical.Categories.DistLatticeSheaf.Diagram where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty
open import Cubical.Data.Sigma
open import Cubical.Data.FinData
open import Cubical.Data.FinData.Order
open import Cubical.Data.Sum

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary.Poset

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Limits.Limits
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Instances.DistLattice

open import Cubical.Algebra.DistLattice
open import Cubical.Algebra.Lattice
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.DistLattice.BigOps

private
  variable
    ℓ ℓ' ℓ'' : Level

data DLShfDiagOb (n : ℕ) : Type where
  sing : Fin n → DLShfDiagOb n
  pair : (i j : Fin n) → i <'Fin j → DLShfDiagOb n

data DLShfDiagHom (n : ℕ) : DLShfDiagOb n → DLShfDiagOb n → Type where
  idAr : {x : DLShfDiagOb n} → DLShfDiagHom n x x
  singPairL : {i j : Fin n} {i<j : i <'Fin j}  → DLShfDiagHom n (sing i) (pair i j i<j)
  singPairR : {i j : Fin n} {i<j : i <'Fin j}→ DLShfDiagHom n (sing j) (pair i j i<j)

module DLShfDiagHomPath where
  variable
   n : ℕ

  -- DLShfDiagHom n x y is a retract of Code x y
  Code : (x y : DLShfDiagOb n) → Type
  Code (sing i) (sing j) = i ≡ j
  Code (sing i) (pair j k j<k) =
      (Σ[ p ∈ (i ≡ j) ] Σ[ i<k ∈ i <'Fin k ] PathP (λ ι → p ι <'Fin k) i<k j<k)
    ⊎ (Σ[ p ∈ (i ≡ k) ] Σ[ j<i ∈ j <'Fin i ] PathP (λ ι → j <'Fin p ι) j<i j<k)
  Code (pair i j i<j) (sing k) = ⊥
  Code (pair i j i<j) (pair k l k<l) =
    Σ[ p ∈ (i ≡ k) × (j ≡ l) ] PathP (λ ι → fst p ι <'Fin snd p ι) i<j k<l

  isSetCode : ∀ (x y : DLShfDiagOb n) → isSet (Code x y)
  isSetCode (sing _) (sing _) = isProp→isSet (isSetFin _ _)
  isSetCode (sing i) (pair j k j<k) =
    isSet⊎
      (isSetΣ (isProp→isSet (isSetFin _ _))
        λ _ → isSetΣ (isProp→isSet (≤'FinIsPropValued _ _))
        λ _ → isOfHLevelPathP 2 (isProp→isSet (≤'FinIsPropValued _ _)) _ _)
      (isSetΣ (isProp→isSet (isSetFin _ _))
        λ _ → isSetΣ (isProp→isSet (≤'FinIsPropValued _ _))
        λ _ → isOfHLevelPathP 2 (isProp→isSet (≤'FinIsPropValued _ _)) _ _)
  isSetCode (pair _ _ _) (sing _) = isProp→isSet isProp⊥
  isSetCode (pair _ _ _) (pair _ _ _) =
    isSetΣ
      (isSet× (isProp→isSet (isSetFin _ _)) (isProp→isSet (isSetFin _ _)))
        λ _ → isOfHLevelPathP 2 (isProp→isSet (≤'FinIsPropValued _ _)) _ _

  encode : (x y : DLShfDiagOb n) → DLShfDiagHom n x y → Code x y
  encode (sing i) (sing .i) idAr = refl
  encode (sing i) (pair .i j i<j) singPairL = inl (refl , i<j , refl)
  encode (sing j) (pair i .j i<j) singPairR = inr (refl , i<j , refl)
  encode (pair i j i<j) (pair .i .j .i<j) idAr = (refl , refl) , refl

  decode : (x y : DLShfDiagOb n) → Code x y → DLShfDiagHom n x y
  decode (sing i) (sing j) p = subst (λ k → DLShfDiagHom _ (sing i) (sing k)) p idAr
  decode (sing i) (pair j k j<k) (inl (p , i<k , q)) =
    transport (λ ι → DLShfDiagHom _ (sing i) (pair (p ι) k (q ι))) singPairL
  decode (sing i) (pair k j k<j) (inr (p , k<i , q)) =
    transport (λ ι → DLShfDiagHom _ (sing i) (pair k (p ι) (q ι))) singPairR
  decode (pair i j i<j) (pair k l k<l) (_ , p) =
    transport (λ ι → DLShfDiagHom _ (pair _ _ i<j) (pair _ _ (p ι))) idAr

  codeRetract : ∀ (x y : DLShfDiagOb n) (f : DLShfDiagHom n x y)
              → decode x y (encode x y f) ≡ f
  codeRetract (sing i) (sing .i) idAr = transportRefl idAr
  codeRetract (sing i) (pair .i k i<k) singPairL = transportRefl singPairL
  codeRetract (sing i) (pair j .i j<i) singPairR = transportRefl singPairR
  codeRetract (pair i j i<j) (pair .i .j .i<j) idAr = transportRefl idAr

  isSetDLShfDiagHom : ∀ (x y : DLShfDiagOb n) → isSet (DLShfDiagHom n x y)
  isSetDLShfDiagHom x y = isSetRetract (encode x y) (decode x y)
                                         (codeRetract x y) (isSetCode x y)

open Category
DLShfDiag : ℕ → Category ℓ-zero ℓ-zero
ob (DLShfDiag n) = DLShfDiagOb n
Hom[_,_] (DLShfDiag n) = DLShfDiagHom n
id (DLShfDiag n) = idAr
_⋆_ (DLShfDiag n) idAr f = f
_⋆_ (DLShfDiag n) singPairL idAr = singPairL
_⋆_ (DLShfDiag n) singPairR idAr = singPairR
⋆IdL (DLShfDiag n) _ = refl
⋆IdR (DLShfDiag n) idAr = refl
⋆IdR (DLShfDiag n) singPairL = refl
⋆IdR (DLShfDiag n) singPairR = refl
⋆Assoc (DLShfDiag n) idAr _ _ = refl
⋆Assoc (DLShfDiag n) singPairL idAr _ = refl
⋆Assoc (DLShfDiag n) singPairR idAr _ = refl
isSetHom (DLShfDiag n) = let open DLShfDiagHomPath in (isSetDLShfDiagHom _ _)

module _ (L' : DistLattice ℓ) where
 private
  L = fst L'
  LCat = (DistLatticeCategory L') ^op
  instance
   _ = snd L'

 open DistLatticeStr ⦃...⦄
 open Join L'
 open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice L'))
 open PosetStr (IndPoset .snd) hiding (_≤_)
 open MeetSemilattice (Lattice→MeetSemilattice (DistLattice→Lattice L'))
      using (∧≤RCancel ; ∧≤LCancel)
 open Order (DistLattice→Lattice L')

 open Category LCat
 open Functor
 open Cone

 FinVec→Diag : {n : ℕ} → FinVec L n → Functor (DLShfDiag n) LCat
 F-ob (FinVec→Diag α) (sing i) = α i
 F-ob (FinVec→Diag α) (pair i j _) = α i ∧l α j
 F-hom (FinVec→Diag α) idAr = is-refl _
 F-hom (FinVec→Diag α) singPairL = ≤m→≤j _ _ (∧≤RCancel _ _)
 F-hom (FinVec→Diag α) singPairR = ≤m→≤j _ _ (∧≤LCancel _ _)
 F-id (FinVec→Diag α) = is-prop-valued _ _ _ _
 F-seq (FinVec→Diag α) _ _ = is-prop-valued _ _ _ _

 ⋁Cone : {n : ℕ} (α : FinVec L n) → Cone (FinVec→Diag α) (⋁ α)
 coneOut (⋁Cone α) (sing i) = ind≤⋁ α i
 coneOut (⋁Cone α) (pair i _ _) = is-trans _ (α i) _ (≤m→≤j _ _ (∧≤RCancel _ _)) (ind≤⋁ α i)
 coneOutCommutes (⋁Cone α) _ = is-prop-valued _ _ _ _

 isLimCone⋁Cone : {n : ℕ} (α : FinVec L n) → isLimCone (FinVec→Diag α) (⋁ α) (⋁Cone α)
 fst (fst (isLimCone⋁Cone α u uCone)) = ⋁IsMax α _ λ i → uCone .coneOut (sing i)
 snd (fst (isLimCone⋁Cone α u uCone)) _ = is-prop-valued _ _ _ _
 snd (isLimCone⋁Cone α _ uCone) _ = Σ≡Prop (λ _ → isPropIsConeMor uCone (⋁Cone α) _)
                                           (is-prop-valued _ _ _ _)

module PullbacksAsDLShfDiags (C : Category ℓ ℓ')
                             (cspan : Cospan C)
                             (pback : Pullback C cspan) where

 open Functor
 open Cone
 open Cospan ⦃...⦄
 open Pullback ⦃...⦄
 instance
  _ = cspan
  _ = pback

 cospanAsDiag : Functor (DLShfDiag 2) C
 F-ob cospanAsDiag (sing zero) = l
 F-ob cospanAsDiag (sing (suc zero)) = r
 F-ob cospanAsDiag (pair _ _ _) = m
 F-hom cospanAsDiag idAr = id C
 F-hom cospanAsDiag {x = sing zero} singPairL = s₁
 F-hom cospanAsDiag {x = sing (suc zero)} singPairL = s₂
 F-hom cospanAsDiag {x = sing zero} singPairR = s₁
 F-hom cospanAsDiag {x = sing (suc zero)} singPairR = s₂
 F-id cospanAsDiag = refl
 F-seq cospanAsDiag idAr idAr = sym (⋆IdL C _)
 F-seq cospanAsDiag idAr singPairL = sym (⋆IdL C _)
 F-seq cospanAsDiag idAr singPairR = sym (⋆IdL C _)
 F-seq cospanAsDiag singPairL idAr = sym (⋆IdR C _)
 F-seq cospanAsDiag singPairR idAr = sym (⋆IdR C _)

 pbPrAsCone : Cone cospanAsDiag pbOb
 coneOut pbPrAsCone (sing zero) = pbPr₁
 coneOut pbPrAsCone (sing (suc zero)) = pbPr₂
 coneOut pbPrAsCone (pair _ _ _) = pbPr₁ ⋆⟨ C ⟩ s₁
 coneOutCommutes pbPrAsCone idAr = ⋆IdR C _
 coneOutCommutes pbPrAsCone (singPairL {zero}) = refl
 coneOutCommutes pbPrAsCone (singPairL {suc zero}) = sym pbCommutes
 coneOutCommutes pbPrAsCone (singPairR {zero} {zero}) = refl
 coneOutCommutes pbPrAsCone (singPairR {zero} {suc zero}) = sym pbCommutes
 coneOutCommutes pbPrAsCone (singPairR {suc zero} {zero}) = refl
 coneOutCommutes pbPrAsCone (singPairR {suc zero} {suc zero}) = sym pbCommutes

 pbAsLimit : isLimCone cospanAsDiag pbOb pbPrAsCone
 pbAsLimit c cc = uniqueExists (fromPBUnivProp .fst .fst)
                               toConeMor
                               (λ _ → isPropIsConeMor cc pbPrAsCone _)
                               (λ f cf → cong fst (fromPBUnivProp .snd (f , fromConeMor cf)))
  where
  fromPBUnivProp : ∃![ hk ∈ C [ c , Pullback.pbOb pback ] ]
                      (coneOut cc (sing zero) ≡ hk ⋆⟨ C ⟩ pbPr₁) ×
                      (coneOut cc (sing (suc zero)) ≡ hk ⋆⟨ C ⟩ pbPr₂)
  fromPBUnivProp = univProp
     (cc .coneOut (sing zero)) (cc .coneOut (sing (suc zero)))
     (cc .coneOutCommutes (singPairL {i<j = s≤s z≤}) ∙ sym (cc .coneOutCommutes singPairR))

  toConeMor : isConeMor cc pbPrAsCone (fromPBUnivProp .fst .fst)
  toConeMor (sing zero) = sym (fromPBUnivProp .fst .snd .fst)
  toConeMor (sing (suc zero)) = sym (fromPBUnivProp .fst .snd .snd)
  toConeMor (pair zero j _) = path
   where
   path : fromPBUnivProp .fst .fst ⋆⟨ C ⟩ (pbPr₁ ⋆⟨ C ⟩ s₁) ≡ cc .coneOut (pair zero j _)
   path = fromPBUnivProp .fst .fst ⋆⟨ C ⟩ (pbPr₁ ⋆⟨ C ⟩ s₁)
        ≡⟨ sym (⋆Assoc C _ _ _) ⟩
          (fromPBUnivProp .fst .fst ⋆⟨ C ⟩ pbPr₁) ⋆⟨ C ⟩ s₁
        ≡⟨ cong (λ f → f ⋆⟨ C ⟩ s₁) (sym (fromPBUnivProp .fst .snd .fst)) ⟩
          cc .coneOut (sing zero) ⋆⟨ C ⟩ s₁
        ≡⟨ cc .coneOutCommutes singPairL ⟩
          cc .coneOut (pair zero j _) ∎
  toConeMor (pair (suc zero) j _) = path
   where
   path : fromPBUnivProp .fst .fst ⋆⟨ C ⟩ (pbPr₁ ⋆⟨ C ⟩ s₁)
        ≡ cc .coneOut (pair (suc zero) j _)
   path = fromPBUnivProp .fst .fst ⋆⟨ C ⟩ (pbPr₁ ⋆⟨ C ⟩ s₁)
        ≡⟨ cong (λ f → fromPBUnivProp .fst .fst ⋆⟨ C ⟩ f) pbCommutes ⟩
          fromPBUnivProp .fst .fst ⋆⟨ C ⟩ (pbPr₂ ⋆⟨ C ⟩ s₂)
        ≡⟨ sym (⋆Assoc C _ _ _) ⟩
          (fromPBUnivProp .fst .fst ⋆⟨ C ⟩ pbPr₂) ⋆⟨ C ⟩ s₂
        ≡⟨ cong (λ f → f ⋆⟨ C ⟩ s₂) (sym (fromPBUnivProp .fst .snd .snd)) ⟩
          cc .coneOut (sing (suc zero)) ⋆⟨ C ⟩ s₂
        ≡⟨ cc .coneOutCommutes singPairL ⟩
          cc .coneOut (pair (suc zero) j _) ∎

  fromConeMor : {f : C [ c , pbOb ]}
              → isConeMor cc pbPrAsCone f
              → (coneOut cc (sing zero) ≡ f ⋆⟨ C ⟩ pbPr₁) ×
                (coneOut cc (sing (suc zero)) ≡ f ⋆⟨ C ⟩ pbPr₂)
  fst (fromConeMor cf) = sym (cf (sing zero))
  snd (fromConeMor cf) = sym (cf (sing (suc zero)))

module DLShfDiagsAsPullbacks (C : Category ℓ ℓ')
                             (F : Functor (DLShfDiag 2) C)
                             (limF : LimCone F) where

 open Cospan
 open Pullback
 open Functor ⦃...⦄
 open Cone ⦃...⦄
 open LimCone ⦃...⦄
 instance
  _ = F
  _ = limF
  _ = limF .limCone

 DiagAsCospan : Cospan C
 l DiagAsCospan = F-ob (sing zero)
 m DiagAsCospan = F-ob (pair zero (suc zero) (s≤s z≤))
 r DiagAsCospan = F-ob (sing (suc zero))
 s₁ DiagAsCospan = F-hom singPairL
 s₂ DiagAsCospan = F-hom singPairR

 LimAsPullback : Pullback C DiagAsCospan
 pbOb LimAsPullback = lim
 pbPr₁ LimAsPullback = coneOut (sing zero)
 pbPr₂ LimAsPullback = coneOut (sing (suc zero))
 pbCommutes LimAsPullback = coneOutCommutes singPairL ∙ sym (coneOutCommutes singPairR)
 univProp LimAsPullback {d = d} f g cSq =
  uniqueExists
    (fromUnivProp .fst .fst)
      (sym (fromUnivProp .fst .snd (sing zero)) , sym (fromUnivProp .fst .snd (sing (suc zero))))
        (λ _ → isProp× (isSetHom C _ _) (isSetHom C _ _))
          λ h' trs → cong fst (fromUnivProp .snd (h' , toConeMor h' trs))
  where
  theCone : Cone F d
  Cone.coneOut theCone (sing zero) = f
  Cone.coneOut theCone (sing (suc zero)) = g
  Cone.coneOut theCone (pair zero zero ())
  Cone.coneOut theCone (pair zero (suc zero) (s≤s z≤)) = f ⋆⟨ C ⟩ DiagAsCospan .s₁
  Cone.coneOut theCone (pair (suc zero) zero ())
  Cone.coneOut theCone (pair (suc zero) (suc zero) (s≤s ()))
  Cone.coneOutCommutes theCone {u} idAr = cong (seq' C (Cone.coneOut theCone u)) F-id
                                        ∙ ⋆IdR C (Cone.coneOut theCone u)
  Cone.coneOutCommutes theCone {sing zero} {pair ._ (suc zero) (s≤s z≤)} singPairL = refl
  Cone.coneOutCommutes theCone {sing (suc zero)} {pair ._ (suc zero) (s≤s ())} singPairL
  Cone.coneOutCommutes theCone {sing (suc zero)} {pair zero ._ (s≤s z≤)} singPairR = sym cSq
  Cone.coneOutCommutes theCone {sing (suc zero)} {pair (suc zero) ._ (s≤s ())} singPairR

  fromUnivProp : ∃![ h ∈ C [ d , lim ] ] isConeMor theCone limCone h
  fromUnivProp = LimCone.univProp limF d theCone

  toConeMor : ∀ (h' : C [ d , lim ])
            → (f ≡ h' ⋆⟨ C ⟩ coneOut (sing zero)) × (g ≡ h' ⋆⟨ C ⟩ coneOut (sing (suc zero)))
            → isConeMor theCone limCone h'
  toConeMor h' (tr₁ , tr₂) (sing zero) = sym tr₁
  toConeMor h' (tr₁ , tr₂) (sing (suc zero)) = sym tr₂
  toConeMor h' (tr₁ , tr₂) (pair zero (suc zero) (s≤s z≤)) = path
    where
    path : h' ⋆⟨ C ⟩ coneOut (pair zero (suc zero) (s≤s z≤))
         ≡ f ⋆⟨ C ⟩ F-hom singPairL
    path = h' ⋆⟨ C ⟩ coneOut (pair zero (suc zero) (s≤s z≤))
         ≡⟨ cong (seq' C h') (sym (coneOutCommutes singPairL)) ⟩
           h' ⋆⟨ C ⟩ (coneOut (sing zero) ⋆⟨ C ⟩ F-hom singPairL)
         ≡⟨ sym (⋆Assoc C _ _ _) ⟩
           (h' ⋆⟨ C ⟩ coneOut (sing zero)) ⋆⟨ C ⟩ F-hom singPairL
         ≡⟨ cong (λ x → seq' C x (F-hom singPairL)) (sym tr₁) ⟩
           f ⋆⟨ C ⟩ F-hom singPairL ∎
  toConeMor h' (tr₁ , tr₂) (pair (suc zero) (suc zero) (s≤s ()))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module list-thms where

-- see list-thms2 for more

open import bool
open import bool-thms
open import functions
open import list
open import nat
open import nat-thms
open import product-thms
open import logic

++[] : ∀{ℓ}{A : Set ℓ} → (l : 𝕃 A) → l ++ [] ≡ l
++[] [] = refl
++[] (x :: xs) rewrite ++[] xs = refl

++-assoc : ∀ {ℓ}{A : Set ℓ} (l1 l2 l3 : 𝕃 A) →
           (l1 ++ l2) ++ l3 ≡ l1 ++ (l2 ++ l3)
++-assoc [] l2 l3 = refl
++-assoc (x :: xs) l2 l3 rewrite ++-assoc xs l2 l3 = refl

length-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) →
            length (l1 ++ l2) ≡ (length l1) + (length l2)
length-++ [] l2 = refl
length-++ (h :: t) l2 rewrite length-++ t l2 = refl

map-append : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} →
             (f : A → B) (l1 l2 : 𝕃 A) →
             map f (l1 ++ l2) ≡ (map f l1) ++ (map f l2)
map-append f [] l2 = refl
map-append f (x :: xs) l2 rewrite map-append f xs l2 = refl

map-compose : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'}{C : Set ℓ''} →
             (f : B → C) (g : A → B) (l : 𝕃 A) →
             map f (map g l) ≡ map (f ∘ g) l
map-compose f g [] = refl
map-compose f g (x :: xs) rewrite map-compose f g xs = refl

foldr-monoid : ∀{ℓ}{A B : Set ℓ}{l₁ l₂ : 𝕃 A}{_⊗_ : B → B → B}{f : A → B}{b : B}
  {p-sym : ∀{a} → b ⊗ a ≡ a}
  {p-assoc : ∀{a b c} → a ⊗ (b ⊗ c) ≡ (a ⊗ b) ⊗ c}
  → (foldr (λ x r → (f x) ⊗ r) b l₁) ⊗ (foldr (λ x r → (f x) ⊗ r) b l₂) ≡ foldr (λ x r → (f x) ⊗ r) b (l₁ ++ l₂)
foldr-monoid {ℓ}{A}{B}{[]}{l₂}{_⊗_}{f}{b}{p-sym} rewrite p-sym {foldr (λ x → _⊗_ (f x)) b l₂} = refl
foldr-monoid {ℓ}{A}{B}{y :: ys}{l₂}{_⊗_}{f}{b}{p-sym}{p-assoc}
 rewrite
   sym (p-assoc {f y}{foldr (λ x → _⊗_ (f x)) b ys}{foldr (λ x → _⊗_ (f x)) b l₂})
 | foldr-monoid {l₁ = ys}{l₂}{_⊗_}{f}{b}{p-sym}{p-assoc}
 = refl

foldr-append : ∀{ℓ₂}{B : Set ℓ₂}{l₁ l₂ : 𝕃 (𝕃 B)} → (foldr _++_ [] l₁) ++ (foldr _++_ [] l₂) ≡ foldr _++_ [] (l₁ ++ l₂)
foldr-append {l₁ = []}{l₂} = refl
foldr-append {_}{B}{l₁ = x :: xs}{l₂} rewrite sym (foldr-append {l₁ = xs}{l₂}) = ++-assoc x (foldr _++_ [] xs) (foldr _++_ [] l₂)

foldr-append-fun : ∀{ℓ₁ ℓ₂}{A : Set ℓ₁}{B : Set ℓ₂}{l₁ l₂ : 𝕃 (A → 𝕃 B)}{a : A}
  → (foldr (λ f → _++_ (f a)) [] l₁) ++ (foldr (λ f → _++_ (f a)) [] l₂) ≡ foldr (λ f → _++_ (f a)) [] (l₁ ++ l₂)
foldr-append-fun {l₁ = []}{_}{a} = refl
foldr-append-fun {l₁ = x :: l₁}{l₂}{a}
 rewrite
    ++-assoc (x a) (foldr (λ f → _++_ (f a)) [] l₁) (foldr (λ f → _++_ (f a)) [] l₂)
  | foldr-append-fun {l₁ = l₁}{l₂}{a}
 = refl

foldr-map : ∀{ℓ}{A : Set ℓ}{l : 𝕃 A} → l ≡ foldr _++_ [] (map (λ x₁ → x₁ :: []) l)
foldr-map {_}{_}{[]} = refl
foldr-map {ℓ}{A}{x :: xs} rewrite sym (foldr-map {ℓ}{A}{xs}) = refl

invert𝕃 : ∀{ℓ}{A : Set ℓ}{t : A}{ts : 𝕃 A} → t :: ts ≢ []
invert𝕃 ()

length-repeat : ∀{ℓ}{A : Set ℓ} (n : ℕ) (a : A) → length (repeat n a) ≡ n
length-repeat 0 a = refl
length-repeat (suc n) a rewrite length-repeat n a = refl

map-repeat : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}(n : ℕ)(a : A)(f : A → B) → map f (repeat n a) ≡ repeat n (f a)
map-repeat 0 a f = refl
map-repeat (suc x) a f rewrite map-repeat x a f = refl

length-map : ∀{ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B)(l : 𝕃 A) → length (map f l) ≡ length l
length-map f [] = refl
length-map f (head :: tail) rewrite length-map f tail = refl

length-reverse-helper : ∀{ℓ}{A : Set ℓ}(h l : 𝕃 A) →
                      length (reverse-helper h l) ≡ length h + length l
length-reverse-helper h [] rewrite +0 (length h) = refl
length-reverse-helper h (x :: xs) rewrite length-reverse-helper (x :: h) xs = sym (+suc (length h) (length xs))

length-reverse : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → length (reverse l) ≡ length l
length-reverse l = length-reverse-helper [] l

reverse-++h : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → reverse-helper l1 l2 ≡ reverse-helper [] l2 ++ l1
reverse-++h l1 [] = refl
reverse-++h l1 (x :: xs) rewrite reverse-++h (x :: l1) xs | reverse-++h (x :: []) xs | ++-assoc (reverse xs) (x :: []) l1 = refl

reverse-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → reverse(l1 ++ l2) ≡ reverse(l2) ++ reverse(l1)
reverse-++ [] l2 rewrite ++[] (reverse l2) = refl
reverse-++ (x :: xs) l2 rewrite reverse-++h (x :: []) (xs ++ l2) | reverse-++ xs l2 | ++-assoc (reverse l2) (reverse xs) (x :: []) | sym (reverse-++h (x :: []) xs) = refl

reverse-involution-aux : ∀{ℓ}{A : Set ℓ}(h h' l : 𝕃 A) → reverse-helper h (reverse-helper h' l) ≡ (reverse-helper [] h') ++ l ++ h
reverse-involution-aux h h' [] = reverse-++h h h'
reverse-involution-aux h h' (x₁ :: l) rewrite reverse-involution-aux h (x₁ :: h') l | reverse-++h (x₁ :: []) h' | ++-assoc (reverse-helper [] h') (x₁ :: []) (l ++ h) = refl

reverse-involution : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → reverse (reverse l) ≡ l
reverse-involution l rewrite reverse-involution-aux [] [] l = ++[] l

reverse-++-bad : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → reverse-bad (l1 ++ l2) ≡ reverse-bad l2 ++ reverse-bad l1
reverse-++-bad [] l2 = sym (++[] (reverse-bad l2))
reverse-++-bad (x :: l1) l2 rewrite reverse-++-bad l1 l2 = ++-assoc (reverse-bad l2) (reverse-bad l1) (x :: [])

reverse-involution-bad : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → reverse-bad (reverse-bad l) ≡ l
reverse-involution-bad [] = refl
reverse-involution-bad (x :: xs) rewrite reverse-++-bad (reverse-bad xs) (x :: []) | reverse-involution-bad xs = refl

=𝕃-refl : ∀{ℓ}{A : Set ℓ}{l1 : 𝕃 A} → (eq : A → A → 𝔹) → ((x y : A) → x ≡ y → eq x y ≡ tt) → =𝕃 eq l1 l1 ≡ tt
=𝕃-refl{l1 = []} eq rise = refl
=𝕃-refl{l1 = x :: xs} eq rise = &&-combo (rise x x refl) (=𝕃-refl{l1 = xs} eq rise)

≡𝕃-from-= : ∀{ℓ}{A : Set ℓ}{l1 l2 : 𝕃 A} → (eq : A → A → 𝔹) → ((x y : A) → eq x y ≡ tt → x ≡ y) → =𝕃 eq l1 l2 ≡ tt → l1 ≡ l2
≡𝕃-from-={l1 = []}{[]} eq drop p = refl
≡𝕃-from-={l1 = x :: xs}{[]} eq drop ()
≡𝕃-from-={l1 = []}{y :: ys} eq drop ()
≡𝕃-from-={l1 = x :: xs}{y :: ys} eq drop p rewrite ≡𝕃-from-={l1 = xs} eq drop (&&-snd{eq x y}{=𝕃 eq xs ys} p) |  drop x y (&&-fst p) = refl

=𝕃-from-≡ : ∀{ℓ}{A : Set ℓ}{l1 l2 : 𝕃 A} → (eq : A → A → 𝔹) → ((x y : A) → x ≡ y → eq x y ≡ tt) → l1 ≡ l2  → =𝕃 eq l1 l2 ≡ tt
=𝕃-from-≡{l2 = l2} eq rise p rewrite p  = =𝕃-refl{l1 = l2} eq rise

multi++-assoc : ∀{ℓ}{A : Set ℓ} → (Ls : 𝕃 (𝕃 A)) → (l0 : 𝕃 A) → (foldr _++_ [] Ls) ++ l0 ≡ (foldr _++_ [] (Ls ++ [ l0 ]))
multi++-assoc [] l' rewrite ++[] l' = refl
multi++-assoc (l :: ls) l' rewrite ++-assoc l (foldr _++_ [] ls) l' | multi++-assoc ls l' = refl

concat-foldr : ∀{ℓ}{A : Set ℓ} → (ls : 𝕃 (𝕃 A)) → (l : 𝕃 A) → concat ls ++ l ≡ foldr _++_ l ls
concat-foldr [] l = refl
concat-foldr (l' :: ls) l rewrite ++-assoc l' (concat ls) l | concat-foldr ls l = refl

--concat-foldr (l' :: (l'' :: ls)) l rewrite ++-assoc l' (concat (l'' :: ls)) l | concat-foldr (l'' :: ls) l = refl

longer-trans : ∀{ℓ}{A : Set ℓ}(l1 l2 l3 : 𝕃 A) →
                l1 longer l2 ≡ tt →
                l2 longer l3 ≡ tt →
                l1 longer l3 ≡ tt
longer-trans [] l2 l3 () q
longer-trans (x :: l1) [] l3 p ()
longer-trans (x :: l1) (x₁ :: l2) [] p q = refl
longer-trans (x :: l1) (x₁ :: l2) (x₂ :: l3) p q = longer-trans l1 l2 l3 p q

filter-idem : ∀{ℓ}{A : Set ℓ}(p : A → 𝔹)(l : 𝕃 A) →
              (filter p (filter p l)) ≡ (filter p l)
filter-idem p [] = refl
filter-idem p (x :: l) with keep (p x)
filter-idem p (x :: l) | tt , p' rewrite p' | p' | filter-idem p l = refl
filter-idem p (x :: l) | ff , p' rewrite p' = filter-idem p l

length-filter : ∀{ℓ}{A : Set ℓ}(p : A → 𝔹)(l : 𝕃 A) →
                length (filter p l) ≤ length l ≡ tt
length-filter p [] = refl
length-filter p (x :: l) with p x
length-filter p (x :: l) | tt = length-filter p l
length-filter p (x :: l) | ff =
  ≤-trans{length (filter p l)} (length-filter p l) (≤-suc (length l))

filter-++ : ∀{ℓ}{A : Set ℓ}(p : A → 𝔹)(l1 l2 : 𝕃 A) → filter p (l1 ++ l2) ≡ filter p l1 ++ filter p l2
filter-++ p [] l2 = refl
filter-++ p (x :: l1) l2 with p x
filter-++ p (x :: l1) l2 | tt rewrite (filter-++ p l1 l2) = refl
filter-++ p (x :: l1) l2 | ff rewrite (filter-++ p l1 l2) = refl

remove-++ : ∀{ℓ}{A : Set ℓ}(eq : A → A → 𝔹)(a : A)(l1 l2 : 𝕃 A) →
            remove eq a (l1 ++ l2) ≡ remove eq a l1 ++ remove eq a l2
remove-++ eq a l1 l2 = filter-++ (λ x → ~ (eq a x)) l1 l2

::-injective : ∀{ℓ}{A : Set ℓ}{x y : A}{xs ys : 𝕃 A} →
               x :: xs ≡ y :: ys → x ≡ y ∧ xs ≡ ys
::-injective refl = refl , refl

concat-++ : ∀{ℓ}{A : Set ℓ}(ls1 ls2 : 𝕃 (𝕃 A)) → concat (ls1 ++ ls2) ≡ (concat ls1) ++ (concat ls2)
concat-++ [] ls2 = refl
concat-++ (l :: ls) ls2 rewrite concat-++ ls ls2 = sym (++-assoc l (concat ls) (concat ls2))

-- This holds as long as we have the equations p₁ and p₂.  We know
-- that these equations are consistant to adopt, because they are
-- equivalent up and an isomorphism, and hence, by univalence they are
-- consistent as equations.  The respective isomorphisms can be found
-- in products-thms.agda.
all-pred-append : ∀{X : Set}{f : X → Set}{l₁ l₂}
  → (p₁ : ∀{ℓ}{A : Set ℓ} → A ≡ ((⊤ {ℓ}) ∧ A))
  → (p₂ : ∀{ℓ}{A B C : Set ℓ} →  (A ∧ (B ∧ C)) ≡ ((A ∧ B) ∧ C))
  → all-pred f (l₁ ++ l₂) ≡ ((all-pred f l₁) ∧ (all-pred f l₂))
all-pred-append {l₁ = []} {l₂} p₁ p₂ = p₁
all-pred-append {X}{f}{x :: l₁} {l₂} p₁ p₂ rewrite all-pred-append {X}{f}{l₁ = l₁} {l₂} p₁ p₂ = p₂

all-pred-triv : {ℓ : Level}{l : 𝕃 (⊤ {ℓ})}(γ : ⊤ {ℓ} → Set ℓ)(p : γ triv) → all-pred γ l
all-pred-triv {_}{[]} γ p = triv
all-pred-triv {_}{triv :: l} γ p = p , all-pred-triv γ p

map-proj-⊎₁ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l : 𝕃 A) →
                proj-⊎₁ {A = A}{B} (map inj₁ l) ≡ l
map-proj-⊎₁ [] = refl
map-proj-⊎₁ {A = A}{B} (x :: l) rewrite map-proj-⊎₁ {A = A}{B} l = refl

map-proj-⊎₂ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l : 𝕃 B) →
                proj-⊎₂ {A = A}{B} (map inj₂ l) ≡ l
map-proj-⊎₂ [] = refl
map-proj-⊎₂ {A = A}{B} (x :: l) rewrite map-proj-⊎₂ {A = A}{B} l = refl

map-proj-⊎₂-[] : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l : 𝕃 A) →
                  proj-⊎₂ {A = A}{B} (map inj₁ l) ≡ []
map-proj-⊎₂-[] [] = refl
map-proj-⊎₂-[] {A = A}{B} (x :: l) rewrite map-proj-⊎₂-[] {A = A}{B} l = refl

map-proj-⊎₁-[] : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → (l : 𝕃 B) →
                  proj-⊎₁ {A = A}{B} (map inj₂ l) ≡ []
map-proj-⊎₁-[] [] = refl
map-proj-⊎₁-[] {A = A}{B} (x :: l) rewrite map-proj-⊎₁-[] {A = A}{B} l = refl

is-empty-++ : ∀{ℓ}{A : Set ℓ}(l1 l2 : 𝕃 A) → is-empty (l1 ++ l2) ≡ is-empty l1 && is-empty l2
is-empty-++ [] l2 = refl
is-empty-++ (x :: l1) l2 = refl

is-empty-ff-length : ∀{ℓ}{A : Set ℓ}(l : 𝕃 A) → is-empty l ≡ ff → length l =ℕ 0 ≡ ff
is-empty-ff-length [] ()
is-empty-ff-length (x :: l) p = refl

ext: agda

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise lifting of relations to vectors
------------------------------------------------------------------------

module Relation.Binary.Vec.Pointwise where

open import Category.Applicative.Indexed
open import Data.Fin
open import Data.Nat
open import Data.Plus as Plus hiding (equivalent; map)
open import Data.Vec as Vec hiding ([_]; head; tail; map)
import Data.Vec.Properties as VecProp
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv
  using (_⇔_; ⇔-setoid; module Equivalence)
import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec

-- Functional definition.

record Pointwise {ℓ} {A B : Set ℓ} (_∼_ : REL A B ℓ)
                 {n} (xs : Vec A n) (ys : Vec B n) : Set ℓ where
  constructor ext
  field app : ∀ i → lookup i xs ∼ lookup i ys

-- Inductive definition.

infixr 5 _∷_

data Pointwise′ {ℓ} {A B : Set ℓ} (_∼_ : REL A B ℓ) :
                ∀ {n} (xs : Vec A n) (ys : Vec B n) → Set ℓ where
  []  : Pointwise′ _∼_ [] []
  _∷_ : ∀ {n x y} {xs : Vec A n} {ys : Vec B n}
        (x∼y : x ∼ y) (xs∼ys : Pointwise′ _∼_ xs ys) →
        Pointwise′ _∼_ (x ∷ xs) (y ∷ ys)

-- The two definitions are equivalent.

equivalent : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n}
               {xs : Vec A n} {ys : Vec B n} →
             Pointwise _∼_ xs ys ⇔ Pointwise′ _∼_ xs ys
equivalent {A = A} {B} {_∼_} = Equiv.equivalence (to _ _) from
  where
  to : ∀ {n} (xs : Vec A n) (ys : Vec B n) →
       Pointwise _∼_ xs ys → Pointwise′ _∼_ xs ys
  to []       []       xs∼ys = []
  to (x ∷ xs) (y ∷ ys) xs∼ys =
    Pointwise.app xs∼ys zero ∷
    to xs ys (ext (Pointwise.app xs∼ys ∘ suc))

  nil : Pointwise _∼_ [] []
  nil = ext λ()

  cons : ∀ {n x y} {xs : Vec A n} {ys : Vec B n} →
         x ∼ y → Pointwise _∼_ xs ys → Pointwise _∼_ (x ∷ xs) (y ∷ ys)
  cons {x = x} {y} {xs} {ys} x∼y xs∼ys = ext helper
    where
    helper : ∀ i → lookup i (x ∷ xs) ∼ lookup i (y ∷ ys)
    helper zero    = x∼y
    helper (suc i) = Pointwise.app xs∼ys i

  from : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
         Pointwise′ _∼_ xs ys → Pointwise _∼_ xs ys
  from []            = nil
  from (x∼y ∷ xs∼ys) = cons x∼y (from xs∼ys)

-- Some destructors.

head : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n x y xs} {ys : Vec B n} →
       Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) → x ∼ y
head (x∼y ∷ xs∼ys) = x∼y

tail : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} {n x y xs} {ys : Vec B n} →
       Pointwise′ _∼_ (x ∷ xs) (y ∷ ys) → Pointwise′ _∼_ xs ys
tail (x∼y ∷ xs∼ys) = xs∼ys

-- Pointwise preserves reflexivity.

refl : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} →
       Reflexive _∼_ → Reflexive (Pointwise _∼_ {n = n})
refl rfl = ext (λ _ → rfl)

-- Pointwise preserves symmetry.

sym : ∀ {ℓ} {A B : Set ℓ} {P : REL A B ℓ} {Q : REL B A ℓ} {n} →
      Sym P Q → Sym (Pointwise P) (Pointwise Q {n = n})
sym sm xs∼ys = ext λ i → sm (Pointwise.app xs∼ys i)

-- Pointwise preserves transitivity.

trans : ∀ {ℓ} {A B C : Set ℓ}
          {P : REL A B ℓ} {Q : REL B C ℓ} {R : REL A C ℓ} {n} →
        Trans P Q R →
        Trans (Pointwise P) (Pointwise Q) (Pointwise R {n = n})
trans trns xs∼ys ys∼zs = ext λ i →
  trns (Pointwise.app xs∼ys i) (Pointwise.app ys∼zs i)

-- Pointwise preserves equivalences.

isEquivalence :
  ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} →
  IsEquivalence _∼_ → IsEquivalence (Pointwise _∼_ {n = n})
isEquivalence equiv = record
  { refl  = refl  (IsEquivalence.refl  equiv)
  ; sym   = sym   (IsEquivalence.sym   equiv)
  ; trans = trans (IsEquivalence.trans equiv)
  }

-- Pointwise preserves decidability.

decidable : ∀ {ℓ} {A B : Set ℓ} {_∼_ : REL A B ℓ} →
            Decidable _∼_ → ∀ {n} → Decidable (Pointwise _∼_ {n = n})
decidable {_∼_ = _∼_} dec xs ys =
  Dec.map (Setoid.sym (⇔-setoid _) equivalent) (decidable′ xs ys)
  where
  decidable′ : ∀ {n} → Decidable (Pointwise′ _∼_ {n = n})
  decidable′ []       []       = yes []
  decidable′ (x ∷ xs) (y ∷ ys) with dec x y
  ... | no ¬x∼y = no (¬x∼y ∘ head)
  ... | yes x∼y with decidable′ xs ys
  ...   | no ¬xs∼ys = no (¬xs∼ys ∘ tail)
  ...   | yes xs∼ys = yes (x∼y ∷ xs∼ys)

-- Pointwise _≡_ is equivalent to _≡_.

Pointwise-≡ : ∀ {ℓ} {A : Set ℓ} {n} {xs ys : Vec A n} →
              Pointwise _≡_ xs ys ⇔ xs ≡ ys
Pointwise-≡ {ℓ} {A} =
  Equiv.equivalence
    (to ∘ _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent))
    (λ xs≡ys → P.subst (Pointwise _≡_ _) xs≡ys (refl P.refl))
  where
  to : ∀ {n} {xs ys : Vec A n} → Pointwise′ _≡_ xs ys → xs ≡ ys
  to []               = P.refl
  to (P.refl ∷ xs∼ys) = P.cong (_∷_ _) $ to xs∼ys

-- Pointwise and Plus commute when the underlying relation is
-- reflexive.

⁺∙⇒∙⁺ : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} {xs ys : Vec A n} →
        Plus (Pointwise _∼_) xs ys → Pointwise (Plus _∼_) xs ys
⁺∙⇒∙⁺ [ ρ≈ρ′ ]             = ext (λ x → [ Pointwise.app ρ≈ρ′ x ])
⁺∙⇒∙⁺ (ρ ∼⁺⟨ ρ≈ρ′ ⟩ ρ′≈ρ″) =
  ext (λ x → _ ∼⁺⟨ Pointwise.app (⁺∙⇒∙⁺ ρ≈ρ′ ) x ⟩
                   Pointwise.app (⁺∙⇒∙⁺ ρ′≈ρ″) x)

∙⁺⇒⁺∙ : ∀ {ℓ} {A : Set ℓ} {_∼_ : Rel A ℓ} {n} {xs ys : Vec A n} →
        Reflexive _∼_ →
        Pointwise (Plus _∼_) xs ys → Plus (Pointwise _∼_) xs ys
∙⁺⇒⁺∙ {ℓ} {A} {_∼_} x∼x =
  Plus.map (_⟨$⟩_ {f₂ = ℓ} (Equivalence.from equivalent)) ∘
  helper ∘
  _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent)
  where
  helper : ∀ {n} {xs ys : Vec A n} →
           Pointwise′ (Plus _∼_) xs ys → Plus (Pointwise′ _∼_) xs ys
  helper []                                                  = [ [] ]
  helper (_∷_ {x = x} {y = y} {xs = xs} {ys = ys} x∼y xs∼ys) =
    x ∷ xs  ∼⁺⟨ Plus.map (λ x∼y   → x∼y ∷ xs∼xs) x∼y ⟩
    y ∷ xs  ∼⁺⟨ Plus.map (λ xs∼ys → x∼x ∷ xs∼ys) (helper xs∼ys) ⟩∎
    y ∷ ys  ∎
    where
    xs∼xs : Pointwise′ _∼_ xs xs
    xs∼xs = _⟨$⟩_ {f₂ = ℓ} (Equivalence.to equivalent) (refl x∼x)

-- Note that ∙⁺⇒⁺∙ cannot be defined if the requirement of reflexivity
-- is dropped.

private

 module Counterexample where

  data D : Set where
    i j x y z : D

  data _R_ : Rel D Level.zero where
    iRj : i R j
    xRy : x R y
    yRz : y R z

  xR⁺z : x [ _R_ ]⁺ z
  xR⁺z =
    x  ∼⁺⟨ [ xRy ] ⟩
    y  ∼⁺⟨ [ yRz ] ⟩∎
    z  ∎

  ix : Vec D 2
  ix = i ∷ x ∷ []

  jz : Vec D 2
  jz = j ∷ z ∷ []

  ix∙⁺jz : Pointwise′ (Plus _R_) ix jz
  ix∙⁺jz = [ iRj ] ∷ xR⁺z ∷ []

  ¬ix⁺∙jz : ¬ Plus′ (Pointwise′ _R_) ix jz
  ¬ix⁺∙jz [ iRj ∷ () ∷ [] ]
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ [ () ∷ yRz ∷ [] ])
  ¬ix⁺∙jz ((iRj ∷ xRy ∷ []) ∷ (() ∷ yRz ∷ []) ∷ _)

  counterexample :
    ¬ (∀ {n} {xs ys : Vec D n} →
         Pointwise (Plus _R_) xs ys →
         Plus (Pointwise _R_) xs ys)
  counterexample ∙⁺⇒⁺∙ =
    ¬ix⁺∙jz (Equivalence.to Plus.equivalent ⟨$⟩
               Plus.map (_⟨$⟩_ (Equivalence.to equivalent))
                 (∙⁺⇒⁺∙ (Equivalence.from equivalent ⟨$⟩ ix∙⁺jz)))

-- Map.

map : ∀ {ℓ} {A : Set ℓ} {_R_ _R′_ : Rel A ℓ} {n} →
      _R_ ⇒ _R′_ → Pointwise _R_ ⇒ Pointwise _R′_ {n}
map R⇒R′ xsRys = ext λ i →
  R⇒R′ (Pointwise.app xsRys i)

-- A variant.

gmap : ∀ {ℓ} {A A′ : Set ℓ}
         {_R_ : Rel A ℓ} {_R′_ : Rel A′ ℓ} {f : A → A′} {n} →
       _R_ =[ f ]⇒ _R′_ →
       Pointwise _R_ =[ Vec.map {n = n} f ]⇒ Pointwise _R′_
gmap {_R′_ = _R′_} {f} R⇒R′ {i = xs} {j = ys} xsRys = ext λ i →
  let module M = Morphism (VecProp.lookup-morphism i) in
  P.subst₂ _R′_ (P.sym $ M.op-<$> f xs)
                (P.sym $ M.op-<$> f ys)
                (R⇒R′ (Pointwise.app xsRys i))


text:
-- Andreas, 2017-01-26.  Testing the --no-eta-equality option.

-- Records in files without the option (unless Agda runs with this
-- option globally), should have eta.

module HaveEtaForImportedRecords.EtaRecord where

open import Agda.Builtin.Equality public

record ⊤ : Set where

private
  test : ∀{x y : ⊤} → x ≡ y
  test = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module _ where

open import Agda.Builtin.Nat

module Postulates where

  infixl 5 _<*>_

  postulate
    F     : Set → Set
    pure  : ∀ {A} → A → F A
    _<*>_ : ∀ {A B} → F (A → B) → F A → F B

  test₀ : F Nat → F Nat → F Nat
  test₀ a b = (| a + b |)

  test₁ : F Nat
  test₁ = (| 5 |)

  test₂ : F Nat → F Nat
  test₂ a = (| suc a |)

  test₃ : F Nat → F Nat
  test₃ a = (| (_+ 5) a |)

  -- Spaces are required! (Issue #2186)
  test₄ : Nat → Nat
  test₄ |n| = suc (|n| + |n|)

module Params {F : Set → Set}
              (pure : ∀ {A} → A → F A)
              (_<*>_ : ∀ {A B} → F (A → B) → F A → F B) where

  test₀ : F Nat → F Nat → F Nat
  test₀ a b = (| a + b |)

  test₁ : F Nat
  test₁ = (| 5 |)

  test₂ : F Nat → F Nat
  test₂ a = (| suc a |)

  test₃ : F Nat → F Nat
  test₃ a = (| (_+ 5) a |)

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
open import Data.Boolean
open import Type

module Data.List.Sorting.HeapSort {ℓ} {T : Type{ℓ}} (_≤?_ : T → T → Bool) where

import      Lvl
open import Data.List
import      Data.List.Functions as List
open import Data.BinaryTree
import      Data.BinaryTree.Heap as Heap
open import Functional using (_∘_)

heapSort : List(T) → List(T)
heapSort = Heap.foldOrdered(_≤?_)(_⊰_) ∅ ∘ List.foldᵣ(Heap.insert(_≤?_)) emptyTree

module Proofs where

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 Lemmachine.Default.Lemmas where
open import Lemmachine
import Lemmachine.Default
import Lemmachine.Lemmas
open Lemmachine.Lemmas Lemmachine.Default.resource
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Maybe
open import Data.Product hiding (map)
open import Data.Function using (const)
open import Data.List.Any hiding (any)

methodAlwaysKnown : ∀ r → any (eqMethod (method r))
                          (knownMethods r) ≡ true
methodAlwaysKnown r with method r
... | HEAD = refl
... | GET = refl
... | PUT = refl
... | DELETE = refl
... | POST = refl
... | TRACE = refl
... | CONNECT = refl
... | OPTIONS = refl

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2020-03-27, issue #3684
-- Warn about duplicate fields instead of hard error.

module DuplicateFields where

postulate X : Set

record D : Set where
  field x : X

d : X → X → D
d x y = record{ x = x; x = y }

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 14-image where

import 13-propositional-truncation
open 13-propositional-truncation public

{- We introduce the image inclusion of a map. -}

precomp-emb :
  { l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} (f : A → X)
  {B : UU l3} ( i : B ↪ X) (q : hom-slice f (map-emb i)) →
  {C : UU l4} ( j : C ↪ X) (r : hom-slice (map-emb i) (map-emb j)) →
  hom-slice f (map-emb j)
precomp-emb f i q j r =
  pair
    ( ( map-hom-slice (map-emb i) (map-emb j) r) ∘
      ( map-hom-slice f (map-emb i) q))
    ( ( triangle-hom-slice f (map-emb i) q) ∙h
      ( ( triangle-hom-slice (map-emb i) (map-emb j) r) ·r
        ( map-hom-slice f (map-emb i) q)))

is-prop-hom-slice :
  { l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) → is-prop (hom-slice f (map-emb i))
is-prop-hom-slice {X = X} f i =
  is-prop-is-equiv
    ( (x : X) → fib f x → fib (map-emb i) x)
    ( fiberwise-hom-hom-slice f (map-emb i))
    ( is-equiv-fiberwise-hom-hom-slice f (map-emb i))
    ( is-prop-Π
      ( λ x → is-prop-Π
        ( λ p → is-prop-map-is-emb (map-emb i) (is-emb-map-emb i) x)))

universal-property-image :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) → is-equiv (precomp-emb f i q j)

universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  UU (lsuc l ⊔ l1 ⊔ l2 ⊔ l3)
universal-property-image' l {X = X} f i q =
  ( C : UU l) (j : C ↪ X) →
    hom-slice f (map-emb j) → hom-slice (map-emb i) (map-emb j)

universal-property-image-universal-property-image' :
  ( l : Level) {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (f : A → X) →
  { B : UU l3} (i : B ↪ X) (q : hom-slice f (map-emb i)) →
  universal-property-image' l f i q → universal-property-image l f i q
universal-property-image-universal-property-image' l f i q up' C j =
  is-equiv-is-prop
    ( is-prop-hom-slice (map-emb i) j)
    ( is-prop-hom-slice f j)
    ( up' C j)

-- Section 13.4

is-small :
  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
is-small l A = Σ (UU l) (λ X → A ≃ X)

is-small-map :
  (l : Level) {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (A → B) → UU (lsuc l ⊔ (l1 ⊔ l2))
is-small-map l {B = B} f = (b : B) → is-small l (fib f b)

is-locally-small :
  (l : Level) {l1 : Level} (A : UU l1) → UU (lsuc l ⊔ l1)
is-locally-small l A = (x y : A) → is-small l (Id x y)

total-subtype :
  {l1 l2 : Level} {A : UU l1} (P : A → UU-Prop l2) → UU (l1 ⊔ l2)
total-subtype {A = A} P = Σ A (λ x → pr1 (P x))

equiv-subtype-equiv :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} {B : UU l2} (e : A ≃ B)
  (C : A → UU-Prop l3) (D : B → UU-Prop l4) →
  ((x : A) → (C x) ↔ (D (map-equiv e x))) →
  total-subtype C ≃ total-subtype D
equiv-subtype-equiv e C D H =
  equiv-toto (λ y → type-Prop (D y)) e
    ( λ x → equiv-iff (C x) (D (map-equiv e x)) (H x))

equiv-comp-equiv' :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} →
  (A ≃ B) → (C : UU l3) → (B ≃ C) ≃ (A ≃ C)
equiv-comp-equiv' e C =
  equiv-subtype-equiv
    ( equiv-precomp-equiv e C)
    ( is-equiv-Prop)
    ( is-equiv-Prop)
    ( λ g →
      pair
        ( is-equiv-comp' g (map-equiv e) (is-equiv-map-equiv e))
        ( λ is-equiv-eg →
          is-equiv-left-factor'
            g (map-equiv e) is-equiv-eg (is-equiv-map-equiv e)))

is-prop-is-small :
  (l : Level) {l1 : Level} (A : UU l1) → is-prop (is-small l A)
is-prop-is-small l A =
  is-prop-is-contr-if-inh
    ( λ Xe →
      is-contr-equiv'
        ( Σ (UU l) (λ Y → (pr1 Xe) ≃ Y))
        ( equiv-tot ((λ Y → equiv-comp-equiv' (pr2 Xe) Y)))
        ( is-contr-total-equiv (pr1 Xe)))

is-prop-is-locally-small :
  (l : Level) {l1 : Level} (A : UU l1) → is-prop (is-locally-small l A)
is-prop-is-locally-small l A =
  is-prop-Π (λ x → is-prop-Π (λ y → is-prop-is-small l (Id x y)))

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
module Builtin where

data Bool : Set where
  false : Bool
  true  : Bool

not : Bool -> Bool
not true = false
not false = true

_||_ : Bool -> Bool -> Bool
true  || _ = true
false || x = x

_&&_ : Bool -> Bool -> Bool
true  && x = x
false && _ = false

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

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

{-# BUILTIN NATURAL Nat  #-}

zero' : Nat
zero' = 0

one : Nat
one = 1

data Int : Set where
  pos : Nat → Int
  negsuc : Nat → Int

postulate
  String : Set
  Float  : Set
  Char   : Set

{-# BUILTIN INTEGER Int    #-}
{-# BUILTIN INTEGERPOS pos #-}
{-# BUILTIN INTEGERNEGSUC negsuc #-}
{-# BUILTIN STRING  String #-}
{-# BUILTIN FLOAT   Float  #-}
{-# BUILTIN CHAR    Char   #-}

infixr 10 _::_
data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST List   #-}
{-# BUILTIN NIL  nil    #-}
{-# BUILTIN CONS  _::_   #-}

primitive

  -- Integer functions
  primShowInteger     : Int -> String

    -- Floating point functions
  primNatToFloat     : Nat   -> Float
  primFloatPlus      : Float -> Float -> Float
  primFloatMinus     : Float -> Float -> Float
  primFloatTimes     : Float -> Float -> Float
  primFloatDiv       : Float -> Float -> Float
  primFloatLess      : Float -> Float -> Bool
  primFloatSqrt      : Float -> Float
  primRound          : Float -> Int
  primFloor          : Float -> Int
  primCeiling        : Float -> Int
  primExp            : Float -> Float
  primLog            : Float -> Float
  primSin            : Float -> Float
  primShowFloat      : Float -> String

    -- Character functions
  primCharEquality   : Char -> Char -> Bool
  primIsLower        : Char -> Bool
  primIsDigit        : Char -> Bool
  primIsAlpha        : Char -> Bool
  primIsSpace        : Char -> Bool
  primIsAscii        : Char -> Bool
  primIsLatin1       : Char -> Bool
  primIsPrint        : Char -> Bool
  primIsHexDigit     : Char -> Bool
  primToUpper        : Char -> Char
  primToLower        : Char -> Char
  primCharToNat      : Char -> Nat
  primNatToChar      : Nat  -> Char -- partial
  primShowChar       : Char -> String

    -- String functions
  primStringToList   : String -> List Char
  primStringFromList : List Char -> String
  primStringAppend   : String -> String -> String
  primStringEquality : String -> String -> Bool
  primShowString     : String -> String

isLower : Char -> Bool
isLower = primIsLower

isAlpha : Char -> Bool
isAlpha = primIsAlpha

isUpper : Char -> Bool
isUpper c = isAlpha c && not (isLower c)

infixl 14 _/_

nat0 = primCharToNat '\0'
int0 = pos nat0

_/_  = primFloatDiv

pi : Float
pi = 3.141592653589793

sin : Float -> Float
sin = primSin

cos : Float -> Float
cos x = sin (primFloatMinus (pi / 2.0) x)

tan : Float -> Float
tan x = sin x / cos x

reverse : {A : Set} -> List A -> List A
reverse xs = rev xs nil
  where
    rev : {A : Set} -> List A -> List A -> List A
    rev nil       ys = ys
    rev (x :: xs) ys = rev xs (x :: ys)

infixr 20 _∘_
_∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
f ∘ g = \x -> f (g x)

map : {A B : Set} -> (A -> B) -> List A -> List B
map f  nil      = nil
map f (x :: xs) = f x :: map f xs

stringAsList : (List Char -> List Char) -> String -> String
stringAsList f = primStringFromList ∘ f ∘ primStringToList

revStr : String -> String
revStr = stringAsList reverse

mapStr : (Char -> Char) -> String -> String
mapStr f = stringAsList (map f)

-- Testing unicode literals
uString = "åäö⊢ξ∀"
uChar   = '∀'

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

thm-show-pos : primShowInteger (pos 42) ≡ "42"
thm-show-pos = refl

thm-show-neg : primShowInteger (negsuc 41) ≡ "-42"
thm-show-neg = refl

thm-floor : primFloor 4.2 ≡ pos 4
thm-floor = refl

thm-ceiling : primCeiling -5.1 ≡ negsuc 4
thm-ceiling = refl


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)

-- 'Heterogeneous' identity morphism and some laws about them.

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

open import Level
open import Relation.Binary.PropositionalEquality

import Categories.Morphism as Morphism

open Category C
open Morphism C

-- If Agda was an extensional type theory, any pair of morphisms
--
--   f : A ⇒ B   and   g : A ⇒ C,
--
-- where `A ≡ B`, would belong to the same homset, even if `A` and `B`
-- are not definitionally equal.  In particular, the identity on `B`
-- could be given the type |id {B} : B ⇒ C|.
--
-- But Agda is an intensional type theory, so the identity cannot have
-- this type, in general.  Instead one needs to manually 'transport'
-- |id {B}| into the homset |B ⇒ C|.  Given |p : B ≡ C| one obtains
--
--   subst (B ⇒_) p (id {B})
--
-- Morphisms like thes are no longer identities (in the strict
-- sense) but they still enjoy many of the properties identities do.
--
-- To make this precise, this module introduces a notion of
-- 'heterogeneous identity', which is an identity morphism whose
-- domain and codomain are propositionally equal (but not necessarily
-- syntically equal).

-- A heterogeneous identity is just the transport of an identity
-- along a 'strict' equation of objects.

hid : ∀ {A B} (p : A ≡ B) → A ⇒ B
hid {A} p = subst (A ⇒_) p id

-- Lemmas about heterogeneous identities

hid-refl : ∀ {A : Obj} → hid refl ≈ id {A}
hid-refl = Equiv.refl

hid-trans : ∀ {A B C} (p : B ≡ C) (q : A ≡ B) →
            hid p ∘ hid q ≈ hid (trans q p)
hid-trans refl refl = identityˡ

hid-symˡ : ∀ {A B} (p : A ≡ B) → hid (sym p) ∘ hid p ≈ id {A}
hid-symˡ refl = identityˡ

hid-symʳ : ∀ {A B} (p : A ≡ B) → hid p ∘ hid (sym p) ≈ id {B}
hid-symʳ refl = identityˡ

hid-iso : ∀ {A B} (p : A ≡ B) → Iso (hid p) (hid (sym p))
hid-iso p = record { isoˡ = hid-symˡ p ; isoʳ = hid-symʳ p }

hid-cong : ∀ {A B} {p q : A ≡ B} → p ≡ q → hid p ≈ hid q
hid-cong refl = Equiv.refl

-- Transporting the domain/codomain is the same as
-- pre/post-composing with heterogeneous identity.

hid-subst-dom : ∀ {A B C} (p : A ≡ B) (f : B ⇒ C) →
                subst (_⇒ C) (sym p) f ≈ f ∘ hid p
hid-subst-dom refl f = Equiv.sym identityʳ

hid-subst-cod : ∀ {A B C} (f : A ⇒ B) (p : B ≡ C) →
                subst (A ⇒_) p f ≈ hid p ∘ f
hid-subst-cod f refl = Equiv.sym identityˡ

hid-subst₂ : ∀ {A B C D} (p : A ≡ B) (q : C ≡ D) (f : A ⇒ C) →
             subst₂ (_⇒_) p q f ≈ hid q ∘ f ∘ hid (sym p)
hid-subst₂ refl refl f = Equiv.sym (Equiv.trans identityˡ identityʳ)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


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

open import Oscar.Class
open import Oscar.Class.Smap
open import Oscar.Class.Transitivity
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Symmetry
open import Oscar.Class.Hmap
open import Oscar.Data.Proposequality
open import Oscar.Data.Substitunction
open import Oscar.Data.Term
open import Oscar.Prelude

module Test.ProblemWithDerivation-3 where

postulate
  A : Set
  B : Set
  _~A~_ : A → A → Set
  _~B~_ : B → B → Set
  s1 : A → B
  f1 : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y

instance

  𝓢urjectivity1 : Smap.class _~A~_ _~B~_ s1 s1
  𝓢urjectivity1 .⋆ _ _ = f1

module _ {𝔭} {𝔓 : Ø 𝔭} where

  open Substitunction 𝔓
  open Term 𝔓

test-1-before : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-1-before {x} {y} = smap

instance

  HmapFromTransleftidentitySymmetry : ∀
    {𝔵} {𝔛 : Ø 𝔵}
    {𝔞} {𝔄 : 𝔛 → Ø 𝔞}
    {𝔟} {𝔅 : 𝔛 → Ø 𝔟}
    (let _∼_ = Arrow 𝔄 𝔅)
    {ℓ̇} {_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ̇}
    {transitivity : Transitivity.type _∼_}
    {reflexivity : Reflexivity.type _∼_}
    {ℓ}
    ⦃ _ : Transleftidentity.class _∼_ _∼̇_ reflexivity transitivity ⦄
    ⦃ _ : ∀ {x y} → Symmetry.class (_∼̇_ {x} {y}) ⦄
    → ∀ {m n}
    → Hmap.class (λ (f : m ∼ n) (P : LeftExtensionṖroperty ℓ _∼_ _∼̇_ m) → π₀ (π₀ P) f)
                 (λ f P → π₀ (π₀ P) (transitivity f reflexivity))
  HmapFromTransleftidentitySymmetry .⋆ P₁ (π₂ , π₃) = π₃ $ symmetry transleftidentity

instance

    𝓣ransleftidentityExtension :
      ∀ {a} {A : Ø a} {b} {B : A → Ø b}
      → Transleftidentity.class (Extension B) _≡̇_ ¡ (flip _∘′_)
    𝓣ransleftidentityExtension .⋆ _ = ∅

    TransleftidentityFunction :
      ∀ {𝔬}
      → Transleftidentity.class Function⟦ 𝔬 ⟧ _≡̇_ ¡ (flip _∘′_)
    TransleftidentityFunction .⋆ _ = ∅

-- Oscar.Property.Setoid.Proposextensequality
module _ {𝔬} {𝔒 : Ø 𝔬} {𝔭} {𝔓 : 𝔒 → Ø 𝔭} where

  instance

    𝓢ymmetryProposextensequality : Symmetry.class Proposextensequality⟦ 𝔓 ⟧
    𝓢ymmetryProposextensequality .⋆ f₁≡̇f₂ x rewrite f₁≡̇f₂ x = ∅

test-1-after : ∀ {x y} → x ~A~ y → s1 x ~B~ s1 y
test-1-after {x} {y} = smap -- FIXME confusion somehow due to 𝓣ransleftidentityExtension, which is somewhat redundant (i.e. we don't need it as an instance given TransleftidentityFunction). needs explanation. -- FIXME ah ha! this is fixed by modification of Symmetry.class (or maybe is it b/c we don't have a Symmetry instance). -- FIXME we still need to see why this doesn't work when we use import Everything. -- FIXME answer is seen by adding `𝓢ymmetryProposextensequality`


text:
open import Level
open import Ordinals
module VL {n : Level } (O : Ordinals {n}) where

open import zf
open import logic
import OD
open import Relation.Nullary
open import Relation.Binary
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
import BAlgbra
open BAlgbra O
open inOrdinal O
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

open OD O
open OD.OD
open ODAxiom odAxiom
-- import ODC
open _∧_
open _∨_
open Bool
open HOD

-- The cumulative hierarchy
--    V 0 := ∅
--    V α + 1 := P ( V α )
--    V α := ⋃ { V β | β < α }

V : ( β : Ordinal ) → HOD
V β = TransFinite  V1 β where
   V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
   V1 x V0 with trio< x o∅
   V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
   V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
   V1 x V0 | tri> ¬a ¬b c with Oprev-p  x
   V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
   V1 x V0 | tri> ¬a ¬b c | no ¬p =
        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }

--
-- L ⊆ HOD ⊆ V
--
-- HOD=V : (x : HOD) → V (odmax x) ∋ x
-- HOD=V x = {!!}

--
-- Definition for Power Set
--
record Definitions  : Set (suc n) where
   field
      Definition : HOD → HOD

open Definitions

Df : Definitions → (x : HOD) → HOD
Df D x = Power x ∩ Definition D x

-- The constructible Sets
--    L 0 := ∅
--    L α + 1 := Df (L α)   -- Definable Power Set
--    V α := ⋃ { L β | β < α }

L : ( β : Ordinal ) → Definitions → HOD
L β D = TransFinite  L1 β where
   L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD )  → HOD
   L1 x L0 with trio< x o∅
   L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
   L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
   L1 x L0 | tri> ¬a ¬b c with Oprev-p  x
   L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x  p) <-osuc ))
   L1 x L0 | tri> ¬a ¬b c | no ¬p =
        record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) →  odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }

V=L0 : Set (suc n)
V=L0 = (x : Ordinal) → V x ≡  L x record { Definition = λ y → y }

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


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

-- Discrete Category.
-- https://ncatlab.org/nlab/show/discrete+category
-- says:
-- A category is discrete if it is both a groupoid and a preorder. That is,
-- every morphism should be invertible, any two parallel morphisms should be equal.
-- The idea is that in a discrete category, no two distinct (nonisomorphic) objects
-- are connectable by any path (morphism), and an object connects to itself only through
-- its identity morphism.

open import Level using (Level; suc; _⊔_)

open import Categories.Category using (Category)
open import Categories.Category.Groupoid using (IsGroupoid)

record IsDiscrete {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C using (Obj; _⇒_; _≈_)
  field
     isGroupoid : IsGroupoid C
     preorder : {A B : Obj} → (f g : A ⇒ B) → f ≈ g

record DiscreteCategory (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    category   : Category o ℓ e
    isDiscrete : IsDiscrete category

  open IsDiscrete isDiscrete public

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Issue417 where

data _≡_ (A : Set₁) : Set₁ → Set₂ where
  refl : A ≡ A

abstract

  A : Set₁
  A = Set

  unfold-A : A ≡ Set
  unfold-A = refl

-- The result of inferring the type of unfold-A is the following:
--
--   Set ≡ Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Mockingbird.Forest using (Forest)

module Mockingbird.Forest.Combination.Vec {b ℓ} (forest : Forest {b} {ℓ}) where

open import Mockingbird.Forest.Combination.Vec.Base forest public

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
module Serializer.Fin where

open import Data.Fin hiding (_+_)
open import Data.Nat
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; const)
open import Function.Bijection
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; setoid )

open import Serializer

instance
  serializerFin : ∀ {n} -> Serializer (Fin n)
  serializerFin {n} = record {
    size = n ;
    from = Function.id ;
    to = Function.id ;
    bijection = Function.Bijection.id }

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
module List where

open import Prelude
open import Star

[_] : Set -> Rel True
[ A ] = \_ _ -> A

List : Set -> Set
List A = Star [ A ] _ _

-- Actually there isn't really that much interesting stuff to be
-- done for lists that isn't generic.

{- Note that the "proofs" are the elements of the list. -}


text:
{-# OPTIONS --safe #-}
{-
This file has been split in two due to slow type checking
combined with insufficient reductions when the
experimental-lossy-unification flag is included.
Part 2: Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2

The goal of these two files is to show that
π₄(S³) ≅ π₃((S² × S²) ⊔ᴬ S²) where A = S² ∨ S².
This is proved in Brunerie (2016) using the James construction and
via (S² × S²) ⊔ᴬ S² ≃ J₂(S²).

In this file, we prove it directly using the encode-decode method. For
the statement of the isomorphism, see part 2.
-}
module Cubical.Homotopy.Group.Pi4S3.S3PushoutIso where

open import Cubical.Homotopy.Loopspace

open import Cubical.Homotopy.Group.Base
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism
open Iso
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Functions.Morphism

open import Cubical.HITs.SetTruncation
  renaming (rec to sRec ; rec2 to sRec2
          ; elim to sElim ; elim2 to sElim2 ; elim3 to sElim3
          ; map to sMap)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp renaming (toSusp to σ)
open import Cubical.HITs.S1 hiding (decode ; encode)

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Bool

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

open import Cubical.HITs.Join
open import Cubical.HITs.Pushout
open import Cubical.HITs.Wedge
open import Cubical.Homotopy.Freudenthal hiding (Code ; encode)
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Truncation renaming
  (rec to trRec ; elim to trElim ; elim2 to trElim2 ; map to trMap)
open import Cubical.Foundations.Function
open import Cubical.HITs.S2

Pushout⋁↪fold⋁ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ
Pushout⋁↪fold⋁ A = Pushout {A = A ⋁ A} ⋁↪ fold⋁

Pushout⋁↪fold⋁∙ : ∀ {ℓ} (A : Pointed ℓ) → Pointed ℓ
fst (Pushout⋁↪fold⋁∙ A) = Pushout⋁↪fold⋁ A
snd (Pushout⋁↪fold⋁∙ A) = inl (pt A , pt A)

-- The type of interest -- ''almost`` equivalent to ΩS³
Pushout⋁↪fold⋁S₊2 = Pushout {A = S₊∙ 2 ⋁ S₊∙ 2} ⋁↪ fold⋁
-- Same type, using base/surf definition of S² (easier to work with)
Pushout⋁↪fold⋁S² = Pushout⋁↪fold⋁ S²∙
-- Truncated version, to be proved equivalent to ∥ ΩS³ ∥₅
∥Pushout⋁↪fold⋁S²∥₅ = hLevelTrunc 5 Pushout⋁↪fold⋁S²

Ω∥S³∥₆ = Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ ∣ north ∣

-- Elimination into sets for Pushout⋁↪fold⋁S²
module _ {ℓ : Level} {P : Pushout⋁↪fold⋁S² → Type ℓ}
         (hlev : ((x : Pushout⋁↪fold⋁S²) → isSet (P x)))
         (b : P (inl (base , base))) where
  private
    ×fun : (x y : S²) → P (inl (x , y))
    ×fun = S²ToSetElim (λ _ → isSetΠ (λ _ → hlev _))
            (S²ToSetElim (λ _ → hlev _) b)

    inrfun : (x : S²) → P (inr x)
    inrfun = S²ToSetElim (λ _ → hlev _) (subst P (push (inl base)) b)

    inl-pp : (x : S²) → PathP (λ i → P (push (inl x) i)) (×fun x base) (inrfun x)
    inl-pp = S²ToSetElim (λ _ → isOfHLevelPathP 2 (hlev _) _ _)
              λ j → transp (λ i → P (push (inl base) (i ∧ j))) (~ j) b

    inr-pp : (x : S²) → PathP (λ i → P (push (inr x) i)) (×fun base x) (inrfun x)
    inr-pp = S²ToSetElim (λ _ → isOfHLevelPathP 2 (hlev _) _ _)
              (transport (λ j → PathP (λ i → P (push (push tt j) i)) (×fun base base)
                                       (inrfun base))
              (inl-pp base))

  Pushout⋁↪fold⋁S²→Set : (x : Pushout⋁↪fold⋁S²) → P x
  Pushout⋁↪fold⋁S²→Set (inl x) = ×fun (fst x) (snd x)
  Pushout⋁↪fold⋁S²→Set (inr x) = inrfun x
  Pushout⋁↪fold⋁S²→Set (push (inl x) i) = inl-pp x i
  Pushout⋁↪fold⋁S²→Set (push (inr x) i) = inr-pp x i
  Pushout⋁↪fold⋁S²→Set (push (push a j) i) = help j i
    where
    help : SquareP (λ j i → P (push (push tt j) i))
                   (λ i → inl-pp base i)
                   (λ i → inr-pp base i)
                   (λ _ → ×fun base base)
                   (λ _ → inrfun base)
    help = toPathP (isProp→PathP (λ _ → isOfHLevelPathP' 1 (hlev _) _ _) _ _)

{- A wedge connectivity lemma for Pushout⋁↪fold⋁S². It can be
stated for general dependent types, but it's easier to work with
in the special case of path types -}
module Pushout⋁↪fold⋁S²WedgeCon {ℓ : Level } {A : Type ℓ}
  (f g : Pushout⋁↪fold⋁S² → A)
  (h : isOfHLevel 5 A)
  (lp : (x : S²) → f (inl (x , base)) ≡ g (inl (x , base)))
  (rp : (x : S²) → f (inl (base , x)) ≡ g (inl (base , x)))
  (r≡l : (x : S²)
       → (sym (cong f (push (inl x))) ∙∙ lp x ∙∙ cong g (push (inl x)))
        ≡ (sym (cong f (push (inr x))) ∙∙ rp x ∙∙ cong g (push (inr x))))
  where
  btm-filler : I → I → I → A
  btm-filler k i j =
    hfill (λ k → λ {(i = i0)
                   → doubleCompPath-filler (sym (cong f (push (inl base))))
                                            (lp base)
                                            (cong g (push (inl base))) (~ k) j
                   ; (i = i1)
                   → doubleCompPath-filler (sym (cong f (push (inr base))))
                                            (rp base)
                                            (cong g (push (inr base))) (~ k) j
                   ; (j = i0) → f (push (push tt i) (~ k))
                   ; (j = i1) → g (push (push tt i) (~ k))})
      (inS (r≡l base i j))
      k

  lp-base≡rp-base : lp base ≡ rp base
  lp-base≡rp-base = (λ i j → btm-filler i1 i j)

  f∘inl≡g∘inl : (x y : S²) → f (inl (x , y)) ≡ g (inl (x , y))
  f∘inl≡g∘inl = wedgeconFunS² (λ _ _ → h _ _) lp rp lp-base≡rp-base

  f∘inl≡g∘inl-base : (x : S²) → f∘inl≡g∘inl x base ≡ lp x
  f∘inl≡g∘inl-base = wedgeconFunS²Id (λ _ _ → h _ _) lp rp lp-base≡rp-base

  f∘inr≡g∘inr : (x : S²) → f (inr x) ≡ g (inr x)
  f∘inr≡g∘inr x = cong f (sym (push (inl x))) ∙∙ lp x ∙∙ cong g (push (inl x))

  inlfill : (x : S²) → I → I → I → A
  inlfill x k i j =
    hfill (λ k → λ { (i = i0) → f∘inl≡g∘inl-base x (~ k) j
                    ; (i = i1) → doubleCompPath-filler
                                   (cong f (sym (push (inl x))))
                                   (lp x)
                                   (cong g (push (inl x))) k j
                    ; (j = i0) → f (push (inl x) (i ∧ k))
                    ; (j = i1) → g (push (inl x) (i ∧ k))})
          (inS (lp x j))
          k

  inrfill : (x : S²) → I → I → I → A
  inrfill x k i j =
    hfill (λ k → λ { (i = i0) → doubleCompPath-filler
                                   (cong f (sym (push (inr x))))
                                   (rp x)
                                   (cong g (push (inr x))) (~ k) j
                    ; (i = i1) → f∘inr≡g∘inr x j
                    ; (j = i0) → f (push (inr x) (i ∨ ~ k))
                    ; (j = i1) → g (push (inr x) (i ∨ ~ k))})
                      (inS (r≡l x (~ i) j))
                      k

  main : (x : Pushout⋁↪fold⋁S²) → f x ≡ g x
  main (inl x) = f∘inl≡g∘inl (fst x) (snd x)
  main (inr x) = f∘inr≡g∘inr x
  main (push (inl x) i) j = inlfill x i1 i j
  main (push (inr x) i) j = inrfill x i1 i j
  main (push (push a i) j) k =
    hcomp (λ r → λ {(i = i0) → inlfill base i1 j k
                   ; (i = i1) → inrfill-side r j k
                   ; (j = i0) → rp base k
                   ; (j = i1) → r≡l base (~ r ∧ i) k
                   ; (k = i0) → f (push (push a i) j)
                   ; (k = i1) → g (push (push a i) j)})
      (hcomp (λ r → λ {(i = i0) → inlfill base r j k
                   ; (i = i1) → doubleCompPath-filler
                                  (cong f (sym (push (inr base))))
                                  (rp base)
                                  (cong g (push (inr base))) (j ∧ r) k
                   ; (j = i0) → lp-base≡rp-base (r ∨ i) k
                   ; (j = i1) → inlfill-side r i k
                   ; (k = i0) → f (push (push a i) (j ∧ r))
                   ; (k = i1) → g (push (push a i) (j ∧ r))})
              (lp-base≡rp-base i k))
    where
    inlfill-side : I → I → I → A
    inlfill-side r i k =
      hcomp (λ j → λ { (r = i0) → btm-filler j i k
                      ; (r = i1) → r≡l base i k
                      ; (i = i0) → doubleCompPath-filler
                                  (cong f (sym (push (inl base))))
                                  (lp base)
                                  (cong g (push (inl base))) (r ∨ ~ j) k
                      ; (i = i1) → doubleCompPath-filler
                                  (cong f (sym (push (inr base))))
                                  (rp base)
                                  (cong g (push (inr base))) (r ∨ ~ j) k
                      ; (k = i0) → f (push (push a i) (r ∨ ~ j))
                      ; (k = i1) → g (push (push a i) (r ∨ ~ j))})
            (r≡l base i k)

    inrfill-side : I → I → I → A
    inrfill-side r j k =
      hcomp (λ i → λ { (r = i0)
                       → (doubleCompPath-filler
                           (cong f (sym (push (inr base))))
                           (rp base)
                           (cong g (push (inr base)))) (j ∨ ~ i)  k
                      ; (r = i1) → inrfill base i j k
                      ; (j = i0) → inrfill base i i0 k
                      ; (j = i1) → r≡l base (~ r) k
                      ; (k = i0) → f (push (inr base) (j ∨ ~ i))
                      ; (k = i1) → g (push (inr base) (j ∨ ~ i))})
            (r≡l base (~ r ∨ ~ j) k)

{-
Goal: Prove Ω ∥ SuspS² ∥₆ ≃ ∥ Pushout⋁↪fold⋁S² ∥₅
This will by done via the encode-decode method. For this, we nede a family
of equivalences ∥ Pushout⋁↪fold⋁S² ∥₅ ≃ ∥ Pushout⋁↪fold⋁S² ∥₅, indexed by S².
In order to define this, we need the following cubes/coherences in
∥ Pushout⋁↪fold⋁S² ∥₅:
-}

→Ω²∥Pushout⋁↪fold⋁S²∥₅ : (x y : S²)
  → Square {A = ∥Pushout⋁↪fold⋁S²∥₅} (λ _ → ∣ inl (x , y) ∣ₕ)
                            (λ _ → ∣ inl (x , y) ∣ₕ)
                            (λ _ → ∣ inl (x , y) ∣ₕ)
                            (λ _ → ∣ inl (x , y) ∣ₕ)
→Ω²∥Pushout⋁↪fold⋁S²∥₅ =
  wedgeconFunS²
    (λ _ _ → isOfHLevelPath 4 (isOfHLevelTrunc 5 _ _) _ _)
    (λ x → λ i j → ∣ inl (x , surf i j) ∣ₕ)
    (λ x → λ i j → ∣ inl (surf i j , x) ∣ₕ)
    λ r i j → ∣ hcomp (λ k → λ { (i = i0) → push (push tt (~ r)) (~ k)
                               ; (i = i1) → push (push tt (~ r)) (~ k)
                               ; (j = i1) → push (push tt (~ r)) (~ k)
                               ; (j = i0) → push (push tt (~ r)) (~ k)
                               ; (r = i0) → push (inr (surf i j)) (~ k)
                               ; (r = i1) → push (inl (surf i j)) (~ k)})
                     (inr (surf i j)) ∣ₕ

→Ω²∥Pushout⋁↪fold⋁S²∥₅Id : (x : S²)
  → →Ω²∥Pushout⋁↪fold⋁S²∥₅ x base ≡  λ i j → ∣ inl (x , surf i j) ∣ₕ
→Ω²∥Pushout⋁↪fold⋁S²∥₅Id =
  wedgeconFunS²Id
    (λ _ _ → isOfHLevelPath 4 (isOfHLevelTrunc 5 _ _) _ _)
    (λ x → λ i j → ∣ inl (x , surf i j) ∣ₕ)
    (λ x → λ i j → ∣ inl (surf i j , x) ∣ₕ)
    λ r i j → ∣ hcomp (λ k → λ { (i = i0) → push (push tt (~ r)) (~ k)
                               ; (i = i1) → push (push tt (~ r)) (~ k)
                               ; (j = i1) → push (push tt (~ r)) (~ k)
                               ; (j = i0) → push (push tt (~ r)) (~ k)
                               ; (r = i0) → push (inr (surf i j)) (~ k)
                               ; (r = i1) → push (inl (surf i j)) (~ k)})
                     (inr (surf i j)) ∣ₕ

push-inl∙push-inr⁻ : (y : S²) → Path Pushout⋁↪fold⋁S² (inl (y , base)) (inl (base , y))
push-inl∙push-inr⁻ y i = (push (inl y) ∙ sym (push (inr y))) i

push-inl∙push-inr⁻∙ : push-inl∙push-inr⁻ base ≡ refl
push-inl∙push-inr⁻∙ =
    (λ k i → (push (inl base) ∙ sym (push (push tt (~ k)))) i)
  ∙ rCancel (push (inl base))

push-inl∙push-inr⁻-filler : I → I → I → I → Pushout⋁↪fold⋁S²
push-inl∙push-inr⁻-filler r i j k =
  hfill (λ r → λ { (i = i0) → push-inl∙push-inr⁻∙ (~ r) k
                  ; (i = i1) → push-inl∙push-inr⁻∙ (~ r) k
                  ; (j = i0) → push-inl∙push-inr⁻∙ (~ r) k
                  ; (j = i1) → push-inl∙push-inr⁻∙ (~ r) k
                  ; (k = i0) → inl (surf i j , base)
                  ; (k = i1) → inl (surf i j , base)})
        (inS (inl (surf i j , base)))
        r

push-inl∙push-inr⁻-hLevFiller : (y : S²)
        → Cube {A = ∥Pushout⋁↪fold⋁S²∥₅}
                (λ j k → ∣ push-inl∙push-inr⁻ y k ∣)
                (λ j k → ∣ push-inl∙push-inr⁻ y k ∣)
                (λ j k → ∣ push-inl∙push-inr⁻ y k ∣)
                (λ j k → ∣ push-inl∙push-inr⁻ y k ∣)
                (→Ω²∥Pushout⋁↪fold⋁S²∥₅ y (pt (S² , base)))
                λ i j → ∣ inl (surf i j , y) ∣
push-inl∙push-inr⁻-hLevFiller =
  S²ToSetElim (λ _ → isOfHLevelPathP' 2
              (isOfHLevelPathP' 3
                (isOfHLevelPathP' 4 (isOfHLevelTrunc 5) _ _) _ _) _ _)
   λ i j k → ∣ push-inl∙push-inr⁻-filler i1 i j k ∣ₕ

{-
We combine the above definitions. The equivalence
∥Pushout⋁↪fold⋁S²∥₅ ≃ ∥Pushout⋁↪fold⋁S²∥₅ (w.r.t. S²) is induced
by the following function
-}
S²→Pushout⋁↪fold⋁S²↺' : (x : S²) → Pushout⋁↪fold⋁S² → ∥Pushout⋁↪fold⋁S²∥₅
S²→Pushout⋁↪fold⋁S²↺' base (inl (x , y)) = ∣ inl (x , y) ∣
S²→Pushout⋁↪fold⋁S²↺' (surf i j) (inl (x , y)) = →Ω²∥Pushout⋁↪fold⋁S²∥₅ x y i j
S²→Pushout⋁↪fold⋁S²↺' base (inr z) = ∣ inl (base , z) ∣ₕ
S²→Pushout⋁↪fold⋁S²↺' (surf i i₁) (inr z) = ∣ inl (surf i i₁ , z) ∣ₕ
S²→Pushout⋁↪fold⋁S²↺' base (push (inl y) k) =
  ∣ (push (inl y) ∙ sym (push (inr y))) k ∣
S²→Pushout⋁↪fold⋁S²↺' (surf i j) (push (inl y) k) =
  push-inl∙push-inr⁻-hLevFiller y i j k
S²→Pushout⋁↪fold⋁S²↺' base (push (inr y) i) = ∣ inl (base , y) ∣
S²→Pushout⋁↪fold⋁S²↺' (surf i j) (push (inr y) k) = ∣ inl (surf i j , y) ∣
S²→Pushout⋁↪fold⋁S²↺' base (push (push a i₁) i) = ∣ push-inl∙push-inr⁻∙ i₁ i ∣
S²→Pushout⋁↪fold⋁S²↺' (surf i j) (push (push a k) l) =
  ∣ hcomp (λ r → λ { (i = i0) → push-inl∙push-inr⁻∙ (k ∨ ~ r) l
                   ; (i = i1) → push-inl∙push-inr⁻∙ (k ∨ ~ r) l
                   ; (j = i0) → push-inl∙push-inr⁻∙ (k ∨ ~ r) l
                   ; (j = i1) → push-inl∙push-inr⁻∙ (k ∨ ~ r) l
                   ; (k = i0) → push-inl∙push-inr⁻-filler r i j l
                   ; (k = i1) → inl (surf i j , base)
                   ; (l = i0) → inl (surf i j , base)
                   ; (l = i1) → inl (surf i j , base)})
         (inl (surf i j , base)) ∣ₕ

{- For easier treatment later, we state its inverse explicitly -}
S²→Pushout⋁↪fold⋁S²↺'⁻ : (x : S²) → Pushout⋁↪fold⋁S² → ∥Pushout⋁↪fold⋁S²∥₅
S²→Pushout⋁↪fold⋁S²↺'⁻ base y = S²→Pushout⋁↪fold⋁S²↺' base y
S²→Pushout⋁↪fold⋁S²↺'⁻ (surf i j) y = S²→Pushout⋁↪fold⋁S²↺' (surf (~ i) j) y

S²→Pushout⋁↪fold⋁S²↺'≡idfun : (x : _) → S²→Pushout⋁↪fold⋁S²↺' base x ≡ ∣ x ∣
S²→Pushout⋁↪fold⋁S²↺'≡idfun (inl x) = refl
S²→Pushout⋁↪fold⋁S²↺'≡idfun (inr x) = cong ∣_∣ₕ (push (inr x))
S²→Pushout⋁↪fold⋁S²↺'≡idfun (push (inl x) i) j =
  ∣ compPath-filler (push (inl x)) (λ i₁ → push (inr x) (~ i₁)) (~ j) i  ∣ₕ
S²→Pushout⋁↪fold⋁S²↺'≡idfun (push (inr x) i) j = ∣ push (inr x) (j ∧ i) ∣
S²→Pushout⋁↪fold⋁S²↺'≡idfun (push (push a i) j) k =
  ∣ coh-lem {A = Pushout⋁↪fold⋁S²}
    (push (inl base)) (push (inr base)) (λ k → push (push tt k)) i j k ∣ₕ
  where
  coh-lem : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ y) (r : p ≡ q)
       → Cube {A = A}
               (λ j k → compPath-filler p (sym q) (~ k) j) (λ k j → q (k ∧ j))
               (λ i k → x) (λ i k → q k)
               (((λ k → p ∙ sym (r (~ k))) ∙ rCancel p))
               r
  coh-lem {A = A} {x = x} {y = y} =
    J (λ y p → (q : x ≡ y) (r : p ≡ q)
             → Cube {A = A}
                     (λ j k → compPath-filler p (sym q) (~ k) j) (λ k j → q (k ∧ j))
                     (λ i k → x) (λ i k → q k)
                     (((λ k → p ∙ sym (r (~ k))) ∙ rCancel p))
                     r)
      λ q → J (λ q r → Cube (λ j k → compPath-filler refl (λ i → q (~ i)) (~ k) j)
                              (λ k j → q (k ∧ j)) (λ i k → x) (λ i k → q k)
                              ((λ k → refl ∙ (λ i → r (~ k) (~ i))) ∙ rCancel refl) r)
               ((λ z j k → lUnit (sym (rUnit (λ _ → x))) z k j)
               ◁ (λ i j k → (refl ∙ (λ i₁ → rUnit (λ _ → x) (~ i₁))) (k ∨ i) j))

S²→Pushout⋁↪fold⋁S²↺ : (x : S²) → ∥Pushout⋁↪fold⋁S²∥₅ → ∥Pushout⋁↪fold⋁S²∥₅
S²→Pushout⋁↪fold⋁S²↺ x = trRec (isOfHLevelTrunc 5) (S²→Pushout⋁↪fold⋁S²↺' x)

isEq-S²→Pushout⋁↪fold⋁S²↺' : (x : _) → isEquiv (S²→Pushout⋁↪fold⋁S²↺ x)
isEq-S²→Pushout⋁↪fold⋁S²↺' =
  S²ToSetElim (λ _ → isProp→isSet (isPropIsEquiv _))
    (subst isEquiv (funExt id≡) (idIsEquiv _))
  where
  id≡ : (x : _) → x ≡ S²→Pushout⋁↪fold⋁S²↺ base x
  id≡ = trElim (λ _ → isOfHLevelPath 5 (isOfHLevelTrunc 5) _ _)
               (sym ∘ S²→Pushout⋁↪fold⋁S²↺'≡idfun)

S²→Pushout⋁↪fold⋁S²↺⁻¹ : (x : S²) → ∥Pushout⋁↪fold⋁S²∥₅ → ∥Pushout⋁↪fold⋁S²∥₅
S²→Pushout⋁↪fold⋁S²↺⁻¹ x = trRec (isOfHLevelTrunc 5) (S²→Pushout⋁↪fold⋁S²↺'⁻ x)

{- S²→Pushout⋁↪fold⋁S²↺⁻¹ is a section of S²→Pushout⋁↪fold⋁S²↺ -}
secS²→Pushout⋁↪fold⋁S²↺ : (x : S²) (y : ∥Pushout⋁↪fold⋁S²∥₅)
  → S²→Pushout⋁↪fold⋁S²↺ x (S²→Pushout⋁↪fold⋁S²↺⁻¹ x y) ≡ y
secS²→Pushout⋁↪fold⋁S²↺ x =
  trElim (λ _ → isOfHLevelPath 5 (isOfHLevelTrunc 5) _ _)
         (h x)
  where
  h : (x : S²) (a : Pushout⋁↪fold⋁S²)
    → S²→Pushout⋁↪fold⋁S²↺ x
        (S²→Pushout⋁↪fold⋁S²↺⁻¹ x ∣ a ∣) ≡ ∣ a ∣
  h base a = cong (S²→Pushout⋁↪fold⋁S²↺ base)
                  (S²→Pushout⋁↪fold⋁S²↺'≡idfun a)
           ∙ S²→Pushout⋁↪fold⋁S²↺'≡idfun a
  h (surf i j) a k = main a k i j
    where
    side : (a : Pushout⋁↪fold⋁S²) → _
    side a = cong (S²→Pushout⋁↪fold⋁S²↺ base) (S²→Pushout⋁↪fold⋁S²↺'≡idfun a)
          ∙ S²→Pushout⋁↪fold⋁S²↺'≡idfun a

    refl-b : Path ∥Pushout⋁↪fold⋁S²∥₅ _ _
    refl-b = (refl {x = ∣ inl (base , base) ∣ₕ})

    main : (a : Pushout⋁↪fold⋁S²)
      → Cube (λ i j → S²→Pushout⋁↪fold⋁S²↺ (surf i j)
                 (S²→Pushout⋁↪fold⋁S²↺⁻¹ (surf i j) ∣ a ∣))
              (λ _ _ → ∣ a ∣)
              (λ i _ → side a i) (λ i _ → side a i)
              (λ i _ → side a i) (λ i _ → side a i)
    main =
      Pushout⋁↪fold⋁S²→Set (λ _ → isOfHLevelPathP' 2
                  (isOfHLevelPathP' 3 (isOfHLevelTrunc 5 _ _) _ _) _ _)
       λ k i j →
         hcomp (λ r → λ { (i = i0) → rUnit refl-b r k
                         ; (i = i1) → rUnit refl-b r k
                         ; (j = i0) → rUnit refl-b r k
                         ; (j = i1) → rUnit refl-b r k
                         ; (k = i0) → →Ω²∥Pushout⋁↪fold⋁S²∥₅Id
                                        (surf (~ i) j) (~ r) i j
                         ; (k = i1) → μ base base})
               (μ-coh k i j)
      where
      μ : (x y : S²) → ∥Pushout⋁↪fold⋁S²∥₅
      μ x y = ∣ inl (x , y) ∣ₕ

      μUnit : (x : S²) → μ x base ≡ μ base x
      μUnit base = refl
      μUnit (surf i j) k = ∣
        hcomp (λ r → λ {(i = i0) → push (push tt k) (~ r)
                       ; (i = i1) → push (push tt k) (~ r)
                       ; (j = i0) → push (push tt k) (~ r)
                       ; (j = i1) → push (push tt k) (~ r)
                       ; (k = i0) → push (inl (surf i j)) (~ r)
                       ; (k = i1) → push (inr (surf i j)) (~ r)})
               (inr (surf i j)) ∣ₕ

      μ-coh : Path (Square {A = ∥Pushout⋁↪fold⋁S²∥₅}
             (λ _ → ∣ inl (base , base) ∣) (λ _ → ∣ inl (base , base) ∣)
             (λ _ → ∣ inl (base , base) ∣) (λ _ → ∣ inl (base , base) ∣))
             (λ i j → ∣ inl (surf (~ i) j , surf i j) ∣ₕ)
             refl
      μ-coh =
            (cong₂Funct (λ (x y : (Path S² base base)) → cong₂ μ x y) (sym surf) surf
           ∙ cong (_∙ cong (cong (μ base)) surf) (λ i → cong (cong (λ x → μUnit x i)) (sym surf))
           ∙ lCancel (cong (cong (μ base)) surf))

retrS²→Pushout⋁↪fold⋁S²↺ : (x : S²) (y : ∥Pushout⋁↪fold⋁S²∥₅)
  → S²→Pushout⋁↪fold⋁S²↺⁻¹ x (S²→Pushout⋁↪fold⋁S²↺ x y) ≡ y
retrS²→Pushout⋁↪fold⋁S²↺ x =
  trElim (λ _ → isOfHLevelPath 5 (isOfHLevelTrunc 5) _ _)
    (main x)
    where
    main : (x : S²) (a : Pushout⋁↪fold⋁S²)
      → S²→Pushout⋁↪fold⋁S²↺⁻¹ x (S²→Pushout⋁↪fold⋁S²↺ x ∣ a ∣) ≡ ∣ a ∣
    main base a = secS²→Pushout⋁↪fold⋁S²↺ base ∣ a ∣
    main (surf i j) a l = secS²→Pushout⋁↪fold⋁S²↺ (surf (~ i) j) ∣ a ∣ l

∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ : (x : S²)
  → Iso ∥Pushout⋁↪fold⋁S²∥₅ ∥Pushout⋁↪fold⋁S²∥₅
fun (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ x) = S²→Pushout⋁↪fold⋁S²↺ x
inv (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ x) = S²→Pushout⋁↪fold⋁S²↺⁻¹ x
rightInv (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ x) = secS²→Pushout⋁↪fold⋁S²↺ x
leftInv (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ x) = retrS²→Pushout⋁↪fold⋁S²↺ x

PreCode : (x : Susp S²) → Type
PreCode north = ∥Pushout⋁↪fold⋁S²∥₅
PreCode south = ∥Pushout⋁↪fold⋁S²∥₅
PreCode (merid a i) = isoToPath (∥Pushout⋁↪fold⋁S²∥₅≃∥Pushout⋁↪fold⋁S²∥₅ a) i

hLevPreCode : (x : Susp S²) → isOfHLevel 5 (PreCode x)
hLevPreCode =
  suspToPropElim base (λ _ → isPropIsOfHLevel 5) (isOfHLevelTrunc 5)

Code : (hLevelTrunc 6 (Susp S²)) → Type ℓ-zero
Code =
  fst ∘ trRec {B = TypeOfHLevel ℓ-zero 5} (isOfHLevelTypeOfHLevel 5)
    λ x → (PreCode x) , (hLevPreCode x)

private
  cong-coherence : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (r : refl ≡ p)
                  → cong (p ∙_) (sym r) ∙ sym (rUnit p)
                  ≡ cong (_∙ p) (sym r) ∙ sym (lUnit p)
  cong-coherence p = J (λ p r → cong (p ∙_) (sym r) ∙ sym (rUnit p)
                    ≡ cong (_∙ p) (sym r) ∙ sym (lUnit p)) refl

{- The function Pushout⋁↪fold⋁S² → Ω∥S³∥₆ will be the obvious one -}
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ : Pushout⋁↪fold⋁S² → Ω∥S³∥₆
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ (inl x) = cong ∣_∣ₕ (σ S²∙ (fst x) ∙ σ S²∙ (snd x))
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ (inr x) = cong ∣_∣ₕ (σ S²∙ x)
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ (push (inl x) i) j =
  ∣ (cong (σ S²∙ x ∙_) (rCancel (merid base)) ∙ sym (rUnit (σ S²∙ x))) i j ∣ₕ
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ (push (inr x) i) j =
  ∣ (cong (_∙ σ S²∙ x) (rCancel (merid base)) ∙ sym (lUnit (σ S²∙ x))) i j ∣ₕ
Pushout⋁↪fold⋁S²→Ω∥S³∥₆ (push (push a k) i) j =
  ∣ cong-coherence (σ S²∙ base) (sym (rCancel (merid base))) k i j ∣ₕ

{- Truncated version (the equivalence) -}
∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ : ∥Pushout⋁↪fold⋁S²∥₅ → Ω∥S³∥₆
∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ =
  trRec (isOfHLevelTrunc 6 _ _) Pushout⋁↪fold⋁S²→Ω∥S³∥₆

decode' : (x : Susp S²) → Code ∣ x ∣
      → Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ ∣ x ∣
decode' north p = ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ p
decode' south p = ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ p ∙ cong ∣_∣ₕ (merid base)
decode' (merid a i) = main a i
  where
  baseId : (x : Pushout⋁↪fold⋁S²)
     → ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ (S²→Pushout⋁↪fold⋁S²↺' base x)
      ≡ ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ ∣ x ∣
  baseId x =
    cong ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ (S²→Pushout⋁↪fold⋁S²↺'≡idfun x)

  mainLemma : (a : S²) (x : Pushout⋁↪fold⋁S²)
     → ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ (S²→Pushout⋁↪fold⋁S²↺'⁻ a x)
       ∙ (λ i → ∣ merid a i ∣)
     ≡ ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ ∣ x ∣ ∙ cong ∣_∣ₕ (merid base)
  mainLemma base x = cong (_∙ cong ∣_∣ₕ (merid base)) (baseId x)
  mainLemma (surf i j) x k = surf-filler x k i j
    where
    ∙ΩbaseId :
      (q : typ (Ω (Susp∙ (typ S²∙)))) → q ≡ q ∙ σ S²∙ base
    ∙ΩbaseId q = rUnit q ∙ cong (q ∙_) (sym (rCancel (merid base)))

    cubeCoherence :
      ∀ {ℓ} {A : Type ℓ} {x : A} {p : x ≡ x}
      → (refl ≡ p)
      → (q : Square {A = x ≡ x} (λ _ → p) (λ _ → p) (λ _ → p) (λ _ → p))
      → Cube {A = Path A x x}
              (λ i j → q i j ∙ q (~ i) j) (λ _ _ → p ∙ p)
              (λ k j → p ∙ p) (λ _ _ → p ∙ p)
              (λ _ _ → p ∙ p) λ _ _ → p ∙ p
    cubeCoherence {A = A} {x = x} {p = p} =
      J (λ p _ → (q : Square {A = x ≡ x}
                        (λ _ → p) (λ _ → p) (λ _ → p) (λ _ → p))
               → Cube {A = Path A x x}
                       (λ i j → q i j ∙ q (~ i) j) (λ _ _ → p ∙ p)
                       (λ k j → p ∙ p) (λ _ _ → p ∙ p)
                       (λ _ _ → p ∙ p) λ _ _ → p ∙ p)
      (λ q →
        (cong₂Funct (λ (x y : Path (x ≡ x) refl refl) → cong₂ _∙_ x y) q (sym q)
      ∙ transport
         (λ i → cong (λ (p : (refl {x = x}) ≡ refl) k → rUnit (p k) i) q
               ∙ cong (λ (p : (refl {x = x}) ≡ refl) k → lUnit (p k) i) (sym q)
               ≡ refl {x = refl {x = lUnit (refl {x = x}) i}})
         (rCancel q)))

    surf-side : (i j r l : I) → hLevelTrunc 6 (Susp S²)
    surf-side i j r l =
      ((cong ∣_∣ₕ (∙ΩbaseId (σ S²∙ (surf (~ i) j)) r))
      ∙ cong ∣_∣ₕ (compPath-filler (merid (surf i j))
                  (sym (merid base)) (~ r))) l

    side : (r l : I) → hLevelTrunc 6 (Susp S²)
    side r l =
      ((cong ∣_∣ₕ (∙ΩbaseId (σ S²∙ base) r))
      ∙ cong ∣_∣ₕ (compPath-filler (merid base)
                  (sym (merid base)) (~ r))) l

    surf-filler : (x : Pushout⋁↪fold⋁S²)
      → Cube {A = Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ ∣ south ∣}
              (λ i j → ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆
                         (S²→Pushout⋁↪fold⋁S²↺' (surf (~ i) j) x)
                       ∙ (λ k → ∣ merid (surf i j) k ∣))
              (λ _ _ → ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ ∣ x ∣
                      ∙ cong ∣_∣ₕ (merid base))
              (λ k j → baseId x k ∙ (λ i₂ → ∣ merid base i₂ ∣))
              (λ k j → baseId x k ∙ (λ i₂ → ∣ merid base i₂ ∣))
              (λ k i → baseId x k ∙ (λ i₂ → ∣ merid base i₂ ∣))
              (λ k i → baseId x k ∙ (λ i₂ → ∣ merid base i₂ ∣))
    surf-filler =
      Pushout⋁↪fold⋁S²→Set
       (λ _ → isOfHLevelPathP' 2
        (isOfHLevelPathP' 3 (isOfHLevelTrunc 6 _ _ _ _) _ _) _ _)
         (λ k i j l → hcomp (λ r
           → λ {(i = i0) → surf-side i0 i0 r l
               ; (i = i1) → surf-side i0 i0 r l
               ; (j = i0) → surf-side i0 i0 r l
               ; (j = i1) → surf-side i0 i0 r l
               ; (k = i0) → surf-side i j r l
               ; (k = i1) → surf-side i0 i0 r l
               ; (l = i0) → ∣ north ∣ₕ
               ; (l = i1) → ∣ merid base r ∣ₕ})
      (cubeCoherence {p = cong ∣_∣ₕ (σ (S²∙) base)}
        (cong (cong ∣_∣ₕ) (sym (rCancel (merid base))))
        (λ i j k → ∣ σ S²∙ (surf (~ i) j) k ∣ₕ) k i j l))

  main : (a : S²)
    → PathP (λ i → Code ∣ merid a i ∣
                  → Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ ∣ merid a i ∣)
                        ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆
                        λ x → ∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆ x
                             ∙ cong ∣_∣ₕ (merid base)
  main a =
    toPathP (funExt
      (trElim (λ _ → isOfHLevelSuc 4 (isOfHLevelTrunc 6 _ _ _ _))
       (λ x
      → (λ j → transp (λ i → Path
                 (hLevelTrunc 6 (Susp S²)) ∣ north ∣ ∣ merid a (i ∨ j) ∣) j
                  (compPath-filler
                   (∥Pushout⋁↪fold⋁S²∥₅→Ω∥S³∥₆
                    (S²→Pushout⋁↪fold⋁S²↺'⁻ a (transportRefl x j)))
                     (cong ∣_∣ₕ (merid a)) j))
      ∙ mainLemma a x)))

decode : (x : hLevelTrunc 6 (Susp S²))
  → Code x → Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ x
decode =
  trElim (λ _ → isOfHLevelΠ 6 λ _ → isOfHLevelPath 6 (isOfHLevelTrunc 6) _ _)
         decode'

decode∙ : decode ∣ north ∣ ∣ inl (base , base) ∣ ≡ refl
decode∙ =
  cong (cong ∣_∣ₕ) (cong (λ x → x ∙ x) (rCancel (merid base)) ∙ sym (rUnit refl))

encode : (x : hLevelTrunc 6 (Susp S²))
  → Path (hLevelTrunc 6 (Susp S²)) ∣ north ∣ x → Code x
encode x p = subst Code p ∣ inl (base , base) ∣

encode-decode : (x : hLevelTrunc 6 (Susp S²))
  → (p : ∣ north ∣ ≡ x) → decode x (encode x p) ≡ p
encode-decode x = J (λ x p → decode x (encode x p) ≡ p)
              (cong (decode ∣ north ∣) (transportRefl ∣ inl (base , base) ∣ₕ)
             ∙ decode∙)

decode-encode : (p : Code ∣ north ∣) → encode ∣ north ∣ (decode ∣ north ∣ p) ≡ p
decode-encode =
  trElim (λ _ → isOfHLevelPath 5 (isOfHLevelTrunc 5) _ _)
    (Pushout⋁↪fold⋁S²WedgeCon.main ((λ a → encode ∣ north ∣ (decode ∣ north ∣ ∣ a ∣))) ∣_∣ₕ
      (isOfHLevelTrunc 5)
      (λ x → cong (encode ∣ north ∣) (cong (cong ∣_∣ₕ) (cong (σ S²∙ x ∙_)
               (rCancel (merid base)) ∙ sym (rUnit (σ S²∙ x))))
             ∙ surf-filler x)
      (λ x → (cong (encode ∣ north ∣) (cong (cong ∣_∣ₕ) (cong (_∙ σ S²∙ x)
               (rCancel (merid base)) ∙ sym (lUnit (σ S²∙ x))))
             ∙ surf-filler x
             ∙ cong ∣_∣ₕ (push (inl x)) ∙ cong ∣_∣ₕ (sym (push (inr x)))))
      λ x → lem (encode ∣ north ∣)
                (cong (decode ∣ north ∣) (cong ∣_∣ₕ (push (inl x))))
                ((cong (decode ∣ north ∣) (cong ∣_∣ₕ (push (inr x)))))
                (surf-filler x) (cong ∣_∣ₕ (push (inl x))) (cong ∣_∣ₕ (sym (push (inr x)))))
  where
  subber = transport (λ j → Code ∣ merid base (~ j) ∣ₕ)

  lem : ∀ {ℓ} {A B : Type ℓ} {x x' y : A} {l w u : B}
       (f : A → B) (p : x ≡ y) (p' : x' ≡ y) (q : f y ≡ l)
       (r : l ≡ w) (r' : w ≡ u)
     → cong f (sym p) ∙∙ cong f p ∙ q ∙∙ r
     ≡ (cong f (sym p') ∙∙ (cong f p' ∙ q ∙ (r ∙ r')) ∙∙ sym r')
  lem {x = x} {x' = x'} {y = y'} {l = l} {w = w} {u = u} f p p' q r r' =
      (λ i → (λ j → f (p (~ j ∨ i))) ∙∙ (λ j → f (p (j ∨ i))) ∙ q ∙∙ r)
   ∙∙ (λ i → (λ j → f (p' (~ j ∨ ~ i))) ∙∙ (λ j → f (p' (j ∨ ~ i)))
            ∙ compPath-filler q r i ∙∙ λ j → r (i ∨ j))
   ∙∙ λ i → cong f (sym p') ∙∙ cong f p' ∙ q
            ∙ compPath-filler r r' i ∙∙ λ j → r' (~ j ∧ i)

  mainId : (x : S²)
    → (S²→Pushout⋁↪fold⋁S²↺' x (inl (base , base))) ≡ ∣ inl (x , base) ∣ₕ
  mainId base = refl
  mainId (surf i i₁) = refl

  surf-filler : (x : S²)
    → encode ∣ north ∣ (λ i → ∣ σ S²∙ x i ∣) ≡ ∣ inl (x , base) ∣
  surf-filler x =
       (λ i → transp (λ j →  Code (∣ merid base (i ∧ ~ j) ∣ₕ)) (~ i)
                   (encode ∣ merid base i ∣
                    λ j → ∣ compPath-filler
                             (merid x) (sym (merid base)) (~ i) j ∣ₕ))
     ∙ cong subber
        (transportRefl (S²→Pushout⋁↪fold⋁S²↺' x (inl (base , base)))
       ∙ mainId x)

IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅ :
  Iso (hLevelTrunc 5 (typ (Ω (Susp∙ S²))))
      (hLevelTrunc 5 Pushout⋁↪fold⋁S²)
IsoΩ∥SuspS²∥₅∥Pushout⋁↪fold⋁S²∥₅ =
  compIso (invIso (PathIdTruncIso _)) is
  where
  is : Iso _ _
  fun is = encode ∣ north ∣
  inv is = decode ∣ north ∣
  rightInv is = decode-encode
  leftInv is = encode-decode ∣ north ∣

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Construction.Properties.EilenbergMoore where

open import Level
import Relation.Binary.PropositionalEquality as ≡

open import Categories.Adjoint
open import Categories.Adjoint.Properties
open import Categories.Category
open import Categories.Functor using (Functor; _∘F_)
open import Categories.Functor.Equivalence
open import Categories.Monad

open import Categories.NaturalTransformation renaming (id to idN)
open import Categories.Morphism.HeterogeneousIdentity

open import Categories.Adjoint.Construction.EilenbergMoore
open import Categories.Category.Construction.EilenbergMoore

private
  variable
    o ℓ e : Level
    𝒞 𝒟 : Category o ℓ e

module _ {F : Functor 𝒞 𝒟} {G : Functor 𝒟 𝒞} (F⊣G : Adjoint F G) where
  private
    T : Monad 𝒞
    T = adjoint⇒monad F⊣G

    𝒞ᵀ : Category _ _ _
    𝒞ᵀ = EilenbergMoore T

    module 𝒞 = Category 𝒞
    module 𝒟 = Category 𝒟
    module 𝒞ᵀ = Category 𝒞ᵀ

    open 𝒞.HomReasoning

    module T = Monad T
    module F = Functor F
    module G = Functor G

    open Adjoint F⊣G
    open NaturalTransformation

  -- Maclane's Comparison Functor
  ComparisonF : Functor 𝒟 𝒞ᵀ
  ComparisonF = record
    { F₀ = λ X → record
      { A = G.F₀ X
      ; action = G.F₁ (counit.η X)
      ; commute = commute (G ∘ˡ counit) (counit.η X)
      ; identity = zag
      }
    ; F₁ = λ {A} {B} f → record
      { arr = G.F₁ f
      ; commute =  begin
        𝒞 [ G.F₁ f ∘ G.F₁ (counit.η A) ]               ≈˘⟨ G.homomorphism ⟩
        G.F₁ (𝒟 [ f ∘ (counit.η A) ])                  ≈˘⟨ G.F-resp-≈ (counit.commute f) ⟩
        G.F₁ (𝒟 [ counit.η B ∘ F.F₁ (G.F₁ f) ])        ≈⟨ G.homomorphism  ⟩
        𝒞 [ G.F₁ (counit.η B) ∘ G.F₁ (F.F₁ (G.F₁ f)) ] ∎
      }
    ; identity = G.identity
    ; homomorphism = G.homomorphism
    ; F-resp-≈ = G.F-resp-≈
    }

  private
    K = ComparisonF
    module K = Functor K
    module Gᵀ = Functor (Forgetful T)
    module Fᵀ = Functor (Free T)

  Comparison∘F≡Free : (ComparisonF ∘F F) ≡F Free T
  Comparison∘F≡Free = record
    { eq₀ = λ X → ≡.refl
    ; eq₁ = λ {A} {B} f → begin
      Module⇒.arr (𝒞ᵀ [ (hid 𝒞ᵀ ≡.refl) ∘ K.F₁ (F.F₁ f) ]) ≈⟨ hid-refl 𝒞ᵀ {A = K.F₀ (F.F₀ B)} ⟩∘⟨refl ⟩
      Module⇒.arr (𝒞ᵀ [ 𝒞ᵀ.id ∘ K.F₁ (F.F₁ f) ])           ≈⟨ 𝒞.identityˡ {f = Module⇒.arr (K.F₁ (F.F₁ f))} ⟩
      Module⇒.arr (K.F₁ (F.F₁ f))                           ≈⟨ refl ⟩
      Module⇒.arr (Fᵀ.F₁ f)                                 ≈˘⟨ 𝒞ᵀ.identityʳ {f = Fᵀ.F₁ f} ⟩
      Module⇒.arr (𝒞ᵀ [ Fᵀ.F₁ f ∘ 𝒞ᵀ.id ])                 ≈˘⟨ refl⟩∘⟨ hid-refl 𝒞ᵀ {A = Fᵀ.F₀ A} ⟩
      Module⇒.arr (𝒞ᵀ [ Fᵀ.F₁ f ∘ (hid 𝒞ᵀ ≡.refl) ])       ∎
    }

  Forgetful∘ComparisonF≡G : (Forgetful T ∘F ComparisonF) ≡F G
  Forgetful∘ComparisonF≡G = record
    { eq₀ = λ X → ≡.refl
    ; eq₁ = λ f → begin
      𝒞 [ (hid 𝒞 ≡.refl) ∘ (Gᵀ.F₁ (K.F₁ f)) ] ≈⟨ hid-refl 𝒞 ⟩∘⟨refl ⟩
      𝒞 [ 𝒞.id ∘ (Gᵀ.F₁ (K.F₁ f)) ]           ≈⟨ 𝒞.identityˡ ⟩
      (Gᵀ.F₁ (K.F₁ f))                         ≈⟨ refl ⟩
      G.F₁ f                                   ≈˘⟨ 𝒞.identityʳ ⟩
      𝒞 [ G.F₁ f ∘ 𝒞.id ]                     ≈˘⟨ refl⟩∘⟨ hid-refl 𝒞 ⟩
      𝒞 [ G.F₁ f ∘ (hid 𝒞 ≡.refl) ]           ∎
    }


text:
{-# OPTIONS --without-K #-}
module overloading.bundle where

open import level

record Bundle {i j} {Base : Set i}
                    (Struct : Base → Set j) : Set (lsuc (i ⊔ j)) where
  constructor bundle
  field
    parent : Base
    struct : Struct parent

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.FromToInit {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

from-to-l-g : (c : A₀₂) → ap (from ∘ to ∘ left) (glue c) == ap left (glue c)
from-to-l-g c =
  ap (from ∘ i₀∙) (glue c)
       =⟨ ap-∘ from i₀∙ (glue c) ⟩
  ap from (ap i₀∙ (glue c))
       =⟨ I₀∙.glue-β c |in-ctx ap from ⟩
  ap from (glue (left c))
       =⟨ From.glue-β (left c) ⟩
  ap left (glue c) ∎

module FromToL = PushoutElim {d = span _ _ _ f₀₁ f₀₃} {P = λ a → from (to (left a)) == left a}
                 (λ a → idp) (λ b → idp) (λ c → ↓-='-in (! (from-to-l-g c)))

from-to-l : (a : A₀∙) → from (to (left a)) == left a
from-to-l = FromToL.f

from-to-r-g : (c : A₄₂) → ap (from ∘ to ∘ right) (glue c) == ap right (glue c)
from-to-r-g c =
  ap (from ∘ i₄∙) (glue c)
       =⟨ ap-∘ from i₄∙ (glue c) ⟩
  ap from (ap i₄∙ (glue c))
       =⟨ I₄∙.glue-β c |in-ctx ap from ⟩
  ap from (glue (right c))
       =⟨ From.glue-β (right c) ⟩
  ap right (glue c) ∎

module FromToR = PushoutElim {d = span _ _ _ f₄₁ f₄₃} {P = λ b → from (to (right b)) == right b}
                 (λ a → idp) (λ b → idp) (λ c → ↓-='-in (! (from-to-r-g c)))

from-to-r : (b : A₄∙) → from (to (right b)) == right b
from-to-r = FromToR.f

from-to-g-l : (a : A₂₀) → glue (left a) == ap from (ap to (glue (left a)))
from-to-g-l a =
  glue (left a)
       =⟨ ! (I∙₀.glue-β a) ⟩
  ap i∙₀ (glue a)
       =⟨ ap-∘ from left (glue a) ⟩
  ap from (ap left (glue a))
       =⟨ ! (To.glue-β (left a)) |in-ctx ap from ⟩
  ap from (ap to (glue (left a))) ∎

from-to-g-r : (b : A₂₄) → glue (right b) == ap from (ap to (glue (right b)))
from-to-g-r b =
  glue (right b)
       =⟨ ! (I∙₄.glue-β b) ⟩
   ap i∙₄ (glue b)
        =⟨ ap-∘ from right (glue b) ⟩
   ap from (ap right (glue b))
        =⟨ ! (To.glue-β (right b)) |in-ctx ap from ⟩
   ap from (ap to (glue (right b))) ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue4260 where

open import Issue4260.M

--  syntax F X = G X

H : Set → Set
H X = G X


text:
module plfa-code.Negation where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import plfa-code.Isomorphism using (_≃_; extensionality)

¬_ : Set → Set
¬ A = A → ⊥

¬-elim : ∀ {A : Set}
  → ¬ A
  → A
    ---
  → ⊥
¬-elim ¬x x = ¬x x

infix 3 ¬_

¬¬-intro : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
¬¬-intro x  =  λ ¬x → ¬x x

¬¬-intro′ : ∀ {A : Set}
  → A
    -----
  → ¬ ¬ A
¬¬-intro′ x ¬x = ¬x x

¬¬¬-elim : ∀ {A : Set}
  → ¬ ¬ ¬ A
    -------
  → ¬ A
¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)

contraposition : ∀ {A B : Set}
  → (A → B)
    ------------
  → (¬ B → ¬ A)
contraposition f ¬y x = ¬y (f x)

_≢_ : ∀ {A : Set} → A → A → Set
x ≢ y  =  ¬ (x ≡ y)

_ : 1 ≢ 2
_ = λ ()

peano : ∀ {m : ℕ} → zero ≢ suc m
peano = λ ()

id : ⊥ → ⊥
id x = x

id′ : ⊥ → ⊥
id′ ()

id≡id′ : id ≡ id′
id≡id′ = extensionality (λ ())

assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
assimilation ¬x ¬x′ = extensionality (λ x → ⊥-elim (¬x′ x))

open Data.Nat using (_<_; _≤_; z≤n; s≤s)
open Relation.Binary.PropositionalEquality using (cong)
open import Function
open Data.Product using (proj₁; proj₂)

---------- practice ----------

<-irreflexive : ∀ {n : ℕ} → ¬ (n < n)
<-irreflexive {suc n} (s≤s n<n) = <-irreflexive n<n

data Trichotomy (m n : ℕ) : Set where
  less    : m < n → ¬ (n < m) → ¬ (m ≡ n) → Trichotomy m n
  greater : n < m → ¬ (m ≡ n) → ¬ (m < n) → Trichotomy m n
  equal   : m ≡ n → ¬ (m < n) → ¬ (n < m) → Trichotomy m n

inv-< : ∀ {m n} → suc m < suc n → m < n
inv-< (s≤s sm<sn) = sm<sn

inv-≡ : ∀ {m n} → suc m ≡ suc n → m ≡ n
inv-≡ refl = refl

<-trichotomy : ∀ (m n : ℕ) → Trichotomy m n
<-trichotomy zero    zero    = equal refl      (λ ()) (λ ())
<-trichotomy zero    (suc n) = less  (s≤s z≤n) (λ ()) (λ ())
<-trichotomy (suc m) zero    = greater (s≤s z≤n) (λ ()) (λ ())
<-trichotomy (suc m) (suc n) with <-trichotomy m n
... | less    m<n ¬n<m ¬m≡n = less       (s≤s m<n) (¬n<m ∘ inv-<) (¬m≡n ∘ inv-≡)
... | greater n<m ¬m≡n ¬m<n = greater    (s≤s n<m) (¬m≡n ∘ inv-≡) (¬m<n ∘ inv-<)
... | equal   m≡n ¬m<n ¬n<m = equal (cong suc m≡n) (¬m<n ∘ inv-<) (¬n<m ∘ inv-<)

⊎-dual-× : ∀ (A B : Set) → ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
⊎-dual-× A B =
  record
  { to      = λ ¬-A⊎B → ⟨ (¬-A⊎B ∘ inj₁) , (¬-A⊎B ∘ inj₂) ⟩
  ; from    = λ{ ¬A×¬B (inj₁ a) → proj₁ ¬A×¬B a
               ; ¬A×¬B (inj₂ b) → proj₂ ¬A×¬B b
               }
  ; from∘to = λ{x → assimilation _ x}
  ; to∘from = λ{ ⟨ ¬a , ¬b ⟩ → refl}
  }

-- ¬ (A × B) ≃ (¬ A) ⊎ (¬ B) does not hold, but we could say:
⊎¬-implies-¬× : ∀ (A B : Set) → (¬ A) ⊎ (¬ B) → ¬ (A × B)
⊎¬-implies-¬× A B (inj₁ ¬a) = λ ab → ¬a (proj₁ ab)
⊎¬-implies-¬× A B (inj₂ ¬b) = λ ab → ¬b (proj₂ ab)

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

em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
em-irrefutable k = k (inj₂ (λ x → k (inj₁ x)))

---------- practice ----------
-- to prove the implying relations among a group of
-- proposition P₀ P₁ P₂ ... Pₙ, we just need prove P₀ → P₁,
-- P₁ → P₂, ..., Pₙ₋₁ → Pₙ, Pₙ → P₀.

P₀ = ∀ {A : Set} → A ⊎ ¬ A
P₁ = ∀ {A : Set} → (¬ ¬ A → A)
P₂ = ∀ {A B : Set} → ((A → B) → A) → A
P₃ = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
P₄ = ∀ {A B : Set} → ¬ (¬ A × ¬ B) → A ⊎ B

P₀⇒P₁ : P₀ → P₁
P₀⇒P₁ p₀ {A} ¬¬a with p₀ {A}
...                 | inj₁ a  = a
...                 | inj₂ ¬a = ⊥-elim (¬¬a ¬a)

P₁⇒P₂ : P₁ → P₂
P₁⇒P₂ p₁ x = p₁ $ λ ¬a → (¬a $ x $ p₁ ∘ const ∘ ¬a)

P₂⇒P₃ : P₂ → P₃
P₂⇒P₃ p₂ {A} {B} f = p₂ {¬ A ⊎ B} {⊥} (λ z → inj₁ (z ∘ inj₂ ∘ f))

--- the prove 'P₃⇒P₄'  below referenced https://github.com/googleson78/plfa

P₃⇒P₀ : P₃ → P₀
P₃⇒P₀ p₃ {A} with p₃ Function.id
...        | inj₁ ¬x = inj₂ ¬x
...        | inj₂  x = inj₁ x

P₁⇒P₄ : P₁ → P₄
P₁⇒P₄ p₁ {A} {B} ¬x = p₁ (λ ¬y → ¬x ⟨ ¬y ∘ inj₁ , ¬y ∘ inj₂ ⟩)

P₃⇒P₄ : P₃ → P₄
P₃⇒P₄ = P₁⇒P₄ ∘ P₀⇒P₁ ∘ P₃⇒P₀

P₄⇒P₀ : P₄ → P₀
P₄⇒P₀ p₄ {A} = p₄ {A} {¬ A} $ proj₂ ˢ proj₁

Stable : Set → Set
Stable A = ¬ ¬ A → A

¬⇒stable : ∀ {A : Set} → ¬ A → Stable (¬ A)
¬⇒stable ¬a = ¬¬¬-elim

×⇒stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
×⇒stable a b = λ x → ⟨ (a $ λ z → x (z ∘ proj₁)) , (b $ λ z → x (z ∘ proj₂)) ⟩

max_stars_repo_name: chirsz-ever/plfa-code

max_issues_repo_name: chirsz-ever/plfa-code

max_forks_repo_name: chirsz-ever/plfa-code


text:
{-# OPTIONS -Werror -WnoEmptyRewritePragma #-}

{-# REWRITE #-}


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

module hott-i where

import 04-inductive-types
open 04-inductive-types public

data 𝕀 : UU lzero where
  left : 𝕀

postulate right : 𝕀

data Path {l : Level} (A : 𝕀 → UU l) : (a : A left) (a' : A right) → UU l where
  pcon : (f : (x : 𝕀) → A x) → Path A (f left) (f right)

apply-path :
  {l : Level} (A : 𝕀 → UU l) (a : A left) (a' : A right) →
  Path A a a' → (x : 𝕀) → A x
apply-path A .(f left) .(f right) (pcon f) x = f x

refl-path :
  {l : Level} (A : UU l) (a : A) → Path (λ x → A) a a
refl-path A a = pcon (λ x → a)

apply-path-pcon :
  {l : Level} (A : 𝕀 → UU l) (f : (x : 𝕀) → A x) →
  (x : 𝕀) → Path (λ y → A x) (apply-path A (f left) (f right) (pcon f) x) (f x)
apply-path-pcon A f x = refl-path (A x) (f x)

left-apply-path :
  {l : Level} (A : 𝕀 → UU l) (a : A left) (a' : A right) (p : Path A a a') →
  Path (λ y → A left) (apply-path A a a' p left) a
left-apply-path A .(f left) .(f right) (pcon f) = refl-path (A left) (f left)

right-apply-path :
  {l : Level} (A : 𝕀 → UU l) (a : A left) (a' : A right) (p : Path A a a') →
  Path (λ y → A right) (apply-path A a a' p right) a'
right-apply-path A .(f left) .(f right) (pcon f) = refl-path (A right) (f right)

free-transport-path :
  {l : Level} (A : 𝕀 → UU l) → A left → (x : 𝕀) → A x
free-transport-path A a left = a

transport-path :
  {l : Level} (A : 𝕀 → UU l) → A left → A right
transport-path A a = free-transport-path A a right

elim-path-lemma :
  {l : Level} {A : UU l} (f : (x : 𝕀) → A) →
  (i : 𝕀) → Path (λ j → A) (f left) (f i)
elim-path-lemma {A = A} f left = refl-path A (f left)

elim-path :
  {l1 l2 : Level} (A : UU l1) (a : A)
  (B : (x : A) (p : Path (λ i → A) a x) → UU l2) →
  B a (refl-path A a) →
  (x : A) (p : Path (λ i → A) a x) → B x p
elim-path A .(f left) B b .(f right) (pcon f) =
  transport-path (λ i → B (f i) {!elim-path-lemma f i!}) b

concat-path :
  {l : Level} {A : UU l} {x y z : A} →
  Path (λ i → A) x y → Path (λ i → A) y z → Path (λ i → A) x z
concat-path {l} {A} {x} p (pcon f) =
  transport-path (λ i → Path (λ j → A) x (f i)) p

function-extensionality' :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} →
  (H : (x : A) → Path (λ i → B x) (f x) (g x)) →
  (i : 𝕀) (x : A) → B x
function-extensionality' {B = B} {f} {g} H i x =
  apply-path (λ j → B x) (f x) (g x) (H x) i

function-extensionality :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} →
  (H : (x : A) → Path (λ i → B x) (f x) (g x)) →
  Path (λ j → (x : A) → B x) f g
function-extensionality {l1} {l2} {A} {B} {f} {g} H =
  concat-path
    ( concat-path
      {!!}
      ( pcon (function-extensionality' H)))
    ( {!!})

{-
pcon-apply-path :
  {l : Level} (A : 𝕀 → UU l) (a : A left) (a' : A right) (p : Path A a a') →
  Path (λ y → Path A a a') (pcon (apply-path A a a' p)) ?
pcon-apply-path A a a' p = ?
-}

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

infix 2 _↔_
record _↔_ {a} {b} (p : Set a) (q : Set b) : Set (a ⊔ b) where
  field
    l2r : p → q
    r2l : q → p

_&_ : Bool → Bool → Bool
true & true = true
_ & _ = false

[_] : Bool → Set
[ P ] = P ≡ true

record ∃ {A : Set} (P : A → Bool) : Set where
  field
    {witness} : A
    proof : [ P witness ]

postulate
  U : Set
  set : Set
  subset : set → set → Bool
  int : set → set → set
  mem : ∀ {A : Set} → A → set → Bool
  mapsF : set → set → Bool
  F : ∀ {A B : Set} → A → B → Bool
  same : ∀ {A B : Set} → A → B → Bool
  equal : set → set → Bool
  invF : set → set → set
  subsetMembershipLaw : ∀ {A} {B} → [ subset A B ] ↔ (∀ {M : Set} {x : M} → [ mem x A ] → [ mem x B ])
--  mapsFLaw : ∀ {A} {B} → [ mapsF A B ] ↔ ((∀ {M : Set} {x : M} → [ mem x A ] → ∃ λ (y : M) → mem y B & F x y)

{-
Problem #758
same as problem 757 but rewritten with only expressions of first-order logic
Given premises:
     (all A)(all B)((subset A B) <-> (all x)((mem x A) -> (mem x B)))    justification = 1.0
     (all A)(all B)(some intAB)(IsInt A B intAB)    justification = 1.0
     (all A)(all B)(all intAB)((IsInt A B intAB) <-> (all x)((mem x intAB) <-> ((mem x A) & (mem x B))))    justification = 1.0
     (all A)(all B)((mapsF A B) <-> ((all x)((mem x A) -> (some y)((mem y B) & (F x y))) & (all x)(all y)(all z)(((mem x A) & ((mem y A) & (mem z A))) -> (((F x y) & (F x z)) -> (same y z)))))    justification = 1.0
     (all A)(all x)(all y)((same x y) -> ((mem x A) -> (mem y A)))    justification = 1.0
     (all x)(same x x)    justification = 1.0
     (all x)(all y)((same x y) <-> (same y x))    justification = 1.0
     (all x)(all y)(all z)(((same x y) & (same y z)) -> (same x z))    justification = 1.0
     (all A)(all B)((equal A B) <-> ((subset A B) & (subset B A)))    justification = 1.0
     (all A)(all B)(some invFBA)(IsInvF B A invFBA)    justification = 1.0
     (all A)(all B)(all invFBA)((IsInvF B A invFBA) <-> (all x)((mem x invFBA) <-> ((mem x A) & (some y)((mem y B) & (F x y)))))    justification = 1.0
Ultimate epistemic interests:
     (all A)(all B)(all X)(all Y)(((mapsF A B) & ((subset X B) & (subset Y B))) -> (some intXY)((IsInt X Y intXY) & (some invFIntXYA)((IsInvF intXY A invFIntXYA) & (some invFXA)((IsInvF X A invFXA) & (some invFYA)((IsInvF Y A invFYA) & (some intInvFXAInvFYA)((IsInt invFXA invFYA intInvFXAInvFYA) & (equal invFIntXYA intInvFXAInvFYA)))))))    interest = 1.0
-}