Transport along equal protected stages and chains

The transfinite construction compares restrictions whose stage types are only propositionally equal. These pointwise transport operations keep all large dependent elimination out of the coherence proofs.

noncomputable def ScottishBook155.ProtectedStage.castSourcePoint {r : ℝ} {A B : ProtectedStage r} (h : A = B) : A.source.carrier → B.source.carrier

Transport a source point along equality of protected stages.

Equations

• ScottishBook155.ProtectedStage.castSourcePoint h = Eq.ndrec (motive := fun {B : ScottishBook155.ProtectedStage r} => A.source.carrier → B.source.carrier) id h

noncomputable def ScottishBook155.ProtectedStage.castTargetPoint {r : ℝ} {A B : ProtectedStage r} (h : A = B) : A.target.carrier → B.target.carrier

Transport a target point along equality of protected stages.

Equations

• ScottishBook155.ProtectedStage.castTargetPoint h = Eq.ndrec (motive := fun {B : ScottishBook155.ProtectedStage r} => A.target.carrier → B.target.carrier) id h

@[simp]

theorem ScottishBook155.ProtectedStage.castSourcePoint_rfl {r : ℝ} {A : ProtectedStage r} (h : A = A) (x : A.source.carrier) : castSourcePoint h x = x

@[simp]

theorem ScottishBook155.ProtectedStage.castTargetPoint_rfl {r : ℝ} {A : ProtectedStage r} (h : A = A) (x : A.target.carrier) : castTargetPoint h x = x

theorem ScottishBook155.ProtectedStage.castSourcePoint_trans {r : ℝ} {A B C : ProtectedStage r} (h : A = B) (h' : B = C) (x : A.source.carrier) : castSourcePoint h' (castSourcePoint h x) = castSourcePoint ⋯ x

theorem ScottishBook155.ProtectedStage.castTargetPoint_trans {r : ℝ} {A B C : ProtectedStage r} (h : A = B) (h' : B = C) (x : A.target.carrier) : castTargetPoint h' (castTargetPoint h x) = castTargetPoint ⋯ x

@[simp]

theorem ScottishBook155.ProtectedStage.castSourcePoint_symm_apply {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : A.source.carrier) : castSourcePoint ⋯ (castSourcePoint h x) = x

theorem ScottishBook155.ProtectedStage.castSourcePoint_apply_symm {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : B.source.carrier) : castSourcePoint h (castSourcePoint ⋯ x) = x

@[simp]

theorem ScottishBook155.ProtectedStage.castTargetPoint_symm_apply {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : A.target.carrier) : castTargetPoint ⋯ (castTargetPoint h x) = x

theorem ScottishBook155.ProtectedStage.castTargetPoint_apply_symm {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : B.target.carrier) : castTargetPoint h (castTargetPoint ⋯ x) = x

noncomputable def ScottishBook155.ProtectedLink.castSource {r L : ℝ} {A A' B : ProtectedStage r} (h : A = A') (P : ProtectedLink A B L) : ProtectedLink A' B L

Change the source stage of a protected link along an equality.

Equations

• ScottishBook155.ProtectedLink.castSource h P = h ▸ P

theorem ScottishBook155.ProtectedLink.castSource_sourceEmbedding {r L : ℝ} {A A' B : ProtectedStage r} (h : A = A') (P : ProtectedLink A B L) (x : A'.source.carrier) : (castSource h P).sourceEmbedding x = P.sourceEmbedding (ProtectedStage.castSourcePoint ⋯ x)

theorem ScottishBook155.ProtectedLink.castSource_sourceProjection {r L : ℝ} {A A' B : ProtectedStage r} (h : A = A') (P : ProtectedLink A B L) (z : B.source.carrier) : (castSource h P).sourceProjection z = ProtectedStage.castSourcePoint h (P.sourceProjection z)

theorem ScottishBook155.ProtectedLink.castSource_targetEmbedding {r L : ℝ} {A A' B : ProtectedStage r} (h : A = A') (P : ProtectedLink A B L) (x : A'.target.carrier) : (castSource h P).targetEmbedding x = P.targetEmbedding (ProtectedStage.castTargetPoint ⋯ x)

theorem ScottishBook155.ProtectedLink.castSource_targetProjection {r L : ℝ} {A A' B : ProtectedStage r} (h : A = A') (P : ProtectedLink A B L) (z : B.target.carrier) : (castSource h P).targetProjection z = ProtectedStage.castTargetPoint h (P.targetProjection z)

noncomputable def ScottishBook155.ProtectedChain.transportSourceSystem {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).source.carrier) : CoherentBiSystem fun (i : ι) => (T i).source.carrier

Transport a source bidirectional system along equality of its protected stage family.

Equations

• ScottishBook155.ProtectedChain.transportSourceSystem h B = h ▸ B

noncomputable def ScottishBook155.ProtectedChain.transportTargetSystem {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).target.carrier) : CoherentBiSystem fun (i : ι) => (T i).target.carrier

Transport a target bidirectional system along equality of its protected stage family.

Equations

• ScottishBook155.ProtectedChain.transportTargetSystem h B = h ▸ B

theorem ScottishBook155.ProtectedChain.transportSourceSystem_embed {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).source.carrier) (i k : ι) (hik : i ≤ k) (x : (T i).source.carrier) : ((transportSourceSystem h B).embed i k hik) x = ProtectedStage.castSourcePoint ⋯ ((B.embed i k hik) (ProtectedStage.castSourcePoint ⋯ x))

theorem ScottishBook155.ProtectedChain.transportSourceSystem_project {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).source.carrier) (i k : ι) (hik : i ≤ k) (z : (T k).source.carrier) : ((transportSourceSystem h B).project i k hik) z = ProtectedStage.castSourcePoint ⋯ ((B.project i k hik) (ProtectedStage.castSourcePoint ⋯ z))

theorem ScottishBook155.ProtectedChain.transportTargetSystem_embed {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).target.carrier) (i k : ι) (hik : i ≤ k) (x : (T i).target.carrier) : ((transportTargetSystem h B).embed i k hik) x = ProtectedStage.castTargetPoint ⋯ ((B.embed i k hik) (ProtectedStage.castTargetPoint ⋯ x))

theorem ScottishBook155.ProtectedChain.transportTargetSystem_project {ι : Type} [LinearOrder ι] {r : ℝ} {S T : ι → ProtectedStage r} (h : S = T) (B : CoherentBiSystem fun (i : ι) => (S i).target.carrier) (i k : ι) (hik : i ≤ k) (z : (T k).target.carrier) : ((transportTargetSystem h B).project i k hik) z = ProtectedStage.castTargetPoint ⋯ ((B.project i k hik) (ProtectedStage.castTargetPoint ⋯ z))

theorem ScottishBook155.ProtectedChain.ext_transport {ι : Type} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (hstage : C.stage = D.stage) (hsource : transportSourceSystem hstage C.sourceSystem = D.sourceSystem) (htarget : transportTargetSystem hstage C.targetSystem = D.targetSystem) : C = D

Equality of protected chains from equality after transporting the two dependent bidirectional systems.

theorem ScottishBook155.ProtectedChain.source_embed_transport {ι : Type} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (h : C = D) (i k : ι) (hik : i ≤ k) (x : (C.stage i).source.carrier) : ProtectedStage.castSourcePoint ⋯ ((C.sourceSystem.embed i k hik) x) = (D.sourceSystem.embed i k hik) (ProtectedStage.castSourcePoint ⋯ x)

theorem ScottishBook155.ProtectedChain.target_embed_transport {ι : Type} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (h : C = D) (i k : ι) (hik : i ≤ k) (x : (C.stage i).target.carrier) : ProtectedStage.castTargetPoint ⋯ ((C.targetSystem.embed i k hik) x) = (D.targetSystem.embed i k hik) (ProtectedStage.castTargetPoint ⋯ x)

theorem ScottishBook155.ProtectedChain.source_project_transport {ι : Type} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (h : C = D) (i k : ι) (hik : i ≤ k) (z : (C.stage k).source.carrier) : ProtectedStage.castSourcePoint ⋯ ((C.sourceSystem.project i k hik) z) = (D.sourceSystem.project i k hik) (ProtectedStage.castSourcePoint ⋯ z)

theorem ScottishBook155.ProtectedChain.target_project_transport {ι : Type} [LinearOrder ι] {r L : ℝ} {C D : ProtectedChain r L} (h : C = D) (i k : ι) (hik : i ≤ k) (z : (C.stage k).target.carrier) : ProtectedStage.castTargetPoint ⋯ ((C.targetSystem.project i k hik) z) = (D.targetSystem.project i k hik) (ProtectedStage.castTargetPoint ⋯ z)