/-

Copyright (c) 2018 Ulrik Buchholtz. All rights reserved.

Released under Apache 2.0 license as described in the file LICENSE.

Authors: Floris van Doorn

-/

import .pointed_pi

open eq pointed equiv sigma is_equiv trunc option pi function fiber sigma.ops

namespace pointed

section bpmap

/- binary pointed maps -/

structure bpmap (A B C : Type*) : Type :=

(f : A → B →* C)

(q : Πb, f pt b = pt)

(r : q pt = respect_pt (f pt))

attribute [coercion] bpmap.f

variables {A B C D A' B' C' : Type*} {f f' : bpmap A B C}

definition respect_pt1 [unfold 4] (f : bpmap A B C) (b : B) : f pt b = pt :=

bpmap.q f b

definition respect_pt2 [unfold 4] (f : bpmap A B C) (a : A) : f a pt = pt :=

respect_pt (f a)

definition respect_ptpt [unfold 4] (f : bpmap A B C) : respect_pt1 f pt = respect_pt2 f pt :=

bpmap.r f

definition bpconst [constructor] (A B C : Type*) : bpmap A B C :=

bpmap.mk (λa, pconst B C) (λb, idp) idp

definition bppmap [constructor] (A B C : Type*) : Type* :=

pointed.MK (bpmap A B C) (bpconst A B C)

definition pmap_of_bpmap [constructor] (f : bppmap A B C) : ppmap A (ppmap B C) :=

begin

fapply pmap.mk,

{ intro a, exact pmap.mk (f a) (respect_pt2 f a) },

{ exact eq_of_phomotopy (phomotopy.mk (respect_pt1 f) (respect_ptpt f)) }

end

definition bpmap_of_pmap [constructor] (f : ppmap A (ppmap B C)) : bppmap A B C :=

begin

apply bpmap.mk (λa, f a) (ap010 pmap.to_fun (respect_pt f)),

exact respect_pt (phomotopy_of_eq (respect_pt f))

end

protected definition bpmap.sigma_char [constructor] (A B C : Type*) :

bpmap A B C ≃ Σ(f : A → B →* C) (q : Πb, f pt b = pt), q pt = respect_pt (f pt) :=

begin

fapply equiv.MK,

{ intro f, exact ⟨f, respect_pt1 f, respect_ptpt f⟩ },

{ intro fqr, exact bpmap.mk fqr.1 fqr.2.1 fqr.2.2 },

{ intro fqr, induction fqr with f qr, induction qr with q r, reflexivity },

{ intro f, induction f, reflexivity }

end

definition to_homotopy_pt_square {f g : A →* B} (h : f ~* g) :

square (respect_pt f) (respect_pt g) (h pt) idp :=

square_of_eq (to_homotopy_pt h)⁻¹

definition bpmap_eq_equiv [constructor] (f f' : bpmap A B C):

f = f' ≃ Σ(h : Πa, f a ~* f' a) (q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp), cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))

vrfl ids

(q pt) (to_homotopy_pt_square (h pt)) :=

begin

refine eq_equiv_fn_eq (bpmap.sigma_char A B C) f f' ⬝e _,

refine !sigma_eq_equiv ⬝e _, esimp,

refine sigma_equiv_sigma (!eq_equiv_homotopy ⬝e pi_equiv_pi_right (λa, !pmap_eq_equiv)) _,

intro h, exact sorry

end

definition bpmap_eq [constructor] (h : Πa, f a ~* f' a)

(q : Πb, square (respect_pt1 f b) (respect_pt1 f' b) (h pt b) idp)

(r : cube (vdeg_square (respect_ptpt f)) (vdeg_square (respect_ptpt f'))

vrfl ids

(q pt) (to_homotopy_pt_square (h pt))) : f = f' :=

(bpmap_eq_equiv f f')⁻¹ᵉ ⟨h, q, r⟩

definition pmap_equiv_bpmap [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=

begin

refine !pmap.sigma_char ⬝e _ ⬝e !bpmap.sigma_char⁻¹ᵉ,

refine sigma_equiv_sigma_right (λf, pmap_eq_equiv (f pt) !pconst) ⬝e _,

refine sigma_equiv_sigma_right (λf, !phomotopy.sigma_char)

end

definition pmap_equiv_bpmap' [constructor] (A B C : Type*) : pmap A (ppmap B C) ≃ bpmap A B C :=

begin

refine equiv_change_fun (pmap_equiv_bpmap A B C) _,

exact bpmap_of_pmap, intro f, reflexivity

end

definition ppmap_pequiv_bppmap [constructor] (A B C : Type*) :

ppmap A (ppmap B C) ≃* bppmap A B C :=

pequiv_of_equiv (pmap_equiv_bpmap' A B C) idp

definition bpmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C')

(k : bpmap A B C) : bpmap A' B' C' :=

begin

fapply bpmap.mk (λa', h ∘* k (f a') ∘* g),

{ intro b', refine ap h _ ⬝ respect_pt h,

exact ap010 (λa b, k a b) (respect_pt f) (g b') ⬝ respect_pt1 k (g b') },

{ apply whisker_right, apply ap02 h, esimp,

induction A with A a₀, induction B with B b₀, induction f with f f₀, induction g with g g₀,

esimp at *, induction f₀, induction g₀, esimp, apply whisker_left, exact respect_ptpt k },

end

definition bppmap_functor [constructor] (f : A' →* A) (g : B' →* B) (h : C →* C') :

bppmap A B C →* bppmap A' B' C' :=

begin

apply pmap.mk (bpmap_functor f g h),

induction A with A a₀, induction B with B b₀, induction C' with C' c₀',

induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,

induction f₀, induction g₀, induction h₀,

reflexivity

end

definition ppcompose_left' [constructor] (g : B →* C) : ppmap A B →* ppmap A C :=

pmap.mk (pcompose g)

begin induction C with C c₀, induction g with g g₀, esimp at *, induction g₀, reflexivity end

definition ppcompose_right' [constructor] (f : A →* B) : ppmap B C →* ppmap A C :=

pmap.mk (λg, g ∘* f)

begin induction B with B b₀, induction f with f f₀, esimp at *, induction f₀, reflexivity end

definition ppmap_pequiv_bppmap_natural (f : A' →* A) (g : B' →* B) (h : C →* C') :

psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A' B' C')

(ppcompose_right' f ∘* ppcompose_left' (ppcompose_right' g ∘* ppcompose_left' h))

(bppmap_functor f g h) :=

begin

induction A with A a₀, induction B with B b₀, induction C' with C' c₀',

induction f with f f₀, induction g with g g₀, induction h with h h₀, esimp at *,

induction f₀, induction g₀, induction h₀,

fapply phomotopy.mk,

{ intro k, fapply bpmap_eq,

{ intro a, exact !passoc⁻¹* },

{ intro b, apply vdeg_square, esimp,

refine ap02 _ !idp_con ⬝ _ ⬝ (ap (λx, ap010 pmap.to_fun x b) !idp_con)⁻¹ᵖ,

refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },

{ exact sorry }},

{ exact sorry }

end

/- maybe this is useful for pointed naturality in C? -/

definition ppmap_pequiv_bppmap_natural_right (h : C →* C') :

psquare (ppmap_pequiv_bppmap A B C) (ppmap_pequiv_bppmap A B C')

(ppcompose_left' (ppcompose_left' h))

(bppmap_functor !pid !pid h) :=

begin

induction A with A a₀, induction B with B b₀, induction C' with C' c₀',

induction h with h h₀, esimp at *, induction h₀,

fapply phomotopy.mk,

{ intro k, fapply bpmap_eq,

{ intro a, exact pwhisker_left _ !pcompose_pid },

{ intro b, apply vdeg_square, esimp,

refine ap02 _ !idp_con ⬝ _,

refine ap02 _ !ap_eq_ap010⁻¹ ⬝ !ap_compose' ⬝ !ap_compose ⬝ !ap_eq_ap010 },

{ exact sorry }},

{ exact sorry }

end

end bpmap

/- fiberwise pointed maps -/

structure dbpmap {A : Type*} (B C : A → Type*) : Type :=

(f : Πa, B a →* C a)

(q : Πb, f pt b = pt)

(r : q pt = respect_pt (f pt))

attribute [coercion] dbpmap.f

variables {A A' : Type*} {B C : A → Type*} {B' C' : A' → Type*} {f f' : dbpmap B C}

definition respect_ptd1 [unfold 4] (f : dbpmap B C) (b : B pt) : f pt b = pt :=

dbpmap.q f b

definition respect_ptd2 [unfold 4] (f : dbpmap B C) (a : A) : f a pt = pt :=

respect_pt (f a)

definition respect_dptpt [unfold 4] (f : dbpmap B C) : respect_ptd1 f pt = respect_ptd2 f pt :=

dbpmap.r f

definition dbpconst [constructor] (B C : A → Type*) : dbpmap B C :=

dbpmap.mk (λa, pconst (B a) (C a)) (λb, idp) idp

definition dbppmap [constructor] (B C : A → Type*) : Type* :=

pointed.MK (dbpmap B C) (dbpconst B C)

definition ppi_of_dbpmap [constructor] (f : dbppmap B C) : Π*a, B a →** C a :=

begin

fapply ppi.mk,

{ intro a, exact pmap.mk (f a) (respect_ptd2 f a) },

{ exact eq_of_phomotopy (phomotopy.mk (respect_ptd1 f) (respect_dptpt f)) }

end

definition dbpmap_of_ppi [constructor] (f : Π*a, B a →** C a) : dbppmap B C :=

begin

apply dbpmap.mk (λa, f a) (ap010 pmap.to_fun (respect_pt f)),

exact respect_pt (phomotopy_of_eq (respect_pt f))

end

protected definition dbpmap.sigma_char [constructor] (B C : A → Type*) :

dbpmap B C ≃ Σ(f : Πa, B a →* C a) (q : Πb, f pt b = pt), q pt = respect_pt (f pt) :=

begin

fapply equiv.MK,

{ intro f, exact ⟨f, respect_ptd1 f, respect_dptpt f⟩ },

{ intro fqr, exact dbpmap.mk fqr.1 fqr.2.1 fqr.2.2 },

{ intro fqr, induction fqr with f qr, induction qr with q r, reflexivity },

{ intro f, induction f, reflexivity }

end

definition dbpmap_eq_equiv [constructor] (f f' : dbpmap B C):

f = f' ≃ Σ(h : Πa, f a ~* f' a) (q : Πb, square (respect_ptd1 f b) (respect_ptd1 f' b) (h pt b) idp), cube (vdeg_square (respect_dptpt f)) (vdeg_square (respect_dptpt f'))

vrfl ids

(q pt) (to_homotopy_pt_square (h pt)) :=

begin

refine eq_equiv_fn_eq (dbpmap.sigma_char B C) f f' ⬝e _,

refine !sigma_eq_equiv ⬝e _, esimp,

refine sigma_equiv_sigma (!eq_equiv_homotopy ⬝e pi_equiv_pi_right (λa, !pmap_eq_equiv)) _,

intro h, exact sorry

end

definition dbpmap_eq [constructor] (h : Πa, f a ~* f' a)

(q : Πb, square (respect_ptd1 f b) (respect_ptd1 f' b) (h pt b) idp)

(r : cube (vdeg_square (respect_dptpt f)) (vdeg_square (respect_dptpt f'))

vrfl ids

(q pt) (to_homotopy_pt_square (h pt))) : f = f' :=

(dbpmap_eq_equiv f f')⁻¹ᵉ ⟨h, q, r⟩

definition ppi_equiv_dbpmap [constructor] (B C : A → Type*) : (Π*a, B a →** C a) ≃ dbpmap B C :=

begin

refine !ppi.sigma_char ⬝e _ ⬝e !dbpmap.sigma_char⁻¹ᵉ,

refine sigma_equiv_sigma_right (λf, pmap_eq_equiv (f pt) !pconst) ⬝e _,

refine sigma_equiv_sigma_right (λf, !phomotopy.sigma_char)

end

definition ppi_equiv_dbpmap' [constructor] (B C : A → Type*) : (Π*a, B a →** C a) ≃ dbpmap B C :=

begin

refine equiv_change_fun (ppi_equiv_dbpmap B C) _,

exact dbpmap_of_ppi, intro f, reflexivity

end

definition pppi_pequiv_dbppmap [constructor] (B C : A → Type*) :

(Π*a, B a →** C a) ≃* dbppmap B C :=

pequiv_of_equiv (ppi_equiv_dbpmap' B C) idp

definition dbpmap_functor [constructor] (f : A' →* A) (g : Πa, B' a →* B (f a)) (h : Πa, C (f a) →* C' a)

(k : dbpmap B C) : dbpmap B' C' :=

begin

fapply dbpmap.mk (λa', h a' ∘* k (f a') ∘* g a'),

{ intro b', refine ap (h pt) _ ⬝ respect_pt (h pt),

exact sorry }, --ap010 (λa b, k a b) (respect_pt f) (g pt b') ⬝ respect_ptd1 k (g pt b') },

{ exact sorry },

-- apply whisker_right, apply ap02 h, esimp,

-- induction A with A a₀, induction B with B b₀, induction f with f f₀, induction g with g g₀,

-- esimp at *, induction f₀, induction g₀, esimp, apply whisker_left, exact respect_dptpt k },

end

end pointed