Other Agda modules in this section (34)
- Equivalences
- Factorizations
- Identifications.EndpointTransport
- Identifications.FunctorCoherence
- Identifications.Inverses
- Identifications.OverBase
- Identifications.ProjectedFactorization
- Identifications.RestrictionDiagrams
- Identifications.RetractionCoherence
- Identifications.SectionEvaluation
- Identifications.TriangleCoherence
- Identifications.Triangles
- ProductConstructions
- Products.BinaryFunctors
- Products.Equivalences
- Products.FirstFactorSubstitution
- Products.PairedVertexFrames
- Products.Pairing
- Products.PairingOverBase
- Products.PairingRestriction
- Products.PairingSquares
- Products.ProductFunctor
- Products.ProductFunctorCoherence
- Products.ProductPairing
- Products.ProductPairingComposition
- Products.ProductPairingIdentity
- Products.ProductRestriction
- Products.TripleEvaluationOuterImage
- RelativeFunctors
- RetractLoops
- Retracts
- Squares
- Supporting
- WhiskeringEquivalence
Chapter 1, rebuild2, checked 14 October 2026 · source revision b982f5a.
# 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 ```