Other Agda modules in this section (31)
- Equivalences
- Factorizations
- Identifications.EndpointTransport
- Identifications.EvaluationFrames
- Identifications.FunctorCoherence
- Identifications.Inverses
- Identifications.OverBase
- Identifications.ProjectedFactorization
- Identifications.RestrictionDiagrams
- Identifications.SectionEvaluation
- Identifications.TriangleCoherence
- Identifications.Triangles
- ProductConstructions
- Products.BinaryFunctors
- Products.Equivalences
- Products.FirstFactorSubstitution
- Products.FramedComparisons
- Products.PairedVertexFrames
- Products.Pairing
- Products.PairingRestriction
- Products.PairingSquares
- Products.ProductFunctor
- Products.ProductFunctorCoherence
- Products.ProductPairing
- Products.ProductPairingComposition
- Products.ProductPairingIdentity
- Products.ProductRestriction
- Products.TripleEvaluationOuterImage
- RelativeFunctors
- Squares
- WhiskeringEquivalence
# Squares of identifications: compatibility import The implementation moved to Section02 to support the early naturality calculus. This path reexports the same definitions and proof bodies. ```agda {-# OPTIONS --without-K #-} module SCT.VolumeI.Chapter01.Section03.Identifications.IdentificationSquares where open import SCT.VolumeI.Chapter01.Section02.IdentificationSquares public ```