module Cubical.Categories.Displayed.Presheaf.Constructions.Quantifiers.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.More
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Dependent
open import Cubical.Foundations.Structure
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Isomorphism.More
open import Cubical.Data.Sigma
import Cubical.Data.Equality as Eq
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Profunctor.General
open import Cubical.Categories.Yoneda
open import Cubical.Categories.Constructions.Fiber
open import Cubical.Categories.Constructions.TotalCategory.Base as ∫
open import Cubical.Categories.Limits.BinProduct.More
open import Cubical.Categories.Presheaf.Base
open import Cubical.Categories.Presheaf.Morphism.Alt
open import Cubical.Categories.Presheaf.Representable
open import Cubical.Categories.Presheaf.Representable.More
open import Cubical.Categories.Presheaf.More
open import Cubical.Categories.Presheaf.Constructions
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.NaturalTransformation renaming (_∘ˡ_ to _∘ˡNT_)
open import Cubical.Categories.NaturalTransformation.More
open import Cubical.Categories.FunctorComprehension
open import Cubical.Categories.Displayed.Base
open import Cubical.Categories.Displayed.Instances.Sets.Base
open import Cubical.Categories.Displayed.Instances.Functor.Base
open import Cubical.Categories.Displayed.Functor
open import Cubical.Categories.Displayed.Profunctor
open import Cubical.Categories.Displayed.NaturalTransformation
open import Cubical.Categories.Displayed.NaturalTransformation.More
open import Cubical.Categories.Displayed.Functor.More
open import Cubical.Categories.Displayed.Adjoint.More
open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Base
open import Cubical.Categories.Displayed.Constructions.Reindex.Properties
open import Cubical.Categories.Displayed.Constructions.Reindex.Limits
open import Cubical.Categories.Displayed.Fibration.Base
open import Cubical.Categories.Displayed.Presheaf
open import Cubical.Categories.Displayed.Presheaf.Constructions.Reindex
open import Cubical.Categories.Displayed.Presheaf.Constructions.Quantifiers.Base
open import Cubical.Categories.Displayed.Presheaf.Constructions.Quantifiers.UniversalProperty
open import Cubical.Categories.Displayed.FunctorComprehension
import Cubical.Categories.Displayed.Presheaf.CartesianLift as PshᴰCL
private
variable
ℓC ℓC' ℓCᴰ ℓCᴰ' ℓ ℓ' ℓP ℓPᴰ ℓQ ℓQᴰ ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
open Functor
open Functorᴰ
open PshHom
open PshHomᴰ
open UniversalElement
open UniversalElementⱽ
-- TODO update to handle opaque reind
-- module _
-- {C : Category ℓC ℓC'}
-- {D : Category ℓD ℓD'}
-- {F : Functor C D}
-- {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
-- {c : C .Category.ob}
-- {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
-- (-×c : BinProductsWith C c)
-- (-×Fc : BinProductsWith D (F ⟅ c ⟆))
-- (F-× : preservesProvidedBinProductsWith F -×c)
-- where
-- private
-- module C = Category C
-- module D = Category D
-- module Cᴰ = Fibers Cᴰ
-- module Dᴰ = Fibers Dᴰ
-- F*Dᴰ = Base.reindex Dᴰ F
-- module F*Dᴰ = Fibers F*Dᴰ
-- module -×c = BinProductsWithNotation -×c
-- module -×Fc = BinProductsWithNotation -×Fc
-- module F⟨-×c⟩ {Γ} =
-- BinProductNotation
-- (preservesUniversalElement→UniversalElement
-- (preservesBinProdCones F Γ c) (-×c Γ) (F-× Γ))
-- module _ {Γ} {dᴰ : F*Dᴰ.ob[ Γ -×c.×a ]} where
-- module F⟨Γ×c⟩ =
-- BinProductNotation
-- (preservesUniversalElement→UniversalElement
-- (preservesBinProdCones F Γ c) (-×c Γ) (F-× Γ))
-- mapProdStr : ∀ {Γ} → D [ F ⟅ Γ -×c.×a ⟆ , F ⟅ Γ ⟆ -×Fc.×a ]
-- mapProdStr = F ⟪ -×c.π₁ ⟫ -×Fc.,p F ⟪ -×c.π₂ ⟫
-- mapProdStrPshHet : ∀ {Γ} →
-- PshHet F (C [-, Γ -×c.×a ]) (D [-, F ⟅ Γ ⟆ -×Fc.×a ])
-- mapProdStrPshHet = yoRec _ mapProdStr
-- prodStrNatTrans : NatTrans (F ∘F -×c.×aF) (-×Fc.×aF ∘F F)
-- prodStrNatTrans .NatTrans.N-ob _ = mapProdStr
-- prodStrNatTrans .NatTrans.N-hom f =
-- -×Fc.,p-extensionality
-- (D.⋆Assoc _ _ _
-- ∙ cong₂ D._⋆_ refl -×Fc.×β₁
-- ∙ (sym $ F .F-seq _ _ )
-- ∙ cong (F .F-hom) -×c.×β₁
-- ∙ F .F-seq _ _
-- ∙ cong₂ D._⋆_ (sym -×Fc.×β₁) refl
-- ∙ D.⋆Assoc _ _ _
-- ∙ cong₂ D._⋆_ refl (sym -×Fc.×β₁)
-- ∙ (sym $ D.⋆Assoc _ _ _))
-- (D.⋆Assoc _ _ _
-- ∙ cong₂ D._⋆_ refl -×Fc.×β₂
-- ∙ (sym $ F .F-seq _ _ )
-- ∙ cong (F .F-hom) -×c.×β₂
-- ∙ (sym -×Fc.×β₂)
-- ∙ cong₂ D._⋆_ refl (sym -×Fc.×β₂)
-- ∙ (sym $ D.⋆Assoc _ _ _))
-- -- We can build this NatTrans/Iso concretely for products, but
-- -- this should be constructible for a general functor comprehension
-- -- I believe its more complex for the abstract case because you
-- -- need to reason about a profunctor heteromorphism mediated by F
-- --
-- -- That is,
-- -- -×c.×aF is replaced with comprehension of S : Profunctor C C ℓS
-- -- -×Fc.×aF is replaced with comprehension of R : Profunctor D D ℓR
-- -- and we have a ProfHet F F S R
-- -- i.e. a natural transformation S ⇒ precomposeF (F ^op) ∘F R ∘F F
-- prodStrNatIso : NatIso (F ∘F -×c.×aF) (-×Fc.×aF ∘F F)
-- prodStrNatIso .NatIso.trans = prodStrNatTrans
-- prodStrNatIso .NatIso.nIso c =
-- isiso
-- (the-is-iso .fst -×Fc.×ue.element)
-- (-×Fc.×ue.intro-natural
-- ∙ -×Fc.×ue.intro≡
-- (the-is-iso .snd .fst -×Fc.×ue.element
-- ∙ sym (PresheafNotation.⋆IdL (BinProductProf D ⟅ _ ⟆) -×Fc.×ue.element)))
-- (F⟨-×c⟩.×ue.intro-natural
-- ∙ F⟨-×c⟩.×ue.intro≡
-- (-×Fc.×ue.universal ((F ∘F -×c.×aF) .F-ob c) .equiv-proof
-- (F-hom F (-×c.×ue.element .fst) , F-hom F (-×c.×ue.element .snd))
-- .fst .snd
-- ∙ sym (PresheafNotation.⋆IdL (BinProductProf D ⟅ _ ⟆) _)))
-- where
-- the-is-iso = isEquivToIsIso _ (F-× c ((-×Fc.×aF ∘F F) .F-ob c))
-- module _
-- (π₁*C : ∀ {Γ} →
-- (Γᴰ : Cᴰ.ob[ Γ ]) → CartesianLift Cᴰ Γᴰ -×c.π₁)
-- (π₁*D : ∀ {Δ} →
-- (Δᴰ : Dᴰ.ob[ Δ ]) → CartesianLift Dᴰ Δᴰ -×Fc.π₁)
-- where
-- private
-- module ∀ⱽCᴰ = UniversalQuantifierPsh -×c π₁*C
-- ∀ⱽPshCᴰ = ∀ⱽCᴰ.∀ⱽPsh
-- module ∀ⱽDᴰ = UniversalQuantifierPsh -×Fc π₁*D
-- ∀ⱽPshDᴰ = ∀ⱽDᴰ.∀ⱽPsh
-- module Fᴰ-weakening (Fᴰ : Functorᴰ F Cᴰ Dᴰ) where
-- Fᴰ-weakening-NatTransᴰ :
-- NatTransᴰ prodStrNatTrans
-- (Fᴰ ∘Fᴰ ∀ⱽCᴰ.weakenπFᴰ)
-- (∀ⱽDᴰ.weakenπFᴰ ∘Fᴰ Fᴰ)
-- Fᴰ-weakening-NatTransᴰ .NatTransᴰ.N-obᴰ xᴰ =
-- ∀ⱽDᴰ.introπF* $
-- Dᴰ.reind (cong (F .F-hom) (C.⋆IdL _) ∙ (sym -×Fc.×β₁)) $
-- Fᴰ .F-homᴰ (elementⱽ (π₁*C xᴰ))
-- Fᴰ-weakening-NatTransᴰ .NatTransᴰ.N-homᴰ fᴰ =
-- Dᴰ.rectify $ Dᴰ.≡out $
-- introᴰ-natural (π₁*D _)
-- ∙ introᴰ≡ (π₁*D _)
-- (change-base (D._⋆ -×Fc.π₁) D.isSetHom
-- (-×Fc.,p-extensionality
-- (D.⋆Assoc _ _ _
-- ∙ D.⟨ refl ⟩⋆⟨ -×Fc.×β₁ ⟩
-- ∙ (sym $ F .F-seq _ _)
-- ∙ cong (F .F-hom) (-×c.×β₁)
-- ∙ F .F-seq _ _
-- ∙ D.⟨ sym -×Fc.×β₁ ⟩⋆⟨ refl ⟩
-- ∙ D.⋆Assoc _ _ _
-- ∙ D.⟨ refl ⟩⋆⟨ sym -×Fc.×β₁ ⟩
-- ∙ (sym $ D.⋆Assoc _ _ _))
-- (D.⋆Assoc _ _ _
-- ∙ D.⟨ refl ⟩⋆⟨ -×Fc.×β₂ ⟩
-- ∙ (sym $ F .F-seq _ _)
-- ∙ cong (F .F-hom) (-×c.×β₂)
-- ∙ sym -×Fc.×β₂
-- ∙ D.⟨ refl ⟩⋆⟨ sym -×Fc.×β₂ ⟩
-- ∙ (sym $ D.⋆Assoc _ _ _))
-- ∙ (sym $ D.⋆IdR _))
-- ((sym $ Dᴰ.reind-filler _)
-- ∙ Dᴰ.⟨ refl ⟩⋆⟨ sym $ Dᴰ.reind-filler _ ⟩
-- ∙ (sym $ ∫.∫F Fᴰ .F-seq _ _)
-- ∙ cong (∫.∫F Fᴰ .F-hom)
-- (∀ⱽCᴰ.βᴰ-πF* _
-- ∙ (sym $ Cᴰ.reind-filler _)
-- ∙ Cᴰ.⟨ sym $ Cᴰ.reind-filler _ ⟩⋆⟨ refl ⟩ )
-- ∙ ∫.∫F Fᴰ .F-seq _ _
-- ∙ Dᴰ.⟨ Dᴰ.reind-filler _ ⟩⋆⟨ refl ⟩
-- ∙ Dᴰ.⟨ sym (∀ⱽDᴰ.βᴰ-πF* _) ⟩⋆⟨ refl ⟩
-- ∙ Dᴰ.⋆Assoc _ _ _
-- ∙ Dᴰ.⟨ refl ⟩⋆⟨ Dᴰ.⟨ Dᴰ.reind-filler _ ⟩⋆⟨ refl ⟩ ∙ Dᴰ.reind-filler _ ⟩
-- ∙ Dᴰ.reind-filler _
-- ∙ sym (∀ⱽDᴰ.βᴰ-πF* _)
-- ∙ Dᴰ.⟨ sym (introᴰ-natural (π₁*D _)) ⟩⋆⟨ refl ⟩
-- ∙ Dᴰ.reind-filler _))
-- Fᴰ-weakening-isNatIsoᴰ-Ty : Type _
-- Fᴰ-weakening-isNatIsoᴰ-Ty =
-- ∀ {x} (xᴰ : Cᴰ.ob[ x ]) →
-- isIsoᴰ Dᴰ (prodStrNatIso .NatIso.nIso x) (Fᴰ-weakening-NatTransᴰ .NatTransᴰ.N-obᴰ xᴰ)
-- module _
-- (Fᴰ-weakening-isNatIsoᴰ : Fᴰ-weakening-isNatIsoᴰ-Ty)
-- where
-- private
-- Fᴰ-weakening-NatIsoᴰ :
-- NatIsoᴰ prodStrNatIso
-- (Fᴰ ∘Fᴰ ∀ⱽCᴰ.weakenπFᴰ)
-- (∀ⱽDᴰ.weakenπFᴰ ∘Fᴰ Fᴰ)
-- Fᴰ-weakening-NatIsoᴰ = record {
-- transᴰ = Fᴰ-weakening-NatTransᴰ
-- ; nIsoᴰ = Fᴰ-weakening-isNatIsoᴰ }
-- module _ {Γ : C.ob} (Qⱽ : Presheafⱽ (F ⟅ Γ ⟆ -×Fc.×a) Dᴰ ℓQᴰ) where
-- private
-- module Qⱽ = PresheafⱽNotation Qⱽ
-- module ∀ⱽPshDᴰ =
-- PresheafⱽNotation (∀ⱽPshDᴰ Qⱽ)
-- module ∀ⱽPshCᴰ =
-- PresheafⱽNotation (∀ⱽPshCᴰ (reindHet' mapProdStrPshHet Fᴰ Qⱽ))
-- -- This can likely be simplified using the UMP of the
-- -- quantifier
-- -- Furhter, any mention of makePshHomPath will
-- -- be replaced when we finish porting our manual PshHoms
-- -- to the locally small category of presheaves
-- reindHet∀PshIsoⱽ :
-- PshIsoⱽ
-- (reindHet' (Functor→PshHet F Γ) Fᴰ (∀ⱽPshDᴰ Qⱽ))
-- (∀ⱽPshCᴰ (reindHet' mapProdStrPshHet Fᴰ Qⱽ))
-- reindHet∀PshIsoⱽ =
-- reindPshIsoⱽ (Functor→PshHet F Γ) reindFuncCompIsoⱽ
-- ⋆PshIsoⱽ reind-seqIsoⱽ _ _ _
-- ⋆PshIsoⱽ reindPshIsoⱽ (Functor→PshHet F Γ ⋆PshHom
-- (Functor→PshHet -×Fc.×aF (F-ob F Γ) ∘ˡ F)) (reind-introIsoⱽ (NatIsoᴰ→PshIsoᴰ (symNatIsoᴰ the-nat-isoᴰ)))
-- ⋆PshIsoⱽ reind-seqIsoⱽ _ _ _
-- ⋆PshIsoⱽ
-- reindPathIsoⱽ
-- (makePshHomPath (funExt₂ λ x p →
-- cong₂ D._⋆_ (D.⋆IdL _ ∙ D.⋆IdR _) refl
-- ∙ (sym $ prodStrNatIso .NatIso.trans .NatTrans.N-hom p)))
-- ⋆PshIsoⱽ invPshIsoⱽ (reind-seqIsoⱽ _ _ _)
-- ⋆PshIsoⱽ reindPshIsoⱽ (Functor→PshHet -×c.×aF Γ) annotateType
-- where
-- -- To avoid ugly goals with many reinds,
-- -- we construct the core of the PshIsoⱽ
-- -- as this NatIsoᴰ. We then turn it into a PshIsoᴰ,
-- -- turn that PshIsoᴰ into a PshIsoⱽ, and patch up
-- -- the necessary reinds in between
-- the-nat-isoᴰ :
-- NatIsoᴰ _
-- ((Qⱽ ∘Fᴰ (Fᴰ ^opFᴰ)) ∘Fᴰ (∀ⱽCᴰ.weakenπFᴰ ^opFᴰ))
-- ((Qⱽ ∘Fᴰ (∀ⱽDᴰ.weakenπFᴰ ^opFᴰ)) ∘Fᴰ (Fᴰ ^opFᴰ))
-- the-nat-isoᴰ =
-- (symNatIsoᴰ $ CATᴰ⋆Assoc _ _ _)
-- ⋆NatIsoᴰ (Qⱽ ∘ʳᴰⁱ
-- (∘Fᴰ-^opFᴰ-NatIsoᴰ ∀ⱽCᴰ.weakenπFᴰ Fᴰ
-- ⋆NatIsoᴰ opNatIsoᴰ (symNatIsoᴰ Fᴰ-weakening-NatIsoᴰ)
-- ⋆NatIsoᴰ (symNatIsoᴰ $ ∘Fᴰ-^opFᴰ-NatIsoᴰ Fᴰ ∀ⱽDᴰ.weakenπFᴰ)))
-- ⋆NatIsoᴰ CATᴰ⋆Assoc _ _ _
-- -- This is needed because there is not enough inference if
-- -- eqToPshIsoⱽ is just used inline above
-- -- sameissue as reindFuncUnitEq in
-- -- Displayed.Presheaf.Constructions.Unit.Properties
-- annotateType :
-- PshIsoⱽ
-- (reind (mapProdStrPshHet ∘ˡ -×c.×aF)
-- ((Qⱽ ∘Fᴰ (Fᴰ ^opFᴰ)) ∘Fᴰ (∀ⱽCᴰ.weakenπFᴰ ^opFᴰ)))
-- (reindHet' mapProdStrPshHet Fᴰ Qⱽ
-- ∘Fᴰ (∀ⱽCᴰ.weakenπFᴰ ^opFᴰ))
-- annotateType = eqToPshIsoⱽ (Eq.refl , Eq.refl)